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.

- 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