Gate merges on Kani, unblock kani-full, and fix reconciliation write-back ordering (#202)

.codescene/code-health-rules.json

@@ -1,11 +1,52 @@
 {
+  "usage": "Kani rule sets are scoped to bounded-proof code only. They deliberately exclude chutoro-core/src/mst/tests/kani_model_equivalence.rs and chutoro-test-support/**/kani_nightly_gate*.rs, which merely carry `kani` in the name and are ordinary Rust under no solver constraint.",
   "rule_sets": [
     {
       "matching_content_path": "chutoro-providers/dense/src/simd/kernels.rs",
       "matching_content_path_doc": "Kernel functions operate directly on `&[f32]` slices and `usize` offsets because SIMD intrinsics require contiguous, unboxed memory and raw index arithmetic",
       "rules": [
         { "name": "Primitive Obsession", "weight": 0.0 }
       ]
+    },
+    {
+      "matching_content_path": "**/kani_proofs/**",
+      "matching_content_path_doc": "Kani proof modules. Harness setup is deliberately repeated per proof entry point: sharing an abstraction over a symbolic node id or level multiplies solver aliasing past the tractable CBMC state space. See the `Kani CI policy` section of docs/developers-guide.md.",
+      "rules": [
+        { "name": "Code Duplication", "weight": 0.0 },
+        { "name": "Primitive Obsession", "weight": 0.0 },
+        { "name": "Excess Number of Function Arguments", "weight": 0.0 },
+        { "name": "Complex Method", "weight": 0.3 }
+      ]
+    },
+    {
+      "matching_content_path": "**/kani_proofs.rs",
+      "matching_content_path_doc": "Single-file Kani proof module; same solver constraint as `**/kani_proofs/**`.",
+      "rules": [
+        { "name": "Code Duplication", "weight": 0.0 },
+        { "name": "Primitive Obsession", "weight": 0.0 },
+        { "name": "Excess Number of Function Arguments", "weight": 0.0 },
+        { "name": "Complex Method", "weight": 0.3 }
+      ]
+    },
+    {
+      "matching_content_path": "**/kani_harness.rs",
+      "matching_content_path_doc": "Kani harnesses. Bundling harness edge arguments into a struct was measured to help break verification: together with the sort and `kruskal_model` refactors below it took `make kani-full` from 17/17 harnesses verified to `kissat: maximum variable index exceeded`, 0 verified. See docs/kani-full-hnsw-hypothesis-testing.md.",
+      "rules": [
+        { "name": "Code Duplication", "weight": 0.0 },
+        { "name": "Primitive Obsession", "weight": 0.0 },
+        { "name": "Excess Number of Function Arguments", "weight": 0.0 },
+        { "name": "Complex Method", "weight": 0.3 }
+      ]
+    },
+    {
+      "matching_content_path": "**/kani_model.rs",
+      "matching_content_path_doc": "Bounded sequential model verified in place of the Rayon production path. Unifying its two bounded insertion sorts and decomposing `kruskal_model` inflated the CBMC formula past the SAT solver's variable-index limit, so the model stays concrete and monomorphic. Its behaviour is pinned instead by exhaustive equivalence tests against production in chutoro-core/src/mst/tests/kani_model_equivalence.rs. `Complex Method` is down-weighted rather than disabled so genuine complexity growth still surfaces in review.",
+      "rules": [
+        { "name": "Code Duplication", "weight": 0.0 },
+        { "name": "Primitive Obsession", "weight": 0.0 },
+        { "name": "Excess Number of Function Arguments", "weight": 0.0 },
+        { "name": "Complex Method", "weight": 0.3 }
+      ]
     }
   ]
 }

.github/workflows/kani-pr.yml

@@ -0,0 +1,52 @@
+name: Kani PR
+
+"on":
+  pull_request:
+    branches: [main]
+    types: [opened, synchronize, reopened]
+    paths:
+      - ".github/workflows/kani-pr.yml"
+      - "**/kani_*.rs"
+      - "chutoro-core/src/hnsw/kani_proofs/**"
+      - "chutoro-core/src/mst/kani_harness.rs"
+      - "chutoro-providers/dense/src/simd/kani_proofs.rs"
+      - "chutoro-core/src/hnsw/**"
+      - "chutoro-core/src/mst/**"
+      - "chutoro-providers/dense/src/simd/**"
+      - "Makefile"
+      - "Cargo.toml"
+      - "Cargo.lock"
+      - "chutoro-core/Cargo.toml"
+      - "chutoro-providers/dense/Cargo.toml"
+      - "tools/kani/VERSION"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: kani-pr-${{ github.ref }}
+  cancel-in-progress: true
+
+env:
+  CARGO_TERM_COLOR: always
+
+jobs:
+  kani:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+      - name: Setup Rust
+        uses: leynos/shared-actions/.github/actions/setup-rust@f4764bea8d813b1a8f7ebc37a44907d3c3b1e0e4
+      - name: Install Kani
+        run: |
+          # tools/kani/VERSION is the single source of truth for the pin;
+          # the Makefile and the workflow contract test read the same file.
+          kani_version="$(tr -d '[:space:]' < tools/kani/VERSION)"
+          cargo install --locked kani-verifier --version "$kani_version"
+          cargo kani setup
+      - name: Run Kani practical suite
+        run: make kani

Makefile

@@ -21,7 +21,8 @@ TYPOS_CONFIG_BUILDER_SOURCE := git+https://github.com/leynos/typos-config-builde
 TYPOS_CONFIG_BUILDER := $(UV_ENV) $(UV) tool run --python 3.14 \
 	--from "$(TYPOS_CONFIG_BUILDER_SOURCE)" typos-config-builder
 VERUS_BIN ?= verus
-KANI_VERSION ?= $(shell $(CARGO) kani -V | awk '{print $$2}')
+KANI_VERSION_FILE ?= tools/kani/VERSION
+KANI_VERSION ?= $(strip $(shell cat $(KANI_VERSION_FILE)))
 KANI_LIB_PATH ?= $(HOME)/.kani/kani-$(KANI_VERSION)/toolchain/lib
 KANI_ENV ?= LD_LIBRARY_PATH="$(KANI_LIB_PATH):$(LD_LIBRARY_PATH)"
 SPELLING_PY_SRCS := \
@@ -95,6 +96,8 @@ nixie: ## Validate Mermaid diagrams
 kani: ## Run Kani practical harnesses
 	$(KANI_ENV) $(CARGO) kani -p chutoro-core --default-unwind 4 --harness verify_bidirectional_links_smoke_2_nodes_1_layer
 	$(KANI_ENV) $(CARGO) kani -p chutoro-core --default-unwind 4 --harness verify_bidirectional_links_reconciliation_2_nodes_1_layer
+	$(KANI_ENV) $(CARGO) kani -p chutoro-core --default-unwind 12 --harness verify_mst_structural_correctness_4_nodes
+	$(KANI_ENV) $(CARGO) kani -p chutoro-core --default-unwind 10 --harness verify_mst_minimality_3_nodes
 	$(KANI_ENV) $(CARGO) kani -p chutoro-providers-dense --default-unwind 4 --harness verify_dense_simd_dispatch_selection_respects_support_masks
 	$(KANI_ENV) $(CARGO) kani -p chutoro-providers-dense --default-unwind 18 --harness verify_dense_simd_tail_padding_lane_bounds
 
@@ -108,8 +111,8 @@ verus: ## Run Verus proofs for edge harvest primitives
 bench: ## Run Criterion benchmarks
 	$(CARGO) bench -p chutoro-benches
 
-test-workflow-contracts: ## Validate the mutation-testing caller contract
-	uv run --with 'pytest>=8' --with 'pyyaml>=6' pytest tests/workflow_contracts -q
+test-workflow-contracts: ## Validate the CI workflow contracts
+	uv run --with 'pytest>=8' --with 'pyyaml>=6' --with 'pathspec>=0.12' pytest tests/workflow_contracts -q
 
 help: ## Show available targets
 	@grep -E '^[a-zA-Z_-]+:.*?##' $(MAKEFILE_LIST) | \

chutoro-core/src/hnsw/cpu/construction.rs

@@ -146,6 +146,22 @@ impl CpuHnsw {
                 reason: "capacity must be greater than zero".into(),
             });
         }
+        #[cfg(feature = "metrics")]
+        {
+            metrics::describe_counter!(
+                "chutoro.hnsw.reconciliation.healed_nodes_total",
+                metrics::Unit::Count,
+                "Nodes re-linked to the entry after removed-edge \
+                 reconciliation isolated them at the base layer."
+            );
+            metrics::describe_counter!(
+                "chutoro.hnsw.reconciliation.orphan_scrubs_total",
+                metrics::Unit::Count,
+                "Orphaned forward edges removed by deferred scrubs, \
+                 labelled by base or upper layer."
+            );
+        }
+
         let base_seed = params.rng_seed();
         let worker_rngs = build_worker_rngs(base_seed);
 

chutoro-core/src/hnsw/graph/core.rs

@@ -170,6 +170,29 @@ pub(crate) struct Graph {
     pub(super) entry: Option<EntryPoint>,
 }
 
+/// Reasons a node context fails validation during attachment.
+///
+/// Shared by the production and Kani constructors so both map the same
+/// checks to their own error representations.
+#[derive(Clone, Copy, Debug)]
+enum AttachNodeError {
+    LevelExceedsMax,
+    OutsideCapacity,
+    Duplicate,
+}
+
+#[cfg(kani)]
+impl AttachNodeError {
+    /// Returns the static reason used by the Kani constructors.
+    fn static_reason(self) -> &'static str {
+        match self {
+            Self::LevelExceedsMax => "node level exceeds max_level",
+            Self::OutsideCapacity => "node is outside pre-allocated capacity",
+            Self::Duplicate => "node already exists",
+        }
+    }
+}
+
 fn should_promote_entry(current: Option<EntryPoint>, level: usize) -> bool {
     level > current.map(|entry| entry.level).unwrap_or(0)
 }
@@ -225,37 +248,68 @@ impl Graph {
 
     pub(crate) fn insert_first(&mut self, ctx: NodeContext) -> Result<(), HnswError> {
         self.attach_node(ctx)?;
-        self.entry = Some(EntryPoint {
-            node: ctx.node,
-            level: ctx.level,
-        });
+        self.promote_entry_to(ctx);
         Ok(())
     }
 
     pub(crate) fn attach_node(&mut self, ctx: NodeContext) -> Result<(), HnswError> {
-        if ctx.level > self.params.max_level() {
-            return Err(HnswError::InvalidParameters {
+        self.attach_node_inner(ctx).map_err(|reason| match reason {
+            AttachNodeError::LevelExceedsMax => HnswError::InvalidParameters {
                 reason: format!(
                     "node {}: level {} exceeds max_level {}",
                     ctx.node,
                     ctx.level,
                     self.params.max_level()
                 ),
-            });
-        }
-        let slot = self
-            .nodes
-            .get_mut(ctx.node)
-            .ok_or_else(|| HnswError::InvalidParameters {
+            },
+            AttachNodeError::OutsideCapacity => HnswError::InvalidParameters {
                 reason: format!("node {} is outside pre-allocated capacity", ctx.node),
-            })?;
+            },
+            AttachNodeError::Duplicate => HnswError::DuplicateNode { node: ctx.node },
+        })
+    }
+
+    /// Validates the context and initialises the node slot.
+    ///
+    /// Shared by the production and Kani constructors; returns a static
+    /// reason so the Kani path never constructs formatted errors.
+    fn attach_node_inner(&mut self, ctx: NodeContext) -> Result<(), AttachNodeError> {
+        if ctx.level > self.params.max_level() {
+            return Err(AttachNodeError::LevelExceedsMax);
+        }
+        let Some(slot) = self.nodes.get_mut(ctx.node) else {
+            return Err(AttachNodeError::OutsideCapacity);
+        };
         if slot.is_some() {
-            return Err(HnswError::DuplicateNode { node: ctx.node });
+            return Err(AttachNodeError::Duplicate);
         }
         *slot = Some(Node::new(ctx.level, ctx.sequence));
         Ok(())
     }
 
+    /// Records the node as the graph entry point.
+    fn promote_entry_to(&mut self, ctx: NodeContext) {
+        self.entry = Some(EntryPoint {
+            node: ctx.node,
+            level: ctx.level,
+        });
+    }
+
+    /// Inserts the first Kani node without constructing formatted production errors.
+    #[cfg(kani)]
+    pub(crate) fn insert_first_for_kani(&mut self, ctx: NodeContext) -> Result<(), &'static str> {
+        self.attach_node_for_kani(ctx)?;
+        self.promote_entry_to(ctx);
+        Ok(())
+    }
+
+    /// Attaches a Kani node without constructing formatted production errors.
+    #[cfg(kani)]
+    pub(crate) fn attach_node_for_kani(&mut self, ctx: NodeContext) -> Result<(), &'static str> {
+        self.attach_node_inner(ctx)
+            .map_err(AttachNodeError::static_reason)
+    }
+
     #[cfg(kani)]
     pub(crate) fn should_promote_entry_for_kani(current: Option<EntryPoint>, level: usize) -> bool {
         should_promote_entry(current, level)

chutoro-core/src/hnsw/insert/commit.rs

@@ -81,7 +81,6 @@ impl<'graph> CommitApplicator<'graph> {
                 max_connections,
             };
 
-            reconciler.reconcile_removed_edges(&ctx, &previous, &next);
             reconciler.reconcile_added_edges(&ctx, &mut next);
 
             let node_ref = reconciler
@@ -92,7 +91,15 @@ impl<'graph> CommitApplicator<'graph> {
                 })?;
             let list = node_ref.neighbours_mut(level);
             list.clear();
-            list.extend(next);
+            list.extend(next.iter().copied());
+
+            // Removed-edge reconciliation must run after the origin's list is
+            // written back. Removing a neighbour's only base-layer edge makes
+            // the connectivity healer link it to the entry node; when the
+            // entry is the origin, healing against the stale pre-write-back
+            // list is clobbered by the write-back, leaving a dangling reverse
+            // edge.
+            reconciler.reconcile_removed_edges(&ctx, &previous, &next);
 
             touched.push((update.node, level));
         }

chutoro-core/src/hnsw/insert/commit/tests/deferred_scrub.rs

@@ -269,3 +269,52 @@ fn eviction_at_base_layer_triggers_healing() -> Result<(), HnswError> {
 
     Ok(())
 }
+
+/// Twin of the retired `verify_bidirectional_links_commit_path_3_nodes` Kani
+/// harness, which exceeded the tractable CBMC state space.
+///
+/// Scenario: node 0's level-1 list is at capacity with node 2. Node 1's
+/// update adds node 0, so `ensure_reverse_edge` evicts node 2 from node 0
+/// and defers a scrub for the orphaned (2 -> 0) forward edge.
+#[rstest]
+fn commit_path_reconciliation_keeps_bidirectionality(
+    params_one_connection: HnswParams,
+) -> Result<(), HnswError> {
+    // Seed node 0 at level-1 capacity with node 2 (bidirectional).
+    let ctx = EvictionTestContext::seeded(
+        params_one_connection,
+        3,
+        (0, 2),
+        NewNodeContext { id: 1, level: 1 },
+    )?;
+    let update = build_update(1, 1, vec![0], ctx.max_connections);
+    let graph = ctx.apply_updates(vec![update])?;
+
+    assert_graph_bidirectional(&graph, 3);
+    assert_no_edge(&graph, 2, 0, 1);
+
+    Ok(())
+}
+
+/// Twin of the retired `verify_eviction_deferred_scrub_reciprocity` Kani
+/// harness, which exceeded the tractable CBMC state space.
+///
+/// Scenario: node 1 is at level-1 capacity with node 2. Node 0's update adds
+/// node 1, evicting node 2 from node 1 and deferring a scrub that removes the
+/// orphaned (2 -> 1) forward edge.
+#[rstest]
+fn eviction_deferred_scrub_keeps_reciprocity(
+    params_one_connection: HnswParams,
+) -> Result<(), HnswError> {
+    // The default fixture seeds node 1 at level-1 capacity with node 2.
+    let ctx = EvictionTestContext::new(params_one_connection)?;
+    let update = build_update(0, 1, vec![1], ctx.max_connections);
+    let graph = ctx.apply_updates(vec![update])?;
+
+    assert_has_edge(&graph, 1, 0, 1);
+    assert_no_edge(&graph, 2, 1, 1);
+    assert_no_edge(&graph, 1, 2, 1);
+    assert_graph_bidirectional(&graph, 4);
+
+    Ok(())
+}