Fil-C on Nix

Filnix wiki

the formal campaign

rocq/theories/Pieces.v

The resource model of the program logic (Logic.v, docs/logic.md), shared with the logic spikes: the pieces of memory an assertion may own, keyed by identity, and the facts about the whole memory that make owning them mean something.

A piece is an object's life (PLive), or one byte (PByte) or aux slot (PAux) at an offset in it. Pieces are keyed by identity, not address, because the model's fresh lets a new object take the addresses of a freed one: an address may belong to two identities in turn, an identity never to two objects. One more kind of piece is no memory: the ghost name of a string the world lends (PName), such as a locale's name, which the world interpretation ties to the world so that a proof can remember, across steps, which string a library call returned.

Two facts about the whole memory are the logics' state interpretation. Live objects do not overlap (live_disjoint), which a run keeps, so a store into one object leaves every other live object's bytes alone. And a safepoint changes no region and no byte, and changes an aux slot only where the capability stored there names a freed object (safepoint_shape, from Runtime.v's collector_live, non_moving and aux_round_trip), so no safepoint frees a live object (keeps_live, once a premise, now a lemma).

From Stdlib Require Import String ZArith List Bool Lia
From Nanofil Require Import Term Syntax Values Memory Runtime ExternalCalls
Import ListNotations
Open Scope Z_scope

Pieces

A piece of memory an assertion may own: the life of the object of identity b, or the byte or aux slot at offset o in it; or the ghost name of the string the world lends under the key k, such as the name of locale category k, which is no memory at all.

37Inductive piece: Type ≔
|PLive
b : Z
|PByte
b o : Z
|PAux
b o : Z
|PName
k : Z

The identity a piece belongs to; a name, which belongs to no object, says 0, and facts about objects skip it (mem_piece).

45Definition piece_idp : piece : Z ≔
match p with
PLiveb | PByteb _ | PAuxb _
⇒
b
PName_
⇒
0

The piece p is a piece of memory, not a name.

49Definition mem_piecep : piece : Prop ≔
match p with
PName_
⇒
False
_
⇒
True

The null pointer, a constant 0 at class p.

53Definition null: ptr ≔
mkPtr0 CNone

The whole memory

The object of identity b is live in m, with the region reg.

58Definition live_atm : mem b : Z reg : region : Prop ≔
object_regionb m_regionsm = Somereg ∧ r_lifereg = Live

The live objects of m do not overlap.

62Definition live_disjointm : mem : Prop ≔
∀b1 r1 b2 r2, live_atm b1 r1 → live_atm b2 r2 → b1 ≠ b2 → r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

m and m' have the same objects, each with the same region.

67Definition same_regionsm m′ : mem : Prop ≔
∀b, object_regionb m_regionsm′ = object_regionb m_regionsm

From m to m', every aux slot is kept, or held a capability of an object freed in m' and now holds one that traps as a freed one does: what the collector may do at a safepoint (aux_round_trip).

73Definition aux_movesm m′ : mem : Prop ≔
∀a, m_auxm′ a = m_auxm a ∨ freed_inm_regionsm′ m_auxm a ∧ traps_as_freedm_regionsm′ m_auxm′ a

The aux slot at a holds the capability c, or c names a freed object and the slot holds one that traps as a freed one does: a stored capability is known up to the collector's rewriting of dead ones (aux_moves). For a capability whose object is live, or no object's, this is equality (aux_holds_live).

82Definition aux_holdsm : mem a : Z c : cap : Prop ≔
m_auxm a = c ∨ freed_inm_regionsm c ∧ traps_as_freedm_regionsm m_auxm a

A freed object's capability stays freed while objects keep their regions.

87Lemma freed_in_same
∀ m m′ c
same_regionsm m′
freed_inm_regionsm c
freed_inm_regionsm′ c
Explore proof 4 tactics

Initial goal

⊢
∀m m′ : mem c : cap, same_regionsm m′ → freed_inm_regionsm c → freed_inm_regionsm′ c

intros m m′ c Hr b & reg & Hc & E & L

m, m′ :
mem
c :
cap
Hr :
same_regionsm m′
b :
Z
reg :
region
Hc :
c = Objb ∨ c = Rob
E :
object_regionb m_regionsm = Somereg
L :
r_lifereg = Freed
⊢
freed_inm_regionsm′ c

exists b, reg

m, m′ :
mem
c :
cap
Hr :
same_regionsm m′
b :
Z
reg :
region
Hc :
c = Objb ∨ c = Rob
E :
object_regionb m_regionsm = Somereg
L :
r_lifereg = Freed
⊢
c = Objb ∨ c = Rob ∧ object_regionb m_regionsm′ = Somereg ∧ r_lifereg = Freed

rewrite Hr

m, m′ :
mem
c :
cap
Hr :
same_regionsm m′
b :
Z
reg :
region
Hc :
c = Objb ∨ c = Rob
E :
object_regionb m_regionsm = Somereg
L :
r_lifereg = Freed
⊢
c = Objb ∨ c = Rob ∧ object_regionb m_regionsm = Somereg ∧ r_lifereg = Freed

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m m′ c Hr b & reg & Hc & E & L
exists b, reg
rewrite Hr
auto

A capability that traps as a freed one keeps doing so while objects keep their regions.

95Lemma traps_as_freed_same
∀ m m′ c
same_regionsm m′
traps_as_freedm_regionsm c
traps_as_freedm_regionsm′ c
Explore proof 4 tactics

Initial goal

⊢
∀m m′ : mem c : cap, same_regionsm m′ → traps_as_freedm_regionsm c → traps_as_freedm_regionsm′ c

intros m m′ c Hr H a size r align Hs

m, m′ :
mem
c :
cap
Hr :
same_regionsm m′
H :
traps_as_freedm_regionsm c
a, size :
Z
r :
rights
align :
Z
Hs :
0 < size
⊢
cap_access_resc m_regionsm′ a size r align = SomeRTrapOutOfBounds

rewrite <- Ha size r align Hs

m, m′ :
mem
c :
cap
Hr :
same_regionsm m′
H :
traps_as_freedm_regionsm c
a, size :
Z
r :
rights
align :
Z
Hs :
0 < size
⊢
cap_access_resc m_regionsm′ a size r align = cap_access_resc m_regionsm a size r align

unfold cap_access_res

m, m′ :
mem
c :
cap
Hr :
same_regionsm m′
H :
traps_as_freedm_regionsm c
a, size :
Z
r :
rights
align :
Z
Hs :
0 < size
⊢
match c with
CNone
⇒
SomeRTrapNullCapability
Objbase
⇒
match object_regionbase m_regionsm′ with
Somereg
⇒
Some
base ≤? a && a + size ≤? r_endreg
→
aligned_resa align
else
RTrapOutOfBounds
None
⇒
None
Robase
⇒
match object_regionbase m_regionsm′ with
Somereg
⇒
Some
base ≤? a && a + size ≤? r_endreg
→
readonly_access_resr a align
else
RTrapOutOfBounds
None
⇒
None
Fn_
⇒
SomeRTrapOutOfBounds
External_
⇒
None
=
match c with
CNone
⇒
SomeRTrapNullCapability
Objbase
⇒
match object_regionbase m_regionsm with
Somereg
⇒
Some
base ≤? a && a + size ≤? r_endreg
→
aligned_resa align
else
RTrapOutOfBounds
None
⇒
None
Robase
⇒
match object_regionbase m_regionsm with
Somereg
⇒
Some
base ≤? a && a + size ≤? r_endreg
→
readonly_access_resr a align
else
RTrapOutOfBounds
None
⇒
None
Fn_
⇒
SomeRTrapOutOfBounds
External_
⇒
None

destruct c ; try reflexivity ; rewrite Hr ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m m′ c Hr H a size r align Hs
rewrite <- Ha size r align Hs
unfold cap_access_res
destruct c ; try reflexivity ; rewrite Hr ; reflexivity

What an aux slot is known to hold survives what a safepoint may do to it (aux_moves) while objects keep their regions.

104Lemma aux_holds_moves
∀ m m′ a c
same_regionsm m′
aux_movesm m′
aux_holdsm a c
aux_holdsm′ a c
Explore proof 12 tactics

Initial goal

⊢
∀m m′ : mem a : Z c : cap, same_regionsm m′ → aux_movesm m′ → aux_holdsm a c → aux_holdsm′ a c

intros m m′ a c Hr Hm E | Hf & Ht ; destruct Hma as E′ | Hf′ & Ht′

4 open

m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
E :
m_auxm a = c
E′ :
m_auxm′ a = m_auxm a
⊢
aux_holdsm′ a c
focused goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
E :
m_auxm a = c
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
aux_holdsm′ a c
focused goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
E′ :
m_auxm′ a = m_auxm a
⊢
aux_holdsm′ a c
focused goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
aux_holdsm′ a c

–left

4 open

m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
E :
m_auxm a = c
E′ :
m_auxm′ a = m_auxm a
⊢
m_auxm′ a = c
deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
E :
m_auxm a = c
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
aux_holdsm′ a c
deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
E′ :
m_auxm′ a = m_auxm a
⊢
aux_holdsm′ a c
deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
aux_holdsm′ a c

rewrite E′

4 open

m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
E :
m_auxm a = c
E′ :
m_auxm′ a = m_auxm a
⊢
m_auxm a = c
deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
E :
m_auxm a = c
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
aux_holdsm′ a c
deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
E′ :
m_auxm′ a = m_auxm a
⊢
aux_holdsm′ a c
deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
aux_holdsm′ a c

exact E

3 open

deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
E :
m_auxm a = c
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
aux_holdsm′ a c
deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
E′ :
m_auxm′ a = m_auxm a
⊢
aux_holdsm′ a c
deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
aux_holdsm′ a c

–right

3 open

m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
E :
m_auxm a = c
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
freed_inm_regionsm′ c ∧ traps_as_freedm_regionsm′ m_auxm′ a
deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
E′ :
m_auxm′ a = m_auxm a
⊢
aux_holdsm′ a c
deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
aux_holdsm′ a c

subst c

3 open

m, m′ :
mem
a :
Z
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
freed_inm_regionsm′ m_auxm a ∧ traps_as_freedm_regionsm′ m_auxm′ a
deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
E′ :
m_auxm′ a = m_auxm a
⊢
aux_holdsm′ a c
deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
aux_holdsm′ a c

split ; exact Hf′ | exact Ht′

2 open

deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
E′ :
m_auxm′ a = m_auxm a
⊢
aux_holdsm′ a c
deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
aux_holdsm′ a c

–right

2 open

m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
E′ :
m_auxm′ a = m_auxm a
⊢
freed_inm_regionsm′ c ∧ traps_as_freedm_regionsm′ m_auxm′ a
deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
aux_holdsm′ a c

rewrite E′

2 open

m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
E′ :
m_auxm′ a = m_auxm a
⊢
freed_inm_regionsm′ c ∧ traps_as_freedm_regionsm′ m_auxm a
deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
aux_holdsm′ a c

split ; exact freed_in_same_ _ _ Hr Hf | exact traps_as_freed_same_ _ _ Hr Ht

deferred goal
m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
aux_holdsm′ a c

–right

m, m′ :
mem
a :
Z
c :
cap
Hr :
same_regionsm m′
Hm :
aux_movesm m′
Hf :
freed_inm_regionsm c
Ht :
traps_as_freedm_regionsm m_auxm a
Hf′ :
freed_inm_regionsm′ m_auxm a
Ht′ :
traps_as_freedm_regionsm′ m_auxm′ a
⊢
freed_inm_regionsm′ c ∧ traps_as_freedm_regionsm′ m_auxm′ a

split ; exact freed_in_same_ _ _ Hr Hf | exact Ht′

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m m′ a c Hr Hm E | Hf & Ht ; destruct Hma as E′ | Hf′ & Ht′
–left
rewrite E′
exact E
–right
subst c
split ; exact Hf′ | exact Ht′
–right
rewrite E′
split ; exact freed_in_same_ _ _ Hr Hf | exact traps_as_freed_same_ _ _ Hr Ht
–right
split ; exact freed_in_same_ _ _ Hr Hf | exact Ht′

For no object's capability, or a live object's, aux_holds is equality.

116Lemma aux_holds_live
∀ m a c
aux_holdsm a c
c = CNone ∨ ∃b reg, c = Objb ∧ live_atm b reg
m_auxm a = c
Explore proof 5 tactics

Initial goal

⊢
∀m : mem a : Z c : cap, aux_holdsm a c → c = CNone ∨ ∃b : Z reg : region, c = Objb ∧ live_atm b reg → m_auxm a = c

intros m a c E | b & reg & Hc & E & L & _ Hc′ ; exact E |

m :
mem
a :
Z
c :
cap
b :
Z
reg :
region
Hc :
c = Objb ∨ c = Rob
E :
object_regionb m_regionsm = Somereg
L :
r_lifereg = Freed
Hc′ :
c = CNone ∨ ∃b : Z reg : region, c = Objb ∧ live_atm b reg
⊢
m_auxm a = c

destruct Hc′ as [ ->| ( b′ & reg′ & -> & E′ & L′ ) ] ; destruct Hc as [ ?|? ] ; discriminate |

m :
mem
a, b :
Z
reg :
region
b′ :
Z
Hc :
Objb′ = Objb ∨ Objb′ = Rob
E :
object_regionb m_regionsm = Somereg
L :
r_lifereg = Freed
reg′ :
region
E′ :
object_regionb′ m_regionsm = Somereg′
L′ :
r_lifereg′ = Live
⊢
m_auxm a = Objb′

destruct Hc as Hc | Hc ; | discriminate

m :
mem
a, b :
Z
reg :
region
b′ :
Z
Hc :
Objb′ = Objb
E :
object_regionb m_regionsm = Somereg
L :
r_lifereg = Freed
reg′ :
region
E′ :
object_regionb′ m_regionsm = Somereg′
L′ :
r_lifereg′ = Live
⊢
m_auxm a = Objb′

injection Hc as ←

m :
mem
a :
Z
reg :
region
b′ :
Z
E :
object_regionb′ m_regionsm = Somereg
L :
r_lifereg = Freed
reg′ :
region
E′ :
object_regionb′ m_regionsm = Somereg′
L′ :
r_lifereg′ = Live
⊢
m_auxm a = Objb′

congruence

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m a c E | b & reg & Hc & E & L & _ Hc′ ; exact E |
destruct Hc′ as [ ->| ( b′ & reg′ & -> & E′ & L′ ) ] ; destruct Hc as [ ?|? ] ; discriminate |
destruct Hc as Hc | Hc ; | discriminate
injection Hc as ←
congruence

A capability whose object is not freed is exactly what the slot holds: the collector rewrites only freed objects' capabilities.

126Lemma aux_holds_kept
∀ m a c
aux_holdsm a c
¬freed_inm_regionsm c
m_auxm a = c
Explore proof 1 tactics

Initial goal

⊢
∀m : mem a : Z c : cap, aux_holdsm a c → ¬freed_inm_regionsm c → m_auxm a = c

intros m a c E | Hf & _ Hn ; exact E | contradiction

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m a c E | Hf & _ Hn ; exact E | contradiction

Bytes

A store of size bytes at a leaves every other byte.

133Lemma store_bytes_other
∀ m a size x a′
¬a ≤ a′ < a + size
m_bytesstore_bytesm a size x a′ = m_bytesm a′
Explore proof 7 tactics

Initial goal

⊢
∀m : mem a size x a′ : Z, ¬a ≤ a′ < a + size → m_bytesstore_bytesm a size x a′ = m_bytesm a′

intros m a size x a′ H

m :
mem
a, size, x, a′ :
Z
H :
¬a ≤ a′ < a + size
⊢
m_bytesstore_bytesm a size x a′ = m_bytesm a′

unfold store_bytes ; cbn [ m_bytes ]

m :
mem
a, size, x, a′ :
Z
H :
¬a ≤ a′ < a + size
⊢
a ≤? a′ && a′ <? a + size
→
byte_ofx a′ − a
else
m_bytesm a′
=
m_bytesm a′

destruct a ≤? a′ && a′ <? a + size eqn: E ; | reflexivity

m :
mem
a, size, x, a′ :
Z
H :
¬a ≤ a′ < a + size
E :
a ≤? a′ && a′ <? a + size = true
⊢
byte_ofx a′ − a = m_bytesm a′

apply andb_true_iff in E as E1 E2

m :
mem
a, size, x, a′ :
Z
H :
¬a ≤ a′ < a + size
E1 :
a ≤? a′ = true
E2 :
a′ <? a + size = true
⊢
byte_ofx a′ − a = m_bytesm a′

apply Z.leb_le in E1

m :
mem
a, size, x, a′ :
Z
H :
¬a ≤ a′ < a + size
E1 :
a ≤ a′
E2 :
a′ <? a + size = true
⊢
byte_ofx a′ − a = m_bytesm a′

apply Z.ltb_lt in E2

m :
mem
a, size, x, a′ :
Z
H :
¬a ≤ a′ < a + size
E1 :
a ≤ a′
E2 :
a′ < a + size
⊢
byte_ofx a′ − a = m_bytesm a′

lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m a size x a′ H
unfold store_bytes ; cbn [ m_bytes ]
destruct a ≤? a′ && a′ <? a + size eqn: E ; | reflexivity
apply andb_true_iff in E as E1 E2
apply Z.leb_le in E1
apply Z.ltb_lt in E2
lia

An 8-byte store of an unsigned 64-bit v reads back as v (ExternalCalls.v's stored_bytes_value).

143Lemma load_store_bytes
∀ m a v
0 ≤ v < 2 ^ 64
load_bytesstore_bytesm a 8 v a 8 = v
Explore proof 5 tactics

Initial goal

⊢
∀m : mem a v : Z, 0 ≤ v < 2 ^ 64 → load_bytesstore_bytesm a 8 v a 8 = v

intros m a v Hv

m :
mem
a, v :
Z
Hv :
0 ≤ v < 2 ^ 64
⊢
load_bytesstore_bytesm a 8 v a 8 = v

rewrite stored_bytes_value by lia

m :
mem
a, v :
Z
Hv :
0 ≤ v < 2 ^ 64
⊢
v mod 256 ^ 8 = v

change 256 ^ 8 with 2 ^ 64

m :
mem
a, v :
Z
Hv :
0 ≤ v < 2 ^ 64
⊢
v mod 2 ^ 64 = v

apply Z.mod_small

m :
mem
a, v :
Z
Hv :
0 ≤ v < 2 ^ 64
⊢
0 ≤ v < 2 ^ 64

exact Hv

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m a v Hv
rewrite stored_bytes_value by lia
change 256 ^ 8 with 2 ^ 64
apply Z.mod_small
exact Hv

Neither a byte store nor an aux store changes an object.

151Lemma store_regions
∀ m a size x c
m_regionsstore_bytesm a size x = m_regionsm ∧ m_regionsstore_auxm a c = m_regionsm
Explore proof 1 tactics

Initial goal

⊢
∀m : mem a size x : Z c : cap, m_regionsstore_bytesm a size x = m_regionsm ∧ m_regionsstore_auxm a c = m_regionsm

split ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
split ; reflexivity

Allocation

After allocating q at base, the object of identity base is the new one, and every other identity finds what it found before.

159Lemma object_region_allocated
∀ m q base b
object_regionb m_regionsallocatedm q base
=
Z.eqbbase b
→
SomemkRegionbase base + req_extentq req_kindq Live
else
object_regionb m_regionsm
Explore proof 2 tactics

Initial goal

⊢
∀ m : mem q : alloc_req base b : Z  ,
object_regionb m_regionsallocatedm q base
=
base =? b
→
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live
else
object_regionb m_regionsm

intros m q base b

m :
mem
q :
alloc_req
base, b :
Z
⊢
object_regionb m_regionsallocatedm q base
=
base =? b
→
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live
else
object_regionb m_regionsm

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m q base b
reflexivity

Allocating at a fresh base keeps live objects apart.

166Lemma live_disjoint_allocated
∀ m q base
live_disjointm
freshm q base
0 ≤ req_extentq
live_disjointallocatedm q base
Explore proof 22 tactics

Initial goal

⊢
∀m : mem q : alloc_req base : Z, live_disjointm → freshm q base → 0 ≤ req_extentq → live_disjointallocatedm q base

intros m q base Hd Hf Hq b1 r1 b2 r2 E1 L1 E2 L2 Hne

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hf :
freshm q base
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsallocatedm q base = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsallocatedm q base = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

destruct Hf as _ & _ & _ & _ & Hover & _

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsallocatedm q base = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsallocatedm q base = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

rewrite object_region_allocated in E1 , E2

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
base =? b1
→
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live
else
object_regionb1 m_regionsm
=
Somer1
L1 :
r_lifer1 = Live
E2 :
base =? b2
→
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live
else
object_regionb2 m_regionsm
=
Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

destruct Z.eqb_specbase b1 as [ <-| N1 ] ; destruct Z.eqb_specbase b2 as [ <-| N2 ]

4 open

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
r1, r2 :
region
E1 :
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Somer1
L1 :
r_lifer1 = Live
E2 :
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Somer2
L2 :
r_lifer2 = Live
Hne :
base ≠ base
⊢
r_endr1 ≤ base ∨ r_endr2 ≤ base
focused goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
r1 :
region
b2 :
Z
r2 :
region
E1 :
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne, N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ base
focused goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1, r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
⊢
r_endr1 ≤ base ∨ r_endr2 ≤ b1
focused goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

–congruence

3 open

deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
r1 :
region
b2 :
Z
r2 :
region
E1 :
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne, N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ base
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1, r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
⊢
r_endr1 ≤ base ∨ r_endr2 ≤ b1
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

–injection E1 as ←

3 open

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b2 :
Z
r2 :
region
L1 :
r_lifer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne, N2 :
base ≠ b2
⊢
r_endr_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live ≤ b2 ∨ r_endr2 ≤ base
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1, r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
⊢
r_endr1 ≤ base ∨ r_endr2 ≤ b1
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

cbn [ r_end ]

3 open

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b2 :
Z
r2 :
region
L1 :
r_lifer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne, N2 :
base ≠ b2
⊢
base + req_extentq ≤ b2 ∨ r_endr2 ≤ base
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1, r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
⊢
r_endr1 ≤ base ∨ r_endr2 ≤ b1
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

specialize Hoverb2 r2 E2

3 open

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
b2 :
Z
r2 :
region
Hover :
¬base < r_endr2 ∧ b2 < base + req_extentq
Hq :
0 ≤ req_extentq
L1 :
r_lifer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne, N2 :
base ≠ b2
⊢
base + req_extentq ≤ b2 ∨ r_endr2 ≤ base
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1, r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
⊢
r_endr1 ≤ base ∨ r_endr2 ≤ b1
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

destruct Z_le_gt_decbase + req_extentq b2 ; left ; lia |

3 open

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
b2 :
Z
r2 :
region
Hover :
¬base < r_endr2 ∧ b2 < base + req_extentq
Hq :
0 ≤ req_extentq
L1 :
r_lifer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne, N2 :
base ≠ b2
g :
base + req_extentq > b2
⊢
base + req_extentq ≤ b2 ∨ r_endr2 ≤ base
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1, r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
⊢
r_endr1 ≤ base ∨ r_endr2 ≤ b1
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

destruct Z_le_gt_decr_endr2 base ; right ; lia |

3 open

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
b2 :
Z
r2 :
region
Hover :
¬base < r_endr2 ∧ b2 < base + req_extentq
Hq :
0 ≤ req_extentq
L1 :
r_lifer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne, N2 :
base ≠ b2
g :
base + req_extentq > b2
g0 :
r_endr2 > base
⊢
base + req_extentq ≤ b2 ∨ r_endr2 ≤ base
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1, r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
⊢
r_endr1 ≤ base ∨ r_endr2 ≤ b1
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

exfalso

3 open

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
b2 :
Z
r2 :
region
Hover :
¬base < r_endr2 ∧ b2 < base + req_extentq
Hq :
0 ≤ req_extentq
L1 :
r_lifer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne, N2 :
base ≠ b2
g :
base + req_extentq > b2
g0 :
r_endr2 > base
⊢
False
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1, r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
⊢
r_endr1 ≤ base ∨ r_endr2 ≤ b1
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

apply Hover

3 open

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
b2 :
Z
r2 :
region
Hover :
¬base < r_endr2 ∧ b2 < base + req_extentq
Hq :
0 ≤ req_extentq
L1 :
r_lifer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne, N2 :
base ≠ b2
g :
base + req_extentq > b2
g0 :
r_endr2 > base
⊢
base < r_endr2 ∧ b2 < base + req_extentq
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1, r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
⊢
r_endr1 ≤ base ∨ r_endr2 ≤ b1
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

lia

2 open

deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1, r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
⊢
r_endr1 ≤ base ∨ r_endr2 ≤ b1
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

–injection E2 as ←

2 open

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
L2 :
r_lifer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
⊢
r_endr1 ≤ base ∨ r_endr_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live ≤ b1
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

cbn [ r_end ]

2 open

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
L2 :
r_lifer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
⊢
r_endr1 ≤ base ∨ base + req_extentq ≤ b1
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

specialize Hoverb1 r1 E1

2 open

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
b1 :
Z
r1 :
region
Hover :
¬base < r_endr1 ∧ b1 < base + req_extentq
Hq :
0 ≤ req_extentq
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
L2 :
r_lifer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
⊢
r_endr1 ≤ base ∨ base + req_extentq ≤ b1
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

destruct Z_le_gt_decr_endr1 base ; left ; lia |

2 open

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
b1 :
Z
r1 :
region
Hover :
¬base < r_endr1 ∧ b1 < base + req_extentq
Hq :
0 ≤ req_extentq
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
L2 :
r_lifer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
g :
r_endr1 > base
⊢
r_endr1 ≤ base ∨ base + req_extentq ≤ b1
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

destruct Z_le_gt_decbase + req_extentq b1 ; right ; lia |

2 open

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
b1 :
Z
r1 :
region
Hover :
¬base < r_endr1 ∧ b1 < base + req_extentq
Hq :
0 ≤ req_extentq
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
L2 :
r_lifer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
g :
r_endr1 > base
g0 :
base + req_extentq > b1
⊢
r_endr1 ≤ base ∨ base + req_extentq ≤ b1
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

exfalso

2 open

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
b1 :
Z
r1 :
region
Hover :
¬base < r_endr1 ∧ b1 < base + req_extentq
Hq :
0 ≤ req_extentq
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
L2 :
r_lifer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
g :
r_endr1 > base
g0 :
base + req_extentq > b1
⊢
False
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

apply Hover

2 open

m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
b1 :
Z
r1 :
region
Hover :
¬base < r_endr1 ∧ b1 < base + req_extentq
Hq :
0 ≤ req_extentq
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
L2 :
r_lifer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Live
Hne :
b1 ≠ base
N1 :
base ≠ b1
g :
r_endr1 > base
g0 :
base + req_extentq > b1
⊢
base < r_endr1 ∧ b1 < base + req_extentq
deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

lia

deferred goal
m :
mem
q :
alloc_req
base :
Z
Hd :
live_disjointm
Hover :
∀b : Z reg : region, object_regionb m_regionsm = Somereg → ¬base < r_endreg ∧ b < base + req_extentq
Hq :
0 ≤ req_extentq
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hne :
b1 ≠ b2
N1 :
base ≠ b1
N2 :
base ≠ b2
⊢
r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

–exact Hdb1 r1 b2 r2 conjE1 L1 conjE2 L2 Hne

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m q base Hd Hf Hq b1 r1 b2 r2 E1 L1 E2 L2 Hne
destruct Hf as _ & _ & _ & _ & Hover & _
rewrite object_region_allocated in E1 , E2
destruct Z.eqb_specbase b1 as [ <-| N1 ] ; destruct Z.eqb_specbase b2 as [ <-| N2 ]
–congruence
–injection E1 as ←
cbn [ r_end ]
specialize Hoverb2 r2 E2
destruct Z_le_gt_decbase + req_extentq b2 ; left ; lia |
destruct Z_le_gt_decr_endr2 base ; right ; lia |
exfalso
apply Hover
lia
–injection E2 as ←
cbn [ r_end ]
specialize Hoverb1 r1 E1
destruct Z_le_gt_decr_endr1 base ; left ; lia |
destruct Z_le_gt_decbase + req_extentq b1 ; right ; lia |
exfalso
apply Hover
lia
–exact Hdb1 r1 b2 r2 conjE1 L1 conjE2 L2 Hne

Safepoints

What any runtime R does at a safepoint: by Runtime.v's collector_live it frees no object.

187Module SafepointShape R : Runtime

No safepoint of R frees a live object, the premise Buffer.v once took: a safepoint changes no region (collector_live).

191Lemma keeps_live
∀ s m s′ m′ b reg
R.safepoints m s′ m′
object_regionb m_regionsm = Somereg
r_lifereg = Live
object_regionb m_regionsm′ = Somereg
Explore proof 3 tactics

Initial goal

⊢
∀s : R.state m : mem s′ : R.state m′ : mem b : Z reg : region, R.safepoints m s′ m′ → object_regionb m_regionsm = Somereg → r_lifereg = Live → object_regionb m_regionsm′ = Somereg

intros s m s′ m′ b reg Hsp E _

s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
b :
Z
reg :
region
Hsp :
R.safepoints m s′ m′
E :
object_regionb m_regionsm = Somereg
⊢
object_regionb m_regionsm′ = Somereg

rewrite R.collector_live_ _ _ _ Hsp

s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
b :
Z
reg :
region
Hsp :
R.safepoints m s′ m′
E :
object_regionb m_regionsm = Somereg
⊢
object_regionb m_regionsm = Somereg

exact E

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros s m s′ m′ b reg Hsp E _
rewrite R.collector_live_ _ _ _ Hsp
exact E

A safepoint keeps every object's region (collector_live) and every byte, and changes an aux slot only as aux_moves allows.

198Lemma safepoint_shape
∀ s m s′ m′
R.safepoints m s′ m′
same_regionsm m′ ∧ m_bytesm′ = m_bytesm ∧ aux_movesm m′
Explore proof 7 tactics

Initial goal

⊢
∀s : R.state m : mem s′ : R.state m′ : mem, R.safepoints m s′ m′ → same_regionsm m′ ∧ m_bytesm′ = m_bytesm ∧ aux_movesm m′

intros s m s′ m′ Hsp

s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
Hsp :
R.safepoints m s′ m′
⊢
same_regionsm m′ ∧ m_bytesm′ = m_bytesm ∧ aux_movesm m′

split ; | split

3 open

s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
Hsp :
R.safepoints m s′ m′
⊢
same_regionsm m′
focused goal
s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
Hsp :
R.safepoints m s′ m′
⊢
m_bytesm′ = m_bytesm
focused goal
s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
Hsp :
R.safepoints m s′ m′
⊢
aux_movesm m′

–intros b

3 open

s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
Hsp :
R.safepoints m s′ m′
b :
Z
⊢
object_regionb m_regionsm′ = object_regionb m_regionsm
deferred goal
s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
Hsp :
R.safepoints m s′ m′
⊢
m_bytesm′ = m_bytesm
deferred goal
s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
Hsp :
R.safepoints m s′ m′
⊢
aux_movesm m′

rewrite R.collector_live_ _ _ _ Hsp

3 open

s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
Hsp :
R.safepoints m s′ m′
b :
Z
⊢
object_regionb m_regionsm = object_regionb m_regionsm
deferred goal
s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
Hsp :
R.safepoints m s′ m′
⊢
m_bytesm′ = m_bytesm
deferred goal
s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
Hsp :
R.safepoints m s′ m′
⊢
aux_movesm m′

reflexivity

2 open

deferred goal
s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
Hsp :
R.safepoints m s′ m′
⊢
m_bytesm′ = m_bytesm
deferred goal
s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
Hsp :
R.safepoints m s′ m′
⊢
aux_movesm m′

–exact R.non_moving_ _ _ _ Hsp

deferred goal
s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
Hsp :
R.safepoints m s′ m′
⊢
aux_movesm m′

–exact R.aux_round_trip_ _ _ _ Hsp

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros s m s′ m′ Hsp
split ; | split
–intros b
rewrite R.collector_live_ _ _ _ Hsp
reflexivity
–exact R.non_moving_ _ _ _ Hsp
–exact R.aux_round_trip_ _ _ _ Hsp

A safepoint of R keeps live objects apart: it changes no region.

208Lemma live_disjoint_safepoint
∀ s m s′ m′
R.safepoints m s′ m′
live_disjointm
live_disjointm′
Explore proof 4 tactics

Initial goal

⊢
∀s : R.state m : mem s′ : R.state m′ : mem, R.safepoints m s′ m′ → live_disjointm → live_disjointm′

intros s m s′ m′ Hsp Hd b1 r1 b2 r2 E1 L1 E2 L2

s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
Hsp :
R.safepoints m s′ m′
Hd :
live_disjointm
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm′ = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm′ = Somer2
L2 :
r_lifer2 = Live
⊢
b1 ≠ b2 → r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

destruct safepoint_shape_ _ _ _ Hsp as Hr & _

s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
Hsp :
R.safepoints m s′ m′
Hd :
live_disjointm
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm′ = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm′ = Somer2
L2 :
r_lifer2 = Live
Hr :
same_regionsm m′
⊢
b1 ≠ b2 → r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

rewrite Hr in E1 , E2

s :
R.state
m :
mem
s′ :
R.state
m′ :
mem
Hsp :
R.safepoints m s′ m′
Hd :
live_disjointm
b1 :
Z
r1 :
region
b2 :
Z
r2 :
region
E1 :
object_regionb1 m_regionsm = Somer1
L1 :
r_lifer1 = Live
E2 :
object_regionb2 m_regionsm = Somer2
L2 :
r_lifer2 = Live
Hr :
same_regionsm m′
⊢
b1 ≠ b2 → r_endr1 ≤ b2 ∨ r_endr2 ≤ b1

exact Hdb1 r1 b2 r2 conjE1 L1 conjE2 L2

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros s m s′ m′ Hsp Hd b1 r1 b2 r2 E1 L1 E2 L2
destruct safepoint_shape_ _ _ _ Hsp as Hr & _
rewrite Hr in E1 , E2
exact Hdb1 r1 b2 r2 conjE1 L1 conjE2 L2