Commit 3c9f273a authored by Léon Gondelman's avatar Léon Gondelman

add tactic to simplify the result of a vcg_solver.

parent cf976fa7
......@@ -19,6 +19,7 @@ theories/vcgen/tests/basics.v
theories/vcgen/tests/unknowns.v
theories/vcgen/tests/test.v
theories/vcgen/tests/swap.v
theories/vcgen/tests/fact.v
theories/tests/test1.v
theories/tests/test2.v
theories/tests/fact.v
......
From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.bi Require Import big_op.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
From iris_c.c_translation Require Import monad translation notation proofmode derived.
From iris_c.lib Require Import locking_heap U.
Definition incr : val := λ: "l",
a_store (a_ret "l") (a_bin_op PlusOp (a_load (a_ret "l")) (a_ret #1)).
Definition factorial_body : val := λ: "n" "c" "r",
a_while
(λ:<>, a_bin_op LtOp (a_load (a_ret "c")) (a_ret "n"))
(λ:<>, incr "c" ;;;;
a_store (a_ret "r")
(a_bin_op MultOp (a_load (a_ret "r")) (a_load (a_ret "c")))).
Definition factorial : val := λ: "n",
a_bind ( λ: "r",
a_bind (λ: "k",
factorial_body "n" "k" "r" ;;;;
(a_load (a_ret "r")))
(a_alloc (a_ret #0%V)))
(a_alloc (a_ret #1%V)).
Section factorial_spec.
Context `{amonadG Σ}.
Lemma incr_spec (l : loc) (n : Z) R Φ :
l C #n - (l C[LLvl] #(n+1) - Φ #(n+1)) -
awp (incr #l) R Φ.
Proof.
iIntros "Hl HΦ". awp_lam. vcg_solver.
Qed.
Lemma factorial_body_spec (n k : nat) (c r: loc) R :
(k n c C[ULvl] #k r C #(fact k)) -
awp (factorial_body #n #c #r) R
(λ _, c C #n r C #(fact n))%I.
Proof.
iIntros "(Hk & Hc & Hr)". do 3 awp_lam.
iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_while_spec. iNext.
iDestruct "Hk" as %Hk. iApply a_if_spec.
vcg_solver. iIntros "Hr Hc".
case_bool_decide.
+ iLeft. iSplit; eauto. awp_lam. rewrite Qp_half_half.
iApply a_sequence_spec. awp_seq. iApply a_sequence_spec.
iApply (incr_spec with "[$Hc]"). iIntros "Hc".
iModIntro. awp_seq. vcg_solver. iIntros "Hc Hr".
iModIntro.
assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
{ rewrite Nat.add_1_r /fact. lia. }
assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia. awp_seq.
iApply ("IH" $! n (k+1)%nat with "[] Hc Hr"). iPureIntro. lia.
+ iRight. iSplit; eauto. iApply a_seq_spec. iModIntro.
assert (k = n) as -> by lia. rewrite Qp_half_half. by iFrame.
Qed.
Lemma factorial_spec (n: nat) R :
awp (factorial #n) R (λ v, v = #(fact n))%I.
Proof.
awp_lam.
iApply awp_bind. awp_alloc_ret r "Hr".
iApply awp_bind. awp_alloc_ret c "Hc".
iApply a_sequence_spec.
iApply (awp_wand _ (λ _, c C #n r C #(fact n))%I with "[Hr Hc]").
- iApply ((factorial_body_spec n 0 c r) with "[$Hr $Hc]"); eauto with lia.
- iIntros (?) "[Hc Hr]". iModIntro. awp_seq.
awp_load_ret r.
Qed.
Lemma factorial_spec_with_inv (n: nat) R :
awp (factorial #n) R (λ v, v = #(fact n))%I.
Proof.
awp_lam.
iApply awp_bind. awp_alloc_ret r "Hr".
iApply awp_bind. awp_alloc_ret c "Hc".
iApply a_sequence_spec. do 3 awp_lam.
iApply (a_while_inv_spec
(k:nat, k n c C #k r C #(fact k))%I with "[Hr Hc]").
- iExists O. eauto with iFrame lia.
- iModIntro. iIntros "H". iDestruct "H" as (k) "(H & Hc & Hr)".
vcg_solver. iIntros "Hr Hc".
case_bool_decide.
+ iRight. iSplit; eauto.
iApply a_sequence_spec. rewrite Qp_half_half.
iApply (incr_spec with "[$Hc]").
iIntros "Hc". iModIntro. awp_seq. vcg_solver.
iIntros "Hc Hr". iModIntro.
assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
{ rewrite Nat.add_1_r /fact. lia. }
assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
iExists (k+1)%nat. eauto with iFrame lia.
+ iLeft. iSplit; eauto. do 2 iModIntro. awp_seq.
iRevert "H". iIntros "%". assert (k = n) as -> by lia.
by awp_load_ret r.
Qed.
End factorial_spec.
......@@ -9,30 +9,18 @@ Section tests_vcg.
Context `{amonadG Σ}.
From iris.proofmode Require Import environments coq_tactics.
Import env_notations.
Lemma tac_exists_known_locs Γs_in Γs_out Γls Γp c ps (Φ: known_locs denv iProp Σ):
MapstoListFromEnv Γs_in Γs_out Γls
ListOfMapsto Γls (penv_to_known_locs Γls) ps
envs_entails (Envs Γp Γs_out c) (denv_interp (penv_to_known_locs Γls) ps -
Φ (penv_to_known_locs Γls) ps)
envs_entails (Envs Γp Γs_in c) ( (E': known_locs) (m': denv), Φ E' m')%I.
Admitted.
Lemma test0 (l : loc) (e: expr) `{Closed [] e}:
l C #1 - awp e True (λ _, True) - awp (e ; ∗ᶜ l) True (λ v, l C #1).
Lemma test0 (l1 l2 : loc) (e: expr) `{Closed [] e}:
l1 C #1 - l2 C #1 - awp e True (λ _, True) - awp (alloc 1; e ; ∗ᶜ l1) True (λ v, l1 C #1 l2 C #1).
Proof.
iIntros "Hl Hawp". vcg_solver. iIntros "Hk".
iApply (awp_wand with "Hawp"). iIntros (v ?).
eapply tac_exists_known_locs; try apply _; simpl.
iIntros "Hl". rewrite /denv_interp; simpl.
(* this part should be automated using a class for dval_interp and solving wf, prefix_of stuff *)
iExists (dValUnknown _). iSplit. iPureIntro. eexists. simpl.
repeat (iSplit; [done|]).
(*/ end of to be automated part *)
iFrame "Hl". iIntros "!> Hl". done.
Qed.
iIntros "Hl1 Hl2 Hawp". vcg_solver.
iIntros "Hl2 Hl1". iApply a_alloc_spec. awp_ret_value.
iIntros (k) "Hk".
vcg_continue.
iModIntro.
iIntros "Hl2 Hl1 Hk".
Abort.
Lemma test1 (l k : loc) (e: expr) `{Closed [] e}:
( Φ v, k C v - (k C #12 - Φ v) - awp e True Φ) -
......@@ -45,35 +33,21 @@ Admitted.
Proof.
iIntros "#He Hl Hk". vcg_solver.
iIntros "Hk". iApply ("He" with "Hk"); iIntros "Hk".
(* this part should be automated *)
iExists [k;l], [Some (DenvItem ULvl 1 (dLitV (dLitInt 12)))].
iExists (dLitV (dLitInt 10)).
iSplit; [done|]. iSplit; [done|].
iFrame "Hk"; iSplitR; first done.
simpl. iIntros "!> Hk Hl".
vcg_continue.
iIntros "!> Hk Hl".
iApply ("He" with "Hk"); iIntros "Hk".
iExists [k;l], [Some (DenvItem ULvl 1 (dLitV (dLitInt 12)));
Some (DenvItem ULvl 1 (dLitV (dLitInt 2)))].
iExists (dLitV (dLitInt 12)). iSplit; [done|]. iSplit; [done|].
iFrame "Hl Hk". iSplitR; first done.
simpl. auto.
vcg_continue. eauto.
Qed.
Lemma test3 (k : loc) :
k C #10 - awp (alloc 11 = ∗ᶜ♯k + 2) True (λ v, True).
Proof.
iIntros "Hk". vcg_solver.
iIntros "Hk".
iApply a_alloc_spec. iApply awp_ret. iApply wp_value.
iApply a_alloc_spec. iApply awp_ret. iApply wp_value.
iIntros (l) "Hl".
iExists [k;l], [Some (DenvItem ULvl (1/2) (dLitV (dLitInt 10)));
Some (DenvItem ULvl 1 (dLitV (dLitInt 11)))],
(dLitV (dLitLoc (dLoc 1))).
iSplit; first done.
iSplit. iPureIntro. apply prefix_cons, prefix_nil.
iFrame "Hl Hk". iSplitR; first done.
simpl. auto.
vcg_continue.
eauto 42 with iFrame.
Qed.
(*
......
......@@ -4,7 +4,64 @@ From iris.bi Require Import big_op.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen.
From iris_c.c_translation Require Import monad translation proofmode notation.
From iris_c.lib Require Import locking_heap U.
From iris.proofmode Require Import environments coq_tactics.
Import env_notations.
Section vcg_continue.
Context `{amonadG Σ}.
Class FromKnownLocs (Γls : penv) (E_old : known_locs) (E_new : known_locs) :=
from_known_locs: True. (*dom Γls ⊂ (elem_of E_old) disj_Union (elem_of E) *)
Global Instance from_known_locs_Nil E_old:
FromKnownLocs [] E_old [].
Proof. done. Qed.
Global Instance from_known_locs_old_cons Γls E_old E_new x q v l i:
LocLookup E_old l i
FromKnownLocs Γls E_old E_new
FromKnownLocs (PenvItem l x q v :: Γls) E_old E_new.
Proof. done. Qed.
Global Instance from_known_locs_new_cons Γls E_old E_new x q v l:
FromKnownLocs Γls E_old E_new
FromKnownLocs (PenvItem l x q v :: Γls) E_old (l :: E_new) | 100.
Proof. done. Qed.
Lemma tac_exists_known_locs Γs_in Γs_out Γls Γp c ps v E_old E_new (Φ: known_locs denv dval iProp Σ):
MapstoListFromEnv Γs_in Γs_out Γls
FromKnownLocs Γls E_old E_new
ListOfMapsto Γls (E_old ++ E_new) ps
envs_entails (Envs Γp Γs_out c)
(denv_wf (E_old ++ E_new) ps Φ (E_old ++ E_new) ps (dValUnknown v))
envs_entails (Envs Γp Γs_in c)
( (E': known_locs) (m': denv) (dv: dval),
v = dval_interp E' dv E_old `prefix_of` E'
(denv_wf E' m')
dval_wf E' dv
denv_interp E' m'
Φ E' m' dv)%I.
Proof.
intros Hsplit. rewrite /ListOfMapsto environments.envs_entails_eq=> Hexhale.
unfold of_envs. simpl. intros HGls Hgoal.
rewrite mapsto_list_from_env.
iIntros "(Hwf & #Hp & Hs & Hls)". iDestruct "Hwf" as %Hwf.
iPoseProof (Hgoal with "[Hs]") as "[% H]".
{ repeat iSplit; eauto.
iPureIntro. split; eauto.
+ apply Hwf.
+ apply Hsplit. apply Hwf.
+ intros i. simpl. destruct (envs_disjoint _ Hwf i) as [Hp | Hp]; simpl in Hp.
* by left.
* right. by apply Hsplit.
}
iExists (E_old++E_new), ps, (dValUnknown v). repeat iSplit; eauto using prefix_app_r.
iFrame. by iApply HGls.
Qed.
End vcg_continue.
(* TODO: How to avoid computing mapsto_wand and dloc under vcg_wp_unknown ? *)
(* Arguments dloc_interp : simpl never. *)
......@@ -26,3 +83,11 @@ Ltac vcg_solver :=
| apply _ (* ListOfMapsto Γls E m *)
| apply _ (* IntoDCexpr E e dce *)
| vcg_compute; simpl ]; intuition.
Ltac vcg_continue :=
eapply tac_exists_known_locs;
[ apply _ (* MapstoListFromEnv Γs_in Γs_out Γls *)
| apply _ (* FromKnownLocs Γls E_old E_new *)
| apply _ (* ListOfMapsto Γls (E_old ++ E_new) ps *)
| repeat (iSplit; first done); simpl
].
\ No newline at end of file
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