Make Rocq formal proofs gating (rocq-proofs is continue-on-error)

[avrabe]

Expected standard (the "full circle"): a formal-verification asset should be (1) wired into CI, (2) gating — not continue-on-error — so a regression actually blocks the merge, and (3) complete — no sorry/axioms standing in for proofs. When any link is missing, the proof exists but cannot stop a regression, so the loop is open. Maybe there is a reason here; if so it should be documented — otherwise it should follow the standard.

Found: the rocq-proofs job (.github/workflows/ci.yml:361-366) runs with continue-on-error: true. The optimization semantic-preservation proofs (WasmSemantics, ConstantFolding/StrengthReduction correctness, and the rocq-of-rust translation link) run and report, but a proof regression passes the build silently.

Recommend: remove continue-on-error from rocq-proofs so proof breakage blocks merge. If non-gating is intentional (runtime, flakiness), document why and/or move to a gating nightly.

Noticed during a kiln verification-corpus audit comparing how each PulseEngine repo wires its proofs.

[avrabe]

Confirmed the gap — and the reason it can't be a one-line fix today.

Current state: the rocq-proofs job is red on main right now (latest ci.yml run: Rocq Formal Proofs = failure). It's red because of the upstream rules_rocq_rust toolchain breakage — the job runs bazel build/test //proofs/... and can't build the proofs. So removing continue-on-error today would flip the whole CI gate red and block every merge, not catch regressions.

Criterion 3 (complete): the proofs currently carry 10 Admitted + 19 Axiom. Gating would catch a regression in the proven parts, but those admits/axioms remain open holes — a separate, larger proof effort.

Sequencing to actually close this (all three links):

1. Land the rules_rocq_rust bump so the job goes green — fixes chore(deps): bump rules_rocq_rust to e4660cc (rules_rust migration; fixes Rocq Formal Proofs CI) #141 / ci: fix Rocq Formal Proofs — bump rules_rocq_rust to hermetic toolchain #139 are exactly this (⚠️ they're redundant; pick one).
2. Then remove continue-on-error → gating. (One-line change once green.)
3. Discharge the Admitted/Axiom for criterion 3 — track separately.

Done now (#170): since the issue rightly says a deviation should be documented if there's a reason, I've documented the rationale + this exact plan inline on the job (comment-only; I deliberately did not remove continue-on-error while red). #170 keeps the loop honest in the interim; step 2 lands the moment #141/#139 make the job green.