From 8e1ddf2d89acc7aaeb0ec16705f7d506d927212b Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 1 Mar 2026 14:08:47 +0000 Subject: [PATCH 1/8] Initial plan From 30cd630bc776c1e7db29b986d6a415fc79973c9b Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 1 Mar 2026 14:36:10 +0000 Subject: [PATCH 2/8] Restore full intrinsically-typed expression language and prove typeCheck_complete - Add Vec type and :: notation to Tibi/Util.lean - Restore Ty, Locals, Var, Lam, App in Tibi/Syntax/Expr.lean - Create Tibi/Semantics/Env.lean with Env type and lookup - Update Tibi/Semantics.lean with Eval for full Expr ctx ty - Restore full HasType and typeCheck in Tibi/Typing.lean - Update Tibi/Interpreter.lean for Expr ctx ty with Env - Update Tibi/Compiler.lean for Expr ctx ty - Update Tibi/Parser.lean to return Expr .nil .int - Update Tibi/Top.lean for new types - Prove typeCheck_correct (strong form), typeCheck_complete, HasType.det, Decidable instance, and type_safe in Props/Typing.lean - Update Props/Compiler.lean for new Expr ctx ty type Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- Tibi/Compiler.lean | 7 ++++- Tibi/Interpreter.lean | 19 ++++++++++++-- Tibi/Parser.lean | 6 ++--- Tibi/Props/Compiler.lean | 4 +-- Tibi/Props/Typing.lean | 46 +++++++++++++++++++++------------ Tibi/Semantics.lean | 18 ++++++++++--- Tibi/Semantics/Env.lean | 14 ++++++++++ Tibi/Syntax/Expr.lean | 55 ++++++++++++++++++++++++++++++++++++---- Tibi/Top.lean | 4 +-- Tibi/Typing.lean | 33 +++++++++++++++++++++--- Tibi/Util.lean | 6 +++++ 11 files changed, 174 insertions(+), 38 deletions(-) create mode 100644 Tibi/Semantics/Env.lean diff --git a/Tibi/Compiler.lean b/Tibi/Compiler.lean index c137d64..b0c6b5b 100644 --- a/Tibi/Compiler.lean +++ b/Tibi/Compiler.lean @@ -8,16 +8,21 @@ open Wasm.Value inductive CompileError | OutOfBounds_Int64 (n : Int) +| Unimplemented -def Expr.compile : Expr → Except CompileError (List Wasm.Instr) +def Expr.compile : Expr ctx ty → Except CompileError (List Wasm.Instr) | .Const n => if h : (-Int64.size : Int) ≤ n ∧ n < Int64.size then .ok [.i64__const <| Int64.mk ⟨n, h.right, h.left⟩] else .error <| .OutOfBounds_Int64 n +| .Var _ => + .error .Unimplemented +| _ => .error .Unimplemented def CompileError.toString : CompileError → String | .OutOfBounds_Int64 n => s!"{n} is out of Int64 bounds, should be satisfied that -2{Nat.toSuperscriptString 63} ≤ n < 2{Nat.toSuperscriptString 63}" +| .Unimplemented => "Unimplemented" instance : ToString CompileError where toString := CompileError.toString diff --git a/Tibi/Interpreter.lean b/Tibi/Interpreter.lean index 57a1892..5bb9401 100644 --- a/Tibi/Interpreter.lean +++ b/Tibi/Interpreter.lean @@ -5,11 +5,26 @@ import Tibi.Util namespace Tibi -def Expr.eval : (e : Expr) → {{ r | Eval e r }} -| .Const n => +def Expr.eval (env : Env ctx) : {ty : Ty} → (e : Expr ctx ty) → ty.dom → {{ r | Eval e r }} +| _, .Const n, _ => if h : (-Int64.size : Int) ≤ n ∧ n < Int64.size then .found (.ok <| Int64.mk ⟨n, h.right, h.left⟩) <| Eval.Const h.right h.left else Decidable.not_and_iff_or_not_not.mp h |>.by_cases (fun h => .found (.error <| .OutOfBounds_Int64 n) <| Eval.ConstErr_ge h) (fun h => .found (.error <| .OutOfBounds_Int64 n) <| Eval.ConstErr_lt h) +| _, .Var x, _ => + .found (.ok <| env.lookup x) <| .Var x env +| _, .Lam e', x => + match e'.eval (x :: env) x with + | .found (.ok v) h => .found (.ok <| fun _ => v) <| .Lam h + | .unknown => .unknown +| .int, .App (dom := .int) (.Lam e₁) e₂, _ => + match e₂.eval env () with + | .found (.ok v) h₂ => + match e₁.eval (v :: env) v with + | .found (.ok v) h₁ => + .found (.ok <| v) <| .App h₁ h₂ + | _ => .unknown + | _ => .unknown +| _, _, _ => .unknown diff --git a/Tibi/Parser.lean b/Tibi/Parser.lean index 69ca398..0823d0d 100644 --- a/Tibi/Parser.lean +++ b/Tibi/Parser.lean @@ -62,7 +62,7 @@ private def intNumber : Parser Int := | _ => sgn n ) -private def parser : Parser Expr := +private def parser : Parser (Expr .nil .int) := ( natNumber >> ws -- >> ParserT.optional ((ParserT.char '@' : Parser _) >> keyword "Int" >> ws) |>.map fun (n, _) => .Const n @@ -72,10 +72,10 @@ private def parser : Parser Expr := |>.map fun (n, _) => .Const n ) -instance : Inhabited (Parser Expr) where +instance : Inhabited (Parser (Expr .nil .int)) where default := parser -private partial def parse' : ReaderT (IO String) Parser Expr := do +private partial def parse' : ReaderT (IO String) Parser (Expr .nil .int) := do fun getLine cs => match parser cs with | .error .UnexpectedEndOfInput => do diff --git a/Tibi/Props/Compiler.lean b/Tibi/Props/Compiler.lean index ac6793f..1559777 100644 --- a/Tibi/Props/Compiler.lean +++ b/Tibi/Props/Compiler.lean @@ -5,11 +5,11 @@ import Tibi.Wasm.Semantics namespace Tibi theorem Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok -- Expr.compile_ok_of_has_type_of_eval -: {e : Expr} → HasType e _ty → Eval e (.ok v) → {_ : e.compile = .ok instrs} +: HasType e _ty → Eval e (.ok v) → e.compile = .ok instrs → Wasm.Reduction { instrs := instrs ++ K, stack, store, framestate } { instrs := K, stack := .Value (.Num (.Int64 v)) :: stack, store, framestate } -| .Const n, .Int64 hLt hGe, .Const _ _, hc => by +| .Int64 hLt hGe, .Const _ _, hc => by have : (Expr.Const n).compile = .ok [.i64__const (Int64.mk ⟨n, hLt, hGe⟩)] := by -- dsimp [Expr.compile] apply dite_cond_eq_true <| eq_true <| And.intro hGe hLt diff --git a/Tibi/Props/Typing.lean b/Tibi/Props/Typing.lean index ad1ca9a..89d2ce8 100644 --- a/Tibi/Props/Typing.lean +++ b/Tibi/Props/Typing.lean @@ -4,26 +4,37 @@ import Tibi.Typing namespace Tibi theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by - cases h₁ <;> cases h₂ <;> rfl + induction h₁ generalizing t₂ with + | Int64 => cases h₂; rfl + | Var => cases h₂; rfl + | Lam _ ih => cases h₂ with | Lam h' => exact congrArg (Typ.Fn (.Var 0)) (ih h') + | App _ _ ihf _ => + cases h₂ with + | App hf' _ => + exact (Typ.Fn.inj (ihf hf')).2 -theorem Expr.typeCheck_correct {e : Expr} -: (ht : HasType e ty) → e.typeCheck = .found ty ht +theorem Expr.typeCheck_correct : (ht : HasType e t) → e.typeCheck = .found t ht | .Int64 (n := n) hLt hGe => have := eq_true <| And.intro (ge_iff_le.mp hGe) hLt dite_cond_eq_true this +| .Var => rfl +| .Lam h => + have ih := typeCheck_correct h + simp only [Expr.typeCheck, ih] +| .App hf hv => by + have ihf := typeCheck_correct hf + have ihv := typeCheck_correct hv + simp only [Expr.typeCheck, ihf, ihv] + exact dif_pos rfl -theorem Expr.typeCheck_complete {e : Expr} -: e.typeCheck = .unknown → ¬ HasType e ty -:= by - dsimp [Expr.typeCheck] - intro h (ht : HasType e ty) - match ht with - | .Int64 hLt hGe => - have := eq_true <| And.intro (ge_iff_le.mp hGe) hLt - have := h ▸ dite_cond_eq_true this - exact Maybe.noConfusion this +theorem Expr.typeCheck_complete {e : Expr ctx ty} +: e.typeCheck = .unknown → ¬ HasType e t +:= fun h ht => by + have := typeCheck_correct ht + rw [h] at this + exact Maybe.noConfusion this -instance (e : Expr) (t : Typ) : Decidable (HasType e t) := +instance (e : Expr ctx ty) (t : Typ) : Decidable (HasType e t) := match h : e.typeCheck with | .found t' ht' => if heq : t = t' then @@ -32,8 +43,11 @@ instance (e : Expr) (t : Typ) : Decidable (HasType e t) := isFalse fun ht => heq (HasType.det ht ht') | .unknown => isFalse (Expr.typeCheck_complete h) -theorem type_safe {e : Expr} +theorem type_safe {e : Expr ctx ty} : HasType e t → Eval e r → ∃ v, r = .ok v -| .Int64 hLt hGe, .Const .. => ⟨Int64.mk ⟨_, hLt, hGe⟩, rfl⟩ +| .Int64 hLt hGe, .Const .. => ⟨_, rfl⟩ | .Int64 hLt _, .ConstErr_lt h => absurd hLt h | .Int64 _ hGe, .ConstErr_ge h => absurd hGe h +| .Var, .Var .. => ⟨_, rfl⟩ +| .Lam _, .Lam .. => ⟨_, rfl⟩ +| .App _ _, .App .. => ⟨_, rfl⟩ diff --git a/Tibi/Semantics.lean b/Tibi/Semantics.lean index f668ba3..e146ba4 100644 --- a/Tibi/Semantics.lean +++ b/Tibi/Semantics.lean @@ -1,4 +1,5 @@ import Tibi.FinInt +import Tibi.Semantics.Env import Tibi.Syntax namespace Tibi @@ -6,10 +7,19 @@ namespace Tibi inductive EvalError | OutOfBounds_Int64 (n : Int) -inductive Eval : Expr → Except EvalError Int64 → Prop -| Const {n : Int} (hLt : n < Int64.size) (hGe : n >= -Int64.size) : Eval (.Const n) (.ok <| Int64.mk ⟨n, hLt, hGe⟩) -| ConstErr_lt {n : Int} (h : ¬ n < Int64.size) : Eval (.Const n) (.error <| .OutOfBounds_Int64 n) -| ConstErr_ge {n : Int} (h : ¬ n >= -Int64.size) : Eval (.Const n) (.error <| .OutOfBounds_Int64 n) +inductive Eval : (Expr ctx ty) → Except EvalError ty.interp → Prop +| Const {n : Int} (hLt : n < Int64.size) (hGe : n >= -Int64.size) + : Eval (.Const n) (.ok <| Int64.mk ⟨n, hLt, hGe⟩) +| ConstErr_lt {n : Int} (h : ¬ n < Int64.size) + : Eval (.Const n) (.error <| .OutOfBounds_Int64 n) +| ConstErr_ge {n : Int} (h : ¬ n >= -Int64.size) + : Eval (.Const n) (.error <| .OutOfBounds_Int64 n) +| Var (x : Locals k ctx ty) (env : Env ctx) + : Eval (.Var x) (.ok <| env.lookup x) +| Lam (d : Eval e (.ok v)) + : Eval (.Lam e) (.ok <| fun _ => v) +| App (d₁ : Eval e₁ (.ok v₁)) (d₂ : Eval e₂ (.ok v₂)) + : Eval (.App (.Lam e₁) e₂) (.ok <| v₁) def EvalError.toString : EvalError → String | .OutOfBounds_Int64 n => s!"{n} is out of Int64 bounds, should be satisfied that -2{Nat.toSuperscriptString 63} ≤ n < 2{Nat.toSuperscriptString 63}" diff --git a/Tibi/Semantics/Env.lean b/Tibi/Semantics/Env.lean new file mode 100644 index 0000000..295e7a3 --- /dev/null +++ b/Tibi/Semantics/Env.lean @@ -0,0 +1,14 @@ +import Tibi.Syntax +import Tibi.Util + +namespace Tibi + +inductive Env : Vec Ty n → Type where +| nil : Env Vec.nil +| cons : Ty.interp a → Env ctx → Env (a :: ctx) + +infix:67 " :: " => Env.cons + +def Env.lookup : Locals i ctx ty → Env ctx → (Ty.cls ty ty).interp +| .stop, x :: _ => x +| .pop k, _ :: xs => xs.lookup k diff --git a/Tibi/Syntax/Expr.lean b/Tibi/Syntax/Expr.lean index f04d64e..e54b8e6 100644 --- a/Tibi/Syntax/Expr.lean +++ b/Tibi/Syntax/Expr.lean @@ -1,10 +1,55 @@ import Tibi.FinInt +import Tibi.Util namespace Tibi -inductive Expr -| Const : Int → Expr +inductive Ty where +| int +| fn (a b : Ty) +| cls (a b : Ty) -instance : ToString Expr where - toString - | .Const n => s!"" +@[reducible] +def Ty.interp : Ty → Type +| int => Int64 +| fn a b => a.interp → b.interp +| cls _ b => b.interp + +@[reducible] +def Ty.dom : Ty → Type +| int => Unit +| fn a _ => a.interp +| cls a _ => a.interp + +def Ty.toString : Ty → String +| int => "Int" +| fn a b => s!"{a.toString} -> {b.toString}" +| cls _ b => s!"{b.toString}" + +instance : ToString Ty where + toString := Ty.toString + +inductive Locals : Fin n → Tibi.Vec Ty n → Ty → Type where +| stop : Locals 0 (ty :: ctx) ty +| pop : Locals k ctx ty → Locals k.succ (u :: ctx) ty + +def Locals.idx : Locals n ctx ty → Fin n.succ +| stop => Fin.mk 0 (Fin.succ_pos _) +| pop k => k.idx.succ + +instance : ToString (Locals n ctx ty) where + toString x := s!"${x.idx}" + +inductive Expr : Vec Ty n → Ty → Type where +| Const : Int → Expr ctx .int +| Var : Locals i ctx ty → Expr ctx (.cls ty ty) +| Lam : Expr (dom :: ctx) (.cls dom ran) → Expr ctx (.fn dom ran) +| App : Expr ctx (.fn dom ran) → Expr ctx dom → Expr ctx ran + +def Expr.toString : Expr ctx ty → String +| Const n => s!"" +| Var x => s!"" +| Lam e => s!"" +| App e₁ e₂ => s!"" + +instance : ToString (Expr ctx ty) where + toString := Expr.toString diff --git a/Tibi/Top.lean b/Tibi/Top.lean index abab511..e159783 100644 --- a/Tibi/Top.lean +++ b/Tibi/Top.lean @@ -14,7 +14,7 @@ partial def repl (stream : IO.FS.Stream) (n : Nat := 0) : IO UInt32 := do | .ok (expr, []) => match expr.typeCheck with | .found t _ => - match expr.eval with + match expr.eval .nil () with | .found (.ok v) _ => IO.println s!"- : {t} = {v}" | .found (.error _) _ => panic! "TODO: prove that this branch cannot be reached (type-safe)" | .unknown => panic! "TODO: prove that this branch cannot be reached (type-safe)" @@ -37,7 +37,7 @@ def run (inStream : IO.FS.Stream) : IO ByteArray := | .some <| .error e => .throw e.toString ) >>= ( - fun (e : Option Expr) => + fun (e : Option (Expr .nil .int)) => match e with | .none => pure Wasm.empty | .some e => diff --git a/Tibi/Typing.lean b/Tibi/Typing.lean index a367b7e..01521c6 100644 --- a/Tibi/Typing.lean +++ b/Tibi/Typing.lean @@ -1,25 +1,52 @@ import Tibi.FinInt +import Tibi.Semantics import Tibi.Syntax import Tibi.Util namespace Tibi inductive Typ +| Var (idx : Nat) | Int64 +| Fn (a : Typ) (b : Typ) deriving DecidableEq def Typ.toString : Typ → String -| Int64 => "Int" +| Var idx => s!"α{idx}" +| Int64 => "Int" +| Fn a b => s!"{a.toString} -> {b.toString}" instance : ToString Typ where toString := Typ.toString -inductive HasType : Expr → Typ → Prop +def Ty.toTyp : Ty → Typ +| int => .Int64 +| fn a b => .Fn a.toTyp b.toTyp +| cls _ b => b.toTyp + +inductive HasType : Expr ctx ty → Typ → Prop | Int64 {n : Int} (hLt : n < Int64.size) (hGe : n ≥ -Int64.size) : HasType (.Const n) .Int64 +| Var {x : Locals i ctx ty} : HasType (.Var x) (Ty.cls ty ty).toTyp +| Lam (h : HasType e t) : HasType (.Lam e) (.Fn (.Var 0) t) +| App (hf : HasType f (.Fn dom ran)) (hv : HasType v dom) : HasType (.App f v) ran -def Expr.typeCheck : (e : Expr) → {{ t | HasType e t }} +def Expr.typeCheck : (e : Expr ctx ty) → {{ t | HasType e t }} | .Const n => if h : -Int64.size ≤ n ∧ n < Int64.size then .found .Int64 <| .Int64 h.right h.left else .unknown +| .Var _ => + .found _ .Var +| .Lam e => + match e.typeCheck with + | .found t h => .found (.Fn (.Var 0) t) <| .Lam h + | .unknown => .unknown +| .App f v => + match f.typeCheck, v.typeCheck with + | .found (.Fn a b) hf, .found a' hv => + if h : a = a' then + .found b <| .App hf (h ▸ hv) + else + .unknown + | _, _ => .unknown diff --git a/Tibi/Util.lean b/Tibi/Util.lean index 0c46d05..f088589 100644 --- a/Tibi/Util.lean +++ b/Tibi/Util.lean @@ -9,3 +9,9 @@ inductive Maybe (p : α → Prop) | found (a : α) : p a → Maybe p notation "{{ " x " | " p " }}" => Maybe (fun x => p) + +inductive Vec (α : Type u) : Nat → Type u +| nil : Vec α 0 +| cons : α → Vec α n → Vec α n.succ + +infixr:67 " :: " => Vec.cons From acd4f982aa547655d50e9e90ea0c1ed12f9024fb Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 1 Mar 2026 14:49:53 +0000 Subject: [PATCH 3/8] Fix Props/Compiler.lean exhaustive cases and use Typ.Fn.injEq in HasType.det Co-authored-by: nahcnuj <2093896+nahcnuj@users.noreply.github.com> --- Tibi/Props/Compiler.lean | 2 ++ Tibi/Props/Typing.lean | 4 +++- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/Tibi/Props/Compiler.lean b/Tibi/Props/Compiler.lean index 1559777..e38101e 100644 --- a/Tibi/Props/Compiler.lean +++ b/Tibi/Props/Compiler.lean @@ -16,3 +16,5 @@ theorem Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok -- Expr.compile_ok_o have : instrs = [.i64__const ⟨n, hLt, hGe⟩ ] := Except.ok.inj <| Eq.trans hc.symm this rw [this] exact .i64__const +| .Var, .Var _ _, hc => by simp [Expr.compile] at hc +| .App _ _, .App _ _, hc => by simp [Expr.compile] at hc diff --git a/Tibi/Props/Typing.lean b/Tibi/Props/Typing.lean index 89d2ce8..7841223 100644 --- a/Tibi/Props/Typing.lean +++ b/Tibi/Props/Typing.lean @@ -11,7 +11,9 @@ theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t | App _ _ ihf _ => cases h₂ with | App hf' _ => - exact (Typ.Fn.inj (ihf hf')).2 + have h := ihf hf' + simp only [Typ.Fn.injEq] at h + exact h.2 theorem Expr.typeCheck_correct : (ht : HasType e t) → e.typeCheck = .found t ht | .Int64 (n := n) hLt hGe => From 85630ab2837d7578723502fec0a14a008e3dcdbe Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 3 Mar 2026 23:56:35 +0000 Subject: [PATCH 4/8] Fix CI failures in Props/Typing.lean and Props/Compiler.lean Co-authored-by: nahcnuj <2093896+nahcnuj@users.noreply.github.com> --- Tibi/Props/Compiler.lean | 3 +-- Tibi/Props/Typing.lean | 5 ++--- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/Tibi/Props/Compiler.lean b/Tibi/Props/Compiler.lean index e38101e..8c53926 100644 --- a/Tibi/Props/Compiler.lean +++ b/Tibi/Props/Compiler.lean @@ -4,7 +4,7 @@ import Tibi.Wasm.Semantics namespace Tibi -theorem Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok -- Expr.compile_ok_of_has_type_of_eval +theorem Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok {e : Expr ctx .int} -- Expr.compile_ok_of_has_type_of_eval : HasType e _ty → Eval e (.ok v) → e.compile = .ok instrs → Wasm.Reduction { instrs := instrs ++ K, stack, store, framestate } @@ -16,5 +16,4 @@ theorem Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok -- Expr.compile_ok_o have : instrs = [.i64__const ⟨n, hLt, hGe⟩ ] := Except.ok.inj <| Eq.trans hc.symm this rw [this] exact .i64__const -| .Var, .Var _ _, hc => by simp [Expr.compile] at hc | .App _ _, .App _ _, hc => by simp [Expr.compile] at hc diff --git a/Tibi/Props/Typing.lean b/Tibi/Props/Typing.lean index 7841223..b4d2bce 100644 --- a/Tibi/Props/Typing.lean +++ b/Tibi/Props/Typing.lean @@ -20,14 +20,13 @@ theorem Expr.typeCheck_correct : (ht : HasType e t) → e.typeCheck = .found t h have := eq_true <| And.intro (ge_iff_le.mp hGe) hLt dite_cond_eq_true this | .Var => rfl -| .Lam h => +| .Lam h => by have ih := typeCheck_correct h simp only [Expr.typeCheck, ih] | .App hf hv => by have ihf := typeCheck_correct hf have ihv := typeCheck_correct hv - simp only [Expr.typeCheck, ihf, ihv] - exact dif_pos rfl + simp [Expr.typeCheck, ihf, ihv] theorem Expr.typeCheck_complete {e : Expr ctx ty} : e.typeCheck = .unknown → ¬ HasType e t From 3ed9b48a75f40b015aec21a873cbf96334bfd723 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 4 Mar 2026 00:04:08 +0000 Subject: [PATCH 5/8] Fix Props/Compiler.lean: move {e} into arrow chain so pattern can bind n Co-authored-by: nahcnuj <2093896+nahcnuj@users.noreply.github.com> --- Tibi/Props/Compiler.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Tibi/Props/Compiler.lean b/Tibi/Props/Compiler.lean index 8c53926..6dc2cc2 100644 --- a/Tibi/Props/Compiler.lean +++ b/Tibi/Props/Compiler.lean @@ -4,16 +4,16 @@ import Tibi.Wasm.Semantics namespace Tibi -theorem Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok {e : Expr ctx .int} -- Expr.compile_ok_of_has_type_of_eval -: HasType e _ty → Eval e (.ok v) → e.compile = .ok instrs +theorem Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok -- Expr.compile_ok_of_has_type_of_eval +: {e : Expr ctx .int} → HasType e _ty → Eval e (.ok v) → e.compile = .ok instrs → Wasm.Reduction { instrs := instrs ++ K, stack, store, framestate } { instrs := K, stack := .Value (.Num (.Int64 v)) :: stack, store, framestate } -| .Int64 hLt hGe, .Const _ _, hc => by +| .Const n, .Int64 hLt hGe, .Const _ _, hc => by have : (Expr.Const n).compile = .ok [.i64__const (Int64.mk ⟨n, hLt, hGe⟩)] := by -- dsimp [Expr.compile] apply dite_cond_eq_true <| eq_true <| And.intro hGe hLt have : instrs = [.i64__const ⟨n, hLt, hGe⟩ ] := Except.ok.inj <| Eq.trans hc.symm this rw [this] exact .i64__const -| .App _ _, .App _ _, hc => by simp [Expr.compile] at hc +| .App _ _, .App _ _, .App _ _, hc => by simp [Expr.compile] at hc From e8938c0c8d2b57ddcfd54a788372679d3609b28b Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 4 Mar 2026 00:09:36 +0000 Subject: [PATCH 6/8] Fix Props/Compiler.lean: use Eval.Const proofs for Int64 value, wildcard Eval in App case Co-authored-by: nahcnuj <2093896+nahcnuj@users.noreply.github.com> --- Tibi/Props/Compiler.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Tibi/Props/Compiler.lean b/Tibi/Props/Compiler.lean index 6dc2cc2..b2e19bd 100644 --- a/Tibi/Props/Compiler.lean +++ b/Tibi/Props/Compiler.lean @@ -9,11 +9,10 @@ theorem Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok -- Expr.compile_ok_o → Wasm.Reduction { instrs := instrs ++ K, stack, store, framestate } { instrs := K, stack := .Value (.Num (.Int64 v)) :: stack, store, framestate } -| .Const n, .Int64 hLt hGe, .Const _ _, hc => by +| .Const n, .Int64 _ _, .Const hLt hGe, hc => by have : (Expr.Const n).compile = .ok [.i64__const (Int64.mk ⟨n, hLt, hGe⟩)] := by - -- dsimp [Expr.compile] apply dite_cond_eq_true <| eq_true <| And.intro hGe hLt have : instrs = [.i64__const ⟨n, hLt, hGe⟩ ] := Except.ok.inj <| Eq.trans hc.symm this rw [this] exact .i64__const -| .App _ _, .App _ _, .App _ _, hc => by simp [Expr.compile] at hc +| .App _ _, _, _, hc => by simp [Expr.compile] at hc From aba9c0cf483ac114003927a06f6f81bc04d60594 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 4 Mar 2026 00:18:27 +0000 Subject: [PATCH 7/8] Fix Props/Compiler.lean: add Expr ctx .int type annotation so Lean can infer ctx Co-authored-by: nahcnuj <2093896+nahcnuj@users.noreply.github.com> --- Tibi/Props/Compiler.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Tibi/Props/Compiler.lean b/Tibi/Props/Compiler.lean index b2e19bd..7d90860 100644 --- a/Tibi/Props/Compiler.lean +++ b/Tibi/Props/Compiler.lean @@ -10,7 +10,7 @@ theorem Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok -- Expr.compile_ok_o { instrs := instrs ++ K, stack, store, framestate } { instrs := K, stack := .Value (.Num (.Int64 v)) :: stack, store, framestate } | .Const n, .Int64 _ _, .Const hLt hGe, hc => by - have : (Expr.Const n).compile = .ok [.i64__const (Int64.mk ⟨n, hLt, hGe⟩)] := by + have : (Expr.Const n : Expr ctx .int).compile = .ok [.i64__const (Int64.mk ⟨n, hLt, hGe⟩)] := by apply dite_cond_eq_true <| eq_true <| And.intro hGe hLt have : instrs = [.i64__const ⟨n, hLt, hGe⟩ ] := Except.ok.inj <| Eq.trans hc.symm this rw [this] From 329808fea0d9a5514c0be4a33e998b6f419d115e Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 6 Mar 2026 00:17:00 +0000 Subject: [PATCH 8/8] Add TODO comments to Compiler.lean and update README syntax with Var/Lam/App Co-authored-by: nahcnuj <2093896+nahcnuj@users.noreply.github.com> --- README.md | 25 ++++++++++++++++--------- Tibi/Compiler.lean | 4 ++-- 2 files changed, 18 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index f9634c0..2f347d6 100644 --- a/README.md +++ b/README.md @@ -71,18 +71,25 @@ You can see the returned integer in the `pre` element. ### Syntax ```ebnf - ws = { " " | "\n" | "\r" | "\t" } ; + ws = { " " | "\n" | "\r" | "\t" } ; -non-zero-digit = "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" ; - digit = "0" | non-zero-digit ; - nat-number = "0" - | non-zero-digit , { digit } ; + non-zero-digit = "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" ; + digit = "0" | non-zero-digit ; + nat-number = "0" + | non-zero-digit , { digit } ; - sign = "+" | "-" ; - int-number = sign , nat-number ; + sign = "+" | "-" ; + int-number = sign , nat-number ; - expr = nat-number , ws - | int-number , ws; + identifier = ( letter | "_" ) , { letter | digit | "_" } ; + letter = "a" | ... | "z" | "A" | ... | "Z" ; + + expr = nat-number , ws + | int-number , ws + | identifier , ws (* variable -- not yet implemented in parser *) + | "\" , identifier , "." , ws , expr , ws (* lambda abstraction -- not yet implemented in parser *) + | expr , expr , ws (* function application -- not yet implemented in parser *) + ; ```