Surface: fv · Severity: unknown (suspicion, unverified — flagged by the repo's own README as an incomplete trace) · Evidence: suspicion, unverified · Target: f91aa82
Claimed (implicit): the certified c10-port capstone's dependency chain is admit-free (the 905-pin census tracks statements; admits are pinned by name+type).
Suspicion: nhchwcoll_hchwpre_msg — an admitted lemma inherited from MM45 — is used at base-c10-split/WOTS_TW_ES.ec:6542, in a file the capstone requires transitively. easycrypt/README.md:84-90 self-discloses the consume-trace as incomplete ("a trace I did not complete"). If the consuming result is on the capstone's path, the capstone rests on an admit; if not, that should be shown mechanically. Owner is actively working this surface (2026-08-20).
Fix: complete the consume-trace (cert_cone already parses requires transitively); if the admit is live in the capstone cone, either discharge it or pin it as a named, marketed assumption. Found 2026-08-20 FV red-team (sub-quorum suspicion — retained honestly, no PoC claimed).
Surface: fv · Severity: unknown (suspicion, unverified — flagged by the repo's own README as an incomplete trace) · Evidence: suspicion, unverified · Target: f91aa82
Claimed (implicit): the certified c10-port capstone's dependency chain is admit-free (the 905-pin census tracks statements; admits are pinned by name+type).
Suspicion:
nhchwcoll_hchwpre_msg— an admitted lemma inherited from MM45 — is used atbase-c10-split/WOTS_TW_ES.ec:6542, in a file the capstone requires transitively.easycrypt/README.md:84-90self-discloses the consume-trace as incomplete ("a trace I did not complete"). If the consuming result is on the capstone's path, the capstone rests on an admit; if not, that should be shown mechanically. Owner is actively working this surface (2026-08-20).Fix: complete the consume-trace (cert_cone already parses requires transitively); if the admit is live in the capstone cone, either discharge it or pin it as a named, marketed assumption. Found 2026-08-20 FV red-team (sub-quorum suspicion — retained honestly, no PoC claimed).