diff --git a/Complexity.lean b/Complexity.lean index e5a79c544a..77459f26ab 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -800,6 +800,10 @@ public import Complexity.Computability.Circuit.Boolean.Synthesis public import Complexity.Computability.Circuit.Boolean.TC0 public import Complexity.Computability.Circuit.Boolean.Tableau.Basic public import Complexity.Computability.Circuit.Boolean.Tableau.Correct +public import Complexity.Computability.Circuit.Boolean.Tableau.Decoder.Assembly +public import Complexity.Computability.Circuit.Boolean.Tableau.Decoder.Circuit +public import Complexity.Computability.Circuit.Boolean.Tableau.Decoder.Fields +public import Complexity.Computability.Circuit.Boolean.Tableau.Decoder.Shape public import Complexity.Computability.Circuit.Boolean.Tableau.Layout public import Complexity.Computability.Circuit.Boolean.Tableau.Space public import Complexity.Computability.Circuit.Boolean.Tableau.Succinct @@ -3162,6 +3166,7 @@ public import Complexity.Foundations.Data.Nat.ArithmeticProgression public import Complexity.Foundations.Data.Nat.Asymptotics public import Complexity.Foundations.Data.Nat.BinarySize public import Complexity.Foundations.Data.Nat.Bits +public import Complexity.Foundations.Data.Nat.Bitwise.Carry public import Complexity.Foundations.Data.Nat.Bitwise.HighestDiff public import Complexity.Foundations.Data.Nat.Bitwise.Multiplication public import Complexity.Foundations.Data.Nat.Bitwise.PackedCount diff --git a/Complexity/Computability/Circuit/Boolean/Tableau/Decoder/Assembly.lean b/Complexity/Computability/Circuit/Boolean/Tableau/Decoder/Assembly.lean new file mode 100644 index 0000000000..0b510a61b0 --- /dev/null +++ b/Complexity/Computability/Circuit/Boolean/Tableau/Decoder/Assembly.lean @@ -0,0 +1,361 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Boolean.Tableau.Decoder.Circuit +import Complexity.Foundations.Data.List.RowMajor +import Complexity.Foundations.Data.Nat.Doubling +import Mathlib.Data.Nat.Size + +/-! +# The decoder circuit of the succinct tableau + +The three stages of the decoder of the tableau formula on bit-field labels +(`Complexity/Computability/Circuit/Boolean/Tableau/Decoder/Circuit.lean`) composed into one +De Morgan circuit (`decoder`). From the bits of a clause number below `2 ^ clauseBits`, it computes +the bits of `Cslib.Circuits.Boolean.Tableau.clauseAt` (`ofFn_eval_decoder`). It has +`O(colBits T + timeBits T + x.length)` gates (`size_decoder_le`): the field stage has +`2 + N + 14 P + (2 ^ (Nat.size x.length + 1) - 1) + x.length` gates for `N = clauseBits` and +`P = N - 4`, the constant stage a number depending only on the machine, and the output stage `63` +gates per output bit. There is no carry-lookahead adder, whose size is not linear in the width. + +Its code is `decoderCode`, written with the code combinators `compCode`, `appendCode`, +`appendCodes` and `formulaCode` on the explicit gate list of the field stage and the constant code +of the constant stage (`code_decoder`). This is the decoder of the sketch of +[Williams, Theorem 6.1, p. 20][Williams2010]: the variables of the clauses of a cell differ from +cell to cell only by the block and the column, which enter through comparisons, increments and +decrements of fields. The sketch first converts the machine to a single-tape machine; this decoder +is built for the multi-tape tableau directly. + +## Main definitions + +* `Cslib.Circuits.Boolean.Tableau.Decoder.decoder`: the decoder circuit. +* `Cslib.Circuits.Boolean.Tableau.Decoder.decoderCode`: its code. +* `Cslib.Circuits.Boolean.Tableau.Decoder.sizeConst`: the constant of its size bound. + +## Main results + +* `Cslib.Circuits.Boolean.Tableau.Decoder.ofFn_eval_decoder`: the decoder computes the clause with + a given number, bit by bit. +* `Cslib.Circuits.Boolean.Tableau.Decoder.size_decoder_le`: it has + `O(colBits T + timeBits T + x.length)` gates. +* `Cslib.Circuits.Boolean.Tableau.Decoder.code_decoder`: its code is `decoderCode`. +* `Cslib.Circuits.Boolean.Tableau.Decoder.exists_decoder`: the three together. + +## References + +* [R. Williams, *Improving exhaustive search implies superpolynomial lower bounds*][Williams2010] +-/ + +@[expose] public section + +namespace Cslib.Circuits.Boolean.Tableau.Decoder + +open Turing MultiTapeTM Cslib.Logic.PL + +variable {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] + (tm : MultiTapeTM k Bool State) + +omit [DecidableEq State] in +/-- There is at least one slot bit. -/ +theorem one_le_slotBits : 1 ≤ slotBits k State := + Nat.size_pos.2 (Fintype.card_pos_iff.2 ⟨Loc.scan .nx⟩) + +/-- The selection of the inputs of the constant stage among the wires of the field stage. -/ +def keySel (s cb tb : ℕ) (x : List Bool) (n T : ℕ) : + Fin (4 + s + 14) → Fin (aWidth s cb tb x n T) := + fun i => ⟨keyWire s cb tb i, keyWire_lt i.isLt⟩ + +/-- The constant stage on the wires of the field stage, beside those wires. -/ +noncomputable def middleCircuit (x : List Bool) (n T : ℕ) : + Circuit signature (aWidth (slotBits k State) (colBits T) (timeBits T) x n T) + (aWidth (slotBits k State) (colBits T) (timeBits T) x n T + 3 * (13 + slotBits k State)) := + (Circuit.wiring signature id).append ((tableCircuit tm).comp + (Circuit.wiring signature (keySel (slotBits k State) (colBits T) (timeBits T) x n T))) + +/-- **The output stage**: one copy of `outTemplate` per output bit, on the wires `wireNat`. -/ +def outputCircuit (s cb tb : ℕ) (x : List Bool) (n T : ℕ) : + Circuit signature (aWidth s cb tb x n T + 3 * (13 + s)) (3 * (2 + (s + cb + tb) + 1)) := + Circuit.pi fun o => (outTemplate.rename fun j => + ⟨wireNat s cb tb x n T o j, wireNat_lt o.isLt j.isLt⟩).toCircuit + +/-- **The decoder circuit** of the tableau formula of `tm` on bit-field labels, for the fixed +prefix `x`, `n` inputs and `T` steps. -/ +noncomputable def decoder {x : List Bool} {n T : ℕ} + (hm : Nat.size x.length ≤ slotBits k State + colBits T + timeBits T) : + Circuit signature (4 + (slotBits k State + colBits T + timeBits T)) + (3 * (2 + (slotBits k State + colBits T + timeBits T) + 1)) := + (outputCircuit (slotBits k State) (colBits T) (timeBits T) x n T).comp + ((middleCircuit tm x n T).comp (fieldCircuit hm)) + +/-! ### The code -/ + +/-- **The code of the decoder**, written with the code combinators `compCode`, `appendCode`, +`appendCodes` and `formulaCode`: the field stage, the constant code of the constant stage, and one +instance of `outTemplate` per output bit (`code_decoder`). -/ +noncomputable def decoderCode : List Bool × ℕ × ℕ → List (Op × List ℕ) × List ℕ + | (x, n, T) => + compCode (4 + (slotBits k State + colBits T + timeBits T)) + (appendCodes (aWidth (slotBits k State) (colBits T) (timeBits T) x n T + + 3 * (13 + slotBits k State)) + ((List.range (3 * (2 + (slotBits k State + colBits T + timeBits T) + 1))).map + fun o => formulaCode (aWidth (slotBits k State) (colBits T) (timeBits T) x n + T + 3 * (13 + slotBits k State)) outTemplate + (fun j => wireNat (slotBits k State) (colBits T) (timeBits T) x n T o + j))) + (compCode (4 + (slotBits k State + colBits T + timeBits T)) + (appendCode (aWidth (slotBits k State) (colBits T) (timeBits T) x n T) + ([], List.range + (aWidth (slotBits k State) (colBits T) (timeBits T) x n T)) + (compCode (aWidth (slotBits k State) (colBits T) (timeBits T) x n T) + (tableCircuit tm).code + ([], (List.range (4 + slotBits k State + 14)).map + (keyWire (slotBits k State) (colBits T) (timeBits T))))) + (fieldGates (slotBits k State) (colBits T) (timeBits T) x n T, + List.range (aWidth (slotBits k State) (colBits T) (timeBits T) x n T))) + +/-- **The code of the decoder circuit is `decoderCode`.** -/ +theorem code_decoder {x : List Bool} {n T : ℕ} + (hm : Nat.size x.length ≤ slotBits k State + colBits T + timeBits T) : + (decoder (n := n) tm hm).code = decoderCode tm (x, n, T) := by + rw [decoder, ← compCode_code, middleCircuit, ← compCode_code, ← appendCode_code, + ← compCode_code, Circuit.code_wiring_id, code_fieldCircuit, outputCircuit, ← appendCodes_code, + Circuit.code_wiring_eq_map (g := keyWire (slotBits k State) (colBits T) (timeBits T)) + (fun j => rfl)] + simp only [decoderCode] + congr 2 + apply List.ext_getElem (by simp; omega) + intro o h₁ h₂ + simp only [List.getElem_ofFn, List.getElem_map, List.getElem_range] + exact (formulaCode_eq_code outTemplate _).symm + +/-! ### Size -/ + +theorem size_outputCircuit_le (s cb tb : ℕ) (x : List Bool) (n T : ℕ) : + (outputCircuit s cb tb x n T).size ≤ 3 * (2 + (s + cb + tb) + 1) * 63 := by + simp only [outputCircuit, Circuit.size_pi, Formula.size_toCircuit] + calc ∑ o : Fin (3 * (2 + (s + cb + tb) + 1)), (outTemplate.rename _).size + ≤ ∑ _o : Fin (3 * (2 + (s + cb + tb) + 1)), 63 := Finset.sum_le_sum fun o _ => by + have := Formula.size_bind_le (c := 0) (s := fun j => Formula.input + (⟨wireNat s cb tb x n T o j, wireNat_lt o.isLt j.isLt⟩ : + Fin (aWidth s cb tb x n T + 3 * (13 + s)))) (fun _ => le_rfl) outTemplate + simpa [Formula.rename, size_outTemplate] using this + _ = 3 * (2 + (s + cb + tb) + 1) * 63 := by simp + +/-- **The decoder has `O(colBits T + timeBits T + x.length)` gates**, with a constant depending +only on the machine. -/ +theorem size_decoder_le {x : List Bool} {n T : ℕ} + (hm : Nat.size x.length ≤ slotBits k State + colBits T + timeBits T) : + (decoder (n := n) tm hm).size ≤ (204 * slotBits k State + 600 + (tableCircuit tm).size) * + (colBits T + timeBits T + x.length + 1) := by + have hX := Nat.two_pow_size_le x.length + have hpow : 2 ^ (Nat.size x.length + 1) = 2 * 2 ^ Nat.size x.length := Nat.pow_succ' + have hout := size_outputCircuit_le (slotBits k State) (colBits T) (timeBits T) x n T + rw [decoder, Circuit.size_comp, Circuit.size_comp, middleCircuit, Circuit.size_append, + Circuit.size_comp, Circuit.size_wiring, Circuit.size_wiring, size_fieldCircuit, + length_fieldGates] + clear hm + generalize (tableCircuit tm).size = S at * + generalize (outputCircuit (slotBits k State) (colBits T) (timeBits T) x n T).size = O at * + generalize slotBits k State = s at * + generalize colBits T = cb at * + generalize timeBits T = tb at * + generalize x.length = X at * + generalize 2 ^ Nat.size X = Y at * + have h1 : 204 * s + 600 + S ≤ (204 * s + 600 + S) * (cb + tb + X + 1) := + Nat.le_mul_of_pos_right _ (by omega) + have h2 : 204 * (cb + tb + X) ≤ (204 * s + 600 + S) * (cb + tb + X) := + Nat.mul_le_mul_right _ (by omega) + rw [Nat.mul_add (204 * s + 600 + S) (cb + tb + X) 1, Nat.mul_one] at h1 ⊢ + rw [hpow] + omega + +/-! ### Correctness -/ + +theorem outBit_congr {s cb tb : ℕ} {ts ts' sel sel' : ℕ → Bool} + (hts : ∀ f < 2 + s, ts f = ts' f) (hsel : ∀ q < 11, sel q = sel' q) (p c t T : ℕ) (lk : Bool) + (i : ℕ) : outBit s cb tb ts sel p c t T lk i = outBit s cb tb ts' sel' p c t T lk i := by + unfold outBit payTerm colTerm timeTerm + simp only [hsel 0 (by omega), hsel 1 (by omega), hsel 2 (by omega), hsel 3 (by omega), + hsel 4 (by omega), hsel 5 (by omega), hsel 6 (by omega), hsel 7 (by omega), hsel 8 (by omega), + hsel 9 (by omega), hsel 10 (by omega)] + split_ifs with h1 h2 + · rw [hts i (by omega)] + · by_cases hq : i - 2 < s + · simp [hq, hts (2 + (i - 2)) (by omega)] + · simp [hq] + · rfl + +/-- The values of the wires of the field and constant stages. -/ +theorem eval_middle_field {x : List Bool} {n T : ℕ} + (hm : Nat.size x.length ≤ slotBits k State + colBits T + timeBits T) (idx : ℕ) + (w : Fin (aWidth (slotBits k State) (colBits T) (timeBits T) x n T + + 3 * (13 + slotBits k State))) : + ((middleCircuit tm x n T).comp (fieldCircuit hm)).eval interpretation + (fun i => idx.testBit i) w = + if h : w.val < aWidth (slotBits k State) (colBits T) (timeBits T) x n T then + fieldVal (slotBits k State) (colBits T) (timeBits T) x n T idx w + else tableFn tm (fun i => fieldVal (slotBits k State) (colBits T) (timeBits T) x n T idx + (keyWire (slotBits k State) (colBits T) (timeBits T) i)) + ⟨w.val - aWidth (slotBits k State) (colBits T) (timeBits T) x n T, by omega⟩ := by + rw [Circuit.eval_comp, middleCircuit, Circuit.eval_append] + split + · rename_i h + have hw : w = Fin.castAdd _ ⟨w.val, h⟩ := rfl + conv_lhs => rw [hw] + rw [Fin.append_left, Circuit.eval_wiring, Function.comp_apply, id, eval_fieldCircuit] + · rename_i h + have hw : w = Fin.natAdd _ (⟨w.val - aWidth (slotBits k State) (colBits T) (timeBits T) x n T, + by omega⟩ : Fin (3 * (13 + slotBits k State))) := by ext; simp; omega + conv_lhs => rw [hw] + rw [Fin.append_right, Circuit.eval_comp, Circuit.eval_wiring, eval_tableCircuit] + congr 1 + funext i + simp [keySel, eval_fieldCircuit] + +theorem getElem?_litBits (w : ℕ) (l : Literal ℕ) {i : ℕ} (hi : i < w + 1) : + (litBits w l)[i]? = some (if i < w then l.1.testBit i else l.2) := by + unfold litBits + split + · rename_i h + rw [List.getElem?_append_left (by simpa using h)] + simp [h] + · rename_i h + rw [List.getElem?_append_right (by simp; omega)] + simp [show i - w = 0 by omega] + +/-- **The decoder computes the clause with a given number**: its outputs are the bits of the +three literals of `clauseAt`, for `n < 2 T` and a fixed prefix of length at most `n`. -/ +theorem ofFn_eval_decoder {x : List Bool} {n T : ℕ} (hn : n < 2 * T) (hx : x.length ≤ n) + (hm : Nat.size x.length ≤ slotBits k State + colBits T + timeBits T) {idx : ℕ} + (hidx : idx < 2 ^ (4 + (slotBits k State + colBits T + timeBits T))) : + List.ofFn ((decoder (n := n) tm hm).eval interpretation (fun i => idx.testBit i)) = + (clauseAt tm x n T idx).flatMap + (litBits (2 + (slotBits k State + colBits T + timeBits T))) := by + have hs := one_le_slotBits (k := k) (State := State) + have h2T : 2 * T < 2 ^ colBits T := Nat.lt_size_self _ + have hT : T < 2 ^ timeBits T := Nat.lt_size_self _ + have hkey := ofBits_keyWire (x := x) (n := n) (T := T) hidx hs h2T hT hn hx + have hcl := clauseOf_eq_map_shapeOf tm x n T (idx % 4) (idx / 4 % 4) (idx / 16) + rw [clauseAt, hcl] + generalize hκ : Key.ofFields (slotBits k State) (colBits T) x.length n T (idx % 4) (idx / 4 % 4) + (idx / 16) = κ at hkey + have hlen := length_shapeOf tm κ + apply List.ext_getElem? + intro o + rw [List.getElem?_ofFn] + by_cases ho : o < 3 * (2 + (slotBits k State + colBits T + timeBits T) + 1) + · have hr : o / (2 + (slotBits k State + colBits T + timeBits T) + 1) < 3 := + Nat.div_lt_of_lt_mul (by rwa [Nat.mul_comm]) + have hi : o % (2 + (slotBits k State + colBits T + timeBits T) + 1) < + 2 + (slotBits k State + colBits T + timeBits T) + 1 := Nat.mod_lt _ (by omega) + rw [dite_eq_left ho] + conv_rhs => rw [← Nat.div_add_mod' o (2 + (slotBits k State + colBits T + timeBits T) + 1)] + rw [List.getElem?_flatMap_mul_add _ _ _ (fun _ _ => by simp [litBits]) (by simpa [hlen]) hi] + rw [List.getElem_map, getElem?_litBits _ _ hi] + congr 1 + -- the left side + rw [decoder, Circuit.eval_comp] + simp only [outputCircuit, Circuit.eval_pi, Formula.eval_toCircuit, Formula.eval_rename] + set z' := ((middleCircuit tm x n T).comp (fieldCircuit hm)).eval interpretation + (fun i => idx.testBit i) with hz' + let z : ℕ → Bool := fun w => if h : w < aWidth (slotBits k State) (colBits T) (timeBits T) + x n T + 3 * (13 + slotBits k State) then z' ⟨w, h⟩ else false + have hzz : (z' ∘ fun j : Fin 28 => (⟨wireNat (slotBits k State) (colBits T) (timeBits T) x n T + o j, wireNat_lt ho j.isLt⟩ : Fin _)) = + fun j : Fin 28 => z (wireNat (slotBits k State) (colBits T) (timeBits T) x n T o j) := by + funext j + simp [z, wireNat_lt ho j.isLt] + have hF : ∀ w < aWidth (slotBits k State) (colBits T) (timeBits T) x n T, + z w = fieldVal (slotBits k State) (colBits T) (timeBits T) x n T idx w := by + intro w hw + simp only [z, show w < aWidth (slotBits k State) (colBits T) (timeBits T) x n T + + 3 * (13 + slotBits k State) by omega, ↓reduceDIte, hz', eval_middle_field, hw] + rw [hzz, eval_outTemplate_wireNat hidx hF] + set r := o / (2 + (slotBits k State + colBits T + timeBits T) + 1) with hrdef + set i := o % (2 + (slotBits k State + colBits T + timeBits T) + 1) with hidef + set sh := (shapeOf tm κ).getD r defaultShape with hsh + have hsh' : sh = (shapeOf tm κ)[r]'(by omega) := by + rw [hsh, List.getD_eq_getElem?_getD, List.getElem?_eq_getElem (by omega)] + rfl + have htab (f : ℕ) (hf : f < 13 + slotBits k State) : + z (aWidth (slotBits k State) (colBits T) (timeBits T) x n T + r * (13 + slotBits k State) + + f) = if f < 2 + slotBits k State then tagSlot sh f + else selOf κ.c0 κ.t0 sh (f - (2 + slotBits k State)) := by + have hlt : r * (13 + slotBits k State) + f < 3 * (13 + slotBits k State) := by + have : r * (13 + slotBits k State) + (13 + slotBits k State) ≤ + 3 * (13 + slotBits k State) := by + rw [← Nat.succ_mul]; exact Nat.mul_le_mul_right _ hr + omega + simp only [z, show aWidth (slotBits k State) (colBits T) (timeBits T) x n T + + r * (13 + slotBits k State) + f < aWidth (slotBits k State) (colBits T) (timeBits T) x n T + + 3 * (13 + slotBits k State) by omega, ↓reduceDIte, hz', eval_middle_field, + show ¬ aWidth (slotBits k State) (colBits T) (timeBits T) x n T + + r * (13 + slotBits k State) + f < aWidth (slotBits k State) (colBits T) (timeBits T) x n T + by omega] + simp only [tableFn, hkey] + have h₁ : (aWidth (slotBits k State) (colBits T) (timeBits T) x n T + + r * (13 + slotBits k State) + f - aWidth (slotBits k State) (colBits T) (timeBits T) + x n T) = r * (13 + slotBits k State) + f := by omega + have h₂ : (r * (13 + slotBits k State) + f) / (13 + slotBits k State) = r := by + rw [Nat.mul_comm, Nat.mul_add_div (by omega), Nat.div_eq_of_lt hf, Nat.add_zero] + have h₃ : (r * (13 + slotBits k State) + f) % (13 + slotBits k State) = f := by + rw [Nat.mul_comm, Nat.mul_add_mod, Nat.mod_eq_of_lt hf] + simp only [h₁, h₂, h₃, hsh] + rw [outBit_congr (ts' := tagSlot sh) (sel' := selOf κ.c0 κ.t0 sh) + (fun f hf => by rw [htab f (by omega), ite_eq_left hf]) + (fun q hq => by rw [htab _ (by omega), ite_eq_right (by omega), Nat.add_sub_cancel_left])] + have hmem : sh ∈ shapeOf tm κ := by rw [hsh']; exact List.getElem_mem _ + have hc0 : κ.c0 = decide (colOf (slotBits k State) (colBits T) (idx / 16) = 0) := by + rw [← hκ]; rfl + have ht0 : κ.t0 = decide (timeOf (slotBits k State) (colBits T) (idx / 16) = 0) := by + rw [← hκ]; rfl + rw [hc0, ht0] + rw [← hκ] at hmem + rw [outBit_shape (x := x) hs (inRange_of_mem_shapeOf tm hmem) ?_ (by omega), ← hsh'] + · rfl + · intro hl + have hp := lt_of_mem_shapeOf tm hmem hl + have hX := Nat.lt_size_self x.length + have hlk : lookW (slotBits k State) (colBits T) (timeBits T) x < + aWidth (slotBits k State) (colBits T) (timeBits T) x n T := lookW_lt + rw [hF _ hlk, lookW, ite_eq_right (by omega), fieldVal_or, + Nat.mod_eq_of_lt (show idx / 16 < 2 ^ Nat.size x.length by omega)] + simp [show idx / 16 ≤ x.length - 1 by omega] + · rw [dite_eq_right ho, eq_comm, List.getElem?_eq_none] + rw [List.length_flatMap, List.map_congr_left (fun a _ => show (litBits + (2 + (slotBits k State + colBits T + timeBits T)) a).length = + 2 + (slotBits k State + colBits T + timeBits T) + 1 by simp [litBits])] + simp only [List.map_const', List.sum_replicate, smul_eq_mul, List.length_map, hlen] + omega + +/-! ### The decoder of the succinct tableau -/ + +/-- The constant of the size bound of the decoder, which depends only on the machine. -/ +noncomputable def sizeConst : ℕ := 204 * slotBits k State + 600 + (tableCircuit tm).size + +/-- **The decoder of the succinct tableau formula**: for `n < 2 T` and a fixed prefix `x` of length +at most `n`, a De Morgan circuit with code `decoderCode tm (x, n, T)` and at most +`sizeConst tm * (colBits T + timeBits T + x.length + 1)` gates computes, from the bits of a clause +number below `2 ^ clauseBits`, the bits of the clause `clauseAt tm x n T idx` of +`Cslib.Circuits.Boolean.Tableau.succinctCNF`: the label of each of its three literals in +`labelBits` bits, least significant first, then its sign. -/ +theorem exists_decoder (x : List Bool) {n T : ℕ} (hn : n < 2 * T) (hx : x.length ≤ n) : + ∃ c : Circuit signature (clauseBits k State T) (3 * (labelBits k State T + 1)), + c.code = decoderCode tm (x, n, T) ∧ + c.size ≤ sizeConst tm * (colBits T + timeBits T + x.length + 1) ∧ + ∀ idx < 2 ^ clauseBits k State T, + List.ofFn (c.eval interpretation fun i => idx.testBit i) = + (clauseAt tm x n T idx).flatMap (litBits (labelBits k State T)) := by + have hm : Nat.size x.length ≤ slotBits k State + colBits T + timeBits T := by + have : Nat.size x.length ≤ colBits T := Nat.size_le_size (by omega) + omega + exact ⟨decoder (n := n) tm hm, code_decoder tm hm, size_decoder_le tm hm, + fun idx hidx => ofFn_eval_decoder tm hn hx hm hidx⟩ + +end Cslib.Circuits.Boolean.Tableau.Decoder diff --git a/Complexity/Computability/Circuit/Boolean/Tableau/Decoder/Circuit.lean b/Complexity/Computability/Circuit/Boolean/Tableau/Decoder/Circuit.lean new file mode 100644 index 0000000000..ce96d301a7 --- /dev/null +++ b/Complexity/Computability/Circuit/Boolean/Tableau/Decoder/Circuit.lean @@ -0,0 +1,611 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Boolean.Tableau.Decoder.Fields +public import Complexity.Computability.Circuit.Boolean.Tableau.Decoder.Shape +public import Complexity.Computability.Circuit.Boolean.CodeTemplate +public import Complexity.Computability.Circuit.Pi +import Mathlib.Data.Nat.Size + +/-! +# The stages of the decoder circuit of the succinct tableau + +The decoder computes, from the bits of a clause number, the bits of the clause of the tableau +formula on bit-field labels (`Cslib.Circuits.Boolean.Tableau.clauseAt`): for each of its three +literals, the label in `labelBits` bits, least significant first, then the sign (`litBits`). It +composes three stages: + +* the field stage (`Complexity/Computability/Circuit/Boolean/Tableau/Decoder/Fields.lean`): + comparison chains, borrows and carries, and the lookup of the fixed prefix `x`; +* a circuit of constant size (`tableCircuit`) that computes the shapes of the three literals + (`Complexity/Computability/Circuit/Boolean/Tableau/Decoder/Shape.lean`) from the clause and tag + bits, the slot bits and the comparisons (`ofBits_keyWire`); +* the output stage: one copy of a fixed formula of 63 gates (`outTemplate`) per output bit, reading + the wires `wireNat`, which selects the bit of the label from the fields chosen by the shape + (`eval_outTemplate_wireNat`). + +The stages are assembled, with the correctness and the linear size of the whole circuit, in +`Complexity/Computability/Circuit/Boolean/Tableau/Decoder/Assembly.lean`. + +## Main definitions + +* `Cslib.Circuits.Boolean.Tableau.Decoder.litBits`: the bits of a literal. +* `Cslib.Circuits.Boolean.Tableau.Decoder.outTemplate`: the formula of an output bit. +* `Cslib.Circuits.Boolean.Tableau.Decoder.tableFn`, + `Cslib.Circuits.Boolean.Tableau.Decoder.tableCircuit`: the constant stage. +* `Cslib.Circuits.Boolean.Tableau.Decoder.wireNat`, + `Cslib.Circuits.Boolean.Tableau.Decoder.keyWire`: the wires read by the output stage and by the + constant stage. +* `Cslib.Circuits.Boolean.Tableau.Decoder.fieldCircuit`: the field stage as a circuit. + +## Main results + +* `Cslib.Circuits.Boolean.Tableau.Decoder.eval_fieldCircuit`: the field stage computes the intended + values. +* `Cslib.Circuits.Boolean.Tableau.Decoder.ofBits_keyWire`: the constant stage reads the key of the + fields of the clause number. +* `Cslib.Circuits.Boolean.Tableau.Decoder.eval_outTemplate_wireNat`: each output bit computes + `outBit`. + +## References + +* [R. Williams, *Improving exhaustive search implies superpolynomial lower bounds*][Williams2010] +-/ + +@[expose] public section + +namespace Cslib.Circuits.Boolean.Tableau.Decoder + +open Turing MultiTapeTM Cslib.Logic.PL + +/-! ### The formula of an output bit -/ + +/-- Input `j` of the formula of an output bit. -/ +def tIn (j : ℕ) (h : j < 28 := by omega) : Formula signature 28 := .input ⟨j, h⟩ + +/-- Term `k` of the formula of an output bit: a selector and the exclusive or of two bits. -/ +def term (k : ℕ) (h : 3 * k + 3 < 28 := by omega) : Formula signature 28 := + (tIn (1 + 3 * k)).and ((tIn (2 + 3 * k)).xor (tIn (3 + 3 * k))) + +/-- **The formula of an output bit**: the input `0`, or one of nine terms, each the conjunction +of a selector with the exclusive or of two bits. -/ +def outTemplate : Formula signature 28 := + (tIn 0).or ((term 0).or ((term 1).or ((term 2).or ((term 3).or ((term 4).or ((term 5).or + ((term 6).or ((term 7).or (term 8))))))))) + +theorem eval_outTemplate (y : Fin 28 → Bool) : + outTemplate.eval interpretation y = + (y 0 || (y 1 && (y 2 ^^ y 3)) || (y 4 && (y 5 ^^ y 6)) || (y 7 && (y 8 ^^ y 9)) || + (y 10 && (y 11 ^^ y 12)) || (y 13 && (y 14 ^^ y 15)) || (y 16 && (y 17 ^^ y 18)) || + (y 19 && (y 20 ^^ y 21)) || (y 22 && (y 23 ^^ y 24)) || (y 25 && (y 26 ^^ y 27))) := by + simp only [outTemplate, term, tIn, Formula.eval_or, Formula.eval_and, Formula.eval_xor, + Formula.eval_input, Bool.or_assoc] + rfl + +/-- The formula of an output bit on the values of numbered wires. -/ +theorem eval_outTemplate_nat (y : ℕ → Bool) : + outTemplate.eval interpretation (fun j => y j) = + (y 0 || (y 1 && (y 2 ^^ y 3)) || (y 4 && (y 5 ^^ y 6)) || (y 7 && (y 8 ^^ y 9)) || + (y 10 && (y 11 ^^ y 12)) || (y 13 && (y 14 ^^ y 15)) || (y 16 && (y 17 ^^ y 18)) || + (y 19 && (y 20 ^^ y 21)) || (y 22 && (y 23 ^^ y 24)) || (y 25 && (y 26 ^^ y 27))) := + eval_outTemplate _ + +theorem size_outTemplate : outTemplate.size = 63 := by + simp [outTemplate, term, tIn] + +/-! ### The bits of a literal -/ + +/-- **The bits of a literal**: its label in `w` bits, least significant first, then its sign. -/ +def litBits (w : ℕ) (l : Literal ℕ) : List Bool := + List.ofFn (fun i : Fin w => l.1.testBit i) ++ [l.2] + +/-! ### The constant stage -/ + +/-- The bit `i` of a bit string, or `false`. -/ +def bitAt {m : ℕ} (b : BitString m) (i : ℕ) : Bool := if h : i < m then b ⟨i, h⟩ else false + +/-- The key of the input bits of the constant stage: the clause and tag bits, `s` slot bits, +and the fourteen comparison chains. -/ +def Key.ofBits (s : ℕ) {m : ℕ} (b : BitString m) : Key where + j := (bitAt b 0).toNat + 2 * (bitAt b 1).toNat + tag := (bitAt b 2).toNat + 2 * (bitAt b 3).toNat + slot := Nat.ofBits fun i : Fin s => bitAt b (4 + i) + c0 := bitAt b (4 + s) + cGt1 := bitAt b (4 + s + 3) + cGtN := bitAt b (4 + s + 4) + cGtN1 := bitAt b (4 + s + 5) + cLt2T := bitAt b (4 + s + 6) + cGt2T := bitAt b (4 + s + 7) + cLtT := bitAt b (4 + s + 8) + cGtT := bitAt b (4 + s + 9) + t0 := bitAt b (4 + s + 2) + tGtT := bitAt b (4 + s + 10) + pLtX := bitAt b (4 + s + 11) + p0 := bitAt b (4 + s + 12) + pGt1 := bitAt b (4 + s + 13) + +variable {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] + (tm : MultiTapeTM k Bool State) + +/-- The default shape. -/ +def defaultShape : Shape := (.const false, .const false) + +/-- **The function of the constant stage**: bit `f` of literal `r` (`f < 13 + s`) is a tag or slot +bit or a selector of the shape of literal `r` of the key of the input bits. -/ +noncomputable def tableFn (b : BitString (4 + slotBits k State + 14)) + (o : Fin (3 * (13 + slotBits k State))) : Bool := + let κ := Key.ofBits (slotBits k State) b + let sh := (shapeOf tm κ).getD (o / (13 + slotBits k State)) defaultShape + if o % (13 + slotBits k State) < 2 + slotBits k State then + tagSlot sh (o % (13 + slotBits k State)) + else selOf κ.c0 κ.t0 sh (o % (13 + slotBits k State) - (2 + slotBits k State)) + +/-- **The constant stage**: a circuit computing `tableFn`, one disjunctive normal form per output. +Its size depends only on the machine. -/ +noncomputable def tableCircuit : + Circuit signature (4 + slotBits k State + 14) (3 * (13 + slotBits k State)) := + Circuit.pi fun o => + (Classical.choose (Formula.exists_computes (fun b => tableFn tm b o))).toCircuit + +theorem eval_tableCircuit (b : BitString (4 + slotBits k State + 14)) : + (tableCircuit tm).eval interpretation b = tableFn tm b := by + funext o + simp only [tableCircuit, Circuit.eval_pi, Formula.eval_toCircuit] + exact Classical.choose_spec (Formula.exists_computes (fun b => tableFn tm b o)) b + +/-! ### The wires of the output stage -/ + +/-- The wire of the constant `b`, after `N` inputs. -/ +def constW (N : ℕ) (b : Bool) : ℕ := if b then N + 1 else N + +/-- The wire of bit `q` of the field of width `w` at offset `off`, or of `false`. -/ +def bitW (N off w q : ℕ) : ℕ := if q < w then off + q else N + +/-- The wire of chain `k` after `q` bits, `true` for `q = 0`. -/ +def chainW (N P k q : ℕ) : ℕ := if q = 0 then N + 1 else chainBase N + k * P + (q - 1) + +/-- The first wire of the term `kk` of the payload bit `q`. -/ +def uWire (s cb tb T q kk : ℕ) : ℕ := + if kk = 0 then 4 + q + else if kk = 1 then bitW (4 + (s + cb + tb)) (4 + s) cb q + else if kk ≤ 5 then + (if s ≤ q ∧ q < s + cb then + (if kk = 5 then constW (4 + (s + cb + tb)) ((2 * T).testBit (q - s)) + else bitW (4 + (s + cb + tb)) (4 + s) cb (q - s)) + else 4 + (s + cb + tb)) + else if kk ≤ 8 then + (if s + cb ≤ q then + (if kk = 8 then constW (4 + (s + cb + tb)) (T.testBit (q - s - cb)) + else bitW (4 + (s + cb + tb)) (4 + s + cb) tb (q - s - cb)) + else 4 + (s + cb + tb)) + else 4 + (s + cb + tb) + +/-- The second wire of the term `kk` of the payload bit `q`: a borrow or a carry. -/ +def vWire (s cb tb q kk : ℕ) : ℕ := + if kk = 1 then chainW (4 + (s + cb + tb)) (s + cb + tb) 0 q + else if kk = 3 then + (if s ≤ q ∧ q < s + cb then chainW (4 + (s + cb + tb)) (s + cb + tb) 0 (q - s) + else 4 + (s + cb + tb)) + else if kk = 4 then + (if s ≤ q ∧ q < s + cb then chainW (4 + (s + cb + tb)) (s + cb + tb) 1 (q - s) + else 4 + (s + cb + tb)) + else if kk = 7 then + (if s + cb ≤ q then chainW (4 + (s + cb + tb)) (s + cb + tb) 2 (q - s - cb) + else 4 + (s + cb + tb)) + else 4 + (s + cb + tb) + +/-- The number of wires of the field stage. -/ +def aWidth (s cb tb : ℕ) (x : List Bool) (n T : ℕ) : ℕ := + 4 + (s + cb + tb) + (fieldGates s cb tb x n T).length + +/-- The wire of the lookup of `x`. -/ +def lookW (s cb tb : ℕ) (x : List Bool) : ℕ := + if x.length = 0 then 4 + (s + cb + tb) + else orBase (4 + (s + cb + tb)) (s + cb + tb) (Nat.size x.length) + (x.length - 1) + +/-- **The wire read at input `j` of the formula of output bit `o`** of the output stage. Output +`o` is bit `o % (3 + P)` of literal `o / (3 + P)`, where `P = s + cb + tb`: two tag bits, `P` +payload bits and the sign. The output `r * (13 + s) + f` of the constant stage is wire +`aWidth + r * (13 + s) + f`. -/ +def wireNat (s cb tb : ℕ) (x : List Bool) (n T o j : ℕ) : ℕ := + if o % (2 + (s + cb + tb) + 1) < 2 then + (if j = 0 then aWidth s cb tb x n T + o / (2 + (s + cb + tb) + 1) * (13 + s) + + o % (2 + (s + cb + tb) + 1) else 4 + (s + cb + tb)) + else if o % (2 + (s + cb + tb) + 1) < 2 + (s + cb + tb) then + (if j = 0 then + (if o % (2 + (s + cb + tb) + 1) - 2 < s then + aWidth s cb tb x n T + o / (2 + (s + cb + tb) + 1) * (13 + s) + o % (2 + (s + cb + tb) + 1) + else 4 + (s + cb + tb)) + else if (j - 1) % 3 = 0 then + aWidth s cb tb x n T + o / (2 + (s + cb + tb) + 1) * (13 + s) + (2 + s + (j - 1) / 3) + else if (j - 1) % 3 = 1 then uWire s cb tb T (o % (2 + (s + cb + tb) + 1) - 2) ((j - 1) / 3) + else vWire s cb tb (o % (2 + (s + cb + tb) + 1) - 2) ((j - 1) / 3)) + else + (if j = 0 then aWidth s cb tb x n T + o / (2 + (s + cb + tb) + 1) * (13 + s) + (2 + s + 9) + else if j = 1 then aWidth s cb tb x n T + o / (2 + (s + cb + tb) + 1) * (13 + s) + (2 + s + 10) + else if j = 2 then lookW s cb tb x + else 4 + (s + cb + tb)) + +/-- The wire of input `i` of the constant stage: a clause, tag or slot bit, or the last gate of a +comparison chain. -/ +def keyWire (s cb tb i : ℕ) : ℕ := + if i < 4 + s then i + else chainBase (4 + (s + cb + tb)) + (i - (4 + s)) * (s + cb + tb) + (s + cb + tb - 1) + +/-! ### Wire bounds -/ + +section Bounds + +variable {s cb tb : ℕ} {x : List Bool} {n T : ℕ} + +theorem chainBase_add_lt_aWidth {k q : ℕ} (hk : k < 14) (hq : q < s + cb + tb) : + chainBase (4 + (s + cb + tb)) + k * (s + cb + tb) + q < aWidth s cb tb x n T := by + have h₁ : k * (s + cb + tb) + (s + cb + tb) ≤ 14 * (s + cb + tb) := by + rw [← Nat.succ_mul]; exact Nat.mul_le_mul_right _ hk + simp only [aWidth, length_fieldGates, chainBase] + omega + +theorem lt_aWidth_of_lt {w : ℕ} (hw : w < 2 * (4 + (s + cb + tb)) + 2) : + w < aWidth s cb tb x n T := by + simp only [aWidth, length_fieldGates] + omega + +theorem constW_lt (b : Bool) : constW (4 + (s + cb + tb)) b < aWidth s cb tb x n T := + lt_aWidth_of_lt (by unfold constW; split <;> omega) + +theorem bitW_lt {off w q : ℕ} (h : off + w ≤ 4 + (s + cb + tb)) : + bitW (4 + (s + cb + tb)) off w q < aWidth s cb tb x n T := + lt_aWidth_of_lt (by unfold bitW; split <;> omega) + +theorem chainW_lt {k q : ℕ} (hk : k < 14) (hq : q ≤ s + cb + tb) : + chainW (4 + (s + cb + tb)) (s + cb + tb) k q < aWidth s cb tb x n T := by + unfold chainW + split + · exact lt_aWidth_of_lt (by omega) + · exact chainBase_add_lt_aWidth hk (by omega) + +theorem uWire_lt (q kk : ℕ) (hq : q < s + cb + tb) : + uWire s cb tb T q kk < aWidth s cb tb x n T := by + unfold uWire + split_ifs <;> first + | exact lt_aWidth_of_lt (by omega) + | exact constW_lt _ + | exact bitW_lt (by omega) + +theorem vWire_lt (q kk : ℕ) (hq : q < s + cb + tb) : + vWire s cb tb q kk < aWidth s cb tb x n T := by + unfold vWire + split_ifs <;> first + | exact lt_aWidth_of_lt (by omega) + | exact chainW_lt (by omega) (by omega) + +theorem lookW_lt : lookW s cb tb x < aWidth s cb tb x n T := by + unfold lookW + split + · exact lt_aWidth_of_lt (by omega) + · simp only [aWidth, length_fieldGates, orBase, treeBase, chainBase] + omega + +/-- The wires of the output stage lie among the wires of the field and constant stages. -/ +theorem wireNat_lt {o j : ℕ} (ho : o < 3 * (2 + (s + cb + tb) + 1)) (hj : j < 28) : + wireNat s cb tb x n T o j < aWidth s cb tb x n T + 3 * (13 + s) := by + have hj3 : (j - 1) / 3 ≤ 8 := by omega + have hr : o / (2 + (s + cb + tb) + 1) < 3 := Nat.div_lt_of_lt_mul (by rwa [Nat.mul_comm]) + have hr' : o / (2 + (s + cb + tb) + 1) * (13 + s) + (13 + s) ≤ 3 * (13 + s) := by + rw [← Nat.succ_mul]; exact Nat.mul_le_mul_right _ hr + have hU := fun kk (hq : o % (2 + (s + cb + tb) + 1) - 2 < s + cb + tb) => + uWire_lt (x := x) (n := n) (T := T) (o % (2 + (s + cb + tb) + 1) - 2) kk hq + have hV := fun kk (hq : o % (2 + (s + cb + tb) + 1) - 2 < s + cb + tb) => + vWire_lt (x := x) (n := n) (T := T) (o % (2 + (s + cb + tb) + 1) - 2) kk hq + have hL := lookW_lt (s := s) (cb := cb) (tb := tb) (x := x) (n := n) (T := T) + have hN : 4 + (s + cb + tb) < aWidth s cb tb x n T := lt_aWidth_of_lt (by omega) + unfold wireNat + split_ifs + all_goals first + | omega + | (have := hU ((j - 1) / 3) (by omega); omega) + | (have := hV ((j - 1) / 3) (by omega); omega) + +theorem keyWire_lt {i : ℕ} (hi : i < 4 + s + 14) : keyWire s cb tb i < aWidth s cb tb x n T := by + unfold keyWire + split + · exact lt_aWidth_of_lt (by omega) + · have h₁ : (i - (4 + s)) * (s + cb + tb) + (s + cb + tb) ≤ 14 * (s + cb + tb) := by + rw [← Nat.succ_mul]; exact Nat.mul_le_mul_right _ (by omega) + have := Nat.one_le_two_pow (n := Nat.size x.length + 1) + simp only [aWidth, length_fieldGates, chainBase] + omega + +end Bounds + +/-! ### The circuit -/ + +section Assembly + +variable {s cb tb : ℕ} {x : List Bool} {n T : ℕ} + +theorem isSome_fieldCode (hm : Nat.size x.length ≤ s + cb + tb) : + (Circuit.ofCode (σ := signature) (4 + (s + cb + tb)) (aWidth s cb tb x n T) + (fieldGates s cb tb x n T, List.range (aWidth s cb tb x n T))).isSome := by + rw [Circuit.isSome_ofCode_iff] + refine ⟨isCodeFrom_of_allGates (allGates_wellFormedAt_fieldGates hm), by simp, fun i hi => ?_⟩ + simpa [aWidth] using hi + +/-- **The field stage** as a circuit whose outputs are all its wires. -/ +noncomputable def fieldCircuit (hm : Nat.size x.length ≤ s + cb + tb) : + Circuit signature (4 + (s + cb + tb)) (aWidth s cb tb x n T) := + (Circuit.ofCode _ _ (fieldGates s cb tb x n T, List.range (aWidth s cb tb x n T))).get + (isSome_fieldCode hm) + +theorem code_fieldCircuit (hm : Nat.size x.length ≤ s + cb + tb) : + (fieldCircuit (n := n) (T := T) hm).code = + (fieldGates s cb tb x n T, List.range (aWidth s cb tb x n T)) := + Circuit.code_of_ofCode_eq_some (Option.some_get _).symm + +theorem size_fieldCircuit (hm : Nat.size x.length ≤ s + cb + tb) : + (fieldCircuit (n := n) (T := T) hm).size = (fieldGates s cb tb x n T).length := by + rw [← Circuit.length_code_fst, code_fieldCircuit] + +theorem eval_fieldCircuit (hm : Nat.size x.length ≤ s + cb + tb) (idx : ℕ) + (w : Fin (aWidth s cb tb x n T)) : + (fieldCircuit hm).eval interpretation (fun i => idx.testBit i) w = + fieldVal s cb tb x n T idx w := by + have hout : ((fieldCircuit (n := n) (T := T) hm).outputs w).toNat = w := by + have h := congrArg Prod.snd (code_fieldCircuit (n := n) (T := T) hm) + simp only [Circuit.code] at h + have := congrArg (fun l => l[w.val]?) h + simpa using this + rw [Circuit.eval_eq_evalOutput, code_fieldCircuit, hout, evalOutput] + exact getD_evalCode_fieldGates hm idx (by simpa [aWidth] using w.isLt) + +end Assembly + +/-! ### Values of the wires read by the output stage -/ + +section Values + +variable {s cb tb : ℕ} {x : List Bool} {n T : ℕ} + +theorem fieldVal_constW (idx : ℕ) (b : Bool) : + fieldVal s cb tb x n T idx (constW (4 + (s + cb + tb)) b) = b := by + cases b + · exact fieldVal_false idx + · exact fieldVal_true idx + +theorem fieldVal_bitW (idx : ℕ) {off w q : ℕ} (h : off + w ≤ 4 + (s + cb + tb)) : + fieldVal s cb tb x n T idx (bitW (4 + (s + cb + tb)) off w q) = + (idx / 2 ^ off % 2 ^ w).testBit q := by + unfold bitW + split + · rw [fieldVal_input idx (by omega), Nat.testBit_mod_two_pow, Nat.testBit_div_two_pow] + simp [*, Nat.add_comm] + · rw [fieldVal_false, Nat.testBit_mod_two_pow] + simp [*] + +theorem fieldVal_payload (idx : ℕ) {q : ℕ} (hq : q < s + cb + tb) : + fieldVal s cb tb x n T idx (4 + q) = (idx / 16).testBit q := by + rw [fieldVal_input idx (by omega), show idx / 16 = idx / 2 ^ 4 from rfl, + Nat.testBit_div_two_pow, Nat.add_comm] + +/-- The value of chain `k` after `q` bits, through `chainW`. -/ +theorem fieldVal_chainW (idx : ℕ) {k q : ℕ} (hk : k < 14) (hq : q ≤ s + cb + tb) + (hinit : (chain s cb tb x.length n T k).init = true) : + fieldVal s cb tb x n T idx (chainW (4 + (s + cb + tb)) (s + cb + tb) k q) = + chainVal (chain s cb tb x.length n T k) idx q := by + unfold chainW + split + · subst q + rw [fieldVal_true] + simp [chainVal, cmp, hinit, Nat.mod_one] + · rw [fieldVal_chain idx hk (by omega), Nat.sub_add_cancel (by omega)] + +/-- The column of the payload, from the clause number. -/ +theorem div_mod_eq_colOf (idx : ℕ) : + idx / 2 ^ (4 + s) % 2 ^ cb = colOf s cb (idx / 16) := by + rw [colOf, Nat.pow_add, ← Nat.div_div_eq_div_mul] + +/-- The block of the payload, from a clause number of `4 + (s + cb + tb)` bits. -/ +theorem div_mod_eq_timeOf {idx : ℕ} (hidx : idx < 2 ^ (4 + (s + cb + tb))) : + idx / 2 ^ (4 + s + cb) % 2 ^ tb = timeOf s cb (idx / 16) := by + have h₁ : idx / 2 ^ (4 + s + cb) = timeOf s cb (idx / 16) := by + rw [timeOf, Nat.pow_add, Nat.pow_add, ← Nat.div_div_eq_div_mul, ← Nat.div_div_eq_div_mul] + rw [h₁, Nat.mod_eq_of_lt] + rw [← h₁] + apply Nat.div_lt_of_lt_mul + rw [← Nat.pow_add] + calc idx < 2 ^ (4 + (s + cb + tb)) := hidx + _ = 2 ^ (4 + s + cb + tb) := by congr 1; omega + +theorem fieldVal_borrowC (idx : ℕ) {q : ℕ} (hq : q ≤ s + cb + tb) : + fieldVal s cb tb x n T idx (chainW (4 + (s + cb + tb)) (s + cb + tb) 0 q) = + decide (colOf s cb (idx / 16) % 2 ^ q = 0) := by + rw [fieldVal_chainW idx (by omega) hq rfl] + simp only [chainVal, chain, ↓reduceIte, cmp, Nat.zero_mod, div_mod_eq_colOf] + simp + +theorem fieldVal_carryC (idx : ℕ) {q : ℕ} (hq : q ≤ s + cb + tb) : + fieldVal s cb tb x n T idx (chainW (4 + (s + cb + tb)) (s + cb + tb) 1 q) = + decide (colOf s cb (idx / 16) % 2 ^ q = 2 ^ q - 1) := by + rw [fieldVal_chainW idx (by omega) hq rfl] + simp only [chainVal, chain, one_ne_zero, ↓reduceIte, cmp, div_mod_eq_colOf] + have hK : (2 ^ (s + cb + tb) - 1) % 2 ^ q = 2 ^ q - 1 := by + obtain ⟨d, hd⟩ : ∃ d, s + cb + tb = q + d := ⟨s + cb + tb - q, by omega⟩ + rw [hd, Nat.pow_add] + have h1 := Nat.one_le_two_pow (n := q) + have h2 := Nat.one_le_two_pow (n := d) + have h3 : 2 ^ q ≤ 2 ^ q * 2 ^ d := Nat.le_mul_of_pos_right _ (by omega) + rw [show 2 ^ q * 2 ^ d - 1 = 2 ^ q * (2 ^ d - 1) + (2 ^ q - 1) by + rw [Nat.mul_sub_one]; omega, Nat.mul_add_mod, Nat.mod_eq_of_lt (by omega)] + rw [hK] + have := Nat.mod_lt (colOf s cb (idx / 16)) (Nat.two_pow_pos q) + rw [Bool.eq_iff_iff] + simp only [Bool.and_true, Bool.or_eq_true, decide_eq_true_eq, or_iff_right_iff_imp] + omega + +theorem fieldVal_borrowT (idx : ℕ) (hidx : idx < 2 ^ (4 + (s + cb + tb))) {q : ℕ} + (hq : q ≤ s + cb + tb) : + fieldVal s cb tb x n T idx (chainW (4 + (s + cb + tb)) (s + cb + tb) 2 q) = + decide (timeOf s cb (idx / 16) % 2 ^ q = 0) := by + rw [fieldVal_chainW idx (by omega) hq rfl] + simp only [chainVal, chain, OfNat.ofNat_ne_zero, OfNat.ofNat_ne_one, ↓reduceIte, cmp, + Nat.zero_mod, div_mod_eq_timeOf hidx] + simp + +/-- **The formula of an output bit computes `outBit`** on the values of its wires: the values of +the field stage, and the outputs `ts` of the constant stage for its literal. -/ +theorem eval_outTemplate_wireNat {z : ℕ → Bool} {idx : ℕ} (hidx : idx < 2 ^ (4 + (s + cb + tb))) + (hF : ∀ w < aWidth s cb tb x n T, z w = fieldVal s cb tb x n T idx w) (o : ℕ) : + outTemplate.eval interpretation (fun j => z (wireNat s cb tb x n T o j)) = + outBit s cb tb + (fun f => z (aWidth s cb tb x n T + o / (2 + (s + cb + tb) + 1) * (13 + s) + f)) + (fun q => z (aWidth s cb tb x n T + o / (2 + (s + cb + tb) + 1) * (13 + s) + (2 + s + q))) + (idx / 16) (colOf s cb (idx / 16)) (timeOf s cb (idx / 16)) T (z (lookW s cb tb x)) + (o % (2 + (s + cb + tb) + 1)) := by + have hN : z (4 + (s + cb + tb)) = false := + (hF _ (lt_aWidth_of_lt (by omega))).trans (fieldVal_false idx) + have hC (b : Bool) : z (constW (4 + (s + cb + tb)) b) = b := + (hF _ (constW_lt b)).trans (fieldVal_constW idx b) + have hcol (q : ℕ) : + z (bitW (4 + (s + cb + tb)) (4 + s) cb q) = (colOf s cb (idx / 16)).testBit q := by + rw [hF _ (bitW_lt (by omega)), fieldVal_bitW idx (by omega), div_mod_eq_colOf] + have htime (q : ℕ) : + z (bitW (4 + (s + cb + tb)) (4 + s + cb) tb q) = (timeOf s cb (idx / 16)).testBit q := by + rw [hF _ (bitW_lt (by omega)), fieldVal_bitW idx (by omega), div_mod_eq_timeOf hidx] + have hb0 {q : ℕ} (hq : q ≤ s + cb + tb) : + z (chainW (4 + (s + cb + tb)) (s + cb + tb) 0 q) = + decide (colOf s cb (idx / 16) % 2 ^ q = 0) := by + rw [hF _ (chainW_lt (by omega) hq), fieldVal_borrowC idx hq] + have hb1 {q : ℕ} (hq : q ≤ s + cb + tb) : + z (chainW (4 + (s + cb + tb)) (s + cb + tb) 1 q) = + decide (colOf s cb (idx / 16) % 2 ^ q = 2 ^ q - 1) := by + rw [hF _ (chainW_lt (by omega) hq), fieldVal_carryC idx hq] + have hb2 {q : ℕ} (hq : q ≤ s + cb + tb) : + z (chainW (4 + (s + cb + tb)) (s + cb + tb) 2 q) = + decide (timeOf s cb (idx / 16) % 2 ^ q = 0) := by + rw [hF _ (chainW_lt (by omega) hq), fieldVal_borrowT idx hidx hq] + rw [eval_outTemplate_nat (fun j => z (wireNat s cb tb x n T o j))] + simp only [wireNat] + unfold outBit + have hi := Nat.mod_lt o (show 0 < 2 + (s + cb + tb) + 1 by omega) + generalize o % (2 + (s + cb + tb) + 1) = i at hi ⊢ + generalize aWidth s cb tb x n T + o / (2 + (s + cb + tb) + 1) * (13 + s) = B + by_cases h2 : i < 2 + · simp [h2, hN] + · by_cases hP : i < 2 + (s + cb + tb) + · have hq : i - 2 < s + cb + tb := by omega + have hi2 : 2 + (i - 2) = i := by omega + generalize i - 2 = q at hq hi2 + subst hi2 + have hp : z (4 + q) = (idx / 16).testBit q := by + rw [hF _ (lt_aWidth_of_lt (by omega)), fieldVal_payload idx hq] + have h0 : z (if q < s then B + (2 + q) else 4 + (s + cb + tb)) = + (decide (q < s) && z (B + (2 + q))) := by + split <;> simp [*] + simp only [h2, hP, ↓reduceIte, h0, uWire, vWire, payTerm, colTerm, + timeTerm, Nat.reduceSub, Nat.reduceDiv, Nat.reduceMod, one_ne_zero, OfNat.ofNat_ne_zero, + OfNat.ofNat_ne_one, Nat.reduceEqDiff, Nat.reduceLeDiff, hp, hcol, hb0 hq.le, hN, + Bool.xor_false, Nat.add_zero] + by_cases hc : s ≤ q ∧ q < s + cb + · have ht : ¬ s + cb ≤ q := by omega + simp only [hc, ht, and_self, ↓reduceIte, hcol, hC, hb0 (show q - s ≤ s + cb + tb by omega), + hb1 (show q - s ≤ s + cb + tb by omega), hN, Bool.xor_false, Bool.and_false, + Bool.or_false, decide_true, decide_false, Bool.true_and, Bool.false_and] + simp only [Bool.or_assoc] + · simp only [hc, ↓reduceIte, hN, Bool.xor_false, Bool.and_false, Bool.or_false, + decide_false, Bool.false_and] + by_cases ht : s + cb ≤ q + · simp only [ht, ↓reduceIte, htime, hC, hb2 (show q - s - cb ≤ s + cb + tb by omega), + decide_true, Bool.true_and] + simp only [Bool.or_assoc] + · simp only [ht, ↓reduceIte, hN, Bool.xor_false, Bool.and_false, Bool.or_false, + decide_false, Bool.false_and] + · simp [h2, hP, hN] + +private theorem ofBits_two (f : Fin 2 → Bool) : Nat.ofBits f = (f 0).toNat + 2 * (f 1).toNat := by + simp only [Nat.ofBits, Fin.foldr_succ, Fin.foldr_zero, Fin.succ_zero_eq_one] + omega + +/-- The value of the last gate of chain `k`. -/ +theorem fieldVal_keyWire_chain (idx : ℕ) {k : ℕ} (hk : k < 14) (hP : 1 ≤ s + cb + tb) : + fieldVal s cb tb x n T idx (keyWire s cb tb (4 + s + k)) = + chainVal (chain s cb tb x.length n T k) idx (s + cb + tb) := by + have h := fieldVal_chain (x := x) (n := n) (T := T) idx hk + (show s + cb + tb - 1 < s + cb + tb by omega) + rw [Nat.sub_add_cancel hP] at h + simp only [keyWire, show ¬ 4 + s + k < 4 + s by omega, ↓reduceIte, + show 4 + s + k - (4 + s) = k by omega] + exact h + +/-- **The key read by the constant stage is the key of the fields** of the clause number. -/ +theorem ofBits_keyWire {idx : ℕ} (hidx : idx < 2 ^ (4 + (s + cb + tb))) (hs : 1 ≤ s) + (h2T : 2 * T < 2 ^ cb) (hT : T < 2 ^ tb) (hn : n < 2 * T) (hx : x.length ≤ n) : + Key.ofBits s (fun i : Fin (4 + s + 14) => fieldVal s cb tb x n T idx (keyWire s cb tb i)) = + Key.ofFields s cb x.length n T (idx % 4) (idx / 4 % 4) (idx / 16) := by + have hP : 1 ≤ s + cb + tb := by omega + have hbit (i : ℕ) (hi : i < 4 + s + 14) : bitAt (fun i : Fin (4 + s + 14) => + fieldVal s cb tb x n T idx (keyWire s cb tb i)) i = + fieldVal s cb tb x n T idx (keyWire s cb tb i) := by simp [bitAt, hi] + have hin (i : ℕ) (hi : i < 4 + s) : bitAt (fun i : Fin (4 + s + 14) => + fieldVal s cb tb x n T idx (keyWire s cb tb i)) i = idx.testBit i := by + rw [hbit i (by omega), keyWire, ite_eq_left hi, fieldVal_input idx (by omega)] + have hch (k : ℕ) (hk : k < 14) : bitAt (fun i : Fin (4 + s + 14) => + fieldVal s cb tb x n T idx (keyWire s cb tb i)) (4 + s + k) = + chainVal (chain s cb tb x.length n T k) idx (s + cb + tb) := by + rw [hbit _ (by omega), fieldVal_keyWire_chain idx hk hP] + have hcb : 2 ^ cb ≤ 2 ^ (s + cb + tb) := Nat.pow_le_pow_right (by norm_num) (by omega) + have htb : 2 ^ tb ≤ 2 ^ (s + cb + tb) := Nat.pow_le_pow_right (by norm_num) (by omega) + have hc : colOf s cb (idx / 16) < 2 ^ cb := Nat.mod_lt _ (Nat.two_pow_pos _) + have ht : timeOf s cb (idx / 16) < 2 ^ tb := by + rw [← div_mod_eq_timeOf hidx]; exact Nat.mod_lt _ (Nat.two_pow_pos _) + have hp : idx / 16 < 2 ^ (s + cb + tb) := by + apply Nat.div_lt_of_lt_mul + calc idx < 2 ^ (4 + (s + cb + tb)) := hidx + _ = 16 * 2 ^ (s + cb + tb) := by rw [Nat.pow_add] + have hpmod : idx / 2 ^ 4 % 2 ^ (s + cb + tb) = idx / 16 := Nat.mod_eq_of_lt hp + have h1 : 1 < 2 ^ (s + cb + tb) := Nat.one_lt_two_pow (by omega) + have hcv (gt : Bool) (K : ℕ) (e : Bool) (hK : K < 2 ^ (s + cb + tb)) : + cmp gt (idx / 2 ^ (4 + s) % 2 ^ cb % 2 ^ (s + cb + tb)) (K % 2 ^ (s + cb + tb)) e = + cmp gt (colOf s cb (idx / 16)) K e := by + rw [div_mod_eq_colOf, Nat.mod_eq_of_lt (by omega), Nat.mod_eq_of_lt hK] + have htv (gt : Bool) (K : ℕ) (e : Bool) (hK : K < 2 ^ (s + cb + tb)) : + cmp gt (idx / 2 ^ (4 + s + cb) % 2 ^ tb % 2 ^ (s + cb + tb)) (K % 2 ^ (s + cb + tb)) e = + cmp gt (timeOf s cb (idx / 16)) K e := by + rw [div_mod_eq_timeOf hidx, Nat.mod_eq_of_lt (by omega), Nat.mod_eq_of_lt hK] + have hpv (gt : Bool) (K : ℕ) (e : Bool) (hK : K < 2 ^ (s + cb + tb)) : + cmp gt (idx / 2 ^ 4 % 2 ^ (s + cb + tb) % 2 ^ (s + cb + tb)) (K % 2 ^ (s + cb + tb)) e = + cmp gt (idx / 16) K e := by + rw [Nat.mod_mod, hpmod, Nat.mod_eq_of_lt hK] + have hc0 : bitAt (fun i : Fin (4 + s + 14) => + fieldVal s cb tb x n T idx (keyWire s cb tb i)) (4 + s) = + chainVal (chain s cb tb x.length n T 0) idx (s + cb + tb) := by + simpa using hch 0 (by omega) + simp only [Key.ofBits, Key.ofFields, hc0, + hin 0 (by omega), hin 1 (by omega), hin 2 (by omega), hin 3 (by omega)] + rw [show (fun i : Fin s => bitAt (fun i : Fin (4 + s + 14) => + fieldVal s cb tb x n T idx (keyWire s cb tb i)) (4 + i)) = + fun i : Fin s => (idx / 16).testBit i from funext fun i => by + rw [hin _ (by omega), show idx / 16 = idx / 2 ^ 4 from rfl, Nat.testBit_div_two_pow, + Nat.add_comm], Nat.ofBits_testBit] + have hj : (idx.testBit 0).toNat + 2 * (idx.testBit 1).toNat = idx % 4 := by + simpa only [ofBits_two, Fin.val_zero, Fin.val_one, Nat.reducePow] using Nat.ofBits_testBit idx 2 + have htag : (idx.testBit 2).toNat + 2 * (idx.testBit 3).toNat = idx / 4 % 4 := by + simpa only [ofBits_two, show idx / 4 = idx / 2 ^ 2 from rfl, Nat.testBit_div_two_pow, + Fin.val_zero, Fin.val_one, Nat.reduceAdd, Nat.reducePow] using Nat.ofBits_testBit (idx / 4) 2 + rw [hj, htag] + simp only [hch 3 (by omega), hch 4 (by omega), hch 5 (by omega), hch 6 (by omega), + hch 7 (by omega), hch 8 (by omega), hch 9 (by omega), hch 2 (by omega), hch 10 (by omega), + hch 11 (by omega), hch 12 (by omega), hch 13 (by omega), chainVal, chain] + simp only [OfNat.ofNat_ne_zero, OfNat.ofNat_ne_one, ↓reduceIte, Nat.reduceEqDiff] + simp (disch := omega) only [hcv, htv, hpv] + simp [cmp] + +end Values + + +end Cslib.Circuits.Boolean.Tableau.Decoder diff --git a/Complexity/Computability/Circuit/Boolean/Tableau/Decoder/Fields.lean b/Complexity/Computability/Circuit/Boolean/Tableau/Decoder/Fields.lean new file mode 100644 index 0000000000..74ce5ab1d3 --- /dev/null +++ b/Complexity/Computability/Circuit/Boolean/Tableau/Decoder/Fields.lean @@ -0,0 +1,660 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Boolean.Tseitin +import Mathlib.Data.Nat.Log +import Mathlib.Data.Nat.Size + +/-! +# Field arithmetic for the decoder of the succinct tableau + +The first stage of the decoder of the tableau formula on bit-field labels +(`Complexity/Computability/Circuit/Boolean/Tableau/Succinct.lean`). Its inputs are the bits of a +clause number: two bits of the clause, two bits of the tag, then a payload of `P = s + cb + tb` +bits made of the slot (`s` bits), the column `c` (`cb` bits) and the block `t` (`tb` bits). It is an +explicit De Morgan gate list (`fieldGates`) of + +* two constants and the negations of the inputs; +* fourteen *comparison chains* of `P` gates each (`chainGate`): bit-serial comparisons of a field + with a constant, least significant bit first, one gate per bit. They compare the column with + `0`, `1`, `n`, `n + 1`, `2 T` and `T`, the block with `0` and `T`, the payload with `0`, `1` and + the length of `x`, and give the borrows and carries of `c - 1`, `c + 1` and `t - 1`; +* a *decoder tree* of `2 ^ (m + 1) - 1` gates (`treeGates`), whose last level is the indicator of + the low `m = Nat.size x.length` bits of the payload, and a chain of `x.length` disjunctions + (`orGate`) that looks up the bit of the hardwired `x` at the payload. + +There are `2 + (4 + P) + 14 P + (2 ^ (m + 1) - 1) + x.length` gates, linear in the field widths and +in the length of `x`; in particular there is no carry-lookahead adder, whose size is not linear. + +Correctness is proved wire by wire: the intended value of every wire (`fieldVal`) is consistent +with its gate (`allGates_consistentAt_fieldGates`), so it is the value the list computes +(`getD_evalCode_of_allGates`). + +## Main definitions + +* `Cslib.Circuits.Boolean.Tableau.Decoder.AllGates`: a property of every gate of a list at its + wire. +* `Cslib.Circuits.Boolean.Tableau.Decoder.cmp`: the comparison computed by a chain. +* `Cslib.Circuits.Boolean.Tableau.Decoder.Chain`, `Cslib.Circuits.Boolean.Tableau.Decoder.chain`: + the fourteen comparison chains. +* `Cslib.Circuits.Boolean.Tableau.Decoder.fieldGates`: the gate list. +* `Cslib.Circuits.Boolean.Tableau.Decoder.fieldVal`: the intended values of its wires. + +## Main results + +* `Cslib.Circuits.Boolean.Tableau.Decoder.getD_evalCode_of_allGates`: a valuation consistent with + every gate of a well-formed list is its evaluation. +* `Cslib.Circuits.Boolean.Tableau.Decoder.getD_evalCode_fieldGates`: the gate list computes the + intended values. +* `Cslib.Circuits.Boolean.Tableau.Decoder.length_fieldGates`: its number of gates. +-/ + +@[expose] public section + +namespace Cslib.Circuits.Boolean.Tableau.Decoder + +/-! ### Gate lists checked gate by gate -/ + +/-- Every gate of `gates`, the first one at wire `base`, satisfies `p` at its wire. -/ +def AllGates (p : ℕ → Op × List ℕ → Prop) (base : ℕ) (gates : List (Op × List ℕ)) : Prop := + ∀ g (hg : g < gates.length), p (base + g) gates[g] + +theorem allGates_append {p : ℕ → Op × List ℕ → Prop} {b : ℕ} {l₁ l₂ : List (Op × List ℕ)} : + AllGates p b (l₁ ++ l₂) ↔ AllGates p b l₁ ∧ AllGates p (b + l₁.length) l₂ := by + constructor + · intro h + refine ⟨fun g hg => ?_, fun g hg => ?_⟩ + · have := h g (by simp only [List.length_append]; omega) + rwa [List.getElem_append_left hg] at this + · have := h (l₁.length + g) (by simp only [List.length_append]; omega) + simpa [List.getElem_append_right, Nat.add_assoc] using this + · rintro ⟨h₁, h₂⟩ g hg + by_cases hg₁ : g < l₁.length + · rw [List.getElem_append_left hg₁] + exact h₁ g hg₁ + · rw [List.getElem_append_right (by omega)] + have := h₂ (g - l₁.length) (by simp only [List.length_append] at hg; omega) + rwa [show b + l₁.length + (g - l₁.length) = b + g by omega] at this + +@[simp] theorem allGates_nil {p : ℕ → Op × List ℕ → Prop} {b : ℕ} : AllGates p b [] := by + simp [AllGates] + +theorem allGates_cons {p : ℕ → Op × List ℕ → Prop} {b : ℕ} {g : Op × List ℕ} + {l : List (Op × List ℕ)} : AllGates p b (g :: l) ↔ p b g ∧ AllGates p (b + 1) l := by + have := allGates_append (p := p) (b := b) (l₁ := [g]) (l₂ := l) + simp only [List.singleton_append, List.length_singleton] at this + rw [this] + refine and_congr_left' ⟨fun h => by simpa using h 0 (by simp), fun h g hg => ?_⟩ + obtain rfl : g = 0 := by simpa using hg + simpa using h + +theorem allGates_map_range {p : ℕ → Op × List ℕ → Prop} {b w : ℕ} {f : ℕ → Op × List ℕ} : + AllGates p b ((List.range w).map f) ↔ ∀ i < w, p (b + i) (f i) := by + simp only [AllGates, List.length_map, List.length_range, List.getElem_map, List.getElem_range] + +theorem allGates_flatMap_range {p : ℕ → Op × List ℕ → Prop} {b w : ℕ} + {f : ℕ → List (Op × List ℕ)} : + AllGates p b ((List.range w).flatMap f) ↔ + ∀ i < w, AllGates p (b + ((List.range i).map fun j => (f j).length).sum) (f i) := by + induction w with + | zero => simp [AllGates] + | succ w ih => + rw [List.range_succ, List.flatMap_append, allGates_append, ih, List.flatMap_singleton, + List.length_flatMap] + constructor + · rintro ⟨h₁, h₂⟩ i hi + rcases Nat.lt_succ_iff_lt_or_eq.1 hi with hi | rfl + · exact h₁ i hi + · exact h₂ + · exact fun h => ⟨fun i hi => h i (by omega), h w (by omega)⟩ + +/-- Blocks of a common length `len` start at multiples of `len`. -/ +theorem sum_range_map_const {len : ℕ} {f : ℕ → List (Op × List ℕ)} (hf : ∀ j, (f j).length = len) + (i : ℕ) : ((List.range i).map fun j => (f j).length).sum = i * len := by + induction i with + | zero => simp + | succ i ih => simp [List.range_succ, hf, Nat.succ_mul] + +/-- Blocks of lengths `2 ^ j` start at `2 ^ i - 1`. -/ +theorem sum_range_two_pow (i : ℕ) : ((List.range i).map fun j => 2 ^ j).sum = 2 ^ i - 1 := by + induction i with + | zero => simp + | succ i ih => + rw [List.range_succ, List.map_append, List.sum_append, ih] + have := Nat.one_le_two_pow (n := i) + simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, Nat.pow_succ] + omega + +/-- A gate reads only wires below its own, with the arity of its operation. -/ +def WellFormedAt (w : ℕ) (g : Op × List ℕ) : Prop := + g.2.length = signature.Arity g.1 ∧ ∀ i ∈ g.2, i < w + +/-- The wire of a gate carries, under `σ`, the value of the gate on the values of its arguments. -/ +def ConsistentAt (σ : ℕ → Bool) (w : ℕ) (g : Op × List ℕ) : Prop := + σ w = g.1.value (σ (g.2.getD 0 0)) (σ (g.2.getD 1 0)) + +/-- A list of well-formed gates is the code of a program. -/ +theorem isCodeFrom_of_allGates {n : ℕ} {gates : List (Op × List ℕ)} + (h : AllGates WellFormedAt n gates) : Program.IsCodeFrom signature n 0 gates := + Program.isCodeFrom_of_getElem fun j hj => by simpa [WellFormedAt] using h j hj + +/-- **A valuation consistent with every gate is the evaluation** of a well-formed gate list. -/ +theorem getD_evalCode_of_allGates {n : ℕ} {gates : List (Op × List ℕ)} + (hwf : AllGates WellFormedAt n gates) (σ : ℕ → Bool) (hσ : AllGates (ConsistentAt σ) n gates) + {w : ℕ} (hw : w < n + gates.length) : + (evalCode interpretation false (List.ofFn fun i : Fin n => σ i) gates).getD w false = σ w := + ((eval_tseitinCNF_eq_true_iff_evalCode (isCodeFrom_of_allGates hwf) σ).1 + ((eval_tseitinCNF_eq_true_iff n gates σ).2 fun g hg => hσ g hg) w hw).symm + +/-- A conjunction (`false`) or a disjunction (`true`). -/ +def andOr (b : Bool) : Op := if b then .or else .and + +@[simp] theorem value_andOr (b x y : Bool) : + (andOr b).value x y = if b then x || y else x && y := by + cases b <;> rfl + +theorem wellFormedAt_const {w : ℕ} (b : Bool) : WellFormedAt w (.const b, []) := + ⟨rfl, by simp⟩ + +theorem wellFormedAt_not {w a : ℕ} (ha : a < w) : WellFormedAt w (.not, [a]) := + ⟨rfl, by simpa using ha⟩ + +theorem wellFormedAt_two {w a b : ℕ} {op : Op} (hop : signature.Arity op = 2) (ha : a < w) + (hb : b < w) : WellFormedAt w (op, [a, b]) := + ⟨by simpa using hop.symm, by simp [ha, hb]⟩ + +theorem arity_andOr (b : Bool) : signature.Arity (andOr b) = 2 := by + cases b <;> rfl + +theorem consistentAt_const {σ : ℕ → Bool} {w : ℕ} {b : Bool} : + ConsistentAt σ w (.const b, []) ↔ σ w = b := Iff.rfl + +theorem consistentAt_not {σ : ℕ → Bool} {w a : ℕ} : + ConsistentAt σ w (.not, [a]) ↔ σ w = !σ a := Iff.rfl + +theorem consistentAt_two {σ : ℕ → Bool} {w a b : ℕ} {op : Op} : + ConsistentAt σ w (op, [a, b]) ↔ σ w = op.value (σ a) (σ b) := Iff.rfl + +/-! ### Bit-serial comparison -/ + +/-- The comparison computed by a chain: `a < b` (for `gt = false`) or `b < a` (for `gt = true`), +with ties decided by `e`. -/ +def cmp (gt : Bool) (a b : ℕ) (e : Bool) : Bool := + if gt then decide (b < a) || (decide (a = b) && e) else decide (a < b) || (decide (a = b) && e) + +/-- The low `i + 1` bits of a number: its bit `i` above its low `i` bits. -/ +theorem mod_two_pow_succ (v i : ℕ) : v % 2 ^ (i + 1) = v % 2 ^ i + 2 ^ i * (v.testBit i).toNat := by + rw [Nat.mod_pow_succ, Nat.toNat_testBit] + +/-- **One step of a comparison chain**: comparing one more bit is a disjunction or a conjunction of +the literal of the bit with the comparison of the lower bits, by the bit of the constant. -/ +theorem cmp_succ (gt : Bool) (v K i : ℕ) (e : Bool) : + cmp gt (v % 2 ^ (i + 1)) (K % 2 ^ (i + 1)) e = + (andOr (K.testBit i ^^ gt)).value (if gt then v.testBit i else !v.testBit i) + (cmp gt (v % 2 ^ i) (K % 2 ^ i) e) := by + rw [mod_two_pow_succ v, mod_two_pow_succ K] + have hv := Nat.mod_lt v (Nat.two_pow_pos i) + have hK := Nat.mod_lt K (Nat.two_pow_pos i) + generalize v % 2 ^ i = a at hv ⊢ + generalize K % 2 ^ i = b at hK ⊢ + generalize 2 ^ i = X at hv hK ⊢ + cases v.testBit i <;> cases K.testBit i <;> cases gt <;> cases e <;> + simp [cmp] <;> omega + +/-- A comparison of numbers below `2 ^ w` on all `w` bits. -/ +theorem cmp_mod_of_lt {gt : Bool} {v K w : ℕ} {e : Bool} (hv : v < 2 ^ w) (hK : K < 2 ^ w) : + cmp gt (v % 2 ^ w) (K % 2 ^ w) e = cmp gt v K e := by + rw [Nat.mod_eq_of_lt hv, Nat.mod_eq_of_lt hK] + +/-! ### The layout -/ + +/-- A comparison chain: the offset and the width of the field it reads, its direction (`gt`: +`K < v` rather than `v < K`), the constant `K` and the tie value `init`. -/ +structure Chain where + /-- The input offset of the field. -/ + off : ℕ + /-- The width of the field. -/ + width : ℕ + /-- Whether the chain decides `K < v` rather than `v < K`. -/ + gt : Bool + /-- The constant. -/ + K : ℕ + /-- The value on equal numbers. -/ + init : Bool + +/-- The fourteen comparison chains, for slot, column and block widths `s`, `cb` and `tb`, an +input bound `n`, a step bound `T` and a hardwired prefix of length `X`: the offset and the width +of the field read, the direction, the constant and the tie value. Chains `0`, `1` and `2` give +the borrows of `c - 1`, the carries of `c + 1` and the borrows of `t - 1`. -/ +def chain (s cb tb X n T : ℕ) (k : ℕ) : Chain := + if k = 0 then ⟨4 + s, cb, false, 0, true⟩ -- c % 2 ^ i = 0 + else if k = 1 then ⟨4 + s, cb, true, 2 ^ (s + cb + tb) - 1, true⟩ -- c % 2 ^ i = 2 ^ i - 1 + else if k = 2 then ⟨4 + s + cb, tb, false, 0, true⟩ -- t % 2 ^ i = 0 + else if k = 3 then ⟨4 + s, cb, true, 1, false⟩ -- 1 < c + else if k = 4 then ⟨4 + s, cb, true, n, false⟩ -- n < c + else if k = 5 then ⟨4 + s, cb, true, n + 1, false⟩ -- n + 1 < c + else if k = 6 then ⟨4 + s, cb, false, 2 * T, false⟩ -- c < 2 T + else if k = 7 then ⟨4 + s, cb, true, 2 * T, false⟩ -- 2 T < c + else if k = 8 then ⟨4 + s, cb, false, T, false⟩ -- c < T + else if k = 9 then ⟨4 + s, cb, true, T, false⟩ -- T < c + else if k = 10 then ⟨4 + s + cb, tb, true, T, false⟩ -- T < t + else if k = 11 then ⟨4, s + cb + tb, false, X, false⟩ -- p < X + else if k = 12 then ⟨4, s + cb + tb, false, 0, true⟩ -- p = 0 + else ⟨4, s + cb + tb, true, 1, false⟩ -- 1 < p + +/-- The start of the comparison chains, after the `N` inputs, the two constants and the `N` +negations. -/ +def chainBase (N : ℕ) : ℕ := 2 * N + 2 + +/-- The start of the decoder tree, after the fourteen chains of `P` gates. -/ +def treeBase (N P : ℕ) : ℕ := chainBase N + 14 * P + +/-- The start of the lookup chain, after the `2 ^ (m + 1) - 1` gates of the tree. -/ +def orBase (N P m : ℕ) : ℕ := treeBase N P + (2 ^ (m + 1) - 1) + +/-- Gate `i` of chain `k`, comparing the field of width `w` at input offset `off`, padded with +zeros to `P` bits, with the constant `K`: its literal is the bit of the field (`gt`) or its +negation, and it combines it with the previous gate of the chain (or the tie value `init`). -/ +def chainGate (N P k : ℕ) (spec : Chain) (i : ℕ) : Op × List ℕ := + (andOr (spec.K.testBit i ^^ spec.gt), + [if i < spec.width then (if spec.gt then spec.off + i else N + 2 + (spec.off + i)) + else (if spec.gt then N else N + 1), + if i = 0 then (if spec.init then N + 1 else N) else chainBase N + k * P + (i - 1)]) + +/-- Node `q` of level `ℓ` of the decoder tree: true at level `0`, and otherwise the node `q % 2 ^ ℓ` +of the level below together with bit `ℓ` of the payload, negated when bit `ℓ` of `q` is clear. -/ +def treeGate (N base ℓ q : ℕ) : Op × List ℕ := + if ℓ = 0 then (.const true, []) + else (.and, [base + (2 ^ (ℓ - 1) - 1) + q % 2 ^ (ℓ - 1), + if q.testBit (ℓ - 1) then 4 + (ℓ - 1) else N + 2 + (4 + (ℓ - 1))]) + +/-- The decoder tree on the low `m` bits of the payload, level by level. -/ +def treeGates (N base m : ℕ) : List (Op × List ℕ) := + (List.range (m + 1)).flatMap fun ℓ => (List.range (2 ^ ℓ)).map (treeGate N base ℓ) + +/-- Gate `i` of the lookup chain: the disjunction of the previous gate with the indicator of the +payload `i` when `x[i]` is true. -/ +def orGate (N tbase m obase : ℕ) (x : List Bool) (i : ℕ) : Op × List ℕ := + (.or, [if i = 0 then N else obase + (i - 1), + if x.getD i false then tbase + (2 ^ m - 1) + i else N]) + +/-- **The field stage of the decoder**, for slot, column and block widths `s`, `cb` and `tb`, a +hardwired input prefix `x`, an input length `n` and a step bound `T`. -/ +def fieldGates (s cb tb : ℕ) (x : List Bool) (n T : ℕ) : List (Op × List ℕ) := + [(.const false, []), (.const true, [])] ++ + (List.range (4 + (s + cb + tb))).map (fun i => (.not, [i])) ++ + (List.range 14).flatMap (fun k => (List.range (s + cb + tb)).map + (chainGate (4 + (s + cb + tb)) (s + cb + tb) k (chain s cb tb x.length n T k))) ++ + treeGates (4 + (s + cb + tb)) (treeBase (4 + (s + cb + tb)) (s + cb + tb)) + (Nat.size x.length) ++ + (List.range x.length).map (orGate (4 + (s + cb + tb)) + (treeBase (4 + (s + cb + tb)) (s + cb + tb)) (Nat.size x.length) + (orBase (4 + (s + cb + tb)) (s + cb + tb) (Nat.size x.length)) x) + +theorem length_treeGates (N base m : ℕ) : (treeGates N base m).length = 2 ^ (m + 1) - 1 := by + rw [treeGates, List.length_flatMap] + simpa using sum_range_two_pow (m + 1) + +/-- **The number of gates of the field stage.** -/ +theorem length_fieldGates (s cb tb : ℕ) (x : List Bool) (n T : ℕ) : + (fieldGates s cb tb x n T).length = + 2 + (4 + (s + cb + tb)) + 14 * (s + cb + tb) + (2 ^ (Nat.size x.length + 1) - 1) + + x.length := by + simp only [fieldGates, List.length_append, List.length_cons, List.length_nil, List.length_map, + List.length_range, length_treeGates, List.length_flatMap, List.map_const', List.sum_replicate, + smul_eq_mul] + +/-! ### The intended values -/ + +/-- The comparison of chain `spec` after `j` bits, on the clause number `idx`. -/ +def chainVal (spec : Chain) (idx j : ℕ) : Bool := + cmp spec.gt (idx / 2 ^ spec.off % 2 ^ spec.width % 2 ^ j) (spec.K % 2 ^ j) spec.init + +/-- **The intended value of each wire** of the field stage on the bits of the clause number +`idx`: the inputs, the constants, the negations, the chains after each bit, the indicators of +the low bits of the payload `p = idx / 16`, and the lookup of `x` at `p`. -/ +def fieldVal (s cb tb : ℕ) (x : List Bool) (n T idx w : ℕ) : Bool := + if w < 4 + (s + cb + tb) then idx.testBit w + else if w = 4 + (s + cb + tb) then false + else if w = 4 + (s + cb + tb) + 1 then true + else if w < chainBase (4 + (s + cb + tb)) then !idx.testBit (w - (4 + (s + cb + tb) + 2)) + else if w < treeBase (4 + (s + cb + tb)) (s + cb + tb) then + chainVal (chain s cb tb x.length n T ((w - chainBase (4 + (s + cb + tb))) / (s + cb + tb))) + idx ((w - chainBase (4 + (s + cb + tb))) % (s + cb + tb) + 1) + else if w < orBase (4 + (s + cb + tb)) (s + cb + tb) (Nat.size x.length) then + decide (idx / 16 % 2 ^ Nat.log 2 (w - treeBase (4 + (s + cb + tb)) (s + cb + tb) + 1) = + w - treeBase (4 + (s + cb + tb)) (s + cb + tb) + 1 - + 2 ^ Nat.log 2 (w - treeBase (4 + (s + cb + tb)) (s + cb + tb) + 1)) + else decide (idx / 16 % 2 ^ Nat.size x.length ≤ + w - orBase (4 + (s + cb + tb)) (s + cb + tb) (Nat.size x.length)) && + x.getD (idx / 16 % 2 ^ Nat.size x.length) false + +/-! ### Correctness -/ + +section Correctness + +variable {s cb tb : ℕ} {x : List Bool} {n T : ℕ} + +private theorem ite_pred {α : Type} {p : α → Prop} {c : Prop} [Decidable c] {a b : α} (ha : p a) + (hb : p b) : p (if c then a else b) := by + split <;> assumption + +/-- The fields read by the chains lie within the inputs. -/ +theorem chain_off_add_width_le (k : ℕ) : + (chain s cb tb x.length n T k).off + (chain s cb tb x.length n T k).width ≤ + 4 + (s + cb + tb) := by + unfold chain + repeat (refine ite_pred (p := fun spec : Chain => + spec.off + spec.width ≤ 4 + (s + cb + tb)) ?_ ?_; · dsimp only; omega) + dsimp only; omega + +private theorem chainWire_lt {k i P : ℕ} (hk : k < 14) (hi : i < P) : k * P + i < 14 * P := by + have : k * P + P ≤ 14 * P := by rw [← Nat.succ_mul]; exact Nat.mul_le_mul_right _ hk + omega + +private theorem chainWire_div {k i P : ℕ} (hi : i < P) : (k * P + i) / P = k := by + rw [Nat.mul_comm, Nat.mul_add_div (by omega), Nat.div_eq_of_lt hi, Nat.add_zero] + +private theorem chainWire_mod {k i P : ℕ} (hi : i < P) : (k * P + i) % P = i := by + rw [Nat.mul_comm, Nat.mul_add_mod, Nat.mod_eq_of_lt hi] + +theorem fieldVal_input (idx : ℕ) {w : ℕ} (hw : w < 4 + (s + cb + tb)) : + fieldVal s cb tb x n T idx w = idx.testBit w := by + simp only [fieldVal, hw, ↓reduceIte] + +theorem fieldVal_false (idx : ℕ) : fieldVal s cb tb x n T idx (4 + (s + cb + tb)) = false := by + simp [fieldVal] + +theorem fieldVal_true (idx : ℕ) : fieldVal s cb tb x n T idx (4 + (s + cb + tb) + 1) = true := by + simp [fieldVal] + +theorem fieldVal_not (idx : ℕ) {j : ℕ} (hj : j < 4 + (s + cb + tb)) : + fieldVal s cb tb x n T idx (4 + (s + cb + tb) + 2 + j) = !idx.testBit j := by + have h₁ : ¬ 4 + (s + cb + tb) + 2 + j < 4 + (s + cb + tb) := by omega + have h₂ : 4 + (s + cb + tb) + 2 + j ≠ 4 + (s + cb + tb) := by omega + have h₃ : 4 + (s + cb + tb) + 2 + j ≠ 4 + (s + cb + tb) + 1 := by omega + have h₄ : 4 + (s + cb + tb) + 2 + j < chainBase (4 + (s + cb + tb)) := by + simp only [chainBase]; omega + simp only [fieldVal, h₁, h₂, h₃, h₄, ↓reduceIte, Nat.add_sub_cancel_left] + +theorem fieldVal_chain (idx : ℕ) {k i : ℕ} (hk : k < 14) (hi : i < s + cb + tb) : + fieldVal s cb tb x n T idx (chainBase (4 + (s + cb + tb)) + k * (s + cb + tb) + i) = + chainVal (chain s cb tb x.length n T k) idx (i + 1) := by + have hw := chainWire_lt hk hi + have h₁ : ¬ chainBase (4 + (s + cb + tb)) + k * (s + cb + tb) + i < 4 + (s + cb + tb) := by + simp only [chainBase]; omega + have h₂ : chainBase (4 + (s + cb + tb)) + k * (s + cb + tb) + i ≠ 4 + (s + cb + tb) := by + simp only [chainBase]; omega + have h₃ : chainBase (4 + (s + cb + tb)) + k * (s + cb + tb) + i ≠ 4 + (s + cb + tb) + 1 := by + simp only [chainBase]; omega + have h₄ : ¬ chainBase (4 + (s + cb + tb)) + k * (s + cb + tb) + i < + chainBase (4 + (s + cb + tb)) := by omega + have h₅ : chainBase (4 + (s + cb + tb)) + k * (s + cb + tb) + i < + treeBase (4 + (s + cb + tb)) (s + cb + tb) := by simp only [treeBase]; omega + have h₆ : chainBase (4 + (s + cb + tb)) + k * (s + cb + tb) + i - + chainBase (4 + (s + cb + tb)) = k * (s + cb + tb) + i := by omega + simp only [fieldVal, h₁, h₂, h₃, h₄, h₅, h₆, ↓reduceIte, chainWire_div hi, + chainWire_mod hi] + +theorem fieldVal_tree (idx : ℕ) {ℓ q : ℕ} (hℓ : ℓ ≤ Nat.size x.length) (hq : q < 2 ^ ℓ) : + fieldVal s cb tb x n T idx (treeBase (4 + (s + cb + tb)) (s + cb + tb) + (2 ^ ℓ - 1) + q) = + decide (idx / 16 % 2 ^ ℓ = q) := by + have hpow : 2 ^ ℓ + q < 2 ^ (Nat.size x.length + 1) := + calc 2 ^ ℓ + q < 2 ^ (ℓ + 1) := by rw [Nat.pow_succ]; omega + _ ≤ 2 ^ (Nat.size x.length + 1) := Nat.pow_le_pow_right (by norm_num) (by omega) + have h1 := Nat.one_le_two_pow (n := ℓ) + have h₀ : ¬ treeBase (4 + (s + cb + tb)) (s + cb + tb) + (2 ^ ℓ - 1) + q < + treeBase (4 + (s + cb + tb)) (s + cb + tb) := by omega + have h₁ : ¬ treeBase (4 + (s + cb + tb)) (s + cb + tb) + (2 ^ ℓ - 1) + q < + 4 + (s + cb + tb) := by simp only [treeBase, chainBase]; omega + have h₂ : treeBase (4 + (s + cb + tb)) (s + cb + tb) + (2 ^ ℓ - 1) + q ≠ 4 + (s + cb + tb) := by + simp only [treeBase, chainBase]; omega + have h₃ : treeBase (4 + (s + cb + tb)) (s + cb + tb) + (2 ^ ℓ - 1) + q ≠ + 4 + (s + cb + tb) + 1 := by simp only [treeBase, chainBase]; omega + have h₄ : ¬ treeBase (4 + (s + cb + tb)) (s + cb + tb) + (2 ^ ℓ - 1) + q < + chainBase (4 + (s + cb + tb)) := by simp only [treeBase]; omega + have h₅ : treeBase (4 + (s + cb + tb)) (s + cb + tb) + (2 ^ ℓ - 1) + q < + orBase (4 + (s + cb + tb)) (s + cb + tb) (Nat.size x.length) := by + simp only [orBase]; omega + have h₆ : treeBase (4 + (s + cb + tb)) (s + cb + tb) + (2 ^ ℓ - 1) + q - + treeBase (4 + (s + cb + tb)) (s + cb + tb) + 1 = 2 ^ ℓ + q := by omega + have hlog : Nat.log 2 (2 ^ ℓ + q) = ℓ := + Nat.log_eq_of_pow_le_of_lt_pow (by omega) (by rw [Nat.pow_succ]; omega) + simp only [fieldVal, h₀, h₁, h₂, h₃, h₄, h₅, h₆, ↓reduceIte, hlog, + Nat.add_sub_cancel_left] + +theorem fieldVal_or (idx : ℕ) (i : ℕ) : + fieldVal s cb tb x n T idx (orBase (4 + (s + cb + tb)) (s + cb + tb) (Nat.size x.length) + i) = + (decide (idx / 16 % 2 ^ Nat.size x.length ≤ i) && + x.getD (idx / 16 % 2 ^ Nat.size x.length) false) := by + have h₀ : ¬ orBase (4 + (s + cb + tb)) (s + cb + tb) (Nat.size x.length) + i < + orBase (4 + (s + cb + tb)) (s + cb + tb) (Nat.size x.length) := by omega + have h₁ : ¬ orBase (4 + (s + cb + tb)) (s + cb + tb) (Nat.size x.length) + i < + 4 + (s + cb + tb) := by simp only [orBase, treeBase, chainBase]; omega + have h₂ : orBase (4 + (s + cb + tb)) (s + cb + tb) (Nat.size x.length) + i ≠ + 4 + (s + cb + tb) := by simp only [orBase, treeBase, chainBase]; omega + have h₃ : orBase (4 + (s + cb + tb)) (s + cb + tb) (Nat.size x.length) + i ≠ + 4 + (s + cb + tb) + 1 := by simp only [orBase, treeBase, chainBase]; omega + have h₄ : ¬ orBase (4 + (s + cb + tb)) (s + cb + tb) (Nat.size x.length) + i < + chainBase (4 + (s + cb + tb)) := by simp only [orBase, treeBase]; omega + have h₅ : ¬ orBase (4 + (s + cb + tb)) (s + cb + tb) (Nat.size x.length) + i < + treeBase (4 + (s + cb + tb)) (s + cb + tb) := by simp only [orBase]; omega + simp only [fieldVal, h₀, h₁, h₂, h₃, h₄, h₅, ↓reduceIte, Nat.add_sub_cancel_left] + +/-- The literal of a chain gate is the bit of its field, or its negation. -/ +private theorem fieldVal_chainLit (idx : ℕ) (k i : ℕ) : + fieldVal s cb tb x n T idx + (if i < (chain s cb tb x.length n T k).width then + (if (chain s cb tb x.length n T k).gt then (chain s cb tb x.length n T k).off + i + else 4 + (s + cb + tb) + 2 + ((chain s cb tb x.length n T k).off + i)) + else (if (chain s cb tb x.length n T k).gt then 4 + (s + cb + tb) + else 4 + (s + cb + tb) + 1)) = + if (chain s cb tb x.length n T k).gt then + (idx / 2 ^ (chain s cb tb x.length n T k).off % + 2 ^ (chain s cb tb x.length n T k).width).testBit i + else !(idx / 2 ^ (chain s cb tb x.length n T k).off % + 2 ^ (chain s cb tb x.length n T k).width).testBit i := by + have hle := chain_off_add_width_le (s := s) (cb := cb) (tb := tb) (x := x) (n := n) (T := T) k + generalize chain s cb tb x.length n T k = spec at hle ⊢ + obtain ⟨off, w, gt, K, init⟩ := spec + simp only at hle ⊢ + by_cases hi : i < w + · cases gt + · simp [hi, fieldVal_not idx (show off + i < 4 + (s + cb + tb) by omega), + Nat.testBit_div_two_pow, Nat.add_comm i off] + · simp [hi, fieldVal_input idx (show off + i < 4 + (s + cb + tb) by omega), + Nat.testBit_div_two_pow, Nat.add_comm i off] + · cases gt + · simp [hi, fieldVal_true] + · simp [hi, fieldVal_false] + +/-- **The gates of the field stage, region by region.** -/ +theorem allGates_fieldGates {p : ℕ → Op × List ℕ → Prop} + (hc₀ : p (4 + (s + cb + tb)) (.const false, [])) + (hc₁ : p (4 + (s + cb + tb) + 1) (.const true, [])) + (hnot : ∀ i < 4 + (s + cb + tb), p (4 + (s + cb + tb) + 2 + i) (.not, [i])) + (hchain : ∀ k < 14, ∀ i < s + cb + tb, + p (chainBase (4 + (s + cb + tb)) + k * (s + cb + tb) + i) + (chainGate (4 + (s + cb + tb)) (s + cb + tb) k (chain s cb tb x.length n T k) i)) + (htree : ∀ ℓ ≤ Nat.size x.length, ∀ q < 2 ^ ℓ, + p (treeBase (4 + (s + cb + tb)) (s + cb + tb) + (2 ^ ℓ - 1) + q) + (treeGate (4 + (s + cb + tb)) (treeBase (4 + (s + cb + tb)) (s + cb + tb)) ℓ q)) + (hor : ∀ i < x.length, + p (orBase (4 + (s + cb + tb)) (s + cb + tb) (Nat.size x.length) + i) + (orGate (4 + (s + cb + tb)) (treeBase (4 + (s + cb + tb)) (s + cb + tb)) + (Nat.size x.length) (orBase (4 + (s + cb + tb)) (s + cb + tb) (Nat.size x.length)) x i)) : + AllGates p (4 + (s + cb + tb)) (fieldGates s cb tb x n T) := by + have hlen : ((List.range 14).flatMap fun k => (List.range (s + cb + tb)).map + (chainGate (4 + (s + cb + tb)) (s + cb + tb) k (chain s cb tb x.length n T k))).length = + 14 * (s + cb + tb) := by + simp only [List.length_flatMap, List.length_map, List.length_range, List.map_const', + List.sum_replicate, smul_eq_mul] + simp only [fieldGates, allGates_append, List.length_append, List.length_cons, List.length_nil, + List.length_map, List.length_range, hlen, length_treeGates, allGates_cons, allGates_nil, + and_true] + refine ⟨⟨⟨⟨⟨hc₀, hc₁⟩, ?_⟩, ?_⟩, ?_⟩, ?_⟩ + · rw [allGates_map_range] + intro i hi + simpa [Nat.add_assoc] using hnot i hi + · rw [allGates_flatMap_range] + intro k hk + rw [sum_range_map_const (len := s + cb + tb) (fun j => by simp), allGates_map_range] + intro i hi + have := hchain k hk i hi + convert this using 2 + simp only [chainBase] + omega + · rw [treeGates, allGates_flatMap_range] + intro ℓ hℓ + simp only [List.length_map, List.length_range] + rw [sum_range_two_pow, allGates_map_range] + intro q hq + have := htree ℓ (by omega) q hq + convert this using 2 + simp only [treeBase, chainBase] + omega + · rw [allGates_map_range] + intro i hi + have := hor i hi + convert this using 2 + simp only [orBase, treeBase, chainBase] + omega + +/-- **The field stage is a well-formed gate list**, when the decoder tree reads only payload +bits. -/ +theorem allGates_wellFormedAt_fieldGates (hm : Nat.size x.length ≤ s + cb + tb) : + AllGates WellFormedAt (4 + (s + cb + tb)) (fieldGates s cb tb x n T) := by + have hX := Nat.lt_size_self x.length + refine allGates_fieldGates (wellFormedAt_const _) (wellFormedAt_const _) + (fun i hi => wellFormedAt_not (by omega)) (fun k hk i hi => ?_) (fun ℓ hℓ q hq => ?_) + (fun i hi => ?_) + · have hle := chain_off_add_width_le (s := s) (cb := cb) (tb := tb) (x := x) (n := n) (T := T) k + refine wellFormedAt_two (arity_andOr _) ?_ ?_ + · simp only [chainBase] + split_ifs <;> omega + · simp only [chainBase] + split_ifs <;> omega + · unfold treeGate + split_ifs with h₀ h₁ + · exact wellFormedAt_const _ + · have hq' := Nat.mod_lt q (Nat.two_pow_pos (ℓ - 1)) + have hpow : 2 ^ ℓ = 2 * 2 ^ (ℓ - 1) := by + rw [← Nat.pow_succ']; congr 1; omega + refine wellFormedAt_two rfl ?_ ?_ <;> simp only [treeBase, chainBase] <;> omega + · have hq' := Nat.mod_lt q (Nat.two_pow_pos (ℓ - 1)) + have hpow : 2 ^ ℓ = 2 * 2 ^ (ℓ - 1) := by + rw [← Nat.pow_succ']; congr 1; omega + refine wellFormedAt_two rfl ?_ ?_ <;> simp only [treeBase, chainBase] <;> omega + · have hpow : 2 ^ (Nat.size x.length + 1) = 2 * 2 ^ Nat.size x.length := Nat.pow_succ' + refine wellFormedAt_two rfl ?_ ?_ <;> simp only [orBase, treeBase, chainBase] <;> + split_ifs <;> omega + +/-- The low `ℓ + 1` bits of two numbers agree exactly when their low `ℓ` bits and their bits `ℓ` +agree. -/ +theorem mod_two_pow_succ_eq_iff {p q ℓ : ℕ} (hq : q < 2 ^ (ℓ + 1)) : + p % 2 ^ (ℓ + 1) = q ↔ p % 2 ^ ℓ = q % 2 ^ ℓ ∧ p.testBit ℓ = q.testBit ℓ := by + conv_lhs => rw [← Nat.mod_eq_of_lt hq, mod_two_pow_succ p, mod_two_pow_succ q] + have ha := Nat.mod_lt p (Nat.two_pow_pos ℓ) + have hb := Nat.mod_lt q (Nat.two_pow_pos ℓ) + generalize p % 2 ^ ℓ = a at ha ⊢ + generalize q % 2 ^ ℓ = b at hb ⊢ + generalize 2 ^ ℓ = X at ha hb ⊢ + cases p.testBit ℓ <;> cases q.testBit ℓ <;> simp <;> omega + +/-- **The intended values are consistent with the gates** of the field stage. -/ +theorem allGates_consistentAt_fieldGates (hm : Nat.size x.length ≤ s + cb + tb) (idx : ℕ) : + AllGates (ConsistentAt (fieldVal s cb tb x n T idx)) (4 + (s + cb + tb)) + (fieldGates s cb tb x n T) := by + have hX := Nat.lt_size_self x.length + refine allGates_fieldGates (consistentAt_const.2 (fieldVal_false idx)) + (consistentAt_const.2 (fieldVal_true idx)) + (fun i hi => consistentAt_not.2 (by rw [fieldVal_not idx hi, fieldVal_input idx hi])) + (fun k hk i hi => ?_) (fun ℓ hℓ q hq => ?_) (fun i hi => ?_) + · rw [chainGate, consistentAt_two, fieldVal_chain idx hk hi, fieldVal_chainLit] + have hprev : fieldVal s cb tb x n T idx + (if i = 0 then (if (chain s cb tb x.length n T k).init then 4 + (s + cb + tb) + 1 + else 4 + (s + cb + tb)) + else chainBase (4 + (s + cb + tb)) + k * (s + cb + tb) + (i - 1)) = + chainVal (chain s cb tb x.length n T k) idx i := by + by_cases h₀ : i = 0 + · subst h₀ + cases h₁ : (chain s cb tb x.length n T k).init + · simp only [↓reduceIte, Bool.false_eq_true, fieldVal_false, chainVal, cmp, pow_zero, + Nat.mod_one, h₁] + simp + · simp only [↓reduceIte, fieldVal_true, chainVal, cmp, pow_zero, Nat.mod_one, h₁] + simp + · simp only [h₀, ↓reduceIte] + rw [fieldVal_chain idx hk (by omega), Nat.sub_add_cancel (by omega)] + rw [hprev, chainVal, chainVal, cmp_succ] + · rw [treeGate] + by_cases h₀ : ℓ = 0 + · subst h₀ + simp only [↓reduceIte] + rw [consistentAt_const, fieldVal_tree idx hℓ hq] + simp only [pow_zero, Nat.lt_one_iff] at hq + simp [hq, Nat.mod_one] + · simp only [h₀, ↓reduceIte] + obtain ⟨ℓ, rfl⟩ : ∃ ℓ', ℓ = ℓ' + 1 := ⟨ℓ - 1, by omega⟩ + simp only [Nat.add_sub_cancel] + have hlit : fieldVal s cb tb x n T idx (if q.testBit ℓ then 4 + ℓ else 4 + (s + cb + tb) + 2 + + (4 + ℓ)) = decide ((idx / 16).testBit ℓ = q.testBit ℓ) := by + have h16 : idx / 16 = idx / 2 ^ 4 := rfl + rw [h16, Nat.testBit_div_two_pow, Nat.add_comm ℓ 4] + split_ifs with hb + · rw [fieldVal_input idx (by omega), hb]; cases idx.testBit (4 + ℓ) <;> rfl + · rw [fieldVal_not idx (by omega)] + simp only [Bool.not_eq_true] at hb + rw [hb]; cases idx.testBit (4 + ℓ) <;> rfl + rw [consistentAt_two, fieldVal_tree idx hℓ hq, + fieldVal_tree idx (by omega) (Nat.mod_lt q (Nat.two_pow_pos ℓ)), hlit] + simp only [Op.value, Bool.decide_and, mod_two_pow_succ_eq_iff hq] + · rw [orGate, consistentAt_two, fieldVal_or idx] + have hsel : fieldVal s cb tb x n T idx (if x.getD i false then + treeBase (4 + (s + cb + tb)) (s + cb + tb) + (2 ^ Nat.size x.length - 1) + i + else 4 + (s + cb + tb)) = + (x.getD i false && decide (idx / 16 % 2 ^ Nat.size x.length = i)) := by + split_ifs with hxi + · rw [fieldVal_tree idx le_rfl (by omega), hxi, Bool.true_and] + · simp only [Bool.not_eq_true] at hxi + rw [fieldVal_false, hxi, Bool.false_and] + rw [hsel] + by_cases h₀ : i = 0 + · subst h₀ + simp only [↓reduceIte] + rw [fieldVal_false] + cases h : decide (idx / 16 % 2 ^ Nat.size x.length = 0) <;> simp_all [Op.value] + · simp only [h₀, ↓reduceIte] + rw [fieldVal_or idx] + by_cases hlt : idx / 16 % 2 ^ Nat.size x.length < i + · have h₁ : idx / 16 % 2 ^ Nat.size x.length ≤ i - 1 := by omega + have h₂ : idx / 16 % 2 ^ Nat.size x.length ≠ i := by omega + simp [Op.value, h₁, hlt.le, h₂] + · by_cases heq : idx / 16 % 2 ^ Nat.size x.length = i + · have h₁ : ¬ idx / 16 % 2 ^ Nat.size x.length ≤ i - 1 := by omega + simp [Op.value, heq] + · have h₁ : ¬ idx / 16 % 2 ^ Nat.size x.length ≤ i - 1 := by omega + have h₂ : ¬ idx / 16 % 2 ^ Nat.size x.length ≤ i := by omega + simp [Op.value, h₁, h₂, heq] + +/-- **The field stage computes the intended values** of its wires on the bits of a clause +number. -/ +theorem getD_evalCode_fieldGates (hm : Nat.size x.length ≤ s + cb + tb) (idx : ℕ) {w : ℕ} + (hw : w < 4 + (s + cb + tb) + (fieldGates s cb tb x n T).length) : + (evalCode interpretation false (List.ofFn fun i : Fin (4 + (s + cb + tb)) => idx.testBit i) + (fieldGates s cb tb x n T)).getD w false = fieldVal s cb tb x n T idx w := by + have h := getD_evalCode_of_allGates (allGates_wellFormedAt_fieldGates hm) _ + (allGates_consistentAt_fieldGates (n := n) (T := T) hm idx) hw + rwa [show (List.ofFn fun i : Fin (4 + (s + cb + tb)) => fieldVal s cb tb x n T idx i) = + List.ofFn fun i => idx.testBit i from + congrArg List.ofFn (funext fun i => fieldVal_input idx i.isLt)] at h + +end Correctness + +end Cslib.Circuits.Boolean.Tableau.Decoder diff --git a/Complexity/Computability/Circuit/Boolean/Tableau/Decoder/Shape.lean b/Complexity/Computability/Circuit/Boolean/Tableau/Decoder/Shape.lean new file mode 100644 index 0000000000..4da1b5af2b --- /dev/null +++ b/Complexity/Computability/Circuit/Boolean/Tableau/Decoder/Shape.lean @@ -0,0 +1,787 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Boolean.Tableau.Succinct +import Complexity.Foundations.Data.Nat.Bitwise.Carry + +/-! +# The clauses of the succinct tableau as symbolic shapes + +A clause of the tableau formula on bit-field labels (`Cslib.Circuits.Boolean.Tableau.clauseOf`) +is determined by finitely many data: its clause and tag fields, its slot, and thirteen comparisons +of the column `c`, the block `t` and the payload `p` with `0`, `1`, `n`, `n + 1`, `2 T`, `T` and +the length of the fixed prefix `x` (`Key`). From these, the clause is a list of three symbolic +literals (`shapeOf`): the label of each literal is a constant, the input `p`, the input `c - 1`, +or a position whose column is `0`, `c`, `c - 1`, `c + 1` or `2 T` and whose block is `t`, `t - 1` +or `T` (`LabelSrc`); its sign is a constant or the bit of `x` at `p` (`SignSrc`). Evaluating the +shapes on the fields gives the clause (`clauseOf_eq_map_shapeOf`). + +This is the case analysis behind the decoder circuit: a circuit of constant size computes the +shape from the key, and circuits linear in the field widths compute the fields `c - 1`, `c + 1` +and `t - 1` and the comparisons. + +## Main definitions + +* `Cslib.Circuits.Boolean.Tableau.Decoder.LabelSrc`, + `Cslib.Circuits.Boolean.Tableau.Decoder.SignSrc`: symbolic labels and signs. +* `Cslib.Circuits.Boolean.Tableau.Decoder.Key`, + `Cslib.Circuits.Boolean.Tableau.Decoder.Key.ofFields`: the finite data determining a clause. +* `Cslib.Circuits.Boolean.Tableau.Decoder.shapeOf`: the symbolic clause of a key. + +## Main results + +* `Cslib.Circuits.Boolean.Tableau.Decoder.clauseOf_eq_map_shapeOf`: the clause with given fields + is the evaluation of the shape of their key. +* `Cslib.Circuits.Boolean.Tableau.Decoder.inRange_of_mem_shapeOf`: the labels of the shapes stay + within their fields. + +## References + +* [R. Williams, *Improving exhaustive search implies superpolynomial lower bounds*][Williams2010] +-/ + +@[expose] public section + +namespace Cslib.Circuits.Boolean.Tableau.Decoder + +open Turing MultiTapeTM Cslib.Logic.PL + +/-! ### Symbolic labels -/ + +/-- The column field of a symbolic position label. -/ +inductive ColSrc where + /-- The column `0`. -/ + | zero + /-- The column `c`. -/ + | same + /-- The column `c - 1`. -/ + | prev + /-- The column `c + 1`. -/ + | next + /-- The column `2 T`. -/ + | last + deriving DecidableEq + +/-- The block field of a symbolic position label. -/ +inductive TimeSrc where + /-- The block `t`. -/ + | same + /-- The block `t - 1`. -/ + | prev + /-- The block `T`. -/ + | top + deriving DecidableEq + +/-- A symbolic label. -/ +inductive LabelSrc where + /-- The constant gate `b`. -/ + | const (b : Bool) + /-- The input `p` (`false`) or `c - 1` (`true`). -/ + | input (fromCol : Bool) + /-- A position, with its slot and the sources of its column and block. -/ + | pos (slot : ℕ) (col : ColSrc) (time : TimeSrc) + +/-- A symbolic sign. -/ +inductive SignSrc where + /-- A constant sign. -/ + | const (b : Bool) + /-- The bit of `x` at the payload. -/ + | lookup + +/-- A symbolic literal. -/ +abbrev Shape := LabelSrc × SignSrc + +/-- The column of a column source. -/ +def ColSrc.eval (c T : ℕ) : ColSrc → ℕ + | .zero => 0 + | .same => c + | .prev => c - 1 + | .next => c + 1 + | .last => 2 * T + +/-- The block of a block source. -/ +def TimeSrc.eval (t T : ℕ) : TimeSrc → ℕ + | .same => t + | .prev => t - 1 + | .top => T + +/-- The label of a symbolic label, for slot and column widths `s` and `cb`, payload `p`, column +`c` and block `t`. -/ +def LabelSrc.eval (s cb p c t T : ℕ) : LabelSrc → ℕ + | .const b => constLabel b + | .input false => inputLabel p + | .input true => inputLabel (c - 1) + | .pos sl cs ts => 2 + 4 * (sl + 2 ^ s * (cs.eval c T + 2 ^ cb * ts.eval t T)) + +/-- The sign of a symbolic sign. -/ +def SignSrc.eval (x : List Bool) (p : ℕ) : SignSrc → Bool + | .const b => b + | .lookup => x.getD p false + +/-- The literal of a symbolic literal. -/ +def Shape.eval (s cb p c t T : ℕ) (x : List Bool) (sh : Shape) : Literal ℕ := + (sh.1.eval s cb p c t T, sh.2.eval x p) + +/-! ### Keys -/ + +/-- **The finite data that determine a clause**: the clause and tag fields, the slot, and +comparisons of the column `c`, the block `t` and the payload `p`. -/ +structure Key where + /-- The clause field. -/ + j : ℕ + /-- The tag field. -/ + tag : ℕ + /-- The slot. -/ + slot : ℕ + /-- `c = 0`. -/ + c0 : Bool + /-- `1 < c`. -/ + cGt1 : Bool + /-- `n < c`. -/ + cGtN : Bool + /-- `n + 1 < c`. -/ + cGtN1 : Bool + /-- `c < 2 T`. -/ + cLt2T : Bool + /-- `2 T < c`. -/ + cGt2T : Bool + /-- `c < T`. -/ + cLtT : Bool + /-- `T < c`. -/ + cGtT : Bool + /-- `t = 0`. -/ + t0 : Bool + /-- `T < t`. -/ + tGtT : Bool + /-- `p < X`, for the length `X` of the fixed prefix. -/ + pLtX : Bool + /-- `p = 0`. -/ + p0 : Bool + /-- `1 < p`. -/ + pGt1 : Bool + +/-- The column of a payload. -/ +abbrev colOf (s cb p : ℕ) : ℕ := p / 2 ^ s % 2 ^ cb + +/-- The block of a payload. -/ +abbrev timeOf (s cb p : ℕ) : ℕ := p / 2 ^ s / 2 ^ cb + +/-- **The key of the fields** `j`, `tag` and `p` of a clause number, for slot and column widths +`s` and `cb`, a prefix of length `X`, `n` inputs and `T` steps. -/ +def Key.ofFields (s cb X n T j tag p : ℕ) : Key where + j := j + tag := tag + slot := p % 2 ^ s + c0 := decide (colOf s cb p = 0) + cGt1 := decide (1 < colOf s cb p) + cGtN := decide (n < colOf s cb p) + cGtN1 := decide (n + 1 < colOf s cb p) + cLt2T := decide (colOf s cb p < 2 * T) + cGt2T := decide (2 * T < colOf s cb p) + cLtT := decide (colOf s cb p < T) + cGtT := decide (T < colOf s cb p) + t0 := decide (timeOf s cb p = 0) + tGtT := decide (T < timeOf s cb p) + pLtX := decide (p < X) + p0 := decide (p = 0) + pGt1 := decide (1 < p) + +/-- The guard of a reference, from a key. -/ +def Key.guard (κ : Key) : Guard → Bool + | .always => true + | .pos => !κ.c0 + | .ltLast => κ.cLt2T + | .inRange => !κ.c0 && !κ.cGtN + | .outRange => !(!κ.c0 && !κ.cGtN) + | .isZero => κ.c0 + | .isEnd => κ.cGtN && !κ.cGtN1 + | .leEnd => !κ.c0 && !κ.cGtN1 + +variable {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] + +/-- Whether a position is admissible in the column, from a key. -/ +def Key.colOK (κ : Key) : Loc k State → Bool + | .scan _ => !κ.cGt2T + | .col .. => !κ.cGt2T + | .glob _ => κ.c0 + | .gf .. => κ.c0 + +/-- The column source of a reference to a position: `0` for the global positions. -/ +def colSrcOf : Loc k State → ColSel → ColSrc + | .glob _, _ => .zero + | .gf .., _ => .zero + | _, .same => .same + | _, .prev => .prev + | _, .next => .next + | _, .last => .last + +/-- The symbolic label of a reference, from a key. -/ +noncomputable def Key.refSrc (κ : Key) : Ref k State → LabelSrc + | .fls => .const false + | .tru => .const true + | .inp => if !κ.c0 && !κ.cGtN then .input true else .const false + | .node p l cs g => if κ.guard g then .pos l.slot (colSrcOf l cs) (if p then .prev else .same) + else .const false + +/-- The initial value of a column feature, from a key. -/ +def Key.colInit (κ : Key) : ColFeat k → Bool + | .inPos => !κ.c0 && !κ.cGt1 + | .head _ => !κ.cLtT && !κ.cGtT + | .cell _ s => decide (s = none) + +variable (tm : MultiTapeTM k Bool State) + +/-- The initial value of a position, from a key. -/ +def Key.initBit (κ : Key) : Loc k State → Bool + | .gf f true j => decide (j = 7) && gfInit tm f + | .col f true j => decide (j = 7) && κ.colInit f + | _ => false + +/-- Clauses on symbolic labels with constant signs. -/ +def lift (cl : Clause LabelSrc) : List Shape := cl.map fun l => (l.1, .const l.2) + +/-- The symbolic tautology. -/ +def tautShape : List Shape := + [(.const false, .const true), (.const false, .const false), (.const false, .const true)] + +/-- The symbolic clause `j` of a position. -/ +noncomputable def posShape (κ : Key) (l : Loc k State) (j : Fin 3) : Clause LabelSrc := + if κ.t0 then tseitinClause (.const (κ.initBit tm l)) (.pos l.slot .same .same) (.const false) + (.const false) j + else + let (op, left, right) := table tm l + tseitinClause op (.pos l.slot .same .same) (κ.refSrc left) (κ.refSrc right) j + +/-- The symbolic label of the output. -/ +noncomputable def outSrc : LabelSrc := + .pos (Loc.gf (k := k) (State := State) (.out (.one true)) true 7).slot .zero .top + +/-- **The symbolic clause of a key**, following `clauseOf`. -/ +noncomputable def shapeOf (κ : Key) : List Shape := + if hj : κ.j < 3 then + if κ.tag = 0 then + if !κ.pGt1 then + lift (tseitinClause (.const !κ.p0) (.const !κ.p0) (.const false) (.const false) ⟨κ.j, hj⟩) + else tautShape + else if κ.tag = 1 then + if κ.j = 0 ∧ κ.pLtX then [(.input false, .lookup), (.input false, .lookup), + (.input false, .lookup)] + else tautShape + else if κ.tag = 2 then + match Loc.ofSlot (k := k) (State := State) κ.slot with + | some l => if !κ.tGtT && κ.colOK l then lift (posShape tm κ l ⟨κ.j, hj⟩) else tautShape + | none => tautShape + else if κ.j = 0 ∧ κ.p0 then + [(outSrc (k := k) (State := State), .const true), + (outSrc (k := k) (State := State), .const true), + (outSrc (k := k) (State := State), .const true)] + else tautShape + else tautShape + +/-! ### Evaluation -/ + +section Eval + +variable {s cb X n T : ℕ} + +theorem Key.guard_ofFields (j tag p : ℕ) (g : Guard) : + (Key.ofFields s cb X n T j tag p).guard g = g.test n T (colOf s cb p) := by + cases g <;> simp only [Key.guard, Key.ofFields, Guard.test, numCols] <;> + rw [Bool.eq_iff_iff] <;> + simp only [Bool.not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not, decide_eq_true_eq, + Order.lt_add_one_iff, Order.add_one_le_iff, Bool.and_eq_true, not_lt, Bool.decide_and, + and_congr_left_iff, Bool.not_and, Bool.not_not, Bool.or_eq_true, not_le, Order.lt_one_iff] <;> + omega + +omit [DecidableEq State] in +theorem Key.colOK_ofFields (j tag p : ℕ) (l : Loc k State) : + (Key.ofFields s cb X n T j tag p).colOK l = decide (l.ColOK T (colOf s cb p)) := by + cases l <;> simp only [Key.colOK, Key.ofFields, Loc.ColOK, numCols] <;> + rw [Bool.eq_iff_iff] <;> simp + +theorem Key.initBit_ofFields (j tag p : ℕ) (l : Loc k State) : + (Key.ofFields s cb X n T j tag p).initBit tm l = Tableau.initBit tm T (colOf s cb p) l := by + rcases l with l | l | ⟨f, (_ | _), j⟩ | ⟨f, (_ | _), j⟩ <;> try rfl + rcases f with _ | i | ⟨i, s⟩ <;> + simp only [Key.initBit, Tableau.initBit, Key.colInit, Tableau.colInit, Key.ofFields] <;> + congr 1 <;> rw [Bool.eq_iff_iff] <;> + simp only [Bool.and_eq_true, Bool.not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not, + not_lt, decide_eq_true_eq] <;> + omega + +omit [DecidableEq State] in +theorem colSrcOf_eval (l : Loc k State) (cs : ColSel) (c T : ℕ) : + (colSrcOf l cs).eval c T = l.labelCol (cs.apply T c) := by + rcases l with l | l | ⟨f, b, j⟩ | ⟨f, b, j⟩ <;> cases cs <;> rfl + +omit [DecidableEq State] in +/-- **The symbolic label of a reference evaluates to its label.** -/ +theorem refSrc_eval {t : ℕ} (j tag p : ℕ) (r : Ref k State) : + ((Key.ofFields (slotBits k State) (colBits T) X n T j tag p).refSrc r).eval (slotBits k State) + (colBits T) p (colOf (slotBits k State) (colBits T) p) t T = + r.label n T t (colOf (slotBits k State) (colBits T) p) := by + rcases r with _ | _ | _ | ⟨q, l, cs, g⟩ + · rfl + · rfl + · simp only [Key.refSrc, Ref.label, Key.ofFields] + by_cases h : 1 ≤ colOf (slotBits k State) (colBits T) p ∧ + colOf (slotBits k State) (colBits T) p ≤ n + · have h₁ : (!decide (colOf (slotBits k State) (colBits T) p = 0) && + !decide (n < colOf (slotBits k State) (colBits T) p)) = true := by + simp only [Bool.and_eq_true, Bool.not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not, + not_lt] + omega + simp only [h₁, h, ↓reduceIte] + rfl + · have h₁ : ¬ (!decide (colOf (slotBits k State) (colBits T) p = 0) && + !decide (n < colOf (slotBits k State) (colBits T) p)) = true := by + simp only [Bool.and_eq_true, Bool.not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not, + not_lt, not_and, not_le] + omega + simp only [h₁, h, ↓reduceIte, Bool.false_eq_true] + rfl + · simp only [Key.refSrc, Ref.label, Key.guard_ofFields] + by_cases hg : g.test n T (colOf (slotBits k State) (colBits T) p) = true + · simp only [hg, ↓reduceIte, LabelSrc.eval, posLabel, colSrcOf_eval] + cases q <;> rfl + · simp only [hg, ↓reduceIte, Bool.false_eq_true] + rfl + +theorem map_eval_lift (s cb p c t T : ℕ) (x : List Bool) (cl : Clause LabelSrc) : + (lift cl).map (Shape.eval s cb p c t T x) = cl.relabel (LabelSrc.eval s cb p c t T) := by + simp [lift, Clause.relabel, Shape.eval, SignSrc.eval, Function.comp_def, Prod.map] + +/-- **The clause with given fields is the evaluation of the shape of their key.** -/ +theorem clauseOf_eq_map_shapeOf (x : List Bool) (n T j tag p : ℕ) : + clauseOf tm x n T j tag p = + (shapeOf tm (Key.ofFields (slotBits k State) (colBits T) x.length n T j tag p)).map + (Shape.eval (slotBits k State) (colBits T) p (colOf (slotBits k State) (colBits T) p) + (timeOf (slotBits k State) (colBits T) p) T x) := by + set κ := Key.ofFields (slotBits k State) (colBits T) x.length n T j tag p with hκ + have hκj : κ.j = j := rfl + have hκtag : κ.tag = tag := rfl + have hκslot : κ.slot = p % 2 ^ slotBits k State := rfl + rw [clauseOf, shapeOf, hκj, hκtag] + by_cases hj : j < 3 + · simp only [hj, ↓reduceDIte] + by_cases h0 : tag = 0 + · simp only [h0, ↓reduceIte] + by_cases hp : p < 2 + · have h₁ : (!κ.pGt1) = true := by + simp only [hκ, Key.ofFields, Nat.div_eq_zero_iff, Nat.pow_eq_zero, OfNat.ofNat_ne_zero, + ne_eq, false_and, false_or, Bool.not_eq_eq_eq_not, Bool.not_true, + decide_eq_false_iff_not, not_lt] + omega + have h₂ : (!κ.p0) = decide (p = 1) := by + rw [Bool.eq_iff_iff] + simp only [hκ, Key.ofFields, Nat.div_eq_zero_iff, Nat.pow_eq_zero, OfNat.ofNat_ne_zero, + ne_eq, false_and, false_or, Bool.not_eq_eq_eq_not, Bool.not_true, + decide_eq_false_iff_not, decide_eq_true_eq] + omega + simp only [hp, h₁, ↓reduceIte, h₂, map_eval_lift, relabel_tseitinClause] + rfl + · have h₁ : ¬ (!κ.pGt1) = true := by + simp only [hκ, Key.ofFields, Nat.div_eq_zero_iff, Nat.pow_eq_zero, OfNat.ofNat_ne_zero, + ne_eq, false_and, false_or, Bool.not_eq_eq_eq_not, Bool.not_true, + decide_eq_false_iff_not, not_lt, not_le] + omega + simp only [hp, h₁, ↓reduceIte] + rfl + · by_cases h1 : tag = 1 + · simp only [h1, ↓reduceIte, one_ne_zero] + by_cases hp : j = 0 ∧ p < x.length + · have h₁ : (j = 0 ∧ κ.pLtX = true) := ⟨hp.1, by simp [hκ, Key.ofFields, hp.2]⟩ + rw [dite_eq_left hp, ite_eq_left h₁] + simp [unitClause, Shape.eval, LabelSrc.eval, SignSrc.eval, List.getElem?_eq_getElem hp.2] + · have h₁ : ¬ (j = 0 ∧ κ.pLtX = true) := by + simp only [hκ, Key.ofFields, Nat.div_eq_zero_iff, Nat.pow_eq_zero, OfNat.ofNat_ne_zero, + ne_eq, false_and, false_or, decide_eq_true_eq, not_and, not_lt] + omega + rw [dite_eq_right hp, ite_eq_right h₁] + rfl + · by_cases h2 : tag = 2 + · simp only [h2, ↓reduceIte, OfNat.ofNat_ne_zero, OfNat.ofNat_ne_one, hκslot] + rcases hl : Loc.ofSlot (k := k) (State := State) (p % 2 ^ slotBits k State) with _ | l + · rfl + · have hc : κ.colOK l = decide (l.ColOK T (colOf (slotBits k State) (colBits T) p)) := + Key.colOK_ofFields _ _ _ l + have hiff : (!κ.tGtT && κ.colOK l) = true ↔ + (p / 2 ^ slotBits k State / 2 ^ colBits T ≤ T ∧ + l.ColOK T (p / 2 ^ slotBits k State % 2 ^ colBits T)) := by + rw [hc]; simp [hκ, Key.ofFields] + simp only + by_cases hok : p / 2 ^ slotBits k State / 2 ^ colBits T ≤ T ∧ + l.ColOK T (p / 2 ^ slotBits k State % 2 ^ colBits T) + · simp only [hok, hiff.2 hok, and_self, ↓reduceIte, map_eval_lift] + unfold posClause posShape + by_cases ht : p / 2 ^ slotBits k State / 2 ^ colBits T = 0 + · have hκt : κ.t0 = true := by simp [hκ, Key.ofFields, ht] + simp only [ht, hκt, ↓reduceIte, relabel_tseitinClause] + rw [hκ, Key.initBit_ofFields] + rfl + · have hκt : κ.t0 = false := by simp [hκ, Key.ofFields, ht] + simp only [ht, hκt, ↓reduceIte, Bool.false_eq_true] + generalize table tm l = e + obtain ⟨op, a, b⟩ := e + simp only [relabel_tseitinClause] + rw [hκ, refSrc_eval, refSrc_eval] + rfl + · have hnot : ¬ (!κ.tGtT && κ.colOK l) = true := fun h => hok (hiff.1 h) + simp only [hok, hnot, ↓reduceIte] + rfl + · simp only [h0, h1, h2, ↓reduceIte] + by_cases hp : j = 0 ∧ p = 0 + · have h₁ : (j = 0 ∧ κ.p0 = true) := ⟨hp.1, by simp [hκ, Key.ofFields, hp.2]⟩ + rw [ite_eq_left hp, ite_eq_left h₁] + simp [unitClause, Shape.eval, LabelSrc.eval, SignSrc.eval, outLabel, outSrc, posLabel, + ColSrc.eval, TimeSrc.eval] + · have h₁ : ¬ (j = 0 ∧ κ.p0 = true) := by + simp only [hκ, Key.ofFields, Nat.div_eq_zero_iff, Nat.pow_eq_zero, + OfNat.ofNat_ne_zero, ne_eq, false_and, false_or, decide_eq_true_eq, not_and] + omega + rw [ite_eq_right hp, ite_eq_right h₁] + rfl + · simp only [hj, ↓reduceDIte] + rfl + +end Eval + +/-! ### Bits -/ + +section Bits + +/-- The tag of a symbolic label. -/ +def LabelSrc.tag : LabelSrc → ℕ + | .const _ => 0 + | .input _ => 1 + | .pos .. => 2 + +/-- The constant part of the payload of a symbolic label, in its slot field. -/ +def LabelSrc.slotVal : LabelSrc → ℕ + | .const b => b.toNat + | .input _ => 0 + | .pos sl _ _ => sl + +/-- The selector `q` of a symbolic label: the payload is `p` (`0`) or `c - 1` (`1`), the column is +`c`, `c - 1`, `c + 1` or `2 T` (`2` to `5`), the block is `t`, `t - 1` or `T` (`6` to `8`). +Decrements of `c = 0` and `t = 0` select nothing, giving `0 = 0 - 1`. -/ +def LabelSrc.sel (c0 t0 : Bool) : LabelSrc → ℕ → Bool + | .const _, _ => false + | .input b, q => (decide (q = 0) && !b) || (decide (q = 1) && b && !c0) + | .pos _ cs ts, q => + (decide (q = 2) && decide (cs = .same)) || (decide (q = 3) && decide (cs = .prev) && !c0) || + (decide (q = 4) && decide (cs = .next)) || (decide (q = 5) && decide (cs = .last)) || + (decide (q = 6) && decide (ts = .same)) || (decide (q = 7) && decide (ts = .prev) && !t0) || + (decide (q = 8) && decide (ts = .top)) + +/-- The selector `q` of a symbolic sign: the constant `true` (`9`) or the lookup (`10`). -/ +def SignSrc.sel : SignSrc → ℕ → Bool + | .const b, q => decide (q = 9) && b + | .lookup, q => decide (q = 10) + +/-- **The tag and slot bits of a shape**: two tag bits, then the slot bits. -/ +def tagSlot (sh : Shape) (f : ℕ) : Bool := + if f < 2 then sh.1.tag.testBit f else sh.1.slotVal.testBit (f - 2) + +/-- **The selectors of a shape**, `0` to `10`. -/ +def selOf (c0 t0 : Bool) (sh : Shape) (q : ℕ) : Bool := sh.1.sel c0 t0 q || sh.2.sel q + +/-- The column field selected by `sel`, at bit `q`. -/ +def colTerm (sel : ℕ → Bool) (c T q : ℕ) : Bool := + (sel 2 && c.testBit q) || (sel 3 && (c.testBit q ^^ decide (c % 2 ^ q = 0))) || + (sel 4 && (c.testBit q ^^ decide (c % 2 ^ q = 2 ^ q - 1))) || (sel 5 && (2 * T).testBit q) + +/-- The block field selected by `sel`, at bit `q`. -/ +def timeTerm (sel : ℕ → Bool) (t T q : ℕ) : Bool := + (sel 6 && t.testBit q) || (sel 7 && (t.testBit q ^^ decide (t % 2 ^ q = 0))) || + (sel 8 && T.testBit q) + +/-- The payload bit `q` selected by the tag and slot bits `ts` and the selectors `sel`. -/ +def payTerm (ts sel : ℕ → Bool) (s cb p c t T q : ℕ) : Bool := + (decide (q < s) && ts (2 + q)) || (sel 0 && p.testBit q) || + (sel 1 && (c.testBit q ^^ decide (c % 2 ^ q = 0))) || + (decide (s ≤ q ∧ q < s + cb) && colTerm sel c T (q - s)) || + (decide (s + cb ≤ q) && timeTerm sel t T (q - s - cb)) + +/-- **The output bit `i` of a literal** with tag and slot bits `ts` and selectors `sel`: the tag +bits, then the payload bits, then the sign. This is what the output stage of the decoder +computes. -/ +def outBit (s cb tb : ℕ) (ts sel : ℕ → Bool) (p c t T : ℕ) (lk : Bool) (i : ℕ) : Bool := + if i < 2 then ts i + else if i < 2 + (s + cb + tb) then payTerm ts sel s cb p c t T (i - 2) + else sel 9 || (sel 10 && lk) + +/-- A symbolic label whose slot and column fit their fields. -/ +def LabelSrc.InRange (s cb c T : ℕ) : LabelSrc → Prop + | .pos sl cs _ => sl < 2 ^ s ∧ cs.eval c T < 2 ^ cb + | _ => True + +/-- The payload of a symbolic label. -/ +def LabelSrc.payload (s cb p c t T : ℕ) : LabelSrc → ℕ + | .const b => b.toNat + | .input false => p + | .input true => c - 1 + | .pos sl cs ts => sl + 2 ^ s * (cs.eval c T + 2 ^ cb * ts.eval t T) + +theorem LabelSrc.eval_eq (s cb p c t T : ℕ) (l : LabelSrc) : + l.eval s cb p c t T = l.tag + 4 * l.payload s cb p c t T := by + rcases l with b | (_ | _) | ⟨sl, cs, ts⟩ <;> simp [LabelSrc.eval, LabelSrc.tag, + LabelSrc.payload, constLabel, inputLabel] + +theorem LabelSrc.tag_lt (l : LabelSrc) : l.tag < 4 := by + rcases l with b | b | ⟨sl, cs, ts⟩ <;> simp [LabelSrc.tag] + +private theorem colTerm_eq {c T q sl : ℕ} (cs : ColSrc) (ts : TimeSrc) (t0 : Bool) + (sg : SignSrc) : + colTerm (selOf (decide (c = 0)) t0 (.pos sl cs ts, sg)) c T q = (cs.eval c T).testBit q := by + cases sg <;> cases cs <;> simp only [colTerm, selOf, LabelSrc.sel, SignSrc.sel, ColSrc.eval] <;> + simp only [decide_true, reduceCtorEq, decide_false, Bool.and_false, Nat.reduceEqDiff, + Bool.and_self, Bool.false_and, Bool.or_self, Nat.succ_ne_self, Nat.zero_testBit, + Bool.or_false, Bool.true_and, Bool.and_true, Bool.false_or, Bool.or_true] + all_goals first + | rw [Nat.testBit_add_one_eq_xor] + | (by_cases hc : c = 0 + · simp [hc] + · rw [Nat.testBit_sub_one_eq_xor (by omega)]; simp [hc]) + +private theorem timeTerm_eq {t T q sl : ℕ} (cs : ColSrc) (ts : TimeSrc) (c0 : Bool) + (sg : SignSrc) : + timeTerm (selOf c0 (decide (t = 0)) (.pos sl cs ts, sg)) t T q = (ts.eval t T).testBit q := by + cases sg <;> cases ts <;> simp only [timeTerm, selOf, LabelSrc.sel, SignSrc.sel, TimeSrc.eval] <;> + simp only [Nat.reduceEqDiff, decide_false, Bool.false_and, Bool.or_self, Nat.succ_ne_self, + decide_true, Bool.and_self, Bool.or_true, reduceCtorEq, Bool.or_false, Bool.true_and, + Bool.and_true, Bool.and_false, Bool.false_or] + all_goals + by_cases ht : t = 0 + · simp [ht] + · rw [Nat.testBit_sub_one_eq_xor (by omega)]; simp [ht] + +/-- **The output bits of a shape are the bits of its literal**: its label below `2 + P` and its +sign at `2 + P`, for `P = s + cb + tb`, at least one slot bit, a looked-up bit that is the bit of +`x` at `p` whenever it is used, and a label whose slot and column fit their fields. -/ +theorem outBit_shape {s cb tb p c t T : ℕ} {x : List Bool} {lk : Bool} (hs : 1 ≤ s) + {sh : Shape} (hR : sh.1.InRange s cb c T) (hlk : sh.2 = .lookup → lk = x.getD p false) + {i : ℕ} (hi : i ≤ 2 + (s + cb + tb)) : + outBit s cb tb (tagSlot sh) (selOf (decide (c = 0)) (decide (t = 0)) sh) p c t T lk i = + if i < 2 + (s + cb + tb) then (sh.1.eval s cb p c t T).testBit i else sh.2.eval x p := by + obtain ⟨l, sg⟩ := sh + rw [LabelSrc.eval_eq, Nat.testBit_add_four_mul l.tag_lt] + unfold outBit + by_cases h2 : i < 2 + · simp [h2, tagSlot, show i < 2 + (s + cb + tb) by omega] + · by_cases hP : i < 2 + (s + cb + tb) + · simp only [h2, hP, ↓reduceIte] + have hq : i - 2 < s + cb + tb := by omega + have hts : 2 + (i - 2) = i := by omega + generalize i - 2 = q at hq hts ⊢ + subst hts + have h21 : ¬ 2 + q ≤ 1 := by omega + rcases l with b | (_ | _) | ⟨sl, cs, ts⟩ + · cases sg <;> simp only [payTerm, tagSlot, Order.lt_two_iff, h21, ↓reduceIte, + LabelSrc.slotVal, add_tsub_cancel_left, selOf, LabelSrc.sel, SignSrc.sel, + OfNat.zero_ne_ofNat, decide_false, Bool.false_and, Bool.or_self, Bool.or_false, + OfNat.one_ne_ofNat, Bool.decide_and, colTerm, Nat.reduceEqDiff, Bool.and_false, timeTerm, + LabelSrc.payload, Bool.and_eq_right_iff_imp, decide_eq_true_eq] + all_goals + intro hqs + cases b <;> simp [Nat.testBit_one_eq_true_iff_self_eq_zero] at hqs + omega + · cases sg <;> simp [payTerm, tagSlot, selOf, LabelSrc.sel, SignSrc.sel, LabelSrc.payload, + LabelSrc.slotVal, colTerm, timeTerm, h21] + · cases sg <;> simp only [payTerm, tagSlot, Order.lt_two_iff, h21, ↓reduceIte, + LabelSrc.slotVal, add_tsub_cancel_left, Nat.zero_testBit, Bool.and_false, selOf, + LabelSrc.sel, decide_true, Bool.not_true, zero_ne_one, decide_false, Bool.and_true, + Bool.false_and, Bool.or_self, SignSrc.sel, OfNat.zero_ne_ofNat, one_ne_zero, + Bool.and_self, Bool.true_and, Bool.false_or, OfNat.one_ne_ofNat, Bool.or_false, + Bool.decide_and, colTerm, OfNat.ofNat_ne_zero, OfNat.ofNat_ne_one, Nat.reduceEqDiff, + timeTerm, LabelSrc.payload] + all_goals + by_cases hc : c = 0 + · simp [hc] + · rw [Nat.testBit_sub_one_eq_xor (by omega)]; simp [hc] + · obtain ⟨hsl, hC⟩ := hR + rw [LabelSrc.payload, Nat.testBit_add_two_pow_mul_add_two_pow_mul hsl hC] + have hcol := colTerm_eq (c := c) (T := T) (q := q - s) (sl := sl) cs ts (decide (t = 0)) sg + have htime := timeTerm_eq (t := t) (T := T) (q := q - s - cb) (sl := sl) cs ts + (decide (c = 0)) sg + simp only [payTerm, hcol, htime] + have h0 : selOf (decide (c = 0)) (decide (t = 0)) (.pos sl cs ts, sg) 0 = false := by + cases sg <;> simp [selOf, LabelSrc.sel, SignSrc.sel] + have h1 : selOf (decide (c = 0)) (decide (t = 0)) (.pos sl cs ts, sg) 1 = false := by + cases sg <;> simp [selOf, LabelSrc.sel, SignSrc.sel] + simp only [h0, h1, Bool.false_and, Bool.or_false, tagSlot, + show ¬ 2 + q < 2 by omega, ↓reduceIte, LabelSrc.slotVal, Nat.add_sub_cancel_left] + by_cases hqs : q < s + · simp [hqs, show ¬ s ≤ q by omega, show ¬ s + cb ≤ q by omega] + · by_cases hqc : q < s + cb + · simp [hqs, hqc, show s ≤ q by omega, show ¬ s + cb ≤ q by omega] + · simp [hqs, hqc, show s + cb ≤ q by omega] + · simp only [h2, hP, ↓reduceIte] + cases sg <;> rcases l with b | b | ⟨sl, cs, ts⟩ <;> + simp only [selOf, LabelSrc.sel, SignSrc.sel, decide_true, Bool.true_and, Bool.false_or, + Nat.succ_ne_self, decide_false, Bool.false_and, Bool.or_self, Bool.or_false, + SignSrc.eval, OfNat.ofNat_ne_zero, OfNat.ofNat_ne_one, Nat.reduceEqDiff, Bool.or_true, + List.getD_eq_getElem?_getD] + all_goals exact hlk rfl + +end Bits + +/-! ### The shapes stay within their fields -/ + +section Range + +theorem fst_mem_tseitinClause {V : Type} {op : Op} {w a b : V} {j : Fin 3} {l : Literal V} + (h : l ∈ tseitinClause op w a b j) : l.1 = w ∨ l.1 = a ∨ l.1 = b := by + obtain ⟨v, s⟩ := l + fin_cases j <;> cases op <;> simp [tseitinClause] at h <;> aesop + +variable {X n T : ℕ} + +omit [DecidableEq State] in +theorem refSrc_inRange {j tag p : ℕ} {r : Ref k State} + (hr : r.InWindow n T (colOf (slotBits k State) (colBits T) p)) : + ((Key.ofFields (slotBits k State) (colBits T) X n T j tag p).refSrc r).InRange + (slotBits k State) (colBits T) (colOf (slotBits k State) (colBits T) p) T := by + rcases r with _ | _ | _ | ⟨q, l, cs, g⟩ + · trivial + · trivial + · simp only [Key.refSrc]; split <;> trivial + · simp only [Key.refSrc, Key.guard_ofFields] + split + · rename_i hg + refine ⟨slot_lt_two_pow l, ?_⟩ + rw [colSrcOf_eval] + exact lt_of_le_of_lt (Loc.labelCol_le l _) (lt_of_lt_of_le (hr hg) (numCols_le_two_pow T)) + · trivial + +/-- A property of every literal of every branch of `shapeOf` holds of its literals. -/ +theorem forall_mem_shapeOf {P : Shape → Prop} (κ : Key) (htaut : ∀ sh ∈ tautShape, P sh) + (h0 : ∀ (hj : κ.j < 3), ∀ sh ∈ lift (tseitinClause (.const !κ.p0) (.const !κ.p0) + (.const false) (.const false) ⟨κ.j, hj⟩), P sh) + (h1 : κ.pLtX = true → P (.input false, .lookup)) + (h2 : ∀ (hj : κ.j < 3) (l : Loc k State), Loc.ofSlot κ.slot = some l → + (!κ.tGtT && κ.colOK l) = true → ∀ sh ∈ lift (posShape tm κ l ⟨κ.j, hj⟩), P sh) + (h3 : P (outSrc (k := k) (State := State), .const true)) : + ∀ sh ∈ shapeOf tm κ, P sh := by + intro sh hsh + unfold shapeOf at hsh + by_cases hj : κ.j < 3 + · rw [dite_eq_left hj] at hsh + by_cases ht0 : κ.tag = 0 + · rw [ite_eq_left ht0] at hsh + split at hsh + · exact h0 hj sh hsh + · exact htaut sh hsh + · rw [ite_eq_right ht0] at hsh + by_cases ht1 : κ.tag = 1 + · rw [ite_eq_left ht1] at hsh + split at hsh + · rename_i hc + simp only [List.mem_cons, List.not_mem_nil, or_false] at hsh + rcases hsh with rfl | rfl | rfl <;> exact h1 hc.2 + · exact htaut sh hsh + · rw [ite_eq_right ht1] at hsh + by_cases ht2 : κ.tag = 2 + · rw [ite_eq_left ht2] at hsh + split at hsh + · rename_i l hl + split at hsh + · rename_i hok + exact h2 hj l hl hok sh hsh + · exact htaut sh hsh + · exact htaut sh hsh + · rw [ite_eq_right ht2] at hsh + split at hsh + · simp only [List.mem_cons, List.not_mem_nil, or_false] at hsh + rcases hsh with rfl | rfl | rfl <;> exact h3 + · exact htaut sh hsh + · rw [dite_eq_right hj] at hsh + exact htaut sh hsh + +/-- **The labels of the shapes fit their fields.** -/ +theorem inRange_of_mem_shapeOf {j tag p : ℕ} {sh : Shape} + (hsh : sh ∈ shapeOf tm (Key.ofFields (slotBits k State) (colBits T) X n T j tag p)) : + sh.1.InRange (slotBits k State) (colBits T) (colOf (slotBits k State) (colBits T) p) T := by + have hc : colOf (slotBits k State) (colBits T) p < 2 ^ colBits T := + Nat.mod_lt _ (Nat.two_pow_pos _) + refine forall_mem_shapeOf (P := fun sh => sh.1.InRange (slotBits k State) (colBits T) + (colOf (slotBits k State) (colBits T) p) T) tm _ ?_ ?_ ?_ ?_ ?_ sh hsh + · intro sh hsh + simp only [tautShape, List.mem_cons, List.not_mem_nil, or_false] at hsh + rcases hsh with rfl | rfl | rfl <;> trivial + · intro hj sh hsh + simp only [lift, List.mem_map] at hsh + obtain ⟨l, hl, rfl⟩ := hsh + rcases fst_mem_tseitinClause hl with h | h | h <;> simp only [h] <;> trivial + · intro _; trivial + · intro hj l _ hok sh hsh + simp only [lift, List.mem_map] at hsh + obtain ⟨lit, hlit, rfl⟩ := hsh + have hok' : l.ColOK T (colOf (slotBits k State) (colBits T) p) := by + have := Key.colOK_ofFields (s := slotBits k State) (cb := colBits T) (X := X) (n := n) + (T := T) j tag p l + simp only [Bool.and_eq_true] at hok + simpa [this] using hok.2 + have hw := table_inWindow (n := n) hok'.lt tm l + unfold posShape at hlit + generalize table tm l = e at hw hlit + obtain ⟨op, a, b⟩ := e + obtain ⟨hra, hrb⟩ := hw + split_ifs at hlit <;> rcases fst_mem_tseitinClause hlit with h | h | h <;> simp only [h] + all_goals first + | trivial + | exact ⟨slot_lt_two_pow _, hc⟩ + | exact refSrc_inRange hra + | exact refSrc_inRange hrb + · exact ⟨slot_lt_two_pow _, Nat.two_pow_pos _⟩ + +/-- **A shape looks up `x` only at a payload within it.** -/ +theorem lt_of_mem_shapeOf {j tag p : ℕ} {sh : Shape} + (hsh : sh ∈ shapeOf tm (Key.ofFields (slotBits k State) (colBits T) X n T j tag p)) + (hlk : sh.2 = .lookup) : p < X := by + revert hlk + refine forall_mem_shapeOf (P := fun sh => sh.2 = .lookup → p < X) tm _ ?_ ?_ ?_ ?_ ?_ sh hsh + · intro sh hsh + simp only [tautShape, List.mem_cons, List.not_mem_nil, or_false] at hsh + rcases hsh with rfl | rfl | rfl <;> simp + · intro hj sh hsh + simp only [lift, List.mem_map] at hsh + obtain ⟨l, -, rfl⟩ := hsh + simp + · intro h _ + simpa [Key.ofFields] using h + · intro hj l _ _ sh hsh + simp only [lift, List.mem_map] at hsh + obtain ⟨l, -, rfl⟩ := hsh + simp + · simp + +/-- A shape has three literals. -/ +theorem length_shapeOf (κ : Key) : (shapeOf tm κ).length = 3 := by + unfold shapeOf + split + · split + · split + · simp [lift] + · rfl + · split + · split <;> rfl + · split + · split + · split + · simp only [lift, List.length_map, posShape] + split <;> simp + · rfl + · rfl + · split <;> rfl + · rfl + +end Range + +end Cslib.Circuits.Boolean.Tableau.Decoder diff --git a/Complexity/Computability/Complexity/Reduction/TruthTableVariants.lean b/Complexity/Computability/Complexity/Reduction/TruthTableVariants.lean index bd12a82a65..0e4c8e2a73 100644 --- a/Complexity/Computability/Complexity/Reduction/TruthTableVariants.lean +++ b/Complexity/Computability/Complexity/Reduction/TruthTableVariants.lean @@ -9,6 +9,7 @@ module public import Complexity.Computability.Complexity.Reduction.TruthTable import Complexity.Foundations.Data.List.Filter +import Complexity.Foundations.Data.List.RowMajor import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat @@ -146,25 +147,6 @@ The composite of `(r, q, d)` from `L` to `B` and `(r', q', d')` from `B` to `C` first-stage query `q (a, i)`, its second-stage queries in a block of `M a ≥ r' (q (a, i))` positions starting at `i * M a`, and evaluates `d'` on each block and `d` on the results. -/ -/-- Indexing a flattened list whose blocks all have length `M`. -/ -private theorem getElem?_flatMap_of_length_eq {ι δ : Type*} (l : List ι) (f : ι → List δ) (M : ℕ) - (hf : ∀ x ∈ l, (f x).length = M) {i j : ℕ} (hi : i < l.length) (hj : j < M) : - (l.flatMap f)[i * M + j]? = (f l[i])[j]? := by - induction l generalizing i with - | nil => simp at hi - | cons x l ih => - have hx := hf x (by simp) - rw [List.flatMap_cons] - cases i with - | zero => - simp only [zero_mul, zero_add, List.getElem_cons_zero] - rw [List.getElem?_append_left (by omega)] - | succ i => - rw [List.getElem?_append_right (by rw [hx]; nlinarith), hx] - have : (i + 1) * M + j - M = i * M + j := by rw [Nat.succ_mul]; omega - rw [this, ih (fun y hy => hf y (by simp [hy])) (by simpa using hi)] - simp - /-- A block of a word of answers. -/ private theorem take_drop_ofFn {n : ℕ} (g : Fin n → Bool) (s c : ℕ) (h : s + c ≤ n) : ((List.ofFn g).drop s).take c = List.ofFn fun j : Fin c => g ⟨s + j, by omega⟩ := by @@ -213,7 +195,7 @@ private theorem ttComp_spec {r : α → ℕ} {q : α × ℕ → β} {d : α × L funext j have hj : j.1 < M a := lt_of_lt_of_le j.2 (hM a i hi) simp only [Set.mem_preimage, ttCompQuery, ttCompQueries] - rw [getElem?_flatMap_of_length_eq _ _ _ hlen (by simpa using hi) hj] + rw [List.getElem?_flatMap_mul_add _ _ _ hlen (by simpa using hi) hj] simp [hj] rw [hblock] cases h : d' (q (a, i), truthTableAnswers (q' ⁻¹' C) r' (q (a, i))) <;> simp [hB, h] diff --git a/Complexity/Foundations/Data/List/RowMajor.lean b/Complexity/Foundations/Data/List/RowMajor.lean index c03ab40239..e7ffdc9922 100644 --- a/Complexity/Foundations/Data/List/RowMajor.lean +++ b/Complexity/Foundations/Data/List/RowMajor.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Erik Demaine. All rights reserved. +Copyright (c) 2026 Erik Demaine, Christian Reitwiessner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Erik Demaine +Authors: Erik Demaine, Christian Reitwiessner -/ module @@ -22,6 +22,8 @@ import Mathlib.Data.List.GetD * `List.flatMap_ofFn_prod`: nested row-major enumeration agrees with the existing product equivalence on finite indices. * `List.getD_flatMap_ofFn`: read a cell at its ordinary flat row-major index. +* `List.getElem?_flatMap_mul_add`: read entry `j` of block `i` of a flattened list whose blocks + all have length `M`. -/ @[expose] public section @@ -61,4 +63,24 @@ theorem getD_flatMap_ofFn {α : Type*} {n d : ℕ} (f : Fin n → Fin d → α) exact (finProdFinEquiv (i, j)).isLt), List.getElem_ofFn] exact congrArg (fun p => f p.1 p.2) (finProdFinEquiv.symm_apply_apply (i, j)) +/-- Indexing a flattened list whose blocks all have length `M`: position `i * M + j` is entry `j` +of block `i`. -/ +theorem getElem?_flatMap_mul_add {ι δ : Type*} (l : List ι) (f : ι → List δ) (M : ℕ) + (hf : ∀ x ∈ l, (f x).length = M) {i j : ℕ} (hi : i < l.length) (hj : j < M) : + (l.flatMap f)[i * M + j]? = (f l[i])[j]? := by + induction l generalizing i with + | nil => simp at hi + | cons x l ih => + have hx := hf x (by simp) + rw [List.flatMap_cons] + cases i with + | zero => + simp only [Nat.zero_mul, Nat.zero_add, List.getElem_cons_zero] + rw [List.getElem?_append_left (by omega)] + | succ i => + rw [List.getElem?_append_right (by rw [hx, Nat.succ_mul]; omega), hx] + have : (i + 1) * M + j - M = i * M + j := by rw [Nat.succ_mul]; omega + rw [this, ih (fun y hy => hf y (by simp [hy])) (by simpa using hi)] + simp + end List diff --git a/Complexity/Foundations/Data/Nat/Bitwise/Carry.lean b/Complexity/Foundations/Data/Nat/Bitwise/Carry.lean new file mode 100644 index 0000000000..0b014bc97e --- /dev/null +++ b/Complexity/Foundations/Data/Nat/Bitwise/Carry.lean @@ -0,0 +1,101 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Data.Nat.Bitwise + +/-! +# Bits of successors, predecessors and packed fields + +Incrementing a number flips bit `q` exactly when all lower bits are one, and decrementing a +positive number flips it exactly when all lower bits are zero. A number packed from fields of +fixed widths has, in each window of bits, the bits of the corresponding field. + +## Main results + +* `Nat.testBit_add_one_eq_xor`, `Nat.testBit_sub_one_eq_xor`: the bits of `c + 1` and `c - 1`. +* `Nat.testBit_add_four_mul`: the bits of a two-bit tag followed by a payload. +* `Nat.testBit_add_two_pow_mul_add_two_pow_mul`: the bits of three packed fields. +-/ + +@[expose] public section + +namespace Nat + +/-- Bit `q` of `c - 1`, for `1 ≤ c`: bit `q` of `c`, flipped when the lower bits of `c` are +zero. -/ +theorem testBit_sub_one_eq_xor {c : ℕ} (hc : 1 ≤ c) (q : ℕ) : + (c - 1).testBit q = (c.testBit q ^^ decide (c % 2 ^ q = 0)) := by + induction q generalizing c with + | zero => + simp only [Nat.testBit_zero, pow_zero, Nat.mod_one, decide_true, Bool.xor_true] + rw [Bool.eq_iff_iff] + simp only [decide_eq_true_eq, Bool.not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not, + Nat.mod_two_not_eq_one] + omega + | succ q ih => + rw [Nat.testBit_succ, Nat.testBit_succ, Nat.pow_succ', Nat.mod_mul] + rcases Nat.even_or_odd c with ⟨d, rfl⟩ | ⟨d, rfl⟩ + · have hd : 1 ≤ d := by omega + have h₁ : (d + d - 1) / 2 = d - 1 := by omega + have h₂ : (d + d) / 2 = d := by omega + have h₃ : (d + d) % 2 = 0 := by omega + rw [h₁, h₂, ih hd, h₃] + congr 2 + rw [Nat.zero_add, Nat.mul_eq_zero] + simp + · have h₁ : (2 * d + 1 - 1) / 2 = d := by omega + have h₂ : (2 * d + 1) / 2 = d := by omega + have h₃ : (2 * d + 1) % 2 = 1 := by omega + rw [h₁, h₂, h₃] + simp + +/-- Bit `q` of `c + 1`: bit `q` of `c`, flipped when the lower bits of `c` are all one. -/ +theorem testBit_add_one_eq_xor (c q : ℕ) : + (c + 1).testBit q = (c.testBit q ^^ decide (c % 2 ^ q = 2 ^ q - 1)) := by + induction q generalizing c with + | zero => + simp only [Nat.testBit_zero, pow_zero, Nat.mod_one, Nat.sub_self, decide_true, Bool.xor_true] + rw [Bool.eq_iff_iff] + simp only [decide_eq_true_eq, Bool.not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not, + Nat.mod_two_not_eq_one] + omega + | succ q ih => + rw [Nat.testBit_succ, Nat.testBit_succ, Nat.pow_succ', Nat.mod_mul] + have hq := Nat.one_le_two_pow (n := q) + rcases Nat.even_or_odd c with ⟨d, rfl⟩ | ⟨d, rfl⟩ + · have h₁ : (d + d + 1) / 2 = d := by omega + have h₂ : (d + d) / 2 = d := by omega + have h₃ : (d + d) % 2 = 0 := by omega + rw [h₁, h₂, h₃] + have : ¬ (2 * (d % 2 ^ q) = 2 * 2 ^ q - 1) := by omega + simp [this] + · have h₁ : (2 * d + 1 + 1) / 2 = d + 1 := by omega + have h₂ : (2 * d + 1) / 2 = d := by omega + have h₃ : (2 * d + 1) % 2 = 1 := by omega + rw [h₁, h₂, h₃, ih d] + congr 2 + exact propext ⟨fun h => by omega, fun h => by omega⟩ + +/-- The bits of a tag and a payload. -/ +theorem testBit_add_four_mul {tag : ℕ} (htag : tag < 4) (pay i : ℕ) : + (tag + 4 * pay).testBit i = if i < 2 then tag.testBit i else pay.testBit (i - 2) := by + rw [Nat.add_comm, show 4 = 2 ^ 2 from rfl, Nat.testBit_two_pow_mul_add _ htag] + +/-- The bits of three fields of widths `s` and `cb` and a high field. -/ +theorem testBit_add_two_pow_mul_add_two_pow_mul {s cb sl C Tm : ℕ} (hsl : sl < 2 ^ s) + (hC : C < 2 ^ cb) (q : ℕ) : + (sl + 2 ^ s * (C + 2 ^ cb * Tm)).testBit q = + if q < s then sl.testBit q else if q < s + cb then C.testBit (q - s) + else Tm.testBit (q - s - cb) := by + rw [Nat.add_comm, Nat.testBit_two_pow_mul_add _ hsl, Nat.add_comm C, + Nat.testBit_two_pow_mul_add _ hC] + split_ifs <;> first | rfl | omega + +end Nat diff --git a/ComplexityTests/TableauDecoder.lean b/ComplexityTests/TableauDecoder.lean new file mode 100644 index 0000000000..84bda62d83 --- /dev/null +++ b/ComplexityTests/TableauDecoder.lean @@ -0,0 +1,89 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Circuit.Boolean.Tableau.Decoder.Assembly + +/-! +# The decoder of the succinct tableau + +The field stage is evaluated on concrete clause numbers with `decide`: one slot bit, two column +bits, one block bit, `x = [true, false]`, `n = 1` and `T = 1`, so `8` inputs and `75` gates. The +comparison chains, the borrows and carries, and the lookup of `x` give the expected values. The +constant stage depends on the noncomputable numbering of positions (`Loc.slot`), so the whole +decoder is checked on a concrete machine through its correctness theorem: the clauses fixing the +inputs and the output have explicit literals, which the decoder emits bit by bit. +-/ + +namespace ComplexityTests.TableauDecoder + +open Cslib Cslib.Circuits Cslib.Circuits.Boolean Cslib.Circuits.Boolean.Tableau +open Cslib.Circuits.Boolean.Tableau.Decoder + +/-- The field stage of the example. -/ +private def gates : List (Op × List ℕ) := fieldGates 1 2 1 [true, false] 1 1 + +/-- The value of wire `w` on the clause number `idx`. -/ +private def wire (idx w : ℕ) : Bool := evalOutput (List.ofFn fun i : Fin 8 => idx.testBit i) gates w + +example : gates.length = 75 := by decide + +-- Chain 4 compares the column `c = idx / 32 % 4` with `n = 1`; its last gate is wire `37`. +example : wire 64 37 = true ∧ wire 32 37 = false ∧ wire 96 37 = true := by decide + +-- Chain 0 gives the borrows of `c - 1`: after one bit, `c % 2 = 0`. +example : wire 64 18 = true ∧ wire 32 18 = false := by decide + +-- Chain 11 compares the payload `p = idx / 16` with the length `2` of `x`. +example : wire 16 (18 + 11 * 4 + 3) = true ∧ wire 32 (18 + 11 * 4 + 3) = false := by decide + +-- The lookup of `x` at the payload is wire `82`: `x[0] = true` and `x[1] = false`. +example : wire 5 82 = true ∧ wire 19 82 = false := by decide + +-- Every wire agrees with its intended value on these clause numbers. +example : (List.range 83).all (fun w => wire 100 w == fieldVal 1 2 1 [true, false] 1 1 100 w) := + by decide +example : (List.range 83).all (fun w => wire 211 w == fieldVal 1 2 1 [true, false] 1 1 211 w) := + by decide + +/-- A machine without work tapes that halts at once with output `[true]`. -/ +private def halt : Turing.MultiTapeTM 0 Bool Unit := + Turing.MultiTapeTM.ofTr () fun _ _ _ => + { inputTape := 0, workTapes := Fin.elim0, output := some true, state := none } + +-- The decoder of `halt` for `x = [true, false]`, `n = 2` and `T = 2`. Clause numbers `4` and `20` +-- (tag `1`) fix the inputs `0` and `1` to `x[0] = true` and `x[1] = false`: each of their three +-- literals is the label `inputLabel i = 1 + 4 i` in `labelBits` bits, then the sign `x[i]`. Clause +-- number `12` (tag `3`) fixes the output wire to `true`. +example : ∃ c : Circuit signature (clauseBits 0 Unit 2) (3 * (labelBits 0 Unit 2 + 1)), + List.ofFn (c.eval interpretation fun i => (4 : ℕ).testBit i) = + [(1, true), (1, true), (1, true)].flatMap (litBits (labelBits 0 Unit 2)) ∧ + List.ofFn (c.eval interpretation fun i => (20 : ℕ).testBit i) = + [(5, false), (5, false), (5, false)].flatMap (litBits (labelBits 0 Unit 2)) ∧ + List.ofFn (c.eval interpretation fun i => (12 : ℕ).testBit i) = + (unitClause (outLabel 0 Unit 2, true)).flatMap (litBits (labelBits 0 Unit 2)) := by + obtain ⟨c, -, -, hc⟩ := exists_decoder halt [true, false] (n := 2) (T := 2) (by norm_num) + (by norm_num) + have hbits : 2 ^ 5 ≤ 2 ^ clauseBits 0 Unit 2 := Nat.pow_le_pow_right (by norm_num) (by + have := one_le_slotBits (k := 0) (State := Unit) + simp only [clauseBits] + omega) + refine ⟨c, ?_, ?_, ?_⟩ <;> rw [hc _ (by omega)] <;> + simp [clauseAt, clauseOf, unitClause, inputLabel] + +variable {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] + (tm : Turing.MultiTapeTM k Bool State) + +-- The decoder of any machine: its code, a linear size bound, and the bits of every clause. +example (x : List Bool) (n T : ℕ) (hn : n < 2 * T) (hx : x.length ≤ n) : + ∃ c : Circuit signature (clauseBits k State T) (3 * (labelBits k State T + 1)), + c.code = decoderCode tm (x, n, T) ∧ + c.size ≤ sizeConst tm * (colBits T + timeBits T + x.length + 1) ∧ + ∀ idx < 2 ^ clauseBits k State T, + List.ofFn (c.eval interpretation fun i => idx.testBit i) = + (clauseAt tm x n T idx).flatMap (litBits (labelBits k State T)) := + exists_decoder tm x hn hx + +end ComplexityTests.TableauDecoder