Skip to content

Instantly share code, notes, and snippets.

@bwbush
Last active December 30, 2023 04:47
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save bwbush/2723c7e0a1b2be24eff82b39a0a39484 to your computer and use it in GitHub Desktop.
Save bwbush/2723c7e0a1b2be24eff82b39a0a39484 to your computer and use it in GitHub Desktop.
Executing a simplified version of Marlowe on Midnight's devnet

Executing a simplified version of Marlowe on Midnight's devnet

Kyd, a Marlowe-like language for smart contracts

The Kyd language is a simplified version of the Marlowe language.

The following Lean 4 types define Kyd. For brevity, we omit the specification of the semantics, but they closely mimic Marlowe's semantics.

structure Money where

structure Party where

inductive Authorize where
| By : Party → Authorize

inductive Action where
| Deposit : Money → Party → Action
| Pay : Money → Party → Party → Action
| Transfer : Money → Party → Party → Action

inductive Contract where
| Terminate : Contract
| Act : Authorize → Action → Contract → Contract

inductive Accounts where
| NoAccount : Accounts
| Account : Party → Money → Accounts → Accounts

inductive Ledger where
| mk : Accounts → Ledger

inductive State where
| mk : Accounts → Contract → State

inductive Context where
| mk : Ledger → State → Context

inductive Transaction where
| mk : Context → Command → Context → Transaction

Implementation in Midnight's Compact language

include "std";

export { Action, Party, Amount, KContract }

enum Action { Deposit, Pay, Transfer }

struct Party {
  ident : ZswapCoinPublicKey;
}

struct Amount {
  value : Unsigned Integer[64];
}

struct KContract {
  action : Action;
  authorize : Party;
  fromParty : Maybe[Party];
  toParty : Maybe[Party];
  amount : Amount;
}

ledger {
  accounts : Map[Party,Amount];
  contracts : List[KContract];
  hasBalance : Cell[Boolean];
  balance : Cell[QualifiedCoinInfo];
  constructor(
    // TODO: This was a workaround because `List` cannot be used in the constructor.
    //       Make this less awkward by replacing it with a fixed-length `Vector`.
    contract1 : Maybe[KContract]
  , contract2 : Maybe[KContract]
  , contract3 : Maybe[KContract]
  , contract4 : Maybe[KContract]
  , contract5 : Maybe[KContract]
  , contract6 : Maybe[KContract]
  , contract7 : Maybe[KContract]
  , contract8 : Maybe[KContract]
  ) {
    if (contract8 != none[KContract]()) ledger.contracts.push_front(contract8.value);
    if (contract7 != none[KContract]()) ledger.contracts.push_front(contract7.value);
    if (contract6 != none[KContract]()) ledger.contracts.push_front(contract6.value);
    if (contract5 != none[KContract]()) ledger.contracts.push_front(contract5.value);
    if (contract4 != none[KContract]()) ledger.contracts.push_front(contract4.value);
    if (contract3 != none[KContract]()) ledger.contracts.push_front(contract3.value);
    if (contract2 != none[KContract]()) ledger.contracts.push_front(contract2.value);
    if (contract1 != none[KContract]()) ledger.contracts.push_front(contract1.value);
  }
}

circuit getBalance(
  party : Party
) : Amount {
  return ledger.accounts.member(party) ? ledger.accounts.lookup(party) : new Amount(0);
}

circuit credit(
  party : Party
, amount : Amount
) : Void {
  const oldBalance = getBalance(party);
  const newBalance = new Amount(oldBalance.value + amount.value as Unsigned Integer[64]);
  ledger.accounts.insert(party, newBalance);
}

circuit debitStrict(
  party : Party
, amount : Amount
, newBalance : Amount
) : Void {
  const oldBalance = getBalance(party);
  assert oldBalance.value == newBalance.value + amount.value "Amounts do not balance.";
  if (newBalance.value == 0)
    ledger.accounts.remove(party);
  else
    ledger.accounts.insert(party, newBalance);
}

circuit debitLenient(
  party : Party
, amount : Amount
) : Void {
  const oldBalance = getBalance(party);
  // TODO: Investigate the underflow semantics of minus.
  const newBalance = new Amount(oldBalance.value - amount.value);
  if (newBalance.value == 0)
    ledger.accounts.remove(party);
  else
    ledger.accounts.insert(party, newBalance);
}

circuit debit(
  party : Party
, amount : Amount
, newBalance : Maybe[Amount]
) : Void {
  if (newBalance == none[Amount]())
    // Do not guard against underflow.
    debitLenient(party, amount);
  else
    // Guard against underflow.
    debitStrict(party, amount, newBalance.value);
}

circuit nextContract(
) : KContract {
  assert !ledger.contracts.is_empty() "Contract has terminated.";
  const next = ledger.contracts.head().value;
  ledger.contracts.pop_front();
  return next;
}

circuit assertNextContract(
  action : Action
, fromParty : Maybe[Party]
, toParty : Maybe[Party]
, amount : Amount
) : Void {
  const authorize = new Party(own_public_key());
  const actual = new KContract(action, authorize, fromParty, toParty, amount);
  const expected = nextContract();
  assert actual == expected "No match against contract.";
}

circuit noParty(
) : Maybe[Party] {
  return none[Party]();
}

circuit someParty(
  party : Party
) : Maybe[Party] {
  return some[Party](party);
}

circuit receiveCoin(
  coin : CoinInfo
) : Amount {
  assert coin.color == native_token() "Attempt to receive non-native token.";
  receive(coin);
  if (ledger.hasBalance) {
    ledger.balance.write_coin(
      merge_coin_immediate(ledger.balance, coin)
    , right[ZswapCoinPublicKey,ContractAddress](ledger.self())
    );
  } else {
    ledger.balance.write_coin(
      coin
    , right[ZswapCoinPublicKey,ContractAddress](ledger.self())
    );
    ledger.hasBalance = true;
  }
  return new Amount(coin.value);
}

circuit sendCoin(
  party : Party
, amount : Amount
) : Void {
  // FIXME: Investigate why the `send` used here does debit the
  //        balance at the contract address, but the credited
  //        funds received at the party's address aren't visible.
  //        See <https://github.com/input-output-hk/midnight-documentation/blob/ffa4d166143d38116471d8ea30ff0839001bacdb/docs/reference/compact/compact-std-library/exports.md?plain=1#L326-L333>.
  const result = send(
    ledger.balance
  , left[ZswapCoinPublicKey,ContractAddress](party.ident)
  , amount.value
  );
  if (result.change == none[CoinInfo]()) {
    ledger.hasBalance = false;
    ledger.balance = null(QualifiedCoinInfo);
  } else {
    ledger.balance.write_coin(
      result.change.value
    , right[ZswapCoinPublicKey,ContractAddress](ledger.self())
    );
  }
}


export circuit deposit(
  toParty : Party
, coin : CoinInfo
) : Void {
  const amount = receiveCoin(coin);
  assertNextContract(Action.Deposit, noParty(), someParty(toParty), amount);
  credit(toParty, amount);
}

export circuit pay(
  fromParty : Party
, toParty : Party
, amount : Amount
, newBalance : Maybe[Amount]
) : Void {
  assertNextContract(Action.Pay, someParty(fromParty), someParty(toParty), amount);
  debit(fromParty, amount, newBalance);
  sendCoin(toParty, amount);
}

export circuit transfer(
  fromParty : Party
, toParty : Party
, amount : Amount
, newFromBalance : Maybe[Amount]
) : Void {
  assertNextContract(Action.Transfer, someParty(fromParty), someParty(toParty), amount);
  debit(fromParty, amount, newFromBalance);
  credit(toParty, amount);
}

Example contract

This simple example contract does the following:

  1. Address 8f9aa1a1... is authorized to deposit 123 micro-tDust into the internal account of address 66c6bdc6....
  2. Then address 00998015... is authorized to pay 123 micro-tDust from that account to itself.
[
  {
    is_some: true                          
  , value: {
      action: Action.Deposit
    , authorize: {ident: {bytes: Buffer.from("8f9aa1a106a17d0489a5539d29df0b745d9a91fc4c936af9988de3746d889632", "hex")}}
    , fromParty: {is_some: false, value: {ident: {bytes: Buffer.from("0000000000000000000000000000000000000000000000000000000000000000", "hex")}}}
    , toParty: {is_some: true, value: {ident: {bytes: Buffer.from("66c6bd9d746f189c20ddfba962820a06673cca9834f459dd35adf9c5cb267541", "hex")}}}
    , amount: {value: 123n}
    }
  },
  {
    is_some: true
  , value: {
      action: Action.Pay
    , authorize: {ident: {bytes: Buffer.from("009980157ce4bde4208adf20279fe4f8ac70e16ad2ba30911c0b08619bfb6d69", "hex")}}
    , fromParty: {is_some: true, value: {ident: {bytes: Buffer.from("66c6bd9d746f189c20ddfba962820a06673cca9834f459dd35adf9c5cb267541", "hex")}}}
    , toParty: {is_some: true, value: {ident: {bytes: Buffer.from("009980157ce4bde4208adf20279fe4f8ac70e16ad2ba30911c0b08619bfb6d69", "hex")}}}
    , amount: {value: 123n}
    }
  }
]

Execute the contract on Midnight's devnet

Transaction 1: Create the contract

Anyone can create the contract, but in this case 8f99aa1a1... does.

# yarn devnet-remote
You can do one of the following:
  1. Build a fresh wallet
  2. Build wallet from a seed
Which would you like to do? 2
Enter your wallet seed: (redacted)
[00:47:16.968] INFO (34541): Your wallet seed is: (redacted)
[00:47:16.971] INFO (34541): Your wallet address is: 8f9aa1a106a17d0489a5539d29df0b745d9a91fc4c936af9988de3746d889632|010001bb6c3991eb983af5f1282fa66dbba40305396029b0aa67e29af11281f4ee820f
[00:47:16.971] INFO (34541): Your wallet public key is: 8f9aa1a106a17d0489a5539d29df0b745d9a91fc4c936af9988de3746d889632
[00:47:16.972] INFO (34541): Your wallet balance is: 0
[00:47:16.972] INFO (34541): Waiting to receive tokens...
[00:47:16.982] INFO (34541): Wallet scanned 0 blocks out of unknown number
[00:47:26.999] INFO (34541): Wallet scanned 0 blocks out of unknown number
[00:47:37.030] INFO (34541): Wallet scanned 179817 blocks out of 1578204
[00:47:47.052] INFO (34541): Wallet scanned 504813 blocks out of 1578207
[00:47:57.077] INFO (34541): Wallet scanned 907788 blocks out of 1578211
[00:48:07.867] INFO (34541): Wallet scanned 1578218 blocks out of 1578218
[00:48:07.869] INFO (34541): Your wallet balance is: 494054

You can do one of the following:
  1. Deploy a new Kyd contract
  2. Join an existing Kyd contract
Which would you like to do? 1
[00:48:11.281] INFO (34541): Deploying Kyd contract...
[00:49:16.760] INFO (34541): Deployed contract at address: 01000166266edec7db0cc559d988ff3cd6d73878be0216446f13c263ff59a7c9bdb114

Transaction 2: Deposit the funds

You can do one of the following:
  1. Display current Kyd contract
  2. Deposit funds into an internal account of the contract
  3. Transfer funds between the contract's internal accounts
  4. Pay funds from an internal account of the contract
  5. Exit
Which would you like to do? 2
Deposit to party's account: 66c6bd9d746f189c20ddfba962820a06673cca9834f459dd35adf9c5cb267541
Deposit amount: 123
[00:50:30.982] INFO (34541): Transaction 361fd1a8ac72fcefd3766631d58a9db736c9655ce98f248a724e4e7948b82669 added in block 1578248

You can do one of the following:
  1. Display current Kyd contract
  2. Deposit funds into an internal account of the contract
  3. Transfer funds between the contract's internal accounts
  4. Pay funds from an internal account of the contract
  5. Exit
Which would you like to do? 5
[00:50:35.745] INFO (34541): Exit
# yarn devnet-remote

Transaction 3. Pay the funds

Now 00998015... connects to the contract and withdraws the funds.

You can do one of the following:
  1. Build a fresh wallet
  2. Build wallet from a seed
Which would you like to do? 2
Enter your wallet seed: (redacted)
[00:50:42.917] INFO (34563): Your wallet seed is: (redacted)
[00:50:42.919] INFO (34563): Your wallet address is: 009980157ce4bde4208adf20279fe4f8ac70e16ad2ba30911c0b08619bfb6d69|0100012eadfc22f891f6cdce5d1f10ed5ff37c77013ac3219e16d5ff0cfc04f9d1bfd1
[00:50:42.919] INFO (34563): Your wallet public key is: 009980157ce4bde4208adf20279fe4f8ac70e16ad2ba30911c0b08619bfb6d69
[00:50:42.920] INFO (34563): Your wallet balance is: 0
[00:50:42.920] INFO (34563): Waiting to receive tokens...
[00:50:42.925] INFO (34563): Wallet scanned 0 blocks out of unknown number
[00:50:52.964] INFO (34563): Wallet scanned 0 blocks out of unknown number
[00:51:02.994] INFO (34563): Wallet scanned 148602 blocks out of 1578262
[00:51:13.018] INFO (34563): Wallet scanned 397086 blocks out of 1578267
[00:51:23.055] INFO (34563): Wallet scanned 696408 blocks out of 1578269
[00:51:33.091] INFO (34563): Wallet scanned 1024213 blocks out of 1578274
[00:51:43.788] INFO (34563): Wallet scanned 1578281 blocks out of 1578281
[00:51:43.789] INFO (34563): Your wallet balance is: 1155015

You can do one of the following:
  1. Deploy a new Kyd contract
  2. Join an existing Kyd contract
Which would you like to do? 2
What is the contract address (in hex)? 01000166266edec7db0cc559d988ff3cd6d73878be0216446f13c263ff59a7c9bdb114
[00:52:51.339] INFO (34563): Joined contract at address: 01000166266edec7db0cc559d988ff3cd6d73878be0216446f13c263ff59a7c9bdb114

You can do one of the following:
  1. Display current Kyd contract
  2. Deposit funds into an internal account of the contract
  3. Transfer funds between the contract's internal accounts
  4. Pay funds from an internal account of the contract
  5. Exit
Which would you like to do? 4
Pay from party's account: 66c6bd9d746f189c20ddfba962820a06673cca9834f459dd35adf9c5cb267541
Pay to party's address: 009980157ce4bde4208adf20279fe4f8ac70e16ad2ba30911c0b08619bfb6d69
Pay amount: 123
[00:54:34.137] INFO (34563): Transaction 88199534d52713051b944eb009070d1209b4b207ef5b8c724b8ccbf8e068f05d added in block 1578323

You can do one of the following:
  1. Display current Kyd contract
  2. Deposit funds into an internal account of the contract
  3. Transfer funds between the contract's internal accounts
  4. Pay funds from an internal account of the contract
  5. Exit
Which would you like to do? 5
[00:54:38.943] INFO (34563): Exit
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment