Ixon v3: usage, ownership, and relative locality in the Ix frontend

.github/workflows/ci.yml

@@ -86,6 +86,10 @@ jobs:
           use-github-cache: false
       - name: Test Ix CLI
         run: lake test --wfail -- cli
+      - name: Test Ixon v3 contracts and consumers
+        run: |
+          lake exe ixon-v3-primitives
+          lake exe ixon-v3-tests --primitives
 
   rust-test:
     runs-on: warp-ubuntu-latest-x64-8x

.gitignore

@@ -10,6 +10,7 @@ result*
 
 #Ix
 *.ixe
+!Tests/Fixtures/ixon-v3/handoff/*.ixe
 plans
 refs
 

Ix/Aggr/Circuit.lean

@@ -533,6 +533,10 @@ def circuit := ⟦
   fn aggr_parse_check_env(bytes: ByteStream) -> (Addr, Option‹Addr›) {
     let (tag, s) = aggr_read_byte(bytes);
     assert_eq!(tag, 0xE5u8, "aggr: claim is not CheckEnv");
+    let (format, s) = aggr_read_byte(s);
+    assert_eq!(format, 3u8, "aggr: unsupported object format");
+    let (validator, s) = aggr_read_byte(s);
+    assert_eq!(validator, 1u8, "aggr: wrong validator identity");
     let (root, s2) = aggr_read_address(s);
     let (assumptions, stop) = aggr_get_opt_address(s2);
     assert_eq!(load(stop), ListNode.Nil,
@@ -800,3 +804,4 @@ def circuit := ⟦
 end Aggr
 
 end
+

Ix/CanonM.lean

@@ -19,6 +19,7 @@ module
 
 public import Ix.Common
 public import Ix.Environment
+public import Ix.SemanticContract
 public import Ix.Address
 
 public section
@@ -600,8 +601,10 @@ partial def exprEqCached (a b : Lean.Expr) : EqState Bool := do
       if !(← exprEqCached valA valB) then return false
       exprEqCached bodyA bodyB
     | .lit lA, .lit lB => pure (lA == lB)
-    -- Mdata entries are ignored for semantic equality (they carry annotations, not semantics)
-    | .mdata _ eA, .mdata _ eB => exprEqCached eA eB
+    -- Presentation metadata is transparent; effective contracts are semantic.
+    | .mdata dataA eA, .mdata dataB eB => do
+      if SemanticContract.leanFields dataA != SemanticContract.leanFields dataB then return false
+      exprEqCached eA eB
     | .proj tnA idxA sA, .proj tnB idxB sB =>
       if tnA != tnB || idxA != idxB then return false
       exprEqCached sA sB
@@ -773,3 +776,4 @@ def uncanonEnvParallel (consts : HashMap Ix.Name Ix.ConstantInfo) (numWorkers :
 end Ix.CanonM
 
 end
+

Ix/Catalog.lean

@@ -44,8 +44,8 @@ open Ixon (PutM GetM putU8 getU8 putBytes getBytes runPut runGet)
 /-- Magic bytes at the head of every `.ixc` file. -/
 def MAGIC : ByteArray := String.toUTF8 "IXC" ++ ⟨#[0, 0, 0, 0, 0]⟩
 
-/-- `.ixc` format version. -/
-def VERSION : UInt32 := 1
+/-- Manifest v2 binds Ixon v3 and erased-lean-v1 catalog claims. -/
+def VERSION : UInt32 := 2
 
 /-- Storage-profile flag: bit0 of the header `flags` word. -/
 def FLAG_CHUNKED : UInt32 := 1
@@ -185,6 +185,8 @@ def ser (c : Catalog) : ByteArray := runPut do
   putU32LE (match c.storage with
     | .chunked _ => FLAG_CHUNKED
     | .fat _ => 0)
+  putU8 3
+  putU8 1
   putAddr c.membersRoot
   putAddr c.contentRoot
   putU32LE c.members.size.toUInt32
@@ -245,6 +247,8 @@ where
       let flags ← getU32LE
       if flags &&& (~~~FLAG_CHUNKED) != 0 then
         throw s!"unknown .ixc flags {flags}"
+      unless (← getU8) == 3 do throw "catalog: unsupported object format"
+      unless (← getU8) == 1 do throw "catalog: wrong validator identity"
       let membersRoot ← getAddr
       let contentRoot ← getAddr
       let memberCount ← getU32LE

Ix/Claim.lean

@@ -154,6 +154,9 @@ inductive Claim where
   | reveal   (comm : Address) (info : RevealConstantInfo)
   | contains (tree : Address) (const : Address)
   | catalog  (members content : Address) (assumptions : Option Address)
+  /-- Combined erased typing and resource admission of the complete addressed
+  environment under the profile committed by `profile`. -/
+  | resource (root profile : Address)
   deriving BEq, Repr, Inhabited
 
 -- ============================================================================
@@ -478,13 +481,15 @@ def VARIANT_CHECK_ENV_CLAIM  : UInt64 := 5
 def VARIANT_REVEAL_CLAIM     : UInt64 := 6
 def VARIANT_CONTAINS_CLAIM   : UInt64 := 7
 def VARIANT_CATALOG_CLAIM    : UInt64 := 8
+def VARIANT_RESOURCE_CLAIM   : UInt64 := 9
 
 def VARIANT_EVAL_PROOF       : UInt64 := 0
 def VARIANT_CHECK_PROOF      : UInt64 := 1
 def VARIANT_CHECK_ENV_PROOF  : UInt64 := 2
 def VARIANT_REVEAL_PROOF     : UInt64 := 3
 def VARIANT_CONTAINS_PROOF   : UInt64 := 4
 def VARIANT_CATALOG_PROOF    : UInt64 := 5
+def VARIANT_RESOURCE_PROOF   : UInt64 := 6
 
 /-- Encode an `Option Address` as `[0x00]` (none) or `[0x01][addr:32]`
     (some). Mirrors `put_opt_addr` in src/ix/ixon/proof.rs. -/
@@ -498,39 +503,64 @@ def getOptAddr : GetM (Option Address) := do
   else if b == 0x01 then return some (← Serialize.get)
   else throw s!"getOptAddr: invalid tag {b}"
 
-def put : Claim → PutM Unit
+/-- Claim and proof payloads bind both the object format and the validator.
+0 is structural-v1, 1 is erased-lean-v1, 2 is resource-v1. -/
+def validatorForVariant (variant : UInt64) : UInt8 :=
+  if variant == VARIANT_REVEAL_CLAIM || variant == VARIANT_CONTAINS_CLAIM then 0
+  else if variant == VARIANT_RESOURCE_CLAIM then 2
+  else 1
+
+def variantOf : Claim → UInt64
+  | .eval .. => VARIANT_EVAL_CLAIM
+  | .check .. => VARIANT_CHECK_CLAIM
+  | .checkEnv .. => VARIANT_CHECK_ENV_CLAIM
+  | .reveal .. => VARIANT_REVEAL_CLAIM
+  | .contains .. => VARIANT_CONTAINS_CLAIM
+  | .catalog .. => VARIANT_CATALOG_CLAIM
+  | .resource .. => VARIANT_RESOURCE_CLAIM
+
+def putScope (validator : UInt8) : PutM Unit := do
+  putU8 3
+  putU8 validator
+
+def getScope (validator : UInt8) : GetM Unit := do
+  unless (← getU8) == 3 do throw "claim: unsupported object format"
+  unless (← getU8) == validator do throw "claim: wrong validator identity"
+
+def put (claim : Claim) : PutM Unit := do
+  putTag4 ⟨FLAG_CLAIM, variantOf claim⟩
+  putScope (validatorForVariant (variantOf claim))
+  match claim with
   | .eval input output assumptions => do
-    putTag4 ⟨FLAG_CLAIM, VARIANT_EVAL_CLAIM⟩
     Serialize.put input
     Serialize.put output
     putOptAddr assumptions
   | .check const assumptions => do
-    putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_CLAIM⟩
     Serialize.put const
     putOptAddr assumptions
   | .checkEnv root assumptions => do
-    putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_ENV_CLAIM⟩
     Serialize.put root
     putOptAddr assumptions
   | .reveal comm info => do
-    putTag4 ⟨FLAG_CLAIM, VARIANT_REVEAL_CLAIM⟩
     Serialize.put comm
     RevealConstantInfo.put info
   | .contains tree const => do
-    putTag4 ⟨FLAG_CLAIM, VARIANT_CONTAINS_CLAIM⟩
     Serialize.put tree
     Serialize.put const
   | .catalog members content assumptions => do
     -- First multi-byte claim tag: 0xE8 0x08 on the wire.
-    putTag4 ⟨FLAG_CLAIM, VARIANT_CATALOG_CLAIM⟩
     Serialize.put members
     Serialize.put content
     putOptAddr assumptions
+  | .resource root profile => do
+    Serialize.put root
+    Serialize.put profile
 
 def get : GetM Claim := do
   let tag ← getTag4
   if tag.flag != FLAG_CLAIM then
     throw s!"Claim.get: expected flag 0xE, got {tag.flag}"
+  getScope (validatorForVariant tag.size)
   if tag.size == VARIANT_EVAL_CLAIM then
     let input ← Serialize.get
     let output ← Serialize.get
@@ -553,10 +583,13 @@ def get : GetM Claim := do
     let content ← Serialize.get
     let asm ← getOptAddr
     return .catalog members content asm
+  else if tag.size == VARIANT_RESOURCE_CLAIM then
+    return .resource (← Serialize.get) (← Serialize.get)
   else
     throw s!"Claim.get: invalid claim variant {tag.size}"
 
 def ser (c : Claim) : ByteArray := runPut (put c)
+def de (bytes : ByteArray) : Except String Claim := runGetExact get bytes
 def commit (c : Claim) : Address := Address.blake3 (ser c)
 
 instance : ToString Claim where
@@ -567,6 +600,7 @@ instance : ToString Claim where
     | .reveal comm info => s!"Reveal({comm}, {repr info})"
     | .contains t c => s!"Contains({t}, {c})"
     | .catalog m c asm => s!"Catalog({m}, {c}, {asm})"
+    | .resource root profile => s!"Resource({root}, {profile})"
 
 end Claim
 
@@ -596,9 +630,11 @@ def variantOf : Ix.Claim → UInt64
   | .reveal _ _     => Ix.Claim.VARIANT_REVEAL_PROOF
   | .contains _ _   => Ix.Claim.VARIANT_CONTAINS_PROOF
   | .catalog _ _ _  => Ix.Claim.VARIANT_CATALOG_PROOF
+  | .resource _ _   => Ix.Claim.VARIANT_RESOURCE_PROOF
 
 def put (p : Proof) : PutM Unit := do
   putTag4 ⟨Ix.Claim.FLAG_PROOF, variantOf p.claim⟩
+  Ix.Claim.putScope (Ix.Claim.validatorForVariant (Ix.Claim.variantOf p.claim))
   match p.claim with
   | .eval input output asm => do
     Serialize.put input
@@ -620,13 +656,17 @@ def put (p : Proof) : PutM Unit := do
     Serialize.put members
     Serialize.put content
     Ix.Claim.putOptAddr asm
+  | .resource root profile => do
+    Serialize.put root
+    Serialize.put profile
   putTag0 ⟨p.proof.size.toUInt64⟩
   putBytes p.proof
 
 def get : GetM Proof := do
   let tag ← getTag4
   if tag.flag != Ix.Claim.FLAG_PROOF then
     throw s!"Ixon.Proof.get: expected flag 0xF, got {tag.flag}"
+  Ix.Claim.getScope (Ix.Claim.validatorForVariant (tag.size + 3))
   let claim : Ix.Claim ←
     if tag.size == Ix.Claim.VARIANT_EVAL_PROOF then do
       let input ← Serialize.get
@@ -654,17 +694,20 @@ def get : GetM Proof := do
       let content ← Serialize.get
       let asm ← Ix.Claim.getOptAddr
       pure (.catalog members content asm)
+    else if tag.size == Ix.Claim.VARIANT_RESOURCE_PROOF then do
+      pure (.resource (← Serialize.get) (← Serialize.get))
     else
       throw s!"Ixon.Proof.get: invalid proof variant {tag.size}"
   let lenTag ← getTag0
   let bytes ← getBytes lenTag.size.toNat
   pure { claim, proof := bytes }
 
 def ser (p : Proof) : ByteArray := runPut (put p)
-def de (bytes : ByteArray) : Except String Proof := runGet get bytes
+def de (bytes : ByteArray) : Except String Proof := runGetExact get bytes
 
 end Proof
 
 end Ixon
 
 end
+

Ix/Cli/CompileCmd.lean

@@ -158,6 +158,7 @@ def runCompileCmd (p : Cli.Parsed) : IO UInt32 := do
   let allowPartial := p.hasFlag "allow-partial"
   let strictAnon := p.hasFlag "anon"
   let start ← IO.monoMsNow
+  let constList ← IO.ofExcept <| Ix.Compile.prepareRegisteredConstants leanEnv constList
   let status ← if strictAnon then
       Ix.CompileM.rsCompileEnvBytesAnonFFI constList outPath allowPartial
     else
@@ -262,3 +263,4 @@ def compileCmd : Cli.Cmd := `[Cli|
 ]
 
 end
+

Ix/Cli/CompileLeanCmd.lean

@@ -53,7 +53,8 @@ def runCompileLeanCmd (p : Cli.Parsed) : IO UInt32 := do
   IO.println s!"[compile-lean] {constList.length} constants, {workers} workers"
 
   let t0 ← IO.monoMsNow
-  match ← Ix.CompileM.compileLeanConsts constList (numWorkers := workers)
+  let input ← IO.ofExcept ((Ix.Compile.compileInputFromEnv fe.env constList).mapError toString)
+  match ← Ix.CompileM.compileLeanInput input (numWorkers := workers)
       (dbg := true) with
   | .error e =>
     IO.println s!"[compile-lean] FAILED: {e}"
@@ -85,7 +86,8 @@ serialize the grounded subset)"
       let tR ← IO.monoMsNow
       let dir ← IO.FS.createTempDir
       let rustOut := dir / "rust-check.ixe"
-      let _ ← Ix.CompileM.rsCompileEnvBytesFFI constList rustOut.toString true
+      let constants ← IO.ofExcept input.prepare
+      let _ ← Ix.CompileM.rsCompileEnvBytesFFI constants rustOut.toString true
       let rustBytes ← IO.FS.readBinFile rustOut
       IO.FS.removeDirAll dir
       let tRe := (← IO.monoMsNow) - tR
@@ -120,3 +122,4 @@ def compileLeanCmd : Cli.Cmd := `[Cli|
 ]
 
 end
+

Ix/Compile/SourceContract.lean

@@ -0,0 +1,4 @@
+module
+
+public import Ix.Compile.SourceContract.Basic
+public import Ix.Compile.SourceContract.Resolve