Adds the `supply_local_method` command and `local_method` methods,
which store and apply methods as a way to shorten repeated
references to large or complicated methods.
It looks like "interpretation" occasionally renames schematic variables.
Finding global facts up to pattern equivalence should give us the original
global version.
Session-qualified imports will be required for Isabelle2018 and help clarify
the structure of sessions in the build tree.
This commit mainly adds a new set of sessions for lib/, including a Lib
session that includes most theories in lib/ and a few separate sessions for
parts that have dependencies beyond CParser or are separate AFP sessions.
The group "lib" collects all lib/ sessions.
As a consequence, other theories should use lib/ theories by session name,
not by path, which in turns means spec and proof sessions should also refer
to each other by session name, not path, to avoid duplicate theory errors in
theory merges later.
Accept "[f x | x \leftarrow t]" in addition to "[f x . x \leftarrow t]",
because the former is what naturally comes out of the Haskell translator, and
the regexps that would be necessary in the Haskell translator for this are
distasteful.
JIRA-VER 927
Adds "non-conditional simplification" method simp_no_cond, and
various equivalents.
This is done by setting the simplifier depth limit to 0, which seems
to be a useful case. It prevents expensive conditional simplification
attempts but leaves the simplifier strategy otherwise unchanged.
This is easy to set up, and link to wpsimp.
Discard some magic that was done to instantiate an induction rule,
and instead use the existing Induct_Tacs package to apply induction
rules, which seems to be successful more often.
Adjusting the strengthen congruence rules for conjunction
and disjunction makes other conjuncts available as assumptions
in strengthening a conjunction. This may be useful occasionally.
To prove that retyping a TCB establishes the state relation for TCBs,
it is necessary to prove that the C FPU null state is always equal to
the Haskell FPU null state. This commit therefore includes some
machinery for maintaining the state relation for the FPU null state,
and repairs many proofs.
These theories supply the interference trace monad with a useful notion of
simulation/refinement, which could be used to prove functional correctness
(similar to corres) in the presence of concurrency.
Adds another style of monad to the existing ones in lib/Monad_WP.
The Interference Trace monad is an extension of the nondeterministic
state monad to record interactions between the task and its environment.
It supports a parallel composition operator.
The VCG for this monad includes the same Hoare triple style as for the
state monads, and also includes a rely-guarantee quintuple which can be
used to verify a parallel composition of programs.
By default, strings (and other lists) cannot be lexicographically
ordered because our theories pull in a conflicting instance of the
"order" class for lists. This theory adds a "lexord_list" wrapper type
that provides lexicographical order.
The subseq_abbreviation mechanism was a useful way of quoting some of a
definition or term, specialised to the case of left-associated sequences.
Lambda abstractions are now handled better.
The previous subseq mechanism required some generalisations. It is now replaced
by match_abbreviation, which is a more general approach.
The match mechanism picks a term, can select a matching subterm, and can
rewrite the selected term based on pattern matching also. The new mechanism
can cover all the cases of the previous one, as shown in examples.
In the cases where the sequence constructor is associative, it can
be handy to immediately save a 'reassociate' theorem, that can be used
to parenthesise out the abbreviated subsequence from any sequence it
appears in.
This can be done by supplying the association rule.
It's annoying that, given automatic definitions (such as we have
with the Haskell translator and C parser), there's no way to capture
a few lines of them.
This mechanism allows you to add an abbreviation for some subsequence of
elements, found somewhere in a theorem, where a sequence is defined by its
constructor and the start and end points are matched by pattern matching.
The main aim of this is for crunch to make consistent decisions about
whether to prove new rules. If any rules in the wp set can be used to
directly solve the goal crunch is working on, then crunch will just
use it.
Other changes include:
- crunch_ignore works properly inside locales again.
- if a rule already exists with the specific name crunch is going
to use, but that rule does not solve the goal crunch is working on
then crunch will now error.
- if crunch fails to prove a goal it will now output a warning if
adding crunch_simps or crunch_wps would allow it to make more
progess.
In particular, some intro! attributes for some wp rules are removed.
These previously caused auto/fastforce to play a really strange role
in some proofs.
The rules for these conditional monadic operators have been a bit
ad-hoc until now, with frequent headaches around the whenE/throwError
pattern.
Adding standard split rules ensures these operators are treated uniformly.
Add two new tactics/methods which can fix common painful problems with
schematic variables.
Method datatype_schem improves unification outcomes, by making judicious use of
selectors like fst/snd/the/hd to bring variables into scope, and also using a
wrapper to avoid singleton constants like True being captured needlessly by
unification.
Method wpfix uses strengthen machinery to instantiate rogue postcondition
schematics to True and to split precondition schematics that are shared across
different sites.
The previous wp_pre would apply a rule (from the named theorems wp_pre) unless
there was already a schematic in the goal. This is frequently prevented by an
irrelevant schematic.
This implementation applies a wp_pre rule unless one of the resulting goals
can be solved by "erule FalseE", that is, unless we would promote a schematic
into the assumption position (or, more rarely, there was already an assumption
schematic or False as an assumption).
These combinator rules do something like what wp_pre does now.
They were helpful in the ancient past, but now that wp_pre exists it is
much better to just use automation.
When given a theorem, find_names finds other names the theorem appears
under, via matching on the whole proposition. It will not identify
unnamed theorems.
It's just a parser tweak for crunch, and runs multiple crunch commands
with the same sections (wps, ignores, etc).
Also update the comments a little, and move them closer to the anchor of
command clicks (the @{command_keyword} antiquotation).
The strengthen implementation can now do a bit more.
The new method strengthen_asm also adjusts assumptions.
The new method strengthen_meth takes a method as a parameter,
e.g. apply (strengthen_meth \<open> rule order.trans \<close>)
does the same thing as apply (strengthen order.trans)
with scope for other exciting applications I haven't thought of.
Notably useful is hoare_vcg_lift_imp' which generates an implication
rather than a disjunction.
Monadic rewrite rules should be modified to preserve bound variable
names, as demonstrated by monadic_rewrite_symb_exec_l'_preserve_names.
Addressing this more comprehensively is left as a TODO item for the
future (see VER-554).
Elimination against the pattern "P v", where both "P" and "v" are free,
can loop, if the rule is marked as a safe elimination rule. In the rules
modified in this commit, variable "v" provides no real benefit, so we
replace the pattern with "P".
This commit adds a method `ac_init`, which converts a ccorres goal into
a corres goal. It also adds an attribute `ac`, which converts a ccorres
fact into a corres fact, in a form suitable for solving goals produced
by `ac_init`.
A number of proofs begin with word_eqI followed by some similar steps,
suggesting a 'word_eqI_solve' proof method, which is implemented here.
Many of these steps are standard, however a tricky part is that constants of
type 'nat' which encode a particular number of bits must often be unfolded.
This was done by expanding the eval_bool machinery to add eval_int_nat, which
tries to evaluate ints and nats.
Testing eval_int_nat revealed the need to improve the code generator setup
somewhat. The Arch locale contains many of the relevant constants, and they are
given global names via requalify_const, but the code generator doesn't know
about them. Some tweaks make them available. I *think* this is safe for
arch_split, as long as the proofs that derive from them are true in each
architecture.
This method/simproc uses the code generator setup to evaluate terms of boolean
type that can be reduced to True/False. Should avoid manual unfolding in
various places.
This computes a value (like the existing value keyword) and also saves
the result of that computation as an abbreviation.
This will be useful in CRefine etc to give names to magic numbers that
derive from configuration variables/constants.
Removes files that were duplicated in cspec/$L4V_ARCH directories to exist directly in
the cspec directory and contain $L4V_ARCH switches where needed. This allows for a single
Makefile for building the C kernel and the KernelInc_C theory, which is different between
architectures, to still exist per L4V_ARCH.
As the build location of the C kernel, and the resulting kernel_all.c_pp artifact, is
moved this change needs to be reflected in all the theory files that refer to it.
After discussion with others, it's clear this is not self-documenting.
A few comments might make it easier to understand what's going on.
Thanks to Matt Brecknell for the more explanatory example.
Introduces F_all2, which allows us to have
a proper stateless precondition in corres_mapM_list_all2
(has access to all introduced goal parameters).
With it is the implicit assumption that the generated
condition can be phrased as a per-element property (although
it may talk about the list as a whole).
* rules for when the state relation is Id.
* rules for modify
* trivial return relations over units (i.e. = or dc)
are now always weakened into a schematic
* corres_pre now performs more conservative weakening
if the goal is already a corresK goal. This prevents
introducing a verification condition in the middle
of a proof.
* corres_inst_eq avoids splitting if statements when
unfolding corres_protect.
* corres_rv correctly handles schematic atomic postconditions
(previously would loop, now instiates them to True)
* corressimp fails on schematic goals to avoid looping
corres method now fails outright if the subgoal
conclusion is schematic, otherwise it can loop.
Handle cases where corressimp
would leave preconditions uninstantiated if the
goal was solved by clarsimp.
This removes corres_choice in favour of making corres_rv smarter.
Now corres_rv can propagate a stateless condition, and the new
corres_rv method (called from corres) tries to push the generated
obligation into the appropriate place (stateless, left or right
precondition) based on which variables it discusses.
This avoids most cases where the corres_rv_wp_left/right or
corres_rv_defer rules needed to be specified manually.
The new "corres_choice_true" and "corres_choice_false" constants
represent a deferred choice for how to propagate a generated
stateless precondition. If possible, we would prefer to do so
via the outermost stateless precondition, since it has access
to all green variables. Importantly corres_rv_defer_left/right
are subsumed by the more general corres_rv_defer.
Also we introduce alternative wp_comb rules which introduce
a corres_inst_eq goal, rather than a raw meta-implication. This
is to avoid cases where the existing wp_comb methods would incorrectly
introduce schematic assumptions, resulting in unprovable goals. This
allows for more carefully controlling unification in cases where
the precondition of a hoare triple doesn't have access to all
necessary green variables.
Avoid introducing schematic assumption when corres preconditions
are concrete put stateless condition is schematic.
Avoid empty ruleset for corres_concrete_rER: causes corres to
loop unless it has at least one member.
Since corres_splits rules are applied conservatively, we
can safely put the straightforward "corresK_if" rule in it,
leaving the reverse rule for corres_search.
Also "when" and "liftM" rules should be corres_splits,
rather than corresK, to handle cases where we might have
some more specific rule about a particular scenario and don't
necessarily want to unwrap the function.
Correswp is wp but with more conservative treatment for
schematics. Rules in wp_comb that do precondition weakening
are avoided when the precondition is schematic, and there
is a final check which fails if any schematic preconditions
are found.
Realistically this should be the default behaviour for wp, but
that's a potentially bigger change.
Instead of doing rewriting corres should only rely on
rule application to ensure it only manipulates the
head function (and only if such manipulation causes
corres progress to be made).
Generated goal premises (i.e. from bind or if split rules)
should in most cases be redundant, as necessary conditions can
simply be propagated. By aggressively protecting them, we afford
ourselves greater control over how function bodies are rewritten.
Allow corressimp to use the return-value relation in its clarsimp step
if doing so allows it to solve the subgoal.
This addresses some occasions where wp generates in-place goals that can
be easily solved (rather than pushing them into preconditions).
Some schematic instantiations require knowledge from return-value
relations. The special const "corres_eq_inst" indicates to corres
that a schematic instantiation should be possible/obvious by
unfolding the protected assumptions and applying fastforce.
This commit fixes a typo in apply_trace which
prevented correct printing of the index of
the lemma used in a grouped lemma.
An example is given in Apply_Trace_Cmd.thy
When faced with a stateful IF conditional on the C side, when you know
exactly what that conditional is evaluating w.r.t. to Haskell side, you
can now say what it is and prove it in an eager manner, in a spirit
similar to ccorres_symb_exec_r_known_rv* lemmas.
Corres lemmas are proven. Remaining:
- A handfull of Hoare triples.
- The Haskell spec for invalidateASID needs to be updated
to close a small hole in each of unmap_pd_corres and
unmap_pdpt_corres.
This overrides the default proof state printing function to also
show any subgoals which have been hidden (protected).
This makes proof states shown during apply_debug more
comprehensible.
This adds new classes of corres rules which require different
goal parameters to be instantiated. corressimp avoids applying
wp or simp rules which would expose schematics.
Japheth Lim
Edward Pierzchalski
Callum Bannister
Ilya Yanok
Rafal Kolanski
Gerwin Klein
Corey Lewis
Thomas Sewell
Matthew Brecknell
Michael Sproul
Thibaut Perami
Joel Beeren
Alejandro Gomez-Londono
Pang Luo
Adrian Danis
Joel Beeren
Daniel Matichuk
Alejandro Gomez-Londono
Sidney Amani
Miki Tanaka