Uniform next-store buffering for data instructions

theorem Complexity.RAM.RegisterStore.Machine.instructionExecutionReady_baseLookup_internal {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue : ℕ) (work : Fin (n + 1) → Tape) (hready : InstructionExecutionReady tapes store pcValue work) : EntryLookupStaticReady tapes.data.lhsLookup store fun (i : Fin n) => work i.castSucc

Restrict the lifted clean lookup ABI to the original data-tape family.

theorem Complexity.RAM.RegisterStore.Machine.finishBufferedDataTM_hoareTime_frame_internal {n : ℕ} (tapes : ControlInstructionTapes n) (oldStore nextStore : Store) (nextPC pcValue : ℕ) (cleanupValues : Fin 5 → ℕ) (remainingValue : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (dataTM : TM n) (dataTime : ℕ) (hpcNext : nextPC = pcValue + 1) (hinput : TM.Parked inp₀) (hdata : dataTM.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₀ ∧ (work tapes.buffer).HasBinaryPrefix (List.flatMap Entry.encode nextStore) ∧ (work tapes.liftedPC).HasBinaryNat pcValue ∧ (work tapes.lifted.data.update.resultCount).HasBinaryNat (List.length nextStore) ∧ (work tapes.liftedSource).HasBinaryContent (List.flatMap Entry.encode oldStore) ∧ (∀ (slot : Fin 5), (work (instructionCleanupTape tapes slot)).HasBinaryNat (cleanupValues slot)) ∧ (work tapes.lifted.data.update.remaining).HasBinaryNat remainingValue ∧ EntryScanReady tapes.lifted.data.update.entry [] (cleanupValues 0).bits work work ∧ (work tapes.lifted.data.shift).HasBinaryNat 0 ∧ (work tapes.lifted.data.tmp).HasBinaryNat 0 ∧ (work tapes.lifted.data.dbl).HasBinaryNat 0 ∧ (∀ (i : Fin (n + 1)), TM.Parked (work i)) ∧ out = (Tape.init []).move Dir3.right) dataTime) : (dataTM.retargetOutput.seqTM (TM.binarySuccTM tapes.liftedPC)).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₀ ∧ BufferedInstructionResult tapes oldStore nextStore nextPC cleanupValues remainingValue work ∧ out = (Tape.init []).move Dir3.right) (dataTime + 1 + TM.binarySuccTime pcValue)

Increment the PC after a redirected data kernel satisfying the common pre-successor boundary.

theorem Complexity.RAM.RegisterStore.Machine.retargetBufferedDataKernel_hoareTime_frame_internal {n : ℕ} (tapes : ControlInstructionTapes n) (oldStore nextStore : Store) (cleanupValues : Fin 5 → ℕ) (remainingValue pcValue : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (dataTM : TM n) (dataTime : ℕ) (Result : (Fin n → Tape) → Prop) (hready : InstructionExecutionReady tapes oldStore pcValue initialWork) (hbase : dataTM.HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ (work = fun (i : Fin n) => initialWork i.castSucc) ∧ out = initialWork tapes.buffer) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ Result work ∧ out.HasBinaryPrefix (List.flatMap Entry.encode nextStore)) dataTime) (hresult : ∀ (work : Fin n → Tape), Result work → work tapes.pc = initialWork tapes.pc.castSucc ∧ (work tapes.data.update.resultCount).HasBinaryNat (List.length nextStore) ∧ (work tapes.data.update.entry.source).HasBinaryContent (List.flatMap Entry.encode oldStore) ∧ (∀ (slot : Fin 5), (work (tapes.data.idx (instructionCleanupParentSlot slot))).HasBinaryNat (cleanupValues slot)) ∧ (work tapes.data.update.remaining).HasBinaryNat remainingValue ∧ EntryScanReady tapes.data.update.entry [] (cleanupValues 0).bits work work ∧ (work tapes.data.shift).HasBinaryNat 0 ∧ (work tapes.data.tmp).HasBinaryNat 0 ∧ (work tapes.data.dbl).HasBinaryNat 0 ∧ ∀ (i : Fin n), TM.Parked (work i)) : dataTM.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₀ ∧ (work tapes.buffer).HasBinaryPrefix (List.flatMap Entry.encode nextStore) ∧ (work tapes.liftedPC).HasBinaryNat pcValue ∧ (work tapes.lifted.data.update.resultCount).HasBinaryNat (List.length nextStore) ∧ (work tapes.liftedSource).HasBinaryContent (List.flatMap Entry.encode oldStore) ∧ (∀ (slot : Fin 5), (work (instructionCleanupTape tapes slot)).HasBinaryNat (cleanupValues slot)) ∧ (work tapes.lifted.data.update.remaining).HasBinaryNat remainingValue ∧ EntryScanReady tapes.lifted.data.update.entry [] (cleanupValues 0).bits work work ∧ (work tapes.lifted.data.shift).HasBinaryNat 0 ∧ (work tapes.lifted.data.tmp).HasBinaryNat 0 ∧ (work tapes.lifted.data.dbl).HasBinaryNat 0 ∧ (∀ (i : Fin (n + 1)), TM.Parked (work i)) ∧ out = (Tape.init []).move Dir3.right) dataTime

Lift a base data-kernel contract through output redirection once its semantic result exposes PC framing, the next-store count, and parked heads.

def Complexity.RAM.RegisterStore.Machine.directInstruction (op : BinaryInstrOp) (destination source₀ source₁ : ℕ) : Instr

Instruction constructor corresponding to a direct arithmetic kernel.

Equations

• Complexity.RAM.RegisterStore.Machine.directInstruction Complexity.RAM.RegisterStore.Machine.BinaryInstrOp.add destination source₀ source₁ = Complexity.RAM.Instr.add destination source₀ source₁
• Complexity.RAM.RegisterStore.Machine.directInstruction Complexity.RAM.RegisterStore.Machine.BinaryInstrOp.sub destination source₀ source₁ = Complexity.RAM.Instr.sub destination source₀ source₁
• Complexity.RAM.RegisterStore.Machine.directInstruction Complexity.RAM.RegisterStore.Machine.BinaryInstrOp.mul destination source₀ source₁ = Complexity.RAM.Instr.mul destination source₀ source₁

theorem Complexity.RAM.RegisterStore.Machine.executeInstructionTM_imm_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue destination value : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (hready : InstructionExecutionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) : (executeInstructionTM tapes (Instr.imm destination value)).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₀ ∧ InstructionExecutionResult tapes (Instr.imm destination value) pcValue store work ∧ out = (Tape.init []).move Dir3.right) (executeInstructionTime tapes (Instr.imm destination value) pcValue store)

Immediate execution redirects the new sparse store and increments the program counter.

theorem Complexity.RAM.RegisterStore.Machine.executeInstructionTM_direct_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (op : BinaryInstrOp) (store : Store) (pcValue destination source₀ source₁ : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (hready : InstructionExecutionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) : (executeInstructionTM tapes (directInstruction op destination source₀ source₁)).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₀ ∧ InstructionExecutionResult tapes (directInstruction op destination source₀ source₁) pcValue store work ∧ out = (Tape.init []).move Dir3.right) (executeInstructionTime tapes (directInstruction op destination source₀ source₁) pcValue store)

A direct arithmetic kernel redirects its next sparse store and increments the program counter.

theorem Complexity.RAM.RegisterStore.Machine.executeInstructionTM_add_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue destination source₀ source₁ : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (hready : InstructionExecutionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) : (executeInstructionTM tapes (Instr.add destination source₀ source₁)).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₀ ∧ InstructionExecutionResult tapes (Instr.add destination source₀ source₁) pcValue store work ∧ out = (Tape.init []).move Dir3.right) (executeInstructionTime tapes (Instr.add destination source₀ source₁) pcValue store)

Direct addition has the common one-buffer instruction contract.

theorem Complexity.RAM.RegisterStore.Machine.executeInstructionTM_sub_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue destination source₀ source₁ : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (hready : InstructionExecutionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) : (executeInstructionTM tapes (Instr.sub destination source₀ source₁)).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₀ ∧ InstructionExecutionResult tapes (Instr.sub destination source₀ source₁) pcValue store work ∧ out = (Tape.init []).move Dir3.right) (executeInstructionTime tapes (Instr.sub destination source₀ source₁) pcValue store)

Direct subtraction has the common one-buffer instruction contract.

theorem Complexity.RAM.RegisterStore.Machine.executeInstructionTM_mul_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue destination source₀ source₁ : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (hready : InstructionExecutionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) : (executeInstructionTM tapes (Instr.mul destination source₀ source₁)).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₀ ∧ InstructionExecutionResult tapes (Instr.mul destination source₀ source₁) pcValue store work ∧ out = (Tape.init []).move Dir3.right) (executeInstructionTime tapes (Instr.mul destination source₀ source₁) pcValue store)

Direct multiplication has the common one-buffer instruction contract.

theorem Complexity.RAM.RegisterStore.Machine.executeInstructionTM_load_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue destination addressRegister : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (hready : InstructionExecutionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) : (executeInstructionTM tapes (Instr.load destination addressRegister)).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₀ ∧ InstructionExecutionResult tapes (Instr.load destination addressRegister) pcValue store work ∧ out = (Tape.init []).move Dir3.right) (executeInstructionTime tapes (Instr.load destination addressRegister) pcValue store)

Indirect-load execution redirects its next sparse store and increments the program counter.

theorem Complexity.RAM.RegisterStore.Machine.executeInstructionTM_store_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue addressRegister source : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (hready : InstructionExecutionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) : (executeInstructionTM tapes (Instr.store addressRegister source)).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₀ ∧ InstructionExecutionResult tapes (Instr.store addressRegister source) pcValue store work ∧ out = (Tape.init []).move Dir3.right) (executeInstructionTime tapes (Instr.store addressRegister source) pcValue store)

Indirect-store execution redirects its next sparse store and increments the program counter.