fix(kernel): reject circular safe definitions and pin IxVM rejection

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

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

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