ATC tutorial: Treatment of ACL2 conditionals with mbt.
After describing how ACL2 conditionals represent C conditional statements and expressions (in atc-tutorial-conditional-statements and atc-tutorial-conditional-expressions), this tutorial page describes how certain ACL2 conditionals do not actually represent C conditional statements and expressions.
These are ACL2 conditionals whose tests are calls of mbt (or mbt$, which expands to mbt): only their `then' branches represent (and are translated to) C code; tests and `else' branches are ignored.
The argument of the built-in macro mbt
must be provably equal to
As explained in atc-tutorial-int-programs, ATC requires the target ACL2 functions to be guard-verified. Accordingly, as explained in atc-tutorial-events, the functional correctness theorems generated by ATC include the target functions' guards as hypotheses. In other words, ATC generates C code that matches the ACL2 code under the guards, which must be verified for ATC to generate code. Thus, the behavior of the ACL2 functions or of the C code outside the guards is irrelevant in some precise sense: so long as the ATC-generated code is called on values that satisfy the guards, the behavior is provably equivalent to the ACL2 counterpart. (Upcoming tutorial pages will describe more precisely this contract between ATC-generated code and external code.)
Given the above, it should be clear why ATC ignores (i.e. does not generate any C code for) mbt tests of ifs and corresponding `else' branches, treating this kind of conditionals as if they were just their `then' branches.
Conditionals with mbt tests are sometimes used in recursive ACL2 functions to ensure that termination can be proved. Recall that termination proofs ignore guards, which are extra-logical in ACL2 (i.e. not part of the logic itself, although they give rise to proof obligations expressed in the logic).
Another circumstance in which mbt may arise
is via certain APT transformations.
For instance, the apt::restrict transformation
generates a new function whose body has the form
For example, both the ACL2 function
(defun |f| (|x|) (declare (xargs :guard (c::sintp |x|))) (if (mbt (c::sintp |x|)) (c::lt-sint-sint |x| (c::sint-dec-const 100)) (list :this-is-not-translated-to-c)))
and the ACL2 function
(defun |f| (|x|) (declare (xargs :guard (c::sintp |x|))) (if (mbt$ (c::sintp |x|)) (c::lt-sint-sint |x| (c::sint-dec-const 100)) (list :this-is-not-translated-to-c)))
represent the C function
int f(int x) { return x < 100; }
which is, in fact, also equally represented by the ACL2 function
(defun |f| (|x|) (declare (xargs :guard (c::sintp |x|))) (c::lt-sint-sint |x| (c::sint-dec-const 100)))
Previous: ACL2 representation of C conditional expressions
Next: ACL2 representation of C conditional statements followed by more code