Crate whale 

Whale is a lock-free incremental computation dependency tracking library.

This crate provides primitives for building incremental computation systems, following the formally verified specification in Lean4.

Key Concepts

• Durability: Nodes have durability levels (0 = volatile, N-1 = stable). A node’s durability cannot exceed its dependencies’ minimum durability.

• Validity: A node is valid if its verified_at >= revision[durability], or all its dependencies haven’t changed since observation.

• Early Cutoff: When a node’s value doesn’t change after recomputation, we use confirm_unchanged to preserve changed_at, preventing unnecessary downstream recomputation.

Example

use whale::{Runtime, Durability};

// Create a runtime with 3 durability levels
let rt: Runtime<&str, (), 3> = Runtime::new();

// Register nodes
rt.register("a", (), Durability::volatile(), vec![]).unwrap();
rt.register("b", (), Durability::volatile(), vec!["a"]).unwrap();

// Check validity
assert!(rt.is_valid(&"a"));
assert!(rt.is_valid(&"b"));

// After updating "a", "b" becomes invalid
rt.register("a", (), Durability::volatile(), vec![]).unwrap();
assert!(!rt.is_valid(&"b"));

// Early cutoff: if "b" recomputes and its value is unchanged
rt.confirm_unchanged(&"b", vec!["a"]).unwrap();
assert!(rt.is_valid(&"b"));

Structs

AtomicRevision

Atomic revision counters for concurrent access.

Dep

Dependency record: tracks which query we depend on and what its changed_at was when we observed it.

Dependencies

Dependencies is a list of dependency records for the queries that this query depends on.

Dependents

Dependents is a list of query IDs that depend on this query.

Durability

Durability level: 0 = most volatile, N-1 = most stable.

Node

Node in the dependency graph.

RegisterResult

Result of a registration operation.

Revision

Revision snapshot: array of counters indexed by durability level.

Runtime

Runtime manages the dependency graph and revision tracking.

Type Aliases

RevisionCounter

Revision counter type - monotonically increasing counter for tracking changes.