Skip to content
GitLab
Commit 81647d05 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Minimize Congress vs Congress_Buggy diff

parent a97bd87b
Show whitespace changes
Inline Side-by-side
src/Congress.v
View file @ 81647d05
......@@ -73,6 +73,131 @@ Record State :=
Instance state_settable : Settable _ :=
settable! build_state <owner; state_rules; proposals; next_proposal_id; members>.
Section Equivalences.
Definition deserialize_rules (v : OakValue) : option Rules :=
do '((a, b), c) <- deserialize v;
Some (build_rules a b c).
Global 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; |}.
Next Obligation.
intros x. unfold deserialize_rules.
rewrite deserialize_serialize.
reflexivity.
Qed.
Global Program Instance setup_equivalence : OakTypeEquivalence Setup :=
{| serialize s := serialize s.(setup_rules);
deserialize or :=
do rules <- deserialize or;
Some (build_setup rules); |}.
Next Obligation.
intros x.
simpl.
rewrite deserialize_serialize.
reflexivity.
Qed.
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).
Global 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.
intros ca.
unfold deserialize_congress_action.
rewrite deserialize_serialize.
destruct ca; reflexivity.
Qed.
Definition deserialize_proposal (v : OakValue) : option Proposal :=
do '(a, b, c, d) <- deserialize v;
Some (build_proposal a b c d).
Global 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.
intros p.
unfold deserialize_proposal.
rewrite deserialize_serialize.
destruct p; 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.
Global Program Instance msg_equivalence : OakTypeEquivalence Msg :=
{| serialize := serialize_msg; deserialize := deserialize_msg; |}.
Next Obligation.
intros msg.
unfold serialize_msg, deserialize_msg.
destruct msg; repeat (simpl; rewrite deserialize_serialize); 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).
Global Program Instance state_equivalence : OakTypeEquivalence State :=
{| serialize := serialize_state; deserialize := deserialize_state; |}.
Next Obligation.
unfold serialize_state, deserialize_state.
destruct x; repeat (simpl; rewrite deserialize_serialize); reflexivity.
Qed.
End Equivalences.
Definition version : Version := 1%nat.
Definition validate_rules (rules : Rules) : bool :=
......@@ -141,6 +266,17 @@ Definition congress_action_to_chain_action (act : CongressAction) : ActionBody :
| cact_call to amt msg => act_call to amt msg
end.
Definition proposal_passed (proposal : Proposal) (state : State) : bool :=
let rules := state.(state_rules) in
let total_votes_for_proposal := Z.of_nat (FMap.size proposal.(votes)) in
let total_members := Z.of_nat (FMap.size state.(members)) in
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
enough_voters && enough_ayes.
Definition do_finish_proposal
(pid : ProposalId)
(state : State)
......@@ -153,19 +289,12 @@ Definition do_finish_proposal
if (cur_slot <? debate_end)%nat then
None
else
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 (FMap.size state.(members)) in
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
if proposal_passed proposal state
then proposal.(actions)
else [] in
let response_chain_acts := map congress_action_to_chain_action response_acts in
let new_state := state<|proposals ::= FMap.remove pid|> in
Some (new_state, response_chain_acts).
Definition receive
......@@ -214,127 +343,6 @@ Definition receive
end.
Definition deserialize_rules (v : OakValue) : option Rules :=
do '((a, b), c) <- deserialize v;
Some (build_rules a b c).
Global 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; |}.
Next Obligation.
intros x. unfold deserialize_rules.
rewrite deserialize_serialize.
reflexivity.
Qed.
Global Program Instance setup_equivalence : OakTypeEquivalence Setup :=
{| serialize s := serialize s.(setup_rules);
deserialize or :=
do rules <- deserialize or;
Some (build_setup rules); |}.
Next Obligation.
intros x.
simpl.
rewrite deserialize_serialize.
reflexivity.
Qed.
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).
Global 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.
intros ca.
unfold deserialize_congress_action.
rewrite deserialize_serialize.
destruct ca; reflexivity.
Qed.
Definition deserialize_proposal (v : OakValue) : option Proposal :=
do '(a, b, c, d) <- deserialize v;
Some (build_proposal a b c d).
Global 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.
intros p.
unfold deserialize_proposal.
rewrite deserialize_serialize.
destruct p; 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.
Global Program Instance msg_equivalence : OakTypeEquivalence Msg :=
{| serialize := serialize_msg; deserialize := deserialize_msg; |}.
Next Obligation.
intros msg.
unfold serialize_msg, deserialize_msg.
destruct msg; repeat (simpl; rewrite deserialize_serialize); 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).
Global Program Instance state_equivalence : OakTypeEquivalence State :=
{| serialize := serialize_state; deserialize := deserialize_state; |}.
Next Obligation.
unfold serialize_state, deserialize_state.
destruct x; repeat (simpl; rewrite deserialize_serialize); reflexivity.
Qed.
Ltac solve_contract_proper :=
repeat
match goal with
......
src/Congress_Buggy.v
View file @ 81647d05
......@@ -476,8 +476,8 @@ Section Theories.
do chain <- builder_add_block chain baker acts (next_num chain) 0;
Some (congress, chain).
Definition final : Address * LocalChainBuilderDepthFirst :=
unpack_option exploit_example.
Definition final :=
(unpack_option exploit_example) <: (@Address LocalChainBase) * LocalChainBuilderDepthFirst.
(* Now we prove that this version of the contract is buggy, i.e. it does not satisfy the
property we proved for the other version of the Congress. We filter out transactions
......@@ -496,5 +496,5 @@ Section Theories.
- reflexivity.
- vm_compute.
lia.
Qed.
Qed.
End Theories.
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