From 61011b935381a203a8cdcb92821950b2f54909b8 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Thu, 26 Mar 2026 19:24:04 -0700 Subject: [PATCH] Add Aiur formal verification framework with #aiur_gen command MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add G field arithmetic (Add, Sub, Mul, eqZero), u8/u32 semantic functions with range predicates, and commutativity theorems to Goldilocks.lean. Enable precompileModules on Ix library for native evaluation under Lean's `module` system. Add `#aiur_gen` command that evaluates an Aiur Toplevel at elaboration time and writes a .lean file with: - Semantic types: Lean inductives from Aiur enums with pointers erased, type aliases as abbrevs, topologically sorted by type references with mutual blocks for cyclic dependencies - Semantic propositions: one inductive per function, one constructor per control-flow path, with assertEq as Prop conjuncts, store/load erased, u8/u32 ops with range constraints, or-patterns expanded, IO operations as unconstrained fresh variables, data constructors inlined, nested match patterns resolved transitively - Topological sorting of both types and functions by dependency graph, with mutual blocks only for actual cycles Add multi-file example: - ExampleBase.lean: Expr type, eval, swap, double_eval (forward ref), simplify_neg (nested match) → ExampleBaseSem.lean - ExampleMain.lean: ExprList, Tree/Forest (mutual types), list_sum, assert_eval, tree_sum/forest_sum (mutual functions), is_even/is_odd (mutual recursion) → ExampleMainSem.lean (imports base) - Example.lean: 10 theorems over generated semantic propositions (determinism, totality, involution, assertEq semantics, spec soundness, mutual type/function soundness, mutual recursion path exclusivity) --- Ix/Aiur/Formal/Example.lean | 161 +++++++ Ix/Aiur/Formal/ExampleBase.lean | 52 +++ Ix/Aiur/Formal/ExampleBaseSem.lean | 55 +++ Ix/Aiur/Formal/ExampleMain.lean | 75 ++++ Ix/Aiur/Formal/ExampleMainSem.lean | 84 ++++ Ix/Aiur/Formal/GenSem.lean | 675 +++++++++++++++++++++++++++++ Ix/Aiur/Goldilocks.lean | 58 +++ lakefile.lean | 1 + 8 files changed, 1161 insertions(+) create mode 100644 Ix/Aiur/Formal/Example.lean create mode 100644 Ix/Aiur/Formal/ExampleBase.lean create mode 100644 Ix/Aiur/Formal/ExampleBaseSem.lean create mode 100644 Ix/Aiur/Formal/ExampleMain.lean create mode 100644 Ix/Aiur/Formal/ExampleMainSem.lean create mode 100644 Ix/Aiur/Formal/GenSem.lean diff --git a/Ix/Aiur/Formal/Example.lean b/Ix/Aiur/Formal/Example.lean new file mode 100644 index 00000000..57004d70 --- /dev/null +++ b/Ix/Aiur/Formal/Example.lean @@ -0,0 +1,161 @@ +module +public import Ix.Aiur.Formal.ExampleMainSem + +/-! +# Aiur Formal Verification — Example Proofs + +Proves properties about the Aiur programs defined across two toplevels: +- `ExampleBase.lean`: `Pair`, `Expr`, `eval`, `swap` → `ExampleBaseSem.lean` +- `ExampleMain.lean`: `ExprList`, `list_sum`, `assert_eval` → `ExampleMainSem.lean` +-/ + +public section + +open Aiur exampleBase exampleMain + +-- ============================================================ +-- 1. Eval is deterministic +-- ============================================================ + +theorem eval_deterministic {e : Expr} {v₁ v₂ : G} {P₁ P₂ : Prop} + (h₁ : eval e v₁ P₁) (h₂ : eval e v₂ P₂) + (hP₁ : P₁) (hP₂ : P₂) : v₁ = v₂ := by + induction h₁ generalizing v₂ P₂ with + | path0 => cases h₂; rfl + | path1 _ _ ih₁ ih₂ => + cases h₂ with + | path1 h₂a h₂b => + show _ + _ = _ + _ + congr 1 + · exact ih₁ h₂a hP₁.1 hP₂.1 + · exact ih₂ h₂b hP₁.2 hP₂.2 + | path2 _ ih => + cases h₂ with + | path2 h₂a => + show (0 : G) - _ = (0 : G) - _ + congr 1; exact ih h₂a hP₁ hP₂ + +-- ============================================================ +-- 2. Eval is total +-- ============================================================ + +theorem eval_total (e : Expr) : + ∃ (v : G) (P : Prop), eval e v P ∧ P := by + induction e with + | Lit n => exact ⟨n, True, .path0, trivial⟩ + | Add a b iha ihb => + obtain ⟨va, Pa, ha, hPa⟩ := iha + obtain ⟨vb, Pb, hb, hPb⟩ := ihb + exact ⟨va + vb, Pa ∧ Pb, .path1 ha hb, hPa, hPb⟩ + | Neg a iha => + obtain ⟨va, Pa, ha, hPa⟩ := iha + exact ⟨(0 : G) - va, Pa, .path2 ha, hPa⟩ + +-- ============================================================ +-- 3. Swap is an involution +-- ============================================================ + +theorem swap_involution {p q r : Pair} {P₁ P₂ : Prop} + (h₁ : swap p q P₁) (h₂ : swap q r P₂) + (_ : P₁) (_ : P₂) : r = p := by + cases h₁; cases h₂; rfl + +-- ============================================================ +-- 4. assert_eval semantics +-- ============================================================ + +theorem assert_eval_correct {e : Expr} {expected : G} {P : Prop} + (h : assert_eval e expected () P) (hP : P) : + ∃ v Pv, eval e v Pv ∧ Pv ∧ v = expected := by + cases h with + | path0 h_eval => exact ⟨_, _, h_eval, hP.1, hP.2⟩ + +-- ============================================================ +-- 5. list_sum is deterministic (uses eval_deterministic cross-toplevel) +-- ============================================================ + +theorem list_sum_deterministic {xs : ExprList} {v₁ v₂ : G} {P₁ P₂ : Prop} + (h₁ : list_sum xs v₁ P₁) (h₂ : list_sum xs v₂ P₂) + (hP₁ : P₁) (hP₂ : P₂) : v₁ = v₂ := by + induction h₁ generalizing v₂ P₂ with + | path0 => cases h₂; rfl + | path1 h₁e _ ih => + cases h₂ with + | path1 h₂e h₂r => + show _ + _ = _ + _ + congr 1 + · exact eval_deterministic h₁e h₂e hP₁.1 hP₂.1 + · exact ih h₂r hP₁.2 hP₂.2 + +-- ============================================================ +-- 6. Spec-based: eval matches a Lean function +-- ============================================================ + +def evalSpec : Expr → G + | .Lit n => n + | .Add a b => evalSpec a + evalSpec b + | .Neg a => (0 : G) - evalSpec a + +theorem eval_sound {e : Expr} {v : G} {P : Prop} + (h : eval e v P) (hP : P) : v = evalSpec e := by + induction h with + | path0 => rfl + | path1 _ _ ih₁ ih₂ => simp only [evalSpec, ih₁ hP.1, ih₂ hP.2] + | path2 _ ih => simp only [evalSpec, ih hP] + +-- ============================================================ +-- 7. Mutual types: tree_sum / forest_sum match Lean specs +-- ============================================================ + +mutual +def treeSpec : Tree → G + | .Leaf n => n + | .Node n f => n + forestSpec f + +def forestSpec : Forest → G + | .Empty => 0 + | .Cons t rest => treeSpec t + forestSpec rest +end + +mutual +def tree_sum_sound {t : Tree} {v : G} {P : Prop} + (h : tree_sum t v P) (hP : P) : v = treeSpec t := by + cases h with + | path0 => rfl + | path1 hf => simp only [treeSpec, forest_sum_sound hf hP] + +def forest_sum_sound {f : Forest} {v : G} {P : Prop} + (h : forest_sum f v P) (hP : P) : v = forestSpec f := by + cases h with + | path0 => rfl + | path1 ht hf => simp only [forestSpec, tree_sum_sound ht hP.1, forest_sum_sound hf hP.2] +end + +-- ============================================================ +-- 8. Mutual recursion: is_even and is_odd constraints are exclusive +-- +-- The path0 constraint (`G.eqZero n = 1`) and the path1 constraint +-- (`G.eqZero n = 0`) cannot both hold. This means path0 and path1 +-- can never fire for the same `n`, which is what makes the mutual +-- semantic propositions deterministic. +-- ============================================================ + +theorem even_odd_path_exclusive {n : G} + (h0 : G.eqZero n = (1 : G)) (h1 : G.eqZero n = (0 : G)) : False := + absurd (h0.symm.trans h1) G.one_ne_zero + +theorem even_zero {n r : G} {P : Prop} + (h : is_even n r P) (hP : P) (hz : G.eqZero n = (1 : G)) : + r = (1 : G) := by + cases h with + | path0 => rfl + | path1 _ => exact (even_odd_path_exclusive hz hP.2).elim + +theorem odd_zero {n r : G} {P : Prop} + (h : is_odd n r P) (hP : P) (hz : G.eqZero n = (1 : G)) : + r = (0 : G) := by + cases h with + | path0 => rfl + | path1 _ => exact (even_odd_path_exclusive hz hP.2).elim + +end diff --git a/Ix/Aiur/Formal/ExampleBase.lean b/Ix/Aiur/Formal/ExampleBase.lean new file mode 100644 index 00000000..02ce69ba --- /dev/null +++ b/Ix/Aiur/Formal/ExampleBase.lean @@ -0,0 +1,52 @@ +module +public import Ix.Aiur.Meta +public import Ix.Aiur.Formal.GenSem + +/-! +# Aiur Formal Verification — Example Base + +Defines a small expression language with an evaluator. +`Example.lean` builds on this with composite types. +-/ + +open Aiur + +def exampleBase := ⟦ + type Pair = (G, G) + + enum Expr { + Lit(G), + Add(&Expr, &Expr), + Neg(&Expr) + } + + fn double_eval(e: Expr) -> G { + eval(e) + eval(e) + } + + fn eval(e: Expr) -> G { + match e { + Expr.Lit(n) => n, + Expr.Add(&a, &b) => eval(a) + eval(b), + Expr.Neg(&a) => 0 - eval(a), + } + } + + fn swap(p: Pair) -> Pair { + (proj(p, 1), proj(p, 0)) + } + + fn simplify_neg(e: Expr) -> Expr { + match e { + Expr.Neg(&inner) => + match inner { + Expr.Neg(&x) => x, + Expr.Lit(n) => Expr.Lit(0 - n), + _ => e, + }, + _ => e, + } + } +⟧ + +#aiur_gen exampleBase "ExampleBaseSem.lean" # diff --git a/Ix/Aiur/Formal/ExampleBaseSem.lean b/Ix/Aiur/Formal/ExampleBaseSem.lean new file mode 100644 index 00000000..3e631576 --- /dev/null +++ b/Ix/Aiur/Formal/ExampleBaseSem.lean @@ -0,0 +1,55 @@ +-- Auto-generated by #aiur_gen. Regenerate, don't edit. +module +public import Ix.Aiur.Goldilocks + +public section + +namespace exampleBase + +open Aiur + +-- ══════ Semantic types ══════ + +abbrev Pair := (G × G) + +inductive Expr where + | Lit : G → Expr + | Add : Expr → Expr → Expr + | Neg : Expr → Expr + +-- ══════ Semantic propositions ══════ + +inductive eval : Expr → G → Prop → Prop where + | path0 : + eval (.Lit n) n True + | path1 : + eval a r0 P0 → + eval b r1 P1 → + eval (.Add a b) (r0 + r1) (P0 ∧ P1) + | path2 : + eval a r0 P0 → + eval (.Neg a) ((0 : G) - r0) (P0) + +inductive swap : Pair → Pair → Prop → Prop where + | path0 : + swap p ((p).2, (p).1) True + +inductive simplify_neg : Expr → Expr → Prop → Prop where + | path0 : + simplify_neg (.Neg (.Neg x)) x True + | path1 : + simplify_neg (.Neg (.Lit n)) (.Lit ((0 : G) - n)) True + | path2 : + simplify_neg (.Neg _) e True + | path3 : + simplify_neg _ e True + +inductive double_eval : Expr → G → Prop → Prop where + | path0 : + eval e r0 P0 → + eval e r1 P1 → + double_eval e (r0 + r1) (P0 ∧ P1) + +end exampleBase + +end diff --git a/Ix/Aiur/Formal/ExampleMain.lean b/Ix/Aiur/Formal/ExampleMain.lean new file mode 100644 index 00000000..05fd3628 --- /dev/null +++ b/Ix/Aiur/Formal/ExampleMain.lean @@ -0,0 +1,75 @@ +module +public import Ix.Aiur.Meta +public import Ix.Aiur.Formal.GenSem + +/-! +# Aiur Formal Verification — Example Main + +Defines `ExprList` and functions that use both `Expr` (from `ExampleBase`) +and `ExprList`, demonstrating cross-toplevel type references and mutual +recursion (`is_even` / `is_odd`). Also demonstrates mutual types +(`Tree` / `Forest`). +-/ + +open Aiur + +def exampleMain := ⟦ + enum ExprList { + Nil, + Cons(&Expr, &ExprList) + } + + enum Tree { + Leaf(G), + Node(G, &Forest) + } + + enum Forest { + Empty, + Cons(&Tree, &Forest) + } + + fn list_sum(xs: ExprList) -> G { + match xs { + ExprList.Nil => 0, + ExprList.Cons(&e, &rest) => eval(e) + list_sum(rest), + } + } + + fn assert_eval(e: Expr, expected: G) { + let result = eval(e); + assert_eq!(result, expected); + } + + fn tree_sum(t: Tree) -> G { + match t { + Tree.Leaf(n) => n, + Tree.Node(n, &f) => n + forest_sum(f), + } + } + + fn forest_sum(f: Forest) -> G { + match f { + Forest.Empty => 0, + Forest.Cons(&t, &rest) => tree_sum(t) + forest_sum(rest), + } + } + + fn is_even(n: G) -> G { + match eq_zero(n) { + 1 => 1, + 0 => is_odd(n - 1), + } + } + + fn is_odd(n: G) -> G { + match eq_zero(n) { + 1 => 0, + 0 => is_even(n - 1), + } + } +⟧ + +#aiur_gen exampleMain "ExampleMainSem.lean" + importing Ix.Aiur.Formal.ExampleBaseSem + opening exampleBase # diff --git a/Ix/Aiur/Formal/ExampleMainSem.lean b/Ix/Aiur/Formal/ExampleMainSem.lean new file mode 100644 index 00000000..c650168d --- /dev/null +++ b/Ix/Aiur/Formal/ExampleMainSem.lean @@ -0,0 +1,84 @@ +-- Auto-generated by #aiur_gen. Regenerate, don't edit. +module +public import Ix.Aiur.Goldilocks +public import Ix.Aiur.Formal.ExampleBaseSem + +public section + +namespace exampleMain + +open Aiur exampleBase + +-- ══════ Semantic types ══════ + +inductive ExprList where + | Nil + | Cons : Expr → ExprList → ExprList + +mutual + +inductive Tree where + | Leaf : G → Tree + | Node : G → Forest → Tree + +inductive Forest where + | Empty + | Cons : Tree → Forest → Forest + +end + +-- ══════ Semantic propositions ══════ + +inductive list_sum : ExprList → G → Prop → Prop where + | path0 : + list_sum .Nil (0 : G) True + | path1 : + eval e r0 P0 → + list_sum rest r1 P1 → + list_sum (.Cons e rest) (r0 + r1) (P0 ∧ P1) + +inductive assert_eval : Expr → G → Unit → Prop → Prop where + | path0 : + eval e r0 P0 → + assert_eval e expected () (P0 ∧ r0 = expected) + +mutual + +inductive tree_sum : Tree → G → Prop → Prop where + | path0 : + tree_sum (.Leaf n) n True + | path1 : + forest_sum f r0 P0 → + tree_sum (.Node n f) (n + r0) (P0) + +inductive forest_sum : Forest → G → Prop → Prop where + | path0 : + forest_sum .Empty (0 : G) True + | path1 : + tree_sum t r0 P0 → + forest_sum rest r1 P1 → + forest_sum (.Cons t rest) (r0 + r1) (P0 ∧ P1) + +end + +mutual + +inductive is_even : G → G → Prop → Prop where + | path0 : + is_even n (1 : G) ((G.eqZero n) = (1 : G)) + | path1 : + is_odd (n - (1 : G)) r0 P0 → + is_even n r0 (P0 ∧ (G.eqZero n) = (0 : G)) + +inductive is_odd : G → G → Prop → Prop where + | path0 : + is_odd n (0 : G) ((G.eqZero n) = (1 : G)) + | path1 : + is_even (n - (1 : G)) r0 P0 → + is_odd n r0 (P0 ∧ (G.eqZero n) = (0 : G)) + +end + +end exampleMain + +end diff --git a/Ix/Aiur/Formal/GenSem.lean b/Ix/Aiur/Formal/GenSem.lean new file mode 100644 index 00000000..5f8a047c --- /dev/null +++ b/Ix/Aiur/Formal/GenSem.lean @@ -0,0 +1,675 @@ +module +public meta import Ix.Aiur.Term +public meta import Lean.Elab +public meta import Lean.Elab.Command + +/-! +# Aiur Formal Verification — `#aiur_gen` Command + +Generates Lean source files from an `Aiur.Toplevel`, containing: + +- **Sem types**: Lean `inductive`s mirroring Aiur enums, with pointers (`&T`) + erased to `T`. Type aliases become `abbrev`s. + +- **Semantic propositions**: one `inductive` per Aiur function, with one + constructor per control-flow path. `assertEq` becomes a `Prop` conjunct, + function calls become premises, `store`/`load` are erased, and u8/u32 + operations carry range constraints. + +Functions are topologically sorted by their call graph. Mutually recursive +clusters are wrapped in `mutual ... end`; acyclic dependencies are emitted +in dependency order. + +## Syntax + +``` +#aiur_gen myTypes "TypesSem.lean" # +#aiur_gen myFuns "FunsSem.lean" importing Ix.Foo.TypesSem opening myTypes # +``` + +- `importing` adds `public import` lines to the generated file. +- `opening` adds `open` declarations for namespaces from those imports. +- `#` at the end completes the syntax and marks the user intent to write the file. +-/ + +public meta section + +namespace Aiur.Formal + +open Aiur +open Lean Elab Command Meta + +-- ════════════════════════════════════════════════════════════ +-- Toplevel evaluation +-- ════════════════════════════════════════════════════════════ + +/-- Evaluate a `Toplevel` constant by name at elaboration time. + Uses `evalConstCheck` (native evaluation), which requires + `precompileModules := true` on the library. -/ +unsafe def evalToplevelImpl (name : Name) : CommandElabM Toplevel := do + let env ← getEnv + let opts ← getOptions + ofExcept <| env.evalConstCheck Toplevel opts ``Toplevel name + +@[implemented_by evalToplevelImpl] +opaque evalToplevel (name : Name) : CommandElabM Toplevel + +-- ════════════════════════════════════════════════════════════ +-- Generated file IR +-- +-- The code generator builds this intermediate representation, +-- then a single `render` pass converts it to a `.lean` file. +-- ════════════════════════════════════════════════════════════ + +/-- A constructor of a generated Lean `inductive`. -/ +structure GenCtor where + name : String + argTypes : List String + +/-- A generated Lean `inductive` (from an Aiur `enum`). -/ +structure GenInductive where + name : String + ctors : List GenCtor + +/-- A generated Lean `abbrev` (from an Aiur `type` alias). -/ +structure GenAlias where + name : String + typ : String + +/-- A constructor of an semantic proposition. + Each one represents a single complete execution path through + the corresponding Aiur function. -/ +structure GenEvalCtor where + /-- Constructor name, e.g. `"path0"`. -/ + name : String + /-- Premises from sub-function calls, e.g. `["eval a r0 P0"]`. -/ + premises : List String + /-- Input patterns (possibly refined by match), e.g. `[".Nil"]`. -/ + inputPats : List String + /-- The output expression, e.g. `"(r0 + r1)"`. -/ + output : String + /-- The accumulated `Prop` constraint, e.g. `"(P0 ∧ P1)"` or `"True"`. -/ + prop : String + +/-- An semantic proposition for one Aiur function. -/ +structure GenEvalRel where + /-- Relation name, e.g. `"eval"`. -/ + name : String + /-- Type signature, e.g. `"Expr → G → Prop → Prop"`. -/ + sig : String + ctors : List GenEvalCtor + deriving Inhabited + +/-- A group of sem types. Mutually recursive data types share + a `mutual` block; acyclic ones are standalone. -/ +inductive GenTypeBlock where + | single : GenInductive → GenTypeBlock + | mutual : List GenInductive → GenTypeBlock + +/-- A group of semantic propositions. Mutually recursive functions share + a `mutual` block; all others are standalone. -/ +inductive GenEvalBlock where + | single : GenEvalRel → GenEvalBlock + | mutual : List GenEvalRel → GenEvalBlock + +/-- The complete IR for a generated `.lean` file. -/ +structure GenFile where + ns : String + imports : List String + opens : List String + aliases : List GenAlias + typeBlocks : List GenTypeBlock + evalBlocks : List GenEvalBlock + +-- ════════════════════════════════════════════════════════════ +-- Rendering IR → String +-- ════════════════════════════════════════════════════════════ + +def GenAlias.render (a : GenAlias) : String := + s!"abbrev {a.name} := {a.typ}\n" + +def GenInductive.render (ind : GenInductive) : String := + let ctors := ind.ctors.map fun c => + if c.argTypes.isEmpty then s!" | {c.name}" + else s!" | {c.name} : {" → ".intercalate c.argTypes} → {ind.name}" + s!"inductive {ind.name} where\n{"\n".intercalate ctors}\n" + +def GenEvalCtor.render (relName : String) (c : GenEvalCtor) : String := + let premises := c.premises.map fun p => s!" {p} →\n" + let inputPats := " ".intercalate c.inputPats + s!" | {c.name} :\n{String.join premises} {relName} {inputPats} {c.output} {c.prop}" + +def GenEvalRel.render (r : GenEvalRel) : String := + let ctors := r.ctors.map (GenEvalCtor.render r.name) + s!"inductive {r.name} : {r.sig} where\n{"\n".intercalate ctors}\n" + +def GenTypeBlock.render : GenTypeBlock → String + | .single ind => ind.render + | .mutual inds => "mutual\n\n" ++ "\n".intercalate (inds.map GenInductive.render) ++ "\nend\n" + +def GenEvalBlock.render : GenEvalBlock → String + | .single r => r.render + | .mutual rs => "mutual\n\n" ++ "\n".intercalate (rs.map GenEvalRel.render) ++ "\nend\n" + +def GenFile.render (f : GenFile) : String := + let imports := "public import Ix.Aiur.Goldilocks\n" ++ + String.join (f.imports.map fun i => s!"public import {i}\n") + let opens := "open Aiur" ++ + (if f.opens.isEmpty then "" else " " ++ " ".intercalate f.opens) + String.join [ + "-- Auto-generated by #aiur_gen. Regenerate, don't edit.\nmodule\n", + imports, + "\npublic section\n\n", + s!"namespace {f.ns}\n\n", + s!"{opens}\n\n", + "-- ══════ Semantic types ══════\n\n", + String.join (f.aliases.map (·.render ++ "\n")), + "\n".intercalate (f.typeBlocks.map (·.render)), + "\n-- ══════ Semantic propositions ══════\n\n", + "\n".intercalate (f.evalBlocks.map (·.render)), + s!"\nend {f.ns}\n\nend\n" + ] + +-- ════════════════════════════════════════════════════════════ +-- Expression-level helpers +-- +-- These produce Lean syntax *fragments* (not whole declarations). +-- Used by the Eval path enumerator below. +-- ════════════════════════════════════════════════════════════ + +/-- Map an Aiur `Typ` to the corresponding Lean type expression. + Pointers are erased: `&T` becomes `T`. -/ +partial def typToSem : Typ → String + | .unit => "Unit" + | .field => "G" + | .pointer t => typToSem t + | .typeRef g => g.toName.toString (escape := false) + | .tuple ts => s!"({" × ".intercalate (ts.toList.map typToSem)})" + | .array t n => s!"(Fin {n} → {typToSem t})" + | .function _ _ => "sorry /- function type -/" + +/-- Render a Goldilocks field element as a Lean numeric literal. -/ +def renderG (g : G) : String := s!"({g.val.toNat} : G)" + +/-- Render an Aiur local variable name as a Lean identifier. -/ +def renderLocal : Local → String + | .str s => s + | .idx n => s!"_v{n}" + +-- ════════════════════════════════════════════════════════════ +-- Sem type construction +-- ════════════════════════════════════════════════════════════ + +def mkGenInductive (dt : DataType) : GenInductive := + { name := dt.name.toName.toString (escape := false) + ctors := dt.constructors.map fun c => + { name := c.nameHead, argTypes := c.argTypes.map typToSem } } + +def mkGenAlias (ta : TypeAlias) : GenAlias := + { name := ta.name.toName.toString (escape := false) + typ := typToSem ta.expansion } + +-- ════════════════════════════════════════════════════════════ +-- Eval path enumeration +-- +-- Walks an Aiur `Term` and enumerates all complete execution +-- paths through it. Each path accumulates: +-- +-- - **Premises**: from function calls (`f.Eval args result P`) +-- - **Prop parts**: from `assertEq` (`a = b`) and match conditions +-- on intermediate values (`G.eqZero n = (1 : G)`) +-- - **Sub-props**: the `P` variables from sub-call premises +-- - **Match bindings**: when the scrutinee is a function input, +-- records `(input, pattern)` to refine the Eval signature +-- +-- The result for each path is a `(outputExpr, GenState)` pair. +-- ════════════════════════════════════════════════════════════ + +/-- A premise in an Eval constructor, e.g. `"eval a r0 P0"`. + Wrapped for clarity; will appear as `premise → ...` in the output. -/ +structure Premise where + text : String + deriving Inhabited + +/-- Mutable state threaded through path enumeration. -/ +structure GenState where + freshVarIdx : Nat := 0 + freshPropIdx : Nat := 0 + premises : Array Premise := #[] + /-- Prop conjuncts from `assertEq` and field-match conditions. -/ + propParts : Array String := #[] + /-- Prop variables introduced by sub-call premises (`P0`, `P1`, ...). -/ + subProps : Array String := #[] + /-- Local variable bindings: name → expression. -/ + bindings : List (String × String) := [] + /-- Match bindings: `(scrutinee, pattern)` for input-level matches. -/ + matchBindings : Array (String × String) := #[] + /-- Named variables (function params + pattern-bound), used to distinguish + input/variable matches (which refine the Eval signature) from + intermediate expression matches (which add Prop constraints). -/ + namedVars : List String := [] + /-- Constructor names from the toplevel's data types. When `app` references + one of these, it emits a constructor expression instead of a premise. -/ + ctorNames : Std.HashSet String := {} + +def GenState.fresh (s : GenState) (prefix_ : String := "r") : String × GenState := + (s!"{prefix_}{s.freshVarIdx}", { s with freshVarIdx := s.freshVarIdx + 1 }) + +def GenState.freshProp (s : GenState) : String × GenState := + let name := s!"P{s.freshPropIdx}" + (name, { s with freshPropIdx := s.freshPropIdx + 1 }) + +def GenState.addPremise (s : GenState) (p : String) : GenState := + { s with premises := s.premises.push ⟨p⟩ } + +def GenState.addProp (s : GenState) (p : String) : GenState := + { s with propParts := s.propParts.push p } + +def GenState.addSubProp (s : GenState) (p : String) : GenState := + { s with subProps := s.subProps.push p } + +def GenState.bind (s : GenState) (name expr : String) : GenState := + { s with bindings := (name, expr) :: s.bindings } + +def GenState.resolve (s : GenState) (name : String) : String := + match s.bindings.find? (·.1 == name) with + | some (_, e) => e + | none => name + +/-- Render the accumulated Prop as a single expression. + Empty → `True`. Single → parenthesized. Multiple → conjoined. -/ +def GenState.renderProp (s : GenState) : String := + let all := s.subProps ++ s.propParts + if all.isEmpty then "True" + else if all.size == 1 then s!"({all[0]!})" + else s!"({" ∧ ".intercalate all.toList})" + +/-- Collect variable names introduced by a pattern. -/ +partial def patternVarNames : Pattern → List String + | .var l => [renderLocal l] + | .pointer p => patternVarNames p + | .or p1 _ => patternVarNames p1 + | .ref _ pats => pats.flatMap patternVarNames + | .tuple ps => ps.toList.flatMap patternVarNames + | .array ps => ps.toList.flatMap patternVarNames + | _ => [] + +/-- Render an Aiur `Pattern` to Lean expression(s). + Returns multiple results when `or` patterns appear at any nesting + level, since each alternative is a distinct execution path. -/ +partial def renderPatExprs (s : GenState) : Pattern → List (String × GenState) + | .var l => [(renderLocal l, s)] + | .wildcard => [("_", s)] + | .field g => [(renderG g, s)] + | .pointer p => renderPatExprs s p + | .or p1 p2 => renderPatExprs s p1 ++ renderPatExprs s p2 + | .ref g pats => + let ctorName := match g.toName with + | .str _ s => s + | n => n.toString (escape := false) + let init : List (List String × GenState) := [([], s)] + let results := pats.foldl (init := init) fun acc pat => + acc.flatMap fun (strs, s) => + (renderPatExprs s pat).map fun (str, s) => (strs ++ [str], s) + results.map fun (argStrs, s) => + if argStrs.isEmpty then (s!".{ctorName}", s) + else (s!"(.{ctorName} {" ".intercalate argStrs})", s) + | .tuple ps => + let init : List (Array String × GenState) := [(#[], s)] + let results := ps.foldl (init := init) fun acc pat => + acc.flatMap fun (strs, s) => + (renderPatExprs s pat).map fun (str, s) => (strs.push str, s) + results.map fun (strs, s) => (s!"({", ".intercalate strs.toList})", s) + | .array ps => + let init : List (Array String × GenState) := [(#[], s)] + let results := ps.foldl (init := init) fun acc pat => + acc.flatMap fun (strs, s) => + (renderPatExprs s pat).map fun (str, s) => (strs.push str, s) + results.map fun (strs, s) => (s!"#[{", ".intercalate strs.toList}]", s) + +/-- Enumerate all execution paths through a `Term`. + Each path produces an output expression and accumulated state. + IO operations produce unconstrained fresh variables (loose semantics). -/ +partial def termPaths (s : GenState) (t : Term) : List (String × GenState) + := match t with + -- Atoms + | .unit => [("()", s)] + | .var l => [(s.resolve (renderLocal l), s)] + | .ref g => [(g.toName.toString (escape := false), s)] + | .data (.field g) => [(renderG g, s)] + | .data (.tuple ts) => + (evalArgs s ts.toList).map fun (strs, s) => + (s!"({", ".intercalate strs})", s) + | .data (.array ts) => + (evalArgs s ts.toList).map fun (strs, s) => + (s!"#[{", ".intercalate strs}]", s) + -- Control flow: transparent wrappers + | .ret t => termPaths s t + | .ann _ t => termPaths s t + | .debug _ _ ret => termPaths s ret + -- Control flow: let binding + | .let pat val body => + (termPaths s val).flatMap fun (vval, s) => + (renderPatExprs s pat).flatMap fun (patExpr, s) => + let s := if patExpr == "_" then s else s.bind patExpr vval + let s := { s with namedVars := s.namedVars ++ patternVarNames pat } + termPaths s body + -- Control flow: match (branches multiply paths) + | .match scrut branches => + (termPaths s scrut).flatMap fun (vscrut, s) => + branches.flatMap fun (pat, body) => + (renderPatExprs s pat).flatMap fun (patStr, s) => + let s := if s.namedVars.contains vscrut then + { s with matchBindings := s.matchBindings.push (vscrut, patStr) } + else + s.addProp s!"{vscrut} = {patStr}" + let s := { s with namedVars := s.namedVars ++ patternVarNames pat } + termPaths s body + -- Field arithmetic + | .add a b => binOp s a b " + " + | .sub a b => binOp s a b " - " + | .mul a b => binOp s a b " * " + | .eqZero a => + (termPaths s a).map fun (va, s) => (s!"(G.eqZero {va})", s) + -- Pointer operations (erased in the semantic domain) + | .store t => termPaths s t + | .load t => termPaths s t + | .ptrVal _ => let (v, s) := s.fresh "io"; [(v, s)] + -- Aggregate operations + | .proj t n => -- Aiur 0-indexed; Lean Prod 1-indexed + (termPaths s t).map fun (vt, s) => (s!"({vt}).{n + 1}", s) + | .get t n => + (termPaths s t).map fun (vt, s) => (s!"({vt})[{n}]", s) + | .slice t i j => + (termPaths s t).map fun (vt, s) => (s!"({vt}).extract {i} {j}", s) + | .set t i val => + (termPaths s t).flatMap fun (vt, s) => + (termPaths s val).map fun (vv, s) => (s!"({vt}).set {i} {vv}", s) + -- Function calls → premise. Data constructors → direct expression. + | .app g args => + let fname := g.toName.toString (escape := false) + let ctorName := match g.toName with + | .str _ s => s + | n => n.toString (escape := false) + if s.ctorNames.contains fname then + (evalArgs s args).map fun (argStrs, s) => + (s!"(.{ctorName} {" ".intercalate argStrs})", s) + else + (evalArgs s args).map fun (argStrs, s) => + let (result, s) := s.fresh "r" + let (prop, s) := s.freshProp + let premise := s!"{fname} {" ".intercalate argStrs} {result} {prop}" + let s := s.addPremise premise |>.addSubProp prop + (result, s) + -- Assertions → Prop conjunct + | .assertEq a b ret => + (termPaths s a).flatMap fun (va, s) => + (termPaths s b).flatMap fun (vb, s) => + termPaths (s.addProp s!"{va} = {vb}") ret + -- u8 operations: result + range constraints (`G.isU8`) on inputs + | .u8And a b => u8BinOp s a b "G.u8And" + | .u8Or a b => u8BinOp s a b "G.u8Or" + | .u8Xor a b => u8BinOp s a b "G.u8Xor" + | .u8LessThan a b => u8BinOp s a b "G.u8LessThan" + | .u8Add a b => u8BinOp s a b "G.u8Add" + | .u8Sub a b => u8BinOp s a b "G.u8Sub" + | .u8ShiftLeft a => u8UnOp s a "G.u8ShiftLeft" + | .u8ShiftRight a => u8UnOp s a "G.u8ShiftRight" + | .u8BitDecomposition a => u8UnOp s a "G.u8BitDecomposition" + -- u32 operations: result + range constraints (`G.isU32`) on inputs + | .u32LessThan a b => + (termPaths s a).flatMap fun (va, s) => + (termPaths s b).map fun (vb, s) => + let s := s.addProp s!"G.isU32 {va}" |>.addProp s!"G.isU32 {vb}" + (s!"(G.u32LessThan {va} {vb})", s) + -- IO: unconstrained fresh variables (loose semantics) + | .ioGetInfo _ => + let (v1, s) := s.fresh "io" + let (v2, s) := s.fresh "io" + [(s!"({v1}, {v2})", s)] + | .ioRead _ len => + let (vars, s) := List.range len |>.foldl (init := ([], s)) fun (vars, s) _ => + let (v, s) := s.fresh "io"; (vars ++ [v], s) + [(s!"#[{", ".intercalate vars}]", s)] + | .ioWrite _ ret => termPaths s ret + | .ioSetInfo _ _ _ ret => termPaths s ret +where + binOp (s : GenState) (a b : Term) (op : String) : List (String × GenState) := + (termPaths s a).flatMap fun (va, s) => + (termPaths s b).map fun (vb, s) => (s!"({va}{op}{vb})", s) + u8BinOp (s : GenState) (a b : Term) (fn : String) : List (String × GenState) := + (termPaths s a).flatMap fun (va, s) => + (termPaths s b).map fun (vb, s) => + let s := s.addProp s!"G.isU8 {va}" |>.addProp s!"G.isU8 {vb}" + (s!"({fn} {va} {vb})", s) + u8UnOp (s : GenState) (a : Term) (fn : String) : List (String × GenState) := + (termPaths s a).map fun (va, s) => + let s := s.addProp s!"G.isU8 {va}" + (s!"({fn} {va})", s) + evalArgs (s : GenState) (args : List Term) : List (List String × GenState) := + args.foldl (init := [([], s)]) fun acc arg => + acc.flatMap fun (strs, s) => + (termPaths s arg).map fun (str, s) => (strs ++ [str], s) + +-- ════════════════════════════════════════════════════════════ +-- Function → GenEvalRel +-- ════════════════════════════════════════════════════════════ + +/-- Build the semantic proposition IR for a single Aiur function. -/ +def mkGenEvalRel (f : Function) (ctorNames : Std.HashSet String) : GenEvalRel := + let fname := f.name.toName.toString (escape := false) + let inputTypes := f.inputs.map fun (_, ty) => typToSem ty + let outputType := typToSem f.output + let sig := " → ".intercalate (inputTypes ++ [outputType, "Prop", "Prop"]) + let namedVars := f.inputs.map fun (l, _) => renderLocal l + let initState : GenState := { + bindings := namedVars.map fun n => (n, n) + namedVars + ctorNames + } + let paths := termPaths initState f.body + let ctors := paths.zipIdx.map fun ((output, gs), i) => + -- Resolve match bindings transitively. E.g. if we have: + -- e → (.Neg inner) and inner → (.Neg x) + -- then `e` should resolve to `(.Neg (.Neg x))`. + -- We do this by resolving the binding map itself: for each binding + -- `v → pat`, replace occurrences of other bound variables in `pat`. + -- We pad parens with spaces to tokenize cleanly. + let bindings := gs.matchBindings + let pad (s : String) := s.replace "(" "( " |>.replace ")" " )" + let unpad (s : String) := s.replace "( " "(" |>.replace " )" ")" + let resolvedBindings := Id.run do + let mut m : Array (String × String) := bindings + for _ in List.range (bindings.size + 1) do + m := m.map fun (var, pat) => + let padded := pad pat + let tokens := padded.splitOn " " + let tokens := tokens.map fun tok => + match m.find? (·.1 == tok) with + | some (_, p) => pad p + | none => tok + (var, unpad (" ".intercalate tokens)) + m + let inputPats := namedVars.map fun name => + match resolvedBindings.find? (·.1 == name) with + | some (_, pat) => pat + | none => name + { name := s!"path{i}" + premises := gs.premises.toList.map (·.text) + inputPats + output + prop := gs.renderProp : GenEvalCtor } + { name := fname, sig, ctors } + +-- ════════════════════════════════════════════════════════════ +-- Dependency graph analysis +-- +-- Computes strongly connected components of a dependency +-- graph and topologically sorts them. SCCs with >1 node +-- become `mutual` blocks; singletons are standalone. +-- Used for both type and function dependency graphs. +-- ════════════════════════════════════════════════════════════ + +/-- Collect all type names referenced (via `typeRef`) in a `Typ`. -/ +partial def collectTypeRefs : Typ → List String + | .typeRef g => [g.toName.toString (escape := false)] + | .pointer t | .array t _ => collectTypeRefs t + | .tuple ts => ts.toList.flatMap collectTypeRefs + | .function args ret => args.flatMap collectTypeRefs ++ collectTypeRefs ret + | _ => [] + +/-- Collect all function names called (via `app`) in a `Term`. -/ +partial def collectCalls : Term → List String + | .app g args => g.toName.toString (escape := false) :: + args.flatMap collectCalls + | .add a b | .sub a b | .mul a b | .u8Xor a b | .u8Add a b | .u8Sub a b + | .u8And a b | .u8Or a b | .u8LessThan a b | .u32LessThan a b => + collectCalls a ++ collectCalls b + | .eqZero a | .store a | .load a | .ptrVal a | .ret a + | .u8BitDecomposition a | .u8ShiftLeft a | .u8ShiftRight a => + collectCalls a + | .ann _ t | .debug _ _ t => collectCalls t + | .assertEq a b ret => collectCalls a ++ collectCalls b ++ collectCalls ret + | .let _ val body => collectCalls val ++ collectCalls body + | .match scrut branches => + collectCalls scrut ++ branches.flatMap fun (_, body) => collectCalls body + | .data (.tuple ts) => ts.toList.flatMap collectCalls + | .data (.array ts) => ts.toList.flatMap collectCalls + | .proj t _ | .get t _ => collectCalls t + | .slice t _ _ => collectCalls t + | .set t _ v => collectCalls t ++ collectCalls v + | .ioSetInfo a b c d => + collectCalls a ++ collectCalls b ++ collectCalls c ++ collectCalls d + | .ioWrite a b => collectCalls a ++ collectCalls b + | .ioGetInfo a | .ioRead a _ => collectCalls a + | _ => [] + +/-- Compute SCCs of a dependency graph and return them in + topological order (dependencies before dependents). -/ +def topoSortSCCs (items : List α) (nameOf : α → String) + (depsOf : α → List String) : List (List α) := + let names := items.map nameOf + let localSet : Std.HashSet String := .ofList names + -- Adjacency: only cross-references to other local items (self-refs excluded) + let adj : Std.HashMap String (List String) := .ofList <| + items.map fun item => + let self := nameOf item + (self, (depsOf item |>.filter fun c => + c != self && localSet.contains c) |>.eraseDups) + let nameToItem : Std.HashMap String α := + .ofList <| items.map fun item => (nameOf item, item) + -- BFS reachability from a given start node + let reachFrom (start : String) : Std.HashSet String := Id.run do + let mut visited : Std.HashSet String := {} + let mut queue := [start] + for _ in List.range (names.length * names.length + 1) do + match queue with + | [] => break + | n :: rest => + queue := rest + if visited.contains n then continue + visited := visited.insert n + queue := queue ++ (adj.getD n []) + return visited + let reachMap : Std.HashMap String (Std.HashSet String) := .ofList <| + names.map fun n => (n, reachFrom n) + -- SCC: A and B are in the same SCC iff A reaches B and B reaches A + let sccOf (name : String) : List String := + names.filter fun other => + (reachMap.getD name {}).contains other && + (reachMap.getD other {}).contains name + -- Collect SCCs in source order, deduplicating + let (sccs, _) := names.foldl (init := ([], ({} : Std.HashSet String))) + fun (sccs, assigned) name => + if assigned.contains name then (sccs, assigned) + else + let cluster := sccOf name + let assigned := cluster.foldl (init := assigned) fun s n => s.insert n + (sccs ++ [cluster], assigned) + -- Topological sort: emit an SCC only after all its dependencies are emitted + let sccIdx : Std.HashMap String Nat := .ofList <| + sccs.zipIdx.flatMap fun (cluster, i) => cluster.map fun n => (n, i) + let sccDeps (cluster : List String) : Std.HashSet Nat := + let myIdx := sccIdx.getD cluster.head! 0 + cluster.foldl (init := {}) fun deps name => + (adj.getD name []).foldl (init := deps) fun deps callee => + let calleeIdx := sccIdx.getD callee myIdx + if calleeIdx != myIdx then deps.insert calleeIdx else deps + Id.run do + let mut remaining : Std.HashSet Nat := .ofList (List.range sccs.length) + let mut result : List (List α) := [] + for _ in List.range (sccs.length + 1) do + if remaining.isEmpty then break + for (cluster, i) in sccs.zipIdx do + if !remaining.contains i then continue + if (sccDeps cluster).toList.all fun d => !remaining.contains d then + remaining := remaining.erase i + result := result ++ [cluster.filterMap nameToItem.get?] + return result + +-- ════════════════════════════════════════════════════════════ +-- Toplevel → GenFile +-- ════════════════════════════════════════════════════════════ + +/-- Build the complete file IR from an Aiur `Toplevel`. -/ +def mkGenFile (top : Toplevel) (ns : String) + (extraImports : List String) (openNs : List String) : GenFile := + let aliases := top.typeAliases.toList.map mkGenAlias + let dts := top.dataTypes.toList + let dtNameOf (dt : DataType) := dt.name.toName.toString (escape := false) + let dtDepsOf (dt : DataType) := + dt.constructors.flatMap fun c => c.argTypes.flatMap collectTypeRefs + let typeGroups := topoSortSCCs dts dtNameOf dtDepsOf + let typeBlocks := typeGroups.map fun group => + let inds := group.map mkGenInductive + match inds with + | [ind] => GenTypeBlock.single ind + | inds => GenTypeBlock.mutual inds + let ctorNames : Std.HashSet String := .ofList <| + dts.flatMap fun dt => + dt.constructors.map fun c => + s!"{dtNameOf dt}.{c.nameHead}" + let funs := top.functions.toList + let funNameOf (f : Function) := f.name.toName.toString (escape := false) + let funDepsOf (f : Function) := collectCalls f.body + let funGroups := topoSortSCCs funs funNameOf funDepsOf + let evalBlocks := funGroups.map fun group => + let rels := group.map (mkGenEvalRel · ctorNames) + match rels with + | [r] => GenEvalBlock.single r + | rs => GenEvalBlock.mutual rs + { ns, imports := extraImports, opens := openNs, + aliases, typeBlocks, evalBlocks } + +-- ════════════════════════════════════════════════════════════ +-- #aiur_gen command +-- ════════════════════════════════════════════════════════════ + +def currentFileDir : CommandElabM System.FilePath := do + let fileName ← getFileName + pure (System.FilePath.mk fileName |>.parent.getD ".") + +syntax "#aiur_gen " ident str (" importing " ident+)? (" opening " ident+)? " #" : command + +elab_rules : command + | `(command| #aiur_gen $topId:ident $file:str + $[ importing $imports*]? $[ opening $opens*]? #) => do + let topName ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo topId + let fileName := file.getString + let top ← evalToplevel topName + let ns := topId.getId.toString (escape := false) + let extraImports := match imports with + | some ids => ids.toList.map fun id => id.getId.toString (escape := false) + | none => [] + let openNs := match opens with + | some ids => ids.toList.map fun id => id.getId.toString (escape := false) + | none => [] + let genFile := mkGenFile top ns extraImports openNs + let dir ← currentFileDir + let outPath := dir / fileName + IO.FS.writeFile outPath genFile.render + logInfo m!"#aiur_gen: wrote {top.dataTypes.size} types, {top.functions.size} functions to {outPath}" + +end Aiur.Formal + +end diff --git a/Ix/Aiur/Goldilocks.lean b/Ix/Aiur/Goldilocks.lean index 97ad74f7..b8f46fb5 100644 --- a/Ix/Aiur/Goldilocks.lean +++ b/Ix/Aiur/Goldilocks.lean @@ -22,6 +22,64 @@ instance : OfNat G n := ⟨G.ofNat n⟩ exact UInt64.lt_trans lt256 (by decide) ⟨u64, h⟩ +instance : Add G where + add a b := G.ofNat (a.val.toNat + b.val.toNat) + +instance : Sub G where + sub a b := G.ofNat (a.val.toNat + gSize.toNat - b.val.toNat) + +instance : Mul G where + mul a b := G.ofNat (a.val.toNat * b.val.toNat) + +/-- Semantic model of Aiur's `eq_zero` primitive. -/ +def G.eqZero (x : G) : G := if x = (0 : G) then 1 else 0 + +/-- The natural number value of a `G` element. -/ +abbrev G.n (x : G) : Nat := x.val.toNat + +/-- Range predicate for u8 operations. -/ +def G.isU8 (x : G) : Prop := x.n < 256 + +/-- Range predicate for u32 operations. -/ +def G.isU32 (x : G) : Prop := x.n < 2 ^ 32 + +-- Semantic models for unsigned integer operations. +-- These mirror the Aiur circuit gadgets, which force range constraints +-- on their inputs and compute the corresponding bitwise/arithmetic result. + +def G.u8And (a b : G) : G := G.ofNat (a.n &&& b.n) +def G.u8Or (a b : G) : G := G.ofNat (a.n ||| b.n) +def G.u8Xor (a b : G) : G := G.ofNat (a.n ^^^ b.n) +def G.u8LessThan (a b : G) : G := if a.n < b.n then 1 else 0 + +/-- u8 addition returns `(result % 256, carry)`. -/ +def G.u8Add (a b : G) : G × G := + (G.ofNat ((a.n + b.n) % 256), G.ofNat ((a.n + b.n) / 256)) + +/-- u8 subtraction returns `(result % 256, borrow)`. -/ +def G.u8Sub (a b : G) : G × G := + (G.ofNat ((a.n + 256 - b.n) % 256), if a.n < b.n then 1 else 0) + +def G.u8ShiftLeft (a : G) : G := G.ofNat ((a.n * 2) % 256) +def G.u8ShiftRight (a : G) : G := G.ofNat (a.n / 2) + +/-- Bit decomposition: returns an 8-element array (LSB first). -/ +def G.u8BitDecomposition (a : G) : Fin 8 → G := + fun i => G.ofNat ((a.n >>> i.val) &&& 1) + +def G.u32LessThan (a b : G) : G := if a.n < b.n then 1 else 0 + +-- Requires native evaluation because G.ofNat uses @[extern] Nat.toUInt64 +theorem G.one_ne_zero : ¬(1 : G) = (0 : G) := by native_decide + +theorem G.add_comm (a b : G) : a + b = b + a := by + show G.ofNat (a.val.toNat + b.val.toNat) = G.ofNat (b.val.toNat + a.val.toNat) + congr 1; omega + +theorem G.mul_comm (a b : G) : a * b = b * a := by + show G.ofNat (a.val.toNat * b.val.toNat) = G.ofNat (b.val.toNat * a.val.toNat) + congr 1; exact Nat.mul_comm _ _ + end Aiur end diff --git a/lakefile.lean b/lakefile.lean index ecf7ab96..8ed7acd1 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -65,6 +65,7 @@ end FFI @[default_target] lean_lib Ix where moreLinkObjs := #[ix_rs] + precompileModules := true lean_exe ix where root := `Main