gcd.v 2.86 KB
Newer Older
1
From iris_c.vcgen Require Import proofmode.
2

Robbert Krebbers's avatar
Robbert Krebbers committed
3
Definition gcd : val := λᶜ "x",
4 5 6 7 8
  "a" ←ᶜ c_ret (Fst "x");
  "b" ←ᶜ c_ret (Snd "x");
  while(∗ᶜ(c_ret "a") != ∗ᶜ(c_ret "b")) {
    if (∗ᶜ(c_ret "a") < ∗ᶜ(c_ret "b")) {
      (c_ret "b") = ∗ᶜ(c_ret "b") - ∗ᶜ(c_ret "a")
9
    } else {
10
      (c_ret "a") = ∗ᶜ(c_ret "a") - ∗ᶜ(c_ret "b")
11
    }
12
  }; ∗ᶜ(c_ret "a").
13

14 15 16 17 18 19 20 21 22 23 24 25 26 27
(* A contrived version of gcd that uses side-effects in expressions from
Krebbers's PhD thesis (p170). Note that instead of gotos, we use an ordinary
while loop. *)
Definition gcd_robbert_thesis : val := λᶜ "x",
  "a" mut c_ret (Fst "x");
  "b" mut c_ret (Snd "x");
  while(0 != ∗ᶜ(c_ret "b")) {
    "tmp" mut 0 ;
    c_ret "b" = (c_ret "tmp" = c_bin_op (CBinOp RemOp)
                                   (∗ᶜ(c_ret "a")) (∗ᶜ(c_ret "b"));
                  c_ret "a" = ∗ᶜ(c_ret "b");
                  ∗ᶜ(c_ret "tmp"))
  }; ∗ᶜ(c_ret "a").

28
Section gcd_spec.
29
  Context `{cmonadG Σ}.
30

31
  Lemma gcd_spec l r a b R :
Robbert Krebbers's avatar
Robbert Krebbers committed
32
    0  a  0  b 
33
    l C #a - r C #b -
34
    CWP gcd (cloc_to_val l, cloc_to_val r)%V @ R {{ v, v = #(Z.gcd a b) }}.
35
  Proof.
36 37
    iIntros (??) "**". iApply cwp_fun; simpl. vcg; iIntros.
    iApply (cwp_whileV_inv ( x y : Z,
38 39 40 41 42 43
      0  x  0  y  Z.gcd x y = Z.gcd a b  l C #x  r C #y)%I with "[-]").
    { iExists a, b. eauto with iFrame. }
    iModIntro. iDestruct 1 as (x y (?&?&Hgcd)) "[??]". vcg. iIntros "** /=".
    case_bool_decide; simpl; [iLeft | iRight]; iSplit; eauto.
    + repeat iModIntro. vcg_continue. simplify_eq/=.
      rewrite -Hgcd Z.gcd_diag Z.abs_eq; eauto with iFrame.
44
    + iModIntro. iApply cwp_if. vcg. iIntros "** /=".
Dan Frumin's avatar
Dan Frumin committed
45
      case_bool_decide; simpl; [ iLeft | iRight ];
46 47 48 49 50
        (iSplit; first done); iModIntro.
      * vcg. iIntros "** !>". iExists x, (y - x); iFrame.
        iPureIntro. rewrite Z.gcd_sub_diag_r. lia.
      * vcg. iIntros "** !>". iExists (x-y), y; iFrame.
        iPureIntro. rewrite Z.gcd_comm Z.gcd_sub_diag_r Z.gcd_comm. lia.
51
  Qed.
52 53 54 55 56 57 58 59 60 61 62 63 64 65 66

  Lemma gcd_robbert_thesis_spec (a b : nat) R :
    CWP gcd_robbert_thesis (#a, #b)%V @ R {{ v, v = #(Nat.gcd a b) }}%I.
  Proof.
    iApply cwp_fun; simpl. vcg; iIntros (p q) "**". iApply (cwp_wand _ (λ _,
      p C #(Nat.gcd a b)  q C #0)%I with "[-]"); last first.
    { iIntros (v) "[??]". vcg_continue; auto. }
    iInduction (lt_wf b) as [[|b] _] "IH" forall (a).
    { vcg. iIntros "!> !> **". rewrite Nat.gcd_0_r. iFrame. }
    vcg. iIntros "!> !>" (t) "!> **".
    rewrite Z.rem_mod_nonneg; [|lia..]; rewrite -Z2Nat_inj_mod.
    iApply (cwp_wand with "(IH [%] [$] [$])"); [by apply Nat.mod_upper_bound|].
    iIntros (v) "[??]". rewrite Nat.gcd_comm Nat.gcd_mod // Nat.gcd_comm.
    vcg_continue. auto with iFrame.
  Qed.
67
End gcd_spec.