diff --git a/Tests/Ix/IxVM/DefinitionDependencies.lean b/Tests/Ix/IxVM/DefinitionDependencies.lean new file mode 100644 index 000000000..fc95712f0 --- /dev/null +++ b/Tests/Ix/IxVM/DefinitionDependencies.lean @@ -0,0 +1,182 @@ +import Tests.Ix.IxVM.Exploits +import Ix.KernelCheck +import Tests.Ix.Tc.AnonDiff + +namespace Tests.Ix.IxVM.DefinitionDependencies + +open LSpec Exploits + +/-- `∀ P : Prop, P` has no closed inhabitant; no axiom is needed for this exploit. -/ +private def everyProp : Ixon.Expr := .leanAll (.sort 0) (.var 0) + +private def identityType : Ixon.Expr := + .leanAll (.sort 0) (.leanAll (.var 0) (.var 1)) + +private def identityValue : Ixon.Expr := + .leanLam (.sort 0) (.leanLam (.var 0) (.var 0)) + +private def definition (kind : Ix.DefKind) (ty value : Ixon.Expr) : Ixon.Definition := + ⟨kind, .safe, 0, ty, value⟩ + +private def block (definitions : Array Ixon.Definition) + (sharing : Array Ixon.Expr := #[]) : Ixon.Env × Address := Id.run do + let (source, address) := storeAt {} + ⟨.muts (definitions.map .defn), sharing, #[], #[.zero]⟩ + let mut source := source + let mut first := address + for i in [:definitions.size] do + let (updated, projection) := storeAt source + ⟨.dPrj ⟨i.toUInt64, address⟩, #[], #[], #[]⟩ + source := { updated with anonHints := updated.anonHints.insert projection (.regular 0) } + if i == 0 then first := projection + return (source, first) + +private def asCase (name intent : String) (fixture : Ixon.Env × Address) + (accept : Bool := false) : ExploitCase := + { name, intent, env := fixture.1, claim := .check fixture.2 none + expectAccept := accept } + +/-- Hand-authored, hash-bound Ixon environments for the Rust soundness fix. +IxVM already rejects circular safe definitions by denying relative peer slots. +Only the rejection cases are shared with IxVM: accepting valid forward peer +references would require a separate completeness change to that kernel. -/ +def cases : Array ExploitCase := Id.run do + let mut result := #[] + for (label, kind) in [("definition", Ix.DefKind.defn), ("theorem", .thm), ("opaque", .opaq)] do + result := result.push (asCase s!"axiom-free-self-{label}" + "prove every proposition by citing the declaration itself" + (storeAt {} ⟨.defn (definition kind everyProp (.recur 0 #[])), #[], #[], #[.zero]⟩)) + result := result.push (asCase s!"mutual-self-{label}" + "hide the same false proof in a one-member mutual block" + (block #[definition kind everyProp (.recur 0 #[])])) + result := result.push (asCase "mutual-two-member-cycle" + "two declarations justify each other's proof of every proposition" + (block #[definition .thm everyProp (.recur 1 #[]), + definition .opaq everyProp (.recur 0 #[])])) + result := result.push (asCase "mutual-cycle-in-let-initializer" + "a let initializer hides a circular proof even when the body ignores it" + (block #[definition .thm identityType + (.leanLet true everyProp (.recur 1 #[]) identityValue), + definition .thm everyProp (.recur 1 #[])])) + result := result.push (asCase "mutual-cycle-through-sharing" + "sharing must not hide an edge of a declaration cycle" + (block #[definition .thm everyProp (.share 0), + definition .opaq everyProp (.recur 0 #[])] #[.recur 1 #[]])) + result := result.push (asCase "mutual-cycle-in-type" + "a declaration type must not depend on its own definition" + (block #[definition .defn (.recur 0 #[]) identityValue])) + result := result.push (asCase "control-acyclic-forward-definition" + "a forward reference to a genuine identity proof is valid" + (block #[definition .thm identityType (.recur 1 #[]), + definition .defn identityType identityValue]) true) + result := result.push (asCase "control-acyclic-forward-type" + "declaration types may depend on a later acyclic type alias" + (block #[definition .thm (.recur 1 #[]) identityValue, + definition .defn (.sort 0) identityType]) true) + result := result.push (asCase "control-acyclic-shared-diamond" + "shared live references are traversed, but unused sharing creates no dependency" + (block #[definition .thm identityType (.share 0), + definition .opaq identityType (.share 0), + definition .defn identityType identityValue] #[.recur 2 #[]]) true) + return result + +/-- IxVM classifies theorems as logical regardless of the safety byte, and +opaque declarations as logical unless explicitly unsafe. Mutual ingress must +use that effective classification too, as standalone ingress already does. -/ +private def ixvmSafetyCases : Array ExploitCase := + #[("theorem-unsafe", Ix.DefKind.thm, Ix.DefinitionSafety.unsaf), + ("theorem-partial", .thm, .part), ("opaque-partial", .opaq, .part)].map + fun (label, kind, safety) => + asCase s!"mutual-self-{label}" + "the wire safety byte must not bypass the safe declaration peer-slot restriction" + (block #[{ definition kind everyProp (.recur 0 #[]) with safety }]) + +def rustTests : IO TestSeq := do + let directory ← IO.FS.createTempDir + try + let mut tests : TestSeq := .done + for c in cases do + let path := directory / s!"{c.name}.ixe" + let bytes ← IO.ofExcept (Ixon.serEnv c.env) + IO.FS.writeBinFile path bytes + let rows ← Ix.KernelCheck.rsCheckAnonFFI path.toString true "" + let .check target _ := c.claim | throw <| IO.userError "expected a Check claim" + let row := rows.find? (fun row => row.1 == toString target) + let correct : Bool := match row with + | none => false + | some (_, error) => + if c.expectAccept then rows.all (·.2.isNone) + else error.any fun e => + (e.message.splitOn "cyclic definition dependency").length > 1 + tests := tests ++ test s!"Rust definition dependencies: {c.name}" correct + return tests + finally + IO.FS.removeDirAll directory + +namespace Fixtures + +def countStruct : Nat → Nat + | 0 => 0 + | n + 1 => countStruct n + 1 +termination_by structural n => n + +def countWellFounded (n : Nat) : Nat := + if h : n = 0 then 0 else countWellFounded (n - 1) + 1 +termination_by n +decreasing_by omega + +mutual + def even : Nat → Bool + | 0 => true + | n + 1 => odd n + termination_by structural n => n + + def odd : Nat → Bool + | 0 => false + | n + 1 => even n + termination_by structural n => n +end + +end Fixtures + +/-- The Rust guard must preserve termination-checked source recursion. +Check every declaration in each exported closure. -/ +private def recursionTests : IO TestSeq := do + let env ← get_env! + let directory ← IO.FS.createTempDir + try + let mut tests : TestSeq := .done + for (label, seeds) in [("structural", [``Fixtures.countStruct]), + ("well-founded", [``Fixtures.countWellFounded]), + ("mutual", [``Fixtures.even, ``Fixtures.odd])] do + for seed in seeds do + let some (.defnInfo declaration) := env.find? seed + | throw <| IO.userError s!"missing elaborated definition {seed}" + unless declaration.safety == .safe do + throw <| IO.userError s!"{seed} is not a safe definition" + let path := directory / s!"{label}.ixe" + let constants := Tests.Tc.AnonDiff.closureOf env seeds + let status ← Ix.CompileM.rsCompileEnvBytesFFI constants path.toString false + unless status.ungrounded.isEmpty do + throw <| IO.userError s!"compilation omitted {status.ungrounded.size} declarations" + let source ← IO.ofExcept <| Ixon.deEnv (← IO.FS.readBinFile path) + let rows ← Ix.KernelCheck.rsCheckAnonFFI path.toString true "" + for seed in seeds do + let some address := source.getAddr? (Ix.Name.fromLeanName seed) + | throw <| IO.userError s!"export omitted {seed}" + unless rows.any (fun row => row.1 == toString address) do + throw <| IO.userError s!"no checking result for {seed}" + tests := tests ++ test s!"Rust accepts safe {label} recursion" (rows.all (·.2.isNone)) + return tests + finally + IO.FS.removeDirAll directory + +def tests (compiled : Aiur.CompiledToplevel) : IO TestSeq := do + let control := asCase "control-closed-identity" + "a genuine closed proof must still be accepted" + (storeAt {} ⟨.defn (definition .thm identityType identityValue), #[], #[], #[.zero]⟩) true + let ixvmCases := cases.filter (fun c => !c.expectAccept) ++ ixvmSafetyCases ++ #[control] + return (← runCases compiled ixvmCases) ++ (← runCases compiled ixvmCases true) ++ + (← rustTests) ++ (← recursionTests) + +end Tests.Ix.IxVM.DefinitionDependencies diff --git a/Tests/Ix/IxVM/Exploits.lean b/Tests/Ix/IxVM/Exploits.lean index ff564a074..75185fbc4 100644 --- a/Tests/Ix/IxVM/Exploits.lean +++ b/Tests/Ix/IxVM/Exploits.lean @@ -1444,6 +1444,34 @@ def cases (base : Ixon.Env) (strAddr falseAddr : Address) /-! ## Runner -/ +/-- Run raw-Ixon cases through the production claim entrypoint. -/ +def runCases (compiled : Aiur.CompiledToplevel) (fixtures : Array ExploitCase) + (useCodegen : Bool := false) : + IO TestSeq := do + let funIdx ← match compiled.getFuncIdx `verify_claim with + | some i => pure i + | none => throw <| IO.userError "verify_claim entrypoint missing" + let mut tests : TestSeq := .done + for c in fixtures do + let verdict := if c.expectAccept then "ACCEPT" else "REJECT" + let engine := if useCodegen then "codegen" else "bytecode" + let label := s!"exploit {engine} {verdict} {c.name}" + match IxVM.ClaimHarness.buildClaimWitness c.env c.claim c.trees with + | .error e => + tests := tests ++ test s!"{label}: witness build failed ({e})" false + | .ok witness => + let execution := if useCodegen then + compiled.bytecode.executeIxVM funIdx witness.input witness.inputIOBuffer + else compiled.bytecode.execute funIdx witness.input witness.inputIOBuffer + match execution with + | .ok _ => + tests := tests ++ + test s!"{label} (accepted — buys: {c.intent})" c.expectAccept + | .error e => + IO.println s!" [{c.name}] rejected by: {e}" + tests := tests ++ test label (!c.expectAccept) + return tests + /-- Run every case against the compiled `IxVM.ixVM` toplevel through the `verify_claim` entrypoint (the production claim path — never the `verify_const` debug entrypoint, whose whole contract is to trust @@ -1456,9 +1484,6 @@ def cases (base : Ixon.Env) (strAddr falseAddr : Address) (or a live exploit appear to be closed) against a stale kernel. -/ def exploitTests (leanEnv : Lean.Environment) (compiled : Aiur.CompiledToplevel) : IO TestSeq := do - let funIdx ← match compiled.getFuncIdx `verify_claim with - | some i => pure i - | none => throw <| IO.userError "verify_claim entrypoint missing" -- Cases that assert something about `String` need the real `String` -- constant to declare a type against; everything else is built from -- nothing. @@ -1482,30 +1507,7 @@ def exploitTests (leanEnv : Lean.Environment) let unitUnitA ← IxVM.ClaimHarness.lookupAddr base ``Unit.unit let iffA ← IxVM.ClaimHarness.lookupAddr base ``Iff let iffRecA ← IxVM.ClaimHarness.lookupAddr base ``Iff.rec - let mut tests : TestSeq := .done - for c in cases base strAddr falseAddr eqA boolA beqA sizeA trueA - falseBoolA reflA natA sizeOfSizeOfA sizeOfMkA unitA unitUnitA - iffA iffRecA do - let verdict := if c.expectAccept then "ACCEPT" else "REJECT" - let label := s!"exploit {verdict} {c.name}" - match IxVM.ClaimHarness.buildClaimWitness c.env c.claim c.trees with - | .error e => - -- A witness that will not build is a broken fixture, not a - -- kernel verdict; never let it read as a pass. - tests := tests ++ test s!"{label}: witness build failed ({e})" false - | .ok witness => - match compiled.bytecode.execute funIdx witness.input witness.inputIOBuffer with - | .ok _ => - tests := tests ++ - test s!"{label} (accepted — buys: {c.intent})" c.expectAccept - | .error e => - -- Surface the rejection reason. A case can pass for the WRONG - -- reason — a malformed fixture that aborts before it reaches - -- the mechanism under attack looks identical to a kernel that - -- correctly refuses the exploit. Print it so the author can - -- confirm the assert that fired is the intended one. - IO.println s!" [{c.name}] rejected by: {e}" - tests := tests ++ test label (!c.expectAccept) - return tests + runCases compiled (cases base strAddr falseAddr eqA boolA beqA sizeA trueA + falseBoolA reflA natA sizeOfSizeOfA sizeOfMkA unitA unitUnitA iffA iffRecA) end Tests.Ix.IxVM.Exploits diff --git a/Tests/Main.lean b/Tests/Main.lean index a33b64044..841b027e3 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -4,6 +4,7 @@ import Tests.Ix.IxonCorpus import Tests.Ix.IxonSyntax import Tests.Ix.IxVM import Tests.Ix.IxVM.Exploits +import Tests.Ix.IxVM.DefinitionDependencies import Tests.Ix.Claim import Tests.Ix.Merkle import Tests.Ix.AssumptionTree @@ -213,6 +214,12 @@ def primaryRunners : List (String × IO UInt32) := [ /-- Ignored test runners - expensive, deferred IO actions run only when explicitly requested -/ def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [ + ("kernel-dependencies", do + match AiurTestEnv.build IxVM.ixVM IxVM.functionGroups with + | .error e => IO.eprintln s!"IxVM setup failed: {e}"; return 1 + | .ok vm => + let tests ← Tests.Ix.IxVM.DefinitionDependencies.tests vm.compiled + LSpec.lspecIO (.ofList [("kernel-dependencies", [tests])]) []), ("ixvm", do let kernelChecks ← kernelChecks env -- the kernel CheckEnv smokes . @@ -245,6 +252,7 @@ def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [ -- reach. Each case pins the kernel's verdict, which is REJECT -- except where accepting is the specified claim semantics. let exploitSeq ← Tests.Ix.IxVM.Exploits.exploitTests env vmEnv.compiled + let dependencySeq ← Tests.Ix.IxVM.DefinitionDependencies.tests vmEnv.compiled let aiurSeq := (kernelChecks ++ [envFull, envFrontier, checkAsm, revealFields, revealExpr, revealModes, revealCPrj, containsTc]).foldl @@ -285,7 +293,7 @@ def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [ (actual = 7_072_190_269)) LSpec.lspecIO (.ofList [("ixvm", - [fullSeq, aiurSeq, arenaSeq, exploitSeq, paritySeq, shardSeq])]) []), + [fullSeq, aiurSeq, arenaSeq, exploitSeq, dependencySeq, paritySeq, shardSeq])]) []), ("validate-aux", runCompileValidateAux env), -- Cross-compiler differential over the same fixture corpus: pure-Lean -- Ix.CompileM per-block vs Rust, root-cause classified (see diff --git a/crates/kernel/src/check.rs b/crates/kernel/src/check.rs index e6a71854c..bfd5e2916 100644 --- a/crates/kernel/src/check.rs +++ b/crates/kernel/src/check.rs @@ -47,6 +47,44 @@ struct ValidationTiming { univ: Duration, } +// Bound dependency traversal independently of type-inference fuel. +const MAX_DEFINITION_DEPENDENCY_STEPS: usize = 1_000_000; + +enum DefinitionDependencyTask { + Enter(KId), + Finish(KId, KConst), +} + +/// References in both the type and value, including projection heads. The +/// expression worklist visits shared syntax once without host-stack recursion. +fn definition_dependencies(c: &KConst) -> Vec> { + let KConst::Defn { ty, val, .. } = c else { return vec![] }; + let mut pending = vec![val, ty]; + let mut seen: FxHashSet = FxHashSet::default(); + let mut refs = vec![]; + while let Some(expr) = pending.pop() { + if !seen.insert(expr.hash_key()) { + continue; + } + match expr.data() { + ExprData::Const(id, ..) => refs.push(id.clone()), + ExprData::App(fun, arg, _) => pending.extend([arg, fun]), + ExprData::Lam(_, _, dom, body, _) | ExprData::All(_, _, dom, body, _) => { + pending.extend([body, dom]) + }, + ExprData::Let(_, ty, val, body, _, _) => { + pending.extend([body, val, ty]); + }, + ExprData::Prj(id, _, major, _) => { + refs.push(id.clone()); + pending.push(major); + }, + _ => {}, + } + } + refs +} + #[derive(Clone, Copy, Debug, Eq, PartialEq)] enum CheckBlockKind { Defn, @@ -660,6 +698,7 @@ impl TypeChecker<'_, M> { if let (Some(t), Some(start)) = (timing.as_deref_mut(), val_start) { t.val += start.elapsed(); } + self.check_definition_dependencies(c)?; }, KConst::Recr { rules, .. } => { let rules_start = timing.as_ref().map(|_| Instant::now()); @@ -683,6 +722,61 @@ impl TypeChecker<'_, M> { Ok(()) } + /// A reference's declared type does not justify a circular definition. + /// Follow every reachable definition, while treating declarations with their + /// own admission rules (axioms, inductives, constructors, recursors) as leaves. + fn check_definition_dependencies( + &mut self, + c: &KConst, + ) -> Result<(), TcError> { + if !matches!(c, KConst::Defn { safety: DefinitionSafety::Safe, .. }) { + return Ok(()); + } + let mut pending: Vec<_> = definition_dependencies(c) + .into_iter() + .rev() + .map(DefinitionDependencyTask::Enter) + .collect(); + let mut active: FxHashSet
= FxHashSet::default(); + let mut finished: FxHashSet
= FxHashSet::default(); + for _ in 0..MAX_DEFINITION_DEPENDENCY_STEPS { + let Some(task) = pending.pop() else { return Ok(()) }; + match task { + DefinitionDependencyTask::Enter(id) => { + if finished.contains(&id.addr) { + continue; + } + if active.contains(&id.addr) { + return Err(TcError::Other(format!( + "cyclic definition dependency at {id}" + ))); + } + let declaration = self.get_const(&id)?; + let dependencies = definition_dependencies(&declaration); + active.insert(id.addr.clone()); + pending.push(DefinitionDependencyTask::Finish(id, declaration)); + pending.extend( + dependencies.into_iter().rev().map(DefinitionDependencyTask::Enter), + ); + }, + DefinitionDependencyTask::Finish(id, declaration) => { + if finished.contains(&id.addr) + || !definition_dependencies(&declaration) + .iter() + .all(|dependency| finished.contains(&dependency.addr)) + { + return Err(TcError::Other(format!( + "incomplete definition dependencies at {id}" + ))); + } + active.remove(&id.addr); + finished.insert(id.addr); + }, + } + } + Err(TcError::MaxRecDepth) + } + fn phase_timing_label_matches(&self, id: &KId) -> bool { match crate::env_var("IX_KERNEL_DEBUG_CONST") { Ok(filter) if filter.is_empty() => true, @@ -1803,6 +1897,195 @@ mod tests { ); } + fn dependency_def( + id: &KId, + ty: AE, + val: AE, + safety: DefinitionSafety, + kind: DefKind, + ) -> KConst { + KConst::Defn { + name: (), + level_params: (), + kind, + safety, + hints: ReducibilityHints::Regular(0), + lvls: 0, + ty, + val, + lean_all: (), + block: id.clone(), + } + } + + fn insert_proposition(env: &mut KEnv) -> AE { + let id = mk_id("P"); + env.insert( + id.clone(), + KConst::Axio { + name: (), + level_params: (), + is_unsafe: false, + lvls: 0, + ty: sort0(), + }, + ); + AE::cnst(id, Box::new([])) + } + + #[test] + fn definition_dependency_rejects_self_justifying_theorem() { + let mut env = KEnv::::new(); + let prop = insert_proposition(&mut env); + let id = mk_id("loop"); + env.insert( + id.clone(), + dependency_def( + &id, + prop, + AE::cnst(id.clone(), Box::new([])), + DefinitionSafety::Safe, + DefKind::Theorem, + ), + ); + let error = TypeChecker::new(&mut env).check_const(&id).unwrap_err(); + assert!(error.to_string().contains("cyclic definition dependency")); + } + + #[test] + fn definition_dependency_rejects_mutual_cycles_in_every_safe_kind() { + for kind in [DefKind::Definition, DefKind::Theorem, DefKind::Opaque] { + let mut env = KEnv::::new(); + let prop = insert_proposition(&mut env); + let left = mk_id("left"); + let right = mk_id("right"); + for (id, target) in [(&left, &right), (&right, &left)] { + env.insert( + id.clone(), + dependency_def( + id, + prop.clone(), + AE::cnst(target.clone(), Box::new([])), + DefinitionSafety::Safe, + kind, + ), + ); + } + let mut tc = TypeChecker::new(&mut env); + for id in [&left, &right] { + let error = tc.check_const(id).unwrap_err(); + assert!(error.to_string().contains("cyclic definition dependency")); + } + } + } + + #[test] + fn definition_dependency_checks_types_and_hidden_values() { + let id = mk_id("hidden_cycle"); + let self_ref = AE::cnst(id.clone(), Box::new([])); + let cases = [ + (self_ref.clone(), sort0()), + (sort0(), AE::lam((), (), sort0(), self_ref.clone())), + (sort0(), AE::let_((), sort0(), self_ref.clone(), sort0(), true)), + (sort0(), AE::all((), (), self_ref.clone(), sort0())), + (sort0(), AE::app(self_ref.clone(), self_ref)), + ]; + for (ty, val) in cases { + let mut env = KEnv::::new(); + env.insert( + id.clone(), + dependency_def( + &id, + ty, + val, + DefinitionSafety::Safe, + DefKind::Definition, + ), + ); + let error = TypeChecker::new(&mut env).check_const(&id).unwrap_err(); + assert!(error.to_string().contains("cyclic definition dependency")); + } + } + + #[test] + fn definition_dependency_preserves_partial_and_unsafe_policy() { + for safety in [DefinitionSafety::Partial, DefinitionSafety::Unsafe] { + let mut env = KEnv::::new(); + let prop = insert_proposition(&mut env); + let id = mk_id("nonlogical_loop"); + env.insert( + id.clone(), + dependency_def( + &id, + prop, + AE::cnst(id.clone(), Box::new([])), + safety, + DefKind::Definition, + ), + ); + TypeChecker::new(&mut env).check_const(&id).unwrap(); + } + } + + #[test] + fn definition_dependency_accepts_acyclic_forward_shared_dependencies() { + let mut env = KEnv::::new(); + let prop = insert_proposition(&mut env); + let witness = mk_id("p"); + env.insert( + witness.clone(), + KConst::Axio { + name: (), + level_params: (), + is_unsafe: false, + lvls: 0, + ty: prop.clone(), + }, + ); + let left = mk_id("left"); + let right = mk_id("right"); + let shared = mk_id("shared"); + let block = mk_id("acyclic_block"); + for (id, value) in [ + (&left, AE::cnst(right.clone(), Box::new([]))), + (&right, AE::cnst(shared.clone(), Box::new([]))), + (&shared, AE::cnst(witness, Box::new([]))), + ] { + let mut declaration = dependency_def( + id, + prop.clone(), + value, + DefinitionSafety::Safe, + DefKind::Theorem, + ); + if let KConst::Defn { block: target, .. } = &mut declaration { + *target = block.clone(); + } + env.insert(id.clone(), declaration); + } + env.insert_block(block, vec![left.clone(), right.clone(), shared.clone()]); + let mut tc = TypeChecker::new(&mut env); + for id in [&left, &shared, &right, &left] { + tc.check_const(id).unwrap(); + } + } + + #[test] + fn definition_dependency_collects_projection_heads() { + let id = mk_id("root"); + let head = mk_id("projection_head"); + let major = mk_id("major"); + let declaration = dependency_def( + &id, + sort0(), + AE::prj(head.clone(), 0, AE::cnst(major.clone(), Box::new([]))), + DefinitionSafety::Safe, + DefKind::Definition, + ); + let refs = super::definition_dependencies(&declaration); + assert_eq!(refs, vec![head, major]); + } + #[test] fn checking_one_definition_checks_sibling_block() { let mut env = KEnv::::new();