Gate merges on Kani, unblock kani-full, and fix reconciliation write-back ordering (#202) - #227
Conversation
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
Summary
WalkthroughChangesFormal verification
Suggested labels: Poem
Caution Pre-merge checks failedPlease resolve all errors before merging. Addressing warnings is optional.
❌ Failed checks (1 error, 5 warnings)
✅ Passed checks (14 passed)
✨ Finishing Touches 💡 2📝 Generate docstrings 💡
🛠️ Fix failing CI checks 💡
🧪 Generate unit tests (beta)
Warning Your free Security trial is over. An organization admin can activate billing to continue. Comment |
![codescene-access[bot]](https://avatars.githubusercontent.com/in/3755875?s=60&v=4){kind=small}
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Add the PR workflow, bring MST proofs into the practical suite, and remove formatted construction failures from the Kani setup paths. The full HNSW reconciliation proof remains under investigation.
`ConnectivityHealer` tracked visited nodes with `std::collections::HashSet`, whose randomised SipHash seed becomes symbolic under Kani. The 3-node bidirectional reconciliation harness is the only harness that reaches the healer (via the base-layer isolation path), which made it intractable and blocked `make kani-full`. Substitute a bounded linear-scan visited set under `#[cfg(kani)]`; production builds keep the `HashSet`. Close the MST modelling boundary: compile the sequential Kani Kruskal model under `cfg(test)` with a cfg-independent `ModelForest` result, and add an exhaustive equivalence suite comparing it against the production Rayon implementation over every edge subset of one-to-four-node complete graphs, four weight schemes, both harness input encodings, and the error cases. Record both authoring rules in the developers' guide Kani CI policy: no standard hash collections on Kani-reachable paths, and every sequential model must carry exhaustive finite-state equivalence tests.
Hand-tracing the three-node bidirectional reconciliation Kani harness exposed a production defect in the insertion commit path. When a staged update removes a neighbour whose only base-layer edge was to the origin, the connectivity healer links the isolated node back to the entry node. With the entry being the origin itself, healing consulted the stale pre-write-back neighbour list, and the subsequent write-back clobbered the healed edge, leaving a dangling reverse edge and violating the bidirectional-links invariant. A new regression test demonstrates the failure against the previous ordering. Reorder `CommitApplicator::apply_neighbour_updates` (and the mirrored Kani helper) so added-edge reconciliation and the origin's write-back run before removed-edge reconciliation; healing then observes the final origin state. Deferred scrubs still run once per batch after all updates. Route the eviction harness through the lean `_for_kani` constructors so it cannot reach `format!`-based production error paths, and drop the unused `push_if_absent` harness helper.
Three deterministic HNSW harnesses drove the full commit machinery on three- and four-node graphs and could not conclude within practical budgets, even after removing symbolic hashing from connectivity healing: the three-node reconciliation harness exceeded twenty minutes in symbolic execution alone, and the three-node commit-path harness exceeded a fifteen-minute solving budget with Kissat. A deterministic harness explores one concrete path, so its value over a unit test is only the absence of undefined behaviour along that path. Retire `verify_bidirectional_links_reconciliation_3_nodes_1_layer`, `verify_bidirectional_links_commit_path_3_nodes`, and `verify_eviction_deferred_scrub_reciprocity`, replacing each with an exact unit-test twin in the commit test suite alongside the existing regression test for the write-back ordering defect the reconciliation harness exposed. Keep the nondeterministic two-node reconciliation and four-node invariant harnesses as the bounded proofs, and drop the helpers only the retired harnesses used. Record the tractability rule and the retirement rationale in the developers' guide and the hypothesis document.
…ull (#202) The no-self-loop and neighbour-uniqueness harnesses drove `apply_reconciled_update_for_kani`, which chained added-edge reconciliation, list write-back, removed-edge reconciliation with its base-layer healing cascade, and deferred scrubs in one formula. The harnesses timed out at twenty minutes even on a two-node graph with a concrete origin and level, so the helper itself is past the tractable CBMC state space at any bound. Remove the helper and prove both invariants on the production `EdgeReconciler::ensure_reverse_edge` surface instead: per-level two-node proofs with nondeterministic forward-edge seeding, each verifying in under seventy seconds with Kissat. Replace the `HashSet` in the uniqueness assertion with a linear scan so the assertion path stays free of symbolic SipHash state. With this restructure `make kani-full` completes: seventeen harnesses across chutoro-core and chutoro-providers-dense verify in under eighteen minutes of wall clock, within the nightly 120-minute budget. Record the tractability rules and the run in the developers' guide, the hypothesis document, and ADR-002.
The github-actions dependency bump on main moved nightly-kani.yml to shared-actions setup-rust f4764be. The pull-request Kani workflow mirrors the nightly provisioning, so update its pin to match.
cc845d0 to
decb24b
Compare
The automatic merge of docs/developers-guide.md during the rebase onto main left two consecutive blank lines before the "Kani CI policy" section, which markdownlint rejects (MD012).
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.
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.
|
@coderabbitai Please investigate the cause of the following issue using codegraph exploration and research, identify a fix and provide an AI coding agent prompt for the fix: |
|
@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. Ensure that this is validated against the current version of the codegraph. If further refinement to address this finding would be deleterious, please supply a clear explanatory one to two paragraph markdown message in a code block that I can paste into the CodeScene web ui's diagnostic suppression function so this diagnostic can be silenced. Code Duplicationchutoro-core/src/hnsw/kani_proofs/invariants.rs: What lead to degradation?The module contains 2 functions with similar structure: check_neighbour_uniqueness_at_level,check_no_self_loops_at_level Why does this problem occur?Duplicated code often leads to code that's harder to change since the same logical change has to be done in multiple functions. More duplication gives lower code health. How to fix it?A certain degree of duplicated code might be acceptable. The problems start when it is the same behavior that is duplicated across the functions in the module, ie. a violation of the Don't Repeat Yourself (DRY) principle. DRY violations lead to code that is changed together in predictable patterns, which is both expensive and risky. DRY violations can be identified using CodeScene's X-Ray analysis to detect clusters of change coupled functions with high code similarity. Read More |
|
@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. Ensure that this is validated against the current version of the codegraph. If further refinement to address this finding would be deleterious, please supply a clear explanatory one to two paragraph markdown message in a code block that I can paste into the CodeScene web ui's diagnostic suppression function so this diagnostic can be silenced. Code Duplicationchutoro-core/src/mst/kani_harness.rs: What lead to degradation?The module contains 2 functions with similar structure: is_valid_forest,is_valid_forest Why does this problem occur?Duplicated code often leads to code that's harder to change since the same logical change has to be done in multiple functions. More duplication gives lower code health. How to fix it?A certain degree of duplicated code might be acceptable. The problems start when it is the same behavior that is duplicated across the functions in the module, ie. a violation of the Don't Repeat Yourself (DRY) principle. DRY violations lead to code that is changed together in predictable patterns, which is both expensive and risky. DRY violations can be identified using CodeScene's X-Ray analysis to detect clusters of change coupled functions with high code similarity. Read More |
|
@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. Ensure that this is validated against the current version of the codegraph. If further refinement to address this finding would be deleterious, please supply a clear explanatory one to two paragraph markdown message in a code block that I can paste into the CodeScene web ui's diagnostic suppression function so this diagnostic can be silenced. Code Duplicationchutoro-core/src/mst/kani_model.rs: What lead to degradation?The module contains 2 functions with similar structure: sort_edges_for_kani,sort_forest_edges_for_kani Why does this problem occur?Duplicated code often leads to code that's harder to change since the same logical change has to be done in multiple functions. More duplication gives lower code health. How to fix it?A certain degree of duplicated code might be acceptable. The problems start when it is the same behavior that is duplicated across the functions in the module, ie. a violation of the Don't Repeat Yourself (DRY) principle. DRY violations lead to code that is changed together in predictable patterns, which is both expensive and risky. DRY violations can be identified using CodeScene's X-Ray analysis to detect clusters of change coupled functions with high code similarity. Read More |
|
@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. Ensure that this is validated against the current version of the codegraph. If further refinement to address this finding would be deleterious, please supply a clear explanatory one to two paragraph markdown message in a code block that I can paste into the CodeScene web ui's diagnostic suppression function so this diagnostic can be silenced. Complex Methodchutoro-core/src/mst/kani_model.rs: kruskal_model What lead to degradation?kruskal_model has a cyclomatic complexity of 12, threshold = 9 Why does this problem occur?A Complex Method has a high cyclomatic complexity. The recommended threshold for the Rust language is a cyclomatic complexity lower than 9. How to fix it?There are many reasons for Complex Method. Sometimes, another design approach is beneficial such as a) modeling state using an explicit state machine rather than conditionals, or b) using table lookup rather than long chains of logic. In other scenarios, the function can be split using EXTRACT FUNCTION. Just make sure you extract natural and cohesive functions. Complex Methods can also be addressed by identifying complex conditional expressions and then using the DECOMPOSE CONDITIONAL refactoring. Helpful refactoring examplesTo get a general understanding of what this code health issue looks like - and how it might be addressed - we have prepared some diffs for illustrative purposes. SAMPLE# complex_method.js
function postItem(item) {
if (!item.id) {
- if (item.x != null && item.y != null) {
- post(item);
- } else {
- throw Error("Item must have x and y");
- }
+ // extract a separate function for creating new item
+ postNew(item);
} else {
- if (item.x < 10 && item.y > 25) {
- put(item);
- } else {
- throw Error("Item must have an x and y value between 10 and 25");
- }
+ // and one for updating existing items
+ updateItem(item);
}
}
+
+function postNew(item) {
+ validateNew(item);
+ post(item);
+}
+
+function updateItem(item) {
+ validateUpdate(item);
+ put(item);
+}
+ |
|
@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. Ensure that this is validated against the current version of the codegraph. If further refinement to address this finding would be deleterious, please supply a clear explanatory one to two paragraph markdown message in a code block that I can paste into the CodeScene web ui's diagnostic suppression function so this diagnostic can be silenced. Code Duplicationchutoro-core/src/hnsw/insert/commit/tests/deferred_scrub.rs: What lead to degradation?The module contains 2 functions with similar structure: commit_path_reconciliation_keeps_bidirectionality,eviction_deferred_scrub_keeps_reciprocity Why does this problem occur?Duplicated code often leads to code that's harder to change since the same logical change has to be done in multiple functions. More duplication gives lower code health. How to fix it?A certain degree of duplicated code might be acceptable. The problems start when it is the same behavior that is duplicated across the functions in the module, ie. a violation of the Don't Repeat Yourself (DRY) principle. DRY violations lead to code that is changed together in predictable patterns, which is both expensive and risky. DRY violations can be identified using CodeScene's X-Ray analysis to detect clusters of change coupled functions with high code similarity. Read More |
![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: 6873caf626
ℹ️ 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".
Reviewer's GuideThis PR makes Kani a path-filtered pull-request merge gate, fixes a production reconciliation ordering defect that could leave dangling reverse edges, restructures HNSW proofs to complete within CI budgets, and adds an exhaustively tested bounded sequential model for Kani verification of the Rayon MST implementation. Sequence diagram for corrected HNSW reconciliation orderingsequenceDiagram
participant CommitApplicator
participant EdgeReconciler
participant Graph
participant ConnectivityHealer
CommitApplicator->>EdgeReconciler: reconcile_added_edges(ctx, next)
CommitApplicator->>Graph: write origin neighbour list
CommitApplicator->>EdgeReconciler: reconcile_removed_edges(ctx, previous, next)
EdgeReconciler->>ConnectivityHealer: ensure_base_connectivity(...)
ConnectivityHealer->>Graph: heal connectivity against entry node
EdgeReconciler-->>CommitApplicator: preserve bidirectional links
Flow diagram for tractable Kani verification tiersflowchart TD
Change[Relevant code or proof change]
Fast[make kani]
Full[make kani-full]
Narrow[Narrow bounded proofs]
Model[Sequential MST model]
Equivalence[Exhaustive model equivalence tests]
Unit[Deterministic unit-test twins]
Success[Verification completes within CI budget]
Change --> Fast
Fast --> Narrow
Fast --> Model
Model --> Equivalence
Change --> Full
Full --> Narrow
Full --> Unit
Equivalence --> Success
Unit --> Success
File-Level Changes
Assessment against linked issues
Possibly linked issues
Tips and commandsInteracting with Sourcery
Customizing Your ExperienceAccess your dashboard to:
Getting Help
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
![sourcery-ai[bot]](https://avatars.githubusercontent.com/in/48477?s=60&v=4){kind=small}
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
ast-grep outline chutoro-core/src/mst/kani_harness.rs --items all
printf '\n--- is_valid_forest definitions and callers ---\n'
rg -n -A70 -B12 '\b(is_valid_forest|verify_mst_)' chutoro-core/src/mst/kani_harness.rs
printf '\n--- MinimumSpanningForest configuration and accessors ---\n'
ast-grep outline chutoro-core/src/mst/mod.rs --items all --match 'MinimumSpanningForest|parallel_kruskal'
rg -n -A60 -B15 '\b(struct MinimumSpanningForest|impl MinimumSpanningForest|fn edges|fn component_count)' chutoro-core/src/mst/mod.rs
printf '\n--- cfg(kani) references in MST sources ---\n'
rg -n -C3 '#\[cfg\((not\()?kani\)\]' chutoro-core/src/mstLength of output: 15305
Suppress this finding. The two Do not extract shared parent-storage logic. A shared abstraction would either introduce dynamic allocation into the Kani-reachable path or add indirection that obscures the verification bound. The current duplication is limited to the union-find loop. It keeps the production implementation unrestricted and the proof implementation bounded. This matches Paste this suppression text into CodeScene: The two `is_valid_forest` functions are mutually exclusive `cfg` implementations of the same validation contract. The non-Kani implementation uses a dynamically sized `Vec<usize>` for arbitrary graph sizes. The Kani implementation rejects graphs larger than four nodes and uses `[usize; 4]` to keep the proof model bounded and to avoid allocator and panic-path modelling.
Do not merge these implementations. A shared storage abstraction would add proof-path complexity or reintroduce dynamic allocation into the Kani build. The small duplicated union-find loop keeps the Kani bound explicit and preserves the required separation between unrestricted production execution and bounded formal verification.You are interacting with an AI system. |
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
|
@coderabbitai please create new GitHub issues for the following: 1. Enforce the 2. Decide and document the upper-layer isolation policy Healing is base-layer-only by design, so an evicted node can legitimately hold an empty neighbour list at level ≥ 1. That's defensible (search descends through the entry, so upper-layer isolation degrades recall, not reachability) — but it's currently folklore, not documented policy. Either record it as a deliberate invariant-exclusion in the design doc's invariants section, or implement upper-layer healing. I'd recommend the former; the issue is the forcing function to make it explicit. 3. Property-test the commit-batch sequencing class the bug came from The write-back ordering defect was a sequencing bug in batch update application, found by hand-trace. Its unit twin pins one instance; the class is "any batch of staged updates containing an isolation transition maintains bidirectionality after commit". A proptest generating small batches of updates (including neighbour removals that isolate nodes, with the entry as origin) and asserting |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
repo="leynos/chutoro"
pr_number="227"
printf '%s\n' '=== Relevant current symbols ==='
ast-grep outline chutoro-core/src/hnsw/insert/reconciliation.rs --items all --view expanded
ast-grep outline chutoro-core/src/hnsw/insert/commit.rs --items all --view expanded
rg -n -C3 \
'\b(ensure_reverse_edge|reconcile_removed_edges|apply_deferred_scrubs|check_all)\b' \
chutoro-core/src/hnsw/insert \
chutoro-core/src/hnsw \
docs/chutoro-design.md
printf '%s\n' '=== Originating PR comment URL ==='
gh api --paginate "repos/$repo/issues/$pr_number/comments?per_page=100" \
--jq '.[] | select(.user.login == "leynos" and (.body | contains("please create new GitHub issues for the following"))) | .html_url' \
| tail -n 1Length of output: 26194 🏁 Script executed: #!/bin/bash
set -euo pipefail
repo="leynos/chutoro"
assignee="leynos"
pr_url="https://github.com/leynos/chutoro/pull/227"
comment_url="https://github.com/leynos/chutoro/pull/227#issuecomment-5400755118"
create_issue() {
local title="$1"
local body_file="$2"
gh issue create \
--repo "$repo" \
--assignee "$assignee" \
--title "$title" \
--body-file "$body_file"
}
issue_one_body="$(mktemp)"
issue_two_body="$(mktemp)"
issue_three_body="$(mktemp)"
trap 'rm -f "$issue_one_body" "$issue_two_body" "$issue_three_body"' EXIT
cat >"$issue_one_body" <<EOF
## Summary
Enforce the \`target != ctx.origin\` precondition in \`EdgeReconciler::ensure_reverse_edge\`.
## Rationale
\`EdgeReconciler::ensure_reverse_edge\` in \`chutoro-core/src/hnsw/insert/reconciliation.rs\` currently accepts a target equal to \`ctx.origin\`. A future staging or trimming change could put the origin in a \`next\` list. The reconciler would then silently write a self-loop. Existing invariant checks detect this after the fact in tests.
## Required changes
- Add \`debug_assert!(target != ctx.origin)\`.
- Add an early \`return false\` when \`target == ctx.origin\`.
- Preserve existing behaviour for valid reverse-edge requests.
- Add a unit test for the degenerate call. Verify that the method returns \`false\` and does not create a self-loop.
- Re-verify the two-node no-self-loop Kani proofs. The proofs must cover the new guard as well as the valid reconciliation path.
## Acceptance criteria
- \`ensure_reverse_edge\` rejects \`target == ctx.origin\`.
- The degenerate unit test passes.
- The two two-node no-self-loop Kani harnesses verify.
- The normal test suite remains green.
## Backlinks
- Source PR: $pr_url
- Requesting comment: $comment_url
- Requested by: @$assignee
EOF
cat >"$issue_two_body" <<EOF
## Summary
Decide and document the upper-layer isolation policy for HNSW insertion reconciliation.
## Rationale
Connectivity healing is intentionally limited to the base layer. An evicted node can therefore have an empty neighbour list at level 1 or above. This may reduce recall, but it does not remove base-layer reachability because search descends from the entry point. This behaviour is not currently an explicit design policy.
## Required decision
Select one policy:
1. Document upper-layer isolation as a deliberate invariant exclusion.
2. Implement upper-layer healing.
The recommended policy is option 1. Record the decision in the HNSW invariants section of \`docs/chutoro-design.md\`. State that base-layer reachability is required, upper-layer isolation is permitted after eviction, and the expected search-quality trade-off.
If the decision is to implement upper-layer healing, define the required invariants, update reconciliation behaviour, and add focused tests.
## Acceptance criteria
- The repository contains an explicit upper-layer isolation policy.
- The policy states whether upper-layer isolation is permitted.
- The policy explains why the base layer and upper layers have different requirements.
- Tests and invariants match the selected policy.
## Backlinks
- Source PR: $pr_url
- Requesting comment: $comment_url
- Requested by: @$assignee
EOF
cat >"$issue_three_body" <<EOF
## Summary
Add a property test for commit-batch sequencing when a staged update isolates a node.
## Rationale
The write-back ordering defect in \`chutoro-core/src/hnsw/insert/commit.rs\` was a sequencing defect in batch update application. The existing unit regression test pins one topology. It does not cover the broader class: a batch of staged updates containing an isolation transition must preserve graph invariants after commit.
## Required changes
Add a \`proptest\` for small staged-update batches in the HNSW insertion commit test surface.
The generator must include neighbour removals that can isolate nodes. Use the entry node as an update origin. Apply the complete commit batch. Then assert \`index.invariants().check_all()\` after the commit.
Keep generated graph sizes and batch sizes small enough for deterministic CI execution. Include shrinking-friendly diagnostics that identify the generated updates and failing topology.
## Affected areas
- \`chutoro-core/src/hnsw/insert/commit.rs\`
- \`chutoro-core/src/hnsw/insert/commit/tests/\`
- \`chutoro-core/src/hnsw/invariants/mod.rs::HnswInvariants::check_all\`
## Acceptance criteria
- A property test generates small commit batches with isolation transitions.
- The test applies each batch through the production commit path.
- The test asserts \`check_all()\` after each completed batch.
- The test exercises removal and deferred-scrub sequencing.
- The test runs in the normal CI test suite.
## Backlinks
- Source PR: $pr_url
- Requesting comment: $comment_url
- Requested by: @$assignee
EOF
printf 'Issue 1: %s\n' "$(create_issue 'Enforce the no-self-loop precondition in EdgeReconciler::ensure_reverse_edge' "$issue_one_body")"
printf 'Issue 2: %s\n' "$(create_issue 'Decide and document the HNSW upper-layer isolation policy' "$issue_two_body")"
printf 'Issue 3: %s\n' "$(create_issue 'Property-test HNSW commit-batch sequencing for isolation transitions' "$issue_three_body")"Length of output: 5505
🧠 Learnings usedYou are interacting with an AI system. |
The verifier version was restated in the pull-request workflow, the workflow contract test, and the developers' guide, while the Makefile derived it from whichever Kani happened to be installed. A bump needed four coordinated edits that nothing checked, and the Makefile could silently disagree with CI. Record the pin once in `tools/kani/VERSION`, matching both the existing Verus convention in `tools/verus/VERSION` and the default version-file location `prover-tools kani install` reads. The Makefile derives `KANI_VERSION` from that file, the workflow interpolates it, the guide points at it, and the pin file itself triggers the gate when it changes. Bumping Kani is now one line. Rework the workflow contracts to assert shapes and relationships instead of specific values, so routine pin bumps cannot fail the build for no defect: - Derive the Kani surface from the tree and assert the path filter covers every harness, rather than pinning an exact filter list. A harness added in a new location now fails until the filter follows. - Assert the pull-request timeout is strictly tighter than the nightly tier, read from the nightly workflow, rather than asserting 30. - Assert the install step derives the version from the pin file and carries no version literal, rather than asserting a version. Add a repository-wide contract covering every workflow: each external action reference must be pinned to a full commit SHA, and any action used in more than one workflow must resolve to the same SHA everywhere. That catches a partially applied Dependabot bump without naming a SHA. Each new assertion was mutation-tested: diverging one shared-actions pin, unpinning an action to a tag, dropping a harness path filter, and raising the pull-request timeout above the nightly budget each fail the suite.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
CodeScene repeatedly asks for abstractions that this branch measured to break bounded verification: unifying the two insertion sorts in the MST model, decomposing `kruskal_model`, and bundling harness edge arguments into a struct together took `make kani-full` from 17/17 harnesses verified to `kissat: maximum variable index exceeded` with none verified. Generic and struct-wrapped constructs inflate the CBMC formula, so proof code stays concrete and monomorphic by design. Without a scoped rule set each pull request relitigates that thread by thread. Add rule sets covering only the six bounded-proof files: the HNSW proof modules, the MST harness and model, and the dense SIMD proofs. Duplication, primitive obsession, and excess-argument rules are disabled there, each with the rationale recorded inline. `Complex Method` is down-weighted to 0.3 rather than disabled, because it is a critical rule and genuine complexity growth should still surface in review. The globs deliberately exclude `kani_model_equivalence.rs` and the `kani_nightly_gate` files, which carry `kani` in the name but are ordinary Rust under no solver constraint; a broad `**/kani_*.rs` glob would have relaxed rules on all three. Scope is asserted against `git ls-files`: exactly the six proof surfaces match, and nothing else. Separately, flatten `_iter_uses` in the action-pin contract test into a generator plus a mapping helper. That finding is in ordinary test code under no solver constraint, so it is fixed rather than suppressed.
|
@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. Ensure that this is validated against the current version of the codegraph. If further refinement to address this finding would be deleterious, please supply a clear explanatory one to two paragraph markdown message in a code block that I can paste into the CodeScene web ui's diagnostic suppression function so this diagnostic can be silenced. tests/workflow_contracts/action_pins_test.py Comment on lines +49 to +61 def _iter_uses(document: object) -> list[str]:
"""Return every ``uses:`` value anywhere in a parsed workflow."""
found: list[str] = []
if isinstance(document, dict):
for key, value in document.items():
if key == "uses" and isinstance(value, str):
found.append(value)
else:
found.extend(_iter_uses(value))
elif isinstance(document, list):
for item in document:
found.extend(_iter_uses(item))
return found❌ New issue: Bumpy Road Ahead |
| @@ -1,4 +1,7 @@ | |||
| //! Kani harnesses for minimum-spanning-forest invariants. | |||
| //! Fast-tier Kani harnesses for minimum-spanning-forest invariants. | |||
There was a problem hiding this comment.
@coderabbitai Addressed in 90a22c1, by scoping the rule rather than changing the code.
This module is Kani bounded-proof code. The primitive arguments are load-bearing: bundling the harness edge arguments into a TriangleEdge struct, together with unifying the two bounded insertion sorts and decomposing kruskal_model, was measured to take make kani-full from 17/17 harnesses verified to kissat: maximum variable index exceeded with none verified. Struct-wrapped and generic constructs inflate the CBMC formula past the SAT solver's variable-index limit.
.codescene/code-health-rules.json now disables Primitive Obsession, Code Duplication, and Excess Number of Function Arguments for the six bounded-proof files only, with the rationale recorded inline and in the Kani CI policy section of docs/developers-guide.md. Complex Method is down-weighted to 0.3 rather than disabled, since it is a critical rule and real complexity growth should still surface.
The globs exclude kani_model_equivalence.rs and the kani_nightly_gate files, which carry kani in the name but are ordinary Rust under no solver constraint. Scope is asserted against git ls-files: exactly the six proof surfaces match.
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 outdated.
This comment was marked as outdated.
Sorry, something went wrong.
The complete-graph sweep emits each undirected pair at most once, so it never reached the model's deduplication path and never probed the bounds of its domain. Both are reachable by real callers: the six-edge budget counts canonical edges before deduplication, so repeats are in-domain. Cover deduplication with identical repeats, a repeat differing only in sequence, a reversed orientation that canonicalizes onto an existing edge, a same-pair pair differing in weight that must not be merged, and duplicates sitting exactly at the six-edge budget. The model and production agree throughout. Pin the contract boundary as well: beyond four nodes or six canonical edges the model reports an invariant violation while production succeeds. That divergence is the modelling contract, so widening a harness past those bounds now fails loudly rather than silently verifying a truncated graph. Deliberately not asserted: that disabling the model's deduplication changes its output. It does not, because the union-find cycle check already rejects a repeated edge, so deduplication mirrors production without being observable in the forest. Mutation testing confirms the suite still detects the mutations that do matter: raising the node bound, reversing the sort order, and deduplicating too aggressively each fail it.
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.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Cover the Kani visited-set substitute in normal CI: the linear-scan set that replaces `HashSet` under `cfg(kani)` is now `LinearVisitedSet`, compiled under `cfg(test)` as well, with rstest cases asserting its insert semantics match `HashSet` across unique, duplicate, and empty sequences. A direct proof was attempted first and measured intractable: a two-node harness driving `ConnectivityHealer::ensure_base_connectivity` timed out after twenty minutes in symbolic execution, matching the earlier finding that the healer's iterative work queue is past the CBMC cliff, so the harness was removed rather than left to re-block the nightly sweep. Add a fast-tier contract test deriving every proof name from the MST harness module and asserting the Makefile's kani target runs each, so the documented tier decision cannot drift; dropping a harness command fails the suite. Emit bounded reconciliation metrics behind the metrics feature: healed-node and orphan-scrub counters with a base or upper layer label and no node identifiers, described at index construction following the session conventions. Document the reciprocal-link insertion guarantee in the users' guide, record the MST Kani model boundary and its equivalence-test closure in the design document and ADR-002, and add docstrings across the diff-touched reconciliation, proof, model, and test-helper functions.
|
@coderabbitai Responding to the pre-merge check rows, reconciled against head 326fd18: Testing (Overall) — actioned, with one measured substitution. The row asked for a Kani harness driving base-layer healing plus a contract test for the MST commands in Docstring Coverage — actioned. Added docstrings across the diff-touched functions: the reconciliation methods, the connectivity healer entry points, the Kani proof helpers and MST model internals, the commit-test fixtures and helpers, the equivalence-test cases, and the parameters User-Facing Documentation — actioned. Developer Documentation — actioned. The design document now records the MST Kani model boundary after Figure 2 (four-node/six-edge bounds, the fixed Testing (Compile-Time / UI) — dismissed as impossible for the Kani half, with the equivalent already gating. Unchanged from the previous two rounds: trybuild runs the normal rustc, which cannot compile Observability — actioned. Reconciliation now emits bounded metrics through the existing Validation at 326fd18: 695 unit tests, 20 workflow-contract tests, fmt, clippy + Whitaker, typecheck, markdownlint, nixie, and |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
printf '%s\n' '=== revision ==='
git rev-parse --short HEAD
git status --short
printf '%s\n' '=== relevant file discovery ==='
fd -HI '^(kani_fast_tier_test|action_pins_test|connectivity|kani_harness|kani_model|kani-full-hnsw-hypothesis-testing)\.(py|rs|md)$' \
tests chutoro-core docs 2>/dev/null || true
printf '%s\n' '=== workflow contract and Makefile Kani tier ==='
ast-grep outline tests/workflow_contracts/kani_fast_tier_test.py --items all --view expanded 2>/dev/null || true
rg -n -C4 'kani:|kani-full:|verify_mst|kani_fast_tier|harness|MST' \
Makefile tests/workflow_contracts/kani_fast_tier_test.py chutoro-core/src/mst/kani_harness.rs 2>/dev/null || true
printf '%s\n' '=== Kani visited-set definition, gates, and tests ==='
ast-grep outline chutoro-core/src/hnsw/insert/connectivity.rs --items all --view expanded 2>/dev/null || true
rg -n -C5 \
'LinearVisitedSet|VisitedSet|HashSet|cfg\(test\)|rstest|ensure_base_connectivity|base.*healing' \
chutoro-core/src/hnsw/insert chutoro-core/src/hnsw 2>/dev/null || true
printf '%s\n' '=== metrics and tracing ==='
rg -n -C5 \
'healed_nodes_total|orphan_scrubs_total|metrics::|counter!|layer.*(base|upper)|reconcile_removed_edges|apply_deferred_scrubs' \
chutoro-core/src/hnsw/insert docs 2>/dev/null || true
printf '%s\n' '=== documentation statements ==='
rg -n -C4 \
'Insertion guarantees|reciprocal|Kani.*model|four.node|six.edge|MstEdge|2026-08-24|change.control|verification policy' \
docs/users-guide.md docs/chutoro-design.md docs/adr-002-adoption-of-kani-formal-verification.md 2>/dev/null || true
printf '%s\n' '=== doc comments in claimed Rust surfaces ==='
rg -n -C1 '^\s*///' \
chutoro-core/src/hnsw/insert/{reconciliation.rs,connectivity.rs} \
chutoro-core/src/hnsw/kani_proofs/invariants.rs \
chutoro-core/src/mst/{kani_model.rs,kani_harness.rs} \
chutoro-core/src/hnsw/insert/commit/tests \
chutoro-core/src/mst/tests/kani_model_equivalence.rs \
chutoro-core/src/hnsw/params.rs 2>/dev/null || trueLength of output: 202568 🏁 Script executed: #!/bin/bash
set -euo pipefail
printf '%s\n' '=== current revision ==='
git rev-parse --short HEAD
printf '%s\n' '=== fast-tier workflow contract ==='
nl -ba tests/workflow_contracts/kani_fast_tier_test.py | sed -n '1,260p'
printf '%s\n' '=== Makefile targets ==='
rg -n -A35 -B3 '^(kani|kani-full|test-workflow-contracts):' Makefile
printf '%s\n' '=== visited-set configuration and tests ==='
nl -ba chutoro-core/src/hnsw/insert/connectivity.rs | sed -n '1,110p'
nl -ba chutoro-core/src/hnsw/insert/connectivity.rs | sed -n '285,350p'
printf '%s\n' '=== all direct base-healing test callers ==='
rg -n -C3 '\bensure_base_connectivity\s*\(' chutoro-core/src
printf '%s\n' '=== documented direct-healing proof measurement ==='
rg -n -C5 \
'2,590|2590|ensure_base_connectivity|timed out|timeout|LinearVisitedSet' \
docs/developers-guide.md docs/kani-full-hnsw-hypothesis-testing.md \
chutoro-core/src/hnsw/insert/connectivity.rs
printf '%s\n' '=== metrics documentation context ==='
rg -n -C5 \
'healed_nodes_total|orphan_scrubs_total|session metric|metrics feature|metrics' \
docs/users-guide.md docs/developers-guide.md docs/chutoro-design.md \
chutoro-core/src/hnsw/insert/reconciliation.rsLength of output: 1649 🏁 Script executed: #!/bin/bash
set -euo pipefail
printf '%s\n' '=== fast-tier workflow contract ==='
cat -n tests/workflow_contracts/kani_fast_tier_test.py | sed -n '1,260p'
printf '%s\n' '=== Makefile targets ==='
rg -n -A35 -B3 '^(kani|kani-full|test-workflow-contracts):' Makefile
printf '%s\n' '=== visited-set configuration and tests ==='
cat -n chutoro-core/src/hnsw/insert/connectivity.rs | sed -n '1,110p'
cat -n chutoro-core/src/hnsw/insert/connectivity.rs | sed -n '285,350p'
printf '%s\n' '=== all direct base-healing callers ==='
rg -n -C3 '\bensure_base_connectivity\s*\(' chutoro-core/src
printf '%s\n' '=== documented direct-healing proof measurement ==='
rg -n -C5 \
'2,590|2590|ensure_base_connectivity|timed out|timeout|LinearVisitedSet' \
docs/developers-guide.md docs/kani-full-hnsw-hypothesis-testing.md \
chutoro-core/src/hnsw/insert/connectivity.rs
printf '%s\n' '=== metrics documentation context ==='
rg -n -C5 \
'healed_nodes_total|orphan_scrubs_total|session metric|metrics feature|metrics' \
docs/users-guide.md docs/developers-guide.md docs/chutoro-design.md \
chutoro-core/src/hnsw/insert/reconciliation.rsLength of output: 41474
Amend the observability statement. The inspected documentation does not contain either reconciliation metric identifier. Do not state that index-construction documentation describes these metrics unless a separate documentation location exists. State that the source implements the metrics under the existing Treat the reported runtime validation as branch-reported. Source inspection passed. This environment cannot independently run the test, lint, or Kani commands. ✏️ Learnings added
🧠 Learnings usedYou are interacting with an AI system. |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
|
@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. Ensure that this is validated against the current version of the codegraph. If further refinement to address this finding would be deleterious, please supply a clear explanatory one to two paragraph markdown message in a code block that I can paste into the CodeScene web ui's diagnostic suppression function so this diagnostic can be silenced. tests/workflow_contracts/kani_fast_tier_test.py Comment on lines +39 to +52 def kani_target() -> str:
"""Return the recipe body of the Makefile's ``kani:`` target."""
lines = MAKEFILE_PATH.read_text(encoding="utf-8").splitlines()
body: list[str] = []
in_target = False
for line in lines:
if re.match(r"^kani:", line):
in_target = True
continue
if in_target:
if line.startswith("\t"):
body.append(line)
else:
break❌ New issue: Bumpy Road Ahead |
This comment was marked as resolved.
This comment was marked as resolved.
Replace the stateful line loop in the fast-tier contract fixture with a single multiline regular expression that matches the first `kani:` header and captures its consecutive tab-indented recipe lines, stopping at the first non-recipe line. One assertion now covers both a missing target and an empty recipe, with the message unchanged. Behaviour is preserved and probed: the first target wins, `kani-full:` is not mistaken for `kani:`, capture stops at the first non-tab line, an end-of-file recipe without a trailing newline is kept, and emptying the real recipe fails the suite with the expected message. The returned string is byte-identical to the previous join for the current Makefile.
There was a problem hiding this comment.
Gates Failed
(1 file with Complex Method)
Our agent can fix these. Install it.
Gates Passed
Reason for failure
| Enforce advisory code health rules | Violations | Code Health Impact | |
|---|---|---|---|
| kani_model.rs | 1 advisory rule | 9.88 | Suppress |
Absence of Expected Change Pattern
- chutoro/chutoro-core/src/hnsw/graph/core.rs is usually changed with: chutoro/chutoro-core/src/hnsw/node.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.
|
@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. Ensure that this is validated against the current version of the codegraph. If further refinement to address this finding would be deleterious, please supply a clear explanatory one to two paragraph markdown message in a code block that I can paste into the CodeScene web ui's diagnostic suppression function so this diagnostic can be silenced. Complex Methodchutoro-core/src/mst/kani_model.rs: kruskal_model What lead to degradation?kruskal_model has a cyclomatic complexity of 12, threshold = 9 Why does this problem occur?A Complex Method has a high cyclomatic complexity. The recommended threshold for the Rust language is a cyclomatic complexity lower than 9. How to fix it?There are many reasons for Complex Method. Sometimes, another design approach is beneficial such as a) modeling state using an explicit state machine rather than conditionals, or b) using table lookup rather than long chains of logic. In other scenarios, the function can be split using EXTRACT FUNCTION. Just make sure you extract natural and cohesive functions. Complex Methods can also be addressed by identifying complex conditional expressions and then using the DECOMPOSE CONDITIONAL refactoring. Helpful refactoring examplesTo get a general understanding of what this code health issue looks like - and how it might be addressed - we have prepared some diffs for illustrative purposes. SAMPLE# complex_method.js
function postItem(item) {
if (!item.id) {
- if (item.x != null && item.y != null) {
- post(item);
- } else {
- throw Error("Item must have x and y");
- }
+ // extract a separate function for creating new item
+ postNew(item);
} else {
- if (item.x < 10 && item.y > 25) {
- put(item);
- } else {
- throw Error("Item must have an x and y value between 10 and 25");
- }
+ // and one for updating existing items
+ updateItem(item);
}
}
+
+function postNew(item) {
+ validateNew(item);
+ post(item);
+}
+
+function updateItem(item) {
+ validateUpdate(item);
+ put(item);
+}
+ |
This comment was marked as resolved.
This comment was marked as resolved.
3 participants
Summary
This branch makes Kani verification an actual merge gate and unblocks the
nightly full tier, closing the gap where no Kani harness gated any merge and
make kani-fullcould not complete. Along the way, the investigation exposedand fixed a genuine production defect in insertion-commit reconciliation.
Closes #202.
The branch delivers four pieces of work:
A pull-request Kani gate. The path-filtered
.github/workflows/kani-pr.yml
workflow runs
make kanion pull requests when Kani harnesses, themodules under proof, the Makefile, or the Cargo dependency graph change,
with pinned actions, a 30-minute timeout, and cancellation of superseded
runs. The fast tier in the Makefile now also
runs both minimum-spanning-tree (MST) harnesses.
A production bug fix. Hand-tracing the three-node reconciliation
harness exposed an ordering defect: removed-edge reconciliation ran
before the origin's neighbour-list write-back, so base-layer connectivity
healing against the entry node could be clobbered by the write-back,
leaving a dangling reverse edge that violates the bidirectional-links
invariant.
chutoro-core/src/hnsw/insert/commit.rs
now writes the origin's list back before removed-edge reconciliation, and
the regression test
isolation_replacement_keeps_bidirectionalitydemonstrates the failure against the previous ordering.
A tractable harness suite.
make kani-fullwas blocked by harnessespast the CBMC state-space cliff: symbolic
HashSethashing inconnectivity healing, three deterministic multi-node harnesses that could
not conclude within 15–20 minute budgets, and a reconciled-update helper
that chained the whole commit machinery into one intractable formula.
The healing visited-set is now a bounded linear scan under
#[cfg(kani)],the deterministic harnesses are retired in favour of exact unit-test
twins, and the no-self-loop and neighbour-uniqueness invariants are
proved on the
ensure_reverse_edgesurface with per-level two-nodeharnesses.
make kani-fullnow verifies all seventeen harnesses inunder eighteen minutes, within the nightly 120-minute budget.
A validated MST model boundary. The sequential Kani model for
parallel Kruskal is now compiled under
cfg(test)as well and backed byexhaustive equivalence tests against the production Rayon implementation
over every edge subset of one-to-four-node complete graphs, four weight
schemes, both harness input encodings, and the error paths.
Review walkthrough
chutoro-core/src/hnsw/insert/commit.rs
for the reconciliation ordering fix, then
chutoro-core/src/hnsw/insert/commit/tests/mod.rs
for the regression test that demonstrates the defect.
chutoro-core/src/hnsw/insert/connectivity.rs
for the Kani-safe visited set, and
chutoro-core/src/hnsw/kani_proofs/invariants.rs
for the restructured invariant proofs.
chutoro-core/src/hnsw/kani_proofs/bidirectional.rs
and
chutoro-core/src/hnsw/insert/commit/tests/deferred_scrub.rs.
chutoro-core/src/mst/tests/kani_model_equivalence.rs
with the model refactor in
chutoro-core/src/mst/kani_model.rs.
.github/workflows/kani-pr.yml
and the Makefile
kanitarget; policy andfindings are recorded in
docs/developers-guide.md,
docs/kani-full-hnsw-hypothesis-testing.md,
and
docs/adr-002-adoption-of-kani-formal-verification.md.
Validation
make kani: all six fast-tier harnessesVERIFICATION:- SUCCESSFUL.make kani-full: seventeen harnesses acrosschutoro-coreandchutoro-providers-dense, all successful, 17m50s wall clock includingKani compilation (nightly budget is 120 minutes).
nextest, markdownlint, nixie): all green; 1094 tests passed, 1 skipped.
coderabbit review --agent --base main: review completed with zerofindings across all twenty-one changed files.
Notes
kani::any), sotheir proof value over a unit test was only the absence of undefined
behaviour along one concrete path — a path each now-passing unit twin
executes in milliseconds. The tractability rules learnt here (no standard
hash collections on Kani-reachable paths, no symbolic index positions,
narrow proof surfaces) are recorded in the developers' guide.
verify_dense_simd_*harnesses and the distance harnesses werealready tractable and are unchanged.
References
Summary by Sourcery
Make Kani verification a pull-request merge gate, restore a tractable full verification tier, and correct HNSW reconciliation ordering that could violate bidirectional connectivity.
New Features:
Bug Fixes:
Enhancements:
Build:
CI:
Documentation:
Tests:
Chores: