Actual ordinary-host metadata controls

The controller copies the existing preprocessing registers, computes its polynomial reservation, and retains its metadata while native callees execute in disjoint banks.

Main definitions

• Controls: raw table/count/packed-length and caller-owned workspace register contents.

Main results

• exec_setup: all ten metadata/constant instructions.

These metadata composition proofs are original.

structure Cslib.Algorithms.WordRAM.ThreeSum.Decision.Controls {r : ℕ} (tab num N V : ℕ) (x : WordRAM.Data (registerCount r)) : Prop

The raw runtime controls for an entire catalogue traversal.

• table : x.regs (controllerRegisters r Decision.table) = tab
• count : x.regs (controllerRegisters r Decision.count) = num
• length : x.regs (controllerRegisters r Decision.length) = N
• envelope : x.regs (controllerRegisters r Decision.envelope) = V
• workspace : x.regs (controllerRegisters r Decision.workspace) = 2 * V
• one : x.regs (controllerRegisters r Decision.one) = 1

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.Controls.congr {r tab num N V : ℕ} {x y : WordRAM.Data (registerCount r)} (h : Controls tab num N V x) (heq : ∀ (i : Fin 16), i ≠ current → i ≠ answer → i ≠ address → i ≠ source → y.regs (controllerRegisters r i) = x.regs (controllerRegisters r i)) : Controls tab num N V y

Controls depend only on their six exact register values.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.exec_setup {r κ n w tab num N : ℕ} (x : WordRAM.Data (registerCount r)) (hn : x.regs (controllerRegisters r inputLength) = n) (ht : x.regs (preprocessingRegisters r ChanHe.Traversal.outputs) = tab) (hc : x.regs (preprocessingRegisters r ChanHe.Traversal.outputCount) = num) (hl : x.regs (preprocessingRegisters r ChanHe.Preprocessing.packedLength) = N) (hb : WordRAM.Fits w (n + 2)) (hE : WordRAM.Fits w (envelopeExponent κ)) : ∃ (y : WordRAM.Data (registerCount r)), WordRAM.ExecWithin w (setup κ) x y 11 ∧ y.regs (controllerRegisters r table) = tab ∧ y.regs (controllerRegisters r count) = num ∧ y.regs (controllerRegisters r length) = N ∧ y.regs (controllerRegisters r scale) = n + 2 ∧ y.regs (controllerRegisters r envelope) = 1 ∧ y.regs (controllerRegisters r remaining) = envelopeExponent κ ∧ y.regs (controllerRegisters r current) = 0 ∧ y.regs (controllerRegisters r one) = 1 ∧ y.regs (controllerRegisters r zero) = 0 ∧ y.regs (controllerRegisters r answer) = x.regs (controllerRegisters r answer) ∧ y.mem = x.mem

Copy the actual unsigned output ABI; no mathematical layout supplies runtime pointers.