Checked limbwise Boolean operations

Little-endian half-word digits support bitwise operations independently in each limb. The fixed register lists determine the code. Four workspace registers are reserved as in schoolbook multiplication.

Main definitions

• Cslib.WordRAM.Multiword.Bitwise.Supported: and, or, and exclusive or.
• Cslib.WordRAM.Multiword.Bitwise.program: one standard instruction per limb.

Main results

• Cslib.WordRAM.Multiword.Bitwise.exec: checked execution, exact reconstructed result, bounded output digits, and preservation of every register outside the output list.

References

• T. Hagerup, Sorting and searching on the word RAM.

def Cslib.WordRAM.Multiword.Bitwise.Supported (f : BinOp) : Prop

The binary Boolean operations supported by the limbwise routine.

theorem Cslib.WordRAM.Multiword.Bitwise.eval_lt {f : BinOp} (hf : Supported f) {k a b : ℕ} (ha : a < 2 ^ k) (hb : b < 2 ^ k) : f.eval a b < 2 ^ k

Boolean operations preserve a power-of-two digit bound.

theorem Cslib.WordRAM.Multiword.Bitwise.eval_cons {f : BinOp} (hf : Supported f) {k a b : ℕ} (ha : a < 2 ^ k) (hb : b < 2 ^ k) (A B : ℕ) : f.eval (a + 2 ^ k * A) (b + 2 ^ k * B) = f.eval a b + 2 ^ k * f.eval A B

A Boolean operation commutes with adjoining one low power-of-two digit.

def Cslib.WordRAM.Multiword.Bitwise.program {r : ℕ} (f : BinOp) : List (Fin (r + 4)) → List (Fin (r + 4)) → List (Fin (r + 4)) → Code Basis.standard (r + 4)

Unrolled limbwise code. A final workspace self-copy makes the empty program executable.

theorem Cslib.WordRAM.Multiword.Bitwise.size_program {r : ℕ} (f : BinOp) (as bs ds : List (Fin (r + 4))) (hab : as.length = bs.length) (had : as.length = ds.length) : (program f as bs ds).size = ds.length + 1

Exact code size, including the final self-copy.

theorem Cslib.WordRAM.Multiword.Bitwise.exec {r w : ℕ} (hw : 2 ≤ w) {f : BinOp} (hf : Supported f) (as bs ds : List (Fin (r + 4))) (hab : as.length = bs.length) (had : as.length = ds.length) (hin : ∀ i ∈ as ++ bs, Workspace.IsDigit i) (hout : ∀ i ∈ ds, Workspace.IsDigit i) (hnd : ds.Nodup) (hdis : ds.Disjoint (as ++ bs)) (x : Data (r + 4)) (ha : Bounded (radix w) x as) (hb : Bounded (radix w) x bs) : ∃ (y : Data (r + 4)), Exec w (program f as bs ds) x y (ds.length + 1) ∧ Bounded (radix w) y ds ∧ value (radix w) y ds = f.eval (value (radix w) x as) (value (radix w) x bs) ∧ Workspace.Frame x y ds ∧ ∀ i ∉ ds, y.regs i = x.regs i

Execute a Boolean operation on equal-length bounded digit lists. Source lists may share registers; destinations are distinct and disjoint from both sources. All non-output registers, including all four workspace registers, are preserved.