Dense-overlay direct arithmetic instructions

theorem Complexity.RAM.RegisterStore.Machine.denseDirectBinaryOperands_hoareTime {n : ℕ} (tapes : BinaryInstructionTapes n) (input : List Bool) (overlay : Store) (source₀ source₁ : ℕ) (initialWork : Fin n → Tape) (out₀ : Tape) (hvalid : DenseOverlay.Valid overlay) (hinitial : EntryLookupStaticReady tapes.lhsLookup overlay initialWork) (hrhs₀ : (initialWork tapes.rhs).HasBinaryNat 0) (houtput : TM.Parked out₀) : ((denseOverlayLookupStaticTM tapes.lhsLookup source₀).seqTM (denseOverlayLookupStaticTM tapes.rhsLookup 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 ∧ DenseDirectBinaryOperandsResult tapes input overlay source₀ source₁ initialWork work ∧ out = out₀) (denseOverlayLookupStaticTime tapes.lhsLookup input.length overlay source₀ + 1 + denseOverlayLookupStaticTime tapes.rhsLookup input.length overlay source₁)

Two fixed dense-overlay reads compose while retaining the shared scanner ABI and the immutable input tape.

theorem Complexity.RAM.RegisterStore.Machine.denseBinaryInstructionUpdateTM_hoareTime_frame {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (overlay : Store) (address lhs rhs : ℕ) (emittedBits : List Bool) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hcanonical : Canonical overlay) (hready : EntryScanReady tapes.update.entry (List.flatMap Entry.encode overlay) address.bits initialWork initialWork) (hlhs : (initialWork tapes.lhs).HasBinaryNat lhs) (hrhs : (initialWork tapes.rhs).HasBinaryNat rhs) (hresult : (initialWork tapes.update.replacement).HasBinaryNat 0) (hshift : (initialWork tapes.shift).HasBinaryNat 0) (htmp : (initialWork tapes.tmp).HasBinaryNat 0) (hdbl : (initialWork tapes.dbl).HasBinaryNat 0) (hremaining : (initialWork tapes.update.remaining).HasBinaryNat (List.length overlay)) (hfound : (initialWork tapes.update.found).HasBinaryNat 0) (hresultCount : (initialWork tapes.update.resultCount).HasBinaryNat (List.length overlay)) (hinput : TM.Parked inp₀) (hwork : ∀ (i : Fin n), TM.Parked (initialWork i)) (houtput : out₀.HasBinaryPrefix emittedBits) : (denseBinaryInstructionUpdateTM tapes op).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ DenseBinaryInstructionUpdateResult tapes op overlay address lhs rhs initialWork work ∧ out.HasBinaryPrefix (emittedBits ++ List.flatMap Entry.encode (DenseOverlay.write overlay address (op.eval lhs rhs)))) (denseBinaryInstructionUpdateTime tapes op overlay address lhs rhs)

Arithmetic feeds its canonical result through successor tagging and into the sparse overlay update controller.

theorem Complexity.RAM.RegisterStore.Machine.denseDirectBinaryInstructionTM_hoareTime_frame {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (input : List Bool) (overlay : Store) (destination source₀ 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) (htmp : (initialWork tapes.tmp).HasBinaryNat 0) (hdbl : (initialWork tapes.dbl).HasBinaryNat 0) (houtput : out₀.HasBinaryPrefix emittedBits) : (denseDirectBinaryInstructionTM tapes op destination source₀ 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 ∧ DenseDirectBinaryInstructionResult tapes op input overlay destination source₀ source₁ initialWork work ∧ out.HasBinaryPrefix (emittedBits ++ List.flatMap Entry.encode (DenseOverlay.write overlay destination (op.eval (DenseOverlay.read input overlay source₀) (DenseOverlay.read input overlay source₁))))) (denseDirectBinaryInstructionTime tapes op input overlay destination source₀ source₁)

Two dense reads, direct destination synthesis, arithmetic, successor tagging, and sparse update implement one RAM arithmetic instruction.