[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.

[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.