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.
Joel Beeren
Thomas Sewell
Matthew Brecknell
Daniel Matichuk
Alejandro Gomez-Londono
Sidney Amani
Gerwin Klein
Rafal Kolanski
Miki Tanaka