def Hex.GF2Poly.xorClmulAt (acc : Array UInt64) (idx : Nat) (x y : UInt64) : Array UInt64

XOR a 128-bit carry-less product into adjacent result words.

Equations

• Hex.GF2Poly.xorClmulAt acc idx x y = match Hex.clmul x y with | (hi, lo) => have acc := acc.set! idx (acc[idx]! ^^^ lo); acc.set! (idx + 1) (acc[idx + 1]! ^^^ hi)