feat(polytime): non-vacuous PPT/IsPolyTime over the DynComputation carrier, sorry-free

[dtumad]

Motivation

Re-extraction of the Turing-machine-grounded polynomial-time layer from the closed reference
draft #481, onto current main: Lean v4.32, current Mathlib/cslib, and the merged
DynComputation-based machine layer (#498/#499) in place of the retired PointedMachine
API. Includes the closure of all three non-triviality sorrys contributed in #487.

The model is unchanged from #481 (and from the design agreed in the #460 review): non-uniform
P/poly relative to pinned canonical boundary encodings, with a single polynomial bounding both
per-step running time and machine description size uniformly across the security parameter —
the description-size bound is what closes the truth-table/unbounded-advice escape. The model
and its statement-site discipline are now documented in docs/agents/polytime-model.md.

What moved under the port

ToMathlib/Computability/ + ToMathlib/Data/BitVec.lean — the TM toolkit on current
Mathlib/cslib. Encodings are raw injective List Bool families (BitEncFam / StrEncFam)
from the start — no intermediate alphabet layer. cslib's restructure
(SingleTapeTuring.Basic → Turing/SingleTape/Deterministic, namespace
Cslib.Turing.SingleTapeTM) is a pure rename — zero proof changes. Per the repo decision
(recorded in the new design doc), nothing here is aimed at upstream Mathlib/cslib PRs; it
stays in ToMathlib/.

MachineCounting.lean and the non-triviality closure (from #487). The counting cruxes
(exists_tmTable_of_card_le, the realizable-covering surjection) and the B-factor argument
port with only signature-level adjustments (ReflTransGen.lift is now a ≤-statement; the
trajectory argument reads through the new run lemma below). Credit: Elias Judin, with the
proofs generated by Aristotle (Harmonic); co-author trailers on the porting commits and
co-authorship in the two files' headers.

Coinductive/PolyTime.lean — MachineAdversary / PolyTimeWitness /
OracleComp.IsPolyTime over the DynComputation carrier. The TM-facing step maps (expose,
updateFlat, output, stepD) are total functions derived from the machine's one-step
view, spelled with Sum combinators so they transport definitionally between machines
sharing the same dynamics. Three fields of the old bundle are gone as theorems, not
hypotheses: readout stability (returns are absorbing by construction), steadiness
(PolyTimeWitness.resolvesIn, handler-free via ResolvesIn), and the syntactic query bound
(PolyTimeWitness.queryBound, from the bounded half of ImplementsWithin via
implementsWithin_iff_implements_and_bound — IsTotalQueryBound is definitionally
IsTotalRollBound).

Coinductive/PolyTimeClosure.lean — closure under input precomposition and output maps.
Much thinner: replacing init is a real OracleMachine.setInit whose runs are unchanged
(unroll_setInit), output post-composition is upstream mapResult (unroll_mapResult), and
the precomposition implements-proofs reduce to input reindexing.

Coinductive/CoinFold.lean — the reusable bounded-coin-fold combinator. The machine is
built by a new generic OracleMachine.ofStep (one-step transition + initialization) and
implements the fold program by one direct unroll induction.

Asymptotics/PolyTime.lean — SecurityGame.secureAgainstPolyTime and the
per-query-loss former, consuming the derived PolyTimeWitness.queryBound.

Semantic-audit pass (post-extraction)

A full audit of the layer (definitions vs. the #460 review record, cslib upstream direction,
axiom footprint) produced the following fixes, all in this PR:

• detTotalTime charges the final readout — the run's answer is
  output (stepD^[steps] s), so the readout at the budget state is a real evaluation; the
  accounting and both bounding theorems gained the matching term. This closes the last open
  feat(OracleComp): oracle strategies as dynamical systems, oracle machines, and TM-grounded poly-time adversaries #460 accounting bullet (the off-by-one).
• PolyTimeWitness.queryBound is a derived theorem, not a field (see above); every
  witness construction site shed the redundant obligation.
• PolyTimeComputable.size is pinned to the Bool alphabet — a bare state count only
  measures description size over a fixed alphabet; the restriction is now in the type rather
  than in prose.
• The unused PackedEncoding/boolify layer is dropped (Encoding.lean, 337 lines of
  dead code that two docstrings mispresented as the model's encoding source).
• exists_tmTable_of_card_le generalized to any SingleTapeTM Bool; stale docstrings
  refreshed throughout (retired names, sorry-era prose, dangling module references);
  IsPolyTime now states its non-uniformity (P/poly) explicitly.

Status of the #460 checklist

• advice/description-size bound: done (descBound; non-triviality certified below);
• termination and state-size bounds over all answer paths: done (ResolvesIn
  quantifies over every typed answer path; StrEncFam.len_le over all states);
• input/message-size assumptions: done (BitEncFam.widBound is intrinsic —
  detTotalTime_le and exists_polynomial_detTotalTime_le are hypothesis-free);
• final-readout accounting: done (this PR's audit pass).

Still deliberately out of scope (documented in docs/agents/polytime-model.md): the
end-to-end compiled single-machine theorem (#460 item 7's "second tier"), bind closure,
and a uniform variant. secureAgainstPolyTime accordingly remains unused by any concrete
security statement this cycle.

Validation

• lake build green; scripts/check-extern-isolation.sh, scripts/check-interop-isolation.sh,
  scripts/check-agent-docs.py
• no literal sorry anywhere in the added files; headline theorems
  (exists_not_isPolyTime_pure, exists_not_implements_pure_of_steps_eq_zero,
  secureAgainstPolyTime_of_advantage_le_mul_totalQueries, PolyTimeWitness.queryBound,
  exists_polynomial_detTotalTime_le) all check at exactly
  [propext, Classical.choice, Quot.sound]
• the ToMathlib layer builds independently of the machine layer

On merge

• Close prove(polytime): close nontriviality certificate #487 (its content is fully ported here, with attribution carried).

🤖 Generated with Claude Code

[github-actions]

🤖 PR Summary

ℹ️ This PR modifies 5 file(s) under ToMathlib/ — consider whether a corresponding upstream PR is needed.

overview of the pr

---

Statistics

Metric	Count
📝 Files Changed	15
✅ Lines Added	3970
❌ Lines Removed	0

---

Lean Declarations

✏️ Added: 243 declaration(s)

ToMathlib/Computability/BitEncoding.lean (28)

• @[simp] theorem length_natToBits (w m : ℕ) : (natToBits w m).length = w
• @[simp] theorem pad_enc (w : ℕ → ℕ) (p : Polynomial ℕ) (hw : ∀ n, w n ≤ p.eval n)
• @[simp] theorem pairFix_enc (e : BitEncFam γ) (s : StrEncFam σ) (n : ℕ) (p : γ n × σ n) :
• @[simp] theorem pairVar_enc (s : StrEncFam σ) (e : BitEncFam β) (n : ℕ) (p : σ n × β n) :
• @[simp] theorem sum_enc_inl {τ : ℕ → Type u} (s₁ : StrEncFam σ) (s₂ : StrEncFam τ)
• @[simp] theorem sum_enc_inr {τ : ℕ → Type u} (s₁ : StrEncFam σ) (s₂ : StrEncFam τ)
• @[simp] theorem toStrEncFam_bound (e : BitEncFam α) : e.toStrEncFam.bound = e.widBound
• @[simp] theorem toStrEncFam_enc (e : BitEncFam α) : e.toStrEncFam.enc = e.enc
• def copy {f : (n : ℕ) → α n → β n} (h : EncPolyTimeFam ea eb f)
• def natToBits (w m : ℕ) : List Bool
• def recode {α' β' : ℕ → Type u} {ea' : (n : ℕ) → α' n → List Bool}
• def toStrEncFam (e : BitEncFam α) : StrEncFam α where
• noncomputable abbrev bool : BitEncFam (fun _ => Bool)
• noncomputable abbrev unit : BitEncFam (fun _ => PUnit.{u + 1})
• noncomputable def bitVec (w : ℕ → ℕ) (p : Polynomial ℕ) (hw : ∀ n, w n ≤ p.eval n) :
• noncomputable def bitVecX : BitEncFam (fun n => BitVec n)
• noncomputable def comp {f : (n : ℕ) → α n → β n} {g : (n : ℕ) → β n → γ n}
• noncomputable def const (ea : (n : ℕ) → α n → List Bool) {eb : (n : ℕ) → β n → List Bool}
• noncomputable def fin (k : ℕ → ℕ) (p : Polynomial ℕ) (hk : ∀ n, k n ≤ p.eval n) :
• noncomputable def id (ea : (n : ℕ) → α n → List Bool) :
• noncomputable def ofFintype [∀ n, Fintype (α n)] {ea : (n : ℕ) → α n → List Bool}
• noncomputable def option (e : BitEncFam α) : BitEncFam (fun n => Option (α n)) where
• noncomputable def pad (w : ℕ → ℕ) (p : Polynomial ℕ) (hw : ∀ n, w n ≤ p.eval n) :
• noncomputable def pair (e₁ : BitEncFam α) (e₂ : BitEncFam β) : BitEncFam (fun n => α n × β n) where
• noncomputable def pairFix (e : BitEncFam γ) (s : StrEncFam σ) :
• noncomputable def pairVar (s : StrEncFam σ) (e : BitEncFam β) : StrEncFam (fun n => σ n × β n) where
• noncomputable def sum {τ : ℕ → Type u} (s₁ : StrEncFam σ) (s₂ : StrEncFam τ) :
• theorem natToBits_inj {w m₁ m₂ : ℕ} (h₁ : m₁ < 2 ^ w) (h₂ : m₂ < 2 ^ w)

ToMathlib/Computability/CslibPolyTime.lean (19)

• @[simp] theorem PolyTimeComputable.size_normalize {f : List Bool → List Bool}
• @[simp] theorem size_copy {f : α → β} (h : EncPolyTime ea eb f) (f' : α → β)
• @[simp] theorem size_id (ea : α → List Bool) : (EncPolyTime.id ea).size = 1
• @[simp] theorem size_recode {α' : Type u'} {β' : Type v'} {ea' : α' → List Bool}
• @[simp] theorem time_recode {α' : Type u'} {β' : Type v'} {ea' : α' → List Bool}
• def PolyTimeComputable.normalize {f : List Symbol → List Symbol}
• def PolyTimeComputable.size {f : List Bool → List Bool}
• def copy {f : α → β} (h : EncPolyTime ea eb f) (f' : α → β) (hf : ∀ a, f a = f' a) :
• def recode {α' : Type u'} {β' : Type v'} {ea' : α' → List Bool} {eb' : β' → List Bool}
• def size {f : α → β} (h : EncPolyTime ea eb f) : ℕ
• def time {f : α → β} (h : EncPolyTime ea eb f) : Polynomial ℕ
• noncomputable def comp {f : α → β} {f' : β → γ}
• noncomputable def id (ea : α → List Bool) : EncPolyTime ea ea _root_.id where
• theorem PolyTimeComputable.monotone_normalize_timeBound {f : List Symbol → List Symbol}
• theorem Polynomial.eval_le_eval {p : Polynomial ℕ} {m n : ℕ} (h : m ≤ n) :
• theorem comp_time {f : α → β} {f' : β → γ}
• theorem comp_time_eval {f : α → β} {f' : β → γ}
• theorem length_le {f : α → β} (h : EncPolyTime ea eb f) (a : α) :
• theorem size_comp {f : α → β} {f' : β → γ}

ToMathlib/Computability/MachineCounting.lean (36)

• abbrev TMTable (d : ℕ) : Type
• def B (d : ℕ) : ℕ
• def RealizableLE (n d : ℕ) : Set (BitVec n → Bool)
• def reify {d : ℕ} (t : TMTable d) : SingleTapeTM Bool where
• def stmtProdEquiv : SingleTapeTM.Stmt Bool ≃ (Option Bool × Option Turing.Dir) where
• lemma decFin_embFin {α : Type*} [Fintype α] {d : ℕ} (hd : Fintype.card α ≤ d) (s : α) :
• lemma embFin_injective {α : Type*} [Fintype α] {d : ℕ} (hd : Fintype.card α ≤ d) :
• lemma normCfg_injective (hemb : Function.Injective emb) :
• lemma normCfg_reflTransGen (hdec : ∀ s, dec (emb s) = some s) {c c' : tm.Cfg}
• lemma reflTransGen_normCfg_reverse (hdec : ∀ s, dec (emb s) = some s) {c : tm.Cfg}
• lemma step_normCfg (hdec : ∀ s, dec (emb s) = some s) (c : tm.Cfg) :
• noncomputable def decFin {α : Type*} [Fintype α] {d : ℕ} (i : Fin d) : Option α
• noncomputable def embFin {α : Type*} [Fintype α] {d : ℕ} (hd : Fintype.card α ≤ d) (s : α) :
• noncomputable def normCfg (c : tm.Cfg) : (reify (normTable tm emb dec)).Cfg
• noncomputable def normTable : TMTable d
• noncomputable def normTr : Fin d → Option Bool → SingleTapeTM.Stmt Bool × Option (Fin d)
• noncomputable def tablePairPred (n d : ℕ) (p : TMTable d × TMTable d) : BitVec n → Bool
• theorem B_sq_le (d : ℕ) (hd : 9 * (d + 1) ≤ 2 ^ d) (hd1 : 1 ≤ d) :
• theorem Outputs_unique (tm : SingleTapeTM Symbol) {l l₁ l₂ : List Symbol}
• theorem PolyTimeComputable.outputs {f : List Symbol → List Symbol}
• theorem _root_.Cslib.Turing.BiTape.mk₁_injective {Symbol : Type} :
• theorem _root_.Relation.ReflTransGen.unique_of_deterministic
• theorem card_bitVec_fun (n : ℕ) : Fintype.card (BitVec n → Bool) = 2 ^ (2 ^ n)
• theorem card_dir : Fintype.card Turing.Dir = 2
• theorem card_stmt : Fintype.card (SingleTapeTM.Stmt Bool) = 9
• theorem card_tmTable (d : ℕ) : Fintype.card (TMTable d) = B d
• theorem card_tmTable_le (d : ℕ) : Fintype.card (TMTable d) ≤ B d
• theorem const_mul_pow_le_two_pow (C k : ℕ) : ∀ᶠ m in atTop, C * (m + 1) ^ k ≤ 2 ^ m
• theorem eventually_count_lt :
• theorem eventually_poly_le (p : Polynomial ℕ) :
• theorem exists_diagonal (S : (n : ℕ) → Finset (BitVec n → Bool))
• theorem exists_realizableLE_covering (n d : ℕ) :
• theorem exists_tmTable_of_card_le (tm : SingleTapeTM Bool)
• theorem nat_pow_le_two_pow (k : ℕ) : ∀ᶠ n in atTop, n ^ k ≤ 2 ^ n
• theorem not_transitionRelation_haltCfg (tm : SingleTapeTM Symbol) (l : List Symbol)
• theorem realizableLE_mono {n : ℕ} {d d' : ℕ} (h : d ≤ d') :

ToMathlib/Computability/PolyTimeTM.lean (34)

• abbrev TableState (S : Finset (List Symbol)) (T : List Symbol → List Symbol) : Type
• def clearComputer : SingleTapeTM Symbol where
• def constComputer (o : Symbol) (os : List Symbol) : SingleTapeTM Symbol where
• def constTimeComputable : (out : List Symbol) →
• def enterState (S : Finset (List Symbol)) (T : List Symbol → List Symbol)
• def prefixClosure (S : Finset (List Symbol)) : Finset (List Symbol)
• def readState (S : Finset (List Symbol)) (T : List Symbol → List Symbol)
• def tableComputer (S : Finset (List Symbol)) (T : List Symbol → List Symbol) :
• def tableTimeComputable (S : Finset (List Symbol)) (T : List Symbol → List Symbol) :
• noncomputable def const {α : Type u} {β : Type v} (ea : α → List Bool)
• noncomputable def constPolyTimeComputable (out : List Symbol) :
• noncomputable def ofFintype {α : Type u} {β : Type v} [Fintype α]
• noncomputable def tablePolyTimeComputable (S : Finset (List Symbol))
• private lemma bitape_head_tail_eq_mk₁ (t : List Symbol) :
• private lemma bitape_mk₁_eq_of_length_pos {t : List Symbol} (h : 0 < t.length) :
• private lemma clearComputer_clear_steps (l : List Symbol) :
• private lemma constComputer_clear_steps (o : Symbol) (os l : List Symbol) :
• private lemma constComputer_enter_step (o : Symbol) (os : List Symbol) :
• private lemma constComputer_write_steps (o : Symbol) (os : List Symbol) (i : ℕ) :
• private lemma tableComputer_blank_step (S : Finset (List Symbol))
• private lemma tableComputer_finish_within (S : Finset (List Symbol))
• private lemma tableComputer_read_step (S : Finset (List Symbol))
• private lemma tableComputer_read_steps (S : Finset (List Symbol))
• private lemma tableComputer_write_steps (S : Finset (List Symbol))
• theorem append_not_mem_prefixClosure {S : Finset (List Symbol)} {l : List Symbol}
• theorem card_prefixClosure_le (S : Finset (List Symbol)) :
• theorem card_tableState (S : Finset (List Symbol)) (T : List Symbol → List Symbol) :
• theorem mem_prefixClosure {S : Finset (List Symbol)} {l : List Symbol} :
• theorem size_constPolyTimeComputable_le (out : List Bool) :
• theorem size_const_le {α : Type u} {β : Type v} (ea : α → List Bool)
• theorem size_ofFintype_le {α : Type u} {β : Type v} [Fintype α]
• theorem size_ofFintype_le_of_bounds {α : Type u} {β : Type v} [Fintype α]
• theorem subset_prefixClosure (S : Finset (List Symbol)) : S ⊆ prefixClosure S
• theorem time_ofFintype_eval_le {α : Type u} {β : Type v} [Fintype α]

ToMathlib/Data/BitVec.lean (7)

• @[simp] theorem getLsbD_overwriteBit_of_ne {i j : ℕ} (h : j ≠ i) (b : Bool) (m : BitVec n) :
• @[simp] theorem getLsbD_overwriteBit_self {i : ℕ} (hi : i < n) (b : Bool) (m : BitVec n) :
• @[simp] theorem overwriteBit_getLsbD_self (i : ℕ) (m : BitVec n) :
• @[simp] theorem overwriteBit_overwriteBit (i : ℕ) (b c : Bool) (m : BitVec n) :
• def overwriteBit (i : ℕ) (b : Bool) (m : BitVec n) : BitVec n
• theorem getLsbD_overwriteBit (i j : ℕ) (b : Bool) (m : BitVec n) :
• theorem involutive_overwriteBit_pair {i : ℕ} (hi : i < n) :

VCVio/CryptoFoundations/Asymptotics/PolyTime.lean (3)

• abbrev secureAgainstMachines {spec : (n : ℕ) → OracleSpec.{0, 0} (ι n)} {α β : ℕ → Type}
• abbrev secureAgainstPolyTime {spec : (n : ℕ) → OracleSpec.{0, 0} (ι n)} {α β : ℕ → Type}
• theorem secureAgainstPolyTime_of_advantage_le_mul_totalQueries

VCVio/OracleComp/Coinductive/CoinFold.lean (16)

• @[reducible] def OracleMachine.ofStep {ι : Type} {spec : OracleSpec.{0, 0} ι} {α β S : Type}
• @[reducible] def coinFoldMachine (rounds : ℕ) (init₀ : σ) : OracleMachine coinSpec Unit β
• @[simp] theorem OracleMachine.view_ofStep {ι : Type} {spec : OracleSpec.{0, 0} ι}
• def coinFoldProg (step : σ → ℕ → Bool → σ) (readout : σ → β) :
• noncomputable def coinFoldAdversary :
• noncomputable def coinFoldAdversaryOfWitnesses :
• noncomputable def coinFoldWitness :
• noncomputable def coinFoldWitnessOfWitnesses :
• theorem coinFoldMachine_implementsWithin (rounds : ℕ) (init₀ : σ) :
• theorem coinFoldMachine_unroll (rounds : ℕ) (init₀ : σ) :
• theorem coinFoldMachine_view_succ (rounds : ℕ) (init₀ : σ)
• theorem coinFoldMachine_view_zero (rounds : ℕ) (init₀ : σ)
• theorem coinFoldProg_succ (step : σ → ℕ → Bool → σ) (readout : σ → β) (r : ℕ) (acc : σ) :
• theorem isPolyTime_coinFold :
• theorem isPolyTime_coinFold_of_witnesses :
• theorem isTotalQueryBound_coinFoldProg (step : σ → ℕ → Bool → σ) (readout : σ → β)

VCVio/OracleComp/Coinductive/PolyTime.lean (40)

• @[simp] theorem OracleComp.OracleMachine.view_ofPureFn {spec : OracleSpec.{0, 0} ι} {α β : Type}
• @[simp] theorem expose_of_view_query [Inhabited ι] (M : OracleMachine spec α β)
• @[simp] theorem output_of_view_return (M : OracleMachine spec α β) {s : M.State} {b : β}
• @[simp] theorem withIface_eIface (bd : BoundaryData spec α β)
• @[simp] theorem withIface_eIn (bd : BoundaryData spec α β)
• @[simp] theorem withIface_eOut (bd : BoundaryData spec α β)
• @[simp] theorem withIn_eIface (bd : BoundaryData spec α β) (e : BitEncFam γ) :

…and 93 more not listed.

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

No findings.

---

📄 **Per-File Summaries**

• AGENTS.md: Added six new file references documenting the TM-grounded polynomial-time adversary model, covering MachineAdversary and OracleComp.IsPolyTime, the bounded coin-fold poly-time combinator, poly-time non-triviality certificate, encoded poly-time witnesses and bit-encoding families, and security against poly-time adversaries. Also added a new entry to the reading guide for the corresponding agent documentation docs/agents/polytime-model.md, helping reviewers navigate the recently introduced poly-time formalization.
• ToMathlib.lean: The file ToMathlib.lean was updated to add imports for newly developed modules. Specifically, it now imports ToMathlib.Computability.BitEncoding, ToMathlib.Computability.CslibPolyTime, ToMathlib.Computability.MachineCounting, ToMathlib.Computability.PolyTimeTM, and ToMathlib.Data.BitVec. These new imports integrate the corresponding definitions and theorems into the project's import graph without modifying any existing declarations.
• ToMathlib/Computability/BitEncoding.lean: This new file introduces the StrEncFam, BitEncFam, and EncPolyTimeFam structures and their combinators, providing canonical fixed-width and variable-width bit encodings with polynomial bounds, and uniform polynomial-time machine families. It defines natToBits for natural numbers, and various BitEncFam constructors (const, fin, bitVec, bitVecX, pair, option, pad) and StrEncFam combinators (pairVar, sum, pairFix), as well as EncPolyTimeFam combinators (recode, id, copy, comp, const, ofFintype). The file establishes the foundational representation for polynomial-time adversarial models in formal cryptography.
• ToMathlib/Computability/CslibPolyTime.lean: This new file introduces Computability.EncPolyTime, a structure bundling a machine-computed total List Bool → List Bool function, a PolyTimeComputable witness and a proof that it intertwines user-supplied encodings ea : α → List Bool and eb : β → List Bool to certify polynomial-time computability of an abstract function f : α → β. It provides EncPolyTime.id (over any encoding), EncPolyTime.copy (to a pointwise-equal function), EncPolyTime.recode (to re-encode domain/codomain with the same machine) and EncPolyTime.comp (composition with degree-multiplying time bound). The file also adds PolyTimeComputable.normalize (replaces a machine's time bound by the evaluation of its own polynomial, with monotonicity proof PolyTimeComputable.monotone_normalize_timeBound), PolyTimeComputable.size (state count for machines over Bool alphabet, with lemma size_normalize) and the supporting lemma Polynomial.eval_le_eval. Theorems time_recode, size_recode, size_copy, size_id, comp_time, comp_time_eval, size_comp and length_le (output length bound) are provided.
• ToMathlib/Computability/MachineCounting.lean: This file adds the combinatorial core for the non‑triviality certificate: it defines TMTable d (canonical d‑state machines) and B d (upper bound on their count), proves card_tmTable and card_tmTable_le, and supplies Fintype/DecidableEq instances for Turing.Dir and SingleTapeTM.Stmt Bool. State normalization (exists_tmTable_of_card_le) shows any SingleTapeTM Bool with ≤ d states computes the same string function as reify of some TMTable d. Determinism lemmas (Outputs_unique) and the RealizableLE set (predicates realizable at description size ≤ d) are introduced, and exists_realizableLE_covering bounds RealizableLE n d by a Finset of cardinality ≤ B d ^ 2. Growth bounds (eventually_poly_le, B_sq_le, eventually_count_lt) show the machine count at threshold 2^(n/4) is eventually below the predicate count 2^(2^n), and exists_diagonal concludes that a family of subexponential size misses a predicate eventually.
• ToMathlib/Computability/PolyTimeTM.lean: The new file ToMathlib/Computability/PolyTimeTM.lean adds several explicit single-tape Turing machines and their polynomial-time correctness proofs. It defines clearComputer and constComputer to erase the input and write a fixed output string, proving constTimeComputable and constPolyTimeComputable for constant functions, along with a state size bound size_constPolyTimeComputable_le. It also introduces tableComputer for finite-table functions (any function with a finite domain), with tableTimeComputable and tablePolyTimeComputable, and size theorems card_prefixClosure_le and card_tableState. In the Computability.EncPolyTime namespace, the file provides the polynomial-time witnesses const and ofFintype (the latter showing that any function with a finite domain is polynomial-time computable under an injective encoding), together with the bounds time_ofFintype_eval_le, size_const_le, size_ofFintype_le, and size_ofFintype_le_of_bounds that give time and description size estimates. No sorry or admit appear in the diff.
• ToMathlib/Data/BitVec.lean: This file defines BitVec.overwriteBit i b m, which returns m with the i-th least significant bit replaced by b (out-of-range indices are a no-op). It provides the getLsbD description theorems getLsbD_overwriteBit_self, getLsbD_overwriteBit_of_ne, and getLsbD_overwriteBit, the idempotence lemma overwriteBit_overwriteBit, the identity lemma overwriteBit_getLsbD_self, and the involution involutive_overwriteBit_pair on BitVec n × Bool that swaps (m, b) with (m with bit i overwritten by b, original bit i of m)– the change of variables underlying uniform-distribution splitting arguments. The file is new and contains nosorryoradmit`.
• VCVio.lean: The diff adds imports for VCVio.CryptoFoundations.Asymptotics.PolyTime and five modules from VCVio.OracleComp.Coinductive (CoinFold, PolyTime, PolyTimeClosure, PolyTimeConstructions, PolyTimeNontrivial). These new imports bring in definitions and theorems about polynomial-time computation and coinductive oracle-machine constructions, which are foundational for the project's security and complexity analysis.
• VCVio/CryptoFoundations/Asymptotics/PolyTime.lean: This new file introduces two abbreviations and one theorem in the SecurityGame namespace. secureAgainstPolyTime instantiates the abstract secureAgainst with the OracleComp.IsPolyTime predicate relative to given boundary data. secureAgainstMachines provides an equivalent formulation for bundled machine adversaries, trivially satisfying the PPT condition. The theorem secureAgainstPolyTime_of_advantage_le_mul_totalQueries states that if a game's advantage against any adversary is bounded by the product of its total query count and a negligible ε, then the game satisfies secureAgainstPolyTime; its proof uses the adversary's witness to extract a polynomial query bound and applies negligible_polynomial_mul.
• VCVio/OracleComp/Coinductive/CoinFold.lean: This new file adds a reusable polynomial-time construction for bounded coin folds: coinFoldProg (a program that flips a coin a polynomial number of times, folding each answer into a finite-state accumulator, then reading out), coinFoldMachine (a Turing machine realizing it), and coinFoldMachine_implementsWithin (proving the machine implements the program within the round bound via fuelled unrolling). It also provides coinFoldAdversary/coinFoldWitness/isPolyTime_coinFold for the case where the accumulator type σ has polynomially bounded cardinality, using Fintype-based table witnesses, and coinFoldAdversaryOfWitnesses/isPolyTime_coinFold_of_witnesses for superpolynomially large accumulators where explicit machine families must be supplied. Additionally, the file introduces a generic OracleMachine.ofStep constructor and a view lemma for building machines from a one-step transition function.
• VCVio/OracleComp/Coinductive/PolyTime.lean: This file introduces the framework for polynomial-time adversaries in Lean: MachineAdversary bundles a family of oracle machines with polynomial round, state-length, time, and description bounds, all relative to pinned canonical boundary encodings (BoundaryData). It defines the implements relation D ⊨ oa (execution matches the program's simulation) and the polynomial-time certificate PolyTimeWitness, with the predicate OracleComp.IsPolyTime for non-uniform PPT. The module contributes step-map accessors (output, expose, updateFlat) and their key theorems, plus total-time bounding (detTotalTime_le) and an exec_eq_of_implements master transfer equation; it also provides BoundaryData, OracleSpec.InterfaceBitEnc (with the coin-oracle instance), and a result that query-free functions are polynomial-time given suitable encoded step witnesses (isPolyTime_pure_of_witnesses). No sorry or admit appears.
• VCVio/OracleComp/Coinductive/PolyTimeClosure.lean: The new file PolyTimeClosure.lean adds a module establishing closure properties of MachineAdversary (and thus OracleComp.IsPolyTime) under input precomposition and output postcomposition. It defines OracleMachine.setInit and mapResult with proofs that they preserve/unroll dynamics (unroll_setInit, runWith_setInit, unroll_mapResult, runWith_mapResult, etc.). It then constructs MachineAdversary.precomp (finite-table precomposition for polynomially bounded input types) and MachineAdversary.precompComp (machine‑witness precomposition for arbitrary input maps), each with an _implements theorem linking the adversary to the precomposed program. It also adds MachineAdversary.mapComp for output postcomposition via a supplied EncPolyTimeFam for Option.map g, with mapComp_implements. The file provides Computability.EncPolyTimeFam.optionMap as a finite‑table witness for output maps on finite output types. Finally, it lifts all three closures to the abstract predicate OracleComp.IsPolyTime via IsPolyTime.precomp, IsPolyTime.precompComp, and IsPolyTime.map. The file contains no sorry or admit.
• VCVio/OracleComp/Coinductive/PolyTimeConstructions.lean: This new file adds three polynomial-time constructions. isPolyTime_coin establishes that a single coin flip is polynomial time via a one-round bounded coin fold with finite tables. isPolyTime_uniformBitVec certifies that uniformBitVec n (which samples a uniform BitVec n by folding n coin flips) is polynomial time, but requires the caller to supply machine families for the fold's step functions because the generic table witnesses of isPolyTime_coinFold are unavailable due to the exponential cardinality of BitVec n. isPolyTime_pure_ofFintype is an ergonomic wrapper over isPolyTime_pure_of_witnesses that certifies any deterministic function on a per-parameter finite input type of polynomially bounded cardinality as polynomial time, using finite-table witnesses for the constant query-selection, identity update, and some ∘ f output.
• VCVio/OracleComp/Coinductive/PolyTimeNontrivial.lean: This new file provides non-triviality certificates for the polynomial-time adversary model at canonical BoundaryData boundaries. It adds a SingleTapeTM-based snocComputer machine that appends a fixed bit to its input, with proofs snocComputer_phaseA, snocComputer_phaseB, and snocComputer_outputsWithinTime establishing its correctness and runtime, exposed as snocTimeComputable, snocPolyTimeComputable, and the EncPolyTime combinators appendBit and exists_iterate. The core theorem exists_poly_realizable_of_implements shows that any adversary implementing a pure predicate factors through an EncPolyTime initialization/output pair with polynomial description size—the key steps = 0 case is proved separately as realizable_of_implements_steps_eq_zero. These feed a counting/diagonalization argument (exists_diagonal_realizable, not_realizable_of_diagonal) that proves the two headline theorems exists_not_implements_pure_of_steps_eq_zero and exists_not_isPolyTime_pure: no polynomial-size machine adversary realizes every bitvector predicate. All proofs are complete with no sorry or admit.
• docs/agents/polytime-model.md: This is a new documentation file, docs/agents/polytime-model.md, which serves as an orientation guide for the Turing-machine-grounded polynomial-time adversary model used in the project. It explains the core definition (OracleComp.IsPolyTime), the purpose of each related file (e.g., BoundaryData, MachineAdversary, EncPolyTimeFam), and the rationale behind key design decisions such as pinned canonical boundaries and description-size bounds. The document inventories what is proven (e.g., exists_not_isPolyTime_pure, MachineAdversary.exists_polynomial_detTotalTime_le) versus what is deferred (e.g., bind closure, uniform variant), and provides semantics notes and a statement-site checklist for new security definitions.

---

Last updated: 2026-08-01 20:11 UTC.

[github-actions]

Build Timing Report

• Commit: 8735c21
• Message: Merge 95d8a9d into 1925179
• Ref: dtumad/polytime-v2
• Comparison baseline: 1925179 from the latest successful main run.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build ToMathlib VCVio LatticeCrypto Extern HashSig Examples VCVioWidgets; warm rebuild lake build ToMathlib VCVio LatticeCrypto Extern HashSig Examples VCVioWidgets; smoke test lake env lean VCVioTest/Smoke.lean.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	689.81	729.83	+40.02	ok
Warm rebuild	4.42	4.58	+0.16	ok
Smoke test	2.59	2.71	+0.12	ok

Incremental Rebuild Signal

• Warm rebuild saved 725.25s vs clean (159.35x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
68.00	71.00	-3.00	LatticeCrypto/MLDSA/Concrete/NTT.lean
67.00	67.00	+0.00	LatticeCrypto/MLKEM/Concrete/NTT.lean
35.00	34.00	+1.00	VCVio/ProgramLogic/Relational/SimulateQ.lean
34.00	37.00	-3.00	VCVio/ProgramLogic/Relational/Loom/Probabilistic.lean
32.00	29.00	+3.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Chain.lean
30.00	26.00	+4.00	LatticeCrypto/MLKEM/Concrete/Encoding.lean
28.00	25.00	+3.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean
26.00	25.00	+1.00	VCVio/OracleComp/Coercions/Add.lean
23.00	19.00	+4.00	VCVio/OracleComp/QueryTracking/Birthday.lean
22.00	23.00	-1.00	VCVio/CryptoFoundations/SecExp.lean
22.00	22.00	+0.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean
20.00	18.00	+2.00	VCVio/EvalDist/Defs/Basic.lean
20.00	22.00	-2.00	VCVio/ProgramLogic/Tactics/Unary/Internals.lean
20.00	21.00	-1.00	VCVio/CryptoFoundations/Fischlin/KnowledgeSoundness.lean
19.00	19.00	+0.00	VCVio/CryptoFoundations/ReplayFork.lean
19.00	17.00	+2.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Hops.lean
18.00	18.00	+0.00	VCVio/ProgramLogic/Tactics/Relational/Internals.lean
17.00	15.00	+2.00	VCVio/EvalDist/Monad/Basic.lean
17.00	17.00	+0.00	VCVio/CryptoFoundations/Fischlin/Completeness.lean
17.00	17.00	+0.00	Examples/SimpleTwoServerPIR.lean