@[extern lean_hex_word_poly_add]

def Hex.WordPoly.add {m : UInt64} (ctx : _root_.MontCtx m) (a b : DensePoly (WordMod ctx)) : DensePoly (WordMod ctx)

Dense addition over a full-word Montgomery ring, with a native array kernel behind the exact Lean contract.

Equations

• Hex.WordPoly.add ctx a b = a + b

@[extern lean_hex_word_poly_sub]

def Hex.WordPoly.sub {m : UInt64} (ctx : _root_.MontCtx m) (a b : DensePoly (WordMod ctx)) : DensePoly (WordMod ctx)

Dense subtraction over a full-word Montgomery ring, with a native array kernel behind the exact Lean contract.

Equations

• Hex.WordPoly.sub ctx a b = a - b

@[extern lean_hex_word_poly_mul]

def Hex.WordPoly.mul {m : UInt64} (ctx : _root_.MontCtx m) (a b : DensePoly (WordMod ctx)) : DensePoly (WordMod ctx)

Dense multiplication over a full-word Montgomery ring. The Lean body is the exact logical contract; lean_hex_word_poly_mul is its allocation-light runtime implementation.

Equations

• Hex.WordPoly.mul ctx a b = a * b

@[extern lean_hex_word_poly_mul_add]

def Hex.WordPoly.mulAdd {m : UInt64} (ctx : _root_.MontCtx m) (a b c d : DensePoly (WordMod ctx)) : DensePoly (WordMod ctx)

Sum of two dense products over a full-word Montgomery ring. The native kernel fuses both convolutions and the final addition into one output pass.

Equations

• Hex.WordPoly.mulAdd ctx a b c d = a * b + c * d

@[simp]

theorem Hex.WordPoly.mul_eq {m : UInt64} (ctx : _root_.MontCtx m) (a b : DensePoly (WordMod ctx)) : mul ctx a b = a * b

The packed runtime kernel has the ordinary dense product as its logical value.

@[simp]

theorem Hex.WordPoly.mulAdd_eq {m : UInt64} (ctx : _root_.MontCtx m) (a b c d : DensePoly (WordMod ctx)) : mulAdd ctx a b c d = a * b + c * d

@[simp]

theorem Hex.WordPoly.add_eq {m : UInt64} (ctx : _root_.MontCtx m) (a b : DensePoly (WordMod ctx)) : add ctx a b = a + b

@[simp]

theorem Hex.WordPoly.sub_eq {m : UInt64} (ctx : _root_.MontCtx m) (a b : DensePoly (WordMod ctx)) : sub ctx a b = a - b