16.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 𝔽₂) and on two 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: n outside {1..6}, or n = 0.
#guard luebeckConwayPolynomial? 2 7 =
  (none : Option (FpPoly 2))
#guard luebeckConwayPolynomial? 2 0 =
  (none : Option (FpPoly 2))

end HexConwayChapter