Commit d7dd1e96 authored by Dan Frumin's avatar Dan Frumin

Reorganize and clean up the tests

parent 6b695042
......@@ -16,13 +16,11 @@ theories/vcgen/denv.v
theories/vcgen/splitenv.v
theories/vcgen/vcgen.v
theories/vcgen/vcg_solver.v
theories/vcgen/tests/basics.v
theories/vcgen/tests/unknowns.v
theories/vcgen/tests/test.v
theories/vcgen/tests/swap.v
theories/vcgen/tests/fact.v
theories/vcgen/tests/memcpy.v
# theories/tests/test1.v
# theories/tests/test2.v
# theories/tests/gcd.v
theories/tests/basics.v
theories/tests/invoke.v
theories/tests/unknowns.v
theories/tests/swap.v
theories/tests/fact.v
theories/tests/memcpy.v
theories/tests/gcd.v
# theories/tests/lists.v
(** Testing basic connectives *)
From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.bi Require Import big_op.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.c_translation Require Import monad translation proofmode derived.
From iris_c.lib Require Import locking_heap U.
Section tests_vcg.
Section test.
Context `{amonadG Σ}.
(** dereferencing *)
Lemma test1 (l : cloc) (v: val) :
l C v - AWP ∗ᶜ ♯ₗl {{ w, w = v l C v }}.
Proof.
iIntros "Hl1". vcg_solver. auto.
Qed.
(** double dereferencing *)
Lemma test2 (l1 l2 : cloc) (v: val) :
l1 C cloc_to_val l2 - l2 C v -
AWP ∗ᶜ ∗ᶜ ♯ₗl1 {{ v, v = #1 l1 C cloc_to_val l2 - l2 C v }}.
Proof.
iIntros "Hl1 Hl2". vcg_solver. auto.
Qed.
(** sequence points *)
Lemma test3 (l : cloc) (v: val) :
l C v - AWP ∗ᶜ ♯ₗl ; ∗ᶜ ♯ₗl {{ w, w = v l C v }}.
Proof.
iIntros "Hl1". vcg_solver. auto.
Qed.
(** assignments *)
Lemma test4 (l : cloc) (v1 v2: val) :
l C v1 - AWP ♯ₗl = a_ret v2 {{ v, v = v2 l C[LLvl] v2 }}.
Proof.
iIntros "Hl1". vcg_solver. auto.
Qed.
Lemma store_load s l R :
s C #0 - l C #1 -
AWP ♯ₗs = ∗ᶜ ♯ₗl @ R {{ _, s C[LLvl] #1 l C #1 }}.
Proof.
iIntros "Hs Hl".
vcg_solver. eauto with iFrame.
Qed.
Lemma store_load_load s1 s2 l R :
s1 C #0 - l C #1 - s2 C #0 -
AWP ♯ₗs1 = ∗ᶜ ♯ₗl ; ∗ᶜ ♯ₗs1 + 42 @ R {{ _, s1 C #1 l C #1 }}.
Proof.
iIntros "Hs1 Hl Hs2". vcg_solver. iModIntro.
rewrite Qp_half_half. eauto with iFrame.
Qed.
(** double dereferencing & modification *)
Lemma test5 (l1 l2 r1 r2 : cloc) (v1 v2: val) :
l1 C cloc_to_val l2 - l2 C v1 -
r1 C cloc_to_val r2 - r2 C v2 -
AWP ♯ₗl1 = ♯ₗr1 ; ∗ᶜ ∗ᶜ ♯ₗl1
{{ w, w = v2
l1 C cloc_to_val r2 l2 C v1 r1 C cloc_to_val r2 - r2 C v2 }}.
Proof.
iIntros "**". vcg_solver. eauto 40.
Qed.
(** par *)
Lemma test_par_1 (l1 l2 : cloc) (v1 v2: val) :
l1 C v1 - l2 C v2 -
AWP ∗ᶜ ♯ₗl1 ||| ∗ᶜ ♯ₗl2
{{ w, w = (v1, v2)%V l1 C v1 l2 C v2 }}.
Proof.
iIntros "**". vcg_solver. rewrite Qp_half_half. eauto with iFrame.
Qed.
Lemma test_par_2 (l1 l2 : cloc) (v1 v2: val) :
l1 C v1 - l2 C v2 -
AWP (♯ₗl1 = a_ret v2) ||| (♯ₗl2 = a_ret v1)
{{ w, w = (v2, v1)%V l1 C[LLvl] v2 l2 C[LLvl] v1 }}.
Proof.
iIntros "**". vcg_solver. eauto with iFrame.
Qed.
(** pre bin op *)
Lemma test6 (l : cloc) (z0 : Z) R:
l C #z0 -
AWP ♯ₗl += 1 @ R {{ v, v = #z0 l C[LLvl] #(z0+1) }}.
Proof.
iIntros "Hl". vcg_solver. eauto.
Qed.
Lemma test7 (l k : cloc) (z0 z1 : Z) R:
l C #z0 -
k C #z1 -
AWP (♯ₗl += 1) + (∗ᶜ♯ₗk) @
R {{ v, v = #(z0+z1) l C[LLvl] #(z0+1) k C #z1 }}.
Proof.
iIntros "Hl Hk". vcg_solver. eauto with iFrame.
Qed.
(** more sequences *)
Lemma test_seq s l :
s C[ULvl] #0 - l C[ULvl] #1 -
AWP (♯ₗl = 2 ; 1 + (♯ₗ l = 1)) + (♯ₗ s = 4)
......@@ -42,7 +135,6 @@ Section tests_vcg.
iIntros "Hl Hk".
vcg_solver. iModIntro. by eauto with iFrame.
Qed.
Definition stupid (l : cloc) : expr :=
a_store (♯ₗ l) ( 1); a_ret #0.
......@@ -63,7 +155,7 @@ Section tests_vcg.
repeat iModIntro. by eauto with iFrame.
Qed.
Lemma test_sp1 l k :
Lemma test_seq6 l k :
l C #0 -
k C #0 -
AWP 1 + (♯ₗl = 1 ; (♯ₗk = 2) + ∗ᶜ ♯ₗl ; ∗ᶜ ♯ₗk + (♯ₗl = 2))
......@@ -74,7 +166,7 @@ Section tests_vcg.
eauto with iFrame.
Qed.
Lemma test_sp2 l :
Lemma test_seq7 l :
l C #0 -
AWP 1 + (♯ₗl = 1 ; ∗ᶜ ♯ₗl + ∗ᶜ ♯ₗl ; ♯ₗl = 2) {{ v, v = #3 l C[LLvl] #2 }}.
Proof.
......@@ -83,28 +175,7 @@ Section tests_vcg.
eauto with iFrame.
Qed.
Lemma store_load s l R :
s C #0 - l C #1 -
AWP ♯ₗs = ∗ᶜ ♯ₗl @ R {{ _, s C[LLvl] #1 l C #1 }}.
Proof.
iIntros "Hs Hl".
vcg_solver. eauto with iFrame.
Qed.
Lemma store_load_load s1 s2 l R :
s1 C #0 - l C #1 - s2 C #0 -
AWP ♯ₗs1 = ∗ᶜ ♯ₗl ; ∗ᶜ ♯ₗs1 + 42 @ R {{ _, s1 C #1 l C #1 }}.
(* (a_store (a_ret #s2) (a_load (a_ret #l)))) R (λ _, s1 ↦U #1 ∗ l ↦U #1). *)
Proof.
iIntros "Hs1 Hl Hs2". vcg_solver. iModIntro.
rewrite Qp_half_half. eauto with iFrame.
Qed.
Lemma test3 l :
l C #1 -
AWP (♯ₗl = 2) + (♯ₗl = 2) {{ _, True }}.
Proof. iIntros "Hl". vcg_solver. Abort.
(** while *)
Lemma test_while l R :
l C #1 -
AWP while (∗ᶜ ♯ₗl < 2) { ♯ₗl = 1 } @ R {{ _, True }}.
......@@ -116,5 +187,5 @@ Section tests_vcg.
iLeft. iSplitR; eauto.
vcg_solver. iIntros "Hl". iModIntro. by iApply "IH".
Qed.
End tests_vcg.
End test.
......@@ -3,65 +3,51 @@ From iris.heap_lang Require Import spin_lock assert par.
From iris.algebra Require Import frac auth.
From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.c_translation Require Import proofmode translation derived.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
Require Import Coq.ZArith.Znumtheory.
(* TODO: Notation, get rid of parenthesis around the while loop *)
Definition gcd : val := λ: "a" "b",
(a_while
(λ:<>, a_un_op NegOp
(a_bin_op EqOp (a_load (a_ret "a")) (a_load (a_ret "b"))))
(λ:<>, a_if (a_bin_op LtOp (a_load (a_ret "a")) (a_load (a_ret "b")))
(λ:<>, a_store (a_ret "b")
((a_bin_op MinusOp (a_load (a_ret "b")) (a_load (a_ret "a")))))
(λ:<>, a_store (a_ret "a")
((a_bin_op MinusOp (a_load (a_ret "a")) (a_load (a_ret "b")))))))
; a_load (a_ret "a").
(while (∗ᶜ(a_ret "a") != ∗ᶜ(a_ret "b")) {
if (∗ᶜ(a_ret "a") < ∗ᶜ(a_ret "b")) {
(a_ret "b") = ∗ᶜ(a_ret "b") - ∗ᶜ(a_ret "a")
} else {
(a_ret "a") = ∗ᶜ(a_ret "a") - ∗ᶜ(a_ret "b")
}
}) ;
∗ᶜ(a_ret "a").
Section gcd_spec.
Context `{amonadG Σ}.
(* TODO: use callᶜ *)
Lemma gcd_spec (a b : Z) (l r: cloc) R :
0 a 0 b
l C #a - r C #b -
awp (gcd (cloc_to_val l) (cloc_to_val r)) R (λ v, v = #(Z.gcd a b)).
Proof.
iIntros (??) "Hl Hr". do 2 awp_lam. iApply a_sequence_spec'. iNext.
iIntros (??) "Hl Hr". unfold gcd. do 2 awp_lam.
(* vcg_solver. *)
(* iIntros "Hr Hl". *)
iApply a_sequence_spec'. iNext.
iApply (a_while_inv_spec ( x y : Z,
0 x 0 y Z.gcd x y = Z.gcd a b l C #x r C #y)%I with "[Hl Hr]").
- iExists a, b. eauto with iFrame.
- iModIntro. iDestruct 1 as (x y (?&?&Hgcd)) "[Hl Hr]".
iApply a_un_op_spec.
iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
assert (x = y x < y y < x) as [Hxy|[Hxy|Hxy]] by lia.
+ iExists #true. simplify_eq /=. iSplit.
{ rewrite/ bin_op_eval //=; case_bool_decide; eauto. }
iExists #false; iSplit; first done. iLeft; iSplit; first done.
do 2 iModIntro. awp_load_ret l. iIntros.
by rewrite -Hgcd Z.gcd_diag Z.abs_eq.
+ iExists #false. simplify_eq /=. iSplit.
{ by rewrite /bin_op_eval //= bool_decide_false; last (intros [= ?]; lia). }
iExists #true; iSplit; first done. iRight; iSplit; first done.
iNext. iApply a_if_spec'.
iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
iExists #true; iSplit.
{ by rewrite /bin_op_eval //= bool_decide_true. }
iLeft. iSplit; first done.
iApply a_store_ret.
iApply (awp_bin_op_load_load with "[$Hr] [$Hl]"). iIntros "Hr Hl".
iExists #(y - x); iSplit; first by eauto with lia.
iExists #y. iIntros "{$Hr} Hr !>".
iExists x, (y-x). iFrame. rewrite -Hgcd Z.gcd_sub_diag_r. eauto with lia.
+ iExists #false. simplify_eq /=. iSplit.
{ by rewrite/ bin_op_eval //= bool_decide_false; last (intros [= ?]; lia). }
iExists #true; iSplit; first done. iRight; iSplit; first done.
iNext. iApply a_if_spec'.
iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
iExists #false. iSplit.
{ by rewrite/ bin_op_eval //= bool_decide_false; last lia. }
iRight; iSplit; first done.
iApply a_store_ret.
iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
iExists #(x - y); iSplit; first by eauto with lia.
iExists #x. iIntros "{$Hl} Hl !>". iExists (x - y), y. iFrame. iPureIntro.
rewrite -Hgcd Z.gcd_comm Z.gcd_sub_diag_r Z.gcd_comm. auto with lia.
vcg_solver.
iIntros "Hr Hl /=".
case_bool_decide; simpl; [ iLeft | iRight ];
iSplit; eauto.
+ repeat iModIntro. vcg_solver.
rewrite Qp_half_half. simplify_eq/=.
rewrite -Hgcd Z.gcd_diag Z.abs_eq; eauto with iFrame.
+ iNext. iApply a_if_spec'.
vcg_solver. rewrite !Qp_half_half.
iIntros "Hl Hr /=".
case_bool_decide; simpl; [ iLeft | iRight ];
(iSplit; first done);
vcg_solver;
eauto 400 with iFrame.
Qed.
End gcd_spec.
(** Testing function calls and AWP resources *)
From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.bi Require Import big_op.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
From iris_c.c_translation Require Import monad translation proofmode derived.
From iris_c.c_translation Require Import monad translation derived proofmode.
From iris_c.lib Require Import locking_heap U.
Section test.
Section tests_vcg.
Context `{amonadG Σ}.
Lemma test1 (l : cloc) (v: val) :
l C v - AWP ∗ᶜ ♯ₗl {{ w, w = v l C v }}.
Proof.
iIntros "Hl1". vcg_solver. auto.
Qed.
(* double dereferencing *)
Lemma test2 (l1 l2 : cloc) (v: val) :
l1 C cloc_to_val l2 - l2 C v -
AWP ∗ᶜ ∗ᶜ ♯ₗl1 {{ v, v = #1 l1 C cloc_to_val l2 - l2 C v }}.
Proof.
iIntros "Hl1 Hl2". vcg_solver. auto.
Qed.
Lemma test3 (l : cloc) (v: val) :
l C v - AWP ∗ᶜ ♯ₗl ; ∗ᶜ ♯ₗl {{ w, w = v l C v }}.
Proof.
iIntros "Hl1". vcg_solver. auto.
Qed.
Lemma test4 (l : cloc) (v1 v2: val) :
l C v1 - AWP ♯ₗl = a_ret v2 {{ v, v = v2 l C[LLvl] v2 }}.
Proof.
iIntros "Hl1". vcg_solver. auto.
Qed.
(* double dereferencing & modification *)
Lemma test5 (l1 l2 r1 r2 : cloc) (v1 v2: val) :
l1 C cloc_to_val l2 - l2 C v1 -
r1 C cloc_to_val r2 - r2 C v2 -
AWP ♯ₗl1 = ♯ₗr1 ; ∗ᶜ ∗ᶜ ♯ₗl1
{{ w, w = v2
l1 C cloc_to_val r2 l2 C v1 r1 C cloc_to_val r2 - r2 C v2 }}.
Proof.
iIntros "**". vcg_solver. eauto 40.
Qed.
Lemma test_par_1 (l1 l2 : cloc) (v1 v2: val) :
l1 C v1 - l2 C v2 -
AWP ∗ᶜ ♯ₗl1 ||| ∗ᶜ ♯ₗl2
{{ w, w = (v1, v2)%V l1 C v1 l2 C v2 }}.
Proof.
iIntros "**". vcg_solver. rewrite Qp_half_half. eauto with iFrame.
Qed.
Lemma test_par_2 (l1 l2 : cloc) (v1 v2: val) :
l1 C v1 - l2 C v2 -
AWP (♯ₗl1 = a_ret v2) ||| (♯ₗl2 = a_ret v1)
{{ w, w = (v2, v1)%V l1 C[LLvl] v2 l2 C[LLvl] v1 }}.
Proof.
iIntros "**". vcg_solver. eauto with iFrame.
Qed.
Definition c_id : val := λ: "v", a_ret ("v").
Lemma test_invoke_1 (l: cloc) R :
......@@ -78,15 +25,15 @@ Section test.
let: "v2" := Snd "vv" in
(a_ret "v1") + (a_ret "v2").
Lemma test_invoke_21 R :
AWP (call (plus_pair, 21 ||| 21)) @ R {{ v, v = #42 }}%I.
Lemma test_invoke_2 R :
AWP call (plus_pair, 21 ||| 21) @ R {{ v, v = #42 }}%I.
Proof.
iIntros. vcg_solver. awp_lam.
do 2 (awp_proj; awp_let).
vcg_solver. by vcg_continue.
Qed.
Lemma test_invoke_22 (l : cloc) R :
Lemma test_invoke_3 (l : cloc) R :
l C #21 -
AWP call (plus_pair, (∗ᶜ ♯ₗl ||| ∗ᶜ ♯ₗl)) @ R
{{ v, v = #42 l C #21 }}%I.
......@@ -96,21 +43,5 @@ Section test.
vcg_solver. iIntros "Hl". vcg_continue.
rewrite Qp_half_half. eauto 42 with iFrame.
Qed.
End tests_vcg.
Lemma test6 (l : cloc) (z0 : Z) R:
l C #z0 -
AWP ♯ₗl += 1 @ R {{ v, v = #z0 l C[LLvl] #(z0+1) }}.
Proof.
iIntros "Hl". vcg_solver. eauto.
Qed.
Lemma test7 (l k : cloc) (z0 z1 : Z) R:
l C #z0 -
k C #z1 -
AWP (♯ₗl += 1) + (∗ᶜ♯ₗk) @
R {{ v, v = #(z0+z1) l C[LLvl] #(z0+1) k C #z1 }}.
Proof.
iIntros "Hl Hk". vcg_solver. eauto with iFrame.
Qed.
End test.
......@@ -90,7 +90,7 @@ Section memcpy.
length ls2 = n
p C ls1 -
q C ls2 -
AWP a_invoke memcpy (♯ₗp ||| (♯ₗq ||| n)) @ R {{ _, p C ls2 q C ls2 }}.
AWP call (memcpy, (♯ₗp ||| (♯ₗq ||| n))) @ R {{ _, p C ls2 q C ls2 }}.
Proof.
iIntros (? ?) "Hp Hq". vcg_solver. awp_lam.
vcg_solver. iIntros (pp) "[Hpp _]".
......
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.algebra Require Import frac auth.
From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.c_translation Require Import proofmode translation derived.
Section test.
Context `{amonadG Σ}.
Lemma test1 (l : cloc) :
l C[LLvl]{1/2} #1 - l C[LLvl]{1/2} #1 -
awp (a_seq #();; a_load (a_ret (cloc_to_val l))) True (λ v, v = #1 l C #1).
Proof.
iIntros "Hl1 Hl2". iCombine "Hl1 Hl2" as "Hl".
rewrite Qp_half_half.
iApply awp_bind.
iApply a_seq_spec.
iModIntro.
awp_lam.
awp_load_ret l.
Qed.
Lemma test2 (l r : cloc) R :
l C #3 - r C #0 -
awp (a_store (a_ret (cloc_to_val l)) (a_ret #1);; a_seq #();; a_load (a_ret (cloc_to_val l))) R (λ v, v = #1).
Proof.
iIntros "Hl Hr".
iApply awp_bind.
iApply a_store_ret.
iApply awp_ret. iApply wp_value. iExists _; iFrame.
iIntros "Hl". awp_seq.
iApply awp_bind.
iApply a_seq_spec.
iModIntro. awp_seq.
awp_load_ret l.
Qed.
Definition swap : val := λ: "l1" "l2",
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 #())
(a_alloc (a_ret #1%nat) (a_ret #0)).
Lemma swap_spec (l1 l2 : cloc) (v1 v2: val) R :
l1 C v1 - l2 C v2 -
awp (swap (cloc_to_val l1) (cloc_to_val l2)) R (λ _, l1 C v2 l2 C v1).
Proof.
iIntros "Hl1 Hl2".
do 2 awp_lam. iApply awp_bind. awp_alloc_ret r "[Hr _]".
compute[cloc_add]. rewrite Nat.add_0_r.
assert ((r.1, r.2) = r) as -> by (destruct r; auto).
iApply a_sequence_spec'.
iNext. iApply (a_store_ret r with "[Hl1 Hl2 Hr]").
awp_load_ret l1. iIntros "Hl1". iExists #0. iFrame.
iIntros "Hr". iModIntro. iApply a_sequence_spec'.
iNext. iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret l2. iIntros "Hl2". iExists v1. iFrame.
iIntros "Hl1". iModIntro. iApply awp_bind.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret r. iIntros "Hr". iExists v2. iFrame.
iIntros "Hl2". awp_seq. iApply a_seq_spec. iModIntro. by iFrame.
Qed.
Lemma test_invoke (l : cloc) R :
l C[LLvl] #1 -
AWP a_invoke (λ: "x", a_load (a_ret "x")) ♯ₗl @ R {{ v, v = #1 l C #1 }}.
Proof.
iIntros "Hl".
iApply a_invoke_simpl.
(* TODO: the followings HANGS coq:
iApply (a_invoke_simpl _ _ _ (λ v, ⌜v = #l⌝)%I). *)
iApply awp_ret. wp_value_head.
iModIntro.
awp_let. awp_load_ret l.
Qed.
Definition assignF : val := λ: "lv",
let: "l" := Fst "lv" in
let: "v" := Snd "lv" in
a_store (a_ret "l") (a_ret "v") ; a_ret "v".
Lemma invoke_assignF_1 l (v v' : val) R :
l C v -
AWP a_invoke assignF (a_par ♯ₗl (a_ret v')) @ R
{{ w, l C v' w = v' }}.
Proof.
iIntros "Hl".
iApply a_invoke_simpl.
iApply (awp_par (λ v, v = cloc_to_val l)%I (λ v, v = v')%I).
- iApply awp_ret. by wp_value_head.
- iNext. iApply awp_ret. by wp_value_head.
- iNext. iIntros (? ? -> ->) "!> !>".
unfold assignF. awp_lam. awp_proj. awp_lam. awp_proj. awp_lam.
iApply a_sequence_spec. iNext.
iApply a_store_ret.
iApply awp_ret; wp_value_head.
iExists _; iFrame. iIntros "Hl".
iModIntro. awp_lam.
iApply awp_ret; wp_value_head. eauto.
Qed.
Lemma invoke_assignF_2 (l : cloc) (v' : val) R :
(AWP (a_invoke assignF (a_par ♯ₗl (a_ret v'))) @ (( v, l C v) R) {{ w, w = v' }})%I.
Proof.
iApply a_invoke_full.
iApply (awp_par (λ v, v = cloc_to_val l)%I (λ v, v = v')%I).
- iApply awp_ret. by wp_value_head.
- iNext. iApply awp_ret. by wp_value_head.
- iNext. iIntros (? ? -> ->) "!> !>".
iIntros "[Hl HR]".
unfold assignF. awp_lam. awp_proj. awp_lam. awp_proj. awp_lam.
iApply a_sequence_spec'. iNext.
iApply a_store_ret.
iApply awp_ret; wp_value_head.
iDestruct "Hl" as (?) "Hl".
iExists _; iFrame. iIntros "Hl".
iModIntro. iApply awp_ret; wp_value_head.
iSplit; eauto with iFrame.
Qed.
Lemma invoke_test (l : cloc) (z0 z1 z2: Z) R :
l C #z0 -
AWP (a_invoke assignF (♯ₗl ||| z1))
+ (a_invoke assignF (♯ₗl ||| z2)) @ R
{{ v, v = #(z1 + z2) ( w, l C w) }}.
Proof.
iIntros "Hl".
iApply (awp_insert_res _ _ ( v, l C v)%I with "[Hl]").
{ iNext. by iExists #z0. }
iApply a_bin_op_spec.
- iApply (invoke_assignF_2 l #z1).
- iApply (invoke_assignF_2 l #z2). (* TODO: we have to give z1/z2 explicitly here *)
- iIntros (? ? -> ->). iExists #(z1+z2). iSplit; eauto.
Qed.
Lemma inc_test1 (l : cloc) (z0 : Z) R:
l C #z0 -
AWP ♯ₗl += 1 @ R {{ v, v = #z0 l C[LLvl] #(z0+1) }}.
Proof.
iIntros "Hl".
iApply (a_pre_bin_op_spec _ _ (λ v, v = cloc_to_val l)%I (λ v, v = #1)%I);
try (iApply awp_ret; by wp_value_head).
iNext. iIntros (? ? -> ->) "HR". iExists _,_,#(z0+1); iFrame.
repeat iSplit; eauto.
Qed.
Lemma inc_test2 (l : loc) (z0 : Z) R:
l C #z0 -
AWP l += 1 @ R {{ v, v = #z0 l C[LLvl] #(z0+1) }}.
Proof.
iIntros "Hl".
iApply (a_pre_incr with "Hl").
iApply awp_ret; wp_value_head. iSplit; eauto.
Qed.
End test.
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.bi.lib Require Import fractional.
From iris.algebra Require Import frac auth.
From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.c_translation Require Import proofmode translation derived.
Section test.
Context `{amonadG Σ}.
Lemma test_fractional (x : cloc) :
x C #1 -
awp (a_store (a_ret (cloc_to_val x)) (a_bin_op PlusOp (a_load (a_ret (cloc_to_val x))) (a_load (a_ret (cloc_to_val x))))) True (λ _, x C[LLvl] #2).
Proof.
iIntros "[Hx Hx']".
iApply (a_store_spec _ _ (λ v, v = (cloc_to_val x)) (λ v, v = #2 x C #1) with "[] [Hx Hx']")%I.
{ iApply awp_ret. wp_value_head. eauto. }
- iApply (a_bin_op_spec _ _ (λ v, v = #1 x C{1 / 2} #1)
(λ v, v = #1 x C{1 / 2} #1)
with "[Hx] [Hx']")%I.
awp_load_ret x.
awp_load_ret x.
iNext. iIntros (? ?) "[% Hx] [% Hx']"; simplify_eq/=.
iExists _; eauto. repeat iSplit; eauto.
by iFrame.
- iNext. iIntros (? ? ->) "[% Hx]"; simplify_eq/=.