From 80d2ea14f9f6e4043b0e5ecbd763ad8c7b6cd33e Mon Sep 17 00:00:00 2001 From: "J. C. Burnham" Date: Thu, 17 Sep 2026 16:36:44 -0400 Subject: [PATCH 1/3] perf(compile): avoid redundant contract preparation passes --- Ix/Compile/SourceContract/Transport.lean | 28 +++++++++++++ Tests/Ix/SourceContract/Driver.lean | 20 +++++++++- crates/compile/src/compile/env.rs | 9 +---- crates/compile/src/graph.rs | 50 ++++++++++++++++++++++++ 4 files changed, 98 insertions(+), 9 deletions(-) diff --git a/Ix/Compile/SourceContract/Transport.lean b/Ix/Compile/SourceContract/Transport.lean index 272f40bde..0013fd9c9 100644 --- a/Ix/Compile/SourceContract/Transport.lean +++ b/Ix/Compile/SourceContract/Transport.lean @@ -102,14 +102,42 @@ def CompileInput.prepare (input : CompileInput) : let resolved ← input.resolve.mapError toString resolved.decorate +/-- Ordinary declarations need no occurrence resolution or decoration. Check +both reserved namespaces in one shared-expression walk, retaining the input +name/uniqueness checks even when there are no contracts to resolve. Any selected +registration or metadata marker uses the full validation path below. -/ +def checkOrdinaryConstants (constants : List (Lean.Name × Lean.ConstantInfo)) + (registered : Lean.Name → Bool) : Except String Bool := do + let hasContracts (expr : Lean.Expr) := (expr.find? fun + | .mdata data _ => data.entries.any fun (key, _) => + sourceAnnotationKey.isPrefixOf key || Ix.SemanticContract.key.isPrefixOf key + | _ => false).isSome + let mut selected : Std.HashSet Lean.Name := {} + for (name, source) in constants do + if name != source.name then + throw (toString <| SourceContractError.declarationNameMismatch name source.name) + if selected.contains name then + throw (toString <| SourceContractError.duplicateDeclaration name) + selected := selected.insert name + if registered name || hasContracts source.type || + ((sourceBody? source).map hasContracts).getD false then return false + if let .recInfo info := source then + if info.rules.any (hasContracts ·.rhs) then return false + return true + def prepareSourceConstants (constants : List (Lean.Name × Lean.ConstantInfo)) : Except String (List (Lean.Name × Lean.ConstantInfo)) := do + if ← checkOrdinaryConstants constants (fun _ => false) then return constants let input ← (CompileInput.fromAnnotations constants).mapError toString input.prepare def prepareRegisteredConstants (env : Lean.Environment) (constants : List (Lean.Name × Lean.ConstantInfo)) : Except String (List (Lean.Name × Lean.ConstantInfo)) := do + let registry := sourceContractExtension.getState env + let hints := sourceMeasureExtension.getState env + if ← checkOrdinaryConstants constants (fun name => registry.contains name || hints.contains name) then + return constants let input ← (compileInputFromEnv env constants).mapError toString input.prepare diff --git a/Tests/Ix/SourceContract/Driver.lean b/Tests/Ix/SourceContract/Driver.lean index 8a2af8c6d..f412920dd 100644 --- a/Tests/Ix/SourceContract/Driver.lean +++ b/Tests/Ix/SourceContract/Driver.lean @@ -33,6 +33,25 @@ private def unsupported (result : Except String α) : Bool := | .ok _ => false def suite : List TestSeq := [ + ioTest "ordinary source preflight preserves declarations and validates names" do + let env ← Lean.mkEmptyEnvironment + let sources := constants plainSource + for prepare in [prepareSourceConstants, prepareRegisteredConstants env] do + if (prepare sources).toOption != some sources then return false + if (prepare (sources ++ sources)).toOption.isSome then return false + if (prepare [(`wrongName, plainSource)]).toOption.isSome then return false + return true, + ioTest "ordinary source preflight cannot bypass reserved semantic metadata" do + let env ← Lean.mkEmptyEnvironment + let source : ConstantInfo := .axiomInfo { + name := plainSource.name, levelParams := [] + type := .mdata (({} : Lean.MData).setNat `ix.contract.unknown 1) plainSource.type + isUnsafe := false } + for prepare in [prepareSourceConstants, prepareRegisteredConstants env] do + if (prepare (constants source)).toOption.isSome then return false + let .ok marked := prepare (constants markedSource) | return false + if marked == constants markedSource then return false + return true, ioTest "Lean constant-list driver rejects an unadmitted annotated axiom" do return unsupported (← compileLeanConsts (constants markedSource) (numWorkers := 1)), ioTest "explicit Lean input rejects a missing annotation registry" do @@ -72,4 +91,3 @@ def suite : List TestSeq := [ end Tests.Ix.SourceContract.Driver end - diff --git a/crates/compile/src/compile/env.rs b/crates/compile/src/compile/env.rs index 2f3146f09..604b3187f 100644 --- a/crates/compile/src/compile/env.rs +++ b/crates/compile/src/compile/env.rs @@ -157,20 +157,13 @@ pub fn compile_env_with_profile( profile: Option<&ixon::resource::addressed::Profile>, ) -> Result { let _memory_sampler = crate::diag::memory_sampler("compile_env"); - let mut semantic_sources = Vec::new(); - for name in lean_env.keys() { - if let Some(c) = lean_env.get(name) - && crate::semantic_contract::inspect_constant(&c)? - { - semantic_sources.push(name.clone()); - } - } let setup_start = Instant::now(); // Whole-env scan: ref graph + immediate groundedness + inductive // groups in one decode per constant — the env decodes lazily, so // each additional full sweep would decode every constant again. let phase_start = Instant::now(); let scan = setup_scan(lean_env.as_ref()); + let semantic_sources = scan.semantic_sources?; if let Some(name) = scan.source_contracts.iter().min_by_key(|name| name.pretty()) { diff --git a/crates/compile/src/graph.rs b/crates/compile/src/graph.rs index d700ef69d..a95fb7542 100644 --- a/crates/compile/src/graph.rs +++ b/crates/compile/src/graph.rs @@ -57,6 +57,8 @@ pub struct SetupScan { pub ind_groups: FxHashMap>, /// Source contracts that the current conservative emitter cannot preserve. pub source_contracts: Vec, + /// Semantic declarations validated during the same lazy decode as the graph. + pub semantic_sources: Result, ixon::CompileError>, } /// Fused whole-env setup pass: one decode per constant feeding the ref @@ -78,6 +80,8 @@ pub fn setup_scan(env: &Env) -> SetupScan { ungrounded: FxHashMap, ind_groups: FxHashMap>, source_contracts: Vec, + semantic_sources: Vec, + semantic_error: Option, } let names: Vec<&Name> = env.keys().collect(); @@ -87,6 +91,11 @@ pub fn setup_scan(env: &Env) -> SetupScan { let Some(constant) = env.get(name) else { return acc; }; + match crate::semantic_contract::inspect_constant(&constant) { + Ok(true) => acc.semantic_sources.push(name.clone()), + Ok(false) => {}, + Err(error) => acc.semantic_error = Some(error), + } let (deps, annotated) = inspect_constant_references(&constant); if annotated { acc.source_contracts.push(name.clone()); @@ -117,6 +126,8 @@ pub fn setup_scan(env: &Env) -> SetupScan { l.in_refs = merge_ref_maps(l.in_refs, r.in_refs); l.ungrounded.extend(r.ungrounded); l.source_contracts.extend(r.source_contracts); + l.semantic_sources.extend(r.semantic_sources); + l.semantic_error = l.semantic_error.or(r.semantic_error); for (k, v) in r.ind_groups { l.ind_groups.entry(k).or_insert(v); } @@ -128,6 +139,10 @@ pub fn setup_scan(env: &Env) -> SetupScan { immediate_ungrounded: acc.ungrounded, ind_groups: acc.ind_groups, source_contracts: acc.source_contracts, + semantic_sources: match acc.semantic_error { + Some(error) => Err(error), + None => Ok(acc.semantic_sources), + }, } } @@ -426,6 +441,40 @@ mod tests { assert_eq!(setup_scan(&env).source_contracts, vec![name]); } + #[test] + fn setup_scan_preserves_semantic_validation() { + use crate::semantic_contract::{Contract, Kind}; + use ixon::contract::{BinderContract, LetKind, ValueContract}; + let contract = Contract { + kind: Kind::All, + binder: BinderContract::default(), + result: ValueContract::shared(), + let_kind: LetKind::Value, + }; + let name = n("Semantic"); + let mut env = Env::default(); + let axiom = |typ| { + ConstantInfo::AxiomInfo(AxiomVal { + cnst: ConstantVal { name: name.clone(), level_params: vec![], typ }, + is_unsafe: false, + }) + }; + env.insert( + name.clone(), + axiom(contract.attach(Expr::all( + n("x"), + sort0(), + sort0(), + BinderInfo::Default, + ))), + ); + assert_eq!(setup_scan(&env).semantic_sources.unwrap(), vec![name.clone()]); + // A well-formed frame attached to the wrong expression must still fail + // before compilation, even though validation now shares the graph decode. + env.insert(name.clone(), axiom(contract.attach(sort0()))); + assert!(setup_scan(&env).semantic_sources.is_err()); + } + #[test] fn source_contract_guard_preserves_native_borrow_metadata() { use crate::compile::{CompileOptions, compile_env_with_options}; @@ -467,6 +516,7 @@ mod tests { immediate_ungrounded: FxHashMap::default(), ind_groups: FxHashMap::default(), source_contracts: Vec::new(), + semantic_sources: Ok(Vec::new()), }; let names: Vec<_> = env.keys().collect(); names From 2151772712c596dd84b2cadfc37b1607471e1143 Mon Sep 17 00:00:00 2001 From: "J. C. Burnham" Date: Thu, 17 Sep 2026 16:37:04 -0400 Subject: [PATCH 2/3] perf(kernel): admit definition dependencies at Ixon ingress --- crates/ffi/examples/check_anon_subject.rs | 31 +-- crates/ffi/src/kernel.rs | 43 ++--- crates/ixon/src/lazy.rs | 28 +++ crates/kernel/src/anon_work.rs | 2 +- crates/kernel/src/check.rs | 6 + crates/kernel/src/ingress.rs | 123 ++++++++++-- crates/kernel/src/ixon_checker.rs | 220 ++++++++++++++++++++++ crates/kernel/src/lib.rs | 1 + crates/kernel/src/resource.rs | 12 +- crates/kernel/src/tc.rs | 4 + docs/kernel_identity.md | 22 +++ sp1/guest/src/main.rs | 9 +- zisk/guest/src/main.rs | 24 ++- 13 files changed, 439 insertions(+), 86 deletions(-) create mode 100644 crates/kernel/src/ixon_checker.rs diff --git a/crates/ffi/examples/check_anon_subject.rs b/crates/ffi/examples/check_anon_subject.rs index 39e6eccc8..7e9f41e75 100644 --- a/crates/ffi/examples/check_anon_subject.rs +++ b/crates/ffi/examples/check_anon_subject.rs @@ -33,10 +33,7 @@ use std::{ use ix_common::address::Address; use ix_kernel::{ anon_work::{AnonWorkItem, build_anon_work}, - env::KEnv, - id::KId, - mode::Anon, - tc::TypeChecker, + ixon_checker::IxonChecker, }; use ixon::env::Env; @@ -132,45 +129,37 @@ fn check(path: &str, primary: &Address) -> Result { ix_kernel::tc::max_rec_fuel(), start.elapsed().as_secs_f64() ); - let mut kenv = KEnv::::new(); + let mut checker = IxonChecker::new(&env); + checker.set_debug_label(format!("#{}", primary.hex())); let _ = ix_kernel::profile::take_op_counts(); ix_kernel::perf::same_head::reset(); let start = Instant::now(); - let (result, last_member_fuel, peak_def_eq_depth, hot_misses) = { - let mut tc = TypeChecker::new_with_lazy_anon(&mut kenv, &env); - tc.set_debug_label(format!("#{}", primary.hex())); - let result = tc.check_const(&KId::new(primary.clone(), ())); - let fuel = tc.fuel_used(); - let peak = tc.def_eq_peak; - // TypeChecker has no Drop accounting. Flush the final member explicitly, - // after capturing its allowance and before discarding the checker. - tc.finish_constant_accounting(); - (result, fuel, peak, tc.hot_miss_summary()) - }; + let result = checker.check_const(primary); + let stats = checker.last_check(); let check_secs = start.elapsed().as_secs_f64(); let ops = ix_kernel::profile::take_op_counts(); let aggregate_fuel = ix_kernel::perf::enabled() - .then(|| kenv.perf.total_rec_fuel_used.load(Ordering::Relaxed)); + .then(|| checker.perf().total_rec_fuel_used.load(Ordering::Relaxed)); let report = serde_json::json!({ "primary": primary.hex(), "scope": "subject-only", "targets": targets, "passed": result.is_ok(), "error": result.as_ref().err().map(ToString::to_string), "load_secs": load_secs, "check_secs": check_secs, "fuel_cap_per_member": ix_kernel::tc::max_rec_fuel(), - "last_member_fuel": last_member_fuel, + "last_member_fuel": stats.fuel_used, // Null unless IX_PERF_COUNTERS is enabled; do not label the final member's // budget as the total fuel of a multi-member work item. - "aggregate_fuel": aggregate_fuel, "last_member_def_eq_peak": peak_def_eq_depth, + "aggregate_fuel": aggregate_fuel, "last_member_def_eq_peak": stats.def_eq_peak, "subst": ops.subst_nodes, "whnf": ops.whnf_calls, "def_eq": ops.def_eq_calls, "intern": ops.intern_nodes, "nat_arith": ops.nat_arith, }); println!("{report}"); - eprint!("{hot_misses}"); + eprint!("{}", stats.hot_misses); eprint!("{}", ix_kernel::perf::same_head::summary()); if ix_kernel::perf::enabled() { // The example does not install a log backend, so KEnv's log::info! // drop summary would otherwise be invisible. No checker work is rerun. - eprint!("{}", kenv.perf.summary()); + eprint!("{}", checker.perf().summary()); } if ix_kernel::perf::reduce_histo_enabled() { print_reductions( diff --git a/crates/ffi/src/kernel.rs b/crates/ffi/src/kernel.rs index 1f98b5581..0be6e2515 100644 --- a/crates/ffi/src/kernel.rs +++ b/crates/ffi/src/kernel.rs @@ -61,6 +61,7 @@ use ix_compile::decompile::decompile_env; use ix_compile::kernel_egress::{ixon_egress, lean_egress}; use ix_kernel::env::KEnv; use ix_kernel::error::TcError; +#[cfg(feature = "test-ffi")] use ix_kernel::id::KId; use ix_kernel::ingress::{ IxonIngressLookups, build_ixon_ingress_lookups, @@ -68,7 +69,7 @@ use ix_kernel::ingress::{ }; #[cfg(feature = "test-ffi")] use ix_kernel::ingress::{ixon_ingress, lean_ingress}; -use ix_kernel::mode::{Anon, CheckDupLevelParams, KernelMode, Meta}; +use ix_kernel::mode::{CheckDupLevelParams, KernelMode, Meta}; use ix_kernel::profile::{BlockProfile, OpCounts, ProfileBuilder, ProfileSink}; use ix_kernel::tc::TypeChecker; use ixon::constant::ConstantInfo as IxonCI; @@ -1331,7 +1332,7 @@ fn resolve_kernel_check_workers_from( // Companion to `run_checks_parallel_on_large_stacks` for the metadata-free // anon path. Iterates `env.consts` exactly once to enumerate work items // (block or standalone), then dispatches to workers each running -// `TypeChecker::::new_with_lazy_anon` against its own `KEnv`. +// `IxonChecker` owns each worker's kernel state and lazy Ixon ingress. // The lazy ingress mechanism (in `tc.rs`) handles cross-block faults // without consulting metadata. @@ -1461,7 +1462,7 @@ fn run_anon_checks_parallel( .name(format!("ix-kernel-check-anon-{worker_idx}")) .stack_size(KERNEL_CHECK_STACK_SIZE) .spawn(move || { - let mut kenv = KEnv::::new(); + let mut checker = ix_kernel::ixon_checker::IxonChecker::new(&env); let clear_every = kernel_check_clear_every(); let mut checks_since_clear = clear_every; loop { @@ -1472,9 +1473,9 @@ fn run_anon_checks_parallel( let item = &work[work_idx]; if checks_since_clear >= clear_every { if retain_capacity == 0 { - kenv.clear_releasing_memory(); + checker.clear_releasing_memory(); } else { - kenv.clear_with_capacity_limit(retain_capacity); + checker.clear_with_capacity_limit(retain_capacity); } checks_since_clear = 0; } @@ -1491,18 +1492,13 @@ fn run_anon_checks_parallel( progress_worker.begin(worker_idx, &prefix); let tc_start = Instant::now(); - let kid = KId::::new(primary_addr.clone(), ()); if record_per_const { // Reset this worker's op counters so the post-check read // attributes exactly this item (incl. TC setup + lazy ingress). let _ = ix_kernel::profile::take_op_counts(); } - let (check_res, item_fuel) = { - let mut tc = - TypeChecker::::new_with_lazy_anon(&mut kenv, &env); - let res = tc.check_const(&kid); - (res, tc.fuel_used()) - }; + let check_res = checker.check_const(&primary_addr); + let item_fuel = checker.last_check().fuel_used; let elapsed = tc_start.elapsed(); if record_per_const { let ops = ix_kernel::profile::take_op_counts(); @@ -1635,8 +1631,7 @@ fn run_anon_checks_parallel( /// projection constants (`IPrj`/`CPrj`/`RPrj`/`DPrj`); Muts blocks /// become block work items whose member + ctor projection addresses /// are reconstructed deterministically via `Constant::commit`. -/// - Workers each get their own `KEnv` and a -/// `LazyAnonIngress`-backed `TypeChecker`. Deep refs fault in +/// - Workers each get their own `IxonChecker`. Deep refs fault in /// lazily via the anon-mode shallow ingress (`ingress_anon_addr_shallow`). /// - Returns `Array (Option CheckError)`, one slot per kernel-checkable /// address discovered during enumeration. @@ -2811,8 +2806,8 @@ fn run_anon_profile_parallel( .name(format!("ix-kernel-profile-{worker_idx}")) .stack_size(KERNEL_CHECK_STACK_SIZE) .spawn(move || { - let mut kenv = KEnv::::new(); - kenv.profile_sink = Some(ProfileSink::new(isolate)); + let mut checker = ix_kernel::ixon_checker::IxonChecker::new(&env); + checker.set_profile_sink(ProfileSink::new(isolate)); let clear_every = kernel_check_clear_every(); let mut checks_since_clear = clear_every; loop { @@ -2823,24 +2818,14 @@ fn run_anon_profile_parallel( // `clear_releasing_memory` preserves `profile_sink`, so recording // accumulates across scheduled-block boundaries. if checks_since_clear >= clear_every { - kenv.clear_releasing_memory(); + checker.clear_releasing_memory(); checks_since_clear = 0; } let primary_addr = match &work[work_idx] { AnonWorkItem::Standalone { addr, .. } => addr.clone(), AnonWorkItem::Block { primary_addr, .. } => primary_addr.clone(), }; - let kid = KId::::new(primary_addr, ()); - let res = { - let mut tc = - TypeChecker::::new_with_lazy_anon(&mut kenv, &env); - let r = tc.check_const(&kid); - // The TypeChecker is recreated per work item, so the final - // constant's record would never be flushed by a trailing reset — - // flush it explicitly. - tc.finish_constant_accounting(); - r - }; + let res = checker.check_const(&primary_addr); if res.is_ok() { passed.fetch_add(1, Ordering::Relaxed); } else { @@ -2848,7 +2833,7 @@ fn run_anon_profile_parallel( } checks_since_clear += 1; } - if let Some(sink) = kenv.profile_sink.take() { + if let Some(sink) = checker.take_profile_sink() { sinks.lock().unwrap().push(sink); } }) diff --git a/crates/ixon/src/lazy.rs b/crates/ixon/src/lazy.rs index 15409a739..a50822af1 100644 --- a/crates/ixon/src/lazy.rs +++ b/crates/ixon/src/lazy.rs @@ -242,6 +242,21 @@ impl LazyConstant { Ok(Arc::new(parsed)) } + /// Materialize at an explicitly verified content address. Loaded entries + /// reuse the deferred check; in-memory entries must also bind their bytes + /// to the map key before kernel ingress may trust the block graph. + pub fn get_at(&self, expected: &Address) -> Result, String> { + if self.pending_addr.as_ref() != Some(expected) + && !self.verify_address(expected) + { + return Err(format!( + "LazyConstant::get_at: bytes do not match {}", + expected.hex() + )); + } + self.get() + } + /// Identify the `ConstantInfo` variant by reading just the outer /// `Tag4` head byte — no allocation, no body parse. /// @@ -336,6 +351,19 @@ mod tests { use crate::expr::Expr; use ix_common::env::DefinitionSafety; + #[test] + fn explicit_address_check_does_not_reuse_another_keys_verdict() { + let c = axiom_constant(); + let mut bytes = Vec::new(); + c.put(&mut bytes); + let addr = Address::hash(&bytes); + let lazy = LazyConstant::from_bytes_deferred(bytes.into(), addr.clone()); + lazy.get_at(&addr).unwrap(); + assert!(lazy.was_verified()); + assert!(lazy.get_at(&Address::hash(b"another key")).is_err()); + lazy.get_at(&addr).unwrap(); + } + fn axiom_constant() -> Constant { Constant::new(ConstantInfo::Axio(Axiom { is_unsafe: false, diff --git a/crates/kernel/src/anon_work.rs b/crates/kernel/src/anon_work.rs index 138aacbc1..2451e76fb 100644 --- a/crates/kernel/src/anon_work.rs +++ b/crates/kernel/src/anon_work.rs @@ -8,7 +8,7 @@ //! typechecking: it matches `rs_kernel_check_anon` in //! `crates/ffi/src/kernel.rs` and is what an Aiur-style verifier //! commits to. Callers iterate the returned `Vec` and -//! invoke `TypeChecker::check_const` on each item's `primary` address; +//! invoke `IxonChecker::check_const` on each item's `primary` address; //! the kernel's internal block coordination handles checking every //! member + ctor of `Block` items. //! diff --git a/crates/kernel/src/check.rs b/crates/kernel/src/check.rs index bfd5e2916..2f53702d4 100644 --- a/crates/kernel/src/check.rs +++ b/crates/kernel/src/check.rs @@ -729,6 +729,12 @@ impl TypeChecker<'_, M> { &mut self, c: &KConst, ) -> Result<(), TcError> { + // Ixon ingress admits all local Rec edges before publishing a block. + // External references are content addressed and cannot form back edges. + // The full traversal remains necessary for arbitrary, mutable raw KEnvs. + if self.ixon_ingress { + return Ok(()); + } if !matches!(c, KConst::Defn { safety: DefinitionSafety::Safe, .. }) { return Ok(()); } diff --git a/crates/kernel/src/ingress.rs b/crates/kernel/src/ingress.rs index 7c69562d6..07ab1203a 100644 --- a/crates/kernel/src/ingress.rs +++ b/crates/kernel/src/ingress.rs @@ -5,7 +5,7 @@ //! universe params and optional metadata). Uses iterative stack-based traversal //! to avoid stack overflow on deeply nested expressions. -use std::cell::Cell; +use std::cell::{Cell, RefCell}; #[cfg(not(target_arch = "riscv64"))] use std::hash::{BuildHasher, Hash}; use std::sync::Arc; @@ -23,7 +23,6 @@ use bignat::Nat; use ix_common::address::Address; #[cfg(not(target_arch = "riscv64"))] use ix_common::env::ConstantInfo as LeanCI; -#[cfg(not(target_arch = "riscv64"))] use ix_common::env::DefinitionSafety; #[cfg(not(target_arch = "riscv64"))] use ix_common::env::Env as LeanEnv; @@ -59,6 +58,8 @@ struct Ctx<'a, M: KernelMode> { univs: &'a [Arc], /// ZIds of mutual block members (for resolving `Expr::Rec`). mut_ctx: Vec>, + /// Rec edges for the definition currently being admitted. + local_refs: Option<&'a RefCell>>, arena: &'a ExprMeta, names: &'a FxHashMap, lvls: Vec, @@ -970,6 +971,9 @@ fn ingress_expr( ) .ok_or_else(|| format!("invalid Rec index {rec_idx}"))? .clone(); + if let Some(refs) = ctx.local_refs { + refs.borrow_mut().insert(mid.addr.clone()); + } let univs = ingress_univ_args(univ_idxs, ctx, intern, univ_cache, stats)?; let decor: M::MField> = @@ -1121,6 +1125,9 @@ fn ingress_expr( format!("CallSite head: invalid Rec index {rec_idx}") })? .clone(); + if let Some(refs) = ctx.local_refs { + refs.borrow_mut().insert(mid.addr.clone()); + } let univs = ingress_univ_args( univ_idxs, ctx, intern, univ_cache, stats, )?; @@ -1587,6 +1594,7 @@ fn ingress_defn( // projection addresses; passing `Some(_)` skips the metadata-derived // `build_mut_ctx` call. Meta callers pass `None`. mut_ctx_override: Option>>, + local_dependencies: Option<&mut LocalDefnDependencies>, ) -> Result, KConst)>, String> { let mut cache: ExprCache = FxHashMap::default(); let mut univ_cache: UnivCache = FxHashMap::default(); @@ -1598,6 +1606,7 @@ fn ingress_defn( .get(&self_id.addr) .map_or(ReducibilityHints::Regular(0), |r| *r); let safety = def.safety; + let local_refs = RefCell::new(FxHashSet::default()); let (level_params, arena, type_root, value_root, all_addrs) = match &meta.info { ConstantMetaInfo::Def { @@ -1626,6 +1635,7 @@ fn ingress_defn( lvls: level_params.clone(), univ_patches: univ_patch_map(meta), meta_univs: &meta.meta_univs, + local_refs: local_dependencies.as_ref().map(|_| &local_refs), synth_counter: Cell::new(0), }; @@ -1659,6 +1669,10 @@ fn ingress_defn( names, ); + if let Some(dependencies) = local_dependencies { + dependencies.insert(&self_id.addr, def.safety, local_refs.into_inner()); + } + Ok(vec![( self_id, KConst::Defn { @@ -1731,6 +1745,7 @@ fn ingress_recursor( lvls: level_params.clone(), univ_patches: univ_patch_map(meta), meta_univs: &meta.meta_univs, + local_refs: None, synth_counter: Cell::new(0), }; @@ -1836,6 +1851,7 @@ fn ingress_standalone( intern, stats, None, + None, ), IxonCI::Axio(ax) => { @@ -1857,6 +1873,7 @@ fn ingress_standalone( lvls: level_params.clone(), univ_patches: univ_patch_map(meta), meta_univs: &meta.meta_univs, + local_refs: None, synth_counter: Cell::new(0), }; let typ = ingress_expr( @@ -1907,6 +1924,7 @@ fn ingress_standalone( lvls: level_params.clone(), univ_patches: univ_patch_map(meta), meta_univs: &meta.meta_univs, + local_refs: None, synth_counter: Cell::new(0), }; let typ = ingress_expr( @@ -2006,6 +2024,7 @@ fn ingress_muts_inductive( lvls: level_params.clone(), univ_patches: univ_patch_map(meta), meta_univs: &meta.meta_univs, + local_refs: None, synth_counter: Cell::new(0), }; @@ -2107,6 +2126,7 @@ fn ingress_muts_inductive( // own `meta_univs` (canonicity §10.6). univ_patches: univ_patch_map(&ctor_named_meta), meta_univs: &ctor_named_meta.meta_univs, + local_refs: None, synth_counter: Cell::new(0), }; let mut ctor_univ_cache: UnivCache = FxHashMap::default(); @@ -2242,6 +2262,7 @@ fn ingress_muts_block( intern, stats, None, + None, )?); }, } @@ -4387,6 +4408,72 @@ fn validate_no_reserved_marker_addresses( use crate::mode::Anon; +/// Fetch a constant with an explicit binding to its map key, including sources +/// assembled in memory rather than loaded with deferred address verification. +fn anon_constant( + env: &IxonEnv, + addr: &Address, +) -> Result>, String> { + env.consts.get(addr).map(|entry| entry.get_at(addr)).transpose() +} + +/// A content-addressed file cannot encode a cycle between distinct blocks +/// without a hash preimage. Rec slots are the only local back edges. Gather +/// them during conversion and check the block before publishing any members. +#[derive(Default)] +struct LocalDefnDependencies { + edges: FxHashMap>, + safe: Vec
, +} + +impl LocalDefnDependencies { + fn insert( + &mut self, + addr: &Address, + safety: DefinitionSafety, + refs: FxHashSet
, + ) { + // Most declarations have no Rec nodes: keep their admission allocation-free. + if refs.is_empty() { + return; + } + if safety == DefinitionSafety::Safe { + self.safe.push(addr.clone()); + } + self.edges.insert(addr.clone(), refs); + } + + fn validate(&self) -> Result<(), String> { + let mut finished = FxHashSet::default(); + let mut active = FxHashSet::default(); + for root in &self.safe { + let mut pending = vec![(root, false)]; + while let Some((addr, exit)) = pending.pop() { + if exit { + active.remove(addr); + finished.insert(addr); + continue; + } + if finished.contains(addr) { + continue; + } + let Some(refs) = self.edges.get(addr) else { + continue; + }; + if !active.insert(addr) { + return Err(format!( + "cyclic definition dependency at {}", + addr.hex() + )); + } + pending.push((addr, true)); + pending.extend(refs.iter().map(|dependency| (dependency, false))); + } + } + Ok(()) + } +} + /// Verify that a projection address computed from a block's structure /// is actually present in the env's consts. Wrapped here so the four /// dispatch arms in `ingress_anon_block` (DPrj/RPrj/IPrj/CPrj) all @@ -4399,7 +4486,8 @@ fn verify_proj_addr_in_env( ctor_idx: Option, anon_env: &IxonEnv, ) -> Result<(), String> { - if anon_env.consts.contains_key(proj_addr) { + if let Some(entry) = anon_env.consts.get(proj_addr) { + entry.get_at(proj_addr)?; return Ok(()); } match ctor_idx { @@ -4482,6 +4570,7 @@ fn ingress_anon_standalone( let mut convert_stats = ConvertStats::new(false); let self_id: KId = KId::new(addr.clone(), ()); + let mut local_dependencies = LocalDefnDependencies::default(); let entries = match &constant.info { IxonCI::Defn(def) => ingress_defn::( def, @@ -4497,6 +4586,7 @@ fn ingress_anon_standalone( &mut kenv.intern, &mut convert_stats, Some(vec![self_id.clone()]), + Some(&mut local_dependencies), )?, IxonCI::Recr(rec) => ingress_recursor::( rec, @@ -4525,6 +4615,7 @@ fn ingress_anon_standalone( &mut convert_stats, )?, }; + local_dependencies.validate()?; insert_standalone_entries(kenv, entries); Ok(self_id) } @@ -4572,6 +4663,7 @@ fn ingress_anon_inductive( // metadata-blind), so no patches are threaded here. univ_patches: FxHashMap::default(), meta_univs: &[], + local_refs: None, synth_counter: Cell::new(0), }; @@ -4620,6 +4712,7 @@ fn ingress_anon_inductive( lvls: Vec::new(), univ_patches: FxHashMap::default(), meta_univs: &[], + local_refs: None, synth_counter: Cell::new(0), }; let mut ctor_univ_cache: UnivCache = FxHashMap::default(); @@ -4700,6 +4793,7 @@ pub fn ingress_anon_block( }) .collect(); + let mut local_dependencies = LocalDefnDependencies::default(); let mut all_entries: Vec<(KId, KConst)> = Vec::new(); let mut member_kids: Vec> = Vec::with_capacity(members.len()); @@ -4728,6 +4822,7 @@ pub fn ingress_anon_block( &mut kenv.intern, &mut convert_stats, Some(mut_ctx.clone()), + Some(&mut local_dependencies), )?; all_entries.extend(entries); }, @@ -4794,6 +4889,7 @@ pub fn ingress_anon_block( } } + local_dependencies.validate()?; insert_muts_entries(kenv, all_entries); Ok(member_kids) } @@ -4809,7 +4905,7 @@ pub fn ingress_anon_addr_shallow( anon_env: &IxonEnv, addr: &Address, ) -> Result { - let Some(constant) = anon_env.get_const(addr) else { + let Some(constant) = anon_constant(anon_env, addr)? else { return Ok(false); }; @@ -4839,13 +4935,14 @@ pub fn ingress_anon_addr_shallow( if kenv.blocks.contains_key(&block_kid) { return Ok(true); } - let block_const = anon_env.get_const(&block_addr).ok_or_else(|| { - format!( - "ingress_anon_addr_shallow: block {} (parent of {}) absent", - block_addr.hex(), - addr.hex() - ) - })?; + let block_const = + anon_constant(anon_env, &block_addr)?.ok_or_else(|| { + format!( + "ingress_anon_addr_shallow: block {} (parent of {}) absent", + block_addr.hex(), + addr.hex() + ) + })?; ingress_anon_block(kenv, anon_env, &block_const, &block_addr)?; return Ok(true); } @@ -5393,6 +5490,7 @@ mod tests { lvls: vec![], univ_patches: FxHashMap::default(), meta_univs: &[], + local_refs: None, synth_counter: Cell::new(0), }; let ixon_env = IxonEnv::new(); @@ -5458,6 +5556,7 @@ mod tests { lvls: vec![mk_name("u"), mk_name("v")], univ_patches, meta_univs: &meta_univs, + local_refs: None, synth_counter: Cell::new(0), }; let mut intern = InternTable::::new(); @@ -5517,6 +5616,7 @@ mod tests { lvls: vec![mk_name("u"), mk_name("v")], univ_patches: FxHashMap::default(), meta_univs: &[], + local_refs: None, synth_counter: Cell::new(0), }; let mut intern = InternTable::::new(); @@ -5587,6 +5687,7 @@ mod tests { lvls: vec![mk_name("u"), mk_name("v")], univ_patches, meta_univs: &meta_univs, + local_refs: None, synth_counter: Cell::new(0), }; let mut intern = InternTable::::new(); diff --git a/crates/kernel/src/ixon_checker.rs b/crates/kernel/src/ixon_checker.rs new file mode 100644 index 000000000..b369d7488 --- /dev/null +++ b/crates/kernel/src/ixon_checker.rs @@ -0,0 +1,220 @@ +//! Checking boundary for decoded Ixon environments. +//! +//! Callers decode .ixe bytes with Ixon before constructing this checker. +//! +//! The worker environment is private: every declaration enters through the +//! kernel's address-verified ingress, which checks local definition cycles +//! before admitting a block. External dependencies are Ixon content +//! addresses, so checking a declaration need not rewalk their expression trees. +//! As with `TypeChecker::check_const`, referenced declarations are assumptions; +//! check every work item to certify a complete environment. + +use ix_common::address::Address; +use ixon::env::Env; + +use crate::env::KEnv; +use crate::error::TcError; +use crate::id::KId; +use crate::mode::Anon; +use crate::profile::ProfileSink; +use crate::tc::TypeChecker; + +/// Diagnostics for the final member of the most recent block check. +#[derive(Default)] +pub struct CheckStats { + pub fuel_used: u64, + pub def_eq_peak: u32, + pub hot_misses: String, +} + +/// A worker whose kernel declarations come exclusively from Ixon ingress. +pub struct IxonChecker<'a> { + source: &'a Env, + kernel: KEnv, + last_check: CheckStats, + debug_label: Option, +} + +impl<'a> IxonChecker<'a> { + pub fn new(source: &'a Env) -> Self { + Self { + source, + kernel: KEnv::new(), + last_check: CheckStats::default(), + debug_label: None, + } + } + + /// Check one standalone declaration or the whole block containing `addr`. + pub fn check_const(&mut self, addr: &Address) -> Result<(), TcError> { + let mut checker = + TypeChecker::new_with_lazy_anon(&mut self.kernel, self.source); + checker.ixon_ingress = true; + if let Some(label) = &self.debug_label { + checker.set_debug_label(label.clone()); + } + let result = checker.check_const(&KId::new(addr.clone(), ())); + self.last_check = CheckStats { + fuel_used: checker.fuel_used(), + def_eq_peak: checker.def_eq_peak, + hot_misses: checker.hot_miss_summary(), + }; + checker.finish_constant_accounting(); + result + } + + pub fn last_check(&self) -> &CheckStats { + &self.last_check + } + + pub fn set_debug_label(&mut self, label: String) { + self.debug_label = Some(label); + } + + pub fn perf(&self) -> &crate::perf::PerfCounters { + &self.kernel.perf + } + + pub fn clear_releasing_memory(&mut self) { + self.kernel.clear_releasing_memory(); + } + + pub fn clear_with_capacity_limit(&mut self, max_capacity: usize) { + self.kernel.clear_with_capacity_limit(max_capacity); + } + + pub fn clear_reduction_caches(&mut self) { + self.kernel.clear_reduction_caches(); + } + + pub fn set_profile_sink(&mut self, sink: ProfileSink) { + self.kernel.profile_sink = Some(sink); + } + + pub fn take_profile_sink(&mut self) -> Option { + self.kernel.profile_sink.take() + } +} + +#[cfg(test)] +mod tests { + use super::*; + use ix_common::env::DefinitionSafety; + use ixon::constant::{ + Constant, ConstantInfo, DefKind, Definition, MutConst, defn_proj_constant, + }; + use ixon::expr::Expr; + use ixon::univ::Univ; + use std::sync::Arc; + + fn definition(value: Expr) -> Definition { + Definition { + kind: DefKind::Definition, + safety: DefinitionSafety::Safe, + lvls: 0, + typ: Arc::new(Expr::Sort(1)), + value: Arc::new(value), + } + } + + fn store(env: &Env, constant: Constant) -> Address { + let addr = constant.commit().0; + env.store_const(addr.clone(), constant); + addr + } + + fn sorts(constant: &mut Constant) { + constant.univs = vec![Univ::zero(), Univ::succ(Univ::zero())]; + } + + fn loaded(env: &Env) -> Env { + let mut bytes = Vec::new(); + env.put(&mut bytes).unwrap(); + Env::get_anon(&mut bytes.as_slice()).unwrap() + } + + #[test] + fn ixon_check_keeps_external_dependencies_lazy() { + let env = Env::new(); + let mut base = Constant::new(ConstantInfo::Defn(definition(Expr::Sort(0)))); + sorts(&mut base); + let mut addr = store(&env, base); + for _ in 0..1024 { + let mut c = + Constant::new(ConstantInfo::Defn(definition(Expr::Ref(0, vec![])))); + sorts(&mut c); + c.refs.push(addr); + addr = store(&env, c); + } + let source = loaded(&env); + let mut checker = IxonChecker::new(&source); + checker.check_const(&addr).unwrap(); + // Only the root and its direct reference's type are needed. Regressing + // to a closure walk would materialize all 1025 declarations here. + assert_eq!(checker.kernel.consts.len(), 2); + } + + #[test] + fn ixon_admission_rejects_local_cycles_atomically() { + for cyclic in [false, true] { + let env = Env::new(); + let mut block = Constant::new(ConstantInfo::Muts(vec![ + MutConst::Defn(definition(Expr::Rec(1, vec![]))), + MutConst::Defn(definition(if cyclic { + Expr::Rec(0, vec![]) + } else { + Expr::Sort(0) + })), + ])); + sorts(&mut block); + let block_addr = store(&env, block); + let first = store(&env, defn_proj_constant(0, block_addr.clone())); + store(&env, defn_proj_constant(1, block_addr)); + let source = loaded(&env); + let mut checker = IxonChecker::new(&source); + let result = checker.check_const(&first); + if cyclic { + assert!( + result + .unwrap_err() + .to_string() + .contains("cyclic definition dependency") + ); + assert!(checker.kernel.consts.is_empty()); + assert!(checker.kernel.blocks.is_empty()); + } else { + result.unwrap(); + } + } + } + + #[test] + fn ixon_admission_verifies_in_memory_address_bindings() { + let source = Env::new(); + let mut c = Constant::new(ConstantInfo::Defn(definition(Expr::Sort(0)))); + sorts(&mut c); + let addr = Address::hash(b"wrong map key"); + source.store_const(addr.clone(), c); + assert!(IxonChecker::new(&source).check_const(&addr).is_err()); + } + + #[test] + fn ixon_admission_verifies_every_projection_before_publishing_a_block() { + let source = Env::new(); + let mut block = Constant::new(ConstantInfo::Muts(vec![ + MutConst::Defn(definition(Expr::Sort(0))), + MutConst::Defn(definition(Expr::Sort(0))), + ])); + sorts(&mut block); + let block_addr = store(&source, block); + let first = store(&source, defn_proj_constant(0, block_addr.clone())); + let sibling = defn_proj_constant(1, block_addr.clone()).commit().0; + // The requested projection and block are valid. Its sibling's bytes lie + // about the index, and must not be hidden by ingress of the whole block. + source.store_const(sibling, defn_proj_constant(0, block_addr)); + let source = loaded(&source); + let mut checker = IxonChecker::new(&source); + assert!(checker.check_const(&first).is_err()); + assert!(checker.kernel.consts.is_empty()); + } +} diff --git a/crates/kernel/src/lib.rs b/crates/kernel/src/lib.rs index 0bffb1eb6..a4f8e864d 100644 --- a/crates/kernel/src/lib.rs +++ b/crates/kernel/src/lib.rs @@ -145,6 +145,7 @@ pub mod id; pub mod inductive; pub mod infer; pub mod ingress; +pub mod ixon_checker; pub mod lctx; pub mod level; pub mod mode; diff --git a/crates/kernel/src/resource.rs b/crates/kernel/src/resource.rs index a18d8ebe9..9f7015dca 100644 --- a/crates/kernel/src/resource.rs +++ b/crates/kernel/src/resource.rs @@ -2,10 +2,14 @@ //! Kernel typechecking on its own makes no resource promise. use crate::anon_work::build_anon_work; +#[cfg(test)] use crate::env::KEnv; +#[cfg(test)] use crate::id::KId; +#[cfg(test)] use crate::mode::Anon; use crate::primitive::PrimAddrs; +#[cfg(test)] use crate::tc::TypeChecker; use ixon::env::Env; use ixon::resource::addressed::{AddressedProgram, Profile, check_resources}; @@ -49,11 +53,9 @@ pub fn validate( check_literal_profile(profile)?; let resolved = check_resources(env, profile)?; let work = build_anon_work(env)?; - let mut kernel = KEnv::::new(); + let mut checker = crate::ixon_checker::IxonChecker::new(env); for item in work { - let id = KId { addr: item.primary().clone(), name: () }; - let mut checker = TypeChecker::new_with_lazy_anon(&mut kernel, env); - checker.check_const(&id).map_err(|error| { + checker.check_const(item.primary()).map_err(|error| { format!( "resource validator: erased typing failed at {}: {error:?}", item.primary().hex() @@ -61,7 +63,7 @@ pub fn validate( })?; // Retain structural declarations but keep reduction caches local to one // work item, as in the existing anonymous driver. - kernel.clear_reduction_caches(); + checker.clear_reduction_caches(); } Ok(resolved) } diff --git a/crates/kernel/src/tc.rs b/crates/kernel/src/tc.rs index acbff3560..0a3dcb8f9 100644 --- a/crates/kernel/src/tc.rs +++ b/crates/kernel/src/tc.rs @@ -116,6 +116,9 @@ pub struct LazyAnonIngress<'a> { pub struct TypeChecker<'a, M: KernelMode> { /// Worker-owned kernel environment (constants, caches, intern table). pub env: &'a mut KEnv, + /// Set only by the Ixon checker, whose private KEnv is populated entirely + /// by address-verified anonymous ingress with local recursion admission. + pub(crate) ixon_ingress: bool, /// Optional read-only Ixon source used to fault constants into `env` when /// typechecking discovers a missing address. lazy_ixon: Option>, @@ -227,6 +230,7 @@ impl<'a, M: KernelMode> TypeChecker<'a, M> { env, lazy_ixon: None, lazy_anon: None, + ixon_ingress: false, prims, ctx: Vec::new(), let_vals: Vec::new(), diff --git a/docs/kernel_identity.md b/docs/kernel_identity.md index a9e6e6985..a64f112c9 100644 --- a/docs/kernel_identity.md +++ b/docs/kernel_identity.md @@ -47,6 +47,28 @@ claim roots ──Merkle──▶ constant Addresses ──parse───▶ terms the kernel typechecked ``` +### Definition dependency admission + +`IxonChecker` consumes an already decoded `ixon::Env`. The path remains +`.ixe → Ixon decoding → kernel ingress → typechecking`. Each worker owns +a private `KEnv`, populated exclusively by anonymous Ixon ingress; callers +cannot insert raw declarations into it. + +Ingress verifies each constant's binding to its map key with +`LazyConstant::get_at`, including all projections admitted with a mutual +block. External dependency addresses are pinned by the constant's bytes: +constructing a cycle between blocks would require solving a hash preimage. +Local `Rec` slots need an explicit check. Ingress collects those edges while +converting definition types and values, follows shared expressions normally, +and rejects cycles reachable from safe definitions before publishing any +member of the block. Acyclic forward references remain valid. + +Consequently, checking one declaration need not traverse the expression +trees of its entire external dependency closure. Those declarations remain +assumptions until their own work items are checked, as in the proof claim +model above. Callers constructing a raw `KEnv` do not have this ingress +invariant; `TypeChecker` retains its defensive dependency traversal for them. + ## Layer 2: kernel node identity (internal, ephemeral, never serialized) Inside one checker run, the kernel needs cheap identity for the diff --git a/sp1/guest/src/main.rs b/sp1/guest/src/main.rs index 48b91c16f..b56b6cdc1 100644 --- a/sp1/guest/src/main.rs +++ b/sp1/guest/src/main.rs @@ -41,10 +41,9 @@ sp1_zkvm::entrypoint!(main); use ix_common::address::Address; use ix_kernel::anon_work::{AnonWorkItem, build_anon_work}; -use ix_kernel::env::KEnv; use ix_kernel::id::KId; use ix_kernel::ingress::ixon_ingress_owned; -use ix_kernel::mode::{Anon, Meta}; +use ix_kernel::mode::Meta; use ix_kernel::tc::TypeChecker; use ixon::env::Env as IxonEnv; use ixon::merkle::{merkle_root_canonical, zero_address}; @@ -160,14 +159,12 @@ pub fn main() { .collect() }; - let mut kenv = KEnv::::new(); let mut failures: u32 = 0; let mut checked_covered: Vec
= Vec::new(); tic!("check_const_loop"); - let mut tc = TypeChecker::::new_with_lazy_anon(&mut kenv, &env); + let mut checker = ix_kernel::ixon_checker::IxonChecker::new(&env); for item in &items_to_check { - let kid = KId::::new(item.primary().clone(), ()); - if tc.check_const(&kid).is_err() { + if checker.check_const(item.primary()).is_err() { failures = failures.saturating_add(1); } // Certify in `consts`-key space (block addr + projections) — the same diff --git a/zisk/guest/src/main.rs b/zisk/guest/src/main.rs index 080782b5c..3856a4190 100644 --- a/zisk/guest/src/main.rs +++ b/zisk/guest/src/main.rs @@ -24,11 +24,7 @@ ziskos::entrypoint!(main); use ix_common::address::Address; -use ix_kernel::anon_work::{build_anon_work, AnonWorkItem}; -use ix_kernel::env::KEnv; -use ix_kernel::id::KId; -use ix_kernel::mode::Anon; -use ix_kernel::tc::TypeChecker; +use ix_kernel::anon_work::{AnonWorkItem, build_anon_work}; use ixon::env::Env as IxonEnv; use ixon::merkle::{merkle_root_canonical, zero_address}; @@ -60,7 +56,8 @@ fn main() { // layer (content-addressed: same constant ⇒ same primary across envs). let check_slice: &[u8] = ziskos::io::read_input_slice(); - let env = IxonEnv::get_anon(&mut &env_bytes[..]).expect("invalid Ixon environment"); + let env = + IxonEnv::get_anon(&mut &env_bytes[..]).expect("invalid Ixon environment"); let work = build_anon_work(&env).expect("build_anon_work"); let total = work.len() as u32; @@ -78,19 +75,19 @@ fn main() { // `Address` orders by raw bytes, so sort + binary_search is correct. let mut want: Vec
= Address::unpack(check_slice).collect(); want.sort_unstable(); - let items: Vec<&AnonWorkItem> = - work.iter().filter(|it| want.binary_search(it.primary()).is_ok()).collect(); + let items: Vec<&AnonWorkItem> = work + .iter() + .filter(|it| want.binary_search(it.primary()).is_ok()) + .collect(); (items, 0, 0) // field_a filled in below once checked_count is known }; let reuse_mode = !check_slice.is_empty(); - let mut kenv = KEnv::::new(); let mut failures: u32 = 0; let mut checked_targets: Vec
= Vec::new(); - let mut tc = TypeChecker::::new_with_lazy_anon(&mut kenv, &env); + let mut checker = ix_kernel::ixon_checker::IxonChecker::new(&env); for item in &items_to_check { - let kid = KId::::new(item.primary().clone(), ()); - if tc.check_const(&kid).is_err() { + if checker.check_const(item.primary()).is_err() { failures = failures.saturating_add(1); } // Certify in `consts`-key space (block addr + projections), matching @@ -129,7 +126,8 @@ fn main() { for t in &checked_targets { if let Some(c) = env.get_const(t) { for r in &c.refs { - if checked_sorted.binary_search(r).is_err() && env.get_blob(r).is_none() { + if checked_sorted.binary_search(r).is_err() && env.get_blob(r).is_none() + { assumptions.push(r.clone()); } } From 6b6161d270574738c5a0ebbe8b88711e024d3e5f Mon Sep 17 00:00:00 2001 From: "J. C. Burnham" Date: Thu, 17 Sep 2026 17:04:17 -0400 Subject: [PATCH 3/3] perf(compile): parallelize source contract presence scans --- Ix/Cli/CompileCmd.lean | 2 ++ Ix/Compile/SourceContract/Transport.lean | 42 +++++++++++++++++++----- Tests/Ix/SourceContract/Driver.lean | 17 ++++++++++ 3 files changed, 52 insertions(+), 9 deletions(-) diff --git a/Ix/Cli/CompileCmd.lean b/Ix/Cli/CompileCmd.lean index 2399302db..30c4506ee 100644 --- a/Ix/Cli/CompileCmd.lean +++ b/Ix/Cli/CompileCmd.lean @@ -159,6 +159,8 @@ def runCompileCmd (p : Cli.Parsed) : IO UInt32 := do let strictAnon := p.hasFlag "anon" let start ← IO.monoMsNow let constList ← IO.ofExcept <| Ix.Compile.prepareRegisteredConstants leanEnv constList + if (← IO.getEnv "IX_VERBOSE").isSome || (← IO.getEnv "IX_COMPILE_DBG").isSome then + IO.eprintln s!"[compile] source contract preparation: {((← IO.monoMsNow) - start).formatMs}" let status ← if strictAnon then Ix.CompileM.rsCompileEnvBytesAnonFFI constList outPath allowPartial else diff --git a/Ix/Compile/SourceContract/Transport.lean b/Ix/Compile/SourceContract/Transport.lean index 0013fd9c9..f31a07fc3 100644 --- a/Ix/Compile/SourceContract/Transport.lean +++ b/Ix/Compile/SourceContract/Transport.lean @@ -102,16 +102,43 @@ def CompileInput.prepare (input : CompileInput) : let resolved ← input.resolve.mapError toString resolved.decorate +/-- Detect either reserved contract namespace, including malformed markers. +This checks presence only; resolution and validation still run for marked input. -/ +def hasContractMetadata (source : Lean.ConstantInfo) : Bool := + let hasContracts (expr : Lean.Expr) := (expr.find? fun + | .mdata data _ => data.entries.any fun (key, _) => + sourceAnnotationKey.isPrefixOf key || Ix.SemanticContract.key.isPrefixOf key + | _ => false).isSome + hasContracts source.type || ((sourceBody? source).map hasContracts).getD false || + match source with + | .recInfo info => info.rules.any (hasContracts ·.rhs) + | _ => false + +/-- Scan small inputs directly and large inputs in independent batches. -/ +def hasAnyContractMetadata + (constants : List (Lean.Name × Lean.ConstantInfo)) : Bool := Id.run do + if constants.length ≤ 1024 then + return constants.any (hasContractMetadata ·.2) + -- Presence is independent for each immutable declaration. Use bounded + -- batches on Lean's worker pool so a whole imported environment does not + -- require a serial expression scan before the parallel Rust compiler. + let mut tasks : Array (Task Bool) := #[] + let mut batch : Array Lean.ConstantInfo := Array.emptyWithCapacity 1024 + for (_, source) in constants do + batch := batch.push source + if batch.size == 1024 then + tasks := tasks.push <| Task.spawn fun _ => batch.any hasContractMetadata + batch := Array.emptyWithCapacity 1024 + if !batch.isEmpty then + tasks := tasks.push <| Task.spawn fun _ => batch.any hasContractMetadata + return tasks.any (·.get) + /-- Ordinary declarations need no occurrence resolution or decoration. Check both reserved namespaces in one shared-expression walk, retaining the input name/uniqueness checks even when there are no contracts to resolve. Any selected registration or metadata marker uses the full validation path below. -/ def checkOrdinaryConstants (constants : List (Lean.Name × Lean.ConstantInfo)) (registered : Lean.Name → Bool) : Except String Bool := do - let hasContracts (expr : Lean.Expr) := (expr.find? fun - | .mdata data _ => data.entries.any fun (key, _) => - sourceAnnotationKey.isPrefixOf key || Ix.SemanticContract.key.isPrefixOf key - | _ => false).isSome let mut selected : Std.HashSet Lean.Name := {} for (name, source) in constants do if name != source.name then @@ -119,11 +146,8 @@ def checkOrdinaryConstants (constants : List (Lean.Name × Lean.ConstantInfo)) if selected.contains name then throw (toString <| SourceContractError.duplicateDeclaration name) selected := selected.insert name - if registered name || hasContracts source.type || - ((sourceBody? source).map hasContracts).getD false then return false - if let .recInfo info := source then - if info.rules.any (hasContracts ·.rhs) then return false - return true + if registered name then return false + return !hasAnyContractMetadata constants def prepareSourceConstants (constants : List (Lean.Name × Lean.ConstantInfo)) : Except String (List (Lean.Name × Lean.ConstantInfo)) := do diff --git a/Tests/Ix/SourceContract/Driver.lean b/Tests/Ix/SourceContract/Driver.lean index f412920dd..f1f1fa49f 100644 --- a/Tests/Ix/SourceContract/Driver.lean +++ b/Tests/Ix/SourceContract/Driver.lean @@ -52,6 +52,23 @@ def suite : List TestSeq := [ let .ok marked := prepare (constants markedSource) | return false if marked == constants markedSource then return false return true, + ioTest "parallel source preflight checks every batch and its final remainder" do + let sources := (List.range 2049).map fun i => + let name := Lean.Name.num plainSource.name i + let source : ConstantInfo := .axiomInfo { + name, levelParams := [], type := plainSource.type, isUnsafe := false } + (name, source) + if (checkOrdinaryConstants sources (fun _ => false)).toOption != some true then return false + for index in [1023, 1024, 2048] do + let marked := sources.mapIdx fun i (name, source) => + if i != index then (name, source) else + let source : ConstantInfo := .axiomInfo { + name, levelParams := [] + type := .mdata (({} : Lean.MData).setNat `ix.contract.unknown 1) source.type + isUnsafe := false } + (name, source) + if (checkOrdinaryConstants marked (fun _ => false)).toOption != some false then return false + return true, ioTest "Lean constant-list driver rejects an unadmitted annotated axiom" do return unsupported (← compileLeanConsts (constants markedSource) (numWorkers := 1)), ioTest "explicit Lean input rejects a missing annotation registry" do