feat(formal): map challenges to native mutants, require witnesses for every semantic case, and check settlement by receipt

.github/workflows/formal-full.yaml

@@ -147,24 +147,27 @@ jobs:
           if-no-files-found: warn
           retention-days: 14
 
-  # Each mutation lane is sharded over three runners. Every shard compiles,
-  # measures every unmodified baseline and evaluates the witness evidence
-  # itself, then measures a contiguous third of the catalog; the merge job
-  # refuses shards whose fingerprints or baselines disagree, so the merged
-  # report is exactly as strict as one sequential run. The lane was bounded
-  # by sequential mutants: run 34669546872 took 17 minutes unsharded. A shard
-  # runs the baselines (2-4 minutes) plus 4-5 mutants (2-4 minutes each);
-  # doubled for a slow runner that stays under 30.
+  # Each mutation lane is sharded. Every shard compiles, measures every
+  # unmodified baseline and evaluates the witness evidence itself, then
+  # measures a contiguous slice of the catalog; the merge job refuses shards
+  # whose fingerprints or baselines disagree, so the merged report is exactly
+  # as strict as one sequential run. The lane is bounded by sequential
+  # mutants: about 1 minute per TypeScript mutant on a fast runner and about 2
+  # on the slow class (13 mutants took 17 minutes unsharded in run
+  # 34669546872). test/formal-validation.test.ts pins the mutants a shard may
+  # hold so that the baselines (2-4 minutes), the slow-class mutant cost and
+  # one hung cohort's 9-minute bound fit the timeout; growing the catalog past
+  # that fails the pull request until the matrix grows.
   typescript-mutations:
     needs: generate
     runs-on: ubuntu-latest
     strategy:
       fail-fast: false
       matrix:
-        shard: [1, 2, 3]
+        shard: [1, 2, 3, 4, 5, 6]
     env:
-      MUTATION_SHARD: ${{ matrix.shard }}/3
-    timeout-minutes: 30
+      MUTATION_SHARD: ${{ matrix.shard }}/6
+    timeout-minutes: 40
     steps:
       - uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803 # v6.1.0
       - uses: ./.github/actions/setup-validation
@@ -247,22 +250,24 @@ jobs:
           if-no-files-found: warn
           retention-days: 14
 
-  # The Go lane bounded the whole workflow: 13 mutants each replaying the
-  # generated cohort for about 105 s on a fast runner, strictly in sequence.
-  # Run 34660598461 took 25 minutes; runs 34669546872 and 34670045249 took 47
-  # and 48 on the slow runner class. A shard compiles, runs the baselines
-  # (2-4 minutes) and 4-5 mutants (2-4 minutes each); doubled for a slow
-  # runner that stays under 40, and one hung cohort adds its 8-minute test
-  # bound before the shard fails.
+  # The Go lane bounds the whole workflow: every mutant replays the generated
+  # cohort, about 1.6 minutes per mutant on a fast runner and about 3 on the
+  # slow class (13 mutants took 25 minutes in run 34660598461 and 47-48 in
+  # runs 34669546872 and 34670045249), strictly in sequence. A shard compiles,
+  # runs the baselines (2-4 minutes) and its slice of the catalog; one hung
+  # cohort adds its 8-minute test bound before the shard fails.
+  # test/formal-validation.test.ts pins the mutants a shard may hold within
+  # the timeout, so catalog growth fails the pull request until the matrix
+  # grows.
   go-mutations:
     needs: generate
     runs-on: ubuntu-latest
     strategy:
       fail-fast: false
       matrix:
-        shard: [1, 2, 3]
+        shard: [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
     env:
-      MUTATION_SHARD: ${{ matrix.shard }}/3
+      MUTATION_SHARD: ${{ matrix.shard }}/10
     timeout-minutes: 40
     steps:
       - uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803 # v6.1.0

.github/workflows/formal.yaml

@@ -48,11 +48,24 @@ jobs:
   # previous text generated, and vice versa, unless the manifest declares an
   # intended change. The reference is the merge base with the pull request's
   # base branch; a push to main has no reference. The step also checks the
-  # composition lint baseline.
+  # composition lint baseline and the kernel fixtures. A kernel change replays
+  # every composed profile in both directions: six profiles took about 35
+  # minutes on the hosted runner, five about 26, and fourteen in one job
+  # overran the 60-minute budget (57 minutes, then a cancellation at the
+  # timeout), so the lane runs as four matrix shards, each replaying a
+  # round-robin quarter of the profiles sorted by name (DIFFERENTIAL_SHARD);
+  # a change outside the kernel skips unchanged closures in under ten. The
+  # gate is the four statuses `differential (1)` to `differential (4)`; none
+  # is required on main. Grow the matrix, and the count in DIFFERENTIAL_SHARD
+  # with it, before a shard approaches the budget.
   differential:
     if: github.event_name == 'pull_request'
     runs-on: ubuntu-latest
-    timeout-minutes: 30
+    timeout-minutes: 60
+    strategy:
+      fail-fast: false
+      matrix:
+        shard: [1, 2, 3, 4]
     steps:
       - uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803 # v6.1.0
         with:
@@ -63,16 +76,17 @@ jobs:
         run: node .github/scripts/fixture-scope.mjs
       - uses: ./.github/actions/setup-quint
         if: steps.fixture-scope.outputs.recompute == 'true'
-      - name: Replay every composed profile's reference corpus through the pull request's text
+      - name: Replay this shard of the composed profiles' reference corpus through the pull request's text
         if: steps.fixture-scope.outputs.recompute == 'true'
         env:
           DIFFERENTIAL_REFERENCE: origin/${{ github.base_ref }}
+          DIFFERENTIAL_SHARD: ${{ matrix.shard }}/4
         run: make differential
-      - name: Preserve differential reports
+      - name: Preserve this shard's differential reports
         if: always() && steps.fixture-scope.outputs.recompute == 'true'
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
         with:
-          name: formal-differential
+          name: formal-differential-${{ matrix.shard }}
           path: |
             .formal-traces/differential/*/report.json
             .formal-traces/differential/**/replay-*/quint-test.log