Immediate sparse-store instructions -- proof internals

theorem Complexity.RAM.RegisterStore.Machine.immediateUpdate_ready_internal {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (destination value : ℕ) (initialWork : Fin n → Tape) (hinitial : EntryLookupStaticReady tapes.lhsLookup store initialWork) : have valueWork := Function.update initialWork tapes.update.replacement ((Tape.init (List.map Γ.ofBool value.bits)).move Dir3.right); have updateWork := Function.update valueWork tapes.update.entry.query ((Tape.init (List.map Γ.ofBool destination.bits)).move Dir3.right); EntryScanReady tapes.update.entry (List.flatMap Entry.encode store) destination.bits updateWork updateWork ∧ (updateWork tapes.update.replacement).HasBinaryNat value ∧ (updateWork tapes.update.remaining).HasBinaryNat (List.length store) ∧ (updateWork tapes.update.found).HasBinaryNat 0 ∧ (updateWork tapes.update.resultCount).HasBinaryNat (List.length store) ∧ ∀ (i : Fin n), TM.Parked (updateWork i)

theorem Complexity.RAM.RegisterStore.Machine.immediateInstructionTM_hoareTime_frame_internal {n : ℕ} (tapes : BinaryInstructionTapes n) (store : Store) (destination value : ℕ) (emittedBits : List Bool) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hcanonical : Canonical store) (hinitial : EntryLookupStaticReady tapes.lhsLookup store initialWork) (hreplacement : (initialWork tapes.update.replacement).HasBinaryNat 0) (hinput : TM.Parked inp₀) (houtput : out₀.HasBinaryPrefix emittedBits) : (immediateInstructionTM tapes destination value).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₀ ∧ ImmediateInstructionResult tapes store destination value initialWork work ∧ out.HasBinaryPrefix (emittedBits ++ List.flatMap Entry.encode (write store destination value))) (immediateInstructionTime tapes store destination value)

Exact semantic and time contract for one immediate sparse assignment.