ABCDEFGHIJKLMNOPQRSTUVWXYZAAABACADAEAFAG
1
Property nameProperty descriptionProperty typeNote on property typeExpected truth
(Solidity)		Note on expected output (Solidity)Certora
output		Note on Certora
spec & output		Expected truth (Move)Note on expected output
(Move)		Move Prover
output		Note on Move Prover
spec & output
2
assets-dec-onlyif-depositif the assets of a user A are decreased after a transaction (of the Bank contract), then that transaction must be a deposit where A is the senderlinear propertysingle-transition invariant1true, up-to transaction fees. Note that, if we also consider fees, the property is false: e.g., if A withdraws a tiny amount, higher than the gas fees. Both Certora and SolCMC seem to ignore fees0spec uses call to a generic method

verification fails because of havoc on transfer. The detailed output Certora shows that it is unsound wrt gas		1true, up-to transaction fees. Note that, if we also consider fees, the property is false.1function specs of the contrapositive: for every transaction that is not a deposit, or for which A is not the sender, the spec checks that the assets of A are not decreased
3
assets-inc-onlyif-withdrawif the assets of a user A are increased after a transaction (of the Bank contract), then that transaction must be a withdraw where A is the senderlinear propertysingle-transition invariant1the property holds because the only way for A to receive ETH is through the transfer in withdraw(). If a low-level call were used instead, it would have been possible for the receiver's fallback to forward the incoming ETH to another address, violating the property0spec uses call to a generic method

verification fails because of havoc on transfer		11function specs of the contrapositive
4
credit-dec-onlyif-withdrawif the credit of a user A is decreased after a transaction (of the Bank contract), then that transaction must be a withdraw where A is the senderlinear propertysingle-transition invariant11spec uses call to a generic method

In order to make verification succeed, the spec must additionally require that the contract is not the sender, even if this cannot happen in practice		11function specs of the contrapositive
5
credit-inc-onlyif-depositif the credit of a user A is increased after a transaction (of the Bank contract), then that transaction must be a deposit where A is the senderlinear propertysingle-transition invariant11spec uses call to a generic method

In order to make verification succeed, the spec must additionally require that the contract is not the sender, even if this cannot happen in practice		11function specs of the contrapositive
6
credits-leq-balancethe assets controlled by the contract are (at least) equal to the sum of all the credits.state invariant1the property holds (not that it would not hold by using eq instead of leq, because of coinbase and selfdestruct transactions)0spec uses hooks and ghost variables.

verification fails (inductive invariant not strong enough?)		1in the Move implementation, credits are modelled as resources, therefore the property is trivially enforced by the Move languageN/A
7
deposit-additivitytwo consecutive successful deposits of n1 and n2 token units performed by the same sender are equivalent to a single deposit of n1+n2 token units, if n1+n2 is less than or equal to the sender’s operation limitbranching propertymetamorphic property1true, up-to transaction fees1spec checks equality of contract storages, using lastStorage. Although docs (https://docs.certora.com/en/latest/docs/cvl/expr.html#comparing-storage) state that equality is checked on contract balances, from the experiments it seems that also users' balances are checked1N/Dthe Move Prover does not admit specs that involve over multiple calls
8
deposit-assets-creditafter a successful deposit(amount), the users’ credit is increased by exactly amount units of Tfunction specpostcondition111in the Move implementation, credits are modelled as resources. Therefore, this property is implied by deposit-assets-transfer1
9
deposit-assets-credit-othersafter a successful deposit(amount), the credits of any user but the sender are preservedfunction specpostcondition11spec uses implicit universal quantification on CVL variables11
10
deposit-assets-transferafter a successful deposit(amount), exactly amount token units pass from the control of the sender to that of the contractfunction specpostcondition11require that sender is not the contract11
11
deposit-assets-transfer-othersafter a successful deposit(amount), the assets controlled by any user but the sender are preservedfunction specpostcondition11spec uses implicit universal quantification on CVL variables

In order to make verification succeed, the spec must additionally require that the contract is not A, even if this cannot happen in practice		11Uses the forall spec
12
deposit-not-reverta transaction deposit(amount) does not abort if amount is less than or equal to the transaction sender’s T balance and operation limitfunction specsuccess condition1not needed to check for overflow, since there is not enough ETH to produce an overflow1no overflow check needed1!coin_store.frozen1Require no overflow
13
deposit-reversibilitythe effect of a deposit(amount) is reverted by an immediately subsequent withdraw(amount)linear propertymultiple-transition invariants0false, when the sender is a contract with a failing fallback/receive. In that case, the deposit succeeds but the withdraw fails.01the property should be true (need to assume that the sender can receive coins?)N/Dthe Move Prover does not admit specs that involve over multiple calls
14
deposit-reverta transaction deposit(amount) aborts if amount is greater than the transaction sender’s T balance or operation limitfunction specsuccess condition111aborts also if !features::spec_is_enabled(features::COIN_TO_FUNGIBLE_ASSET_MIGRATION)1spec uses "pragma aborts_if_is_partial", since there could be other causes for the abort
15
exists-at-least-one-credit-changeafter a successful transaction, the credits of at least one account have changedlinear propertysingle-transition invariant1this property is true, because the transfer() does not carry enough gas for further callsN/Dspec not expressible in CVL: mix of forall / exists quantifiers11global invariant with forall / exists
16
exists-unique-asset-changeafter a successful transaction, the assets of exactly one account (except the contract’s) have changedlinear propertysingle-transition invariant1this property is true, because the transfer() does not carry enough gas for further callsN/Dspec not expressible in CVL: mix of forall / exists quantifiers1push0verification fails unexpectedly
17
exists-unique-credit-changeafter a successful transaction, the credits of exactly one account have changedlinear propertysingle-transition invariant1this property is true, because the transfer() does not carry enough gas for further callsN/Dspec not expressible in CVL: mix of forall / exists quantifiers11global invariant with forall / exists
18
no-frozen-assetsif the contract controls some assets, then someone can transfer them from the contract to some other user (in one or more transactions)branching propertyliquidity0the property is false, since the contract balance could be higher than credits (this is possible through coinbase or selfdestruct transactions). This extra budget cannot be withdrawn from the contractN/Dnote that satisfy rules are not a faithful specification of this property, since, e.g., they also take unreachable states into account1the property should be true, since there are no ways to inject untracked tokens into the contractN/D
19
no-frozen-creditsif some user has strictly positive credits, then they can transfer them from the contract to some other user (in one or more transactions)branching propertyliquidity1N/Dnote that satisfy rules are not a faithful specification of this property, since, e.g., they also take unreachable states into account1the property should be true, since there are no ways to inject untracked tokens into the contractN/D
20
oplimit-immutablethe operation limit never changesstate invariant1keyword "immutable" makes the property enforced by the compilerN/A11invariant update [global]
21
owner-immutablethe owner never changesstate invariant1keyword "immutable" makes the property enforced by the compilerN/A1the address associated with the contract is set by the move_to in the init() function, and never changed after thenN/Dit seems that there is no way of reasoning about resource movements in the spec language
22
withdraw-additivitytwo consecutive successful withdraw of n1 and n2 token units (performed by the same sender) are equivalent to a single withdraw of n1+n2 token units, if n1+n2 is less than or equal to the sender’s operation limitbranching propertymetamorphic property1no reentrancy, since the withdraw implementation uses the transfer method (not enough gas for reentrancy)1spec checks equality of contract storages, using lastStorage. Although docs (https://docs.certora.com/en/latest/docs/cvl/expr.html#comparing-storage) state that equality is checked on contract balances, from the experiments it seems that also users' balances are checked1N/Dthe Move Prover does not admit specs that involve over multiple calls
23
withdraw-assets-creditafter a successful withdraw(amount), the users’ credit is decreased by exactly amount units of T.function specpostcondition111in the Move implementation, credits are modelled as resources. Therefore, this property is implied by withdraw-assets-transfer1
24
withdraw-assets-credit-othersafter a successful withdraw(amount), the credits of any user but the sender are preserved.function specpostcondition11spec uses implicit universal quantification on CVL variables11spec uses forall
25
withdraw-assets-transferafter a successful withdraw(amount), exactly amount units of T pass from the control of the contract to that of the sender.function specpostcondition1transfer() does not have enough gas to allow the receiver to perform further transfers0havoc on transfer(). The verifier does not seem to use the assumption that transfer() does not have enough gas to perform other calls1requires !features::spec_is_enabled(features::COIN_TO_FUNGIBLE_ASSET_MIGRATION)1
26
withdraw-assets-transfer-eoaafter a successful withdraw(amount) performed by an EOA, exactly amount units of T pass from the control of the contract to that of the sender.function specpostcondition1the sender is an EOA, it always accepts the transfer01equal to withdraw-assets-transfer
27
withdraw-assets-transfer-othersafter a successful withdraw(amount), the assets controlled by any user but the sender are preserved.function specpostcondition1the property holds because transfer() does not have enough gas to allow the receiver to perform further calls (no reentrancy)0spec uses implicit universal quantification on CVL variables

verification fails because of havoc on transfer() 		11
28
withdraw-not-reverta transaction withdraw(amount) does not abort if amount is less or equal to the transaction sender’s credit and operation limit.function specsuccess condition0the property is false: withdraw() reverts, e.g., if the sender is a contract whose receive function fails)01requires !coin_store.frozen1
29
withdraw-reverta transaction withdraw(amount) aborts if amount is greater than the transaction sender’s credit or operation limit.function specsuccess condition1111spec uses "pragma aborts_if_is_partial", since there could be other causes for the abort
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100