|
|
|---|
|
|
|
|---|
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, needs the deeply embedded semantics. 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 parameters (perhaps 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 PFCS, or even extend PFCS 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 PFCS 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 extends to attempts to reason about PFCSes (whether parameterized or not) directly in terms of the defined semantics.
Fortunately, it should be possible to prove rules that facilitate reasoning with the deeply embedded semantics. These rules let us avoid dealing explcitly with proof trees. These rules are work in progress.