Commit 4661f503 authored by Léon Gondelman's avatar Léon Gondelman
Browse files

wip on combine function (need for vcg_sp) : need to check the new definition...

wip on combine function (need for vcg_sp) : need to check the new definition of vcg_sp and reprove the correctness of vcg_wp; NB: combine_function is implemented in an inefficient way (should be reimplemented using sorting functions on lists)
parent 16e66ba5
......@@ -113,7 +113,6 @@ Section vcg.
| [] => Φ
end.
Lemma vcg_inhale_list_sound' E s t :
wp_interp E (append_inhale_list s t) - env_ps_dv_interp E s wp_interp E t.
Proof.
......@@ -180,12 +179,94 @@ Lemma vcg_inhale_list_sound' E s t :
Notation "l ↦( x , q ) v" :=
(mapsto l x q%Qp v%V) (at level 20, q at level 50, format "l ↦( x , q ) v").
Lemma find_and_remove_env_ps_dv_interp E ps i ps' x q dv :
find_and_remove ps (dLoc i) = Some (ps', (x,q,dv))
env_ps_dv_interp E ps env_ps_dv_interp E ps' (dloc_interp E (dLoc i)) (x , q) (dval_interp E dv).
Proof. unfold env_ps_dv_interp. apply find_and_remove_big_sepL. Qed.
(* vcg_sp E s de = Some (s1, s2, dv)
Instance dval_EqDecision : EqDecision dval.
Proof. solve_decision. Defined.
Fixpoint sum_frac (ps: env_ps_dv) (p: (nat * (level * Qp * dval))) :=
match ps with
| [] => [p]
| (i, ((xi, qi), dvi)) :: ps' =>
match p with
| (j, ((xj, qj), dvj)) =>
if bool_decide (i = j) && bool_decide (xi = xj) && bool_decide (dvi = dvj)
then sum_frac ps' (j, ((xj, Qp_plus qi qj), dvj))
else (i, ((xi, qi), dvi)) :: sum_frac ps' p
end
end.
Lemma env_ps_dv_interp_cons_perm E a b ps:
env_ps_dv_interp E (b :: a :: ps)
env_ps_dv_interp E (a :: b :: ps).
Proof.
unfold env_ps_dv_interp. rewrite !big_opL_cons. iStartProof.
iSplit; iIntros "(? & ? & ?)"; iFrame.
Qed.
Lemma env_ps_dv_interp_tail E b ps1 ps2:
(env_ps_dv_interp E ps1 - env_ps_dv_interp E ps2)
(env_ps_dv_interp E (b :: ps1) - env_ps_dv_interp E (b :: ps2)).
Proof.
iIntros "H (Hb & Hps)".
iFrame. iApply ("H" with "Hps").
Qed.
Lemma sum_frac_correct E p ps:
env_ps_dv_interp E (sum_frac ps p) env_ps_dv_interp E (p :: ps).
Proof.
iInduction ps as [|[j [[xj qj] dvj] ] ts] "IH" forall (p); simpl; iSplit;
try (done || simpl in H0;
simplify_eq /=; iIntros "[H1 H2]"; iFrame);
try eauto; destruct p as [i [[xi qi ] dvi]];
repeat (case_bool_decide; simplify_eq /=; simpl).
- iIntros "H"; iSpecialize ("IH" with "H"). admit.
- rewrite env_ps_dv_interp_cons_perm.
iApply env_ps_dv_interp_tail. iIntros "H". iApply ("IH" with "H").
- rewrite env_ps_dv_interp_cons_perm.
iApply env_ps_dv_interp_tail. iIntros "H". iApply ("IH" with "H").
- rewrite env_ps_dv_interp_cons_perm.
iApply env_ps_dv_interp_tail. iIntros "H". iApply ("IH" with "H").
- admit.
- rewrite env_ps_dv_interp_cons_perm.
iApply env_ps_dv_interp_tail. iIntros "H". iApply ("IH" with "H").
- rewrite env_ps_dv_interp_cons_perm.
iApply env_ps_dv_interp_tail. iIntros "H". iApply ("IH" with "H").
- rewrite env_ps_dv_interp_cons_perm.
iApply env_ps_dv_interp_tail. iIntros "H". iApply ("IH" with "H").
Admitted.
Definition sum_frac_all (ps: env_ps_dv) := fold_left (sum_frac) ps [].
Lemma sum_frac_all_correct_aux E ps acc:
env_ps_dv_interp E (ps ++ acc)
env_ps_dv_interp E (fold_left sum_frac ps acc).
Proof.
revert acc. induction ps.
- done.
- intros acc. simpl. specialize (IHps ((sum_frac acc a))). rewrite -IHps.
rewrite -env_ps_dv_interp_app. rewrite sum_frac_correct.
assert (a :: ps ++ acc = ps ++ a :: acc). admit.
rewrite H0. by rewrite !env_ps_dv_interp_app.
Admitted.
Lemma sum_frac_all_correct E ps :
env_ps_dv_interp E ps env_ps_dv_interp E (sum_frac_all ps).
Proof.
unfold sum_frac_all. rewrite -sum_frac_all_correct_aux.
assert (ps ++ [] = ps). rewrite -app_nil_end; reflexivity.
by rewrite H0.
Qed.
Definition combine ps1 ps2 := sum_frac_all (ps1 ++ ps2).
(* vcg_sp E s de = Some (s1, s2, dv)
- s1 = s / resources for de
- s2 = new resources that you get from de
*)
......@@ -205,14 +286,13 @@ Lemma vcg_inhale_list_sound' E s t :
| dCStore de1 de2 =>
''(s1, s2, dv1) vcg_sp E s de1;
i is_dloc E dv1;
''(s3, ((x, q%Qp), dvi)) find_and_remove s1 (dLoc i);
''(s1', s2', dv2) vcg_sp E s3 de2;
''(s3, ((x, q), dvi)) find_and_remove (combine s1 s2) (dLoc i);
''(s1', s2', dv2) vcg_sp E ((i, ((x,q),dvi)) :: s3) de2;
(* Search for (dLoc i) in the combined s1 and s2 *)
(* NB: this should be fixed, adding 'q' to env as well *)
(* NB: idem for the level 'x', actually, as above *)
if (bool_decide (q = 1%Qp) && bool_decide (x = ULvl))
then Some (s1', (i, ((LLvl, 1%Qp), dv2)) :: s2 ++ s2', dv2)
else None
(* NB: this should be fixed, adding 'q' & 'x' to env *)
if (bool_decide (q = Qp_one) && bool_decide (x = ULvl))
then Some (s1', (i, ((LLvl, 1%Qp), dv2)) :: s2 ++ s2', dv2)
else None
| dCBinOp op de1 de2 =>
''(s1, s2, dv1) vcg_sp E s de1;
''(s1', s2', dv2) vcg_sp E s1 de2;
......@@ -223,15 +303,39 @@ Lemma vcg_inhale_list_sound' E s t :
end
end.
(*Variable l: loc.
(*l := !l + 1 ==> s1 = []; s2 = l ↦ {1,L} 42 ; dv = 42 *)
(*
Eval simpl in match (sum_frac_all
[(0%nat, (ULvl, (1 / 2 / 2)%Qp, dLitV (dLitInt 41))) ; (0%nat, (ULvl, (1 / 2)%Qp, dLitV (dLitInt 41)))]) with l => l end.
Variable l: loc.
(* l := !l + 1 ==> s1 = []; s2 = l ↦ {1,L} 42 ; dv = 42 *)
Eval simpl in vcg_sp [l] [(0%nat,(ULvl, 1%Qp, dLitV (dLitInt 41)))]
(dCBinOp
PlusOp
(dCLoad (dCVal (dLitV (dLitLoc (dLoc 0)))))
(dCLoad (dCVal (dLitV (dLitLoc (dLoc 0)))))).
Eval simpl in vcg_sp [l] [(0%nat,(ULvl, 1%Qp, dLitV (dLitInt 41)))]
(dCLoad (dCVal (dLitV (dLitLoc (dLoc 0))))).
Eval simpl in find_and_remove (combine
[(0%nat, (ULvl, (1 / 2)%Qp, dLitV (dLitInt 41)))]
[(0%nat, (ULvl, (1 / 2)%Qp, dLitV (dLitInt 41)))])
(dLoc 0).
Eval simpl in vcg_sp [l] [(0%nat,(ULvl, 1%Qp, dLitV (dLitInt 41)))]
(dCStore
(dCVal (dLitV (dLitLoc (dLoc 0))))
(dCLoad (dCVal (dLitV (dLitLoc (dLoc 0)))))).
Eval simpl in vcg_sp [l] [(0%nat,(ULvl, 1%Qp, dLitV (dLitInt 41)))]
(dCStore
(dCVal (dLitV (dLitLoc (dLoc 0))))
(dCBinOp
PlusOp
(dCLoad (dCVal (dLitV (dLitLoc (dLoc 0)))))
(dCVal (dLitV (dLitInt 1))))).*)
(dCVal (dLitV (dLitInt 1))))).
Eval simpl in vcg_sp [l] [(0%nat,(ULvl, 1%Qp, dLitV (dLitInt 41)))]
(dCStore
(dCVal (dLitV (dLitLoc (dLoc 0))))
(dCVal (dLitV (dLitInt 1)))).
*)
Lemma vcg_sp_correct E s de s1 s2 dv R :
vcg_sp E s de = Some (s1, s2, dv)
......@@ -257,7 +361,7 @@ Lemma vcg_inhale_list_sound' E s t :
iIntros (?) "[% Hs2']". simplify_eq/=. iExists _, _. iSplit; eauto.
iFrame "Hl2". iIntros "Hl2". iSplit; eauto.
by iFrame.
- specialize (IHde1 s).
- (* specialize (IHde1 s).
destruct (vcg_sp E s de1) as [[[s1' s2'] dv1]|]; simplify_eq /=.
destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
destruct d as [l|?]; simplify_eq/=.
......@@ -265,13 +369,16 @@ Lemma vcg_inhale_list_sound' E s t :
destruct Hfar as [[s3 [[x q] dv'']]|]; simplify_eq/=.
specialize (IHde2 s3).
destruct (vcg_sp E s3 de2) as [[[s1'' s2''] dv2]|]; simplify_eq /=.
unfold combine in *.
destruct ( find_and_remove (sum_frac_all (s1' ++ s2')) (dLoc l))
as [[ s' [[x' q'] dv'] ] |]; simplify_eq /=.
case_bool_decide; simplify_eq/=.
case_bool_decide; simplify_eq/=.
rewrite IHde1; last done. iDestruct "Hs" as "[Hs1' Hawp1]".
rewrite find_and_remove_env_ps_dv_interp; last done.
iDestruct "Hs1'" as "[Hs3 Hl]".
rewrite IHde2; last done.
iDestruct "Hs3" as "[$ Hawp2]".
iDestruct "Hs3" as "[Hs1'' Hawp2]".
iApply (a_store_spec _ _ (λ j, ⌜j = dloc_interp E (dLoc l)⌝ ∧ env_ps_dv_interp E s2')%I with "[Hawp1] Hawp2").
{ iApply (awp_wand with "Hawp1").
iIntros (?) "[% H]". simplify_eq/=. iExists _; eauto. }
......@@ -280,7 +387,7 @@ Lemma vcg_inhale_list_sound' E s t :
iIntros "Hl". iSplit; eauto.
iFrame "Hl".
iCombine "Hs2' Hs2''" as "Hs2". (* TODO: how it's working with append here ? *)
iFrame.
iFrame. *) admit.
- specialize (IHde1 s).
destruct (vcg_sp E s de1) as [[[s1' s2'] dv1]|]; simplify_eq /=.
specialize (IHde2 s1').
......@@ -294,7 +401,7 @@ Lemma vcg_inhale_list_sound' E s t :
iExists (dval_interp E dv). repeat iSplit; eauto.
+ iPureIntro. apply dbin_op_eval_correct. rewrite -HeqHboe. reflexivity.
+ iCombine "Hs2' Hs2''" as "Hs2". iFrame.
Qed.
Admitted.
(* TODO: fix the Qp's correctly using vcg_sp *)
Fixpoint vcg_wp (E: env_locs) (s: env_ps_dv) (de : dcexpr) (R : iProp Σ) (Φ : dval wp_expr) : wp_expr :=
......
Supports Markdown
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