pq-verify v2.9.0

Fixed

• A response answering one question twice could verify. A second answer
  to the same tcId replaced the first, so a response carrying a wrong answer
  followed by the right one reported VERIFIED. Any question answered more
  than once is now a finding, whatever the answers say.
• A truncated .json.gz response crashed the CLI with EOFError instead
  of reporting CANNOT VERIFY.
• Readers bound their input. A response larger than 64 MiB (measured
  after decompression, so a gzip bomb cannot expand in memory) or a hybrid
  transcript larger than 1 MiB is CANNOT VERIFY, and at most one byte past
  the limit is read. The largest genuine documents are about 3.3 MB and 8 KB.
• Freivalds used published seeds. Every Freivalds check drew its random
  vector from a constant in the source (42, trial + 1, ...), so anyone could
  compute it and build an NTT output that is wrong in several coefficients
  yet passes. The seed is now drawn from the OS once per run and printed;
  PQV_FREIVALDS_SEED=0x... replays a run.
• The Hasse check rejected genuine curves. It used 2*isqrt(p), which is
  one short of ⌊2√p⌋ for p = 7, 13, ..., and reported y² = x³ + 3 over F₇
  (t = −5) as CRITICAL. The bound is now isqrt(4p). Since no curve can
  exceed it, a violation is now reported as a defect in pq-verify's point
  count, not the curve's, and the "near-extreme trace" MEDIUM finding, which
  is not a known weakness, is gone.
• Two self-suite checks could not fail. "100,000 NTT butterflies"
  compared (a + w*b) % q with itself; it now runs every butterfly through
  the engine's Montgomery multiply and compares with integer arithmetic.
  "Freivalds throughput" passed unconditionally; it now requires every
  correct NTT to be accepted. The self-suite is still 160 checks.
• The Coq certificates proved almost nothing about the run. The "Full
  Kyber-768 NTT" certificate contained one layer-0 butterfly, and the batch
  certificate proved sums of random numbers drawn for the purpose. See Changed.

Changed

• --verify-hybrid recomputes the ML-KEM half, or does not say VERIFIED.
  Nothing tied the ciphertext in the server share to the ML-KEM secret in the
  combined secret, so a transcript with a corrupted ciphertext was reported
  VERIFIED. A transcript may now carry the client's ephemeral ML-KEM
  decapsulation key (clientMlkemDecapsulationKey, optional, like the ECDHE
  private scalars): pq-verify checks it against the client share and FIPS 203
  §7.3, decapsulates the ciphertext and compares the result byte-for-byte.
  Without the key that check is NOT CHECKED and the result is PARTIAL, so
  transcripts that verified before without it now report PARTIAL.
• Coq certificates are real, and checked for axioms. The NTT certificate
  defines the FIPS 203 forward NTT and zeta table in Coq and proves
  ntt input = output for all 256 coefficients (896 butterflies), plus
  17¹²⁸ ≡ −1 (mod 3329). The batch certificate proves pq-verify's ML-KEM and
  ML-DSA zeta tables are root^brv(i) mod q as FIPS 203/204 define them. A
  certificate passes only if coqc accepts it and Print Assumptions
  reports every theorem closed, so an Admitted proof (which coqc accepts)
  or an added axiom fails. The "Coq-certified" tagline is replaced by what is
  actually proved.

Added

• General proofs, pq-verify --proofs. pq_verify/coq/ now holds
  theorems that quantify over every input, checked by coqc with every theorem
  required to be closed (no axioms, no Admitted):

  • NTT.v: the FIPS 203 (ML-KEM) and FIPS 204 (ML-DSA) forward NTT equal
    the Chinese-remainder map they are defined to compute, for every
    256-coefficient input. The transform is written once, generic over its
    arithmetic; a map that preserves the arithmetic commutes with it, so
    running it once on symbolic linear forms gives its matrix, which Coq
    checks entry by entry against the CRT matrix.
  • Reduce.v: montgomery_reduce (ML-KEM, ML-DSA), barrett_reduce
    (ML-KEM, all 65,536 int16 inputs) and reduce32 (ML-DSA) are congruent
    to their input and within bound for every input in range, with no
    intermediate overflow.
  • Per-run NTT certificates now emit NTT.v's transform verbatim, so they
    are about the proved definition.

• Finding: two documented bounds in pq-crystals/dilithium ref/reduce.c
  are off by one. montgomery_reduce documents -Q < r < Q for
  -2^31 Q <= a <= Q 2^31, but a = Q 2^31 returns Q; reduce32
  documents r >= -6283008, but a = -255·2^23 - 2^22 returns -6283009.
  The code is right and no ML-DSA input comes near either point; the comments
  overstate it. The proofs state the true bounds, and both witnesses are
  checked theorems. (ML-KEM's comment excludes its corresponding point and is
  exact.)

• Wycheproof and CCTV edge-case vectors, pinned. 24 files from C2SP
  Wycheproof (3fa63dd) and CCTV (50a8ecf) ship in
  pq_verify/vectors/edge_vectors.json.gz, each with its upstream sha256 in
  EDGE_MANIFEST.json; tools/pin_edge_vectors.py re-pins them
  deterministically. They cover what NIST's ACVP vectors mostly do not:
  strcmp-trap ciphertexts, unlucky XOF sampling, every coefficient value
  q…4095 at every position of an encapsulation key, corrupted decapsulation
  keys, malleated ciphertexts, and ML-DSA hint, norm-bound and context edges.

  • --audit-kem runs them against the vendor library as three new stages,
    edgeValid, edgeEk, edgeDk (edge=False to skip). The pinned vendor
    table records them: mlkem-native 4,320/4,320; PQClean accepts all 2,931
    invalid encapsulation keys and all 6 invalid decapsulation keys while
    every valid output is byte-exact.
  • pq-verify --edge-cases [SET] runs them against pq-verify's own
    references (kyber-py, dilithium-py), with --json and --fail-on-finding.
  • The doctor checks the bundle's digests offline and runs the vectors
    against the installed references (--fast skips that run): a failure not
    in KNOWN_REFERENCE_DEFECTS BLOCKs.

• Finding: dilithium-py 1.4.0 accepts a repeated hint index. FIPS 204
  Algorithm 21 (HintBitUnpack) requires strictly increasing indices;
  dilithium-py compares with < instead of <=, so Wycheproof's "repeated
  hint" signature verifies for ML-DSA-44/65/87. It is fixed upstream
  (GiacomoPope/dilithium-py bd9b552) but in no release. pq-verify grades
  third-party signatures against NIST's expected results, not dilithium-py's
  verdict, so no third-party result changes; --edge-cases reports the
  reference as FINDINGS PRESENT until a fixed release can be pinned.

• tests/fuzz_readers.py — a structure-aware fuzzer for the readers that
  take files from outside parties. It mutates genuine responses and
  transcripts ~25 ways (type confusion, truncation, deep nesting, oversized
  and gzipped input, flipped hex digits, duplicate entries) and requires, for
  every case, no exception, an honest status, prompt termination, a CLI exit
  of 0/1/2, and no VERIFIED for a document that differs from a genuine one.
  It found all three bugs above and the hybrid gap. A seeded slice runs in
  the test suite.

---

Verifying this release

gh attestation verify pq_verify-2.9.0-py3-none-any.whl \
   --repo bigDSanalyst/pq-verify

Built by .github/workflows/release.yml from commit c029a633f46b4400e34b8c3c5cbcb1bbee854dd6,
after the full suite and all 855 NIST ACVP vectors passed on Python 3.9 through 3.13.
An SPDX SBOM is attached and attested.