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
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);
}
This simple example contract does the following:
- Address
8f9aa1a1...
is authorized to deposit 123 micro-tDust
into the internal account of address66c6bdc6...
. - 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}
}
}
]
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
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
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