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.
Require Import Coq.ZArith.Znumtheory.

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


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