Commit 0e5fd3bb authored by Léon Gondelman's avatar Léon Gondelman

a small clean up, putting functions working on env_ps_dv in a separate file 'env.v'

parent c04e7a10
......@@ -10,6 +10,7 @@ theories/c_translation/proofmode.v
theories/c_translation/translation.v
theories/c_translation/derived.v
theories/vcgen/dcexpr.v
theories/vcgen/env.v
theories/vcgen/splitenv.v
theories/vcgen/vcgen.v
# theories/vcgen/test.v
......
......@@ -24,6 +24,9 @@ From iris_c.c_translation Require Import monad translation proofmode.
| dLitV : dbase_lit dval
| dValUnknown : val dval.
Global Instance dval_EqDecision : EqDecision dval.
Proof. solve_decision. Defined.
Inductive doption (A : Type) : Type :=
| dNone : doption A
| dSome : A doption A
......
From iris.proofmode Require Import environments coq_tactics.
Import env_notations.
From iris_c.vcgen Require Import dcexpr.
From iris_c.lib Require Import U locking_heap.
From iris_c.c_translation Require Import monad.
From iris.algebra Require Import frac.
Section env.
Context `{amonadG Σ}.
Notation "l ↦( x , q ) v" :=
(mapsto l x q%Qp v%V) (at level 20, q at level 50, format "l ↦( x , q ) v").
Definition env_locs := list loc.
Definition is_dloc (E: env_locs) (dv: dval) : option nat :=
match dv with
| dLitV (dLitLoc (dLoc i)) => Some i
| _ => None
end.
Definition env_ps := list (loc * ((level * frac) * val)).
Definition env_ps_dv := list (nat * ((level * frac) * dval)).
Definition ps_loc {A B: Type} (p : A * ((level * frac) * B)) : A := p.1.
Definition ps_frc {A B: Type} (p : A * ((level * frac) * B)) : frac := p.2.1.2.
Definition ps_lvl {A B: Type} (p : A * ((level * frac) * B)) : level := p.2.1.1.
Definition ps_val {A B: Type} (p : A * ((level * frac) * B)) : B := p.2.2.
Definition env_ps_interp (ps : env_ps) : iProp Σ :=
([ list] p ps, ps_loc p (ps_lvl p, ps_frc p) ps_val p)%I.
Definition env_ps_dv_interp E (ps : env_ps_dv) : iProp Σ :=
([ list] p ps,
dloc_interp E (dLoc (ps_loc p)) (ps_lvl p, ps_frc p) dval_interp E (ps_val p))%I.
Lemma env_ps_dv_interp_app E s1 s2 :
((env_ps_dv_interp E s1 env_ps_dv_interp E s2))%I (env_ps_dv_interp E (s1 ++ s2))%I.
Proof. by unfold env_ps_dv_interp; rewrite big_sepL_app. Qed.
Lemma env_ps_dv_interp_cons E p ps:
dloc_interp E (dLoc (ps_loc p)) (ps_lvl p,ps_frc p) dval_interp E (ps_val p)
env_ps_dv_interp E ps env_ps_dv_interp E (p :: ps).
Proof.
unfold env_ps_dv_interp. rewrite !big_opL_cons. iStartProof.
iSplit; eauto with iFrame.
Qed.
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_mono 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.
Fixpoint find_and_remove (ps: env_ps_dv) (dl: dloc) :
option (env_ps_dv * ((level * frac) * dval)) :=
match ps with
| [] => None
| (i, (xq, dv)) :: ps' =>
if (bool_decide (dl = dLoc i))
then Some (ps', (xq, dv))
else match find_and_remove ps' dl with
| None => None
| Some (rs, w) => Some ((i,(xq, dv)) :: rs, w)
end
end.
Lemma find_and_remove_dLocUnknown ps l :
find_and_remove ps (dLocUnknown l) = None.
Proof. induction ps as [|[? [? ?]] ?]; eauto; simpl; by rewrite IHps. Qed.
Lemma find_and_remove_dLocKnown ps ps' d w' :
find_and_remove ps d = Some (ps', w') i, d = dLoc i.
Proof.
case d; eauto; intros ?; rewrite find_and_remove_dLocUnknown; inversion 1.
Qed.
Lemma find_and_remove_big_sepL ps i ps' w' (Φ : nat * ((level * frac) * dval) iProp Σ) :
find_and_remove ps (dLoc i) = Some (ps', w')
([ list] lw ps, Φ lw)%I (([ list] lw ps', Φ lw) Φ (i, w'))%I.
Proof.
iIntros (Hfind). iInduction ps as [|[j [q dw] ] ts] "IH" forall (ps' Hfind);
simpl; iSplit; try (done || simpl in H0; case_bool_decide;
simplify_eq /=; iIntros "[H1 H2]"; iFrame); simpl in Hfind;
iIntros "[HΦ Hlst]"; case_bool_decide; simplify_eq /=; [iFrame| |iFrame|].
- destruct (find_and_remove ts (dLoc i)); simplify_eq /=.
destruct p; simplify_eq /=. iFrame. by iApply "IH".
- destruct (find_and_remove ts (dLoc i)); simplify_eq /=.
destruct p; simplify_eq /=. iDestruct "HΦ" as "[HΦ Hl]".
iFrame. iApply ("IH" $! e); first done. iFrame.
Qed.
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.
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 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").
rewrite (app_comm_cons []).
rewrite -!env_ps_dv_interp_cons. iDestruct "IH" as "(H1 & $)". simpl.
rewrite mapsto_fractional. iDestruct "H1" as "(H1 & H2)". iFrame.
- rewrite env_ps_dv_interp_cons_perm.
iApply env_ps_dv_interp_mono. iIntros "H". iApply ("IH" with "H").
- rewrite env_ps_dv_interp_cons_perm.
iApply env_ps_dv_interp_mono. iIntros "H". iApply ("IH" with "H").
- rewrite env_ps_dv_interp_cons_perm.
iApply env_ps_dv_interp_mono. iIntros "H". iApply ("IH" with "H").
- iIntros "H". iApply "IH". rewrite (app_comm_cons []).
rewrite -!env_ps_dv_interp_cons. iDestruct "H" as "(H1 & H2 & H3)". iFrame.
- rewrite env_ps_dv_interp_cons_perm.
iApply env_ps_dv_interp_mono. iIntros "H". iApply ("IH" with "H").
- rewrite env_ps_dv_interp_cons_perm.
iApply env_ps_dv_interp_mono. iIntros "H". iApply ("IH" with "H").
- rewrite env_ps_dv_interp_cons_perm.
iApply env_ps_dv_interp_mono. iIntros "H". iApply ("IH" with "H").
Qed.
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.
rewrite !app_comm_cons.
rewrite (app_comm_cons [] acc).
rewrite (app_comm_cons [] ps).
rewrite -!env_ps_dv_interp_app.
iStartProof. iSplit.
+ iIntros "[[H1 H2] H3]"; eauto with iFrame.
+ iIntros "(H1 & H2 & H3)". eauto with iFrame.
Qed.
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 find_and_remove_2 s1 s2 dl :=
match find_and_remove (sum_frac_all s1) dl, find_and_remove (sum_frac_all s2) dl with
| Some (s1', ((x1, q1), dv1)), Some (s2', ((x2, q2), dv2)) =>
if bool_decide (x1 = x2) && bool_decide (dv1 = dv2)
then Some (s1', s2', ((x2, Qp_plus q1 q2), dv2))
else Some (s1', s2, ((x1, q1), dv1))
| Some (s1', ((x1, q1), dv1)), None => Some (s1', s2, ((x1, q1), dv1))
| None, Some (s2', ((x2, q2), dv2)) => Some (s1, s2', ((x2, q2), dv2))
| None, None => None
end.
Lemma find_and_remove_2_env_ps_dv_interp E ps1 ps2 i ps1' ps2' x q dv :
find_and_remove_2 ps1 ps2 (dLoc i) = Some (ps1', ps2', (x,q, dv))
env_ps_dv_interp E ps1 -
(env_ps_dv_interp E ps1' (env_ps_dv_interp E ps2 - env_ps_dv_interp E ps2'
(dloc_interp E (dLoc i)) (x , q) (dval_interp E dv))).
(* env_ps_dv_interp E (ps1 ++ ps2) ⊣⊢
env_ps_dv_interp E ps1' ∗ env_ps_dv_interp E ps2' ∗
(dloc_interp E (dLoc i)) ↦(x , q) (dval_interp E dv). *)
Proof.
rewrite /find_and_remove_2.
rewrite (sum_frac_all_correct _ ps1).
rewrite (sum_frac_all_correct _ ps2).
remember (find_and_remove (sum_frac_all ps1) (dLoc i)) as Hfar1.
destruct Hfar1 as [[s1 [ [x1 q1] dv1]]|].
remember (find_and_remove (sum_frac_all ps2) (dLoc i)) as Hfar2.
destruct Hfar2 as [[s2 [ [x2 q2] dv2]]|].
repeat (case_bool_decide; simplify_eq /=); intros; simplify_eq /=.
- rewrite find_and_remove_env_ps_dv_interp; last eauto.
rewrite (find_and_remove_env_ps_dv_interp _ (sum_frac_all ps2)); last eauto.
iIntros "[Hps1' Hi1]". eauto with iFrame.
- rewrite find_and_remove_env_ps_dv_interp; last eauto.
rewrite -(sum_frac_all_correct _ ps2').
iIntros "[$ Hi1]". iIntros "Hps2'". iFrame.
- rewrite find_and_remove_env_ps_dv_interp; last eauto.
rewrite -(sum_frac_all_correct _ ps2').
iIntros "[$ Hi1]". iIntros "Hps2'". iFrame.
- rewrite find_and_remove_env_ps_dv_interp; last eauto.
intros; simplify_eq/=. rewrite -(sum_frac_all_correct _ ps2').
iIntros "[$ Hi1]". iIntros "Hps2'". iFrame.
- remember (find_and_remove (sum_frac_all ps2) (dLoc i)) as Hfar2.
destruct Hfar2 as [[s2 [ [x2 q2] dv2]]|].
repeat (case_bool_decide; simplify_eq /=); intros; simplify_eq /=.
+ rewrite (find_and_remove_env_ps_dv_interp _ (sum_frac_all ps2)); last eauto.
rewrite -!sum_frac_all_correct.
eauto with iFrame.
+ inversion 1.
Qed.
End env.
\ No newline at end of file
From iris.proofmode Require Import environments coq_tactics.
Import env_notations.
From iris_c.vcgen Require Import dcexpr.
From iris_c.vcgen Require Import dcexpr env.
From iris_c.lib Require Import U locking_heap.
From iris_c.c_translation Require Import monad.
From iris.algebra Require Import frac.
......@@ -8,54 +8,8 @@ From iris.algebra Require Import frac.
Section splitenv.
Context `{amonadG Σ}.
Definition env_locs := list loc.
Definition env_ps := list (loc * ((level * frac) * val)).
Definition env_ps_dv := list (nat * ((level * frac) * dval)).
Definition ps_loc {A B: Type} (p : A * ((level * frac) * B)) : A := p.1.
Definition ps_frc {A B: Type} (p : A * ((level * frac) * B)) : frac := p.2.1.2.
Definition ps_lvl {A B: Type} (p : A * ((level * frac) * B)) : level := p.2.1.1.
Definition ps_val {A B: Type} (p : A * ((level * frac) * B)) : B := p.2.2.
Notation "l ↦( x , q ) v" :=
(mapsto l x q%Qp v%V) (at level 20, q at level 50, format "l ↦( x , q ) v").
Definition env_ps_interp (ps : env_ps) : iProp Σ :=
([ list] p ps, ps_loc p (ps_lvl p, ps_frc p) ps_val p)%I.
Definition env_ps_dv_interp E (ps : env_ps_dv) : iProp Σ :=
([ list] p ps,
dloc_interp E (dLoc (ps_loc p)) (ps_lvl p, ps_frc p) dval_interp E (ps_val p))%I.
Lemma env_ps_dv_interp_app E s1 s2 :
((env_ps_dv_interp E s1 env_ps_dv_interp E s2))%I (env_ps_dv_interp E (s1 ++ s2))%I.
Proof. by unfold env_ps_dv_interp; rewrite big_sepL_app. Qed.
Lemma env_ps_dv_interp_cons E p ps:
dloc_interp E (dLoc (ps_loc p)) (ps_lvl p,ps_frc p) dval_interp E (ps_val p)
env_ps_dv_interp E ps env_ps_dv_interp E (p :: ps).
Proof.
unfold env_ps_dv_interp. rewrite !big_opL_cons. iStartProof.
iSplit; eauto with iFrame.
Qed.
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_mono 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.
(mapsto l x q%Qp v%V) (at level 20, q at level 50, format "l ↦( x , q ) v").
Definition env_to_known_locs (Γls : env_ps) : env_locs := map fst Γls.
......
This diff is collapsed.
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