Documentation

Complexitylib.Models.RandomAccessMachine.Simulation.RegisterStore.Machine.Instruction.DenseCtrlSim

Dense-overlay control-instruction simulation #

source
theorem Complexity.RAM.RegisterStore.Machine.denseExecuteInstructionTM_jz_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (overlay : Store) (pcValue source target : ℕ) (initialWork : Fin (n + 1) → Tape) (hvalid : DenseOverlay.Valid overlay) (hready : InstructionExecutionReady tapes overlay pcValue initialWork) :
(denseExecuteInstructionTM tapes (Instr.jz source target)).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.jz source target) pcValue overlay work ∧ out = (Tape.init []).move Dir3.right) (denseExecuteInstructionTime tapes input (Instr.jz source target) pcValue overlay)

Dense conditional-zero execution preserves the overlay and exposes the generic buffered endpoint.

source
theorem Complexity.RAM.RegisterStore.Machine.denseExecuteInstructionTM_jmp_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (overlay : Store) (pcValue target : ℕ) (initialWork : Fin (n + 1) → Tape) (hready : InstructionExecutionReady tapes overlay pcValue initialWork) :
(denseExecuteInstructionTM tapes (Instr.jmp target)).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.jmp target) pcValue overlay work ∧ out = (Tape.init []).move Dir3.right) (denseExecuteInstructionTime tapes input (Instr.jmp target) pcValue overlay)

Dense unconditional-jump execution preserves the overlay and exposes the generic buffered endpoint.

source
theorem Complexity.RAM.RegisterStore.Machine.denseExecuteInstructionTM_halt_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (overlay : Store) (pcValue : ℕ) (initialWork : Fin (n + 1) → Tape) (hready : InstructionExecutionReady tapes overlay pcValue initialWork) :
(denseExecuteInstructionTM tapes Instr.halt).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.halt pcValue overlay work ∧ out = (Tape.init []).move Dir3.right) (denseExecuteInstructionTime tapes input Instr.halt pcValue overlay)

Dense halt execution preserves both the overlay and program counter and exposes the generic buffered endpoint.