Commit 55169406 authored by Dan Frumin's avatar Dan Frumin

Tried proving increment function

parent 0337bba4
......@@ -109,4 +109,73 @@ Section test.
iApply a_seq_spec. iUnlock; iFrame.
Qed.
Definition incr1 : val := λ: "l",
a_store (a_ret "l") (a_bin_op PlusOp (a_load "l") (a_ret #1)).
Lemma incr1_spec (l : loc) (n : Z) R :
l U #n -
awp (incr1 #l) R (λ _, l L #(n+1)).
Proof.
iIntros "Hl". awp_lam.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
iApply awp_bind.
iApply (awp_par (λ v, v = #l) (λ v, v = #(n+1) l U #n) with "[] [Hl]")%I.
- by iApply awp_value.
- rewrite /awp.
iApply wp_value.
iIntros (γ π env lk) "#Hlock1 Hunfl1". do 2 wp_let.
Opaque par.
repeat wp_pure _.
admit.
- iNext. iIntros (? ?) "% [% Hl]"; simplify_eq.
iNext. awp_lam.
(* a_store_spec copypasta ahead *)
iApply awp_atomic_env.
iIntros (env) "Henv HR". wp_lam.
{ rewrite {2}/env_inv.
iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
iDestruct "Hlocks" as %Hlocks.
iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hl.
assert (#l X).
{ unfold correct_locks in *. intros Hx. apply Hl.
destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. }
wp_proj.
wp_apply (mset_add_spec with "[$HX]"); eauto.
iIntros "HX". wp_seq.
iAssert (⌜σ !! l = Some ULvl%I) with "[Hσ Hl]" as %?.
{ rewrite mapsto_eq /mapsto_def.
iDestruct "Hl" as "[Hv Hl]".
by iDestruct (own_valid_2 with "Hσ Hl")
as %[?%heap_singleton_included _]%auth_valid_discrete_2. }
iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ Hl") as "[Hσ Hl]".
do 2 wp_proj. rewrite mapsto_eq /mapsto_def.
iDestruct "Hl" as "[Hv Hl]".
rewrite (big_sepM_lookup_acc _ _ l ULvl); last done.
iDestruct "Hls" as "[Hl' Hls]".
iDestruct "Hl'" as (?) "Hl'".
iDestruct (mapsto_agree l (1/2) (1/2) with "Hl' Hv") as %->.
iCombine "Hv Hl'" as "Hv".
wp_store.
iDestruct "Hv" as "[Hv Hl']".
iSpecialize ("Hls" with "[Hl']"); eauto.
wp_proj. iFrame "HR". iSplitR "Hl Hv".
- iExists ({[#l]} X),(<[l:=LLvl]> σ). iFrame. iSplitL.
+ rewrite -big_sepM_insert_override; eauto.
+ (* TODO: a separate lemma somewhere *)
iPureIntro. rewrite locked_locs_lock.
revert Hlocks. rewrite /correct_locks /set_Forall. set_solver.
- iFrame. }
Admitted.
End test.
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