|
|
|---|
|
|
|
|---|
Proof support for PFCSes.
PFCSes representing specific gadgets can be reasoned about (to prove properties of them, such as compliance to specifications) using either the shallowly or deeply embedded semantics. Both work fine for the case of fixed, completely defined PFCSes. However, to reason about parameterized families of PFCSes, such as a gadget to decompose a number into a varying number of bits (where the number of bits is a parameter), or even more simply a gadget parameterized over the choice of names of its variables, the deeply embedded semantics is needed.
The reason is that we can define an ACL2 function that takes the parameters as inputs and returns the corresponding gadget in PFCS abstract syntax, whose properties we can then prove, universally quantified over the aforementioned parameters (possibly with some restrictions on the parameters). This is only possible in the deeply embedded semantics, which treats the PFCS abstract syntax explicitly. In contrast, the shallowly embedded semantics turns fixed instances of PFCS abstract syntax into ACL2 predicates, without an easy way to parameterize them. It may be possible to extend the shallowly embedded semantics to recognize and take into account certain forms of parameterized PFCSes, or even extend PFCSes with forms of parameterization. It may be also possible to define ACL2 functions that generate both PFCS abstract syntax and associated proofs, based on the kind of parameters mentioned above. But for now, with PFCSes and their shallowly embedded semantics being what they are, the deeply embedded semantics must be used to reason about parameterized PFCSes.
However, the (deeply embedded) semantics of PFCSes is somewhat complicated, defined in terms of existentially quantified proof trees and their execution. The reason for that complication is discussed in semantics-deeply-embedded. The complication burdens the task to reason about PFCSes (whether parameterized or not) directly in terms of the deeply embedded semantics.
Therefore, here we provide functions and theorems (rules) to facilitate reasoning with the deeply embedded semantics. These let us dispense with explicitly dealing with proof trees, and instead have essentially alternative definitions of semantic predicates like constraint-satp that are expressed in simpler terms than via existentially quantified proof trees. (These alternative definitions could not be used as actual definitions, because of the recursion and existential quantification issues discussed in semantics-deeply-embedded.)
Currently we provide the following forms of proof support:
More proof rules may be added here in the future, but it should be clear from the list above that we already have rules to cover both kinds of single constraints as well as lists of constraints.