LocalBlockchainTests.v 5.51 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
  Definition congress_1 : Address :=
15
    BoundedN.of_Z_const AddrSize (Z.of_N ContractAddrBase).
16

17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
  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.

  Definition ChainBuilder := builder_type.

  Definition chain1 : ChainBuilder := builder_initial.
32

33
34
35
36
37
38
39
  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
40
    end.
41

42
43
44
45
46
  Local Coercion to_env (cb : ChainBuilder) : Environment :=
    builder_env cb.

  Compute (block_header chain1).

47
  (* Baker mines an empty block (and gets some coins) *)
48
  Definition chain2 : ChainBuilder :=
49
    unpack_option (chain1.(builder_add_block) baker [] 2 0).
50

51
52
53
54
  Compute (account_balance chain2 person_1).
  Compute (account_balance chain2 baker).

  (* Baker transfers 10 coins to person_1 *)
55
  Definition chain3 : ChainBuilder :=
56
57
58
59
60
    unpack_option (
        chain2.(builder_add_block)
                 baker
                 [build_act baker (act_transfer person_1 10)]
                 3 0).
61

62
63
64
  Compute (account_balance chain3 person_1).
  Compute (account_balance chain3 baker).

65
  (* person_1 deploys a Congress contract *)
66
  Definition setup_rules :=
67
    {| min_vote_count_permille := 200; (* 20% of congress needs to vote *)
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
68
       margin_needed_permille := 501;
69
70
       debating_period_in_blocks := 0; |}.

71
  Definition setup := Congress.build_setup setup_rules.
72

73
  Definition deploy_congress : ActionBody :=
74
    create_deployment 5 Congress.contract setup.
75

76
  Definition chain4 : ChainBuilder :=
77
78
79
80
81
    unpack_option (
        chain3.(builder_add_block)
                 baker
                 [build_act person_1 deploy_congress]
                 4 0).
82
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.