gcd.v 3.23 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
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")))))))
Robbert Krebbers's avatar
Robbert Krebbers committed
17
     ; a_load (a_ret "a").
18 19

Section gcd_spec.
20
  Context `{amonadG Σ}.
21

Robbert Krebbers's avatar
Robbert Krebbers committed
22 23
  Lemma gcd_spec (a b : Z) (l r: loc) R :
    0  a  0  b 
24
    l C #a - r C #b -
25 26
    awp (gcd #l #r) R (λ v, v = #(Z.gcd a b)).
  Proof.
27
    iIntros (??) "Hl Hr". do 2 awp_lam. iApply a_sequence_spec'. iNext.
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
      iApply a_un_op_spec.
      iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
Robbert Krebbers's avatar
Robbert Krebbers committed
34
      assert (x = y  x < y  y < x) as [Hxy|[Hxy|Hxy]] by lia.
35 36 37
      + iExists #true. simplify_eq /=. iSplit.
        { rewrite/ bin_op_eval //=; case_bool_decide; eauto. }
        iExists #false; iSplit; first done. iLeft; iSplit; first done.
38
        do 2 iModIntro. awp_load_ret l. iIntros.
Robbert Krebbers's avatar
Robbert Krebbers committed
39 40 41 42
        by rewrite -Hgcd Z.gcd_diag Z.abs_eq.
      + iExists #false. simplify_eq /=. iSplit.
        { by rewrite /bin_op_eval //= bool_decide_false; last (intros [= ?]; lia). }
        iExists #true; iSplit; first done. iRight; iSplit; first done.
43
        iNext. iApply a_if_spec'.
44 45
        iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
        iExists #true; iSplit.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
        { by rewrite /bin_op_eval //= bool_decide_true. }
47
        iLeft. iSplit; first done.
48 49 50
        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.
Robbert Krebbers's avatar
Robbert Krebbers committed
51 52 53 54 55
        iExists #y. iIntros "{$Hr} Hr !>".
        iExists x, (y-x). iFrame. rewrite -Hgcd Z.gcd_sub_diag_r. eauto with lia.
      + iExists #false. simplify_eq /=. iSplit.
        { by rewrite/ bin_op_eval //= bool_decide_false; last (intros [= ?]; lia). }
        iExists #true; iSplit; first done. iRight; iSplit; first done.
56
        iNext. iApply a_if_spec'.
57 58
        iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
        iExists #false. iSplit.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
        { by rewrite/ bin_op_eval //= bool_decide_false; last lia. }
60
        iRight; iSplit; first done.
61 62 63
        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.
Robbert Krebbers's avatar
Robbert Krebbers committed
64 65
        iExists #x. iIntros "{$Hl} Hl !>". iExists (x - y), y. iFrame. iPureIntro.
        rewrite -Hgcd Z.gcd_comm Z.gcd_sub_diag_r Z.gcd_comm. auto with lia.
66 67
  Qed.
End gcd_spec.