Structured RAM decoded-gate evaluator — definitions

This kernel evaluates one already-decoded fan-in-two gate against a mutable wire memo. It uses indirect reads for both references and an indirect write to append the result. Boolean negation, AND, and OR are implemented arithmetically, so the instruction count is independent of the gate and wire values.

def Complexity.RAM.Structured.GateEval.opReg : ℕ

Encoded gate-operation bit: zero for AND and one for OR.

Equations

• Complexity.RAM.Structured.GateEval.opReg = 0

def Complexity.RAM.Structured.GateEval.negated0Reg : ℕ

Negation bit for the first gate input.

Equations

• Complexity.RAM.Structured.GateEval.negated0Reg = 1

def Complexity.RAM.Structured.GateEval.negated1Reg : ℕ

Negation bit for the second gate input.

Equations

• Complexity.RAM.Structured.GateEval.negated1Reg = 2

def Complexity.RAM.Structured.GateEval.address0Reg : ℕ

First gate-input index, then its physical memo address.

Equations

• Complexity.RAM.Structured.GateEval.address0Reg = 3

def Complexity.RAM.Structured.GateEval.address1Reg : ℕ

Second gate-input index, then the append address.

Equations

• Complexity.RAM.Structured.GateEval.address1Reg = 4

def Complexity.RAM.Structured.GateEval.wireCountReg : ℕ

Number of wire values already present in the memo.

Equations

• Complexity.RAM.Structured.GateEval.wireCountReg = 5

def Complexity.RAM.Structured.GateEval.value0Reg : ℕ

Loaded and optionally negated first input value.

Equations

• Complexity.RAM.Structured.GateEval.value0Reg = 6

def Complexity.RAM.Structured.GateEval.value1Reg : ℕ

Loaded and optionally negated second input value.

Equations

• Complexity.RAM.Structured.GateEval.value1Reg = 7

def Complexity.RAM.Structured.GateEval.outputReg : ℕ

Final gate value.

Equations

• Complexity.RAM.Structured.GateEval.outputReg = 8

def Complexity.RAM.Structured.GateEval.scratchReg : ℕ

Arithmetic scratch register.

Equations

• Complexity.RAM.Structured.GateEval.scratchReg = 9

def Complexity.RAM.Structured.GateEval.baseReg : ℕ

Physical base address of the wire memo.

Equations

• Complexity.RAM.Structured.GateEval.baseReg = 10

def Complexity.RAM.Structured.GateEval.wireBase : ℕ

First register occupied by memoized wire bits.

Equations

• Complexity.RAM.Structured.GateEval.wireBase = 11

def Complexity.RAM.Structured.GateEval.inputStore (gate : CircuitCode.RawGate) (wires : List Bool) : Store

Register representation of a decoded gate and its incoming wire memo.

Equations

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

def Complexity.RAM.Structured.GateEval.xorOps (value negated : ℕ) : List Basic

Branch-free arithmetic implementation of Boolean XOR.

Equations

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

def Complexity.RAM.Structured.GateEval.addressOps : List Basic

Convert the two absolute wire indices to physical memo addresses.

Equations

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

def Complexity.RAM.Structured.GateEval.loadOps : List Basic

Indirectly read the gate's two inputs.

Equations

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

def Complexity.RAM.Structured.GateEval.evalOps : List Basic

Branch-free AND/OR selection. Both candidate values are formed and the operation bit arithmetically selects the result.

Equations

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

def Complexity.RAM.Structured.GateEval.appendOps : List Basic

Compute the next memo address and append the result indirectly.

Equations

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

def Complexity.RAM.Structured.GateEval.ops : List Basic

Evaluate one gate and append its Boolean result to the wire memo.

Equations

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

def Complexity.RAM.Structured.GateEval.program : Cmd

Straight-line decoded-gate evaluator, grouped at semantic proof boundaries.

Equations

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

structure Complexity.RAM.Structured.GateEval.ReadyAt (base : ℕ) (gate : CircuitCode.RawGate) (wires : List Bool) (store : Store) : Prop

Semantic calling convention for evaluating a decoded gate in an existing store. The memo may begin at any address above the evaluator's control prefix.

• base_ge : wireBase ≤ base

  The memo is disjoint from the evaluator's control registers.

• op_eq : store opReg = Input.bitValue gate.opBit

  The operation register contains the canonical gate-operation bit.

• negated0_eq : store negated0Reg = Input.bitValue gate.negated₀

  The first negation register contains its canonical bit.

• negated1_eq : store negated1Reg = Input.bitValue gate.negated₁

  The second negation register contains its canonical bit.

• address0_eq : store address0Reg = gate.input₀

  The first address register contains the first absolute wire reference.

• address1_eq : store address1Reg = gate.input₁

  The second address register contains the second absolute wire reference.

• wireCount_eq : store wireCountReg = wires.length

  The wire-count register contains the current memo length.

• base_eq : store baseReg = base

  The base register points to the physical memo.

• wire_eq (index : ℕ) : index < wires.length → store (base + index) = match wires[index]? with | some bit => Input.bitValue bit | none => 0

  Physical memo cells contain the semantic wire bits.

def Complexity.RAM.Structured.GateEval.compiled : Program

Concrete compiled RAM kernel.

Equations

• Complexity.RAM.Structured.GateEval.compiled = Complexity.RAM.Structured.GateEval.program.compile

def Complexity.RAM.Structured.GateEval.stepCount : ℕ

The branch-free kernel always takes twenty source and compiled steps.

Equations

• Complexity.RAM.Structured.GateEval.stepCount = 20

def Complexity.RAM.Structured.GateEval.timeBound (wireCount : ℕ) : ℕ

Uniform logarithmic-cost budget for one gate.

Equations

• Complexity.RAM.Structured.GateEval.timeBound wireCount = 80 * (Complexity.RAM.bitlen (wireCount + Complexity.RAM.Structured.GateEval.wireBase + 1) + 1)

def Complexity.RAM.Structured.GateEval.spaceBound (wireCount : ℕ) : ℕ

Peak-space budget including the appended wire.

Equations

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

def Complexity.RAM.Structured.GateEval.logarithmicBound (wireCount : ℕ) : ℕ

Shifted logarithmic comparison function for one-gate time.

Equations

• Complexity.RAM.Structured.GateEval.logarithmicBound wireCount = Complexity.RAM.bitlen (wireCount + Complexity.RAM.Structured.GateEval.wireBase + 1) + 1

def Complexity.RAM.Structured.GateEval.quasilinearBound (wireCount : ℕ) : ℕ

Shifted quasilinear comparison function for the explicit memo space.

Equations

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