LocalBlockchainTests.v 6.05 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
From SmartContracts Require Import Extras.
From RecordUpdate Require Import RecordUpdate.
10
11
12
13
14
15
From Coq Require Import List.
From Coq Require Import ZArith.
Import ListNotations.

Section LocalBlockchainTests.
  (* Addresses *)
16
17
18
19
20
21
22
23
24
25
26
27
  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.

28
  Definition ChainBuilder := LocalChainBuilderDepthFirst.
29
30

  Definition chain1 : ChainBuilder := builder_initial.
31

32
33
  Compute (block_header chain1).

34
35
36
37
38
  Definition add_block (chain : ChainBuilder) acts : option ChainBuilder :=
    let header :=
        (block_header chain)<|block_height ::= S|><|slot_number ::= S|> in
    builder_add_block chain baker header acts.

39
  (* Baker mines an empty block (and gets some coins) *)
40
  Definition chain2 : ChainBuilder :=
41
    unpack_option (add_block chain1 []).
42

43
44
45
46
  Compute (account_balance chain2 person_1).
  Compute (account_balance chain2 baker).

  (* Baker transfers 10 coins to person_1 *)
47
  Definition chain3 : ChainBuilder :=
48
    unpack_option (add_block chain2 [build_act baker (act_transfer person_1 10)]).
49

50
51
52
  Compute (account_balance chain3 person_1).
  Compute (account_balance chain3 baker).

53
  (* person_1 deploys a Congress contract *)
54
  Definition setup_rules :=
55
    {| min_vote_count_permille := 200; (* 20% of congress needs to vote *)
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
56
       margin_needed_permille := 501;
57
58
       debating_period_in_blocks := 0; |}.

59
  Definition setup := Congress.build_setup setup_rules.
60

61
  Definition deploy_congress : ActionBody :=
62
    create_deployment 5 Congress.contract setup.
63

64
  Definition chain4 : ChainBuilder :=
65
    unpack_option (add_block chain3 [build_act person_1 deploy_congress]).
66

67
  Definition congress_1 : Address :=
68
    match outgoing_txs (builder_trace chain4) person_1 with
69
70
71
72
    | tx :: _ => tx_to tx
    | _ => person_1
    end.

73
74
75
76
  Compute (account_balance chain4 person_1).
  Compute (account_balance chain4 baker).
  Compute (account_balance chain4 congress_1).

77
  Definition congress_ifc
78
    : ContractInterface Congress.Msg Congress.State :=
79
80
    match get_contract_interface
            chain4 congress_1
81
            Congress.Msg Congress.State with
82
83
84
    | Some x => x
    (* Using unpack_option here is extremely slow *)
    | None =>
85
86
      @build_contract_interface
        _ _ _
87
88
89
90
        baker
        (fun c => None)
        (fun a m => deploy_congress)
    end.
91

92
  Definition congress_state chain : Congress.State :=
93
94
    match congress_ifc.(get_state) chain with
    | Some s => s
95
96
    (* And also here *)
    | None => {| owner := baker;
97
                 state_rules := setup_rules;
98
                 proposals := FMap.empty;
99
                 next_proposal_id := 0;
100
                 members := FMap.empty |}
101
102
103
    end.

  Compute (congress_ifc.(get_state) chain4).
104
  Compute (FMap.elements (congress_state chain4).(members)).
105

106
  (* person_1 adds person_1 and person_2 as members of congress *)
107
  Definition add_person p :=
108
    congress_ifc.(send) 0 (Some (add_member p)).
109

110
  Definition chain5 : ChainBuilder :=
111
112
113
    let acts := [build_act person_1 (add_person person_1);
                 build_act person_1 (add_person person_2)] in
    unpack_option (add_block chain4 acts).
114

115
  Compute (FMap.elements (congress_state chain5).(members)).
116
117
118
119
  Compute (account_balance chain5 congress_1).

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

123
  Definition chain6 : ChainBuilder :=
124
    unpack_option (add_block chain5 [build_act person_1 create_proposal_call]).
125

126
  Compute (FMap.elements (congress_state chain6).(proposals)).
127

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
128
  (* person_1 and person_2 vote for the proposal *)
129
  Definition vote_proposal :=
130
    congress_ifc.(send) 0 (Some (vote_for_proposal 1)).
131

132
  Definition chain7 : ChainBuilder :=
133
134
    let acts := [build_act person_1 vote_proposal; build_act person_2 vote_proposal] in
    unpack_option (add_block chain6 acts).
135

136
  Compute (FMap.elements (congress_state chain7).(proposals)).
137

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
138
  (* Person 3 finishes the proposal (anyone can finish it after voting) *)
139
  Definition finish_proposal :=
140
    congress_ifc.(send) 0 (Some (finish_proposal 1)).
141

142
  Definition chain8 : ChainBuilder :=
143
    unpack_option (add_block chain7 [build_act person_3 finish_proposal]).
144

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
145
  Compute (FMap.elements (congress_state chain8).(proposals)).
146
147
  (* Balances before: *)
  Compute (account_balance chain7 congress_1).
148
  Compute (account_balance chain7 person_3).
149
150
  (* Balances after: *)
  Compute (account_balance chain8 congress_1).
151
  Compute (account_balance chain8 person_3).
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
152
  Print Assumptions chain8.
153
End LocalBlockchainTests.
154

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
155
Hint Resolve congress_txs_after_block : core.
156
157
(* The congress satisfies a property specialized to the local blockchain DFS: *)
Lemma congress_txs_after_local_chain_block
158
159
          (prev new : LocalChainBuilderDepthFirst) baker header acts :
  builder_add_block prev baker header acts = Some new ->
160
161
  forall addr,
    env_contracts new addr = Some (Congress.contract : WeakContract) ->
162
163
    length (outgoing_txs (builder_trace new) addr) <=
    num_acts_created_in_proposals (incoming_txs (builder_trace new) addr).
164
165
166
Proof. eauto. Qed.
(* And of course, it is satisfied for the breadth first chain as well. *)
Lemma congress_txs_after_local_chain_bf_block
167
168
      (prev new : LocalChainBuilderBreadthFirst) baker header acts :
  builder_add_block prev baker header acts = Some new ->
169
170
  forall addr,
    env_contracts new addr = Some (Congress.contract : WeakContract) ->
171
172
    length (outgoing_txs (builder_trace new) addr) <=
    num_acts_created_in_proposals (incoming_txs (builder_trace new) addr).
173
Proof. eauto. Qed.