Bump Clean to current main (f3abad7c) and Lean to v4.35.0 in formal/

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

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,100 @@ 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. 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 := .pull
+    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

formal/LambdaVM/Field.lean

@@ -108,24 +108,17 @@ 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
 
-/-- 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
     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)
@@ -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

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

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

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)

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 :=