Compilation theorem for finite numeric structured-RAM switches

theorem Complexity.RAM.Structured.Switch.select_compiled {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)) : ∃ (cost : ℕ) (space : ℕ), Exec (select count test one branch) initial final (stepCount code branchSteps) cost space ∧ run (select count test one branch).compile (stepCount code branchSteps) { pc := 0, regs := initial } = { pc := (select count test one branch).codeSize, regs := final } ∧ Halted (select count test one branch).compile (run (select count test one branch).compile (stepCount code branchSteps) { pc := 0, regs := initial }) ∧ logTimeUpto (select count test one branch).compile (stepCount code branchSteps) { pc := 0, regs := initial } ≤ costBound code branchCost (Internal.valueWidth valueBound) ∧ spaceUpto (select count test one branch).compile (stepCount code branchSteps) { pc := 0, regs := initial } ≤ Internal.envelopeSpace indexBound valueBound

End-to-end compilation of a measured finite switch.