gcd.v 3.58 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.
6
Require Import Coq.ZArith.Znumtheory.
7

8 9 10 11 12 13 14 15 16 17
Definition gcd : val := λ: "a" "b",
   (a_while
     (λ:<>, a_un_op NegOp
              (a_bin_op EqOp (a_load (a_ret "a")) (a_load (a_ret "b"))))
     (λ:<>, a_if (a_bin_op LtOp (a_load (a_ret "a")) (a_load (a_ret "b")))
            (λ:<>, a_store (a_ret "b")
             ((a_bin_op MinusOp (a_load (a_ret "b")) (a_load (a_ret "a")))))
            (λ:<>, a_store (a_ret "a")
             ((a_bin_op MinusOp (a_load (a_ret "a")) (a_load (a_ret "b")))))))
     ;;;; a_load (a_ret "a").
18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42


Section gcd_spec.
  Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.

  Lemma gcd_spec (a b : Z) (l r: loc) R:
    a >= 0 - b >= 0 -
    l U #a - r U #b -
    awp (gcd #l #r) R (λ v, v = #(Z.gcd a b)).
  Proof.
    iIntros "% % Hl Hr".
    do 2 awp_lam. iApply a_sequence_spec.
    iApply (a_while_inv_spec
              ( (x y: Z),  l U #x  r U #y 
                            x >= 0  y >= 0  Zgcd x y = Zgcd a b)%I
              with "[Hl Hr]").
    - eauto with iFrame.
    - iModIntro. iIntros "H".  iDestruct "H" as (x y) "(Hl & Hr & % & % & %)".
      iApply a_un_op_spec.
      iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
      assert (Hxy: x = y  x < y  y < x) by lia.
      destruct Hxy as [Hxy|[Hxy|Hxy]].
      + iExists #true. simplify_eq /=. iSplit.
        { rewrite/ bin_op_eval //=; case_bool_decide; eauto. }
        iExists #false; iSplit; first done. iLeft; iSplit; first done.
43
        do 2 iModIntro. awp_seq. awp_load_ret l. iIntros.
44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
        rewrite- H5. iPureIntro. symmetry. rewrite Z.gcd_diag.
        rewrite Z.abs_eq; eauto with lia.
      + iExists #false.  simplify_eq /=. iSplit.
        { rewrite/ bin_op_eval //=.
          case_bool_decide. inversion H6; subst. lia. eauto. }
        iExists #true;  iSplit; first done. iRight; iSplit; first done.
        iApply a_if_spec.
        iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
        iExists #true; iSplit.
        { rewrite/ bin_op_eval //=. case_bool_decide; eauto. }
        iLeft. iSplit; first done. awp_seq.
        iApply a_store_ret.
        iApply (awp_bin_op_load_load with "[$Hr] [$Hl]"). iIntros "Hr Hl".
        iExists #(y - x); iSplit; first by eauto with lia.
        iExists #y. iFrame. iIntros "Hr". iModIntro.
        iExists x, (y-x). iFrame. iPureIntro.
        do 2 (split; first by lia). rewrite -H5; apply Z.gcd_sub_diag_r.
      + iExists #false.  simplify_eq /=. iSplit.
        { rewrite/ bin_op_eval //=.
          case_bool_decide. inversion H6; subst. lia. eauto. }
        iExists #true;  iSplit; first done. iRight; iSplit; first done.
        iApply a_if_spec.
        iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
        iExists #false. iSplit.
        { rewrite/ bin_op_eval //=.
          case_bool_decide. inversion H6; subst. lia. eauto. }
        iRight; iSplit; first done. awp_seq.
        iApply a_store_ret.
        iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
        iExists #(x - y); iSplit; first by eauto with lia.
        iExists #x. iFrame. iIntros "Hl". iModIntro.
        iExists (x-y), y. iFrame. iPureIntro.
        do 2 (split; first by lia).
        rewrite -H5 Z.gcd_comm (Z.gcd_comm x); apply Z.gcd_sub_diag_r.
  Qed.
End gcd_spec.