fix: bump ordeal 0.9.1 → 0.14.0 — rem_s can now route through trap_gate

[avrabe]

Completes the consumer side of ordeal#84 (= ordeal#72), and removes one blocker from #288.

The gap

ordeal < 0.10.0's trap_div(DivOp::RemS) wrongly included the INT_MIN/-1 overflow clause (WASM Core §4.4.1: only idiv_s traps there; irem_s(INT_MIN, -1) = 0, defined). So this gate falsely rejected the sound rem_s(INT_MIN,-1) → 0 fold as a phantom trap mismatch — which is why rem_s stayed on the per-pass static guard. ordeal fixed it in v0.10.0; this picks it up (0.14.0 current).

The un-pinning test is mutation-checked, not asserted

# ordeal 0.14.0:
test trap_gate::tests::rem_s_int_min_neg1_fold_is_accepted ... ok

# pin flipped back to ordeal 0.9.1:
FAILED — "rem_s(INT_MIN,-1) -> 0 is a sound fold and must be ACCEPTED
          (ordeal < 0.10.0 falsely rejected it), got RejectCounterexample([])"

That reproduces the historical false rejection exactly. The dual guard is included: a wrong-value rem_s fold (→ 1 instead of 0) is still rejected, so accepting the sound fold did not wave rem_s folds through.

Also fixed

div_define's doc comment described 0.9.1's bug as spec ("INT_MIN/-1 overflow for the signed ops" — it's div_s only).

Gate

Full loom-core suite with the verification feature: 655 tests, 0 failed. API compatible across ordeal 0.10–0.14 — no code changes needed beyond docs + tests.

What this does NOT do

#288's systemic finding stands: trap_gate is still never called by any pass (confirmed on ad39d1c — the only external reference is a test). This bump removes the rem_s blocker for that wiring; the wiring itself — a per-fold gate call inside constant_folding, with its cost/caching design questions — is its own effort and shouldn't ride along in a dependency bump.

🤖 Generated with Claude Code

https://claude.ai/code/session_01EBJ6kdJ16E3hnsBbq9Lwf1

[avrabe]

CI note: the two non-green checks are not caused by this PR. Rocq Formal Proofs fails on main's HEAD as well (verified on the current main commit — pre-existing), and Verification Gate (rivet-driven) was cancelled downstream of it. The 23 checks that exercise this change (build, loom-core suite incl. the new trap_gate tests, clippy, fmt) all pass. Leaving the merge decision to the maintainer since the red is main's, not this branch's — merging around it vs fixing Rocq first is a repo-health call I shouldn't make from a dependency bump.