From ecc7a3476737961f270e60d49d33c93160b4ee6f Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Thu, 17 Sep 2026 14:03:37 +0000 Subject: [PATCH] fix(kernel): reject circular safe definitions and pin IxVM rejection The Rust kernel could accept a safe declaration whose value was a reference to itself: looking up the reference returned its declared type without establishing that its definition was well founded. For example, with only P : Prop as an axiom, `theorem loop : P := loop` was accepted. Raw Ixon can also encode an axiom-free circular definition of `forall P : Prop, P`, or put the same attack in a singleton or mutually dependent definition block. This is a soundness defect: invalid proofs were accepted. Port the Rust admission guard from argumentcomputer/ix#630 (2f0b47c2). Before typechecking a safe definition, traverse definition references in both its type and value, including binder domains, let initializers, shared syntax, and projection heads. Explicit worklists distinguish active declarations from completed ones and reject cycles, including cycles spanning internal blocks. Expression traversal deduplicates shared syntax without recursive host-stack calls. The host traversal fails closed at one million dependency tasks. Axioms, inductives, constructors, and recursors retain their own admission rules; partial and unsafe definitions retain their existing policy. IxVM is already protected against this attack: ingress gives safe definitions neither a standalone self-reference slot nor mutual peer slots. Add hash-bound Ixon exploit fixtures to demonstrate that protection through the production verify_claim entrypoint, using both the bytecode interpreter and generated executor. Cover self-reference in definitions, theorems, and opaque declarations; mutual cycles; cycles hidden in types, let initializers, and sharing; and misleading theorem/opaque safety bytes. A closed identity proof must be accepted as a positive control. These tests require successful witness construction before checking rejection. No IxVM implementation, generated code, or FFT pin changes are needed. The Rust unit regressions reproduced acceptance before the fix. They now reject the attacks and cover projection-head dependency collection and preservation of partial/unsafe behavior. The serialized fixtures also run through the Rust checker with hash verification enabled, requiring the cycle diagnostic for invalid targets. Positive Rust controls retain valid acyclic forward references and shared dependencies. Exported structural, well-founded, and mutual recursion fixtures check all 33, 1350, and 26 targets respectively, with no omitted requested definitions. The shared fixtures run in the focused kernel-dependencies runner and the IxVM suite. Validation: - cargo test --locked --release -p ix-kernel: 846 passed, 8 ignored. - lake test --wfail -- --ignored kernel-dependencies: 44 checks passed. - cargo clippy --locked --release --workspace --all-targets --features ix-ffi/parallel,ix-ffi/net,ix-ffi/test-ffi -- -D warnings: passed. - cargo fmt --all -- --check and git diff --check: passed. - ix codegen --check: all three generated targets are up to date. Co-authored-by: John C. Burnham --- Tests/Ix/IxVM/DefinitionDependencies.lean | 182 ++++++++++++++ Tests/Ix/IxVM/Exploits.lean | 58 ++--- Tests/Main.lean | 10 +- crates/kernel/src/check.rs | 283 ++++++++++++++++++++++ 4 files changed, 504 insertions(+), 29 deletions(-) create mode 100644 Tests/Ix/IxVM/DefinitionDependencies.lean 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();