Congress.v 7.23 KB
Newer Older
1
2
3
4
5
6
7
8
9
From Coq Require Import String.
From Coq Require Import List.
From Coq Require Import ZArith.
From Coq Require Import Program.Basics.
From Coq Require MSets FMapAVL.
From Coq Require OrderedTypeEx.
From SmartContracts Require Import Blockchain.
From RecordUpdate Require Import RecordUpdate.

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
10
11
12
13
14
15
16
Import ListNotations.
Import RecordSetNotations.

Definition TxOut := nat.
Definition ProposalId := nat.
Definition Chain := nat.

17
18
19
20
Module AddressSet := MSetAVL.Make Address.as_modern_OT.
Module NatKeyedMap := FMapAVL.Make OrderedTypeEx.Nat_as_OT.
Module AddressKeyedMap := FMapAVL.Make Address.as_old_OT.

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
21
22
Record Proposal :=
  {
23
    txs : list TxOut ;
24
    votes : AddressKeyedMap.t Z ;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
25
    voteResult : Z ;
26
    proposedIn : block_id
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
27
28
  }.

29
30
31
32
33
34
Instance etaProposal : Settable _ :=
  mkSettable
    ((constructor Build_Proposal) <*> txs
                                  <*> votes
                                  <*> voteResult
                                  <*> proposedIn)%set.
35

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
36
37
38
39
40
41
42
43
44
45
46
47
48
Record Rules :=
  {
    minVoteCountPermille : Z ;
    marginNeededPermille : Z ;
    debatingPeriodInBlocks : Z
  }.

Record Setup :=
  {
    setupRules : Rules
  }.

Inductive Msg :=
49
| TransferOwnership : address -> Msg
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
50
| ChangeRules : Rules -> Msg
51
52
| AddMember : address -> Msg
| RemoveMember : address -> Msg
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
53
54
55
56
57
58
59
60
| CreateProposal : list TxOut -> Msg
| VoteForProposal : ProposalId -> Msg
| VoteAgainstProposal : ProposalId -> Msg
| RetractVote : ProposalId -> Msg
| FinishProposal : ProposalId -> Msg.

Record State :=
  {
61
    owner : address ;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
62
    stateRules : Rules ;
63
    proposals : NatKeyedMap.t Proposal ;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
64
    nextProposalId : ProposalId ;
65
    members : AddressSet.t
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
66
67
68
69
70
71
72
73
74
  }.

Instance etaState : Settable _ :=
  mkSettable
    ((constructor Build_State) <*> owner
                               <*> stateRules
                               <*> proposals
                               <*> nextProposalId
                               <*> members)%set.
75
76
  
Definition version : version := 1.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
77
78
79
80
81
82
83

Definition validateRules (rules : Rules) : bool :=
    (rules.(minVoteCountPermille) >=? 0)%Z
        && (rules.(minVoteCountPermille) <=? 1000)%Z
        && (rules.(marginNeededPermille) >=? 0)%Z
        && (rules.(marginNeededPermille) <=? 1000)%Z
        && (rules.(debatingPeriodInBlocks) >=? 0)%Z.
84

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
85

86
Definition init (chain : Chain) (details : contract_call_details) (setup : Setup) : option State :=
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
87
88
89
  if validateRules setup.(setupRules) then
    Some {| owner := details.(from) ;
            stateRules := setup.(setupRules) ; 
90
            proposals := NatKeyedMap.empty _ ;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
91
            nextProposalId := 1 ;
92
            members := AddressSet.empty |}
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
93
94
95
  else
    None.

96
97
98
Definition addProposal (txs : list TxOut) (chain : Chain) (state : State) : State :=
  let id := state.(nextProposalId) in
  let proposal := {| txs := txs ;
99
                     votes := AddressKeyedMap.empty _ ;
100
                     voteResult := 0 ;
101
                     proposedIn := 0 |} in (* todo: fixme *)
102
103
104
  let newProposals := NatKeyedMap.add id proposal state.(proposals) in
  state[proposals := newProposals][nextProposalId := id + 1].

105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
Local Definition option_bind {A B : Type} (f : A -> option B) (v : option A) : option B :=
  match v with
  | Some val => f val
  | None => None
  end.

Local Notation "'do' X <- A ; B" := (option_bind (fun X => B) A)
                                      (at level 200, X ident, A at level 100, B at level 200).

Local Notation unit := Some.

Definition voteProposal
           (voter : address)
           (pid : ProposalId)
           (vote : Z)
           (state : State)
  : option State :=
  do proposal <- NatKeyedMap.find pid state.(proposals) ;
  let oldVote := match AddressKeyedMap.find voter proposal.(votes) with
                 | Some oldVote => oldVote
                 | None => 0%Z
                 end in
  let newVotes := AddressKeyedMap.add voter vote proposal.(votes) in
  let newVoteResult := (proposal.(voteResult) - oldVote + vote)%Z in
  let newProposal := proposal[votes := newVotes][voteResult := newVoteResult] in
  unit (set proposals (NatKeyedMap.add pid newProposal) state).

Definition retractVote
           (voter : address)
           (pid : ProposalId)
           (state : State)
  : option State :=
  do proposal <- NatKeyedMap.find pid state.(proposals) ;
  do oldVote <- AddressKeyedMap.find voter proposal.(votes) ;
  let newVotes := AddressKeyedMap.remove voter proposal.(votes) in
  let newVoteResult := (proposal.(voteResult) - oldVote)%Z in
  let newProposal := proposal[votes := newVotes][voteResult := newVoteResult] in
  unit (set proposals (NatKeyedMap.add pid newProposal) state).

Definition finishProposal
           (pid : ProposalId)
           (state : State)
           (chain : Chain)
  : option (State * list TxOut) :=
  do proposal <- NatKeyedMap.find pid state.(proposals) ;
  let rules := state.(stateRules) in
  let debateEnd := ((Z.of_nat proposal.(proposedIn)) + rules.(debatingPeriodInBlocks))%Z in
  let curBlock := 0%Z in (* todo: fixme *)
  if (curBlock <? debateEnd)%Z then
    None
  else
    let newState := set proposals (NatKeyedMap.remove pid) state in
    let totalVotesForProposal := Z.of_nat (AddressKeyedMap.cardinal proposal.(votes)) in
    let totalMembers := Z.of_nat (AddressSet.cardinal state.(members)) in
    let ayeVotes := ((proposal.(voteResult) + totalVotesForProposal) / 2)%Z in
    let voteCountPermille := (totalVotesForProposal * 1000 / totalMembers)%Z in
    let ayePermille := (ayeVotes * 1000 / totalVotesForProposal)%Z in
    let enoughVoters : bool := (voteCountPermille >=? rules.(minVoteCountPermille))%Z in
    let enoughAyes : bool := (ayePermille >=? rules.(marginNeededPermille))%Z in
    let responseTxs := if (enoughVoters && enoughAyes)%bool then proposal.(txs) else [] in
    unit (newState, responseTxs).

167
168
169
170
171
172
173
174
175
Definition receive
           (chain : Chain)
           (state : State)
           (details : contract_call_details)
           (maybeMsg : option Msg)
  : option (State * list TxOut) :=
  let sender := details.(from) in
  let isFromOwner := sender =? state.(owner) in
  let isFromMember := AddressSet.mem sender state.(members) in
176
  let withoutTxs := option_map (fun newState => (newState, [])) in
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
  match isFromOwner, isFromMember, maybeMsg with
  | true, _, Some (TransferOwnership newOwner) =>
        Some (state[owner := newOwner], [])

  | true, _, Some (ChangeRules newRules) =>
        if validateRules newRules then
        Some (state[stateRules := newRules], [])
        else
        None

  | true, _, Some (AddMember newMember) =>
        let newMembers := AddressSet.add newMember state.(members) in
        Some (state[members := newMembers], [])

  | true, _, Some (RemoveMember oldMember) =>
        let newMembers := AddressSet.remove oldMember state.(members) in
        Some (state[members := newMembers], [])

  | _, true, Some (CreateProposal txs) =>
        Some (addProposal txs chain state, [])

198
199
200
201
202
203
204
205
206
207
208
209
  | _, true, Some (VoteForProposal id) =>
        withoutTxs (voteProposal sender id 1 state)

  | _, true, Some (VoteAgainstProposal id) =>
        withoutTxs (voteProposal sender id (-1) state)
                              
  | _, true, Some (RetractVote id) =>
        withoutTxs (retractVote sender id state)

  | _, _, Some (FinishProposal id) =>
        finishProposal id state chain

210
211
212
213
  | _, _, _ =>
        None
    
  end.
214