System-level-marking-view-proof-utilities
General-purpose code-proof libraries to include in the
system-level marking view (with A/D flag updates on)
When reasoning about an supervisor-mode program in the
system-level marking view of the x86 ISA model, include the
book x86isa/proofs/utilities/sys-view/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-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-in-marking-view.
- When monitoring
x86-fetch-decode-execute-opener-in-marking-view tells you
that a hypothesis involving get-prefixes-alt was not
rewritten to t:
Monitor
get-prefixes-alt-opener-lemma-no-prefix-byte.
Note that if the instruction under consideration has prefix
bytes, you should monitor one of these rules instead:
get-prefixes-alt-opener-lemma-group-1-prefix-in-marking-view
get-prefixes-alt-opener-lemma-group-2-prefix-in-marking-view
get-prefixes-alt-opener-lemma-group-3-prefix-in-marking-view
get-prefixes-alt-opener-lemma-group-4-prefix-in-marking-view.
Other useful rules involving get-prefixes-alt are:
get-prefixes-alt-and-wb-in-system-level-marking-view-disjoint-from-paging-structures
and
mv-nth-3-get-prefixes-alt-no-prefix-byte.
- When monitoring other rules above indicates that an
instruction is not being fetched successfully using rb-alt:
Monitor one-read-with-rb-alt-from-program-at-alt-in-marking-view.
- When monitoring other rules above indicates that ACL2 can't
resolve that the program remained unchanged (program-at-alt) after a write operation wb occurred:
Monitor program-at-alt-wb-disjoint-in-sys-view.
An instance of where monitoring this rule might be helpful is when
the program-at hypothesis of
one-read-with-rb-alt-from-program-at-alt-in-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-alt-from-program-at-alt-in-marking-view is
not being relieved.
- When reasoning about disjointness/overlap of memory regions:
Monitor one of these rules:
rb-alt-wb-equal-in-sys-view
rb-alt-wb-disjoint-in-sys-view
rb-alt-and-wb-to-paging-structures-disjoint
rb-wb-disjoint-in-sys-view
rb-wb-equal-in-sys-view
all-xlation-governing-entries-paddrs-and-mv-nth-1-wb-disjoint
la-to-pas-values-and-mv-nth-1-wb-disjoint-from-xlation-gov-addrs.
Note that rb is rewritten to rb-alt when the read is
being done from a program address.
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
- Rb-alt
- Unwind-x86-interpreter-in-marking-view
- Definitions of rules to monitor in the system-level marking view
- Program-at-alt
- Get-prefixes-alt
- Rewriting get-prefixes to get-prefixes-alt
- Get-prefixes-in-system-level-marking-view
- Rb-in-system-level-marking-view
- Xlate-equiv-memory-and-rml08
- Reasoning-about-page-tables
- Las-to-pas-two-n-ind-hint
- Find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux
- Replace-element
- Phys-mem-values-same
