Commit fb1b63e1 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Use Z scope in Congress and use proper block numbers

parent 86c3f6dd
Pipeline #10695 passed with stage
in 2 minutes and 25 seconds
......@@ -10,9 +10,10 @@ From RecordUpdate Require Import RecordUpdate.
Import ListNotations.
Import RecordSetNotations.
Open Scope Z.
Definition TxOut := nat.
Definition ProposalId := nat.
Definition Chain := nat.
Module AddressSet := MSetAVL.Make Address.as_modern_OT.
Module NatKeyedMap := FMapAVL.Make OrderedTypeEx.Nat_as_OT.
......@@ -73,34 +74,34 @@ Instance etaState : Settable _ :=
<*> nextProposalId
<*> members)%set.
Definition version : version := 1.
Definition version : version := 1%nat.
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.
(rules.(minVoteCountPermille) >=? 0)
&& (rules.(minVoteCountPermille) <=? 1000)
&& (rules.(marginNeededPermille) >=? 0)
&& (rules.(marginNeededPermille) <=? 1000)
&& (rules.(debatingPeriodInBlocks) >=? 0).
Definition init (chain : Chain) (details : contract_call_details) (setup : Setup) : option State :=
Definition init (chain : chain) (details : contract_call_details) (setup : Setup) : option State :=
if validateRules setup.(setupRules) then
Some {| owner := details.(from) ;
stateRules := setup.(setupRules) ;
proposals := NatKeyedMap.empty _ ;
nextProposalId := 1 ;
nextProposalId := 1%nat ;
members := AddressSet.empty |}
else
None.
Definition addProposal (txs : list TxOut) (chain : Chain) (state : State) : State :=
Definition addProposal (txs : list TxOut) (chain : chain) (state : State) : State :=
let id := state.(nextProposalId) in
let headBlock := chain.(headBlock) in
let proposal := {| txs := txs ;
votes := AddressKeyedMap.empty _ ;
voteResult := 0 ;
proposedIn := 0 |} in (* todo: fixme *)
proposedIn := headBlock.(header).(blockNumber) |} in
let newProposals := NatKeyedMap.add id proposal state.(proposals) in
state[proposals := newProposals][nextProposalId := id + 1].
state[proposals := newProposals][nextProposalId := (id + 1)%nat].
Local Definition option_bind {A B : Type} (f : A -> option B) (v : option A) : option B :=
match v with
......@@ -111,7 +112,7 @@ Local Definition option_bind {A B : Type} (f : A -> option B) (v : option A) : o
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.
Local Notation ret := Some.
Definition voteProposal
(voter : address)
......@@ -122,12 +123,12 @@ Definition voteProposal
do proposal <- NatKeyedMap.find pid state.(proposals) ;
let oldVote := match AddressKeyedMap.find voter proposal.(votes) with
| Some oldVote => oldVote
| None => 0%Z
| None => 0
end in
let newVotes := AddressKeyedMap.add voter vote proposal.(votes) in
let newVoteResult := (proposal.(voteResult) - oldVote + vote)%Z in
let newVoteResult := proposal.(voteResult) - oldVote + vote in
let newProposal := proposal[votes := newVotes][voteResult := newVoteResult] in
unit (set proposals (NatKeyedMap.add pid newProposal) state).
ret (set proposals (NatKeyedMap.add pid newProposal) state).
Definition retractVote
(voter : address)
......@@ -137,41 +138,41 @@ Definition retractVote
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 newVoteResult := proposal.(voteResult) - oldVote in
let newProposal := proposal[votes := newVotes][voteResult := newVoteResult] in
unit (set proposals (NatKeyedMap.add pid newProposal) state).
ret (set proposals (NatKeyedMap.add pid newProposal) state).
Definition finishProposal
(pid : ProposalId)
(state : State)
(chain : Chain)
(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
let debateEnd := (Z.of_nat proposal.(proposedIn)) + rules.(debatingPeriodInBlocks) in
let curBlock := chain.(headBlock) in
if (Z.of_nat curBlock.(header).(blockNumber)) <? debateEnd 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 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
let responseTxs := if (enoughVoters && enoughAyes)%bool then proposal.(txs) else [] in
unit (newState, responseTxs).
ret (newState, responseTxs).
Definition receive
(chain : Chain)
(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 isFromOwner := (sender =? state.(owner))%address in
let isFromMember := AddressSet.mem sender state.(members) in
let withoutTxs := option_map (fun newState => (newState, [])) in
match isFromOwner, isFromMember, maybeMsg with
......@@ -180,9 +181,9 @@ Definition receive
| true, _, Some (ChangeRules newRules) =>
if validateRules newRules then
Some (state[stateRules := newRules], [])
Some (state[stateRules := newRules], [])
else
None
None
| true, _, Some (AddMember newMember) =>
let newMembers := AddressSet.add newMember state.(members) in
......@@ -195,20 +196,19 @@ Definition receive
| _, true, Some (CreateProposal txs) =>
Some (addProposal txs chain state, [])
| _, true, Some (VoteForProposal id) =>
withoutTxs (voteProposal sender id 1 state)
| _, true, Some (VoteForProposal pid) =>
withoutTxs (voteProposal sender pid 1 state)
| _, true, Some (VoteAgainstProposal pid) =>
withoutTxs (voteProposal sender pid (-1) state)
| _, true, Some (VoteAgainstProposal id) =>
withoutTxs (voteProposal sender id (-1) state)
| _, true, Some (RetractVote id) =>
withoutTxs (retractVote sender id state)
| _, true, Some (RetractVote pid) =>
withoutTxs (retractVote sender pid state)
| _, _, Some (FinishProposal id) =>
finishProposal id state chain
| _, _, Some (FinishProposal pid) =>
finishProposal pid state chain
| _, _, _ =>
None
end.
\ No newline at end of file
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment