def Hex.GF2Poly.clmulCoeffAt (idx : Nat) (x y : UInt64) (n : Nat) : Bool

Equations

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

def Hex.GF2Poly.xorBoolList (bits : List Bool) : Bool

XOR-fold a list of bits: xorBoolList bits is the parity of bits, folding != from false, so it is true exactly when an odd number of entries are true. The carryless-multiplication proofs reduce each output coefficient to such an XOR fold over a list of partial-product bits.

Equations

• Hex.GF2Poly.xorBoolList bits = List.foldl (fun (acc bit : Bool) => acc != bit) false bits

def Hex.GF2Poly.xorWordList : List UInt64 → UInt64

XOR a list of machine words as the word-level analogue of xorBoolList.

Equations

• Hex.GF2Poly.xorWordList [] = 0
• Hex.GF2Poly.xorWordList (word :: words) = word ^^^ Hex.GF2Poly.xorWordList words

def Hex.GF2Poly.clmulWordAt (idx : Nat) (x y : UInt64) (slot : Nat) : UInt64

The raw word contribution of a single clmul x y placed at word offset idx, projected to result word slot slot.

Equations

• Hex.GF2Poly.clmulWordAt idx x y slot = if slot = idx then (Hex.clmul x y).snd else if slot = idx + 1 then (Hex.clmul x y).fst else 0

def Hex.GF2Poly.leftAssocSourceTripleContribs (xs ys zs : Array UInt64) (n : Nat) : List Bool

Source-word contribution list for one coefficient of the left-associated raw product (xs * ys) * zs. The outer product contributes a word slot and a zs source word; each such intermediate word is expanded back to the xs/ys source pair contributions that created it.

Equations

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

def Hex.GF2Poly.rightAssocSourceTripleContribs (xs ys zs : Array UInt64) (n : Nat) : List Bool

Source-word contribution list for one coefficient of the right-associated raw product xs * (ys * zs). The outer product contributes an xs source word and an intermediate word slot; each intermediate word is expanded back to the ys/zs source pair contributions that created it.

Equations

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

def Hex.GF2Poly.leftAssocFixedTripleContribs (i j k : Nat) (x y z : UInt64) (n slotBound : Nat) : List Bool

Contributions from one fixed source triple (i,j,k) to the left-associated word product, varying only the intermediate (xs * ys) result slot.

Equations

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

def Hex.GF2Poly.rightAssocFixedTripleContribs (i j k : Nat) (x y z : UInt64) (n slotBound : Nat) : List Bool

Contributions from one fixed source triple (i,j,k) to the right-associated word product, varying only the intermediate (ys * zs) result slot.

Equations

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

def Hex.GF2Poly.wordBitAt (word : UInt64) (bit : Nat) : Bool

The selected bit of one machine word, using the same projection shape as the existing coefficient lemmas.

Equations

• Hex.GF2Poly.wordBitAt word bit = (word >>> bit.toUInt64 &&& 1 != 0)

def Hex.GF2Poly.oneHotBitWord (word : UInt64) (bit : Nat) : UInt64

The one-hot contribution of a selected source bit of a word.

Equations

• Hex.GF2Poly.oneHotBitWord word bit = if Hex.GF2Poly.wordBitAt word bit = true then 1 <<< bit.toUInt64 else 0