Commit 81ce92fd authored by Robbert Krebbers's avatar Robbert Krebbers

Update examples to use total weakest preconditions.

parent 8076fe39
...@@ -9,6 +9,13 @@ Definition assert : val := ...@@ -9,6 +9,13 @@ Definition assert : val :=
(* just below ;; *) (* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope. Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Lemma twp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} :
WP e @ E [{ v, v = #true Φ #() }] - WP assert: e @ E [{ Φ }].
Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} : Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} :
WP e @ E {{ v, v = #true Φ #() }} - WP assert: e @ E {{ Φ }}. WP e @ E {{ v, v = #true Φ #() }} - WP assert: e @ E {{ Φ }}.
Proof. Proof.
......
(** This file is essentially a bunch of testcases. *) (** This file is essentially a bunch of testcases. *)
From iris.program_logic Require Export weakestpre hoare. From iris.program_logic Require Export weakestpre total_weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import adequacy. From iris.heap_lang Require Import adequacy.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
...@@ -34,7 +34,7 @@ Section LiftingTests. ...@@ -34,7 +34,7 @@ Section LiftingTests.
let: "y" := ref #1 in let: "y" := ref #1 in
"x" <- !"x" + #1 ;; !"x". "x" <- !"x" + #1 ;; !"x".
Lemma heap_e2_spec E : WP heap_e2 @ E {{ v, v = #2 }}%I. Lemma heap_e2_spec E : WP heap_e2 @ E [{ v, v = #2 }]%I.
Proof. Proof.
iIntros "". rewrite /heap_e2. iIntros "". rewrite /heap_e2.
wp_alloc l. wp_let. wp_alloc l'. wp_let. wp_alloc l. wp_let. wp_alloc l'. wp_let.
...@@ -46,7 +46,7 @@ Section LiftingTests. ...@@ -46,7 +46,7 @@ Section LiftingTests.
let: "f" := λ: "z", "z" + #1 in let: "f" := λ: "z", "z" + #1 in
if: "x" then "f" #0 else "f" #1. if: "x" then "f" #0 else "f" #1.
Lemma heap_e3_spec E : WP heap_e3 @ E {{ v, v = #1 }}%I. Lemma heap_e3_spec E : WP heap_e3 @ E [{ v, v = #1 }]%I.
Proof. Proof.
iIntros "". rewrite /heap_e3. iIntros "". rewrite /heap_e3.
by repeat (wp_pure _). by repeat (wp_pure _).
...@@ -56,7 +56,7 @@ Section LiftingTests. ...@@ -56,7 +56,7 @@ Section LiftingTests.
let: "x" := (let: "y" := ref (ref #1) in ref "y") in let: "x" := (let: "y" := ref (ref #1) in ref "y") in
! ! !"x". ! ! !"x".
Lemma heap_e4_spec : WP heap_e4 {{ v, v = #1 }}%I. Lemma heap_e4_spec : WP heap_e4 [{ v, v = #1 }]%I.
Proof. Proof.
rewrite /heap_e4. wp_alloc l. wp_alloc l'. wp_let. rewrite /heap_e4. wp_alloc l. wp_alloc l'. wp_let.
wp_alloc l''. wp_let. by repeat wp_load. wp_alloc l''. wp_let. by repeat wp_load.
...@@ -65,7 +65,7 @@ Section LiftingTests. ...@@ -65,7 +65,7 @@ Section LiftingTests.
Definition heap_e5 : expr := Definition heap_e5 : expr :=
let: "x" := ref (ref #1) in FAA (!"x") (#10 + #1) + ! !"x". let: "x" := ref (ref #1) in FAA (!"x") (#10 + #1) + ! !"x".
Lemma heap_e5_spec E : WP heap_e5 @ E {{ v, v = #13 }}%I. Lemma heap_e5_spec E : WP heap_e5 @ E [{ v, v = #13 }]%I.
Proof. Proof.
rewrite /heap_e5. wp_alloc l. wp_alloc l'. wp_let. rewrite /heap_e5. wp_alloc l. wp_alloc l'. wp_let.
wp_load. wp_op. wp_faa. do 2 wp_load. wp_op. done. wp_load. wp_op. wp_faa. do 2 wp_load. wp_op. done.
...@@ -81,16 +81,17 @@ Section LiftingTests. ...@@ -81,16 +81,17 @@ Section LiftingTests.
Lemma FindPred_spec n1 n2 E Φ : Lemma FindPred_spec n1 n2 E Φ :
n1 < n2 n1 < n2
Φ #(n2 - 1) - WP FindPred #n2 #n1 @ E {{ Φ }}. Φ #(n2 - 1) - WP FindPred #n2 #n1 @ E [{ Φ }].
Proof. Proof.
iIntros (Hn) "HΦ". iLöb as "IH" forall (n1 Hn). iIntros (Hn) "HΦ".
iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn).
wp_rec. wp_let. wp_op. wp_let. wp_rec. wp_let. wp_op. wp_let.
wp_op; case_bool_decide; wp_if. wp_op; case_bool_decide; wp_if.
- iApply ("IH" with "[%] HΦ"). omega. - iApply ("IH" with "[%] [%] HΦ"); omega.
- by assert (n1 = n2 - 1) as -> by omega. - by assert (n1' = n2 - 1) as -> by omega.
Qed. Qed.
Lemma Pred_spec n E Φ : Φ #(n - 1) - WP Pred #n @ E {{ Φ }}. Lemma Pred_spec n E Φ : Φ #(n - 1) - WP Pred #n @ E [{ Φ }].
Proof. Proof.
iIntros "HΦ". wp_lam. iIntros "HΦ". wp_lam.
wp_op. case_bool_decide; wp_if. wp_op. case_bool_decide; wp_if.
...@@ -101,7 +102,7 @@ Section LiftingTests. ...@@ -101,7 +102,7 @@ Section LiftingTests.
Qed. Qed.
Lemma Pred_user E : Lemma Pred_user E :
(WP let: "x" := Pred #42 in Pred "x" @ E {{ v, v = #40 }})%I. WP let: "x" := Pred #42 in Pred "x" @ E [{ v, v = #40 }]%I.
Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed. Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
End LiftingTests. End LiftingTests.
......
(** Correctness of in-place list reversal *) (** Correctness of in-place list reversal *)
From iris.program_logic Require Export weakestpre hoare. From iris.program_logic Require Export total_weakestpre weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.proofmode Require Export tactics. From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
...@@ -27,26 +27,26 @@ Definition rev : val := ...@@ -27,26 +27,26 @@ Definition rev : val :=
end. end.
Lemma rev_acc_wp hd acc xs ys : Lemma rev_acc_wp hd acc xs ys :
{{{ is_list hd xs is_list acc ys }}} [[{ is_list hd xs is_list acc ys }]]
rev hd acc rev hd acc
{{{ w, RET w; is_list w (reverse xs ++ ys) }}}. [[{ w, RET w; is_list w (reverse xs ++ ys) }]].
Proof. Proof.
iIntros (Φ) "[Hxs Hys] HΦ". iIntros (Φ) "[Hxs Hys] HΦ".
iLöb as "IH" forall (hd acc xs ys Φ). wp_rec. wp_let. iInduction xs as [|x xs] "IH" forall (hd acc ys Φ);
destruct xs as [|x xs]; iSimplifyEq. iSimplifyEq; wp_rec; wp_let.
- wp_match. by iApply "HΦ". - wp_match. by iApply "HΦ".
- iDestruct "Hxs" as (l hd' ->) "[Hx Hxs]". - iDestruct "Hxs" as (l hd' ->) "[Hx Hxs]".
wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store. wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
iApply ("IH" $! hd' (SOMEV #l) xs (x :: ys) with "Hxs [Hx Hys]"); simpl. iApply ("IH" $! hd' (SOMEV #l) (x :: ys) with "Hxs [Hx Hys]"); simpl.
{ iExists l, acc; by iFrame. } { iExists l, acc; by iFrame. }
iNext. iIntros (w). rewrite cons_middle assoc -reverse_cons. iApply "HΦ". iIntros (w). rewrite cons_middle assoc -reverse_cons. iApply "HΦ".
Qed. Qed.
Lemma rev_wp hd xs : Lemma rev_wp hd xs :
{{{ is_list hd xs }}} rev hd (InjL #()) {{{ w, RET w; is_list w (reverse xs) }}}. [[{ is_list hd xs }]] rev hd NONE [[{ w, RET w; is_list w (reverse xs) }]].
Proof. Proof.
iIntros (Φ) "Hxs HΦ". iIntros (Φ) "Hxs HΦ".
iApply (rev_acc_wp hd NONEV xs [] with "[$Hxs //]"). iApply (rev_acc_wp hd NONEV xs [] with "[$Hxs //]").
iNext; iIntros (w). rewrite right_id_L. iApply "HΦ". iIntros (w). rewrite right_id_L. iApply "HΦ".
Qed. Qed.
End list_reverse. End list_reverse.
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre total_weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.proofmode Require Export tactics. From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
...@@ -35,9 +35,9 @@ Definition sum' : val := λ: "t", ...@@ -35,9 +35,9 @@ Definition sum' : val := λ: "t",
!"l". !"l".
Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) : Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) :
{{{ l #n is_tree v t }}} [[{ l #n is_tree v t }]]
sum_loop v #l sum_loop v #l
{{{ RET #(); l #(sum t + n) is_tree v t }}}. [[{ RET #(); l #(sum t + n) is_tree v t }]].
Proof. Proof.
iIntros (Φ) "[Hl Ht] HΦ". iIntros (Φ) "[Hl Ht] HΦ".
iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); simpl; wp_rec; wp_let. iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); simpl; wp_rec; wp_let.
...@@ -55,7 +55,7 @@ Proof. ...@@ -55,7 +55,7 @@ Proof.
Qed. Qed.
Lemma sum_wp `{!heapG Σ} v t : Lemma sum_wp `{!heapG Σ} v t :
{{{ is_tree v t }}} sum' v {{{ RET #(sum t); is_tree v t }}}. [[{ is_tree v t }]] sum' v [[{ RET #(sum t); is_tree v t }]].
Proof. Proof.
iIntros (Φ) "Ht HΦ". rewrite /sum' /=. iIntros (Φ) "Ht HΦ". rewrite /sum' /=.
wp_let. wp_alloc l as "Hl". wp_let. wp_let. wp_alloc l as "Hl". wp_let.
......
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