diff --git a/formal/.gitignore b/formal/.gitignore new file mode 100644 index 000000000..01f8cdb63 --- /dev/null +++ b/formal/.gitignore @@ -0,0 +1 @@ +.lake/ diff --git a/formal/LambdaVM.lean b/formal/LambdaVM.lean new file mode 100644 index 000000000..c17601a11 --- /dev/null +++ b/formal/LambdaVM.lean @@ -0,0 +1,12 @@ +module + +public import LambdaVM.Field +public import LambdaVM.Templates.IsBit +public import LambdaVM.Tables.Bitwise +public import LambdaVM.Templates.IsByte +public import LambdaVM.Buses.Alu +public import LambdaVM.Tables.Lt +public import LambdaVM.Tables.Eq +public import LambdaVM.Tables.Shift +public import LambdaVM.Ensembles.EqLookup +public import LambdaVM.Channels.Counted diff --git a/formal/LambdaVM/Buses/Alu.lean b/formal/LambdaVM/Buses/Alu.lean new file mode 100644 index 000000000..410f4a7d2 --- /dev/null +++ b/formal/LambdaVM/Buses/Alu.lean @@ -0,0 +1,86 @@ +module + +public import LambdaVM.Field + +@[expose] public section + +/-! +# ALU bus (`BusId::Alu`) + +`ALU[out; in1, in2, flags]`: operands and result travel as `(lo32, hi32)` pairs, `flags` +carries the `alu_op` descriptor plus per-chip flag bits. Every ALU chip pushes to this +channel; the CPU pulls. Each chip adds the clause of `Guarantees` for its own `opsel`. +-/ + +namespace LambdaVM.Alu + +structure Msg (F : Type) where + in1Lo : F + in1Hi : F + in2Lo : F + in2Hi : F + flags : F + outLo : F + outHi : F +deriving ProvableStruct + +/-- `alu_op` descriptors (`prover/src/tables/types.rs`). -/ +def opselEQ : ℕ := 3 +def opselLT : ℕ := 4 +def opselSHIFT : ℕ := 5 + +/-- Two's complement reading of a 64-bit value. -/ +def toInt64 (n : ℕ) : ℤ := if n < 2^63 then (n : ℤ) else (n : ℤ) - 2^64 + +/-- `lhs < rhs`, signed or unsigned, as a bit. -/ +def ltRaw (signed L R : ℕ) : ℕ := + if signed = 1 then (if toInt64 L < toInt64 R then 1 else 0) else (if L < R then 1 else 0) + +/-- LT result: `(lhs < rhs) xor invert`. -/ +def ltBit (signed invert L R : ℕ) : ℕ := + if ltRaw signed L R = invert then 0 else 1 + +/-- EQ result: `(a = b) xor invert`. -/ +def eqBit (invert A B : ℕ) : ℕ := + if (if A = B then 1 else 0) = invert then 0 else 1 + +/-- Arithmetic right shift of a 64-bit value: sign-extend to 128 bits, shift, truncate. -/ +def sra64 (x k : ℕ) : ℕ := + if x < 2^63 then x >>> k else ((x + (2^128 - 2^64)) >>> k) % 2^64 + +/-- `SHIFT` result (spec/shift.typ): the shift amount is reduced mod 32 for word instructions +and mod 64 otherwise; `direction` picks left (0) or right (1); `signed` picks the arithmetic +right shift. Word results are not sign-extended here (the CPU does that). -/ +def shiftResult (word signed direction x s : ℕ) : ℕ := + let k := s % (if word = 1 then 32 else 64) + if direction = 0 then (x <<< k) % 2^64 + else if signed = 0 then x >>> k + else sra64 x k + +/-- 64-bit value of a `(lo32, hi32)` pair. -/ +def dword (lo hi : F p) : ℕ := lo.val + 2^32 * hi.val + +/-- What a puller learns. The caller must have range-checked both words of both operands +(the chips' `IS_WORD` assumptions). One clause per `opsel`. -/ +def Guarantees (m : Msg (F p)) : Prop := + m.in1Lo.val < 2^32 → m.in1Hi.val < 2^32 → m.in2Lo.val < 2^32 → m.in2Hi.val < 2^32 → + -- LT (spec/lt.typ): flags = opsel(LT) + 32·signed + 64·invert, out = [res, 0] + (∀ s i : ℕ, s < 2 → i < 2 → m.flags = ((opselLT + 32 * s + 64 * i : ℕ) : F p) → + m.outHi = 0 ∧ + m.outLo = ((ltBit s i (dword m.in1Lo m.in1Hi) (dword m.in2Lo m.in2Hi) : ℕ) : F p)) ∧ + -- EQ (spec/eq.typ): flags = opsel(EQ) + 64·invert, out = [res, 0] + (∀ i : ℕ, i < 2 → m.flags = ((opselEQ + 64 * i : ℕ) : F p) → + m.outHi = 0 ∧ + m.outLo = ((eqBit i (dword m.in1Lo m.in1Hi) (dword m.in2Lo m.in2Hi) : ℕ) : F p)) ∧ + -- SHIFT (spec/shift.typ): flags = opsel(SHIFT) + word_instr + 32·signed + 64·direction, + -- only the low byte of the shift amount matters + (∀ w s d : ℕ, w < 2 → s < 2 → d < 2 → + m.flags = ((opselSHIFT + w + 32 * s + 64 * d : ℕ) : F p) → + m.outLo.val < 2^32 ∧ m.outHi.val < 2^32 ∧ + dword m.outLo m.outHi = shiftResult w s d (dword m.in1Lo m.in1Hi) (m.in2Lo.val % 256)) + +def channel : Channel (F p) Msg where + name := "ALU" + Guarantees m _ := Guarantees m + +end LambdaVM.Alu diff --git a/formal/LambdaVM/Channels/Counted.lean b/formal/LambdaVM/Channels/Counted.lean new file mode 100644 index 000000000..00627daa0 --- /dev/null +++ b/formal/LambdaVM/Channels/Counted.lean @@ -0,0 +1,309 @@ +module + +public import Clean.Air.Balance +public import LambdaVM.Tables.Bitwise +public import Mathlib.Tactic.LinearCombination + +@[expose] public section + +/-! +# 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`). +-/ + +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) + +/-- `channel` with pulls allowed to carry a count up to `N`. -/ +def counted (N : ℕ) (channel : Channel F Message) : RawChannel F where + name := channel.name + 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 + +/-- Pull `msg` with multiplicity `-count`. -/ +@[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⟩]) + +/-- 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⟩]) + +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⟩] + 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⟩] + channelsWithGuarantees _ _ := [] + +attribute [explicit_circuit_no_unfold] pullIf emit + +/-- `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_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 + grts_of_not_pull := by + intro msg mult data hnp + simp only [counted] + exact fun hp => absurd hp hnp + +/-- On a message whose nonzero multiplicities are all counted pulls, the balance is minus a +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) → + ∃ 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⟩ + | i :: l, h => by + obtain ⟨s, hs, hb, ha⟩ := + balanceOf_counted N msg l (fun j hj => h j (List.mem_cons_of_mem _ hj)) + rw [balanceOf_cons] + simp only [List.length_cons, Nat.mul_succ] + by_cases hm : i.msg = msg + · by_cases h0 : i.mult = 0 + · refine ⟨s, by omega, ?_, ?_⟩ + · rw [if_pos hm, h0, 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 + refine ⟨k + s, by omega, ?_, ?_⟩ + · rw [if_pos hm, hk, hb]; push_cast; ring + · intro a _ _ _; omega + · refine ⟨s, by omega, ?_, ?_⟩ + · rw [if_neg hm, hb, zero_add] + · intro a ha' ham ha0 + rcases List.mem_cons.mp ha' with rfl | ha' + · exact absurd ham hm + · 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. -/ +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 + by_contra! hno + 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] + rcases bound with bound | hchar + · intro hk0 + rw [Lean.Grind.IsCharP.natCast_eq_zero_iff_of_lt _ (by omega)] at hk0 + omega + · rw [CharP.ringChar_zero_iff_CharZero] at hchar + exact Nat.cast_ne_zero.mpr (by omega) + have hs1 := h1 a ha rfl ha0 + have hzero := balance a.msg + rw [hb, neg_eq_zero] at hzero + rcases bound with bound | hchar + · rw [Lean.Grind.IsCharP.natCast_eq_zero_iff_of_lt _ (by omega)] at hzero + omega + · rw [CharP.ringChar_zero_iff_CharZero] at hchar + rw [Nat.cast_eq_zero] at hzero + omega + +/-- `RawChannel.Consistent` for a counted channel, under the stronger balance premise. -/ +theorem consistent (N : ℕ) (channel : RawChannel F) [Normal N channel] + (interactions : List (Interaction F)) (data : ProverData F) + (bound : N * interactions.length < ringChar F ∨ ringChar F = 0) + (balance : ∀ msg, balanceOf interactions msg = 0) + (reqs : ∀ i ∈ interactions, i.channel = channel ∧ i.Requirements data) : + ∀ i ∈ interactions, i.Guarantees data := by + intro a a_mem + simp only [Interaction.Guarantees, Interaction.Requirements, Interaction.msgVector] at reqs ⊢ + intro _ + 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 + have ⟨b_channel_eq, b_reqs⟩ := reqs _ b_mem + symm at b_channel_eq + simp only [b_msg_eq] at b_reqs + convert b_reqs + +/-! ## `N = 1` is Clean's normal channel -/ + +omit [DecidableEq F] in +lemma isPull_one_iff (mult : F) : IsPull 1 mult ↔ mult = -1 := by + constructor + · rintro ⟨k, hk1, hk, rfl⟩ + have : k = 1 := by omega + subst this; simp + · 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 + +example (channel : Channel F Message) : (counted 1 channel).Consistent := inferInstance + +end LambdaVM.Counted + +/-! ## `N ≥ 2` is not `Consistent` under Clean's balance premise -/ + +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. -/ +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] + 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⟩ + · refine ⟨rfl, ?_⟩ + simp only [Interaction.Requirements, mk, counted, Interaction.msgVector] + intro _ hnp + exact absurd ⟨N, by omega, le_rfl, rfl⟩ hnp + · refine ⟨rfl, ?_⟩ + 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 + simp only [Interaction.Guarantees, mk, counted, Interaction.msgVector] at hg + apply hm + have h := hg trivial ⟨1, le_rfl, by omega, by simp⟩ + convert h + simp [ProvableType.fromElements_toElements] + +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 +under `channelsWithRequirements` because the requirement on an out-of-range `μ` is only +discharged by the byte guarantee, which lawfulness cannot see; soundness can. -/ + +namespace LambdaVM.Counted.Demo +open LambdaVM Bitwise + +structure Row (F : Type) where + mu : F + x : F +deriving ProvableStruct + +def main (r : Var Row (F p)) : Circuit (F p) Unit := do + AreBytes.pull (r.mu, 0) + pullIf 255 IsHalf r.mu r.x + +def circuit : GeneralFormalCircuit (F p) Row unit where + main + Spec r _ _ := r.mu ≠ 0 → r.x.val < 65536 + ProverAssumptions r _ _ := r.mu.val < 256 ∧ r.x.val < 65536 + channelsWithRequirements := [counted 255 IsHalf] + requirementsChannelsLawful input_var i₀ := by + obtain ⟨mu, x⟩ := input_var + simp only [circuit_norm, main, pullIf, areBytesTable] + grind + 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 ⊢ + 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 => + ⟨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] + 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 new file mode 100644 index 000000000..e9de6b71a --- /dev/null +++ b/formal/LambdaVM/Ensembles/EqLookup.lean @@ -0,0 +1,102 @@ +module + +public import LambdaVM.Tables.Eq +public import Clean.Air.OrderedChannel + +@[expose] public section + +/-! +# The first ensemble: BITWISE lookups feeding the EQ chip + +Three components and three channels, in dependency order: the provider of `IS_HALF`, the +provider of `ZERO`, the EQ chip. Every channel is finished before the next table that pulls +from it, so Clean's ordered-channel soundness applies: in any witness whose constraints hold +and whose channels balance, every EQ row with `μ = 1` computes the equality bit. +-/ + +namespace LambdaVM.Ensembles +open Air.Flat + +/-- The provider side of a static lookup channel: one circuit that emits every entry of the +table with the prover's multiplicity for it. Its row is the vector of multiplicities, the +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 + 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] + Spec _ _ _ := True + soundness := by + circuit_proof_start + intro i _ _ + exact (slc.guarantees_iff _).mpr (List.getElem_mem _) + completeness := by circuit_proof_start + +/-- The provider has no pulls, and requires only its own channel. -/ +@[circuit_norm] +lemma pushStatic_channelsWithGuarantees {Message : TypeMap} [ProvableType Message] + (slc : StaticLookupChannel (F p) Message) [NeZero slc.table.length] : + (pushStatic slc).channelsWithGuarantees = [] := by + simp [circuit_norm, pushStatic] + +@[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 + +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) + +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 + +/-- 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⟩ → + ∀ row ∈ table.table, EQ.RowSpec (valueFromOffset EQ.Row 0 (table.environment row)) := by + have hsound : eqLookup.ensemble.TableSoundness := + Ensemble.tableSoundness_of_soundChannels + ⟨eqLookup.finished, eqLookup.finished_subset, eqLookup.soundChannels⟩ + 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 + simp only at hmem + intro row _ + rcases hmem with h | h | h | h <;> subst h <;> exact trivial + have hspec := hsound witness hassume hc hb + 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 + simp only at hcomp + subst hcomp + exact this + +end LambdaVM.Ensembles diff --git a/formal/LambdaVM/Export.lean b/formal/LambdaVM/Export.lean new file mode 100644 index 000000000..03db89207 --- /dev/null +++ b/formal/LambdaVM/Export.lean @@ -0,0 +1,22 @@ +import LambdaVM +import Clean.Circuit.Json + +/-! +Exports the operations of each modeled chip as JSON, for the differential check against the +Rust prover (`prover/src/tests/lean_diff.rs`). Variables are numbered in `Row` field order, +which is the Rust column order. +-/ + +open Lean LambdaVM + +def exportCircuit (name : String) {Row : TypeMap} [ProvableType Row] + (main : Var Row (F p) → Circuit (F p) Unit) : IO Unit := do + let ops := (main (varFromOffset Row 0)).operations 0 + let json := Json.mkObj [("name", name), ("columns", size Row), ("operations", toJson ops)] + IO.FS.writeFile s!"export/{name}.json" (json.pretty 100) + IO.println s!"wrote export/{name}.json" + +def main : IO Unit := do + exportCircuit "lt" LT.main + exportCircuit "eq" EQ.main + exportCircuit "shift" SHIFT.main diff --git a/formal/LambdaVM/Field.lean b/formal/LambdaVM/Field.lean new file mode 100644 index 000000000..7d03fa0da --- /dev/null +++ b/formal/LambdaVM/Field.lean @@ -0,0 +1,191 @@ +module + +public import Clean.Circuit +public import CompPoly.Fields.Goldilocks + +@[expose] public section + +namespace LambdaVM + +/-- Goldilocks, the base field of the Lambda VM prover: `2^64 - 2^32 + 1`. -/ +abbrev p : ℕ := Goldilocks.fieldSize + +instance : Fact p.Prime := ⟨Goldilocks.is_prime⟩ + +-- Size facts that Clean's gadgets ask for. +instance : Fact (p > 512) := by decide +instance : Fact (p > 2^16 + 2^8) := by decide +instance : Fact (p > 2^32) := by decide + +example : FiniteField (F p) := inferInstance + +end LambdaVM + +namespace LambdaVM + +/-! ## Lifting field identities on small naturals back to `ℕ` -/ + +lemma lt_p_of_lt_two_pow_40 {n : ℕ} (h : n < 2^40) : n < p := lt_trans h (by decide) + +lemma val_natCast_of_lt_two_pow_40 {n : ℕ} (h : n < 2^40) : ((n : F p)).val = n := + ZMod.val_natCast_of_lt (lt_p_of_lt_two_pow_40 h) + +/-- Casting naturals below `p` into the field is injective. -/ +lemma natCast_inj_of_lt {a b : ℕ} (ha : a < p) (hb : b < p) (h : (a : F p) = (b : F p)) : a = b := by + rw [ZMod.natCast_eq_natCast_iff', Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb] at h + exact h + +/-- `x.val = n` once `x` is known to be the cast of a small `n`. -/ +lemma val_eq_of_eq_natCast {x : F p} {n : ℕ} (h : x = (n : F p)) (hn : n < 2^40) : x.val = n := by + rw [h]; exact val_natCast_of_lt_two_pow_40 hn + +lemma isBool_of_mul_one_sub {x : F p} (h : x * (1 - x) = 0) : IsBool x := by + rw [mul_eq_zero, sub_eq_zero] at h + exact h.imp id Eq.symm + +lemma isBool_of_val_lt_two {x : F p} (h : x.val < 2) : IsBool x := by + have hx : x = (x.val : F p) := (ZMod.natCast_zmod_val x).symm + rcases Nat.lt_succ_iff.mp h |>.lt_or_eq with h0 | h1 + · left; rw [hx, Nat.lt_one_iff.mp h0]; simp + · right; rw [hx, h1]; simp + +/-- `2⁻³²`, the constant `INV_SHIFT_32` of the prover's constraint templates. -/ +def inv32 : F p := ((2 : F p)^32)⁻¹ + +lemma two_pow_32_ne_zero : (2 : F p)^32 ≠ 0 := by + have h : ((2^32 : ℕ) : F p) ≠ 0 := by + intro h0 + have := congrArg ZMod.val h0 + rw [val_natCast_of_lt_two_pow_40 (by norm_num), ZMod.val_zero] at this + norm_num at this + push_cast at h + exact h + +lemma inv32_mul_two_pow : inv32 * (2 : F p)^32 = 1 := inv_mul_cancel₀ two_pow_32_ne_zero +lemma two_pow_mul_inv32 : (2 : F p)^32 * inv32 = 1 := mul_inv_cancel₀ two_pow_32_ne_zero + +/-- A carry constraint `c = (a − b)·2⁻³²` with `c` boolean and `a, b` small lifts to +`a = b + c·2³²` on naturals. -/ +lemma carry_lift {a b c : F p} (ha : a.val < 2^36) (hb : b.val < 2^36) (hc : IsBool c) + (hdef : c = (a - b) * inv32) : a.val = b.val + c.val * 2^32 := by + have hab : a = b + c * 2^32 := by + rw [hdef, mul_assoc, inv32_mul_two_pow, mul_one]; ring + have hcast : ((a.val : ℕ) : F p) = ((b.val + c.val * 2^32 : ℕ) : F p) := by + push_cast + simp only [ZMod.natCast_zmod_val] + exact hab + have hc2 := IsBool.val_lt_two hc + exact natCast_inj_of_lt (lt_p_of_lt_two_pow_40 (by omega)) (lt_p_of_lt_two_pow_40 (by omega)) hcast + +end LambdaVM + +namespace LambdaVM + +lemma isBool_mul_one_sub {x : F p} (h : IsBool x) : x * (1 - x) = 0 := by + rcases h with rfl | rfl <;> simp + +/-- A field element with value below 2 is `0` or `1`, together with its value. -/ +lemma eq_zero_or_one_of_val {x : F p} (h : x.val < 2) : + (x = 0 ∧ x.val = 0) ∨ (x = 1 ∧ x.val = 1) := by + rcases isBool_of_val_lt_two h with rfl | rfl + · left; exact ⟨rfl, ZMod.val_zero⟩ + · right; refine ⟨rfl, ?_⟩ + rw [← Nat.cast_one]; exact val_natCast_of_lt_two_pow_40 (by norm_num) + +end LambdaVM + +namespace LambdaVM + +/-- A conditional interaction with a boolean multiplicity never has an active requirement. -/ +lemma requirement_vacuous {mu : F p} (h : mu * (mu - 1) = 0) (hne1 : ¬ -mu = -1) (hne0 : ¬ mu = 0) : + False := by + rcases IsBool.iff_mul_sub_one.mpr h with h0 | h1 + · exact hne0 h0 + · exact hne1 (by rw [h1]) + +end LambdaVM + +namespace LambdaVM + +lemma val_one_eq : (1 : F p).val = 1 := by + rw [← Nat.cast_one]; exact val_natCast_of_lt_two_pow_40 (by norm_num) + +end LambdaVM + +namespace LambdaVM + +lemma val_ofNat (n : ℕ) [n.AtLeastTwo] (h : n < 2^40) : (OfNat.ofNat n : F p).val = n := by + rw [← Nat.cast_ofNat]; exact val_natCast_of_lt_two_pow_40 h + +lemma val_neg_one : (-1 : F p).val = p - 1 := by + rw [ZMod.neg_val, if_neg one_ne_zero, val_one_eq] + +lemma three_lt_p : 3 < p := by decide + +/-- A field difference of two small naturals is small only if it does not wrap. -/ +lemma val_sub_of_val_lt {a b : ℕ} (ha : a < 2^40) (hb : b < 2^40) + (h : ((a : F p) - (b : F p)).val < 2^40) : b ≤ a ∧ ((a : F p) - (b : F p)).val = a - b := by + by_cases hab : b ≤ a + · refine ⟨hab, ?_⟩ + rw [← Nat.cast_sub hab] + exact val_natCast_of_lt_two_pow_40 (by omega) + · exfalso + have hlt : a < b := by omega + have h1 : ((a : F p) - (b : F p)) = -(((b - a : ℕ) : F p)) := by + rw [Nat.cast_sub hlt.le]; ring + rw [h1, ZMod.neg_val] at h + have hne : ((b - a : ℕ) : F p) ≠ 0 := by + intro h0 + 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 + 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)] + +/-- 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) + (h3 : IsBool (1 - l0 - l1 - l2)) : l0.val + l1.val + l2.val ≤ 1 := by + have hp := three_lt_p + have h3' := IsBool.val_lt_two h3 + rcases h0 with rfl | rfl <;> rcases h1 with rfl | rfl <;> rcases h2 with rfl | rfl + all_goals simp only [ZMod.val_zero, val_one_eq] + all_goals try omega + all_goals first + | (norm_num at h3'; done) + | (norm_num at h3'; simp only [val_neg_two] at h3'; omega) + +end LambdaVM + +namespace LambdaVM + +lemma eq_natCast_of_val {x : F p} {n : ℕ} (h : x.val = n) : x = (n : F p) := by + rw [← h, ZMod.natCast_zmod_val] + +end LambdaVM + +namespace LambdaVM + +/-- `requirement_vacuous` for the spec's form of the bit constraint, `μ·(1 − μ) = 0`. -/ +lemma requirement_vacuous' {mu : F p} (h : mu * (1 - mu) = 0) (hne1 : ¬ -mu = -1) (hne0 : ¬ mu = 0) : + False := by + rcases isBool_of_mul_one_sub h with h0 | h1 + · exact hne0 h0 + · exact hne1 (by rw [h1]) + +end LambdaVM diff --git a/formal/LambdaVM/Tables/Bitwise.lean b/formal/LambdaVM/Tables/Bitwise.lean new file mode 100644 index 000000000..faca1c382 --- /dev/null +++ b/formal/LambdaVM/Tables/Bitwise.lean @@ -0,0 +1,362 @@ +module + +public import LambdaVM.Field + +@[expose] public section + +/-! +# BITWISE (spec/bitwise.typ) + +Preprocessed table with one row per `(X, Y, Z) ∈ Byte × Byte × B4`, indexed by +`i = X + 256·Y + 65536·Z`, exactly as `generate_bitwise_row` in `prover/src/tables/bitwise.rs`. +Each bus the table serves is a static lookup channel whose rows are a projection of `row i`; +the channel's `Guarantees` is the semantic reading of that projection, and `guarantees_iff` +proves the two agree. Bus names follow `BusId` in `prover/src/tables/types.rs`. +-/ + +namespace LambdaVM.Bitwise + +/-- The eleven precomputed columns of one row, as naturals. -/ +structure Row where + x : ℕ + y : ℕ + z : ℕ + and : ℕ + or : ℕ + xor : ℕ + msb8 : ℕ + msb16 : ℕ + zero : ℕ + sll : ℕ + sllc : ℕ + +def numRows : ℕ := 2^20 + +/-- Row index of `(x, y, z)`. -/ +def index (x y z : ℕ) : ℕ := x + 256 * y + 65536 * z + +/-- `generate_bitwise_row`, with `/` and `%` where Rust masks and shifts the index. -/ +def row (i : ℕ) : Row := + let x := i % 256 + let y := i / 256 % 256 + let z := i / 65536 % 16 + let halfword := x + 256 * y + { x, y, z + and := x &&& y + or := x ||| y + xor := x ^^^ y + msb8 := x / 128 + msb16 := halfword / 32768 + zero := if x = 0 ∧ y = 0 ∧ z = 0 then 1 else 0 + sll := if z = 0 then halfword else (halfword <<< z) % 65536 + sllc := if z = 0 then 0 else halfword >>> (16 - z) } + +def rows : List Row := (List.range numRows).map row + +lemma mem_rows_iff {r : Row} : r ∈ rows ↔ ∃ i < numRows, row i = r := by + simp [rows, List.mem_map, List.mem_range] + +lemma index_lt {x y z : ℕ} (hx : x < 256) (hy : y < 256) (hz : z < 16) : + index x y z < numRows := by + unfold index numRows; omega + +lemma row_x_lt (i : ℕ) : (row i).x < 256 := Nat.mod_lt _ (by norm_num) +lemma row_y_lt (i : ℕ) : (row i).y < 256 := Nat.mod_lt _ (by norm_num) +lemma row_z_lt (i : ℕ) : (row i).z < 16 := Nat.mod_lt _ (by norm_num) + +lemma row_index {x y z : ℕ} (hx : x < 256) (hy : y < 256) (hz : z < 16) : + row (index x y z) = + let halfword := x + 256 * y + { x, y, z + and := x &&& y + or := x ||| y + xor := x ^^^ y + msb8 := x / 128 + msb16 := halfword / 32768 + zero := if x = 0 ∧ y = 0 ∧ z = 0 then 1 else 0 + sll := if z = 0 then halfword else (halfword <<< z) % 65536 + sllc := if z = 0 then 0 else halfword >>> (16 - z) } := by + have h1 : index x y z % 256 = x := by unfold index; omega + have h2 : index x y z / 256 % 256 = y := by unfold index; omega + have h3 : index x y z / 65536 % 16 = z := by unfold index; omega + simp only [row, h1, h2, h3] + +/-- Everything in the table is below `2^20 < p`, so casting to the field is injective. -/ +lemma lt_p_of_lt_two_pow_20 {n : ℕ} (h : n < 2^20) : n < p := lt_trans h (by decide) + +lemma val_natCast_of_lt_two_pow_20 {n : ℕ} (h : n < 2^20) : ((n : F p)).val = n := + ZMod.val_natCast_of_lt (lt_p_of_lt_two_pow_20 h) + +/-! ## Range-check channels -/ + +/-- `ARE_BYTES[X, Y]` (`BusId::AreBytes`): both values are bytes. -/ +def areBytesTable : StaticLookupChannel (F p) fieldPair where + name := "ARE_BYTES" + table := rows.map fun r => ((r.x : F p), (r.y : F p)) + Guarantees | (x, y) => x.val < 256 ∧ y.val < 256 + guarantees_iff := by + rintro ⟨x, y⟩ + simp only [List.mem_map, mem_rows_iff, Prod.mk.injEq] + constructor + · rintro ⟨hx, hy⟩ + refine ⟨row (index x.val y.val 0), ⟨_, index_lt hx hy (by norm_num), rfl⟩, ?_, ?_⟩ + · rw [row_index hx hy (by norm_num)]; exact ZMod.natCast_zmod_val x + · rw [row_index hx hy (by norm_num)]; exact ZMod.natCast_zmod_val y + · rintro ⟨r, ⟨i, _, rfl⟩, rfl, rfl⟩ + 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 + +/-- `IS_HALF[X + 256·Y]` (`BusId::IsHalfword`): the value is a halfword. -/ +def isHalfTable : StaticLookupChannel (F p) field where + name := "IS_HALF" + table := rows.map fun r => ((r.x + 256 * r.y : ℕ) : F p) + Guarantees h := h.val < 65536 + guarantees_iff := by + intro h + simp only [List.mem_map, mem_rows_iff] + constructor + · intro hh + refine ⟨row (index (h.val % 256) (h.val / 256) 0), + ⟨_, index_lt (by omega) (by omega) (by norm_num), rfl⟩, ?_⟩ + rw [row_index (by omega) (by omega) (by norm_num)] + simp only + rw [show h.val % 256 + 256 * (h.val / 256) = h.val by omega] + exact ZMod.natCast_zmod_val h + · rintro ⟨r, ⟨i, _, rfl⟩, rfl⟩ + 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 + +/-- `IS_B20[X + 256·Y + 65536·Z]` (`BusId::IsB20`): the value is below `2^20`. -/ +def isB20Table : StaticLookupChannel (F p) field where + name := "IS_B20" + table := rows.map fun r => ((r.x + 256 * r.y + 65536 * r.z : ℕ) : F p) + Guarantees v := v.val < 2^20 + guarantees_iff := by + intro v + simp only [List.mem_map, mem_rows_iff] + constructor + · intro hv + refine ⟨row (index (v.val % 256) (v.val / 256 % 256) (v.val / 65536)), + ⟨_, index_lt (by omega) (by omega) (by omega), rfl⟩, ?_⟩ + rw [row_index (by omega) (by omega) (by omega)] + simp only + rw [show v.val % 256 + 256 * (v.val / 256 % 256) + 65536 * (v.val / 65536) = v.val by omega] + exact ZMod.natCast_zmod_val v + · rintro ⟨r, ⟨i, _, rfl⟩, rfl⟩ + 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 + +/-! ## Bit-extraction channels -/ + +lemma row_msb8 (i : ℕ) : (row i).msb8 = (row i).x / 128 := rfl +lemma row_msb16 (i : ℕ) : (row i).msb16 = ((row i).x + 256 * (row i).y) / 32768 := rfl +lemma row_zero (i : ℕ) : + (row i).zero = if (row i).x = 0 ∧ (row i).y = 0 ∧ (row i).z = 0 then 1 else 0 := rfl + +/-- `MSB8[X] -> MSB8` (`BusId::Msb8`): `X` is a byte and the output is its top bit. -/ +def msb8Table : StaticLookupChannel (F p) fieldPair where + name := "MSB8" + table := rows.map fun r => ((r.x : F p), (r.msb8 : F p)) + Guarantees | (x, m) => x.val < 256 ∧ m.val = x.val / 128 + guarantees_iff := by + rintro ⟨x, m⟩ + simp only [List.mem_map, mem_rows_iff, Prod.mk.injEq] + constructor + · rintro ⟨hx, hm⟩ + refine ⟨row (index x.val 0 0), ⟨_, index_lt hx (by norm_num) (by norm_num), rfl⟩, ?_, ?_⟩ + · rw [row_index hx (by norm_num) (by norm_num)]; exact ZMod.natCast_zmod_val x + · rw [row_index hx (by norm_num) (by norm_num)] + simp only + rw [← hm]; exact ZMod.natCast_zmod_val m + · rintro ⟨r, ⟨i, _, rfl⟩, rfl, rfl⟩ + have := row_x_lt i + rw [val_natCast_of_lt_two_pow_20 (by omega), val_natCast_of_lt_two_pow_20 (by rw [row_msb8]; omega), + row_msb8] + exact ⟨this, rfl⟩ + +abbrev Msb8 : Channel (F p) fieldPair := .fromStatic _ _ msb8Table + +/-- `MSB16[X + 256·Y] -> MSB16` (`BusId::Msb16`): a halfword and its top bit. -/ +def msb16Table : StaticLookupChannel (F p) fieldPair where + name := "MSB16" + table := rows.map fun r => (((r.x + 256 * r.y : ℕ) : F p), (r.msb16 : F p)) + Guarantees | (h, m) => h.val < 65536 ∧ m.val = h.val / 32768 + guarantees_iff := by + rintro ⟨h, m⟩ + simp only [List.mem_map, mem_rows_iff, Prod.mk.injEq] + constructor + · rintro ⟨hh, hm⟩ + refine ⟨row (index (h.val % 256) (h.val / 256) 0), + ⟨_, index_lt (by omega) (by omega) (by norm_num), rfl⟩, ?_, ?_⟩ + · rw [row_index (by omega) (by omega) (by norm_num)] + simp only + rw [show h.val % 256 + 256 * (h.val / 256) = h.val by omega] + exact ZMod.natCast_zmod_val h + · rw [row_index (by omega) (by omega) (by norm_num)] + simp only + rw [show h.val % 256 + 256 * (h.val / 256) = h.val by omega, ← hm] + exact ZMod.natCast_zmod_val m + · rintro ⟨r, ⟨i, _, rfl⟩, rfl, rfl⟩ + have := row_x_lt i; have := row_y_lt i + rw [val_natCast_of_lt_two_pow_20 (by omega), val_natCast_of_lt_two_pow_20 (by rw [row_msb16]; omega), + row_msb16] + exact ⟨by omega, rfl⟩ + +abbrev Msb16 : Channel (F p) fieldPair := .fromStatic _ _ msb16Table + +/-- `ZERO[X + 256·Y + 65536·Z] -> ZERO` (`BusId::Zero`): a 20-bit value and its zero flag. -/ +def zeroTable : StaticLookupChannel (F p) fieldPair where + name := "ZERO" + table := rows.map fun r => (((r.x + 256 * r.y + 65536 * r.z : ℕ) : F p), (r.zero : F p)) + Guarantees | (v, z) => v.val < 2^20 ∧ z = if v = 0 then 1 else 0 + guarantees_iff := by + rintro ⟨v, z⟩ + simp only [List.mem_map, mem_rows_iff, Prod.mk.injEq] + constructor + · rintro ⟨hv, hz⟩ + refine ⟨row (index (v.val % 256) (v.val / 256 % 256) (v.val / 65536)), + ⟨_, index_lt (by omega) (by omega) (by omega), rfl⟩, ?_, ?_⟩ + · rw [row_index (by omega) (by omega) (by omega)] + simp only + rw [show v.val % 256 + 256 * (v.val / 256 % 256) + 65536 * (v.val / 65536) = v.val by omega] + exact ZMod.natCast_zmod_val v + · rw [row_index (by omega) (by omega) (by omega)] + simp only + have hiff : (v.val % 256 = 0 ∧ v.val / 256 % 256 = 0 ∧ v.val / 65536 = 0) ↔ v = 0 := by + rw [← ZMod.val_eq_zero]; omega + rw [hz] + simp only [hiff] + split_ifs <;> simp + · rintro ⟨r, ⟨i, _, rfl⟩, rfl, rfl⟩ + 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), row_zero] + refine ⟨by omega, ?_⟩ + have hn : (((row i).x + 256 * (row i).y + 65536 * (row i).z : ℕ) : F p) = 0 ↔ + ((row i).x = 0 ∧ (row i).y = 0 ∧ (row i).z = 0) := by + rw [← ZMod.val_eq_zero, val_natCast_of_lt_two_pow_20 (by omega)]; omega + simp only [hn] + split_ifs <;> simp + +abbrev Zero : Channel (F p) fieldPair := .fromStatic _ _ zeroTable + +/-! ## Byte ALU and halfword shift channels -/ + +/-- Message of `BYTE_ALU[opsel, X, Y] -> out` (`BusId::ByteAlu`), `opsel` = AND 0 / OR 1 / XOR 2. -/ +structure ByteAluMsg (F : Type) where + opsel : F + x : F + y : F + out : F +deriving ProvableStruct + +lemma row_and (i : ℕ) : (row i).and = (row i).x &&& (row i).y := rfl +lemma row_or (i : ℕ) : (row i).or = (row i).x ||| (row i).y := rfl +lemma row_xor (i : ℕ) : (row i).xor = (row i).x ^^^ (row i).y := rfl + +lemma and_lt_256 {x y : ℕ} (hy : y < 256) : x &&& y < 256 := Nat.and_le_right.trans_lt hy +lemma or_lt_256 {x y : ℕ} (hx : x < 256) (hy : y < 256) : x ||| y < 256 := by + have := Nat.or_lt_two_pow (n := 8) (by norm_num; exact hx) (by norm_num; exact hy) + norm_num at this; exact this +lemma xor_lt_256 {x y : ℕ} (hx : x < 256) (hy : y < 256) : x ^^^ y < 256 := by + have := Nat.xor_lt_two_pow (n := 8) (by norm_num; exact hx) (by norm_num; exact hy) + norm_num at this; exact this + +def byteAluTable : StaticLookupChannel (F p) ByteAluMsg where + name := "BYTE_ALU" + table := rows.flatMap fun r => + [ ⟨0, r.x, r.y, r.and⟩, ⟨1, r.x, r.y, r.or⟩, ⟨2, r.x, r.y, r.xor⟩ ] + Guarantees + | { opsel, x, y, out } => + x.val < 256 ∧ y.val < 256 ∧ + ((opsel = 0 ∧ out.val = x.val &&& y.val) ∨ + (opsel = 1 ∧ out.val = x.val ||| y.val) ∨ + (opsel = 2 ∧ out.val = x.val ^^^ y.val)) + guarantees_iff := by + rintro ⟨opsel, x, y, out⟩ + simp only [List.mem_flatMap, mem_rows_iff, List.mem_cons, + List.not_mem_nil, or_false, ByteAluMsg.mk.injEq] + constructor + · rintro ⟨hx, hy, hop⟩ + refine ⟨row (index x.val y.val 0), ⟨_, index_lt hx hy (by norm_num), rfl⟩, ?_⟩ + rw [row_index hx hy (by norm_num)] + simp only + rcases hop with ⟨rfl, hout⟩ | ⟨rfl, hout⟩ | ⟨rfl, hout⟩ + · left; refine ⟨by simp, (ZMod.natCast_zmod_val x).symm, (ZMod.natCast_zmod_val y).symm, ?_⟩ + rw [← hout]; exact (ZMod.natCast_zmod_val out).symm + · right; left; refine ⟨by simp, (ZMod.natCast_zmod_val x).symm, (ZMod.natCast_zmod_val y).symm, ?_⟩ + rw [← hout]; exact (ZMod.natCast_zmod_val out).symm + · right; right; refine ⟨by simp, (ZMod.natCast_zmod_val x).symm, (ZMod.natCast_zmod_val y).symm, ?_⟩ + rw [← hout]; exact (ZMod.natCast_zmod_val out).symm + · rintro ⟨r, ⟨i, _, rfl⟩, ⟨rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl⟩⟩ + all_goals + have hx := row_x_lt i; have hy := row_y_lt i + rw [val_natCast_of_lt_two_pow_20 (by omega), val_natCast_of_lt_two_pow_20 (by omega)] + refine ⟨hx, hy, ?_⟩ + · left; rw [row_and, val_natCast_of_lt_two_pow_20 (by linarith [and_lt_256 (x := (row i).x) hy])] + simp + · right; left; rw [row_or, val_natCast_of_lt_two_pow_20 (by linarith [or_lt_256 hx hy])] + simp + · 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 + +/-- Message of `HWSL[X + 256·Y, Z] -> [SLL, SLLC]` (`BusId::Hwsl`). -/ +structure HwslMsg (F : Type) where + h : F + z : F + sll : F + sllc : F +deriving ProvableStruct + +lemma row_sll (i : ℕ) : (row i).sll = + if (row i).z = 0 then (row i).x + 256 * (row i).y + else (((row i).x + 256 * (row i).y) <<< (row i).z) % 65536 := rfl +lemma row_sllc (i : ℕ) : (row i).sllc = + if (row i).z = 0 then 0 else ((row i).x + 256 * (row i).y) >>> (16 - (row i).z) := rfl + +def hwslTable : StaticLookupChannel (F p) HwslMsg where + name := "HWSL" + table := rows.map fun r => ⟨((r.x + 256 * r.y : ℕ) : F p), r.z, r.sll, r.sllc⟩ + Guarantees + | { h, z, sll, sllc } => + h.val < 65536 ∧ z.val < 16 ∧ + sll.val = (if z.val = 0 then h.val else (h.val <<< z.val) % 65536) ∧ + sllc.val = (if z.val = 0 then 0 else h.val >>> (16 - z.val)) + guarantees_iff := by + rintro ⟨h, z, sll, sllc⟩ + simp only [List.mem_map, mem_rows_iff, HwslMsg.mk.injEq] + constructor + · rintro ⟨hh, hz, hsll, hsllc⟩ + refine ⟨row (index (h.val % 256) (h.val / 256) z.val), + ⟨_, index_lt (by omega) (by omega) hz, rfl⟩, ?_⟩ + rw [row_index (by omega) (by omega) hz] + simp only + rw [show h.val % 256 + 256 * (h.val / 256) = h.val by omega] + refine ⟨ZMod.natCast_zmod_val h, ZMod.natCast_zmod_val z, ?_, ?_⟩ + · rw [← hsll]; exact ZMod.natCast_zmod_val sll + · rw [← hsllc]; exact ZMod.natCast_zmod_val sllc + · rintro ⟨r, ⟨i, _, rfl⟩, rfl, rfl, rfl, rfl⟩ + have hx := row_x_lt i; have hy := row_y_lt i; have hz := row_z_lt i + have hsll_lt : (row i).sll < 65536 := by + rw [row_sll]; split_ifs + · omega + · exact Nat.mod_lt _ (by norm_num) + have hsllc_lt : (row i).sllc < 65536 := by + rw [row_sllc]; split_ifs + · norm_num + · exact (Nat.shiftRight_le _ _).trans_lt (by omega) + rw [val_natCast_of_lt_two_pow_20 (by omega), val_natCast_of_lt_two_pow_20 (by omega), + val_natCast_of_lt_two_pow_20 (by omega), val_natCast_of_lt_two_pow_20 (by omega), + row_sll, row_sllc] + exact ⟨by omega, hz, rfl, rfl⟩ + +abbrev Hwsl : Channel (F p) HwslMsg := .fromStatic _ _ hwslTable + +end LambdaVM.Bitwise diff --git a/formal/LambdaVM/Tables/Eq.lean b/formal/LambdaVM/Tables/Eq.lean new file mode 100644 index 000000000..112a5fc36 --- /dev/null +++ b/formal/LambdaVM/Tables/Eq.lean @@ -0,0 +1,250 @@ +module + +public import LambdaVM.Tables.Bitwise +public import LambdaVM.Buses.Alu +public import Mathlib.Tactic.LinearCombination + +@[expose] public section + +/-! +# EQ (spec/eq.typ) + +One row per equality test `res = (a = b) xor invert`. Columns follow `prover/src/tables/eq.rs`: +`a`, `b` as `DWordWL` (two words), `diff = a − b` as four halves, the `eq` bit, `res`, `μ`. + +`diff` is enforced with the SUB template (the ADD carries of `b + diff = a`), its halves are +range-checked, and `eq` is the ZERO lookup of their sum: four halves sum to zero iff all are +zero iff `a = b`. +-/ + +namespace LambdaVM.EQ +open Alu (eqBit dword) + +structure Row (F : Type) where + a0 : F + a1 : F + b0 : F + b1 : F + invert : F + res : F + diff0 : F + diff1 : F + diff2 : F + diff3 : F + eq : F + mu : F +deriving ProvableStruct + +/-- The chip's arithmetic on naturals: with `b + diff = a (mod 2⁶⁴)` and everything in range, +the halves of `diff` sum to zero exactly when `a = b`. -/ +theorem core {a0 a1 b0 b1 d0 d1 d2 d3 c0 c1 : ℕ} + (ha0 : a0 < 2^32) (ha1 : a1 < 2^32) (hb0 : b0 < 2^32) (hb1 : b1 < 2^32) + (hd0 : d0 < 2^16) (hd1 : d1 < 2^16) (hd2 : d2 < 2^16) (hd3 : d3 < 2^16) + (hc0 : c0 < 2) (hc1 : c1 < 2) + (e0 : b0 + (d0 + 65536 * d1) = a0 + c0 * 2^32) + (e1 : b1 + (d2 + 65536 * d3) + c0 = a1 + c1 * 2^32) : + d0 + d1 + d2 + d3 = 0 ↔ a0 + 2^32 * a1 = b0 + 2^32 * b1 := by + have h64 : b0 + 2^32 * b1 + (d0 + 65536 * d1 + 2^32 * (d2 + 65536 * d3)) + = a0 + 2^32 * a1 + c1 * 2^64 := by omega + rcases (by omega : c1 = 0 ∨ c1 = 1) with rfl | rfl + · constructor <;> intro h <;> omega + · constructor <;> intro h <;> omega + +def main (r : Var Row (F p)) : Circuit (F p) Unit := do + -- IS_HALF[diff[i]], IS_BIT + Bitwise.IsHalf.pullIf r.mu r.diff0 + Bitwise.IsHalf.pullIf r.mu r.diff1 + Bitwise.IsHalf.pullIf r.mu r.diff2 + Bitwise.IsHalf.pullIf r.mu r.diff3 + assertZero (r.invert * (1 - r.invert)) + -- SUB = ADD: the carries of b + diff = a are bits + let diffLo := r.diff0 + 65536 * r.diff1 + let diffHi := r.diff2 + 65536 * r.diff3 + let c0 := (r.b0 + diffLo - r.a0) * inv32 + let c1 := (r.b1 + diffHi + c0 - r.a1) * inv32 + assertZero (c0 * (1 - c0)) + assertZero (c1 * (1 - c1)) + -- ZERO[Σ diff[i]] -> eq + Bitwise.Zero.pullIf r.mu (r.diff0 + r.diff1 + r.diff2 + r.diff3, r.eq) + -- res = eq xor invert + assertZero (r.res + 2 * r.eq * r.invert - r.eq - r.invert) + -- μ : Bit (no deduplication) + assertZero (r.mu * (1 - r.mu)) + -- output: ALU[a, b, opsel(EQ) + 64·invert] -> [res, 0] + Alu.channel.pushIf r.mu ⟨r.a0, r.a1, r.b0, r.b1, 3 + 64 * r.invert, r.res, 0⟩ + +/-- The honest prover's row, as `generate_eq_trace` fills it. -/ +def Honest (r : Row (F p)) : Prop := + IsBool r.mu ∧ IsBool r.invert ∧ + r.a0.val < 2^32 ∧ r.a1.val < 2^32 ∧ r.b0.val < 2^32 ∧ r.b1.val < 2^32 ∧ + r.diff0.val < 2^16 ∧ r.diff1.val < 2^16 ∧ r.diff2.val < 2^16 ∧ r.diff3.val < 2^16 ∧ + -- diff = a − b (mod 2⁶⁴) + (r.b0.val + 2^32 * r.b1.val + + (r.diff0.val + 65536 * r.diff1.val + 2^32 * (r.diff2.val + 65536 * r.diff3.val))) % 2^64 + = r.a0.val + 2^32 * r.a1.val ∧ + r.eq.val = (if r.a0.val + 2^32 * r.a1.val = r.b0.val + 2^32 * r.b1.val then 1 else 0) ∧ + r.res.val = eqBit r.invert.val (r.a0.val + 2^32 * r.a1.val) (r.b0.val + 2^32 * r.b1.val) + +/-- What an active row establishes: with range-checked operands, `res` is the equality bit. -/ +def RowSpec (r : Row (F p)) : Prop := + r.mu = 1 → r.a0.val < 2^32 → r.a1.val < 2^32 → r.b0.val < 2^32 → r.b1.val < 2^32 → + r.res = ((eqBit r.invert.val (r.a0.val + 2^32 * r.a1.val) (r.b0.val + 2^32 * r.b1.val) : ℕ) : F p) + +def circuit : GeneralFormalCircuit (F p) Row unit where + main + Spec r _ _ := RowSpec r + channelsWithRequirements := [Alu.channel.toRaw] + requirementsChannelsLawful input_var i₀ := by + obtain ⟨a0, a1, b0, b1, invert, res, diff0, diff1, diff2, diff3, eq, mu⟩ := input_var + simp only [circuit_norm, main, Alu.channel, Bitwise.isHalfTable, Bitwise.zeroTable] + constructor + · intro channel h; tauto + · intro env h + refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;> + · intro hne1 hne0 + exact (requirement_vacuous' h.2.2.2.2 hne1 hne0).elim + + soundness := by + circuit_proof_start [main, RowSpec, Alu.channel, Alu.Guarantees, Bitwise.isHalfTable, + Bitwise.zeroTable] + obtain ⟨h_d0, h_d1, h_d2, h_d3, h_i, h_c0, h_c1, h_z, h_res, h_mu⟩ := h_holds + rcases isBool_of_mul_one_sub h_mu with h0 | h1 + · subst h0; simp + subst h1 + have hib : IsBool input_invert := isBool_of_mul_one_sub h_i + have hi_2 := IsBool.val_lt_two hib + have hd0 := h_d0 rfl + have hd1 := h_d1 rfl + have hd2 := h_d2 rfl + have hd3 := h_d3 rfl + obtain ⟨-, heq⟩ := h_z rfl + -- the equality bit, from the pulled guarantees and the SUB carries + have key : input_a0.val < 2^32 → input_a1.val < 2^32 → input_b0.val < 2^32 → + input_b1.val < 2^32 → + input_res = ((eqBit input_invert.val (input_a0.val + 2^32 * input_a1.val) + (input_b0.val + 2^32 * input_b1.val) : ℕ) : F p) := by + intro ha0 ha1 hb0 hb1 + set c0 := (input_b0 + (input_diff0 + 65536 * input_diff1) - input_a0) * inv32 with hc0 + set c1 := (input_b1 + (input_diff2 + 65536 * input_diff3) + c0 - input_a1) * inv32 with hc1 + have hc0b : IsBool c0 := isBool_of_mul_one_sub h_c0 + have hc1b : IsBool c1 := isBool_of_mul_one_sub h_c1 + have hc0_2 := IsBool.val_lt_two hc0b + have hval_lo : (input_b0 + (input_diff0 + 65536 * input_diff1)).val + = input_b0.val + (input_diff0.val + 65536 * input_diff1.val) := + val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega) + have hval_hi : (input_b1 + (input_diff2 + 65536 * input_diff3) + c0).val + = input_b1.val + (input_diff2.val + 65536 * input_diff3.val) + c0.val := + val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega) + have e0 := carry_lift (by omega) (by omega) hc0b hc0 + rw [hval_lo] at e0 + have e1 := carry_lift (by omega) (by omega) hc1b hc1 + rw [hval_hi] at e1 + have hcore := core ha0 ha1 hb0 hb1 hd0 hd1 hd2 hd3 hc0_2 (IsBool.val_lt_two hc1b) e0 e1 + have hval_sum : (input_diff0 + input_diff1 + input_diff2 + input_diff3).val + = input_diff0.val + input_diff1.val + input_diff2.val + input_diff3.val := + val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega) + have hz : input_diff0 + input_diff1 + input_diff2 + input_diff3 = 0 ↔ + input_a0.val + 2^32 * input_a1.val = input_b0.val + 2^32 * input_b1.val := by + rw [← ZMod.val_eq_zero, hval_sum]; exact hcore + have heq_cast : input_eq = ((if input_a0.val + 2^32 * input_a1.val + = input_b0.val + 2^32 * input_b1.val then 1 else 0 : ℕ) : F p) := by + rw [heq] + simp only [hz] + split_ifs <;> simp + have hres' : input_res = input_eq + input_invert - 2 * input_eq * input_invert := by + linear_combination h_res + rcases eq_zero_or_one_of_val hi_2 with ⟨rfl, hiv⟩ | ⟨rfl, hiv⟩ <;> + rw [hres', heq_cast, hiv] <;> + 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 + refine ⟨?_, ?_, ?_⟩ + · -- the LT clause does not apply: opsel(EQ) + 64·i ≠ opsel(LT) + 32·s + 64·i' + intro s i hs hi hflags + exfalso + have h1 : ((3 + 64 * input_invert.val : ℕ) : F p) + = ((Alu.opselLT + 32 * s + 64 * i : ℕ) : F p) := by + rw [← hflags]; push_cast; simp only [ZMod.natCast_zmod_val] + have h2 := natCast_inj_of_lt (lt_p_of_lt_two_pow_40 (by omega)) + (lt_p_of_lt_two_pow_40 (by simp only [Alu.opselLT]; omega)) h1 + simp only [Alu.opselLT] at h2 + omega + swap + · -- nor the SHIFT clause + intro w s d hw hs hd hflags + exfalso + have h1 : ((3 + 64 * input_invert.val : ℕ) : F p) + = ((Alu.opselSHIFT + w + 32 * s + 64 * d : ℕ) : F p) := by + rw [← hflags]; push_cast; simp only [ZMod.natCast_zmod_val] + have h2 := natCast_inj_of_lt (lt_p_of_lt_two_pow_40 (by omega)) + (lt_p_of_lt_two_pow_40 (by simp only [Alu.opselSHIFT]; omega)) h1 + simp only [Alu.opselSHIFT] at h2 + omega + intro i hi hflags + have hiv : input_invert.val = i := by + have h1 : ((3 + 64 * input_invert.val : ℕ) : F p) = ((Alu.opselEQ + 64 * i : ℕ) : F p) := by + rw [← hflags]; push_cast; simp only [ZMod.natCast_zmod_val] + have h2 := natCast_inj_of_lt (lt_p_of_lt_two_pow_40 (by omega)) + (lt_p_of_lt_two_pow_40 (by simp only [Alu.opselEQ]; omega)) h1 + simp only [Alu.opselEQ] at h2 + omega + rw [key ha0 ha1 hb0 hb1, hiv] + simp only [dword] + + ProverAssumptions r _ _ := Honest r + + completeness := by + circuit_proof_start [main, Alu.channel, Alu.Guarantees, Bitwise.isHalfTable, Bitwise.zeroTable, + Honest] + obtain ⟨hmu, hib, ha0, ha1, hb0, hb1, hd0, hd1, hd2, hd3, hsum, heq, hres⟩ := h_assumptions + obtain ⟨k0, hk0, e0⟩ : ∃ k0, k0 < 2 ∧ + input_b0.val + (input_diff0.val + 65536 * input_diff1.val) = input_a0.val + k0 * 2^32 := + ⟨(input_b0.val + (input_diff0.val + 65536 * input_diff1.val)) / 2^32, by omega, by omega⟩ + obtain ⟨k1, hk1, e1⟩ : ∃ k1, k1 < 2 ∧ + input_b1.val + (input_diff2.val + 65536 * input_diff3.val) + k0 = input_a1.val + k1 * 2^32 := + ⟨(input_b1.val + (input_diff2.val + 65536 * input_diff3.val) + k0) / 2^32, by omega, by omega⟩ + set c0 := (input_b0 + (input_diff0 + 65536 * input_diff1) - input_a0) * inv32 with hc0 + set c1 := (input_b1 + (input_diff2 + 65536 * input_diff3) + c0 - input_a1) * inv32 with hc1 + have hc0k : c0 = (k0 : F p) := by + have h := congrArg (fun n : ℕ => (n : F p)) e0 + push_cast at h + simp only [ZMod.natCast_zmod_val] at h + have h' : input_b0 + (input_diff0 + 65536 * input_diff1) - input_a0 = (k0 : F p) * 2^32 := by + linear_combination h + rw [hc0, h', mul_assoc, two_pow_mul_inv32, mul_one] + have hc1k : c1 = (k1 : F p) := by + have h := congrArg (fun n : ℕ => (n : F p)) e1 + push_cast at h + simp only [ZMod.natCast_zmod_val] at h + have h' : input_b1 + (input_diff2 + 65536 * input_diff3) + c0 - input_a1 = (k1 : F p) * 2^32 := by + rw [hc0k]; linear_combination h + rw [hc1, h', mul_assoc, two_pow_mul_inv32, mul_one] + have hval_sum : (input_diff0 + input_diff1 + input_diff2 + input_diff3).val + = input_diff0.val + input_diff1.val + input_diff2.val + input_diff3.val := + val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega) + have hcore := core ha0 ha1 hb0 hb1 hd0 hd1 hd2 hd3 hk0 hk1 e0 e1 + have hz : input_diff0 + input_diff1 + input_diff2 + input_diff3 = 0 ↔ + input_a0.val + 2^32 * input_a1.val = input_b0.val + 2^32 * input_b1.val := by + rw [← ZMod.val_eq_zero, hval_sum]; exact hcore + have heq_cast : input_eq = ((if input_a0.val + 2^32 * input_a1.val + = input_b0.val + 2^32 * input_b1.val then 1 else 0 : ℕ) : F p) := by + rw [← heq, ZMod.natCast_zmod_val] + have hres_cast : input_res = ((eqBit input_invert.val (input_a0.val + 2^32 * input_a1.val) + (input_b0.val + 2^32 * input_b1.val) : ℕ) : F p) := by + rw [← hres, ZMod.natCast_zmod_val] + refine ⟨fun _ => by omega, fun _ => by omega, fun _ => by omega, fun _ => by omega, + isBool_mul_one_sub hib, ?_, ?_, fun _ => ⟨by rw [hval_sum]; omega, ?_⟩, ?_, + isBool_mul_one_sub hmu⟩ + · rw [hc0k]; rcases (by omega : k0 = 0 ∨ k0 = 1) with rfl | rfl <;> simp + · rw [hc1k]; rcases (by omega : k1 = 0 ∨ k1 = 1) with rfl | rfl <;> simp + · rw [heq_cast] + simp only [hz] + split_ifs <;> simp + · rw [hres_cast, heq_cast] + rcases eq_zero_or_one_of_val (IsBool.val_lt_two hib) with ⟨rfl, hiv⟩ | ⟨rfl, hiv⟩ <;> + rw [hiv] <;> + simp only [eqBit] <;> + split_ifs <;> (try norm_num) <;> omega + +end LambdaVM.EQ diff --git a/formal/LambdaVM/Tables/Lt.lean b/formal/LambdaVM/Tables/Lt.lean new file mode 100644 index 000000000..358208e0d --- /dev/null +++ b/formal/LambdaVM/Tables/Lt.lean @@ -0,0 +1,342 @@ +module + +public import LambdaVM.Tables.Bitwise +public import LambdaVM.Buses.Alu +public import Mathlib.Tactic.LinearCombination + +@[expose] public section + +/-! +# LT (spec/lt.typ) + +One row per `(lhs, rhs, signed, invert)` comparison. Columns follow `prover/src/tables/lt.rs`: +`lhs`/`rhs` as `DWordHHW` limbs (word, half, half), `lhs_sub_rhs` as four halves, the two +sign bits, `lt`, `res = lt xor invert` and the multiplicity `μ`. + +The carries of `rhs + lhs_sub_rhs = lhs (mod 2⁶⁴)` are virtual: `carry = (…)·2⁻³²`. +-/ + +namespace LambdaVM.LT +open Alu (toInt64 ltRaw ltBit dword) + +structure Row (F : Type) where + lhs0 : F + lhs1 : F + lhs2 : F + rhs0 : F + rhs1 : F + rhs2 : F + signed : F + lt : F + sub0 : F + sub1 : F + sub2 : F + sub3 : F + lhsMsb : F + rhsMsb : F + invert : F + res : F + mu : F +deriving ProvableStruct + +/-- The LT chip's arithmetic on naturals: the carries of the limb-wise identity +`rhs + (lhs − rhs mod 2⁶⁴) = lhs + c₁·2⁶⁴` decide `lhs < rhs`, and the top halves decide the signs. -/ +theorem core + {l0 l1 l2 r0 r1 r2 s0 s1 s2 s3 c0 c1 A B : ℕ} + (hl0 : l0 < 2^32) (hl1 : l1 < 2^16) (hl2 : l2 < 2^16) + (hr0 : r0 < 2^32) (hr1 : r1 < 2^16) (hr2 : r2 < 2^16) + (hs0 : s0 < 2^16) (hs1 : s1 < 2^16) (hs2 : s2 < 2^16) (hs3 : s3 < 2^16) + (hc0 : c0 < 2) (hc1 : c1 < 2) + (hA : A = l2 / 32768) (hB : B = r2 / 32768) + (e0 : r0 + (s0 + 65536 * s1) = l0 + c0 * 2^32) + (e1 : r1 + 65536 * r2 + (s2 + 65536 * s3) + c0 = l1 + 65536 * l2 + c1 * 2^32) : + let L := l0 + 2^32 * (l1 + 65536 * l2) + let R := r0 + 2^32 * (r1 + 65536 * r2) + (c1 = 1 ↔ L < R) ∧ (A = 1 ↔ 2^63 ≤ L) ∧ (B = 1 ↔ 2^63 ≤ R) ∧ A < 2 ∧ B < 2 ∧ + (toInt64 L < toInt64 R ↔ ((A = 1 ∧ B = 0) ∨ (A = B ∧ L < R))) := by + intro L R + subst hA hB + refine ⟨by omega, by omega, by omega, by omega, by omega, ?_⟩ + simp only [toInt64] + split_ifs <;> omega + +def main (r : Var Row (F p)) : Circuit (F p) Unit := do + -- μ : Bit. The spec types it so; the Rust chip does not constrain it (see README). + assertZero (r.mu * (1 - r.mu)) + -- range: IS_HALF[lhs[1]], IS_HALF[rhs[1]], IS_BIT, IS_BIT + Bitwise.IsHalf.pullIf r.mu r.lhs1 + Bitwise.IsHalf.pullIf r.mu r.rhs1 + assertZero (r.signed * (1 - r.signed)) + assertZero (r.invert * (1 - r.invert)) + -- defs: MSB16[lhs[2]] -> lhs_msb, MSB16[rhs[2]] -> rhs_msb + Bitwise.Msb16.pullIf r.mu (r.lhs2, r.lhsMsb) + Bitwise.Msb16.pullIf r.mu (r.rhs2, r.rhsMsb) + let lhsHi := r.lhs1 + 65536 * r.lhs2 + let rhsHi := r.rhs1 + 65536 * r.rhs2 + let subLo := r.sub0 + 65536 * r.sub1 + let subHi := r.sub2 + 65536 * r.sub3 + let c0 := (r.rhs0 + subLo - r.lhs0) * inv32 + let c1 := (rhsHi + subHi + c0 - lhsHi) * inv32 + -- lt = signed·(A(1−B) + A·C + (1−B)·C) + (1−signed)·C, with C = carry[1] + assertZero (r.lt - (r.signed * (r.lhsMsb * (1 - r.rhsMsb) + r.lhsMsb * c1 + (1 - r.rhsMsb) * c1) + + (1 - r.signed) * c1)) + -- res = lt xor invert + assertZero (r.res + 2 * r.lt * r.invert - r.lt - r.invert) + -- sub: IS_BIT, IS_HALF[lhs_sub_rhs[i]] + assertZero (c0 * (1 - c0)) + assertZero (c1 * (1 - c1)) + Bitwise.IsHalf.pullIf r.mu r.sub0 + Bitwise.IsHalf.pullIf r.mu r.sub1 + Bitwise.IsHalf.pullIf r.mu r.sub2 + Bitwise.IsHalf.pullIf r.mu r.sub3 + -- output: ALU[lhs, rhs, opsel(LT) + 32·signed + 64·invert] -> [res, 0] + Alu.channel.pushIf r.mu + ⟨r.lhs0, lhsHi, r.rhs0, rhsHi, 4 + 32 * r.signed + 64 * r.invert, r.res, 0⟩ + +lemma ltRaw_lt_two {s L R : ℕ} : ltRaw s L R < 2 := by + unfold ltRaw; split_ifs <;> omega + +/-- On an honest row the `lt` bit is the chip's polynomial `s·Q(A, B, C) + (1 − s)·C`. -/ +lemma ltRaw_eq_poly {s A B k1 L R : ℕ} (hs : s < 2) (hA2 : A < 2) (hB2 : B < 2) (hk : k1 < 2) + (hC : k1 = 1 ↔ L < R) (hA : A = 1 ↔ 2^63 ≤ L) (hB : B = 1 ↔ 2^63 ≤ R) + (hS : toInt64 L < toInt64 R ↔ ((A = 1 ∧ B = 0) ∨ (A = B ∧ L < R))) : + ltRaw s L R = s * (A * (1 - B) + A * k1 + (1 - B) * k1) + (1 - s) * k1 := by + unfold ltRaw + rcases (by omega : s = 0 ∨ s = 1) with rfl | rfl <;> + rcases (by omega : A = 0 ∨ A = 1) with rfl | rfl <;> + rcases (by omega : B = 0 ∨ B = 1) with rfl | rfl <;> + rcases (by omega : k1 = 0 ∨ k1 = 1) with rfl | rfl <;> + norm_num at hC hA hB hS ⊢ <;> + first + | (exfalso; omega) + | (rw [← not_lt, hS]; omega) + | simp [hS, hC] + +lemma ltBit_eq {s i L R : ℕ} (hi : i < 2) : + ltBit s i L R = ltRaw s L R + i - 2 * ltRaw s L R * i := by + unfold ltBit + have := ltRaw_lt_two (s := s) (L := L) (R := R) + rcases (by omega : ltRaw s L R = 0 ∨ ltRaw s L R = 1) with h | h <;> + rcases (by omega : i = 0 ∨ i = 1) with rfl | rfl <;> simp [h] + +/-- The `lt` constraint, from the natural-number identity. -/ +lemma lt_constraint {signed A B k1 lt : F p} {sv Av Bv kv : ℕ} + (hs : signed = (sv : F p)) (hA : A = (Av : F p)) (hB : B = (Bv : F p)) (hk : k1 = (kv : F p)) + (hs2 : sv < 2) (hB2 : Bv < 2) + (hlt : lt = ((sv * (Av * (1 - Bv) + Av * kv + (1 - Bv) * kv) + (1 - sv) * kv : ℕ) : F p)) : + lt - (signed * (A * (1 - B) + A * k1 + (1 - B) * k1) + (1 - signed) * k1) = 0 := by + subst hs hA hB hk hlt + push_cast [Nat.cast_sub (by omega : Bv ≤ 1), Nat.cast_sub (by omega : sv ≤ 1)] + ring + +/-- The `res = lt xor invert` constraint, from the natural-number identity. -/ +lemma res_constraint {lt invert res : F p} {ltv iv : ℕ} + (hlt : lt = (ltv : F p)) (hi : invert = (iv : F p)) (hltv : ltv < 2) (hiv : iv < 2) + (hres : res = ((ltv + iv - 2 * ltv * iv : ℕ) : F p)) : + res + 2 * lt * invert - lt - invert = 0 := by + subst hlt hi hres + rcases (by omega : ltv = 0 ∨ ltv = 1) with rfl | rfl <;> + rcases (by omega : iv = 0 ∨ iv = 1) with rfl | rfl <;> norm_num + +/-- The honest prover's row, as `generate_lt_trace` fills it. -/ +def Honest (r : Row (F p)) : Prop := + IsBool r.mu ∧ IsBool r.signed ∧ IsBool r.invert ∧ + r.lhs0.val < 2^32 ∧ r.lhs1.val < 2^16 ∧ r.lhs2.val < 2^16 ∧ + r.rhs0.val < 2^32 ∧ r.rhs1.val < 2^16 ∧ r.rhs2.val < 2^16 ∧ + r.sub0.val < 2^16 ∧ r.sub1.val < 2^16 ∧ r.sub2.val < 2^16 ∧ r.sub3.val < 2^16 ∧ + -- lhs_sub_rhs = lhs − rhs (mod 2⁶⁴) + (r.rhs0.val + 2^32 * (r.rhs1.val + 65536 * r.rhs2.val) + + (r.sub0.val + 65536 * r.sub1.val + 2^32 * (r.sub2.val + 65536 * r.sub3.val))) % 2^64 + = r.lhs0.val + 2^32 * (r.lhs1.val + 65536 * r.lhs2.val) ∧ + r.lhsMsb.val = r.lhs2.val / 32768 ∧ r.rhsMsb.val = r.rhs2.val / 32768 ∧ + r.lt.val = ltRaw r.signed.val (r.lhs0.val + 2^32 * (r.lhs1.val + 65536 * r.lhs2.val)) + (r.rhs0.val + 2^32 * (r.rhs1.val + 65536 * r.rhs2.val)) ∧ + r.res.val = ltBit r.signed.val r.invert.val (r.lhs0.val + 2^32 * (r.lhs1.val + 65536 * r.lhs2.val)) + (r.rhs0.val + 2^32 * (r.rhs1.val + 65536 * r.rhs2.val)) + +def circuit : GeneralFormalCircuit (F p) Row unit where + main + Spec _ _ _ := True + channelsWithRequirements := [Alu.channel.toRaw] + requirementsChannelsLawful input_var i₀ := by + obtain ⟨lhs0, lhs1, lhs2, rhs0, rhs1, rhs2, signed, lt, sub0, sub1, sub2, sub3, + lhsMsb, rhsMsb, invert, res, mu⟩ := input_var + simp only [circuit_norm, main, Alu.channel, Bitwise.isHalfTable, Bitwise.msb16Table] + constructor + · intro channel h; tauto + · intro env h + refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> + · intro hne1 hne0 + exact (requirement_vacuous' h.1 hne1 hne0).elim + + soundness := by + circuit_proof_start [main, Alu.channel, Alu.Guarantees, Bitwise.isHalfTable, Bitwise.msb16Table] + obtain ⟨h_mu, h_l1, h_r1, h_s, h_i, h_lm, h_rm, h_lt, h_res, h_c0, h_c1, h_s0, h_s1, h_s2, h_s3⟩ := + h_holds + -- μ ∈ {0, 1}; with μ = 0 every requirement is vacuous + rcases isBool_of_mul_one_sub h_mu with h0 | h1 + · subst h0; simp + subst h1 + refine ⟨by simp, by simp, by simp, by simp, by simp, by simp, by simp, by simp, ?_⟩ + intro _ _ hl0 hlhi hr0 hrhi + refine ⟨?_, ?_, ?_⟩ + rotate_left + · -- the EQ clause does not apply: opsel(LT) + 32·s + 64·i ≠ opsel(EQ) + 64·i' + intro i hi hflags + exfalso + have hsb := isBool_of_mul_one_sub h_s + have hib := isBool_of_mul_one_sub h_i + have hs_2 := IsBool.val_lt_two hsb + have hi_2 := IsBool.val_lt_two hib + have h1 : ((4 + 32 * input_signed.val + 64 * input_invert.val : ℕ) : F p) + = ((Alu.opselEQ + 64 * i : ℕ) : F p) := by + rw [← hflags]; push_cast; simp only [ZMod.natCast_zmod_val] + have h2 := natCast_inj_of_lt (lt_p_of_lt_two_pow_40 (by omega)) + (lt_p_of_lt_two_pow_40 (by simp only [Alu.opselEQ]; omega)) h1 + simp only [Alu.opselEQ] at h2 + omega + · -- nor the SHIFT clause: opsel(SHIFT) + w + 32·s + 64·d ≡ 5 or 6 (mod 32) + intro w s d hw hs hd hflags + exfalso + have hsb := isBool_of_mul_one_sub h_s + have hib := isBool_of_mul_one_sub h_i + have hs_2 := IsBool.val_lt_two hsb + have hi_2 := IsBool.val_lt_two hib + have h1 : ((4 + 32 * input_signed.val + 64 * input_invert.val : ℕ) : F p) + = ((Alu.opselSHIFT + w + 32 * s + 64 * d : ℕ) : F p) := by + rw [← hflags]; push_cast; simp only [ZMod.natCast_zmod_val] + have h2 := natCast_inj_of_lt (lt_p_of_lt_two_pow_40 (by omega)) + (lt_p_of_lt_two_pow_40 (by simp only [Alu.opselSHIFT]; omega)) h1 + simp only [Alu.opselSHIFT] at h2 + omega + intro s i hs hi hflags + -- the pulled guarantees are now unconditional + have hl1 := h_l1 rfl + have hr1 := h_r1 rfl + obtain ⟨hl2, hlm⟩ := h_lm rfl + obtain ⟨hr2, hrm⟩ := h_rm rfl + have hs0 := h_s0 rfl + have hs1 := h_s1 rfl + have hs2 := h_s2 rfl + have hs3 := h_s3 rfl + -- the virtual carries + set c0 := (input_rhs0 + (input_sub0 + 65536 * input_sub1) - input_lhs0) * inv32 with hc0 + set c1 := (input_rhs1 + 65536 * input_rhs2 + (input_sub2 + 65536 * input_sub3) + c0 + - (input_lhs1 + 65536 * input_lhs2)) * inv32 with hc1 + have hc0b : IsBool c0 := isBool_of_mul_one_sub h_c0 + have hc1b : IsBool c1 := isBool_of_mul_one_sub h_c1 + have hsb : IsBool input_signed := isBool_of_mul_one_sub h_s + have hib : IsBool input_invert := isBool_of_mul_one_sub h_i + have hc0_2 := IsBool.val_lt_two hc0b + have hc1_2 := IsBool.val_lt_two hc1b + have hs_2 := IsBool.val_lt_two hsb + have hi_2 := IsBool.val_lt_two hib + -- values of the composite limbs + have hval_lhsHi : (input_lhs1 + 65536 * input_lhs2).val = input_lhs1.val + 65536 * input_lhs2.val := + val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega) + have hval_rhsHi : (input_rhs1 + 65536 * input_rhs2).val = input_rhs1.val + 65536 * input_rhs2.val := + val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega) + have hval_lo : (input_rhs0 + (input_sub0 + 65536 * input_sub1)).val + = input_rhs0.val + (input_sub0.val + 65536 * input_sub1.val) := + val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega) + have hval_hi : (input_rhs1 + 65536 * input_rhs2 + (input_sub2 + 65536 * input_sub3) + c0).val + = input_rhs1.val + 65536 * input_rhs2.val + (input_sub2.val + 65536 * input_sub3.val) + c0.val := + val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega) + -- the carry identities, on naturals + have e0 := carry_lift (by omega) (by omega) hc0b hc0 + rw [hval_lo] at e0 + have e1 := carry_lift (by omega) (by omega) hc1b hc1 + rw [hval_hi, hval_lhsHi] at e1 + obtain ⟨hC, hA, hB, hA2, hB2, hS⟩ := + core hl0 hl1 hl2 hr0 hr1 hr2 hs0 hs1 hs2 hs3 hc0_2 hc1_2 hlm hrm e0 e1 + -- decode the flags + have hsi : input_signed.val = s ∧ input_invert.val = i := by + have h1 : ((4 + 32 * input_signed.val + 64 * input_invert.val : ℕ) : F p) + = ((Alu.opselLT + 32 * s + 64 * i : ℕ) : F p) := by + rw [← hflags]; push_cast; simp only [ZMod.natCast_zmod_val] + have h2 := natCast_inj_of_lt (lt_p_of_lt_two_pow_40 (by omega)) + (lt_p_of_lt_two_pow_40 (by simp only [Alu.opselLT]; omega)) h1 + simp only [Alu.opselLT] at h2 + omega + -- lt and res as field identities in the boolean values + have hlt' : input_lt = input_signed * (input_lhsMsb * (1 - input_rhsMsb) + input_lhsMsb * c1 + + (1 - input_rhsMsb) * c1) + (1 - input_signed) * c1 := by + rw [← sub_eq_zero]; exact h_lt + have hres' : input_res = input_lt + input_invert - 2 * input_lt * input_invert := by + linear_combination h_res + rw [← ZMod.natCast_zmod_val input_signed, ← ZMod.natCast_zmod_val input_lhsMsb, + ← ZMod.natCast_zmod_val input_rhsMsb, ← ZMod.natCast_zmod_val c1, hsi.1] at hlt' + rw [← ZMod.natCast_zmod_val input_invert, hsi.2] at hres' + simp only [dword, hval_lhsHi, hval_rhsHi] + rcases (by omega : s = 0 ∨ s = 1) with rfl | rfl <;> + rcases (by omega : i = 0 ∨ i = 1) with rfl | rfl <;> + rcases (by omega : input_lhsMsb.val = 0 ∨ input_lhsMsb.val = 1) with hAv | hAv <;> + rcases (by omega : input_rhsMsb.val = 0 ∨ input_rhsMsb.val = 1) with hBv | hBv <;> + rcases (by omega : c1.val = 0 ∨ c1.val = 1) with hcv | hcv <;> + simp only [hAv, hBv, hcv, Nat.cast_zero, Nat.cast_one] at hlt' hA hB hC hS <;> + norm_num at hlt' hA hB hC hS <;> + first + | (exfalso; omega) + | (subst hlt'; norm_num at hres'; simp [ltBit, ltRaw, hS, hC, hres']) + + + ProverAssumptions r _ _ := Honest r + + completeness := by + circuit_proof_start [main, Alu.channel, Alu.Guarantees, Bitwise.isHalfTable, Bitwise.msb16Table, + Honest] + obtain ⟨hmu, hsb, hib, hl0, hl1, hl2, hr0, hr1, hr2, hs0, hs1, hs2, hs3, hsum, hlm, hrm, hlt, hres⟩ := + h_assumptions + set L := input_lhs0.val + 2^32 * (input_lhs1.val + 65536 * input_lhs2.val) with hL + set R := input_rhs0.val + 2^32 * (input_rhs1.val + 65536 * input_rhs2.val) with hR + -- the honest carries + obtain ⟨k0, hk0, e0⟩ : ∃ k0, k0 < 2 ∧ + input_rhs0.val + (input_sub0.val + 65536 * input_sub1.val) = input_lhs0.val + k0 * 2^32 := + ⟨(input_rhs0.val + (input_sub0.val + 65536 * input_sub1.val)) / 2^32, by omega, by omega⟩ + obtain ⟨k1, hk1, e1⟩ : ∃ k1, k1 < 2 ∧ + input_rhs1.val + 65536 * input_rhs2.val + (input_sub2.val + 65536 * input_sub3.val) + k0 + = input_lhs1.val + 65536 * input_lhs2.val + k1 * 2^32 := + ⟨(input_rhs1.val + 65536 * input_rhs2.val + (input_sub2.val + 65536 * input_sub3.val) + k0) / 2^32, + by omega, by omega⟩ + set c0 := (input_rhs0 + (input_sub0 + 65536 * input_sub1) - input_lhs0) * inv32 with hc0 + set c1 := (input_rhs1 + 65536 * input_rhs2 + (input_sub2 + 65536 * input_sub3) + c0 + - (input_lhs1 + 65536 * input_lhs2)) * inv32 with hc1 + have hc0k : c0 = (k0 : F p) := by + have h := congrArg (fun n : ℕ => (n : F p)) e0 + push_cast at h + simp only [ZMod.natCast_zmod_val] at h + have h' : input_rhs0 + (input_sub0 + 65536 * input_sub1) - input_lhs0 = (k0 : F p) * 2^32 := by + linear_combination h + rw [hc0, h', mul_assoc, two_pow_mul_inv32, mul_one] + have hc1k : c1 = (k1 : F p) := by + have h := congrArg (fun n : ℕ => (n : F p)) e1 + push_cast at h + simp only [ZMod.natCast_zmod_val] at h + have h' : input_rhs1 + 65536 * input_rhs2 + (input_sub2 + 65536 * input_sub3) + c0 + - (input_lhs1 + 65536 * input_lhs2) = (k1 : F p) * 2^32 := by + rw [hc0k]; linear_combination h + rw [hc1, h', mul_assoc, two_pow_mul_inv32, mul_one] + have hA2 : input_lhsMsb.val < 2 := by omega + have hB2 : input_rhsMsb.val < 2 := by omega + obtain ⟨hC, hA, hB, -, -, hS⟩ := + core hl0 hl1 hl2 hr0 hr1 hr2 hs0 hs1 hs2 hs3 hk0 hk1 hlm hrm e0 e1 + have hpoly := ltRaw_eq_poly (IsBool.val_lt_two hsb) hA2 hB2 hk1 hC hA hB hS + have hlt_raw : input_lt = ((ltRaw input_signed.val L R : ℕ) : F p) := by + rw [← hlt, ZMod.natCast_zmod_val] + have hres_cast : input_res = ((ltRaw input_signed.val L R + input_invert.val + - 2 * ltRaw input_signed.val L R * input_invert.val : ℕ) : F p) := by + rw [← ltBit_eq (IsBool.val_lt_two hib), ← hres, ZMod.natCast_zmod_val] + refine ⟨isBool_mul_one_sub hmu, fun _ => by omega, fun _ => by omega, + isBool_mul_one_sub hsb, isBool_mul_one_sub hib, + fun _ => ⟨by omega, hlm⟩, fun _ => ⟨by omega, hrm⟩, ?_, ?_, ?_, ?_, + fun _ => by omega, fun _ => by omega, fun _ => by omega, fun _ => by omega⟩ + · exact lt_constraint (ZMod.natCast_zmod_val input_signed).symm + (ZMod.natCast_zmod_val input_lhsMsb).symm (ZMod.natCast_zmod_val input_rhsMsb).symm hc1k + (IsBool.val_lt_two hsb) hB2 (by rw [hlt_raw, hpoly]) + · exact res_constraint hlt_raw (ZMod.natCast_zmod_val input_invert).symm ltRaw_lt_two + (IsBool.val_lt_two hib) hres_cast + · rw [hc0k]; rcases (by omega : k0 = 0 ∨ k0 = 1) with rfl | rfl <;> simp + · rw [hc1k]; rcases (by omega : k1 = 0 ∨ k1 = 1) with rfl | rfl <;> simp + + +end LambdaVM.LT diff --git a/formal/LambdaVM/Tables/Shift.lean b/formal/LambdaVM/Tables/Shift.lean new file mode 100644 index 000000000..d1e86e208 --- /dev/null +++ b/formal/LambdaVM/Tables/Shift.lean @@ -0,0 +1,814 @@ +module + +public import LambdaVM.Tables.Bitwise +public import LambdaVM.Buses.Alu +public import LambdaVM.Tables.ShiftCore +public import Mathlib.Tactic.LinearCombination + +@[expose] public section + +/-! +# SHIFT (spec/shift.typ) + +One row per shift. Columns follow `prover/src/tables/shift.rs`: `in` as four halves, the low +byte of the shift amount plus its upper limbs for the ALU bus, the three flags, `out` as two +words, and the scratch of the two-phase design: `bit_shift = shift mod 16` (or its complement +when shifting right), `zbs = [bit_shift = 0]`, the HWSL outputs `X[i], Y[i]`, the one-hot +`limb_shift`, and the sign bit. +-/ + +namespace LambdaVM.SHIFT +open Alu (dword shiftResult) +open ShiftCore (sll sllc limbs) + +structure Row (F : Type) where + in0 : F + in1 : F + in2 : F + in3 : F + shiftAmount : F + direction : F + signed : F + wordInstr : F + out0 : F + out1 : F + isNegative : F + bitShift : F + zbs : F + x0 : F + x1 : F + x2 : F + x3 : F + x4 : F + y0 : F + y1 : F + y2 : F + y3 : F + ls0 : F + ls1 : F + ls2 : F + mu : F + shiftB1 : F + shiftH1 : F + shiftHigh : F +deriving ProvableStruct + +/-- The `shifted` limbs of the spec as one polynomial, over expressions or over field values: +`mu`, `d` (direction), the stored one-hot `l0 l1 l2`, the extension limb `e`, and the HWSL +outputs `x0..x4`, `y0..y3`. Kept folded during circuit proofs; `eval_shiftedPoly` pushes +evaluation inside. -/ +def shiftedPoly {R : Type} [Add R] [Mul R] [Sub R] [OfNat R 1] + (mu d l0 l1 l2 e x0 x1 x2 x3 x4 y0 y1 y2 y3 : R) : R × R × R × R := + let l3 := 1 - l0 - l1 - l2 + let left := mu - d + let right := d + let il0 := x0 + let il1 := x1 + y0 + let il2 := x2 + y1 + let il3 := x3 + y2 + let ir0 := y0 + x1 + let ir1 := y1 + x2 + let ir2 := y2 + x3 + let ir3 := y3 + x4 + (left * (l0 * il0) + right * (l0 * ir0 + l1 * ir1 + l2 * ir2 + l3 * ir3), + left * (l0 * il1 + l1 * il0) + right * (l0 * ir1 + l1 * ir2 + l2 * ir3 + e * l3), + left * (l0 * il2 + l1 * il1 + l2 * il0) + right * (l0 * ir2 + l1 * ir3 + e * (l2 + l3)), + left * (l0 * il3 + l1 * il2 + l2 * il1 + l3 * il0) + right * (l0 * ir3 + e * (l1 + l2 + l3))) + +def main (r : Var Row (F p)) : Circuit (F p) Unit := do + let left := r.mu - r.direction + let right := r.direction + let extension := 65535 * r.isNegative + let ls3 := 1 - r.ls0 - r.ls1 - r.ls2 + let sh := shiftedPoly r.mu r.direction r.ls0 r.ls1 r.ls2 extension + r.x0 r.x1 r.x2 r.x3 r.x4 r.y0 r.y1 r.y2 r.y3 + -- constraints, in the order of `ShiftConstraints::eval` + assertZero (r.direction * (1 - r.mu)) + assertZero (r.zbs * (r.x0 - r.in0 * left)) + assertZero (r.zbs * (r.x1 - r.in1 * left)) + assertZero (r.zbs * (r.x2 - r.in2 * left)) + assertZero (r.zbs * (r.x3 - r.in3 * left)) + assertZero (r.zbs * r.x4) + assertZero (r.zbs * (r.y0 - r.in0 * right)) + assertZero (r.zbs * (r.y1 - r.in1 * right)) + assertZero (r.zbs * (r.y2 - r.in2 * right)) + assertZero (r.zbs * (r.y3 - r.in3 * right)) + assertZero (r.ls0 * (1 - r.ls0)) + assertZero (r.ls1 * (1 - r.ls1)) + assertZero (r.ls2 * (1 - r.ls2)) + assertZero (ls3 * (1 - ls3)) + assertZero (r.out0 - sh.1 - sh.2.1 * 65536) + assertZero (r.out1 - sh.2.2.1 - sh.2.2.2 * 65536) + assertZero (r.direction * (1 - r.direction)) + assertZero (r.signed * (1 - r.signed)) + assertZero (r.wordInstr * (1 - r.wordInstr)) + assertZero (r.zbs * (1 - r.zbs)) + assertZero (r.mu * (1 - r.mu)) + assertZero ((1 - r.signed) * r.isNegative) + -- interactions, in the order of `bus_interactions` + Bitwise.Msb16.pullIf r.signed (r.in3, r.isNegative) + Bitwise.ByteAlu.pullIf left ⟨0, r.shiftAmount, 15, r.bitShift⟩ + Bitwise.ByteAlu.pullIf right ⟨0, 256 - 16 * r.zbs - r.shiftAmount, 15, r.bitShift⟩ + Bitwise.Zero.pullIf r.mu (r.bitShift, r.zbs) + Bitwise.Hwsl.pullIf (1 - r.zbs) ⟨r.in0, r.bitShift, r.x0, r.y0⟩ + Bitwise.Hwsl.pullIf (1 - r.zbs) ⟨r.in1, r.bitShift, r.x1, r.y1⟩ + Bitwise.Hwsl.pullIf (1 - r.zbs) ⟨r.in2, r.bitShift, r.x2, r.y2⟩ + Bitwise.Hwsl.pullIf (1 - r.zbs) ⟨r.in3, r.bitShift, r.x3, r.y3⟩ + Bitwise.Hwsl.pullIf (1 - r.zbs) ⟨extension, r.bitShift, r.x4, extension - r.x4⟩ + Bitwise.ByteAlu.pullIf r.mu + ⟨0, r.shiftAmount, 48 - 32 * r.wordInstr, 48 - 48 * r.ls0 - 32 * r.ls1 - 16 * r.ls2⟩ + Alu.channel.pushIf r.mu + ⟨r.in0 + 65536 * r.in1, r.in2 + 65536 * r.in3, + r.shiftAmount + 256 * r.shiftB1 + 65536 * r.shiftH1, r.shiftHigh, + 5 + r.wordInstr + 32 * r.signed + 64 * r.direction, r.out0, r.out1⟩ + Bitwise.AreBytes.pull (r.shiftAmount, r.shiftB1) + Bitwise.IsHalf.pullIf r.mu r.shiftH1 + Bitwise.IsHalf.pullIf r.mu r.in0 + Bitwise.IsHalf.pullIf r.mu r.in1 + Bitwise.IsHalf.pullIf r.mu r.in2 + Bitwise.IsHalf.pullIf r.mu r.in3 + +lemma eval_shiftedPoly_1 (env : Environment (F p)) + (mu d l0 l1 l2 e x0 x1 x2 x3 x4 y0 y1 y2 y3 : Expression (F p)) : + Expression.eval env (shiftedPoly mu d l0 l1 l2 e x0 x1 x2 x3 x4 y0 y1 y2 y3).1 + = (shiftedPoly (env mu) (env d) (env l0) (env l1) (env l2) (env e) (env x0) (env x1) (env x2) + (env x3) (env x4) (env y0) (env y1) (env y2) (env y3)).1 := by + simp only [shiftedPoly, circuit_norm] +lemma eval_shiftedPoly_2 (env : Environment (F p)) + (mu d l0 l1 l2 e x0 x1 x2 x3 x4 y0 y1 y2 y3 : Expression (F p)) : + Expression.eval env (shiftedPoly mu d l0 l1 l2 e x0 x1 x2 x3 x4 y0 y1 y2 y3).2.1 + = (shiftedPoly (env mu) (env d) (env l0) (env l1) (env l2) (env e) (env x0) (env x1) (env x2) + (env x3) (env x4) (env y0) (env y1) (env y2) (env y3)).2.1 := by + simp only [shiftedPoly, circuit_norm] +lemma eval_shiftedPoly_3 (env : Environment (F p)) + (mu d l0 l1 l2 e x0 x1 x2 x3 x4 y0 y1 y2 y3 : Expression (F p)) : + Expression.eval env (shiftedPoly mu d l0 l1 l2 e x0 x1 x2 x3 x4 y0 y1 y2 y3).2.2.1 + = (shiftedPoly (env mu) (env d) (env l0) (env l1) (env l2) (env e) (env x0) (env x1) (env x2) + (env x3) (env x4) (env y0) (env y1) (env y2) (env y3)).2.2.1 := by + simp only [shiftedPoly, circuit_norm] +lemma eval_shiftedPoly_4 (env : Environment (F p)) + (mu d l0 l1 l2 e x0 x1 x2 x3 x4 y0 y1 y2 y3 : Expression (F p)) : + Expression.eval env (shiftedPoly mu d l0 l1 l2 e x0 x1 x2 x3 x4 y0 y1 y2 y3).2.2.2 + = (shiftedPoly (env mu) (env d) (env l0) (env l1) (env l2) (env e) (env x0) (env x1) (env x2) + (env x3) (env x4) (env y0) (env y1) (env y2) (env y3)).2.2.2 := by + simp only [shiftedPoly, circuit_norm] + +/-- Over field values that are casts of naturals (with `μ = 1`), `shiftedPoly` is the cast of +`ShiftCore.shifted`. -/ +lemma shiftedPoly_cast {d l0 l1 l2 e x0 x1 x2 x3 x4 y0 y1 y2 y3 : ℕ} (hd : d ≤ 1) + (hl : l0 + l1 + l2 ≤ 1) : + let shF := shiftedPoly (1 : F p) (d : F p) (l0 : F p) (l1 : F p) (l2 : F p) (e : F p) + (x0 : F p) (x1 : F p) (x2 : F p) (x3 : F p) (x4 : F p) (y0 : F p) (y1 : F p) (y2 : F p) (y3 : F p) + let sh := ShiftCore.shifted d l0 l1 l2 e x0 x1 x2 x3 x4 y0 y1 y2 y3 + shF.1 = (sh.1 : F p) ∧ shF.2.1 = (sh.2.1 : F p) ∧ shF.2.2.1 = (sh.2.2.1 : F p) ∧ + shF.2.2.2 = (sh.2.2.2 : F p) := by + intro shF sh + have h1 : l0 ≤ 1 := by omega + have h2 : l1 ≤ 1 - l0 := by omega + have h3 : l2 ≤ 1 - l0 - l1 := by omega + simp only [shF, sh, shiftedPoly, ShiftCore.shifted] + push_cast [Nat.cast_sub hd, Nat.cast_sub h1, Nat.cast_sub h2, Nat.cast_sub h3] + refine ⟨by ring, by ring, by ring, by ring⟩ + +/-- What an active row establishes: `out` is `in` shifted by the low byte of the amount. -/ +def RowSpec (r : Row (F p)) : Prop := + r.mu = 1 → + r.out0.val < 2^32 ∧ r.out1.val < 2^32 ∧ + r.out0.val + 2^32 * r.out1.val + = shiftResult r.wordInstr.val r.signed.val r.direction.val + (ShiftCore.limbs r.in0.val r.in1.val r.in2.val r.in3.val) r.shiftAmount.val + +/-- The `shifted` limbs of a row, on naturals. -/ +def shiftedOf (r : Row (F p)) : ℕ × ℕ × ℕ × ℕ := + ShiftCore.shifted r.direction.val r.ls0.val r.ls1.val r.ls2.val (65535 * r.isNegative.val) + r.x0.val r.x1.val r.x2.val r.x3.val r.x4.val r.y0.val r.y1.val r.y2.val r.y3.val + +/-- The honest prover's active row, as `generate_shift_trace` fills it (`compute_aux`). -/ +def Honest (r : Row (F p)) : Prop := + r.mu = 1 ∧ IsBool r.direction ∧ IsBool r.signed ∧ IsBool r.wordInstr ∧ + r.in0.val < 65536 ∧ r.in1.val < 65536 ∧ r.in2.val < 65536 ∧ r.in3.val < 65536 ∧ + r.shiftAmount.val < 256 ∧ r.shiftB1.val < 256 ∧ r.shiftH1.val < 65536 ∧ + r.isNegative.val = (if r.signed.val = 1 then r.in3.val / 32768 else 0) ∧ + r.bitShift.val = (if r.direction.val = 0 then r.shiftAmount.val % 16 + else (16 - r.shiftAmount.val % 16) % 16) ∧ + r.zbs = (if r.bitShift = 0 then 1 else 0) ∧ + (r.x0.val = if r.bitShift.val = 0 then (if r.direction.val = 0 then r.in0.val else 0) + else sll r.in0.val r.bitShift.val) ∧ + (r.x1.val = if r.bitShift.val = 0 then (if r.direction.val = 0 then r.in1.val else 0) + else sll r.in1.val r.bitShift.val) ∧ + (r.x2.val = if r.bitShift.val = 0 then (if r.direction.val = 0 then r.in2.val else 0) + else sll r.in2.val r.bitShift.val) ∧ + (r.x3.val = if r.bitShift.val = 0 then (if r.direction.val = 0 then r.in3.val else 0) + else sll r.in3.val r.bitShift.val) ∧ + (r.x4.val = if r.bitShift.val = 0 then 0 else sll (65535 * r.isNegative.val) r.bitShift.val) ∧ + (r.y0.val = if r.bitShift.val = 0 then (if r.direction.val = 0 then 0 else r.in0.val) + else sllc r.in0.val r.bitShift.val) ∧ + (r.y1.val = if r.bitShift.val = 0 then (if r.direction.val = 0 then 0 else r.in1.val) + else sllc r.in1.val r.bitShift.val) ∧ + (r.y2.val = if r.bitShift.val = 0 then (if r.direction.val = 0 then 0 else r.in2.val) + else sllc r.in2.val r.bitShift.val) ∧ + (r.y3.val = if r.bitShift.val = 0 then (if r.direction.val = 0 then 0 else r.in3.val) + else sllc r.in3.val r.bitShift.val) ∧ + -- limb_shift: one-hot at (shift / 16) mod (4 or 2) + (r.ls0.val = if r.shiftAmount.val / 16 % (4 - 2 * r.wordInstr.val) = 0 then 1 else 0) ∧ + (r.ls1.val = if r.shiftAmount.val / 16 % (4 - 2 * r.wordInstr.val) = 1 then 1 else 0) ∧ + (r.ls2.val = if r.shiftAmount.val / 16 % (4 - 2 * r.wordInstr.val) = 2 then 1 else 0) ∧ + -- out = shifted, as two words + r.out0.val = (shiftedOf r).1 + 65536 * (shiftedOf r).2.1 ∧ + r.out1.val = (shiftedOf r).2.2.1 + 65536 * (shiftedOf r).2.2.2 + +/-- A padding row: everything zero except `zbs = 1`. -/ +def Padding (r : Row (F p)) : Prop := + r.mu = 0 ∧ r.direction = 0 ∧ r.signed = 0 ∧ r.wordInstr = 0 ∧ r.zbs = 1 ∧ + r.isNegative = 0 ∧ r.x0 = 0 ∧ r.x1 = 0 ∧ r.x2 = 0 ∧ r.x3 = 0 ∧ r.x4 = 0 ∧ + r.y0 = 0 ∧ r.y1 = 0 ∧ r.y2 = 0 ∧ r.y3 = 0 ∧ r.ls0 = 0 ∧ r.ls1 = 0 ∧ r.ls2 = 0 ∧ + r.out0 = 0 ∧ r.out1 = 0 ∧ r.shiftAmount = 0 ∧ r.shiftB1 = 0 + +/-- `HWSL[e, b]`'s second output for an extension limb: `e − sll e b` is `sllc e b`. -/ +lemma ext_sllc {e b : ℕ} (he : e = 0 ∨ e = 65535) (hb : b < 16) : + sll e b ≤ e ∧ e - sll e b = sllc e b := by + rcases he with rfl | rfl <;> interval_cases b <;> simp [sll, sllc] + +/-- The `zbs` override of an `X` scratch cell holds on an honest row. -/ +lemma override_x {zbs x i d : F p} {b : ℕ} (hzb : IsBool zbs) (hdb : IsBool d) + (hiff : zbs = 1 → b = 0) + (hx : x.val = if b = 0 then (if d.val = 0 then i.val else 0) else sll i.val b) : + zbs * (x - i * (1 - d)) = 0 := by + rcases hzb with hz | hz + · rw [hz, zero_mul] + · rw [if_pos (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 + rw [ZMod.val_injective _ hx]; ring + · rw [hd] at hx ⊢ + simp only [val_one_eq, one_ne_zero, if_false] at hx + rw [(ZMod.val_eq_zero _).mp hx]; ring + +/-- The `zbs` override of a `Y` scratch cell holds on an honest row. -/ +lemma override_y {zbs y i d : F p} {b : ℕ} (hzb : IsBool zbs) (hdb : IsBool d) + (hiff : zbs = 1 → b = 0) + (hy : y.val = if b = 0 then (if d.val = 0 then 0 else i.val) else sllc i.val b) : + zbs * (y - i * d) = 0 := by + rcases hzb with hz | hz + · rw [hz, zero_mul] + · rw [if_pos (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 + rw [(ZMod.val_eq_zero _).mp hy]; ring + · rw [hd] at hy ⊢ + simp only [val_one_eq, one_ne_zero, if_false] at hy + rw [ZMod.val_injective _ hy]; ring + +@[reducible] +instance elaborated : ElaboratedCircuit (F p) Row unit main := by elaborate_circuit + +theorem soundness : + GeneralFormalCircuit.Soundness (F p) (Input := Row) (Output := unit) main (fun _ _ => True) + (fun r _ _ => RowSpec r) := by + circuit_proof_start [main, RowSpec, Alu.channel, Alu.Guarantees, Bitwise.isHalfTable, + Bitwise.msb16Table, Bitwise.byteAluTable, Bitwise.zeroTable, Bitwise.hwslTable, + Bitwise.areBytesTable] + obtain ⟨h_dm, h_zx0, h_zx1, h_zx2, h_zx3, h_zx4, h_zy0, h_zy1, h_zy2, h_zy3, + h_ls0, h_ls1, h_ls2, h_ls3, h_out0, h_out1, h_dir, h_sg, h_w, h_zbs, h_mu, h_neg, + h_msb, h_balL, h_balR, h_zero, h_hw0, h_hw1, h_hw2, h_hw3, h_hw4, h_lsb, + h_ab, h_h1, h_in0, h_in1, h_in2, h_in3⟩ := h_holds + have hdb := isBool_of_mul_one_sub h_dir + have hsb := isBool_of_mul_one_sub h_sg + have hwb := isBool_of_mul_one_sub h_w + have hzb := isBool_of_mul_one_sub h_zbs + have hmb := isBool_of_mul_one_sub h_mu + have hl0b := isBool_of_mul_one_sub h_ls0 + have hl1b := isBool_of_mul_one_sub h_ls1 + have hl2b := isBool_of_mul_one_sub h_ls2 + have hl3b := isBool_of_mul_one_sub h_ls3 + have hleft : IsBool (input_mu - input_direction) := by + rcases hmb with h | h <;> rcases hdb with h' | h' <;> simp_all [IsBool] + have hzb' : IsBool (1 - input_zbs) := by + rcases hzb with h | h <;> simp [h, IsBool] + rcases hmb with hmu0 | hmu1 + · -- μ = 0: nothing is required of the row + rw [hmu0] at hleft ⊢ + refine ⟨fun h => absurd h (by norm_num), ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, + ?_, ?_⟩ + 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) + subst hmu1 + -- the facts every active row has + have hd2 := IsBool.val_lt_two hdb + have hs2 := IsBool.val_lt_two hsb + have hw2 := IsBool.val_lt_two hwb + have hz2 := IsBool.val_lt_two hzb + have hl0 := IsBool.val_lt_two hl0b + have hl1 := IsBool.val_lt_two hl1b + have hl2 := IsBool.val_lt_two hl2b + have honehot := onehot_of_isBool hl0b hl1b hl2b hl3b + obtain ⟨hsA, hB1⟩ := h_ab + obtain ⟨-, hzbs_eq⟩ := h_zero rfl + have hH1 := h_h1 rfl + have hi0 := h_in0 rfl + have hi1 := h_in1 rfl + have hi2 := h_in2 rfl + have hi3 := h_in3 rfl + have h15 : (15 : F p).val = 15 := val_ofNat 15 (by norm_num) + have h02ne : (0 : F p) ≠ 2 := by + intro h + have := congrArg ZMod.val h + rw [ZMod.val_zero, val_ofNat 2 (by norm_num)] at this + omega + -- 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] + 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] + 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] + 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 + rcases hzb with hz0 | hz1 + · rw [hz0] at hx hand + simp only [mul_zero, sub_zero] at hx hand + rw [show (256 : F p) = ((256 : ℕ) : F p) by norm_num] at hx hand + obtain ⟨hle, hval⟩ := val_sub_of_val_lt (by norm_num) (by omega) (lt_trans hx (by norm_num)) + rw [hval] at hand + omega + · rw [hz1] at hx hand + rw [show (256 : F p) - 16 * 1 = ((240 : ℕ) : F p) by norm_num] at hx hand + obtain ⟨hle, hval⟩ := val_sub_of_val_lt (by norm_num) (by omega) (lt_trans hx (by norm_num)) + rw [hval] at hand + omega + · exact absurd h02 h02ne + -- the sign bit + 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] + have : input_isNegative = 0 := by simpa using h_neg + rw [this, ZMod.val_zero] + · rw [hs1]; simp only [val_one_eq, if_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 := + val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega) + -- the HWSL outputs, or their overrides when bit_shift = 0 + have hxy : (input_x0.val = if input_bitShift.val = 0 then (if input_direction.val = 0 then input_in0.val else 0) + else sll input_in0.val input_bitShift.val) ∧ + (input_x1.val = if input_bitShift.val = 0 then (if input_direction.val = 0 then input_in1.val else 0) + else sll input_in1.val input_bitShift.val) ∧ + (input_x2.val = if input_bitShift.val = 0 then (if input_direction.val = 0 then input_in2.val else 0) + else sll input_in2.val input_bitShift.val) ∧ + (input_x3.val = if input_bitShift.val = 0 then (if input_direction.val = 0 then input_in3.val else 0) + else sll input_in3.val input_bitShift.val) ∧ + (input_x4.val = if input_bitShift.val = 0 then 0 + else sll (65535 * input_isNegative.val) input_bitShift.val) ∧ + (input_y0.val = if input_bitShift.val = 0 then (if input_direction.val = 0 then 0 else input_in0.val) + else sllc input_in0.val input_bitShift.val) ∧ + (input_y1.val = if input_bitShift.val = 0 then (if input_direction.val = 0 then 0 else input_in1.val) + else sllc input_in1.val input_bitShift.val) ∧ + (input_y2.val = if input_bitShift.val = 0 then (if input_direction.val = 0 then 0 else input_in2.val) + else sllc input_in2.val input_bitShift.val) ∧ + (input_y3.val = if input_bitShift.val = 0 then (if input_direction.val = 0 then 0 else input_in3.val) + else sllc input_in3.val input_bitShift.val) := by + rcases hzb with hz0 | hz1 + · -- bit_shift ≠ 0: the lookups fix X and Y + have hbne : input_bitShift.val ≠ 0 := by + intro h; have := hzb_iff.mpr h; rw [hz0, ZMod.val_zero] at this; omega + obtain ⟨-, -, hx0v, hy0v⟩ := h_hw0 (by rw [hz0]; norm_num) + obtain ⟨-, -, hx1v, hy1v⟩ := h_hw1 (by rw [hz0]; norm_num) + obtain ⟨-, -, hx2v, hy2v⟩ := h_hw2 (by rw [hz0]; norm_num) + obtain ⟨-, -, hx3v, hy3v⟩ := h_hw3 (by rw [hz0]; norm_num) + obtain ⟨-, -, hx4v, -⟩ := h_hw4 (by rw [hz0]; norm_num) + rw [hext] at hx4v + simp only [if_neg hbne] + exact ⟨hx0v, hx1v, hx2v, hx3v, hx4v, hy0v, hy1v, hy2v, hy3v⟩ + · -- bit_shift = 0: the overrides + 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] + 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, + 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, + 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 + have hL : 16 * (input_ls1.val + 2 * input_ls2.val + + 3 * (1 - input_ls0.val - input_ls1.val - input_ls2.val)) + = input_shiftAmount.val &&& (48 - 32 * input_wordInstr.val) := by + obtain ⟨-, -, hand | ⟨h02, -⟩⟩ := h_lsb rfl + · have hmask : (48 - 32 * input_wordInstr).val = 48 - 32 * input_wordInstr.val := by + rcases hwb with hw0 | hw1 + · rw [hw0]; simp only [mul_zero, sub_zero, ZMod.val_zero]; exact val_ofNat 48 (by norm_num) + · rw [hw1]; norm_num; exact val_ofNat 16 (by norm_num) + have henc : (48 - 48 * input_ls0 - 32 * input_ls1 - 16 * input_ls2).val + = 48 - 48 * input_ls0.val - 32 * input_ls1.val - 16 * input_ls2.val := by + rcases hl0b with h0 | h0 <;> rcases hl1b with h1 | h1 <;> rcases hl2b with h2 | h2 <;> + · rw [h0, h1, h2] + simp only [h0, h1, h2, ZMod.val_zero, val_one_eq] at honehot ⊢ + first + | omega + | (norm_num; done) + | (norm_num; exact val_ofNat _ (by norm_num)) + rw [henc, hmask] at hand + omega + · exact absurd h02 h02ne + -- the arithmetic + have hcore := ShiftCore.main hd2 hs2 hw2 hsA hi0 hi1 hi2 hi3 hl0 hl1 hl2 honehot hL hb hn + hx0 hx1 hx2 hx3 hx4 hy0 hy1 hy2 hy3 + simp only at hcore + obtain ⟨hsh0, hsh1, hsh2, hsh3, hres⟩ := hcore + -- the output words + have hcast := shiftedPoly_cast (e := 65535 * input_isNegative.val) + (x0 := input_x0.val) (x1 := input_x1.val) (x2 := input_x2.val) (x3 := input_x3.val) + (x4 := input_x4.val) (y0 := input_y0.val) (y1 := input_y1.val) (y2 := input_y2.val) + (y3 := input_y3.val) (by omega : input_direction.val ≤ 1) honehot + simp only at hcast + obtain ⟨hc1, hc2, hc3, hc4⟩ := hcast + rw [eval_shiftedPoly_1, eval_shiftedPoly_2] at h_out0 + rw [eval_shiftedPoly_3, eval_shiftedPoly_4] at h_out1 + simp only [circuit_norm, h_input] at h_out0 h_out1 + rw [← ZMod.natCast_zmod_val input_direction, ← ZMod.natCast_zmod_val input_ls0, + ← ZMod.natCast_zmod_val input_ls1, ← ZMod.natCast_zmod_val input_ls2, + ← ZMod.natCast_zmod_val input_isNegative, ← ZMod.natCast_zmod_val input_x0, + ← ZMod.natCast_zmod_val input_x1, ← ZMod.natCast_zmod_val input_x2, + ← ZMod.natCast_zmod_val input_x3, ← ZMod.natCast_zmod_val input_x4, + ← ZMod.natCast_zmod_val input_y0, ← ZMod.natCast_zmod_val input_y1, + ← ZMod.natCast_zmod_val input_y2, ← ZMod.natCast_zmod_val input_y3, + show (65535 : F p) * ((input_isNegative.val : ℕ) : F p) + = ((65535 * input_isNegative.val : ℕ) : F p) by push_cast; ring] at h_out0 h_out1 + rw [hc1, hc2] at h_out0 + rw [hc3, hc4] at h_out1 + have hout0 : input_out0.val = (ShiftCore.shifted input_direction.val input_ls0.val input_ls1.val + input_ls2.val (65535 * input_isNegative.val) input_x0.val input_x1.val input_x2.val + input_x3.val input_x4.val input_y0.val input_y1.val input_y2.val input_y3.val).1 + + 65536 * (ShiftCore.shifted input_direction.val input_ls0.val input_ls1.val + input_ls2.val (65535 * input_isNegative.val) input_x0.val input_x1.val input_x2.val + input_x3.val input_x4.val input_y0.val input_y1.val input_y2.val input_y3.val).2.1 := + val_eq_of_eq_natCast (by push_cast; linear_combination h_out0) (by omega) + have hout1 : input_out1.val = (ShiftCore.shifted input_direction.val input_ls0.val input_ls1.val + input_ls2.val (65535 * input_isNegative.val) input_x0.val input_x1.val input_x2.val + input_x3.val input_x4.val input_y0.val input_y1.val input_y2.val input_y3.val).2.2.1 + + 65536 * (ShiftCore.shifted input_direction.val input_ls0.val input_ls1.val + input_ls2.val (65535 * input_isNegative.val) input_x0.val input_x1.val input_x2.val + input_x3.val input_x4.val input_y0.val input_y1.val input_y2.val input_y3.val).2.2.2 := + val_eq_of_eq_natCast (by push_cast; linear_combination h_out1) (by omega) + have key : input_out0.val < 2^32 ∧ input_out1.val < 2^32 ∧ + input_out0.val + 2^32 * input_out1.val + = shiftResult input_wordInstr.val input_signed.val input_direction.val + (limbs input_in0.val input_in1.val input_in2.val input_in3.val) + input_shiftAmount.val := by + refine ⟨by omega, by omega, ?_⟩ + rw [← hres, hout0, hout1] + simp only [limbs] + omega + -- the row spec and the bus requirements + refine ⟨fun _ => key, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ + 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) + | skip + -- what remains is the ALU push + intro _ _ hin1lo hin1hi hin2lo hin2hi + have hflags_ne : ∀ (w s d : ℕ), w < 2 → s < 2 → d < 2 → + 5 + input_wordInstr + 32 * input_signed + 64 * input_direction + = ((Alu.opselSHIFT + w + 32 * s + 64 * d : ℕ) : F p) → + input_wordInstr.val = w ∧ input_signed.val = s ∧ input_direction.val = d := by + intro w s d hw hs hd hflags + have h1 : ((5 + input_wordInstr.val + 32 * input_signed.val + 64 * input_direction.val : ℕ) : F p) + = ((Alu.opselSHIFT + w + 32 * s + 64 * d : ℕ) : F p) := by + rw [← hflags]; push_cast; simp only [ZMod.natCast_zmod_val] + have h2 := natCast_inj_of_lt (lt_p_of_lt_two_pow_40 (by omega)) + (lt_p_of_lt_two_pow_40 (by simp only [Alu.opselSHIFT]; omega)) h1 + simp only [Alu.opselSHIFT] at h2 + omega + refine ⟨?_, ?_, ?_⟩ + · -- not LT: 5 + w + 32 s + 64 d ≠ 4 + 32 s' + 64 i (mod 32) + intro s i hs hi hflags + exfalso + have h1 : ((5 + input_wordInstr.val + 32 * input_signed.val + 64 * input_direction.val : ℕ) : F p) + = ((Alu.opselLT + 32 * s + 64 * i : ℕ) : F p) := by + rw [← hflags]; push_cast; simp only [ZMod.natCast_zmod_val] + have h2 := natCast_inj_of_lt (lt_p_of_lt_two_pow_40 (by omega)) + (lt_p_of_lt_two_pow_40 (by simp only [Alu.opselLT]; omega)) h1 + simp only [Alu.opselLT] at h2 + omega + · -- not EQ + intro i hi hflags + exfalso + have h1 : ((5 + input_wordInstr.val + 32 * input_signed.val + 64 * input_direction.val : ℕ) : F p) + = ((Alu.opselEQ + 64 * i : ℕ) : F p) := by + rw [← hflags]; push_cast; simp only [ZMod.natCast_zmod_val] + have h2 := natCast_inj_of_lt (lt_p_of_lt_two_pow_40 (by omega)) + (lt_p_of_lt_two_pow_40 (by simp only [Alu.opselEQ]; omega)) h1 + simp only [Alu.opselEQ] at h2 + omega + · intro w s d hw hs hd hflags + obtain ⟨rfl, rfl, rfl⟩ := hflags_ne w s d hw hs hd hflags + have hv1 : (input_in0 + 65536 * input_in1).val = input_in0.val + 65536 * input_in1.val := + val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega) + have hv2 : (input_in2 + 65536 * input_in3).val = input_in2.val + 65536 * input_in3.val := + val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega) + have hin1 : dword (input_in0 + 65536 * input_in1) (input_in2 + 65536 * input_in3) + = limbs input_in0.val input_in1.val input_in2.val input_in3.val := by + simp only [dword, limbs, hv1, hv2]; omega + have hv3 : (input_shiftAmount + 256 * input_shiftB1 + 65536 * input_shiftH1).val + = input_shiftAmount.val + 256 * input_shiftB1.val + 65536 * input_shiftH1.val := + val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega) + have hin2 : (input_shiftAmount + 256 * input_shiftB1 + 65536 * input_shiftH1).val % 256 + = input_shiftAmount.val := by + rw [hv3]; omega + rw [hin1, hin2] + exact ⟨key.1, key.2.1, key.2.2⟩ + + +theorem completeness : + GeneralFormalCircuit.Completeness (F p) (Input := Row) (Output := unit) main + (fun r _ _ => Honest r ∨ Padding r) (fun _ _ _ => True) := by + circuit_proof_start [main, Alu.channel, Alu.Guarantees, Bitwise.isHalfTable, Bitwise.msb16Table, + Bitwise.byteAluTable, Bitwise.zeroTable, Bitwise.hwslTable, Bitwise.areBytesTable, Honest, + Padding, shiftedOf] + rcases h_assumptions with + ⟨hmu, hdb, hsb, hwb, hi0, hi1, hi2, hi3, hsA, hB1, hH1, hn, hb, hzbs, hx0, hx1, hx2, hx3, hx4, + hy0, hy1, hy2, hy3, hl0, hl1, hl2, hout0, hout1⟩ | + ⟨hmu, hd, hs, hw, hz, hneg, hx0, hx1, hx2, hx3, hx4, hy0, hy1, hy2, hy3, hl0, hl1, hl2, + hout0, hout1, hsA, hB1⟩ + · -- an active row + subst hmu + have hd2 := IsBool.val_lt_two hdb + have hs2 := IsBool.val_lt_two hsb + have hw2 := IsBool.val_lt_two hwb + have h15 : (15 : F p).val = 15 := val_ofNat 15 (by norm_num) + have hn2 : input_isNegative.val < 2 := by rw [hn]; split_ifs <;> omega + have hb16 : input_bitShift.val < 16 := by rw [hb]; split_ifs <;> omega + have hL4 : input_shiftAmount.val / 16 % (4 - 2 * input_wordInstr.val) < 4 := by + rcases (by omega : input_wordInstr.val = 0 ∨ input_wordInstr.val = 1) with h | h <;> + rw [h] <;> omega + -- the bits as field values + have hl0b : IsBool input_ls0 := isBool_of_val_lt_two (by rw [hl0]; split_ifs <;> omega) + have hl1b : IsBool input_ls1 := isBool_of_val_lt_two (by rw [hl1]; split_ifs <;> omega) + have hl2b : IsBool input_ls2 := isBool_of_val_lt_two (by rw [hl2]; split_ifs <;> omega) + have honehot : input_ls0.val + input_ls1.val + input_ls2.val ≤ 1 := by + rw [hl0, hl1, hl2]; split_ifs <;> omega + have hnb : IsBool input_isNegative := isBool_of_val_lt_two hn2 + have hzb : IsBool input_zbs := by rw [hzbs]; split_ifs <;> simp [IsBool] + 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] + have hne : input_bitShift.val ≠ 0 := by rwa [Ne, ZMod.val_eq_zero] + constructor + · intro h; exact absurd h zero_ne_one + · intro h; exact absurd h hne + have hext : (65535 * input_isNegative).val = 65535 * input_isNegative.val := + val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega) + -- the arithmetic core and the output words + have hL : 16 * (input_ls1.val + 2 * input_ls2.val + + 3 * (1 - input_ls0.val - input_ls1.val - input_ls2.val)) + = input_shiftAmount.val &&& (48 - 32 * input_wordInstr.val) := by + rcases (by omega : input_wordInstr.val = 0 ∨ input_wordInstr.val = 1) with h | h + · rw [h] at hl0 hl1 hl2 ⊢; rw [ShiftCore.and48 hsA, hl0, hl1, hl2]; split_ifs <;> omega + · rw [h] at hl0 hl1 hl2 ⊢; rw [ShiftCore.and16 hsA, hl0, hl1, hl2]; split_ifs <;> omega + have hcore := ShiftCore.main hd2 hs2 hw2 hsA hi0 hi1 hi2 hi3 + (by rw [hl0]; split_ifs <;> omega) (by rw [hl1]; split_ifs <;> omega) + (by rw [hl2]; split_ifs <;> omega) honehot hL hb hn hx0 hx1 hx2 hx3 hx4 hy0 hy1 hy2 hy3 + simp only at hcore + obtain ⟨hsh0, hsh1, hsh2, hsh3, -⟩ := hcore + have hcast := shiftedPoly_cast (e := 65535 * input_isNegative.val) + (x0 := input_x0.val) (x1 := input_x1.val) (x2 := input_x2.val) (x3 := input_x3.val) + (x4 := input_x4.val) (y0 := input_y0.val) (y1 := input_y1.val) (y2 := input_y2.val) + (y3 := input_y3.val) (by omega : input_direction.val ≤ 1) honehot + simp only at hcast + obtain ⟨hc1, hc2, hc3, hc4⟩ := hcast + have hout0' : input_out0 = (((ShiftCore.shifted input_direction.val input_ls0.val input_ls1.val + input_ls2.val (65535 * input_isNegative.val) input_x0.val input_x1.val input_x2.val + input_x3.val input_x4.val input_y0.val input_y1.val input_y2.val input_y3.val).1 + + 65536 * (ShiftCore.shifted input_direction.val input_ls0.val input_ls1.val + input_ls2.val (65535 * input_isNegative.val) input_x0.val input_x1.val input_x2.val + input_x3.val input_x4.val input_y0.val input_y1.val input_y2.val input_y3.val).2.1 : ℕ) : F p) := by + rw [← hout0, ZMod.natCast_zmod_val] + have hout1' : input_out1 = (((ShiftCore.shifted input_direction.val input_ls0.val input_ls1.val + input_ls2.val (65535 * input_isNegative.val) input_x0.val input_x1.val input_x2.val + input_x3.val input_x4.val input_y0.val input_y1.val input_y2.val input_y3.val).2.2.1 + + 65536 * (ShiftCore.shifted input_direction.val input_ls0.val input_ls1.val + input_ls2.val (65535 * input_isNegative.val) input_x0.val input_x1.val input_x2.val + input_x3.val input_x4.val input_y0.val input_y1.val input_y2.val input_y3.val).2.2.2 : ℕ) : F p) := by + rw [← hout1, ZMod.natCast_zmod_val] + -- field forms of the naturals + have hdc := (ZMod.natCast_zmod_val input_direction).symm + have hl0c := (ZMod.natCast_zmod_val input_ls0).symm + have hl1c := (ZMod.natCast_zmod_val input_ls1).symm + have hl2c := (ZMod.natCast_zmod_val input_ls2).symm + have hnc := (ZMod.natCast_zmod_val input_isNegative).symm + have hx0c := (ZMod.natCast_zmod_val input_x0).symm + have hx1c := (ZMod.natCast_zmod_val input_x1).symm + have hx2c := (ZMod.natCast_zmod_val input_x2).symm + have hx3c := (ZMod.natCast_zmod_val input_x3).symm + have hx4c := (ZMod.natCast_zmod_val input_x4).symm + have hy0c := (ZMod.natCast_zmod_val input_y0).symm + have hy1c := (ZMod.natCast_zmod_val input_y1).symm + have hy2c := (ZMod.natCast_zmod_val input_y2).symm + have hy3c := (ZMod.natCast_zmod_val input_y3).symm + have hiff : input_zbs = 1 → input_bitShift.val = 0 := hzb_iff.mp + have hl3b : IsBool (1 - input_ls0 - input_ls1 - input_ls2) := by + rcases hl0b with h0 | h0 <;> rcases hl1b with h1 | h1 <;> rcases hl2b with h2 | h2 <;> + simp only [h0, h1, h2, ZMod.val_zero, val_one_eq] at honehot ⊢ <;> + first | omega | norm_num [IsBool] + refine ⟨by simp, override_x hzb hdb hiff hx0, override_x hzb hdb hiff hx1, + override_x hzb hdb hiff hx2, override_x hzb hdb hiff hx3, ?_, + override_y hzb hdb hiff hy0, override_y hzb hdb hiff hy1, override_y hzb hdb hiff hy2, + override_y hzb hdb hiff hy3, isBool_mul_one_sub hl0b, + isBool_mul_one_sub hl1b, isBool_mul_one_sub hl2b, isBool_mul_one_sub hl3b, ?_, ?_, + isBool_mul_one_sub hdb, isBool_mul_one_sub hsb, isBool_mul_one_sub hwb, + isBool_mul_one_sub hzb, by simp, ?_, + ?_, ?_, ?_, fun _ => ⟨by omega, hzbs⟩, ?_, ?_, ?_, ?_, ?_, ?_, ⟨hsA, hB1⟩, fun _ => hH1, + fun _ => hi0, fun _ => hi1, fun _ => hi2, fun _ => hi3⟩ + · -- zbs · X[4] = 0 + rcases hzb with hz | hz + · rw [hz, zero_mul] + · rw [if_pos (hiff hz)] at hx4 + rw [hz, one_mul, (ZMod.val_eq_zero _).mp hx4] + · -- out[0] + rw [eval_shiftedPoly_1, eval_shiftedPoly_2] + simp only [circuit_norm, h_input] + rw [hdc, hl0c, hl1c, hl2c, hnc, hx0c, hx1c, hx2c, hx3c, hx4c, hy0c, hy1c, hy2c, hy3c, + show (65535 : F p) * ((input_isNegative.val : ℕ) : F p) + = ((65535 * input_isNegative.val : ℕ) : F p) by push_cast; ring, hc1, hc2, hout0'] + push_cast; ring + · -- out[1] + rw [eval_shiftedPoly_3, eval_shiftedPoly_4] + simp only [circuit_norm, h_input] + rw [hdc, hl0c, hl1c, hl2c, hnc, hx0c, hx1c, hx2c, hx3c, hx4c, hy0c, hy1c, hy2c, hy3c, + show (65535 : F p) * ((input_isNegative.val : ℕ) : F p) + = ((65535 * input_isNegative.val : ℕ) : F p) by push_cast; ring, hc3, hc4, hout1'] + push_cast; ring + · -- (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 + rw [(ZMod.val_eq_zero _).mp hn]; ring + · rw [hs]; ring + · -- MSB16[in[3]] when signed + intro h + have hs1 : input_signed = 1 := neg_inj.mp 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 + 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 + 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 + rw [hzbs, if_pos ((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 + rw [hz, Nat.cast_sub (by omega)]; push_cast + rw [ZMod.natCast_zmod_val input_shiftAmount]; ring + rw [hcast, val_natCast_of_lt_two_pow_40 (by omega), h15, ShiftCore.and15, hb] + exact ⟨by omega, by norm_num, Or.inl (by omega)⟩ + · have hb0 : input_bitShift.val = 0 := hiff hz + have hle : input_shiftAmount.val ≤ 240 := by omega + have hcast : (256 : F p) - 16 * input_zbs - input_shiftAmount + = ((240 - input_shiftAmount.val : ℕ) : F p) := by + rw [hz, Nat.cast_sub hle]; push_cast + rw [ZMod.natCast_zmod_val input_shiftAmount]; ring + rw [hcast, val_natCast_of_lt_two_pow_40 (by omega), h15, ShiftCore.and15, hb0] + exact ⟨by omega, by norm_num, Or.inl (by omega)⟩ + · -- HWSL[in[0], 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 hx0 hy0 + exact ⟨hi0, hb16, by rw [hx0]; simp [sll, hbne], by rw [hy0]; simp [sllc, hbne]⟩ + · 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 + exact ⟨hi1, hb16, by rw [hx1]; simp [sll, hbne], by rw [hy1]; simp [sllc, hbne]⟩ + · 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 + exact ⟨hi2, hb16, by rw [hx2]; simp [sll, hbne], by rw [hy2]; simp [sllc, hbne]⟩ + · 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 + exact ⟨hi3, hb16, by rw [hx3]; simp [sll, hbne], by rw [hy3]; simp [sllc, hbne]⟩ + · -- 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 + 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 + = 65535 * input_isNegative.val - input_x4.val := by + rw [← hx4] at hle + 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] + exact val_natCast_of_lt_two_pow_40 (by omega) + refine ⟨by rw [hext]; omega, hb16, ?_, ?_⟩ + · rw [hext, hx4]; try simp [sll, hbne] + · rw [hdiff, hext, hx4, hsub]; try simp [sllc, hbne] + · -- BYTE_ALU[AND, shift, mask] + intro _ + have hmask : (48 - 32 * input_wordInstr).val = 48 - 32 * input_wordInstr.val := by + rcases hwb with hw0 | hw0 + · rw [hw0]; simp only [mul_zero, sub_zero, ZMod.val_zero]; exact val_ofNat 48 (by norm_num) + · rw [hw0]; norm_num; exact val_ofNat 16 (by norm_num) + refine ⟨hsA, by rw [hmask]; omega, Or.inl ?_⟩ + rw [hmask] + have hand : input_shiftAmount.val &&& (48 - 32 * input_wordInstr.val) + = 16 * (input_shiftAmount.val / 16 % (4 - 2 * input_wordInstr.val)) := by + rcases (by omega : input_wordInstr.val = 0 ∨ input_wordInstr.val = 1) with h | h + · rw [h]; simpa using ShiftCore.and48 hsA + · rw [h]; simpa using ShiftCore.and16 hsA + rw [hand] + rw [eq_natCast_of_val hl0, eq_natCast_of_val hl1, eq_natCast_of_val hl2] + rcases (by omega : input_shiftAmount.val / 16 % (4 - 2 * input_wordInstr.val) = 0 ∨ + input_shiftAmount.val / 16 % (4 - 2 * input_wordInstr.val) = 1 ∨ + input_shiftAmount.val / 16 % (4 - 2 * input_wordInstr.val) = 2 ∨ + input_shiftAmount.val / 16 % (4 - 2 * input_wordInstr.val) = 3) with hLv | hLv | hLv | hLv + · rw [hLv]; norm_num + · rw [hLv]; norm_num; exact val_ofNat 16 (by norm_num) + · rw [hLv]; norm_num; exact val_ofNat 32 (by norm_num) + · rw [hLv]; norm_num; exact val_ofNat 48 (by norm_num) + · -- a padding row + subst hmu hd hs hw hz hneg hx0 hx1 hx2 hx3 hx4 hy0 hy1 hy2 hy3 hl0 hl1 hl2 hout0 hout1 hsA hB1 + refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> + · try simp only [eval_shiftedPoly_1, eval_shiftedPoly_2, eval_shiftedPoly_3, eval_shiftedPoly_4] + simp [circuit_norm, h_input, shiftedPoly] + + +def circuit : GeneralFormalCircuit (F p) Row unit where + main + elaborated + Spec r _ _ := RowSpec r + channelsWithRequirements := [Alu.channel.toRaw] + requirementsChannelsLawful input_var i₀ := by + obtain ⟨in0, in1, in2, in3, shiftAmount, direction, signed, wordInstr, out0, out1, isNegative, + bitShift, zbs, x0, x1, x2, x3, x4, y0, y1, y2, y3, ls0, ls1, ls2, mu, shiftB1, shiftH1, + shiftHigh⟩ := input_var + simp only [circuit_norm, main, Alu.channel, Bitwise.isHalfTable, Bitwise.msb16Table, + Bitwise.byteAluTable, Bitwise.zeroTable, Bitwise.hwslTable, Bitwise.areBytesTable] + constructor + · intro channel h; tauto + · intro env h + obtain ⟨h_dm, -, -, -, -, -, -, -, -, -, -, -, -, -, -, -, h_dir, h_sg, -, h_zbs, h_mu, -⟩ := h + have hdb := isBool_of_mul_one_sub h_dir + have hsb := isBool_of_mul_one_sub h_sg + have hzb := isBool_of_mul_one_sub h_zbs + have hmb := isBool_of_mul_one_sub h_mu + 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 + + soundness := soundness + ProverAssumptions r _ _ := Honest r ∨ Padding r + + completeness := completeness + +end LambdaVM.SHIFT diff --git a/formal/LambdaVM/Tables/ShiftCore.lean b/formal/LambdaVM/Tables/ShiftCore.lean new file mode 100644 index 000000000..02bbda8ad --- /dev/null +++ b/formal/LambdaVM/Tables/ShiftCore.lean @@ -0,0 +1,211 @@ +module + +public import LambdaVM.Buses.Alu + +@[expose] public section + +/-! +# The arithmetic of the SHIFT chip, on naturals + +`spec/shift.typ` shifts in two phases: by `bit_shift < 16` bits inside each 16-bit limb using +the `HWSL` lookup, then by whole limbs using the one-hot `limb_shift`. These lemmas prove that +the limb recombination the chip constrains equals the shift of the 64-bit value. +-/ + +namespace LambdaVM.ShiftCore +open Alu (shiftResult sra64) + +/-- `HWSL` as in BITWISE: `(h << z) mod 2^16` and `h >> (16 − z)`, with the `z = 0` convention. -/ +def sll (h z : ℕ) : ℕ := if z = 0 then h else (h <<< z) % 65536 +def sllc (h z : ℕ) : ℕ := if z = 0 then 0 else h >>> (16 - z) + +def limbs (a0 a1 a2 a3 : ℕ) : ℕ := a0 + 65536 * a1 + 2^32 * a2 + 2^48 * a3 + +theorem and15 (s : ℕ) : s &&& 15 = s % 16 := by + have := Nat.and_two_pow_sub_one_eq_mod s 4 + norm_num at this + exact this + +theorem and48 {s : ℕ} (hs : s < 256) : s &&& 48 = 16 * (s / 16 % 4) := by + interval_cases s <;> decide + +theorem and16 {s : ℕ} (hs : s < 256) : s &&& 16 = 16 * (s / 16 % 2) := by + interval_cases s <;> decide + +/-- Left shift: phase 1 (`bit_shift = b`) and phase 2 (`limb_shift = L`) together. -/ +theorem leftShift {i0 i1 i2 i3 b L : ℕ} + (h0 : i0 < 65536) (h1 : i1 < 65536) (h2 : i2 < 65536) (h3 : i3 < 65536) + (hb : b < 16) (hL : L < 4) : + let il0 := sll i0 b + let il1 := sll i1 b + sllc i0 b + let il2 := sll i2 b + sllc i1 b + let il3 := sll i3 b + sllc i2 b + let sh0 := if L = 0 then il0 else 0 + let sh1 := if L = 0 then il1 else if L = 1 then il0 else 0 + let sh2 := if L = 0 then il2 else if L = 1 then il1 else if L = 2 then il0 else 0 + let sh3 := if L = 0 then il3 else if L = 1 then il2 else if L = 2 then il1 else il0 + sh0 < 65536 ∧ sh1 < 65536 ∧ sh2 < 65536 ∧ sh3 < 65536 ∧ + limbs sh0 sh1 sh2 sh3 = (limbs i0 i1 i2 i3 <<< (16 * L + b)) % 2^64 := by + intro il0 il1 il2 il3 sh0 sh1 sh2 sh3 + simp only [il0, il1, il2, il3, sh0, sh1, sh2, sh3, limbs, sll, sllc, Nat.shiftLeft_eq, + Nat.shiftRight_eq_div_pow] + interval_cases b <;> interval_cases L <;> norm_num <;> omega + +/-- Right shift, phase 1: `bit_shift = b = (16 − r) mod 16` turns the limbs of `in` (plus one +extension limb `e` above) into the limbs of `in >> r`. -/ +theorem rightIntra {i0 i1 i2 i3 r b e : ℕ} + (h0 : i0 < 65536) (h1 : i1 < 65536) (h2 : i2 < 65536) (h3 : i3 < 65536) + (hr : r < 16) (hb : b = (16 - r) % 16) (he : e = 0 ∨ e = 65535) : + let xi (h : ℕ) := if b = 0 then 0 else sll h b + let yi (h : ℕ) := if b = 0 then h else sllc h b + let x4 := if b = 0 then 0 else sll e b + let ir0 := yi i0 + xi i1 + let ir1 := yi i1 + xi i2 + let ir2 := yi i2 + xi i3 + let ir3 := yi i3 + x4 + ir0 < 65536 ∧ ir1 < 65536 ∧ ir2 < 65536 ∧ ir3 < 65536 ∧ + limbs ir0 ir1 ir2 ir3 = ((limbs i0 i1 i2 i3 + e * 2^64) >>> r) % 2^64 := by + intro xi yi x4 ir0 ir1 ir2 ir3 + simp only [xi, yi, x4, ir0, ir1, ir2, ir3, limbs, sll, sllc, Nat.shiftLeft_eq, + Nat.shiftRight_eq_div_pow] + rcases he with rfl | rfl <;> interval_cases r <;> norm_num at hb <;> subst hb <;> norm_num <;> omega + +/-- Right shift, phase 2: `limb_shift = L` moves whole limbs, filling with `e`. -/ +theorem rightLimb {a0 a1 a2 a3 L e : ℕ} + (h0 : a0 < 65536) (h1 : a1 < 65536) (h2 : a2 < 65536) (h3 : a3 < 65536) + (hL : L < 4) (he : e = 0 ∨ e = 65535) : + let sh0 := if L = 0 then a0 else if L = 1 then a1 else if L = 2 then a2 else a3 + let sh1 := if L = 0 then a1 else if L = 1 then a2 else if L = 2 then a3 else e + let sh2 := if L = 0 then a2 else if L = 1 then a3 else e + let sh3 := if L = 0 then a3 else e + sh0 < 65536 ∧ sh1 < 65536 ∧ sh2 < 65536 ∧ sh3 < 65536 ∧ + limbs sh0 sh1 sh2 sh3 + = ((limbs a0 a1 a2 a3 + e * (2^64 + 2^80 + 2^96)) >>> (16 * L)) % 2^64 := by + intro sh0 sh1 sh2 sh3 + simp only [sh0, sh1, sh2, sh3, limbs, Nat.shiftRight_eq_div_pow] + rcases he with rfl | rfl <;> interval_cases L <;> norm_num <;> omega + +/-- The two phases compose into one shift of a 128-bit sign-extended value. -/ +theorem rightCompose {X r L e : ℕ} (hX : X < 2^64) (hr : r < 16) (hL : L < 4) + (he : e = 0 ∨ e = 65535) : + ((((X + e * 2^64) >>> r) % 2^64 + e * (2^64 + 2^80 + 2^96)) >>> (16 * L)) % 2^64 + = ((X + e * (2^64 + 2^80 + 2^96 + 2^112)) >>> (16 * L + r)) % 2^64 := by + simp only [Nat.shiftRight_eq_div_pow] + rcases he with rfl | rfl <;> interval_cases r <;> interval_cases L <;> norm_num <;> omega + +/-- The `shifted` limbs exactly as the row polynomial reads them, on naturals: +`d` is `direction`, `l0 l1 l2` the stored one-hot limbs, `e` the extension limb. -/ +def shifted (d l0 l1 l2 e x0 x1 x2 x3 x4 y0 y1 y2 y3 : ℕ) : ℕ × ℕ × ℕ × ℕ := + let l3 := 1 - l0 - l1 - l2 + let left := 1 - d + let right := d + let il0 := x0 + let il1 := x1 + y0 + let il2 := x2 + y1 + let il3 := x3 + y2 + let ir0 := y0 + x1 + let ir1 := y1 + x2 + let ir2 := y2 + x3 + let ir3 := y3 + x4 + (left * (l0 * il0) + right * (l0 * ir0 + l1 * ir1 + l2 * ir2 + l3 * ir3), + left * (l0 * il1 + l1 * il0) + right * (l0 * ir1 + l1 * ir2 + l2 * ir3 + e * l3), + left * (l0 * il2 + l1 * il1 + l2 * il0) + right * (l0 * ir2 + l1 * ir3 + e * (l2 + l3)), + left * (l0 * il3 + l1 * il2 + l2 * il1 + l3 * il0) + right * (l0 * ir3 + e * (l1 + l2 + l3))) + +/-- The chip's arithmetic: from the decoded `bit_shift`, the one-hot `limb_shift`, the sign bit +and the HWSL outputs (or their `zbs` overrides), the recombined limbs are the shift result. -/ +theorem main {d sg w s i0 i1 i2 i3 l0 l1 l2 b n x0 x1 x2 x3 x4 y0 y1 y2 y3 : ℕ} + (hd : d < 2) (hsg : sg < 2) (hw : w < 2) (hs : s < 256) + (h0 : i0 < 65536) (h1 : i1 < 65536) (h2 : i2 < 65536) (h3 : i3 < 65536) + (hl0 : l0 < 2) (hl1 : l1 < 2) (hl2 : l2 < 2) (hl : l0 + l1 + l2 ≤ 1) + (hL : 16 * (l1 + 2 * l2 + 3 * (1 - l0 - l1 - l2)) = s &&& (48 - 32 * w)) + (hb : b = if d = 0 then s % 16 else (16 - s % 16) % 16) + (hn : n = if sg = 1 then i3 / 32768 else 0) + (hx0 : x0 = if b = 0 then (if d = 0 then i0 else 0) else sll i0 b) + (hx1 : x1 = if b = 0 then (if d = 0 then i1 else 0) else sll i1 b) + (hx2 : x2 = if b = 0 then (if d = 0 then i2 else 0) else sll i2 b) + (hx3 : x3 = if b = 0 then (if d = 0 then i3 else 0) else sll i3 b) + (hx4 : x4 = if b = 0 then 0 else sll (65535 * n) b) + (hy0 : y0 = if b = 0 then (if d = 0 then 0 else i0) else sllc i0 b) + (hy1 : y1 = if b = 0 then (if d = 0 then 0 else i1) else sllc i1 b) + (hy2 : y2 = if b = 0 then (if d = 0 then 0 else i2) else sllc i2 b) + (hy3 : y3 = if b = 0 then (if d = 0 then 0 else i3) else sllc i3 b) : + let sh := shifted d l0 l1 l2 (65535 * n) x0 x1 x2 x3 x4 y0 y1 y2 y3 + sh.1 < 65536 ∧ sh.2.1 < 65536 ∧ sh.2.2.1 < 65536 ∧ sh.2.2.2 < 65536 ∧ + limbs sh.1 sh.2.1 sh.2.2.1 sh.2.2.2 = shiftResult w sg d (limbs i0 i1 i2 i3) s := by + intro sh + -- the one-hot index and the shift amount + have hmask : s &&& (48 - 32 * w) = 16 * (s / 16 % (4 - 2 * w)) := by + rcases (by omega : w = 0 ∨ w = 1) with rfl | rfl + · simpa using and48 hs + · simpa using and16 hs + rw [hmask] at hL + have hn2 : n < 2 := by rw [hn]; split_ifs <;> omega + have he : 65535 * n = 0 ∨ 65535 * n = 65535 := by omega + 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 + 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) + simp only at core + have hk : s % (if w = 1 then 32 else 64) = 16 * (s / 16 % (4 - 2 * w)) + s % 16 := by + rcases (by omega : w = 0 ∨ w = 1) with rfl | rfl <;> simp <;> omega + have hLv : s / 16 % (4 - 2 * w) = l1 + 2 * l2 + 3 * (1 - l0 - l1 - l2) := by omega + rcases (by omega : (l0 = 1 ∧ l1 = 0 ∧ l2 = 0) ∨ (l0 = 0 ∧ l1 = 1 ∧ l2 = 0) ∨ + (l0 = 0 ∧ l1 = 0 ∧ l2 = 1) ∨ (l0 = 0 ∧ l1 = 0 ∧ l2 = 0)) with + ⟨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] + 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 + 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 + obtain ⟨hr0, hr1, hr2, hr3, hir⟩ := p1 + have p2 := rightLimb hr0 hr1 hr2 hr3 (L := l1 + 2 * l2 + 3 * (1 - l0 - l1 - l2)) (by omega) he + simp only at p2 + obtain ⟨hs0, hs1, hs2, hs3, hsh⟩ := p2 + rw [hir, rightCompose hX hr (by omega) he] at hsh + have hk : s % (if w = 1 then 32 else 64) = 16 * (s / 16 % (4 - 2 * w)) + s % 16 := by + rcases (by omega : w = 0 ∨ w = 1) with rfl | rfl <;> simp <;> omega + -- the result as the shift of the sign-extended value + 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] + 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 ⊢ + 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 ⊢ + 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 [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] + norm_num + rw [hres] + have hLv : s / 16 % (4 - 2 * w) = l1 + 2 * l2 + 3 * (1 - l0 - l1 - l2) := by omega + rw [hLv] + rcases (by omega : (l0 = 1 ∧ l1 = 0 ∧ l2 = 0) ∨ (l0 = 0 ∧ l1 = 1 ∧ l2 = 0) ∨ + (l0 = 0 ∧ l1 = 0 ∧ l2 = 1) ∨ (l0 = 0 ∧ l1 = 0 ∧ l2 = 0)) with + ⟨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 hs0 hs1 hs2 hs3 hsh + refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;> + first | (norm_num; done) | (norm_num; assumption) + +end LambdaVM.ShiftCore diff --git a/formal/LambdaVM/Templates/IsBit.lean b/formal/LambdaVM/Templates/IsBit.lean new file mode 100644 index 000000000..0aa545502 --- /dev/null +++ b/formal/LambdaVM/Templates/IsBit.lean @@ -0,0 +1,45 @@ +module + +public import LambdaVM.Field +public import Clean.Gadgets.Boolean + +@[expose] public section + +/-! +# IS_BIT (spec/is_bit.typ) + +Constraint template: when `cond ≠ 0`, `X` must lie in `{0, 1}`. +Single constraint: `cond · X · (1 − X) = 0`. +-/ + +namespace LambdaVM.IsBit + +structure Inputs (F : Type) where + cond : F + x : F +deriving ProvableStruct + +def main (inputs : Var Inputs (F p)) : Circuit (F p) Unit := + assertZero (inputs.cond * inputs.x * (1 - inputs.x)) + +def circuit : FormalAssertion (F p) Inputs where + main + + Spec := fun { cond, x } => cond ≠ 0 → IsBool x + + soundness := by + circuit_proof_start + intro h_cond + simp only [mul_eq_zero, sub_eq_zero] at h_holds + rcases h_holds with (h | h) | h + · exact absurd h h_cond + · exact Or.inl h + · exact Or.inr h.symm + + completeness := by + circuit_proof_start + by_cases h_cond : input_cond = 0 + · simp [h_cond] + · rcases h_spec h_cond with h | h <;> simp [h] + +end LambdaVM.IsBit diff --git a/formal/LambdaVM/Templates/IsByte.lean b/formal/LambdaVM/Templates/IsByte.lean new file mode 100644 index 000000000..9d23fa29c --- /dev/null +++ b/formal/LambdaVM/Templates/IsByte.lean @@ -0,0 +1,89 @@ +module + +public import LambdaVM.Tables.Bitwise + +@[expose] public section + +/-! +# IS_BYTE / ARE_BYTES (spec/is_byte.typ) + +`IS_BYTE` is one interaction `ARE_BYTES[0, X]` with multiplicity `cond`; +`ARE_BYTES` is the unconditional two-byte form (the CPU sends it on every row). +Both are macros expanded inline in the chips that use them: `cond` is a flag that the chip +itself constrains to be boolean, and a conditional interaction needs that constraint in the +same circuit to be lawful. +-/ + +namespace LambdaVM + +open Bitwise (AreBytes areBytesTable) + +/-- `ARE_BYTES`: both `x` and `y` are bytes. -/ +@[circuit_norm] +def areBytes (x y : Expression (F p)) : Circuit (F p) Unit := + AreBytes.pull (x, y) + +/-- `IS_BYTE`: `x` is a byte whenever `cond = 1`. -/ +@[circuit_norm] +def isByte (cond x : Expression (F p)) : Circuit (F p) Unit := + AreBytes.pullIf cond (0, x) + +-- Circuit inference does not unfold user wrappers; bridge each one to its body. +instance (x y : Expression (F p)) : ExplicitCircuit (areBytes x y) := + .of_eq (circuit' := AreBytes.pull (x, y)) rfl (by infer_explicit_circuit) +instance (cond x : Expression (F p)) : ExplicitCircuit (isByte cond x) := + .of_eq (circuit' := AreBytes.pullIf cond (0, x)) rfl (by infer_explicit_circuit) + +/-! The two templates as stand-alone assertions, to pin down their meaning. -/ + +namespace AreBytesCheck + +def circuit : FormalAssertion (F p) fieldPair where + main input := do areBytes input.1 input.2 + Spec | (x, y) => x.val < 256 ∧ y.val < 256 + soundness := by + circuit_proof_start [areBytes, areBytesTable] + exact h_holds + completeness := by + circuit_proof_start [areBytes, areBytesTable] + exact h_spec + +end AreBytesCheck + +namespace IsByteCheck + +structure Inputs (F : Type) where + cond : F + x : F +deriving ProvableStruct + +def circuit : FormalAssertion (F p) Inputs where + main inputs := do + -- IS_BIT<1, cond>: in a chip this is one of the chip's own flag constraints + assertZero (inputs.cond * (1 - inputs.cond)) + isByte inputs.cond inputs.x + + Assumptions := fun { cond, .. } => IsBool cond + Spec := fun { cond, x } => cond = 1 → x.val < 256 + + requirementsChannelsLawful input_var i₀ := by + obtain ⟨cond, x⟩ := input_var + simp only [circuit_norm, isByte, areBytesTable] + grind + + soundness := by + circuit_proof_start [isByte, areBytesTable] + obtain ⟨h_bool, h_pull⟩ := h_holds + rw [mul_eq_zero, sub_eq_zero] at h_bool + rcases h_bool with rfl | h1 + · simp + · subst h1 + simp_all + + completeness := by + circuit_proof_start [isByte, areBytesTable] + rcases h_assumptions with rfl | rfl <;> simp_all + +end IsByteCheck + +end LambdaVM diff --git a/formal/README.md b/formal/README.md new file mode 100644 index 000000000..09bab7a30 --- /dev/null +++ b/formal/README.md @@ -0,0 +1,169 @@ +# Lambda VM formal model (Clean / Lean 4) + +Lean 4 project that models the Lambda VM arithmetization in +[Clean](https://github.com/Verified-zkEVM/clean) and proves it against `spec/`. + +What it covers: the AIR tables, the LogUp buses (Clean "channels") and the +semantic specification of each table. What it does not cover: the STARK / +FRI / WHIR prover, the LogUp argument itself, the executor, GPU code. + +## Layout + +- `LambdaVM/Field.lean` — Goldilocks as the base field (`F p`), with the size + facts Clean's gadgets ask for. Primality comes from CompPoly's Pratt certificate. +- `LambdaVM/Buses/` — the buses that are not static tables. `Alu.lean` is the + unified ALU bus: message layout as in `BusId::Alu`, the caller's `IS_WORD` + assumptions on both operands as hypotheses, and one `Guarantees` clause per + `opsel` (LT and EQ so far). A chip pushing with one `opsel` discharges the + other clauses by showing its flags cannot decode as them. +- `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 + arithmetic argument of `spec/lt.typ` on naturals, `Honest` is the row + `generate_lt_trace` produces, and the `GeneralFormalCircuit` proves that a row + that pulls its range checks pushes a correct ALU result (soundness) and that an + honest row satisfies everything (completeness). `Eq.lean` is the EQ chip in the + same shape: SUB carries, four IS_HALF pulls, a ZERO pull on the sum of the + halves, `res = eq xor invert`; its `μ` is a bit, as in PR #1016. + +- `LambdaVM/Ensembles/` — tables wired together through their channels. + `EqLookup.lean` is the first one: `pushStatic` is the provider side of any + static lookup channel (its row is the vector of multiplicities, the role of + the `μ` columns of BITWISE), and `eqLookup` chains the IS_HALF provider, the + ZERO provider and the EQ chip in dependency order. `eq_rows_correct` is the + first global theorem: for any witness whose constraints hold and whose + channels balance, every EQ row with `μ = 1` and range-checked operands + carries the equality bit. The lookup argument is what turns the pulled range + checks into facts. +- `LambdaVM/Tables/ShiftCore.lean` and `Shift.lean` — the SHIFT chip. `ShiftCore` + is the two-phase shift argument of `spec/shift.typ` on naturals (HWSL + per limb, then whole limbs, left and right, logical and arithmetic), ending in + `ShiftCore.main`, which takes exactly the facts the row gives (decoded + `bit_shift`, one-hot `limb_shift`, sign bit, HWSL outputs or their `zbs` + overrides) and concludes `shiftResult`. `Shift.lean` mirrors the 22 constraints + and 17 interactions of `shift.rs` and proves soundness and completeness, the + latter for both the honest active row and the padding row. + +## Lessons for big chips (from SHIFT) + +- Precompute the `ElaboratedCircuit` instance (`instance elaborated := by + elaborate_circuit`) and pass it explicitly; without it every proof of a + 38-operation circuit times out at elaboration. +- Keep large row polynomials folded behind a definition (`shiftedPoly`) with a + lemma that pushes `Expression.eval` inside, and bridge to the natural-number + version with one cast lemma. +- State `soundness` and `completeness` as standalone theorems and reference + them from the structure; the structure itself otherwise exceeds the heartbeat + budget while abstracting the proof terms. +- `rw ... at h` closes goals by `rfl`; a following `simp`/`ring` then fails with + "no goals". Guard with `try` where the rewrite may already close the goal. + +## Differential check against the Rust prover + +The Lean circuits are hand transcriptions of `prover/src/tables/*.rs`. The check +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. +2. `diff/lean_diff.rs` is a prover test. Install it as + `prover/src/tests/lean_diff.rs`, add `pub mod lean_diff;` to + `prover/src/tests/mod.rs` and `serde_json = "1"` to the prover's + dev-dependencies, then run + `cargo test -p lambda-vm-prover lean_diff -- --nocapture`. + +For each table the test evaluates the Lean asserts and the Rust `ConstraintSet` +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 models follow PR #1016 (`fix/multiplicity-soundness`), so the test is meant +to run on that branch (a git worktree of it works). Result there, 2026-10-20: + +- EQ: 5 constraints and 6 interactions, exact match. +- SHIFT: 22 constraints and 17 interactions, exact match. +- LT: exact match except the two documented deltas: `μ·(1 − μ) = 0` exists + only in Lean, `ARE_BYTES[μ, 0]` exists only in Rust. + +The check compares polynomials, not zero sets: it caught `μ·(μ − 1)` versus +`μ·(1 − μ)` in EQ, which is why the Lean bit constraints use the spec's form. + +## 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. +`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. +- `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`. +- `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 + `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 + `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`. +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`, + which is a local constraint and makes the requirement vacuous at lawfulness. + +Until then LT keeps `μ ∈ {0, 1}` (see below). + +## Known differences from the Rust prover + +- `LT` constrains `μ·(1 − μ) = 0`. The spec types `μ` as `Bit`; `lt.rs` has no + constraint on it and uses it as a deduplication count. Clean only grants a + channel guarantee to a pull with multiplicity exactly 1, which is the + faithful reading: a sender multiplicity outside `{0, 1}` is not protected by + the LogUp balance (two rows with `μ = 1` and `μ = −1` cancel each other's + lookups). The same pattern exists in MUL, DVRM, SHIFT, EQ and BYTEWISE. +- `LambdaVM/Templates/` — the constraint templates of the spec (`IS_BIT`, + `IS_BYTE`, `ARE_BYTES`, ...), with `Spec` taken from the corresponding + `spec/*.typ` page, not from the constraints. Templates that are only + interactions are plain `Circuit` helpers meant to be expanded inline in a chip; + each comes with a `*Check` assertion that pins down its meaning. + +## Building + +```sh +# once: Lean toolchain manager +curl https://elan.lean-lang.org/elan-init.sh -sSf | sh + +cd formal +lake update # clones Clean, Mathlib, CompPoly at the pinned revisions +lake exe cache get # Mathlib prebuilt binaries (without this, ~1 h of compile) +lake build +``` + +Clean itself is compiled from source; only the modules we import are built. + +## Conventions + +- Files use Clean's module header: `module` / `public import ...` / + `@[expose] public section`. +- One table or template per file. `Spec` states the meaning of the rows in + terms of the spec's variables; `Assumptions` are the preconditions the + caller table must establish. +- Proofs start with `circuit_proof_start` (or `circuit_proof_all` when it + closes the goal). See Clean's `AGENTS.md` and `doc/proving-guide.md`. +- Clean's circuit inference does not unfold user-defined `Circuit` helpers. A + 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. diff --git a/formal/diff/lean_diff.rs b/formal/diff/lean_diff.rs new file mode 100644 index 000000000..5d889a15e --- /dev/null +++ b/formal/diff/lean_diff.rs @@ -0,0 +1,402 @@ +//! Differential check of the Lean models in `formal/` against the Rust tables. +//! +//! `formal/export/.json` holds the operations of each Lean row circuit: +//! the constraint polynomials (`assert`) and the bus interactions (`interact`), +//! with variables numbered in Rust column order. For each of LT, EQ and SHIFT +//! this test evaluates them on random rows next to the Rust `ConstraintSet` and +//! `bus_interactions()`, and matches them as multisets of functions +//! (Schwartz–Zippel over [`TRIALS`] rows). It also checks that the Lean +//! constraints vanish on honest Rust traces, padding rows included. +//! +//! Run with `cargo test -p lambda-vm-prover lean_diff -- --nocapture`. + +use std::collections::HashMap; + +use serde_json::Value; +use stark::constraint_ir::eval_program_base; +use stark::constraints::builder::{CaptureBuilder, ConstraintSet, num_base_from_meta}; +use stark::lookup::{BusInteraction, LinearTerm, Multiplicity}; + +use crate::tables::types::{FE, GoldilocksExtension, GoldilocksField}; + +type Gl = GoldilocksField; +type Gl3 = GoldilocksExtension; + +const TRIALS: usize = 64; + +// ============================================================================= +// Lean side: the exported operations +// ============================================================================= + +enum Expr { + Var(usize), + Const(u64), + Add(Box, Box), + Mul(Box, Box), +} + +fn parse_expr(v: &Value) -> Expr { + match v["type"].as_str().expect("expr type") { + "var" => Expr::Var(v["index"].as_u64().expect("var index") as usize), + "const" => Expr::Const(v["value"].as_u64().expect("const value")), + "add" => Expr::Add(Box::new(parse_expr(&v["lhs"])), Box::new(parse_expr(&v["rhs"]))), + "mul" => Expr::Mul(Box::new(parse_expr(&v["lhs"])), Box::new(parse_expr(&v["rhs"]))), + other => panic!("unknown expression node {other}"), + } +} + +fn eval(e: &Expr, row: &[FE]) -> FE { + match e { + Expr::Var(i) => row[*i].clone(), + Expr::Const(c) => FE::from(*c), + Expr::Add(a, b) => eval(a, row) + eval(b, row), + Expr::Mul(a, b) => eval(a, row) * eval(b, row), + } +} + +struct LeanInteract { + channel: String, + mult: Expr, + msg: Vec, +} + +struct LeanCircuit { + columns: usize, + asserts: Vec, + interacts: Vec, +} + +fn load_lean(name: &str) -> LeanCircuit { + let path = format!("{}/../formal/export/{name}.json", env!("CARGO_MANIFEST_DIR")); + let text = std::fs::read_to_string(&path).unwrap_or_else(|e| panic!("{path}: {e}")); + let json: Value = serde_json::from_str(&text).expect("json"); + let columns = json["columns"].as_u64().expect("columns") as usize; + let mut asserts = Vec::new(); + let mut interacts = Vec::new(); + for op in json["operations"].as_array().expect("operations") { + if let Some(a) = op.get("assert") { + asserts.push(parse_expr(a)); + } else if let Some(i) = op.get("interact") { + interacts.push(LeanInteract { + channel: i["channel"].as_str().expect("channel").to_string(), + mult: parse_expr(&i["multiplicity"]), + msg: i["message"].as_array().expect("message").iter().map(parse_expr).collect(), + }); + } else { + panic!("unexpected operation {op}"); + } + } + LeanCircuit { columns, asserts, interacts } +} + +/// Clean channel name → Lambda VM `BusId` (see `tables/types.rs`). +fn bus_id_of(channel: &str) -> u64 { + match channel { + "ARE_BYTES" => 0, + "IS_HALF" => 1, + "IS_B20" => 2, + "MSB8" => 6, + "MSB16" => 7, + "ZERO" => 8, + "HWSL" => 9, + "BYTE_ALU" => 24, + "ALU" => 25, + other => panic!("unknown channel {other}"), + } +} + +// ============================================================================= +// Rust side: constraints and interactions evaluated on a row +// ============================================================================= + +fn multiplicity_at(m: &Multiplicity, row: &[FE]) -> FE { + let col = |c: usize| row[c].clone(); + match m { + Multiplicity::One => FE::one(), + Multiplicity::Column(c) => col(*c), + Multiplicity::Sum(a, b) => col(*a) + col(*b), + Multiplicity::Negated(c) => FE::one() - col(*c), + Multiplicity::Diff(a, b) => col(*a) - col(*b), + Multiplicity::Sum3(a, b, c) => col(*a) + col(*b) + col(*c), + Multiplicity::Linear(terms) => { + let mut acc = FE::zero(); + for t in terms { + match *t { + LinearTerm::Column { coefficient, column } => { + acc += col(column) * FE::from(coefficient) + } + LinearTerm::ColumnUnsigned { coefficient, column } => { + acc += col(column) * FE::from(coefficient) + } + LinearTerm::Constant(v) => acc += FE::from(v), + } + } + acc + } + } +} + +/// `(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. +fn rust_interaction_at(i: &BusInteraction, row: &[FE]) -> (u64, FE, Vec) { + let m = multiplicity_at(&i.multiplicity, row); + let m = if i.is_sender { -m } else { m }; + let elems = i.values.iter().flat_map(|v| v.combine_from(|c| row[c].clone())).collect(); + (i.bus_id, m, elems) +} + +fn lean_interaction_at(i: &LeanInteract, row: &[FE]) -> (u64, FE, Vec) { + (bus_id_of(&i.channel), eval(&i.mult, row), i.msg.iter().map(|e| eval(e, row)).collect()) +} + +// ============================================================================= +// Matching +// ============================================================================= + +struct SplitMix64(u64); +impl SplitMix64 { + fn next_u64(&mut self) -> u64 { + self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = self.0; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) + } +} + +fn random_rows(num_cols: usize, seed: u64) -> Vec> { + let mut rng = SplitMix64(seed); + (0..TRIALS).map(|_| (0..num_cols).map(|_| FE::from(rng.next_u64())).collect()).collect() +} + +/// Greedy multiset matching of fingerprints; returns the unmatched indices on each side. +fn unmatched(lean: &[K], rust: &[K]) -> (Vec, Vec) { + let mut pool: HashMap> = HashMap::new(); + for (j, k) in rust.iter().enumerate() { + pool.entry(k.clone()).or_default().push(j); + } + let mut lean_unmatched = Vec::new(); + for (i, k) in lean.iter().enumerate() { + match pool.get_mut(k).and_then(|v| v.pop()) { + Some(_) => {} + None => lean_unmatched.push(i), + } + } + let rust_unmatched: Vec = pool.into_values().flatten().collect(); + (lean_unmatched, rust_unmatched) +} + +fn fp(x: &FE) -> u64 { + x.canonical_u64() +} + +struct Report { + lean_asserts_unmatched: Vec, + rust_constraints_unmatched: Vec, + lean_interacts_unmatched: Vec, + rust_interacts_unmatched: Vec, +} + +fn compare>( + label: &str, + lean: &LeanCircuit, + set: &CS, + interactions: &[BusInteraction], + num_cols: usize, + honest_rows: &[Vec], +) -> Report { + assert_eq!(lean.columns, num_cols, "[{label}] column count"); + + // The Rust constraints as an evaluable program. + let meta = set.meta(); + let n = meta.len(); + let mut cb = CaptureBuilder::::new(); + set.eval(&mut cb); + let (prog, _) = cb.finish(num_base_from_meta(&meta)); + + // Fingerprints over random rows. + let rows = random_rows(num_cols, 0xC1EA_0000 ^ label.len() as u64); + let lean_fp: Vec> = lean + .asserts + .iter() + .map(|e| rows.iter().map(|r| fp(&eval(e, r))).collect()) + .collect(); + let rust_fp: Vec> = + (0..n).map(|i| rows.iter().map(|r| fp(&eval_program_base(&prog, i, r))).collect()).collect(); + let (lean_asserts_unmatched, rust_constraints_unmatched) = unmatched(&lean_fp, &rust_fp); + + let lean_ifp: Vec<(u64, Vec, Vec>)> = lean + .interacts + .iter() + .map(|i| { + let evals: Vec<_> = rows.iter().map(|r| lean_interaction_at(i, r)).collect(); + ( + evals[0].0, + evals.iter().map(|e| fp(&e.1)).collect(), + evals.iter().map(|e| e.2.iter().map(fp).collect()).collect(), + ) + }) + .collect(); + let rust_ifp: Vec<(u64, Vec, Vec>)> = interactions + .iter() + .map(|i| { + let evals: Vec<_> = rows.iter().map(|r| rust_interaction_at(i, r)).collect(); + ( + evals[0].0, + evals.iter().map(|e| fp(&e.1)).collect(), + evals.iter().map(|e| e.2.iter().map(fp).collect()).collect(), + ) + }) + .collect(); + let (li, ri) = unmatched(&lean_ifp, &rust_ifp); + let lean_interacts_unmatched = li.iter().map(|&i| lean.interacts[i].channel.clone()).collect(); + let rust_interacts_unmatched = ri.iter().map(|&j| interactions[j].bus_id).collect(); + + // Every Lean constraint vanishes on the honest trace. + for (r, row) in honest_rows.iter().enumerate() { + for (i, e) in lean.asserts.iter().enumerate() { + assert_eq!(eval(e, row), FE::zero(), "[{label}] Lean assert {i} on honest row {r}"); + } + for i in 0..n { + assert_eq!(eval_program_base(&prog, i, row), FE::zero(), "[{label}] Rust constraint {i} on honest row {r}"); + } + } + + println!( + "[{label}] Lean: {} asserts, {} interactions | Rust: {} constraints, {} interactions", + lean.asserts.len(), + lean.interacts.len(), + n, + interactions.len() + ); + println!( + "[{label}] unmatched Lean asserts {:?}, unmatched Rust constraints {:?}, unmatched Lean interactions {:?}, unmatched Rust interactions (bus ids) {:?}", + lean_asserts_unmatched, rust_constraints_unmatched, lean_interacts_unmatched, rust_interacts_unmatched + ); + Report { + lean_asserts_unmatched, + rust_constraints_unmatched, + lean_interacts_unmatched, + rust_interacts_unmatched, + } +} + +fn rows_of(trace: &stark::trace::TraceTable, num_cols: usize) -> Vec> { + (0..trace.num_rows()) + .map(|r| (0..num_cols).map(|c| trace.main_table.get(r, c).clone()).collect()) + .collect() +} + +const EDGE: [u64; 8] = [0, 1, 0xFF, 0xFFFF, 0x7FFF_FFFF_FFFF_FFFF, 0x8000_0000_0000_0000, u64::MAX - 1, u64::MAX]; + +// ============================================================================= +// Tables +// ============================================================================= + +#[test] +fn lean_diff_lt() { + use crate::tables::lt::{LtConstraints, LtOperation, bus_interactions, cols, generate_lt_trace}; + let mut rng = SplitMix64(0x17); + let mut ops = Vec::new(); + for &a in &EDGE { + for &b in &EDGE { + for signed in [false, true] { + for invert in [false, true] { + ops.push(LtOperation::new_with_invert(a, b, signed, invert)); + } + } + } + } + for _ in 0..256 { + ops.push(LtOperation::new_with_invert( + rng.next_u64(), + rng.next_u64(), + rng.next_u64() & 1 == 1, + rng.next_u64() & 1 == 1, + )); + } + let trace = generate_lt_trace(&ops); + let report = compare( + "LT", + &load_lean("lt"), + &LtConstraints, + &bus_interactions(), + cols::NUM_COLUMNS, + &rows_of(&trace, cols::NUM_COLUMNS), + ); + // Known deltas: the Lean model keeps `μ·(μ − 1) = 0` (spec: `μ : Bit`), the Rust chip bounds + // `μ` with the `ARE_BYTES[μ, 0]` send instead (PR #1016). + assert_eq!(report.lean_asserts_unmatched.len(), 1, "[LT] only the μ bit constraint should be Lean-only"); + assert!(report.rust_constraints_unmatched.is_empty(), "[LT] Rust-only constraints"); + assert!(report.lean_interacts_unmatched.is_empty(), "[LT] Lean-only interactions"); + assert_eq!(report.rust_interacts_unmatched, vec![0], "[LT] only ARE_BYTES[μ, 0] should be Rust-only"); +} + +#[test] +fn lean_diff_eq() { + use crate::tables::eq::{EqConstraints, EqOperation, bus_interactions, cols, generate_eq_trace}; + let mut rng = SplitMix64(0xE0); + let mut ops = Vec::new(); + for &a in &EDGE { + for &b in &EDGE { + for invert in [false, true] { + ops.push(EqOperation::new(a, b, invert)); + } + } + } + for _ in 0..256 { + let a = rng.next_u64(); + let b = if rng.next_u64() & 1 == 1 { a } else { rng.next_u64() }; + ops.push(EqOperation::new(a, b, rng.next_u64() & 1 == 1)); + } + let trace = generate_eq_trace(&ops); + let report = compare( + "EQ", + &load_lean("eq"), + &EqConstraints, + &bus_interactions(), + cols::NUM_COLUMNS, + &rows_of(&trace, cols::NUM_COLUMNS), + ); + assert!(report.lean_asserts_unmatched.is_empty() && report.rust_constraints_unmatched.is_empty(), "[EQ] constraints differ"); + assert!(report.lean_interacts_unmatched.is_empty() && report.rust_interacts_unmatched.is_empty(), "[EQ] interactions differ"); +} + +#[test] +fn lean_diff_shift() { + use crate::tables::shift::{ShiftConstraints, ShiftOperation, bus_interactions, cols, generate_shift_trace}; + let mut rng = SplitMix64(0x5F); + let mut ops = Vec::new(); + for &v in &EDGE { + for s in [0u64, 1, 15, 16, 17, 31, 32, 33, 47, 48, 63, 64, 65, 255, 256, u64::MAX] { + for direction in [false, true] { + for signed in [false, true] { + for word in [false, true] { + ops.push(ShiftOperation::new(v, s, direction, signed, word)); + } + } + } + } + } + for _ in 0..512 { + ops.push(ShiftOperation::new( + rng.next_u64(), + rng.next_u64(), + rng.next_u64() & 1 == 1, + rng.next_u64() & 1 == 1, + rng.next_u64() & 1 == 1, + )); + } + let trace = generate_shift_trace(&ops); + let report = compare( + "SHIFT", + &load_lean("shift"), + &ShiftConstraints, + &bus_interactions(), + cols::NUM_COLUMNS, + &rows_of(&trace, cols::NUM_COLUMNS), + ); + assert!(report.lean_asserts_unmatched.is_empty() && report.rust_constraints_unmatched.is_empty(), "[SHIFT] constraints differ"); + assert!(report.lean_interacts_unmatched.is_empty() && report.rust_interacts_unmatched.is_empty(), "[SHIFT] interactions differ"); +} diff --git a/formal/export/eq.json b/formal/export/eq.json new file mode 100644 index 000000000..cc2edcd8d --- /dev/null +++ b/formal/export/eq.json @@ -0,0 +1,234 @@ +{"operations": + [{"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 11}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 6}], + "channel": "IS_HALF"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 11}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 7}], + "channel": "IS_HALF"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 11}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 8}], + "channel": "IS_HALF"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 11}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 9}], + "channel": "IS_HALF"}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 4}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": {"type": "var", "index": 4}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 0}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 7}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 6}}, + "lhs": {"type": "var", "index": 2}}}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 0}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 7}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 6}}, + "lhs": {"type": "var", "index": 2}}}}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 1}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 0}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 7}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 6}}, + "lhs": {"type": "var", "index": 2}}}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 9}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 8}}, + "lhs": {"type": "var", "index": 3}}}}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 1}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 0}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 7}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 6}}, + "lhs": {"type": "var", "index": 2}}}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 9}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 8}}, + "lhs": {"type": "var", "index": 3}}}}}}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 11}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": + [{"type": "add", + "rhs": {"type": "var", "index": 9}, + "lhs": + {"type": "add", + "rhs": {"type": "var", "index": 8}, + "lhs": + {"type": "add", "rhs": {"type": "var", "index": 7}, "lhs": {"type": "var", "index": 6}}}}, + {"type": "var", "index": 10}], + "channel": "ZERO"}}, + {"assert": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 4}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 10}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 4}, + "lhs": + {"type": "mul", "rhs": {"type": "var", "index": 10}, "lhs": {"value": 2, "type": "const"}}}, + "lhs": {"type": "var", "index": 5}}}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 11}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": {"type": "var", "index": 11}}}, + {"interact": + {"multiplicity": {"type": "var", "index": 11}, + "message": + [{"type": "var", "index": 0}, + {"type": "var", "index": 1}, + {"type": "var", "index": 2}, + {"type": "var", "index": 3}, + {"type": "add", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 4}, "lhs": {"value": 64, "type": "const"}}, + "lhs": {"value": 3, "type": "const"}}, + {"type": "var", "index": 5}, + {"value": 0, "type": "const"}], + "channel": "ALU"}}], + "name": "eq", + "columns": 12} \ No newline at end of file diff --git a/formal/export/lt.json b/formal/export/lt.json new file mode 100644 index 000000000..583ebc861 --- /dev/null +++ b/formal/export/lt.json @@ -0,0 +1,493 @@ +{"operations": + [{"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 16}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": {"type": "var", "index": 16}}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 16}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 1}], + "channel": "IS_HALF"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 16}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 4}], + "channel": "IS_HALF"}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 6}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": {"type": "var", "index": 6}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 14}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": {"type": "var", "index": 14}}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 16}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 2}, {"type": "var", "index": 12}], + "channel": "MSB16"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 16}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 5}, {"type": "var", "index": 13}], + "channel": "MSB16"}}, + {"assert": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 2}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 1}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 0}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 9}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 8}}, + "lhs": {"type": "var", "index": 3}}}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 11}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 10}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 5}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 4}}}}}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 6}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}}, + "lhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 2}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 1}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 0}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 9}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 8}}, + "lhs": {"type": "var", "index": 3}}}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 11}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 10}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 5}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 4}}}}}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 13}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 2}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 1}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 0}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 9}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 8}}, + "lhs": {"type": "var", "index": 3}}}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 11}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 10}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 5}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 4}}}}}}, + "lhs": {"type": "var", "index": 12}}, + "lhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 13}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": {"type": "var", "index": 12}}}}, + "lhs": {"type": "var", "index": 6}}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"type": "var", "index": 7}}}, + {"assert": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 14}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 7}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 14}, + "lhs": + {"type": "mul", "rhs": {"type": "var", "index": 7}, "lhs": {"value": 2, "type": "const"}}}, + "lhs": {"type": "var", "index": 15}}}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 0}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 9}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 8}}, + "lhs": {"type": "var", "index": 3}}}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 0}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 9}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 8}}, + "lhs": {"type": "var", "index": 3}}}}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 2}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 1}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 0}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 9}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 8}}, + "lhs": {"type": "var", "index": 3}}}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 11}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 10}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 5}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 4}}}}}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 2}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 1}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"value": 18446744065119617026, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 0}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 9}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 8}}, + "lhs": {"type": "var", "index": 3}}}}, + "lhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 11}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 10}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 5}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 4}}}}}}}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 16}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 8}], + "channel": "IS_HALF"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 16}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 9}], + "channel": "IS_HALF"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 16}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 10}], + "channel": "IS_HALF"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 16}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 11}], + "channel": "IS_HALF"}}, + {"interact": + {"multiplicity": {"type": "var", "index": 16}, + "message": + [{"type": "var", "index": 0}, + {"type": "add", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 2}, "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 1}}, + {"type": "var", "index": 3}, + {"type": "add", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 5}, "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 4}}, + {"type": "add", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 14}, "lhs": {"value": 64, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 6}, "lhs": {"value": 32, "type": "const"}}, + "lhs": {"value": 4, "type": "const"}}}, + {"type": "var", "index": 15}, + {"value": 0, "type": "const"}], + "channel": "ALU"}}], + "name": "lt", + "columns": 17} \ No newline at end of file diff --git a/formal/export/shift.json b/formal/export/shift.json new file mode 100644 index 000000000..0ff43f48d --- /dev/null +++ b/formal/export/shift.json @@ -0,0 +1,883 @@ +{"operations": + [{"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 25}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": {"type": "var", "index": 5}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 5}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"type": "var", "index": 25}}, + "lhs": {"type": "var", "index": 0}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"type": "var", "index": 13}}, + "lhs": {"type": "var", "index": 12}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 5}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"type": "var", "index": 25}}, + "lhs": {"type": "var", "index": 1}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"type": "var", "index": 14}}, + "lhs": {"type": "var", "index": 12}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 5}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"type": "var", "index": 25}}, + "lhs": {"type": "var", "index": 2}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"type": "var", "index": 15}}, + "lhs": {"type": "var", "index": 12}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 5}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"type": "var", "index": 25}}, + "lhs": {"type": "var", "index": 3}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"type": "var", "index": 16}}, + "lhs": {"type": "var", "index": 12}}}, + {"assert": + {"type": "mul", "rhs": {"type": "var", "index": 17}, "lhs": {"type": "var", "index": 12}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 5}, "lhs": {"type": "var", "index": 0}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"type": "var", "index": 18}}, + "lhs": {"type": "var", "index": 12}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 5}, "lhs": {"type": "var", "index": 1}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"type": "var", "index": 19}}, + "lhs": {"type": "var", "index": 12}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 5}, "lhs": {"type": "var", "index": 2}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"type": "var", "index": 20}}, + "lhs": {"type": "var", "index": 12}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 5}, "lhs": {"type": "var", "index": 3}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"type": "var", "index": 21}}, + "lhs": {"type": "var", "index": 12}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 22}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": {"type": "var", "index": 22}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 23}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": {"type": "var", "index": 23}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 24}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": {"type": "var", "index": 24}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 24}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 23}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 22}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 24}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 23}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 22}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}}}}}, + {"assert": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", + "rhs": {"value": 65536, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 24}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 23}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 22}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}}}, + "lhs": + {"type": "mul", + "rhs": {"type": "var", "index": 10}, + "lhs": {"value": 65535, "type": "const"}}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": {"type": "var", "index": 17}, + "lhs": {"type": "var", "index": 21}}, + "lhs": {"type": "var", "index": 24}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": {"type": "var", "index": 16}, + "lhs": {"type": "var", "index": 20}}, + "lhs": {"type": "var", "index": 23}}, + "lhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": {"type": "var", "index": 15}, + "lhs": {"type": "var", "index": 19}}, + "lhs": {"type": "var", "index": 22}}}}}, + "lhs": {"type": "var", "index": 5}}, + "lhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 13}, "lhs": {"type": "var", "index": 23}}, + "lhs": + {"type": "mul", + "rhs": + {"type": "add", "rhs": {"type": "var", "index": 18}, "lhs": {"type": "var", "index": 14}}, + "lhs": {"type": "var", "index": 22}}}, + "lhs": + {"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"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", "rhs": {"type": "var", "index": 17}, "lhs": {"type": "var", "index": 21}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 24}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 23}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 22}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}}}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": {"type": "var", "index": 16}, + "lhs": {"type": "var", "index": 20}}, + "lhs": {"type": "var", "index": 24}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": {"type": "var", "index": 15}, + "lhs": {"type": "var", "index": 19}}, + "lhs": {"type": "var", "index": 23}}, + "lhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": {"type": "var", "index": 14}, + "lhs": {"type": "var", "index": 18}}, + "lhs": {"type": "var", "index": 22}}}}}, + "lhs": {"type": "var", "index": 5}}, + "lhs": + {"type": "mul", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 13}, "lhs": {"type": "var", "index": 22}}, + "lhs": + {"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"}}, + "lhs": {"type": "var", "index": 8}}}}, + {"assert": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", + "rhs": {"value": 65536, "type": "const"}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 24}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 23}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 22}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}}}, + "lhs": + {"type": "add", + "rhs": {"type": "var", "index": 24}, + "lhs": {"type": "var", "index": 23}}}, + "lhs": + {"type": "mul", + "rhs": {"type": "var", "index": 10}, + "lhs": {"value": 65535, "type": "const"}}}, + "lhs": + {"type": "mul", + "rhs": + {"type": "add", "rhs": {"type": "var", "index": 17}, "lhs": {"type": "var", "index": 21}}, + "lhs": {"type": "var", "index": 22}}}, + "lhs": {"type": "var", "index": 5}}, + "lhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 13}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 24}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 23}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 22}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}}}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": {"type": "var", "index": 18}, + "lhs": {"type": "var", "index": 14}}, + "lhs": {"type": "var", "index": 24}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": {"type": "var", "index": 19}, + "lhs": {"type": "var", "index": 15}}, + "lhs": {"type": "var", "index": 23}}, + "lhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": {"type": "var", "index": 20}, + "lhs": {"type": "var", "index": 16}}, + "lhs": {"type": "var", "index": 22}}}}}, + "lhs": + {"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"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 24}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 23}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 22}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}}}, + "lhs": {"type": "var", "index": 24}}, + "lhs": + {"type": "mul", + "rhs": {"type": "var", "index": 10}, + "lhs": {"value": 65535, "type": "const"}}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": {"type": "var", "index": 17}, + "lhs": {"type": "var", "index": 21}}, + "lhs": {"type": "var", "index": 23}}, + "lhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": {"type": "var", "index": 16}, + "lhs": {"type": "var", "index": 20}}, + "lhs": {"type": "var", "index": 22}}}}, + "lhs": {"type": "var", "index": 5}}, + "lhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 13}, "lhs": {"type": "var", "index": 24}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": {"type": "var", "index": 18}, + "lhs": {"type": "var", "index": 14}}, + "lhs": {"type": "var", "index": 23}}, + "lhs": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": {"type": "var", "index": 19}, + "lhs": {"type": "var", "index": 15}}, + "lhs": {"type": "var", "index": 22}}}}, + "lhs": + {"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"}}, + "lhs": {"type": "var", "index": 9}}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 5}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": {"type": "var", "index": 5}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 6}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": {"type": "var", "index": 6}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 7}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": {"type": "var", "index": 7}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 12}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": {"type": "var", "index": 12}}}, + {"assert": + {"type": "mul", + "rhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 25}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}, + "lhs": {"type": "var", "index": 25}}}, + {"assert": + {"type": "mul", + "rhs": {"type": "var", "index": 10}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 6}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 1, "type": "const"}}}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 6}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 3}, {"type": "var", "index": 10}], + "channel": "MSB16"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "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"}}, + "message": + [{"value": 0, "type": "const"}, + {"type": "var", "index": 4}, + {"value": 15, "type": "const"}, + {"type": "var", "index": 11}], + "channel": "BYTE_ALU"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 5}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": + [{"value": 0, "type": "const"}, + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 4}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 12}, "lhs": {"value": 16, "type": "const"}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 256, "type": "const"}}}, + {"value": 15, "type": "const"}, + {"type": "var", "index": 11}], + "channel": "BYTE_ALU"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 25}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 11}, {"type": "var", "index": 12}], + "channel": "ZERO"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "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"}}, + "message": + [{"type": "var", "index": 0}, + {"type": "var", "index": 11}, + {"type": "var", "index": 13}, + {"type": "var", "index": 18}], + "channel": "HWSL"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "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"}}, + "message": + [{"type": "var", "index": 1}, + {"type": "var", "index": 11}, + {"type": "var", "index": 14}, + {"type": "var", "index": 19}], + "channel": "HWSL"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "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"}}, + "message": + [{"type": "var", "index": 2}, + {"type": "var", "index": 11}, + {"type": "var", "index": 15}, + {"type": "var", "index": 20}], + "channel": "HWSL"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "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"}}, + "message": + [{"type": "var", "index": 3}, + {"type": "var", "index": 11}, + {"type": "var", "index": 16}, + {"type": "var", "index": 21}], + "channel": "HWSL"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "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"}}, + "message": + [{"type": "mul", "rhs": {"type": "var", "index": 10}, "lhs": {"value": 65535, "type": "const"}}, + {"type": "var", "index": 11}, + {"type": "var", "index": 17}, + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 17}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "mul", + "rhs": {"type": "var", "index": 10}, + "lhs": {"value": 65535, "type": "const"}}}], + "channel": "HWSL"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 25}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": + [{"value": 0, "type": "const"}, + {"type": "var", "index": 4}, + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 7}, "lhs": {"value": 32, "type": "const"}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 48, "type": "const"}}, + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 24}, "lhs": {"value": 16, "type": "const"}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 23}, "lhs": {"value": 32, "type": "const"}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 22}, + "lhs": {"value": 48, "type": "const"}}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "lhs": {"value": 48, "type": "const"}}}}], + "channel": "BYTE_ALU"}}, + {"interact": + {"multiplicity": {"type": "var", "index": 25}, + "message": + [{"type": "add", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 1}, "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 0}}, + {"type": "add", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 3}, "lhs": {"value": 65536, "type": "const"}}, + "lhs": {"type": "var", "index": 2}}, + {"type": "add", + "rhs": + {"type": "mul", + "rhs": {"type": "var", "index": 27}, + "lhs": {"value": 65536, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 26}, "lhs": {"value": 256, "type": "const"}}, + "lhs": {"type": "var", "index": 4}}}, + {"type": "var", "index": 28}, + {"type": "add", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 5}, "lhs": {"value": 64, "type": "const"}}, + "lhs": + {"type": "add", + "rhs": + {"type": "mul", "rhs": {"type": "var", "index": 6}, "lhs": {"value": 32, "type": "const"}}, + "lhs": + {"type": "add", "rhs": {"type": "var", "index": 7}, "lhs": {"value": 5, "type": "const"}}}}, + {"type": "var", "index": 8}, + {"type": "var", "index": 9}], + "channel": "ALU"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"value": 1, "type": "const"}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 4}, {"type": "var", "index": 26}], + "channel": "ARE_BYTES"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 25}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 27}], + "channel": "IS_HALF"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 25}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 0}], + "channel": "IS_HALF"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 25}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 1}], + "channel": "IS_HALF"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 25}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 2}], + "channel": "IS_HALF"}}, + {"interact": + {"multiplicity": + {"type": "mul", + "rhs": {"type": "var", "index": 25}, + "lhs": {"value": 18446744069414584320, "type": "const"}}, + "message": [{"type": "var", "index": 3}], + "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 new file mode 100644 index 000000000..88c14c478 --- /dev/null +++ b/formal/lake-manifest.json @@ -0,0 +1,116 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/Verified-zkEVM/clean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "1a6c28426372bb99af79e533aa7b9a0788eff0d7", + "name": "Clean", + "manifestFile": "lake-manifest.json", + "inputRev": "1a6c28426372bb99af79e533aa7b9a0788eff0d7", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/Verified-zkEVM/CompPoly.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "a09455a22fea4623a2a1c5b363cf6efc61486a83", + "name": "CompPoly", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.1", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "0df444a360eaa60ab8c11dca51a86af692955474", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.1", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "16f02aa7642864af59f1ff0e384a015994db9118", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.0", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "«lambda-vm-formal»", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/formal/lakefile.toml b/formal/lakefile.toml new file mode 100644 index 000000000..855683b74 --- /dev/null +++ b/formal/lakefile.toml @@ -0,0 +1,15 @@ +name = "lambda-vm-formal" +defaultTargets = ["LambdaVM"] + +[leanOptions] +autoImplicit = false +relaxedAutoImplicit = false + +# Clean pinned to a revision; Mathlib and CompPoly come in through Clean's manifest. +[[require]] +name = "Clean" +git = "https://github.com/Verified-zkEVM/clean" +rev = "1a6c28426372bb99af79e533aa7b9a0788eff0d7" + +[[lean_lib]] +name = "LambdaVM" diff --git a/formal/lean-toolchain b/formal/lean-toolchain new file mode 100644 index 000000000..a8afa7d1b --- /dev/null +++ b/formal/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.33.1