Skip to content

Commit ad3d492

Browse files
shaunazzopardishaunazzopardi
committed
new use case
1 parent a944963 commit ad3d492

File tree

3 files changed

+219
-0
lines changed

3 files changed

+219
-0
lines changed

‎use-cases/WalletWithDeposit/MonitoredWalletWithDeposit.sol

Lines changed: 148 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,148 @@
1+
contract LARVA_WalletWithDeposit {
2+
modifier LARVA_Constructor {
3+
_;
4+
{
5+
LARVA_EnableContract();
6+
}
7+
}
8+
modifier LARVA_DEA_1_handle_after_assignment_history {
9+
_;
10+
if ((LARVA_STATE_1 == 0) && (history[depositProvider.wallet] != depositProvider.name)) {
11+
LARVA_STATE_1 = 5;
12+
LARVA_reparation();
13+
}
14+
}
15+
modifier LARVA_DEA_1_handle_after_assignment_depositProvider {
16+
_;
17+
if ((LARVA_STATE_1 == 0) && (owner == depositProvider.wallet)) {
18+
LARVA_STATE_1 = 4;
19+
LARVA_reparation();
20+
}
21+
}
22+
modifier LARVA_DEA_1_handle_after_assignment_deposit {
23+
_;
24+
if ((LARVA_STATE_1 == 0) && (true)) {
25+
LARVA_STATE_1 = 3;
26+
LARVA_reparation();
27+
}
28+
}
29+
modifier LARVA_DEA_1_handle_after_transfer {
30+
_;
31+
if ((LARVA_STATE_1 == 0) && (address(this).balance >= deposit)) {
32+
LARVA_STATE_1 = 2;
33+
LARVA_reparation();
34+
}
35+
}
36+
modifier LARVA_DEA_1_handle_before_end__parameters_ () {
37+
if ((LARVA_STATE_1 == 0)) {
38+
LARVA_STATE_1 = 1;
39+
}
40+
_;
41+
}
42+
int8 LARVA_STATE_1 = 0;
43+
function LARVA_set_deposit_pre (uint _deposit) LARVA_DEA_1_handle_after_assignment_deposit internal returns (uint) {
44+
LARVA_previous_deposit = deposit;
45+
deposit = _deposit;
46+
return LARVA_previous_deposit;
47+
}
48+
function LARVA_set_deposit_post (uint _deposit) LARVA_DEA_1_handle_after_assignment_deposit internal returns (uint) {
49+
LARVA_previous_deposit = deposit;
50+
deposit = _deposit;
51+
return deposit;
52+
}
53+
uint private LARVA_previous_deposit;
54+
function LARVA_set_depositProvider_pre_wallet (address payable _value) internal returns (address payable) {
55+
LARVA_previous_depositProvider = depositProvider;
56+
depositProvider.wallet = _value;
57+
return LARVA_previous_depositProvider;
58+
}
59+
function LARVA_set_depositProvider_pre_name (string _value) internal returns (string) {
60+
LARVA_previous_depositProvider = depositProvider;
61+
depositProvider.name = _value;
62+
return LARVA_previous_depositProvider;
63+
}
64+
function LARVA_set_depositProvider_pre (Provider _depositProvider) LARVA_DEA_1_handle_after_assignment_depositProvider internal returns (Provider) {
65+
LARVA_previous_depositProvider = depositProvider;
66+
depositProvider = _depositProvider;
67+
return LARVA_previous_depositProvider;
68+
}
69+
function LARVA_set_depositProvider_pre_wallet (address payable _value) internal returns (address payable) {
70+
LARVA_previous_depositProvider = depositProvider;
71+
depositProvider.wallet = _value;
72+
return depositProvider;
73+
}
74+
function LARVA_set_depositProvider_pre_name (string _value) internal returns (string) {
75+
LARVA_previous_depositProvider = depositProvider;
76+
depositProvider.name = _value;
77+
return depositProvider;
78+
}
79+
function LARVA_set_depositProvider_post (Provider _depositProvider) LARVA_DEA_1_handle_after_assignment_depositProvider internal returns (Provider) {
80+
LARVA_previous_depositProvider = depositProvider;
81+
depositProvider = _depositProvider;
82+
return depositProvider;
83+
}
84+
Provider private LARVA_previous_depositProvider;
85+
function LARVA_set_history_pre (address _index, string _history_value) LARVA_DEA_1_handle_after_assignment_history internal returns (string) {
86+
LARVA_previous_history_value = history;
87+
history[_index] = _history_value;
88+
return LARVA_previous_history;
89+
}
90+
function LARVA_set_history_post (address _index, string _history_value) LARVA_DEA_1_handle_after_assignment_history internal returns (string) {
91+
LARVA_previous_history_value = history;
92+
history[_index] = _history_value;
93+
return history;
94+
}
95+
string private LARVA_previous_history;
96+
function LARVA_transfer (address payable _to, uint amount) LARVA_DEA_1_handle_after_transfer internal {
97+
LARVA_set_history_pre(_to, amount);
98+
}
99+
function LARVA_reparation () private {
100+
revert();
101+
}
102+
enum LARVA_STATUS {RUNNING, STOPPED}
103+
function LARVA_EnableContract () private {
104+
LARVA_Status = LARVA_STATUS.RUNNING;
105+
}
106+
function LARVA_DisableContract () private {
107+
LARVA_Status = LARVA_STATUS.STOPPED;
108+
}
109+
LARVA_STATUS private LARVA_Status = LARVA_STATUS.STOPPED;
110+
modifier LARVA_ContractIsEnabled {
111+
require(LARVA_Status == LARVA_STATUS.RUNNING);
112+
_;
113+
}
114+
uint private deposit;
115+
address payable owner;
116+
struct Provider {
117+
address payable wallet;
118+
string name;
119+
}
120+
Provider private depositProvider;
121+
mapping (address => string) private history;
122+
modifier iss (address _owner) {
123+
require(msg.sender == _owner);
124+
_;
125+
}
126+
constructor (string memory name, address payable _depositProvider) LARVA_Constructor payable {
127+
require(msg.value > 0, "Must be started with a deposit.");
128+
(owner, deposit) = ((payable(msg.sender), msg.value));
129+
depositProvider = Provider(_depositProvider, name);
130+
history[_depositProvider] = name;
131+
}
132+
function transfer (address payable to, uint tokens) LARVA_ContractIsEnabled iss(owner) external returns (bool success) {
133+
LARVA_transfer(to, tokens);
134+
}
135+
function changeOwnerAndDepositProvider (address payable _owner, string memory name, address payable _depositProvider) LARVA_ContractIsEnabled external iss(_depositProvider) returns (bool success) {
136+
{
137+
Provider depositProvider_LARVA;
138+
(owner, depositProvider_LARVA) = ((_owner, Provider(_depositProvider, name)));
139+
LARVA_set_depositProvider_post(depositProvider_LARVA);
140+
}
141+
LARVA_set_history_post(_depositProvider, name);
142+
}
143+
function end () LARVA_DEA_1_handle_before_end__parameters_ LARVA_ContractIsEnabled external iss(owner) returns (bool success) {
144+
LARVA_transfer(depositProvider.wallet, deposit);
145+
selfdestruct(owner);
146+
}
147+
148+
}

‎use-cases/WalletWithDeposit/WalletWithDeposit.sol

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
contract WalletWithDeposit{
2+
3+
uint deposit;
4+
address payable owner;
5+
struct Provider {
6+
address payable wallet;
7+
string name;
8+
}
9+
10+
Provider depositProvider;
11+
mapping(address => string) history;
12+
13+
modifier iss(address _owner) {
14+
require(msg.sender == _owner);
15+
_;
16+
}
17+
18+
constructor(string memory name, address payable _depositProvider) payable {
19+
require(msg.value > 0, "Must be started with a deposit.");
20+
(owner, deposit) = (payable(msg.sender), msg.value);
21+
depositProvider = Provider(_depositProvider, name);
22+
history[_depositProvider] = name;
23+
}
24+
25+
function transfer(address payable to, uint tokens) iss(owner) external returns (bool success){
26+
to.transfer(tokens);
27+
}
28+
29+
function changeOwnerAndDepositProvider (address payable _owner, string memory name, address payable _depositProvider) external iss(_depositProvider) returns (bool success){
30+
(owner, depositProvider) = (_owner, Provider(_depositProvider, name));
31+
history[_depositProvider] = name;
32+
}
33+
34+
function end () external iss(owner) returns (bool success){
35+
depositProvider.wallet.transfer(deposit);
36+
selfdestruct(owner);
37+
}
38+
}

‎use-cases/WalletWithDeposit/WalletWithDepositSpec.dea

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
monitor WalletWithDeposit{
2+
3+
declarations{
4+
}
5+
6+
initialisation{
7+
LARVA_EnableContract();
8+
}
9+
10+
reparation{
11+
revert();
12+
}
13+
14+
DEA ProtectedDeposit{
15+
states{
16+
Start: initial;
17+
Ending;
18+
LessThanDeposit: bad;
19+
DepositModified: bad;
20+
OwnerIsSameAsDepositProvider: bad;
21+
BadHistoryModification: bad;
22+
}
23+
24+
transitions{
25+
Start -[aftertransfer | address(this).balance >= deposit]-> LessThanDeposit;
26+
Start -[deposit@(true)]-> DepositModified;
27+
Start -[depositProvider@(owner == depositProvider.wallet)]-> OwnerIsSameAsDepositProvider;
28+
Start -[history@(history[depositProvider.wallet] != depositProvider.name)]-> BadHistoryModification;
29+
Start -[before(end())]-> Ending;
30+
}
31+
}
32+
33+
}

0 commit comments

Comments
 (0)