Verified finite numeric switches for structured RAM programs #
The theorem in this module gives exact source step accounting and explicit logarithmic-cost and peak-space bounds for a finite numeric switch.
theorem
Complexity.RAM.Structured.Switch.select_exec
{count test one : ℕ}
(branch : Fin count → Cmd)
(initial final : Store)
{code branchSteps : ℕ}
(hcode : code < count)
(htest : initial test = code)
(hone : initial one = 1)
(hne : test ≠ one)
(hbranch : ∃ (cost : ℕ) (space : ℕ), Exec (branch ⟨code, hcode⟩) (cleared initial test) final branchSteps cost space)
:
A valid numeric code selects its corresponding branch, without requiring a resource envelope. This semantic form supports composition before a larger program chooses a shared cost and space bound.
theorem
Complexity.RAM.Structured.Switch.select_measured
{count test one indexBound valueBound : ℕ}
(branch : Fin count → Cmd)
(initial final : Store)
{code branchSteps branchCost : ℕ}
(hcode : code < count)
(htest : initial test = code)
(hone : initial one = 1)
(hne : test ≠ one)
(htestIndex : test < indexBound)
(hinitial : Internal.StoreEnvelope indexBound valueBound initial)
(hbranch :
Internal.MeasuredRuns (branch ⟨code, hcode⟩) (cleared initial test) final branchSteps branchCost
(Internal.envelopeSpace indexBound valueBound))
:
Internal.MeasuredRuns (select count test one branch) initial final (stepCount code branchSteps)
(costBound code branchCost (Internal.valueWidth valueBound)) (Internal.envelopeSpace indexBound valueBound)
A valid numeric code selects its corresponding branch. The selected branch starts with the test register cleared, matching the decrementing implementation. The result carries an exact transition count and envelope-based resource bounds.