gcd.v 3.63 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 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 43 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 80 81 82 83 84 85 86 87 88
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.


Section gcd.


  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").
End gcd.


Section gcd_spec.

  Require Import Coq.ZArith.Znumtheory.

  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.
        do 2 iModIntro. awp_seq. awp_load_ret l #y. iIntros.
        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.