rocq/theories/Heap.v
The ghost heap of the program logic (Logic.v): what each piece of memory holds, when a ghost heap of pieces agrees with the memory, and the ownership of a list of pieces in Iris's gen_heap. Taken from the logic spike's IrisHeap.v, which keeps the parts about its own language of whole configurations.
The ghost heap is Iris's gen_heap from Pieces.v's piece to a pval: an object's life with its region, a byte, or a capability in an aux slot. It agrees with a memory when a life token names a live object, and a byte or aux piece names a registered object and, while that object is live, is inside its bounds and holds what the memory holds there, an aux slot up to the collector's rewriting of dead capabilities (agree_piece). Since every piece names a registered object, a fresh base has no pieces yet.
The lemmas say what keeps agreement: a safepoint (agree_piece_safepoint), a store into a live object, which keeps every piece it does not write (frame_ok, cell_store_ok, ptr_store_ok), and an allocation, whose new pieces agree (obj_ps_agree) and which keeps the old ones (agree_piece_allocated). pts ps owns the pieces ps; pts_lookup, pts_update and pts_alloc read, write and allocate them against the authoritative heap. Nothing here is about one runtime or one language.
Pieces and their values
What a piece holds: an object's life with its region, a byte, the capability in an aux slot, or, for a life token, the end of the object's life: a free turns a VLive token into VFreed, since the ghost heap has no way to give a piece up. A name holds the pointer p and the text t of the string the world lends; the memory has nothing to say about it, and the world interpretation ties it to the world. A codec, under a name key, holds the world's multibyte codec, which the memory has nothing to say about either. A stream, under a name key, holds a FILE handle p and, while it is open, its physical pending count and logical FIFO, or nothing once it is closed: libc's state, which only the world interpretation reads. A getopt token, under a name key, holds getopt's optarg and optind, which the world interpretation ties to libc's cells.
| | | VLive | reg : region | |
| | | VByte | v : Z | |
| | | VAux | c : cap | |
| | | VFreed | ||
| | | VName | p : ptr t : listZ | |
| | | VCodec | c : term | |
| | | VStream | p : ptr pending : optionZ × listZ | |
| | | VGetopt | optarg : ptr optind : Z |
Pieces have decidable equality.
Explore proof 1 tactics
Source script
Pieces are countable, by an injection into sums of integers.
Explore proof 2 tactics
Initial goal
refine inj_countable'λp ⇒ match p with PLiveb ⇒ inlb PByteb o ⇒ inrinlb, o PAuxb o ⇒ inrinrinlb, o PNamek ⇒ inrinrinrk end λt ⇒ match t with inlb ⇒ PLiveb inrinlb, o ⇒ PByteb o inrinrinlb, o ⇒ PAuxb o inrinrinrk ⇒ PNamek end _
by intros
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Agreement with the memory
The object of identity b is registered in m, live or freed.
While the object b is live in m, offset o is inside its bounds and P holds.
The piece l with the value v agrees with the memory m: a life token names a live object with its region, or, ended, a registered one; a byte or aux piece names a registered object and, while it is live, is inside its bounds and holds the memory's byte, or the capability up to aux_holds; a name, a codec, a stream or a getopt token agrees with every memory.
Every piece of the ghost heap h agrees with the memory m.
Every piece of the list ps agrees with the memory m.
What owning the pieces ps tells a step about the memory m: they agree with it, live objects do not overlap, and every object fits the address space.
From m to m', every piece whose key is not among ks keeps agreeing: a step that writes only the pieces ks.
The eight byte pieces of the little-endian x at offset o of the object b.
The ghost heap h with the pieces ps written over it, the first of a key winning.
The pieces of a new object of the request q at base: its life, a zero byte and an empty aux slot at each offset.
Facts about agreement
A byte store keeps every region.
Explore proof 1 tactics
Initial goal
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An aux store keeps every region.
Explore proof 1 tactics
A byte store keeps every aux slot.
Explore proof 1 tactics
Initial goal
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An aux store changes only its own slot.
Explore proof 1 tactics
Explore proof 3 tactics
Initial goal
induction ps as | lv ps IH ; cbn ; tauto |
rewrite IH
tauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A piece of a list that agrees agrees.
Explore proof 4 tactics
Initial goal
induction ps as | l′ v′ ps IH ; cbn ; intros H Hin
2 openfocused goal
–by apply not_elem_of_nil in Hin
deferred goal
–apply elem_of_cons in Hin as = → → | Hin ; tauto |
apply IH ; tauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A list agrees if each of its pieces does.
Explore proof 10 tactics
Initial goal
induction ps as | l v ps IH ; cbn ; intros H ; done |
split
2 open–apply H
2 openapply elem_of_cons
2 openby left
–apply IH
intros l′ v′ Hin
apply H
apply elem_of_cons
by right
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A cell agrees when each of its eight bytes does.
Explore proof 8 tactics
Initial goal
unfold cell ; cbn [ map all_agree fst snd ]
split
2 openfocused goal
–intros H i Hi
2 opendeferred goal
assert i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7 as Hc by lia
2 opendeferred goal
destruct Hc as [ ->| [ ->| [ ->| [ ->| [ ->| [ ->| [ ->| -> ] ] ] ] ] ] ] ; tauto
deferred goal
–intros H
repeat split ; apply H ; lia |
exact I
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Byte i of a cell is one of its keys.
Explore proof 6 tactics
Initial goal
intros Hi
apply list_elem_of_In
unfold cell
cbn
assert i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7 as Hc by lia
destruct Hc as [ ->| [ ->| [ ->| [ ->| [ ->| [ ->| [ ->| -> ] ] ] ] ] ] ] ; repeat first left ; reflexivity | right
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A piece of memory that agrees names a registered object.
Explore proof 3 tactics
Initial goal
destruct l as b | b o | b o | k , v as reg | x | c | | q t | cd | sq sp | ga gi ; cbn ; unfold live_at , registered ; try tauto
intros _ E _
congruence
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A live object stays live while regions are kept.
Explore proof 3 tactics
Initial goal
unfold live_at
intros →
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Live objects stay apart while regions are kept.
Explore proof 4 tactics
Initial goal
intros E Hd b1 r1 b2 r2
unfold live_at
rewrite E
apply Hd
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
What a safepoint may do keeps a piece's agreement.
Explore proof 13 tactics
Initial goal
intros Hr Hb Ha
pose proof Hr as Hr′
unfold same_regions in Hr′
destruct l as b | b o | b o | k , v as reg | x | c | | q t | cd | sq sp | ga gi ; cbn ; try tauto ; unfold live_at , registered , in_live ; rewrite ! Hr′ ; try tauto
2 openfocused goal
–rewrite Hb
2 opendeferred goal
tauto
deferred goal
–intros Hreg Hin
split ; exact Hreg |
intros reg E L
destruct Hinreg E L as Ho & He & Hx
split ; exact Ho |
split ; exact He |
exact aux_holds_movesm m′ b + o c Hr Ha Hx
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Two live objects' addresses differ.
Explore proof 2 tactics
Initial goal
intros Hd H H′ Hne Ha Ha′
destruct Hdb reg b′ reg′ H H′ Hne ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An 8-byte store inside the live object b, whose bytes are among the keys ks, keeps every other piece's agreement.
Explore proof 27 tactics
Initial goal
intros Hd Hl Ho He → Hks l v Hn Ha
destruct l as b′ | b′ o′ | b′ o′ | k , v as reg′ | y | c | | q t | cd | sq sp | ga gi ; cbn [ agree_piece ] in Ha |- * ; try contradiction ; try exact I
4 openfocused goal
focused goal
focused goal
–exact live_at_regions_ _ _ _ regions_store_bytes_ _ _ _ Ha
3 opendeferred goal
deferred goal
deferred goal
–unfold registered in *
3 opendeferred goal
deferred goal
rewrite regions_store_bytes
3 opendeferred goal
deferred goal
exact Ha
2 opendeferred goal
deferred goal
–unfold registered , in_live in *
2 opendeferred goal
rewrite ! regions_store_bytes
2 opendeferred goal
destruct Ha as Hr Hin
2 opendeferred goal
split ; exact Hr |
2 opendeferred goal
intros reg′ E L
2 opendeferred goal
destruct Hinreg′ E L as Ho′ & He′ & Hb
2 opendeferred goal
split ; exact Ho′ |
2 opendeferred goal
split ; exact He′ |
2 opendeferred goal
rewrite store_bytes_other ; exact Hb |
2 opendeferred goal
intros Hin′
2 opendeferred goal
destruct Z.eq_decb′ b as [ ->| Hne ]
3 openfocused goal
deferred goal
+apply Hn
3 opendeferred goal
deferred goal
replace o′ with o + o′ − o by lia
3 opendeferred goal
deferred goal
apply Hks
3 opendeferred goal
deferred goal
lia
2 opendeferred goal
deferred goal
+apply live_apartm b reg b′ reg′ b′ + o′ b′ + o′ Hd Hl conjE L ; congruence | lia | lia |
2 opendeferred goal
destruct Hl as El Ll
2 opendeferred goal
destruct Hdb reg b′ reg′ conjEl Ll conjE L ; congruence | | ; lia
deferred goal
–unfold registered , in_live , aux_holds in *
rewrite ! regions_store_bytes aux_store_bytes
exact Ha
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An aux store inside the live object b, whose slot is among the keys ks, keeps every other piece's agreement.
Explore proof 29 tactics
Initial goal
intros Hd Hl Ho He → Hk l v Hn Ha
destruct l as b′ | b′ o′ | b′ o′ | k , v as reg′ | y | c′ | | q t | cd | sq sp | ga gi ; cbn [ agree_piece ] in Ha |- * ; try contradiction ; try exact I
4 openfocused goal
focused goal
–exact live_at_regions_ _ _ _ regions_store_aux_ _ _ Ha
3 opendeferred goal
deferred goal
–unfold registered in *
3 opendeferred goal
rewrite regions_store_aux
3 opendeferred goal
exact Ha
2 opendeferred goal
–unfold registered , in_live in *
2 openrewrite ! regions_store_aux
2 openexact Ha
–unfold registered , in_live , aux_holds in *
rewrite ! regions_store_aux
destruct Ha as Hr Hin
split ; exact Hr |
intros reg′ E L
destruct Hinreg′ E L as Ho′ & He′ & Hx
split ; exact Ho′ |
split ; exact He′ |
rewrite aux_store_aux
assert Hne : b′ + o′ =? b + o = false
2 openfocused goal
{apply Z.eqb_neq
2 opendeferred goal
destruct Z.eq_decb′ b as [ ->| Hne ]
3 openfocused goal
deferred goal
–intros Heq
3 opendeferred goal
deferred goal
apply Hn
3 opendeferred goal
deferred goal
replace o′ with o by lia
3 opendeferred goal
deferred goal
exact Hk
2 opendeferred goal
deferred goal
–destruct Hl as El Ll
2 opendeferred goal
destruct Hdb reg b′ reg′ conjEl Ll conjE L ; congruence | | ; lia
deferred goal
rewrite Hne
exact Hx
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A change that keeps every region and writes bytes and aux slots only inside the live object b, at offsets whose pieces are among the keys ks, keeps every other piece's agreement: a byte or aux slot of another live object lies outside b, since live objects do not overlap.
Explore proof 35 tactics
Initial goal
intros Hr Hd Hl Hb Hx l v Hn Ha
assert Hout : ∀b′ o′ reg′, live_atm b′ reg′ → 0 ≤ o′ → b′ + o′ < r_endreg′ → b ≤ b′ + o′ < r_endreg → b′ = b ∧ b′ + o′ − b = o′
2 openfocused goal
{intros b′ o′ reg′ Hl′ Ho He Hin
2 opendeferred goal
destruct Z.eq_decb′ b as [ ->| Hne ] ; split ; reflexivity | lia |
2 opendeferred goal
exfalso
2 opendeferred goal
exact live_apartm b reg b′ reg′ b′ + o′ b′ + o′ Hd Hl Hl′ not_eq_symHne Hin ltac:lia eq_refl
deferred goal
destruct l as b′ | b′ o′ | b′ o′ | k , v as reg′ | y | c | | q t | cd | sq sp | ga gi ; cbn [ agree_piece ] in Ha |- * ; try contradiction ; try exact I
4 openfocused goal
focused goal
focused goal
–exact live_at_regions_ _ _ _ Hr Ha
3 opendeferred goal
deferred goal
deferred goal
–unfold registered in *
3 opendeferred goal
deferred goal
rewrite Hr
3 opendeferred goal
deferred goal
exact Ha
2 opendeferred goal
deferred goal
–unfold registered , in_live in *
2 opendeferred goal
rewrite Hr
2 opendeferred goal
destruct Ha as Hreg Hin
2 opendeferred goal
split ; exact Hreg |
2 opendeferred goal
intros reg′ E L
2 opendeferred goal
destruct Hinreg′ E L as Ho & He & Hy
2 opendeferred goal
split ; exact Ho |
2 opendeferred goal
split ; exact He |
2 opendeferred goal
rewrite Hb ; exact Hy |
2 opendeferred goal
intros Hin′
2 opendeferred goal
destruct Houtb′ o′ reg′ conjE L Ho He Hin′ as → →
2 opendeferred goal
exact Hn
deferred goal
–unfold registered , in_live , aux_holds in *
rewrite Hr
destruct Ha as Hreg Hin
split ; exact Hreg |
intros reg′ E L
destruct Hinreg′ E L as Ho & He & Hy
split ; exact Ho |
split ; exact He |
rewrite Hx ; exact Hy |
intros Hin′
destruct Houtb′ o′ reg′ conjE L Ho He Hin′ as → →
exact Hn
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Framing composes.
Explore proof 2 tactics
Initial goal
intros H1 H2 l v Hn Ha
apply H2 , H1 ; assumption
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Framing over fewer keys frames over more.
Explore proof 4 tactics
Initial goal
intros Hs H l v Hn Ha
apply H ; | exact Ha
intros Hin
apply Hn , Hs , Hin
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The eight bytes of a cell of the live object b read back as its value modulo 2^64.
Explore proof 12 tactics
Initial goal
intros E L Hc →
rewrite all_agree_cell in Hc
assert Hagree : ∀i, 0 ≤ i < 8 → m_bytesm b + o + i = m_bytesstore_bytesm b + o 8 x b + o + i
2 openfocused goal
{intros i Hi
2 opendeferred goal
rewrite stored_byte ; | exact Hi
2 opendeferred goal
destruct Hci Hi as _ Hin
2 opendeferred goal
destruct Hinreg E L as _ & _ & Hb
2 opendeferred goal
replace b + o + i with b + o + i by lia
2 opendeferred goal
exact Hb
deferred goal
rewrite load_bytes_agreem store_bytesm b + o 8 x b + o 8 ; | lia | exact Hagree
rewrite stored_bytes_value ; | lia
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An 8-byte store at offset o of the live object b: its cell holds the new value, and nothing else changes.
Explore proof 21 tactics
Initial goal
intros Hd Hl Ho He Ha
split
2 openfocused goal
–apply all_agree_cell
2 opendeferred goal
intros i Hi
2 opendeferred goal
cbn [ agree_piece ]
2 opendeferred goal
unfold registered , in_live
2 opendeferred goal
rewrite regions_store_bytes
2 opendeferred goal
destruct Hl as E L
2 opendeferred goal
split ; congruence |
2 opendeferred goal
intros reg′ E′ _
2 opendeferred goal
rewrite E in E′
2 opendeferred goal
injection E′ as ←
2 opendeferred goal
split ; lia |
2 opendeferred goal
split ; lia |
2 opendeferred goal
subst a
2 opendeferred goal
replace b + o + i with b + o + i by lia
2 opendeferred goal
apply stored_byte
2 opendeferred goal
exact Hi
deferred goal
–eapply frame_store_bytes ; exact Hd | exact Hl | exact Ho | exact He | exact Ha |
intros i Hi
apply cell_keys , Hi
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A pointer store (aux then address bytes, at offset 0) into the live object b: its aux slot and first cell hold the pointer, and nothing else changes.
Explore proof 45 tactics
Initial goal
intros Hd Hl He →
set m1 := store_auxm b c
assert Hd1 : live_disjointm1 by apply live_disjoint_regionsm ; reflexivity | exact Hd
assert Hl1 : live_atm1 b reg by apply live_at_regionsm ; reflexivity | exact Hl
destruct cell_store_okm1 b reg 0 b x Hd1 Hl1 ltac:lia ltac:lia ltac:lia as Hc Hf
split ; reflexivity |
split
2 openfocused goal
–apply all_agree_app
2 opendeferred goal
split ; | exact Hc
2 opendeferred goal
cbn [ all_agree fst snd agree_piece ]
2 opendeferred goal
split ; | split ; | exact I
3 openfocused goal
deferred goal
+apply live_at_regionsm ; reflexivity | exact Hl
2 opendeferred goal
deferred goal
+unfold registered , in_live , aux_holds
2 opendeferred goal
rewrite regions_store_bytes aux_store_bytes
2 opendeferred goal
unfold m1
2 opendeferred goal
rewrite regions_store_aux aux_store_aux
2 opendeferred goal
destruct Hl as E L
2 opendeferred goal
split ; congruence |
2 opendeferred goal
intros reg′ E′ _
2 opendeferred goal
rewrite E in E′
2 opendeferred goal
injection E′ as ←
2 opendeferred goal
split ; lia |
2 opendeferred goal
split ; lia |
2 opendeferred goal
left
2 opendeferred goal
replace b + 0 =? b with true ; reflexivity |
2 opendeferred goal
symmetry
2 opendeferred goal
apply Z.eqb_eq
2 opendeferred goal
lia
deferred goal
–apply frame_ok_trans_ m m1
2 openfocused goal
+apply frame_store_aux_ m b reg 0 ; exact Hd | exact Hl | lia | lia | lia |
2 opendeferred goal
rewrite fmap_app
2 opendeferred goal
apply elem_of_app
2 opendeferred goal
left
2 opendeferred goal
cbn
2 opendeferred goal
apply elem_of_cons
2 opendeferred goal
right
2 opendeferred goal
apply elem_of_cons
2 opendeferred goal
left
2 opendeferred goal
reflexivity
deferred goal
+eapply frame_ok_mono ; | exact Hf
intros l Hin
rewrite fmap_app
apply elem_of_app
right
exact Hin
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A key of overwrite ps h comes from ps, or from h when ps does not name it.
Explore proof 19 tactics
Initial goal
induction ps as | l′ v′ ps IH ; cbn
2 open–intros H
2 openright
2 opensplit ; apply not_elem_of_nil | exact H
–rewrite lookup_insert
destruct decidel′ = l as [ ->| Hne ]
2 open+intros = →
2 openleft
2 openapply elem_of_cons
2 openby left
+intros H
destruct IHH as Hin | Hn Hh
2 open∗left
2 openapply elem_of_cons
2 openby right
∗right
split ; | exact Hh
apply not_elem_of_cons
split ; congruence | exact Hn
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Every piece of a new object at base names base.
Explore proof 4 tactics
Initial goal
unfold obj_ps
intros Hin
apply elem_of_cons in Hin as = → → | Hin ; reflexivity |
apply elem_of_app in Hin as Hin | Hin ; apply list_elem_of_fmap in Hin as i & = → → & _ ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A new object's pieces are pieces of memory.
Explore proof 4 tactics
Initial goal
unfold obj_ps
intros Hin
apply elem_of_cons in Hin as = → → | Hin ; exact I |
apply elem_of_app in Hin as Hin | Hin ; apply list_elem_of_fmap in Hin as i & = → → & _ ; exact I
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The keys of a new object's pieces are distinct.
Explore proof 22 tactics
Initial goal
unfold obj_ps
pose proof NoDup_seqZ0 req_extentq as Hl
revert Hl
generalize seqZ0 req_extentq as ns
intros ns Hl
rewrite fmap_cons fmap_app -! list_fmap_compose
apply NoDup_cons
split
2 open–rewrite elem_of_app ! list_elem_of_fmap
2 openintros i & Hi & _ | i & Hi & _ ; discriminate Hi
–apply NoDup_app
split ; | split
3 openfocused goal
+apply NoDup_fmap_2_strong ; | exact Hl
3 opendeferred goal
intros i j _ _ Hij
3 opendeferred goal
by injection Hij
2 opendeferred goal
+intros l
2 openrewrite ! list_elem_of_fmap
2 openintros i & → & _ j & Hj & _
2 opendiscriminate Hj
+apply NoDup_fmap_2_strong ; | exact Hl
intros i j _ _ Hij
by injection Hij
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Each piece of a new object at a fresh base agrees with the memory after the allocation.
Explore proof 12 tactics
Initial goal
intros Hf Hq Hin
destruct Hf as _ & _ & _ & _ & _ & Hz
unfold obj_ps in Hin
apply elem_of_cons in Hin as = → → | Hin
2 openfocused goal
–cbn [ agree_piece ]
2 opendeferred goal
unfold live_at
2 opendeferred goal
rewrite object_region_allocated Z.eqb_refl
2 opendeferred goal
split ; reflexivity
deferred goal
–apply elem_of_app in Hin as Hin | Hin ; apply list_elem_of_fmap in Hin as i & = → → & Hi ; apply elem_of_seqZ in Hi ; cbn [ agree_piece ] ; unfold registered , in_live ; rewrite object_region_allocated Z.eqb_refl ; split ; discriminate | ; intros reg′ = ← _ ; cbn [ r_end ] ; split ; lia | ; split ; lia | ; destruct Hzbase + i ltac:lia as Hb Ha
2 openfocused goal
+exact Hb
deferred goal
+left
exact Ha
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A freed capability stays freed after an allocation at a new base.
Explore proof 6 tactics
Initial goal
intros Hn b & reg & Hc & E & L
exists b, reg
split ; exact Hc |
split ; | exact L
rewrite object_region_allocated
destruct Z.eqb_specbase b as [ <-| ] ; congruence | exact E
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A capability that traps as a freed one still does after an allocation at a new base.
Explore proof 4 tactics
Initial goal
intros Hn H a size r align Hs
rewrite <- Ha size r align Hs
unfold cap_access_res
destruct c as | b | b | f | n ; try reflexivity ; rewrite object_region_allocated ; destruct Z.eqb_specbase b as [ <-| ] ; | reflexivity ; specialize Ha size r align Hs ; unfold cap_access_res in H ; rewrite Hn in H ; discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An allocation at a new base keeps every old piece's agreement.
Explore proof 23 tactics
Initial goal
intros Hn
assert Ho : ∀b, object_regionb m_regionsm ≠ None → object_regionb m_regionsallocatedm q base = object_regionb m_regionsm
2 openfocused goal
{intros b Hb
2 opendeferred goal
rewrite object_region_allocated
2 opendeferred goal
destruct Z.eqb_specbase b as [ <-| ] ; contradiction | reflexivity
deferred goal
destruct l as b | b o | b o | k , v as reg | x | c | | p t | cd | sq sp | ga gi ; cbn [ agree_piece ] ; try tauto ; unfold live_at , registered , in_live
4 openfocused goal
focused goal
focused goal
–intros E L
4 opendeferred goal
deferred goal
deferred goal
rewrite Ho ; | congruence
4 opendeferred goal
deferred goal
deferred goal
auto
3 opendeferred goal
deferred goal
deferred goal
–intros Hr
3 opendeferred goal
deferred goal
rewrite Ho ; exact Hr
2 opendeferred goal
deferred goal
–intros Hr Hin
2 opendeferred goal
rewrite Ho ; | exact Hr
2 opendeferred goal
split ; exact Hr | exact Hin
deferred goal
–intros Hr Hin
rewrite Ho ; | exact Hr
split ; exact Hr |
intros reg E L
destruct Hinreg E L as Ho′ & He & Hx
split ; exact Ho′ |
split ; exact He |
destruct Hx as Hx | Hf Ht ; left ; exact Hx | right
split ; exact freed_in_allocated_ _ _ _ Hn Hf | exact traps_as_freed_allocated_ _ _ _ Hn Ht
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Owning pieces
Ownership of each piece of the list ps with its value.
Owning two lists of pieces is owning their concatenation.
Explore proof 1 tactics
Owned pieces are in the authoritative heap.
Explore proof 11 tactics
Initial goal
induction ps as | l v ps IH ; iIntros Hh Hps
2 open–iPureIntro
2 openintros l v Hin
2 openby apply not_elem_of_nil in Hin
–rewrite / pts /=
iDestruct Hps as [Hl Hps]
iDestruct gen_heap_valid with Hh Hl as %Hl
iDestruct IH with Hh Hps as %Hps
iPureIntro
intros l′ v′ Hin
apply elem_of_cons in Hin as = → → | Hin ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Owned pieces can be given new values with the same keys.
Explore proof 15 tactics
Initial goal
revert ps′
induction ps as | l v ps IH ; intros | l′ v′ ps′ Hk ; try discriminate Hk
2 openfocused goal
–iIntros Hh _
2 opendeferred goal
iModIntro
2 opendeferred goal
iFrame
2 opendeferred goal
by rewrite / pts
deferred goal
–cbn in Hk
injection Hk as → Hk
iIntros Hh Hps
rewrite / pts /=
iDestruct Hps as [Hl Hps]
iMod IHps′ Hk with Hh Hps as [Hh Hps]
iMod gen_heap_update with Hh Hl as [Hh Hl]
2 openiModIntro
2 openiFrame
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Pieces with distinct keys, none in the heap, can be allocated.
Explore proof 25 tactics
Initial goal
induction ps as | l v ps IH ; intros Hnd Hfr
2 openfocused goal
–iIntros Hh
2 opendeferred goal
iModIntro
2 opendeferred goal
iFrame
2 opendeferred goal
by rewrite / pts
deferred goal
–cbn in Hnd
apply NoDup_cons in Hnd as Hn Hnd
iIntros Hh
iMod IHHnd with Hh as [Hh Hps]
2 openfocused goal
{intros l′ v′ Hin
2 opendeferred goal
apply Hfrl′ v′
2 opendeferred goal
apply elem_of_cons
2 opendeferred goal
by right
deferred goal
iMod gen_heap_alloc_ l v with Hh as (Hh & Hl & _)
2 openfocused goal
{destruct overwriteps h !! l as v′ | eqn: E ; | reflexivity
2 opendeferred goal
destruct lookup_overwrite_ _ _ _ E as Hin | _ Hh
3 openfocused goal
deferred goal
–exfalso
3 opendeferred goal
deferred goal
apply Hn
3 opendeferred goal
deferred goal
exact list_elem_of_fmap_2fst _ l, v′ Hin
2 opendeferred goal
deferred goal
–rewrite Hfrl v in Hh ; discriminate |
2 opendeferred goal
apply elem_of_cons
2 opendeferred goal
by left
deferred goal
iModIntro
rewrite / pts /=
iFrame
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.