diff --git a/.agents/skills/lean-abstract/SKILL.md b/.agents/skills/lean-abstract/SKILL.md index 4dcb37ca1..dd6b9a132 100644 --- a/.agents/skills/lean-abstract/SKILL.md +++ b/.agents/skills/lean-abstract/SKILL.md @@ -47,6 +47,9 @@ This requirement applies transitively: an alias or wrapper around an internal de - **Prefer ordinary types and quantifiers**: Prefer functions, `List`, `Fin n → α`, quantifiers, membership, and equalities over custom interfaces, typeclasses, or implementation-specific dependent records. - **Use `Fin n → α` for homogeneous tuples**: For more than two homogeneous components, prefer `Fin n → α` over nested cross products, with short descriptive aliases for indices. - **Explicit encodings**: When a theorem depends on a binary encoding (such as `encCNF` or binary tree encodings), either spell out the encoding combinators (`frame`, `encodePair`, `encodeList`, `Nat.bits`) directly in the abstract or explicitly allow the foundational encoding module. When packaging an encoding function `encodeX : X → List Bool` into an embedding `def encX : X ↪ List Bool := ⟨encodeX, encodeX_injective⟩`, declare `theorem encodeX_injective : Function.Injective encodeX := Bridge.encodeX_injective` as a local `theorem` before `def encX`: `#check_abstract` traverses the `value?` of non-theorem `def`s and stops at `theorem` proof boundaries, and `scripts/abstract_to_tex.py` elides undocumented `*_injective` helper theorems following a definition block (and only those). +- **Share foundations, keep semantics visible**: Use the small audited `ComplexityAbstracts.Encoding` and `ComplexityAbstracts.Computation` modules for common serialization and polynomial-time conventions. Keep complexity-class, game and problem definitions in each abstract. Import every used foundation explicitly, allow it in `#check_abstract`, and list the complete foundation import closure in the catalogue entry's `foundations`. The renderer includes these definitions in each standalone PDF and once at the end of the combined catalogue. +- **Lead with the mathematics**: Put encoding and machine representation details in a `## Representation details` module-doc section. The renderer moves that section and its following declarations to an appendix, ending at the next level-two section. Do not put headline or selected supporting theorems there. Explain every resource-significant convention in the main text, including unary versus binary sizes, uniformity and clock semantics. Moving a definition does not excuse hiding its meaning. +- **Migrate clients to canonical names**: Extract shared definitions without deprecated aliases and update all in-repository clients, following `AGENTS.md`. - **State plain machine bounds where possible**: `Complexitylib` uses `ComputableTidilyInPolyTime` internally for compositional closure (`@[fun_prop]`), and proves it equivalent to plain upstream `Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength` with `Cslib.PolynomiallyBounded`. Using the plain upstream notion in the abstract lets a reader verify the theorem statement without needing to inspect tidy-machine invariants. --- @@ -78,7 +81,7 @@ Start each conceptual block's docstring (`/-- ... -/` or `/-! ... -/`) with a co - Explain unfamiliar `Mathlib` or `Cslib` predicates (e.g., `Nat.bits`, `Function.Embedding`, `Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength`) by their mathematical meaning before naming the Lean symbol. - State totality, halting, and answer-preservation guarantees explicitly when describing reductions or verifiers. -- In the module docstring (`/-! # ... -/`), explain that a reader only needs to inspect the definitions and theorem statements in `*Abstract.lean` to verify that the formalization proves the intended mathematical claim; Lean verifies the proofs through `*Bridge.lean` and `#check_abstract` audits the dependency boundary. +- In the module docstring (`/-! # ... -/`), explain that a reader only needs to inspect the definitions and theorem statements in `*Abstract.lean` and its displayed shared foundations to verify that the formalization proves the intended mathematical claim; Lean verifies the proofs through `*Bridge.lean` and `#check_abstract` audits the dependency boundary. --- @@ -117,9 +120,9 @@ Start each conceptual block's docstring (`/-- ... -/` or `/-! ... -/`) with a co Consult these concrete implementations in `abstracts/ComplexityAbstracts/`: -- **Pattern A (Unfolded types, zero `Complexity.*` dependencies)**: +- **Pattern A (Unfolded types, shared audited foundations)**: [CookLevinAbstract.lean](../../../abstracts/ComplexityAbstracts/CookLevinAbstract.lean) and [CookLevinBridge.lean](../../../abstracts/ComplexityAbstracts/CookLevinBridge.lean) (`SAT` and `ExactThreeSAT` are `NP`-complete, `UNSAT` is `coNP`-complete). -- **Pattern B (Fresh `inductive` syntax + polymorphic `Presentation` / `Laws`, zero `Complexity.*` dependencies)**: +- **Pattern B (Fresh `inductive` syntax + polymorphic `Presentation` / `Laws`, shared audited foundations)**: [TQBFAbstract.lean](../../../abstracts/ComplexityAbstracts/TQBFAbstract.lean) and [TQBFBridge.lean](../../../abstracts/ComplexityAbstracts/TQBFBridge.lean) (`TQBF` is `PSPACE`-complete). - **Pattern A reusing another bridge**: [SubsetSumAbstract.lean](../../../abstracts/ComplexityAbstracts/SubsetSumAbstract.lean) and [SubsetSumBridge.lean](../../../abstracts/ComplexityAbstracts/SubsetSumBridge.lean) (`SubsetSum` is `NP`-complete with numbers in binary; the bridge reuses the plain `NP` transfer lemmas of `CookLevinBridge`). diff --git a/ComplexityTests.lean b/ComplexityTests.lean index c588ffe5d..56a1b7075 100644 --- a/ComplexityTests.lean +++ b/ComplexityTests.lean @@ -2,6 +2,7 @@ import ComplexityTests.AWPPAmplification import ComplexityTests.AWPPLowness import ComplexityTests.Abstracts.All import ComplexityTests.Abstracts.CheckTests +import ComplexityTests.Abstracts.InputLayouts import ComplexityTests.AdaptivePPT import ComplexityTests.Advice import ComplexityTests.AffineController diff --git a/ComplexityTests/Abstracts/InputLayouts.lean b/ComplexityTests/Abstracts/InputLayouts.lean new file mode 100644 index 000000000..a6482fe4b --- /dev/null +++ b/ComplexityTests/Abstracts/InputLayouts.lean @@ -0,0 +1,53 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +-- upstream: local-only (formal abstract regression tests) + +import ComplexityAbstracts.FormulaBoundsAbstract +import ComplexityAbstracts.USTCONAbstract + +/-! # Input layout checks for the Andreev and undirected-connectivity abstracts -/ + +namespace ComplexityTests.Abstracts.InputLayouts + +open FormulaBoundsAbstract + +-- Coordinate zero is the least significant address bit. +example : tableIndex 3 ![true, true, false] = 3 := by decide + +-- The first bit of the second block follows the four table bits and the first block. +example (x : Fin 10 → Bool) : blockInput (b := 2) (m := 3) x 1 0 = x 7 := + blockInput_eq (b := 2) (m := 3) x 1 0 7 rfl + +-- Block parities are (true, false), so the answer is table entry one. +example : andreev 2 2 ![false, true, false, false, true, false, true, true] = true := by + decide + +-- Empty addresses and empty blocks both select the first table entry. +example (x : Fin 1 → Bool) : andreev 0 3 x = x 0 := rfl + +example (x : Fin 4 → Bool) : andreev 2 0 x = x 0 := rfl + +private def singleton : USTCONAbstract.Instance := + ⟨1, ⟨⟨fun _ _ => false, by simp⟩, 0, 0⟩⟩ + +private def edgeWithIsolatedVertex : USTCONAbstract.Instance := + ⟨3, ⟨⟨fun a b => decide (a.val + b.val = 1), by decide⟩, 0, 2⟩⟩ + +-- The smallest valid instance has a one-bit matrix and coincident endpoints. +example : USTCONAbstract.encode singleton = [true, false, false, false, false] := by decide + +example : singleton ∈ USTCONAbstract.USTCON := SimpleGraph.Reachable.refl _ + +-- Vertices zero and one are adjacent; vertex two is isolated. Headers name endpoints zero and two. +example : USTCONAbstract.encode edgeWithIsolatedVertex = + [true, true, true, false, false, true, true, false, + false, true, false, true, false, false, false, false, false] := by decide + +-- An endpoint rules out a zero-vertex instance. +example (I : USTCONAbstract.Instance) : 0 < I.vertexCount := Fin.pos I.source + +end ComplexityTests.Abstracts.InputLayouts diff --git a/abstracts/ComplexityAbstracts.lean b/abstracts/ComplexityAbstracts.lean index 194edb1e1..c86006020 100644 --- a/abstracts/ComplexityAbstracts.lean +++ b/abstracts/ComplexityAbstracts.lean @@ -1,12 +1,14 @@ import ComplexityAbstracts.BarringtonAbstract import ComplexityAbstracts.BarringtonBridge import ComplexityAbstracts.Check +import ComplexityAbstracts.Computation import ComplexityAbstracts.ConstantDepthAbstract import ComplexityAbstracts.ConstantDepthBridge import ComplexityAbstracts.CookLevinAbstract import ComplexityAbstracts.CookLevinBridge import ComplexityAbstracts.CryptographyAbstract import ComplexityAbstracts.CryptographyBridge +import ComplexityAbstracts.Encoding import ComplexityAbstracts.FaginAbstract import ComplexityAbstracts.FaginBridge import ComplexityAbstracts.FormulaBoundsAbstract diff --git a/abstracts/ComplexityAbstracts/BarringtonAbstract.lean b/abstracts/ComplexityAbstracts/BarringtonAbstract.lean index ca2b92494..372243dfd 100644 --- a/abstracts/ComplexityAbstracts/BarringtonAbstract.lean +++ b/abstracts/ComplexityAbstracts/BarringtonAbstract.lean @@ -32,7 +32,10 @@ Lean checks the bridge proof and `#check_abstract` audits the statement boundary namespace ComplexityTests.Abstracts.BarringtonAbstract /-- A nonuniform NC¹ language has a polynomial-size De Morgan circuit at each input length, -with depth at most a constant times `floor(log₂ n)+1`. Every gate, constants included, costs one. -/ +with depth at most a constant times `floor(log₂ n)+1`. Every gate, constants included, costs one. +Here `L : Language Bool` is a set of finite bit strings. `L.slice n x` tests whether the word +`List.ofFn x` belongs to `L`; `single` makes that Boolean the sole circuit output, and `Computes` +requires agreement on every input. -/ def InNC1 (L : Language Bool) : Prop := ∃ (c : ℕ) (size : ℕ → ℕ), Cslib.PolynomiallyBounded size ∧ ∀ n, ∃ C : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature n 1, @@ -43,7 +46,8 @@ def InNC1 (L : Language Bool) : Prop := /-- A width-five permutation program reads one input bit per instruction, selects one of two permutations, and multiplies the selected permutations in instruction order. The elementary `MonoidProgram` model is explicitly allowed; it is a list of `(position, selection function)` -instructions. Its length is polynomial and its final permutation is tested against a set. -/ +instructions. Its length is polynomial. Both the program and the acceptance set may depend on +input length; acceptance tests the entire final permutation. -/ def HasWidthFivePrograms (L : Language Bool) : Prop := ∃ size : ℕ → ℕ, Cslib.PolynomiallyBounded size ∧ ∀ n, ∃ (P : Cslib.BranchingPrograms.MonoidProgram (Fin n) Bool (Equiv.Perm (Fin 5))) diff --git a/abstracts/ComplexityAbstracts/BarringtonBridge.lean b/abstracts/ComplexityAbstracts/BarringtonBridge.lean index efd9553c9..97c1abd8b 100644 --- a/abstracts/ComplexityAbstracts/BarringtonBridge.lean +++ b/abstracts/ComplexityAbstracts/BarringtonBridge.lean @@ -13,7 +13,10 @@ import Complexity.Computability.Circuit.Boolean.BarringtonClass namespace ComplexityTests.Abstracts.BarringtonBridge /-- A nonuniform NC¹ language has a polynomial-size De Morgan circuit at each input length, -with depth at most a constant times `floor(log₂ n)+1`. Every gate, constants included, costs one. -/ +with depth at most a constant times `floor(log₂ n)+1`. Every gate, constants included, costs one. +Here `L : Language Bool` is a set of finite bit strings. `L.slice n x` tests whether the word +`List.ofFn x` belongs to `L`; `single` makes that Boolean the sole circuit output, and `Computes` +requires agreement on every input. -/ def InNC1 (L : Language Bool) : Prop := ∃ (c : ℕ) (size : ℕ → ℕ), Cslib.PolynomiallyBounded size ∧ ∀ n, ∃ C : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature n 1, @@ -24,7 +27,8 @@ def InNC1 (L : Language Bool) : Prop := /-- A width-five permutation program reads one input bit per instruction, selects one of two permutations, and multiplies the selected permutations in instruction order. The elementary `MonoidProgram` model is explicitly allowed; it is a list of `(position, selection function)` -instructions. Its length is polynomial and its final permutation is tested against a set. -/ +instructions. Its length is polynomial. Both the program and the acceptance set may depend on +input length; acceptance tests the entire final permutation. -/ def HasWidthFivePrograms (L : Language Bool) : Prop := ∃ size : ℕ → ℕ, Cslib.PolynomiallyBounded size ∧ ∀ n, ∃ (P : Cslib.BranchingPrograms.MonoidProgram (Fin n) Bool (Equiv.Perm (Fin 5))) diff --git a/abstracts/ComplexityAbstracts/Computation.lean b/abstracts/ComplexityAbstracts/Computation.lean new file mode 100644 index 000000000..3f889a846 --- /dev/null +++ b/abstracts/ComplexityAbstracts/Computation.lean @@ -0,0 +1,45 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +-- upstream: local-only (formal abstract foundations) + +import ComplexityAbstracts.Check +import ComplexityAbstracts.Encoding +import Cslib.Computability.Machines.Turing.MultiTape.Deterministic +import Cslib.Foundations.Data.Nat.PolynomialBound + +/-! # Polynomial-time functions and verifiers + +One deterministic binary multi-tape Turing machine, with finitely many states, computes the +function on every encoded input. Its time and work space are polynomially bounded in input bit +length. Input is read-only and output is write-only. The machine is uniform: its code and its +bounds are fixed before the input is chosen. No condition is imposed on words outside an +encoding's image. + +A verifier receives an instance and a certificate. Its running time is polynomial in their +combined encoded length, not just the instance length. The pair encoding has length +`2 * |enc x| + 1 + |w|`, so it gives the usual polynomial bound in `|enc x| + |w|`. +-/ + +namespace ComplexityTests.Abstracts.Computation + +/-- Total polynomial-time computation on encoded inputs, with explicit time and space bounds. -/ +def PolyTime {α β : Type} (f : α → β) (a : α ↪ List Bool) (b : β ↪ List Bool) : Prop := + ∃ t s : ℕ → ℕ, Cslib.PolynomiallyBounded t ∧ Cslib.PolynomiallyBounded s ∧ + Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength f a b t s + +/-- One total polynomial-time deterministic verifier, on an instance and a binary certificate. -/ +def PolyTimeVerifier {α : Type} (enc : α ↪ List Bool) (V : α × List Bool → Bool) : Prop := + PolyTime V (Encoding.encPair enc Encoding.encBits) Encoding.encBool + +end ComplexityTests.Abstracts.Computation + +/-- +info: abstract audit passed for `ComplexityTests.Abstracts.Computation`: +2 root declarations, 33 dependencies checked +-/ +#guard_msgs (whitespace := lax) in +#check_abstract ComplexityTests.Abstracts.Computation allowing [ComplexityAbstracts.Encoding] diff --git a/abstracts/ComplexityAbstracts/ConstantDepthAbstract.lean b/abstracts/ComplexityAbstracts/ConstantDepthAbstract.lean index 945b00d9b..38bfe54d5 100644 --- a/abstracts/ComplexityAbstracts/ConstantDepthAbstract.lean +++ b/abstracts/ComplexityAbstracts/ConstantDepthAbstract.lean @@ -44,7 +44,9 @@ abbrev ACBasis := Cslib.Circuits.Boolean.Unbounded.signature def meaning : Cslib.Circuits.Interpretation ACBasis Bool := Cslib.Circuits.Boolean.Unbounded.interpretation -/-- Charge one for AND/OR, including their nullary constant cases; negations are free. -/ +/-- Depth charges one for AND/OR, including their nullary constant cases, and zero for NOT. +This weight affects depth only: `C.size` counts every operation gate, including NOT and +constants. -/ def andOrCost : Cslib.Circuits.Boolean.Unbounded.Op → ℕ | .not => 0 | .and _ | .or _ => 1 @@ -57,7 +59,7 @@ def modularMeaning (p : ℕ) : /-- **Håstad.** A parity circuit of AND/OR depth at most `d` needs `2^s` gates whenever `s ≥ 2` and `17s(16s+1)^(d-2) ≤ n`. Subtraction is in naturals. This gives the sharp exponent -`1/(d-1)` for every fixed `d ≥ 2`; negations cost zero in the depth bound. -/ +`1/(d-1)` for every fixed `d ≥ 2`. Negations cost zero in depth and one gate in size. -/ theorem hastad {n d s : ℕ} (C : Cslib.Circuits.Circuit ACBasis n 1) (correct : ∀ x, C.eval meaning x 0 = parity n x) (hs : 2 ≤ s) (depth : C.depthWith andOrCost ≤ d) (budget : 17 * s * (16 * s + 1) ^ (d - 2) ≤ n) : diff --git a/abstracts/ComplexityAbstracts/ConstantDepthBridge.lean b/abstracts/ComplexityAbstracts/ConstantDepthBridge.lean index 1d7685b5f..8d04dbc8d 100644 --- a/abstracts/ComplexityAbstracts/ConstantDepthBridge.lean +++ b/abstracts/ComplexityAbstracts/ConstantDepthBridge.lean @@ -25,7 +25,9 @@ abbrev ACBasis := Cslib.Circuits.Boolean.Unbounded.signature def meaning : Cslib.Circuits.Interpretation ACBasis Bool := Cslib.Circuits.Boolean.Unbounded.interpretation -/-- Charge one for AND/OR, including their nullary constant cases; negations are free. -/ +/-- Depth charges one for AND/OR, including their nullary constant cases, and zero for NOT. +This weight affects depth only: `C.size` counts every operation gate, including NOT and +constants. -/ def andOrCost : Cslib.Circuits.Boolean.Unbounded.Op → ℕ | .not => 0 | .and _ | .or _ => 1 @@ -38,7 +40,7 @@ def modularMeaning (p : ℕ) : /-- **Håstad.** A parity circuit of AND/OR depth at most `d` needs `2^s` gates whenever `s ≥ 2` and `17s(16s+1)^(d-2) ≤ n`. Subtraction is in naturals. This gives the sharp exponent -`1/(d-1)` for every fixed `d ≥ 2`; negations cost zero in the depth bound. -/ +`1/(d-1)` for every fixed `d ≥ 2`. Negations cost zero in depth and one gate in size. -/ theorem hastad {n d s : ℕ} (C : Cslib.Circuits.Circuit ACBasis n 1) (correct : ∀ x, C.eval meaning x 0 = parity n x) (hs : 2 ≤ s) (depth : C.depthWith andOrCost ≤ d) (budget : 17 * s * (16 * s + 1) ^ (d - 2) ≤ n) : diff --git a/abstracts/ComplexityAbstracts/CookLevinAbstract.lean b/abstracts/ComplexityAbstracts/CookLevinAbstract.lean index 5e4863397..f68fae2f3 100644 --- a/abstracts/ComplexityAbstracts/CookLevinAbstract.lean +++ b/abstracts/ComplexityAbstracts/CookLevinAbstract.lean @@ -7,6 +7,8 @@ Authors: Samuel Schlesinger -- upstream: local-only (formal abstract library) import ComplexityAbstracts.Check +import ComplexityAbstracts.Encoding +import ComplexityAbstracts.Computation import ComplexityAbstracts.CookLevinBridge /-! # Cook–Levin: satisfiability captures efficient verification @@ -20,7 +22,7 @@ Thus SAT is NP-complete, and its complement UNSAT is coNP-complete. The definitions below specify CNF formulas, their binary encoding, total polynomial-time reductions and native finite-state machine bounds. The claims are about asymptotic complexity, not a fast practical SAT solver. Lean checks the bridge proofs; `#check_abstract` checks that the -statements use only the definitions here and upstream mathematical and machine foundations. +statements use the definitions here, the displayed shared foundations, and upstream mathematics. ## References @@ -66,77 +68,34 @@ has length 3 (repeated literals within a clause are permitted). -/ def ExactThreeSAT : Set Formula := {φ | (∀ c ∈ φ, c.length = 3) ∧ Satisfiable φ} -/-! ## Binary encoding convention +/-! ## Representation details -Values are encoded injectively as bitstrings (`List Bool`). A bitstring `w` is -framed by encoding each bit `b` as `[true, b]` and appending `[false]`, making -framed bitstrings self-delimiting under concatenation. Pairs frame the first -component before appending the second, and lists concatenate the framed -encodings of their elements. Natural numbers use Mathlib's canonical -little-endian binary digits `Nat.bits` (`0 ↦ []`, positive `n` with least -significant bit first and final bit `true`). +CNF formulas are lists of clauses with binary variable indices. The following fixed encoding +uses the common framing conventions in the appendix. -/ -/-- Frame a bitstring: write each bit `b` as `[true, b]`, then terminate with `[false]`. -/ -def frame (w : List Bool) : List Bool := - w.flatMap (fun b => [true, b]) ++ [false] - -/-- Encode a pair by framing the encoding of its first component and appending the encoding of -its second component. -/ -def encodePair {α β : Type} (encA : α → List Bool) (encB : β → List Bool) (p : α × β) : - List Bool := - frame (encA p.1) ++ encB p.2 - -/-- Encode a list by concatenating the framed encodings of its elements. -/ -def encodeList {α : Type} (enc : α → List Bool) (l : List α) : List Bool := - l.flatMap (frame ∘ enc) - /-- Encode a CNF formula as a list of clauses, each a list of literals `(v, b)` encoded as the pair of `Nat.bits v` and the one-bit word `[b]`. -/ def encodeCNF : Formula → List Bool := - encodeList (encodeList (encodePair Nat.bits (fun b => [b]))) - -theorem encodePair_injective {α β : Type} (encA : α ↪ List Bool) (encB : β ↪ List Bool) : - Function.Injective (encodePair encA encB) := - CookLevinBridge.encodePair_injective encA encB + Encoding.encodeList (Encoding.encodeList (Encoding.encodePair Nat.bits (fun b => [b]))) theorem encodeCNF_injective : Function.Injective encodeCNF := CookLevinBridge.encodeCNF_injective -/-- Injective encoding of bitstrings as themselves. -/ -def encBits : List Bool ↪ List Bool := Function.Embedding.refl _ - -/-- Injective encoding of a single Boolean as a one-bit word `[b]`. -/ -def encBool : Bool ↪ List Bool := - ⟨fun b => [b], by intro a b h; injection h⟩ - -/-- Injective framed encoding of pairs. -/ -def encPair {α β : Type} (encA : α ↪ List Bool) (encB : β ↪ List Bool) : α × β ↪ List Bool := - ⟨encodePair encA encB, encodePair_injective encA encB⟩ - /-- Injective framed binary encoding of CNF formulas. -/ def encCNF : Formula ↪ List Bool := ⟨encodeCNF, encodeCNF_injective⟩ -/-! ## Polynomial-time computability, NP, coNP, and completeness +/-! ## Efficient verification and reductions -In upstream `Cslib`, `Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength f encA encB t s` -means that there exists a deterministic multi-tape Turing machine with a binary -tape alphabet and finitely many states that halts on every encoded input -`encA a` within `t (encA a).length` steps and `s (encA a).length` work-tape -cells, leaving `encB (f a)` on its output tape. `Cslib.PolynomiallyBounded` -asserts that a growth bound `ℕ → ℕ` is bounded above by a polynomial. +`Computation.PolyTimeVerifier enc V` means that one deterministic machine halts on every +instance/certificate pair in polynomial time in their combined bit length. The machine and +polynomial bound are fixed for the problem. We use certificates of exactly `p(|enc a|)` bits; +this is the fixed-length certificate convention. `Computation.PolyTime` is the same total +computation contract for general input and output encodings. Their definitions are in the +foundations appendix. -/ -/-- A total function `f : α → β` is computable in polynomial time with respect -to input encoding `encA` and output encoding `encB` if some deterministic -multi-tape binary Turing machine computes it within polynomially bounded time -and space in the input bit length. -/ -def ComputableInPolyTime {α β : Type} (f : α → β) - (encA : α ↪ List Bool) (encB : β ↪ List Bool) : Prop := - ∃ t s : ℕ → ℕ, Cslib.PolynomiallyBounded t ∧ Cslib.PolynomiallyBounded s ∧ - Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength f encA encB t s - /-- A function `V : α × List Bool → Bool` verifies a decision problem `A` with certificate length polynomial `p` if an instance `a` belongs to `A` exactly when there is a binary certificate `w` of length `p(|enc a|)` accepted by `V`. -/ @@ -149,7 +108,7 @@ problems that have a polynomial-time verifier with polynomially long binary certificates. -/ def NP {α : Type} (enc : α ↪ List Bool) : Set (Set α) := {A | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), - ComputableInPolyTime V (encPair enc encBits) encBool ∧ IsVerifier enc p V A} + Computation.PolyTimeVerifier enc V ∧ IsVerifier enc p V A} /-- The class coNP consists of decision problems whose complements belong to NP. -/ def coNP {α : Type} (enc : α ↪ List Bool) : Set (Set α) := @@ -160,7 +119,7 @@ problem `B` (with encoding `encB`) if a polynomial-time computable map `f` preserves yes/no membership on every instance. -/ def PolyTimeReducible {α β : Type} (encA : α ↪ List Bool) (encB : β ↪ List Bool) (A : Set α) (B : Set β) : Prop := - ∃ f : α → β, ComputableInPolyTime f encA encB ∧ ∀ a, a ∈ A ↔ f a ∈ B + ∃ f : α → β, Computation.PolyTime f encA encB ∧ ∀ a, a ∈ A ↔ f a ∈ B /-- A problem `B` is NP-complete if it belongs to NP and every NP problem (over any instance type `α` and injective binary encoding `encA`) reduces to `B` in @@ -196,10 +155,12 @@ theorem exactThreeSAT_npComplete : NPComplete encCNF ExactThreeSAT := CookLevinBridge.exactThreeSAT_npComplete /-- -info: abstract audit passed for `ComplexityTests.Abstracts.CookLevinAbstract`: 28 root -declarations, 68 dependencies checked +info: abstract audit passed for `ComplexityTests.Abstracts.CookLevinAbstract`: +19 root declarations, 69 dependencies checked -/ #guard_msgs (whitespace := lax) in -#check_abstract ComplexityTests.Abstracts.CookLevinAbstract +#check_abstract ComplexityTests.Abstracts.CookLevinAbstract allowing [ + ComplexityAbstracts.Encoding, ComplexityAbstracts.Computation +] end ComplexityTests.Abstracts.CookLevinAbstract diff --git a/abstracts/ComplexityAbstracts/CryptographyAbstract.lean b/abstracts/ComplexityAbstracts/CryptographyAbstract.lean index 0e6079a26..943c993fc 100644 --- a/abstracts/ComplexityAbstracts/CryptographyAbstract.lean +++ b/abstracts/ComplexityAbstracts/CryptographyAbstract.lean @@ -7,6 +7,8 @@ Authors: Samuel Schlesinger -- upstream: local-only (formal abstract library) import ComplexityAbstracts.Check +import ComplexityAbstracts.Encoding +import ComplexityAbstracts.Computation import ComplexityAbstracts.CryptographyBridge /-! # One-way functions, generators and adaptive pseudorandom functions @@ -19,9 +21,9 @@ Goldreich–Goldwasser–Micali construction then produces a keyed function that consistently chosen random function even when each query depends on earlier answers. Existence of a one-way function remains a hypothesis; efficiency and security use uniform finite-control machines with strict polynomial bounds and independent fair coins. -Lean checks the explicit experiments below through `CryptographyBridge`, and `#check_abstract` -allows only the six foundational oracle-syntax and machine modules described in the adaptive -section across the implementation boundary. +The definitions and theorem statements below specify the claim; Lean checks their proofs through +`CryptographyBridge`. The audit allows only the listed foundational program, interpretation and +machine modules across the implementation boundary, without importing a security definition. ## References @@ -38,37 +40,6 @@ as credited in `Complexity.Languages.Probabilistic.Basic`. namespace ComplexityTests.Abstracts.CryptographyAbstract -/-- Self-delimiting framing: double each bit `b` to `[true,b]` and terminate with `[false]`. -/ -def frame (w : List Bool) : List Bool := w.flatMap (fun b => [true, b]) ++ [false] - -/-- Encode a pair by framing its first component and appending its second. -/ -def encodePair {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) (p : α × β) : - List Bool := frame (a p.1) ++ b p.2 - -theorem encodePair_injective {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) : - Function.Injective (encodePair a b) := CryptographyBridge.encodePair_injective a b - -/-- The injective pair encoding. The arrow `↪` means an injective function. -/ -def pairEncoding {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) : α × β ↪ List Bool := - ⟨encodePair a b, encodePair_injective a b⟩ - -/-- Bitstrings encode as themselves. -/ -def bitsEncoding : List Bool ↪ List Bool := Function.Embedding.refl _ - -/-- The security parameter is supplied in unary: `n` consecutive true bits. -/ -def unaryEncoding : ℕ ↪ List Bool := ⟨fun n => List.replicate n true, - fun _ _ h => by simpa only [List.length_replicate] using congrArg List.length h⟩ - -/-- A Boolean output encodes as one bit. -/ -def boolEncoding : Bool ↪ List Bool := ⟨fun b => [b], fun _ _ h => by injection h⟩ - -/-- One deterministic finite-state binary multitape Turing machine halts with the encoded -answer on every encoded input, within polynomially bounded time and space in its bit length. -`ComputableInTimeAndSpaceOfLength` is the upstream machine contract; both bounds are uniform. -/ -def PolyTime {α β : Type} (f : α → β) (a : α ↪ List Bool) (b : β ↪ List Bool) : Prop := - ∃ t s : ℕ → ℕ, Cslib.PolynomiallyBounded t ∧ Cslib.PolynomiallyBounded s ∧ - Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength f a b t s - /-- Exactly `n` independent fair bits, as a word of length `n`. -/ noncomputable def uniformBits (n : ℕ) : PMF (List Bool) := (Cslib.Probability.PMF.uniformOfFintype (Fin n → Bool)).map List.ofFn @@ -80,7 +51,8 @@ are fixed before the input. This also bounds every execution, rather than its ex def StrictPPT {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) (law : α → PMF β) : Prop := ∃ (c d : ℕ) (evaluate : α → List Bool → β), - PolyTime (fun p : α × List Bool => evaluate p.1 p.2) (pairEncoding a bitsEncoding) b ∧ + Computation.PolyTime (fun p : α × List Bool => evaluate p.1 p.2) + (Encoding.encPair a Encoding.encBits) b ∧ ∀ x, law x = (uniformBits (c * ((a x).length + 1) ^ d)).map (evaluate x) /-- A nonnegative error is negligible if multiplication by every fixed power of the security @@ -97,20 +69,22 @@ The test receives the unary seed length and a sample. `bind` samples the word an the test with independent coins; `nndist` is the absolute difference of success probabilities. -/ def Indistinguishable (X Y : ℕ → PMF (List Bool)) : Prop := ∀ test : ℕ → List Bool → PMF Bool, - StrictPPT (pairEncoding unaryEncoding bitsEncoding) boolEncoding + StrictPPT (Encoding.encPair Encoding.encUnary Encoding.encBits) Encoding.encBool (fun p => test p.1 p.2) → - Negligible (fun n => nndist (probability ((X n).bind (test n))) - (probability ((Y n).bind (test n)))) + Negligible (fun n => nndist + (probability (do let sample ← X n; test n sample)) + (probability (do let sample ← Y n; test n sample))) /-- A polynomial-time function is one-way if every strict PPT inverter, given unary `n` and `f(x)` for a uniform `n`-bit `x`, finds any preimage only with negligible probability. The candidate's length is unrestricted, and recovering the sampled `x` is unnecessary. -/ def OneWay (f : List Bool → List Bool) : Prop := - PolyTime f bitsEncoding bitsEncoding ∧ + Computation.PolyTime f Encoding.encBits Encoding.encBits ∧ ∀ inverter : ℕ → List Bool → PMF (List Bool), - StrictPPT (pairEncoding unaryEncoding bitsEncoding) bitsEncoding + StrictPPT (Encoding.encPair Encoding.encUnary Encoding.encBits) Encoding.encBits (fun p => inverter p.1 p.2) → - Negligible (fun n => probability ((uniformBits n).bind fun x => + Negligible (fun n => probability (do + let x ← uniformBits n (inverter n (f x)).map fun candidate => f candidate == f x)) /-- A deterministic polynomial-time generator has exact seed-dependent output length, @@ -118,7 +92,7 @@ strictly expands every length, and its uniform-seed outputs are indistinguishabl uniform distribution at that output length. The security parameter in both games is the seed length. The function need not be injective. -/ def PseudorandomGenerator (g : List Bool → List Bool) (length : ℕ → ℕ) : Prop := - PolyTime g bitsEncoding bitsEncoding ∧ + Computation.PolyTime g Encoding.encBits Encoding.encBits ∧ (∀ seed, (g seed).length = length seed.length) ∧ (∀ n, n < length n) ∧ Indistinguishable (fun n => (uniformBits n).map g) (fun n => uniformBits (length n)) @@ -142,7 +116,8 @@ computable in polynomial time with unary input and output. The resulting algorit deterministic polynomial time and secure against the same uniform strict PPT tests. -/ theorem stretch {g : List Bool → List Bool} (hg : PseudorandomGenerator g (fun n => n + 1)) (target : ℕ → ℕ) - (htarget : PolyTime target unaryEncoding unaryEncoding) (hgreater : ∀ n, n < target n) : + (htarget : Computation.PolyTime target Encoding.encUnary Encoding.encUnary) + (hgreater : ∀ n, n < target n) : ∃ g' : List Bool → List Bool, PseudorandomGenerator g' target := CryptographyBridge.stretch hg target htarget hgreater @@ -152,84 +127,67 @@ A program is a terminating interaction tree. It can return a result, request an uniform sample, or submit a word and branch on the oracle's reply. Its next requests may depend on earlier replies. Termination alone gives no efficiency: the separate machine certificate below charges ordinary computation, query writing, reply access and output writing. - -The allowed machine is a binary multitape Turing machine with finite control and one named -oracle channel. Each channel has a write-only query buffer and a read-only reply tape with a -head. An ordinary transition reads input/work/reply cells, performs an upstream tape action, -appends at most one bit to the query buffer and moves the reply head by at most one cell. -A query instruction submits that buffer, installs the oracle's reply, resets the reply head -and clears the buffer. Each live instruction uses one independent fair bit to select between -two transitions. Each ordinary or query instruction costs one unit; the handler's computation -is external. The bounded interpreter starts with blank work and communication tapes and -returns the written output on halting or clock exhaustion. A later normalization theorem in -the implementation supplies an intrinsically halting realization with polynomial overhead. -/ -/-- Two disjoint effects: `.inl n` requests a fresh uniform `Fin (n+1)`; `.inr ((),word)` -submits a word to the single external channel and receives a word. This foundational response -family is reused exactly so the machine interpreter has the same typed interface. -/ -abbrev OracleResponse : Sum ℕ (Unit × List Bool) → Type := - Cslib.probOracleSpec (fun _ : Unit × List Bool => List Bool) - -/-- The free interaction tree for these effects. Upstream `PFunctor.FreeM` has two constructors: -`pure value` returns, and `liftBind request continuation` branches on the response. -/ +/-- Programs with private finite-uniform samples and one word-query channel. A request is +`((), word)` and its reply is a word. Sampling is independent of the external oracle; strict +fair-coin realizability is a separate requirement in `OraclePPT`. -/ abbrev OracleProgram (β : Type) := - (PFunctor.mk (Sum ℕ (Unit × List Bool)) OracleResponse).FreeM β + Cslib.ProbOracleComp (fun _ : Unit × List Bool => List Bool) β /-- Interpret a program against any shared stateful probabilistic handler. Fresh random draws are independent of that handler and leave its private state unchanged; external requests can update it. The result retains both the program's output and the final handler state. -/ noncomputable def execute {State β : Type} (program : OracleProgram β) (oracle : Unit × List Bool → StateT State PMF (List Bool)) (s : State) : PMF (β × State) := - (PFunctor.FreeM.liftM (P := ⟨Sum ℕ (Unit × List Bool), OracleResponse⟩) - (fun q => match q with - | .inl n => StateT.lift (Cslib.Probability.PMF.uniformOfFintype (Fin (n + 1))) - | .inr request => oracle request) program).run s + Cslib.ProbOracleComp.runWith oracle program s /-- One uniform finite-control oracle machine realizes the entire interaction, at a strict polynomial clock in the encoded unary parameter and auxiliary input. Equality is required for every handler and starting state, preserving the final state as well as the output. The machine cannot return an arbitrarily long reply for free: access and output writing are charged. -This is not a mere bound on the number of oracle queries. -/ +Each instruction costs one unit; oracle computation is external. The clocked run returns its +written output on halting or clock exhaustion. The definition does not require the unclocked +machine to halt; this is not a mere bound on the number of oracle queries. -/ def OraclePPT (program : ℕ → List Bool → OracleProgram Bool) : Prop := ∃ (k : ℕ) (Control : Type) (_ : Finite Control) (machine : Turing.MultiTapePTM k Bool Control Unit) (c d : ℕ), ∀ n aux (State : Type) (oracle : Unit × List Bool → StateT State PMF (List Bool)) s, - execute (boolEncoding <$> program n aux) oracle s = - execute (machine.runOracle (c * ((encodePair unaryEncoding bitsEncoding (n, aux)).length - + 1) ^ d) (encodePair unaryEncoding bitsEncoding (n, aux))) oracle s + let input := Encoding.encPair Encoding.encUnary Encoding.encBits (n, aux) + execute (Encoding.encBool <$> program n aux) oracle s = + execute (machine.runOracle (c * (input.length + 1) ^ d) input) oracle s -/-- Run a program against a fixed deterministic word oracle, with independent private samples. -/ +/-- Run a program against a fixed deterministic word oracle, with independent private samples. +The handler has no changing state: `Unit` is its single state, discarded from the result. -/ noncomputable def evaluateOracle {β : Type} (program : OracleProgram β) (oracle : List Bool → List Bool) : PMF β := - PFunctor.FreeM.liftM (P := ⟨Sum ℕ (Unit × List Bool), OracleResponse⟩) - (fun q => match q with - | .inl n => Cslib.Probability.PMF.uniformOfFintype (Fin (n + 1)) - | .inr request => PMF.pure (oracle request.2)) program + (Cslib.ProbOracleComp.runWith + (fun request => StateT.lift (PMF.pure (oracle request.2))) program ()).map Prod.fst /-- The real experiment samples one uniform key and consistently answers every valid query with that key's function. Wrong-length queries return the empty word. The adversary receives unary `n` and an empty auxiliary input. -/ noncomputable def realPRF (family : List Bool → List Bool → List Bool) - (adversary : ℕ → List Bool → OracleProgram Bool) (n : ℕ) : PMF Bool := - (uniformBits n).bind fun key => evaluateOracle (adversary n []) + (adversary : ℕ → List Bool → OracleProgram Bool) (n : ℕ) : PMF Bool := do + let key ← uniformBits n + evaluateOracle (adversary n []) (fun query => if query.length = n then family key query else []) /-- The ideal experiment samples one entire uniform function from `n` bits to `n` bits and reuses it across all adaptive calls. This is a probability specification; a lazy cache in the implementation realizes the same law without constructing its exponential truth table. Malformed queries are rejected in exactly the same way as in the real experiment. -/ -noncomputable def idealPRF (adversary : ℕ → List Bool → OracleProgram Bool) (n : ℕ) : PMF Bool := - (Cslib.Probability.PMF.uniformOfFintype ((Fin n → Bool) → Fin n → Bool)).bind - fun table => evaluateOracle (adversary n []) (fun query => - if query.length = n then List.ofFn (table fun i => query.getD i.val false) else []) +noncomputable def idealPRF (adversary : ℕ → List Bool → OracleProgram Bool) (n : ℕ) : PMF Bool := do + let table ← Cslib.Probability.PMF.uniformOfFintype ((Fin n → Bool) → Fin n → Bool) + evaluateOracle (adversary n []) (fun query => + if query.length = n then List.ofFn (table fun i => query.getD i.val false) else []) /-- A uniform adaptive pseudorandom function family has a deterministic polynomial-time keyed evaluator, `n`-bit answers to valid `n`-bit queries under `n`-bit keys, and negligible advantage between the preceding games for every one strict uniform adaptive oracle-PPT adversary. -/ def PseudorandomFunction (family : List Bool → List Bool → List Bool) : Prop := - PolyTime (fun p : List Bool × List Bool => family p.1 p.2) - (pairEncoding bitsEncoding bitsEncoding) bitsEncoding ∧ + Computation.PolyTime (fun p : List Bool × List Bool => family p.1 p.2) + (Encoding.encPair Encoding.encBits Encoding.encBits) Encoding.encBits ∧ (∀ key query, query.length = key.length → (family key query).length = key.length) ∧ ∀ adversary : ℕ → List Bool → OracleProgram Bool, OraclePPT adversary → Negligible (fun n => nndist (probability (realPRF family adversary n)) @@ -242,14 +200,31 @@ theorem adaptive_functions {f : List Bool → List Bool} (hf : OneWay f) : ∃ family : List Bool → List Bool → List Bool, PseudorandomFunction family := CryptographyBridge.adaptive_functions hf +/-! ## Representation details + +The binary multitape machine has finite control and one oracle channel with a write-only query +buffer and a read-only reply tape. An ordinary instruction performs an upstream tape action, +appends at most one bit to the query buffer and moves the reply head by at most one cell. A query +instruction submits the buffer, installs the reply, resets the reply head and clears the buffer. +Each live instruction uses one independent fair bit to select between two transitions. The +interpreter starts with blank work and communication tapes. Its clock bounds every run, including +query construction and reply access, while the handler's computation is external. +-/ + +/-- The underlying response family, retained for clients inspecting the program representation: +`.inl n` requests a fresh uniform `Fin (n+1)`; `.inr ((),word)` requests an external word reply. -/ +abbrev OracleResponse : Sum ℕ (Unit × List Bool) → Type := + Cslib.probOracleSpec (fun _ : Unit × List Bool => List Bool) + /-- -info: abstract audit passed for `ComplexityTests.Abstracts.CryptographyAbstract`: 33 root -declarations, 254 dependencies checked +info: abstract audit passed for `ComplexityTests.Abstracts.CryptographyAbstract`: 21 root declarations, 252 dependencies checked -/ #guard_msgs (whitespace := lax) in #check_abstract ComplexityTests.Abstracts.CryptographyAbstract allowing [ + ComplexityAbstracts.Encoding, ComplexityAbstracts.Computation, Complexity.Languages.Probabilistic.Basic, Complexity.Languages.Probabilistic.Oracle, + Complexity.Languages.Probabilistic.Oracle.Interaction, Complexity.Computability.Machines.Turing.MultiTape.Machine, Complexity.Computability.Machines.Turing.MultiTape.Machine.Program, Complexity.Computability.Machines.Turing.MultiTape.Probabilistic, diff --git a/abstracts/ComplexityAbstracts/CryptographyBridge.lean b/abstracts/ComplexityAbstracts/CryptographyBridge.lean index 21ecce45e..d881262fa 100644 --- a/abstracts/ComplexityAbstracts/CryptographyBridge.lean +++ b/abstracts/ComplexityAbstracts/CryptographyBridge.lean @@ -13,6 +13,7 @@ import Complexity.Crypto.Computational.GoldreichLevin.HardCore import Complexity.Crypto.Computational.Stretch import Complexity.Crypto.Computational.OneWayToPRF import Complexity.Computability.Probabilistic.CoinTape +import Complexity.Languages.Probabilistic.Oracle.Interaction import Complexity.Tactic.PPT /-! # Bridge for uniform cryptographic constructions @@ -178,25 +179,18 @@ abbrev OracleResponse : Sum ℕ (Unit × List Bool) → Type := Cslib.probOracleSpec (fun _ : Unit × List Bool => List Bool) abbrev OracleProgram (β : Type) := - (PFunctor.mk (Sum ℕ (Unit × List Bool)) OracleResponse).FreeM β + Cslib.ProbOracleComp (fun _ : Unit × List Bool => List Bool) β noncomputable def execute {State β : Type} (program : OracleProgram β) (oracle : Unit × List Bool → StateT State PMF (List Bool)) (s : State) : PMF (β × State) := - (PFunctor.FreeM.liftM (P := ⟨Sum ℕ (Unit × List Bool), OracleResponse⟩) - (fun q => match q with - | .inl n => StateT.lift (Cslib.Probability.PMF.uniformOfFintype (Fin (n + 1))) - | .inr request => oracle request) program).run s + ProbOracleComp.runWith oracle program s theorem execute_eq {State β : Type} (program : OracleProgram β) (oracle : Unit × List Bool → StateT State PMF (List Bool)) (s : State) : execute program oracle s = (OracleComp.interpret (ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle) - program).run s := by - unfold execute OracleComp.interpret - congr 2 - funext q - cases q <;> rfl + program).run s := rfl def OraclePPT (program : ℕ → List Bool → OracleProgram Bool) : Prop := ∃ (k : ℕ) (Control : Type) (_ : Finite Control) @@ -222,30 +216,35 @@ theorem oraclePPT_iff {program : ℕ → List Bool → OracleProgram Bool} : noncomputable def evaluateOracle {β : Type} (program : OracleProgram β) (oracle : List Bool → List Bool) : PMF β := - PFunctor.FreeM.liftM (P := ⟨Sum ℕ (Unit × List Bool), OracleResponse⟩) - (fun q => match q with - | .inl n => Cslib.Probability.PMF.uniformOfFintype (Fin (n + 1)) - | .inr request => PMF.pure (oracle request.2)) program + (ProbOracleComp.runWith + (fun request => StateT.lift (PMF.pure (oracle request.2))) program ()).map Prod.fst theorem evaluateOracle_eq {β : Type} (program : OracleProgram β) (oracle : List Bool → List Bool) : evaluateOracle program oracle = OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle (fun request => PMF.pure (oracle request.2))) program := by - unfold evaluateOracle OracleComp.interpret - congr 1 - funext q - cases q <;> rfl + have hlift : ProbOracleComp.handler (fun n => StateT.lift (σ := Unit) (ProbComp.unifOracle n)) + (fun request : Unit × List Bool => StateT.lift (PMF.pure (oracle request.2))) = + (fun q => StateT.lift + (ProbOracleComp.handler ProbComp.unifOracle (fun request => PMF.pure (oracle request.2)) + q)) := by + funext q + cases q <;> rfl + simp only [evaluateOracle, ProbOracleComp.runWith, hlift, OracleComp.run_interpret_lift] + simp only [PMF.monad_map_eq_map, PMF.map_comp] + exact PMF.map_id _ noncomputable def realPRF (family : List Bool → List Bool → List Bool) - (adversary : ℕ → List Bool → OracleProgram Bool) (n : ℕ) : PMF Bool := - (uniformBits n).bind fun key => evaluateOracle (adversary n []) + (adversary : ℕ → List Bool → OracleProgram Bool) (n : ℕ) : PMF Bool := do + let key ← uniformBits n + evaluateOracle (adversary n []) (fun query => if query.length = n then family key query else []) -noncomputable def idealPRF (adversary : ℕ → List Bool → OracleProgram Bool) (n : ℕ) : PMF Bool := - (Cslib.Probability.PMF.uniformOfFintype ((Fin n → Bool) → Fin n → Bool)).bind - fun table => evaluateOracle (adversary n []) (fun query => - if query.length = n then List.ofFn (table fun i => query.getD i.val false) else []) +noncomputable def idealPRF (adversary : ℕ → List Bool → OracleProgram Bool) (n : ℕ) : PMF Bool := do + let table ← Cslib.Probability.PMF.uniformOfFintype ((Fin n → Bool) → Fin n → Bool) + evaluateOracle (adversary n []) (fun query => + if query.length = n then List.ofFn (table fun i => query.getD i.val false) else []) def PseudorandomFunction (family : List Bool → List Bool → List Bool) : Prop := PolyTime (fun p : List Bool × List Bool => family p.1 p.2) diff --git a/abstracts/ComplexityAbstracts/Encoding.lean b/abstracts/ComplexityAbstracts/Encoding.lean new file mode 100644 index 000000000..6692fcb10 --- /dev/null +++ b/abstracts/ComplexityAbstracts/Encoding.lean @@ -0,0 +1,74 @@ +/- +Copyright (c) 2026 Christian Reitwiessner, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner, Samuel Schlesinger +-/ + +-- upstream: local-only (formal abstract foundations) + +import ComplexityAbstracts.Check +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat + +/-! # Binary input conventions + +An encoding is an injective map to finite bitstrings; `↪` records injectivity. These fixed +conventions specify the inputs and outputs of the machines used in the abstracts. Framing makes +component boundaries recoverable with linear overhead. Natural numbers use binary digits unless +an abstract explicitly supplies a unary parameter. Changing binary to unary can change a +complexity claim. The delimiter convention below fixes the precise machine input. + +The conventions are those of Christian Reitwiessner's native-machine encoding API. Their exact +definitions are collected here so each theorem can be read before its serialization details. +-/ + +namespace ComplexityTests.Abstracts.Encoding + +/-- Make a word self-delimiting: tag each bit by `true` and finish with `false`. -/ +def frame (w : List Bool) : List Bool := w.flatMap (fun b => [true, b]) ++ [false] + +/-- Frame the first component, then append the second. -/ +def encodePair {α β : Type} (a : α → List Bool) (b : β → List Bool) (p : α × β) : + List Bool := frame (a p.1) ++ b p.2 + +/-- Concatenate the framed elements of a list. -/ +def encodeList {α : Type} (enc : α → List Bool) (l : List α) : List Bool := + l.flatMap (frame ∘ enc) + +theorem encodePair_injective {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) : + Function.Injective (encodePair a b) := (Turing.MultiTapeTM.encPair a b).injective + +theorem encodeList_injective {α : Type} (enc : α ↪ List Bool) : + Function.Injective (encodeList enc) := (Turing.MultiTapeTM.encList enc).injective + +theorem bits_injective : Function.Injective Nat.bits := Turing.MultiTapeTM.encNat.injective + +/-- Injective encoding of a pair. Its length is `2 * |a x| + 1 + |b y|`. -/ +def encPair {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) : α × β ↪ List Bool := + ⟨encodePair a b, encodePair_injective a b⟩ + +/-- Injective encoding of a list. -/ +def encList {α : Type} (enc : α ↪ List Bool) : List α ↪ List Bool := + ⟨encodeList enc, encodeList_injective enc⟩ + +/-- Canonical binary digits, least significant first; zero has the empty encoding. -/ +def encNat : ℕ ↪ List Bool := ⟨Nat.bits, bits_injective⟩ + +/-- A Boolean is a single bit. -/ +def encBool : Bool ↪ List Bool := ⟨fun b => [b], by intro a b h; injection h⟩ + +/-- A bitstring is its own encoding. -/ +def encBits : List Bool ↪ List Bool := Function.Embedding.refl _ + +/-- Unary size or security parameter: exactly `n` bits. -/ +def encUnary : ℕ ↪ List Bool := ⟨fun n => List.replicate n true, by + intro a b h + simpa only [List.length_replicate] using congrArg List.length h⟩ + +end ComplexityTests.Abstracts.Encoding + +/-- +info: abstract audit passed for `ComplexityTests.Abstracts.Encoding`: +14 root declarations, 32 dependencies checked +-/ +#guard_msgs (whitespace := lax) in +#check_abstract ComplexityTests.Abstracts.Encoding diff --git a/abstracts/ComplexityAbstracts/FaginAbstract.lean b/abstracts/ComplexityAbstracts/FaginAbstract.lean index 287e16869..762618460 100644 --- a/abstracts/ComplexityAbstracts/FaginAbstract.lean +++ b/abstracts/ComplexityAbstracts/FaginAbstract.lean @@ -7,6 +7,8 @@ Authors: Samuel Schlesinger -- upstream: local-only (formal abstract library) import ComplexityAbstracts.Check +import ComplexityAbstracts.Encoding +import ComplexityAbstracts.Computation import ComplexityAbstracts.FaginBridge /-! # Fagin's theorem @@ -33,52 +35,6 @@ Lean checks the explicit logical and computational correspondence through the br namespace ComplexityTests.Abstracts.FaginAbstract -/-- Frame each bit as `[true, b]` and terminate the word with `[false]`. -/ -def frame (w : List Bool) : List Bool := w.flatMap (fun b => [true, b]) ++ [false] - -/-- Encode a pair by framing its first component and appending its second component. -/ -def encodePair {α β : Type} (a : α → List Bool) (b : β → List Bool) (p : α × β) : - List Bool := frame (a p.1) ++ b p.2 - -/-- Encode a list by concatenating its framed elements. -/ -def encodeList {α : Type} (enc : α → List Bool) (l : List α) : List Bool := - l.flatMap (frame ∘ enc) - -theorem encodePair_injective {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) : - Function.Injective (encodePair a b) := FaginBridge.encodePair_injective a b - -theorem encodeList_injective {α : Type} (enc : α ↪ List Bool) : - Function.Injective (encodeList enc) := FaginBridge.encodeList_injective enc - -/-- Pair encoding; `↪` records injectivity. -/ -def encPair {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) : α × β ↪ List Bool := - ⟨encodePair a b, encodePair_injective a b⟩ - -/-- List encoding. -/ -def encList {α : Type} (enc : α ↪ List Bool) : List α ↪ List Bool := - ⟨encodeList enc, encodeList_injective enc⟩ - -/-- A Boolean is encoded by a single bit. -/ -def encBool : Bool ↪ List Bool := ⟨fun b => [b], by intro a b h; injection h⟩ - -/-- Bitstrings encode themselves. -/ -def encBits : List Bool ↪ List Bool := Function.Embedding.refl _ - -/-- A single finite-state binary multi-tape machine computes `f` on every encoded input, -within polynomial time and work space. Inputs are read-only; outputs are write-only. -`Cslib.PolynomiallyBounded` means bounded above by some polynomial. -/ -def ComputableInPolyTime {α β : Type} (f : α → β) - (a : α ↪ List Bool) (b : β ↪ List Bool) : Prop := - ∃ t s : ℕ → ℕ, Cslib.PolynomiallyBounded t ∧ Cslib.PolynomiallyBounded s ∧ - Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength f a b t s - -/-- NP consists of problems with a polynomial-time deterministic verifier and binary -certificates of an exact polynomial length. The verifier halts on every input pair. -/ -def NP {α : Type} (enc : α ↪ List Bool) : Set (Set α) := - {A | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), - ComputableInPolyTime V (encPair enc encBits) encBool ∧ - ∀ a, a ∈ A ↔ ∃ w : List Bool, w.length = p.eval (enc a).length ∧ V (a, w) = true} - /-- Relation variables with prescribed arities, used for existential second-order quantifiers. There are no function symbols; a relation symbol is its index together with its arity equation. -/ def relationVariables {ι : Type} (arity : ι → ℕ) : FirstOrder.Language where @@ -107,17 +63,35 @@ def IsoClosed {L : FirstOrder.Language} (K : Set (CategoryTheory.Bundled.{0} L.S ∀ ⦃M N : CategoryTheory.Bundled.{0} L.Structure⦄ [Finite M], (FirstOrder.Language.Equiv L M N) → (M ∈ K ↔ N ∈ K) +/-! ## Efficient verification + +`Computation.PolyTimeVerifier enc V` means one deterministic verifier running in polynomial +time in the combined encoded length of its instance and certificate, on every such pair. +The fixed certificate length is the polynomial `p` evaluated at the instance bit length. +The machine and encoding conventions are collected in the foundations appendix. +-/ + +/-- NP consists of problems with a polynomial-time deterministic verifier and binary +certificates of an exact polynomial length. The verifier halts on every input pair. -/ +def NP {α : Type} (enc : α ↪ List Bool) : Set (Set α) := + {A | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), + Computation.PolyTimeVerifier enc V ∧ + ∀ a, a ∈ A ↔ ∃ w : List Bool, w.length = p.eval (enc a).length ∧ V (a, w) = true} + /-- Parsed input data: cardinality and one Boolean truth table for each relation symbol. -/ abbrev Input := ℕ × List (List Bool) -/-- An injective encoding of cardinalities in unary. -/ -def encUnary : ℕ ↪ List Bool := - ⟨fun n => List.replicate n true, by - intro a b h - simpa only [List.length_replicate] using congrArg List.length h⟩ +/-! ## Representation details + +An input gives the universe size in unary and one truth table per relation symbol. Unary size +ensures that input length is at least the universe size, even for an empty vocabulary. +A `CategoryTheory.Bundled L.Structure` is simply a universe together with an interpretation +of the symbols of `L`. The decoder below uses the universe `Fin a.1`. +-/ /-- Encode the unary cardinality and the framed list of relation truth tables. -/ -def encInput : Input ↪ List Bool := encPair encUnary (encList encBits) +def encInput : Input ↪ List Bool := + Encoding.encPair Encoding.encUnary (Encoding.encList Encoding.encBits) /-- Decode input data according to a finite enumeration of all relation symbols, with arities. The first tuple coordinate is least significant (`finFunctionFinEquiv`); missing entries read @@ -128,6 +102,8 @@ false. The theorem's query language separately rejects incorrect table sizes. -/ RelMap r x := (a.2.getD (symbols.symm ⟨_, r⟩).val []).getD (finFunctionFinEquiv x).val false = true +/-! ## The query language -/ + /-- Parsed data is well formed when every relation symbol has a table of exactly `n^arity` bits, including one bit for every nullary relation even when `n=0`. -/ def WellFormed {L : FirstOrder.Language} {count : ℕ} @@ -151,9 +127,11 @@ theorem fagin {L : FirstOrder.Language} [L.IsRelational] {count : ℕ} /-- info: abstract audit passed for `ComplexityTests.Abstracts.FaginAbstract`: -25 root declarations, 100 dependencies checked +12 root declarations, 101 dependencies checked -/ #guard_msgs (whitespace := lax) in -#check_abstract ComplexityTests.Abstracts.FaginAbstract +#check_abstract ComplexityTests.Abstracts.FaginAbstract allowing [ + ComplexityAbstracts.Encoding, ComplexityAbstracts.Computation +] end ComplexityTests.Abstracts.FaginAbstract diff --git a/abstracts/ComplexityAbstracts/FormulaBoundsAbstract.lean b/abstracts/ComplexityAbstracts/FormulaBoundsAbstract.lean index cc2991252..7f4aa4256 100644 --- a/abstracts/ComplexityAbstracts/FormulaBoundsAbstract.lean +++ b/abstracts/ComplexityAbstracts/FormulaBoundsAbstract.lean @@ -62,15 +62,36 @@ noncomputable def minimumLeaves {n : ℕ} (f : (Fin n → Bool) → Bool) : ℕ def parity (n : ℕ) (x : Fin n → Bool) : Bool := decide ((Finset.univ.filter fun i => x i = true).card % 2 = 1) -/-- The binary number represented by a word, with coordinate zero least significant. -/ +/-- The binary number represented by a word, with coordinate zero least significant: +the value is `∑ i, (if bits i then 1 else 0) * 2^i`. -/ def tableIndex (n : ℕ) : (Fin n → Bool) ≃ Fin (2 ^ n) := (Equiv.arrowCongr (Equiv.refl (Fin n)) finTwoEquiv.symm).trans finFunctionFinEquiv -/-- Andreev's function: the first `2^b` bits are a truth table; the next `b*m` bits form `b` -blocks whose parities address that table. The table is part of the input, not a hardwired oracle. -/ +/-- The address is the ordinary binary value, with bit zero least significant. -/ +theorem tableIndex_val {b : ℕ} (bits : Fin b → Bool) : + (tableIndex b bits).val = ∑ i : Fin b, (if bits i then 1 else 0) * 2 ^ i.val := + FormulaBoundsBridge.tableIndex_val bits + +/-- The first `2^b` input bits form the truth table, in address order. -/ +def tableInput {b m : ℕ} (x : Fin (2 ^ b + b * m) → Bool) : Fin (2 ^ b) → Bool := + fun i => x (Fin.castAdd (b * m) i) + +/-- The remaining input is `b` consecutive blocks of `m` bits. Block `j`, position `t`, is +input position `2^b + m*j + t`. -/ +def blockInput {b m : ℕ} (x : Fin (2 ^ b + b * m) → Bool) (j : Fin b) : Fin m → Bool := + fun t => x (Fin.natAdd (2 ^ b) (finProdFinEquiv (j, t))) + +/-- Reading block `j` at position `t` reads exactly the indicated flat input coordinate. -/ +theorem blockInput_eq {b m : ℕ} (x : Fin (2 ^ b + b * m) → Bool) (j : Fin b) (t : Fin m) + (i : Fin (2 ^ b + b * m)) (hi : i.val = 2 ^ b + m * j.val + t.val) : + blockInput x j t = x i := + FormulaBoundsBridge.blockInput_eq x j t i hi + +/-- Andreev's function reads the truth-table entry addressed by the `b` block parities. +The table is part of the input, not a hardwired oracle. Its bit at address zero is used when +there are no blocks (`b = 0`), or when every block is empty (`m = 0`). -/ def andreev (b m : ℕ) (x : Fin (2 ^ b + b * m) → Bool) : Bool := - x (Fin.castAdd (b * m) (tableIndex b fun j => - parity m fun t => x (Fin.natAdd (2 ^ b) (finProdFinEquiv (j, t))))) + tableInput x (tableIndex b fun j => parity m (blockInput x j)) /-- **Spira.** Balancing preserves the function and bounds AND/OR depth by four times the ceiling logarithm of the original leaf count. For a constant expression the bound is zero. -/ @@ -130,8 +151,8 @@ theorem andreev_lower_bound : 144 * b ^ 2 * (Nat.log 2 b + 2) ^ 3 * minimumLeaves (andreev b m) ^ 2 := FormulaBoundsBridge.andreev_lower_bound -/-- info: abstract audit passed for `ComplexityTests.Abstracts.FormulaBoundsAbstract`: 17 root -declarations, 115 dependencies checked -/ +/-- info: abstract audit passed for `ComplexityTests.Abstracts.FormulaBoundsAbstract`: 21 root +declarations, 119 dependencies checked -/ #guard_msgs (whitespace := lax) in #check_abstract ComplexityTests.Abstracts.FormulaBoundsAbstract allowing [ Complexity.Computability.Circuit.Formula diff --git a/abstracts/ComplexityAbstracts/FormulaBoundsBridge.lean b/abstracts/ComplexityAbstracts/FormulaBoundsBridge.lean index 1193388d8..6d06a1e27 100644 --- a/abstracts/ComplexityAbstracts/FormulaBoundsBridge.lean +++ b/abstracts/ComplexityAbstracts/FormulaBoundsBridge.lean @@ -41,15 +41,43 @@ noncomputable def minimumLeaves {n : ℕ} (f : (Fin n → Bool) → Bool) : ℕ def parity (n : ℕ) (x : Fin n → Bool) : Bool := decide ((Finset.univ.filter fun i => x i = true).card % 2 = 1) -/-- The binary number represented by a word, with coordinate zero least significant. -/ +/-- The binary number represented by a word, with coordinate zero least significant: +the value is `∑ i, (if bits i then 1 else 0) * 2^i`. -/ def tableIndex (n : ℕ) : (Fin n → Bool) ≃ Fin (2 ^ n) := (Equiv.arrowCongr (Equiv.refl (Fin n)) finTwoEquiv.symm).trans finFunctionFinEquiv -/-- Andreev's function: the first `2^b` bits are a truth table; the next `b*m` bits form `b` -blocks whose parities address that table. The table is part of the input, not a hardwired oracle. -/ +/-- The address is the ordinary binary value, with bit zero least significant. -/ +theorem tableIndex_val {b : ℕ} (bits : Fin b → Bool) : + (tableIndex b bits).val = ∑ i : Fin b, (if bits i then 1 else 0) * 2 ^ i.val := by + change (finFunctionFinEquiv (fun i => finTwoEquiv.symm (bits i))).val = _ + rw [finFunctionFinEquiv_apply] + apply Finset.sum_congr rfl + intro i _ + cases bits i <;> simp [finTwoEquiv] + +/-- The first `2^b` input bits form the truth table, in address order. -/ +def tableInput {b m : ℕ} (x : Fin (2 ^ b + b * m) → Bool) : Fin (2 ^ b) → Bool := + fun i => x (Fin.castAdd (b * m) i) + +/-- The remaining input is `b` consecutive blocks of `m` bits. Block `j`, position `t`, is +input position `2^b + m*j + t`. -/ +def blockInput {b m : ℕ} (x : Fin (2 ^ b + b * m) → Bool) (j : Fin b) : Fin m → Bool := + fun t => x (Fin.natAdd (2 ^ b) (finProdFinEquiv (j, t))) + +/-- Reading block `j` at position `t` reads exactly the indicated flat input coordinate. -/ +theorem blockInput_eq {b m : ℕ} (x : Fin (2 ^ b + b * m) → Bool) (j : Fin b) (t : Fin m) + (i : Fin (2 ^ b + b * m)) (hi : i.val = 2 ^ b + m * j.val + t.val) : + blockInput x j t = x i := by + apply congrArg x + apply Fin.ext + change 2 ^ b + (t.val + m * j.val) = i.val + omega + +/-- Andreev's function reads the truth-table entry addressed by the `b` block parities. +The table is part of the input, not a hardwired oracle. Its bit at address zero is used when +there are no blocks (`b = 0`), or when every block is empty (`m = 0`). -/ def andreev (b m : ℕ) (x : Fin (2 ^ b + b * m) → Bool) : Bool := - x (Fin.castAdd (b * m) (tableIndex b fun j => - parity m fun t => x (Fin.natAdd (2 ^ b) (finProdFinEquiv (j, t))))) + tableInput x (tableIndex b fun j => parity m (blockInput x j)) /-- **Spira.** Balancing preserves the function and bounds AND/OR depth by four times the ceiling logarithm of the original leaf count. For a constant expression the bound is zero. -/ diff --git a/abstracts/ComplexityAbstracts/PCPAbstract.lean b/abstracts/ComplexityAbstracts/PCPAbstract.lean index 8a3983de9..ae40dd1a2 100644 --- a/abstracts/ComplexityAbstracts/PCPAbstract.lean +++ b/abstracts/ComplexityAbstracts/PCPAbstract.lean @@ -7,6 +7,8 @@ Authors: Bolton Bailey, Samuel Schlesinger -- upstream: local-only (formal abstract library) import ComplexityAbstracts.Check +import ComplexityAbstracts.Encoding +import ComplexityAbstracts.Computation import ComplexityAbstracts.PCPBridge /-! # The PCP theorem @@ -33,55 +35,18 @@ statement's dependency boundary. namespace ComplexityTests.Abstracts.PCPAbstract -/-- Frame each bit as `[true, b]` and terminate the word with `[false]`. -/ -def frame (w : List Bool) : List Bool := w.flatMap (fun b => [true, b]) ++ [false] +/-! ## Efficient verification -/-- Encode a pair by framing its first component and appending its second component. -/ -def encodePair {α β : Type} (a : α → List Bool) (b : β → List Bool) (p : α × β) : - List Bool := frame (a p.1) ++ b p.2 - -/-- Encode a list by concatenating its framed elements. -/ -def encodeList {α : Type} (enc : α → List Bool) (l : List α) : List Bool := - l.flatMap (frame ∘ enc) - -theorem encodePair_injective {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) : - Function.Injective (encodePair a b) := PCPBridge.encodePair_injective a b - -theorem encodeList_injective {α : Type} (enc : α ↪ List Bool) : - Function.Injective (encodeList enc) := PCPBridge.encodeList_injective enc - -theorem bits_injective : Function.Injective Nat.bits := PCPBridge.bits_injective - -/-- Natural numbers are encoded by their canonical little-endian binary digits. -/ -def encNat : ℕ ↪ List Bool := ⟨Nat.bits, bits_injective⟩ - -/-- Pair encoding; `↪` records injectivity. -/ -def encPair {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) : α × β ↪ List Bool := - ⟨encodePair a b, encodePair_injective a b⟩ - -/-- List encoding. -/ -def encList {α : Type} (enc : α ↪ List Bool) : List α ↪ List Bool := - ⟨encodeList enc, encodeList_injective enc⟩ - -/-- A Boolean is encoded by a single bit. -/ -def encBool : Bool ↪ List Bool := ⟨fun b => [b], by intro a b h; injection h⟩ - -/-- Bitstrings encode themselves. -/ -def encBits : List Bool ↪ List Bool := Function.Embedding.refl _ - -/-- A single finite-state binary multi-tape machine computes `f` on every encoded input, -within polynomial time and work space. Inputs are read-only; outputs are write-only. -`Cslib.PolynomiallyBounded` means bounded above by some polynomial. -/ -def ComputableInPolyTime {α β : Type} (f : α → β) - (a : α ↪ List Bool) (b : β ↪ List Bool) : Prop := - ∃ t s : ℕ → ℕ, Cslib.PolynomiallyBounded t ∧ Cslib.PolynomiallyBounded s ∧ - Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength f a b t s +`Computation.PolyTimeVerifier enc V` is one deterministic verifier that halts on every pair +in polynomial time in `|enc a| + |w|`. Its code and bound are fixed before either input is +chosen. Certificates here have exactly the polynomial length `p(|enc a|)`. +-/ /-- NP consists of problems with a polynomial-time deterministic verifier and binary certificates of an exact polynomial length. The verifier halts on every input pair. -/ def NP {α : Type} (enc : α ↪ List Bool) : Set (Set α) := {A | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), - ComputableInPolyTime V (encPair enc encBits) encBool ∧ + Computation.PolyTimeVerifier enc V ∧ ∀ a, a ∈ A ↔ ∃ w : List Bool, w.length = p.eval (enc a).length ∧ V (a, w) = true} /-- Read a finite proof at the queried addresses. Positions beyond its end read as false. -/ @@ -94,6 +59,30 @@ def acceptCount {α : Type} (queries : α × List Bool → List ℕ) (Finset.univ.filter fun r : Fin n → Bool => verdict ((a, List.ofFn r), proofAnswers proof (queries (a, List.ofFn r))) = true).card +/-! ## Representation details + +All three verifier routines run in polynomial time. Query positions are binary integers, so +constructing their addresses is charged; the proof itself is accessed only at those positions. +-/ + +/-- Native polynomial-time realization of the coin count, query list and verdict. -/ +def EfficientVerifier {α : Type} (enc : α ↪ List Bool) (coins : α → ℕ) + (queries : α × List Bool → List ℕ) + (verdict : (α × List Bool) × List Bool → Bool) : Prop := + Computation.PolyTime coins enc Encoding.encNat ∧ + Computation.PolyTime queries (Encoding.encPair enc Encoding.encBits) + (Encoding.encList Encoding.encNat) ∧ + Computation.PolyTime verdict + (Encoding.encPair (Encoding.encPair enc Encoding.encBits) Encoding.encBits) Encoding.encBool + +/-! ## Probabilistically checkable proofs + +Randomness is a uniformly chosen word of exactly `coins a` bits. Thus the acceptance +probability is `acceptCount / 2^(coins a)`. The final inequality below says it is at most +one half, without division or rounding. `EfficientVerifier` charges coin counting, query selection +and the final verdict. +-/ + /-- Nonadaptive probabilistically checkable proofs: one fixed polynomial-time algorithm computes the number of random bits, the list of binary proof addresses and the final verdict. For constants `c,d`, it uses at most `c*r(n)` random bits and `d*q(n)` queries. A yes-instance @@ -102,9 +91,7 @@ accepted on at most half of the random strings. -/ def PCP {α : Type} (r q : ℕ → ℕ) (enc : α ↪ List Bool) : Set (Set α) := {A | ∃ (coins : α → ℕ) (queries : α × List Bool → List ℕ) (verdict : (α × List Bool) × List Bool → Bool) (c d : ℕ), - ComputableInPolyTime coins enc encNat ∧ - ComputableInPolyTime queries (encPair enc encBits) (encList encNat) ∧ - ComputableInPolyTime verdict (encPair (encPair enc encBits) encBits) encBool ∧ + EfficientVerifier enc coins queries verdict ∧ (∀ a, coins a ≤ c * r (enc a).length) ∧ (∀ a ρ, ρ.length = coins a → (queries (a, ρ)).length ≤ d * q (enc a).length) ∧ (∀ a ∈ A, ∃ proof : List Bool, ∀ ρ, ρ.length = coins a → @@ -115,13 +102,18 @@ def PCP {α : Type} (r q : ℕ → ℕ) (enc : α ↪ List Bool) : Set (Set α) soundness at most one half. Queries are nonadaptive; their binary addresses and all computation are charged, including the full gap-graph construction. -/ theorem pcp_theorem {α : Type} (enc : α ↪ List Bool) : - NP enc = PCP (fun n => Nat.log 2 n + 1) (fun _ => 1) enc := PCPBridge.pcp_theorem enc + NP enc = PCP (fun n => Nat.log 2 n + 1) (fun _ => 1) enc := by + unfold PCP EfficientVerifier + simp only [and_assoc] + exact PCPBridge.pcp_theorem enc /-- info: abstract audit passed for `ComplexityTests.Abstracts.PCPAbstract`: -18 root declarations, 83 dependencies checked +7 root declarations, 85 dependencies checked -/ #guard_msgs (whitespace := lax) in -#check_abstract ComplexityTests.Abstracts.PCPAbstract +#check_abstract ComplexityTests.Abstracts.PCPAbstract allowing [ + ComplexityAbstracts.Encoding, ComplexityAbstracts.Computation +] end ComplexityTests.Abstracts.PCPAbstract diff --git a/abstracts/ComplexityAbstracts/ResolutionAbstract.lean b/abstracts/ComplexityAbstracts/ResolutionAbstract.lean index cfa72407f..70df7c13b 100644 --- a/abstracts/ComplexityAbstracts/ResolutionAbstract.lean +++ b/abstracts/ComplexityAbstracts/ResolutionAbstract.lean @@ -10,8 +10,9 @@ import ComplexityAbstracts.ResolutionBridge /-! # A formal abstract of Haken's resolution lower bound -The pigeonhole principle has a short CNF expression but exponentially long resolution -refutations. This file defines the exact line-proof rule and pigeonhole formula and states +The pigeonhole principle with `n + 1` pigeons and `n` holes has a CNF of polynomial size in `n`, +but its resolution refutations need exponentially many lines in `n`. This file defines the +exact line-proof rule and pigeonhole formula and states Haken's lower bound, following the Beame–Pitassi bottleneck argument. A reader can inspect the definitions and theorem statements here without reading proof @@ -78,8 +79,9 @@ theorem pigeonhole_satisfiable (m n : ℕ) : Satisfiable (pigeonhole m n) ↔ m ResolutionBridge.pigeonhole_satisfiable m n /-- **Haken:** every resolution refutation with `s` lines of the formula for `n + 1` pigeons -and `n` holes satisfies `2^(floor(n/24)) ≤ s`. The formal proof follows the Beame–Pitassi -bottleneck argument, rather than obtaining this bound from size–width. -/ +and `n` holes satisfies `2^(floor(n/24)) ≤ s`. The exponential parameter is the number of holes, +not the length of an encoding of the CNF. The proof follows the Beame–Pitassi bottleneck +argument. -/ theorem haken {n s : ℕ} (hs : RefutableInSize (pigeonhole (n + 1) n) s) : 2 ^ (n / 24) ≤ s := ResolutionBridge.haken_of_rules IsProof diff --git a/abstracts/ComplexityAbstracts/SavitchAbstract.lean b/abstracts/ComplexityAbstracts/SavitchAbstract.lean index 6ffc83901..f69011481 100644 --- a/abstracts/ComplexityAbstracts/SavitchAbstract.lean +++ b/abstracts/ComplexityAbstracts/SavitchAbstract.lean @@ -18,8 +18,9 @@ by trying possible midpoints and checking the two halves in turn, reusing storag calls. The deterministic computation may take far longer, but its memory remains polynomial. The statement concerns binary multi-tape machines on encoded inputs. Every nondeterministic -branch halts, and every computation prefix obeys its space bound; read-only input and write-only -output are not charged. We state equality of the polynomial-space classes, rather than the fully +branch terminates (a stuck branch rejects), and every computation prefix obeys its space bound. +Read-only input and write-only output are not charged. We state equality of the polynomial-space +classes, rather than the fully parameterized quadratic-space simulation bound. Lean checks the transfer through the bridge, and `#check_abstract` audits the public dependencies. @@ -56,14 +57,14 @@ def DecidesInSpace {α : Type} {k : ℕ} {State : Type} ∀ a, ∃ t, M.RunsInTime (enc a) t /-- Nondeterministic polynomial space, with one fixed finite-state machine and all branches -halting; the space bound holds along every computation prefix, including rejecting branches. -/ +terminating; the space bound holds along every computation prefix, including rejecting branches. -/ def NPSPACE {α : Type} (enc : α ↪ List Bool) : Set (Set α) := {A | ∃ (k : ℕ) (State : Type) (_ : Finite State) (M : Turing.MultiTapeNTM k Bool State) (s : α → ℕ), (∃ b : ℕ → ℕ, Cslib.PolynomiallyBounded b ∧ ∀ a, s a ≤ b (enc a).length) ∧ DecidesInSpace M enc A s} /-- Savitch's equality of polynomial-space classes. Every nondeterministic computation -prefix obeys its space bound, and every branch halts (a stuck branch rejects). This does not +prefix obeys its space bound, and every branch terminates (a stuck branch rejects). This does not assert the fully parameterized `NSPACE(s) ⊆ DSPACE(s²)` theorem. -/ theorem savitch {α : Type} (enc : α ↪ List Bool) : NPSPACE enc = PSPACE enc := SavitchBridge.savitch enc diff --git a/abstracts/ComplexityAbstracts/ShamirAbstract.lean b/abstracts/ComplexityAbstracts/ShamirAbstract.lean index 8ab9ef23c..956be8f2c 100644 --- a/abstracts/ComplexityAbstracts/ShamirAbstract.lean +++ b/abstracts/ComplexityAbstracts/ShamirAbstract.lean @@ -23,8 +23,9 @@ stateful randomized provers. Completeness is at least two thirds and soundness a bounds and correctness apply to encoded instances. The explicit foundational model below distinguishes finite-uniform requests in program syntax from their efficient fair-coin realization. -Lean checks the bridge, and the audit permits only the seven listed foundational program and -machine modules, with no complexity-class or headline-result allowance. +The definitions and theorem statement below specify the claim. Lean checks the bridge, and the +audit permits only the seven listed foundational program and machine modules, with no +complexity-class or headline-result allowance. ## References @@ -50,12 +51,9 @@ abbrev InteractiveProgram (β : Type) := /-- One fixed finite fair-coin machine and one polynomial clock realize the entire joint law of the program's encoded result and the oracle's final state, against every stateful oracle. -Each live instruction consumes one fresh fair bit to select between two transitions. Ordinary -steps perform an upstream tape action, append at most one bit to a query buffer and move a -read-only reply head by at most one cell. A query step submits the buffer, installs the reply, -resets the reply head and clears the buffer. Each instruction costs one unit; the oracle's -computation is external. The bounded run observes its written output on halting or clock -exhaustion, so the definition does not pretend the unclocked machine has already halted. -/ +The clock charges computation, query writing, reply access and output writing. Each instruction +costs one unit; the prover's computation is external. The bounded run returns its written output +on halting or clock exhaustion; it does not require the unclocked machine to halt. -/ def StrictOraclePPT {α β : Type} (enc : α ↪ List Bool) (out : β ↪ List Bool) (program : α → InteractiveProgram β) : Prop := ∃ (k : ℕ) (Control : Type) (_ : Finite Control) @@ -97,6 +95,17 @@ deterministic polynomial space. Provers may be stateful, randomized and unbounde theorem ip_eq_pspace {α : Type} (enc : α ↪ List Bool) : IP enc = PSPACE enc := ShamirBridge.ip_eq_pspace enc +/-! ## Representation details + +The fair-coin machine uses one independent fair bit at each live instruction to choose between +two transitions. Ordinary instructions perform an upstream tape action, append at most one bit +to a query buffer and move a read-only reply head by at most one cell. A query instruction submits +the buffer, installs the reply, resets the reply head and clears the buffer. Query construction +and reply access therefore consume the verifier's clock, while the prover's computation does not. +Private sampling leaves the prover's state unchanged. The required equality preserves both the +verifier's output and the final prover state for every initial state and response strategy. +-/ + /-- info: abstract audit passed for `ComplexityTests.Abstracts.ShamirAbstract`: 10 root declarations, 213 dependencies checked diff --git a/abstracts/ComplexityAbstracts/SubsetSumAbstract.lean b/abstracts/ComplexityAbstracts/SubsetSumAbstract.lean index b3a1a72a7..2e1f51e8b 100644 --- a/abstracts/ComplexityAbstracts/SubsetSumAbstract.lean +++ b/abstracts/ComplexityAbstracts/SubsetSumAbstract.lean @@ -7,6 +7,8 @@ Authors: Samuel Schlesinger -- upstream: local-only (formal abstract library) import ComplexityAbstracts.Check +import ComplexityAbstracts.Encoding +import ComplexityAbstracts.Computation import ComplexityAbstracts.SubsetSumBridge /-! # A formal abstract of Subset Sum NP-completeness @@ -15,11 +17,9 @@ This file defines the Subset Sum decision problem on finite lists of natural num encoding, polynomial-time verifiers, the class NP and polynomial-time many-one reductions, and proves that Subset Sum is NP-complete when numbers are written in binary. -To check that the formalization establishes this result, a reader only needs to inspect the -definitions and theorem statements in this file. Every public definition and theorem statement -depends only on this file, `Mathlib`, and upstream `Cslib`'s multi-tape Turing machine model; -`#check_abstract` mechanically verifies that no internal `Complexitylib` declarations leak into the -statements, and Lean checks the proofs through `SubsetSumBridge`. +A reader can inspect the definitions and theorem statements here together with the displayed +shared-foundation appendix. `#check_abstract` audits their dependencies on upstream mathematics +and machine models; Lean checks the proofs through `SubsetSumBridge`. ## References @@ -38,84 +38,26 @@ most once. -/ def SubsetSum : Set (List ℕ × ℕ) := {x | ∃ s : List ℕ, s.Sublist x.1 ∧ s.sum = x.2} -/-! ## Binary encoding convention +/-! ## Representation details -Values are encoded injectively as bitstrings (`List Bool`). A bitstring `w` is -framed by encoding each bit `b` as `[true, b]` and appending `[false]`, making -framed bitstrings self-delimiting under concatenation. Pairs frame the first -component before appending the second, and lists concatenate the framed -encodings of their elements. Natural numbers use Mathlib's canonical -little-endian binary digits `Nat.bits` (`0 ↦ []`, positive `n` with least -significant bit first and final bit `true`). +The input list and target are encoded in binary. Each input occurrence can be selected once; +input size includes every number's binary digits. The fixed pair/list delimiters are given below. -/ -/-- Frame a bitstring: write each bit `b` as `[true, b]`, then terminate with `[false]`. -/ -def frame (w : List Bool) : List Bool := - w.flatMap (fun b => [true, b]) ++ [false] - -/-- Encode a pair by framing the encoding of its first component and appending the encoding of -its second component. -/ -def encodePair {α β : Type} (encA : α → List Bool) (encB : β → List Bool) (p : α × β) : - List Bool := - frame (encA p.1) ++ encB p.2 - -/-- Encode a list by concatenating the framed encodings of its elements. -/ -def encodeList {α : Type} (enc : α → List Bool) (l : List α) : List Bool := - l.flatMap (frame ∘ enc) - -theorem encodePair_injective {α β : Type} (encA : α ↪ List Bool) (encB : β ↪ List Bool) : - Function.Injective (encodePair encA encB) := - CookLevinBridge.encodePair_injective encA encB - -theorem encodeList_injective {α : Type} (enc : α ↪ List Bool) : - Function.Injective (encodeList enc) := - SubsetSumBridge.encodeList_injective enc - -theorem bits_injective : Function.Injective Nat.bits := - SubsetSumBridge.bits_injective - -/-- Injective binary encoding of natural numbers by `Nat.bits`. -/ -def encNat : ℕ ↪ List Bool := - ⟨Nat.bits, bits_injective⟩ - -/-- Injective framed encoding of lists. -/ -def encList {α : Type} (enc : α ↪ List Bool) : List α ↪ List Bool := - ⟨encodeList enc, encodeList_injective enc⟩ - -/-- Injective framed encoding of pairs. -/ -def encPair {α β : Type} (encA : α ↪ List Bool) (encB : β ↪ List Bool) : α × β ↪ List Bool := - ⟨encodePair encA encB, encodePair_injective encA encB⟩ - -/-- Injective encoding of bitstrings as themselves. -/ -def encBits : List Bool ↪ List Bool := Function.Embedding.refl _ - -/-- Injective encoding of a single Boolean as a one-bit word `[b]`. -/ -def encBool : Bool ↪ List Bool := - ⟨fun b => [b], by intro a b h; injection h⟩ - /-- Injective binary encoding of Subset Sum instances: the list of numbers, then the target. -/ def encSubsetSum : List ℕ × ℕ ↪ List Bool := - encPair (encList encNat) encNat + Encoding.encPair (Encoding.encList Encoding.encNat) Encoding.encNat -/-! ## Polynomial-time computability, NP, and NP-completeness +/-! ## Efficient verification and reductions -In upstream `Cslib`, `Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength f encA encB t s` -means that there exists a deterministic multi-tape Turing machine with a binary -tape alphabet and finitely many states that halts on every encoded input -`encA a` within `t (encA a).length` steps and `s (encA a).length` work-tape -cells, leaving `encB (f a)` on its output tape. `Cslib.PolynomiallyBounded` -asserts that a growth bound `ℕ → ℕ` is bounded above by a polynomial. +`Computation.PolyTimeVerifier enc V` means that one deterministic machine halts on every +instance/certificate pair in polynomial time in their combined bit length. The machine and +polynomial bound are fixed for the problem. We use certificates of exactly `p(|enc a|)` bits; +this is the fixed-length certificate convention. `Computation.PolyTime` is the same total +computation contract for general input and output encodings. Their definitions are in the +foundations appendix. -/ -/-- A total function `f : α → β` is computable in polynomial time with respect -to input encoding `encA` and output encoding `encB` if some deterministic -multi-tape binary Turing machine computes it within polynomially bounded time -and space in the input bit length. -/ -def ComputableInPolyTime {α β : Type} (f : α → β) - (encA : α ↪ List Bool) (encB : β ↪ List Bool) : Prop := - ∃ t s : ℕ → ℕ, Cslib.PolynomiallyBounded t ∧ Cslib.PolynomiallyBounded s ∧ - Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength f encA encB t s - /-- A function `V : α × List Bool → Bool` verifies a decision problem `A` with certificate length polynomial `p` if an instance `a` belongs to `A` exactly when there is a binary certificate `w` of length `p(|enc a|)` accepted by `V`. -/ @@ -128,14 +70,14 @@ problems that have a polynomial-time verifier with polynomially long binary certificates. -/ def NP {α : Type} (enc : α ↪ List Bool) : Set (Set α) := {A | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), - ComputableInPolyTime V (encPair enc encBits) encBool ∧ IsVerifier enc p V A} + Computation.PolyTimeVerifier enc V ∧ IsVerifier enc p V A} /-- Problem `A` (with encoding `encA`) many-one reduces in polynomial time to problem `B` (with encoding `encB`) if a polynomial-time computable map `f` preserves yes/no membership on every instance. -/ def PolyTimeReducible {α β : Type} (encA : α ↪ List Bool) (encB : β ↪ List Bool) (A : Set α) (B : Set β) : Prop := - ∃ f : α → β, ComputableInPolyTime f encA encB ∧ ∀ a, a ∈ A ↔ f a ∈ B + ∃ f : α → β, Computation.PolyTime f encA encB ∧ ∀ a, a ∈ A ↔ f a ∈ B /-- A problem `B` is NP-complete if it belongs to NP and every NP problem (over any instance type `α` and injective binary encoding `encA`) reduces to `B` in @@ -153,10 +95,12 @@ theorem subsetSum_npComplete : NPComplete encSubsetSum SubsetSum := SubsetSumBridge.subsetSum_npComplete /-- -info: abstract audit passed for `ComplexityTests.Abstracts.SubsetSumAbstract`: 20 root -declarations, 61 dependencies checked +info: abstract audit passed for `ComplexityTests.Abstracts.SubsetSumAbstract`: +7 root declarations, 62 dependencies checked -/ #guard_msgs (whitespace := lax) in -#check_abstract ComplexityTests.Abstracts.SubsetSumAbstract +#check_abstract ComplexityTests.Abstracts.SubsetSumAbstract allowing [ + ComplexityAbstracts.Encoding, ComplexityAbstracts.Computation +] end ComplexityTests.Abstracts.SubsetSumAbstract diff --git a/abstracts/ComplexityAbstracts/TQBFAbstract.lean b/abstracts/ComplexityAbstracts/TQBFAbstract.lean index ba3523550..5a02f24da 100644 --- a/abstracts/ComplexityAbstracts/TQBFAbstract.lean +++ b/abstracts/ComplexityAbstracts/TQBFAbstract.lean @@ -7,6 +7,8 @@ Authors: Samuel Schlesinger -- upstream: local-only (formal abstract library) import ComplexityAbstracts.Check +import ComplexityAbstracts.Encoding +import ComplexityAbstracts.Computation import ComplexityAbstracts.TQBFBridge /-! # A formal abstract of the PSPACE-completeness of TQBF @@ -17,12 +19,9 @@ space (`PSPACE`), and polynomial-time many-one reductions, and proves that the true closed quantified Boolean formulas (`TQBF`) form a `PSPACE`-complete problem. -To check that the formalization establishes this result, a reader only needs to -inspect the definitions and theorem statements in this file. Every public -definition and theorem statement depends only on this file, `Mathlib`, and -upstream `Cslib`'s multi-tape Turing machine model; `#check_abstract` -mechanically verifies that no internal `Complexitylib` declarations leak into -the statements, and Lean checks the proofs through `TQBFBridge`. +A reader can inspect the definitions and theorem statements here together with the displayed +shared-foundation appendix. `#check_abstract` audits their dependencies on upstream mathematics +and machine models; Lean checks the proofs through `TQBFBridge`. ## References @@ -88,7 +87,7 @@ excluded from `TQBF`. -/ def TQBF : Set Formula := {φ | φ.Closed ∧ φ.eval (fun _ => false) = true} -/-! ## Prefix-order binary encoding +/-! ## Representation details A formula is serialized in prefix (Polish) order as a list of `(kind, var)` tokens, where `kind ∈ {0, …, 7}` identifies the constructor (`var`, `top`, @@ -109,27 +108,13 @@ def Formula.tokens : Formula → List (ℕ × ℕ) | .ex v φ => (6, v) :: φ.tokens | .all v φ => (7, v) :: φ.tokens -/-- Frame a bitstring: write each bit `b` as `[true, b]`, then terminate with `[false]`. -/ -def frame (w : List Bool) : List Bool := - w.flatMap (fun b => [true, b]) ++ [false] - -/-- Encode a pair by framing the encoding of its first component and appending the encoding of -its second component. -/ -def encodePair {α β : Type} (encA : α → List Bool) (encB : β → List Bool) (p : α × β) : - List Bool := - frame (encA p.1) ++ encB p.2 - -/-- Encode a list by concatenating the framed encodings of its elements. -/ -def encodeList {α : Type} (enc : α → List Bool) (l : List α) : List Bool := - l.flatMap (frame ∘ enc) - /-- Encode a token `(kind, var)` as the pair of `kind` in unary and `var` in binary. -/ def encodeToken : ℕ × ℕ → List Bool := - encodePair (fun k => List.replicate k true) Nat.bits + Encoding.encodePair (fun k => List.replicate k true) Nat.bits /-- Encode a formula as the list encoding of its prefix-order tokens. -/ def encodeQBF (φ : Formula) : List Bool := - encodeList encodeToken φ.tokens + Encoding.encodeList encodeToken φ.tokens theorem encodeQBF_injective : Function.Injective encodeQBF := TQBFBridge.encodeQBF_injective @@ -145,17 +130,18 @@ theorem encodeQBF_injective : Function.Injective encodeQBF := def encQBF : Formula ↪ List Bool := ⟨encodeQBF, encodeQBF_injective⟩ -/-- Injective encoding of a single Boolean as a one-bit word `[b]`. -/ -def encBool : Bool ↪ List Bool := - ⟨fun b => [b], by intro a b h; injection h⟩ - /-! ## Polynomial space (`PSPACE`) and PSPACE-completeness +`Computation.PolyTime` below is total polynomial-time computation in the input bit length, +with its exact machine contract in the foundations appendix. Variable indices are in binary; +counting syntax nodes alone would not account for their lengths. + In upstream `Cslib`, `Turing.MultiTapeTM.ComputableInTimeAndSpace f encIn encOut t s` means that one deterministic binary multi-tape Turing machine with finitely many states halts on every input `encIn a` within `t a` steps and `s a` work-tape cells, outputting `encOut (f a)`. Read-only input cells and write-only output -cells are not charged to work space. +cells are not charged to work space. The time bound is unrestricted; termination is required, +but polynomial running time is not. -/ /-- A decision problem `A : Set α` (with instance encoding `enc`) belongs to @@ -165,22 +151,14 @@ number of work-tape cells bounded by a polynomial in the input bit length. -/ def PSPACE {α : Type} (enc : α ↪ List Bool) : Set (Set α) := {A | ∃ (f : α → Bool) (t : α → ℕ) (s : ℕ → ℕ), Cslib.PolynomiallyBounded s ∧ - Turing.MultiTapeTM.ComputableInTimeAndSpace f enc encBool + Turing.MultiTapeTM.ComputableInTimeAndSpace f enc Encoding.encBool t (fun a => s (enc a).length) ∧ ∀ a, a ∈ A ↔ f a = true} -/-- A total function `f : α → β` is computable in polynomial time with respect -to `encA` and `encB` if a deterministic multi-tape Turing machine computes it -within polynomially bounded time and space in the input bit length. -/ -def ComputableInPolyTime {α β : Type} (f : α → β) - (encA : α ↪ List Bool) (encB : β ↪ List Bool) : Prop := - ∃ t s : ℕ → ℕ, Cslib.PolynomiallyBounded t ∧ Cslib.PolynomiallyBounded s ∧ - Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength f encA encB t s - /-- Polynomial-time many-one reducibility between encoded decision problems. -/ def PolyTimeReducible {α β : Type} (encA : α ↪ List Bool) (encB : β ↪ List Bool) (A : Set α) (B : Set β) : Prop := - ∃ f : α → β, ComputableInPolyTime f encA encB ∧ ∀ a, a ∈ A ↔ f a ∈ B + ∃ f : α → β, Computation.PolyTime f encA encB ∧ ∀ a, a ∈ A ↔ f a ∈ B /-- A problem `B` is PSPACE-complete if it belongs to PSPACE and every PSPACE problem (over any instance type `α` and injective binary encoding `encA`) @@ -205,10 +183,12 @@ theorem tqbf_pspaceComplete : PSPACEComplete encQBF TQBF := (by constructor <;> intros <;> rfl) /-- -info: abstract audit passed for `ComplexityTests.Abstracts.TQBFAbstract`: 87 root -declarations, 130 dependencies checked +info: abstract audit passed for `ComplexityTests.Abstracts.TQBFAbstract`: +81 root declarations, 130 dependencies checked -/ #guard_msgs (whitespace := lax) in -#check_abstract ComplexityTests.Abstracts.TQBFAbstract +#check_abstract ComplexityTests.Abstracts.TQBFAbstract allowing [ + ComplexityAbstracts.Encoding, ComplexityAbstracts.Computation +] end ComplexityTests.Abstracts.TQBFAbstract diff --git a/abstracts/ComplexityAbstracts/TodaAbstract.lean b/abstracts/ComplexityAbstracts/TodaAbstract.lean index 782f148c6..335d11d8b 100644 --- a/abstracts/ComplexityAbstracts/TodaAbstract.lean +++ b/abstracts/ComplexityAbstracts/TodaAbstract.lean @@ -7,6 +7,8 @@ Authors: Samuel Schlesinger -- upstream: local-only (formal abstract library) import ComplexityAbstracts.Check +import ComplexityAbstracts.Encoding +import ComplexityAbstracts.Computation import ComplexityAbstracts.TodaBridge /-! # Toda's theorem @@ -21,11 +23,13 @@ hierarchy in polynomial time with counting access, without asserting the reverse The oracle counts certificates accepted by a deterministic verifier in polynomial time and answers queries about individual binary digits. One native polynomial clock governs the entire stateful interaction, including constructing queries and reading replies. Correctness holds for every -extension of valid bit answers to words outside the query encoding's image; the model below also -separates finite-uniform program syntax from fair-coin efficiency. +extension of valid bit answers to words outside the query encoding's image. The decision program +is deterministic. Its resource bound is expressed by exact realization on a clocked fair-coin +machine; the same interaction interface also supports randomized programs. -Lean checks the bridge, and the audit permits only the listed foundational program and machine -modules, with no complexity-class or Toda-theorem allowance. +The definitions and theorem statement below specify the claim. Lean checks the bridge, and the +audit permits only the listed foundational program and machine modules, with no complexity-class +or Toda-theorem allowance. ## References @@ -35,38 +39,40 @@ modules, with no complexity-class or Toda-theorem allowance. namespace ComplexityTests.Abstracts.TodaAbstract -/-- Frame each bit as `[true, b]` and terminate the word with `[false]`. -/ -def frame (w : List Bool) : List Bool := w.flatMap (fun b => [true, b]) ++ [false] - -/-- Encode a pair by framing its first component and appending its second component. -/ -def encodePair {α β : Type} (a : α → List Bool) (b : β → List Bool) (p : α × β) : - List Bool := frame (a p.1) ++ b p.2 - -theorem encodePair_injective {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) : - Function.Injective (encodePair a b) := TodaBridge.encodePair_injective a b - -theorem bits_injective : Function.Injective Nat.bits := TodaBridge.bits_injective +/-- Count the accepted binary strings of exactly `n` bits. -/ +def acceptCount {α : Type} (V : α × List Bool → Bool) (a : α) (n : ℕ) : ℕ := + (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = true).card -/-- Natural numbers are encoded by their canonical little-endian binary digits. -/ -def encNat : ℕ ↪ List Bool := ⟨Nat.bits, bits_injective⟩ +/-- A #P function counts witnesses of a fixed polynomial length accepted by one total +polynomial-time deterministic verifier. Counts are natural numbers in binary. -/ +def SharpP {α : Type} (enc : α ↪ List Bool) : Set (α → ℕ) := + {f | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), + Computation.PolyTimeVerifier enc V ∧ + ∀ a, f a = acceptCount V a (p.eval (enc a).length)} -/-- Pair encoding; `↪` records injectivity. -/ -def encPair {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) : α × β ↪ List Bool := - ⟨encodePair a b, encodePair_injective a b⟩ +/-- Alternating quantifiers over fixed-length blocks of bits, with an existential first +quantifier when `q=true`. Each subsequent block has the opposite quantifier. -/ +def Alternation : Bool → List ℕ → (List Bool → Prop) → Prop + | _, [], V => V [] + | true, n :: ns, V => ∃ w : List Bool, w.length = n ∧ Alternation false ns (fun v => V (w ++ v)) + | false, n :: ns, V => ∀ w : List Bool, w.length = n → Alternation true ns (fun v => V (w ++ v)) -/-- A Boolean is encoded by a single bit. -/ -def encBool : Bool ↪ List Bool := ⟨fun b => [b], by intro a b h; injection h⟩ +/-- The polynomial hierarchy: a fixed finite number of alternating polynomial-length +certificate blocks followed by a total polynomial-time verifier. The number of alternations +and the length polynomials are fixed for the language, not supplied as part of an instance. -/ +def PH {α : Type} (enc : α ↪ List Bool) : Set (Set α) := + {A | ∃ (ps : List (Polynomial ℕ)) (V : α × List Bool → Bool), + Computation.PolyTimeVerifier enc V ∧ + ∀ a, a ∈ A ↔ Alternation true (ps.map (fun p => p.eval (enc a).length)) + (fun w => V (a, w) = true)} -/-- Bitstrings encode themselves. -/ -def encBits : List Bool ↪ List Bool := Function.Embedding.refl _ +/-! The counting oracle is accessed by a deterministic program: it can return an answer or make +a word query, and later queries may depend on earlier replies. The probabilistic interface below +is used only to state its machine resource contract; it adds no random operation to this program. +-/ -/-- A single finite-state binary multi-tape machine computes `f` on every encoded input, -within polynomial time and work space. Inputs are read-only; outputs are write-only. -`Cslib.PolynomiallyBounded` means bounded above by some polynomial. -/ -def ComputableInPolyTime {α β : Type} (f : α → β) - (a : α ↪ List Bool) (b : β ↪ List Bool) : Prop := - ∃ t s : ℕ → ℕ, Cslib.PolynomiallyBounded t ∧ Cslib.PolynomiallyBounded s ∧ - Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength f a b t s +/-- Deterministic word-query programs; the syntax has queries but no random operation. -/ +abbrev QueryProgram (β : Type) := Cslib.OracleComp (fun _ : Unit × List Bool => List Bool) β /-- A terminating return/request tree. A private request indexed by `n` draws a fresh uniform `Fin (n+1)`; an external request sends `((), word)` and receives a word. Private draws do not @@ -77,12 +83,9 @@ abbrev InteractiveProgram (β : Type) := /-- One fixed finite fair-coin machine and one polynomial clock realize the entire joint law of the program's encoded result and the oracle's final state, against every stateful oracle. -Each live instruction consumes one fresh fair bit to select between two transitions. Ordinary -steps perform an upstream tape action, append at most one bit to a query buffer and move a -read-only reply head by at most one cell. A query step submits the buffer, installs the reply, -resets the reply head and clears the buffer. Each instruction costs one unit; the oracle's -computation is external. The bounded run observes its written output on halting or clock -exhaustion, so the definition does not pretend the unclocked machine has already halted. -/ +The clock charges computation, query writing, reply access and output writing. Each instruction +costs one unit; oracle computation is external. The bounded run returns its written output on +halting or clock exhaustion; it does not require the unclocked machine to halt. -/ def StrictOraclePPT {α β : Type} (enc : α ↪ List Bool) (out : β ↪ List Bool) (program : α → InteractiveProgram β) : Prop := ∃ (k : ℕ) (Control : Type) (_ : Finite Control) @@ -93,53 +96,25 @@ def StrictOraclePPT {α β : Type} (enc : α ↪ List Bool) (out : β ↪ List B Cslib.ProbOracleComp.runWith oracle (machine.runOracle (c * ((enc a).length + 1) ^ d) (enc a)) s -/-- Deterministic word-query programs; the syntax has queries but no random operation. -/ -abbrev QueryProgram (β : Type) := Cslib.OracleComp (fun _ : Unit × List Bool => List Bool) β - /-- An oracle language replies to each requested word with its one-bit membership verdict. -/ noncomputable def languageOracle (B : Set (List Bool)) (q : Unit × List Bool) : List Bool := [@decide (q.2 ∈ B) (Classical.propDecidable _)] -/-- Count the accepted binary strings of exactly `n` bits. -/ -def acceptCount {α : Type} (V : α × List Bool → Bool) (a : α) (n : ℕ) : ℕ := - (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = true).card - -/-- A #P function counts witnesses of a fixed polynomial length accepted by one total -polynomial-time deterministic verifier. Counts are natural numbers in binary. -/ -def SharpP {α : Type} (enc : α ↪ List Bool) : Set (α → ℕ) := - {f | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), - ComputableInPolyTime V (encPair enc encBits) encBool ∧ - ∀ a, f a = acceptCount V a (p.eval (enc a).length)} - -/-- Alternating quantifiers over fixed-length blocks of bits, with an existential first -quantifier when `q=true`. Each subsequent block has the opposite quantifier. -/ -def Alternation : Bool → List ℕ → (List Bool → Prop) → Prop - | _, [], V => V [] - | true, n :: ns, V => ∃ w : List Bool, w.length = n ∧ Alternation false ns (fun v => V (w ++ v)) - | false, n :: ns, V => ∀ w : List Bool, w.length = n → Alternation true ns (fun v => V (w ++ v)) - -/-- The polynomial hierarchy: a fixed finite number of alternating polynomial-length -certificate blocks followed by a total polynomial-time verifier. The number of alternations -and the length polynomials are fixed for the language, not supplied as part of an instance. -/ -def PH {α : Type} (enc : α ↪ List Bool) : Set (Set α) := - {A | ∃ (ps : List (Polynomial ℕ)) (V : α × List Bool → Bool), - ComputableInPolyTime V (encPair enc encBits) encBool ∧ - ∀ a, a ∈ A ↔ Alternation true (ps.map (fun p => p.eval (enc a).length)) - (fun w => V (a, w) = true)} - /-- An oracle language answers the bits of `f`: every valid query `(b,i)` returns the `i`th binary digit. Answers to words outside the encoding image are unrestricted. -/ def AnswersBits {β : Type} (enc : β ↪ List Bool) (f : β → ℕ) (B : Set (List Bool)) : Prop := - ∀ b i, encPair enc encNat (b, i) ∈ B ↔ (f b).testBit i + ∀ b i, Encoding.encPair enc Encoding.encNat (b, i) ∈ B ↔ (f b).testBit i /-- Deterministic polynomial time with a #P oracle, via bit queries. The program must decide the language against every extension of the valid bit answers to malformed query words. -Its native machine clock is polynomial uniformly over every stateful oracle. -/ +Its native machine clock is polynomial uniformly over every stateful oracle. Interpreting each +query through `ProbOracleComp.query` embeds the deterministic program into the shared interaction +model without drawing coins. The machine must realize that program's entire joint law exactly. -/ def PWithSharpPOracle {α : Type} (enc : α ↪ List Bool) : Set (Set α) := {A | ∃ (β : Type) (b : β ↪ List Bool) (f : β → ℕ), f ∈ SharpP b ∧ ∃ program : α → QueryProgram Bool, - StrictOraclePPT enc encBool + StrictOraclePPT enc Encoding.encBool (fun a => Cslib.OracleComp.interpret Cslib.ProbOracleComp.query (program a)) ∧ ∀ B : Set (List Bool), AnswersBits b f B → ∀ a, a ∈ A ↔ Cslib.OracleComp.interpret (m := Id) (languageOracle B) (program a) = true} @@ -162,12 +137,23 @@ theorem toda {α : Type} (enc : α ↪ List Bool) : PH enc ⊆ PWithSharpPOracle rw [hclass] exact TodaBridge.toda enc +/-! ## Representation details + +The fair-coin machine uses one independent fair bit at each live instruction to choose between +two transitions. Ordinary instructions perform an upstream tape action, append at most one bit +to a query buffer and move a read-only reply head by at most one cell. A query instruction submits +the buffer, installs the reply, resets the reply head and clears the buffer. Thus constructing a +query and accessing its answer are charged even though the oracle's own computation is external. +The output and final oracle state must agree for every handler, not just for the counting oracle. +-/ + /-- info: abstract audit passed for `ComplexityTests.Abstracts.TodaAbstract`: -25 root declarations, 237 dependencies checked +15 root declarations, 238 dependencies checked -/ #guard_msgs (whitespace := lax) in #check_abstract ComplexityTests.Abstracts.TodaAbstract allowing [ + ComplexityAbstracts.Encoding, ComplexityAbstracts.Computation, Complexity.Computability.Machines.Turing.MultiTape.Machine, Complexity.Computability.Machines.Turing.MultiTape.Machine.Program, Complexity.Computability.Machines.Turing.MultiTape.Probabilistic, diff --git a/abstracts/ComplexityAbstracts/TodaBridge.lean b/abstracts/ComplexityAbstracts/TodaBridge.lean index 3405953c1..85ca22931 100644 --- a/abstracts/ComplexityAbstracts/TodaBridge.lean +++ b/abstracts/ComplexityAbstracts/TodaBridge.lean @@ -47,31 +47,6 @@ def ComputableInPolyTime {α β : Type} (f : α → β) ∃ t s : ℕ → ℕ, Cslib.PolynomiallyBounded t ∧ Cslib.PolynomiallyBounded s ∧ Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength f a b t s -/-- Word-query programs with fresh private random bits. This foundational program type is an -explicit trusted model boundary, not a definition of an efficiency or complexity class. -/ -abbrev InteractiveProgram (β : Type) := - Cslib.ProbOracleComp (fun _ : Unit × List Bool => List Bool) β - -/-- One fixed finite fair-coin machine and one polynomial clock realize the entire joint law -of the program's encoded result and the oracle's final state, against every stateful oracle. -The clock charges constructing requests and reading replies; oracle computation is external. -/ -def StrictOraclePPT {α β : Type} (enc : α ↪ List Bool) (out : β ↪ List Bool) - (program : α → InteractiveProgram β) : Prop := - ∃ (k : ℕ) (Control : Type) (_ : Finite Control) - (machine : Turing.MultiTapePTM k Bool Control Unit) (c d : ℕ), - ∀ a (State : Type) - (oracle : Unit × List Bool → StateT State PMF (List Bool)) s, - Cslib.ProbOracleComp.runWith oracle (out <$> program a) s = - Cslib.ProbOracleComp.runWith oracle - (machine.runOracle (c * ((enc a).length + 1) ^ d) (enc a)) s - -/-- Deterministic word-query programs; the syntax has queries but no random operation. -/ -abbrev QueryProgram (β : Type) := Cslib.OracleComp (fun _ : Unit × List Bool => List Bool) β - -/-- An oracle language replies to each requested word with its one-bit membership verdict. -/ -noncomputable def languageOracle (B : Set (List Bool)) (q : Unit × List Bool) : List Bool := - [@decide (q.2 ∈ B) (Classical.propDecidable _)] - /-- Count the accepted binary strings of exactly `n` bits. -/ def acceptCount {α : Type} (V : α × List Bool → Bool) (a : α) (n : ℕ) : ℕ := (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = true).card @@ -99,6 +74,31 @@ def PH {α : Type} (enc : α ↪ List Bool) : Set (Set α) := ∀ a, a ∈ A ↔ Alternation true (ps.map (fun p => p.eval (enc a).length)) (fun w => V (a, w) = true)} +/-- Word-query programs with fresh private random bits. This foundational program type is an +explicit trusted model boundary, not a definition of an efficiency or complexity class. -/ +abbrev InteractiveProgram (β : Type) := + Cslib.ProbOracleComp (fun _ : Unit × List Bool => List Bool) β + +/-- One fixed finite fair-coin machine and one polynomial clock realize the entire joint law +of the program's encoded result and the oracle's final state, against every stateful oracle. +The clock charges constructing requests and reading replies; oracle computation is external. -/ +def StrictOraclePPT {α β : Type} (enc : α ↪ List Bool) (out : β ↪ List Bool) + (program : α → InteractiveProgram β) : Prop := + ∃ (k : ℕ) (Control : Type) (_ : Finite Control) + (machine : Turing.MultiTapePTM k Bool Control Unit) (c d : ℕ), + ∀ a (State : Type) + (oracle : Unit × List Bool → StateT State PMF (List Bool)) s, + Cslib.ProbOracleComp.runWith oracle (out <$> program a) s = + Cslib.ProbOracleComp.runWith oracle + (machine.runOracle (c * ((enc a).length + 1) ^ d) (enc a)) s + +/-- Deterministic word-query programs; the syntax has queries but no random operation. -/ +abbrev QueryProgram (β : Type) := Cslib.OracleComp (fun _ : Unit × List Bool => List Bool) β + +/-- An oracle language replies to each requested word with its one-bit membership verdict. -/ +noncomputable def languageOracle (B : Set (List Bool)) (q : Unit × List Bool) : List Bool := + [@decide (q.2 ∈ B) (Classical.propDecidable _)] + /-- An oracle language answers the bits of `f`: every valid query `(b,i)` returns the `i`th binary digit. Answers to words outside the encoding image are unrestricted. -/ def AnswersBits {β : Type} (enc : β ↪ List Bool) (f : β → ℕ) diff --git a/abstracts/ComplexityAbstracts/USTCONAbstract.lean b/abstracts/ComplexityAbstracts/USTCONAbstract.lean index daf2c691c..84fd30cb1 100644 --- a/abstracts/ComplexityAbstracts/USTCONAbstract.lean +++ b/abstracts/ComplexityAbstracts/USTCONAbstract.lean @@ -42,22 +42,36 @@ abbrev Instance := Σ n : ℕ, {adj : Fin n → Fin n → Bool // (∀ a b, adj a b = adj b a) ∧ (∀ a, adj a a = false)} × Fin n × Fin n +/-- The number of vertices of an instance. -/ +def Instance.vertexCount (I : Instance) : ℕ := I.1 + +/-- The symmetric, zero-diagonal adjacency matrix of an instance. -/ +def Instance.adjacency (I : Instance) : Fin I.vertexCount → Fin I.vertexCount → Bool := + I.2.1.val + +/-- The source vertex. Its existence ensures that the vertex count is positive. -/ +def Instance.source (I : Instance) : Fin I.vertexCount := I.2.2.1 + +/-- The target vertex. -/ +def Instance.target (I : Instance) : Fin I.vertexCount := I.2.2.2 + /-- The graph determined by the adjacency matrix. -/ -def graph (I : Instance) : SimpleGraph (Fin I.1) where - Adj a b := I.2.1.val a b = true +def graph (I : Instance) : SimpleGraph (Fin I.vertexCount) where + Adj a b := I.adjacency a b = true symm.symm a b h := (I.2.1.property.1 b a).trans h - loopless.irrefl a h := by simp only [I.2.1.property.2 a, Bool.false_eq_true] at h + loopless.irrefl a h := by simp only [Instance.adjacency, I.2.1.property.2 a, + Bool.false_eq_true] at h /-- Undirected s–t connectivity: a finite walk connects the distinguished vertices. -/ -def USTCON : Set Instance := {I | (graph I).Reachable I.2.2.1 I.2.2.2} +def USTCON : Set Instance := {I | (graph I).Reachable I.source I.target} -/-- Unary vertex count, source and target, separated by zero bits, followed by the matrix -row by row. Vertex indices range below `n`, so division and remainder select valid entries. -/ +/-- Encode the unary header `1^n 0 1^s 0 1^t 0`, then the adjacency matrix row by row. +`List.ofFn` lists coordinates in increasing order; flattening the list of rows gives exactly +`n²` matrix bits. This is the same binary encoding used by the machine theorem. -/ def encode (I : Instance) : List Bool := - List.replicate I.1 true ++ false :: (List.replicate I.2.2.1.val true ++ false :: - (List.replicate I.2.2.2.val true ++ false :: List.ofFn (fun i : Fin (I.1 * I.1) => - I.2.1.val ⟨i.val / I.1, Nat.div_lt_of_lt_mul i.isLt⟩ - ⟨i.val % I.1, Nat.mod_lt _ (Nat.pos_of_ne_zero (fun h => by simpa [h] using i.isLt))⟩))) + List.replicate I.vertexCount true ++ false :: (List.replicate I.source.val true ++ false :: + (List.replicate I.target.val true ++ false :: + (List.ofFn fun row => List.ofFn (I.adjacency row)).flatten)) theorem encode_injective : Function.Injective encode := USTCONBridge.encode_injective @@ -81,7 +95,7 @@ theorem ustcon_mem_l : USTCON ∈ L encInstance := USTCONBridge.ustcon_mem_l /-- info: abstract audit passed for `ComplexityTests.Abstracts.USTCONAbstract`: -15 root declarations, 74 dependencies checked +18 root declarations, 68 dependencies checked -/ #guard_msgs (whitespace := lax) in #check_abstract ComplexityTests.Abstracts.USTCONAbstract diff --git a/abstracts/ComplexityAbstracts/USTCONBridge.lean b/abstracts/ComplexityAbstracts/USTCONBridge.lean index f4dc1134c..78fce5930 100644 --- a/abstracts/ComplexityAbstracts/USTCONBridge.lean +++ b/abstracts/ComplexityAbstracts/USTCONBridge.lean @@ -7,6 +7,7 @@ Authors: Samuel Schlesinger -- upstream: local-only (formal abstract library) import Complexity.Computability.Complexity.Classes.LogSpace.USTCON +import Mathlib.Data.List.OfFn /-! # Transfer of Reingold's theorem along the exact adjacency-matrix encoding -/ @@ -21,22 +22,36 @@ abbrev Instance := Σ n : ℕ, {adj : Fin n → Fin n → Bool // (∀ a b, adj a b = adj b a) ∧ (∀ a, adj a a = false)} × Fin n × Fin n +/-- The number of vertices of an instance. -/ +def Instance.vertexCount (I : Instance) : ℕ := I.1 + +/-- The symmetric, zero-diagonal adjacency matrix of an instance. -/ +def Instance.adjacency (I : Instance) : Fin I.vertexCount → Fin I.vertexCount → Bool := + I.2.1.val + +/-- The source vertex. Its existence ensures that the vertex count is positive. -/ +def Instance.source (I : Instance) : Fin I.vertexCount := I.2.2.1 + +/-- The target vertex. -/ +def Instance.target (I : Instance) : Fin I.vertexCount := I.2.2.2 + /-- The graph determined by the adjacency matrix. -/ -def graph (I : Instance) : SimpleGraph (Fin I.1) where - Adj a b := I.2.1.val a b = true +def graph (I : Instance) : SimpleGraph (Fin I.vertexCount) where + Adj a b := I.adjacency a b = true symm.symm a b h := (I.2.1.property.1 b a).trans h - loopless.irrefl a h := by simp only [I.2.1.property.2 a, Bool.false_eq_true] at h + loopless.irrefl a h := by simp only [Instance.adjacency, I.2.1.property.2 a, + Bool.false_eq_true] at h /-- Undirected s–t connectivity: a finite walk connects the distinguished vertices. -/ -def USTCON : Set Instance := {I | (graph I).Reachable I.2.2.1 I.2.2.2} +def USTCON : Set Instance := {I | (graph I).Reachable I.source I.target} -/-- Unary vertex count, source and target, separated by zero bits, followed by the matrix -row by row. Vertex indices range below `n`, so division and remainder select valid entries. -/ +/-- Encode the unary header `1^n 0 1^s 0 1^t 0`, then the adjacency matrix row by row. +`List.ofFn` lists coordinates in increasing order; flattening the list of rows gives exactly +`n²` matrix bits. This is the same binary encoding used by the machine theorem. -/ def encode (I : Instance) : List Bool := - List.replicate I.1 true ++ false :: (List.replicate I.2.2.1.val true ++ false :: - (List.replicate I.2.2.2.val true ++ false :: List.ofFn (fun i : Fin (I.1 * I.1) => - I.2.1.val ⟨i.val / I.1, Nat.div_lt_of_lt_mul i.isLt⟩ - ⟨i.val % I.1, Nat.mod_lt _ (Nat.pos_of_ne_zero (fun h => by simpa [h] using i.isLt))⟩))) + List.replicate I.vertexCount true ++ false :: (List.replicate I.source.val true ++ false :: + (List.replicate I.target.val true ++ false :: + (List.ofFn fun row => List.ofFn (I.adjacency row)).flatten)) def toInternal (I : Instance) : Cslib.Complexity.USTCONInstance := ⟨I.1, I.2.1.val, I.2.1.property.1, I.2.1.property.2, I.2.2.1, I.2.2.2⟩ @@ -48,7 +63,28 @@ theorem of_to (I : Instance) : ofInternal (toInternal I) = I := rfl theorem to_of (I : Cslib.Complexity.USTCONInstance) : toInternal (ofInternal I) = I := rfl -theorem encode_eq (I : Instance) : encode I = Cslib.Complexity.encUSTCON (toInternal I) := rfl +theorem encode_eq (I : Instance) : encode I = Cslib.Complexity.encUSTCON (toInternal I) := by + have matrix_eq : (List.ofFn fun row => List.ofFn (I.adjacency row)).flatten = + (toInternal I).matrix := by + rw [Cslib.Complexity.USTCONInstance.matrix, List.ofFn_mul] + congr 1 + apply congrArg List.ofFn + funext row + apply congrArg List.ofFn + funext col + change I.adjacency row col = I.adjacency _ _ + congr 1 + · apply Fin.ext + change row.val = (row.val * I.vertexCount + col.val) / I.vertexCount + rw [Nat.add_comm, Nat.add_mul_div_right _ _ (Fin.pos row), + Nat.div_eq_of_lt col.isLt, Nat.zero_add] + · apply Fin.ext + change col.val = (row.val * I.vertexCount + col.val) % I.vertexCount + rw [Nat.add_comm, Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt col.isLt] + change _ = List.replicate I.vertexCount true ++ false :: + (List.replicate I.source.val true ++ false :: + (List.replicate I.target.val true ++ false :: (toInternal I).matrix)) + rw [encode, matrix_eq] theorem encode_injective : Function.Injective encode := by intro I J h @@ -77,6 +113,9 @@ theorem ustcon_mem_l : USTCON ∈ L encInstance := by refine ⟨fun I => f (toInternal I), ⟨fun I => t (toInternal I), c, k, State, hfin, M, ?_⟩, fun I => hA (toInternal I)⟩ intro I + change M.ComputesInTimeAndSpace (encode I) _ _ + (c * (Nat.log2 (encode I).length + 1)) + rw [encode_eq] exact hM (toInternal I) end ComplexityTests.Abstracts.USTCONBridge diff --git a/abstracts/ComplexityAbstracts/WordRAMAbstract.lean b/abstracts/ComplexityAbstracts/WordRAMAbstract.lean index 2f212c90b..45cf18329 100644 --- a/abstracts/ComplexityAbstracts/WordRAMAbstract.lean +++ b/abstracts/ComplexityAbstracts/WordRAMAbstract.lean @@ -213,7 +213,7 @@ of registers, decides it. -/ def DecidableInTime {α : Type*} (A : Set α) (encode : α → List ℕ) (T bits : α → ℕ) : Prop := ∃ r, ∃ p : Program r, Decides p A encode T bits -/-! ## Main theorems +/-! ## Connection to the library Two theorems say that the machine of this file is the library's word RAM `Cslib.WordRAM` over its exact basis `Cslib.WordRAM.Basis.exact`. Names with the prefix `Cslib.WordRAM.` are from the diff --git a/abstracts/README.md b/abstracts/README.md index 12eba80a4..5fed338d1 100644 --- a/abstracts/README.md +++ b/abstracts/README.md @@ -4,9 +4,10 @@ The catalogue promotes twelve major result groups. Each has a checked Lean abstr definitions needed to understand its statement, a bridge to the library proof, and an audited dependency boundary. Some abstracts also allowlist a few library modules for foundational models (for example circuit signatures or oracle runs); each such abstract names them in its docstring, and -a reader must inspect them as well. The generated PDFs display those definitions and statements with -proof bodies omitted. Lean checks the proofs; independent review must still check their intended -meaning. +a reader must inspect them as well. The generated PDFs present the mathematical definitions and +selected statements first, followed by exact representation details and any shared foundations in +appendices. Proof bodies are omitted. Lean checks the proofs; independent review must still check +their intended meaning. The [combined PDF](https://github.com/cslib-community/complexitylib/releases/download/formal-abstracts/catalogue.pdf) and individual PDFs are published from main by the **Formal abstract PDFs** workflow. PR builds @@ -90,6 +91,27 @@ artifact selection follows [download-artifact v4](https://github.com/actions/dow ## Layout and sources +The source section `/-! ## Representation details ... -/` marks definitions and explanations +to display in an appendix. The group ends at the next `##` section heading. Its definitions are +retained in full; selected theorem statements must remain in the main presentation. These are +presentation conventions in comments, not new Lean syntax. + +An entry using shared definitions lists their modules in its `foundations` array, for example +`["ComplexityAbstracts.Encoding", "ComplexityAbstracts.Computation"]`. The list must exactly match +the abstract's direct foundation imports and their transitive foundation imports. The audit helper +and proof bridges are excluded from that display check; Lean's `#check_abstract` still checks the +actual elaborated dependency boundary, including dependencies of allowed definitions. A listed +foundation cannot be another abstract or bridge, and missing, duplicate, unused or cyclic +foundation modules fail validation. + +Individual PDFs include the needed foundations with their definitions, theorem signatures, +namespaces and source links. The combined catalogue displays each foundation once, after the +selected abstracts. `provenance.json` records each foundation's source digest and declaration +links, and a source change during rendering invalidates the build. Single-file Markdown and TeX +previews also include imported foundations and identify their local source digests. Moving a +definition to an appendix does not establish an encoding-invariance or model-equivalence theorem; +any such change still needs a checked correspondence in Lean. + The typography, syntax colors and pale code boxes adapt Erik Demaine and Stefan Langerman’s [translation-tiling paper style](https://github.com/edemaine/translation-tiling-paper/blob/5309313e662377d2efb353acba454859469606bd/paper.texlish) and [Lean snippet extraction workflow](https://github.com/edemaine/translation-tiling-paper/blob/5309313e662377d2efb353acba454859469606bd/figures/extract_lean_snippets.py). diff --git a/abstracts/catalogue.json b/abstracts/catalogue.json index e48ab8dd3..a3d85d161 100644 --- a/abstracts/catalogue.json +++ b/abstracts/catalogue.json @@ -11,7 +11,11 @@ ], "summary": "Every efficiently checkable bit-string problem reduces in polynomial time to satisfiability.", "scope": "Explicit CNF encoding, total native-machine reductions, and UNSAT coNP-completeness.", - "namespace": "ComplexityTests.Abstracts.CookLevinAbstract" + "namespace": "ComplexityTests.Abstracts.CookLevinAbstract", + "foundations": [ + "ComplexityAbstracts.Encoding", + "ComplexityAbstracts.Computation" + ] }, { "id": "pcp", @@ -22,7 +26,11 @@ ], "summary": "NP proofs can be checked with logarithmic randomness and constantly many nonadaptive queries.", "scope": "Perfect completeness, soundness at most one half, and explicit native efficiency; construction constants are large.", - "namespace": "ComplexityTests.Abstracts.PCPAbstract" + "namespace": "ComplexityTests.Abstracts.PCPAbstract", + "foundations": [ + "ComplexityAbstracts.Encoding", + "ComplexityAbstracts.Computation" + ] }, { "id": "fagin", @@ -33,7 +41,11 @@ ], "summary": "Existential second-order logic captures precisely the isomorphism-invariant NP properties of finite relational structures.", "scope": "Finite relational signatures, explicit encodings, empty universes and nullary relations.", - "namespace": "ComplexityTests.Abstracts.FaginAbstract" + "namespace": "ComplexityTests.Abstracts.FaginAbstract", + "foundations": [ + "ComplexityAbstracts.Encoding", + "ComplexityAbstracts.Computation" + ] }, { "id": "savitch", @@ -77,7 +89,11 @@ ], "summary": "Every problem in the polynomial hierarchy is decidable in polynomial time with an exact counting oracle.", "scope": "Witness counts and oracle bit answers are explicit; correctness holds for every extension of valid oracle answers.", - "namespace": "ComplexityTests.Abstracts.TodaAbstract" + "namespace": "ComplexityTests.Abstracts.TodaAbstract", + "foundations": [ + "ComplexityAbstracts.Encoding", + "ComplexityAbstracts.Computation" + ] }, { "id": "barrington", @@ -124,7 +140,11 @@ ], "summary": "One-wayness yields pseudorandomness, from an extra output bit to functions secure against adaptive oracle queries.", "scope": "Uniform probabilistic polynomial time with explicit native evaluators, negligible advantage and full stateful oracle semantics; asymptotic security, not a concrete implementation audit.", - "namespace": "ComplexityTests.Abstracts.CryptographyAbstract" + "namespace": "ComplexityTests.Abstracts.CryptographyAbstract", + "foundations": [ + "ComplexityAbstracts.Encoding", + "ComplexityAbstracts.Computation" + ] }, { "id": "resolution", diff --git a/scripts/abstract_to_tex.py b/scripts/abstract_to_tex.py index d221e3423..f176217ec 100644 --- a/scripts/abstract_to_tex.py +++ b/scripts/abstract_to_tex.py @@ -2,10 +2,13 @@ """Render a Complexitylib *Abstract.lean file into Markdown or pdflatex-ready LaTeX.""" import argparse +import hashlib from pathlib import Path import re import sys +from proof_lengths import CHAR_LITERAL + UNICODE_TO_TEX_MATH = { "ℕ": r"\mathbb{N}", @@ -110,6 +113,93 @@ } +def lean_code(text: str) -> str: + """Mask comments and literals, preserving source positions and line numbers.""" + result, index, depth = list(text), 0, 0 + while index < len(text): + if depth: + if text.startswith("/-", index): + depth += 1 + width = 2 + elif text.startswith("-/", index): + depth -= 1 + width = 2 + else: + width = 1 + elif text.startswith("/-", index): + depth, width = 1, 2 + elif text.startswith("--", index): + end = text.find("\n", index) + width = (len(text) if end < 0 else end) - index + elif text[index] == "'" and (literal := CHAR_LITERAL.match(text, index)): + width = len(literal.group()) + elif text[index] == '"' or (text[index] == "r" and re.match(r'r#+"', text[index:])): + raw = re.match(r'r(#+)"', text[index:]) + if raw: + close = '"' + raw.group(1) + end = text.find(close, index + len(raw.group())) + width = (len(text) if end < 0 else end + len(close)) - index + else: + end = index + 1 + while end < len(text): + if text[end] == "\\": + end += 2 + elif text[end] == '"': + end += 1 + break + else: + end += 1 + width = end - index + else: + index += 1 + continue + for offset in range(index, min(index + width, len(text))): + if text[offset] != "\n": + result[offset] = " " + index += width + return "".join(result) + + +def module_source_path(module: str, root: Path) -> Path: + """Resolve a module in the dedicated abstract library, never an arbitrary path.""" + if not isinstance(module, str) or not re.fullmatch( + r"ComplexityAbstracts\.[A-Za-z_][A-Za-z0-9_]*", module): + raise ValueError(f"Not a formal-abstract module: {module}") + return Path(root).joinpath("abstracts", *module.split(".")).with_suffix(".lean") + + +def foundation_modules(source: Path, root: Path) -> list[str]: + """Find directly imported shared foundations and their dependency closure in source order. + + Bridges and the audit helper supply proofs, not displayed definitions. Imports from outside + the abstract library are handled by Lean's dependency audit rather than this display check. + """ + ordered, visiting, visited = [], set(), set() + + def visit(path): + for match in re.finditer(r"^\s*(?:(?:public|meta)\s+)*import\s+([^\n]+)", + lean_code(path.read_text()), re.MULTILINE): + for module in match.group(1).split(): + if not module.startswith("ComplexityAbstracts."): + continue + dependency = module_source_path(module, root) + if module == "ComplexityAbstracts.Check" or module.endswith("Bridge"): + continue + if module.endswith("Abstract"): + raise ValueError(f"A shared foundation cannot be another abstract: {module}") + if module in visiting: + raise ValueError(f"Cyclic shared foundations: {module}") + if module not in visited: + visiting.add(module) + visit(dependency) + visiting.remove(module) + visited.add(module) + ordered.append(module) + + visit(Path(source)) + return ordered + + def parse_abstract(text: str): """Extract the title, module introduction, and alternating docstring/code sections.""" mod_match = re.search(r"/-\!\s*#\s*([^\n]+)\n(.*?)-/", text, re.DOTALL) @@ -139,18 +229,51 @@ def parse_abstract(text: str): pos = 0 for m in re.finditer(r"(/-\!(.*?)-/|/--(.*?)-/)", body, re.DOTALL): code_before = body[pos:m.start()].strip() - if code_before and sections: - sections[-1]["code"] += ("\n\n" if sections[-1]["code"] else "") + code_before + if code_before: + if not sections: + sections.append({"kind": "section", "doc": "", "code": code_before}) + else: + sections[-1]["code"] += ("\n\n" if sections[-1]["code"] else "") + code_before is_section = m.group(1).startswith("/-!") doc = (m.group(2) if is_section else m.group(3)).strip() sections.append({"kind": "section" if is_section else "decl", "doc": doc, "code": ""}) pos = m.end() trailing = body[pos:].strip() - if trailing and sections: - sections[-1]["code"] += ("\n\n" if sections[-1]["code"] else "") + trailing + if trailing: + if not sections: + sections.append({"kind": "section", "doc": "", "code": trailing}) + else: + sections[-1]["code"] += ("\n\n" if sections[-1]["code"] else "") + trailing return title, intro, sections +def section_heading(item: dict): + return (re.match(r"^##\s+([^\n]+)\n?(.*)", item["doc"], re.DOTALL) + if item["kind"] == "section" else None) + + +def split_sections(sections: list[dict]) -> tuple[list[dict], list[dict]]: + """Keep the mathematical presentation first and move marked representation details last.""" + main, details, destination = [], [], "main" + for item in sections: + heading = section_heading(item) + if heading: + destination = "details" if heading.group(1).strip() == "Representation details" else "main" + (details if destination == "details" else main).append(item) + return main, details + + +def presentation_sections(sections: list[dict]) -> list[dict]: + main, details = split_sections(sections) + if not details: + return main + appendix = [{"kind": "section", "doc": "## Appendix: representation details", "code": ""}] + for item in details: + heading = section_heading(item) + appendix.append({**item, "doc": heading.group(2).strip()} if heading else item) + return main + appendix + + def strip_theorem_proof(block: str) -> str: """Strip the proof body after the top-level `:=` of a theorem declaration.""" depth = 0 @@ -173,6 +296,28 @@ def strip_theorem_proof(block: str) -> str: ) +def declaration_body(block: str) -> str: + """Skip leading Lean attributes without interpreting their quoted strings as syntax.""" + masked = lean_code(block) + pos = len(masked) - len(masked.lstrip()) + while masked.startswith("@[", pos): + depth, end = 1, pos + 2 + while end < len(masked) and depth: + depth += (masked[end] == "[") - (masked[end] == "]") + end += 1 + if depth: + return block[pos:] + pos = end + while pos < len(masked) and masked[pos].isspace(): + pos += 1 + return block[pos:] + + +def theorem_name(block: str): + match = re.match(r"(?:private\s+)?(?:theorem|lemma)\s+([^\s:{(]+)", declaration_body(block)) + return match.group(1) if match else None + + def clean_code_for_display(code: str, is_undocumented_tail: bool = False) -> str: """Keep definitions and theorem signatures while eliding proof bodies. @@ -187,9 +332,9 @@ def clean_code_for_display(code: str, is_undocumented_tail: bool = False) -> str block = block.strip() if not block: continue - if INJECTIVITY_HELPER_RE.match(block) and (idx > 0 or is_undocumented_tail): + if INJECTIVITY_HELPER_RE.match(declaration_body(block)) and (idx > 0 or is_undocumented_tail): continue - if re.match(r"^(?:private\s+)?theorem\s+", block): + if theorem_name(block): kept.append(strip_theorem_proof(block)) else: # Replace inline proof terms `, by ...⟩` inside structure constructors with `, _⟩` @@ -224,10 +369,10 @@ def escape_tex_code_line(line: str) -> str: def escape_tex_prose(text: str) -> str: """Convert docstring prose (with inline `...` code spans and **bold**) into pdflatex.""" # Split by inline code spans `...` first so `**` inside code is untouched - parts = re.split(r"(`[^`]+`|\[[^\[\]]+\]\[[A-Za-z0-9_:.-]+\])", text) + parts = re.split(r"(`[^`]+`|\[[^\[\]]+\]\s*\[[A-Za-z0-9_:.-]+\])", text) rendered = [] for part in parts: - reference = re.fullmatch(r"\[([^\[\]]+)\]\[([A-Za-z0-9_:.-]+)\]", part) + reference = re.fullmatch(r"\[([^\[\]]+)\]\s*\[([A-Za-z0-9_:.-]+)\]", part) if reference: rendered.append(escape_tex_prose(reference.group(1)) + r" {\footnotesize (" + escape_tex_prose(reference.group(2)) + ")}") @@ -258,9 +403,17 @@ def render_tex_intro(intro: str) -> list[str]: lines = [] in_list = False item_parts = [] + paragraph = [] + + def flush_paragraph(): + if paragraph: + lines.append(escape_tex_prose(" ".join(paragraph))) + paragraph.clear() + for raw in intro.splitlines(): line = raw.strip() if line.startswith("* "): + flush_paragraph() if not in_list: lines.append("\\begin{itemize}\\raggedright") in_list = True @@ -279,18 +432,22 @@ def render_tex_intro(intro: str) -> list[str]: in_list = False heading = re.match(r"^##\s*(.+)$", line) if heading: + flush_paragraph() lines.append(f"\\subsubsection*{{{escape_tex_prose(heading.group(1).strip())}}}") + elif line: + paragraph.append(line) else: - lines.append(escape_tex_prose(line)) + flush_paragraph() if in_list: lines.append("\\item{} " + escape_tex_prose(" ".join(item_parts))) lines.append("\\end{itemize}") + flush_paragraph() return lines def render_tex(title: str, intro: str, sections: list[dict]) -> str: lines = [f"\\subsection{{{escape_tex_prose(title)}}}", "", *render_tex_intro(intro), ""] - for item in sections: + for item in presentation_sections(sections): doc = item["doc"] if item["kind"] == "section": m = re.match(r"^##\s*([^\n]+)\n?(.*)", doc, re.DOTALL) @@ -319,7 +476,7 @@ def render_tex(title: str, intro: str, sections: list[dict]) -> str: def render_markdown(title: str, intro: str, sections: list[dict]) -> str: lines = [f"# {title}", "", intro, ""] - for item in sections: + for item in presentation_sections(sections): lines.append(item["doc"]) code = clean_code_for_display(item["code"], is_undocumented_tail=(item["kind"] == "section")) if code: @@ -328,16 +485,34 @@ def render_markdown(title: str, intro: str, sections: list[dict]) -> str: return "\n".join(lines).strip() + "\n" +def render_source(path: Path, format: str) -> str: + """Render one source and its shared foundations for a standalone local preview.""" + path = path.resolve() + renderer = render_tex if format == "tex" else render_markdown + result = renderer(*parse_abstract(path.read_text())) + root = path.parent.parent.parent + modules = foundation_modules(path, root) + for module in modules: + source = module_source_path(module, root) + title, intro, sections = parse_abstract(source.read_text()) + sha = hashlib.sha256(source.read_bytes()).hexdigest() + provenance = f"Source: `{source.relative_to(root)}`. SHA256: `{sha}`." + if format == "markdown": + provenance = f"[Lean source]({source.as_uri()}). SHA256: `{sha}`." + result += "\n" + renderer("Shared foundation: " + title, + provenance + "\n\n" + intro, sections) + return result + + def main(): parser = argparse.ArgumentParser(description=__doc__) parser.add_argument("path", type=Path, help="Path to *Abstract.lean file") parser.add_argument("--format", choices=("markdown", "tex"), default="markdown") args = parser.parse_args() - title, intro, sections = parse_abstract(args.path.read_text()) - if args.format == "tex": - sys.stdout.write(render_tex(title, intro, sections)) - else: - sys.stdout.write(render_markdown(title, intro, sections)) + try: + sys.stdout.write(render_source(args.path, args.format)) + except (OSError, ValueError) as error: + parser.exit(1, f"Abstract render failed: {error}\n") if __name__ == "__main__": diff --git a/scripts/build_abstracts.py b/scripts/build_abstracts.py index 8904da6fe..80dd4f5be 100644 --- a/scripts/build_abstracts.py +++ b/scripts/build_abstracts.py @@ -13,7 +13,6 @@ import xml.etree.ElementTree as ET import abstract_to_tex as render -from proof_lengths import CHAR_LITERAL ROOT = Path(__file__).resolve().parents[1] @@ -45,9 +44,27 @@ \definecolor{leanblue}{RGB}{41,110,166} \definecolor{leangreen}{RGB}{38,128,89} \hypersetup{colorlinks=true,urlcolor=leanblue,linkcolor=leanblue} +\tcbset{leandeclarationmeasure/.style={}} \newtcolorbox{leanbox}{breakable,enhanced,colback=black!3,colframe=black!45, boxrule=0.5pt,arc=2pt,left=7pt,right=7pt,top=5pt,bottom=5pt, - before skip=7pt,after skip=9pt} + before skip=7pt,after skip=9pt,leandeclarationmeasure} +% Measure a declaration's prose and code at their actual display width. Keep the pair +% together only below 35% of the text height; larger declarations retain breakable boxes. +% environ is already required by tcolorbox. These bodies contain display text, not counters. +\newsavebox{\leandeclarationbox} +\NewEnviron{leandeclaration}{% + \par + \sbox{\leandeclarationbox}{% + \begin{minipage}{\linewidth} + \setlength{\parskip}{0.45em} + \tcbset{leandeclarationmeasure/.style={unbreakable}}% + \BODY + \end{minipage}}% + \ifdim\dimexpr\ht\leandeclarationbox+\dp\leandeclarationbox\relax<0.35\textheight + \noindent\usebox{\leandeclarationbox}\par + \else + \BODY + \fi} \setlength{\parindent}{0pt} \setlength{\parskip}{0.45em} \setlength{\emergencystretch}{2em} @@ -70,59 +87,11 @@ def git(root, *args): def module_source_path(module, root=ROOT): - """Resolve the dedicated abstract library's modules within its configured source root.""" - if not isinstance(module, str) or not re.fullmatch( - r"ComplexityAbstracts\.[A-Za-z_][A-Za-z0-9_]*", module): - raise ValueError(f"Not a formal-abstract module: {module}") - return Path(root).joinpath("abstracts", *module.split(".")).with_suffix(".lean") + return render.module_source_path(module, root) def _lean_code(text): - """Mask comments and strings while preserving source positions and line numbers.""" - result, index, depth = list(text), 0, 0 - while index < len(text): - if depth: - if text.startswith("/-", index): - depth += 1 - width = 2 - elif text.startswith("-/", index): - depth -= 1 - width = 2 - else: - width = 1 - elif text.startswith("/-", index): - depth, width = 1, 2 - elif text.startswith("--", index): - end = text.find("\n", index) - width = (len(text) if end < 0 else end) - index - # A quote directly after an identifier character is part of the name (`lemma'`). - elif text[index] == "'" and (literal := CHAR_LITERAL.match(text, index)): - width = literal.end() - index - elif text[index] == '"' or (text[index] == "r" and re.match(r'r#+"', text[index:])): - raw = re.match(r'r(#+)"', text[index:]) - if raw: - close = '"' + raw.group(1) - end = text.find(close, index + len(raw.group())) - width = (len(text) if end < 0 else end + len(close)) - index - else: - end = index + 1 - while end < len(text): - if text[end] == "\\": - end += 2 - elif text[end] == '"': - end += 1 - break - else: - end += 1 - width = end - index - else: - index += 1 - continue - for offset in range(index, min(index + width, len(text))): - if text[offset] != "\n": - result[offset] = " " - index += width - return "".join(result) + return render.lean_code(text) def _namespace_contexts(text): @@ -155,6 +124,28 @@ def declaration_line(text, name): return matches[0] +def entry_foundations(entry, root=ROOT): + """Require the manifest to name exactly the source's imported foundation closure.""" + listed = entry.get("foundations", []) + if not isinstance(listed, list) or any(not isinstance(module, str) for module in listed): + raise ValueError(f"Foundations must be a list of module names in {entry['id']}") + if len(listed) != len(set(listed)): + raise ValueError(f"Duplicate foundation in {entry['id']}") + for module in listed: + path = module_source_path(module, root) + if module == "ComplexityAbstracts.Check" or module.endswith(("Abstract", "Bridge")): + raise ValueError(f"Not a shared foundation: {module}") + if not path.is_file(): + raise ValueError(f"Missing shared foundation source: {module}") + render.split_sections(render.parse_abstract(path.read_text())[2]) + expected = render.foundation_modules(module_source_path(entry["module"], root), root) + missing, unused = set(expected) - set(listed), set(listed) - set(expected) + if missing or unused: + raise ValueError(f"Foundation manifest mismatch in {entry['id']}: " + f"missing {sorted(missing)}, unused {sorted(unused)}") + return expected + + def load_catalogue(manifest, root=ROOT): data = json.loads(Path(manifest).read_text()) if not isinstance(data, dict) or not isinstance(data.get("title"), str) or not data["title"].strip(): @@ -183,6 +174,7 @@ def load_catalogue(manifest, root=ROOT): r"[A-Za-z_][A-Za-z0-9_]*(?:\.[A-Za-z_][A-Za-z0-9_]*)*", namespace): raise ValueError(f"Invalid abstract namespace: {namespace}") text = source.read_text() + main_sections, _ = render.split_sections(render.parse_abstract(text)[2]) declared, contexts = _namespace_contexts(text) if namespace not in declared: raise ValueError(f"Abstract namespace {namespace} is not declared in {source}") @@ -204,6 +196,14 @@ def load_catalogue(manifest, root=ROOT): raise ValueError(f"Headline is outside namespace {namespace}: {name}") if not re.match(r"\s*(?:theorem|lemma)\s", text.splitlines()[line - 1]): raise ValueError(f"Selected headline is not a theorem: {name}") + main_theorems = set(re.findall( + r"^\s*(?:theorem|lemma)\s+([^\s:{(]+)", + "\n\n".join(_lean_code(item["code"]) for item in main_sections), re.MULTILINE)) + outside_main = {name.rsplit(".", 1)[-1] for name in [*headlines, *supporting]} - main_theorems + if outside_main: + raise ValueError(f"Selected statements must be in the main presentation: " + f"{sorted(outside_main)}") + entry_foundations(entry, root) return entries @@ -232,7 +232,84 @@ def highlighted_line(line): return "".join(pieces) -def render_entry(entry, repository, sha, dirty, root=ROOT): +def render_sections(sections, selected=None): + """Display all definitions, and either all theorem signatures or an explicit selection.""" + lines, displayed = [], set() + for item in sections: + item_lines = [] + code = render.clean_code_for_display(item["code"], + is_undocumented_tail=item["kind"] == "section") + kept = [] + for block in re.split(r"\n\s*\n", code): + theorem = render.theorem_name(block) + if not theorem or selected is None or theorem in selected: + kept.append(block) + if theorem: + displayed.add(theorem) + code = "\n\n".join(kept).strip() + if item["kind"] == "decl" and item["code"].strip() and not code: + continue + heading = render.section_heading(item) + if heading: + item_lines.extend([r"\subsection*{" + render.escape_tex_prose(heading.group(1).strip()) + "}", + render.escape_tex_prose(heading.group(2).strip())]) + else: + item_lines.append(render.escape_tex_prose(item["doc"])) + if code: + code_lines = [highlighted_line(line) or "~" for line in code.splitlines()] + item_lines.extend([r"\begin{leanbox}\small\ttfamily\raggedright\noindent", + " \\\\\n".join(code_lines), r"\par\end{leanbox}"]) + if item["kind"] == "decl" and code: + lines.extend([r"\begin{leandeclaration}", *item_lines, r"\end{leandeclaration}"]) + else: + lines.extend(item_lines) + return "\n\n".join(lines), displayed + + +def foundation_record(module, repository, sha, root=ROOT): + source = module_source_path(module, root) + text = source.read_text() + declared, contexts = _namespace_contexts(text) + relative = source.relative_to(root) + declarations = [] + for number, line in enumerate(_lean_code(text).splitlines(), 1): + match = re.match(r"\s*(?:(?:private|noncomputable)\s+)?" + r"(?:def|abbrev|theorem|lemma|inductive|structure)\s+([\w'.]+)", line) + if match: + name = ".".join(filter(None, (contexts[number], match.group(1)))) + declarations.append({"declaration": name, "line": number, + "url": source_url(repository, sha, relative, number)}) + return {"module": module, "source": str(relative), "source_sha256": digest(source), + "url": source_url(repository, sha, relative), "namespaces": sorted(declared), + "declarations": declarations} + + +def render_foundations(modules, repository, sha, root=ROOT): + if not modules: + return "" + lines = [r"\section*{Appendix: shared foundations}", + "These checked definitions specify the representations and machine bounds used " + "above. They are displayed once here; their Lean sources remain part of the " + "document's provenance."] + for module in dict.fromkeys(modules): + source = module_source_path(module, root) + title, intro, sections = render.parse_abstract(source.read_text()) + record = foundation_record(module, repository, sha, root) + lines.extend([r"\subsection*{" + render.escape_tex_prose(title) + "}", + r"{\small " + link(record["url"], "Lean source") + ". Namespaces: " + + ", ".join(render.escape_tex_prose("`" + ns + "`") + for ns in record["namespaces"]) + ".}"]) + if record["declarations"]: + lines.append(r"{\small Declarations: " + ", ".join( + link(item["url"], render.escape_tex_prose( + "`" + item["declaration"].rsplit(".", 1)[-1] + "`")) + for item in record["declarations"]) + ".}") + lines.extend([*render.render_tex_intro(intro), + render_sections(render.presentation_sections(sections))[0]]) + return "\n\n".join(lines) + "\n" + + +def render_entry(entry, repository, sha, dirty, root=ROOT, *, include_foundations=True): source = module_source_path(entry["module"], root) text = source.read_text() _, intro, sections = render.parse_abstract(text) @@ -256,33 +333,21 @@ def render_entry(entry, repository, sha, dirty, root=ROOT): r"\par\emph{Scope.} " + render.escape_tex_prose(entry["scope"]) + r"\end{quote}", "", *render.render_tex_intro(intro), ""]) selected = {name.rsplit(".", 1)[-1] for name in displayed_names} - displayed = set() - for item in sections: - code = render.clean_code_for_display(item["code"], - is_undocumented_tail=item["kind"] == "section") - kept = [] - for block in re.split(r"\n\s*\n", code): - theorem = re.match(r"(?:private\s+)?(?:theorem|lemma)\s+(\S+)", block) - if not theorem or theorem.group(1) in selected: - kept.append(block) - if theorem: - displayed.add(theorem.group(1)) - code = "\n\n".join(kept).strip() - if item["kind"] == "decl" and item["code"].strip() and not code: - continue - doc = item["doc"] - heading = re.match(r"^##\s*([^\n]+)\n?(.*)", doc, re.DOTALL) if item["kind"] == "section" else None - if heading: - lines.extend([r"\subsection*{" + render.escape_tex_prose(heading.group(1).strip()) + "}", - render.escape_tex_prose(heading.group(2).strip())]) - else: - lines.append(render.escape_tex_prose(doc)) - if code: - code_lines = [highlighted_line(line) or "~" for line in code.splitlines()] - lines.extend([r"\begin{leanbox}\small\ttfamily\raggedright\noindent", - " \\\\\n".join(code_lines), r"\par\end{leanbox}"]) + main, _ = render.split_sections(sections) + _, displayed = render_sections(main, selected) if displayed != selected: - raise ValueError(f"Selected statements were not rendered: {sorted(selected - displayed)}") + raise ValueError("Selected statements were not rendered in the main presentation: " + f"{sorted(selected - displayed)}") + lines.append(render_sections(render.presentation_sections(sections), selected)[0]) + modules = entry_foundations(entry, root) + if modules: + lines.insert(-1, r"{\small Shared foundation definitions appear in the appendix: " + + ", ".join(link(source_url(repository, sha, + module_source_path(module, root).relative_to(root)), + render.escape_tex_prose("`" + module + "`")) + for module in modules) + ".}") + if include_foundations: + lines.append(render_foundations(modules, repository, sha, root)) return "\n\n".join(lines) + "\n" @@ -336,9 +401,13 @@ def build(manifest, output, *, root=ROOT, require_clean=False): if not shutil.which("latexmk"): raise ValueError("latexmk is required (see abstracts/README.md for TeX dependencies)") inputs = {Path(manifest), root / "scripts/build_abstracts.py", root / "scripts/abstract_to_tex.py"} + all_foundations = [] for entry in entries: source = module_source_path(entry["module"], root) inputs.add(source) + modules = entry_foundations(entry, root) + all_foundations.extend(modules) + inputs.update(module_source_path(module, root) for module in modules) bridge = source.with_name(source.name.replace("Abstract.lean", "Bridge.lean")) if bridge.is_file(): inputs.add(bridge) @@ -353,17 +422,20 @@ def build(manifest, output, *, root=ROOT, require_clean=False): stale.unlink() bodies, documents = [], [] for entry in entries: - body = render_entry(entry, repository, sha, dirty, root) + body = render_entry(entry, repository, sha, dirty, root, include_foundations=False) bodies.append(body) tex = output / (entry["id"] + ".tex") - tex.write_text(document(body)) + modules = entry_foundations(entry, root) + tex.write_text(document(body + render_foundations(modules, repository, sha, root))) pdf = build_pdf(tex) source = module_source_path(entry["module"], root) text = source.read_text() documents.append({ "id": entry["id"], "title": entry["title"], "pdf": pdf.name, "pdf_sha256": digest(pdf), "source": str(source.relative_to(root)), - "source_sha256": digest(source), "headlines": [ + "source_sha256": digest(source), + "foundations": [foundation_record(module, repository, sha, root) for module in modules], + "headlines": [ {"declaration": name, "line": declaration_line(text, name), "url": source_url(repository, sha, source.relative_to(root), declaration_line(text, name))} @@ -386,7 +458,9 @@ def build(manifest, output, *, root=ROOT, require_clean=False): render.escape_tex_prose(entry["summary"])) index.extend([r"\end{itemize}", r"\clearpage"]) catalogue = output / "catalogue.tex" - catalogue.write_text(document("\n\n".join(index) + "\n\\clearpage\n".join(bodies))) + foundations = render_foundations(all_foundations, repository, sha, root) + catalogue.write_text(document("\n\n".join(index) + "\n\\clearpage\n".join(bodies) + + ("\n\\clearpage\n" + foundations if foundations else ""))) catalogue_pdf = build_pdf(catalogue) event_path = os.environ.get("GITHUB_EVENT_PATH") event = json.loads(Path(event_path).read_text()) if event_path else {} @@ -403,7 +477,8 @@ def build(manifest, output, *, root=ROOT, require_clean=False): "run_url": (f"https://github.com/{repository}/actions/runs/{os.environ['GITHUB_RUN_ID']}" if os.environ.get("GITHUB_RUN_ID") else None), "run_attempt": os.environ.get("GITHUB_RUN_ATTEMPT"), - "catalogue": {"pdf": "catalogue.pdf", "pdf_sha256": digest(catalogue_pdf)}, + "catalogue": {"pdf": "catalogue.pdf", "pdf_sha256": digest(catalogue_pdf), + "foundations": list(dict.fromkeys(all_foundations))}, "documents": documents, "inputs": input_records, "style_sources": [STYLE_SOURCE, EXTRACTION_SOURCE], diff --git a/scripts/test_abstract_to_tex.py b/scripts/test_abstract_to_tex.py index bd1d0a982..02cadfc9a 100644 --- a/scripts/test_abstract_to_tex.py +++ b/scripts/test_abstract_to_tex.py @@ -16,6 +16,53 @@ class AbstractToTexTests(unittest.TestCase): + def test_representation_sections_move_after_results_without_losing_code(self): + sample = """/-! # Title +An abstract. +-/ +namespace Example +universe u +/-! ## Representation details +The exact delimiter convention. +-/ +/-- A delimiter. -/ +def delimiter : Bool := false +/-! A continuation of the representation explanation. -/ +def serial : List Bool := [delimiter] +/-! ## Main result -/ +/-- The result. -/ +theorem headline : serial = [false] := rfl +/-! ## Representation details -/ +/-- A second representation detail. -/ +def extra : Nat := 2 +end Example +""" + title, intro, sections = abstract_to_tex.parse_abstract(sample) + for renderer in (abstract_to_tex.render_markdown, abstract_to_tex.render_tex): + with self.subTest(renderer=renderer.__name__): + output = renderer(title, intro, sections) + self.assertIn("universe u", output) + self.assertLess(output.index("headline"), output.index("Appendix:")) + self.assertLess(output.index("Appendix:"), output.index("def delimiter")) + self.assertLess(output.index("def serial"), output.index("def extra")) + self.assertEqual(output.count("def delimiter"), 1) + self.assertIn("continuation of the representation", output) + self.assertNotIn("rfl", output) + + def test_undocumented_declarations_are_not_silently_omitted(self): + sample = "/-! # Title\nIntro.\n-/\nnamespace Example\ndef first := 1\nend Example\n" + output = abstract_to_tex.render_markdown(*abstract_to_tex.parse_abstract(sample)) + self.assertIn("def first := 1", output) + + def test_lean_scanner_preserves_primed_identifiers_beside_character_literals(self): + text = "def result := f' 'a'\ndef quote := '\"'\nnamespace Real\n" + masked = abstract_to_tex.lean_code(text) + self.assertIn("f'", masked) + self.assertNotIn("'a'", masked) + self.assertNotIn("\"", masked) + self.assertIn("namespace Real", masked) + self.assertEqual(len(masked), len(text)) + def test_all_abstracts_render_markdown_and_tex(self): expected_theorems = { "CookLevinAbstract.lean": [ @@ -76,6 +123,30 @@ def test_strip_theorem_proof_preserves_named_arguments(self): r"Check \texttt{x ** y} and \textbf{bold} text.", ) + def test_attributed_theorems_strip_proofs_and_injectivity_helpers(self): + attribute = '@[deprecated (since := "2026-10-23")]\n' + sample = "def encX := f\n\n" + attribute + ( + "theorem encX_injective : Function.Injective encX := Bridge.proof\n\n") + attribute + ( + "lemma visible : P := Bridge.other_proof") + output = abstract_to_tex.clean_code_for_display(sample) + self.assertNotIn("encX_injective", output) + self.assertNotIn("Bridge.", output) + self.assertIn("lemma visible : P", output) + self.assertEqual(abstract_to_tex.theorem_name(attribute + "theorem selected : P := proof"), + "selected") + + def test_wrapped_prose_is_one_paragraph_and_citation_keys_allow_whitespace(self): + output = abstract_to_tex.render_tex_intro( + "A machine has read-only input and write-only\noutput, with a polynomial bound.\n\n" + "A separate paragraph.\n## References\n" + "* [A. Author, *A paper*]\n [Reference2026]\n") + self.assertEqual(output[0], + "A machine has read-only input and write-only output, with a polynomial bound.") + self.assertEqual(output[1], "A separate paragraph.") + self.assertIn(r"\item{} A. Author, \emph{A paper} {\footnotesize (Reference2026)}", output) + self.assertEqual(abstract_to_tex.escape_tex_prose("[A title]\n[Reference2026]"), + r"A title {\footnotesize (Reference2026)}") + def test_only_injectivity_helpers_are_elided(self): sample = ( "def encX : X → List Bool := f\n\n" diff --git a/scripts/test_build_abstracts.py b/scripts/test_build_abstracts.py index 1fa0a2d32..51c1d1fa7 100644 --- a/scripts/test_build_abstracts.py +++ b/scripts/test_build_abstracts.py @@ -53,6 +53,149 @@ def setUp(self): def write_manifest(self, entries): self.manifest.write_text(json.dumps({"title": "Selected abstracts", "entries": entries})) + def add_foundations(self): + modules = ["ComplexityAbstracts.Encoding", "ComplexityAbstracts.Computation"] + for module, imports, name in ( + (modules[0], "import Complexity.ProofOnly\n", "binaryCode"), + (modules[1], "import ComplexityAbstracts.Encoding\n", "polynomialTime"), + ): + build.module_source_path(module, self.root).write_text( + imports + f"/-! # {module.rsplit('.', 1)[-1]} foundation\n" + "Exact checked definitions.\n-/\n" + f"namespace ComplexityTests.Abstracts.{module.rsplit('.', 1)[-1]}\n" + f"/-- The foundational definition {name}. -/\ndef {name} : Nat := 0\n" + f"end ComplexityTests.Abstracts.{module.rsplit('.', 1)[-1]}\n") + source = build.module_source_path(self.entry["module"], self.root) + source.write_text("import ComplexityAbstracts.Check\n" + "import ComplexityAbstracts.ExampleBridge\n" + "import ComplexityAbstracts.Computation\n" + SOURCE) + self.entry["foundations"] = modules + self.write_manifest([self.entry]) + return modules + + @staticmethod + def fake_pdf(tex): + pdf = tex.with_suffix(".pdf") + pdf.write_bytes(b"%PDF-fixture") + return pdf + + def test_foundations_require_an_exact_manifest_and_import_closure(self): + modules = self.add_foundations() + self.assertEqual(build.entry_foundations(self.entry, self.root), modules) + self.assertEqual(build.load_catalogue(self.manifest, self.root), [self.entry]) + for listed, message in ((None, "list of module"), (modules * 2, "Duplicate foundation"), + ([modules[1]], "missing"), ([], "missing"), + (["Other.Encoding"], "formal-abstract module"), + (["ComplexityAbstracts.Missing"], "Missing shared foundation"), + (["ComplexityAbstracts.ExampleAbstract"], "Not a shared")): + self.entry["foundations"] = listed + self.write_manifest([self.entry]) + with self.subTest(listed=listed), self.assertRaisesRegex(ValueError, message): + build.load_catalogue(self.manifest, self.root) + self.entry["foundations"] = modules + build.module_source_path(self.entry["module"], self.root).write_text(SOURCE) + self.write_manifest([self.entry]) + with self.assertRaisesRegex(ValueError, "unused"): + build.load_catalogue(self.manifest, self.root) + + def test_comment_import_spoofs_do_not_create_foundation_dependencies(self): + source = build.module_source_path(self.entry["module"], self.root) + source.write_text('/- import ComplexityAbstracts.Missing -/\n' + SOURCE + + '\ndef banner := "import ComplexityAbstracts.Missing"\n') + self.assertEqual(build.entry_foundations(self.entry, self.root), []) + + def test_cyclic_foundations_fail_closed(self): + modules = self.add_foundations() + source = build.module_source_path(modules[0], self.root) + source.write_text("import ComplexityAbstracts.Computation\n" + source.read_text()) + with self.assertRaisesRegex(ValueError, "Cyclic shared foundations"): + build.load_catalogue(self.manifest, self.root) + + def test_foundations_are_displayed_with_source_and_declaration_links(self): + modules = self.add_foundations() + output = build.render_entry(self.entry, "owner/repo", "a" * 40, False, self.root) + self.assertLess(output.index(r"\textbf{theorem}"), output.index("Appendix: shared")) + self.assertIn("binary", output) + self.assertIn("polynomial", output) + for module in modules: + record = build.foundation_record(module, "owner/repo", "a" * 40, self.root) + self.assertIn(record["url"], output) + self.assertIn(record["declarations"][0]["url"], output) + self.assertEqual(record["source_sha256"], + build.digest(build.module_source_path(module, self.root))) + self.assertIn("ComplexityTests.Abstracts.Encoding", + build.foundation_record(modules[0], "owner/repo", "a" * 40, + self.root)["namespaces"]) + + def test_combined_catalogue_includes_shared_foundations_once(self): + modules = self.add_foundations() + other = {**self.entry, "id": "second", "module": "ComplexityAbstracts.SecondAbstract", + "namespace": "ComplexityTests.Abstracts.SecondAbstract", + "headline_theorems": ["ComplexityTests.Abstracts.SecondAbstract.chosen"]} + source = build.module_source_path(self.entry["module"], self.root).read_text() + build.module_source_path(other["module"], self.root).write_text( + source.replace("ExampleAbstract", "SecondAbstract")) + self.write_manifest([self.entry, other]) + with patch.object(build, "git", side_effect=["a" * 40, ""]), \ + patch.object(build.shutil, "which", return_value="latexmk"), \ + patch.object(build, "build_pdf", side_effect=self.fake_pdf): + result = build.build(self.manifest, self.root / "build", root=self.root) + for name in ("example", "second", "catalogue"): + output = (self.root / f"build/{name}.tex").read_text() + self.assertEqual(output.count(r"\section*{Appendix: shared foundations}"), 1) + self.assertEqual(output.count(r"\subsection*{Encoding foundation}"), 1) + self.assertEqual(output.count(r"\subsection*{Computation foundation}"), 1) + combined = (self.root / "build/catalogue.tex").read_text() + self.assertGreater(combined.index("Appendix: shared"), combined.index(r"\hypertarget{second}")) + self.assertEqual(result["catalogue"]["foundations"], modules) + for module in modules: + path = build.module_source_path(module, self.root) + self.assertIn({"path": str(path.relative_to(self.root)), "sha256": build.digest(path)}, + result["inputs"]) + self.assertEqual([record["module"] for record in result["documents"][0]["foundations"]], + modules) + + def test_foundation_change_during_generation_invalidates_provenance(self): + modules = self.add_foundations() + + def changing_pdf(tex): + path = build.module_source_path(modules[0], self.root) + path.write_text(path.read_text() + "\n-- changed\n") + return self.fake_pdf(tex) + + with patch.object(build, "git", side_effect=["a" * 40, ""]), \ + patch.object(build.shutil, "which", return_value="latexmk"), \ + patch.object(build, "build_pdf", side_effect=changing_pdf): + with self.assertRaisesRegex(ValueError, "Source changed.*Encoding.lean"): + build.build(self.manifest, self.root / "build", root=self.root) + self.assertFalse((self.root / "build/provenance.json").exists()) + + def test_selected_theorems_cannot_be_moved_to_an_appendix(self): + source = build.module_source_path(self.entry["module"], self.root) + source.write_text(SOURCE.replace("/-- The selected result. -/", + "/-! ## Representation details -/\n/-- The selected result. -/")) + with self.assertRaisesRegex(ValueError, "main presentation"): + build.load_catalogue(self.manifest, self.root) + + def test_other_section_headings_do_not_hide_selected_theorems(self): + source = build.module_source_path(self.entry["module"], self.root) + source.write_text(SOURCE.replace("/-- The selected result. -/", + "/-! ## Other results -/\n/-- The selected result. -/")) + self.assertEqual(build.load_catalogue(self.manifest, self.root), [self.entry]) + self.assertIn("theorem chosen", build.render.render_source(source, "markdown")) + + def test_standalone_previews_include_foundation_definitions_and_digests(self): + modules = self.add_foundations() + source = build.module_source_path(self.entry["module"], self.root) + for format in ("markdown", "tex"): + output = build.render.render_source(source, format) + for module in modules: + path = build.module_source_path(module, self.root) + self.assertIn(build.digest(path), output) + self.assertIn("binary", output) + self.assertIn("polynomial", output) + self.assertLess(output.index("chosen"), output.index("Shared foundation:")) + def test_module_source_path_uses_dedicated_library_root(self): self.assertEqual(build.module_source_path(self.entry["module"], self.root), self.root / "abstracts/ComplexityAbstracts/ExampleAbstract.lean") @@ -155,6 +298,46 @@ def test_display_keeps_definitions_and_selected_statements_without_proofs(self): self.assertIn("a" * 40 + "/abstracts/ComplexityAbstracts/ExampleAbstract.lean", rendered) self.assertIn(r"\textcolor{leanblue}", rendered) + def test_attributed_unselected_theorems_do_not_leak_docs_or_proofs(self): + sections = [{"kind": "decl", "doc": "Unselected compatibility helper.", + "code": '@[deprecated (since := "2026-10-23")]\n' + "theorem helper : True := Bridge.helper"}, + {"kind": "decl", "doc": "Selected result.", + "code": "@[simp]\ntheorem chosen : True := Bridge.chosen"}] + output, displayed = build.render_sections(sections, {"chosen"}) + self.assertEqual(displayed, {"chosen"}) + self.assertNotIn("helper", output) + self.assertNotIn("Bridge", output) + self.assertIn("chosen", output) + + @unittest.skipUnless(shutil.which("latexmk") and shutil.which("pdftotext") + and shutil.which("kpsewhich"), "TeX/Poppler not installed") + def test_short_declaration_stays_together_and_long_definition_still_breaks(self): + for package in ("libertine.sty", "newtxmath.sty", "zi4.sty", "tcolorbox.sty"): + if subprocess.run(["kpsewhich", package], capture_output=True).returncode: + self.skipTest(f"TeX package missing: {package}") + short = {"kind": "decl", "doc": "ExplanationMarker belongs to this declaration.", + "code": "def ShortMarker : Nat :=\n 123456"} + long = {"kind": "decl", "doc": "A longer definition must remain breakable.", + "code": "def longDefinition : List Nat := [\n" + + ",\n".join(f" {n}" for n in range(1001, 1081)) + "]"} + body = r"\vbox to 0.94\textheight{\hbox{BeforeMarker}\vfil}\par" + "\n" + \ + build.render_sections([short, long])[0] + tex = self.root / "pagination.tex" + tex.write_text(build.document(body)) + pdf = build.build_pdf(tex) + pages = subprocess.check_output(["pdftotext", "-layout", str(pdf), "-"], text=True).split("\f") + + def page_of(marker): + return next(i for i, page in enumerate(pages) if marker in page) + + self.assertGreater(page_of("ExplanationMarker"), page_of("BeforeMarker")) + self.assertEqual(page_of("ExplanationMarker"), page_of("ShortMarker")) + self.assertEqual(page_of("ShortMarker"), page_of("123456")) + self.assertLess(page_of("1001"), page_of("1080")) + for number in range(1001, 1081): + self.assertIn(str(number), "\n".join(pages)) + def test_source_links_pin_the_declaration_line(self): line = build.declaration_line(SOURCE, self.entry["headline_theorems"][0]) self.assertEqual(SOURCE.splitlines()[line - 1], "theorem chosen : value = 0 := rfl") @@ -247,6 +430,7 @@ def test_styled_pdfs_build_with_source_pinned_hyperlinks(self): for package in ("libertine.sty", "newtxmath.sty", "zi4.sty", "tcolorbox.sty"): if subprocess.run(["kpsewhich", package], capture_output=True).returncode: self.skipTest(f"TeX package missing: {package}") + self.add_foundations() with patch.object(build, "git", side_effect=["a" * 40, ""]): result = build.build(self.manifest, self.root / "build", root=self.root, require_clean=True) @@ -255,8 +439,10 @@ def test_styled_pdfs_build_with_source_pinned_hyperlinks(self): if shutil.which("pdfinfo"): links = subprocess.check_output( ["pdfinfo", "-url", str(self.root / "build/example.pdf")], text=True) - self.assertIn("/blob/" + "a" * 40 + - "/abstracts/ComplexityAbstracts/ExampleAbstract.lean#L10", links) + self.assertIn(result["documents"][0]["headlines"][0]["url"], links) + for foundation in result["documents"][0]["foundations"]: + self.assertIn(foundation["url"], links) + self.assertIn(foundation["declarations"][0]["url"], links) if __name__ == "__main__":