Commit 51300b29 authored by Ike Mulder's avatar Ike Mulder
Browse files

Got 'various' file working, added TPSPEC.

parent c3eda252
Pipeline #66205 passed with stage
in 8 minutes and 48 seconds
......@@ -4,106 +4,9 @@ From reloc.logic Require Import model rules derived.
From diaframe.symb_exec Require Import defs weakestpre.
From diaframe Require Import util_classes tele_utils util_instances.
Import bi.
Section complementary_template.
Definition complementary_mod {PROP : bi} {A} (M : PROP PROP) : relation ((A PROP) PROP) :=
(λ M1 M2, P Q, M1 P M2 Q M $ a, P a Q a).
Definition template_M_inv {PROP : bi} n (M : PROP PROP) (TT1 TT2 : tele) Ps Ps': (TT1 * TT2 PROP) PROP
:= (λ P, .. (tt1 : TT1), (tele_app Ps tt1) - ^n (M $ .. (tt2 : TT2),
(tele_app (tele_app Ps' tt1) tt2) P (tt1, tt2)))%I.
Lemma templates_complementary {PROP : bi} n (M1 M2 M3 M: PROP PROP) (TT1 TT2 : tele) (Ps : TT1 -t> PROP) Ps' :
ModalityEC M1
ModalityEC M2
ModalityEC M3
( P, (M1 $ ^n (M2 $ M3 P)%I M P))
complementary_mod M (template_M n M1 M3 TT1 TT2 Ps Ps') (template_M_inv n M2 TT1 TT2 Ps Ps').
Proof.
rewrite /template_M_inv => HM1 HM2 HM3 HM P Q /=.
rewrite modality_ec_frame_l.
rewrite -HM.
apply HM1.
iIntros "[HL HR]".
iDestruct "HL" as (tt1) "[HPs HPs']".
iSpecialize ("HR" $! tt1 with "HPs").
iIntros "!>"; iStopProof.
rewrite modality_ec_frame_r.
apply HM2.
iIntros "[HR HPs']".
iDestruct "HR" as (tt2) "[HR HQ]".
iSpecialize ("HPs'" $! tt2 with "HR").
iStopProof.
rewrite modality_ec_frame_r.
apply HM3.
by eapply exist_intro'.
Qed.
Lemma complementary_shows_wand {PROP : bi} {A} (M M' : (A PROP) PROP) (modality : PROP PROP) :
complementary_mod modality M M' Q, M' Q P, M P - modality $ a, P a Q a.
Proof.
move => HMM' Q.
iIntros "HM" (P) "HMP".
iCombine "HMP HM" as "HM".
by rewrite HMM'.
Qed.
End complementary_template.
Section tpwp.
Context `{!relocG Σ}.
Definition tpwp_def j e E1 E2 Φ : iProp Σ := spec_ctx - j e ={E1, E2}= Φ.
Global Arguments tpwp_def j e E1 E2 Φ /.
Definition tpwp_aux : seal (@tpwp_def). Proof. by eexists. Qed.
Definition tpwp := tpwp_aux.(unseal).
Global Opaque tpwp.
Global Arguments tpwp : simpl never.
Lemma tpwp_eq : tpwp = tpwp_def.
Proof. by rewrite -tpwp_aux.(seal_eq). Qed.
Lemma from_tpwp j e E1 E2 Φ : (|={E1}=> tpwp j e E1 E2 Φ) spec_ctx - j e ={E1, E2}= Φ.
Proof. rewrite tpwp_eq /=. iIntros "H #HS Hj". iMod "H". by iApply "H". Qed.
Lemma refines_spec_ctx tl (tr : expr) E A :
(spec_ctx - (REL tl << tr @ E : A)) (REL tl << tr @ E : A).
Proof.
iIntros "Hrel".
rewrite {2}refines_eq /refines_def {1}/refines_right /=.
iIntros (j') "[#Hs Htr]".
iCombine "Hs Htr" as "Htr".
iRevert "Htr".
fold (refines_right j' tr).
change (refines_right j' tr) with
match inl tr : rhs_t with
| inl e => refines_right j' e
| inr k => j' = k%I
end.
set (tr' := inl tr).
iRevert (j').
fold (refines_def E tl tr' A). rewrite /tr'.
rewrite -refines_eq.
by iApply "Hrel".
Qed.
From diaframe.examples.external.reloc Require Export tp_steps.
Lemma from_tpwp_pre_rel j e tl (tr : expr) E A :
(|={E}=> tpwp j e E E (REL tl << tr @ E : A)) j e - REL tl << tr @ E : A%I.
Proof.
rewrite tpwp_eq /=.
iIntros "HjR Hj".
iApply refines_spec_ctx.
iIntros "#Hs".
iApply fupd_refines.
iMod "HjR".
by iApply "HjR".
Qed.
End tpwp.
Notation "'TPWP' e @ j ; E1 , E2 {{ Φ }}" := (tpwp j e E1 E2 Φ)
(at level 20, e, Φ at level 200) : bi_scope.
Import bi.
Section reloc_executor.
......@@ -117,10 +20,6 @@ Section reloc_executor.
Global Instance as_right_execute tl (tr : expr) E A : AsExecutionOf (REL tl << tr @ E : A) right_execute tr [tele_arg tl; E; A].
Proof. done. Qed.
Instance tp_reduction_condition : ReductionCondition (iPropI Σ) expr coPset :=
(λ A E e e' M, j K, spec_ctx j fill K e - P, M P ={E}= a, P a j fill K (e' a))%I.
Global Arguments tp_reduction_condition A E e e' M /.
Global Instance tp_reduction_condition_well_behaved_equiv A :
Proper ((=) ==> (=) ==>
(pointwise_relation _ (=)) ==>
......@@ -362,123 +261,6 @@ Section reloc_executor.
iMod ("HK" with "Hj"). rewrite -HK.
by iApply wp_bind_inv.
Qed.
Proposition tp_condition_execution_step_general {A B : tele} e1 E1 E2 P e2 Q pre:
( j K', spec_ctx j fill K' e1 -
.. (a : A), tele_app P a - (|={E2}=> .. (b : B), spec_ctx j fill K' (tele_app (tele_app e2 a) b) (tele_app (tele_app Q a) b)))
ReductionStep' tp_reduction_condition pre e1 0%nat (fupd E1 E2) (fupd E2 E1) A B P e2 Q E1.
Proof.
rewrite /ReductionStep' /ReductionTemplateStep => Hjk.
iIntros "_" (j K) "[#Hs Hj]".
erewrite <-complementary_shows_wand; last first.
- eapply (templates_complementary _ _ (fupd E2 E2)); [iSolveTC..| ].
intros R =>/=.
by erewrite !fupd_trans.
- rewrite /template_M_inv bi_tforall_forall; simpl.
iIntros (a) "HP".
iPoseProof (Hjk j K with "[$Hs $Hj] HP") as "HQ".
iMod "HQ" as (b) "[_ [Hj HQ]]".
iExists b.
by iFrame.
Qed.
Open Scope expr_scope.
Global Instance load_step_tp (l : loc) q E1 :
ReductionStep (tp_reduction_condition, E1) ! #l fupd E1 E1 v, l ↦ₛ{q} v nclose specN E1 ; empty_hyp_first =[^0]=> fupd E1 E1 v l ↦ₛ{q} v.
Proof.
apply: tp_condition_execution_step_general => //= j K.
iIntros "?" (v) "(? & %)".
rewrite -step_load => //.
iFrame.
Qed.
Global Instance store_step_tp (l : loc) e v' E1 :
IntoVal e v'
ReductionStep (tp_reduction_condition, E1) #l <- e fupd E1 E1 v, l ↦ₛ v nclose specN E1; empty_hyp_first =[^0]=> fupd E1 E1 #() l ↦ₛ v'.
Proof.
move => <- /=.
apply: tp_condition_execution_step_general => //= j K.
iIntros "?" (v) "(? & %)".
rewrite -step_store => //.
iFrame.
Qed.
Global Instance alloc_step_tp e v E1:
IntoVal e v
ReductionStep (tp_reduction_condition, E1) ref e fupd E1 E1 nclose specN E1 ; empty_hyp_first =[^0]=> l : loc, fupd E1 E1 #l l ↦ₛ v.
Proof.
move => <- /=.
apply: tp_condition_execution_step_general => //= j K.
apply wand_intro_r, wand_elim_r', pure_elim' => H.
apply wand_intro_r.
by rewrite left_id -step_alloc // left_id.
Qed.
Global Instance cmpxchg_step_tp e1 e2 v1 v2 E1 (l : loc) :
IntoVal e1 v1
IntoVal e2 v2
ReductionStep (tp_reduction_condition, E1) (CmpXchg #l e1 e2) fupd E1 E1 v, l ↦ₛ v vals_compare_safe v v1 nclose specN E1 ; empty_hyp_first =[^0]=>
b : bool, fupd E1 E1 (v, #b)%V b = true v = v1 l ↦ₛ v2 b = false v v1 l ↦ₛ v.
Proof.
move => <-<- /=.
apply: tp_condition_execution_step_general => //= j K.
apply bi.forall_intro => x.
apply bi.wand_intro_r.
rewrite !assoc.
apply bi.wand_elim_r', bi.pure_elim' => HNE.
apply bi.wand_intro_r.
rewrite left_id.
apply bi.wand_elim_r', bi.pure_elim' => Hvs.
apply bi.wand_intro_r.
rewrite left_id -assoc.
destruct (decide (v1 = x)).
- rewrite step_cmpxchg_suc => //.
apply fupd_mono.
rewrite -(exist_intro _).
apply sep_mono_r.
rewrite pure_True // left_id.
rewrite pure_True // left_id.
rewrite pure_False // left_absorb right_id.
iIntros "$".
- rewrite step_cmpxchg_fail => //.
apply fupd_mono.
rewrite -(exist_intro false).
apply sep_mono_r.
rewrite pure_False // left_absorb left_id.
rewrite pure_True // left_id.
rewrite pure_True // left_id //.
Qed.
Global Instance fork_step_tp e E1 :
ReductionStep (tp_reduction_condition, E1) Fork e fupd E1 E1 nclose specN E1 ; empty_hyp_first =[^0]=> i : nat, fupd E1 E1 #() i e.
Proof.
apply: tp_condition_execution_step_general => //= j K.
apply bi.wand_intro_r.
apply bi.wand_elim_r', bi.pure_elim' => HNE.
apply bi.wand_intro_r.
rewrite left_id step_fork //.
iIntros ">[%x ([#Hs Hj] & _ & Hx)]".
iExists _. by iFrame "# ∗".
Qed.
Lemma pure_step_tp φ n (e : expr) e' E1 E2 :
PureExec φ n e e'
ReductionStep (tp_reduction_condition, E1) e fupd E1 E2 ⌜φ nclose specN E2 ; empty_hyp_first =[^0]=> fupd E2 E1 e' emp.
Proof.
move => Hpure.
apply: tp_condition_execution_step_general => //= j K.
apply bi.wand_intro_r.
apply bi.wand_elim_r', bi.pure_elim' => [[HNE Hφ]].
apply bi.wand_intro_r.
rewrite left_id right_id -step_pure //.
Qed.
Global Instance pure_step_tp_inst φ n (e : expr) e' E :
PureExec φ n e e'
ReductionStep (tp_reduction_condition, E) e fupd E E ⌜φ nclose specN E ; empty_hyp_first =[^0]=> fupd E E e' emp.
Proof. exact: pure_step_tp. Qed.
End reloc_executor.
......
From reloc.lib Require Import lock counter.
From diaframe.examples.external.reloc Require Import reloc_automation_base class_instances_reloc_logatom.
From diaframe.examples.external.reloc Require Import reloc_automation_base class_instances_reloc_logatom tp_steps.
From diaframe.heap_lang Require Import atomic_instances_heaplang.
......@@ -18,6 +18,10 @@ End fg_spec.
Section counter_refinement.
Context `{!relocG Σ}.
Global Instance fg_increment_tp_spec (l : loc) E1 E2 :
TPSPEC E1, E2 (z : Z), {{ l ↦ₛ #z } } FG_increment #l {{ RET #z; l ↦ₛ #(z + 1) } }.
Proof. rewrite /FG_increment. iStepsS. Qed.
Lemma FG_CG_increment_refinement lk cnt cnt' :
inv counterN (counter_inv lk cnt cnt') -
REL FG_increment #cnt << CG_increment #cnt' lk : lrel_int.
......
......@@ -126,74 +126,52 @@ Section main.
Qed.
Section lock_n_stack_specs.
(* spin lock specs as tp executions, so that automation can apply them *)
(* spec notation only works for wp_red_cond, so this uses the more explicit reductionstep *)
Global Instance newlock_step_tp E1 :
ReductionStep (tp_reduction_condition, E1) reloc.lib.lock.newlock #() fupd E1 E1 nclose specN E1 ; empty_hyp_first =[^0]=>
l : loc, fupd E1 E1 #l l ↦ₛ #false.
(* spin lock specs as tp executions, so that automation can apply them *)
Global Instance tpspec_goal pre e E1 E2 TT1 TT2 P e' Q :
AsEmpValidWeak
(ReductionTPStep tp_reduction_condition pre e E1 E2 TT1 TT2 P e' Q E1)
(( j K, nclose specN E2 - .. a : TT1,
pre tele_app P a - TPWP (fill K e) @ j; E2 , E2 {{ (e'' : expr), j fill K e''
.. (b : TT2), e'' = tele_app (tele_app e' a) b tele_app (tele_app Q a) b }})) | 10.
Proof.
apply: tp_condition_execution_step_general => //= j K.
iStepS.
iStepS.
iRevert "H1 H2".
rewrite bi.intuitionistically_elim /reloc.lib.lock.newlock.
move => HjWP.
apply: tp_condition_execution_step_general => //= j K HE.
iIntros "[#Hs Hj]" (a) "HP".
iRevert "Hs Hj". rewrite bi.intuitionistically_elim.
iApply from_tpwp.
iPoseProof (HjWP $! j K with "[%//] HP") as "H".
rewrite tpwp_eq /tpwp_def. iStepsS.
iMod ("H" with "H4 H5") as (e'') "[Hj [%b [-> HQ]]]".
iExists b.
iStepsS.
Qed.
Global Instance acquirelock_step_tp (l : loc) E1:
ReductionStep (tp_reduction_condition, E1) reloc.lib.lock.acquire #l fupd E1 E1 l ↦ₛ #false nclose specN E1 ; empty_hyp_first =[^0]=>
fupd E1 E1 #() l ↦ₛ #true.
Proof.
apply: tp_condition_execution_step_general => //= j K.
iStepS.
iStepS.
iRevert "H1 H2".
rewrite bi.intuitionistically_elim /reloc.lib.lock.acquire.
iApply from_tpwp.
iStepsS.
Qed.
Global Instance newlock_step_tp E1 :
TPSPEC E1 {{ True } } reloc.lib.lock.newlock #() {{ (l : loc), RET #l; l ↦ₛ #false } }.
Proof. rewrite /newlock. iStepsS. Qed.
Global Instance releaselock_step_tp (l : loc) E1 b:
ReductionStep (tp_reduction_condition, E1) reloc.lib.lock.release #l fupd E1 E1 l ↦ₛ #b nclose specN E1 ; empty_hyp_first =[^0]=>
fupd E1 E1 #() l ↦ₛ #false.
Proof.
apply: tp_condition_execution_step_general => //= j K.
iStepS.
iStepS.
iRevert "H1 H2".
rewrite bi.intuitionistically_elim /reloc.lib.lock.release.
iApply from_tpwp.
iStepsS.
Qed.
Global Instance acquirelock_step_tp (l : loc) E1 E2 :
TPSPEC E1, E2 {{ l ↦ₛ # false } } acquire #l {{ RET #(); l ↦ₛ #true } }.
Proof. rewrite /acquire. iStepsS. Qed.
(* CG stack steps *)
Global Instance CG_push_step_tp (rs : val) tl (v : val) E1 :
ReductionStep (tp_reduction_condition, E1) CG_locked_push rs v fupd E1 E1 is_stack rs tl nclose specN E1 ; empty_hyp_first =[^0]=>
fupd E1 E1 #() is_stack rs (v :: tl).
Proof.
apply: tp_condition_execution_step_general => //= j K.
iStepS.
iStepS.
iRevert "H1 H2".
rewrite bi.intuitionistically_elim /CG_locked_push /CG_push.
iApply from_tpwp.
iStepsS.
Qed.
Global Instance releaselock_step_tp (l : loc) E1 E2 b:
TPSPEC E1, E2 {{ l ↦ₛ # b } } release #l {{ RET #(); l ↦ₛ #false } }.
Proof. rewrite /release. iStepsS. Qed.
Global Instance CG_pop_step_tp (rs : val) vs E1 :
ReductionStep (tp_reduction_condition, E1) CG_locked_pop rs fupd E1 E1 is_stack rs vs nclose specN E1 ; empty_hyp_first =[^0]=>
(v' : val), fupd E1 E1 v'
v' = NONEV vs = [] is_stack rs [] v tl, vs = v :: tl v' = SOMEV v is_stack rs tl.
Proof.
apply: tp_condition_execution_step_general => //= j K.
iStepS.
iStepS.
iRevert "H1 H2".
rewrite bi.intuitionistically_elim /CG_locked_pop /CG_pop /rec_unfold.
iApply from_tpwp.
destruct vs as [|v vs]; iSmash.
(* CG stack steps *)
Global Instance CG_push_step_tp (rs : val) (v : val) E1 E2 :
TPSPEC E1, E2 tl, {{ is_stack rs tl } } CG_locked_push rs v {{ RET #(); is_stack rs (v :: tl) } }.
Proof. rewrite /CG_locked_push /CG_push. iStepsS. Qed.
Global Instance CG_pop_step_tp (rs : val) E1 E2 :
TPSPEC E1, E2 vs, {{ is_stack rs vs } }
CG_locked_pop rs
{{ (v' : val), RET v';
v' = NONEV vs = [] is_stack rs []
v tl, vs = v :: tl v' = SOMEV v is_stack rs tl } }.
Proof.
rewrite /CG_locked_pop /CG_pop /rec_unfold.
iStepsS. destruct x1 as [|v vs]; iSmash.
Qed.
Obligation Tactic := program_verify.
......
......@@ -179,10 +179,10 @@ Section proof.
iApply (refines_pack (stackInt A)).
repeat iApply refines_pair.
- iStepsS. rel_rec_r. iStepsS.
- iStepsS. iStepR. do 2 iStepS.
- iStepsS. iStepR. do 3 iStepS.
iApply (FG_CG_pop_refinement with "H5").
solve_ndisj.
- iStepsS. iStepR. do 2 iStepS.
- iStepsS. iStepR. do 3 iStepS.
iApply (FG_CG_push_refinement with "H4 H5").
solve_ndisj.
Qed.
......
......@@ -27,7 +27,7 @@ Section symbol_refinement.
REL symbol1 << symbol2 : () lrel_symbol.
Proof.
do 36 iStepS. unfold symbol2.
do 36 iStepR.
do 47 iStepR.
iAssert (|={}=> γ γl,
inv sizeN (table_inv' γ x x2 x0 x3)
is_lock (relocN.@"lock1") γl #x1 (lok_inv x x2 x0 x3 #x4) )%I
......@@ -36,16 +36,12 @@ Section symbol_refinement.
iApply (refines_pack (tableR γ)).
repeat (iApply refines_pair).
- unfold eqKey; iStepsS.
- iStepsS. do 33 iStepR.
iRestore.
iStepsS. repeat iStepR.
iRestore.
- iStepsS. (* after store: run store on RHS. *) do 44 iStepR. iRestore.
iStepsS. (* after store CONS: run all on RHS *) repeat iStepR. iRestore.
iStepsS.
- iStepsS. repeat iStepR. rewrite bool_decide_true; last lia.
do 6 iStepR.
iRestore.
iStepsS. repeat iStepR.
iRestore.
- iStepsS. (* after load, do load on RHS. *) repeat iStepR. rewrite bool_decide_true; last lia.
do 8 iStepR. iRestore.
iStepsS. (* after 2nd load, do 2nd load on RHS. *) repeat iStepR. iRestore.
repeat iApply refines_app; [iApply nth_int_typed |iStepsS..].
Qed.
......@@ -53,7 +49,7 @@ Section symbol_refinement.
REL symbol2 << symbol1 : () lrel_symbol.
Proof.
do 36 iStepS. unfold symbol1.
do 36 iStepR.
do 47 iStepR.
iAssert (|={}=> γ γl,
inv sizeN (table_inv' γ x x2 x0 x3)
is_lock (relocN.@"lock1") γl #x1 (lok_inv x x2 x0 x3 #x4) )%I
......@@ -62,15 +58,13 @@ Section symbol_refinement.
iApply (refines_pack (tableR γ)).
repeat (iApply refines_pair).
- unfold eqKey; iStepsS.
- iStepsS. do 33 iStepR.
iRestore.
iStepsS. repeat iStepR.
iRestore.
- iStepsS. (* after store: run store on RHS. *) do 44 iStepR. iRestore.
iStepsS. (* after store CONS: run all on RHS *) repeat iStepR. iRestore.
iStepsS.
- iStepsS. rewrite bool_decide_true; last lia.
iStepsS. iRestore.
iStepsS. do 6 iStepR. iRestore.
iStepsS. repeat iStepR. iRestore.
iStepsS. (* first op: do nothing on RHS. *) iRestore.
iStepsS. (* this load: do load on RHS. *) do 8 iStepR. iRestore.
iStepsS. (* 2nd load: do 2nd load on RHS. *) repeat iStepR. iRestore.
repeat iApply refines_app; [iApply nth_int_typed |iStepsS..].
Qed.
End cell_refinement.
\ No newline at end of file
End symbol_refinement.
\ No newline at end of file
......@@ -10,10 +10,7 @@ Section tests.
l #3 -
r ↦ₛ #4 -
REL (!#l;;!#l+#1) << (!#r;;#0+!#r) : EqI.
Proof.
iIntros "Hl Hr".
iStepsS.
Qed.
Proof. iStepsS. Qed.
Lemma refines_pure_r E K' e e' t A n
(Hspec : nclose specN E) ϕ :
......@@ -23,10 +20,10 @@ Section tests.
Proof.
rewrite refines_eq /refines_def => Hpure Hϕ /=.
iIntros "Hlog". iIntros (j) "[#Hs Hj]".
iApply (class_instances_reloc.from_tpwp with "[Hlog]") => //.
iApply (tp_steps.from_tpwp with "[Hlog]") => //.
rewrite -fill_app.
iStepsS.
rewrite fill_app class_instances_reloc.tpwp_eq /=.
rewrite fill_app tp_steps.tpwp_eq /=.
iStepS.
iStepS.
iApply ("Hlog"). iStepsS.
......
......@@ -6,6 +6,7 @@ From diaframe.lib Require Import own_hints ticket_cmra.
From iris.algebra Require Export auth gset.
From reloc.lib Require Import lock counter.
From iris.heap_lang.lib Require Import ticket_lock.
(* A different `acquire` function to showcase the atomic rule for FG_increment *)
......
From iris.bi Require Import bi telescopes lib.laterable.
From reloc.logic.proofmode Require Import spec_tactics tactics.
From reloc.logic Require Import model rules derived.
From diaframe.symb_exec Require Import defs.
From diaframe Require Import proofmode_base.
Section tpwp.
Context `{!relocG Σ}.
Definition tpwp_def j e E1 E2 Φ : iProp Σ := spec_ctx - j e ={E1, E2}= Φ.
Global Arguments tpwp_def j e E1 E2 Φ /.
Definition tpwp_aux : seal (@tpwp_def). Proof. by eexists. Qed.
Definition tpwp := tpwp_aux.(unseal).
Global Opaque tpwp.
Global Arguments tpwp : simpl never.
Lemma tpwp_eq : tpwp = tpwp_def.
Proof. by rewrite -tpwp_aux.(seal_eq). Qed.
Lemma from_tpwp j e E1 E2 Φ : (|={E1}=> tpwp j e E1 E2 Φ) spec_ctx - j e ={E1, E2}= Φ.
Proof. rewrite tpwp_eq /=. iIntros "H #HS Hj". iMod "H". by iApply "H". Qed.
Lemma refines_spec_ctx tl (tr : expr) E A :
(spec_ctx - (REL tl << tr @ E : A)) (REL tl << tr @ E : A).
Proof.
iIntros "Hrel".
rewrite {2}refines_eq /refines_def {1}/refines_right /=.
iIntros (j') "[#Hs Htr]".
iCombine "Hs Htr" as "Htr".
iRevert "Htr".
fold (refines_right j' tr).
change (refines_right j' tr) with
match inl tr : rhs_t with
| inl e => refines_right j' e
| inr k => j' = k%I
end.
set (tr' := inl tr).
iRevert (j').
fold (refines_def E tl tr' A).