diff --git a/Benchmarks/CheckNatAddComm.lean b/Benchmarks/CheckNatAddComm.lean index 954078f4..f5748e05 100644 --- a/Benchmarks/CheckNatAddComm.lean +++ b/Benchmarks/CheckNatAddComm.lean @@ -24,20 +24,20 @@ def main : IO Unit := do | throw (IO.userError "Merging failed") let .ok compiled := toplevel.compile | throw (IO.userError "Compilation failed") - let some funIdx := compiled.getFuncIdx `kernel_check_test - | throw (IO.userError "Aiur function not found") + let some funIdx := compiled.getFuncIdx `verify_claim + | throw (IO.userError "verify_claim entrypoint missing") let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters let env ← get_env! - let ixonEnv ← IxVM.CheckHarness.loadIxonEnv ``Nat.add_comm env - let ioBuffer := IxVM.CheckHarness.buildKernelCheckIOBuffer ixonEnv - let targetAddrBytes := IxVM.CheckHarness.kernelCheckTarget ``Nat.add_comm ixonEnv - -- check_deps=1 here: bench full transitive checking. - let input := targetAddrBytes.push 1 + let ixonEnv ← IxVM.ClaimHarness.loadIxonEnv ``Nat.add_comm env + let target ← IxVM.ClaimHarness.lookupAddr ixonEnv ``Nat.add_comm + -- `assumptions = none` = full transitive typecheck. + let witness ← IO.ofExcept <| IxVM.ClaimHarness.buildClaimWitness ixonEnv + (Ix.Claim.check target none) let _ ← bgroup "Kernel typechecking" { oneShot := true } do throughput (.Elements ixonEnv.consts.size.toUInt64 "consts") bench "check Nat.add_comm" - (aiurSystem.prove friParameters funIdx input) - ioBuffer + (aiurSystem.prove friParameters funIdx witness.input) + witness.inputIOBuffer return diff --git a/Benchmarks/IxVM.lean b/Benchmarks/IxVM.lean index e65379a7..d38c2ed2 100644 --- a/Benchmarks/IxVM.lean +++ b/Benchmarks/IxVM.lean @@ -29,8 +29,8 @@ def main : IO Unit := do let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters let env ← get_env! - let ixonEnv ← IxVM.CheckHarness.loadIxonEnv ``Nat.add_comm env - let (ioBuffer, n) := IxVM.CheckHarness.buildSerdeIOBuffer ixonEnv + let ixonEnv ← IxVM.ClaimHarness.loadIxonEnv ``Nat.add_comm env + let (ioBuffer, n) := IxVM.ClaimHarness.buildSerdeIOBuffer ixonEnv let _ ← bgroup "IxVM benchmarks" { oneShot := true } do throughput (.Elements n.toUInt64 "consts") diff --git a/Ix/IxVM.lean b/Ix/IxVM.lean index 6959a137..1ed8bf2c 100644 --- a/Ix/IxVM.lean +++ b/Ix/IxVM.lean @@ -18,7 +18,8 @@ public import Ix.IxVM.Kernel.DefEq public import Ix.IxVM.Kernel.Inductive public import Ix.IxVM.Kernel.CanonicalCheck public import Ix.IxVM.Kernel.Check -public import Ix.IxVM.CheckHarness +public import Ix.IxVM.Kernel.Claim +public import Ix.IxVM.ClaimHarness public section @@ -42,25 +43,6 @@ def entrypoints := ⟦ } } - -- `check_deps` controls whether transitive dependencies are - -- typechecked along with the target. When 1, runs `check_all` - -- (current behavior). When 0, runs `check_const` only on the target - -- — saving the per-dep `validate_const_well_scoped`, `k_check`, - -- recursor canonical-build, positivity, etc. Deps still need to be - -- in `k_consts`/`addrs` so the target's own `whnf`/`infer` can - -- resolve `Const` refs; the IOBuffer payload doesn't shrink. - pub fn kernel_check_test(target_addr: [G; 32], check_deps: G) { - let target = store(target_addr); - let (k_consts, addrs) = ingress_with_primitives(target); - match check_deps { - 0 => - let target_pos = find_addr_idx(target, addrs, 0); - let ci = load(list_lookup(k_consts, target_pos)); - check_const(ci, target_pos, k_consts, addrs), - _ => check_all(k_consts, k_consts, addrs), - } - } - fn level_cmp_tests() { -- Zero ≤ anything assert_eq!(level_leq(KLevel.Zero, KLevel.Param(0)), 1); @@ -187,6 +169,7 @@ def ixVM : Except Aiur.Global Aiur.Source.Toplevel := do let vm ← vm.merge inductive_check let vm ← vm.merge canonicalCheck let vm ← vm.merge check + let vm ← vm.merge claim vm.merge entrypoints end IxVM diff --git a/Ix/IxVM/CheckHarness.lean b/Ix/IxVM/CheckHarness.lean deleted file mode 100644 index a40f0b0d..00000000 --- a/Ix/IxVM/CheckHarness.lean +++ /dev/null @@ -1,134 +0,0 @@ -module -public import Ix.Aiur.Protocol -public import Ix.Ixon -public import Ix.CompileM -public import Ix.Common - -public section - -namespace IxVM.CheckHarness - -/-- Run the Lean → Ixon FFI pipeline for `name`'s transitive closure. -/ -def loadIxonEnv (name : Lean.Name) (leanEnv : Lean.Environment) : IO Ixon.Env := do - let constList := Lean.collectDependencies name leanEnv.constants - let rawEnv ← Ix.CompileM.rsCompileEnvFFI constList - pure rawEnv.toEnv - -/-- Compile the union of `names`'s transitive closures into one shared - Ixon env. Drivers like `KernelArena.lean` use this to pay the - Lean→Ixon compile cost once and then build per-target IOBuffers via - `buildKernelCheckIOBufferFor`. -/ -def loadSharedIxonEnv (names : Array Lean.Name) (leanEnv : Lean.Environment) : - IO Ixon.Env := do - let constList := names.foldl (init := []) fun acc n => - Lean.collectDependencies n leanEnv.constants ++ acc - let mut seen : Lean.NameSet := {} - let mut deduped : List (Lean.Name × Lean.ConstantInfo) := [] - for entry in constList do - if !seen.contains entry.fst then - seen := seen.insert entry.fst - deduped := entry :: deduped - let rawEnv ← Ix.CompileM.rsCompileEnvFFI deduped - pure rawEnv.toEnv - -/-- Walk the Constant ref-graph from `target` to compute the set of - addresses needed to type-check it. Mirrors Aiur's `load_with_deps`: - follow `Constant.refs` plus the projection's `block_addr` (the parent - Muts wrapper) for IPrj/CPrj/RPrj/DPrj. -/ -partial def closureFrom (env : Ixon.Env) (target : Address) : Std.HashSet Address := Id.run do - let mut visited : Std.HashSet Address := {} - let mut worklist : Array Address := #[target] - while !worklist.isEmpty do - let addr := worklist.back! - worklist := worklist.pop - if visited.contains addr then continue - visited := visited.insert addr - match env.consts.get? addr with - | none => pure () - | some c => - for r in c.refs do - if !visited.contains r then worklist := worklist.push r - let blockAddr? : Option Address := match c.info with - | .iPrj p => some p.block - | .cPrj p => some p.block - | .rPrj p => some p.block - | .dPrj p => some p.block - | _ => none - match blockAddr? with - | some ba => if !visited.contains ba then worklist := worklist.push ba - | none => pure () - return visited - -/-- Build the `ixon_serde_test` / `ixon_serde_blake3_bench` IOBuffer: - one entry per const, keyed by its index. Returns the buffer and the - count `n` (which the Aiur entrypoint receives as input). -/ -def buildSerdeIOBuffer (ixonEnv : Ixon.Env) : Aiur.IOBuffer × Nat := - ixonEnv.consts.valuesIter.fold (init := (default, 0)) fun (ioBuffer, i) c => - let (_, bytes) := Ixon.Serialize.put c |>.run default - (ioBuffer.extend #[.ofNat i] (bytes.data.map .ofUInt8), i + 1) - -/-- Encode a `Lean.ReducibilityHints` as a single `G` per the convention - Aiur's `load_constant_hint` decodes (opaque → 0, abbrev → 0xFFFFFFFF, - regular n → clamp(1 + n, 0xFFFFFFFE)). -/ -private def hintToG : Lean.ReducibilityHints → Aiur.G - | .opaque => .ofNat 0 - | .abbrev => .ofNat 0xFFFFFFFF - | .regular n => - let v := 1 + n.toNat - .ofNat (if v > 0xFFFFFFFE then 0xFFFFFFFE else v) - -/-- Insert all per-address entries for `addr`s satisfying `keep` into - `ioBuffer`, following the IOBuffer convention: - - | key | value | meaning | - |------------------------|----------------|---------| - | `addr` (32 G) | const bytes | primary data; empty value = `addr` is a blob | - | `addr ++ [0]` (33 G) | raw blob bytes | referenced data (verified by Aiur via blake3) | - | `addr ++ [1]` (33 G) | single G | Defn `ReducibilityHints` encoding | - - Suffix tags use `Array.push` (O(1) amortized) rather than prefix - `++ Array` (O(n) allocation). -/ -private def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool) - (ioBuffer : Aiur.IOBuffer) : Aiur.IOBuffer := Id.run do - let mut ioBuffer := ioBuffer - for (addr, c) in ixonEnv.consts do - if !keep addr then continue - let (_, bytes) := Ixon.Serialize.put c |>.run default - let key : Array Aiur.G := addr.hash.data.map .ofUInt8 - ioBuffer := ioBuffer.extend key (bytes.data.map .ofUInt8) - for (addr, rawBytes) in ixonEnv.blobs do - if !keep addr then continue - let hashKey : Array Aiur.G := addr.hash.data.map .ofUInt8 - ioBuffer := ioBuffer.extend (hashKey.push 0) - (rawBytes.data.map fun b => .ofNat b.toNat) - ioBuffer := ioBuffer.extend hashKey #[] - for (_, named) in ixonEnv.named do - if !keep named.addr then continue - match named.constMeta with - | .defn _ _ hints _ _ _ _ _ => - let hashKey : Array Aiur.G := named.addr.hash.data.map .ofUInt8 - ioBuffer := ioBuffer.extend (hashKey.push 1) #[hintToG hints] - | _ => pure () - return ioBuffer - -/-- Build the full `kernel_check_test` IOBuffer for the entire `ixonEnv`. -/ -def buildKernelCheckIOBuffer (ixonEnv : Ixon.Env) : Aiur.IOBuffer := - addEntries ixonEnv (fun _ => true) default - -/-- Blake3 address bytes of `name` (the target input to `kernel_check_test`). -/ -def kernelCheckTarget (name : Lean.Name) (ixonEnv : Ixon.Env) : Array Aiur.G := - match ixonEnv.getAddr? (Ix.Name.fromLeanName name) with - | some addr => addr.hash.data.map .ofUInt8 - | none => panic! s!"{name} not found in Ixon environment" - -/-- Build a minimal `kernel_check_test` IOBuffer reachable from `target` - in `ixonEnv`. Used by drivers (e.g. `KernelArena.lean`) that compile - a single shared env once and then check many targets against it. -/ -def buildKernelCheckIOBufferFor (ixonEnv : Ixon.Env) (target : Address) : - Aiur.IOBuffer := - let closure := closureFrom ixonEnv target - addEntries ixonEnv closure.contains default - -end IxVM.CheckHarness - -end diff --git a/Ix/IxVM/ClaimHarness.lean b/Ix/IxVM/ClaimHarness.lean new file mode 100644 index 00000000..2e93e9a6 --- /dev/null +++ b/Ix/IxVM/ClaimHarness.lean @@ -0,0 +1,266 @@ +module +public import Ix.Aiur.Protocol +public import Ix.Ixon +public import Ix.Claim +public import Ix.AssumptionTree +public import Ix.CompileM +public import Ix.Common + +public section + +/-! +# IxVM Claim harness + +Lean-side glue between `Ix.Claim` and the Aiur `verify_claim` / +`dbg_check_const` entrypoints in `Ix/IxVM/Kernel/Claim.lean`. + +The harness handles every step the Aiur side cannot: + +1. **Lean → Ixon compile**: `loadIxonEnv` / `loadSharedIxonEnv` walk + the Lean environment, run `Ix.CompileM.rsCompileEnvFFI`, and + return an `Ixon.Env` representing the constants' transitive + closure. + +2. **Closure layout**: `closureFrom` follows `Constant.refs` (+ + projection block addresses) from a target address. Mirrors the + Aiur kernel's `load_with_deps` so the IOBuffer carries exactly + what the kernel will look up. + +3. **IOBuffer population**: `addEntries` seeds the constants, blobs, + and Defn reducibility hints under their content-addressed keys + (`addr`, `addr ++ [0]`, `addr ++ [1]`). The Aiur kernel reads via + `io_get_info` + `#read_byte_stream` and blake3-verifies each + payload against its key. + +4. **Witness construction**: `buildClaimWitness` serializes any + `Ix.Claim`, seeds the bytes at `key = blake3(claim)`, pulls in the + right closure per variant, and threads any caller-supplied + `AssumptionTree`s under their merkle roots. The resulting + `ClaimWitness` packs (a) the entrypoint name (`verify_claim`), + (b) the 32-G public input (`claim_digest`), and (c) the populated + IOBuffer. + +5. **Debug witnesses**: `buildDbgCheckConst` builds the non-claim + `dbg_check_const` invocation (subject-only check, transitive + deps trusted). Used by the arena suite and + `lake exe kernel --debug-fast`. + +The serde primitive `buildSerdeIOBuffer` survives here because the +benchmark/test entrypoint `ixon_serde_test` shares the same IOBuffer +plumbing — its inputs are still indexed integers rather than blake3 +keys. + +## Helpers + +* `envCanonicalTree` — convenience that returns the canonical merkle + tree over an env's const addresses. Hands the caller a tree whose + root they can plug into a `Claim.checkEnv` claim. +* `hintToG` — `Lean.ReducibilityHints → Aiur.G` encoding shared with + Aiur's `load_constant_hint`. +-/ +namespace IxVM.ClaimHarness + +/-- Run the Lean → Ixon FFI pipeline for `name`'s transitive closure. -/ +def loadIxonEnv (name : Lean.Name) (leanEnv : Lean.Environment) : IO Ixon.Env := do + let constList := Lean.collectDependencies name leanEnv.constants + let rawEnv ← Ix.CompileM.rsCompileEnvFFI constList + pure rawEnv.toEnv + +/-- Resolve a Lean name to its `Ixon.Env` `Address`, or fail with a + descriptive `IO` error. Used by every claim/witness builder that + starts from a Lean name. -/ +def lookupAddr (ixonEnv : Ixon.Env) (name : Lean.Name) : IO Address := + match ixonEnv.getAddr? (Ix.Name.fromLeanName name) with + | some addr => pure addr + | none => throw <| IO.userError s!"{name} not found in Ixon environment" + +/-- Compile the union of `names`'s transitive closures into one shared + Ixon env. Drivers like `KernelArena.lean` use this to pay the + Lean→Ixon compile cost once and then build per-target IOBuffers via + `buildClaimWitness` / `buildDbgCheckConst`. -/ +def loadSharedIxonEnv (names : Array Lean.Name) (leanEnv : Lean.Environment) : + IO Ixon.Env := do + let mut seen : Lean.NameSet := {} + let mut deduped : Array (Lean.Name × Lean.ConstantInfo) := #[] + for n in names do + for entry in Lean.collectDependencies n leanEnv.constants do + if !seen.contains entry.fst then + seen := seen.insert entry.fst + deduped := deduped.push entry + let rawEnv ← Ix.CompileM.rsCompileEnvFFI deduped.toList + pure rawEnv.toEnv + +/-- Walk the Constant ref-graph from `target` to compute the set of + addresses needed to type-check it. Mirrors Aiur's `load_with_deps`: + follow `Constant.refs` plus the projection's `block_addr` (the parent + Muts wrapper) for IPrj/CPrj/RPrj/DPrj. -/ +partial def closureFrom (env : Ixon.Env) (target : Address) : Std.HashSet Address := Id.run do + let mut visited : Std.HashSet Address := {} + let mut worklist : Array Address := #[target] + while !worklist.isEmpty do + let addr := worklist.back! + worklist := worklist.pop + if visited.contains addr then continue + visited := visited.insert addr + let some c := env.consts.get? addr | continue + for r in c.refs do worklist := worklist.push r + match c.info with + | .iPrj p | .cPrj p => worklist := worklist.push p.block + | _ => pure () + match c.info with + | .rPrj p | .dPrj p => worklist := worklist.push p.block + | _ => pure () + return visited + +/-- Build the `ixon_serde_test` / `ixon_serde_blake3_bench` IOBuffer: + one entry per const, keyed by its index. Returns the buffer and the + count `n` (which the Aiur entrypoint receives as input). -/ +def buildSerdeIOBuffer (ixonEnv : Ixon.Env) : Aiur.IOBuffer × Nat := + ixonEnv.consts.valuesIter.fold (init := (default, 0)) fun (ioBuffer, i) c => + let (_, bytes) := Ixon.Serialize.put c |>.run default + (ioBuffer.extend #[.ofNat i] (bytes.data.map .ofUInt8), i + 1) + +/-- Encode a `Lean.ReducibilityHints` as a single `G` per the convention + Aiur's `load_constant_hint` decodes (opaque → 0, abbrev → 0xFFFFFFFF, + regular n → clamp(1 + n, 0xFFFFFFFE)). -/ +private def hintToG : Lean.ReducibilityHints → Aiur.G + | .opaque => .ofNat 0 + | .abbrev => .ofNat 0xFFFFFFFF + | .regular n => .ofNat (min (1 + n.toNat) 0xFFFFFFFE) + +/-- Insert all per-address entries for `addr`s satisfying `keep` into + `ioBuffer`, following the IOBuffer convention: + + | key | value | meaning | + |------------------------|----------------|---------| + | `addr` (32 G) | const bytes | primary data; empty value = `addr` is a blob | + | `addr ++ [0]` (33 G) | raw blob bytes | referenced data (verified by Aiur via blake3) | + | `addr ++ [1]` (33 G) | single G | Defn `ReducibilityHints` encoding | + + Suffix tags use `Array.push` (O(1) amortized) rather than prefix + `++ Array` (O(n) allocation). -/ +def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool) + (ioBuffer : Aiur.IOBuffer) : Aiur.IOBuffer := Id.run do + let mut ioBuffer := ioBuffer + for (addr, c) in ixonEnv.consts do + if !keep addr then continue + let (_, bytes) := Ixon.Serialize.put c |>.run default + let key : Array Aiur.G := addr.hash.data.map .ofUInt8 + ioBuffer := ioBuffer.extend key (bytes.data.map .ofUInt8) + for (addr, rawBytes) in ixonEnv.blobs do + if !keep addr then continue + let hashKey : Array Aiur.G := addr.hash.data.map .ofUInt8 + ioBuffer := ioBuffer.extend (hashKey.push 0) + (rawBytes.data.map fun b => .ofNat b.toNat) + ioBuffer := ioBuffer.extend hashKey #[] + for (_, named) in ixonEnv.named do + if !keep named.addr then continue + match named.constMeta with + | .defn _ _ hints _ _ _ _ _ => + let hashKey : Array Aiur.G := named.addr.hash.data.map .ofUInt8 + ioBuffer := ioBuffer.extend (hashKey.push 1) #[hintToG hints] + | _ => pure () + return ioBuffer + +-- ============================================================================ +-- Claim witness builders +-- ============================================================================ + +/-- A ready-to-run Aiur invocation: function name to dispatch, public + input (`Array G`), and the IOBuffer pre-populated with every + blake3-keyed witness payload the entrypoint will demand. -/ +structure ClaimWitness where + funcName : Lean.Name + input : Array Aiur.G + inputIOBuffer : Aiur.IOBuffer + deriving Inhabited + +/-- Convert an `Address` to its `Array G` IOBuffer-key form. -/ +@[inline] private def addrKey (a : Address) : Array Aiur.G := + a.hash.data.map .ofUInt8 + +/-- Look up the `AssumptionTree` at `root` in the caller-supplied + `trees` map and seed its serialized bytes at key=`root` in + `ioBuffer`. Aiur's `load_assumption_tree` reads bytes by key and + asserts the merkle fold matches the key. Fails when the caller + didn't supply a tree the claim references. -/ +private def seedTreeAt (root : Address) + (trees : Std.HashMap Address Ix.AssumptionTree) + (ioBuffer : Aiur.IOBuffer) : Except String Aiur.IOBuffer := + match trees.get? root with + | some tree => + let bytes := Ix.AssumptionTree.ser tree + .ok (ioBuffer.extend (addrKey tree.root) (bytes.data.map .ofUInt8)) + | none => .error s!"no assumption tree supplied for root {root}" + +/-- Build the witness for `verify_claim` against `claim`. + + `trees` is a caller-supplied map of merkle-root → tree; every root + that appears in the claim (assumption root, env root, contains + tree root) MUST have an entry. `Ix.AssumptionTree.canonical` builds + the canonical sorted+padded shape if you start from a leaf list. + + Per-variant IOBuffer payload: + - `Check addr none`: closure of `addr`. + - `Check addr (some r)`: closure of `addr` + assumption tree at `r`. + - `Eval i o asm`: closure of `i ∪ o` (+ optional asm tree). + - `CheckEnv root asm`: full env entries + env-tree at `root` + (+ optional asm tree). + - `Reveal comm info`: closure of `comm`. Info bytes ride inside + the claim bytes already. + - `Contains tree target`: tree at `tree`. No const ingest. + + Returns `Except String ClaimWitness`: error message names the + missing assumption root when applicable. + + Eval-claim invocations currently hit the placeholder + `assert_eq!(0,1)` arm of `verify_claim` at proving time. -/ +def buildClaimWitness (env : Ixon.Env) (claim : Ix.Claim) + (trees : Std.HashMap Address Ix.AssumptionTree := {}) : + Except String ClaimWitness := do + let claimBytes := Ix.Claim.ser claim + let digestKey := addrKey (Address.blake3 claimBytes) + let mut ioBuffer : Aiur.IOBuffer := default + ioBuffer := ioBuffer.extend digestKey (claimBytes.data.map .ofUInt8) + let seedAsm asm buf := match asm with + | some r => seedTreeAt r trees buf + | none => .ok buf + match claim with + | .check addr asm => + ioBuffer := addEntries env (closureFrom env addr).contains ioBuffer + ioBuffer ← seedAsm asm ioBuffer + | .eval input output asm => + let inputClosure := closureFrom env input + let outputClosure := closureFrom env output + ioBuffer := addEntries env + (fun a => inputClosure.contains a || outputClosure.contains a) ioBuffer + ioBuffer ← seedAsm asm ioBuffer + | .checkEnv root asm => + ioBuffer := addEntries env (fun _ => true) ioBuffer + ioBuffer ← seedTreeAt root trees ioBuffer + ioBuffer ← seedAsm asm ioBuffer + | .reveal comm _info => + ioBuffer := addEntries env (closureFrom env comm).contains ioBuffer + | .contains tree _target => + ioBuffer ← seedTreeAt tree trees ioBuffer + return { funcName := `verify_claim + input := digestKey, inputIOBuffer := ioBuffer } + +/-- Canonical merkle tree over every const address in `env`. Returns + `none` for an empty env. Convenience for callers that want to + issue a `CheckEnv` claim against the env's canonical merkle root. -/ +def envCanonicalTree (env : Ixon.Env) : Option Ix.AssumptionTree := + Ix.AssumptionTree.canonical (env.consts.keys.toArray) + +/-- Build the witness for the debug `dbg_check_const` Aiur entrypoint. + *Not a claim*: subject-only check, transitive deps trusted. Used by + the arena suite and `lake exe kernel --debug-fast`. -/ +def buildDbgCheckConst (env : Ixon.Env) (target : Address) : ClaimWitness := + let closure := closureFrom env target + let ioBuffer := addEntries env closure.contains default + { funcName := `dbg_check_const + input := addrKey target, inputIOBuffer := ioBuffer } + +end IxVM.ClaimHarness + +end diff --git a/Ix/IxVM/Kernel/Claim.lean b/Ix/IxVM/Kernel/Claim.lean new file mode 100644 index 00000000..26c7b008 --- /dev/null +++ b/Ix/IxVM/Kernel/Claim.lean @@ -0,0 +1,1030 @@ +/- + # Aiur kernel claim dispatcher + + The flow mirrors how constants are loaded: hash the bytes, assert + equality with the supplied digest, deserialize once into an Aiur + ADT, and use the structured value. No scattered inline-parse + comparisons. + + claim_digest ── IOBuffer ─▶ claim_bytes + │ + ▼ + blake3 assert + │ + ▼ + get_claim ◀ deserialize + │ + ▼ + match Claim variant ◀ structured use + + Wire format mirrors `Ix/Claim.lean`: + + Variant 3 EvalClaim (input output : Addr) (asm : Opt Addr) + Variant 4 CheckClaim (const : Addr) (asm : Opt Addr) + Variant 5 CheckEnvClaim (root : Addr) (asm : Opt Addr) + Variant 6 RevealClaim (comm : Addr) (info : RevealConstantInfo) + Variant 7 ContainsClaim (tree : Addr) (const : Addr) + + Eval is the only `run_*` arm still placeholder — Rust kernel has + not pinned reduction semantics yet. +-/ +module +public import Ix.Aiur.Meta +public import Ix.IxVM.KernelTypes +public import Ix.IxVM.Ingress +public import Ix.IxVM.IxonSerialize +public import Ix.IxVM.IxonDeserialize +public import Ix.IxVM.Kernel.Check + +public section + +namespace IxVM + +def claim := ⟦ + -- ============================================================================ + -- Reveal-specific ADT mirror. `RevealConstantInfo` parallels + -- `ConstantInfo` (from `Ix/IxVM/Ixon.lean`) but every payload field + -- is wrapped in `Option‹…›` for selective revelation, and Expr + -- fields are replaced by their content-hashed `Addr`. The shape is + -- a 1:1 copy of `Ix.RevealConstantInfo` in `Ix/Claim.lean`. + -- ============================================================================ + + -- (ruleIdx, fields, rhs_addr). `rhs_addr` = blake3(put_expr rhs). + enum RevealRecursorRule { + Mk(U64, U64, Addr) + } + + -- (isUnsafe, lvls, cidx, params, fields, typ). + enum RevealConstructorInfo { + Mk(Option‹G›, Option‹U64›, Option‹U64›, + Option‹U64›, Option‹U64›, Option‹Addr›) + } + + enum RevealMutConstInfo { + Defn(Option‹DefKind›, Option‹DefinitionSafety›, + Option‹U64›, Option‹Addr›, Option‹Addr›), + Indc(Option‹G›, Option‹G›, Option‹G›, + Option‹U64›, Option‹U64›, Option‹U64›, Option‹U64›, + Option‹Addr›, + Option‹List‹(U64, RevealConstructorInfo)››), + Recr(Option‹G›, Option‹G›, + Option‹U64›, Option‹U64›, Option‹U64›, + Option‹U64›, Option‹U64›, + Option‹Addr›, Option‹List‹RevealRecursorRule››) + } + + enum RevealConstantInfo { + Defn(Option‹DefKind›, Option‹DefinitionSafety›, + Option‹U64›, Option‹Addr›, Option‹Addr›), + Recr(Option‹G›, Option‹G›, + Option‹U64›, Option‹U64›, Option‹U64›, + Option‹U64›, Option‹U64›, + Option‹Addr›, Option‹List‹RevealRecursorRule››), + Axio(Option‹G›, Option‹U64›, Option‹Addr›), + Quot(Option‹QuotKind›, Option‹U64›, Option‹Addr›), + CPrj(Option‹U64›, Option‹U64›, Option‹Addr›), + RPrj(Option‹U64›, Option‹Addr›), + IPrj(Option‹U64›, Option‹Addr›), + DPrj(Option‹U64›, Option‹Addr›), + Muts(List‹(U64, RevealMutConstInfo)›) + } + + -- The full claim ADT — parallels `Ix.Claim` in `Ix/Claim.lean`. + enum Claim { + Eval(Addr, Addr, Option‹Addr›), + Check(Addr, Option‹Addr›), + CheckEnv(Addr, Option‹Addr›), + Reveal(Addr, RevealConstantInfo), + Contains(Addr, Addr) + } + + -- ============================================================================ + -- Wire-format helpers shared across the deserializers. + -- ============================================================================ + + -- `Option
` per `Ix/Claim.lean::putOptAddr` (top-level + -- `assumptions` slot, NOT the bitmask-gated reveal-fields form). + -- [0x00] → none + -- [0x01][addr:32] → some addr + fn get_opt_addr(stream: ByteStream) -> (Option‹Addr›, ByteStream) { + let (tag, s) = read_byte(stream); + match tag { + 0 => (Option.None, s), + 1 => + let (addr, s2) = get_address(s); + (Option.Some(addr), s2), + } + } + + -- Bitmask-gated decoders for the per-field Reveal payloads. + fn get_opt_u64_masked(mb: G, stream: ByteStream) + -> (Option‹U64›, ByteStream) { + match mb { + 0 => (Option.None, stream), + _ => + let (n, s) = get_tag0(stream); + (Option.Some(n), s), + } + } + + fn get_opt_addr_masked(mb: G, stream: ByteStream) + -> (Option‹Addr›, ByteStream) { + match mb { + 0 => (Option.None, stream), + _ => + let (a, s) = get_address(stream); + (Option.Some(a), s), + } + } + + fn get_opt_bool_masked(mb: G, stream: ByteStream) + -> (Option‹G›, ByteStream) { + match mb { + 0 => (Option.None, stream), + _ => + let (b, s) = read_byte(stream); + (Option.Some(b), s), + } + } + + fn get_opt_def_kind_masked(mb: G, stream: ByteStream) + -> (Option‹DefKind›, ByteStream) { + match mb { + 0 => (Option.None, stream), + _ => + let (b, s) = read_byte(stream); + match b { + 0 => (Option.Some(DefKind.Definition), s), + 1 => (Option.Some(DefKind.Opaque), s), + 2 => (Option.Some(DefKind.Theorem), s), + }, + } + } + + fn get_opt_def_safety_masked(mb: G, stream: ByteStream) + -> (Option‹DefinitionSafety›, ByteStream) { + match mb { + 0 => (Option.None, stream), + _ => + let (b, s) = read_byte(stream); + match b { + 0 => (Option.Some(DefinitionSafety.Unsafe), s), + 1 => (Option.Some(DefinitionSafety.Safe), s), + 2 => (Option.Some(DefinitionSafety.Partial), s), + }, + } + } + + fn get_opt_quot_kind_masked(mb: G, stream: ByteStream) + -> (Option‹QuotKind›, ByteStream) { + match mb { + 0 => (Option.None, stream), + _ => + let (b, s) = read_byte(stream); + match b { + 0 => (Option.Some(QuotKind.Typ), s), + 1 => (Option.Some(QuotKind.Ctor), s), + 2 => (Option.Some(QuotKind.Lift), s), + 3 => (Option.Some(QuotKind.Ind), s), + }, + } + } + + -- ============================================================================ + -- RevealRecursorRule list parser. + -- Wire: `Tag0(count) + count × (Tag0(idx) + Tag0(fields) + Address)`. + -- ============================================================================ + fn get_reveal_rule(stream: ByteStream) -> (RevealRecursorRule, ByteStream) { + let (rule_idx, s) = get_tag0(stream); + let (fields, s) = get_tag0(s); + let (rhs, s) = get_address(s); + (RevealRecursorRule.Mk(rule_idx, fields, rhs), s) + } + + fn get_reveal_rule_list_inner(stream: ByteStream, count: U64) + -> (List‹RevealRecursorRule›, ByteStream) { + match u64_is_zero(count) { + 1 => (store(ListNode.Nil), stream), + _ => + let (rule, s) = get_reveal_rule(stream); + let (rest, s2) = get_reveal_rule_list_inner(s, relaxed_u64_pred(count)); + (store(ListNode.Cons(rule, rest)), s2), + } + } + + fn get_opt_rule_list_masked(mb: G, stream: ByteStream) + -> (Option‹List‹RevealRecursorRule››, ByteStream) { + match mb { + 0 => (Option.None, stream), + _ => + let (count, s) = get_tag0(stream); + let (rules, s2) = get_reveal_rule_list_inner(s, count); + (Option.Some(rules), s2), + } + } + + -- ============================================================================ + -- RevealConstructorInfo parser. 6 optional fields, mask bits 0..5. + -- ============================================================================ + fn get_reveal_ctor_info(stream: ByteStream) + -> (RevealConstructorInfo, ByteStream) { + let (mask, s) = get_tag0(stream); + let mask_lo = u8_bit_decomposition(mask[0]); + let [b0, b1, b2, b3, b4, b5, _, _] = mask_lo; + let (is_unsafe, s) = get_opt_bool_masked(b0, s); + let (lvls, s) = get_opt_u64_masked(b1, s); + let (cidx, s) = get_opt_u64_masked(b2, s); + let (params, s) = get_opt_u64_masked(b3, s); + let (fields, s) = get_opt_u64_masked(b4, s); + let (typ, s) = get_opt_addr_masked(b5, s); + (RevealConstructorInfo.Mk(is_unsafe, lvls, cidx, params, fields, typ), s) + } + + fn get_ctor_entry(stream: ByteStream) + -> ((U64, RevealConstructorInfo), ByteStream) { + let (idx, s) = get_tag0(stream); + let (info, s) = get_reveal_ctor_info(s); + ((idx, info), s) + } + + fn get_ctor_entry_list_inner(stream: ByteStream, count: U64) + -> (List‹(U64, RevealConstructorInfo)›, ByteStream) { + match u64_is_zero(count) { + 1 => (store(ListNode.Nil), stream), + _ => + let (entry, s) = get_ctor_entry(stream); + let (rest, s2) = get_ctor_entry_list_inner(s, relaxed_u64_pred(count)); + (store(ListNode.Cons(entry, rest)), s2), + } + } + + fn get_opt_ctor_entry_list_masked(mb: G, stream: ByteStream) + -> (Option‹List‹(U64, RevealConstructorInfo)››, ByteStream) { + match mb { + 0 => (Option.None, stream), + _ => + let (count, s) = get_tag0(stream); + let (list, s2) = get_ctor_entry_list_inner(s, count); + (Option.Some(list), s2), + } + } + + -- ============================================================================ + -- RevealMutConstInfo parser. variant + mask + per-bit fields. + -- ============================================================================ + fn get_reveal_mut_const_info(stream: ByteStream) + -> (RevealMutConstInfo, ByteStream) { + let (variant, s) = read_byte(stream); + let (mask, s) = get_tag0(s); + let mask_lo = u8_bit_decomposition(mask[0]); + let [b0, b1, b2, b3, b4, b5, b6, b7] = mask_lo; + let mask_hi = u8_bit_decomposition(mask[1]); + let [b8, _, _, _, _, _, _, _] = mask_hi; + match variant { + 0 => + let (kind, s) = get_opt_def_kind_masked(b0, s); + let (safety, s) = get_opt_def_safety_masked(b1, s); + let (lvls, s) = get_opt_u64_masked(b2, s); + let (typ, s) = get_opt_addr_masked(b3, s); + let (value, s) = get_opt_addr_masked(b4, s); + (RevealMutConstInfo.Defn(kind, safety, lvls, typ, value), s), + 1 => + let (is_recr, s) = get_opt_bool_masked(b0, s); + let (refl, s) = get_opt_bool_masked(b1, s); + let (is_unsafe, s) = get_opt_bool_masked(b2, s); + let (lvls, s) = get_opt_u64_masked(b3, s); + let (params, s) = get_opt_u64_masked(b4, s); + let (indices, s) = get_opt_u64_masked(b5, s); + let (nested, s) = get_opt_u64_masked(b6, s); + let (typ, s) = get_opt_addr_masked(b7, s); + let (ctors, s) = get_opt_ctor_entry_list_masked(b8, s); + (RevealMutConstInfo.Indc(is_recr, refl, is_unsafe, lvls, params, + indices, nested, typ, ctors), s), + 2 => + let (k, s) = get_opt_bool_masked(b0, s); + let (is_unsafe, s) = get_opt_bool_masked(b1, s); + let (lvls, s) = get_opt_u64_masked(b2, s); + let (params, s) = get_opt_u64_masked(b3, s); + let (indices, s) = get_opt_u64_masked(b4, s); + let (motives, s) = get_opt_u64_masked(b5, s); + let (minors, s) = get_opt_u64_masked(b6, s); + let (typ, s) = get_opt_addr_masked(b7, s); + let (rules, s) = get_opt_rule_list_masked(b8, s); + (RevealMutConstInfo.Recr(k, is_unsafe, lvls, params, indices, + motives, minors, typ, rules), s), + } + } + + fn get_mut_entry(stream: ByteStream) + -> ((U64, RevealMutConstInfo), ByteStream) { + let (idx, s) = get_tag0(stream); + let (info, s) = get_reveal_mut_const_info(s); + ((idx, info), s) + } + + fn get_mut_entry_list_inner(stream: ByteStream, count: U64) + -> (List‹(U64, RevealMutConstInfo)›, ByteStream) { + match u64_is_zero(count) { + 1 => (store(ListNode.Nil), stream), + _ => + let (entry, s) = get_mut_entry(stream); + let (rest, s2) = get_mut_entry_list_inner(s, relaxed_u64_pred(count)); + (store(ListNode.Cons(entry, rest)), s2), + } + } + + -- ============================================================================ + -- RevealConstantInfo parser. `variant + mask:Tag0 + per-bit fields`. + -- ============================================================================ + fn get_reveal_info(stream: ByteStream) -> (RevealConstantInfo, ByteStream) { + let (variant, s) = read_byte(stream); + let (mask, s) = get_tag0(s); + let mask_lo = u8_bit_decomposition(mask[0]); + let [b0, b1, b2, b3, b4, b5, b6, b7] = mask_lo; + let mask_hi = u8_bit_decomposition(mask[1]); + let [b8, _, _, _, _, _, _, _] = mask_hi; + match variant { + 0 => + let (kind, s) = get_opt_def_kind_masked(b0, s); + let (safety, s) = get_opt_def_safety_masked(b1, s); + let (lvls, s) = get_opt_u64_masked(b2, s); + let (typ, s) = get_opt_addr_masked(b3, s); + let (value, s) = get_opt_addr_masked(b4, s); + (RevealConstantInfo.Defn(kind, safety, lvls, typ, value), s), + 1 => + let (k, s) = get_opt_bool_masked(b0, s); + let (is_unsafe, s) = get_opt_bool_masked(b1, s); + let (lvls, s) = get_opt_u64_masked(b2, s); + let (params, s) = get_opt_u64_masked(b3, s); + let (indices, s) = get_opt_u64_masked(b4, s); + let (motives, s) = get_opt_u64_masked(b5, s); + let (minors, s) = get_opt_u64_masked(b6, s); + let (typ, s) = get_opt_addr_masked(b7, s); + let (rules, s) = get_opt_rule_list_masked(b8, s); + (RevealConstantInfo.Recr(k, is_unsafe, lvls, params, indices, + motives, minors, typ, rules), s), + 2 => + let (is_unsafe, s) = get_opt_bool_masked(b0, s); + let (lvls, s) = get_opt_u64_masked(b1, s); + let (typ, s) = get_opt_addr_masked(b2, s); + (RevealConstantInfo.Axio(is_unsafe, lvls, typ), s), + 3 => + let (kind, s) = get_opt_quot_kind_masked(b0, s); + let (lvls, s) = get_opt_u64_masked(b1, s); + let (typ, s) = get_opt_addr_masked(b2, s); + (RevealConstantInfo.Quot(kind, lvls, typ), s), + 4 => + let (idx, s) = get_opt_u64_masked(b0, s); + let (cidx, s) = get_opt_u64_masked(b1, s); + let (block, s) = get_opt_addr_masked(b2, s); + (RevealConstantInfo.CPrj(idx, cidx, block), s), + 5 => + let (idx, s) = get_opt_u64_masked(b0, s); + let (block, s) = get_opt_addr_masked(b1, s); + (RevealConstantInfo.RPrj(idx, block), s), + 6 => + let (idx, s) = get_opt_u64_masked(b0, s); + let (block, s) = get_opt_addr_masked(b1, s); + (RevealConstantInfo.IPrj(idx, block), s), + 7 => + let (idx, s) = get_opt_u64_masked(b0, s); + let (block, s) = get_opt_addr_masked(b1, s); + (RevealConstantInfo.DPrj(idx, block), s), + 8 => + let (components, s) = match b0 { + 0 => (store(ListNode.Nil), s), + 1 => + let (count, s2) = get_tag0(s); + get_mut_entry_list_inner(s2, count), + }; + (RevealConstantInfo.Muts(components), s), + } + } + + -- ============================================================================ + -- Claim parser. Parses Tag4(0xE, variant) wrapper + per-variant + -- payload into the `Claim` ADT. + -- ============================================================================ + fn get_claim(bytes: ByteStream) -> (Claim, ByteStream) { + let (tag, s) = get_tag4(bytes); + let (flag, size) = tag; + assert_eq!(flag, 0xE); + let variant = size[0]; + match variant { + 3 => + let (input, s) = get_address(s); + let (output, s) = get_address(s); + let (asm, s) = get_opt_addr(s); + (Claim.Eval(input, output, asm), s), + 4 => + let (c, s) = get_address(s); + let (asm, s) = get_opt_addr(s); + (Claim.Check(c, asm), s), + 5 => + let (root, s) = get_address(s); + let (asm, s) = get_opt_addr(s); + (Claim.CheckEnv(root, asm), s), + 6 => + let (comm, s) = get_address(s); + let (info, s) = get_reveal_info(s); + (Claim.Reveal(comm, info), s), + 7 => + let (tree, s) = get_address(s); + let (target, s) = get_address(s); + (Claim.Contains(tree, target), s), + } + } + + -- Load + verify a claim from the IOBuffer at key=`digest`. Mirrors + -- `load_verified_constant`: read bytes, recompute blake3, assert + -- equality, deserialize, assert no trailing data. + fn load_verified_claim(digest: [G; 32]) -> Claim { + let (idx, len) = io_get_info(digest); + let bytes = #read_byte_stream(idx, len); + let h = blake3(bytes); + assert_eq!( + [ + h[0][0], h[0][1], h[0][2], h[0][3], + h[1][0], h[1][1], h[1][2], h[1][3], + h[2][0], h[2][1], h[2][2], h[2][3], + h[3][0], h[3][1], h[3][2], h[3][3], + h[4][0], h[4][1], h[4][2], h[4][3], + h[5][0], h[5][1], h[5][2], h[5][3], + h[6][0], h[6][1], h[6][2], h[6][3], + h[7][0], h[7][1], h[7][2], h[7][3] + ], + digest + ); + let (claim, rest) = get_claim(bytes); + assert_eq!(load(rest), ListNode.Nil); + claim + } + + -- ============================================================================ + -- Content hash of an `Expr`: `blake3(put_expr expr)`. Per + -- docs/Ixon.md:970-971 — Reveal claim's `Option
` Expr + -- fields bind to this hash. + -- ============================================================================ + fn expr_addr(e_ref: &Expr) -> Addr { + let bytes = put_expr(load(e_ref), store(ListNode.Nil)); + let h = blake3(bytes); + store([ + h[0][0], h[0][1], h[0][2], h[0][3], + h[1][0], h[1][1], h[1][2], h[1][3], + h[2][0], h[2][1], h[2][2], h[2][3], + h[3][0], h[3][1], h[3][2], h[3][3], + h[4][0], h[4][1], h[4][2], h[4][3], + h[5][0], h[5][1], h[5][2], h[5][3], + h[6][0], h[6][1], h[6][2], h[6][3], + h[7][0], h[7][1], h[7][2], h[7][3] + ]) + } + + -- ============================================================================ + -- Per-field equality checks. None = no-op (selective reveal); + -- Some(claimed) = assert equality with the real field. + -- ============================================================================ + fn def_kind_tag(k: DefKind) -> G { + match k { + DefKind.Definition => 0, + DefKind.Opaque => 1, + DefKind.Theorem => 2, + } + } + + fn def_safety_tag(s: DefinitionSafety) -> G { + match s { + DefinitionSafety.Unsafe => 0, + DefinitionSafety.Safe => 1, + DefinitionSafety.Partial => 2, + } + } + + fn quot_kind_tag(k: QuotKind) -> G { + match k { + QuotKind.Typ => 0, + QuotKind.Ctor => 1, + QuotKind.Lift => 2, + QuotKind.Ind => 3, + } + } + + fn check_opt_def_kind(real: DefKind, opt: Option‹DefKind›) { + match opt { + Option.None => (), + Option.Some(claimed) => + assert_eq!(def_kind_tag(real), def_kind_tag(claimed)); + (), + } + } + + fn check_opt_def_safety(real: DefinitionSafety, + opt: Option‹DefinitionSafety›) { + match opt { + Option.None => (), + Option.Some(claimed) => + assert_eq!(def_safety_tag(real), def_safety_tag(claimed)); + (), + } + } + + fn check_opt_quot_kind(real: QuotKind, opt: Option‹QuotKind›) { + match opt { + Option.None => (), + Option.Some(claimed) => + assert_eq!(quot_kind_tag(real), quot_kind_tag(claimed)); + (), + } + } + + fn check_opt_bool(real: G, opt: Option‹G›) { + match opt { + Option.None => (), + Option.Some(claimed) => + assert_eq!(real, claimed); + (), + } + } + + fn check_opt_u64(real: U64, opt: Option‹U64›) { + match opt { + Option.None => (), + Option.Some(claimed) => + assert_eq!(real, claimed); + (), + } + } + + fn check_opt_addr(real: Addr, opt: Option‹Addr›) { + match opt { + Option.None => (), + Option.Some(claimed) => + assert_eq!(load(real), load(claimed)); + (), + } + } + + fn check_opt_expr_addr(real_e: &Expr, opt: Option‹Addr›) { + match opt { + Option.None => (), + Option.Some(claimed) => + let computed = expr_addr(real_e); + assert_eq!(load(computed), load(claimed)); + (), + } + } + + -- Walk both lists in lockstep: claimed (idx, fields, rhs_addr) per + -- entry vs real (fields, rhs:&Expr) — positional `idx` is read but + -- not asserted (matches `Ix.RevealRecursorRule.ruleIdx` semantics). + fn check_recr_rules(real: List‹RecursorRule›, + claimed: List‹RevealRecursorRule›) { + match load(claimed) { + ListNode.Nil => + match load(real) { + ListNode.Nil => (), + }, + ListNode.Cons(cr, rest_claimed) => + match load(real) { + ListNode.Cons(rr, rest_real) => + match cr { + RevealRecursorRule.Mk(_c_idx, c_fields, c_rhs) => + match rr { + RecursorRule.Mk(r_fields, r_rhs) => + assert_eq!(r_fields, c_fields); + let _ = check_opt_expr_addr(r_rhs, Option.Some(c_rhs)); + check_recr_rules(rest_real, rest_claimed), + }, + }, + }, + } + } + + fn check_opt_recr_rules(real: List‹RecursorRule›, + opt: Option‹List‹RevealRecursorRule››) { + match opt { + Option.None => (), + Option.Some(claimed) => check_recr_rules(real, claimed), + } + } + + -- Constructor revelation: compare the Constructor at position `idx` + -- in the real list against the per-field Option‹…› bits. + fn check_ctor_entry(real_list: List‹Constructor›, + idx: U64, + info: RevealConstructorInfo) { + let real_ctor = list_lookup_u64(real_list, idx); + match info { + RevealConstructorInfo.Mk(opt_unsafe, opt_lvls, opt_cidx, + opt_params, opt_fields, opt_typ) => + match real_ctor { + Constructor.Mk(r_unsafe, r_lvls, r_cidx, r_params, r_fields, r_typ) => + let _ = check_opt_bool(r_unsafe, opt_unsafe); + let _ = check_opt_u64(r_lvls, opt_lvls); + let _ = check_opt_u64(r_cidx, opt_cidx); + let _ = check_opt_u64(r_params, opt_params); + let _ = check_opt_u64(r_fields, opt_fields); + check_opt_expr_addr(r_typ, opt_typ), + }, + } + } + + fn check_ctor_entries(real_list: List‹Constructor›, + claimed: List‹(U64, RevealConstructorInfo)›) { + match load(claimed) { + ListNode.Nil => (), + ListNode.Cons(entry, rest) => + match entry { + (idx, info) => + let _ = check_ctor_entry(real_list, idx, info); + check_ctor_entries(real_list, rest), + }, + } + } + + fn check_opt_ctor_entries(real_list: List‹Constructor›, + opt: Option‹List‹(U64, RevealConstructorInfo)››) { + match opt { + Option.None => (), + Option.Some(claimed) => check_ctor_entries(real_list, claimed), + } + } + + -- MutConst revelation: dispatch on the real variant vs the claimed + -- variant; mismatched pairs fail. + fn check_mut_const(real: MutConst, claimed: RevealMutConstInfo) { + match real { + MutConst.Defn(d) => + match claimed { + RevealMutConstInfo.Defn(opt_kind, opt_safety, opt_lvls, + opt_typ, opt_value) => + match d { + Definition.Mk(r_kind, r_safety, r_lvls, r_typ, r_value) => + let _ = check_opt_def_kind(r_kind, opt_kind); + let _ = check_opt_def_safety(r_safety, opt_safety); + let _ = check_opt_u64(r_lvls, opt_lvls); + let _ = check_opt_expr_addr(r_typ, opt_typ); + check_opt_expr_addr(r_value, opt_value), + }, + }, + MutConst.Indc(i) => + match claimed { + RevealMutConstInfo.Indc(opt_recr, opt_refl, opt_unsafe, opt_lvls, + opt_params, opt_indices, opt_nested, + opt_typ, opt_ctors) => + match i { + Inductive.Mk(r_recr, r_refl, r_unsafe, r_lvls, r_params, + r_indices, r_nested, r_typ, r_ctors) => + let _ = check_opt_bool(r_recr, opt_recr); + let _ = check_opt_bool(r_refl, opt_refl); + let _ = check_opt_bool(r_unsafe, opt_unsafe); + let _ = check_opt_u64(r_lvls, opt_lvls); + let _ = check_opt_u64(r_params, opt_params); + let _ = check_opt_u64(r_indices, opt_indices); + let _ = check_opt_u64(r_nested, opt_nested); + let _ = check_opt_expr_addr(r_typ, opt_typ); + check_opt_ctor_entries(r_ctors, opt_ctors), + }, + }, + MutConst.Recr(r) => + match claimed { + RevealMutConstInfo.Recr(opt_k, opt_unsafe, opt_lvls, opt_params, + opt_indices, opt_motives, opt_minors, + opt_typ, opt_rules) => + match r { + Recursor.Mk(r_k, r_unsafe, r_lvls, r_params, r_indices, + r_motives, r_minors, r_typ, r_rules) => + let _ = check_opt_bool(r_k, opt_k); + let _ = check_opt_bool(r_unsafe, opt_unsafe); + let _ = check_opt_u64(r_lvls, opt_lvls); + let _ = check_opt_u64(r_params, opt_params); + let _ = check_opt_u64(r_indices, opt_indices); + let _ = check_opt_u64(r_motives, opt_motives); + let _ = check_opt_u64(r_minors, opt_minors); + let _ = check_opt_expr_addr(r_typ, opt_typ); + check_opt_recr_rules(r_rules, opt_rules), + }, + }, + } + } + + fn check_muts_components(real: List‹MutConst›, + claimed: List‹(U64, RevealMutConstInfo)›) { + match load(claimed) { + ListNode.Nil => (), + ListNode.Cons(entry, rest_claimed) => + match entry { + (idx, info) => + let real_mc = list_lookup_u64(real, idx); + let _ = check_mut_const(real_mc, info); + check_muts_components(real, rest_claimed), + }, + } + } + + -- ============================================================================ + -- Merkle leaf / node hash (Ix.Merkle.leafHash / nodeHash). + -- ============================================================================ + fn leaf_hash(addr: Addr) -> Addr { + let tail = put_address(addr, store(ListNode.Nil)); + let bytes = store(ListNode.Cons(0, tail)); + let h = blake3(bytes); + store([ + h[0][0], h[0][1], h[0][2], h[0][3], + h[1][0], h[1][1], h[1][2], h[1][3], + h[2][0], h[2][1], h[2][2], h[2][3], + h[3][0], h[3][1], h[3][2], h[3][3], + h[4][0], h[4][1], h[4][2], h[4][3], + h[5][0], h[5][1], h[5][2], h[5][3], + h[6][0], h[6][1], h[6][2], h[6][3], + h[7][0], h[7][1], h[7][2], h[7][3] + ]) + } + + fn node_hash(l: Addr, r: Addr) -> Addr { + let tail = put_address(l, put_address(r, store(ListNode.Nil))); + let bytes = store(ListNode.Cons(1, tail)); + let h = blake3(bytes); + store([ + h[0][0], h[0][1], h[0][2], h[0][3], + h[1][0], h[1][1], h[1][2], h[1][3], + h[2][0], h[2][1], h[2][2], h[2][3], + h[3][0], h[3][1], h[3][2], h[3][3], + h[4][0], h[4][1], h[4][2], h[4][3], + h[5][0], h[5][1], h[5][2], h[5][3], + h[6][0], h[6][1], h[6][2], h[6][3], + h[7][0], h[7][1], h[7][2], h[7][3] + ]) + } + + -- ============================================================================ + -- Assumption-tree parser / loader. Same as constants: load bytes, + -- recompute root via merkle fold, assert match. + -- ============================================================================ + fn parse_atree_body(stream: ByteStream) -> (Addr, List‹Addr›, ByteStream) { + let (tag, s) = read_byte(stream); + match tag { + 0 => + let (addr, s2) = get_address(s); + let h = leaf_hash(addr); + (h, store(ListNode.Cons(addr, store(ListNode.Nil))), s2), + 1 => + (store([0; 32]), store(ListNode.Nil), s), + 2 => + let (lh, ll, s2) = parse_atree_body(s); + let (rh, rl, s3) = parse_atree_body(s2); + let h = node_hash(lh, rh); + (h, list_concat(ll, rl), s3), + } + } + + fn load_assumption_tree(root: Addr) -> List‹Addr› { + let raw = load(root); + let (idx, len) = io_get_info(raw); + let bytes = #read_byte_stream(idx, len); + let (tag, s) = get_tag4(bytes); + let (flag, size) = tag; + assert_eq!(flag, 0xE); + assert_eq!(size[0], 2); + let (computed_root, leaves, rest) = parse_atree_body(s); + assert_eq!(load(rest), ListNode.Nil); + let computed_arr = load(computed_root); + assert_eq!(computed_arr, raw); + leaves + } + + fn addr_in_list(target: Addr, xs: List‹Addr›) -> G { + match load(xs) { + ListNode.Nil => 0, + ListNode.Cons(a, rest) => + match address_eq(target, a) { + 1 => 1, + _ => addr_in_list(target, rest), + }, + } + } + + -- ============================================================================ + -- check_all variant that skips positions whose addr is in the + -- supplied assumption-leaf list. + -- ============================================================================ + fn check_all_skipping(consts: List‹&KConstantInfo›, + top: List‹&KConstantInfo›, + addrs: List‹Addr›, + asm_leaves: List‹Addr›) { + let _ = check_canonical_block_sort(top); + check_all_skipping_iter(consts, top, addrs, asm_leaves, 0) + } + + fn check_all_skipping_iter(consts: List‹&KConstantInfo›, + top: List‹&KConstantInfo›, + addrs: List‹Addr›, + asm_leaves: List‹Addr›, + pos: G) { + match load(consts) { + ListNode.Nil => (), + ListNode.Cons(&ci, rest) => + let addr = list_lookup(addrs, pos); + match addr_in_list(addr, asm_leaves) { + 1 => + check_all_skipping_iter(rest, top, addrs, asm_leaves, pos + 1), + _ => + let _ = check_const(ci, pos, top, addrs); + check_all_skipping_iter(rest, top, addrs, asm_leaves, pos + 1), + }, + } + } + + -- ============================================================================ + -- Per-variant handlers. Each takes already-parsed claim fields. + -- ============================================================================ + fn run_check(const_addr: Addr, asm: Option‹Addr›) { + let (k_consts, addrs) = ingress_with_primitives(const_addr); + match asm { + Option.None => check_all(k_consts, k_consts, addrs), + Option.Some(asm_root) => + let asm_leaves = load_assumption_tree(asm_root); + check_all_skipping(k_consts, k_consts, addrs, asm_leaves), + } + } + + fn run_contains(tree_root: Addr, target_addr: Addr) { + let leaves = load_assumption_tree(tree_root); + assert_eq!(addr_in_list(target_addr, leaves), 1); + () + } + + fn run_check_env(env_root: Addr, asm: Option‹Addr›) { + let env_leaves = load_assumption_tree(env_root); + let asm_leaves = match asm { + Option.None => store(ListNode.Nil), + Option.Some(asm_root) => load_assumption_tree(asm_root), + }; + check_env_iter(env_leaves, asm_leaves) + } + + fn check_env_iter(env_leaves: List‹Addr›, asm_leaves: List‹Addr›) { + match load(env_leaves) { + ListNode.Nil => (), + ListNode.Cons(leaf, rest) => + match addr_in_list(leaf, asm_leaves) { + 1 => + check_env_iter(rest, asm_leaves), + _ => + let (k_consts, addrs) = ingress_with_primitives(leaf); + let target_pos = find_addr_idx(leaf, addrs, 0); + let ci = load(list_lookup(k_consts, target_pos)); + let _ = check_const(ci, target_pos, k_consts, addrs); + check_env_iter(rest, asm_leaves), + }, + } + } + + -- Reveal: real constant at `comm` must match the variant of `info` + -- AND every Some-field's claimed value must equal the real field. + fn run_reveal(comm_addr: Addr, info: RevealConstantInfo) { + let c = load_verified_constant(comm_addr); + match c { + Constant.Mk(ci, _, _, _) => + match ci { + ConstantInfo.Defn(d) => + match info { + RevealConstantInfo.Defn(opt_kind, opt_safety, opt_lvls, + opt_typ, opt_value) => + match d { + Definition.Mk(r_kind, r_safety, r_lvls, r_typ, r_value) => + let _ = check_opt_def_kind(r_kind, opt_kind); + let _ = check_opt_def_safety(r_safety, opt_safety); + let _ = check_opt_u64(r_lvls, opt_lvls); + let _ = check_opt_expr_addr(r_typ, opt_typ); + check_opt_expr_addr(r_value, opt_value), + }, + }, + ConstantInfo.Recr(r) => + match info { + RevealConstantInfo.Recr(opt_k, opt_unsafe, opt_lvls, opt_params, + opt_indices, opt_motives, opt_minors, + opt_typ, opt_rules) => + match r { + Recursor.Mk(r_k, r_unsafe, r_lvls, r_params, r_indices, + r_motives, r_minors, r_typ, r_rules) => + let _ = check_opt_bool(r_k, opt_k); + let _ = check_opt_bool(r_unsafe, opt_unsafe); + let _ = check_opt_u64(r_lvls, opt_lvls); + let _ = check_opt_u64(r_params, opt_params); + let _ = check_opt_u64(r_indices, opt_indices); + let _ = check_opt_u64(r_motives, opt_motives); + let _ = check_opt_u64(r_minors, opt_minors); + let _ = check_opt_expr_addr(r_typ, opt_typ); + check_opt_recr_rules(r_rules, opt_rules), + }, + }, + ConstantInfo.Axio(a) => + match info { + RevealConstantInfo.Axio(opt_unsafe, opt_lvls, opt_typ) => + match a { + Axiom.Mk(r_unsafe, r_lvls, r_typ) => + let _ = check_opt_bool(r_unsafe, opt_unsafe); + let _ = check_opt_u64(r_lvls, opt_lvls); + check_opt_expr_addr(r_typ, opt_typ), + }, + }, + ConstantInfo.Quot(q) => + match info { + RevealConstantInfo.Quot(opt_kind, opt_lvls, opt_typ) => + match q { + Quotient.Mk(r_kind, r_lvls, r_typ) => + let _ = check_opt_quot_kind(r_kind, opt_kind); + let _ = check_opt_u64(r_lvls, opt_lvls); + check_opt_expr_addr(r_typ, opt_typ), + }, + }, + ConstantInfo.CPrj(p) => + match info { + RevealConstantInfo.CPrj(opt_idx, opt_cidx, opt_block) => + match p { + ConstructorProj.Mk(r_idx, r_cidx, r_block) => + let _ = check_opt_u64(r_idx, opt_idx); + let _ = check_opt_u64(r_cidx, opt_cidx); + check_opt_addr(r_block, opt_block), + }, + }, + ConstantInfo.RPrj(p) => + match info { + RevealConstantInfo.RPrj(opt_idx, opt_block) => + match p { + RecursorProj.Mk(r_idx, r_block) => + let _ = check_opt_u64(r_idx, opt_idx); + check_opt_addr(r_block, opt_block), + }, + }, + ConstantInfo.IPrj(p) => + match info { + RevealConstantInfo.IPrj(opt_idx, opt_block) => + match p { + InductiveProj.Mk(r_idx, r_block) => + let _ = check_opt_u64(r_idx, opt_idx); + check_opt_addr(r_block, opt_block), + }, + }, + ConstantInfo.DPrj(p) => + match info { + RevealConstantInfo.DPrj(opt_idx, opt_block) => + match p { + DefinitionProj.Mk(r_idx, r_block) => + let _ = check_opt_u64(r_idx, opt_idx); + check_opt_addr(r_block, opt_block), + }, + }, + ConstantInfo.Muts(real_mc_list) => + match info { + RevealConstantInfo.Muts(claimed_components) => + check_muts_components(real_mc_list, claimed_components), + }, + }, + } + } + + fn run_eval(input: Addr, output: Addr, asm: Option‹Addr›) { + -- Eval semantics undefined upstream; placeholder until Rust kernel + -- pins them. + assert_eq!(0, 1); + () + } + + -- ============================================================================ + -- Top-level entrypoint. + -- ============================================================================ + -- + -- Public input: 32-G blake3 digest of `Claim.ser claim`. Flow + -- mirrors `load_verified_constant`: hash-verified bytes deserialize + -- into a typed `Claim`, then dispatch. + pub fn verify_claim(claim_digest: [G; 32]) { + let claim = load_verified_claim(claim_digest); + match claim { + Claim.Eval(input, output, asm) => run_eval(input, output, asm), + Claim.Check(c, asm) => run_check(c, asm), + Claim.CheckEnv(root, asm) => run_check_env(root, asm), + Claim.Reveal(comm, info) => run_reveal(comm, info), + Claim.Contains(tree, target) => run_contains(tree, target), + } + } + + -- ============================================================================ + -- dbg_check_const: NON-CLAIM debug entrypoint. Subject-only check, + -- transitive deps trusted. Used by the arena suite and `lake exe + -- kernel --debug-fast`. Verifier policy must reject this funcidx + -- as a production claim. + -- ============================================================================ + pub fn dbg_check_const(target_addr: [G; 32]) { + let target = store(target_addr); + let (k_consts, addrs) = ingress_with_primitives(target); + let target_pos = find_addr_idx(target, addrs, 0); + let ci = load(list_lookup(k_consts, target_pos)); + check_const(ci, target_pos, k_consts, addrs) + } +⟧ + +end IxVM + +end diff --git a/Kernel.lean b/Kernel.lean index 54fe8019..1cef44e4 100644 --- a/Kernel.lean +++ b/Kernel.lean @@ -15,7 +15,8 @@ def parseName (arg : String) : Lean.Name := def main (args : List String) : IO UInt32 := do let env ← get_env! let dbg := args.contains "--dbg" - let args := args.filter (· != "--dbg") + let debugFast := args.contains "--debug-fast" + let args := args.filter fun a => a != "--dbg" && a != "--debug-fast" let toplevel ← match IxVM.ixVM with | .error e => IO.eprintln s!"Toplevel merging failed: {e}"; return 1 | .ok t => pure t @@ -23,12 +24,12 @@ def main (args : List String) : IO UInt32 := do let decls ← match toplevel.mkDecls with | .error e => IO.eprintln s!"mkDecls failed: {e}"; return 1 | .ok d => pure d - pure (interpCheck decls · env) + pure (interpCheck decls debugFast · env) else let compiled ← match toplevel.compile with | .error e => IO.eprintln s!"Compilation failed: {e}"; return 1 | .ok c => pure c - pure (check compiled · env) + pure (check compiled debugFast · env) if args.isEmpty then for (name, _) in env.constants do let res ← run name @@ -43,10 +44,25 @@ def main (args : List String) : IO UInt32 := do if res ≠ 0 then return res pure 0 where - check compiled name env : IO UInt32 := do + -- Build the test case for `name`. `debugFast = false` → claim path + -- (full transitive typecheck); `debugFast = true` → `dbg_check_const` + -- (subject only, trust deps). + mkTestCase debugFast name env : IO AiurTestCase := do + if debugFast then + let ixonEnv ← IxVM.ClaimHarness.loadIxonEnv name env + let target ← IxVM.ClaimHarness.lookupAddr ixonEnv name + let witness := IxVM.ClaimHarness.buildDbgCheckConst ixonEnv target + pure { functionName := witness.funcName + label := s!"Kernel check {name}" + input := witness.input, inputIOBuffer := witness.inputIOBuffer + expectedIOBuffer := witness.inputIOBuffer + interpret := false, executionOnly := true } + else + kernelCheck name env + check compiled debugFast name env : IO UInt32 := do IO.println s!"Typechecking {name}" (← IO.getStdout).flush - let testCase ← kernelCheck name env + let testCase ← mkTestCase debugFast name env let funIdx := compiled.getFuncIdx testCase.functionName |>.get! match compiled.bytecode.execute funIdx testCase.input testCase.inputIOBuffer with | .error e => @@ -62,10 +78,10 @@ where let stats := Aiur.computeStats compiled queryCounts Aiur.printStats stats pure 0 - interpCheck decls name env : IO UInt32 := do + interpCheck decls debugFast name env : IO UInt32 := do IO.println s!"Interpreting {name}" (← IO.getStdout).flush - let testCase ← kernelCheck name env + let testCase ← mkTestCase debugFast name env let funcName := Aiur.Global.mk testCase.functionName -- Get function's input types to properly unflatten the input array let inputTypes ← match decls.getByKey funcName with diff --git a/Tests/Ix/IxVM.lean b/Tests/Ix/IxVM.lean index 974b4828..2826e798 100644 --- a/Tests/Ix/IxVM.lean +++ b/Tests/Ix/IxVM.lean @@ -1,10 +1,11 @@ module public import Ix.Meta -public import Ix.IxVM.CheckHarness +public import Ix.AssumptionTree +public import Ix.IxVM.ClaimHarness public import Tests.Aiur.Common -open IxVM.CheckHarness +open IxVM.ClaimHarness /-! # Aiur kernel test fixtures @@ -18,7 +19,8 @@ Test-purpose declarations exercised by the `ixvm` test runner. Layout: * `serdeNatAddComm` — Ixon serialize/deserialize round-trip via the `ixon_serde_test` Aiur entrypoint. * `kernelCheck` / `kernelChecks` — single-constant and curated-list - runners against the `kernel_check_test` Aiur entrypoint. + runners against the `verify_claim` Aiur entrypoint, driving a + `Ix.Claim.check addr none` claim. -/ /-! ## Primitive reduction theorems -/ @@ -91,16 +93,17 @@ public def serdeNatAddComm (env : Lean.Environment) : IO AiurTestCase := do expectedIOBuffer := ioBuffer interpret := false, executionOnly := true } -/-- Build a `kernel_check_test` invocation for `name` with full - transitive checking (`check_deps = 1`). -/ +/-- Build a `verify_claim` invocation for `name` driving the claim + `Ix.Claim.check addr none` — fully transitive typecheck of the + target's closure. -/ public def kernelCheck (name : Lean.Name) (env : Lean.Environment) : IO AiurTestCase := do let ixonEnv ← loadIxonEnv name env - let ioBuffer := buildKernelCheckIOBuffer ixonEnv - let targetAddrBytes := kernelCheckTarget name ixonEnv - pure { functionName := `kernel_check_test, label := s!"Kernel check {name}" - input := targetAddrBytes.push 1, inputIOBuffer := ioBuffer - expectedIOBuffer := ioBuffer + let target ← lookupAddr ixonEnv name + let witness ← IO.ofExcept <| buildClaimWitness ixonEnv (Ix.Claim.check target none) + pure { functionName := witness.funcName, label := s!"Kernel check {name}" + input := witness.input, inputIOBuffer := witness.inputIOBuffer + expectedIOBuffer := witness.inputIOBuffer interpret := false, executionOnly := true } /-- Names listed as strings to dodge name-quotation parser issues with @@ -137,3 +140,134 @@ private def nameOfString (str : String) : Lean.Name := public def kernelChecks (env : Lean.Environment) : IO (List AiurTestCase) := kernelCheckNames.map nameOfString |>.mapM (kernelCheck · env) + +/-! ## Claim variant smoke tests + +Each builds an `AiurTestCase` exercising one of the non-`Check-None` +arms of `verify_claim`. All seven tests share a single Ixon env +built once over `{Nat.zero, Nat.add_comm}` — `Nat.zero` for its +small CPrj + Muts (the `Nat` block), `Nat.add_comm` for its Defn +theorems. Loading once instead of per-test cuts Lean→Ixon compile +work by ~6×. -/ + +/-- Wrap a `ClaimWitness` as an execution-only `AiurTestCase`. -/ +private def asTestCase (label : String) (witness : ClaimWitness) : AiurTestCase := + { functionName := witness.funcName, label + input := witness.input, inputIOBuffer := witness.inputIOBuffer + expectedIOBuffer := witness.inputIOBuffer + interpret := false, executionOnly := true } + +/-- Locate the first constant in `env.consts` whose `ConstantInfo` + satisfies `pred`, or fail with `IO.userError`. -/ +private def findConstWithOrThrow (ixonEnv : Ixon.Env) (label : String) + (pred : Ixon.ConstantInfo → Bool) : IO (Address × Ixon.ConstantInfo) := do + for (addr, c) in ixonEnv.consts do + if pred c.info then return (addr, c.info) + throw <| IO.userError s!"no {label} const found in shared smoke env" + +/-- Single-entry HashMap for one `(root, tree)` pairing. -/ +private def singletonTrees (tree : Ix.AssumptionTree) : + Std.HashMap Address Ix.AssumptionTree := + ({} : Std.HashMap _ _).insert tree.root tree + +/-- `Check` claim with `assumptions = some tree.root` covering every + transitive dep — kernel ends up checking only the subject. -/ +public def claimCheckWithAsm (ixonEnv : Ixon.Env) : IO AiurTestCase := do + let target ← lookupAddr ixonEnv ``Nat.zero + let closure := closureFrom ixonEnv target + let depLeaves : Array Address := + closure.fold (init := #[]) fun acc a => + if a == target then acc else acc.push a + let some tree := Ix.AssumptionTree.canonical depLeaves + | throw <| IO.userError "deps unexpectedly empty for Nat.zero" + let witness ← IO.ofExcept <| buildClaimWitness ixonEnv + (Ix.Claim.check target (some tree.root)) (singletonTrees tree) + pure (asTestCase "Claim Check with-asm (Nat.zero)" witness) + +/-- `Contains` claim against a synthetic 3-leaf merkle tree. -/ +public def claimContains : IO AiurTestCase := do + let a : Address := ⟨⟨Array.replicate 32 0x11⟩⟩ + let b : Address := ⟨⟨Array.replicate 32 0x22⟩⟩ + let c : Address := ⟨⟨Array.replicate 32 0x33⟩⟩ + let some tree := Ix.AssumptionTree.canonical #[a, b, c] + | throw <| IO.userError "Contains tree build failed" + let witness ← IO.ofExcept <| buildClaimWitness ({} : Ixon.Env) + (Ix.Claim.contains tree.root b) (singletonTrees tree) + pure (asTestCase "Claim Contains (synthetic 3-leaf)" witness) + +/-- `CheckEnv` claim over the shared smoke env. -/ +public def claimCheckEnv (ixonEnv : Ixon.Env) : IO AiurTestCase := do + let some tree := envCanonicalTree ixonEnv + | throw <| IO.userError "envCanonicalTree empty" + let witness ← IO.ofExcept <| buildClaimWitness ixonEnv + (Ix.Claim.checkEnv tree.root none) (singletonTrees tree) + pure (asTestCase "Claim CheckEnv (shared smoke env)" witness) + +/-- `Reveal` Defn with `kind` + `safety` only — exercises the + enum-tag compare path with no Expr hashing. -/ +public def claimRevealDefnFields (ixonEnv : Ixon.Env) : IO AiurTestCase := do + let (comm, info) ← findConstWithOrThrow ixonEnv "Defn" + fun ci => match ci with | .defn _ => true | _ => false + let .defn d := info + | throw <| IO.userError "findConstWith returned non-Defn" + let revealInfo : Ix.RevealConstantInfo := + .defn (some d.kind) (some d.safety) none none none + let witness ← IO.ofExcept <| buildClaimWitness ixonEnv (Ix.Claim.reveal comm revealInfo) + pure (asTestCase "Claim Reveal Defn (kind+safety)" witness) + +/-- `Reveal` CPrj — projection idx, cidx, block fields. -/ +public def claimRevealCPrj (ixonEnv : Ixon.Env) : IO AiurTestCase := do + let (comm, info) ← findConstWithOrThrow ixonEnv "CPrj" + fun ci => match ci with | .cPrj _ => true | _ => false + let .cPrj p := info + | throw <| IO.userError "findConstWith returned non-CPrj" + let revealInfo : Ix.RevealConstantInfo := + .cPrj (some p.idx) (some p.cidx) (some p.block) + let witness ← IO.ofExcept <| buildClaimWitness ixonEnv (Ix.Claim.reveal comm revealInfo) + pure (asTestCase "Claim Reveal CPrj (all fields)" witness) + +/-- `Reveal` Defn `typ` via content-hash binding — exercises the + Aiur `expr_addr` path against `blake3(putExpr d.typ)` on Lean. -/ +public def claimRevealDefnExpr (ixonEnv : Ixon.Env) : IO AiurTestCase := do + let (comm, info) ← findConstWithOrThrow ixonEnv "Defn" + fun ci => match ci with | .defn _ => true | _ => false + let .defn d := info + | throw <| IO.userError "findConstWith returned non-Defn" + let typAddr := Address.blake3 (Ixon.runPut (Ixon.putExpr d.typ)) + let revealInfo : Ix.RevealConstantInfo := + .defn none none none (some typAddr) none + let witness ← IO.ofExcept <| buildClaimWitness ixonEnv (Ix.Claim.reveal comm revealInfo) + pure (asTestCase "Claim Reveal Defn (typ Expr addr)" witness) + +/-- `Reveal` Muts — first component, one variant-appropriate + field set. -/ +public def claimRevealMuts (ixonEnv : Ixon.Env) : IO AiurTestCase := do + let (comm, info) ← findConstWithOrThrow ixonEnv "Muts" + fun ci => match ci with | .muts _ => true | _ => false + let .muts components := info + | throw <| IO.userError "findConstWith returned non-Muts" + let some firstMc := components[0]? + | throw <| IO.userError "Muts components empty" + let revealMc : Ix.RevealMutConstInfo := match firstMc with + | .defn d => .defn (some d.kind) (some d.safety) none none none + | .indc i => .indc (some i.recr) (some i.refl) (some i.isUnsafe) + none none none none none none + | .recr r => .recr (some r.k) (some r.isUnsafe) none none none none none + none none + let revealInfo : Ix.RevealConstantInfo := .muts #[(0, revealMc)] + let witness ← IO.ofExcept <| buildClaimWitness ixonEnv (Ix.Claim.reveal comm revealInfo) + pure (asTestCase "Claim Reveal Muts (first component)" witness) + +/-- All claim-variant smoke tests packaged for the `ixvm` runner. + Builds the shared Ixon env once and threads it through every + test. -/ +public def claimSmokeTests (env : Lean.Environment) : IO (List AiurTestCase) := do + let ixonEnv ← loadSharedIxonEnv #[``Nat.zero, ``Nat.add_comm] env + let t1 ← claimCheckWithAsm ixonEnv + let t2 ← claimContains + let t3 ← claimCheckEnv ixonEnv + let t4 ← claimRevealDefnFields ixonEnv + let t5 ← claimRevealCPrj ixonEnv + let t6 ← claimRevealDefnExpr ixonEnv + let t7 ← claimRevealMuts ixonEnv + pure [t1, t2, t3, t4, t5, t6, t7] diff --git a/Tests/Ix/Kernel/Arena.lean b/Tests/Ix/Kernel/Arena.lean index 86297e86..dc5922db 100644 --- a/Tests/Ix/Kernel/Arena.lean +++ b/Tests/Ix/Kernel/Arena.lean @@ -1,13 +1,19 @@ /- Drives the Aiur kernel through every lean-kernel-arena tutorial fixture (`Tests.Ix.Kernel.TutorialDefs` + `NatReduction`) using the - shared `IxVM.ixVM` toplevel + `kernel_check_test` entrypoint. + shared `IxVM.ixVM` toplevel + `dbg_check_const` entrypoint. Each fixture's outcome is classified against the test case's expected outcome (good must typecheck; bad must be rejected via Aiur execution error, where the error originates from an `assert_eq!` failure inside the Aiur kernel source). + `dbg_check_const` is a DEBUG entrypoint, not a claim — it + type-checks only the target and trusts transitive deps. Arena uses + it for the per-fixture speed advantage (shared deps would otherwise + be revalidated N times). Verifier policy must never accept this + funcidx as a production claim. + Skips: - test cases registered via `bad_raw_consts` (decls live in `TutorialMeta.rawConstsExt`, not `env.constants`, so Aiur ingress @@ -22,7 +28,7 @@ import Ix.Meta import Ix.Aiur.Protocol import Ix.Aiur.Compiler import Ix.IxVM -import Ix.IxVM.CheckHarness +import Ix.IxVM.ClaimHarness import Tests.Aiur.Common import Tests.Ix.Kernel.TutorialMeta import Tests.Ix.Kernel.TutorialDefs @@ -31,7 +37,7 @@ import LSpec open LSpec open Tests.Ix.Kernel.TutorialMeta -open IxVM.CheckHarness +open IxVM.ClaimHarness namespace Tests.Ix.Kernel.Arena @@ -75,7 +81,7 @@ private def collectChecks (env : Lean.Environment) : Array ArenaCheck := Id.run out := out.push { name := n, expectPass := pass } return out -/-- Build the `kernel_check_test` input for `name` against the shared +/-- Build the `dbg_check_const` input for `name` against the shared `ixonEnv`. Returns `error` when `compile_env` filtered the constant (no Ixon address) — caller treats that as a skip. -/ private def buildInput (ixonEnv : Ixon.Env) (name : Lean.Name) : @@ -83,21 +89,19 @@ private def buildInput (ixonEnv : Ixon.Env) (name : Lean.Name) : match ixonEnv.getAddr? (Ix.Name.fromLeanName name) with | none => .error "ungrounded by compile_env" | some addr => - let ioBuffer := buildKernelCheckIOBufferFor ixonEnv addr - let targetAddrBytes : Array Aiur.G := addr.hash.data.map .ofUInt8 - -- check_deps=0: only the target const is type-checked. Each fixture - -- runs in isolation; we don't need to revalidate every transitive - -- dep N times. - .ok (targetAddrBytes.push 0, ioBuffer) + -- Subject-only check via `dbg_check_const`. Each fixture runs in + -- isolation; we don't revalidate transitive deps N times. + let witness := buildDbgCheckConst ixonEnv addr + .ok (witness.input, witness.inputIOBuffer) /-- Run the arena suite against `compiled` (already-compiled Aiur `IxVM.ixVM` toplevel) using a single shared Ixon env. Returns one `TestSeq` entry per fixture. -/ def arenaTests (env : Lean.Environment) (compiled : Aiur.CompiledToplevel) : IO TestSeq := do - let funIdx ← match compiled.getFuncIdx `kernel_check_test with + let funIdx ← match compiled.getFuncIdx `dbg_check_const with | some i => pure i - | none => throw <| IO.userError "kernel_check_test entrypoint missing" + | none => throw <| IO.userError "dbg_check_const entrypoint missing" let checks := collectChecks env let ixonEnv ← loadSharedIxonEnv (checks.map (·.name)) env let mut tests : TestSeq := .done diff --git a/Tests/Main.lean b/Tests/Main.lean index 06f38ae1..441a3446 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -95,7 +95,9 @@ def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [ let kernelUnitTests := .exec `kernel_unit_tests let serdeNatAddCommTest ← serdeNatAddComm env let kernelChecks ← kernelChecks env - let aiurTests := [kernelUnitTests, serdeNatAddCommTest] ++ kernelChecks + let claimSmokes ← claimSmokeTests env + let aiurTests := [kernelUnitTests, serdeNatAddCommTest] + ++ kernelChecks ++ claimSmokes -- The arena suite shares the compiled toplevel with the AiurTestCase -- runs above; build it once here and weave the resulting TestSeq in -- alongside `mkAiurTests`'s output.