Repository navigation
Merged
Conversation
… fails is a recorded failure, not a skipped comparison; the fact asserts compared == admitted (refs #2288) Verify finding F1 (live cell): ValidatorOrderingPropertyTests returned null from ValidateWith on a re-analysis throw (`catch { return null; }`) or failure (the multi-line `if (!analysis.Success || ...)` that evaded the line-based scan), and the caller returned/continued, so a re-analysis that failed on every sample left the fact green with "0/30 programs compared". ValidateWith now reports why (`out failure`), the caller records it on a failure queue asserted empty, a throw propagates and fails the sample, and the fact asserts total > 0 and compared == total. mutation M1 (ValidateWith always returns null): broken -> red (1 failed: "30 admitted program(s) did not re-analyse clean ... reference run: mutation M1"), restored -> green (18 passed, filter ValidatorOrdering|JudgeSourceTests|Roster.YInjected). Commit state: ValidatorOrdering + PropertyOracleConformance + TypedGeneratorRoster + ProcessGlobalStateConformance 43/0/0 (measured). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017D8V5muKcTsUwCKAHghw1h
…he NeverThrows lanes judge every raw sample for a throw or SPY0909, the span/async/determinism/CFG lanes stop catching, and the differential sweep's generated arm records what it refuses and must reach its target (refs #2288) Verify finding F2 (the oracle matrix did not drain to one kind): - ClassInheritance/FunctionSemantics/TypedAnalyze `*_NeverThrowsInternalError` caught only InternalCompilerErrorException, which Analyze never lets escape (the last-chance handler records SPY0909), and swallowed every other exception: they could not fail. They now judge each raw sample through the new ErrorInjector.JudgeNoInternalError (null unless the analysis throws or records SPY0909; a refusal is allowed, the sample is unfiltered) via JudgeSamples, asserting Tested > 0 and no failure. - DiagnosticSpan x3 and Async `AsyncFunction_Deterministic` lose `catch { /* swallow */ }`; Determinism's Compile/CompileFull lose their throw-to-sentinel catches and TypedCompilation_ProducesIdenticalCSharp fails when an ADMITTED program produces no C# instead of skipping the comparison; CfgWellFormedness (same universe, same shape) loses its catch-all, so a throw from compile, re-parse or the CFG builder fails the sample (a refused random program is still skipped — the untyped generator's programs are not well typed). - DifferentialExecutionTests' generated arm (a GapDiscovery sweep, trait and fixed-size arm kept): a candidate Sharpy refuses or throws on is recorded on a RejectionSink through the new SemanticFilter.AdmitWellTyped (WellTypedProgram's admission rule for one sample, without the forced GC — the class is not in a serial collection), an admitted candidate whose re-parse fails or throws is a recorded failure, only the subset filter discards, and AssertGeneratedArmSound requires no unexplained rejection, no failure and Programs == Target. A new fact GeneratedArm_DropsNothingSilently_AndReachesItsTarget guards the arm without the CPython oracle (the sweep's fact returns early when python3 is absent). - ClassInheritance's super-call counter is renamed superCallsTested (an applicability counter, for the scanner's lower-bound rule in the next commit). mutation M7 (production, src/Sharpy.Compiler/Compiler.cs: throw at the start of Analyze and of Compile): broken -> red (12 failed of 12: the 3 NeverThrows, DiagnosticSpan x3, Determinism x3, CfgWellFormedness, Async determinism, GeneratedArm), restored -> green. mutation M8 (production, ControlFlowValidator.VisitFunctionDef throws on `main` -> SPY0909, no exception escapes): broken -> red (3 failed of 3 NeverThrows: "100/100 typed programs crashed the compiler ... SPY0909"); control: the BASE NeverThrows lanes (git show HEAD versions) under the same mutation -> green (3 passed) — the old lanes were vacuous; restored -> green. Commit state: the touched classes + DifferentialExecution (sweep included) + PropertyOracleConformance + TypedGeneratorRoster + ProcessGlobalStateConformance 73/0/0 (measured). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017D8V5muKcTsUwCKAHghw1h
…KnownRedRefusal("#2212", …)` so the issue-state gate reads its cite; the JudgeSource probe pin cites no issue (refs #2288, refs #2212)
Verify finding F5: ErrorInjector's ExplicitInstantiationConstraintPin was target-typed
(`new("#2212", …)`), invisible to KNOWNRED_CELL_RE (`new\s+\w*KnownRed\w*\s*\(\s*"#?(\d+)"`),
so #2212 closing without the pin draining would leave /push green. JudgeSourceTests' probe
pin cited "#2288" (also target-typed, invisible), which would read as a stale cite once
#2288 closes; it is "probe-pin" now — no `#<digits>`, never a cite.
Gate rows (allowlist_issue_state.scan over the two files): at the base, 2 rows (the two
#2143 pins); now 3 — `ErrorInjector.cs:722 [2212]` added; JudgeSourceTests none either way.
mutation M-H6 (the pin's cite -> "#2250", a CLOSED issue): broken -> red
(`python3 build_tools/allowlist_issue_state.py --paths ErrorInjector.cs` exit 1:
"ErrorInjector.cs:722 ... → #2250 CLOSED"), restored -> green (exit 0).
Commit state: JudgeSourceTests + ErrorCompleteness + PropertyOracleConformance 37/0/0
(measured); issue-state gate over ErrorInjector/JudgeSourceTests/KnownGeneratorPins exit 0.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017D8V5muKcTsUwCKAHghw1h
…ing diagnostic carrying the code and no error, not one distinct warning code (refs #2288) Verify finding F6 / plan Design Decision 6 ("exactly one diagnostic of the expected severity with the expected code, and no error"): JudgeDiagnostics compared DISTINCT warning codes, so two SPY0463 warnings (two broken facts) collapsed to one code and passed. The arm now counts warning diagnostics (`warningDiagnostics == 1`) beside the distinct-code check; the refusal message prints the count. Two JudgeSourceTests cells: two non-exhaustive matches -> refused ("warnings [SPY0463] (2 warning diagnostic(s))"); the warning beside an unrelated SPY0450 (a statement after `return`) -> refused (already refused before, now pinned). Measured first that the two warning lanes carry exactly one such diagnostic per sample under the stricter arm: MatchNonExhaustive 50/50 drew SPY0463, UnusedImportProgram 20/20 drew warning SPY0452 (PatternMatch/ImportResolution green). mutation M2 (`warningDiagnostics == 1` -> `>= 1`, i.e. one distinct code again): broken -> red (1 failed: WarningArm_TwoOfTheExpectedWarning_IsRefused), restored -> green. Commit state: JudgeSourceTests + PatternMatch + ImportResolution + PropertyOracleConformance 27/0/0 (measured). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017D8V5muKcTsUwCKAHghw1h
… it — a YInjected row to a refusal lane naming its member and code, a Y row's member to an acceptance verdict, a Y label to the member its generator calls (refs #2288) Verify finding F3: the roster's lane claims were a hand model checked only for member resolution and `^SPY\d{4}$`; a code, a deleted soundness fact or a label/lambda mismatch drifted green. PropertySourceIndex (new, Roslyn) indexes every method of Properties/** outside the roster and Generators/Typed/ (its X.Y references, string literals, same-file calls and their closure). Three facts: (a) YInjected_RowsAreBackedByTheirRefusalProperty — a generator-member row needs a property method naming the member AND the code literal in ONE body whose closure names CompilerDiagnosticSeverity.<row severity> and reaches ErrorInjector.Judge/JudgeSource/ JudgeProject; an ErrorInjector row needs the injector's own body to draw exactly that code (its only code literal; a Warning severity named iff the row is a warning) and a property method referencing it whose closure reaches ErrorInjector.Judge. All 32 rows checked. (b) YGenerated_RowsAreBackedByAnAcceptanceProperty — every Y member is referenced by a property method whose closure reaches an acceptance verdict from the named set: SemanticFilter. {WellTypedProgram, CompilableProgram, WellTypedSource, CompilableProject, AdmitWellTyped}, ErrorInjector.JudgeClean, PropertyCorpus.AssertAllPassOrAllowed with allowedCodes null, VariancePropertyTests.AssertEverySampleIsDiagnosticFree, and Assert.Equal(x.Total, x.Passed). (c) YGenerated_LabelIsTheMemberItsGeneratorCalls — each `new Y("Label", () => …)` lambda calls (or passes as a method group) exactly one generator method, the label, following the roster's consumer-argument helpers; the syntax count equals ExpectedYGenerated (103). mutation M3 (roster: the await-outside-async row's "SPY0273" -> "SPY0274"): broken -> red (1 failed, (a): "no property method names the member and \"SPY0274\" in one body …"), restored -> green. mutation M4 (FStringPropertyTests.FString_WithFormatSpecs_CompilesClean deleted, on disk): broken -> red (1 failed, (b): "GenFStrings.FStringWithFormatSpecs: no property method samples it and reaches an acceptance verdict"), restored -> green. mutation M5 (the UnaryOperatorProgram row relabelled "GenOperators.BinaryOperatorProgram"): broken -> red (1 failed, (c): "line 768: label 'GenOperators.BinaryOperatorProgram', the generator calls [GenOperators.UnaryOperatorProgram]"), restored -> green. Commit state: TypedGeneratorRoster + PropertyOracleConformance + ProcessGlobalStateConformance 45/0/0 (measured). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017D8V5muKcTsUwCKAHghw1h
…alized token stream, not lines, and bans the verify round's evasions — parenthesized/multiplied thresholds, lower bounds on any non-applicability counter, code literals compared outside the seam, a HasErrors verdict, and a catch that swallows what the pipeline threw (refs #2288) Verify finding F1 (instrument): PropertyOracleConformanceTests matched six regexes per LINE, so `!analysis.Success` / `|| …` split over two lines evaded it (the live ValidatorOrdering cell, drained in bd313602f), and eleven measured spellings passed. Now: - Unit: the banned regexes run over the file's token stream with every trivia run (whitespace, newlines, comments) collapsed to one space (Roslyn), so a split spelling is one statement's text and a comment is never a hit; a hit reports the line of its first token and its enclosing statement. - threshold: also `> (total / 2)`, `passed * 2 > total`, `2 * passed > total`, `total / 2 < passed` (a multiplied counter compared with a literal, `x * 2) > 2`, and a relative tolerance `/ av) <= RelTol` are benign look-alikes). - lower-bound: inside any Assert, `x > 0`, `x >= 1`, `x != 0` (either side) and Assert.NotEmpty(x) on any counter except the applicability counters — names ending (case-insensitively) in tested, total, admitted, compared, injected, programs; for .Count/.Length the receiver's name. Renamed to fit: narrowed -> narrowedTested (ErrorCompleteness), RowsChecked -> RowsTested (roster); Differential's `results.Count > 0` becomes `results.Count == programs.Count` (every program classified; non-emptiness is the corpus assert above it). superCallsTested landed in c37894748. - any-failure: also `if (!r.Success) count++` with no throw/assert in the branch. - code-literal (new): a SPY code literal passed to Equal/Contains/Equals/StartsWith/… or compared with == / != against something that is not `.Code` (that is code-compare's spelling); the seam's own `JudgeSource(src, "SPY0273", …)` and `new InjectionResult(m, "SPY0220")` stay benign. - has-errors (new): `.HasErrors` asserted true, or counted by an if with no throw/assert. - swallow-catch (new): a catch whose try reaches the pipeline under test (Analyze, Compile, CompileAndExecute, CompileToCSharp, Unparse, ParseModule, TokenizeAll, Validate, Judge*; or new Compiler/Parser/Lexer/ControlFlowGraphBuilder/ProjectCompilationHelper) and whose body neither throws, asserts, calls a record verb (Add, AddRange, Enqueue, TryAdd, Reject, Exclude, Fail, Record) nor returns/assigns a message string or the caught exception. A catch around the CPython oracle's process management does not reach the pipeline and is not judged. The allowlist stays at 0 rows: c37894748/bd313602f drained every hit; no legitimate hit needed a rule beyond the documented ones above. Positive control: 38 hits = prefix 1, threshold 9, lower-bound 6, any-failure 3, two-bucket 1, catch-increment 2, code-compare 5, code-literal 5, has-errors 2, swallow-catch 4; every benign look-alike (now incl. the applicability floors, the seam's code literals, Assert.False(HasErrors), recording catches, a pipeline-free catch) draws none; the split any-failure and threshold are reported at their first token's line. mutation S8/M6 (ValidatorOrdering re-typed with `if (!analysis.Success` / `|| analysis.Module is null) return null;` split over two lines, on disk): broken -> red (1 failed: "ValidatorOrdering PropertyTests.cs has 1 [any-failure] hit(s) (lines 198)"), restored -> green (4 passed). Commit state = the round's final tree: edit loop Properties.Semantic|Census|Conformance|Roster| Infrastructure|Properties.CodeGen|DifferentialExecution 18011/0/0 (measured, DifferentialExecution sweep included). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017D8V5muKcTsUwCKAHghw1h
…grams through the sink and must check a CFG from every admitted program — it checked 0 CFGs from 50 programs and passed (refs #2288) Hardening ledger row (cfgsChecked printed, never asserted). Measured first: with only an applicability floor added, the lane went red at once — "0 CFGs checked from 50 programs". The untyped GenSharpy.Module generator never produced a compiling program with a top-level function, and the lane skipped every refused program, so no CFG had ever been built by it. Now the lane samples GenFunctions.ModuleWithFunctions(TypeEnv.Default, "int", fuel: 2) through SemanticFilter.CompilableProgram with a RejectionSink (asserted no unexplained rejection; the #2169 Unparser cell is the one pin), throws when an admitted program has no FunctionDef, and asserts cfgsTested > 0. Measured: 152 CFGs from 50 programs, rejections 3/53 (pinned #2169 ×3, unexplained 0); restored run 147 CFGs, 5/55 all pinned. mutation M-skip (test: every FunctionDef skipped): broken -> red (1 failed: "ModuleWithFunctions drew a module without a function"), restored -> green. mutation M-prod (production, ControlFlowGraphBuilder.Connect drops `to.AddPredecessor(from)`): broken -> red (1 failed: "Successor BB2:body_start of BB0:entry is missing matching predecessor edge"); control: the PRIOR lane (HEAD version) under the same mutation -> green ("0 CFGs checked from 50 programs") — the old lane could not fail; restored (cp + touch, cmp-verified) -> green. Commit state: CfgWellFormedness + PropertyOracleConformance + ProcessGlobalStateConformance + TypedGeneratorRoster 46/0/0 (measured). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017D8V5muKcTsUwCKAHghw1h
… are recorded failures — TypeSoundness's two execution lanes no longer filter run failures by four .NET exception names, and OverloadOrderIndependence no longer compares a caught throw as a signature (refs #2288) P63 verify round (sibling-cell prober K1, plan oracle-matrix kinds "filtered" / "no-throw"). TypedProgram_ExecutesWithoutRuntimeTypeErrors and TypedProgram_WithCollections_… recorded a failed run only when stderr named InvalidCast/NullReference/InvalidOperation/ArrayTypeMismatch; every other failure (a Sharpy runtime error, an ArgumentException, a Roslyn emit failure with empty stderr) was admitted silently — dd4ca1e cured only FilteredTypedProgram. Both now record every failed run, as FilteredTypedProgram does. ResolutionSignature caught any compiler throw and returned "THREW:<type>", so a throw identical in every declaration order compared equal and passed (the shape H2 cured in DeterminismPropertyTests); the throw now propagates and fails the sample. Measured: TypeSoundness 4/4, OverloadOrderIndependence 1/1 green @ this tree (no admitted sample fails to run; no throw). Mutations (worktree @ f10b838 + this patch, restored by cp + touch): - MB: Builtins.PrintWithOptions throws ArgumentException → TypeSoundness red (3 failed: both execution lanes + FilteredTypedProgram; WithOptionals is analyse-only and stays green); at f10b838 the same mutant left both execution lanes green (prober, measured). - MC: Compiler.Compile throws on every call → before this patch OverloadOrderIndependence 1/1 GREEN (vacuous, measured); after it RED (1 failed, "P63-verify mutant MC"). - Restored → 22/22 green (TypeSoundness | OverloadOrderIndependence | JudgeSourceTests). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ScHwfTQy7v2FAujH3NSLQg
… — the expected code beside a second error is refused (refs #2288) P63 verify round (class-cure auditor): weakening the error arm to `errors.Contains(expected)` left all 319 Properties.Semantic tests green — JudgeSourceTests had the warning arm's "beside an error / beside a second warning" cells but no error-arm twin. New cell: SPY0220 + SPY0200 (measured with the built sharpyc @ f10b838) judged for SPY0220 → refused, "drew [SPY0200, SPY0220]". Mutation (worktree @ f10b838 + this patch): `errors is [var only] && only == expected` → `errors.Contains(expected)` → red (1 failed: ErrorArm_ExpectedCodeBesideASecondError_IsRefused); restored → green (JudgeSourceTests all passed, 22/22 with the sibling lanes). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ScHwfTQy7v2FAujH3NSLQg
…ST — the mapping c285511 added was untested (refs #2288) P63 verify round (class-cure auditor): reverting `states[num] = "PULL_REQUEST" if "/pull/" in url else state` to `= state` left the pytest file 25/25 green — every test stubs query_states, so an OPEN pull request cited as a tracker would pass the gate unnoticed. New cells stub subprocess.run for `gh issue view`: a /pull/ url in states OPEN/MERGED/CLOSED → PULL_REQUEST; an /issues/ url keeps its state (positive control). Mutation: the mapping reverted → red (3 failed, the three PR-url cells; the issue-url control stays green); restored (cp + touch) → green (29 passed). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ScHwfTQy7v2FAujH3NSLQg
…osed #2288 from the roster's GeneratorTrackers (refs #2288) P63 verify round, Section B: every caller uses SelfAndDescendants; no roster row cites #2288 (the issue-state gate would redden on one), so the set only named a closed issue. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ScHwfTQy7v2FAujH3NSLQg
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
P63 (#2288) hardening, close-out and verify-round fixes. Tests and build_tools only; no production change.
Gate 80411/0/4 @ 27bf064 (measured). Residue filed on #2324 and #2335.
🤖 Generated with Claude Code
https://claude.ai/code/session_01ScHwfTQy7v2FAujH3NSLQg