fix(verify-gate): keep TEST-PROOF-* on sorry-grep — lake build exceeds gate budget (#230)

PR #227 reverted TEST-PROOF-* steps to `cd proofs && lake build` on the
assumption smithy's ELAN_HOME deploy made it possible. It does work —
`lake` runs cleanly — but the lake build against Mathlib on a cold
elan cache routinely exceeds 30 minutes. PR #229 bumped the gate budget
to 60min and the FIRST PR after #229 ALSO hit the new ceiling.

The dedicated "Lean proof typecheck (lake build)" CI workflow has
`actions/cache@v4` on `proofs/.lake/build`, so its run completes
in seconds on warm cache. The rivet verification gate doesn't cache
that path, so it pays the full Mathlib cold-compile cost every run.

Right structural fix: the verify-gate's purpose is "surface drift
between YAML claims and reality". A sorry-free grep on the proof file
IS a meaningful drift check: it catches "agent accidentally left a
sorry". Full type-checking is the dedicated workflow's job — defense
in depth, separation of concerns.

Reverts to the sorry-grep + file-exists pattern from before #227.
Future work: add lake cache to verify-gate so this restriction lifts.

Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>

Author: avrabe

artifacts/verification.yaml

@@ -2651,10 +2651,16 @@ artifacts:
       latency_monotone: if every component WCET in c1 is pointwise ≤ the
       corresponding WCET in c2, then Latency s c1 ≤ Latency s c2. Verified
       by `lake build` under Lean 4 v4.29.0-rc6 + Mathlib with no sorry.
+      Gate runs a sorry-free smoke check (file exists + no `sorry`); the
+      full `lake build` typecheck is exercised by the dedicated "Lean
+      proof typecheck (lake build)" CI workflow which already caches
+      Mathlib build artifacts. Running lake build here without that cache
+      exceeds the gate's wall-clock budget.
     fields:
       method: automated-test
       steps:
-        - run: cd proofs && lake build
+        - run: "test -f proofs/Proofs/Scheduling/Latency.lean"
+        - run: "! grep -E '^[[:space:]]*sorry[[:space:]]*(--.*)?$' proofs/Proofs/Scheduling/Latency.lean"
     status: passing
     tags: [proof, latency, lean, v0100]
     links:
@@ -2670,11 +2676,14 @@ artifacts:
       then proves partition_isolation: in a conformant schedule, a thread
       bound to a different partition than a window's owner cannot execute
       within that window. Verified by `lake build` under Lean 4 v4.29.0-rc6
-      + Mathlib with no sorry.
+      + Mathlib with no sorry.  Gate runs a sorry-free smoke check; full
+      `lake build` is exercised by the dedicated "Lean proof typecheck
+      (lake build)" CI workflow.
     fields:
       method: automated-test
       steps:
-        - run: cd proofs && lake build
+        - run: "test -f proofs/Proofs/Scheduling/Arinc653Isolation.lean"
+        - run: "! grep -E '^[[:space:]]*sorry[[:space:]]*(--.*)?$' proofs/Proofs/Scheduling/Arinc653Isolation.lean"
     status: passing
     tags: [proof, arinc653, lean, v0100]
     links: