Congress.v 11.7 KB
Newer Older
1
2
3
4
From Coq Require Import String.
From Coq Require Import ZArith.
From Coq Require Import Program.Basics.
From SmartContracts Require Import Blockchain.
5
6
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
7
From SmartContracts Require Import Containers.
8
From RecordUpdate Require Import RecordUpdate.
9
(* This is included last to default things to list rather than map/set *)
10
From Coq Require Import List.
11

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
12
13
14
Import ListNotations.
Import RecordSetNotations.

15
Open Scope Z.
16
Set Primitive Projections.
17

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
18
19
Definition ProposalId := nat.

20
21
22
23
Inductive CongressAction :=
  | cact_transfer (to : Address) (amount : Amount)
  | cact_call (to : Address) (amount : Amount) (msg : OakValue).

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
24
Record Proposal :=
25
  build_proposal {
26
    actions : list CongressAction;
27
    votes : FMap Address Z;
28
29
    vote_result : Z;
    proposed_in : BlockId;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
30
31
  }.

32
Instance eta_proposal : Settable _ :=
33
  mkSettable
34
    ((constructor build_proposal) <*> actions
35
                                  <*> votes
36
37
                                  <*> vote_result
                                  <*> proposed_in)%settable.
38

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
39
Record Rules :=
40
41
42
43
  build_rules {
    min_vote_count_permille : Z;
    margin_needed_permille : Z;
    debating_period_in_blocks : Z;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
44
45
46
  }.

Record Setup :=
47
48
  build_setup {
    setup_rules : Rules;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
49
50
51
  }.

Inductive Msg :=
52
53
54
55
56
57
58
59
60
  | transfer_ownership : Address -> Msg
  | change_rules : Rules -> Msg
  | add_member : Address -> Msg
  | remove_member : Address -> Msg
  | create_proposal : list CongressAction -> Msg
  | vote_for_proposal : ProposalId -> Msg
  | vote_against_proposal : ProposalId -> Msg
  | retract_vote : ProposalId -> Msg
  | finish_proposal : ProposalId -> Msg.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
61
62

Record State :=
63
64
65
  build_state {
    owner : Address;
    state_rules : Rules;
66
    proposals : FMap nat Proposal;
67
    next_proposal_id : ProposalId;
68
    members : FMap Address unit;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
69
70
  }.

71
Instance eta_state : Settable _ :=
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
72
  mkSettable
73
74
    ((constructor build_state) <*> owner
                               <*> state_rules
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
75
                               <*> proposals
76
77
                               <*> next_proposal_id
                               <*> members)%settable.
78

79
80
81
82
83
84
85
86
87
Definition version : Version := 1%nat.

Definition validate_rules (rules : Rules) : bool :=
    (rules.(min_vote_count_permille) >=? 0)
        && (rules.(min_vote_count_permille) <=? 1000)
        && (rules.(margin_needed_permille) >=? 0)
        && (rules.(margin_needed_permille) <=? 1000)
        && (rules.(debating_period_in_blocks) >=? 0).

88
Definition init (ctx : ContractCallContext) (setup : Setup) : option State :=
89
90
  if validate_rules setup.(setup_rules) then
    Some {| owner := ctx.(ctx_from);
91
            state_rules := setup.(setup_rules);
92
            proposals := FMap.empty;
93
            next_proposal_id := 1%nat;
94
            members := FMap.empty |}
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
95
96
97
  else
    None.

98
Definition add_proposal (actions : list CongressAction) (chain : Chain) (state : State) : State :=
99
100
101
  let id := state.(next_proposal_id) in
  let head_block := chain.(head_block) in
  let proposal := {| actions := actions;
102
                     votes := FMap.empty;
103
104
                     vote_result := 0;
                     proposed_in := head_block.(block_header).(block_number) |} in
105
  let new_proposals := FMap.add id proposal state.(proposals) in
106
107
108
109
  state[[proposals := new_proposals]][[next_proposal_id := (id + 1)%nat]].

Definition vote_on_proposal
           (voter : Address)
110
111
112
113
           (pid : ProposalId)
           (vote : Z)
           (state : State)
  : option State :=
114
115
  do proposal <- FMap.find pid state.(proposals);
  let old_vote := match FMap.find voter proposal.(votes) with
116
                 | Some old => old
117
                 | None => 0
118
                 end in
119
  let new_votes := FMap.add voter vote proposal.(votes) in
120
121
  let new_vote_result := proposal.(vote_result) - old_vote + vote in
  let new_proposal := proposal[[votes := new_votes]][[vote_result := new_vote_result]] in
122
  Some (state[[proposals ::= FMap.add pid new_proposal]]).
123

124
Definition do_retract_vote
125
           (voter : Address)
126
127
128
           (pid : ProposalId)
           (state : State)
  : option State :=
129
130
131
  do proposal <- FMap.find pid state.(proposals);
  do old_vote <- FMap.find voter proposal.(votes);
  let new_votes := FMap.remove voter proposal.(votes) in
132
133
  let new_vote_result := proposal.(vote_result) - old_vote in
  let new_proposal := proposal[[votes := new_votes]][[vote_result := new_vote_result]] in
134
  Some (state[[proposals ::= FMap.add pid new_proposal]]).
135

136
137
138
139
140
141
Definition congress_action_to_chain_action (act : CongressAction) : ChainAction :=
  match act with
  | cact_transfer to amt => act_transfer to amt
  | cact_call to amt msg => act_call to amt msg
  end.

142
Definition do_finish_proposal
143
144
           (pid : ProposalId)
           (state : State)
145
146
           (chain : Chain)
  : option (State * list ChainAction) :=
147
  do proposal <- FMap.find pid state.(proposals);
148
149
150
151
  let rules := state.(state_rules) in
  let debate_end := (Z.of_nat proposal.(proposed_in)) + rules.(debating_period_in_blocks) in
  let cur_block := chain.(head_block) in
  if (Z.of_nat cur_block.(block_header).(block_number)) <? debate_end then
152
153
    None
  else
154
155
    let new_state := state[[proposals ::= FMap.remove pid]] in
    let total_votes_for_proposal := Z.of_nat (FMap.size proposal.(votes)) in
156
    let total_members := Z.of_nat (FMap.size state.(members)) in
157
158
159
160
161
162
163
164
    let aye_votes := (proposal.(vote_result) + total_votes_for_proposal) / 2 in
    let vote_count_permille := total_votes_for_proposal * 1000 / total_members in
    let aye_permille := aye_votes * 1000 / total_votes_for_proposal in
    let enough_voters := vote_count_permille >=? rules.(min_vote_count_permille) in
    let enough_ayes := aye_permille >=? rules.(margin_needed_permille) in
    let response_acts :=
        if (enough_voters && enough_ayes)%bool
        then proposal.(actions)
165
        else [] in
166
167
    let response_chain_acts := map congress_action_to_chain_action response_acts in
    Some (new_state, response_chain_acts).
168

169
Definition receive
170
           (ctx : ContractCallContext)
171
           (state : State)
172
173
           (maybe_msg : option Msg)
  : option (State * list ChainAction) :=
174
  let chain := ctx.(ctx_chain) in
175
176
  let sender := ctx.(ctx_from) in
  let is_from_owner := (sender =? state.(owner))%address in
177
  let is_from_member := FMap.mem sender state.(members) in
178
  let without_actions := option_map (fun new_state => (new_state, [])) in
179
  match is_from_owner, is_from_member, maybe_msg with
180
  | true, _, Some (transfer_ownership new_owner) =>
181
        Some (state[[owner := new_owner]], [])
182

183
  | true, _, Some (change_rules new_rules) =>
184
        if validate_rules new_rules then
185
            Some (state[[state_rules := new_rules]], [])
186
        else
187
            None
188

189
  | true, _, Some (add_member new_member) =>
190
        Some (state[[members ::= FMap.add new_member tt]], [])
191

192
  | true, _, Some (remove_member old_member) =>
193
        Some (state[[members ::= FMap.remove old_member]], [])
194

195
  | _, true, Some (create_proposal actions) =>
196
        Some (add_proposal actions chain state, [])
197

198
  | _, true, Some (vote_for_proposal pid) =>
199
        without_actions (vote_on_proposal sender pid 1 state)
200

201
  | _, true, Some (vote_against_proposal pid) =>
202
        without_actions (vote_on_proposal sender pid (-1) state)
203

204
205
206
207
208
  | _, true, Some (retract_vote pid) =>
        without_actions (do_retract_vote sender pid state)

  | _, _, Some (finish_proposal pid) =>
        do_finish_proposal pid state chain
209

210
211
  | _, _, _ =>
        None
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226

  end.

Definition deserialize_rules (v : OakValue) : option Rules :=
  do '((a, b), c) <- deserialize v;
  Some (build_rules a b c).

Program Instance rules_equivalence : OakTypeEquivalence Rules :=
  {| serialize r := let (a, b, c) := r in serialize (a, b, c);
     (* Why does
     deserialize v :=
       do '((a, b), c) <- deserialize v;
       Some (build_rules a b c); |}.
       not work here? *)
     deserialize := deserialize_rules; |}.
227
228
229
230
231
Next Obligation.
  intros x. unfold deserialize_rules.
  rewrite deserialize_serialize.
  reflexivity.
Qed.
232
233
234
235
236
237

Program Instance setup_equivalence : OakTypeEquivalence Setup :=
  {| serialize s := serialize s.(setup_rules);
     deserialize or :=
       do rules <- deserialize or;
       Some (build_setup rules); |}.
238
239
240
241
242
243
Next Obligation.
  intros x.
  simpl.
  rewrite deserialize_serialize.
  reflexivity.
Qed.
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260

Definition deserialize_congress_action (v : OakValue) : option CongressAction :=
  do val <- deserialize v;
  Some (match val with
  | inl (to, amount) => cact_transfer to amount
  | inr (to, amount, msg) => cact_call to amount msg
  end).

Program Instance congress_action_equivalence : OakTypeEquivalence CongressAction :=
  {| serialize ca :=
       serialize
         match ca with
         | cact_transfer to amount => inl (to, amount)
         | cact_call to amount msg => inr (to, amount, msg)
         end;
     deserialize := deserialize_congress_action; |}.
Next Obligation.
261
  intros ca.
262
  unfold deserialize_congress_action.
263
264
  rewrite deserialize_serialize.
  destruct ca; reflexivity.
265
266
267
268
269
270
271
272
273
274
275
276
277
Qed.

Definition deserialize_proposal (v : OakValue) : option Proposal :=
  do '(a, b, c, d) <- deserialize v;
  Some (build_proposal a b c d).

Program Instance proposal_equivalence : OakTypeEquivalence Proposal :=
  {| serialize p :=
       let (a, b, c, d) := p in
       serialize (a, b, c, d);
     deserialize := deserialize_proposal;
  |}.
Next Obligation.
278
  intros p.
279
  unfold deserialize_proposal.
280
281
  rewrite deserialize_serialize.
  destruct p; reflexivity.
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
Qed.

Definition serialize_msg (m : Msg) : OakValue :=
  serialize
    match m with
    | transfer_ownership a => (0, serialize a)
    | change_rules r => (1, serialize r)
    | add_member a => (2, serialize a)
    | remove_member a => (3, serialize a)
    | create_proposal l => (4, serialize l)
    | vote_for_proposal pid => (5, serialize pid)
    | vote_against_proposal pid => (6, serialize pid)
    | retract_vote pid => (7, serialize pid)
    | finish_proposal pid => (8, serialize pid)
    end.

Definition deserialize_msg (v : OakValue) : option Msg :=
  do '(tag, v) <- deserialize v;
  match tag with
  | 0 => option_map transfer_ownership (deserialize v)
  | 1 => option_map change_rules (deserialize v)
  | 2 => option_map add_member (deserialize v)
  | 3 => option_map remove_member (deserialize v)
  | 4 => option_map create_proposal (deserialize v)
  | 5 => option_map vote_for_proposal (deserialize v)
  | 6 => option_map vote_against_proposal (deserialize v)
  | 7 => option_map retract_vote (deserialize v)
  | 8 => option_map finish_proposal (deserialize v)
  | _ => None
  end.

Program Instance msg_equivalence : OakTypeEquivalence Msg :=
  {| serialize := serialize_msg; deserialize := deserialize_msg; |}.
Next Obligation.
316
  intros msg.
317
  unfold serialize_msg, deserialize_msg.
318
  destruct msg; repeat (simpl; rewrite deserialize_serialize); reflexivity.
319
320
321
322
323
324
325
326
327
328
329
330
331
332
Qed.

Definition serialize_state (s : State) : OakValue :=
  let (a, b, c, d, e) := s in
  serialize (a, b, c, d, e).

Definition deserialize_state (v : OakValue) : option State :=
  do '(a, b, c, d, e) <- deserialize v;
  Some (build_state a b c d e).

Program Instance state_equivalence : OakTypeEquivalence State :=
  {| serialize := serialize_state; deserialize := deserialize_state; |}.
Next Obligation.
  unfold serialize_state, deserialize_state.
333
  destruct x; repeat (simpl; rewrite deserialize_serialize); reflexivity.
334
335
336
337
Qed.

Definition contract : Contract Setup Msg State :=
  build_contract version init receive.
338

339

340
341
342
343
344
345
346
347
348
(*
(* This first property states that the Congress will only send out actions
   to be performed if there is a matching CreateProposal somewhere in the
   past. That is, no CreateProposal can lead to two batches of actions being
   sent out, and the actions correspond to the ones passed in CreateProposal. *)
Theorem congress_no_unmatched_actions
        (chain : Chain)
        (
*)