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

.github/workflows/kani-pr.yml

@@ -0,0 +1,44 @@
+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"
+  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
+      - name: Setup Rust
+        uses: leynos/shared-actions/.github/actions/setup-rust@f4764bea8d813b1a8f7ebc37a44907d3c3b1e0e4
+      - name: Install Kani
+        run: |
+          cargo install --locked kani-verifier
+          cargo kani setup
+      - name: Run Kani practical suite
+        run: make kani

Makefile

@@ -95,6 +95,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
 

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

@@ -256,6 +256,33 @@ impl Graph {
         Ok(())
     }
 
+    /// 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.entry = Some(EntryPoint {
+            node: ctx.node,
+            level: ctx.level,
+        });
+        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> {
+        if ctx.level > self.params.max_level() {
+            return Err("node level exceeds max_level");
+        }
+        let Some(slot) = self.nodes.get_mut(ctx.node) else {
+            return Err("node is outside pre-allocated capacity");
+        };
+        if slot.is_some() {
+            return Err("node already exists");
+        }
+        *slot = Some(Node::new(ctx.level, ctx.sequence));
+        Ok(())
+    }
+
     #[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,76 @@ 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> {
+    let max_connections = params_one_connection.max_connections();
+    let mut graph = Graph::with_capacity(params_one_connection, 3);
+
+    insert_node(&mut graph, 0, 1, 0)?;
+    insert_node(&mut graph, 1, 1, 1)?;
+    insert_node(&mut graph, 2, 1, 2)?;
+
+    // Seed node 0 at level-1 capacity with node 2 (bidirectional).
+    add_edge_if_missing(&mut graph, 0, 2, 1);
+    add_edge_if_missing(&mut graph, 2, 0, 1);
+
+    let update = build_update(1, 1, vec![0], max_connections);
+    let new_node = NewNodeContext { id: 1, level: 1 };
+
+    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);
+    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> {
+    let max_connections = params_one_connection.max_connections();
+    let mut graph = Graph::with_capacity(params_one_connection, 4);
+
+    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)?;
+
+    // Seed node 1 at level-1 capacity with node 2 (bidirectional).
+    add_edge_if_missing(&mut graph, 1, 2, 1);
+    add_edge_if_missing(&mut graph, 2, 1, 1);
+
+    let update = build_update(0, 1, vec![1], max_connections);
+    let new_node = NewNodeContext { id: 3, level: 1 };
+
+    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_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");
@@ -277,3 +307,47 @@ 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)?;
+
+    for node_id in 0..3usize {
+        let node = graph.node(node_id).expect("node exists");
+        for &neighbour in node.neighbours(0) {
+            let other = graph.node(neighbour).expect("neighbour exists");
+            assert!(
+                other.neighbours(0).contains(&node_id),
+                "edge {node_id}->{neighbour} has no reverse edge",
+            );
+        }
+    }
+    Ok(())
+}

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

@@ -7,12 +7,44 @@
 //! The healing process uses an iterative work queue to avoid deep recursion
 //! that could cause stack overflow with pathological graph configurations.
 
+#[cfg(not(kani))]
 use std::collections::HashSet;
 
 use super::limits::compute_connection_limit;
 use super::types::{LinkContext, UpdateContext};
 use crate::hnsw::graph::Graph;
 
+/// Visited-node set for the iterative healing queues.
+///
+/// Production builds use a `HashSet`. Under Kani the default hasher's
+/// randomized SipHash state is symbolic, which makes bounded verification of
+/// any healing path intractable, so a linear-scan `Vec` set is substituted;
+/// healing queues visit each node at most once, so the scan stays bounded.
+#[cfg(not(kani))]
+type VisitedSet = HashSet<usize>;
+
+#[cfg(kani)]
+#[derive(Debug, Default)]
+struct VisitedSet {
+    seen: Vec<usize>,
+}
+
+#[cfg(kani)]
+impl VisitedSet {
+    fn new() -> Self {
+        Self::default()
+    }
+
+    /// Inserts `id`, returning `true` when it was not already present.
+    fn insert(&mut self, id: usize) -> bool {
+        if self.seen.contains(&id) {
+            return false;
+        }
+        self.seen.push(id);
+        true
+    }
+}
+
 #[derive(Debug)]
 pub(super) struct ConnectivityHealer<'graph> {
     pub(super) graph: &'graph mut Graph,
@@ -29,7 +61,7 @@ impl<'graph> ConnectivityHealer<'graph> {
     /// due to evictions, avoiding deep recursion that could cause stack overflow.
     pub(super) fn ensure_base_connectivity(&mut self, node: usize, max_connections: usize) {
         let mut work_queue: Vec<usize> = vec![node];
-        let mut visited: HashSet<usize> = HashSet::new();
+        let mut visited = VisitedSet::new();
 
         while let Some(current) = work_queue.pop() {
             if !visited.insert(current) {
@@ -83,7 +115,7 @@ impl<'graph> ConnectivityHealer<'graph> {
     /// Processes evicted nodes iteratively to restore their connectivity.
     fn process_eviction_queue(&mut self, initial: usize, max_connections: usize) {
         let mut work_queue: Vec<usize> = vec![initial];
-        let mut visited: HashSet<usize> = HashSet::new();
+        let mut visited = VisitedSet::new();
 
         while let Some(current) = work_queue.pop() {
             if let Some(evicted) = self.try_heal_node(&mut visited, current, max_connections) {
@@ -95,7 +127,7 @@ impl<'graph> ConnectivityHealer<'graph> {
     /// Attempts to heal connectivity for a single node, returning any newly evicted node.
     fn try_heal_node(
         &mut self,
-        visited: &mut HashSet<usize>,
+        visited: &mut VisitedSet,
         current: usize,
         max_connections: usize,
     ) -> Option<usize> {