Skip to content

Commit 60f76a6

Browse files
konnovkonnov
authored
Merge pull request #156 from freespek/igor/generate-tla
An EJS template to populate the TLA+ spec of xycloans
2 parents de1d92f + 45a5e31 commit 60f76a6

11 files changed

Lines changed: 349 additions & 30 deletions

File tree

‎ContractExamples/contracts/alert/src/test.rs‎

Lines changed: 14 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -7,33 +7,41 @@ use soroban_sdk::{
77
};
88

99
#[test]
10-
fn test() {
10+
fn test_ok() {
1111
let env = Env::default();
1212
let tx_hash: String = String::from_str(&env, "txhash");
1313

14-
let contract_id = env.register_contract(None, Alert);
14+
let contract_id = env.register(Alert, ());
1515
// <X>Client is automagically created.
1616
let client = AlertClient::new(&env, &contract_id);
1717

18-
1918
assert_eq!(client.emit_and_store_violation(&tx_hash, &VerificationStatus::NoViolation), VerificationStatus::NoViolation);
2019
// NoViolation triggers an emit but no store
2120
assert_eq!(
2221
env.events().all(),
23-
vec![&env, (contract_id.clone(),(ALERTS, OK).into_val(&env),VerificationStatus::NoViolation.into_val(&env))]
22+
vec![&env, (contract_id.clone(),(ALERTS, OK).into_val(&env), VerificationStatus::NoViolation.into_val(&env))]
2423
);
2524

2625
// should be empty
2726
let alerts = client.alerts();
2827
assert!(alerts.is_empty());
28+
}
29+
30+
#[test]
31+
fn test_violation() {
32+
let env = Env::default();
33+
let tx_hash: String = String::from_str(&env, "txhash");
34+
35+
let contract_id = env.register(Alert, ());
36+
// <X>Client is automagically created.
37+
let client = AlertClient::new(&env, &contract_id);
2938

3039
// Violation triggers an emit and a store
3140
assert_eq!(client.emit_and_store_violation(&tx_hash, &VerificationStatus::Violation), VerificationStatus::Violation);
3241
assert_eq!(
3342
env.events().all(),
3443
vec![&env,
35-
(contract_id.clone(),(ALERTS, OK).into_val(&env),VerificationStatus::NoViolation.into_val(&env)),
36-
(contract_id.clone(),(ALERTS, VIOLATION).into_val(&env),VerificationStatus::Violation.into_val(&env))
44+
(contract_id.clone(),(ALERTS, VIOLATION).into_val(&env), VerificationStatus::Violation.into_val(&env))
3745
]
3846
);
3947

‎ContractExamples/contracts/megacontract/src/test.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ fn test() {
1313
let env = Env::default();
1414
let addr = Address::generate(&env);
1515

16-
let contract_id = env.register_contract(None, MegaContract);
16+
let contract_id = env.register(MegaContract, ());
1717
// <X>Client is automagically created.
1818
let client = MegaContractClient::new(&env, &contract_id);
1919

‎ContractExamples/contracts/setter/src/test.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ fn test() {
2121
let env = Env::default();
2222
let addr = Address::generate(&env);
2323

24-
let contract_id = env.register_contract(None, SetterContract);
24+
let contract_id = env.register(SetterContract, ());
2525
// <X>Client is automagically created.
2626
let client = SetterContractClient::new(&env, &contract_id);
2727

‎doc/case-studies/xycloans/MCxycloans_monitor.ejs.tla‎

Lines changed: 168 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,168 @@
1+
------------------------------- MODULE MC -------------------------------
2+
<%#
3+
/*
4+
* An EJS template for generating the initial state from the aggregated state of the contract.
5+
*
6+
* Usage:
7+
*
8+
* npx ejs MCxycloans_monitor.ejs.tla -f state.json >MC.tla
9+
*
10+
* Igor Konnov, 2024
11+
*/
12+
%>
13+
(* THIS MODULE IS AUTOGENERATED FROM SOROBAN STATE *)
14+
EXTENDS Integers, Apalache, xycloans_types
15+
16+
\* the set of all possible token amounts
17+
AMOUNTS == Nat
18+
\* the contract address for the xycLoans contract
19+
XYCLOANS == "<%- contractId %>"
20+
\* the token address
21+
XLM_TOKEN_SAC_TESTNET == "<%- storage[contractId].instance.TokenId %>"
22+
23+
<%
24+
const balanceAddrs =
25+
Object.keys(storage[contractId].persistent)
26+
.filter((key) => key.startsWith("Balance,"))
27+
.map((key) => key.split(",")[1])
28+
%>
29+
\* user-controlled addresses
30+
USER_ADDR == {
31+
<%-
32+
balanceAddrs
33+
.map((addr) => ` "${addr}"`)
34+
.join(",\n")
35+
%>
36+
}
37+
38+
<%
39+
const tokenAddrs =
40+
Object.keys(storage[storage[contractId].instance.TokenId].persistent)
41+
.filter((key) => key.startsWith("Balance,"))
42+
.filter((key) => key !== `Balance,${contractId}`)
43+
.map((key) => key.split(",")[1])
44+
%>
45+
\* addresses that hold token balances
46+
TOKEN_ADDR == {
47+
<%-
48+
tokenAddrs
49+
.map((addr) => ` "${addr}"`)
50+
.join(",\n")
51+
%>
52+
}
53+
54+
\* the pool of addresses to draw the values from
55+
ADDR == { XYCLOANS, XLM_TOKEN_SAC_TESTNET } \union TOKEN_ADDR \union USER_ADDR
56+
57+
VARIABLES
58+
\* @type: $tx;
59+
last_tx,
60+
\* @type: Str -> Int;
61+
shares,
62+
\* @type: Int;
63+
total_shares,
64+
\* @type: Int;
65+
fee_per_share_universal,
66+
\* Keep track of the current storage,
67+
\* which can be only changed by a successful transaction.
68+
\* @type: $storage;
69+
storage
70+
71+
INSTANCE xycloans_monitor
72+
73+
<%
74+
function renderKVStore(storage, prefix, mapper = (x) => x) {
75+
return Object.keys(storage)
76+
.filter((key) => key.startsWith(prefix))
77+
.map((key) => key.split(",")[1])
78+
.map((addr) => ` <<"${addr}", ${mapper(storage[prefix + addr])}>>`)
79+
.join(",\n")
80+
}
81+
%>
82+
83+
Init ==
84+
LET init_stor == [
85+
self_instance |-> [
86+
FeePerShareUniversal |-> <%- storage[contractId].instance.FeePerShareUniversal %>,
87+
TokenId |-> "<%- storage[contractId].instance.TokenId %>"
88+
],
89+
self_persistent |-> [
90+
Balance |-> SetAsFun({
91+
<%-
92+
renderKVStore(storage[contractId].persistent, "Balance,")
93+
%>
94+
}),
95+
MaturedFeesParticular |-> SetAsFun({
96+
<%-
97+
renderKVStore(storage[contractId].persistent, "MaturedFeesParticular,")
98+
%>
99+
}),
100+
FeePerShareParticular |-> SetAsFun({
101+
<%-
102+
renderKVStore(storage[contractId].persistent, "FeePerShareParticular,")
103+
%>
104+
})
105+
],
106+
token_persistent |-> [ Balance |-> SetAsFun({
107+
<%-
108+
renderKVStore(storage[storage[contractId].instance.TokenId].persistent, "Balance,", (x) => x.amount)
109+
%>
110+
})]
111+
]
112+
IN
113+
\* initialize the monitor non-deterministically
114+
/\ shares \in [ USER_ADDR -> Nat ]
115+
/\ total_shares \in Nat
116+
/\ fee_per_share_universal \in Nat
117+
\* initialize the contract state that we model
118+
/\ last_tx = [
119+
call |-> Constructor(XYCLOANS),
120+
status |-> TRUE,
121+
env |-> [
122+
current_contract_address |-> XYCLOANS,
123+
storage |-> init_stor,
124+
old_storage |-> init_stor
125+
]
126+
]
127+
/\ storage = init_stor
128+
129+
Next ==
130+
\* Generate some values for the storage.
131+
\* For value generation, we go over all addresses, not subsets of addresses.
132+
\E fpsu \in AMOUNTS, tid \in { "", XLM_TOKEN_SAC_TESTNET }:
133+
\E b, mfp, fpsp, tb \in [ ADDR -> AMOUNTS ]:
134+
LET new_stor == [
135+
self_instance |-> [ FeePerShareUniversal |-> fpsu, TokenId |-> tid ],
136+
self_persistent |->
137+
[ Balance |-> b, MaturedFeesParticular |-> mfp, FeePerShareParticular |-> fpsp ],
138+
token_persistent |-> [ Balance |-> tb ]
139+
]
140+
env == [
141+
current_contract_address |-> XYCLOANS,
142+
storage |-> new_stor,
143+
old_storage |-> storage
144+
]
145+
IN
146+
\E addr \in USER_ADDR, amount \in AMOUNTS, success \in BOOLEAN:
147+
/\ \/ LET tx == [ env |-> env, call |-> Initialize(XLM_TOKEN_SAC_TESTNET), status |-> success ] IN
148+
initialize(tx) /\ last_tx' = tx
149+
\/ LET tx == [ env |-> env, call |-> Deposit(addr, amount), status |-> success ] IN
150+
deposit(tx) /\ last_tx' = tx
151+
\/ LET tx == [ env |-> env, call |-> Borrow(addr, amount), status |-> success ] IN
152+
borrow(tx) /\ last_tx' = tx
153+
\/ LET tx == [ env |-> env, call |-> UpdateFeeRewards(addr), status |-> success ] IN
154+
update_fee_rewards(tx) /\ last_tx' = tx
155+
/\ storage' = IF success THEN new_stor ELSE storage
156+
157+
\* restrict the executions to the successful transactions
158+
NextOk ==
159+
Next /\ last_tx'.status
160+
161+
\* use this falsy invariant to generate examples of successful transactions
162+
NoSuccessInv ==
163+
~IsConstructor(last_tx.call) => ~last_tx.status
164+
165+
\* use this view to generate better test coverage
166+
\* apalache-mc check --max-error=10 --length=10 --inv=NoSuccessInv --view=View MCxycloans_monitor.tla
167+
View == <<last_tx.status, VariantTag(last_tx.call)>>
168+
=========================================================================================

‎doc/case-studies/xycloans/ingest.js‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
#!/usr/bin/env node
2+
/**
3+
* Ingest a counterexample produced by Apalache and produce the corresponding
4+
* command for stellar-cli.
5+
*
6+
* In this case study, we write the script manually. In the future, this could
7+
* be automated. Alternatively, we could execute the counterexample with
8+
* js-stellar-sdk. However, we believe that the command line interface offers us
9+
* more flexibility.
10+
*
11+
* Igor Konnov, 2024
12+
*/
13+
14+
const fs = require('fs')
15+
const assert = require('assert')
16+
const { execSync } = require('child_process')
17+
18+
network = 'testnet'
19+
20+
// Since stellar-cli does not let us sign a transaction by supplying a public key,
21+
// we have to extract account ids. Shall we add a command to solarkraft?
22+
function readOrFindAccounts() {
23+
const accountsFile = 'accounts.json'
24+
if (!fs.existsSync(accountsFile)) {
25+
execSync('solarkraft accounts')
26+
}
27+
try {
28+
return JSON.parse(fs.readFileSync(accountsFile, 'utf8'))
29+
} catch (err) {
30+
console.error(`Error reading ${accountsFile}: ${err.message}`)
31+
process.exit(1)
32+
}
33+
}
34+
35+
// check that we have at least two arguments
36+
const args = process.argv.slice(2)
37+
if (args.length < 2) {
38+
console.log('Usage: ingest.js state.json trace.json')
39+
console.log(' state.json is the aggregated state, as produced by solarkraft aggregate')
40+
console.log(' trace.json is the ITF trace, as produced by Apalache')
41+
process.exit(1)
42+
}
43+
44+
// read the state and the trace from the JSON files
45+
let state
46+
let trace
47+
try {
48+
state = JSON.parse(fs.readFileSync(args[0], 'utf8'))
49+
trace = JSON.parse(fs.readFileSync(args[1], 'utf8'))
50+
} catch (err) {
51+
console.error(`Error reading the input files: ${err.message}`)
52+
process.exit(1)
53+
}
54+
55+
const call = trace.states[1].last_tx.call
56+
const callType = call.tag
57+
assert(callType !== undefined, 'traces.states[1].last_tx.call.tag is undefined')
58+
59+
const accounts = readOrFindAccounts()
60+
61+
// produce the arguments for the xycloans transaction
62+
let signer
63+
let callArgs
64+
switch (callType) {
65+
case 'Deposit': {
66+
signer = accounts[call.value.from]
67+
const amount = call.value.amount["#bigint"]
68+
callArgs = `deposit --from ${call.value.from} --amount ${amount}`
69+
break
70+
}
71+
72+
case 'Borrow': {
73+
signer = accounts[call.value.receiver_id]
74+
const amount = call.value.amount["#bigint"]
75+
callArgs = `borrow --receiver_id ${call.value.receiver_id} --amount ${amount}`
76+
break
77+
}
78+
79+
case 'UpdateFeeRewards':
80+
signer = accounts[call.value.addr]
81+
callArgs = `update_fee_rewards --addr ${signer}`
82+
break
83+
84+
default:
85+
console.error(`Unknown call type: ${callType}`)
86+
process.exit(1)
87+
}
88+
89+
assert(signer !== undefined, 'signer is undefined')
90+
91+
// produce the command for stellar-cli
92+
const cmd =
93+
`stellar contract invoke --id ${state.contractId} --source ${signer} --network ${network} -- ${callArgs}`
94+
console.log(cmd)

‎doc/case-studies/xycloans/xycloans_monitor.tla‎

Lines changed: 11 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ initialize(tx) ==
7070
\* @type: $tx => Bool;
7171
deposit(tx) ==
7272
LET call == AsDeposit(tx.call)
73-
token == tx.env.storage.self_instance.TokenId
73+
token == tx.env.old_storage.self_instance.TokenId
7474
new_shares == [ shares EXCEPT ![call.from] = @ + call.amount ]
7575
IN
7676
/\ IsDeposit(tx.call)
@@ -86,9 +86,10 @@ deposit(tx) ==
8686
\* these conditions are not required by a monitor, but needed to avoid spurious generated values
8787
/\ succeeds_with(tx,
8888
\A other \in DOMAIN tx.env.storage.self_persistent.Balance \ {call.from}:
89-
/\ other \in DOMAIN tx.env.old_storage.self_persistent.Balance
90-
/\ tx.env.storage.self_persistent.Balance[other] = tx.env.old_storage.self_persistent.Balance[other])
89+
other \in DOMAIN tx.env.old_storage.self_persistent.Balance
90+
=> tx.env.storage.self_persistent.Balance[other] = tx.env.old_storage.self_persistent.Balance[other])
9191
/\ succeeds_with(tx, call.amount > 0)
92+
/\ succeeds_with(tx, tx.env.storage.self_instance.TokenId = token)
9293
\* update the monitor state
9394
/\ shares' = new_shares
9495
/\ total_shares' = total_shares + call.amount
@@ -97,6 +98,7 @@ deposit(tx) ==
9798
\* @type: $tx => Bool;
9899
borrow(tx) ==
99100
LET call == AsBorrow(tx.call)
101+
token == tx.env.old_storage.self_instance.TokenId
100102
expected_fee == div_ceil(call.amount * STROOP, 12500000000)
101103
expected_fee_per_share_universal ==
102104
tx.env.old_storage.self_instance.FeePerShareUniversal
@@ -113,8 +115,9 @@ borrow(tx) ==
113115
/\ succeeds_with(tx, token_balance(tx.env, rcvr) = old_token_balance(tx.env, rcvr) - call.amount)
114116
/\ succeeds_with(tx, token_balance(tx.env, self) = old_token_balance(tx.env, self) + call.amount)
115117
\* these conditions are not required by a monitor, but needed to avoid spurious generated values
116-
/\ succeeds_with(tx, tx.env.storage.self_persistent = tx.env.old_storage.self_persistent)
118+
\*/\ succeeds_with(tx, tx.env.storage.self_persistent = tx.env.old_storage.self_persistent)
117119
/\ succeeds_with(tx, call.amount > 0)
120+
/\ succeeds_with(tx, tx.env.storage.self_instance.TokenId = token)
118121
\* update the monitor state
119122
\* we update the fee per share to compute rewards later
120123
/\ fee_per_share_universal' = expected_fee_per_share_universal
@@ -123,6 +126,7 @@ borrow(tx) ==
123126
\* @type: $tx => Bool;
124127
update_fee_rewards(tx) ==
125128
LET call == AsUpdateFeeRewards(tx.call)
129+
token == tx.env.old_storage.self_instance.TokenId
126130
fees_not_yet_considered ==
127131
fee_per_share_universal - get_or_else(tx.env.old_storage.self_persistent.FeePerShareParticular, call.addr, 0)
128132
expected_reward == div_floor(get_or_else(shares, call.addr, 0) * fees_not_yet_considered, STROOP)
@@ -137,8 +141,9 @@ update_fee_rewards(tx) ==
137141
\* delta of matured rewards for `addr` have been added
138142
/\ expected_reward = actual_reward
139143
\* these conditions are not required by a monitor, but needed to avoid spurious generated values
140-
/\ succeeds_with(tx,
141-
tx.env.storage.self_persistent.Balance = tx.env.old_storage.self_persistent.Balance)
144+
\*/\ succeeds_with(tx,
145+
\* tx.env.storage.self_persistent.Balance = tx.env.old_storage.self_persistent.Balance)
146+
/\ succeeds_with(tx, tx.env.storage.self_instance.TokenId = token)
142147
\* update the monitor state
143148
/\ UNCHANGED <<shares, total_shares, fee_per_share_universal>>
144149

0 commit comments

Comments
 (0)