Structured RAM decoded-gate evaluator — proof internals #
theorem
Complexity.RAM.Structured.GateEval.routine_measured_internal
{bound base : ℕ}
{gate : CircuitCode.RawGate}
{wires : List Bool}
{store : Store}
(hready : ReadyAt base gate wires store)
(hstore : Internal.StoreEnvelope bound bound store)
(value0 value1 : Bool)
(hvalue0 : wires[gate.input₀]? = some value0)
(hvalue1 : wires[gate.input₁]? = some value1)
(happend : base + wires.length < bound)
:
∃ (final : Store),
Internal.MeasuredRuns program store final stepCount (80 * Internal.valueWidth bound)
(Internal.envelopeSpace bound bound) ∧ Internal.StoreEnvelope bound bound final ∧ final outputReg = Input.bitValue (gate.eval value0 value1) ∧ final (base + wires.length) = Input.bitValue (gate.eval value0 value1) ∧ final baseReg = base ∧ final wireCountReg = wires.length ∧ (∀ (index : ℕ) (hindex : index < wires.length), final (base + index) = Input.bitValue wires[index]) ∧ ∀ (index : ℕ), wireBase ≤ index → index ≠ base + wires.length → final index = store index
theorem
Complexity.RAM.Structured.GateEval.routine_exec_internal
{base : ℕ}
{gate : CircuitCode.RawGate}
{wires : List Bool}
{store : Store}
(hready : ReadyAt base gate wires store)
(value0 value1 : Bool)
(hvalue0 : wires[gate.input₀]? = some value0)
(hvalue1 : wires[gate.input₁]? = some value1)
:
∃ (final : Store) (cost : ℕ) (space : ℕ),
Exec program store final stepCount cost space ∧ final outputReg = Input.bitValue (gate.eval value0 value1) ∧ final (base + wires.length) = Input.bitValue (gate.eval value0 value1) ∧ final baseReg = base ∧ final wireCountReg = wires.length ∧ (∀ (index : ℕ) (hindex : index < wires.length), final (base + index) = Input.bitValue wires[index]) ∧ ∀ (index : ℕ), wireBase ≤ index → index ≠ base + wires.length → final index = store index
theorem
Complexity.RAM.Structured.GateEval.program_measured_internal
(gate : CircuitCode.RawGate)
(wires : List Bool)
(value0 value1 : Bool)
(hvalue0 : wires[gate.input₀]? = some value0)
(hvalue1 : wires[gate.input₁]? = some value1)
(hgate : gate.WellFormedAt wires.length)
:
∃ (final : Store) (cost : ℕ) (space : ℕ),
Exec program (inputStore gate wires) final stepCount cost space ∧ cost ≤ timeBound wires.length ∧ space ≤ spaceBound wires.length ∧ final outputReg = Input.bitValue (gate.eval value0 value1) ∧ final (wireBase + wires.length) = Input.bitValue (gate.eval value0 value1) ∧ ∀ (index : ℕ) (hindex : index < wires.length), final (wireBase + index) = Input.bitValue wires[index]