Congress.v 11.4 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 : FSet Address;
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 := FSet.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
156
    let new_state := state[[proposals ::= FMap.remove pid]] in
    let total_votes_for_proposal := Z.of_nat (FMap.size proposal.(votes)) in
    let total_members := Z.of_nat (FSet.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
178
  let is_from_member := FSet.mem sender state.(members) in
  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 ::= FSet.add new_member]], [])
191

192
  | true, _, Some (remove_member old_member) =>
193
        Some (state[[members ::= FSet.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
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
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
316
317
318
319
320
321
322
323

  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; |}.

Program Instance setup_equivalence : OakTypeEquivalence Setup :=
  {| serialize s := serialize s.(setup_rules);
     deserialize or :=
       do rules <- deserialize or;
       Some (build_setup rules); |}.

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.
  unfold deserialize_congress_action.
  rewrite ote_equivalence.
  destruct x; reflexivity.
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.
  unfold deserialize_proposal.
  rewrite ote_equivalence.
  destruct x; reflexivity.
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.
  unfold serialize_msg, deserialize_msg.
  destruct x; repeat (simpl; rewrite ote_equivalence); reflexivity.
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.
  destruct x; repeat (simpl; rewrite ote_equivalence); reflexivity.
Qed.

Definition contract : Contract Setup Msg State :=
  build_contract version init receive.
324
325
326
327
328
329
330
331
332
333

(*
(* 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)
        (
*)