-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #156 from freespek/igor/generate-tla
An EJS template to populate the TLA+ spec of xycloans
- Loading branch information
Showing
11 changed files
with
349 additions
and
30 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,168 @@ | ||
| ------------------------------- MODULE MC ------------------------------- | ||
| <%# | ||
| /* | ||
| * An EJS template for generating the initial state from the aggregated state of the contract. | ||
| * | ||
| * Usage: | ||
| * | ||
| * npx ejs MCxycloans_monitor.ejs.tla -f state.json >MC.tla | ||
| * | ||
| * Igor Konnov, 2024 | ||
| */ | ||
| %> | ||
| (* THIS MODULE IS AUTOGENERATED FROM SOROBAN STATE *) | ||
| EXTENDS Integers, Apalache, xycloans_types | ||
|
|
||
| \* the set of all possible token amounts | ||
| AMOUNTS == Nat | ||
| \* the contract address for the xycLoans contract | ||
| XYCLOANS == "<%- contractId %>" | ||
| \* the token address | ||
| XLM_TOKEN_SAC_TESTNET == "<%- storage[contractId].instance.TokenId %>" | ||
|
|
||
| <% | ||
| const balanceAddrs = | ||
| Object.keys(storage[contractId].persistent) | ||
| .filter((key) => key.startsWith("Balance,")) | ||
| .map((key) => key.split(",")[1]) | ||
| %> | ||
| \* user-controlled addresses | ||
| USER_ADDR == { | ||
| <%- | ||
| balanceAddrs | ||
| .map((addr) => ` "${addr}"`) | ||
| .join(",\n") | ||
| %> | ||
| } | ||
|
|
||
| <% | ||
| const tokenAddrs = | ||
| Object.keys(storage[storage[contractId].instance.TokenId].persistent) | ||
| .filter((key) => key.startsWith("Balance,")) | ||
| .filter((key) => key !== `Balance,${contractId}`) | ||
| .map((key) => key.split(",")[1]) | ||
| %> | ||
| \* addresses that hold token balances | ||
| TOKEN_ADDR == { | ||
| <%- | ||
| tokenAddrs | ||
| .map((addr) => ` "${addr}"`) | ||
| .join(",\n") | ||
| %> | ||
| } | ||
|
|
||
| \* the pool of addresses to draw the values from | ||
| ADDR == { XYCLOANS, XLM_TOKEN_SAC_TESTNET } \union TOKEN_ADDR \union USER_ADDR | ||
|
|
||
| VARIABLES | ||
| \* @type: $tx; | ||
| last_tx, | ||
| \* @type: Str -> Int; | ||
| shares, | ||
| \* @type: Int; | ||
| total_shares, | ||
| \* @type: Int; | ||
| fee_per_share_universal, | ||
| \* Keep track of the current storage, | ||
| \* which can be only changed by a successful transaction. | ||
| \* @type: $storage; | ||
| storage | ||
|
|
||
| INSTANCE xycloans_monitor | ||
|
|
||
| <% | ||
| function renderKVStore(storage, prefix, mapper = (x) => x) { | ||
| return Object.keys(storage) | ||
| .filter((key) => key.startsWith(prefix)) | ||
| .map((key) => key.split(",")[1]) | ||
| .map((addr) => ` <<"${addr}", ${mapper(storage[prefix + addr])}>>`) | ||
| .join(",\n") | ||
| } | ||
| %> | ||
|
|
||
| Init == | ||
| LET init_stor == [ | ||
| self_instance |-> [ | ||
| FeePerShareUniversal |-> <%- storage[contractId].instance.FeePerShareUniversal %>, | ||
| TokenId |-> "<%- storage[contractId].instance.TokenId %>" | ||
| ], | ||
| self_persistent |-> [ | ||
| Balance |-> SetAsFun({ | ||
| <%- | ||
| renderKVStore(storage[contractId].persistent, "Balance,") | ||
| %> | ||
| }), | ||
| MaturedFeesParticular |-> SetAsFun({ | ||
| <%- | ||
| renderKVStore(storage[contractId].persistent, "MaturedFeesParticular,") | ||
| %> | ||
| }), | ||
| FeePerShareParticular |-> SetAsFun({ | ||
| <%- | ||
| renderKVStore(storage[contractId].persistent, "FeePerShareParticular,") | ||
| %> | ||
| }) | ||
| ], | ||
| token_persistent |-> [ Balance |-> SetAsFun({ | ||
| <%- | ||
| renderKVStore(storage[storage[contractId].instance.TokenId].persistent, "Balance,", (x) => x.amount) | ||
| %> | ||
| })] | ||
| ] | ||
| IN | ||
| \* initialize the monitor non-deterministically | ||
| /\ shares \in [ USER_ADDR -> Nat ] | ||
| /\ total_shares \in Nat | ||
| /\ fee_per_share_universal \in Nat | ||
| \* initialize the contract state that we model | ||
| /\ last_tx = [ | ||
| call |-> Constructor(XYCLOANS), | ||
| status |-> TRUE, | ||
| env |-> [ | ||
| current_contract_address |-> XYCLOANS, | ||
| storage |-> init_stor, | ||
| old_storage |-> init_stor | ||
| ] | ||
| ] | ||
| /\ storage = init_stor | ||
|
|
||
| Next == | ||
| \* Generate some values for the storage. | ||
| \* For value generation, we go over all addresses, not subsets of addresses. | ||
| \E fpsu \in AMOUNTS, tid \in { "", XLM_TOKEN_SAC_TESTNET }: | ||
| \E b, mfp, fpsp, tb \in [ ADDR -> AMOUNTS ]: | ||
| LET new_stor == [ | ||
| self_instance |-> [ FeePerShareUniversal |-> fpsu, TokenId |-> tid ], | ||
| self_persistent |-> | ||
| [ Balance |-> b, MaturedFeesParticular |-> mfp, FeePerShareParticular |-> fpsp ], | ||
| token_persistent |-> [ Balance |-> tb ] | ||
| ] | ||
| env == [ | ||
| current_contract_address |-> XYCLOANS, | ||
| storage |-> new_stor, | ||
| old_storage |-> storage | ||
| ] | ||
| IN | ||
| \E addr \in USER_ADDR, amount \in AMOUNTS, success \in BOOLEAN: | ||
| /\ \/ LET tx == [ env |-> env, call |-> Initialize(XLM_TOKEN_SAC_TESTNET), status |-> success ] IN | ||
| initialize(tx) /\ last_tx' = tx | ||
| \/ LET tx == [ env |-> env, call |-> Deposit(addr, amount), status |-> success ] IN | ||
| deposit(tx) /\ last_tx' = tx | ||
| \/ LET tx == [ env |-> env, call |-> Borrow(addr, amount), status |-> success ] IN | ||
| borrow(tx) /\ last_tx' = tx | ||
| \/ LET tx == [ env |-> env, call |-> UpdateFeeRewards(addr), status |-> success ] IN | ||
| update_fee_rewards(tx) /\ last_tx' = tx | ||
| /\ storage' = IF success THEN new_stor ELSE storage | ||
|
|
||
| \* restrict the executions to the successful transactions | ||
| NextOk == | ||
| Next /\ last_tx'.status | ||
|
|
||
| \* use this falsy invariant to generate examples of successful transactions | ||
| NoSuccessInv == | ||
| ~IsConstructor(last_tx.call) => ~last_tx.status | ||
|
|
||
| \* use this view to generate better test coverage | ||
| \* apalache-mc check --max-error=10 --length=10 --inv=NoSuccessInv --view=View MCxycloans_monitor.tla | ||
| View == <<last_tx.status, VariantTag(last_tx.call)>> | ||
| ========================================================================================= |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,94 @@ | ||
| #!/usr/bin/env node | ||
| /** | ||
| * Ingest a counterexample produced by Apalache and produce the corresponding | ||
| * command for stellar-cli. | ||
| * | ||
| * In this case study, we write the script manually. In the future, this could | ||
| * be automated. Alternatively, we could execute the counterexample with | ||
| * js-stellar-sdk. However, we believe that the command line interface offers us | ||
| * more flexibility. | ||
| * | ||
| * Igor Konnov, 2024 | ||
| */ | ||
|
|
||
| const fs = require('fs') | ||
| const assert = require('assert') | ||
| const { execSync } = require('child_process') | ||
|
|
||
| network = 'testnet' | ||
|
|
||
| // Since stellar-cli does not let us sign a transaction by supplying a public key, | ||
| // we have to extract account ids. Shall we add a command to solarkraft? | ||
| function readOrFindAccounts() { | ||
| const accountsFile = 'accounts.json' | ||
| if (!fs.existsSync(accountsFile)) { | ||
| execSync('solarkraft accounts') | ||
| } | ||
| try { | ||
| return JSON.parse(fs.readFileSync(accountsFile, 'utf8')) | ||
| } catch (err) { | ||
| console.error(`Error reading ${accountsFile}: ${err.message}`) | ||
| process.exit(1) | ||
| } | ||
| } | ||
|
|
||
| // check that we have at least two arguments | ||
| const args = process.argv.slice(2) | ||
| if (args.length < 2) { | ||
| console.log('Usage: ingest.js state.json trace.json') | ||
| console.log(' state.json is the aggregated state, as produced by solarkraft aggregate') | ||
| console.log(' trace.json is the ITF trace, as produced by Apalache') | ||
| process.exit(1) | ||
| } | ||
|
|
||
| // read the state and the trace from the JSON files | ||
| let state | ||
| let trace | ||
| try { | ||
| state = JSON.parse(fs.readFileSync(args[0], 'utf8')) | ||
| trace = JSON.parse(fs.readFileSync(args[1], 'utf8')) | ||
| } catch (err) { | ||
| console.error(`Error reading the input files: ${err.message}`) | ||
| process.exit(1) | ||
| } | ||
|
|
||
| const call = trace.states[1].last_tx.call | ||
| const callType = call.tag | ||
| assert(callType !== undefined, 'traces.states[1].last_tx.call.tag is undefined') | ||
|
|
||
| const accounts = readOrFindAccounts() | ||
|
|
||
| // produce the arguments for the xycloans transaction | ||
| let signer | ||
| let callArgs | ||
| switch (callType) { | ||
| case 'Deposit': { | ||
| signer = accounts[call.value.from] | ||
| const amount = call.value.amount["#bigint"] | ||
| callArgs = `deposit --from ${call.value.from} --amount ${amount}` | ||
| break | ||
| } | ||
|
|
||
| case 'Borrow': { | ||
| signer = accounts[call.value.receiver_id] | ||
| const amount = call.value.amount["#bigint"] | ||
| callArgs = `borrow --receiver_id ${call.value.receiver_id} --amount ${amount}` | ||
| break | ||
| } | ||
|
|
||
| case 'UpdateFeeRewards': | ||
| signer = accounts[call.value.addr] | ||
| callArgs = `update_fee_rewards --addr ${signer}` | ||
| break | ||
|
|
||
| default: | ||
| console.error(`Unknown call type: ${callType}`) | ||
| process.exit(1) | ||
| } | ||
|
|
||
| assert(signer !== undefined, 'signer is undefined') | ||
|
|
||
| // produce the command for stellar-cli | ||
| const cmd = | ||
| `stellar contract invoke --id ${state.contractId} --source ${signer} --network ${network} -- ${callArgs}` | ||
| console.log(cmd) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.