Proof-generation
Proof generation utilities.
We collect some proof generation utilities
that should be of general use.
ACL2 functions that carry out proof-generating transformations
have certain general inputs and outputs that are independent from
the constructs being transformed and even the specific transformations.
We provide data structures gin and gout
for these general inputs and outputs (the g stands for `general').
We provide functions to generate theorems for expression, statements, etc.
These functions take the old and new constructs as inputs,
which must be in the formalized subset,
and in some cases must satisfy additional restrictions.
The callers check these conditions,
but they are double-checked here,
throwing hard errors if not satisfied, which should never happen.
The theorems generated for the various constructs say that:
- If the execution of the old construct does not yield an error,
neither does the execution of the new construct,
and the two executions return the same results.
- If applicable to the construct,
the type of the result is consistent with the type, or set of types,
statically determined by the validator for the construct.
For statements and some other constructs,
the sets of types are actually sets of optional types,
where nil indicates termination without a return.
A void type indicates termination with a return without value.
Any other type indicates termination with a return
with a value of that type.
- If applicable to the construct,
if the computation state before the construct
includes certain variables with values of certain types,
the computation state after the construct
includes certain variables with values of certain types.
These are sometimes the same variables (e.g. for assignments),
but other times there are more variables at the end
(e.g. for declarations).
Some transformations turn C constructs into semantically equal ones.
If the sub-constructs of a super-construct
are turned into semantically equal ones,
with theorems asserting that semantic equalities,
those equalities can be lifted to the super-construct,
and a theorem for the super-construct can be generated,
with a proof that makes use of the theorems for the sub-constructs.
We provide some utilities to lift equalities in the manner just explained.
Together with the equalities, the theorems also assert
facts about the types of the constructs involved;
perhaps these could be teased apart in the future.
We also expect to generalize equalities to more complex relations,
in these or in other utilities in the future.
The utilities for these equality lifting have names
starting with xeq, to convey the idea of
transformations (x) according to equalities (eq).
Subtopics
- Xeq-fundef
- Equality lifting transformation of a function definition.
- Xeq-expr-binary
- Equality lifting transformation of a binary expression.
- Xeq-block-item-list-cons
- Equality lifting transformation of a non-empty list of block items.
- Xeq-stmt-ifelse
- Equality lifting transformation of an if-else statement.
- Xeq-expr-cond
- Equality lifting transformation of a conditional expression.
- Xeq-expr-const
- Equality transformation of a constant.
- Gen-param-thms
- Generate theorems about the parameters of a function.
- Gen-expr-thm
- Generate a theorem for the transformation of an expression.
- Gen-from-params
- Generate certain pieces of information
from the formal parameters of a function.
- Xeq-decl-decl
- Equality lifting transformation of a non-static-assert declaration.
- Xeq-expr-unary
- Equality lifting transformation of a unary expression.
- Xeq-stmt-dowhile
- Equality lifting transformation of a do-while loop.
- Xeq-expr-cast
- Equality lifting transformation of a cast expression.
- Lift-expr-pure-thm
- Lift a theorem for a pure expression
from c::exec-expr-pure to c::exec-expr.
- Xeq-stmt-while
- Equality lifting transformation of a while loop.
- Gout
- General outputs for transformation functions.
- Gen-block-item-list-thm
- Generate a theorem for the transformation of a list of block items.
- Xeq-stmt-if
- Equality lifting transformation of
an if statement (without else).
- Gin
- General inputs for transformation functions.
- Xeq-expr-ident
- Equality transformation of an identifier expression (i.e. variable).
- Gen-expr-pure-thm
- Generate a theorem for the transformation of a pure expression.
- Gen-block-item-thm
- Generate a theorem for the transformation of a block item.
- Xeq-stmt-expr
- Equality lifting transformation of an expression statement.
- Gen-initer-single-thm
- Generate a theorem for the transformation of a single initializer.
- Gen-init-scope-thm
- Generate a theorem about the initial scope of a function.
- Xeq-stmt-return
- Equality lifting transformation of a return statement.
- Gen-decl-thm
- Generate a theorem for the transformation of a declaration.
- Gen-stmt-thm
- Generate a theorem for the transformation of a statement.
- Xeq-block-item-decl
- Equality lifting transformation of
a block item that consists of a declaration.
- Xeq-initer-single
- Equality lifting transformation of
an initializer consisting of a single expression.
- Xeq-block-item-stmt
- Equality lifting transformation of
a block items that consists of a statement.
- Xeq-stmt-compound
- Equality lifting transformation of a compound statement.
- Gen-thm-name
- Generate a theorem name.
- Gin-update
- Update a gin with a gout.
- Gen-var-assertions
- Generate assertions about certain variables
having values of certain types in a computation state.
- Tyspecseq-to-type
- Map a type specifier sequence from the language formalization
to the corresponding type.
- Xeq-block-item-list-empty
- Equality lifting transformation of the empty list of block items.
- Gout-no-thm
- Build a gout without a theorem name.
- Irr-gout
- Irrelevant general outputs for transformation functions.
