ci(idris2): flip build oracle to strict (closes #70 follow-up) (#118)

The Idris2 build oracle was landed non-blocking in PR #106 because
several pre-existing typecheck/parse errors prevented `idris2 --build`
from succeeding. All four blockers have since cleared:

* #105 — Model.idr DecEq impossible-pattern + equivRefl hole
* #109 — Composition.idr applyOp via Model primitives + cascade
* #112 — RMO AuditEntry.proof rename (Idris2 0.8.0 reserved keyword)
* #113 — RMO hardwareEraseIrreversible single-line signature
* #117 — RMO overwriteIrreversible LTE + auditTrailCompleteness Elem import

Local verification post-#117:

    $ idris2 --build proofs/idris2/valence-shell.ipkg
    1/4: Building Filesystem.Model       OK
    2/4: Building Filesystem.RMO         OK
    3/4: Building Filesystem.Operations  OK
    4/4: Building Filesystem.Composition OK

Flip the workflow's terminal `exit 0` → `exit 1`, upgrade the warning
to an error, and document the precondition chain.

Follow-up (owner action): add `verify-idris2 (Idris2 build oracle)` to
the repo's branch protection required-checks list so the strict gate
propagates to merge blocking.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/idris-verification.yml

@@ -114,8 +114,14 @@ jobs:
       - name: Gate on build status
         if: steps.idris2-build.outputs.build_exit != '0'
         run: |
-          echo "::warning::Idris2 build oracle FAILED (exit ${{ steps.idris2-build.outputs.build_exit }}). Tracked as pre-existing debt in #94."
-          # Non-blocking by default. To make this a required gate once pre-
-          # existing issues are fixed, change `exit 0` to `exit 1` below and
-          # add to branch protection's required checks list.
-          exit 0
+          echo "::error::Idris2 build oracle FAILED (exit ${{ steps.idris2-build.outputs.build_exit }})."
+          # Strict gate as of 2026-06-02. All four Idris2 modules
+          # (Model, RMO, Operations, Composition) now build cleanly via:
+          #   * #105 (Model.idr DecEq impossible-pattern + equivRefl hole)
+          #   * #109 (Composition.idr applyOp via Model primitives + cascade)
+          #   * #112 (RMO AuditEntry.proof rename — Idris2 0.8.0 reserved keyword)
+          #   * #113 (RMO hardwareEraseIrreversible single-line signature)
+          #   * #117 (RMO overwriteIrreversible LTE + auditTrailCompleteness Elem import)
+          # Add this job to branch protection's required checks list to
+          # propagate strict-gating to merge.
+          exit 1