Checked constant-instruction most-significant-bit execution

The 44 virtual slots spell out the arithmetic in MSB.msb. Slot zero holds the input; the other 43 slots are constants or binary standard RAM operations. The checked compiler expands them into standard instructions at the original physical word width, using eighteen half-word digits per virtual value. Every virtual intermediate fits in 6w bits.

Main definitions

• MSB.Program.values: the mathematical value at each virtual slot.
• MSB.Program.ops: the source operations, with an unused placeholder at slot zero.
• MSB.Program.output, MSB.Program.zeroTest: physical registers for the final scalar answer and input-zero test.
• MSB.Program.positiveCode, MSB.Program.twoBitCode, MSB.Program.code, MSB.Program.finishCode: the compiled multiword graph, width-two fallback, and zero-dispatch wrappers.
• MSB.Program.scalarCode: composable register entry with charged workspace initialization.
• MSB.Program.program: a halting program for the ordinary singleton input encoding.

Main results

• MSB.Program.eval_ops: each executed operation computes its specified value.
• MSB.Program.ops_earlier: each operation reads only earlier slots.
• MSB.Program.values_output: the final slot contains the highest set-bit index.
• MSB.Program.exec_scalarCode: arbitrary-memory register entry for widths at least three.
• MSB.Program.executes_program: halting execution within 200001 instructions for w ≥ 2.

Code depends on the width through preprocessing constants, with uniformly bounded size and 836 physical registers. The scalar entry uses registers four and six for input and output; the remainder of its register workspace may change. Memory is preserved exactly. There is no uniform fixed-code preprocessing theorem or claim that the constants are generated at run time.

References

• Fredman and Willard, Surpassing the information theoretic bound with fusion trees.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.values (s x : ℕ) : Fin 44 → ℕ

The values of the 44 virtual slots. The two comparison/count stages use the named pure expressions from MSB, so their intermediate bounds remain reusable.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.ops (s : ℕ) : Fin 44 → WordRAM.Multiword.Circuit.Operation 44

Source operations in destination order. Slot zero is an unused placeholder: execution starts at slot one with the input already present in slot zero.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.eval_ops (s x : ℕ) (i : Fin 44) (hi : i ≠ 0) : WordRAM.Multiword.Circuit.Operation.eval (values s x) (ops s i) = values s x i

Every executed source node agrees with its pure arithmetic expression.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.ops_earlier (s : ℕ) (i : Fin 44) : WordRAM.Multiword.Circuit.Operation.Earlier i (ops s i)

All source operands precede their destination, including the unused constant placeholder at zero. Hence each executed destination is fresh.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.values_output {w x : ℕ} (hx0 : 0 < x) (hx : x < 2 ^ w) : values (clusterSize w) x 43 = x.log2

With the width-dependent cluster size, the final source value is the highest set-bit index. This is a source-graph result, without a RAM execution assertion.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.output : Fin (WordRAM.Multiword.Bank.capacity 44 + 4)

Physical register containing the final scalar answer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.zeroTest : Fin (WordRAM.Multiword.Bank.capacity 44 + 4)

A physical zero used for the input-zero branch.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.positiveCode (w : ℕ) : WordRAM.Code WordRAM.Basis.standard (WordRAM.Multiword.Bank.capacity 44 + 4)

The forty-three arithmetic nodes, followed by checked scalar reconstruction.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.twoBitCode : WordRAM.Code WordRAM.Basis.standard (WordRAM.Multiword.Bank.capacity 44 + 4)

Width two needs only division by two: its possible indices are zero and one.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.code (w : ℕ) : WordRAM.Code WordRAM.Basis.standard (WordRAM.Multiword.Bank.capacity 44 + 4)

The width-selected checked program. For larger widths the zero case returns zero and positive inputs execute the full graph. All constants and conversions are charged.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.size_code (w : ℕ) : (code w).size ≤ 200000

A fixed register count and a fixed code-size bound, shared by every physical width.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.exec_code {w z : ℕ} (hw : 2 ≤ w) (hz : z < 2 ^ w) : ∃ (y : WordRAM.Data (WordRAM.Multiword.Bank.capacity 44 + 4)), WordRAM.ExecWithin w (code w) (WordRAM.Data.init [z]) y 200000 ∧ y.regs output = z.log2 ∧ y.mem = (WordRAM.Data.init [z]).mem

The complete standard-basis program executes at the original physical width, from the ordinary singleton RAM input, within a constant instruction count independent of width. No preloaded wide constants, digit encodings, or MSB oracle are assumptions.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.finishCode (w : ℕ) : WordRAM.Code WordRAM.Basis.standard (WordRAM.Multiword.Bank.capacity 44 + 4)

Zero dispatch and positive arithmetic after the input bank entry has been established.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.scalarCode (w : ℕ) : WordRAM.Code WordRAM.Basis.standard (WordRAM.Multiword.Bank.capacity 44 + 4)

Register entry point for composition. The caller supplies its fitting input in physical register four. All 792 bank digits are cleared, the input is split in 44 instructions, and the same checked graph returns its answer in physical register six. No memory is read.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.size_scalarCode (w : ℕ) : (scalarCode w).size ≤ 200000

The scalar-entry MSB code has size at most 200000 at every word width.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.exec_scalarCode {w : ℕ} (hw : 3 ≤ w) (x : WordRAM.Data (WordRAM.Multiword.Bank.capacity 44 + 4)) (hz : WordRAM.Fits w (x.regs WordRAM.Multiword.Bank.inputReg)) : ∃ (y : WordRAM.Data (WordRAM.Multiword.Bank.capacity 44 + 4)), WordRAM.ExecWithin w (scalarCode w) x y 200000 ∧ y.regs output = (x.regs WordRAM.Multiword.Bank.inputReg).log2 ∧ y.mem = x.mem

Composable scalar-register execution. The entire incoming register file and memory may be arbitrary. Only the input register must fit. The routine preserves memory exactly and returns Nat.log2 in physical register six within 200000 instructions, including clearing. Registers inside this 836-register workspace may change; renamed embeddings frame all others.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.program (w : ℕ) : WordRAM.Program WordRAM.Basis.standard (WordRAM.Multiword.Bank.capacity 44 + 4)

The complete flat standard-basis program, with its final halt charged separately.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.length_program (w : ℕ) : List.length (program w) ≤ 200001

The assembled halting MSB program has at most 200001 instructions.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.executes_program {w z : ℕ} (hw : 2 ≤ w) (hz : z < 2 ^ w) : ∃ t ≤ 200001, WordRAM.Executes w (program w) (WordRAM.State.init [z]) z.log2 t

Actual halting execution returning the most-significant-set-bit index, with zero returning zero. The register count and the time bound are independent of physical width.