From 05ee95796f524d086b063ca50a6882af64e109e1 Mon Sep 17 00:00:00 2001 From: ayhon Date: Sat, 18 Jul 2026 12:40:46 +0200 Subject: [PATCH 1/6] fix: typo --- Iris/Iris/BI/WeakestPre.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Iris/Iris/BI/WeakestPre.lean b/Iris/Iris/BI/WeakestPre.lean index 270c15662..6d84d642c 100644 --- a/Iris/Iris/BI/WeakestPre.lean +++ b/Iris/Iris/BI/WeakestPre.lean @@ -40,7 +40,7 @@ instance : Std.IsPreorder Stuckness where @[simp] theorem le_MaybeStuck {s : Stuckness} : s ≤ MaybeStuck := by cases s <;> grind only [Stuckness, LE.le, instLE] -@[simp] theorem NotSuck_le {s : Stuckness} : NotStuck ≤ s := by +@[simp] theorem NotStuck_le {s : Stuckness} : NotStuck ≤ s := by cases s <;> grind only [Stuckness, LE.le, instLE] end Stuckness From 65f4cd11ed138695746a8c739354c98c8bb97588 Mon Sep 17 00:00:00 2001 From: ayhon Date: Sat, 18 Jul 2026 16:09:21 +0200 Subject: [PATCH 2/6] fix: texan triple uses a wand, not an implication --- Iris/Iris/BI/WeakestPre.lean | 5 +-- Iris/Iris/Tests/WeakestPre.lean | 62 ++++++++++++++++----------------- 2 files changed, 34 insertions(+), 33 deletions(-) diff --git a/Iris/Iris/BI/WeakestPre.lean b/Iris/Iris/BI/WeakestPre.lean index 6d84d642c..d0deff3f5 100644 --- a/Iris/Iris/BI/WeakestPre.lean +++ b/Iris/Iris/BI/WeakestPre.lean @@ -129,8 +129,9 @@ meta def wpTexanTriple : Lean.Macro | `(⦃ $P:term ⦄ $wpExpr ⦃ $[$[$xs:ident]* ,]? RET $pat ; $Q:term ⦄) | `({{ $P:term }} $wpExpr {{ $[$[$xs:ident]* ,]? RET $pat ; $Q:term }}) => do let k ← match xs with - | some xs => `(∀ $xs*, $Q:term → Φ $pat) - | none => `($Q:term → Φ $pat) + | some xs => + `(iprop(∀ $xs*, $Q:term -∗ Φ $pat)) + | none => `($Q:term -∗ Φ $pat) `(iprop(∀ Φ, $P -∗ ▷ $k -∗ (WP $wpExpr {{ Φ }}))) | _ => Lean.Macro.throwUnsupported diff --git a/Iris/Iris/Tests/WeakestPre.lean b/Iris/Iris/Tests/WeakestPre.lean index b2316c870..fad38bf8a 100644 --- a/Iris/Iris/Tests/WeakestPre.lean +++ b/Iris/Iris/Tests/WeakestPre.lean @@ -183,64 +183,64 @@ variable [BI PROP] variable (e : Expr)(s : A)(E : CoPset) variable (P Q : PROP) -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q → Φ (x + y)) -∗ WP e @ s ; E {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q -∗ Φ (x + y)) -∗ WP e @ s ; E {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} e @ s ; E {{ x y , RET (x+y) ; Q }} -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q → Φ (x + y)) -∗ WP e @ E {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q -∗ Φ (x + y)) -∗ WP e @ E {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} e @ E {{ x y , RET (x+y) ; Q }} -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q → Φ (x + y)) -∗ WP e @ E ? {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q -∗ Φ (x + y)) -∗ WP e @ E ? {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} e @ E ? {{ x y , RET (x+y) ; Q }} -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q → Φ (x + y)) -∗ WP e {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q -∗ Φ (x + y)) -∗ WP e {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} e {{ x y , RET (x+y) ; Q }} -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q → Φ (x + y)) -∗ WP e ? {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q -∗ Φ (x + y)) -∗ WP e ? {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} e ? {{ x y , RET (x+y) ; Q }} -/-- info: iprop(∀ Φ, P -∗ ▷ (Q → Φ 0) -∗ WP e @ s ; E {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ ▷ (Q -∗ Φ 0) -∗ WP e @ s ; E {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} e @ s ; E {{ RET 0 ; Q }} -/-- info: iprop(∀ Φ, P -∗ ▷ (Q → Φ 0) -∗ WP e @ E {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ ▷ (Q -∗ Φ 0) -∗ WP e @ E {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} e @ E {{ RET 0 ; Q }} -/-- info: iprop(∀ Φ, P -∗ ▷ (Q → Φ 0) -∗ WP e @ E ? {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ ▷ (Q -∗ Φ 0) -∗ WP e @ E ? {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} e @ E ? {{ RET 0 ; Q }} -/-- info: iprop(∀ Φ, P -∗ ▷ (Q → Φ 0) -∗ WP e {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ ▷ (Q -∗ Φ 0) -∗ WP e {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} e {{ RET 0 ; Q }} -/-- info: iprop(∀ Φ, P -∗ ▷ (Q → Φ 0) -∗ WP e ? {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ ▷ (Q -∗ Φ 0) -∗ WP e ? {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} e ? {{ RET 0 ; Q }} -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q → Φ (x + y)) -∗ WP e @ s ; E {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q -∗ Φ (x + y)) -∗ WP e @ s ; E {{ Φ }} ) : PROP -/ #guard_msgs in #check ⦃ P ⦄ e @ s ; E ⦃ x y , RET (x+y) ; Q ⦄ -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q → Φ (x + y)) -∗ WP e @ E {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q -∗ Φ (x + y)) -∗ WP e @ E {{ Φ }} ) : PROP -/ #guard_msgs in #check ⦃ P ⦄ e @ E ⦃ x y , RET (x+y) ; Q ⦄ -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q → Φ (x + y)) -∗ WP e @ E ? {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q -∗ Φ (x + y)) -∗ WP e @ E ? {{ Φ }} ) : PROP -/ #guard_msgs in #check ⦃ P ⦄ e @ E ? ⦃ x y , RET (x+y) ; Q ⦄ -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q → Φ (x + y)) -∗ WP e {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q -∗ Φ (x + y)) -∗ WP e {{ Φ }} ) : PROP -/ #guard_msgs in #check ⦃ P ⦄ e ⦃ x y , RET (x+y) ; Q ⦄ -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q → Φ (x + y)) -∗ WP e ? {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x y, Q -∗ Φ (x + y)) -∗ WP e ? {{ Φ }} ) : PROP -/ #guard_msgs in #check ⦃ P ⦄ e ? ⦃ x y , RET (x+y) ; Q ⦄ -/-- info: iprop(∀ Φ, P -∗ ▷ (Q → Φ 0) -∗ WP e @ s ; E {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ ▷ (Q -∗ Φ 0) -∗ WP e @ s ; E {{ Φ }} ) : PROP -/ #guard_msgs in #check ⦃ P ⦄ e @ s ; E ⦃ RET 0 ; Q ⦄ -/-- info: iprop(∀ Φ, P -∗ ▷ (Q → Φ 0) -∗ WP e @ E {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ ▷ (Q -∗ Φ 0) -∗ WP e @ E {{ Φ }} ) : PROP -/ #guard_msgs in #check ⦃ P ⦄ e @ E ⦃ RET 0 ; Q ⦄ -/-- info: iprop(∀ Φ, P -∗ ▷ (Q → Φ 0) -∗ WP e @ E ? {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ ▷ (Q -∗ Φ 0) -∗ WP e @ E ? {{ Φ }} ) : PROP -/ #guard_msgs in #check ⦃ P ⦄ e @ E ? ⦃ RET 0 ; Q ⦄ -/-- info: iprop(∀ Φ, P -∗ ▷ (Q → Φ 0) -∗ WP e {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ ▷ (Q -∗ Φ 0) -∗ WP e {{ Φ }} ) : PROP -/ #guard_msgs in #check ⦃ P ⦄ e ⦃ RET 0 ; Q ⦄ -/-- info: iprop(∀ Φ, P -∗ ▷ (Q → Φ 0) -∗ WP e ? {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ ▷ (Q -∗ Φ 0) -∗ WP e ? {{ Φ }} ) : PROP -/ #guard_msgs in #check ⦃ P ⦄ e ? ⦃ RET 0 ; Q ⦄ end TestTexanTriple @@ -288,31 +288,31 @@ variable (PROP : Type _) [BI PROP] variable [Wp PROP Exp Val Stuckness] variable (E : CoPset) (P Q : PROP) -/-- info: iprop(∀ Φ, P -∗ ▷ (Q → Φ hl_val(#1)) -∗ WP hl(#1) {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ ▷ (Q -∗ Φ hl_val(#1)) -∗ WP hl(#1) {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} hl(#1) {{ RET hl_val(#1); Q }} -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q → Φ x) -∗ WP hl((#1 + #2)) {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q -∗ Φ x) -∗ WP hl((#1 + #2)) {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} hl(#1 + #2) {{ x, RET x; Q }} -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q → Φ x) -∗ WP hl((#1 < #2)) {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q -∗ Φ x) -∗ WP hl((#1 < #2)) {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} hl(#1 < #2) {{ x, RET x; Q }} /-- -info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q → Φ x) -∗ WP hl(if (#0 < #1) then #1 else #2) {{ Φ }} ) : PROP +info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q -∗ Φ x) -∗ WP hl(if (#0 < #1) then #1 else #2) {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} hl(if #0 < #1 then #1 else #2) {{ x, RET x; Q }} -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q → Φ x) -∗ WP hl((λ x, x)) {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q -∗ Φ x) -∗ WP hl((λ x, x)) {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} hl(λ x, x) {{ x, RET x; Q }} -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q → Φ x) -∗ WP hl((rec f x := f x)) {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q -∗ Φ x) -∗ WP hl((rec f x := f x)) {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} hl(rec f x := f x) {{ x, RET x; Q }} -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q → Φ x) -∗ WP hl(#1; #2) {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q -∗ Φ x) -∗ WP hl(#1; #2) {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} hl(#1; #2) {{ x, RET x; Q }} -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q → Φ x) -∗ WP hl((#1, #2)) {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q -∗ Φ x) -∗ WP hl((#1, #2)) {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} hl((#1, #2)) {{ x, RET x; Q }} -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q → Φ x) -∗ WP hl(ref(#0)) {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q -∗ Φ x) -∗ WP hl(ref(#0)) {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} hl(ref(#0)) {{ x, RET x; Q }} /-- -info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q → Φ x) -∗ WP hl(if (#1 < #2) then (#1 + #1) else #0) {{ Φ }} ) : PROP +info: iprop(∀ Φ, P -∗ (▷ ∀ x, Q -∗ Φ x) -∗ WP hl(if (#1 < #2) then (#1 + #1) else #0) {{ Φ }} ) : PROP -/ #guard_msgs in #check {{ P }} hl(if #1 < #2 then #1 + #1 else #0) {{ x, RET x; Q }} -/-- info: iprop(∀ Φ, P -∗ (▷ ∀ v, ⌜v = hl_val(#1)⌝ → Φ v) -∗ WP hl(#1) {{ Φ }} ) : PROP -/ +/-- info: iprop(∀ Φ, P -∗ (▷ ∀ v, ⌜v = hl_val(#1)⌝ -∗ Φ v) -∗ WP hl(#1) {{ Φ }} ) : PROP -/ #guard_msgs in #check ({{ P }} hl(#1) {{ v, RET v; ⌜v = hl_val(#1)⌝ }} : PROP) end HeapLangTestTexanTriple From 557c7b7d9d242e2ce51e2384ff1896c6960105fc Mon Sep 17 00:00:00 2001 From: ayhon Date: Sat, 18 Jul 2026 16:09:50 +0200 Subject: [PATCH 3/6] feat: prohibit whitespace between brackets in WP and texan triples --- Iris/Iris/BI/WeakestPre.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Iris/Iris/BI/WeakestPre.lean b/Iris/Iris/BI/WeakestPre.lean index d0deff3f5..4d9c66e42 100644 --- a/Iris/Iris/BI/WeakestPre.lean +++ b/Iris/Iris/BI/WeakestPre.lean @@ -63,8 +63,8 @@ declare_syntax_cat wpPostcond -- example {a : PUnit.{i}} : PUnit.{i} := a -- ^^ -- see: https://github.com/leanprover-community/iris-lean/pull/393 -syntax " {" "{ " wpPostcondInner " }" "} " : wpPostcond -syntax " [" "{ " wpPostcondInner " }" "] " : wpPostcond +syntax " {" noWs "{ " wpPostcondInner " }" noWs "} " : wpPostcond +syntax " [" noWs "{ " wpPostcondInner " }" noWs "] " : wpPostcond syntax " ⦃ " wpPostcondInner " ⦄ " : wpPostcond syntax " 〖 " wpPostcondInner " 〗 " : wpPostcond @@ -72,10 +72,10 @@ syntax (name := wp) "WP " wpExpr wpPostcond : term syntax texanPostcondInner := (ident+ ", ")? " RET " term:min "; " term:min declare_syntax_cat texanPostcond -syntax " {" "{ " texanPostcondInner " }" "} " : texanPostcond +syntax " {" noWs "{ " texanPostcondInner " }" noWs "} " : texanPostcond syntax " ⦃ " texanPostcondInner " ⦄ " : texanPostcond declare_syntax_cat texanPrecond -syntax " {" "{ " term:min " }" "} " : texanPrecond +syntax " {" noWs "{ " term:min " }" noWs "} " : texanPrecond syntax " ⦃ " term:min " ⦄ " : texanPrecond syntax (name := texanTriple) texanPrecond wpExpr texanPostcond : term From efdc3e429097d8c82d1800ce9ab9d192b40feb5e Mon Sep 17 00:00:00 2001 From: ayhon Date: Sat, 18 Jul 2026 16:12:26 +0200 Subject: [PATCH 4/6] feat: allow specifying binder type in texan triples --- Iris/Iris/BI/WeakestPre.lean | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/Iris/Iris/BI/WeakestPre.lean b/Iris/Iris/BI/WeakestPre.lean index 4d9c66e42..f9617aa83 100644 --- a/Iris/Iris/BI/WeakestPre.lean +++ b/Iris/Iris/BI/WeakestPre.lean @@ -70,7 +70,7 @@ syntax " 〖 " wpPostcondInner " 〗 " : wpPostcond syntax (name := wp) "WP " wpExpr wpPostcond : term -syntax texanPostcondInner := (ident+ ", ")? " RET " term:min "; " term:min +syntax texanPostcondInner := ((ppSpace (binderIdent <|> bracketedBinder))+ ", ")? " RET " term:min "; " term:min declare_syntax_cat texanPostcond syntax " {" noWs "{ " texanPostcondInner " }" noWs "} " : texanPostcond syntax " ⦃ " texanPostcondInner " ⦄ " : texanPostcond @@ -126,10 +126,18 @@ meta def wpMacro : Lean.Macro := fun stx => do @[macro texanTriple] meta def wpTexanTriple : Lean.Macro - | `(⦃ $P:term ⦄ $wpExpr ⦃ $[$[$xs:ident]* ,]? RET $pat ; $Q:term ⦄) - | `({{ $P:term }} $wpExpr {{ $[$[$xs:ident]* ,]? RET $pat ; $Q:term }}) => do + | `(⦃ $P:term ⦄ $wpExpr ⦃ $[$[$xs]* ,]? RET $pat ; $Q:term ⦄) + | `({{ $P:term }} $wpExpr {{ $[$[$xs]* ,]? RET $pat ; $Q:term }}) => do + + let transform (xs : Array (TSyntax [`Lean.binderIdent, `Lean.Parser.Term.bracketedBinder])) : MacroM <| TSyntaxArray [`ident, `Lean.Parser.Term.hole, `Lean.Parser.Term.bracketedBinder] := + xs.mapM fun + | `(binderIdent|_) => `(hole|_) + | `(binderIdent|$i:ident) => `(ident|$i) + | `(bracketedBinder|$x) => `(bracketedBinder|$x) + let k ← match xs with | some xs => + let xs ← transform xs -- TSyntax cast `(iprop(∀ $xs*, $Q:term -∗ Φ $pat)) | none => `($Q:term -∗ Φ $pat) `(iprop(∀ Φ, $P -∗ ▷ $k -∗ (WP $wpExpr {{ Φ }}))) From 6522c8b3592a243f48bb6acb025bcdd1ae2ca0fd Mon Sep 17 00:00:00 2001 From: ayhon Date: Sat, 18 Jul 2026 22:04:16 +0200 Subject: [PATCH 5/6] feat: lazycoin example --- Iris/Iris/HeapLang/Lib/LazyCoin.lean | 138 +++++++++++++++++++++++++ Iris/Iris/HeapLang/Lib/NondetBool.lean | 56 ++++++++++ Iris/Iris/HeapLang/PrimitiveLaws.lean | 30 +++++- Iris/Iris/Std/CoPset.lean | 2 + 4 files changed, 225 insertions(+), 1 deletion(-) create mode 100644 Iris/Iris/HeapLang/Lib/LazyCoin.lean create mode 100644 Iris/Iris/HeapLang/Lib/NondetBool.lean diff --git a/Iris/Iris/HeapLang/Lib/LazyCoin.lean b/Iris/Iris/HeapLang/Lib/LazyCoin.lean new file mode 100644 index 000000000..cfffd7d5a --- /dev/null +++ b/Iris/Iris/HeapLang/Lib/LazyCoin.lean @@ -0,0 +1,138 @@ +module + +public import Iris.HeapLang +public import Iris.BI +public import Iris.HeapLang.Lib.NondetBool + +namespace Iris.HeapLang + +-- type Coin := Ref (Option Bool) × ProphId +def newCoin := hl_val% + λ _, (ref(none()), newProph()) + +-- readCoin(cp : Coin) : Bool +def readCoin := hl_val% + λ cp, + let c := fst(cp); + let p := snd(cp); + match !c with + | none() => -- The prophecy hasn't been resolved yet + let r := &nondetBool #(); + c ← some(r); + resolveProph(p, r); + r + | some(v) => -- The prophecy has been resolved already + v + +variable [HeapLangGS hlc GF] + +section Proofs + +open HeapLang + +def prophecyToBool (vs : List (Val × Val)) : Bool := + if let some (_, v) := vs.head? then + v = hl_val(#true) + else false + +@[simp, grind =] +theorem prophecyToBool_of_bool (vs : List (Val × Val)) (v : Val) (b : Bool) : + prophecyToBool ((v, hl_val(#b)) :: vs) = b := by + cases b <;> rfl + +/-- `cp` is a pair of `c` and `p`, where if p is a prophecy with resolutions `vs` + such that if `c` is non-null, it points to the first resolution value of `vs` -/ +def coin (cp : Val) (b : Bool) : IProp GF := iprop% + ∃ (c : Loc) (p : ProphId) (vs : List (Val × Val)), + ⌜ cp = hl_val((#c, #p)) ⌝ ∗ proph p vs ∗ + (c ↦ hl_val(some(#b)) ∨ (c ↦ hl_val(none()) ∗ ⌜ b = prophecyToBool vs ⌝)) + +def coin2 (cp : Val) (b : Bool) : IProp GF := iprop% + ∃ (c : Loc) (p : ProphId) (vs : List (Val × Val)), + ⌜ cp = hl_val((#c, #p)) ⌝ ∗ proph p vs ∗ ∃ (v : Val), c ↦ v ∗ + (⌜v = hl_val(some(#b)) ∨ (v = hl_val(none()) ∧ b = prophecyToBool vs )⌝) + +theorem coin_coin2 (cp : Val) (b : Bool) : coin (GF := GF) cp b = coin2 cp b := by + apply Iris.BI.BIBase.BiEntails.to_eq + unfold coin coin2 + constructor + · refine BI.exists_mono fun c => ?_ + refine BI.exists_mono fun p => ?_ + refine BI.exists_mono fun vs => ?_ + refine BI.sep_mono .rfl ?_ + refine BI.sep_mono .rfl ?_ + iintro ⟨_ | ⟨_, %_⟩⟩ + · iexists _ + iframe + itrivial + · iexists _ + iframe + ipureintro + grind + · refine BI.exists_mono fun c => ?_ + refine BI.exists_mono fun p => ?_ + refine BI.exists_mono fun vs => ?_ + refine BI.sep_mono .rfl ?_ + refine BI.sep_mono .rfl ?_ + iintro ⟨%v, Hc, (%eq | ⟨%eq, _⟩)⟩ <;> subst eq + · ileft; iframe + · iright; iframe + +theorem newCoin.spec : ⊢@{IProp GF} + {{ True }} hl(&newCoin #()) {{ c b, RET c; coin c b }} := by + iintro %Φ - K + unfold newCoin + wp_pures + wp_bind newProph() + ihave ∗aux := wp_new_proph + iapply wp_strong_mono (Std.IsPreorder.le_refl _) CoPset.subseteq_refl $$ aux + iintro %v ⟨%p, %pvs, %eq, h⟩ !>; subst eq + wp_pures + wp_bind ref(_) + iapply wp_alloc + iintro %l !> Hl + wp_pures + iintro !> + iapply K + unfold coin + iexists l, p, pvs + isplitl []; itrivial + iframe + iright + iframe + ipureintro + rfl + +theorem readCoin.spec (cp : Val) (b : Bool) : ⊢@{IProp GF} + {{ coin cp b }} hl(&readCoin &cp) {{ RET hl_val(#b); coin cp b }} := by + conv => enter [1,1]; unfold coin + iintro %Φ ⟨%c, %p, %pvs, %cp_eq, proph, disj⟩ K + unfold readCoin + subst cp_eq + wp_pures + wp_bind !_ + icases disj with (Hsome | ⟨Hnone, %b_eq⟩) + · iapply wp_load $$ Hsome + iintro !> Hc + wp_pures + iintro !> + iapply K + iexists c, p, pvs + iframe; ipureintro; rfl + · subst b_eq + iapply wp_load $$ Hnone + iintro !> Hc + wp_pures + wp_bind &nondetBool _; iapply nondetBool.spec $$ [//]; iintro !> %b - + wp_pures + wp_bind _ ← _; iapply wp_store $$ Hc; iintro !> Hc + wp_pure; wp_pure + wp_bind resolveProph(_, _); iapply wp_resolve_proph $$ proph + iintro %pvs' %pvs_eq proph + subst pvs_eq + wp_pures + iintro !> + simp only [prophecyToBool_of_bool] + iapply K + iexists c, p, pvs' + iframe; ipureintro; rfl diff --git a/Iris/Iris/HeapLang/Lib/NondetBool.lean b/Iris/Iris/HeapLang/Lib/NondetBool.lean new file mode 100644 index 000000000..24fff8872 --- /dev/null +++ b/Iris/Iris/HeapLang/Lib/NondetBool.lean @@ -0,0 +1,56 @@ +module + +public import Iris.ProgramLogic.WeakestPre +public import Iris.HeapLang.ProofMode +public import Iris.HeapLang.PrimitiveLaws +public import Iris.Instances.Lib.Invariants + +namespace Iris.HeapLang + +public section + +variable [HeapLangGS hlc GF] + +def nondetBool := hl_val% λ _, + let l := ref(#true); + fork( + l ← #false + ); + !l + +theorem nondetBool.spec : ⊢@{IProp GF} + {{ True }} hl(&nondetBool #()) {{ (b : Bool), RET hl_val(#b); True }} := by + iintro %Φ - K + unfold nondetBool + wp_pures + wp_bind ref(_) + iapply wp_alloc + iintro %l !> Hl + wp_pures + iapply fupd_wp + ihave >#inv := inv_alloc `rnd ⊤ iprop(∃ (b : Bool), l ↦ hl_val(#b)) $$ [Hl] + · iexists ?_; iassumption + iintro !> + wp_bind fork(_) + iapply wp_fork $$ [K] [] + · inext + wp_pures + iapply wp_atomic + ihave >⟨⟨%b, Hl⟩, Hclose⟩ := inv_acc CoPset.subseteq_top $$ inv + iintro !> + iapply wp_load $$ Hl + iintro !> Hl + ihave aux := Hclose $$ [Hl] + · iexists ?_; iassumption + icases aux with >- + iintro !> + iapply K $$ [//] + · inext + iapply wp_atomic + ihave >⟨⟨%b, Hl⟩, Hclose⟩ := inv_acc CoPset.subseteq_top $$ inv + iintro !> + iapply wp_store $$ Hl + iintro !> Hl + iapply Hclose + iexists ?_ + iassumption diff --git a/Iris/Iris/HeapLang/PrimitiveLaws.lean b/Iris/Iris/HeapLang/PrimitiveLaws.lean index 9e1a724c3..403dea6ec 100644 --- a/Iris/Iris/HeapLang/PrimitiveLaws.lean +++ b/Iris/Iris/HeapLang/PrimitiveLaws.lean @@ -605,7 +605,7 @@ theorem wp_resolve_strong {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × iapply HΦ $$ %pvs'' %hpvs'_eq Hele theorem wp_resolve {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × Val)} - (hatom : Language.Atomic Language.Atomicity.StronglyAtomic e) (hne : toVal e = none) : + (hatom : Language.Atomic Language.Atomicity.StronglyAtomic e) (hne : toVal e = none := by decide) : proph p pvs -∗ WP e @ s; E {{ r, ∀ pvs', ⌜pvs = (r, w) :: pvs'⌝ -∗ proph p pvs' -∗ Φ r }} -∗ WP hl(resolve(&e, v(#p), v(&w))) @ s; E {{ Φ }} := by @@ -618,6 +618,34 @@ theorem wp_resolve {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × Val)} iframe Hp iexact Hcont +theorem wp_resolve_proph {p : ProphId} {w : Val} {pvs : List (Val × Val)} : + proph p pvs -∗ + (∀ pvs', ⌜pvs = (hl_val(#()), w) :: pvs'⌝ -∗ proph p pvs' -∗ Φ hl_val(#())) -∗ + WP hl(resolveProph(v(#p), v(&w))) @ s; E {{ Φ }} := by + iintro proph K + let Ki := ECtxItem.resolveL (ECtxItem.appL hl_val(#())) hl_val(#p) hl_val(&w) + have shape: hl(resolveProph(#p ,&w)) = fill (Expr := Exp) [Ki] hl(λ _, #()) := by + simp [fillItem, Ki, ECtxItem.fill] + rw [shape] + iapply wp_bind + iapply wp_pure_step_fupd (Hφ := ⟨⟩) + simp only [Nat.repeat, EctxItemLanguage.fill_cons, fillItem, ECtxItem.fill, EctxItemLanguage.fill_nil, wp_value_iff, Ki] + iintro !> !> !> _ !> + have hatom : Language.Atomic Language.Atomicity.StronglyAtomic hl((v(λ _, #())) #()) := by + constructor + intro σ _ _ _ _ h + apply prim_step_to_val_always_to_val (κsₐ := []) (σ₁ₐ := σ) ?next h + case next => + apply ProgramLogic.EctxLanguage.primStep_of_baseStep + simp only [BaseStep.baseStep, val_to_ofVal] + constructor + rfl + iapply wp_resolve hatom (hne := by decide) $$ proph + iapply wp_rec rfl + simp only [Exp.subst, wp_value_iff] + iintro !> !> + iassumption + end Lifting end Iris.HeapLang diff --git a/Iris/Iris/Std/CoPset.lean b/Iris/Iris/Std/CoPset.lean index c860d2776..2b221ca75 100644 --- a/Iris/Iris/Std/CoPset.lean +++ b/Iris/Iris/Std/CoPset.lean @@ -371,6 +371,8 @@ theorem not_in_union {p} {X1 X2 : CoPset} : ¬ p ∈ X1 ∪ X2 <-> ¬ p ∈ X1 · exact ⟨(Hu <| in_union.mpr <| .inl ·), (Hu <| in_union.mpr <| .inr ·)⟩ · exact in_union.mp Hu |>.elim H1 H2 +@[refl] theorem subseteq_refl {X : CoPset} : X ⊆ X := λ _ => id + theorem subseteq_trans {X Y Z : CoPset} (Hxy : X ⊆ Y) (Hyz : Y ⊆ Z) : X ⊆ Z := fun p => (Hyz p) ∘ (Hxy p) From ddb886b23acc1cc6e6a0c11af14c113abace5324 Mon Sep 17 00:00:00 2001 From: ayhon Date: Sat, 18 Jul 2026 22:15:27 +0200 Subject: [PATCH 6/6] cleanup --- Iris/Iris/HeapLang/Lib/LazyCoin.lean | 33 +--------------------------- 1 file changed, 1 insertion(+), 32 deletions(-) diff --git a/Iris/Iris/HeapLang/Lib/LazyCoin.lean b/Iris/Iris/HeapLang/Lib/LazyCoin.lean index cfffd7d5a..132cd3688 100644 --- a/Iris/Iris/HeapLang/Lib/LazyCoin.lean +++ b/Iris/Iris/HeapLang/Lib/LazyCoin.lean @@ -24,7 +24,7 @@ def readCoin := hl_val% | some(v) => -- The prophecy has been resolved already v -variable [HeapLangGS hlc GF] +variable {hlc GF} [HeapLangGS hlc GF] section Proofs @@ -47,37 +47,6 @@ def coin (cp : Val) (b : Bool) : IProp GF := iprop% ⌜ cp = hl_val((#c, #p)) ⌝ ∗ proph p vs ∗ (c ↦ hl_val(some(#b)) ∨ (c ↦ hl_val(none()) ∗ ⌜ b = prophecyToBool vs ⌝)) -def coin2 (cp : Val) (b : Bool) : IProp GF := iprop% - ∃ (c : Loc) (p : ProphId) (vs : List (Val × Val)), - ⌜ cp = hl_val((#c, #p)) ⌝ ∗ proph p vs ∗ ∃ (v : Val), c ↦ v ∗ - (⌜v = hl_val(some(#b)) ∨ (v = hl_val(none()) ∧ b = prophecyToBool vs )⌝) - -theorem coin_coin2 (cp : Val) (b : Bool) : coin (GF := GF) cp b = coin2 cp b := by - apply Iris.BI.BIBase.BiEntails.to_eq - unfold coin coin2 - constructor - · refine BI.exists_mono fun c => ?_ - refine BI.exists_mono fun p => ?_ - refine BI.exists_mono fun vs => ?_ - refine BI.sep_mono .rfl ?_ - refine BI.sep_mono .rfl ?_ - iintro ⟨_ | ⟨_, %_⟩⟩ - · iexists _ - iframe - itrivial - · iexists _ - iframe - ipureintro - grind - · refine BI.exists_mono fun c => ?_ - refine BI.exists_mono fun p => ?_ - refine BI.exists_mono fun vs => ?_ - refine BI.sep_mono .rfl ?_ - refine BI.sep_mono .rfl ?_ - iintro ⟨%v, Hc, (%eq | ⟨%eq, _⟩)⟩ <;> subst eq - · ileft; iframe - · iright; iframe - theorem newCoin.spec : ⊢@{IProp GF} {{ True }} hl(&newCoin #()) {{ c b, RET c; coin c b }} := by iintro %Φ - K