ci(missions-comparator): raise the stack limit before the judge (nanoda overflow on KWin certificates)

.github/workflows/missions-comparator.yml

@@ -206,6 +206,14 @@ jobs:
         run: |
           set -uo pipefail
           echo "lean4export = $COMPARATOR_LEAN4EXPORT ; nanoda = $COMPARATOR_NANODA"
+          # Stack (2026-09-24, #615 run 36055910789): nanoda's kernel is recursive and the KWin
+          # artifacts carry large `decide +kernel` LDL^T certificates; replaying them overflowed
+          # the 8 MB MAIN-thread stack ("thread 'main' has overflowed its stack", exit 134).
+          # RUST_MIN_STACK only sizes spawned threads, so raise the process limit here; the
+          # comparator's children (lean4export, nanoda) inherit it. Fall back to 4 GB if the
+          # runner's hard limit refuses unlimited; never let the fallback itself fail the job.
+          ulimit -s unlimited 2>/dev/null || ulimit -s 4194304 2>/dev/null || echo "::warning::could not raise the stack limit (ulimit -s); large certificates may overflow nanoda"
+          echo "stack limit (KB): $(ulimit -s)"
           fail=0; pass=0
           {
             echo "## missions-comparator: ${{ matrix.island }} shard ${{ matrix.shard }} (run ${{ github.run_id }})"

telperion/docs/AUDIT_INDEPENDENCE_2026-09-23.md

@@ -90,7 +90,11 @@ on a GitHub-hosted runner from a clean checkout. It is **not** independent of th
 vocabulary: the registered statement is elaborated in the artifact's own namespace and
 `open` context on the island, not against the campaign's vocabulary mirror
 (`Statements.RHDefs`, `MMDefs`), because the Comparator needs both sides in one Lake
-workspace. Whether the mirror still matches the island is `missions/mirrors.py` and the
+workspace. The judge step raises the process stack limit (`ulimit -s unlimited`, 4 GB
+fallback) before invoking the Comparator: nanoda replays proofs recursively and the large
+`decide +kernel` certificates of the KWin artifacts overflowed the 8 MB main-thread stack
+(#615, run 36055910789); a stack overflow is a runner limit, not a verdict, and the job
+says so. Whether the mirror still matches the island is `missions/mirrors.py` and the
 islands' `generate.py --check` jobs. Whether the island's `DBN.H` is the de Bruijn-Newman
 `H` is the read-back's job. The judge closes the gap between the two: given the vocabulary,
 the artifact proves this proposition and nothing weaker.