Proof-carrying binary routine control -- definitions

This module adds value-level zero branching and canonical binary count-up loops to BinaryRoutine.

The loop certificate here deliberately differs from TM.BinaryForLoopSpec in two ways required by the routine interface. It starts at an arbitrary value, so body obligations are restricted to the reachable segment, and it accepts bounded iteration witnesses because BinaryRoutine.Sound advertises an upper bound rather than an exact runtime. Comparisons and endpoints remain exact.

structure Complexity.TM.BinaryForSegmentSpec {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) (bodyTime : ℕ → ℕ) (startValue limitValue : ℕ) : Type

A bounded execution certificate for the reachable segment of a canonical binary count-up loop.

Unlike BinaryForLoopSpec, iterations may finish before their advertised bound and obligations below startValue are not requested.

• counter_ne_limit : counterIdx ≠ limitIdx

  The counter and preserved-limit tapes are distinct.

• scanCfg : ℕ → Cfg n (body.binaryForTM counterIdx limitIdx).Q

  Canonical scanner configuration at each reachable counter value.

• iterationStartCfg : ℕ → Cfg n (body.binaryForTM counterIdx limitIdx).Q

  Configuration at the composite body-plus-successor entry.

• iterationDoneCfg : ℕ → Cfg n (body.binaryForTM counterIdx limitIdx).Q

  Configuration after the composite body-plus-successor iteration.

• doneCfg : Cfg n (body.binaryForTM counterIdx limitIdx).Q

  Final halted driver configuration.

• testRun (value : ℕ) : startValue ≤ value → value < limitValue → (body.binaryForTM counterIdx limitIdx).reachesIn (binaryForCompareTime limitValue) (self.scanCfg value) (self.iterationStartCfg value)

  A nonterminal comparison enters the composite iteration exactly.

• iterationTime : ℕ → ℕ

  Selected actual runtime of each reachable composite iteration.

• iterationTime_le (value : ℕ) : startValue ≤ value → value < limitValue → self.iterationTime value ≤ binaryForIterationTime bodyTime value

  The selected runtime stays within the advertised iteration bound.

• iterationRun (value : ℕ) : startValue ≤ value → value < limitValue → (body.binaryForTM counterIdx limitIdx).reachesIn (self.iterationTime value) (self.iterationStartCfg value) (self.iterationDoneCfg value)

  The composite iteration runs for its selected actual runtime.

• loopbackStep (value : ℕ) : startValue ≤ value → value < limitValue → (body.binaryForTM counterIdx limitIdx).step (self.iterationDoneCfg value) = some (self.scanCfg (value + 1))

  The preserving loopback seam starts the next comparison.

• doneRun : (body.binaryForTM counterIdx limitIdx).reachesIn (binaryForCompareTime limitValue) (self.scanCfg limitValue) self.doneCfg

  Equality at the limit completes the final comparison exactly.

• doneHalted : (body.binaryForTM counterIdx limitIdx).halted self.doneCfg

  The supplied final driver configuration is genuinely halted.

structure Complexity.TM.BinaryForSegmentSpaceSpec {n : ℕ} {body : TM n} {counterIdx limitIdx : Fin n} {bodyTime : ℕ → ℕ} {startValue limitValue : ℕ} (spec : body.BinaryForSegmentSpec counterIdx limitIdx bodyTime startValue limitValue) (inputLength spaceBound : ℕ) : Prop

All-prefix auxiliary-space obligations for a bounded reachable loop segment.

• testPrefixWithin (value time : ℕ) (cfg : Cfg n (body.binaryForTM counterIdx limitIdx).Q) : startValue ≤ value → value ≤ limitValue → time ≤ binaryForCompareTime limitValue → (body.binaryForTM counterIdx limitIdx).reachesIn time (spec.scanCfg value) cfg → cfg.WithinAuxSpace inputLength spaceBound

  Every reachable comparison prefix stays inside the shared budget.

• iterationPrefixWithin (value time : ℕ) (cfg : Cfg n (body.binaryForTM counterIdx limitIdx).Q) : startValue ≤ value → value < limitValue → time ≤ spec.iterationTime value → (body.binaryForTM counterIdx limitIdx).reachesIn time (spec.iterationStartCfg value) cfg → cfg.WithinAuxSpace inputLength spaceBound

  Every reachable composite-iteration prefix stays inside the budget.

def Complexity.BinaryRoutine.branchZero {n : ℕ} (idx : Fin n) (onZero onPositive : BinaryRoutine n) : BinaryRoutine n

Select between two routines by whether a canonical binary work value is zero. The blank branch is the zero branch.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.BinaryRoutine.binaryForStep {n : ℕ} (body : BinaryRoutine n) (counterIdx : Fin n) (values : BinaryValues n) : BinaryValues n

One pure count-up iteration: apply the body effect, then overwrite the preserved counter with its successor.

Equations

• body.binaryForStep counterIdx values = Function.update (body.effect values) counterIdx (values counterIdx + 1)

def Complexity.BinaryRoutine.binaryForValues {n : ℕ} (body : BinaryRoutine n) (counterIdx : Fin n) (initial : BinaryValues n) : ℕ → BinaryValues n

Pure work-vector trajectory after a number of count-up iterations.

Equations

• body.binaryForValues counterIdx initial 0 = initial
• body.binaryForValues counterIdx initial count.succ = body.binaryForStep counterIdx (body.binaryForValues counterIdx initial count)

def Complexity.BinaryRoutine.binaryForEmitted {n : ℕ} (body : BinaryRoutine n) (counterIdx : Fin n) (initial : BinaryValues n) : ℕ → List Bool

Word emitted by the first count iterations of a count-up body.

Equations

• body.binaryForEmitted counterIdx initial 0 = []
• body.binaryForEmitted counterIdx initial count.succ = body.binaryForEmitted counterIdx initial count ++ body.emitted (body.binaryForValues counterIdx initial count)

def Complexity.BinaryRoutine.binaryForBodyTime {n : ℕ} (body : BinaryRoutine n) (counterIdx : Fin n) (initial : BinaryValues n) (startValue value : ℕ) : ℕ

Body-time bound at an absolute counter value in a pure trajectory.

Equations

• body.binaryForBodyTime counterIdx initial startValue value = body.timeBound (body.binaryForValues counterIdx initial (value - startValue))

def Complexity.BinaryRoutine.binaryForCount {n : ℕ} (counterIdx limitIdx : Fin n) (values : BinaryValues n) : ℕ

Number of iterations remaining between the initial counter and limit.

Equations

• Complexity.BinaryRoutine.binaryForCount counterIdx limitIdx values = values limitIdx - values counterIdx

def Complexity.BinaryRoutine.binaryForTime {n : ℕ} (body : BinaryRoutine n) (counterIdx limitIdx : Fin n) (values : BinaryValues n) : ℕ

Advertised upper bound for a proof-carrying binary count-up loop.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.BinaryRoutine.binaryForIterationSpace {n : ℕ} (body : BinaryRoutine n) (counterIdx : Fin n) (initialSpace : ℕ) (initial : BinaryValues n) (count : ℕ) : ℕ

Space needed by one body-plus-successor iteration. This is a maximum, not a sum: sequential phases reuse the same work cells.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.BinaryRoutine.binaryForIterationSpaceMax {n : ℕ} (body : BinaryRoutine n) (counterIdx : Fin n) (initialSpace : ℕ) (initial : BinaryValues n) : ℕ → ℕ

Maximum space of the first count iterations.

Equations

• One or more equations did not get rendered due to their size.
• body.binaryForIterationSpaceMax counterIdx initialSpace initial 0 = initialSpace

def Complexity.BinaryRoutine.binaryForSpace {n : ℕ} (body : BinaryRoutine n) (counterIdx limitIdx : Fin n) (initialSpace : ℕ) (values : BinaryValues n) : ℕ

Reusable auxiliary-space bound for a binary count-up loop. Comparison width and per-iteration requirements are maximized, so the number of iterations does not itself consume space.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.BinaryRoutine.binaryFor {n : ℕ} (body : BinaryRoutine n) (counterIdx limitIdx : Fin n) : BinaryRoutine n

Iterate body while a canonical binary counter is strictly below a preserved canonical limit, incrementing the counter after every body run.

The domain honestly requires the body at every reachable intermediate value and requires its pure effect to preserve both controller values.

Equations

• One or more equations did not get rendered due to their size.