diff --git a/Iris/Iris/BI/BI.lean b/Iris/Iris/BI/BI.lean index 9bee2419..fd33d508 100644 --- a/Iris/Iris/BI/BI.lean +++ b/Iris/Iris/BI/BI.lean @@ -107,6 +107,10 @@ theorem BIBase.BiEntails.ofMono [BI PROP1] [BI PROP2] {mod : PROP1 → PROP2} ∀ {P Q : PROP1}, P ⊣⊢ Q → mod P ⊣⊢ mod Q := fun h => ⟨mono h.1, mono h.2⟩ +theorem BIBase.BiEntails.proper [BI PROP] {a a' b b' : PROP} (ha : a ≡ a') (hb : b ≡ b') : (a ⊣⊢ b ↔ a' ⊣⊢ b') where + mp h := equiv_iff.1 (ha.symm.trans (equiv_iff.2 h) |>.trans hb) + mpr h := equiv_iff.1 (ha.trans (equiv_iff.2 h) |>.trans hb.symm) + export BIBase ( Entails emp pure and or imp sForall sExists «forall» «exists» sep wand persistently BiEntails iff wandIff affinely absorbingly diff --git a/Iris/Iris/BI/Plainly.lean b/Iris/Iris/BI/Plainly.lean index 7843d327..0bf505c0 100644 --- a/Iris/Iris/BI/Plainly.lean +++ b/Iris/Iris/BI/Plainly.lean @@ -371,17 +371,13 @@ instance limitPreserving_plain {A} [COFE A] (Φ : A → PROP) (Φne : OFE.NonExp section BigOp -theorem BiEntails_proper {a a' b b' : PROP} (ha : a ≡ a') (hb : b ≡ b') : (a ⊣⊢ b ↔ a' ⊣⊢ b') where - mp h := equiv_iff.1 (ha.symm.trans (equiv_iff.2 h) |>.trans hb) - mpr h := equiv_iff.1 (ha.trans (equiv_iff.2 h) |>.trans hb.symm) - @[rocq_alias plainly_sep_weak_homomorphism] instance plainly_sep_weak_homomorphism [BIPositive PROP][BIAffine PROP] : Algebra.WeakMonoidHomomorphism BIBase.sep BIBase.sep iprop(emp) iprop(emp) BIBase.BiEntails (BIBase.plainly (PROP := PROP)) where rel_refl := .rfl rel_trans := .trans - rel_proper := BiEntails_proper + rel_proper := BIBase.BiEntails.proper op_proper aa' bb' := equiv_iff.1 (sep_ne.eqv (equiv_iff.2 aa') (equiv_iff.2 bb')) map_ne := inferInstance map_op := plainly_sep @@ -391,7 +387,7 @@ instance plainly_and_weak_homomorphism : (BIBase.plainly (PROP := PROP)) where rel_refl := .rfl rel_trans := .trans - rel_proper := BiEntails_proper + rel_proper := BIBase.BiEntails.proper op_proper aa' bb' := equiv_iff.1 (and_ne.eqv (equiv_iff.2 aa') (equiv_iff.2 bb')) map_ne := inferInstance map_op := plainly_and @@ -401,7 +397,7 @@ instance plainly_or_weak_homomorphism [SbiEmpValidExist PROP] : (BIBase.plainly (PROP := PROP)) where rel_refl := .rfl rel_trans := .trans - rel_proper := BiEntails_proper + rel_proper := BIBase.BiEntails.proper op_proper aa' bb' := equiv_iff.1 (or_ne.eqv (equiv_iff.2 aa') (equiv_iff.2 bb')) map_ne := inferInstance map_op := plainly_or diff --git a/Iris/Iris/BI/Updates.lean b/Iris/Iris/BI/Updates.lean index 2187c2bc..a8f91ef9 100644 --- a/Iris/Iris/BI/Updates.lean +++ b/Iris/Iris/BI/Updates.lean @@ -310,6 +310,32 @@ theorem fupd_trans_frame {E1 E2 E3 : CoPset} {P Q : PROP} : fupd_frame_l.trans <| fupd_elim <| ((sep_assoc.2.trans <| sep_mono_l sep_comm.1).trans <| sep_mono_l wand_elim_r).trans <| fupd_frame_r.trans <| BIFUpdate.mono emp_sep.1 +@[rocq_alias fupd_or_homomorphism] +instance fupd_sep_homomorphism E : + Algebra.MonoidHomomorphism (M₁ := PROP) sep sep emp emp (flip Entails) (fupd E E) where + rel_refl := .rfl + rel_trans := flip .trans + rel_proper H G := ⟨fun J => (equiv_iff.1 G).mpr.trans (J.trans (equiv_iff.1 H).mp) + , fun J => (equiv_iff.1 G).mp.trans (J.trans (equiv_iff.1 H).mpr)⟩ + op_proper := sep_mono + map_ne := BIFUpdate.ne + map_op := fupd_sep + map_unit := fupd_intro + +@[rocq_alias big_sepL_fupd] +theorem BigSepL2.big_sepL_fupd {A : Type _} E (Φ : Nat → A → PROP) l : + ([∗list] k↦x ∈ l, |={E}=> Φ k x) ⊢ |={E}=> [∗list] k↦x ∈ l, Φ k x := + Algebra.BigOpL.bigOpL_hom (R := flip Entails) Φ l + +@[rocq_alias big_sepL2_fupd] +theorem BigSepL2.big_sepL2_fupd {A B : Type _} E (Φ : Nat → A → B → PROP) l1 l2 : + ([∗list] k↦x;y ∈ l1;l2, |={E}=> Φ k x y) ⊢ |={E}=> [∗list] k↦x;y ∈ l1;l2, Φ k x y := by + refine BigSepL2.bigSepL2_alt.mp.trans ?_ + refine persistent_and_affinely_sep_l.mp.trans ?_ + refine .trans ?_ (mono BigSepL2.bigSepL2_alt.mpr) + refine .trans ?_ (mono persistent_and_affinely_sep_l.mpr) + exact .trans (sep_mono_r (BigSepL2.big_sepL_fupd E _ _ )) fupd_frame_l + end FUpdLaws section StepFUpdLaws @@ -394,6 +420,20 @@ theorem step_fupdN_le {n m : Nat} {Eo Ei : CoPset} {P : PROP} : theorem step_fupd_fupd {Eo Ei : CoPset} {P : PROP} : (|={Eo}[Ei]▷=> P) ⊣⊢ (|={Eo}[Ei]▷=> |={Eo}=> P) := ⟨mono <| later_mono <| mono fupd_intro, mono <| later_mono BIFUpdate.trans⟩ +@[rocq_alias step_fupdN_mono] +theorem step_fupdN_mono {n : Nat} {Eo Ei : CoPset} {P Q : PROP} (H : P ⊢ Q) : + (|={Eo}[Ei]▷=>^[n] P) ⊢ (|={Eo}[Ei]▷=>^[n] Q) := by + induction n with + | zero => exact H + | succ k IH => exact mono (later_mono (mono IH)) + +@[rocq_alias step_fupdN_S_fupd] +theorem step_fupdN_S_fupd {n : Nat} {E : CoPset} {P : PROP} : + (|={E}[∅]▷=>^[n + 1] P) ⊣⊢ (|={E}[∅]▷=>^[n + 1] |={E}=> P) := by + refine ⟨mono <| later_mono <| mono <| step_fupdN_mono fupd_intro, ?_⟩ + simp only [Nat.repeat_add] + exact step_fupdN_mono step_fupd_fupd.mpr + end StepFUpdLaws section StepFUpdPlainlyLaws diff --git a/Iris/Iris/ProgramLogic/Adequacy.lean b/Iris/Iris/ProgramLogic/Adequacy.lean new file mode 100644 index 00000000..4256efdd --- /dev/null +++ b/Iris/Iris/ProgramLogic/Adequacy.lean @@ -0,0 +1,419 @@ +/- +Copyright (c) 2026 Haokun Li. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Haokun Li, Sergei Stepanenko +-/ +module + +public import Iris.Algebra +public import Iris.BI +public import Iris.ProofMode +public import Iris.ProgramLogic.WeakestPre +public import Iris.Std.FromMathlib + +namespace Iris.ProgramLogic + +open Iris OFE COFE BI Iris.BI Iris.Algebra Std FromMathlib LawfulSet +open Iris.ProgramLogic.PrimStep +open Language.Notation + +@[expose] public section + +variable {hlc : Bool} {Expr State Obs Val : Type _} +variable [Language Expr State Obs Val] +variable {GF : BundledGFunctors} [iG : IrisGS_gen hlc Expr GF] + +abbrev wptp (s : Stuckness) (es : List Expr) (Φs : List (Val → IProp GF)) : IProp GF := + iprop([∗list] e;Φ ∈ es;Φs, WP e @ s ; ⊤ {{ Φ }}) + +@[rocq_alias steps_sum] +def steps_sum (numLaters : Nat → Nat) : Nat → Nat → Nat + | _, 0 => 0 + | start, n + 1 => numLaters start + 1 + steps_sum numLaters (start + 1) n + +@[rocq_alias wp_step] +theorem wp_step (s : Stuckness) (e1 : Expr) (σ1 : State) + (ns : Nat) (κ κs : List Obs) (e2 : Expr) (σ2 : State) (efs : List Expr) (nt : Nat) + (Φ : Val → IProp GF) + (Hstep : (e1, σ1) -<κ>-> (e2, σ2, efs)) : + ⊢ stateInterp σ1 ns (κ ++ κs) nt -∗ + £ (iG.numLatersPerStep ns + 1) -∗ + WP e1 @ s ; ⊤ {{ Φ }} + ={⊤,∅}=∗ + |={∅}▷=>^[iG.numLatersPerStep ns + 1] |={∅,⊤}=> + stateInterp σ2 (ns + 1) κs (nt + efs.length) ∗ + WP e2 @ s ; ⊤ {{ Φ }} ∗ + wptp s efs (List.replicate efs.length iG.forkPost) := by + rw [IProp.ext wp_unfold] + simp only [wp.pre, Language.val_stuck Hstep] + iintro Hσ Hcred Hwp + imod Hwp $$ %σ1 %ns %κ %κs %nt Hσ with ⟨%_, Hcont⟩ + imodintro + ihave Hcont := Hcont $$ %e2 %σ2 %efs %Hstep Hcred + iapply step_fupdN_wand $$ Hcont + iintro >⟨HSI, Hwp2, Hefs⟩ + imodintro + iframe HSI Hwp2 + iapply BigSepL2.bigSepL2_replicate_right.mpr + iexact Hefs + +@[rocq_alias wptp_step] +theorem wptp_step (s : Stuckness) (es1 es2 : List Expr) + (κ κs : List Obs) (σ1 σ2 : State) (ns : Nat) (Φs : List (Val → IProp GF)) (nt : Nat) + (Hstep : (es1, σ1) -<κ>->ₜₚ (es2, σ2)) : + ⊢ stateInterp σ1 ns (κ ++ κs) nt -∗ + £ (iG.numLatersPerStep ns + 1) -∗ + wptp s es1 Φs -∗ + ∃ nt', |={⊤,∅}=> |={∅}▷=>^[iG.numLatersPerStep ns + 1] |={∅,⊤}=> + stateInterp σ2 (ns + 1) κs (nt + nt') ∗ + wptp s es2 (Φs ++ List.replicate nt' iG.forkPost) := by + cases Hstep with | @atomic e1' _ _ e2' _ efs H_prim t₁ t₂ => + iintro Hσ Hcred Hwptp + iexists efs.length + icases BigSepL2.bigSepL2_app_inv_left $$ Hwptp with ⟨%Φs1, %Φs2, %hΦs, Hwptp1, Hwptp2⟩ + icases BigSepL2.bigSepL2_cons_inv_left $$ Hwptp2 with ⟨%Φ_head, %Φs2', %hΦs2, Hwp_e1, Hwptp3⟩ + subst hΦs hΦs2 + imod wp_step (Hstep := H_prim) $$ Hσ Hcred Hwp_e1 with Hstep + imodintro + iapply step_fupdN_wand $$ Hstep + iintro >⟨HSI, Hwp_e2, Hwptp_efs⟩ + imodintro + iframe HSI + icases BigSepL2.bigSepL2_length $$ Hwptp1 with %Hlen1 + icases BigSepL2.bigSepL2_length $$ Hwptp3 with %Hlen3 + simp only [List.append_assoc, List.cons_append] + iapply BigSepL2.bigSepL2_append (.inl Hlen1); iframe Hwptp1 + iapply BigSepL2.bigSepL2_cons; iframe Hwp_e2 + iapply BigSepL2.bigSepL2_append (.inl Hlen3); iframe Hwptp3 Hwptp_efs + +@[rocq_alias wp_not_stuck] +theorem wp_not_stuck (κs : List Obs) (nt : Nat) (e : Expr) (σ : State) + (ns : Nat) (Φ : Val → IProp GF) : + ⊢ stateInterp σ ns κs nt -∗ + WP e @ Stuckness.NotStuck ; ⊤ {{ Φ }} ={⊤,∅}=∗ ⌜NotStuck (e, σ)⌝ := by + rw [IProp.ext wp_unfold] + unfold wp.pre + match h : toVal e with + | some v => + dsimp only + iintro _ _ + iapply fupd_mask_intro_discard empty_subset + ipure_intro + exact .inl (by rw [h]; rfl) + | none => + dsimp only + iintro Hst Hcont + ispecialize Hcont $$ %σ %ns %([]) %κs %nt + rw [List.nil_append] + imod Hcont $$ Hst with ⟨%H, _⟩ + imodintro + ipure_intro + exact .inr H + +@[rocq_alias wptp_preservation] +theorem wptp_preservation (s : Stuckness) (n : Nat) (es1 es2 : List Expr) + (κs κs' : List Obs) (σ1 σ2 : State) (ns : Nat) + (Φs : List (Val → IProp GF)) (nt : Nat) + (Hsteps : (es1, σ1) -<κs>->ₜₚ^[n] (es2, σ2)) : + ⊢ stateInterp σ1 ns (κs ++ κs') nt -∗ + £ (steps_sum iG.numLatersPerStep ns n) -∗ + wptp s es1 Φs ={⊤,∅}=∗ + |={∅}▷=>^[steps_sum iG.numLatersPerStep ns n] |={∅,⊤}=> ∃ nt', + stateInterp σ2 (n + ns) κs' (nt + nt') ∗ + wptp s es2 (Φs ++ List.replicate nt' iG.forkPost) := by + generalize hρ1 : (es1, σ1) = ρ1 at Hsteps + generalize hρ2 : (es2, σ2) = ρ2 at Hsteps + induction Hsteps generalizing nt κs' Φs ns es1 σ1 es2 σ2 with + | refl ρ => + cases hρ1; cases hρ2 + simp only [Nat.zero_add, List.nil_append, steps_sum, Nat.repeat] + iintro Hσ _ Hwptp + iapply fupd_mask_intro empty_subset + iintro Hcl; imod Hcl; imodintro + iexists 0 + simp only [List.replicate, List.append_nil] + iframe Hσ + iexact Hwptp + | @cons n_inner ρ1' ρ_mid ρ2' obs obs' hstep hrest ih => + cases hρ1; cases hρ2 + cases ρ_mid with | mk e_mid σ_mid => + rw [List.append_assoc obs obs' κs'] + dsimp only [steps_sum] + rw [Nat.repeat_add] + iintro Hσ ⟨Hcred1, Hcred2⟩ Hwptp + icases wptp_step s es1 e_mid obs (obs' ++ κs') σ1 σ_mid ns Φs nt hstep + $$ Hσ Hcred1 Hwptp with ⟨%nt'_step, >Hwptp_step⟩ + imodintro + iapply step_fupdN_S_fupd.2 + iapply step_fupdN_wand $$ Hwptp_step + iintro >⟨HSI, Hwptp_mid⟩ + imod ih _ _ _ _ _ _ _ _ rfl rfl $$ HSI Hcred2 Hwptp_mid with Hih + imodintro + iapply step_fupdN_wand $$ Hih + iintro >⟨%nt_inner', HSI', Hwptp'⟩ + iexists (nt'_step + nt_inner') + rw [Nat.add_assoc, Nat.add_comm _ 1, ←Nat.add_assoc] + rw [←List.replicate_append_replicate, List.append_assoc] + iframe HSI' Hwptp' + +@[rocq_alias wptp_postconditions] +theorem wptp_postconditions (Φs : List (Val → IProp GF)) (κs' : List Obs) + (s : Stuckness) (n : Nat) (es1 es2 : List Expr) (κs : List Obs) + (σ1 σ2 : State) (ns nt : Nat) + (Hsteps : (es1, σ1) -<κs>->ₜₚ^[n] (es2, σ2)) : + ⊢ stateInterp σ1 ns (κs ++ κs') nt -∗ + £ (steps_sum iG.numLatersPerStep ns n) -∗ + wptp s es1 Φs ={⊤,∅}=∗ + |={∅}▷=>^[steps_sum iG.numLatersPerStep ns n] |={∅,⊤}=> ∃ nt', + stateInterp σ2 (n + ns) κs' (nt + nt') ∗ + [∗list] e;Φ ∈ es2;Φs ++ List.replicate nt' iG.forkPost, + (toVal e).elim iprop(True) Φ := by + iintro Hσ Hcred Hwptp + imod wptp_preservation s n es1 es2 κs κs' σ1 σ2 ns Φs nt Hsteps + $$ Hσ Hcred Hwptp with Hpres + imodintro + iapply step_fupdN_wand $$ Hpres + iintro >⟨%nt', HSI, Hwptp_es2⟩ + iexists nt'; iframe HSI + iapply BigSepL2.big_sepL2_fupd + iapply BigSepL2.bigSepL2_impl $$ Hwptp_es2 + imodintro + iintro %k %x1 %x2 %Hin %Hlen Hwp + cases hv : toVal x1 + · imodintro; apply true_intro + · simp only [Option.elim_some] + iapply wp_value_fupd $$ Hwp + constructor; grind + +#rocq_ignore wptp_progress "Rocq version moved to a version with no progress lemmas" +theorem wptp_progress (Φs : List (Val → IProp GF)) (κs' : List Obs) (n : Nat) + (es1 es2 : List Expr) (κs : List Obs) (σ1 σ2 : State) (ns nt : Nat) (e2 : Expr) + (Hsteps : (es1, σ1) -<κs>->ₜₚ^[n] (es2, σ2)) (Hel : e2 ∈ es2) : + ⊢ stateInterp σ1 ns (κs ++ κs') nt -∗ + £ (steps_sum iG.numLatersPerStep ns n) -∗ + wptp .NotStuck es1 Φs ={⊤,∅}=∗ + |={∅}▷=>^[steps_sum iG.numLatersPerStep ns n] |={∅}=> + ⌜NotStuck (e2, σ2)⌝ := by + iintro Hσ Hcred Ht + imod wptp_preservation .NotStuck n es1 es2 κs κs' σ1 σ2 ns Φs nt Hsteps + $$ Hσ Hcred Ht with Hpres + imodintro + iapply step_fupdN_wand $$ Hpres + iintro >⟨%nt'', HSI, Hwptp⟩ + obtain ⟨i, hi⟩ := List.getElem?_of_mem Hel + icases BigSepL2.bigSepL2_length $$ Hwptp with %hlen + have hi_lt := (List.getElem?_eq_some_iff.mp hi).1 + have hi_Φ := List.getElem?_eq_getElem (hlen ▸ hi_lt) + icases BigSepL2.bigSepL2_lookup_acc hi hi_Φ $$ Hwptp with ⟨Hwp_e2, _⟩ + iapply wp_not_stuck $$ HSI Hwp_e2 + +#rocq_ignore wp_progress_gen "Rocq version moved to a version with no progress lemmas" +omit iG in +theorem wp_progress_gen [InvGpreS GF] (es : List Expr) (σ1 : State) (n : Nat) (κs : List Obs) + (t2 : List Expr) (σ2 : State) (e2 : Expr) (numLaters : Nat → Nat) + (Hwp : ∀ [InvGS_gen hlc GF], + ⊢ |={⊤}=> + ∃ (stateI : State → Nat → List Obs → Nat → IProp GF) + (Φs : List (Val → IProp GF)) (forkPost : Val → IProp GF) + (mono : ∀ σ ns obs nt, stateI σ ns obs nt ⊢ |={∅}=> stateI σ (ns + 1) obs nt), + let _ : IrisGS_gen hlc Expr GF := .mk (toStateInterp := ⟨stateI⟩) numLaters forkPost mono + iprop(stateI σ1 0 κs 0 ∗ wptp Stuckness.NotStuck es Φs)) + (Hsteps : (es, σ1) -<κs>->ₜₚ^[n] (t2, σ2)) + (Hel : e2 ∈ t2) : + NotStuck (e2, σ2) := by + apply pure_soundness (PROP := IProp GF) + refine step_fupdN_soundness_gen (steps_sum numLaters 0 n + 1) (steps_sum numLaters 0 n + 1) hlc ?_ + iintro %Hinv ⟨Hcr_1, Hcr_k⟩ + imod Hwp with ⟨%stateI, %Φs, %forkPost, %mono, HSI, Hwptp⟩ + letI iG : IrisGS_gen hlc Expr GF := .mk (toStateInterp := ⟨stateI⟩) numLaters forkPost mono + ihave Hres := wptp_progress Φs [] n es t2 κs σ1 σ2 0 0 e2 Hsteps Hel $$ [HSI] Hcr_k Hwptp + · simp only [List.append_nil]; iframe + imod Hres; imodintro + iapply step_fupdN_S_fupd.2 + simp only [Nat.repeat] + imodintro; imodintro; imodintro; iframe + +omit iG in +@[rocq_alias wp_strong_adequacy_gen] +theorem wp_strong_adequacy_gen [InvGpreS GF] (s : Stuckness) (es : List Expr) (σ1 : State) + (n : Nat) (κs : List Obs) (t2 : List Expr) (σ2 : State) (φ : Prop) + (numLaters : Nat → Nat) (Hwp : ∀ [InvGS_gen hlc GF], + ⊢ |={⊤}=> + ∃ (stateI : State → Nat → List Obs → Nat → IProp GF) + (Φs : List (Val → IProp GF)) (forkPost : Val → IProp GF) + (mono : ∀ σ ns obs nt, stateI σ ns obs nt ⊢ |={∅}=> stateI σ (ns + 1) obs nt), + let _ : IrisGS_gen hlc Expr GF := .mk (toStateInterp := ⟨stateI⟩) numLaters forkPost mono + iprop(stateI σ1 0 κs 0 ∗ + ([∗list] e;Φ ∈ es;Φs, WP e @ s ; ⊤ {{ Φ }}) ∗ + (∀ (es' t2' : List Expr), + ⌜t2 = es' ++ t2'⌝ -∗ ⌜es'.length = es.length⌝ -∗ + ⌜∀ e2, s = .NotStuck → e2 ∈ t2 → NotStuck (e2, σ2)⌝ -∗ + stateI σ2 n [] t2'.length -∗ + ([∗list] e;Φ ∈ es';Φs, (toVal e).elim iprop(True) Φ) -∗ + ([∗list] v ∈ List.filterMap toVal t2', forkPost v) -∗ + |={⊤,∅}=> ⌜φ⌝))) + (Hsteps : (es, σ1) -<κs>->ₜₚ^[n] (t2, σ2)) : + φ := by + apply pure_soundness (PROP := IProp GF) + refine step_fupdN_soundness_gen (steps_sum numLaters 0 n + 1) (steps_sum numLaters 0 n + 1) hlc ?_ + iintro %Hinv ⟨Hcr_1, Hcr_k⟩ + imod Hwp with ⟨%stateI, %Φs, %forkPost, %mono, HSI_init, Hwptp_bsl, Hφ⟩ + letI iG : IrisGS_gen hlc Expr GF := .mk (toStateInterp := ⟨stateI⟩) numLaters forkPost mono + ihave %hlen_es_Φs := BigSepL2.bigSepL2_length $$ Hwptp_bsl + imod wptp_postconditions (Hsteps := Hsteps) (κs' := []) (ns := 0) $$ [HSI_init] Hcr_k Hwptp_bsl with H + · simp only [List.append_nil]; iframe + imodintro + iapply step_fupdN_S_fupd.2 + simp only [Nat.repeat] + imodintro; imodintro; imodintro + iapply step_fupdN_wand $$ H + iintro >⟨%nt', Hst, Hwptp⟩ + icases BigSepL2.bigSepL2_app_inv_right $$ Hwptp with ⟨%es', %t2', %Heq, Hes', Ht2'⟩ + icases BigSepL2.bigSepL2_length $$ Ht2' with %Hlen2 + rw [List.length_replicate] at Hlen2; subst Hlen2 + icases BigSepL2.bigSepL2_length $$ Hes' with %Hlen3 + simp only [Nat.add_zero, Nat.zero_add] + iapply Hφ $$ %es' %t2' [//] [//] [] Hst Hes' [Ht2'] + · ipure_intro + rintro e2 ⟨⟩ hel + refine wp_progress_gen (GF := GF) (hlc := hlc) es σ1 n κs t2 σ2 e2 numLaters ?_ Hsteps hel + iintro %_ + imod Hwp with ⟨%stateI, %Φs, %forkPost, %mono, HSI, Hwptp_bs, _Hφ⟩ + let iG_local : IrisGS_gen hlc Expr GF := .mk (toStateInterp := ⟨stateI⟩) numLaters forkPost mono + imodintro + iexists stateI, Φs, forkPost, mono + simp only [forall_const] + iframe HSI Hwptp_bs + · icases BigSepL2.bigSepL2_replicate_right $$ Ht2' with Ht2' + iapply BigSepL.bigSepL_filterMap + iapply BigSepL.bigSepL_mono $$ Ht2' + iintro %_ %x %_ + cases toVal x + · dsimp + iintro H; iapply BI.true_emp $$ H + · dsimp + iintro H; iexact H + +@[rocq_alias wp_strong_adequacy] +abbrev wp_strong_adequacy := @wp_strong_adequacy_gen true + +@[rocq_alias adequate] +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 + adequate_not_stuck : + ∀ (t2 : List Expr) (σ2 : State) (e2 : Expr), + s = .NotStuck → ([e1], σ1) -·->ₜₚ* (t2, σ2) → e2 ∈ t2 → NotStuck (e2, σ2) + +@[rocq_alias adequate_alt] +theorem adequate_alt (s : Stuckness) (e1 : Expr) (σ1 : State) + (φ : Val → State → Prop) : + adequate s e1 σ1 φ ↔ + ∀ (t2 : List Expr) (σ2 : State), + ([e1], σ1) -·->ₜₚ* (t2, σ2) → + (∀ (v2 : Val) (t2' : List Expr), t2 = ToVal.ofVal v2 :: t2' → φ v2 σ2) ∧ + (∀ (e2 : Expr), s = .NotStuck → e2 ∈ t2 → NotStuck (e2, σ2)) := by + refine ⟨fun ⟨hres, hns⟩ t2 σ2 hreach => ⟨?_, ?_⟩, fun h => ⟨?_, ?_⟩⟩ + · rintro v2 t2' ⟨⟩ + exact hres _ _ _ hreach + · exact fun e2 hs hel => hns _ _ _ hs hreach hel + · exact fun t2 σ2 v2 hreach => ((h _ _ hreach).1) v2 t2 rfl + · exact fun t2 σ2 e2 hs hreach hel => ((h _ _ hreach).2) e2 hs hel + +@[rocq_alias adequate_tp_safe] +theorem adequate_tp_safe (e1 : Expr) (t2 : List Expr) (σ1 σ2 : State) + (φ : Val → State → Prop) (had : adequate .NotStuck e1 σ1 φ) + (hsteps : ([e1], σ1) -·->ₜₚ* (t2, σ2)) : + (∀ e ∈ t2, ∃ v, ToVal.toVal e = some v) ∨ + ∃ (t3 : List Expr) (σ3 : State), (t2, σ2) -·->ₜₚ (t3, σ3) := by + by_cases hall : ∀ e ∈ t2, ∃ v, ToVal.toVal e = some v + · exact .inl hall + · simp [Classical.not_forall] at hall + obtain ⟨e2, ⟨hel, hne⟩⟩ := hall + have hns : NotStuck (e2, σ2) := had.adequate_not_stuck t2 σ2 e2 rfl hsteps hel + rcases hns with hv | ⟨obs, e3, σ3, efs, hstep⟩ + · exfalso; rcases hv2 : ToVal.toVal e2 with _ | v <;> grind + obtain ⟨t2', t2'', rfl⟩ := List.append_of_mem hel + exact .inr ⟨t2' ++ e3 :: t2'' ++ efs, σ3, obs, Language.Step.of_primStep hstep⟩ + +omit iG in +@[rocq_alias wp_adequacy_gen] +theorem wp_adequacy_gen [InvGpreS GF] (s : Stuckness) (e : Expr) (σ : State) (φ : Val → Prop) + (Hwp : ∀ [InvGS_gen hlc GF] (κs : List Obs), + ⊢ iprop(|={⊤}=> + ∃ (stateI : State → List Obs → IProp GF) + (forkPost : Val → IProp GF), + letI _ : IrisGS_gen hlc Expr GF := + .mk (toStateInterp := ⟨fun σ _ κs _ => stateI σ κs⟩) (fun _ => 0) forkPost + (fun _ _ _ _ => fupd_intro) + iprop(stateI σ κs ∗ WP e @ s ; ⊤ {{ v, ⌜φ v⌝ }}))) : + adequate s e σ (fun v _ => φ v) := by + refine (adequate_alt s e σ (fun v _ => φ v)).mpr ?_ + intro t2 σ2 hreach + obtain ⟨n, κs, hsteps⟩ := (Language.erasedStep_nSteps _ _).mp hreach + apply wp_strong_adequacy_gen (GF := GF) (hlc := hlc) s (Hsteps := hsteps) (numLaters := fun _ => 0) + iintro %Hinv + imod Hwp κs with ⟨%Hst, %Hfork, ⟨Hst, Hwp⟩⟩ + iexists (λ σ _ κs _ => Hst σ κs), [(λ v => iprop(⌜φ v⌝))], Hfork, (fun _ _ _ _ => fupd_intro) + dsimp only + imodintro + iframe + isplitl [Hwp] + · iapply BigSepL2.bigSepL2_singleton; iframe + iintro %_ %_ %Heq %_ %HNS Hst Hwptp _ + iapply fupd_mask_intro_discard empty_subset + icases BigSepL2.bigSepL2_cons_inv_right $$ Hwptp with ⟨%e', %_, %Heq', Hpost, H⟩ + subst Heq' Heq + dsimp only [List.cons_append, List.length_cons, Nat.pred_eq_sub_one, Nat.add_one_sub_one] + icases BigSepL2.bigSepL2_nil_inv_right $$ H with %Heq + subst Heq + cases h : toVal e' + · ipure_intro; grind + · dsimp only [Option.elim_some]; icases Hpost with %Hpost + ipure_intro; grind + +@[rocq_alias wp_adequacy] +abbrev wp_adequacy := @wp_adequacy_gen true + +omit iG in +@[rocq_alias wp_invariance_gen] +theorem wp_invariance_gen [InvGpreS GF] (s : Stuckness) (e1 : Expr) (σ1 σ2 : State) (t2 : List Expr) + (φ : Prop) + (Hwp : ∀ [InvGS_gen hlc GF] (κs : List Obs), + ⊢ iprop(|={⊤}=> + ∃ (stateI : State → List Obs → Nat → IProp GF) + (forkPost : Val → IProp GF), + letI _ : IrisGS_gen hlc Expr GF := .mk (toStateInterp := ⟨fun σ _ => stateI σ⟩) + (fun _ => 0) forkPost (fun _ _ _ _ => fupd_intro) + iprop(stateI σ1 κs 0 ∗ WP e1 @ s ; ⊤ {{ _v, iprop(True) }} ∗ + (stateI σ2 [] (.pred (List.length t2)) -∗ ∃ (E : CoPset), |={⊤,E}=> ⌜φ⌝)))) + (Hsteps : ([e1], σ1) -·->ₜₚ* (t2, σ2)) : + φ := by + obtain ⟨n, κs, hsteps⟩ := (Language.erasedStep_nSteps _ _).mp Hsteps + apply wp_strong_adequacy_gen (GF := GF) (hlc := hlc) s (Hsteps := hsteps) (numLaters := fun _ => 0) + iintro %Hinv + imod Hwp κs with ⟨%Hst, %Hfork, ⟨Hst, Hwp, Hcont⟩⟩ + iexists ((λ σ _ => Hst σ)), [(λ _ => iprop(True))], Hfork, (fun _ _ _ _ => fupd_intro) + dsimp only + imodintro + iframe Hst + isplitl [Hwp] + · iapply BigSepL2.bigSepL2_singleton; iframe + iintro %_ %_ %Heq %_ %_ Hst Hwptp _ + icases BigSepL2.bigSepL2_cons_inv_right $$ Hwptp with ⟨%_, %_, %Heq', _, H⟩ + subst Heq' Heq + dsimp only [List.cons_append, List.length_cons, Nat.pred_eq_sub_one, Nat.add_one_sub_one] + icases BigSepL2.bigSepL2_nil_inv_right $$ H with %Heq + subst Heq + icases Hcont $$ [Hst] with ⟨%_, >Hcont⟩ + · simp only [List.nil_append, refl] + iapply fupd_mask_intro_discard empty_subset + iframe Hcont + +@[rocq_alias wp_invariance] +abbrev wp_invariance := @wp_invariance_gen true + +end +end Iris.ProgramLogic diff --git a/Iris/Iris/Std/Nat.lean b/Iris/Iris/Std/Nat.lean index 5b676adc..e2790828 100644 --- a/Iris/Iris/Std/Nat.lean +++ b/Iris/Iris/Std/Nat.lean @@ -9,7 +9,7 @@ module namespace Nat -theorem repeat_add {A : Type} (n1 n2 : Nat) (f : A → A) (x : A) : +theorem repeat_add {A : Type _} (n1 n2 : Nat) (f : A → A) (x : A) : (n1 + n2).repeat f x = n1.repeat f (n2.repeat f x) := by induction n1 with | zero => simp [«repeat»] diff --git a/Iris/PORTING.md b/Iris/PORTING.md index deb1b7be..6fc1cf89 100644 --- a/Iris/PORTING.md +++ b/Iris/PORTING.md @@ -290,3 +290,4 @@ See proofmode at https://leanprover-community.github.io/iris-lean/ - [x] `ectx_language.v` - [x] `ectxi_language.v` - [x] `weakestpre.v` + - [x] `adequacy.v`