Presentation 20230802 tllhug yuldsl progress report

YulDSL, Linear Haskell & YOLC: A Progress Report

⚠ This file is automatically generated from this org file using this script.

The exported presentation can be accessed via this githack link.

REVISIONS:

Date	Notes
2023-08-02	Tallinn HUG First Meetup Talk.

What You Will Hear About

What is YulDSL and why?
“Evaluating Linear Functions to Symmetric Monoidal Categories” ☠.
Linear Haskell overview.
What is yolc?

YulDSL

A DSL for Solidity/Yul

Yul is an intermediate language designed to support different backends.
But for now, Yul is tightly coupled with Solidity as its frontend language and EVM (Ethereum Virtual Machine) as its backend.
- Solidity is the de-facto programming language for EVM.
- “Web3 projects lose over $2 billion to hacks and exploits in 2022” alone.
YulDSL is a DSL for Yul.

An Yul Example

object "Contract1" {
    // This is the constructor code of the contract.
    code {
        function power(base, exponent) -> result {
            switch exponent
            case 0 { result := 1 }
            case 1 { result := base }
            default {
                result := power(mul(base, base), div(exponent, 2))
                switch mod(exponent, 2)
                case 1 { result := mul(base, result) }
            }
        }

        power
    }
}
    // ...
}

YulDSL as a Categorical Language

Definition of Category

-- from 'base' library:
-- | A class for categories. Instances should satisfy the laws
--
-- [Right identity] @f '.' 'id'  =  f@
-- [Left identity]  @'id' '.' f  =  f@
-- [Associativity]  @f '.' (g '.' h)  =  (f '.' g) '.' h@
--
class Category cat where
    -- | the identity morphism
    id :: cat a a

    -- | morphism composition
    (.) :: cat b c -> cat a b -> cat a c

-- from 'linear-smc' library
class Category k where
  type Obj k :: Type -> Constraint {-<-}
  id   :: Obj k a => a `k` a
  (∘)  :: (Obj k a, Obj k b, Obj k c)
       => (b `k` c) -> (a `k` b) -> a `k` c

Haskell Version of YulDSL (An eDSL, “e” as in Embedded)

-- (Only an excerpt)
data YulCat a b where
-- ...
  YulId   :: forall a.       YulO2 a a     => YulCat a a
  YulComp :: forall a b c.   YulO3 a b c   => YulCat c b -> YulCat a c -> YulCat a b
-- ...
  YulApFun :: forall a b. YulO2 a b => Fn a b -> YulCat a b
  YulITE   :: forall a  . YulO1 a   => YulCat (BOOL, (a, a)) a
  YulMap   :: forall a b. YulO2 a b => YulCat a b -> YulCat [a] [b]
  YulFoldl :: forall a b. YulO2 a b => YulCat (b, a) b -> YulCat [a] b
-- ...
  YulNot :: YulCat BOOL BOOL
  YulAnd :: YulCat (BOOL, BOOL) BOOL
  YulOr  :: YulCat (BOOL, BOOL) BOOL
  YulNumAdd :: forall a. YulNum a => YulCat (a, a) a
  YulNumNeg :: forall a. YulNum a => YulCat a a
-- ...
  YulSGet :: forall a. YulVal a => YulCat ADDR a
  YulSPut :: forall a. YulVal a => YulCat (ADDR, a) ()

YulDSL Can Be Implemented in Other Languages

For “made in Rust”™ folks.
Compatible implementations of the DSL in different languages can be a foundation for an interoperable module system for them.

Motivation Behind YulDSL

Promote Haskell as a safe alternative to Solidity for building on EVM. Why Haskell?
- Leverage its strong type system, tooling and library ecosystem.
- Interopable with Agda, a language suited for writing smart contracts the correctness-by-construction way.
Making a case that we should build fewer new languages when some mature language, such as Haskell, is well suited to provide eDSL to new problem domains.
Building smart contracts at Superfluid using YulDSL.

Linear Functions & SMC

The Paper

Bernardy, Jean-Philippe, and Arnaud Spiwack. “Evaluating linear functions to symmetric monoidal categories.”

Symmetric Monoidal Category & Its Wire Diagrams

SMC is a formal language for such wiring diagrams, notably with these “combinators”

An Example SMC Wire Diagram

This is also called “point-free style.”
However, this type of categorical language is difficult for (normal) human brains.

Same Example But With Variables

The “open semicolon” notation is akin to the “(,)” operator in Haskell.
The familiar Latin letters are so-called “variables” that allow human brains to “delimit” their thinking pattern which helps them to understand or construct programs “more naturally.”

Linear Functions to the Rescue

Correspondence Between Linear Functions & SMC

Indeed, every linear function can be interpreted in terms of an smc. This is a well known fact, proven for example by Szabo [1978, Ch. 3] or Benton [1995].

“Frontend for human; mathematics as backend”

Linear functions is a “frontend language” human can naturally program with.
SMC is the “backend language” that is mathematical and compositional. Compositionality is good for:
- program reusability,
- compositionally correct methodology (Conal Elliot) for program correctness,
- etc.

Linear Haskell

`-XLinearTypes`

A function f is linear if: when its result is consumed exactly once, then its argument is consumed exactly once.

linearity over the arrow: a %1 ->
Multiplicity-polymorphism: forall a b w. a %w -> b
Status: experimental and has limitations.

Relevant Libraries

linear-base

Prelude.Linear as a linear replacement for Prelude.
Additional primitives specific for programming linear functions: Consumable, Moveable, Unrestricted, etc.
Some functions may require -XImpredicativeTypes additionally.

linear-smc

-- | A port represents an input or an output of type @a@ of a morphism in the SMC.
data P k r a

-- | Encode a morphism in the SMC to linear function from port @a@ to port @b@
encode :: O3 k r a b => (a `k` b) -> P k r a %1 -> P k r b~

-- | Decode a linear function from port @a@ to port @b@ to its morphism in the SMC.
decode :: forall a b k con.
          ( con (), con ~ Obj k, Monoidal k, con a, con b
          , forall α β. (con α, con β) => con (α, β)
          )
       => (forall r. Obj k r => P k r a %1 -> P k r b)
       -> a `k` b

An Demo: In-place QuickSort

linear-haskell-demo.hs

(taken from a Tweag blog post)

YOLC: A Frontend for YulDSL

Using Linear Haskell & SMC

The linear-smc Playbook

Define your DSL as a categorical language.

Define SMC instances for your DSL:

instance Category YulCat where
  type Obj YulCat = YulObj
  id  = YulId
  (∘) = YulComp

instance Monoidal YulCat where
  (×)     = YulProd
  unitor  = YulCoerce
  unitor' = YulCoerce
  assoc   = YulCoerce
  assoc'  = YulCoerce
  swap    = YulSwap

instance Cartesian YulCat where
  dis = YulDis
  dup = YulDup

Define additional linear combinators for your domain.
Profit.

A Short Example

rangeSum :: Fn (UINT256 :> UINT256 :> UINT256) UINT256
rangeSum = defun "rangeSum" \(a :> b :> c) ->
  dup2P a & \(a, a') ->
  dup2P b & \(b, b') ->
  dup2P c & \(c, c') ->
  dup2P (a + b) & \ (d, d') ->
  mkUnit a' & \(a', u) ->
  a' + ifThenElse (d <? c) (apfun rangeSum (d' :> b' :> c')) (yulConst 0 u)

A non-linear functions sub-language to calculate these pure values may be more handy to write.
ifThenElse is suited to be used in conjunction with the RebindableSyntax extension.

ERC20 Transfer Function

-- | ERC20 transfer function (no negative balance check for simplicity).
erc20_transfer :: Fn (ADDR :> ADDR :> UINT256) BOOL
erc20_transfer = defun "transfer" \(from :> to :> amount) ->
  (copyAp amount
    (\amount -> passAp from erc20_balance_of & \(from, balance) ->
        erc20_balance_storage from <== balance - amount)
    (\amount -> passAp to erc20_balance_of & \(to, balance) ->
        erc20_balance_storage to <== balance + amount)) &
  yulConst true

`yolc` command line interface

nix-shell$ yolc -h
yolc, the YulDSL commandline transpiler.

Usage: yolc [options] yol_module_spec...

-m [output_mode] Valid output modes: show, plantuml, yul (default)
-h               Display this help and exit
-v               Output more information about what is going on

yol_module_spec: {package_path:}module_name{[symbol...,]}
  where 1) both package_path and symbol list is optional,
        2) default package_path is current working directory (/home/hellwolf/Projects/my/yul-dsl-monorepo),
        3) and default symbol is 'defsym' (TODO, use object instead).

Full Pipeline

scale 500 height

artifact "YulDSL in Haskell" as hsyuldsl
artifact "YulDSL in Rust :D" as rsyuldsl
artifact "Visual Block for YulDSL" as vbyuldsl
agent yolc
artifact "Yul code" as yulcode
agent solc
artifact "EVM Bytecode" as evmbin
agent forge
artifact "EVM Network Instance" as evmnetwork
hsyuldsl -down-> yolc : Compile to YulDSL
rsyuldsl -down-> yolc : Compile to YulDSL
vbyuldsl -down-> yolc : Editing YulDSL visually
yolc     -down-> yulcode : Code generation
yulcode  -down-> solc : Pass yul to solc
solc     -down-> evmbin: Compile yul to binary
evmbin   -down-> forge : Pass to foundry
forge    -down-> evmnetwork : Use foundry to deploy the binary

RESULTS:

Demo

!NOTE!: the work is still in its early stage.

Other Approaches

Since SMC is well suited for visually programming your program formally, so does YulDSL, e.g.:

block-based programming: https://blockell.netlify.app/
https://code.world/blocks

Arrow and its `proc` sugar notation also offer a way of wiring computational graphs:

ArrowPlus a => (<+>) :: a b c -> a b c -> a b c

expr' = (proc x -> returnA -< x)
        <+> (proc x -> do
                symbol Plus -< ()
                y <- term -< ()
                expr' -< x + y)
        <+> (proc x -> do
                symbol Minus -< ()
                y <- term -< ()
                expr' -< x - y)

Other Categories

Traced monoidal category provides an additional notion of feedback over SMC.
YulDSL has a richer structure than SMC, namely also cartesian closed.
- Cartesian closed category (CCC) is correspondent to lambda-calculus, hence normal Haskell function can even be translated to CCC.
- There are various compiling to categories projects. The most notable one is from Conal Elliott. But due to the production-readiness, it is harder to set it up.

What’s Next for YulDSL & YOLC?

Feature complete.
Ship it!

Thank You

Slides available from the wiki area of the yul-dsl-monorepo by searching “yuldsl progress”.