The proof structure still largely follows Thibaut's scheme; this commit
merely adds some speedup, style cleanup, and documentation.
Unfortunately, the proof state seems to be just large enough that the
built-in record update ruleset runs into limitations, and the standard
clasimp tactics start to fail on subgoals in an unpredictable way.
This is ostensibly more principled than the earlier proof, which simply
unfolded all the monad combinators. However, there was also no existing
framework for using monad_commute, so we need to make one up just to
do this single proof.
Mainly repercusion of changes occuring for Access:
- Fix subjectReads and subjectAffects with new authorities
- SILC label is forbidden to contain any transferable cap
- Lots of lemma that required is_subject on their parameter now only
require aag_can_read when possible
- Major cleanup of the integrity ==> subjectAffects proofs for kheap,
CDT and user memory.
Integrity and pasRefined are majorly changed
The main repercussions are:
- 3 new authorities in the policy: Call, Reply, and DeleteDerived
- The cdt and the caps state are linked in pasRefined
- CDT parentship no longer implies control in certain cases (is_transferable)
- CDT parentship now implies DeleteDerived
- Introduction of cdt_change_allowed that specifies which slot your are
allowed to modify
- Integrity for CDT and CDT list use cdt_changes_allowed
- Integrity for objects in now expressed as a transitive closure of
atomic transition rules
Uses proof body terms to disambiguate the names encoutered in
dependency extraction, rather than using (for example)
Thm.full_prop_of.
The result is that this catches a few more missing dependencies,
enough to correctly identify unused lemmas large sessions
like CRefine.
Normal abbreviations are not contracted on pretty printing when defined
inside a locale. This commit provide the command locale_abbrev which does
contract on pretty print even when defined inside a locale. It cannot be
used with abbreviations that mention fixed locale variables (whereas the
standard abbreviations can).
Co-authored-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
- Previously printed `~` for negative numbers, which is invalid
JSON. Now prints `-`.
- Previously the outpout would unconditionally trim
'underscore-number' suffixes. Now uses theory context to determine
if it's likely to be an index into a theory list or an existing
fact name.
- Changed JSON structure to avoid using dynamic names for keys, i.e.
from this:
{
"my_theory_name": {...}
}
to this:
{
"theory": "my_theory_name",
"content": {...}
}
This should make processing the output slightly nicer by matching
what other tools expect.
- Changed JSON structure to consolidate dependencies. Lemmas are no
longer special-cased.
* Context :
We would like to prove that, for ARM_HYP architecture,
the current vcpu is always the vcpu associated to the current thread.
See issue https://jira.csiro.au/browse/VER-770
and PR 291 http://bitbucket.keg.ertos.in.nicta.com.au/projects/SEL4/repos/l4v/pull-requests/291
* Intermediate step : the vcpu of the idle thread is always None
In this commit we update the proofs of abstract invariants for
the arm_hyp architecture, so that the new version of `valid_idle`,
stating that the vcpu of the idle thread is always None, holds.
* Context :
We would like to prove that, for ARM_HYP architecture,
the current vcpu is always the vcpu associated to the current thread.
See issue https://jira.csiro.au/browse/VER-770
and PR 291 http://bitbucket.keg.ertos.in.nicta.com.au/projects/SEL4/repos/l4v/pull-requests/291
* Intermediate step : the vcpu of the idle thread is always none
In this commit, we modify the `valid_idle` invariant so that it includes
the fact that the vcpu of the idle thread is always None.
This is needed for PR291 (see Context above).
`valid_idle` beeing defined with `idle_tcb_at`,
we changed the definition of `idle_tcb_at`
so that it can convey information about the architecture.
And we defined `valid_arch_idle`
that states that the vcpu of an iarch_tcb is None.
* What changed :
Even if these changes are only interesting for the
abstract invariants for arm_hyp architecture
(that are being extended),
it implied changes to several generic and architecture-specific
files of the astract invariants (AInvs) sessions.
Co-authored-by : Corey Lewis <corey.lewis@data61.csiro.au>
Co-authored-by : Santiago Bautista <santiago.bautista@data61.csiro.au>