rocq/theories/Identity.v
Objects last: what a run of Machine R, the machine over a runtime R, leaves of the objects it finds (docs/formal.md, Campaign 3; docs/rocq.md, Identities persist).
The reuse forms trust a check that passed earlier, as long as the names it read are unchanged. That is sound only if the object it checked is still there when the reuse comes: as it was, so the check passes again, or freed, so it traps out of bounds. A run must never lose the object, or a new one could take its base and an old capability would name the new object. This file proves that memory persists over every run that starts ready (mreachable_persists): every object keeps its identity.
Decisions
| Decision | Why |
|---|---|
free_ids follows from an axiom | the module type's free_lifetime says each identity after a free was one before, not the reverse; free_keeps_ids (mbrock's decision, with axiom-identity.c) says the reverse, as rooting does at safepoints |
| an allocation's base was no object's | fresh says so, which is what keeps an old capability from naming the new object |
| the regions of a step are compared, not its bytes | kept already says where a step writes; identity is about the region list alone |
From Stdlib Require Import String ZArith List Bool Lia
From Nanofil Require Import Term Syntax Values Memory Runtime Ops Semantics Machine
Import ListNotations
Open Scope Z_scope
Identities persist
Every object of memory m is still an object of memory m': each base that names a region in m (object_region) names one in m', possibly changed. A step that satisfies this keeps every identity.
∀b reg, object_regionb m_regionsm = Somereg → ∃reg′, object_regionb m_regionsm′ = Somereg′
The region reg as a free, or the end of its frame, leaves it: the same base and kind, its bounds emptied (its end at its base), and marked Freed, so that every access to it traps out of bounds.
Each object of memory m is in memory m' as it was, or as its freed_region: nothing is lost, and no base is given to another object. This is how memory persists along a run, and why a check that passed in m passes again in m' or traps (persists_access).
∀b reg, object_regionb m_regionsm = Somereg → object_regionb m_regionsm′ = Somereg ∨ object_regionb m_regionsm′ = Somefreed_regionreg
The region object_region finds for base b in a region list rs has base b.
Explore proof 3 tactics
Initial goal
⊢
∀b : Z rs : listregion reg : region, object_regionb rs = Somereg → r_basereg = b
intros b rs reg
⊢
object_regionb rs = Somereg → r_basereg = b
induction rs as | r rs IH ; simpl ; discriminate |
⊢
destruct Z.eqbr_baser b eqn: E ; intros H ; injection H as ← ; apply Z.eqb_eq ; exact E | exact IH
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros b rs reg
induction rs as | r rs IH ; simpl ; discriminate |
destruct Z.eqbr_baser b eqn: E ; intros H ; injection H as ← ; apply Z.eqb_eq ; exact E | exact IH
A memory persists from itself.
Explore proof 3 tactics
Initial goal
intros m b reg H
⊢
object_regionb m_regionsm = Somereg ∨ object_regionb m_regionsm = Somefreed_regionreg
left
⊢
object_regionb m_regionsm = Somereg
exact H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m b reg H
left
exact H
Persistence composes: if m2 persists from m1 and m3 from m2, then m3 persists from m1.
Explore proof 5 tactics
Initial goal
intros m1 m2 m3 H12 H23 b reg H1
⊢
object_regionb m_regionsm3 = Somereg ∨ object_regionb m_regionsm3 = Somefreed_regionreg
destruct H12_ _ H1 as H2 | H2
2 openm1, m2, m3 :
H12 :
persistsm1 m2
H23 :
persistsm2 m3
b :
Z
reg :
H1 :
object_regionb m_regionsm1 = Somereg
H2 :
object_regionb m_regionsm2 = Somereg
⊢
object_regionb m_regionsm3 = Somereg ∨ object_regionb m_regionsm3 = Somefreed_regionreg
focused goal
m1, m2, m3 :
H12 :
persistsm1 m2
H23 :
persistsm2 m3
b :
Z
reg :
H1 :
object_regionb m_regionsm1 = Somereg
H2 :
object_regionb m_regionsm2 = Somefreed_regionreg
⊢
object_regionb m_regionsm3 = Somereg ∨ object_regionb m_regionsm3 = Somefreed_regionreg
–exact H23_ _ H2
deferred goal
m1, m2, m3 :
H12 :
persistsm1 m2
H23 :
persistsm2 m3
b :
Z
reg :
H1 :
object_regionb m_regionsm1 = Somereg
H2 :
object_regionb m_regionsm2 = Somefreed_regionreg
⊢
object_regionb m_regionsm3 = Somereg ∨ object_regionb m_regionsm3 = Somefreed_regionreg
–right
m1, m2, m3 :
H12 :
persistsm1 m2
H23 :
persistsm2 m3
b :
Z
reg :
H1 :
object_regionb m_regionsm1 = Somereg
H2 :
object_regionb m_regionsm2 = Somefreed_regionreg
⊢
object_regionb m_regionsm3 = Somefreed_regionreg
destruct H23_ _ H2 as H3 | H3 ; exact H3
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m1 m2 m3 H12 H23 b reg H1
destruct H12_ _ H1 as H2 | H2
–exact H23_ _ H2
–right
destruct H23_ _ H2 as H3 | H3 ; exact H3
A memory m' with the same region list as m persists from m.
Explore proof 4 tactics
Initial goal
intros m m′ E b reg H
⊢
object_regionb m_regionsm′ = Somereg ∨ object_regionb m_regionsm′ = Somefreed_regionreg
left
⊢
object_regionb m_regionsm′ = Somereg
rewrite E
⊢
object_regionb m_regionsm = Somereg
exact H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m m′ E b reg H
left
rewrite E
exact H
A change of memory from m to m' persists where it is a region_step (each object of m' was one of m, unchanged or ended in place) and loses no identity (ids). These are what the program and the runtime may do to regions.
Explore proof 10 tactics
Initial goal
⊢
∀m m′ : mem, region_stepm m′ → idsm m′ → persistsm m′
intros m m′ Hr Hi b reg H
⊢
object_regionb m_regionsm′ = Somereg ∨ object_regionb m_regionsm′ = Somefreed_regionreg
destruct Hi_ _ H as reg′ H′
m, m′ :
Hr :
region_stepm m′
Hi :
idsm m′
b :
Z
reg :
H :
object_regionb m_regionsm = Somereg
reg′ :
H′ :
object_regionb m_regionsm′ = Somereg′
⊢
object_regionb m_regionsm′ = Somereg ∨ object_regionb m_regionsm′ = Somefreed_regionreg
destruct Hr_ _ H′ as reg0 & E0 & → | _ & → ; rewrite H in E0 ; injection E0 as ←
2 openm, m′ :
Hr :
region_stepm m′
Hi :
idsm m′
b :
Z
reg :
H :
object_regionb m_regionsm = Somereg
H′ :
object_regionb m_regionsm′ = Somereg
⊢
object_regionb m_regionsm′ = Somereg ∨ object_regionb m_regionsm′ = Somefreed_regionreg
focused goal
⊢
object_regionb m_regionsm′ = Somereg ∨ object_regionb m_regionsm′ = Somefreed_regionreg
–left
2 openm, m′ :
Hr :
region_stepm m′
Hi :
idsm m′
b :
Z
reg :
H :
object_regionb m_regionsm = Somereg
H′ :
object_regionb m_regionsm′ = Somereg
⊢
object_regionb m_regionsm′ = Somereg
deferred goal
⊢
object_regionb m_regionsm′ = Somereg ∨ object_regionb m_regionsm′ = Somefreed_regionreg
exact H′
deferred goal
⊢
object_regionb m_regionsm′ = Somereg ∨ object_regionb m_regionsm′ = Somefreed_regionreg
–right
⊢
object_regionb m_regionsm′ = Somefreed_regionreg
rewrite H′
unfold freed_region
rewrite object_region_base_ _ _ H
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m m′ Hr Hi b reg H
destruct Hi_ _ H as reg′ H′
destruct Hr_ _ H′ as reg0 & E0 & → | _ & → ; rewrite H in E0 ; injection E0 as ←
–left
exact H′
The same for a lifetime_step, what the runtime's free and its safepoint action may do: with no identity lost, memory persists.
Explore proof 2 tactics
Initial goal
⊢
∀m m′ : mem, lifetime_stepm m′ → idsm m′ → persistsm m′
intros m m′ Hl Hi
⊢
persistsm m′
exact region_ids_persists_ _ lifetime_region_step_ _ Hl Hi
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m m′ Hl Hi
exact region_ids_persists_ _ lifetime_region_step_ _ Hl Hi
The same for kept, what the program's own steps between allocations may do to memory.
Explore proof 2 tactics
Initial goal
intros m m′ Hr _ Hi
⊢
persistsm m′
exact region_ids_persists_ _ Hr Hi
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m m′ Hr _ Hi
exact region_ids_persists_ _ Hr Hi
Explore proof 8 tactics
Initial goal
intros m q base Hn b reg H
⊢
object_regionb m_regionsallocatedm q base = Somereg ∨ object_regionb m_regionsallocatedm q base = Somefreed_regionreg
left
⊢
object_regionb m_regionsallocatedm q base = Somereg
simpl
⊢
else
=
Somereg
destruct Z.eqbbase b eqn: E ; | exact H
m :
q :
base :
Z
Hn :
object_regionbase m_regionsm = None
b :
Z
reg :
H :
object_regionb m_regionsm = Somereg
E :
base =? b = true
apply Z.eqb_eq in E
m :
q :
base :
Z
Hn :
object_regionbase m_regionsm = None
b :
Z
reg :
H :
object_regionb m_regionsm = Somereg
E :
base = b
subst
rewrite Hn in H
discriminate H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m q base Hn b reg H
left
simpl
destruct Z.eqbbase b eqn: E ; | exact H
apply Z.eqb_eq in E
subst
rewrite Hn in H
discriminate H
Steps that write keep the regions
A store (store_res, store_res/7) writes bytes but leaves the region list unchanged.
Explore proof 3 tactics
Initial goal
unfold store_res
⊢
match w with
⇒
match x with
_
⇒
None
_
⇒
match x with
_
⇒
None
=
Somer, m′
→
intros w m a c x r m′ H
w :
m :
a :
Z
c :
x :
r :
resunit
m′ :
H :
match w with
⇒
match x with
_
⇒
None
_
⇒
match x with
_
⇒
None
=
Somer, m′
destruct w , x ; try discriminate ; cases H ; inversion H ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Folding a memory update f over a list xs leaves the region list unchanged where each application of f does. A helper for lists of store effects.
Explore proof 9 tactics
Initial goal
intros A f xs
induction xs as | x xs IH ; simpl ; intros m0 m′ Hf H
2 openA :
Type
m0, m′ :
H :
Somem0 = Somem′
focused goal
A :
Type
x :
A
xs :
listA
IH :
m0, m′ :
H :
–injection H as ←
2 openA :
Type
m0 :
deferred goal
A :
Type
x :
A
xs :
listA
IH :
m0, m′ :
H :
reflexivity
deferred goal
A :
Type
x :
A
xs :
listA
IH :
m0, m′ :
H :
–destruct fm0 x as m1 | eqn: E
2 openA :
Type
x :
A
xs :
listA
IH :
m0, m′ :
m1 :
E :
fm0 x = Somem1
H :
focused goal
A :
Type
x :
A
xs :
listA
IH :
m0, m′ :
E :
fm0 x = None
H :
+rewrite IH_ _ Hf H
2 openA :
Type
x :
A
xs :
listA
IH :
m0, m′ :
m1 :
E :
fm0 x = Somem1
H :
deferred goal
A :
Type
x :
A
xs :
listA
IH :
m0, m′ :
E :
fm0 x = None
H :
exact Hf_ _ _ E
deferred goal
A :
Type
x :
A
xs :
listA
IH :
m0, m′ :
E :
fm0 x = None
H :
+rewrite fold_left_none in H
A :
Type
x :
A
xs :
listA
IH :
m0, m′ :
E :
fm0 x = None
H :
None = Somem′
discriminate H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros A f xs
induction xs as | x xs IH ; simpl ; intros m0 m′ Hf H
–injection H as ←
reflexivity
–destruct fm0 x as m1 | eqn: E
+rewrite IH_ _ Hf H
exact Hf_ _ _ E
+rewrite fold_left_none in H
discriminate H
The effects of storing the pointer x at address a (pointer_store_effects, pointer_store_effects//6) leave the region list unchanged.
Explore proof 4 tactics
Initial goal
intros a x m es m′ H
apply fold_regionseffect pointer_store_effecta x es m m′ ; | exact H
intros m1 e m2 E
destruct e ; simpl in E ; try discriminate E ; injection E as ← ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros a x m es m′ H
apply fold_regionseffect pointer_store_effecta x es m m′ ; | exact H
intros m1 e m2 E
destruct e ; simpl in E ; try discriminate E ; injection E as ← ; reflexivity
Reading a variadic argument through the argument pointer p (va_arg_res) leaves the region list unchanged, though it may write memory.
Explore proof 3 tactics
Initial goal
unfold va_arg_res
⊢
SomeRVal_
⇒
Somestep, align
⇒
match access_resm ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align ptr_capptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp step Read 8 with
SomeRVal_
⇒
match store_resWl m ptr_addrp ptr_capp WIntptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align + step with
SomeRVal_, m1
⇒
match k with
⇒
_
⇒
SomeRValWIntload_bytesm1 ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align width_bytesw, m1
_
⇒
None
_
⇒
None
None
⇒
None
_
⇒
None
=
Somer, m′
→
intros k p m r m′ H
k :
p :
m :
m′ :
H :
SomeRVal_
⇒
Somestep, align
⇒
match access_resm ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align ptr_capptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp step Read 8 with
SomeRVal_
⇒
match store_resWl m ptr_addrp ptr_capp WIntptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align + step with
SomeRVal_, m1
⇒
match k with
⇒
_
⇒
SomeRValWIntload_bytesm1 ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align width_bytesw, m1
_
⇒
None
_
⇒
None
None
⇒
None
_
⇒
None
=
Somer, m′
cases H;match type of H withSome_, = Some_, ⇒assert x = y as ← by congruenceend;first
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold va_arg_res
intros k p m r m′ H
cases H;match type of H withSome_, = Some_, ⇒assert x = y as ← by congruenceend;first
Explore proof 3 tactics
Initial goal
unfold op_res , float_integer
⊢
match o with
⇒
⇒
match xs with
⇒
match xs with
=
SomeOpResr m′
→
intros o k xs m r m′ H
o :
k :
xs :
listword
m :
m′ :
H :
match o with
⇒
⇒
match xs with
⇒
match xs with
=
SomeOpResr m′
destruct o ; cases H ; inversion H ; subst;first
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A memory keeps its own identities.
Explore proof 2 tactics
Initial goal
intros m b reg H
⊢
∃reg′ : region, object_regionb m_regionsm = Somereg′
eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m b reg H
eauto
Keeping identities composes, from m1 to m2 to m3.
Explore proof 3 tactics
Initial goal
intros m1 m2 m3 H12 H23 b reg H
⊢
∃reg′ : region, object_regionb m_regionsm3 = Somereg′
destruct H12_ _ H as reg2 H2
m1, m2, m3 :
H12 :
idsm1 m2
H23 :
idsm2 m3
b :
Z
reg :
H :
object_regionb m_regionsm1 = Somereg
reg2 :
H2 :
object_regionb m_regionsm2 = Somereg2
⊢
∃reg′ : region, object_regionb m_regionsm3 = Somereg′
exact H23_ _ H2
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m1 m2 m3 H12 H23 b reg H
destruct H12_ _ H as reg2 H2
exact H23_ _ H2
A memory with the same region list as m keeps every identity of m.
Explore proof 3 tactics
Initial goal
intros m m′ E b reg H
⊢
∃reg′ : region, object_regionb m_regionsm′ = Somereg′
rewrite E
⊢
∃reg′ : region, object_regionb m_regionsm = Somereg′
eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m m′ E b reg H
rewrite E
eauto
Ending an invocation's named locals as it returns, as invalidate_locals/3 does, frees each in place and drops no object: every identity is kept.
Explore proof 14 tactics
Initial goal
⊢
∀locals : listname × optionZ m m′ : mem, invalidate_localslocals m = Somem′ → idsm m′
unfold invalidate_locals
⊢
intros locals
induction locals as | x slot ls IH ; simpl ; intros m m′ H
2 open–injection H as ←
2 openapply ids_refl
–destruct slot as base | ; | exact IH_ _ H
destruct object_regionbase m_regionsm as reg | eqn: Er ; simpl in H ; | rewrite fold_left_none in H ; discriminate H
x :
base :
Z
ls :
listname × optionZ
IH :
m, m′ :
reg :
Er :
object_regionbase m_regionsm = Somereg
H :
fold_left
let* m ≔ acc in
ls
=
Somem′
⊢
idsm m′
destruct r_kindreg , r_lifereg ; simpl in H ; try rewrite fold_left_none in H ; discriminate H
x :
base :
Z
ls :
listname × optionZ
IH :
m, m′ :
reg :
Er :
object_regionbase m_regionsm = Somereg
H :
fold_left
let* m ≔ acc in
ls
=
Somem′
⊢
idsm m′
destruct replace_regionbase _ m_regionsm as rs | eqn: Ers ; simpl in H ; | rewrite fold_left_none in H ; discriminate H
eapply ids_trans ; | exact IH_ _ H
x :
base :
Z
ls :
listname × optionZ
IH :
m, m′ :
reg :
Er :
object_regionbase m_regionsm = Somereg
rs :
listregion
Ers :
H :
fold_left
let* m ≔ acc in
ls
=
Somem′
intros b r0 Hb
x :
base :
Z
ls :
listname × optionZ
IH :
m, m′ :
reg :
Er :
object_regionbase m_regionsm = Somereg
rs :
listregion
Ers :
H :
fold_left
let* m ≔ acc in
ls
=
Somem′
b :
Z
r0 :
Hb :
object_regionb m_regionsm = Somer0
simpl
x :
base :
Z
ls :
listname × optionZ
IH :
m, m′ :
reg :
Er :
object_regionbase m_regionsm = Somereg
rs :
listregion
Ers :
H :
fold_left
let* m ≔ acc in
ls
=
Somem′
b :
Z
r0 :
Hb :
object_regionb m_regionsm = Somer0
⊢
∃reg′ : region, object_regionb rs = Somereg′
rewrite object_region_replace_ _ _ _ b Ers eq_refl
x :
base :
Z
ls :
listname × optionZ
IH :
m, m′ :
reg :
Er :
object_regionbase m_regionsm = Somereg
rs :
listregion
Ers :
H :
fold_left
let* m ≔ acc in
ls
=
Somem′
b :
Z
r0 :
Hb :
object_regionb m_regionsm = Somer0
destruct Z.eqbb base ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold invalidate_locals
intros locals
induction locals as | x slot ls IH ; simpl ; intros m m′ H
–injection H as ←
apply ids_refl
–destruct slot as base | ; | exact IH_ _ H
destruct object_regionbase m_regionsm as reg | eqn: Er ; simpl in H ; | rewrite fold_left_none in H ; discriminate H
destruct r_kindreg , r_lifereg ; simpl in H ; try rewrite fold_left_none in H ; discriminate H
destruct replace_regionbase _ m_regionsm as rs | eqn: Ers ; simpl in H ; | rewrite fold_left_none in H ; discriminate H
eapply ids_trans ; | exact IH_ _ H
intros b r0 Hb
simpl
rewrite object_region_replace_ _ _ _ b Ers eq_refl
destruct Z.eqbb base ; eauto
A step keeps every identity
A free function (from a pointer word and a memory to a result and a new memory) keeps every identity: what it frees stays an object, freed in place. The runtime axiom free_keeps_ids gives this of R's free (R_free_ids).
∀x m r m′, freex m = Somer, m′ → idsm m′
Explore proof 4 tactics
Initial goal
intros ge fr m i e l m′ Hfree H
destruct i
8 openfocused goal
focused goal
focused goal
focused goal
focused goal
focused goal
1: destruct special_leto eqn: Es ; destruct o ; try discriminate Es | rewrite inst_step_let_ _ _ _ _ _ _ Es in H
11 openge :
fr :
m :
d :
k :
x :
off, bytes :
Z
r :
align :
Z
args :
listvalue
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m Letd k CheckLocalx off bytes r align args = SomeIContinuee l m′
Es :
special_letCheckLocalx off bytes r align = true
⊢
idsm m′
focused goal
focused goal
focused goal
ge :
fr :
m :
d :
k :
o :
args :
listvalue
e :
l :
listname × optionZ
m′ :
H :
Es :
special_leto = false
⊢
idsm m′
focused goal
focused goal
focused goal
focused goal
focused goal
focused goal
all: unfold inst_step , external_call , bind_res , store_out in H ; cases H ; inversion H ; subst;first
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge fr m i e l m′ Hfree H
destruct i
1: destruct special_leto eqn: Es ; destruct o ; try discriminate Es | rewrite inst_step_let_ _ _ _ _ _ _ Es in H
all: unfold inst_step , external_call , bind_res , store_out in H ; cases H ; inversion H ; subst;first
A return (return_step) from configuration c to c' keeps every identity: it only ends the returning frame's locals.
Explore proof 5 tactics
Initial goal
unfold return_step
intros c o c′ H
apply or_stuck_next in H
cases H ; inversion H ; subst ; simpl
c :
o :
m :
Heqo0 :
invalidate_localsfr_localsc_framec c_memc = Somem
f :
p0 :
Heql :
c_callersc = f, p0 :: l
o0 :
Heqo1 :
e :
Heqo2 :
returned_envpd_resp0 o0 fr_envf = Somee
H :
SomeNextc_frame ≔ fr_fn ≔ fr_fnf; fr_env ≔ e; fr_locals ≔ fr_localsf; fr_doomed ≔ fr_doomedf; fr_at ≔ fr_atf; c_callers ≔ l; c_mem ≔ m; c_fuel ≔ c_fuelc = SomeNextc_frame ≔ fr_fn ≔ fr_fnf; fr_env ≔ e; fr_locals ≔ fr_localsf; fr_doomed ≔ fr_doomedf; fr_at ≔ fr_atf; c_callers ≔ l; c_mem ≔ m; c_fuel ≔ c_fuelc
match goal withE : invalidate_locals_ _ = Some_ |- _⇒exact invalidate_locals_ids_ _ _ Eend
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold return_step
intros c o c′ H
apply or_stuck_next in H
cases H ; inversion H ; subst ; simpl
match goal withE : invalidate_locals_ _ = Some_ |- _⇒exact invalidate_locals_ids_ _ _ Eend
A jump at the end of block l (jump_step) keeps every identity: it takes an edge, which leaves memory alone, or returns.
Explore proof 4 tactics
Initial goal
unfold jump_step , edge_step
intros ge c l j c′ H
cases H ; unstuck H
9 openge :
c :
l :
j :
c′ :
r :
t :
l0 :
Heqt0 :
t = Tol0
H :
Nextcontinue_atc with_pointc_framec Enteredge_labelTol0 Somel c_memc c_fuelc = Nextc′
focused goal
ge :
c :
l :
j :
c′ :
r :
v :
t1, t2 :
Heqj0 :
j = JBranchv t1 t2
w :
n :
Z
Heqw0 :
w = WIntn
l0 :
Heqt :
H :
SomeNextcontinue_atc with_pointc_framec Enteredge_labelTol0 Somel c_memc c_fuelc = SomeNextc′
focused goal
focused goal
focused goal
ge :
c :
l :
j :
c′ :
v :
t1, t2 :
Heqj0 :
j = JBranchv t1 t2
w :
n :
Z
Heqw0 :
w = WIntn
l0 :
Heqt :
H :
SomeNextcontinue_atc with_pointc_framec Enteredge_labelTol0 Somel c_memc c_fuelc = SomeNextc′
focused goal
ge :
c :
l :
j :
c′ :
v :
t1, t2 :
Heqj0 :
j = JBranchv t1 t2
w :
n :
Z
Heqw0 :
w = WIntn
l0 :
Heqt :
H :
SomeNextcontinue_atc with_pointc_framec Enteredge_labelPolll0 Somel c_memc c_fuelc = SomeNextc′
focused goal
focused goal
all: first
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
A step of configuration c that allocates nothing (Next c') keeps every identity of its memory, where ge's free does. Allocations are step_fresh_regions.
Explore proof 4 tactics
Initial goal
unfold step , inst_next
⊢
→
Snapshot[ ] l
⇒
Snapshot_ :: _ as xs l
⇒
else
Freshheap_req16 8 × Z.of_natDatatypes.lengthxs λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesxs base allocatedc_memc heap_req16 8 × Z.of_natDatatypes.lengthxs base; c_fuel ≔ c_fuelc
=
Nextc′
→
intros ge c c′ Hfree H
ge :
c, c′ :
H :
Snapshot[ ] l
⇒
Snapshot_ :: _ as xs l
⇒
else
Freshheap_req16 8 × Z.of_natDatatypes.lengthxs λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesxs base allocatedc_memc heap_req16 8 × Z.of_natDatatypes.lengthxs base; c_fuel ≔ c_fuelc
=
Nextc′
cases H ; unstuck H
5 openfocused goal
focused goal
focused goal
focused goal
ge :
c, c′ :
l :
insts :
listinst
j :
i :
l0 :
listinst
Heql0 :
insts = i :: l0
Heqo :
i0 :
Heqo1 :
doomed_resultge c_framec c_memc i i0 = Somep
f :
xs :
listword
pd :
Heqi1 :
fstp = ICallf xs pd
f0 :
Heqo2 :
call_framef xs = Somef0
all: first
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Storing the variadic arguments xs from address a (snapshot_values, snapshot_values/5), as a variadic function's entry does into its new snapshot object, leaves the region list unchanged.
∀ xs a m
m_regionssnapshot_valuesxs a m = m_regionsm
Explore proof 2 tactics
Initial goal
⊢
∀xs : listword a : Z m : mem, m_regionssnapshot_valuesxs a m = m_regionsm
induction xs as | x xs IH ; intros a m ; simpl ; reflexivity |
⊢
match x with
=
destruct x ; rewrite IH ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
induction xs as | x xs IH ; intros a m ; simpl ; reflexivity |
destruct x ; rewrite IH ; reflexivity
Proof 5 steps Qed
unfold op_res , op_res_int , float_integer
intros o k xs m q kont H
destruct o ; cases H ; inversion H ; subst
intros base
reflexivity
Explore proof 5 tactics
Initial goal
intros ge fr m i q k H
destruct i
8 openfocused goal
focused goal
focused goal
focused goal
focused goal
focused goal
1: destruct special_leto eqn: Es ; destruct o ; try discriminate Es | rewrite inst_step_let_ _ _ _ _ _ _ Es in H
11 openge :
fr :
m :
d :
k0 :
x :
off, bytes :
Z
r :
align :
Z
args :
listvalue
q :
H :
inst_stepge fr m Letd k0 CheckLocalx off bytes r align args = SomeIFreshq k
Es :
special_letCheckLocalx off bytes r align = true
focused goal
focused goal
focused goal
focused goal
focused goal
focused goal
focused goal
focused goal
focused goal
all: unfold inst_step , external_call , bind_res , store_out in H ; cases H ; inversion H ; subst ; intros base
2 openge :
fr :
m :
d :
k0 :
o :
args :
listvalue
q :
l :
listclass
Heqo0 :
op_arg_classeso k0 = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
H :
Es :
special_leto = false
base :
Z
focused goal
ge :
fr :
m :
x :
size :
Z
H :
base :
Z
all: first
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge fr m i q k H
destruct i
1: destruct special_leto eqn: Es ; destruct o ; try discriminate Es | rewrite inst_step_let_ _ _ _ _ _ _ Es in H
all: unfold inst_step , external_call , bind_res , store_out in H ; cases H ; inversion H ; subst ; intros base
all: first
A step that allocates (Fresh q k) does the same: whatever base the runtime gives, the next configuration's regions are the old ones with the new object added. An allocation adds one identity and drops none.
Explore proof 11 tactics
Initial goal
unfold step , inst_next
⊢
Snapshot[ ] l
⇒
Snapshot_ :: _ as xs l
⇒
else
Freshheap_req16 8 × Z.of_natDatatypes.lengthxs λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesxs base allocatedc_memc heap_req16 8 × Z.of_natDatatypes.lengthxs base; c_fuel ≔ c_fuelc
=
Freshq k
→
intros ge c q k H
ge :
c :
q :
k :
Z → config
H :
Snapshot[ ] l
⇒
Snapshot_ :: _ as xs l
⇒
else
Freshheap_req16 8 × Z.of_natDatatypes.lengthxs λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesxs base allocatedc_memc heap_req16 8 × Z.of_natDatatypes.lengthxs base; c_fuel ≔ c_fuelc
=
Freshq k
cases H ; unstuck H ; try exfalso ; exact jump_step_not_fresh_ _ _ _ _ _ H
2 openge :
c :
q :
k :
Z → config
xs :
listword
l :
w :
l0 :
listword
Heql0 :
xs = w :: l0
Heqb :
negbforallbsnapshot_word w :: l0 = false
H :
Freshheap_req16 8 × Z.of_natDatatypes.lengthw :: l0 λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesw :: l0 base allocatedc_memc heap_req16 8 × Z.of_natDatatypes.lengthw :: l0 base; c_fuel ≔ c_fuelc = Freshq k
all: injection H as Hq Hk ; subst q k ; intros base
2 openge :
c :
xs :
listword
l :
w :
l0 :
listword
Heql0 :
xs = w :: l0
Heqb :
negbforallbsnapshot_word w :: l0 = false
base :
Z
⊢
m_regionsc_memc_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ match w with WIntn ⇒ snapshot_valuesl0 base + 8 store_bytesallocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthl0~0~0~0 base base 8 n WPtrp ⇒ snapshot_valuesl0 base + 8 store_auxstore_bytesallocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthl0~0~0~0 base base 8 ptr_addrp base ptr_capp WLimit_ _ ⇒ snapshot_valuesl0 base + 8 allocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthl0~0~0~0 base end; c_fuel ≔ c_fuelc = m_regionsallocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthl0~0~0~0 base
–match goal withHp : fr_at_ = Snapshot _ |- _⇒exact snapshot_values_regionsxs base _end
–match goal withE : doomed_result_ _ _ _ _ = Some , Hc : fst = IFresh_ _ |- _⇒destruct doomed_result_out_ _ _ _ _ _ E as Ho | e′ & l′ & Ho | o′ & Ho ; rewrite Ho in Hc ; try discriminate Hcend
subst
match goal withE2 : inst_step_ _ _ _ = SomeIFresh_ |- _⇒pose proof inst_step_fresh_regions_ _ _ _ _ _ E2 base as Hkend
simpl
match goal withHk : m_regionssnd = _ |- _⇒destruct t as e1 l1 m1end
exact Hk
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge c q k H
cases H ; unstuck H ; try exfalso ; exact jump_step_not_fresh_ _ _ _ _ _ H
all: injection H as Hq Hk ; subst q k ; intros base
–match goal withHp : fr_at_ = Snapshot _ |- _⇒exact snapshot_values_regionsxs base _end
–match goal withE : doomed_result_ _ _ _ _ = Some , Hc : fst = IFresh_ _ |- _⇒destruct doomed_result_out_ _ _ _ _ _ E as Ho | e′ & l′ & Ho | o′ & Ho ; rewrite Ho in Hc ; try discriminate Hcend
subst
match goal withE2 : inst_step_ _ _ _ = SomeIFresh_ |- _⇒pose proof inst_step_fresh_regions_ _ _ _ _ _ E2 base as Hkend
simpl
match goal withHk : m_regionssnd = _ |- _⇒destruct t as e1 l1 m1end
exact Hk
A check that passed passes again, or its object was freed
Where an access check of a nonempty range (size bytes at address a, through the capability c, with rights r and alignment al) passed in memory m, it passes the same way in any memory m' that persists from m, or traps out of bounds because the object was freed. This is what makes it sound to reuse a check.
∀ m m′ a c size r al u
access_resm′ a c size r al = SomeRValu ∨ access_resm′ a c size r al = SomeRTrapOutOfBounds
Explore proof 3 tactics
Initial goal
⊢
∀m m′ : mem a : Z c : cap size : Z r : rights al : Z u : unit, persistsm m′ → 0 < size → access_resm a c size r al = SomeRValu → access_resm′ a c size r al = SomeRValu ∨ access_resm′ a c size r al = SomeRTrapOutOfBounds
unfold access_res , cap_access_res
intros m m′ a c size r al u Hp Hs H
destruct c as | base | base | f | n ; try discriminate H ; destruct object_regionbase m_regionsm as reg | eqn: E ; try discriminate H ; destruct Hp_ _ E as E′ | E′ ; rewrite E' ; left ; exact H | right | left ; exact H | right ; pose proof object_region_base_ _ _ E as Hb ; simpl ; rewrite Hb ; destruct base ≤? a && a + size ≤? base eqn: Eb ; try reflexivity ; apply andb_true_iff in Eb as E1 E2 ; apply Z.leb_le in E1 ; apply Z.leb_le in E2 ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold access_res , cap_access_res
intros m m′ a c size r al u Hp Hs H
destruct c as | base | base | f | n ; try discriminate H ; destruct object_regionbase m_regionsm as reg | eqn: E ; try discriminate H ; destruct Hp_ _ E as E′ | E′ ; rewrite E' ; left ; exact H | right | left ; exact H | right ; pose proof object_region_base_ _ _ E as Hb ; simpl ; rewrite Hb ; destruct base ≤? a && a + size ≤? base eqn: Eb ; try reflexivity ; apply andb_true_iff in Eb as E1 E2 ; apply Z.leb_le in E1 ; apply Z.leb_le in E2 ; lia
Over runs
Import RM
R's free keeps every identity, by the runtime axiom free_keeps_ids: free reclaims nothing; only the collector does, at a safepoint.
Explore proof 5 tactics
Initial goal
⊢
free_idsR.free
intros x m r m′ H b reg Hb
⊢
∃reg′ : region, object_regionb m_regionsm′ = Somereg′
pose proof R.free_keeps_ids_ _ _ _ H b as Hk
x :
m :
r :
resunit
m′ :
H :
R.freex m = Somer, m′
b :
Z
reg :
Hb :
object_regionb m_regionsm = Somereg
Hk :
object_regionb m_regionsm ≠ None → object_regionb m_regionsm′ ≠ None
⊢
∃reg′ : region, object_regionb m_regionsm′ = Somereg′
destruct object_regionb m_regionsm′ as reg′ | ; eauto |
x :
m :
r :
resunit
m′ :
H :
R.freex m = Somer, m′
b :
Z
reg :
Hb :
object_regionb m_regionsm = Somereg
Hk :
object_regionb m_regionsm ≠ None → None ≠ None
⊢
∃reg′ : region, None = Somereg′
exfalso
x :
m :
r :
resunit
m′ :
H :
R.freex m = Somer, m′
b :
Z
reg :
Hb :
object_regionb m_regionsm = Somereg
Hk :
object_regionb m_regionsm ≠ None → None ≠ None
⊢
False
apply Hk ; rewrite Hb ; discriminate | reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros x m r m′ H b reg Hb
pose proof R.free_keeps_ids_ _ _ _ H b as Hk
destruct object_regionb m_regionsm′ as reg′ | ; eauto |
exfalso
apply Hk ; rewrite Hb ; discriminate | reflexivity
Each machine step (mstep) from a state where R is ready (ready_state) persists memory, where the genv's free is R's: a step that allocates nothing ends objects in place, an allocation adds one at a fresh base, and R's safepoint action keeps every identity (rooting).
Explore proof 17 tactics
Initial goal
unfold ready_state
intros ge st st′ Hge Hr Hs
destruct Hs as c c′ s E | c q k s base s′ E He Hal | c s s′ m′ _ Hsp ; simpl in *
3 openfocused goal
–apply kept_ids_persists
4 openfocused goal
deferred goal
+eapply step_next_kept ; rewrite Hge ; exact free_kept | exact E
3 opendeferred goal
deferred goal
+eapply step_next_ids ; rewrite Hge ; exact R_free_ids | exact E
2 opendeferred goal
–destruct step_fresh_kept_ _ _ _ E as Ha _
2 openge :
Hge :
ge_freege = R.free
c :
s :
R.state
Hr :
R.readys c_memc
q :
k :
Z → config
base :
Z
s′ :
R.state
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
Ha :
0 < req_alignq
destruct R.fresh_allocation_ _ _ _ _ Hr Ha He Hal as _ & _ & _ & Hnone & _ _
2 openge :
Hge :
ge_freege = R.free
c :
s :
R.state
Hr :
R.readys c_memc
q :
k :
Z → config
base :
Z
s′ :
R.state
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
Ha :
0 < req_alignq
Hnone :
object_regionbase m_regionsc_memc = None
eapply persists_trans ; exact allocated_persists_ q _ Hnone |
2 openge :
Hge :
ge_freege = R.free
c :
s :
R.state
Hr :
R.readys c_memc
q :
k :
Z → config
base :
Z
s′ :
R.state
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
Ha :
0 < req_alignq
Hnone :
object_regionbase m_regionsc_memc = None
apply persists_same
2 openge :
Hge :
ge_freege = R.free
c :
s :
R.state
Hr :
R.readys c_memc
q :
k :
Z → config
base :
Z
s′ :
R.state
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
Ha :
0 < req_alignq
Hnone :
object_regionbase m_regionsc_memc = None
exact step_fresh_regions_ _ _ _ E base
–apply lifetime_ids_persists ; exact R.safepoint_lifetime_ _ _ _ Hsp |
intros b reg H
pose proof R.rooting_ _ _ _ Hsp b as Hroot
ge :
Hge :
ge_freege = R.free
c :
s :
R.state
Hr :
R.readys c_memc
s′ :
R.state
m′ :
Hsp :
R.safepoints c_memc s′ m′
b :
Z
reg :
H :
object_regionb m_regionsc_memc = Somereg
Hroot :
object_regionb m_regionsc_memc ≠ None → object_regionb m_regionsm′ ≠ None
⊢
∃reg′ : region, object_regionb m_regionsm′ = Somereg′
destruct object_regionb m_regionsm′ as reg′ | eqn: E′ ; eauto |
ge :
Hge :
ge_freege = R.free
c :
s :
R.state
Hr :
R.readys c_memc
s′ :
R.state
m′ :
Hsp :
R.safepoints c_memc s′ m′
b :
Z
reg :
H :
object_regionb m_regionsc_memc = Somereg
E′ :
object_regionb m_regionsm′ = None
Hroot :
object_regionb m_regionsc_memc ≠ None → None ≠ None
⊢
∃reg′ : region, None = Somereg′
exfalso
ge :
Hge :
ge_freege = R.free
c :
s :
R.state
Hr :
R.readys c_memc
s′ :
R.state
m′ :
Hsp :
R.safepoints c_memc s′ m′
b :
Z
reg :
H :
object_regionb m_regionsc_memc = Somereg
E′ :
object_regionb m_regionsm′ = None
Hroot :
object_regionb m_regionsc_memc ≠ None → None ≠ None
⊢
False
apply Hroot ; rewrite H ; discriminate | reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold ready_state
intros ge st st′ Hge Hr Hs
destruct Hs as c c′ s E | c q k s base s′ E He Hal | c s s′ m′ _ Hsp ; simpl in *
–apply kept_ids_persists
+eapply step_next_kept ; rewrite Hge ; exact free_kept | exact E
+eapply step_next_ids ; rewrite Hge ; exact R_free_ids | exact E
–destruct step_fresh_kept_ _ _ _ E as Ha _
destruct R.fresh_allocation_ _ _ _ _ Hr Ha He Hal as _ & _ & _ & Hnone & _ _
eapply persists_trans ; exact allocated_persists_ q _ Hnone |
apply persists_same
exact step_fresh_regions_ _ _ _ E base
–apply lifetime_ids_persists ; exact R.safepoint_lifetime_ _ _ _ Hsp |
intros b reg H
pose proof R.rooting_ _ _ _ Hsp b as Hroot
destruct object_regionb m_regionsm′ as reg′ | eqn: E′ ; eauto |
exfalso
apply Hroot ; rewrite H ; discriminate | reflexivity
Over a run that starts ready, the memory of every later state (mreachable: any number of machine steps) persists from the first: each object is in every later state as it was, or freed.
Explore proof 5 tactics
Initial goal
⊢
∀ge : genv st st′ : mstate, ge_freege = R.free → mreachablege st st′ → ready_statest → persistsc_memfstst c_memfstst′
intros ge st st′ Hge H
⊢
ready_statest → persistsc_memfstst c_memfstst′
induction H as st st′ Hs | st | st1 st2 st3 H12 IH1 _ IH2 ; intros Hr
3 openfocused goal
–eapply mstep_persists ; eauto
2 opendeferred goal
–apply persists_refl
–eapply persists_trans ; exact IH1Hr | apply IH2 ; exact mreachable_ready_ _ _ Hge H12 Hr
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge st st′ Hge H
induction H as st st′ Hs | st | st1 st2 st3 H12 IH1 _ IH2 ; intros Hr
–eapply mstep_persists ; eauto
–apply persists_refl
–eapply persists_trans ; exact IH1Hr | apply IH2 ; exact mreachable_ready_ _ _ Hge H12 Hr
The same for the interpreter's runtime InterpRuntime, which proves every runtime axiom.
Under the interpreter's runtime, every run that starts ready persists memory, with no hypothesis but that the genv's free is the interpreter's.
∀ ge st st′
Explore proof 2 tactics
Initial goal
⊢
∀ge : genv st st′ : InterpIdentity.RM.mstate, ge_freege = InterpRuntime.free → InterpIdentity.RM.mreachablege st st′ → InterpIdentity.RM.ready_statest → persistsc_memfstst c_memfstst′
intros ge st st′ Hge H Hr
exact InterpIdentity.mreachable_persists_ _ _ Hge H Hr
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge st st′ Hge H Hr
exact InterpIdentity.mreachable_persists_ _ _ Hge H Hr