gcd.v 3.58 KB
 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 committed May 07, 2018 6 ``````Require Import Coq.ZArith.Znumtheory. `````` 7 `````` `````` Dan Frumin committed May 07, 2018 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. `````` Dan Frumin committed May 07, 2018 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.``````