Add ML-DSA rejection acceptance foundation

[BenKnill]

Summary

• add a reusable HOL Light model of rejection-sampling acceptance bitmaps, prefix counts, stopping indices, table indices, and loop-event coordinates;
• connect the eta2 and eta4 nibble filters to that shared acceptance model;
• make same-directory proof dependencies explicit with ./... paths.

This materially advances issue #1160, but it does not complete either *_SUBROUTINE_SAFE result. The remaining work is to connect the proved public acceptance/event skeleton to the concrete machine-event trace and then discharge the subroutine wrappers.

Proof evidence and boundary

• The development loop and durable replay milestones succeeded for the staged foundation, culminating in the final 21-binding helper skeleton with zero added axioms.
• The helper committed here is the exact proved source (SHA-256 1b0bcc7154c98740d8e09a048d1539f14a942205a43c4d88e153e36701a79384).
• A later, separate full-source eta4 attempt was killed by SIGKILL (signal 9 / exit 137, approximately 5.45 GB resident memory). It produced no proof claim.
• The experimental, unproved mldsa_rej_uniform_eta4_body_events.ml theorem is deliberately excluded from this PR.

Issue #1160 therefore remains open.

Packaging checks

• isolated worktree based on exact upstream commit 41c00dac3f3ce4f578f16aee9f9cd25e6bc05add;
• three intended paths compared byte-for-byte with the proved development checkout;
• git diff --check passed;
• no Python bytecode or unrelated .grok* artifacts included;
• HOL/profile execution was intentionally not repeated during packaging.

[hanno-becker]

The above bitmap definition seems to replicate logic that's already there: In the MLDSA_REJ_UNIFORM_ETA2_SUBROUTINE_CORRECT specification we already unpack the byte input into a list of nibbles of the right length (in that case, for example, it's inlist : 4 word list), so the bitmap in question is just a map applied on that inlist.

My expectation here is that we can largely follow the existing constant-time specification, but that instead of passing inlist to the event-generating function, we just pass the bitmap. Please note also that I believe @jakemas was looking into this issue in particular. You should either consult with him on the respective issue or pick a different one for a first contribution.

[hanno-becker]

Thank you @BenKnill for your interest and contribution! We don't currently accept contributions from people we don't know. If you are interested in contributing, would you kindly reach out on Discord or via mail to introduce yourself? Thank you!