From 878a84e072dab68f6a4b594f94f4958d6f2f5bcc Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Sun, 10 May 2026 02:23:58 -0600 Subject: [PATCH] Add Tiny Go Core (TGC): kernel calculus with proven determinism. GolangLean/Core/ holds a small calculus that surface Go is intended to desugar into. Three files: Syntax.lean - Term, BinOp; thirteen syntactic forms covering let-binding, lambda, application, references (Go's & / *), conditionals, sequencing. Semantics.lean - Value, EnvList, Heap, BinOp.apply, BigStep relation. Heap is Array Value; references are indices. Closures capture EnvList lexically, as in Go. Fourteen big-step constructors, one per syntactic form (with ifte split into ifTR / ifFR). Determinism.lean - theorem BigStep.deterministic: BigStep h env e v1 h1 -> BigStep h env e v2 h2 -> v1 = v2 /\ h1 = h2 Proof by induction on the first derivation, case analysis on the second. The ifTR/ifFR cross-cases close by contradiction via Bool.noConfusion. No sorries, no axioms, no admits. The kernel is small enough to extend compositionally: each new syntactic form adds one constructor and one case to each proof. Type system and concurrency layer come later. Strategic note: this kernel is shaped so the same construction will work for any sequential calculus. When octive-lean grows a parallel Tiny Octave Core, the determinism proof's structure will line up case-for-case where the languages share constructors. That alignment is the seed of the cross-language layer. --- GolangLean.lean | 3 + GolangLean/Core/Determinism.lean | 107 +++++++++++++++++++++++++++++ GolangLean/Core/Semantics.lean | 113 +++++++++++++++++++++++++++++++ GolangLean/Core/Syntax.lean | 36 ++++++++++ 4 files changed, 259 insertions(+) create mode 100644 GolangLean/Core/Determinism.lean create mode 100644 GolangLean/Core/Semantics.lean create mode 100644 GolangLean/Core/Syntax.lean diff --git a/GolangLean.lean b/GolangLean.lean index aaf57ef..c2b4ed8 100644 --- a/GolangLean.lean +++ b/GolangLean.lean @@ -11,3 +11,6 @@ import GolangLean.REPL import GolangLean.PureEval import GolangLean.BigStep import GolangLean.ValueEquiv +import GolangLean.Core.Syntax +import GolangLean.Core.Semantics +import GolangLean.Core.Determinism diff --git a/GolangLean/Core/Determinism.lean b/GolangLean/Core/Determinism.lean new file mode 100644 index 0000000..083ea24 --- /dev/null +++ b/GolangLean/Core/Determinism.lean @@ -0,0 +1,107 @@ +import GolangLean.Core.Semantics + +namespace GolangLean.Core + +/-! # Determinism of TGC big-step. + + `BigStep h env e v₁ h₁ → BigStep h env e v₂ h₂ → v₁ = v₂ ∧ h₁ = h₂` + +By induction on the first derivation, with case analysis on the second. +For each pair of constructors, either the term-shape forces them to agree +(so we apply the IHs to the sub-derivations) or, in the `ifte` case where +two rules share a term shape, an IH on the condition gives a contradictory +boolean. -/ + +theorem BigStep.deterministic + {h : Heap} {env : Env} {e : Term} {v₁ v₂ : Value} {h₁ h₂ : Heap} + (D₁ : BigStep h env e v₁ h₁) (D₂ : BigStep h env e v₂ h₂) : + v₁ = v₂ ∧ h₁ = h₂ := by + induction D₁ generalizing v₂ h₂ with + | unitR => + cases D₂; exact ⟨rfl, rfl⟩ + | intLitR n => + cases D₂; exact ⟨rfl, rfl⟩ + | boolLitR b => + cases D₂; exact ⟨rfl, rfl⟩ + | varR hLook => + cases D₂ with + | varR hLook' => + have heq := hLook.symm.trans hLook' + exact ⟨Option.some.inj heq, rfl⟩ + | lamR x body => + cases D₂; exact ⟨rfl, rfl⟩ + | appR _ _ _ ih1 ih2 ihb => + cases D₂ with + | appR D1' D2' Db' => + have ⟨hClos, hH1⟩ := ih1 D1' + injection hClos with hx hbody henv + subst hx; subst hbody; subst henv; subst hH1 + have ⟨hArg, hH2⟩ := ih2 D2' + subst hArg; subst hH2 + exact ihb Db' + | letInR _ _ ih1 ih2 => + cases D₂ with + | letInR D1' D2' => + have ⟨hv1, hH1⟩ := ih1 D1' + subst hv1; subst hH1 + exact ih2 D2' + | ifTR _ _ ihc iht => + cases D₂ with + | ifTR Dc' Dt' => + have ⟨_, hH1⟩ := ihc Dc' + subst hH1 + exact iht Dt' + | ifFR Dc' _ => + have ⟨hb, _⟩ := ihc Dc' + injection hb with hb_eq + exact Bool.noConfusion hb_eq + | ifFR _ _ ihc ihf => + cases D₂ with + | ifTR Dc' _ => + have ⟨hb, _⟩ := ihc Dc' + injection hb with hb_eq + exact Bool.noConfusion hb_eq + | ifFR Dc' Df' => + have ⟨_, hH1⟩ := ihc Dc' + subst hH1 + exact ihf Df' + | binopR _ _ Hop ih1 ih2 => + cases D₂ with + | binopR D1' D2' Hop' => + have ⟨hv1, hH1⟩ := ih1 D1' + subst hv1; subst hH1 + have ⟨hv2, hH2⟩ := ih2 D2' + subst hv2; subst hH2 + have heq := Hop.symm.trans Hop' + exact ⟨Option.some.inj heq, rfl⟩ + | refMkR _ ih => + cases D₂ with + | refMkR D' => + have ⟨hv, hH⟩ := ih D' + subst hv; subst hH + exact ⟨rfl, rfl⟩ + | derefR _ Hget ih => + cases D₂ with + | derefR D' Hget' => + have ⟨hloc, hH⟩ := ih D' + injection hloc with hloceq + subst hloceq; subst hH + have heq := Hget.symm.trans Hget' + exact ⟨Option.some.inj heq, rfl⟩ + | assignR _ _ _ ih1 ih2 => + cases D₂ with + | assignR D1' D2' _ => + have ⟨hloc, hH1⟩ := ih1 D1' + injection hloc with hloceq + subst hloceq; subst hH1 + have ⟨hv, hH2⟩ := ih2 D2' + subst hv; subst hH2 + exact ⟨rfl, rfl⟩ + | seqR _ _ ih1 ih2 => + cases D₂ with + | seqR D1' D2' => + have ⟨_, hH1⟩ := ih1 D1' + subst hH1 + exact ih2 D2' + +end GolangLean.Core diff --git a/GolangLean/Core/Semantics.lean b/GolangLean/Core/Semantics.lean new file mode 100644 index 0000000..701d93c --- /dev/null +++ b/GolangLean/Core/Semantics.lean @@ -0,0 +1,113 @@ +import GolangLean.Core.Syntax + +namespace GolangLean.Core + +/-! # Big-step operational semantics for Tiny Go Core. + +State is `Heap × Env`. The heap is an `Array Value`; references are +indices. Env is a list of (name, value) bindings — innermost shadowing +outermost. Closures capture the env at the point of `lam`-evaluation +(lexical scope, as in Go). + +The relation is + + BigStep h env e v h' + +read "starting from heap `h` and env `env`, term `e` evaluates to value +`v` and produces heap `h'`". One inductive constructor per syntactic +form. Every premise either appeals to `BigStep` recursively or to a +total side-condition (lookup, binop application, bounds). -/ + +mutual + + inductive Value where + | vUnit : Value + | vInt : Int → Value + | vBool : Bool → Value + | vClos : String → Term → EnvList → Value + | vLoc : Nat → Value + + inductive EnvList where + | nil : EnvList + | cons : String → Value → EnvList → EnvList + +end + +abbrev Env := EnvList +abbrev Heap := Array Value + +namespace EnvList + +def lookup : EnvList → String → Option Value + | .nil, _ => none + | .cons k v r, x => if k = x then some v else lookup r x + +def extend (env : EnvList) (x : String) (v : Value) : EnvList := + .cons x v env + +end EnvList + +namespace BinOp + +def apply : BinOp → Value → Value → Option Value + | .add, .vInt a, .vInt b => some (.vInt (a + b)) + | .sub, .vInt a, .vInt b => some (.vInt (a - b)) + | .mul, .vInt a, .vInt b => some (.vInt (a * b)) + | .eq, .vInt a, .vInt b => some (.vBool (a == b)) + | .eq, .vBool a, .vBool b => some (.vBool (a == b)) + | .lt, .vInt a, .vInt b => some (.vBool (a < b)) + | _, _, _ => none + +end BinOp + +inductive BigStep : Heap → Env → Term → Value → Heap → Prop where + | unitR {h env} : + BigStep h env .unitT .vUnit h + | intLitR {h env} (n : Int) : + BigStep h env (.intLit n) (.vInt n) h + | boolLitR {h env} (b : Bool) : + BigStep h env (.boolLit b) (.vBool b) h + | varR {h env x v} (hLook : env.lookup x = some v) : + BigStep h env (.var x) v h + | lamR {h env} (x : String) (body : Term) : + BigStep h env (.lam x body) (.vClos x body env) h + | appR {h env e1 e2 x body env' v_arg v h1 h2 h3} + (D1 : BigStep h env e1 (.vClos x body env') h1) + (D2 : BigStep h1 env e2 v_arg h2) + (Db : BigStep h2 (env'.extend x v_arg) body v h3) : + BigStep h env (.app e1 e2) v h3 + | letInR {h env x e1 e2 v1 v2 h1 h2} + (D1 : BigStep h env e1 v1 h1) + (D2 : BigStep h1 (env.extend x v1) e2 v2 h2) : + BigStep h env (.letIn x e1 e2) v2 h2 + | ifTR {h env e e1 e2 v h1 h2} + (Dc : BigStep h env e (.vBool true) h1) + (Dt : BigStep h1 env e1 v h2) : + BigStep h env (.ifte e e1 e2) v h2 + | ifFR {h env e e1 e2 v h1 h2} + (Dc : BigStep h env e (.vBool false) h1) + (Df : BigStep h1 env e2 v h2) : + BigStep h env (.ifte e e1 e2) v h2 + | binopR {h env op e1 e2 v1 v2 v h1 h2} + (D1 : BigStep h env e1 v1 h1) + (D2 : BigStep h1 env e2 v2 h2) + (Hop : op.apply v1 v2 = some v) : + BigStep h env (.binop op e1 e2) v h2 + | refMkR {h env e v h1} + (D : BigStep h env e v h1) : + BigStep h env (.refMk e) (.vLoc h1.size) (h1.push v) + | derefR {h env e loc v h1} + (D : BigStep h env e (.vLoc loc) h1) + (Hget : h1[loc]? = some v) : + BigStep h env (.deref e) v h1 + | assignR {h env e1 e2 loc v h1 h2} + (D1 : BigStep h env e1 (.vLoc loc) h1) + (D2 : BigStep h1 env e2 v h2) + (Hin : loc < h2.size) : + BigStep h env (.assign e1 e2) .vUnit (h2.set! loc v) + | seqR {h env e1 e2 v1 v2 h1 h2} + (D1 : BigStep h env e1 v1 h1) + (D2 : BigStep h1 env e2 v2 h2) : + BigStep h env (.seq e1 e2) v2 h2 + +end GolangLean.Core diff --git a/GolangLean/Core/Syntax.lean b/GolangLean/Core/Syntax.lean new file mode 100644 index 0000000..b78dcf8 --- /dev/null +++ b/GolangLean/Core/Syntax.lean @@ -0,0 +1,36 @@ +namespace GolangLean.Core + +/-! # Tiny Go Core (TGC) — abstract syntax. + +A small calculus that captures the *essential computation* of Go's +sequential fragment: variables, functions, mutable references (Go's `&`/`*`), +sequencing, and conditionals. Everything in surface Go is intended to +desugar into this kernel. + +What is *not* here: types (introduced in a later module), goroutines, +channels, structs, slices, methods, interfaces. The point of starting tiny +is that every theorem we prove about TGC carries over once those +extensions are added compositionally. -/ + +inductive BinOp where + | add | sub | mul + | eq | lt + deriving Repr, BEq, DecidableEq, Inhabited + +inductive Term where + | unitT : Term + | intLit : Int → Term + | boolLit : Bool → Term + | var : String → Term + | lam : String → Term → Term -- λ x. e + | app : Term → Term → Term + | letIn : String → Term → Term → Term -- let x = e₁ in e₂ + | ifte : Term → Term → Term → Term + | binop : BinOp → Term → Term → Term + | refMk : Term → Term -- &e (allocate) + | deref : Term → Term -- *e (read) + | assign : Term → Term → Term -- *p = e + | seq : Term → Term → Term + deriving Repr, Inhabited + +end GolangLean.Core