LocalBlockchainTests.v 4.14 KB
Newer Older
1
2
From SmartContracts Require Import Monads.
From SmartContracts Require Import Blockchain.
3
From SmartContracts Require LocalBlockchain.
4
5
From SmartContracts Require Import Congress.
From SmartContracts Require Import Oak.
6
From SmartContracts Require Import Containers.
7
8
9
10
11
12
13
14
15
16
17
18
From Coq Require Import List.
From Coq Require Import ZArith.
Import ListNotations.

Section LocalBlockchainTests.
  (* Addresses *)
  Let congress_1 := 1.
  Let baker := 10.
  Let person_1 := 11.
  Let person_2 := 12.
  Let person_3 := 13.

19
20
21
  Let chain1 :=
    initial_chain_builder LocalBlockchain.lc_builder_interface.

22
23
24
25
26
27
28
  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
29
    end.
30
31

  (* Baker mines an empty block (and gets some coins) *)
32
33
  Let chain2 : ChainBuilder :=
    unpack_option (chain1.(add_block) baker []).
34

35
36
37
38
  Compute (account_balance chain2 person_1).
  Compute (account_balance chain2 baker).

  (* Baker transfers 10 coins to person_1 *)
39
40
  Let chain3 : ChainBuilder :=
    unpack_option (chain2.(add_block) baker [(baker, act_transfer person_1 10)]).
41

42
43
44
  Compute (account_balance chain3 person_1).
  Compute (account_balance chain3 baker).

45
  (* person_1 deploys a Congress contract *)
46
47
  Let setup_rules :=
    {| min_vote_count_permille := 200; (* 20% of congress needs to vote *)
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
48
       margin_needed_permille := 501;
49
50
       debating_period_in_blocks := 0; |}.

51
52
  Let setup := Congress.build_setup setup_rules.

53
  Let deploy_congress : ChainAction :=
54
    create_deployment 5 Congress.contract setup.
55

56
57
  Let chain4 : ChainBuilder :=
    unpack_option (chain3.(add_block) baker [(person_1, deploy_congress)]).
58
59

  Compute (contract_deployment chain4 congress_1).
60
61
62
63
  Compute (account_balance chain4 person_1).
  Compute (account_balance chain4 baker).
  Compute (account_balance chain4 congress_1).

64
  Let congress_ifc :=
65
66
    unpack_option
      (get_contract_interface chain4 congress_1 Congress.Setup Congress.Msg Congress.State).
67
68
69
70
71
72

  Let congress_state chain : Congress.State :=
    match congress_ifc.(get_state) chain with
    | Some s => s
    | None => {| owner := 0;
                 state_rules := setup_rules;
73
                 proposals := FMap.empty;
74
                 next_proposal_id := 0;
75
                 members := FMap.empty |}
76
77
78
    end.

  Compute (congress_ifc.(get_state) chain4).
79
  Compute (FMap.elements (congress_state chain4).(members)).
80

81
82
  (* person_1 adds person_1 and person_2 as members of congress *)
  Let add_person p :=
83
    congress_ifc.(call) 0 (add_member p).
84

85
86
87
88
89
  Let chain5 : ChainBuilder :=
    unpack_option
      (chain4.(add_block)
                baker
                [(person_1, add_person person_1); (person_1, add_person person_2)]).
90

91
  Compute (FMap.elements (congress_state chain5).(members)).
92
93
94
95
96
  Compute (account_balance chain5 congress_1).

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

99
100
101
  Let chain6 : ChainBuilder :=
    unpack_option (chain5.(add_block) baker [(person_1, create_proposal_call)]).

102
  Compute (FMap.elements (congress_state chain6).(proposals)).
103

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
104
  (* person_1 and person_2 vote for the proposal *)
105
  Let vote_proposal :=
106
    congress_ifc.(call) 0 (vote_for_proposal 1).
107

108
109
110
111
  Let chain7 : ChainBuilder :=
    unpack_option
      (chain6.(add_block) baker [(person_1, vote_proposal); (person_2, vote_proposal)]).

112
  Compute (FMap.elements (congress_state chain7).(proposals)).
113

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
114
  (* Person 3 finishes the proposal (anyone can finish it after voting) *)
115
  Let finish_proposal :=
116
    congress_ifc.(call) 0 (finish_proposal 1).
117

118
119
120
  Let chain8 : ChainBuilder :=
    unpack_option (chain7.(add_block) baker [(person_3, finish_proposal)]).

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
121
  Compute (FMap.elements (congress_state chain8).(proposals)).
122
123
  (* Balances before: *)
  Compute (account_balance chain7 congress_1).
124
  Compute (account_balance chain7 person_3).
125
126
  (* Balances after: *)
  Compute (account_balance chain8 congress_1).
127
  Compute (account_balance chain8 person_3).
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
128
  Print Assumptions chain8.
129
End LocalBlockchainTests.