Add NIST GHASH <-> POLYVAL bridge (Gueron Proposition 1)#396
Merged
Conversation
Introduces common/ghash_nist_bridge.ml with the formal proof of Gueron's Proposition 1 (CSCML 2023): bit-reflecting inputs, carry-less multiplying, reducing mod P(x), and bit-reflecting back equals polyval_dot with an x-shifted key. Key definitions and lemmas: - bit_reflect128: bit-reflection on 128-bit words (word_reversefields 1) - BIT_REFLECT128, REFLECT128_INVOLUTION, REFLECT128_XOR - PMUL_REFLECT128: reflecting both factors reverses the product - GHASH_POLYVAL_RECIPROCAL: P(x) and Q(x) coefficient reciprocity - PMUL_GHASH_POLYVAL_REFLECT: the bit-level P-to-Q transport - GUERON_PROP1: the main theorem Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Define nist_dot (the native NIST GHASH multiply) and nist_ghash (recursive Horner iteration using nist_dot, matching NIST SP 800-38D). Prove the bridge theorems connecting them to the POLYVAL layer: - NIST_DOT_IS_POLYVAL_DOT: nist_dot a b = polyval_dot a (ghash_twist b) - NIST_GHASH_IS_POLYVAL: by list induction via GUERON_PROP1 - NIST_GHASH_NIL, NIST_GHASH_CONS, NIST_GHASH_APPEND Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
nebeid
changed the title
nebeid
force-pushed
the
ghash-nist-bridge-pr
branch
3 times, most recently
from
c32f41b to
714e26f
Compare
Replace QXP_EQ_XQPMULP (Q * x * p = x * pmul(Q,p)) with the simpler QP_EQ_QPMULP (Q * p = pmul(Q,p)), which follows directly from POLY_OF_WORD_PMUL_2N. This lets the witness be poly(zx(REF m)) instead of x * poly(zx(ushr(REF m, 1))), eliminating word_ushr from the proof entirely. Supporting changes: - BIT_WORD_ZX_USHR_REFLECT -> BIT_WORD_ZX_REFLECT (no precondition) - PMUL_GHASH_POLYVAL_REFLECT: bijection 127-j instead of 126-j - RHS_PMUL_BOUND_DIRECT: simpler proof using BIT_POLYVAL_WORD - Remove BOOL_POLY_MUL_VARPOW_COMM, POLY_MUL_VAR_SHIFT (no longer needed) - Align all comment closing brackets to column 79 Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
nebeid
force-pushed
the
ghash-nist-bridge-pr
branch
from
714e26f to
10b15a8
Compare
Contributor
nice! |
nebeid
force-pushed
the
ghash-nist-bridge-pr
branch
from
10b15a8 to
f1eaf2b
Compare
jargh
approved these changes
May 22, 2026
Contributor
jargh
left a comment
jargh
left a comment
There was a problem hiding this comment.
All looks great, thank you! We should eventually be able to simplify it using some of the new HOL Light library material like poly_recip, but all the results seem sound.
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
3 participants
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.
Introduces
common/ghash_nist_bridge.ml, the formal bridge betweenthe NIST SP 800-38D GHASH specification (bit-reflected, mod P(x)) and
the POLYVAL-based computation (natural bit order, mod Q(x)) used by
the AES-GCM assembly implementations.
Key definitions
nist_dot a b: the native NIST GHASH "•" operation — bit-reflectinputs, carry-less multiply, reduce mod P(x), bit-reflect the result.
nist_ghash h acc xs: recursive Horner iteration usingnist_dot,matching the NIST SP 800-38D specification directly.
Key theorems
GUERON_PROP1: the main algebraic bridge —bit_reflect128(ghash_reduce(pmul(REF a, REF b))) = polyval_dot a (ghash_twist b).This is the formal statement of Gueron's Proposition 1 (CSCML 2023).
NIST_DOT_IS_POLYVAL_DOT:nist_dot a b = polyval_dot a (ghash_twist b).NIST_GHASH_IS_POLYVAL:nist_ghash h acc xs = ghash_polyval_acc (ghash_twist h) acc xs.Proved non-trivially by list induction via
GUERON_PROP1(not adefinitional unfolding).
NIST_GHASH_NIL,NIST_GHASH_CONS,NIST_GHASH_APPEND.Proof simplification (commit 3)
The GUERON_PROP1 proof was simplified to eliminate
word_ushrfrom theideal-membership witness. The original proof factored
xout ofREF(m)(valid sincebit 0 (REF m) = F) and usedQXP_EQ_XQPMULPto rewrite
Q · (x · p). The simplified proof usesQP_EQ_QPMULP(
Q · p = pmul(Q_word, p), a direct consequence ofPOLY_OF_WORD_PMUL_2N) with witnesspoly(zx(REF m))directly.This also removes
BOOL_POLY_MUL_VARPOW_COMMandPOLY_MUL_VAR_SHIFT.Dependencies
This PR depends on #394 (
common/polyval_ghash.ml), which depends on#393 (
common/polyval.mlstructural infrastructure). #392 and #388 arealready merged.
Testing
common/ghash_nist_bridge.mlloads cleanly in HOL Light (~530s).No
CHEAT_TACornew_axiomin the proofs.