diff --git a/.codescene/code-health-rules.json b/.codescene/code-health-rules.json index ba7a8f0e..4b43f3b4 100644 --- a/.codescene/code-health-rules.json +++ b/.codescene/code-health-rules.json @@ -1,4 +1,5 @@ { + "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", @@ -6,6 +7,47 @@ "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. The model is excluded from CodeScene method checks because their prescribed decompositions invalidate the bounded proof; reconsider the exception only with successful `make kani` and `make kani-full` verification.", + "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.0 }, + { "name": "Large Method", "weight": 0.0 } + ] } ] } diff --git a/.github/workflows/kani-pr.yml b/.github/workflows/kani-pr.yml new file mode 100644 index 00000000..61832342 --- /dev/null +++ b/.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 diff --git a/Makefile b/Makefile index 223a46ae..53e0fb41 100644 --- a/Makefile +++ b/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) | \ diff --git a/chutoro-core/src/hnsw/cpu/construction.rs b/chutoro-core/src/hnsw/cpu/construction.rs index 0e0ee254..91fd3d27 100644 --- a/chutoro-core/src/hnsw/cpu/construction.rs +++ b/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); diff --git a/chutoro-core/src/hnsw/graph/core.rs b/chutoro-core/src/hnsw/graph/core.rs index 833337f8..338bd308 100644 --- a/chutoro-core/src/hnsw/graph/core.rs +++ b/chutoro-core/src/hnsw/graph/core.rs @@ -170,6 +170,29 @@ pub(crate) struct Graph { pub(super) entry: Option, } +/// 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, 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, level: usize) -> bool { should_promote_entry(current, level) diff --git a/chutoro-core/src/hnsw/insert/commit.rs b/chutoro-core/src/hnsw/insert/commit.rs index 9908ab96..38df6ddc 100644 --- a/chutoro-core/src/hnsw/insert/commit.rs +++ b/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)); } diff --git a/chutoro-core/src/hnsw/insert/commit/tests/deferred_scrub.rs b/chutoro-core/src/hnsw/insert/commit/tests/deferred_scrub.rs index c4ed3284..c461a380 100644 --- a/chutoro-core/src/hnsw/insert/commit/tests/deferred_scrub.rs +++ b/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(()) +} diff --git a/chutoro-core/src/hnsw/insert/commit/tests/mod.rs b/chutoro-core/src/hnsw/insert/commit/tests/mod.rs index 4fb9184a..965c8441 100644 --- a/chutoro-core/src/hnsw/insert/commit/tests/mod.rs +++ b/chutoro-core/src/hnsw/insert/commit/tests/mod.rs @@ -12,6 +12,7 @@ use crate::hnsw::{ use rstest::{fixture, rstest}; #[fixture] +/// Provides parameters with a fan-out of two for commit tests. fn params_two_connections() -> HnswParams { match HnswParams::new(2, 4) { Ok(params) => params, @@ -19,6 +20,7 @@ fn params_two_connections() -> HnswParams { } } +/// Inserts a node, seeding the entry point on the first insertion. fn insert_node( graph: &mut Graph, node: usize, @@ -37,6 +39,7 @@ fn insert_node( } } +/// Panics unless the two nodes link to each other at the level. fn assert_bidirectional_edge(graph: &Graph, node_a: usize, node_b: usize, level: usize) { let Some(a) = graph.node(node_a) else { panic!("node {node_a} should exist"); @@ -58,6 +61,7 @@ fn assert_bidirectional_edge(graph: &Graph, node_a: usize, node_b: usize, level: ); } +/// Builds a staged update paired with its finalized neighbour list. fn build_update( node: usize, level: usize, @@ -182,6 +186,7 @@ fn commit_updates_report_missing_origin(params_two_connections: HnswParams) { // --------------------------------------------------------------------------- #[fixture] +/// Provides parameters with a fan-out of one so level 1 evicts. fn params_one_connection() -> HnswParams { match HnswParams::new(1, 4) { Ok(params) => params, @@ -189,6 +194,37 @@ 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", + ); + } +} + +/// Panics unless the directed edge is present at the level. 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 +239,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 +250,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::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 { 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 +324,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(()) +} diff --git a/chutoro-core/src/hnsw/insert/connectivity.rs b/chutoro-core/src/hnsw/insert/connectivity.rs index 2a7e3289..a87d2229 100644 --- a/chutoro-core/src/hnsw/insert/connectivity.rs +++ b/chutoro-core/src/hnsw/insert/connectivity.rs @@ -7,18 +7,63 @@ //! 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 the linear-scan set below is substituted; +/// healing queues visit each node at most once, so the scan stays bounded. +#[cfg(not(kani))] +type VisitedSet = HashSet; + +#[cfg(kani)] +type VisitedSet = LinearVisitedSet; + +/// Linear-scan visited set standing in for `HashSet` under Kani. +/// +/// Compiled under `cfg(test)` as well so its equivalence to `HashSet` +/// semantics is asserted in normal CI: the healing path itself is past the +/// tractable CBMC state space even at two nodes (a direct harness timed out +/// in symbolic execution), so this substitute is validated by test rather +/// than by proof. +#[cfg(any(kani, test))] +#[derive(Debug, Default)] +struct LinearVisitedSet { + seen: Vec, +} + +#[cfg(any(kani, test))] +impl LinearVisitedSet { + /// Creates an empty visited set. + #[cfg(kani)] + 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, } impl<'graph> ConnectivityHealer<'graph> { + /// Creates a healer over the graph. pub(super) fn new(graph: &'graph mut Graph) -> Self { Self { graph } } @@ -29,7 +74,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 = vec![node]; - let mut visited: HashSet = HashSet::new(); + let mut visited = VisitedSet::new(); while let Some(current) = work_queue.pop() { if !visited.insert(current) { @@ -56,6 +101,7 @@ impl<'graph> ConnectivityHealer<'graph> { } } + /// Links the new node to the origin, dispatching on layer semantics. pub(super) fn link_new_node(&mut self, ctx: &UpdateContext, new_node: usize) -> bool { if ctx.level == 0 { self.link_new_node_base_layer(ctx, new_node) @@ -83,7 +129,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 = vec![initial]; - let mut visited: HashSet = 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 +141,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, + visited: &mut VisitedSet, current: usize, max_connections: usize, ) -> Option { @@ -246,3 +292,35 @@ impl<'graph> ConnectivityHealer<'graph> { None } } + +#[cfg(test)] +mod tests { + //! Equivalence coverage for the Kani visited-set substitute. + + use std::collections::HashSet; + + use rstest::rstest; + + use super::LinearVisitedSet; + + /// The linear-scan set must report insertions exactly as `HashSet` does, + /// because Kani builds substitute it for the production `HashSet` inside + /// the healing work queues. + #[rstest] + #[case::all_unique(&[1, 2, 3, 4])] + #[case::immediate_duplicate(&[7, 7])] + #[case::interleaved_duplicates(&[3, 1, 3, 2, 1, 3])] + #[case::single(&[0])] + #[case::empty(&[])] + fn linear_set_matches_hash_set_semantics(#[case] sequence: &[usize]) { + let mut linear = LinearVisitedSet::default(); + let mut hashed = HashSet::new(); + for &id in sequence { + assert_eq!( + linear.insert(id), + hashed.insert(id), + "insert({id}) diverged from HashSet semantics", + ); + } + } +} diff --git a/chutoro-core/src/hnsw/insert/mod.rs b/chutoro-core/src/hnsw/insert/mod.rs index da1ce675..beb30046 100644 --- a/chutoro-core/src/hnsw/insert/mod.rs +++ b/chutoro-core/src/hnsw/insert/mod.rs @@ -20,8 +20,6 @@ mod types; pub(super) use executor::{InsertionExecutor, TrimJob, TrimResult}; pub(super) use planner::{InsertionPlanner, PlanningInputs}; -#[cfg(kani)] -pub(crate) use types::{FinalisedUpdate, NewNodeContext, StagedUpdate}; use crate::hnsw::types::{CandidateEdge, InsertionPlan}; @@ -140,164 +138,6 @@ fn assume_node_has_level(graph: &crate::hnsw::graph::Graph, node_id: usize, leve kani::assume(neighbours_deduped); } -/// Validates that the new node exists, exposes the level, and has deduplicated -/// neighbours at that level. -#[cfg(kani)] -fn validate_new_node_for_kani(graph: &crate::hnsw::graph::Graph, new_node: &types::NewNodeContext) { - assume_node_has_level(graph, new_node.id, new_node.level); -} - -/// Validates the origin node state, neighbour list structure, and target nodes -/// for commit-path updates. -#[cfg(kani)] -fn validate_update_for_kani( - graph: &crate::hnsw::graph::Graph, - update: &types::FinalisedUpdate, - max_connections: usize, -) { - let (staged, neighbours) = update; - assume_node_has_level(graph, staged.node, staged.ctx.level); - - let deduped = is_deduped(neighbours.as_slice()); - debug_assert!( - deduped, - "Kani commit update neighbour list must be deduplicated" - ); - kani::assume(deduped); - - let no_self_loops = !neighbours.contains(&staged.node); - debug_assert!( - no_self_loops, - "Kani commit update neighbours must not contain the origin" - ); - kani::assume(no_self_loops); - - let limit = limits::compute_connection_limit(staged.ctx.level, max_connections); - let within_limit = neighbours.len() <= limit; - debug_assert!( - within_limit, - "Kani commit update neighbours must respect connection limits" - ); - kani::assume(within_limit); - - let mut targets_exist = true; - let mut targets_level_valid = true; - for &id in neighbours { - let candidate = graph.node(id); - let exists = candidate.is_some(); - targets_exist &= exists; - let level_valid = candidate - .map(|node| staged.ctx.level < node.level_count()) - .unwrap_or(false); - targets_level_valid &= level_valid; - } - debug_assert!( - targets_exist, - "Kani commit update neighbours must exist in the graph" - ); - kani::assume(targets_exist); - - debug_assert!( - targets_level_valid, - "Kani commit update neighbours must expose the requested level" - ); - kani::assume(targets_level_valid); -} - -/// Applies the full commit-path update sequence for Kani harnesses. -/// -/// This helper drives the same reconciliation and deferred scrub logic used in -/// production by calling [`CommitApplicator::apply_neighbour_updates`] and -/// [`CommitApplicator::apply_new_node_neighbours`]. It constrains inputs to -/// match production preconditions so Kani explores valid states. -#[cfg(kani)] -pub(crate) fn apply_commit_updates_for_kani( - graph: &mut crate::hnsw::graph::Graph, - max_connections: usize, - new_node: types::NewNodeContext, - updates: Vec, -) -> Result<(), crate::hnsw::error::HnswError> { - validate_new_node_for_kani(graph, &new_node); - - for update in &updates { - validate_update_for_kani(graph, update, max_connections); - } - - let mut applicator = commit::CommitApplicator::new(graph); - let (reciprocated, _touched) = - applicator.apply_neighbour_updates(updates, max_connections, new_node)?; - applicator.apply_new_node_neighbours(new_node.id, new_node.level, reciprocated)?; - - Ok(()) -} - -/// Applies reconciliation logic to a single update for Kani harnesses. -/// -/// This helper mirrors the production commit flow (removed-edge reconciliation, -/// added-edge reconciliation, list write-back, and deferred scrubs) while -/// keeping the setup compact for bounded verification. -/// -/// # Examples -/// ```rust,ignore -/// use crate::hnsw::{ -/// graph::{Graph, NodeContext}, -/// insert::{apply_reconciled_update_for_kani, KaniUpdateContext}, -/// params::HnswParams, -/// }; -/// -/// let params = HnswParams::new(2, 2).expect("params must be valid"); -/// let mut graph = Graph::with_capacity(params, 2); -/// graph -/// .insert_first(NodeContext { node: 0, level: 0, sequence: 0 }) -/// .expect("insert node 0"); -/// graph -/// .attach_node(NodeContext { node: 1, level: 0, sequence: 1 }) -/// .expect("attach node 1"); -/// let ctx = KaniUpdateContext::new(0, 0, 2); -/// let mut next = vec![1]; -/// apply_reconciled_update_for_kani(&mut graph, ctx, &mut next); -/// ``` -#[cfg(kani)] -pub(crate) fn apply_reconciled_update_for_kani( - graph: &mut crate::hnsw::graph::Graph, - ctx: KaniUpdateContext, - next: &mut Vec, -) { - assume_node_has_level(graph, ctx.origin, ctx.level); - next.retain(|&target| target != ctx.origin); - let previous = graph - .node(ctx.origin) - .map(|node| node.neighbours(ctx.level).to_vec()) - .unwrap_or_else(|| { - debug_assert!(false, "Kani update origin must exist in the graph"); - Vec::new() - }); - - let next_deduped = is_deduped(next); - debug_assert!(next_deduped, "Kani update next list must be deduplicated"); - kani::assume(next_deduped); - for &target in next.iter() { - assume_node_has_level(graph, target, ctx.level); - } - - let update_ctx = types::UpdateContext { - origin: ctx.origin, - level: ctx.level, - max_connections: ctx.max_connections, - }; - let mut reconciler = reconciliation::EdgeReconciler::new(graph); - reconciler.reconcile_removed_edges(&update_ctx, &previous, next.as_slice()); - reconciler.reconcile_added_edges(&update_ctx, next); - - if let Some(node_ref) = reconciler.graph_mut().node_mut(ctx.origin) { - let list = node_ref.neighbours_mut(ctx.level); - list.clear(); - list.extend(next.iter().copied()); - } - - reconciler.apply_deferred_scrubs(ctx.max_connections); -} - /// Ensures a reverse edge using the production reconciler for Kani harnesses. /// /// This helper calls the same reconciliation code used during insertion diff --git a/chutoro-core/src/hnsw/insert/reconciliation.rs b/chutoro-core/src/hnsw/insert/reconciliation.rs index 0d6fac50..2cf0b00a 100644 --- a/chutoro-core/src/hnsw/insert/reconciliation.rs +++ b/chutoro-core/src/hnsw/insert/reconciliation.rs @@ -24,6 +24,7 @@ pub(super) struct EdgeReconciler<'graph> { } impl<'graph> EdgeReconciler<'graph> { + /// Creates a reconciler over the graph with no scrubs pending. pub(super) fn new(graph: &'graph mut Graph) -> Self { Self { graph, @@ -31,14 +32,20 @@ impl<'graph> EdgeReconciler<'graph> { } } + /// Returns mutable access to the underlying graph. pub(super) fn graph_mut(&mut self) -> &mut Graph { self.graph } + /// Returns shared access to the underlying graph. pub(super) fn graph(&self) -> &Graph { self.graph } + /// Removes reciprocal edges for neighbours dropped from the origin. + /// + /// Runs after the origin's list write-back so base-layer healing of any + /// newly isolated node observes final state rather than the stale list. pub(super) fn reconcile_removed_edges( &mut self, ctx: &UpdateContext, @@ -72,16 +79,30 @@ impl<'graph> EdgeReconciler<'graph> { return; } + tracing::debug!( + operation = "reconcile_removed_edges", + level = ctx.level, + isolated_count = isolated.len(), + "healing base connectivity for nodes isolated by removed edges" + ); + #[cfg(feature = "metrics")] + metrics::counter!("chutoro.hnsw.reconciliation.healed_nodes_total") + .increment(isolated.len() as u64); let mut healer = ConnectivityHealer::new(self.graph); for node in isolated { healer.ensure_base_connectivity(node, ctx.max_connections); } } + /// Retains only targets whose reverse edge could be ensured. pub(super) fn reconcile_added_edges(&mut self, ctx: &UpdateContext, next: &mut Vec) { next.retain(|&target| self.ensure_reverse_edge(ctx, target)); } + /// Ensures `target` links back to the origin, evicting if at capacity. + /// + /// Returns `false` when the target is missing or lacks the level. An + /// eviction defers a scrub for the orphaned forward edge. pub(super) fn ensure_reverse_edge(&mut self, ctx: &UpdateContext, target: usize) -> bool { let Some(target_node) = self.graph.node_mut(target) else { return false; @@ -155,6 +176,17 @@ impl<'graph> EdgeReconciler<'graph> { continue; } + tracing::debug!( + operation = "apply_deferred_scrubs", + level = scrub.level, + "scrubbing orphaned forward edge left by an eviction" + ); + #[cfg(feature = "metrics")] + metrics::counter!( + "chutoro.hnsw.reconciliation.orphan_scrubs_total", + "layer" => if scrub.level == 0 { "base" } else { "upper" } + ) + .increment(1); let ctx = UpdateContext { origin: scrub.origin, level: scrub.level, @@ -175,6 +207,8 @@ impl<'graph> EdgeReconciler<'graph> { neighbour_was_removed && is_base_layer && is_now_isolated } + /// Removes the origin's forward edge to `target`, healing base-layer + /// isolation the removal causes. pub(super) fn remove_forward_edge_from(&mut self, ctx: &UpdateContext, target: usize) { let Some(origin_node) = self.graph.node_mut(ctx.origin) else { return; diff --git a/chutoro-core/src/hnsw/insert/test_helpers.rs b/chutoro-core/src/hnsw/insert/test_helpers.rs index e853b42c..d4dd266a 100644 --- a/chutoro-core/src/hnsw/insert/test_helpers.rs +++ b/chutoro-core/src/hnsw/insert/test_helpers.rs @@ -1,11 +1,18 @@ //! Test-only helpers for repairing graph connectivity and reciprocity. +// `cargo kani` sets `cfg(kani)` but not `cfg(test)`, so anything reachable +// only from tests must be gated or it becomes dead code under `-D warnings`. +#[cfg(test)] use super::{ connectivity::ConnectivityHealer, limits::compute_connection_limit, reconciliation::EdgeReconciler, types::UpdateContext, }; use crate::hnsw::graph::Graph; +/// Appends a directed edge unless it is already present. +/// +/// The Kani body asserts the origin exists so proofs stay non-vacuous; +/// the test body downgrades that to a debug assertion. pub(crate) fn add_edge_if_missing(graph: &mut Graph, origin: usize, target: usize, level: usize) { #[cfg(kani)] { @@ -32,6 +39,8 @@ pub(crate) fn add_edge_if_missing(graph: &mut Graph, origin: usize, target: usiz } } +#[cfg(test)] +/// Panics when the directed edge is present at the given level. pub(super) fn assert_no_edge(graph: &Graph, origin: usize, target: usize, level: usize) { if let Some(node) = graph.node(origin) && level < node.level_count() @@ -43,11 +52,13 @@ pub(super) fn assert_no_edge(graph: &Graph, origin: usize, target: usize, level: } } +#[cfg(test)] #[derive(Debug)] pub(super) struct TestHelpers<'graph> { pub(super) graph: &'graph mut Graph, } +#[cfg(test)] impl<'graph> TestHelpers<'graph> { pub(super) fn new(graph: &'graph mut Graph) -> Self { Self { graph } diff --git a/chutoro-core/src/hnsw/kani_proofs/bidirectional.rs b/chutoro-core/src/hnsw/kani_proofs/bidirectional.rs index e48f5258..85cbf378 100644 --- a/chutoro-core/src/hnsw/kani_proofs/bidirectional.rs +++ b/chutoro-core/src/hnsw/kani_proofs/bidirectional.rs @@ -1,14 +1,9 @@ //! Bidirectional-link Kani harnesses for bounded HNSW graphs. -use super::{add_bidirectional_edge, push_if_absent}; +use super::add_bidirectional_edge; use crate::hnsw::{ - error::HnswError, - graph::{EdgeContext, Graph, NodeContext}, - insert::{ - FinalisedUpdate, KaniUpdateContext, NewNodeContext, StagedUpdate, - apply_commit_updates_for_kani, apply_reconciled_update_for_kani, - ensure_reverse_edge_for_kani, test_helpers::add_edge_if_missing, - }, + graph::{Graph, NodeContext}, + insert::{KaniUpdateContext, ensure_reverse_edge_for_kani, test_helpers::add_edge_if_missing}, invariants::is_bidirectional, params::HnswParams, }; @@ -20,143 +15,34 @@ use crate::hnsw::{ #[kani::proof] #[kani::unwind(4)] fn verify_bidirectional_links_smoke_2_nodes_1_layer() { - let Ok(params) = HnswParams::new(1, 1) else { + let Ok(params) = HnswParams::new_for_kani(1, 1) else { kani::assert(false, "Kani params must be valid"); return; }; let mut graph = Graph::with_capacity(params, 2); - let inserted = graph - .insert_first(NodeContext { - node: 0, - level: 0, - sequence: 0, - }) - .is_ok(); - kani::assert(inserted, "Kani smoke insert must succeed"); - let attached = graph - .attach_node(NodeContext { - node: 1, - level: 0, - sequence: 1, - }) - .is_ok(); - kani::assert(attached, "Kani smoke attach must succeed"); - - add_bidirectional_edge(&mut graph, 0, 1, 0); - - kani::assert( - is_bidirectional(&graph), - "bidirectional invariant violated in smoke harness", - ); -} - -/// Builds the 3-node, 2-level graph used by the commit-path harness. -/// -/// Inserts nodes 0, 1, and 2 at level 1 and seeds a bidirectional edge -/// between nodes 0 and 2 so that node 0's level-1 neighbour list is at -/// capacity before the commit path runs. -/// -/// Returns `(graph, max_connections)` on success. -fn setup_commit_path_graph() -> Result<(Graph, usize), HnswError> { - let params = HnswParams::new(1, 2)?; - let max_connections = params.max_connections(); - let mut graph = Graph::with_capacity(params, 3); - graph.insert_first(NodeContext { + let Ok(()) = graph.insert_first_for_kani(NodeContext { node: 0, - level: 1, + level: 0, sequence: 0, - })?; - graph.attach_node(NodeContext { - node: 1, - level: 1, - sequence: 1, - })?; - graph.attach_node(NodeContext { - node: 2, - level: 1, - sequence: 2, - })?; - add_edge_if_missing(&mut graph, 0, 2, 1); - add_edge_if_missing(&mut graph, 2, 0, 1); - Ok((graph, max_connections)) -} - -/// Verifies that HNSW graph edges are bidirectional (symmetric). -/// -/// This harness drives the production commit-path reconciliation logic to -/// ensure that bidirectional edges and deferred scrubs produce a symmetric -/// graph for a bounded configuration. -/// -/// # Verification Bounds -/// -/// - **Nodes**: 3 (IDs 0, 1, 2) -/// - **Levels**: 2 (levels 0 and 1) to allow capacity-1 eviction on level 1 -/// - **Edges**: Deterministic setup to trigger a deferred scrub -/// -/// # Invariant Under Test -/// -/// The bidirectional links invariant states that for every directed edge -/// `(u, v)` at level `l`, there must exist a reverse edge `(v, u)` at the -/// same level. This is essential for HNSW search correctness. -/// -/// # What This Proves -/// -/// If this harness passes, Kani has verified that the commit-path -/// reconciliation logic (including deferred scrubs) produces a bidirectional -/// graph for the bounded configuration. -#[kani::proof] -#[kani::unwind(10)] -fn verify_bidirectional_links_commit_path_3_nodes() { - let Ok((mut graph, max_connections)) = setup_commit_path_graph() else { - kani::assert(false, "commit-path graph setup must succeed"); - return; - }; - - let Some(node_zero) = graph.node(0) else { - kani::assert(false, "node 0 must exist after seeding commit-path edge"); + }) else { + kani::assert(false, "Kani smoke insert must succeed"); return; }; - let Some(node_two) = graph.node(2) else { - kani::assert(false, "node 2 must exist after seeding commit-path edge"); + let Ok(()) = graph.attach_node_for_kani(NodeContext { + node: 1, + level: 0, + sequence: 1, + }) else { + kani::assert(false, "Kani smoke attach must succeed"); return; }; - kani::assert( - node_zero.neighbours(1).contains(&2), - "node 0 must contain seeded level-1 edge to node 2", - ); - kani::assert( - node_two.neighbours(1).contains(&0), - "node 2 must contain seeded level-1 edge to node 0", - ); - let update_ctx = EdgeContext { - level: 1, - max_connections, - }; - let staged = StagedUpdate { - node: 1, - ctx: update_ctx, - candidates: vec![0], - }; - let updates: Vec = vec![(staged, vec![0])]; - let new_node = NewNodeContext { id: 1, level: 1 }; - apply_commit_updates_for_kani(&mut graph, max_connections, new_node, updates) - .expect("commit-path updates must succeed"); + add_bidirectional_edge(&mut graph, 0, 1, 0); kani::assert( is_bidirectional(&graph), - "bidirectional invariant violated after commit-path reconciliation", - ); - - let Some(node_two) = graph.node(2) else { - kani::assert(false, "node 2 must exist after commit-path reconciliation"); - return; - }; - let node_two_has_edge = node_two.neighbours(1).contains(&0); - kani::assert( - !node_two_has_edge, - "deferred scrub should remove evicted forward edge", + "bidirectional invariant violated in smoke harness", ); } @@ -175,29 +61,29 @@ fn verify_bidirectional_links_commit_path_3_nodes() { #[kani::proof] #[kani::unwind(4)] fn verify_bidirectional_links_reconciliation_2_nodes_1_layer() { - let Ok(params) = HnswParams::new(1, 1) else { + let Ok(params) = HnswParams::new_for_kani(1, 1) else { kani::assert(false, "Kani params must be valid"); return; }; let max_connections = params.max_connections(); let mut graph = Graph::with_capacity(params, 2); - let inserted = graph - .insert_first(NodeContext { - node: 0, - level: 0, - sequence: 0, - }) - .is_ok(); - kani::assert(inserted, "Kani reconciliation insert must succeed"); - let attached = graph - .attach_node(NodeContext { - node: 1, - level: 0, - sequence: 1, - }) - .is_ok(); - kani::assert(attached, "Kani reconciliation attach must succeed"); + let Ok(()) = graph.insert_first_for_kani(NodeContext { + node: 0, + level: 0, + sequence: 0, + }) else { + kani::assert(false, "Kani reconciliation insert must succeed"); + return; + }; + let Ok(()) = graph.attach_node_for_kani(NodeContext { + node: 1, + level: 0, + sequence: 1, + }) else { + kani::assert(false, "Kani reconciliation attach must succeed"); + return; + }; let should_link = kani::any::(); if should_link { add_edge_if_missing(&mut graph, 0, 1, 0); @@ -211,65 +97,3 @@ fn verify_bidirectional_links_reconciliation_2_nodes_1_layer() { "bidirectional invariant violated after reconciliation", ); } - -/// Verifies reconciliation on a 3-node graph (heavier, but broader coverage). -/// -/// This harness is intentionally more expensive and is intended for -/// `make kani-full` runs rather than the default `make kani`. -#[kani::proof] -#[kani::unwind(10)] -fn verify_bidirectional_links_reconciliation_3_nodes_1_layer() { - let params = HnswParams::new(2, 2).expect("params must be valid"); - let max_connections = params.max_connections(); - let mut graph = Graph::with_capacity(params, 3); - - graph - .insert_first(NodeContext { - node: 0, - level: 0, - sequence: 0, - }) - .expect("insert node 0"); - graph - .attach_node(NodeContext { - node: 1, - level: 0, - sequence: 1, - }) - .expect("attach node 1"); - graph - .attach_node(NodeContext { - node: 2, - level: 0, - sequence: 2, - }) - .expect("attach node 2"); - - // Seed a bidirectional baseline graph. - if kani::any::() { - add_bidirectional_edge(&mut graph, 0, 1, 0); - } - if kani::any::() { - add_bidirectional_edge(&mut graph, 0, 2, 0); - } - if kani::any::() { - add_bidirectional_edge(&mut graph, 1, 2, 0); - } - - // Proposed trimmed neighbours for node 0 (may add or remove edges). - let mut next: Vec = Vec::new(); - if kani::any::() { - push_if_absent(&mut next, 1); - } - if kani::any::() { - push_if_absent(&mut next, 2); - } - - let ctx = KaniUpdateContext::new(0, 0, max_connections); - apply_reconciled_update_for_kani(&mut graph, ctx, &mut next); - - kani::assert( - is_bidirectional(&graph), - "bidirectional invariant violated after reconciliation", - ); -} diff --git a/chutoro-core/src/hnsw/kani_proofs/eviction.rs b/chutoro-core/src/hnsw/kani_proofs/eviction.rs deleted file mode 100644 index 3e747ffc..00000000 --- a/chutoro-core/src/hnsw/kani_proofs/eviction.rs +++ /dev/null @@ -1,141 +0,0 @@ -//! Eviction-focused Kani harnesses for HNSW commit reconciliation. - -use super::{EdgeAssertion, has_node_link}; -use crate::hnsw::{ - error::HnswError, - graph::{EdgeContext, Graph, NodeContext}, - insert::{ - FinalisedUpdate, NewNodeContext, StagedUpdate, apply_commit_updates_for_kani, - test_helpers::add_edge_if_missing, - }, - invariants::is_bidirectional, - params::HnswParams, -}; - -/// Sets up a graph with 4 nodes at level 1 for eviction testing. -/// -/// Returns a graph with nodes 0, 1, 2, 3 all inserted at level 1, -/// configured with `max_connections = 1` so that level 1 has capacity 1. -fn setup_eviction_test_graph(params: HnswParams) -> Result { - let mut graph = Graph::with_capacity(params, 4); - - // Insert 4 nodes at level 1 - graph.insert_first(NodeContext { - node: 0, - level: 1, - sequence: 0, - })?; - graph.attach_node(NodeContext { - node: 1, - level: 1, - sequence: 1, - })?; - graph.attach_node(NodeContext { - node: 2, - level: 1, - sequence: 2, - })?; - graph.attach_node(NodeContext { - node: 3, - level: 1, - sequence: 3, - })?; - - Ok(graph) -} - -/// Verifies that eviction triggers correct deferred scrub behaviour. -/// -/// This harness exercises the eviction path in `ensure_reverse_edge` and -/// verifies that `apply_deferred_scrubs` correctly removes orphaned forward -/// edges while maintaining the bidirectional invariant. -/// -/// # Verification Bounds -/// -/// - **Nodes**: 4 (IDs 0, 1, 2, 3) -/// - **Levels**: 2 (levels 0 and 1) to allow capacity-1 eviction on level 1 -/// - **Edges**: Deterministic setup to trigger eviction and deferred scrub -/// -/// # Scenario -/// -/// 1. Node 1 is seeded at capacity (1 edge) with node 2 at level 1 -/// 2. Node 0 adds node 1 as a neighbour at level 1 -/// 3. `ensure_reverse_edge(origin=0, target=1)` evicts node 2 from node 1 -/// 4. A `DeferredScrub { origin: 2, target: 1, level: 1 }` is created -/// 5. `apply_deferred_scrubs` removes the orphaned edge 2 → 1 -/// -/// # What This Proves -/// -/// If this harness passes, Kani has verified that: -/// - Eviction correctly removes the furthest neighbour -/// - Deferred scrubs correctly remove orphaned forward edges -/// - The bidirectional invariant is maintained throughout -#[kani::proof] -#[kani::unwind(10)] -fn verify_eviction_deferred_scrub_reciprocity() { - // Use max_connections = 1 so level 1 has capacity 1 and can evict. - let Ok(params) = HnswParams::new(1, 2) else { - kani::assert(false, "failed to construct eviction HNSW params"); - return; - }; - let max_connections = params.max_connections(); - let setup_result = setup_eviction_test_graph(params); - kani::assert( - setup_result.is_ok(), - "failed to construct eviction test graph", - ); - let Ok(mut graph) = setup_result else { - return; - }; - - // Seed node 1 at capacity with node 2 (bidirectional at level 1). - // This ensures node 1's level-1 neighbour list is full. - add_edge_if_missing(&mut graph, 1, 2, 1); - add_edge_if_missing(&mut graph, 2, 1, 1); - - // Update: node 0 adds node 1 as neighbour at level 1. - // When ensure_reverse_edge(origin=0, target=1) runs, node 1 is at - // capacity, so node 2 is evicted and a deferred scrub is created. - let update_ctx = EdgeContext { - level: 1, - max_connections, - }; - let staged = StagedUpdate { - node: 0, - ctx: update_ctx, - candidates: vec![1], - }; - let updates: Vec = vec![(staged, vec![1])]; - let new_node = NewNodeContext { id: 3, level: 1 }; - - let commit_result = - apply_commit_updates_for_kani(&mut graph, max_connections, new_node, updates); - kani::assert(commit_result.is_ok(), "commit-path updates must succeed"); - if commit_result.is_err() { - return; - } - - // Assert bidirectional invariant holds after eviction and deferred scrub. - kani::assert( - is_bidirectional(&graph), - "bidirectional invariant violated after eviction and deferred scrub", - ); - - // Assert node 1 links to node 0 (the new edge). - kani::assert( - has_node_link(&graph, EdgeAssertion::new(1, 0, 1)), - "node 1 should link to node 0 after eviction", - ); - - // Assert node 2's forward edge to node 1 was scrubbed. - kani::assert( - !has_node_link(&graph, EdgeAssertion::new(2, 1, 1)), - "deferred scrub should remove node 2's forward edge to node 1", - ); - - // Assert node 1 no longer links to node 2 (it was evicted). - kani::assert( - !has_node_link(&graph, EdgeAssertion::new(1, 2, 1)), - "node 1 should no longer link to node 2 after eviction", - ); -} diff --git a/chutoro-core/src/hnsw/kani_proofs/invariants.rs b/chutoro-core/src/hnsw/kani_proofs/invariants.rs index 956aed47..6e23bd2d 100644 --- a/chutoro-core/src/hnsw/kani_proofs/invariants.rs +++ b/chutoro-core/src/hnsw/kani_proofs/invariants.rs @@ -1,19 +1,22 @@ //! Invariant-model Kani harnesses for bounded HNSW graph state. -use std::collections::HashSet; - use crate::hnsw::{ graph::{Graph, NodeContext}, - insert::{KaniUpdateContext, apply_reconciled_update_for_kani}, + insert::{KaniUpdateContext, ensure_reverse_edge_for_kani, test_helpers::add_edge_if_missing}, invariants::has_no_self_loops, params::HnswParams, types::EntryPoint, }; -fn setup_four_node_graph(params: HnswParams) -> Option { - let mut graph = Graph::with_capacity(params, 4); +/// Builds the bounded two-node graph used by the invariant proofs. +/// +/// Both nodes expose levels 0 and 1, and construction is asserted +/// non-vacuous: nodes, level counts, and the entry point are checked +/// so a no-op constructor cannot satisfy the proofs trivially. +fn setup_two_node_graph(params: HnswParams) -> Option { + let mut graph = Graph::with_capacity(params, 2); if graph - .insert_first(NodeContext { + .insert_first_for_kani(NodeContext { node: 0, level: 1, sequence: 0, @@ -24,7 +27,7 @@ fn setup_four_node_graph(params: HnswParams) -> Option { return None; } if graph - .attach_node(NodeContext { + .attach_node_for_kani(NodeContext { node: 1, level: 1, sequence: 1, @@ -34,41 +37,39 @@ fn setup_four_node_graph(params: HnswParams) -> Option { kani::assert(false, "failed to attach node 1"); return None; } - if graph - .attach_node(NodeContext { - node: 2, - level: 0, - sequence: 2, - }) - .is_err() - { - kani::assert(false, "failed to attach node 2"); - return None; - } - if graph - .attach_node(NodeContext { - node: 3, - level: 0, - sequence: 3, - }) - .is_err() - { - kani::assert(false, "failed to attach node 3"); - return None; - } + + // Guard against vacuous proofs: a no-op constructor would leave the + // graph empty and every downstream invariant trivially satisfied. + kani::assert( + graph.node(0).is_some_and(|node| node.level_count() == 2), + "node 0 must exist with two levels after construction", + ); + kani::assert( + graph.node(1).is_some_and(|node| node.level_count() == 2), + "node 1 must exist with two levels after construction", + ); + kani::assert( + graph.entry().is_some_and(|entry| entry.node == 0), + "entry point must reference node 0 after construction", + ); Some(graph) } +/// Reports whether a neighbour list is free of duplicate entries. fn slice_has_no_duplicates(neighbours: &[usize]) -> bool { - let mut seen = HashSet::new(); - for &neighbour in neighbours { - if !seen.insert(neighbour) { - return false; + // A linear scan keeps the assertion path free of `HashSet`'s symbolic + // SipHash state, which is intractable under Kani. + for idx in 0..neighbours.len() { + for candidate in (idx + 1)..neighbours.len() { + if neighbours[idx] == neighbours[candidate] { + return false; + } } } true } +/// Reports whether every neighbour list at every level is duplicate-free. fn graph_neighbours_are_unique(graph: &Graph) -> bool { for (_node_id, node) in graph.nodes_iter() { for level in 0..node.level_count() { @@ -80,77 +81,73 @@ fn graph_neighbours_are_unique(graph: &Graph) -> bool { true } -fn symbolic_update_level() -> usize { - let level = kani::any::(); - kani::assume(level <= 1); - level -} - -fn bounded_level_one_node_for_kani() -> usize { - let node = kani::any::(); - kani::assume(node < 2); - node -} - -fn update_origin_for_level(level: usize) -> usize { - if level == 1 { - bounded_level_one_node_for_kani() - } else { - bounded_node_id_for_kani() - } -} - -fn upper_layer_peer(origin: usize) -> usize { - if origin == 0 { 1 } else { 0 } -} +/// Prepares the bounded two-node graph and update context shared by the +/// per-level reverse-edge proofs. +/// +/// Constructs bounded parameters, builds the two-node graph, seeds the +/// forward edge from node 0 to node 1 nondeterministically, and returns the +/// graph together with the origin's update context. Returns `None` when +/// construction fails, after asserting the failure. +/// +/// This helper is private to this module and serves the bounded two-node +/// Kani reconciliation proofs only. It must not become a general +/// graph-construction abstraction: widening it beyond two nodes, a concrete +/// level, or this seeding pattern would reintroduce the state-space growth +/// recorded in the developers' guide, "Kani CI policy". +fn setup_reverse_edge_proof(level: usize) -> Option<(Graph, KaniUpdateContext)> { + let Ok(params) = HnswParams::new_for_kani(2, 2) else { + kani::assert(false, "failed to construct bounded HNSW params"); + return None; + }; + let max_connections = params.max_connections(); + let mut graph = setup_two_node_graph(params)?; -fn deduped_targets(first: usize, second: usize) -> Vec { - let mut targets = vec![first, second]; - if first == second { - targets.pop(); + if kani::any::() { + add_edge_if_missing(&mut graph, 0, 1, level); } - targets + let ctx = KaniUpdateContext::new(0, level, max_connections); + Some((graph, ctx)) } /// Verifies that no node has itself as a neighbour (no self-loops). /// -/// This harness creates a bounded 4-node graph and nondeterministically adds -/// edges between distinct nodes. Since the edge addition helper never creates -/// self-loops, this verifies that the invariant holds for all possible edge -/// configurations. +/// This harness drives the production `EdgeReconciler::ensure_reverse_edge` +/// path on a bounded 2-node graph, with a nondeterministic choice of whether +/// the forward edge is seeded first, and asserts that no self-loop appears. +/// +/// The graph is bounded at two nodes and the level is a concrete argument: +/// the full reconciled-update helper and symbolic level indices push the +/// solver past the tractable CBMC state space (see the developers' guide, +/// "Kani CI policy"). Broader configurations are covered by the +/// graph-topology property suites. /// /// # Verification Bounds /// -/// - **Nodes**: 4 (IDs 0, 1, 2, 3) -/// - **Levels**: 2 (levels 0 and 1) -/// - **Edges**: Nondeterministic selection between distinct nodes +/// - **Nodes**: 2 (IDs 0, 1), both exposing levels 0 and 1 +/// - **Levels**: One concrete level per proof entry point +/// - **Edges**: Nondeterministic forward-edge seeding #[kani::proof] -#[kani::unwind(10)] -fn verify_no_self_loops_4_nodes() { - let Ok(params) = HnswParams::new(2, 2) else { - kani::assert(false, "failed to construct bounded HNSW params"); - return; - }; - let max_connections = params.max_connections(); - let Some(mut graph) = setup_four_node_graph(params) else { - return; - }; +#[kani::solver(kissat)] +#[kani::unwind(4)] +fn verify_no_self_loops_2_nodes_base_layer() { + check_no_self_loops_at_level(0); +} - let level = symbolic_update_level(); - let origin = update_origin_for_level(level); - let target = bounded_node_id_for_kani(); - let ctx = KaniUpdateContext::new(origin, level, max_connections); - let mut next = deduped_targets(target, upper_layer_peer(origin)); - apply_reconciled_update_for_kani(&mut graph, ctx, &mut next); +/// Level-1 sibling of [`verify_no_self_loops_2_nodes_base_layer`]. +#[kani::proof] +#[kani::solver(kissat)] +#[kani::unwind(4)] +fn verify_no_self_loops_2_nodes_upper_layer() { + check_no_self_loops_at_level(1); +} - if kani::any::() { - let second_level = symbolic_update_level(); - let second_origin = update_origin_for_level(second_level); - let second_target = bounded_node_id_for_kani(); - let second_ctx = KaniUpdateContext::new(second_origin, second_level, max_connections); - let mut second_next = deduped_targets(second_target, upper_layer_peer(second_origin)); - apply_reconciled_update_for_kani(&mut graph, second_ctx, &mut second_next); - } +/// Shared body for the per-level no-self-loop proofs. +fn check_no_self_loops_at_level(level: usize) { + let Some((mut graph, ctx)) = setup_reverse_edge_proof(level) else { + return; + }; + let added = ensure_reverse_edge_for_kani(&mut graph, ctx, 1); + kani::assert(added, "reverse edge must be ensured"); kani::assert( has_no_self_loops(&graph), @@ -160,36 +157,43 @@ fn verify_no_self_loops_4_nodes() { /// Verifies that neighbour lists contain no duplicates. /// -/// This harness drives the production reconciliation/write-back helper and -/// inspects the resulting graph adjacency rather than a separate model. +/// This harness drives `EdgeReconciler::ensure_reverse_edge` twice for the +/// same `(origin, target, level)` tuple, with nondeterministic forward-edge +/// seeding, and asserts that the repeated reconciliation never duplicates a +/// neighbour entry. +/// +/// The bounds are chosen for the same tractability reason as +/// [`verify_no_self_loops_2_nodes_base_layer`]. /// /// # Verification Bounds /// -/// - **Nodes**: 4 (IDs 0, 1, 2, 3) -/// - **Levels**: 2 (levels 0 and 1) -/// - **Updates**: Nondeterministic edge addition via reconciliation +/// - **Nodes**: 2 (IDs 0, 1), both exposing levels 0 and 1 +/// - **Levels**: One concrete level per proof entry point +/// - **Updates**: Two reconciliations of the same edge #[kani::proof] -#[kani::unwind(10)] -fn verify_neighbour_uniqueness_4_nodes() { - let Ok(params) = HnswParams::new(2, 2) else { - kani::assert(false, "failed to construct bounded HNSW params"); - return; - }; - let max_connections = params.max_connections(); - let Some(mut graph) = setup_four_node_graph(params) else { - return; - }; +#[kani::solver(kissat)] +#[kani::unwind(4)] +fn verify_neighbour_uniqueness_2_nodes_base_layer() { + check_neighbour_uniqueness_at_level(0); +} - let level = symbolic_update_level(); - let origin = update_origin_for_level(level); - let first_target = bounded_node_id_for_kani(); - let second_target = bounded_node_id_for_kani(); - let ctx = KaniUpdateContext::new(origin, level, max_connections); - let mut next = deduped_targets(first_target, upper_layer_peer(origin)); - apply_reconciled_update_for_kani(&mut graph, ctx, &mut next); +/// Level-1 sibling of [`verify_neighbour_uniqueness_2_nodes_base_layer`]. +#[kani::proof] +#[kani::solver(kissat)] +#[kani::unwind(4)] +fn verify_neighbour_uniqueness_2_nodes_upper_layer() { + check_neighbour_uniqueness_at_level(1); +} - let mut replacement = deduped_targets(second_target, upper_layer_peer(origin)); - apply_reconciled_update_for_kani(&mut graph, ctx, &mut replacement); +/// Shared body for the per-level neighbour-uniqueness proofs. +fn check_neighbour_uniqueness_at_level(level: usize) { + let Some((mut graph, ctx)) = setup_reverse_edge_proof(level) else { + return; + }; + let first = ensure_reverse_edge_for_kani(&mut graph, ctx, 1); + kani::assert(first, "first reconciliation must succeed"); + let second = ensure_reverse_edge_for_kani(&mut graph, ctx, 1); + kani::assert(second, "repeated reconciliation must succeed"); kani::assert( graph_neighbours_are_unique(&graph), @@ -197,12 +201,6 @@ fn verify_neighbour_uniqueness_4_nodes() { ); } -fn bounded_node_id_for_kani() -> usize { - let id: usize = kani::any(); - kani::assume(id < 4); - id -} - /// Verifies entry-point validity and maximality after insertions. /// /// This harness inserts nodes with nondeterministically chosen levels and @@ -222,6 +220,7 @@ fn bounded_node_id_for_kani() -> usize { /// - If the graph is non-empty, the entry point exists, references a valid /// node, and has a level at least as high as any other node in the graph. #[kani::proof] +#[kani::solver(kissat)] #[kani::unwind(12)] fn verify_entry_point_validity_4_nodes() { let levels = [ @@ -243,18 +242,21 @@ fn verify_entry_point_validity_4_nodes() { ); } +/// Draws a nondeterministic node level bounded to the proof domain. fn bounded_entry_level_for_kani() -> usize { let level: usize = kani::any(); kani::assume(level <= 2); level } +/// Applies the production entry-promotion rule to the model entry point. fn promote_entry_model_for_kani(entry: &mut EntryPoint, node: usize, level: usize) { if Graph::should_promote_entry_for_kani(Some(*entry), level) { *entry = EntryPoint { node, level }; } } +/// Reports whether the entry references a valid node at the maximum level. fn entry_is_valid_for_kani(entry: EntryPoint, levels: &[usize; 4]) -> bool { entry.node < levels.len() && entry.level == levels[entry.node] diff --git a/chutoro-core/src/hnsw/kani_proofs/mod.rs b/chutoro-core/src/hnsw/kani_proofs/mod.rs index b9a55b97..856c921f 100644 --- a/chutoro-core/src/hnsw/kani_proofs/mod.rs +++ b/chutoro-core/src/hnsw/kani_proofs/mod.rs @@ -9,7 +9,7 @@ //! # Running Harnesses //! //! ```bash -//! cargo kani -p chutoro-core --harness verify_bidirectional_links_commit_path_3_nodes +//! cargo kani -p chutoro-core --harness verify_bidirectional_links_smoke_2_nodes_1_layer //! ``` //! //! Or via the Makefile (practical harnesses): @@ -18,7 +18,7 @@ //! make kani //! ``` //! -//! Run the full suite (includes heavier 3-node harnesses): +//! Run the full suite (package-wide sweep): //! //! ```bash //! make kani-full @@ -33,35 +33,11 @@ //! verification strategy. mod bidirectional; -mod eviction; mod invariants; use crate::hnsw::{graph::Graph, insert::test_helpers::add_edge_if_missing}; -pub(super) struct EdgeAssertion { - source: usize, - target: usize, - level: usize, -} - -impl EdgeAssertion { - pub(super) fn new(source: usize, target: usize, level: usize) -> Self { - Self { - source, - target, - level, - } - } -} - -/// Returns `true` when source links to target at the given level. -pub(super) fn has_node_link(graph: &Graph, edge: EdgeAssertion) -> bool { - graph - .node(edge.source) - .map(|n| n.neighbours(edge.level).contains(&edge.target)) - .unwrap_or(false) -} - +/// Seeds a forward and reverse edge pair between two existing nodes. pub(super) fn add_bidirectional_edge( graph: &mut Graph, origin: usize, @@ -71,9 +47,3 @@ pub(super) fn add_bidirectional_edge( add_edge_if_missing(graph, origin, target, level); add_edge_if_missing(graph, target, origin, level); } - -pub(super) fn push_if_absent(list: &mut Vec, value: usize) { - if !list.contains(&value) { - list.push(value); - } -} diff --git a/chutoro-core/src/hnsw/params.rs b/chutoro-core/src/hnsw/params.rs index de28f9f5..ab57e12d 100644 --- a/chutoro-core/src/hnsw/params.rs +++ b/chutoro-core/src/hnsw/params.rs @@ -15,6 +15,27 @@ pub struct HnswParams { distance_cache: DistanceCacheConfig, } +/// Reasons parameter validation fails. +/// +/// Shared by the production and Kani constructors so both map the same +/// checks to their own error representations. +#[derive(Clone, Copy, Debug)] +enum ParamsError { + ZeroMaxConnections, + EfBelowMaxConnections, +} + +#[cfg(kani)] +impl ParamsError { + /// Returns the static reason used by the Kani constructor. + fn static_reason(self) -> &'static str { + match self { + Self::ZeroMaxConnections => "max_connections must be greater than zero", + Self::EfBelowMaxConnections => "ef_construction must be at least max_connections", + } + } +} + impl HnswParams { /// Creates a new parameter set with explicit neighbour and search widths. /// @@ -29,17 +50,42 @@ impl HnswParams { /// assert_eq!(params.max_connections(), 16); /// ``` pub fn new(max_connections: usize, ef_construction: usize) -> Result { - if max_connections == 0 { - return Err(HnswError::InvalidParameters { + Self::validate_and_build(max_connections, ef_construction).map_err(|reason| match reason { + ParamsError::ZeroMaxConnections => HnswError::InvalidParameters { reason: "max_connections must be greater than zero".into(), - }); - } - if ef_construction < max_connections { - return Err(HnswError::InvalidParameters { + }, + ParamsError::EfBelowMaxConnections => HnswError::InvalidParameters { reason: format!( "ef_construction ({ef_construction}) must be >= max_connections ({max_connections})" ), - }); + }, + }) + } + + /// Creates Kani parameters without constructing formatted production errors. + #[cfg(kani)] + pub(crate) fn new_for_kani( + max_connections: usize, + ef_construction: usize, + ) -> Result { + Self::validate_and_build(max_connections, ef_construction) + .map_err(ParamsError::static_reason) + } + + /// Validates the parameters and constructs the defaults. + /// + /// Shared by the production and Kani constructors; returns a static + /// reason so the Kani path never constructs formatted errors, and keeps + /// `max_level`, `rng_seed`, and `level_multiplier` defined once. + fn validate_and_build( + max_connections: usize, + ef_construction: usize, + ) -> Result { + if max_connections == 0 { + return Err(ParamsError::ZeroMaxConnections); + } + if ef_construction < max_connections { + return Err(ParamsError::EfBelowMaxConnections); } Ok(Self { max_connections, @@ -129,10 +175,14 @@ impl HnswParams { } impl Default for HnswParams { + /// Returns the documented default parameters of sixteen and sixty-four. fn default() -> Self { match Self::new(16, 64) { Ok(params) => params, - Err(err) => unreachable!("default parameters must be valid: {err}"), + // The reason is deliberately not bound: Kani rewrites + // `unreachable!` to discard its format arguments, which would + // leave the binding unused under `cfg(kani)` and `-D warnings`. + Err(_) => unreachable!("default parameters (16, 64) must be valid"), } } } diff --git a/chutoro-core/src/mst/kani_harness.rs b/chutoro-core/src/mst/kani_harness.rs index 6ee6b10a..13a892ad 100644 --- a/chutoro-core/src/mst/kani_harness.rs +++ b/chutoro-core/src/mst/kani_harness.rs @@ -1,4 +1,7 @@ -//! Kani harnesses for minimum-spanning-forest invariants. +//! Fast-tier Kani harnesses for minimum-spanning-forest invariants. +//! +//! Both harnesses run under `make kani` and the nightly `make kani-full` +//! package sweep. use super::*; @@ -18,32 +21,31 @@ fn validate_edges_canonical(edges: &[MstEdge]) -> bool { /// Validates MST forest structural invariants for Kani verification. /// /// Returns `true` if the forest satisfies: +/// - At most four nodes (the harness bound) /// - Edge count equals `n - c` where `n` is node count and `c` is component count -/// - No self-loops (source != target for all edges) -/// - Canonical ordering (source < target for all edges) +/// - No self-loops and canonical ordering (`source < target` for all edges) /// - Acyclic structure (no cycles detected via union-find) +/// +/// The enclosing module is compiled only under `cfg(kani)`, so no per-item +/// cfg gate is needed. pub(crate) fn is_valid_forest( node_count: usize, edges: &[MstEdge], component_count: usize, ) -> bool { - // Forest must have n - c edges - if edges.len() != node_count.saturating_sub(component_count) { + if node_count > 4 || edges.len() != node_count.saturating_sub(component_count) { return false; } - - // No self-loops and canonical ordering if !validate_edges_canonical(edges) { return false; } - // Acyclic check via union-find - let mut parent: Vec = (0..node_count).collect(); + let mut parent = [0, 1, 2, 3]; for edge in edges { let root_s = kani_find_root(&mut parent, edge.source()); let root_t = kani_find_root(&mut parent, edge.target()); if root_s == root_t { - return false; // Cycle detected + return false; } parent[root_t] = root_s; } @@ -78,29 +80,30 @@ mod kani_proofs { /// /// - **Nodes**: 4 (to keep solver time reasonable) /// - **Edges**: Up to 6 (complete graph on 4 nodes) - /// - **Weights**: Represented as u8 cast to f32 for finite guarantees + /// - **Weights**: A fixed finite representative, as weights do not affect + /// the structural invariants #[kani::proof] + #[kani::solver(kissat)] #[kani::unwind(12)] fn verify_mst_structural_correctness_4_nodes() { let node_count = 4usize; // Nondeterministically select edges from the complete graph // 4 nodes = 6 possible undirected edges - let edge_pairs = [(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)]; - - let mut edges = Vec::new(); - let mut seq = 0u64; - for &(source, target) in &edge_pairs { - if kani::any::() { - let weight: u8 = kani::any(); - edges.push(CandidateEdge::new(source, target, f32::from(weight), seq)); - seq = seq.saturating_add(1); - } - } + let edges = [ + selected_candidate(0, 1, 0, 0), + selected_candidate(0, 2, 0, 1), + selected_candidate(0, 3, 0, 2), + selected_candidate(1, 2, 0, 3), + selected_candidate(1, 3, 0, 4), + selected_candidate(2, 3, 0, 5), + ]; // With valid finite weights, parallel_kruskal_from_edges should not fail - let forest = parallel_kruskal_from_edges(node_count, edges.iter()) - .expect("MST computation should succeed for valid inputs"); + let Ok(forest) = parallel_kruskal_from_edges(node_count, edges.iter()) else { + kani::assert(false, "MST computation should succeed for valid inputs"); + return; + }; let mst_edges = forest.edges(); let component_count = forest.component_count(); @@ -127,33 +130,29 @@ mod kani_proofs { /// Verifies MST minimality property for bounded graphs. /// - /// This harness verifies that the MST includes minimum weight edges by - /// checking that the total weight is minimal. For a 3-node graph, if - /// all edges are present, the MST must exclude the heaviest edge that - /// would create a cycle. + /// This harness verifies that the forest is weight-minimal, not merely + /// structurally valid. It draws the edge selection explicitly, computes + /// the expected minimal spanning weight for that selection, and asserts + /// that the returned forest matches it. When the full triangle is + /// selected, this forces the heaviest edge (weight 2) to be excluded. #[kani::proof] + #[kani::solver(kissat)] #[kani::unwind(10)] fn verify_mst_minimality_3_nodes() { let node_count = 3usize; - let mut edges = Vec::new(); - - // Create edges with distinct weights to verify minimality - let weight0: u8 = kani::any(); - let weight1: u8 = kani::any(); - let weight2: u8 = kani::any(); - - if kani::any::() { - edges.push(CandidateEdge::new(0, 1, f32::from(weight0), 0)); - } - if kani::any::() { - edges.push(CandidateEdge::new(1, 2, f32::from(weight1), 1)); - } - if kani::any::() { - edges.push(CandidateEdge::new(0, 2, f32::from(weight2), 2)); - } - - let forest = parallel_kruskal_from_edges(node_count, edges.iter()) - .expect("MST computation should succeed for valid inputs"); + let select_01 = kani::any::(); + let select_12 = kani::any::(); + let select_02 = kani::any::(); + let edges = [ + candidate_or_self_loop(0, 1, 0, 0, select_01), + candidate_or_self_loop(1, 2, 1, 1, select_12), + candidate_or_self_loop(0, 2, 2, 2, select_02), + ]; + + let Ok(forest) = parallel_kruskal_from_edges(node_count, edges.iter()) else { + kani::assert(false, "MST computation should succeed for valid inputs"); + return; + }; let mst_edges = forest.edges(); @@ -171,5 +170,67 @@ mod kani_proofs { "connected MST should have n-1 edges", ); } + + // Verify minimality: the forest's total weight must equal the + // minimal spanning weight for the selected edge subset. Weights are + // small integers, so f32 summation is exact. + let total_weight: f32 = mst_edges.iter().map(|edge| edge.weight()).sum(); + let expected = expected_minimal_weight(select_01, select_12, select_02); + kani::assert( + total_weight == expected, + "MST total weight must be minimal for the selected edges", + ); + } + + /// Returns `true` when the weight-2 edge closes the triangle and must + /// therefore be excluded from the minimal spanning tree. + fn heavy_edge_is_redundant(select_01: bool, select_12: bool, select_02: bool) -> bool { + select_01 && select_12 && select_02 + } + + /// Returns the minimal spanning weight of the triangle subset where edge + /// (0,1) weighs 0, edge (1,2) weighs 1, and edge (0,2) weighs 2. + /// + /// Edge (0,1) contributes nothing to the total. Selected edges cannot + /// otherwise form a cycle, so the forest is exactly the selected edges + /// unless the heavy edge closes the triangle and is excluded. + fn expected_minimal_weight(select_01: bool, select_12: bool, select_02: bool) -> f32 { + let mut weight = 0.0; + if select_12 { + weight += 1.0; + } + if select_02 && !heavy_edge_is_redundant(select_01, select_12, select_02) { + weight += 2.0; + } + weight + } + + /// Builds an edge whose inclusion Kani chooses nondeterministically. + /// + /// A deselected edge degenerates to a self-loop, which validation + /// discards, so both branches stay within the bounded edge budget. + fn selected_candidate( + source: usize, + target: usize, + weight: u8, + sequence: u64, + ) -> CandidateEdge { + candidate_or_self_loop(source, target, weight, sequence, kani::any::()) + } + + /// Builds the edge when `selected`, or a same-weight self-loop (which + /// validation discards) when not. + fn candidate_or_self_loop( + source: usize, + target: usize, + weight: u8, + sequence: u64, + selected: bool, + ) -> CandidateEdge { + if selected { + CandidateEdge::new(source, target, f32::from(weight), sequence) + } else { + CandidateEdge::new(source, source, f32::from(weight), sequence) + } } } diff --git a/chutoro-core/src/mst/kani_model.rs b/chutoro-core/src/mst/kani_model.rs new file mode 100644 index 00000000..5a4eaf40 --- /dev/null +++ b/chutoro-core/src/mst/kani_model.rs @@ -0,0 +1,233 @@ +//! Sequential Kani model for parallel Kruskal execution. +//! +//! Kani models concurrency as sequential execution. This model preserves the +//! production algorithm's validated edge ordering and deterministic union +//! selection while omitting Rayon and synchronisation internals that do not +//! contribute to the forest invariants proved by the bounded harnesses. +//! It is compiled only for Kani harnesses and for the exhaustive +//! model-equivalence tests; production callers must not use it. + +use crate::CandidateEdge; + +#[cfg(kani)] +use super::MinimumSpanningForest; +use super::{MstEdge, MstError, validate_and_canonicalize_edge}; + +/// Placeholder edge used to initialise the bounded forest buffer. +const EMPTY_MST_EDGE: MstEdge = MstEdge { + source: 0, + target: 0, + weight: 0.0, + sequence: 0, +}; + +/// Bounded forest produced by the sequential Kani model. +/// +/// The representation is cfg-independent so the equivalence tests can compare +/// it directly against the production forest. +#[derive(Clone, Debug, PartialEq)] +pub(super) struct ModelForest { + edges: [MstEdge; 3], + edge_count: usize, + component_count: usize, +} + +impl ModelForest { + /// Returns the accepted forest edges in sorted order. + #[cfg(test)] + #[rustfmt::skip] + pub(super) fn edges(&self) -> &[MstEdge] { &self.edges[..self.edge_count] } + + /// Returns the number of connected components in the resulting forest. + #[cfg(test)] + #[rustfmt::skip] + pub(super) fn component_count(&self) -> usize { self.component_count } +} + +/// Computes the Kani-only sequential model of parallel Kruskal. +#[cfg(kani)] +pub(super) fn parallel_kruskal_from_edges_for_kani<'a>( + node_count: usize, + edges: impl IntoIterator, +) -> Result { + let forest = kruskal_model(node_count, edges)?; + Ok(MinimumSpanningForest { + edges: forest.edges, + edge_count: forest.edge_count, + component_count: forest.component_count, + }) +} + +/// Runs the bounded sequential Kruskal model shared by Kani and the +/// equivalence tests. +pub(super) fn kruskal_model<'a>( + node_count: usize, + edges: impl IntoIterator, +) -> Result { + if node_count == 0 { + return Err(MstError::EmptyGraph); + } + + if node_count > 4 { + return Err(MstError::InvariantViolation { + invariant: "Kani MST model supports at most four nodes", + index: node_count, + lock_count: 4, + }); + } + + let mut edge_list = [None; 6]; + let mut edge_count = 0; + for edge in edges { + if let Some(edge) = validate_and_canonicalize_edge(edge, node_count)? { + let Some(slot) = edge_list.get_mut(edge_count) else { + return Err(MstError::InvariantViolation { + invariant: "Kani MST model supports at most six edges", + index: edge_count, + lock_count: edge_list.len(), + }); + }; + *slot = Some(edge); + edge_count += 1; + } + } + sort_edges_for_kani(&mut edge_list, edge_count); + edge_count = deduplicate_edges_for_kani(&mut edge_list, edge_count); + + let mut parents = [0, 1, 2, 3]; + let mut ranks = [0; 4]; + let mut node = 0; + while node < node_count { + parents[node] = node; + node += 1; + } + let mut component_count = node_count; + let mut forest_edges = [EMPTY_MST_EDGE; 3]; + let mut forest_edge_count = 0; + + let mut index = 0; + while index < edge_count { + let Some(edge) = edge_list[index] else { + return Err(MstError::InvariantViolation { + invariant: "Kani MST edge buffer must be populated", + index, + lock_count: edge_count, + }); + }; + let source_root = find_root(&mut parents, edge.source); + let target_root = find_root(&mut parents, edge.target); + if source_root != target_root { + union_roots(&mut parents, &mut ranks, source_root, target_root); + component_count = component_count.saturating_sub(1); + forest_edges[forest_edge_count] = edge; + forest_edge_count += 1; + } + + if component_count == 1 && forest_edge_count == node_count.saturating_sub(1) { + break; + } + index += 1; + } + + sort_forest_edges_for_kani(&mut forest_edges, forest_edge_count); + Ok(ModelForest { + edges: forest_edges, + edge_count: forest_edge_count, + component_count, + }) +} + +/// Insertion-sorts the populated prefix of the bounded edge buffer. +fn sort_edges_for_kani(edges: &mut [Option], edge_count: usize) { + let mut index = 1; + while index < edge_count { + let mut current = index; + while current > 0 && should_swap_edges(edges, current) { + edges.swap(current, current - 1); + current -= 1; + } + index += 1; + } +} + +/// Compacts adjacent duplicates out of the sorted prefix. +/// +/// Returns the number of unique edges retained. +fn deduplicate_edges_for_kani(edges: &mut [Option], edge_count: usize) -> usize { + let mut unique_count = 0; + let mut index = 0; + while index < edge_count { + if let Some(edge) = edges[index] { + let is_duplicate = unique_count > 0 && duplicate_edges(edges[unique_count - 1], edge); + if !is_duplicate { + edges[unique_count] = Some(edge); + unique_count += 1; + } + } + index += 1; + } + unique_count +} + +/// Insertion-sorts the accepted forest edges into canonical order. +fn sort_forest_edges_for_kani(edges: &mut [MstEdge], edge_count: usize) { + let mut index = 1; + while index < edge_count { + let mut current = index; + while current > 0 && edges[current] < edges[current - 1] { + edges.swap(current, current - 1); + current -= 1; + } + index += 1; + } +} + +/// Reports whether adjacent populated slots are out of order. +/// +/// Pairs involving an empty slot never swap; the sorted prefix is fully +/// populated at the only call site, so that arm is defensive. +fn should_swap_edges(edges: &[Option], current: usize) -> bool { + match (edges[current], edges[current - 1]) { + (Some(current), Some(previous)) => current < previous, + _ => false, + } +} + +/// Reports whether two edges share weight and canonical endpoints. +fn duplicate_edges(left: Option, right: MstEdge) -> bool { + left.is_some_and(|left| { + left.weight == right.weight && left.source == right.source && left.target == right.target + }) +} + +/// Finds the union-find root of `node`, halving paths as it walks. +fn find_root(parents: &mut [usize; 4], node: usize) -> usize { + let mut current = node; + while parents[current] != current { + let parent = parents[current]; + let grandparent = parents[parent]; + if grandparent != parent { + parents[current] = grandparent; + } + current = parent; + } + current +} + +/// Unions two roots by rank, breaking ties towards the smaller id. +fn union_roots(parents: &mut [usize; 4], ranks: &mut [usize; 4], left: usize, right: usize) { + let (parent, child) = if ranks[left] > ranks[right] { + (left, right) + } else if ranks[right] > ranks[left] { + (right, left) + } else if left <= right { + (left, right) + } else { + (right, left) + }; + + parents[child] = parent; + if ranks[left] == ranks[right] { + ranks[parent] = ranks[parent].saturating_add(1); + } +} diff --git a/chutoro-core/src/mst/mod.rs b/chutoro-core/src/mst/mod.rs index aca1ad61..00eeb965 100644 --- a/chutoro-core/src/mst/mod.rs +++ b/chutoro-core/src/mst/mod.rs @@ -4,14 +4,20 @@ //! backends. The algorithm parallelizes the global edge sort via Rayon and //! performs concurrent cycle checks using a striped-lock union-find. +#[cfg(not(kani))] mod union_find; +#[cfg(any(kani, test))] +mod kani_model; + use std::cmp::Ordering; +#[cfg(not(kani))] use rayon::prelude::*; use crate::{CandidateEdge, EdgeHarvest}; +#[cfg(not(kani))] use self::union_find::ConcurrentUnionFind; /// Errors returned while computing a minimum spanning tree/forest. @@ -150,18 +156,39 @@ impl PartialOrd for MstEdge { /// The output of a minimum spanning forest computation. /// /// When the input graph is connected, the forest is a minimum spanning tree. +#[cfg(not(kani))] #[derive(Clone, Debug, PartialEq)] pub struct MinimumSpanningForest { edges: Vec, component_count: usize, } +/// Bounded Kani representation of a minimum spanning forest. +/// +/// The Kani harnesses exercise at most four nodes, so the forest has at most +/// three edges. Keeping that representation inline avoids modelling allocator +/// and panic paths that are unrelated to forest invariants. +#[cfg(kani)] +#[derive(Clone, Debug, PartialEq)] +pub struct MinimumSpanningForest { + edges: [MstEdge; 3], + edge_count: usize, + component_count: usize, +} + impl MinimumSpanningForest { /// Returns the MST/forest edges. #[must_use] #[rustfmt::skip] + #[cfg(not(kani))] pub fn edges(&self) -> &[MstEdge] { &self.edges } + /// Returns the MST/forest edges in the Kani bounded model. + #[must_use] + #[rustfmt::skip] + #[cfg(kani)] + pub fn edges(&self) -> &[MstEdge] { &self.edges[..self.edge_count] } + /// Returns the number of connected components in the resulting forest. #[must_use] #[rustfmt::skip] @@ -238,6 +265,7 @@ fn validate_and_canonicalize_edge( })) } +#[cfg(not(kani))] fn process_weight_group( group: &[MstEdge], union_find: &ConcurrentUnionFind, @@ -254,6 +282,7 @@ fn process_weight_group( Ok(accepted) } +#[cfg(not(kani))] fn is_mst_complete( node_count: usize, union_find: &ConcurrentUnionFind, @@ -262,6 +291,7 @@ fn is_mst_complete( union_find.components() == 1 && forest_edges.len() == node_count.saturating_sub(1) } +#[cfg(not(kani))] fn prepare_edge_list<'a>( edges: impl IntoIterator, node_count: usize, @@ -291,47 +321,55 @@ pub(crate) fn parallel_kruskal_from_edges<'a>( node_count: usize, edges: impl IntoIterator, ) -> Result { - if node_count == 0 { - return Err(MstError::EmptyGraph); + #[cfg(kani)] + { + return kani_model::parallel_kruskal_from_edges_for_kani(node_count, edges); } - let edge_list = prepare_edge_list(edges, node_count)?; - - if edge_list.is_empty() { - return Ok(MinimumSpanningForest { - edges: Vec::new(), - component_count: node_count, - }); - } + #[cfg(not(kani))] + { + if node_count == 0 { + return Err(MstError::EmptyGraph); + } - let union_find = ConcurrentUnionFind::new(node_count); - let mut forest_edges = Vec::with_capacity(node_count.saturating_sub(1)); + let edge_list = prepare_edge_list(edges, node_count)?; - let mut cursor = 0; - while cursor < edge_list.len() { - let weight = edge_list[cursor].weight; - let mut next = cursor.saturating_add(1); - while next < edge_list.len() && edge_list[next].weight == weight { - next = next.saturating_add(1); + if edge_list.is_empty() { + return Ok(MinimumSpanningForest { + edges: Vec::new(), + component_count: node_count, + }); } - let group = &edge_list[cursor..next]; - let accepted = process_weight_group(group, &union_find)?; + let union_find = ConcurrentUnionFind::new(node_count); + let mut forest_edges = Vec::with_capacity(node_count.saturating_sub(1)); + + let mut cursor = 0; + while cursor < edge_list.len() { + let weight = edge_list[cursor].weight; + let mut next = cursor.saturating_add(1); + while next < edge_list.len() && edge_list[next].weight == weight { + next = next.saturating_add(1); + } - forest_edges.extend(accepted); + let group = &edge_list[cursor..next]; + let accepted = process_weight_group(group, &union_find)?; - if is_mst_complete(node_count, &union_find, &forest_edges) { - break; + forest_edges.extend(accepted); + + if is_mst_complete(node_count, &union_find, &forest_edges) { + break; + } + + cursor = next; } - cursor = next; + forest_edges.sort_unstable(); + Ok(MinimumSpanningForest { + edges: forest_edges, + component_count: union_find.components(), + }) } - - forest_edges.sort_unstable(); - Ok(MinimumSpanningForest { - edges: forest_edges, - component_count: union_find.components(), - }) } #[cfg(kani)] diff --git a/chutoro-core/src/mst/tests/kani_model_equivalence.rs b/chutoro-core/src/mst/tests/kani_model_equivalence.rs new file mode 100644 index 00000000..92d67827 --- /dev/null +++ b/chutoro-core/src/mst/tests/kani_model_equivalence.rs @@ -0,0 +1,272 @@ +//! Exhaustive equivalence tests for the sequential Kani MST model. +//! +//! The Kani harnesses verify `kani_model::kruskal_model` rather than the +//! Rayon-based production path, so the model is a modelling boundary. These +//! tests close that boundary by enumerating every edge subset of the complete +//! graph on one to four nodes, under several weight assignments and both +//! subset encodings used by the harnesses, and asserting that the model and +//! the production implementation produce identical forests. + +use rstest::rstest; + +use crate::CandidateEdge; + +use super::super::kani_model::kruskal_model; +use super::super::{MstError, parallel_kruskal_from_edges}; + +/// How deselected complete-graph edges are represented in the input. +#[derive(Clone, Copy, Debug)] +enum DeselectedEdge { + /// The edge is omitted from the input entirely. + Omitted, + /// The edge degenerates to a self-loop, mirroring the harness encoding. + SelfLoop, +} + +/// Weight assignment applied to the complete-graph edge at `index`. +#[derive(Clone, Copy, Debug)] +enum WeightScheme { + AllEqual, + Ascending, + Descending, + PairedDuplicates, +} + +impl WeightScheme { + /// Returns the weight this scheme assigns to the edge at `index`. + fn weight(self, index: usize, edge_total: usize) -> f32 { + #[expect( + clippy::cast_precision_loss, + reason = "edge indices are at most six, far below f32 precision limits" + )] + match self { + Self::AllEqual => 1.0, + Self::Ascending => index as f32, + Self::Descending => (edge_total - index) as f32, + Self::PairedDuplicates => (index / 2) as f32, + } + } +} + +/// Returns the complete-graph edge list for `node_count` nodes. +fn complete_graph_pairs(node_count: usize) -> Vec<(usize, usize)> { + let mut pairs = Vec::new(); + for source in 0..node_count { + for target in (source + 1)..node_count { + pairs.push((source, target)); + } + } + pairs +} + +/// Builds the candidate edges for one subset mask of the complete graph. +fn build_candidates( + pairs: &[(usize, usize)], + mask: usize, + scheme: WeightScheme, + deselected: DeselectedEdge, +) -> Vec { + let mut candidates = Vec::new(); + for (index, &(source, target)) in pairs.iter().enumerate() { + let selected = mask & (1 << index) != 0; + let weight = scheme.weight(index, pairs.len()); + let sequence = index as u64; + if selected { + candidates.push(CandidateEdge::new(source, target, weight, sequence)); + } else if matches!(deselected, DeselectedEdge::SelfLoop) { + candidates.push(CandidateEdge::new(source, source, weight, sequence)); + } + } + candidates +} + +/// Compares the model and production forests for one input, returning a +/// description of the first divergence. +fn check_equivalence(node_count: usize, candidates: &[CandidateEdge]) -> Result<(), String> { + let production = parallel_kruskal_from_edges(node_count, candidates.iter()) + .map_err(|error| format!("production Kruskal failed: {error}"))?; + let model = kruskal_model(node_count, candidates.iter()) + .map_err(|error| format!("Kani model failed: {error}"))?; + + if model.edges() != production.edges() { + return Err(format!( + "edge mismatch for nodes={node_count}, input={candidates:?}: \ + model={:?}, production={:?}", + model.edges(), + production.edges(), + )); + } + if model.component_count() != production.component_count() { + return Err(format!( + "component mismatch for nodes={node_count}, input={candidates:?}: \ + model={}, production={}", + model.component_count(), + production.component_count(), + )); + } + Ok(()) +} + +#[rstest] +#[case::omitted(DeselectedEdge::Omitted)] +#[case::self_loop(DeselectedEdge::SelfLoop)] +/// Sweeps every edge subset of one-to-four-node complete graphs. +/// +/// Each subset runs under every weight scheme and the given deselected +/// edge encoding; model and production must agree exactly. +fn model_matches_production_for_all_bounded_graphs(#[case] deselected: DeselectedEdge) { + let schemes = [ + WeightScheme::AllEqual, + WeightScheme::Ascending, + WeightScheme::Descending, + WeightScheme::PairedDuplicates, + ]; + + for node_count in 1..=4 { + let pairs = complete_graph_pairs(node_count); + for scheme in schemes { + for mask in 0..(1usize << pairs.len()) { + let candidates = build_candidates(&pairs, mask, scheme, deselected); + if let Err(divergence) = check_equivalence(node_count, &candidates) { + panic!("{divergence}"); + } + } + } + } +} + +#[rstest] +#[case::empty_graph(0, vec![], MstError::EmptyGraph)] +#[case::invalid_source( + 2, + vec![CandidateEdge::new(5, 1, 1.0, 0)], + MstError::InvalidNodeId { node: 5, node_count: 2 }, +)] +#[case::invalid_target( + 2, + vec![CandidateEdge::new(0, 7, 1.0, 0)], + MstError::InvalidNodeId { node: 7, node_count: 2 }, +)] +#[case::non_finite_weight( + 2, + vec![CandidateEdge::new(0, 1, f32::NAN, 0)], + MstError::NonFiniteWeight { left: 0, right: 1 }, +)] +/// Asserts the model rejects invalid inputs with production's errors. +fn model_matches_production_errors( + #[case] node_count: usize, + #[case] candidates: Vec, + #[case] expected: MstError, +) { + let production = parallel_kruskal_from_edges(node_count, candidates.iter()); + let model = kruskal_model(node_count, candidates.iter()); + + assert_eq!( + production.expect_err("production must reject input"), + expected + ); + assert_eq!(model.expect_err("model must reject input"), expected); +} + +/// Exercises the deduplication path, which the complete-graph sweep above +/// cannot reach because it emits each undirected pair at most once. +/// +/// Duplicates are in-domain: the model's six-edge budget counts canonical +/// edges before deduplication, so a caller may legitimately supply repeats. +/// Deduplication interacts with the `(weight, source, target, sequence)` +/// ordering, which is where a divergence would hide. +#[rstest] +#[case::identical_repeat( + 3, + vec![ + CandidateEdge::new(0, 1, 1.0, 0), + CandidateEdge::new(0, 1, 1.0, 0), + CandidateEdge::new(1, 2, 2.0, 1), + ], +)] +#[case::same_edge_differing_sequence( + 3, + vec![ + CandidateEdge::new(0, 1, 1.0, 5), + CandidateEdge::new(0, 1, 1.0, 2), + CandidateEdge::new(1, 2, 2.0, 1), + ], +)] +#[case::reversed_orientation_then_duplicate( + 3, + vec![ + CandidateEdge::new(1, 0, 1.0, 0), + CandidateEdge::new(0, 1, 1.0, 0), + CandidateEdge::new(1, 2, 2.0, 1), + ], +)] +#[case::same_pair_differing_weights_must_not_dedupe( + 3, + vec![ + CandidateEdge::new(0, 1, 1.0, 0), + CandidateEdge::new(0, 1, 3.0, 1), + CandidateEdge::new(1, 2, 2.0, 2), + ], +)] +#[case::duplicates_at_the_six_edge_budget( + 4, + vec![ + CandidateEdge::new(0, 1, 1.0, 0), + CandidateEdge::new(0, 1, 1.0, 0), + CandidateEdge::new(1, 2, 2.0, 1), + CandidateEdge::new(2, 3, 3.0, 2), + CandidateEdge::new(0, 3, 4.0, 3), + CandidateEdge::new(1, 3, 5.0, 4), + ], +)] +fn model_matches_production_for_duplicate_edges( + #[case] node_count: usize, + #[case] candidates: Vec, +) { + if let Err(divergence) = check_equivalence(node_count, &candidates) { + panic!("{divergence}"); + } +} + +/// Pins the model's bounded domain, where it deliberately diverges. +/// +/// Beyond four nodes or six canonical edges the model reports an invariant +/// violation while production succeeds. That is the modelling contract, not +/// a defect: widening a harness past these bounds must fail loudly rather +/// than silently verify a truncated graph. +#[rstest] +#[case::seven_canonical_edges( + 4, + vec![ + CandidateEdge::new(0, 1, 1.0, 0), + CandidateEdge::new(0, 2, 2.0, 1), + CandidateEdge::new(0, 3, 3.0, 2), + CandidateEdge::new(1, 2, 4.0, 3), + CandidateEdge::new(1, 3, 5.0, 4), + CandidateEdge::new(2, 3, 6.0, 5), + CandidateEdge::new(0, 1, 9.0, 6), + ], + "Kani MST model supports at most six edges", +)] +#[case::five_nodes( + 5, + vec![CandidateEdge::new(0, 4, 1.0, 0)], + "Kani MST model supports at most four nodes", +)] +fn model_rejects_inputs_outside_its_bounded_domain( + #[case] node_count: usize, + #[case] candidates: Vec, + #[case] expected_invariant: &str, +) { + assert!( + parallel_kruskal_from_edges(node_count, candidates.iter()).is_ok(), + "production must accept this input; only the bounded model rejects it", + ); + + let error = kruskal_model(node_count, candidates.iter()) + .expect_err("the model must reject input outside its bounded domain"); + let MstError::InvariantViolation { invariant, .. } = error else { + panic!("expected an invariant violation, got {error:?}"); + }; + assert_eq!(invariant, expected_invariant); +} diff --git a/chutoro-core/src/mst/tests/mod.rs b/chutoro-core/src/mst/tests/mod.rs index e2ce7f1d..9add34aa 100644 --- a/chutoro-core/src/mst/tests/mod.rs +++ b/chutoro-core/src/mst/tests/mod.rs @@ -151,3 +151,4 @@ fn undirected_edges_are_canonicalized_and_deduplicated() { } mod forests; +mod kani_model_equivalence; diff --git a/docs/adr-002-adoption-of-kani-formal-verification.md b/docs/adr-002-adoption-of-kani-formal-verification.md index 2ecdd5da..300caac2 100644 --- a/docs/adr-002-adoption-of-kani-formal-verification.md +++ b/docs/adr-002-adoption-of-kani-formal-verification.md @@ -220,6 +220,27 @@ demonstrates: - Added explicit `kani::assume` preconditions in the commit-path helper to align with production invariants and keep Kani runtimes manageable. +### 2026-08-24: Tractability Restructure and CI Gating + +- Hand-tracing the three-node reconciliation harness exposed a production + ordering defect (healing clobbered by the origin's write-back); the fix and + the retirement of the intractable deterministic harnesses are recorded in + [kani-full-hnsw-hypothesis-testing.md](./kani-full-hnsw-hypothesis-testing.md) + and the developers' guide "Kani CI policy" section. +- The commit-path, three-node reconciliation, and eviction-scrub harnesses + exceeded practical CBMC budgets and are replaced by exact unit-test twins; + the no-self-loop and neighbour-uniqueness invariants are now proved on the + `ensure_reverse_edge` surface with per-level two-node harnesses. +- `make kani` gates pull requests via the path-filtered `kani-pr.yml` + workflow, and `make kani-full` (17 harnesses, roughly 18 minutes) runs + nightly post-merge. +- MST proofs verify a bounded `cfg(kani)` sequential model of parallel + Kruskal (at most four nodes, six canonical edges, fixed-size forest + representation) rather than the Rayon production path; the modelling + boundary is closed by exhaustive equivalence tests in + `chutoro-core/src/mst/tests/kani_model_equivalence.rs`, and + out-of-domain inputs fail loudly with invariant violations. + ### Verification Targets (Next Invariants) The following invariants are explicitly defined to avoid ambiguity, and are @@ -284,6 +305,12 @@ intended as future formal verification targets: - 2025-12-27: Recorded audit recommendations, added explicit verification targets (five additional invariants), and clarified the plan for a nightly "slow" Kani CI job while keeping normal test runs unchanged. +- 2026-08-24: Retired harnesses past the CBMC tractability cliff in favour of + unit-test twins and narrow-surface proofs, fixed the reconciliation + write-back ordering defect the investigation exposed, and wired `make kani` + into pull-request CI with `make kani-full` remaining the nightly tier. +- 2026-08-24: Documented the MST Kani model boundary and its equivalence-test + closure in the design document and this ADR. ## References diff --git a/docs/chutoro-design.md b/docs/chutoro-design.md index bed6ff05..81010e45 100644 --- a/docs/chutoro-design.md +++ b/docs/chutoro-design.md @@ -1262,44 +1262,59 @@ nodes) while preserving the previous short-circuit behaviour for fail-fast callers. The formal verification harnesses extend these guarantees by exercising the -commit path under bounded conditions, ensuring reconciliation and deferred -scrubs still satisfy the bidirectional edge invariant. The sequence below -illustrates the commit-path harness flow used by Kani. +production reconciliation entry points under bounded conditions. Multi-node +harnesses that drove the whole commit sequence (trimmed write-back, reverse +edge reconciliation, and deferred scrubs) in one formula proved intractable +for the Bounded Model Checker for C (CBMC) and were retired in favour of +exact unit-test twins in `chutoro-core/src/hnsw/insert/commit/tests/`; the +investigation and the resulting tractability policy are recorded in +[the hypothesis document](./kani-full-hnsw-hypothesis-testing.md) and the +developers' guide "Kani CI policy" section. The remaining Kani proofs drive +`EdgeReconciler::ensure_reverse_edge` directly on two-node graphs, as the +sequence below illustrates. ```mermaid sequenceDiagram actor KaniVerifier participant KaniHarness participant HnswGraph - participant KaniCommitHelper - participant CommitApplicator - participant DeferredScrubLogic + participant KaniReverseEdgeHelper + participant EdgeReconciler participant Invariants - KaniVerifier->>KaniHarness: run_commit_path_harness - KaniHarness->>HnswGraph: build_3_node_single_layer_graph - KaniHarness->>HnswGraph: seed_neighbour_lists_with_eviction_case + KaniVerifier->>KaniHarness: run_reverse_edge_harness + KaniHarness->>HnswGraph: build_2_node_graph_via_lean_constructors + KaniHarness->>HnswGraph: nondeterministically_seed_forward_edge - KaniHarness->>KaniCommitHelper: apply_commit_updates_for_kani(graph, update_specs) - KaniCommitHelper->>KaniCommitHelper: kani_assume_preconditions(graph, update_specs) - KaniCommitHelper->>CommitApplicator: apply_neighbour_updates(final_updates, max_connections, new_node) + KaniHarness->>KaniReverseEdgeHelper: ensure_reverse_edge_for_kani(graph, ctx, target) + KaniReverseEdgeHelper->>KaniReverseEdgeHelper: kani_assume_preconditions(graph, ctx, target) + KaniReverseEdgeHelper->>EdgeReconciler: ensure_reverse_edge(ctx, target) + EdgeReconciler->>HnswGraph: insert_or_confirm_reverse_edge - CommitApplicator->>HnswGraph: apply_trimmed_neighbour_lists - CommitApplicator->>HnswGraph: reconcile_reverse_edges - CommitApplicator->>DeferredScrubLogic: schedule_deferred_scrubs - DeferredScrubLogic->>HnswGraph: remove_one_way_edges + EdgeReconciler-->>KaniReverseEdgeHelper: bool + KaniReverseEdgeHelper-->>KaniHarness: bool - CommitApplicator-->>KaniCommitHelper: Result - KaniCommitHelper-->>KaniHarness: Result - - KaniHarness->>Invariants: is_bidirectional(graph) + KaniHarness->>Invariants: is_bidirectional / has_no_self_loops / neighbours_are_unique Invariants-->>KaniHarness: bool KaniHarness-->>KaniVerifier: assert_invariant_holds ``` -_Figure 2: Commit-path Kani harness flow for bidirectional invariant checks, -using a bounded three-node scenario (the implementation uses level 1 to -exercise eviction and deferred scrubs)._ +_Figure 2: Reverse-edge Kani harness flow for the bidirectional, no-self-loop, +and neighbour-uniqueness invariant checks, using bounded two-node scenarios +with one concrete level per proof entry point._ + +Minimum spanning tree (MST) proofs verify a bounded sequential model of +the parallel Kruskal implementation, compiled only under `cfg(kani)`, +because the Bounded Model Checker for C (CBMC) cannot absorb the Rayon +and concurrent union-find machinery. The model is bounded at four nodes +and six canonical edges, represents the forest as a fixed `[MstEdge; 3]` +array in place of production's growable vector, and preserves the +production edge ordering, deduplication, and deterministic union +selection. Inputs outside those bounds fail with an invariant violation +rather than silently truncating. The model's fidelity to production is +pinned by exhaustive equivalence tests over every edge subset of one- to +four-node complete graphs +(`chutoro-core/src/mst/tests/kani_model_equivalence.rs`). _Implementation update (2026-01-17)._ A nightly slow CI job runs `make kani-full` only when the `main` branch has a commit within the last 24 @@ -1309,6 +1324,11 @@ PR CI path remains unchanged so formal verification stays opt-in for daily development loops. Small future timestamp skews (up to 300 seconds) are treated as skips rather than failures to avoid false negatives from clock drift. +_Implementation update (2026-08-24)._ Formal verification is no longer +opt-in for pull requests: the path-filtered `kani-pr.yml` workflow runs +`make kani` whenever Kani harnesses, the modules under proof, the Makefile, +or the Cargo manifests change. The nightly `kani-full` sweep is unchanged. + _Implementation update (2026-02-02)._ Verus proofs now cover the edge harvest primitives described in `docs/property-testing-design.md` Appendix A. The proofs live in `verus/edge_harvest_proofs.rs` and model diff --git a/docs/developers-guide.md b/docs/developers-guide.md index ae05541e..55af5e11 100644 --- a/docs/developers-guide.md +++ b/docs/developers-guide.md @@ -427,6 +427,84 @@ selection: `chutoro-providers-dense`. Keep new dense harnesses small enough for `make kani` unless they are intentionally slow-lane proofs. +## Kani CI policy + +`make kani` is the pull-request gate. The path-filtered +`.github/workflows/kani-pr.yml` workflow runs it when Kani harnesses, their +production modules, the Makefile, or the Cargo dependency graph changes. + +`make kani-full` is the post-merge nightly tier. The +`.github/workflows/nightly-kani.yml` workflow checks out `main` and runs the +full suite only when its commit-recency gate permits it. + +### Installing Kani + +CI and local runs use the kani-verifier release pinned in +`tools/kani/VERSION`, which is the single source of truth for the version. +`prover-tools kani install` reads that file by default; install it directly +with: + +```sh +cargo install --locked kani-verifier --version "$(cat tools/kani/VERSION)" +cargo kani setup +``` + +The Makefile derives `KANI_VERSION` from the same file, the `kani-pr.yml` +workflow interpolates it rather than restating it, and a workflow contract +test fails the build if a version literal reappears in the workflow. +Bumping Kani is therefore a one-line change to `tools/kani/VERSION`. + +The two minimum-spanning-tree (MST) harnesses are fast-tier proofs and run in +`make kani`. The full tier remains the package-wide sweep across every +declared harness, including the distance and HNSW invariant proofs that are +not in the fast list. + +Kani harnesses must stay within the tractable CBMC state space. For graph +code there is a sharp combinatorial cliff between two-node and three-node +configurations that drive the full commit machinery: three deterministic +multi-node harnesses (three-node reconciliation, three-node commit path, and +four-node eviction scrub) each exceeded 15 to 20 minutes without concluding +and were retired. A deterministic harness explores a single concrete path, so +its value over a unit test is only the absence of undefined behaviour along +that path; each retired harness is replaced by an exact unit-test twin in +`chutoro-core/src/hnsw/insert/commit/tests/deferred_scrub.rs` and +`.../commit/tests/mod.rs`. Reserve Kani proofs for small nondeterministic +state spaces where exhaustive exploration adds coverage a test cannot. + +Two further tractability rules follow from the same investigation. Keep +symbolic values out of index positions: a symbolic node id or level index +multiplies solver aliasing through every `node_mut` and `neighbours(level)` +access, so fix the origin and split per-level proof entry points with a +concrete level argument instead. Keep each proof on a narrow production +surface: a helper that chains added-edge reconciliation, write-back, +removed-edge reconciliation, and deferred scrubs in one formula was +intractable even on a two-node graph, while per-call proofs of +`ensure_reverse_edge` verify in about a minute. + +Harness construction must avoid panic-capable paths such as `.expect(...)` and +production errors that build messages with `format!` before an invariant +assertion. Prefer +`let Ok(value) = operation else { kani::assert(false, "..."); return; };` and +lean `#[cfg(kani)]` constructors that return static reasons. + +Where production code relies on concurrency that Kani models sequentially, a +`#[cfg(kani)]` model must preserve the production ordering and selection +semantics while omitting only unsupported runtime machinery. Every such model +must be backed by exhaustive finite-state equivalence tests against the +production implementation over the model's full bounded input domain; see +`chutoro-core/src/mst/tests/kani_model_equivalence.rs`. + +Standard hash collections must not appear on any Kani-reachable path. The +default `HashMap`/`HashSet` hasher seeds symbolic SipHash state that makes even +fully deterministic harnesses intractable. Substitute a bounded linear-scan +structure under `#[cfg(kani)]`, as `ConnectivityHealer`'s visited set does in +`chutoro-core/src/hnsw/insert/connectivity.rs`. + +Keep each `#[kani::unwind(N)]` bound as tight as the harness permits; do not +increase a default bound to compensate for proof cost. For a demonstrably slow +full-tier harness, benchmark `#[kani::solver(kissat)]` or +`#[kani::solver(cadical)]` and retain the faster verified configuration. + ## Benchmarks The `chutoro-benches` crate provides Criterion benchmarks for the four CPU diff --git a/docs/kani-full-hnsw-hypothesis-testing.md b/docs/kani-full-hnsw-hypothesis-testing.md index 783821bf..6179b43e 100644 --- a/docs/kani-full-hnsw-hypothesis-testing.md +++ b/docs/kani-full-hnsw-hypothesis-testing.md @@ -254,12 +254,59 @@ conditions. ## Current conclusion -The likely immediate blocker is the HNSW `verify_entry_point_validity_4_nodes` -full-tier harness. The dense SIMD 2.2.7 harnesses are not the direct cause, and -the run does not appear to be blocked by obvious resource contention. The -strongest surviving theory is that the HNSW harness construction leaves -panic-capable paths available to Kani, causing CBMC to spend the budget in Rust -`core::str` panic and slice-error formatting. +`verify_entry_point_validity_4_nodes` is panic-free in the current split-module +layout. With the `kissat` solver it verifies 63 checks in 0.17 seconds. The +surviving formatting cost came from sibling harnesses that reached +`format!`-based production error paths during graph and parameter construction. + +Phase 1 replaced those construction paths with `#[cfg(kani)]` lean constructors +returning static error reasons, and replaced harness `.expect(...)` calls with +Kani assertions and early returns. + +The residual non-completion had three further causes, all resolved: + +1. **Symbolic hashing in connectivity healing.** `ConnectivityHealer` tracked + visited nodes with `std::collections::HashSet`, whose randomized SipHash + seed is symbolic under Kani. The three-node reconciliation harness is the + only harness reaching the healer (via base-layer isolation), which made it + intractable while the two-node harness stayed fast. The healer now uses a + bounded linear-scan visited set under `#[cfg(kani)]`. + +2. **Deterministic multi-node harnesses past the CBMC cliff.** Even after the + hashing fix, `verify_bidirectional_links_reconciliation_3_nodes_1_layer` + exceeded 20 minutes in symbolic execution, and + `verify_bidirectional_links_commit_path_3_nodes` exceeded a 15-minute + budget while solving. These harnesses were fully deterministic (no + `kani::any`), so their value over a unit test was only the absence of + undefined behaviour along one concrete path. Hand-tracing the three-node + reconciliation harness exposed a genuine production 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. The commit path now + writes the origin's list back before removed-edge reconciliation, and a + deterministic regression test + (`isolation_replacement_keeps_bidirectionality`) pins the fix. The three + deterministic heavy harnesses (three-node reconciliation, three-node + commit path, four-node eviction scrub) are retired in favour of exact + unit-test twins in `chutoro-core/src/hnsw/insert/commit/tests/`. + +3. **The full reconciled-update helper is intractable at any bound.** The + no-self-loop and neighbour-uniqueness harnesses drove + `apply_reconciled_update_for_kani`, which chains added-edge + reconciliation, write-back, removed-edge reconciliation (including the + base-layer healing cascade), and deferred scrubs in one formula. The + harnesses timed out at 20 minutes even on a two-node graph with a + concrete origin and concrete level. The helper was removed and both + invariants are now proved on the `ensure_reverse_edge` surface: per-level + two-node proofs with nondeterministic edge seeding + (`verify_no_self_loops_2_nodes_base_layer` and siblings), which verify in + 18 to 66 seconds each. Broader configurations remain covered by the + graph-topology property suites. + +The investigation is resolved. `make kani-full` completes: all 17 harnesses +across `chutoro-core` and `chutoro-providers-dense` verify successfully in +17 minutes 50 seconds of wall-clock time (including Kani compilation) on a +six-core development machine, well within the nightly 120-minute budget. ## Notes for executing agent diff --git a/docs/users-guide.md b/docs/users-guide.md index b44b6bfd..42b16021 100644 --- a/docs/users-guide.md +++ b/docs/users-guide.md @@ -211,6 +211,17 @@ implement `DataSource + Sync`, matching the requirement for parallel insertion. For an end-to-end example, see the Rustdoc for `chutoro_core::CpuHnsw::insert_harvesting`. +### Insertion guarantees + +Insertion maintains reciprocal links: every neighbour edge the index +stores has a matching reverse edge at the same layer, and a point whose +last base-layer neighbour is displaced by later insertions is re-linked +through the entry point rather than left unreachable. Search therefore +never strands an inserted point, and `search` results reflect every +point accepted by `insert` or `insert_harvesting`. These guarantees are +verified by bounded Kani proofs and property tests; see the developers' +guide for the verification policy. + ## Results and assignments `Chutoro::run` returns a `ClusteringResult`, which exposes the per-item diff --git a/tests/workflow_contracts/action_pins_test.py b/tests/workflow_contracts/action_pins_test.py new file mode 100644 index 00000000..e6c671c6 --- /dev/null +++ b/tests/workflow_contracts/action_pins_test.py @@ -0,0 +1,129 @@ +"""Repository-wide contract for GitHub Actions pins. + +Dependabot owns the pin values and updates them as a single group, so these +tests assert shape and consistency rather than any specific commit. Naming a +SHA here would duplicate the one thing that is expected to change, turning +every routine bump into a spurious failure. + +Two properties are checked across every workflow: + +- every third-party ``uses:`` reference is pinned to a full 40-hex commit + SHA, not a branch or tag, so a moved tag cannot alter what CI executes; and +- an action referenced from more than one workflow resolves to the *same* + SHA everywhere, so a partially applied bump is caught rather than leaving + workflows silently running different revisions of the same action. + +Run via ``make test-workflow-contracts``. +""" + +from __future__ import annotations + +import re +from collections import defaultdict +from collections.abc import Iterator +from pathlib import Path + +import pytest +import yaml + +REPO_ROOT = Path(__file__).resolve().parents[2] +WORKFLOW_DIR = REPO_ROOT / ".github" / "workflows" + +#: ``owner/repo[/path]@ref`` split into the action identity and its ref. +USES_RE = re.compile(r"^(?P[^@]+)@(?P.+)$") +SHA_RE = re.compile(r"^[0-9a-f]{40}$") + +#: Local composite actions and reusable workflows referenced by relative path +#: carry no ref, so they are outside this contract. +LOCAL_PREFIXES = ("./", "../") + + +def _workflow_files() -> list[Path]: + """Return every workflow definition in the repository.""" + return sorted( + path + for path in WORKFLOW_DIR.iterdir() + if path.suffix in {".yml", ".yaml"} and path.is_file() + ) + + +def _iter_uses(document: object) -> Iterator[str]: + """Yield every ``uses:`` value anywhere in a parsed workflow.""" + if isinstance(document, dict): + yield from _iter_uses_in_mapping(document) + elif isinstance(document, list): + for item in document: + yield from _iter_uses(item) + + +def _iter_uses_in_mapping(mapping: dict[str, object]) -> Iterator[str]: + """Yield the ``uses:`` value of one mapping, then recurse into the rest.""" + for key, value in mapping.items(): + if key == "uses" and isinstance(value, str): + yield value + else: + yield from _iter_uses(value) + + +@pytest.fixture(scope="module") +def references() -> dict[str, dict[str, set[str]]]: + """Map each action to the SHAs it is pinned at, and where. + + Shaped as ``{action: {sha: {workflow, ...}}}`` so a failure can name the + workflows that disagree. + """ + collected: dict[str, dict[str, set[str]]] = defaultdict( + lambda: defaultdict(set) + ) + for path in _workflow_files(): + document = yaml.safe_load(path.read_text(encoding="utf-8")) + for uses in _iter_uses(document): + if uses.startswith(LOCAL_PREFIXES): + continue + match = USES_RE.match(uses) + assert match, f"{path.name}: unparseable uses value {uses!r}" + collected[match["action"]][match["ref"]].add(path.name) + return collected + + +def test_workflows_are_discovered() -> None: + """Guard the derivation: an empty scan would pass everything vacuously.""" + workflows = _workflow_files() + assert workflows, f"no workflow definitions found under {WORKFLOW_DIR}" + + +def test_every_action_is_pinned_to_a_commit_sha( + references: dict[str, dict[str, set[str]]], +) -> None: + """No workflow may track a branch or a movable tag.""" + assert references, "no external action references were discovered" + + unpinned = { + f"{action}@{ref}": sorted(workflows) + for action, refs in references.items() + for ref, workflows in refs.items() + if not SHA_RE.match(ref) + } + assert not unpinned, ( + "every action must be pinned to a full 40-hex commit SHA rather than " + f"a branch or tag; these are not: {unpinned!r}" + ) + + +def test_shared_actions_are_consistent_across_workflows( + references: dict[str, dict[str, set[str]]], +) -> None: + """An action used more than once resolves to one SHA everywhere. + + This is what catches a partially applied Dependabot bump: the pin itself + may be any value, but it must not differ between workflows. + """ + divergent = { + action: {ref: sorted(workflows) for ref, workflows in refs.items()} + for action, refs in references.items() + if len(refs) > 1 + } + assert not divergent, ( + "each action must resolve to the same commit SHA in every workflow; " + f"these diverge: {divergent!r}" + ) diff --git a/tests/workflow_contracts/kani_fast_tier_test.py b/tests/workflow_contracts/kani_fast_tier_test.py new file mode 100644 index 00000000..9968c283 --- /dev/null +++ b/tests/workflow_contracts/kani_fast_tier_test.py @@ -0,0 +1,73 @@ +"""Contract between the fast-tier Makefile target and the fast-tier docs. + +``make kani`` is the pull-request gate, so its meaning depends on which +harnesses the ``kani:`` target actually runs. The MST harness module +documents that both of its proofs are fast-tier; this test derives the +harness names from that source file and asserts the Makefile runs each, +so the tier decision cannot drift from the documented one. Deriving the +names rather than restating them keeps the contract self-maintaining: a +proof added to the module fails here until the Makefile carries it. + +Run via ``make test-workflow-contracts``. +""" + +from __future__ import annotations + +import re +from pathlib import Path + +import pytest + +REPO_ROOT = Path(__file__).resolve().parents[2] +MAKEFILE_PATH = REPO_ROOT / "Makefile" + +#: Harness modules whose module docs declare every proof fast-tier. +FAST_TIER_SOURCES = (REPO_ROOT / "chutoro-core" / "src" / "mst" / "kani_harness.rs",) + +PROOF_RE = re.compile(r"^\s*fn\s+(verify_\w+)", re.MULTILINE) + +#: The first ``kani:`` target header and its immediately following +#: tab-indented recipe lines; the capture stops at the first line that is +#: not tab-indented. +KANI_TARGET_RE = re.compile( + r"^kani:[^\n]*\n(?P(?:\t[^\n]*(?:\n|$))*)", + re.MULTILINE, +) + + +def _fast_tier_harnesses() -> list[str]: + """Return every proof name declared in the fast-tier harness modules.""" + names: list[str] = [] + for source in FAST_TIER_SOURCES: + names.extend(PROOF_RE.findall(source.read_text(encoding="utf-8"))) + return names + + +@pytest.fixture(scope="module") +def kani_target() -> str: + """Return the recipe body of the Makefile's ``kani:`` target.""" + match = KANI_TARGET_RE.search(MAKEFILE_PATH.read_text(encoding="utf-8")) + assert match and match["recipe"], ( + "the Makefile must define a kani: target with a recipe" + ) + return match["recipe"].rstrip("\n") + + +def test_fast_tier_sources_declare_harnesses() -> None: + """Guard the derivation: an empty scan would pass everything vacuously.""" + harnesses = _fast_tier_harnesses() + assert harnesses, ( + f"no proofs found in {[str(p) for p in FAST_TIER_SOURCES]}; " + "the derivation regex or source list is broken" + ) + + +def test_make_kani_runs_every_fast_tier_harness(kani_target: str) -> None: + """Each documented fast-tier proof appears in the gating target.""" + missing = [ + name for name in _fast_tier_harnesses() if name not in kani_target + ] + assert not missing, ( + "the Makefile kani: target must run every fast-tier harness declared " + f"in the MST harness module; missing: {missing!r}" + ) diff --git a/tests/workflow_contracts/kani_pr_test.py b/tests/workflow_contracts/kani_pr_test.py new file mode 100644 index 00000000..9ec798e2 --- /dev/null +++ b/tests/workflow_contracts/kani_pr_test.py @@ -0,0 +1,273 @@ +"""Contract tests for the pull-request Kani gate workflow. + +The workflow is declarative configuration: it decides when the Kani gate +runs, what the checkout may do with the workflow token, and which Kani +version verifies the proofs. These tests parse the workflow with PyYAML +and pin that contract, so drift (losing a path filter, unpinning an +action or the verifier, widening permissions, or dropping the gating +step) fails CI on the pull request that introduces it. + +These tests assert shapes and relationships, never specific pinned +values. Restating a pin in a test only duplicates the thing that changes, +so a routine bump fails the build for no defect. Accordingly: action pins +are checked for shape (a 40-hex commit SHA on the correct action path) and +for cross-workflow consistency in ``action_pins_test``; the path filter is +checked by deriving the Kani surface from the tree and asserting the +filter covers it; and the verifier version is checked only for the +workflow deriving it from ``tools/kani/VERSION`` -- the single source of +truth also read by the Makefile and by ``prover-tools kani install``. + +Run via ``make test-workflow-contracts``. +""" + +from __future__ import annotations + +import re +from pathlib import Path + +import pathspec +import pytest +import yaml + +REPO_ROOT = Path(__file__).resolve().parents[2] +WORKFLOW_PATH = REPO_ROOT / ".github" / "workflows" / "kani-pr.yml" +NIGHTLY_PATH = REPO_ROOT / ".github" / "workflows" / "nightly-kani.yml" +#: Single source of truth for the pinned Kani verifier version. +KANI_VERSION_PATH = REPO_ROOT / "tools" / "kani" / "VERSION" +SEMVER_RE = re.compile(r"^\d+\.\d+\.\d+$") +#: A literal version argument, e.g. ``--version 1.2.3``. The workflow must +#: interpolate the pin file instead, so this pattern must never match. +VERSION_LITERAL_RE = re.compile(r"--version\s+[\"']?\d") + +CHECKOUT_RE = re.compile(r"^actions/checkout@[0-9a-f]{40}$") +SETUP_RUST_RE = re.compile( + r"^leynos/shared-actions/\.github/actions/setup-rust@[0-9a-f]{40}$" +) + +#: Non-source inputs that change what the gate runs, so a change to any of +#: them must trigger it. Everything else is derived from the tree below. +GATE_INPUTS = ("Makefile", "Cargo.lock", "tools/kani/VERSION") + + +def _kani_surface() -> list[str]: + """Return every Kani harness path in the tree, repository-relative. + + Derived rather than enumerated so a harness added in a new location + fails this contract until the path filter covers it. + """ + surface = { + path.relative_to(REPO_ROOT).as_posix() + for path in REPO_ROOT.rglob("kani_*.rs") + if "target" not in path.parts + } + surface |= { + path.relative_to(REPO_ROOT).as_posix() + for path in REPO_ROOT.rglob("kani_proofs/*.rs") + if "target" not in path.parts + } + return sorted(surface) + + +def _uncovered(paths: list[str], patterns: list[str]) -> list[str]: + """Return the paths no filter pattern matches.""" + spec = pathspec.PathSpec.from_lines("gitignore", patterns) + return [path for path in paths if not spec.match_file(path)] + + + +@pytest.fixture(scope="module") +def workflow() -> dict[str, object]: + """Parse the workflow file once for every contract test.""" + return yaml.safe_load(WORKFLOW_PATH.read_text(encoding="utf-8")) + + +def _triggers(workflow: dict[str, object]) -> dict[str, object]: + """Return the ``on:`` mapping (PyYAML parses the bare key as True).""" + triggers = workflow.get("on", workflow.get(True)) + assert isinstance(triggers, dict), "the workflow must declare an on: mapping" + return triggers + + +def _kani_job(workflow: dict[str, object]) -> dict[str, object]: + """Return the single gating job.""" + jobs = workflow.get("jobs") + assert isinstance(jobs, dict), "the workflow must declare a jobs mapping" + assert list(jobs) == ["kani"], ( + f"expected a single job named 'kani', found {sorted(jobs)}" + ) + return jobs["kani"] + + +def _steps(workflow: dict[str, object]) -> list[dict[str, object]]: + """Return the gating job's step list.""" + steps = _kani_job(workflow).get("steps") + assert isinstance(steps, list) and steps, "jobs.kani.steps is missing" + return steps + + +def test_pull_request_trigger_covers_the_kani_surface( + workflow: dict[str, object], +) -> None: + """The gate fires on main-targeted PRs touching Kani-relevant paths.""" + triggers = _triggers(workflow) + pull_request = triggers.get("pull_request") + assert isinstance(pull_request, dict), "on.pull_request is missing" + assert pull_request.get("branches") == ["main"], ( + f"on.pull_request.branches must be ['main'], got " + f"{pull_request.get('branches')!r}" + ) + assert pull_request.get("types") == ["opened", "synchronize", "reopened"], ( + f"on.pull_request.types must cover opened/synchronize/reopened, got " + f"{pull_request.get('types')!r}" + ) + patterns = pull_request.get("paths") + assert isinstance(patterns, list) and patterns, ( + f"on.pull_request.paths must list filter patterns, got {patterns!r}" + ) + + surface = _kani_surface() + assert surface, "no Kani harnesses were discovered; the derivation is broken" + missed = _uncovered(surface, patterns) + assert not missed, ( + "on.pull_request.paths must cover every Kani harness in the tree; " + f"these are not matched by any pattern: {missed!r}" + ) + + missed_inputs = _uncovered(list(GATE_INPUTS), patterns) + assert not missed_inputs, ( + "on.pull_request.paths must cover the inputs that change what the " + f"gate runs; these are not matched by any pattern: {missed_inputs!r}" + ) + + assert "workflow_dispatch" in triggers, "on.workflow_dispatch is missing" + + +def test_workflow_permissions_are_read_only(workflow: dict[str, object]) -> None: + """The workflow token grants contents: read and nothing broader.""" + permissions = workflow.get("permissions") + assert permissions == {"contents": "read"}, ( + f"permissions must be exactly {{'contents': 'read'}}, got {permissions!r}" + ) + + +def test_concurrency_cancels_superseded_runs(workflow: dict[str, object]) -> None: + """A newer push cancels the previous run for the same ref.""" + concurrency = workflow.get("concurrency") + assert isinstance(concurrency, dict), "the workflow must declare concurrency" + assert concurrency.get("group") == "kani-pr-${{ github.ref }}", ( + f"concurrency.group must key on the triggering ref, got " + f"{concurrency.get('group')!r}" + ) + assert concurrency.get("cancel-in-progress") is True, ( + f"concurrency.cancel-in-progress must be true, got " + f"{concurrency.get('cancel-in-progress')!r}" + ) + + +def test_job_timeout_is_tighter_than_the_nightly_budget( + workflow: dict[str, object], +) -> None: + """The PR gate is bounded, and strictly tighter than the nightly tier.""" + timeout = _kani_job(workflow).get("timeout-minutes") + assert isinstance(timeout, int) and timeout > 0, ( + f"jobs.kani.timeout-minutes must be a positive integer, got {timeout!r}" + ) + + nightly = yaml.safe_load(NIGHTLY_PATH.read_text(encoding="utf-8")) + nightly_jobs = nightly.get("jobs") + assert isinstance(nightly_jobs, dict) and nightly_jobs, ( + "the nightly Kani workflow must declare a job to compare against" + ) + nightly_timeout = next(iter(nightly_jobs.values())).get("timeout-minutes") + assert isinstance(nightly_timeout, int), ( + f"the nightly job must declare timeout-minutes, got {nightly_timeout!r}" + ) + assert timeout < nightly_timeout, ( + "the pull-request gate must be tighter than the nightly tier: " + f"PR is {timeout} minutes, nightly is {nightly_timeout}" + ) + + +def test_checkout_is_pinned_and_does_not_persist_credentials( + workflow: dict[str, object], +) -> None: + """Checkout is SHA-pinned and drops the token before running PR code.""" + steps = _steps(workflow) + checkout = steps[0] + uses = checkout.get("uses") + assert isinstance(uses, str) and CHECKOUT_RE.match(uses), ( + f"the first step must be actions/checkout pinned to a 40-hex commit " + f"SHA, got {uses!r}" + ) + with_block = checkout.get("with") + assert isinstance(with_block, dict) and ( + with_block.get("persist-credentials") is False + ), ( + "the checkout step must set persist-credentials: false so the " + f"workflow token is not retained in Git configuration, got " + f"{with_block!r}" + ) + + +def test_setup_rust_is_pinned_to_a_commit_sha(workflow: dict[str, object]) -> None: + """The shared setup-rust action is referenced at a full commit SHA.""" + steps = _steps(workflow) + uses_values = [step.get("uses") for step in steps if step.get("uses")] + assert any( + isinstance(uses, str) and SETUP_RUST_RE.match(uses) for uses in uses_values + ), ( + "a step must use leynos/shared-actions setup-rust pinned to a " + f"40-hex commit SHA, got {uses_values!r}" + ) + + +def test_kani_install_is_locked_and_version_pinned( + workflow: dict[str, object], +) -> None: + """The verifier installs with --locked at an exact approved version.""" + steps = _steps(workflow) + install_runs = [ + step.get("run") + for step in steps + if isinstance(step.get("run"), str) and "kani-verifier" in step["run"] + ] + assert len(install_runs) == 1, ( + f"expected exactly one Kani install step, found {len(install_runs)}" + ) + run = install_runs[0] + assert "--locked" in run, ( + f"the install step must pass --locked, got {run!r}" + ) + assert "tools/kani/VERSION" in run, ( + "the install step must read the pinned version from " + f"tools/kani/VERSION rather than restating it, got {run!r}" + ) + assert VERSION_LITERAL_RE.search(run) is None, ( + "the install step must not hardcode a version literal; the pin " + f"belongs solely in tools/kani/VERSION, got {run!r}" + ) + assert "cargo kani setup" in run, ( + f"the install step must run cargo kani setup, got {run!r}" + ) + + +def test_pinned_kani_version_file_is_a_bare_semver() -> None: + """The pin file holds one machine-readable version and nothing else.""" + assert KANI_VERSION_PATH.is_file(), ( + f"the pinned Kani version file is missing: {KANI_VERSION_PATH}" + ) + raw = KANI_VERSION_PATH.read_text(encoding="utf-8") + version = raw.strip() + assert SEMVER_RE.match(version), ( + f"tools/kani/VERSION must contain a bare MAJOR.MINOR.PATCH version, " + f"got {raw!r}" + ) + + +def test_gating_step_runs_the_practical_suite(workflow: dict[str, object]) -> None: + """The gate runs make kani, the fast practical tier.""" + steps = _steps(workflow) + run_steps = [step.get("run") for step in steps if isinstance(step.get("run"), str)] + assert any(run.strip() == "make kani" for run in run_steps), ( + f"a step must run 'make kani' as the gating command, got {run_steps!r}" + ) diff --git a/tools/kani/VERSION b/tools/kani/VERSION new file mode 100644 index 00000000..328185ca --- /dev/null +++ b/tools/kani/VERSION @@ -0,0 +1 @@ +0.67.0