From iris_c.vcgen Require Import vcg_solver. Local Open Scope Z_scope. (* TODO: Notation, get rid of parenthesis around the while loop *) Definition gcd : val := λ: "a" "b", (whileᶜ (∗ᶜ(a_ret "a") !=ᶜ ∗ᶜ(a_ret "b")) { ifᶜ (∗ᶜ(a_ret "a") <ᶜ ∗ᶜ(a_ret "b")) { (a_ret "b") =ᶜ ∗ᶜ(a_ret "b") -ᶜ ∗ᶜ(a_ret "a") } elseᶜ { (a_ret "a") =ᶜ ∗ᶜ(a_ret "a") -ᶜ ∗ᶜ(a_ret "b") } }) ;ᶜ ∗ᶜ(a_ret "a"). Section gcd_spec. Context `{amonadG Σ}. (* TODO: use callᶜ *) Lemma gcd_spec (a b : Z) (l r: cloc) R : 0 ≤ a → 0 ≤ b → l ↦C #a -∗ r ↦C #b -∗ awp (gcd (cloc_to_val l) (cloc_to_val r)) R (λ v, ⌜v = #(Z.gcd a b)⌝). Proof. iIntros (??) "Hl Hr". unfold gcd. do 2 awp_lam. (* vcg_solver. *) (* iIntros "Hr Hl". *) iApply a_sequence_spec'. iApply (a_while_inv_spec (∃ x y : Z, ⌜0 ≤ x ∧ 0 ≤ y ∧ Z.gcd x y = Z.gcd a b⌝ ∧ l ↦C #x ∗ r ↦C #y)%I with "[Hl Hr]"). - iExists a, b. eauto with iFrame. - iModIntro. iDestruct 1 as (x y (?&?&Hgcd)) "[Hl Hr]". vcg_solver. iIntros "Hr Hl /=". case_bool_decide; simpl; [ iLeft | iRight ]; iSplit; eauto. + repeat iModIntro. vcg_solver. rewrite Qp_half_half. simplify_eq/=. rewrite -Hgcd Z.gcd_diag Z.abs_eq; eauto with iFrame. + iNext. iApply a_if_spec'. vcg_solver. rewrite !Qp_half_half. iIntros "Hl Hr /=". case_bool_decide; simpl; [ iLeft | iRight ]; (iSplit; first done); vcg_solver; eauto 400 with iFrame. Qed. End gcd_spec.