EVM Compiler

Main.lean

@@ -1,10 +1,4 @@
-import Yatima.Cli.ContAddrCmd
-import Yatima.Cli.TypecheckCmd
-import Yatima.Cli.CodeGenCmd
-import Yatima.Cli.ProveCmd
-import Yatima.Cli.VerifyCmd
-import Yatima.Cli.IpfsCmd
-import Yatima.Cli.PrintPrimsCmd
+import Yatima
 
 opaque VERSION : String :=
   s!"{Lean.versionString}|0.0.1"

Yatima.lean

@@ -31,6 +31,8 @@ import Yatima.CodeGen.Preloads
 import Yatima.CodeGen.PrettyPrint
 import Yatima.CodeGen.Simp
 import Yatima.CodeGen.Test
+import Yatima.Compiler.Yul
+import Yatima.Compiler.Grin
 import Yatima.ContAddr.ContAddr
 import Yatima.ContAddr.ContAddrError
 import Yatima.ContAddr.ContAddrM

Yatima/Compiler/Compiler.lean

@@ -0,0 +1,84 @@
+import Yatima.Compiler.GrinM
+import Yatima.Compiler.Debug
+import Lean.Expr
+open Lean.Compiler.LCNF
+
+def Lean.FVarId.toVar (id : Lean.FVarId) : Yatima.Grin.Var := .mk id.name
+
+namespace Yatima.Grin
+
+def mkFreshVar : GrinM Var := do
+  pure ⟨← Lean.mkFreshId⟩
+
+def paramsToVars (params : Array Param) : List Var :=
+  params.toList.map (fun param => param.fvarId.toVar)
+
+def fetch? (id : Lean.FVarId) : GrinM SExpr := do
+  match ← varKind id with
+  | .pointer => pure $ .fetch id.toVar .none
+  | .basic => pure $ svar id.toVar
+
+def applyArgs (fnc : Var) : (args : List Arg) → GrinM Expr
+| [] => pure $ .ret $ svar fnc
+| .erased :: args => applyArgs fnc args
+| .type _ :: args => applyArgs fnc args
+| .fvar id :: args => do
+  let apply := .apply fnc (.var id.toVar)
+  let newVar ← mkFreshVar
+  let rest ← applyArgs newVar args
+  pure $ .seq apply (.svar newVar) rest
+
+mutual
+partial def PScheme : Alt → GrinM (CPat × Expr)
+| .default code => do
+  let expr ← RScheme code
+  pure (.default, expr)
+| .alt ctor params code  => do
+  let args := paramsToVars params
+  let tag := .C ⟨ ctor ⟩
+  let expr ← RScheme code
+  pure (.ctag tag args, expr)
+
+partial def RScheme : Code → GrinM Expr
+| .let decl k => match decl.value with
+  | .erased => RScheme k
+  | .value val => do
+    pure $ .ret $ slit val
+  | .proj _ idx struct => do
+    let structPtr := struct.toVar
+    let proj := .fetch structPtr (some idx)
+    pure $ .ret proj
+  | .const _name _ _args => throw "TODO"
+  | .fvar fnc args => do
+    let fncVal ← fetch? fnc
+    let newVar ← mkFreshVar
+    pure $ .seq fncVal (.svar newVar) (← applyArgs newVar args.toList)
+| .cases case => do
+  let some patExprs := NEList.nonEmpty (← case.alts.toList.mapM PScheme)
+    | throw "Empty pattern"
+  -- Since every variable is initially strict, we don't need to eval before
+  let caseVal ← fetch? case.discr
+  let newVar ← mkFreshVar
+  let caseExpr := .case (.sval $ .var newVar) patExprs
+  pure $ .seq caseVal (.svar newVar) caseExpr
+  -- pure expr
+| .return fvarId => do
+  -- In the lazy case, a return is a call to eval, but since we chose strict semantics this
+  -- will either be a `fetch` or `unit` instruction depending on whether the variable is a
+  -- pointer or basic value
+  pure $ .ret $ ← fetch? fvarId
+| .fun _decl _k => throw "Should not find function definition here (?)"
+-- We need to figure out a way to implement join points
+| .jp _decl _k => throw "TODO"
+| .jmp _fvarId _args => throw "TODO"
+| .unreach _type => throw "Unreach found"
+end
+
+def compileDeclaration (decl : Decl) : GrinM Binding := do
+  let defn := ⟨decl.name⟩
+  let args := paramsToVars decl.params
+  let body ← RScheme decl.value
+  let binding := { defn, args, body }
+  pure binding
+
+end Yatima.Grin

Yatima/Compiler/Debug.lean

@@ -0,0 +1,59 @@
+import Lean.Compiler.LCNF
+open Lean.Compiler.LCNF
+
+namespace Lean.Compiler.LCNF
+
+instance : ToString FVarId where
+  toString x := toString x.name
+
+instance : ToString Param where
+  toString x := s!"{x.fvarId}"
+
+instance [ToString K] : ToString (AltCore K) where
+  toString
+    | .alt ctor params k => s!"{ctor} {params} => {k}"
+    | .default k => s!"_ => {k}"
+
+instance : ToString LitValue where
+  toString
+  | .natVal x => s!"{x}"
+  | .strVal x => s!"\"{x}\""
+
+instance : ToString Arg where
+  toString
+  | .erased => "ε"
+  | .type .. => "τ"
+  | .fvar id => s!"{id}"
+
+instance : ToString LetValue where
+  toString
+    | .value lit => s!"{lit}"
+    | .erased .. => "ε"
+    | .proj _ idx struct => s!"(π {idx} {struct})"
+    | .const cnst _ args => s!"(const {cnst} {args})"
+    | .fvar id args => s!"(fvar {id} {args})"
+
+instance : ToString LetDecl where
+  toString decl := s!"{decl.fvarId} := {decl.value}"
+
+instance [ToString K] : ToString (FunDeclCore K) where
+  toString decl := s!"{decl.fvarId} {decl.params} := {decl.value}"
+
+instance [ToString K] : ToString (CasesCore K) where
+  toString cases := s!"{cases.discr} {cases.alts}"
+
+partial def Code.toString (code : Code) : String :=
+  let _ : ToString Code := ⟨toString⟩
+  match code with
+  | .let decl k => s!"(let {decl} in {k})"
+  | .fun decl k => s!"(fun {decl} in {k})"
+  | .jp decl k => s!"(jp {decl} in {k})"
+  | .jmp id args => s!"(jmp {id} {args})"
+  | .cases case => s!"(match {case})"
+  | .return id => s!"(return {id.name})"
+  | .unreach _ => "unreach"
+
+instance : ToString Code where
+  toString code := code.toString
+
+end Lean.Compiler.LCNF

Yatima/Compiler/Grin.lean

@@ -0,0 +1,85 @@
+import Lean.Expr
+import Lean.Compiler.LCNF
+import YatimaStdLib.NonEmpty
+
+open Lean.Compiler.LCNF
+
+-- Based on https://nbviewer.org/github/grin-compiler/grin/blob/master/papers/boquist.pdf
+namespace Yatima.Grin
+
+/-- Var represents a variable binding, such as in a function definition in a pattern -/
+structure Var where
+  data : Lean.Name
+/-- Id represents a known definition, such as a function or constructor -/
+structure Id where
+  data : Lean.Name
+/-- VarKind tells us whether a variable is a pointer or a basic value -/
+inductive VarKind
+| pointer
+| basic
+
+inductive Tag where
+-- Suspended full applications
+| F : Id → Tag
+-- Partial applications
+| P : Id → Nat → Tag
+-- Saturated constructors
+| C : Id → Tag
+
+abbrev Literal := LitValue
+
+inductive SVal where
+  | lit : Literal → SVal
+  | var : Var → SVal
+
+inductive Val where
+  | ctag  : Tag → List SVal → Val
+  | stag  : Tag → Val
+  | empty : Val
+  | sval  : SVal → Val
+
+inductive CPat where
+  -- Complete tag pattern
+  | ctag : Tag → List Var → CPat
+  -- Single tag pattern
+  | stag : Tag → CPat
+  -- Default case
+  | default : CPat
+  | lit  : Literal → CPat
+
+inductive LPat where
+  | ctag  : Tag → List SVal → LPat
+  | cvar  : Var → List SVal → LPat
+  | stag  : Tag → LPat
+  | svar  : Var → LPat
+
+inductive SExpr where
+  | unit   : Val → SExpr
+  | store  : Val → SExpr
+  | fetch  : Var → Option Nat → SExpr
+  | update : Var → Val → SExpr
+  -- Known function call
+  | call   : Id → NEList SVal → SExpr
+  -- Evaluation of unknown expression
+  | eval   : Var → SExpr
+  -- Application of unknown function to a list of arguments
+  | apply  : Var → SVal → SExpr
+
+inductive Expr where
+  | ret  : SExpr → Expr
+  | seq  : SExpr → LPat → Expr → Expr
+  | join : Expr → LPat → Expr → Expr
+  | case : Val → NEList (CPat × Expr) → Expr
+
+structure Binding where
+  defn : Id
+  args : List Var
+  body : Expr
+
+abbrev Prog := NEList Binding
+
+-- Helper functions
+def svar (var : Var) : SExpr := .unit $ .sval $ .var var
+def slit (lit : Literal) : SExpr := .unit $ .sval $ .lit lit
+
+end Yatima.Grin

Yatima/Compiler/GrinM.lean

@@ -0,0 +1,53 @@
+import Yatima.Compiler.Grin
+
+open Lean.Compiler.LCNF
+
+namespace Yatima.Grin
+
+-- The Grin compiler monad
+structure GrinEnv where
+  varKind : Lean.NameMap VarKind
+  env : Lean.Environment
+
+structure GrinState where
+  bindings : Lean.NameMap Binding
+  visited  : Lean.NameSet
+  ngen     : Lean.NameGenerator
+  deriving Inhabited
+
+abbrev GrinM := ReaderT GrinEnv $ EStateM String GrinState
+
+instance : Lean.MonadNameGenerator GrinM where
+  getNGen := return (← get).ngen
+  setNGen ngen := modify fun s => { s with ngen := ngen }
+
+def visit (name : Lean.Name) : GrinM Unit :=
+  modify fun s => { s with visited := s.visited.insert name }
+
+@[inline] def isVisited (n : Lean.Name) : GrinM Bool :=
+  return (← get).visited.contains n
+
+@[inline] def varKind (n : Lean.FVarId) : GrinM VarKind := do
+  match (← read).varKind.find? n.name with
+  | some kind => pure kind
+  | none => throw "Unknown variable"
+
+@[inline] def getBinding (n : Lean.FVarId) : GrinM Binding := do
+  match (← get).bindings.find? n.name with
+  | some binding => pure binding
+  | none => throw "Unknown variable"
+
+@[inline] def addBinding (n : Lean.FVarId) (binding : Binding) : GrinM Unit :=
+  modify (fun state => { state with bindings := state.bindings.insert n.name binding })
+
+def GrinM.run (env : GrinEnv) (s : GrinState) (m : GrinM α) :
+    EStateM.Result String GrinState α :=
+  m env |>.run s
+
+def getDecl (declName : Lean.Name) : GrinM Decl := do
+  let env := (← read).env
+  let some decl := getDeclCore? env monoExt declName
+    | throw s!"environment does not contain {declName}"
+  pure decl
+
+end Yatima.Grin