Commit 9197f96f authored by Ike Mulder's avatar Ike Mulder
Browse files

Added tutorial files.

parent 9fdaacb2
......@@ -4,8 +4,17 @@
*.vos
*.glob
theories/**/*.tex
tutorial/*.tex
**/coqdoc.sty
**/coqdoc.css
tutorial/*.pdf
tutorial/*.html
tutorial/*.log
tutorial/*.fls
tutorial/*.fdb_latexmk
tutorial/*.out
*.crashcoqide
.*.aux
**.aux
.coqdeps.d
.allvfiles.d
.curvfiles.d
......
COQDOCEXTRAFLAGS = --body-only -s
COQDOCEXTRAFLAGS = -s -p '\usepackage{textgreek}\usepackage[libertine]{newtxmath}\DeclareUnicodeCharacter{8988}{$$\ulcorner$$}\DeclareUnicodeCharacter{8989}{$$\urcorner$$}\DeclareUnicodeCharacter{10033}{$$\gamma$$}\DeclareUnicodeCharacter{8875}{$$\VDash$$}' --no-index
......@@ -12,11 +12,11 @@ HAS_EXTERNAL := $(shell if [ -d "./external" ] && [ -n "$$(find ./external/ -typ
# above if statement checks if there are regular files in that directory
# this should indicate having run `git submodule init --update --recursive`
ifeq ("$(HAS_EXTERNAL)", "1")
SRC_DIRS := 'theories' 'external'
SRC_DIRS := 'theories' 'external' 'tutorial'
SRC_FIND_OPTS :=
COQ_PROJ_FILE = _CoqProject
else
SRC_DIRS := 'theories'
SRC_DIRS := 'theories' 'tutorial'
SRC_FIND_OPTS := -not \( -path theories/examples/external -prune \)
COQ_PROJ_FILE = _CoqProject_noext
endif
......
(** Welcome to the Diaframe tutorial, part 1!
In this example, we will be verifying a modified version of the 'oneshot' example from the
'Iris from the ground up' paper (%\url{https://doi.org/10.1017/S0956796818000151}% #<a href="https://doi.org/10.1017/S0956796818000151">link</a>#), section 2.
Although the program itself is not very useful, it is relatively simple,
and can illustrate the core reasoning principles of Iris and the automation of Diaframe.
Before we dive into the verification, we need to get access to Iris and Diaframe. *)
From iris.heap_lang Require Import proofmode.
From diaframe.heap_lang Require Import stepping_tacs.
(** The first imports give us access to Iris's heap_lang language, along with its notation and tactics.
The second import loads the Diaframe tactics, as well as a collection of hints for the heap_lang language.
To verify this example, we will be needing some ghost resources. An in-depth explanation of
these is beyond the scope of this tutorial, more information can be found in the
%Iris documentation: \url{https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/resource_algebras.md}.%
#<a href="https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/resource_algebras.md">Iris documentation.</a>#
The next two lines give us access to the required resources, and load additional Diaframe hints concerning these.
*)
From iris.algebra Require Import agree csum excl.
From diaframe.lib Require Import own_hints.
(** We now define the methods of our example.
These are all written in heap_lang, a lambda-calculus with access to a heap.
Relevant heap operations for this example are:
- [ref v] allocates and returns a new location that initially maps to value [v].
- [! l] performs a 'load': it returns the value [v] for which [l ↦ v].
- [CAS l v1 v2] performs a Compare And Swap operation.
It checks whether currently [l ↦ v1], and only if so, writes [v2] to location [l].
It returns a boolean indicating whether this swap happened.
*)
Definition mk_oneshot : val :=
λ: "_", ref NONE.
(** [mk_oneshot] simply allocates a location which initially mapsto to [NONE], or nil.
The idea of this example is to allow multiple threads to try to write [SOME] number to this location,
but only one may succeed. By this agreement, any thread is allowed to read the location.
Moreover, any thread that witnesses that this location now maps to [SOME] number [z],
knows that this location will forever map to this number [z].
We define the following operations on such a 'oneshot' location:
*)
Definition tryset : val :=
λ: "c" "n", CAS "c" NONE (SOME "n") ;; #().
(** [tryset l z] will _try_ to _set_ oneshot-location [l] to the number [z].
The method does not report on its success.
Note that the binders of heap_lang are strings. This is done because heap_lang is a deeply embedded language.
The notation [#()] stands for the unit value.
*)
Definition check : val :=
λ: "c",
match: ! "c" with
NONE => λ: "_", #()
| SOME "n" => λ: "_",
match: ! "c" with
NONE => #() #() (* unsafe *)
| SOME "m" =>
if: "m" = "n" then #() else #() #()
end
end.
(** [check l] returns a closure [f]. This closure remembers the value once read from location [l].
If the closure is called, it will compare the newly read value ["m"] to the previously read value ["n"].
If these are unequal, the closure will (try to) execute [#() #()], which applies the unit value to the unit value.
This would be unsafe. We aim to show that the closure returned by [check l] is, in fact, safe,
so the branches with [#() #()] are unreachable.
What follows now are some incantations to modularly get access to our desired ghost state.
We will discuss the properties of this ghost state further on.
*)
Definition oneshotR := csumR (exclR unitO) (agreeR ZO).
Class oneshotG Σ := OneShotG {
oneshot_tokG :> inG Σ oneshotR
}.
Definition oneshotΣ : gFunctors := #[GFunctor oneshotR].
Global Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ oneshotG Σ := verify.
Section verification.
(** We are now ready to write down the desired invariants and specifications.
To enable modular verification, the specifications are parametrized over a [Σ : gFunctors].
Think of this [Σ] as a kind of ghost-state register. To perform the verification, we need
access to the ↦-connective, and to our desired 'oneshot' ghost state. To express that
the ghost-state register [Σ] should contains these, we write: *)
Context `{!heapGS Σ, !oneshotG Σ}.
(** The idea is now that this verification works for all registers having at least these two kinds of ghost state.
We will need an invariant for this verification, which also needs a name.
*)
Let N := nroot.@"oneshot".
(** We are now ready to write down the invariant: *)
Definition oneshot_inv γ (l : loc) : iProp Σ :=
(v : val), l v
(v = NONEV own γ (Cinl $ Excl ())
(z : Z), v = SOMEV #z own γ (Cinr $ to_agree z)).
(** There are several things to note here. We could have written [oneshot_inv] as
<<
Definition oneshot_inv' γ (l : loc) : iProp Σ :=
(l ↦ NONEV ∗ own γ (Cinl $ Excl ())) ∨
(∃ (z : Z), l ↦ SOMEV #z ∗ own γ (Cinr $ to_agree z)).
>>
We do not do this, since Diaframe's hint search cannot recurse into disjunctions.
[l ↦ v] is taken out of the disjunction to ensure that Diaframe can find it when needed.
Another thing to note is the order of the resources. By setting [l ↦ v] first,
the physical value [v] can be used to guide the proof search, indicating which side
of the disjunction to try to prove.
Another important part is, of course, the ghost state [own γ _]. The relevant rules of our ghost state are:
- allocation: [⊢ |==> ∃ γ, own γ (Cinl $ Excl ())]
- 'shooting': [own γ (Cinl $ Excl ()) ⊢ |==> own γ (Cinr $ to_agree n)]
- shot-duplication: [own γ (Cinr $ to_agree n) ⊣⊢ own γ (Cinr $ to_agree n) ∗ own γ (Cinr $ to_agree n)]
- shot-agreement: [own γ (Cinr $ to_agree n) ∗ own γ (Cinr $ to_agree m) ⊢ ⌜m = n⌝]
By importing [own_hints], Diaframe is aware of all these rules, except the shooting rule.
To present a clean interface for clients, we hide away the details of the invariant.
We do this by defining an [is_oneshot] predicate, as below, and use this in all our specifications.
*)
Definition is_oneshot γ (v : val) : iProp Σ := (l : loc), v = #l inv N (oneshot_inv γ l).
(** Alright, let's do our first verification!
The following lemma is our desired specification of [mk_oneshot]: no preconditions,
and the returned value [is_oneshot].
This is a 'regular' Iris Texan Triple -- mostly equivalent to a standard hoare triple, but
easier to use in interactive proofs.
[mk_oneshot_spec_manual] shows how one could verify this in regular Iris.
*)
Lemma mk_oneshot_spec_manual :
{{{ True }}} mk_oneshot #() {{{ γ v, RET v; is_oneshot γ v }}}.
Proof.
iStartProof. (** This shows what a Texan Triple unfolds to. *)
iIntros (Φ) "_ HΦ".
wp_lam.
wp_alloc l as "Hl".
iMod (own_alloc _) as (γ) "Hγ"; last first.
- iApply "HΦ".
iExists l. iSplitR => //.
iApply inv_alloc.
iExists NONEV. eauto with iFrame.
- done.
Qed.
(** We will now tackle the same goal, but using Diaframe. *)
Lemma mk_oneshot_spec_1 :
{{{ True }}} mk_oneshot #() {{{ γ v, RET v; is_oneshot γ v }}}.
Proof.
(** To prove our specification, we first enter the Iris Proof Mode. *)
iStartProof.
(** Diaframe's most relevant tactic is [iStepS]. It performs a single _chunk of steps_ of the
automation described in the paper. Let's see what happens.
We will explain the actions of [iStepS] after each call, as well as a comparable IPM command.
*)
iStepS. (** Introduce the predicate [x]. [iIntros (x)] *)
iStepS. (** Introduce the trivial hypothesis [True] [iIntros "_"] *)
iStepS. (** Introduce the hypothesis on [x] [iIntros "H1"] *)
iStepS. (** Use pure reduction to unfold [mk_oneshot] [wp_lam], roughly *)
iStepS. (** Introduce the later modality, strip it off ["H1"] ... *)
iStepS. (** pure_reduction: [InjL] → [InjLV] [wp_pures], roughly *)
iStepS. (** Introduce the later modality ... *)
iStepS. (** Apply the specification of [ref] [wp_alloc x0 as "H2"], roughly *)
iStepS. (** Prove the precondition of [ref]: trivial ... *)
iStepS. (** Introduce the newly allocated location [x0] ... *)
iStepS. (** Introduce the later modality ... *)
iStepS. (** Acquire resource ["H2": x0 ↦ InjLV #()] ... *)
iStepS. (** Apply the wp-value rule ... *)
iStepS. (** This does not correspond to a single IPM tactic.
Diaframe finds a hint from "H1" to our goal, which notices that the [γ] argument to "H1" need
not be instantiated right away. The resulting goal thus existentially quantifies over [γ], which will be crucial later.
To reach this goal with regular IPM tactics, one can use
[iAssert (|={⊤}=> ∃ γ, is_oneshot γ #x0)%I with "[H2]" as ">[%γ Hγ]"; last by iApply "H1".] *)
iStepS. (** Instantiates _only_ the second existentials with [x0]. This, again, does not correspond to a single IPM tactic *)
iStepS. (** Applies the invariant allocation rule, but beneath the binder [x1] *)
iStepS. (** Instantiates _only_ the second existential with [InjLV #()] *)
iStepS. (** Simplifies the disjunction. *)
Fail iStepS. (** [iStepS] fails to proceed, since it is not smart enough to eliminate the second branch. What now? *)
(* To investigate where how Diaframe gets stuck, we can look at the smaller steps. These can be witnessed by first running
[iStepDebug], then running [solveStep] one or several times. Essentially, << iStepS := iStepDebug; repeat solveSteps >>. *)
iStepDebug. (** We see that the focused goal _is_ a disjunction. To choose a side, we can use IPM's [iLeft] or [iRight] tactic. *)
iLeft. (** Now we are back in a goal Diaframe can handle: *)
iStepS. (** Applies the own allocation rule. *)
iStepS. (** Solves the remaining pure goal. *)
Qed.
(** The repetition of [iStepS] in the proof above is not required or recommended, but illustrates the individual steps taken by Diaframe.
You can let Diaframe take more steps by using the [iStepsS] command.
Texan Triples as above are nice, but such specifications are not automatically available to Diaframe. To make specifications
available to Diaframe, write them as SPEC triples. For example: *)
Lemma mk_oneshot_spec_2 :
SPEC {{ True }} mk_oneshot #() {{ γ (v : val), RET v; is_oneshot γ v }}.
Proof.
iStepsS. (** Runs [iStepS] until it gets stuck, like in line 186 above. Note that this also performs [iStartProof] if necessary. *)
iSmash. (** If you get stuck on a disjunction, you can try to use [iSmash].
[iSmash] is like [iStepsS], but tries both [iLeft] and [iRight] when it gets stuck. *)
Restart. (** So actually, this entire goal can be solved by [iSmash]. Indeed: *)
iSmash.
Qed.
(** Since the proofs become just a single tactic, we are in shape to generate proofs automatically with [Program].
Diaframe provides a tweaked version of both [iSmash] and [iStepsS] for automatic proof generation with [Program].
Enable this as follows: *)
Local Obligation Tactic := program_smash_verify.
Global Program Instance mk_oneshot_spec_3 :
SPEC {{ True }} mk_oneshot #() {{ γ (v : val), RET v; is_oneshot γ v }}.
(* We want to verify [tryset] next. We need the following lemma for ghost state to proceed.
This is the 'shooting' ghost rule mentioned above. The proof need not be understood. *)
Lemma shoot_update γ n :
own γ (Cinl $ Excl ()) |==> own γ (Cinr $ to_agree n) own γ (Cinr $ to_agree n).
Proof. rewrite -own_op -Cinr_op agree_idemp. by apply own_update, cmra_update_exclusive. Qed.
(** We will now verify that tryset is _safe_. The specification is simply: *)
Lemma tryset_spec_1 γ (v : val) (z : Z) :
SPEC {{ is_oneshot γ v }} tryset v #z {{ RET #(); True }}.
Proof. (** Let's run the automation and see what happens. *)
iStepsS. (** We get stuck! Diaframe does not know how to proceed.
We ended up here as follows. To perform the CAS, we needed access to [l ↦ v].
Diaframe opened the invariant accordingly. Now consider the case where the CAS succeeds (the other case poses no problem).
We need to restore the invariant [oneshot_inv]. Diaframe sees that the left-hand side of the disjunction is contradictory,
so tries to prove the right-hand side. It gets stuck at our current goal, where we need to perform a ghost-update to proceed.
What now? One approach is to return to a regular IPM goal, and continue with a manual proof.
*)
unseal_diaframe => /=. (** Now we are back to a regular Iris goal, and finish using [shoot_update]. *)
iSplitL.
- iMod (shoot_update with "H3") as "[$ #H3]". done.
- iStepsS. (** This goal poses no problems for Diaframe. *)
Qed.
(** Instead of reverting to a manual proof, one can also register a hint for Diaframe.
In this case, this can be done as follows. *)
Instance shoot_hint γ z :
BiAbd (TTl := [tele]) (TTr := [tele]) (* no goal and sidecondition existentials *)
false (* indicates key hypothesis is spatial, not persistent *)
(own γ $ Cinl $ Excl ()) (* key hypothesis *)
(own γ $ Cinr $ to_agree z) (* atomic goal *)
(bupd) (* modality behind which goal can be proven *)
emp%I (* sidecondition / anti-frame *)
(own γ $ Cinr $ to_agree z) (* residue / frame *).
Proof. rewrite /BiAbd /=. iStepS. iApply shoot_update. iStepsS. Qed.
(** Note that we use [bupd] as the modality, instead of [fupd _ _] as in the paper.
Diaframe uses the fact that [|==> P ⊢ |={E,E}=> P] for all [P] and [E] to apply such hints. *)
(** Now try running the Diaframe automation again for the verification of [tryset]! *)
Global Instance tryset_spec_2 γ (v : val) (z : Z) :
SPEC {{ is_oneshot γ v }} tryset v #z {{ RET #(); True }}.
Proof. Admitted.
(** Again, try running the Diaframe automation for the verification of [check].
An interesting part of [check] is that it returns a closure,
and the specification of this closure is part of the postcondition of [check]:
the [□ WP f #() {{ w, ⌜w = #()⌝] part. Prefixing this with [□], means that the specification keeps holding,
i.e. that we can execute the closure more than once. *)
Global Instance check_spec γ (v : val) :
SPEC {{ is_oneshot γ v }} check v {{ (f : val), RET f; WP f #() {{ w, w = #() }}}}.
Proof. Admitted.
(* We need the following once we make is_oneshot Opaque *)
Global Program Instance oneshot_persistent γ v : Persistent (is_oneshot γ v).
End verification.
(** This is to prevent anyone (including Diaframe) to look inside the following definitions.
That should no longer be necessary: the specifications are all one should need. *)
Global Opaque is_oneshot mk_oneshot tryset check.
(** We have verified our oneshot library -- let's use it to verify some clients!
These clients do not do anything fancy, but they make use of the following facts:
- [is_oneshot _ _] can be shared between threads
- closures returned by [check] can be used multiple times, and concurrently
*)
Definition client_thread : val :=
λ: "c" "n",
let: "f_pre" := check "c" in
Fork ("f_pre" #());;
tryset "c" "n";;
let: "f_post" := check "c" in
Fork ("f_post" #());;
"f_post" #() ;;
"f_pre" #().
Definition oneshot_client : val :=
λ: <>,
let: "c" := mk_oneshot #() in
Fork (client_thread "c" #5) ;;
Fork (client_thread "c" #3) ;;
check "c" #().
Section client_verification.
(** We start the verification of clients. Once again, we parametrize over appropriate [Σ]s. *)
Context `{!heapGS Σ, !oneshotG Σ}.
(** The verifications just show the client programs are safe. *)
Global Instance client_thread_spec γ (v : val) (z : Z) :
SPEC {{ is_oneshot γ v }} client_thread v #z {{ RET #(); True }}.
Proof. Admitted.
Global Instance oneshot_client_spec :
SPEC {{ True }} oneshot_client #() {{ RET #(); True }}.
Proof. Admitted.
End client_verification.
(** To conclude this example, we generate a closed proof of safety of [oneshot_client].
For a more thorough explanations, see the
%Iris documentation: \url{https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/resource_algebras.md#obtaining-a-closed-proof}.%
#<a href="https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/resource_algebras.md##obtaining-a-closed-proof">Iris documentation.</a>#
*)
From iris.heap_lang Require Import adequacy.
(** We need a specific [Σ] for a closed proof - the 'ghost-state register' which needs to satisfy [heapGS Σ] and [oneshotG Σ].
This can be constructed as follows. *)
Definition clientΣ : gFunctors := #[ heapΣ; oneshotΣ ].
(** The statement '[oneshot_client #()] is safe' in Coq becomes the following: *)
Lemma client_adequate σ : adequate NotStuck (oneshot_client #()) σ (λ _ _, True).
Proof. apply (heap_adequacy clientΣ)=> ?. iStepsS. Qed.
(** We can ask Coq to check if any Axioms were used in the proof of [client_adequate].
If you have completed the proofs correctly, this should print: 'Closed under the global context' *)
Print Assumptions client_adequate.
(** Welcome to the Diaframe tutorial, part 2.
In this example, we will be verifying an implementation of the Treiber stack.
This tutorial assumes that you have finished part 1 of the tutorial. You may want to
return to part 1 if you do not grasp pieces of this tutorial.
*)
From iris.heap_lang Require Import proofmode.
From diaframe.heap_lang Require Import stepping_tacs.
Definition new_stack : val :=
λ: <>, ref NONEV.
Definition push_this : val :=
rec: "push" "s" "l" :=
let: "tail" := ! "s" in
"l" + #1 <- "tail" ;;
if: CAS "s" "tail" (SOME "l") then
#()
else
"push" "s" "l".
Definition push : val :=
λ: "s" "v",
let: "l" := AllocN #2 "v" in
push_this "s" "l".
Definition pop : val :=
rec: "pop" "s" :=
match: !"s" with
NONE => NONEV
| SOME "l" =>
let: "next" := !("l" + #1) in
if: CAS "s" (SOME "l") "next" then
SOME (! "l")
else
"pop" "s"
end.
(** This example features two new heap operations:
- The store operation [l <- v] writes value [v] to location [l]
- The [AllocN n v] allocates an array of length [n], initialized with value [v]
The [+ₗ] operation is used to add an offset to a pointer, i.e. to index in an array.
Additionally, the [push_this] and [pop] methods feature the [rec:] keyword.
This indicates the definition of a _recursive_ function. The first argument to [rec:]
is a binder, containing the recursive reference to the current function.
We will not be needing any ghost-state for this example. What we will need,
is a recursive definition of what it means to be a stack.
*)
Section verification.
Context `{!heapGS Σ}.
(** The algorithm described above operates on memory that has a specific layout:
locations [l] for which [l ↦ v], and [l +ₗ 1 ↦ ml], where either [ml = NONEV] or [ml = SOMEV l'],
with [l'] the again the same layout. We want to indicate that [SOMEV l] describes a
list of values, with [v] being the head of the list, and [ml] describing the tail of the list.
In the spirit of iCAP, we may want these values to satisfy some predicate P. For example,
if the stored values are locations, the predicate P may require them to map to a certain value.
In Iris, such a definition can be given as follows:
*)
Fixpoint is_list (P : val iProp Σ) (xs : list val) (lv : val) : iProp Σ :=
match xs with
| [] => lv = NONEV
| x :: xs => (l : loc), lv = SOMEV #l l ↦□ x P x
lv', (l + 1) ↦□ lv' is_list P xs lv'
end.
(** We make use of the persistent mapsto [l ↦□ _] here. This is necessary, since
a very slow [pop] may try to load a location that has been [pop]'ed concurrently
a while ago. The relevant rule for this persistent mapsto is [l ↦{#q} v ⊢ |==> l ↦□ v].
The stack just contains a pointer to a value which [is_list], so we have:
*)
Definition stack_inv P l :=
( vl, l vl xs, is_list P xs vl)%I.
(** And as before, we wrap this in an [is_stack] predicate to hide away the implementation details *)
Let N := nroot .@ "stack".
Definition is_stack (P : val iProp Σ) v : iProp Σ :=
(l : loc), v = #l inv N (stack_inv P l)%I.
(** Our ideal specification for [new_stack] is as follows. *)
Global Instance new_stack_spec :
SPEC {{ True }}
new_stack #()
{{ (s : val), RET s; P, |={}=> is_stack P s }}.
Proof.
iStepsS.
(** We get stuck here! Diaframe does not have native support for recursive definitions like [is_list].
We need an appropriate hint. Remember that we got stuck on a goal of the form:
[∃ xs, is_list P xs NONEV]
*)
Abort.
(** Exercise: change the hint to have proper side-conditions and frame, then prove the hint. *)
Global Instance biabd_islist_none xs P :
BiAbd (TTl := [tele]) (TTr := [tele])
false empty_hyp_first
(is_list P xs NONEV)
id
emp%I (* sidecondition - replace me *)
False%I (* residue - replace me *).
Proof.
rewrite /BiAbd /=.
(** This hint has key hypothesis [empty_hyp_first]. This is another special proposition that is treated
differently by the proof search strategy, like [empty_hyp_last] (ε₁ in the paper). The semantics of
[empty_hyp_first] is just [True], but this hypothesis is always the first hypothesis in every environment Δ.
It can be used for hints to add simplification rules.
*)
iStepS.
Admitted.
(** For this hint, we use [id] as the modality. Diaframe automatically uses the fact that
[id P ⊢ |={E,E}=> P] for all [E] and [P] when applying such hints. *)
Obligation Tactic := verify_tac.
Global Program Instance new_stack_spec :
SPEC {{ True }}
new_stack #()
{{ (s : val), RET s; P, |={}=> is_stack P s }}.
(** Now we can get on with the verification of [push_this]. The specification we want is as follows. *)
Global Instance push_this_spec P (s : val) (l : loc) (v w : val) :
SPEC {{ is_stack P s l v (l + 1) w P v }}
push_this s #l
{{ RET #(); True }}.
Proof.
iStepsS.
(** Like before, we just try [iStepsS]. This time, it stops at just [WP push_this ..], and
does not unfold [push_this]. This is because Diaframe's heap_lang support is set up to
_not_ unfold recursive functions. Verifications of such functions usually require
a form of induction.
In this case, we use Löb induction, as follows. *)
iLöb as "IH" forall (w).
(** We now skip ahead to the part of the verification that currently poses problems.
We start with [wp_lam] to force unfolding [push_this] - as noted above, Diaframe won't do that *)
wp_lam. do 24 iStepS.
(** Stepping again shows us the specification of [CAS]/[CmpXchg] *)
iStepS.
(** The problem lies in the [vals_compare_safe] proposition.
As heap_lang is a lambda-calculus, lambda's are also values. The current semantics
of heap_lang allow storing any value in a location, including lambda's. Such locations
can also be CAS'ed, which would require a comparison of lambda's. This has been deemed
unrealistic, so the specification of CAS requires the two compared values to satisfy
[vals_compare_safe]. This boils down to requiring that either value is [val_is_unboxed],
meaning a 'regular' literal value.
In our situation, we do not have this information available, so the [vals_is_unboxed]
becomes an unsolvable proof obligation.
*)
iStepS.
Unshelve.
(** This is problematic. What to do? Well, [vals_compare_safe v] actually follows from
[is_list _ _ v]: either [v = NONEV] or there is a location [l] such that [v = SOMEV #l],
and in both cases we get [vals_is_unboxed v].
We need a way to make sure Diaframe picks up this information. *)
Abort.
(** This is what the [MergablePersist] typeclass is responsible for. It is written in CPS for
efficiency reasons. [MergablePersist H1 C] means that for all [p] [H2] [Hout],
[C p H2 Hout] means that [H1 ∗ □?p H2 ⊢ □ Hout]. Diaframe uses this information to
additionally learn [Hout] when introducing [H1] into a context that already contains [H2].
We can again take [H2] to be [empty_hyp_first], to learn [Hout] everytime we introduce [H1]
into a context. *)
Instance is_list_remember_1 P xs v :
MergablePersist (is_list P xs v) (λ p Pin Pout,
TCAnd (TCEq Pin empty_hyp_first)
(TCEq Pout (val_is_unboxed v)))%I | 30.
Proof.
rewrite /MergablePersist => p Pin Pout [-> ->] /=.
destruct xs; iStepsS.
Qed.
(** We now retry the verification of [push_this] *)
Lemma push_this_spec_1 P (s : val) (l : loc) (v w : val) :
SPEC {{ is_stack P s l v (l + 1) w P v }}
push_this s #l
{{ RET #(); True }}.
Proof.
iStepsS. iLöb as "IH" forall (w).
wp_lam. iStepsS.
(** We get stuck once again, on a goal of shape
[∃ xs, is_list P xs (SOMEV #l)]. All spatial hypotheses are relevant.
One way to proceed is as follows:
*)
iExists (v :: x5). iStepsS.
Qed.
(** Exercise: Create and prove a hint so that above proof can be done automatically.
Tips:
- Take [empty_hyp_last] as key hypothesis
- Look at the definition of [is_list] to figure out the sideconditions.
- If you want to use existential quantification over side conditions,
specify [(TTl := [tele_pair val; list val; val])] and use a lambda for your
sideconditions and residue, i.e. [(λ x xs' t, False)%I]
If you complete this exercise, the following should be provable with [Program]:
*)
Global Instance push_this_spec_2 P (s : val) (l : loc) (v w : val) :
SPEC {{ is_stack P s l v (l + 1) w P v }}
push_this s #l
{{ RET #(); True }}.
Proof. Admitted.
(** Note that we do not need to indicate the need for Löb induction when we use [Program]. This is because
[program_verify_tac] incorporates Löb induction by default. *)
Global Instance push_spec P (s v : val) :
SPEC {{ is_stack P s P v }}
push s v
{{