Compiler fixes for auxiliary constant generation

.gitignore

@@ -7,3 +7,7 @@
 # Nix
 result*
 .direnv/
+
+#Ix
+*.ixe
+plans

Benchmarks/Compile/CompileMutualFixtures.lean

@@ -0,0 +1 @@
+import Tests.Ix.Compile.Mutual

Benchmarks/Compile/lake-manifest.json

@@ -21,6 +21,13 @@
    "inputRev": "v4.29.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
+  {"type": "path",
+   "scope": "",
+   "name": "ix",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../..",
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
@@ -110,6 +117,26 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": true,
-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/argumentcomputer/Blake3.lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
+   "name": "Blake3",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/argumentcomputer/LSpec",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
+   "name": "LSpec",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "Compile",
  "lakeDir": ".lake"}

Benchmarks/Compile/lakefile.toml

@@ -17,6 +17,13 @@ name = "CompileMathlib"
 [[lean_lib]]
 name = "CompileFLT"
 
+[[lean_lib]]
+name = "CompileMutualFixtures"
+
+[[require]]
+name = "ix"
+path = "../.."
+
 [[require]]
 name = "flt"
 git = "https://github.com/ImperialCollegeLondon/FLT"

Ix/Claim.lean

@@ -94,10 +94,9 @@ structure RevealRecursorRule where
 inductive RevealMutConstInfo where
   | defn (kind : Option DefKind) (safety : Option DefinitionSafety)
          (lvls : Option UInt64) (typ : Option Address) (value : Option Address)
-  | indc (isRecr : Option Bool) (refl : Option Bool) (isUnsafe : Option Bool)
-         (lvls : Option UInt64) (params : Option UInt64)
-         (indices : Option UInt64) (nested : Option UInt64)
-         (typ : Option Address) (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
+  | indc (isUnsafe : Option Bool) (lvls : Option UInt64) (params : Option UInt64)
+         (indices : Option UInt64) (typ : Option Address)
+         (ctors : Option (Array (UInt64 × RevealConstructorInfo)))
   | recr (k : Option Bool) (isUnsafe : Option Bool) (lvls : Option UInt64)
          (params : Option UInt64) (indices : Option UInt64)
          (motives : Option UInt64) (minors : Option UInt64)
@@ -240,19 +239,15 @@ def put : RevealMutConstInfo → PutM Unit
     match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
     match typ with | some a => Serialize.put a | none => pure ()
     match value with | some a => Serialize.put a | none => pure ()
-  | .indc isRecr refl isUnsafe lvls params indices nested typ ctors => do
+  | .indc isUnsafe lvls params indices typ ctors => do
     putU8 1
-    let mask := computeMask [isRecr.isSome, refl.isSome, isUnsafe.isSome,
-                             lvls.isSome, params.isSome, indices.isSome,
-                             nested.isSome, typ.isSome, ctors.isSome]
+    let mask := computeMask [isUnsafe.isSome, lvls.isSome, params.isSome, 
+      indices.isSome, typ.isSome, ctors.isSome]
     putTag0 ⟨mask⟩
-    match isRecr with | some b => putBoolField b | none => pure ()
-    match refl with | some b => putBoolField b | none => pure ()
     match isUnsafe with | some b => putBoolField b | none => pure ()
     match lvls with | some n => putTag0 ⟨n⟩ | none => pure ()
     match params with | some n => putTag0 ⟨n⟩ | none => pure ()
     match indices with | some n => putTag0 ⟨n⟩ | none => pure ()
-    match nested with | some n => putTag0 ⟨n⟩ | none => pure ()
     match typ with | some a => Serialize.put a | none => pure ()
     match ctors with | some c => putCtors c | none => pure ()
   | .recr k isUnsafe lvls params indices motives minors typ rules => do
@@ -283,16 +278,13 @@ def get : GetM RevealMutConstInfo := do
     let value ← getOpt mask 16 Serialize.get
     return .defn kind safety lvls typ value
   | 1 => do -- Indc
-    let isRecr ← getOpt mask 1 getBoolField
-    let refl ← getOpt mask 2 getBoolField
-    let isUnsafe ← getOpt mask 4 getBoolField
-    let lvls ← getOpt mask 8 getTag0Size
-    let params ← getOpt mask 16 getTag0Size
-    let indices ← getOpt mask 32 getTag0Size
-    let nested ← getOpt mask 64 getTag0Size
-    let typ ← getOpt mask 128 Serialize.get
-    let ctors ← getOpt mask 256 getCtors
-    return .indc isRecr refl isUnsafe lvls params indices nested typ ctors
+    let isUnsafe ← getOpt mask 1 getBoolField
+    let lvls ← getOpt mask 2 getTag0Size
+    let params ← getOpt mask 4 getTag0Size
+    let indices ← getOpt mask 8 getTag0Size
+    let typ ← getOpt mask 16 Serialize.get
+    let ctors ← getOpt mask 32 getCtors
+    return .indc isUnsafe lvls params indices typ ctors
   | 2 => do -- Recr
     let k ← getOpt mask 1 getBoolField
     let isUnsafe ← getOpt mask 2 getBoolField

Ix/Commit.lean

@@ -208,8 +208,7 @@ def openMutConst (mc : Ixon.MutConst) : RevealMutConstInfo :=
       for j in [:i.ctors.size] do
         arr := arr.push (j.toUInt64, openConstructor i.ctors[j]!)
       return arr
-    .indc (some i.recr) (some i.refl) (some i.isUnsafe)
-      (some i.lvls) (some i.params) (some i.indices) (some i.nested)
+    .indc (some i.isUnsafe) (some i.lvls) (some i.params) (some i.indices)
       (some (exprAddr i.typ)) (some ctors)
   | .recr r =>
     let rules := Id.run do

Ix/Common.lean

@@ -328,6 +328,40 @@ private partial def collectDependenciesAux (const : Lean.ConstantInfo)
     goExpr consts acc val.value
   | .recInfo val =>
     let acc ← collectNames val.all acc
+    -- The compiler processes a declaration's recursors as one block, and
+    -- they cross-reference in rule RHSs (`A.rec`'s rule calls `A.rec_1`,
+    -- `A.rec_2`'s calls `C.rec`), so the closure needs every sibling:
+    -- `<ind>.rec` per block inductive plus the nested-aux `<all0>.rec_N`.
+    let siblings := val.all.filterMap fun ind =>
+      let n := Lean.mkRecName ind
+      if consts.contains n then some n else none
+    let auxSiblings : List Lean.Name := Id.run do
+      let mut out := []
+      let mut i := 1
+      repeat
+        match val.all.head? with
+        | none => break
+        | some base =>
+          let n := Lean.Name.mkStr base s!"rec_{i}"
+          if consts.contains n then
+            out := n :: out
+            i := i + 1
+          else break
+      return out
+    let acc ← collectNames (siblings ++ auxSiblings) acc
+    -- A nested-aux recursor's rules recurse via the external container's
+    -- ctors; its evaporated form aliases that container's recursor
+    -- (`List.rec`), which no collected expr mentions — pull it via each
+    -- rule ctor's owning inductive.
+    let extRecs := val.rules.filterMap fun rule =>
+      match consts.find? rule.ctor with
+      | some (.ctorInfo cv) =>
+        if val.all.contains cv.induct then none
+        else
+          let n := Lean.mkRecName cv.induct
+          if consts.contains n then some n else none
+      | _ => none
+    let acc ← collectNames extRecs acc
     let acc ← goExpr consts acc val.type
     val.rules.foldlM (init := acc) fun acc rule => goExpr consts acc rule.rhs
 where

Ix/CompileM.lean

@@ -1112,13 +1112,10 @@ def compileInductive (i : InductiveVal) (ctorVals : Array ConstructorVal)
     let ctxAddrs ← getMutCtxAddrs
 
     let ind : Ixon.Inductive := {
-      recr := i.isRec
-      refl := i.isReflexive
       isUnsafe := i.isUnsafe
       lvls := i.cnst.levelParams.size.toUInt64
       params := i.numParams.toUInt64
       indices := i.numIndices.toUInt64
-      nested := i.numNested.toUInt64
       typ := typeExpr
       ctors := ctors
     }
@@ -1194,13 +1191,10 @@ def compileInductiveData (i : Ind)
     let ctxAddrs ← getMutCtxAddrs
 
     let ind : Ixon.Inductive := {
-      recr := i.isRec
-      refl := i.isReflexive
       isUnsafe := i.isUnsafe
       lvls := i.levelParams.size.toUInt64
       params := i.numParams.toUInt64
       indices := i.numIndices.toUInt64
-      nested := i.numNested.toUInt64
       typ := typeExpr
       ctors := ctors
     }

Ix/DecompileM.lean

@@ -670,8 +670,9 @@ def decompileInductive (ind : Ixon.Inductive) (cnst : Constant) (cMeta : Constan
     cnst := { name, levelParams := univParams, type := typeExpr },
     numParams := ind.params.toNat, numIndices := ind.indices.toNat,
     all := allNames, ctors := ctorNames,
-    numNested := ind.nested.toNat, isRec := ind.recr,
-    isUnsafe := ind.isUnsafe, isReflexive := ind.refl }
+    -- temporary stub until we update the Lean compiler and decompiler semantics
+    numNested := 0, isRec := false
+    isUnsafe := ind.isUnsafe, isReflexive := false }
   pure (indVal, ctors)
 
 /-! ## Projection Handling -/

Ix/IxVM/Convert.lean

@@ -314,11 +314,11 @@ def convert := ⟦
     match ctx {
       ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) =>
         match ind {
-          Inductive.Mk(is_rec, is_refl, is_unsafe, lvls, params, indices, nested, typ, _) =>
+          Inductive.Mk(is_unsafe, lvls, params, indices, typ, _) =>
             let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs);
             KConstantInfo.Induct(
               flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices),
-              ctor_idxs, is_rec, is_refl, is_unsafe, flatten_u64(nested), block_addr),
+              ctor_idxs, is_unsafe, block_addr),
         },
     }
   }

Ix/IxVM/Ingress.lean

@@ -175,7 +175,7 @@ def ingress := ⟦
     match mc {
       MutConst.Indc(ind) =>
         match ind {
-          Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
+          Inductive.Mk(_, _, _, _, _, ctors) =>
             list_length(ctors) + 1,
         },
       MutConst.Recr(_) => 1,
@@ -850,7 +850,7 @@ def ingress := ⟦
         match mc {
           MutConst.Indc(ind) =>
             match ind {
-              Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
+              Inductive.Mk(_, _, _, _, _, ctors) =>
                 let num_ctors = list_length(ctors);
                 let this_ctors = build_ctor_idxs(num_ctors, cur_pos, 0);
                 let rest_ctors = build_rule_ctor_idxs_walk(rest,
@@ -998,7 +998,7 @@ def ingress := ⟦
             match mc {
               MutConst.Indc(ind) =>
                 match ind {
-                  Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
+                  Inductive.Mk(_, _, _, _, _, ctors) =>
                     build_ctor_idxs(list_length(ctors), cur_pos, 0),
                 },
               _ => store(ListNode.Nil),
@@ -1027,7 +1027,7 @@ def ingress := ⟦
     match mc {
       MutConst.Indc(ind) =>
         match ind {
-          Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
+          Inductive.Mk(_, _, _, _, _, ctors) =>
             let num_ctors = list_length(ctors);
             let induct_pos = block_start + member_offset(members, member_idx);
             let ctor_idxs = build_ctor_idxs(num_ctors, induct_pos, 0);
@@ -1546,7 +1546,7 @@ def ingress := ⟦
             match mc {
               MutConst.Indc(ind) =>
                 match ind {
-                  Inductive.Mk(_, _, _, _, _, _, _, _, ctors) =>
+                  Inductive.Mk(_, _, _, _, _, ctors) =>
                     list_length(ctors),
                 },
               _ => 0,

Ix/IxVM/Ixon.lean

@@ -83,9 +83,9 @@ def ixon := ⟦
     Mk(G, U64, U64, U64, U64, &Expr)
   }
 
-  -- Inductive: (recr, refl, is_unsafe, lvls, params, indices, nested, typ, ctors)
+  -- Inductive: (is_unsafe, lvls, params, indices, typ, ctors)
   enum Inductive {
-    Mk(G, G, G, U64, U64, U64, U64, &Expr, List‹Constructor›)
+    Mk(G, U64, U64, U64, &Expr, List‹Constructor›)
   }
 
   -- InductiveProj: (idx, block_address)

Ix/IxVM/IxonDeserialize.lean

@@ -479,21 +479,18 @@ def ixonDeserialize := ⟦
   }
 
   -- Inductive: byte(bools) + Tag0(lvls) + Tag0(params) + Tag0(indices) +
-  --            Tag0(nested) + expr(typ) + Tag0(ctors_len) + ctors...
+  --            expr(typ) + Tag0(ctors_len) + ctors...
   fn get_inductive(stream: ByteStream) -> (Inductive, ByteStream) {
     let (bools_byte, s) = read_byte(stream);
     let bits = u8_bit_decomposition(bools_byte);
-    let recr = bits[0];
-    let refl = bits[1];
-    let is_unsafe = bits[2];
+    let is_unsafe = bits[0];
     let (lvls, s2) = get_tag0(s);
     let (params, s3) = get_tag0(s2);
     let (indices, s4) = get_tag0(s3);
-    let (nested, s5) = get_tag0(s4);
-    let (typ, s6) = get_expr(s5);
-    let (ctors_len, s7) = get_tag0(s6);
-    let (ctors, s8) = get_constructor_list(s7, ctors_len);
-    (Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, store(typ), ctors), s8)
+    let (typ, s5) = get_expr(s4);
+    let (ctors_len, s6) = get_tag0(s5);
+    let (ctors, s7) = get_constructor_list(s6, ctors_len);
+    (Inductive.Mk(is_unsafe, lvls, params, indices, store(typ), ctors), s7)
   }
 
   -- ============================================================================

Ix/IxVM/IxonSerialize.lean

@@ -387,17 +387,15 @@ def ixonSerialize := ⟦
 
   fn put_inductive(indc: Inductive, rest: ByteStream) -> ByteStream {
     match indc {
-      Inductive.Mk(recr, refl, is_unsafe, lvls, params, indices, nested, &typ, ctors) =>
-        let bools = recr + 2 * refl + 4 * is_unsafe;
+      Inductive.Mk(is_unsafe, lvls, params, indices, &typ, ctors) =>
         let ctors_len = list_length_u64(ctors);
-        store(ListNode.Cons(u8_from_field_unsafe(bools),
+        store(ListNode.Cons(u8_from_field_unsafe(is_unsafe),
           put_tag0(lvls,
             put_tag0(params,
               put_tag0(indices,
-                put_tag0(nested,
-                  put_expr(typ,
-                    put_tag0(ctors_len,
-                      put_constructor_list(ctors, rest))))))))),
+                put_expr(typ,
+                  put_tag0(ctors_len,
+                    put_constructor_list(ctors, rest)))))))),
     }
   }