gcd.v 2.86 KB
 Robbert Krebbers committed Oct 17, 2018 1 ``````From iris_c.vcgen Require Import proofmode. `````` 2 `````` `````` Robbert Krebbers committed Nov 15, 2018 3 ``````Definition gcd : val := λᶜ "x", `````` Robbert Krebbers committed Nov 16, 2018 4 5 6 7 8 `````` "a" ←ᶜ c_ret (Fst "x");ᶜ "b" ←ᶜ c_ret (Snd "x");ᶜ whileᶜ(∗ᶜ(c_ret "a") !=ᶜ ∗ᶜ(c_ret "b")) { ifᶜ (∗ᶜ(c_ret "a") <ᶜ ∗ᶜ(c_ret "b")) { (c_ret "b") =ᶜ ∗ᶜ(c_ret "b") -ᶜ ∗ᶜ(c_ret "a") `````` Robbert Krebbers committed Nov 13, 2018 9 `````` } elseᶜ { `````` Robbert Krebbers committed Nov 16, 2018 10 `````` (c_ret "a") =ᶜ ∗ᶜ(c_ret "a") -ᶜ ∗ᶜ(c_ret "b") `````` Robbert Krebbers committed Nov 13, 2018 11 `````` } `````` Robbert Krebbers committed Nov 16, 2018 12 `````` };ᶜ ∗ᶜ(c_ret "a"). `````` 13 `````` `````` Robbert Krebbers committed Jan 12, 2019 14 15 16 17 18 19 20 21 22 23 24 25 26 27 ``````(* A contrived version of gcd that uses side-effects in expressions from Krebbers's PhD thesis (p170). Note that instead of gotos, we use an ordinary while loop. *) Definition gcd_robbert_thesis : val := λᶜ "x", "a" ←mutᶜ c_ret (Fst "x");ᶜ "b" ←mutᶜ c_ret (Snd "x");ᶜ whileᶜ(♯0 !=ᶜ ∗ᶜ(c_ret "b")) { "tmp" ←mutᶜ ♯0 ;ᶜ c_ret "b" =ᶜ (c_ret "tmp" =ᶜ c_bin_op (CBinOp RemOp) (∗ᶜ(c_ret "a")) (∗ᶜ(c_ret "b"));ᶜ c_ret "a" =ᶜ ∗ᶜ(c_ret "b");ᶜ ∗ᶜ(c_ret "tmp")) };ᶜ ∗ᶜ(c_ret "a"). `````` 28 ``````Section gcd_spec. `````` Robbert Krebbers committed Nov 16, 2018 29 `````` Context `{cmonadG Σ}. `````` 30 `````` `````` Robbert Krebbers committed Nov 13, 2018 31 `````` Lemma gcd_spec l r a b R : `````` Robbert Krebbers committed May 14, 2018 32 `````` 0 ≤ a → 0 ≤ b → `````` Robbert Krebbers committed Jun 19, 2018 33 `````` l ↦C #a -∗ r ↦C #b -∗ `````` Robbert Krebbers committed Nov 16, 2018 34 `````` CWP gcd (cloc_to_val l, cloc_to_val r)%V @ R {{ v, ⌜v = #(Z.gcd a b)⌝ }}. `````` 35 `````` Proof. `````` Robbert Krebbers committed Nov 16, 2018 36 37 `````` iIntros (??) "**". iApply cwp_fun; simpl. vcg; iIntros. iApply (cwp_whileV_inv (∃ x y : Z, `````` Robbert Krebbers committed Nov 13, 2018 38 39 40 41 42 43 `````` ⌜0 ≤ x ∧ 0 ≤ y ∧ Z.gcd x y = Z.gcd a b⌝ ∧ l ↦C #x ∗ r ↦C #y)%I with "[-]"). { iExists a, b. eauto with iFrame. } iModIntro. iDestruct 1 as (x y (?&?&Hgcd)) "[??]". vcg. iIntros "** /=". case_bool_decide; simpl; [iLeft | iRight]; iSplit; eauto. + repeat iModIntro. vcg_continue. simplify_eq/=. rewrite -Hgcd Z.gcd_diag Z.abs_eq; eauto with iFrame. `````` Robbert Krebbers committed Nov 16, 2018 44 `````` + iModIntro. iApply cwp_if. vcg. iIntros "** /=". `````` Dan Frumin committed Oct 09, 2018 45 `````` case_bool_decide; simpl; [ iLeft | iRight ]; `````` Robbert Krebbers committed Nov 13, 2018 46 47 48 49 50 `````` (iSplit; first done); iModIntro. * vcg. iIntros "** !>". iExists x, (y - x); iFrame. iPureIntro. rewrite Z.gcd_sub_diag_r. lia. * vcg. iIntros "** !>". iExists (x-y), y; iFrame. iPureIntro. rewrite Z.gcd_comm Z.gcd_sub_diag_r Z.gcd_comm. lia. `````` 51 `````` Qed. `````` Robbert Krebbers committed Jan 12, 2019 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 `````` Lemma gcd_robbert_thesis_spec (a b : nat) R : CWP gcd_robbert_thesis (#a, #b)%V @ R {{ v, ⌜v = #(Nat.gcd a b)⌝ }}%I. Proof. iApply cwp_fun; simpl. vcg; iIntros (p q) "**". iApply (cwp_wand _ (λ _, p ↦C #(Nat.gcd a b) ∗ q ↦C #0)%I with "[-]"); last first. { iIntros (v) "[??]". vcg_continue; auto. } iInduction (lt_wf b) as [[|b] _] "IH" forall (a). { vcg. iIntros "!> !> **". rewrite Nat.gcd_0_r. iFrame. } vcg. iIntros "!> !>" (t) "!> **". rewrite Z.rem_mod_nonneg; [|lia..]; rewrite -Z2Nat_inj_mod. iApply (cwp_wand with "(IH [%] [\$] [\$])"); [by apply Nat.mod_upper_bound|]. iIntros (v) "[??]". rewrite Nat.gcd_comm Nat.gcd_mod // Nat.gcd_comm. vcg_continue. auto with iFrame. Qed. `````` 67 ``End gcd_spec.``