Dense-overlay instruction simulation

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

Every statically selected RAM instruction realizes the common dense buffered snapshot-step contract.