From 92462771af2bacd2cf652149b7f7e7f40acff5fb Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Mon, 23 Mar 2026 10:55:45 -0700 Subject: [PATCH] Fix level_leq incompleteness and redesign AiurTestCase API MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Level comparison: - Fix Succ ≤ Max incompleteness when an IMax child covers some assignments while a non-IMax child covers the rest. When both Max branches fail, case-split on a param from b to resolve IMax nodes. - Add unit test for the counterexample (u+1 = max(1, imax(u+1, u))). - Add full soundness and completeness argument for level_leq in KERNEL.md covering all 12 cases, with supporting lemmas for monotonicity, zero witness, and case-split soundness. AiurTestCase API: - Add defaults to all structure fields (label auto-derives from functionName, arrays default to #[], IO buffers default to default). - Rewrite noIO as a proper function, add exec shorthand for execution-only tests. - Replace raw anonymous constructors with named field syntax across Hashes.lean, IxVM.lean, Aiur.lean, and Main.lean. --- Ix/IxVM.lean | 90 +++++++++++++++++++++ Ix/IxVM/KERNEL.md | 174 +++++++++++++++++++++++++++++++++++++++-- Ix/IxVM/Kernel.lean | 164 +++++++++++++++++++++++++++++++++++++- Tests/Aiur/Aiur.lean | 6 +- Tests/Aiur/Common.lean | 43 ++++++---- Tests/Aiur/Hashes.lean | 6 +- Tests/Ix/IxVM.lean | 7 +- Tests/Main.lean | 4 +- 8 files changed, 460 insertions(+), 34 deletions(-) diff --git a/Ix/IxVM.lean b/Ix/IxVM.lean index 5ac597dc..0895a062 100644 --- a/Ix/IxVM.lean +++ b/Ix/IxVM.lean @@ -41,6 +41,96 @@ def entrypoints := ⟦ k_check_all_go(k_consts, k_consts, nat_idx, str_idx, 0) } + fn level_cmp_tests() { + -- Zero ≤ anything + assert_eq!(level_leq(KLevel.Zero, KLevel.Param(0)), 1); + + -- Param(u) ≤ Param(u) (reflexivity) + assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(0)), 1); + + -- Param(u) ≤ Param(v) fails (u ≠ v, set u > v) + assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(1)), 0); + + -- Succ(u) ≤ Succ(u) (peel both succs) + assert_eq!(level_leq( + KLevel.Succ(store(KLevel.Param(0))), + KLevel.Succ(store(KLevel.Param(0)))), 1); + + -- Succ(u) ≤ u fails (u+1 > u at any assignment) + assert_eq!(level_leq( + KLevel.Succ(store(KLevel.Param(0))), + KLevel.Param(0)), 0); + + -- === level_leq: Param ≤ Succ reduction === + + -- Param(u) ≤ Succ(Param(u)) (u ≤ u+1, reduces to u ≤ u) + assert_eq!(level_leq( + KLevel.Param(0), + KLevel.Succ(store(KLevel.Param(0)))), 1); + + -- === level_leq: Max distribution === + + -- max(u, v) ≤ max(u, v) (reflexivity via distribution) + let max_uv = KLevel.Max(store(KLevel.Param(0)), store(KLevel.Param(1))); + assert_eq!(level_leq(max_uv, max_uv), 1); + + -- u ≤ max(u, v) (try-each-branch: first branch succeeds) + assert_eq!(level_leq(KLevel.Param(0), max_uv), 1); + + -- max(u, v) ≤ u fails (set v > u) + assert_eq!(level_leq(max_uv, KLevel.Param(0)), 0); + + -- === level_leq: IMax case-splitting === + + -- imax(u, v) ≤ max(u, v) (case-split on v: v=0 gives 0 ≤ max(0,0)=0; v>0 gives max=max) + let imax_uv = KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(1))); + assert_eq!(level_leq(imax_uv, max_uv), 1); + + -- max(u, v) ≤ imax(u, v) fails (set v=0: max(u,0) = u but imax(u,0) = 0; take u=1) + assert_eq!(level_leq(max_uv, imax_uv), 0); + + -- === level_leq: Succ ≤ Max with IMax child (the case-split fix) === + + -- u+1 = max(1, imax(u+1, u)): equal for all σ + -- σ(u)=0: 1 = max(1, imax(1,0)) = max(1,0) = 1 + -- σ(u)=n>0: n+1 = max(1, max(n+1,n)) = n+1 + -- This is the case that requires case-splitting through Max when + -- neither branch (Succ(Zero) or IMax) alone dominates Succ(Param(u)). + let a = KLevel.Succ(store(KLevel.Param(0))); + let b = KLevel.Max( + store(KLevel.Succ(store(KLevel.Zero))), + store(KLevel.IMax( + store(KLevel.Succ(store(KLevel.Param(0)))), + store(KLevel.Param(0))))); + assert_eq!(level_equal(a, b), 1); + + -- === level_equal: semantic equality === + + -- imax(u, u) = u (when u=0: imax(0,0)=0=u; when u>0: max(u,u)=u) + assert_eq!(level_equal( + KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(0))), + KLevel.Param(0)), 1); + + -- max(u, 0) = u + assert_eq!(level_equal( + KLevel.Max(store(KLevel.Param(0)), store(KLevel.Zero)), + KLevel.Param(0)), 1); + + -- level_imax reduces imax(u, 1+v) to max(u, 1+v) and imax(u, 0) to 0 + let succ_v = KLevel.Succ(store(KLevel.Param(1))); + assert_eq!(level_eq( + level_imax(KLevel.Param(0), succ_v), + KLevel.Max(store(KLevel.Param(0)), store(succ_v))), 1); + + assert_eq!(level_eq( + level_imax(KLevel.Param(0), KLevel.Zero), + KLevel.Zero), 1); + } + + fn kernel_unit_tests() { + level_cmp_tests() + } + /- # Benchmark entrypoints -/ fn ixon_serde_blake3_bench(n: G) { diff --git a/Ix/IxVM/KERNEL.md b/Ix/IxVM/KERNEL.md index eb820682..8e5a7b16 100644 --- a/Ix/IxVM/KERNEL.md +++ b/Ix/IxVM/KERNEL.md @@ -152,11 +152,175 @@ If `B` is NOT in `Prop`, then `imax uA uB = max uA uB`, the standard predicative Two levels are equal if they evaluate to the same natural number under every assignment of parameters. The Aiur kernel uses `level_equal(a, b) = level_leq(a, b) ∧ level_leq(b, a)`, -where `level_leq` is sound and complete. For `IMax` forms whose second argument might be -zero, `level_leq` case-splits on a parameter `p` from that argument: it substitutes `p → 0` -(eliminating the `IMax`) and `p → Succ(p)` (resolving `IMax` to `Max`), checking the -inequality in both cases. It also distributes `Succ` over `Max` and handles -`Param(i) ≤ Succ(X)` by recursing to `Param(i) ≤ X` (valid since levels are integer-valued). +where `level_leq` is sound and complete. + +#### Semantics + +A *level assignment* σ maps parameter indices to natural numbers. Every level `l` +evaluates to a natural number ⟦l⟧σ: + +- ⟦Zero⟧σ = 0 +- ⟦Param(i)⟧σ = σ(i) +- ⟦Succ(l)⟧σ = 1 + ⟦l⟧σ +- ⟦Max(a, b)⟧σ = max(⟦a⟧σ, ⟦b⟧σ) +- ⟦IMax(a, b)⟧σ = if ⟦b⟧σ = 0 then 0 else max(⟦a⟧σ, ⟦b⟧σ) + +We write `a ≤ b` to mean ⟦a⟧σ ≤ ⟦b⟧σ for all σ, and `a = b` to mean `a ≤ b ∧ b ≤ a`. +Let σ₀ denote the assignment mapping every parameter to 0. + +#### Reduced levels + +The functions `level_max` and `level_imax` produce levels in *reduced form*. +The key invariant: + +> **(R)** If `IMax(a, b)` appears in a reduced level, then `level_is_not_zero(b) = 0`. + +This holds because `level_imax(a, b)` returns `Zero` when `b = Zero`, returns +`level_max(a, b)` when `b = Succ(_)` or `level_is_not_zero(b) = 1`, and only +produces an `IMax` node otherwise. + +All levels entering `level_leq` are reduced: the initial levels come from +`level_inst_params` / `level_reduce` (which build via `level_max`/`level_imax`), +and the case-split substitutions use `level_subst_reduce` (which also builds via +`level_max`/`level_imax`). + +#### Monotonicity + +**Lemma (Monotonicity).** All level expressions are monotone in their parameters: +if σ₁(i) ≤ σ₂(i) for all i, then ⟦l⟧σ₁ ≤ ⟦l⟧σ₂. + +*Proof.* By induction on `l`. The Zero, Param, Succ, and Max cases are immediate. +For IMax(a, b): if ⟦b⟧σ₁ = 0, then ⟦IMax(a,b)⟧σ₁ = 0 ≤ ⟦IMax(a,b)⟧σ₂. +If ⟦b⟧σ₁ > 0, then by IH ⟦b⟧σ₂ ≥ ⟦b⟧σ₁ > 0, so +⟦IMax(a,b)⟧σ₁ = max(⟦a⟧σ₁, ⟦b⟧σ₁) ≤ max(⟦a⟧σ₂, ⟦b⟧σ₂) = ⟦IMax(a,b)⟧σ₂. ∎ + +#### Zero witness + +**Lemma (Zero Witness).** `level_is_not_zero(l) = 0` if and only if ⟦l⟧₀ = 0 +(where σ₀(i) = 0 for all i). Equivalently, `level_is_not_zero(l) = 1` if and only +if ⟦l⟧σ ≥ 1 for all σ. + +*Proof.* (⇒) By induction: Zero and Param evaluate to 0 under σ₀. Succ returns 1, +so this case is excluded. Max(a,b) with both children returning 0 gives +max(⟦a⟧₀, ⟦b⟧₀) = max(0, 0) = 0. IMax(a,b) with `level_is_not_zero(b) = 0` +gives ⟦b⟧₀ = 0 by IH, so ⟦IMax(a,b)⟧₀ = 0. + +(⇐) If `level_is_not_zero(l) = 1`, by induction: Succ(x) ≥ 1 always. +Max(a,b) with at least one child having `level_is_not_zero = 1`: that child is ≥ 1 +for all σ (IH), so max ≥ 1. IMax(a,b) with `level_is_not_zero(b) = 1`: +⟦b⟧σ ≥ 1 for all σ (IH), so IMax = max(a,b) ≥ b ≥ 1. ∎ + +**Corollary.** For a reduced `IMax(a, b)` (invariant R), ⟦IMax(a, b)⟧₀ = 0. + +#### Case-split soundness + +The case-split technique substitutes a parameter `p` with `Zero` and `Succ(Param(p))`. +This is sound and complete for universal quantification over σ(p): + +- Every σ has σ(p) = 0 or σ(p) ≥ 1. +- When σ(p) = 0: captured by the `p → Zero` substitution. +- When σ(p) ≥ 1: write σ(p) = 1 + σ'(p). Then ⟦l[p ↦ Succ(Param(p))]⟧σ' = ⟦l⟧σ, + so the `p → Succ(Param(p))` substitution captures all σ(p) ≥ 1. + +Hence `∀σ. ⟦a⟧σ ≤ ⟦b⟧σ` iff both `∀σ. ⟦a[p↦0]⟧σ ≤ ⟦b[p↦0]⟧σ` and +`∀σ. ⟦a[p↦S(p)]⟧σ ≤ ⟦b[p↦S(p)]⟧σ`. + +#### Soundness and completeness of `level_leq` + +**Theorem.** For reduced levels `a` and `b`, `level_leq(a, b) = 1` if and only if +`a ≤ b` (i.e., ⟦a⟧σ ≤ ⟦b⟧σ for all σ). + +*Proof.* By case analysis on `level_leq`. In each case we show the return value is 1 +iff the inequality holds universally. + +**Case `a = Zero`:** Returns 1. Correct: 0 ≤ ⟦b⟧σ for all σ. + +**Case `a = Max(a1, a2)`:** Returns `level_leq(a1, b) * level_leq(a2, b)`. +max(⟦a1⟧σ, ⟦a2⟧σ) ≤ ⟦b⟧σ iff ⟦a1⟧σ ≤ ⟦b⟧σ and ⟦a2⟧σ ≤ ⟦b⟧σ. ∎ + +**Case `a = Succ(Max(x, y))`:** Distributes to `level_leq(Succ(x), b) * level_leq(Succ(y), b)`. +Correct: 1 + max(⟦x⟧σ, ⟦y⟧σ) = max(1 + ⟦x⟧σ, 1 + ⟦y⟧σ), reducing to the Max case. ∎ + +**Case `a = Succ(a1)`, `a1` not Max, `b = Succ(b1)`:** Returns `level_leq(a1, b1)`. +1 + ⟦a1⟧σ ≤ 1 + ⟦b1⟧σ iff ⟦a1⟧σ ≤ ⟦b1⟧σ. ∎ + +**Case `a = Succ(a1)`, `a1` not Max, `b = Zero` or `Param(j)` or `IMax(_, _)`:** +Returns 0. Correct by Zero Witness: ⟦b⟧₀ = 0 (b = Zero is immediate; Param(j) gives +σ₀(j) = 0; IMax is 0 under σ₀ by the Corollary), but ⟦Succ(a1)⟧₀ ≥ 1. ∎ + +**Case `a = Succ(a1)`, `a1` not Max, `b = Max(b1, b2)`:** First tries +`level_leq(a, b1)` and `level_leq(a, b2)`. If either returns 1, the result is sound +(a ≤ bi implies a ≤ max(b1, b2)). If both return 0 and `b` has no params, returns 0 +(b is a concrete number; the try-each-branch is complete for concrete values). If both +return 0 and `b` has params, case-splits on a param `p` from `b`. This is sound and +complete by Case-Split Soundness above — after substitution, `level_subst_reduce` +re-reduces the result, resolving any IMax whose conditioning variable was `p`. +The recursion terminates because each case-split strictly reduces the number of free +parameters. After all IMax nodes are resolved (finitely many case-splits), the levels +are tropical polynomials (max-plus over Succ chains and Params), for which the +try-each-branch heuristic IS complete: + +> *Tropical completeness:* For tropical polynomials (no IMax), `Succ(a1) ≤ Max(b1, b2)` +> for all σ implies `Succ(a1) ≤ b1` for all σ or `Succ(a1) ≤ b2` for all σ. +> +> *Proof sketch:* Since ⟦Succ(a1)⟧₀ ≥ 1, we have max(⟦b1⟧₀, ⟦b2⟧₀) ≥ 1, so +> WLOG ⟦b1⟧₀ ≥ 1, hence `level_is_not_zero(b1) = 1` (Zero Witness). Since b1 is a +> tropical polynomial with `level_is_not_zero = 1`, it is Succ or Max (not IMax, not +> Param, not Zero). Being a tropical polynomial, b1 is of the form max(σ(pᵢ) + cᵢ) +> with all cᵢ ≥ 0. For any Param(q) appearing in a with Succ-offset k: ⟦a⟧σ grows as +> σ(q) + k, and for a ≤ Max(b1, b2) to hold universally as σ(q) → ∞, some branch must +> contain a term σ(q) + c with c ≥ k. Since b1 is tropical and always ≥ 1 (no IMax +> zeroing), all its terms are unconditional — any term σ(q) + c in b1 contributes +> b1 ≥ σ(q) + c for ALL σ. So if b1 contains the dominating terms for a, then a ≤ b1. ∎ + +**Case `a = Param(i)`, `b = Param(j)`:** Returns `eq_zero(i - j)`, i.e., 1 iff i = j. +Correct: σ(i) ≤ σ(j) for all σ iff i = j (otherwise set σ(i) > σ(j)). ∎ + +**Case `a = Param(i)`, `b = Succ(b1)`:** Returns `level_leq(Param(i), b1)`, +i.e., reduces `σ(i) ≤ 1 + ⟦b1⟧σ` to `σ(i) ≤ ⟦b1⟧σ`. + +*Soundness:* If σ(i) ≤ ⟦b1⟧σ then σ(i) ≤ 1 + ⟦b1⟧σ. ∎ + +*Completeness:* Suppose σ(i) ≤ 1 + ⟦b1⟧σ for all σ. Fix all parameters except i and +define f(n) = ⟦b1⟧(σ[i ↦ n]). By monotonicity, f is non-decreasing. The premise gives +n ≤ 1 + f(n) for all n ≥ 0. We need n ≤ f(n) for all n. + +For n > 0: every IMax in b1 whose second argument depends on Param(i) is resolved +(since n > 0 makes any monotone expression involving Param(i) positive, and +`level_subst_reduce` normalizes away such IMax nodes). So for n > 0, f(n) includes +an unconditional term n + c for some c ≥ 0 (from each Param(i) path in b1). +If such a term exists, f(n) ≥ n + c ≥ n. If no such term exists, f is eventually +constant, and n ≤ 1 + C fails for large n — contradicting the premise. + +For n = 0: f(0) ≥ 0 trivially. ∎ + +**Case `a = Param(i)`, `b = Max(b1, b2)`:** Tries each branch. Sound (a ≤ bi +implies a ≤ max(b1, b2)). Complete: at σ₀, σ₀(i) = 0 ≤ max(⟦b1⟧₀, ⟦b2⟧₀), +which holds trivially — so the argument is subtler. Since σ(i) is unbounded, at least +one bk must contain Param(i) + c (c ≥ 0) unconditionally (not zeroed by IMax). That +branch satisfies bk ≥ σ(i), so Param(i) ≤ bk. If the only Param(i) terms are inside +IMax nodes, then at σ₀ (where IMax zeroes them), b = max(const₁, const₂), and +σ(i) ≤ max(const₁, const₂) fails for large σ(i) — contradicting the premise. ∎ + +**Case `a = Param(i)`, `b = IMax(b1, b2)`:** Case-splits on a param from b2. +Sound and complete by Case-Split Soundness. ∎ + +**Case `a = Param(i)`, `b = Zero`:** Returns 0. Correct: σ(i) ≤ 0 fails for σ(i) = 1. ∎ + +**Case `a = IMax(a1, a2)`, `level_is_not_zero(a2) = 1`:** Treats as Max(a1, a2): +returns `level_leq(a1, b) * level_leq(a2, b)`. Correct: a2 ≥ 1 for all σ (Zero Witness), +so IMax(a1, a2) = max(a1, a2). ∎ + +**Case `a = IMax(a1, a2)`, `level_is_not_zero(a2) = 0`:** Case-splits on a param +from a2. Sound and complete by Case-Split Soundness. Note: `level_is_not_zero(a2) = 0` +and `a` is reduced, so a2 has at least one param (otherwise a2 is Zero and +`level_imax` would have reduced the IMax away). ∎ + +#### Termination + +Each case either reduces the structural size of the levels (Succ peeling, Max +distribution) or reduces the number of free parameters (case-split substitution). +Since both measures are bounded, the recursion terminates. ### Level Instantiation diff --git a/Ix/IxVM/Kernel.lean b/Ix/IxVM/Kernel.lean index 73411bb3..71e033e7 100644 --- a/Ix/IxVM/Kernel.lean +++ b/Ix/IxVM/Kernel.lean @@ -1,6 +1,67 @@ module public import Ix.Aiur.Meta +/-! +# Aiur Kernel — Lean 4 Type Checker Circuit + +A complete Lean 4 kernel type checker written in Aiur, a DSL for zero-knowledge +proof circuits. Verifies that every definition and theorem in a Lean environment +is well-typed. + +## Architecture + +The kernel uses **Normalization by Evaluation (NbE)**: expressions (`KExpr`) are +evaluated into semantic values (`KVal`) using closures and environments, giving +O(1) beta reduction instead of O(|body|) substitution walks. Free variables use +**de Bruijn levels** (stable under binder entry) rather than indices. + +The core is three mutually recursive operations: +- `k_eval` / `k_whnf`: evaluate expressions and reduce to weak head normal form +- `k_infer` / `k_check`: infer types and bidirectionally check against expected types +- `k_is_def_eq`: check definitional equality (proof irrelevance, eta, lazy delta) + +## Aiur Constraints + +Aiur circuits have no mutation, no dynamic indexing, and no non-tail matches. +Instead of explicit caches (WHNF cache, equiv manager, thunk memoization), the +Aiur runtime's function-call caching provides call-by-need semantics: calling +`k_eval(expr, env, top)` with the same arguments returns the cached result. + +## Implemented Features + +| Feature | Status | +|----------------------------------|--------| +| Lazy eval (thunks in spines) | ✅ | +| Eager beta optimization | ✅ | +| Delta unfolding (WHNF) | ✅ | +| Iota reduction (recursor) | ✅ | +| K-reduction (Prop recursors) | ✅ | +| Nat literal iota | ✅ | +| Quotient reduction | ✅ | +| Function eta | ✅ | +| Struct eta | ✅ | +| Bidirectional checking | ✅ | +| Level comparison (sound+complete)| ✅ | + +## Known Limitations + +| Feature | Status | +|----------------------------------|--------------------------------------| +| Nat primitives (add, mul, ...) | ❌ uses iota (exponential for large) | +| String primitives | ❌ | +| Unit-like types | ❌ | +| Lazy delta (hint-based) | ⚠️ unfolds both sides | +| Proof irrelevance | ⚠️ partial (FVar returns Sort 1) | +| Inductive block validation | ❌ trusts input | +| Delta step limit | ❌ | + +## File Organization + +Types are in `KernelTypes.lean` (`KExpr`, `KVal`, `KLevel`, `KConstantInfo`). +Ixon ↔ kernel conversion is in `Convert.lean`. Content-addressed constant +loading is in `Ingress.lean`. This file contains all kernel logic. +-/ + public section namespace IxVM @@ -147,6 +208,15 @@ def kernel := ⟦ -- ============================================================================ -- Level operations + -- + -- Universe levels are symbolic expressions (Zero, Succ, Max, IMax, Param) + -- evaluated under assignments σ : Param → ℕ. Two levels are equal iff they + -- agree under all assignments. IMax(a, b) = 0 when b = 0, else max(a, b); + -- this gives impredicativity of Prop. + -- + -- Levels are maintained in "reduced form" by level_max and level_imax: + -- an IMax(a, b) node only survives when b could be zero (level_is_not_zero = 0). + -- This invariant is key to the completeness of level_leq. -- ============================================================================ -- Check if a level is definitely not zero (sound approximation) @@ -255,7 +325,26 @@ def kernel := ⟦ } } - -- level_leq: check a <= b for all param assignments (sound and complete) + -- Check ⟦a⟧σ ≤ ⟦b⟧σ for all level assignments σ : Param → ℕ. + -- Returns 1 iff the inequality holds universally; 0 otherwise. + -- + -- Sound and complete for reduced levels. Proof sketch by case: + -- Zero ≤ b: trivially true (0 ≤ anything) + -- Max(a1,a2) ≤ b: iff a1 ≤ b ∧ a2 ≤ b + -- Succ(Max(x,y)) ≤ b: distribute: succ(max) = max(succ,succ) + -- Succ(a1) ≤ Succ(b1): peel both succs + -- Succ(a1) ≤ Zero/Param/IMax: false (Zero Witness: reduced IMax evaluates to 0 at σ₀) + -- Succ(a1) ≤ Max(b1,b2): try each branch; if both fail and b has params, case-split + -- to resolve IMax children (tropical completeness after resolution) + -- Param(i) ≤ Param(j): iff i = j + -- Param(i) ≤ Succ(b1): reduces to Param(i) ≤ b1 (complete by monotonicity argument) + -- Param(i) ≤ Max(b1,b2): try each branch (complete: Param tracks through some branch) + -- Param(i) ≤ IMax(b1,b2): case-split on a param in b2 + -- IMax(a1,a2) ≤ b: if a2 definitely nonzero, treat as Max; else case-split on a2 + -- + -- Case-splitting substitutes p → 0 and p → Succ(Param(p)), partitioning all assignments. + -- Each split strictly reduces free params, ensuring termination. + -- See KERNEL.md §3 "Level Comparison" for the full formal argument. fn level_leq(a: KLevel, b: KLevel) -> G { match a { KLevel.Zero => 1, @@ -274,7 +363,27 @@ def kernel := ⟦ let r1 = level_leq(a, b1); match r1 { 1 => 1, - 0 => level_leq(a, b2), + 0 => + let r2 = level_leq(a, b2); + match r2 { + 1 => 1, + -- Neither branch alone dominates; case-split on a param in b + -- to resolve any IMax children (see INCOMPLETE.md) + 0 => + let bfull = KLevel.Max(store(b1), store(b2)); + let hp = level_has_param(bfull); + match hp { + 0 => 0, + _ => + let p = level_any_param(bfull); + let sp = KLevel.Succ(store(KLevel.Param(p))); + let a0 = level_subst_reduce(a, p, KLevel.Zero); + let b0 = level_subst_reduce(bfull, p, KLevel.Zero); + let a1s = level_subst_reduce(a, p, sp); + let b1s = level_subst_reduce(bfull, p, sp); + level_leq(a0, b0) * level_leq(a1s, b1s), + }, + }, }, _ => 0, }, @@ -440,6 +549,12 @@ def kernel := ⟦ -- ============================================================================ -- Evaluation (NbE) + -- + -- Normalization by Evaluation: expressions (KExpr) are evaluated into semantic + -- values (KVal) using closures. A lambda captures its environment; applying it + -- pushes the argument, giving O(1) beta reduction. Constants evaluate to + -- neutrals (no eager delta unfolding) — definition unfolding is deferred to WHNF. + -- Free variables use de Bruijn levels (stable under binder entry). -- ============================================================================ -- Force a thunk: if it's a Thunk, evaluate it; otherwise return as-is @@ -553,6 +668,11 @@ def kernel := ⟦ -- ============================================================================ -- Iota reduction (recursor on constructor) + -- + -- When a recursor meets the constructor it can pattern-match on, reduce: + -- Nat.rec motive hz hs (Nat.succ n) → hs n (Nat.rec motive hz hs n) + -- Also handles Nat literal iota: Lit(0) matches the zero constructor, + -- Lit(n+1) matches succ with Lit(n) as predecessor. -- ============================================================================ -- Get induct_idx from a constructor's constant info @@ -737,7 +857,12 @@ def kernel := ⟦ } -- ============================================================================ - -- WHNF (additional reductions beyond eval) + -- WHNF (Weak Head Normal Form) + -- + -- Reduce a value until its outermost constructor is visible. The WHNF loop + -- applies projection reduction, iota (recursor on ctor), delta (definition + -- unfolding), and quotient reduction, retrying after each successful step. + -- Does not reduce under binders or inside arguments. -- ============================================================================ -- Reduce a value to Weak Head Normal Form by retrying projection, iota, and delta reductions @@ -810,6 +935,10 @@ def kernel := ⟦ -- ============================================================================ -- Quotation (values back to expressions) + -- + -- Readback from the semantic domain: converts KVal back to KExpr. + -- Needed when instantiating universe parameters or building the Pi type + -- for a lambda's inferred type. Converts de Bruijn levels back to indices. -- ============================================================================ -- Quote a value back into an expression (readback), converting free variables @@ -873,6 +1002,11 @@ def kernel := ⟦ -- ============================================================================ -- Type inference + -- + -- Infer the type of an expression (k_infer) or check it against an expected + -- type (k_check). Bidirectional: when checking a lambda against a Pi type, + -- the expected codomain is pushed through the body, avoiding an expensive + -- infer + isDefEq. -- ============================================================================ -- Infer the type of an expression under the given type and value environments. @@ -1062,6 +1196,11 @@ def kernel := ⟦ -- ============================================================================ -- Proof irrelevance helpers + -- + -- If a : P and b : P where P : Prop (Sort 0), then a ≡ b. + -- k_infer_val_type is best-effort: returns Sort 1 sentinel for FVar/Lam/Proj, + -- so proof irrelevance won't trigger for free-variable-headed proofs. + -- Conservative (never unsound) but incomplete. -- ============================================================================ -- Apply a spine of argument values to a type by walking through Pi-bindings @@ -1155,6 +1294,10 @@ def kernel := ⟦ -- ============================================================================ -- Struct eta helpers + -- + -- Structure eta: s ≡ ⟨s.1, s.2, ...⟩ for single-constructor types. + -- If one side is a Ctor of a struct-like inductive (1 constructor, no indices), + -- compare each field against Proj(i, other_side). -- ============================================================================ -- Get num_fields from a constructor's constant info @@ -1218,6 +1361,14 @@ def kernel := ⟦ -- ============================================================================ -- Definitional equality + -- + -- The most complex part of the kernel. Uses a layered approach: + -- 1. Quick syntactic check (sorts, literals) + -- 2. Reduce both sides to WHNF + -- 3. Proof irrelevance (both proofs of Props ⟹ compare types) + -- 4. Structural comparison (k_is_def_eq_core) + -- 5. Struct eta (s ≡ ⟨s.1, s.2, ...⟩) + -- 6. Lazy delta unfolding (try unfolding constants to make progress) -- ============================================================================ -- Check definitional equality of two values: first try a quick syntactic check, @@ -1574,6 +1725,10 @@ def kernel := ⟦ -- ============================================================================ -- Declaration checking + -- + -- Verify each constant in the environment: its type must be a Sort, and its + -- value (if any) must have the declared type. Processes axioms, definitions, + -- theorems, opaques, quotients, inductives, constructors, and recursors. -- ============================================================================ -- Type-check a single constant declaration against the environment. @@ -1636,6 +1791,9 @@ def kernel := ⟦ -- ============================================================================ -- Primitive type discovery + -- + -- Scan the constant list to find the index of the Nat inductive type. + -- Used for Nat literal iota reduction and Nat literal ↔ constructor equality. -- ============================================================================ -- Count the number of entries in a KGList diff --git a/Tests/Aiur/Aiur.lean b/Tests/Aiur/Aiur.lean index c8d3208f..13ee9061 100644 --- a/Tests/Aiur/Aiur.lean +++ b/Tests/Aiur/Aiur.lean @@ -495,9 +495,9 @@ def aiurTestCases : List AiurTestCase := [ .noIO `assert_eq_trivial #[] #[], -- IO - ⟨`read_write_io, "read_write_io", #[], #[], - ⟨#[1, 2, 3, 4], .ofList [(#[0], ⟨0, 4⟩)]⟩, - ⟨#[1, 2, 3, 4, 1, 2, 3, 4], .ofList [(#[0], ⟨0, 4⟩), (#[1], ⟨0, 8⟩)]⟩⟩, + { functionName := `read_write_io + inputIOBuffer := ⟨#[1, 2, 3, 4], .ofList [(#[0], ⟨0, 4⟩)]⟩ + expectedIOBuffer := ⟨#[1, 2, 3, 4, 1, 2, 3, 4], .ofList [(#[0], ⟨0, 4⟩), (#[1], ⟨0, 8⟩)]⟩ }, -- Byte operations .noIO `shr_shr_shl_decompose #[87] #[0, 1, 0, 1, 0, 1, 0, 0], diff --git a/Tests/Aiur/Common.lean b/Tests/Aiur/Common.lean index 31cef12d..942f490f 100644 --- a/Tests/Aiur/Common.lean +++ b/Tests/Aiur/Common.lean @@ -14,14 +14,20 @@ open LSpec SlimCheck Gen structure AiurTestCase where functionName : Lean.Name - label : String - input : Array Aiur.G - expectedOutput : Array Aiur.G - inputIOBuffer: Aiur.IOBuffer - expectedIOBuffer: Aiur.IOBuffer + label : String := toString functionName + input : Array Aiur.G := #[] + expectedOutput : Array Aiur.G := #[] + inputIOBuffer : Aiur.IOBuffer := default + expectedIOBuffer : Aiur.IOBuffer := default + executionOnly : Bool := false -def AiurTestCase.noIO (name : Lean.Name) := - (AiurTestCase.mk name (toString name) · · default default) +def AiurTestCase.noIO (functionName : Lean.Name) + (input expectedOutput : Array Aiur.G) : AiurTestCase := + { functionName, input, expectedOutput } + +def AiurTestCase.exec (functionName : Lean.Name) + (input : Array Aiur.G := #[]) (expectedOutput : Array Aiur.G := #[]) : AiurTestCase := + { functionName, input, expectedOutput, executionOnly := true } def commitmentParameters : Aiur.CommitmentParameters := { logBlowup := 1 @@ -58,16 +64,19 @@ def AiurTestEnv.runTestCase (env : AiurTestEnv) (testCase : AiurTestCase) : Test (execOutput == testCase.expectedOutput) let execIOTest := test s!"Execute IOBuffer matches for {label}" (execIOBuffer == testCase.expectedIOBuffer) - let (claim, proof, ioBuffer) := env.aiurSystem.prove - friParameters funIdx testCase.input testCase.inputIOBuffer - let claimTest := test s!"Claim matches for {label}" - (claim == Aiur.buildClaim funIdx testCase.input testCase.expectedOutput) - let ioTest := test s!"IOBuffer matches for {label}" - (ioBuffer == testCase.expectedIOBuffer) - let proof := .ofBytes proof.toBytes - let pvTest := withExceptOk s!"Prove/verify works for {label}" - (env.aiurSystem.verify friParameters claim proof) fun _ => .done - execOutputTest ++ execIOTest ++ claimTest ++ ioTest ++ pvTest + let execTest := execOutputTest ++ execIOTest + if testCase.executionOnly then execTest + else + let (claim, proof, ioBuffer) := env.aiurSystem.prove + friParameters funIdx testCase.input testCase.inputIOBuffer + let claimTest := test s!"Claim matches for {label}" + (claim == Aiur.buildClaim funIdx testCase.input testCase.expectedOutput) + let ioTest := test s!"IOBuffer matches for {label}" + (ioBuffer == testCase.expectedIOBuffer) + let proof := .ofBytes proof.toBytes + let pvTest := withExceptOk s!"Prove/verify works for {label}" + (env.aiurSystem.verify friParameters claim proof) fun _ => .done + execTest ++ claimTest ++ ioTest ++ pvTest def mkAiurTests (toplevelFn : Except Aiur.Global Aiur.Toplevel) (cases : List AiurTestCase) : TestSeq := diff --git a/Tests/Aiur/Hashes.lean b/Tests/Aiur/Hashes.lean index 0fe8ea4e..74a901ae 100644 --- a/Tests/Aiur/Hashes.lean +++ b/Tests/Aiur/Hashes.lean @@ -13,7 +13,8 @@ def mkBlake3HashTestCase (size : Nat) : AiurTestCase := let input := inputBytes.map .ofUInt8 let output := outputBytes.map .ofUInt8 let buffer := ⟨input, .ofList [(#[0], ⟨0, size⟩)]⟩ -- key is fixed as #[0] - ⟨`blake3_test, s!"blake3 (size={size})", #[], output, buffer, buffer⟩ + { functionName := `blake3_test, label := s!"blake3 (size={size})" + expectedOutput := output, inputIOBuffer := buffer, expectedIOBuffer := buffer } def mkSha256HashTestCase (size : Nat) : AiurTestCase := let inputBytes := Array.range size |>.map Nat.toUInt8 @@ -21,7 +22,8 @@ def mkSha256HashTestCase (size : Nat) : AiurTestCase := let input := inputBytes.map .ofUInt8 let output := outputBytes.map .ofUInt8 let buffer := ⟨input, .ofList [(#[0], ⟨0, size⟩)]⟩ -- key is fixed as #[0] - ⟨`sha256_test, s!"sha256 (size={size})", #[], output, buffer, buffer⟩ + { functionName := `sha256_test, label := s!"sha256 (size={size})" + expectedOutput := output, inputIOBuffer := buffer, expectedIOBuffer := buffer } public def blake3TestCases : List AiurTestCase := [ mkBlake3HashTestCase 0, diff --git a/Tests/Ix/IxVM.lean b/Tests/Ix/IxVM.lean index 95383c7a..1a9a3781 100644 --- a/Tests/Ix/IxVM.lean +++ b/Tests/Ix/IxVM.lean @@ -12,7 +12,8 @@ public def serdeNatAddComm (env : Lean.Environment) : IO AiurTestCase := do let (ioBuffer, n) := ixonConsts.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) - pure ⟨`ixon_serde_test, "Ixon serde test", #[.ofNat n], #[], ioBuffer, ioBuffer⟩ + pure { functionName := `ixon_serde_test, label := "Ixon serde test" + input := #[.ofNat n], inputIOBuffer := ioBuffer, expectedIOBuffer := ioBuffer } def kernelCheck (name : Lean.Name) (env : Lean.Environment) : IO AiurTestCase := do let constList := Lean.collectDependencies name env.constants @@ -42,8 +43,8 @@ def kernelCheck (name : Lean.Name) (env : Lean.Environment) : IO AiurTestCase := | none => panic! s!"{name} not found in Ixon environment" let targetAddrBytes : Array Aiur.G := targetAddr.hash.data.map .ofUInt8 - pure ⟨`kernel_check_test, s!"Kernel check {name}", - targetAddrBytes, #[], ioBuffer, ioBuffer⟩ + pure { functionName := `kernel_check_test, label := s!"Kernel check {name}" + input := targetAddrBytes, inputIOBuffer := ioBuffer, expectedIOBuffer := ioBuffer } public def kernelCheckNatAddComm (env : Lean.Environment) : IO AiurTestCase := do kernelCheck ``Nat.add_comm env diff --git a/Tests/Main.lean b/Tests/Main.lean index db7de763..2bb0a24d 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -69,10 +69,12 @@ def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [ let r2 ← LSpec.lspecEachIO sha256TestCases fun tc => pure (sha256Env.runTestCase tc) return if r1 == 0 && r2 == 0 then 0 else 1), ("ixvm", do + let kernelUnitTests := .exec `kernel_unit_tests let serdeNatAddCommTest ← serdeNatAddComm env let kernelCheckNatAddCommTest ← kernelCheckNatAddComm env let kernelCheckNatSubLeOfLeAddTest ← kernelCheckNatSubLeOfLeAdd env - let tests := [serdeNatAddCommTest, kernelCheckNatAddCommTest, kernelCheckNatSubLeOfLeAddTest] + let tests := [kernelUnitTests, serdeNatAddCommTest, + kernelCheckNatAddCommTest, kernelCheckNatSubLeOfLeAddTest] LSpec.lspecIO (.ofList [("ixvm", [mkAiurTests IxVM.ixVM tests])]) []), ("rbtree-map", do IO.println "rbtree-map"