LocalBlockchainTests.v 6.34 KB
Newer Older
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
1
2
3
4
5
(* This file computes with the Congress and an actual blockchain
implementation, showing that everything computes from within Coq. It
also contains specializations of the results proven in Congress.v to
our particular implementations of blockchains. *)

6
7
From SmartContracts Require Import Monads.
From SmartContracts Require Import Blockchain.
8
From SmartContracts Require Import LocalBlockchain.
9
From SmartContracts Require Import Congress.
10
From SmartContracts Require Import Containers.
11
From SmartContracts Require Import BoundedN.
12
From SmartContracts Require Import Extras.
13
From SmartContracts Require Import Serializable.
14
From RecordUpdate Require Import RecordUpdate.
15
16
17
18
19
20
From Coq Require Import List.
From Coq Require Import ZArith.
Import ListNotations.

Section LocalBlockchainTests.
  (* Addresses *)
21
  Definition creator : Address :=
22
23
24
25
26
27
28
29
30
31
32
    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.

33
  Definition ChainBuilder := LocalChainBuilderDepthFirst.
34
35

  Definition chain1 : ChainBuilder := builder_initial.
36

37
38
  Definition add_block (chain : ChainBuilder) acts : option ChainBuilder :=
    let header :=
39
40
41
42
43
44
45
46
        {| block_height := S (chain_height chain);
           block_slot := S (current_slot chain);
           block_finalized_height := finalized_height chain;
           block_creator := creator;
           block_reward := 50; |} in
    builder_add_block chain header acts.

  (* Creator created an empty block (and gets some coins) *)
47
  Definition chain2 : ChainBuilder :=
48
    unpack_option (add_block chain1 []).
49

50
  Compute (account_balance chain2 person_1).
51
  Compute (account_balance chain2 creator).
52

53
  (* Creator transfers 10 coins to person_1 *)
54
  Definition chain3 : ChainBuilder :=
55
    unpack_option (add_block chain2 [build_act creator (act_transfer person_1 10)]).
56

57
  Compute (account_balance chain3 person_1).
58
  Compute (account_balance chain3 creator).
59

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

66
  Definition setup := Congress.build_setup setup_rules.
67

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

71
  Definition chain4 : ChainBuilder :=
72
    unpack_option (add_block chain3 [build_act person_1 deploy_congress]).
73

74
  Definition congress_1 : Address :=
75
    match outgoing_txs (builder_trace chain4) person_1 with
76
77
78
79
    | tx :: _ => tx_to tx
    | _ => person_1
    end.

80
  Compute (account_balance chain4 person_1).
81
  Compute (account_balance chain4 creator).
82
83
  Compute (account_balance chain4 congress_1).

84
85
  Definition congress_ifc : ContractInterface Congress.Msg :=
    match get_contract_interface chain4 congress_1 Congress.Msg with
86
87
88
    | Some x => x
    (* Using unpack_option here is extremely slow *)
    | None =>
89
      @build_contract_interface
90
        _ _
91
        creator
92
93
        (fun a m => deploy_congress)
    end.
94

95
96
  Definition congress_state lc : Congress.State :=
    match env_contract_states lc congress_1 >>= deserialize with
97
    | Some s => s
98
    (* And also here *)
99
    | None => {| owner := creator;
100
                 state_rules := setup_rules;
101
                 proposals := FMap.empty;
102
                 next_proposal_id := 0;
103
                 members := FMap.empty |}
104
105
    end.

106
  Compute (congress_state chain4).
107
  Compute (FMap.elements (congress_state chain4).(members)).
108

109
  (* person_1 adds person_1 and person_2 as members of congress *)
110
  Definition add_person p :=
111
    congress_ifc.(send) 0 (Some (add_member p)).
112

113
  Definition chain5 : ChainBuilder :=
114
115
116
    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).
117

118
  Compute (FMap.elements (congress_state chain5).(members)).
119
120
121
122
  Compute (account_balance chain5 congress_1).

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

126
  Definition chain6 : ChainBuilder :=
127
    unpack_option (add_block chain5 [build_act person_1 create_proposal_call]).
128

129
  Compute (FMap.elements (congress_state chain6).(proposals)).
130

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

135
  Definition chain7 : ChainBuilder :=
136
137
    let acts := [build_act person_1 vote_proposal; build_act person_2 vote_proposal] in
    unpack_option (add_block chain6 acts).
138

139
  Compute (FMap.elements (congress_state chain7).(proposals)).
140

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

145
  Definition chain8 : ChainBuilder :=
146
    unpack_option (add_block chain7 [build_act person_3 finish_proposal]).
147

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

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