amadan
sim: hostlife: mutate.sh learns the rare-at-depth outcome; hostguard, stale-hold-release and strict-spawn are caught at 30,000
The admitting CAS ahead of the start moved three rules below the 3,000-seed line (hostguard 2 / 30,000, stale-hold-release 15 / 30,000, strict-spawn 1 / 30,000 on rev 7.11). None has a witness of its own (strict-spawn's belongs to its combination), so expected-outcomes.txt gains `rare <N>`: below N a miss is expected, at N or more it is MISSED, and a catch is never STALE. The three box-side fences leave the file: start-check-claim-gen is caught alone again, so the triple is too.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
2 files changed,
+14
−4
internal/sim/hostlife/expected-outcomes.txt+6 −2internal/sim/hostlife/mutate.sh+8 −2
diff --git a/internal/sim/hostlife/expected-outcomes.txt b/internal/sim/hostlife/expected-outcomes.txt| index a5b6c00b1..72504e3d2 100644 |
| --- a/internal/sim/hostlife/expected-outcomes.txt |
| +++ b/internal/sim/hostlife/expected-outcomes.txt |
| @@ -2,7 +2,9 @@ |
| # expected to be caught alone, by the random sweep or by its witness |
| # (witness_test.go), and is reported EXPECTED-MISS; the sweep fails if it |
| # is caught (the expectation is stale). Spec §14.2.5 gives the |
| -# combination that catches each, or why none does. |
| +# combination that catches each, or why none does. A rule listed `rare N` |
| +# has no witness and the random sweep reaches it only at N seeds or more |
| +# (rev 7.11); below N its miss is expected. |
| claim-cas-opid missed caught with revalidate-before-effect |
| config-before-probe missed liveness only: a target that cannot render config fails its probe and rolls back |
| readiness-key missed liveness only: T2 avoids a pointless cut |
| @@ -16,4 +18,6 @@ door-by-version missed subsumed by C3a and, since rev 7.8, by writer epochs (cla |
| registration-check missed a cheap extra: subsumed by purge-claim-fence and fence-etag together |
| exec-writer missed one of four admission fences (claim rev 6.8.1): the AdmitWriter CAS refuses a box that is not op.exec; caught with exec-admission, hold-op-open and start-check-claim-gen (witness) |
| admit-bind-op missed caught with claim-cas-opid: the model's general CAS condition on op.id (C2) already refuses a closure whose operation changed; the binding adds the phase and the kinds in which no writer opens, and its witness needs both gone |
| -exec-admission,hold-op-open,start-check-claim-gen missed the three box-side fences alone (rev 7.5's admission triple): under writer sessions the old source's wake has no certificate for the current session, and the AdmitWriter CAS alone refuses a box that is not op.exec (claim rev 6.8.1, exec-writer); the four-rule combination with exec-writer is the one that fails |
| +hostguard rare 30000 the guard's race is reached by the sweep at 30,000 (2 / 30,000 on rev 7.11; 5 / 3,000 on rev 7.10, before the admitting CAS moved ahead of the start) |
| +stale-hold-release rare 30000 reached at 30,000 (15 / 30,000 on rev 7.11; 2 / 3,000 on rev 7.10) |
| +strict-spawn rare 30000 its witness holds alone (the combination with evidence-whole-tree is the witness's); the sweep reaches it at 30,000 (1 / 30,000 on rev 7.11; 3 / 3,000 on rev 7.10) |
diff --git a/internal/sim/hostlife/mutate.sh b/internal/sim/hostlife/mutate.sh| index c4ff0590c..c583d97f5 100755 |
| --- a/internal/sim/hostlife/mutate.sh |
| +++ b/internal/sim/hostlife/mutate.sh |
| @@ -34,8 +34,11 @@ |
| # Expected outcomes live in expected-outcomes.txt beside this script: a |
| # rule listed there as `missed` (liveness-only, unreachable, or caught |
| # only in a stated combination: its witness holds alone) is reported as |
| -# EXPECTED-MISS. The sweep exits nonzero on any ERROR, on any unexpected |
| -# MISSED, and on any rule listed as `missed` that is CAUGHT (STALE). |
| +# EXPECTED-MISS. A rule listed as `rare <N>` (rev 7.11) has no witness |
| +# and is caught by the random sweep only at N seeds or more: below N a |
| +# miss is EXPECTED-MISS and a catch is CAUGHT; at N or more a miss is |
| +# MISSED. The sweep exits nonzero on any ERROR, on any unexpected MISSED, |
| +# and on any rule listed as `missed` that is CAUGHT (STALE). |
| # |
| # Scratch (the binary, every run's log, the verdicts) lives under |
| # ${HOSTLIFE_SCRATCH:-$TMPDIR/hostlife-sim}; remove it once, after the |
| @@ -80,6 +83,7 @@ one() { |
| HOSTLIFE_MUTATE=$r HOSTLIFE_SEEDS=$SEEDS "$BIN" -test.run '^TestHostLifecycle$' -test.count=1 -test.v -test.timeout 180m >"$log" 2>&1 |
| rc=$? |
| expect=$(awk -v r="$r" '$1==r {print $2}' "$PKG/expected-outcomes.txt" 2>/dev/null) |
| + depth=$(awk -v r="$r" '$1==r {print $3}' "$PKG/expected-outcomes.txt" 2>/dev/null) |
| nviol=$(grep -o "[0-9]* of $SEEDS seeds violated an invariant" "$log" | head -1 | awk '{print $1}') |
| seed=$(grep -o "first seed [0-9]*" "$log" | head -1 | awk '{print $3}') |
| clean=$(grep -c "^ sim_test.go:[0-9]*: $SEEDS seeds, 0 failed.*mutated=\"$r\"" "$log") |
| @@ -131,6 +135,8 @@ one() { |
| fi |
| elif [ "$expect" = "missed" ]; then |
| echo "EXPECTED-MISS $r: $sweep; witness $wit" | tee "$verdict" |
| + elif [ "$expect" = "rare" ] && [ -n "$depth" ] && [ "$SEEDS" -lt "$depth" ]; then |
| + echo "EXPECTED-MISS $r: $sweep; witness $wit (rare: caught at $depth seeds)" | tee "$verdict" |
| else |
| echo "MISSED $r: $sweep; witness $wit" | tee "$verdict" |
| fi |