Kani verification for build_adjacency with tests and tooling#186
Merged
Kani verification for build_adjacency with tests and tooling#186
Conversation
WalkthroughEnable Kani bounded-model checking: add Kani harnesses and test seam, promote visibility for testing, add installer/runner scripts and Makefile target, register Changes
Sequence Diagram(s)sequenceDiagram
participant Dev as Developer
participant Make as Makefile
participant Run as "scripts/run-kani.sh"
participant Install as "scripts/install-kani.sh"
participant CargoKani as "cargo-kani (Kani)"
participant RustCode as "common crate (build_adjacency + harnesses)"
Dev->>Make: make kani
Make->>Run: invoke ./scripts/run-kani.sh
Run->>Install: ensure Kani installed (install-kani.sh)
Install-->>Run: return install dir and toolchain
Run->>CargoKani: set PATH and env, run cargo-kani kani [--harness filter]
CargoKani->>RustCode: execute Kani harnesses in common/
RustCode-->>CargoKani: proof results (pass/fail)
CargoKani-->>Run: exit code
Run-->>Make: propagate exit code
Make-->>Dev: display result
Poem
🚥 Pre-merge checks | ✅ 5 | ❌ 2❌ Failed checks (1 warning, 1 inconclusive)
✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
![codescene-delta-analysis[bot]](https://avatars.githubusercontent.com/in/53921?s=60&v=4){kind=small}
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Reviewer's GuideImplements a Kani-based bounded model checking workflow for the Sequence diagram for adjacency_report using build_adjacencysequenceDiagram
participant BehaviourTest as BehaviourTestDecompositionAdjacency
participant TestSupport as TestSupportDecomposition
participant Community as CommunityModule
participant Report as AdjacencyReport
BehaviourTest->>TestSupport: adjacency_report(node_count, edges)
TestSupport->>TestSupport: validate edges (bounds, left < right)
alt invalid_input
TestSupport-->>BehaviourTest: Err(String)
else valid_input
TestSupport->>Community: build_adjacency(node_count, &edges)
Community-->>TestSupport: adjacency Vec<Vec<(usize,u64)>>
TestSupport->>Report: construct AdjacencyReport(adjacency)
TestSupport-->>BehaviourTest: Ok(AdjacencyReport)
BehaviourTest->>Report: is_symmetric(), all_indices_in_bounds(), is_sorted(), neighbours_of(...)
Report-->>BehaviourTest: assertions data
end
Class diagram for build_adjacency, Kani harnesses, and adjacency test-support seamclassDiagram
class CommunityModule {
+pub(crate) fn build_adjacency(node_count usize, edges & [SimilarityEdge]) Vec~Vec~(usize,u64)~~
}
class SimilarityEdge {
-left usize
-right usize
-weight u64
+pub(crate) fn new(left usize, right usize, weight u64) SimilarityEdge
+pub(crate) fn left() usize
+pub(crate) fn right() usize
+pub(crate) fn weight() u64
}
class CommunityKaniModule {
+const MAX_NODES usize
+const MAX_EDGES usize
+fn constrained_edges(node_count usize) Vec~SimilarityEdge~
+fn verify_build_adjacency_length()
+fn verify_build_adjacency_preserves_edges()
+fn verify_build_adjacency_indices_in_bounds()
+fn verify_build_adjacency_symmetry()
+fn verify_build_adjacency_sorted_neighbours()
}
class TestSupportDecomposition {
+fn adjacency_report(node_count usize, edges Vec~SimilarityEdge~) Result~AdjacencyReport,String~
}
class AdjacencyReport {
+fn is_symmetric() bool
+fn all_indices_in_bounds() bool
+fn is_sorted() bool
+fn neighbours_of(node usize) Vec~(usize,u64)~
}
class BehaviourTestDecompositionAdjacency {
+bdd_scenarios()
}
CommunityModule "1" o-- "many" SimilarityEdge
CommunityKaniModule ..> CommunityModule : uses build_adjacency
CommunityKaniModule ..> SimilarityEdge : constructs
TestSupportDecomposition ..> CommunityModule : calls build_adjacency
TestSupportDecomposition ..> SimilarityEdge : uses
TestSupportDecomposition "1" o-- "1" AdjacencyReport
BehaviourTestDecompositionAdjacency ..> TestSupportDecomposition : uses adjacency_report
BehaviourTestDecompositionAdjacency ..> AdjacencyReport : asserts properties
File-Level Changes
Tips and commandsInteracting with Sourcery
Customizing Your ExperienceAccess your dashboard to:
Getting Help
|
leynos
changed the title
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
devboxerhub
bot
force-pushed
the
kani-verify-build-adjacency-w7ihby
branch
from
2879d10 to
bf86635
Compare
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
![sourcery-ai[bot]](https://avatars.githubusercontent.com/in/48477?s=60&v=4){kind=small}
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 851fcccb3e
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 3
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
docs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.md (1)
544-547:⚠️ Potential issue | 🟡 MinorUse consistent
-izespelling: "localization" not "localisation".Per en-GB-oxendict conventions, use the
-izesuffix. The document already uses "localization" elsewhere (line 572).Triage:
[type:spelling]Proposed fix
-- **Five separate proof harnesses for failure localisation**: the five +- **Five separate proof harnesses for failure localization**: the five🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@docs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.md` around lines 544 - 547, Replace the British spelling "localisation" with the consistent American spelling "localization" wherever it appears in this document (the occurrence flagged uses "localisation"); update the single word to "localization" to match the existing usage elsewhere and ensure consistency across the file.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@common/tests/features/decomposition_adjacency.feature`:
- Around line 13-17: The scenario title "Malformed edge input is rejected" is
ambiguous because the step "And an edge from 2 to 1 with weight 5" is in-bounds
for a 3-node graph; clarify the invariant by either renaming the scenario to
indicate the canonical-order requirement (e.g., "Rejected when edge endpoints
are not in canonical left < right order") or change the step to use an
out-of-range endpoint (e.g., use node index 3 or higher) if you intend to test
out-of-bounds rejection; update the Scenario header and/or the step "And an edge
from 2 to 1 with weight 5" accordingly to reflect which invariant is under test.
In `@docs/brain-trust-lints-design.md`:
- Around line 544-547: Replace the British spelling "localisation" with the
American "localization" in the sentence that starts "Five separate proof
harnesses for failure localisation" so it reads "Five separate proof harnesses
for failure localization"; search for the exact phrase "Five separate proof
harnesses for failure localisation" (or occurrences of "failure localisation")
and update them to "failure localization" to maintain the -ize convention.
In `@scripts/install-kani.sh`:
- Around line 63-74: Set the RUSTUP_TOOLCHAIN environment variable so Cargo uses
the Kani-installed toolchain: after determining toolchain_tag in
scripts/install-kani.sh (and when creating the symlink at
install_dir/toolchain), ensure run-kani.sh exports RUSTUP_TOOLCHAIN using that
same toolchain_tag (or read the pinned version from
install_dir/rust-toolchain-version) immediately after the PATH setup so Cargo
will prefer the Kani toolchain; update run-kani.sh to export
RUSTUP_TOOLCHAIN="${toolchain_tag}" (or the read value) before invoking
cargo/rustup commands.
---
Outside diff comments:
In
`@docs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.md`:
- Around line 544-547: Replace the British spelling "localisation" with the
consistent American spelling "localization" wherever it appears in this document
(the occurrence flagged uses "localisation"); update the single word to
"localization" to match the existing usage elsewhere and ensure consistency
across the file.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 5da14c08-12f2-44e9-8312-bb97e3c0b186
📒 Files selected for processing (16)
Makefilecommon/Cargo.tomlcommon/src/decomposition_advice/community.rscommon/src/decomposition_advice/community_kani.rscommon/src/decomposition_advice/mod.rscommon/src/decomposition_advice/tests.rscommon/src/decomposition_advice/tests/adjacency.rscommon/src/test_support/decomposition.rscommon/src/test_support/decomposition_adjacency.rscommon/tests/decomposition_adjacency_behaviour.rscommon/tests/features/decomposition_adjacency.featuredocs/brain-trust-lints-design.mddocs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.mddocs/roadmap.mdscripts/install-kani.shscripts/run-kani.sh
Owner
Author
|
@coderabbitai Please suggest a fix for this issue and supply a prompt for an AI coding agent to enable it to apply the fix. Include the file and symbol names indicated in the issue at the head of your response. common/src/decomposition_advice/community_kani.rs Comment on file fn verify_build_adjacency_sorted_neighbours() {
let node_count = constrained_node_count();
let edges = constrained_edges(node_count);
let adjacency = build_adjacency(node_count, &edges);
for bucket in &adjacency {
for window in bucket.windows(2) {
assert!(window[0].0 <= window[1].0);
}
}
}❌ New issue: Code Duplication |
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@docs/brain-trust-lints-design.md`:
- Around line 528-530: Update the description so it accurately states that
scripts/run-kani.sh runs all Kani harnesses by default and only applies a filter
when a specific harness argument is supplied; replace the current sentence that
claims it invokes the pinned cargo-kani binary filtering to
verify_build_adjacency by default with text noting the default "run all
harnesses" behavior and that passing a harness name causes the script to filter
to that harness, and ensure the make kani reference reflects this default
behavior.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 203fb15a-ce43-49e6-81e6-dd455e8cb821
📒 Files selected for processing (3)
common/tests/features/decomposition_adjacency.featuredocs/brain-trust-lints-design.mdscripts/run-kani.sh
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@docs/brain-trust-lints-design.md`:
- Around line 540-544: In the sentence under the "Harness inputs constrained to
the production edge contract" paragraph (the sentence mentioning
`build_similarity_edges` and `kani::assume`) insert a comma before the
coordinating conjunction "so" to correctly separate the independent clauses
(i.e., change "...no duplicate unordered pairs. The Kani harnesses enforce these
same `kani::assume` preconditions, so the proof covers exactly the inputs that
production code can generate.").
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: b49fe0c4-0d3e-44a9-8f81-ce0e54bcb870
📒 Files selected for processing (1)
docs/brain-trust-lints-design.md
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@docs/developers-guide.md`:
- Line 64: The section heading "Kani Bounded Model Checking" is title case;
rename it to sentence case to match docs style by changing the heading text used
in the markdown (the string "Kani Bounded Model Checking") to sentence case
(e.g., "Kani bounded model checking") so the heading conforms to the project's
documentation style rules.
- Around line 154-156: The phrase "behavior-driven" in the documentation
sentence describing the common::test_support::decomposition module should use
en-GB spelling; replace "behavior-driven" with "behaviour-driven" in that line
(e.g., the sentence starting "for integration and behavior-driven tests:") so
the docs conform to the en-GB-oxendict guideline.
- Around line 177-179: Update the markdown link in developers-guide.md so it
correctly points from docs/developers-guide.md to the execplan file under
docs/execplans: replace the current broken relative target with a relative path
that starts from the docs folder (e.g.,
./execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.md)
so the link text
"6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.md"
resolves correctly.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 6271bd29-e185-4853-a6c8-9e114f7bb8dc
📒 Files selected for processing (2)
docs/brain-trust-lints-design.mddocs/developers-guide.md
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Owner
Author
|
@coderabbitai Have the following now been resolved? Annul any requirements that violate the en-GB-oxendict spelling (-ize / -yse / -our) conventions (for example a request to replace "normalize" with "normalise" or "artefact" with "artifact"), or where the requirement unnecessarily increases cyclomatic complexity. |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: Length of output: 13259
Individual Comment 2 — still outstandingThe BDD acronym appears without expansion as early as line 67 of The expansion |
Owner
Author
|
@coderabbitai are you satisfied that the introduced proof is substantive, rigorous, and well-founded? |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: Length of output: 10541
What the proof gets rightProperty coverage is complete for the stated contract. The five harnesses collectively assert everything
Constraint generation correctly mirrors the production contract. The bounded model is maximally dense. With
Weight fidelity is doubly verified — both Two genuine gaps worth noting1. No exclusion property. #[kani::proof]
#[kani::unwind(7)]
fn verify_build_adjacency_no_spurious_edges() {
let (node_count, edges, adjacency) = symbolic_adjacency();
kani::assume(node_count > 0);
for (node, bucket) in adjacency.iter().enumerate() {
for &(neighbour, weight) in bucket {
let in_input = edges.iter().any(|e| {
(e.left == node && e.right == neighbour && e.weight == weight)
|| (e.right == node && e.left == neighbour && e.weight == weight)
});
assert!(in_input);
}
}
}2. Sort verification is limited to 2-element lists. Minor observation
Summary: the proof is correct, honestly scoped, and covers the primary contract of |
devboxerhub
bot
force-pushed
the
kani-verify-build-adjacency-w7ihby
branch
from
1a8189c to
fc961c2
Compare
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
…jacency length check Replaced assert!(adjacency.len() == node_count) with assert_eq!(adjacency.len(), node_count) to improve clarity and provide better failure messages in the test function verify_build_adjacency_length. Co-authored-by: devboxerhub[bot] <devboxerhub[bot]@users.noreply.github.com>
leynos
changed the title
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
There was a problem hiding this comment.
Actionable comments posted: 7
♻️ Duplicate comments (1)
common/tests/decomposition_adjacency_behaviour.rs (1)
129-132: 🧹 Nitpick | 🔵 TrivialRename the scenario binding function to match canonical-order rejection semantics.
Align the function name with the updated feature scenario text to prevent intent drift.
Proposed refactor
#[scenario(path = "tests/features/decomposition_adjacency.feature", index = 1)] -fn scenario_malformed_edge_input_is_rejected(world: AdjacencyWorld) { +fn scenario_edges_not_in_canonical_order_are_rejected(world: AdjacencyWorld) { let _ = world; }🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@common/tests/decomposition_adjacency_behaviour.rs` around lines 129 - 132, Rename the test scenario function to reflect the canonical-order rejection semantics by renaming the function scenario_malformed_edge_input_is_rejected to scenario_malformed_edge_input_rejected_canonical_order (and update any references or imports accordingly); keep the same #[scenario(path = "tests/features/decomposition_adjacency.feature", index = 1)] annotation and AdjacencyWorld parameter so the scenario binding remains intact.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@common/src/decomposition_advice/community_kani.rs`:
- Around line 169-190: Add an inline NOTE/TODO immediately above the assertion
inside verify_build_adjacency_sorted_neighbours to call out the MAX_NODES = 3
coverage limitation (that bucket.windows(2) only exercises 0–2 element sorts and
defects at 3+ elements are invisible). Reference the assertion using
bucket.windows(2) / assert!(window[0].0 <= window[1].0) so maintainers see the
limitation at the exact check and can find the surrounding explanation in the
function-level comment.
In `@common/src/test_support/decomposition_adjacency.rs`:
- Around line 134-143: The helper has_mirror currently indexes
neighbours[neighbour] unsafely; add a precondition check to make the intent
explicit by inserting a debug_assert!(neighbour < neighbours.len(), "has_mirror:
neighbour index out of bounds - callers (e.g. adjacency_report) must guarantee
valid indices") and then rewrite the body to use
neighbours.get(neighbour).map_or(false, |list| list.iter().any(|&(mirror,
mirror_weight)| mirror == node && mirror_weight == weight)) so release builds
won't panic but debug builds will assert if invariants are violated.
In `@docs/brain-trust-lints-design.md`:
- Around line 536-538: The acronym "CBMC" must be expanded at first mention in
this subsection; change the sentence containing "CBMC" (the one starting "These
bounds are kept deliberately small because Rust's standard `sort_by` generates
deeply nested loops that cause CBMC state-space explosion...") to include the
full term before the acronym, e.g., "the C Bounded Model Checker (CBMC)" or more
standard "the C Bounded Model Checker (CBMC)", so the expanded term appears
immediately before "(CBMC)" on first use and subsequent mentions keep using
"CBMC".
In `@docs/developers-guide.md`:
- Around line 137-140: Replace the first occurrence of the acronym "CBMC" with
its expanded form "CBMC (C Bounded Model Checker)" and leave subsequent mentions
as "CBMC"; update the sentence in the "Bounded symbolic inputs" paragraph that
currently reads about CBMC so it now reads "...cause CBMC (C Bounded Model
Checker) state-space explosion..." ensuring only the first use is expanded and
the rest of the document keeps the acronym.
In
`@docs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.md`:
- Around line 391-393: Update the unhappy-path bullet in the docs so its
rejection condition matches the canonical-order case: replace the phrase
"out-of-range endpoint" with a clear `left >= right` rejection description
(ensure the wording matches the implemented and retrospective sections elsewhere
in this document) so the test-support wrapper unhappy-path text aligns with the
shipped canonical-order rejection case.
In `@scripts/install-kani.sh`:
- Around line 48-51: Update the curl invocation that downloads the Kani asset
(the curl command using variables asset_name, KANI_RELEASE_TAG, and tmp_dir) to
add bounded retry and timeout controls: use --retry 3 (not --retry-all-errors),
--connect-timeout 20 and --max-time 300 so transient network glitches are
retried a few times and each attempt has connection and overall time limits
before writing the tarball to "${tmp_dir}/${asset_name}" and extracting to
"${install_root}".
- Line 2: The script currently uses "set -eu" which can miss failures in
pipelines and then proceeds to create a broken symlink when toolchain_dir is
empty; change to "set -euo pipefail" and after computing toolchain_dir (the
variable populated by the grep pipeline) add a validation block that checks
toolchain_dir is non-empty and is a directory (or readable) before calling ln
-s; if the check fails, print a clear error via echo or >&2 and exit 1 so the
symlink step (ln -s ...) is never attempted with an invalid path.
---
Duplicate comments:
In `@common/tests/decomposition_adjacency_behaviour.rs`:
- Around line 129-132: Rename the test scenario function to reflect the
canonical-order rejection semantics by renaming the function
scenario_malformed_edge_input_is_rejected to
scenario_malformed_edge_input_rejected_canonical_order (and update any
references or imports accordingly); keep the same #[scenario(path =
"tests/features/decomposition_adjacency.feature", index = 1)] annotation and
AdjacencyWorld parameter so the scenario binding remains intact.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 91bde17c-e870-49ef-9e16-9812a15988ea
📒 Files selected for processing (18)
Makefilecommon/Cargo.tomlcommon/src/decomposition_advice/community.rscommon/src/decomposition_advice/community_kani.rscommon/src/decomposition_advice/mod.rscommon/src/decomposition_advice/tests.rscommon/src/decomposition_advice/tests/adjacency.rscommon/src/test_support/decomposition.rscommon/src/test_support/decomposition_adjacency.rscommon/tests/decomposition_adjacency_behaviour.rscommon/tests/features/decomposition_adjacency.featuredocs/adr-002-dylint-expect-attribute-macro.mddocs/brain-trust-lints-design.mddocs/developers-guide.mddocs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.mddocs/roadmap.mdscripts/install-kani.shscripts/run-kani.sh
docs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.md
Outdated
Show resolved
Hide resolved
…ce test safety checks - Added retry and timeout options for kani asset download to improve robustness. - Added verification for kani Rust toolchain directory presence to prevent setup failures. - Added debug_assert in has_mirror to catch out-of-bounds indexing early. - Adjusted has_mirror to use get() with fallback to prevent panics due to invalid indices. - Updated comments and docs formatting for CBMC references. - Clarified scenario function name to better reflect test purpose. Co-authored-by: devboxerhub[bot] <devboxerhub[bot]@users.noreply.github.com>
leynos
changed the title
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
There was a problem hiding this comment.
Actionable comments posted: 7
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@common/src/decomposition_advice/community_kani.rs`:
- Around line 154-165: The current verify_build_adjacency_no_spurious_edges
harness only checks provenance of each adjacency entry and misses duplicate
entries; update verify_build_adjacency_no_spurious_edges (which consumes
symbolic_adjacency returning node_count, edges, adjacency) to also compute for
each node the expected_degree by counting edges where edge.left == node or
edge.right == node and assert_eq!(adjacency[node].len(), expected_degree) before
iterating buckets, so duplicated adjacency entries will fail the proof.
In `@common/src/test_support/decomposition_adjacency.rs`:
- Around line 16-20: Add Rustdoc field-level comments to the public struct
EdgeInput: add /// comments above the fields `left`, `right`, and `weight`
describing their meaning and constraints — e.g., that `left` and `right` are
node indices in canonical order (left <= right) and that `weight` is a
non-negative u64 representing the edge weight — so generated docs show the field
semantics and positivity/canonical-order contract for `EdgeInput`.
- Around line 175-207: The public API returns Result<AdjacencyReport, String>
from adjacency_report and validate_edges; replace this opaque String with a
semantic error enum (e.g., AdjacencyError) that derives std::error::Error via
thiserror and implements Display, then change signatures of adjacency_report and
validate_edges to return Result<AdjacencyReport, AdjacencyError> and
Result<Vec<SimilarityEdge>, AdjacencyError> respectively; add enum variants for
NonCanonicalEdge {index, left, right}, EndpointOutOfRange {index, right,
node_count}, ZeroWeight {index}, and propagate those variants from the checks in
validate_edges (include the index and offending values in the variants) so
callers can match on structured failure cases, and update any callers/tests to
expect the new error type.
In `@docs/brain-trust-lints-design.md`:
- Around line 577-580: Replace the phrase "One unhappy-path BDD scenario
validates test-support input rejection" with "One unhappy-path behaviour-driven
development (BDD) scenario validates test-support input rejection" so that the
acronym BDD is expanded on first use; update the occurrence in the docs section
that contains "adjacency_report" and "build_adjacency" to keep the surrounding
sentence unchanged except for the expanded term.
In `@docs/developers-guide.md`:
- Around line 205-206: Update the documentation text that describes the
EdgeInput struct so the acronym BDD is expanded on first use: change the phrase
"for BDD scenarios" to "for behaviour-driven development (BDD) scenarios" when
describing **`EdgeInput`** to introduce the acronym before reuse.
In
`@docs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.md`:
- Around line 142-145: Update the progress bullet that currently reads "all 5
shipped harnesses" to "all 6 shipped harnesses" so the log reflects the added
proof (verify_build_adjacency_no_spurious_edges); edit the text around the `make
kani` completion line to replace "5" with "6" and ensure wording remains
consistent with the rest of the document.
In `@scripts/install-kani.sh`:
- Around line 45-60: After extracting the downloaded Kani tarball into
install_root, immediately verify the expected binary kani_driver_bin exists and
is executable; if it does not, print a clear error to stderr and exit non‑zero
so we fail fast (this prevents creating a broken cargo_kani_bin symlink later).
Update the block that downloads and extracts the bundle (the if [ ! -x
"${kani_driver_bin}" ] branch) to perform this check right after tar -xzf and
before the subsequent symlink logic, using kani_driver_bin and cargo_kani_bin as
the referenced symbols.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 2a2b4d38-1f41-4f57-925d-0b8a48dfa9eb
📒 Files selected for processing (7)
common/src/decomposition_advice/community_kani.rscommon/src/test_support/decomposition_adjacency.rscommon/tests/decomposition_adjacency_behaviour.rsdocs/brain-trust-lints-design.mddocs/developers-guide.mddocs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.mdscripts/install-kani.sh
docs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.md
Show resolved
Hide resolved
… errors to adjacency_report - Introduce AdjacencyError enum for typed validation errors instead of string messages - Validate edges for non-canonical order, out-of-range endpoints, and zero weights with detailed errors - Update adjacency_report signature to return Result with AdjacencyError - Add unit tests covering new error cases - Update consumers and tests to handle new error type - Minor docs updates to reflect error handling improvements Co-authored-by: devboxerhub[bot] <devboxerhub[bot]@users.noreply.github.com>
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@common/src/test_support/decomposition_adjacency.rs`:
- Around line 85-108: The Rustdoc examples use the wrong crate import path
(common::...), causing doctest failures; update each executable doctest to
import the real crate name (whitaker_common) instead—e.g. change occurrences in
the examples that reference adjacency_report, EdgeInput, node_count,
neighbours_of (and any other runnable examples in this file) from
common::test_support::decomposition::... to
whitaker_common::test_support::decomposition::..., and apply the same
replacement for all executable Rustdoc blocks in this file (including the other
ranges called out).
In `@docs/developers-guide.md`:
- Around line 192-206: Update the API summary to reflect that adjacency_report
returns Result<AdjacencyReport, AdjacencyError> (not a bare AdjacencyReport):
change the first bullet to state the Result return type and describe the error
path, list and briefly describe the AdjacencyError variants that can be produced
(e.g., out-of-bounds, unsorted/canonical-order, non-positive weight,
duplicate/invalid edges) and how callers should handle the Result (e.g.,
pattern-match, unwrap, or propagate), and ensure the AdjacencyReport and its
methods (is_symmetric, all_indices_in_bounds, is_sorted, neighbours_of) and
EdgeInput are unchanged but note they live on the Ok branch of the Result.
In
`@docs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.md`:
- Around line 325-336: Update the “minimum required assertions” list to include
the shipped no-spurious-edges check as an additional harness assertion (so the
checklist reflects six harnesses), by adding an item describing the exclusion
property implemented by verify_build_adjacency_no_spurious_edges (the function
in community_kani.rs) that ensures no spurious edges are present after building
adjacency; keep the existing five assertions intact and add this new assertion
text consistent with the others so the document and the later retrospective both
reflect the shipped proof.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: b1f1853f-6286-45f7-9d11-575e29476898
📒 Files selected for processing (8)
common/src/decomposition_advice/community_kani.rscommon/src/test_support/decomposition.rscommon/src/test_support/decomposition_adjacency.rscommon/tests/decomposition_adjacency_behaviour.rsdocs/brain-trust-lints-design.mddocs/developers-guide.mddocs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.mdscripts/install-kani.sh
docs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.md
Show resolved
Hide resolved
Owner
Author
|
@coderabbitai Please suggest a fix for this issue and supply a prompt for an AI coding agent to enable it to apply the fix. Include the file and symbol names indicated in the issue at the head of your response. common/src/decomposition_advice/community_kani.rs Comment on file fn verify_build_adjacency_no_spurious_edges() {
let (node_count, edges, adjacency) = symbolic_adjacency();
kani::assume(node_count > 0);
for (node, bucket) in adjacency.iter().enumerate() {
let expected_degree = edges
.iter()
.filter(|edge| edge.left == node || edge.right == node)
.count();
assert_eq!(bucket.len(), expected_degree);
for &(neighbour, weight) in bucket {
let in_input = edges.iter().any(|e| {
(e.left == node && e.right == neighbour && e.weight == weight)
|| (e.right == node && e.left == neighbour && e.weight == weight)
});
assert!(in_input);
}
}
}❌ New issue: Complex Method |
This comment was marked as resolved.
This comment was marked as resolved.
…ncy_report error handling - Adjusted documentation for `adjacency_report` to return a Result with `AdjacencyError` variants. - Clarified edge input validation and error handling in developer guide and design docs. - Updated code examples to use `whitaker_common` crate and handle errors properly. - Enhanced execplan documentation to include spurious edge verification step. These changes improve clarity on test-support input validation and error scenarios without altering production code behavior. Co-authored-by: devboxerhub[bot] <devboxerhub[bot]@users.noreply.github.com>
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In
`@docs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.md`:
- Around line 25-27: Replace the first standalone "CBMC" mention with its
expanded form "C Bounded Model Checker (CBMC)" and leave subsequent uses as
"CBMC"; locate the initial occurrence of the token "CBMC" in the sentence
starting "make kani installs or reuses..." and update that single instance so
the acronym is defined on first use.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: d86dfa44-0f91-4225-a41b-dd577a37c67a
📒 Files selected for processing (4)
common/src/test_support/decomposition_adjacency.rsdocs/brain-trust-lints-design.mddocs/developers-guide.mddocs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.md
docs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.md
Show resolved
Hide resolved
…ification proof Extracted helper functions `incident_degree` and `is_edge_in_input` from inline code in the `verify_build_adjacency_no_spurious_edges` proof to improve readability and maintainability. These functions count incident edges and check edge existence regardless of orientation, respectively, simplifying assertions in the verification harness. Co-authored-by: devboxerhub[bot] <devboxerhub[bot]@users.noreply.github.com>
leynos
changed the title
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
…ll and run scripts Added detailed usage documentation to `scripts/install-kani.sh` and `scripts/run-kani.sh` explaining environment variables, arguments, and script behavior. Also updated the developers guide to document the new `SimilarityEdge::new` constructor for internal use, clarifying API usage and test support patterns. Co-authored-by: devboxerhub[bot] <devboxerhub[bot]@users.noreply.github.com>
leynos
changed the title
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: Length of output: 4326
No further work is required for either check. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Changes
common/src/decomposition_advice/community_kani.rs(new file) containing bounded-model harnesses forbuild_adjacency.pub(crate) fn build_adjacencyincommon/src/decomposition_advice/community.rsto allow harness/test-support access without widening public API.SimilarityEdge::newconstructor for tests (crate-private).common/src/decomposition_advice/tests/adjacency.rs(new).common/src/test_support/decomposition.rsupdated to expose an adjacency report seam.common/src/test_support/decomposition_adjacency.rs(new) providing a test-support module for adjacency observations.common/tests/decomposition_adjacency_behaviour.rs(new).common/tests/features/decomposition_adjacency.feature(new).docs/brain-trust-lints-design.mdupdated with 6.4.5 decisions;docs/roadmap.mdupdated to mark 6.4.5 done.kanitarget.scripts/install-kani.shandscripts/run-kani.shto install and run Kani with a focused harness filter.docs/execplans/6-4-5-use-kani-to-verify-build-adjacency-preserves-similarity-edges.mddetailing scope, constraints, and validation plan.Rationale
Notes
📎 Task: https://www.devboxer.com/task/dd8d35c4-13b6-4b91-84df-a0f46663eb18