20.4. Worked example🔗

The block below runs the lookup on the supported pair (2, 3) (the Conway polynomial C(2, 3) = 1 + x + x³ over 𝔽₂), further supported binary degrees, and unsupported pairs.

open Hex Hex.Conway

namespace HexConwayChapter

-- The committed table stores C(2,3) ascending by
-- degree: 1 + x + x³.
#guard luebeckConwayCoeffs? 2 3 = some [1, 1, 0, 1]

-- The lookup builds the FpPoly from those
-- coefficients, hitting the committed literal.
#guard luebeckConwayPolynomial? 2 3 =
  some luebeckConwayPolynomial_2_3

-- The SupportedEntry witness packages the same hit,
-- and conwayPoly reads the modulus back out.
#guard supportedEntry_2_3.poly =
  luebeckConwayPolynomial_2_3
#guard conwayPoly 2 3 supportedEntry_2_3 =
  luebeckConwayPolynomial_2_3

-- Unsupported pairs return none rather than
-- searching or generating certificates.
#guard luebeckConwayPolynomial? 2 8 =
  some luebeckConwayPolynomial_2_8
#guard luebeckConwayPolynomial? 2 16 =
  some luebeckConwayPolynomial_2_16
Hex.Conway.primitive_2_16 : Primitive 2 16 supportedEntry_2_16 [3, 5, 17, 257] [1, 1, 1, 1]#check primitive_2_16
Hex.Conway.compat_2_8_16 : Compatible 2 8 16 supportedEntry_2_8 supportedEntry_2_16#check compat_2_8_16
#guard luebeckConwayPolynomial? 2 129 =
  (none : Option (FpPoly 2))
#guard luebeckConwayPolynomial? 3 129 =
  (none : Option (FpPoly 3))
#guard luebeckConwayPolynomial? 2 0 =
  (none : Option (FpPoly 2))

end HexConwayChapter