ci(nightly): stop the Compiler.Tests property soak running the owner-only MutationCensus (fixes #2392)

.github/workflows/nightly.yml

@@ -37,8 +37,10 @@ jobs:
       fail-fast: false
       matrix:
         include:
+          # Census is the owner-run MutationCensus report: ~87 rows x CsCheck_Time in ONE test, past the
+          # 20 min hang timeout, and it asserts only that it ran (#2392). It also needs SHARPY_CENSUS=1.
           - project: Sharpy.Compiler.Tests
-            filter: "Category=RandomProperty|Category=Property"
+            filter: "(Category=RandomProperty|Category=Property)&Category!=Census"
           # These three have a handful of CsCheck samples, not all tagged, so they run whole.
           - project: Sharpy.Core.Tests
             filter: "Category!=Benchmark"
@@ -51,7 +53,8 @@ jobs:
       # does: every sample that passes no `time:` (none in src/ do) runs for this many seconds.
       # CsCheck picks a fresh seed per run and prints the failing one.
       CsCheck_Time: ${{ inputs.seconds_per_property || '15' }}
-      # The injection lanes sample this many programs instead of 100 (PropertyIterations.cs).
+      # The injection lanes sample this many programs instead of 100 (PropertyIterations.cs). It does
+      # not switch on the mutation census; that takes SHARPY_CENSUS=1, which this job never sets.
       SHARPY_PROPERTY_ITER: '600'
       # The numeric-literal twin fails instead of skipping without a Python 3.12+ oracle.
       SHARPY_REQUIRE_PYTHON_ORACLE: '1'

docs/design/gap-discovery-contracts.md

@@ -56,7 +56,7 @@ deployment closure (`StandaloneDeploymentTests` for the used stdlib closure; `Re
 | Contextual-keyword escape totality (#2166) | A backtick-escaped contextual keyword is an identifier at every site: an escaped soft keyword parses as a fresh identifier would. The predicate "this token is the contextual keyword *k*" is `Identifier ∧ ¬IsBacktickEscaped ∧ Value == k` (`Parser.IsContextualKeyword`) and "this node is the placeholder" is `Identifier { Name: "_", IsNameBacktickEscaped: false }` (`Parser.IsPlaceholder`), over ONE roster (`ContextualKeywords.All`, 13 words) | `ContextualKeywordEscapeSweepTests` (regular suite) — every corpus fixture of `FormatterMeaningPreservationSweepTests` × every unescaped roster-word identifier token at EVERY position (ordinary-identifier positions are the sweep's own green controls, so no position predicate can go stale): the escaped twin (that token in backticks) and the renamed twin (a fresh identifier of the escaped spelling's length, byte-aligned) must have the same `ContextualKeywordEscapeOracle.Outcome` — the parse-diagnostic `(code, line, column)` multiset, else the preorder AST shape (record types + enum-valued properties); one cell per (fixture, token value), census line `CKE-CENSUS`; ratchets `contextual-keyword-escape-allowlist.txt` (`stem token # #issue reason`, drain-on-fix) + `Parser/ContextualKeywordEscapeMatrixTests` — 26 (keyword, site) rows × {bare (construct present), renamed (ground truth), escaped (construct absent, named node kind or parse error, escaped ≡ renamed)} + binding-target/ordinary-read rows for every keyword, roster totality anchored to the literal 13, in-file `KnownRed` drain-on-fix | #2166 |
 | CLI input totality (#2173, #2223) | Every option every `sharpyc` command accepts — its own and the recursive globals — is honoured, refused for that input kind with a message, or documented as ignored in `--help`, never silently dropped; ONE registry (`CommandOptionEffects`, keyed by command path) generates the help notes and refusals, and the globals rule makes a command that compiles honour all nine globals and one that analyses honour the seven analysis-facing ones | `CliOptionEffectSweepTests` — reflective walk of the real root (every leaf command × own + recursive options, `compile` × {.spy, .spyproj}): refused cells are invoked, ignored cells' `--help` text is checked, honoured cells are observed by a named evidence test or a `GlobalOptionProbes` probe run on that command; synthetic-grammar positive controls; allowlist `src/Sharpy.Cli.Tests/cli-option-effect-allowlist.txt` | #2223 |
 | In-process isolation (#2250; P54) | A compile, and every semantic query on its result, is a function of its inputs alone — the same under 1, 2 or 8 concurrent compilations, on a cold or a warm `CompilerApi`, in a fresh or a long-lived process; every CLR name resolves against ONE `AssemblyVisibility` = a process-constant framework index ∪ the assemblies the compilation's own `ModuleRegistry` loaded, into a load context keyed by its reference set (`ReferenceLoadContext`); the master `BuiltinRegistry` is frozen after construction and a user definition never writes a master symbol; a stdlib module global CPython makes thread-safe is read and written under one module lock; a per-event artefact (crash bundle) is created exclusively | `InProcessIsolationSweepTests` (GapDiscovery, its own CI step: corpus × seeded schedule × sharing × threads × {Analyze, Compile}, allowlist `in-process-isolation-allowlist.txt`); `ProcessWideResolutionScanTests` (Roslyn symbol census of every process-wide resolution/load site: roster + drain-on-fix allowlist, literal anchors); `StaticStateConformanceTests` rule 2b (static `ConcurrentDictionary`/`Lazy`/`ConditionalWeakTable` rostered with a key-purity reason; static auto-properties included); `TpaNamespaceGateTests`, `RegistryIsolationTests`, `CompileServerE2ETests.RequestSequence_NoRef_Ref_NoRef…`, `WarmInstanceParityTests` (Lsp) + `MasterRegistryImmutabilityTests` (master symbols frozen, key-set snapshot); `StdlibModuleGlobalRosterTests` (written-after-init census) + `StdlibModuleGlobalConcurrencyTests` (CPython's process-wide model at 1/2/8 threads); `CrashBundleExclusivityTests`; `CliStaticStateConformanceTests` | #2250 |
-| Typed-generator reach and refusal-oracle strength (#2288; P63; #2324; P63b) | Every construct the language spec defines has a roster row stating, per lane, what the typed property generator proves, and every verdict is measured: a generated-lane **Y** means every raw sample of the named generator member contains the construct and some property samples that member with the SAME arguments and consumes an acceptance verdict, an injected-lane **Y** means every applicable sample draws exactly ONE named code at the named severity (or is a pinned known red), and every SPY code a spec file names is claimed by a row of that file or by a cited `UnclaimedSpecCodes` row; a spec file with no row, a row whose anchor heading is gone, and a Y whose generator never emits the construct are red. An injected lane breaks ONE fact of a generated program at a site the mutation generator enumerates from the AST. Every verdict comes from ONE seam (`ErrorInjector.JudgeDiagnostics` fronted by `JudgeSource`/`JudgeProject`/`Judge`, `JudgeClean`/`JudgeNoInternalError`/`JudgeNoDiagnostic`, `IntegrationTestBase.JudgeRun`, and the `SemanticFilter` `RejectionSink`, which records each refused or throwing sample, fails on any rejection no declared pin explains, and names the codes when every sample is refused); a lane outside the seam only CONSUMES verdicts | `TypedGeneratorRosterTests` — universe = directory scan of `docs/language_specification/*.md` minus README (125 files, an exact anchor), literal rows anchored to a `##`/`#` heading, a RAW fixed-seed corpus per Y row (`Generators/Typed/RawCorpus`: generator → Unparser → parser, AST predicate must hit), reflection-checked member labels, the roster ↔ property link by generator ARGUMENT (helpers followed, named arguments placed by parameter) and by a CONSUMED verdict (`PropertySourceIndex.IsConsumed`), `SpecCodes_EveryNamedCodeIsClaimedByARow` (320 (file, code) pairs; cited rows are `new KnownRedSpecCode("#N", …)`, `ProseCrossReference` only to a file that names and claims the code), literal totality anchors, `NoConstruct` only for a file with no Sharpy block of any marker; the mutation generator `Generators/Typed/Mutations/` — `AstRewriter` (reflective immutable-AST replace over init properties, annotations included; `AstRewriterTests` reach-tests every node kind of every typed member's raw corpus), `ProgramFacts` (slot types from the program's own syntax, never the compiler), `MutationSites` (9 positions × families; `MutationSitesTests` pins a literal matrix of cells per base), `PositionMutations`/`DeclarationShapes` (one-fact breaks, site chosen by FNV-1a of the sample), `MutationLanes` (lane × base matrix), `MutationCensus` (opt-in `SkippableFact`, `SHARPY_PROPERTY_ITER`: the drawn-code table per lane × base, inert mutations a bucket of their own); `ErrorInjector.Mutations.cs` — one thin member per lane carrying its ONE code literal, sampled by `ErrorCompletenessPropertyTests` at `PropertyIterations.Injection` (100; the 600-sample census is the close-out record, D1 (a)); `PropertyOracleConformanceTests` — Roslyn syntax rules over every `Properties/Semantic` file and every typed-generator consumer outside the seam: R1 no `catch`, R2 no verdict-surface read (`.Success`/`.HasErrors`/`.IsError`/`.IsWarning`; two runs compared exempt by shape), R3 a code literal / `DiagnosticCodes` member / `.Code` read flows only into the seam (printing a code is legal), R4 no numeric bound in an assertion but `x > 0` and value (in)equality (FluentAssertions included), R5 a seam verdict is consumed, never tested or discarded — per-line positive control of every planted spelling, allowlist drained to 0; one shared pin roster `KnownGeneratorPins` (empty since its #2169 Unparser cell was fixed and drained, R-HP); N/KnownRed rows are `KnownRedRow("#N", …)` so `check_allowlist_issue_state.sh` reddens when a cited issue closes, and the gate accepts only an OPEN issue | #2287 (N-generated: no generator emits the construct; 161 spec-code cites), #2324 (N-injected residue: 3 literal rows + 120 spec-code cites — a typed code in a generated file with no injected lane), #2212/#2143/#2335/#2021/#2363 (KnownRed pins) |
+| Typed-generator reach and refusal-oracle strength (#2288; P63; #2324; P63b) | Every construct the language spec defines has a roster row stating, per lane, what the typed property generator proves, and every verdict is measured: a generated-lane **Y** means every raw sample of the named generator member contains the construct and some property samples that member with the SAME arguments and consumes an acceptance verdict, an injected-lane **Y** means every applicable sample draws exactly ONE named code at the named severity (or is a pinned known red), and every SPY code a spec file names is claimed by a row of that file or by a cited `UnclaimedSpecCodes` row; a spec file with no row, a row whose anchor heading is gone, and a Y whose generator never emits the construct are red. An injected lane breaks ONE fact of a generated program at a site the mutation generator enumerates from the AST. Every verdict comes from ONE seam (`ErrorInjector.JudgeDiagnostics` fronted by `JudgeSource`/`JudgeProject`/`Judge`, `JudgeClean`/`JudgeNoInternalError`/`JudgeNoDiagnostic`, `IntegrationTestBase.JudgeRun`, and the `SemanticFilter` `RejectionSink`, which records each refused or throwing sample, fails on any rejection no declared pin explains, and names the codes when every sample is refused); a lane outside the seam only CONSUMES verdicts | `TypedGeneratorRosterTests` — universe = directory scan of `docs/language_specification/*.md` minus README (125 files, an exact anchor), literal rows anchored to a `##`/`#` heading, a RAW fixed-seed corpus per Y row (`Generators/Typed/RawCorpus`: generator → Unparser → parser, AST predicate must hit), reflection-checked member labels, the roster ↔ property link by generator ARGUMENT (helpers followed, named arguments placed by parameter) and by a CONSUMED verdict (`PropertySourceIndex.IsConsumed`), `SpecCodes_EveryNamedCodeIsClaimedByARow` (320 (file, code) pairs; cited rows are `new KnownRedSpecCode("#N", …)`, `ProseCrossReference` only to a file that names and claims the code), literal totality anchors, `NoConstruct` only for a file with no Sharpy block of any marker; the mutation generator `Generators/Typed/Mutations/` — `AstRewriter` (reflective immutable-AST replace over init properties, annotations included; `AstRewriterTests` reach-tests every node kind of every typed member's raw corpus), `ProgramFacts` (slot types from the program's own syntax, never the compiler), `MutationSites` (9 positions × families; `MutationSitesTests` pins a literal matrix of cells per base), `PositionMutations`/`DeclarationShapes` (one-fact breaks, site chosen by FNV-1a of the sample), `MutationLanes` (lane × base matrix), `MutationCensus` (opt-in `SkippableFact`, `SHARPY_CENSUS=1` with `SHARPY_PROPERTY_ITER` samples per row: the drawn-code table per lane × base, inert mutations a bucket of their own); `ErrorInjector.Mutations.cs` — one thin member per lane carrying its ONE code literal, sampled by `ErrorCompletenessPropertyTests` at `PropertyIterations.Injection` (100; the 600-sample census is the close-out record, D1 (a)); `PropertyOracleConformanceTests` — Roslyn syntax rules over every `Properties/Semantic` file and every typed-generator consumer outside the seam: R1 no `catch`, R2 no verdict-surface read (`.Success`/`.HasErrors`/`.IsError`/`.IsWarning`; two runs compared exempt by shape), R3 a code literal / `DiagnosticCodes` member / `.Code` read flows only into the seam (printing a code is legal), R4 no numeric bound in an assertion but `x > 0` and value (in)equality (FluentAssertions included), R5 a seam verdict is consumed, never tested or discarded — per-line positive control of every planted spelling, allowlist drained to 0; one shared pin roster `KnownGeneratorPins` (empty since its #2169 Unparser cell was fixed and drained, R-HP); N/KnownRed rows are `KnownRedRow("#N", …)` so `check_allowlist_issue_state.sh` reddens when a cited issue closes, and the gate accepts only an OPEN issue | #2287 (N-generated: no generator emits the construct; 161 spec-code cites), #2324 (N-injected residue: 3 literal rows + 120 spec-code cites — a typed code in a generated file with no injected lane), #2212/#2143/#2335/#2021/#2363 (KnownRed pins) |
 | Numeric-literal fidelity (#2300 C1; P68; cells #2339) | A numeric spelling in the grammar Sharpy shares with CPython is ONE constant with CPython's value (BigInteger for ints, IEEE bits for floats) or refused by both, judged at the program altitude (`ast.parse` constant), not at the token altitude; the Sharpy-only syntax (suffix roster, `j`, trailing-dot floats) is excluded only by a literal table citing the spec sentence, and every excluded row is pinned to Sharpy's own verdict | `NumericLiteralTwinTests` (regular suite) — form × separator placement × exponent × following character (49,432 spellings) against batched `build_tools/differential_lex/number_oracle.py` through ONE locator (`Sharpy.TestInfrastructure/Oracles/PythonInterpreter`, required under `SHARPY_REQUIRE_PYTHON_ORACLE=1` in CI); `SharpyOnlyRows_LexAsTheSpecSays` (83 hand rows); ratchet `Lexer/numeric-literal-twin-allowlist.txt` (`01`, `0_1` — the leading-zero DEVIATION-by-default cell, ruled at `/batch-issues`) | #2300 |
 | Token position and line-ending totality (#2300 C2/C3/C6; P68; cells #2338) | Every token's `(Line, Column, Position, length)` names its own source slice (R1–R7 of `TokenPositionReconstruction`), and tokens, diagnostics and line facts are invariant under LF / CRLF / lone CR and a present / absent / doubled trailing newline | `LexerCorpusTwinTests` — every fixture × 9 twins (≈3.56 M tokens) through `Sharpy.TestInfrastructure/Lexing/TokenPositionReconstruction` (its own R-rule positive controls in `TokenPositionReconstructionTests`; P67 extends it with AST node ends, #2295); `EofConstructRosterTests` — 142 constructs (totality over operator/delimiter `TokenType`s) × 7 endings, no exception escapes; shared ratchet `Lexer/lexer-position-allowlist.txt` (rows cite #2338). Instrument limit: `FStringText`/`FStringFormatSpec`/`FStringConversion` carry no `SourceLength`, so their slice is read as the gap to the next token | #2300 #2338 |
 | Literal-loss scanner agreement (#2300 C5; P68) | On text recovery drops, the literal-loss scanner's facts (opener crossing, continuation, open bracket, header colon, field state) equal the clean lexer's facts for the same lines | `LiteralLossScannerDifferentialTests` — `Injected_ScannerAgreesWithTheCleanLexersFacts`: the corpus prefix through line k × 4 error constructs (`$`, bad escape, bad conversion, tab indent) + backtick / escaped-quote / field-split / unbalanced-brace clean twins (≈284 k cells), against the clean-lexer oracle (`.CleanFacts.cs`); `Shapes_LexerFactsMatchTheirConstructionKnownTruth` — the P22 shape builders over every fixture; ratchet `Lexer/literal-loss-scanner-allowlist.txt` (0 rows) | #2300 (#2274 known limits) |

src/Sharpy.Compiler.Tests/Properties/Generators/Typed/Mutations/MutationCensus.cs

@@ -9,13 +9,14 @@ namespace Sharpy.Compiler.Tests.Properties.Generators.Typed;
 
 /// <summary>
 /// The drawn-code table (#2324, P63b Phase 1 Task 4): for every (lane, base) row of
-/// <see cref="MutationLanes.Census"/>, <see cref="PropertyIterations.Override"/> well-typed samples of the
+/// <see cref="MutationLanes.Census"/>, <see cref="PropertyIterations.Injection"/> well-typed samples of the
 /// base (through <see cref="SemanticFilter.WellTypedProgram"/> with a sink), the lane's break applied,
 /// the result analysed through <see cref="PropertyAnalysis.Codes"/>, and the codes bucketed. It is a
 /// REPORT, not a guard: it decides nothing and asserts only that it ran. A lane is wired in
 /// <c>ErrorInjector.Mutations.cs</c> with the code its row draws at ≥ 99 %; two codes is a bad injection
 /// or a cascade cell; CLEAN is a by-design candidate or a missing refusal; a throw is an ICE cell. Runs
-/// only when <see cref="PropertyIterations.Variable"/> is set (skipped in the suite and the gate); set
+/// only when <see cref="PropertyIterations.CensusVariable"/> is <c>1</c> (skipped in the suite, the gate and the
+/// nightly soak, which raises <see cref="PropertyIterations.Variable"/> but must not run this, #2392); set
 /// <c>SHARPY_CENSUS_OUT</c> to a file path to keep the table (appended row by row) and <c>SHARPY_CENSUS_FILTER</c> to run a chunk.
 /// </summary>
 [Trait("Category", "Property")]
@@ -33,8 +34,9 @@ public MutationCensus(ITestOutputHelper output)
     [SkippableFact]
     public void DrawnCodes_PerLaneAndBase()
     {
-        Skip.IfNot(PropertyIterations.Override is not null, $"set {PropertyIterations.Variable} to run the mutation census");
-        var iter = PropertyIterations.Override!.Value;
+        Skip.IfNot(PropertyIterations.CensusRequested,
+            $"set {PropertyIterations.CensusVariable}=1 (and {PropertyIterations.Variable} for the sample count) to run the mutation census");
+        var iter = PropertyIterations.Injection;
         // SHARPY_CENSUS_FILTER: '|'-separated substrings of "Lane @ Base" (a chunk of the matrix — a whole
         // 600-sample census outruns the dotnet wrapper's silence watchdog, so it runs in chunks).
         var filters = (Environment.GetEnvironmentVariable("SHARPY_CENSUS_FILTER") ?? "")