From 585d2f7102e613c00b2a185182379ba19ee7cdc6 Mon Sep 17 00:00:00 2001
From: jotabulacios <jbulacios@fi.uba.ar>
Date: Mon, 2 Nov 2026 14:57:09 -0300
Subject: [PATCH 1/6] Build the model on the counted-pulls branch of the Clean
 fork, and prove the counted channel consistent there.

The lakefile points at the fork branch, which adds pulls of multiplicity up to N, a counted channel
and soundness by finishing order on top of Clean f3abad7c. For now it is a path dependency on the
build server (../../clean-fork-main); it becomes a git dependency on yetanotherco/clean once the
branch is pushed. Channels/Counted.lean gains consistentUpTo: under BalancedUpTo N, which the fork's
balance checks provide, the counted channel is consistent. It is the positive counterpart of
not_consistent, which still shows the gap under BalancedInteractions alone.
---
 formal/LambdaVM/Channels/Counted.lean | 31 ++++++++++++++++++++++++++-
 formal/lake-manifest.json             |  8 +++----
 formal/lakefile.toml                  |  5 +++--
 3 files changed, 36 insertions(+), 8 deletions(-)

diff --git a/formal/LambdaVM/Channels/Counted.lean b/formal/LambdaVM/Channels/Counted.lean
index 85a826a16..f0640db5b 100644
--- a/formal/LambdaVM/Channels/Counted.lean
+++ b/formal/LambdaVM/Channels/Counted.lean
@@ -19,7 +19,9 @@ The price is in the balance premise. `exists_push_of_pull` needs `N · length <
 `BalancedInteractions` only matches pulls of multiplicity `1`, and counts a pull of any other
 nonzero multiplicity as a push; `not_consistent` shows the gap is real: for `N ≥ 2` the counted
 channel is not `Consistent`, so it cannot be finished in a `SoundEnsemble` until that premise
-carries the bound. With `N = 1` everything coincides (`counted 1 channel` is `Normal`).
+carries the bound. With `N = 1` everything coincides (`counted 1 channel` is `Normal`). With the
+bounded balance `BalancedUpTo N` of the modified Clean (`counted-pulls`), `consistentUpTo` closes
+the gap.
 -/
 
 namespace LambdaVM.Counted
@@ -275,6 +277,33 @@ theorem not_consistent (N : ℕ) (hN : 2 ≤ N) (hN' : N ≤ 255)
   convert h
   simp [ProvableType.fromElements_toElements]
 
+/-- With the bounded balance of the modified Clean (`BalancedUpTo N`, the premise `not_consistent`
+asks for), the counted channel is consistent: a pull of `1, …, N` is matched by an interaction
+that is not such a pull, and that interaction's requirement is the guarantee. -/
+instance consistentUpTo (N : ℕ) (channel : Channel (F p) Message) :
+    (counted N channel).ConsistentUpTo N where
+  consistent interactions data balanced reqs a a_mem := by
+    obtain ⟨ a_channel, - ⟩ := reqs a a_mem
+    by_cases a_pull : a.PullUpTo N
+    case neg =>
+      rcases a with ⟨ _, a_direction, a_mult, a_msg, a_size ⟩
+      subst a_channel
+      simp only [Interaction.Guarantees, counted]
+      exact fun h_direction h_count => absurd ⟨ h_direction, h_count ⟩ a_pull
+    obtain ⟨ b, b_mem, b_msg, b_ne_zero, b_not_pull ⟩ := balanced.matchedUpTo a a_mem a_pull
+    obtain ⟨ b_channel, b_reqs ⟩ := reqs b b_mem
+    rcases a with ⟨ _, a_direction, a_mult, a_msg, a_size ⟩
+    rcases b with ⟨ _, b_direction, b_mult, b_msg', b_size ⟩
+    subst a_channel b_channel
+    simp only at b_msg
+    subst b_msg
+    simp only [Interaction.Guarantees, Interaction.Requirements, Interaction.msgVector,
+      counted] at b_reqs ⊢
+    intro _ _
+    cases b_direction with
+    | push => exact b_reqs b_ne_zero
+    | pull => exact b_reqs b_ne_zero (b_not_pull rfl)
+
 end LambdaVM.Counted
 
 /-! ## A deduplicated row
diff --git a/formal/lake-manifest.json b/formal/lake-manifest.json
index ca5842997..288e99646 100644
--- a/formal/lake-manifest.json
+++ b/formal/lake-manifest.json
@@ -1,15 +1,13 @@
 {"version": "1.3.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/Verified-zkEVM/clean",
-   "type": "git",
-   "subDir": null,
+ [{"type": "path",
    "scope": "",
-   "rev": "f3abad7c099e49f847836c1883dd9e7c539f06f9",
    "name": "Clean",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "f3abad7c099e49f847836c1883dd9e7c539f06f9",
    "inherited": false,
+   "dir": "../../clean-fork-main",
+   "copy": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/Verified-zkEVM/CompPoly.git",
    "type": "git",
diff --git a/formal/lakefile.toml b/formal/lakefile.toml
index 8c801fdea..f2deaa523 100644
--- a/formal/lakefile.toml
+++ b/formal/lakefile.toml
@@ -6,10 +6,11 @@ autoImplicit = false
 relaxedAutoImplicit = false
 
 # Clean pinned to a revision; Mathlib and CompPoly come in through Clean's manifest.
+# PoC: Clean local con pulls contados y orden por cierre de canales (rama counted-pulls).
+# La ruta es la del servidor de builds (~/lvc/formal-bump435/formal -> ~/lvc/clean-fork-main).
 [[require]]
 name = "Clean"
-git = "https://github.com/Verified-zkEVM/clean"
-rev = "f3abad7c099e49f847836c1883dd9e7c539f06f9"
+path = "../../clean-fork-main"
 
 [[lean_lib]]
 name = "LambdaVM"

From b9072b31f7be52f081cc8a4d407953d6e8d4a954 Mon Sep 17 00:00:00 2001
From: jotabulacios <jbulacios@fi.uba.ar>
Date: Mon, 2 Nov 2026 14:57:09 -0300
Subject: [PATCH 2/6] Let LT answer up to 255 identical queries per row, as the
 Rust chip does.

mu is now a byte instead of a bit: the row pulls IS_HALF and MSB16 with multiplicity mu through
counted channels, and bounds mu by pulling ARE_BYTES[mu, 0]. The row spec holds for rows with
mu != 0, and the honest prover keeps mu below 2^8. With this the Lean LT chip matches the Rust one
exactly, so lean_diff.rs no longer expects the mu bit constraint on the Lean side and ARE_BYTES on
the Rust side; it asserts that no constraint or interaction appears on one side only.
---
 formal/LambdaVM/Tables/Lt.lean | 93 ++++++++++++++++++----------------
 formal/export/lt.json          | 15 ++----
 prover/src/tests/lean_diff.rs  | 18 +++----
 3 files changed, 63 insertions(+), 63 deletions(-)

diff --git a/formal/LambdaVM/Tables/Lt.lean b/formal/LambdaVM/Tables/Lt.lean
index 89de939f8..410a5a8e6 100644
--- a/formal/LambdaVM/Tables/Lt.lean
+++ b/formal/LambdaVM/Tables/Lt.lean
@@ -1,6 +1,7 @@
 module
 
 public import LambdaVM.Tables.Bitwise
+public import Clean.Air.CountedChannel
 public import LambdaVM.Buses.Alu
 public import LambdaVM.Templates.IsBit
 public import LambdaVM.Templates.Add
@@ -70,17 +71,24 @@ theorem core
   rw [Alu.slt_ofNat_iff (by omega) (by omega)]
   split_ifs <;> omega
 
+/-- The largest multiplicity of an LT row: `MU_MAX` in `prover/src/tables/types.rs`. -/
+abbrev muMax : ℕ := 255
+
+/-- `IS_HALF` and `MSB16` with pulls of multiplicity up to `muMax`. -/
+abbrev IsHalfC : RawChannel (F p) := Bitwise.IsHalf.counted muMax
+abbrev Msb16C : RawChannel (F p) := Bitwise.Msb16.counted muMax
+
 def main (r : Var Row (F p)) : Circuit (F p) Unit := do
-  -- μ : Bit here; the spec and lt.rs range-check it as a byte (see README).
-  isBit r.mu
+  -- μ : Byte, as in the spec and lt.rs: ARE_BYTES[μ, 0]
+  Bitwise.AreBytes.pull (r.mu, 0)
   -- range: IS_HALF[lhs[1]], IS_HALF[rhs[1]], IS_BIT<signed>, IS_BIT<invert>
-  Bitwise.IsHalf.pullIf r.mu r.lhs1
-  Bitwise.IsHalf.pullIf r.mu r.rhs1
+  Bitwise.IsHalf.pullUpTo muMax r.mu r.lhs1
+  Bitwise.IsHalf.pullUpTo muMax r.mu r.rhs1
   isBit r.signed
   isBit r.invert
   -- defs: MSB16[lhs[2]] -> lhs_msb, MSB16[rhs[2]] -> rhs_msb
-  Bitwise.Msb16.pullIf r.mu (r.lhs2, r.lhsMsb)
-  Bitwise.Msb16.pullIf r.mu (r.rhs2, r.rhsMsb)
+  Bitwise.Msb16.pullUpTo muMax r.mu (r.lhs2, r.lhsMsb)
+  Bitwise.Msb16.pullUpTo muMax r.mu (r.rhs2, r.rhsMsb)
   let lhsHi := r.lhs1 + 65536 * r.lhs2
   let rhsHi := r.rhs1 + 65536 * r.rhs2
   let subLo := r.lhsSubRhs0 + 65536 * r.lhsSubRhs1
@@ -94,11 +102,11 @@ def main (r : Var Row (F p)) : Circuit (F p) Unit := do
   assertZero (r.res + 2 * r.lt * r.invert - r.lt - r.invert)
   -- sub: IS_BIT<carry[i]>, IS_HALF[lhs_sub_rhs[i]]
   sub ⟨r.lhs0, lhsHi⟩ ⟨r.rhs0, rhsHi⟩ ⟨subLo, subHi⟩
-  Bitwise.IsHalf.pullIf r.mu r.lhsSubRhs0
-  Bitwise.IsHalf.pullIf r.mu r.lhsSubRhs1
-  Bitwise.IsHalf.pullIf r.mu r.lhsSubRhs2
-  Bitwise.IsHalf.pullIf r.mu r.lhsSubRhs3
-  -- output: ALU[lhs, rhs, opsel(LT) + 32·signed + 64·invert] -> [res, 0]
+  Bitwise.IsHalf.pullUpTo muMax r.mu r.lhsSubRhs0
+  Bitwise.IsHalf.pullUpTo muMax r.mu r.lhsSubRhs1
+  Bitwise.IsHalf.pullUpTo muMax r.mu r.lhsSubRhs2
+  Bitwise.IsHalf.pullUpTo muMax r.mu r.lhsSubRhs3
+  -- output: ALU[lhs, rhs, opsel(LT) + 32·signed + 64·invert] -> [res, 0], μ times
   Alu.channel.pushIf r.mu
     ⟨r.lhs0, lhsHi, r.rhs0, rhsHi, 4 + 32 * r.signed + 64 * r.invert, r.res, 0⟩
 
@@ -147,7 +155,7 @@ lemma res_constraint {lt invert res : F p} {ltv iv : ℕ}
 
 /-- The honest prover's row, as `generate_lt_trace` fills it. -/
 def Honest (r : Row (F p)) : Prop :=
-  IsBool r.mu ∧ IsBool r.signed ∧ IsBool r.invert ∧
+  r.mu.val < 2^8 ∧ IsBool r.signed ∧ IsBool r.invert ∧
   r.lhs0.val < 2^32 ∧ r.lhs1.val < 2^16 ∧ r.lhs2.val < 2^16 ∧
   r.rhs0.val < 2^32 ∧ r.rhs1.val < 2^16 ∧ r.rhs2.val < 2^16 ∧
   r.lhsSubRhs0.val < 2^16 ∧ r.lhsSubRhs1.val < 2^16 ∧ r.lhsSubRhs2.val < 2^16 ∧ r.lhsSubRhs3.val < 2^16 ∧
@@ -160,46 +168,46 @@ def Honest (r : Row (F p)) : Prop :=
 
 /-- What an active row establishes: with range-checked low words, `res` is the comparison bit. -/
 def RowSpec (r : Row (F p)) : Prop :=
-  r.mu = 1 → r.lhs0.val < 2^32 → r.rhs0.val < 2^32 →
+  r.mu ≠ 0 → r.lhs0.val < 2^32 → r.rhs0.val < 2^32 →
     r.res = ((ltBit r.signed.val r.invert.val r.lhsVal r.rhsVal : ℕ) : F p)
 
 def circuit : GeneralFormalCircuit (F p) Row unit where
+  name := "LT"
   main
   Spec r _ _ := RowSpec r
-  channelsWithRequirements := [Alu.channel.toRaw]
+  channelsWithRequirements := [Alu.channel.toRaw, IsHalfC, Msb16C]
   requirementsChannelsLawful input_var i₀ := by
-    obtain ⟨lhs0, lhs1, lhs2, rhs0, rhs1, rhs2, signed, lt, lhsSubRhs0, lhsSubRhs1, lhsSubRhs2, lhsSubRhs3,
-      lhsMsb, rhsMsb, invert, res, mu⟩ := input_var
-    simp only [circuit_norm, main, isBit, sub, add, Add.carry0, Add.carry1, Alu.channel,
-      Bitwise.isHalfTable, Bitwise.msb16Table]
-    constructor
-    · intro channel h; tauto
-    · intro env h
-      -- each pull owes a multiplicity of 0 or 1: μ is a bit
-      exact mul_one_sub_eq_zero_iff.mp h.1
+    obtain ⟨lhs0, lhs1, lhs2, rhs0, rhs1, rhs2, signed, lt, lhsSubRhs0, lhsSubRhs1, lhsSubRhs2,
+      lhsSubRhs3, lhsMsb, rhsMsb, invert, res, mu⟩ := input_var
+    simp only [circuit_norm, main, isBit, sub, add, Add.carry0, Add.carry1, IsHalfC, Msb16C,
+      Bitwise.IsHalf, Bitwise.Msb16, Bitwise.AreBytes]
+    intro channel h
+    tauto
 
   soundness := by
     circuit_proof_start [main, isBit, sub, add, Add.carry0, Add.carry1, RowSpec, Row.lhsVal, Row.rhsVal,
-      dword, Alu.channel, Alu.Guarantees, Bitwise.isHalfTable, Bitwise.msb16Table]
-    obtain ⟨h_mu, h_l1, h_r1, h_s, h_i, h_lm, h_rm, h_lt, h_res, h_c0, h_c1, h_s0, h_s1, h_s2, h_s3⟩ :=
-      h_holds
-    -- μ ∈ {0, 1}; with μ = 0 every requirement is vacuous
-    rcases mul_one_sub_eq_zero_iff.mp h_mu with h0 | h1
-    · subst h0; simp
-    subst h1
+      dword, Alu.channel, Alu.Guarantees, Bitwise.isHalfTable, Bitwise.msb16Table, Bitwise.areBytesTable]
+    obtain ⟨⟨h_mu, -⟩, h_l1, h_r1, h_s, h_i, h_lm, h_rm, h_lt, h_res, h_c0, h_c1, h_s0, h_s1, h_s2,
+      h_s3⟩ := h_holds
+    -- with μ = 0 every requirement is vacuous
+    by_cases h0 : input_mu = 0
+    · simp [h0]
+    -- otherwise ARE_BYTES[μ, 0] makes μ a count of at most 255, so the pulls get their guarantees
+    have hcount : Channel.CountUpTo muMax input_mu :=
+      Channel.countUpTo_of_val h0 (by simp only [muMax]; omega)
     have hsb : IsBool input_signed := mul_one_sub_eq_zero_iff.mp h_s
     have hib : IsBool input_invert := mul_one_sub_eq_zero_iff.mp h_i
     have hs_2 := IsBool.val_lt_two hsb
     have hi_2 := IsBool.val_lt_two hib
     -- the pulled guarantees are now unconditional
-    have hl1 := h_l1 rfl
-    have hr1 := h_r1 rfl
-    obtain ⟨hl2, hlm⟩ := h_lm rfl
-    obtain ⟨hr2, hrm⟩ := h_rm rfl
-    have hs0 := h_s0 rfl
-    have hs1 := h_s1 rfl
-    have hs2 := h_s2 rfl
-    have hs3 := h_s3 rfl
+    have hl1 := h_l1 hcount
+    have hr1 := h_r1 hcount
+    obtain ⟨hl2, hlm⟩ := h_lm hcount
+    obtain ⟨hr2, hrm⟩ := h_rm hcount
+    have hs0 := h_s0 hcount
+    have hs1 := h_s1 hcount
+    have hs2 := h_s2 hcount
+    have hs3 := h_s3 hcount
     -- values of the composite limbs
     have hval_lhsHi : (input_lhs1 + 65536 * input_lhs2).val = input_lhs1.val + 65536 * input_lhs2.val :=
       val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega)
@@ -255,8 +263,8 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
       first
       | (exfalso; omega)
       | (subst hlt'; norm_num at hres'; simp [hAv, hBv, hC, hres'])
-    refine ⟨fun _ hl0 hr0 => key _ _ rfl rfl hl0 hr0, by simp, by simp, by simp, by simp, by simp,
-      by simp, by simp, by simp, ?_⟩
+    refine ⟨fun _ hl0 hr0 => key _ _ rfl rfl hl0 hr0, .inr hcount, .inr hcount, .inr hcount,
+      .inr hcount, .inr hcount, .inr hcount, .inr hcount, .inr hcount, ?_⟩
     intro _ hl0 hlhi hr0 hrhi
     -- the flag byte, read as a natural
     have hflagsV : (4 + 32 * input_signed + 64 * input_invert : F p).val
@@ -278,7 +286,7 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
 
   completeness := by
     circuit_proof_start [main, isBit, sub, add, Add.carry0, Add.carry1, Alu.channel, Alu.Guarantees,
-      Bitwise.isHalfTable, Bitwise.msb16Table, Honest, Row.lhsVal, Row.rhsVal]
+      Bitwise.isHalfTable, Bitwise.msb16Table, Bitwise.areBytesTable, Honest, Row.lhsVal, Row.rhsVal]
     obtain ⟨hmu, hsb, hib, hl0, hl1, hl2, hr0, hr1, hr2, hs0, hs1, hs2, hs3, hsum, hlm, hrm, hlt, hres⟩ :=
       h_assumptions
     set L := input_lhs0.val + 2^32 * (input_lhs1.val + 65536 * input_lhs2.val) with hL
@@ -314,7 +322,7 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
     have hres_cast : input_res = ((ltRaw input_signed.val L R + input_invert.val
         - 2 * ltRaw input_signed.val L R * input_invert.val : ℕ) : F p) := by
       rw [← ltBit_eq (IsBool.val_lt_two hib), ← hres, ZMod.natCast_zmod_val]
-    refine ⟨mul_one_sub_eq_zero_iff.mpr hmu, fun _ => by omega, fun _ => by omega,
+    refine ⟨⟨hmu, by simp⟩, fun _ => by omega, fun _ => by omega,
       mul_one_sub_eq_zero_iff.mpr hsb, mul_one_sub_eq_zero_iff.mpr hib,
       fun _ => ⟨by omega, hlm⟩, fun _ => ⟨by omega, hrm⟩, ?_, ?_, ?_, ?_,
       fun _ => by omega, fun _ => by omega, fun _ => by omega, fun _ => by omega⟩
@@ -326,5 +334,4 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
     · rw [hc0k]; rcases (by omega : k0 = 0 ∨ k0 = 1) with rfl | rfl <;> simp
     · rw [hc1k]; rcases (by omega : k1 = 0 ∨ k1 = 1) with rfl | rfl <;> simp
 
-
 end LambdaVM.LT
diff --git a/formal/export/lt.json b/formal/export/lt.json
index 800c9d42d..5caa8e178 100644
--- a/formal/export/lt.json
+++ b/formal/export/lt.json
@@ -1,14 +1,9 @@
 {"operations":
- [{"assert":
-   {"type": "mul",
-    "rhs":
-    {"type": "add",
-     "rhs":
-     {"type": "mul",
-      "rhs": {"type": "var", "index": 16},
-      "lhs": {"value": 18446744069414584320, "type": "const"}},
-     "lhs": {"value": 1, "type": "const"}},
-    "lhs": {"type": "var", "index": 16}}},
+ [{"interact":
+   {"multiplicity": {"value": 1, "type": "const"},
+    "message": [{"type": "var", "index": 16}, {"value": 0, "type": "const"}],
+    "direction": "pull",
+    "channel": "ARE_BYTES"}},
   {"interact":
    {"multiplicity": {"type": "var", "index": 16},
     "message": [{"type": "var", "index": 1}],
diff --git a/prover/src/tests/lean_diff.rs b/prover/src/tests/lean_diff.rs
index cdabf95e8..0f9521321 100644
--- a/prover/src/tests/lean_diff.rs
+++ b/prover/src/tests/lean_diff.rs
@@ -361,12 +361,11 @@ fn lean_diff_lt() {
         cols::NUM_COLUMNS,
         &rows_of(&trace, cols::NUM_COLUMNS),
     );
-    // Known deltas: the Lean model keeps `μ·(1 − μ) = 0` (assert 0), the Rust chip bounds
-    // `μ` with the `ARE_BYTES[μ, 0]` send instead.
-    assert_eq!(
-        report.lean_asserts_unmatched,
-        vec![0],
-        "[LT] only the μ bit constraint should be Lean-only"
+    // The Lean model bounds `μ` with the `ARE_BYTES[μ, 0]` pull, as the Rust chip does, so the
+    // two agree exactly.
+    assert!(
+        report.lean_asserts_unmatched.is_empty(),
+        "[LT] Lean-only constraints"
     );
     assert!(
         report.rust_constraints_unmatched.is_empty(),
@@ -376,10 +375,9 @@ fn lean_diff_lt() {
         report.lean_interacts_unmatched.is_empty(),
         "[LT] Lean-only interactions"
     );
-    assert_eq!(
-        report.rust_interacts_unmatched,
-        vec![0],
-        "[LT] only ARE_BYTES[μ, 0] should be Rust-only"
+    assert!(
+        report.rust_interacts_unmatched.is_empty(),
+        "[LT] Rust-only interactions"
     );
 }
 

From d836289b0c5481219d98aae2028bcf74421f65f3 Mon Sep 17 00:00:00 2001
From: jotabulacios <jbulacios@fi.uba.ar>
Date: Mon, 2 Nov 2026 14:57:09 -0300
Subject: [PATCH 3/6] Add MIN, a toy ALU operation with the shape of DIVREM, to
 test counted pulls on one bus.

MIN is not an RV64IM operation. Its chip pulls an LT result from the ALU bus and pushes its own
result on the same bus, as the division chip pulls LT and MUL results and pushes DIVREM. The ALU
guarantee gets a MIN clause (opsel 7), so EQ, LT and SHIFT also prove that their pushes are not MIN
results.
---
 formal/LambdaVM.lean               |  1 +
 formal/LambdaVM/Buses/Alu.lean     | 10 ++-
 formal/LambdaVM/Tables/Eq.lean     |  6 +-
 formal/LambdaVM/Tables/Lt.lean     |  5 +-
 formal/LambdaVM/Tables/MinToy.lean | 98 ++++++++++++++++++++++++++++++
 formal/LambdaVM/Tables/Shift.lean  |  6 +-
 6 files changed, 122 insertions(+), 4 deletions(-)
 create mode 100644 formal/LambdaVM/Tables/MinToy.lean

diff --git a/formal/LambdaVM.lean b/formal/LambdaVM.lean
index 298ab5036..fe0cf14f2 100644
--- a/formal/LambdaVM.lean
+++ b/formal/LambdaVM.lean
@@ -13,3 +13,4 @@ public import LambdaVM.Tables.Eq
 public import LambdaVM.Tables.Shift
 public import LambdaVM.Ensembles.EqLookup
 public import LambdaVM.Channels.Counted
+public import LambdaVM.Tables.MinToy
diff --git a/formal/LambdaVM/Buses/Alu.lean b/formal/LambdaVM/Buses/Alu.lean
index 9f06b1123..96f96bb33 100644
--- a/formal/LambdaVM/Buses/Alu.lean
+++ b/formal/LambdaVM/Buses/Alu.lean
@@ -65,6 +65,10 @@ def shiftResult (word signed direction x s : ℕ) : ℕ :=
   else if signed = 0 then x >>> k
   else sra64 x k
 
+/-- `opsel` of MIN: a toy operation for the counted-pulls PoC, not an RV64IM op. It has the shape of
+DIVREM: its chip pulls LT on this bus and pushes its own result on the same bus. -/
+def opselMIN : ℕ := 7
+
 /-- What a puller learns. The caller must have range-checked both words of both operands
 (the chips' `IS_WORD` assumptions). One clause per `opsel`, selected by the flag byte read
 as a natural. -/
@@ -83,7 +87,11 @@ def Guarantees (m : Msg (F p)) : Prop :=
     (∀ w s d : ℕ, w < 2 → s < 2 → d < 2 →
       m.flags.val = opselSHIFT + w + 32 * s + 64 * d →
       m.outLo.val < 2^32 ∧ m.outHi.val < 2^32 ∧
-      dword m.outLo m.outHi = shiftResult w s d (dword m.in1Lo m.in1Hi) (m.in2Lo.val % 256))
+      dword m.outLo m.outHi = shiftResult w s d (dword m.in1Lo m.in1Hi) (m.in2Lo.val % 256)) ∧
+    -- MIN (toy, see `opselMIN`): flags = opsel(MIN), out = the unsigned minimum
+    (m.flags.val = opselMIN →
+      m.outLo.val < 2^32 ∧ m.outHi.val < 2^32 ∧
+      dword m.outLo m.outHi = min (dword m.in1Lo m.in1Hi) (dword m.in2Lo m.in2Hi))
 
 def channel : Channel (F p) Msg where
   name := "ALU"
diff --git a/formal/LambdaVM/Tables/Eq.lean b/formal/LambdaVM/Tables/Eq.lean
index 3fcee4831..380b14e0f 100644
--- a/formal/LambdaVM/Tables/Eq.lean
+++ b/formal/LambdaVM/Tables/Eq.lean
@@ -165,7 +165,7 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
     -- the flag byte, read as a natural
     have hflagsV : (3 + 64 * input_invert : F p).val = 3 + 64 * input_invert.val :=
       val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega)
-    refine ⟨?_, ?_, ?_⟩
+    refine ⟨?_, ?_, ?_, ?_⟩
     · -- the LT clause does not apply: opsel(EQ) + 64·i ≠ opsel(LT) + 32·s + 64·i'
       intro s i hs hi hflags
       exfalso; rw [hflagsV] at hflags; simp only [opselLT] at hflags; omega
@@ -173,6 +173,10 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
     · -- nor the SHIFT clause
       intro w s d hw hs hd hflags
       exfalso; rw [hflagsV] at hflags; simp only [opselSHIFT] at hflags; omega
+    swap
+    · -- nor the MIN clause
+      intro hflags
+      exfalso; rw [hflagsV] at hflags; simp only [Alu.opselMIN] at hflags; omega
     intro i hi hflags
     rw [hflagsV] at hflags; simp only [opselEQ] at hflags
     rw [key ha0 ha1 hb0 hb1, show input_invert.val = i by omega]
diff --git a/formal/LambdaVM/Tables/Lt.lean b/formal/LambdaVM/Tables/Lt.lean
index 410a5a8e6..badb095b6 100644
--- a/formal/LambdaVM/Tables/Lt.lean
+++ b/formal/LambdaVM/Tables/Lt.lean
@@ -270,7 +270,7 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
     have hflagsV : (4 + 32 * input_signed + 64 * input_invert : F p).val
         = 4 + 32 * input_signed.val + 64 * input_invert.val :=
       val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega)
-    refine ⟨?_, ?_, ?_⟩
+    refine ⟨?_, ?_, ?_, ?_⟩
     · intro s i hs hi hflags
       rw [hflagsV] at hflags; simp only [opselLT] at hflags
       rw [key s i (by omega) (by omega) hl0 hr0, hval_lhsHi, hval_rhsHi]
@@ -280,6 +280,9 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
     · -- nor the SHIFT clause: opsel(SHIFT) + w + 32·s + 64·d ≡ 5 or 6 (mod 32)
       intro w s d hw hs hd hflags
       exfalso; rw [hflagsV] at hflags; simp only [opselSHIFT] at hflags; omega
+    · -- nor the MIN clause
+      intro hflags
+      exfalso; rw [hflagsV] at hflags; simp only [Alu.opselMIN] at hflags; omega
 
 
   ProverAssumptions r _ _ := Honest r
diff --git a/formal/LambdaVM/Tables/MinToy.lean b/formal/LambdaVM/Tables/MinToy.lean
new file mode 100644
index 000000000..b86dee773
--- /dev/null
+++ b/formal/LambdaVM/Tables/MinToy.lean
@@ -0,0 +1,98 @@
+module
+
+public import LambdaVM.Buses.Alu
+public import LambdaVM.Templates.IsBit
+
+@[expose] public section
+
+/-!
+# MIN (toy, for the counted-pulls PoC)
+
+A chip with the shape of DVRM: it pulls an LT result on the ALU bus and pushes its own result on
+the same bus. `out = lt ? a : b` limb by limb, where `lt = (a < b)` comes from the pulled LT
+message. One table, one bus, no cycle: it receives `flags = opsel(LT)` and owes
+`flags = opsel(MIN)`.
+-/
+
+namespace LambdaVM.MinToy
+
+structure Row (F : Type) where
+  a0 : F
+  a1 : F
+  b0 : F
+  b1 : F
+  lt : F
+  out0 : F
+  out1 : F
+  mu : F
+deriving ProvableStruct
+
+def main (r : Var Row (F p)) : Circuit (F p) Unit := do
+  isBit r.mu
+  -- ALU[a, b, opsel(LT)] -> [lt, 0]: unsigned, no invert. Pulled on every row, padding included.
+  Alu.channel.pull ⟨r.a0, r.a1, r.b0, r.b1, 4, r.lt, 0⟩
+  -- out = lt ? a : b
+  assertZero (r.out0 - (r.lt * r.a0 + (1 - r.lt) * r.b0))
+  assertZero (r.out1 - (r.lt * r.a1 + (1 - r.lt) * r.b1))
+  -- ALU[a, b, opsel(MIN)] -> out
+  Alu.channel.pushIf r.mu ⟨r.a0, r.a1, r.b0, r.b1, 7, r.out0, r.out1⟩
+
+lemma val_lit (n : ℕ) (h : n < 2^40) : ((n : F p)).val = n :=
+  ZMod.val_natCast_of_lt (lt_p_of_lt_two_pow_40 h)
+
+/-- The honest prover's row: `lt` is the comparison and `out` the selected operand. -/
+def Honest (r : Row (F p)) : Prop :=
+  IsBool r.mu ∧ r.lt = ((Alu.ltBit 0 0 (dword r.a0 r.a1) (dword r.b0 r.b1) : ℕ) : F p) ∧
+  r.out0 = r.lt * r.a0 + (1 - r.lt) * r.b0 ∧ r.out1 = r.lt * r.a1 + (1 - r.lt) * r.b1
+
+def circuit : GeneralFormalCircuit (F p) Row unit where
+  name := "MIN"
+  main
+  Spec _ _ _ := True
+  channelsWithRequirements := [Alu.channel.toRaw]
+  soundness := by
+    circuit_proof_start [main, isBit, Alu.channel, Alu.Guarantees]
+    obtain ⟨-, h_pull, h_o0, h_o1⟩ := h_holds
+    intro _ ha0 ha1 hb0 hb1
+    have h4 : (4 : F p).val = 4 := by simpa using val_lit 4 (by norm_num)
+    have h7 : (7 : F p).val = 7 := by simpa using val_lit 7 (by norm_num)
+    -- the pulled LT result, with μ = 1
+    obtain ⟨hLT, -⟩ := h_pull ha0 ha1 hb0 hb1
+    have hlt := hLT 0 0 (by norm_num) (by norm_num) (by rw [h4]; simp [opselLT])
+    have hL : dword input_a0 input_a1 < 2^64 := by unfold dword; omega
+    have hR : dword input_b0 input_b1 < 2^64 := by unfold dword; omega
+    rw [h7]
+    -- only the MIN clause applies to flags = 7
+    refine ⟨fun s i hs hi h => by simp only [opselLT] at h; omega,
+      fun i hi h => by simp only [opselEQ] at h; omega,
+      fun w s d hw hs hd h => by simp only [opselSHIFT] at h; omega, fun _ => ?_⟩
+    by_cases hLR : dword input_a0 input_a1 < dword input_b0 input_b1
+    · have h1 : input_lt = 1 := by
+        rw [hlt]; simp [Alu.ltBit, Alu.ltRaw, Alu.ult_ofNat_iff hL hR, hLR]
+      have e0 : input_out0 = input_a0 := by rw [h1] at h_o0; linear_combination h_o0
+      have e1 : input_out1 = input_a1 := by rw [h1] at h_o1; linear_combination h_o1
+      rw [e0, e1, min_eq_left hLR.le]
+      exact ⟨ha0, ha1, rfl⟩
+    · have h1 : input_lt = 0 := by
+        rw [hlt]; simp [Alu.ltBit, Alu.ltRaw, Alu.ult_ofNat_iff hL hR, hLR]
+      have e0 : input_out0 = input_b0 := by rw [h1] at h_o0; linear_combination h_o0
+      have e1 : input_out1 = input_b1 := by rw [h1] at h_o1; linear_combination h_o1
+      rw [e0, e1, min_eq_right (not_lt.mp hLR)]
+      exact ⟨hb0, hb1, rfl⟩
+
+  ProverAssumptions r _ _ := Honest r
+  completeness := by
+    circuit_proof_start [main, isBit, Alu.channel, Alu.Guarantees, Honest]
+    obtain ⟨hmu, hlt, ho0, ho1⟩ := h_assumptions
+    have h4 : (4 : F p).val = 4 := by simpa using val_lit 4 (by norm_num)
+    refine ⟨mul_one_sub_eq_zero_iff.mpr hmu, ?_, by rw [ho0]; ring, by rw [ho1]; ring⟩
+    intro _ _ _ _
+    rw [h4]
+    refine ⟨fun s i hs hi h => ?_, fun i hi h => by simp only [opselEQ] at h; omega,
+      fun w s d hw hs hd h => by simp only [opselSHIFT] at h; omega,
+      fun h => by simp only [Alu.opselMIN] at h; omega⟩
+    simp only [opselLT] at h
+    obtain ⟨rfl, rfl⟩ : s = 0 ∧ i = 0 := by omega
+    exact hlt
+
+end LambdaVM.MinToy
diff --git a/formal/LambdaVM/Tables/Shift.lean b/formal/LambdaVM/Tables/Shift.lean
index 3b9afedbf..9016373f6 100644
--- a/formal/LambdaVM/Tables/Shift.lean
+++ b/formal/LambdaVM/Tables/Shift.lean
@@ -508,13 +508,17 @@ theorem soundness :
     have hflagsV : (5 + input_wordInstr + 32 * input_signed + 64 * input_direction : F p).val
         = 5 + input_wordInstr.val + 32 * input_signed.val + 64 * input_direction.val :=
       val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega)
-    refine ⟨?_, ?_, ?_⟩
+    refine ⟨?_, ?_, ?_, ?_⟩
     · -- not LT: 5 + w + 32 s + 64 d ≠ 4 + 32 s' + 64 i (mod 32)
       intro s i hs hi hflags
       exfalso; rw [hflagsV] at hflags; simp only [opselLT] at hflags; omega
     · -- not EQ
       intro i hi hflags
       exfalso; rw [hflagsV] at hflags; simp only [opselEQ] at hflags; omega
+    swap
+    · -- not MIN
+      intro hflags
+      exfalso; rw [hflagsV] at hflags; simp only [Alu.opselMIN] at hflags; omega
     · intro w s d hw hs hd hflags
       rw [hflagsV] at hflags; simp only [opselSHIFT] at hflags
       obtain ⟨rfl, rfl, rfl⟩ : input_wordInstr.val = w ∧ input_signed.val = s ∧

From 19305add2df7180fae501f7b468575e4c886e0de Mon Sep 17 00:00:00 2001
From: jotabulacios <jbulacios@fi.uba.ar>
Date: Mon, 2 Nov 2026 14:57:10 -0300
Subject: [PATCH 4/6] Prove LT and MIN sound by finishing order, including a
 counted MIN on the ALU bus.

LtStaged builds the LT ensemble with counted IS_HALF and MSB16 and proves its table soundness with
tableSoundness_of_staged: ARE_BYTES is finished first, so LT's bound mu <= 255 on its counted pulls
follows from that guarantee. It then adds MIN, finishing the ALU bus in two stages, every message
that is not MIN before MIN. CountedSameBus does the same with CMIN, which pulls LT and pushes MIN
with a counted multiplicity on the ALU bus, the shape of a deduplicated division chip, and proves it
sound with tableSoundness_of_stagedOn.
---
 formal/LambdaVM.lean                          |   2 +
 formal/LambdaVM/Ensembles/CountedSameBus.lean | 280 +++++++++++++
 formal/LambdaVM/Ensembles/LtStaged.lean       | 395 ++++++++++++++++++
 3 files changed, 677 insertions(+)
 create mode 100644 formal/LambdaVM/Ensembles/CountedSameBus.lean
 create mode 100644 formal/LambdaVM/Ensembles/LtStaged.lean

diff --git a/formal/LambdaVM.lean b/formal/LambdaVM.lean
index fe0cf14f2..64923b6c8 100644
--- a/formal/LambdaVM.lean
+++ b/formal/LambdaVM.lean
@@ -14,3 +14,5 @@ public import LambdaVM.Tables.Shift
 public import LambdaVM.Ensembles.EqLookup
 public import LambdaVM.Channels.Counted
 public import LambdaVM.Tables.MinToy
+public import LambdaVM.Ensembles.LtStaged
+public import LambdaVM.Ensembles.CountedSameBus
diff --git a/formal/LambdaVM/Ensembles/CountedSameBus.lean b/formal/LambdaVM/Ensembles/CountedSameBus.lean
new file mode 100644
index 000000000..de7d05c51
--- /dev/null
+++ b/formal/LambdaVM/Ensembles/CountedSameBus.lean
@@ -0,0 +1,280 @@
+module
+
+public import LambdaVM.Ensembles.LtStaged
+
+@[expose] public section
+
+/-!
+# Counted pulls and a response on the same bus (PoC)
+
+The shape of DVRM with everything at once. The ALU bus is a counted channel. One table, CMIN,
+answers `μ ≤ 255` identical MIN requests per row: it pulls an LT result on the ALU bus with
+multiplicity `μ`, bounded by its own pull of `ARE_BYTES[μ, 0]`, and pushes the MIN result `μ`
+times on the same bus. The LT answers come from a provider that stands for the LT table.
+
+Stages, oldest first: `ARE_BYTES`, the ALU messages that are not MIN, the MIN messages. CMIN's
+requirement on its counted pull (`μ = 0 ∨ 1 ≤ μ ≤ 255`) uses its guarantee on `ARE_BYTES`; its
+requirement on the MIN push uses its guarantee on the LT pull, in the earlier ALU class.
+-/
+
+namespace LambdaVM.CountedMin
+open LambdaVM.LT (muMax)
+
+/-- The ALU bus with pulls of multiplicity up to `muMax`. -/
+abbrev AluC : RawChannel (F p) := Alu.channel.counted muMax
+
+def main (r : Var MinToy.Row (F p)) : Circuit (F p) Unit := do
+  -- μ : Byte: ARE_BYTES[μ, 0]
+  Bitwise.AreBytes.pull (r.mu, 0)
+  -- ALU[a, b, opsel(LT)] -> [lt, 0], μ times
+  Alu.channel.pullUpTo muMax r.mu ⟨r.a0, r.a1, r.b0, r.b1, 4, r.lt, 0⟩
+  -- out = lt ? a : b
+  assertZero (r.out0 - (r.lt * r.a0 + (1 - r.lt) * r.b0))
+  assertZero (r.out1 - (r.lt * r.a1 + (1 - r.lt) * r.b1))
+  -- ALU[a, b, opsel(MIN)] -> out, μ times
+  Alu.channel.emitUpTo muMax r.mu ⟨r.a0, r.a1, r.b0, r.b1, 7, r.out0, r.out1⟩
+
+/-- The honest prover's row: `μ` a byte, `lt` the comparison and `out` the selected operand. -/
+def Honest (r : MinToy.Row (F p)) : Prop :=
+  r.mu.val < 2^8 ∧ r.lt = ((Alu.ltBit 0 0 (dword r.a0 r.a1) (dword r.b0 r.b1) : ℕ) : F p) ∧
+  r.out0 = r.lt * r.a0 + (1 - r.lt) * r.b0 ∧ r.out1 = r.lt * r.a1 + (1 - r.lt) * r.b1
+
+def circuit : GeneralFormalCircuit (F p) MinToy.Row unit where
+  name := "CMIN"
+  main
+  Spec _ _ _ := True
+  channelsWithRequirements := [AluC]
+  requirementsChannelsLawful input_var i₀ := by
+    obtain ⟨a0, a1, b0, b1, lt, out0, out1, mu⟩ := input_var
+    simp only [circuit_norm, main, AluC, Bitwise.AreBytes]
+    intro channel h
+    tauto
+  soundness := by
+    circuit_proof_start [main, Alu.channel, Alu.Guarantees, Bitwise.areBytesTable]
+    obtain ⟨⟨h_mu, -⟩, h_pull, h_o0, h_o1⟩ := h_holds
+    -- with μ = 0 nothing is owed
+    by_cases h0 : input_mu = 0
+    · simp [h0]
+    -- otherwise ARE_BYTES[μ, 0] makes μ a count of at most 255
+    have hcount : Channel.CountUpTo muMax input_mu :=
+      Channel.countUpTo_of_val h0 (by simp only [muMax]; omega)
+    refine ⟨.inr hcount, fun _ ha0 ha1 hb0 hb1 => ?_⟩
+    have h4 : (4 : F p).val = 4 := by simpa using MinToy.val_lit 4 (by norm_num)
+    have h7 : (7 : F p).val = 7 := by simpa using MinToy.val_lit 7 (by norm_num)
+    -- the pulled LT result
+    obtain ⟨hLT, -⟩ := h_pull hcount ha0 ha1 hb0 hb1
+    have hlt := hLT 0 0 (by norm_num) (by norm_num) (by rw [h4]; simp [opselLT])
+    have hL : dword input_a0 input_a1 < 2^64 := by unfold dword; omega
+    have hR : dword input_b0 input_b1 < 2^64 := by unfold dword; omega
+    rw [h7]
+    refine ⟨fun s i hs hi h => by simp only [opselLT] at h; omega,
+      fun i hi h => by simp only [opselEQ] at h; omega,
+      fun w s d hw hs hd h => by simp only [opselSHIFT] at h; omega, fun _ => ?_⟩
+    by_cases hLR : dword input_a0 input_a1 < dword input_b0 input_b1
+    · have h1 : input_lt = 1 := by
+        rw [hlt]; simp [Alu.ltBit, Alu.ltRaw, Alu.ult_ofNat_iff hL hR, hLR]
+      have e0 : input_out0 = input_a0 := by rw [h1] at h_o0; linear_combination h_o0
+      have e1 : input_out1 = input_a1 := by rw [h1] at h_o1; linear_combination h_o1
+      rw [e0, e1, min_eq_left hLR.le]
+      exact ⟨ha0, ha1, rfl⟩
+    · have h1 : input_lt = 0 := by
+        rw [hlt]; simp [Alu.ltBit, Alu.ltRaw, Alu.ult_ofNat_iff hL hR, hLR]
+      have e0 : input_out0 = input_b0 := by rw [h1] at h_o0; linear_combination h_o0
+      have e1 : input_out1 = input_b1 := by rw [h1] at h_o1; linear_combination h_o1
+      rw [e0, e1, min_eq_right (not_lt.mp hLR)]
+      exact ⟨hb0, hb1, rfl⟩
+
+  ProverAssumptions r _ _ := Honest r
+  completeness := by
+    circuit_proof_start [main, Alu.channel, Alu.Guarantees, Bitwise.areBytesTable, Honest]
+    obtain ⟨hmu, hlt, ho0, ho1⟩ := h_assumptions
+    have h4 : (4 : F p).val = 4 := by simpa using MinToy.val_lit 4 (by norm_num)
+    refine ⟨⟨hmu, by simp⟩, ?_, by rw [ho0]; ring, by rw [ho1]; ring⟩
+    intro _ _ _ _ _
+    rw [h4]
+    refine ⟨fun s i hs hi h => ?_, fun i hi h => by simp only [opselEQ] at h; omega,
+      fun w s d hw hs hd h => by simp only [opselSHIFT] at h; omega,
+      fun h => by simp only [Alu.opselMIN] at h; omega⟩
+    simp only [opselLT] at h
+    obtain ⟨rfl, rfl⟩ : s = 0 ∧ i = 0 := by omega
+    exact hlt
+
+/-! ## The ensemble: ARE_BYTES, the LT answers, CMIN -/
+
+open Air.Flat
+open Ensembles.LtStaged (providerComponent countedProviderComponent demandOn isMinMsg
+  isMinMsg_toElements msg_eval mu_count providerComponent_guarantees
+  providerComponent_requirements countedProviderComponent_guarantees
+  countedProviderComponent_requirements)
+
+def cminComponent : Component (F p) where
+  circuit := circuit
+  generation := demandOn Alu.channel _
+
+@[circuit_norm] lemma cminComponent_guarantees :
+    cminComponent.circuit.channelsWithGuarantees = [Bitwise.AreBytes.toRaw, AluC] := rfl
+@[circuit_norm] lemma cminComponent_requirements :
+    cminComponent.circuit.channelsWithRequirements = [AluC] := rfl
+
+/-- Stages, newest first: the MIN messages, the other ALU messages, ARE_BYTES. -/
+def stages : List (Stage (F p)) :=
+  [{ channel := AluC, cls := isMinMsg }, { channel := AluC, cls := fun m => !isMinMsg m },
+   { channel := Bitwise.AreBytes.toRaw }]
+
+/-- The LT answers stand for the LT table: a provider of ALU messages on the counted bus. -/
+def ensemble : Ensemble (F p) unit where
+  tables := [providerComponent Bitwise.AreBytes, countedProviderComponent muMax Alu.channel,
+    cminComponent]
+  unique_names := by
+    simp [providerComponent, countedProviderComponent, cminComponent, Ensembles.LtStaged.provider,
+      Ensembles.LtStaged.countedProvider, circuit, Alu.channel, Bitwise.AreBytes,
+      Bitwise.areBytesTable, StaticLookupChannel.toChannel]
+  channels := [AluC, Bitwise.AreBytes.toRaw]
+  unique_channel_names := by
+    simp [AluC, circuit_norm, Alu.channel, Bitwise.AreBytes, Bitwise.areBytesTable]
+  tables_channels := by
+    intro table h
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl <;>
+      simp only [GeneralFormalCircuit.channels, providerComponent_guarantees,
+        providerComponent_requirements, countedProviderComponent_guarantees,
+        countedProviderComponent_requirements, cminComponent_guarantees,
+        cminComponent_requirements] <;>
+      simp [AluC]
+  verifier_channels := by simp [circuit_norm]
+
+/-- `msg_eval`, in the form `simp` leaves an evaluated message in. -/
+lemma msg_eval_array {M : TypeMap} [ProvableType M] (env : Environment (F p))
+    (x : M (Expression (F p))) :
+    Array.map (Expression.eval env) (toElements x).toArray = (toElements (eval env x)).toArray := by
+  rw [← Vector.toArray_map]
+  exact msg_eval env x
+
+lemma isMinMsg_eval (env : Environment (F p)) (m : Alu.Msg (Expression (F p))) :
+    isMinMsg (Array.map (fun x => Expression.eval env x) (toElements m).toArray) =
+      decide ((eval env m).flags = 7) := by
+  rw [show (fun x => Expression.eval env x) = Expression.eval env from rfl, msg_eval_array,
+    isMinMsg_toElements]
+
+lemma areBytesTable_guarantees (x y : F p) :
+    Bitwise.areBytesTable.Guarantees (x, y) ↔ x.val < 2^8 ∧ y.val < 2^8 := Iff.rfl
+
+lemma bytes_ne_alu : Bitwise.AreBytes.toRaw ≠ Channel.counted muMax Alu.channel := by
+  intro h
+  have := congrArg RawChannel.name h
+  simp [circuit_norm, Alu.channel, Bitwise.AreBytes, Bitwise.areBytesTable, StaticLookupChannel.toChannel,
+    Channel.counted, Channel.toRaw] at this
+
+/-- Each row of CMIN has two interactions on the ALU bus: the LT pull, which is not a MIN message,
+and the MIN push. -/
+lemma cmin_alu_shape {table : Table (F p)} (h_comp : table.component = cminComponent)
+    {i : Interaction (F p)} (h_i : i ∈ table.interactionsWith AluC) :
+    (i.direction = .pull ∧ isMinMsg i.msg = false) ∨
+      (i.direction = .push ∧ isMinMsg i.msg = true) := by
+  cases table
+  simp only at h_comp
+  subst h_comp
+  simp [Table.interactionsWith, List.mem_flatMap, Operations.interactionValuesWith_eq_map,
+    Component.interactionsWith_eq, Component.rowOperations, cminComponent, circuit, main, AluC,
+    circuit_norm] at h_i
+  obtain ⟨row, -, a, ha, rfl⟩ := h_i
+  split_ifs at ha with h_eq
+  · exfalso
+    have := congrArg RawChannel.name h_eq
+    simp [Bitwise.areBytesTable, Channel.counted, Alu.channel, circuit_norm] at this
+  simp only [List.mem_cons, List.not_mem_nil, or_false] at ha
+  rcases ha with rfl | rfl
+  · left
+    simp only [AbstractInteraction.eval, Channel.pulledUpTo]
+    erw [msg_eval, isMinMsg_toElements]
+    simp (config := { decide := true }) [circuit_norm]
+  · right
+    simp only [AbstractInteraction.eval, Channel.emittedUpTo]
+    erw [msg_eval, isMinMsg_toElements]
+    simp (config := { decide := true }) [circuit_norm]
+
+/-- CMIN's counted pull owes `μ = 0 ∨ 1 ≤ μ ≤ 255`, which its guarantee on ARE_BYTES gives. -/
+lemma cmin_pull_requirement {table : Table (F p)} (h_comp : table.component = cminComponent)
+    (g_bytes : ∀ i ∈ table.interactionsWith Bitwise.AreBytes.toRaw, i.Guarantees table.data)
+    {i : Interaction (F p)} (h_i : i ∈ table.interactionsWith AluC)
+    (h_pull : i.direction = .pull) : i.Requirements table.data := by
+  cases table
+  simp only at h_comp
+  subst h_comp
+  simp [Table.interactionsWith, List.mem_flatMap, Operations.interactionValuesWith_eq_map,
+    Component.interactionsWith_eq, Component.rowOperations, cminComponent, circuit, main, AluC,
+    circuit_norm, forall_exists_index, and_imp] at h_i g_bytes
+  obtain ⟨row, hrow, a, ha, rfl⟩ := h_i
+  split_ifs at ha with h_eq
+  · exfalso
+    have := congrArg RawChannel.name h_eq
+    simp [Bitwise.areBytesTable, Channel.counted, Alu.channel, circuit_norm] at this
+  simp only [List.mem_cons, List.not_mem_nil, or_false] at ha
+  rcases ha with rfl | rfl
+  · have g := g_bytes _ row hrow (Or.inl rfl)
+    simp only [AbstractInteraction.eval, ChannelInteraction.toRaw, pulled, Interaction.Guarantees,
+      Channel.toRaw, Interaction.msgVector] at g
+    have g1 := g trivial (by simp [circuit_norm])
+    simp only [Vector.mk_toArray, ProvableType.fromElements_eval_toElements] at g1
+    simp only [circuit_norm, explicit_provable_type, areBytesTable_guarantees] at g1
+    simp only [AbstractInteraction.eval, Channel.pulledUpTo, Interaction.Requirements,
+      Channel.counted]
+    exact mu_count g1.1
+  · simp [AbstractInteraction.eval, Channel.emittedUpTo] at h_pull
+
+theorem tableSoundness : ensemble.TableSoundness (Balance.logUpUpTo muMax) := by
+  apply Ensemble.tableSoundness_of_stagedOn stages rfl
+  · intro s hs
+    simp only [stages, List.mem_cons, List.not_mem_nil, or_false] at hs
+    rcases hs with rfl | rfl | rfl <;> simp [ensemble]
+  · intro component h c hc msg
+    simp only [ensemble, List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl
+    iterate 2 simp [providerComponent_guarantees, countedProviderComponent_guarantees] at hc
+    · rw [cminComponent_guarantees] at hc
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hc
+      rcases hc with rfl | rfl
+      · exact ⟨{ channel := Bitwise.AreBytes.toRaw }, by simp [stages], rfl, rfl⟩
+      · cases h : isMinMsg msg
+        · exact ⟨{ channel := AluC, cls := fun m => !isMinMsg m }, by simp [stages], rfl,
+            by simp [h]⟩
+        · exact ⟨{ channel := AluC, cls := isMinMsg }, by simp [stages], rfl, h⟩
+  · intro s hs
+    show s.channel.ConsistentUpTo muMax
+    simp only [stages, List.mem_cons, List.not_mem_nil, or_false] at hs
+    rcases hs with rfl | rfl | rfl <;> infer_instance
+  · intro component h
+    simp only [ensemble, List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl
+    -- the providers pull nothing
+    iterate 2
+      refine ⟨?_, ?_, ?_, trivial⟩ <;>
+        exact Component.requirementsAfterOn_of_guarantees_subset (by
+          simp [providerComponent_guarantees, countedProviderComponent_guarantees])
+    refine ⟨?_, ?_, ?_, trivial⟩
+    -- MIN messages: after the LT pull's class and ARE_BYTES
+    · apply Component.requirementsAfterOn_of_covered
+      intro table h_comp c hc i h_i h_pull
+      rw [cminComponent_guarantees] at hc
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hc
+      rcases hc with rfl | rfl
+      · exact ⟨{ channel := Bitwise.AreBytes.toRaw }, by simp, rfl, rfl⟩
+      · rcases cmin_alu_shape h_comp h_i with ⟨-, h_cls⟩ | ⟨h_push, -⟩
+        · exact ⟨{ channel := AluC, cls := fun m => !isMinMsg m }, by simp, rfl, by simp [h_cls]⟩
+        · simp [h_push] at h_pull
+    -- the other ALU messages: only the counted pull, bounded through ARE_BYTES
+    · rintro table h_comp - - guarantees i h_i h_cls
+      rcases cmin_alu_shape h_comp h_i with ⟨h_pull, -⟩ | ⟨-, h_min⟩
+      · exact cmin_pull_requirement h_comp
+          (fun j hj => guarantees { channel := Bitwise.AreBytes.toRaw } (by simp) j hj rfl)
+          h_i h_pull
+      · simp [h_min] at h_cls
+    -- nothing owed on ARE_BYTES
+    · apply Component.requirementsAfterOn_of_not_mem
+      rw [cminComponent_requirements, List.mem_singleton]
+      intro h
+      have := congrArg RawChannel.name h
+      simp [circuit_norm, AluC, Alu.channel, Bitwise.AreBytes, Bitwise.areBytesTable,
+        StaticLookupChannel.toChannel, Channel.counted, Channel.toRaw] at this
+
+end LambdaVM.CountedMin
diff --git a/formal/LambdaVM/Ensembles/LtStaged.lean b/formal/LambdaVM/Ensembles/LtStaged.lean
new file mode 100644
index 000000000..fb60cccb6
--- /dev/null
+++ b/formal/LambdaVM/Ensembles/LtStaged.lean
@@ -0,0 +1,395 @@
+module
+
+public import LambdaVM.Tables.Lt
+public import LambdaVM.Tables.MinToy
+public import Clean.Air.StagedChannels
+
+@[expose] public section
+
+/-!
+# LT with counted pulls (PoC)
+
+`ARE_BYTES`, `IS_HALF` and `MSB16` providers and the LT chip, with `μ` a byte as in `lt.rs`.
+LT pulls `IS_HALF` and `MSB16` with multiplicity `μ`, so they are counted channels, and the bound
+`μ ≤ 255` comes from LT's own pull of `ARE_BYTES[μ, 0]`. Clean's `OrderedChannel` cannot express
+that (LT pulls from and owes requirements on `IS_HALF`); soundness by channel finishing order can:
+
+  ARE_BYTES → IS_HALF (counted) → MSB16 (counted) → ALU
+
+LT's requirements on `IS_HALF` and `MSB16` (`μ = 0 ∨ 1 ≤ μ ≤ 255`) follow from its guarantee on
+`ARE_BYTES`, which is finished before them.
+-/
+
+namespace LambdaVM.Ensembles.LtStaged
+open Air.Flat LambdaVM.LT
+
+variable {Message : TypeMap} [ProvableType Message]
+
+/-- A provider row: pushes `value` `multiplicity` times, assuming `value` satisfies the channel's
+guarantee. Stands for the BITWISE table, whose rows are fixed. -/
+def provider (channel : Channel (F p) Message) :
+    GeneralFormalCircuit (F p) (ProvablePair Message field) unit where
+  name := channel.name
+  main | (value, multiplicity) => channel.emit multiplicity value
+  channelsWithRequirements := [channel.toRaw]
+  Assumptions input data := channel.Guarantees input.1 data
+  Spec _ _ _ := True
+  soundness := by
+    circuit_proof_start
+    rcases input with ⟨value, multiplicity⟩
+    simp_all
+  completeness := by circuit_proof_start
+
+/-- The same, on `channel.counted N`. -/
+def countedProvider (N : ℕ) (channel : Channel (F p) Message) :
+    GeneralFormalCircuit (F p) (ProvablePair Message field) unit where
+  name := channel.name
+  main | (value, multiplicity) => channel.emitUpTo N multiplicity value
+  channelsWithRequirements := [channel.counted N]
+  Assumptions input data := channel.Guarantees input.1 data
+  Spec _ _ _ := True
+  soundness := by
+    circuit_proof_start
+    rcases input with ⟨value, multiplicity⟩
+    simp_all
+  completeness := by circuit_proof_start
+
+@[circuit_norm] lemma provider_channelsWithGuarantees (channel : Channel (F p) Message) :
+    (provider channel).channelsWithGuarantees = [] := rfl
+@[circuit_norm] lemma countedProvider_channelsWithGuarantees (N : ℕ) (channel : Channel (F p) Message) :
+    (countedProvider N channel).channelsWithGuarantees = [] := rfl
+@[circuit_norm] lemma provider_channelsWithRequirements (channel : Channel (F p) Message) :
+    (provider channel).channelsWithRequirements = [channel.toRaw] := rfl
+@[circuit_norm] lemma countedProvider_channelsWithRequirements (N : ℕ)
+    (channel : Channel (F p) Message) :
+    (countedProvider N channel).channelsWithRequirements = [channel.counted N] := rfl
+@[circuit_norm] lemma lt_channelsWithRequirements :
+    LT.circuit.channelsWithRequirements = [Alu.channel.toRaw, IsHalfC, Msb16C] := rfl
+@[circuit_norm] lemma lt_channelsWithGuarantees :
+    LT.circuit.channelsWithGuarantees = [Bitwise.AreBytes.toRaw, IsHalfC, IsHalfC, Msb16C, Msb16C,
+      IsHalfC, IsHalfC, IsHalfC, IsHalfC] := rfl
+
+/-- Witness generation is not part of this PoC: every component answers demand on its channel. -/
+def demandOn (channel : Channel (F p) Message) (Input : TypeMap) [ProvableType Input] :
+    WitnessGeneration.Generation (F p) Input :=
+  .demand {
+    channel
+    trigger := .pull
+    input _ := pure (fromElements (Vector.replicate (size Input) .multiplicity)) }
+
+def providerComponent (channel : Channel (F p) Message) : Component (F p) where
+  circuit := provider channel
+  generation := demandOn channel _
+  Assumptions input data := channel.Guarantees input.1 data
+  circuit_assumptions_of_assumptions := by intro _ _ _ _ _ h; exact h
+
+def countedProviderComponent (N : ℕ) (channel : Channel (F p) Message) : Component (F p) where
+  circuit := countedProvider N channel
+  generation := demandOn channel _
+  Assumptions input data := channel.Guarantees input.1 data
+  circuit_assumptions_of_assumptions := by intro _ _ _ _ _ h; exact h
+
+def ltComponent : Component (F p) where
+  circuit := LT.circuit
+  generation := demandOn Alu.channel _
+
+@[circuit_norm] lemma providerComponent_guarantees (channel : Channel (F p) Message) :
+    (providerComponent channel).circuit.channelsWithGuarantees = [] := rfl
+@[circuit_norm] lemma providerComponent_requirements (channel : Channel (F p) Message) :
+    (providerComponent channel).circuit.channelsWithRequirements = [channel.toRaw] := rfl
+@[circuit_norm] lemma countedProviderComponent_guarantees (N : ℕ) (channel : Channel (F p) Message) :
+    (countedProviderComponent N channel).circuit.channelsWithGuarantees = [] := rfl
+@[circuit_norm] lemma countedProviderComponent_requirements (N : ℕ)
+    (channel : Channel (F p) Message) :
+    (countedProviderComponent N channel).circuit.channelsWithRequirements =
+      [channel.counted N] := rfl
+@[circuit_norm] lemma ltComponent_guarantees :
+    ltComponent.circuit.channelsWithGuarantees = [Bitwise.AreBytes.toRaw, IsHalfC, IsHalfC, Msb16C,
+      Msb16C, IsHalfC, IsHalfC, IsHalfC, IsHalfC] := rfl
+@[circuit_norm] lemma ltComponent_requirements :
+    ltComponent.circuit.channelsWithRequirements = [Alu.channel.toRaw, IsHalfC, Msb16C] := rfl
+
+/-- Finishing order, newest first. -/
+def finished : List (RawChannel (F p)) :=
+  [Alu.channel.toRaw, Msb16C, IsHalfC, Bitwise.AreBytes.toRaw]
+
+def ensemble : Ensemble (F p) unit where
+  tables := [providerComponent Bitwise.AreBytes, countedProviderComponent muMax Bitwise.IsHalf,
+    countedProviderComponent muMax Bitwise.Msb16, ltComponent]
+  unique_names := by
+    simp [providerComponent, countedProviderComponent, ltComponent, provider, countedProvider,
+      LT.circuit, Bitwise.AreBytes, Bitwise.IsHalf, Bitwise.Msb16, Bitwise.areBytesTable,
+      Bitwise.isHalfTable, Bitwise.msb16Table, StaticLookupChannel.toChannel]
+  channels := finished
+  unique_channel_names := by
+    simp [finished, circuit_norm, Alu.channel, Bitwise.AreBytes, Bitwise.IsHalf, Bitwise.Msb16,
+      Bitwise.areBytesTable, Bitwise.isHalfTable, Bitwise.msb16Table]
+  tables_channels := by
+    intro table h
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl | rfl <;>
+      simp only [GeneralFormalCircuit.channels, providerComponent_guarantees, providerComponent_requirements, countedProviderComponent_guarantees, countedProviderComponent_requirements, ltComponent_guarantees, ltComponent_requirements] <;>
+      simp [finished, IsHalfC, Msb16C]
+  verifier_channels := by simp [circuit_norm]
+
+/-- `μ` from `ARE_BYTES[μ, 0]` is an inactive or counted pull. -/
+lemma mu_count {x : F p} (h : x.val < 256) : x = 0 ∨ Channel.CountUpTo muMax x := by
+  by_cases h0 : x = 0
+  · exact .inl h0
+  · exact .inr (Channel.countUpTo_of_val h0 (by simp only [muMax]; omega))
+
+/-- LT's requirements on its counted pulls follow from its guarantee on `ARE_BYTES`. -/
+theorem lt_requirementsAfter_counted {c : RawChannel (F p)} (hc : c = IsHalfC ∨ c = Msb16C)
+    {earlier : List (RawChannel (F p))} (h_earlier : Bitwise.AreBytes.toRaw ∈ earlier) :
+    ltComponent.RequirementsAfter c earlier := by
+  rintro table h_comp - constraints guarantees row hrow
+  have g := guarantees _ h_earlier row hrow
+  cases table
+  simp only at h_comp
+  subst h_comp
+  simp only [Component.channelGuarantees_iff, Component.channelRequirements_iff] at g ⊢
+  simp (config := { decide := true }) [circuit_norm, Component.rowOperations, ltComponent,
+    LT.circuit, LT.main, isBit, sub, add, Add.carry0, Add.carry1, IsHalfC, Msb16C, Alu.channel,
+    Bitwise.AreBytes, Bitwise.IsHalf, Bitwise.Msb16, Bitwise.areBytesTable, Bitwise.isHalfTable,
+    Bitwise.msb16Table, StaticLookupChannel.toChannel] at g ⊢
+  have hm := mu_count g.1
+  rcases hc with rfl | rfl <;>
+    simp (config := { decide := true }) [hm, IsHalfC, Msb16C, Bitwise.IsHalf, Bitwise.Msb16,
+      Bitwise.isHalfTable, Bitwise.msb16Table, StaticLookupChannel.toChannel]
+  -- the ALU push is on another channel
+  all_goals
+    intro h
+    have := congrArg RawChannel.name h
+    simp [Channel.counted, Channel.toRaw] at this
+
+theorem tableSoundness : ensemble.TableSoundness (Balance.logUpUpTo muMax) := by
+  apply Ensemble.tableSoundness_of_staged finished rfl (List.Subset.refl _)
+  · intro component h
+    simp only [ensemble, List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl | rfl <;>
+      simp only [providerComponent_guarantees, countedProviderComponent_guarantees,
+        ltComponent_guarantees] <;>
+      simp [finished, IsHalfC, Msb16C]
+  · intro c hc
+    show c.ConsistentUpTo muMax
+    simp only [finished, List.mem_cons, List.not_mem_nil, or_false] at hc
+    rcases hc with rfl | rfl | rfl | rfl <;> infer_instance
+  · intro component h
+    simp only [ensemble, List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl | rfl
+    -- the providers pull nothing
+    iterate 3
+      exact Component.stagedRequirements_of_forall fun _ _ _ =>
+        Component.requirementsAfter_of_guarantees_subset (by
+          simp only [providerComponent_guarantees, countedProviderComponent_guarantees,
+            List.nil_subset])
+    -- LT: ALU after its pulls, the counted pulls after ARE_BYTES, nothing owed on ARE_BYTES
+    refine ⟨?_, lt_requirementsAfter_counted (.inr rfl) (by simp),
+      lt_requirementsAfter_counted (.inl rfl) (by simp), ?_, trivial⟩
+    · apply Component.requirementsAfter_of_guarantees_subset
+      simp only [ltComponent_guarantees]
+      simp [IsHalfC, Msb16C]
+    · apply Component.requirementsAfter_of_not_mem
+      simp only [ltComponent_requirements, List.mem_cons, List.not_mem_nil, or_false, not_or]
+      refine ⟨fun h => ?_, fun h => ?_, fun h => ?_⟩ <;> have := congrArg RawChannel.name h <;>
+        simp [circuit_norm, IsHalfC, Msb16C, Alu.channel, Bitwise.AreBytes, Bitwise.IsHalf,
+          Bitwise.Msb16, Bitwise.areBytesTable, Bitwise.isHalfTable, Bitwise.msb16Table,
+          StaticLookupChannel.toChannel] at this
+
+end LambdaVM.Ensembles.LtStaged
+
+/-!
+## Adding MIN: one table pulls and pushes on the same bus
+
+MIN pulls an LT result from the ALU bus and pushes its own result on the same bus. Ordering by
+whole channels can't place it: ALU would have to be finished before MIN (for its pull) and after
+it (for its push). Ordering by stages can: the ALU messages that are not MIN are finished first,
+then the MIN messages. MIN is one table; only the bus is read in two classes.
+-/
+
+namespace LambdaVM.Ensembles.LtStaged
+open Air.Flat LambdaVM.LT
+
+def minComponent : Component (F p) where
+  circuit := MinToy.circuit
+  generation := demandOn Alu.channel _
+
+@[circuit_norm] lemma minComponent_guarantees :
+    minComponent.circuit.channelsWithGuarantees = [Alu.channel.toRaw] := rfl
+@[circuit_norm] lemma minComponent_requirements :
+    minComponent.circuit.channelsWithRequirements = [Alu.channel.toRaw] := rfl
+
+/-- The ALU messages of MIN: read as an ALU message, the flag field is `opsel(MIN)`. -/
+def isMinMsg (msg : Array (F p)) : Bool :=
+  if h : msg.size = size Alu.Msg then
+    decide ((fromElements (⟨msg, h⟩ : Vector (F p) (size Alu.Msg)) : Alu.Msg (F p)).flags = 7)
+  else false
+
+lemma isMinMsg_toElements (m : Alu.Msg (F p)) :
+    isMinMsg (toElements m).toArray = decide (m.flags = 7) := by
+  simp [isMinMsg, ProvableType.fromElements_toElements]
+
+/-- The message of an evaluated interaction, as the evaluated typed message. -/
+lemma msg_eval {M : TypeMap} [ProvableType M] (env : Environment (F p)) (x : M (Expression (F p))) :
+    ((toElements x).map (Expression.eval env)).toArray = (toElements (eval env x)).toArray := by
+  rw [← ProvableType.fromElements_eval_toElements (env := env) x,
+    ProvableType.toElements_fromElements, Vector.toArray_map]
+
+/-- Each row of MIN has two interactions on ALU: the LT pull, which is not a MIN message, and
+the MIN push. -/
+lemma min_alu_shape {table : Table (F p)} (h_comp : table.component = minComponent)
+    {i : Interaction (F p)} (h_i : i ∈ table.interactionsWith Alu.channel.toRaw) :
+    (i.direction = .pull ∧ isMinMsg i.msg = false) ∨
+      (i.direction = .push ∧ isMinMsg i.msg = true) := by
+  cases table
+  simp only at h_comp
+  subst h_comp
+  simp [Table.interactionsWith, List.mem_flatMap, Operations.interactionValuesWith_eq_map,
+    Component.interactionsWith_eq, Component.rowOperations, minComponent, MinToy.circuit,
+    MinToy.main, isBit, circuit_norm] at h_i
+  obtain ⟨row, -, rfl | rfl⟩ := h_i
+  · left
+    simp only [AbstractInteraction.eval, ChannelInteraction.toRaw, pulled, msg_eval,
+      isMinMsg_toElements]
+    simp (config := { decide := true }) [circuit_norm]
+  · right
+    simp only [AbstractInteraction.eval, ChannelInteraction.toRaw, pushedIf, msg_eval,
+      isMinMsg_toElements]
+    simp (config := { decide := true }) [circuit_norm]
+
+/-- MIN's pull, of multiplicity `1`, owes nothing beyond its multiplicity. -/
+lemma min_pull_requirements {table : Table (F p)} (h_comp : table.component = minComponent)
+    (constraints : table.Constraints) {i : Interaction (F p)}
+    (h_i : i ∈ table.interactionsWith Alu.channel.toRaw) (h_pull : i.direction = .pull) :
+    i.Requirements table.data := by
+  cases table
+  simp only at h_comp
+  subst h_comp
+  simp [Table.interactionsWith, List.mem_flatMap, Operations.interactionValuesWith_eq_map,
+    Component.interactionsWith_eq, Component.rowOperations, minComponent, MinToy.circuit,
+    MinToy.main, isBit, circuit_norm] at h_i
+  obtain ⟨row, -, rfl | rfl⟩ := h_i
+  · simp [AbstractInteraction.eval, ChannelInteraction.toRaw, pulled, Interaction.Requirements,
+      Channel.toRaw]
+    exact .inr (by simp [circuit_norm])
+  · simp [AbstractInteraction.eval, ChannelInteraction.toRaw, pushedIf] at h_pull
+
+/-- Stages, newest first. The ALU bus is finished in two classes: first every message that is
+not MIN, then the MIN messages. -/
+def stages : List (Stage (F p)) :=
+  [{ channel := Alu.channel.toRaw, cls := isMinMsg },
+   { channel := Alu.channel.toRaw, cls := fun m => !isMinMsg m },
+   { channel := Msb16C }, { channel := IsHalfC }, { channel := Bitwise.AreBytes.toRaw }]
+
+def ensembleMin : Ensemble (F p) unit where
+  tables := [providerComponent Bitwise.AreBytes, countedProviderComponent muMax Bitwise.IsHalf,
+    countedProviderComponent muMax Bitwise.Msb16, ltComponent, minComponent]
+  unique_names := by
+    simp [providerComponent, countedProviderComponent, ltComponent, minComponent, provider,
+      countedProvider, LT.circuit, MinToy.circuit, Bitwise.AreBytes, Bitwise.IsHalf, Bitwise.Msb16,
+      Bitwise.areBytesTable, Bitwise.isHalfTable, Bitwise.msb16Table, StaticLookupChannel.toChannel]
+  channels := finished
+  unique_channel_names := ensemble.unique_channel_names
+  tables_channels := by
+    intro table h
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl | rfl | rfl <;>
+      simp only [GeneralFormalCircuit.channels, providerComponent_guarantees,
+        providerComponent_requirements, countedProviderComponent_guarantees,
+        countedProviderComponent_requirements, ltComponent_guarantees, ltComponent_requirements,
+        minComponent_guarantees, minComponent_requirements] <;>
+      simp [finished, IsHalfC, Msb16C]
+  verifier_channels := by simp [circuit_norm]
+
+/-- A channel other than ALU, by name. -/
+lemma ne_alu {c : RawChannel (F p)}
+    (hc : c = IsHalfC ∨ c = Msb16C ∨ c = Bitwise.AreBytes.toRaw) : c ∉ [Alu.channel.toRaw] := by
+  rw [List.mem_singleton]
+  intro h
+  have := congrArg RawChannel.name h
+  rcases hc with rfl | rfl | rfl <;>
+    simp [circuit_norm, IsHalfC, Msb16C, Alu.channel, Bitwise.AreBytes, Bitwise.IsHalf,
+      Bitwise.Msb16, Bitwise.areBytesTable, Bitwise.isHalfTable, Bitwise.msb16Table,
+      StaticLookupChannel.toChannel, Channel.counted, Channel.toRaw] at this
+
+theorem tableSoundness_withMin : ensembleMin.TableSoundness (Balance.logUpUpTo muMax) := by
+  apply Ensemble.tableSoundness_of_stagedOn stages rfl
+  · intro s hs
+    simp only [stages, List.mem_cons, List.not_mem_nil, or_false] at hs
+    rcases hs with rfl | rfl | rfl | rfl | rfl <;> simp [ensembleMin, finished]
+  · intro component h c hc msg
+    simp only [ensembleMin, List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl | rfl | rfl
+    iterate 3 simp [providerComponent_guarantees, countedProviderComponent_guarantees] at hc
+    · rw [ltComponent_guarantees] at hc
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hc
+      rcases hc with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> simp [stages]
+    · rw [minComponent_guarantees, List.mem_singleton] at hc
+      subst hc
+      cases h : isMinMsg msg
+      · exact ⟨{ channel := Alu.channel.toRaw, cls := fun m => !isMinMsg m }, by simp [stages],
+          rfl, by simp [h]⟩
+      · exact ⟨{ channel := Alu.channel.toRaw, cls := isMinMsg }, by simp [stages], rfl, h⟩
+  · intro s hs
+    show s.channel.ConsistentUpTo muMax
+    simp only [stages, List.mem_cons, List.not_mem_nil, or_false] at hs
+    rcases hs with rfl | rfl | rfl | rfl | rfl <;> infer_instance
+  · intro component h
+    simp only [ensembleMin, List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl | rfl | rfl
+    -- the providers pull nothing
+    iterate 3
+      refine ⟨?_, ?_, ?_, ?_, ?_, trivial⟩ <;>
+        exact Component.requirementsAfterOn_of_guarantees_subset (by
+          simp [providerComponent_guarantees, countedProviderComponent_guarantees])
+    -- LT: both ALU classes after its pulls, the counted pulls after ARE_BYTES
+    · refine ⟨?_, ?_, ?_, ?_, ?_, trivial⟩
+      iterate 2
+        apply Component.requirementsAfterOn_of_guarantees_subset
+        rw [ltComponent_guarantees]
+        intro c hc msg
+        simp only [List.mem_cons, List.not_mem_nil, or_false] at hc
+        rcases hc with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> simp
+      · exact Component.requirementsAfterOn_of_requirementsAfter
+          (lt_requirementsAfter_counted (earlier := [IsHalfC, Bitwise.AreBytes.toRaw]) (.inr rfl)
+            (by simp))
+          (by
+            intro c hc
+            simp only [List.mem_cons, List.not_mem_nil, or_false] at hc
+            rcases hc with rfl | rfl
+            · exact ⟨{ channel := IsHalfC }, by simp, rfl, fun _ => rfl⟩
+            · exact ⟨{ channel := Bitwise.AreBytes.toRaw }, by simp, rfl, fun _ => rfl⟩)
+      · exact Component.requirementsAfterOn_of_requirementsAfter
+          (lt_requirementsAfter_counted (earlier := [Bitwise.AreBytes.toRaw]) (.inl rfl) (by simp))
+          (by
+            intro c hc
+            rw [List.mem_singleton] at hc
+            subst hc
+            exact ⟨{ channel := Bitwise.AreBytes.toRaw }, by simp, rfl, fun _ => rfl⟩)
+      · apply Component.requirementsAfterOn_of_not_mem
+        simp only [ltComponent_requirements, List.mem_cons, List.not_mem_nil, or_false, not_or]
+        refine ⟨fun h => ?_, fun h => ?_, fun h => ?_⟩ <;> have := congrArg RawChannel.name h <;>
+          simp [circuit_norm, IsHalfC, Msb16C, Alu.channel, Bitwise.AreBytes, Bitwise.IsHalf,
+            Bitwise.Msb16, Bitwise.areBytesTable, Bitwise.isHalfTable, Bitwise.msb16Table,
+            StaticLookupChannel.toChannel] at this
+    -- MIN: the MIN class after the other ALU class, which holds its LT pull
+    · refine ⟨?_, ?_, ?_, ?_, ?_, trivial⟩
+      · apply Component.requirementsAfterOn_of_covered
+        intro table h_comp c hc i h_i h_pull
+        rw [minComponent_guarantees, List.mem_singleton] at hc
+        subst hc
+        rcases min_alu_shape h_comp h_i with ⟨-, h_cls⟩ | ⟨h_push, -⟩
+        · exact ⟨{ channel := Alu.channel.toRaw, cls := fun m => !isMinMsg m }, by simp,
+            rfl, by simp [h_cls]⟩
+        · simp [h_push] at h_pull
+      · -- on the other class MIN owes only its pull's multiplicity, from its constraints
+        rintro table h_comp - constraints - i h_i h_cls
+        rcases min_alu_shape h_comp h_i with ⟨h_pull, -⟩ | ⟨-, h_min⟩
+        · exact min_pull_requirements h_comp constraints h_i h_pull
+        · simp [h_min] at h_cls
+      all_goals
+        apply Component.requirementsAfterOn_of_not_mem
+        rw [minComponent_requirements]
+        exact ne_alu (by simp)
+
+end LambdaVM.Ensembles.LtStaged

From 3cd8087a840aaae4d38a1fcb2095593ab5a5b677 Mon Sep 17 00:00:00 2001
From: jotabulacios <jbulacios@fi.uba.ar>
Date: Tue, 3 Nov 2026 10:16:57 -0300
Subject: [PATCH 5/6] Take Clean from the counted-pulls branch of the
 yetanotherco/clean fork on GitHub instead of a local path, so the branch
 builds anywhere and not only on the build server. The pinned revision,
 1cf67e24, is the same Clean the model was built against (counted pulls and
 soundness by finishing order on top of Clean main f3abad7c); Mathlib and
 CompPoly are unchanged.

---
 formal/lake-manifest.json | 8 +++++---
 formal/lakefile.toml      | 9 +++++----
 2 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/formal/lake-manifest.json b/formal/lake-manifest.json
index 288e99646..0fd1d9f57 100644
--- a/formal/lake-manifest.json
+++ b/formal/lake-manifest.json
@@ -1,13 +1,15 @@
 {"version": "1.3.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"type": "path",
+ [{"url": "https://github.com/yetanotherco/clean",
+   "type": "git",
+   "subDir": null,
    "scope": "",
+   "rev": "1cf67e24816808b880aa6af8592047cf42546efc",
    "name": "Clean",
    "manifestFile": "lake-manifest.json",
+   "inputRev": "1cf67e24816808b880aa6af8592047cf42546efc",
    "inherited": false,
-   "dir": "../../clean-fork-main",
-   "copy": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/Verified-zkEVM/CompPoly.git",
    "type": "git",
diff --git a/formal/lakefile.toml b/formal/lakefile.toml
index f2deaa523..0f85231ad 100644
--- a/formal/lakefile.toml
+++ b/formal/lakefile.toml
@@ -5,12 +5,13 @@ defaultTargets = ["LambdaVM", "LambdaVMExport"]
 autoImplicit = false
 relaxedAutoImplicit = false
 
-# Clean pinned to a revision; Mathlib and CompPoly come in through Clean's manifest.
-# PoC: Clean local con pulls contados y orden por cierre de canales (rama counted-pulls).
-# La ruta es la del servidor de builds (~/lvc/formal-bump435/formal -> ~/lvc/clean-fork-main).
+# Clean from the counted-pulls branch of the yetanotherco fork (on Clean main f3abad7c): pulls of
+# multiplicity up to N and soundness by finishing order. Mathlib and CompPoly come in through
+# Clean's manifest.
 [[require]]
 name = "Clean"
-path = "../../clean-fork-main"
+git = "https://github.com/yetanotherco/clean"
+rev = "1cf67e24816808b880aa6af8592047cf42546efc"
 
 [[lean_lib]]
 name = "LambdaVM"

From c146bd2a259b60d37197b6cde2e69b2cfd42b0b7 Mon Sep 17 00:00:00 2001
From: jotabulacios <jbulacios@fi.uba.ar>
Date: Wed, 4 Nov 2026 11:00:51 -0300
Subject: [PATCH 6/6] =?UTF-8?q?Update=20formal/README=20for=20counted=20pu?=
 =?UTF-8?q?lls:=20LT=20now=20pulls=20IS=5FHALF=20and=20MSB16=20with=20mult?=
 =?UTF-8?q?iplicity=20=CE=BC=20through=20Channel.counted=20255=20and=20mat?=
 =?UTF-8?q?ches=20lt.rs=20exactly,=20so=20the=20LT=20deltas=20and=20the=20?=
 =?UTF-8?q?"LT=20keeps=20=CE=BC=20a=20bit"=20notes=20are=20gone.=20The=20c?=
 =?UTF-8?q?ounted-pulls=20section=20says=20what=20the=20model=20takes=20fr?=
 =?UTF-8?q?om=20the=20yetanotherco/clean=20fork=20(Balance.logUpUpTo,=20Ch?=
 =?UTF-8?q?annel.counted,=20soundness=20by=20finishing=20order)=20and=20de?=
 =?UTF-8?q?scribes=20the=20LtStaged=20and=20CountedSameBus=20ensembles;=20?=
 =?UTF-8?q?the=20layout=20lists=20MinToy=20and=20flags=20MIN=20as=20a=20to?=
 =?UTF-8?q?y=20stand-in=20for=20DVRM=20on=20the=20ALU=20bus.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 formal/README.md | 56 +++++++++++++++++++++++++++++++++---------------
 1 file changed, 39 insertions(+), 17 deletions(-)

diff --git a/formal/README.md b/formal/README.md
index b7f834d01..f9ca91344 100644
--- a/formal/README.md
+++ b/formal/README.md
@@ -25,8 +25,9 @@ FRI / WHIR prover, the LogUp argument itself, the executor, GPU code.
 - `LambdaVM/Buses/` — the buses that are not static tables. `Alu.lean` is the
   unified ALU bus: message layout as in `BusId::Alu`, the caller's `IS_WORD`
   assumptions on both operands as hypotheses, and one `Guarantees` clause per
-  `opsel` (LT, EQ and SHIFT). The flag byte is read as a natural, so a chip
-  pushing with one `opsel` discharges the other clauses by `omega`.
+  `opsel` (LT, EQ, SHIFT and the toy MIN of the counted-pulls PoC). The flag
+  byte is read as a natural, so a chip pushing with one `opsel` discharges the
+  other clauses by `omega`.
 - `LambdaVM/Tables/` — one file per chip. `Bitwise.lean` transcribes the
   precomputed row function of `prover/src/tables/bitwise.rs` and defines each bus
   the table serves as a `StaticLookupChannel` (read through `toChannel`), with
@@ -49,7 +50,8 @@ FRI / WHIR prover, the LogUp argument itself, the executor, GPU code.
   first global theorem: for any witness whose constraints hold and whose
   channels balance, every EQ row with `μ = 1` and range-checked operands
   carries the equality bit. The lookup argument is what turns the pulled range
-  checks into facts.
+  checks into facts. `LtStaged.lean` and `CountedSameBus.lean` are the
+  counted-pulls ensembles (see below).
 - `LambdaVM/Tables/ShiftCore.lean` and `Shift.lean` — the SHIFT chip. `ShiftCore`
   is the two-phase shift argument of `spec/shift.typ` on naturals (HWSL
   per limb, then whole limbs, left and right, logical and arithmetic), ending in
@@ -58,6 +60,10 @@ FRI / WHIR prover, the LogUp argument itself, the executor, GPU code.
   overrides) and concludes `shiftResult`. `Shift.lean` mirrors the 22 constraints
   and 17 interactions of `shift.rs` and proves soundness and completeness, the
   latter for both the honest active row and the padding row.
+- `LambdaVM/Tables/MinToy.lean` — MIN, a toy ALU operation with the shape of
+  DVRM: it pulls an LT result on the ALU bus and pushes its own result on the
+  same bus. Not an RV64IM operation; it stands in for DVRM until DVRM is
+  modelled.
 
 ## Lessons for big chips (from SHIFT)
 
@@ -99,8 +105,8 @@ Result on `main` after that merge, 2026-10-28:
 
 - EQ: 5 constraints and 6 interactions, exact match.
 - SHIFT: 22 constraints and 17 interactions, exact match.
-- LT: exact match except the two documented deltas: `μ·(1 − μ) = 0` exists
-  only in Lean, `ARE_BYTES[μ, 0]` exists only in Rust.
+- LT: 6 constraints and 10 interactions, exact match, with `μ` a byte as in
+  `lt.rs`.
 
 The check compares polynomials, not zero sets: it caught `μ·(μ − 1)` versus
 `μ·(1 − μ)` in EQ, which is why the Lean bit constraints use the spec's form.
@@ -139,26 +145,42 @@ multiplicity is a requirement the row cannot meet.
   `channelsWithRequirements`: an out-of-range `μ` is only ruled out by the byte
   guarantee, which lawfulness does not see but soundness does.
 
-What upstream Clean needs for an end-to-end LT theorem with byte `μ`:
+An end-to-end LT theorem with byte `μ` needs two things Clean main lacks:
 
 1. A `Balance` for counted pulls: `BalancedInteractions` matching a pull of
    `1, …, N`, and a `fits` that bounds `N * count` rather than `count` by the
    characteristic.
-2. Either a dependency-aware `OrderedChannel` (a table may hold guarantees and
+2. A dependency-aware finishing order: a table may hold guarantees and
    requirements on the same channel when the requirements depend only on
-   channels finished earlier), or the range check of `μ` as a static `lookup`,
-   which is a local constraint and makes the requirement vacuous at lawfulness.
-
-Until then LT keeps `μ ∈ {0, 1}` (see below).
+   channels finished earlier.
+
+The model takes both from the `counted-pulls` branch of
+[yetanotherco/clean](https://github.com/yetanotherco/clean/tree/counted-pulls),
+Clean main `f3abad7c` plus three commits: `Balance.logUpUpTo N` with
+`RawChannel.ConsistentUpTo N`, the typed `Channel.counted N`, and
+`Ensemble.tableSoundness_of_staged` / `_stagedOn` (soundness by finishing
+order of channels, and of message classes within a channel). On top of it:
+
+- `Tables/Lt.lean` pulls `IS_HALF` and `MSB16` with multiplicity `μ` through
+  `Channel.counted 255`, bounded by its own pull of `ARE_BYTES[μ, 0]`, exactly
+  as `lt.rs`.
+- `Ensembles/LtStaged.lean` proves the LT ensemble sound under
+  `Balance.logUpUpTo 255`, finishing `ARE_BYTES` before the counted `IS_HALF`
+  and `MSB16` and those before ALU. Its second half adds MIN, which pulls LT
+  and pushes MIN on the ALU bus: ALU is finished in two stages, the non-MIN
+  messages first and the MIN messages after.
+- `Ensembles/CountedSameBus.lean` (CMIN) does the same with the ALU bus itself
+  counted: a row answers `μ` identical MIN requests, the full shape of DVRM.
+
+`Channels/Counted.lean` above predates the fork. Its `not_consistent` is the
+reason the fork's balance carries the `N * count` bound; its `consistentUpTo`
+shows the counted channel is consistent under the fork's `BalancedUpTo N`.
+Nothing else uses it.
 
 ## Known differences from the Rust prover
 
-- `LT` constrains `μ·(1 − μ) = 0`. The spec types `μ` as `Byte` with
-  `IS_BYTE[μ]` and `lt.rs` sends `ARE_BYTES[μ, 0]`, because LT deduplicates
-  rows and `μ` is a count. Clean only grants a channel guarantee to a pull with
-  multiplicity exactly 1, so until the counted pulls above land upstream the
-  model keeps `μ` a bit. Every chip whose `μ` the spec types as `Byte` (MUL,
-  DVRM, BRANCH, BYTEWISE) will need the same treatment.
+- Every chip whose `μ` the spec types as `Byte` (MUL, DVRM, BRANCH, BYTEWISE)
+  needs the counted treatment LT got above; none of them is modelled yet.
 - The `spec/` copy in this repository lags the `spec/main` branch; the spec the
   models follow is the branch (EQ's `μ` is `Bit` with `IS_BIT[μ]` there).