Example: Computing the Difference Between Two Integers
The following example computes the absolute difference between two integers.
int delta(int x, int y)
/*@ Require
0 <= x && x <= 100 &&
0 <= y && y <= 100 &&
emp
Ensure
__return == Z::abs(x - y) && emp
*/
{
if (x < y) {
return y - x;
}
else {
return x - y;
}
}
The specification uses the mathematical function Z::abs, which represents absolute value on integers. It corresponds to Z.abs from the Rocq standard library. To use external Rocq definitions in QCP specifications, we declare them with Extern Coq.
/*@ Extern Coq (Z::abs: Z -> Z) */
When QCP verifies this function, it generates two VCs:
x_319_pre < y_316_pre &&
0 <= x_319_pre && x_319_pre <= 100 &&
0 <= y_316_pre && y_316_pre <= 100
|-- y_316_pre - x_319_pre == Z.abs(x_319_pre - y_316_pre)
x_319_pre >= y_316_pre &&
0 <= x_319_pre && x_319_pre <= 100 &&
0 <= y_316_pre && y_316_pre <= 100
|-- x_319_pre - y_316_pre == Z.abs(x_319_pre - y_316_pre)
The proofs depend on the definition of Z.abs, so QCP cannot prove them automatically.
The user must prove these VCs in Rocq. QCP generates four Rocq files:
delta_goal.v
delta_proof_auto.v
delta_proof_manual.v
delta_goal_check.v
The first file describes all VCs. The second file contains the conclusions that QCP can prove automatically. Both are generated by QCP. The third file contains the VCs that QCP cannot prove automatically, and the user should complete proofs there. The fourth file checks that all VCs from the goal file are proved by either the automatic or manual proof file.
Generating Rocq Files and Completing Proofs
The following command generates the four Rocq files:
symexec --goal-file=delta_goal.v --proof-auto-file=delta_proof_auto.v --proof-manual-file=delta_proof_manual.v --input-file=delta.c
In the web IDE, the user can also click the CoqProofGen button to obtain these files.
The symbolic execution of delta generates two manually proved VCs. In delta_goal.v, they are represented as definitions of propositions.
Definition delta_return_wit_1_split_goal_1 :=
forall (y_pre: Z) (x_pre: Z)
(PreH1: x_pre >= y_pre)
(PreH2: 0 <= x_pre)
(PreH3: x_pre <= 100)
(PreH4: 0 <= y_pre)
(PreH5: y_pre <= 100),
x_pre - y_pre = Z.abs (x_pre - y_pre).
Definition delta_return_wit_2_split_goal_1 :=
forall (y_pre: Z) (x_pre: Z)
(PreH1: x_pre <> y_pre)
(PreH2: 0 <= x_pre)
(PreH3: x_pre <= 100)
(PreH4: 0 <= y_pre)
(PreH5: y_pre <= 100),
x_pre - y_pre = Z.abs (y_pre - x_pre).
QCP generates a rough skeleton in delta_proof_manual.v.
Lemma proof_of_delta_return_wit_1_split_goal_1:
delta_return_wit_1_split_goal_1.
Proof. Abort.
Lemma proof_of_delta_return_wit_2_split_goal_1:
delta_return_wit_2_split_goal_1.
Proof. Abort.
The two VCs are simple and can be proved as follows:
Lemma proof_of_delta_return_wit_1_split_goal_1:
delta_return_wit_1_split_goal_1.
Proof. pre_process. lia. Qed.
Lemma proof_of_delta_return_wit_2_split_goal_1:
delta_return_wit_2_split_goal_1.
Proof. pre_process. lia. Qed.
Here pre_process is a Rocq proof command provided by QCP that unfolds the VC proposition, and lia is Rocq's automated tactic for linear arithmetic.
Example: Checking Whether a Number Is Prime
The following example checks whether a number is prime.
int test_prime(unsigned int x)
/*@ Require
0 <= x && x <= 1000000000 && emp
Ensure
((__return == 1 && prime(x)) ||
(__return == 0 && (! prime(x)))) && emp
*/
{
if (x < 2) {
return 0;
}
int d;
for (d = 2; d * d <= x; d++) {
if (x % d == 0) {
return 0;
}
}
return 1;
}
The specification uses the predicate prime, where prime(x) states that x is a prime number. Since this program contains a loop, we add a loop invariant.
int test_prime(unsigned int x)
/*@ Require
0 <= x && x <= 1000000000 && emp
Ensure
((__return == 1 && prime(x)) ||
(__return == 0 && (! prime(x)))) && emp
*/
{
if (x < 2) {
return 0;
}
int d;
/*@ Inv Assert
x == x@pre &&
2 <= d && d <= 31624 &&
2 <= x@pre && x@pre <= 1000000000 &&
(! HasFactorBetween(x@pre, 2, d))
*/
for (d = 2; d * d <= x; d++) {
if (x % d == 0) {
return 0;
}
}
return 1;
}
The predicate HasFactorBetween(x, low, high) means that x has at least one factor in the interval [low, high - 1]. Unlike Z::abs and prime, this predicate is not from the Rocq standard library; it is a custom definition used for this invariant. We can define it in a Rocq file test_prime_lib.v:
Definition HasFactorBetween (x lo hi: Z): Prop :=
exists k, lo <= k /\ k < hi /\ Z.divide k x.
Then the C file imports the predicate and declares both prime and HasFactorBetween:
/*@ Import Coq Require Import test_prime_lib */
/*@ Extern Coq (prime: Z -> Prop)
(HasFactorBetween: Z -> Z -> Z -> Prop) */
With these declarations, the four Rocq files generated by QCP can refer to test_prime_lib.v and use the definition of HasFactorBetween.
test_prime_goal.v
test_prime_proof_auto.v
test_prime_proof_manual.v
test_prime_goal_check.v
For example, the following VCs must be manually proved in Rocq to verify the functional correctness of test_prime.
Definition test_prime_entail_wit_1_split_goal_1 :=
forall (x_pre: Z)
(PreH1: x_pre >= 2)
(PreH2: 0 <= x_pre)
(PreH3: x_pre <= 1000000000),
~ HasFactorBetween x_pre 2 2.
Definition test_prime_entail_wit_2_split_goal_1 :=
forall (x_pre: Z) (d: Z)
(PreH1: x_pre % d <> 0)
(PreH2: d * d <= x_pre)
(PreH3: 2 <= d)
(PreH4: d <= 31624)
(PreH5: 2 <= x_pre)
(PreH6: x_pre <= 1000000000)
(PreH7: ~ HasFactorBetween x_pre 2 d),
~ HasFactorBetween x_pre 2 (d + 1).
Definition test_prime_return_wit_3_split_goal_1 :=
forall (x_pre: Z)
(PreH1: x_pre < 2)
(PreH2: 0 <= x_pre)
(PreH3: x_pre <= 1000000000),
~ prime x_pre.
Definition test_prime_return_wit_2_split_goal_1 :=
forall (x_pre: Z) (d: Z)
(PreH1: x_pre % d = 0)
(PreH2: d * d <= x_pre)
(PreH3: 2 <= d)
(PreH4: d <= 31624)
(PreH5: 2 <= x_pre)
(PreH6: x_pre <= 1000000000)
(PreH7: ~ HasFactorBetween x_pre 2 d),
~ prime x_pre.
Definition test_prime_return_wit_1_split_goal_1 :=
forall (x_pre: Z) (d: Z)
(PreH1: d * d > x_pre)
(PreH2: 2 <= d)
(PreH3: d <= 31624)
(PreH4: 2 <= x_pre)
(PreH5: x_pre <= 1000000000)
(PreH6: ~ HasFactorBetween x_pre 2 d ),
prime x_pre.
The declaration prime: Z -> Prop means that prime is a unary predicate on integers. Given an integer argument, it produces a proposition. Similarly, HasFactorBetween is a ternary predicate on integers, so its type is Z -> Z -> Z -> Prop.
The manual VCs required for delta and test_prime are still relatively simple: they involve basic mathematical properties rather than separation-logic reasoning. Later tutorials and real verification tasks can involve more complex VCs.