Concrete sparse-store arithmetic instruction kernel

This layer joins the width-efficient arithmetic machines to encoded sparse update. The destination address and two looked-up operands are supplied on canonical work tapes; the arithmetic result is written directly to the update controller's replacement tape, so no value-sized bridge is hidden between the two phases.

inductive Complexity.RAM.RegisterStore.Machine.BinaryInstrOp : Type

The three arithmetic operations shared by RAM register instructions.

• add : BinaryInstrOp
• sub : BinaryInstrOp
• mul : BinaryInstrOp

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instDecidableEqBinaryInstrOp : DecidableEq BinaryInstrOp

Equations

• Complexity.RAM.RegisterStore.Machine.instDecidableEqBinaryInstrOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes (n : ℕ) : Type

Eighteen pairwise-distinct tapes used by arithmetic followed by sparse update. Slots 0..12 are the update controller, slots 13 and 14 are the operands, and slots 15..17 are multiplication scratch.

• idx : Fin 18 → Fin n

  Complete injective physical assignment.

• injective : Function.Injective self.idx

  No two semantic roles alias.

def Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.update {n : ℕ} (tapes : BinaryInstructionTapes n) : EntryUpdateTapes n

The thirteen-tape sparse-update view.

Equations

• tapes.update = { idx := fun (i : Fin 13) => tapes.idx ⟨↑i, ⋯⟩, injective := ⋯ }

def Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.lhs {n : ℕ} (tapes : BinaryInstructionTapes n) : Fin n

First looked-up arithmetic operand.

Equations

• tapes.lhs = tapes.idx 13

def Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.rhs {n : ℕ} (tapes : BinaryInstructionTapes n) : Fin n

Second looked-up arithmetic operand.

Equations

• tapes.rhs = tapes.idx 14

def Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.shift {n : ℕ} (tapes : BinaryInstructionTapes n) : Fin n

Multiplication's shifted-multiplicand scratch tape.

Equations

• tapes.shift = tapes.idx 15

def Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.tmp {n : ℕ} (tapes : BinaryInstructionTapes n) : Fin n

Multiplication's first alternating scratch tape.

Equations

• tapes.tmp = tapes.idx 16

def Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.dbl {n : ℕ} (tapes : BinaryInstructionTapes n) : Fin n

Multiplication's second alternating scratch tape.

Equations

• tapes.dbl = tapes.idx 17

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.ne {n : ℕ} (tapes : BinaryInstructionTapes n) {i j : Fin 18} (hne : i ≠ j) : tapes.idx i ≠ tapes.idx j

Parent-slot inequality gives physical tape inequality.

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.update_ne_lhs {n : ℕ} (tapes : BinaryInstructionTapes n) (slot : Fin 13) : tapes.update.idx slot ≠ tapes.lhs

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.update_ne_rhs {n : ℕ} (tapes : BinaryInstructionTapes n) (slot : Fin 13) : tapes.update.idx slot ≠ tapes.rhs

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.update_ne_shift {n : ℕ} (tapes : BinaryInstructionTapes n) (slot : Fin 13) : tapes.update.idx slot ≠ tapes.shift

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.update_ne_tmp {n : ℕ} (tapes : BinaryInstructionTapes n) (slot : Fin 13) : tapes.update.idx slot ≠ tapes.tmp

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.update_ne_dbl {n : ℕ} (tapes : BinaryInstructionTapes n) (slot : Fin 13) : tapes.update.idx slot ≠ tapes.dbl

def Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.lhsLookupSlot (i : Fin 14) : Fin 18

Parent slots for a reusable lookup whose destination is lhs.

Equations

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

def Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.lhsLookup {n : ℕ} (tapes : BinaryInstructionTapes n) : EntryLookupRestoreTapes n

Reusable sparse lookup view targeting the first operand.

Equations

• tapes.lhsLookup = { idx := fun (i : Fin 14) => tapes.idx (Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.lhsLookupSlot i), injective := ⋯ }

def Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.rhsLookupSlot (i : Fin 14) : Fin 18

Parent slots for a reusable lookup whose destination is rhs.

Equations

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

def Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.rhsLookup {n : ℕ} (tapes : BinaryInstructionTapes n) : EntryLookupRestoreTapes n

Reusable sparse lookup view targeting the second operand.

Equations

• tapes.rhsLookup = { idx := fun (i : Fin 14) => tapes.idx (Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.rhsLookupSlot i), injective := ⋯ }

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.lhsLookup_count {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.lhsLookup.idx 9 = tapes.update.remaining

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.rhsLookup_count {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.rhsLookup.idx 9 = tapes.update.remaining

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.lhsLookup_countSource {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.lhsLookup.countSource = tapes.update.resultCount

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.rhsLookup_countSource {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.rhsLookup.countSource = tapes.update.resultCount

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.lhsLookup_querySource {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.lhsLookup.querySource = tapes.shift

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.rhsLookup_querySource {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.rhsLookup.querySource = tapes.shift

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.lhsLookup_destination {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.lhsLookup.destination = tapes.lhs

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.rhsLookup_destination {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.rhsLookup.destination = tapes.rhs

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.lhsLookup_copyScratch {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.lhsLookup.copyScratch = tapes.update.found

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.rhsLookup_copyScratch {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.rhsLookup.copyScratch = tapes.update.found

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.lhsLookup_ne_rhs {n : ℕ} (tapes : BinaryInstructionTapes n) (slot : Fin 14) : tapes.lhsLookup.idx slot ≠ tapes.rhs

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.rhsLookup_ne_lhs {n : ℕ} (tapes : BinaryInstructionTapes n) (slot : Fin 14) : tapes.rhsLookup.idx slot ≠ tapes.lhs

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.lhsLookup_ne_tmp {n : ℕ} (tapes : BinaryInstructionTapes n) (slot : Fin 14) : tapes.lhsLookup.idx slot ≠ tapes.tmp

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.rhsLookup_ne_tmp {n : ℕ} (tapes : BinaryInstructionTapes n) (slot : Fin 14) : tapes.rhsLookup.idx slot ≠ tapes.tmp

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.lhsLookup_ne_dbl {n : ℕ} (tapes : BinaryInstructionTapes n) (slot : Fin 14) : tapes.lhsLookup.idx slot ≠ tapes.dbl

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.rhsLookup_ne_dbl {n : ℕ} (tapes : BinaryInstructionTapes n) (slot : Fin 14) : tapes.rhsLookup.idx slot ≠ tapes.dbl

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.lhsLookup_ne_replacement {n : ℕ} (tapes : BinaryInstructionTapes n) (slot : Fin 14) : tapes.lhsLookup.idx slot ≠ tapes.update.replacement

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.rhsLookup_ne_replacement {n : ℕ} (tapes : BinaryInstructionTapes n) (slot : Fin 14) : tapes.rhsLookup.idx slot ≠ tapes.update.replacement

def Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.indirectLoadLookupSlot (i : Fin 14) : Fin 18

Parent slots for a loaded indirect read. The first operand supplies the runtime address and the update replacement tape receives the loaded value.

Equations

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

def Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.indirectLoadLookup {n : ℕ} (tapes : BinaryInstructionTapes n) : EntryLookupRestoreTapes n

Reusable loaded lookup view for indirect load.

Equations

• tapes.indirectLoadLookup = { idx := fun (i : Fin 14) => tapes.idx (Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.indirectLoadLookupSlot i), injective := ⋯ }

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.indirectLoadLookup_count {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.indirectLoadLookup.idx 9 = tapes.update.remaining

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.indirectLoadLookup_countSource {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.indirectLoadLookup.countSource = tapes.update.resultCount

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.indirectLoadLookup_querySource {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.indirectLoadLookup.querySource = tapes.lhs

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.indirectLoadLookup_destination {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.indirectLoadLookup.destination = tapes.update.replacement

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.indirectLoadLookup_copyScratch {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.indirectLoadLookup.copyScratch = tapes.update.found

def Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.mulSlot (i : Fin 6) : Fin 18

Multiplication-role parent slots. The accumulator deliberately aliases the update replacement slot 10.

Equations

• Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.mulSlot i = match ↑i with | 0 => 13 | 1 => 14 | 2 => 10 | 3 => 15 | 4 => 16 | x => 17

def Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.mul {n : ℕ} (tapes : BinaryInstructionTapes n) : TM.BinaryShiftMulABI n

Six-tape multiplication view, with its accumulator on update replacement.

Equations

• tapes.mul = { tape := { toFun := fun (i : Fin 6) => tapes.idx (Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.mulSlot i), inj' := ⋯ } }

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.mul_lhs {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.mul.lhs = tapes.lhs

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.mul_rhs {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.mul.rhs = tapes.rhs

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.mul_acc {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.mul.acc = tapes.update.replacement

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.mul_shift {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.mul.shift = tapes.shift

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.mul_tmp {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.mul.tmp = tapes.tmp

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.mul_dbl {n : ℕ} (tapes : BinaryInstructionTapes n) : tapes.mul.dbl = tapes.dbl

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.arithmeticDistinct {n : ℕ} (tapes : BinaryInstructionTapes n) : TM.BinaryRippleAddDistinct tapes.lhs tapes.rhs tapes.update.replacement

The addition/subtraction operands and result are pairwise distinct.

theorem Complexity.RAM.RegisterStore.Machine.BinaryInstructionTapes.subtractionDistinct {n : ℕ} (tapes : BinaryInstructionTapes n) : TM.BinaryRippleSubDistinct tapes.lhs tapes.rhs tapes.update.replacement

The same physical inequalities as a subtraction certificate.

structure Complexity.RAM.RegisterStore.Machine.ControlInstructionTapes (n : ℕ) : Type

The arithmetic/store ABI together with one disjoint canonical program- counter tape. Nineteen work tapes suffice for every RAM instruction.

• data : BinaryInstructionTapes n

  The complete data-instruction assignment.

• pc : Fin n

  Canonical binary program counter.

• pc_ne (slot : Fin 18) : self.pc ≠ self.data.idx slot

  The program counter aliases no data-instruction role.

theorem Complexity.RAM.RegisterStore.Machine.ControlInstructionTapes.data_ne_pc {n : ℕ} (tapes : ControlInstructionTapes n) (slot : Fin 18) : tapes.data.idx slot ≠ tapes.pc

Every data-instruction role is distinct from the program counter.

theorem Complexity.RAM.RegisterStore.Machine.ControlInstructionTapes.lhs_ne_pc {n : ℕ} (tapes : ControlInstructionTapes n) : tapes.data.lhs ≠ tapes.pc

The first loaded operand is distinct from the program counter.

theorem Complexity.RAM.RegisterStore.Machine.ControlInstructionTapes.pc_ne_lhs {n : ℕ} (tapes : ControlInstructionTapes n) : tapes.pc ≠ tapes.data.lhs

The program counter is distinct from the first loaded operand.

theorem Complexity.RAM.RegisterStore.Machine.ControlInstructionTapes.lookup_ne_pc {n : ℕ} (tapes : ControlInstructionTapes n) (slot : Fin 14) : tapes.data.lhsLookup.idx slot ≠ tapes.pc

No tape owned by the first lookup aliases the program counter.

def Complexity.RAM.RegisterStore.Machine.BinaryInstrOp.eval : BinaryInstrOp → ℕ → ℕ → ℕ

Pure result of the selected arithmetic operation.

Equations

• Complexity.RAM.RegisterStore.Machine.BinaryInstrOp.add.eval x✝¹ x✝ = x✝¹ + x✝
• Complexity.RAM.RegisterStore.Machine.BinaryInstrOp.sub.eval x✝¹ x✝ = x✝¹ - x✝
• Complexity.RAM.RegisterStore.Machine.BinaryInstrOp.mul.eval x✝¹ x✝ = x✝¹ * x✝

def Complexity.RAM.RegisterStore.Machine.binaryInstructionArithmeticTM {n : ℕ} (tapes : BinaryInstructionTapes n) : BinaryInstrOp → TM n

Concrete arithmetic phase selected in finite control.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.RegisterStore.Machine.binaryInstructionArithmeticTM tapes Complexity.RAM.RegisterStore.Machine.BinaryInstrOp.mul = Complexity.TM.binaryShiftMulTM tapes.mul

structure Complexity.RAM.RegisterStore.Machine.BinaryInstructionArithmeticResult {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (lhs rhs : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Uniform endpoint of the selected arithmetic phase.

• lhsValue : (finalWork tapes.lhs).HasBinaryNat lhs

  First operand is restored canonically.

• rhsValue : (finalWork tapes.rhs).HasBinaryNat rhs

  Second operand is restored canonically.

• result : (finalWork tapes.update.replacement).HasBinaryNat (op.eval lhs rhs)

  The update replacement tape contains the selected result.

• shift : (finalWork tapes.shift).HasBinaryNat 0

  Multiplication scratch is reset.

• tmp : (finalWork tapes.tmp).HasBinaryNat 0

  First alternating scratch is reset.

• dbl : (finalWork tapes.dbl).HasBinaryNat 0

  Second alternating scratch is reset.

• parked (i : Fin n) : TM.Parked (finalWork i)

  Every work head is parked at the phase boundary.

• frame (i : Fin n) : i ≠ tapes.lhs → i ≠ tapes.rhs → i ≠ tapes.update.replacement → i ≠ tapes.shift → i ≠ tapes.tmp → i ≠ tapes.dbl → finalWork i = initialWork i

  Tapes outside the six arithmetic roles are literally preserved.

def Complexity.RAM.RegisterStore.Machine.BinaryInstructionUpdateResult {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (store : Store) (address lhs rhs : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Uniform endpoint of arithmetic followed by encoded sparse update.

Equations

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

def Complexity.RAM.RegisterStore.Machine.binaryInstructionUpdateTM {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) : TM n

Arithmetic followed immediately by the fixed sparse update controller.

Equations

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

def Complexity.RAM.RegisterStore.Machine.directBinaryInstructionTM {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (destination source₀ source₁ : ℕ) : TM n

Load two direct register operands, prepare the direct destination address, then run arithmetic and sparse update.

Equations

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

def Complexity.RAM.RegisterStore.Machine.indirectLoadInstructionTM {n : ℕ} (tapes : BinaryInstructionTapes n) (destination addressRegister : ℕ) : TM n

Load an address register, perform the loaded indirect read into the update replacement tape, synthesize the direct destination, and update the store.

Equations

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

def Complexity.RAM.RegisterStore.Machine.immediateInstructionTM {n : ℕ} (tapes : BinaryInstructionTapes n) (destination value : ℕ) : TM n

Synthesize an immediate value and direct destination, then update the sparse store.

Equations

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

def Complexity.RAM.RegisterStore.Machine.indirectStoreInstructionTM {n : ℕ} (tapes : BinaryInstructionTapes n) (addressRegister source : ℕ) : TM n

Load the indirect destination and direct source, copy both into the update ABI, and update the sparse store.

Equations

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

def Complexity.RAM.RegisterStore.Machine.setProgramCounterTM {n : ℕ} (pc : Fin n) (target : ℕ) : TM n

Replace the canonical binary program counter by a fixed literal.

Equations

• Complexity.RAM.RegisterStore.Machine.setProgramCounterTM pc target = (Complexity.TM.resetBinaryWorkTM pc).seqTM (Complexity.TM.binaryAddConstTM pc target)

def Complexity.RAM.RegisterStore.Machine.zeroJumpInstructionTM {n : ℕ} (tapes : ControlInstructionTapes n) (source target : ℕ) : TM n

Conditional-zero control instruction. The fixed sparse read is cleared after branching so the reusable lookup ABI is restored at the endpoint.

Equations

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

def Complexity.RAM.RegisterStore.Machine.jumpInstructionTM {n : ℕ} (tapes : ControlInstructionTapes n) (target : ℕ) : TM n

Unconditional jump control instruction.

Equations

• Complexity.RAM.RegisterStore.Machine.jumpInstructionTM tapes target = Complexity.RAM.RegisterStore.Machine.setProgramCounterTM tapes.pc target

def Complexity.RAM.RegisterStore.Machine.haltInstructionTM {n : ℕ} : TM n

Halt is represented by a one-step exact no-op instruction kernel. The outer run controller detects halt before beginning another iteration.

Equations

• Complexity.RAM.RegisterStore.Machine.haltInstructionTM = Complexity.TM.skipTM

structure Complexity.RAM.RegisterStore.Machine.ControlInstructionReady {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue : ℕ) (work : Fin n → Tape) : Prop

Canonical entry boundary for a control instruction.

• lookup : EntryLookupStaticReady tapes.data.lhsLookup store work

  The fixed sparse-lookup ABI is ready.

• pc : (work tapes.pc).HasBinaryNat pcValue

  The program counter contains the represented value.

structure Complexity.RAM.RegisterStore.Machine.ControlInstructionResult {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Semantic endpoint shared by the three control-only instruction forms.

• ready : ControlInstructionReady tapes store pcValue finalWork

  The clean control ABI is restored with the new program counter.

• sourceCells : (finalWork tapes.data.update.entry.source).cells = (initialWork tapes.data.update.entry.source).cells

  The encoded source cells are read-only.

• frame (i : Fin n) : i ≠ tapes.pc → (∀ (slot : Fin 14), i ≠ tapes.data.lhsLookup.idx slot) → finalWork i = initialWork i

  Every tape outside the lookup ABI and PC assignment is preserved.

def Complexity.RAM.RegisterStore.Machine.setProgramCounterTime (pcValue target : ℕ) : ℕ

Runtime for replacing a canonical program counter by a literal.

Equations

• Complexity.RAM.RegisterStore.Machine.setProgramCounterTime pcValue target = Complexity.TM.resetBinaryWorkTime 1 pcValue.bits.length + 1 + Complexity.TM.binaryAddConstTime target 0

def Complexity.RAM.RegisterStore.Machine.zeroJumpInstructionTime {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue source target : ℕ) : ℕ

Runtime for conditional-zero control, including lookup and operand reset.

Equations

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

def Complexity.RAM.RegisterStore.Machine.jumpInstructionTime (pcValue target : ℕ) : ℕ

Runtime for an unconditional jump.

Equations

• Complexity.RAM.RegisterStore.Machine.jumpInstructionTime pcValue target = Complexity.RAM.RegisterStore.Machine.setProgramCounterTime pcValue target

def Complexity.RAM.RegisterStore.Machine.haltInstructionTime : ℕ

Runtime for the exact halt no-op.

Equations

• Complexity.RAM.RegisterStore.Machine.haltInstructionTime = 1

def Complexity.RAM.RegisterStore.Machine.DirectBinaryOperandsResult {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (source₀ source₁ : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Boundary after the two direct source-register lookups.

Equations

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

def Complexity.RAM.RegisterStore.Machine.DirectBinaryAddressResult {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (destination source₀ source₁ : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Boundary after the direct destination literal has been synthesized on the update query tape.

Equations

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

structure Complexity.RAM.RegisterStore.Machine.DirectBinaryUpdateReady {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (destination source₀ source₁ : ℕ) (work : Fin n → Tape) : Prop

Exact update-controller ABI established by the lookup and address-loading prefix of a direct arithmetic instruction.

• scanner : EntryScanReady tapes.update.entry (List.flatMap Entry.encode store) destination.bits work work
• lhs : (work tapes.lhs).HasBinaryNat (read store source₀)
• rhs : (work tapes.rhs).HasBinaryNat (read store source₁)
• replacement : (work tapes.update.replacement).HasBinaryNat 0
• shift : (work tapes.shift).HasBinaryNat 0
• tmp : (work tapes.tmp).HasBinaryNat 0
• dbl : (work tapes.dbl).HasBinaryNat 0
• remaining : (work tapes.update.remaining).HasBinaryNat (List.length store)
• found : (work tapes.update.found).HasBinaryNat 0
• resultCount : (work tapes.update.resultCount).HasBinaryNat (List.length store)
• parked (i : Fin n) : TM.Parked (work i)

def Complexity.RAM.RegisterStore.Machine.DirectBinaryInstructionResult {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (store : Store) (destination source₀ source₁ : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Semantic endpoint of a complete direct arithmetic instruction.

Equations

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

def Complexity.RAM.RegisterStore.Machine.IndirectLoadInstructionResult {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (destination addressRegister : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Semantic endpoint of a complete indirect load.

Equations

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

def Complexity.RAM.RegisterStore.Machine.ImmediateInstructionResult {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (destination value : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Semantic endpoint of one immediate assignment.

Equations

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

def Complexity.RAM.RegisterStore.Machine.IndirectStoreInstructionResult {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (addressRegister source : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Semantic endpoint of one indirect store.

Equations

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

def Complexity.RAM.RegisterStore.Machine.binaryInstructionArithmeticTime (op : BinaryInstrOp) (lhs rhs : ℕ) : ℕ

Operation-specific arithmetic budget.

Equations

• Complexity.RAM.RegisterStore.Machine.binaryInstructionArithmeticTime Complexity.RAM.RegisterStore.Machine.BinaryInstrOp.add lhs rhs = Complexity.TM.binaryRippleAddTime lhs rhs
• Complexity.RAM.RegisterStore.Machine.binaryInstructionArithmeticTime Complexity.RAM.RegisterStore.Machine.BinaryInstrOp.sub lhs rhs = Complexity.TM.binaryRippleSubTime lhs rhs
• Complexity.RAM.RegisterStore.Machine.binaryInstructionArithmeticTime Complexity.RAM.RegisterStore.Machine.BinaryInstrOp.mul lhs rhs = Complexity.TM.binaryShiftMulTime lhs rhs

def Complexity.RAM.RegisterStore.Machine.binaryInstructionUpdateTime {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (store : Store) (address lhs rhs : ℕ) : ℕ

Complete arithmetic-plus-update budget, including the composition seam.

Equations

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

def Complexity.RAM.RegisterStore.Machine.directBinaryInstructionTime {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (store : Store) (destination source₀ source₁ : ℕ) : ℕ

Complete direct arithmetic-instruction budget.

Equations

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

def Complexity.RAM.RegisterStore.Machine.indirectLoadInstructionTime {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (destination addressRegister : ℕ) : ℕ

Complete indirect-load instruction budget.

Equations

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

def Complexity.RAM.RegisterStore.Machine.immediateInstructionTime {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (destination value : ℕ) : ℕ

Complete immediate-assignment instruction budget.

Equations

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

def Complexity.RAM.RegisterStore.Machine.indirectStoreInstructionTime {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (addressRegister source : ℕ) : ℕ

Complete indirect-store instruction budget.

Equations

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