Commit 1e470a3a authored by MEVEL Glen's avatar MEVEL Glen

dumped code from private repo

parents
CoqMakefile.conf
Makefile.coq
*.v.d
*.aux
*.glob
*.vo
.lia.cache
## Compiling
To compile the Coq scripts:
cd src/
make
The first time (and each time `_CoqProject` is updated), it also creates the
file `Makefile.coq`.
Other recipes are available, such as `all`, `clean` and `userinstall` (Makefile
taken from [here][coqproject]).
[coqproject]: https://blog.zhenzhang.me/2016/09/19/coq-dev.html
## Index of modules
* `Misc`: some basic things
* `Auth_nat`, `Auth_mnat`: simple lemmas about the authoritative resources on
(ℕ, +) and (ℕ, max)
* `Reduction`: generic lemmas about reduction, safety, closedness, fresh
locations… [should be renamed or split into several files]
* `Tactics`: tactics that help reducing concrete terms
* `Translation`: definition of the translation and syntactic lemmas about it
* `Simulation`: Lemmas about the operational semantics of the translation
* `TimeCredits`: implementation of time credits
* `TimeReceipts`: implementation of time receipts
* `Examples`: a (too) simple example illustrating the use of time credits
* `LibThunk`: implementation of timed thunks using time credits [WIP, does not
compile for now]
* `test`: an alternative proof of the main theorem of time credits, that does
not rely on the unsafe behaviour of `tick` [to be merged into `TimeCredits`]
From iris Require Export algebra.auth base_logic.lib.own proofmode.tactics.
Notation "'●mnat' n" := (Auth (A:=mnat) (Excl' n%nat) ε) (at level 20).
Notation "'◯mnat' n" := (Auth (A:=mnat) None n%nat) (at level 20).
Section Auth_mnat.
Context `{inG Σ (authR mnatUR)}.
Lemma own_auth_mnat_null (γ : gname) (m : mnat) :
own γ (mnat m) -
own γ (mnat m) own γ (mnat 0).
Proof.
by rewrite - own_op (_ : mnat m mnat 0 = mnat m).
Qed.
Global Arguments own_auth_mnat_null _ _%nat_scope.
Lemma auth_mnat_update_read_auth (γ : gname) (m : mnat) :
own γ (mnat m) -
|==> own γ (mnat m) own γ (mnat m).
Proof.
iIntros "H●".
iDestruct (own_auth_mnat_null with "H●") as "[H● H◯]".
(iMod (own_update_2 with "H● H◯") as "[$ $]" ; last done).
apply auth_update, mnat_local_update. lia.
Qed.
Global Arguments auth_mnat_update_read_auth _ _%nat_scope.
Lemma auth_mnat_update_incr (γ : gname) (m k : mnat) :
own γ (mnat m) -
|==> own γ (mnat (m + k : mnat)).
Proof.
iIntros "H●". iDestruct (own_auth_mnat_null with "H●") as "[H● H◯]".
iMod (own_update_2 with "H● H◯") as "[$ _]" ; last done.
apply auth_update, mnat_local_update. lia.
Qed.
Global Arguments auth_mnat_update_incr _ (_ _)%nat_scope.
End Auth_mnat.
\ No newline at end of file
From iris Require Export algebra.auth base_logic.lib.own proofmode.tactics.
Notation "'●nat' n" := (Auth (A:=nat) (Excl' n%nat) ε) (at level 20).
Notation "'◯nat' n" := (Auth (A:=nat) None n%nat) (at level 20).
Section Auth_nat.
Context `{inG Σ (authR natUR)}.
Lemma auth_nat_alloc (n : nat) :
(|==> γ, own γ ( n) own γ ( n))%I.
Proof.
by iMod (own_alloc ( n n)) as (γ) "[? ?]" ; auto with iFrame.
Qed.
Lemma own_auth_nat_le (γ : gname) (m n : nat) :
own γ (nat m) -
own γ (nat n) -
(n m)%nat.
Proof.
iIntros "H● H◯".
by iDestruct (own_valid_2 with "H● H◯")
as % [?%nat_le_sum _] % auth_valid_discrete_2.
Qed.
Lemma own_auth_nat_null (γ : gname) (m : nat) :
own γ (nat m) -
own γ (nat m) own γ (nat 0).
Proof.
by rewrite - own_op (_ : nat m nat 0 = nat m).
Qed.
Lemma auth_nat_update_incr (γ : gname) (m k : nat) :
own γ (nat m) -
|==> own γ (nat (m + k)) own γ (nat k).
Proof.
iIntros "H●". iDestruct (own_auth_nat_null with "H●") as "[H● H◯]".
iMod (own_update_2 with "H● H◯") as "[$ $]" ; last done.
apply auth_update, nat_local_update. lia.
Qed.
Lemma auth_nat_update_decr (γ : gname) (m n k : nat) :
(k n)%nat
own γ (nat m) -
own γ (nat n) -
|==> own γ (nat (m - k)) own γ (nat (n - k)).
Proof.
iIntros (I) "H● H◯".
iDestruct (own_auth_nat_le with "H● H◯") as %J.
iMod (own_update_2 with "H● H◯") as "[$ $]" ; last done.
apply auth_update, nat_local_update. lia.
Qed.
Lemma own_auth_nat_weaken (γ : gname) (n n : nat) :
(n n)%nat
own γ (nat n) -
own γ (nat n).
Proof.
iIntros (I) "H".
rewrite (_ : n = (n - n) + n)%nat ; last lia.
iDestruct "H" as "[_$]".
Qed.
End Auth_nat.
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
# https://blog.zhenzhang.me/2016/09/19/coq-dev.html
# Makefile originally taken from coq-club
%: Makefile.coq phony
+make -f Makefile.coq $@
all: Makefile.coq
+make -f Makefile.coq all
clean: Makefile.coq
+make -f Makefile.coq clean
rm -f Makefile.coq
Makefile.coq: _CoqProject Makefile
coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq
_CoqProject: ;
Makefile: ;
phony: ;
.PHONY: all clean phony
From mathcomp Require Export ssreflect.
From stdpp Require Export base list relations.
Tactic Notation "make_eq" constr(t) "as" ident(x) ident(E) :=
set x := t ;
assert (t = x) as E by reflexivity ;
clearbody x.
Lemma take_cons {A : Type} (n : nat) (x : A) (xs : list A) :
(0 < n)%nat take n (x :: xs) = x :: take (n-1)%nat xs.
Proof.
intros <- % Nat.succ_pred_pos. by rewrite /= - minus_n_O.
Qed.
Lemma drop_cons {A : Type} (n : nat) (x : A) (xs : list A) :
(0 < n)%nat drop n (x :: xs) = drop (n-1)%nat xs.
Proof.
intros <- % Nat.succ_pred_pos. by rewrite /= - minus_n_O.
Qed.
Lemma nsteps_split `{R : relation A} m n x y :
nsteps R (m+n) x y
(z : A), nsteps R m x z nsteps R n z y.
Proof.
revert x ; induction m as [ | m' IH ] ; intros x H.
- exists x. split ; [ constructor | assumption ].
- inversion H as [ (*…*) | sum' x_ z y_ Hxz Hzy Esum' Ex Ey ] ; clear dependent sum' x_ y_.
apply IH in Hzy as (ω & Hzω & Hωy).
exists ω. split ; first econstructor ; eassumption.
Qed.
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 e1 ltac:(fun v1 => go (AppRCtx v1 :: K) e2)
| App ?e1 ?e2 => go (AppLCtx e2 :: K) e1
| 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
| 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
| 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 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
| _ =>
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 erewrite of_to_val in Hstep.
Qed.
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) ; econstructor
)
end ;
simpl_to_of_val.
\ No newline at end of file
This diff is collapsed.
From iris.heap_lang Require Import proofmode notation adequacy.
From iris.algebra Require Import auth.
From iris.base_logic Require Import invariants.
From iris.proofmode Require Import classes.
From stdpp Require Import namespaces.
Require Import Auth_nat Auth_mnat Misc Reduction Tactics.
Require Export Translation Simulation.
(* Require Import TimeCredits. *)
Implicit Type e : expr.
Implicit Type v : val.
Implicit Type σ : state.
Implicit Type t : list expr.
Implicit Type K : ectx heap_ectx_lang.
Implicit Type m n : nat.
(* rem: Unicode notations?
* medals: 🏅🥇🎖
* gears: ⚙⛭
* shields: ⛨
* florettes: ✿❀
* squares: ▣ ▢ ▤ ▥ ☑
* circles: ◉ ◎ ◌ ◍ ☉
* pentagons: ⬟ ⬠
* hexagons: ⬢ ⬡
* shogi pieces: ☗ ☖
* other: ⮝ ⮙ ⯊ ⯎
*)
(*
* Prerequisites on the global monoid Σ
*)
Class timeReceiptHeapPreG Σ := {
timeReceiptHeapPreG_heapPreG :> heapPreG Σ ;
timeReceiptHeapPreG_inG1 :> inG Σ (authR natUR) ;
timeReceiptHeapPreG_inG2 :> inG Σ (authR mnatUR) ;
}.
Class timeReceiptLoc := {
timeReceiptLoc_loc : loc ;
}.
Class timeReceiptHeapG Σ := {
timeReceiptHeapG_heapG :> heapG Σ ;
timeReceiptHeapG_inG1 :> inG Σ (authR natUR) ;
timeReceiptHeapG_inG2 :> inG Σ (authR mnatUR) ;
timeReceiptHeapG_loc :> timeReceiptLoc ;
timeReceiptHeapG_name1 : gname ;
timeReceiptHeapG_name2 : gname ;
}.
Local Notation γ1 := timeReceiptHeapG_name1.
Local Notation γ2 := timeReceiptHeapG_name2.
Local Notation := timeReceiptLoc_loc.
(*
* Implementation and specification of `TR` and `tock`
*)
Section Tock.
Context `{timeReceiptLoc}.
Definition loop : val :=
rec: "f" <> := "f" #().
Definition tock : val :=
tick loop .
End Tock.
Section TockSpec.
Context `{timeReceiptHeapG Σ}.
Definition TR (n : nat) : iProp Σ :=
own γ1 (nat n).
Definition TRdup (n : mnat) : iProp Σ :=
own γ2 (mnat n).
Arguments TRdup _%nat_scope.
Lemma TR_plus m n :
TR (m + n) (TR m TR n)%I.
Proof. by rewrite /TR auth_frag_op own_op. Qed.
Lemma TR_succ n :
TR (S n) (TR 1 TR n)%I.
Proof. by rewrite (eq_refl : S n = 1 + n)%nat TR_plus. Qed.
Lemma TR_timeless n :
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.
Lemma TRdup_max m n :
TRdup (m `max` n) (TRdup m TRdup n)%I.
Proof. by rewrite /TRdup auth_frag_op own_op. Qed.
Lemma TRdup_timeless n :
Timeless (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.
Definition timeReceiptN := nroot .@ "timeReceipt".
Definition TOCKCTXT (nmax : nat) : iProp Σ :=
inv timeReceiptN ( (n:nat), #(nmax-n-1) own γ1 (nat n) own γ2 (mnat n) (n < nmax)%nat)%I.
Lemma TR_nmax_absurd (nmax : nat) (E : coPset) :
timeReceiptN E
TOCKCTXT nmax - TR nmax ={E}= False.
Proof.
iIntros (?) "#Inv Hγ1◯".
iInv timeReceiptN as (n) ">(Hℓ & Hγ1● & Hγ2● & In)" "InvClose" ; iDestruct "In" as %In.
iDestruct (own_auth_nat_le with "Hγ1● Hγ1◯") as %In'.
exfalso ; lia.
Qed.
Lemma TR_TRdup (nmax : nat) (E : coPset) (n : nat) :
timeReceiptN E
TOCKCTXT nmax - TR n ={E}= TR n TRdup n.
Proof.
iIntros (?) "#Inv Hγ1◯".
iInv timeReceiptN as (m) ">(Hℓ & Hγ1● & Hγ2● & Im)" "InvClose".
iDestruct (own_auth_nat_le with "Hγ1● Hγ1◯") as %In.
iDestruct (auth_mnat_update_read_auth with "Hγ2●") as ">[Hγ2● Hγ2◯]".
iAssert (TR n TRdup n)%I with "[$Hγ1◯ Hγ2◯]" as "$". {
rewrite (_ : m = m `max` n) ; last lia.
iDestruct "Hγ2◯" as "[_ $]".
}
iApply "InvClose". auto with iFrame.
Qed.
Theorem loop_spec s E (Φ : val iProp Σ) :
WP loop #() @ s ; E {{ Φ }}%I.
Proof.
iLöb as "IH". wp_rec. iExact "IH".
Qed.
Theorem tock_spec (nmax : nat) s E e v :
timeReceiptN E
IntoVal e v
TOCKCTXT nmax -
{{{ True }}} tock e @ s ; E {{{ RET v ; TR 1 }}}.
Proof.
intros ? <- % of_to_val. iIntros "#Inv" (Ψ) "!# _ HΨ".
iLöb as "IH".
wp_lam.
(* open the invariant, in order to read the value k = nmax−n−1 of location ℓ: *)
wp_bind (! _)%E ;
iInv timeReceiptN as (n) ">(Hℓ & Hγ1● & Hγ2● & In)" "InvClose" ; iDestruct "In" as %In.
wp_load.
(* close the invariant: *)
iMod ("InvClose" with "[ Hℓ Hγ1● Hγ2● ]") as "_" ; [ by auto with iFrame | iModIntro ].
wp_let.
(* test whether k ≤ 0: *)
wp_op ; destruct (bool_decide (nmax - n - 1 0)) eqn:Im ; wp_if.
(* — if k ≤ 0 then we loop indefinitely, which gives us any spec we want
(because we are reasoning in partial correctness): *)
- iApply loop_spec.
(* — otherwise: *)
- apply Is_true_false in Im ; rewrite -> bool_decide_spec in Im.
wp_op.
(* open the invariant again, in order to perform CAS on location ℓ: *)
wp_bind (CAS _ _ _)%E ;
iInv timeReceiptN as (n') ">(Hℓ & Hγ1● & Hγ2● & In')" "InvClose" ; iDestruct "In'" as %In'.
(* test whether the value ℓ is still k, by comparing n with n': *)
destruct (nat_eq_dec n n') as [ <- | Hneq ].
(* — if it holds, then CAS succeeds and ℓ is decremented: *)
+ wp_cas_suc.
(* reform the invariant with n+1 instead of n, and an additional time
receipt produced: *)
replace (nmax - n - 1 - 1) with (nmax - (n+1)%nat - 1) by lia.
iMod (auth_nat_update_incr _ _ 1 with "Hγ1●") as "[Hγ1● Hγ1◯]" ; simpl.
iMod (auth_mnat_update_incr _ _ 1 with "Hγ2●") as "Hγ2●" ; simpl.
assert ((n+1) < nmax)%nat by lia.
(* close the invariant: *)
iMod ("InvClose" with "[ Hℓ Hγ1● Hγ2● ]") as "_" ; [ by auto with iFrame | iModIntro ].
(* finish: *)
wp_if. iApply "HΨ" ; iExact "Hγ1◯".
(* — otherwise, CAS fails and ℓ is unchanged: *)
+ wp_cas_fail ; first (injection ; lia).
(* close the invariant as is: *)
iMod ("InvClose" with "[ Hℓ Hγ1● Hγ2● ]") as "_" ; [ by auto with iFrame | iModIntro ] ; clear dependent n.
wp_if.
(* conclude using the induction hypothesis: *)
iApply ("IH" with "HΨ").
Qed.
Theorem tock_spec_simple (nmax : nat) v :
TOCKCTXT nmax -
{{{ True }}} tock v {{{ RET v ; TR 1 }}}.
Proof.
iIntros "#Inv" (Ψ) "!# H HΨ".
by iApply (tock_spec with "Inv H HΨ").
Qed.
End TockSpec.
(*
* Simulation
*)
Notation trtranslation := (translation tock).
Notation trtranslationV := (translationV tock).
Notation trtranslationS := (translationS tock).
Notation trtranslationKi := (translationKi tock).
Notation trtranslationK := (translationK tock).
Notation "E« e »" := (trtranslation e%E).
Notation "V« v »" := (trtranslationV v%V).
Notation "Ki« ki »" := (trtranslationKi ki).
Notation "K« K »" := (trtranslationK K).
Notation "S« σ »" := (trtranslationS σ%V).
Notation "S« σ , n »" := (<[ := LitV (LitInt n%nat)]> (trtranslationS σ%V)).
Notation "T« t »" := (trtranslation <$> t%E).
Notation "« e »" := (trtranslation e%E).
Notation "« e »" := (trtranslation e%E) : expr_scope.
Notation "« v »" := (trtranslationV v%V) : val_scope.
(* for some reason, these notations make parsing fail,
* even if they only regard printing… *)
(*
Notation "« e »" := (trtranslation e%E) (only printing).
Notation "« v »" := (trtranslationV v%V) (only printing).
Notation "« ki »" := (trtranslationKi ki) (only printing).
Notation "« K »" := (trtranslationK K) (only printing).
Notation "« σ »" := (trtranslationS σ%V) (only printing).
Notation "« σ , n »" := (<[ℓ := LitV (LitInt n%nat)]> (trtranslationS σ%V)) (only printing).
Notation "« t »" := (trtranslation <$> t%E) (only printing).
*)
Section Soundness.
(* TODO *)
End Soundness.
(*
* Proof-mode tactics for proving WP of translated expressions
*)
Section Tactics.
(* TODO *)
End Tactics.
Ltac wp_tock :=
idtac.
\ No newline at end of file
This diff is collapsed.
-Q . ""
Auth_mnat.v
Auth_nat.v
Examples.v
LibThunk.v
Misc.v
Reduction.v
Tactics.v
test.v
Simulation.v
TimeCredits.v
TimeReceipts.v
Translation.v
From iris.heap_lang Require Import proofmode notation adequacy.
From iris.algebra Require Import auth.
From iris.base_logic Require Import invariants.
From iris.proofmode Require Import classes.
From stdpp Require Import namespaces.
Require Import Auth_nat TimeCredits.
Local Notation γ := timeCreditHeapG_name.
Local Notation := timeCreditLoc_loc.
Lemma gen_heap_ctx_mapsto {Σ : gFunctors} {Hgen : gen_heapG loc val Σ} (σ : state) (l : loc) (v v' : val) :
σ !! l = Some v
gen_heap_ctx σ -
l v' -
v = v'.
Proof.
iIntros (Hσ) "Hheap Hl".
rewrite /gen_heap_ctx /=.
unfold mapsto ; destruct mapsto_aux as [_->] ; rewrite /mapsto_def /=.
iDestruct (own_valid_2 with "Hheap Hl") as %H.
iPureIntro.
assert (CmraDiscrete (gen_heapUR loc val)) as Hdiscrete by apply _.
apply ((auth_valid_discrete_2 (H:=Hdiscrete))) in H as [H _].
apply gen_heap_singleton_included in H.
pose proof (eq_stepl Hσ H) as E. by injection E.
Qed.
Lemma spec_tctranslation__bounded {Σ} m (ψ : val Prop) e :
( `{timeCreditHeapG Σ},
TICKCTXT -
{{{ TC m }}} «e» {{{ v, RET v ; ⌜ψ v }}}
)
`{!timeCreditLoc} `{!timeCreditHeapPreG Σ} σ1 t2 σ2 (z : Z),
rtc 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.
(* … now we have to prove a WP for some state interpretation, for which
* we settle the needed invariant TICKCTXT. *)
set σ' := S«σ1».
(* allocate the heap, including cell ℓ (on which we need to keep an eye): *)
iMod (own_alloc ( to_gen_heap (<[ := #m]> σ') to_gen_heap {[ := #m]}))
as (h) "[Hh● Hℓ◯]".
{
apply auth_valid_discrete_2 ; split.
- rewrite - insert_delete ; set σ'' := delete σ'.
unfold to_gen_heap ; rewrite 2! fmap_insert fmap_empty insert_empty.
exists (to_gen_heap σ'').
rewrite (@gmap.insert_singleton_op _ _ _ _ (to_gen_heap σ'')) //.
rewrite lookup_fmap ; apply fmap_None, lookup_delete.
- apply to_gen_heap_valid.
}
(* allocate the ghost state associated with ℓ: *)
iMod (auth_nat_alloc m) as (γ) "[Hγ● Hγ◯]".
(* packing all those bits, build the heap instance necessary to use time credits: *)
destruct HtcPreG as [[HinvPreG [HgenHeapPreInG]] HinG] ; simpl ; clear HinvPreG.
pose (Build_timeCreditHeapG Σ (HeapG Σ HinvG (GenHeapG _ _ Σ _ _ HgenHeapPreInG h)) HinG _ γ)
as HtcHeapG.
(* create the invariant: *)
iAssert (|={}=> TICKCTXT)%I with "[Hℓ◯ Hγ●]" as "> #Hinv".
{
iApply inv_alloc.
iExists m.
unfold mapsto ; destruct mapsto_aux as [_ ->] ; simpl.
unfold to_gen_heap ; rewrite fmap_insert fmap_empty insert_empty.
by iFrame.
}
(* finally, use the user-given specification: *)
iModIntro. iExists gen_heap_ctx. 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… *)
iIntros "Hheap2".
(* open the invariant: *)
iInv timeCreditN as (m') ">[Hc Hγ●]" "InvClose".
(* derive that z = m' (that is, the relative integer is in fact a natural integer): *)
iDestruct (gen_heap_ctx_mapsto with "Hheap2 Hc") as %Eq ; first (by apply lookup_insert) ;
injection Eq as ->.
(* close the invariant (in fact, this is not required): *)
iMod ("InvClose" with "[-]") as "_" ; first by auto with iFrame.
(* conclude: *)
iMod (fupd_intro_mask' ) as "_" ; first done. iPureIntro.
lia.
Qed.
\ No newline at end of file