Fresh-input entry for proof-carrying binary routines #
This module packages the seam from a fresh Turing-machine configuration to a
canonical binary routine. The input is scanned once to obtain its length, and
the resulting routine inherits a total all-prefix ComputesInSpace contract.
Main results #
Sound.afterInputLength_hoareTimeSpacegives the per-input composed contract.Sound.afterInputLength_computesInSpacepackages the resulting function transducer.
theorem
Complexity.BinaryRoutine.Sound.afterInputLength_hoareTimeSpace
{n : ℕ}
{routine : BinaryRoutine n}
(hsound : routine.Sound)
(lengthIdx : Fin n)
(input : List Bool)
(hrequires : routine.requires (inputLengthValues lengthIdx input.length))
:
(afterInputLength lengthIdx routine).HoareTimeSpace
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) =>
inp = Tape.init (List.map Γ.ofBool input) ∧ (work = fun (x : Fin n) => Tape.init []) ∧ out = Tape.init [])
(fun (x : Tape) (x_1 : Fin n → Tape) (out : Tape) => out.HasOutput (afterInputLengthFunction lengthIdx routine input))
(afterInputLengthTime lengthIdx routine input.length) input.length
(afterInputLengthSpace lengthIdx routine input.length)
A sound routine with its unary input length loaded into one work value has the expected fresh-start time-and-space contract.
theorem
Complexity.BinaryRoutine.Sound.afterInputLength_computesInSpace
{n : ℕ}
{routine : BinaryRoutine n}
(hsound : routine.Sound)
(lengthIdx : Fin n)
(hrequires : ∀ (length : ℕ), routine.requires (inputLengthValues lengthIdx length))
:
(afterInputLength lengthIdx routine).ComputesInSpace (afterInputLengthFunction lengthIdx routine)
(afterInputLengthSpace lengthIdx routine)
A sound routine whose pure precondition holds at every input length yields a total function transducer with the composed all-prefix space bound.
theorem
Complexity.BinaryRoutine.afterInputLengthSpace_bigO_log
{n : ℕ}
(lengthIdx : Fin n)
(routine : BinaryRoutine n)
(hroutine :
BigO (fun (length : ℕ) => routine.spaceBound (TM.binaryLengthSpace length) (inputLengthValues lengthIdx length))
fun (length : ℕ) => Nat.log 2 length)
:
BigO (afterInputLengthSpace lengthIdx routine) fun (length : ℕ) => Nat.log 2 length
A logarithmic bound for the routine phase, measured from the binary-length counter's own budget, lifts to the complete fresh-input composition.