From 3737904bcd18f50c0a1d4e6b425f613fc4b6b99d Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Sat, 4 Jul 2026 20:01:42 +0200 Subject: [PATCH 1/3] perf: compute the solver's up/down pair by a single recursion Fix.Impl.up and Fix.Impl.down were mutually recursive, so the compiled code for either hom at level k+1 recomputes both branches at every level, which is 2^k recursive calls. Computing the pair at every level by a single recursion makes that O(k). All solver proofs are unchanged up to structure eta. --- Iris/Iris/Algebra/COFESolver.lean | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/Iris/Iris/Algebra/COFESolver.lean b/Iris/Iris/Algebra/COFESolver.lean index 4c3f6eb44..05a35f0e1 100644 --- a/Iris/Iris/Algebra/COFESolver.lean +++ b/Iris/Iris/Algebra/COFESolver.lean @@ -35,16 +35,20 @@ instance instA (n) : COFE (A F n) := (A' F n).2 #rocq_ignore solver.A_cofe "Inference succeeds automatically via `instA`/`instA'`" variable (F) in -mutual +/-- The section/retraction pair at every level, computed by a single recursion so +that evaluating either component at level `k` costs `O(k)` (the naive mutual +recursion recomputes both branches at every level, which is `2^k`). -/ +def updown : ∀ k, (A F k -n> A F (k+1)) × (A F (k+1) -n> A F k) + | 0 => (⟨fun _ => inh.default, ⟨fun _ _ _ _ => .rfl⟩⟩, ⟨fun _ => ⟨()⟩, ⟨fun _ _ _ _ => .rfl⟩⟩) + | k+1 => let (u, d) := updown k; (map d u, map u d) + +variable (F) in @[rocq_alias solver.f] -def up : ∀ k, A F k -n> A F (k+1) - | 0 => ⟨fun _ => inh.default, ⟨fun _ _ _ _ => .rfl⟩⟩ - | k+1 => map (down k) (up k) +def up (k : Nat) : A F k -n> A F (k+1) := (updown F k).1 + +variable (F) in -- rocq_alias solver.g -def down : ∀ k, A F (k+1) -n> A F k - | 0 => ⟨fun _ => ⟨()⟩, ⟨fun _ _ _ _ => .rfl⟩⟩ - | k+1 => map (up k) (down k) -end +def down (k : Nat) : A F (k+1) -n> A F k := (updown F k).2 #rocq_ignore solver.f_S "Not needed" #rocq_ignore solver.g_S "Not needed" From d3193659b035b26cf9f408953513600737926fe0 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Sun, 5 Jul 2026 11:37:08 +0200 Subject: [PATCH 2/3] test: guard the runtime cost of the solver's up/down pair Iris.Tests.COFESolverEval round-trips a value through tower level 21 at runtime and reads back a Nat payload, so the up/down homs must actually be constructed by the compiled code. The cost is checked against a pure baseline computation timed in the same interpreter, which makes the budget machine-independent: the paired recursion costs a few baseline units, while recomputing the two branches at every level costs several hundred and fails the budget deterministically instead of hanging the build. The depth and baseline size can be overridden via environment variables for experiments. --- Iris/Iris/Algebra/COFESolver.lean | 2 +- Iris/Iris/Tests/COFESolverEval.lean | 78 +++++++++++++++++++++++++++++ 2 files changed, 79 insertions(+), 1 deletion(-) create mode 100644 Iris/Iris/Tests/COFESolverEval.lean diff --git a/Iris/Iris/Algebra/COFESolver.lean b/Iris/Iris/Algebra/COFESolver.lean index 05a35f0e1..f941bbe04 100644 --- a/Iris/Iris/Algebra/COFESolver.lean +++ b/Iris/Iris/Algebra/COFESolver.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2025 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Mario Carneiro +Authors: Mario Carneiro, Sebastian Graf -/ module diff --git a/Iris/Iris/Tests/COFESolverEval.lean b/Iris/Iris/Tests/COFESolverEval.lean new file mode 100644 index 000000000..132eb8536 --- /dev/null +++ b/Iris/Iris/Tests/COFESolverEval.lean @@ -0,0 +1,78 @@ +/- +Copyright (c) 2026 Sebastian Graf. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Graf +-/ +-- Deliberately not a `module`: since `module`s can only import `module`s, it +-- is not listed in `Iris.Tests`; the `IrisTest` glob builds it. +-- module + +import Iris.Algebra.COFESolver + +/-! +Regression guard for the runtime cost of the solver's section/retraction pair. + +`Fix.Impl.up`/`Fix.Impl.down` are computed by a single recursion producing the +pair at every level, so evaluating either hom at level `k` makes `O(k)` +recursive calls; recomputing the two branches separately at every level makes +that `2^k`. + +The `#eval` round-trips a value through level `k = 21` of the tower and reads +back a `Nat` threaded through the `constOF` component, so the hom construction +is demanded at runtime and cannot be erased as dead code. Compiled evaluation +is not subject to `maxHeartbeats`, so the check is a wall-clock budget, +calibrated against a pure baseline computation timed in the same interpreter +so that machine speed cancels out: the healthy path costs a few baseline +units, the exponential path several hundred. The exponential path still +terminates at this depth (in tens of seconds), so a regression fails with the +budget error rather than hanging the build. +-/ + +namespace Iris.Tests.COFESolverEval + +open Iris Iris.COFE Iris.COFE.OFunctor Iris.COFE.OFunctor.Fix.Impl OFE + +/-- A functor whose `map` captures both the covariant and the contravariant +hom (via `HomOF`), with a `LeibnizO Nat` payload to read back (via `constOF`). +The capture forces both components of the up/down pair at every level when the +homs are constructed at runtime. -/ +abbrev F : ∀ (α β : Type), [COFE α] → [COFE β] → Type := + ProdOF (HomOF (LaterOF IdOF) (LaterOF IdOF)) (constOF (LeibnizO Nat)) + +instance : Inhabited (F (ULift Unit) (ULift Unit)) := ⟨Hom.id, ⟨42⟩⟩ + +/-- Round-trip the seed value up to level `1 + k` of the tower and back down to +level `1`, returning the `Nat` payload. `k` stays a runtime value, so no +elaboration-time reduction of `A F k` is involved: the cost measured is that of +running the compiled `up`/`down`. -/ +def roundTrip (k : Nat) : Nat := + let x1 : A F 1 := up F 0 ⟨()⟩ + let xk : A F (1 + k) := upN F (k := 1) k x1 + let y1 : A F 1 := downN F (k := 1) k xk + (y1 : (Later (ULift Unit) -n> Later (ULift Unit)) × LeibnizO Nat).2.car + +#eval show IO Unit from do + -- Reading these at runtime keeps the round-trip from being lifted out as a + -- closed term and evaluated before the timestamps. + let k := ((← IO.getEnv "COFESOLVER_EVAL_DEPTH").bind (·.toNat?)).getD 21 + let n := ((← IO.getEnv "COFESOLVER_EVAL_BASELINE").bind (·.toNat?)).getD 200000 + -- Baseline unit: a pure fold in the same interpreter. + let b0 ← IO.monoNanosNow + let base := (List.range n).foldl (· + ·) 0 + unless base == n * (n - 1) / 2 do + throw <| IO.userError "COFESolverEval: baseline computed a wrong sum" + let b1 ← IO.monoNanosNow + -- The measured round-trip. + let t0 ← IO.monoNanosNow + let v := roundTrip k + unless v == 42 do + throw <| IO.userError s!"COFESolverEval: expected 42, got {v}" + let t1 ← IO.monoNanosNow + let baseline := max (b1 - b0) 1 + let ratio := (t1 - t0) / baseline + if ratio > 20 then + throw <| IO.userError s!"COFESolverEval: `down F {k}` cost {ratio} baseline \ + units (limit 20); the up/down pair is being recomputed exponentially" + IO.println s!"COFESolverEval: ok ({ratio} baseline units)" + +end Iris.Tests.COFESolverEval From db799f16a64eacecbfa6fcf369f7f8cbb19cbe5c Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Tue, 7 Jul 2026 12:22:16 +0200 Subject: [PATCH 3/3] Delete Iris/Iris/Tests/COFESolverEval.lean --- Iris/Iris/Tests/COFESolverEval.lean | 78 ----------------------------- 1 file changed, 78 deletions(-) delete mode 100644 Iris/Iris/Tests/COFESolverEval.lean diff --git a/Iris/Iris/Tests/COFESolverEval.lean b/Iris/Iris/Tests/COFESolverEval.lean deleted file mode 100644 index 132eb8536..000000000 --- a/Iris/Iris/Tests/COFESolverEval.lean +++ /dev/null @@ -1,78 +0,0 @@ -/- -Copyright (c) 2026 Sebastian Graf. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Sebastian Graf --/ --- Deliberately not a `module`: since `module`s can only import `module`s, it --- is not listed in `Iris.Tests`; the `IrisTest` glob builds it. --- module - -import Iris.Algebra.COFESolver - -/-! -Regression guard for the runtime cost of the solver's section/retraction pair. - -`Fix.Impl.up`/`Fix.Impl.down` are computed by a single recursion producing the -pair at every level, so evaluating either hom at level `k` makes `O(k)` -recursive calls; recomputing the two branches separately at every level makes -that `2^k`. - -The `#eval` round-trips a value through level `k = 21` of the tower and reads -back a `Nat` threaded through the `constOF` component, so the hom construction -is demanded at runtime and cannot be erased as dead code. Compiled evaluation -is not subject to `maxHeartbeats`, so the check is a wall-clock budget, -calibrated against a pure baseline computation timed in the same interpreter -so that machine speed cancels out: the healthy path costs a few baseline -units, the exponential path several hundred. The exponential path still -terminates at this depth (in tens of seconds), so a regression fails with the -budget error rather than hanging the build. --/ - -namespace Iris.Tests.COFESolverEval - -open Iris Iris.COFE Iris.COFE.OFunctor Iris.COFE.OFunctor.Fix.Impl OFE - -/-- A functor whose `map` captures both the covariant and the contravariant -hom (via `HomOF`), with a `LeibnizO Nat` payload to read back (via `constOF`). -The capture forces both components of the up/down pair at every level when the -homs are constructed at runtime. -/ -abbrev F : ∀ (α β : Type), [COFE α] → [COFE β] → Type := - ProdOF (HomOF (LaterOF IdOF) (LaterOF IdOF)) (constOF (LeibnizO Nat)) - -instance : Inhabited (F (ULift Unit) (ULift Unit)) := ⟨Hom.id, ⟨42⟩⟩ - -/-- Round-trip the seed value up to level `1 + k` of the tower and back down to -level `1`, returning the `Nat` payload. `k` stays a runtime value, so no -elaboration-time reduction of `A F k` is involved: the cost measured is that of -running the compiled `up`/`down`. -/ -def roundTrip (k : Nat) : Nat := - let x1 : A F 1 := up F 0 ⟨()⟩ - let xk : A F (1 + k) := upN F (k := 1) k x1 - let y1 : A F 1 := downN F (k := 1) k xk - (y1 : (Later (ULift Unit) -n> Later (ULift Unit)) × LeibnizO Nat).2.car - -#eval show IO Unit from do - -- Reading these at runtime keeps the round-trip from being lifted out as a - -- closed term and evaluated before the timestamps. - let k := ((← IO.getEnv "COFESOLVER_EVAL_DEPTH").bind (·.toNat?)).getD 21 - let n := ((← IO.getEnv "COFESOLVER_EVAL_BASELINE").bind (·.toNat?)).getD 200000 - -- Baseline unit: a pure fold in the same interpreter. - let b0 ← IO.monoNanosNow - let base := (List.range n).foldl (· + ·) 0 - unless base == n * (n - 1) / 2 do - throw <| IO.userError "COFESolverEval: baseline computed a wrong sum" - let b1 ← IO.monoNanosNow - -- The measured round-trip. - let t0 ← IO.monoNanosNow - let v := roundTrip k - unless v == 42 do - throw <| IO.userError s!"COFESolverEval: expected 42, got {v}" - let t1 ← IO.monoNanosNow - let baseline := max (b1 - b0) 1 - let ratio := (t1 - t0) / baseline - if ratio > 20 then - throw <| IO.userError s!"COFESolverEval: `down F {k}` cost {ratio} baseline \ - units (limit 20); the up/down pair is being recomputed exponentially" - IO.println s!"COFESolverEval: ok ({ratio} baseline units)" - -end Iris.Tests.COFESolverEval