diff --git a/Iris/Iris/ProgramLogic/AbstractEctxLangCompleteness.lean b/Iris/Iris/ProgramLogic/AbstractEctxLangCompleteness.lean new file mode 100644 index 000000000..39ed20de6 --- /dev/null +++ b/Iris/Iris/ProgramLogic/AbstractEctxLangCompleteness.lean @@ -0,0 +1,148 @@ +/- +Copyright (c) 2026 Markus de Medeiros. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Iris.Algebra +public import Iris.BI +public import Iris.ProofMode +public import Iris.ProgramLogic.Language +public import Iris.ProgramLogic.EctxLanguage +public import Iris.ProgramLogic.Adequacy +public import Iris.ProgramLogic.ThreadPool +public import Iris.ProgramLogic.AbstractWeakestPre +public import Iris.ProgramLogic.AbstractLangCompleteness +public import Iris.Instances.Lib.Invariants +public import Iris.Instances.Lib.CInvariants +public import Iris.Instances.Lib.GhostMap +public import Iris.Std.FromMathlib + +namespace Iris.ProgramLogic + +open Iris Iris.BI Iris.Algebra Std FromMathlib +open Iris.ProgramLogic.PrimStep +open Language Language.Notation + +@[expose] public section + +section AbstractEctxCompleteness + +variable {Expr State Obs Val Ectx : Type _} +variable [EctxLanguage Expr Ectx State Obs Val] +variable {GF : BundledGFunctors} {HLC : HasLC} [IrisGS_gen HLC Expr GF] +variable {H : Type _ → Type _} [LawfulFiniteMap H Nat] +variable [TI : TpinvGS GF Expr H] + +public def ectxLangCompletenessStmt (wp : AbstractWP Expr Val GF) + (heap_inv : List Expr → State → IProp GF) (n : Nat) (C : List Expr) (e₁ : Expr) (σ : State) + (K : Ectx) (E : CoPset) : IProp GF := iprop% + ⌜BaseStep.Reducible (e₁, σ)⌝ -∗ + (n ↪thread (EvContext.fill K e₁)) -∗ + heap_inv C σ ∗ tpInv C ∗ ⌜cfgSafe (C, σ)⌝ ={E}=∗ + ((⌜Atomic .WeaklyAtomic e₁⌝ ∗ + (∀ Φ, + (▷ ∀ κ v₂ σ' efs, + ⌜PrimStep.primStep (e₁, σ) κ (ToVal.ofVal v₂, σ', efs)⌝ -∗ + isThread n (.own 1) (EvContext.fill K e₁) -∗ + tpInv C ==∗ + (heap_inv ((C.set n (EvContext.fill K (ToVal.ofVal v₂))) ++ efs) σ' -∗ Φ v₂) ∗ + [∗list] _i ↦ etp ∈ efs, wp ⊤ etp (fun (_ : Val) => iprop(True))) -∗ + wp E e₁ Φ)) + ∨ + (heap_inv C σ ∗ tpInv C ∗ ∀ Ψ, + (▷ ∀ e₂ efs, + (∀ σ₁ C₁, + heap_inv C₁ σ₁ ∗ tpInv C₁ ∗ ⌜cfgSafe (C₁, σ₁)⌝ ={E}=∗ + ∃ κ σ₁', + ⌜PrimSteps e₁ σ₁ κ e₂ σ₁' efs⌝ ∗ + isThread n (.own 1) (EvContext.fill K e₁) ∗ + tpInv C₁ ∗ + heap_inv ((C₁.set n (EvContext.fill K e₂)) ++ efs) σ₁') ={⊤}=∗ + wp ⊤ e₂ Ψ ∗ + ([∗list] _j ↦ etp ∈ efs, wp ⊤ etp (fun (_ : Val) => iprop(True)))) -∗ + wp ⊤ e₁ Ψ)) + +public class AbstractEctxLangCompletenessGen + (wp : AbstractWP Expr Val GF) [BindAbstractWP wp] where + heap_inv : List Expr → State → IProp GF + heap_inv_timeless (C : List Expr) (σ : State) : Timeless (heap_inv C σ) + ectx_lang_completeness (n : Nat) (C : List Expr) (e₁ : Expr) (σ : State) (K : Ectx) (E : CoPset) : + ⊢ ectxLangCompletenessStmt wp heap_inv n C e₁ σ K E + +attribute [instance] AbstractEctxLangCompletenessGen.heap_inv_timeless + +end AbstractEctxCompleteness + +/-! ### Lifting the ectx-level soundness equation to the prim level. -/ + +section Lifting + +variable {Expr State Obs Val Ectx : Type _} +variable [EctxLanguage Expr Ectx State Obs Val] +variable {GF : BundledGFunctors} {HLC : HasLC} [IrisGS_gen HLC Expr GF] +variable {H : Type _ → Type _} [LawfulFiniteMap H Nat] +variable [TI : TpinvGS GF Expr H] +variable {wp : AbstractWP Expr Val GF} +variable [BWP : BindAbstractWP wp] +variable [AEC : AbstractEctxLangCompletenessGen wp] + +theorem weakestpre_ectx_to_prim_completeness (n : Nat) (C : List Expr) (e₁ : Expr) + (σ : State) (E : CoPset) : + ⊢ abstractECTXLangComplete (TI := TI) wp AEC.heap_inv n C e₁ σ E := by + iintro %Hred Htok ⟨Hheap, Htp, %Hsafe⟩ + obtain ⟨κ, e', σ', efs, hstep⟩ := Hred + obtain @⟨e₁', e₂', K, Hbase⟩ := hstep + have Hbred : BaseStep.Reducible (e₁', σ) := ⟨κ, e₂', σ', efs, Hbase⟩ + have key := AEC.ectx_lang_completeness n C e₁' σ K E + unfold ectxLangCompletenessStmt at key + imod key $$ %Hbred Htok [Hheap Htp] with (⟨%Hatom, HH⟩ | ⟨Hheap, Htp, HH⟩) + · iframe Hheap Htp %Hsafe + · clear key + imodintro + ileft + iexists (fill (Expr := Expr) K), e₁' + have Hctx : Context (fill (Expr := Expr) K) := inferInstance + have Heq : fill (Expr := Expr) K e₁' = fill (Expr := Expr) K e₁' := rfl + have Hnv : ToVal.toVal e₁' = none := EctxLanguage.val_stuck Hbase + iframe %Hctx %Heq %Hnv %Hatom + iintro %Ψ Hpre + iapply HH $$ Hpre + · clear key + imodintro + iright + iframe Hheap Htp + iintro %Ψ Hc + iapply (BWP.wp_bind (K := fill (Expr := Expr) K) (e := e₁') (Φ := Ψ)).1 + iapply HH + inext + iintro %e₂ %efs H + ihave Hprem : iprop(∀ σ₁ C₁, + AEC.heap_inv C₁ σ₁ ∗ tpInv C₁ ∗ ⌜cfgSafe (C₁, σ₁)⌝ ={E}=∗ + ∃ κ σ₁', ⌜PrimSteps (fill (Expr := Expr) K e₁') σ₁ κ (fill (Expr := Expr) K e₂) σ₁' efs⌝ ∗ + (n ↪thread fill (Expr := Expr) K e₁') ∗ tpInv C₁ ∗ + AEC.heap_inv (C₁.set n (fill (Expr := Expr) K e₂) ++ efs) σ₁') $$ [H] + · iintro %σ₁ %C₁ ⟨Hi, Htp1, %Hs⟩ + imod H $$ [Hi Htp1] with ⟨%κ', %σ₁', %Hps, Htok2, Htp1', Hhp⟩ + · iframe Hi Htp1 %Hs + imodintro + iexists κ', σ₁' + iframe Htok2 Htp1' Hhp + ipureintro + exact Hps.fill + imod Hc $$ Hprem with ⟨Hwp, Hlist⟩ + imodintro + iframe + iapply (BWP.wp_bind (K := fill (Expr := Expr) K) (e := e₂) (Φ := Ψ)).2 $$ Hwp + +instance abstract_ectx_to_completeness : + AbstractLangCompletenessGen wp where + heap_inv := AEC.heap_inv + heap_inv_timeless := AEC.heap_inv_timeless + lang_completeness {n C e₁ σ E} := weakestpre_ectx_to_prim_completeness n C e₁ σ E + +end Lifting + +end + +end Iris.ProgramLogic diff --git a/Iris/Iris/ProgramLogic/AbstractLangCompleteness.lean b/Iris/Iris/ProgramLogic/AbstractLangCompleteness.lean new file mode 100644 index 000000000..dfbe5ecab --- /dev/null +++ b/Iris/Iris/ProgramLogic/AbstractLangCompleteness.lean @@ -0,0 +1,400 @@ +/- +Copyright (c) 2026 Markus de Medeiros. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Iris.Algebra +public import Iris.BI +public import Iris.ProofMode +public import Iris.ProgramLogic.Language +public import Iris.ProgramLogic.Adequacy +public import Iris.ProgramLogic.ThreadPool +public import Iris.ProgramLogic.AbstractWeakestPre +public import Iris.Instances.Lib.Invariants +public import Iris.Instances.Lib.CInvariants +public import Iris.Instances.Lib.GhostMap +public import Iris.Std.FromMathlib + +namespace Iris.ProgramLogic + +open Iris Iris.BI Iris.Algebra Std FromMathlib +open Iris.ProgramLogic.PrimStep +open Language Language.Notation + +@[expose] public section + +section AbstractCompleteness + +variable {Expr State Obs Val : Type _} [Language Expr State Obs Val] +variable {GF : BundledGFunctors} {HLC : HasLC} [IrisGS_gen HLC Expr GF] +variable {H : Type _ → Type _} [LawfulFiniteMap H Nat] +variable [TI : TpinvGS GF Expr H] + +public abbrev abstractECTXLangComplete (wp : AbstractWP Expr Val GF) (I : List Expr → State → IProp GF) + (n : Nat) (C : List Expr) (e₁ : Expr) (σ : State) (E : CoPset) : + IProp GF := iprop% + ⌜PrimStep.Reducible (e₁, σ)⌝ -∗ (n ↪thread e₁) -∗ I C σ ∗ tpInv C ∗ ⌜cfgSafe (C, σ)⌝ ={E}=∗ + ((∃ (K : Expr → Expr) (e₁' : Expr), + ⌜Context K⌝ ∗ ⌜e₁ = K e₁'⌝ ∗ ⌜ToVal.toVal e₁' = none⌝ ∗ ⌜Atomic .WeaklyAtomic e₁'⌝ ∗ + ∀ Ψ, + (▷ ∀ κ v₂ σ' efs, + ⌜PrimStep.primStep (e₁', σ) κ ((ToVal.ofVal v₂ : Expr), σ', efs)⌝ -∗ + (n ↪thread e₁) -∗ + tpInv C ==∗ + (I ((C.set n (K (ToVal.ofVal v₂))) ++ efs) σ' -∗ Ψ v₂) ∗ + [∗list] _i ↦ etp ∈ efs, wp ⊤ etp (fun (_ : Val) => iprop% True)) -∗ + wp E e₁' Ψ) ∨ + (I C σ ∗ tpInv C ∗ ∀ Ψ, + (▷ ∀ e₂ efs, + (∀ σ₁ C₁, I C₁ σ₁ ∗ tpInv C₁ ∗ ⌜cfgSafe (C₁, σ₁)⌝ ={E}=∗ + ∃ κ σ₁', + ⌜PrimSteps e₁ σ₁ κ e₂ σ₁' efs⌝ ∗ (n ↪thread e₁) ∗ tpInv C₁ ∗ + I ((C₁.set n e₂) ++ efs) σ₁') ={⊤}=∗ + wp ⊤ e₂ Ψ ∗ ([∗list] _j ↦ etp ∈ efs, wp ⊤ etp (fun (_ : Val) => iprop% True))) -∗ + wp ⊤ e₁ Ψ)) + +/-- A weakest precondition for a Language is complete -/ +public class AbstractLangCompletenessGen + (wp : AbstractWP Expr Val GF) [LawfulAbstractWP wp] where + heap_inv : List Expr → State → IProp GF + heap_inv_timeless (C : List Expr) (σ : State) : Timeless (heap_inv C σ) + lang_completeness {n C e₁ σ E} : ⊢ abstractECTXLangComplete wp heap_inv n C e₁ σ E + +attribute [instance] AbstractLangCompletenessGen.heap_inv_timeless + +end AbstractCompleteness + +section Completeness + +variable {Expr State Obs Val : Type _} [Language Expr State Obs Val] +variable {GF : BundledGFunctors} {HLC : HasLC} [IrisGS_gen HLC Expr GF] +variable {H : Type _ → Type _} [LawfulFiniteMap H Nat] +variable [TI : TpinvGS GF Expr H] +variable {wp : AbstractWP Expr Val GF} +variable [LWP : LawfulAbstractWP wp] [IAO : InvOpenAbstractWP wp] +variable [ACG : AbstractLangCompletenessGen wp] +variable [CInvG GF] + +/-- Namespace under which the completeness invariant lives. -/ +public def completenessN : Namespace := nroot .@ (1 : Pos) + +public def cfgInv (Cini : List Expr × State) (f : Forking) : IProp GF := iprop% + ∃ cfg : List Expr × State, + ACG.heap_inv cfg.1 cfg.2 ∗ tpInv cfg.1 ∗ ⌜cfgSafeForking cfg f⌝ ∗ ⌜Cini -·->ₜₚ* cfg⌝ + +instance cfgInv_timeless (Cini : List Expr × State) (f : Forking) : + Timeless (cfgInv (wp := wp) Cini f) := by + unfold cfgInv; infer_instance + +public def isCcfg (Cini : List Expr × State) (f : Forking) (γ : GName) : IProp GF := + CancelableInvariant.cinv completenessN γ (cfgInv (wp := wp) Cini f) + +instance isCcfg_persistent (Cini : List Expr × State) (f : Forking) (γ : GName) : + Persistent (isCcfg (wp := wp) Cini f γ : IProp GF) := by + unfold isCcfg; infer_instance + +omit [CInvG GF] in +theorem bigSepL_const_congr {α β : Type _} {P : IProp GF} {l1 : List α} {l2 : List β} + (h : l1.length = l2.length) : ([∗list] _x ∈ l1, P) ⊣⊢ ([∗list] _x ∈ l2, P) := + BigSepL.bigSepL_replicate.symm.trans (.trans (h ▸ .rfl) (BigSepL.bigSepL_replicate)) + +theorem own_divide_forks {α : Type _} (γ : GName) (qc : Qp) (l : List α) : + CancelableInvariant.own (GF := GF) γ qc ⊢ + CancelableInvariant.own γ (qc.divide_even (l.length + 1) (Nat.succ_pos _) : Qp) ∗ + ([∗list] _x ∈ l, + CancelableInvariant.own γ (qc.divide_even (l.length + 1) (Nat.succ_pos _) : Qp)) := by + have h := fractional_divide_equal + (Φ := fun p : Qp => CancelableInvariant.own (GF := GF) γ p) qc l.length + rw [List.replicate_succ'] at h + refine h.trans ((BigSepL.bigSepL_snoc).1.trans + (sep_comm.1.trans (sep_mono_right (bigSepL_const_congr (by simp)).1))) + +theorem qp_div_ofPNat_succ_nil {α : Type _} (qc : Qp) {l : List α} (h : l = []) : + qc.divide_even (l.length + 1) (Nat.succ_pos _) = qc := by + simp only [h, List.length_nil, Nat.zero_add]; grind + +theorem weakestpre_completeness (Cini : List Expr × State) (f : Forking) (γ : GName) (q : Qp) + (n : Nat) (e : Expr) : + isCcfg (TI := TI) (wp := wp) Cini f γ -∗ + CancelableInvariant.own γ q -∗ + isThread (TI := TI) n (.own 1) e -∗ + wp ⊤ e (fun v => iprop% + isThread (TI := TI) n (.own 1) (ToVal.ofVal v) ∗ + ∃ q' : Qp, CancelableInvariant.own γ q' ∗ ⌜f = .doesNotFork → q = q'⌝) := by + iintro #Hinv + iloeb as IH generalizing %q %n %e + iintro Hq He + have Hn : nclose completenessN ⊆ ⊤ := fun _ _ => CoPset.mem_full + iapply IAO.inv_open_maybe (E₂ := ⊤ \ nclose completenessN) _ _ _ Std.LawfulSet.diff_subset_left + unfold isCcfg + imod CancelableInvariant.acc Hn $$ [$] [$] with ⟨>Hinv2, Hq, Hclose⟩ + unfold cfgInv + icases Hinv2 with ⟨%cfg, Hheap, HtpInv, %Hx⟩ + rcases Hx with ⟨Hsafe, Hreach⟩ + ihave %Hlu := tpInv_lookup $$ [$] [$] + have ⟨HnotStuck, Hforking⟩ := Hsafe .refl + rcases HnotStuck (List.mem_of_getElem? Hlu) with Hv|HnotStuck' + · iclear Hinv + replace ⟨v, Hv⟩ := Option.isSome_iff_exists.mp Hv + obtain rfl := (coe_of_toVal_eq_some Hv).symm; clear Hv + imodintro + ileft + iexists id, v + have Hframe1 : Context (Expr := Expr) id := by infer_instance + have Hframe2 : (↑v : Expr) = id ↑v := rfl + have Hframe3 : Atomic Atomicity.WeaklyAtomic (↑v : Expr) := val_atomic + iframe %Hframe1 %Hframe2 %Hframe3 + clear Hframe1 Hframe2 Hframe3 + simp only [id_eq] + iapply LWP.wp_value + imodintro + imod Hclose $$ [HtpInv Hheap] with - + · inext + iexists cfg + iframe Hheap HtpInv %Hreach %Hsafe + · imodintro + iapply LWP.wp_value + imodintro + iframe + iexists q + iframe + ipureintro + grind + · imod AbstractLangCompletenessGen.lang_completeness $$ %HnotStuck' He [Hheap HtpInv] + with (⟨%K, %e₁, %Hctx, %Heq, %Hval, %Hatom, H⟩|⟨Hheap, Htpinv, H⟩) + · have aux : cfgSafe (cfg.fst, cfg.snd) := cfgSafe_of_cfgSafeForking Hsafe + iframe %aux Hheap HtpInv + · iclear Hinv + imodintro + ileft + iexists K, e₁ + iframe %Hctx %Heq %Hatom + iapply H + iintro !> %κ %v₂ %σ₂' %Hefs %Hbase He HtpInv + icases own_divide_forks γ q Hefs $$ Hq with ⟨Hq, Hefsfrac⟩ + imod (tpInv_update cfg.fst n e (K ↑v₂)) $$ HtpInv He with ⟨HtpInv, He⟩ + imod (tpInv_new_threads Hefs (cfg.fst.set n (K ↑v₂))) $$ HtpInv with ⟨HtpInv, Hefs_threads⟩ + imodintro + isplitl [Hclose Hq He HtpInv] + · iintro Hheap + have Hprim : (e, cfg.snd) -<κ>-> (K ↑v₂, σ₂', Hefs) := Heq ▸ Context.primStep_fill Hbase + obtain ⟨Hsafe', Hnf⟩ := cfg_safeStep Hsafe Hlu Hprim + imod Hclose $$ [Hheap HtpInv] with - + · inext + iexists (cfg.fst.set n (K ↑v₂) ++ Hefs, σ₂') + iframe Hheap HtpInv + ipureintro + exact ⟨Hsafe', Hreach.tail ⟨κ, cfg_step Hlu Hprim⟩⟩ + imodintro + iapply LWP.wp_wand $$ [Hq He] + · iapply IH $$ Hq He + iintro %v ⟨Hthread, %q', Hq', %Hfork⟩ + iframe Hthread + iexists q' + iframe Hq' + ipureintro + intro hnf + rw [← Hfork hnf] + congr 1 + exact (qp_div_ofPNat_succ_nil q (Hnf hnf)).symm + · ihave Hcomb : iprop([∗list] k ↦ e' ∈ Hefs, + (((cfg.fst.set n (K ↑v₂)).length + k) ↪thread e') ∗ + CancelableInvariant.own γ + (q.divide_even (Hefs.length + 1) (Nat.succ_pos _) : Qp)) + $$ [Hefs_threads Hefsfrac] + · iapply (BigSepL.bigSepL_sep_eqv).2 + iframe Hefs_threads Hefsfrac + iapply BigSepL.bigSepL_impl $$ Hcomb + iintro !> %k %e' %_ ⟨He, Hq⟩ + iapply LWP.wp_wand $$ [Hq He] + · iapply IH $$ Hq He + iintro %v _ + ipureintro + trivial + · imodintro + iright + imod Hclose $$ [Hheap Htpinv] with - + · inext + iexists cfg + -- FIXME: needs a better proof of this + have Hframe : cfgSafeForking cfg f := @«inferInstanceAs» (cfgSafeForking cfg f) Hsafe + iframe Hheap Htpinv %Hreach %Hframe + imodintro + iapply H + inext + iintro %e₂ %efs H + imod CancelableInvariant.acc Hn $$ [$] [$] with ⟨>Hinv2, Hq, Hclose⟩ + icases Hinv2 with ⟨%cfg2, Hheap, Htpinv, %Hsafe2, %Hreach2⟩ + imod H $$ [Hheap Htpinv] with ⟨%κ, %σ1', %Hprim, He, Htpinv, Hhp⟩ + · iframe Hheap Htpinv + ipureintro + exact cfgSafe_of_cfgSafeForking Hsafe2 + icases own_divide_forks γ q efs $$ Hq with ⟨Hq, Hefsfrac⟩ + ihave %Hlu2 := tpInv_lookup $$ Htpinv He + obtain ⟨Hsafe2', Hforking2⟩ := cfg_safeSteps Hsafe2 Hlu2 Hprim + imod (tpInv_update cfg2.fst n e e₂) $$ Htpinv He with ⟨Htpinv, He⟩ + imod (tpInv_new_threads efs (cfg2.fst.set n e₂)) $$ Htpinv with ⟨Htpinv, Hefs_threads⟩ + imod Hclose $$ [Hhp Htpinv] with - + · inext + iexists (cfg2.fst.set n e₂ ++ efs, σ1') + iframe Hhp Htpinv + ipureintro + exact ⟨Hsafe2', Hreach2.trans (cfg_steps Hlu2 Hprim)⟩ + imodintro + isplitl [Hq He] + · iapply LWP.wp_wand $$ [Hq He] + · iapply IH $$ Hq He + iintro %v ⟨Hthread, %q', Hq', %Hfork⟩ + iframe Hthread + iexists q' + iframe Hq' + ipureintro + intro hnf + rw [← Hfork hnf] + congr 1 + exact (qp_div_ofPNat_succ_nil q (Hforking2 hnf)).symm + · ihave Hcomb : iprop([∗list] k ↦ e' ∈ efs, + (((cfg2.fst.set n e₂).length + k) ↪thread e') ∗ + CancelableInvariant.own γ + (q.divide_even (efs.length + 1) (Nat.succ_pos _) : Qp)) + $$ [Hefs_threads Hefsfrac] + · iapply (BigSepL.bigSepL_sep_eqv).2 + iframe Hefs_threads Hefsfrac + iapply BigSepL.bigSepL_impl $$ Hcomb + iintro !> %k %e' %_ ⟨He, Hq⟩ + iapply LWP.wp_wand $$ [Hq He] + · iapply IH $$ Hq He + iintro %v _ + ipureintro + trivial + +-- Here + +/-- `adequate` gives a WP with a pure postcondition from an `adequate` fact. -/ +theorem weakestpre_sem_completeness (e : Expr) (σ : State) (φ : Val → Prop) + (Hade : adequate .NotStuck e σ (fun v _ => φ v)) : + ⊢ tpInvIni (TI := TI) -∗ + ACG.heap_inv [e] σ -∗ + wp ⊤ e (fun v => iprop% ⌜φ v⌝) := by + have Hsafe0 : cfgSafeForking ([e], σ) .doesFork := + fun {C₂} hreach => + ⟨fun {e2} hmem => Hade.adequate_not_stuck _ _ e2 rfl hreach hmem, + fun hf => Forking.noConfusion hf⟩ + iintro Hini Hheap + iapply LWP.fupd_wp + imod (tpInv_set [e]) $$ Hini with ⟨Hauth, Hfrags⟩ + imod (CancelableInvariant.alloc ⊤ completenessN + (cfgInv (wp := wp) ([e], σ) .doesFork)) $$ [Hauth Hheap] with ⟨%γ, #Hinv, Hq⟩ + · inext + unfold cfgInv + iexists ([e], σ) + iframe Hheap Hauth %Hsafe0 + ipureintro + exact .refl + have Hn0 : (completenessN : CoPset) ⊆ ⊤ := fun _ _ => CoPset.mem_full + ihave He0 := (Iris.BI.BigSepL.bigSepL_singleton + (Φ := fun n e' => isThread (TI := TI) n (.own 1) e') (x := e)).1 $$ Hfrags + imodintro + iapply LWP.wp_fupd + ihave Hccfg : iprop(isCcfg (wp := wp) ([e], σ) .doesFork γ) $$ [Hinv] + · unfold isCcfg; iexact Hinv + ihave Hwp := weakestpre_completeness (wp := wp) ([e], σ) .doesFork γ (One.one : Qp) 0 e + $$ Hccfg Hq He0 + iapply LWP.wp_wand $$ Hwp + iintro %v ⟨Hv, %q', Hq', _⟩ + imod (CancelableInvariant.acc (E := ⊤) (N := completenessN) (γ := γ) (p := q') + (P := cfgInv (wp := wp) ([e], σ) .doesFork) Hn0) $$ Hinv Hq' with ⟨>Hinv2, Hq', Hclose2⟩ + unfold cfgInv + icases Hinv2 with ⟨%cfg, Hheap, Htpinv, %Hsafe2, %Hreach2⟩ + ihave %Hlu := tpInv_lookup $$ Htpinv Hv + imod Hclose2 $$ [Hheap Htpinv] with - + · inext + iexists cfg + iframe Hheap Htpinv %Hsafe2 %Hreach2 + imodintro + ipureintro + obtain ⟨tp2, σ2⟩ := cfg + rcases tp2 with _ | ⟨hd, rest⟩ + · simp at Hlu + · simp only [List.getElem?_cons_zero, Option.some.injEq] at Hlu + subst Hlu + exact Hade.adequate_result rest σ2 v Hreach2 + +theorem weakestpre_sem_completeness_nofork_strong + (e : Expr) (σ : State) (φ : Val → State → Prop) + (Hade : AdequateNoFork .NotStuck e σ (fun v σ' => φ v σ')) : + ⊢ tpInvIni (TI := TI) -∗ + ACG.heap_inv [e] σ -∗ + wp ⊤ e (fun v => + iprop% ∃ σ' : State, + tpInv (TI := TI) [ToVal.ofVal v] ∗ + isThread (TI := TI) 0 (.own 1) (ToVal.ofVal v) ∗ + ACG.heap_inv [ToVal.ofVal v] σ' ∗ + ⌜φ v σ'⌝) := by + have Hsafe0 : cfgSafeForking ([e], σ) .doesNotFork := by + rintro ⟨tp2, σ2⟩ hreach + refine ⟨fun {e2} hmem => Hade.not_stuck rfl hreach hmem, ?_⟩ + intro _ e2 hmem e' σ' κ efs hstep + exact adequateNoFork_efs_nil Hade hreach hmem hstep + have Hn0 : (completenessN : CoPset) ⊆ ⊤ := fun _ _ => CoPset.mem_full + iintro Hini Hheap + iapply LWP.fupd_wp + imod (tpInv_set [e]) $$ Hini with ⟨Hauth, Hfrags⟩ + imod (CancelableInvariant.alloc ⊤ completenessN + (cfgInv (wp := wp) ([e], σ) .doesNotFork)) $$ [Hauth Hheap] with ⟨%γ, #Hinv, Hq⟩ + · inext + unfold cfgInv + iexists ([e], σ) + iframe Hheap Hauth %Hsafe0 + ipureintro + exact .refl + ihave He0 := (Iris.BI.BigSepL.bigSepL_singleton + (Φ := fun n e' => isThread (TI := TI) n (.own 1) e') (x := e)).1 $$ Hfrags + imodintro + iapply LWP.wp_fupd + ihave Hccfg : iprop(isCcfg (wp := wp) ([e], σ) .doesNotFork γ) $$ [Hinv] + · unfold isCcfg; iexact Hinv + ihave Hwp := weakestpre_completeness (wp := wp) ([e], σ) .doesNotFork γ (One.one : Qp) 0 e + $$ Hccfg Hq He0 + iapply LWP.wp_wand $$ Hwp + iintro %v ⟨Hv, %q', Hq', %His1⟩ + obtain rfl := His1 rfl + imod (CancelableInvariant.cancel ⊤ completenessN γ + (cfgInv (wp := wp) ([e], σ) .doesNotFork) Hn0) $$ Hinv Hq' with >Hinv2 + unfold cfgInv + icases Hinv2 with ⟨%cfg, Hheap, Htpinv, %Hsafe2, %Hreach2⟩ + ihave %Hlu := tpInv_lookup $$ Htpinv Hv + imodintro + obtain ⟨tp2, σ2⟩ := cfg + rcases tp2 with _ | ⟨hd, rest⟩ + · simp at Hlu + · simp only [List.getElem?_cons_zero, Option.some.injEq] at Hlu + subst Hlu + have hlen := Hade.no_fork Hreach2 + rw [List.length_cons] at hlen + obtain rfl := List.length_eq_zero_iff.mp (by omega : rest.length = 0) + iexists σ2 + iframe Htpinv Hv Hheap + ipureintro + exact Hade.result Hreach2 + +theorem weakestpre_sem_completeness_nofork + (e : Expr) (σ : State) (φ : Val → State → Prop) + (Hade : AdequateNoFork .NotStuck e σ (fun v σ' => φ v σ')) : + ⊢ tpInvIni (TI := TI) -∗ + ACG.heap_inv [e] σ -∗ + wp ⊤ e (fun v => + iprop% ∃ σ' : State, ACG.heap_inv [ToVal.ofVal v] σ' ∗ ⌜φ v σ'⌝) := by + iintro Hini Hheap + ihave Hw := weakestpre_sem_completeness_nofork_strong (wp := wp) e σ φ Hade $$ Hini Hheap + iapply LWP.wp_wand $$ Hw + iintro %v ⟨%σ2, _, _, Hh, Hphi⟩ + iexists σ2 + iframe + +end Completeness + +end + +end Iris.ProgramLogic diff --git a/Iris/Iris/ProgramLogic/Adequacy.lean b/Iris/Iris/ProgramLogic/Adequacy.lean index 9cd153298..19b451411 100644 --- a/Iris/Iris/ProgramLogic/Adequacy.lean +++ b/Iris/Iris/ProgramLogic/Adequacy.lean @@ -234,8 +234,7 @@ theorem wp_strong_adequacy_gen [InvGpreS GF] (s : Stuckness) (es : List Expr) ( abbrev wp_strong_adequacy := @wp_strong_adequacy_gen .hasLC @[rocq_alias adequate] -structure adequate (s : Stuckness) (e1 : Expr) (σ1 : State) - (φ : Val → State → Prop) : Prop where +structure adequate (s : Stuckness) (e1 : Expr) (σ1 : State) (φ : Val → State → Prop) : Prop where adequate_result : ∀ (t2 : List Expr) (σ2 : State) (v2 : Val), ([e1], σ1) -·->ₜₚ* (ToVal.ofVal v2 :: t2, σ2) → φ v2 σ2 @@ -243,6 +242,11 @@ structure adequate (s : Stuckness) (e1 : Expr) (σ1 : State) ∀ (t2 : List Expr) (σ2 : State) (e2 : Expr), s = .NotStuck → ([e1], σ1) -·->ₜₚ* (t2, σ2) → e2 ∈ t2 → NotStuck (e2, σ2) +structure AdequateNoFork (s : Stuckness) (e₁ : Expr) (σ₁ : State) (φ : Val → State → Prop) : Prop where + no_fork {t₂ σ₂} : ([e₁], σ₁) -·->ₜₚ* (t₂, σ₂) → t₂.length = 1 + result {t₂ σ₂ v₂} : ([e₁], σ₁) -·->ₜₚ* (ToVal.ofVal v₂ :: t₂, σ₂) → φ v₂ σ₂ + not_stuck {t₂ σ₂ e₂} : s = .NotStuck → ([e₁], σ₁) -·->ₜₚ* (t₂, σ₂) → e₂ ∈ t₂ → NotStuck ⟨e₂, σ₂⟩ + @[rocq_alias adequate_alt] theorem adequate_alt (s : Stuckness) (e1 : Expr) (σ1 : State) (φ : Val → State → Prop) : @@ -274,6 +278,25 @@ theorem adequate_tp_safe (e1 : Expr) (t2 : List Expr) (σ1 σ2 : State) obtain ⟨t2', t2'', rfl⟩ := List.append_of_mem hel exact .inr ⟨t2' ++ e3 :: t2'' ++ efs, σ3, obs, Language.Step.of_primStep hstep⟩ +theorem adequateNoFork_step {e₁ e₂ : Expr} {σ₁ σ₂ s Q} + (Hstep : ([e₁], σ₁) -·->ₜₚ* ([e₂], σ₂)) (H : AdequateNoFork s e₁ σ₁ Q) : + AdequateNoFork s e₂ σ₂ Q := + ⟨(H.no_fork <| Hstep.trans ·), (H.result <| Hstep.trans ·), (H.not_stuck · <| Hstep.trans ·)⟩ + +theorem adequateNoFork_primStep {e₁ e₂ : Expr} {κ σ₁ σ₂ s Q} + (Hstep : (e₁, σ₁) -<κ>-> (e₂, σ₂, [])) + (H : AdequateNoFork s e₁ σ₁ Q) : AdequateNoFork s e₂ σ₂ Q := + adequateNoFork_step (.tail .refl ⟨κ, .of_primStep Hstep (t₁ := []) (t₂ := [])⟩) H + +theorem adequateNoFork_efs_nil {e₁ : Expr} {σ₁ s φ} (H : AdequateNoFork s e₁ σ₁ φ) + {t₂ σ₂ e₂} (Hsteps : ([e₁], σ₁) -·->ₜₚ* (t₂, σ₂)) (Hmem : e₂ ∈ t₂) + {κ e' σ' efs} (Hstep : (e₂, σ₂) -<κ>-> (e', σ', efs)) : efs = [] := by + obtain ⟨t₂a, t₂b, rfl⟩ := List.append_of_mem Hmem + have Hlen := H.no_fork (Hsteps.tail ⟨κ, .atomic Hstep t₂a t₂b⟩) + refine List.length_eq_zero_iff.mp ?_ + simp [List.length_append] at Hlen + omega + omit iG in @[rocq_alias wp_adequacy_gen] theorem wp_adequacy_gen [InvGpreS GF] (s : Stuckness) (e : Expr) (σ : State) (φ : Val → Prop) diff --git a/Iris/Iris/ProgramLogic/ThreadPool.lean b/Iris/Iris/ProgramLogic/ThreadPool.lean new file mode 100644 index 000000000..d6d6436a0 --- /dev/null +++ b/Iris/Iris/ProgramLogic/ThreadPool.lean @@ -0,0 +1,268 @@ +/- +Copyright (c) 2026 Markus de Medeiros. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Iris.ProgramLogic.Language +public import Iris.ProgramLogic.EctxLanguage +public import Iris.ProgramLogic.Adequacy +public import Iris.Instances.Lib.GhostMap +public import Iris.Std.FromMathlib +public import Batteries.Data.List.Lemmas + +namespace Iris.ProgramLogic + +open Iris.ProgramLogic.PrimStep +open Language Language.Notation Relation FromMathlib FromMathlib.Relation.TransGen + +@[expose] public section + +variable {Expr State Obs Val : Type _} [Λ : Language Expr State Obs Val] + +/-! ### Multi-step prim reduction on a single thread -/ + +/-- Transitive closure of `primStep` with accumulated observations and forks. -/ +inductive PrimSteps : Expr → State → List Obs → Expr → State → List Expr → Prop where + | once {e₁ σ₁ κ e₂ σ₂ efs} : + (e₁, σ₁) -<κ>-> (e₂, σ₂, efs) → + PrimSteps e₁ σ₁ κ e₂ σ₂ efs + | next {e₁ σ₁ κ₁ e₂ σ₂ efs₁ κ₂ e₃ σ₃ efs₂} : + (e₁, σ₁) -<κ₁>-> (e₂, σ₂, efs₁) → + PrimSteps e₂ σ₂ κ₂ e₃ σ₃ efs₂ → + PrimSteps e₁ σ₁ (κ₁ ++ κ₂) e₃ σ₃ (efs₁ ++ efs₂) + +/-! ### Configuration safety -/ + +inductive Forking where + | doesFork + | doesNotFork + +def cfgNotStuck (C : List Expr × State) : Prop := + ∀ {e}, e ∈ C.1 → NotStuck (e, C.2) + +def cfgForking (C : List Expr × State) (f : Forking) : Prop := + f = .doesNotFork → ∀ e ∈ C.1, ∀ {e' σ' κ efs}, (e, C.2) -<κ>-> (e', σ', efs) → efs = [] + +def cfgSafeForking (C : List Expr × State) (f : Forking) : Prop := + ∀ {C₂}, (C -·->ₜₚ* C₂) → cfgNotStuck C₂ ∧ cfgForking C₂ f + +def cfgSafe (C : List Expr × State) : Prop := + ∀ {C₂}, (C -·->ₜₚ* C₂) → cfgNotStuck C₂ + +theorem cfgSafe_of_cfgSafeForking {C : List Expr × State} {f : Forking} + (H : cfgSafeForking C f) : cfgSafe C := fun Hp _ => H Hp |>.1 + +theorem PrimSteps.fill {K : Expr → Expr} [Context K] {e₁ σ₁ κ e₂ σ₂ efs} + (Hs : PrimSteps e₁ σ₁ κ e₂ σ₂ efs) : PrimSteps (K e₁) σ₁ κ (K e₂) σ₂ efs := + match Hs with + | once hstep => .once <| Context.primStep_fill hstep + | next hstep hsteps => .next (Context.primStep_fill hstep) hsteps.fill + +theorem cfg_step {tp : List Expr} {σ : State} {n : Nat} {e : Expr} + {κ : List Obs} {e' : Expr} {σ' : State} {efs : List Expr} + (Hlu : tp[n]? = some e) (Hprim : (e, σ) -<κ>-> (e', σ', efs)) : + Step (tp, σ) κ (tp.set n e' ++ efs, σ') := by + obtain ⟨hlt, rfl⟩ := List.getElem?_eq_some_iff.mp Hlu + simpa only [List.getElem_cons_drop hlt, List.take_append_drop, + ← List.set_eq_take_cons_drop e' hlt] using + Step.of_primStep Hprim (t₁ := tp.take n) (t₂ := tp.drop (n+1)) + +theorem getElem?_set_append_self {tp : List Expr} {n : Nat} {a : Expr} {efs : List Expr} + (hlt : n < tp.length) : (tp.set n a ++ efs)[n]? = some a := by + rw [List.getElem?_append_left (by rwa [List.length_set]), List.getElem?_set_self hlt] + +theorem set_append_set_append {tp : List Expr} {n : Nat} {a b : Expr} + {efs₁ efs₂ : List Expr} (hlt : n < tp.length) : + (tp.set n a ++ efs₁).set n b ++ efs₂ = tp.set n b ++ (efs₁ ++ efs₂) := by + rw [List.set_append_left _ _ (by rwa [List.length_set]), List.set_set, List.append_assoc] + +theorem cfg_stepsTc {tp : List Expr} {σ : State} {n e κ e' σ' efs} + (Hlu : tp[n]? = some e) (Hprim : PrimSteps e σ κ e' σ' efs) : + Relation.TransGen ErasedStep (tp, σ) (tp.set n e' ++ efs, σ') := by + revert Hlu + induction Hprim generalizing tp with + | once hstep => exact fun Hlu => .single ⟨_, cfg_step Hlu hstep⟩ + | @next _ _ _ e₂ _ efs₁ _ _ _ _ hstep _ ih => + intro Hlu + have hlt : n < tp.length := (List.getElem?_eq_some_iff.mp Hlu).1 + have rest := ih (tp := tp.set n e₂ ++ efs₁) (getElem?_set_append_self hlt) + rw [set_append_set_append hlt] at rest + exact head ⟨_, cfg_step Hlu hstep⟩ rest + +theorem cfg_steps {tp : List Expr} {σ : State} {n e κ e' σ' efs} (Hlu : tp[n]? = some e) + (Hprim : PrimSteps e σ κ e' σ' efs) : (tp, σ) -·->ₜₚ* (tp.set n e' ++ efs, σ') := + to_reflTransGen (cfg_stepsTc Hlu Hprim) + +theorem cfg_safeStep {tp : List Expr} {σ : State} {f n e κ e' σ' efs} + (Hsafe : cfgSafeForking (tp, σ) f) (Hlu : tp[n]? = some e) + (Hprim : (e, σ) -<κ>-> (e', σ', efs)) : + cfgSafeForking (tp.set n e' ++ efs, σ') f ∧ (f = .doesNotFork → efs = []) := by + refine ⟨fun {C₂ Hrtc} => ?_, fun hf => ?_⟩ + · exact Hsafe (.head ⟨κ, cfg_step Hlu Hprim⟩ Hrtc) + · exact Hsafe .refl |>.2 hf e (List.mem_of_getElem? Hlu) Hprim + +theorem cfg_safeSteps {tp : List Expr} {σ : State} {f n e κ e' σ' efs} + (Hsafe : cfgSafeForking (tp, σ) f) (Hlu : tp[n]? = some e) + (Hprim : PrimSteps e σ κ e' σ' efs) : + cfgSafeForking (tp.set n e' ++ efs, σ') f ∧ + (f = .doesNotFork → efs = []) := by + revert Hsafe Hlu + induction Hprim generalizing tp with + | once hstep => exact fun Hsafe Hlu => cfg_safeStep Hsafe Hlu hstep + | @next _ _ _ e₂ _ efs₁ _ _ _ _ hstep _ ih => + intro Hsafe Hlu + have hlt := (List.getElem?_eq_some_iff.mp Hlu).1 + obtain ⟨Hsafe2, Hnf⟩ := cfg_safeStep Hsafe Hlu hstep + obtain ⟨Hsafe3, Hnf2⟩ := + ih (tp := tp.set n e₂ ++ efs₁) Hsafe2 (getElem?_set_append_self hlt) + rw [set_append_set_append hlt] at Hsafe3 + exact ⟨Hsafe3, fun hf => by simp [Hnf hf, Hnf2 hf]⟩ + +theorem nSteps_trans {n m : Nat} {ρ₁ ρ₂ ρ₃ : List Expr × State} {κa κb : List Obs} + (H1 : ρ₁ -<κa>->ₜₚ^[n] ρ₂) (H2 : ρ₂ -<κb>->ₜₚ^[m] ρ₃) : + ρ₁ -<(κa ++ κb)>->ₜₚ^[(n + m)] ρ₃ := by + induction H1 with + | refl ρ => simpa using H2 + | cons hstep _ ih => + rw [Nat.add_right_comm, List.append_assoc] + exact NSteps.cons hstep (ih H2) + +theorem nSteps_one {ρ₁ ρ₂ : List Expr × State} {κ : List Obs} + (H : ρ₁ -<κ>->ₜₚ ρ₂) : ρ₁ -<κ>->ₜₚ^[1] ρ₂ := by + simpa using NSteps.cons H (.refl _) + +theorem nSteps_r {n} {ρ₁ ρ₂ ρ₃ : List Expr × State} {κ κs : List Obs} + (H1 : ρ₁ -<κs>->ₜₚ^[n] ρ₂) (H2 : ρ₂ -<κ>->ₜₚ ρ₃) : ρ₁ -<(κs ++ κ)>->ₜₚ^[(n + 1)] ρ₃ := + nSteps_trans H1 (nSteps_one H2) + +theorem primSteps_atomic {e : Expr} {σ κ e₂ σ' efs} + (Hatom : Atomic .StronglyAtomic e) (Hsteps : PrimSteps e σ κ e₂ σ' efs) : + ((e, σ) -<κ>-> (e₂, σ', efs)) ∧ (ToVal.toVal e₂).isSome := by + cases Hsteps with + | once hstep => exact ⟨hstep, Hatom.atomic hstep⟩ + | next hstep hsteps2 => + have hv := Hatom.atomic hstep + cases hsteps2 with + | once h3 => simp [Language.val_stuck h3] at hv + | next h3 _ => simp [Language.val_stuck h3] at hv + +end + +/-! ### Thread-pool ghost-state invariant -/ + +section ghost +open Iris CMRA Std + +variable {GF : BundledGFunctors} +variable {H : Type _ → Type _} [LawfulFiniteMap H Nat] +variable {Expr : Type _} + +/-- The ghost state needed to track a thread-pool invariant -/ +public class TpinvGS (GF : BundledGFunctors) (Expr : Type _) (H : outParam <| Type _ → Type _) + [LawfulFiniteMap H Nat] extends GhostMapG GF Nat Expr H where + tp_name : GName + +variable [TI : TpinvGS GF Expr H] + +public def isThread (n : Nat) (dq : DFrac) (e : Expr) : IProp GF := + TI.tp_name ↪◯MAP[n]{dq} e + +notation k " ↪thread{" dq "} " v => isThread k dq v +notation k " ↪thread " v => isThread k (DFrac.own 1) v + +public def tpInvIni : IProp GF := + TI.tp_name ↪●MAP (∅ : H Expr) + +public def tpInv (tp : List Expr) : IProp GF := iprop% + ∃ m : H Expr, ⌜∀ n, PartialMap.get? m n = tp[n]?⌝ ∗ TI.tp_name ↪●MAP m + +public instance tpInv_timeless (tp : List Expr) : Iris.BI.Timeless (tpInv (TI := TI) tp) := by + unfold tpInv; infer_instance + +public theorem tpInv_lookup (tp : List Expr) (n : Nat) (e₁ : Expr) (dq : DFrac) : + tpInv tp ⊢@{IProp GF} (n ↪thread{dq} e₁) -∗ ⌜tp[n]? = some e₁⌝ := by + unfold tpInv isThread + iintro ⟨%m, %He, Hauth⟩ Hfrag + ihave %Hlookup := ghost_map_lookup $$ Hauth Hfrag + ipureintro + rw [← Hlookup, He _] + +public theorem tpInv_update (tp : List Expr) (n : Nat) (e₁ e₂ : Expr) : + tpInv tp ⊢@{IProp GF} + (n ↪thread e₁) ==∗ tpInv (tp.set n e₂) ∗ (n ↪thread e₂) := by + iintro Hinv Hfrag + ihave %Hlookup := tpInv_lookup $$ Hinv Hfrag + unfold tpInv isThread + ihave ⟨%m, %He, Hauth⟩ := Hinv + imod ghost_map_update (w := e₂) $$ Hauth Hfrag with ⟨Hauth, Hfrag⟩ + imodintro + iframe + iexists (Std.insert m n e₂) + iframe; ipureintro; intro n + grind [LawfulPartialMap.get?_insert] + +public theorem tpInv_new_threads (efs tp : List Expr) : + ⊢@{IProp GF} tpInv tp ==∗ (tpInv (tp ++ efs) ∗ ([∗list] n ↦ e' ∈ efs, (tp.length + n) ↪thread e')) := by + unfold tpInv isThread + iintro ⟨%m, %He, Hauth⟩ + have Hdisj : PartialMap.disjoint (FiniteMap.map_seq (M := H) tp.length efs) m := by + rw [PartialMap.disjoint_iff] + intro k + rcases Nat.lt_or_ge k tp.length with h | h + · left; rw [LawfulFiniteMap.get?_map_seq, if_neg (by omega)] + · right; rw [He k, List.getElem?_eq_none h] + imod ghost_map_insert_big (FiniteMap.map_seq tp.length efs) Hdisj $$ Hauth + with ⟨Hauth, Hlist⟩ + imodintro + isplitl [Hauth] + · iexists (FiniteMap.map_seq tp.length efs ∪ m) + iframe + ipureintro + intro n + show get? (FiniteMap.map_seq tp.length efs ∪ m) n = (tp ++ efs)[n]? + rw [LawfulPartialMap.get?_union, LawfulFiniteMap.get?_map_seq, He n] + rcases Nat.lt_or_ge n tp.length with h | h + · rw [if_neg (by omega), List.getElem?_append_left h]; rfl + · rw [if_pos h, List.getElem?_append_right h, List.getElem?_eq_none h] + cases efs[n - tp.length]? <;> rfl + · iapply (Iris.BI.BigSepM.bigSepM_map_seq).mp + iexact Hlist + +public theorem tpInv_set (C : List Expr) : + ⊢@{IProp GF} tpInvIni (Expr := Expr) ==∗ tpInv C ∗ ([∗list] n ↦ e ∈ C, n ↪thread e) := by + iintro Hauth + imod tpInv_new_threads C [] $$ [Hauth] with ⟨Hi, Hlist⟩ + · unfold tpInvIni tpInv + iexists ∅ + iframe + ipureintro + exact get?_empty + imodintro + simp + iframe + +end ghost + +/-! ### Allocation -/ + +section alloc +open Iris CMRA Std + +variable {GF : BundledGFunctors} +variable {H : Type _ → Type _} [LawfulFiniteMap H Nat] +variable {Expr : Type _} [GhostMapG GF Nat Expr H] + +open Classical in +public theorem tpInv_alloc : + ⊢@{IProp GF} |==> ∃ γ, + tpInvIni (Expr := Expr) (TI := { toGhostMapG := inferInstance, tp_name := γ }) := by + imod @ghost_map_alloc_empty _ Nat Expr H with ⟨%γ, H⟩ + imodintro + iexists γ + unfold tpInvIni + iexact H + +end alloc + +end Iris.ProgramLogic