Verifying factorial in C with Coq

factorial.c

#include <stddef.h>

unsigned factorial(unsigned n) {
  unsigned acc = 1;
  unsigned y = 0;
  while(y < n) {
    y++;
    acc *= y;
  }
  return acc;
}

int main(void) {
  unsigned int x;
  x = factorial(6);
  return (int)x;
}

run.sh

#! /usr/bin/env nix-shell
#! nix-shell -i bash -p coq_8_13 coqPackages.VST compcert
#! nix-shell -I nixpkgs=https://github.com/NixOS/nixpkgs/archive/432fc2d9a67f92e05438dff5fdc2b39d33f77997.tar.gz
set -uex

clightgen -normalize factorial.c
coqc factorial.v
coqc Verif_factorial.v

Verif_factorial.v

Require Import VST.floyd.proofauto.
Require Import VST.floyd.library.
Require Import factorial.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs.  mk_varspecs prog. Defined.

(* First we right down a specification of factorial in Coq that
   operates on integers. We need to prove that it terminates as well. *)
Function factorial (n: Z) { measure Z.to_nat n } :=
 if Z_gt_dec n 0 then n * factorial (n-1) else 1.
Proof.
lia.
Defined.

(* Note: C identifiers are prefixed with _*)
(* Next we provide a specification for the C function factorial *)
Definition factorial_spec : ident * funspec :=
DECLARE _factorial
(* Variables in the WITH clause are visible in the whole declaration *)
 WITH n : Z
(* Input value has type unsigned int  *)
 PRE [ tuint ]
(* n must be less than max_unsigned *)
  PROP  (0 <= n <= Int.max_unsigned)
(* The input's value is n *)
  PARAMS (Vint (Int.repr n))
(* No spatial memory conditions *)
  SEP   ()

(* The return value has type unsigned int *)
 POST [ tuint ]
 PROP ()
(* We assert that the return value is n! *)
  RETURN (Vint (Int.repr (factorial n)))
  SEP ().

(* We also give a spec for the main function *)
Definition main_spec :=
 DECLARE _main
 WITH gv: globals
 PRE [ ] main_pre prog tt gv
 POST [ tint ]
   PROP ()
   RETURN (Vint (Int.repr (factorial 6)))
   SEP (TT).

(* Gprog ties it all together. *)
Definition Gprog : funspecs :=
  ltac:(with_library prog [ factorial_spec; main_spec ]).

(* Prove that factorial in C satisfies its spec. *)
Lemma body_factorial: semax_body Vprog Gprog f_factorial factorial_spec.
Proof.
(* All semax_body proofs begin this way *)
  start_function.
(* unsigned _acc = 1; *)
  forward.
(* unsigned _y = 0; *)
  forward.
(* Hit a while loop, have to provide a loop invariant to proceed. *)
(* The loop invariant says that there is an integer y such that
   (PROP) 0 <= y <= n
   (LOCAL) the identifier _y holds the value of y
           the identifier _n holds the value of n
           the identifier  _acc holds the factorial of y.
   (SEP) There are no memory separation assertions.
*)
  forward_while
   (EX y: Z,
     PROP  (0 <= y <= n)
     LOCAL (temp _y (Vint (Int.repr y));
            temp _n (Vint (Int.repr n));
            temp _acc (Vint (Int.repr (factorial y))))
     SEP   ()).
(* forward_while generates 4 subgoals *)
(* First we prove that the loop invariant holds on entry to the loop *)
  - Exists 0.
    entailer!.
(* Next we prove that the loop test (y < n) evaluates without crashing
   (this is usually trivial). *)
  - entailer!.
(*
  Now the proof state looks like this

  Espec : OracleKind
  n : Z
  Delta_specs : PTree.t funspec
  Delta := abbreviate : tycontext
  H : 0 <= n <= Int.max_unsigned
  y : Z
  HRE : y < n
  H0 : 0 <= y <= n
  POSTCONDITION := abbreviate : ret_assert
  MORE_COMMANDS := abbreviate : statement
  ============================
  semax Delta
    (PROP ( )
     LOCAL (temp _y (Vint (Int.repr y)); temp _n (Vint (Int.repr n));
     temp _acc (Vint (Int.repr (factorial y))))  SEP ())
    (_y = (_y + (1));
     MORE_COMMANDS) POSTCONDITION

  We are proving that if the loop invariant holds up to a certain
  point, it also holds in the next iteration. Note we have helpful
  assumptions in context (HRE, H0).

*)
  - forward.
    forward.
    Exists (y + 1).
    entailer!.
(* Now we have to prove

  Vint (Int.repr (factorial (y + 1)))
= Vint (Int.repr (factorial y * (y + 1)))

  this is pretty trivial.
*)
    do 2 f_equal.
    rewrite factorial_equation.
    replace (y + 1 - 1) with y by lia.
    destruct (Z_gt_dec _ _); try lia.
(* Finally, after the loop we have that _acc := y!, _y := y and _n := n.

  ...
  HRE : y >= n
  H0 : 0 <= y <= n
  ============================
  semax Delta
    (PROP ( )
     LOCAL (temp _y (Vint (Int.repr y)); temp _n (Vint (Int.repr n));
     temp _acc (Vint (Int.repr (factorial y))))  SEP ())
    (return _acc;) POSTCONDITION

  POSTCONDITION is an abbreviation for the assertion that the
  factorial function returns n!  Note that HRE and H0 together imply
  y = n, so _acc := n! as desired.
*)
  - assert (y = n) by lia.
    forward.
Qed.

Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
Proof.
  start_function.
(* x = factorial(6); *)
  forward_call.
(* Need to show function precondition is satisfied:
   (0 <= 6 <= Int.max_unsigned), this is trivial. *)
  - computable.
(* Now forward through a return x to prove main returns 6!. *)
  - forward.
Qed.

(* Use a trivial external specification since we don't do any external
   I/O. *)
Existing Instance NullExtension.Espec.

(* Prove that the whole program prog is correct. *)
Lemma prog_correct: semax_prog prog tt Vprog Gprog.
Proof.
  prove_semax_prog.

  semax_func_cons body_factorial.
  semax_func_cons body_main.
Qed.

Goal True.
idtac "factorial is verified".
Abort.