Recover Ixon v3 compilation and anonymous kernel-check performance

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

Ix/Compile/SourceContract/Transport.lean

@@ -102,14 +102,66 @@ 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 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 then return false
+  return !hasAnyContractMetadata constants
+
 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
 

Tests/Ix/SourceContract/Driver.lean

@@ -33,6 +33,42 @@ 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 "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
@@ -72,4 +108,3 @@ def suite : List TestSeq := [
 end Tests.Ix.SourceContract.Driver
 
 end
-

crates/compile/src/compile/env.rs

@@ -157,20 +157,13 @@ pub fn compile_env_with_profile(
   profile: Option<&ixon::resource::addressed::Profile>,
 ) -> Result<CompileState, CompileError> {
   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())
   {

crates/compile/src/graph.rs

@@ -57,6 +57,8 @@ pub struct SetupScan {
   pub ind_groups: FxHashMap<Name, Vec<Name>>,
   /// Source contracts that the current conservative emitter cannot preserve.
   pub source_contracts: Vec<Name>,
+  /// Semantic declarations validated during the same lazy decode as the graph.
+  pub semantic_sources: Result<Vec<Name>, 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<Name, crate::ground::GroundError>,
     ind_groups: FxHashMap<Name, Vec<Name>>,
     source_contracts: Vec<Name>,
+    semantic_sources: Vec<Name>,
+    semantic_error: Option<ixon::CompileError>,
   }
 
   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

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<bool, String> {
     ix_kernel::tc::max_rec_fuel(),
     start.elapsed().as_secs_f64()
   );
-  let mut kenv = KEnv::<Anon>::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(