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

.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/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(())
+}

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

@@ -189,6 +189,36 @@ fn params_one_connection() -> HnswParams {
     }
 }
 
+/// Asserts that every edge in the graph has its reverse edge at every level.
+fn assert_graph_bidirectional(graph: &Graph, node_count: usize) {
+    for node_id in 0..node_count {
+        let Some(node) = graph.node(node_id) else {
+            panic!("node {node_id} should exist");
+        };
+        for level in 0..node.level_count() {
+            assert_level_edges_reciprocated(graph, node_id, node.neighbours(level), level);
+        }
+    }
+}
+
+/// Asserts that each listed neighbour links back to `node_id` at `level`.
+fn assert_level_edges_reciprocated(
+    graph: &Graph,
+    node_id: usize,
+    neighbours: &[usize],
+    level: usize,
+) {
+    for &neighbour in neighbours {
+        let Some(other) = graph.node(neighbour) else {
+            panic!("neighbour {neighbour} should exist");
+        };
+        assert!(
+            level < other.level_count() && other.neighbours(level).contains(&node_id),
+            "edge {node_id}->{neighbour} at level {level} has no reverse edge",
+        );
+    }
+}
+
 fn assert_has_edge(graph: &Graph, origin: usize, target: usize, level: usize) {
     let Some(node) = graph.node(origin) else {
         panic!("node {origin} should exist");
@@ -203,7 +233,7 @@ fn assert_has_edge(graph: &Graph, origin: usize, target: usize, level: usize) {
     );
 }
 
-/// Context for eviction tests with a 4-node graph where node 1 is at capacity.
+/// Context for eviction tests over a level-1 graph with one seeded edge pair.
 struct EvictionTestContext {
     graph: Graph,
     max_connections: usize,
@@ -214,19 +244,30 @@ impl EvictionTestContext {
     /// Creates a test graph with 4 nodes at level 1, where node 1 is seeded
     /// at capacity with a bidirectional edge to node 2.
     fn new(params: HnswParams) -> Result<Self, HnswError> {
+        Self::seeded(params, 4, (1, 2), NewNodeContext { id: 3, level: 1 })
+    }
+
+    /// Creates a test graph with `node_count` nodes at level 1, seeding the
+    /// `seeded_pair` nodes with a bidirectional level-1 edge so the first of
+    /// the pair sits at capacity.
+    fn seeded(
+        params: HnswParams,
+        node_count: usize,
+        seeded_pair: (usize, usize),
+        new_node: NewNodeContext,
+    ) -> Result<Self, HnswError> {
         let max_connections = params.max_connections();
-        let mut graph = Graph::with_capacity(params, 4);
+        let mut graph = Graph::with_capacity(params, node_count);
 
-        insert_node(&mut graph, 0, 1, 0)?;
-        insert_node(&mut graph, 1, 1, 1)?;
-        insert_node(&mut graph, 2, 1, 2)?;
-        insert_node(&mut graph, 3, 1, 3)?;
+        for node in 0..node_count {
+            let sequence = u64::try_from(node).unwrap_or(u64::MAX);
+            insert_node(&mut graph, node, 1, sequence)?;
+        }
 
-        // Seed node 1 at capacity with node 2 (bidirectional)
-        add_edge_if_missing(&mut graph, 1, 2, 1);
-        add_edge_if_missing(&mut graph, 2, 1, 1);
+        let (first, second) = seeded_pair;
+        add_edge_if_missing(&mut graph, first, second, 1);
+        add_edge_if_missing(&mut graph, second, first, 1);
 
-        let new_node = NewNodeContext { id: 3, level: 1 };
         Ok(Self {
             graph,
             max_connections,
@@ -277,3 +318,38 @@ fn eviction_scrubs_orphaned_forward_edge(
 }
 
 mod deferred_scrub;
+
+/// Regression test: replacing a neighbour whose only base-layer edge was to
+/// the origin must not leave a dangling reverse edge.
+///
+/// Removing node 1 from node 0's list isolates node 1 at the base layer, so
+/// the connectivity healer links it back to the entry node, which is node 0
+/// itself. Removed-edge reconciliation therefore has to run after node 0's
+/// neighbour list is written back; healing against the stale pre-write-back
+/// list is clobbered by the write-back, leaving `1 -> 0` without `0 -> 1`.
+#[rstest]
+fn isolation_replacement_keeps_bidirectionality(
+    params_two_connections: HnswParams,
+) -> Result<(), HnswError> {
+    let max_connections = params_two_connections.max_connections();
+    let mut graph = Graph::with_capacity(params_two_connections, 3);
+
+    insert_node(&mut graph, 0, 0, 0)?;
+    insert_node(&mut graph, 1, 0, 1)?;
+    insert_node(&mut graph, 2, 0, 2)?;
+
+    add_edge_if_missing(&mut graph, 0, 1, 0);
+    add_edge_if_missing(&mut graph, 1, 0, 0);
+
+    // Node 0 replaces neighbour 1 with neighbour 2, isolating node 1.
+    let update = build_update(0, 0, vec![2], max_connections);
+    let new_node = NewNodeContext { id: 2, level: 0 };
+
+    let mut applicator = CommitApplicator::new(&mut graph);
+    let (reciprocated, _) =
+        applicator.apply_neighbour_updates(vec![update], max_connections, new_node)?;
+    applicator.apply_new_node_neighbours(new_node.id, new_node.level, reciprocated)?;
+
+    assert_graph_bidirectional(&graph, 3);
+    Ok(())
+}