From 83c8a7c862080323aa6bc22b16eeca5288f7ab94 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Fri, 28 Aug 2026 21:46:57 -0700 Subject: [PATCH 1/6] feat(tocslib): add polynomial-time single-tape toolkit --- AGENTS.md | 4 + PolyFunTest/ToCslib/Basic.lean | 37 ++ ToCslib.lean | 20 + ToCslib/Computability/BitEncoding.lean | 455 +++++++++++++++ ToCslib/Computability/PolyTime.lean | 214 +++++++ .../SingleTape/BasicMachines.lean | 525 ++++++++++++++++++ .../Computability/SingleTape/Counting.lean | 518 +++++++++++++++++ ToCslib/Data/BitVec.lean | 78 +++ docs/wiki/repo-map.md | 12 + lakefile.toml | 10 +- 10 files changed, 1871 insertions(+), 2 deletions(-) create mode 100644 PolyFunTest/ToCslib/Basic.lean create mode 100644 ToCslib.lean create mode 100644 ToCslib/Computability/BitEncoding.lean create mode 100644 ToCslib/Computability/PolyTime.lean create mode 100644 ToCslib/Computability/SingleTape/BasicMachines.lean create mode 100644 ToCslib/Computability/SingleTape/Counting.lean create mode 100644 ToCslib/Data/BitVec.lean diff --git a/AGENTS.md b/AGENTS.md index cc914dc..ab2ff75 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -112,6 +112,10 @@ and depend on this library. - `PolyFun/Control/LTS/Trace.lean`: generic finite visible traces over the silent/visible `Control.LTS` layer and preservation by weak simulation. - `PolyFun/Logic/`: small logic helpers (`HEq`). +- `ToCslib/`: a separate low-level Lake library of reusable extensions to the + pinned cslib machine API. It imports cslib and Mathlib but never PolyFun, + oracle semantics, probability, or cryptography. Concrete PolyFun backend + adapters may import it explicitly; the generated `PolyFun` umbrella does not. - `PolyFunTest/`: separate test / worked-example library (glob `PolyFunTest.+`), built by `lake test` and kept out of the `lake lint` scope. Holds the dynamical / interaction worked examples and the diff --git a/PolyFunTest/ToCslib/Basic.lean b/PolyFunTest/ToCslib/Basic.lean new file mode 100644 index 0000000..ade9037 --- /dev/null +++ b/PolyFunTest/ToCslib/Basic.lean @@ -0,0 +1,37 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma, Elias Judin, Quang Dao +-/ + +module + +public import ToCslib + +/-! +# Direct canaries for the ToCslib substrate + +These examples pin bit order, finite-table semantic orientation, overwrite +selection, and the cardinality used by the machine-counting argument. +-/ + +open ToCslib.Computability + +example : natToBits 3 5 = [true, false, true] := by decide + +example (bit : Bool) : + let encoding : Bool → List Bool := fun value => [value] + let witness := EncPolyTime.ofFintype encoding (by + intro left right equality + have headEquality := congrArg List.head? equality + simpa [encoding] using headEquality) encoding (!·) + witness.toFun (encoding bit) = encoding (!bit) := by + dsimp only + exact EncPolyTime.map_encode _ bit + +example {n index : ℕ} (hindex : index < n) (bit : Bool) (value : BitVec n) : + (value.overwriteBit index bit).getLsbD index = bit := by + exact BitVec.getLsbD_overwriteBit_self hindex bit value + +example : Fintype.card (BitVec 2 → Bool) = 16 := by + simpa using card_bitVec_fun 2 diff --git a/ToCslib.lean b/ToCslib.lean new file mode 100644 index 0000000..4d8a188 --- /dev/null +++ b/ToCslib.lean @@ -0,0 +1,20 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma, Elias Judin +-/ + +module + +public import ToCslib.Computability.BitEncoding +public import ToCslib.Computability.SingleTape.Counting +public import ToCslib.Data.BitVec + +/-! +# Extensions of the pinned cslib machine library + +This library contains reusable facts and constructions about cslib machines. It +does not import PolyFun's realizability theory or any downstream oracle or +cryptographic semantics. Backend adapters in `PolyFun.Realizability.Backend` +may import these modules explicitly. +-/ diff --git a/ToCslib/Computability/BitEncoding.lean b/ToCslib/Computability/BitEncoding.lean new file mode 100644 index 0000000..78d9d3e --- /dev/null +++ b/ToCslib/Computability/BitEncoding.lean @@ -0,0 +1,455 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ +module + +public import ToCslib.Computability.SingleTape.BasicMachines +public import Mathlib.Data.Nat.Bitwise +public import Mathlib.Data.Nat.Log + +/-! +# Canonical Fixed-Width Bit Encodings and Uniform Machine Families + +The canonical boundary representation for the polynomial-time adversary model, and the +reusable unit of machine-computability it consumes. + +## Why fixed canonical encodings + +"Computable in polynomial time relative to *some* encoding" is vacuous: an encoding +`enc x := std x ++ block (f x)` caches any function `f` inside the representation, and +every machine witness degenerates to a projection. Polynomial time is only well-defined +relative to a *fixed canonical* representation (syntactic frameworks fix one implicitly +through the programming language's value representation; a machine-grounded framework +must fix it explicitly). This file provides that representation: + +* `ToCslib.Computability.StrEncFam` — a security-parameter-indexed family of injective raw + `List Bool` encodings with a polynomial length bound. This is the *variable-width* + notion, the representation freedom left to a machine's internal state. +* `ToCslib.Computability.BitEncFam` — the *fixed-width* refinement: at each parameter every + value encodes to exactly `wid n` bits, with `wid` polynomially bounded. This is the + canonical *boundary* representation for inputs, outputs, and oracle interfaces. The + polynomial width bound is the formal content of the Katz–Lindell `1^n` convention: + all game values at parameter `n` have `poly(n)`-length representations, so + "polynomial in `n`" and "polynomial in the input length" agree. +* Constructors: `BitEncFam.const` (fixed-width binary index encoding of a finite type), + `BitEncFam.bitVec`/`bitVecX` (raw bits), `BitEncFam.pair` (append — widths are fixed, + so no tags or alphabets are needed), `BitEncFam.option` (tag bit plus padded payload), + and `StrEncFam.pairVar` (variable-width left ++ fixed-width right, injective because + the split point is determined from the right — the shape of a machine's + state/answer update input). +* `ToCslib.Computability.EncPolyTimeFam` — a family of `EncPolyTime` witnesses with uniform + polynomial time and description-size bounds: the reusable unit "this function family + is computed by polynomial machines relative to these encodings". Base machines + produce these; the closure combinators (`comp`, `id`, `const`, `ofFintype`) compose + them; a polynomial-time adversary carries four of them. + +Everything here is raw `α → List Bool`: no intermediate alphabet types and no one-hot +symbol relabeling — encodings are binary from the start, so encoded lengths are the +bit-lengths the polynomial bounds speak about. +-/ + +@[expose] public section + +universe u + +open Cslib.Turing.SingleTapeTM + +namespace ToCslib.Computability + +/-! ## Fixed-width binary strings for natural numbers -/ + +/-- The `w` low bits of `m`, least significant first. -/ +def natToBits (w m : ℕ) : List Bool := (List.range w).map m.testBit + +@[simp] theorem length_natToBits (w m : ℕ) : (natToBits w m).length = w := by + simp [natToBits] + +/-- Distinct numbers below `2 ^ w` have distinct `w`-bit strings. -/ +theorem natToBits_inj {w m₁ m₂ : ℕ} (h₁ : m₁ < 2 ^ w) (h₂ : m₂ < 2 ^ w) + (h : natToBits w m₁ = natToBits w m₂) : m₁ = m₂ := by + refine Nat.eq_of_testBit_eq fun i => ?_ + rcases lt_or_ge i w with hi | hi + · have := List.map_inj_left.mp (by simpa [natToBits] using h) i (List.mem_range.mpr hi) + exact this + · rw [Nat.testBit_eq_false_of_lt (lt_of_lt_of_le h₁ (Nat.pow_le_pow_right (by omega) hi)), + Nat.testBit_eq_false_of_lt (lt_of_lt_of_le h₂ (Nat.pow_le_pow_right (by omega) hi))] + +/-! ## Variable-width bounded string encodings -/ + +/-- A security-parameter-indexed family of injective raw bit-string encodings with a +polynomial length bound: the representation freedom left to a machine's internal +state. Injectivity is the only semantic demand; the length bound is what keeps +resource accounting polynomial. -/ +structure StrEncFam (α : ℕ → Type u) : Type u where + /-- The raw bit-string encoding at each parameter. -/ + enc : (n : ℕ) → α n → List Bool + /-- The encoding is injective at each parameter. -/ + enc_injective : ∀ n, Function.Injective (enc n) + /-- Polynomial bound on encoded lengths (over *all* values, not only reachable ones). -/ + bound : Polynomial ℕ + /-- All encodings respect the length bound. -/ + len_le : ∀ n x, (enc n x).length ≤ bound.eval n + +/-! ## Fixed-width canonical boundary encodings -/ + +/-- A security-parameter-indexed family of **fixed-width** raw bit-string encodings: +the canonical boundary representation. At parameter `n` every value encodes to exactly +`wid n` bits, and `wid` is polynomially bounded — the formal content of the +Katz–Lindell `1^n` convention. Fixed widths make pairing literal append and let the +split point of any concatenation be recovered positionally, with no alphabets, tags, +or self-delimiting machinery. -/ +structure BitEncFam (α : ℕ → Type u) : Type u where + /-- The exact encoded width at each parameter. -/ + wid : ℕ → ℕ + /-- Polynomial bound on the widths — the `1^n` convention. -/ + widBound : Polynomial ℕ + /-- The widths respect the bound. -/ + wid_le : ∀ n, wid n ≤ widBound.eval n + /-- The raw bit-string encoding at each parameter. -/ + enc : (n : ℕ) → α n → List Bool + /-- Every encoding has exactly the fixed width. -/ + len_eq : ∀ n x, (enc n x).length = wid n + /-- The encoding is injective at each parameter. -/ + enc_injective : ∀ n, Function.Injective (enc n) + +namespace BitEncFam + +variable {α β : ℕ → Type u} + +/-- Forget the fixed width, keeping the polynomial length bound. -/ +def toStrEncFam (e : BitEncFam α) : StrEncFam α where + enc := e.enc + enc_injective := e.enc_injective + bound := e.widBound + len_le n x := (e.len_eq n x).le.trans (e.wid_le n) + +@[simp] theorem toStrEncFam_enc (e : BitEncFam α) : e.toStrEncFam.enc = e.enc := rfl + +@[simp] theorem toStrEncFam_bound (e : BitEncFam α) : e.toStrEncFam.bound = e.widBound := rfl + +/-- The canonical encoding of a constant finite type: the fixed-width binary encoding +of the enumeration index, width `⌈log₂ card γ⌉`. `Unit` gets width `0`, `Bool` width +`1`, `Fin k` width `⌈log₂ k⌉`. -/ +noncomputable def const (γ : Type u) [Fintype γ] : BitEncFam (fun _ => γ) where + wid _ := Nat.clog 2 (Fintype.card γ) + widBound := .C (Nat.clog 2 (Fintype.card γ)) + wid_le _ := by simp + enc _ x := natToBits (Nat.clog 2 (Fintype.card γ)) (Fintype.equivFin γ x) + len_eq _ _ := length_natToBits _ _ + enc_injective n x y h := by + have hlt : ∀ z : γ, ((Fintype.equivFin γ) z : ℕ) < 2 ^ Nat.clog 2 (Fintype.card γ) := + fun z => lt_of_lt_of_le (Fintype.equivFin γ z).isLt (Nat.le_pow_clog one_lt_two _) + exact (Fintype.equivFin γ).injective (Fin.val_injective (natToBits_inj (hlt x) (hlt y) h)) + +/-- The canonical `Unit` boundary: width `0`. -/ +noncomputable abbrev unit : BitEncFam (fun _ => PUnit.{u + 1}) := const PUnit + +/-- The canonical `Bool` boundary: width `1`. -/ +noncomputable abbrev bool : BitEncFam (fun _ => Bool) := const Bool + +/-- The canonical encoding of a `Fin (k n + 1)` family (e.g. a round counter): the +binary index in exactly `k n` bits, using `i ≤ k n < 2 ^ (k n)`. -/ +noncomputable def fin (k : ℕ → ℕ) (p : Polynomial ℕ) (hk : ∀ n, k n ≤ p.eval n) : + BitEncFam (fun n => Fin (k n + 1)) where + wid := k + widBound := p + wid_le := hk + enc n i := natToBits (k n) i + len_eq n i := length_natToBits _ _ + enc_injective n i j h := by + have hlt : ∀ m : Fin (k n + 1), (m : ℕ) < 2 ^ k n := + fun m => lt_of_lt_of_le m.isLt (Nat.succ_le_of_lt Nat.lt_two_pow_self) + exact Fin.val_injective (natToBits_inj (hlt i) (hlt j) h) + +/-- The canonical encoding of a bitvector family: the raw bits, least significant +first, width exactly `w n` — linear, where a unary enumeration would be exponential. -/ +noncomputable def bitVec (w : ℕ → ℕ) (p : Polynomial ℕ) (hw : ∀ n, w n ≤ p.eval n) : + BitEncFam (fun n => BitVec (w n)) where + wid := w + widBound := p + wid_le := hw + enc n v := (List.range (w n)).map v.getLsbD + len_eq n v := by simp + enc_injective n v₁ v₂ h := by + refine BitVec.eq_of_getLsbD_eq_iff.mpr fun i hi => ?_ + exact List.map_inj_left.mp h i (List.mem_range.mpr hi) + +/-- The canonical `BitVec n` boundary. -/ +noncomputable def bitVecX : BitEncFam (fun n => BitVec n) := + bitVec id .X fun n => (Polynomial.eval_X (x := n)).ge + +/-- Pair two fixed-width boundaries by literal append: the widths are fixed, so the +split point is positional and no separator is needed. Widths add. -/ +noncomputable def pair (e₁ : BitEncFam α) (e₂ : BitEncFam β) : BitEncFam (fun n => α n × β n) where + wid n := e₁.wid n + e₂.wid n + widBound := e₁.widBound + e₂.widBound + wid_le n := by + have := e₁.wid_le n; have := e₂.wid_le n + simp only [Polynomial.eval_add]; omega + enc n p := e₁.enc n p.1 ++ e₂.enc n p.2 + len_eq n p := by rw [List.length_append, e₁.len_eq, e₂.len_eq] + enc_injective n p q h := by + obtain ⟨h₁, h₂⟩ := List.append_inj h (by rw [e₁.len_eq, e₁.len_eq]) + exact Prod.ext (e₁.enc_injective n h₁) (e₂.enc_injective n h₂) + +/-- The canonical optional boundary: one tag bit, then the payload (zero-padded for +`none`), width `1 + wid`. This is the shape of a machine's optional readout. -/ +noncomputable def option (e : BitEncFam α) : BitEncFam (fun n => Option (α n)) where + wid n := e.wid n + 1 + widBound := e.widBound + .C 1 + wid_le n := by have := e.wid_le n; simp only [Polynomial.eval_add, Polynomial.eval_C]; omega + enc n + | Option.none => false :: List.replicate (e.wid n) false + | Option.some x => true :: e.enc n x + len_eq n x := by cases x <;> simp [e.len_eq] + enc_injective n x y h := by + cases x <;> cases y <;> simp only [List.cons.injEq] at h + · rfl + · exact absurd h.1 (by simp) + · exact absurd h.1 (by simp) + · exact congrArg _ (e.enc_injective n h.2) + +end BitEncFam + +/-! ## Variable-left, fixed-right pairing -/ + +namespace StrEncFam + +variable {σ β : ℕ → Type u} + +/-- Pair a variable-width encoding with a fixed-width one by append: injective because +the fixed-width right component determines the split point from the right. This is the +input shape of a machine's state/answer update. -/ +noncomputable def pairVar (s : StrEncFam σ) (e : BitEncFam β) : StrEncFam (fun n => σ n × β n) where + enc n p := s.enc n p.1 ++ e.enc n p.2 + enc_injective n p q h := by + obtain ⟨h₁, h₂⟩ := List.append_inj' h (by rw [e.len_eq, e.len_eq]) + exact Prod.ext (s.enc_injective n h₁) (e.enc_injective n h₂) + bound := s.bound + e.widBound + len_le n p := by + rw [List.length_append, e.len_eq] + have := s.len_le n p.1; have := e.wid_le n + simp only [Polynomial.eval_add]; omega + +@[simp] theorem pairVar_enc (s : StrEncFam σ) (e : BitEncFam β) (n : ℕ) (p : σ n × β n) : + (s.pairVar e).enc n p = s.enc n p.1 ++ e.enc n p.2 := rfl + +/-- Tag-bit sum of raw string encodings: `false ::` the left payload, `true ::` the +right payload. The state shape of a two-phase (`⊕`-state) machine. -/ +noncomputable def sum {τ : ℕ → Type u} (s₁ : StrEncFam σ) (s₂ : StrEncFam τ) : + StrEncFam (fun n => σ n ⊕ τ n) where + enc n := Sum.elim (fun x => false :: s₁.enc n x) (fun y => true :: s₂.enc n y) + enc_injective n x y h := by + cases x <;> cases y <;> simp only [Sum.elim_inl, Sum.elim_inr, List.cons.injEq] at h + · exact congrArg Sum.inl (s₁.enc_injective n h.2) + · exact absurd h.1 (by simp) + · exact absurd h.1 (by simp) + · exact congrArg Sum.inr (s₂.enc_injective n h.2) + bound := s₁.bound + s₂.bound + .C 1 + len_le n x := by + cases x with + | inl x => + have := s₁.len_le n x + simp only [Sum.elim_inl, List.length_cons, Polynomial.eval_add, Polynomial.eval_C] + omega + | inr y => + have := s₂.len_le n y + simp only [Sum.elim_inr, List.length_cons, Polynomial.eval_add, Polynomial.eval_C] + omega + +@[simp] theorem sum_enc_inl {τ : ℕ → Type u} (s₁ : StrEncFam σ) (s₂ : StrEncFam τ) + (n : ℕ) (x : σ n) : (s₁.sum s₂).enc n (Sum.inl x) = false :: s₁.enc n x := rfl + +@[simp] theorem sum_enc_inr {τ : ℕ → Type u} (s₁ : StrEncFam σ) (s₂ : StrEncFam τ) + (n : ℕ) (y : τ n) : (s₁.sum s₂).enc n (Sum.inr y) = true :: s₂.enc n y := rfl + +end StrEncFam + +namespace BitEncFam + +variable {γ : ℕ → Type u} {σ : ℕ → Type u} + +/-- Pair a fixed-width encoding on the left with a variable-width one on the right by +append — the mirror of `StrEncFam.pairVar`. Injective because the fixed-width left +component determines the split point from the left. This is the state shape of a +machine carrying a fixed-width value alongside a running machine's state. -/ +noncomputable def pairFix (e : BitEncFam γ) (s : StrEncFam σ) : + StrEncFam (fun n => γ n × σ n) where + enc n p := e.enc n p.1 ++ s.enc n p.2 + enc_injective n p q h := by + obtain ⟨h₁, h₂⟩ := List.append_inj h (by rw [e.len_eq, e.len_eq]) + exact Prod.ext (e.enc_injective n h₁) (s.enc_injective n h₂) + bound := e.widBound + s.bound + len_le n p := by + rw [List.length_append, e.len_eq] + have := s.len_le n p.2; have := e.wid_le n + simp only [Polynomial.eval_add]; omega + +@[simp] theorem pairFix_enc (e : BitEncFam γ) (s : StrEncFam σ) (n : ℕ) (p : γ n × σ n) : + (e.pairFix s).enc n p = e.enc n p.1 ++ s.enc n p.2 := rfl + +/-- The all-zero padding block of a prescribed fixed width: a `PUnit` boundary whose +encoding is `wid n` zero bits — the `none`-payload shape of `BitEncFam.option`. -/ +noncomputable def pad (w : ℕ → ℕ) (p : Polynomial ℕ) (hw : ∀ n, w n ≤ p.eval n) : + BitEncFam (fun _ => PUnit.{u + 1}) where + wid := w + widBound := p + wid_le := hw + enc n _ := List.replicate (w n) false + len_eq n _ := List.length_replicate + enc_injective _ x y _ := by cases x; cases y; rfl + +@[simp] theorem pad_enc (w : ℕ → ℕ) (p : Polynomial ℕ) (hw : ∀ n, w n ≤ p.eval n) + (n : ℕ) (x : PUnit) : (pad w p hw).enc n x = List.replicate (w n) false := rfl + +end BitEncFam + +/-! ## Uniform polynomial-time machine families -/ + +/-- A family of encoded polynomial-time machine witnesses with **uniform** polynomial +bounds: one machine per security parameter computing `f n` relative to the given +string encodings, a single polynomial bounding all running times (in `n` plus the +input length), and a single polynomial bounding all description sizes (the advice +bound — without it, per-parameter table machines smuggle unbounded advice). This is +the reusable unit of the polynomial-time adversary model: base machines produce these, +combinators compose them, and an adversary's four step functions each carry one. + +Like `EncPolyTime`, the structure imposes nothing on the encodings themselves; its +certifying power comes from the call site pinning the injective families +(`ToCslib.Computability.BitEncFam`, `ToCslib.Computability.StrEncFam`). -/ +structure EncPolyTimeFam {α β : ℕ → Type u} + (ea : (n : ℕ) → α n → List Bool) (eb : (n : ℕ) → β n → List Bool) + (f : (n : ℕ) → α n → β n) : Type (u + 1) where + /-- The machine witness at each parameter. -/ + wit : (n : ℕ) → EncPolyTime (ea n) (eb n) (f n) + /-- Uniform polynomial bound on running times, in `n` plus the input length. -/ + time : Polynomial ℕ + /-- Every witness runs within the uniform time bound. -/ + time_le : ∀ n k, ((wit n).time).eval k ≤ time.eval (n + k) + /-- Uniform polynomial bound on description sizes — the advice bound. -/ + size : Polynomial ℕ + /-- Every witness's machine description is within the advice bound. -/ + size_le : ∀ n, (wit n).size ≤ size.eval n + +namespace EncPolyTimeFam + +variable {α β γ : ℕ → Type u} + {ea : (n : ℕ) → α n → List Bool} {eb : (n : ℕ) → β n → List Bool} + {ec : (n : ℕ) → γ n → List Bool} + +/-- Transport a witness family along string-equal encodings on both sides: the machines, +time polynomial, and advice bound are untouched (`EncPolyTime.recode` per parameter). +The workhorse for pure re-bracketings of encoded data — `cons`/append associativity and +pair/sum reshuffles cost no machine content. -/ +def recode {α' β' : ℕ → Type u} {ea' : (n : ℕ) → α' n → List Bool} + {eb' : (n : ℕ) → β' n → List Bool} {f : (n : ℕ) → α n → β n} + (h : EncPolyTimeFam ea eb f) (φ : (n : ℕ) → α' n → α n) (g : (n : ℕ) → α' n → β' n) + (hin : ∀ n x, ea' n x = ea n (φ n x)) + (hout : ∀ n x, eb' n (g n x) = eb n (f n (φ n x))) : + EncPolyTimeFam ea' eb' g where + wit n := (h.wit n).recode (φ n) (g n) (hin n) (hout n) + time := h.time + time_le := h.time_le + size := h.size + size_le := h.size_le + +/-- The identity family: one state, unit time. -/ +noncomputable def id (ea : (n : ℕ) → α n → List Bool) : + EncPolyTimeFam ea ea (fun _ => _root_.id) where + wit n := .id (ea n) + time := .C 1 + time_le n k := by + simp only [EncPolyTime.time, EncPolyTime.id, PolyTimeComputable.id, Polynomial.eval_one, + Polynomial.eval_C] + exact le_rfl + size := .C 1 + size_le n := by simp + +/-- Transport a family along pointwise-equal functions. -/ +def copy {f : (n : ℕ) → α n → β n} (h : EncPolyTimeFam ea eb f) + (f' : (n : ℕ) → α n → β n) (hf : ∀ n x, f n x = f' n x) : + EncPolyTimeFam ea eb f' where + wit n := (h.wit n).copy (f' n) (hf n) + time := h.time + time_le n k := by simpa [EncPolyTime.copy, EncPolyTime.time] using h.time_le n k + size := h.size + size_le n := by simpa using h.size_le n + +/-- Composition of uniform families: witnesses compose by `EncPolyTime.comp`; the +uniform time bound composes through the output-length envelope, and description +sizes add. + +The composed time bound substitutes one polynomial into another, so degrees multiply: +a fixed number of `comp`s stays polynomial, but iterating to a depth that grows with +`n` does not. Polynomial-length runs account time additively per step instead +(a total-time accounting theorem); only description size composes additively. -/ +noncomputable def comp {f : (n : ℕ) → α n → β n} {g : (n : ℕ) → β n → γ n} + (h : EncPolyTimeFam ea eb f) (h' : EncPolyTimeFam eb ec g) : + EncPolyTimeFam ea ec (fun n => g n ∘ f n) where + wit n := (h.wit n).comp (h'.wit n) + time := h.time + h'.time.comp (.C 1 + .X + h.time) + time_le n k := by + rw [EncPolyTime.comp_time_eval] + have h1 : ((h.wit n).time).eval k ≤ h.time.eval (n + k) := h.time_le n k + have h2 : ((h'.wit n).time).eval (1 + k + ((h.wit n).time).eval k) ≤ + h'.time.eval (n + (1 + k + ((h.wit n).time).eval k)) := h'.time_le n _ + have h3 : h'.time.eval (n + (1 + k + ((h.wit n).time).eval k)) ≤ + h'.time.eval (1 + (n + k) + h.time.eval (n + k)) := + Polynomial.eval_le_eval (by omega) + simp only [Polynomial.eval_add, Polynomial.eval_comp, Polynomial.eval_X, + Polynomial.eval_C] + omega + size := h.size + h'.size + size_le n := by + rw [EncPolyTime.size_comp] + have := h.size_le n; have := h'.size_le n + simp only [Polynomial.eval_add]; omega + +/-- The constant family, from a length bound on the encoded constants: the machine +erases its input and writes the constant. -/ +noncomputable def const (ea : (n : ℕ) → α n → List Bool) {eb : (n : ℕ) → β n → List Bool} + (c : (n : ℕ) → β n) (B : Polynomial ℕ) (hB : ∀ n, (eb n (c n)).length ≤ B.eval n) : + EncPolyTimeFam ea eb (fun n _ => c n) where + wit n := .const (ea n) (eb n) (c n) + time := .X + B + .C 2 + time_le n k := by + have hlen := hB n + have hmono : B.eval n ≤ B.eval (n + k) := Polynomial.eval_le_eval (Nat.le_add_right n k) + change ((constPolyTimeComputable (eb n (c n))).poly).eval k ≤ _ + simp only [constPolyTimeComputable, Polynomial.eval_add, Polynomial.eval_X, + Polynomial.eval_C] + omega + size := B + .C 2 + size_le n := by + refine (EncPolyTime.size_const_le _ _ _).trans ?_ + have := hB n + simp only [Polynomial.eval_add, Polynomial.eval_C]; omega + +/-- The finite-table family, for input families of polynomially bounded cardinality +and encoding length: any function family is computable by lookup tables, within the +advice bound exactly when the domain stays polynomially small. -/ +noncomputable def ofFintype [∀ n, Fintype (α n)] {ea : (n : ℕ) → α n → List Bool} + (hea : ∀ n, Function.Injective (ea n)) {eb : (n : ℕ) → β n → List Bool} + (f : (n : ℕ) → α n → β n) + (cardIn : Polynomial ℕ) (hcard : ∀ n, Fintype.card (α n) ≤ cardIn.eval n) + (lenIn : Polynomial ℕ) (hlenIn : ∀ n x, (ea n x).length ≤ lenIn.eval n) + (lenOut : Polynomial ℕ) (hlenOut : ∀ n x, (eb n (f n x)).length ≤ lenOut.eval n) : + EncPolyTimeFam ea eb f where + wit n := .ofFintype (ea n) (hea n) (eb n) (f n) + time := .X + lenOut + .C 1 + time_le n k := by + refine (EncPolyTime.time_ofFintype_eval_le (hea n) (hlenOut n) k).trans ?_ + have : lenOut.eval n ≤ lenOut.eval (n + k) := Polynomial.eval_le_eval (Nat.le_add_right n k) + simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C]; omega + size := cardIn * (lenIn + .C 1 + lenOut) + .C 1 + size_le n := by + refine (EncPolyTime.size_ofFintype_le_of_bounds (hea n) (hcard n) (hlenIn n) + (hlenOut n)).trans ?_ + simp only [Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_C] + exact le_rfl + +end EncPolyTimeFam + +end ToCslib.Computability diff --git a/ToCslib/Computability/PolyTime.lean b/ToCslib/Computability/PolyTime.lean new file mode 100644 index 0000000..cda6e42 --- /dev/null +++ b/ToCslib/Computability/PolyTime.lean @@ -0,0 +1,214 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ +module + +public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic +public import Mathlib.Algebra.Polynomial.Eval.Degree + +/-! +# Encoded Polynomial-Time Computability + +Cslib's `Cslib.Turing.SingleTapeTM.PolyTimeComputable` certifies polynomial-time computability +of raw string functions `List Symbol → List Symbol`. This file adds the encoding layer: +`ToCslib.Computability.EncPolyTime ea eb f` witnesses that a function `f : α → β` between +arbitrary types is polynomial-time computable relative to `Bool`-string encodings +`ea : α → List Bool` and `eb : β → List Bool`, by bundling a machine-computed total +string function that intertwines the encodings. The encodings are supplied by call +sites; the adversary model pins the injective fixed-width and length-bounded families +of `ToCslib.Computability.BitEncoding` (`ToCslib.Computability.BitEncFam`, +`ToCslib.Computability.StrEncFam`) at its boundaries. + +Identity and composition (`EncPolyTime.id`, `EncPolyTime.comp`) lift directly from +Cslib's proven `PolyTimeComputable.id` and `PolyTimeComputable.comp`; the monotone +time-bound side condition of the latter is discharged by `PolyTimeComputable.normalize`, +which replaces a machine's time bound with its own polynomial. + +Besides the running time `EncPolyTime.time`, every witness has a **description size** +`EncPolyTime.size`: the state count of its machine. Cslib's `PolyTimeComputable` bounds +only the running time, which suffices for a *single* function but not for a *family* of +witnesses indexed by a security parameter: a finite-table machine looks up any function +in linear time using one state per valid input, so without a size bound a family of +witnesses smuggles unbounded advice and the induced "polynomial-time" class contains +every function on polynomially-encodable domains. Families must therefore bound +`size` polynomially as well (see a uniform description bound), giving the standard +non-uniform P/poly model. +-/ + +@[expose] public section + +universe u v w u' v' + +/-- Evaluation of a natural-number polynomial is monotone in the argument. -/ +theorem Polynomial.eval_le_eval {p : Polynomial ℕ} {m n : ℕ} (h : m ≤ n) : + p.eval m ≤ p.eval n := by + rw [p.eval_eq_sum_range, p.eval_eq_sum_range] + exact Finset.sum_le_sum fun i _ => Nat.mul_le_mul_left _ (Nat.pow_le_pow_left h i) + +namespace Cslib.Turing.SingleTapeTM + +variable {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] + +/-- Replace the time bound of a polynomial-time machine by the evaluation of its own +polynomial. The resulting bound is monotone, as required by `PolyTimeComputable.comp` +for the second machine. -/ +def PolyTimeComputable.normalize {f : List Symbol → List Symbol} + (h : PolyTimeComputable f) : PolyTimeComputable f where + tm := h.tm + timeBound n := h.poly.eval n + outputsFunInTime a := (h.outputsFunInTime a).of_le (h.bounds _) + poly := h.poly + bounds _ := le_rfl + +theorem PolyTimeComputable.monotone_normalize_timeBound {f : List Symbol → List Symbol} + (h : PolyTimeComputable f) : Monotone h.normalize.timeBound := + fun _ _ hmn => Polynomial.eval_le_eval hmn + +/-- The description size of a machine witness over the two-symbol tape alphabet: its +number of states. Over the fixed `Bool` alphabet the transition table has exactly three +rows per state, so the state count measures the machine's description up to a constant +factor — the "advice" of a non-uniform family, and the quantity the machine-counting +bound `B` counts. Time bounds alone do not control it: a table machine looks up any +function on a finite domain in linear time using one state per valid input. + +Deliberately restricted to `Symbol := Bool`: over a family of growing alphabets the +transition table has `Fintype.card Symbol + 1` rows per state, so a bare state count +would undercount the description (a one-state machine over an alphabet of size `2 ^ n` +hides `2 ^ n` advice bits in its transition row). -/ +def PolyTimeComputable.size {f : List Bool → List Bool} + (h : PolyTimeComputable f) : ℕ := Fintype.card h.tm.State + +@[simp] theorem PolyTimeComputable.size_normalize {f : List Bool → List Bool} + (h : PolyTimeComputable f) : h.normalize.size = h.size := rfl + +end Cslib.Turing.SingleTapeTM + +namespace ToCslib.Computability + +open Cslib.Turing.SingleTapeTM + +variable {α : Type u} {β : Type v} {γ : Type w} + +/-- A witness that `f : α → β` is polynomial-time computable relative to `Bool`-string +encodings of its domain and codomain: a total string function, computed by a single-tape +machine in polynomial time, that maps the encoding of `a` to the encoding of `f a`. + +The string function is total: its behavior on strings outside the range of `ea` is +unconstrained. The structure imposes nothing on `ea` and `eb` themselves — with a +non-injective codomain encoding it is trivially inhabited — so its certifying power +comes from the call site pinning injective encoding families +(`ToCslib.Computability.BitEncFam`, `ToCslib.Computability.StrEncFam`). -/ +structure EncPolyTime (ea : α → List Bool) (eb : β → List Bool) (f : α → β) where + /-- The total string function the machine computes. -/ + toFun : List Bool → List Bool + /-- The machine computing `toFun`, with its polynomial time bound. -/ + polyTime : PolyTimeComputable toFun + /-- The string function intertwines the encodings. -/ + map_encode : ∀ a, toFun (ea a) = eb (f a) + +namespace EncPolyTime + +variable {ea : α → List Bool} {eb : β → List Bool} {ec : γ → List Bool} + +/-- The polynomial time bound of the underlying machine. -/ +def time {f : α → β} (h : EncPolyTime ea eb f) : Polynomial ℕ := h.polyTime.poly + +/-- The description size (machine state count) of the underlying machine. Families of +witnesses indexed by a security parameter must bound this polynomially — the advice +bound of the non-uniform P/poly model; see the module docstring. -/ +def size {f : α → β} (h : EncPolyTime ea eb f) : ℕ := h.polyTime.size + +/-- The identity function is polynomial-time computable relative to any encoding. -/ +noncomputable def id (ea : α → List Bool) : EncPolyTime ea ea _root_.id where + toFun := _root_.id + polyTime := PolyTimeComputable.id + map_encode _ := rfl + +/-- The identity witness has a single machine state. -/ +@[simp] theorem size_id (ea : α → List Bool) : (EncPolyTime.id ea).size = 1 := + Fintype.card_punit + +/-- Transport a witness along a pointwise-equal function. -/ +def copy {f : α → β} (h : EncPolyTime ea eb f) (f' : α → β) (hf : ∀ a, f a = f' a) : + EncPolyTime ea eb f' where + toFun := h.toFun + polyTime := h.polyTime + map_encode a := (h.map_encode a).trans (congrArg eb (hf a)) + +/-- Transporting along a pointwise-equal function preserves the machine, hence the size. -/ +@[simp] theorem size_copy {f : α → β} (h : EncPolyTime ea eb f) (f' : α → β) + (hf : ∀ a, f a = f' a) : (h.copy f' hf).size = h.size := rfl + +/-- Transport a witness along string-equal encodings on both sides: if `ea'` encodes +each `a'` exactly as `ea` encodes `φ a'`, and `eb'` encodes each `g a'` exactly as `eb` +encodes `f (φ a')`, the same machine witnesses `g` relative to `ea'`/`eb'`. The machine, +time, and size are untouched — this discharges pure re-bracketings and re-taggings of +encoded data (`cons`/append associativity, pair/sum reshuffles) with no machine content. -/ +def recode {α' : Type u'} {β' : Type v'} {ea' : α' → List Bool} {eb' : β' → List Bool} + {f : α → β} (h : EncPolyTime ea eb f) (φ : α' → α) (g : α' → β') + (hin : ∀ a', ea' a' = ea (φ a')) (hout : ∀ a', eb' (g a') = eb (f (φ a'))) : + EncPolyTime ea' eb' g where + toFun := h.toFun + polyTime := h.polyTime + map_encode a' := by rw [hin, h.map_encode, ← hout] + +/-- Recoding preserves the machine's time polynomial. -/ +@[simp] theorem time_recode {α' : Type u'} {β' : Type v'} {ea' : α' → List Bool} + {eb' : β' → List Bool} {f : α → β} (h : EncPolyTime ea eb f) (φ : α' → α) (g : α' → β') + (hin : ∀ a', ea' a' = ea (φ a')) (hout : ∀ a', eb' (g a') = eb (f (φ a'))) : + (h.recode φ g hin hout).time = h.time := rfl + +/-- Recoding preserves the machine, hence the description size. -/ +@[simp] theorem size_recode {α' : Type u'} {β' : Type v'} {ea' : α' → List Bool} + {eb' : β' → List Bool} {f : α → β} (h : EncPolyTime ea eb f) (φ : α' → α) (g : α' → β') + (hin : ∀ a', ea' a' = ea (φ a')) (hout : ∀ a', eb' (g a') = eb (f (φ a'))) : + (h.recode φ g hin hout).size = h.size := rfl + +/-- Composition of encoded polynomial-time witnesses, from Cslib's +`PolyTimeComputable.comp`. + +Time bounds compose by substitution (`comp_time`), so degrees multiply: iterating +`comp` to polynomial depth does not stay polynomial-time, and polynomial-length runs +must instead account time additively per step (as a total-time accounting theorem +does). Only the description size composes additively (`size_comp`). -/ +noncomputable def comp {f : α → β} {f' : β → γ} + (h : EncPolyTime ea eb f) (h' : EncPolyTime eb ec f') : + EncPolyTime ea ec (f' ∘ f) where + toFun := h'.toFun ∘ h.toFun + polyTime := h.polyTime.comp h'.polyTime.normalize h'.polyTime.monotone_normalize_timeBound + map_encode a := by + simp only [Function.comp_apply, h.map_encode, h'.map_encode] + +/-- The polynomial time bound of a composition, unfolded: the first machine's polynomial plus +the second's evaluated at the first's output-length envelope `1 + X + h.time`. -/ +theorem comp_time {f : α → β} {f' : β → γ} + (h : EncPolyTime ea eb f) (h' : EncPolyTime eb ec f') : + (h.comp h').time = h.time + h'.time.comp (1 + Polynomial.X + h.time) := rfl + +/-- Evaluation of the composed time bound: `h`'s cost at input length `k`, plus `h'`'s cost at the +length `h`'s output can reach (`1 + k + h.time.eval k`). -/ +theorem comp_time_eval {f : α → β} {f' : β → γ} + (h : EncPolyTime ea eb f) (h' : EncPolyTime eb ec f') (k : ℕ) : + (h.comp h').time.eval k = h.time.eval k + h'.time.eval (1 + k + h.time.eval k) := by + rw [comp_time]; simp [Polynomial.eval_comp] + +/-- The composed machine is Cslib's phase-sum `compComputer`, so description sizes add. -/ +theorem size_comp {f : α → β} {f' : β → γ} + (h : EncPolyTime ea eb f) (h' : EncPolyTime eb ec f') : + (h.comp h').size = h.size + h'.size := + Fintype.card_sum + +/-- The output encoding of a polynomial-time computable function is at most polynomially +longer than the input encoding, by `output_length_le_input_length_add_time`. -/ +theorem length_le {f : α → β} (h : EncPolyTime ea eb f) (a : α) : + (eb (f a)).length ≤ max 1 (ea a).length + h.time.eval (ea a).length := by + rw [← h.map_encode a] + refine le_trans (output_length_le_input_length_add_time h.polyTime.tm _ _ _ + (h.polyTime.outputsFunInTime (ea a))) ?_ + exact Nat.add_le_add_left (h.polyTime.bounds _) _ + +end EncPolyTime + +end ToCslib.Computability diff --git a/ToCslib/Computability/SingleTape/BasicMachines.lean b/ToCslib/Computability/SingleTape/BasicMachines.lean new file mode 100644 index 0000000..4ac0737 --- /dev/null +++ b/ToCslib/Computability/SingleTape/BasicMachines.lean @@ -0,0 +1,525 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ +module + +public import ToCslib.Computability.PolyTime + +/-! +# Base Polynomial-Time Machines + +Concrete single-tape machines witnessing polynomial-time computability of basic +functions, in Cslib's `Cslib.Turing.SingleTapeTM` model: + +- `Cslib.Turing.SingleTapeTM.clearComputer` / `Cslib.Turing.SingleTapeTM.constComputer`: erase the + input and produce a fixed output string, giving `constPolyTimeComputable` and the + encoding-level witness `ToCslib.Computability.EncPolyTime.const` for constant functions. +- `Cslib.Turing.SingleTapeTM.tableComputer`: read the input into machine state through the + prefix tree of a finite set of valid inputs, then write the corresponding table + output, giving `tablePolyTimeComputable` and the encoding-level witness + `ToCslib.Computability.EncPolyTime.ofFintype`: **any function with a finite domain is + polynomial-time computable** relative to an injective encoding — but with a + description size (`EncPolyTime.size_ofFintype_le`) that grows with the domain's + total encoded length, so a *family* of tables stays within a polynomial advice + bound (a uniform description bound) only on domains of polynomially bounded + cardinality. Within that regime it subsumes constants, relabelings, and projections, + and discharges all four per-step machine witnesses for + small-state oracle machines. + +The machines follow one design: **clear the input moving right, then write the output +backwards moving left**. Clearing onto an empty left stack keeps the tape in canonical +form (`StackTape` normalizes blanks), and writing the output back-to-front while moving +left lands the head on its first symbol, which is exactly the halting configuration +`BiTape.mk₁` — no rewind phases are needed. + +Base machines for *unbounded* domains (symbol relabeling, projections with respect to +paired encodings of infinite types) would follow the same skeleton and remain future +work; together with `EncPolyTime.comp` (from Cslib's proven machine composition) they +would extend the generic witnesses beyond finite domains, stated in the raw-encoding +family form (`ToCslib.Computability.EncPolyTimeFam`) used by backend adapters. +-/ + +@[expose] public section + +universe u v + +namespace Cslib.Turing.SingleTapeTM + +open Relation + +variable {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] + +/-! ## The machines -/ + +/-- Erase the input moving right, then halt: computes the constant `[]`. -/ +def clearComputer : SingleTapeTM Symbol where + State := Unit + q₀ := () + tr _ h := match h with + | some _ => ⟨⟨none, some .right⟩, some ()⟩ + | none => ⟨⟨none, none⟩, none⟩ + +/-- Erase the input moving right, then write `o :: os` backwards moving left: computes +the constant `o :: os`. State `.inl ()` is the clearing phase; state `.inr i` writes +symbol `i` of the output next. -/ +def constComputer (o : Symbol) (os : List Symbol) : SingleTapeTM Symbol where + State := Unit ⊕ Fin (o :: os).length + q₀ := .inl () + tr q h := match q with + | .inl () => match h with + | some _ => ⟨⟨none, some .right⟩, some (.inl ())⟩ + | none => ⟨⟨none, none⟩, some (.inr ⟨os.length, by simp⟩)⟩ + | .inr i => ⟨⟨some (o :: os)[i], if i.val = 0 then none else some .left⟩, + if i.val = 0 then none else some (.inr ⟨i.val - 1, by omega⟩)⟩ + +/-! ## Clearing-phase verification -/ + +omit [Inhabited Symbol] [Fintype Symbol] in +private lemma bitape_head_tail_eq_mk₁ (t : List Symbol) : + (⟨(StackTape.mapSome t).head, ∅, (StackTape.mapSome t).tail⟩ : BiTape Symbol) = + .mk₁ t := by + cases t with + | nil => rfl + | cons a as => rfl + +private lemma clearComputer_clear_steps (l : List Symbol) : + RelatesInSteps (clearComputer (Symbol := Symbol)).TransitionRelation + ⟨some (), .mk₁ l⟩ ⟨some (), .nil⟩ l.length := by + induction l with + | nil => exact .refl _ + | cons c t ih => + refine .head _ ⟨some (), .mk₁ t⟩ _ _ ?_ ih + change (clearComputer (Symbol := Symbol)).step ⟨some (), .mk₁ (c :: t)⟩ = _ + rw [← bitape_head_tail_eq_mk₁ t] + rfl + +private lemma constComputer_clear_steps (o : Symbol) (os l : List Symbol) : + RelatesInSteps (constComputer o os).TransitionRelation + ⟨some (.inl ()), .mk₁ l⟩ ⟨some (.inl ()), .nil⟩ l.length := by + induction l with + | nil => exact .refl _ + | cons c t ih => + refine .head _ ⟨some (.inl ()), .mk₁ t⟩ _ _ ?_ ih + change (constComputer o os).step ⟨some (.inl ()), .mk₁ (c :: t)⟩ = _ + rw [← bitape_head_tail_eq_mk₁ t] + rfl + +/-! ## Writing-phase verification -/ + +private lemma constComputer_enter_step (o : Symbol) (os : List Symbol) : + (constComputer o os).TransitionRelation ⟨some (.inl ()), .nil⟩ + ⟨some (.inr ⟨os.length, by simp⟩), + ⟨none, ∅, .mapSome ((o :: os).drop (os.length + 1))⟩⟩ := by + change (constComputer o os).step _ = _ + rw [show (o :: os).drop (os.length + 1) = [] by simp] + rfl + +private lemma constComputer_write_steps (o : Symbol) (os : List Symbol) (i : ℕ) : + ∀ (hi : i < (o :: os).length), + RelatesInSteps (constComputer o os).TransitionRelation + ⟨some (.inr ⟨i, hi⟩), ⟨none, ∅, .mapSome ((o :: os).drop (i + 1))⟩⟩ + ⟨none, .mk₁ (o :: os)⟩ (i + 1) := by + induction i with + | zero => + intro hi + refine .single ?_ + change (constComputer o os).step _ = _ + rfl + | succ i ih => + intro hi + refine .head _ ⟨some (.inr ⟨i, by omega⟩), + ⟨none, ∅, .mapSome ((o :: os).drop (i + 1))⟩⟩ _ _ ?_ (ih (by omega)) + change (constComputer o os).step _ = _ + rw [List.drop_eq_getElem_cons hi] + rfl + +/-! ## Assembly -/ + +/-- Constant functions are machine-computable in linear time. -/ +def constTimeComputable : (out : List Symbol) → + TimeComputable (Symbol := Symbol) (fun _ => out) + | [] => + { tm := clearComputer + timeBound := fun n => n + 1 + outputsFunInTime := fun l => by + refine ⟨l.length + 1, le_rfl, ?_⟩ + exact RelatesInSteps.tail + (r := (clearComputer (Symbol := Symbol)).TransitionRelation) + ⟨some (), .mk₁ l⟩ ⟨some (), .nil⟩ ⟨none, .mk₁ []⟩ _ + (clearComputer_clear_steps l) rfl } + | o :: os => + { tm := constComputer o os + timeBound := fun n => n + (os.length + 2) + outputsFunInTime := fun l => by + refine ⟨l.length + (1 + (os.length + 1)), by omega, ?_⟩ + exact (constComputer_clear_steps o os l).trans + ((RelatesInSteps.single (constComputer_enter_step o os)).trans + (constComputer_write_steps o os os.length (by simp))) } + +/-- Constant functions are machine-computable in polynomial time. -/ +noncomputable def constPolyTimeComputable (out : List Symbol) : + PolyTimeComputable (Symbol := Symbol) (fun _ => out) where + toTimeComputable := constTimeComputable out + poly := .X + .C (out.length + 2) + bounds n := by + cases out with + | nil => + simp only [constTimeComputable, Polynomial.eval_add, Polynomial.eval_X, + Polynomial.eval_C, List.length_nil] + omega + | cons o os => + simp only [constTimeComputable, Polynomial.eval_add, Polynomial.eval_X, + Polynomial.eval_C, List.length_cons] + omega + +/-- The constant-function machine has at most `out.length + 2` states: one clearing +state plus one writing state per output symbol. Stated over `Bool`, the alphabet +`PolyTimeComputable.size` is defined at. -/ +theorem size_constPolyTimeComputable_le (out : List Bool) : + (constPolyTimeComputable out).size ≤ out.length + 2 := by + cases out with + | nil => + change Fintype.card Unit ≤ 2 + simp + | cons o os => + change Fintype.card (Unit ⊕ Fin (o :: os).length) ≤ (o :: os).length + 2 + simp only [Fintype.card_sum, Fintype.card_unit, Fintype.card_fin, List.length_cons] + omega + +/-! ## The finite-table machine + +A machine computing `fun l => if l ∈ S then T l else []` for a *finite* set `S` of +valid inputs: read the input into machine state through the prefix tree of `S` +(clearing as it goes), then on the blank look up the table and write the output +backwards moving left exactly as `constComputer` does. Inputs that stop matching any +prefix of `S` fall into an absorbing junk state and clear to a blank tape. -/ + +section Table + +variable [DecidableEq Symbol] + +omit [Inhabited Symbol] [Fintype Symbol] [DecidableEq Symbol] in +private lemma bitape_mk₁_eq_of_length_pos {t : List Symbol} (h : 0 < t.length) : + (BiTape.mk₁ t : BiTape Symbol) = ⟨some t[0], ∅, .mapSome (t.drop 1)⟩ := by + cases t with + | nil => simp at h + | cons a as => rfl + +omit [Inhabited Symbol] [Fintype Symbol] in +/-- All prefixes of members of `S`: the reading states of `tableComputer`. -/ +def prefixClosure (S : Finset (List Symbol)) : Finset (List Symbol) := + S.biUnion fun s => s.inits.toFinset + +omit [Inhabited Symbol] [Fintype Symbol] in +theorem mem_prefixClosure {S : Finset (List Symbol)} {l : List Symbol} : + l ∈ prefixClosure S ↔ ∃ s ∈ S, l <+: s := by + simp [prefixClosure, List.mem_inits] + +omit [Inhabited Symbol] [Fintype Symbol] in +theorem subset_prefixClosure (S : Finset (List Symbol)) : S ⊆ prefixClosure S := + fun s hs => mem_prefixClosure.mpr ⟨s, hs, List.prefix_refl s⟩ + +omit [Inhabited Symbol] [Fintype Symbol] in +/-- Path independence of falling out of the prefix tree: once the consumed prefix +matches no member of `S`, no extension does either. -/ +theorem append_not_mem_prefixClosure {S : Finset (List Symbol)} {l : List Symbol} + (h : l ∉ prefixClosure S) (b : Symbol) : l ++ [b] ∉ prefixClosure S := by + intro hmem + obtain ⟨s, hs, hpre⟩ := mem_prefixClosure.mp hmem + exact h (mem_prefixClosure.mpr ⟨s, hs, (List.prefix_append l [b]).trans hpre⟩) + +omit [Inhabited Symbol] [Fintype Symbol] in +/-- States of the finite-table machine: reading (tracking the consumed prefix through +the prefix tree of `S`), junk (clearing an unmatched input), or writing symbol `i` of +the table output of `s`. -/ +abbrev TableState (S : Finset (List Symbol)) (T : List Symbol → List Symbol) : Type := + ({l // l ∈ prefixClosure S} ⊕ Unit) ⊕ (Σ s : {s // s ∈ S}, Fin (T s.1).length) + +omit [Inhabited Symbol] [Fintype Symbol] in +/-- The state after consuming the prefix `l`: still reading if `l` can extend to a +member of `S`, junk otherwise. Totality in `l` makes the reading-step lemma uniform +(via `append_not_mem_prefixClosure`). -/ +def readState (S : Finset (List Symbol)) (T : List Symbol → List Symbol) + (l : List Symbol) : TableState S T := + if h : l ∈ prefixClosure S then .inl (.inl ⟨l, h⟩) else .inl (.inr ()) + +omit [Inhabited Symbol] [Fintype Symbol] in +/-- The state entered on reaching the blank at the end of the input with consumed +prefix `l`: write the table output backwards if `l ∈ S` and the output is nonempty, +otherwise halt (the tape is already the blank output). -/ +def enterState (S : Finset (List Symbol)) (T : List Symbol → List Symbol) + (l : List Symbol) : Option (TableState S T) := + if hS : l ∈ S then + if hT : (T l).length = 0 then none + else some (.inr ⟨⟨l, hS⟩, + ⟨(T l).length - 1, by change (T l).length - 1 < (T l).length; omega⟩⟩) + else none + +/-- The finite-table machine: clear the input moving right while tracking the consumed +prefix through the prefix tree of `S`; on the blank, look up the table and write the +output backwards moving left. Computes `fun l => if l ∈ S then T l else []`. -/ +def tableComputer (S : Finset (List Symbol)) (T : List Symbol → List Symbol) : + SingleTapeTM Symbol where + State := TableState S T + q₀ := readState S T [] + tr q h := match q with + | .inl (.inl ⟨l, _⟩) => match h with + | some b => ⟨⟨none, some .right⟩, some (readState S T (l ++ [b]))⟩ + | none => ⟨⟨none, none⟩, enterState S T l⟩ + | .inl (.inr ()) => match h with + | some _ => ⟨⟨none, some .right⟩, some (.inl (.inr ()))⟩ + | none => ⟨⟨none, none⟩, none⟩ + | .inr ⟨s, i⟩ => ⟨⟨some (T s.1)[i], if i.val = 0 then none else some .left⟩, + if i.val = 0 then none else some (.inr ⟨s, ⟨i.val - 1, by omega⟩⟩)⟩ + +/-! ### Reading-phase verification -/ + +private lemma tableComputer_read_step (S : Finset (List Symbol)) + (T : List Symbol → List Symbol) (l : List Symbol) (b : Symbol) (t : List Symbol) : + (tableComputer S T).TransitionRelation + ⟨some (readState S T l), .mk₁ (b :: t)⟩ + ⟨some (readState S T (l ++ [b])), .mk₁ t⟩ := by + change (tableComputer S T).step _ = _ + rw [← bitape_head_tail_eq_mk₁ t] + by_cases h : l ∈ prefixClosure S + · simp only [readState] + rw [dif_pos h] + rfl + · simp only [readState] + rw [dif_neg h, dif_neg (append_not_mem_prefixClosure h b)] + rfl + +private lemma tableComputer_read_steps (S : Finset (List Symbol)) + (T : List Symbol → List Symbol) (t l : List Symbol) : + RelatesInSteps (tableComputer S T).TransitionRelation + ⟨some (readState S T l), .mk₁ t⟩ ⟨some (readState S T (l ++ t)), .nil⟩ + t.length := by + induction t generalizing l with + | nil => rw [List.append_nil]; exact .refl _ + | cons b t ih => + refine .head _ ⟨some (readState S T (l ++ [b])), .mk₁ t⟩ _ _ + (tableComputer_read_step S T l b t) ?_ + have h := ih (l ++ [b]) + rwa [← List.append_cons] at h + +/-! ### Lookup and writing-phase verification -/ + +private lemma tableComputer_blank_step (S : Finset (List Symbol)) + (T : List Symbol → List Symbol) (l : List Symbol) : + (tableComputer S T).TransitionRelation + ⟨some (readState S T l), .nil⟩ ⟨enterState S T l, .nil⟩ := by + change (tableComputer S T).step _ = _ + by_cases h : l ∈ prefixClosure S + · simp only [readState] + rw [dif_pos h] + rfl + · simp only [readState, enterState] + rw [dif_neg h, dif_neg fun hS => h (subset_prefixClosure S hS)] + rfl + +private lemma tableComputer_write_steps (S : Finset (List Symbol)) + (T : List Symbol → List Symbol) (s : {s // s ∈ S}) (i : ℕ) : + ∀ (hi : i < (T s.1).length), + RelatesInSteps (tableComputer S T).TransitionRelation + ⟨some (.inr ⟨s, ⟨i, hi⟩⟩), ⟨none, ∅, .mapSome ((T s.1).drop (i + 1))⟩⟩ + ⟨none, .mk₁ (T s.1)⟩ (i + 1) := by + induction i with + | zero => + intro hi + refine .single ?_ + change (tableComputer S T).step _ = _ + rw [bitape_mk₁_eq_of_length_pos hi] + rfl + | succ i ih => + intro hi + refine .head _ ⟨some (.inr ⟨s, ⟨i, by omega⟩⟩), + ⟨none, ∅, .mapSome ((T s.1).drop (i + 1))⟩⟩ _ _ ?_ (ih (by omega)) + change (tableComputer S T).step _ = _ + rw [List.drop_eq_getElem_cons hi] + rfl + +private lemma tableComputer_finish_within (S : Finset (List Symbol)) + (T : List Symbol → List Symbol) (l : List Symbol) : + RelatesWithinSteps (tableComputer S T).TransitionRelation + ⟨some (readState S T l), .nil⟩ + ⟨none, .mk₁ (if l ∈ S then T l else [])⟩ + ((S.sup fun s => (T s).length) + 1) := by + have h1 := tableComputer_blank_step S T l + simp only [enterState] at h1 + by_cases hS : l ∈ S + · by_cases hT : (T l).length = 0 + · rw [dif_pos hS, dif_pos hT] at h1 + rw [if_pos hS, List.length_eq_zero_iff.mp hT] + exact RelatesWithinSteps.of_le (.single h1) (by omega) + · rw [dif_pos hS, dif_neg hT] at h1 + rw [if_pos hS] + have h2 := tableComputer_write_steps S T ⟨l, hS⟩ ((T l).length - 1) + (by change (T l).length - 1 < (T l).length; omega) + rw [show (T l).length - 1 + 1 = (T l).length from by omega, + List.drop_length] at h2 + refine RelatesWithinSteps.of_le + ((RelatesWithinSteps.single h1).trans + (RelatesWithinSteps.of_relatesInSteps h2)) ?_ + have hle : (T l).length ≤ S.sup fun s => (T s).length := + Finset.le_sup (f := fun s => (T s).length) hS + omega + · rw [dif_neg hS] at h1 + rw [if_neg hS] + exact RelatesWithinSteps.of_le (.single h1) (by omega) + +/-! ### Assembly -/ + +/-- Finite tables are machine-computable in linear time: `n` steps to read the input +into state, then at most one plus the longest table output to write the result. -/ +def tableTimeComputable (S : Finset (List Symbol)) (T : List Symbol → List Symbol) : + TimeComputable (Symbol := Symbol) (fun l => if l ∈ S then T l else []) where + tm := tableComputer S T + timeBound n := n + ((S.sup fun s => (T s).length) + 1) + outputsFunInTime l := by + exact (RelatesWithinSteps.of_relatesInSteps + (tableComputer_read_steps S T l [])).trans (tableComputer_finish_within S T l) + +/-- Finite tables are machine-computable in polynomial time. -/ +noncomputable def tablePolyTimeComputable (S : Finset (List Symbol)) + (T : List Symbol → List Symbol) : + PolyTimeComputable (Symbol := Symbol) (fun l => if l ∈ S then T l else []) where + toTimeComputable := tableTimeComputable S T + poly := .X + .C ((S.sup fun s => (T s).length) + 1) + bounds n := by + simp only [tableTimeComputable, Polynomial.eval_add, Polynomial.eval_X, + Polynomial.eval_C] + omega + +/-! ### Description size of the table machine + +The table machine's *time* is linear, but its *state count* — the reading prefix tree +plus the writing states — grows with the total length of the valid inputs and their +table outputs. This is the advice a table smuggles: a family of tables over +exponentially large domains has exponential description size, which is why witness +families must carry an explicit size bound (`ToCslib.Computability.EncPolyTime.size`). -/ + +omit [Inhabited Symbol] [Fintype Symbol] in +/-- The prefix tree of a finite set of strings has at most `∑ (length + 1)` nodes. -/ +theorem card_prefixClosure_le (S : Finset (List Symbol)) : + (prefixClosure S).card ≤ ∑ s ∈ S, (s.length + 1) := + Finset.card_biUnion_le.trans (Finset.sum_le_sum fun s _ => + (List.toFinset_card_le _).trans (by simp)) + +omit [Inhabited Symbol] [Fintype Symbol] in +/-- The state count of the finite-table machine: prefix-tree nodes, the junk state, and +one writing state per output symbol. -/ +theorem card_tableState (S : Finset (List Symbol)) (T : List Symbol → List Symbol) : + Fintype.card (TableState S T) = + ((prefixClosure S).card + 1) + ∑ s ∈ S, (T s).length := by + simp [TableState, Fintype.card_sigma, Finset.sum_attach S fun s => (T s).length] + +end Table + +end Cslib.Turing.SingleTapeTM + +namespace ToCslib.Computability.EncPolyTime + +/-- Constant functions are polynomial-time computable relative to any encodings. -/ +noncomputable def const {α : Type u} {β : Type v} (ea : α → List Bool) + (eb : β → List Bool) (c : β) : EncPolyTime ea eb (fun _ => c) where + toFun _ := eb c + polyTime := Cslib.Turing.SingleTapeTM.constPolyTimeComputable (eb c) + map_encode _ := rfl + +/-- **Any function with a finite domain is polynomial-time computable** relative to an +injective input encoding: the machine reads the input into state through the prefix +tree of the finitely many valid encodings, then writes the encoded output. The trade is +time for description: the machine has one reading state per prefix of a valid input +(`size_ofFintype_le`), so families of these witnesses respect a polynomial advice bound +only on domains of polynomially bounded cardinality. Instantiated at the injective +encodings of `ToCslib.Computability.BitEncFam` / +`ToCslib.Computability.StrEncFam`, this discharges the per-step machine witnesses. -/ +noncomputable def ofFintype {α : Type u} {β : Type v} [Fintype α] + (ea : α → List Bool) (hea : Function.Injective ea) (eb : β → List Bool) + (f : α → β) : EncPolyTime ea eb f where + toFun l := if l ∈ Finset.univ.image ea + then ((Function.partialInv ea l).map fun a => eb (f a)).getD [] else [] + polyTime := Cslib.Turing.SingleTapeTM.tablePolyTimeComputable (Finset.univ.image ea) + fun l => ((Function.partialInv ea l).map fun a => eb (f a)).getD [] + map_encode a := by + rw [if_pos (Finset.mem_image_of_mem ea (Finset.mem_univ a)), + Function.partialInv_left hea] + rfl + +/-- The finite-table witness runs in time linear in the input plus the longest encoded +output: with a pointwise bound `B` on the output encodings, evaluation at `k` is at +most `k + (B + 1)`. This is the shape that discharges the uniform per-step time bounds +of parameter-indexed backend certificates. -/ +theorem time_ofFintype_eval_le {α : Type u} {β : Type v} [Fintype α] + {ea : α → List Bool} (hea : Function.Injective ea) {eb : β → List Bool} + {f : α → β} {B : ℕ} (hB : ∀ a, (eb (f a)).length ≤ B) (k : ℕ) : + (ofFintype ea hea eb f).time.eval k ≤ k + (B + 1) := by + have htime : (ofFintype ea hea eb f).time = + .X + .C (((Finset.univ.image ea).sup fun l => + (((Function.partialInv ea l).map fun a => eb (f a)).getD []).length) + 1) := rfl + have hsup : ((Finset.univ.image ea).sup fun l => + (((Function.partialInv ea l).map fun a => eb (f a)).getD []).length) ≤ B := by + refine Finset.sup_le fun l hl => ?_ + obtain ⟨a, -, rfl⟩ := Finset.mem_image.mp hl + rw [Function.partialInv_left hea] + exact hB a + rw [htime, Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C] + omega + +/-- The constant-function witness has at most `(eb c).length + 2` machine states. -/ +theorem size_const_le {α : Type u} {β : Type v} (ea : α → List Bool) + (eb : β → List Bool) (c : β) : + (const ea eb c).size ≤ (eb c).length + 2 := + Cslib.Turing.SingleTapeTM.size_constPolyTimeComputable_le (eb c) + +/-- The description size of the finite-table witness: the machine hard-codes the whole +input/output table, so its state count grows with the **total encoded length of the +domain** — for a domain of exponential cardinality this is exponential advice, however +fast the machine runs. Families of `ofFintype` witnesses are therefore only usable +where the domain cardinality is polynomially bounded in the security parameter. -/ +theorem size_ofFintype_le {α : Type u} {β : Type v} [Fintype α] + {ea : α → List Bool} (hea : Function.Injective ea) (eb : β → List Bool) + (f : α → β) : + (ofFintype ea hea eb f).size ≤ + (∑ a : α, ((ea a).length + 1)) + 1 + ∑ a : α, (eb (f a)).length := by + change Fintype.card (Cslib.Turing.SingleTapeTM.TableState (Finset.univ.image ea) + fun l => ((Function.partialInv ea l).map fun a => eb (f a)).getD []) ≤ _ + rw [Cslib.Turing.SingleTapeTM.card_tableState] + have hinj : ∀ a ∈ Finset.univ, ∀ b ∈ Finset.univ, ea a = ea b → a = b := + fun a _ b _ h => hea h + have h1 : (Cslib.Turing.SingleTapeTM.prefixClosure (Finset.univ.image ea)).card ≤ + ∑ a : α, ((ea a).length + 1) := by + refine (Cslib.Turing.SingleTapeTM.card_prefixClosure_le _).trans (le_of_eq ?_) + rw [Finset.sum_image hinj] + have h2 : (∑ s ∈ Finset.univ.image ea, + (((Function.partialInv ea s).map fun a => eb (f a)).getD []).length) = + ∑ a : α, (eb (f a)).length := by + rw [Finset.sum_image hinj] + exact Finset.sum_congr rfl fun a _ => by rw [Function.partialInv_left hea]; rfl + omega + +/-- Discharge form of `size_ofFintype_le`: a cardinality bound on the domain and +pointwise bounds on both encodings give the table size bound consumed by +a uniform description bound fields. -/ +theorem size_ofFintype_le_of_bounds {α : Type u} {β : Type v} [Fintype α] + {ea : α → List Bool} (hea : Function.Injective ea) {eb : β → List Bool} + {f : α → β} {A La B : ℕ} (hcard : Fintype.card α ≤ A) + (hla : ∀ a, (ea a).length ≤ La) (hB : ∀ a, (eb (f a)).length ≤ B) : + (ofFintype ea hea eb f).size ≤ A * (La + 1 + B) + 1 := by + refine (size_ofFintype_le hea eb f).trans ?_ + have h1 : (∑ a : α, ((ea a).length + 1)) ≤ Fintype.card α * (La + 1) := by + refine (Finset.sum_le_card_nsmul _ _ (La + 1) fun a _ => ?_).trans_eq (by + simp [smul_eq_mul]) + have := hla a; omega + have h2 : (∑ a : α, (eb (f a)).length) ≤ Fintype.card α * B := by + refine (Finset.sum_le_card_nsmul _ _ B fun a _ => hB a).trans_eq (by + simp [smul_eq_mul]) + have h3 : Fintype.card α * (La + 1) ≤ A * (La + 1) := Nat.mul_le_mul_right _ hcard + have h4 : Fintype.card α * B ≤ A * B := Nat.mul_le_mul_right _ hcard + calc (∑ a : α, ((ea a).length + 1)) + 1 + ∑ a : α, (eb (f a)).length + ≤ A * (La + 1) + 1 + A * B := by omega + _ = A * (La + 1 + B) + 1 := by ring + +end ToCslib.Computability.EncPolyTime diff --git a/ToCslib/Computability/SingleTape/Counting.lean b/ToCslib/Computability/SingleTape/Counting.lean new file mode 100644 index 0000000..f310d9b --- /dev/null +++ b/ToCslib/Computability/SingleTape/Counting.lean @@ -0,0 +1,518 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma, Elias Judin +-/ +module + +public import ToCslib.Computability.BitEncoding +public import Mathlib.Analysis.SpecificLimits.Normed +public import Mathlib.Data.FinEnum + +/-! +# Counting Polynomial-Size Turing Machines + +The combinatorial core of the non-triviality certificate for the machine-grounded +polynomial-time model : only +sub-doubly-exponentially many predicates `BitVec n → Bool` are realizable by +`d`-state single-tape machines, while there are `2 ^ (2 ^ n)` such predicates. + +The pieces, each isolated so the diagonalization argument reads as pure counting: + +* **Canonical `d`-state machines** (`Cslib.Turing.SingleTapeTM.TMTable`): a transition table + `Fin d → Option Bool → Stmt Bool × Option (Fin d)` together with an initial state. + These are a `Fintype` with an explicit, provable cardinality + (`card_tmTable`, bounded by `Cslib.Turing.SingleTapeTM.B`), and `reify` packages one back + into a `SingleTapeTM Bool`. The `Fintype`/`DecidableEq` instances for the underlying + `Turing.Dir` and `SingleTapeTM.Stmt Bool` are supplied here. +* **State normalization** (`exists_tmTable_of_card_le`): any + `SingleTapeTM Bool` with at most `d` states computes the same string function as + `reify` of some `TMTable d`. +* **Realizable predicates** (`ToCslib.Computability.RealizableLE`): the predicates realizable by + an input/output `EncPolyTime` pair of description size at most `d`. This set is covered + by a `Finset` of cardinality at most `B d ^ 2` (`exists_realizableLE_covering`, the + counting core: the cover of `RealizableLE n d` by the image of + `TMTable d × TMTable d` under `tablePairPred`, built from state normalization), and it is + monotone in `d` (`realizableLE_mono`). +* **Growth bounds**: every polynomial is eventually dominated by `2 ^ (n / 4)` + (`ToCslib.Computability.eventually_poly_le`), while the machine count stays below the function + count (`ToCslib.Computability.eventually_count_lt`). +* **The function space** has cardinality `2 ^ (2 ^ n)` (`ToCslib.Computability.card_bitVec_fun`), + and a `Finset` family of subexponential cardinality misses a diagonal predicate + eventually (`ToCslib.Computability.exists_diagonal`). +-/ + +@[expose] public section + +open Filter Asymptotics + +namespace Cslib.Turing.SingleTapeTM + +/-! ## Finiteness of statements and directions -/ + +/-- A `SingleTapeTM.Stmt` is a pair of an optional write symbol and an optional move. -/ +def stmtProdEquiv : SingleTapeTM.Stmt Bool ≃ (Option Bool × Option Turing.Dir) where + toFun s := (s.symbol, s.movement) + invFun p := ⟨p.1, p.2⟩ + left_inv _ := rfl + right_inv _ := rfl + +instance instFintypeDirToCslib : Fintype Turing.Dir := + ⟨{Turing.Dir.left, Turing.Dir.right}, fun d => by cases d <;> decide⟩ + +instance instDecidableEqStmtBoolToCslib : DecidableEq (SingleTapeTM.Stmt Bool) := + fun _ _ => decidable_of_iff _ stmtProdEquiv.injective.eq_iff + +noncomputable instance instFintypeStmtBoolToCslib : Fintype (SingleTapeTM.Stmt Bool) := + Fintype.ofEquiv _ stmtProdEquiv.symm + +theorem card_dir : Fintype.card Turing.Dir = 2 := by decide + +theorem card_stmt : Fintype.card (SingleTapeTM.Stmt Bool) = 9 := by + rw [Fintype.card_congr stmtProdEquiv]; decide + +/-! ## Canonical `d`-state machines -/ + +/-- A canonical `d`-state single-tape machine over `Bool`: a transition table on states +`Fin d` together with an initial state. Every machine with at most `d` states computes, +after relabeling, the same function as `reify` of one of these (`exists_tmTable_of_card_le`), +so `TMTable d` is the finite index of `d`-state machines used for counting. -/ +abbrev TMTable (d : ℕ) : Type := + (Fin d → Option Bool → SingleTapeTM.Stmt Bool × Option (Fin d)) × Fin d + +noncomputable instance (d : ℕ) : Fintype (TMTable d) := inferInstance + +instance (d : ℕ) : DecidableEq (TMTable d) := inferInstance + +/-- A crude closed-form upper bound on the number of `d`-state machines: the exact +cardinality `card_tmTable`. -/ +def B (d : ℕ) : ℕ := (9 * (d + 1)) ^ (3 * d) * d + +/-- The exact number of canonical `d`-state machines: each of the `d` states maps each of +the `3` head symbols (`Option Bool`) to one of the `9 * (d + 1)` statement/next-state +pairs, and there are `d` choices of initial state. -/ +theorem card_tmTable (d : ℕ) : Fintype.card (TMTable d) = B d := by + simp only [B, TMTable, Fintype.card_prod, Fintype.card_fun, card_stmt, + Fintype.card_option, Fintype.card_fin, Fintype.card_bool, ← pow_mul] + +theorem card_tmTable_le (d : ℕ) : Fintype.card (TMTable d) ≤ B d := + (card_tmTable d).le + +/-- Package a canonical table back into a `SingleTapeTM Bool` on state space `Fin d`. -/ +def reify {d : ℕ} (t : TMTable d) : SingleTapeTM Bool where + State := Fin d + q₀ := t.2 + tr := t.1 + +/-! ## State-relabeling normalization construction + +The machinery discharging `exists_tmTable_of_card_le`: relabel the finite state space of a +machine `tm` through `Fintype.equivFin`, embed `Fin (card tm.State)` into `Fin d` along the +cardinality inequality (`embFin`), and transport the transition function on the image +(`normTr`), sending every spare state (those outside the image, detected by `decFin`) to a +fixed halting transition. Configurations transport along `normCfg`, single steps correspond +(`step_normCfg`), and this lifts through `ReflTransGen` in both directions +(`normCfg_reflTransGen`, `reflTransGen_normCfg_reverse`), giving the `Outputs` equivalence. -/ + +section Normalize + +/-- Embed a finite type into `Fin d` (with `card ≤ d`) via its `Fintype.equivFin` labeling. -/ +noncomputable def embFin {α : Type*} [Fintype α] {d : ℕ} (hd : Fintype.card α ≤ d) (s : α) : + Fin d := + (Fintype.equivFin α s).castLE hd + +/-- The partial inverse of `embFin`: recover the state whose label is `i`, or `none` for +spare indices `i` with no preimage. -/ +noncomputable def decFin {α : Type*} [Fintype α] {d : ℕ} (i : Fin d) : Option α := + if hi : (i : ℕ) < Fintype.card α then some ((Fintype.equivFin α).symm ⟨i, hi⟩) else none + +/-- `decFin` inverts `embFin` on the image. -/ +lemma decFin_embFin {α : Type*} [Fintype α] {d : ℕ} (hd : Fintype.card α ≤ d) (s : α) : + (decFin (embFin hd s) : Option α) = some s := by + have hlt : ((embFin hd s : Fin d) : ℕ) < Fintype.card α := by + simp only [embFin, Fin.val_castLE]; exact (Fintype.equivFin α s).isLt + simp only [decFin, dif_pos hlt] + congr 1 + apply (Fintype.equivFin α).symm_apply_eq.mpr + apply Fin.ext + simp [embFin, Fin.val_castLE] + +/-- `embFin` is injective. -/ +lemma embFin_injective {α : Type*} [Fintype α] {d : ℕ} (hd : Fintype.card α ≤ d) : + Function.Injective (embFin hd) := fun _ _ hab => + (Fintype.equivFin α).injective (Fin.castLE_injective hd hab) + +variable {d : ℕ} (tm : SingleTapeTM Bool) (emb : tm.State → Fin d) + (dec : Fin d → Option tm.State) + +/-- Transition table transporting `tm`'s transitions along `emb`; spare states (those with +`dec i = none`) are given a fixed halting transition. -/ +noncomputable def normTr : Fin d → Option Bool → SingleTapeTM.Stmt Bool × Option (Fin d) := + fun i b => + match dec i with + | some s => ((tm.tr s b).1, (tm.tr s b).2.map emb) + | none => (default, none) + +/-- The canonical `d`-state table normalizing `tm` onto `Fin d` along `emb`/`dec`. -/ +noncomputable def normTable : TMTable d := (normTr tm emb dec, emb tm.q₀) + +/-- Transport a configuration of `tm` to the reified normalized machine. -/ +noncomputable def normCfg (c : tm.Cfg) : (reify (normTable tm emb dec)).Cfg := + ⟨c.state.map emb, c.BiTape⟩ + +variable {tm emb dec} + +/-- The reified normalized machine's step transports `tm`'s step along `normCfg`, provided +`dec` inverts `emb` on the image. -/ +lemma step_normCfg (hdec : ∀ s, dec (emb s) = some s) (c : tm.Cfg) : + (reify (normTable tm emb dec)).step (normCfg tm emb dec c) + = (tm.step c).map (normCfg tm emb dec) := by + obtain ⟨st, tp⟩ := c + cases st with + | none => rfl + | some q => + have hdq : dec (emb q) = some q := hdec q + rcases htr : tm.tr q tp.head with ⟨⟨wr, dir⟩, q''⟩ + simp only [step, normCfg, reify, normTable, normTr, Option.map_some, hdq, htr] + rfl + +/-- `normCfg` is injective when `emb` is. -/ +lemma normCfg_injective (hemb : Function.Injective emb) : + Function.Injective (normCfg tm emb dec) := by + rintro ⟨s1, t1⟩ ⟨s2, t2⟩ h + simp only [normCfg, Cfg.mk.injEq] at h + obtain ⟨hs, ht⟩ := h + have hss : s1 = s2 := Option.map_injective hemb hs + subst hss; subst ht; rfl + +/-- A run of `tm` maps forward to a run of the normalized machine. -/ +lemma normCfg_reflTransGen (hdec : ∀ s, dec (emb s) = some s) {c c' : tm.Cfg} + (h : Relation.ReflTransGen tm.TransitionRelation c c') : + Relation.ReflTransGen (reify (normTable tm emb dec)).TransitionRelation + (normCfg tm emb dec c) (normCfg tm emb dec c') := by + have hstep : ∀ a b, tm.TransitionRelation a b → + (reify (normTable tm emb dec)).TransitionRelation + (normCfg tm emb dec a) (normCfg tm emb dec b) := by + intro a b hab + have hs := step_normCfg hdec a + rw [show tm.step a = some b from hab, Option.map_some] at hs + exact hs + exact Relation.ReflTransGen.lift (normCfg tm emb dec) hstep c c' h + +/-- A run of the normalized machine from an image configuration stays in the image and maps +back to a run of `tm`. -/ +lemma reflTransGen_normCfg_reverse (hdec : ∀ s, dec (emb s) = some s) {c : tm.Cfg} + {c' : (reify (normTable tm emb dec)).Cfg} + (h : Relation.ReflTransGen (reify (normTable tm emb dec)).TransitionRelation + (normCfg tm emb dec c) c') : + ∃ c₂, c' = normCfg tm emb dec c₂ ∧ Relation.ReflTransGen tm.TransitionRelation c c₂ := by + induction h with + | refl => exact ⟨c, rfl, Relation.ReflTransGen.refl⟩ + | @tail b e hab hbc ih => + obtain ⟨c₂, rfl, hrun⟩ := ih + have hs := step_normCfg hdec c₂ + rw [show (reify (normTable tm emb dec)).step (normCfg tm emb dec c₂) = some e from hbc] at hs + obtain ⟨c₃, hstep, hc3⟩ := Option.map_eq_some_iff.mp hs.symm + exact ⟨c₃, hc3.symm, hrun.tail hstep⟩ + +end Normalize + +/-! ## Determinism of machine runs + +Supporting facts for `ToCslib.Computability.exists_realizableLE_covering`: a single-tape machine +is deterministic (its `step` is a function), so the output list of a halting run is +unique. This lets the covering predicate attached to a table pair be read off by an +unbounded-search-free choice construction and still agree with any witness predicate. -/ + +section Determinism + +/-- In a relation that is a partial function (deterministic), two irreducible points +reachable from a common source coincide. -/ +theorem _root_.Relation.ReflTransGen.unique_of_deterministic + {α : Type*} {R : α → α → Prop} + (hdet : ∀ {a b c : α}, R a b → R a c → b = c) + {a b c : α} (hb : Relation.ReflTransGen R a b) (hc : Relation.ReflTransGen R a c) + (hbf : ∀ y, ¬ R b y) (hcf : ∀ y, ¬ R c y) : b = c := by + induction hb using Relation.ReflTransGen.head_induction_on with + | refl => + rcases hc.cases_head with h | ⟨y, hy, _⟩ + · exact h + · exact absurd hy (hbf y) + | head h' _ ih => + rename_i a' _ + rcases hc.cases_head with h | ⟨y, hy, hyc⟩ + · exact absurd (h ▸ h') (hcf a') + · rw [hdet h' hy] at ih; exact ih hyc + +/-- Distinct input lists give distinct initial/halting tapes: `BiTape.mk₁` is injective. -/ +theorem _root_.Cslib.Turing.BiTape.mk₁_injective {Symbol : Type} : + Function.Injective (Cslib.Turing.BiTape.mk₁ : List Symbol → Cslib.Turing.BiTape Symbol) := by + intro l₁ l₂ h + cases l₁ with + | nil => + cases l₂ with + | nil => rfl + | cons b t => simp [Cslib.Turing.BiTape.mk₁, Cslib.Turing.BiTape.nil] at h + | cons a s => + cases l₂ with + | nil => simp [Cslib.Turing.BiTape.mk₁, Cslib.Turing.BiTape.nil] at h + | cons b t => + simp only [Cslib.Turing.BiTape.mk₁, Cslib.Turing.BiTape.mk.injEq, Option.some.injEq] at h + obtain ⟨hab, -, hst⟩ := h + have : (s.map some) = (t.map some) := by + have := congrArg Cslib.Turing.StackTape.toList hst + simpa [Cslib.Turing.StackTape.mapSome] using this + have hst' : s = t := List.map_injective_iff.mpr (Option.some_injective _) this + rw [hab, hst'] + +variable {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] + +/-- A halting configuration is irreducible: no transition leaves the halting state. -/ +theorem not_transitionRelation_haltCfg (tm : SingleTapeTM Symbol) (l : List Symbol) + (y : tm.Cfg) : ¬ tm.TransitionRelation (tm.haltCfg l) y := by + intro hy + simp only [TransitionRelation, haltCfg, step] at hy + exact absurd hy (by simp) + +/-- The output list of a halting machine run is unique: the machine is deterministic. -/ +theorem Outputs_unique (tm : SingleTapeTM Symbol) {l l₁ l₂ : List Symbol} + (h1 : tm.Outputs l l₁) (h2 : tm.Outputs l l₂) : l₁ = l₂ := by + have hcfg : tm.haltCfg l₁ = tm.haltCfg l₂ := by + refine Relation.ReflTransGen.unique_of_deterministic (R := tm.TransitionRelation) + (fun {a b c} hab hac => ?_) h1 h2 (not_transitionRelation_haltCfg tm l₁) + (not_transitionRelation_haltCfg tm l₂) + rw [TransitionRelation] at hab hac + rw [hab] at hac + exact Option.some.inj hac + have := congrArg Cfg.BiTape hcfg + simp only [haltCfg] at this + exact Cslib.Turing.BiTape.mk₁_injective this + +/-- A polynomial-time machine halts with the correct output on every input. -/ +theorem PolyTimeComputable.outputs {f : List Symbol → List Symbol} + (h : PolyTimeComputable f) (a : List Symbol) : h.tm.Outputs a (f a) := by + obtain ⟨m, _, hm⟩ := h.outputsFunInTime a + exact hm.reflTransGen + +end Determinism + +/-! ## State normalization -/ + +/-- Every `SingleTapeTM Bool` with at most `d` states has the same `Outputs` relation as +`reify` of some `TMTable d` — the state space is relabeled to `Fin d` along +`Fintype.equivFin`. It is the machine-theoretic input to +`exists_realizableLE_covering`. -/ +theorem exists_tmTable_of_card_le (tm : SingleTapeTM Bool) + {d : ℕ} (hd : Fintype.card tm.State ≤ d) : + ∃ t : TMTable d, ∀ l l', (reify t).Outputs l l' ↔ tm.Outputs l l' := by + refine ⟨normTable tm (embFin hd) (decFin (α := tm.State)), fun l l' => ?_⟩ + have hdec : ∀ s, decFin (α := tm.State) (embFin hd s) = some s := decFin_embFin hd + have hemb : Function.Injective (embFin (α := tm.State) hd) := embFin_injective hd + have hinit : normCfg tm (embFin hd) (decFin (α := tm.State)) (tm.initCfg l) + = (reify (normTable tm (embFin hd) (decFin (α := tm.State)))).initCfg l := rfl + have hhalt : normCfg tm (embFin hd) (decFin (α := tm.State)) (tm.haltCfg l') + = (reify (normTable tm (embFin hd) (decFin (α := tm.State)))).haltCfg l' := rfl + constructor + · intro hout + have hout' : Relation.ReflTransGen + (reify (normTable tm (embFin hd) (decFin (α := tm.State)))).TransitionRelation + (normCfg tm (embFin hd) (decFin (α := tm.State)) (tm.initCfg l)) + ((reify (normTable tm (embFin hd) (decFin (α := tm.State)))).haltCfg l') := by + rw [hinit]; exact hout + obtain ⟨c₂, hc₂, hrun⟩ := reflTransGen_normCfg_reverse hdec hout' + rw [← hhalt] at hc₂ + have hcfg : tm.haltCfg l' = c₂ := normCfg_injective hemb hc₂ + rw [← hcfg] at hrun + exact hrun + · intro hout + have hmap := normCfg_reflTransGen hdec hout + rw [hinit, hhalt] at hmap + exact hmap + +end Cslib.Turing.SingleTapeTM + +namespace ToCslib.Computability + +open Cslib.Turing.SingleTapeTM + +/-! ## Realizable predicates -/ + +/-- The predicates `BitVec n → Bool` realizable at description size at most `d`: those +computed by an initialization witness into some state encoding followed by an output +witness, both `EncPolyTime` machines of description size at most `d`, against the canonical +`BitVec`/`Option Bool` boundary encodings. An implementing machine adversary at these +boundaries lands its computed predicate here (its `initF`/`outputF` witnesses), and the +count of such predicates is controlled by counting the underlying machines +(`exists_realizableLE_covering`). -/ +def RealizableLE (n d : ℕ) : Set (BitVec n → Bool) := + {g | ∃ (σ : Type) (es : σ → List Bool) (init : BitVec n → σ) (output : σ → Option Bool) + (_i : EncPolyTime (BitEncFam.bitVecX.enc n) es init) + (_o : EncPolyTime es (BitEncFam.bool.option.enc n) output), + _i.size ≤ d ∧ _o.size ≤ d ∧ ∀ x, output (init x) = some (g x)} + +/-- Realizability at a larger description size is a weaker requirement. -/ +theorem realizableLE_mono {n : ℕ} {d d' : ℕ} (h : d ≤ d') : + RealizableLE n d ⊆ RealizableLE n d' := by + rintro g ⟨σ, es, init, output, i, o, hi, ho, hg⟩ + exact ⟨σ, es, init, output, i, o, hi.trans h, ho.trans h, hg⟩ + +open Classical in +/-- The total predicate `BitVec n → Bool` attached to a pair of canonical `d`-state tables: +run `reify p.1` on the canonical input encoding of `x`, feed its (deterministic) output to +`reify p.2`, and decode the resulting canonical `Option Bool` encoding. Totality is ensured +by a deterministic choice over the (at most one, by `Outputs_unique`) successful run, with +an arbitrary `false` fallback where no such run exists — no claim that either raw table +pair halts or is polynomial-time. -/ +noncomputable def tablePairPred (n d : ℕ) (p : TMTable d × TMTable d) : BitVec n → Bool := + fun x => + if h : ∃ b : Bool, ∃ l₁ : List Bool, + (reify p.1).Outputs (BitEncFam.bitVecX.enc n x) l₁ ∧ + (reify p.2).Outputs l₁ (BitEncFam.bool.option.enc n (some b)) + then h.choose else false + +/-- The realizable predicates at description size at most `d` are covered by a `Finset` of +cardinality at most `B d ^ 2`. State normalization (`exists_tmTable_of_card_le`) reduces each +realizing pair of witness machines to a pair `TMTable d × TMTable d` of canonical `d`-state +tables; the realized predicate is recovered from the two tables by `tablePairPred` (running +both reified machines and decoding the canonical output encoding, using determinism of the +runs via `Outputs_unique`). Thus `RealizableLE n d` lands in the image of +`TMTable d × TMTable d` under `tablePairPred`, whence +`card ≤ Fintype.card (TMTable d × TMTable d) = B d ^ 2` (`card_tmTable`). The map need not be +injective — it only needs to cover the realizable set. -/ +theorem exists_realizableLE_covering (n d : ℕ) : + ∃ s : Finset (BitVec n → Bool), RealizableLE n d ⊆ ↑s ∧ s.card ≤ B d ^ 2 := by + classical + refine ⟨Finset.image (tablePairPred n d) + (Finset.univ : Finset (TMTable d × TMTable d)), ?_, ?_⟩ + · rintro g ⟨σ, es, init, output, i, o, hi, ho, hg⟩ + obtain ⟨t₁, ht₁⟩ := exists_tmTable_of_card_le i.polyTime.tm (d := d) hi + obtain ⟨t₂, ht₂⟩ := exists_tmTable_of_card_le o.polyTime.tm (d := d) ho + refine Finset.mem_coe.mpr (Finset.mem_image.mpr ⟨(t₁, t₂), Finset.mem_univ _, ?_⟩) + funext x + have hrun1 : (reify t₁).Outputs (BitEncFam.bitVecX.enc n x) (es (init x)) := by + rw [ht₁] + have h := i.polyTime.outputs (BitEncFam.bitVecX.enc n x) + rwa [i.map_encode x] at h + have hrun2 : (reify t₂).Outputs (es (init x)) + (BitEncFam.bool.option.enc n (some (g x))) := by + rw [ht₂] + have h := o.polyTime.outputs (es (init x)) + rwa [o.map_encode (init x), hg x] at h + have hex : ∃ b : Bool, ∃ l₁ : List Bool, + (reify t₁).Outputs (BitEncFam.bitVecX.enc n x) l₁ ∧ + (reify t₂).Outputs l₁ (BitEncFam.bool.option.enc n (some b)) := + ⟨g x, es (init x), hrun1, hrun2⟩ + have hpick : tablePairPred n d (t₁, t₂) x = hex.choose := dif_pos hex + rw [hpick] + obtain ⟨l₁', hl1', hl2'⟩ := hex.choose_spec + have hl1eq : l₁' = es (init x) := Outputs_unique _ hl1' hrun1 + rw [hl1eq] at hl2' + have henc := Outputs_unique _ hl2' hrun2 + exact Option.some.inj ((BitEncFam.bool.option).enc_injective n henc) + · refine Finset.card_image_le.trans ?_ + rw [Finset.card_univ, Fintype.card_prod, card_tmTable, sq] + +/-! ## Cardinality of the predicate space -/ + +/-- There are exactly `2 ^ (2 ^ n)` predicates `BitVec n → Bool`. -/ +theorem card_bitVec_fun (n : ℕ) : Fintype.card (BitVec n → Bool) = 2 ^ (2 ^ n) := by + rw [Fintype.card_fun, Fintype.card_bool, ← FinEnum.card_eq_fintypeCard, FinEnum.card_bitVec] + +/-! ## Polynomial versus exponential growth -/ + +/-- Any fixed power is eventually dominated by `2 ^ n`. -/ +theorem nat_pow_le_two_pow (k : ℕ) : ∀ᶠ n in atTop, n ^ k ≤ 2 ^ n := by + have h : (fun n : ℕ => (n : ℝ) ^ k) =o[atTop] fun n : ℕ => (2 : ℝ) ^ n := + isLittleO_pow_const_const_pow_of_one_lt k (by norm_num) + refine h.eventuallyLE.mono fun n hn => ?_ + simp only [Real.norm_eq_abs] at hn + rw [abs_of_nonneg (by positivity), abs_of_nonneg (by positivity)] at hn + exact_mod_cast (by push_cast; exact hn : ((n ^ k : ℕ) : ℝ) ≤ ((2 ^ n : ℕ) : ℝ)) + +/-- A constant multiple of any fixed power of `n + 1` is eventually dominated by `2 ^ n`. -/ +theorem const_mul_pow_le_two_pow (C k : ℕ) : ∀ᶠ m in atTop, C * (m + 1) ^ k ≤ 2 ^ m := by + filter_upwards [eventually_ge_atTop (C * 2 ^ k), eventually_ge_atTop 1, + nat_pow_le_two_pow (k + 1)] with m hm hm1 hm3 + calc C * (m + 1) ^ k ≤ C * (2 * m) ^ k := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) k) + _ = C * 2 ^ k * m ^ k := by rw [mul_pow]; ring + _ ≤ m * m ^ k := Nat.mul_le_mul_right _ hm + _ = m ^ (k + 1) := by rw [pow_succ]; ring + _ ≤ 2 ^ m := hm3 + +/-- **Polynomials are eventually dominated by `2 ^ (n / 4)`.** The exponent `n / 4` is the +threshold fed to the machine count: fast enough to eventually exceed every polynomial +description bound (this lemma), yet slow enough that the resulting machine count stays below +`2 ^ (2 ^ n)` (`eventually_count_lt`). -/ +theorem eventually_poly_le (p : Polynomial ℕ) : + ∀ᶠ n in atTop, p.eval n ≤ 2 ^ (n / 4) := by + obtain ⟨C, k, hCk⟩ : ∃ C k : ℕ, ∀ n : ℕ, p.eval n ≤ C * (n + 1) ^ k := by + refine ⟨∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i, p.natDegree, fun n => ?_⟩ + rw [Polynomial.eval_eq_sum_range, Finset.sum_mul] + refine Finset.sum_le_sum fun i hi => ?_ + rw [Finset.mem_range] at hi + exact Nat.mul_le_mul_left _ ((Nat.pow_le_pow_left (by omega) i).trans + (Nat.pow_le_pow_right (by omega) (by omega))) + have htend : Tendsto (fun n : ℕ => n / 4) atTop atTop := + Nat.tendsto_div_const_atTop (by norm_num) + filter_upwards [htend.eventually (const_mul_pow_le_two_pow (C * 4 ^ k) k)] with n hn + calc p.eval n ≤ C * (n + 1) ^ k := hCk n + _ ≤ C * 4 ^ k * (n / 4 + 1) ^ k := by + rw [mul_assoc, ← mul_pow] + exact Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) k) + _ ≤ 2 ^ (n / 4) := hn + +/-- A crude closed-form bound on the squared machine count: for `9 * (d + 1) ≤ 2 ^ d` and +`d ≥ 1`, `B d ^ 2 ≤ 2 ^ (8 * d ^ 2)`. Uses `9 * (d + 1) ≤ 2 ^ d` on the statement/next-state +base and `d ^ 2 ≤ 2 ^ (2 * d)` on the initial-state factor. -/ +theorem B_sq_le (d : ℕ) (hd : 9 * (d + 1) ≤ 2 ^ d) (hd1 : 1 ≤ d) : + B d ^ 2 ≤ 2 ^ (8 * d ^ 2) := by + have hd2 : d ^ 2 ≤ 2 ^ (2 * d) := by + calc d ^ 2 ≤ (2 ^ d) ^ 2 := Nat.pow_le_pow_left (Nat.le_of_lt d.lt_two_pow_self) 2 + _ = 2 ^ (2 * d) := by rw [← pow_mul, Nat.mul_comm] + calc B d ^ 2 = ((9 * (d + 1)) ^ (3 * d)) ^ 2 * d ^ 2 := by rw [B, mul_pow] + _ = (9 * (d + 1)) ^ (6 * d) * d ^ 2 := by rw [← pow_mul]; ring_nf + _ ≤ (2 ^ d) ^ (6 * d) * 2 ^ (2 * d) := Nat.mul_le_mul (Nat.pow_le_pow_left hd _) hd2 + _ = 2 ^ (6 * d ^ 2) * 2 ^ (2 * d) := by rw [← pow_mul]; ring_nf + _ = 2 ^ (6 * d ^ 2 + 2 * d) := by rw [← pow_add] + _ ≤ 2 ^ (8 * d ^ 2) := Nat.pow_le_pow_right (by norm_num) (by nlinarith [hd1]) + +/-- **The squared machine count at the threshold size `2 ^ (n / 4)` stays below the +predicate count `2 ^ (2 ^ n)` eventually.** The count at size `d = 2 ^ (n / 4)` is at most +`2 ^ (8 * d ^ 2)` (`B_sq_le`, whose hypothesis `9 * (d + 1) ≤ 2 ^ d` holds cofinitely as +`d → ∞`), and its exponent `8 * d ^ 2 = 2 ^ (3 + n / 4 * 2)` is eventually below `2 ^ n`. -/ +theorem eventually_count_lt : + ∀ᶠ n in atTop, B (2 ^ (n / 4)) ^ 2 < 2 ^ (2 ^ n) := by + have htwo : Tendsto (fun m : ℕ => 2 ^ m) atTop atTop := + tendsto_atTop_mono (fun m => (Nat.lt_two_pow_self).le) tendsto_id + have htend : Tendsto (fun n : ℕ => 2 ^ (n / 4)) atTop atTop := + htwo.comp (Nat.tendsto_div_const_atTop (by norm_num)) + filter_upwards [htend.eventually (const_mul_pow_le_two_pow 9 1), + eventually_ge_atTop 8] with n ha hn + rw [pow_one] at ha + refine lt_of_le_of_lt (B_sq_le _ ha Nat.one_le_two_pow) ?_ + apply Nat.pow_lt_pow_right (by norm_num) + calc 8 * (2 ^ (n / 4)) ^ 2 + = 2 ^ (3 + n / 4 * 2) := by rw [show (8 : ℕ) = 2 ^ 3 from rfl, ← pow_mul, ← pow_add] + _ < 2 ^ n := Nat.pow_lt_pow_right (by norm_num) (by omega) + +/-! ## The diagonal predicate -/ + +/-- A `Finset` family of subexponential cardinality misses a predicate eventually: if +`(S n).card < 2 ^ (2 ^ n)` cofinitely, some family `f` has `f n ∉ S n` cofinitely. -/ +theorem exists_diagonal (S : (n : ℕ) → Finset (BitVec n → Bool)) + (hS : ∀ᶠ n in atTop, (S n).card < 2 ^ (2 ^ n)) : + ∃ f : (n : ℕ) → BitVec n → Bool, ∀ᶠ n in atTop, f n ∉ S n := by + classical + have key : ∀ n, (S n).card < 2 ^ (2 ^ n) → ∃ g : BitVec n → Bool, g ∉ S n := by + intro n hn + have hlt : (S n).card < (Finset.univ : Finset (BitVec n → Bool)).card := by + rw [Finset.card_univ, card_bitVec_fun]; exact hn + obtain ⟨e, -, he⟩ := Finset.exists_mem_notMem_of_card_lt_card hlt + exact ⟨e, he⟩ + refine ⟨fun n => if h : (S n).card < 2 ^ (2 ^ n) then (key n h).choose else default, ?_⟩ + refine hS.mono fun n hn => ?_ + simp only [dif_pos hn] + exact (key n hn).choose_spec + +end ToCslib.Computability diff --git a/ToCslib/Data/BitVec.lean b/ToCslib/Data/BitVec.lean new file mode 100644 index 0000000..a9e09f5 --- /dev/null +++ b/ToCslib/Data/BitVec.lean @@ -0,0 +1,78 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ +module + +public import Mathlib.Data.BitVec + +/-! +# Overwriting a Single Bit of a Bitvector + +This file defines `BitVec.overwriteBit i b m`, the bitvector `m` with its `i`-th least +significant bit replaced by `b`, together with its `getLsbD` description and the involution +`(m, b) ↦ (m with bit i overwritten by b, original bit i of m)` on `BitVec n × Bool`. +The involution is the change of variables underlying uniform-distribution splitting +arguments: sampling a uniform bitvector and reading its `i`-th bit is equivalent to +sampling a uniform bit and a uniform bitvector and overwriting the `i`-th bit. +-/ + +@[expose] public section + +namespace BitVec + +variable {n : ℕ} + +/-- Overwrite the `i`-th least significant bit of `m` with `b`, leaving all other bits +unchanged. Out-of-range positions (`n ≤ i`) leave `m` unmodified. -/ +def overwriteBit (i : ℕ) (b : Bool) (m : BitVec n) : BitVec n := + if b then m ||| twoPow n i else m &&& ~~~ twoPow n i + +theorem getLsbD_overwriteBit_self {i : ℕ} (hi : i < n) (b : Bool) (m : BitVec n) : + (overwriteBit i b m).getLsbD i = b := by + cases b <;> simp [overwriteBit, hi] + +@[simp] theorem getElem_overwriteBit_self {i : ℕ} (hi : i < n) (b : Bool) + (m : BitVec n) : (overwriteBit i b m)[i] = b := by + cases b <;> simp [overwriteBit] + +@[simp] theorem getLsbD_overwriteBit_of_ne {i j : ℕ} (h : j ≠ i) (b : Bool) (m : BitVec n) : + (overwriteBit i b m).getLsbD j = m.getLsbD j := by + rcases lt_or_ge j n with hj | hj + · cases b <;> simp [overwriteBit, h, hj] + · cases b <;> simp [overwriteBit, getLsbD_of_ge _ _ hj] + +theorem getLsbD_overwriteBit (i j : ℕ) (b : Bool) (m : BitVec n) : + (overwriteBit i b m).getLsbD j = if j = i ∧ i < n then b else m.getLsbD j := by + rcases eq_or_ne j i with rfl | h + · rcases lt_or_ge j n with hj | hj + · rw [if_pos ⟨rfl, hj⟩] + exact getLsbD_overwriteBit_self hj b m + · cases b <;> simp [overwriteBit, getLsbD_of_ge _ _ hj, Nat.not_lt.mpr hj] + · simp [h] + +/-- Overwriting the same position twice keeps only the outer write. -/ +@[simp] theorem overwriteBit_overwriteBit (i : ℕ) (b c : Bool) (m : BitVec n) : + overwriteBit i c (overwriteBit i b m) = overwriteBit i c m := + eq_of_getLsbD_eq_iff.mpr fun j _ => by + simp only [getLsbD_overwriteBit] + split <;> simp_all + +/-- Overwriting a bit with its current value is the identity. -/ +@[simp] theorem overwriteBit_getLsbD_self (i : ℕ) (m : BitVec n) : + overwriteBit i (m.getLsbD i) m = m := + eq_of_getLsbD_eq_iff.mpr fun j _ => by + rw [getLsbD_overwriteBit] + split <;> simp_all + +/-- Pairing a bitvector with its `i`-th bit while overwriting that bit with the paired +value is an involution on `BitVec n × Bool`. This is the change of variables that splits +a uniform bitvector by the value of its `i`-th bit. -/ +theorem involutive_overwriteBit_pair {i : ℕ} (hi : i < n) : + Function.Involutive fun p : BitVec n × Bool => + (overwriteBit i p.2 p.1, p.1.getLsbD i) := by + rintro ⟨m, b⟩ + simp [getLsbD_overwriteBit_self hi] + +end BitVec diff --git a/docs/wiki/repo-map.md b/docs/wiki/repo-map.md index 7f93f75..89c52e4 100644 --- a/docs/wiki/repo-map.md +++ b/docs/wiki/repo-map.md @@ -33,6 +33,9 @@ PolyFun/ quarantine root (Do/Basic) Logic/ small logic helpers (HEq) +ToCslib/ separate low-level extensions to the pinned cslib machine + API; imports cslib and Mathlib, never PolyFun + docs/wiki/ agent-facing notes (this directory) scripts/ repo utilities (validate, lint, update-lib, port helpers) .github/workflows/ CI workflows @@ -43,6 +46,15 @@ scripts/ repo utilities (validate, lint, update-lib, port helpers) Imports flow strictly downward, cycles are a build error. The DAG is also recorded in [`AGENTS.md`](../../AGENTS.md): +`ToCslib` is a separate lower library rather than part of this DAG: + +```text +Cslib + Mathlib -> ToCslib -> optional PolyFun backend adapters +``` + +It contains concrete machine constructions and lemmas, but no realizability, +oracle, probability, or cryptographic policy. + ```text PFunctor/{Basic, Bound, M, Equiv, Chart, Lens} -> PFunctor/{Cofree, Trace} diff --git a/lakefile.toml b/lakefile.toml index 6bf7278..b178df6 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,12 +1,12 @@ name = "PolyFun" defaultTargets = ["PolyFun"] -# `lake lint` runs Batteries' environment linters over the `PolyFun` library. +# `lake lint` runs Batteries' environment linters over both production libraries. # `lake test` builds the `PolyFunTest` library; any failing `example` / # `#guard` / `#eval` fails elaboration. This mirrors Mathlib and cslib, which # reuse `batteries/runLinter` rather than shipping a local runner. lintDriver = "batteries/runLinter" -lintDriverArgs = ["PolyFun"] +lintDriverArgs = ["PolyFun", "ToCslib"] testDriver = "PolyFunTest" [leanOptions] @@ -42,6 +42,12 @@ rev = "v4.33.1" [[lean_lib]] name = "PolyFun" +# Low-level extensions of the pinned cslib machine API. This target does not +# import PolyFun and is intentionally separate from the generated `PolyFun` +# umbrella; PolyFun backend adapters may import it explicitly. +[[lean_lib]] +name = "ToCslib" + # Test / worked-example library. Built by `lake test`, kept out of the # `lake lint` scope (which lints only `PolyFun`). Glob-based, so no umbrella # file is generated; the file-header style linter is relaxed on test files. From dc25dccee8528322c66c144721f5dd431cdaba23 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Fri, 28 Aug 2026 21:49:25 -0700 Subject: [PATCH 2/6] feat(tocslib): encode optional variable-width values --- PolyFunTest/ToCslib/Basic.lean | 4 ++++ ToCslib/Computability/BitEncoding.lean | 27 ++++++++++++++++++++++++++ 2 files changed, 31 insertions(+) diff --git a/PolyFunTest/ToCslib/Basic.lean b/PolyFunTest/ToCslib/Basic.lean index ade9037..2990b57 100644 --- a/PolyFunTest/ToCslib/Basic.lean +++ b/PolyFunTest/ToCslib/Basic.lean @@ -35,3 +35,7 @@ example {n index : ℕ} (hindex : index < n) (bit : Bool) (value : BitVec n) : example : Fintype.card (BitVec 2 → Bool) = 16 := by simpa using card_bitVec_fun 2 + +example (state : StrEncFam fun _ ↦ Bool) (parameter : ℕ) (value : Bool) : + state.option.enc parameter none ≠ state.option.enc parameter (some value) := by + simp diff --git a/ToCslib/Computability/BitEncoding.lean b/ToCslib/Computability/BitEncoding.lean index 78d9d3e..c9e950d 100644 --- a/ToCslib/Computability/BitEncoding.lean +++ b/ToCslib/Computability/BitEncoding.lean @@ -236,6 +236,33 @@ noncomputable def pairVar (s : StrEncFam σ) (e : BitEncFam β) : StrEncFam (fun @[simp] theorem pairVar_enc (s : StrEncFam σ) (e : BitEncFam β) (n : ℕ) (p : σ n × β n) : (s.pairVar e).enc n p = s.enc n p.1 ++ e.enc n p.2 := rfl +/-- Optional values for a variable-width encoding: `false` represents `none`, +while `true :: payload` represents `some payload`. -/ +noncomputable def option (s : StrEncFam σ) : StrEncFam (fun n => Option (σ n)) where + enc n + | none => [false] + | some value => true :: s.enc n value + enc_injective n left right equality := by + cases left <;> cases right <;> simp only [List.cons.injEq] at equality + · rfl + · exact absurd equality.1 (by simp) + · exact absurd equality.1 (by simp) + · exact congrArg some (s.enc_injective n equality.2) + bound := s.bound + .C 1 + len_le n value := by + cases value with + | none => simp + | some value => + have := s.len_le n value + simp only [List.length_cons, Polynomial.eval_add, Polynomial.eval_C] + omega + +@[simp] theorem option_enc_none (s : StrEncFam σ) (n : ℕ) : + s.option.enc n none = [false] := rfl + +@[simp] theorem option_enc_some (s : StrEncFam σ) (n : ℕ) (value : σ n) : + s.option.enc n (some value) = true :: s.enc n value := rfl + /-- Tag-bit sum of raw string encodings: `false ::` the left payload, `true ::` the right payload. The state shape of a two-phase (`⊕`-state) machine. -/ noncomputable def sum {τ : ℕ → Type u} (s₁ : StrEncFam σ) (s₂ : StrEncFam τ) : From 77cf2862e264a1991689321d23c3bcce1d9193bb Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Fri, 28 Aug 2026 22:01:28 -0700 Subject: [PATCH 3/6] feat(tocslib): add fixed-bit append machine --- PolyFunTest/ToCslib/Basic.lean | 3 + ToCslib.lean | 1 + ToCslib/Computability/SingleTape/Snoc.lean | 193 +++++++++++++++++++++ 3 files changed, 197 insertions(+) create mode 100644 ToCslib/Computability/SingleTape/Snoc.lean diff --git a/PolyFunTest/ToCslib/Basic.lean b/PolyFunTest/ToCslib/Basic.lean index 2990b57..265687a 100644 --- a/PolyFunTest/ToCslib/Basic.lean +++ b/PolyFunTest/ToCslib/Basic.lean @@ -39,3 +39,6 @@ example : Fintype.card (BitVec 2 → Bool) = 16 := by example (state : StrEncFam fun _ ↦ Bool) (parameter : ℕ) (value : Bool) : state.option.enc parameter none ≠ state.option.enc parameter (some value) := by simp + +example (input : List Bool) : + (EncPolyTime.appendBit id true).toFun input = input ++ [true] := rfl diff --git a/ToCslib.lean b/ToCslib.lean index 4d8a188..fc7ed86 100644 --- a/ToCslib.lean +++ b/ToCslib.lean @@ -8,6 +8,7 @@ module public import ToCslib.Computability.BitEncoding public import ToCslib.Computability.SingleTape.Counting +public import ToCslib.Computability.SingleTape.Snoc public import ToCslib.Data.BitVec /-! diff --git a/ToCslib/Computability/SingleTape/Snoc.lean b/ToCslib/Computability/SingleTape/Snoc.lean new file mode 100644 index 0000000..6bece8c --- /dev/null +++ b/ToCslib/Computability/SingleTape/Snoc.lean @@ -0,0 +1,193 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma, Elias Judin +-/ +module + +public import ToCslib.Computability.PolyTime + +/-! +# Appending a fixed bit with a single-tape machine + +This supplies the missing low-level string primitive needed to feed a fixed +encoded answer into a machine state. It is independent of PolyFun and oracle +semantics. The encoding-level API also records the additive description-size +bound for finite iteration; it makes no polynomial-time claim about an +iteration count that grows with the security parameter. +-/ + +@[expose] public section + +namespace Cslib.Turing.SingleTapeTM + +open Cslib.Turing Relation + +/-- Append `c` at the right end of the input and return the head to the first symbol. -/ +def snocComputer (c : Bool) : SingleTapeTM Bool where + State := Unit ⊕ Unit + q₀ := .inl () + tr q h := match q with + | .inl () => match h with + | some b => ⟨⟨some b, some .right⟩, some (.inl ())⟩ + | none => ⟨⟨some c, some .left⟩, some (.inr ())⟩ + | .inr () => match h with + | some b => ⟨⟨some b, some .left⟩, some (.inr ())⟩ + | none => ⟨⟨none, some .right⟩, none⟩ + +private def snocPush : StackTape Bool → List Bool → StackTape Bool + | left, [] => left + | left, bit :: tail => snocPush (StackTape.cons (some bit) left) tail + +@[simp] private lemma snocPush_nil (left : StackTape Bool) : snocPush left [] = left := rfl + +@[simp] private lemma snocPush_cons (left : StackTape Bool) (bit : Bool) (tail : List Bool) : + snocPush left (bit :: tail) = snocPush (StackTape.cons (some bit) left) tail := rfl + +private lemma stackTape_ext {left right : StackTape Bool} + (equality : left.toList = right.toList) : left = right := by + cases left + cases right + cases equality + rfl + +private lemma snocPush_toList (left : StackTape Bool) (input : List Bool) : + (snocPush left input).toList = input.reverse.map some ++ left.toList := by + induction input generalizing left with + | nil => simp + | cons bit tail induction => + rw [snocPush_cons, induction (StackTape.cons (some bit) left), + StackTape.cons_some_toList] + simp + +private lemma mk₁_eq (input : List Bool) : + (BiTape.mk₁ input : BiTape Bool) = + ⟨(StackTape.mapSome input).head, ∅, (StackTape.mapSome input).tail⟩ := by + cases input <;> rfl + +private lemma snocComputer_phaseA (c : Bool) (left : StackTape Bool) : + ∀ input : List Bool, + RelatesInSteps (snocComputer c).TransitionRelation + ⟨some (.inl ()), + ⟨(StackTape.mapSome input).head, left, (StackTape.mapSome input).tail⟩⟩ + ⟨some (.inl ()), ⟨none, snocPush left input, ∅⟩⟩ input.length := by + intro input + induction input generalizing left with + | nil => exact .refl _ + | cons bit tail induction => + refine .head _ (t' := (⟨some (.inl ()), + ⟨(StackTape.mapSome tail).head, StackTape.cons (some bit) left, + (StackTape.mapSome tail).tail⟩⟩ : (snocComputer c).Cfg)) _ _ ?_ ?_ + · rfl + · simpa using induction (StackTape.cons (some bit) left) + +private lemma snocComputer_phaseB (c : Bool) : + ∀ (input : List Bool) (right : StackTape Bool), + RelatesInSteps (snocComputer c).TransitionRelation + ⟨some (.inr ()), + ⟨(StackTape.mapSome input).head, (StackTape.mapSome input).tail, right⟩⟩ + ⟨none, ⟨(snocPush right input).head, ∅, (snocPush right input).tail⟩⟩ + (input.length + 1) := by + intro input + induction input with + | nil => intro right; exact .single rfl + | cons bit tail induction => + intro right + refine .head _ (t' := (⟨some (.inr ()), + ⟨(StackTape.mapSome tail).head, (StackTape.mapSome tail).tail, + StackTape.cons (some bit) right⟩⟩ : (snocComputer c).Cfg)) _ _ ?_ ?_ + · rfl + · simpa using induction (StackTape.cons (some bit) right) + +private lemma snocPush_empty (input : List Bool) : + snocPush (∅ : StackTape Bool) input = StackTape.mapSome input.reverse := by + apply stackTape_ext + rw [snocPush_toList] + simp [StackTape.mapSome] + +private lemma snocPush_final (c : Bool) (input : List Bool) : + snocPush (StackTape.cons (some c) ∅) input.reverse = + StackTape.mapSome (input ++ [c]) := by + apply stackTape_ext + rw [snocPush_toList, StackTape.cons_some_toList] + simp [StackTape.mapSome] + +/-- `snocComputer` outputs `input ++ [c]` within `2 * input.length + 2` steps. -/ +theorem snocComputer_outputsWithinTime (c : Bool) (input : List Bool) : + (snocComputer c).OutputsWithinTime input (input ++ [c]) (2 * input.length + 2) := by + have forward := snocComputer_phaseA c ∅ input + have backward := snocComputer_phaseB c input.reverse (StackTape.cons (some c) ∅) + rw [← snocPush_empty input, snocPush_final c input] at backward + have chain : + RelatesInSteps (snocComputer c).TransitionRelation + ⟨some (.inl ()), (BiTape.mk₁ input : BiTape Bool)⟩ + ⟨none, (BiTape.mk₁ (input ++ [c]) : BiTape Bool)⟩ + (input.length + (1 + (input.reverse.length + 1))) := by + rw [mk₁_eq input, mk₁_eq (input ++ [c])] + exact forward.trans ((RelatesInSteps.single (by rfl)).trans backward) + refine RelatesWithinSteps.of_le + (RelatesWithinSteps.of_relatesInSteps chain) ?_ + simp only [List.length_reverse] + omega + +/-- The exact linear-time witness for appending a fixed bit. -/ +def snocTimeComputable (c : Bool) : TimeComputable (fun input => input ++ [c]) where + tm := snocComputer c + timeBound n := 2 * n + 2 + outputsFunInTime input := snocComputer_outputsWithinTime c input + +/-- Appending a fixed bit is polynomial-time computable. -/ +noncomputable def snocPolyTimeComputable (c : Bool) : + PolyTimeComputable (fun input => input ++ [c]) where + toTimeComputable := snocTimeComputable c + poly := 2 * Polynomial.X + Polynomial.C 2 + bounds n := by simp [snocTimeComputable, two_mul] + +/-- The append machine has two states. -/ +theorem size_snocPolyTimeComputable (c : Bool) : + (snocPolyTimeComputable c).size ≤ 2 := by + change Fintype.card (Unit ⊕ Unit) ≤ 2 + simp + +end Cslib.Turing.SingleTapeTM + +namespace ToCslib.Computability.EncPolyTime + +open Cslib.Turing.SingleTapeTM + +/-- View the identity through an output encoding with one fixed bit appended. -/ +noncomputable def appendBit {σ : Type} (encoding : σ → List Bool) (c : Bool) : + EncPolyTime encoding (fun value => encoding value ++ [c]) _root_.id where + toFun input := input ++ [c] + polyTime := snocPolyTimeComputable c + map_encode _ := rfl + +/-- The append witness uses at most two states. -/ +theorem size_appendBit {σ : Type} (encoding : σ → List Bool) (c : Bool) : + (appendBit encoding c).size ≤ 2 := size_snocPolyTimeComputable c + +/-- A fixed finite iterate has description size at most one plus the sum of +the step-machine sizes. This is description accounting only: composing a +parameter-dependent number of polynomial-time machines is not asserted to +have a uniform polynomial running-time bound. -/ +theorem exists_iterate {σ : Type} (encoding : σ → List Bool) {step : σ → σ} + (stepCode : EncPolyTime encoding encoding step) : + ∀ count : ℕ, ∃ code : EncPolyTime encoding encoding (step^[count]), + code.size ≤ 1 + count * stepCode.size := by + intro count + induction count with + | zero => + refine ⟨(EncPolyTime.id encoding).copy (step^[0]) (fun state => ?_), ?_⟩ + · simp + · simp + | succ count induction => + obtain ⟨code, sizeBound⟩ := induction + refine ⟨(code.comp stepCode).copy (step^[count + 1]) (fun state => ?_), ?_⟩ + · exact (Function.iterate_succ_apply' step count state).symm + · rw [size_copy, size_comp] + have multiplication : + (count + 1) * stepCode.size = count * stepCode.size + stepCode.size := by + ring + omega + +end ToCslib.Computability.EncPolyTime From 673fdc8af50080f32ec2c989ba0e35ce2e325ddb Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Fri, 28 Aug 2026 22:15:57 -0700 Subject: [PATCH 4/6] fix(tocslib): pin encoding claims and lint root --- .github/workflows/ci.yml | 4 +++- ToCslib/Computability/BitEncoding.lean | 31 ++++++++++++++------------ ToCslib/Computability/PolyTime.lean | 9 ++++---- lakefile.toml | 2 +- scripts/validate.sh | 1 + 5 files changed, 27 insertions(+), 20 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 56f537e..55cde66 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -92,7 +92,9 @@ jobs: run: lake build --wfail - name: Run environment linters - run: lake lint + run: | + lake build ToCslib + lake lint test: name: Test diff --git a/ToCslib/Computability/BitEncoding.lean b/ToCslib/Computability/BitEncoding.lean index c9e950d..aff369f 100644 --- a/ToCslib/Computability/BitEncoding.lean +++ b/ToCslib/Computability/BitEncoding.lean @@ -10,17 +10,17 @@ public import Mathlib.Data.Nat.Bitwise public import Mathlib.Data.Nat.Log /-! -# Canonical Fixed-Width Bit Encodings and Uniform Machine Families +# Pinned Fixed-Width Bit Encodings and Uniform Machine Families -The canonical boundary representation for the polynomial-time adversary model, and the +The pinned boundary representation for the polynomial-time adversary model, and the reusable unit of machine-computability it consumes. -## Why fixed canonical encodings +## Why encodings must be pinned "Computable in polynomial time relative to *some* encoding" is vacuous: an encoding `enc x := std x ++ block (f x)` caches any function `f` inside the representation, and every machine witness degenerates to a projection. Polynomial time is only well-defined -relative to a *fixed canonical* representation (syntactic frameworks fix one implicitly +relative to a *fixed, trusted* representation (syntactic frameworks fix one implicitly through the programming language's value representation; a machine-grounded framework must fix it explicitly). This file provides that representation: @@ -29,10 +29,11 @@ must fix it explicitly). This file provides that representation: notion, the representation freedom left to a machine's internal state. * `ToCslib.Computability.BitEncFam` — the *fixed-width* refinement: at each parameter every value encodes to exactly `wid n` bits, with `wid` polynomially bounded. This is the - canonical *boundary* representation for inputs, outputs, and oracle interfaces. The - polynomial width bound is the formal content of the Katz–Lindell `1^n` convention: - all game values at parameter `n` have `poly(n)`-length representations, so - "polynomial in `n`" and "polynomial in the input length" agree. + pinned *boundary* representation for inputs, outputs, and oracle interfaces. The + structure does not itself certify that an encoding is canonical: call sites must pin + a trusted constructor or an explicitly reviewed encoding. Its polynomial width bound + ensures every boundary value has `poly(n)` length; machine-family bounds charge `n` + separately and therefore do not require the input width to grow with `n`. * Constructors: `BitEncFam.const` (fixed-width binary index encoding of a finite type), `BitEncFam.bitVec`/`bitVecX` (raw bits), `BitEncFam.pair` (append — widths are fixed, so no tags or alphabets are needed), `BitEncFam.option` (tag bit plus padded payload), @@ -92,14 +93,16 @@ structure StrEncFam (α : ℕ → Type u) : Type u where /-- All encodings respect the length bound. -/ len_le : ∀ n x, (enc n x).length ≤ bound.eval n -/-! ## Fixed-width canonical boundary encodings -/ +/-! ## Pinned fixed-width boundary encodings -/ -/-- A security-parameter-indexed family of **fixed-width** raw bit-string encodings: -the canonical boundary representation. At parameter `n` every value encodes to exactly +/-- A security-parameter-indexed family of **fixed-width** raw bit-string encodings. +At parameter `n` every value encodes to exactly `wid n` bits, and `wid` is polynomially bounded — the formal content of the -Katz–Lindell `1^n` convention. Fixed widths make pairing literal append and let the -split point of any concatenation be recovered positionally, with no alphabets, tags, -or self-delimiting machinery. -/ +security-parameter size convention used by this family model. Fixed widths make pairing +literal append and let the split point of any concatenation be recovered positionally, +with no alphabets, tags, or self-delimiting machinery. Fixed width alone does not rule +out a malicious encoding that caches a function value; sound statements pin a trusted +encoding rather than existentially selecting one. -/ structure BitEncFam (α : ℕ → Type u) : Type u where /-- The exact encoded width at each parameter. -/ wid : ℕ → ℕ diff --git a/ToCslib/Computability/PolyTime.lean b/ToCslib/Computability/PolyTime.lean index cda6e42..54b203e 100644 --- a/ToCslib/Computability/PolyTime.lean +++ b/ToCslib/Computability/PolyTime.lean @@ -68,10 +68,11 @@ theorem PolyTimeComputable.monotone_normalize_timeBound {f : List Symbol → Lis /-- The description size of a machine witness over the two-symbol tape alphabet: its number of states. Over the fixed `Bool` alphabet the transition table has exactly three -rows per state, so the state count measures the machine's description up to a constant -factor — the "advice" of a non-uniform family, and the quantity the machine-counting -bound `B` counts. Time bounds alone do not control it: a table machine looks up any -function on a finite domain in linear time using one state per valid input. +rows per state, and each target-state entry needs logarithmically many bits. Thus a +polynomial state-count bound is polynomially equivalent to a conventional transition- +table bit-size bound (rather than equal up to a constant factor). It is the advice +measure counted by `B`. Time bounds alone do not control it: a table machine looks up +any function on a finite domain in linear time using one state per valid input. Deliberately restricted to `Symbol := Bool`: over a family of growing alphabets the transition table has `Fintype.card Symbol + 1` rows per state, so a bare state count diff --git a/lakefile.toml b/lakefile.toml index b178df6..051ca2c 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -49,7 +49,7 @@ name = "PolyFun" name = "ToCslib" # Test / worked-example library. Built by `lake test`, kept out of the -# `lake lint` scope (which lints only `PolyFun`). Glob-based, so no umbrella +# `lake lint` scope (which lints `PolyFun` and `ToCslib`). Glob-based, so no umbrella # file is generated; the file-header style linter is relaxed on test files. [[lean_lib]] name = "PolyFunTest" diff --git a/scripts/validate.sh b/scripts/validate.sh index 03ef1ad..b91044f 100755 --- a/scripts/validate.sh +++ b/scripts/validate.sh @@ -70,6 +70,7 @@ python3 ./scripts/check-docs-integrity.py if (( run_lint )); then echo "" echo "# Running environment linters (lake lint)" + lake build ToCslib lake lint fi From 27d4cb427d0bc712590e546de82c7c2a2a23984d Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Fri, 28 Aug 2026 23:12:55 -0700 Subject: [PATCH 5/6] fix(tocslib): generalize family universes --- PolyFunTest/ToCslib/Basic.lean | 19 +++++++++++++++++++ ToCslib.lean | 4 ++-- ToCslib/Computability/BitEncoding.lean | 22 +++++++++++----------- scripts/validate.sh | 2 +- 4 files changed, 33 insertions(+), 14 deletions(-) diff --git a/PolyFunTest/ToCslib/Basic.lean b/PolyFunTest/ToCslib/Basic.lean index 265687a..7190466 100644 --- a/PolyFunTest/ToCslib/Basic.lean +++ b/PolyFunTest/ToCslib/Basic.lean @@ -42,3 +42,22 @@ example (state : StrEncFam fun _ ↦ Bool) (parameter : ℕ) (value : Bool) : example (input : List Bool) : (EncPolyTime.appendBit id true).toFun input = input ++ [true] := rfl + +/-! Mixed-universe canaries: encoding products and machine families do not require +their source and target families to live in the same universe. -/ + +noncomputable example (lower : BitEncFam fun _ ↦ Bool) + (higher : BitEncFam fun _ ↦ ULift.{1} Bool) : + BitEncFam (fun _ ↦ Bool × ULift.{1} Bool) := + lower.pair higher + +noncomputable example (lower : StrEncFam fun _ ↦ Bool) + (higher : BitEncFam fun _ ↦ ULift.{1} Bool) : + StrEncFam (fun _ ↦ Bool × ULift.{1} Bool) := + lower.pairVar higher + +example {α : ℕ → Type} {β : ℕ → Type 1} + {ea : (n : ℕ) → α n → List Bool} {eb : (n : ℕ) → β n → List Bool} + {f : (n : ℕ) → α n → β n} (witness : EncPolyTimeFam ea eb f) : + EncPolyTimeFam ea eb f := + witness diff --git a/ToCslib.lean b/ToCslib.lean index fc7ed86..ff9ed68 100644 --- a/ToCslib.lean +++ b/ToCslib.lean @@ -16,6 +16,6 @@ public import ToCslib.Data.BitVec This library contains reusable facts and constructions about cslib machines. It does not import PolyFun's realizability theory or any downstream oracle or -cryptographic semantics. Backend adapters in `PolyFun.Realizability.Backend` -may import these modules explicitly. +cryptographic semantics. Optional backend libraries may import these modules +explicitly without making cslib a dependency of generic PolyFun. -/ diff --git a/ToCslib/Computability/BitEncoding.lean b/ToCslib/Computability/BitEncoding.lean index aff369f..8c98952 100644 --- a/ToCslib/Computability/BitEncoding.lean +++ b/ToCslib/Computability/BitEncoding.lean @@ -53,7 +53,7 @@ bit-lengths the polynomial bounds speak about. @[expose] public section -universe u +universe u v w u' v' open Cslib.Turing.SingleTapeTM @@ -119,7 +119,7 @@ structure BitEncFam (α : ℕ → Type u) : Type u where namespace BitEncFam -variable {α β : ℕ → Type u} +variable {α : ℕ → Type u} {β : ℕ → Type v} /-- Forget the fixed width, keeping the polynomial length bound. -/ def toStrEncFam (e : BitEncFam α) : StrEncFam α where @@ -220,7 +220,7 @@ end BitEncFam namespace StrEncFam -variable {σ β : ℕ → Type u} +variable {σ : ℕ → Type u} {β : ℕ → Type v} /-- Pair a variable-width encoding with a fixed-width one by append: injective because the fixed-width right component determines the split point from the right. This is the @@ -268,7 +268,7 @@ noncomputable def option (s : StrEncFam σ) : StrEncFam (fun n => Option (σ n)) /-- Tag-bit sum of raw string encodings: `false ::` the left payload, `true ::` the right payload. The state shape of a two-phase (`⊕`-state) machine. -/ -noncomputable def sum {τ : ℕ → Type u} (s₁ : StrEncFam σ) (s₂ : StrEncFam τ) : +noncomputable def sum {τ : ℕ → Type v} (s₁ : StrEncFam σ) (s₂ : StrEncFam τ) : StrEncFam (fun n => σ n ⊕ τ n) where enc n := Sum.elim (fun x => false :: s₁.enc n x) (fun y => true :: s₂.enc n y) enc_injective n x y h := by @@ -289,17 +289,17 @@ noncomputable def sum {τ : ℕ → Type u} (s₁ : StrEncFam σ) (s₂ : StrEnc simp only [Sum.elim_inr, List.length_cons, Polynomial.eval_add, Polynomial.eval_C] omega -@[simp] theorem sum_enc_inl {τ : ℕ → Type u} (s₁ : StrEncFam σ) (s₂ : StrEncFam τ) +@[simp] theorem sum_enc_inl {τ : ℕ → Type v} (s₁ : StrEncFam σ) (s₂ : StrEncFam τ) (n : ℕ) (x : σ n) : (s₁.sum s₂).enc n (Sum.inl x) = false :: s₁.enc n x := rfl -@[simp] theorem sum_enc_inr {τ : ℕ → Type u} (s₁ : StrEncFam σ) (s₂ : StrEncFam τ) +@[simp] theorem sum_enc_inr {τ : ℕ → Type v} (s₁ : StrEncFam σ) (s₂ : StrEncFam τ) (n : ℕ) (y : τ n) : (s₁.sum s₂).enc n (Sum.inr y) = true :: s₂.enc n y := rfl end StrEncFam namespace BitEncFam -variable {γ : ℕ → Type u} {σ : ℕ → Type u} +variable {γ : ℕ → Type u} {σ : ℕ → Type v} /-- Pair a fixed-width encoding on the left with a variable-width one on the right by append — the mirror of `StrEncFam.pairVar`. Injective because the fixed-width left @@ -349,9 +349,9 @@ combinators compose them, and an adversary's four step functions each carry one. Like `EncPolyTime`, the structure imposes nothing on the encodings themselves; its certifying power comes from the call site pinning the injective families (`ToCslib.Computability.BitEncFam`, `ToCslib.Computability.StrEncFam`). -/ -structure EncPolyTimeFam {α β : ℕ → Type u} +structure EncPolyTimeFam {α : ℕ → Type u} {β : ℕ → Type v} (ea : (n : ℕ) → α n → List Bool) (eb : (n : ℕ) → β n → List Bool) - (f : (n : ℕ) → α n → β n) : Type (u + 1) where + (f : (n : ℕ) → α n → β n) : Type (max (u + 1) (v + 1)) where /-- The machine witness at each parameter. -/ wit : (n : ℕ) → EncPolyTime (ea n) (eb n) (f n) /-- Uniform polynomial bound on running times, in `n` plus the input length. -/ @@ -365,7 +365,7 @@ structure EncPolyTimeFam {α β : ℕ → Type u} namespace EncPolyTimeFam -variable {α β γ : ℕ → Type u} +variable {α : ℕ → Type u} {β : ℕ → Type v} {γ : ℕ → Type w} {ea : (n : ℕ) → α n → List Bool} {eb : (n : ℕ) → β n → List Bool} {ec : (n : ℕ) → γ n → List Bool} @@ -373,7 +373,7 @@ variable {α β γ : ℕ → Type u} time polynomial, and advice bound are untouched (`EncPolyTime.recode` per parameter). The workhorse for pure re-bracketings of encoded data — `cons`/append associativity and pair/sum reshuffles cost no machine content. -/ -def recode {α' β' : ℕ → Type u} {ea' : (n : ℕ) → α' n → List Bool} +def recode {α' : ℕ → Type u'} {β' : ℕ → Type v'} {ea' : (n : ℕ) → α' n → List Bool} {eb' : (n : ℕ) → β' n → List Bool} {f : (n : ℕ) → α n → β n} (h : EncPolyTimeFam ea eb f) (φ : (n : ℕ) → α' n → α n) (g : (n : ℕ) → α' n → β' n) (hin : ∀ n x, ea' n x = ea n (φ n x)) diff --git a/scripts/validate.sh b/scripts/validate.sh index b91044f..c849162 100755 --- a/scripts/validate.sh +++ b/scripts/validate.sh @@ -87,7 +87,7 @@ if (( run_axioms )); then echo "" echo "# Enforcing zero axiom/sorry debt" - lake exe polyfun-axiomsweep --check + lake exe polyfun-axiomsweep --root PolyFun --root ToCslib --check fi echo "" From b2fb3e760e58576b454f92cd71f3b9e3a7070ec9 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Fri, 28 Aug 2026 23:22:18 -0700 Subject: [PATCH 6/6] ci: build axiom sweep roots --- scripts/validate.sh | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/scripts/validate.sh b/scripts/validate.sh index c849162..532e987 100755 --- a/scripts/validate.sh +++ b/scripts/validate.sh @@ -81,6 +81,10 @@ if (( run_test )); then fi if (( run_axioms )); then + echo "" + echo "# Building axiom sweep roots" + lake build PolyFun ToCslib + echo "" echo "# Testing the axiom sweep tool" ./scripts/test-axiomsweep.sh