Contents:
Library ConCert.Examples.Congress.tests.Congress_BuggyGens
From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import BoundedN.
From ConCert.Execution Require Import Containers.
From ConCert.Execution Require Import Serializable.
#[warnings="-notation-incompatible-prefix"]
From ConCert.Execution.Test Require Import QCTest.
From ConCert.Examples.Congress Require Import Congress_Buggy.
From Coq Require Import ZArith.
From Coq Require Import List. Import ListNotations.
Import MonadNotation.
Arguments SerializedValue : clear implicits.
Arguments deserialize : clear implicits.
Arguments serialize : clear implicits.
Definition serializeMsg := serialize Msg _.
Definition gRulesSized (n : nat) : G Rules :=
vote_count <- choose(1%Z, 1000%Z) ;;
margin <- choose(1%Z, 1000%Z) ;;
liftM (build_rules vote_count margin) arbitrary.
#[export]
Instance genRulesSized : GenSized Rules :=
{|
arbitrarySized := gRulesSized
|}.
#[export]
Instance genSetupSized : GenSized Setup :=
{|
arbitrarySized n := liftM build_setup (arbitrarySized n)
|}.
(* ------------------ generators of actions --------------------------- *)
Definition congressContractsMembers_nonowners state : list Address :=
let members := (map fst o FMap.elements) (members state) in
let non_owner_members := filter (fun member => address_neqb member (owner state)) members in
non_owner_members.
Definition gCongressMember_without_caller (state : Congress_Buggy.State)
(calling_addr : Address)
(contract_addr : Address)
: GOpt Address :=
let members := (map fst o FMap.elements) (members state) in
let members_without_caller := List.remove address_eqdec calling_addr members in
match members_without_caller with
| [] => returnGen None
| m ::ms => liftM Some (elems_ m members_without_caller)
end.
Definition try_newCongressMember_fix (members : list Address)
nr_attempts curr_nr
: option Address :=
let fix aux nr_attempts curr_nr :=
match nr_attempts with
| 0 => None
| S n' =>
match @BoundedN.of_nat AddrSize curr_nr with
| Some addr_attempt =>
if List.existsb (address_eqb addr_attempt) members
then aux n' (S curr_nr)
else Some addr_attempt
| None => None
end
end in aux nr_attempts curr_nr.
Definition try_newCongressMember (state : Congress_Buggy.State)
(congress_addr : Address)
(nr_attempts : nat)
: option Address :=
let members := (map fst o FMap.elements) (members state) in
try_newCongressMember_fix members nr_attempts 0.
Definition bindCallerIsOwnerOpt {A : Type}
(state : Congress_Buggy.State)
(calling_addr : Address)
(contract_addr : Address)
(g : GOpt A)
: GOpt A :=
if address_eqb calling_addr contract_addr
then g
else if address_eqb state.(owner) calling_addr
then g
else returnGen None.
Definition try_gNewOwner state calling_addr contract_addr : GOpt Address :=
bindCallerIsOwnerOpt state calling_addr contract_addr
(gCongressMember_without_caller state calling_addr contract_addr).
Definition validate_addr (a : Address) : GOpt (address_is_contract a = false) :=
match (Bool.bool_dec (address_is_contract a) true) with
| left _ => returnGen None
| right p => returnGenSome (Bool.not_true_is_false _ p)
end.
Definition vote_proposal (caddr : Address)
(members_and_proposals : FMap Address (list ProposalId))
(call : forall (caddr : Address) (origin : Address),
address_is_contract origin = false -> Msg -> GOpt Action)
(vote : ProposalId -> Msg) : GOpt Action :=
'(member, pids) <-- sampleFMapOpt members_and_proposals ;;
p <-- validate_addr member ;;
pid <-- elems_opt pids ;;
call caddr member p (vote pid).
(* Returns a mapping to proposals which have been discussed long enough, according to the
current rules in the given congress' state *)
Definition finishable_proposals (state : Congress_Buggy.State)
(current_slot : nat)
: FMap ProposalId Proposal :=
let pids_map_filtered := filter_FMap (fun '(_, proposal) =>
proposal.(proposed_in) + state.(state_rules).(debating_period_in_blocks) <=? current_slot
) state.(proposals) in
if 0 <? FMap.size pids_map_filtered
then pids_map_filtered
else FMap.empty.
Definition lc_contract_members_and_proposals_new_voters (state : Congress_Buggy.State)
: (FMap Address (list ProposalId)) :=
let candidate_members := (map fst o FMap.elements) (members state) in
let proposals_pairs := FMap.elements (proposals state) in
if (0 <? length candidate_members) && (0 <? length proposals_pairs)
then
let voters_to_proposals : FMap Address (list ProposalId) :=
List.fold_left (fun acc m =>
let unvoted_proposals : list (ProposalId * Proposal) :=
List.filter (fun p => match FMap.find m (votes (snd p)) with
| Some _ => false
| None => true
end) proposals_pairs in
match List.map fst unvoted_proposals with
| [] => acc
| _ as ps => FMap.add m ps acc
end
) candidate_members FMap.empty in
voters_to_proposals
else FMap.empty.
Definition lc_contract_members_and_proposals_with_votes (state : Congress_Buggy.State)
: FMap Address (list ProposalId) :=
let members : list Address := (map fst o FMap.elements) (members state) in
let proposals_map : FMap nat Proposal :=
filter_FMap (fun p => 0 =? (FMap.size (votes (snd p)))) (proposals state) in
if (0 <? length members) && (0 =? (FMap.size proposals_map))
then (
let propIds : list ProposalId := (map fst o FMap.elements) proposals_map in
fold_left (fun acc m => FMap.add m propIds acc) members FMap.empty
)
else FMap.empty.
Fixpoint GCongressAction (env : Environment)
(fuel : nat)
(caddr : Address)
: GOpt Action :=
let call contract_addr caller_addr caller_addr_is_user msg :=
amount <- match env.(env_account_balances) caller_addr with
| 0%Z => returnGen 0%Z
| caller_balance => choose (0%Z, caller_balance)
end ;;
returnGenSome (build_act caller_addr caller_addr
(congress_action_to_chain_action (cact_call contract_addr amount (serializeMsg msg)))) in
congress_state <-- returnGen (get_contract_state Congress_Buggy.State env caddr) ;;
let members := (map fst o FMap.elements) congress_state.(members) in
let owner := congress_state.(owner) in
match fuel with
| 0 =>
backtrack [
(* transfer_ownership *)
(1, members <-- elems_opt (congressContractsMembers_nonowners congress_state) ;;
new_owner <-- (try_gNewOwner congress_state owner caddr) ;;
p <-- validate_addr owner ;;
call caddr owner p (transfer_ownership new_owner)
) ;
(* change_rules *)
(1, rules <- gRulesSized 4 ;;
p <-- validate_addr owner ;;
call caddr owner p (change_rules rules)
) ;
(* add_member *)
(2, addr <-- returnGen (try_newCongressMember congress_state caddr 10) ;;
p <-- validate_addr owner ;;
call caddr owner p (add_member addr)
) ;
(* remove_member *)
(1, member <-- elems_opt members ;;
p <-- validate_addr owner ;;
call caddr owner p (remove_member member)
) ;
(* vote_for_proposal *)
(* Requirements:
- contract with a proposal and members must exist
- only members which have not already voted can vote again *)
(2, vote_proposal caddr (lc_contract_members_and_proposals_new_voters congress_state)
call vote_for_proposal) ;
(* vote_against_proposal *)
(2, vote_proposal caddr (lc_contract_members_and_proposals_new_voters congress_state)
call vote_against_proposal) ;
(* retract_vote *)
(2, vote_proposal caddr (lc_contract_members_and_proposals_with_votes congress_state)
call retract_vote) ;
(* finish_proposal *)
(* Requirements:
- only contract owner can finish proposals
- the debating period must have passed *)
(2, '(pid, _) <-- sampleFMapOpt (finishable_proposals congress_state env.(current_slot)) ;;
p <-- validate_addr owner ;;
call caddr owner p (finish_proposal pid)
)
]
| S fuel' => backtrack [
(3, GCongressAction env fuel' caddr) ;
(* add_proposal *)
(1,
(* recurse. Msg is converted to a SerializedType using 'serialize' *)
(* This makes it possible to create proposals about proposals about proposals etc... *)
(* Note: currently we don't support having multiple actions in a proposal *)
(* Note: the way we recurse may be too restrictive - we fix a caddr, which may cause gCongressMember
to return None even though it could have succeeded for another caddr.
Maybe this is not a big issue, though. *)
act <-- GCongressAction env fuel' caddr ;;
let caller_addr := act.(act_from) in
match act.(act_body) with
| act_call caddr amount msg =>
member <-- elems_opt members ;;
let ca := cact_call caddr amount msg in
p <-- validate_addr member ;;
call caddr member p (create_proposal [ca])
| _ => returnGenSome act
end)
]
end.
From ConCert.Execution Require Import BoundedN.
From ConCert.Execution Require Import Containers.
From ConCert.Execution Require Import Serializable.
#[warnings="-notation-incompatible-prefix"]
From ConCert.Execution.Test Require Import QCTest.
From ConCert.Examples.Congress Require Import Congress_Buggy.
From Coq Require Import ZArith.
From Coq Require Import List. Import ListNotations.
Import MonadNotation.
Arguments SerializedValue : clear implicits.
Arguments deserialize : clear implicits.
Arguments serialize : clear implicits.
Definition serializeMsg := serialize Msg _.
Definition gRulesSized (n : nat) : G Rules :=
vote_count <- choose(1%Z, 1000%Z) ;;
margin <- choose(1%Z, 1000%Z) ;;
liftM (build_rules vote_count margin) arbitrary.
#[export]
Instance genRulesSized : GenSized Rules :=
{|
arbitrarySized := gRulesSized
|}.
#[export]
Instance genSetupSized : GenSized Setup :=
{|
arbitrarySized n := liftM build_setup (arbitrarySized n)
|}.
(* ------------------ generators of actions --------------------------- *)
Definition congressContractsMembers_nonowners state : list Address :=
let members := (map fst o FMap.elements) (members state) in
let non_owner_members := filter (fun member => address_neqb member (owner state)) members in
non_owner_members.
Definition gCongressMember_without_caller (state : Congress_Buggy.State)
(calling_addr : Address)
(contract_addr : Address)
: GOpt Address :=
let members := (map fst o FMap.elements) (members state) in
let members_without_caller := List.remove address_eqdec calling_addr members in
match members_without_caller with
| [] => returnGen None
| m ::ms => liftM Some (elems_ m members_without_caller)
end.
Definition try_newCongressMember_fix (members : list Address)
nr_attempts curr_nr
: option Address :=
let fix aux nr_attempts curr_nr :=
match nr_attempts with
| 0 => None
| S n' =>
match @BoundedN.of_nat AddrSize curr_nr with
| Some addr_attempt =>
if List.existsb (address_eqb addr_attempt) members
then aux n' (S curr_nr)
else Some addr_attempt
| None => None
end
end in aux nr_attempts curr_nr.
Definition try_newCongressMember (state : Congress_Buggy.State)
(congress_addr : Address)
(nr_attempts : nat)
: option Address :=
let members := (map fst o FMap.elements) (members state) in
try_newCongressMember_fix members nr_attempts 0.
Definition bindCallerIsOwnerOpt {A : Type}
(state : Congress_Buggy.State)
(calling_addr : Address)
(contract_addr : Address)
(g : GOpt A)
: GOpt A :=
if address_eqb calling_addr contract_addr
then g
else if address_eqb state.(owner) calling_addr
then g
else returnGen None.
Definition try_gNewOwner state calling_addr contract_addr : GOpt Address :=
bindCallerIsOwnerOpt state calling_addr contract_addr
(gCongressMember_without_caller state calling_addr contract_addr).
Definition validate_addr (a : Address) : GOpt (address_is_contract a = false) :=
match (Bool.bool_dec (address_is_contract a) true) with
| left _ => returnGen None
| right p => returnGenSome (Bool.not_true_is_false _ p)
end.
Definition vote_proposal (caddr : Address)
(members_and_proposals : FMap Address (list ProposalId))
(call : forall (caddr : Address) (origin : Address),
address_is_contract origin = false -> Msg -> GOpt Action)
(vote : ProposalId -> Msg) : GOpt Action :=
'(member, pids) <-- sampleFMapOpt members_and_proposals ;;
p <-- validate_addr member ;;
pid <-- elems_opt pids ;;
call caddr member p (vote pid).
(* Returns a mapping to proposals which have been discussed long enough, according to the
current rules in the given congress' state *)
Definition finishable_proposals (state : Congress_Buggy.State)
(current_slot : nat)
: FMap ProposalId Proposal :=
let pids_map_filtered := filter_FMap (fun '(_, proposal) =>
proposal.(proposed_in) + state.(state_rules).(debating_period_in_blocks) <=? current_slot
) state.(proposals) in
if 0 <? FMap.size pids_map_filtered
then pids_map_filtered
else FMap.empty.
Definition lc_contract_members_and_proposals_new_voters (state : Congress_Buggy.State)
: (FMap Address (list ProposalId)) :=
let candidate_members := (map fst o FMap.elements) (members state) in
let proposals_pairs := FMap.elements (proposals state) in
if (0 <? length candidate_members) && (0 <? length proposals_pairs)
then
let voters_to_proposals : FMap Address (list ProposalId) :=
List.fold_left (fun acc m =>
let unvoted_proposals : list (ProposalId * Proposal) :=
List.filter (fun p => match FMap.find m (votes (snd p)) with
| Some _ => false
| None => true
end) proposals_pairs in
match List.map fst unvoted_proposals with
| [] => acc
| _ as ps => FMap.add m ps acc
end
) candidate_members FMap.empty in
voters_to_proposals
else FMap.empty.
Definition lc_contract_members_and_proposals_with_votes (state : Congress_Buggy.State)
: FMap Address (list ProposalId) :=
let members : list Address := (map fst o FMap.elements) (members state) in
let proposals_map : FMap nat Proposal :=
filter_FMap (fun p => 0 =? (FMap.size (votes (snd p)))) (proposals state) in
if (0 <? length members) && (0 =? (FMap.size proposals_map))
then (
let propIds : list ProposalId := (map fst o FMap.elements) proposals_map in
fold_left (fun acc m => FMap.add m propIds acc) members FMap.empty
)
else FMap.empty.
Fixpoint GCongressAction (env : Environment)
(fuel : nat)
(caddr : Address)
: GOpt Action :=
let call contract_addr caller_addr caller_addr_is_user msg :=
amount <- match env.(env_account_balances) caller_addr with
| 0%Z => returnGen 0%Z
| caller_balance => choose (0%Z, caller_balance)
end ;;
returnGenSome (build_act caller_addr caller_addr
(congress_action_to_chain_action (cact_call contract_addr amount (serializeMsg msg)))) in
congress_state <-- returnGen (get_contract_state Congress_Buggy.State env caddr) ;;
let members := (map fst o FMap.elements) congress_state.(members) in
let owner := congress_state.(owner) in
match fuel with
| 0 =>
backtrack [
(* transfer_ownership *)
(1, members <-- elems_opt (congressContractsMembers_nonowners congress_state) ;;
new_owner <-- (try_gNewOwner congress_state owner caddr) ;;
p <-- validate_addr owner ;;
call caddr owner p (transfer_ownership new_owner)
) ;
(* change_rules *)
(1, rules <- gRulesSized 4 ;;
p <-- validate_addr owner ;;
call caddr owner p (change_rules rules)
) ;
(* add_member *)
(2, addr <-- returnGen (try_newCongressMember congress_state caddr 10) ;;
p <-- validate_addr owner ;;
call caddr owner p (add_member addr)
) ;
(* remove_member *)
(1, member <-- elems_opt members ;;
p <-- validate_addr owner ;;
call caddr owner p (remove_member member)
) ;
(* vote_for_proposal *)
(* Requirements:
- contract with a proposal and members must exist
- only members which have not already voted can vote again *)
(2, vote_proposal caddr (lc_contract_members_and_proposals_new_voters congress_state)
call vote_for_proposal) ;
(* vote_against_proposal *)
(2, vote_proposal caddr (lc_contract_members_and_proposals_new_voters congress_state)
call vote_against_proposal) ;
(* retract_vote *)
(2, vote_proposal caddr (lc_contract_members_and_proposals_with_votes congress_state)
call retract_vote) ;
(* finish_proposal *)
(* Requirements:
- only contract owner can finish proposals
- the debating period must have passed *)
(2, '(pid, _) <-- sampleFMapOpt (finishable_proposals congress_state env.(current_slot)) ;;
p <-- validate_addr owner ;;
call caddr owner p (finish_proposal pid)
)
]
| S fuel' => backtrack [
(3, GCongressAction env fuel' caddr) ;
(* add_proposal *)
(1,
(* recurse. Msg is converted to a SerializedType using 'serialize' *)
(* This makes it possible to create proposals about proposals about proposals etc... *)
(* Note: currently we don't support having multiple actions in a proposal *)
(* Note: the way we recurse may be too restrictive - we fix a caddr, which may cause gCongressMember
to return None even though it could have succeeded for another caddr.
Maybe this is not a big issue, though. *)
act <-- GCongressAction env fuel' caddr ;;
let caller_addr := act.(act_from) in
match act.(act_body) with
| act_call caddr amount msg =>
member <-- elems_opt members ;;
let ca := cact_call caddr amount msg in
p <-- validate_addr member ;;
call caddr member p (create_proposal [ca])
| _ => returnGenSome act
end)
]
end.