formal: wave-1 close-out (averin)

[zachyking]

Problem

Wave-1 close-out (VUL-15 cross-language half). vultrino computes averin's params hiding commitment for its use PoP, but no shared vector pinned the two implementations to a third, and nothing in CI regenerated the committed vector files from their generators.

Fix / Proof

• vectors/params-commitment.v1.json: 11 golden commitments over the four field domains (empty and multibyte values, lengths 255/256/1024, NUL and high bytes) plus 8 rejected nonce strings, produced by the independent Python reference scripts/vectors/gen_params_commitment.py (stdlib only; --check fails when stale). Owner averin, pinned in vectors/vectors.lock; vultrino keeps a byte-identical copy.
• core/tests/params_commitment_vectors.rs: commit::commit reproduces every vector and the FFI-strict decode refuses every rejected nonce.
• Claim params-commitment-vectors-match-reference (kit v2 and legacy register, FORMAL.md re-rendered) with killing mutant seams-commit-nonce-not-bound (the nonce is dropped from the preimage).
• CI: the formal-kit job now runs gen_authority_v3.py --check and gen_params_commitment.py --check (regenerate and compare).

Red-first / bite evidence

check_mutants.py --only seams-commit-nonce-not-bound: killed (detector exit 101, a failing assertion on the vector, not a compile error).

Gates run

gen_params_commitment.py --check, cargo test -p averin-decision-core --test params_commitment_vectors, check_claims.py --claims formal/kit-claims.json (264 checks, 0 failures), scripts/check-claims.py, kit unit tests, check_vectors_lock.py --peer vultrino=....

What this does NOT establish

Only the listed inputs. The reference and implementation share the written format (RCP 9.3), so a flaw in the format is in both. Not that the nonce is random or that a commitment hides a value. Copy identity with vultrino is checked only by the local --peer run, not by CI. evidence_run is not recorded yet (a CI run on main will prove it).

Merge order

1. averin (this) 2. vultrino (vendors this file) 3. govder 4. feir-os; leria is independent.

[cloudflare-workers-and-pages]

Deploying averin-verify with    Cloudflare Pages

Latest commit:	6e5d05f
Status:	✅  Deploy successful!
Preview URL:	https://afebfbad.averin-verify.pages.dev
Branch Preview URL:	https://formal-p3-w1close.averin-verify.pages.dev

View logs