Direct sparse-store arithmetic instructions -- proof internals #
theorem
Complexity.RAM.RegisterStore.Machine.scanner_rhs_of_lhs_internal
{n : ℕ}
(tapes : BinaryInstructionTapes n)
(store : Store)
(source : ℕ)
(initialWork finalWork : Fin n → Tape)
(hlookup : EntryLookupStaticResult tapes.lhsLookup store source initialWork finalWork)
:
EntryScanReady tapes.rhsLookup.scan.entry (List.flatMap Entry.encode store) [] finalWork finalWork
theorem
Complexity.RAM.RegisterStore.Machine.rhsReady_of_lhs_internal
{n : ℕ}
(tapes : BinaryInstructionTapes n)
(store : Store)
(source : ℕ)
(initialWork finalWork : Fin n → Tape)
(hinitial : EntryLookupStaticReady tapes.lhsLookup store initialWork)
(hrhs : (initialWork tapes.rhs).HasBinaryNat 0)
(hlookup : EntryLookupStaticResult tapes.lhsLookup store source initialWork finalWork)
:
EntryLookupStaticReady tapes.rhsLookup store finalWork
theorem
Complexity.RAM.RegisterStore.Machine.scanner_updateQuery_internal
{n : ℕ}
(tapes : BinaryInstructionTapes n)
(store : Store)
(destination : ℕ)
(work : Fin n → Tape)
(hscanner : EntryScanReady tapes.rhsLookup.scan.entry (List.flatMap Entry.encode store) [] work work)
:
EntryScanReady tapes.update.entry (List.flatMap Entry.encode store) destination.bits
(Function.update work tapes.update.entry.query ((Tape.init (List.map Γ.ofBool destination.bits)).move Dir3.right))
(Function.update work tapes.update.entry.query ((Tape.init (List.map Γ.ofBool destination.bits)).move Dir3.right))
theorem
Complexity.RAM.RegisterStore.Machine.directBinaryOperands_hoareTime_internal
{n : ℕ}
(tapes : BinaryInstructionTapes n)
(store : Store)
(source₀ source₁ : ℕ)
(initialWork : Fin n → Tape)
(inp₀ out₀ : Tape)
(hinitial : EntryLookupStaticReady tapes.lhsLookup store initialWork)
(hrhs₀ : (initialWork tapes.rhs).HasBinaryNat 0)
(hinput : TM.Parked inp₀)
(houtput : TM.Parked out₀)
:
((entryLookupStaticTM tapes.lhsLookup source₀).seqTM (entryLookupStaticTM tapes.rhsLookup source₁)).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₀ ∧ DirectBinaryOperandsResult tapes store source₀ source₁ initialWork work ∧ out = out₀)
(entryLookupStaticTime tapes.lhsLookup store source₀ + 1 + entryLookupStaticTime tapes.rhsLookup store source₁)
The shared two-direct-operand prefix used by arithmetic and indirect store instructions.
theorem
Complexity.RAM.RegisterStore.Machine.directBinaryInstructionTM_hoareTime_frame_internal
{n : ℕ}
(tapes : BinaryInstructionTapes n)
(op : BinaryInstrOp)
(store : Store)
(destination source₀ source₁ : ℕ)
(emittedBits : List Bool)
(initialWork : Fin n → Tape)
(inp₀ out₀ : Tape)
(hcanonical : Canonical store)
(hinitial : EntryLookupStaticReady tapes.lhsLookup store 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)
(hinput : TM.Parked inp₀)
(houtput : out₀.HasBinaryPrefix emittedBits)
:
(directBinaryInstructionTM tapes op destination source₀ source₁).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₀ ∧ DirectBinaryInstructionResult tapes op store destination source₀ source₁ initialWork work ∧ out.HasBinaryPrefix
(emittedBits ++ List.flatMap Entry.encode (write store destination (op.eval (read store source₀) (read store source₁)))))
(directBinaryInstructionTime tapes op store destination source₀ source₁)
Two fixed sparse reads, direct destination synthesis, width-efficient arithmetic, and sparse update compose to the pure direct RAM operation.