gcd.v 1.61 KB
Newer Older
1 2
From iris_c.vcgen Require Import vcg_solver.
Local Open Scope Z_scope.
3

4
(* TODO: Notation, get rid of parenthesis around the while loop *)
5
Definition gcd : val := λ: "a" "b",
6 7 8 9 10 11 12 13
   (while (∗ᶜ(a_ret "a") != ∗ᶜ(a_ret "b")) {
     if (∗ᶜ(a_ret "a") < ∗ᶜ(a_ret "b")) {
       (a_ret "b") = ∗ᶜ(a_ret "b") - ∗ᶜ(a_ret "a")
     } else {
       (a_ret "a") = ∗ᶜ(a_ret "a") - ∗ᶜ(a_ret "b")
     }
   }) ;
   ∗ᶜ(a_ret "a").
14 15

Section gcd_spec.
16
  Context `{amonadG Σ}.
17

18
  (* TODO: use callᶜ *)
Dan Frumin's avatar
Dan Frumin committed
19
  Lemma gcd_spec (a b : Z) (l r: cloc) R :
Robbert Krebbers's avatar
Robbert Krebbers committed
20
    0  a  0  b 
21
    l C #a - r C #b -
Dan Frumin's avatar
Dan Frumin committed
22
    awp (gcd (cloc_to_val l) (cloc_to_val r)) R (λ v, v = #(Z.gcd a b)).
23
  Proof.
24 25 26
    iIntros (??) "Hl Hr". unfold gcd. do 2 awp_lam.
    (* vcg_solver. *)
    (* iIntros "Hr Hl". *)
27
    iApply a_sequence_spec'.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
    iApply (a_while_inv_spec ( x y : Z,
29
      0  x  0  y  Z.gcd x y = Z.gcd a b  l C #x  r C #y)%I with "[Hl Hr]").
Robbert Krebbers's avatar
Robbert Krebbers committed
30
    - iExists a, b. eauto with iFrame.
31
    - iModIntro.  iDestruct 1 as (x y (?&?&Hgcd)) "[Hl Hr]".
32 33 34 35 36 37 38 39 40 41 42 43 44 45
      vcg_solver.
      iIntros "Hr Hl /=".
      case_bool_decide; simpl; [ iLeft | iRight ];
        iSplit; eauto.
      + repeat iModIntro. vcg_solver.
        rewrite Qp_half_half. simplify_eq/=.
        rewrite -Hgcd Z.gcd_diag Z.abs_eq; eauto with iFrame.
      + iNext. iApply a_if_spec'.
        vcg_solver. rewrite !Qp_half_half.
        iIntros "Hl Hr /=".
        case_bool_decide; simpl; [ iLeft | iRight ];
          (iSplit; first done);
          vcg_solver;
          eauto 400 with iFrame.
46 47
  Qed.
End gcd_spec.