App-view-proof-utilities
General-purpose code-proof libraries to include in the
application-level view
When reasoning about an application program in the
application-level view of the x86 ISA model, include the book
x86isa/proofs/utilities/app-view/top to make use of some
standard rules you would need to control the symbolic simulation of
the program.
If unwinding the (x86-run ... x86) expression during your
proof attempt does not result in a 'clean' expression (i.e., one
entirely in terms of updates made to the initial state as opposed to
in terms of x86-fetch-decode-execute or x86-run), then
there is a good chance that you're missing some preconditions, or
that the existing rules are not good enough. In any case, it can
help to monitor the existing rules to figure out what's
wrong. Feel free to send on suggestions for new rules or improving
existing ones!
You can monitor the following rules, depending on the kind of
subgoals you see, to get some clues. You can find definitions of
these rules in unwind-x86-interpreter-in-app-view.
- When the subgoal has calls of x86-run:
Monitor x86-run-opener-not-ms-not-zp-n.
- When the subgoal has calls of x86-fetch-decode-execute:
Monitor x86-fetch-decode-execute-opener.
- When monitoring x86-fetch-decode-execute-opener tells you
that a hypothesis involving get-prefixes was not rewritten
to t:
Monitor
get-prefixes-opener-lemma-no-prefix-byte or
get-prefixes-opener-lemma-no-legacy-prefix-but-rex-prefix.
Note that if the instruction under consideration has prefix
bytes, you should monitor one of these rules instead:
get-prefixes-opener-lemma-group-1-prefix
get-prefixes-opener-lemma-group-2-prefix
get-prefixes-opener-lemma-group-3-prefix
get-prefixes-opener-lemma-group-4-prefix.
- When monitoring other rules above indicates that an
instruction is not being fetched successfully using rb:
Monitor one-read-with-rb-from-program-at.
- When monitoring other rules above indicates that ACL2 can't
resolve that the program remained unchanged (program-at) after a write operation wb occurred:
Monitor program-at-wb-disjoint.
An instance of where monitoring this rule might be helpful is when
the program-at hypothesis of rb-in-terms-of-nth-and-pos
is not being relieved.
- When reasoning about disjointness/overlap of memory regions:
rb-wb-disjoint
rb-wb-subset
rb-wb-equal
separate-smaller-regions
separate-contiguous-regions
Subtopics
- Unwind-x86-interpreter-in-app-view
- Definitions of rules to monitor in the application-level
view
