From iris_c.vcgen Require Import proofmode. Definition gcd : val := λᶜ "x", "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") } elseᶜ { (c_ret "a") =ᶜ ∗ᶜ(c_ret "a") -ᶜ ∗ᶜ(c_ret "b") } };ᶜ ∗ᶜ(c_ret "a"). (* 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"). Section gcd_spec. Context `{cmonadG Σ}. Lemma gcd_spec l r a b R : 0 ≤ a → 0 ≤ b → l ↦C #a -∗ r ↦C #b -∗ CWP gcd (cloc_to_val l, cloc_to_val r)%V @ R {{ v, ⌜v = #(Z.gcd a b)⌝ }}. Proof. iIntros (??) "**". iApply cwp_fun; simpl. vcg; iIntros. iApply (cwp_whileV_inv (∃ x y : Z, ⌜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. + iModIntro. iApply cwp_if. vcg. iIntros "** /=". case_bool_decide; simpl; [ iLeft | iRight ]; (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. Qed. 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. End gcd_spec.