Commit b09f14ae authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Bump

parent c069c7ce
......@@ -9,7 +9,7 @@ synopsis: "Iris with time credits and time credits"
depends: [
"coq" { (>= "8.14" & < "8.15~") | (= "dev") }
"coq-iris" { (= "dev.2021-12-09.1.f52f9f6a") | (= "dev") }
"coq-iris" { (= "dev.2022-05-17.1.56e9d264") | (= "dev") }
"coq-tlc" { (= "20210316") }
]
......
......@@ -399,7 +399,7 @@ Lemma tac_wp_tick `{tctrHeapG Σ} Δ pe Δ1 Δ2 Δ3 Δ' i i' n max_tc s E K (v :
envs_entails Δ' (WP fill K v @ s; E {{ Φ }})
envs_entails Δ (WP fill K (App tick v) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=>??? HTC1 HTC2 HTRdup HTR HWP.
rewrite envs_entails_unseal=>??? HTC1 HTC2 HTRdup HTR HWP.
iIntros "HΔ".
iAssert (TCTR_invariant max_tc) as "#Hinv".
{ destruct pe.
......@@ -759,15 +759,14 @@ Section Soundness.
(* (1) adequate result: *)
- intros t2 σ2 v2 Hsteps.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
assert (σ2 !! = None)
by (simpl ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
pose (Build_TickCounter (fresh (dom σ2))) as Hloc.
assert (σ2 !! = None) by (simpl ; eapply not_elem_of_dom, is_fresh).
by eapply adequate_tctranslation__adequate_result.
(* (2) safety: *)
- intros t2 σ2 e2 _ Hsteps He2.
(* build a location ℓ which is fresh in e2 and in the domain of σ2: *)
pose (set1 := loc_set_of_expr e2 : gset loc).
pose (set2 := dom (gset loc) σ2 : gset loc).
pose (set2 := dom σ2 : gset loc).
pose (Build_TickCounter (fresh (set1 set2))) as Hloc.
eassert ( set1 set2) as [H1 H2] % not_elem_of_union
by (unfold ; apply is_fresh).
......@@ -780,9 +779,8 @@ Section Soundness.
(* (3) bounded time: *)
- intros t2 σ2 k.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
assert (σ2 !! = None)
by (unfold ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
pose (Build_TickCounter (fresh (dom σ2))) as Hloc.
assert (σ2 !! = None) by (unfold ; eapply not_elem_of_dom, is_fresh).
specialize (Hadq Hloc) as Hsafe % safe_adequate.
by eapply safe_tctranslation__bounded.
Qed.
......
......@@ -523,7 +523,7 @@ Proof.
(* (1) adequate result: *)
- intros n t2 σ2 v2 Hnsteps Inm.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Hloc := Build_TickCounter (fresh (dom (gset loc) σ2)) : TickCounter).
pose (Hloc := Build_TickCounter (fresh (dom σ2)) : TickCounter).
assert (σ2 !! = None)
by (simpl ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
by eapply adequate_translation__nadequate_result.
......@@ -531,7 +531,7 @@ Proof.
- intros n t2 σ2 e2 _ Hnsteps Inm He2.
(* build a location ℓ which is fresh in e2 and in the domain of σ2: *)
pose (set1 := loc_set_of_expr e2 : gset loc).
pose (set2 := dom (gset loc) σ2 : gset loc).
pose (set2 := dom σ2 : gset loc).
pose (Hloc := Build_TickCounter (fresh (set1 set2)) : TickCounter).
eassert ( set1 set2) as [H1 H2] % not_elem_of_union
by (unfold ; apply is_fresh).
......
......@@ -369,9 +369,8 @@ Section Soundness.
intros Hadq.
intros t2 σ2 k.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
assert (σ2 !! = None)
by (unfold ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
pose (Build_TickCounter (fresh (dom σ2))) as Hloc.
assert (σ2 !! = None) by (unfold ; eapply not_elem_of_dom, is_fresh).
specialize (Hadq Hloc) as Hsafe % safe_adequate.
by eapply safe_tctranslation__bounded.
Qed.
......@@ -513,7 +512,7 @@ Section Tactics.
envs_entails Δ'' (WP fill K v @ s; E {{ Φ }})
envs_entails Δ (WP fill K (App tick v) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq => HsubsetE ???? Hentails''.
rewrite envs_entails_unseal => HsubsetE ???? Hentails''.
rewrite envs_lookup_intuitionistic_sound // intuitionistically_elim. apply wand_elim_r'.
rewrite -wp_bind.
eapply wand_apply ; first by (iIntros "HTC1 HΦ #Htick" ; iApply (tick_spec with "Htick HTC1 HΦ")).
......
......@@ -170,15 +170,14 @@ Proof.
(* (1) adequate result: *)
- intros t2 σ2 v2 Hsteps.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
assert (σ2 !! = None)
by (simpl ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
pose (Build_TickCounter (fresh (dom σ2))) as Hloc.
assert (σ2 !! = None) by (simpl ; eapply not_elem_of_dom, is_fresh).
by eapply adequate_tctranslation__adequate_result.
(* (2) safety: *)
- intros t2 σ2 e2 _ Hsteps He2.
(* build a location ℓ which is fresh in e2 and in the domain of σ2: *)
pose (set1 := loc_set_of_expr e2 : gset loc).
pose (set2 := dom (gset loc) σ2 : gset loc).
pose (set2 := dom σ2 : gset loc).
pose (Build_TickCounter (fresh (set1 set2))) as Hloc.
eassert ( set1 set2) as [H1 H2] % not_elem_of_union
by (unfold ; apply is_fresh).
......@@ -294,9 +293,8 @@ Lemma spec_tctranslation__bounded' {Σ} m ψ e :
Proof.
intros Hspec HtcPreG σ t2 σ2 n Hnsteps.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
assert (σ2 !! = None)
by (unfold ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
pose (Build_TickCounter (fresh (dom σ2))) as Hloc.
assert (σ2 !! = None) by (unfold ; eapply not_elem_of_dom, is_fresh).
eapply simulation_exec_alt in Hnsteps ; auto.
assert (0 m-n)%Z by by eapply spec_tctranslation__bounded.
lia.
......
......@@ -380,7 +380,7 @@ Lemma tac_wp_tick `{timeReceiptHeapG Σ} Δ pe Δ1 Δ2 Δ' i max_tc s E K (v : v
envs_entails Δ' (WP fill K v @ s; E {{ Φ }})
envs_entails Δ (WP fill K (App tick v) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=>??? HTRdup HTR HWP.
rewrite envs_entails_unseal=>??? HTRdup HTR HWP.
iIntros "HΔ".
iAssert (TR_invariant max_tc) as "#Hinv".
{ destruct pe.
......
......@@ -604,7 +604,7 @@ Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
Proof. destruct Ki1, Ki2; intros; by simplify_eq. Qed.
Lemma alloc_fresh v σ :
let l := fresh (dom (gset loc) σ) in
let l := fresh (dom σ) in
head_step (Alloc $ Val v) σ [] (Val $ LitV $ LitLoc l) (<[l:=v]> σ) [].
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
......
......@@ -29,7 +29,7 @@ Lemma tac_wp_pure `{heapGS Σ} Δ Δ' s E K e1 e2 φ n Φ :
envs_entails Δ' (WP (fill K e2) @ s; E {{ Φ }})
envs_entails Δ (WP (fill K e1) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite envs_entails_unseal=> ??? HΔ'. rewrite into_laterN_env_sound /=.
(* We want [pure_exec_fill] to be available to TC search locally. *)
pose proof @pure_exec_fill.
rewrite HΔ' -lifting.wp_pure_step_later //.
......@@ -37,7 +37,7 @@ Qed.
Lemma tac_wp_value `{heapGS Σ} Δ s E Φ v :
envs_entails Δ (Φ v) envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
Proof. rewrite envs_entails_eq=> ->. by apply wp_value. Qed.
Proof. rewrite envs_entails_unseal=> ->. by apply wp_value. Qed.
Ltac wp_value_head :=
eapply tac_wp_value; reduction.pm_prettify.
......@@ -99,7 +99,7 @@ Lemma tac_wp_bind `{heapGS Σ} K Δ s E Φ e f :
f = (λ e, fill K e) (* as an eta expanded hypothesis so that we can `simpl` it *)
envs_entails Δ (WP e @ s; E {{ v, WP f (Val v) @ s; E {{ Φ }} }})%I
envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_bind. Qed.
Proof. rewrite envs_entails_unseal=> -> ->. by apply: wp_bind. Qed.
Ltac wp_bind_core K :=
lazymatch eval hnf in K with
......@@ -132,7 +132,7 @@ Lemma tac_wp_alloc Δ Δ' s E j K v Φ :
envs_entails Δ'' (WP fill K (Val $ LitV l) @ s; E {{ Φ }}))
envs_entails Δ (WP fill K (Alloc v) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ? HΔ.
rewrite envs_entails_unseal=> ? HΔ.
rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
......@@ -145,7 +145,7 @@ Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (Load (LitV l)) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ???.
rewrite envs_entails_unseal=> ???.
rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
......@@ -158,7 +158,7 @@ Lemma tac_wp_store Δ Δ' Δ'' s E i K l v v' Φ :
envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (Store (LitV l) (Val v')) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ????.
rewrite envs_entails_unseal=> ????.
rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
......@@ -173,7 +173,7 @@ Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v v1 v2 Φ :
(v v1 envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }}))
envs_entails Δ (WP fill K (CAS (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ???? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
rewrite envs_entails_unseal=> ???? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
- rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl.
apply later_mono, sep_mono_r. rewrite right_id. apply wand_mono; auto.
......@@ -190,7 +190,7 @@ Lemma tac_wp_cas_fail Δ Δ' s E i K l q v v1 v2 Φ :
envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ?????.
rewrite envs_entails_unseal=> ?????.
rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
......@@ -204,7 +204,7 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ :
envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ??????; subst.
rewrite envs_entails_unseal=> ??????; subst.
rewrite -wp_bind. eapply wand_apply.
{ eapply wp_cas_suc; eauto. by left. }
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
......@@ -218,7 +218,7 @@ Lemma tac_wp_faa Δ Δ' Δ'' s E i K l z1 z2 Φ :
envs_entails Δ'' (WP fill K (Val $ LitV z1) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ????.
rewrite envs_entails_unseal=> ????.
rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ _ z1 z2).
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
......
Supports Markdown
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