Repository navigation
Expand file tree
/
Copy pathLocalBlockchainTests.v
More file actions
220 lines (184 loc) · 8.23 KB
/
Copy pathLocalBlockchainTests.v
File metadata and controls
220 lines (184 loc) · 8.23 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
(* This file computes with the Congress and an actual blockchain
implementation, showing that everything computes from within Rocq. It
also contains specializations of the results proven in Congress.v to
our particular implementations of blockchains. *)
From ConCert.Utils Require Import Automation.
From ConCert.Execution Require Import Monad.
From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import Containers.
From ConCert.Execution Require Import BoundedN.
From ConCert.Execution Require Import ResultMonad.
From ConCert.Execution Require Import Serializable.
From ConCert.Execution.Test Require Import LocalBlockchain.
From ConCert.Examples.Congress Require Import Congress.
From ConCert.Examples.Congress Require Import CongressCorrect.
From Stdlib Require Import List. Import ListNotations.
From Stdlib Require Import ZArith.
Section LocalBlockchainTests.
Let AddrSize := (2^128)%N.
Instance Base : ChainBase := LocalChainBase AddrSize.
Instance ChainBuilder : ChainBuilderType := LocalChainBuilderImpl AddrSize true.
(* Addresses *)
Definition creator : Address :=
BoundedN.of_Z_const AddrSize 10.
Definition person_1 : Address :=
BoundedN.of_Z_const AddrSize 11.
Definition person_2 : Address :=
BoundedN.of_Z_const AddrSize 12.
Definition person_3 : Address :=
BoundedN.of_Z_const AddrSize 13.
Definition chain1 : ChainBuilder := builder_initial.
Definition add_block (chain : ChainBuilder) acts : result ChainBuilder AddBlockError :=
let header :=
{| block_height := S (chain_height chain);
block_slot := S (current_slot chain);
block_finalized_height := finalized_height chain;
block_creator := creator;
block_reward := 50; |} in
builder_add_block chain header acts.
(* Creator created an empty block (and gets some coins) *)
Definition chain2 : ChainBuilder :=
unpack_result (add_block chain1 []).
Goal (env_account_balances chain2 person_1) = 0%Z.
Proof. vm_compute. reflexivity. Qed.
Goal (env_account_balances chain2 creator) = 50%Z.
Proof. vm_compute. reflexivity. Qed.
(* Creator transfers 10 coins to person_1 *)
Definition chain3 : ChainBuilder :=
unpack_result (add_block chain2 [build_act creator creator (act_transfer person_1 10)]).
Goal (env_account_balances chain3 person_1) = 10%Z.
Proof. vm_compute. reflexivity. Qed.
Goal (env_account_balances chain3 creator) = 90%Z.
Proof. vm_compute. reflexivity. Qed.
(* person_1 deploys a Congress contract *)
Definition setup_rules :=
{| min_vote_count_permille := 200; (* 20% of congress needs to vote *)
margin_needed_permille := 501;
debating_period_in_blocks := 0;
|}.
Definition setup := Congress.build_setup setup_rules.
Definition deploy_congress : ActionBody :=
create_deployment 5 Congress.contract setup.
Definition chain4 : ChainBuilder :=
unpack_result (add_block chain3 [build_act person_1 person_1 deploy_congress]).
Definition congress_1 : Address :=
match outgoing_txs (builder_trace chain4) person_1 with
| tx :: _ => tx_to tx
| _ => person_1
end.
Goal (env_account_balances chain4 person_1) = 5%Z.
Proof. vm_compute. reflexivity. Qed.
Goal (env_account_balances chain4 creator) = 140%Z.
Proof. vm_compute. reflexivity. Qed.
Goal (env_account_balances chain4 congress_1) = 5%Z.
Proof. vm_compute. reflexivity. Qed.
Definition congress_ifc : ContractInterface Congress.Msg :=
match get_contract_interface chain4 congress_1 Congress.Msg with
| Some x => x
(* Using unpack_option here is extremely slow *)
| None =>
@build_contract_interface
_ _
creator
(fun a m => deploy_congress)
end.
Definition congress_state lc : Congress.State :=
match env_contract_states lc congress_1 >>= deserialize with
| Some s => s
(* And also here *)
| None => {| owner := creator;
state_rules := setup_rules;
proposals := FMap.empty;
next_proposal_id := 0;
members := FMap.empty |}
end.
Goal (congress_state chain4) = {|
owner := person_1;
state_rules := {|
min_vote_count_permille := 200;
margin_needed_permille := 501;
debating_period_in_blocks := 0
|};
proposals := FMap.empty;
next_proposal_id := 1;
members := FMap.empty
|}.
Proof. vm_compute. reflexivity. Qed.
Goal (FMap.elements (congress_state chain4).(members)) = [].
Proof. vm_compute. reflexivity. Qed.
(* person_1 adds person_1 and person_2 as members of congress *)
Definition add_person p :=
congress_ifc.(send) 0 (Some (add_member p)).
Definition chain5 : ChainBuilder :=
let acts := [build_act person_1 person_1 (add_person person_1);
build_act person_1 person_1 (add_person person_2)] in
unpack_result (add_block chain4 acts).
Goal Permutation.Permutation (FMap.elements (congress_state chain5).(members)) [(person_1, tt); (person_2, tt)].
Proof. vm_compute. perm_simplify. Qed.
Goal (env_account_balances chain5 congress_1) = 5%Z.
Proof. vm_compute. reflexivity. Qed.
(* person_1 creates a proposal to send 3 coins to person_3 using funds
of the contract *)
Definition create_proposal_call :=
congress_ifc.(send) 0 (Some (create_proposal [cact_transfer person_3 3])).
Definition chain6 : ChainBuilder :=
unpack_result (add_block chain5 [build_act person_1 person_1 create_proposal_call]).
Goal (FMap.elements (congress_state chain6).(proposals)) =
[(1, {|
actions := [cact_transfer person_3 3];
votes := FMap.empty;
vote_result := 0;
proposed_in := 5 |})].
Proof. vm_compute. reflexivity. Qed.
(* person_1 and person_2 vote for the proposal *)
Definition vote_proposal :=
congress_ifc.(send) 0 (Some (vote_for_proposal 1)).
Definition chain7 : ChainBuilder :=
let acts := [build_act person_1 person_1 vote_proposal;
build_act person_2 person_2 vote_proposal] in
unpack_result (add_block chain6 acts).
Goal (match FMap.find 1 (congress_state chain7).(proposals) with Some x => x.(vote_result) | None => 0%Z end) = 2%Z.
Proof. vm_compute. reflexivity. Qed.
(* Person 3 finishes the proposal (anyone can finish it after voting) *)
Definition finish_proposal :=
congress_ifc.(send) 0 (Some (finish_proposal 1)).
Definition chain8 : ChainBuilder :=
unpack_result (add_block chain7 [build_act person_3 person_3 finish_proposal]).
Goal (FMap.elements (congress_state chain8).(proposals)) = [].
Proof. vm_compute. reflexivity. Qed.
(* Balances before: *)
Goal (env_account_balances chain7 congress_1) = 5%Z.
Proof. vm_compute. reflexivity. Qed.
Goal (env_account_balances chain7 person_3) = 0%Z.
Proof. vm_compute. reflexivity. Qed.
(* Balances after: *)
Goal (env_account_balances chain8 congress_1) = 2%Z.
Proof. vm_compute. reflexivity. Qed.
Goal (env_account_balances chain8 person_3) = 3%Z.
Proof. vm_compute. reflexivity. Qed.
Hint Resolve congress_correct_after_block : core.
Definition BuilderDF := LocalChainBuilderImpl AddrSize true.
(* The congress satisfies a property specialized to the local blockchain DFS: *)
Lemma congress_txs_after_local_chain_block
(prev new : BuilderDF) header acts :
builder_add_block prev header acts = Ok new ->
forall caddr,
env_contracts new caddr = Some (Congress.contract : WeakContract) ->
exists inc_calls,
incoming_calls Congress.Msg (builder_trace new) caddr = Some inc_calls /\
length (outgoing_txs (builder_trace new) caddr) <=
num_acts_created_in_proposals inc_calls.
Proof. eauto. Qed.
(* And of course, it is satisfied for the breadth first chain as well. *)
Definition BuilderBF := LocalChainBuilderImpl AddrSize false.
Lemma congress_txs_after_local_chain_bf_block
(prev new : BuilderBF) header acts :
builder_add_block prev header acts = Ok new ->
forall caddr,
env_contracts new caddr = Some (Congress.contract : WeakContract) ->
exists inc_calls,
incoming_calls Congress.Msg (builder_trace new) caddr = Some inc_calls /\
length (outgoing_txs (builder_trace new) caddr) <=
num_acts_created_in_proposals inc_calls.
Proof. eauto. Qed.
End LocalBlockchainTests.