gcd.v 1.94 KB
Newer Older
1 2 3 4 5
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.algebra Require Import frac auth.
From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.c_translation Require Import proofmode translation derived.
Dan Frumin's avatar
Dan Frumin committed
6 7
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.

8
Require Import Coq.ZArith.Znumtheory.
9

Dan Frumin's avatar
Dan Frumin committed
10
(* TODO: Notation, get rid of parenthesis around the while loop *)
11
Definition gcd : val := λ: "a" "b",
Dan Frumin's avatar
Dan Frumin committed
12 13 14 15 16 17 18 19
   (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").
20 21

Section gcd_spec.
22
  Context `{amonadG Σ}.
23

Dan Frumin's avatar
Dan Frumin committed
24
  (* TODO: use callᶜ *)
Dan Frumin's avatar
Dan Frumin committed
25
  Lemma gcd_spec (a b : Z) (l r: cloc) R :
Robbert Krebbers's avatar
Robbert Krebbers committed
26
    0  a  0  b 
27
    l C #a - r C #b -
Dan Frumin's avatar
Dan Frumin committed
28
    awp (gcd (cloc_to_val l) (cloc_to_val r)) R (λ v, v = #(Z.gcd a b)).
29
  Proof.
Dan Frumin's avatar
Dan Frumin committed
30 31 32 33
    iIntros (??) "Hl Hr". unfold gcd. do 2 awp_lam.
    (* vcg_solver. *)
    (* iIntros "Hr Hl". *)
    iApply a_sequence_spec'. iNext.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
    iApply (a_while_inv_spec ( x y : Z,
35
      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
36
    - iExists a, b. eauto with iFrame.
37
    - iModIntro.  iDestruct 1 as (x y (?&?&Hgcd)) "[Hl Hr]".
Dan Frumin's avatar
Dan Frumin committed
38 39 40 41 42 43 44 45 46 47 48 49 50 51
      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.
52 53
  Qed.
End gcd_spec.