Semantics-deeply-embedded
Deeply embedded semantics of PFCSes.
The semantics informally described in semantics
can be formalized, mathematically, as a function
with the following characteristics.
This mathematical semantic function takes the following inputs:
- A constraint, of type constraint.
- A list of definitions, of type definition-list.
- An assignment,
i.e. a finite map from variables to prime field elements.
- The prime.
The mathematical semantic function
returns one of the following possible outputs:
- The boolean `true', indicating that,
given the input list of definitions,
the input constraint is satisfied by the input assignment.
- The boolean `false', indicating that,
given the input list of definitions,
the input constraint is not satisfied by the input assignment.
- An error, indicating that,
given the input list of definitions,
the input constraint cannot be evaluated as satisfied or not.
The third output happens when, for instance,
the constraint references
a variable that is not in the assignment,
or a relation that is not in the list of definitions.
This should never happen when the list of definitions is well-formed, as we plan to prove formally.
Attempting to define this mathematical semantic function in ACL2
runs into an issue.
A constraint that is a call of a relation is satisfied
when all the constraints that form the body of the relation are satisfied,
in some assignment that extends the one that assigns
the actual parameters to the formal parameters.
This is an existential quantification,
which is expressed via defun-sk in ACL2,
but the mathematical semantic function we are describing is recursive,
and a mutual recursion cannot involve a defun-sk in ACL2.
To overcome this issue,
we formalize a logical proof system
to derive assertions about the mathematical semantic function,
and then we define the function in ACL2 in terms of the proof system.
Subtopics
- Exec-proof-tree
- Execute a proof tree.
- Assertion-list->constr-list
- Lift assertion->constr to lists.
- Assertion-list->asg-list
- Lift assertion->asg to lists.
- Eval-expr
- Evaluate an expression, given an assignment and a prime field.
- Eval-expr-list
- Lift eval-expr to lists.
- Assertion
- Fixtype of semantic assertions.
- Assignment-wfp
- Check if an assignment is well-formed.
- Proof-outcome
- Fixtype of semantic proof outcomes.
- Proof-list-outcome
- Fixtype of semantic proof list outcomes.
- Assertion-list-from
- Lift assertion to lists.
- Definition-satp
- Check if a sequence of prime field elements
satisfies a named PFCS definition.
- Constraint-satp
- Semantic function checking if a constaint is satisfied,
given a list of definitions, an assignment, and a prime field.
- Assignment
- Fixtype of assignments.
- System-satp
- Check if an assignment satisfies a system.
- Constraint-list-satp
- Semantic function saying if an assignment
satisfies a list of constraints,
given a list of definitions and a prime field.
- Assertion-list
- Fixtype of lists of semantic assertions.
- Assignment-list
- Fixtype of lists of assignments.
- Proof-trees
