Autoharness: constructor-based value generation (--constructor-args) by tautschnig · Pull Request #4717 · model-checking/kani

tautschnig · 2026-08-05T15:51:03Z

Description

The top-100/500 crates.io failure triage (#3832) showed the largest class of genuine false alarms is nondeterministic receivers violating private type invariants: e.g. time's Date packs a validated ordinal into a private field, so raw field synthesis produces invalid dates and fails every method harness (194+ harnesses in the top-100 triage attributed to this class).

Under the new opt-in --constructor-args flag, kani::any::<T> for private-field structs is synthesized as: generate nondeterministic constructor arguments, call one of T's public constructors, assume success (switching on the discriminant for Option<Self>/Result<Self, E> returns), and return the payload. Constructor search prefers Self over Option<Self> over Result<Self, E> returns, then more arguments over fewer; it excludes non-public, doc-hidden (_unchecked macro exports that assert preconditions), unsafe, zero-argument (Instant::now() reaches unsupported clock_gettime; single-point coverage regardless), and generic constructors — each exclusion was validated empirically on the time crate.

Per the bounded-features policy (#4691 discussion), the option is opt-in because it under-approximates (only constructor-reachable values are explored): harnesses are marked "(ctor)" via new is_ctor_based metadata, with an explanatory note in the summary. The sound successor (mining the type's own validity assertions into filters) is a follow-up PR building on this one.

Measured on time-0.3.54: 341 -> 538 verified, 500 -> 315 failures (203 false alarms eliminated; 17 new failures from constructors with documented panics, a logged refinement).

Note that constructor arguments must themselves already implement Arbitrary (they do not get the argument-position extensions — slices, smart pointers, nested constructors). Besides keeping phase 1 small, that requirement is what makes recursive and mutually-recursive constructors (fn combine(a: Node, b: u32) -> Node, or A::from_b/B::from_a) structurally unreachable, so generation cannot recurse forever. Verified by hand.

Changes from the original branch (rebase onto main)

main gained --bounded-arguments, per-parameter generic instantiation and the JSON frontend since this branch was cut, which surfaced three defects:

--bounded-arguments was silently ignored. The branch replaced the bounded_arguments parameter of add_auto_harness_args with constructor_args instead of adding to it. Both are now forwarded and compose: a harness that is both reads #[kani::proof] (bounded) (ctor) and both explanatory notes print independently. The compiler side carries an AutoHarnessCaveats { is_bounded, is_ctor_based } struct rather than reusing main's single bool slot, so the two independent flags cannot be swapped at a call site.
The "(ctor)" marker could lie. uses_ctor_generation also accepted find_unchecked_constructor, but nothing in AutomaticArbitraryPass used that search — and automatic::inline_with_assumed_panics, the consumer named in its doc comment, does not exist. A type whose only constructor was an _unchecked builder was therefore marked "(ctor)" and given the under-approximation caveat while generation actually fell back to raw field synthesis. Reproduced, then fixed by making the marking predicate test exactly what generation tests; find_unchecked_constructor (75 lines, no remaining callers) was removed rather than shipped as dead code, and the follow-up should reintroduce it with its consumer. Pinned by a new OnlyUnchecked case in the test.
is_ctor_based was missing from the JSON export. frontend/schema_utils.rs emitted is_bounded only, so a JSON consumer could tell a bounded run apart but not a constructor-based one. Added and asserted in schema_utils_test.rs.

Also adapted to VariantDef::idx no longer being public (reconstructed via VariantIdx::to_val, as generate_enum_body already does) and routed the pass through main's shared AnyModels instead of duplicating kani_any/kani_assume fields.

Testing

cargo_autoharness_constructor runs the same crate with and without the flag: without, the invariant-violating false alarms appear; with it, they disappear and the affected harnesses carry the "(ctor)" marker. It covers a Option<Self>-returning constructor (Day), a direct-returning one (Celsius), a Result<Self, E>-returning one (Even), and a type with only an _unchecked constructor (OnlyUnchecked) that must not be marked.

All 23 script-based autoharness tests pass, as does the full script-based-pre suite, cargo test -p kani-driver/-p kani-compiler/-p kani_metadata, clippy --workspace --tests, and kani-fmt --check.

Towards #3832.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Copilot

Pull request overview

This PR extends Kani’s autoharness generation to reduce false alarms from invalid synthesized values by (a) optionally generating private-field struct values via public constructors (--constructor-args, with “(ctor)” reporting) and (b) constraining synthesized scalar values to rustc-valid layout niches. It also adds script-based regression tests and updates documentation.

Changes:

Add opt-in constructor-based value generation for private-field structs under --constructor-args, and mark affected harnesses as “(ctor)” with an explanatory note.
Constrain synthesized scalar-ABI values to their rustc_layout_scalar_valid_range niche via kani::assume.
Add script-based regression tests for both the niche handling and constructor-based generation, plus user documentation.

Reviewed changes

Copilot reviewed 21 out of 22 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs	Adds a minimal crate with private-field invariants and constructors to exercise ctor-based generation.
tests/script-based-pre/cargo_autoharness_constructor/constructor.sh	Script-based test invoking autoharness with/without `--constructor-args` and filtering output.
tests/script-based-pre/cargo_autoharness_constructor/constructor.expected	Expected output showing failures without the flag and “(ctor)” successes with it.
tests/script-based-pre/cargo_autoharness_constructor/config.yml	Wires the constructor script test into the script-based test harness.
tests/script-based-pre/cargo_autoharness_constructor/Cargo.toml	Declares the new script-based test crate.
tests/script-based-pre/autoharness_niche/run.sh	Script test driver for niche-constrained scalar generation.
tests/script-based-pre/autoharness_niche/niche_probe.rs	Defines a `rustc_layout_scalar_valid_range` type and checks both correctness and coverage reachability.
tests/script-based-pre/autoharness_niche/expected	Expected output for the niche probe.
tests/script-based-pre/autoharness_niche/config.yml	Wires the niche script test into the script-based test harness.
kani-driver/src/sarif.rs	Updates test metadata initialization for the new `is_ctor_based` field.
kani-driver/src/metadata.rs	Updates test metadata initialization for the new `is_ctor_based` field.
kani-driver/src/autoharness/mod.rs	Adds `--constructor-args` plumbing, “(ctor)” rendering, and the summary note.
kani-driver/src/args/autoharness_args.rs	Adds CLI flags/docs for `--constructor-args` (and `--bounded-arguments`).
kani-compiler/src/kani_middle/transform/automatic.rs	Implements ctor-based `kani::any` synthesis for private-field structs and niche assumptions for scalar values.
kani-compiler/src/kani_middle/mod.rs	Adds constructor discovery utilities, niche inspection, and ctor-based harness-marking support.
kani-compiler/src/kani_middle/metadata.rs	Threads `is_ctor_based` into generated harness metadata.
kani-compiler/src/kani_middle/codegen_units.rs	Computes and propagates `is_ctor_based` for automatic harness metadata.
kani-compiler/src/args.rs	Adds compiler-side flags `--autoharness-constructor-args` (and `--autoharness-bounded-arguments`).
kani_metadata/src/harness.rs	Adds `HarnessMetadata::is_ctor_based` with serde defaulting.
docs/src/reference/experimental/autoharness.md	Documents `--constructor-args` behavior and its under-approximation caveat.
Cargo.lock	Changes the locked `charon` version.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

The top-100 crates.io failure triage (model-checking#3832) showed the largest class of genuine false alarms is generated receivers violating private type invariants (e.g. time's Date packs a validated ordinal; raw field synthesis produces invalid dates, failing every method harness). Under the new opt-in --constructor-args flag, kani::any::<T> for private-field structs is synthesized as: generate nondeterministic constructor arguments, call one of T's public constructors, assume success (switching on the discriminant for Option<Self>/Result<Self, E> returns), and return the payload. Constructor search excludes non-public, doc-hidden (commonly _unchecked variants exported for macros that assert preconditions), unsafe, zero-argument (single-point coverage; Instant::now() reaches unsupported clock_gettime), and generic constructors; it prefers Self over Option<Self> over Result<Self, E> returns, then more arguments over fewer. The option is opt-in because it under-approximates (only constructor-reachable values are explored): harnesses are marked "(ctor)" via new is_ctor_based metadata, with an explanatory note in the summary. Measured on time-0.3.54: 341 -> 538 verified, 500 -> 315 failures. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…o_fn_def The merge of main upgraded to nightly-2026-05-01, where tcx.type_of(def_id).instantiate_identity() yields an Unnormalized wrapper that no longer implements Stable. Match the rest of the codebase by stabilizing the EarlyBinder and taking its .value.

Extend --constructor-args with assert mining: prefer assert-guarded representation constructors (unsafe / doc-hidden / _unchecked-named, returning Self; generic ADTs instantiated with their own args), inlined into the synthesized kani::any body with every validity statement converted into a filter on the nondeterministic arguments: - kani::assert(cond, msg) calls (Kani's macro overrides have already rewritten user asserts/panics into these) -> kani::assume(cond); - hint::assert_unchecked(cond) (UB-hint contracts, e.g. deranged's new_unchecked) -> kani::assume(cond); - raw panic-entry calls -> assume(false) + unreachable; - MIR Assert terminators (overflow checks) -> assume(cond == expected). Calls within the inlined body whose callees contain such validity statements are recursively inlined (depth <= 3, <= 32 blocks per callee, plain-call fallback), covering nested patterns like time's Time::__from_hms_nanos_unchecked calling deranged's new_unchecked. Such a constructor is typically the raw representation builder whose asserts state the type's validity contract exactly, and is surjective onto the valid value space; the generated set is then precisely the values passing the type's own validity assertions. New MutableBody primitives push_raw_bb/split_with_terminator support the inlining; an allowlist remapper bails out (falling back to checked-constructor generation) on unsupported constructs. Measured on time-0.3.54 (vs. 341 ok / 500 fail baseline): checked-ctor assumption 538/315; hand-written invariants 490/363; assert mining 595/258 (251 fixed, 8 broke -- predominantly CBMC 60s-timeouts from formula growth, a logged refinement). Rebased onto the constructor-args PR (model-checking#4717): re-introduces find_unchecked_constructor (removed there) and adapts to the AnyModels refactor. Also folds in review-driven robustness fixes -- match hint::assert_unchecked by exact path rather than substring, guard the assert-argument access -- and documents the vacuous-harness caveat for an unsatisfiable constructor (tracked in model-checking#4757). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Extend --constructor-args with assert mining: prefer assert-guarded representation constructors (unsafe / doc-hidden / _unchecked-named, returning Self; generic ADTs instantiated with their own args), inlined into the synthesized kani::any body with every validity statement converted into a filter on the nondeterministic arguments: - kani::assert(cond, msg) calls (Kani's macro overrides have already rewritten user asserts/panics into these) -> kani::assume(cond); - hint::assert_unchecked(cond) (UB-hint contracts, e.g. deranged's new_unchecked) -> kani::assume(cond); - raw panic-entry calls -> assume(false) + unreachable; - MIR Assert terminators (overflow checks) -> assume(cond == expected). Calls within the inlined body whose callees contain such validity statements are recursively inlined (depth <= 3, <= 32 blocks per callee, plain-call fallback), covering nested patterns like time's Time::__from_hms_nanos_unchecked calling deranged's new_unchecked. Such a constructor is typically the raw representation builder whose asserts state the type's validity contract exactly, and is surjective onto the valid value space; the generated set is then precisely the values passing the type's own validity assertions. New MutableBody primitives push_raw_bb/split_with_terminator support the inlining; an allowlist remapper bails out (falling back to checked-constructor generation) on unsupported constructs. Measured on time-0.3.54 (vs. 341 ok / 500 fail baseline): checked-ctor assumption 538/315; hand-written invariants 490/363; assert mining 595/258 (251 fixed, 8 broke -- predominantly CBMC 60s-timeouts from formula growth, a logged refinement). Rebased onto the constructor-args PR (model-checking#4717): re-introduces find_unchecked_constructor (removed there) and adapts to the AnyModels refactor. Also folds in review-driven robustness fixes -- match hint::assert_unchecked by exact path rather than substring, guard the assert-argument access, remap `unwind: Cleanup` targets on inlined Call/Assert/Drop terminators (not just the normal target) -- and documents the vacuous-harness caveat for an unsatisfiable constructor (tracked in model-checking#4757). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…ecking#4718) ### Description Stacked on model-checking#4716 and model-checking#4717 (review only the last commit). Extends `--constructor-args` with assert mining: the constructor search now prefers assert-guarded *representation constructors* (unsafe / doc-hidden / `_unchecked`-named, returning `Self`), which are inlined into the synthesized `kani::any` body with every validity statement converted into a *filter* on the nondeterministic arguments: - `kani::assert(cond, msg)` calls (Kani's macro overrides have already rewritten user asserts/panics into these) become `kani::assume(cond)`; - `hint::assert_unchecked(cond)` (UB-hint contracts, e.g. deranged's `new_unchecked`) becomes `kani::assume(cond)`; - raw panic-entry calls become `assume(false); unreachable`; - MIR `Assert` terminators (overflow checks) become `assume(cond == expected)`. Calls within the inlined body whose callees contain such validity statements are recursively inlined (depth ≤ 3, ≤ 32 blocks per callee, plain-call fallback otherwise) — this covers nested patterns like time's `Time::__from_hms_nanos_unchecked` calling deranged's `RangedU32::new_unchecked`. The insight: an unchecked representation constructor's assertions state the type's validity contract *exactly* (they were written as the caller's proof obligations), and the constructor is surjective onto the valid value space — so the generated set is precisely the values passing the type's own validity assertions. This is strictly better than assuming a checked constructor's success (which may reach only a subset of valid values and interferes with functions' own `Result` paths). Measured on time-0.3.54 (baseline 341 verified / 500 failing): checked-ctor assumption gives 538/315, hand-written `Invariant` impls for three types give 490/363, **assert mining gives 595/258** (251 harnesses fixed, 8 regressed — predominantly CBMC 60-second timeouts from formula growth of inlined generation, logged as a refinement). ### Testing The `cargo_autoharness_constructor` test gains a nested-unchecked-constructor case (a wrapper constructor calling an inner `new_unchecked` with `debug_assert`s): fails without `--constructor-args`, passes with it. Niche and autoderive suites pass. Towards model-checking#3832. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…checking#4721) ### Description Stacked on model-checking#4716/model-checking#4717/model-checking#4718 (review only the last commit). Adds autoharness support for `&[T]`, `&mut [T]` and `Vec<T>` arguments with primitive integer/float element types, generated **unbounded**: fresh allocations of nondeterministic size, so verification results hold for **all** lengths. Loops that cannot be fully unwound surface as *visible* unwinding-assertion failures instead of silently bounded successes — the soundness-signaling design validated in the top-500 evaluations (model-checking#3832). - `&mut [T]`: each call leaks a fresh allocation, so the slice is exclusive by construction. - `Vec<T>`: `from_raw_parts` with capacity matching the allocation layout (freed on drop); ZST elements use the documented dangling-pointer pattern (loop-free, as generation code must be). - The models are optional (require `alloc`), following the smart-pointer-model precedent: absent in `verify-std`'s no-core flow, where these argument types simply stay unsupported. - Element scope: only types where raw nondeterministic memory is valid as-is. The companion `SliceValidityAssume` hook (lowered directly to pure quantified goto expressions, bypassing the closure-based quantifier path) exists for niched element types, but CBMC's SAT backend silently drops symbolic-bound quantifiers (model-checking#4719), so `bool`/`NonZero*` elements remain unsupported until the in-progress CBMC quantifier-instantiation work lands — at which point `slice_elem_unbounded_ok` re-admits them. Corpus measurement (top-500, full-stack sweep): zero ICEs; the expected shift of silently-bounded loop successes into visible unwinding failures (http 6→18, prost 0→14, encoding_rs 26→35) with loop-free properties over slices/Vecs verifying for all lengths (covers pin lengths beyond 100,000). ### Testing New `cargo_autoharness_vec_unbounded` test: loop-free accessors pass for all lengths, covers verify large lengths/extreme contents/empty values reachable, a looping consumer pins the visible unwinding-failure contract, and a mutable-slice writer verifies. Constructor/niche/autoderive suites pass. Towards model-checking#3832. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…-checking#4722) ### Description Stacked on model-checking#4716/model-checking#4717/model-checking#4718/model-checking#4721 (review only the last commit). Mines type invariants from a type's *own assertions*: conditions over the receiver's fields asserted on every normal return path of **at least two** distinct methods (a frequency filter against method-local preconditions). Corpus grounding: 1,977 such assertion sites across 131 of the top-500 crates. Admission is conservative — post-dominance (per match-arm for enums, yielding variant-guarded conjuncts), call-free single-assignment backward slices (one-level pure-getter inlining excepted), extraction into a pure expression AST that re-materializes as total, loop-free MIR. Two consumers: - under `--constructor-args` (same heuristic umbrella, same "(ctor)" marker): generated values **assume** the mined conjuncts — covering types with no viable constructor, at lower formula cost than constructor inlining; - new `--check-invariants`: values returned by verified functions are **checked** against the mined conjuncts — through `&T` and `Option`/`Result` payloads (`None`/`Err` pass vacuously) — with a distinct property message naming the asserting methods. This turns autoharness into an automatic invariant-preservation checker: the classic "constructors establish, methods preserve" obligation, with zero annotations. ### Testing The regression test pins eight behaviors: struct and enum (variant-guarded) invariants assumed for generated values (false alarms eliminated, markers attached); getter-mined conditions; a buggy producer returning an invariant-violating value caught by the output check (direct and `Result`-wrapped); correct producers and `Err` paths passing; and a single-method precondition honestly *not* mined. Constructor/niche/vec/autoderive suites pass. Towards model-checking#3832. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…checking#4725) Stacked on model-checking#4717 (`--constructor-args`); only the last commit is new. Marked draft until model-checking#4717 merges. A top-500 crates.io autoharness sweep (tracking model-checking#3832) ICEd in constructor discovery on 12 crates; three root causes: 1. **Item own lifetimes** (brotli, sharded-slab): `AtomicU8::from_ptr<'a>`-style constructors were resolved with the ADT args only — arity mismatch panic. 2. **Lifetime position** (regex-automata, gimli, redox_syscall, arc-swap, clap_builder, event-listener, crypto-bigint): `impl<'h> Searcher<'h>` places the lifetime first, so appending erased lifetimes is insufficient — the argument list is now built positionally against the item's full parent+own generics, rejecting shape mismatches up front (rustc's instantiation panics on kind mismatches rather than returning `Err`). 3. **Escaping bound regions** (async-io, js-sys, quinn-udp, wasm-bindgen): `BorrowedFd<'_>`-style arguments read from a skipped fn-sig binder panicked the trait solver's dummy-binder wrap; such candidates are rejected as non-generatable. All 12 crates verified clean with this branch. The constructor regression test gains all three shapes. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

### Description Bumps `rust-toolchain.toml` from `nightly-2026-05-01` to `nightly-2026-06-01`. Four upstream changes drive most of this. #### 1. `Retag` moved onto `Rvalue::Use` `StatementKind::Retag` and `RetagKind` are gone; `Rvalue::Use` now carries a `WithRetag` flag instead: ```rust Use(Operand, WithRetag), ``` Kani never modelled retags (they are Stacked-Borrows/Miri only), so the statement arms are dropped, the flag is ignored when reading a `Use`, and synthesized `Use`s pass `WithRetag::No`. `internal_mir`'s `RetagKind` conversion becomes a `WithRetag` one. #### 2. `Variants::Multiple` stores a `VariantLayout`, not a `LayoutData` The new type carries only per-field offsets — no `FieldsShape` (so no field order) and no alignment. Variant layouts now come from `Layout::for_variant`, which is what `rustc_codegen_ssa` does and which restores the field order. A new `variant_layout` helper is used by **both** the type side (`codegen_enum_cases`) and the value side (`codegen_aggregate`), so the goto struct's components and the operands initializing them cannot disagree. That change bit back: `for_variant` reports the *enum's* align for a variant (`align: parent.align`), which over-pads every variant and inflates the enum. `check_vtable_size` caught it as an ICE on `tests/cargo-kani/iss2857` (48 vs 55 bytes). So `codegen_struct_fields`/`codegen_alignment_padding` now take the align explicitly, and a variant's own align is computed as the maximum of its fields' aligns — which is what the per-variant `LayoutData` used to carry. #### 3. `rustc_layout_scalar_valid_range_start`/`_end` were removed Replaced by pattern types, the same move `core::num::niche_types` made. The tests that define ranged scalar newtypes are converted to `std::pat::pattern_type!`. This narrows the layout-niche feature added in model-checking#4716: a pattern type is not an ADT and has no `Arbitrary` implementation, so `can_derive_arbitrary` cannot synthesize a struct that has one as a field, and locally-defined ranged types are now skipped rather than harnessed. The assumption still works end to end through `std::time::Duration` (the motivating case from the model-checking#3832 triage), and `tests/script-based-pre/autoharness_niche` pins both halves so the reduced reach is asserted by a test rather than silent. Tracked in model-checking#4758 with a concrete fix sketch. #### 4. New `Rvalue::Reborrow` User-definable reborrowing of ADTs via `CoerceShared`. It is documented as a bitwise copy today, but the same docs anticipate it changing memory layout, so codegen reports it as an unsupported construct rather than silently modelling it as a copy. The points-to analysis treats it as pointing wherever its place does. #### Assorted API changes | Change | Site | | --- | --- | | `CodegenBackend` moved `CrateInfo` from `codegen_crate` to `join_codegen` | both backends' `compiler_interface.rs` | | `rustc_data_structures::stable_hasher` renamed to `stable_hash`; `HashStable`/`hash_stable` to `StableHash`/`stable_hash` | `reachability.rs` | | The `normalize` callback of `ptr_metadata_ty{,_or_tail}` now takes `Unnormalized` | `typ.rs` | | More `FieldDef::ty` and `instantiate*` sites need `.skip_normalization()` | `typ.rs`, `intrinsics.rs` | | `TagEncoding::Niche`'s `niche_variants` is the lang `RangeInclusive` (public `start`/`last` fields, not methods) | `rvalue.rs`, `statement.rs` | | New `useless_borrows_in_formatting` clippy lint | 11 sites across the workspace | #### Test change worth calling out `vtable_size_align_drop` no longer asserts the exact identity of the vtable's drop pointer. Traced with Kani's debug logging: the drop-glue shim is now `core::ptr::drop_glue::<T>` rather than `core::ptr::drop_in_place::<T>`, and `drop_glue` is not nameable from source. It checks the slot is populated instead; the size and align fields the test is named for are unchanged. This weakens the test — it no longer checks the slot holds the drop glue *for the right type* — so it is tracked in model-checking#4759 with options for restoring that coverage. Both of these failures were confirmed to be genuine `nightly-2026-06-01` regressions rather than pre-existing fragility, by rebuilding the parent commit against `nightly-2026-05-01`, where both pass. #### `drop_in_place` now takes a reference to reach the drop glue Related to the same rename: `core::ptr::drop_in_place` used to *be* the drop lang item, with its body replaced wholesale by the compiler. It is now a wrapper that calls the new `drop_glue` lang item through `&mut *to_drop`, and creating that reference asserts the pointee is aligned and valid — so dropping through a raw pointer carries a precondition it did not before. That surfaced in `expected/loop-contract/loop_assigns_for_vec.rs`, whose `loop_modifies` havocs the word holding `v.len()` while the invariant only constrains `i`; the drop after the loop then sees an unconstrained length. Strengthening the invariant with `v.len() == i * 3 + 3` is rejected (`Rust intrinsic assumption failed`), so expressing what the drop needs looks like a loop-contracts limitation rather than something this PR can fix. The test is renamed `loop_assigns_for_vec_fixme.rs` with the analysis recorded in the file, tracked in model-checking#4761. Verified that `Vec`'s internal layout is unchanged, so the test's hard-coded `.add(2)` offset for `len` is still correct. Two contract tests that deliberately pin a *total check count* needed their numbers updated: `capture_load_checks_elided` 36 → 34 and `capture_load_user_deref_pass` 60 → 58 (two checks in `read_answer`'s own body became unreachable). In both cases the assertion the test actually exists for still holds — no user-facing `pointer_dereference` group came back in the first, and the pinned `{closure#3}::{closure#0}.pointer_dereference.1 - Status: SUCCESS` is still present in the second — so the counts were updated with a note in each test explaining that the total is plumbing-sensitive and what it still guards against. ### Testing Local, macOS aarch64, CBMC 6.10.0 (`cbmc-6.9.0-214-g45436eea34`), all re-run after rebasing onto current `main` (which now includes model-checking#4717, whose new `Rvalue::Use` construction site also needed the `WithRetag` argument): | Suite | Result | | --- | --- | | `kani` | **607 passed**, 0 failed, 23 ignored | | `cargo-kani` | **71 passed**, 0 failed | | `script-based-pre` | **68 passed**, 0 failed, 1 ignored | | `std-checks` | 5 passed, 0 failed | | `cargo-ui` | 30 passed, 0 failed | | `coverage` | 20 passed, 0 failed | | `ui` | 151 passed, 2 failed — both the `cadical` tests, see below | | `expected` | **474 passed**, 0 failed, 16 fixme/ignored | | `prusti` / `smack` / `kani-docs` / `json-handler` / `cargo-coverage` / `firecracker` | 8 / 40 / 13 / 5 / 2 / 0 passed, 0 failed | Other gates, all clean: - `cargo build-dev` - `cargo build-dev -- --features cprover --features llbc` - `cargo clippy --workspace --tests` and `RUSTFLAGS="--cfg=kani_sysroot" cargo clippy --workspace` - `./scripts/kani-fmt.sh --check` - `RUSTFLAGS="-D warnings" cargo build --no-default-features --features cprover` - Unit tests: `cprover_bindings`, `kani-compiler`, `kani-driver`, `kani_metadata`, `kani --features concrete_playback`, `kani_macros` Environment caveat: this CBMC build has no `cadical`, so `ui/solver-{attribute,option}/cadical` fail locally on output text only (`"The specified solver, 'cadical', is not available"`), and `expected/shadow/slices/slice_split` is very slow under the MiniSat fallback. Both are expected to be clean on CI. Towards model-checking#4758, model-checking#4759, model-checking#4761. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

## Part A — Normative summary RFC 0015 proposes a consumer contract for Kani's `--export-json <path>` output. The flag shipped in model-checking#4472 behind `-Z unstable-options`. This RFC proposes a dedicated `-Z export-json` gate and a versioned JSON document describing one verification run. The contract defines: - Per-harness outcomes, failed properties, and check and cover results grouped by status. - Tool versions, effective configuration, and harness selection needed to interpret results. - Vacuity predicates and the settings needed to interpret unreachable assertions. - Completeness states, atomic file writes, and rules for missing results, failures, and schema compatibility. Shipped JSON already exposes processed property statuses and unreachable counts. This proposal specifies how consumers should interpret them, including when a successful harness has unreachable assertions and whether the export accounts for every selected harness. The export complements `--sarif`, which reports findings for code-scanning tools. The proposed JSON also includes successful-check counts and cover results. The schema remains unstable. Whether it should replace the shipped v1 shape, and how to resolve the remaining configuration and provenance gaps before stabilization, remain open questions. The RFC example illustrates the proposed schema; it is not captured verification output. This PR changes documentation only. The RFC file contains the complete normative proposal. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- ## Part B — Extended reference (informative — not part of the normative RFC) Part B is informative and is **not part of the normative RFC**. It preserves the longer explanations and implementation notes moved out of the RFC and adds no normative requirements. <details> <summary><b>Read the extended reference</b></summary> # Extended reference (informative) Supporting reference for RFC 0015 / [PR model-checking#4727](model-checking#4727). The RFC contains the proposed contract. This reference preserves explanations, implementation comparisons and deferred-work detail moved out of it; it adds no normative requirements. Interim home: a PR body comment. The explanatory material can later be adapted for the Kani book or implementation documentation. Revision-specific observations below describe those revisions, not a claim that one implementation already emits the entire proposed schema. ## 1. Revisions and illustrative example Source descriptions below use checkout `902daa525`. Historical PoC behavior is qualified by `7b125f1b`; later upstream behavior from model-checking#4717/model-checking#4719 is qualified by `10bc1ae04`. These revisions have different capabilities; the proposed schema is not a description of any one of their emitted files. The RFC output example is **an example of the proposed 0015 document**, for the vacuity case the motivation describes: two ordinary assertions made unreachable by one contradictory `kani::assume`. The PoC at `7b125f1b47e36ca4cc50c4041abeca01912f80f9` contains a synthetic unit test, `export_checks_unreachable_under_contradictory_assume`, that constructs two unreachable assertions and a successful result. It supports the illustrated result semantics, but is not a captured verification run. The RFC's harness, provenance, timings, and JSON are illustrative, not a measured run or verbatim PoC output. That PoC emits flat `kani_version`/`cbmc_version` fields (not the grouped `tools` object) and a boolean `run_complete` (not `run_state`), and lacks `is_bounded` and `configuration.coverage_enabled`. It already has `summary` and all seven totals; this RFC refines their treatment of non-completed harnesses, as specified in the RFC. The marker, warning caps and directory-path validation are proposed changes, not PoC capabilities. At `902daa525`, `--fail-fast` collects a `Result<Vec<_>>` and returns only the failing result on error, discarding other results even if those harnesses completed. The later model-checking#4744 fix retains completed results. Completeness measures reported entries, not which missing harnesses ran. ## 2. Field explanations and warnings **Tool provenance (`tools`).** The `tools` object records the versions of the core tools whose behaviour can change a result: `kani` itself (always known, so never `null`), the `rustc` toolchain `kani-compiler` was built against, and `cbmc`. It is the machine-readable form of the versions Kani already prints, narrowing the gap in [model-checking#2572](model-checking#2572). One rule for the two probed entries: **a version that cannot be determined is `null`, never guessed** — whether the probe binary is missing, refuses `--version`, or prints nothing parseable. (An earlier draft also carried `goto_cc`/`goto_instrument`/`goto_synthesizer` versions and a `solvers[]` array of every resolved solver; those are cut from v1 to keep it to the core — see the "Full tool & solver provenance" future-work item. The solver CBMC actually ran with is still recoverable per harness from `harnesses[].resolved_solver`.) **Harnesses that are not `--harness`-selectable.** An `is_automatically_generated` harness (from `kani autoharness`) cannot be selected by `--harness`/`--exact` at all: `find_proof_harnesses` skips generated harnesses regardless of filter. Its `name` is still reported (a real, unique identifier), but a consumer must not use it as a `--harness` argument when `is_automatically_generated` is `true`. A `#[kani::proof_for_contract]` harness, by contrast, *is* selectable, and its `name` is the harness function's own path — not the target it proves a contract for (that is `attributes.kind.ProofForContract.target_fn`, see §7). **Why not `mangled_name`.** `HarnessMetadata` also carries a `mangled_name` (the harness's name in CBMC's symbol table), but this schema does not export it and it would not serve as a selector: it identifies the harness to CBMC, not to Kani's CLI, and `--harness` does not accept it. `name` (`pretty_name`) is chosen because it is simultaneously human-readable, module-qualified, and directly re-runnable. `checks`/`covers` bucket every included property exhaustively by CBMC status. This partition and `n_properties` cover exactly what they bucket; `code_coverage` (COVERED/UNCOVERED) properties under `--coverage` are outside both and `n_properties` (no dedicated place today), so `n_properties == checks.total + covers.total` holds on a `COMPLETED` harness. `checks.success` is a bare count, unlike every other bucket: successful-check identities are numerous and of little value, whereas `covers.satisfied` names its properties because covers are user-authored and few. Exporting successful-check identities is future work. **The `checks` / `covers` partition criterion.** A property goes into `covers` exactly when `property_id.class == "cover"` (`Property::is_cover_property`, `kani-driver/src/cbmc_output_parser.rs`); every property whose class is neither `"cover"` nor `"code_coverage"` goes into `checks` (including `"assertion"`, which carries ordinary `assert!`/panic checks). This is a syntactic test on the CBMC-assigned class, independent of `status`: a cover-class property carrying a status normally seen among checks (or vice versa) still partitions by `class` and is recorded in that domain's `other[]` array rather than crossing over (see the RFC’s Value domains). `code_coverage`-class properties are excluded from both buckets entirely. **`failed_properties[]` membership.** `failed_properties[]` names exactly the properties in `checks.failure` (`class` is neither `"cover"` nor `"code_coverage"`, with `status == "FAILURE"`), with the full per-property shape rather than `checks.failure`'s bare id list. It does **not** include `checks.error` (an `ERROR` is solver-level "could not determine," bucketed separately — see `failure_kind == "ERROR"`) or any cover-class property (`covers.unsatisfiable` is that bucket's own list). This is why `n_failed == len(checks.failure)` on a `COMPLETED` harness: `n_failed` is `failed_properties.len()`, whose membership *is* `checks.failure`'s. **`warnings`** is empty in the illustrative vacuity example. The synthetic fragment below shows the shape of an untruncated warning, not a captured CBMC message or a warning-size measurement. The `warnings_truncated` field and the `truncated`/`original_chars` pair are this proposal's additions, not emitted by the PoC at `7b125f1b`, which collects warning strings without truncation: ```json { "warnings": [ { "message": "Example warning", "truncated": false, "original_chars": null } ], "warnings_truncated": 0 } ``` `truncated`/`original_chars` replace a `[truncated; N chars total]` suffix inside `message`: a structural field a consumer checks without pattern-matching free text, avoiding the text parsing this RFC argues against. `original_chars` is `null` when `truncated` is `false` (nothing was cut). See “Statistics and truncation” below for what this field does and does not promise. ### Statistics and truncation Symex time, VCC counts and solver time exist only inside CBMC's free-text messages; extracting them requires pattern-matching human-readable output, which causes the fragility this RFC is intended to prevent. `benchcomp` does exactly this today; the right fix is structured data from CBMC, not more scraping. The `warnings` field carries CBMC's messages as non-contractual free text, subject to the caps below: CBMC's `--json-ui` stream tags each message with a `messageType` (e.g. `"WARNING"`), and this schema includes the `WARNING`-typed messages, for example the SAT backend's `warning: ignoring forall` / `warning: ignoring exists`, emitted when it cannot encode a quantifier with non-constant bounds. Later upstream [PR model-checking#4719](model-checking#4719), present at `10bc1ae04` but absent at `902daa525`, explicitly parses these prefixes, counts the ignored quantifiers, and overrides the property-derived result with failure and `FailedProperties::Error`. This internal interpretation does not make warning text a versioned interface: an export consumer treats each message as opaque display text and uses Kani's computed outcome instead of pattern-matching it. Two consequences: - **`warnings` is outside the `schema_version` compatibility guarantees.** The field's presence and its `[{ "message": …, "truncated": …, "original_chars": … }]` shape are contractual; the *contents* of `message` are not, and must not be pattern-matched or assumed stable across versions. - **`warnings` is bounded, with explicit, structural truncation markers.** The PoC collects warning strings without a length or count cap, so it places no fixed bound on their contribution to file size. This proposal caps each `message` at a fixed, implementation-defined length and truncates it on a character boundary, with the fact and extent carried as siblings `truncated: bool` and `original_chars: integer | null` (pre-truncation count, `null` exactly when `truncated` is `false`) rather than a suffix inside `message`. The per-harness `warnings` array is separately capped at a fixed count, with a sibling `warnings_truncated` integer per harness (`0` when nothing was dropped) recording how many *entries* were omitted. A consumer can always tell "no more warnings" from "we stopped recording". These structural fields are schema-versioned; the `message` text is not. ### Warning retention by outcome Warnings do not depend on a property result array: CBMC may emit messages and then crash or be killed. The PoC at `7b125f1b` preserves collected warnings on its no-results crash/OOM path. Its timeout path instead constructs a fresh result with no warnings. The export preserves whatever warnings the driver retains, applying the same caps for every outcome; `[]` means none were retained, not proof that CBMC emitted none. ## 3. Migration inventory The inventory wording below is retained from the longer draft. Its shorthand for per-property detail is inconsistent with that draft’s field tables: successful checks are counts, and `other[]` holds only `{id, status}`. The RFC retains those field-table definitions unchanged. - **Shipped fields dropped or transformed in this shape — keep, drop, or make mandatory?** model-checking#4472's document (`create_metadata_json`, `create_harness_metadata_json`, `process_cbmc_results` in `kani-driver/src/frontend/schema_utils.rs`) carries a number of fields this schema does not restore as-is. Grouped by proposed treatment: - **Dropped, no successor field today:** `build_mode` (`"debug"`/`"release"`); `harnesses[].mangled_name` (see “Why not `mangled_name`” in §2); the source range's `end_line` (only `original_start_line` survives, as `harnesses[].line`); `goto_file` (the generated modeling file path); per-check `description`/`location` for every property, not just the failed and `other`-bucketed ones (the shipped shape records full detail for every check; this schema records identities only for `success`/`unreachable`/`undetermined`/`error`/`unknown`, and full records only for `failed_properties`/`unsupported_constructs`/`other[]`); CBMC's OS banner (`cbmc_metadata.os_info`); and CBMC execution statistics (`cbmc_stats`: symex time, VCC counts, solver time — see "Why is CBMC statistics data excluded?" and the "Per-check timing" future-work item). - **The effective `--object-bits` value stays an open question.** It configures CBMC's pointer-object encoding and is useful verification provenance. The shipped writer already records it per harness at `cbmc[].configuration.object_bits`, resolving either Kani's default or the explicit `--cbmc-args` value. Its source is per-run state, so this schema could restore it under `configuration` or retain a per-harness field. On triage (model-checking#4731) a maintainer (feliperodri) classed it niche relative to `is_bounded`. Leaving it dropped is a provenance gap: adopting this RFC should file (or update) a tracking issue for its representation, resolved before or as part of stabilization. - **The Cargo provenance `project.workspace_root` / `output_dir`, and `harnesses[].file`'s base directory.** `harnesses[].file` is written relative to the invocation directory (`std::env::current_dir()`), not any field this document carries; for a `cargo kani` run from the workspace root the two coincide, but for a standalone `kani-driver` invocation or a script that `cd`s first they need not. Restoring `workspace_root` (or defining `file` as workspace-relative) makes `file` resolvable by a consumer that does not trust the launch directory. `--target-dir` does affect `output_dir`: Cargo builds derive it as `<target-dir>/kani/<triple>/debug/deps` (using Cargo's target directory when the flag is absent). It can stay dropped as an artifact-location field, but cannot be assumed to use the default path. - **`is_ctor_based`** is absent from `HarnessMetadata` and the shipped writer at `902daa525`, but present in both at later upstream `10bc1ae04`. There it records constructor-based generation or mined-invariant filtering: success covers only values admitted by that mechanism. This is a soundness-relevant restriction, independently of `is_bounded`. Its representation remains open in this draft, but support for exporting these harnesses must carry the restriction explicitly before stabilization; omitting it cannot justify reading their results as unrestricted proofs. ## 4. Configuration explanations and implementation inventory **`configuration.checks.assertion_reach_checks`.** Whether Kani inserted reachability checks ahead of ordinary assertions (`true` unless `--no-assertion-reach-checks` was passed). With reach-checks off, an assertion made unreachable by a contradictory `kani::assume` is recorded in `checks.success` instead of `checks.unreachable`, silently preventing the vacuity indication this schema provides; `configuration` records exactly such toggles that change how a result must be read. **`configuration.checks.ignore_global_asm` and `.extra_pointer_checks`.** Two more flags recorded for the same reason. `ignore_global_asm` mirrors `--ignore-global-asm`: when `true`, Kani did not error on `global_asm!`, so any behavior reachable only through that inline assembly is absent from the model and a proof can pass vacuously with respect to its effects. `extra_pointer_checks` mirrors `--extra-pointer-checks`: when `true`, Kani adds obligations for invalid pointers in relational operations and pointer-arithmetic overflow, so two runs differing only in this flag check different property sets, and `checks.total`/`checks.success` are not comparable between them. **`configuration.checks.memory_safety`, `.overflow`, `.unwinding`, and `.undefined_function`.** The remaining four `checks` bools, each mirroring a `--no-*-checks` flag (all default `true`; the field name records the check being *on*, not the flag that turns it off): - `memory_safety` mirrors `--no-memory-safety-checks` (and `--no-default-checks`, the whole group). `false` leaves out-of-bounds accesses and invalid-pointer dereferences unchecked; such a run can pass while containing the memory-safety bugs Kani is intended to detect. - `overflow` mirrors `--no-overflow-checks`. `false` omits CBMC's NaN check and disables its division-by-zero check. It does **not** disable Rust/MIR arithmetic-overflow or integer division-by-zero assertions: Kani still compiles with `-C overflow-checks=on` and emits those MIR assertions (subject separately to `prove_safety_only`). - `unwinding` mirrors `--no-unwinding-checks`. `false` stops CBMC asserting the loop/recursion bound covered every execution, so a bounded proof can silently miss behavior past the bound. - `undefined_function` mirrors `--no-undefined-function-checks`. `false` skips Kani's generation of `assert-false-assume-false` bodies for undefined functions. Calls remain, with CBMC's default nondeterministic-return behavior; this does not model their possible side effects. **`configuration.checks.assert_contracts` and `.prove_safety_only`.** These flags change generated checks and assumptions, and therefore what a successful result establishes: - `assert_contracts` mirrors `--no-assert-contracts` (`true` unless it was passed; it requires `-Z function-contracts`). When `false`, ordinary calls to contracted functions use `ContractMode::Original`: the original body executes and its contract instrumentation is omitted (`kani_middle/transform/contracts.rs`). The contracts are neither asserted nor assumed, so success does not establish those contract obligations. Explicit `proof_for_contract` checking and `stub_verified` replacement modes take precedence and retain their respective instrumentation. - `prove_safety_only` mirrors `--prove-safety-only` (default `false`; requires `-Z unstable-options`). When `true`, `codegen_assert_assume` emits only an assumption for `PropertyClass::Assertion`. This includes ordinary user assertions and panic checks; success is conditional on those assumptions, not evidence that the converted assertions hold. Direct `codegen_assert` calls remain checks, including the internal `CheckHook`'s `Assertion`-class properties. The conversion is specific to the code-generation path, not every property with that class. All nine meet the same "changes which properties are generated, or what a status means" test. **Partial inventory of `VerificationArgs` (at `902daa525`).** Recorded directly: the nine `checks` bools, `coverage_enabled`, and `cbmc_args`. Recorded elsewhere in the document, so not duplicated here: `-Z` features that add or remove properties (`uninit-checks`, `function-contracts`, `loop-contracts`, `mem-predicates`, `quantifiers`, `stubbing`) are visible by name in `enabled_unstable_features`; `--unwind`/`--default-unwind` in per-harness `resolved_unwind`, resolved in the order CLI `--unwind` > harness `#[kani::unwind]` > `--default-unwind` (`is_bounded` instead describes autoharness argument generation); `--solver` in the per-harness `resolved_solver`; `--harness-timeout` in `harness_timeout_s` and the per-harness `outcome.kind`. This inventory is **incomplete**: `--synthesize-loop-contracts` transforms each goto model before CBMC, while `-Z restrict-vtable --no-restrict-vtable` disables virtual-call restriction without changing the recorded `-Z` feature set. Neither effective setting is represented in the proposed fields. Their representation and the rest of the inventory must be resolved under the policy before stabilization; `cbmc_args` does not capture Kani-generated options. The proposed exclusion of `--randomize-layout [seed]` is a scope choice: it changes the *program under test* (type layout), so its seed belongs in a future subject/provenance block. Presentation and execution options also need individual treatment: regular/terse output controls rendering, but `--output-format=old` uses mock results and is rejected with export. At `902daa525`, `--quiet` suppresses the failure exit in `print_final_summary`, so a failed harness can be exported as failed while Kani exits 0. That is a driver bug, not a different verification verdict. `--jobs` changes concurrency and can affect resource outcomes and which results exist under fail-fast; `--concrete-playback` changes trace generation and formula slicing as well as producing tests. These options cannot all be classified as affecting only presentation. Future flags must be assessed under the same policy in the PR that adds them. **`configuration.coverage_enabled`.** Mirrors `--coverage` (mandatory bool, default `false`). It causes `code_coverage` (`COVERED`/`UNCOVERED`) properties to exist; these are excluded from `checks`, `covers`, and `n_properties`, so it meets the `configuration` policy, and without it a consumer cannot tell "no coverage properties in this schema yet" from "`--coverage` never passed." It sits alongside `checks.*`, not nested under it. The configuration policy itself remains in the RFC. ## 5. Deferred provenance and memory work - **Full tool & solver provenance beyond `kani`/`rustc`/`cbmc`.** An earlier draft of this schema recorded `goto_cc`/`goto_instrument`/`goto_synthesizer` versions and a `tools.solvers[]` array of `{name, version}` per resolved solver (the shape the shipped model-checking#4472 writer already emits), plus a proposed `source: "builtin"|"external"` discriminator (this schema's own addition, not part of model-checking#4472) to disambiguate a `null` version. Cut from v1 to keep it to the core (per [model-checking#4731](model-checking#4731)): probing the extra tools' and external solvers' `--version` spawns a process per tool beyond the probes v1 already needs, and the solver CBMC ran with is already recoverable per harness from `harnesses[].resolved_solver`. A follow-up can restore the fuller `tools.solvers[]` block if a consumer needs the solver *binary* versions. **File a tracking issue on adoption.** - **Host machine environment (`machine`).** An earlier draft carried `machine.cpu_count`, `.total_memory_bytes`, `.memory_limit_bytes`, `.os`, `.arch`. Cut from v1: environment metadata that helps triage performance/OOM but is not needed to reproduce a verdict. A follow-up can reintroduce a `machine` block if performance-oriented consumers ask for it. **File a tracking issue on adoption.** - **Per-check timing and resource data.** Used elsewhere (GNATprove reports per-obligation prover data), but not available from CBMC's structured output today. - **A machine-reproducible counterexample.** `--concrete-playback` already derives a concrete value vector; exposing it would let a consumer reproduce a failure without modifying source. - **A finer failure classification.** Kani computes whether a failure involved unwinding assertions or reachable undefined functions, then collapses them; separating them would let a consumer tell "raise `--unwind` and retry" from "fix the code". - **A harness-level triviality signal**, aggregating what RFC 0003 already identifies as the vacuity concern. - **Aggregate coverage**, deferring to `kani-cov` and RFC 0011. - **The contract trust chain.** A harness using `stub_verified` is sound only if the contract's own proof passed. Kani already enforces at compile time that such a harness exists; because this schema records both relationships, a consumer can check the run-time condition itself today, and Kani could report the resolved status later. - **Per-harness peak memory.** A `getrusage(RUSAGE_CHILDREN)`-based approach was prototyped and rejected: `ru_maxrss` is a process-wide running *maximum*, not a per-child figure, so the result is order-dependent (only a harness whose peak memory exceeds that of every earlier harness gets a value; a later one with a lower peak reads `null` even under memory pressure) and is not attempted under `--jobs`, where the counter is shared across siblings. An accurate figure needs per-child accounting (e.g. `wait4()`-based rusage per child, or a per-child cgroup with its own `memory.peak`), which this schema does not attempt. Kani infers OOM from the **CBMC child's** status 137 when no property result array is available, and this schema exposes that inference as `outcome.kind == "OUT_OF_MEMORY"`. Kani normally exits 1 for the failed harness, not 137; at `902daa525`, the `--quiet` bug can instead leave its exit code at 0. ## 6. Failure and completeness explanations **Failure scenarios.** - The output path is not writable → reported as an error with a non-zero exit, never silently ignored. The verification *verdict* is computed independently and never rewritten by an export problem. The up-front marker write fails before verification starts; the terminal export runs after the harness verdicts but *before* the SARIF artifact and final summary line, so a terminal export failure aborts those remaining steps. (Whether it should suppress the SARIF write is an implementation question, not settled here.) - Any `tools.*` version cannot be determined → that field is `null`, never guessed; see "Tool provenance" above. - A harness times out, is OOM-killed, or CBMC crashes on it → that harness's `outcome.kind` (`TIMEOUT`/`OUT_OF_MEMORY`/`CRASHED`) records it and the file is still written. Run completeness is *verdict-independent*: as long as every selected harness has an entry in the terminal document, `run_state` is `COMPLETE` (a suite where every harness times out is complete accounting for unsuccessful verification attempts). `PARTIAL` means the terminal document lacks some selected harness results; `INCOMPLETE` means only the marker was published. - Kani itself crashes (a `kani-compiler` ICE, a panic in `kani-driver`, a `SIGKILL`) → no terminal document is written: the single terminal write happens once at the very end (`verify_project`), and any hard error before it unwinds past it. There is no run-level `"CRASHED"` value; all that remains is a stale `INCOMPLETE` marker (or, if the crash preceded it, whatever file already existed). See "How `run_state` and `outcome.kind` co-occur" below. - The `--export-json` path already holds a file → it is **overwritten up front with an atomic `run_state: "INCOMPLETE"` marker** once harness verification begins (after the crate is built), so an earlier run's results cannot be misread as this run's, and a run that terminates after that without finishing leaves a file that records that it did not finish (replacing an earlier delete-up-front design; see the RFC’s completeness contract and open question). - The parent directory does not exist → it is created (`create_dir_all`), matching `--sarif`. A path that is itself an existing directory fails today only when the write is attempted (the same-directory temp write cannot be created inside a file-shaped target); adopting this RFC moves that to the argument-parse-time rejection proposed under *Interaction with other flags*, so the failure occurs before any verification work, as for `--sarif`. The shipped difference is an accident of implementation order, not intentional. **How `run_state` and `outcome.kind` co-occur.** `outcome` is meaningful only once Kani reaches a terminal write, and at run level its `kind` has exactly one value: `COMPLETED`. The marker (`run_state == "INCOMPLETE"`) is written *before* that and carries no `outcome`. A run-level `outcome.kind == "CRASHED"` does not exist (see the crash scenario above); what a consumer observes instead is a stale `INCOMPLETE` marker, or a missing file. The crash indication is that staleness rather than a field value. Every producible combination: | `run_state` | `outcome` | |---|---| | `INCOMPLETE` (marker) | absent | | `COMPLETE` | `{"kind": "COMPLETED"}` | | `PARTIAL` | `{"kind": "COMPLETED"}` | | `NO_HARNESSES_SELECTED` | `{"kind": "COMPLETED"}` | Per-harness `outcome.kind == "CRASHED"` is unaffected and remains possible: the run can finish, reach its terminal write, and report that CBMC crashed on one harness. This describes one harness in a completed document, distinct from Kani never reaching the write. **`NO_HARNESSES_SELECTED` means exactly one thing: an unfiltered run of a selected project or workspace with no selectable harness** (no `#[kani::proof]`, or under `autoharness` no eligible function). It cannot arise from a `--harness` filter: a filter set that matches nothing — and, with `--exact`, any single filter that matches nothing — is rejected at harness selection (`no_harness_match_error` in `kani-driver/src/metadata.rs`, since model-checking#4743) with a non-zero exit. Harness selection precedes the `INCOMPLETE` marker write and every export, so that case produces **no document at all**, not a terminal document with a non-empty `requested_filters`. Hence in a `NO_HARNESSES_SELECTED` document `harness_selection.requested_filters == []`, `unmatched_filters == []`, and `matched_count == 0`. `unmatched_filters` is non-empty only in a `COMPLETE`/`PARTIAL` document written without `--exact`, where at least one filter matched and the named ones did not. **Cover-only vacuity is not detected by this schema alone.** The RFC’s normative and advisory vacuity predicates read only `checks.*`; an `unreachable` *cover* is recorded in `covers.unreachable` and satisfies neither. A consumer wanting the corresponding indication for covers should additionally apply `covers.total > 0 && covers.unreachable.len() == covers.total` per harness, since this schema does not apply it for them. `null` always means *not measured or not applicable*, never a guess, and is always distinguishable from `0`, `false`, and `[]`. ## 7. Casing and requested versus resolved values **Casing.** The file mixes three conventions, and one rule explains all three: *a value keeps the serialization of the Rust type it comes from, and this schema does not fork types to re-case them.* - **snake_case keys**, because the schema reuses `kani_metadata` and `cbmc_output_parser` types directly (`HarnessAttributes`, `AssignsContract`, `CheckStatus`); re-casing would fork those types, recreate the duplication problem in [model-checking#3541](model-checking#3541), or break existing `.kani-metadata.json` consumers. Those three already derive `Serialize`; but `Property`, `PropertyId`, and `SourceLocation` derive only `Deserialize` (never serialized out), so `failed_properties[]`/`unsupported_constructs[]`/`checks.other[]`/`covers.other[]` are purpose-built export structs rather than a direct embedding of `Property`. - **SCREAMING_SNAKE_CASE enum values** (`outcome.kind`, `verdict`, `failure_kind`, `run_state`, every `status`), mirroring the reused CBMC-status types (`CheckStatus`, `FailedProperties`); the new enums (`Outcome`, `verdict`, `run_state`) use it too, so a consumer sees one value convention across the file. (Multi-word values like `NO_HARNESSES_SELECTED` need an explicit `SCREAMING_SNAKE_CASE` rename, since `CheckStatus`'s `UPPERCASE` coincides with it only for single-word variants.) - **PascalCase, object-shaped**, for the two embedded `kani_metadata` attribute enums below, which keep their own serde derivation untouched for the same no-forking reason. **Fields that are not always strings.** Two reused `kani_metadata` enums have non-unit variants and so serialize as *objects*, not strings: - `harnesses[].attributes.kind` is `"Proof"` or `"Test"`, but `{"ProofForContract": {"target_fn": "…"}}` for a contract-proof harness. - `harnesses[].attributes.solver` is `"Cadical"`, `"Z3"`, etc. for a named solver, but `{"Binary": "…"}` for a custom solver path. These are the *requested* attributes, carried verbatim from `.kani-metadata.json`; the resolved counterparts (`resolved_solver`, `resolved_unwind`) are plain scalars (a string or number, or `null`), never the object forms above. **Reconciling the two solver spellings.** `attributes.solver` is the *requested* value in `CbmcSolver`'s PascalCase (`"Cadical"`, or `{"Binary": "<path>"}` for a custom solver); `resolved_solver` is the lowercase built-in name or custom binary path CBMC actually ran with. Effective precedence is the last solver-selecting `--cbmc-args` override > CLI `--solver` > harness attribute > default: Kani appends `cbmc_args` after its own solver flags. Bare `--smt2` leaves the choice to CBMC and yields `null`. Compare `attributes.solver` against `resolved_solver` for "asked for" vs "ran". This proposal follows `kani list` by recording tool version and schema version in separate fields; see the RFC’s **Compatibility policy**. </details> --------- Co-authored-by: Felipe R. Monteiro <felisous@amazon.com>

tautschnig requested a review from a team as a code owner August 5, 2026 15:51

Copilot AI lite review requested due to automatic review settings August 5, 2026 15:51

github-actions Bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Aug 5, 2026

Copilot started reviewing on behalf of tautschnig August 5, 2026 15:51

View session

tautschnig mentioned this pull request Aug 5, 2026

Autoharness: mine constructor assertions into value filters #4718

Merged

Copilot AI reviewed Aug 5, 2026

View reviewed changes

Comment thread kani-driver/src/autoharness/mod.rs Resolved

Comment thread kani-compiler/src/kani_middle/mod.rs Resolved

feliperodri added the Z-Autoharness Issue related to autoharness subcommand label Aug 6, 2026

This was referenced Aug 6, 2026

Autoharness: unbounded slice, mutable slice and Vec arguments #4721

Merged

Autoharness: mine type invariants from a type's own assertions #4722

Merged

Fix three constructor-discovery ICEs from the crates.io sweep #4725

Merged

feliperodri added this to the Autoharness milestone Aug 18, 2026

feliperodri force-pushed the ctor-pr branch from 00b63ea to df99a58 Compare August 25, 2026 14:24

feliperodri requested a review from a team as a code owner August 25, 2026 14:24

feliperodri approved these changes Aug 25, 2026

View reviewed changes

feliperodri enabled auto-merge August 25, 2026 14:42

feliperodri added this pull request to the merge queue Aug 25, 2026

github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Aug 25, 2026

feliperodri added this pull request to the merge queue Aug 25, 2026

github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Aug 25, 2026

feliperodri added 2 commits August 25, 2026 12:03

Merge branch 'main' into ctor-pr

8dfba40

feliperodri enabled auto-merge August 25, 2026 16:18

feliperodri mentioned this pull request Aug 25, 2026

Autoharness --constructor-args: an unsatisfiable constructor yields a vacuous (always-Success) harness #4757

Closed

feliperodri added this pull request to the merge queue Aug 25, 2026

Merged via the queue into model-checking:main with commit d5e7a7c Aug 25, 2026
33 of 34 checks passed

feliperodri mentioned this pull request Aug 25, 2026

Upgrade Rust toolchain to nightly-2026-06-01 #4760

Merged

ivmat mentioned this pull request Sep 8, 2026

RFC: Structured verification results (export-json) #4727

Merged

CYJ904 mentioned this pull request Oct 6, 2026

Autoharness: add --alias-arguments to model aliasing between arguments #4958

Open

feliperodri added the [C] Feature / Enhancement A new feature request or enhancement to an existing feature. label Nov 6, 2026

Navigation Menu

Repository navigation

Autoharness: constructor-based value generation (--constructor-args) - #4717

Autoharness: constructor-based value generation (--constructor-args)#4717
feliperodri merged 3 commits into
model-checking:mainfrom
tautschnig:ctor-pr

tautschnig commented Aug 5, 2026 •

edited by feliperodri

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

tautschnig commented Aug 5, 2026 • edited by feliperodri Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

Changes from the original branch (rebase onto main)

Testing

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

tautschnig commented Aug 5, 2026 •

edited by feliperodri

Loading