Native selection of canonical signed keys

All arithmetic is unsigned. The sign bit and magnitude are decoded explicitly, the label is formed by addition or subtraction, and its two digits are computed with native shifts and remainders. The repeated-value case doubles the key and subtracts its original sign bit.

Main definitions

• Select.program: concrete selection and transformation instructions.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.magnitude : Fin 48

Magnitude bound, followed by two bit positions, selected digit and scan mode.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.beta : Fin 48

Magnitude bound, followed by two bit positions, selected digit and scan mode.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.beta' : Fin 48

Magnitude bound, followed by two bit positions, selected digit and scan mode.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.digit : Fin 48

Magnitude bound, followed by two bit positions, selected digit and scan mode.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.mode : Fin 48

Magnitude bound, followed by two bit positions, selected digit and scan mode.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.key : Fin 48

Input key; replaced by its selected output value.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.count : Fin 48

Full input multiplicity, read without truncation.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.zero : Fin 48

Small constants installed by the scan.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.one : Fin 48

Small constants installed by the scan.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.two : Fin 48

Small constants installed by the scan.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.three : Fin 48

Small constants installed by the scan.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.four : Fin 48

Small constants installed by the scan.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.five : Fin 48

Small constants installed by the scan.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.sign : Fin 48

Scratch registers for decoding and label digits.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.label : Fin 48

Scratch registers for decoding and label digits.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.bitA : Fin 48

Scratch registers for decoding and label digits.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.bitB : Fin 48

Scratch registers for decoding and label digits.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.take : Fin 48

Selection flag, either zero or one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.absolute : Fin 48

Magnitude temporary.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.labels : WordRAM.Code WordRAM.Basis.standard 48

Explicit native sign/magnitude decoding, shifted label and binary digit computation.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.skip : WordRAM.Code WordRAM.Basis.standard 48

A no-op used by unsuccessful selections.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.choose : WordRAM.Code WordRAM.Basis.standard 48

Select one of the six finite scan modes and perform the repeated-value transformation.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.program : WordRAM.Code WordRAM.Basis.standard 48

Every decoding, arithmetic, branch and selection instruction is part of this code.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.not_readsWidth : ¬program.ReadsWidth

This scalar program never reads the physical word width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.labels_preserves (j : Fin 48) (hj : ↑j ≤ 12) : WordRAM.Code.Preserves j labels

Registers below the decoding scratch are preserved by label calculation.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.preserves (j : Fin 48) (hj : ↑j ≤ 12 ∧ ↑j ≠ 5 ∨ 19 ≤ ↑j) : WordRAM.Code.Preserves j program

Selection preserves all caller parameters, constants and scan registers.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.labels_exec {w : ℕ} (x : WordRAM.Data 48) (hz : x.regs zero = 0) (h2 : x.regs two = 2) (hkey : WordRAM.Fits w (x.regs key)) (habs : x.regs key / 2 ≤ 2 * x.regs magnitude) (hfit : WordRAM.Fits w (4 * x.regs magnitude + 2)) : ∃ (y : WordRAM.Data 48), WordRAM.ExecWithin w labels x y 11 ∧ y.regs sign = x.regs key % 2 ∧ y.regs label = Math.label (x.regs magnitude) (x.regs key) ∧ y.regs bitA = Math.label (x.regs magnitude) (x.regs key) >>> x.regs beta % 2 ∧ y.regs bitB = Math.label (x.regs magnitude) (x.regs key) >>> x.regs beta' % 2 ∧ y.mem = x.mem

Decoding and both binary digits cost at most eleven native instructions.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.choose_exec {w : ℕ} (x : WordRAM.Data 48) (hz : x.regs zero = 0) (h1 : x.regs one = 1) (h2 : x.regs two = 2) (h3 : x.regs three = 3) (h4 : x.regs four = 4) (h5 : x.regs five = 5) (hs : x.regs sign = x.regs key % 2) (hfit : WordRAM.Fits w (2 * x.regs key)) (hsmall : WordRAM.Fits w 5) : ∃ (y : WordRAM.Data 48), WordRAM.ExecWithin w choose x y 20 ∧ y.regs take = (Math.flag (x.regs bitA) (x.regs bitB) (x.regs digit) (x.regs mode) (x.regs key, x.regs count)).toNat ∧ y.regs key = Math.value (x.regs mode) (x.regs key) ∧ y.mem = x.mem

Selection from already computed digits, with the full repeated-value count.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Select.exec {w : ℕ} (x : WordRAM.Data 48) (hz : x.regs zero = 0) (h1 : x.regs one = 1) (h2 : x.regs two = 2) (h3 : x.regs three = 3) (h4 : x.regs four = 4) (h5 : x.regs five = 5) (hkey : WordRAM.Fits w (x.regs key)) (habs : x.regs key / 2 ≤ 2 * x.regs magnitude) (hfit : WordRAM.Fits w (4 * x.regs magnitude + 2)) (hdouble : WordRAM.Fits w (2 * x.regs key)) (hsmall : WordRAM.Fits w 5) : ∃ (y : WordRAM.Data 48), WordRAM.ExecWithin w program x y 31 ∧ y.regs take = (Math.keep (x.regs magnitude) (x.regs beta) (x.regs beta') (x.regs digit) (x.regs mode) (x.regs key, x.regs count)).toNat ∧ y.regs key = Math.value (x.regs mode) (x.regs key) ∧ y.mem = x.mem

Complete native scalar selection. Its cost includes decoding, both label bits and doubling.