Concrete sparse-store arithmetic instruction kernel -- proof internals #
theorem
Complexity.RAM.RegisterStore.Machine.binaryInstructionArithmeticTM_hoareTime_frame_internal
{n : ℕ}
(tapes : BinaryInstructionTapes n)
(op : BinaryInstrOp)
(lhs rhs : ℕ)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(hlhs : (work₀ tapes.lhs).HasBinaryNat lhs)
(hrhs : (work₀ tapes.rhs).HasBinaryNat rhs)
(hresult : (work₀ tapes.update.replacement).HasBinaryNat 0)
(hshift : (work₀ tapes.shift).HasBinaryNat 0)
(htmp : (work₀ tapes.tmp).HasBinaryNat 0)
(hdbl : (work₀ tapes.dbl).HasBinaryNat 0)
(hinput : TM.Parked inp₀)
(hwork : ∀ (i : Fin n), TM.Parked (work₀ i))
(houtput : TM.Parked out₀)
:
(binaryInstructionArithmeticTM tapes op).HoareTime
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀)
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) =>
inp = inp₀ ∧ BinaryInstructionArithmeticResult tapes op lhs rhs work₀ work ∧ out = out₀)
(binaryInstructionArithmeticTime op lhs rhs)
The selected width-efficient arithmetic phase has one uniform framed contract.
theorem
Complexity.RAM.RegisterStore.Machine.binaryInstructionUpdateTM_hoareTime_frame_internal
{n : ℕ}
(tapes : BinaryInstructionTapes n)
(op : BinaryInstrOp)
(store : Store)
(address lhs rhs : ℕ)
(emittedBits : List Bool)
(initialWork : Fin n → Tape)
(inp₀ out₀ : Tape)
(hcanonical : Canonical store)
(hready : EntryScanReady tapes.update.entry (List.flatMap Entry.encode store) 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 store))
(hfound : (initialWork tapes.update.found).HasBinaryNat 0)
(hresultCount : (initialWork tapes.update.resultCount).HasBinaryNat (List.length store))
(hinput : TM.Parked inp₀)
(hwork : ∀ (i : Fin n), TM.Parked (initialWork i))
(houtput : out₀.HasBinaryPrefix emittedBits)
:
(binaryInstructionUpdateTM 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₀ ∧ BinaryInstructionUpdateResult tapes op store address lhs rhs initialWork work ∧ out.HasBinaryPrefix (emittedBits ++ List.flatMap Entry.encode (write store address (op.eval lhs rhs))))
(binaryInstructionUpdateTime tapes op store address lhs rhs)
Arithmetic feeds its canonical result directly into sparse update.