LocalBlockchainTests.v 6.46 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
  Definition congress_1 : Address :=
78
    match outgoing_txs (builder_trace chain4) person_1 with
79
80
81
82
    | tx :: _ => tx_to tx
    | _ => person_1
    end.

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

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

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

  Compute (congress_ifc.(get_state) chain4).
114
  Compute (FMap.elements (congress_state chain4).(members)).
115

116
  (* person_1 adds person_1 and person_2 as members of congress *)
117
  Definition add_person p :=
118
    congress_ifc.(send) 0 (Some (add_member p)).
119

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

127
  Compute (FMap.elements (congress_state chain5).(members)).
128
129
130
131
  Compute (account_balance chain5 congress_1).

  (* person_1 creates a proposal to send 3 coins to person_3 using funds
     of the contract *)
132
  Definition create_proposal_call :=
133
    congress_ifc.(send) 0 (Some (create_proposal [cact_transfer person_3 3])).
134

135
  Definition chain6 : ChainBuilder :=
136
137
138
139
140
    unpack_option (
        chain5.(builder_add_block)
                 baker
                 [build_act person_1 create_proposal_call]
                 6 0).
141

142
  Compute (FMap.elements (congress_state chain6).(proposals)).
143

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
144
  (* person_1 and person_2 vote for the proposal *)
145
  Definition vote_proposal :=
146
    congress_ifc.(send) 0 (Some (vote_for_proposal 1)).
147

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

155
  Compute (FMap.elements (congress_state chain7).(proposals)).
156

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
157
  (* Person 3 finishes the proposal (anyone can finish it after voting) *)
158
  Definition finish_proposal :=
159
    congress_ifc.(send) 0 (Some (finish_proposal 1)).
160

161
  Definition chain8 : ChainBuilder :=
162
163
164
165
166
    unpack_option (
        chain7.(builder_add_block)
                 baker
                 [build_act person_3 finish_proposal]
                 8 0).
167

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
168
  Compute (FMap.elements (congress_state chain8).(proposals)).
169
170
  (* Balances before: *)
  Compute (account_balance chain7 congress_1).
171
  Compute (account_balance chain7 person_3).
172
173
  (* Balances after: *)
  Compute (account_balance chain8 congress_1).
174
  Compute (account_balance chain8 person_3).
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
175
  Print Assumptions chain8.
176
End LocalBlockchainTests.
177

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
178
Hint Resolve congress_txs_after_block : core.
179
180
181
182
183
184
(* 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) ->
185
186
    length (outgoing_txs (builder_trace new) addr) <=
    num_acts_created_in_proposals (incoming_txs (builder_trace new) addr).
187
188
189
190
191
192
193
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) ->
194
195
    length (outgoing_txs (builder_trace new) addr) <=
    num_acts_created_in_proposals (incoming_txs (builder_trace new) addr).
196
Proof. eauto. Qed.