Update QuickChick to v2.0.0 (AU-COBRA#226)

.github/coq-concert.opam.locked

@@ -21,7 +21,7 @@ depends: [
   "coq-metacoq-utils" {= "1.2+8.17"}
   "coq-rust-extraction" {= "dev"}
   "coq-elm-extraction" {= "dev"}
-  "coq-quickchick" {= "1.6.5"}
+  "coq-quickchick" {= "2.0.0"}
   "coq-stdpp" {= "1.8.0"}
 ]
 build: [

coq-concert.opam

@@ -16,7 +16,7 @@ doc: "https://au-cobra.github.io/ConCert/toc.html"
 depends: [
   "coq" {>= "8.17" & < "8.18~"}
   "coq-bignums" {>= "8"}
-  "coq-quickchick" {>= "1.6.4" & <= "1.6.5"}
+  "coq-quickchick" {= "2.0.0"}
   "coq-metacoq-utils" {= "1.2+8.17"}
   "coq-metacoq-common" {= "1.2+8.17"}
   "coq-metacoq-template" {= "1.2+8.17"}

examples/bat/BATGens.v

@@ -33,12 +33,12 @@ Module BATGens (Info : BATGensInfo).
   Definition account_balance (env : Environment) (addr : Address) : Amount :=
     (env_account_balances env) addr.
 
-  Definition get_refundable_accounts state : list (G (option Address)) :=
+  Definition get_refundable_accounts state : list (GOpt Address) :=
     let balances_list := FMap.elements (balances state) in
     let filtered_balances := filter (fun x => (bat_addr_refundable || (address_neqb bat_addr (fst x))) && (0 <? (snd x))%N) balances_list in
       map returnGen (map Some (map fst filtered_balances)).
 
-  Definition get_fundable_accounts env : G (option Address) :=
+  Definition get_fundable_accounts env : GOpt Address :=
     let freq_accounts := map (fun addr => (if bat_addr_fundable || (address_neqb addr bat_addr) then Z.to_nat (account_balance env addr) else 0, returnGenSome addr)) accounts in
       freq_ (returnGen None) freq_accounts.
 
@@ -54,13 +54,13 @@ Module BATGens (Info : BATGensInfo).
     then
       returnGen None
     else
-      from_addr <- get_fundable_accounts env ;;
-      value <- bindGen (gFund_amount env state from_addr) returnGenSome ;;
+      from_addr <-- get_fundable_accounts env ;;
+      value <- gFund_amount env state from_addr ;;
       returnGenSome (from_addr, value, create_tokens).
 
   Definition gCreateTokensInvalid (env : Environment) (state : BATCommon.State) : GOpt (Address * Amount * Msg) :=
-    from_addr <- get_fundable_accounts env ;;
-    value <- bindGen (choose (1, account_balance env from_addr)%Z) returnGenSome ;;
+    from_addr <-- get_fundable_accounts env ;;
+    value <- choose (1, account_balance env from_addr)%Z ;;
     returnGenSome (from_addr, value, create_tokens).
 
   Definition gRefund (env : Environment) (state : BATCommon.State) : GOpt (Address * Msg) :=
@@ -72,7 +72,7 @@ Module BATGens (Info : BATGensInfo).
     then
       returnGen None
     else
-      from_addr <- oneOf_ (returnGen None) accounts ;;
+      from_addr <-- oneOf_ (returnGen None) accounts ;;
       returnGenSome (from_addr, refund).
 
   Definition gRefundInvalid (env : Environment) (state : BATCommon.State) : G (Address * Msg) :=
@@ -106,15 +106,15 @@ Module BATGens (Info : BATGensInfo).
   Definition gApprove (state : BATCommon.State) : GOpt (Address * Msg) :=
     if eip20_transactions_before_finalized || state.(isFinalized)
     then
-      bindGenOpt (EIP20.gApprove (token_state state))
+      bindOpt (EIP20.gApprove (token_state state))
           (fun '(caller, msg) => returnGenSome (caller, tokenMsg msg))
     else
       returnGen None.
 
   Definition gTransfer_from (state : BATCommon.State) : GOpt (Address * Msg) :=
     if eip20_transactions_before_finalized || state.(isFinalized)
     then
-      bindGenOpt (EIP20.gTransfer_from (token_state state))
+      bindOpt (EIP20.gTransfer_from (token_state state))
           (fun '(caller, msg) => returnGenSome (caller, tokenMsg msg))
     else
       returnGen None.
@@ -126,40 +126,40 @@ Module BATGens (Info : BATGensInfo).
   Definition gBATActionValid (env : Environment) : GOpt Action :=
     let call contract_addr caller_addr value msg :=
       returnGenSome (build_call caller_addr contract_addr value msg) in
-    state <- returnGen (get_contract_state BATCommon.State env contract_addr) ;;
+    state <-- returnGen (get_contract_state BATCommon.State env contract_addr) ;;
     backtrack [
       (* transfer *)
-      (1, bindGenOpt (gTransfer env state)
+      (1, bindOpt (gTransfer env state)
           (fun '(caller, msg) =>
             call contract_addr caller (0%Z) msg
           )
       );
       (* transfer_from *)
-      (2, bindGenOpt (gTransfer_from state)
+      (2, bindOpt (gTransfer_from state)
           (fun '(caller, msg) =>
             call contract_addr caller (0%Z) msg
           )
       );
       (* approve *)
-      (1, bindGenOpt (gApprove state)
+      (1, bindOpt (gApprove state)
           (fun '(caller, msg) =>
             call contract_addr caller (0%Z) msg
           )
       );
       (* create_tokens *)
-      (5, bindGenOpt (gCreateTokens env state)
+      (5, bindOpt (gCreateTokens env state)
           (fun '(caller, value, msg) =>
             call contract_addr caller value msg
           )
       );
       (* refund *)
-      (10, bindGenOpt (gRefund env state)
+      (10, bindOpt (gRefund env state)
           (fun '(caller, msg) =>
             call contract_addr caller (0%Z) msg
           )
       );
       (* finalize *)
-      (10, bindGenOpt (gFinalize env state)
+      (10, bindOpt (gFinalize env state)
           (fun '(caller, msg) =>
             call contract_addr caller (0%Z) msg
           )
@@ -174,26 +174,26 @@ Module BATGens (Info : BATGensInfo).
   Definition gBATActionInvalid (env : Environment) : GOpt Action :=
     let call contract_addr caller_addr value msg :=
       returnGenSome (build_call caller_addr contract_addr value msg) in
-    state <- returnGen (get_contract_state BATCommon.State env contract_addr) ;;
+    state <-- returnGen (get_contract_state BATCommon.State env contract_addr) ;;
     backtrack [
       (* transfer *)
       (1, '(caller, msg) <- EIP20.gTransfer env (token_state state) ;;
           call contract_addr caller (0%Z) (tokenMsg msg)
       ) ;
       (* transfer_from *)
-      (2, bindGenOpt (EIP20.gTransfer_from (token_state state))
+      (2, bindOpt (EIP20.gTransfer_from (token_state state))
           (fun '(caller, msg) =>
             call contract_addr caller (0%Z) (tokenMsg msg)
           )
       );
       (* approve *)
-      (1, bindGenOpt (EIP20.gApprove (token_state state))
+      (1, bindOpt (EIP20.gApprove (token_state state))
           (fun '(caller, msg) =>
             call contract_addr caller (0%Z) (tokenMsg msg)
           )
       );
       (* create_tokens *)
-      (5, bindGenOpt (gCreateTokensInvalid env state)
+      (5, bindOpt (gCreateTokensInvalid env state)
           (fun '(caller, value, msg) =>
             call contract_addr caller value msg
           )
@@ -222,9 +222,9 @@ Module BATGens (Info : BATGensInfo).
       which order they will be executed in)
   *)
   Definition gBATAction (env : Environment) : GOpt Action :=
-    state <- returnGen (get_contract_state BATCommon.State env contract_addr) ;;
+    state <-- returnGen (get_contract_state BATCommon.State env contract_addr) ;;
     freq [
-      (5, bindGenOpt (gBATActionValid env)
+      (5, bindOpt (gBATActionValid env)
           (fun '(action) =>
             match action.(act_body) with
             | act_transfer _ _ => returnGen None

examples/congress/tests/CongressGens.v

@@ -16,11 +16,6 @@ Definition serializeMsg := serialize Msg _.
 
 (* ChainGens for the types defined in the Congress contract *)
 
-(* Helper function *)
-Definition genToOpt {A : Type} (g : G A) : GOpt A :=
-  a <- g ;;
-  returnGenSome a.
-
 Definition gRulesSized (n : nat) : G Rules :=
   vote_count <- choose(1%Z, 1000%Z) ;;
   margin <- choose(1%Z, 1000%Z) ;;
@@ -125,9 +120,9 @@ Definition try_gNewOwner state calling_addr contract_addr : GOpt Address :=
 Definition vote_proposal (caddr : Address)
                          (members_and_proposals : FMap Address (list ProposalId))
                          (call : Address -> Address -> Msg -> GOpt Action)
-                         (vote : ProposalId -> Msg) :=
-  '(member, pids) <- sampleFMapOpt members_and_proposals ;;
-  pid <- elems_opt pids ;;
+                         (vote : ProposalId -> Msg) : GOpt Action :=
+  '(member, pids) <-- sampleFMapOpt members_and_proposals ;;
+  pid <-- elems_opt pids ;;
   call caddr member (vote pid).
 
 (* Returns a mapping to proposals which have been discussed long enough, according to the
@@ -147,34 +142,34 @@ Fixpoint GCongressAction (env : Environment)
                          (fuel : nat)
                          (caddr : Address)
                          : GOpt Action :=
-  let call contract_addr caller_addr msg :=
+  let call contract_addr caller_addr msg : GOpt Action :=
     amount <- match env.(env_account_balances) caller_addr with
-              | 0%Z => returnGenSome 0%Z
-              | caller_balance => genToOpt (choose (0%Z, caller_balance))
-              end ;;
+               | 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.State env caddr) ;;
+  congress_state <-- returnGen (get_contract_state Congress.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) ;;
+      (1, members <-- elems_opt (congressContractsMembers_nonowners congress_state) ;;
+          new_owner <-- (try_gNewOwner congress_state owner caddr) ;;
           call caddr owner (transfer_ownership new_owner)
       ) ;
       (* change_rules *)
-      (1, rules <- genToOpt (gRulesSized 4) ;;
+      (1, rules <- gRulesSized 4 ;;
           (call caddr owner (change_rules rules))
       ) ;
       (* add_member *)
-      (2, addr <- returnGen (try_newCongressMember congress_state caddr 10) ;;
+      (2, addr <-- returnGen (try_newCongressMember congress_state caddr 10) ;;
           call caddr owner (add_member addr)
       ) ;
       (* remove_member *)
-      (1, member <- elems_opt members ;;
+      (1, member <-- elems_opt members ;;
           call caddr owner (remove_member member)
       ) ;
       (* vote_for_proposal *)
@@ -193,7 +188,7 @@ Fixpoint GCongressAction (env : Environment)
       (* Requirements:
          - only contract owner can finish proposals
          - the debating period must have passed *)
-      (2, '(pid, _) <- sampleFMapOpt (finishable_proposals congress_state env.(current_slot)) ;;
+      (2, '(pid, _) <-- sampleFMapOpt (finishable_proposals congress_state env.(current_slot)) ;;
           call caddr owner (finish_proposal pid)
       )
     ]
@@ -207,13 +202,14 @@ Fixpoint GCongressAction (env : Environment)
       (* 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 ;;
+      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 ;;
+        member <-- elems_opt members ;;
         let ca := cact_call caddr amount msg in
-        call caddr member (create_proposal [ca])
+        returnGenSome ( act)
+        (* call caddr member (create_proposal [ca]) *)
       | _ => returnGenSome act
       end)
   ]

examples/congress/tests/Congress_BuggyGens.v

@@ -33,12 +33,6 @@ Instance genSetupSized : GenSized Setup :=
 
 (* ------------------ generators of actions --------------------------- *)
 
-(* helpers *)
-
-Definition genToOpt {A : Type} (g : G A) : GOpt A :=
-  a <- g ;;
-  returnGenSome a.
-
 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
@@ -96,18 +90,18 @@ Definition try_gNewOwner state calling_addr contract_addr : GOpt Address :=
 
 Definition validate_addr (a : Address) : GOpt (address_is_contract a = false) :=
   match (Bool.bool_dec (address_is_contract a) true ) with
-  | left _ => ret None
-  | right p => ret (Some (Bool.not_true_is_false _ p))
+  | 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) :=
-  '(member, pids) <- sampleFMapOpt members_and_proposals ;;
-  p <- validate_addr member ;;
-  pid <- elems_opt pids ;;
+                         (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
@@ -161,36 +155,36 @@ Fixpoint GCongressAction (env : Environment)
                          : GOpt Action :=
   let call contract_addr caller_addr caller_addr_is_user msg :=
     amount <- match env.(env_account_balances) caller_addr with
-              | 0%Z => returnGenSome 0%Z
-              | caller_balance => genToOpt (choose (0%Z, caller_balance))
+              | 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) ;;
+  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 ;;
+      (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 <- genToOpt (gRulesSized 4) ;;
-          p <- validate_addr owner ;;
+      (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 ;;
+      (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 ;;
+      (1, member <-- elems_opt members ;;
+          p <-- validate_addr owner ;;
           call caddr owner p (remove_member member)
       ) ;
       (* vote_for_proposal *)
@@ -209,8 +203,8 @@ Fixpoint GCongressAction (env : Environment)
       (* 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 ;;
+      (2, '(pid, _) <-- sampleFMapOpt (finishable_proposals congress_state env.(current_slot)) ;;
+          p <-- validate_addr owner ;;
           call caddr owner p (finish_proposal pid)
       )
     ]
@@ -224,13 +218,13 @@ Fixpoint GCongressAction (env : Environment)
       (* 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 ;;
+      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 ;;
+        member <-- elems_opt members ;;
         let ca := cact_call caddr amount msg in
-        p <- validate_addr member ;;
+        p <-- validate_addr member ;;
         call caddr member p (create_proposal [ca])
       | _ => returnGenSome act
       end)