Tape cursors for the streaming circuit evaluator

The evaluator repeatedly rewinds, indexes, and extends canonical binary tapes. BinaryCursor keeps the complete canonical cell contents fixed while exposing the current zero-based read position. This is intentionally internal: the neutral endpoint and suffix predicates remain the public tape API.

def Complexity.CircuitCode.Machine.Internal.BinaryCursor (t : Tape) (bits : List Bool) (position : ℕ) : Prop

A zero-based cursor into a tape with exact canonical binary contents. The position may also equal the string length, in which case the cursor reads the first trailing blank.

Equations

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

def Complexity.CircuitCode.Machine.Internal.BinaryAtMarker (t : Tape) (bits : List Bool) : Prop

The boundary state reached after rewinding a canonical binary tape onto its left-end marker.

Equations

• Complexity.CircuitCode.Machine.Internal.BinaryAtMarker t bits = (t.head = 0 ∧ t.cells = (Complexity.Tape.init (List.map Complexity.Γ.ofBool bits)).cells)

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.ofHasBinaryPrefix {t : Tape} {bits : List Bool} (h : t.HasBinaryPrefix bits) (h₀ : t.cells 0 = Γ.start) : BinaryCursor t bits bits.length

An appendable binary prefix is a cursor at its first trailing blank once its left marker is known.

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.atFirstBit {t : Tape} {bits : List Bool} (hhead : t.head = 1) (hcells : t.cells = (Tape.init (List.map Γ.ofBool bits)).cells) : BinaryCursor t bits 0

Exact canonical cells and a head at cell one form the position-zero cursor.

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.startInvariant {t : Tape} {bits : List Bool} {position : ℕ} (h : BinaryCursor t bits position) : t.StartInvariant

A binary cursor carries the standard unique-left-marker invariant.

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.read_ne_start {t : Tape} {bits : List Bool} {position : ℕ} (h : BinaryCursor t bits position) : t.read ≠ Γ.start

A binary cursor is always parked away from the left-end marker.

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.preserve {t : Tape} {bits : List Bool} {position : ℕ} (h : BinaryCursor t bits position) : t.writeAndMove (TM.readBackWrite t.read).toΓ (TM.idleDir t.read) = t

The controller's preserve action leaves a cursor tape unchanged.

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.applyMoveRight {t : Tape} {bits : List Bool} {position : ℕ} (h : BinaryCursor t bits position) : t.writeAndMove (TM.readBackWrite t.read).toΓ Dir3.right = t.move Dir3.right

The controller's right action changes only the cursor head.

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.applyMoveLeft {t : Tape} {bits : List Bool} {position : ℕ} (h : BinaryCursor t bits position) : t.writeAndMove (TM.readBackWrite t.read).toΓ (TM.moveLeftDir t.read) = t.move Dir3.left

The controller's guarded-left action is an ordinary left move for a binary cursor.

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.toMarker {t : Tape} {bits : List Bool} (h : BinaryCursor t bits 0) : BinaryAtMarker (t.writeAndMove (TM.readBackWrite t.read).toΓ (TM.moveLeftDir t.read)) bits

The guarded-left action from position zero enters the left-marker state used by every controller rewind.

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.read_of_lt {t : Tape} {bits : List Bool} {position : ℕ} (h : BinaryCursor t bits position) (hlt : position < bits.length) : t.read = Γ.ofBool bits[position]

Reading a cursor strictly inside the string returns that indexed bit.

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.read_frontier {t : Tape} {bits : List Bool} (h : BinaryCursor t bits bits.length) : t.read = Γ.blank

A cursor at the frontier reads the first trailing blank.

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.hasBinaryString {t : Tape} {bits : List Bool} (h : BinaryCursor t bits 0) : t.HasBinaryString bits

A position-zero cursor exposes the neutral completed-string contract.

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.hasBinarySuffix {t : Tape} {bits : List Bool} (h : BinaryCursor t bits 0) : t.HasBinarySuffix bits

A position-zero cursor exposes the whole string as its remaining suffix.

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.moveRight {t : Tape} {bits : List Bool} {position : ℕ} (h : BinaryCursor t bits position) (hlt : position < bits.length) : BinaryCursor (t.move Dir3.right) bits (position + 1)

Moving right advances an in-bounds cursor and preserves its contents.

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.moveLeft {t : Tape} {bits : List Bool} {position : ℕ} (h : BinaryCursor t bits position) (hpos : 0 < position) : BinaryCursor (t.move Dir3.left) bits (position - 1)

Moving left retreats a positive cursor and preserves its contents.

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.hasBinaryPrefix {t : Tape} {bits : List Bool} (h : BinaryCursor t bits bits.length) : t.HasBinaryPrefix bits

A frontier cursor exposes the existing appendable-prefix contract.

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.append {t : Tape} {bits : List Bool} (bit : Bool) (h : BinaryCursor t bits bits.length) : BinaryCursor (t.writeAndMove (Γ.ofBool bit) Dir3.right) (bits ++ [bit]) (bits ++ [bit]).length

Writing at the frontier and moving right appends one bit and leaves a new frontier cursor.

theorem Complexity.CircuitCode.Machine.Internal.BinaryCursor.appendWritable {t : Tape} {bits : List Bool} (bit : Bool) (h : BinaryCursor t bits bits.length) : BinaryCursor (t.writeAndMove (Γw.ofBool bit).toΓ Dir3.right) (bits ++ [bit]) (bits ++ [bit]).length

Writable-alphabet form of append, matching the controller transition exactly.

theorem Complexity.CircuitCode.Machine.Internal.BinaryAtMarker.read_start {t : Tape} {bits : List Bool} (h : BinaryAtMarker t bits) : t.read = Γ.start

A canonical marker state reads the unique left-end marker.

theorem Complexity.CircuitCode.Machine.Internal.BinaryAtMarker.startInvariant {t : Tape} {bits : List Bool} (h : BinaryAtMarker t bits) : t.StartInvariant

A canonical marker state carries the standard tape invariant.

theorem Complexity.CircuitCode.Machine.Internal.BinaryAtMarker.applyMoveRight {t : Tape} {bits : List Bool} (h : BinaryAtMarker t bits) : t.writeAndMove (TM.readBackWrite t.read).toΓ Dir3.right = t.move Dir3.right

Writing back at the immutable marker and moving right is exactly an ordinary right move.

theorem Complexity.CircuitCode.Machine.Internal.BinaryAtMarker.returnToFirstBit {t : Tape} {bits : List Bool} (h : BinaryAtMarker t bits) : BinaryCursor (t.writeAndMove (TM.readBackWrite t.read).toΓ Dir3.right) bits 0

The controller's marker bounce returns to the position-zero cursor.