LocalBlockchainTests.v 4.28 KB
Newer Older
1
2
3
4
5
From SmartContracts Require Import Monads.
From SmartContracts Require Import Blockchain.
From SmartContracts Require Import LocalBlockchain.
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
19
20
21
22
23
24
25
26
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.

  Let otry x :=
    match x with
    | Some y => y
    | None => LocalBlockchain.initial_chain
    end.
  Let lce_to_chain l := build_chain lc_interface l.(lce_lc) .
  Local Coercion lce_to_chain : LocalChainEnvironment >-> Chain.

27
28
29
30
31
32
33
  Let chain1 :=
    LocalBlockchain.initial_chain.

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

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

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

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

44
  (* person_1 deploys a Congress contract *)
45
46
47
48
49
  Let setup_rules :=
    {| min_vote_count_permille := 200; (* 20% of congress needs to vote *)
       margin_needed_permille := 500;
       debating_period_in_blocks := 0; |}.

50
51
  Let setup := Congress.build_setup setup_rules.

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

55
56
57
58
  Let chain4 :=
    otry (LocalBlockchain.add_block baker [(person_1, deploy_congress)] chain3).

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

63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
  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;
85
                 proposals := FMap.empty;
86
                 next_proposal_id := 0;
87
                 members := FSet.empty |}
88
89
90
    end.

  Compute (congress_ifc.(get_state) chain4).
91
  Compute (FSet.elements (congress_state chain4).(members)).
92

93
94
  (* person_1 adds person_1 and person_2 as members of congress *)
  Let add_person p :=
95
    congress_ifc.(call) 0 (add_member p).
96
97
98
99

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

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

  Let chain6 := otry (LocalBlockchain.add_block baker [(person_1, create_proposal_call)] chain5).
109
  Compute (FMap.elements (congress_state chain6).(proposals)).
110
111
112

  (* person_1 and person_2 votes for the proposal *)
  Let vote_proposal :=
113
    congress_ifc.(call) 0 (vote_for_proposal 1).
114
115
116

  Let chain7 := otry (LocalBlockchain.add_block baker [(person_1, vote_proposal);
                                                       (person_2, vote_proposal)] chain6).
117
  Compute (FMap.elements (congress_state chain7).(proposals)).
118
119
120

  (* Finish the proposal *)
  Let finish_proposal :=
121
    congress_ifc.(call) 0 (finish_proposal 1).
122
123

  Let chain8 := otry (LocalBlockchain.add_block baker [(person_1, finish_proposal)] chain7).
124
125
  (* Balances before: *)
  Compute (account_balance chain7 congress_1).
126
  Compute (account_balance chain7 person_3).
127
128
  (* Balances after: *)
  Compute (account_balance chain8 congress_1).
129
130
  Compute (account_balance chain8 person_3).
End LocalBlockchainTests.