Linear-time canonical binary addition -- rewind proof internals

This module packages the three-rewind tail of binaryRippleAddTM into one framed Hoare-time contract.

def Complexity.TM.binaryRippleAddCanonicalTape (bits : List Bool) : Tape

Canonical parked tape containing the supplied little-endian binary digits.

Equations

• Complexity.TM.binaryRippleAddCanonicalTape bits = (Complexity.Tape.init (List.map Complexity.Γ.ofBool bits)).move Complexity.Dir3.right

theorem Complexity.TM.binaryRippleAddRewindTM_hoareTime_frame_internal {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) (hdistinct : BinaryRippleAddDistinct lhsIdx rhsIdx resultIdx) (lhsBits rhsBits resultBits : List Bool) (lhsBound rhsBound resultBound : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hlhs : (work₀ lhsIdx).HasBinaryContent lhsBits) (hlhsStart : (work₀ lhsIdx).cells 0 = Γ.start) (hlhsHead : 1 ≤ (work₀ lhsIdx).head ∧ (work₀ lhsIdx).head ≤ lhsBound) (hrhs : (work₀ rhsIdx).HasBinaryContent rhsBits) (hrhsStart : (work₀ rhsIdx).cells 0 = Γ.start) (hrhsHead : 1 ≤ (work₀ rhsIdx).head ∧ (work₀ rhsIdx).head ≤ rhsBound) (hresult : (work₀ resultIdx).HasBinaryContent resultBits) (hresultStart : (work₀ resultIdx).cells 0 = Γ.start) (hresultHead : 1 ≤ (work₀ resultIdx).head ∧ (work₀ resultIdx).head ≤ resultBound) (hinput : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → Parked (work₀ i)) (houtput : Parked out₀) : ((rewindWorkTM lhsIdx).seqTM ((rewindWorkTM rhsIdx).seqTM (rewindWorkTM resultIdx))).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 lhsIdx = binaryRippleAddCanonicalTape lhsBits ∧ work rhsIdx = binaryRippleAddCanonicalTape rhsBits ∧ work resultIdx = binaryRippleAddCanonicalTape resultBits ∧ (∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → work i = work₀ i) ∧ out = out₀) (lhsBound + rhsBound + resultBound + 8)