### wp_tick fro Combined.v

parent 0a8217ea
 ... @@ -200,28 +200,31 @@ Section Definitions. ... @@ -200,28 +200,31 @@ Section Definitions. ∗ own γ2 (●mnat (max_tc - m)) ∗ own γ2 (●mnat (max_tc - m)) )%I. )%I. Lemma zero_TC : Lemma zero_TC E: TCTR_invariant ={⊤}=∗ TC 0. ↑tctrN ⊆ E → TCTR_invariant ={E}=∗ TC 0. Proof using. Proof using. iIntros "#Htickinv". iIntros (?) "#Htickinv". iInv tctrN as (m) ">(? & ? & H● & ?)" "InvClose". iInv tctrN as (m) ">(? & ? & H● & ?)" "InvClose". iDestruct (own_auth_nat_null with "H●") as "[H● \$]". iDestruct (own_auth_nat_null with "H●") as "[H● \$]". iApply "InvClose" ; eauto with iFrame. iApply "InvClose" ; eauto with iFrame. Qed. Qed. Lemma zero_TR : Lemma zero_TR E: TCTR_invariant ={⊤}=∗ TR 0. ↑tctrN ⊆ E → TCTR_invariant ={E}=∗ TR 0. Proof using. Proof using. iIntros "#Htickinv". iIntros (?) "#Htickinv". iInv tctrN as (m) ">(? & ? & ? & Hγ1● & ?)" "InvClose". iInv tctrN as (m) ">(? & ? & ? & Hγ1● & ?)" "InvClose". iDestruct (own_auth_nat_null with "Hγ1●") as "[Hγ1● \$]". iDestruct (own_auth_nat_null with "Hγ1●") as "[Hγ1● \$]". iApply "InvClose" ; eauto with iFrame. iApply "InvClose" ; eauto with iFrame. Qed. Qed. Lemma zero_TRdup : Lemma zero_TRdup E : TCTR_invariant ={⊤}=∗ TRdup 0. ↑tctrN ⊆ E → TCTR_invariant ={E}=∗ TRdup 0. Proof using. Proof using. iIntros "#Htickinv". iIntros (?) "#Htickinv". iInv tctrN as (m) ">(? & ? & ? & ? & Hγ2●)" "InvClose". iInv tctrN as (m) ">(? & ? & ? & ? & Hγ2●)" "InvClose". iDestruct (own_auth_mnat_null with "Hγ2●") as "[Hγ2● \$]". iDestruct (own_auth_mnat_null with "Hγ2●") as "[Hγ2● \$]". iApply "InvClose" ; eauto with iFrame. iApply "InvClose" ; eauto with iFrame. ... @@ -363,55 +366,86 @@ Section Definitions. ... @@ -363,55 +366,86 @@ Section Definitions. End Definitions. End Definitions. (* (* * Proof-mode tactics for proving WP of translated expressions * Proof-mode tactics for proving WP of translated expressions *) *) (* TODO: a version of the tactics working with the abstract interface: *) Lemma tac_wp_tick `{tctrHeapG Σ} Δ pe Δ1 Δ2 Δ3 Δ' i i' n max_tc s E K (v : val) Φ : ↑tctrN ⊆ E → Section Tactics. MaybeIntoLaterNEnvs 1 Δ Δ1 → Context {Σ : gFunctors}. envs_lookup i Δ = Some (pe, TCTR_invariant max_tc) → Implicit Types Φ : val → iProp Σ. envs_lookup i' Δ1 = Some (false, TC (S n)) → Implicit Types Δ : envs (uPredI (iResUR Σ)). envs_simple_replace i' false (Esnoc Enil i' (TC n)) Δ1 = Some Δ2 → Lemma tac_wp_tick `{tctrHeapG Σ} Δ Δ1 Δ2 Δ3 Δ' i j1 j2 j3 max_tc m n p s E K (v : val) Φ : (∃ j pe' p, envs_lookup j Δ2 = Some (pe', TRdup p) ∧ ↑tctrN ⊆ E → envs_simple_replace j pe' (Esnoc Enil j (TRdup (S p))) Δ2 = Some Δ3) ∨ MaybeIntoLaterNEnvs 1 Δ Δ1 → Δ2 = Δ3 → envs_lookup i Δ = Some (true, TCTR_invariant max_tc) → envs_lookup j1 Δ1 = Some (false, TC (S m)) → (∃ j n, envs_lookup j Δ3 = Some (false, TR n) ∧ envs_lookup j3 Δ1 = Some (false, TR n) → envs_simple_replace j false (Esnoc Enil j (TR (S n))) Δ3 = Some Δ') ∨ envs_lookup j2 Δ1 = Some (false, TRdup p) → Δ3 = Δ' → envs_simple_replace j1 false (Esnoc Enil j1 (TC m)) Δ1 = Some Δ3 → envs_simple_replace j3 false (Esnoc Enil j3 (TR (S n))) Δ3 = Some Δ2 → envs_entails Δ' (WP fill K v @ s; E {{ Φ }}) → envs_simple_replace j2 false (Esnoc Enil j2 (TRdup (S p))) Δ2 = Some Δ' → envs_entails Δ (WP fill K (App tick v) @ s; E {{ Φ }}). envs_entails Δ' (WP fill K v @ s; E {{ Φ }}) → Proof. envs_entails Δ (WP fill K (App tick v) @ s; E {{ Φ }}). rewrite envs_entails_eq=>??? HTC1 HTC2 HTRdup HTR HWP. Admitted. iIntros "HΔ". iAssert (TCTR_invariant max_tc) as "#Hinv". End Tactics. { destruct pe. iDestruct (envs_lookup_sound _ i true with "HΔ") as "[? _]"=>//. Ltac wp_tick := iDestruct (envs_lookup_sound _ i false with "HΔ") as "[? _]"=>//. } iDestruct (into_laterN_env_sound with "HΔ") as "HΔ1"=>//. iDestruct (envs_simple_replace_singleton_sound with "HΔ1") as "[HTC HΔ2]"=>//=. iDestruct "HTC" as "[>HTC HTC']". iDestruct ("HΔ2" with "HTC'") as "HΔ2". iApply wp_bind. destruct HTR as [(j & n' & HTR1 & HTR2)| ->], HTRdup as [(j' & pe'' & p & HTRDup1 & HTRDup2)| ->]. - iDestruct (envs_simple_replace_singleton_sound with "HΔ2") as "[HTRdup HΔ3]"=>//. rewrite bi.intuitionistically_if_elim -bi.intuitionistically_intuitionistically_if. iDestruct "HTRdup" as "#>HTRdup". iApply (tick_spec with "[//] [\$HTC \$HTRdup]")=>//. iIntros "!> [HTR #HTRdup']". iApply HWP. rewrite Nat.add_comm. iSpecialize ("HΔ3" with "[//]"). iDestruct (envs_simple_replace_singleton_sound with "HΔ3") as "[HTR' HΔ']"=>//=. iCombine "HTR HTR'" as "HTR". iDestruct ("HΔ'" with "HTR") as "\$". - iMod (zero_TRdup with "Hinv") as "HTRdup"=>//. iApply (tick_spec with "[//] [\$HTC \$HTRdup]")=>//. iIntros "!> [HTR _]". iApply HWP. iDestruct (envs_simple_replace_singleton_sound with "HΔ2") as "[HTR' HΔ']"=>//=. iCombine "HTR HTR'" as "HTR". iDestruct ("HΔ'" with "HTR") as "\$". - iDestruct (envs_simple_replace_singleton_sound with "HΔ2") as "[HTRdup HΔ']"=>//. rewrite bi.intuitionistically_if_elim -bi.intuitionistically_intuitionistically_if. iDestruct "HTRdup" as "#>HTRdup". iApply (tick_spec with "[//] [\$HTC \$HTRdup]")=>//. iIntros "!> [_ #HTRdup']". iApply HWP. rewrite Nat.add_comm. iDestruct ("HΔ'" with "[//]") as "\$". - iMod (zero_TRdup with "Hinv") as "HTRdup"=>//. iApply (tick_spec with "[//] [\$HTC \$HTRdup]")=>//. iIntros "!> [_ #HTRdup']". by iApply HWP. Qed. Ltac wp_tick ::= iStartProof ; iStartProof ; lazymatch goal with lazymatch goal with | |- envs_entails _ (wp ?s ?E ?e ?Q) => | |- envs_entails _ (wp ?s ?E ?e ?Q) => first first [ reshape_expr false e ltac:(fun K e' => [ reshape_expr false e ltac:(fun K e' => eapply (tac_wp_tick _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ K) eapply (tac_wp_tick _ _ _ _ _ _ _ _ _ _ _ _ K) ) ) | fail 1 "wp_tick: cannot find 'tick ?v' in" e ] ; | fail 1 "wp_tick: cannot find 'tick ?v' in" e ] ; [ try solve_ndisj [ try solve_ndisj | exact _ | exact _ | (* lookup invariant: *) (iAssumptionCore || fail "wp_tick: cannot find TCTR_invariant") | (* lookup invariant: *) (iAssumptionCore || fail "wp_tick: cannot find TR_invariant") | (* lookup TC: *) (iAssumptionCore || fail "wp_tick: cannot find TC (S _)") | (* lookup TC *) (iAssumptionCore || fail "wp_tick: cannot find (TC (S _))") | (* lookup TRdup: *) (iAssumptionCore || fail "wp_tick: cannot find TRdup _") | (* replace TC *) proofmode.reduction.pm_reflexivity | (* lookup TR: *) (iAssumptionCore || fail "wp_tick: cannot find TR _") | (* lookup TRdup: *) ( | (* replace TC: *) proofmode.reduction.pm_reflexivity left; eexists _, _, _; split; | (* replace TRdup: *) proofmode.reduction.pm_reflexivity [iAssumptionCore | proofmode.reduction.pm_reflexivity] | (* replace TR: *) proofmode.reduction.pm_reflexivity || right; reflexivity) | (* lookup TR: *) ( left; eexists _, _; split; [iAssumptionCore | proofmode.reduction.pm_reflexivity] || right; reflexivity) | wp_expr_simpl ] | wp_expr_simpl ] | |- envs_entails _ (twp ?s ?E ?e ?Q) => | |- envs_entails _ (twp ?s ?E ?e ?Q) => fail "wp_tick is not implemented for twp" fail "wp_tick is not implemented for twp" ... @@ -428,26 +462,3 @@ Proof using. ... @@ -428,26 +462,3 @@ Proof using. iIntros "#Inv HTC HTRdup HTR". iIntros "#Inv HTC HTRdup HTR". wp_tick. wp_tick. Abort. Abort. Ltac wp_tick_rec := wp_tick ; first [ wp_rec | match goal with | |-context [ App ?f _ ] => unlock f ; wp_rec | |-context [ App (translation ?f) _ ] => unlock f ; wp_rec | |-context [ App (of_val (translationV ?f)) _ ] => unlock f ; wp_rec end | fail ]. Ltac wp_tick_lam := wp_tick_rec. Ltac wp_tick_let := wp_tick ; wp_let. Ltac wp_tick_seq := wp_tick ; wp_seq. Ltac wp_tick_op := wp_tick ; wp_op. Ltac wp_tick_if := wp_tick ; wp_if. Ltac wp_tick_match := wp_tick ; wp_match ; do 2 wp_lam ; wp_tick ; wp_lam. Ltac wp_tick_proj := wp_tick ; wp_proj. Ltac wp_tick_alloc loc := wp_tick ; wp_alloc loc. Ltac wp_tick_load := wp_tick ; wp_load. Ltac wp_tick_store := wp_tick ; wp_store. \ No newline at end of file
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