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.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.values_input (s x : ℕ) : values s x 0 = x

Slot zero is the supplied input.

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_msb (s x : ℕ) (hx : 0 < x) : values s x 43 = msb s x

On nonzero inputs, the last slot is exactly the arithmetic expression msb.

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.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.values_mem (s x : ℕ) (i : Fin 44) : values s x i ∈ clusterStageValues s x ∨ values s x i ∈ powerStageValues s (clusterSummary s x) ∨ values s x i ∈ powerStageValues s (x >>> (smallMSB s (clusterSummary s x) * s) &&& 2 ^ s - 1) ∨ values s x i = 1 ∨ values s x i = smallMSB s (clusterSummary s x) * s ∨ values s x i = x >>> (smallMSB s (clusterSummary s x) * s) ∨ values s x i = values s x 43

Each virtual value occurs in an audited stage list, apart from the unit constant, the selected-cluster offset, the unmasked selected input, and the final output.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.values_lt {w x : ℕ} (hw : 0 < w) (hx0 : 0 < x) (hx : x < 2 ^ w) (i : Fin 44) : values (clusterSize w) x i < 2 ^ (6 * w)

All 44 virtual values fit in the audited 6w virtual bits.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.clusterSize_lt {w : ℕ} (hw : 3 ≤ w) : clusterSize w < w

At widths at least three, the precomputed cluster size is strictly smaller than the physical width.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.twice_width_lt {w : ℕ} (hw : 3 ≤ w) : 2 * w < 2 ^ w

Twice the physical width itself fits in a physical word at widths at least three.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.guarded_fits {w z : ℕ} (hw : 3 ≤ w) (hz : z < 2 ^ clusterSize w) : WordRAM.Fits w (2 ^ clusterSize w) ∧ WordRAM.Fits w z ∧ WordRAM.Fits w (2 ^ clusterSize w + z)

The two guarded comparison inputs and their sums fit in physical words.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.shift_amounts_fit {w x : ℕ} (hw : 3 ≤ w) : WordRAM.Fits w (clusterSize w * clusterSize w) ∧ WordRAM.Fits w (clusterSize w) ∧ WordRAM.Fits w ((clusterSize w - 1) * (clusterSize w + 1)) ∧ WordRAM.Fits w (smallMSB (clusterSize w) (clusterSummary (clusterSize w) x) * clusterSize w)

Every shift count used by the source graph fits in one physical word.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.output_add_fits {w x : ℕ} (hx0 : 0 < x) (hx : x < 2 ^ w) : have s := clusterSize w; have c := smallMSB s (clusterSummary s x); have v := x >>> (c * s) &&& 2 ^ s - 1; WordRAM.Fits w (c * s) ∧ WordRAM.Fits w (smallMSB s v) ∧ WordRAM.Fits w (c * s + smallMSB s v)

The final addition has fitting operands and result.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.ops_admissible {w x : ℕ} (hw : 3 ≤ w) (hx0 : 0 < x) (hx : x < 2 ^ w) (i : Fin 44) (hi : i ≠ 0) : WordRAM.Multiword.Circuit.Operation.Admissible w (values (clusterSize w) x) (ops (clusterSize w) i)

Every executed node satisfies the concrete multiword compiler's admissibility contract. Only the additions and shift counts require physical-word bounds.

@[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.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.size_positiveCode (w : ℕ) : (positiveCode w).size ≤ 172045

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.Program.exec_positiveCode {w z : ℕ} (hw : 3 ≤ w) (hz0 : 0 < z) (hz : z < 2 ^ w) (x : WordRAM.Data (WordRAM.Multiword.Bank.capacity 44 + 4)) (hx : WordRAM.Multiword.Bank.Encodes w x (WordRAM.Multiword.Circuit.prefix (values (clusterSize w) z) 1)) : ∃ (y : WordRAM.Data (WordRAM.Multiword.Bank.capacity 44 + 4)), WordRAM.ExecWithin w (positiveCode w) x y 172045 ∧ y.regs output = z.log2 ∧ y.mem = x.mem

Execution of the actual expanded graph on a positive input. Every virtual operation is discharged by Circuit.exec_emit, which uses the checked single-word routines.

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

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

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.