LocalBlockchainTests.v 4.17 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
  Let otry x :=
    match x with
    | Some y => y
25
    | None => chain1
26
    end.
27
28
29

  (* Baker mines an empty block (and gets some coins) *)
  Let chain2 :=
30
    otry (chain1.(add_block) baker []).
31

32
33
34
35
  Compute (account_balance chain2 person_1).
  Compute (account_balance chain2 baker).

  (* Baker transfers 10 coins to person_1 *)
36
  Let chain3 :=
37
    otry (chain2.(add_block) baker [(baker, act_transfer person_1 10)]).
38

39
40
41
  Compute (account_balance chain3 person_1).
  Compute (account_balance chain3 baker).

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

48
49
  Let setup := Congress.build_setup setup_rules.

50
  Let deploy_congress : ChainAction :=
51
    create_deployment 5 Congress.contract setup.
52

53
  Let chain4 :=
54
    otry (chain3.(add_block) baker [(person_1, deploy_congress)]).
55
56

  Compute (contract_deployment chain4 congress_1).
57
58
59
60
  Compute (account_balance chain4 person_1).
  Compute (account_balance chain4 baker).
  Compute (account_balance chain4 congress_1).

61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
  Let congress_ifc :=
    match get_contract_interface
            chain4 congress_1
            Congress.Setup Congress.Msg Congress.State with
    | Some x => x
    (* This stuff is just to make the test example easier
       since we know it will not fail *)
    | None =>
      build_contract_interface
        0
        0
        setup
        (fun c => None)
        (fun a => deploy_congress)
        (fun a m => deploy_congress)
    end.

  Let congress_state chain : Congress.State :=
    match congress_ifc.(get_state) chain with
    | Some s => s
    | None => {| owner := 0;
                 state_rules := setup_rules;
83
                 proposals := FMap.empty;
84
                 next_proposal_id := 0;
85
                 members := FSet.empty |}
86
87
88
    end.

  Compute (congress_ifc.(get_state) chain4).
89
  Compute (FSet.elements (congress_state chain4).(members)).
90

91
92
  (* person_1 adds person_1 and person_2 as members of congress *)
  Let add_person p :=
93
    congress_ifc.(call) 0 (add_member p).
94

95
96
  Let chain5 := otry (chain4.(add_block) baker [(person_1, add_person person_1);
                                                (person_1, add_person person_2)]).
97

98
  Compute (FSet.elements (congress_state chain5).(members)).
99
100
101
102
103
  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 :=
104
    congress_ifc.(call) 0 (create_proposal [cact_transfer person_3 3]).
105

106
  Let chain6 := otry (chain5.(add_block) baker [(person_1, create_proposal_call)]).
107
  Compute (FMap.elements (congress_state chain6).(proposals)).
108

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
109
110
  (* person_1 and person_2 vote for the proposal *)
  Let vote_proposal  :=
111
    congress_ifc.(call) 0 (vote_for_proposal 1).
112

113
114
  Let chain7 := otry (chain6.(add_block) baker [(person_1, vote_proposal);
                                                (person_2, vote_proposal)]).
115
  Compute (FMap.elements (congress_state chain7).(proposals)).
116

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

121
  Let chain8 := otry (chain7.(add_block) baker [(person_3, finish_proposal)]).
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
122
  Compute (FMap.elements (congress_state chain8).(proposals)).
123
124
  (* Balances before: *)
  Compute (account_balance chain7 congress_1).
125
  Compute (account_balance chain7 person_3).
126
127
  (* Balances after: *)
  Compute (account_balance chain8 congress_1).
128
  Compute (account_balance chain8 person_3).
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
129
  Print Assumptions chain8.
130
End LocalBlockchainTests.