Addition of a fixed natural to a canonical binary tape #
This module exposes the literal-frame and resource contracts for a finite sequence of binary successors compiled from a hardwired natural constant.
Main results #
binaryAddConstTM_reachesIn_framegives the exact runtime and endpoint.binaryAddConstTM_hoareTime_framepackages the exact literal frame.binaryAddConstTM_hoareTimeSpace_framegives a width-based prefix bound.binaryAddConstTM_isTransducerproves append-only-output safety.
theorem
Complexity.TM.binaryAddConstTM_reachesIn_frame
{n : ℕ}
(idx : Fin n)
(constant dstValue : ℕ)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(hdst : (work₀ idx).HasBinaryNat dstValue)
(hinp : Parked inp₀)
(hother : ∀ (i : Fin n), i ≠ idx → Parked (work₀ i))
(hout : Parked out₀)
:
(binaryAddConstTM idx constant).reachesIn (binaryAddConstTime constant dstValue)
{ state := (binaryAddConstTM idx constant).qstart, input := inp₀, work := work₀, output := out₀ }
{ state := (binaryAddConstTM idx constant).qhalt, input := inp₀,
work := Function.update work₀ idx ((Tape.init (List.map Γ.ofBool (dstValue + constant).bits)).move Dir3.right),
output := out₀ }
Fixed-constant addition has the advertised exact runtime and changes only the destination tape.
theorem
Complexity.TM.binaryAddConstTM_hoareTime_frame
{n : ℕ}
(idx : Fin n)
(constant dstValue : ℕ)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(hdst : (work₀ idx).HasBinaryNat dstValue)
(hinp : Parked inp₀)
(hother : ∀ (i : Fin n), i ≠ idx → Parked (work₀ i))
(hout : Parked out₀)
:
(binaryAddConstTM idx constant).HoareTime
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀)
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) =>
inp = inp₀ ∧ work = Function.update work₀ idx ((Tape.init (List.map Γ.ofBool (dstValue + constant).bits)).move Dir3.right) ∧ out = out₀)
(binaryAddConstTime constant dstValue)
Time-bounded literal-frame contract for fixed-constant addition.
theorem
Complexity.TM.binaryAddConstTM_hoareTimeSpace_frame
{n : ℕ}
(idx : Fin n)
(constant dstValue inputLength initialSpace : ℕ)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(hdst : (work₀ idx).HasBinaryNat dstValue)
(hinp : Parked inp₀)
(hother : ∀ (i : Fin n), i ≠ idx → Parked (work₀ i))
(hout : Parked out₀)
(hworkSpace : ∀ (i : Fin n), (work₀ i).head ≤ initialSpace)
(hinputSpace : inp₀.head ≤ inputLength + initialSpace + 1)
:
(binaryAddConstTM idx constant).HoareTimeSpace
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀)
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) =>
inp = inp₀ ∧ work = Function.update work₀ idx ((Tape.init (List.map Γ.ofBool (dstValue + constant).bits)).move Dir3.right) ∧ out = out₀)
(binaryAddConstTime constant dstValue) inputLength (binaryAddConstSpace initialSpace constant dstValue)
Every prefix of fixed-constant addition respects a bound controlled by the final destination width.
theorem
Complexity.TM.binaryAddConstTM_isTransducer
{n : ℕ}
(idx : Fin n)
(constant : ℕ)
:
(binaryAddConstTM idx constant).IsTransducer
Fixed-constant addition never moves its output head left.