doc: reconcile the finite-field SPECs with the shipped API - #9298
Merged
Conversation
added 3 commits
August 20, 2026 05:06
Rewrites the hex-gfq, hex-conway, and hex-gfq-field SPEC API blocks to the signatures that actually ship, states the committed-table coverage limit outright, and brings hex-gfq-mathlib's SPEC up to the depth of the computational ones. Defines the composite GF2q n = GaloisField 2 n, which both SPECs named and neither library provided, moves the two committed-entry classes out of the Conway namespace into GFq where they are declared, documents the committed-prime word bounds and two other public declarations, and says what invPoly does at zero instead of leaving it unspecified. Progress file: progress/2026-07-28T12-36-04Z.md
The move of hex-gfq's committed-entry block from Hex.Conway to Hex.GFq renamed every declaration in it, not just the two classes; the chapter still cited packedGF2Entry_2_1_irreducible and its siblings by their old path.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR rewrites the
hex-gfq,hex-conway, andhex-gfq-fieldSPEC API blocks to the signatures that actually ship, states the committed-table coverage limit outright, and bringshex-gfq-mathlib's SPEC up to the depth of the computational ones. The SPECs had drifted behind the implementation: the shippedFiniteFieldtakes an extra prime witness and an ambientZMod64.Bounds,conwayPolytakes aSupportedEntry, andGFq/GFqC/GF2qare three constructors rather than one.It also defines the composite
GF2q n ≃+* GaloisField 2 n, which both SPECs named and neither library provided; the two legs already existed. The two committed-entry classes move out of theConwaynamespace intoGFq, where they are declared and where a reader will look for them, along with the packed binary modulus and certificate they name. The committed-prime word bounds and two other public declarations gain docstrings, andinvPolynow says what it returns at zero rather than leaving it unspecified.🤖 Prepared with Claude Code