Formal verification for the ECSM affine selector

[nicole-graus]

Motivation

#879 publishes yR, which makes two things observable that weren't: the input point's parity, and yR's representation. Both are closed by new checks in that PR. This adds an independent model and a soundness gate so those checks are verified rather than argued.
Additive only — 28 files under docs/verification/ecsm-affine/, no repo source touched.

Description

• Oracle — secp256k1 and both ecall semantics reimplemented from the curve definition (no k256, no repo code), anchored by 9 independent checks including a cross-check against the PyPI ecdsa package.
• Gate — z3/sympy lemmas over the surface Perf/ecsm affine selector #879 adds: the IS_AFFINE selector and its Ecall pinning, OverflowKind::YrLtP, the yG read / yR write, and the address-limb bounds.
• Anchors — the model is evaluated on 32 witnesses from the repo's own ecsm::compute_witness{,_with_y} before any UNSAT is trusted, and 19 premises the gate assumes about the Rust are read from source and mutation-tested.

Seven distinct attacks are exhibited constructively. Every new check in #879 has a control showing it is load-bearing.

Two results worth reading:

• The YrLtP band really is populated — there is a secp256k1 point with y = 1, so yR + p is 32-byte representable. The forgery is carried through the ECDAS relation and its carry window, not just asserted at the value level.
• The parity gap is instantiated: two complete witnesses over the same (xG, k), both satisfying all 423 in-table constraints, same xR, different yR. Reproduced 9× from crypto/ecsm itself.

How to test

cd docs/verification/ecsm-affine
python3 -m venv .venv && ./.venv/bin/pip install z3-solver sympy ecdsa
./run_gate.sh