Skip to content

Standardize Rust formatting - #370

Draft
leynos wants to merge 9 commits into
harden-lint-installerfrom
harden-lint-rustfmt
Draft

leynos wants to merge 9 commits into
harden-lint-installerfrom
harden-lint-rustfmt

Conversation

@leynos

@leynos leynos commented Aug 30, 2026 •

Copy link
Copy Markdown
Owner

Summary

This branch adopts the estate rustfmt profile and reformats the workspace under it. The change is mechanical — no behaviour changes accompany it — which is exactly why it is isolated here rather than mixed into the fix PRs below it in the stack, where it would have buried them.

The profile requires a nightly rustfmt. It enables crate-granular imports grouped std-external-crate, doc-comment code formatting, comment and string wrapping, single-line functions, try shorthand, and field-init shorthand.

Sixth PR in the lint-hardening stack, based on harden-lint-installer.

Review walkthrough

  • .rustfmt.toml is the only file worth reading closely. Note the ignore list: the Dylint UI fixtures under examples/ are excluded because their .stderr expectations match compiler output byte for byte, including line and column numbers — reformatting them silently shifts those spans and breaks the suite. Fixtures under ui/ need no entry, as they are not Cargo targets.
  • The remaining 298 files are pure reformatting; reviewing them line by line is not a good use of anyone's time. The validation below is the substantive check.
  • The three rstest fixtures that fn_single_line collapsed onto one line gained the existing allow_fixture_expansion_lints attribute: the collapsed body trips unused_braces inside the #[fixture] expansion, and this attribute scopes the allowance to the generated code rather than to the surrounding module.

Validation

  • cargo fmt --all -- --check: pass, and idempotent.
  • make markdownlint: pass, 76 files, 0 errors.
  • Hosted CI is green on this exact head. Run
    38934959335 is
    success against f3392ba, and its linux-full job
    (log)
    covers the gates this PR is judged on. It was dispatched by
    workflow_dispatch, because this branch cannot receive a pull_request
    run — see the stack note below.
    • Check formatting — pass.
    • Lint (make lint) — pass, 3m21s.
    • Full workspace suite, run by make publish-check via
      nextest run --profile ci: 1665 tests run: 1665 passed (5 slow),
      5 skipped
      , 0 failures.
    • Enforce en-GB-oxendict spelling, Nixie, Markdown lint,
      Workflow contract tests, Publish dry run — all pass.
    • The suite figure includes the three tests that use the Dylint
      example-harness lock, which is where local runs are affected (see the
      notes below).
  • Reviewed specifically for format_strings corruption: reformatting can split a string literal mid-escape, turning \n into a literal n, which compiles cleanly and only surfaces in exact-match assertions. Both corruption signatures were swept across every reformatted file — a continuation backslash followed by an escape-body character, and a line ending in an escaped backslash. Five multi-line literals were flagged by the first sweep and all five are legitimate word-boundary continuations.

Notes

  • The stack: test-quality sweep → spelling → module structure → support-crate lint fixes → installer lint fixes → rustfmt profile → lint configuration → whitaker self-linting gate.

  • This PR cannot receive pull_request CI, and that is a stack condition,
    not a property of the diff.
    refs/pull/370/merge does not exist, unlike
    every other layer (Correct en-GB-oxendict spellings in code symbols and prose #363 347a9dd3a, Adopt directory-based module structure #364 9cc02773f, Fix workspace-lint violations across support crates #365 1f53b6486,
    Fix workspace-lint violations across the installer #369 c797fbaca, Harden workspace lint, format, and documentation gates #371 ba9d750a5, Run the Whitaker suite over Whitaker's own sources #372 39b4757f0). GitHub only recomputes
    a merge ref when it can attempt the merge, and the harden-lint-* branches
    are members of a GitHub native stack (stack 367, id 723477, base main,
    spanning Sweep test, fixture, and assertion quality #362–Run the Whitaker suite over Whitaker's own sources #372 plus Plan: Collect brain trust diagnostics into a SARIF emitter (6.5.1) #354 and Record an ADR formalizing the brain trust lint driver interfaces (6.1.3) #358; readable at
    GET /repos/leynos/whitaker/stacks/367). The stack
    primitive rejects base changes outright — re-asserting the current base
    returns 422 Cannot change the base branch because the pull request is part of a stack — and it will not recompute a member's merge ref while a lower
    layer conflicts. The break is at Fix workspace-lint violations across support crates #365: it forked from harden-lint-modules
    at ab2bc5195 (2026-08-28) and its base has since gained 108 commits, so a
    merge produces 87 conflict records (75 content, 1 rename/delete, 11
    add/add) and it reports CONFLICTING/DIRTY. Correct en-GB-oxendict spellings in code symbols and prose #363 and Adopt directory-based module structure #364 are
    MERGEABLE/CLEAN; Fix workspace-lint violations across the installer #369, Standardize Rust formatting #370 and Run the Whitaker suite over Whitaker's own sources #372 all read UNKNOWN. The push at
    16:44:59Z and the close/reopen at 17:28Z should both have fired
    synchronize/reopened, and neither did. ci.yml has no draft guard, so
    draft status is not the cause. Fix workspace-lint violations across support crates #365's repair belongs to its own PR.

  • A local make test cannot complete on this shared host, for one reason.
    This is not a property of this diff — the same commit is green in CI, where
    the condition does not exist.

    This host routes every rustc invocation through a shared build-limits
    supervisor with a small compile-slot pool. With ~176 build-limits-rustc
    processes queued by other agents, the Dylint UI tests could not build their
    lint libraries: compile requests sat 75-265 deep and expired. That produces
    four failures, and each one names the cause in its own panic message:

    test panic site cause
    example_compiles_without_diagnostics::case_1 tests/ui.rs:88 harness-lock timeout
    example_harness_collects_call_site_evidence tests/ui.rs:105 RunnerFailure → failed to build lint library
    ui::aliased_test_crate_non_companion_… lib_ui_tests.rs:95 LibraryBuildFailed
    sha2_0_11_pre_migration_patterns_… trybuild run.rs:63 LibraryBuildFailed

    The lock timeout is a consequence of the same starvation, not a separate
    fault. The example-harness lock is deliberately held across the whole example
    run — including the lint-library build — so a test that is stuck waiting for
    a compile slot holds the lock the whole time. Observed directly: the lock
    owner was a ui test whose child cargo build was parked in
    build-limits-rustc (wchan=poll_schedule_timeout, 0 CPU ticks over 20 s),
    holding /tmp/rstest-helper-example-harness.owner-lock. A sibling then span
    the 31-minute (1860 s) ACQUIRE_TIMEOUT and panicked.

    The final local run logged
    1631/1652 tests run: 1621 passed (1 slow), 10 failed, 5 skipped before the
    harness stopped it at 60 minutes with whitaker_clones_core cases still
    waiting for slots; the 10 failures are retries of those same 4 tests. Treat
    this run as inconclusive, and the hosted run above as authoritative.

    Separately, make lint failed twice at its first step (cargo doc) on the
    same starvation — whitaker sat at "0 ahead" for 270 s and admission
    expired, with build-limits-status unqueryable ([Errno 11]). Once the pool
    drained, the same commit passed cleanly: cargo doc 22 s, then clippy
    --workspace --all-targets --all-features -- -D warnings in 2 m 16 s, exit 0.

  • Why local and CI differ on the compiler wrapper. Upstream
    dylint_testing-6.0.1 recognises a compiler invocation by testing whether the
    first argument is rustc (upstream src/lib.rs:345). Locally,
    ~/.cargo/config.toml sets rustc-wrapper, so Cargo reports
    Running `<wrapper> /path/rustc --crate-name …` , the first argument is the
    wrapper, and a local UI run dies with Found no `rustc` invocations. CI sets
    RUSTC_WRAPPER: sccache and has no repository rustc-wrapper configuration,
    so it does not reproduce this: the CI log for the run above contains zero
    occurrences of either signature. The workspace carries a vendored patch for
    this case, pushed on harden-lint-support-crates (424cf7a); this PR's base
    d6af163 forked before it landed and so does not inherit it. That is a
    stack-ordering fact, not a defect in the reformat.

    This diff changes no manifest, lockfile, nextest configuration, or test
    expectation: .config/nextest.toml, Cargo.toml, Cargo.lock,
    crates/no_unwrap_or_else_panic/src/lib_ui_tests.rs and
    crates/rstest_helper_should_be_fixture/tests/ui.rs are byte-identical to the
    base. The one non-mechanical file in the diff, tests/ui/harness_lock.rs,
    differs by a single collapsed accessor whose logic and constants are
    unchanged.

References

leynos added 7 commits August 28, 2026 19:39
Establish the base of the lint-hardening PR stack: the test, fixture,
helper, and assertion improvements, separated from the lint-config,
formatting, and rename changes stacked above so each review stays
scoped.

- Fixtures and setup helpers become fallible and propagate errors; the
  test body performs the unwrap with a descriptive expect. rstest
  fixtures are consumed as `#[from(fixture)] fixture_res: Result<..>`
  so bindings keep their names.
- Assertion blocks are decomposed into named helpers, pure queries, and
  single-purpose assertion macros; duplicated step logic is extracted
  (binstall value comparison, adjacency neighbour lookup, CLI default
  condition tables).
- Test modules gain explanatory `//!` opening lines; self-named test
  module files move to `mod.rs` form.
- `test_support` gains scoped environment helpers backed by `temp_env`
  alongside the existing guard; a new `whitaker_test_macros` crate
  provides `allow_fixture_expansion_lints` for fixture expansion noise.

Symbols follow main's current API; renames and signature changes land
in their own PRs above this one.
Follow-up pass over the base sweep, driven by a seven-category audit:

- whitaker_sarif: collapse ~18 near-identical serde match-panic
  round-trip blocks into shared test-support helpers (JSON round-trip
  and serialize-then-check), keeping match-panic internally so the
  helpers stay clean under a future no-expect-outside-tests gate.
- config_loading behaviour steps: extract the repeated shared-config
  lookup into one fallible helper feeding five thin then-steps.
- behaviour_cli support assertions: decompose the monolithic assertion
  functions into fallible lookups, pure queries, and thin wrappers,
  following the toolchain_steps exemplar.
- whitaker_clones_core: split assert_region's fallible computation from
  its equality assertion, and convert ten ast tests whose Result
  returns were decorative (every `?` on always-valid literal
  constructors) into plain asserting tests with descriptive expects.
Rename code symbols and prose to Oxford spelling (-ize/-yze for the
-ise pairs; analyse-family words correctly keep -yse): normalize,
localize, summarize, recognized, serialize, and the SARIF domain terms
Artifact -> Artefact across whitaker_sarif and its consumers.

The SARIF 2.1.0 wire format spells its properties `artifactLocation`
and `artifacts`, so those fields carry explicit `#[serde(rename)]`
pins with doc comments explaining that the wire name is fixed by the
schema rather than derived from the field name. External identifiers
(`CompilerArtifact`, cargo metadata types, GitHub Actions flags) keep
the external system's spelling.

Feature files and step definitions are renamed together, and the typos
configuration is pruned from 255 ignore patterns to the residual set
the corrected tree still needs, so the spelling gate now enforces the
convention.

A handful of self-named module files move to mod.rs form here because
the renames were entangled with those moves.
Move the remaining self-named module files to mod.rs form
(install_flow, toolchain) and extract oversized in-src test modules
into sibling files (list, workspace, downloader, the non-UTF-8
boundary tests, the dependency-binary fakes, and the deps repository
tests), each wired with the repo's `#[cfg(test)] #[path]` convention
and opening with an explanatory `//!` line.

The moves are content-preserving: extracted test bodies are this
tree's code verbatim; only the module structure changes. This keeps
every module inside the 400-line budget the lint configuration later
in this stack will enforce, without entangling the structural review
with lint fixes.
Behaviour-preserving refactors across common/, whitaker_sarif,
whitaker_clones_core, the lint crates, the suite, and the root crate,
clearing the violations a stricter lint configuration later in this
stack will enforce, while staying green under the current gates:

- panic-prone operations give way to descriptive errors or checked
  alternatives (indexing and slicing via get/split_at_checked, no
  unwrap/expect outside tests, no panicking closures in Result
  contexts);
- shadowed bindings are renamed meaningfully; wildcard matches name
  their single variants; string pushes and format chains use their
  cheaper forms;
- the Dylint registration entry point moves behind a new
  declare_dylint_register_entry! macro in common, so consumer crates
  contain no unsafe tokens of their own;
- the environment-variable test guards give way to temp_env-backed
  scoped helpers, and the last EnvVarGuard consumer is ported, so the
  guard itself retires;
- missing documentation is filled in rather than waived.

Installer changes are deliberately absent; they form the next PR in
the stack.
Complete the support-crate wave with the second half of the donor's
fixes, keeping them out of the installer PR above.

Each lint crate's `impl_late_lint!` invocation moves into a private
`declaration` module carrying one reasoned expectation: the macro
expands to items with no documentable source location, so `missing_docs`
cannot be satisfied at the invocation site, and an `#[expect]` on the
macro call itself does not propagate into the expansion. The same
treatment isolates `base_newtype!`, which emits an explicit `Clone` on a
`Copy` type. Each crate then re-exports an explicit `{LINT, LintPass}`
surface rather than a glob.

The remainder are the usual behaviour-preserving fixes: parameters taken
by reference where they were needlessly moved, checked indexing and
slicing, total matches in place of `unreachable!`, meaningful names for
shadowed bindings, and assertion messages where they were missing.
Clear the installer's share of the violations a stricter lint
configuration later in this stack will enforce, while staying green
under the current gates.

Several API changes land here because the fixes require them:

- `BaseDirs` methods drop their redundant suffixes (`home`,
  `executables`, `whitaker_data`); the external `UserDirs::home_dir`
  call inside the implementation keeps its own name;
- `InstallArgs` regroups its flags into `lint_selection`, `execution`,
  and `skip` flatten structs, so no single struct carries an excess of
  booleans;
- install metrics report integer permille rather than a float rate, so
  assertions compare exactly instead of within a tolerance;
- test helpers that previously panicked (`LocalServer::start`, the
  fake-binary writers, `load_cargo_toml`, `extract_binstall_table`)
  return `Result` and let callers propagate;
- parameters that were needlessly moved are taken by reference;
- the repository-release install path moves to its own module, with
  its executor, tool, and dependency grouped into a
  `RepositoryInstallRequest` so the extraction stays within the
  argument budget;
- the root check swaps `libc::geteuid` for `rustix`, removing the last
  `unsafe` block in the installer and the `libc` dependency with it.

A `#[expect(clippy::cast_sign_loss)]` is removed rather than retained:
the timestamp arithmetic it covered now uses `div_euclid`/`rem_euclid`
and a checked conversion.
@coderabbitai

coderabbitai Bot commented Aug 30, 2026 •

Copy link
Copy Markdown

Important

Draft PR not reviewed

Draft PRs are not automatically reviewed by default.

  • Trigger a manual review

To automatically review draft PRs, update your CodeRabbit configuration:

reviews:
  auto_review:
    drafts: true
  • Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Comment @coderabbitai help to get the list of available commands.

codescene-access[bot]

This comment was marked as outdated.

leynos and others added 2 commits October 12, 2026 21:32
Reformat the affected guidance and remove duplicate blank
lines so the repository Markdown checks pass.
Adopt the estate rustfmt profile and reformat the workspace under it.
The profile requires a nightly rustfmt: it enables crate-granular,
std-external-crate-grouped imports, doc-comment code formatting,
comment and string wrapping, single-line functions, and try shorthand.

The Dylint UI fixtures under `examples/` are excluded explicitly. Their
`.stderr` expectations match compiler output byte for byte, including
line and column numbers, so reformatting them silently shifts those
spans and breaks the suite. Fixtures under `ui/` are already immune
because they are not Cargo targets.

`fn_single_line` collapses short rstest fixtures onto one line, and the
`#[fixture]` expansion then trips `unused_braces` on the collapsed
body. The three affected fixtures carry the existing
`allow_fixture_expansion_lints` attribute, which scopes the allowance
to the generated code rather than to the surrounding module.

This commit is mechanical: no behaviour changes accompany it, which is
why it is isolated from the fix PRs below it in the stack.
@leynos
leynos force-pushed the harden-lint-rustfmt branch from 9f08657 to f3392ba Compare October 16, 2026 16:44
codescene-access[bot]

This comment was marked as outdated.

@leynos leynos closed this Oct 16, 2026
@leynos leynos reopened this Oct 16, 2026

@codescene-access codescene-access Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Gates Passed
6 Quality Gates Passed

See analysis details in CodeScene

Absence of Expected Change Pattern

  • whitaker/suite/src/driver.rs is usually changed with: whitaker/suite/src/lints.rs
  • whitaker/common/tests/i18n_behaviour.rs is usually changed with: whitaker/common/tests/i18n_quality/suite.rs
  • whitaker/common/src/decomposition_advice/tests/mod.rs is usually changed with: whitaker/common/src/decomposition_advice/mod.rs
  • whitaker/common/src/test_support/decomposition.rs is usually changed with: whitaker/common/src/decomposition_advice/mod.rs
  • whitaker/installer/src/deps/tests.rs is usually changed with: whitaker/installer/src/deps.rs

Quality Gate Profile: Pay Down Tech Debt
Install CodeScene MCP: safeguard and uplift AI-generated code. Catch issues early with our IDE extension and CLI tool.

@wafflecat-df12

Copy link
Copy Markdown
Collaborator

@coderabbitai are you satisfied that the introduced proof(s) (this PR introduces no new proofs; it reflows three existing Kani harness sources — common/src/decomposition_advice/community_kani/propagate_labels.rs (4 #[kani::proof] harnesses), crates/whitaker_clones_core/src/ast/kani.rs (4 harnesses), and crates/whitaker_clones_core/src/index/kani.rs (10 harnesses)) remain substantive, rigorous, and well-founded after this change?

Published head: f3392ba8e05b04a106cd4b2dd15d19b777d95118; comparison base: d6af16316b88db83b508c015a32fa90b351a811c.

Proof inventory and claims: the three files above, 18 #[kani::proof] harnesses in total, including verify_propagate_labels_returns_vector_per_input, verify_propagate_labels_preserves_label_indices, verify_propagate_labels_zero_iterations_keeps_initial_labels, verify_propagate_labels_bounded_return_for_any_max_iterations, verify_smallest_covering_node_selects_minimal_range, verify_smallest_covering_root_fallback, verify_kind_index_is_bounded, verify_count_accumulation_is_order_independent_bounded, verify_lsh_config_new_symbolic, verify_lsh_config_new_overflow_product, verify_min_hasher_sketch_rejects_empty_input, verify_min_hasher_sketch_is_deterministic, verify_min_hasher_sketch_ignores_duplicate_hashes, and verify_lsh_index_rejects_self_pairs. This PR changes no proposition, bound, assumption, assertion, or constant value; it is a rustfmt normalization only.

Production correspondence: unchanged by this PR. The affected .rustfmt.toml options are group_imports = "StdExternalCrate", fn_single_line, hex_literal_case = "Lower", and wrap_comments.

Assumptions, trusted boundaries, domain, and bounds: unchanged. The KANI_* bound constants and const _: () = assert!(...) cross-checks are carried through verbatim apart from hex digit case (0xA076_1D64_78BD_642F to 0xa076_1d64_78bd_642f, etc. — identical values).

Verifier evidence: no Kani run is attached to this assessment. This PR does not alter any harness body, so no per-obligation outcome can have changed; I am not claiming a verifier result I did not obtain. Kani is not wired into .github/workflows/*.yml, so hosted CI does not run it either. I am happy to be corrected if you consider a fresh cargo kani run necessary.

Non-vacuity and limitations: my evidence is a token-level comparison rather than a verifier run. Normalizing comments, identifier internals, whitespace, and hex-digit case, and comparing the token multiset across base and head, gives zero differing tokens for ast/kani.rs and index/kani.rs. For propagate_labels.rs the only difference is that two use statements are merged into one group: use super::super::propagate_labels_report; plus use super::shared::bounded_iteration_count; becomes use super::{super::propagate_labels_report, shared::bounded_iteration_count}; — the same two imports, same paths, same visibility. No harness body is touched in any of the three files. The residual gap is that this proves the sources are semantically identical but is not itself a verification outcome.

Assessment-ID: PR370-PROOFS-20261016-01

Please echo the Assessment-ID and assessed base/head in your substantive reply.
This is an assessment conversation, not a request to start a formal PR review.

Check substance, rigour, foundations, and correspondence to production code. Identify each unresolved concern or missing inspection explicitly.

Context: this PR is a rustfmt normalization of 298 files (297 .rs, 1 .toml). It contains no new proof. The question is whether the reflow of existing harnesses leaves them well-founded. The PR is currently blocked below by an unrelated stack-layer defect (harden-lint-installer is missing trunk's [patch.crates-io] + vendor/dylint_testing, which breaks Dylint UI example tests), and will be rebased; I have verified the three Kani files are byte-identical between harden-lint-support-crates and harden-lint-installer, so this content is stable across that rebase.

@coderabbitai

coderabbitai Bot commented Oct 16, 2026

Copy link
Copy Markdown

Tip

For best results, initiate chat on the files or code changes.

🧩 Analysis chain

🏁 Script executed:

#!/bin/bash
set -euo pipefail
base=d6af16316b88db83b508c015a32fa90b351a811c
head=f3392ba8e05b04a106cd4b2dd15d19b777d95118
git rev-parse HEAD
git cat-file -t "$base"
git cat-file -t "$head"
git diff "$base" "$head" -- common/src/decomposition_advice/community_kani/propagate_labels.rs crates/whitaker_clones_core/src/ast/kani.rs crates/whitaker_clones_core/src/index/kani.rs .rustfmt.toml
for f in common/src/decomposition_advice/community_kani/propagate_labels.rs crates/whitaker_clones_core/src/ast/kani.rs crates/whitaker_clones_core/src/index/kani.rs; do
  ast-grep outline "$f" --items all
done
fd -i 'kani|propagate_labels|shared|Cargo.toml|rust-toolchain' common crates/whitaker_clones_core .github

Length of output: 1132


🏁 Script executed:

#!/bin/bash
gh api 'repos/leynos/whitaker/compare/d6af16316b88db83b508c015a32fa90b351a811c...f3392ba8e05b04a106cd4b2dd15d19b777d95118' --jq '{status, total_commits, files: [.files[] | select(.filename == "common/src/decomposition_advice/community_kani/propagate_labels.rs" or .filename == "crates/whitaker_clones_core/src/ast/kani.rs" or .filename == "crates/whitaker_clones_core/src/index/kani.rs" or .filename == ".rustfmt.toml") | {filename,status,patch}]}'
for f in common/src/decomposition_advice/community_kani/propagate_labels.rs crates/whitaker_clones_core/src/ast/kani.rs crates/whitaker_clones_core/src/index/kani.rs; do
  ast-grep outline "$f" --items all
  cat -n "$f"
done
fd -i 'kani|propagate_labels|shared|Cargo.toml|rust-toolchain' common crates/whitaker_clones_core .github

Length of output: 40239


🏁 Script executed:

#!/bin/bash
ast-grep outline common/src/decomposition_advice --items all --match 'propagate_labels|bounded_iteration_count|minimal_feature_vector|label|iteration'
ast-grep outline crates/whitaker_clones_core/src/ast --items all
ast-grep outline crates/whitaker_clones_core/src/index --items all
ast-grep outline common/src/decomposition_advice/community_kani/shared.rs --items all
cat -n common/src/decomposition_advice/community_kani/shared.rs
rg -n -C3 'cfg\(.*kani|cfg_attr\(.*kani|KANI_|fn (propagate_labels_report|select_smallest_covering|kind_counts|from_checked_lane_seeds_for_kani|candidate_pair_summary_for_kani|bounded_iteration_count)\b' common/src/decomposition_advice crates/whitaker_clones_core/src
rg -n -i -C2 '\bkani\b|unwind|overflow' Makefile Cargo.toml common/Cargo.toml crates/whitaker_clones_core/Cargo.toml .github

Length of output: 51593


🏁 Script executed:

#!/bin/bash
for f in common/src/decomposition_advice/community.rs crates/whitaker_clones_core/src/ast/features.rs crates/whitaker_clones_core/src/ast/tree.rs crates/whitaker_clones_core/src/ast/lowering.rs scripts/run-kani.sh; do
ast-grep outline "$f" --items all
done
sed -n '130,342p' common/src/decomposition_advice/community.rs
cat -n crates/whitaker_clones_core/src/ast/cover.rs
sed -n '1,65p;155,170p;220,265p' crates/whitaker_clones_core/src/ast/features.rs
sed -n '1,110p' crates/whitaker_clones_core/src/ast/tree.rs
sed -n '145,255p' crates/whitaker_clones_core/src/ast/lowering.rs
cat -n crates/whitaker_clones_core/src/index/types.rs
cat -n crates/whitaker_clones_core/src/index/lsh.rs
sed -n '1,155p;275,370p' crates/whitaker_clones_core/src/index/minhash.rs
cat -n scripts/run-kani.sh
cat crates/whitaker_clones_core/Cargo.toml
gh api 'repos/leynos/whitaker/compare/d6af16316b88db83b508c015a32fa90b351a811c...f3392ba8e05b04a106cd4b2dd15d19b777d95118' --jq '.files[] | select(.filename | test("^common/src/decomposition_advice/(community.rs|community_kani/shared.rs|vector.rs)$|^crates/whitaker_clones_core/src/(ast/(features|cover|tree|lowering).rs|index/(types|lsh|minhash).rs)$|^scripts/run-kani.sh$|Cargo.toml$")) | {filename,patch}'

Length of output: 76533


🏁 Script executed:

#!/bin/bash
sed -n '192,220p' crates/whitaker_clones_core/src/ast/features.rs
ast-grep run --pattern 'select_smallest_covering($$$)' --lang rust crates/whitaker_clones_core/src
ast-grep outline scripts/install-kani.sh --items all
sed -n '1,105p' scripts/install-kani.sh
rg -n -C2 'kani|unwind|overflow' .github scripts/run-kani.sh common/Cargo.toml crates/whitaker_clones_core/Cargo.toml Cargo.toml
python - <<'PY'
import pathlib,re
p=pathlib.Path('crates/whitaker_clones_core/src/index/minhash.rs')
s=p.read_text()
part=s[s.index('#[cfg(kani)]\nfn sketch_values'):s.index('/// Extracts sorted')]
indices=[int(x) for x in re.findall(r'minimum_mixed_hash\(seeds\[(\d+)\], unique_hashes\)',part)]
print('Kani MinHash lane sequence equals range(128):',indices==list(range(128)))
for name in ['common/src/decomposition_advice/community_kani/propagate_labels.rs','crates/whitaker_clones_core/src/ast/kani.rs','crates/whitaker_clones_core/src/index/kani.rs']:
 print(name, pathlib.Path(name).read_text().count('#[kani::proof]'))
PY

Length of output: 10107


🤖 web_search executed:

Kani Rust verifier 0.67 loop unwinding bound loop runs N times unwind N+1 final condition check arithmetic overflow default checks documentation

Length of output: 944


@wafflecat-df12 accept the narrow preservation claim, but keep it separate from a claim that all 18 harnesses establish their properties successfully. The formatting change preserves the inspected proof obligations. The existing harnesses remain substantive bounded checks, but inspection exposed unresolved foundations and correspondence concerns.

Assessment-ID: PR370-PROOFS-20261016-01
Assessed base: d6af16316b88db83b508c015a32fa90b351a811c
Assessed head: f3392ba8e05b04a106cd4b2dd15d19b777d95118

Preservation and substance

I confirmed the 4 + 4 + 10 inventory. I inspected the exact comparison through GitHub after the local checkout lacked the base object.

The three harness-file diffs contain only import regrouping, whitespace, comment wrapping, and hex-digit case changes. The inspected production-helper and proof-adapter diffs also preserve their logic.

The harnesses contain meaningful assertions:

  • Propagation: label-vector length, valid label indices, zero-iteration identity, and the reported iteration bound.
  • AST: minimal covering ranges, no-cover results, KindId round-tripping, and sibling-order-independent counts.
  • Index: constructor validation, overflowing-product rejection, empty-input rejection, selected MinHash lane properties, and bounded candidate-pair scenarios.

Do not treat token-multiset equality as semantic-equivalence evidence by itself. A multiset discards token order. The actual diffs support your preservation claim more directly.

Unresolved concerns

  1. Resolve the propagation arithmetic domain before claiming successful verification.

    symbolic_adjacency() permits independently symbolic positive u64 weights. Production score_label() uses ordinary *score += weight.

    A permitted counterexample is a complete three-node graph with every weight equal to u64::MAX. With the fixed method names, nodes 0 and 1 adopt label 1 during the first pass. Node 2 then accumulates two maximum weights for label 1. That addition overflows.

    This affects the harnesses that permit non-zero iterations. It is pre-existing, not introduced here. Either justify a production-valid aggregate-weight bound or establish the intended overflow behaviour. Do not suppress the arithmetic check merely to obtain a pass.

  2. Check the AST traversal unwind bound.

    bounded_tree() constructs five nodes. Production count_node_kinds() visits them through a while let ... pending.pop() loop. The relevant harnesses specify #[kani::unwind(5)].

    Kani normally needs an additional unwind to establish the final loop exit. Its documentation gives the corresponding N + 1 rule. Confirm this obligation with the pinned verifier; 5 appears insufficient for five body executions. The constant assertion relating unwind to tree depth does not establish a bound for this iterative node traversal. Kani unwinding documentation

  3. Limit the AST correspondence claim to the code actually exercised.

    The covering harnesses call select_smallest_covering(). The parser adapter instead uses its separate select_covering_node() implementation.

    The harness named verify_smallest_covering_root_fallback establishes that the helper returns None for two concrete scenarios. It does not establish parser-root fallback. The inspected parser selector returns AstError::SpanOutOfBounds when it selects no node.

    The counting harnesses do exercise production kind_counts(). However, they use one fixed five-node shape. Order independence alone does not establish exact counts; an always-zero implementation could satisfy that equality.

  4. Retain the index proof-adapter boundary explicitly.

    Under cfg(kani), LSH replaces production bucket storage and candidate_pairs() with bounded insertion records and candidate_pair_summary_for_kani(). The scenarios fit the adapter capacities, and both paths share CandidatePair::new(). However, these harnesses do not verify the production bucket-and-set implementation directly.

    MinHash has a narrower correspondence gap. I checked that its unrolled implementation calls the shared minimum-hash helper for lanes 0..127 in order. Nevertheless, the harnesses use proof-only seeds, concrete hash sets, and assertions on lanes 0, 64, and 127. Do not generalize those results to all inputs, all seeds, or production seed generation.

Verifier evidence and conclusion

No Kani run was supplied or performed. The configured unwind bounds and safety properties therefore remain unconfirmed. The workflow search found no Kani invocation. Ordinary tests do not close that evidence gap.

Do not require a fresh Kani run solely because these sources were reformatted. Require a pinned Kani run before asserting that all 18 harnesses pass, particularly to settle the arithmetic and unwinding concerns above.

The formatting PR preserves the existing assurance and its existing limitations. It does not introduce these concerns, and it does not resolve them. Reassess any changed proof dependencies after the rebase. I did not independently verify the stack-layer vendor defect or the claimed cross-branch byte identity.

Thanks for clarifying the assessment scope. No formal review was triggered.


✏️ Learnings added
Learnt from: wafflecat-df12
URL: https://github.com/leynos/whitaker/pull/370

Timestamp: 2026-10-16T18:44:07.575Z
Learning: In leynos/whitaker, distinguish preservation of existing Kani harnesses from successful verifier outcomes. The clone-detector wrapper scripts/run-kani.sh runs harnesses with --no-default-features, excluding the parser adapter. The covering harnesses in crates/whitaker_clones_core/src/ast/kani.rs exercise select_smallest_covering(), while parser lowering uses a separate select_covering_node() implementation. The LSH harnesses use cfg(kani)-specific storage and candidate_pair_summary_for_kani(), not production candidate_pairs(); retain this production-correspondence boundary in proof assessments.

Note: Learnings are effective only in the context of similar code segments. To apply general coding guidelines, please configure review instructions. You can manage existing learnings in the app.

You are interacting with an AI system.

@pandalump

Copy link
Copy Markdown
Collaborator

Assessment PR370-PROOFS-20261016-01 — thank you, this is a genuinely useful
scoping correction and I accept all four points.

Accepted and recorded. I am retracting the "all 18 harnesses establish their
properties" framing and keeping only the preservation claim: the reformatting
leaves the inspected proof obligations byte-equivalent in substance. I also drop
token-multiset equality as the evidence for it — you are right that a multiset
discards order, and the direct diff of the three harness files is the stronger
and more honest support.

Your four concerns are all pre-existing and out of scope for this PR, and I
have recorded them as such rather than acting on them here:

  1. Propagation arithmetic. The u64::MAX weight counterexample over a
    complete three-node graph is a real domain gap: symbolic_adjacency()
    admits weights whose sum overflows under score_label()'s plain *score += weight. A production-valid aggregate bound or an explicit overflow policy is
    the right resolution. Not suppressed here.
  2. AST unwind bound. Your N+1 reading of the Kani unwind rule is correct, and
    it matters: count_node_kinds() visits five nodes through a while let … pending.pop() loop, so #[kani::unwind(5)] may be one short of the required
    six. I have not confirmed this against the pinned verifier, so I am recording
    it as unconfirmed rather than asserting either way.
  3. AST correspondence. Agreed — verify_smallest_covering_root_fallback
    exercises select_smallest_covering(), while parser lowering uses the
    separate select_covering_node(), so it does not establish parser-root
    fallback. Your point that an always-zero implementation would satisfy a
    five-node order-independence assertion is well taken.
  4. Index adapter boundary. Agreed and preserved as stated: the LSH harnesses
    use cfg(kani) storage and candidate_pair_summary_for_kani(), not
    production candidate_pairs(), and the MinHash assertions cover lanes 0, 64
    and 127 only.

On the verifier-evidence question: no Kani run is claimed for this PR, and I
agree none is required merely because the sources were reformatted. A pinned
Kani run is required before anyone asserts the 18 harnesses pass, and that
belongs with the arithmetic and unwinding work above, not here.

One correction to my own earlier framing, for the record: the 1652/1652 passed figure I had been citing came from the August head 9f08657, where CI's
coverage-check job logged 1652 tests run: 1652 passed (5 slow), 5 skipped.
It does not describe the current candidate after the restack, and I have
removed that claim from the PR description. The current head fails make test
for two separately reproduced reasons inherited from the base layer — a
compiler-wrapper parsing defect in upstream dylint_testing-6.0.1 that the
workspace's vendored patch fixes, and a host-global example-harness lock keyed
on std::env::temp_dir() whose 31-minute acquire timeout leaves only a
one-minute margin over its 30-minute stale-recovery window. Both are recorded
in the PR description with the evidence for each.

You noted you did not independently verify the stack-layer defect or the claimed
cross-branch byte identity; neither is needed for your assessment, and I have
not asked you to.

@buzzybee-df12

Copy link
Copy Markdown
Collaborator

Correction to my own evidence statement in the previous comment, for the record.
The assessment answers above (the four accepted concerns and the retraction of
token-multiset equality) are unaffected; this is only about the validation
evidence I cited.

I was wrong that the current head fails make test, and wrong to attribute
the local failures to two independent layered defects.

Hosted CI is green on the exact candidate. Run
38934959335 is
success at f3392ba, and its linux-full job
(log)
runs the full workspace suite via make publish-check:

Summary [ 561.093s] 1665 tests run: 1665 passed (5 slow), 5 skipped

with Check formatting, Lint, spelling, Nixie, Markdown lint and
Workflow contract tests all passing. My earlier statement described a local
condition as a property of the candidate.

The two failure classes are one chain, not two defects. This host routes
rustc through a shared build-limits supervisor. While ~176 compile requests
were queued by other agents, the Dylint UI tests could not build their lint
libraries, and each failure names that in its own panic message — e.g.
failed to build lint library for rstest_helper_should_be_fixture: followed by
[build-limits] shlex: waiting for a compile slot (265 ahead, 45s).

The lock timeout is downstream of the same starvation rather than a separate
fault. The example-harness lock is deliberately held across the whole example
run, including the lint-library build, so a test parked waiting for a compile
slot holds the lock the entire time. I confirmed this directly: the lock owner
was a ui test whose child cargo build was blocked in build-limits-rustc
(wchan=poll_schedule_timeout, 0 CPU ticks over 20 s) while holding
/tmp/rstest-helper-example-harness.owner-lock; a sibling then exhausted its
31-minute acquire timeout. Four distinct tests failed — three on lint-library
builds, one on the lock — and all four trace to admission.

make lint likewise failed twice at its first step (cargo doc) on the same
starvation, then passed cleanly once the pool drained (cargo doc 22 s; clippy
--workspace --all-targets --all-features -- -D warnings, exit 0).

So make check-fmt, make lint and make typecheck all pass locally, and the
hosted suite is green; a local make test under that contention cannot complete
(1631/1652 before I stopped it) and is inconclusive rather than failing.

The vendored dylint_testing patch remains a real, separate incompatibility —
locally ~/.cargo/config.toml sets rustc-wrapper, so Cargo's --verbose
output prefixes the wrapper and upstream dylint_testing-6.0.1 rejects the
invocation because its first argument is not rustc (src/lib.rs:345). CI sets
RUSTC_WRAPPER: sccache with no config-file wrapper, so it does not reproduce
there. That patch is pushed on harden-lint-support-crates (424cf7a); my base
d6af163 forked before it landed. It is a stack-ordering fact, not a defect in
this diff, and it is not what produced the failures above.

The PR description has been corrected accordingly.

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants