LocalBlockchainTests.v 5.55 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
26
27
28
  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.
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
41
42
43
  Local Coercion to_env (cb : ChainBuilder) : Environment :=
    builder_env cb.

  Compute (block_header chain1).

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

48
49
50
51
  Compute (account_balance chain2 person_1).
  Compute (account_balance chain2 baker).

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

59
60
61
  Compute (account_balance chain3 person_1).
  Compute (account_balance chain3 baker).

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

68
  Definition setup := Congress.build_setup setup_rules.
69

70
  Definition deploy_congress : ActionBody :=
71
    create_deployment 5 Congress.contract setup.
72

73
  Definition chain4 : ChainBuilder :=
74
75
76
77
78
    unpack_option (
        chain3.(builder_add_block)
                 baker
                 [build_act person_1 deploy_congress]
                 4 0).
79

80
81
82
83
84
85
  Definition congress_1 : Address :=
    match outgoing_txs chain4 person_1 with
    | tx :: _ => tx_to tx
    | _ => person_1
    end.

86
  Compute (contract_deployment chain4 congress_1).
87
88
89
90
  Compute (account_balance chain4 person_1).
  Compute (account_balance chain4 baker).
  Compute (account_balance chain4 congress_1).

91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
  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.
107

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

  Compute (congress_ifc.(get_state) chain4).
120
  Compute (FMap.elements (congress_state chain4).(members)).
121

122
  (* person_1 adds person_1 and person_2 as members of congress *)
123
  Definition add_person p :=
124
    congress_ifc.(call) 0 (add_member p).
125

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

133
  Compute (FMap.elements (congress_state chain5).(members)).
134
135
136
137
  Compute (account_balance chain5 congress_1).

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

141
  Definition chain6 : ChainBuilder :=
142
143
144
145
146
    unpack_option (
        chain5.(builder_add_block)
                 baker
                 [build_act person_1 create_proposal_call]
                 6 0).
147

148
  Compute (FMap.elements (congress_state chain6).(proposals)).
149

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

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

161
  Compute (FMap.elements (congress_state chain7).(proposals)).
162

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

167
  Definition chain8 : ChainBuilder :=
168
169
170
171
172
    unpack_option (
        chain7.(builder_add_block)
                 baker
                 [build_act person_3 finish_proposal]
                 8 0).
173

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
174
  Compute (FMap.elements (congress_state chain8).(proposals)).
175
176
  (* Balances before: *)
  Compute (account_balance chain7 congress_1).
177
  Compute (account_balance chain7 person_3).
178
179
  (* Balances after: *)
  Compute (account_balance chain8 congress_1).
180
  Compute (account_balance chain8 person_3).
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
181
  Print Assumptions chain8.
182
End LocalBlockchainTests.