def Hex.clmulAccumulateBit (acc : UInt64 × UInt64) (a : UInt64) (bitIdx : Nat) : UInt64 × UInt64

XOR the carry-less partial product a * x^bitIdx into the (hi, lo) accumulator. The caller must supply bitIdx < 64.

Equations

• One or more equations did not get rendered due to their size.

def Hex.pureClmul (a b : UInt64) : UInt64 × UInt64

Pure Lean carry-less multiplication of two 64-bit words, returned as (hi, lo) for the 128-bit product.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.pureClmul_xor_left (x y z : UInt64) : pureClmul (x ^^^ y) z = ((pureClmul x z).fst ^^^ (pureClmul y z).fst, (pureClmul x z).snd ^^^ (pureClmul y z).snd)

The pure carry-less multiplier is linear in its left word argument over bitwise XOR.

@[simp]

theorem Hex.pureClmul_zero_left (x : UInt64) : pureClmul 0 x = (0, 0)

The pure carry-less multiplier returns zero when the left word is zero.

@[simp]

theorem Hex.pureClmul_zero_right (x : UInt64) : pureClmul x 0 = (0, 0)

The pure carry-less multiplier returns zero when the right word is zero.

def Hex.clmulOneHotStep (a : UInt64) (hot : Nat) (acc : UInt64 × UInt64) (bitIdx : Nat) : UInt64 × UInt64

One fold step for multiplying by the one-hot right word 1 <<< hot: accumulate a's partial product at bitIdx only when bitIdx is the hot bit.

Equations

• Hex.clmulOneHotStep a hot acc bitIdx = if (1 <<< hot.toUInt64 >>> bitIdx.toUInt64 &&& 1 != 0) = true then Hex.clmulAccumulateBit acc a bitIdx else acc

theorem Hex.pureClmul_oneHot (a : UInt64) {bit : Nat} (hbit : bit < 64) : pureClmul a (1 <<< bit.toUInt64) = if bit = 0 then (0, a) else (a >>> (64 - bit).toUInt64, a <<< bit.toUInt64)

Carry-less multiplication by an in-word monomial has one contributing partial product in the pure fold.

def Hex.clmulOneHotLeftLowStep (hot : Nat) (a lo : UInt64) (bitIdx : Nat) : UInt64

Low-word fold step for the one-hot left word 1 <<< hot: XOR 1 <<< (hot + bitIdx) into the low word when bit bitIdx of a is set and hot + bitIdx < 64, otherwise leave it unchanged.

Equations

• Hex.clmulOneHotLeftLowStep hot a lo bitIdx = if (a >>> bitIdx.toUInt64 &&& 1 != 0) = true then if hot + bitIdx < 64 then lo ^^^ 1 <<< (hot + bitIdx).toUInt64 else lo else lo

theorem Hex.pureClmul_oneHot_left_snd (a : UInt64) {bit : Nat} (hbit : bit < 64) : (pureClmul (1 <<< bit.toUInt64) a).snd = if bit = 0 then a else a <<< bit.toUInt64

Low word of pure carry-less multiplication with an in-word monomial on the left.

def Hex.clmulOneHotLeftHighStep (hot : Nat) (a hi : UInt64) (bitIdx : Nat) : UInt64

High-word fold step for the one-hot left word 1 <<< hot: XOR 1 <<< (hot + bitIdx - 64) into the high word when bit bitIdx of a is set and 64 ≤ hot + bitIdx, otherwise leave it unchanged.

Equations

• Hex.clmulOneHotLeftHighStep hot a hi bitIdx = if (a >>> bitIdx.toUInt64 &&& 1 != 0) = true then if hot + bitIdx < 64 then hi else hi ^^^ 1 <<< (hot + bitIdx - 64).toUInt64 else hi

theorem Hex.pureClmul_oneHot_left_fst (a : UInt64) {bit : Nat} (hbit : bit < 64) : (pureClmul (1 <<< bit.toUInt64) a).fst = if bit = 0 then 0 else a >>> (64 - bit).toUInt64

High word of pure carry-less multiplication with an in-word monomial on the left.

theorem Hex.pureClmul_oneHot_left (a : UInt64) {bit : Nat} (hbit : bit < 64) : pureClmul (1 <<< bit.toUInt64) a = if bit = 0 then (0, a) else (a >>> (64 - bit).toUInt64, a <<< bit.toUInt64)

Pure carry-less multiplication with an in-word monomial on the left.

@[extern lean_hex_clmul_u64]

def Hex.clmul (a b : UInt64) : UInt64 × UInt64

Trusted runtime hook for carry-less multiplication.

The compiled C shim must return the same (hi, lo) pair as Hex.pureClmul; the intrinsic-backed implementations are an optimization only.

Equations

• Hex.clmul a b = Hex.pureClmul a b

theorem Hex.clmul_eq_pureClmul (a b : UInt64) : clmul a b = pureClmul a b

The trusted extern-backed multiplier has Hex.pureClmul as its logical reference semantics.

theorem Hex.clmul_eq_pureClmul_fst (a b : UInt64) : (clmul a b).fst = (pureClmul a b).fst

The high word of the extern-backed multiplier has pureClmul as its logical reference semantics.

theorem Hex.clmul_eq_pureClmul_snd (a b : UInt64) : (clmul a b).snd = (pureClmul a b).snd

The low word of the extern-backed multiplier has pureClmul as its logical reference semantics.

@[simp]

theorem Hex.clmul_zero_left (x : UInt64) : clmul 0 x = (0, 0)

Carry-less multiplication by zero on the left returns the zero product.

@[simp]

theorem Hex.clmul_zero_right (x : UInt64) : clmul x 0 = (0, 0)

Carry-less multiplication by zero on the right returns the zero product.

theorem Hex.clmul_oneHot (a : UInt64) {bit : Nat} (hbit : bit < 64) : clmul a (1 <<< bit.toUInt64) = if bit = 0 then (0, a) else (a >>> (64 - bit).toUInt64, a <<< bit.toUInt64)

Runtime clmul, under its trusted reference contract, agrees with the one-hot pure carry-less multiplication split.

theorem Hex.clmul_xor_left (x y z : UInt64) : clmul (x ^^^ y) z = ((clmul x z).fst ^^^ (clmul y z).fst, (clmul x z).snd ^^^ (clmul y z).snd)

Runtime clmul, under its trusted reference contract, is linear in its left word argument over bitwise XOR.

theorem Hex.clmul_oneHot_fst (a : UInt64) {bit : Nat} (hbit : bit < 64) : (clmul a (1 <<< bit.toUInt64)).fst = if bit = 0 then 0 else a >>> (64 - bit).toUInt64

High word of carry-less multiplication by an in-word monomial.

theorem Hex.clmul_oneHot_snd (a : UInt64) {bit : Nat} (hbit : bit < 64) : (clmul a (1 <<< bit.toUInt64)).snd = if bit = 0 then a else a <<< bit.toUInt64

Low word of carry-less multiplication by an in-word monomial.

theorem Hex.clmul_oneHot_left (a : UInt64) {bit : Nat} (hbit : bit < 64) : clmul (1 <<< bit.toUInt64) a = if bit = 0 then (0, a) else (a >>> (64 - bit).toUInt64, a <<< bit.toUInt64)

Runtime clmul, under its trusted reference contract, with an in-word monomial on the left.

theorem Hex.clmul_oneHot_left_fst (a : UInt64) {bit : Nat} (hbit : bit < 64) : (clmul (1 <<< bit.toUInt64) a).fst = if bit = 0 then 0 else a >>> (64 - bit).toUInt64

High word of carry-less multiplication with an in-word monomial on the left.

theorem Hex.clmul_oneHot_left_snd (a : UInt64) {bit : Nat} (hbit : bit < 64) : (clmul (1 <<< bit.toUInt64) a).snd = if bit = 0 then a else a <<< bit.toUInt64

Low word of carry-less multiplication with an in-word monomial on the left.

def Hex.xorPair (x y : UInt64 × UInt64) : UInt64 × UInt64

Componentwise bitwise XOR of two (hi, lo) word pairs. This is the addition law on 128-bit carry-less products, used to combine partial products in the bit-fold reformulations of clmul.

Equations

• Hex.xorPair x y = (x.fst ^^^ y.fst, x.snd ^^^ y.snd)

def Hex.wordBitXorStep (w acc : UInt64) (bit : Nat) : UInt64

Fold step that XORs the monomial x^bit into the accumulator exactly when bit bit of w is set, leaving it unchanged otherwise. Folding this over all bit positions reassembles w from its set bits.

Equations

• Hex.wordBitXorStep w acc bit = if (w >>> bit.toUInt64 &&& 1 != 0) = true then acc ^^^ 1 <<< bit.toUInt64 else acc

def Hex.wordBitFold (w : UInt64) : UInt64

Reconstruct w by folding wordBitXorStep over all 64 bit positions, re-expressing the word as the XOR of its one-hot monomials.

Equations

• Hex.wordBitFold w = List.foldl (Hex.wordBitXorStep w) 0 (List.range 64)

def Hex.clmulLeftBitFoldStep (w y : UInt64) (acc : UInt64 × UInt64) (bit : Nat) : UInt64 × UInt64

Fold step accumulating the partial product clmul (x^bit) y (one-hot on the left factor) into acc when bit bit of w is set. Folded over all bits this computes clmul w y.

Equations

• Hex.clmulLeftBitFoldStep w y acc bit = if (w >>> bit.toUInt64 &&& 1 != 0) = true then Hex.xorPair acc (Hex.clmul (1 <<< bit.toUInt64) y) else acc

def Hex.clmulRightBitFoldStep (w y : UInt64) (acc : UInt64 × UInt64) (bit : Nat) : UInt64 × UInt64

Fold step accumulating the partial product clmul y (x^bit) (one-hot on the right factor) into acc when bit bit of w is set. The right-factor twin of clmulLeftBitFoldStep, used to commute the two arguments.

Equations

• Hex.clmulRightBitFoldStep w y acc bit = if (w >>> bit.toUInt64 &&& 1 != 0) = true then Hex.xorPair acc (Hex.clmul y (1 <<< bit.toUInt64)) else acc

def Hex.clmulPureRightStep (w y : UInt64) (acc : UInt64 × UInt64) (bit : Nat) : UInt64 × UInt64

Fold step driving clmul y w the way pureClmul does: apply the executable clmulAccumulateBit acc y bit when bit bit of w is set, else keep acc. Links the executable fold to clmulRightBitFoldStep.

Equations

• Hex.clmulPureRightStep w y acc bit = if (w >>> bit.toUInt64 &&& 1 != 0) = true then Hex.clmulAccumulateBit acc y bit else acc

theorem Hex.clmul_comm (x y : UInt64) : clmul x y = clmul y x

Carry-less word multiplication is commutative. This is the reusable word-level symmetry needed by packed polynomial multiplication proofs.

theorem Hex.clmul_xor_right (x y z : UInt64) : clmul x (y ^^^ z) = ((clmul x y).fst ^^^ (clmul x z).fst, (clmul x y).snd ^^^ (clmul x z).snd)

Runtime clmul, under its trusted reference contract, is linear in its right word argument over bitwise XOR.

theorem Hex.pureClmul_comm (x y : UInt64) : pureClmul x y = pureClmul y x

Pure carry-less word multiplication is commutative.

theorem Hex.pureClmul_xor_right (x y z : UInt64) : pureClmul x (y ^^^ z) = ((pureClmul x y).fst ^^^ (pureClmul x z).fst, (pureClmul x y).snd ^^^ (pureClmul x z).snd)

The pure carry-less multiplier is linear in its right word argument over bitwise XOR.