Dense-overlay indirect store

theorem Complexity.RAM.RegisterStore.Machine.denseIndirectStoreInstructionTM_hoareTime_frame {n : ℕ} (tapes : BinaryInstructionTapes n) (input : List Bool) (overlay : Store) (addressRegister source : ℕ) (emittedBits : List Bool) (initialWork : Fin n → Tape) (out₀ : Tape) (hvalid : DenseOverlay.Valid overlay) (hinitial : EntryLookupStaticReady tapes.lhsLookup overlay initialWork) (hrhs₀ : (initialWork tapes.rhs).HasBinaryNat 0) (hreplacement : (initialWork tapes.update.replacement).HasBinaryNat 0) (houtput : out₀.HasBinaryPrefix emittedBits) : (denseIndirectStoreInstructionTM tapes addressRegister source).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ DenseIndirectStoreInstructionResult tapes input overlay addressRegister source initialWork work ∧ out.HasBinaryPrefix (emittedBits ++ List.flatMap Entry.encode (DenseOverlay.write overlay (DenseOverlay.read input overlay addressRegister) (DenseOverlay.read input overlay source)))) (denseIndirectStoreInstructionTime tapes input overlay addressRegister source)

Exact semantic and time contract for one dense-overlay indirect store.