Commit af8c5367 authored by Léon Gondelman's avatar Léon Gondelman

add bin_op_spec

parent 06c3dc56
......@@ -54,7 +54,7 @@ Definition a_while: val :=
Section proofs.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Lemma a_seq_spec R Φ :
Lemma a_seq_spec R Φ :
U (Φ #()) -
awp (a_seq #()) R Φ.
Proof.
......@@ -175,6 +175,27 @@ Section proofs.
- iApply ("HΦ" with "HΨ Hl'").
Qed.
Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : bin_op) (e1 e2: expr) :
awp e1 R Ψ1 - awp e2 R Ψ2 -
( v1 v2, Ψ1 v1 - Ψ2 v2 -
w, bin_op_eval op v1 v2 = Some w Φ w)-
awp (a_bin_op op e1 e2) R Φ.
Proof.
iIntros "H1 H2 HΦ".
iApply (a_fill [AppRCtx (a_bin_op op) ; AppLCtx e2] with "H1").
iIntros (w) "HΨ1 /=". awp_lam.
iApply (a_fill [AppRCtx (LamV "x2" ((a_bind (λ: "vv", a_ret (BinOp op (Fst "vv") (Snd "vv"))))%E ((a_par w) "x2")))%E] with "H2") .
iIntros (v) "HΨ2 /=". awp_lam.
iApply awp_bind.
iApply ((awp_par Ψ1 Ψ2) with "[$HΨ1] [$HΨ2]").
iNext. iIntros (w1 w2) "HΨ1 HΨ2"; subst.
iNext. awp_lam. iApply awp_ret. do 2 wp_proj.
iSpecialize ("HΦ" with "HΨ1 HΨ2").
iDestruct "HΦ" as (w0) "[% H]".
by wp_pure _.
Qed.
Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
awp e1 R (λ v, l : loc, v = #l Ψ1 l)-
awp e2 R Ψ2 -
......@@ -232,7 +253,7 @@ iDestruct ("HΦ" with "H1 H2") as (v) "[Hv HΦ]".
revert Hlocks. rewrite /correct_locks /set_Forall. set_solver.
- iApply "HΦ". iFrame.
Qed.
Lemma a_if_spec R Φ Ψ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
awp e R Ψ -
( v, Ψ v - (v = #true awp e1 R Φ) (v = #false awp e2 R Φ)) -
......
......@@ -9,6 +9,16 @@ From iris_c.c_translation Require Import monad lifting proofmode translation.
Section test.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Definition factorial_body : val := λ: "n" "c" "r",
a_while
(λ:<>, a_bin_op LeOp (a_load (a_ret "c")) (a_ret "n"))
(λ:<>, a_store (a_ret "c")
( a_bin_op PlusOp (a_load (a_ret "c")) (a_ret #1)) ;;;;
a_store (a_ret "r")
(a_bin_op MultOp (a_load (a_ret "r")) (a_load (a_ret "c"))) ;;;
a_seq #()).
Lemma test1 (l : loc) :
l L #1 -
awp (a_seq #();;; a_load (a_ret #l))%E True (fun v => v = #1 l U #1).
......@@ -73,7 +83,7 @@ Section test.
(* Qed. *)
Definition swap : val := λ: "l1" "l2",
a_bind (λ: "r",
a_bind (λ: "r",
(a_store (a_ret "r") (a_load (a_ret "l1"))) ;;;;
(a_store (a_ret "l1") (a_load (a_ret "l2"))) ;;;;
((a_store (a_ret "l2") (a_load (a_ret "r")))) ;;; a_seq #())
......@@ -94,7 +104,7 @@ Section test.
iApply (a_store_spec _ _ (λ l, l = r)%I (λ v, v = v1 l1 U v1)%I with "[] [Hl1]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ iApply (a_load_spec _ _ (λ v, v = l1)%I).
- iApply awp_ret. iApply wp_value; eauto.
- iApply awp_ret. iApply wp_value; eauto.
- iIntros (? ->). iExists _; iFrame. eauto. }
iIntros (? ? ->) "[% Hl1]"; subst.
iExists _; iFrame. iIntros "Hr". iUnlock.
......@@ -104,17 +114,17 @@ Section test.
iApply (a_store_spec _ _ (λ l, l = l1)%I (λ v, v = v2 l2 U v2)%I with "[] [Hl2]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ iApply (a_load_spec _ _ (λ v, v = l2)%I).
- iApply awp_ret. iApply wp_value; eauto.
- iApply awp_ret. iApply wp_value; eauto.
- iIntros (? ->). iExists _; iFrame. eauto. }
iIntros (? ? ->) "[% Hl2]"; subst.
iExists _; iFrame. iIntros "Hl1". iUnlock.
awp_seq.
iApply awp_bind.
iApply (a_store_spec _ _ (λ l, l = l2)%I (λ v, v = v1 r U v1)%I with "[] [Hr]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ iApply (a_load_spec _ _ (λ v, v = r)%I).
- iApply awp_ret. iApply wp_value; eauto.
- iApply awp_ret. iApply wp_value; eauto.
- iIntros (? ->). iExists _; iFrame. eauto. }
iIntros (? ? ->) "[% Hr]"; subst.
Opaque awp.
......
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