Commit 845d6b1d authored by Robbert Krebbers's avatar Robbert Krebbers

Add proof of strange version of gcd from my thesis.

parent c9017ed0
......@@ -11,6 +11,20 @@ Definition gcd : val := λᶜ "x",
}
}; ∗ᶜ(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 Σ}.
......@@ -35,4 +49,19 @@ Section gcd_spec.
* 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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment