Skip to content

Commit

Permalink
Add some automation to make proofs more concise
Browse files Browse the repository at this point in the history
  • Loading branch information
@tchajed
tchajed committed May 10, 2024
1 parent 15d77c6 commit 16342a3
Show file tree
Hide file tree
Showing 2 changed files with 89 additions and 140 deletions.
47 changes: 47 additions & 0 deletions src/goose_lang/automation/extra_tactics.v
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
From iris.proofmode Require Import coq_tactics reduction.
From Perennial.goose_lang Require Import proofmode.
From Perennial.Helpers Require Import NamedProps.

From Perennial.goose_lang Require Import struct.struct.

Set Default Proof Using "Type".

Ltac wp_start :=
lazymatch goal with
| |- envs_entails _ _ => fail "already in a proofmode goal"
| _ => idtac
end;
iIntros (Φ) "Hpre HΦ";
lazymatch goal with
| |- context[Esnoc _ (INamed "HΦ") (▷ ?Q)%I] =>
set (post:=Q)
end;
lazymatch iTypeOf "Hpre" with
| Some (_, named _ _ ∗ _)%I => iNamed "Hpre"
| Some (_, named _ _)%I => iNamed "Hpre"
| _ => idtac
end;
wp_call.

Ltac wp_auto :=
repeat first [
wp_load
| wp_store
| wp_loadField
| wp_storeField
| wp_pures
].

(* TODO: these tactics are in proofmode.v but don't actually parse; adding them
here and adding (at level 0) fixes this for some reason. *)
Tactic Notation (at level 0) "wp_apply" open_constr(lem) "as" constr(pat) :=
wp_apply lem; last (iIntros pat); wp_auto.
Tactic Notation (at level 0) "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
wp_apply lem; last (iIntros ( x1 ) pat); wp_auto.
Tactic Notation (at level 0) "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) :=
wp_apply lem; last (iIntros ( x1 x2 ) pat); wp_auto.
Tactic Notation (at level 0) "wp_apply" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
wp_apply lem; last (iIntros ( x1 x2 x3 ) pat); wp_auto.
182 changes: 42 additions & 140 deletions src/program_proof/tutorial/kvservice/proof.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,10 @@ From Goose.github_com.mit_pdos.gokv.tutorial Require Import kvservice.
From Perennial.program_proof.grove_shared Require Import urpc_proof monotonic_pred.
From Perennial.program_proof Require Import marshal_stateless_proof.
From Perennial.program_proof Require Import std_proof.
From Perennial.goose_lang.automation Require Import extra_tactics.
From Perennial.goose_lang Require Import proofmode.

Unset Printing Projections.

(********************************************************************************)

Expand Down Expand Up @@ -585,23 +589,11 @@ Lemma wp_Server__getFreshNum (s:loc) Ψ :
{{{ (n:u64), RET #n; Ψ n }}}
.
Proof.
iIntros (Φ) "Hpre HΦ".
iNamed "Hpre".
wp_lam.
wp_pures.
wp_start.
iNamed "Hsrv".
wp_loadField.
wp_apply (acquire_spec with "[$]").
iIntros "[Hlocked Hown]".
iNamed "Hown".
wp_pures.
wp_loadField.
wp_pures.
wp_loadField.
wp_apply (wp_SumAssumeNoOverflow).
iIntros (Hoverflow).
wp_storeField.
wp_loadField.
wp_auto.
wp_apply (acquire_spec with "[$]") as "[Hlocked Hown]"; iNamed "Hown"; wp_auto.
wp_apply (wp_SumAssumeNoOverflow) as (Hoverflow) "".
wp_apply (release_spec with "[-HΦ Hspec]").
{
iFrame "∗#". iNext.
Expand All @@ -625,58 +617,34 @@ Lemma wp_Server__put (s:loc) args_ptr (args:putArgs.t) Ψ :
}}}
.
Proof.
iIntros (Φ) "Hpre HΦ".
iNamed "Hpre".
wp_lam.
wp_pures.
wp_start.
iNamed "Hsrv".
wp_loadField.
wp_apply (acquire_spec with "[$]").
iIntros "[Hlocked Hown]".
iNamed "Hown".
wp_pures.
wp_auto.
wp_apply (acquire_spec with "[$]") as "[Hlocked Hown]"; iNamed "Hown".
iNamed "Hargs".
wp_loadField.
wp_loadField.
wp_apply (wp_MapGet with "HlastRepliesM").
iIntros (??) "[%HlastReply HlastRepliesM]".
wp_pures.
wp_if_destruct.
wp_auto.
wp_apply (wp_MapGet with "HlastRepliesM") as (??) "[%HlastReply HlastRepliesM]".
wp_if_destruct; wp_auto.
{ (* case: this is a duplicate request *)
wp_loadField.
wp_apply (release_spec with "[-HΦ Hspec]").
{
iFrame "∗#". iNext.
repeat iExists _.
iFrame.
}
wp_pures.
iApply "HΦ".
iApply "Hspec".
iApply ("HΦ" with "Hspec").
}
wp_loadField.
wp_loadField.
wp_loadField.
wp_apply (wp_MapInsert with "HkvsM").
{ done. }
iIntros "HkvsM".
wp_pures.
wp_loadField.
wp_loadField.
wp_apply (wp_MapInsert with "HlastRepliesM").
{ done. }
iIntros "HlastRepliesM".
wp_pures.
wp_loadField.
wp_apply (wp_MapInsert with "HkvsM") as "HkvsM"; first done.
wp_apply (wp_MapInsert with "HlastRepliesM") as "HlastRepliesM"; first done.
wp_apply (release_spec with "[-HΦ Hspec]").
{
iFrame "∗#". iNext.
repeat iExists _.
iFrame.
}
wp_pures.
iApply "HΦ".
iApply "Hspec".
iApply ("HΦ" with "Hspec").
Qed.

Lemma wp_Server__conditionalPut (s:loc) args_ptr (args:conditionalPutArgs.t) Ψ :
Expand All @@ -689,25 +657,15 @@ Lemma wp_Server__conditionalPut (s:loc) args_ptr (args:conditionalPutArgs.t) Ψ
{{{ r, RET #(str r); Ψ r }}}
.
Proof.
iIntros (Φ) "Hpre HΦ".
iNamed "Hpre".
wp_lam.
wp_pures.
wp_start.
iNamed "Hsrv".
wp_loadField.
wp_apply (acquire_spec with "[$]").
iIntros "[Hlocked Hown]".
iNamed "Hown".
wp_pures.
wp_auto.
wp_apply (acquire_spec with "[$]") as "[Hlocked Hown]"; iNamed "Hown".
iNamed "Hargs".
wp_loadField.
wp_loadField.
wp_apply (wp_MapGet with "HlastRepliesM").
iIntros (??) "[%HlastReply HlastRepliesM]".
wp_pures.
wp_if_destruct.
wp_auto.
wp_apply (wp_MapGet with "HlastRepliesM") as (??) "[%HlastReply HlastRepliesM]".
wp_if_destruct; wp_auto.
{ (* case: this is a duplicate request *)
wp_loadField.
wp_apply (release_spec with "[-HΦ Hspec]").
{
iFrame "∗#". iNext.
Expand All @@ -718,71 +676,35 @@ Proof.
iApply "HΦ".
iApply "Hspec".
}
wp_apply (wp_ref_to).
{ repeat econstructor. }
iIntros (ret2_ptr) "Hret".
wp_pures.
wp_loadField.
wp_loadField.
wp_apply (wp_MapGet with "HkvsM").
iIntros (??) "[Hlookup HkvsM]".
wp_pures.
wp_loadField.
wp_pures.
wp_if_destruct.
wp_apply (wp_ref_to) as (ret2_ptr) "Hret"; first val_ty.
wp_apply (wp_MapGet with "HkvsM") as (??) "[Hlookup HkvsM]".
wp_if_destruct; wp_auto.
{ (* case: the old value matches the expected value *)
wp_loadField.
wp_loadField.
wp_loadField.
wp_apply (wp_MapInsert with "HkvsM").
{ done. }
iIntros "HkvsM".
wp_apply (wp_MapInsert with "HkvsM") as "HkvsM"; first done.
(* FIXME: delete typed_map.map_insert *)
rewrite /typed_map.map_insert.
wp_pures.
wp_store.
wp_pures.
wp_load.
wp_loadField.
wp_loadField.
wp_apply (wp_MapInsert with "HlastRepliesM").
{ done. }
iIntros "HlastRepliesM".
wp_pures.
wp_loadField.
wp_apply (wp_MapInsert with "HlastRepliesM") as "HlastRepliesM"; first done.
wp_apply (release_spec with "[-HΦ Hspec Hret]").
{
iFrame "∗#". iNext.
repeat iExists _.
iFrame.
}
wp_pures.
wp_load.
wp_auto.
iModIntro.
iApply "HΦ".
iApply "Hspec".
iApply ("HΦ" with "Hspec").
}

wp_pures.
wp_load.
wp_loadField.
wp_loadField.
wp_apply (wp_MapInsert with "HlastRepliesM").
{ done. }
iIntros "HlastRepliesM".
wp_pures.
wp_loadField.
wp_apply (wp_MapInsert with "HlastRepliesM") as "HlastRepliesM"; first done.
wp_apply (release_spec with "[-HΦ Hspec Hret]").
{
iFrame "∗#". iNext.
repeat iExists _.
iFrame.
}
wp_pures.
wp_load.
wp_auto.
iModIntro.
iApply "HΦ".
iApply "Hspec".
iApply ("HΦ" with "Hspec").
Qed.

Lemma wp_Server__get (s:loc) args_ptr (args:getArgs.t) Ψ :
Expand All @@ -797,25 +719,15 @@ Lemma wp_Server__get (s:loc) args_ptr (args:getArgs.t) Ψ :
}}}
.
Proof.
iIntros (Φ) "Hpre HΦ".
iNamed "Hpre".
wp_lam.
wp_pures.
wp_start.
iNamed "Hsrv".
wp_loadField.
wp_apply (acquire_spec with "[$]").
iIntros "[Hlocked Hown]".
iNamed "Hown".
wp_pures.
wp_auto.
wp_apply (acquire_spec with "[$]") as "[Hlocked Hown]"; iNamed "Hown".
iNamed "Hargs".
wp_loadField.
wp_loadField.
wp_apply (wp_MapGet with "HlastRepliesM").
iIntros (??) "[%HlastReply HlastRepliesM]".
wp_pures.
wp_if_destruct.
wp_auto.
wp_apply (wp_MapGet with "HlastRepliesM") as (??) "[%HlastReply HlastRepliesM]".
wp_if_destruct; wp_auto.
{ (* case: this is a duplicate request *)
wp_loadField.
wp_apply (release_spec with "[-HΦ Hspec]").
{
iFrame "∗#". iNext.
Expand All @@ -826,18 +738,8 @@ Proof.
iApply "HΦ".
iApply "Hspec".
}
wp_loadField.
wp_loadField.
wp_apply (wp_MapGet with "HkvsM").
iIntros (?? )"[Hlookup HkvsM]".
wp_pures.
wp_loadField.
wp_loadField.
wp_apply (wp_MapInsert with "HlastRepliesM").
{ done. }
iIntros "HlastRepliesM".
wp_pures.
wp_loadField.
wp_apply (wp_MapGet with "HkvsM") as (??) "[%Hlookup HkvsM]".
wp_apply (wp_MapInsert with "HlastRepliesM") as "HlastRepliesM"; first done.
wp_apply (release_spec with "[-HΦ Hspec]").
{
iFrame "∗#". iNext.
Expand Down

0 comments on commit 16342a3

Please sign in to comment.