Efficient saved-coin evaluators for typed PPT programs

A strict PPT witness realizes its result from a uniformly sampled polynomial-length tape. Its deterministic saved-coin evaluator has a genuine TM certificate, including tape preparation and cleanup. Normalizing arbitrary tapes to the witness budget gives a total typed evaluator whose every result belongs to the original program's support. No decoder on arbitrary output words is assumed: supported output words have unique preimages under the declared encoding.

Main results

• Cslib.Probability.IsPPTOn.exists_coin_machine: one finite machine realizes all inputs from uniform saved coins.
• Cslib.Probability.IsPPTOn.exists_polyTime_coin_evaluator: efficient evaluation on raw words.
• Cslib.Probability.IsPPTOn.exists_total_seeded_evaluator: a total efficient typed evaluator, supported on every seed and exact under any sufficiently long uniform seed.
• Cslib.Probability.IsPPTOn.exists_seeded_evaluator: the exact-budget specialization.
• Cslib.Probability.IsPPTOn.exists_padded_coin_evaluator, Cslib.Probability.IsPPTOn.exists_padded_bool_coin_evaluator: one longer saved tape can be reused across inputs of different lengths.

References

Adapted from Computability/Probabilistic/CoinTape.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the common machine, standard pair encoding and tidy computability calculus.

theorem Cslib.Probability.IsPPTOn.exists_coin_machine {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → ProbComp β} (h : IsPPTOn input output program) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : Turing.MultiTapePTM k Bool State) (c : ℕ) (d : ℕ), ∀ (a : α), PMF.map (⇑output) (program a).eval = PMF.map (fun (coins : List Bool) => machine.runClosedCoins coins (input a)) (BitString.uniformList (c * ((input a).length + 1) ^ d))

One finite machine and one polynomial budget realize the whole program family from saved fair bits. Neither witness depends on the input value.

theorem Cslib.Probability.IsPPTOn.exists_polyTime_coin_evaluator {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → ProbComp β} (h : IsPPTOn input output program) : ∃ (c : ℕ) (d : ℕ) (evaluate : List Bool → List Bool → List Bool), Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : List Bool × List Bool) => evaluate p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits ∧ ∀ (a : α), PMF.map (⇑output) (program a).eval = PMF.map (fun (coins : List Bool) => evaluate coins (input a)) (BitString.uniformList (c * ((input a).length + 1) ^ d))

The encoded evaluator accepts arbitrary raw input and coin words and is uniformly polynomial time. Its exact realization law applies to encoded inputs at the stated budget.

theorem Cslib.Probability.IsPPTOn.exists_total_seeded_evaluator {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → ProbComp β} (h : IsPPTOn input output program) : ∃ (c : ℕ) (d : ℕ) (evaluate : α → List Bool → β), Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : α × List Bool) => evaluate p.1 p.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) output ∧ (∀ (a : α) (coins : List Bool), evaluate a coins ∈ (program a).eval.support) ∧ ∀ (a : α) (length : ℕ), c * ((input a).length + 1) ^ d ≤ length → (program a).eval = PMF.map (evaluate a) (BitString.uniformList length)

Every typed PPT program has a total deterministic polynomial-time evaluator. Every seed produces a supported result. Short seeds are padded; longer seeds are truncated to the program's budget. Every uniform seed at least that long yields exactly the program's distribution.

Computability is relative to the output encoding and requires no decoder for invalid words.

theorem Cslib.Probability.IsPPTOn.exists_seeded_evaluator {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → ProbComp β} (h : IsPPTOn input output program) : ∃ (c : ℕ) (d : ℕ) (evaluate : α → List Bool → β), Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : α × List Bool) => evaluate p.1 p.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) output ∧ ∀ (a : α), (program a).eval = PMF.map (evaluate a) (BitString.uniformList (c * ((input a).length + 1) ^ d))

The exact-budget specialization of the total seeded evaluator.

theorem Cslib.Probability.IsPPTOn.exists_padded_coin_evaluator {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → ProbComp β} (h : IsPPTOn input output program) : ∃ (c : ℕ) (d : ℕ) (evaluate : List Bool → List Bool → List Bool), Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : List Bool × List Bool) => evaluate p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits ∧ ∀ (a : α) (length : ℕ), c * ((input a).length + 1) ^ d ≤ length → PMF.map (⇑output) (program a).eval = PMF.map (fun (coins : List Bool) => evaluate coins (input a)) (BitString.uniformList length)

A typed program can use one larger saved tape across inputs of different lengths. The raw word evaluator trims to each input's own budget and accepts arbitrary encoded words.

theorem Cslib.Probability.IsPPTOn.exists_padded_bool_coin_evaluator {α : Type} {input : α ↪ List Bool} {program : α → ProbComp Bool} (h : IsPPTOn input Turing.MultiTapeTM.encBool program) : ∃ (c : ℕ) (d : ℕ) (evaluate : List Bool → List Bool → List Bool), Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : List Bool × List Bool) => evaluate p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits ∧ ∀ (a : α) (length : ℕ), c * ((input a).length + 1) ^ d ≤ length → (program a).eval = PMF.map (fun (coins : List Bool) => (evaluate coins (input a)).headD false) (BitString.uniformList length)

Reading the raw evaluator's first bit preserves a Boolean program's distribution. The shared tape budget may depend only on a bound on the encoded input size.