Theory Micro_Rust_Examples.Crush_Examples
theory Crush_Examples
imports Micro_Rust_Std_Lib.StdLib_All
begin
section‹▩‹crush› guide›
text‹This file is a brief guide to usage and configuration of the ▩‹crush› family of tactics.›
subsection‹Overview›
text‹▩‹crush› is a high-level tactic for dealing with goals in classical and
separation logic. ▩‹crush› is never trying to be 'clever'. Its goal, instead,
is to do the (seemingly) obvious thing reliably, and to discharge hundreds or thousands
of elementary reasoning steps without human intervention. The proof author is then left with
the tasks of calling ▩‹crush› suitably -- which is what the bulk of this guide is about -- and
filling in the steps that ▩‹crush› cannot solve (such as providing loop invariants, for example).
The birds'-eye view of ▩‹crush› is that of a long disjunction of different branches.
That is, try branch A; if it fails, try branch B; if it fails, try branch C, and so on.
Care has to be taken in choosing the order of branches correctly, both for correctness and
for performance: Regarding correctness, for example, introducing schematic variables must
be handled with a lower priority than operations introducing free variables -- otherwise, the
schematic variables may not instantiate correctly. Regarding performance, powerful tactics
such as a plain ▩‹simp› or ▩‹clarsimp› have to be called with low priority, or otherwise ▩‹crush›
will be too slow for the highly complex goals that we use it for. Even more powerful tactics
such as ▩‹force›, ▩‹blast› or ▩‹auto› are not considered at all. Instead, branches aim to implement
their solution strategy through a mixture of standard tactics ▩‹simp only›, ▩‹elim›, and ▩‹intro›,
or custom ML.
▩‹crush› is highly configurable and shares part of its configuration mechanism with the classical
reasonders such as ▩‹clarsimp›, ▩‹force› or ▩‹auto›: That is, simplification rules can be added/removed
via ▩‹simp add/del: ...›, introduction, split and elimination rules can be added via ▩‹intro: ...›,
▩‹elim: ...› or ▩‹split: ...›. However, there are various other configuration options that the user
needs to be aware of, some specific to separation logic, some refining the classical reasoning.
Those configuration options will be described and exemplified below. It is essential that the users
familiarizes themselves with the configurations, as a bare ▩‹apply crush› is rarely getting far.
▩‹crush› comes in three variants:
- ▩‹crush_base_step›: A single iteration of the ▩‹crush› loop
- ▩‹fastcrush_base›: Run the `crush` loop on the current goal and all emerging goals, until no
progress can be made anymore.
- ▩‹crush_base›: Run the ▩‹crush› loop on all goals and all emerging goals, until no progress
can be made anymore.
Since, like ▩‹auto› for example, ▩‹crush_base› can affect the entire goal set, using it in the middle
of proofs can make them harder to maintain. Relying on ▩‹fastcrush_base› usually leads to more robust
proofs. Finally, ▩‹crush_base_step› is mostly useful for debugging purposes; complex proofs require
hundreds of iterations of the ▩‹crush› loop, so manual invocation of ▩‹crush_base_step› is typically
not useful.
›
subsection‹▩‹crush› arguments and configurations›
text‹In this section, we go through various arguments and configuration options of ▩‹crush›
and explain and exemplify their use.
All options apply to all of ▩‹crush›, ▩‹fastcrush› and ▩‹crush_step›, but we illustrate them for
▩‹crush› only.›
subsubsection‹Classical reasoning options›
text‹▩‹crush› supports all arguments that classical reasoning tactics like ▩‹clarsimp›,
▩‹auto›, ▩‹fastforce› or ▩‹force› do. Some examples:›
paragraph‹Simplification rules›
notepad
begin
fix a b :: bool
assume h: ‹a ≡ b›
and b: ‹b›
have ‹a›
apply (clarsimp simp add: h)
apply (rule b)
done
next
fix a b :: bool
assume h: ‹a ≡ b›
and b: ‹b›
have ‹a›
apply (crush_base simp add: h)
apply (rule b)
done
end
paragraph‹Elimination rules›
notepad
begin
fix a b c :: bool
assume h: ‹⋀R. a ⟹ (b ⟹ R) ⟹ R›
and j: ‹b ⟹ c›
have ‹a ⟹ c›
apply (clarsimp elim!: h)
apply (rule j, force)
done
next
fix a b c :: bool
assume h: ‹⋀R. a ⟹ (b ⟹ R) ⟹ R›
and j: ‹b ⟹ c›
have ‹a ⟹ c›
apply (crush_base elim!: h)
apply (rule j, force)
done
end
paragraph‹Split rules›
notepad
begin
fix a b c :: bool
assume 1: ‹a ⟹ b›
and 2: ‹¬ a ⟹ c›
have ‹if a then b else c›
apply (clarsimp split!: if_splits)
using 1 2 apply auto
done
next
fix a b c :: bool
assume 1: ‹a ⟹ b›
and 2: ‹¬ a ⟹ c›
have ‹if a then b else c›
apply (crush_base split!: if_splits)
using 1 2 apply auto
done
end
text‹Note, however, that ▩‹clarsimp› is attempted by ▩‹crush› with very low priority. This can not
only be an issue for performance, but also for correctness, as the following example shows. It is
a bit artifical, but instances of this pattern do emerge in practice:›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
assumes PQ: ‹⋀x. P x ⤏ Q x›
begin
definition ‹Some_Ex ≡ ⨆x. P x›
lemma ‹Some_Ex ⤏ (⨆x. Q x)›
apply (crush_base simp add: Some_Ex_def)
oops
text‹We can confirm that the simplification happened too late by single-stepping through the proof:›
lemma ‹Some_Ex ⤏ (⨆x. Q x)›
apply (crush_base_step simp add: Some_Ex_def)
apply (crush_base_step simp add: Some_Ex_def)
apply (crush_base_step simp add: Some_Ex_def)
oops
end
text‹The next section shows how to fix the situation through 'eager' simplification.›
subsubsection‹Premise/Conclusion simplifications›
text‹The previous section explained that simplifications registered via ▩‹... simp add: ...›
are unfolded with very low priority, which can lead to ▩‹crush› introducing unsolvable schematics
too early. To remedy, ∗‹premises› can be unfolded with higher priority by using the
▩‹simp prems add: ...› parameter. It appplies to both pure and spatial premises.›
text‹Let's see how the previous example can be fixed using ▩‹simp prems add: ...›:›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
assumes PQ: ‹⋀x. P x ⤏ Q x›
begin
definition ‹Some_Ex ≡ ⨆x. P x›
lemma ‹Some_Ex ⤏ (⨆x. Q x)›
apply (crush_base simp prems add: Some_Ex_def)
apply (rule PQ)
done
text‹We can confirm that the simplification happened earlier than in the previous example
by single-stepping through the proof:›
lemma ‹Some_Ex ⤏ (⨆x. Q x)›
apply (crush_base_step simp prems add: Some_Ex_def)
apply (crush_base_step simp prems add: Some_Ex_def)
apply (crush_base_step simp prems add: Some_Ex_def)
apply (rule PQ)
done
text‹▩‹simp prems/concls› should automatically eta expand definitions:›
definition not_eta_expanded where ‹not_eta_expanded ≡ λx f. f x›
lemma ‹⋀foo. not_eta_expanded f t ⤏ foo›
apply (crush_base simp prems add: not_eta_expanded_def)
oops
end
text‹There is also ▩‹simp concls add: ...› for unfolding pure or spatial ∗‹conclusions›. In contrast
to ▩‹simp prems add: ...›, this is less about correctness than about performance: Unfolding conclusions
late should not lead to bad schematics, but it can lead to performance issues because ▩‹simp add: ...›
is costly and (therefore) only attempted late withihn ▩‹crush›.›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
assumes PQ: ‹⋀x. P x ⤏ Q x›
begin
definition ‹Some_Ex T ≡ ⨆x. T x›
lemma ‹Some_Ex P ⤏ Some_Ex Q›
apply (crush_base simp prems add: Some_Ex_def simp concls add: Some_Ex_def)
apply (rule PQ)
done
text‹We can confirm that ▩‹simp prems add: ...› takes precedence over ▩‹simp concls add: ...›,
that is, premises are unfolded with higher priority than conclusions:›
lemma ‹Some_Ex P ⤏ Some_Ex Q›
apply (crush_base_step simp prems add: Some_Ex_def simp concls add: Some_Ex_def)
apply (crush_base_step simp prems add: Some_Ex_def simp concls add: Some_Ex_def)
apply (crush_base_step simp prems add: Some_Ex_def simp concls add: Some_Ex_def)
apply (crush_base_step simp prems add: Some_Ex_def simp concls add: Some_Ex_def)
apply (rule PQ)
done
end
text‹You can also combine ▩‹simp prems› and ▩‹simp concls› by providing a list of
simpsets which should be modified. The 'normal' simpset used for the ▩‹[clar]simp›
branch in ▩‹crush› is identified by ▩‹generic›:›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
assumes PQ: ‹⋀x. P x ⤏ Q x›
begin
definition ‹Some_Ex ≡ ⨆x. P x›
lemma ‹Some_Ex ⤏ (⨆x. Q x)›
apply (crush_base simp [prems, concls, generic] add: Some_Ex_def)
apply (rule PQ)
done
end
text‹If you write ▩‹simp add: ...›, the default set of simpsets is determined by the
configuration of ▩‹Crush_Config.crush_simp_general_implies_prems› and
▩‹Crush_Config.crush_simp_general_implies_concls›. Depending on whether they are set/unset,
▩‹simp add: ...› will by default include ▩‹prems/concls›; it will always include ▩‹generic›.
Currently, ▩‹Crush_Config.crush_simp_general_implies_prems› and
▩‹Crush_Config.crush_simp_general_implies_concls› are both globally ▩‹false› by default.›
text‹Finally, there is also ▩‹simp early add/del: ...› which are simplifications which are attempted
at highest priority in the first branch of ▩‹crush›. The underlying named theorem list is ▩‹crush_early_simps›.
WARNING: Be careful with adding to ▩‹crush_early_simps› globally -- it may not only break existing proofs
but also cause a significant slowdown since early simplification is attempted at high priority.›
subsubsection‹High-priority introduction rules›
text‹In the previous sections, we discussed how ▩‹crush› includes a low priority branch for ▩‹clarsimp›
and its configuration via ▩‹simp add/del: ...›, but that for performance and correctness dedicated
parameters ▩‹simp prems/concls/early add/del: ...› should be used.
The situation for introduction rules is similar: They can be registered via ▩‹intro[!]: ...›, in which
case they will be attempted as part of ▩‹clarsimp›, but only with very low priority.
To apply safe introduction rules at high priority, you can instead use ▩‹intro add: ...›, which will
make ▩‹crush› attempt the respective rules in a high priority branch. The underlying named theorem list
is ▩‹crush_intros›, which can also be populated locally/globally via ▩‹declare/notes› as usual.
Beware of the minor syntactic difference between ▩‹crush intro: foo›, which affects only the low-priority
▩‹clarsimp› branch, and ▩‹crush intro add: foo›, which adds to high-priority introduction rules.
Note that ▩‹intro add: ...› registers classical introduction rules. Introduction rules for
separation logic are discussed next.›
subsubsection‹Separation logic introduction and destruction rules›
text‹Separation logic introduction rules can be registered with ▩‹seplog rule add: ...›. Under the
hood, this applies the ▩‹aentails_rule› tactic that we already discussed in 🗏‹../Crush/Examples.thy›.›
text‹Using ▩‹seplog drule add: ...›, the previous example can be subsumed into a single ▩‹crush›
call.›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
assumes PQ: ‹⋀x. P x ⤏ Q x›
begin
definition ‹Some_Ex ≡ ⨆x. P x›
lemma ‹Some_Ex ⤏ (⨆x. Q x)›
by (crush_base simp prems add: Some_Ex_def seplog rule add: PQ)
text‹Similarly, spatial assertions can be destructed using ▩‹seplog drule add: ...›, which wraps
▩‹aentails_drule›.›
lemma ‹Some_Ex ⤏ (⨆x. Q x)›
by (crush_base simp prems add: Some_Ex_def seplog drule add: PQ)
end
text‹Separation logic introduction and destruction rules can have pure premises as well, in which
case those premises will be introduced as new subgoals:›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
and R :: bool
assumes PQ: ‹⋀x. R ⟹ P x ⤏ Q x›
begin
definition ‹Some_Ex ≡ ⨆x. P x›
lemma ‹R ⟹ Some_Ex ⤏ (⨆x. Q x)›
by (crush_base simp prems add: Some_Ex_def seplog rule add: PQ)
lemma ‹R ⟹ Some_Ex ⤏ (⨆x. Q x)›
by (crush_base simp prems add: Some_Ex_def seplog drule add: PQ)
end
subsubsection‹Generic simplifications›
text‹We have already seen that ▩‹crush› applies simplification rules for separation logic
automatically. For example, the previous example requires ▩‹crush› to use
▩‹
lemma aexists_entailsL':
assumes ‹⋀x. x ∈ S ⟹ φ x ⤏ ψ›
shows ‹(⨆x ∈ S. φ x) ⤏ ψ›
lemma aexists_entailsR:
assumes ‹φ ⤏ ψ x›
shows ‹φ ⤏ (⨆x. ψ x)›
›
from 🗏‹../Shallow_Separation_Logic/Assertion_Language.thy›, to destruct the existential premise
and to introduce a schematic for the existentially quantified variable in the goal.›
text‹There are many more separation logic simplification and introduction steps that are routinely
applied by ▩‹crush›, such as associativity normalization for ▩‹⋆›, distributivity of ▩‹⋆› and ▩‹⨆›,
cancellation, or hoisting out of pure premises. Here is another example:›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
and α β γ δ :: ‹'s assert›
and R :: bool
assumes PQ: ‹⋀x. R ⟹ P x ⋆ β ⤏ Q x ⋆ γ›
and P_ucincl[ucincl_intros]: ‹⋀x. ucincl (P x)›
begin
definition ‹Some_Ex ≡ ⨆x. P x›
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
by (crush_base simp prems add: Some_Ex_def seplog rule add: PQ)
text‹This example would already be rather tedious to prove by hand. Indeed, already the number of
▩‹crush› steps has increased notably:›
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
apply (crush_base_step simp prems add: Some_Ex_def seplog rule add: PQ)
apply (crush_base_step simp prems add: Some_Ex_def seplog rule add: PQ)
apply (crush_base_step simp prems add: Some_Ex_def seplog rule add: PQ)
apply (crush_base_step simp prems add: Some_Ex_def seplog rule add: PQ)
apply (crush_base_step simp prems add: Some_Ex_def seplog rule add: PQ)
apply (crush_base_step simp prems add: Some_Ex_def seplog rule add: PQ)
apply (crush_base_step simp prems add: Some_Ex_def seplog rule add: PQ)
apply (crush_base_step simp prems add: Some_Ex_def seplog rule add: PQ)
done
end
text‹Usually, ▩‹crush›'s simplifications are robust and do not need tweaking, and in the rare case
where simplifications need to be watched closely, one can either call individual ▩‹crush› steps
or fall back to lower level tactics and rules.
One notable exception is the omission of rules introducting schematics, which may sometimes need to
be withheld to avoid unsolvable schematics (even though ▩‹simp prems add: ...› and guards -- described below --
already help to avoid those situations).
If you want to prevent ▩‹crush› from introducing schematics for existentially quantified goals,
use ▩‹no_schematics›.›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
and α β γ :: ‹'s assert›
and R :: bool
assumes PQ: ‹⋀x. R ⟹ P x ⋆ β ⤏ Q x ⋆ γ›
and P_ucincl[ucincl_intros]: ‹⋀x. ucincl (P x)›
begin
definition ‹Some_Ex ≡ ⨆x. P x›
ucincl_auto Some_Ex
lemma ‹Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ γ›
apply (crush_base simp add: Some_Ex_def no_schematics)
apply (crush_base seplog rule add: PQ)
done
end
subsection‹Disabling case splits›
text‹By default ▩‹crush› uses ▩‹safe› to split disjunctive premises, and to split conjunctive
subgoals. While safe, this can sometimes lead to an explosion in the number of subgoals, which
is problematic from a performance perspective, esp. if the various cases still have reasoning in
common. ▩‹crush› itself applies ▩‹safe› with a low priority to do as much common reasoning on the
cases as possible, but if such common reasoning happens outside of ▩‹crush›, ▩‹crush› must be forced
not to use ▩‹safe› at all. This is done by passing the ▩‹no_safe› argument.›
experiment
fixes A B C D :: bool
begin
lemma ‹A ∨ B ⟹ C ∧ D›
apply crush_base
oops
text‹Trying again without ▩‹safe›:›
lemma ‹A ∨ B ⟹ C ∧ D›
apply ((crush_base no_safe)?)
oops
end
text‹WARNING: As it stands, ▩‹crush› will unconditionally split ▩‹spatial› goals, and ∗‹never›
split spatial disjunctions:›
experiment
fixes P Q R S :: ‹'s::sepalg assert›
and A B C D :: bool
begin
lemma ‹A ∨ B ⟹ (P ⊔ Q ⤏ R ⊓ S)›
apply crush_base
oops
text‹Trying again without ▩‹safe›:›
lemma ‹A ∨ B ⟹ (P ⊔ Q ⤏ R ⊓ S)›
apply (crush_base no_safe)
oops
end
subsubsection‹Adding branches›
text‹As mentioned, ▩‹crush› never tries to be 'clever' and deliberately relies on foundational tactics
only. If you find that within the realm of some proof(s) you repeatedly need to switch between ▩‹crush›
and another context-specific proof step, you can locally register this step as another branch of ▩‹crush›
using ▩‹branch add: ...›, which takes a ∗‹method› as an argument.›
experiment
fixes A B C D :: bool
assumes AB_CD: ‹A ⟹ C› ‹A ⟹ D› ‹B ⟹ C› ‹B ⟹ D›
begin
lemma ‹A ∨ B ⟹ C ∧ D›
by (crush_base branch add: ‹intro AB_CD; assumption›)
end
subsubsection‹Debugging ▩‹crush››
text‹If ▩‹crush› behaves surprisingly and you find yourself in need of inspecting what is happening,
there are multiple options.
A useful first step is typically to reproduce the issue with ▩‹fastcrush› rather than ▩‹crush›.
The former should be easier to debug since it applies only to the current goal, while ▩‹crush› applies
to ∗‹all› goals. Also, you should try to minimize the number of arguments passed to ▩‹crush›:
Can you ascribe the unexpected behavior to the addition/deletion of a certain argument?
When that's done, consider one of the following steps:›
paragraph‹Single-stepping›
text‹You can replace ▩‹crush/fastcrush› by ▩‹crush_[base_]step› to trace what ▩‹crush› is doing.
Note, however, that for complex ▩‹crush› calls this may require you to copy-paste the respective
▩‹crush› call dozens or hundreds of times, which is not terribly user friendly.›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
and α β γ δ :: ‹'s assert›
and R :: bool
assumes PQ: ‹⋀x. R ⟹ P x ⋆ β ⤏ Q x ⋆ γ›
and P_ucincl[ucincl_intros]: ‹⋀x. ucincl (P x)›
begin
definition ‹Some_Ex ≡ ⨆x. P x›
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
by (crush_base simp prems add: Some_Ex_def seplog rule add: PQ)
text‹This example would already be rather tedious to prove by hand. Indeed, already the number of
▩‹crush› steps has increased notably:›
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
apply (crush_base_step simp prems add: Some_Ex_def seplog rule add: PQ)
apply (crush_base_step simp prems add: Some_Ex_def seplog rule add: PQ)
apply (crush_base_step simp prems add: Some_Ex_def seplog rule add: PQ)
apply (crush_base_step simp prems add: Some_Ex_def seplog rule add: PQ)
apply (crush_base_step simp prems add: Some_Ex_def seplog rule add: PQ)
apply (crush_base_step simp prems add: Some_Ex_def seplog rule add: PQ)
apply (crush_base_step simp prems add: Some_Ex_def seplog rule add: PQ)
apply (crush_base_step simp prems add: Some_Ex_def seplog rule add: PQ)
done
end
paragraph‹Use gas›
text‹You can limit the maximum number of ▩‹crush› iterations by providing the numeric ▩‹gas› argument
in conjunction with ▩‹bigstep: false›. This allows you to conduct a binary search to look out for
where ▩‹crush›'s behavior starts to diverge from your expectation.›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
and α β γ δ :: ‹'s assert›
and R :: bool
assumes PQ: ‹⋀x. R ⟹ P x ⋆ β ⤏ Q x ⋆ γ›
and P_ucincl[ucincl_intros]: ‹⋀x. ucincl (P x)›
begin
definition ‹Some_Ex ≡ ⨆x. P x›
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
by (crush_base simp prems add: Some_Ex_def seplog rule add: PQ)
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
apply (crush_base simp prems add: Some_Ex_def seplog rule add: PQ bigstep: false gas: 10)
done
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
apply (crush_base simp prems add: Some_Ex_def seplog rule add: PQ bigstep: false gas: 5)
oops
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
apply (crush_base simp prems add: Some_Ex_def seplog rule add: PQ bigstep: false gas: 8)
done
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
apply (crush_base simp prems add: Some_Ex_def seplog rule add: PQ bigstep: false gas: 7)
oops
end
paragraph‹Use single-stepping›
text‹You can also run ▩‹crush› in single-stepping mode by passing ▩‹stepwise›.
Then, the ▩‹step› command can be used to run the ▩‹crush› once a time. Multiple steps can be taken
using ▩‹step n›, and the entire tactic can be run via ▩‹step *›. You can also run until one of the
goals matches a certain pattern using ▩‹step to goal pattern "PATTERN"›, or until one of the premises
of one of the goals satisfies a certain pattern, using ▩‹step to premise pattern "PATTERN"›. In both
cases, the pattern is expected to be of type ▩‹bool› (not ▩‹prop›). To stop at the occurrence of a
specific schematic, use ▩‹step to schematic "name" index›, where ▩‹?name'idx› is the target schematic.›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
and α β γ δ :: ‹'s assert›
and R :: bool
assumes PQ: ‹⋀x. R ⟹ P x ⋆ β ⤏ Q x ⋆ γ›
and P_ucincl[ucincl_intros]: ‹⋀x. ucincl (P x)›
begin
definition ‹Some_Ex ≡ ⨆x. P x›
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
using [[crush_log_toplevel]]
apply (crush_base simp prems add: Some_Ex_def seplog rule add: PQ stepwise)
step to goal pattern "_ ⤏ (⨆_. _)"
step
step 2
step *
done
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
using [[crush_log_toplevel]]
apply (crush_base simp prems add: Some_Ex_def seplog rule add: PQ stepwise)
step to premise pattern "R"
step *
done
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
using [[crush_log_toplevel]]
apply (crush_base simp prems add: Some_Ex_def seplog rule add: PQ stepwise)
step to schematic "x" 7
step *
done
end
paragraph‹Use backtracking›
text‹You can also use backtracking to retroactively inspect the path ▩‹crush› has taken. For this,
you set the ▩‹history› argument and use Isabelle's normal backtracking command
▩‹back› after the tactic invocation.›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
and α β γ δ :: ‹'s assert›
and R :: bool
assumes PQ: ‹⋀x. R ⟹ P x ⋆ β ⤏ Q x ⋆ γ›
and P_ucincl[ucincl_intros]: ‹⋀x. ucincl (P x)›
begin
definition ‹Some_Ex ≡ ⨆x. P x›
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
apply (crush_base simp prems add: Some_Ex_def seplog rule add: PQ history)
back back back back
back back back
oops
end
text‹Using backtracking is often more effective than ▩‹gas› as one can easily paste a very large
number of ▩‹back back back ...› blocks and do a binary search by moving the cursor through them,
which will show the intermediate states of ▩‹crush› in the output panel.›
text‹WARNING: You should ∗‹not› use backtracking to manually revert ▩‹crush› to the last good intermediate
goal and continue manually from there: Instead, it should only be used temporarily to identify what
went wrong where, and fix the proof. Manual backtracking would lead to proofs that are very hard to
maintain in the face of changes to ▩‹crush›. For the same reason, ▩‹gas› should only be used as a
debugging mechanism, not as a way to control ▩‹crush›.›
paragraph‹Aborting ▩‹crush››
text‹Another mechanism by which ▩‹crush› can be debugged is by stopping it once the goal matches
a given criterion. The motivation, here, is to facilitate identifying the ▩‹crush› step at which
a certain goal has emerged.
There are two variants: First, you can specify a pattern against which the meta-conclusion of the
intermediate goals should be matched, stopping ▩‹crush› if so. More generally, via ▩‹abort at filter: ...›
you can specify an arbitrary abort filter of type ▩‹Proof.context -> term -> bool› which goal
meta-conclusions will be fed through.›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
and α β γ δ :: ‹'s assert›
and R :: bool
assumes PQ: ‹⋀x. R ⟹ P x ⋆ β ⤏ Q x ⋆ γ›
and P_ucincl[ucincl_intros]: ‹⋀x. ucincl (P x)›
begin
definition ‹Some_Ex ≡ ⨆x. P x›
ucincl_auto Some_Ex
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
apply (crush_base bigstep:false abort at pattern: "_ ⤏ (⨆_. _)")
oops
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
apply (crush_base bigstep:false simp prems add: Some_Ex_def seplog rule add: PQ abort at filter: ‹
fn (ctxt : Proof.context) => fn (goal : term) =>
let val _ = Pretty.block [Pretty.str "Current goal: ",
goal |> Syntax.pretty_term ctxt] |> Pretty.writeln
in not (Separation_Logic_Tactics.is_entailment goal) end›)
oops
end
paragraph‹Case splitting›
experiment
begin
lemma ‹(case y of Some t ⇒ True | None ⇒ True) ⟹ α ⤏ 𝒲𝒫 Γ ⟦ match x { Some(y) ⇒ f(), None ⇒ g() } ⟧ β γ δ›
apply (crush_base split!: option.splits)
oops
lemma ‹(case y of Some t ⇒ True | None ⇒ True) ⟹ α ⤏ 𝒲𝒫 Γ ⟦ match x { None ⇒ f(), Some(y) ⇒ g() } ⟧ β γ δ›
apply (crush_base wp split: option.splits)
oops
end
paragraph‹Logging ▩‹crush››
text‹You can get a trace of the steps that ▩‹crush› has run by adding ▩‹crush_log_toplevel›.
If you want to see all intermediate goals, add ▩‹crush_log_goal›:›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
and α β γ δ :: ‹'s assert›
and R :: bool
assumes PQ: ‹⋀x. R ⟹ P x ⋆ β ⤏ Q x ⋆ γ›
and P_ucincl[ucincl_intros]: ‹⋀x. ucincl (P x)›
begin
definition ‹Some_Ex ≡ ⨆x. P x›
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
using [[crush_log_toplevel]]
by (crush_base simp prems add: Some_Ex_def seplog rule add: PQ)
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
using [[crush_log_toplevel, crush_log_goal]]
by (crush_base simp prems add: Some_Ex_def seplog rule add: PQ)
end
text‹There are various other logging options which can be used to trace individual branches.
See 🗏‹../Crush/config.ML› for a complete list.›
paragraph‹Comparing two ▩‹crush› calls›
text‹It sometimes happens that one notices one ▩‹crush› call succeeding and another failing, but it
not being clear where the divergence is emerging. In this case, you can use the ▩‹divergence›
tactical, which takes two methods as arguments and repeats them in lock-step to find the point
of divergence. It then stops and uses backtracking to allow the user to inspect the diverging states.
Note that the tactics passed to ▩‹divergence› have to be repeatable, to for use with ▩‹crush›
one needs to pass ▩‹crush_base_step›.
Here is a simple example demonstrating the higher priority of ▩‹simp prems ...› vs. ▩‹simp›:›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
assumes PQ: ‹⋀x. P x ⤏ Q x›
begin
definition ‹Some_Ex ≡ ⨆x. P x›
lemma ‹Some_Ex ⤏ (⨆x. Q x)›
apply (divergence
‹crush_base_step simp prems add: Some_Ex_def›
‹crush_base_step simp add: Some_Ex_def›
)
back
back
oops
end
subsubsection‹Profiling ▩‹crush››
text‹Despite all efforts to keep ▩‹crush› fast, some ▩‹crush› invocations can take a long time.
In this case, the general profiling variant ▩‹applyτ› can be used in conjunction with some or all
of the configuration options ▩‹crush_time_...› to get a timing profile for ▩‹crush›.
NB: Unfortunately, timing profiles are proof local, so you cannot currently aggregate performance
statistics along multiple proofs.›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
and α β γ δ :: ‹'s assert›
and R :: bool
assumes PQ: ‹⋀x. R ⟹ P x ⋆ β ⤏ Q x ⋆ γ›
and P_ucincl[ucincl_intros]: ‹⋀x. ucincl (P x)›
begin
definition ‹Some_Ex ≡ ⨆x. P x›
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
using [[crush_time_toplevel, crush_timing_threshold=5]]
applyτ (crush_base simp prems add: Some_Ex_def seplog rule add: PQ)
show_timelogs
done
end
text‹If you suspect that poor performance of ▩‹crush› is due to a particular branch running slowly,
you can instruct ▩‹crush› to stop when the duration of single step surpasses a configurable threshold.
For example, ▩‹[clar]simp› invocations on highly complex goals can sometimes take seconds, and in this
case the abort mechanism is a good way to identify and debug them.›
experiment
fixes P Q :: ‹'a ⇒ 's::sepalg assert›
and α β γ δ :: ‹'s assert›
and R :: bool
assumes PQ: ‹⋀x. R ⟹ P x ⋆ β ⤏ Q x ⋆ γ›
and P_ucincl[ucincl_intros]: ‹⋀x. ucincl (P x)›
begin
definition ‹Some_Ex ≡ ⨆x. P x›
lemma ‹δ ⋆ Some_Ex ⋆ (α ⋆ β) ⋆ ⟨R⟩ ⤏ α ⋆ (⨆x. Q x) ⋆ (γ ⋆ δ)›
using [[crush_time_steps, crush_time_step_bound_ms=1000]]
apply (crush_base simp prems add: Some_Ex_def bigstep: false branch add: ‹sleep 2›)
oops
end
subsubsection‹Reasoning in the weakest precondition calculus›
text‹In addition to classical and generic separation logic reasoning, ▩‹crush› supports reasoning
in the weakest precondition (WP) calculus for μRust. ▩‹crush› is aware of WP-rules for various μRust
program constructs and discharges them automatically, thereby effectively stepping through programs.›
text‹We consider a simple example of a μRust expression swapping the values of two references:›
context reference
begin
adhoc_overloading store_update_const ⇌
update_fun
definition swap_ref :: ‹('a, 'b, 'v) ref ⇒ ('a, 'b, 'v) ref ⇒ ('s, unit, unit, 'abort, 'i prompt, 'o prompt_output) expression› where
‹swap_ref rA rB ≡ ⟦
let oldA = *rA;
let oldB = *rB;
rA = oldB;
rB = oldA;
⟧›
text‹Let's prove that this indeed swaps the contents of the references ▩‹rA› and ▩‹rB›:›
lemma swap_ref_correct:
fixes Γ :: ‹('s, 'abort, 'i, 'o) striple_context›
and gA gB :: 'b
and vA vB :: 'v
and rA rB :: ‹('a, 'b, 'v) ref›
shows ‹Γ ;
rA ↦ ⟨⊤⟩ gA↓vA ⋆ rB ↦⟨⊤⟩ gB↓vB
⊢ swap_ref rA rB
⊣ (λ_. (⨆gA' gB'. rA ↦ ⟨⊤⟩ gA'↓vB ⋆ rB ↦⟨⊤⟩ gB'↓vA))
⨝ ⊥ ⨝ ⊥
›
apply (simp add: wp_sstriple_iff)
using [[crush_log_toplevel]]
apply (crush_base simp add: swap_ref_def)
done
text‹NB: It is instructive to see how many low-level proof steps are already necessary for code
as simple as this:›
lemma
fixes Γ :: ‹('s, 'abort, 'i, 'o) striple_context›
and gA gB :: 'b
and vA vB :: 'v
and rA rB :: ‹('a, 'b, 'v) ref›
shows ‹Γ ;
rA ↦ ⟨⊤⟩ gA↓vA ⋆ rB ↦⟨⊤⟩ gB↓vB
⊢ swap_ref rA rB
⊣ (λ_. (⨆gA' gB'. rA ↦ ⟨⊤⟩ gA'↓vB ⋆ rB ↦⟨⊤⟩ gB'↓vA))
⨝ ⊥ ⨝ ⊥
›
apply (simp add: wp_sstriple_iff)
using [[crush_log_toplevel]]
apply (crush_base simp add: swap_ref_def stepwise)
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
step
done
subsubsection‹Function contracts and specifications›
text‹Normally, we would not reason about individual μRust expressions, but functions, and use
specifications and contracts to do so. We illustrate this in the example of the above
reference-swapping code wrapped into a function:›
definition swap_ref_fun :: ‹('a, 'b, 'v) ref ⇒ ('a, 'b, 'v) ref ⇒ ('s, unit, 'abort, 'i prompt, 'o prompt_output) function_body› where
‹swap_ref_fun rA rB ≡ FunctionBody ⟦
let oldA = *rA;
let oldB = *rB;
rA = oldB;
rB = oldA;
⟧›
text‹The contract for a uRust function is usually captured in a separate definition of type
▩‹function_contract›. In this case:›
definition swap_ref_fun_contract ::
‹('a, 'b, 'v) ref ⇒ ('a, 'b, 'v) ref ⇒ 'b ⇒ 'v ⇒ 'b ⇒ 'v ⇒ ('s, unit, 'abort) function_contract›
where ‹swap_ref_fun_contract rA rB gA vA gB vB ≡
let pre = rA ↦ ⟨⊤⟩ gA↓vA ⋆ rB ↦⟨⊤⟩ gB↓vB in
let post = λ_. (⨆gA' gB'. rA ↦ ⟨⊤⟩ gA'↓vB ⋆ rB ↦⟨⊤⟩ gB'↓vA) in
make_function_contract pre post›
text‹Note how we are force to make all contextual parameters of the function specification arguments
to the function contract definition.›
text‹As with all assertions, we need to prove that pre and post conditions are upwards closed.
Luckily, there is custom automation to do this:›
ucincl_auto swap_ref_fun_contract
text‹If the proof isn't trivial, you can use ▩‹ucincl_proof› instead to open up a proof context
for the required ▩‹ucincl› assertions.›
text‹Next, we state and prove the function specification:›
lemma swap_ref_fun_spec:
shows ‹Γ; swap_ref_fun rA rB ⊨⇩F swap_ref_fun_contract rA rB gA vA gB vB›
apply (crush_boot f: swap_ref_fun_def contract: swap_ref_fun_contract_def)
apply crush_base
done
text‹Next, imagine we write a higher-level function which relies on ▩‹swap_ref_fun›.›
definition rotate_ref3 :: ‹('a, 'b, 'v) ref ⇒ ('a, 'b, 'v) ref ⇒ ('a, 'b, 'v) ref ⇒ ('s, unit, 'abort, 'i prompt, 'o prompt_output) function_body› where
‹rotate_ref3 rA rB rC ≡ FunctionBody ⟦
swap_ref_fun (rA, rB);
swap_ref_fun (rB, rC);
⟧›
text‹Next, we write the contract for ▩‹rotate_ref3›:›
definition rotate_ref3_contract ::
‹('a, 'b, 'v) ref ⇒ ('a, 'b, 'v) ref ⇒ ('a, 'b, 'v) ref ⇒ 'b ⇒ 'v ⇒ 'b ⇒ 'v ⇒ 'b ⇒ 'v ⇒ ('s, unit, 'abort) function_contract›
where ‹rotate_ref3_contract rA rB rC gA vA gB vB gC vC ≡
let pre = rA ↦ ⟨⊤⟩ gA↓vA ⋆ rB ↦⟨⊤⟩ gB↓vB ⋆ rC ↦⟨⊤⟩ gC↓vC in
let post = λ_. (⨆gA' gB' gC'. rA ↦ ⟨⊤⟩ gA'↓vB ⋆ rB ↦⟨⊤⟩ gB'↓vC ⋆ rC ↦⟨⊤⟩ gC'↓vA) in
make_function_contract pre post›
ucincl_auto rotate_ref3_contract
text‹To prove the specification for ▩‹rotate_ref3›, we could just unfold/inline the definition of
▩‹swap_ref_fun›:›
lemma rotate_ref3_spec:
shows ‹Γ; rotate_ref3 rA rB rC ⊨⇩F rotate_ref3_contract rA rB rC gA vA gB vB gC vC›
apply (crush_boot f: rotate_ref3_def contract: rotate_ref3_contract_def)
apply (crush_base simp add: swap_ref_fun_def)
done
text‹This ∗‹can› work, but may lead to issues with SSA normalization. The more robust way to inline
a function is to explicitly mark it via the ▩‹inline: ...› configuration option:›
lemma rotate_ref3_spec':
shows ‹Γ; rotate_ref3 rA rB rC ⊨⇩F rotate_ref3_contract rA rB rC gA vA gB vB gC vC›
apply (crush_boot f: rotate_ref3_def contract: rotate_ref3_contract_def)
apply (crush_base inline: swap_ref_fun_def)
done
text‹This looks like a fine proof -- certainly without much work -- but we effectively need to reprove
the spec for ▩‹swap_ref_fun› with every invocation, which is neither scalable nor modular.
Instead, the proof should refer to the already-proven specification of ▩‹swap_ref_fun›. This is done
by registering spec and proof via ▩‹contracts add: ...› and ▩‹spec add: ...›, respectively:›
lemma
notes image_cong[cong del]
shows ‹Γ; rotate_ref3 rA rB rC ⊨⇩F rotate_ref3_contract rA rB rC gA vA gB vB gC vC›
apply (crush_boot f: rotate_ref3_def contract: rotate_ref3_contract_def)
using [[crush_log_toplevel]]
apply (crush_base specs add: swap_ref_fun_spec contracts add: swap_ref_fun_contract_def)
done
text‹To avoid explicitly listing all specifications and contracts needed by a proof, one can
alternatively globally or locally populate the underlying named theorem lists ▩‹crush_specs›
and ▩‹crush_contracts›. This is the prevalent style used in the code base, where we mark
contracts/specs as ▩‹crush_contracts/crush_specs› at time of definition/proofs.›
declare swap_ref_fun_spec[crush_specs, crush_specs_eager]
declare swap_ref_fun_contract_def[crush_contracts]
lemma
shows ‹Γ; rotate_ref3 rA rB rC ⊨⇩F rotate_ref3_contract rA rB rC gA vA gB vB gC vC›
apply (crush_boot f: rotate_ref3_def contract: rotate_ref3_contract_def)
by crush_base
no_adhoc_overloading store_update_const ⇌
update_fun
end
subsubsection‹Reasoning about references and structures›
text‹The next examples demonstrate how ▩‹crush› can reason about structure and array manipulation.
They are also useful as vehicles to understand and improve the underlying focus and lens mechanics.›
text‹The examples will operate on the following structures:›