Concrete sparse-store arithmetic instruction kernel

This surface exposes the first complete instruction-level composition in the RAM-to-TM direction: two canonical operands are combined by a width-efficient binary machine and the result is committed by the fixed encoded-store update controller. A redirected form writes the new store to a fresh work buffer.

theorem Complexity.RAM.RegisterStore.Machine.binaryInstructionArithmeticTM_hoareTime_frame {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (lhs rhs : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hlhs : (work₀ tapes.lhs).HasBinaryNat lhs) (hrhs : (work₀ tapes.rhs).HasBinaryNat rhs) (hresult : (work₀ tapes.update.replacement).HasBinaryNat 0) (hshift : (work₀ tapes.shift).HasBinaryNat 0) (htmp : (work₀ tapes.tmp).HasBinaryNat 0) (hdbl : (work₀ tapes.dbl).HasBinaryNat 0) (hinput : TM.Parked inp₀) (hwork : ∀ (i : Fin n), TM.Parked (work₀ i)) (houtput : TM.Parked out₀) : (binaryInstructionArithmeticTM tapes op).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ BinaryInstructionArithmeticResult tapes op lhs rhs work₀ work ∧ out = out₀) (binaryInstructionArithmeticTime op lhs rhs)

Uniform framed contract for the selected arithmetic operation.

theorem Complexity.RAM.RegisterStore.Machine.binaryInstructionUpdateTM_hoareTime_frame {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (store : Store) (address lhs rhs : ℕ) (emittedBits : List Bool) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hcanonical : Canonical store) (hready : EntryScanReady tapes.update.entry (List.flatMap Entry.encode store) address.bits initialWork initialWork) (hlhs : (initialWork tapes.lhs).HasBinaryNat lhs) (hrhs : (initialWork tapes.rhs).HasBinaryNat rhs) (hresult : (initialWork tapes.update.replacement).HasBinaryNat 0) (hshift : (initialWork tapes.shift).HasBinaryNat 0) (htmp : (initialWork tapes.tmp).HasBinaryNat 0) (hdbl : (initialWork tapes.dbl).HasBinaryNat 0) (hremaining : (initialWork tapes.update.remaining).HasBinaryNat (List.length store)) (hfound : (initialWork tapes.update.found).HasBinaryNat 0) (hresultCount : (initialWork tapes.update.resultCount).HasBinaryNat (List.length store)) (hinput : TM.Parked inp₀) (hwork : ∀ (i : Fin n), TM.Parked (initialWork i)) (houtput : out₀.HasBinaryPrefix emittedBits) : (binaryInstructionUpdateTM tapes op).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ BinaryInstructionUpdateResult tapes op store address lhs rhs initialWork work ∧ out.HasBinaryPrefix (emittedBits ++ List.flatMap Entry.encode (write store address (op.eval lhs rhs)))) (binaryInstructionUpdateTime tapes op store address lhs rhs)

Width-efficient arithmetic followed by a semantics-exact sparse write.

theorem Complexity.RAM.RegisterStore.Machine.binaryInstructionUpdateTM_retargetOutput_hoareTime_frame {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (store : Store) (address lhs rhs : ℕ) (emittedBits : List Bool) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (hcanonical : Canonical store) (hready : EntryScanReady tapes.update.entry (List.flatMap Entry.encode store) address.bits (fun (i : Fin n) => initialWork i.castSucc) fun (i : Fin n) => initialWork i.castSucc) (hlhs : (initialWork tapes.lhs.castSucc).HasBinaryNat lhs) (hrhs : (initialWork tapes.rhs.castSucc).HasBinaryNat rhs) (hresult : (initialWork tapes.update.replacement.castSucc).HasBinaryNat 0) (hshift : (initialWork tapes.shift.castSucc).HasBinaryNat 0) (htmp : (initialWork tapes.tmp.castSucc).HasBinaryNat 0) (hdbl : (initialWork tapes.dbl.castSucc).HasBinaryNat 0) (hremaining : (initialWork tapes.update.remaining.castSucc).HasBinaryNat (List.length store)) (hfound : (initialWork tapes.update.found.castSucc).HasBinaryNat 0) (hresultCount : (initialWork tapes.update.resultCount.castSucc).HasBinaryNat (List.length store)) (hinput : TM.Parked inp₀) (hwork : ∀ (i : Fin n), TM.Parked (initialWork i.castSucc)) (hbuffer : (initialWork (Fin.last n)).HasBinaryPrefix emittedBits) : (binaryInstructionUpdateTM tapes op).retargetOutput.HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ (BinaryInstructionUpdateResult tapes op store address lhs rhs (fun (i : Fin n) => initialWork i.castSucc) fun (i : Fin n) => work i.castSucc) ∧ (work (Fin.last n)).HasBinaryPrefix (emittedBits ++ List.flatMap Entry.encode (write store address (op.eval lhs rhs))) ∧ out = (Tape.init []).move Dir3.right) (binaryInstructionUpdateTime tapes op store address lhs rhs)

Redirect the updated encoded store into a fresh last work tape while the real output remains the standard blank parked tape.

theorem Complexity.RAM.RegisterStore.Machine.binaryInstructionUpdateTM_isTransducer {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) : (binaryInstructionUpdateTM tapes op).IsTransducer

Arithmetic and sparse update are both one-way-output machines.

theorem Complexity.RAM.RegisterStore.Machine.directBinaryInstructionTM_hoareTime_frame {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (store : Store) (destination source₀ source₁ : ℕ) (emittedBits : List Bool) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hcanonical : Canonical store) (hinitial : EntryLookupStaticReady tapes.lhsLookup store initialWork) (hrhs₀ : (initialWork tapes.rhs).HasBinaryNat 0) (hreplacement : (initialWork tapes.update.replacement).HasBinaryNat 0) (htmp : (initialWork tapes.tmp).HasBinaryNat 0) (hdbl : (initialWork tapes.dbl).HasBinaryNat 0) (hinput : TM.Parked inp₀) (houtput : out₀.HasBinaryPrefix emittedBits) : (directBinaryInstructionTM tapes op destination source₀ source₁).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ DirectBinaryInstructionResult tapes op store destination source₀ source₁ initialWork work ∧ out.HasBinaryPrefix (emittedBits ++ List.flatMap Entry.encode (write store destination (op.eval (read store source₀) (read store source₁))))) (directBinaryInstructionTime tapes op store destination source₀ source₁)

Two direct sparse-register reads, arithmetic, and the destination write realize one complete direct add, sub, or mul instruction.

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

Direct arithmetic instruction simulation never moves the output head left.

theorem Complexity.RAM.RegisterStore.Machine.directBinaryInstructionTM_prefix_withinAuxSpace {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (store : Store) (destination source₀ source₁ inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (directBinaryInstructionTM tapes op destination source₀ source₁).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (directBinaryInstructionTM tapes op destination source₀ source₁).reachesIn time start current) (htime : time ≤ directBinaryInstructionTime tapes op store destination source₀ source₁) : current.WithinAuxSpace inputLength (initialSpace + directBinaryInstructionTime tapes op store destination source₀ source₁)

Every prefix of a direct arithmetic instruction respects the coarse initial-space-plus-total-time auxiliary-space envelope.

theorem Complexity.RAM.RegisterStore.Machine.indirectLoadInstructionTM_hoareTime_frame {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (destination addressRegister : ℕ) (emittedBits : List Bool) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hcanonical : Canonical store) (hinitial : EntryLookupStaticReady tapes.lhsLookup store initialWork) (hreplacement : (initialWork tapes.update.replacement).HasBinaryNat 0) (hinput : TM.Parked inp₀) (houtput : out₀.HasBinaryPrefix emittedBits) : (indirectLoadInstructionTM tapes destination addressRegister).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ IndirectLoadInstructionResult tapes store destination addressRegister initialWork work ∧ out.HasBinaryPrefix (emittedBits ++ List.flatMap Entry.encode (write store destination (read store (read store addressRegister))))) (indirectLoadInstructionTime tapes store destination addressRegister)

A fixed-address lookup followed by a loaded runtime-address lookup and sparse update realizes one indirect load.

theorem Complexity.RAM.RegisterStore.Machine.indirectLoadInstructionTM_isTransducer {n : ℕ} (tapes : BinaryInstructionTapes n) (destination addressRegister : ℕ) : (indirectLoadInstructionTM tapes destination addressRegister).IsTransducer

Indirect-load simulation never moves the output head left.

theorem Complexity.RAM.RegisterStore.Machine.indirectLoadInstructionTM_prefix_withinAuxSpace {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (destination addressRegister inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (indirectLoadInstructionTM tapes destination addressRegister).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (indirectLoadInstructionTM tapes destination addressRegister).reachesIn time start current) (htime : time ≤ indirectLoadInstructionTime tapes store destination addressRegister) : current.WithinAuxSpace inputLength (initialSpace + indirectLoadInstructionTime tapes store destination addressRegister)

Every indirect-load prefix respects the coarse initial-space-plus-total-time auxiliary-space envelope.

theorem Complexity.RAM.RegisterStore.Machine.immediateInstructionTM_hoareTime_frame {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (destination value : ℕ) (emittedBits : List Bool) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hcanonical : Canonical store) (hinitial : EntryLookupStaticReady tapes.lhsLookup store initialWork) (hreplacement : (initialWork tapes.update.replacement).HasBinaryNat 0) (hinput : TM.Parked inp₀) (houtput : out₀.HasBinaryPrefix emittedBits) : (immediateInstructionTM tapes destination value).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ ImmediateInstructionResult tapes store destination value initialWork work ∧ out.HasBinaryPrefix (emittedBits ++ List.flatMap Entry.encode (write store destination value))) (immediateInstructionTime tapes store destination value)

Immediate-value and destination synthesis followed by sparse update realizes one imm instruction.

theorem Complexity.RAM.RegisterStore.Machine.immediateInstructionTM_isTransducer {n : ℕ} (tapes : BinaryInstructionTapes n) (destination value : ℕ) : (immediateInstructionTM tapes destination value).IsTransducer

Immediate-instruction simulation never moves the output head left.

theorem Complexity.RAM.RegisterStore.Machine.immediateInstructionTM_prefix_withinAuxSpace {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (destination value inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (immediateInstructionTM tapes destination value).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (immediateInstructionTM tapes destination value).reachesIn time start current) (htime : time ≤ immediateInstructionTime tapes store destination value) : current.WithinAuxSpace inputLength (initialSpace + immediateInstructionTime tapes store destination value)

Every immediate-instruction prefix respects the coarse initial-space-plus-total-time auxiliary-space envelope.

theorem Complexity.RAM.RegisterStore.Machine.indirectStoreInstructionTM_hoareTime_frame {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (addressRegister source : ℕ) (emittedBits : List Bool) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hcanonical : Canonical store) (hinitial : EntryLookupStaticReady tapes.lhsLookup store initialWork) (hrhs₀ : (initialWork tapes.rhs).HasBinaryNat 0) (hreplacement : (initialWork tapes.update.replacement).HasBinaryNat 0) (hinput : TM.Parked inp₀) (houtput : out₀.HasBinaryPrefix emittedBits) : (indirectStoreInstructionTM tapes addressRegister source).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ IndirectStoreInstructionResult tapes store addressRegister source initialWork work ∧ out.HasBinaryPrefix (emittedBits ++ List.flatMap Entry.encode (write store (read store addressRegister) (read store source)))) (indirectStoreInstructionTime tapes store addressRegister source)

Two direct lookups followed by framed binary copies into the update ABI realize one indirect store.

theorem Complexity.RAM.RegisterStore.Machine.indirectStoreInstructionTM_isTransducer {n : ℕ} (tapes : BinaryInstructionTapes n) (addressRegister source : ℕ) : (indirectStoreInstructionTM tapes addressRegister source).IsTransducer

Indirect-store simulation never moves the output head left.

theorem Complexity.RAM.RegisterStore.Machine.indirectStoreInstructionTM_prefix_withinAuxSpace {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (addressRegister source inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (indirectStoreInstructionTM tapes addressRegister source).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (indirectStoreInstructionTM tapes addressRegister source).reachesIn time start current) (htime : time ≤ indirectStoreInstructionTime tapes store addressRegister source) : current.WithinAuxSpace inputLength (initialSpace + indirectStoreInstructionTime tapes store addressRegister source)

Every indirect-store prefix respects the coarse initial-space-plus-total-time auxiliary-space envelope.

theorem Complexity.RAM.RegisterStore.Machine.setProgramCounterTM_hoareTime_frame {n : ℕ} (pc : Fin n) (pcValue target : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hpc : (work₀ pc).HasBinaryNat pcValue) (hinput : TM.Parked inp₀) (hwork : ∀ (i : Fin n), TM.Parked (work₀ i)) (houtput : TM.Parked out₀) : (setProgramCounterTM pc target).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = Function.update work₀ pc ((Tape.init (List.map Γ.ofBool target.bits)).move Dir3.right) ∧ out = out₀) (setProgramCounterTime pcValue target)

Reset and replace a canonical binary program counter by a fixed literal.

theorem Complexity.RAM.RegisterStore.Machine.zeroJumpInstructionTM_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue source target : ℕ) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hready : ControlInstructionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (zeroJumpInstructionTM tapes source target).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ ControlInstructionResult tapes store (if read store source = 0 then target else pcValue + 1) initialWork work ∧ out = out₀) (zeroJumpInstructionTime tapes store pcValue source target)

Conditional-zero control realizes sparse jz and restores its loaded operand to the clean lookup ABI.

theorem Complexity.RAM.RegisterStore.Machine.jumpInstructionTM_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue target : ℕ) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hready : ControlInstructionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (jumpInstructionTM tapes target).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ ControlInstructionResult tapes store target initialWork work ∧ out = out₀) (jumpInstructionTime pcValue target)

Unconditional control replaces the program counter by its jump target.

theorem Complexity.RAM.RegisterStore.Machine.haltInstructionTM_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue : ℕ) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hready : ControlInstructionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : haltInstructionTM.HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ ControlInstructionResult tapes store pcValue initialWork work ∧ out = out₀) haltInstructionTime

Halt is an exact no-op at the clean control boundary.

theorem Complexity.RAM.RegisterStore.Machine.setProgramCounterTM_isTransducer {n : ℕ} (pc : Fin n) (target : ℕ) : (setProgramCounterTM pc target).IsTransducer

Program-counter replacement never moves the output head left.

theorem Complexity.RAM.RegisterStore.Machine.zeroJumpInstructionTM_isTransducer {n : ℕ} (tapes : ControlInstructionTapes n) (source target : ℕ) : (zeroJumpInstructionTM tapes source target).IsTransducer

Conditional-zero control never moves the output head left.

theorem Complexity.RAM.RegisterStore.Machine.jumpInstructionTM_isTransducer {n : ℕ} (tapes : ControlInstructionTapes n) (target : ℕ) : (jumpInstructionTM tapes target).IsTransducer

Unconditional jump control never moves the output head left.

theorem Complexity.RAM.RegisterStore.Machine.haltInstructionTM_isTransducer {n : ℕ} : haltInstructionTM.IsTransducer

Halt control never moves the output head left.

theorem Complexity.RAM.RegisterStore.Machine.zeroJumpInstructionTM_prefix_withinAuxSpace {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue source target inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (zeroJumpInstructionTM tapes source target).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (zeroJumpInstructionTM tapes source target).reachesIn time start current) (htime : time ≤ zeroJumpInstructionTime tapes store pcValue source target) : current.WithinAuxSpace inputLength (initialSpace + zeroJumpInstructionTime tapes store pcValue source target)

Every conditional-zero prefix respects the coarse initial-space-plus-total-time auxiliary-space envelope.

theorem Complexity.RAM.RegisterStore.Machine.jumpInstructionTM_prefix_withinAuxSpace {n : ℕ} (tapes : ControlInstructionTapes n) (pcValue target inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (jumpInstructionTM tapes target).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (jumpInstructionTM tapes target).reachesIn time start current) (htime : time ≤ jumpInstructionTime pcValue target) : current.WithinAuxSpace inputLength (initialSpace + jumpInstructionTime pcValue target)

Every unconditional-jump prefix respects the coarse initial-space-plus-total-time auxiliary-space envelope.

theorem Complexity.RAM.RegisterStore.Machine.haltInstructionTM_prefix_withinAuxSpace {n : ℕ} (inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n haltInstructionTM.Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : haltInstructionTM.reachesIn time start current) (htime : time ≤ haltInstructionTime) : current.WithinAuxSpace inputLength (initialSpace + haltInstructionTime)

Every halt prefix respects its one-step auxiliary-space envelope.