Commit 3eb3006a authored by Dan Frumin's avatar Dan Frumin

More opaquenes and some derived rules without heap-lang reductions

parent 3a40fb69
......@@ -256,6 +256,7 @@ Section a_wp_run.
End a_wp_run.
(* Make sure that we only use the provided rules and don't break the abstraction *)
Typeclasses Opaque a_ret a_bind (* a_run *) a_atomic a_atomic_env a_par.
Opaque a_ret a_bind (* a_run *) a_atomic a_atomic_env a_par.
(* Definition locking_heapΣ : gFunctors := *)
......
......@@ -237,7 +237,7 @@ Section proofs.
Lemma a_sequence_spec R Φ (f e : expr) :
AsVal f
awp e R (λ v, U (awp (f v) R Φ)) -
awp e R (λ v, U (awp (f v) R Φ)) -
awp (a_seq_bind f e) R Φ.
Proof.
iIntros ([fv <-]) "H". rewrite /a_seq_bind /=. awp_lam.
......@@ -247,9 +247,20 @@ Section proofs.
iModIntro. by awp_lam.
Qed.
Lemma a_sequence_spec' R Φ (e e' : expr) :
Closed [] e'
awp e R (λ v, U (awp e' R Φ)) -
awp (a_seq_bind (λ: <>, e') e)%E R Φ.
Proof.
iIntros (?) "He".
iApply a_sequence_spec.
iApply (awp_wand with "He"). iNext.
iIntros (?) "He'". iModIntro. by awp_lam.
Qed.
Lemma a_while_spec R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
awp (a_if c
(λ:<>, (#() ;; b) ;;;; a_while (λ:<>, c) (λ:<>, b))
(λ:<>, (λ:<>, b) #() ;;;; a_while (λ:<>, c) (λ:<>, b))
a_seq)%E R Φ -
awp (a_while (λ:<>, c) (λ:<>, b))%E R Φ.
Proof.
......@@ -271,6 +282,31 @@ Section proofs.
iIntros (v) "[[% H] | [% H]]"; simplify_eq; awp_lam; by awp_if.
Qed.
Lemma a_if_spec' R Φ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
awp e R (λ v, (v = #true awp e1 R Φ)
(v = #false awp e2 R Φ)) -
awp (a_if e (λ: <>, e1) (λ: <>, e2))%E R Φ.
Proof.
iIntros "He". iApply a_if_spec.
iApply (awp_wand with "He").
iIntros (v) "[[% Hv] | [% Hv]]"; subst; [iLeft|iRight]; iSplit; eauto; by awp_lam.
Qed.
Lemma a_while_spec' R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
awp c R (λ v, (v = #true
awp b R (λ _, U (awp (a_while (λ:<>, c) (λ:<>, b))%E R Φ)))
(v = #false awp (a_seq #()) R Φ)) -
awp (a_while (λ:<>, c) (λ:<>, b))%E R Φ.
Proof.
iIntros "H".
awp_lam. awp_lam. awp_seq.
iApply a_if_spec.
iApply (awp_wand with "H").
iIntros (v) "[[% Hv]|[% Hv]]"; subst; [iLeft|iRight]; iSplit; eauto.
awp_seq. iApply a_sequence_spec'. iNext.
awp_seq. done.
Qed.
Lemma a_invoke_spec (ef ea : expr) (R : iProp Σ) Ψ Φ (f : val) :
IntoVal ef f
awp ea R Ψ -
......@@ -283,7 +319,7 @@ Section proofs.
iIntros (a) "Ha". awp_let.
iApply a_sequence_spec.
iApply (awp_wand with "Ha"). clear a.
iIntros (a) "HΨ".
iNext. iIntros (a) "HΨ".
iSpecialize ("Hfa" with "HΨ").
iModIntro.
awp_let.
......@@ -313,7 +349,7 @@ Section proofs.
Lemma a_while_inv_spec I R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
I -
(I - awp c R (λ v, (v = #false U (Φ #()))
(v = #true (awp b R (λ _, U I))))%I) -
(v = #true (awp b R (λ _, U I))))%I) -
awp (a_while (λ:<>, c) (λ:<>, b))%E R Φ.
Proof.
iIntros "Hi #Hinv". iLöb as "IH".
......@@ -323,7 +359,7 @@ Section proofs.
iIntros (v) "[(% & H) | (% & H)] //="; subst.
- iRight. iSplit; by eauto; iApply a_seq_spec.
- iLeft. iSplit; first eauto. awp_seq.
iApply a_sequence_spec. awp_seq.
iApply a_sequence_spec. iNext. awp_seq.
iApply (awp_wand with "H").
iIntros (v) "Hi !>". awp_seq.
by iApply ("IH" with "Hi").
......@@ -331,4 +367,6 @@ Section proofs.
End proofs.
(* Make sure that we only use the provided rules and don't break the abstraction *)
Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke.
Typeclasses Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke.
Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke a_ret.
......@@ -46,9 +46,7 @@ Section factorial_spec.
(λ _, c C #n r C #(fact n))%I.
Proof.
iIntros "(Hk & Hc & Hr)". do 3 awp_lam.
iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_while_spec. iNext.
iDestruct "Hk" as %Hk.
iApply a_if_spec.
iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_while_spec'. iNext.
iApply (a_bin_op_spec _ _
(λ v, v = #k c C #k)%I (λ v, v = #n)%I with "[Hc]").
- awp_load_ret c.
......@@ -57,9 +55,9 @@ Section factorial_spec.
rewrite /bin_op_eval /=. iExists _; iSplit; eauto.
case_bool_decide.
+ iLeft. iSplit; eauto.
do 2 (awp_seq; iApply a_sequence_spec).
iApply a_sequence_spec'. iNext.
iApply (incr_spec with "[$Hc]").
iIntros "Hc". iModIntro. awp_seq.
iIntros "Hc". iModIntro.
iApply (a_store_ret with "[Hr Hc]").
iApply (a_bin_op_spec _ _
(λ v, v = #(fact k) r C #(fact k))%I
......@@ -72,12 +70,12 @@ Section factorial_spec.
{ rewrite Nat.add_1_r /fact. lia. }
iExists #(fact (k+1)); repeat (iSplit; eauto).
iExists #(fact k). iFrame. iIntros "Hr".
iModIntro. awp_seq.
iModIntro.
assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
iApply ("IH" $! n (k+1)%nat with "[] Hc Hr"). iPureIntro. lia.
+ iRight. iSplit; eauto.
iApply a_seq_spec. iModIntro.
assert (k = n) as -> by lia. by iFrame.
iApply a_seq_spec. iModIntro. iDestruct "Hk" as %Hk.
assert (k = n) as -> by lia. by iFrame.
Qed.
Lemma factorial_spec (n: nat) R :
......@@ -86,7 +84,7 @@ Section factorial_spec.
awp_lam.
iApply awp_bind. awp_alloc_ret r "Hr".
iApply awp_bind. awp_alloc_ret c "Hc".
iApply a_sequence_spec.
iApply a_sequence_spec. iNext.
iApply (awp_wand _ (λ _, c C #n r C #(fact n))%I with "[Hr Hc]").
- iApply ((factorial_body_spec n 0 c r) with "[$Hr $Hc]"); eauto with lia.
- iIntros (?) "[Hc Hr]". iModIntro. awp_seq.
......@@ -99,7 +97,7 @@ Section factorial_spec.
awp_lam.
iApply awp_bind. awp_alloc_ret r "Hr".
iApply awp_bind. awp_alloc_ret c "Hc".
iApply a_sequence_spec. do 3 awp_lam.
iApply a_sequence_spec'. iNext. do 3 awp_lam.
iApply (a_while_inv_spec
(k:nat, k n c C #k r C #(fact k))%I with "[Hr Hc]").
- iExists O. eauto with iFrame lia.
......@@ -111,8 +109,8 @@ Section factorial_spec.
+ iNext. iIntros (v1 v2) "[% Hc] %"; subst.
rewrite /bin_op_eval /=. iExists _; iSplit; eauto.
case_bool_decide.
* iRight. iSplit; eauto.
iApply a_sequence_spec.
* iRight. iSplit; eauto. iNext.
iApply a_sequence_spec. iNext.
iApply (incr_spec with "[$Hc]").
iIntros "Hc". iModIntro. awp_seq.
iApply (a_store_ret with "[Hr Hc]").
......@@ -129,7 +127,7 @@ Section factorial_spec.
iExists #(fact k). iFrame. iIntros "Hr". iModIntro.
assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
iExists (k+1)%nat. eauto with iFrame lia.
* iLeft. iSplit; eauto. do 2 iModIntro. awp_seq.
* iLeft. iSplit; eauto. do 2 iModIntro.
iRevert "H". iIntros "%". assert (k = n) as -> by lia.
by awp_load_ret r.
Qed.
......
......@@ -24,27 +24,27 @@ Section gcd_spec.
l C #a - r C #b -
awp (gcd #l #r) R (λ v, v = #(Z.gcd a b)).
Proof.
iIntros (??) "Hl Hr". do 2 awp_lam. iApply a_sequence_spec.
iIntros (??) "Hl Hr". do 2 awp_lam. 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]".
- 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_seq. awp_load_ret l. iIntros.
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.
iApply a_if_spec.
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. awp_seq.
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.
......@@ -53,11 +53,11 @@ Section gcd_spec.
+ 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.
iApply a_if_spec.
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. awp_seq.
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.
......
......@@ -113,7 +113,7 @@ Section in_place_reversal.
iIntros "Hlst". awp_lam.
iApply awp_bind; awp_alloc_ret i "Hi".
iApply awp_bind; awp_alloc_ret j "Hj".
iApply a_sequence_spec.
iApply a_sequence_spec'. iNext.
iApply (a_while_inv_spec ( ls rs rhd hd, i C hd is_list hd ls
j C rhd is_list rhd rs (reverse rs)++ls=xs)%I with "[Hlst Hj Hi]").
- iExists xs, [], (InjLV #()), hd; eauto with iFrame.
......@@ -125,24 +125,24 @@ Section in_place_reversal.
iNext. iIntros (? ?) "[-> Hi ] ->". destruct ls.
+ rewrite{1}/ is_list. iDestruct "Hls" as "->".
iExists #true; iSplit; first done. iExists #false; iSplit; first done.
iLeft; iSplit; first done. do 2 iModIntro. awp_seq. awp_load_ret j.
iLeft; iSplit; first done. do 2 iModIntro. awp_load_ret j.
iIntros "_". simplify_eq /=. by rewrite app_nil_r reverse_involutive.
+ iDestruct "Hls" as (l lnxt) "(-> & Hl & Hls)". fold is_list.
iExists #false; iSplit; first done; iExists #true; iSplit; first done.
iRight. iSplit; first done. iApply awp_bind.
iApply a_alloc_spec. iApply a_list_next_spec.
iNext. iApply a_alloc_spec. iApply a_list_next_spec.
awp_load_ret i. iIntros "Hi". iExists l, lnxt, v, ls.
iSplit; first done. iFrame. iIntros "Hl Hls".
iIntros (k) "Hk". awp_let. iApply a_sequence_spec.
iIntros (k) "Hk". awp_let. iApply a_sequence_spec'; iNext.
iApply (a_list_store_next_spec _ _
(λ z, z = (v, SOMEV #l) i C (SOMEV #l) )%I
(λ v, v = rhd j C rhd)%I with "[Hi Hl] [Hj]").
{ awp_load_ret i. eauto 42 with iFrame. }
{ awp_load_ret j. }
iIntros (? ? ?) "(% & Hi) (% & Hj)". simplify_eq.
iIntros "Hl". iModIntro. awp_seq. iApply a_sequence_spec.
iIntros "Hl". iModIntro. iApply a_sequence_spec'; iNext.
iApply (a_move_spec with "[$Hj $Hi Hls Hrs Hk Hl]").
iIntros "Hi Hj". iModIntro. awp_seq.
iIntros "Hi Hj". iModIntro.
iApply (a_move_spec with "[$Hi $Hk Hls Hrs Hj Hl]").
iIntros "Hk Hi". iModIntro. iExists ls, (v :: rs), (InjRV #l), lnxt.
iFrame. iSplit.
......
......@@ -92,7 +92,7 @@ Section test.
+ iNext. iIntros (? ? -> ->); done.
- iIntros (? ->). iModIntro.
unfold assignF. awp_lam. awp_proj. awp_lam. awp_proj. awp_lam.
iApply a_sequence_spec.
iApply a_sequence_spec. iNext.
iApply a_store_ret.
iApply awp_ret; wp_value_head.
iExists _; iFrame. iIntros "Hl".
......@@ -112,7 +112,7 @@ Section test.
- iIntros (? ->). iModIntro.
iIntros "[Hl HR]". iExists R%I. iFrame.
unfold assignF. awp_lam. awp_proj. awp_lam. awp_proj. awp_lam.
iApply a_sequence_spec.
iApply a_sequence_spec. iNext.
iApply a_store_ret.
iApply awp_ret; wp_value_head.
iDestruct "Hl" as (?) "Hl".
......
......@@ -39,21 +39,21 @@ Section factorial_spec.
(λ _, c C #n r C #(fact n))%I.
Proof.
iIntros "(Hk & Hc & Hr)". do 3 awp_lam.
iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_while_spec. iNext.
iDestruct "Hk" as %Hk. iApply a_if_spec.
vcg_solver. iIntros "Hr Hc".
iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_while_spec'. iNext.
vcg_solver. rewrite Qp_half_half. iIntros "Hr Hc".
case_bool_decide.
+ iLeft. iSplit; eauto. awp_lam. rewrite Qp_half_half.
iApply a_sequence_spec. awp_seq. iApply a_sequence_spec.
iApply (incr_spec with "[$Hc]"). iIntros "Hc".
iModIntro. awp_seq. vcg_solver. iIntros "Hc Hr".
+ iLeft. iSplit; eauto.
iApply a_sequence_spec'; iNext.
iApply (incr_spec with "Hc"). iIntros "Hc".
iModIntro. vcg_solver. iIntros "Hc Hr".
iModIntro.
assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
{ rewrite Nat.add_1_r /fact. lia. }
assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia. awp_seq.
assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
iApply ("IH" $! n (k+1)%nat with "[] Hc Hr"). iPureIntro. lia.
+ iRight. iSplit; eauto. iApply a_seq_spec. iModIntro.
assert (k = n) as -> by lia. rewrite Qp_half_half. by iFrame.
iDestruct "Hk" as %Hk.
assert (k = n) as -> by lia. by iFrame.
Qed.
Lemma factorial_spec (n: nat) R :
......@@ -62,10 +62,10 @@ Section factorial_spec.
awp_lam.
iApply awp_bind. awp_alloc_ret r "Hr".
iApply awp_bind. awp_alloc_ret c "Hc".
iApply a_sequence_spec.
iApply a_sequence_spec'. iNext.
iApply (awp_wand _ (λ _, c C #n r C #(fact n))%I with "[Hr Hc]").
- iApply ((factorial_body_spec n 0 c r) with "[$Hr $Hc]"); eauto with lia.
- iIntros (?) "[Hc Hr]". iModIntro. awp_seq.
- iIntros (?) "[Hc Hr]". iModIntro.
awp_load_ret r.
Qed.
......@@ -75,7 +75,7 @@ Section factorial_spec.
awp_lam.
iApply awp_bind. awp_alloc_ret r "Hr".
iApply awp_bind. awp_alloc_ret c "Hc".
iApply a_sequence_spec. do 3 awp_lam.
iApply a_sequence_spec'. iNext. do 3 awp_lam.
iApply (a_while_inv_spec
(k:nat, k n c C #k r C #(fact k))%I with "[Hr Hc]").
- iExists O. eauto with iFrame lia.
......@@ -83,16 +83,16 @@ Section factorial_spec.
vcg_solver. iIntros "Hr Hc".
case_bool_decide.
+ iRight. iSplit; eauto.
iApply a_sequence_spec. rewrite Qp_half_half.
iApply (incr_spec with "[$Hc]").
iIntros "Hc". iModIntro. awp_seq. vcg_solver.
iNext. iApply a_sequence_spec'. iNext. rewrite Qp_half_half.
iApply (incr_spec with "Hc").
iIntros "Hc". iModIntro. vcg_solver.
iIntros "Hc Hr". iModIntro.
assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
{ rewrite Nat.add_1_r /fact. lia. }
assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
iExists (k+1)%nat. eauto with iFrame lia.
+ iLeft. iSplit; eauto. do 2 iModIntro. awp_seq.
iRevert "H". iIntros "%". assert (k = n) as -> by lia.
by awp_load_ret r.
+ iLeft. iSplit; eauto. do 2 iModIntro.
iRevert "H". iIntros "%". assert (k = n) as -> by lia.
by awp_load_ret r.
Qed.
End factorial_spec.
......@@ -2,7 +2,7 @@ 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 notation.
From iris_c.lib Require Import locking_heap U.
Section tests_vcg.
......@@ -136,4 +136,16 @@ Section tests_vcg.
(a_store (a_ret #l) (a_ret #2)))%E True (λ v, True).
Proof. iIntros "Hl". vcg_solver. Abort.
Lemma test_while (l : loc) R :
l C #1 -
awp (a_while (λ: <>, ((a_bin_op LtOp) (∗ᶜ l)) 2)
(λ: <>, l = 1))%E R (λ _, True).
Proof.
iIntros "Hl".
iLöb as "IH".
iApply a_while_spec'. iNext.
vcg_solver. rewrite Qp_half_half. iIntros "Hl".
iLeft. iSplitR; eauto.
vcg_solver. iIntros "Hl". iModIntro. by iApply "IH".
Qed.
End tests_vcg.
......@@ -344,19 +344,15 @@ Section vcg_spec.
destruct (vcg_sp E _ de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
iPoseProof IHde1 as "Hawp1"; first done.
iPoseProof IHde2 as "Hawp2"; first done.
(* TODO: wtf? *)
assert (AsVal (λ: <>, dcexpr_interp E de2)).
{ exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
unfold popstack in Hsp.
destruct ms2 as [|t ms2'] eqn:Houteq; simplify_eq/=.
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
iClear "Hawp1 Hawp2".
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
iApply a_sequence_spec. iApply (awp_wand with "Hawp1").
iApply a_sequence_spec'. iNext. iApply (awp_wand with "Hawp1").
iIntros (?) "[% HmNew1]". simplify_eq/=. iClear "Hawp".
rewrite (denv_unlock_interp E mNew1).
iModIntro.
awp_seq. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
iModIntro. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
iApply (awp_wand with "Hawp2"). iIntros (?) "[% HmNew2]".
rewrite -denv_merge_interp. iSplit; eauto with iFrame.
Qed.
......@@ -682,12 +678,11 @@ Section vcg_spec.
eauto with iFrame.
- simpl in Hwf; apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
rewrite IHde1 //. iSpecialize ("Hm" with "Hwp"); fold vcg_wp.
iApply (a_sequence_spec with "[Hm]"); fold dcexpr_interp.
{ exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
iApply (awp_wand with "Hm"). iIntros (v) "Hex".
iApply (a_sequence_spec' with "[Hm]"); fold dcexpr_interp.
iNext. iApply (awp_wand with "Hm"). iIntros (v) "Hex".
iDestruct "Hex" as (Enew dv m' Hpre Hpre' Hm'wf) "(% & Hm & Hwp)". simpl.
rewrite denv_unlock_interp.
iModIntro. rewrite IHde2 //. awp_seq. iSpecialize ("Hm" with "Hwp").
iModIntro. rewrite IHde2 //. iSpecialize ("Hm" with "Hwp").
specialize (dcexpr_interp_mono E Enew de2 Hwf2 Hpre').
intro Heq; rewrite Heq. iApply (awp_wand with "Hm").
iIntros (v1) "Hex".
......
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