LocalBlockchainTests.v 6.44 KB
Newer Older
1
2
From SmartContracts Require Import Monads.
From SmartContracts Require Import Blockchain.
3
From SmartContracts Require Import LocalBlockchain.
4
5
From SmartContracts Require Import Congress.
From SmartContracts Require Import Oak.
6
From SmartContracts Require Import Containers.
7
From SmartContracts Require Import BoundedN.
8
9
10
11
12
13
From Coq Require Import List.
From Coq Require Import ZArith.
Import ListNotations.

Section LocalBlockchainTests.
  (* Addresses *)
14
15
16
17
18
19
20
21
22
23
24
25
  Definition baker : 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.

26
  Definition ChainBuilder := LocalChainBuilderDepthFirst.
27
28

  Definition chain1 : ChainBuilder := builder_initial.
29

30
31
32
33
34
35
36
  Definition unpack_option {A : Type} (a : option A) :=
    match a return match a with
                   | Some _ => A
                   | None => unit
                   end with
    | Some x => x
    | None => tt
37
    end.
38

39
40
  Compute (block_header chain1).

41
  (* Baker mines an empty block (and gets some coins) *)
42
  Definition chain2 : ChainBuilder :=
43
    unpack_option (chain1.(builder_add_block) baker [] 2 0).
44

45
46
47
48
  Compute (account_balance chain2 person_1).
  Compute (account_balance chain2 baker).

  (* Baker transfers 10 coins to person_1 *)
49
  Definition chain3 : ChainBuilder :=
50
51
52
53
54
    unpack_option (
        chain2.(builder_add_block)
                 baker
                 [build_act baker (act_transfer person_1 10)]
                 3 0).
55

56
57
58
  Compute (account_balance chain3 person_1).
  Compute (account_balance chain3 baker).

59
  (* person_1 deploys a Congress contract *)
60
  Definition setup_rules :=
61
    {| min_vote_count_permille := 200; (* 20% of congress needs to vote *)
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
62
       margin_needed_permille := 501;
63
64
       debating_period_in_blocks := 0; |}.

65
  Definition setup := Congress.build_setup setup_rules.
66

67
  Definition deploy_congress : ActionBody :=
68
    create_deployment 5 Congress.contract setup.
69

70
  Definition chain4 : ChainBuilder :=
71
72
73
74
75
    unpack_option (
        chain3.(builder_add_block)
                 baker
                 [build_act person_1 deploy_congress]
                 4 0).
76

77
78
79
80
81
82
  Definition congress_1 : Address :=
    match outgoing_txs chain4 person_1 with
    | tx :: _ => tx_to tx
    | _ => person_1
    end.

83
  Compute (contract_deployment chain4 congress_1).
84
85
86
87
  Compute (account_balance chain4 person_1).
  Compute (account_balance chain4 baker).
  Compute (account_balance chain4 congress_1).

88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
  Definition congress_ifc
    : ContractInterface Congress.Setup Congress.Msg Congress.State :=
    match get_contract_interface
            chain4 congress_1
            Congress.Setup Congress.Msg Congress.State with
    | Some x => x
    (* Using unpack_option here is extremely slow *)
    | None =>
      build_contract_interface
        baker
        0
        setup
        (fun c => None)
        (fun a => deploy_congress)
        (fun a m => deploy_congress)
    end.
104

105
  Definition congress_state chain : Congress.State :=
106
107
    match congress_ifc.(get_state) chain with
    | Some s => s
108
109
    (* And also here *)
    | None => {| owner := baker;
110
                 state_rules := setup_rules;
111
                 proposals := FMap.empty;
112
                 next_proposal_id := 0;
113
                 members := FMap.empty |}
114
115
116
    end.

  Compute (congress_ifc.(get_state) chain4).
117
  Compute (FMap.elements (congress_state chain4).(members)).
118

119
  (* person_1 adds person_1 and person_2 as members of congress *)
120
  Definition add_person p :=
121
    congress_ifc.(call) 0 (add_member p).
122

123
  Definition chain5 : ChainBuilder :=
124
    unpack_option
125
      (chain4.(builder_add_block)
126
                baker
127
128
                [build_act person_1 (add_person person_1); build_act person_1 (add_person person_2)]
                5 0).
129

130
  Compute (FMap.elements (congress_state chain5).(members)).
131
132
133
134
  Compute (account_balance chain5 congress_1).

  (* person_1 creates a proposal to send 3 coins to person_3 using funds
     of the contract *)
135
  Definition create_proposal_call :=
136
    congress_ifc.(call) 0 (create_proposal [cact_transfer person_3 3]).
137

138
  Definition chain6 : ChainBuilder :=
139
140
141
142
143
    unpack_option (
        chain5.(builder_add_block)
                 baker
                 [build_act person_1 create_proposal_call]
                 6 0).
144

145
  Compute (FMap.elements (congress_state chain6).(proposals)).
146

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
147
  (* person_1 and person_2 vote for the proposal *)
148
  Definition vote_proposal :=
149
    congress_ifc.(call) 0 (vote_for_proposal 1).
150

151
  Definition chain7 : ChainBuilder :=
152
153
154
155
156
    unpack_option (
        chain6.(builder_add_block)
                 baker
                 [build_act person_1 vote_proposal; build_act person_2 vote_proposal]
                 7 0).
157

158
  Compute (FMap.elements (congress_state chain7).(proposals)).
159

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
160
  (* Person 3 finishes the proposal (anyone can finish it after voting) *)
161
  Definition finish_proposal :=
162
    congress_ifc.(call) 0 (finish_proposal 1).
163

164
  Definition chain8 : ChainBuilder :=
165
166
167
168
169
    unpack_option (
        chain7.(builder_add_block)
                 baker
                 [build_act person_3 finish_proposal]
                 8 0).
170

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
171
  Compute (FMap.elements (congress_state chain8).(proposals)).
172
173
  (* Balances before: *)
  Compute (account_balance chain7 congress_1).
174
  Compute (account_balance chain7 person_3).
175
176
  (* Balances after: *)
  Compute (account_balance chain8 congress_1).
177
  Compute (account_balance chain8 person_3).
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
178
  Print Assumptions chain8.
179
End LocalBlockchainTests.
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197

Hint Resolve congress_txs_after_block.
(* The congress satisfies a property specialized to the local blockchain DFS: *)
Lemma congress_txs_after_local_chain_block
          (prev new : LocalChainBuilderDepthFirst) baker acts slot finalization_height :
  builder_add_block prev baker acts slot finalization_height = Some new ->
  forall addr,
    env_contracts new addr = Some (Congress.contract : WeakContract) ->
    length (outgoing_txs new addr) <= num_acts_created_in_proposals new addr.
Proof. eauto. Qed.
(* And of course, it is satisfied for the breadth first chain as well. *)
Lemma congress_txs_after_local_chain_bf_block
      (prev new : LocalChainBuilderBreadthFirst) baker acts slot finalization_height :
  builder_add_block prev baker acts slot finalization_height = Some new ->
  forall addr,
    env_contracts new addr = Some (Congress.contract : WeakContract) ->
    length (outgoing_txs new addr) <= num_acts_created_in_proposals new addr.
Proof. eauto. Qed.