Compositional width bounds for binary routines -- proof internals #
theorem
Complexity.BinaryRoutine.SpaceBoundInLogAt.of_le_internal
{n : ℕ}
{routine : BinaryRoutine n}
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{bound : ℕ → ℕ}
(hle : ∀ (inputLength : ℕ), routine.spaceBound (initialSpace inputLength) (values inputLength) ≤ bound inputLength)
(hbound : BigO bound fun (inputLength : ℕ) => Nat.log 2 inputLength)
:
routine.SpaceBoundInLogAt initialSpace values
theorem
Complexity.BinaryRoutine.SpaceBoundInLogAt.restrict_internal
{n : ℕ}
{routine : BinaryRoutine n}
{requires : BinaryValues n → Prop}
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
(hspace : routine.SpaceBoundInLogAt initialSpace values)
:
(routine.restrict requires).SpaceBoundInLogAt initialSpace values
theorem
Complexity.BinaryRoutine.SpaceBoundInLogAt.seq_internal
{n : ℕ}
{first second : BinaryRoutine n}
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
(hfirst : first.SpaceBoundInLogAt initialSpace values)
(hsecond : second.SpaceBoundInLogAt initialSpace fun (inputLength : ℕ) => first.effect (values inputLength))
:
(first.seq second).SpaceBoundInLogAt initialSpace values
theorem
Complexity.BinaryRoutine.SpaceBoundInLogAt.branchZero_internal
{n : ℕ}
{onZero onPositive : BinaryRoutine n}
(idx : Fin n)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
(hzero : onZero.SpaceBoundInLogAt initialSpace values)
(hpositive : onPositive.SpaceBoundInLogAt initialSpace values)
:
(branchZero idx onZero onPositive).SpaceBoundInLogAt initialSpace values
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.mono_internal
{n : ℕ}
{routine : BinaryRoutine n}
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width width' : ℕ → ℕ}
(hspace : routine.SpaceBoundByWidthAt initialSpace values width)
(hle : ∀ (inputLength : ℕ), width inputLength ≤ width' inputLength)
:
routine.SpaceBoundByWidthAt initialSpace values width'
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.restrict_internal
{n : ℕ}
{routine : BinaryRoutine n}
{requires : BinaryValues n → Prop}
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hspace : routine.SpaceBoundByWidthAt initialSpace values width)
:
(routine.restrict requires).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.emitBits_internal
{n : ℕ}
(word : List Bool)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
:
(emitBits word).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.identity_internal
{n : ℕ}
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
:
identity.SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.clear_internal
{n : ℕ}
(idx : Fin n)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hvalue : ∀ (inputLength : ℕ), values inputLength idx ≤ width inputLength)
:
(clear idx).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.binarySucc_internal
{n : ℕ}
(idx : Fin n)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hvalue : ∀ (inputLength : ℕ), values inputLength idx ≤ width inputLength)
:
(binarySucc idx).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.binaryPred_internal
{n : ℕ}
(idx : Fin n)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hvalue : ∀ (inputLength : ℕ), values inputLength idx - 1 + 1 ≤ width inputLength)
:
(binaryPred idx).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.binaryCopy_internal
{n : ℕ}
(srcIdx dstIdx counterIdx : Fin n)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hsrc : ∀ (inputLength : ℕ), values inputLength srcIdx ≤ width inputLength)
(hdst : ∀ (inputLength : ℕ), values inputLength dstIdx ≤ width inputLength)
:
(binaryCopy srcIdx dstIdx counterIdx).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.addConst_internal
{n : ℕ}
(idx : Fin n)
(constant : ℕ)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hvalue : ∀ (inputLength : ℕ), values inputLength idx + constant ≤ width inputLength)
:
(addConst idx constant).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.add_internal
{n : ℕ}
(srcIdx dstIdx counterIdx : Fin n)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hsrc : ∀ (inputLength : ℕ), values inputLength srcIdx ≤ width inputLength)
(hsum : ∀ (inputLength : ℕ), values inputLength dstIdx + values inputLength srcIdx ≤ width inputLength)
:
(add srcIdx dstIdx counterIdx).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.mulAdd_internal
{n : ℕ}
(leftIdx rightIdx accIdx mulCounterIdx addCounterIdx : Fin n)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hleft : ∀ (inputLength : ℕ), values inputLength leftIdx ≤ width inputLength)
(hright : ∀ (inputLength : ℕ), values inputLength rightIdx ≤ width inputLength)
(htotal :
∀ (inputLength : ℕ),
values inputLength accIdx + values inputLength leftIdx * values inputLength rightIdx + values inputLength leftIdx ≤ width inputLength)
:
(mulAdd leftIdx rightIdx accIdx mulCounterIdx addCounterIdx).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.evalPolynomial_internal
{n : ℕ}
(inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx : Fin n)
(p : Polynomial ℕ)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hvalue : ∀ (inputLength : ℕ), 2 * TM.binaryPolynomialValueCap p (values inputLength inputIdx) ≤ width inputLength)
:
(evalPolynomial inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx p).SpaceBoundByWidthAt initialSpace values
width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.emitNatCode_internal
{n : ℕ}
(counterIdx valueIdx : Fin n)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hvalue : ∀ (inputLength : ℕ), values inputLength valueIdx ≤ width inputLength)
:
(emitNatCode counterIdx valueIdx).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.emitRawGate_internal
{n : ℕ}
(op : AndOrOp)
(negated₀ negated₁ : Bool)
(emitCounterIdx input₀Idx input₁Idx : Fin n)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hinput₀ : ∀ (inputLength : ℕ), values inputLength input₀Idx ≤ width inputLength)
(hinput₁ : ∀ (inputLength : ℕ), values inputLength input₁Idx ≤ width inputLength)
:
(emitRawGate op negated₀ negated₁ emitCounterIdx input₀Idx input₁Idx).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.emitRawGateStep_internal
{n : ℕ}
(op : AndOrOp)
(negated₀ negated₁ : Bool)
(emitCounterIdx availableIdx input₀Idx input₁Idx : Fin n)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(havailable : ∀ (inputLength : ℕ), values inputLength availableIdx ≤ width inputLength)
(hinput₀ : ∀ (inputLength : ℕ), values inputLength input₀Idx ≤ width inputLength)
(hinput₁ : ∀ (inputLength : ℕ), values inputLength input₁Idx ≤ width inputLength)
:
(emitRawGateStep op negated₀ negated₁ emitCounterIdx availableIdx input₀Idx input₁Idx).SpaceBoundByWidthAt initialSpace
values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.seq_internal
{n : ℕ}
{first second : BinaryRoutine n}
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hfirst : first.SpaceBoundByWidthAt initialSpace values width)
(hsecond : second.SpaceBoundByWidthAt initialSpace (fun (inputLength : ℕ) => first.effect (values inputLength)) width)
:
(first.seq second).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.set_internal
{n : ℕ}
(idx : Fin n)
(value : ℕ)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hcurrent : ∀ (inputLength : ℕ), values inputLength idx ≤ width inputLength)
(hvalue : ∀ (inputLength : ℕ), value ≤ width inputLength)
:
(set idx value).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.seqList_internal
{n : ℕ}
(routines : List (BinaryRoutine n))
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hspace : SeqListSpaceBoundByWidthAt routines initialSpace values width)
:
(seqList routines).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SeqListSpaceBoundByWidthAt.append_internal
{n : ℕ}
(first second : List (BinaryRoutine n))
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hfirst : SeqListSpaceBoundByWidthAt first initialSpace values width)
(hsecond :
SeqListSpaceBoundByWidthAt second initialSpace (fun (inputLength : ℕ) => (seqList first).effect (values inputLength))
width)
:
SeqListSpaceBoundByWidthAt (first ++ second) initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.repeatRoutine_of_invariant_internal
{n : ℕ}
(count : ℕ)
(routine : BinaryRoutine n)
(invariant : BinaryValues n → Prop)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hvalues : ∀ (inputLength : ℕ), invariant (values inputLength))
(hspace :
∀ (trajectory : ℕ → BinaryValues n),
(∀ (inputLength : ℕ), invariant (trajectory inputLength)) →
routine.SpaceBoundByWidthAt initialSpace trajectory width)
(heffect : ∀ (current : BinaryValues n), invariant current → invariant (routine.effect current))
:
(repeatRoutine count routine).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.branchZero_internal
{n : ℕ}
{onZero onPositive : BinaryRoutine n}
(idx : Fin n)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hzero : onZero.SpaceBoundByWidthAt initialSpace values width)
(hpositive : onPositive.SpaceBoundByWidthAt initialSpace values width)
:
(branchZero idx onZero onPositive).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.to_log_internal
{n : ℕ}
{routine : BinaryRoutine n}
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hspace : routine.SpaceBoundByWidthAt initialSpace values width)
(hinitial : BigO initialSpace fun (inputLength : ℕ) => Nat.log 2 inputLength)
(p : Polynomial ℕ)
(hwidth : ∀ (inputLength : ℕ), width inputLength ≤ Polynomial.eval inputLength p)
:
routine.SpaceBoundInLogAt initialSpace values
theorem
Complexity.BinaryRoutine.SpaceBoundInLogAt.emitBits_internal
{n : ℕ}
(word : List Bool)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
(hinitial : BigO initialSpace fun (inputLength : ℕ) => Nat.log 2 inputLength)
:
(emitBits word).SpaceBoundInLogAt initialSpace values
theorem
Complexity.BinaryRoutine.SpaceBoundInLogAt.identity_internal
{n : ℕ}
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
(hinitial : BigO initialSpace fun (inputLength : ℕ) => Nat.log 2 inputLength)
:
identity.SpaceBoundInLogAt initialSpace values
theorem
Complexity.BinaryRoutine.BinaryForSpaceEnvelope.iterationSpaceMax_le_internal
{n : ℕ}
{body : BinaryRoutine n}
{counterIdx limitIdx : Fin n}
{initialSpace : ℕ}
{initial : BinaryValues n}
{bound : ℕ}
(envelope : body.BinaryForSpaceEnvelope counterIdx limitIdx initialSpace initial bound)
:
body.binaryForIterationSpaceMax counterIdx initialSpace initial (binaryForCount counterIdx limitIdx initial) ≤ bound
theorem
Complexity.BinaryRoutine.BinaryForSpaceEnvelope.binaryForSpace_le_internal
{n : ℕ}
{body : BinaryRoutine n}
{counterIdx limitIdx : Fin n}
{initialSpace : ℕ}
{initial : BinaryValues n}
{bound : ℕ}
(envelope : body.BinaryForSpaceEnvelope counterIdx limitIdx initialSpace initial bound)
:
theorem
Complexity.BinaryRoutine.BinaryForSpaceEnvelope.spaceBound_le_internal
{n : ℕ}
{body : BinaryRoutine n}
{counterIdx limitIdx : Fin n}
{initialSpace : ℕ}
{initial : BinaryValues n}
{bound : ℕ}
(envelope : body.BinaryForSpaceEnvelope counterIdx limitIdx initialSpace initial bound)
:
theorem
Complexity.BinaryRoutine.SpaceBoundInLogAt.binaryFor_of_envelope_internal
{n : ℕ}
{body : BinaryRoutine n}
{counterIdx limitIdx : Fin n}
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{bound : ℕ → ℕ}
(henvelope :
∀ (inputLength : ℕ),
body.BinaryForSpaceEnvelope counterIdx limitIdx (initialSpace inputLength) (values inputLength) (bound inputLength))
(hbound : BigO bound fun (inputLength : ℕ) => Nat.log 2 inputLength)
:
(body.binaryFor counterIdx limitIdx).SpaceBoundInLogAt initialSpace values
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.binaryFor_of_envelope_internal
{n : ℕ}
{body : BinaryRoutine n}
{counterIdx limitIdx : Fin n}
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(constant : ℕ)
(henvelope :
∀ (inputLength : ℕ),
body.BinaryForSpaceEnvelope counterIdx limitIdx (initialSpace inputLength) (values inputLength)
(initialSpace inputLength + constant * (width inputLength).size + constant))
:
(body.binaryFor counterIdx limitIdx).SpaceBoundByWidthAt initialSpace values width
theorem
Complexity.BinaryRoutine.SpaceBoundByWidthAt.binaryFor_of_clamped_body_internal
{n : ℕ}
{body : BinaryRoutine n}
{counterIdx limitIdx : Fin n}
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hlimit : ∀ (inputLength : ℕ), values inputLength limitIdx ≤ width inputLength)
(hcounter :
∀ (inputLength count : ℕ),
count < binaryForCount counterIdx limitIdx (values inputLength) →
body.binaryForValues counterIdx (values inputLength) count counterIdx ≤ width inputLength)
(hbody :
body.SpaceBoundByWidthAt (fun (code : ℕ) => initialSpace (Nat.unpair code).1)
(body.binaryForClampedValues counterIdx limitIdx values) fun (code : ℕ) => width (Nat.unpair code).1)
:
(body.binaryFor counterIdx limitIdx).SpaceBoundByWidthAt initialSpace values width