Commit a88548b5 authored by Dan Frumin's avatar Dan Frumin
Browse files

Fix a bunch of tests

parent e5406329
......@@ -7,32 +7,34 @@ From iris_c.c_translation Require Import proofmode translation.
Section derived.
Context `{amonadG Σ}.
Lemma a_load_ret (l: loc) (q : Qp) (w: val) R Φ:
l C{q} w (l C{q} w - Φ w) -
awp (a_load (a_ret (#l)%E)) R Φ.
Lemma a_load_ret (cl: cloc) (q : Qp) (w: val) R Φ:
cl C{q} w (cl C{q} w - Φ w) -
awp (a_load (a_ret (cloc_to_val cl)%E)) R Φ.
Proof.
iIntros "H". iApply a_load_spec.
iApply awp_ret. wp_value_head.
iExists l, w. by iFrame.
iExists cl, w. by iFrame.
Qed.
Lemma a_alloc_ret (e: expr) (ev: val) R Φ:
IntoVal e ev
( l: loc, l C ev - Φ #l) -
awp (a_alloc (a_ret e)) R Φ.
Lemma a_alloc_ret (n: nat) (e2: expr) (ev2: val) R Φ:
IntoVal e2 ev2
( l: loc, (l,O) C replicate n ev2 - Φ (cloc_to_val (l,O))) -
awp (a_alloc (a_ret #n) (a_ret e2)) R Φ.
Proof.
iIntros (?) "H". iApply a_alloc_spec.
iApply awp_ret. by iApply wp_value.
iIntros (?) "H". iApply (a_alloc_spec _ _ (λ v, v = #n)%I (λ v, v = ev2)%I).
- iApply awp_ret. by iApply wp_value.
- iApply awp_ret. by iApply wp_value.
- iNext. iIntros (? ? -> ->). iExists n; iSplit; eauto.
Qed.
Lemma a_store_ret (l:loc) (e: expr) `{Closed [] e} R Φ :
awp e R (λ w, v, l C v (l C[LLvl] w - Φ w)) -
awp (a_store (a_ret #l) e) R Φ.
Lemma a_store_ret (cl:cloc) (e: expr) `{Closed [] e} R Φ :
awp e R (λ w, v, cl C v (cl C[LLvl] w - Φ w)) -
awp (a_store (a_ret (cloc_to_val cl)) e) R Φ.
Proof.
iIntros "H".
iApply ((a_store_spec _ _
(λ l1, l1 = #l)%I
(λ w, v, (l C v (l C[LLvl] w - Φ w)))%I ) with "[] [$H] []").
(λ l1, l1 = cloc_to_val cl)%I
(λ w, v, (cl C v (cl C[LLvl] w - Φ w)))%I ) with "[] [$H] []").
- iApply awp_ret; iApply wp_value; eauto.
- iNext. iIntros (? w) "-> H".
iDestruct "H" as (v) "H".
......@@ -43,7 +45,7 @@ Section derived.
Ltac awp_ret_value := iApply awp_ret; iApply wp_value; eauto.
Ltac awp_alloc_ret r h := iApply a_alloc_ret; iIntros (r) h; awp_lam.
Lemma awp_bin_op_load_load op (l r : loc) (v1 v2: val) R Φ :
(*Lemma awp_bin_op_load_load op (l r : loc) (v1 v2: val) R Φ :
l ↦C v1 -∗ r ↦C v2 -∗
(l ↦C v1 -∗ r ↦C v2 -∗ ∃ w : val, ⌜bin_op_eval op v1 v2 = Some w⌝ ∧ Φ w) -∗
awp (a_bin_op op (a_load (a_ret #l)) (a_load (a_ret #r))) R Φ.
......@@ -65,7 +67,7 @@ Section derived.
iIntros "(Hs & Ht & H)".
iApply a_store_ret. awp_load_ret t. iIntros "Ht".
iExists v. iFrame. iSpecialize ("H" with "Ht"). done.
Qed.
Qed. *)
Lemma a_invoke_simpl (ef ea : expr) R Φ (f : val) :
IntoVal ef f
......
......@@ -7,9 +7,9 @@ From iris_c.c_translation Require Import proofmode translation derived.
Section test.
Context `{amonadG Σ}.
Lemma test1 (l : loc) :
Lemma test1 (l : cloc) :
l C[LLvl]{1/2} #1 - l C[LLvl]{1/2} #1 -
awp (a_seq #();; a_load (a_ret #l)) True (λ v, v = #1 l C #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.
......@@ -20,9 +20,9 @@ Section test.
awp_load_ret l.
Qed.
Lemma test2 (l r : loc) R :
Lemma test2 (l r : cloc) R :
l C #3 - r C #0 -
awp (a_store (a_ret #l) (a_ret #1);; a_seq #();; a_load (a_ret #l)) R (λ v, v = #1).
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.
......@@ -40,32 +40,34 @@ Section test.
(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 #0)).
(a_alloc (a_ret #1%nat) (a_ret #0)).
Lemma swap_spec (l1 l2 : loc) (v1 v2: val) R :
Lemma swap_spec (l1 l2 : cloc) (v1 v2: val) R :
l1 C v1 - l2 C v2 -
awp (swap #l1 #l2) R (λ _, l1 C v2 l2 C v1).
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".
iApply a_sequence_spec.
do 2 awp_lam. iApply awp_bind. iApply (a_alloc_ret 1 #0).
iIntros (r) "Hr". awp_lam.
iApply a_sequence_spec'.
iNext.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret l1. iIntros "Hl1". iExists #0. iFrame.
iIntros "Hr". iModIntro. awp_seq. iApply a_sequence_spec.
iApply (a_store_ret (r,0%nat) with "[Hl1 Hl2 Hr]").
awp_load_ret l1. iIntros "Hl1". iExists #0. iDestruct "Hr" as "[Hr _]". compute[cloc_add]. simpl. iFrame.
iIntros "Hr". iModIntro. iApply a_sequence_spec'.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
iNext. iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret l2. iIntros "Hl2". iExists v1. iFrame.
iIntros "Hl1". iModIntro. awp_seq. iApply awp_bind.
iIntros "Hl1". iModIntro. iApply awp_bind.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret r. iIntros "Hr". iExists v2. iFrame.
awp_load_ret (r,0%nat). iIntros "Hr". iExists v2. iFrame.
iIntros "Hl2". awp_seq. iApply a_seq_spec. iModIntro. by iFrame.
Qed.
Lemma test_invoke (l : loc) R :
Lemma test_invoke (l : cloc) R :
l C[LLvl] #1 -
awp (a_invoke (λ: "x", a_load (a_ret "x"))%E (a_ret #l)) R (λ v, v = #1 l C #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.
......@@ -83,12 +85,12 @@ Section test.
Lemma invoke_assignF_1 l (v v' : val) R :
l C v -
awp (a_invoke assignF (a_par (a_ret #l) (a_ret v'))) R
(λ w, l C v' w = 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 = #l)%I (λ v, v = v')%I).
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 (? ? -> ->) "!> !>".
......@@ -101,15 +103,14 @@ Section test.
iApply awp_ret; wp_value_head. eauto.
Qed.
Lemma invoke_assignF_2 (l : loc) (v' : val) R :
awp (a_invoke assignF (a_par (a_ret #l) (a_ret v')))
(( v, l C v) R)%I (λ w, w = v')%I.
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 = #l)%I (λ v, v = v')%I).
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 (? ? -> ->) "!> !>".
- iNext. iIntros (? ? -> ->) "!> !>".
iIntros "[Hl HR]".
unfold assignF. awp_lam. awp_proj. awp_lam. awp_proj. awp_lam.
iApply a_sequence_spec'. iNext.
......@@ -121,10 +122,10 @@ Section test.
iSplit; eauto with iFrame.
Qed.
Lemma invoke_test (l : loc) (z0 z1 z2: Z) R :
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
AWP (a_invoke assignF (l ||| z1))
+ (a_invoke assignF (l ||| z2)) @ R
{{ v, v = #(z1 + z2) ( w, l C w) }}.
Proof.
iIntros "Hl".
......@@ -136,12 +137,12 @@ Section test.
- iIntros (? ? -> ->). iExists #(z1+z2). iSplit; eauto.
Qed.
Lemma inc_test1 (l : loc) (z0 : Z) R:
Lemma inc_test1 (l : cloc) (z0 : Z) R:
l C #z0 -
AWP l += 1 @ R {{ v, v = #z0 l C[LLvl] #(z0+1) }}.
AWP l += 1 @ R {{ v, v = #z0 l C[LLvl] #(z0+1) }}.
Proof.
iIntros "Hl".
iApply (a_pre_bin_op_spec _ _ (λ v, v = #l)%I (λ v, v = #1)%I);
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.
......
......@@ -8,38 +8,38 @@ From iris_c.lib Require Import locking_heap U.
Section test.
Context `{amonadG Σ}.
Lemma test1 (l : loc) (v: val) :
l C v - awp (∗ᶜ l) True (λ w, w = v l C v).
Lemma test1 (l : cloc) (v: val) :
l C v - awp (∗ᶜ l) True (λ w, w = v l C v).
Proof.
iIntros "Hl1". vcg_solver. auto.
Qed.
(* double dereferencing *)
Lemma test2 (l1 l2 : loc) (v: val) :
l1 C #l2 - l2 C v -
awp ( ∗ᶜ ∗ᶜ l1) True (λ v, v = #1 l1 C #l2 - l2 C v).
Lemma test2 (l1 l2 : cloc) (v: val) :
l1 C cloc_to_val l2 - l2 C v -
awp ( ∗ᶜ ∗ᶜ l1) True (λ v, v = #1 l1 C cloc_to_val l2 - l2 C v).
Proof.
iIntros "Hl1 Hl2". vcg_solver. auto.
Qed.
Lemma test3 (l : loc) (v: val) :
l C v - awp (∗ᶜ l ; ∗ᶜ l) True (λ w, w = v l C v).
Lemma test3 (l : cloc) (v: val) :
l C v - awp (∗ᶜ l ; ∗ᶜ l) True (λ w, w = v l C v).
Proof.
iIntros "Hl1". vcg_solver. auto.
Qed.
Lemma test4 (l : loc) (v1 v2: val) :
l C v1 - awp ( l = a_ret v2) True (λ v, v = v2 l C[LLvl] v2).
Lemma test4 (l : cloc) (v1 v2: val) :
l C v1 - awp ( l = a_ret v2) True (λ v, v = v2 l C[LLvl] v2).
Proof.
iIntros "Hl1". vcg_solver. auto.
Qed.
(* double dereferencing & modification *)
Lemma test5 (l1 l2 r1 r2 : loc) (v1 v2: val) :
l1 C #l2 - l2 C v1 -
r1 C #r2 - r2 C v2 -
awp ( l1 = r1 ; ∗ᶜ ∗ᶜ l1 ) True
(λ w, w = v2 l1 C #r2 l2 C v1 r1 C #r2 - r2 C v2).
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 ) True
(λ 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. auto.
Qed.
......
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