Dense-overlay data-instruction simulation

theorem Complexity.RAM.RegisterStore.Machine.denseExecuteInstructionTM_imm_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (overlay : Store) (pcValue destination value : ℕ) (initialWork : Fin (n + 1) → Tape) (hvalid : DenseOverlay.Valid overlay) (hready : InstructionExecutionReady tapes overlay pcValue initialWork) : (denseExecuteInstructionTM tapes (Instr.imm destination value)).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ DenseInstructionExecutionResult tapes input (Instr.imm destination value) pcValue overlay work ∧ out = (Tape.init []).move Dir3.right) (denseExecuteInstructionTime tapes input (Instr.imm destination value) pcValue overlay)

A dense immediate write produces the generic buffered endpoint and advances the program counter.

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

Instruction constructor corresponding to a dense direct arithmetic kernel.

Equations

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

theorem Complexity.RAM.RegisterStore.Machine.denseExecuteInstructionTM_direct_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (op : BinaryInstrOp) (input : List Bool) (overlay : Store) (pcValue destination source₀ source₁ : ℕ) (initialWork : Fin (n + 1) → Tape) (hvalid : DenseOverlay.Valid overlay) (hready : InstructionExecutionReady tapes overlay pcValue initialWork) : (denseExecuteInstructionTM tapes (denseDirectInstruction op destination source₀ source₁)).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ DenseInstructionExecutionResult tapes input (denseDirectInstruction op destination source₀ source₁) pcValue overlay work ∧ out = (Tape.init []).move Dir3.right) (denseExecuteInstructionTime tapes input (denseDirectInstruction op destination source₀ source₁) pcValue overlay)

A dense direct arithmetic instruction produces the generic buffered endpoint and advances the program counter.

theorem Complexity.RAM.RegisterStore.Machine.denseExecuteInstructionTM_add_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (overlay : Store) (pcValue destination source₀ source₁ : ℕ) (initialWork : Fin (n + 1) → Tape) (hvalid : DenseOverlay.Valid overlay) (hready : InstructionExecutionReady tapes overlay pcValue initialWork) : (denseExecuteInstructionTM tapes (Instr.add destination source₀ source₁)).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ DenseInstructionExecutionResult tapes input (Instr.add destination source₀ source₁) pcValue overlay work ∧ out = (Tape.init []).move Dir3.right) (denseExecuteInstructionTime tapes input (Instr.add destination source₀ source₁) pcValue overlay)

Dense direct addition has the common buffered instruction contract.

theorem Complexity.RAM.RegisterStore.Machine.denseExecuteInstructionTM_sub_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (overlay : Store) (pcValue destination source₀ source₁ : ℕ) (initialWork : Fin (n + 1) → Tape) (hvalid : DenseOverlay.Valid overlay) (hready : InstructionExecutionReady tapes overlay pcValue initialWork) : (denseExecuteInstructionTM tapes (Instr.sub destination source₀ source₁)).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ DenseInstructionExecutionResult tapes input (Instr.sub destination source₀ source₁) pcValue overlay work ∧ out = (Tape.init []).move Dir3.right) (denseExecuteInstructionTime tapes input (Instr.sub destination source₀ source₁) pcValue overlay)

Dense direct subtraction has the common buffered instruction contract.

theorem Complexity.RAM.RegisterStore.Machine.denseExecuteInstructionTM_mul_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (overlay : Store) (pcValue destination source₀ source₁ : ℕ) (initialWork : Fin (n + 1) → Tape) (hvalid : DenseOverlay.Valid overlay) (hready : InstructionExecutionReady tapes overlay pcValue initialWork) : (denseExecuteInstructionTM tapes (Instr.mul destination source₀ source₁)).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ DenseInstructionExecutionResult tapes input (Instr.mul destination source₀ source₁) pcValue overlay work ∧ out = (Tape.init []).move Dir3.right) (denseExecuteInstructionTime tapes input (Instr.mul destination source₀ source₁) pcValue overlay)

Dense direct multiplication has the common buffered instruction contract.

theorem Complexity.RAM.RegisterStore.Machine.denseExecuteInstructionTM_load_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (overlay : Store) (pcValue destination addressRegister : ℕ) (initialWork : Fin (n + 1) → Tape) (hvalid : DenseOverlay.Valid overlay) (hready : InstructionExecutionReady tapes overlay pcValue initialWork) : (denseExecuteInstructionTM tapes (Instr.load destination addressRegister)).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ DenseInstructionExecutionResult tapes input (Instr.load destination addressRegister) pcValue overlay work ∧ out = (Tape.init []).move Dir3.right) (denseExecuteInstructionTime tapes input (Instr.load destination addressRegister) pcValue overlay)

A dense indirect load produces the generic buffered endpoint and advances the program counter.

theorem Complexity.RAM.RegisterStore.Machine.denseExecuteInstructionTM_store_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (overlay : Store) (pcValue addressRegister source : ℕ) (initialWork : Fin (n + 1) → Tape) (hvalid : DenseOverlay.Valid overlay) (hready : InstructionExecutionReady tapes overlay pcValue initialWork) : (denseExecuteInstructionTM tapes (Instr.store addressRegister source)).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ DenseInstructionExecutionResult tapes input (Instr.store addressRegister source) pcValue overlay work ∧ out = (Tape.init []).move Dir3.right) (denseExecuteInstructionTime tapes input (Instr.store addressRegister source) pcValue overlay)

A dense indirect store produces the generic buffered endpoint and advances the program counter.