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

Copy-paste and customize heap_lang in this repo.

Side effects : use a specific Val constructor for values (many simplifications), native machine integers.
parent ab4583c1
......@@ -103,7 +103,7 @@ Important modules are highlighted.
#### Generic translation and “tick”
The basic properties of the translation are proven in `Translation.v` (for
example, `translation_subst` and `translation_of_val`).
example, `translation_subst`).
In `Simulation.v`:
......
-Q theories iris_time
-arg -w -arg -notation-overridden
-arg -w -arg -notation-overridden,-redundant-canonical-projection
theories/heap_lang/lang.v
theories/heap_lang/adequacy.v
theories/heap_lang/lifting.v
theories/heap_lang/notation.v
theories/heap_lang/proofmode.v
theories/heap_lang/tactics.v
theories/heap_lang/lib/assert.v
theories/Auth_mnat.v
theories/Auth_nat.v
theories/MachineIntegers.v
theories/ClockIntegers.v
theories/Examples.v
theories/Misc.v
......
From iris.heap_lang Require Import proofmode notation.
From iris_time Require Import TimeReceipts MachineIntegers.
From iris_time.heap_lang Require Import proofmode notation.
From iris_time Require Import TimeReceipts.
From stdpp Require Import numbers.
Open Scope Z_scope.
......@@ -13,28 +13,32 @@ Section clock_int.
Context `{timeReceiptHeapG Σ}.
Context (nmax : nat).
Context `(nmax max_int).
Context `(nmax max_mach_int).
Definition is_clock_int (n : nat) : iProp Σ :=
TR n.
Definition is_clock_int (n : Z) : iProp Σ :=
(0 n TR (Z.to_nat n))%I.
(* Clock integers support addition, which consumes its arguments: *)
Lemma clock_int_add_spec n1 n2 :
Lemma clock_int_add_spec (n1 n2 : mach_int) :
TR_invariant nmax -
{{{ is_clock_int n1 is_clock_int n2 }}}
machine_int_add #n1 #n2
{{{ RET #(n1+n2) ; is_clock_int (n1+n2) }}}.
{{{ is_clock_int (`n1) is_clock_int (`n2) }}}
#n1 + #n2
{{{ H, RET #(LitMachInt ((`n1+`n2) H)) ; is_clock_int (`n1+`n2) }}}.
Proof.
iIntros "#Htrinv" (Φ) "!# (H1 & H2) Post".
iAssert (TR (n1+n2)) with "[H1 H2]" as "H" ; first by (rewrite TR_plus ; iFrame).
iDestruct (TR_lt_nmax with "Htrinv H") as ">(H & %)" ; first done.
wp_apply (machine_int_add_spec n1 n2 with "[] [H Post]") .
{
iPureIntro. unfold min_int in *. lia.
}
{
iNext ; iIntros "%". iApply "Post". iFrame "H".
}
iIntros "#Htrinv" (Φ) "!# ([% H1] & [% H2]) Post".
iAssert (TR (Z.to_nat (`n1+`n2))) with "[H1 H2]" as "H".
{ rewrite Z2Nat.inj_add // TR_plus. iFrame. }
iDestruct (TR_lt_nmax with "Htrinv H") as ">(H & Hnmax)" ; [done|].
iDestruct "Hnmax" as %Hnmax.
assert (`n1 + `n2 < max_mach_int).
{ rewrite -(Nat2Z.id nmax) in Hnmax. apply Z2Nat.inj_lt in Hnmax; lia. }
assert (bool_decide (mach_int_bounded (`n1 + `n2))).
{ apply bool_decide_pack. split; [|done].
(* FIXME : why isn't lia able to do this directly? *)
trans 0. unfold min_mach_int; lia. lia. }
wp_op.
{ by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left. }
iApply "Post". iIntros "{$H} /= !%". lia.
Qed.
End clock_int.
......@@ -48,54 +52,62 @@ Section snapclock_int.
Context `{timeReceiptHeapG Σ}.
Context (nmax : nat).
Context `(nmax max_int).
Context `(nmax max_mach_int).
Definition is_snapclock_int (n : nat) : iProp Σ :=
TRdup n.
Definition is_snapclock_int (n : Z) : iProp Σ :=
(0 n TRdup (Z.to_nat n))%I.
(* Snapclock integers are persistent (in particular they are duplicable): *)
Lemma snapclock_int_persistent (n : nat) :
Lemma snapclock_int_persistent (n : Z) :
Persistent (is_snapclock_int n).
Proof. exact _. Qed.
(* Snapclock integers support incrementation: *)
Lemma snapclock_int_incr_spec n1 :
Lemma snapclock_int_incr_spec (n1 : mach_int) :
TR_invariant nmax -
{{{ is_snapclock_int n1 }}}
tick #() ;; machine_int_add #n1 #1
{{{ RET #(n1+1) ; is_snapclock_int (n1+1) }}}.
{{{ is_snapclock_int (`n1) }}}
tick #() ;; #n1 + #mach_int_1
{{{ H, RET #(LitMachInt ((`n1+1) H)) ; is_snapclock_int (`n1+1) }}}.
Proof.
iIntros "#Htrinv" (Φ) "!# H1 Post".
iIntros "#Htrinv" (Φ) "!# [% H1] Post".
wp_apply (tick_spec_simple nmax #() with "Htrinv H1"). iIntros "(_ & H)".
iDestruct (TRdup_lt_nmax with "Htrinv H") as ">(H & %)" ; first done.
wp_seq.
wp_apply (machine_int_add_spec n1 1 with "[] [H Post]") .
{
iPureIntro. unfold min_int in *. lia.
}
{
iNext ; iIntros "%". iApply "Post". iFrame "H".
}
iDestruct (TRdup_lt_nmax with "Htrinv H") as ">(H & Hnmax)" ; first done.
iDestruct "Hnmax" as %Hnmax. wp_seq.
assert (`n1 + 1 < max_mach_int).
{ rewrite -(Nat2Z.id nmax) (_:1%nat = Z.to_nat 1) // -Z2Nat.inj_add // in Hnmax.
apply Z2Nat.inj_lt in Hnmax; lia. }
assert (bool_decide (mach_int_bounded (`n1 + 1))).
{ apply bool_decide_pack. split; [|done].
(* FIXME : why isn't lia able to do this directly? *)
trans 0. unfold min_mach_int; lia. lia. }
wp_op.
{ by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left. }
iApply "Post". iSplit. auto with lia.
by rewrite Z2Nat.inj_add //.
Qed.
(* Snapclock integers also support a limited form of addition: *)
Lemma snapclock_int_add_spec n1 n2 m :
Lemma snapclock_int_add_spec (n1 n2 : mach_int) (m : Z) :
TR_invariant nmax -
{{{ is_snapclock_int n1 is_snapclock_int n2
is_snapclock_int m n1+n2 m }}}
machine_int_add #n1 #n2
{{{ RET #(n1+n2) ; is_snapclock_int (n1+n2) }}}.
{{{ is_snapclock_int (`n1) is_snapclock_int (`n2)
is_snapclock_int m `n1+`n2 m }}}
#n1 + #n2
{{{ H, RET #(LitMachInt ((`n1+`n2) H)) ; is_snapclock_int (`n1+`n2) }}}.
Proof.
iIntros "#Htrinv" (Φ) "!# (_ & _ & Hm & %) Post".
iDestruct (TRdup_lt_nmax with "Htrinv Hm") as ">(Hm & %)" ; first done.
iDestruct (TRdup_weaken m (n1 + n2) with "Hm") as "H" ; first lia.
wp_apply (machine_int_add_spec n1 n2 with "[] [H Post]") .
{
iPureIntro. unfold min_int in *. lia.
}
{
iNext ; iIntros "%". iApply "Post". iFrame "H".
}
iIntros "#Htrinv" (Φ) "!# ([% _] & [% _] & [% Hm] & %) Post".
iDestruct (TRdup_lt_nmax with "Htrinv Hm") as ">(Hm & Hnmax)" ; first done.
iDestruct "Hnmax" as %Hnmax.
assert (m < max_mach_int).
{ rewrite -(Nat2Z.id nmax) in Hnmax. apply Z2Nat.inj_lt in Hnmax; lia. }
iDestruct (TRdup_weaken (Z.to_nat m) (Z.to_nat (`n1 + `n2)) with "Hm") as "H".
{ apply Z2Nat.inj_le; lia. }
assert (bool_decide (mach_int_bounded (`n1 + `n2))).
{ apply bool_decide_pack. split; [|lia].
(* FIXME : why isn't lia able to do this directly? *)
trans 0. unfold min_mach_int; lia. lia. }
wp_op.
{ by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left. }
iApply "Post". iSplit; [|done]. auto with lia.
Qed.
End snapclock_int.
(* code taken from the Iris tutorial *)
From iris.heap_lang Require Import proofmode notation.
From iris_time.heap_lang Require Import proofmode notation.
From iris.program_logic Require Import adequacy.
From iris_time Require Import TimeCredits Reduction.
......@@ -120,27 +120,23 @@ Proof.
Qed.
Lemma sum_list_translation_spec `{!timeCreditHeapG Σ} (l : list Z) (v : val) :
TC_invariant -
{{{ is_list_tr l v TC (3 + 10 * length l) }}} « sum_list v » {{{ RET #(sum_list_coq l) ; is_list_tr l v }}}.
{{{ is_list_tr l v TC (4 + 13 * length l) }}} « sum_list v » {{{ RET #(sum_list_coq l) ; is_list_tr l v }}}.
Proof.
iIntros "#Htickinv !#" (Φ) "[Hl Htc] Post".
iInduction l as [|x l] "IH" forall (v Φ).
- simpl.
rewrite !translation_of_val.
iDestruct "Hl" as %->.
wp_tick_rec. wp_tick_match.
by iApply "Post".
- replace (3 + 10 * length (x :: l))%nat with (13 + 10 * length l)%nat by (simpl ; lia).
simpl.
rewrite !translation_of_val. setoid_rewrite translation_of_val.
- replace (4 + 13 * length (x :: l))%nat with (17 + 13 * length l)%nat by (simpl ; lia).
iDestruct "Hl" as (p) "[-> Hl]" ; iDestruct "Hl" as (v) "[Hp Hl]".
wp_tick_rec.
wp_tick_match.
wp_tick_rec. wp_tick_match.
wp_tick_load. wp_tick_proj. wp_tick_let.
wp_tick_load. wp_tick_proj. wp_tick_let.
iDestruct "Htc" as "[Htc1 Htc]".
wp_apply ("IH" with "Hl Htc"). iIntros "Hl".
wp_tick_op.
iApply "Post". eauto with iFrame.
iApply "Post". simpl. eauto with iFrame.
Qed.
Definition make_list : val :=
......@@ -162,37 +158,33 @@ Lemma make_list_spec `{!heapG Σ} (n : nat) :
Proof.
iIntros (Φ) "_ Post".
iInduction n as [|n'] "IH" forall (Φ) ; simpl.
- wp_rec. wp_op. wp_if.
- wp_rec. wp_op. wp_if. wp_inj.
by iApply "Post".
- wp_rec. wp_op. wp_if.
wp_op.
assert (Z.of_nat n' = Z.of_nat (S n') - 1) as Eq by lia ; simpl in Eq ; destruct Eq.
wp_apply "IH". iIntros (v') "Hl".
change (Z.pos $ Pos.of_succ_nat n') with (Z.of_nat $ S n').
wp_alloc p.
wp_alloc p. wp_inj.
iApply "Post". eauto with iFrame.
Qed.
Lemma make_list_translation_spec `{!timeCreditHeapG Σ} (n : nat) :
TC_invariant -
{{{ TC (3+5*n) }}} «make_list #n» {{{ v', RET v' ; is_list (make_list_coq n) v' }}}.
{{{ TC (4+7*n) }}} «make_list #n» {{{ v', RET v' ; is_list (make_list_coq n) v' }}}.
Proof.
iIntros "#Htickinv !#" (Φ) "Htc Post".
iInduction n as [|n'] "IH" forall (Φ).
- simpl.
rewrite !translation_of_val.
wp_tick_rec. wp_tick_op. wp_tick_if.
- wp_tick_rec. wp_tick_op. wp_tick_if. wp_tick_inj.
by iApply "Post".
- replace (3 + 5 * S n')%nat with (8 + 5 * n')%nat by lia.
simpl.
rewrite !translation_of_val.
- replace (4 + 7 * S n')%nat with (11 + 7 * n')%nat by lia.
wp_tick_rec. wp_tick_op. wp_tick_if.
wp_tick_op.
assert (Z.of_nat n' = Z.of_nat (S n') - 1) as Eq by lia ; simpl in Eq ; destruct Eq.
iDestruct "Htc" as "[Htc1 Htc]".
iDestruct "Htc" as "[? [? [? Htc]]]".
wp_apply ("IH" with "Htc"). iIntros (v') "Hl".
change (Z.pos $ Pos.of_succ_nat n') with (Z.of_nat $ S n').
wp_tick_alloc p.
iApply "Post". eauto with iFrame.
wp_tick_pair. wp_tick_alloc p. wp_tick_inj.
iApply "Post". simpl. eauto with iFrame.
Qed.
Definition prgm (n : nat) : expr :=
......@@ -236,18 +228,14 @@ Proof.
Qed.
Lemma prgm_translation_spec `{!timeCreditHeapG Σ} (n : nat) :
TC_invariant -
{{{ TC (6+15*n) }}} «prgm n» {{{ v, RET v ; v = #(n*(n+1)/2) }}}.
{{{ TC (8+20*n) }}} «prgm n» {{{ v, RET v ; v = #(n*(n+1)/2) }}}.
Proof.
iIntros "#Htickinv !#" (Φ) "Htc Post".
unfold prgm.
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 ;
replace (8+20*n)%nat with ((4+7*n) + (4+13*n))%nat by lia ;
rewrite TC_plus ; iDestruct "Htc" as "[Htc_make Htc_sum]".
unfold prgm. simpl_trans.
wp_apply (make_list_translation_spec with "Htickinv Htc_make"). iIntros (v) "Hl".
iDestruct (is_list_translation with "Hl") as "[Hl ->]".
rewrite - !translation_of_val.
change (« sum_list » (tick « v »)) with « sum_list v ».
wp_apply (sum_list_translation_spec with "Htickinv [Hl Htc_sum]"). {
rewrite - is_list_tr_is_list_translation.
erewrite length_make_list_coq. iFrame.
......@@ -257,11 +245,10 @@ Qed.
Lemma prgm_timed_spec (n : nat) (σ : state) `{!timeCreditHeapPreG Σ} :
adequate NotStuck (prgm n) σ (λ v _, v = #(n*(n+1)/2))
bounded_time (prgm n) σ (6 + 15 * n)%nat.
bounded_time (prgm n) σ (8 + 20 * n)%nat.
Proof.
apply (spec_tctranslation__adequate_and_bounded' (Σ:=Σ)).
- by intros _ ->.
- rewrite !andb_True ; repeat split ; apply is_closed_of_val.
- intros HtcHeapG. apply prgm_translation_spec.
- assumption.
Qed.
From iris.heap_lang Require Import proofmode notation.
Open Scope Z_scope.
Definition w : nat := 64.
Definition max_int : Z := 1 (w-1).
Definition min_int : Z := - max_int.
Definition max_uint : Z := 2 * max_int.
(*
* Bare machine integers can overflow.
*)
Section machine_int.
Context `{heapG Σ}.
Definition is_machine_int (n : Z) : iProp Σ :=
min_int n < max_int%I.
Definition machine_int_add : val :=
λ: "x" "y",
("x" + "y" + #max_int) `rem` #max_uint - #max_int.
(* Machine addition does not overflow when some inequality is met: *)
Lemma machine_int_add_spec n1 n2 :
{{{ is_machine_int n1 is_machine_int n2 min_int n1+n2 < max_int }}}
machine_int_add #n1 #n2
{{{ RET #(n1+n2) ; is_machine_int (n1+n2) }}}.
Proof.
iIntros (Φ) "(_ & _ & %) Post". repeat (wp_pure _).
(* boring arithmetic proof: *)
assert ((n1 + n2 + max_int) `rem` max_uint - max_int = n1 + n2) as ->. {
assert ((n1 + n2 + max_int) `rem` max_uint = n1 + n2 + max_int). {
apply Z.rem_small. unfold min_int, max_uint in *. lia.
}
lia.
}
by iApply "Post".
Qed.
End machine_int.
This diff is collapsed.
This diff is collapsed.
From iris.heap_lang Require Export lang tactics.
(*
* Tactics for reducing terms
*)
Ltac simpl_to_of_val :=
rewrite /= ? to_of_val //.
Ltac rewrite_into_values :=
repeat (lazymatch goal with
| H : to_val _ = Some _ |- _ =>
eapply of_to_val in H as <-
end).
Ltac reshape_expr_ordered b e tac :=
let rec go K e :=
match e with
| _ =>
lazymatch b with
| false => tac K e
| true => fail
end
| 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 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 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
| InjR ?e => go (InjRCtx :: K) e
| 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 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
| true => tac K e
end
end in go (@nil ectx_item) e.
Local Lemma head_step_into_val e σ e' v' σ' efs :
IntoVal e' v'
head_step e σ (of_val v') σ' efs
head_step e σ e' σ' efs.
Proof.
intros Hval Hstep. by rewrite Hval in Hstep.
Qed.
From iris_time.heap_lang Require Export lang tactics.
Ltac prim_step :=
lazymatch goal with
| |- prim_step ?e _ _ _ _ =>
reshape_expr_ordered true e ltac:(fun K e' =>
esplit with K e' _ ; [ reflexivity | reflexivity | ] ;
(idtac + (eapply head_step_into_val; [apply _|])) ; econstructor
| |- prim_step ?e _ _ _ _ _ =>
reshape_expr true e ltac:(fun K e' =>
esplit with K e' _ ; [ reflexivity | reflexivity | ] ; econstructor
)
end ;
simpl_to_of_val.
end.
From iris.heap_lang Require Import proofmode notation.
From iris_time.heap_lang Require Import proofmode notation.
From iris.base_logic.lib Require Import na_invariants.
From stdpp Require Import namespaces.
......@@ -34,12 +34,12 @@ Section Thunk.
own γ (mnat ac)
(
( (f : val),
t UNEVALUATEDV f
{{{ TC nc }}} f #() {{{ v, RET v ; φ v }}}
t UNEVALUATEDV « f »
{{{ TC nc }}} « f #() » {{{ v, RET « v » ; φ v }}}
TC ac
)
( (v : val),
t EVALUATEDV v
t EVALUATEDV « v »
φ v
(nc ac)%nat
)
......@@ -88,15 +88,15 @@ Section Thunk.
Lemma create_spec p nc φ f :
TC_invariant -
{{{ TC 1 ( {{{ TC nc }}} f #() {{{ v, RET v ; φ v }}} ) }}}
«create» f
{{{ TC 3 ( {{{ TC nc }}} «f #()» {{{ v, RET « v » ; φ v }}} ) }}}
«create f»
{{{ (t : loc), RET #t ; Thunk p t nc φ }}}.
Proof.
iIntros "#Htickinv" (Φ) "!# [? Hf] Post".
iDestruct (zero_TC with "Htickinv") as ">Htc0".
iMod (auth_mnat_alloc 0) as (γ) "[Hγ● Hγ◯]".
iApply wp_fupd.
unlock create ; wp_lam. wp_tick_alloc t.
wp_tick_lam. wp_tick_inj. wp_tick_alloc t.
iApply "Post".
iExists γ, nc ; rewrite (_ : nc - nc = 0)%nat ; last lia.
iFrame "Hγ◯".
......@@ -108,16 +108,16 @@ Section Thunk.
(thunkN t) F
( (v : val), φ v - φ v φ v)
TC_invariant -
{{{ TC 7 Thunk p t 0 φ na_own p F }}}
«force» #t
{{{ v, RET v ; φ v na_own p F }}}.
{{{ TC 11 Thunk p t 0 φ na_own p F }}}
«force #t»
{{{ v, RET «v» ; φ v na_own p F }}}.
Proof.
iIntros (? Hφdup).
iIntros "#Htickinv" (Φ) "!# (? & #Hthunk & Hp) Post".
iDestruct "Hthunk" as (γ nc) "#[Hthunkinv Hγ◯]".
rewrite (_ : nc - 0 = nc)%nat ; last lia.
iApply wp_fupd.
unlock force ; wp_lam.
wp_tick_lam.
(* reading the thunk *)
iDestruct (na_inv_open p F (thunkN t) with "Hthunkinv Hp")
as ">(Hthunk & Hp & Hclose)" ; [done|done|] ;
......@@ -129,8 +129,8 @@ Section Thunk.
wp_tick_load. wp_tick_match.
iDestruct (own_auth_mnat_le with "Hγ● Hγ◯") as %I.
iDestruct (TC_weaken _ _ I with "Htc") as "Htc".
wp_tick ; wp_apply ("Hf" with "Htc") ; iIntros (v) "Hv".
wp_tick_let. wp_tick_store. wp_tick_seq.
wp_apply ("Hf" with "Htc") ; iIntros (v) "Hv".
wp_tick_let. wp_tick_inj. wp_tick_store. wp_tick_seq.
iApply "Post".
iDestruct (Hφdup with "Hv") as "[Hv $]".
iApply "Hclose". iFrame "Hp".
......
This diff is collapsed.
From iris.heap_lang Require Import proofmode notation adequacy lang.
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris.base_logic Require Import invariants.
From iris_time Require Import Auth_nat Reduction TimeCredits.
......@@ -57,12 +57,11 @@ Local Notation ℓ := tick_counter.
* a proof that the original expression is safe. *)
Lemma safe_tctranslation__safe_here {Hloc : TickCounter} m e σ :
is_closed [] e
loc_fresh_in_expr e
safe «e» S«σ, m»
is_Some (to_val e) reducible e σ.
Proof.
intros Hclosed Hfresh Hsafe.
intros Hfresh Hsafe.
(* case analysis on whether e is a value *)
destruct (to_val e) as [ v | ] eqn:Hnotval.
(* if e is a value, then we get the result immediately: *)
......@@ -70,11 +69,23 @@ Proof.
(* if e is not a value, then we show that it is reducible: *)
- right.
(* we decompose e into a maximal evaluation context K and a head-redex: *)
pose proof (not_val_fill_active_item _ Hclosed Hnotval) as He ; clear Hclosed Hnotval.
destruct He as [ (K & e1 & ->) | (K & ki & v & -> & Hactive) ].
pose proof (not_val_fill_active_item _ Hnotval) as He ; clear Hnotval.
destruct He as [ (K & x & ->) |
[ (K & e1 & ->) |
[ (K & f & x & e1 & ->) |
(K & ki & v & -> & Hactive) ]]].
(* either e = Var x: *)
+ (* then Var x is stuck *)
exfalso. eapply stuck_not_safe; [|done]. rewrite translation_fill.
apply stuck_fill, head_stuck_stuck.
{ split; [done|]. intros ???? Hstep. inversion Hstep. }
apply ectxi_language_sub_redexes_are_values=>-[] //.
(* either e = K[Fork e1]: *)
+ (* then we easily derive a reduction from e: *)
eexists _, _, _. apply Ectx_step', ForkS.
eexists _, _, _, _. apply Ectx_step', ForkS.
(* either e = K[Rec f x e1]: *)
+ (* then we easily derive a reduction from e: *)
eexists _, _, _, _. apply Ectx_step', RecS.
(* or e = K[ki[v]] where ki is an active item: *)
+ (* it is enough to show that ki[v] is reducible: *)
apply loc_fresh_in_expr_fill_inv in Hfresh ;
......@@ -108,15 +119,14 @@ Proof.
* exact Hred.
Qed.
Lemma safe_tctranslation__safe {Hloc : TickCounter} m e σ t2 σ2 e2 :
is_closed [] e
loc_fresh_in_expr e2
σ2 !! = None
safe «e» S«σ, m»
rtc step ([e], σ) (t2, σ2)
rtc erased_step ([e], σ) (t2, σ2)
e2 t2
is_Some (to_val e2) reducible e2 σ2.
Proof.
intros Hclosed He Hℓσ Hsafe [n Hnsteps] % rtc_nsteps He2.
intros He Hℓσ Hsafe [n Hnsteps] % rtc_nsteps He2.
assert (n m)%nat by by eapply safe_tctranslation__bounded.
assert (safe «e2» S«σ2, m-n») as Hsafe2.
{
......@@ -125,12 +135,6 @@ Proof.
- eassumption.
- change [«e»] with T«[e]». apply simulation_exec_success' ; auto.
}
assert (is_closed [] e2) as Hclosede2.
{
assert (Forall (is_closed []) t2) as Hclosedt2
by eauto using nsteps_rtc, is_closed_exec.
by eapply Forall_forall in Hclosedt2 ; last exact He2.
}
by eapply safe_tctranslation__safe_here.
Qed.
......@@ -138,31 +142,29 @@ Qed.
* a proof that the original expression has adequate results. *)
Lemma adequate_tctranslation__adequate_result {Hloc : TickCounter} m φ e σ t2 σ2 v2 :
is_closed [] e
σ2 !! = None
adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v))
rtc step ([e], σ) (of_val v2 :: t2, σ2)
rtc erased_step ([e], σ) (Val v2 :: t2, σ2)
φ v2.
Proof.
intros Hclosed Hfresh Hadq [n Hnsteps] % rtc_nsteps.
intros Hfresh Hadq [n Hnsteps] % rtc_nsteps.
assert (safe «e» S«σ, m») as Hsafe by by eapply safe_adequate.
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 _ _ _ (λ 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.
replace (Val «v2» :: _) with (T«Val v2 :: t2») by done.
eapply simulation_exec_success' ; eauto.
Qed.
(* now lets combine the two results. *)
Lemma adequate_tctranslation__adequate m φ e σ :
is_closed [] e
( `{TickCounter}, adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v)))
adequate NotStuck e σ (λ v σ, φ v).
Proof.
intros Hclosed Hadq.
intros Hadq.
split.
(* (1) adequate result: *)
- intros t2 σ2 v2 Hsteps.
......@@ -180,7 +182,7 @@ Proof.
eassert ( set1 set2) as [H1 H2] % not_elem_of_union
by (unfold ; apply is_fresh).
assert (loc_fresh_in_expr e2)
by by apply loc_not_in_set_is_fresh.
by by apply loc_not_in_set_is_fresh_in_expr.
assert (σ2 !! = None)
by by (simpl ; eapply not_elem_of_dom).
specialize (Hadq Hloc) as Hsafe % safe_adequate.
......@@ -249,13 +251,13 @@ Lemma spec_tctranslation__bounded {Σ} m ψ e :
{{{ TC m }}} «e» {{{ v, RET v ; ⌜ψ v }}}
)
`{TickCounter} `{timeCreditHeapPreG Σ} σ1 t2 σ2 (z : Z),
rtc step ([«e»], S«σ1, m») (T«t2», S«σ2, z»)
rtc erased_step ([«e»], S«σ1, m») (T«t2», S«σ2, z»)
0 z.
Proof.
intros Hspec Hloc HtcPreG σ1 t2 σ2 z Hsteps.
(* apply the invariance result. *)
apply (wp_invariance Σ _ NotStuck «e» S«σ1,m» T«t2» S«σ2,z») ; simpl ; last assumption.
intros HinvG.
intros HinvG κs κs'.
(* now we have to prove a WP for some state interpretation, for which
* we settle the needed invariant TC_invariant. *)
set σ' := S«σ1».
......@@ -287,7 +289,7 @@ Proof.
by iFrame.
}
(* finally, use the user-given specification: *)
iModIntro. iExists gen_heap_ctx. iFrame "Hh●".
iModIntro. iExists (λ σ _ _, gen_heap_ctx σ), (λ _, True)%I. iFrame "Hh●".
iSplitL ; first (iApply (Hspec with "Hinv Hγ◯") ; auto).
(* it remains to prove that the interpretation of the final state, along
* with the invariant, implies the inequality *)
......@@ -307,12 +309,10 @@ Qed.
(* The simulation lemma with no assumption that m n. *)
Axiom simulation_exec_alt : {Hloc : TickCounter} m n t1 σ1 t2 σ2,
σ2 !! = None
Forall (is_closed []) t1
nsteps step m (t1, σ1) (t2, σ2)
rtc step (T«t1», S«σ1, n») (T«t2», S«σ2, (n-m)%Z»).
nsteps erased_step m (t1, σ1) (t2, σ2)
rtc erased_step (T«t1», S«σ1, n») (T«t2», S«σ2, (n-m)%Z»).
Lemma spec_tctranslation__bounded' {Σ} m ψ e :
is_closed [] e
( `{timeCreditHeapG Σ},
TC_invariant -
{{{ TC m }}} «e» {{{ v, RET v ; ⌜ψ v }}}
......@@ -320,7 +320,7 @@ Lemma spec_tctranslation__bounded' {Σ} m ψ e :
`{!timeCreditHeapPreG Σ} σ,
bounded_time e σ m.
Proof.
intros Hclosed Hspec HtcPreG σ t2 σ2 n Hnsteps.
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)
......
From iris.heap_lang Require Import proofmode notation adequacy lang.
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris.base_logic Require Import invariants.