Congress.v 7.2 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
Import ListNotations.
Import RecordSetNotations.

13
14
Open Scope Z.

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
15
16
17
Definition TxOut := nat.
Definition ProposalId := nat.

18
19
20
21
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
22
23
Record Proposal :=
  {
24
    txs : list TxOut ;
25
    votes : AddressKeyedMap.t Z ;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
26
    voteResult : Z ;
27
    proposedIn : block_id
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
28
29
  }.

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

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

Record Setup :=
  {
    setupRules : Rules
  }.

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

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

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

Definition validateRules (rules : Rules) : bool :=
80
81
82
83
84
    (rules.(minVoteCountPermille) >=? 0)
        && (rules.(minVoteCountPermille) <=? 1000)
        && (rules.(marginNeededPermille) >=? 0)
        && (rules.(marginNeededPermille) <=? 1000)
        && (rules.(debatingPeriodInBlocks) >=? 0).
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 _ ;
91
            nextProposalId := 1%nat ;
92
            members := AddressSet.empty |}
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
93
94
95
  else
    None.

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

106
107
108
109
110
111
112
113
114
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).

115
Local Notation ret := Some.
116
117
118
119
120
121
122
123
124
125

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
126
                 | None => 0
127
128
                 end in
  let newVotes := AddressKeyedMap.add voter vote proposal.(votes) in
129
  let newVoteResult := proposal.(voteResult) - oldVote + vote in
130
  let newProposal := proposal[votes := newVotes][voteResult := newVoteResult] in
131
  ret (set proposals (NatKeyedMap.add pid newProposal) state).
132
133
134
135
136
137
138
139
140

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
141
  let newVoteResult := proposal.(voteResult) - oldVote in
142
  let newProposal := proposal[votes := newVotes][voteResult := newVoteResult] in
143
  ret (set proposals (NatKeyedMap.add pid newProposal) state).
144
145
146
147

Definition finishProposal
           (pid : ProposalId)
           (state : State)
148
           (chain : chain)
149
150
151
  : option (State * list TxOut) :=
  do proposal <- NatKeyedMap.find pid state.(proposals) ;
  let rules := state.(stateRules) in
152
153
154
  let debateEnd := (Z.of_nat proposal.(proposedIn)) + rules.(debatingPeriodInBlocks) in
  let curBlock := chain.(headBlock) in
  if (Z.of_nat curBlock.(header).(blockNumber)) <? debateEnd then
155
156
157
158
159
    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
160
161
162
163
164
    let ayeVotes := (proposal.(voteResult) + totalVotesForProposal) / 2 in
    let voteCountPermille := totalVotesForProposal * 1000 / totalMembers in
    let ayePermille := ayeVotes * 1000 / totalVotesForProposal in
    let enoughVoters := voteCountPermille >=? rules.(minVoteCountPermille) in
    let enoughAyes := ayePermille >=? rules.(marginNeededPermille) in
165
    let responseTxs := if (enoughVoters && enoughAyes)%bool then proposal.(txs) else [] in
166
    ret (newState, responseTxs).
167

168
Definition receive
169
           (chain : chain)
170
171
172
173
174
           (state : State)
           (details : contract_call_details)
           (maybeMsg : option Msg)
  : option (State * list TxOut) :=
  let sender := details.(from) in
175
  let isFromOwner := (sender =? state.(owner))%address in
176
  let isFromMember := AddressSet.mem sender state.(members) in
177
  let withoutTxs := option_map (fun newState => (newState, [])) in
178
179
180
181
182
183
  match isFromOwner, isFromMember, maybeMsg with
  | true, _, Some (TransferOwnership newOwner) =>
        Some (state[owner := newOwner], [])

  | true, _, Some (ChangeRules newRules) =>
        if validateRules newRules then
184
            Some (state[stateRules := newRules], [])
185
        else
186
            None
187
188
189
190
191
192
193
194
195
196
197
198

  | 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, [])

199
200
201
202
203
  | _, true, Some (VoteForProposal pid) =>
        withoutTxs (voteProposal sender pid 1 state)

  | _, true, Some (VoteAgainstProposal pid) =>
        withoutTxs (voteProposal sender pid (-1) state)
204

205
206
  | _, true, Some (RetractVote pid) =>
        withoutTxs (retractVote sender pid state)
207

208
209
  | _, _, Some (FinishProposal pid) =>
        finishProposal pid state chain
210

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