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:

- A rule
`constraint-satp-of-equal`, to rewrite`constraint-satp`over an equality constraint to an alternative definition`constraint-equal-satp`, which is directly expressed in terms of the two expressions being equal and non-erroneous. - A rule
`constraint-satp-of-relation`, to rewrite`constraint-satp`over a relation application constraint to an alternative definition`constraint-relation-satp`, which is directly expressed in terms of the satisfaction of the suitably instantiated body of the relation. - Rules that decompose
`constraint-list-satp`into`constraint-satp`of the elements, specifically`constraint-list-satp-of-cons`and`constraint-list-satp-of-append`, along with rules`constraint-list-satp-of-nil`and`constraint-list-satp-of-atom`to resolve empty lists of constraints as alwasy satisfied. We also have a rule`constraint-list-satp-of-rev`that simplifies`rev`away, since constraint satisfaction is not ordered-dependent. - A rule that turns
`constraint-satp`of a relation constraint into`definition-satp`of the relation and of the values that the arguments evaluate to. This is useful for compositional proofs of PFCSes, because by reducing the satisfaction of an inner relation call, performed in the body of an outer relation, to the satisfaction of the definition of the inner relation, one can use properties proved about the inner relation to prove properties about the outer relation.

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.

- Constraint-relation-satp
- Satisfaction of a relation constraint, expressed without proof trees.
- Constraint-equal-satp
- Satisfaction of an equality constraint, expressed without proof trees.
- Constraint-relation-nofreevars-satp
- Satisfaction of a relation constraint without free variables, expressed without proof trees.
- Exec-proof-tree-when-constraint-relation
- Characterization of a proof tree for a relation constraint.
- Constraint-satp-of-relation
- Proof rule for relation application constraints.
- Exec-proof-tree-when-constraint-equal
- Characterization of a proof tree for an equality constraint.
- Constraint-satp-of-relation-when-nofreevars
- Proof rule for relation application constraints, for the case in which the relation has no free variables.
- Constraint-list-satp-of-atom
- Proof rule for the empty list of constraints expressed as any atom.
- Constraint-list-satp-of-cons
- Proof rule for a
`cons`list of constraints. - Constraint-satp-to-definition-satp
- Proof rule to turn relation constraint satisfaction to definition satisfaction.
- Constraint-satp-of-equal
- Proof rule for equality constraints.
- Constraint-list-satp-of-append
- Proof rule for the concatenation of lists of constraints.
- Constraint-list-satp-of-rev
- Proof rule for a reversed list of constraints.
- Constraint-list-satp-of-nil
- Proof rule for the empty list of constraint.