Skip to main content

Demo: verifying fibonacci function

10/21/24demoliterate

Demo: verifying fibonacci function

The Coq code for this file is at src/sys_verif/program_proof/demos/fibonacci_proof.v.

The code in go/functional/functional.go implements func Fibonacci(n uint6) uint64, computing the nth Fibonacci number.

We prove this function correct, proving that the imperative, loop-based implementation Go is equivalent to a recursive, functional implementation in Gallina.

From sys_verif.program_proof Require Import prelude empty_ffi.
From sys_verif.program_proof Require Import functional_init.

Section proof.
Context `{hG: !heapGS Σ}.
Context `{!globalsGS Σ} {go_ctx: GoContext}.

Fixpoint fibonacci (n: nat): nat :=
  match n with
  | 0 => 0
  | 1 => 1
  (* a little care is needed for Coq to accept that this function terminates *)
  | S (S n_minus_2 as n_minus_1) => fibonacci n_minus_2 + fibonacci n_minus_1
  end%nat.

We will need some helper lemmas. These are only required because the specification will assume that the final result doesn't overflow, and we will use that to show that the intermediate results also don't overflow.

Lemma fibonacci_S i :
  (1 ≤ i)%nat →
  fibonacci (S i) = (fibonacci i + fibonacci (i-1))%nat.
Proof.
  intros Hle.
  destruct i; simpl.
  { lia. (* contradicts assumption *) }
  replace (i - 0)%nat with i by lia.
  lia.
Qed.

Lemma fibonacci_monotonic i1 i2 :
  (i1 ≤ i2)%nat →
  fibonacci i1 ≤ fibonacci i2.
Proof.
  intros Hle.
  destruct (decide (i1 = i2)).
  { subst; lia. }

  assert (∃ d, i2 = S (d + i1)) as H.
  { exists (i2 - i1 - 1)%nat. lia. }
  destruct H as [d ?]; subst.

  move: Hle.
  clear.
  induction d.
  - destruct i1; simpl; lia.
  - simpl in *; lia.
Qed.

Lemma if_decide_bool_decide_eq_true (P: Prop) `{!Decision P}
  {A} (x y: A) :
  (if decide (# (bool_decide P) = #true) then x else y) =
  if decide P then x else y.
Proof.
  destruct (decide P).
  - rewrite decide_True //.
    rewrite bool_decide_eq_true_2 //.
  - rewrite decide_False //.
    rewrite bool_decide_eq_false_2 //.
    rewrite to_val_unseal /to_val_def /=.
    congruence.
Qed.

Lemma if_decide_bool_decide_eq_false (P: Prop) `{!Decision P}
  {A} (x y: A) :
  (if decide (# (bool_decide P) = #false) then x else y) =
  if decide P then y else x.
Proof.
  destruct (decide P).
  - rewrite decide_False //.
    rewrite bool_decide_eq_true_2 //.
    rewrite to_val_unseal /to_val_def /=.
    congruence.
  - rewrite decide_True //.
    rewrite bool_decide_eq_false_2 //.
Qed.

Here is the statement of what it means for Fibonacci (the Go function) to be correct.

Lemma wp_Fibonacci (n: w64) :
  {{{ is_pkg_init functional ∗ ⌜Z.of_nat (fibonacci (uint.nat n)) < 2^64⌝ }}}
    @! functional.Fibonacci #n
  {{{ (c: w64), RET #c; ⌜uint.nat c = fibonacci (uint.nat n)⌝ }}}.
Proof.
  wp_start as "%Hoverflow".
  wp_alloc n_l as "n"; wp_auto.
  wp_if_destruct.
  { iApply "HΦ".
    iPureIntro.
    reflexivity.
  }
  wp_auto.

The core of the proof's argument is this loop invariant about the prev and cur variables.

  iAssert (∃ (i prev cur: w64),
              "fib_prev" ∷ fib_prev_ptr ↦ prev ∗
              "fib_cur" ∷ fib_cur_ptr ↦ cur ∗
              "i" ∷ i_ptr ↦ i ∗
              "%Hi_ge" ∷ ⌜1 ≤ uint.Z i ≤ uint.Z n⌝ ∗
              "%Hprev" ∷ ⌜uint.nat prev = fibonacci (uint.nat i - 1)⌝ ∗
              "%Hcur" ∷ ⌜uint.nat cur = fibonacci (uint.nat i)⌝
            )%I
            with "[$i $fib_prev $fib_cur]" as "IH".
  { iPureIntro.
    split.
    { word. }
    split.
    { reflexivity. }
    reflexivity. }
  wp_for; iNamed "IH"; wp_auto.
  - rewrite if_decide_bool_decide_eq_true //.
    destruct (decide _); try wp_auto.
    + iApply wp_for_post_do. wp_auto.
      iFrame.
      iPureIntro.
      split.
      * word.
      * split.
        { rewrite Hcur. f_equal; word. }
        replace (uint.nat (word.add i (W64 1))) with
          (S (uint.nat i)) by word.
        rewrite fibonacci_S; [ word | ].
        (* we need to show the [word.add] doesn't overflow to finish the proof *)
        assert (uint.Z cur + uint.Z prev < 2^64) as Hsum.
        {
          (* to prove this, we'll use the fact that [uint.nat cur + uint.nat
      prev = fibonacci (S i)], and that [fibonacci] is monotonic. We know that
      [i < n] as part of the loop invariant. *)
          pose proof (fibonacci_monotonic (S (uint.nat i)) (uint.nat n)) as Hi_n.
          rewrite -> fibonacci_S in Hi_n by word.
          word. }
        word.
    + rewrite if_decide_bool_decide_eq_false //.
      destruct (decide _); try wp_auto.
      { word. }
      iApply "HΦ".
      iPureIntro.
      assert (uint.Z i = uint.Z n) by word.
      congruence.
Qed.

End proof.
Last Updated