Commit 4cff19f9 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Change the definition of [has_disjoint_siblings].

parent 30cdb30f
Pipeline #44299 passed with stage
in 18 minutes and 3 seconds
......@@ -233,22 +233,31 @@ Definition allocation_in_range (al : allocation) : Prop :=
Instance elem_of_alloc : ElemOf addr allocation :=
λ a al, al.(al_start) a < al_end al.
Definition has_disjoint_siblings (am : allocs) (id1 : alloc_id) (al1 : allocation) : Prop :=
id2 al2,
id2 id1
am !! id2 = Some al2
al1.(al_alive) = true
al2.(al_alive) = true
al2.(al_parent) = al1.(al_parent)
al1 ## al2.
Lemma has_disjoint_siblings_insert am id1 id2 al1 al2 :
am !! id2 = Some al2
has_disjoint_siblings am id1 al1
has_disjoint_siblings am id2 al2
has_disjoint_siblings (<[id1:=al1]> am) id2 al2.
Proof.
move => Hid2 Hdisj1 Hdisj2 id0 al0 Hne Hid0 ?? Hpar.
Definition has_disjoint_siblings (am : allocs) (id1 : alloc_id) : Prop :=
al1,
am !! id1 = Some al1
id2 al2,
id2 id1
am !! id2 = Some al2
al1.(al_alive) = true
al2.(al_alive) = true
al2.(al_parent) = al1.(al_parent)
al1 ## al2.
Lemma has_disjoint_siblings_insert am id1 id2 al1:
am !! id1 = Some al1
has_disjoint_siblings am id1
has_disjoint_siblings am id2
has_disjoint_siblings (<[id1:=al1]> am) id2.
Proof.
move => Hid1 [al1'][Hid1']Hdisj1 [al2][Hid2]Hdisj2.
rewrite Hid1 in Hid1'. move: Hid1' => [] ?. subst al1'.
exists al2. split. {
destruct (decide (id2 = id1)) as [->|].
- by rewrite lookup_insert -Hid1 -Hid2.
- by rewrite lookup_insert_ne.
}
move => id0 al0 Hne Hid0 ?? Hpar.
destruct (decide (id0 = id1)) as [->|].
+ rewrite lookup_insert in Hid0. simplify_eq.
assert (al0 ## al2); last by set_solver. by eapply Hdisj1.
......@@ -256,10 +265,14 @@ Proof.
Qed.
Lemma has_disjoint_siblings_insert_id am id al:
has_disjoint_siblings am id al
has_disjoint_siblings (<[id:=al]> am) id al.
am !! id = Some al
has_disjoint_siblings am id
has_disjoint_siblings (<[id:=al]> am) id.
Proof.
move => Hdisj ???. rewrite lookup_insert_ne; naive_solver.
move => Hid [al'][Hid']Hdisj.
rewrite Hid in Hid'. move: Hid' => [] ?. subst al'.
exists al. split; first by rewrite lookup_insert.
move => ???. rewrite lookup_insert_ne; naive_solver.
Qed.
(** ** Representation of the state of the heap and allocation operations. *)
......@@ -364,7 +377,7 @@ Inductive push_new_block : heap_state → loc → alloc_id → nat → heap_stat
al al_p
length v = n
heap_lookup a v (λ cur_id, cur_id = id_p) (λ lk, lk = RSt 0) σ.(hs_heap)
has_disjoint_siblings σ.(hs_allocs) id al
has_disjoint_siblings (<[id := al]> σ.(hs_allocs)) id
push_new_block σ l id n {|
hs_heap := heap_update a (replicate n MPoison) (λ _, id) (λ _, RSt 0) σ.(hs_heap);
hs_allocs := <[id := al]> σ.(hs_allocs);
......@@ -397,7 +410,7 @@ Inductive valid_root_path (am : allocs) (id : alloc_id) : list alloc_id → Prop
am !! id = Some al
al.(al_parent) = None
allocation_in_range al
has_disjoint_siblings am id al
has_disjoint_siblings am id
valid_root_path am id []
| Valid_root_path_cons id2 ids al1 al2 :
am !! id = Some al1
......@@ -406,14 +419,14 @@ Inductive valid_root_path (am : allocs) (id : alloc_id) : list alloc_id → Prop
al1.(al_parent) = Some id2
al1 al2
(al1.(al_alive) = true al2.(al_alive) = true)
has_disjoint_siblings am id al1
has_disjoint_siblings am id
valid_root_path am id2 ids
valid_root_path am id (id2 :: ids).
Lemma valid_root_path_disjoint_siblings am id ids al:
valid_root_path am id ids
am !! id = Some al
has_disjoint_siblings am id al.
has_disjoint_siblings am id.
Proof.
move => [].
- move => ? -> *. by simplify_eq.
......@@ -423,20 +436,35 @@ Qed.
Lemma valid_root_path_insert_not_in am id0 al0 id ids:
valid_root_path am id ids
id0 id :: ids
has_disjoint_siblings am id0 al0
am !! id0 = None
has_disjoint_siblings (<[id0:=al0]> am) id0
valid_root_path (<[id0:=al0]> am) id ids.
Proof.
elim; clear.
- move => id al ??? Hdisj1 ? Hdisj2.
- move => id al ??? Hdisj1 ? ? Hdisj2.
eapply Valid_root_path_singleton => //.
rewrite lookup_insert_ne; [ done | set_solver | .. ].
by eapply has_disjoint_siblings_insert.
- move => id1 id2 al1 al2 ??????? Hdisj1 ? IH ? Hdisj2.
destruct Hdisj1 as [al1 [??]].
exists al1. split. { rewrite lookup_insert_ne //. set_solver. }
move => id2 ?? Hid2 *. destruct (decide (id2 = id0)) as [->|].
+ rewrite lookup_insert in Hid2. simplify_eq.
destruct Hdisj2 as [?[H ?]]. rewrite lookup_insert in H. simplify_eq.
assert (x ## al); last by set_solver. eapply H1 => //.
by rewrite lookup_insert_ne => //.
+ eapply H0 => //. by rewrite lookup_insert_ne in Hid2.
- move => id1 id2 al1 al2 ??????? Hdisj1 ? IH ?? Hdisj2.
eapply Valid_root_path_cons => //.
{ rewrite lookup_insert_ne; [ done | set_solver ]. }
{ rewrite lookup_insert_ne; [ done | set_solver ]. }
{ by eapply has_disjoint_siblings_insert. }
apply IH; [set_solver | done].
{ destruct Hdisj1 as [al [??]]. exists al.
split. { rewrite lookup_insert_ne; first done. set_solver. }
move => id3 ?? Hid3 *. destruct (decide (id3 = id0)) as [->|].
* rewrite lookup_insert in Hid3. simplify_eq.
destruct Hdisj2 as [?[H ?]]. rewrite lookup_insert in H. simplify_eq.
assert (x ## al2); last by set_solver. eapply H1 => //.
by rewrite lookup_insert_ne => //.
* eapply H0 => //. by rewrite lookup_insert_ne in Hid3. }
apply IH; [set_solver | done | done].
Qed.
Lemma valid_root_path_subset am id1 id2 al1 al2 ids:
......@@ -530,21 +558,26 @@ Lemma allocs_wf_insert_root (am : allocs) (id : alloc_id) (al : allocation) :
allocation_in_range al
al.(al_parent) = None
am !! id = None
has_disjoint_siblings am id al
has_disjoint_siblings (<[id := al]> am) id
allocs_wf am
allocs_wf (<[id := al]> am).
Proof.
move => Hal1 Hal2 Hid Hdisj Hwf id0 [al0 Hid0].
destruct Hdisj as [al' [Heq Hdisj]].
rewrite lookup_insert in Heq; move: Heq => []?; subst al'.
destruct (decide (id0 = id)) as [->|].
- exists [].
eapply Valid_root_path_singleton;
[rewrite lookup_insert //|..] => //.
exists al. split; first by rewrite lookup_insert.
move => ??? H *. rewrite lookup_insert_ne // in H.
rewrite lookup_insert in Hid0. simplify_eq. by eapply Hdisj.
rewrite lookup_insert in Hid0. simplify_eq.
eapply Hdisj => //. by rewrite lookup_insert_ne.
- rewrite lookup_insert_ne // in Hid0.
apply mk_is_Some in Hid0.
move: (Hwf id0 Hid0) => [ids H].
exists ids. apply valid_root_path_insert_not_in => //.
exists ids. apply valid_root_path_insert_not_in => //; last first.
{ exists al. rewrite lookup_insert. done. }
move => /elem_of_cons [] // ?.
assert (is_Some (am !! id)) as [? Habsurd]; last by rewrite Hid in Habsurd.
eapply valid_root_path_ids_in_allocs => //. set_solver.
......@@ -556,7 +589,7 @@ Lemma allocs_wf_insert_node (am : allocs) (id1 id2 : alloc_id) (al1 al2 : alloca
al1.(al_parent) = Some id2
am !! id1 = None
am !! id2 = Some al2
has_disjoint_siblings am id1 al1
has_disjoint_siblings (<[id1 := al1]> am) id1
allocs_wf am
allocs_wf (<[id1 := al1]> am).
Proof.
......@@ -568,7 +601,6 @@ Proof.
eapply Valid_root_path_cons; [by rewrite lookup_insert|..] => //.
{ rewrite lookup_insert_ne //. naive_solver. }
{ naive_solver. }
{ move => ??? Ham ?. rewrite lookup_insert_ne // in Ham. by eapply Hdisj. }
apply valid_root_path_insert_not_in => //.
move => /elem_of_cons [] ?; first naive_solver.
assert (is_Some (am !! id1)) as [? Habsurd]; last by rewrite Hid1 in Habsurd.
......@@ -601,12 +633,15 @@ Proof.
destruct (decide (idr = id)) as [->|].
+ eapply Valid_root_path_singleton;
[by rewrite lookup_insert|..]; try naive_solver.
eexists; split; first by rewrite lookup_insert.
move => ??? H ???. simplify_eq.
+ eapply Valid_root_path_singleton;
[by rewrite lookup_insert_ne|..]; try naive_solver.
eexists; split; first by rewrite lookup_insert_ne.
move => idx ?? H ???. destruct (decide (idx = id)) as [->|].
* rewrite lookup_insert in H. simplify_eq.
* rewrite lookup_insert_ne // in H. simplify_eq. by eapply Hdisj.
* rewrite lookup_insert_ne // in H. simplify_eq.
destruct Hdisj as [?[? Hdisj]]. simplify_eq. by eapply Hdisj.
- move => id1 id2 al1 al2 ??????? Hdisj ??.
destruct (decide (id1 = id)) as [->|];
destruct (decide (id2 = id)) as [->|].
......@@ -616,20 +651,25 @@ Proof.
+ eapply Valid_root_path_cons;
[by rewrite lookup_insert|..];
rewrite ?lookup_insert_ne; try naive_solver.
eexists; split; first by rewrite lookup_insert.
move => ??? H ???. simplify_eq.
+ assert (al_alive al2 = false) as Hal2. { by eapply Hnac. }
eapply Valid_root_path_cons;
[by rewrite lookup_insert_ne|..];
rewrite ?lookup_insert //; [naive_solver|naive_solver|..].
eexists; split; first by rewrite lookup_insert_ne.
move => idx ?? H ???. destruct (decide (idx = id)) as [->|].
* rewrite lookup_insert in H. simplify_eq.
* rewrite lookup_insert_ne // in H. by eapply Hdisj.
* rewrite lookup_insert_ne // in H. simplify_eq.
destruct Hdisj as [?[? Hdisj]]. simplify_eq. by eapply Hdisj.
+ eapply Valid_root_path_cons;
[by rewrite lookup_insert_ne|..];
rewrite ?lookup_insert_ne //.
eexists; split; first by rewrite lookup_insert_ne.
move => idx ?? H ???. destruct (decide (idx = id)) as [->|].
* rewrite lookup_insert in H. simplify_eq.
* rewrite lookup_insert_ne // in H. by eapply Hdisj.
* rewrite lookup_insert_ne // in H.
destruct Hdisj as [?[? Hdisj]]. simplify_eq. by eapply Hdisj.
Qed.
(** ** Heap state invariant definition. *)
......@@ -684,10 +724,12 @@ Definition heap_state_invariant (st : heap_state) : Prop :=
Lemma heap_range_free_disjoint_siblings h am id al:
heap_state_invariant {| hs_heap := h; hs_allocs := am; |}
heap_range_free h al.(al_start) al.(al_len)
has_disjoint_siblings am id al.
has_disjoint_siblings (<[id:=al]> am) id.
Proof.
move => [/= Ham][Hcell Halh] Hfree.
exists al; split; first by rewrite lookup_insert.
move => id0 al0 Hne /= Hid0 ??? a0 H1 H2.
rewrite lookup_insert_ne // in Hid0.
eapply Halh in H2 => //. rewrite /= (Hfree _ H1) in H2.
by inversion H2.
Qed.
......@@ -770,6 +812,8 @@ Proof.
move: (valid_root_path_root _ _ _ _ Hvrp0 Hid0) => [id_r][al_r]Hid_r.
destruct Hid_r as (Hid_r & Hlast & ? & Halive & ?).
assert (al ## al_r); last by set_solver.
destruct Hdisj as [al' [Heq Hdisj]].
rewrite Hal_a in Heq; move: Heq => [] ?; subst al'.
apply (Hdisj id_r al_r); [|naive_solver..].
move => ?; subst id_r. simplify_eq.
assert (aid ids0) as Hin. { apply last_elem_of_list in Hlast. set_solver. apply _. }
......@@ -883,6 +927,8 @@ Proof.
move => id_c ? Hid_c Hc_alive ? Hc_parent. assert (id_c id) as Hne.
{ move => ?. simplify_eq. rewrite lookup_insert in Hid_c. simplify_eq. }
rewrite lookup_insert_ne // in Hid_c.
destruct Hdisj as [al' [Heq Hdisj]].
rewrite Hid in Heq; move: Heq => [] ?; subst al'.
move: (Hdisj id_c _ Hne Hid_c eq_refl Hc_alive).
rewrite Hc_parent. set_solver.
+ rewrite heap_update_lookup_not_in_range in Ha0; last first.
......
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