Presentation functional solidity

Pure Functional Solidity for Fun and Profit

⚠ 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-04-06	Draft started for EthereumZüri.ch
2023-04-11	v1.1 for EthereumZürich
2023-04-13	v1.2 for EthereumZürich

The Goals of The Talk

Demonstrate the possibility of limited functional programming in Solidity.
Use the new paradigm to build a simple super token step by step.
Examples of using Certora to formally verify the code.
Make you interested in functional programming.

Re-imagine What Is a Token

Mental Model for a Super Token

Token is like a bank, containing a collection of /accounts/.
Each account has an owner, representing the owner’s wallet with a collection of /monetary units/.
Each /monetary unit/ provides a balance and a set of payment primitives.

Generalized Payment Primitives

shift (ERC20.transfer, 1 to 1 instant transfer of value)
flow (1 to 1 constant flow of value, aka. “money streaming”)
distribute (1 to N instant transfer of value)
distributeFlow (1 to N constant flow of value)

—

	1 to 1	1 to N
	<c>	<c>
instant	`shift`	`distribute`
constant flow	`flow`	`distributeFlow`

Frictionless Value

Real time: modeled as moving per second (per block in effect).
Composable: can be “chained” with other payment primitives; using the value the same moment its received.

Programmability

On-chain Mechanism: using callbacks to perform conditional logic (e.g. flow based decentralized exchange reacting to incoming flow changed).
Off-chain Incentives: any other conditional logic that is impossible to do on-chain (e.g. time condition).

More Thoughts about Super Token

As a helpful analogy, think of these monetary units as smarter “coins/cards/notes” in your wallets.
Optionally, in some a UTXO-based systems, the on-chain representation of account could be completely bypassed.

Let’s Build a Simple Super Token Today

With all generalized payment primitives.
For fun!
Disclaimer: many things missing, not for production!

Steps of Building a Simple Super Token

Monetary Type
The Smallest Monetary Unit Type: Basic Particle
Laws for Monetary Units
Monetary Unit Type for a Pool of Money
The 2-primitives
Make It Actually Do Something

Step 1) Monetary Types

Using custom types to wrap numerical values,
and operator overloading (since 0.8.19).

Time

/// Time value represented by uint32 unix timestamp.
type Time is uint32;

function mt_t_add_t(Time a, Time b) pure returns (Time) {
    return Time.wrap(Time.unwrap(a) + Time.unwrap(b));
}

function mt_t_sub_t(Time a, Time b) pure returns (Time) {
    return Time.wrap(Time.unwrap(a) - Time.unwrap(b));
}

using { mt_t_add_t as +, mt_t_sub_t as - } for Time global;

Value

/// Monetary value represented with signed integer.
type Value is int256;

function mt_v_add_v(Value a, Value b) pure returns (Value) {
    return Value.wrap(Value.unwrap(a) + Value.unwrap(b));
}

function mt_v_sub_v(Value a, Value b) pure returns (Value) {
    return Value.wrap(Value.unwrap(a) - Value.unwrap(b));
}

using { mt_v_add_v as +, mt_v_sub_v as - } for Value global;

FlowRate

type FlowRate is int128;

function mt_r_add_r(FlowRate a, FlowRate b) pure returns (FlowRate) {
    return FlowRate.wrap(FlowRate.unwrap(a) + FlowRate.unwrap(b));
}

function mt_r_sub_r(FlowRate a, FlowRate b) pure returns (FlowRate) {
    return FlowRate.wrap(FlowRate.unwrap(a) - FlowRate.unwrap(b));
}

using { mt_r_add_r as +, mt_r_sub_r as - } for FlowRate global;

Unit

/// Unit value represented with half the size of `Value`.
type Unit is int128;

function mt_u_add_u(Unit a, Unit b) pure returns (Unit) {
    return Unit.wrap(Unit.unwrap(a) + Unit.unwrap(b));
}

function mt_u_sub_u(Unit a, Unit b) pure returns (Unit) {
    return Unit.wrap(Unit.unwrap(a) - Unit.unwrap(b));
}

using { mt_u_add_u as +, mt_u_sub_u as - } for Unit global;

Using Additional Library for Mixed-Types Operators

library AdditionalMonetaryTypeHelpers {
    //...
    function inv(FlowRate r) internal pure returns (FlowRate) {
        return FlowRate.wrap(-FlowRate.unwrap(r));
    }
    function mul(FlowRate r, Time t) internal pure returns (Value) {
        return Value.wrap(FlowRate.unwrap(r) * int(uint(Time.unwrap(t))));
    }
    //...
}
using AdditionalMonetaryTypeHelpers for Time global;
using AdditionalMonetaryTypeHelpers for Value global;
using AdditionalMonetaryTypeHelpers for Unit global;
using AdditionalMonetaryTypeHelpers for FlowRate global;

Steps of Building a Simple Super Token

Monetary Type
The Smallest Monetary Unit Type: Basic Particle
Laws for Monetary Units
Monetary Unit Type for a Pool of Money
The 2-primitives
Make It Actually Do Something

Step 2) The Smallest Monetary Unit: Basic Particle

The building block for payment primitives.

Data Definition

struct BasicParticle {
    Time     _settled_at;
    Value    _settled_value;
    FlowRate _flow_rate;
}

`clone`: make it purer

“Strictly Pure”:
- NB! References types passed with the “memory” keyword can be modified by pure functions!
- We use clone semantics rigorously to support even purer solidity functions.

/// Pure data clone function.
function clone(BasicParticle memory a) internal pure
    returns (BasicParticle memory b)
{
    b._settled_at = a._settled_at;
    b._settled_value = a._settled_value;
    b._flow_rate = a._flow_rate;
}

Note the boilerplate needed. There is no general way to do “memcpy” in Solidity (lack of sizeof and a EVM opcode?).

`rtb`: the real time balance function

/// Monetary unit rtb function for basic particle/universal index.
function rtb(BasicParticle memory a, Time t) internal pure
    returns (Value v)
{
    return a._flow_rate.mul(t - a._settled_at) + a._settled_value;
}

`settle`: synchronize values to a specific time

NB! This is the most important operation, other operations must be applied to monetary units settled to the same time.

/// Monetary unit settle function for basic particle/universal index.
function settle(BasicParticle memory a, Time t) internal pure
    returns (BasicParticle memory b)
{
    b = a.clone();
    b._settled_value = rtb(a, t);
    b._settled_at = t;
}

Steps of Building a Simple Super Token

Monetary Type
The Smallest Monetary Unit Type: Basic Particle
Laws for Monetary Units
Monetary Unit Type for a Pool of Money
The 2-primitives
Make It Actually Do Something

Step 3) Laws for Monetary Units

Mathematical laws that governs how these functions should work together.
Tested through property testing,
- through foundry fuzzing testing framework,
- or formally verified using SMTChecker or tools like Certora.

All Monetary Units Are Monoid

Monoid: a data type that’s equipped with a binary operator “$×$” (“mappend”) and satisfies these laws:

Monoidal Identity Law

$$ ∅ × x = x\ and\ x × ∅ = x $$

function test_u_monoid_identity(BasicParticle memory p1) external
{
    BasicParticle memory id;
    assertEq(p1, p1.mappend(id), "e1");
    assertEq(p1, id.mappend(p1), "e2");
}

Monoidal Associativity Law

$$ (a × b) × c = a × (b × c) $$

function test_u_monoid_assoc(BasicParticle memory p1,
                             BasicParticle memory p2,
                             BasicParticle memory p3) external
{
    assertEq(p1.mappend(p2).mappend(p3),
             p1.mappend(p2.mappend(p3)));
}

Monetary Unit Has Its Own Laws

Settle-Idempotence Law

$$ a.settle(t1).settled\_at() = t1 $$ $$ a.settle(t1).settle(t1) = a.settle(t1) $$

function test_u_settle_idempotence(BasicParticle memory p, uint16 m) external
{
    Time t1 = p.settled_at() + Time.wrap(m);
    BasicParticle memory p1 = p.settle(t1);
    BasicParticle memory p2 = p1.settle(t1);
    assertEq(p1.settled_at(), t1, "e1");
    assertEq(p1, p2, "e2");
}

Fun fact: ChatGPT4 understood the test function name and can generate almost correct test code.

Constant RTB Law

$$ a.settle(t1).rtb(t3) = a.settle(t2).rtb(t3) = a.rtb(t3) $$ $$ a.settle(t1).settle(t2).rtb(t3) = a.rtb(t3) $$

function test_u_constant_rtb(BasicParticle memory p,
                             uint16 m1,
                             uint16 m2,
                             uint16 m3) external
{
    Time t1 = p.settled_at() + Time.wrap(m1);
    Time t2 = t1 + Time.wrap(m2);
    Time t3 = t2 + Time.wrap(m3);
    assertEq(p.settle(t1).rtb(t3), p.rtb(t3), "e1");
    assertEq(p.settle(t2).rtb(t3), p.rtb(t3), "e2");
    assertEq(p.settle(t1).settle(t2).rtb(t3), p.rtb(t3), "e3");
}

Steps of Building a Simple Super Token

Monetary Type
The Smallest Monetary Unit Type: Basic Particle
Laws for Monetary Units
Monetary Unit Type for a Pool of Money
The 2-primitives
Make It Actually Do Something

Step 4) Monetary Units for a Pool of Money

What can be a good data structure for 1 to N payment primitives?
Each pool has members.
Each member owns some amount of units.
Anyone can distribute money through a pool to its members.
These distributions can be instant or as flows.
Member’s share of these distributions are proportional to number of units relative to others’.

Data Definitions

struct PDPoolIndex {
    Unit          total_units;
    // measured per unit
    BasicParticle _wrapped_particle;
}

struct PDPoolMember {
    Unit          owned_units;
    Value         _settled_value;
    // a copy of wrapped_particle
    BasicParticle _synced_particle;
}

/// The monetary unit for a pool member
struct PDPoolMemberMU {
    PDPoolIndex  i;
    PDPoolMember m;
}

`rtb` function

function rtb(PDPoolMemberMU memory a, Time t) internal pure
    returns (Value v)
{
    return a.m._settled_value +
        (a.i._wrapped_particle.rtb(t)
         - a.m._synced_particle.rtb(a.m._synced_particle.settled_at())
        ).mul(a.m.owned_units);
}

`settle` function

function settle(PDPoolIndex memory a, Time t) internal pure
    returns (PDPoolIndex memory m)
{
    m = a.clone();
    m.wrapped_particle = m.wrapped_particle.settle(t);
}

function settle(PDPoolMemberMU memory a, Time t) internal pure
    returns (PDPoolMemberMU memory b)
{
    b.i = a.i.settle(t);
    b.m = a.m.clone();
    b.m.settled_value = a.rtb(t);
    b.m.synced_particle = b.i.wrapped_particle;
}

The Laws Again

PDPoolMemberMU is a type of PDPoolMemberMU.
The same monoid Laws & monetary unit laws should be satisfied.

Steps of Building a Simple Super Token

Monetary Type
The Smallest Monetary Unit Type: Basic Particle
Laws for Monetary Units
Monetary Unit Type for a Pool of Money
The 2-primitives
Make It Actually Do Something

Step 5) The 2-primitives

We define 2-primitives as payment primitives that involve two monetary units, typically indexed as “from” and “to” respectively:

shift2: shift value between from and to.
flow2: set absolute flow rate between from and to.
- shift_flow2: a variant to shift flow rate between from and to.

`flow2` primitive

function flow2(BasicParticle memory a,
               BasicParticle memory b,
               FlowRate r,
               Time t) internal pure
    returns (BasicParticle memory m,
             BasicParticle memory n)
{
    m = a.settle(t).flow1(r.inv());
    n = b.settle(t).flow1(r);
}

function flow2(BasicParticle memory a,
               PDPoolIndex memory b,
               FlowRate r,
               Time t) internal pure
    returns (BasicParticle memory m,
             PDPoolIndex memory n, FlowRate r1)
{
    (n, r1) = b.settle(t).flow1(r);
    m = a.settle(t).flow1(r1.inv());
}

NB! Both implementations of flow2 are almost identical!

`shift_flow2b` 2-primitive

function shift_flow2b
    (BasicParticle memory a,
     BasicParticle memory b,
     FlowRate dr,
     Time t) internal pure
    returns
        (BasicParticle memory m,
         BasicParticle memory n)
{
    BasicParticle memory mempty;
    BasicParticle memory a1;
    BasicParticle memory a2;
    FlowRate r = b.flow_rate();
    (a1,  ) = mempty
        .flow2(b, r.inv(), t);
    (a2, n) = mempty
        .flow2(b, r + dr, t);
    m = a .mappend(a1).mappend(a2);
}

function shift_flow2b
    (BasicParticle memory a,
     PDPoolIndex memory b,
     FlowRate dr,
     Time t) internal pure
    returns (BasicParticle memory m,
             PDPoolIndex memory n,
             FlowRate r1)
{
    BasicParticle memory mempty;
    BasicParticle memory a1;
    BasicParticle memory a2;
    FlowRate r = b.flow_rate();
    (a1,  ,   ) = mempty
        .flow2(b, r.inv(), t);
    (a2, n, r1) = mempty
        .flow2(b, r + dr, t);
    m = a .mappend(a1).mappend(a2);
}

NB! They are almost identical too!
We need generic programming in solidity!

Laws for `flow-2` Primitive

Law of Conservation of Value (LCV)

Any combination of payment primitives should yield a constant sum of balances of all involved accounts at any time.

Property for Two Accounts + Two Ops

The following property proves that the LCV is true for two accounts and any combination of two consecutive payment primitives.

function run_uu_test(uint16 m1, int64 x1, uint16 m2, int64 x2, uint16 m3,
                     function (BasicParticle memory, BasicParticle memory, Time, int64)
                         internal pure
                         returns (BasicParticle memory, BasicParticle memory) op1,
                     function (BasicParticle memory, BasicParticle memory, Time, int64)
                         internal pure
                         returns (BasicParticle memory, BasicParticle memory) op2
                    ) internal {
    UU_Test_Data memory d;
    d.t1 = Time.wrap(m1);
    d.t2 = d.t1 + Time.wrap(m2);
    d.t3 = d.t2 + Time.wrap(m3);

    (d.a, d.b) = op1(d.a, d.b, d.t1, x1);
    (d.a, d.b) = op2(d.a, d.b, d.t2, x2);
    assertEq(0, Value.unwrap(d.a.rtb(d.t3) + d.b.rtb(d.t3)));
}

Generate Tests

function test_uu_ss(uint16 m1, int64 x1, uint16 m2, int64 x2, uint16 m3) external {
    run_uu_test(m1, x1, m2, x2, m3, uu_shift2, uu_shift2);
}
function test_uu_ff(uint16 m1, int64 r1, uint16 m2, int64 r2, uint16 m3) external {
    run_uu_test(m1, r1, m2, r2, m3, uu_flow2, uu_flow2);
}
function test_uu_fs(uint16 m1, int64 r1, uint16 m2, int64 x2, uint16 m3) external {
    run_uu_test(m1, r1, m2, x2, m3, uu_flow2, uu_shift2);
}
function test_uu_sf(uint16 m1, int64 x1, uint16 m2, int64 r2, uint16 m3) external {
    run_uu_test(m1, x1, m2, r2, m3, uu_shift2, uu_flow2);
}

Combine this property and monoid laws, one should be able to reason the law of conservation of value is satisfied.

Mapping from 2-primitives to Payment Primitives

BasicParticle can be also known as universal index (uIdx), meaning every account is expected to have one and usually only one.
In contrast, PDPoolIndex (pdpIdx) is an index for pools.
Then we have can compose two 2-premitives and different index types to get all four payment primitives:
- transfer = shift2(:uIdx, :uIdx)
- flow = flow2(:uIdx, :uIdx)
- distribute = shift2(:uIdx, :pdpIdx)
- distributeFlow = flow2(:uIdx, :pdpIdx)

Steps of Building a Simple Super Token

Monetary Type
The Smallest Monetary Unit Type: Basic Particle
Laws for Monetary Units
Monetary Unit Type for a Pool of Money
The 2-primitives
Make It Actually Do Something

Step 6) Make It Actually Do Something

So far so good, now we have a strictly pure solidity library (SemanticMoney.sol) for building super tokens with generalized payment primitives.
One problem: they can’t do anything useful!
Wait for it … 🥁

The M-Word

No one has managed to explain what is a monad.
But let us focus on what we need at hand:
A reusable code that uses ~SemanticMoney.sol~ for building super tokens

Monad for Building Super Tokens

Some reusable codes assemble SemanticMoney.sol functions and user extended code in a correct linear sequence.
- That, basically is what monad is about: a linear code sequence of effects woven with pure functions.
Most of programming languages is giant monad with different syntaxes and ergonomics for achieving computational effects.
- Solidity is a normal programming language, and there are two ways of expressing the reusable linear code sequence.

TokenMonad with Abstract Contract & Virtual Functions

TokenMonad: an abstract contract with virtual functions.
_doXYZ functions: linear sequence of effects calling virtual functions for user injected logic.
bytes memory eff: for user defined data passing through calls linearly.

TokenMonad Snippets

abstract contract TokenMonad { /* ... */
    function _setUIndex(bytes memory eff, address owner, BasicParticle memory p)
        internal virtual returns (bytes memory);

    function _doFlow(bytes memory eff, address from, address to,
                     bytes32 flowHash, FlowRate flowRate, Time t)
        internal returns (bytes memory)
    {
        FlowRate flowRateDelta = flowRate - _getFlowRate(eff, flowHash);
        BasicParticle memory a = _getUIndex(eff, from);
        BasicParticle memory b = _getUIndex(eff, to);
        (a, b) = a.shift_flow2b(b, flowRateDelta, t);
        eff = _setUIndex(eff, from, a);
        eff = _setUIndex(eff, to, b);
        eff = _setFlowInfo(eff, flowHash, from, to, flowRate);
        return eff;
    }
/* ... */ }

Implement token.flow Using TokenMonad

function flow(address from, address to, FlowId flowId, FlowRate flowRate) public
    returns (bool success)
{
    // check inputs
    require(!_isPool(to), "Use distributeFlow to pool");
    require(FlowRate.unwrap(flowRate) >= 0, "Flow rate must not be negative");
    require(from != to, "Shall not send flow to oneself");

    // simple permission control
    require(msg.sender == from, "No flow permission");

    // prepare local variables (let bindings)
    Time t = Time.wrap(uint32(block.timestamp));
    bytes32 flowHash = getFlowHash(from, to, flowId);

    // Make updates
    bytes memory eff = _tokenEff(/* your own extra contexts put here */);
    _doFlow(eff, from, to, flowHash, flowRate, t);
    return true;
}

TokenEff with Function Pointers & Pipeline Ergonomics

Now for something more radical…
Emulating ergonomics of effectful programming.
- hot stuff in functional programming; generalized try/catch:

log {
  …
} handle {
 case (Logger.debug message -> remainderOfProgram ) ->
   print ("Debug: " ++ message)
   remainderOfProgram
 case (Logger.warn message -> remainderOfProgram ) ->
   print ("Warn: " ++ message)
   remainderOfProgram
}

TokenEff Snippet (1) Eff Data & Function Pointers

struct TokenEff {/* ... */
    function (TokenEff memory, address /*owner*/, BasicParticle memory)
        internal returns (TokenEff memory) setUIndex;
/* ... */}

library TokenEffLib {
    // wrapping function pointer (handler)
    function setUIndex (TokenEff memory eff, address owner,
                        BasicParticle memory p)
        internal returns (TokenEff memory)
    {
        return eff.setUIndex(eff, owner, p);
    }
}
using TokenEffLib for TokenEff global;

TokenEff Snippet (2) `TokenEffLib.flow`

library TokenEffLib {
    function flow(TokenEff memory eff, address from, address to,
                  bytes32 flowHash, FlowRate flowRate, Time t)
        internal returns (TokenEff memory)
    {
        FlowRate flowRateDelta = flowRate - eff.getFlowRate(flowHash);
        BasicParticle memory a = eff.getUIndex(from);
        BasicParticle memory b = eff.getUIndex(to);
        (a, b) = a.shift_flow2a(b, flowRateDelta, t);
        return eff.setUIndex(from, a)
            .setUIndex(to, b)
            .setFlowInfo(eff, flowHash, from, to, flowRate);
    }
}

Reimplement token.flow Using TokenEff

function flow(address from, address to, FlowId flowId, FlowRate flowRate) public
    returns (bool success)
{
    //..

    // prepare local variables (let bindings)
    Time t = Time.wrap(uint32(block.timestamp));
    bytes32 flowHash = getFlowHash(from, to, flowId);

    Value bufferAmount = _calculateRequiredBuffer(flowRate);

    // Make updates (
    _tokenEff(/* extra context for setting up handlers*/)
        .shift(from, address(this), bufferAmount)
        .flow(from, to, flowHash, flowRate, t);
    return true;
}

What Have We Achieved?

A solidity library for building Super Token.
- Strictly pure (all inputs are copied or cloned).
- Using common structure such as monoid leveraging existing laws (“theorem for free”)
- Defining new laws and test them with property based testing.
Two variants reusable monadic interface reducing further boilerplate needed for building Super Token.
- TokenMonad using abstract contracts and virtual functions for extensions.
- TokenEff using library and emulating a pipeline ergonomics in Solidity.

“It is all cute and exotic, but why it matters?”

What Is Functional Programming

Implement as much code as possible in data definition, equations and logical formulas (properties).
- For these codes, strictly pure functions are your friends because of referential transparency!
To make code actually useful, implement computational strategies:
- typically as sequential programs (aka. Monads!),
- also concurrent and graph computing:
  - typically for distributed (UTXO!) and high performance computing;
  - think of spreadsheet as an example, in its pure form, it is functional programming and graph computing!

Why Functional Programming

The gateway drug: “Hughes, J., 1989. Why functional programming matters.”
“As software becomes more and more complex, it is more and more important to structure it well. Well-structured software is easy to write, easy to debug, and provides a collection of modules that can be re-used to reduce future programming costs”
Keywords: better debugging, better re-usability, less maintenance cost.
AUTHOR’S CLAIM: best suited way to structure smart contracts.

Formal Verification Becomes Easier

Properties can also be tested through formal verification tools.
- Solidity has built-in SMTChecker for limited range of verifications.
- Certora is a packaged solution using a more expressive static analysis and constraint solving language called “Certora Verification Language”.

Relentless modularization and breakdown of code makes these tools work better.

Magic 1 - Rules: Test Property Mathematically

token.flow during any state of the token should result no new net flow rate change:

rule poolless_flow_constant_flowrate_sum() {
    //... omitted some boiler plates

    int128 r0 = getFlowRate(a, b, i);
    int128 ar1 = getNetFlowRate(a);
    int128 br1 = getNetFlowRate(b);

    bool successful = flow(e1, a, b, i, r);
    assert successful;

    int128 r1 = getFlowRate(a, b, i);
    int128 ar2 = getNetFlowRate(a);
    int128 br2 = getNetFlowRate(b);

    assert r == r1;
    assert to_mathint(ar1) - to_mathint(ar2)
        == to_mathint(r) - to_mathint(r0);
    assert to_mathint(ar2) - to_mathint(ar1)
        == to_mathint(br1) - to_mathint(br2);
}

Magic 2 - Inductive Reasoning Through Invariance

Inductively prove that total flow rate of the system is always ZERO:

invariant zero_net_flow_rate() totalFlowRate() == 0
    filtered { f -> f.selector !=
                   /* absorbParticlesFromPool(address[],(uint32,int256,int128)[]) */
                   0x57587b39
               && f.selector !=
                   operatorSetIndex((int128,(uint32,int256,int128))).selector
               && f.selector !=
                   operatorConnectMember(uint32,address,bool).selector }

Thank you for listening!

*Let’s Make Solidity Code Better Using Functional Programming Now!!*

Transcript available from github-wiki:superfluid-finance/protocol-monorepo.

Docs | Dashboard | Console | Twitter | Discord

Superfluid Protocol Wiki

Governance Overview
- Governance Process: Minimum Deposit Policy
- Superfluid Governance Multisigs
For Contributors
Development Process
Protocol EVMv1 Operations
Protocol EVMv1 Technical Notes
Protocol EVMv1 Core Subgraph
- Subgraph Data Integrity Reference

Presentation functional solidity

Pure Functional Solidity for Fun and Profit

The Goals of The Talk

Re-imagine What Is a Token

Mental Model for a Super Token

Generalized Payment Primitives

Frictionless Value

Programmability

More Thoughts about Super Token

Let’s Build a Simple Super Token Today

Steps of Building a Simple Super Token

Step 1) Monetary Types

Time

Value

FlowRate

Unit

Using Additional Library for Mixed-Types Operators

Steps of Building a Simple Super Token

Step 2) The Smallest Monetary Unit: Basic Particle

Data Definition

clone: make it purer

rtb: the real time balance function

settle: synchronize values to a specific time

Steps of Building a Simple Super Token

Step 3) Laws for Monetary Units

All Monetary Units Are Monoid

Monoidal Identity Law

Monoidal Associativity Law

Monetary Unit Has Its Own Laws

Settle-Idempotence Law

Constant RTB Law

Steps of Building a Simple Super Token

Step 4) Monetary Units for a Pool of Money

Data Definitions

rtb function

settle function

The Laws Again

Steps of Building a Simple Super Token

Step 5) The 2-primitives

flow2 primitive

shift_flow2b 2-primitive

Laws for flow-2 Primitive

Law of Conservation of Value (LCV)

Property for Two Accounts + Two Ops

Generate Tests

Mapping from 2-primitives to Payment Primitives

Steps of Building a Simple Super Token

Step 6) Make It Actually Do Something

The M-Word

Monad for Building Super Tokens

TokenMonad with Abstract Contract & Virtual Functions

TokenMonad Snippets

Implement token.flow Using TokenMonad

TokenEff with Function Pointers & Pipeline Ergonomics

TokenEff Snippet (1) Eff Data & Function Pointers

TokenEff Snippet (2) TokenEffLib.flow

Reimplement token.flow Using TokenEff

What Have We Achieved?

“It is all cute and exotic, but why it matters?”

What Is Functional Programming

Why Functional Programming

Formal Verification Becomes Easier

Magic 1 - Rules: Test Property Mathematically

Magic 2 - Inductive Reasoning Through Invariance

Thank you for listening!

Clone this wiki locally

`clone`: make it purer

`rtb`: the real time balance function

`settle`: synchronize values to a specific time

`rtb` function

`settle` function

`flow2` primitive

`shift_flow2b` 2-primitive

Laws for `flow-2` Primitive

TokenEff Snippet (2) `TokenEffLib.flow`