QuickChick - Property-Based Testing

QuickChick is a property-based testing tool for Coq that automatically generates test cases. Ursus integrates with QuickChick to complement formal verification with automated testing.

What is QuickChick?

QuickChick:

• Generates random test inputs automatically
• Tests properties on many examples
• Finds counterexamples when properties fail
• Complements proofs with empirical validation

Enabling QuickChick

Contract Attribute

Enable QuickChick for a contract:

#[quickchick = on]
#[translation = on]
#[language = solidity]
Contract MyContract ;

Property Definition

Define testable properties:

Definition prop_transfer_preserves_total (from to: address) (amount: uint256) :=
  forall s,
    let s' := exec_transfer from to amount s in
    total_supply s' = total_supply s.

Running Tests

coqc -Q . MyProject MyContract.v
./test_MyContract

Property-Based Testing

Example: Transfer Properties

(* Property: Balance decreases for sender *)
Definition prop_transfer_decreases_sender_balance
  (from to: address) (amount: uint256) (s: ContractState) :=
  balance s from >= amount ->
  let s' := exec_transfer from to amount s in
  balance s' from = balance s from - amount.

(* Property: Balance increases for recipient *)
Definition prop_transfer_increases_recipient_balance
  (from to: address) (amount: uint256) (s: ContractState) :=
  from <> to ->
  balance s from >= amount ->
  let s' := exec_transfer from to amount s in
  balance s' to = balance s to + amount.

(* Property: Total supply unchanged *)
Definition prop_transfer_preserves_total_supply
  (from to: address) (amount: uint256) (s: ContractState) :=
  let s' := exec_transfer from to amount s in
  total_supply s' = total_supply s.

QuickChick Annotations

(* Mark property for testing *)
QuickChick prop_transfer_preserves_total_supply.

(* Custom generators *)
Instance genAddress : Gen address := ...
Instance genUint256 : Gen uint256 := ...
Instance genContractState : Gen ContractState := ...

Generators

Built-in Generators

QuickChick provides generators for basic types:

Gen bool        (* Random booleans *)
Gen nat         (* Random natural numbers *)
Gen Z           (* Random integers *)
Gen list A      (* Random lists *)

Custom Generators

Define generators for contract types:

(* Generate random address *)
Instance genAddress : Gen address :=
  {| arbitrary :=
       a <- arbitrary;
       returnGen (mkAddress a)
  |}.

(* Generate random uint256 *)
Instance genUint256 : Gen uint256 :=
  {| arbitrary :=
       n <- choose (0, 2^256 - 1);
       returnGen (N_to_uint256 n)
  |}.

(* Generate random contract state *)
Instance genContractState : Gen ContractState :=
  {| arbitrary :=
       supply <- arbitrary;
       balances <- arbitrary;
       returnGen (mkContractState supply balances)
  |}.

Shrinking

When a test fails, QuickChick tries to find a minimal counterexample:

Instance shrinkUint256 : Shrink uint256 :=
  {| shrink n :=
       if n > 0 then [n / 2; n - 1] else []
  |}.

Testing vs. Proving

Best practice: Use both!

1. QuickChick - Find bugs quickly
2. Proofs - Guarantee correctness

Example Workflow

Step 1: Write Property

Definition prop_no_overflow (x y: uint256) :=
  x + y >= x.

Step 2: Test with QuickChick

QuickChick prop_no_overflow.

Output:

QuickChecking prop_no_overflow
*** Failed after 42 tests and 0 shrinks. (0 discards)
Counterexample: x = 2^256 - 1, y = 1

Step 3: Fix Implementation

Definition safe_add (x y: uint256) : option uint256 :=
  let result := x + y in
  if result >= x then Some result else None.

Step 4: Prove Correctness

Theorem safe_add_no_overflow:
  forall x y result,
    safe_add x y = Some result ->
    result >= x /\ result >= y.
Proof.
  (* Formal proof *)
Qed.

See Also

• Verification Overview - Introduction to verification
• Verification Principles - Core concepts
• QuickChick official documentation - Property-based testing framework