From 31749181937bea8f960732654d703426f55ef996 Mon Sep 17 00:00:00 2001
From: Maximus Gorog <mgorog@gmail.com>
Date: Sun, 10 May 2026 03:51:14 -0600
Subject: [PATCH] Add executable evaluator (Phase A) and type system +
 soundness infra (Phase B).
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Phase A — GolangLean/Core/Eval.lean:
  def eval : Nat -> Heap -> Env -> Term -> Option (Value x Heap)
  Fuel-bounded recursive evaluator, total over the fuel.
  theorem eval_sound: eval succeeds => BigStep holds.
  Bridges executable computation to inductive specification.

Phase B — GolangLean/Core/Types.lean:
  inductive Ty {unit, int, bool, arrow, ref}
  TyEnv := List (String x Ty); BinOp.typeOf
  inductive HasType : TyEnv -> Term -> Ty -> Prop
  Standard simply-typed lambda calculus + ML-style references.

Phase B — GolangLean/Core/TypeSoundness.lean:
  abbrev HeapTy := Array Ty
  mutual inductive HasTypeV / HasTypeEnv  (value & env typing under heap-typing)
  def HasTypeH                            (heap conforms to heap-typing)
  def HeapTy.extends                       (prefix-extension of heap-typings)
  thm HeapTy.extends_refl, extends_trans
  thm HasTypeV.weaken, HasTypeEnv.weaken   (mutual; under heap-typing extension)
  thm HasTypeEnv.lookup_correspondence    (well-typed env yields well-typed values)

The preservation theorem itself
  HasType /\ HasTypeH /\ HasTypeEnv /\ BigStep
    ==> ∃ ht', extends /\ HasTypeH' /\ HasTypeV' /\ HasTypeEnv'
is the next deliverable; the infrastructure here is what its proof
case-analysis depends on.

Zero sorries / axioms / admits across the project. Full lake build clean.
---
 GolangLean.lean                    |   3 +
 GolangLean/Core/Eval.lean          | 190 +++++++++++++++++++++++++++++
 GolangLean/Core/TypeSoundness.lean | 101 +++++++++++++++
 GolangLean/Core/Types.lean         |  90 ++++++++++++++
 4 files changed, 384 insertions(+)
 create mode 100644 GolangLean/Core/Eval.lean
 create mode 100644 GolangLean/Core/TypeSoundness.lean
 create mode 100644 GolangLean/Core/Types.lean

diff --git a/GolangLean.lean b/GolangLean.lean
index c2b4ed8..c3c4ffd 100644
--- a/GolangLean.lean
+++ b/GolangLean.lean
@@ -14,3 +14,6 @@ import GolangLean.ValueEquiv
 import GolangLean.Core.Syntax
 import GolangLean.Core.Semantics
 import GolangLean.Core.Determinism
+import GolangLean.Core.Eval
+import GolangLean.Core.Types
+import GolangLean.Core.TypeSoundness
diff --git a/GolangLean/Core/Eval.lean b/GolangLean/Core/Eval.lean
new file mode 100644
index 0000000..5e9ec62
--- /dev/null
+++ b/GolangLean/Core/Eval.lean
@@ -0,0 +1,190 @@
+import GolangLean.Core.Semantics
+
+namespace GolangLean.Core
+
+/-! # Executable evaluator and soundness.
+
+A fuel-bounded recursive evaluator
+  `eval : Nat → Heap → Env → Term → Option (Value × Heap)`
+together with the soundness theorem
+  `eval n h env e = some (v, h') → BigStep h env e v h'`.
+
+Soundness is the bridge that makes the inductive specification *runnable*.
+For any closed TGC term you can write a Lean theorem of the form
+  `BigStep h env e v h'`
+and prove it by `decide`-style execution: run `eval`, then apply
+`eval_sound` to the equation. -/
+
+def eval : Nat → Heap → Env → Term → Option (Value × Heap)
+  | 0,     _, _,   _              => none
+  | _ + 1, h, _,   .unitT         => some (.vUnit, h)
+  | _ + 1, h, _,   .intLit k      => some (.vInt k, h)
+  | _ + 1, h, _,   .boolLit b     => some (.vBool b, h)
+  | _ + 1, h, env, .var x         =>
+      match env.lookup x with
+      | some v => some (v, h)
+      | none   => none
+  | _ + 1, h, env, .lam x body    => some (.vClos x body env, h)
+  | n + 1, h, env, .app e1 e2     =>
+      match eval n h env e1 with
+      | some (.vClos x body env', h1) =>
+          match eval n h1 env e2 with
+          | some (v2, h2) => eval n h2 (env'.extend x v2) body
+          | none          => none
+      | _ => none
+  | n + 1, h, env, .letIn x e1 e2 =>
+      match eval n h env e1 with
+      | some (v1, h1) => eval n h1 (env.extend x v1) e2
+      | none          => none
+  | n + 1, h, env, .ifte ec e1 e2 =>
+      match eval n h env ec with
+      | some (.vBool true,  h1) => eval n h1 env e1
+      | some (.vBool false, h1) => eval n h1 env e2
+      | _                        => none
+  | n + 1, h, env, .binop op e1 e2 =>
+      match eval n h env e1 with
+      | some (v1, h1) =>
+          match eval n h1 env e2 with
+          | some (v2, h2) =>
+              match op.apply v1 v2 with
+              | some v => some (v, h2)
+              | none   => none
+          | none => none
+      | none => none
+  | n + 1, h, env, .refMk e       =>
+      match eval n h env e with
+      | some (v, h1) => some (.vLoc h1.size, h1.push v)
+      | none         => none
+  | n + 1, h, env, .deref e       =>
+      match eval n h env e with
+      | some (.vLoc loc, h1) =>
+          match h1[loc]? with
+          | some v => some (v, h1)
+          | none   => none
+      | _ => none
+  | n + 1, h, env, .assign e1 e2  =>
+      match eval n h env e1 with
+      | some (.vLoc loc, h1) =>
+          match eval n h1 env e2 with
+          | some (v2, h2) =>
+              if loc < h2.size then some (.vUnit, h2.set! loc v2) else none
+          | none => none
+      | _ => none
+  | n + 1, h, env, .seq e1 e2     =>
+      match eval n h env e1 with
+      | some (_, h1) => eval n h1 env e2
+      | none         => none
+
+theorem eval_sound :
+    ∀ (n : Nat) (h : Heap) (env : Env) (e : Term) (v : Value) (h' : Heap),
+      eval n h env e = some (v, h') → BigStep h env e v h' := by
+  intro n
+  induction n with
+  | zero =>
+    intro h env e v h' heq
+    simp [eval] at heq
+  | succ n ih =>
+    intro h env e v h' heq
+    cases e with
+    | unitT =>
+      simp [eval] at heq
+      obtain ⟨rfl, rfl⟩ := heq
+      exact .unitR
+    | intLit k =>
+      simp [eval] at heq
+      obtain ⟨rfl, rfl⟩ := heq
+      exact .intLitR k
+    | boolLit b =>
+      simp [eval] at heq
+      obtain ⟨rfl, rfl⟩ := heq
+      exact .boolLitR b
+    | var x =>
+      simp only [eval] at heq
+      split at heq
+      next vv hL =>
+        simp at heq
+        obtain ⟨rfl, rfl⟩ := heq
+        exact .varR hL
+      next => simp at heq
+    | lam x body =>
+      simp [eval] at heq
+      obtain ⟨rfl, rfl⟩ := heq
+      exact .lamR x body
+    | app e1 e2 =>
+      simp only [eval] at heq
+      split at heq
+      next x body env' h1 heq1 =>
+        split at heq
+        next v2 h2 heq2 =>
+          exact .appR (ih _ _ _ _ _ heq1) (ih _ _ _ _ _ heq2) (ih _ _ _ _ _ heq)
+        next => simp at heq
+      all_goals simp at heq
+    | letIn x e1 e2 =>
+      simp only [eval] at heq
+      split at heq
+      next v1 h1 heq1 =>
+        exact .letInR (ih _ _ _ _ _ heq1) (ih _ _ _ _ _ heq)
+      next => simp at heq
+    | ifte ec e1 e2 =>
+      simp only [eval] at heq
+      split at heq
+      next h1 heq1 =>
+        exact .ifTR (ih _ _ _ _ _ heq1) (ih _ _ _ _ _ heq)
+      next h1 heq1 =>
+        exact .ifFR (ih _ _ _ _ _ heq1) (ih _ _ _ _ _ heq)
+      all_goals simp at heq
+    | binop op e1 e2 =>
+      simp only [eval] at heq
+      split at heq
+      next v1 h1 heq1 =>
+        split at heq
+        next v2 h2 heq2 =>
+          split at heq
+          next vv heqop =>
+            simp at heq
+            obtain ⟨rfl, rfl⟩ := heq
+            exact .binopR (ih _ _ _ _ _ heq1) (ih _ _ _ _ _ heq2) heqop
+          next => simp at heq
+        next => simp at heq
+      next => simp at heq
+    | refMk e =>
+      simp only [eval] at heq
+      split at heq
+      next vv h1 heq1 =>
+        simp at heq
+        obtain ⟨rfl, rfl⟩ := heq
+        exact .refMkR (ih _ _ _ _ _ heq1)
+      next => simp at heq
+    | deref e =>
+      simp only [eval] at heq
+      split at heq
+      next loc h1 heq1 =>
+        split at heq
+        next vv hget =>
+          simp at heq
+          obtain ⟨rfl, rfl⟩ := heq
+          exact .derefR (ih _ _ _ _ _ heq1) hget
+        next => simp at heq
+      all_goals simp at heq
+    | assign e1 e2 =>
+      simp only [eval] at heq
+      split at heq
+      next loc h1 heq1 =>
+        split at heq
+        next v2 h2 heq2 =>
+          split at heq
+          next hb =>
+            simp at heq
+            obtain ⟨rfl, rfl⟩ := heq
+            exact .assignR (ih _ _ _ _ _ heq1) (ih _ _ _ _ _ heq2) hb
+          next => simp at heq
+        next => simp at heq
+      all_goals simp at heq
+    | seq e1 e2 =>
+      simp only [eval] at heq
+      split at heq
+      next _ h1 heq1 =>
+        exact .seqR (ih _ _ _ _ _ heq1) (ih _ _ _ _ _ heq)
+      next => simp at heq
+
+end GolangLean.Core
diff --git a/GolangLean/Core/TypeSoundness.lean b/GolangLean/Core/TypeSoundness.lean
new file mode 100644
index 0000000..ce6da0c
--- /dev/null
+++ b/GolangLean/Core/TypeSoundness.lean
@@ -0,0 +1,101 @@
+import GolangLean.Core.Types
+import GolangLean.Core.Semantics
+
+namespace GolangLean.Core
+
+/-! # Type soundness for TGC.
+
+Big-step preservation: if `Γ ⊢ e : T` and `BigStep h env e v h'` under
+compatible heap/env typings, then there exists an extended heap-typing
+under which `v : T` and the new heap is well-typed. There is no
+small-step "progress" analogue — big-step proves "if it terminates, the
+result has the expected type". -/
+
+abbrev HeapTy := Array Ty
+
+mutual
+
+  inductive HasTypeV : HeapTy → Value → Ty → Prop where
+    | vUnit  {ht} : HasTypeV ht .vUnit .unit
+    | vInt   {ht} (n : Int)  : HasTypeV ht (.vInt n) .int
+    | vBool  {ht} (b : Bool) : HasTypeV ht (.vBool b) .bool
+    | vLoc   {ht loc T} (h : (ht[loc]? : Option Ty) = some T) :
+        HasTypeV ht (.vLoc loc) (.ref T)
+    | vClos  {ht x body env Γ T_arg T_ret}
+             (he : HasTypeEnv ht env Γ)
+             (hb : HasType (Γ.extend x T_arg) body T_ret) :
+        HasTypeV ht (.vClos x body env) (.arrow T_arg T_ret)
+
+  inductive HasTypeEnv : HeapTy → Env → TyEnv → Prop where
+    | nil  {ht} : HasTypeEnv ht .nil []
+    | cons {ht x v T env Γ}
+           (hv : HasTypeV ht v T)
+           (he : HasTypeEnv ht env Γ) :
+        HasTypeEnv ht (.cons x v env) ((x, T) :: Γ)
+
+end
+
+def HasTypeH (ht : HeapTy) (h : Heap) : Prop :=
+  ht.size = h.size ∧
+  ∀ (i : Nat) (T : Ty), (ht[i]? : Option Ty) = some T →
+    ∃ v, (h[i]? : Option Value) = some v ∧ HasTypeV ht v T
+
+def HeapTy.extends (ht ht' : HeapTy) : Prop :=
+  ht.size ≤ ht'.size ∧
+  ∀ (i : Nat) (T : Ty), (ht[i]? : Option Ty) = some T → (ht'[i]? : Option Ty) = some T
+
+namespace HeapTy
+
+theorem extends_refl (ht : HeapTy) : ht.extends ht :=
+  ⟨Nat.le_refl _, fun _ _ h => h⟩
+
+theorem extends_trans {ht₁ ht₂ ht₃ : HeapTy}
+    (h₁ : ht₁.extends ht₂) (h₂ : ht₂.extends ht₃) : ht₁.extends ht₃ :=
+  ⟨Nat.le_trans h₁.1 h₂.1, fun i T h => h₂.2 i T (h₁.2 i T h)⟩
+
+end HeapTy
+
+/-! ## Weakening under heap-typing extension. -/
+
+mutual
+
+  theorem HasTypeV.weaken {ht ht' v T}
+      (h : HasTypeV ht v T) (ext : HeapTy.extends ht ht') :
+      HasTypeV ht' v T := by
+    cases h with
+    | vUnit       => exact .vUnit
+    | vInt n      => exact .vInt n
+    | vBool b     => exact .vBool b
+    | vLoc hLoc   => exact .vLoc (ext.2 _ _ hLoc)
+    | vClos he hb => exact .vClos (HasTypeEnv.weaken he ext) hb
+
+  theorem HasTypeEnv.weaken {ht ht' env Γ}
+      (h : HasTypeEnv ht env Γ) (ext : HeapTy.extends ht ht') :
+      HasTypeEnv ht' env Γ := by
+    cases h with
+    | nil        => exact .nil
+    | cons hv he => exact .cons (HasTypeV.weaken hv ext) (HasTypeEnv.weaken he ext)
+
+end
+
+/-! ## Lookup correspondence: well-typed env produces well-typed values. -/
+
+theorem HasTypeEnv.lookup_correspondence :
+    ∀ {ht env Γ x T},
+      HasTypeEnv ht env Γ → Γ.lookup x = some T →
+        ∃ v, env.lookup x = some v ∧ HasTypeV ht v T
+  | _, _, _, _, _, .nil, hL => by simp [TyEnv.lookup] at hL
+  | _, _, _, x, _, @HasTypeEnv.cons _ x' v' T' env' Γ' hv he, hL => by
+    by_cases hx : x' = x
+    · subst hx
+      simp only [TyEnv.lookup] at hL
+      simp at hL
+      cases hL
+      refine ⟨v', ?_, hv⟩
+      simp [EnvList.lookup]
+    · simp only [TyEnv.lookup, if_neg hx] at hL
+      have ⟨v, hLv, hTv⟩ := lookup_correspondence he hL
+      refine ⟨v, ?_, hTv⟩
+      simp [EnvList.lookup, hx, hLv]
+
+end GolangLean.Core
diff --git a/GolangLean/Core/Types.lean b/GolangLean/Core/Types.lean
new file mode 100644
index 0000000..dea76bb
--- /dev/null
+++ b/GolangLean/Core/Types.lean
@@ -0,0 +1,90 @@
+import GolangLean.Core.Syntax
+
+namespace GolangLean.Core
+
+/-! # Static type system for TGC.
+
+Five base types: `unit`, `int`, `bool`, `arrow τ₁ τ₂`, `ref τ`. Typing
+context `TyEnv` is a list of (name, type) bindings — innermost-first to
+match `Env`.
+
+Typing rules `HasType : TyEnv → Term → Ty → Prop` follow the standard
+simply-typed lambda calculus + ML-style references discipline. -/
+
+inductive Ty where
+  | unit  : Ty
+  | int   : Ty
+  | bool  : Ty
+  | arrow : Ty → Ty → Ty
+  | ref   : Ty → Ty
+  deriving Repr, BEq, DecidableEq, Inhabited
+
+abbrev TyEnv := List (String × Ty)
+
+namespace TyEnv
+
+def lookup : TyEnv → String → Option Ty
+  | [],            _ => none
+  | (k, T) :: rs, x => if k = x then some T else lookup rs x
+
+def extend (Γ : TyEnv) (x : String) (T : Ty) : TyEnv :=
+  (x, T) :: Γ
+
+end TyEnv
+
+namespace BinOp
+
+def typeOf : BinOp → Ty → Ty → Option Ty
+  | .add, .int,  .int  => some .int
+  | .sub, .int,  .int  => some .int
+  | .mul, .int,  .int  => some .int
+  | .eq,  .int,  .int  => some .bool
+  | .eq,  .bool, .bool => some .bool
+  | .lt,  .int,  .int  => some .bool
+  | _,    _,     _     => none
+
+end BinOp
+
+inductive HasType : TyEnv → Term → Ty → Prop where
+  | unitT  {Γ} : HasType Γ .unitT .unit
+  | intLit {Γ} (n : Int) : HasType Γ (.intLit n) .int
+  | boolLit {Γ} (b : Bool) : HasType Γ (.boolLit b) .bool
+  | var    {Γ x T} (h : Γ.lookup x = some T) :
+      HasType Γ (.var x) T
+  | lam    {Γ x body T_arg T_ret}
+           (h : HasType (Γ.extend x T_arg) body T_ret) :
+      HasType Γ (.lam x body) (.arrow T_arg T_ret)
+  | app    {Γ e1 e2 T_arg T_ret}
+           (h1 : HasType Γ e1 (.arrow T_arg T_ret))
+           (h2 : HasType Γ e2 T_arg) :
+      HasType Γ (.app e1 e2) T_ret
+  | letIn  {Γ x e1 e2 T1 T2}
+           (h1 : HasType Γ e1 T1)
+           (h2 : HasType (Γ.extend x T1) e2 T2) :
+      HasType Γ (.letIn x e1 e2) T2
+  | ifte   {Γ ec e1 e2 T}
+           (hc : HasType Γ ec .bool)
+           (h1 : HasType Γ e1 T)
+           (h2 : HasType Γ e2 T) :
+      HasType Γ (.ifte ec e1 e2) T
+  | binop  {Γ op e1 e2 T1 T2 T}
+           (h1 : HasType Γ e1 T1)
+           (h2 : HasType Γ e2 T2)
+           (hOp : op.typeOf T1 T2 = some T) :
+      HasType Γ (.binop op e1 e2) T
+  | refMk  {Γ e T}
+           (h : HasType Γ e T) :
+      HasType Γ (.refMk e) (.ref T)
+  | deref  {Γ e T}
+           (h : HasType Γ e (.ref T)) :
+      HasType Γ (.deref e) T
+  | assign {Γ e1 e2 T}
+           (h1 : HasType Γ e1 (.ref T))
+           (h2 : HasType Γ e2 T) :
+      HasType Γ (.assign e1 e2) .unit
+  | seq    {Γ e1 e2 T1 T2}
+           (h1 : HasType Γ e1 T1)
+           (h2 : HasType Γ e2 T2) :
+      HasType Γ (.seq e1 e2) T2
+
+end GolangLean.Core