[CYJ904]

Resolves #4979.

This rewrites the autoharness reference page (docs/src/reference/experimental/autoharness.md) to match the implementation on main, following the structure proposed in #4979: selecting functions, generating harnesses (arguments, assumptions, checks), verifying and reading results, soundness caveats, and an architecture overview for contributors.

How the items in #4979 are addressed:

1. Unbounded slices and Vec: new "Primitive slices and Vec" section; "Bounded Arguments" and "Arguments Implementing Arbitrary" now distinguish the primitive unbounded models from the bounded generators.
2. Fn-bound generics: "Generic Functions" (instantiation) and "Fn-bound closures" (the model and its limits).
3. Box/Rc/Arc: new "Box, Rc and Arc" section.
4. Layout niches: new "Layout niches" section under Assumptions.
5. Default settings: new "Default settings" section (60s timeout, unwind 20, and the reminder printed when a harness fails).
6. Skip reasons: new "Skip reasons" section listing every reason shown to users, plus the hidden "Kani implementation" case.
7. SIMD and const-generic rejections: "Generic Functions".
8. CLI items: --std in "Usage", --list --format in "Listing functions (--list)", and the bound flags in "Bounded Arguments".

The soundness caveats are now collected in one section: single monomorphization, aliasing between arguments, bounded arguments, vacuous constructors, and the mined-invariant heuristic. That section also has an "Other limitations" subsection that is not in the proposed structure. It lists the under-approximations that apply by default without a marker in the summary table. Happy to drop or move it if you prefer.

While writing the page we found and reported two issues, both described in the caveats:

1. Autoharness: Fn-bound closure models have no side effects, so callbacks that modify shared state are not covered #4994: the Fn-bound closure models have no side effects, so callbacks that modify shared state are not covered.
2. Autoharness --constructor-args: mined-invariant filtering of types with their own Arbitrary is not marked "(ctor)" #4995: under --constructor-args, mined-invariant filtering of a type with its own Arbitrary implementation is not marked "(ctor)".

Other fixes:

1. A link to the mined invariants section whose anchor did not match the generated heading id.
2. The overview and usage text that still said every argument must implement Arbitrary.

Notes for review:

1. If Autoharness: fail a harness that no generated input reaches #4978 merges first, the "Vacuous constructors" caveat should be updated or removed. If Autoharness: add --alias-arguments to model aliasing between arguments #4958 merges first, the aliasing caveat should point to --alias-arguments.
2. The page builds with mdBook without new warnings, and all same-page links resolve.

Contributors:

1. Selecting functions: @acearyanarun
2. Generating harnesses: @wodex1nhaoIeng
3. Skeleton, usage, verifying and reading results, soundness caveats, architecture overview, and integration: @CYJ904

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

[CYJ904]

@acearyanarun @wodex1nhaoIeng the skeleton is up: the current page moved into Felipe's structure, no wording changes yet. Could you take a look and say whether the layout works for you?

If it does, there are three parts to fill in so we don't edit the same lines:

1. Selecting functions (skip reasons, generic instantiation, --list/--format)
2. Generating harnesses (arguments, assumptions, checks)
3. Usage, results, soundness caveats, architecture

[feliperodri]

did you review these changes? do they seem helpful? @acearyanarun @Tianshu-Huang @wodex1nhaoIeng @srivatsansamraj

[Copilot]

🟢 Approval recommended

Only a minor, non-blocking section-link correction remains in this documentation-only change.

1 open issue

• Fix constructor-generation links to match the heading anchor · New

What changed in this PR

Updates the autoharness reference to reflect current implementation and organize guidance around selecting functions, generating inputs, and interpreting verification results.

Changes:

• Documents supported argument models, generic instantiation, skip reasons, and CLI options.
• Explains verification defaults, result markers, and soundness limitations.
• Adds a contributor-oriented overview of the driver/compiler pipeline.

File	Description
docs/​src/​reference/​experimental/​autoharness.md	Reorganizes and expands the autoharness reference, including modeling limits and architecture.

_{Review effort: Balanced}

[Tianshu-Huang]

I checked the page against main and everything matches, and all the #4979 items are in. The anchors are fine too, Yanjun is right about the en dash. Approving.

[wodex1nhaoIeng]

Looks good to me, but since I contributed some commits to this PR, I’m not sure whether it would be appropriate for me to review it.

[acearyanarun]

Hi Felipe, yes, I reviewed the updated documentation, particularly the function-selection and skip-reason sections I contributed to.

I noticed two minor improvements: some CLI flags in headings render as en dashes, and the function-selection order could be clarified to include the comptime and no-body checks. Neither appears blocking.

Overall, the changes look good to me!

[feliperodri]

Thanks for the restructure. The headings follow the structure proposed in #4979, and the claims I spot-checked against the code are accurate (generic instantiation candidates and limits, skip reasons, default timeout/unwind, --list and --std behavior, unbounded slice/Vec models, mined-invariant limits, Fn model shapes).

Requesting changes for the following, in priority order:

1. Add the visual overview (inline comment on the "Selecting functions" heading). This is the main change I'd like to see.
2. Fix the imprecise selection-order sentence (inline comment).
3. Make the two fragile heading anchors robust (inline comments).
4. Confirm the docs build. Only the "Auto Label" check has reported on this PR, so no CI job has built the book. Please run mdbook build docs locally and confirm there are no new warnings and no broken links, or get the docs workflow approved to run.
5. Optional, not blocking: the page is now ~790 lines. Consider a follow-up that splits it into overview, argument generation, and soundness pages.

I'll re-review once these are addressed.

[feliperodri]

Add a visual overview here. The headings follow the structure from #4979, but the three-phase diagram from that issue is not in the page; only the contributor architecture diagram at the bottom is. Readers who want the big picture first have nothing to anchor on.

Please add a short "How it works" section before this heading (after the Example) with the SELECT / GENERATE / VERIFY & REPORT diagram, and link each box to its section here (#selecting-functions, #generating-harnesses, #verifying-and-reading-results, #soundness-caveats). The diagram is in #4979 (comment). Update the arguments/assumptions/checks lists in it only where this page differs.

[CYJ904]

Added a "How it works" section after the Example with the diagram from #4979. The box titles link to their sections (#selecting-functions, #generating-harnesses, #verifying-and-reading-results, #soundness-caveats, and the architecture section). To make the boxes clickable while keeping the ASCII layout, the diagram is a raw <pre><code class="language-text"> block, so it renders the same as a regular text code block.

I compared the arguments/assumptions/checks lists against the page and every item has a matching section. The only change is "mined inv. (ctor)", since the page documents mined invariants as applying only under --constructor-args. The rest of the diagram is unchanged from the issue.

[feliperodri]

This ordering is slightly imprecise. In automatic_harness_partition (kani-compiler/src/kani_middle/codegen_units.rs) the checks run in this order:

1. Kani instrumentation functions (KaniImpl) and compile-time-only functions (Comptime), both before generic instantiation;
2. generic instantiation (GenericFn);
3. NoBody, then proof harnesses and Kani trait impls (KaniImpl), then the include/exclude filter (UserFilter), then unsupported variadic;
4. argument support (MissingArbitraryImpl / RequiresBoundedArguments).

Either list this order, or soften the sentence (for example "Selection roughly proceeds as follows") so it does not claim instantiation is the first check. The skip-reason table could also say that the first failed check wins, which it already does in the paragraph above the table.

[CYJ904]

Thanks, good catch. In 3186465 the paragraph now lists the checks in the order automatic_harness_partition runs them: Kani-internal and compile-time-only functions before generic instantiation, then the body, proof-harness/Kani trait impl, include/exclude and variadic checks, and finally argument support. The skip-reason table intro now also says its rows follow that order (they already did). I also noted that compile-time-only functions, like generic ones, are reported regardless of the filters.

[feliperodri]

The link target for this heading, #bounded-arguments-opt-in---bounded-arguments, is used in several places (skip reasons, Default settings, Formatting, Soundness caveats). It works today, but it depends on how mdBook turns the punctuation in this heading into an id, so a small mdBook change would break all of those links at once. Consider a plain heading such as ##### Bounded arguments (--bounded-arguments) or ##### Bounded arguments, and update the links. (This also avoids the near-duplicate with the ### Bounded arguments heading under Soundness caveats, which is currently disambiguated only by the suffix.)

[CYJ904]

Renamed to "Bounded argument generation" (id bounded-argument-generation) and updated all five links in 3186465. I didn't use either suggested name because each runs into one of the other concerns: "Bounded arguments (--bounded-arguments)" has a plain-text "--", so its id would depend on smart punctuation like the constructor heading, and plain "Bounded arguments" would take the soundness caveat's id and push that one to bounded-arguments-1. The flag is still named in the section's first paragraph.

[feliperodri]

Same concern as the Bounded Arguments heading: #constructor-based-generation-constructor-args only resolves because of how mdBook's smart punctuation treats the -- in a plain-text heading (Copilot flagged this and the explanation in the thread is right for the current build). Wrapping the flag in backticks, as --check-invariants already is, or dropping the flag from the heading text, would make the id independent of that setting.

[CYJ904]

Dropped the flag from the heading, so it is now "Constructor-based generation" (id constructor-based-generation), and updated both links in 3186465. "Listing functions (--list)" had the same issue (no links yet), so I dropped the flag there too.

[CYJ904]

Thanks for the careful review! All items are addressed:

1. Visual overview: new "How it works" section with the Autoharness documentation is out of date and missing several features #4979 diagram; each box links to its section.
2. Selection order: the paragraph now follows automatic_harness_partition exactly.
3. Heading anchors: both headings (and "Listing functions") no longer have punctuation that depends on mdBook settings, and all links are updated.
4. Docs build: built locally with mdbook 0.5.2 and mdbook-graphviz 0.3.1 on the final version and compared against main. No new warnings (the 4 existing ones in attributes.md and faq.md are on main too) and no new broken links; a link check over the generated HTML finds 0 broken links on the autoharness page. The PR also fixes one broken link that main has (#mined-invariants---check-invariants).
5. Happy to do the split in a follow-up PR once this one lands.