Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Coneris wp #42

Merged
merged 17 commits into from
Sep 13, 2024
Merged

Coneris wp #42

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
7a95adc
progress in changing wp of coneris
hei411 Sep 11, 2024
dc21fdb
define modalities for weakest pre
hei411 Sep 11, 2024
fa3a855
specialize state step coupl modality with emptyset mask
hei411 Sep 11, 2024
d317687
updated weakestpre.v
hei411 Sep 12, 2024
dfd6824
add useful lemma
hei411 Sep 12, 2024
3ee1497
lifting.v done
hei411 Sep 12, 2024
1d52753
ectx_lifting.v completed
hei411 Sep 12, 2024
a83e098
sketch of adequacy
hei411 Sep 12, 2024
dcea04d
complete wp_adequacy_val_fupd
hei411 Sep 12, 2024
af7d00b
progress with adequacy
hei411 Sep 13, 2024
a340581
NIT
hei411 Sep 13, 2024
b267566
NIT
hei411 Sep 13, 2024
6fe6977
NIT
hei411 Sep 13, 2024
ae7dbcb
fix adequacy
hei411 Sep 13, 2024
65898e3
NIT
hei411 Sep 13, 2024
5d67c5d
fix error rules
hei411 Sep 13, 2024
7f1bcf9
fix rand counter
hei411 Sep 13, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 5 additions & 8 deletions theories/con_prob_lang/erasure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -632,7 +632,7 @@ Local Lemma force_first_thread_scheduler_lemma' `{Hcountable:Countable sch_int_
(e::es1)!!num=Some e1 ->
to_val e = None ->
to_val e1 = None ->
(prim_step e1 σ1 ≫= λ '(e', s, l), sch_exec sch n (initial, (<[num:=e']> (e::es1 ++ l), s))) = sch_exec (force_first_thread_scheduler sch num initial) (S n) (None, (e::es1, σ1)).
(prim_step e1 σ1 ≫= λ '(e', s, l), sch_exec sch n (initial, (<[num:=e']> (e::es1) ++ l, s))) = sch_exec (force_first_thread_scheduler sch num initial) (S n) (None, (e::es1, σ1)).
Proof.
intros H Hv Hv'.
rewrite /force_first_thread_scheduler{2}/sch_exec.
Expand All @@ -643,9 +643,6 @@ Proof.
rewrite !dret_id_left.
erewrite force_first_thread_scheduler_lemma.
repeat f_equal.
rewrite -insert_app_l.
- by rewrite app_comm_cons.
- by eapply lookup_lt_Some.
Qed.


Expand All @@ -655,8 +652,8 @@ Lemma prim_coupl_step_prim_sch_erasable `{Hcountable:Countable sch_int_σ} e n e
to_val e = None ->
to_val e1 = None ->
Rcoupl
(prim_step e1 σ1 ≫= λ '(e', s, l), sch_exec sch n (ζ, (<[num:=e']> (e::es1 ++ l), s)))
(μ ≫= (λ σ2, prim_step e1 σ2 ≫= λ '(e', s, l), sch_exec sch n (ζ, (<[num:=e']> (e::es1 ++ l), s))))
(prim_step e1 σ1 ≫= λ '(e', s, l), sch_exec sch n (ζ, (<[num:=e']> (e::es1) ++ l, s)))
(μ ≫= (λ σ2, prim_step e1 σ2 ≫= λ '(e', s, l), sch_exec sch n (ζ, (<[num:=e']> (e::es1) ++ l, s))))
eq.
Proof.
intros H1 H2 H3 H4.
Expand All @@ -677,8 +674,8 @@ Lemma prim_coupl_step_prim' `{Hcountable:Countable sch_int_σ} e n es1 σ1 α bs
to_val e = None ->
to_val e1 = None ->
Rcoupl
(prim_step e1 σ1 ≫= λ '(e', s, l), sch_exec sch n (ζ, (<[num:=e']> (e::es1 ++ l), s)))
(state_step σ1 α ≫= (λ σ2, prim_step e1 σ2 ≫= λ '(e', s, l), sch_exec sch n (ζ, (<[num:=e']> (e::es1 ++ l), s))))
(prim_step e1 σ1 ≫= λ '(e', s, l), sch_exec sch n (ζ, (<[num:=e']> (e::es1) ++ l, s)))
(state_step σ1 α ≫= (λ σ2, prim_step e1 σ2 ≫= λ '(e', s, l), sch_exec sch n (ζ, (<[num:=e']> (e::es1) ++ l, s))))
eq.
Proof.
intros H1 H2 H3 H4.
Expand Down
277 changes: 145 additions & 132 deletions theories/coneris/adequacy.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,97 +25,118 @@ Section adequacy.
⌜ 0 <= ε ⌝ -∗
⌜ 0 <= ε' ⌝ -∗
⌜pgl μ R ε⌝ -∗
(∀ a , ⌜R a⌝ ={∅}▷=∗^(S n) ⌜pgl (f a) T ε'⌝) -∗
|={∅}▷=>^(S n) ⌜pgl (dbind f μ) T (ε + ε')⌝ : iProp Σ.
(∀ a , ⌜R a⌝ ={∅}=∗ |={∅}▷=>^(n) ⌜pgl (f a) T ε'⌝) -∗
|={∅}=> |={∅}▷=>^(n) ⌜pgl (dbind f μ) T (ε + ε')⌝ : iProp Σ.
Proof.
iIntros (???) "H".
iApply (step_fupdN_mono _ _ _ (⌜(∀ a b, R a → pgl (f a) T ε')⌝)).
{ iIntros (?). iPureIntro. eapply pgl_dbind; eauto. }
iIntros (???) "/=".
iMod ("H" with "[//]"); auto.
iApply ("H" with "[//]").
Qed.

Lemma pgl_dbind_adv' `{Countable A, Countable A'}
(f : A → distr A') (μ : distr A) (R : A → Prop) (T : A' → Prop) ε ε' n :
⌜ 0 <= ε ⌝ -∗
⌜ exists r, forall a, 0 <= ε' a <= r ⌝ -∗
⌜pgl μ R ε⌝ -∗
(∀ a , ⌜R a⌝ ={∅}▷=∗^(S n) ⌜pgl (f a) T (ε' a)⌝) -∗
|={∅}▷=>^(S n) ⌜pgl (dbind f μ) T (ε + SeriesC (λ a : A, (μ a * ε' a)%R))⌝ : iProp Σ.
(∀ a , ⌜R a⌝ ={∅}=∗ |={∅}▷=>^(n) ⌜pgl (f a) T (ε' a)⌝) -∗
|={∅}=> |={∅}▷=>^(n) ⌜pgl (dbind f μ) T (ε + Expval μ ε')⌝ : iProp Σ.
Proof.
iIntros (???) "H".
iApply (step_fupdN_mono _ _ _ (⌜(∀ a b, R a → pgl (f a) T (ε' a))⌝)).
{ iIntros (?). iPureIntro. eapply pgl_dbind_adv; eauto. }
iIntros (???) "/=".
iMod ("H" with "[//]"); auto.
iApply ("H" with "[//]").
Qed.

Lemma glm_erasure `{Countable sch_int_state} (ζ : sch_int_state) (e : expr)
chosen_e es (σ : state) (n : nat) φ (ε : nonnegreal) (sch: scheduler con_prob_lang_mdp sch_int_state) (num:nat) `{!TapeOblivious sch_int_state sch}:
to_val e = None ->
to_val chosen_e = None →
(e::es)!!num = Some chosen_e->
glm chosen_e σ ε (λ '(e2, σ2, efs) ε',
|={∅}▷=>^(S n) ⌜pgl (sch_exec sch n (ζ, (<[num:=e2]>(e::es++efs), σ2))) φ ε'⌝)
⊢ |={∅}▷=>^(S n)
⌜pgl (prim_step chosen_e σ ≫= λ '(e', s, l), sch_exec sch n (ζ, (<[num:= e']>(e :: es ++ l), s))) φ ε⌝.

Lemma wp_adequacy_val_fupd `{Countable sch_int_state} (ζ : sch_int_state) e es (sch: scheduler con_prob_lang_mdp sch_int_state) n v σ ε φ `{!TapeOblivious sch_int_state sch}:
to_val e = Some v →
state_interp σ ∗ err_interp ε ∗
WP e {{ v, ⌜φ v ⌝ }} ⊢
|={⊤, ∅}=> ⌜pgl (sch_exec sch n (ζ, (Val v :: es, σ))) φ ε⌝.
Proof.
iIntros (Hv Hv' Hfound) "Hexec".
iAssert (⌜to_val chosen_e = None⌝)%I as "-#H"; [done|].
iAssert (⌜(e::es)!!num = Some chosen_e⌝)%I as "-#H'"; [done|].
iRevert "Hexec H H'".
rewrite /glm /glm'.
set (Φ := (λ '((e1, σ1), ε''),
(⌜to_val e1 = None⌝ -∗ ⌜to_val e = None⌝ -∗ ⌜(e :: es) !! num = Some e1⌝ ={∅}▷=∗^(S n)
⌜pgl (prim_step e1 σ1 ≫= λ '(e', s, l), sch_exec sch n (ζ, (<[num:=e']> (e :: es ++ l), s))) φ ε''⌝)%I) :
prodO partial_cfgO NNRO → iPropI Σ).
assert (NonExpansive Φ).
{ intros m ((?&?)&?) ((?&?)&?) [[[=] [=]] [=]]. by simplify_eq. }
set (F := (glm_pre
(λ '(e2, σ2, efs) (ε' : nonnegreal),
|={∅}▷=>^(S n) ⌜pgl (sch_exec sch n (ζ, (<[num:=e2]> (e :: es ++ efs), σ2))) φ ε'⌝))%I).
iPoseProof (least_fixpoint_iter F Φ with "[]") as "H"; last first.
{ iIntros "Hfix % %".
by iMod ("H" $! ((_, _)) with "Hfix [//][//][//]"). }
iIntros "!#" ([[e1 σ1] ε'']). rewrite /F/Φ/glm_pre.
clear Hv Hv'.
iIntros "[(%R & %ε1 & %ε2 & %Hred & (%r & %Hr) & % & %Hlift & H)| H] %Hv %Hv' %Hlookup".
- iApply step_fupdN_mono.
{ apply pure_mono. eapply pgl_mon_grading; done. }
iApply pgl_dbind_adv'.
+ iPureIntro; apply cond_nonneg.
+ iPureIntro. exists r. split; [apply cond_nonneg|done].
+ done.
+ iIntros ([[??]?] ?).
rewrite step_fupd_fupdN_S.
iMod ("H" with "[//]") as "[%|H]".
{ iApply step_fupdN_intro; try done. iPureIntro.
apply pgl_1; lra.
}
done.
- iDestruct "H" as "(%R2 & %μ & %ε1 & %ε2 & %Herasable & (%r & %Hr) & % & %Hlift & H)".
iApply (step_fupdN_mono _ _ _
(⌜∀ σ2 , R2 σ2 → pgl (prim_step e1 σ2 ≫= λ '(e', s, l), sch_exec sch n (ζ, (<[num:=e']> (e :: es ++ l), s))) φ
(ε2 σ2)⌝)%I).
{ iIntros (?). iPureIntro.
unshelve erewrite (Rcoupl_eq_elim _ _ (prim_coupl_step_prim_sch_erasable _ _ _ _ _ _ _ μ _ _ _ _)); try done.
apply (pgl_mon_grading _ _
(ε1 + (SeriesC (λ ρ , μ ρ * ε2 ρ)))) => //.
eapply pgl_dbind_adv; eauto; [by destruct ε1|].
exists r.
intros a.
split; [by destruct (ε2 _) | by apply Hr].
iIntros (Hval) "(?&?&Hwp)".
rewrite pgl_wp_unfold/pgl_wp_pre.
iMod ("Hwp" with "[$]") as "H".
simpl. rewrite Hval.
iRevert (σ ε) "H".
iApply state_step_coupl_ind.
iModIntro.
iIntros (??) "[%|[>(_&_&%)|(%R&%μ&%&%&%Herasable&%&%Hineq&%Hpgl&H)]]".
- iPureIntro. by apply pgl_1.
- iApply fupd_mask_intro; first done.
iIntros "_".
iPureIntro.
erewrite sch_exec_is_final; last done.
eapply pgl_mon_grading; last apply pgl_dret; auto.
- erewrite <-Herasable; last done.
iApply (fupd_mono _ _ (⌜_⌝)%I).
{ iPureIntro.
intros H'.
eapply pgl_mon_grading; first apply Hineq.
eapply pgl_dbind_adv; [auto| |exact H'|exact].
naive_solver.
}
iIntros (??).
by iMod ("H" with "[//]") as "[? _]".
Qed.

Lemma state_step_coupl_erasure `{Countable sch_int_state} (ζ : sch_int_state) es σ ε Z n (sch: scheduler con_prob_lang_mdp sch_int_state) φ `{H0 : !TapeOblivious sch_int_state sch}:
state_step_coupl σ ε Z -∗
(∀ σ2 ε2, Z σ2 ε2 ={∅}=∗ |={∅}▷=>^(n)
⌜pgl (sch_exec sch n (ζ, (es, σ2))) φ ε2⌝) -∗
|={∅}=> |={∅}▷=>^(n)
⌜pgl (sch_exec sch n (ζ, (es, σ))) φ ε⌝.
Proof.
iRevert (σ ε).
iApply state_step_coupl_ind.
iIntros "!>" (σ ε) "[%|[?|(%&%μ&%&%&%Herasable&%&%&%&H)]] Hcont".
- iApply step_fupdN_intro; first done.
iPureIntro.
by apply pgl_1.
- by iMod ("Hcont" with "[$]").
- rewrite -Herasable.
iApply (step_fupdN_mono _ _ _ (⌜pgl _ _ (_+_)⌝)%I).
{ iPureIntro.
intros. eapply pgl_mon_grading; exact.
}
iIntros (σ2 Hσ2).
iApply step_fupd_fupdN_S.
iMod ("H" with "[//]") as "H"; iModIntro.
iDestruct "H" as "[%|H]".
{ iApply step_fupdN_intro; try done.
iPureIntro.
apply pgl_1. apply Rge_le. done.
iApply (pgl_dbind_adv' with "[][][][-]"); [done|naive_solver|done|].
iIntros (??).
iMod ("H" with "[//]") as "[H _]".
simpl.
iApply ("H" with "[$]").
Qed.

Lemma state_step_coupl_erasure' `{Countable sch_int_state} (ζ : sch_int_state) e es e' σ ε Z n num (sch: scheduler con_prob_lang_mdp sch_int_state) φ `{!TapeOblivious sch_int_state sch}:
((e::es)!!num = Some e') ->
to_val e = None ->
to_val e' = None ->
state_step_coupl σ ε Z -∗
(∀ σ2 ε2, Z σ2 ε2 ={∅}=∗ |={∅}▷=>^(S n)
⌜pgl (prim_step e' σ2 ≫= λ '(e3, σ3, efs), sch_exec sch n (ζ, (<[num:=e3]> (e :: es) ++ efs, σ3))) φ ε2⌝) -∗
|={∅}=> |={∅}▷=>^(S n)
⌜pgl (prim_step e' σ ≫= λ '(e3, σ3, efs), sch_exec sch n (ζ, (<[num:=e3]> (e :: es) ++ efs, σ3))) φ ε⌝.
Proof.
intros ???.
iRevert (σ ε).
iApply state_step_coupl_ind.
iIntros "!>" (σ ε) "[%|[?|(%&%μ&%&%&%&%&%&%&H)]] Hcont".
- iApply step_fupdN_intro; first done.
iPureIntro.
by apply pgl_1.
- by iMod ("Hcont" with "[$]").
- unshelve erewrite (Rcoupl_eq_elim _ _ (prim_coupl_step_prim_sch_erasable _ _ _ _ _ _ _ μ _ _ _ _)); [done..|].
iApply (step_fupdN_mono _ _ _ (⌜pgl _ _ (_+_)⌝)%I).
{ iPureIntro.
intros. eapply pgl_mon_grading; exact.
}
by iApply "H".
Qed.
iApply (pgl_dbind_adv'); [done|naive_solver|done|].
iIntros (??).
iMod ("H" with "[//]") as "[H _]".
simpl.
iApply ("H" with "[$]").
Qed.

Lemma wp_refRcoupl_step_fupdN `{Countable sch_int_state} (ζ : sch_int_state) (ε : nonnegreal)
(e : expr) es (σ : state) n φ (sch: scheduler con_prob_lang_mdp sch_int_state) `{!TapeOblivious sch_int_state sch}:
Expand All @@ -124,42 +145,33 @@ Section adequacy.
Proof.
iInduction n as [|n] "IH" forall (ζ ε e es σ); iIntros "((Hσh & Hσt) & Hε & Hwp & Hwps)".
- Local Transparent sch_exec.
rewrite /sch_exec /=.
destruct (to_val e) eqn:Heq.
+ apply of_to_val in Heq as <-.
rewrite pgl_wp_value_fupd.
iMod "Hwp" as "%".
iApply fupd_mask_intro; [set_solver|]; iIntros.
iPureIntro.
apply (pgl_mon_grading _ _ 0); [apply cond_nonneg | ].
apply pgl_dret; auto.
+ iApply fupd_mask_intro; [set_solver|]; iIntros "_".
iPureIntro.
iApply wp_adequacy_val_fupd; last iFrame.
done.
+ rewrite /sch_exec /=.
iApply fupd_mask_intro; [set_solver|]; iIntros "_".
iPureIntro. rewrite Heq.
apply pgl_dzero,
Rle_ge,
cond_nonneg.
- rewrite sch_exec_Sn /sch_step_or_final/=.
destruct (to_val e) eqn:Heq.
+ apply of_to_val in Heq as <-.
rewrite pgl_wp_value_fupd.
iMod "Hwp" as "%".
iApply fupd_mask_intro; [set_solver|]; iIntros "_".
iApply step_fupdN_intro; [done|]. do 4 iModIntro.
iPureIntro.
rewrite dret_id_left'/=.
erewrite sch_exec_is_final; last done.
apply (pgl_mon_grading _ _ 0); [apply cond_nonneg | ].
apply pgl_dret; auto.
iMod (wp_adequacy_val_fupd with "[$]") as "%"; first done.
repeat iModIntro.
by iApply step_fupdN_intro.
+ rewrite {1}/sch_step. rewrite <-dbind_assoc.
replace (ε) with (0+ε)%NNR; last (apply nnreal_ext;simpl; lra).
iApply pgl_dbind'; [done|
iApply fupd_mask_intro; first done.
iIntros "Hclose".
rewrite -fupd_idemp.
iApply (pgl_dbind' _ _ _ _ _ _ (S _)); [done|
iPureIntro; apply cond_nonneg|
iPureIntro;apply pgl_trivial;simpl;lra|
..].
iApply fupd_mask_intro; first done.
iIntros "Hclose".
iIntros ([sch_σ sch_a] _).
rewrite step_fupd_fupdN_S.
iMod "Hclose" as "_".
simpl. rewrite Heq.
destruct ((e::es)!!sch_a) as [chosen_e|] eqn:Hlookup; rewrite Hlookup; last first.
Expand All @@ -182,65 +194,66 @@ Section adequacy.
iApply ec_supply_eq; last done.
simpl. lra.
}
rewrite dmap_comp/dmap-dbind_assoc.
erewrite (distr_ext _ _); last first.
{ intros x. erewrite (dbind_ext_right _ _ (λ '(_,_,_), _)); last first.
- intros [[??]?].
by rewrite dret_id_left/=.
- done.
}
destruct sch_a as [|sch_a].
* (* step main thread *)
rewrite pgl_wp_unfold /pgl_wp_pre/=Heq.
rewrite pgl_wp_unfold /pgl_wp_pre. iSimpl in "Hwp". rewrite Heq.
iMod ("Hwp" with "[$]") as "Hlift".
replace (0+ε)%NNR with ε; [|apply nnreal_ext; simpl; lra].
iPoseProof
(glm_mono _ (λ '(e2, σ2, efs) ε', |={∅}▷=>^(S n)
⌜pgl (sch_exec sch n (sch_σ, (<[0%nat:=e2]>(e::es++efs), σ2))) φ ε'⌝)%I
with "[%] [-Hlift] Hlift") as "H"; first done.
{ simpl.
iIntros ([[??]?]?) "H!>!>".
iMod "H" as "(Hstate & Herr_auth & Hwp & Hwps')".
iApply ("IH").
iFrame. }
iModIntro. rewrite /dmap -!dbind_assoc.
erewrite dbind_ext_right; last first.
{ intros [[]]. rewrite !dret_id_left.
by instantiate (1 := (λ '(e',s,l), sch_exec sch n (sch_σ, (<[0%nat := e']> (e :: es ++ l), s)))).
iApply (state_step_coupl_erasure' with "[$Hlift]"); [done..|].
iIntros (σ2 ε2) "(%&%&%&%&%&%&%&H)".
iApply (step_fupdN_mono _ _ _ (⌜pgl _ _ (_+_)⌝)%I).
{ iPureIntro.
intros. eapply pgl_mon_grading; exact.
}
iApply glm_erasure; last first; try done.
replace chosen_e with e; first done.
simpl in Hlookup. by simplify_eq.
replace (chosen_e) with e; last by (simpl in Hlookup; simplify_eq).
iApply (pgl_dbind_adv' with "[][][][-]"); [done|naive_solver|done|].
iIntros ([[??]?]?).
iMod ("H" with "[//]") as "H".
simpl.
do 3 iModIntro.
iApply (state_step_coupl_erasure with "[$][-]").
iIntros (??) ">(?&?&?&?)".
iApply ("IH" with "[-]"). iFrame.
* (* step other threads*)
simpl in Hlookup.
apply elem_of_list_split_length in Hlookup as (l1 & l2 & -> & ->).
iDestruct "Hwps" as "[Hl1 [Hwp' Hl2]]".
rewrite (pgl_wp_unfold _ _ chosen_e)/pgl_wp_pre/=.
rewrite (pgl_wp_unfold _ _ chosen_e)/pgl_wp_pre.
iSimpl in "Hwp'".
rewrite Hcheckval.
iMod ("Hwp'" with "[$]") as "Hlift".
replace (0+ε)%NNR with ε; [|apply nnreal_ext; simpl; lra].
iPoseProof
(glm_mono _ (λ '(e2, σ2, efs) ε', |={∅}▷=>^(S n)
⌜pgl (sch_exec sch n (sch_σ, (<[(S (length l1))%nat:=e2]>(e::(l1++chosen_e::l2)++efs), σ2))) φ ε'⌝)%I
with "[%] [-Hlift] Hlift") as "H"; first done.
iApply (state_step_coupl_erasure' _ e _ chosen_e with "[$]"); [|done..|].
{ simpl.
iIntros ([[??]?]?) "H!>!>".
iMod "H" as "(Hstate & Herr_auth & Hwp' & Hwps')".
iApply ("IH").
iFrame.
rewrite -app_assoc.
rewrite insert_app_r_alt; last lia.
replace (_-_)%nat with 0%nat by lia. simpl.
repeat iApply big_sepL_app; iFrame.
rewrite lookup_app_r//.
by replace (_-_)%nat with 0%nat by lia.
}
iModIntro.
rewrite /dmap -!dbind_assoc.
erewrite dbind_ext_right; last first.
{ intros [[]]. rewrite !dret_id_left.
instantiate (1 := (λ '(e',s,l), sch_exec sch n (sch_σ, (<[S (length l1):=e']> (e :: (l1 ++ chosen_e :: l2) ++ l), s)))). simpl.
rewrite -insert_app_l; first done.
rewrite app_length. simpl; lia.
iIntros (σ2 ε2) "(%&%&%&%&%&%&%&H)".
iApply (step_fupdN_mono _ _ _ (⌜pgl _ _ (_+_)⌝)%I).
{ iPureIntro.
intros. eapply pgl_mon_grading; exact.
}
iApply glm_erasure; try done.
simpl. rewrite lookup_app_r; last lia.
iApply (pgl_dbind_adv' with "[][][][-]"); [done|naive_solver|done|].
iIntros ([[??]?]?).
iMod ("H" with "[//]") as "H".
simpl.
do 3 iModIntro.
iApply (state_step_coupl_erasure with "[$][-]").
iIntros (??) ">(?&?&?&?)".
iApply ("IH" with "[-]"). iFrame.
rewrite insert_app_r_alt//.
replace (_-_)%nat with 0%nat by lia.
done.
simpl.
iFrame.
Qed.


End adequacy.

Class conerisGpreS Σ := ConerisGpreS {
Expand Down
Loading
Loading