Structured RAM serialized-gate step — proof internals

theorem Complexity.RAM.Structured.GateStep.program_measured_internal (gate : CircuitCode.RawGate) (wires : List Bool) (value0 value1 : Bool) (hvalue0 : wires[gate.input₀]? = some value0) (hvalue1 : wires[gate.input₁]? = some value1) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec program (inputStore gate wires) final (stepCount gate) cost space ∧ cost ≤ timeBound gate wires ∧ space ≤ spaceBound gate wires ∧ final GateEval.outputReg = Input.bitValue (gate.eval value0 value1) ∧ final (memoBase gate + wires.length) = Input.bitValue (gate.eval value0 value1) ∧ ∀ (index : ℕ) (hindex : index < wires.length), final (memoBase gate + index) = Input.bitValue wires[index]

theorem Complexity.RAM.Structured.GateStep.program_exec_internal (gate : CircuitCode.RawGate) (wires : List Bool) (value0 value1 : Bool) (hvalue0 : wires[gate.input₀]? = some value0) (hvalue1 : wires[gate.input₁]? = some value1) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec program (inputStore gate wires) final (stepCount gate) cost space ∧ final GateEval.outputReg = Input.bitValue (gate.eval value0 value1) ∧ final (memoBase gate + wires.length) = Input.bitValue (gate.eval value0 value1) ∧ ∀ (index : ℕ) (hindex : index < wires.length), final (memoBase gate + index) = Input.bitValue wires[index]