Structured RAM iterable serialized-gate step — proof internals

theorem Complexity.RAM.Structured.GateStreamStep.marshal_ready_internal {gateStart nextPointer remaining base : ℕ} {gate : CircuitCode.RawGate} {wires : List Bool} {store : Store} (hparsed : Parsed gateStart nextPointer remaining base gate wires store) : GateEval.ReadyAt base gate wires (Basic.execList marshalOps store) ∧ Basic.execList marshalOps store spillPointerReg = nextPointer ∧ Basic.execList marshalOps store spillRemainingReg = remaining

theorem Complexity.RAM.Structured.GateStreamStep.routine_exec_internal {gateStart base : ℕ} {gate : CircuitCode.RawGate} {tail wires : List Bool} {store : Store} (hready : Ready gateStart base gate tail wires store) (hbound : Internal.StoreEnvelope (codeEnd gateStart gate tail) (codeEnd gateStart gate tail) store) (value0 value1 : Bool) (hvalue0 : wires[gate.input₀]? = some value0) (hvalue1 : wires[gate.input₁]? = some value1) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec routine store final (stepCount gate) cost space ∧ final UnaryDecode.pointerReg = gateStart + gate.encode.length ∧ final UnaryDecode.remainingReg = tail.length ∧ final memoBaseReg = base ∧ final wireCountMetaReg = wires.length + 1 ∧ final (base + wires.length) = Input.bitValue (gate.eval value0 value1) ∧ (∀ (index : ℕ) (hindex : index < wires.length), final (base + index) = Input.bitValue wires[index]) ∧ ∀ (delta : ℕ), final (gateStart + gate.encode.length + delta) = match tail[delta]? with | some bit => Input.bitValue bit | none => 0