Commit f149a710 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Update wrt Iris dev.2018-10-13.0.7041c043

parent 1fe68c70
......@@ -4,8 +4,9 @@ Makefile.coq
*.aux
*.glob
*.vo
*.vio
.lia.cache
*.tar.gz
*.sw[po]
\#*.v#
_opam
\ No newline at end of file
_opam
......@@ -240,7 +240,7 @@ Lemma prgm_translation_spec `{!timeCreditHeapG Σ} (n : nat) :
Proof.
iIntros "#Htickinv !#" (Φ) "Htc Post".
unfold prgm.
change « sum_list (make_list (LitV n)) » with («sum_list» (tick «make_list #n»)).
change « sum_list (make_list (LitV n)) » with ((tick «sum_list») «make_list #n»).
rewrite !translation_of_val.
replace (6+15*n)%nat with ((3+5*n) + (3+10*n))%nat by lia ;
rewrite TC_plus ; iDestruct "Htc" as "[Htc_make Htc_sum]".
......@@ -256,7 +256,7 @@ Proof.
Qed.
Lemma prgm_timed_spec (n : nat) (σ : state) `{!timeCreditHeapPreG Σ} :
adequate NotStuck (prgm n) σ (λ v, v = #(n*(n+1)/2))
adequate NotStuck (prgm n) σ (λ v _, v = #(n*(n+1)/2))
bounded_time (prgm n) σ (6 + 15 * n)%nat.
Proof.
apply (spec_tctranslation__adequate_and_bounded' (Σ:=Σ)).
......@@ -264,4 +264,4 @@ Proof.
- rewrite !andb_True ; repeat split ; apply is_closed_of_val.
- intros HtcHeapG. apply prgm_translation_spec.
- assumption.
Qed.
\ No newline at end of file
Qed.
......@@ -440,8 +440,8 @@ Section ActiveItem.
Definition ectx_item_is_active (Ki : ectx_item) : bool :=
match Ki with
| AppRCtx _ | UnOpCtx _ | BinOpRCtx _ _ | IfCtx _ _ | FstCtx | SndCtx
| CaseCtx _ _ | AllocCtx | LoadCtx | StoreRCtx _ | CasRCtx _ _ | FaaRCtx _ => true
| AppLCtx _ | UnOpCtx _ | BinOpLCtx _ _ | IfCtx _ _ | FstCtx | SndCtx
| CaseCtx _ _ | AllocCtx | LoadCtx | StoreLCtx _ | CasLCtx _ _ | FaaLCtx _ => true
| _ => false
end.
......@@ -482,9 +482,9 @@ Section ActiveItem.
Proof.
induction e ;
try maximal_ectx_from_subterm IHe ;
try maximal_ectx_from_subterm IHe1 ;
try maximal_ectx_from_subterm IHe2 ;
try maximal_ectx_from_subterm IHe3 ;
try maximal_ectx_from_subterm IHe2 ;
try maximal_ectx_from_subterm IHe1 ;
maximal_ectx_empty.
Qed.
......@@ -605,7 +605,7 @@ End ActiveItem.
Section Safety.
Definition safe e σ : Prop :=
adequate NotStuck e σ (λ _, True).
adequate NotStuck e σ (λ _ _, True).
(*
Lemma safe_alt e σ :
......@@ -622,7 +622,7 @@ Section Safety.
Qed.
*)
Lemma safe_adequate e σ (φ : val Prop) :
Lemma safe_adequate e σ (φ : val state Prop) :
adequate NotStuck e σ φ
safe e σ.
Proof.
......
......@@ -71,11 +71,8 @@ Section Tick_exec.
tick v
)%E (<[ := #(S n)]> σ).
{
prim_step ; first exact _.
replace (rec: "tick" "x" := _)%E with (of_val tick) by by unlock tick.
unfold subst ; simpl ; fold subst.
rewrite ! subst_is_closed_nil // ; apply is_closed_of_val.
}
prim_step ; first exact _. simpl_subst. repeat f_equal.
unfold tick. by unlock. }
apply prim_exec_cons_nofork
with (
let: "k" := #(S n) in
......@@ -100,9 +97,7 @@ Section Tick_exec.
tick v
)%E (<[ := #(S n)]> σ).
{
prim_step ; first exact _.
unfold subst ; simpl ; fold subst.
rewrite ! subst_is_closed_nil // ; apply is_closed_of_val.
prim_step ; first exact _. by simpl_subst.
}
apply prim_exec_cons_nofork
with (
......@@ -129,8 +124,7 @@ Section Tick_exec.
apply prim_exec_cons_nofork
with (if: #true then v else tick v)%E (<[ := #(S n - 1)]> (<[ := #(S n)]> σ)).
{
prim_step.
apply lookup_insert.
prim_step; [apply lookup_insert|auto].
}
replace (S n - 1) with (Z.of_nat n) by lia.
rewrite insert_insert.
......@@ -144,7 +138,7 @@ Section Tick_exec.
Lemma exec_tick_case_branch e1 v2 σ :
is_closed [] e1
prim_exec (tick_case_branch (λ: <>, e1) v2)%E σ (e1 (tick v2)) σ [].
prim_exec (tick_case_branch (λ: <>, e1) v2)%E σ ((tick e1) v2) σ [].
Proof.
intros ; assert (Closed [] e1) by exact.
unfold tick_case_branch ; unlock.
......@@ -154,20 +148,15 @@ Section Tick_exec.
- rewrite /= decide_left //.
- exact _.
}
simpl_subst.
eapply prim_exec_cons_nofork.
{
prim_step ;
fold subst.
rewrite subst_is_closed_nil ; last apply is_closed_of_val.
exact _.
prim_step. exact _.
}
eapply prim_exec_cons_nofork, prim_exec_nil ; simpl.
simpl_subst.
eapply prim_exec_cons_nofork, prim_exec_nil.
{
unfold subst ; simpl ; fold subst.
rewrite subst_is_closed_nil ; last assumption.
rewrite subst_is_closed_nil ; last by apply is_closed_subst, is_closed_of_val.
rewrite subst_is_closed_nil ; last apply is_closed_of_val.
by prim_step.
prim_step.
}
Qed.
......@@ -251,7 +240,12 @@ Section SimulationLemma.
(* BetaS f x e1 e2 v2 e' σ : *)
- assert (Closed (f :b: x :b: []) « e1 ») by by apply is_closed_translation.
rewrite 2! translation_subst' translation_of_val.
tick_then_step_then_stop.
replace (rec: f x := « e1 »)%E with (of_val (rec: f x := « e1 »)%V)
by by unlock.
(* FIXME : tick_then_step_then_stop does not work here. *)
eapply prim_exec_transitive_nofork. exec_tick_success.
eapply prim_exec_cons_nofork, prim_exec_nil.
simpl. unlock. prim_step.
(* UnOpS op e v v' σ : *)
- tick_then_step_then_stop.
by apply un_op_eval_translation.
......@@ -301,10 +295,12 @@ Section SimulationLemma.
rewrite lookup_insert_ne ; last done.
by apply lookup_translationS_Some.
+ eauto using translationV_injective.
+ by apply vals_cas_compare_safe_translationV.
(* CasSucS l e1 v1 e2 v2 σ : *)
- tick_then_step_then_stop.
rewrite lookup_insert_ne ; last exact I.
by apply lookup_translationS_Some.
+ rewrite lookup_insert_ne ; last exact I.
by apply lookup_translationS_Some.
+ by apply vals_cas_compare_safe_translationV.
(* FaaS l i1 e2 i2 σ : *)
- tick_then_step_then_stop.
rewrite lookup_insert_ne ; last exact I.
......@@ -429,7 +425,7 @@ Section SimulationLemma.
| idtac
].
(* BetaS *)
- destruct v1 ; try discriminate E.
- destruct v ; try discriminate E.
eexhibit_prim_step.
(* UnOpS *)
- eexhibit_prim_step.
......@@ -465,10 +461,12 @@ Section SimulationLemma.
(* CasFailS *)
- apply lookup_translationS_Some_inv in Hbound_l as (? & ? & ->).
exhibit_prim_step (#false)%E.
intros ? % (f_equal translationV). contradiction.
+ intros ? % (f_equal translationV). contradiction.
+ by apply vals_cas_compare_safe_translationV_inv.
(* CasSucS *)
- apply lookup_translationS_Some_inv in Hbound_l as (? & ? & -> % translationV_injective).
exhibit_prim_step (#true)%E.
by apply vals_cas_compare_safe_translationV_inv.
(* FaaS *)
- apply lookup_translationS_Some_inv in Hbound_l as (? & ? & -> % eq_sym % translationV_lit_inv).
rewrite to_of_val in Hval_e2 ; injection Hval_e2 as -> % translationV_lit_inv.
......@@ -559,10 +557,12 @@ Section SimulationLemma.
(* assuming the adequacy of the translated expression,
* a proof that the original expression has m-adequate results. *)
(* FIXME : this is a weaker result than the adequacy result of Iris,
where the predicate can also speak about the final state. *)
Lemma adequate_translation__adequate_result m n φ e σ t2 σ2 v2 :
is_closed [] e
σ2 !! = None
adequate NotStuck «e» S«σ, m» (φ invtranslationV)
adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v))
nsteps step n ([e], σ) (of_val v2 :: t2, σ2)
(n m)%nat
φ v2.
......@@ -571,7 +571,7 @@ Section SimulationLemma.
assert (safe «e» S«σ, m») as Hsafe by by eapply safe_adequate.
replace (φ v2) with ((φ invtranslationV) (translationV v2))
by (simpl ; by rewrite invtranslationV_translationV).
eapply adequate_result ; first done.
eapply (adequate_result _ _ _ (λ v σ, φ (invtranslationV v))); first done.
change [«e»%E] with T«[e]».
replace (of_val «v2» :: _) with (T«of_val v2 :: t2») by by rewrite - translation_of_val.
eapply simulation_exec_success' ; eauto.
......@@ -583,7 +583,7 @@ End SimulationLemma. (* we close the section here as we now want to quantify ove
Lemma adequate_translation__adequate m φ e σ :
is_closed [] e
( {Hloc : TickCounter}, adequate NotStuck «e» S«σ, m» (φ invtranslationV))
( {Hloc : TickCounter}, adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v)))
nadequate NotStuck m e σ φ.
Proof.
intros Hclosed Hadq.
......
......@@ -23,15 +23,15 @@ Ltac reshape_expr_ordered b e tac :=
| false => tac K e
| true => fail
end
| App ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (AppRCtx v1 :: K) e2)
| App ?e1 ?e2 => go (AppLCtx e2 :: K) e1
| App ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (AppLCtx v2 :: K) e1)
| App ?e1 ?e2 => go (AppRCtx e1 :: K) e2
| UnOp ?op ?e => go (UnOpCtx op :: K) e
| BinOp ?op ?e1 ?e2 =>
reshape_val e1 ltac:(fun v1 => go (BinOpRCtx op v1 :: K) e2)
| BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
reshape_val e2 ltac:(fun v2 => go (BinOpLCtx op v2 :: K) e1)
| BinOp ?op ?e1 ?e2 => go (BinOpRCtx op e1 :: K) e2
| If ?e0 ?e1 ?e2 => go (IfCtx e1 e2 :: K) e0
| Pair ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (PairRCtx v1 :: K) e2)
| Pair ?e1 ?e2 => go (PairLCtx e2 :: K) e1
| Pair ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (PairLCtx v2 :: K) e1)
| Pair ?e1 ?e2 => go (PairRCtx e1 :: K) e2
| Fst ?e => go (FstCtx :: K) e
| Snd ?e => go (SndCtx :: K) e
| InjL ?e => go (InjLCtx :: K) e
......@@ -39,14 +39,14 @@ Ltac reshape_expr_ordered b e tac :=
| Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
| Alloc ?e => go (AllocCtx :: K) e
| Load ?e => go (LoadCtx :: K) e
| Store ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (StoreRCtx v1 :: K) e2)
| Store ?e1 ?e2 => go (StoreLCtx e2 :: K) e1
| CAS ?e0 ?e1 ?e2 => reshape_val e0 ltac:(fun v0 => first
[ reshape_val e1 ltac:(fun v1 => go (CasRCtx v0 v1 :: K) e2)
| go (CasMCtx v0 e2 :: K) e1 ])
| CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0
| FAA ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (FaaRCtx v1 :: K) e2)
| FAA ?e1 ?e2 => go (FaaLCtx e2 :: K) e1
| Store ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (StoreLCtx v2 :: K) e1)
| Store ?e1 ?e2 => go (StoreRCtx e1 :: K) e2
| CAS ?e0 ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => first
[ reshape_val e1 ltac:(fun v1 => go (CasLCtx v1 v2 :: K) e0)
| go (CasMCtx e0 v2 :: K) e1 ])
| CAS ?e0 ?e1 ?e2 => go (CasRCtx e0 e1 :: K) e2
| FAA ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (FaaLCtx v2 :: K) e1)
| FAA ?e1 ?e2 => go (FaaRCtx e1 :: K) e2
| _ =>
lazymatch b with
| false => fail
......@@ -59,7 +59,7 @@ Local Lemma head_step_into_val e σ e' v' σ' efs :
head_step e σ (of_val v') σ' efs
head_step e σ e' σ' efs.
Proof.
intros Hval Hstep. by erewrite of_to_val in Hstep.
intros Hval Hstep. by rewrite Hval in Hstep.
Qed.
Ltac prim_step :=
......@@ -67,7 +67,7 @@ Ltac prim_step :=
| |- prim_step ?e _ _ _ _ =>
reshape_expr_ordered true e ltac:(fun K e' =>
esplit with K e' _ ; [ reflexivity | reflexivity | ] ;
(idtac + eapply head_step_into_val) ; econstructor
(idtac + (eapply head_step_into_val; [apply _|])) ; econstructor
)
end ;
simpl_to_of_val.
\ No newline at end of file
simpl_to_of_val.
From iris.heap_lang Require Import proofmode notation adequacy.
From iris.heap_lang Require Import proofmode notation adequacy lang.
From iris.base_logic Require Import invariants.
From iris_time Require Import Auth_nat Misc Reduction Tactics.
......@@ -96,15 +96,14 @@ Section TickSpec.
Timeless (TC n).
Proof. exact _. Qed.
(* note: IntoAnd false will become IntoSep in a future version of Iris *)
Global Instance into_sep_TC_plus m n p : IntoAnd p (TC (m + n)) (TC m) (TC n).
Proof. rewrite /IntoAnd TC_plus ; iIntros "[Hm Hn]". destruct p ; iFrame. Qed.
Global Instance from_sep_TC_plus m n : FromAnd false (TC (m + n)) (TC m) (TC n).
Proof. by rewrite /FromAnd TC_plus. Qed.
Global Instance into_sep_TC_succ n p : IntoAnd p (TC (S n)) (TC 1) (TC n).
Proof. rewrite /IntoAnd TC_succ ; iIntros "[H1 Hn]". destruct p ; iFrame. Qed.
Global Instance from_sep_TC_succ n : FromAnd false (TC (S n)) (TC 1) (TC n).
Proof. by rewrite /FromAnd [TC (S n)] TC_succ. Qed.
Global Instance into_sep_TC_plus m n : IntoSep (TC (m + n)) (TC m) (TC n).
Proof. by rewrite /IntoSep TC_plus. Qed.
Global Instance from_sep_TC_plus m n : FromSep (TC (m + n)) (TC m) (TC n).
Proof. by rewrite /FromSep TC_plus. Qed.
Global Instance into_sep_TC_succ n : IntoSep (TC (S n)) (TC 1) (TC n).
Proof. by rewrite /IntoSep TC_succ. Qed.
Global Instance from_sep_TC_succ n : FromSep (TC (S n)) (TC 1) (TC n).
Proof. by rewrite /FromSep [TC (S n)] TC_succ. Qed.
Definition timeCreditN := nroot .@ "timeCredit".
......@@ -126,7 +125,7 @@ Section TickSpec.
TC_invariant -
{{{ TC 1 }}} tick e @ s ; E {{{ RET v ; True }}}.
Proof.
intros ? <- % of_to_val. iIntros "#Inv" (Ψ) "!# Hγ◯ HΨ".
intros ? <-. iIntros "#Inv" (Ψ) "!# Hγ◯ HΨ".
iLöb as "IH".
wp_lam.
(* open the invariant, in order to read the value n of location : *)
......@@ -350,6 +349,8 @@ Section Simulation.
try not_safe_tick.
(* BetaS f x e1 e2 v2 e' σ : *)
- assert (Closed (f :b: x :b: []) « e1 ») by by apply is_closed_translation.
replace (rec: f x := « e1 »)%E with (of_val (rec: f x := « e1 »)%V)
by by unlock.
not_safe_tick.
(* ForkS e σ : *)
- eapply not_safe_prim_step ; last prim_step.
......@@ -446,7 +447,7 @@ Section Soundness.
Lemma adequate_tctranslation__bounded m φ e σ :
is_closed [] e
( `{TickCounter}, adequate NotStuck «e» S«σ, m» (φ invtranslationV))
( `{TickCounter}, adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v)))
bounded_time e σ m.
Proof.
intros Hclosed Hadq.
......@@ -466,9 +467,9 @@ Section Soundness.
Lemma adequate_tctranslation__adequate_and_bounded m φ e σ :
is_closed [] e
( (k : nat), (k m)%nat
`{TickCounter}, adequate NotStuck «e» S«σ, k» (φ invtranslationV)
`{TickCounter}, adequate NotStuck «e» S«σ, k» (λ v σ, φ (invtranslationV v))
)
adequate NotStuck e σ φ bounded_time e σ m.
adequate NotStuck e σ (λ v σ, φ v) bounded_time e σ m.
Proof.
intros Hclosed Hadq.
assert (bounded_time e σ m) as Hbounded
......@@ -494,7 +495,7 @@ Section Soundness.
{{{ TC m }}} «e» {{{ v, RET v ; ⌜ψ v }}}
)
`{timeCreditHeapPreG Σ} `{TickCounter} σ,
(k : nat), (k m)%nat adequate NotStuck «e» S«σ,k» ψ.
(k : nat), (k m)%nat adequate NotStuck «e» S«σ,k» (λ v σ, ψ v).
Proof.
intros Hspec HpreG Hloc σ k Ik.
(* apply the adequacy results. *)
......@@ -541,7 +542,7 @@ Section Soundness.
{{{ TC m }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
)
{_ : timeCreditHeapPreG Σ} σ,
adequate NotStuck e σ φ bounded_time e σ m.
adequate NotStuck e σ (λ v σ, φ v) bounded_time e σ m.
Proof.
intros Hclosed Hspec HpreG σ.
apply adequate_tctranslation__adequate_and_bounded ; first done.
......@@ -557,7 +558,7 @@ Section Soundness.
{{{ TC m }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
)
{_ : timeCreditHeapPreG Σ} σ,
adequate NotStuck e σ φ bounded_time e σ m.
adequate NotStuck e σ (λ v σ, φ v) bounded_time e σ m.
Proof.
intros Hclosed Hspec HpreG σ.
eapply spec_tctranslation__adequate_and_bounded ; try done.
......@@ -576,7 +577,7 @@ Section Soundness.
{{{ TC m }}} «e» {{{ v, RET v ; ⌜φ v }}}
)
{_ : timeCreditHeapPreG Σ} σ,
adequate NotStuck e σ φ bounded_time e σ m.
adequate NotStuck e σ (λ v σ, φ v) bounded_time e σ m.
Proof.
intros Hφ Hclosed Hspec HpreG σ.
apply (spec_tctranslation__adequate_and_bounded (Σ:=Σ)) ; try assumption.
......@@ -600,7 +601,7 @@ Section Tactics.
Context {Σ : gFunctors}.
Implicit Types Φ : val iProp Σ.
Implicit Types Δ : envs (iResUR Σ).
Implicit Types Δ : envs (uPredI (iResUR Σ)).
(* concrete version: *)
Lemma tac_wp_tick `{timeCreditHeapG Σ} Δ Δ' Δ'' s E i j n K e v Φ :
......@@ -613,8 +614,8 @@ Section Tactics.
envs_entails Δ'' (WP fill K v @ s; E {{ Φ }})
envs_entails Δ (WP fill K (App tick e) @ s; E {{ Φ }}).
Proof.
unfold envs_entails => HsubsetE ????? Hentails''.
rewrite envs_lookup_persistent_sound // persistently_elim. apply wand_elim_r'.
rewrite envs_entails_eq => HsubsetE ????? Hentails''.
rewrite envs_lookup_persistent_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Φ")).
rewrite into_laterN_env_sound -later_sep /=. apply later_mono.
......@@ -657,7 +658,7 @@ Ltac wp_tick :=
| exact _
| solve_TICKCTXT ()
| solve_TC ()
| env_cbv ; reflexivity
| proofmode.reduction.pm_reflexivity
| finish () ]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
fail "wp_tick is not implemented for twp"
......@@ -685,4 +686,4 @@ Ltac wp_tick_match := wp_tick ; wp_match ; do 2 wp_lam ; wp_tick.
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
Ltac wp_tick_store := wp_tick ; wp_store.
From iris.heap_lang Require Import proofmode notation adequacy.
From iris.heap_lang Require Import proofmode notation adequacy lang.
From iris.base_logic Require Import invariants.
From iris_time Require Import Auth_nat Reduction TimeCredits.
......@@ -140,7 +140,7 @@ Qed.
Lemma adequate_tctranslation__adequate_result {Hloc : TickCounter} m φ e σ t2 σ2 v2 :
is_closed [] e
σ2 !! = None
adequate NotStuck «e» S«σ, m» (φ invtranslationV)
adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v))
rtc step ([e], σ) (of_val v2 :: t2, σ2)
φ v2.
Proof.
......@@ -149,7 +149,7 @@ Proof.
assert (n m)%nat by by eapply safe_tctranslation__bounded.
replace (φ v2) with ((φ invtranslationV) (translationV v2))
by (simpl ; by rewrite invtranslationV_translationV).
eapply adequate_result ; first done.
eapply (adequate_result _ _ _ (λ v σ, φ (invtranslationV v))) ; first done.
change [«e»%E] with T«[e]».
replace (of_val «v2» :: _) with (T«of_val v2 :: t2») by by rewrite - translation_of_val.
eapply simulation_exec_success' ; eauto.
......@@ -159,8 +159,8 @@ Qed.
Lemma adequate_tctranslation__adequate m φ e σ :
is_closed [] e
( `{TickCounter}, adequate NotStuck «e» S«σ, m» (φ invtranslationV))
adequate NotStuck e σ φ.
( `{TickCounter}, adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v)))
adequate NotStuck e σ (λ v σ, φ v).
Proof.
intros Hclosed Hadq.
split.
......
From iris.heap_lang Require Import proofmode notation adequacy.
From iris.heap_lang Require Import proofmode notation adequacy lang.
From iris.base_logic Require Import invariants.
From iris_time Require Import Auth_nat Auth_mnat Misc Reduction Tactics.
......@@ -109,15 +109,14 @@ Section TockSpec.
Timeless (TR n).
Proof. exact _. Qed.
(* note: IntoAnd false will become IntoSep in a future version of Iris *)
Global Instance into_sep_TR_plus m n p : IntoAnd p (TR (m + n)) (TR m) (TR n).
Proof. rewrite /IntoAnd TR_plus ; iIntros "[Hm Hn]". destruct p ; iFrame. Qed.
Global Instance from_sep_TR_plus m n : FromAnd false (TR (m + n)) (TR m) (TR n).
Proof. by rewrite /FromAnd TR_plus. Qed.
Global Instance into_sep_TR_succ n p : IntoAnd p (TR (S n)) (TR 1) (TR n).
Proof. rewrite /IntoAnd TR_succ ; iIntros "[H1 Hn]". destruct p ; iFrame. Qed.
Global Instance from_sep_TR_succ n : FromAnd false (TR (S n)) (TR 1) (TR n).
Proof. by rewrite /FromAnd [TR (S n)] TR_succ. Qed.
Global Instance into_sep_TR_plus m n : IntoSep (TR (m + n)) (TR m) (TR n).
Proof. by rewrite /IntoSep TR_plus. Qed.
Global Instance from_sep_TR_plus m n : FromSep (TR (m + n)) (TR m) (TR n).
Proof. by rewrite /FromSep TR_plus. Qed.
Global Instance into_sep_TR_succ n : IntoSep (TR (S n)) (TR 1) (TR n).
Proof. by rewrite /IntoSep TR_succ. Qed.
Global Instance from_sep_TR_succ n : FromSep (TR (S n)) (TR 1) (TR n).
Proof. by rewrite /FromSep [TR (S n)] TR_succ. Qed.
Lemma TRdup_max m n :
TRdup (m `max` n) (TRdup m TRdup n)%I.
......@@ -134,11 +133,10 @@ Section TockSpec.
Persistent (TRdup n).
Proof. exact _. Qed.
(* note: IntoAnd false will become IntoSep in a future version of Iris *)
Global Instance into_sep_TRdup_max m n p : IntoAnd p (TRdup (m `max` n)) (TRdup m) (TRdup n).
Proof. rewrite /IntoAnd TRdup_max ; iIntros "[Hm Hn]". destruct p ; iFrame. Qed.
Global Instance from_sep_TRdup_max m n : FromAnd false (TRdup (m `max` n)) (TRdup m) (TRdup n).
Proof. by rewrite /FromAnd TRdup_max. Qed.
Global Instance into_sep_TRdup_max m n : IntoSep (TRdup (m `max` n)) (TRdup m) (TRdup n).
Proof. by rewrite /IntoSep TRdup_max. Qed.
Global Instance from_sep_TRdup_max m n : FromSep (TRdup (m `max` n)) (TRdup m) (TRdup n).
Proof. by rewrite /FromSep TRdup_max. Qed.
Definition timeReceiptN := nroot .@ "timeReceipt".
......@@ -230,7 +228,7 @@ Section TockSpec.
TR_invariant -
{{{ TRdup m }}} tock e @ s ; E {{{ RET v ; TR 1 TRdup (m+1) }}}.
Proof.
intros ? <- % of_to_val. iIntros "#Inv" (Ψ) "!# Hγ2◯ HΨ".
intros ? <-. iIntros "#Inv" (Ψ) "!# Hγ2◯ HΨ".
iLöb as "IH".
wp_lam.
(* open the invariant, in order to read the value k = nmaxn1 of location : *)
......@@ -317,7 +315,8 @@ Section Soundness.
TR_invariant nmax -
{{{ True }}} «e» {{{ v, RET v ; ⌜ψ v }}}
)
`{timeReceiptHeapPreG Σ} `{TickCounter} σ, adequate NotStuck «e» S«σ,nmax-1» ψ.
`{timeReceiptHeapPreG Σ} `{TickCounter} σ,
adequate NotStuck «e» S«σ,nmax-1» (λ v σ, ψ v).
Proof.
intros Inmax Hspec HpreG Hloc σ.
(* apply the adequacy results. *)
......@@ -404,4 +403,4 @@ Section Tactics.
End Tactics.
Ltac wp_tock :=
idtac.
\ No newline at end of file
idtac.
......@@ -38,21 +38,21 @@ Section Translation.
* This ad-hoc semantics calls for an ad-hoc definition of the translation in
* that case because, to observe the simulation lemma, the translation of
* [Case (InjL v) e1 e2] must reduce to the translation of [e1 v], which is
* [«e1» (tick «e2»)]. To do so --which means preserving the weird evaluation
* [(tick «e1») «v»]. To do so --which means preserving the weird evaluation
* order--, we use the helper term below: *)
Definition tick_case_branch : val :=
(λ: "f" "x", "f" #() (tick "x"))%V.
(λ: "f" "x", tick ("f" #()) "x")%V.
Fixpoint translation (e : expr) : expr :=
match e with
(* Base lambda calculus *)
| Var _ => e
| Rec f x e => Rec f x (translation e)
| App e1 e2 => (translation e1) (tick $ translation e2)
| App e1 e2 => (tick $ translation e1) (translation e2)
(* Base types and their operations *)
| Lit _ => e
| UnOp op e => UnOp op (tick $ translation e)
| BinOp op e1 e2 => BinOp op (translation e1) (tick $ translation e2)
| BinOp op e1 e2 => BinOp op (tick $ translation e1) (translation e2)
| If e0 e1 e2 => If (tick $ translation e0) (translation e1) (translation e2)
(* Products *)
| Pair e1 e2 => Pair (translation e1) (translation e2)
......@@ -70,9 +70,9 @@ Section Translation.
(* Heap *)
| Alloc e => Alloc (tick $ translation e)
| Load e => Load (tick $ translation e)
| Store e1 e2 => Store (translation e1) (tick $ translation e2)
| CAS e0 e1 e2 => CAS (translation e0) (translation e1) (tick $ translation e2)
| FAA e1 e2 => FAA (translation e1) (tick $ translation e2)
| Store e1 e2 => Store (tick $ translation e1) (translation e2)
| CAS e0 e1 e2 => CAS (tick $ translation e0) (translation e1) (translation e2)
| FAA e1 e2 => FAA (tick $ translation e1) (translation e2)
end %E.
Lemma is_closed_translation xs e :
......@@ -99,14 +99,14 @@ Section Translation.
Definition translationKi (Ki : ectx_item) : ectx_item :=
match Ki with
| AppLCtx e2 => AppLCtx (tick $ translation e2)
| AppRCtx v1 => AppRCtx (translationV v1)
| AppLCtx v2 => AppLCtx (translationV v2)
| AppRCtx e1 => AppRCtx (tick $ translation e1)
| UnOpCtx op => UnOpCtx op
| BinOpLCtx op e2 => BinOpLCtx op (tick $ translation e2)
| BinOpRCtx op v1 => BinOpRCtx op (translationV v1)
| BinOpLCtx op v2 => BinOpLCtx op (translationV v2)
| BinOpRCtx op e1 => BinOpRCtx op (tick $ translation e1)
| IfCtx e1 e2 => IfCtx (translation e1) (translation e2)
| PairLCtx e2 => PairLCtx (translation e2)
| PairRCtx v1 => PairRCtx (translationV v1)
| PairLCtx v2 => PairLCtx (translationV v2)
| PairRCtx e1 => PairRCtx (translation e1)
| FstCtx => FstCtx
| SndCtx => SndCtx
| InjLCtx => InjLCtx
......@@ -117,13 +117,13 @@ Section Translation.
(tick_case_branch (λ: <>, translation e2))%E
| AllocCtx => AllocCtx
| LoadCtx => LoadCtx
| StoreLCtx e2 => StoreLCtx (tick $ translation e2)
| StoreRCtx v1 => StoreRCtx (translationV v1)
| CasLCtx e1 e2 => CasLCtx (translation e1) (tick $ translation e2)
| CasMCtx v0 e2 => CasMCtx (translationV v0) (tick $ translation e2)
| CasRCtx v0 v1 => CasRCtx (translationV v0) (translationV v1)
| FaaLCtx e2 => FaaLCtx (tick $ translation e2)
| FaaRCtx v1 => FaaRCtx (translationV v1)
| StoreLCtx v2 => StoreLCtx (translationV v2)
| StoreRCtx e1 => StoreRCtx (tick $ translation e1)
| CasLCtx v0 v1 => CasLCtx (translationV v0) (translationV v1)
| CasMCtx e1 v1 => CasMCtx (tick $ translation e1) (translationV v1)
| CasRCtx e1 e2 => CasRCtx (tick $ translation e1) (translation e2)
| FaaLCtx v2 => FaaLCtx (translationV v2)
| FaaRCtx e1 => FaaRCtx (tick $ translation e1)
end.
Definition translationKi_aux (Ki : ectx_item) : ectx _ :=
......@@ -184,7 +184,7 @@ Section Translation.
v, e = of_val v.
Proof.
revert e.
induction v' as
induction v' as
[ (* RecV *) f' x' e1' Hclosed_e1'
| (* LitV *) lit'
| (* PairV *) v1' IH1 v2' IH2
......@@ -192,9 +192,9 @@ Section Translation.
| (* InjRV *) v1' IH1
] ;
intros
[
[
| (* Rec *) f x e1
|
|
| (* Lit *) lit
| | |
| (* Pair *) e1 e2
......@@ -258,8 +258,13 @@ Section Translation.
(* eliminating all spurious cases, since e2 must have the same head
constructor as e1: *)
try discriminate 1 ; injection 1 ;
(* all subgoals are straightforward by applying the induction hypotheses: *)
intros ; f_equal ; auto.
(* most of the subgoals are straightforward by applying the induction hypotheses: *)
intros ; f_equal ; auto;
(* one last trick is needed for Fork *)
match goal with
| H : translation ?e = Fork (translation _) |- _ => by destruct e
| H : Fork (translation _) = translation ?e |- _ => by destruct e
end.
Qed.
Lemma translationV_injective v1 v2 :
......@@ -275,7 +280,7 @@ Section Translation.
Lemma translation_fill_item Ki e :
translation (fill_item Ki e) = fill (translationKi_aux Ki) (translation e).
Proof.
destruct Ki ; rewrite /= ? translation_of_val ; reflexivity.
destruct Ki ; try (rewrite /= ? translation_of_val ; reflexivity).
Qed.
Lemma translation_fill_item_active (ki : ectx_item) v :
......@@ -389,8 +394,8 @@ Section Translation.
intros H.
destruct op ; try (
destruct v1, v2 ; try discriminate H ;
simpl ; case_match ; try discriminate H ;
simpl ; case_match ; try discriminate H ;
unfold bin_op_eval in * ;
do 3 try (case_match ; try discriminate H) ;
by injection H as <-
).
(* Remaining case: op = EqOp *)
......@@ -442,6 +447,23 @@ Section Translation.
by intros ? % of_val_inj % translationV_lit_inv.
Qed.
Lemma vals_cas_compare_safe_translationV v1 v2 :
vals_cas_compare_safe v1 v2
vals_cas_compare_safe (translationV v1) (translationV v2).
Proof.
intros [].