Commit 4c3f5b17 authored by Ralf Jung's avatar Ralf Jung

add some more printing to some tests

Just to cover more cases, hopefully.
parent f5defba3
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
hd, acc : val
xs, ys : list val
Φ : val → iPropI Σ
============================
"Hxs" : is_list hd xs
"Hys" : is_list acc ys
"HΦ" : ∀ w : val, is_list w (reverse xs ++ ys) -∗ Φ w
--------------------------------------∗
WP (rev hd) acc [{ v, Φ v }]
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
acc : val
ys : list val
Φ : val → iPropI Σ
============================
"Hys" : is_list acc ys
"HΦ" : ∀ w : val, is_list w ys -∗ Φ w
--------------------------------------∗
WP match: InjL #() with
InjL <> => acc
| InjR "l" =>
let: "tmp1" := Fst ! "l" in
let: "tmp2" := Snd ! "l" in
"l" <- ("tmp1", acc);; (rev "tmp2") (InjL #())
end [{ v, Φ v }]
......@@ -31,10 +31,10 @@ Lemma rev_acc_wp hd acc xs ys :
rev hd acc
[[{ w, RET w; is_list w (reverse xs ++ ys) }]].
Proof.
iIntros (Φ) "[Hxs Hys] HΦ".
iIntros (Φ) "[Hxs Hys] HΦ". Show.
iInduction xs as [|x xs] "IH" forall (hd acc ys Φ);
iSimplifyEq; wp_rec; wp_let.
- wp_match. by iApply "HΦ".
- Show. wp_match. by iApply "HΦ".
- iDestruct "Hxs" as (l hd' ->) "[Hx Hxs]".
wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
iApply ("IH" $! hd' (SOMEV #l) (x :: ys) with "Hxs [Hx Hys]"); simpl.
......
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
one_shotG0 : one_shotG Σ
Φ : val → iProp Σ
N : namespace
l : loc
γ : gname
============================
"HN" : inv N (one_shot_inv γ l)
--------------------------------------□
"Hl" : l ↦ InjLV #()
_ : own γ Pending
--------------------------------------∗
one_shot_inv γ l
∗ (⌜InjLV #() = InjLV #()⌝
∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
one_shotG0 : one_shotG Σ
Φ : val → iProp Σ
N : namespace
l : loc
γ : gname
m, m' : Z
============================
"HN" : inv N (one_shot_inv γ l)
"Hγ'" : own γ (Shot m)
--------------------------------------□
"Hl" : l ↦ InjRV #m'
"Hγ" : own γ (Shot m')
--------------------------------------∗
|={⊤ ∖ ↑N}=> ▷ one_shot_inv γ l
∗ WP match: InjR #m' with
InjL <> => assert: #false
| InjR "m" => assert: #m = "m"
end {{ _, True }}
......@@ -67,16 +67,16 @@ Proof.
iAssert (one_shot_inv γ l (v = NONEV n : Z,
v = SOMEV #n own γ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
{ iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
+ iSplit. iLeft; by iSplitL "Hl". eauto.
+ Show. iSplit. iLeft; by iSplitL "Hl". eauto.
+ iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
iSplitL "Hinv"; first by eauto.
iModIntro. wp_let. iIntros "!#". wp_seq.
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
{ by wp_match. }
wp_match. wp_bind (! _)%E.
iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
iInv N as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
{ by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
wp_load.
wp_load. Show.
iDestruct (own_valid_2 with "Hγ Hγ'") as %?%agree_op_invL'; subst.
iModIntro. iSplitL "Hl".
{ iNext; iRight; by eauto. }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment