Commit bfa32cfe authored by Robbert Krebbers's avatar Robbert Krebbers

Rename stuff to be consistent with the paper.

parent 81137d7c
This diff is collapsed.
...@@ -2,41 +2,41 @@ From iris.heap_lang Require Export proofmode notation. ...@@ -2,41 +2,41 @@ From iris.heap_lang Require Export proofmode notation.
From iris_c.c_translation Require Export monad. From iris_c.c_translation Require Export monad.
From iris.proofmode Require Import coq_tactics. From iris.proofmode Require Import coq_tactics.
Lemma tac_awp_bind `{amonadG Σ} K Δ R Φ e f : Lemma tac_cwp_bind `{cmonadG Σ} K Δ R Φ e f :
f = (λ e, fill K e) (* as an eta expanded hypothesis so that we can `simpl` it *) f = (λ e, fill K e) (* as an eta expanded hypothesis so that we can `simpl` it *)
envs_entails Δ (WP e {{ v, awp (f (of_val v)) R Φ }})%I envs_entails Δ (WP e {{ v, cwp (f (of_val v)) R Φ }})%I
envs_entails Δ (awp (fill K e) R Φ). envs_entails Δ (cwp (fill K e) R Φ).
Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_awp_bind. Qed. Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_cwp_bind. Qed.
Ltac awp_bind_core K := Ltac cwp_bind_core K :=
lazymatch eval hnf in K with lazymatch eval hnf in K with
| [] => idtac | [] => idtac
| _ => eapply (tac_awp_bind K); [simpl; reflexivity|lazy beta] | _ => eapply (tac_cwp_bind K); [simpl; reflexivity|lazy beta]
end. end.
Tactic Notation "awp_apply" open_constr(lem) := Tactic Notation "cwp_apply" open_constr(lem) :=
iPoseProofCore lem as false true (fun H => iPoseProofCore lem as false true (fun H =>
lazymatch goal with lazymatch goal with
| |- envs_entails _ (awp ?e ?R ?Q) => | |- envs_entails _ (cwp ?e ?R ?Q) =>
reshape_expr e ltac:(fun K e' => reshape_expr e ltac:(fun K e' =>
awp_bind_core K; iApplyHyp H; try iNext (*; try wp_expr_simpl*) ) || cwp_bind_core K; iApplyHyp H; try iNext (*; try wp_expr_simpl*) ) ||
lazymatch iTypeOf H with lazymatch iTypeOf H with
| Some (_,?P) => fail "awp_apply: cannot apply" P | Some (_,?P) => fail "cwp_apply: cannot apply" P
end end
| _ => fail "awp_apply: not a 'awp'" | _ => fail "cwp_apply: not a 'cwp'"
end). end).
Lemma tac_awp_pure `{amonadG Σ} Δ Δ' K e1 e2 e φ n R Φ : Lemma tac_cwp_pure `{cmonadG Σ} Δ Δ' K e1 e2 e φ n R Φ :
e = fill K e1 e = fill K e1
PureExec φ n e1 e2 PureExec φ n e1 e2
φ φ
MaybeIntoLaterNEnvs n Δ Δ' MaybeIntoLaterNEnvs n Δ Δ'
envs_entails Δ' (awp (fill K e2) R Φ) envs_entails Δ' (cwp (fill K e2) R Φ)
envs_entails Δ (awp e R Φ). envs_entails Δ (cwp e R Φ).
Proof. Proof.
rewrite envs_entails_eq=> -> ??? HΔ'. rewrite envs_entails_eq=> -> ??? HΔ'.
rewrite into_laterN_env_sound /=. rewrite into_laterN_env_sound /=.
rewrite HΔ' -awp_pure //. rewrite HΔ' -cwp_pure //.
Qed. Qed.
Tactic Notation "tac_bind_helper" := Tactic Notation "tac_bind_helper" :=
...@@ -52,48 +52,48 @@ Tactic Notation "tac_bind_helper" := ...@@ -52,48 +52,48 @@ Tactic Notation "tac_bind_helper" :=
replace e with (fill K' e') by (by rewrite ?fill_app)) replace e with (fill K' e') by (by rewrite ?fill_app))
end; reflexivity. end; reflexivity.
Tactic Notation "awp_pure" open_constr(efoc) := Tactic Notation "cwp_pure" open_constr(efoc) :=
iStartProof; iStartProof;
lazymatch goal with lazymatch goal with
| |- envs_entails _ (awp ?e ?R ?Q) => | |- envs_entails _ (cwp ?e ?R ?Q) =>
let e := eval simpl in e in let e := eval simpl in e in
reshape_expr e ltac:(fun K e' => reshape_expr e ltac:(fun K e' =>
unify e' efoc; unify e' efoc;
eapply (tac_awp_pure _ _ _ _ _ (fill K e')); eapply (tac_cwp_pure _ _ _ _ _ (fill K e'));
[tac_bind_helper (* e = fill K e' *) [tac_bind_helper (* e = fill K e' *)
|apply _ (* PureExec *) |apply _ (* PureExec *)
|try fast_done (* The pure condition for PureExec *) |try fast_done (* The pure condition for PureExec *)
|apply _ (* IntoLaters *) |apply _ (* IntoLaters *)
|simpl |simpl
]) ])
|| fail "awp_pure: cannot find" efoc "in" e "or" efoc "is not a redex" || fail "cwp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
| _ => fail "awp_pure: not an 'awp'" | _ => fail "cwp_pure: not an 'cwp'"
end. end.
(* See Iris for documentation on this tactic *) (* See Iris for documentation on this tactic *)
Ltac awp_pures := Ltac cwp_pures :=
iStartProof; iStartProof;
repeat (awp_pure _; []). (* The `;[]` makes sure that no side-condition repeat (cwp_pure _; []). (* The `;[]` makes sure that no side-condition
magically spawns. *) magically spawns. *)
Tactic Notation "awp_rec" := Tactic Notation "cwp_rec" :=
let H := fresh in let H := fresh in
assert (H := AsRecV_recv_locked); assert (H := AsRecV_recv_locked);
awp_pure (App _ _); cwp_pure (App _ _);
clear H. clear H.
Tactic Notation "awp_if" := awp_pure (If _ _ _). Tactic Notation "cwp_if" := cwp_pure (If _ _ _).
Tactic Notation "awp_if_true" := awp_pure (If (LitV (LitBool true)) _ _). Tactic Notation "cwp_if_true" := cwp_pure (If (LitV (LitBool true)) _ _).
Tactic Notation "awp_if_false" := awp_pure (If (LitV (LitBool false)) _ _). Tactic Notation "cwp_if_false" := cwp_pure (If (LitV (LitBool false)) _ _).
Tactic Notation "awp_unop" := awp_pure (UnOp _ _). Tactic Notation "cwp_unop" := cwp_pure (UnOp _ _).
Tactic Notation "awp_binop" := awp_pure (BinOp _ _ _). Tactic Notation "cwp_binop" := cwp_pure (BinOp _ _ _).
Tactic Notation "awp_op" := awp_unop || awp_binop. Tactic Notation "cwp_op" := cwp_unop || cwp_binop.
Tactic Notation "awp_lam" := awp_rec. Tactic Notation "cwp_lam" := cwp_rec.
Tactic Notation "awp_let" := awp_lam. Tactic Notation "cwp_let" := cwp_lam.
Tactic Notation "awp_seq" := awp_lam. Tactic Notation "cwp_seq" := cwp_lam.
Tactic Notation "awp_proj" := awp_pure (Fst _) || awp_pure (Snd _). Tactic Notation "cwp_proj" := cwp_pure (Fst _) || cwp_pure (Snd _).
Tactic Notation "awp_case" := awp_pure (Case _ _ _). Tactic Notation "cwp_case" := cwp_pure (Case _ _ _).
Tactic Notation "awp_match" := awp_case; awp_let. Tactic Notation "cwp_match" := cwp_case; cwp_let.
Tactic Notation "awp_inj" := awp_pure (InjL _) || wp_pure (InjR _). Tactic Notation "cwp_inj" := cwp_pure (InjL _) || wp_pure (InjR _).
Tactic Notation "awp_pair" := awp_pure (Pair _ _). Tactic Notation "cwp_pair" := cwp_pure (Pair _ _).
Tactic Notation "awp_closure" := awp_pure (Rec _ _ _). Tactic Notation "cwp_closure" := cwp_pure (Rec _ _ _).
This diff is collapsed.
...@@ -2,44 +2,44 @@ ...@@ -2,44 +2,44 @@
From iris_c.vcgen Require Import proofmode. From iris_c.vcgen Require Import proofmode.
Section test. Section test.
Context `{amonadG Σ}. Context `{cmonadG Σ}.
(** dereferencing *) (** dereferencing *)
Lemma test1 cl v : Lemma test1 cl v :
cl C v - AWP ∗ᶜ ♯ₗcl {{ w, w = v cl C v }}. cl C v - CWP ∗ᶜ ♯ₗcl {{ w, w = v cl C v }}.
Proof. iIntros. vcg. auto. Qed. Proof. iIntros. vcg. auto. Qed.
(** double dereferencing *) (** double dereferencing *)
Lemma test2 cl1 cl2 v : Lemma test2 cl1 cl2 v :
cl1 C cloc_to_val cl2 - cl2 C v - cl1 C cloc_to_val cl2 - cl2 C v -
AWP ∗ᶜ ∗ᶜ ♯ₗcl1 {{ v, v = #1 cl1 C cloc_to_val cl2 - cl2 C v }}. CWP ∗ᶜ ∗ᶜ ♯ₗcl1 {{ v, v = #1 cl1 C cloc_to_val cl2 - cl2 C v }}.
Proof. iIntros. vcg. auto. Qed. Proof. iIntros. vcg. auto. Qed.
(** sequence points *) (** sequence points *)
Lemma test3 cl v : Lemma test3 cl v :
cl C v - AWP ∗ᶜ ♯ₗcl ; ∗ᶜ ♯ₗcl {{ w, w = v cl C v }}. cl C v - CWP ∗ᶜ ♯ₗcl ; ∗ᶜ ♯ₗcl {{ w, w = v cl C v }}.
Proof. iIntros. vcg. auto. Qed. Proof. iIntros. vcg. auto. Qed.
(** assignments *) (** assignments *)
Lemma test4 (l : cloc) (v1 v2: val) : Lemma test4 (l : cloc) (v1 v2: val) :
l C v1 - AWP ♯ₗl = a_ret v2 {{ v, v = v2 l C[LLvl] v2 }}. l C v1 - CWP ♯ₗl = c_ret v2 {{ v, v = v2 l C[LLvl] v2 }}.
Proof. iIntros. vcg. auto. Qed. Proof. iIntros. vcg. auto. Qed.
Lemma store_load s l R : Lemma store_load s l R :
s C #0 - l C #1 - s C #0 - l C #1 -
AWP ♯ₗs = ∗ᶜ ♯ₗl @ R {{ _, s C[LLvl] #1 l C #1 }}. CWP ♯ₗs = ∗ᶜ ♯ₗl @ R {{ _, s C[LLvl] #1 l C #1 }}.
Proof. iIntros. vcg. auto with iFrame. Qed. Proof. iIntros. vcg. auto with iFrame. Qed.
Lemma store_load_load s1 s2 l R : Lemma store_load_load s1 s2 l R :
s1 C #0 - l C #1 - s2 C #0 - s1 C #0 - l C #1 - s2 C #0 -
AWP ♯ₗs1 = ∗ᶜ ♯ₗl ; ∗ᶜ ♯ₗs1 + 42 @ R {{ _, s1 C #1 l C #1 }}. CWP ♯ₗs1 = ∗ᶜ ♯ₗl ; ∗ᶜ ♯ₗs1 + 42 @ R {{ _, s1 C #1 l C #1 }}.
Proof. iIntros. vcg. auto with iFrame. Qed. Proof. iIntros. vcg. auto with iFrame. Qed.
(** double dereferencing & modification *) (** double dereferencing & modification *)
Lemma test5 (l1 l2 r1 r2 : cloc) (v1 v2: val) : Lemma test5 (l1 l2 r1 r2 : cloc) (v1 v2: val) :
l1 C cloc_to_val l2 - l2 C v1 - l1 C cloc_to_val l2 - l2 C v1 -
r1 C cloc_to_val r2 - r2 C v2 - r1 C cloc_to_val r2 - r2 C v2 -
AWP ♯ₗl1 = ♯ₗr1 ; ∗ᶜ ∗ᶜ ♯ₗl1 CWP ♯ₗl1 = ♯ₗr1 ; ∗ᶜ ∗ᶜ ♯ₗl1
{{ w, w = v2 {{ w, w = v2
l1 C cloc_to_val r2 l2 C v1 r1 C cloc_to_val r2 - r2 C v2 }}. l1 C cloc_to_val r2 l2 C v1 r1 C cloc_to_val r2 - r2 C v2 }}.
Proof. iIntros. vcg. auto with iFrame. Qed. Proof. iIntros. vcg. auto with iFrame. Qed.
...@@ -47,86 +47,86 @@ Section test. ...@@ -47,86 +47,86 @@ Section test.
(** par *) (** par *)
Lemma test_par_1 (l1 l2 : cloc) (v1 v2: val) : Lemma test_par_1 (l1 l2 : cloc) (v1 v2: val) :
l1 C v1 - l2 C v2 - l1 C v1 - l2 C v2 -
AWP ∗ᶜ ♯ₗl1 ||| ∗ᶜ ♯ₗl2 CWP ∗ᶜ ♯ₗl1 ||| ∗ᶜ ♯ₗl2
{{ w, w = (v1, v2)%V l1 C v1 l2 C v2 }}. {{ w, w = (v1, v2)%V l1 C v1 l2 C v2 }}.
Proof. iIntros. vcg. auto with iFrame. Qed. Proof. iIntros. vcg. auto with iFrame. Qed.
Lemma test_par_2 (l1 l2 : cloc) (v1 v2: val) : Lemma test_par_2 (l1 l2 : cloc) (v1 v2: val) :
l1 C v1 - l2 C v2 - l1 C v1 - l2 C v2 -
AWP (♯ₗl1 = a_ret v2) ||| (♯ₗl2 = a_ret v1) CWP (♯ₗl1 = c_ret v2) ||| (♯ₗl2 = c_ret v1)
{{ w, w = (v2, v1)%V l1 C[LLvl] v2 l2 C[LLvl] v1 }}. {{ w, w = (v2, v1)%V l1 C[LLvl] v2 l2 C[LLvl] v1 }}.
Proof. iIntros. vcg. auto with iFrame. Qed. Proof. iIntros. vcg. auto with iFrame. Qed.
(** pre bin op *) (** pre bin op *)
Lemma test6 (l : cloc) (z0 : Z) R: Lemma test6 (l : cloc) (z0 : Z) R:
l C #z0 - l C #z0 -
AWP ♯ₗl += 1 @ R {{ v, v = #z0 l C[LLvl] #(1 + z0) }}. CWP ♯ₗl += 1 @ R {{ v, v = #z0 l C[LLvl] #(1 + z0) }}.
Proof. iIntros. vcg. eauto with iFrame. Qed. Proof. iIntros. vcg. eauto with iFrame. Qed.
Lemma test7 (l k : cloc) (z0 z1 : Z) R: Lemma test7 (l k : cloc) (z0 z1 : Z) R:
l C #z0 - l C #z0 -
k C #z1 - k C #z1 -
AWP (♯ₗl += 1) + (∗ᶜ♯ₗk) @ R CWP (♯ₗl += 1) + (∗ᶜ♯ₗk) @ R
{{ v, v = #(z0+z1) l C[LLvl] #(1 + z0) k C #z1 }}. {{ v, v = #(z0+z1) l C[LLvl] #(1 + z0) k C #z1 }}.
Proof. iIntros. vcg. eauto with iFrame. Qed. Proof. iIntros. vcg. eauto with iFrame. Qed.
(** more sequences *) (** more sequences *)
Lemma test_seq s l : Lemma test_seq s l :
s C[ULvl] #0 - l C[ULvl] #1 - s C[ULvl] #0 - l C[ULvl] #1 -
AWP (♯ₗl = 2 ; 1 + (♯ₗ l = 1)) + (♯ₗ s = 4) CWP (♯ₗl = 2 ; 1 + (♯ₗ l = 1)) + (♯ₗ s = 4)
{{ v, v = #6 s C[LLvl] #4 l C[LLvl] #1 }}. {{ v, v = #6 s C[LLvl] #4 l C[LLvl] #1 }}.
Proof. iIntros. vcg. eauto with iFrame. Qed. Proof. iIntros. vcg. eauto with iFrame. Qed.
Lemma test_seq2 s l : Lemma test_seq2 s l :
s C[ULvl] #0 - l C[ULvl] #1 - s C[ULvl] #0 - l C[ULvl] #1 -
AWP (♯ₗl = 2 ; ∗ᶜ ♯ₗl) + (♯ₗs = 4) {{ v, v = #6 s C[LLvl] #4 l C #2 }}. CWP (♯ₗl = 2 ; ∗ᶜ ♯ₗl) + (♯ₗs = 4) {{ v, v = #6 s C[LLvl] #4 l C #2 }}.
Proof. iIntros. vcg. eauto with iFrame. Qed. Proof. iIntros. vcg. eauto with iFrame. Qed.
Lemma test_seq3 l : Lemma test_seq3 l :
l C #0 - l C #0 -
AWP ♯ₗl = 2 ; 1 + (♯ₗl = 1) {{ _, l C[LLvl] #1 }}. CWP ♯ₗl = 2 ; 1 + (♯ₗl = 1) {{ _, l C[LLvl] #1 }}.
Proof. iIntros. vcg. eauto with iFrame. Qed. Proof. iIntros. vcg. eauto with iFrame. Qed.
Lemma test_seq4 l k : Lemma test_seq4 l k :
l C #0 - l C #0 -
k C #0 - k C #0 -
AWP (♯ₗl = 2 ; 1 + (♯ₗl = 1)) + (♯ₗk = 2 ; 1 + (♯ₗk = 1)) CWP (♯ₗl = 2 ; 1 + (♯ₗl = 1)) + (♯ₗk = 2 ; 1 + (♯ₗk = 1))
{{ v, v = #4 l C[LLvl] #1 k C[LLvl] #1 }}. {{ v, v = #4 l C[LLvl] #1 k C[LLvl] #1 }}.
Proof. iIntros. vcg. eauto with iFrame. Qed. Proof. iIntros. vcg. eauto with iFrame. Qed.
Definition stupid (l : cloc) : expr := Definition stupid (l : cloc) : expr :=
♯ₗ l = 1; a_ret #0. ♯ₗ l = 1; c_ret #0.
Lemma test_seq_fail l : Lemma test_seq_fail l :
l C[ULvl] #0 - l C[ULvl] #0 -
AWP (stupid l + stupid l) + (a_ret #0) {{ v, l C #1 }}. CWP (stupid l + stupid l) + (c_ret #0) {{ v, l C #1 }}.
Proof. iIntros. vcg. Fail by eauto with iFrame. Abort. Proof. iIntros. vcg. Fail by eauto with iFrame. Abort.
Lemma test_seq5 l k : Lemma test_seq5 l k :
l C #0 - l C #0 -
k C #0 - k C #0 -
AWP 0 + (♯ₗl = 1 ; ♯ₗk = 2 ; 0) {{ v, v = #0 l C #1 k C #2 }}. CWP 0 + (♯ₗl = 1 ; ♯ₗk = 2 ; 0) {{ v, v = #0 l C #1 k C #2 }}.
Proof. iIntros. vcg. eauto with iFrame. Qed. Proof. iIntros. vcg. eauto with iFrame. Qed.
Lemma test_seq6 l k : Lemma test_seq6 l k :
l C #0 - l C #0 -
k C #0 - k C #0 -
AWP 1 + (♯ₗl = 1 ; (♯ₗk = 2) + ∗ᶜ ♯ₗl ; ∗ᶜ ♯ₗk + (♯ₗl = 2)) CWP 1 + (♯ₗl = 1 ; (♯ₗk = 2) + ∗ᶜ ♯ₗl ; ∗ᶜ ♯ₗk + (♯ₗl = 2))
{{ v, v = #5 l C[LLvl] #2 k C #2 }}. {{ v, v = #5 l C[LLvl] #2 k C #2 }}.
Proof. iIntros. vcg. eauto with iFrame. Qed. Proof. iIntros. vcg. eauto with iFrame. Qed.
Lemma test_seq7 l : Lemma test_seq7 l :
l C #0 - l C #0 -
AWP 1 + (♯ₗl = 1 ; ∗ᶜ ♯ₗl + ∗ᶜ ♯ₗl ; ♯ₗl = 2) {{ v, v = #3 l C[LLvl] #2 }}. CWP 1 + (♯ₗl = 1 ; ∗ᶜ ♯ₗl + ∗ᶜ ♯ₗl ; ♯ₗl = 2) {{ v, v = #3 l C[LLvl] #2 }}.
Proof. iIntros. vcg. eauto with iFrame. Qed. Proof. iIntros. vcg. eauto with iFrame. Qed.
(** while *) (** while *)
Lemma test_while l R : Lemma test_while l R :
l C #1 - l C #1 -
AWP while (∗ᶜ ♯ₗl < 2) { ♯ₗl = 1 } @ R {{ _, True }}. CWP while (∗ᶜ ♯ₗl < 2) { ♯ₗl = 1 } @ R {{ _, True }}.
Proof. Proof.
iIntros. vcg. iIntros. iLöb as "IH". iIntros. vcg. iIntros. iLöb as "IH".
iApply a_whileV_spec; iNext. iApply cwp_whileV; iNext.
vcg. iIntros "Hl". vcg. iIntros "Hl".
iLeft. iSplitR; eauto. iModIntro. iLeft. iSplitR; eauto. iModIntro.
vcg. iIntros "Hl". iModIntro. by iApply "IH". vcg. iIntros "Hl". iModIntro. by iApply "IH".
......
From iris_c.vcgen Require Import proofmode. From iris_c.vcgen Require Import proofmode.
Section test. Section test.
Context `{amonadG Σ}. Context `{cmonadG Σ}.
Lemma ptr_plus_test1 p q n v1 R Φ : Lemma ptr_plus_test1 p q n v1 R Φ :
Φ (cloc_to_val (cloc_plus p n)) - Φ (cloc_to_val (cloc_plus p n)) -
p C v1 - p C v1 -
q C cloc_to_val p - q C cloc_to_val p -
AWP ∗ᶜ♯ₗq +∗ᶜ n @ R {{ v, Φ v p C v1 q C cloc_to_val p }}. CWP ∗ᶜ♯ₗq +∗ᶜ n @ R {{ v, Φ v p C v1 q C cloc_to_val p }}.
Proof. iIntros. vcg. eauto with iFrame. Qed. Proof. iIntros. vcg. eauto with iFrame. Qed.
End test. End test.
From iris_c.vcgen Require Import proofmode. From iris_c.vcgen Require Import proofmode.
Definition inc : val := λᶜ "l", Definition inc : val := λᶜ "l",
a_ret "l" += 1 ; (). c_ret "l" += 1 ; ().
Definition factorial : val := λᶜ "n", Definition factorial : val := λᶜ "n",
"r" mut 1; "r" mut 1;
"c" mut 0; "c" mut 0;
while (∗ᶜ (a_ret "c") < a_ret "n") { while (∗ᶜ (c_ret "c") < c_ret "n") {
call (a_ret inc) (a_ret "c"); call (c_ret inc) (c_ret "c");
a_ret "r" = ∗ᶜ (a_ret "r") * ∗ᶜ (a_ret "c") c_ret "r" = ∗ᶜ (c_ret "r") * ∗ᶜ (c_ret "c")
}; };
∗ᶜ(a_ret "r"). ∗ᶜ(c_ret "r").
Section factorial_spec. Section factorial_spec.
Context `{amonadG Σ}. Context `{cmonadG Σ}.
Lemma inc_spec l (n : Z) R Φ : Lemma inc_spec l (n : Z) R Φ :
l C #n - (l C #(1 + n) - Φ #()) - l C #n - (l C #(1 + n) - Φ #()) -
AWP inc (cloc_to_val l) @ R {{ Φ }}. CWP inc (cloc_to_val l) @ R {{ Φ }}.
Proof. Proof.
iIntros "? H". iApply a_fun_spec; simpl. vcg; iIntros "? !>". by iApply "H". iIntros "? H". iApply cwp_fun; simpl. vcg; iIntros "? !>". by iApply "H".
Qed. Qed.
Lemma factorial_spec (n: nat) R : Lemma factorial_spec (n: nat) R :
AWP factorial #n @ R {{ v, v = #(fact n) }}%I. CWP factorial #n @ R {{ v, v = #(fact n) }}%I.
Proof. Proof.
iApply a_fun_spec; simpl. vcg. iIntros (r c) "**". iApply cwp_fun; simpl. vcg. iIntros (r c) "**".
iApply (awp_wand _ (λ _, c C #n r C #(fact n))%I with "[-]"); last first. iApply (cwp_wand _ (λ _, c C #n r C #(fact n))%I with "[-]"); last first.
{ iIntros (?) "[Hc Hr]". vcg_continue. eauto with iFrame. } { iIntros (?) "[Hc Hr]". vcg_continue. eauto with iFrame. }
iAssert ( k : nat, k n c C #k r C #(fact k))%I with "[-]" as (k Hk) "[??]". iAssert ( k : nat, k n c C #k r C #(fact k))%I with "[-]" as (k Hk) "[??]".
{ iExists 0%nat. eauto with lia iFrame. } { iExists 0%nat. eauto with lia iFrame. }
iLöb as "IH" forall (n k Hk). iApply a_whileV_spec; iNext. iLöb as "IH" forall (n k Hk). iApply cwp_whileV; iNext.
vcg. iIntros "**". case_bool_decide. vcg. iIntros "**". case_bool_decide.
+ iLeft. iSplit; eauto. iModIntro. vcg. + iLeft. iSplit; eauto. iModIntro. vcg.
iIntros "Hc Hr !> $ !>". iApply (inc_spec with "Hc"); iIntros "Hc". iIntros "Hc Hr !> $ !>". iApply (inc_spec with "Hc"); iIntros "Hc".
......
From iris_c.vcgen Require Import proofmode. From iris_c.vcgen Require Import proofmode.
Definition gcd : val := λᶜ "x", Definition gcd : val := λᶜ "x",
"a" ←ᶜ a_ret (Fst "x"); "a" ←ᶜ c_ret (Fst "x");
"b" ←ᶜ a_ret (Snd "x"); "b" ←ᶜ c_ret (Snd "x");
while(∗ᶜ(a_ret "a") != ∗ᶜ(a_ret "b")) { while(∗ᶜ(c_ret "a") != ∗ᶜ(c_ret "b")) {
if (∗ᶜ(a_ret "a") < ∗ᶜ(a_ret "b")) { if (∗ᶜ(c_ret "a") < ∗ᶜ(c_ret "b")) {
(a_ret "b") = ∗ᶜ(a_ret "b") - ∗ᶜ(a_ret "a") (c_ret "b") = ∗ᶜ(c_ret "b") - ∗ᶜ(c_ret "a")
} else { } else {
(a_ret "a") = ∗ᶜ(a_ret "a") - ∗ᶜ(a_ret "b") (c_ret "a") = ∗ᶜ(c_ret "a") - ∗ᶜ(c_ret "b")
} }
}; ∗ᶜ(a_ret "a"). }; ∗ᶜ(c_ret "a").
Section gcd_spec. Section gcd_spec.
Context `{amonadG Σ}. Context `{cmonadG Σ}.
Lemma gcd_spec l r a b R : Lemma gcd_spec l r a b R :
0 a 0 b 0 a 0 b
l C #a - r C #b -