refactor: run the gate's verification with Effect

[Sequela02]

Second part of moving Tesota's coordination code to Effect 4 (after #486): the gate's verification.

What a stop did

Measured on Windows with a scratch script running the real gate on the engine, a check whose test script starts a process of its own and waits a minute, stopped once both run: the run ended 1.3-1.5 s after the stop, and the gate's handler finished at the same moment. runProcess alone stops that tree (Git's bash, npm, node and its child) in about 200 ms, and taskkill /T takes about 190 ms. So the gate went on working for over a second after the stop, building evidence for a receipt.

Change

• settle, prove and measure are Effect.gen programs, one step per stage and per file, run with Effect.runPromise(…, { signal }). The stop interrupts between steps: no later step starts and no later progress is published. The gate no longer threads ctx.signal ?? new AbortController().signal through its stages.
• step runs each stage: on interruption it aborts the stage's signal and waits for it, so a check's processes or Dafny's have stopped before the gate reports. The first version used Effect.promise, which does not wait; measured, the run then ended in 8 ms with both processes still alive.
• A stop during verification settles with the receipt a stop before verification gives, now with "the operator stopped the run while Tesota verified it" and no evidence, as the owner chose. One function, stopped, builds both.
• docs/concepts/verification.md and docs/guides/receipts.md say what a stop during verification does.

Checks

• Stop during that check, four runs each:

  	Before	After
  Stop to run end	1,286-1,524 ms	211-240 ms
  The check's process and its child	gone	gone

• New test in packages/core/tests/gate.test.ts: a stop while a project's check runs ends the run aborted, with the stopped receipt, and with both processes the check started gone. It fails on the gate before this change.

• Gate tests: root 48 passed, engine 35 passed.

• bun run check locally: root 264 passed; engine 320 passed, 3 skipped; lint and types clean. The budget fails on shell memory (115.6 MB, limit 115 MB), this machine's noise (Windows first-frame budget fails on runner noise #462); CI decides.