Non-marking-view-proof-utilities
General-purpose code-proof libraries to include in the
system-level non-marking view (with A/D flag updates off)
When reasoning about an supervisor-mode program in the
system-level non-marking view of the x86 ISA model, include
the book x86isa/proofs/utilities/sys-view/non-marking-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-non-marking-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-in-non-marking-view.
- 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-in-non-marking-view.
An instance of where monitoring this rule might be helpful is when
the program-at hypothesis of
one-read-with-rb-from-program-at-in-non-marking-view is not
being relieved.
- When inferring the canonical nature of a linear address:
Monitor member-p-canonical-address-listp.
This is useful if you believe that the canonical nature of a
linear address should be inferable from the canonical nature of a
list of addresses, of which that address is a member. An instance
of where monitoring this rule
might be helpful is when the member-p hypothesis of
one-read-with-rb-from-program-at-in-non-marking-view is not
being relieved.
- When reasoning about disjointness/overlap of memory regions:
rb-wb-disjoint-in-non-marking-view
rb-wb-equal-in-non-marking-view
la-to-pas-values-and-mv-nth-1-wb-disjoint-from-xlation-gov-addrs-in-non-marking-view
all-xlation-governing-entries-paddrs-and-mv-nth-1-wb-disjoint-in-non-marking-view
When symbolically simulating supervisor-mode programs, you might
also want to do the following, which replaces ACL2's default ancestor
check with something simpler:
(local (include-book "tools/trivial-ancestors-check" :dir :system))
(local (acl2::use-trivial-ancestors-check))
Subtopics
- Unwind-x86-interpreter-in-non-marking-view
- Definitions of rules to monitor in the system-level
non-marking view
