Verification Guarantees and Limits

How to interpret verification results and guard elision safely

Reader question: What does each check or proof status guarantee, and when does the generated program retain runtime checks?

Calor verifies individual contract obligations under a positive, enumerated model of .NET behavior. It does not claim whole-program correctness, and the number of soundness gaps that have not yet been found is not knowable.

Select checks explicitly

Type and effect checks run by default on the supplied Calor inputs. They do not analyze every external library or all raw C# bodies. Static bug-pattern analysis requires --analyze; Z3 contract verification requires --verify.

Runtime contract checking is a separate choice:

These compiler modes are not the .NET Debug/Release build configuration. Both debug and release modes can emit checks. Unsupported body shapes, disabled checks, and compilation errors must be reviewed separately from proof status. --keep-proven-guards disables proof-based removal; it does not enable checks when contract mode is off or repair unsupported lowering.

The Seven Statuses

Preconditions are never elided from satisfiability results. A vacuous proof is reported with a flag and also keeps its runtime check.

Compiling with --verify removes an eligible runtime postcondition guard by default — but only after a clean, non-vacuous, assumption-free proof. assumed and inconclusive outcomes do not authorize proof-based removal. This does not promise a guard when checking is disabled or lowering is unsupported. Pass --verify --keep-proven-guards to retain otherwise-emitted guards and use verdicts as diagnostics only. Historical mode changes belong in the changelog. Regression suites cover bounded modeled forms; they do not prove soundness for all programs.

Parameter mutation and numeric limits

A postcondition observes parameter values at function exit, not a frozen entry snapshot. Entry preconditions cannot simply be reused after a parameter changes. The parameter-poststate fix rejects unmodeled mutations, including implicit getter/conversion paths that may mutate ref aliases, rather than claiming a proof. Read the returned status and retain runtime checks where supported.

Integer overflow policy

Native Calor defaults to TRAP, using checked arithmetic. For example, 46340 * 46340 returns 2147395600, but 46341 * 46341 throws OverflowException. Contract mode and overflow policy are separate: --contract-mode off disables contract checks, not this overflow exception. A postcondition describes normal returns, not a promise of exception-free execution.

Converted C# modules explicitly record their source overflow policy. Ordinary unchecked C# uses the module attribute overflow=unchecked, preserving its wrapping behavior; it does not inherit native Calor's default. Explicit checked/unchecked contexts remain distinct. Unscoped raw C# from a globally checked compilation is rejected, not silently treated as unchecked.

Verification follows the selected policy. A predicate proof that depends on an unestablished arithmetic-safety condition carries the named checked-arithmetic assumption and cannot authorize proof-based guard removal. Read the reported status and assumptions rather than treating --verify as a universal overflow-safety guarantee.

Floating-point NaN, infinities, overflow, overloaded operators, and repeated property evaluation need their own semantics. Identities such as x == x or x - x == 0 are not universal .NET laws. The untyped simplifier preserves unknown operands and their evaluations instead of assuming IEEE reflexivity, built-in operators, or purity. A supported literal fold is not a general symbolic proof. The September soundness audit tracks these boundaries in parameter poststate and typed simplification. Their regression suites are bounded checks, not whole-program guarantees.

Runtime quantifier limits

Runtime quantifiers retain the full predicate, including short-circuit guards and observable evaluations. Finite-domain lowering preserves the declared integer type and evaluation order only when the compiler can certify the required bounds and their stability. It does not move an unknown getter ahead of another condition to discover a range.

When a requested runtime check cannot be lowered faithfully, compilation fails with Calor0326 before proof-based guard removal. There is no silent static-only fallback, and even a proven result does not authorize unsupported runtime lowering. Disabling runtime contracts is a separate, explicit mode choice.

Modeling boundaries

Nullability checks are not solver proofs

Calor 0.22 rejects possibly-null values at specified initialization, native-return, and resolved method-input boundaries. It covers scalar strings, supported arrays and one-level string generic payloads, and identity-proven nominal references. Mutable assignment/rebinding and constructor input enforcement remain excluded. See the support table and migration guide. These checks enforce supported receiving boundaries, not every use of a reference.

The production checks trust available interop annotations and conservatively treat truly missing (Oblivious) annotations as possibly null. They do not prove that external implementations honor those annotations. A passing bounded regression matrix is not whole-program null safety.

These checks do not lift the D3/D12/D14 safeguards below. D3 concerns nullability, D12 string indexing/counting semantics, and D14 the reference model. #875 remains open. String/array/user-type proof demotions and their retained runtime guards remain necessary.

If a proof is carried by a Z3 sort that is total where the .NET value may be null, the result is assumed, not proven.

Strings

Proofs touching Z3 string theory are assumed. Two semantic differences make elision unsafe today:

• Z3 strings have no null value; .NET string references may be null.
• Z3 counts UTF-8 bytes; .NET string.Length counts UTF-16 code units.

Non-ordinal comparison modes are unsupported. Mode-less StartsWith, EndsWith, and IndexOf are also refused because their .NET overloads use the current culture. State StringComparison.Ordinal when that is the intended semantics.

Arrays and User Types

Array and user-type sorts are total in Z3 but nullable references in .NET. Postcondition proofs for signatures naming those types are therefore assumed, even when a particular postcondition mentions only result. This is intentionally conservative: it costs an optimization instead of deleting a runtime check on a false proof.

Arithmetic and Expressions

• Division and remainder add divisor and signed-overflow side conditions. A proof that needs them is assumed; some conditionally evaluated positions are unsupported.
• Narrow integer arithmetic is refused where C# promotion would diverge from the solver model.
• Shift counts are masked as C# masks them.
• Unregistered user fields and unmodeled contract calls are unsupported, not guessed.

Runtime Lowering Is a Separate Boundary

A sound static proof and correct runtime-check placement are different problems. Current lowering routes structured returns, including early and nested returns, through a shared postcondition exit when checks are enabled. Opaque raw-C# bodies are rejected with Calor1001, because their returns cannot be identified structurally. Iterator postconditions are rejected with Calor1004; their semantics across yield are not defined. These diagnostics are not successful enforcement or proof.

Type and Effect Defaults

Type checking is on by default. Use --no-type-check on the root build command, CALOR_NO_TYPE_CHECK=1 on other entry points, or CalorTypeCheck=false in MSBuild only as explicit migration opt-outs. These controls do not disable active binding errors Calor0272–Calor0274. Neither effect controls nor --transpile-only bypass those errors.

Effect enforcement is also on by default. Interop assumptions propagate, and override/interface effect variance is checked. Calling a function value — a callback parameter, a bound lambda, a callback field — is not an error: the compiler reads the callback's own §E{…} and charges it to the caller. Calor0418 is reserved for invoking something that is provably not a function at all.

Contract proofs do not establish effect completeness. Indexed heap stores, including compound assignments, charge mut. Receiver and index evaluations and invoked property accessors contribute their effects; a simple property write does not charge a final getter that it never reads. The indexed-assignment fix covers these paths, not universally complete effect checking.

--no-enforce-effects disables the gate. --permissive-effects assumes a call the compiler cannot look up does nothing, so Calor0411 and Calor0425 go unreported and Calor0410 is demoted to a warning; it never waives Calor0424, Calor0420, or Calor0421. Because unknown calls are counted as doing nothing, it voids the effect guarantee — see Effects for exactly what it does and does not waive.

Review Checklist

1. With --verify, eligible postcondition guards may be removed; add --keep-proven-guards to retain otherwise-emitted guards.
2. Treat only a non-vacuous, assumption-free proven as eligible for elision.
3. Read every named assumption on assumed results.
4. Keep unsupported, unknown, timeout, and unavailable distinct; their remedies differ.
5. Check for Calor0326, Calor1001, and Calor1004 before relying on runtime enforcement.
6. Record any effect or contract waiver in review.

Use calor verify for raw results and calor review-packet for a change-oriented report.