perf(rust-kernel): Intern-assigned uids, symbolic Nat offsets, environment-machine WHNF reducer

crates/compile/src/kernel_egress.rs

@@ -384,9 +384,9 @@ struct EgressCtx {
   /// Memoized expression conversion. Keyed by `KExpr::addr()` (content
   /// hash); same hash → same Ixon expression (within a single block's
   /// tables).
-  expr_cache: FxHashMap<blake3::Hash, Arc<IxonExpr>>,
+  expr_cache: FxHashMap<ix_kernel::env::Addr, Arc<IxonExpr>>,
   /// Memoized universe conversion.
-  univ_cache: FxHashMap<blake3::Hash, Arc<IxonUniv>>,
+  univ_cache: FxHashMap<ix_kernel::env::Addr, Arc<IxonUniv>>,
 }
 
 impl EgressCtx {

crates/ixon/src/lazy.rs

@@ -104,6 +104,15 @@ pub struct LazyConstant {
   /// this `None`; their `get()` parses fresh and does not store —
   /// see the module-level "Cache policy" docs.
   cache: Option<Arc<Constant>>,
+  /// Deferred address verification: when set (the `.ixe` load paths),
+  /// `get()` checks `Address::hash(bytes) == pending_addr` before
+  /// parsing. This moves the per-constant content-hash from env parse
+  /// time to first materialization, so constants that are shipped in a
+  /// closure but never forced by the typechecker are never hashed —
+  /// while everything the kernel CERTIFIES is still verified (checking
+  /// a constant forces its materialization). `None` for the
+  /// compile-side path, which owns the parsed value already.
+  pending_addr: Option<Address>,
 }
 
 impl LazyConstant {
@@ -114,7 +123,22 @@ impl LazyConstant {
   /// `Constant::put` produced for the address this entry is stored
   /// under. Use [`Self::verify_address`] for an explicit check.
   pub fn from_bytes(bytes: Arc<[u8]>) -> Self {
-    LazyConstant { bytes: BytesSource::Heap(bytes), cache: None }
+    LazyConstant {
+      bytes: BytesSource::Heap(bytes),
+      cache: None,
+      pending_addr: None,
+    }
+  }
+
+  /// Like [`Self::from_bytes`], but with the address-binding check
+  /// deferred to first [`Self::get`]. Used by `Env::get_anon` so env
+  /// parse time does not pay one content hash per constant.
+  pub fn from_bytes_deferred(bytes: Arc<[u8]>, addr: Address) -> Self {
+    LazyConstant {
+      bytes: BytesSource::Heap(bytes),
+      cache: None,
+      pending_addr: Some(addr),
+    }
   }
 
   /// Construct from a memory-mapped window. The `Arc<Mmap>` keeps
@@ -124,7 +148,11 @@ impl LazyConstant {
   /// Used by `Env::get_anon_mmap` to avoid heap-copying the on-disk
   /// byte stream — the OS page cache is the source of truth.
   pub fn from_mmap_slice(mmap: Arc<Mmap>, offset: usize, len: usize) -> Self {
-    LazyConstant { bytes: BytesSource::Mmap { mmap, offset, len }, cache: None }
+    LazyConstant {
+      bytes: BytesSource::Mmap { mmap, offset, len },
+      cache: None,
+      pending_addr: None,
+    }
   }
 
   /// Construct from a structured `Constant` (the in-memory build path,
@@ -137,6 +165,7 @@ impl LazyConstant {
     LazyConstant {
       bytes: BytesSource::Heap(buf.into()),
       cache: Some(Arc::new(c)),
+      pending_addr: None,
     }
   }
 
@@ -151,6 +180,16 @@ impl LazyConstant {
     if let Some(c) = &self.cache {
       return Ok(c.clone());
     }
+    if let Some(expected) = &self.pending_addr {
+      let computed = Address::hash(self.bytes.as_slice());
+      if computed != *expected {
+        return Err(format!(
+          "LazyConstant::get: bytes hash to {} but stored under {}",
+          computed.hex(),
+          expected.hex()
+        ));
+      }
+    }
     let mut slice: &[u8] = self.bytes.as_slice();
     let parsed = Constant::get(&mut slice)
       .map_err(|e| format!("LazyConstant::get: {e}"))?;

crates/ixon/src/serialize.rs

@@ -1419,6 +1419,20 @@ impl Env {
       }
       let (bytes, rest) = buf.split_at(len);
       *buf = rest;
+      // Blob bytes are bound to their address HERE, eagerly: literal
+      // identity downstream (kernel `ExprKey::Nat`/`Str` interning,
+      // `Constant.refs` blob entries, assumption filtering) keys on the
+      // address, so an unverified blob would let an adversarial env bind
+      // wrong bytes to a content address. Blobs are a small fraction of
+      // env bytes; constants stay lazily verified (see LazyConstant).
+      let computed = Address::hash(bytes);
+      if computed != addr {
+        return Err(format!(
+          "Env::get: blob bytes hash to {} but stored under {}",
+          computed.hex(),
+          addr.hex()
+        ));
+      }
       env.blobs.insert(addr, bytes.to_vec());
     }
 
@@ -1568,6 +1582,20 @@ impl Env {
       }
       let (bytes, rest) = buf.split_at(len);
       *buf = rest;
+      // Blob bytes are bound to their address HERE, eagerly: literal
+      // identity downstream (kernel `ExprKey::Nat`/`Str` interning,
+      // `Constant.refs` blob entries, assumption filtering) keys on the
+      // address, so an unverified blob would let an adversarial env bind
+      // wrong bytes to a content address. Blobs are a small fraction of
+      // env bytes; constants stay lazily verified (see LazyConstant).
+      let computed = Address::hash(bytes);
+      if computed != addr {
+        return Err(format!(
+          "Env::get_anon: blob bytes hash to {} but stored under {}",
+          computed.hex(),
+          addr.hex()
+        ));
+      }
       env.blobs.insert(addr, bytes.to_vec());
     }
 
@@ -1585,17 +1613,16 @@ impl Env {
       }
       let (bytes, rest) = buf.split_at(len);
       *buf = rest;
-      let computed = Address::hash(bytes);
-      if computed != addr {
-        return Err(format!(
-          "Env::get_anon: const at idx {i} bytes hash to {} but stored under {}",
-          computed.hex(),
-          addr.hex()
-        ));
-      }
-      env
-        .consts
-        .insert(addr, crate::lazy::LazyConstant::from_bytes(bytes.into()));
+      let _ = i;
+      // Address binding is verified lazily at first materialization
+      // (`LazyConstant::get`) instead of one content hash per constant
+      // here — constants shipped in a closure but never forced by the
+      // typechecker are never hashed, while everything the kernel
+      // certifies still gets verified on the way in.
+      env.consts.insert(
+        addr.clone(),
+        crate::lazy::LazyConstant::from_bytes_deferred(bytes.into(), addr),
+      );
     }
 
     // Section 3: Names — parse and DISCARD. We still need a populated
@@ -1769,6 +1796,20 @@ impl Env {
       }
       let (bytes, rest) = buf.split_at(len);
       buf = rest;
+      // Blob bytes are bound to their address HERE, eagerly: literal
+      // identity downstream (kernel `ExprKey::Nat`/`Str` interning,
+      // `Constant.refs` blob entries, assumption filtering) keys on the
+      // address, so an unverified blob would let an adversarial env bind
+      // wrong bytes to a content address. Blobs are a small fraction of
+      // env bytes; constants stay lazily verified (see LazyConstant).
+      let computed = Address::hash(bytes);
+      if computed != addr {
+        return Err(format!(
+          "Env::get_anon_mmap: blob bytes hash to {} but stored under {}",
+          computed.hex(),
+          addr.hex()
+        ));
+      }
       env.blobs.insert(addr, bytes.to_vec());
     }
 
@@ -2452,8 +2493,16 @@ mod tests {
     let off = 68 + 3;
     assert!(off < buf.len());
     buf[off] ^= 0xFF;
-    let res = Env::get_anon(&mut buf.as_slice());
-    let err = res.expect_err("tampered const bytes should be rejected");
+    // Address binding is verified lazily: parse succeeds, but the
+    // tampered constant is rejected at first materialization (which is
+    // what gates anything the kernel certifies).
+    let parsed = Env::get_anon(&mut buf.as_slice())
+      .expect("get_anon defers per-const verification");
+    let entry = parsed.consts.iter().next().expect("one const");
+    let err = entry
+      .value()
+      .get()
+      .expect_err("tampered const bytes should be rejected at get()");
     assert!(
       err.contains("bytes hash to") && err.contains("but stored under"),
       "expected per-entry verify error, got: {err}"

crates/kernel/Cargo.toml

@@ -36,5 +36,12 @@ quickcheck_macros = { workspace = true }
 name = "perf_check"
 path = "examples/perf_check.rs"
 
+# Native single-constant check (one work item via the lazy-anon path the
+# Zisk guest uses), so the `IX_*` instrumentation can target one expensive
+# constant without re-checking its whole env.
+[[example]]
+name = "check_one"
+path = "examples/check_one.rs"
+
 [lints]
 workspace = true

crates/kernel/examples/check_one.rs

@@ -0,0 +1,72 @@
+//! Native single-constant check, mirroring the Zisk guest's reuse-mode path
+//! (`zisk/guest/src/main.rs`): resolve a Lean NAME through the env's `named`
+//! metadata to its ingress block, then `check_const` exactly that work item
+//! with the lazy-anon TypeChecker. Exists so the kernel's `IX_*`
+//! instrumentation (inert inside zkVM guests — see `src/lib.rs::env_var_os`)
+//! can be pointed at one expensive constant without re-checking a whole env.
+//!
+//!   IX_PERF_COUNTERS=1 cargo run --release --example check_one -- \
+//!     ~/ix/init.ixe '_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instRxcHasSize_eq'
+
+use std::env;
+use std::fs;
+use std::time::Instant;
+
+use ix_kernel::anon_work::build_anon_work;
+use ix_kernel::env::KEnv;
+use ix_kernel::id::KId;
+use ix_kernel::mode::Anon;
+use ix_kernel::tc::TypeChecker;
+use ixon::constant::ConstantInfo as CI;
+use ixon::env::Env as IxonEnv;
+
+fn main() {
+  env_logger::builder()
+    .filter_level(log::LevelFilter::Info)
+    .format_timestamp(None)
+    .init();
+  let path = env::args().nth(1).expect("usage: check_one <ixe> <name>");
+  let name = env::args().nth(2).expect("usage: check_one <ixe> <name>");
+  let bytes = fs::read(&path).expect("read ixe");
+
+  let t_parse = Instant::now();
+  let env = IxonEnv::get(&mut &bytes[..]).expect("decode env");
+  eprintln!("[check_one] parse:   {:>8.2?}", t_parse.elapsed());
+
+  // Name → constant address → ingress block (mirrors zisk-host
+  // `block_of_addr`): a projection's `block`, else the address itself.
+  let addr = env
+    .named
+    .iter()
+    .find(|e| e.key().pretty() == name || e.key().to_string() == name)
+    .map_or_else(
+      || panic!("no constant named {name:?} in {path}"),
+      |e| e.value().addr.clone(),
+    );
+  let block = match env.get_const(&addr).map(|c| c.info.clone()) {
+    Some(CI::IPrj(p)) => p.block,
+    Some(CI::CPrj(p)) => p.block,
+    Some(CI::RPrj(p)) => p.block,
+    Some(CI::DPrj(p)) => p.block,
+    _ => addr.clone(),
+  };
+
+  let work = build_anon_work(&env).expect("build_anon_work");
+  let item =
+    work.iter().find(|it| *it.primary() == block).expect("work item for block");
+
+  let mut kenv = KEnv::<Anon>::new();
+  let mut tc = TypeChecker::<Anon>::new_with_lazy_anon(&mut kenv, &env);
+  let kid = KId::<Anon>::new(item.primary().clone(), ());
+  let t_check = Instant::now();
+  let result = tc.check_const(&kid);
+  eprintln!(
+    "[check_one] check:   {:>8.2?}  result: {:?}",
+    t_check.elapsed(),
+    result.is_ok()
+  );
+  if let Err(e) = result {
+    eprintln!("[check_one] error: {e:?}");
+    std::process::exit(1);
+  }
+}