Repository navigation
Research: CsFv (C# SMT contract verifier) — soundness anti-patterns as negative controls + per-method receipt idea (kill-first) #457
Description
Classification
- Type: bounded research / related-work extraction / negative-control design
- Priority: P3 backlog; no production implementation authorized
- Upstream: NuGet
CsFv12.22.0 (+CsFv.Analyzers,CsFv.Contracts), "C# formal verification — contract attributes and Roslyn analyzer". The nuspec points togithub.com/hapyy/cs-fvat commitd87658f80abf14aaf0dffb12a2d751dcfc2b23a8, but that repository returns 404 (private or removed); no PDB, SourceLink or.snupkg. - License: CC BY-NC-ND 4.0. Ideas and observed defects may be discussed; no code may be copied or adapted.
- Related, not replaced: Research: Beni-inspired ownership differential oracle and obligation-mutant validation #455 (obligation-mutant validation), Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405 (semantic mutation harness), Research: Cilica-style analysis invalidation and pass verification for OwnIR (bounded spike) #456 (unknown/incomplete vs clean outcomes), Research: AI-assisted ownership-analysis setup with auditable assumptions (TrustInSoft / Microsoft) #452 (auditable assumptions), P-002 (verification backend), P-037 /
formal/p037-kernel. - Default decision: nothing to port. The value is (a) a list of soundness anti-patterns to turn into Own.NET regression controls and (b) one IDE-facing idea.
Evidence basis
- Read: the four assemblies of 12.22.0, decompiled locally with ILSpy 11.2 (with Microsoft.CodeAnalysis 5.0.0 references; no unresolved-type markers left). Everything below was read in that code.
- Not done: the analyzer was not executed (no solver run, no generated
.smt2inspected). Statements about runtime behaviour are inferences from the code.
How CsFv works (confirmed in code)
- A Roslyn analyzer registers on
OperationKind.MethodBody. SmtGenerator.GenerateSmtCode(method)builds an SMT-LIB string: parameters/locals asdeclare-const(SSA for reassigned locals),return eas(assert (= result e)),[Requires("…")]strings re-parsed as C# expressions and asserted,[Ensures("…")]asserted negated, then(check-sat).- The string is piped to an external
cvc5 --lang=smt2 --incremental, falling back toz3 -smt2 -infrom PATH (10 s timeout on the z3 path).unsat→ success diagnostic,sat→ failure. - Diagnostics distinguish success / failure / no verifiable properties / generation error / solver unavailable / solver error.
Anti-patterns worth a control in Own.NET (confirmed in code unless marked)
| # | CsFv behaviour | Where | Own.NET control it suggests |
|---|---|---|---|
| A1 | The verdict is the last sat/unsat line of solver output (LastOrDefault), while one script contains several check-sat (loop VCs inside push/pop plus the final query). A failing intermediate obligation is discarded. |
Z3CliStrategy, RealCvc5Runner |
Any aggregation of per-obligation results must be an explicit AND; a fixture with one failing intermediate obligation must turn the aggregate red. |
| A2 | Loop "invariant preserved" VC does not encode the body: it emits the comment ; Execute loop body: plus the body text, declares <var>_next constants that nothing uses, then asserts I ∧ B ∧ ¬I — unsat by construction. |
LoopInvariantEncoder.EncodeLoopVerificationConditions |
Per obligation kind, a mutant on which the obligation must fail (overlaps #455/#405); a check that cannot fail is a defect even when green. |
| A3 | Preconditions inferred from the method's own body are asserted as assumptions when verifying that same method — they silence exactly the faults they were inferred from. | SmtGenerator (inferred precondition facts) |
A summary/fact derived from M must never be an assumption while checking M itself, including SCC/recursive cases. Worth a conformance test even if spec/Inference.md already rules it out. |
| A4 | Several inferred postconditions are asserted as separate (assert (not p_i)), i.e. "all false at once" instead of "at least one false"; if one is provable the rest are reported verified too. (Explicit [Ensures] uses (or …) correctly.) |
SmtGenerator (inferred postcondition facts) |
Tests on the combination layer specifically, not only on single obligations. |
| A5 | Contract attributes are recognised by simple name (Requires / RequiresAttribute, any namespace). |
SmtGenerator.ExtractContracts |
Supports matching Own.NET protocol attributes by fully-qualified name rather than by name (the open follow-up on [ProtocolToken] / [ProtocolRegion]). |
| A6 | Silently inactive machinery: bcl-stubs.json (BCL method contracts) is loaded from AppContext.BaseDirectory but is not in the package; MultiSolverValidator and SolverSelfTest exist but have no callers. |
BclStubLoader, CsFv.Verification |
Every disabled/unwired source of facts should be visible in coverage output, not only in code. |
| A7 | Primitive semantics differ from C#: int/long → unbounded Int (no overflow), / → div, % → mod (floor semantics, not C# truncation for negatives); calls → uninterpreted functions. |
ConvertTypeToSmt, SimpleMethodEncoder.EncodeBinaryOperation, EncodeInvocation |
Same lesson as "an op exists ≠ its semantics fit" (release ≠ move): quote the semantics of every reused op before relying on it. |
One idea that may be worth keeping
Per-method receipt in the IDE. CsFv reports "nothing verifiable here" as its own outcome, separate from success. Own.NET's precision floor resolves doubt toward silence, so in the editor "checked, no findings" and "not analysed / refused" currently look the same; coverage is only visible in the opt-in --binding-coverage sidecar. A receipt like "N obligations discharged, M refused (reason)" on a method would make silence auditable. Inference only — cost and noise not assessed; relates to the planned first-class analysis refusal and to #456.
Bounded investigation (kill-first)
- For A1–A4, check whether Own.NET already has a test that would catch the analogous failure (aggregation, unfalsifiable obligation, self-assumption, combination of several facts). Record what is already covered; stop for any item already covered.
- For at most two uncovered items, write one fixture + one mutant each (negative control must turn red on the unmodified checker when the defect is injected, then restore).
- A5: decide documented reserved names vs fully-qualified matching (owner decision).
- Receipt idea: one paragraph on where the data would come from (sidecar / refusal records) and what would make it noise; no implementation.
Kill condition: if A1–A4 are all already covered by existing Own.NET tests, close as "no action; anti-patterns recorded".
Activity