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.
This commit is contained in:
Maximus Gorog
parent
2173e196fe
commit
878a84e072
4 changed files with 259 additions and 0 deletions
|
|
@ -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
|
||||
|
|
|
|||
107
GolangLean/Core/Determinism.lean
Normal file
107
GolangLean/Core/Determinism.lean
Normal file
|
|
@ -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
|
||||
113
GolangLean/Core/Semantics.lean
Normal file
113
GolangLean/Core/Semantics.lean
Normal file
|
|
@ -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
|
||||
36
GolangLean/Core/Syntax.lean
Normal file
36
GolangLean/Core/Syntax.lean
Normal file
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue