From 3b0497091da2520e40672e82e90e6414607737b9 Mon Sep 17 00:00:00 2001
From: jotabulacios <jbulacios@fi.uba.ar>
Date: Mon, 2 Nov 2026 14:53:51 -0300
Subject: [PATCH 1/6] Bump Clean to f3abad7c (current main, Lean v4.35.0) and
 adapt the model to its channel API.

Clean removed StaticLookupChannel in favour of Air.Flat.Lookup, so the structure moves to
LambdaVM/StaticLookup.lean and BITWISE reads its tables through toChannel. Interactions now carry a
direction and a nonnegative multiplicity, and a pull must have multiplicity 0 or 1: EQ, LT and SHIFT
discharge that from their existing bit constraints, and their guarantees are stated for
multiplicity 1 instead of -1. EqLookup is rewritten for the current SoundEnsemble API (a balance
parameter, channels added before tables, unique table names, a demand generation mode per
component), and eq_rows_correct takes the InteractionsFit premise that TableSoundness now has.
Channels/Counted.lean is ported to directions; not_consistent needs only two interactions, since a
pull of multiplicity N >= 2 counts as a push. A grind call in IsByte that no longer closes its goal
is replaced by a direct proof. The export now records each interaction's direction, so the JSON
files are regenerated and lean_diff.rs signs Lean multiplicities by direction. Nothing that is
proven changes.
---
 formal/LambdaVM.lean                    |   1 +
 formal/LambdaVM/Channels/Counted.lean   | 199 +++++++++++++-----------
 formal/LambdaVM/Ensembles/EqLookup.lean | 125 ++++++++++-----
 formal/LambdaVM/StaticLookup.lean       |  31 ++++
 formal/LambdaVM/Tables/Bitwise.lean     |  17 +-
 formal/LambdaVM/Tables/Eq.lean          |   8 +-
 formal/LambdaVM/Tables/Lt.lean          |   7 +-
 formal/LambdaVM/Tables/Shift.lean       |  40 ++---
 formal/LambdaVM/Templates/IsByte.lean   |   5 +-
 formal/export/eq.json                   |  31 ++--
 formal/export/lt.json                   |  49 ++----
 formal/export/shift.json                | 145 +++++++----------
 formal/lake-manifest.json               |  32 ++--
 formal/lakefile.toml                    |   2 +-
 formal/lean-toolchain                   |   2 +-
 prover/src/tests/lean_diff.rs           |  15 +-
 16 files changed, 379 insertions(+), 330 deletions(-)
 create mode 100644 formal/LambdaVM/StaticLookup.lean

diff --git a/formal/LambdaVM.lean b/formal/LambdaVM.lean
index 9950beb14..298ab5036 100644
--- a/formal/LambdaVM.lean
+++ b/formal/LambdaVM.lean
@@ -2,6 +2,7 @@ module
 
 public import LambdaVM.Field
 public import LambdaVM.AluOp
+public import LambdaVM.StaticLookup
 public import LambdaVM.Templates.IsBit
 public import LambdaVM.Templates.Add
 public import LambdaVM.Tables.Bitwise
diff --git a/formal/LambdaVM/Channels/Counted.lean b/formal/LambdaVM/Channels/Counted.lean
index 00627daa0..d3c4c0981 100644
--- a/formal/LambdaVM/Channels/Counted.lean
+++ b/formal/LambdaVM/Channels/Counted.lean
@@ -9,16 +9,17 @@ public import Mathlib.Tactic.LinearCombination
 /-!
 # Counted pulls
 
-A deduplicated row pulls its range checks with multiplicity `-μ`, `μ ∈ [0, 255]`
-(`MU_MAX`, PR #1016). Clean grants a channel guarantee at multiplicity `-1` only.
-`counted N channel` is the raw channel that grants it at `-1, …, -N` and charges every other
-nonzero multiplicity with the requirement, exactly as `Channel.toRaw` does for `-1`.
-
-The price is in the balance premise. `exists_push_of_pull` needs `N · length < char F`;
-Clean's `BalancedInteractions` only provides `length < char F`, and `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`).
+A deduplicated row pulls its range checks with multiplicity `μ ∈ [0, 255]` (`MU_MAX`, PR #1016).
+Clean's typed channels give the guarantee only to a pull of multiplicity `1`, and require every
+pull to have multiplicity `0` or `1`. `counted N channel` is the raw channel that gives the
+guarantee to a pull of multiplicity `1, …, N` and charges every other nonzero interaction with
+the requirement, as a push.
+
+The price is in the balance premise. `exists_push_of_pull` needs `N · length < char F`. Clean's
+`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`).
 -/
 
 namespace LambdaVM.Counted
@@ -26,8 +27,8 @@ namespace LambdaVM.Counted
 variable {F : Type} [FiniteField F] [DecidableEq F]
 variable {Message : TypeMap} [ProvableType Message]
 
-/-- `mult = -k` for a count `1 ≤ k ≤ N`. -/
-def IsPull (N : ℕ) (mult : F) : Prop := ∃ k : ℕ, 1 ≤ k ∧ k ≤ N ∧ mult = -(k : F)
+/-- `mult = k` for a count `1 ≤ k ≤ N`. -/
+def IsPull (N : ℕ) (mult : F) : Prop := ∃ k : ℕ, 1 ≤ k ∧ k ≤ N ∧ mult = (k : F)
 
 /-- `channel` with pulls allowed to carry a count up to `N`. -/
 def counted (N : ℕ) (channel : Channel F Message) : RawChannel F where
@@ -35,49 +36,59 @@ def counted (N : ℕ) (channel : Channel F Message) : RawChannel F where
   arity := size Message
   Guarantees mult message data :=
     IsPull N mult → channel.Guarantees (fromElements message) data
-  Requirements mult message data :=
-    mult ≠ 0 → ¬ IsPull N mult → channel.Guarantees (fromElements message) data
+  Requirements direction mult message data :=
+    match direction with
+    | .push => mult ≠ 0 → channel.Guarantees (fromElements message) data
+    | .pull => mult ≠ 0 → ¬ IsPull N mult → channel.Guarantees (fromElements message) data
 
-/-- Pull `msg` with multiplicity `-count`. -/
+/-- Pull `msg` `count` times. -/
 @[circuit_norm]
 def pullIf (N : ℕ) (channel : Channel F Message) (count : Expression F)
     (msg : Message (Expression F)) : Circuit F Unit := fun _ =>
-  ((), [.interact ⟨counted N channel, -count, toElements msg, true⟩])
+  ((), [.interact ⟨counted N channel, .pull, count, toElements msg⟩])
 
 /-- The provider side: emit `msg` with multiplicity `mult`. -/
 @[circuit_norm]
 def emit (N : ℕ) (channel : Channel F Message) (mult : Expression F)
     (msg : Message (Expression F)) : Circuit F Unit := fun _ =>
-  ((), [.interact ⟨counted N channel, mult, toElements msg, false⟩])
+  ((), [.interact ⟨counted N channel, .push, mult, toElements msg⟩])
 
 instance {N : ℕ} {channel : Channel F Message} {count : Expression F} :
     ExplicitCircuits (F := F) (pullIf N channel count) where
   output _ _ := ()
   localLength _ _ := 0
-  operations msg _ := [.interact ⟨counted N channel, -count, toElements msg, true⟩]
+  operations msg _ := [.interact ⟨counted N channel, .pull, count, toElements msg⟩]
   channelsWithGuarantees _ _ := [counted N channel]
 
 instance {N : ℕ} {channel : Channel F Message} {mult : Expression F} :
     ExplicitCircuits (F := F) (emit N channel mult) where
   output _ _ := ()
   localLength _ _ := 0
-  operations msg _ := [.interact ⟨counted N channel, mult, toElements msg, false⟩]
+  operations msg _ := [.interact ⟨counted N channel, .push, mult, toElements msg⟩]
   channelsWithGuarantees _ _ := []
 
 attribute [explicit_circuit_no_unfold] pullIf emit
 
-/-- `RawChannel.Normal` with the pull multiplicity `-1` widened to `-1, …, -N`. -/
+/-- An interaction that acts as a push of its message: an active push, or a pull whose
+multiplicity is not a count. -/
+def PushLike (N : ℕ) (i : Interaction F) : Prop :=
+  i.mult ≠ 0 ∧ (i.direction = .pull → ¬ IsPull N i.mult)
+
+/-- `RawChannel.Normal` with the pull multiplicity `1` widened to `1, …, N`. -/
 class Normal (N : ℕ) (channel : RawChannel F) : Prop where
-  grts_of_reqs : ∀ (msg : Vector F channel.arity) (mult : F) data, mult ≠ 0 → ¬ IsPull N mult →
-    channel.Requirements mult msg data → ∀ mult', IsPull N mult' → channel.Guarantees mult' msg data
+  grts_of_reqs : ∀ (msg : Vector F channel.arity) (direction : Channel.Direction) (mult : F) data,
+    mult ≠ 0 → (direction = .pull → ¬ IsPull N mult) →
+    channel.Requirements direction mult msg data →
+    ∀ mult', IsPull N mult' → channel.Guarantees mult' msg data
   grts_of_not_pull : ∀ (msg : Vector F channel.arity) (mult : F) data, ¬ IsPull N mult →
     channel.Guarantees mult msg data
 
 instance (N : ℕ) (channel : Channel F Message) : Normal N (counted N channel) where
   grts_of_reqs := by
-    intro msg mult data h0 hnp reqs mult' hp
-    simp only [counted] at reqs ⊢
-    exact fun _ => reqs h0 hnp
+    intro msg direction mult data h0 hnp reqs mult' hp
+    cases direction <;> simp only [counted] at reqs ⊢
+    · exact fun _ => reqs h0
+    · exact fun _ => reqs h0 (hnp rfl)
   grts_of_not_pull := by
     intro msg mult data hnp
     simp only [counted]
@@ -87,7 +98,7 @@ instance (N : ℕ) (channel : Channel F Message) : Normal N (counted N channel)
 natural number bounded by `N` per interaction, and positive as soon as one pull is active. -/
 lemma balanceOf_counted (N : ℕ) (msg : Array F) :
     ∀ (l : List (Interaction F)),
-    (∀ i ∈ l, i.msg = msg → i.mult ≠ 0 → IsPull N i.mult) →
+    (∀ i ∈ l, i.msg = msg → i.mult ≠ 0 → i.direction = .pull ∧ IsPull N i.mult) →
     ∃ s : ℕ, s ≤ N * l.length ∧ balanceOf l msg = -(s : F) ∧
       (∀ a ∈ l, a.msg = msg → a.mult ≠ 0 → 1 ≤ s)
   | [], _ => ⟨0, by simp, by simp [balanceOf], by simp⟩
@@ -99,14 +110,18 @@ lemma balanceOf_counted (N : ℕ) (msg : Array F) :
     by_cases hm : i.msg = msg
     · by_cases h0 : i.mult = 0
       · refine ⟨s, by omega, ?_, ?_⟩
-        · rw [if_pos hm, h0, hb, zero_add]
+        · have hsigned : i.signedMult = 0 := by
+            cases hd : i.direction <;> simp [Interaction.signedMult, hd, h0]
+          rw [if_pos hm, hsigned, hb, zero_add]
         · intro a ha' ham ha0
           rcases List.mem_cons.mp ha' with rfl | ha'
           · exact absurd h0 ha0
           · exact ha a ha' ham ha0
-      · obtain ⟨k, hk1, hkN, hk⟩ := h i (by simp) hm h0
+      · obtain ⟨hd, k, hk1, hkN, hk⟩ := h i (by simp) hm h0
         refine ⟨k + s, by omega, ?_, ?_⟩
-        · rw [if_pos hm, hk, hb]; push_cast; ring
+        · rw [if_pos hm, hb]
+          simp only [Interaction.signedMult, hd, hk]
+          push_cast; ring
         · intro a _ _ _; omega
     · refine ⟨s, by omega, ?_, ?_⟩
       · rw [if_neg hm, hb, zero_add]
@@ -116,20 +131,26 @@ lemma balanceOf_counted (N : ℕ) (msg : Array F) :
         · exact ha a ha' ham ha0
 
 /-- `exists_push_of_pull` for counted pulls. The balance premise must bound the total count,
-`N * length`, by the characteristic; Clean's `BalancedInteractions` bounds `length` only. -/
+`N * length`, by the characteristic; Clean's `BalancedInteractions` only matches pulls of
+multiplicity `1`. -/
 theorem exists_push_of_pull (N : ℕ) (interactions : List (Interaction F))
     (bound : N * interactions.length < ringChar F ∨ ringChar F = 0)
     (balance : ∀ msg, balanceOf interactions msg = 0) :
-    ∀ a ∈ interactions, IsPull N a.mult →
-      ∃ b ∈ interactions, b.msg = a.msg ∧ b.mult ≠ 0 ∧ ¬ IsPull N b.mult := by
-  intro a ha hpull
+    ∀ a ∈ interactions, a.direction = .pull → IsPull N a.mult →
+      ∃ b ∈ interactions, b.msg = a.msg ∧ PushLike N b := by
+  intro a ha hdir hpull
   by_contra! hno
-  obtain ⟨s, hs, hb, h1⟩ := balanceOf_counted N a.msg interactions hno
+  have hno' : ∀ i ∈ interactions, i.msg = a.msg → i.mult ≠ 0 →
+      i.direction = .pull ∧ IsPull N i.mult := by
+    intro i hi hm h0
+    by_contra hc
+    exact hno i hi hm ⟨h0, fun hd hp => hc ⟨hd, hp⟩⟩
+  obtain ⟨s, hs, hb, h1⟩ := balanceOf_counted N a.msg interactions hno'
   have hlen : 0 < interactions.length := List.length_pos_of_mem ha
   have hNlen : N ≤ N * interactions.length := Nat.le_mul_of_pos_right N hlen
   have ha0 : a.mult ≠ 0 := by
     obtain ⟨k, hk1, hkN, hk⟩ := hpull
-    rw [hk, neg_ne_zero]
+    rw [hk]
     rcases bound with bound | hchar
     · intro hk0
       rw [Lean.Grind.IsCharP.natCast_eq_zero_iff_of_lt _ (by omega)] at hk0
@@ -155,15 +176,16 @@ theorem consistent (N : ℕ) (channel : RawChannel F) [Normal N channel]
     ∀ i ∈ interactions, i.Guarantees data := by
   intro a a_mem
   simp only [Interaction.Guarantees, Interaction.Requirements, Interaction.msgVector] at reqs ⊢
-  intro _
+  intro hdir
   have a_channel_eq := (reqs a a_mem).1
   have a_msg_size : a.msg.size = channel.arity := by rw [a.same_size, a_channel_eq]
   suffices channel.Guarantees a.mult ⟨a.msg, a_msg_size⟩ data by convert this
   by_cases a_pull : IsPull N a.mult
   case neg => exact Normal.grts_of_not_pull ⟨a.msg, a_msg_size⟩ a.mult data a_pull
   obtain ⟨b, b_mem, b_msg_eq, b_ne_zero, b_not_pull⟩ :=
-    exists_push_of_pull N interactions bound balance a a_mem a_pull
-  apply Normal.grts_of_reqs ⟨a.msg, a_msg_size⟩ b.mult data b_ne_zero b_not_pull _ a.mult a_pull
+    exists_push_of_pull N interactions bound balance a a_mem hdir a_pull
+  apply Normal.grts_of_reqs ⟨a.msg, a_msg_size⟩ b.direction b.mult data b_ne_zero b_not_pull _
+    a.mult a_pull
   have ⟨b_channel_eq, b_reqs⟩ := reqs _ b_mem
   symm at b_channel_eq
   simp only [b_msg_eq] at b_reqs
@@ -172,7 +194,7 @@ theorem consistent (N : ℕ) (channel : RawChannel F) [Normal N channel]
 /-! ## `N = 1` is Clean's normal channel -/
 
 omit [DecidableEq F] in
-lemma isPull_one_iff (mult : F) : IsPull 1 mult ↔ mult = -1 := by
+lemma isPull_one_iff (mult : F) : IsPull 1 mult ↔ mult = 1 := by
   constructor
   · rintro ⟨k, hk1, hk, rfl⟩
     have : k = 1 := by omega
@@ -180,14 +202,19 @@ lemma isPull_one_iff (mult : F) : IsPull 1 mult ↔ mult = -1 := by
   · rintro rfl; exact ⟨1, le_rfl, le_rfl, by simp⟩
 
 instance (channel : Channel F Message) : (counted 1 channel).Normal where
-  grts_of_reqs := by
-    intro msg mult data h0 h1 reqs
-    simp only [counted, isPull_one_iff] at reqs ⊢
-    exact fun _ => reqs h0 h1
-  grts_of_ne_neg_one := by
-    intro msg mult data h1
-    simp only [counted, isPull_one_iff]
-    exact fun h => absurd h h1
+  guarantees_of_requirements := by
+    rintro ⟨_, a_direction, a_mult, a_msg, a_size⟩ ⟨_, b_direction, b_mult, b_msg, b_size⟩
+      data rfl rfl (rfl : a_msg = b_msg) a_pull ⟨b_ne_zero, b_not_one⟩ b_reqs
+    cases b_direction <;>
+      simp only [Interaction.Guarantees, Interaction.Requirements, Interaction.msgVector, counted,
+        isPull_one_iff] at b_reqs ⊢
+    · exact fun _ _ => b_reqs b_ne_zero
+    · exact fun _ _ => b_reqs b_ne_zero (b_not_one rfl)
+  guarantees_of_not_pull := by
+    rintro ⟨_, direction, mult, msg, size⟩ data rfl not_pull
+    simp only [Interaction.Pull, not_and] at not_pull
+    simp only [Interaction.Guarantees, counted, isPull_one_iff]
+    exact fun h_direction h_mult => absurd h_mult (not_pull h_direction)
 
 example (channel : Channel F Message) : (counted 1 channel).Consistent := inferInstance
 
@@ -198,52 +225,41 @@ end LambdaVM.Counted
 namespace LambdaVM.Counted
 variable {Message : TypeMap} [ProvableType Message]
 
-/-- The witness `BalancedInteractions` admits but the counted channel cannot survive:
-`p / N` pulls of `-N` and `p % N` pulls of `-1` on one message, nothing pushed. It has fewer
-than `p` interactions, balances to `-p = 0`, and claims the guarantee on a message that is
-not in the table. -/
+/-- The witness `BalancedInteractions` admits but the counted channel cannot survive: one pull of
+`N` and one pull of `1` on a message that is not in the table, nothing pushed. Clean counts the
+pull of `N` as a push of the message, so the pull of `1` is matched; the counted channel reads
+both as pulls, and the guarantee of the second is false. -/
 theorem not_consistent (N : ℕ) (hN : 2 ≤ N) (hN' : N ≤ 255)
     (channel : Channel (F p) Message) (m : Message (F p)) (data : ProverData (F p))
     (hm : ¬ channel.Guarantees m data) : ¬ (counted N channel).Consistent := by
   rintro ⟨hc⟩
   let mk : F p → Interaction (F p) := fun mult =>
-    ⟨counted N channel, mult, (toElements m).toArray, by simp [counted], true⟩
-  let l := List.replicate (p / N) (mk (-(N : F p))) ++ List.replicate (p % N) (mk (-1))
-  have hdvd : ¬ N ∣ p := by
-    intro h
-    rcases (Fact.out : p.Prime).eq_one_or_self_of_dvd N h with h1 | h2
-    · omega
-    · have : (255 : ℕ) < p := by decide
-      omega
-  have hmod : 0 < p % N := Nat.pos_of_ne_zero (fun h => hdvd (Nat.dvd_of_mod_eq_zero h))
-  have hmem : mk (-1) ∈ l := by
-    simp only [l, List.mem_append, List.mem_replicate]
-    exact Or.inr ⟨by omega, trivial⟩
-  have hlen : l.length < ringChar (F p) ∨ ringChar (F p) = 0 := by
-    left
-    rw [ZMod.ringChar_zmod_n]
-    simp only [l, List.length_append, List.length_replicate]
-    have h1 : p / N ≤ p / 2 := Nat.div_le_div_left hN (by norm_num)
-    have h2 : p % N < N := Nat.mod_lt _ (by omega)
-    have h3 : p / 2 + 255 < p := by decide
-    omega
-  have hbal : ∀ msg, balanceOf l msg = 0 := by
-    intro msg
-    simp only [l, balanceOf_append]
-    rw [balanceOf_eq_of_const_mult' (mult := -(N : F p)) (by intro i hi; rw [(List.mem_replicate.mp hi).2]),
-      balanceOf_eq_of_const_mult' (mult := -1) (by intro i hi; rw [(List.mem_replicate.mp hi).2])]
-    simp only [List.countP_replicate]
-    by_cases hmsg : (toElements m).toArray = msg
-    · simp only [mk, hmsg, decide_true, if_true]
-      have : ((N * (p / N) + p % N : ℕ) : F p) = 0 := by
-        rw [Nat.div_add_mod]; exact ZMod.natCast_self p
-      push_cast at this
-      linear_combination -this
-    · simp [mk, hmsg]
+    ⟨counted N channel, .pull, mult, (toElements m).toArray, by simp [counted]⟩
+  let l := [mk (N : F p), mk 1]
+  have hval : ((N : ℕ) : F p).val = N := ZMod.val_natCast_of_lt (lt_p_of_lt_two_pow_40 (by omega))
+  have hN0 : (N : F p) ≠ 0 := by
+    intro h; have := congrArg ZMod.val h; rw [hval, ZMod.val_zero] at this; omega
+  have hN1 : (N : F p) ≠ 1 := by
+    intro h; have := congrArg ZMod.val h; rw [hval, ZMod.val_one] at this; omega
+  have hbal : BalancedInteractions l := by
+    constructor
+    · -- the pull of `1` is matched by the pull of `N`, which Clean reads as a push
+      intro a ha _
+      refine ⟨mk (N : F p), by simp [l], ?_, hN0, fun _ => hN1⟩
+      simp only [l, List.mem_cons, List.not_mem_nil, or_false] at ha
+      rcases ha with rfl | rfl <;> rfl
+    · -- the multiplicity `N` is not `0` or `1`, so only messages with no interaction qualify
+      intro msg is_bool
+      by_cases hmsg : (toElements m).toArray = msg
+      · exfalso
+        rcases is_bool (mk (N : F p)) (by simp [l]) hmsg with h | h
+        · exact hN0 h
+        · exact hN1 h
+      · simp [activeCount, l, mk, hmsg]
   have hreqs : ∀ i ∈ l, i.channel = counted N channel ∧ i.Requirements data := by
     intro i hi
-    simp only [l, List.mem_append, List.mem_replicate] at hi
-    rcases hi with ⟨_, rfl⟩ | ⟨_, rfl⟩
+    simp only [l, List.mem_cons, List.not_mem_nil, or_false] at hi
+    rcases hi with rfl | rfl
     · refine ⟨rfl, ?_⟩
       simp only [Interaction.Requirements, mk, counted, Interaction.msgVector]
       intro _ hnp
@@ -252,7 +268,7 @@ theorem not_consistent (N : ℕ) (hN : 2 ≤ N) (hN' : N ≤ 255)
       simp only [Interaction.Requirements, mk, counted, Interaction.msgVector]
       intro _ hnp
       exact absurd ⟨1, le_rfl, by omega, by simp⟩ hnp
-  have hg := hc l data ⟨hlen, hbal⟩ hreqs (mk (-1)) hmem
+  have hg := hc l data hbal hreqs (mk 1) (by simp [l])
   simp only [Interaction.Guarantees, mk, counted, Interaction.msgVector] at hg
   apply hm
   have h := hg trivial ⟨1, le_rfl, by omega, by simp⟩
@@ -264,7 +280,7 @@ end LambdaVM.Counted
 /-! ## A deduplicated row
 
 `μ` is range-checked as a byte through `ARE_BYTES` and `x` is pulled from `IS_HALF` with
-multiplicity `-μ`: the shape of every dedup chip after PR #1016. The counted channel is listed
+multiplicity `μ`: the shape of every dedup chip after PR #1016. The counted channel is listed
 under `channelsWithRequirements` because the requirement on an out-of-range `μ` is only
 discharged by the byte guarantee, which lawfulness cannot see; soundness can. -/
 
@@ -292,18 +308,17 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
   soundness := by
     circuit_proof_start [main, pullIf, counted, areBytesTable, isHalfTable]
     simp only [AbstractInteraction.Guarantees, AbstractInteraction.Requirements, circuit_norm,
-      ProvableType.fromElements_eval_toElements, h_input] at h_holds ⊢
+      h_input] at h_holds ⊢
     obtain ⟨⟨h_mu, _⟩, h_x⟩ := h_holds
     -- an active row pulls with the count `μ.val ∈ [1, 255]`
-    have key : input_mu ≠ 0 → IsPull 255 (-input_mu) := fun h0 =>
+    have key : input_mu ≠ 0 → IsPull 255 input_mu := fun h0 =>
       ⟨input_mu.val, by have := (ZMod.val_ne_zero _).mpr h0; omega, by omega,
         by rw [ZMod.natCast_zmod_val]⟩
     refine ⟨fun h0 => h_x (key h0), fun h0 hnp => absurd (key ?_) hnp⟩
     exact h0
   completeness := by
     circuit_proof_start [main, pullIf, counted, areBytesTable, isHalfTable]
-    simp only [AbstractInteraction.Guarantees, circuit_norm,
-      ProvableType.fromElements_eval_toElements, h_input]
+    simp only [AbstractInteraction.Guarantees, circuit_norm, h_input]
     exact ⟨⟨h_assumptions.1, by rw [ZMod.val_zero]; norm_num⟩, fun _ => h_assumptions.2⟩
 
 end LambdaVM.Counted.Demo
diff --git a/formal/LambdaVM/Ensembles/EqLookup.lean b/formal/LambdaVM/Ensembles/EqLookup.lean
index e9de6b71a..d031460e1 100644
--- a/formal/LambdaVM/Ensembles/EqLookup.lean
+++ b/formal/LambdaVM/Ensembles/EqLookup.lean
@@ -22,14 +22,15 @@ table with the prover's multiplicity for it. Its row is the vector of multiplici
 role the `μ` columns of BITWISE play. -/
 def pushStatic {Message : TypeMap} [ProvableType Message] (slc : StaticLookupChannel (F p) Message)
     [NeZero slc.table.length] : GeneralFormalCircuit (F p) (fields slc.table.length) unit where
+  name := slc.name
   main mults := do
     let _ ← Circuit.mapFinRange slc.table.length fun i =>
-      (Channel.fromStatic (F p) Message slc).emit mults[i] (const slc.table[i])
-  channelsWithRequirements := [(Channel.fromStatic (F p) Message slc).toRaw]
+      slc.toChannel.emit mults[i] (const slc.table[i])
+  channelsWithRequirements := [slc.toChannel.toRaw]
   Spec _ _ _ := True
   soundness := by
     circuit_proof_start
-    intro i _ _
+    intro i _
     exact (slc.guarantees_iff _).mpr (List.getElem_mem _)
   completeness := by circuit_proof_start
 
@@ -43,58 +44,98 @@ lemma pushStatic_channelsWithGuarantees {Message : TypeMap} [ProvableType Messag
 @[circuit_norm]
 lemma pushStatic_channelsWithRequirements {Message : TypeMap} [ProvableType Message]
     (slc : StaticLookupChannel (F p) Message) [NeZero slc.table.length] :
-    (pushStatic slc).channelsWithRequirements = [(Channel.fromStatic (F p) Message slc).toRaw] := rfl
+    (pushStatic slc).channelsWithRequirements = [slc.toChannel.toRaw] := rfl
 
-lemma RawChannel.ne_of_name_ne {c1 c2 : RawChannel (F p)} (h : c1.name ≠ c2.name) : c1 ≠ c2 :=
-  fun e => h (congrArg RawChannel.name e)
+/-- The provider as a component. Clean main asks every component for its witness generation;
+the multiplicities are counted from the demand on the channel. -/
+def pushStaticComponent {Message : TypeMap} [ProvableType Message]
+    (slc : StaticLookupChannel (F p) Message) [NeZero slc.table.length] : Component (F p) where
+  circuit := pushStatic slc
+  generation := .demand {
+    channel := slc.toChannel
+    trigger := .pull
+    input _ := pure (fromElements (Vector.replicate slc.table.length .multiplicity)) }
+
+/-- The EQ chip as a component, generated from the demand on the ALU bus. -/
+def eqComponent : Component (F p) where
+  circuit := EQ.circuit
+  generation := .demand {
+    channel := Alu.channel
+    trigger := .push
+    input _ := pure (fromElements (Vector.replicate (size EQ.Row) .multiplicity)) }
+
+@[circuit_norm] lemma pushStaticComponent_circuit {Message : TypeMap} [ProvableType Message]
+    (slc : StaticLookupChannel (F p) Message) [NeZero slc.table.length] :
+    (pushStaticComponent slc).circuit = pushStatic slc := rfl
+@[circuit_norm] lemma pushStatic_name {Message : TypeMap} [ProvableType Message]
+    (slc : StaticLookupChannel (F p) Message) [NeZero slc.table.length] :
+    (pushStatic slc).name = slc.name := rfl
+@[circuit_norm] lemma eqComponent_circuit : eqComponent.circuit = EQ.circuit := rfl
+@[circuit_norm] lemma pushStaticComponent_channelsWithGuarantees {Message : TypeMap}
+    [ProvableType Message] (slc : StaticLookupChannel (F p) Message) [NeZero slc.table.length] :
+    (pushStaticComponent slc).circuit.channelsWithGuarantees = [] :=
+  pushStatic_channelsWithGuarantees slc
+@[circuit_norm] lemma pushStaticComponent_channelsWithRequirements {Message : TypeMap}
+    [ProvableType Message] (slc : StaticLookupChannel (F p) Message) [NeZero slc.table.length] :
+    (pushStaticComponent slc).circuit.channelsWithRequirements = [slc.toChannel.toRaw] := rfl
+@[circuit_norm] lemma eq_name : EQ.circuit.name = "EQ" := rfl
+@[circuit_norm] lemma isHalfTable_name : Bitwise.isHalfTable.name = "IS_HALF" := rfl
+@[circuit_norm] lemma zeroTable_name : Bitwise.zeroTable.name = "ZERO" := rfl
+@[circuit_norm] lemma alu_name : Alu.channel.name = "ALU" := rfl
+@[circuit_norm] lemma eqComponent_channelsWithGuarantees :
+    eqComponent.circuit.channelsWithGuarantees = [Bitwise.IsHalf.toRaw, Bitwise.IsHalf.toRaw,
+      Bitwise.IsHalf.toRaw, Bitwise.IsHalf.toRaw, Bitwise.Zero.toRaw] := rfl
+@[circuit_norm] lemma eqComponent_channelsWithRequirements :
+    eqComponent.circuit.channelsWithRequirements = [Alu.channel.toRaw] := rfl
 
 instance : NeZero Bitwise.isHalfTable.table.length :=
   ⟨by simp [Bitwise.isHalfTable, Bitwise.rows, Bitwise.numRows]⟩
 instance : NeZero Bitwise.zeroTable.table.length :=
   ⟨by simp [Bitwise.zeroTable, Bitwise.rows, Bitwise.numRows]⟩
 
-def eqLookup : SoundEnsemble (F p) unit :=
-  SoundEnsemble.empty (F p) unit
-  |>.addTable ⟨pushStatic Bitwise.isHalfTable⟩
-      (by rw [pushStatic_channelsWithGuarantees]; simp)
-      (by simp only [circuit_norm, List.not_mem_nil, false_implies, implies_true])
-  |>.addFinishedChannel Bitwise.IsHalf.toRaw
-  |>.addTable ⟨pushStatic Bitwise.zeroTable⟩
-      (by rw [pushStatic_channelsWithGuarantees]; simp)
-      (by
-        intro channel hc
-        simp only [circuit_norm, List.mem_singleton] at hc
-        subst hc
-        rw [pushStatic_channelsWithRequirements, List.mem_singleton]
-        exact RawChannel.ne_of_name_ne (by decide))
-  |>.addFinishedChannel Bitwise.Zero.toRaw
-  |>.addTable ⟨EQ.circuit⟩
-      (by simp [circuit_norm, EQ.circuit, Bitwise.isHalfTable, Bitwise.zeroTable])
-      (by simp [circuit_norm, EQ.circuit, Alu.channel, Bitwise.isHalfTable, Bitwise.zeroTable])
-  |>.addFinishedChannel Alu.channel.toRaw
+def eqLookup (balance : Balance (F p)) : SoundEnsemble (F p) unit balance :=
+  SoundEnsemble.empty (F p) unit balance
+  |>.addChannel Bitwise.IsHalf.toRaw
+  |>.addTable (pushStaticComponent Bitwise.isHalfTable)
+      (by rw [pushStaticComponent_channelsWithGuarantees]; exact List.nil_subset _)
+      (by rw [pushStaticComponent_channelsWithRequirements]; simp [circuit_norm])
+  |>.markFinished Bitwise.IsHalf.toRaw
+  |>.addChannel Bitwise.Zero.toRaw
+  |>.addTable (pushStaticComponent Bitwise.zeroTable)
+      (by rw [pushStaticComponent_channelsWithGuarantees]; exact List.nil_subset _)
+      (by rw [pushStaticComponent_channelsWithRequirements]; simp [circuit_norm])
+  |>.markFinished Bitwise.Zero.toRaw
+  |>.addChannel Alu.channel.toRaw
+  |>.addTable eqComponent
+      (by rw [eqComponent_channelsWithGuarantees]; simp [circuit_norm])
+      (by rw [eqComponent_channelsWithRequirements]; simp [circuit_norm])
+  |>.markFinished Alu.channel.toRaw
 
-/-- Lookup soundness, concretely: if the constraints of every table hold and every channel
-balances, then every EQ row with `μ = 1` and range-checked operands carries the equality bit. -/
-theorem eq_rows_correct (witness : EnsembleWitness eqLookup.ensemble)
-    (hc : witness.Constraints) (hb : witness.BalancedChannels) :
-    ∀ table ∈ witness.tables, table.component = ⟨EQ.circuit⟩ →
+/-- Lookup soundness, concretely: if the constraints of every table hold, every channel has few
+enough interactions for the balance check, and every channel balances, then every EQ row with
+`μ = 1` and range-checked operands carries the equality bit. -/
+theorem eq_rows_correct {balance : Balance (F p)}
+    (witness : EnsembleWitness (eqLookup balance).ensemble)
+    (hc : witness.Constraints) (hfit : witness.InteractionsFit balance)
+    (hb : witness.Balanced balance) :
+    ∀ table ∈ witness.tables, table.component = eqComponent →
       ∀ row ∈ table.table, EQ.RowSpec (valueFromOffset EQ.Row 0 (table.environment row)) := by
-  have hsound : eqLookup.ensemble.TableSoundness :=
+  have hsound : (eqLookup balance).ensemble.TableSoundness balance :=
     Ensemble.tableSoundness_of_soundChannels
-      ⟨eqLookup.finished, eqLookup.finished_subset, eqLookup.soundChannels⟩
+      ⟨(eqLookup balance).finished, (eqLookup balance).finished_subset,
+        (eqLookup balance).soundChannels⟩
+  -- no component assumes anything
   have hassume : witness.Assumptions := by
-    intro table htable
-    have hmem := EnsembleWitness.mem_allTables_component_of_mem_allTables htable
-    simp only [circuit_norm, eqLookup, Ensemble.allTables, List.mem_cons, List.not_mem_nil,
-      or_false] at hmem
-    obtain ⟨comp, width, tbl, data, uw⟩ := table
+    intro table htable row _
+    have hmem := witness.component_mem_tables_of_mem htable
+    simp only [eqLookup, circuit_norm, List.mem_cons, List.not_mem_nil, or_false] at hmem
+    obtain ⟨comp, tbl, data, uw, ll, frm, dc⟩ := table
     simp only at hmem
-    intro row _
-    rcases hmem with h | h | h | h <;> subst h <;> exact trivial
-  have hspec := hsound witness hassume hc hb
+    rcases hmem with rfl | rfl | rfl <;> trivial
+  have hspec := (hsound witness hassume hc hfit hb).2
   intro table htable hcomp row hrow
-  have := hspec table (witness.mem_allTables_of_mem_tables htable) row hrow
-  obtain ⟨comp, width, tbl, data, uw⟩ := table
+  have := hspec table htable row hrow
+  obtain ⟨comp, tbl, data, uw, ll, frm, dc⟩ := table
   simp only at hcomp
   subst hcomp
   exact this
diff --git a/formal/LambdaVM/StaticLookup.lean b/formal/LambdaVM/StaticLookup.lean
new file mode 100644
index 000000000..04301bb1b
--- /dev/null
+++ b/formal/LambdaVM/StaticLookup.lean
@@ -0,0 +1,31 @@
+module
+
+public import Clean.Circuit.Channel
+
+@[expose] public section
+
+/-!
+# Static lookup channels
+
+A table the verifier knows, given as a list of rows, read through a channel whose guarantee is
+the semantic reading of a row. Clean main replaced its `StaticLookupChannel` by `Air.Flat.Lookup`,
+whose rows are witness programs of the row index. The formal model keeps its tables as lists, with
+`guarantees_iff` relating each list to its reading, so the structure lives here.
+-/
+
+namespace LambdaVM
+
+structure StaticLookupChannel (F : Type) [Field F] (Message : TypeMap) [ProvableType Message] where
+  name : String
+  table : List (Message F)
+  Guarantees : Message F → Prop
+  guarantees_iff : ∀ msg, Guarantees msg ↔ msg ∈ table
+
+/-- The channel through which other components read the table. -/
+@[circuit_norm]
+def StaticLookupChannel.toChannel {F : Type} [Field F] {Message : TypeMap} [ProvableType Message]
+    (slc : StaticLookupChannel F Message) : Channel F Message where
+  name := slc.name
+  Guarantees msg _ := slc.Guarantees msg
+
+end LambdaVM
diff --git a/formal/LambdaVM/Tables/Bitwise.lean b/formal/LambdaVM/Tables/Bitwise.lean
index a38ce9d86..b3fc628ca 100644
--- a/formal/LambdaVM/Tables/Bitwise.lean
+++ b/formal/LambdaVM/Tables/Bitwise.lean
@@ -2,6 +2,7 @@ module
 
 public import LambdaVM.Field
 public import LambdaVM.AluOp
+public import LambdaVM.StaticLookup
 
 @[expose] public section
 
@@ -120,7 +121,7 @@ def areBytesTable : StaticLookupChannel (F p) fieldPair where
       exact ⟨by rw [val_natCast_of_lt_two_pow_20 (by linarith [row_x_lt i])]; exact row_x_lt i,
              by rw [val_natCast_of_lt_two_pow_20 (by linarith [row_y_lt i])]; exact row_y_lt i⟩
 
-abbrev AreBytes : Channel (F p) fieldPair := .fromStatic _ _ areBytesTable
+abbrev AreBytes : Channel (F p) fieldPair := areBytesTable.toChannel
 
 /-- `IS_HALF[X + 2^8·Y]` (`BusId::IsHalfword`): the value is a halfword. -/
 def isHalfTable : StaticLookupChannel (F p) field where
@@ -142,7 +143,7 @@ def isHalfTable : StaticLookupChannel (F p) field where
       have := row_x_lt i; have := row_y_lt i
       rw [val_natCast_of_lt_two_pow_20 (by omega)]; omega
 
-abbrev IsHalf : Channel (F p) field := .fromStatic _ _ isHalfTable
+abbrev IsHalf : Channel (F p) field := isHalfTable.toChannel
 
 /-- `IS_B20[X + 2^8·Y + 2^16·Z]` (`BusId::IsB20`): the value is below `2^20`. -/
 def isB20Table : StaticLookupChannel (F p) field where
@@ -164,7 +165,7 @@ def isB20Table : StaticLookupChannel (F p) field where
       have := row_x_lt i; have := row_y_lt i; have := row_z_lt i
       rw [val_natCast_of_lt_two_pow_20 (by omega)]; omega
 
-abbrev IsB20 : Channel (F p) field := .fromStatic _ _ isB20Table
+abbrev IsB20 : Channel (F p) field := isB20Table.toChannel
 
 /-! ## Bit-extraction channels -/
 
@@ -194,7 +195,7 @@ def msb8Table : StaticLookupChannel (F p) fieldPair where
         row_msb8]
       exact ⟨this, rfl⟩
 
-abbrev Msb8 : Channel (F p) fieldPair := .fromStatic _ _ msb8Table
+abbrev Msb8 : Channel (F p) fieldPair := msb8Table.toChannel
 
 /-- `MSB16[X + 2^8·Y] -> MSB16` (`BusId::Msb16`): a halfword and its top bit. -/
 def msb16Table : StaticLookupChannel (F p) fieldPair where
@@ -222,7 +223,7 @@ def msb16Table : StaticLookupChannel (F p) fieldPair where
         row_msb16]
       exact ⟨by omega, rfl⟩
 
-abbrev Msb16 : Channel (F p) fieldPair := .fromStatic _ _ msb16Table
+abbrev Msb16 : Channel (F p) fieldPair := msb16Table.toChannel
 
 /-- `ZERO[X + 2^8·Y + 2^16·Z] -> ZERO` (`BusId::Zero`): a 20-bit value and its zero flag. -/
 def zeroTable : StaticLookupChannel (F p) fieldPair where
@@ -257,7 +258,7 @@ def zeroTable : StaticLookupChannel (F p) fieldPair where
       simp only [hn]
       split_ifs <;> simp
 
-abbrev Zero : Channel (F p) fieldPair := .fromStatic _ _ zeroTable
+abbrev Zero : Channel (F p) fieldPair := zeroTable.toChannel
 
 /-! ## Byte ALU and halfword shift channels -/
 
@@ -319,7 +320,7 @@ def byteAluTable : StaticLookupChannel (F p) ByteAluMsg where
       · right; right; rw [row_xor, val_natCast_of_lt_two_pow_20 (by linarith [xor_lt_256 hx hy])]
         simp
 
-abbrev ByteAlu : Channel (F p) ByteAluMsg := .fromStatic _ _ byteAluTable
+abbrev ByteAlu : Channel (F p) ByteAluMsg := byteAluTable.toChannel
 
 /-- Message of `HWSL[X + 2^8·Y, Z] -> [SLL, SLLC]` (`BusId::Hwsl`). -/
 structure HwslMsg (F : Type) where
@@ -364,6 +365,6 @@ def hwslTable : StaticLookupChannel (F p) HwslMsg where
         row_sll, row_sllc, sll_eq hh, sllc_eq hh]
       exact ⟨hh, hz, rfl, rfl⟩
 
-abbrev Hwsl : Channel (F p) HwslMsg := .fromStatic _ _ hwslTable
+abbrev Hwsl : Channel (F p) HwslMsg := hwslTable.toChannel
 
 end LambdaVM.Bitwise
diff --git a/formal/LambdaVM/Tables/Eq.lean b/formal/LambdaVM/Tables/Eq.lean
index 48f1d4d65..3fcee4831 100644
--- a/formal/LambdaVM/Tables/Eq.lean
+++ b/formal/LambdaVM/Tables/Eq.lean
@@ -92,6 +92,7 @@ def RowSpec (r : Row (F p)) : Prop :=
     r.res = ((eqBit r.invert.val (dword r.a0 r.a1) (dword r.b0 r.b1) : ℕ) : F p)
 
 def circuit : GeneralFormalCircuit (F p) Row unit where
+  name := "EQ"
   main
   Spec r _ _ := RowSpec r
   channelsWithRequirements := [Alu.channel.toRaw]
@@ -102,9 +103,8 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
     constructor
     · intro channel h; tauto
     · intro env h
-      refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;>
-      · intro hne1 hne0
-        exact (requirement_vacuous h.2.2.2.2 hne1 hne0).elim
+      -- each pull owes a multiplicity of 0 or 1: μ is a bit
+      exact mul_one_sub_eq_zero_iff.mp h.2.2.2.2
 
   soundness := by
     circuit_proof_start [main, isBit, sub, add, Add.carry0, Add.carry1, RowSpec, dword, Alu.channel,
@@ -161,7 +161,7 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
       simp only [eqBit] <;>
       split_ifs <;> (try norm_num) <;> omega
     refine ⟨fun _ => key, by simp, by simp, by simp, by simp, by simp, ?_⟩
-    intro _ _ ha0 ha1 hb0 hb1
+    intro _ ha0 ha1 hb0 hb1
     -- 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)
diff --git a/formal/LambdaVM/Tables/Lt.lean b/formal/LambdaVM/Tables/Lt.lean
index bbcfbfebe..89de939f8 100644
--- a/formal/LambdaVM/Tables/Lt.lean
+++ b/formal/LambdaVM/Tables/Lt.lean
@@ -175,9 +175,8 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
     constructor
     · intro channel h; tauto
     · intro env h
-      refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;>
-      · intro hne1 hne0
-        exact (requirement_vacuous h.1 hne1 hne0).elim
+      -- each pull owes a multiplicity of 0 or 1: μ is a bit
+      exact mul_one_sub_eq_zero_iff.mp h.1
 
   soundness := by
     circuit_proof_start [main, isBit, sub, add, Add.carry0, Add.carry1, RowSpec, Row.lhsVal, Row.rhsVal,
@@ -258,7 +257,7 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
       | (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, ?_⟩
-    intro _ _ hl0 hlhi hr0 hrhi
+    intro _ hl0 hlhi hr0 hrhi
     -- the flag byte, read as a natural
     have hflagsV : (4 + 32 * input_signed + 64 * input_invert : F p).val
         = 4 + 32 * input_signed.val + 64 * input_invert.val :=
diff --git a/formal/LambdaVM/Tables/Shift.lean b/formal/LambdaVM/Tables/Shift.lean
index 9e1f2d8d3..16130b8bd 100644
--- a/formal/LambdaVM/Tables/Shift.lean
+++ b/formal/LambdaVM/Tables/Shift.lean
@@ -297,14 +297,16 @@ theorem soundness :
     rcases hmb with hmu0 | hmu1
     · -- μ = 0: nothing is required of the row
       rw [hmu0] at hleft ⊢
-      refine ⟨fun h => absurd h (by norm_num), ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_,
-        ?_, ?_⟩
+      -- each pull owes a multiplicity of 0 or 1, and the inactive push owes nothing
+      constructorm* _ ∧ _
       all_goals first
-        | exact req_vacuous hsb
-        | exact req_vacuous hleft
-        | exact req_vacuous hdb
-        | exact req_vacuous hzb'
-        | (intro _ h0; exact absurd rfl h0)
+        | exact hsb
+        | exact hleft
+        | exact hdb
+        | exact hzb'
+        | (left; rfl)
+        | (intro h; exact absurd rfl h)
+        | (intro h; exact absurd h (by norm_num))
     subst hmu1
     -- the facts every active row has
     have hd2 := IsBool.val_lt_two hdb
@@ -491,16 +493,18 @@ theorem soundness :
       simp only [limbs]
       omega
     -- the row spec and the bus requirements
-    refine ⟨fun _ => key, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+    refine ⟨fun _ => key, ?_⟩
+    -- each pull owes a multiplicity of 0 or 1
+    constructorm* _ ∧ _
     all_goals first
-      | exact req_vacuous hsb
-      | exact req_vacuous hleft
-      | exact req_vacuous hdb
-      | exact req_vacuous hzb'
-      | exact (fun h => absurd rfl h)
+      | exact hsb
+      | exact hleft
+      | exact hdb
+      | exact hzb'
+      | (right; rfl)
       | skip
     -- what remains is the ALU push
-    intro _ _ hin1lo hin1hi hin2lo hin2hi
+    intro _ hin1lo hin1hi hin2lo hin2hi
     -- the flag byte, read as a natural
     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 :=
@@ -662,20 +666,20 @@ theorem completeness :
         · rw [hs]; ring
       · -- MSB16[in[3]] when signed
         intro h
-        have hs1 : input_signed = 1 := neg_inj.mp h
+        have hs1 : input_signed = 1 := h
         rw [hs1, val_one_eq, if_pos rfl] at hn
         exact ⟨hi3, hn⟩
       · -- BYTE_ALU[AND, shift, 15] when left
         intro h
         have hd0 : input_direction = 0 := by
-          have := neg_inj.mp h
+          have := h
           linear_combination -this
         rw [hd0, ZMod.val_zero, if_pos rfl] at hb
         refine ⟨hsA, by rw [h15]; norm_num, Or.inl ?_⟩
         rw [h15, ShiftCore.and15, hb]
       · -- BYTE_ALU[AND, 256 − 16·zbs − shift, 15] when right
         intro h
-        have hd1 : input_direction = 1 := neg_inj.mp h
+        have hd1 : input_direction = 1 := h
         rw [hd1, val_one_eq, if_neg one_ne_zero] at hb
         rcases hzb with hz | hz
         · have hbne : input_bitShift.val ≠ 0 := fun h0 => by
@@ -788,8 +792,8 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
       have hsb := mul_one_sub_eq_zero_iff.mp h_sg
       have hzb := mul_one_sub_eq_zero_iff.mp h_zbs
       have hmb := mul_one_sub_eq_zero_iff.mp h_mu
+      -- each pull owes a multiplicity of 0 or 1
       constructorm* _ ∧ _ <;>
-      · intro h1 h0
         rcases hmb with hm | hm <;> rcases hdb with hd | hd <;> rcases hzb with hz | hz <;>
           rcases hsb with hs | hs <;> simp_all
 
diff --git a/formal/LambdaVM/Templates/IsByte.lean b/formal/LambdaVM/Templates/IsByte.lean
index fc710391e..4e645223e 100644
--- a/formal/LambdaVM/Templates/IsByte.lean
+++ b/formal/LambdaVM/Templates/IsByte.lean
@@ -70,7 +70,10 @@ def circuit : FormalAssertion (F p) Inputs where
   requirementsChannelsLawful input_var i₀ := by
     obtain ⟨cond, x⟩ := input_var
     simp only [circuit_norm, isByte, isBit, areBytesTable]
-    grind
+    intro _ h
+    rcases mul_eq_zero.mp h with h0 | h1
+    · exact Or.inl h0
+    · exact Or.inr (sub_eq_zero.mp h1).symm
 
   soundness := by
     circuit_proof_start [isByte, isBit, areBytesTable]
diff --git a/formal/export/eq.json b/formal/export/eq.json
index cc2edcd8d..7a6ec8d5b 100644
--- a/formal/export/eq.json
+++ b/formal/export/eq.json
@@ -1,31 +1,23 @@
 {"operations":
  [{"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 11},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 11},
     "message": [{"type": "var", "index": 6}],
+    "direction": "pull",
     "channel": "IS_HALF"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 11},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 11},
     "message": [{"type": "var", "index": 7}],
+    "direction": "pull",
     "channel": "IS_HALF"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 11},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 11},
     "message": [{"type": "var", "index": 8}],
+    "direction": "pull",
     "channel": "IS_HALF"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 11},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 11},
     "message": [{"type": "var", "index": 9}],
+    "direction": "pull",
     "channel": "IS_HALF"}},
   {"assert":
    {"type": "mul",
@@ -172,10 +164,7 @@
          "lhs": {"type": "var", "index": 8}},
         "lhs": {"type": "var", "index": 3}}}}}}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 11},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 11},
     "message":
     [{"type": "add",
       "rhs": {"type": "var", "index": 9},
@@ -185,6 +174,7 @@
        "lhs":
        {"type": "add", "rhs": {"type": "var", "index": 7}, "lhs": {"type": "var", "index": 6}}}},
      {"type": "var", "index": 10}],
+    "direction": "pull",
     "channel": "ZERO"}},
   {"assert":
    {"type": "add",
@@ -229,6 +219,7 @@
       "lhs": {"value": 3, "type": "const"}},
      {"type": "var", "index": 5},
      {"value": 0, "type": "const"}],
+    "direction": "push",
     "channel": "ALU"}}],
  "name": "eq",
  "columns": 12}
\ No newline at end of file
diff --git a/formal/export/lt.json b/formal/export/lt.json
index 583ebc861..800c9d42d 100644
--- a/formal/export/lt.json
+++ b/formal/export/lt.json
@@ -10,18 +10,14 @@
      "lhs": {"value": 1, "type": "const"}},
     "lhs": {"type": "var", "index": 16}}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 16},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 16},
     "message": [{"type": "var", "index": 1}],
+    "direction": "pull",
     "channel": "IS_HALF"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 16},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 16},
     "message": [{"type": "var", "index": 4}],
+    "direction": "pull",
     "channel": "IS_HALF"}},
   {"assert":
    {"type": "mul",
@@ -44,18 +40,14 @@
      "lhs": {"value": 1, "type": "const"}},
     "lhs": {"type": "var", "index": 14}}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 16},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 16},
     "message": [{"type": "var", "index": 2}, {"type": "var", "index": 12}],
+    "direction": "pull",
     "channel": "MSB16"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 16},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 16},
     "message": [{"type": "var", "index": 5}, {"type": "var", "index": 13}],
+    "direction": "pull",
     "channel": "MSB16"}},
   {"assert":
    {"type": "add",
@@ -438,32 +430,24 @@
           "lhs": {"value": 65536, "type": "const"}},
          "lhs": {"type": "var", "index": 4}}}}}}}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 16},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 16},
     "message": [{"type": "var", "index": 8}],
+    "direction": "pull",
     "channel": "IS_HALF"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 16},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 16},
     "message": [{"type": "var", "index": 9}],
+    "direction": "pull",
     "channel": "IS_HALF"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 16},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 16},
     "message": [{"type": "var", "index": 10}],
+    "direction": "pull",
     "channel": "IS_HALF"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 16},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 16},
     "message": [{"type": "var", "index": 11}],
+    "direction": "pull",
     "channel": "IS_HALF"}},
   {"interact":
    {"multiplicity": {"type": "var", "index": 16},
@@ -488,6 +472,7 @@
        "lhs": {"value": 4, "type": "const"}}},
      {"type": "var", "index": 15},
      {"value": 0, "type": "const"}],
+    "direction": "push",
     "channel": "ALU"}}],
  "name": "lt",
  "columns": 17}
\ No newline at end of file
diff --git a/formal/export/shift.json b/formal/export/shift.json
index 0ff43f48d..13f556ca7 100644
--- a/formal/export/shift.json
+++ b/formal/export/shift.json
@@ -618,34 +618,27 @@
       "lhs": {"value": 18446744069414584320, "type": "const"}},
      "lhs": {"value": 1, "type": "const"}}}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 6},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 6},
     "message": [{"type": "var", "index": 3}, {"type": "var", "index": 10}],
+    "direction": "pull",
     "channel": "MSB16"}},
   {"interact":
    {"multiplicity":
-    {"type": "mul",
+    {"type": "add",
      "rhs":
-     {"type": "add",
-      "rhs":
-      {"type": "mul",
-       "rhs": {"type": "var", "index": 5},
-       "lhs": {"value": 18446744069414584320, "type": "const"}},
-      "lhs": {"type": "var", "index": 25}},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+     {"type": "mul",
+      "rhs": {"type": "var", "index": 5},
+      "lhs": {"value": 18446744069414584320, "type": "const"}},
+     "lhs": {"type": "var", "index": 25}},
     "message":
     [{"value": 0, "type": "const"},
      {"type": "var", "index": 4},
      {"value": 15, "type": "const"},
      {"type": "var", "index": 11}],
+    "direction": "pull",
     "channel": "BYTE_ALU"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 5},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 5},
     "message":
     [{"value": 0, "type": "const"},
      {"type": "add",
@@ -663,93 +656,81 @@
        "lhs": {"value": 256, "type": "const"}}},
      {"value": 15, "type": "const"},
      {"type": "var", "index": 11}],
+    "direction": "pull",
     "channel": "BYTE_ALU"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 25},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 25},
     "message": [{"type": "var", "index": 11}, {"type": "var", "index": 12}],
+    "direction": "pull",
     "channel": "ZERO"}},
   {"interact":
    {"multiplicity":
-    {"type": "mul",
+    {"type": "add",
      "rhs":
-     {"type": "add",
-      "rhs":
-      {"type": "mul",
-       "rhs": {"type": "var", "index": 12},
-       "lhs": {"value": 18446744069414584320, "type": "const"}},
-      "lhs": {"value": 1, "type": "const"}},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+     {"type": "mul",
+      "rhs": {"type": "var", "index": 12},
+      "lhs": {"value": 18446744069414584320, "type": "const"}},
+     "lhs": {"value": 1, "type": "const"}},
     "message":
     [{"type": "var", "index": 0},
      {"type": "var", "index": 11},
      {"type": "var", "index": 13},
      {"type": "var", "index": 18}],
+    "direction": "pull",
     "channel": "HWSL"}},
   {"interact":
    {"multiplicity":
-    {"type": "mul",
+    {"type": "add",
      "rhs":
-     {"type": "add",
-      "rhs":
-      {"type": "mul",
-       "rhs": {"type": "var", "index": 12},
-       "lhs": {"value": 18446744069414584320, "type": "const"}},
-      "lhs": {"value": 1, "type": "const"}},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+     {"type": "mul",
+      "rhs": {"type": "var", "index": 12},
+      "lhs": {"value": 18446744069414584320, "type": "const"}},
+     "lhs": {"value": 1, "type": "const"}},
     "message":
     [{"type": "var", "index": 1},
      {"type": "var", "index": 11},
      {"type": "var", "index": 14},
      {"type": "var", "index": 19}],
+    "direction": "pull",
     "channel": "HWSL"}},
   {"interact":
    {"multiplicity":
-    {"type": "mul",
+    {"type": "add",
      "rhs":
-     {"type": "add",
-      "rhs":
-      {"type": "mul",
-       "rhs": {"type": "var", "index": 12},
-       "lhs": {"value": 18446744069414584320, "type": "const"}},
-      "lhs": {"value": 1, "type": "const"}},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+     {"type": "mul",
+      "rhs": {"type": "var", "index": 12},
+      "lhs": {"value": 18446744069414584320, "type": "const"}},
+     "lhs": {"value": 1, "type": "const"}},
     "message":
     [{"type": "var", "index": 2},
      {"type": "var", "index": 11},
      {"type": "var", "index": 15},
      {"type": "var", "index": 20}],
+    "direction": "pull",
     "channel": "HWSL"}},
   {"interact":
    {"multiplicity":
-    {"type": "mul",
+    {"type": "add",
      "rhs":
-     {"type": "add",
-      "rhs":
-      {"type": "mul",
-       "rhs": {"type": "var", "index": 12},
-       "lhs": {"value": 18446744069414584320, "type": "const"}},
-      "lhs": {"value": 1, "type": "const"}},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+     {"type": "mul",
+      "rhs": {"type": "var", "index": 12},
+      "lhs": {"value": 18446744069414584320, "type": "const"}},
+     "lhs": {"value": 1, "type": "const"}},
     "message":
     [{"type": "var", "index": 3},
      {"type": "var", "index": 11},
      {"type": "var", "index": 16},
      {"type": "var", "index": 21}],
+    "direction": "pull",
     "channel": "HWSL"}},
   {"interact":
    {"multiplicity":
-    {"type": "mul",
+    {"type": "add",
      "rhs":
-     {"type": "add",
-      "rhs":
-      {"type": "mul",
-       "rhs": {"type": "var", "index": 12},
-       "lhs": {"value": 18446744069414584320, "type": "const"}},
-      "lhs": {"value": 1, "type": "const"}},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+     {"type": "mul",
+      "rhs": {"type": "var", "index": 12},
+      "lhs": {"value": 18446744069414584320, "type": "const"}},
+     "lhs": {"value": 1, "type": "const"}},
     "message":
     [{"type": "mul", "rhs": {"type": "var", "index": 10}, "lhs": {"value": 65535, "type": "const"}},
      {"type": "var", "index": 11},
@@ -763,12 +744,10 @@
       {"type": "mul",
        "rhs": {"type": "var", "index": 10},
        "lhs": {"value": 65535, "type": "const"}}}],
+    "direction": "pull",
     "channel": "HWSL"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 25},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 25},
     "message":
     [{"value": 0, "type": "const"},
      {"type": "var", "index": 4},
@@ -802,6 +781,7 @@
           "lhs": {"value": 48, "type": "const"}},
          "lhs": {"value": 18446744069414584320, "type": "const"}},
         "lhs": {"value": 48, "type": "const"}}}}],
+    "direction": "pull",
     "channel": "BYTE_ALU"}},
   {"interact":
    {"multiplicity": {"type": "var", "index": 25},
@@ -836,48 +816,37 @@
        {"type": "add", "rhs": {"type": "var", "index": 7}, "lhs": {"value": 5, "type": "const"}}}},
      {"type": "var", "index": 8},
      {"type": "var", "index": 9}],
+    "direction": "push",
     "channel": "ALU"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"value": 1, "type": "const"},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"value": 1, "type": "const"},
     "message": [{"type": "var", "index": 4}, {"type": "var", "index": 26}],
+    "direction": "pull",
     "channel": "ARE_BYTES"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 25},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 25},
     "message": [{"type": "var", "index": 27}],
+    "direction": "pull",
     "channel": "IS_HALF"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 25},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 25},
     "message": [{"type": "var", "index": 0}],
+    "direction": "pull",
     "channel": "IS_HALF"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 25},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 25},
     "message": [{"type": "var", "index": 1}],
+    "direction": "pull",
     "channel": "IS_HALF"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 25},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 25},
     "message": [{"type": "var", "index": 2}],
+    "direction": "pull",
     "channel": "IS_HALF"}},
   {"interact":
-   {"multiplicity":
-    {"type": "mul",
-     "rhs": {"type": "var", "index": 25},
-     "lhs": {"value": 18446744069414584320, "type": "const"}},
+   {"multiplicity": {"type": "var", "index": 25},
     "message": [{"type": "var", "index": 3}],
+    "direction": "pull",
     "channel": "IS_HALF"}}],
  "name": "shift",
  "columns": 29}
\ No newline at end of file
diff --git a/formal/lake-manifest.json b/formal/lake-manifest.json
index 88c14c478..ca5842997 100644
--- a/formal/lake-manifest.json
+++ b/formal/lake-manifest.json
@@ -1,41 +1,41 @@
-{"version": "1.2.0",
+{"version": "1.3.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/Verified-zkEVM/clean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "1a6c28426372bb99af79e533aa7b9a0788eff0d7",
+   "rev": "f3abad7c099e49f847836c1883dd9e7c539f06f9",
    "name": "Clean",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "1a6c28426372bb99af79e533aa7b9a0788eff0d7",
+   "inputRev": "f3abad7c099e49f847836c1883dd9e7c539f06f9",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/Verified-zkEVM/CompPoly.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a09455a22fea4623a2a1c5b363cf6efc61486a83",
+   "rev": "06686e4c70939af82203af21516f8ab8a21a8051",
    "name": "CompPoly",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.1",
+   "inputRev": "v4.35.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0df444a360eaa60ab8c11dca51a86af692955474",
+   "rev": "56a005855ea17e0b0958f73ec801ae140b0a1679",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.1",
+   "inputRev": "v4.35.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
+   "rev": "dfa4f38190d07c37e315953e08b90fe2d95b3c24",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
+   "rev": "d6b4c7be5be75ec4917c873ac50c756dc1436372",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "16f02aa7642864af59f1ff0e384a015994db9118",
+   "rev": "a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
+   "rev": "df72b022e558978a1c50264cfc4d7fec86fa8e04",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
+   "rev": "4a174c490d8707121c4a9290800489f105d85e07",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
+   "rev": "dce0ad79c486cb1fb504af04f953c3466b0c6db8",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
+   "rev": "66e469188fe07963e5cf666c7d4433f45b8131c5",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,10 +105,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
+   "rev": "c24fe6078c630e89b489bffe59b3e20ac30d12c8",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0",
+   "inputRev": "v4.35.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "«lambda-vm-formal»",
diff --git a/formal/lakefile.toml b/formal/lakefile.toml
index 5401f2b70..8c801fdea 100644
--- a/formal/lakefile.toml
+++ b/formal/lakefile.toml
@@ -9,7 +9,7 @@ relaxedAutoImplicit = false
 [[require]]
 name = "Clean"
 git = "https://github.com/Verified-zkEVM/clean"
-rev = "1a6c28426372bb99af79e533aa7b9a0788eff0d7"
+rev = "f3abad7c099e49f847836c1883dd9e7c539f06f9"
 
 [[lean_lib]]
 name = "LambdaVM"
diff --git a/formal/lean-toolchain b/formal/lean-toolchain
index a8afa7d1b..a6aff065d 100644
--- a/formal/lean-toolchain
+++ b/formal/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.33.1
+leanprover/lean4:v4.35.0
diff --git a/prover/src/tests/lean_diff.rs b/prover/src/tests/lean_diff.rs
index 5d44d0948..fd689c413 100644
--- a/prover/src/tests/lean_diff.rs
+++ b/prover/src/tests/lean_diff.rs
@@ -63,6 +63,8 @@ fn eval(e: &Expr, row: &[FE]) -> FE {
 
 struct LeanInteract {
     channel: String,
+    /// Clean's direction: a pull takes the message from the channel, a push adds it.
+    pull: bool,
     mult: Expr,
     msg: Vec<Expr>,
 }
@@ -89,6 +91,11 @@ fn load_lean(name: &str) -> LeanCircuit {
         } else if let Some(i) = op.get("interact") {
             interacts.push(LeanInteract {
                 channel: i["channel"].as_str().expect("channel").to_string(),
+                pull: match i["direction"].as_str().expect("direction") {
+                    "pull" => true,
+                    "push" => false,
+                    other => panic!("unknown direction {other}"),
+                },
                 mult: parse_expr(&i["multiplicity"]),
                 msg: i["message"]
                     .as_array()
@@ -129,8 +136,9 @@ fn bus_id_of(channel: &str) -> u64 {
 // =============================================================================
 
 /// `(bus id, signed multiplicity, bus elements)` of a Rust interaction on a row. A sender
-/// adds `+m`, a receiver `−m`; Clean's pull is `−e` and push `+e`, so the signs agree once a
-/// receiver (the table that answers the lookup, Clean's push) keeps its multiplicity.
+/// adds `+m`, a receiver `−m`; Clean's pull of multiplicity `e` counts `−e` and its push `+e`,
+/// so the signs agree once a receiver (the table that answers the lookup, Clean's push) keeps
+/// its multiplicity.
 fn rust_interaction_at(i: &BusInteraction, row: &[FE]) -> (u64, FE, Vec<FE>) {
     let m = i.multiplicity.evaluate_with(|c| row[c]);
     let m = if i.is_sender { -m } else { m };
@@ -143,9 +151,10 @@ fn rust_interaction_at(i: &BusInteraction, row: &[FE]) -> (u64, FE, Vec<FE>) {
 }
 
 fn lean_interaction_at(i: &LeanInteract, row: &[FE]) -> (u64, FE, Vec<FE>) {
+    let m = eval(&i.mult, row);
     (
         bus_id_of(&i.channel),
-        eval(&i.mult, row),
+        if i.pull { -m } else { m },
         i.msg.iter().map(|e| eval(e, row)).collect(),
     )
 }

From 48fd9e74f1903d2012f5db6ee1fea74502a72a8f Mon Sep 17 00:00:00 2001
From: jotabulacios <jbulacios@fi.uba.ar>
Date: Mon, 2 Nov 2026 14:53:54 -0300
Subject: [PATCH 2/6] Rename the if/dif lemmas that Lean v4.35.0 deprecates,
 and drop a skip fallback the linter flags.

if_true, if_false, if_pos, if_neg, dif_pos and dif_neg become ite_true, ite_false, ite_eq_left,
ite_eq_right, dite_eq_left and dite_eq_right, as in Clean. In SHIFT, first | ... | skip becomes
try first | ..., which behaves the same. The build has no warnings left.
---
 formal/LambdaVM/Channels/Counted.lean |  6 +--
 formal/LambdaVM/Field.lean            |  4 +-
 formal/LambdaVM/Tables/Shift.lean     | 63 +++++++++++++--------------
 formal/LambdaVM/Tables/ShiftCore.lean | 16 +++----
 4 files changed, 44 insertions(+), 45 deletions(-)

diff --git a/formal/LambdaVM/Channels/Counted.lean b/formal/LambdaVM/Channels/Counted.lean
index d3c4c0981..85a826a16 100644
--- a/formal/LambdaVM/Channels/Counted.lean
+++ b/formal/LambdaVM/Channels/Counted.lean
@@ -112,19 +112,19 @@ lemma balanceOf_counted (N : ℕ) (msg : Array F) :
       · refine ⟨s, by omega, ?_, ?_⟩
         · have hsigned : i.signedMult = 0 := by
             cases hd : i.direction <;> simp [Interaction.signedMult, hd, h0]
-          rw [if_pos hm, hsigned, hb, zero_add]
+          rw [ite_eq_left hm, hsigned, hb, zero_add]
         · intro a ha' ham ha0
           rcases List.mem_cons.mp ha' with rfl | ha'
           · exact absurd h0 ha0
           · exact ha a ha' ham ha0
       · obtain ⟨hd, k, hk1, hkN, hk⟩ := h i (by simp) hm h0
         refine ⟨k + s, by omega, ?_, ?_⟩
-        · rw [if_pos hm, hb]
+        · rw [ite_eq_left hm, hb]
           simp only [Interaction.signedMult, hd, hk]
           push_cast; ring
         · intro a _ _ _; omega
     · refine ⟨s, by omega, ?_, ?_⟩
-      · rw [if_neg hm, hb, zero_add]
+      · rw [ite_eq_right hm, hb, zero_add]
       · intro a ha' ham ha0
         rcases List.mem_cons.mp ha' with rfl | ha'
         · exact absurd ham hm
diff --git a/formal/LambdaVM/Field.lean b/formal/LambdaVM/Field.lean
index ef5d4630d..68b42649c 100644
--- a/formal/LambdaVM/Field.lean
+++ b/formal/LambdaVM/Field.lean
@@ -108,7 +108,7 @@ lemma val_sub_of_val_lt {a b : ℕ} (ha : a < 2^40) (hb : b < 2^40)
       have := congrArg ZMod.val h0
       rw [val_natCast_of_lt_two_pow_40 (by omega), ZMod.val_zero] at this
       omega
-    rw [if_neg hne, val_natCast_of_lt_two_pow_40 (by omega)] at h
+    rw [ite_eq_right hne, val_natCast_of_lt_two_pow_40 (by omega)] at h
     have hp : 2^41 < p := by decide
     omega
 
@@ -125,7 +125,7 @@ lemma val_neg_two : (-2 : F p).val = p - 2 := by
     have := congrArg ZMod.val h
     rw [val_ofNat 2 (by norm_num), ZMod.val_zero] at this
     omega
-  rw [ZMod.neg_val, if_neg h2, val_ofNat 2 (by norm_num)]
+  rw [ZMod.neg_val, ite_eq_right h2, val_ofNat 2 (by norm_num)]
 
 /-- Three bits whose complement `1 − l0 − l1 − l2` is also a bit are at most one-hot. -/
 lemma onehot_of_isBool {l0 l1 l2 : F p} (h0 : IsBool l0) (h1 : IsBool l1) (h2 : IsBool l2)
diff --git a/formal/LambdaVM/Tables/Shift.lean b/formal/LambdaVM/Tables/Shift.lean
index 16130b8bd..644f70abf 100644
--- a/formal/LambdaVM/Tables/Shift.lean
+++ b/formal/LambdaVM/Tables/Shift.lean
@@ -241,14 +241,14 @@ lemma override_x {zbs x i d : F p} {b : ℕ} (hzb : IsBool zbs) (hdb : IsBool d)
     zbs * (x - i * (1 - d)) = 0 := by
   rcases hzb with hz | hz
   · rw [hz, zero_mul]
-  · rw [if_pos (hiff hz)] at hx
+  · rw [ite_eq_left (hiff hz)] at hx
     rw [hz, one_mul, sub_eq_zero]
     rcases hdb with hd | hd
     · rw [hd] at hx ⊢
-      simp only [ZMod.val_zero, if_true] at hx
+      simp only [ZMod.val_zero, ite_true] at hx
       rw [ZMod.val_injective _ hx]; ring
     · rw [hd] at hx ⊢
-      simp only [val_one_eq, one_ne_zero, if_false] at hx
+      simp only [val_one_eq, one_ne_zero, ite_false] at hx
       rw [(ZMod.val_eq_zero _).mp hx]; ring
 
 /-- The `zbs` override of a `Y` scratch cell holds on an honest row. -/
@@ -258,14 +258,14 @@ lemma override_y {zbs y i d : F p} {b : ℕ} (hzb : IsBool zbs) (hdb : IsBool d)
     zbs * (y - i * d) = 0 := by
   rcases hzb with hz | hz
   · rw [hz, zero_mul]
-  · rw [if_pos (hiff hz)] at hy
+  · rw [ite_eq_left (hiff hz)] at hy
     rw [hz, one_mul, sub_eq_zero]
     rcases hdb with hd | hd
     · rw [hd] at hy ⊢
-      simp only [ZMod.val_zero, if_true] at hy
+      simp only [ZMod.val_zero, ite_true] at hy
       rw [(ZMod.val_eq_zero _).mp hy]; ring
     · rw [hd] at hy ⊢
-      simp only [val_one_eq, one_ne_zero, if_false] at hy
+      simp only [val_one_eq, one_ne_zero, ite_false] at hy
       rw [ZMod.val_injective _ hy]; ring
 
 @[reducible]
@@ -333,19 +333,19 @@ theorem soundness :
     -- zbs is the zero flag of bit_shift
     have hzb_iff : input_zbs.val = 1 ↔ input_bitShift.val = 0 := by
       by_cases hb0 : input_bitShift = 0
-      · rw [hzbs_eq, if_pos hb0, val_one_eq, hb0, ZMod.val_zero]; simp
-      · rw [hzbs_eq, if_neg hb0, ZMod.val_zero]
+      · rw [hzbs_eq, ite_eq_left hb0, val_one_eq, hb0, ZMod.val_zero]; simp
+      · rw [hzbs_eq, ite_eq_right hb0, ZMod.val_zero]
         have : input_bitShift.val ≠ 0 := by rwa [Ne, ZMod.val_eq_zero]
         omega
     -- bit_shift from the BYTE_ALU lookups
     have hb : input_bitShift.val = if input_direction.val = 0 then input_shiftAmount.val % 16
         else (16 - input_shiftAmount.val % 16) % 16 := by
       rcases hdb with hd0 | hd1
-      · rw [hd0]; simp only [ZMod.val_zero, if_true]
+      · rw [hd0]; simp only [ZMod.val_zero, ite_true]
         obtain ⟨-, -, hand | ⟨h02, -⟩⟩ := h_balL (by rw [hd0]; norm_num)
         · rw [hand, h15, ShiftCore.and15]
         · exact absurd h02 h02ne
-      · rw [hd1]; simp only [val_one_eq, one_ne_zero, if_false]
+      · rw [hd1]; simp only [val_one_eq, one_ne_zero, ite_false]
         obtain ⟨hx, -, hand | ⟨h02, -⟩⟩ := h_balR (by rw [hd1])
         · rw [h15, ShiftCore.and15] at hand
           rw [← ZMod.natCast_zmod_val input_shiftAmount] at hx hand
@@ -366,10 +366,10 @@ theorem soundness :
     have hn : input_isNegative.val = if input_signed.val = 1 then input_in3.val / 32768 else 0 := by
       rcases hsb with hs0 | hs1
       · rw [hs0] at h_neg ⊢
-        simp only [ZMod.val_zero, zero_ne_one, if_false]
+        simp only [ZMod.val_zero, zero_ne_one, ite_false]
         have : input_isNegative = 0 := by simpa using h_neg
         rw [this, ZMod.val_zero]
-      · rw [hs1]; simp only [val_one_eq, if_true]
+      · rw [hs1]; simp only [val_one_eq, ite_true]
         exact (h_msb (by rw [hs1])).2
     have hn2 : input_isNegative.val < 2 := by rw [hn]; split_ifs <;> omega
     have hext : (65535 * input_isNegative).val = 65535 * input_isNegative.val :=
@@ -403,7 +403,7 @@ theorem soundness :
         obtain ⟨hi3', -, hx3v, hy3v⟩ := h_hw3 (by rw [hz0]; norm_num)
         obtain ⟨hi4', -, hx4v, -⟩ := h_hw4 (by rw [hz0]; norm_num)
         rw [hext] at hx4v hi4'
-        simp only [if_neg hbne]
+        simp only [ite_eq_right hbne]
         exact ⟨sll_of_eq hi0' hx0v, sll_of_eq hi1' hx1v, sll_of_eq hi2' hx2v, sll_of_eq hi3' hx3v,
           sll_of_eq hi4' hx4v, sllc_of_eq hi0' hy0v, sllc_of_eq hi1' hy1v, sllc_of_eq hi2' hy2v,
           sllc_of_eq hi3' hy3v⟩
@@ -411,15 +411,15 @@ theorem soundness :
         have hb0 : input_bitShift.val = 0 := hzb_iff.mp (by rw [hz1, val_one_eq])
         rw [hz1] at h_zx0 h_zx1 h_zx2 h_zx3 h_zx4 h_zy0 h_zy1 h_zy2 h_zy3
         simp only [one_mul, sub_eq_zero] at h_zx0 h_zx1 h_zx2 h_zx3 h_zx4 h_zy0 h_zy1 h_zy2 h_zy3
-        simp only [if_pos hb0]
+        simp only [ite_eq_left hb0]
         rcases hdb with hd0 | hd1
         · rw [hd0] at h_zx0 h_zx1 h_zx2 h_zx3 h_zy0 h_zy1 h_zy2 h_zy3 ⊢
           simp only [sub_zero, mul_one, mul_zero] at h_zx0 h_zx1 h_zx2 h_zx3 h_zy0 h_zy1 h_zy2 h_zy3
-          simp only [ZMod.val_zero, if_true, h_zx0, h_zx1, h_zx2, h_zx3, h_zy0, h_zy1, h_zy2, h_zy3,
+          simp only [ZMod.val_zero, ite_true, h_zx0, h_zx1, h_zx2, h_zx3, h_zy0, h_zy1, h_zy2, h_zy3,
             h_zx4, and_self]
         · rw [hd1] at h_zx0 h_zx1 h_zx2 h_zx3 h_zy0 h_zy1 h_zy2 h_zy3 ⊢
           simp only [sub_self, mul_one, mul_zero] at h_zx0 h_zx1 h_zx2 h_zx3 h_zy0 h_zy1 h_zy2 h_zy3
-          simp only [val_one_eq, one_ne_zero, if_false, h_zx0, h_zx1, h_zx2, h_zx3, h_zy0, h_zy1,
+          simp only [val_one_eq, one_ne_zero, ite_false, h_zx0, h_zx1, h_zx2, h_zx3, h_zy0, h_zy1,
             h_zy2, h_zy3, h_zx4, ZMod.val_zero, and_self]
     obtain ⟨hx0, hx1, hx2, hx3, hx4, hy0, hy1, hy2, hy3⟩ := hxy
     -- the one-hot limb index from the BYTE_ALU lookup
@@ -496,13 +496,12 @@ theorem soundness :
     refine ⟨fun _ => key, ?_⟩
     -- each pull owes a multiplicity of 0 or 1
     constructorm* _ ∧ _
-    all_goals first
+    all_goals try first
       | exact hsb
       | exact hleft
       | exact hdb
       | exact hzb'
       | (right; rfl)
-      | skip
     -- what remains is the ALU push
     intro _ hin1lo hin1hi hin2lo hin2hi
     -- the flag byte, read as a natural
@@ -570,8 +569,8 @@ theorem completeness :
       have hzb_iff : input_zbs = 1 ↔ input_bitShift.val = 0 := by
         rw [hzbs]
         by_cases hb0 : input_bitShift = 0
-        · rw [if_pos hb0, hb0, ZMod.val_zero]; simp
-        · rw [if_neg hb0]
+        · rw [ite_eq_left hb0, hb0, ZMod.val_zero]; simp
+        · rw [ite_eq_right hb0]
           have hne : input_bitShift.val ≠ 0 := by rwa [Ne, ZMod.val_eq_zero]
           constructor
           · intro h; exact absurd h zero_ne_one
@@ -642,7 +641,7 @@ theorem completeness :
       · -- zbs · X[4] = 0
         rcases hzb with hz | hz
         · rw [hz, zero_mul]
-        · rw [if_pos (hiff hz)] at hx4
+        · rw [ite_eq_left (hiff hz)] at hx4
           rw [hz, one_mul, (ZMod.val_eq_zero _).mp hx4]
       · -- out[0]
         rw [eval_shiftedPoly_1, eval_shiftedPoly_2]
@@ -661,29 +660,29 @@ theorem completeness :
       · -- (1 − signed) · is_negative = 0
         rcases hsb with hs | hs
         · rw [hs] at hn ⊢
-          simp only [ZMod.val_zero, zero_ne_one, if_false] at hn
+          simp only [ZMod.val_zero, zero_ne_one, ite_false] at hn
           rw [(ZMod.val_eq_zero _).mp hn]; ring
         · rw [hs]; ring
       · -- MSB16[in[3]] when signed
         intro h
         have hs1 : input_signed = 1 := h
-        rw [hs1, val_one_eq, if_pos rfl] at hn
+        rw [hs1, val_one_eq, ite_eq_left rfl] at hn
         exact ⟨hi3, hn⟩
       · -- BYTE_ALU[AND, shift, 15] when left
         intro h
         have hd0 : input_direction = 0 := by
           have := h
           linear_combination -this
-        rw [hd0, ZMod.val_zero, if_pos rfl] at hb
+        rw [hd0, ZMod.val_zero, ite_eq_left rfl] at hb
         refine ⟨hsA, by rw [h15]; norm_num, Or.inl ?_⟩
         rw [h15, ShiftCore.and15, hb]
       · -- BYTE_ALU[AND, 256 − 16·zbs − shift, 15] when right
         intro h
         have hd1 : input_direction = 1 := h
-        rw [hd1, val_one_eq, if_neg one_ne_zero] at hb
+        rw [hd1, val_one_eq, ite_eq_right one_ne_zero] at hb
         rcases hzb with hz | hz
         · have hbne : input_bitShift.val ≠ 0 := fun h0 => by
-            rw [hzbs, if_pos ((ZMod.val_eq_zero _).mp h0)] at hz; exact one_ne_zero hz
+            rw [hzbs, ite_eq_left ((ZMod.val_eq_zero _).mp h0)] at hz; exact one_ne_zero hz
           have hs1 : 1 ≤ input_shiftAmount.val := by omega
           have hcast : (256 : F p) - 16 * input_zbs - input_shiftAmount
               = ((256 - input_shiftAmount.val : ℕ) : F p) := by
@@ -704,32 +703,32 @@ theorem completeness :
         have hbne : input_bitShift.val ≠ 0 := fun h0 => by
           have := hzb_iff.mpr h0
           rw [this] at h; norm_num at h
-        rw [if_neg hbne] at hx0 hy0
+        rw [ite_eq_right hbne] at hx0 hy0
         exact ⟨hi0, hb16, by rw [hx0]; exact sll_eq hi0, by rw [hy0]; exact sllc_eq hi0⟩
       · intro h
         have hbne : input_bitShift.val ≠ 0 := fun h0 => by
           have := hzb_iff.mpr h0
           rw [this] at h; norm_num at h
-        rw [if_neg hbne] at hx1 hy1
+        rw [ite_eq_right hbne] at hx1 hy1
         exact ⟨hi1, hb16, by rw [hx1]; exact sll_eq hi1, by rw [hy1]; exact sllc_eq hi1⟩
       · intro h
         have hbne : input_bitShift.val ≠ 0 := fun h0 => by
           have := hzb_iff.mpr h0
           rw [this] at h; norm_num at h
-        rw [if_neg hbne] at hx2 hy2
+        rw [ite_eq_right hbne] at hx2 hy2
         exact ⟨hi2, hb16, by rw [hx2]; exact sll_eq hi2, by rw [hy2]; exact sllc_eq hi2⟩
       · intro h
         have hbne : input_bitShift.val ≠ 0 := fun h0 => by
           have := hzb_iff.mpr h0
           rw [this] at h; norm_num at h
-        rw [if_neg hbne] at hx3 hy3
+        rw [ite_eq_right hbne] at hx3 hy3
         exact ⟨hi3, hb16, by rw [hx3]; exact sll_eq hi3, by rw [hy3]; exact sllc_eq hi3⟩
       · -- HWSL[extension, bit_shift]
         intro h
         have hbne : input_bitShift.val ≠ 0 := fun h0 => by
           have := hzb_iff.mpr h0
           rw [this] at h; norm_num at h
-        rw [if_neg hbne] at hx4
+        rw [ite_eq_right hbne] at hx4
         have he : 65535 * input_isNegative.val = 0 ∨ 65535 * input_isNegative.val = 65535 := by omega
         obtain ⟨hle, hsub⟩ := ext_sllc he hb16
         have hdiff : (65535 * input_isNegative - input_x4).val
@@ -738,7 +737,7 @@ theorem completeness :
           rw [show (65535 : F p) * input_isNegative - input_x4
               = ((65535 * input_isNegative.val - input_x4.val : ℕ) : F p) by
             rw [Nat.cast_sub hle]; push_cast
-            rw [ZMod.natCast_zmod_val input_isNegative, ZMod.natCast_zmod_val input_x4]; try ring]
+            rw [ZMod.natCast_zmod_val input_isNegative, ZMod.natCast_zmod_val input_x4]]
           exact val_natCast_of_lt_two_pow_40 (by omega)
         refine ⟨by rw [hext]; omega, hb16, ?_, ?_⟩
         · rw [hext, hx4]; exact sll_eq (by omega)
diff --git a/formal/LambdaVM/Tables/ShiftCore.lean b/formal/LambdaVM/Tables/ShiftCore.lean
index 9eba419f5..d6c0c07d7 100644
--- a/formal/LambdaVM/Tables/ShiftCore.lean
+++ b/formal/LambdaVM/Tables/ShiftCore.lean
@@ -145,7 +145,7 @@ theorem main {d sg w s i0 i1 i2 i3 l0 l1 l2 b n x0 x1 x2 x3 x4 y0 y1 y2 y3 : ℕ
   have hX : limbs i0 i1 i2 i3 < 2^64 := by unfold limbs; omega
   rcases (by omega : d = 0 ∨ d = 1) with rfl | rfl
   · -- left shift: `shifted` is the if-form of `leftShift` with `L` the one-hot index
-    simp only [if_true] at hb
+    simp only [ite_true] at hb
     subst hb
     have hb16 : s % 16 < 16 := Nat.mod_lt _ (by norm_num)
     have core := leftShift h0 h1 h2 h3 hb16 (L := l1 + 2 * l2 + 3 * (1 - l0 - l1 - l2)) (by omega)
@@ -158,14 +158,14 @@ theorem main {d sg w s i0 i1 i2 i3 l0 l1 l2 b n x0 x1 x2 x3 x4 y0 y1 y2 y3 : ℕ
       ⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩ <;>
     · simp only [shifted, sh, hx0, hx1, hx2, hx3, hx4, hy0, hy1, hy2, hy3]
       norm_num at core hLv ⊢
-      simp only [shiftResult, if_true]
+      simp only [shiftResult, ite_true]
       rw [hk, hLv]
       norm_num at core ⊢
       by_cases hz : s % 16 = 0
       · simpa [sll, sllc, hz] using core
       · simpa [sll, sllc, hz] using core
   · -- right shift: phase 1, phase 2, and their composition
-    simp only [one_ne_zero, if_false] at hb
+    simp only [one_ne_zero, ite_false] at hb
     have hr : s % 16 < 16 := Nat.mod_lt _ (by norm_num)
     have p1 := rightIntra h0 h1 h2 h3 hr hb he
     simp only at p1
@@ -180,22 +180,22 @@ theorem main {d sg w s i0 i1 i2 i3 l0 l1 l2 b n x0 x1 x2 x3 x4 y0 y1 y2 y3 : ℕ
     have hres : shiftResult w sg 1 (limbs i0 i1 i2 i3) s
         = ((limbs i0 i1 i2 i3 + 65535 * n * (2^64 + 2^80 + 2^96 + 2^112))
             >>> (16 * (s / 16 % (4 - 2 * w)) + s % 16)) % 2^64 := by
-      simp only [shiftResult, one_ne_zero, if_false]
+      simp only [shiftResult, one_ne_zero, ite_false]
       rw [hk]
       have hX63 : limbs i0 i1 i2 i3 < 2^63 ↔ i3 < 32768 := by unfold limbs; omega
       rcases (by omega : sg = 0 ∨ sg = 1) with rfl | rfl
-      · simp only [if_true, zero_ne_one, if_false] at hn ⊢
+      · simp only [ite_true, zero_ne_one, ite_false] at hn ⊢
         subst hn
         simp only [mul_zero, zero_mul, add_zero]
         rw [Nat.mod_eq_of_lt (lt_of_le_of_lt (Nat.shiftRight_le _ _) hX)]
-      · simp only [if_true, one_ne_zero, if_false] at hn ⊢
+      · simp only [ite_true, one_ne_zero, ite_false] at hn ⊢
         subst hn
         rcases (by omega : i3 / 32768 = 0 ∨ i3 / 32768 = 1) with h | h
         · have hlt : limbs i0 i1 i2 i3 < 2^63 := hX63.mpr (by omega)
-          rw [h]; simp only [mul_zero, zero_mul, add_zero, sra64, if_pos hlt]
+          rw [h]; simp only [mul_zero, zero_mul, add_zero, sra64, ite_eq_left hlt]
           rw [Nat.mod_eq_of_lt (lt_of_le_of_lt (Nat.shiftRight_le _ _) hX)]
         · have hge : ¬ limbs i0 i1 i2 i3 < 2^63 := by rw [hX63]; omega
-          rw [h]; simp only [sra64, if_neg hge]
+          rw [h]; simp only [sra64, ite_eq_right hge]
           norm_num
     rw [hres]
     have hLv : s / 16 % (4 - 2 * w) = l1 + 2 * l2 + 3 * (1 - l0 - l1 - l2) := by omega

From 194d06e1eb1138dae8a34851923eaf9081a95107 Mon Sep 17 00:00:00 2001
From: jotabulacios <jbulacios@fi.uba.ar>
Date: Tue, 3 Nov 2026 11:30:27 -0300
Subject: [PATCH 3/6] =?UTF-8?q?Remove=20req=5Fvacuous=20and=20requirement?=
 =?UTF-8?q?=5Fvacuous,=20which=20no=20proof=20uses=20since=20the=20bump,?=
 =?UTF-8?q?=20and=20the=20renames=20left=20in=20SHIFT's=20completeness=20p?=
 =?UTF-8?q?roof.=20Both=20lemmas=20discharged=20a=20pull=20requirement=20s?=
 =?UTF-8?q?tated=20with=20the=20old=20multiplicity=20-1=20(`=C2=AC=20-e=20?=
 =?UTF-8?q?=3D=20-1=20=E2=86=92=20=C2=AC=20e=20=3D=200=20=E2=86=92=20P`),?=
 =?UTF-8?q?=20which=20the=20directed=20interactions=20no=20longer=20produc?=
 =?UTF-8?q?e.=20In=20SHIFT,=20the=20hypotheses=20that=20needed=20neg=5Finj?=
 =?UTF-8?q?.mp=20to=20go=20from=20`-x=20=3D=20-1`=20to=20`x=20=3D=201`=20n?=
 =?UTF-8?q?ow=20arrive=20as=20`x=20=3D=201`,=20so=20they=20are=20introduce?=
 =?UTF-8?q?d=20under=20their=20final=20names=20instead=20of=20being=20copi?=
 =?UTF-8?q?ed.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 formal/LambdaVM/Field.lean        | 15 ---------------
 formal/LambdaVM/Tables/Shift.lean | 10 +++-------
 2 files changed, 3 insertions(+), 22 deletions(-)

diff --git a/formal/LambdaVM/Field.lean b/formal/LambdaVM/Field.lean
index 68b42649c..2fd41f968 100644
--- a/formal/LambdaVM/Field.lean
+++ b/formal/LambdaVM/Field.lean
@@ -112,13 +112,6 @@ lemma val_sub_of_val_lt {a b : ℕ} (ha : a < 2^40) (hb : b < 2^40)
     have hp : 2^41 < p := by decide
     omega
 
-/-- A requirement `¬ -e = -1 → ¬ e = 0 → P` is vacuous for a boolean `e`. -/
-lemma req_vacuous {e : F p} (h : IsBool e) {P : Prop} : ¬ -e = -1 → ¬ e = 0 → P := by
-  intro h1 h0
-  rcases h with rfl | rfl
-  · exact absurd rfl h0
-  · exact absurd rfl h1
-
 lemma val_neg_two : (-2 : F p).val = p - 2 := by
   have h2 : (2 : F p) ≠ 0 := by
     intro h
@@ -142,12 +135,4 @@ lemma onehot_of_isBool {l0 l1 l2 : F p} (h0 : IsBool l0) (h1 : IsBool l1) (h2 :
 lemma eq_natCast_of_val {x : F p} {n : ℕ} (h : x.val = n) : x = (n : F p) := by
   rw [← h, ZMod.natCast_zmod_val]
 
-/-- A conditional interaction whose multiplicity is a bit (`μ·(1 − μ) = 0`) never has an
-active requirement. -/
-lemma requirement_vacuous {mu : F p} (h : mu * (1 - mu) = 0) (hne1 : ¬ -mu = -1) (hne0 : ¬ mu = 0) :
-    False := by
-  rcases mul_one_sub_eq_zero_iff.mp h with h0 | h1
-  · exact hne0 h0
-  · exact hne1 (by rw [h1])
-
 end LambdaVM
diff --git a/formal/LambdaVM/Tables/Shift.lean b/formal/LambdaVM/Tables/Shift.lean
index 644f70abf..3b9afedbf 100644
--- a/formal/LambdaVM/Tables/Shift.lean
+++ b/formal/LambdaVM/Tables/Shift.lean
@@ -664,21 +664,17 @@ theorem completeness :
           rw [(ZMod.val_eq_zero _).mp hn]; ring
         · rw [hs]; ring
       · -- MSB16[in[3]] when signed
-        intro h
-        have hs1 : input_signed = 1 := h
+        intro hs1
         rw [hs1, val_one_eq, ite_eq_left rfl] at hn
         exact ⟨hi3, hn⟩
       · -- BYTE_ALU[AND, shift, 15] when left
         intro h
-        have hd0 : input_direction = 0 := by
-          have := h
-          linear_combination -this
+        have hd0 : input_direction = 0 := by linear_combination -h
         rw [hd0, ZMod.val_zero, ite_eq_left rfl] at hb
         refine ⟨hsA, by rw [h15]; norm_num, Or.inl ?_⟩
         rw [h15, ShiftCore.and15, hb]
       · -- BYTE_ALU[AND, 256 − 16·zbs − shift, 15] when right
-        intro h
-        have hd1 : input_direction = 1 := h
+        intro hd1
         rw [hd1, val_one_eq, ite_eq_right one_ne_zero] at hb
         rcases hzb with hz | hz
         · have hbne : input_bitShift.val ≠ 0 := fun h0 => by

From bf586300d392c2c2f2596cec297f7e29d280303d Mon Sep 17 00:00:00 2001
From: jotabulacios <jbulacios@fi.uba.ar>
Date: Tue, 3 Nov 2026 15:12:28 -0300
Subject: [PATCH 4/6] =?UTF-8?q?Reword=20the=20doc=20comment=20of=20rust=5F?=
 =?UTF-8?q?interaction=5Fat=20in=20lean=5Fdiff.rs=20so=20it=20states=20the?=
 =?UTF-8?q?=20sign=20the=20comparison=20uses:=20a=20sender=20(Clean's=20pu?=
 =?UTF-8?q?ll)=20counts=20=E2=88=92m=20and=20a=20receiver=20(Clean's=20pus?=
 =?UTF-8?q?h)=20+m.=20The=20old=20first=20sentence=20described=20the=20pro?=
 =?UTF-8?q?ver's=20LogUp=20sum,=20where=20a=20sender=20adds=20+m,=20and=20?=
 =?UTF-8?q?read=20as=20if=20it=20contradicted=20the=20code=20below=20it.?=
 =?UTF-8?q?=20Comment=20only,=20no=20code=20change.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 prover/src/tests/lean_diff.rs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/prover/src/tests/lean_diff.rs b/prover/src/tests/lean_diff.rs
index fd689c413..cdabf95e8 100644
--- a/prover/src/tests/lean_diff.rs
+++ b/prover/src/tests/lean_diff.rs
@@ -135,10 +135,10 @@ fn bus_id_of(channel: &str) -> u64 {
 // Rust side: constraints and interactions evaluated on a row
 // =============================================================================
 
-/// `(bus id, signed multiplicity, bus elements)` of a Rust interaction on a row. A sender
-/// adds `+m`, a receiver `−m`; Clean's pull of multiplicity `e` counts `−e` and its push `+e`,
-/// so the signs agree once a receiver (the table that answers the lookup, Clean's push) keeps
-/// its multiplicity.
+/// `(bus id, signed multiplicity, bus elements)` of a Rust interaction on a row, signed the way
+/// Clean signs it: a sender (Clean's pull) counts `−m`, a receiver (the table that answers the
+/// lookup, Clean's push) counts `+m`. This is the opposite of the prover's LogUp sum, where a
+/// sender adds `+m`; `lean_interaction_at` signs Lean's pulls the same way.
 fn rust_interaction_at(i: &BusInteraction, row: &[FE]) -> (u64, FE, Vec<FE>) {
     let m = i.multiplicity.evaluate_with(|c| row[c]);
     let m = if i.is_sender { -m } else { m };

From 377b125e7ad56f13a44723b3f397bfe12148dedc Mon Sep 17 00:00:00 2001
From: jotabulacios <jbulacios@fi.uba.ar>
Date: Tue, 3 Nov 2026 15:40:34 -0300
Subject: [PATCH 5/6] Answer pull demand in eqComponent generation

Clean's Demand.direction is the net sign of a message, pushes minus
pulls, so a demand of direction .pull is one that was pulled more often
than pushed and needs a component that pushes to answer it. EQ pushes
its result on the ALU bus, so its generation mode has to trigger on
.pull, the same way pushStaticComponent does and the same way Clean's
own add8Component and lookup provider do. The field is inert today,
since generation is not part of TableSoundness and nothing here runs
Clean's witness generator, but .push described a component that answers
pushes by pulling, which EQ never does.
---
 formal/LambdaVM/Ensembles/EqLookup.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/formal/LambdaVM/Ensembles/EqLookup.lean b/formal/LambdaVM/Ensembles/EqLookup.lean
index d031460e1..b2abf4a3a 100644
--- a/formal/LambdaVM/Ensembles/EqLookup.lean
+++ b/formal/LambdaVM/Ensembles/EqLookup.lean
@@ -56,12 +56,14 @@ def pushStaticComponent {Message : TypeMap} [ProvableType Message]
     trigger := .pull
     input _ := pure (fromElements (Vector.replicate slc.table.length .multiplicity)) }
 
-/-- The EQ chip as a component, generated from the demand on the ALU bus. -/
+/-- The EQ chip as a component, generated from the demand on the ALU bus. EQ pushes its result,
+so the demand it answers is a pull: `Demand.direction` is `.pull` when a message was pulled more
+often than pushed. -/
 def eqComponent : Component (F p) where
   circuit := EQ.circuit
   generation := .demand {
     channel := Alu.channel
-    trigger := .push
+    trigger := .pull
     input _ := pure (fromElements (Vector.replicate (size EQ.Row) .multiplicity)) }
 
 @[circuit_norm] lemma pushStaticComponent_circuit {Message : TypeMap} [ProvableType Message]

From 23894db99a74ca802b232c7b982de7a5cb38c7de Mon Sep 17 00:00:00 2001
From: jotabulacios <jbulacios@fi.uba.ar>
Date: Tue, 3 Nov 2026 15:40:38 -0300
Subject: [PATCH 6/6] Update formal/README for the new Clean API

The Clean bump changed the things this file documents: pulls carry a
nonnegative multiplicity with an explicit direction instead of a
negative one, a pull owes a multiplicity of 0 or 1, BalancedInteractions
no longer carries the interaction count bound (it moved to the Balance's
fits, reaching soundness as the InteractionsFit premise), and
not_consistent is now a two-interaction witness instead of the p/N
construction. Also lists LambdaVM/StaticLookup.lean, which the bump
added, and records that the export format carries the direction.
---
 formal/README.md | 57 ++++++++++++++++++++++++++++++++----------------
 1 file changed, 38 insertions(+), 19 deletions(-)

diff --git a/formal/README.md b/formal/README.md
index 9b89fcbe9..b7f834d01 100644
--- a/formal/README.md
+++ b/formal/README.md
@@ -17,6 +17,11 @@ FRI / WHIR prover, the LogUp argument itself, the executor, GPU code.
   `spec/*.typ` page: `IsBit.circuit`, `IsByteCheck.circuit`, `Add.circuit`.
 - `LambdaVM/AluOp.lean` — the `alu_op` descriptors of `types.rs`, one enumeration
   for the `opsel` of BYTE_ALU and the low bits of the ALU flag byte.
+- `LambdaVM/StaticLookup.lean` — `StaticLookupChannel`: a table the verifier
+  knows, given as a list of rows, with `guarantees_iff` relating the list to the
+  semantic reading of a row, and `toChannel` for the components that read it.
+  Clean main replaced its own `StaticLookupChannel` by `Air.Flat.Lookup`, whose
+  rows are witness programs of the row index, so the structure lives here.
 - `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
@@ -24,9 +29,10 @@ FRI / WHIR prover, the LogUp argument itself, the executor, GPU code.
   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`, with the semantic `Guarantees`
-  proven equivalent to table membership. `Lt.lean` is the LT chip: the row
-  circuit mirrors `lt.rs` (constraints and interactions, in order), `core` is the
+  the table serves as a `StaticLookupChannel` (read through `toChannel`), with
+  the semantic `Guarantees` proven equivalent to table membership. `Lt.lean` is
+  the LT chip: the row circuit mirrors `lt.rs` (constraints and interactions, in
+  order), `core` is the
   arithmetic argument of `spec/lt.typ` on naturals, `Honest` is the row
   `generate_lt_trace` produces, `RowSpec` is what an active row establishes, and
   the `GeneralFormalCircuit` proves that a row that pulls its range checks
@@ -74,7 +80,8 @@ that they are the same polynomials and the same bus interactions is mechanical:
 
 1. `lake env lean --run LambdaVM/Export.lean` writes `export/{lt,eq,shift}.json`:
    every `assert` as an expression tree and every `interact` with its channel,
-   multiplicity and message, variables numbered in Rust column order.
+   direction, multiplicity and message, variables numbered in Rust column order.
+   Multiplicities are nonnegative; the direction carries the sign.
 2. `prover/src/tests/lean_diff.rs` is the prover test that reads them:
    `cargo test -p lambda-vm-prover lean_diff -- --nocapture`.
 
@@ -83,7 +90,9 @@ on 64 random rows and matches them as multisets of functions, does the same for
 the interactions (bus id, signed multiplicity, message elements), and checks
 that every Lean constraint vanishes on honest traces from `generate_*_trace`,
 padding rows included; the Lean-only constraints of the documented deltas are
-skipped there.
+skipped there. The sign of an interaction comes from its direction: a Rust
+sender is Clean's pull and counts `−m`, a receiver is Clean's push and counts
+`+m`.
 
 The models follow the multiplicity constraints of PR #1016, merged 2026-10-23.
 Result on `main` after that merge, 2026-10-28:
@@ -102,30 +111,39 @@ The check compares polynomials, not zero sets: it caught `μ·(μ − 1)` versus
 
 ## Counted pulls (`μ ∈ [0, 255]`)
 
-After PR #1016 a deduplicated row pulls its range checks with multiplicity `-μ`,
-`μ` a byte. Clean's typed channel grants the guarantee at `-1` only; any other
-nonzero multiplicity is a requirement the row cannot meet.
+After PR #1016 a deduplicated row pulls its range checks with multiplicity `μ`,
+`μ` a byte. Clean's typed channel grants the guarantee to a pull of multiplicity
+`1` only, and requires every pull to carry `0` or `1`; any other nonzero
+multiplicity is a requirement the row cannot meet.
 `LambdaVM/Channels/Counted.lean` is the generalisation:
 
-- `counted N channel` grants the guarantee at `-1, …, -N` and charges every
-  other nonzero multiplicity, mirroring `Channel.toRaw`. `pullIf`/`emit` are the
-  circuit operations, with `ExplicitCircuits` instances so elaboration works.
+- `counted N channel` grants the guarantee to a pull of `1, …, N` and charges
+  every other nonzero interaction, mirroring `Channel.toRaw`. `pullIf`/`emit`
+  are the circuit operations, with `ExplicitCircuits` instances so elaboration
+  works.
 - `exists_push_of_pull` and `consistent` are Clean's lemmas for this channel.
-  Their balance premise is `N · length < char F`, not Clean's `length < char F`.
+  Their balance premise is `N · length < char F`. Clean's `BalancedInteractions`
+  carries no length bound of its own: the bound is the `fits` of the `Balance`
+  the ensemble is checked against, and reaches soundness as the
+  `InteractionsFit` premise of `TableSoundness`. For `Balance.logUp`, `fits` is
+  `count < char F`.
 - `not_consistent` proves the premise cannot be weakened: for `2 ≤ N ≤ 255`
-  over Goldilocks, `p / N` pulls of `-N` plus `p % N` pulls of `-1` on a message
-  outside the table balance to `-p = 0` with fewer than `p` interactions, so
+  over Goldilocks, one pull of `N` and one pull of `1` on a message outside the
+  table satisfy `BalancedInteractions` — Clean counts the pull of `N` as a push
+  of the message, so the pull of `1` is matched — while the counted channel
+  reads both as pulls and the guarantee of the second is false. So
   `RawChannel.Consistent` is false and the channel cannot be finished in a
   `SoundEnsemble`. With `N = 1` the channel is `Normal`, as in Clean.
 - `Demo.circuit` is the shape of a dedup row: `ARE_BYTES[μ, 0]` then a counted
-  `IS_HALF` pull with multiplicity `-μ`. The counted channel sits in
+  `IS_HALF` pull with multiplicity `μ`. The counted channel sits in
   `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 `μ`:
 
-1. A per-channel multiplicity bound in `BalancedInteractions`
-   (`bound * length < ringChar F`), threaded through `BalancedChannels`.
+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
    requirements on the same channel when the requirements depend only on
    channels finished earlier), or the range check of `μ` as a static `lookup`,
@@ -170,5 +188,6 @@ Clean itself is compiled from source; only the modules we import are built.
   helper used inside a `main` needs an `ExplicitCircuit` instance, bridged to
   its body with `ExplicitCircuit.of_eq rfl (by infer_explicit_circuit)`.
 - A conditional interaction (`pullIf cond`) is only lawful when the same circuit
-  constrains `cond` to be boolean; multiplicities outside `{0, 1}` turn the
-  channel guarantee into a proof obligation.
+  constrains `cond` to be boolean: Clean requires every pull to carry
+  multiplicity `0` or `1`, and a pull outside `{0, 1}` is a requirement the
+  circuit cannot discharge at lawfulness.