trust_engine: add a formally verified derivation kernel

.veri/.gitignore

@@ -0,0 +1,3 @@
+# Verifier build scratch (run_log, intermediate rounds, the dafny->rust crate).
+# Clean artifacts are written to each module's configured output dir instead.
+build/

.veri/veri.toml

@@ -0,0 +1,15 @@
+# Veri project configuration for intermesh.
+# Run `python3 -m veri_build.pipeline build <name>` from this directory.
+
+[keys]
+# Path to a file containing the raw Anthropic API key. Exported as
+# ANTHROPIC_API_KEY for the build (an already-set env var wins).
+anthropic = "~/.veri-api-key"
+
+# The verified trust-engine kernel. Spec → output paths are relative to this
+# directory (the project root containing .veri/).
+[[modules]]
+name    = "trust_engine"
+spec    = "src/trust_engine.veri.md"
+output  = "src/trust_engine/kernel/"
+timeout = 1800

Cargo.toml

@@ -6,9 +6,16 @@ publish = false
 
 [workspace]
 members = ["xtask"]
+# The verified trust-engine kernel is a generated, self-contained crate (its own
+# vendored dafny_runtime). Keep it out of the workspace; intermesh depends on it
+# only under the `verified-kernel` feature.
+exclude = ["src/trust_engine/kernel"]
 
 [features]
 test-perf = []
+# Route Derivation::derive through the verified, Dafny-extracted kernel so the
+# existing trust-engine tests run against it.
+verified-kernel = ["dep:trust_engine_kernel"]
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
@@ -95,5 +102,10 @@ too_many_lines = "allow"
 missing_errors_doc = "allow"
 missing_panics_doc = "allow"
 
+[dependencies.trust_engine_kernel]
+package = "TrustEngine"
+path = "src/trust_engine/kernel"
+optional = true
+
 [dev-dependencies]
 rayon = "1.11.0"

src/trust_engine.rs

@@ -1,17 +1,36 @@
-use crate::assert::UnwrapAssert;
 use crate::authorization::Authz;
 use crate::constraint::Constraint;
 use crate::endor;
 use crate::ident::{Name, NamePattern};
 use crate::imid::Imid;
 use arc_swap::ArcSwap;
-use ipnet::IpNet;
 use serde::{Deserialize, Serialize};
 use std::collections::{BTreeMap, BTreeSet};
-use std::net::{IpAddr, Ipv4Addr};
+use std::net::IpAddr;
 use std::sync::Arc;
 use tokio::sync::Mutex;
-use tracing::{info, instrument, warn};
+use tracing::instrument;
+
+// Used only by the native trust engine (the verified-kernel path replaces it).
+#[cfg(not(feature = "verified-kernel"))]
+use {
+    ipnet::IpNet,
+    std::net::Ipv4Addr,
+    tracing::{info, warn},
+};
+// Used by the native engine and by tests (the `.assert()` helper).
+#[cfg(any(test, not(feature = "verified-kernel")))]
+use crate::assert::UnwrapAssert;
+
+// The verified-kernel path. Under the `verified-kernel` feature, `derive`
+// delegates to the Dafny-extracted kernel: `runner` orchestrates (marshal in →
+// kernel → marshal out); `marshal` does the interning / claim explosion /
+// relation building both directions. Both pull in the generated kernel crate.
+#[cfg(feature = "verified-kernel")]
+mod marshal;
+#[cfg(feature = "verified-kernel")]
+mod runner;
+
 /* OPT: Regarding Optimizations
  *
  * This code is intentionally highly un-optimized.  If you're reading this
@@ -28,12 +47,6 @@ use tracing::{info, instrument, warn};
  * that will change dramatically with a proper algorithmic optimization later.
  */
 
-// Maximum iterations for fixed-point derivation. Any reasonable trust policy
-// should converge well before this limit. The cap exists primarily for DOS
-// mitigation - malicious or misconfigured deep delegation chains could
-// otherwise waste CPU indefinitely.
-const MAX_DERIVATION_ITERATIONS: usize = 50;
-
 // A TrustEngine holds the derived lookup tables from an endorsement base set.
 // It uses an internal datalog engine to process positive endorsement facts and
 // constraints to produce verified lookup tables. Signed-message preprocessing
@@ -176,6 +189,82 @@ impl Derivation {
         }
     }
 
+    // Verified-kernel path: delegate to the Dafny-extracted kernel via the
+    // marshalling runner, preserving derive's bookkeeping (iteration, input) so
+    // the rest of the engine behaves identically. The kernel always derives from
+    // scratch — the same least fixed point the native loop converges to.
+    #[cfg(feature = "verified-kernel")]
+    fn derive(&self, bases: &BTreeSet<endor::Base>) -> Derivation {
+        let mut result = runner::run(&self.my_imid, bases);
+        result.iteration = self.iteration + 1;
+        result.input.clone_from(bases);
+        result
+    }
+
+    // Compute derived indexes after the fixed-point loop converges.
+    fn finalize(&mut self) {
+        // Build imid_to_names as inverse of name_to_imid
+        self.imid_to_names.clear();
+        for (name, imids) in &self.name_to_imid {
+            for imid in imids {
+                self.imid_to_names
+                    .entry(imid.clone())
+                    .or_default()
+                    .insert(name.clone());
+            }
+        }
+
+        // Compute my_authz_to and my_authz_from from authorization rules.
+        // Done here rather than in apply_endor() because pattern matching
+        // depends on name_to_imid being complete.
+        self.my_authz_to.clear();
+        self.my_authz_from.clear();
+        for authz in &self.my_authz {
+            let sources = self.expand_authz_side(&authz.source_imids, &authz.source_patterns);
+            let destinations =
+                self.expand_authz_side(&authz.destination_imids, &authz.destination_patterns);
+
+            if sources.contains(&self.my_imid) {
+                self.my_authz_to.extend(destinations.iter().cloned());
+            }
+            if destinations.contains(&self.my_imid) {
+                self.my_authz_from.extend(sources);
+            }
+        }
+    }
+
+    fn expand_authz_side(
+        &self,
+        imids: &BTreeSet<Imid>,
+        patterns: &BTreeSet<NamePattern>,
+    ) -> BTreeSet<Imid> {
+        let mut expanded: BTreeSet<Imid> = imids.iter().cloned().collect();
+        for pattern in patterns {
+            expanded.extend(self.imids_in_pattern(pattern).cloned());
+        }
+        expanded
+    }
+
+    // OPT: an imid_to_name and a name_to_pattern index could optimize this.
+    fn imids_in_pattern<'a>(&'a self, pattern: &'a NamePattern) -> impl Iterator<Item = &'a Imid> {
+        self.name_to_imid
+            .iter()
+            .filter(move |(name, _)| pattern.matches(name))
+            .flat_map(|(_, imids)| imids)
+    }
+}
+
+// The native trust engine: the fixed-point loop and its gating helpers. Under
+// the `verified-kernel` feature the kernel replaces this whole path, so it
+// compiles only when that feature is off.
+#[cfg(not(feature = "verified-kernel"))]
+impl Derivation {
+    // Maximum iterations for fixed-point derivation. Any reasonable trust policy
+    // should converge well before this limit. The cap exists primarily for DOS
+    // mitigation - malicious or misconfigured deep delegation chains could
+    // otherwise waste CPU indefinitely.
+    const MAX_DERIVATION_ITERATIONS: usize = 50;
+
     fn derive(&self, bases: &BTreeSet<endor::Base>) -> Derivation {
         info!("Trust Engine Derive");
 
@@ -222,7 +311,7 @@ impl Derivation {
         // convergence is mathematically guaranteed. MAX_DERIVATION_ITERATIONS
         // catches bugs or unexpectedly deep delegation chains before returning
         // an unsafe partial derivation.
-        for _ in 0..MAX_DERIVATION_ITERATIONS {
+        for _ in 0..Self::MAX_DERIVATION_ITERATIONS {
             let mut changed = false;
             for base in bases {
                 changed = result.apply_endor(base) || changed;
@@ -234,7 +323,7 @@ impl Derivation {
 
         panic!(
             "trust engine failed to converge after {} iterations ({} endorsements, {} names, {} IPs, {} constraints)",
-            MAX_DERIVATION_ITERATIONS,
+            Self::MAX_DERIVATION_ITERATIONS,
             result.input.len(),
             result.name_to_imid.len(),
             result.imid_to_ip.len(),
@@ -338,50 +427,6 @@ impl Derivation {
         changed
     }
 
-    // Compute derived indexes after the fixed-point loop converges.
-    fn finalize(&mut self) {
-        // Build imid_to_names as inverse of name_to_imid
-        self.imid_to_names.clear();
-        for (name, imids) in &self.name_to_imid {
-            for imid in imids {
-                self.imid_to_names
-                    .entry(imid.clone())
-                    .or_default()
-                    .insert(name.clone());
-            }
-        }
-
-        // Compute my_authz_to and my_authz_from from authorization rules.
-        // Done here rather than in apply_endor() because pattern matching
-        // depends on name_to_imid being complete.
-        self.my_authz_to.clear();
-        self.my_authz_from.clear();
-        for authz in &self.my_authz {
-            let sources = self.expand_authz_side(&authz.source_imids, &authz.source_patterns);
-            let destinations =
-                self.expand_authz_side(&authz.destination_imids, &authz.destination_patterns);
-
-            if sources.contains(&self.my_imid) {
-                self.my_authz_to.extend(destinations.iter().cloned());
-            }
-            if destinations.contains(&self.my_imid) {
-                self.my_authz_from.extend(sources);
-            }
-        }
-    }
-
-    fn expand_authz_side(
-        &self,
-        imids: &BTreeSet<Imid>,
-        patterns: &BTreeSet<NamePattern>,
-    ) -> BTreeSet<Imid> {
-        let mut expanded: BTreeSet<Imid> = imids.iter().cloned().collect();
-        for pattern in patterns {
-            expanded.extend(self.imids_in_pattern(pattern).cloned());
-        }
-        expanded
-    }
-
     fn constraint_permits_endorser(&self, constraint: &Constraint, endorser: &Imid) -> bool {
         // OPT: Once a target is permitted by a constraint it's always permitted
         // Memoization could be helpful here.
@@ -396,14 +441,6 @@ impl Derivation {
             || self.patterns_contains(&constraint.target_patterns, target)
     }
 
-    // OPT: an imid_to_name and a name_to_pattern index could optimize this.
-    fn imids_in_pattern<'a>(&'a self, pattern: &'a NamePattern) -> impl Iterator<Item = &'a Imid> {
-        self.name_to_imid
-            .iter()
-            .filter(move |(name, _)| pattern.matches(name))
-            .flat_map(|(_, imids)| imids)
-    }
-
     fn patterns_contains<'a>(
         &self,
         patterns: impl IntoIterator<Item = &'a NamePattern>,