Fil-C on Nix

Filnix wiki

the formal campaign

rocq/theories/Machine.v

Campaign 3's machine: Semantics.v's steps run over a Runtime (Runtime.v), and the first invariant of every run, that the runtime stays ready to allocate (formal.md, Campaign 3; rocq.md).

Semantics.v's step_rel takes any fresh base for an allocation and has no other thread. The machine of a runtime R is what one thread's program sees run under R: R chooses each allocation's base, R's free runs each call of libc's free (Run.v's Driver makes the genv so), and R may act before an instruction where R.at_safepoint holds and before a poll edge is taken, and nowhere else. That is what lets the validator keep evidence across every other instruction and edge.

Decisions

DecisionWhy
the runtime acts *before* an at_safepoint instruction or a poll edgethe instruction then runs on what the runtime left, as native code does after a pollcheck
an allocation with a negative extent has no machine stepfresh_allocation covers extents from 0; only a local's constant size can be negative, and valid refuses it (sizes 0 to 2^31-1), while heap sizes are read at l and so never negative
ending a local is not lifetime_step's freeRuntime.v's region_step lets any live object end, of any kind; the axioms' lifetime_step speaks of the runtime's free, which empties only heap objects
From Stdlib Require Import String ZArith List Bool Lia Relations
From Nanofil Require Import Term Syntax Values Memory Ops Semantics Runtime
Import ListNotations
Open Scope Z_scope

Case analysis

A tactic: split on every match in the hypothesis H whose scrutinee names no bound variable, outermost first, dropping the cases where H's computation gives no result or another one.

33Ltac cases H ≔
repeat match type of H withcontext [match ?x with _ ⇒ _ end]⇒destruct x eqn :? ; cbv beta iota zeta in H ; try discriminate Hend

What the program does to memory

Leaving memory as it is is kept.

42Lemma kept_refl
∀ m
keptm m
Explore proof 2 tactics

Initial goal

⊢
∀m : mem, keptm m

intros m

m :
⊢
keptm m

split ; intros b reg′ E ; exists reg' ; auto | auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m
split ; intros b reg′ E ; exists reg' ; auto | auto

Two kept changes in a row, from m1 to m2 and m2 to m3, are one kept change.

47Lemma kept_trans
∀ m1 m2 m3
keptm1 m2
keptm2 m3
keptm1 m3
Explore proof 20 tactics

Initial goal

⊢
∀m1 m2 m3 : mem, keptm1 m2 → keptm2 m3 → keptm1 m3

intros m1 m2 m3 R12 & O12 R23 & O23

m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
⊢
keptm1 m3

split

2 open

m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
⊢
focused goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
⊢
∀a : Z, ¬in_objectm1 a → m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

–intros b reg3 E3

2 open

m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
b :
Z
reg3 :
E3 :
object_regionb m_regionsm3 = Somereg3
⊢
∃reg : region, object_regionb m_regionsm1 = Somereg ∧ reg3 = reg ∨ r_lifereg = Live ∧ reg3 = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg; r_life ≔ Freed
deferred goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
⊢
∀a : Z, ¬in_objectm1 a → m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

destruct R23_ _ E3 as reg2 & E2 & H23

2 open

m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
b :
Z
reg3 :
E3 :
object_regionb m_regionsm3 = Somereg3
reg2 :
E2 :
object_regionb m_regionsm2 = Somereg2
H23 :
reg3 = reg2 ∨ r_lifereg2 = Live ∧ reg3 = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg2; r_life ≔ Freed
⊢
∃reg : region, object_regionb m_regionsm1 = Somereg ∧ reg3 = reg ∨ r_lifereg = Live ∧ reg3 = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg; r_life ≔ Freed
deferred goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
⊢
∀a : Z, ¬in_objectm1 a → m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

destruct R12_ _ E2 as reg1 & E1 & H12

2 open

m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
b :
Z
reg3 :
E3 :
object_regionb m_regionsm3 = Somereg3
reg2 :
E2 :
object_regionb m_regionsm2 = Somereg2
H23 :
reg3 = reg2 ∨ r_lifereg2 = Live ∧ reg3 = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg2; r_life ≔ Freed
reg1 :
E1 :
object_regionb m_regionsm1 = Somereg1
H12 :
reg2 = reg1 ∨ r_lifereg1 = Live ∧ reg2 = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg1; r_life ≔ Freed
⊢
∃reg : region, object_regionb m_regionsm1 = Somereg ∧ reg3 = reg ∨ r_lifereg = Live ∧ reg3 = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg; r_life ≔ Freed
deferred goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
⊢
∀a : Z, ¬in_objectm1 a → m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

exists reg1

2 open

m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
b :
Z
reg3 :
E3 :
object_regionb m_regionsm3 = Somereg3
reg2 :
E2 :
object_regionb m_regionsm2 = Somereg2
H23 :
reg3 = reg2 ∨ r_lifereg2 = Live ∧ reg3 = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg2; r_life ≔ Freed
reg1 :
E1 :
object_regionb m_regionsm1 = Somereg1
H12 :
reg2 = reg1 ∨ r_lifereg1 = Live ∧ reg2 = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg1; r_life ≔ Freed
⊢
object_regionb m_regionsm1 = Somereg1 ∧ reg3 = reg1 ∨ r_lifereg1 = Live ∧ reg3 = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg1; r_life ≔ Freed
deferred goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
⊢
∀a : Z, ¬in_objectm1 a → m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

split ; auto

2 open

m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
b :
Z
reg3 :
E3 :
object_regionb m_regionsm3 = Somereg3
reg2 :
E2 :
object_regionb m_regionsm2 = Somereg2
H23 :
reg3 = reg2 ∨ r_lifereg2 = Live ∧ reg3 = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg2; r_life ≔ Freed
reg1 :
E1 :
object_regionb m_regionsm1 = Somereg1
H12 :
reg2 = reg1 ∨ r_lifereg1 = Live ∧ reg2 = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg1; r_life ≔ Freed
⊢
reg3 = reg1 ∨ r_lifereg1 = Live ∧ reg3 = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg1; r_life ≔ Freed
deferred goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
⊢
∀a : Z, ¬in_objectm1 a → m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

destruct H23 as → | L2 & → ; destruct H12 as → | L1 & → ; auto

deferred goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
⊢
∀a : Z, ¬in_objectm1 a → m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

–intros a Hn

m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
⊢
m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

assert Hn2 : ¬in_objectm2 a

2 open

m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
⊢
¬in_objectm2 a
focused goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
Hn2 :
¬in_objectm2 a
⊢
m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

{intros b & reg2 & E2 & Hr

2 open

m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
b :
Z
reg2 :
E2 :
object_regionb m_regionsm2 = Somereg2
Hr :
b ≤ a < r_endreg2
⊢
False
deferred goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
Hn2 :
¬in_objectm2 a
⊢
m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

destruct R12_ _ E2 as reg1 & E1 & → | _ & →

3 open

m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
b :
Z
reg1 :
Hr :
b ≤ a < r_endreg1
E2 :
object_regionb m_regionsm2 = Somereg1
E1 :
object_regionb m_regionsm1 = Somereg1
⊢
False
focused goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
b :
Z
reg1 :
Hr :
b ≤ a < r_endr_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg1; r_life ≔ Freed
E2 :
object_regionb m_regionsm2 = Somer_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg1; r_life ≔ Freed
E1 :
object_regionb m_regionsm1 = Somereg1
⊢
False
deferred goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
Hn2 :
¬in_objectm2 a
⊢
m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

–apply Hn

3 open

m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
b :
Z
reg1 :
Hr :
b ≤ a < r_endreg1
E2 :
object_regionb m_regionsm2 = Somereg1
E1 :
object_regionb m_regionsm1 = Somereg1
⊢
deferred goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
b :
Z
reg1 :
Hr :
b ≤ a < r_endr_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg1; r_life ≔ Freed
E2 :
object_regionb m_regionsm2 = Somer_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg1; r_life ≔ Freed
E1 :
object_regionb m_regionsm1 = Somereg1
⊢
False
deferred goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
Hn2 :
¬in_objectm2 a
⊢
m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

exists b, reg1

3 open

m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
b :
Z
reg1 :
Hr :
b ≤ a < r_endreg1
E2 :
object_regionb m_regionsm2 = Somereg1
E1 :
object_regionb m_regionsm1 = Somereg1
⊢
object_regionb m_regionsm1 = Somereg1 ∧ b ≤ a < r_endreg1
deferred goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
b :
Z
reg1 :
Hr :
b ≤ a < r_endr_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg1; r_life ≔ Freed
E2 :
object_regionb m_regionsm2 = Somer_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg1; r_life ≔ Freed
E1 :
object_regionb m_regionsm1 = Somereg1
⊢
False
deferred goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
Hn2 :
¬in_objectm2 a
⊢
m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

auto

2 open

deferred goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
b :
Z
reg1 :
Hr :
b ≤ a < r_endr_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg1; r_life ≔ Freed
E2 :
object_regionb m_regionsm2 = Somer_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg1; r_life ≔ Freed
E1 :
object_regionb m_regionsm1 = Somereg1
⊢
False
deferred goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
Hn2 :
¬in_objectm2 a
⊢
m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

–simpl in Hr

2 open

m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
b :
Z
reg1 :
Hr :
b ≤ a < b
E2 :
object_regionb m_regionsm2 = Somer_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg1; r_life ≔ Freed
E1 :
object_regionb m_regionsm1 = Somereg1
⊢
False
deferred goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
Hn2 :
¬in_objectm2 a
⊢
m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

lia

deferred goal
m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
Hn2 :
¬in_objectm2 a
⊢
m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

destruct O12a Hn as B1 A1

m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
Hn2 :
¬in_objectm2 a
B1 :
m_bytesm2 a = m_bytesm1 a
A1 :
m_auxm2 a = m_auxm1 a
⊢
m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

destruct O23a Hn2 as B2 A2

m1, m2, m3 :
R12 :
O12 :
∀a : Z, ¬in_objectm1 a → m_bytesm2 a = m_bytesm1 a ∧ m_auxm2 a = m_auxm1 a
R23 :
O23 :
∀a : Z, ¬in_objectm2 a → m_bytesm3 a = m_bytesm2 a ∧ m_auxm3 a = m_auxm2 a
a :
Z
Hn :
¬in_objectm1 a
Hn2 :
¬in_objectm2 a
B1 :
m_bytesm2 a = m_bytesm1 a
A1 :
m_auxm2 a = m_auxm1 a
B2 :
m_bytesm3 a = m_bytesm2 a
A2 :
m_auxm3 a = m_auxm2 a
⊢
m_bytesm3 a = m_bytesm1 a ∧ m_auxm3 a = m_auxm1 a

split ; congruence

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m1 m2 m3 R12 & O12 R23 & O23
split
–intros b reg3 E3
destruct R23_ _ E3 as reg2 & E2 & H23
destruct R12_ _ E2 as reg1 & E1 & H12
exists reg1
split ; auto
destruct H23 as → | L2 & → ; destruct H12 as → | L1 & → ; auto
–intros a Hn
assert Hn2 : ¬in_objectm2 a
{intros b & reg2 & E2 & Hr
destruct R12_ _ E2 as reg1 & E1 & → | _ & →
–apply Hn
exists b, reg1
auto
–simpl in Hr
lia
destruct O12a Hn as B1 A1
destruct O23a Hn2 as B2 A2
split ; congruence

A change the runtime's free may make (lifetime_step) is one the program may make (region_step): it ends only live objects.

62Lemma lifetime_region_step
∀ m m′
Explore proof 5 tactics

Initial goal

⊢
∀m m′ : mem, lifetime_stepm m′ → region_stepm m′

intros m m′ H b reg′ E

m, m′ :
H :
b :
Z
reg′ :
E :
object_regionb m_regionsm′ = Somereg′
⊢
∃reg : region, object_regionb m_regionsm = Somereg ∧ reg′ = reg ∨ r_lifereg = Live ∧ reg′ = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg; r_life ≔ Freed

destruct H_ _ E as reg & E0 & → | Hk & Hl & → ; exists reg ; split ; auto

m, m′ :
H :
b :
Z
E :
object_regionb m_regionsm′ = Somer_base ≔ b; r_end ≔ b; r_kind ≔ Heap; r_life ≔ Freed
reg :
E0 :
Hk :
r_kindreg = Heap
Hl :
r_lifereg = Live
⊢
r_base ≔ b; r_end ≔ b; r_kind ≔ Heap; r_life ≔ Freed = reg ∨ r_lifereg = Live ∧ r_base ≔ b; r_end ≔ b; r_kind ≔ Heap; r_life ≔ Freed = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg; r_life ≔ Freed

right

m, m′ :
H :
b :
Z
E :
object_regionb m_regionsm′ = Somer_base ≔ b; r_end ≔ b; r_kind ≔ Heap; r_life ≔ Freed
reg :
E0 :
Hk :
r_kindreg = Heap
Hl :
r_lifereg = Live
⊢
r_lifereg = Live ∧ r_base ≔ b; r_end ≔ b; r_kind ≔ Heap; r_life ≔ Freed = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg; r_life ≔ Freed

rewrite Hk

m, m′ :
H :
b :
Z
E :
object_regionb m_regionsm′ = Somer_base ≔ b; r_end ≔ b; r_kind ≔ Heap; r_life ≔ Freed
reg :
E0 :
Hk :
r_kindreg = Heap
Hl :
r_lifereg = Live
⊢
r_lifereg = Live ∧ r_base ≔ b; r_end ≔ b; r_kind ≔ Heap; r_life ≔ Freed = r_base ≔ b; r_end ≔ b; r_kind ≔ Heap; r_life ≔ Freed

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m m′ H b reg′ E
destruct H_ _ E as reg & E0 & → | Hk & Hl & → ; exists reg ; split ; auto
right
rewrite Hk
auto

Every memory change the function free makes is kept: what a free that meets the lifetime and retention axioms does.

71Definition free_keepsfree : word → mem → optionresunit × mem : Prop ≔
∀x m r m′, freex m = Somer, m′ → keptm m′

A successful access check covers its bytes with one object's bounds: if the check of size bytes at a passes, every address from a up to a + size is inside an object.

77Lemma access_in
∀ m a c size r align u b
access_resm a c size r align = SomeRValu
a ≤ b < a + size
Explore proof 3 tactics

Initial goal

⊢
∀m : mem a : Z c : cap size : Z r : rights align : Z u : unit, access_resm a c size r align = SomeRValu → ∀b : Z, a ≤ b < a + size → in_objectm b

unfold access_res , cap_access_res

⊢
∀ m : mem a : Z c : cap size : Z r : rights align : Z u : unit  ,
match c with
Objbase
⇒
let* reg ≔ object_regionbase m_regionsm in
Some
base ≤? a && a + size ≤? r_endreg
→
Robase
⇒
let* reg ≔ object_regionbase m_regionsm in
Some
base ≤? a && a + size ≤? r_endreg
→
⇒
None
=
SomeRValu
→
∀b : Z, a ≤ b < a + size → in_objectm b

intros m a c size r align u H b Hb

m :
a :
Z
c :
size :
Z
align :
Z
u :
unit
H :
match c with
Objbase
⇒
let* reg ≔ object_regionbase m_regionsm in
Some
base ≤? a && a + size ≤? r_endreg
→
Robase
⇒
let* reg ≔ object_regionbase m_regionsm in
Some
base ≤? a && a + size ≤? r_endreg
→
⇒
None
=
SomeRValu
b :
Z
Hb :
a ≤ b < a + size
⊢

destruct c as | base | base | f | n ; try discriminate ; destruct object_regionbase m_regionsm as reg | eqn: E ; try discriminate ; destruct base ≤? a && a + size ≤? r_endreg eqn: Eb ; try discriminate ; apply andb_true_iff in Eb as E1 E2 ; apply Z.leb_le in E1 ; apply Z.leb_le in E2 ; exists base, reg ; split ; auto ; lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m a c size r align u H b Hb
destruct c as | base | base | f | n ; try discriminate ; destruct object_regionbase m_regionsm as reg | eqn: E ; try discriminate ; destruct base ≤? a && a + size ≤? r_endreg eqn: Eb ; try discriminate ; apply andb_true_iff in Eb as E1 E2 ; apply Z.leb_le in E1 ; apply Z.leb_le in E2 ; exists base, reg ; split ; auto ; lia

Writing size bytes at a is kept if they are all inside objects.

90Lemma store_bytes_kept
∀ m a size x
∀b, a ≤ b < a + size → in_objectm b
keptm store_bytesm a size x
Explore proof 15 tactics

Initial goal

⊢
∀m : mem a size x : Z, ∀b : Z, a ≤ b < a + size → in_objectm b → keptm store_bytesm a size x

intros m a size x Hin

m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
⊢
keptm store_bytesm a size x

split

2 open

m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
⊢
focused goal
m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
⊢
∀a0 : Z, ¬in_objectm a0 → m_bytesstore_bytesm a size x a0 = m_bytesm a0 ∧ m_auxstore_bytesm a size x a0 = m_auxm a0

–intros b reg′ E

2 open

m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
b :
Z
reg′ :
E :
object_regionb m_regionsstore_bytesm a size x = Somereg′
⊢
∃reg : region, object_regionb m_regionsm = Somereg ∧ reg′ = reg ∨ r_lifereg = Live ∧ reg′ = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg; r_life ≔ Freed
deferred goal
m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
⊢
∀a0 : Z, ¬in_objectm a0 → m_bytesstore_bytesm a size x a0 = m_bytesm a0 ∧ m_auxstore_bytesm a size x a0 = m_auxm a0

exists reg′

2 open

m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
b :
Z
reg′ :
E :
object_regionb m_regionsstore_bytesm a size x = Somereg′
⊢
object_regionb m_regionsm = Somereg′ ∧ reg′ = reg′ ∨ r_lifereg′ = Live ∧ reg′ = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg′; r_life ≔ Freed
deferred goal
m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
⊢
∀a0 : Z, ¬in_objectm a0 → m_bytesstore_bytesm a size x a0 = m_bytesm a0 ∧ m_auxstore_bytesm a size x a0 = m_auxm a0

split ; exact E | auto

deferred goal
m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
⊢
∀a0 : Z, ¬in_objectm a0 → m_bytesstore_bytesm a size x a0 = m_bytesm a0 ∧ m_auxstore_bytesm a size x a0 = m_auxm a0

–intros b Hn

m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
b :
Z
Hn :
⊢
m_bytesstore_bytesm a size x b = m_bytesm b ∧ m_auxstore_bytesm a size x b = m_auxm b

simpl

m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
b :
Z
Hn :
⊢
a ≤? b && b <? a + size
→
byte_ofx b − a
else
=
∧
m_auxm b = m_auxm b

split ; auto

m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
b :
Z
Hn :
⊢
a ≤? b && b <? a + size
→
byte_ofx b − a
else
=

destruct a ≤? b && b <? a + size eqn: E ; auto

m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
b :
Z
Hn :
E :
a ≤? b && b <? a + size = true
⊢
byte_ofx b − a = m_bytesm b

exfalso

m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
b :
Z
Hn :
E :
a ≤? b && b <? a + size = true
⊢
False

apply Hn , Hin

m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
b :
Z
Hn :
E :
a ≤? b && b <? a + size = true
⊢
a ≤ b < a + size

apply andb_true_iff in E as E1 E2

m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
b :
Z
Hn :
E1 :
a ≤? b = true
E2 :
b <? a + size = true
⊢
a ≤ b < a + size

apply Z.leb_le in E1

m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
b :
Z
Hn :
E1 :
a ≤ b
E2 :
b <? a + size = true
⊢
a ≤ b < a + size

apply Z.ltb_lt in E2

m :
a, size, x :
Z
Hin :
∀b : Z, a ≤ b < a + size → in_objectm b
b :
Z
Hn :
E1 :
a ≤ b
E2 :
b < a + size
⊢
a ≤ b < a + size

lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m a size x Hin
split
–intros b reg′ E
exists reg′
split ; exact E | auto
–intros b Hn
simpl
split ; auto
destruct a ≤? b && b <? a + size eqn: E ; auto
exfalso
apply Hn , Hin
apply andb_true_iff in E as E1 E2
apply Z.leb_le in E1
apply Z.ltb_lt in E2
lia

Storing a capability in the aux at a is kept if a is inside an object.

103Lemma store_aux_kept
∀ m a c
Explore proof 12 tactics

Initial goal

⊢
∀m : mem a : Z c : cap, in_objectm a → keptm store_auxm a c

intros m a c Hin

m :
a :
Z
c :
Hin :
⊢

split

2 open

m :
a :
Z
c :
Hin :
focused goal
m :
a :
Z
c :
Hin :
⊢
∀a0 : Z, ¬in_objectm a0 → m_bytesstore_auxm a c a0 = m_bytesm a0 ∧ m_auxstore_auxm a c a0 = m_auxm a0

–intros b reg′ E

2 open

m :
a :
Z
c :
Hin :
b :
Z
reg′ :
E :
object_regionb m_regionsstore_auxm a c = Somereg′
⊢
∃reg : region, object_regionb m_regionsm = Somereg ∧ reg′ = reg ∨ r_lifereg = Live ∧ reg′ = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg; r_life ≔ Freed
deferred goal
m :
a :
Z
c :
Hin :
⊢
∀a0 : Z, ¬in_objectm a0 → m_bytesstore_auxm a c a0 = m_bytesm a0 ∧ m_auxstore_auxm a c a0 = m_auxm a0

exists reg′

2 open

m :
a :
Z
c :
Hin :
b :
Z
reg′ :
E :
object_regionb m_regionsstore_auxm a c = Somereg′
⊢
object_regionb m_regionsm = Somereg′ ∧ reg′ = reg′ ∨ r_lifereg′ = Live ∧ reg′ = r_base ≔ b; r_end ≔ b; r_kind ≔ r_kindreg′; r_life ≔ Freed
deferred goal
m :
a :
Z
c :
Hin :
⊢
∀a0 : Z, ¬in_objectm a0 → m_bytesstore_auxm a c a0 = m_bytesm a0 ∧ m_auxstore_auxm a c a0 = m_auxm a0

split ; exact E | auto

deferred goal
m :
a :
Z
c :
Hin :
⊢
∀a0 : Z, ¬in_objectm a0 → m_bytesstore_auxm a c a0 = m_bytesm a0 ∧ m_auxstore_auxm a c a0 = m_auxm a0

–intros b Hn

m :
a :
Z
c :
Hin :
b :
Z
Hn :
⊢
m_bytesstore_auxm a c b = m_bytesm b ∧ m_auxstore_auxm a c b = m_auxm b

simpl

m :
a :
Z
c :
Hin :
b :
Z
Hn :
⊢
m_bytesm b = m_bytesm b
∧
b =? a
→
c
else
=

split ; auto

m :
a :
Z
c :
Hin :
b :
Z
Hn :
⊢
b =? a
→
c
else
=

destruct Z.eqbb a eqn: E ; auto

m :
a :
Z
c :
Hin :
b :
Z
Hn :
E :
b =? a = true
⊢
c = m_auxm b

apply Z.eqb_eq in E

m :
a :
Z
c :
Hin :
b :
Z
Hn :
E :
b = a
⊢
c = m_auxm b

subst

m :
a :
Z
c :
Hin :
Hn :
⊢
c = m_auxm a

contradiction

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m a c Hin
split
–intros b reg′ E
exists reg′
split ; exact E | auto
–intros b Hn
simpl
split ; auto
destruct Z.eqbb a eqn: E ; auto
apply Z.eqb_eq in E
subst
contradiction

Writes leave the objects where they were: an address inside an object before a byte write is inside one after it.

114Lemma in_object_store_bytes
∀ m a size x b
Explore proof 1 tactics

Initial goal

⊢
∀m : mem a size x b : Z, in_objectm b → in_objectstore_bytesm a size x b

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
auto

The same for a capability stored in the aux.

119Lemma in_object_store_aux
∀ m a c b
Explore proof 1 tactics

Initial goal

⊢
∀m : mem a : Z c : cap b : Z, in_objectm b → in_objectstore_auxm a c b

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
auto

A store as store_res/7 does it is kept: it writes the bytes, and a pointer's capability, only after its access check passed.

124Lemma store_res_kept
∀ w m a c x r m′
store_resw m a c x = Somer, m′
keptm m′
Explore proof 3 tactics

Initial goal

⊢
∀w : width m : mem a : Z c : cap x : word r : resunit m′ : mem, store_resw m a c x = Somer, m′ → keptm m′

unfold store_res

⊢
∀ w : width m : mem a : Z c : cap x : word r : resunit m′ : mem  ,
match w with
⇒
match x with
⇒
let* chk ≔ access_resm a c width_bytesw Write 8 in
Some
chk
match chk with
_
⇒
None
_
⇒
match x with
⇒
let* chk ≔
match w with
⇒
8
_
⇒
1
in
Some
chk
match chk with
_
⇒
None
=
Somer, m′
→
keptm m′

intros w m a c x r m′ H

m :
a :
Z
c :
x :
r :
resunit
m′ :
H :
match w with
⇒
match x with
⇒
let* chk ≔ access_resm a c width_bytesw Write 8 in
Some
chk
match chk with
_
⇒
None
_
⇒
match x with
⇒
let* chk ≔
match w with
⇒
8
_
⇒
1
in
Some
chk
match chk with
_
⇒
None
=
Somer, m′
⊢
keptm m′

destruct w , x ; try discriminate ; cases H ; inversion H ; subst ; try apply kept_refl;match goal withE : access_res_ _ _ _ _ _ = SomeRVal_ |- kept_ store_aux_ _ _⇒eapply kept_trans ; | apply store_aux_kept ; apply store_bytes_kept ; intros b Hb ; eapply access_in ; exact E | exact Hb | apply in_object_store_bytes ; eapply access_in ; exact E | simpl ; liaE : access_res_ _ _ _ _ _ = SomeRVal_ |- _⇒apply store_bytes_kept ; intros b Hb ; eapply access_in ; exact E | exact Hbend

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
unfold store_res
intros w m a c x r m′ H
destruct w , x ; try discriminate ; cases H ; inversion H ; subst ; try apply kept_refl;match goal withE : access_res_ _ _ _ _ _ = SomeRVal_ |- kept_ store_aux_ _ _⇒eapply kept_trans ; | apply store_aux_kept ; apply store_bytes_kept ; intros b Hb ; eapply access_in ; exact E | exact Hb | apply in_object_store_bytes ; eapply access_in ; exact E | simpl ; liaE : access_res_ _ _ _ _ _ = SomeRVal_ |- _⇒apply store_bytes_kept ; intros b Hb ; eapply access_in ; exact E | exact Hbend

A fold of memory changes that starts from no memory ends with none.

140Lemma fold_left_none
∀ A : Type f : mem → A → optionmem xs
fold_left
λ acc x  ⇒
let* m1 ≔ acc in
fm1 x
xs
None
=
None
Explore proof 2 tactics

Initial goal

⊢
∀ A : Type f : mem → A → optionmem xs : listA  ,
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
None
=
None

intros A f xs

A :
Type
f :
mem → A → optionmem
xs :
listA
⊢
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
None
=
None

induction xs ; simpl ; auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros A f xs
induction xs ; simpl ; auto

A fold of memory changes f over xs, from m0, is kept if each change is kept and keeps P, where P holds of m0.

146Lemma fold_kept
∀ A : Type P : mem → Prop f : mem → A → optionmem xs m0 m′
Pm0
∀m1 x m2, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
fold_left
λ acc x  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem0
=
Somem′
keptm0 m′
Explore proof 10 tactics

Initial goal

⊢
∀ A : Type P : mem → Prop f : mem → A → optionmem xs : listA m0 m′ : mem  ,
Pm0
→
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
→
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem0
=
Somem′
→
keptm0 m′

intros A P f xs

A :
Type
P :
mem → Prop
f :
mem → A → optionmem
xs :
listA
⊢
∀ m0 m′ : mem  ,
Pm0
→
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
→
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem0
=
Somem′
→
keptm0 m′

induction xs as | x xs IH ; simpl ; intros m0 m′ H0 Hf H

2 open

A :
Type
P :
mem → Prop
f :
mem → A → optionmem
m0, m′ :
H0 :
Pm0
Hf :
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
H :
Somem0 = Somem′
⊢
keptm0 m′
focused goal
A :
Type
P :
mem → Prop
f :
mem → A → optionmem
x :
A
xs :
listA
IH :
∀ m0 m′ : mem  ,
Pm0
→
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
→
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem0
=
Somem′
→
keptm0 m′
m0, m′ :
H0 :
Pm0
Hf :
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
H :
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
fm0 x
=
Somem′
⊢
keptm0 m′

–inversion H ; subst

2 open

A :
Type
P :
mem → Prop
f :
mem → A → optionmem
m′ :
H0 :
Pm′
Hf :
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
H :
Somem′ = Somem′
⊢
keptm′ m′
deferred goal
A :
Type
P :
mem → Prop
f :
mem → A → optionmem
x :
A
xs :
listA
IH :
∀ m0 m′ : mem  ,
Pm0
→
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
→
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem0
=
Somem′
→
keptm0 m′
m0, m′ :
H0 :
Pm0
Hf :
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
H :
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
fm0 x
=
Somem′
⊢
keptm0 m′

apply kept_refl

deferred goal
A :
Type
P :
mem → Prop
f :
mem → A → optionmem
x :
A
xs :
listA
IH :
∀ m0 m′ : mem  ,
Pm0
→
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
→
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem0
=
Somem′
→
keptm0 m′
m0, m′ :
H0 :
Pm0
Hf :
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
H :
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
fm0 x
=
Somem′
⊢
keptm0 m′

–destruct fm0 x as m1 | eqn: E

2 open

A :
Type
P :
mem → Prop
f :
mem → A → optionmem
x :
A
xs :
listA
IH :
∀ m0 m′ : mem  ,
Pm0
→
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
→
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem0
=
Somem′
→
keptm0 m′
m0, m′ :
H0 :
Pm0
Hf :
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
m1 :
E :
fm0 x = Somem1
H :
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem1
=
Somem′
⊢
keptm0 m′
focused goal
A :
Type
P :
mem → Prop
f :
mem → A → optionmem
x :
A
xs :
listA
IH :
∀ m0 m′ : mem  ,
Pm0
→
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
→
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem0
=
Somem′
→
keptm0 m′
m0, m′ :
H0 :
Pm0
Hf :
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
E :
fm0 x = None
H :
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
None
=
Somem′
⊢
keptm0 m′

+destruct Hf_ _ _ H0 E as H1 K1

2 open

A :
Type
P :
mem → Prop
f :
mem → A → optionmem
x :
A
xs :
listA
IH :
∀ m0 m′ : mem  ,
Pm0
→
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
→
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem0
=
Somem′
→
keptm0 m′
m0, m′ :
H0 :
Pm0
Hf :
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
m1 :
E :
fm0 x = Somem1
H :
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem1
=
Somem′
H1 :
Pm1
K1 :
keptm0 m1
⊢
keptm0 m′
deferred goal
A :
Type
P :
mem → Prop
f :
mem → A → optionmem
x :
A
xs :
listA
IH :
∀ m0 m′ : mem  ,
Pm0
→
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
→
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem0
=
Somem′
→
keptm0 m′
m0, m′ :
H0 :
Pm0
Hf :
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
E :
fm0 x = None
H :
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
None
=
Somem′
⊢
keptm0 m′

eapply kept_trans ; exact K1 |

2 open

A :
Type
P :
mem → Prop
f :
mem → A → optionmem
x :
A
xs :
listA
IH :
∀ m0 m′ : mem  ,
Pm0
→
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
→
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem0
=
Somem′
→
keptm0 m′
m0, m′ :
H0 :
Pm0
Hf :
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
m1 :
E :
fm0 x = Somem1
H :
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem1
=
Somem′
H1 :
Pm1
K1 :
keptm0 m1
⊢
keptm1 m′
deferred goal
A :
Type
P :
mem → Prop
f :
mem → A → optionmem
x :
A
xs :
listA
IH :
∀ m0 m′ : mem  ,
Pm0
→
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
→
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem0
=
Somem′
→
keptm0 m′
m0, m′ :
H0 :
Pm0
Hf :
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
E :
fm0 x = None
H :
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
None
=
Somem′
⊢
keptm0 m′

eapply IH ; eauto

deferred goal
A :
Type
P :
mem → Prop
f :
mem → A → optionmem
x :
A
xs :
listA
IH :
∀ m0 m′ : mem  ,
Pm0
→
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
→
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem0
=
Somem′
→
keptm0 m′
m0, m′ :
H0 :
Pm0
Hf :
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
E :
fm0 x = None
H :
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
None
=
Somem′
⊢
keptm0 m′

+rewrite fold_left_none in H

A :
Type
P :
mem → Prop
f :
mem → A → optionmem
x :
A
xs :
listA
IH :
∀ m0 m′ : mem  ,
Pm0
→
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
→
fold_left
λ acc : optionmem x : A  ⇒
let* m1 ≔ acc in
fm1 x
xs
Somem0
=
Somem′
→
keptm0 m′
m0, m′ :
H0 :
Pm0
Hf :
∀m1 : mem x : A m2 : mem, Pm1 → fm1 x = Somem2 → Pm2 ∧ keptm1 m2
E :
fm0 x = None
H :
None = Somem′
⊢
keptm0 m′

discriminate

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros A P f xs
induction xs as | x xs IH ; simpl ; intros m0 m′ H0 Hf H
–inversion H ; subst
apply kept_refl
–destruct fm0 x as m1 | eqn: E
+destruct Hf_ _ _ H0 E as H1 K1
eapply kept_trans ; exact K1 |
eapply IH ; eauto
+rewrite fold_left_none in H
discriminate

A pointer store's effects es (pointer_store_effects/4) at the address a are kept, if the access check of its 8 bytes passed.

161Lemma pointer_store_effects_kept
∀ a x m es m′
∀b, a ≤ b < a + 8 → in_objectm b
pointer_store_effectsa x m es = Somem′
keptm m′
Explore proof 20 tactics

Initial goal

⊢
∀a : Z x : ptr m : mem es : listeffect m′ : mem, ∀b : Z, a ≤ b < a + 8 → in_objectm b → pointer_store_effectsa x m es = Somem′ → keptm m′

intros a x m es m′ Hin H

a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
⊢
keptm m′

apply fold_kepteffect λm1 ⇒ m_regionsm1 = m_regionsm pointer_store_effecta x es m m′ ; auto

a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
⊢
∀m1 : mem x0 : effect m2 : mem, m_regionsm1 = m_regionsm → pointer_store_effecta x m1 x0 = Somem2 → m_regionsm2 = m_regionsm ∧ keptm1 m2

intros m1 e m2 Hr E

a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
m2 :
E :
pointer_store_effecta x m1 e = Somem2
⊢
m_regionsm2 = m_regionsm ∧ keptm1 m2

assert Hin1 : ∀b, a ≤ b < a + 8 → in_objectm1 b

2 open

a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
m2 :
E :
pointer_store_effecta x m1 e = Somem2
⊢
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
focused goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
m2 :
E :
pointer_store_effecta x m1 e = Somem2
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
⊢
m_regionsm2 = m_regionsm ∧ keptm1 m2

{intros b Hb

2 open

a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
m2 :
E :
pointer_store_effecta x m1 e = Somem2
b :
Z
Hb :
a ≤ b < a + 8
⊢
deferred goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
m2 :
E :
pointer_store_effecta x m1 e = Somem2
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
⊢
m_regionsm2 = m_regionsm ∧ keptm1 m2

unfold in_object

2 open

a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
m2 :
E :
pointer_store_effecta x m1 e = Somem2
b :
Z
Hb :
a ≤ b < a + 8
⊢
∃b0 : Z reg : region, object_regionb0 m_regionsm1 = Somereg ∧ b0 ≤ b < r_endreg
deferred goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
m2 :
E :
pointer_store_effecta x m1 e = Somem2
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
⊢
m_regionsm2 = m_regionsm ∧ keptm1 m2

rewrite Hr

2 open

a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
m2 :
E :
pointer_store_effecta x m1 e = Somem2
b :
Z
Hb :
a ≤ b < a + 8
⊢
∃b0 : Z reg : region, object_regionb0 m_regionsm = Somereg ∧ b0 ≤ b < r_endreg
deferred goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
m2 :
E :
pointer_store_effecta x m1 e = Somem2
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
⊢
m_regionsm2 = m_regionsm ∧ keptm1 m2

apply Hin

2 open

a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
m2 :
E :
pointer_store_effecta x m1 e = Somem2
b :
Z
Hb :
a ≤ b < a + 8
⊢
a ≤ b < a + 8
deferred goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
m2 :
E :
pointer_store_effecta x m1 e = Somem2
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
⊢
m_regionsm2 = m_regionsm ∧ keptm1 m2

auto

deferred goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
m2 :
E :
pointer_store_effecta x m1 e = Somem2
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
⊢
m_regionsm2 = m_regionsm ∧ keptm1 m2

destruct e ; simpl in E ; try discriminate ; inversion E ; subst ; split ; auto using kept_refl

3 open

a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
E :
Somestore_auxm1 a ptr_capx = Somestore_auxm1 a ptr_capx
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
focused goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
E :
Somestore_bytesm1 a 8 ptr_addrx = Somestore_bytesm1 a 8 ptr_addrx
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
focused goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b

–apply store_aux_kept , Hin1

3 open

a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
E :
Somestore_auxm1 a ptr_capx = Somestore_auxm1 a ptr_capx
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
⊢
a ≤ a < a + 8
deferred goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
E :
Somestore_bytesm1 a 8 ptr_addrx = Somestore_bytesm1 a 8 ptr_addrx
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
deferred goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b

lia

2 open

deferred goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
E :
Somestore_bytesm1 a 8 ptr_addrx = Somestore_bytesm1 a 8 ptr_addrx
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
deferred goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b

–apply store_bytes_kept

2 open

a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
E :
Somestore_bytesm1 a 8 ptr_addrx = Somestore_bytesm1 a 8 ptr_addrx
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
⊢
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
deferred goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b

exact Hin1

deferred goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b

–eapply kept_trans ; | apply store_bytes_kept

2 open

a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
focused goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
⊢
∀b : Z, a ≤ b < a + 8 → in_objectstore_auxm1 a ptr_capx b

+apply store_aux_kept , Hin1

2 open

a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
⊢
a ≤ a < a + 8
deferred goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
⊢
∀b : Z, a ≤ b < a + 8 → in_objectstore_auxm1 a ptr_capx b

lia

deferred goal
a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
⊢
∀b : Z, a ≤ b < a + 8 → in_objectstore_auxm1 a ptr_capx b

+intros b Hb

a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
b :
Z
Hb :
a ≤ b < a + 8

apply in_object_store_aux , Hin1

a :
Z
x :
m :
es :
listeffect
m′ :
Hin :
∀b : Z, a ≤ b < a + 8 → in_objectm b
H :
pointer_store_effectsa x m es = Somem′
m1 :
Hin1 :
∀b : Z, a ≤ b < a + 8 → in_objectm1 b
b :
Z
Hb :
a ≤ b < a + 8
⊢
a ≤ b < a + 8

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros a x m es m′ Hin H
apply fold_kepteffect λm1 ⇒ m_regionsm1 = m_regionsm pointer_store_effecta x es m m′ ; auto
intros m1 e m2 Hr E
assert Hin1 : ∀b, a ≤ b < a + 8 → in_objectm1 b
{intros b Hb
unfold in_object
rewrite Hr
apply Hin
auto
destruct e ; simpl in E ; try discriminate ; inversion E ; subst ; split ; auto using kept_refl
–apply store_aux_kept , Hin1
lia
exact Hin1
–eapply kept_trans ; | apply store_bytes_kept
+apply store_aux_kept , Hin1
lia
+intros b Hb
apply in_object_store_aux , Hin1
auto

Reading a variadic argument (va_arg_res/4) is kept: its one write is a checked store.

181Lemma va_arg_res_kept
∀ k p m r m′
va_arg_resk p m = Somer, m′
keptm m′
Explore proof 3 tactics

Initial goal

⊢
∀k : class p : ptr m : mem r : resword m′ : mem, va_arg_resk p m = Somer, m′ → keptm m′

unfold va_arg_res

⊢
∀ k : class p : ptr m : mem r : resword m′ : mem  ,
match access_resm ptr_addrp ptr_capp 8 Read 8 with
SomeRVal_
⇒
match va_cellk with
Somestep, align
⇒
let* w ≔ class_widthk in
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
⇒
SomeRValWPtrptr_addr ≔ load_bytesm1 ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align 8; ptr_cap ≔ aux_atm1 ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align, m1
_
⇒
SomeRValWIntload_bytesm1 ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align width_bytesw, m1
SomeRTrapwhy, m1
⇒
SomeRTrapwhy, m1
_
⇒
None
SomeRTrapwhy
⇒
SomeRTrapwhy, m
_
⇒
None
None
⇒
None
SomeRTrapwhy
⇒
SomeRTrapwhy, m
_
⇒
None
=
Somer, m′
→
keptm m′

intros k p m r m′ H

p :
m :
m′ :
H :
match access_resm ptr_addrp ptr_capp 8 Read 8 with
SomeRVal_
⇒
match va_cellk with
Somestep, align
⇒
let* w ≔ class_widthk in
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
⇒
SomeRValWPtrptr_addr ≔ load_bytesm1 ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align 8; ptr_cap ≔ aux_atm1 ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align, m1
_
⇒
SomeRValWIntload_bytesm1 ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align width_bytesw, m1
SomeRTrapwhy, m1
⇒
SomeRTrapwhy, m1
_
⇒
None
SomeRTrapwhy
⇒
SomeRTrapwhy, m
_
⇒
None
None
⇒
None
SomeRTrapwhy
⇒
SomeRTrapwhy, m
_
⇒
None
=
Somer, m′
⊢
keptm m′

cases H;match type of H withSome_, ?x = Some_, ?y⇒assert x = y as ← by congruenceend;first|apply kept_refl|match goal withE : store_res_ _ _ _ _ = Some_ |- _⇒exact store_res_kept_ _ _ _ _ _ _ Eend

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_, ?x = Some_, ?y⇒assert x = y as ← by congruenceend;first|apply kept_refl|match goal withE : store_res_ _ _ _ _ = Some_ |- _⇒exact store_res_kept_ _ _ _ _ _ _ Eend

congruence, not inversion: inversion takes seconds over the loaded words' arithmetic

An op changes memory only by va_arg: an integer op leaves it as it is.

193Lemma op_res_int_mem
∀ o k xs m r m′
op_res_into k xs m = SomeOpResr m′
m′ = m
Explore proof 3 tactics

Initial goal

⊢
∀o : op k : class xs : listword m : mem r : resword m′ : mem, op_res_into k xs m = SomeOpResr m′ → m′ = m

unfold op_res_int

⊢
∀ o : op k : class xs : listword m : mem r : resword m′ : mem  ,
match o with
⇒
let* w ≔ additive_resk o xs in
SomeOpResRValw m
Allocalign
⇒
match xs with
WIntsize
⇒
else
SomeOpAllocheap_reqalign size λbase : Z ⇒ WPtrptr_addr ≔ base; ptr_cap ≔ Objbase, allocatedm heap_reqalign size base
WIntsize :: _ :: _
⇒
None
_
⇒
None
Checklo hi r0 al
⇒
match k with
⇒
match xs with
⇒
let* chk ≔ access_resm raw_addressptr_addrp lo ptr_capp hi − lo r0 al in
WPtrp :: _ :: _
⇒
None
_
⇒
None
_
⇒
None
CheckAheadlo hi r0 al ahi
⇒
match k with
⇒
match xs with
⇒
match access_resm raw_addressptr_addrp lo ptr_capp ahi − lo r0 al with
SomeRTrapwhy
⇒
SomeOpResRTrapwhy m
None
⇒
None
_
⇒
match access_resm raw_addressptr_addrp lo ptr_capp hi − lo r0 al with
SomeRTrapwhy
⇒
None
⇒
None
_
⇒
WPtrp :: _ :: _
⇒
None
_
⇒
None
_
⇒
None
Renewlo hi r0 al
⇒
match k with
⇒
match xs with
[ ]
⇒
None
q1
⇒
None
q1; x
⇒
match q1 with
⇒
match x with
⇒
→
let* chk ≔ access_resm raw_addressptr_addrp lo ptr_capp hi − lo r0 al in
let* r′ ≔ renew_reschk p m in
SomeOpResr′ m
q1 :: x :: _ :: _
⇒
None
_
⇒
None
RenewHulllo hi r0 al
⇒
match k with
⇒
match xs with
[ ]
⇒
None
ql
⇒
None
ql; qh
⇒
None
ql; qh; x
⇒
match ql with
⇒
match qh with
⇒
match x with
⇒
→
let* chk ≔ access_resm raw_addressptr_addrp lo ptr_capp hi − lo r0 al in
let* r′ ≔ renew_reschk p m in
SomeOpResr′ m
ql :: qh :: x :: _ :: _
⇒
None
_
⇒
None
HalfCheckbd lo hi r0 al
⇒
match k with
⇒
match xs with
[ ]
⇒
None
q1
⇒
None
q1; x
⇒
match q1 with
⇒
match x with
⇒
→
let* chk ≔ access_resm raw_addressptr_addrp lo ptr_capp hi − lo r0 al in
match half_passesbd m raw_addressptr_addrp lo hi − lo ptr_capp r0 al with
SomeSomeok′
⇒
SomeOpReshalf_reschk ok′ WPtrp m
SomeNone
⇒
None
⇒
None
q1 :: x :: _ :: _
⇒
None
_
⇒
None
⇒
match k with
⇒
match xs with
⇒
match ptr_capp with
Objbase | Robase
⇒
let* reg ≔ object_regionbase m_regionsm in
Some
_
⇒
WPtrp :: _ :: _
⇒
None
_
⇒
None
_
⇒
None
RenewIflo hi r0 al
⇒
match k with
⇒
match xs with
⇒
let* chk ≔ access_resm raw_addressptr_addrp lo ptr_capp hi − lo r0 al in
g =? 0
→
else
match chk with
_
⇒
let* r′ ≔ renew_reschk p m in
SomeOpResr′ m
WPtrp :: WIntg :: _ :: _
⇒
None
WPtrp | WPtrp :: WPtr_ :: _ | WPtrp :: WLimit_ _ :: _
⇒
None
_
⇒
None
_
⇒
None
Limitsize
⇒
match k with
⇒
match xs with
WPtrp :: _ :: _
⇒
None
_
⇒
None
_
⇒
None
CheckLimitlo hi r0 al
⇒
match k with
⇒
match xs with
⇒
None
WPtrp; u
⇒
match u with
WLimitc size
⇒
cap_eqbc ptr_capp && size =? hi − lo
→
let* chk ≔ access_resm raw_addressptr_addrp lo ptr_capp hi − lo r0 al in
WPtrp :: u :: _ :: _
⇒
None
_
⇒
None
_
⇒
None
RawLoadt off
⇒
match xs with
⇒
let* r0 ≔ int_load_rest k m raw_addressptr_addrp off ptr_capp in
SomeOpResraw_resr0 m
WPtrp :: _ :: _
⇒
None
_
⇒
None
⇒
match k with
⇒
match xs with
⇒
SomeRVal_
⇒
SomeRTrapwhy | SomeRUncheckedwhy
⇒
None
⇒
None
WPtrp :: _ :: _
⇒
None
_
⇒
None
_
⇒
None
⇒
None
_
⇒
let* w ≔ aluo k xs in
SomeOpResRValw m
=
SomeOpResr m′
→
m′ = m

intros o k xs m r m′ H

o :
xs :
listword
m :
m′ :
H :
match o with
⇒
let* w ≔ additive_resk o xs in
SomeOpResRValw m
Allocalign
⇒
match xs with
WIntsize
⇒
else
SomeOpAllocheap_reqalign size λbase : Z ⇒ WPtrptr_addr ≔ base; ptr_cap ≔ Objbase, allocatedm heap_reqalign size base
WIntsize :: _ :: _
⇒
None
_
⇒
None
Checklo hi r al
⇒
match k with
⇒
match xs with
⇒
let* chk ≔ access_resm raw_addressptr_addrp lo ptr_capp hi − lo r al in
WPtrp :: _ :: _
⇒
None
_
⇒
None
_
⇒
None
CheckAheadlo hi r al ahi
⇒
match k with
⇒
match xs with
⇒
match access_resm raw_addressptr_addrp lo ptr_capp ahi − lo r al with
SomeRTrapwhy
⇒
SomeOpResRTrapwhy m
None
⇒
None
_
⇒
match access_resm raw_addressptr_addrp lo ptr_capp hi − lo r al with
SomeRTrapwhy
⇒
None
⇒
None
_
⇒
WPtrp :: _ :: _
⇒
None
_
⇒
None
_
⇒
None
Renewlo hi r al
⇒
match k with
⇒
match xs with
[ ]
⇒
None
q1
⇒
None
q1; x
⇒
match q1 with
⇒
match x with
⇒
→
let* chk ≔ access_resm raw_addressptr_addrp lo ptr_capp hi − lo r al in
let* r′ ≔ renew_reschk p m in
SomeOpResr′ m
q1 :: x :: _ :: _
⇒
None
_
⇒
None
RenewHulllo hi r al
⇒
match k with
⇒
match xs with
[ ]
⇒
None
ql
⇒
None
ql; qh
⇒
None
ql; qh; x
⇒
match ql with
⇒
match qh with
⇒
match x with
⇒
→
let* chk ≔ access_resm raw_addressptr_addrp lo ptr_capp hi − lo r al in
let* r′ ≔ renew_reschk p m in
SomeOpResr′ m
ql :: qh :: x :: _ :: _
⇒
None
_
⇒
None
HalfCheckbd lo hi r al
⇒
match k with
⇒
match xs with
[ ]
⇒
None
q1
⇒
None
q1; x
⇒
match q1 with
⇒
match x with
⇒
→
let* chk ≔ access_resm raw_addressptr_addrp lo ptr_capp hi − lo r al in
match half_passesbd m raw_addressptr_addrp lo hi − lo ptr_capp r al with
SomeSomeok′
⇒
SomeOpReshalf_reschk ok′ WPtrp m
SomeNone
⇒
None
⇒
None
q1 :: x :: _ :: _
⇒
None
_
⇒
None
⇒
match k with
⇒
match xs with
⇒
match ptr_capp with
Objbase | Robase
⇒
let* reg ≔ object_regionbase m_regionsm in
Some
_
⇒
WPtrp :: _ :: _
⇒
None
_
⇒
None
_
⇒
None
RenewIflo hi r al
⇒
match k with
⇒
match xs with
⇒
let* chk ≔ access_resm raw_addressptr_addrp lo ptr_capp hi − lo r al in
g =? 0
→
else
match chk with
_
⇒
let* r′ ≔ renew_reschk p m in
SomeOpResr′ m
WPtrp :: WIntg :: _ :: _
⇒
None
WPtrp | WPtrp :: WPtr_ :: _ | WPtrp :: WLimit_ _ :: _
⇒
None
_
⇒
None
_
⇒
None
Limitsize
⇒
match k with
⇒
match xs with
WPtrp :: _ :: _
⇒
None
_
⇒
None
_
⇒
None
CheckLimitlo hi r al
⇒
match k with
⇒
match xs with
⇒
None
WPtrp; u
⇒
match u with
WLimitc size
⇒
cap_eqbc ptr_capp && size =? hi − lo
→
let* chk ≔ access_resm raw_addressptr_addrp lo ptr_capp hi − lo r al in
WPtrp :: u :: _ :: _
⇒
None
_
⇒
None
_
⇒
None
RawLoadt off
⇒
match xs with
⇒
let* r ≔ int_load_rest k m raw_addressptr_addrp off ptr_capp in
WPtrp :: _ :: _
⇒
None
_
⇒
None
⇒
match k with
⇒
match xs with
⇒
SomeRVal_
⇒
SomeRTrapwhy | SomeRUncheckedwhy
⇒
None
⇒
None
WPtrp :: _ :: _
⇒
None
_
⇒
None
_
⇒
None
⇒
None
_
⇒
let* w ≔ aluo k xs in
SomeOpResRValw m
=
SomeOpResr m′
⊢
m′ = m

destruct o ; cases H ; inversion H ; auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
unfold op_res_int
intros o k xs m r m′ H
destruct o ; cases H ; inversion H ; auto

An op that gives a result changes memory as kept allows.

199Lemma op_res_kept
∀ o k xs m r m′
op_reso k xs m = SomeOpResr m′
keptm m′
Explore proof 3 tactics

Initial goal

⊢
∀o : op k : class xs : listword m : mem r : resword m′ : mem, op_reso k xs m = SomeOpResr m′ → keptm m′

unfold op_res , float_integer

⊢
∀ o : op k : class xs : listword m : mem r : resword m′ : mem  ,
match o with
Add | Sub | Mul | Div | Neg | Copy
⇒
match fmt_ofk with
Somef
⇒
let* r0 ≔ float_arithmetico f xs in
None
⇒
op_res_into k xs m
Cmpc ck
⇒
match xs with
⇒
match fmt_ofck with
Somef
⇒
None
⇒
op_res_into k xs m
WInta :: WIntb :: _ :: _
⇒
match fmt_ofck with
Some_
⇒
None
None
⇒
op_res_into k xs m
WInta | WInta :: WPtr_ :: _ | WInta :: WLimit_ _ :: _
⇒
match fmt_ofck with
Some_
⇒
None
None
⇒
op_res_into k xs m
_
⇒
match fmt_ofck with
Some_
⇒
None
None
⇒
op_res_into k xs m
⇒
match xs with
⇒
let* from ≔ fmt_offk in
let* m0 ≔ modulusk in
let 'lo, hi ≔
match sg with
⇒
−m0 / 2, m0 / 2 − 1
⇒
0, m0 − 1
in
match Ieee.ieee_to_intfrom x with
Somen
⇒
lo ≤? n && n ≤? hi
→
SomeOpResRValWIntn mod m0 m
else
SomeOpUBTAtom"float_conversion"
None
⇒
SomeOpUBTAtom"float_conversion"
WIntx :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
⇒
match fmt_ofk with
Somef
⇒
match xs with
⇒
let* n ≔ integer_sourceik sg x in
WIntx :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
None
⇒
op_res_into k xs m
⇒
match xs with
WIntx :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
⇒
match xs with
⇒
let* r0 ≔ float_converto k x in
WIntx :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
⇒
match xs with
⇒
let* rm ≔ va_arg_resk p m in
SomeOpResfstrm sndrm
WPtrp :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
=
SomeOpResr m′
→
keptm m′

intros o k xs m r m′ H

o :
xs :
listword
m :
m′ :
H :
match o with
Add | Sub | Mul | Div | Neg | Copy
⇒
match fmt_ofk with
Somef
⇒
let* r ≔ float_arithmetico f xs in
None
⇒
op_res_into k xs m
Cmpc ck
⇒
match xs with
⇒
match fmt_ofck with
Somef
⇒
None
⇒
op_res_into k xs m
WInta :: WIntb :: _ :: _
⇒
match fmt_ofck with
Some_
⇒
None
None
⇒
op_res_into k xs m
WInta | WInta :: WPtr_ :: _ | WInta :: WLimit_ _ :: _
⇒
match fmt_ofck with
Some_
⇒
None
None
⇒
op_res_into k xs m
_
⇒
match fmt_ofck with
Some_
⇒
None
None
⇒
op_res_into k xs m
⇒
match xs with
⇒
let* from ≔ fmt_offk in
let* m0 ≔ modulusk in
let 'lo, hi ≔
match sg with
⇒
−m0 / 2, m0 / 2 − 1
⇒
0, m0 − 1
in
match Ieee.ieee_to_intfrom x with
Somen
⇒
lo ≤? n && n ≤? hi
→
SomeOpResRValWIntn mod m0 m
else
SomeOpUBTAtom"float_conversion"
None
⇒
SomeOpUBTAtom"float_conversion"
WIntx :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
⇒
match fmt_ofk with
Somef
⇒
match xs with
⇒
let* n ≔ integer_sourceik sg x in
WIntx :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
None
⇒
op_res_into k xs m
⇒
match xs with
WIntx :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
⇒
match xs with
⇒
let* r ≔ float_converto k x in
WIntx :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
⇒
match xs with
⇒
let* rm ≔ va_arg_resk p m in
SomeOpResfstrm sndrm
WPtrp :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
=
SomeOpResr m′
⊢
keptm m′

destruct o ; cases H ; inversion H ; subst;first|apply kept_refl|match goal withE : op_res_int_ _ _ _ = Some_ |- _⇒rewrite op_res_int_mem_ _ _ _ _ _ E ; apply kept_reflend|match goal withE : va_arg_res_ _ _ = Some?rm |- _⇒destruct rm ; exact va_arg_res_kept_ _ _ _ _ Eend

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros o k xs m r m′ H
destruct o ; cases H ; inversion H ; subst;first|apply kept_refl|match goal withE : op_res_int_ _ _ _ = Some_ |- _⇒rewrite op_res_int_mem_ _ _ _ _ _ E ; apply kept_reflend|match goal withE : va_arg_res_ _ _ = Some?rm |- _⇒destruct rm ; exact va_arg_res_kept_ _ _ _ _ Eend

Only the op alloc allocates: a heap object with a positive alignment, and it writes nothing into the new memory.

212Lemma op_res_alloc
∀ o k xs m q kont
op_reso k xs m = SomeOpAllocq kont
0 < req_alignq ∧ ∀base, keptallocatedm q base sndkontbase
Proof 4 steps Qed
intros o k xs m q kont H
destruct o ; cases H ; inversion H ; subst
split ; simpl ; lia | intros base ; apply kept_refl

Ending an invocation's locals (invalidate_locals/3) is kept: it ends live stack objects, and writes nothing.

223Lemma invalidate_locals_kept
∀ locals m m′
invalidate_localslocals m = Somem′
keptm m′
Proof 20 steps Qed
intros locals m m′ H
eapply fold_keptname × optionZ λ_ ⇒ True ; exact I | | exact H
intros m1 x slot m2 _ E
split ; auto
simpl in E
cases E ; inversion E ; subst ; try apply kept_refl
match goal withEr : replace_region?base _ _ = Some_ |- _⇒split ; intros b reg′ Eb ; simpl in Eb ; rewrite object_region_replace_ _ _ _ b Er eq_refl in Eb ; destruct Z.eqbb base eqn: Ez | intros a _ ; simpl ; autoend
–apply Z.eqb_eq in Ez
subst
inversion Eb ; subst
eexists
split ; eassumption |
right
split ; assumption |
f_equal
symmetry
assumption
–exists reg'
auto

What a step does to memory

The argument snapshot a variadic callee takes writes its words into the snapshot object: if the 8 bytes per word from a on are inside objects, snapshot_values is kept.

242Lemma snapshot_kept
∀ xs a m
∀b, a ≤ b < a + 8 × Z.of_natlengthxs → in_objectm b
Explore proof 26 tactics

Initial goal

⊢
∀xs : listword a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m

induction xs as | x xs IH ; simpl ; intros a m Hin

2 open

a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + 0 → in_objectm b
⊢
keptm m
focused goal
x :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
match x with

–apply kept_refl

deferred goal
x :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
match x with

–destruct x as n | p | c size

3 open

n :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
focused goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
focused goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

+eapply kept_trans ; | apply IH

4 open

n :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
focused goal
n :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
∀b : Z, a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs → in_objectstore_bytesm a 8 n b
deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

∗apply store_bytes_kept

4 open

n :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
∀b : Z, a ≤ b < a + 8 → in_objectm b
deferred goal
n :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
∀b : Z, a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs → in_objectstore_bytesm a 8 n b
deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

intros b Hb

4 open

n :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
b :
Z
Hb :
a ≤ b < a + 8
⊢
deferred goal
n :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
∀b : Z, a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs → in_objectstore_bytesm a 8 n b
deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

apply Hin

4 open

n :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
b :
Z
Hb :
a ≤ b < a + 8
⊢
a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0
deferred goal
n :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
∀b : Z, a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs → in_objectstore_bytesm a 8 n b
deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

lia

3 open

deferred goal
n :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
∀b : Z, a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs → in_objectstore_bytesm a 8 n b
deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

∗intros b Hb

3 open

n :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
b :
Z
Hb :
a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs
deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

apply in_object_store_bytes , Hin

3 open

n :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
b :
Z
Hb :
a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs
⊢
a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0
deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

lia

2 open

deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

+eapply kept_trans ; | apply IH

3 open

p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
focused goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
∀b : Z, a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs → in_objectstore_auxstore_bytesm a 8 ptr_addrp a ptr_capp b
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

∗eapply kept_trans ; | apply store_aux_kept

4 open

p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
focused goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
∀b : Z, a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs → in_objectstore_auxstore_bytesm a 8 ptr_addrp a ptr_capp b
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

--apply store_bytes_kept

4 open

p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
∀b : Z, a ≤ b < a + 8 → in_objectm b
deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
∀b : Z, a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs → in_objectstore_auxstore_bytesm a 8 ptr_addrp a ptr_capp b
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

intros b Hb

4 open

p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
b :
Z
Hb :
a ≤ b < a + 8
⊢
deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
∀b : Z, a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs → in_objectstore_auxstore_bytesm a 8 ptr_addrp a ptr_capp b
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

apply Hin

4 open

p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
b :
Z
Hb :
a ≤ b < a + 8
⊢
a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0
deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
∀b : Z, a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs → in_objectstore_auxstore_bytesm a 8 ptr_addrp a ptr_capp b
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

lia

3 open

deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
∀b : Z, a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs → in_objectstore_auxstore_bytesm a 8 ptr_addrp a ptr_capp b
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

--apply in_object_store_bytes , Hin

3 open

p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
a ≤ a < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0
deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
∀b : Z, a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs → in_objectstore_auxstore_bytesm a 8 ptr_addrp a ptr_capp b
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

lia

2 open

deferred goal
p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
∀b : Z, a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs → in_objectstore_auxstore_bytesm a 8 ptr_addrp a ptr_capp b
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

∗intros b Hb

2 open

p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
b :
Z
Hb :
a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

apply in_object_store_aux , in_object_store_bytes , Hin

2 open

p :
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
b :
Z
Hb :
a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs
⊢
a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0
deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

lia

deferred goal
c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
keptm snapshot_valuesxs a + 8 m

+apply IH

c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
⊢
∀b : Z, a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs → in_objectm b

intros b Hb

c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
b :
Z
Hb :
a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs
⊢

apply Hin

c :
size :
Z
xs :
listword
IH :
∀a : Z m : mem, ∀b : Z, a ≤ b < a + 8 × Z.of_natDatatypes.lengthxs → in_objectm b → keptm snapshot_valuesxs a m
a :
Z
m :
Hin :
∀b : Z, a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 → in_objectm b
b :
Z
Hb :
a + 8 ≤ b < a + 8 + 8 × Z.of_natDatatypes.lengthxs
⊢
a ≤ b < a + Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0

lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
induction xs as | x xs IH ; simpl ; intros a m Hin
–apply kept_refl
–destruct x as n | p | c size
+eapply kept_trans ; | apply IH
intros b Hb
apply Hin
lia
∗intros b Hb
lia
+eapply kept_trans ; | apply IH
∗eapply kept_trans ; | apply store_aux_kept
intros b Hb
apply Hin
lia
--apply in_object_store_bytes , Hin
lia
∗intros b Hb
lia
+apply IH
intros b Hb
apply Hin
lia

A heap request's extent covers its size: the runtime is asked for at least as many bytes as the object needs.

262Lemma heap_req_extent
∀ align size
size ≤ req_extentheap_reqalign size
Explore proof 5 tactics

Initial goal

⊢
∀align size : Z, size ≤ req_extentheap_reqalign size

intros align size

align, size :
Z
⊢
size ≤ req_extentheap_reqalign size

simpl

align, size :
Z
⊢
size ≤ size + 15 / 16 × 16

pose proof Z.div_modsize + 15 16 ltac:lia

align, size :
Z
H :
size + 15 = 16 × size + 15 / 16 + size + 15 mod 16
⊢
size ≤ size + 15 / 16 × 16

pose proof Z.mod_pos_boundsize + 15 16 ltac:lia

align, size :
Z
H :
size + 15 = 16 × size + 15 / 16 + size + 15 mod 16
H0 :
0 ≤ size + 15 mod 16 < 16
⊢
size ≤ size + 15 / 16 × 16

lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros align size
simpl
pose proof Z.div_modsize + 15 16 ltac:lia
pose proof Z.mod_pos_boundsize + 15 16 ltac:lia
lia

The new object's bytes are inside it: after allocating q at base, every address from base up to base plus the extent is inside an object.

272Lemma in_allocated
∀ m q base b
base ≤ b < base + req_extentq
Explore proof 5 tactics

Initial goal

⊢
∀m : mem q : alloc_req base b : Z, base ≤ b < base + req_extentq → in_objectallocatedm q base b

intros m q base b Hb

m :
base, b :
Z
Hb :
base ≤ b < base + req_extentq
⊢

exists base, mkRegionbase base + req_extentq req_kindq Live

m :
base, b :
Z
Hb :
base ≤ b < base + req_extentq
⊢
object_regionbase m_regionsallocatedm q base = Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live ∧ base ≤ b < r_endr_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live

simpl

m :
base, b :
Z
Hb :
base ≤ b < base + req_extentq
⊢
base =? base
→
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live
=
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live
∧
base ≤ b < base + req_extentq

rewrite Z.eqb_refl

m :
base, b :
Z
Hb :
base ≤ b < base + req_extentq
⊢
Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live = Somer_base ≔ base; r_end ≔ base + req_extentq; r_kind ≔ req_kindq; r_life ≔ Live ∧ base ≤ b < base + req_extentq

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m q base b Hb
exists base, mkRegionbase base + req_extentq req_kindq Live
simpl
rewrite Z.eqb_refl
auto

A variadic callee's snapshot is written into its new object.

280Lemma snapshot_alloc_kept
∀ xs m base
let q ≔ heap_req16 8 × Z.of_natlengthxs in
keptallocatedm q base snapshot_valuesxs base allocatedm q base
Explore proof 7 tactics

Initial goal

⊢
∀ xs : listword m : mem base : Z  ,
let q ≔ heap_req16 8 × Z.of_natDatatypes.lengthxs in
keptallocatedm q base snapshot_valuesxs base allocatedm q base

intros xs m base q

xs :
listword
m :
base :
Z
q :=
heap_req16 8 × Z.of_natDatatypes.lengthxs : alloc_req
⊢
keptallocatedm q base snapshot_valuesxs base allocatedm q base

apply snapshot_kept

xs :
listword
m :
base :
Z
q :=
heap_req16 8 × Z.of_natDatatypes.lengthxs : alloc_req
⊢
∀b : Z, base ≤ b < base + 8 × Z.of_natDatatypes.lengthxs → in_objectallocatedm q base b

intros b Hb

xs :
listword
m :
base :
Z
q :=
heap_req16 8 × Z.of_natDatatypes.lengthxs : alloc_req
b :
Z
Hb :
base ≤ b < base + 8 × Z.of_natDatatypes.lengthxs
⊢

apply in_allocated

xs :
listword
m :
base :
Z
q :=
heap_req16 8 × Z.of_natDatatypes.lengthxs : alloc_req
b :
Z
Hb :
base ≤ b < base + 8 × Z.of_natDatatypes.lengthxs
⊢
base ≤ b < base + req_extentq

pose proof heap_req_extent16 8 × Z.of_natlengthxs

xs :
listword
m :
base :
Z
q :=
heap_req16 8 × Z.of_natDatatypes.lengthxs : alloc_req
b :
Z
Hb :
base ≤ b < base + 8 × Z.of_natDatatypes.lengthxs
H :
8 × Z.of_natDatatypes.lengthxs ≤ req_extentheap_req16 8 × Z.of_natDatatypes.lengthxs
⊢
base ≤ b < base + req_extentq

unfold q

xs :
listword
m :
base :
Z
q :=
heap_req16 8 × Z.of_natDatatypes.lengthxs : alloc_req
b :
Z
Hb :
base ≤ b < base + 8 × Z.of_natDatatypes.lengthxs
H :
8 × Z.of_natDatatypes.lengthxs ≤ req_extentheap_req16 8 × Z.of_natDatatypes.lengthxs
⊢
base ≤ b < base + req_extentheap_req16 8 × Z.of_natDatatypes.lengthxs

lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros xs m base q
intros b Hb
pose proof heap_req_extent16 8 × Z.of_natlengthxs
unfold q
lia

The instruction i is the one doomed_result/5 reads: a check_ahead.

290Definition ahead_insti : inst : bool ≔
match i with
Let_ A CheckAhead_ _ _ _ _ _
⇒
true
_
⇒
false

For every instruction but a check_ahead, doomed_result changes only an unchecked outcome: in a doomed frame it becomes the early trap, unless it is an alias or a wrong limit.

296Lemma doomed_result_other
∀ ge fr m i out
ahead_insti = false
doomed_resultge fr m i out
=
match out with
⇒
match fr_doomedfr, w with
Somewhy, Alias | WhyLimit
⇒
Someout, fr_doomedfr
Somewhy, _
⇒
None, _
⇒
Someout, None
_
⇒
Someout, fr_doomedfr
Explore proof 6 tactics

Initial goal

⊢
∀ ge : genv fr : frame m : mem i : inst out : inst_out  ,
ahead_insti = false
→
doomed_resultge fr m i out
=
match out with
⇒
match fr_doomedfr with
Somewhy
⇒
match w with
⇒
Someout, fr_doomedfr
None
⇒
Someout, None
_
⇒
Someout, fr_doomedfr

intros ge fr m i out E

ge :
fr :
m :
i :
E :
ahead_insti = false
⊢
doomed_resultge fr m i out
=
match out with
⇒
match fr_doomedfr with
Somewhy
⇒
match w with
⇒
Someout, fr_doomedfr
None
⇒
Someout, None
_
⇒
Someout, fr_doomedfr

destruct i ; try reflexivity

ge :
fr :
m :
d :
o :
args :
listvalue
E :
ahead_instLetd k o args = false
⊢
doomed_resultge fr m Letd k o args out
=
match out with
⇒
match fr_doomedfr with
Somewhy
⇒
match w with
⇒
Someout, fr_doomedfr
None
⇒
Someout, None
_
⇒
Someout, fr_doomedfr

destruct k ; try reflexivity

ge :
fr :
m :
d :
o :
args :
listvalue
E :
ahead_instLetd A o args = false
⊢
doomed_resultge fr m Letd A o args out
=
match out with
⇒
match fr_doomedfr with
Somewhy
⇒
match w with
⇒
Someout, fr_doomedfr
None
⇒
Someout, None
_
⇒
Someout, fr_doomedfr

destruct o ; try reflexivity

ge :
fr :
m :
d :
lo, hi :
Z
align, ahi :
Z
args :
listvalue
E :
ahead_instLetd A CheckAheadlo hi r align ahi args = false
⊢
doomed_resultge fr m Letd A CheckAheadlo hi r align ahi args out
=
match out with
⇒
match fr_doomedfr with
Somewhy
⇒
match w with
⇒
Someout, fr_doomedfr
None
⇒
Someout, None
_
⇒
Someout, fr_doomedfr

destruct args as | v | v′ args ; try reflexivity

ge :
fr :
m :
d :
lo, hi :
Z
align, ahi :
Z
E :
ahead_instLetd A CheckAheadlo hi r align ahi v = false
⊢
doomed_resultge fr m Letd A CheckAheadlo hi r align ahi v out
=
match out with
⇒
match fr_doomedfr with
Somewhy
⇒
match w with
⇒
Someout, fr_doomedfr
None
⇒
Someout, None
_
⇒
Someout, fr_doomedfr

discriminate E

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros ge fr m i out E
destruct i ; try reflexivity
destruct k ; try reflexivity
destruct o ; try reflexivity
destruct args as | v | v′ args ; try reflexivity
discriminate E

doomed_result (doomed_result/5) passes the instruction's result on, or continues with the memory unchanged, or stops.

316Lemma doomed_result_out
∀ ge fr m i out od
doomed_resultge fr m i out = Someod
fstod = out ∨ ∃e l, fstod = IContinuee l m ∨ ∃o, fstod = IStopo
Explore proof 10 tactics

Initial goal

⊢
∀ge : genv fr : frame m : mem i : inst out : inst_out od : inst_out × optionreason, doomed_resultge fr m i out = Someod → fstod = out ∨ ∃e : env l : listname × optionZ, fstod = IContinuee l m ∨ ∃o : outcome, fstod = IStopo

intros ge fr m i out od H

ge :
fr :
m :
i :
od :
inst_out × optionreason
H :
doomed_resultge fr m i out = Someod
⊢
fstod = out ∨ ∃e : env l : listname × optionZ, fstod = IContinuee l m ∨ ∃o : outcome, fstod = IStopo

destruct ahead_insti eqn: Ea

2 open

ge :
fr :
m :
i :
od :
inst_out × optionreason
H :
doomed_resultge fr m i out = Someod
Ea :
ahead_insti = true
⊢
fstod = out ∨ ∃e : env l : listname × optionZ, fstod = IContinuee l m ∨ ∃o : outcome, fstod = IStopo
focused goal
ge :
fr :
m :
i :
od :
inst_out × optionreason
H :
doomed_resultge fr m i out = Someod
Ea :
ahead_insti = false
⊢
fstod = out ∨ ∃e : env l : listname × optionZ, fstod = IContinuee l m ∨ ∃o : outcome, fstod = IStopo

–destruct i ; try discriminate Ea

2 open

ge :
fr :
m :
d :
o :
args :
listvalue
od :
inst_out × optionreason
H :
doomed_resultge fr m Letd k o args out = Someod
Ea :
ahead_instLetd k o args = true
⊢
fstod = out ∨ ∃e : env l : listname × optionZ, fstod = IContinuee l m ∨ ∃o0 : outcome, fstod = IStopo0
deferred goal
ge :
fr :
m :
i :
od :
inst_out × optionreason
H :
doomed_resultge fr m i out = Someod
Ea :
ahead_insti = false
⊢
fstod = out ∨ ∃e : env l : listname × optionZ, fstod = IContinuee l m ∨ ∃o : outcome, fstod = IStopo

destruct k ; try discriminate Ea

2 open

ge :
fr :
m :
d :
o :
args :
listvalue
od :
inst_out × optionreason
H :
doomed_resultge fr m Letd A o args out = Someod
Ea :
ahead_instLetd A o args = true
⊢
fstod = out ∨ ∃e : env l : listname × optionZ, fstod = IContinuee l m ∨ ∃o0 : outcome, fstod = IStopo0
deferred goal
ge :
fr :
m :
i :
od :
inst_out × optionreason
H :
doomed_resultge fr m i out = Someod
Ea :
ahead_insti = false
⊢
fstod = out ∨ ∃e : env l : listname × optionZ, fstod = IContinuee l m ∨ ∃o : outcome, fstod = IStopo

destruct o ; try discriminate Ea

2 open

ge :
fr :
m :
d :
lo, hi :
Z
align, ahi :
Z
args :
listvalue
od :
inst_out × optionreason
H :
doomed_resultge fr m Letd A CheckAheadlo hi r align ahi args out = Someod
Ea :
ahead_instLetd A CheckAheadlo hi r align ahi args = true
⊢
fstod = out ∨ ∃e : env l : listname × optionZ, fstod = IContinuee l m ∨ ∃o : outcome, fstod = IStopo
deferred goal
ge :
fr :
m :
i :
od :
inst_out × optionreason
H :
doomed_resultge fr m i out = Someod
Ea :
ahead_insti = false
⊢
fstod = out ∨ ∃e : env l : listname × optionZ, fstod = IContinuee l m ∨ ∃o : outcome, fstod = IStopo

destruct args as | v | v′ args ; try discriminate Ea

2 open

ge :
fr :
m :
d :
lo, hi :
Z
align, ahi :
Z
od :
inst_out × optionreason
H :
doomed_resultge fr m Letd A CheckAheadlo hi r align ahi v out = Someod
Ea :
ahead_instLetd A CheckAheadlo hi r align ahi v = true
⊢
fstod = out ∨ ∃e : env l : listname × optionZ, fstod = IContinuee l m ∨ ∃o : outcome, fstod = IStopo
deferred goal
ge :
fr :
m :
i :
od :
inst_out × optionreason
H :
doomed_resultge fr m i out = Someod
Ea :
ahead_insti = false
⊢
fstod = out ∨ ∃e : env l : listname × optionZ, fstod = IContinuee l m ∨ ∃o : outcome, fstod = IStopo

unfold doomed_result in H

2 open

ge :
fr :
m :
d :
lo, hi :
Z
align, ahi :
Z
od :
inst_out × optionreason
H :
match out with
⇒
let* p ≔ value_xge fr_envfr P v in
Some
match fr_doomedfr with
Somew
⇒
Somew
None
⇒
Somewhy
⇒
match fr_doomedfr with
Somewhy
⇒
match w with
⇒
Someout, fr_doomedfr
None
⇒
Someout, None
_
⇒
Someout, fr_doomedfr
=
Someod
Ea :
ahead_instLetd A CheckAheadlo hi r align ahi v = true
⊢
fstod = out ∨ ∃e : env l : listname × optionZ, fstod = IContinuee l m ∨ ∃o : outcome, fstod = IStopo
deferred goal
ge :
fr :
m :
i :
od :
inst_out × optionreason
H :
doomed_resultge fr m i out = Someod
Ea :
ahead_insti = false
⊢
fstod = out ∨ ∃e : env l : listname × optionZ, fstod = IContinuee l m ∨ ∃o : outcome, fstod = IStopo

cases H ; inversion H ; subst ; simpl ; eauto

deferred goal
ge :
fr :
m :
i :
od :
inst_out × optionreason
H :
doomed_resultge fr m i out = Someod
Ea :
ahead_insti = false
⊢
fstod = out ∨ ∃e : env l : listname × optionZ, fstod = IContinuee l m ∨ ∃o : outcome, fstod = IStopo

–rewrite doomed_result_other_ _ _ _ _ Ea in H

ge :
fr :
m :
i :
od :
inst_out × optionreason
H :
match out with
⇒
match fr_doomedfr with
Somewhy
⇒
match w with
⇒
Someout, fr_doomedfr
None
⇒
Someout, None
_
⇒
Someout, fr_doomedfr
=
Someod
Ea :
ahead_insti = false
⊢
fstod = out ∨ ∃e : env l : listname × optionZ, fstod = IContinuee l m ∨ ∃o : outcome, fstod = IStopo

cases H ; inversion H ; subst ; simpl ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros ge fr m i out od H
destruct ahead_insti eqn: Ea
–destruct i ; try discriminate Ea
destruct k ; try discriminate Ea
destruct o ; try discriminate Ea
destruct args as | v | v′ args ; try discriminate Ea
unfold doomed_result in H
cases H ; inversion H ; subst ; simpl ; eauto
–rewrite doomed_result_other_ _ _ _ _ Ea in H
cases H ; inversion H ; subst ; simpl ; eauto

The ops inst_step reads in a let of its own (a local's check, a function check, the variadic area); every other op's let is the generic one.

330Definition special_leto : op : bool ≔
match o with
⇒
true
_
⇒
false

For any other op o, inst_step of a let is the generic case: read the arguments at their classes, run the op, and bind its result, stop, or allocate.

336Lemma inst_step_let
∀ ge fr m d k o args
special_leto = false
inst_stepge fr m Letd k o args
=
let e ≔ fr_envfr in
let locals ≔ fr_localsfr in
let* classes ≔ op_arg_classeso k in
let* xs ≔ map2_optionvalue_xge e classes args in
let* out ≔ op_reso k xs m in
match out with
OpResr m′
⇒
Somebind_resd r e locals m′
OpUBwhy
⇒
SomeIStopUBwhy
OpAllocq kont
⇒
Some
λ base  ⇒
let x, m′ ≔ kontbase in
putd x e, locals, m′
Explore proof 2 tactics

Initial goal

⊢
∀ ge : genv fr : frame m : mem d : name k : class o : op args : listvalue  ,
special_leto = false
→
inst_stepge fr m Letd k o args
=
let e ≔ fr_envfr in
let locals ≔ fr_localsfr in
let* classes ≔ op_arg_classeso k in
let* xs ≔ map2_optionvalue_xge e classes args in
match op_reso k xs m with
SomeOpResr m′
⇒
Somebind_resd r e locals m′
SomeOpUBwhy
⇒
SomeIStopUBwhy
SomeOpAllocq kont
⇒
Some
λ base : Z  ⇒
let x, m′ ≔ kontbase in
putd x e, locals, m′
None
⇒
None

intros ge fr m d k o args Es

ge :
fr :
m :
d :
o :
args :
listvalue
Es :
special_leto = false
⊢
inst_stepge fr m Letd k o args
=
let e ≔ fr_envfr in
let locals ≔ fr_localsfr in
let* classes ≔ op_arg_classeso k in
let* xs ≔ map2_optionvalue_xge e classes args in
match op_reso k xs m with
SomeOpResr m′
⇒
Somebind_resd r e locals m′
SomeOpUBwhy
⇒
SomeIStopUBwhy
SomeOpAllocq kont
⇒
Some
λ base : Z  ⇒
let x, m′ ≔ kontbase in
putd x e, locals, m′
None
⇒
None

destruct o ; try discriminate Es ; destruct k ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros ge fr m d k o args Es
destruct o ; try discriminate Es ; destruct k ; reflexivity

An instruction that continues changes memory as kept allows, where the genv's free does (free_keeps).

354Lemma inst_step_kept
∀ ge fr m i e l m′
inst_stepge fr m i = SomeIContinuee l m′
keptm m′
Explore proof 4 tactics

Initial goal

⊢
∀ge : genv fr : frame m : mem i : inst e : env l : listname × optionZ m′ : mem, free_keepsge_freege → inst_stepge fr m i = SomeIContinuee l m′ → keptm m′

intros ge fr m i e l m′ Hfree H

ge :
fr :
m :
i :
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m i = SomeIContinuee l m′
⊢
keptm m′

destruct i

9 open

ge :
fr :
m :
d :
o :
args :
listvalue
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m Letd k o args = SomeIContinuee l m′
⊢
keptm m′
focused goal
ge :
fr :
m :
d :
o :
args :
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m Flightd o args lower = SomeIContinuee l m′
⊢
keptm m′
focused goal
ge :
fr :
m :
off :
Z
v, a :
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m RawStorew off v a = SomeIContinuee l m′
⊢
keptm m′
focused goal
ge :
fr :
m :
off :
Z
v, a :
es :
listeffect
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m RawStorePointeroff v a es = SomeIContinuee l m′
⊢
keptm m′
focused goal
ge :
fr :
m :
callee :
args :
listarg
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m Callr callee args = SomeIContinuee l m′
⊢
keptm m′
focused goal
ge :
fr :
m :
callee :
args :
listarg
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m RawCallr callee args = SomeIContinuee l m′
⊢
keptm m′
focused goal
ge :
fr :
m :
x :
size :
Z
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m LocalAllocx size = SomeIContinuee l m′
⊢
keptm m′
focused goal
ge :
fr :
m :
file :
line :
Z
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m Locfile line = SomeIContinuee l m′
⊢
keptm m′
focused goal
ge :
fr :
m :
q :
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m Touchq = SomeIContinuee l m′
⊢
keptm m′

1: destruct special_leto eqn: Es ; destruct o ; try discriminate Es | rewrite inst_step_let_ _ _ _ _ _ _ Es in H

12 open

ge :
fr :
m :
d :
x :
off, bytes :
Z
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
⊢
keptm m′
focused goal
ge :
fr :
m :
d :
args :
listvalue
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m Letd k CheckFunction args = SomeIContinuee l m′
⊢
keptm m′
focused goal
ge :
fr :
m :
d :
args :
listvalue
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m Letd k VaArgs args = SomeIContinuee l m′
Es :
⊢
keptm m′
focused goal
ge :
fr :
m :
d :
o :
args :
listvalue
e :
l :
listname × optionZ
m′ :
H :
let e ≔ fr_envfr in
let locals ≔ fr_localsfr in
let* classes ≔ op_arg_classeso k in
let* xs ≔ map2_optionvalue_xge e classes args in
match op_reso k xs m with
SomeOpResr m′
⇒
Somebind_resd r e locals m′
SomeOpUBwhy
⇒
SomeIStopUBwhy
SomeOpAllocq kont
⇒
Some
λ base : Z  ⇒
let x, m′ ≔ kontbase in
putd x e, locals, m′
None
⇒
None
=
SomeIContinuee l m′
Es :
special_leto = false
⊢
keptm m′
focused goal
ge :
fr :
m :
d :
o :
args :
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m Flightd o args lower = SomeIContinuee l m′
⊢
keptm m′
focused goal
ge :
fr :
m :
off :
Z
v, a :
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m RawStorew off v a = SomeIContinuee l m′
⊢
keptm m′
focused goal
ge :
fr :
m :
off :
Z
v, a :
es :
listeffect
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m RawStorePointeroff v a es = SomeIContinuee l m′
⊢
keptm m′
focused goal
ge :
fr :
m :
callee :
args :
listarg
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m Callr callee args = SomeIContinuee l m′
⊢
keptm m′
focused goal
ge :
fr :
m :
callee :
args :
listarg
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m RawCallr callee args = SomeIContinuee l m′
⊢
keptm m′
focused goal
ge :
fr :
m :
x :
size :
Z
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m LocalAllocx size = SomeIContinuee l m′
⊢
keptm m′
focused goal
ge :
fr :
m :
file :
line :
Z
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m Locfile line = SomeIContinuee l m′
⊢
keptm m′
focused goal
ge :
fr :
m :
q :
e :
l :
listname × optionZ
m′ :
H :
inst_stepge fr m Touchq = SomeIContinuee l m′
⊢
keptm m′

all: unfold inst_step , external_call , bind_res , store_out in H ; cases H ; inversion H ; subst;first|apply kept_refl|match goal withE : op_res_ _ _ _ = SomeOpRes_ _ |- _⇒exact op_res_kept_ _ _ _ _ _ Eend|match goal withE : ge_free_ _ _ = Some_, _ |- _⇒exact Hfree_ _ _ _ Eend|match goal withE : store_res_ _ _ _ _ = Some_, _ |- _⇒exact store_res_kept_ _ _ _ _ _ _ Eend|match goal withA : access_res_ _ _ _ _ _ = SomeRVal_ , E : pointer_store_effects_ _ _ _ = Some_ |- _⇒apply pointer_store_effects_kept_ _ _ _ _ access_in_ _ _ _ _ _ _ A Eend

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|apply kept_refl|match goal withE : op_res_ _ _ _ = SomeOpRes_ _ |- _⇒exact op_res_kept_ _ _ _ _ _ Eend|match goal withE : ge_free_ _ _ = Some_, _ |- _⇒exact Hfree_ _ _ _ Eend|match goal withE : store_res_ _ _ _ _ = Some_, _ |- _⇒exact store_res_kept_ _ _ _ _ _ _ Eend|match goal withA : access_res_ _ _ _ _ _ = SomeRVal_ , E : pointer_store_effects_ _ _ _ = Some_ |- _⇒apply pointer_store_effects_kept_ _ _ _ _ access_in_ _ _ _ _ _ _ A Eend

An instruction that allocates asks for a positive alignment, and writes nothing yet into the memory with the new object.

374Lemma inst_step_fresh
∀ ge fr m i q k
inst_stepge fr m i = SomeIFreshq k
0 < req_alignq ∧ ∀base, keptallocatedm q base sndkbase
Explore proof 5 tactics

Initial goal

⊢
∀ge : genv fr : frame m : mem i : inst q : alloc_req k : Z → env × listname × optionZ × mem, inst_stepge fr m i = SomeIFreshq k → 0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase

intros ge fr m i q k H

ge :
fr :
m :
i :
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m i = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase

destruct i

9 open

ge :
fr :
m :
d :
k0 :
o :
args :
listvalue
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m Letd k0 o args = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
d :
o :
args :
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m Flightd o args lower = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
off :
Z
v, a :
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m RawStorew off v a = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
off :
Z
v, a :
es :
listeffect
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m RawStorePointeroff v a es = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
callee :
args :
listarg
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m Callr callee args = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
callee :
args :
listarg
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m RawCallr callee args = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
x :
size :
Z
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m LocalAllocx size = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
file :
line :
Z
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m Locfile line = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
q0 :
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m Touchq0 = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase

1: destruct special_leto eqn: Es ; destruct o ; try discriminate Es | rewrite inst_step_let_ _ _ _ _ _ _ Es in H

12 open

ge :
fr :
m :
d :
k0 :
x :
off, bytes :
Z
align :
Z
args :
listvalue
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m Letd k0 CheckLocalx off bytes r align args = SomeIFreshq k
Es :
special_letCheckLocalx off bytes r align = true
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
d :
k0 :
args :
listvalue
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m Letd k0 CheckFunction args = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
d :
k0 :
args :
listvalue
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m Letd k0 VaArgs args = SomeIFreshq k
Es :
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
d :
k0 :
o :
args :
listvalue
k :
Z → env × listname × optionZ × mem
H :
let e ≔ fr_envfr in
let locals ≔ fr_localsfr in
let* classes ≔ op_arg_classeso k0 in
let* xs ≔ map2_optionvalue_xge e classes args in
match op_reso k0 xs m with
SomeOpResr m′
⇒
Somebind_resd r e locals m′
SomeOpUBwhy
⇒
SomeIStopUBwhy
SomeOpAllocq kont
⇒
Some
λ base : Z  ⇒
let x, m′ ≔ kontbase in
putd x e, locals, m′
None
⇒
None
=
SomeIFreshq k
Es :
special_leto = false
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
d :
o :
args :
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m Flightd o args lower = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
off :
Z
v, a :
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m RawStorew off v a = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
off :
Z
v, a :
es :
listeffect
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m RawStorePointeroff v a es = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
callee :
args :
listarg
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m Callr callee args = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
callee :
args :
listarg
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m RawCallr callee args = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
x :
size :
Z
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m LocalAllocx size = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
file :
line :
Z
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m Locfile line = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase
focused goal
ge :
fr :
m :
q0 :
k :
Z → env × listname × optionZ × mem
H :
inst_stepge fr m Touchq0 = SomeIFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedm q base sndkbase

all: unfold inst_step , external_call , bind_res , store_out in H ; cases H ; inversion H ; subst

2 open

ge :
fr :
m :
d :
k0 :
o :
args :
listvalue
l :
listclass
Heqo0 :
op_arg_classeso k0 = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
k1 :
Z → word × mem
H :
Some
λ base : Z  ⇒
let x, m′ ≔ k1base in
putd x fr_envfr, fr_localsfr, m′
=
Some
λ base : Z  ⇒
let x, m′ ≔ k1base in
putd x fr_envfr, fr_localsfr, m′
Heqo2 :
op_reso k0 l0 m = SomeOpAllocq k1
Es :
special_leto = false
⊢
0 < req_alignq
∧
∀ base : Z  ,
snd
let x, m′ ≔ k1base in
putd x fr_envfr, fr_localsfr, m′
focused goal
ge :
fr :
m :
x :
size :
Z
Heqo :
lookupx fr_localsfr = SomeNone
H :
SomeIFreshlocal_reqsize λbase : Z ⇒ fr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = SomeIFreshlocal_reqsize λbase : Z ⇒ fr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base
⊢
0 < req_alignlocal_reqsize ∧ ∀base : Z, keptallocatedm local_reqsize base sndfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base

all: first|split ; simpl ; lia | intros base ; simpl ; apply kept_refl|match goal withE : op_res_ _ _ _ = SomeOpAlloc_ _ |- _⇒destruct op_res_alloc_ _ _ _ _ _ E as Ha Hkend;split;|exact Ha|intros base ; specialize Hkbase ; simpl;match goal withHk : kept_ snd?t |- _⇒destruct tend;exact Hk

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
all: first|split ; simpl ; lia | intros base ; simpl ; apply kept_refl|match goal withE : op_res_ _ _ _ = SomeOpAlloc_ _ |- _⇒destruct op_res_alloc_ _ _ _ _ _ E as Ha Hkend;split;|exact Ha|intros base ; specialize Hkbase ; simpl;match goal withHk : kept_ snd?t |- _⇒destruct tend;exact Hk

or_stuck gives a next configuration only if it was given one.

392Lemma or_stuck_next
∀ why r c
or_stuckwhy r = Nextc
r = SomeNextc
Explore proof 2 tactics

Initial goal

⊢
∀why : string r : optionstep_result c : config, or_stuckwhy r = Nextc → r = SomeNextc

intros why r c H

why :
r :
H :
or_stuckwhy r = Nextc
⊢
r = SomeNextc

destruct r ; simpl in H ; congruence

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros why r c H
destruct r ; simpl in H ; congruence

or_stuck gives an allocation only if it was given one.

396Lemma or_stuck_fresh
∀ why r q k
or_stuckwhy r = Freshq k
r = SomeFreshq k
Explore proof 2 tactics

Initial goal

⊢
∀why : string r : optionstep_result q : alloc_req k : Z → config, or_stuckwhy r = Freshq k → r = SomeFreshq k

intros why r q k H

why :
r :
k :
Z → config
H :
or_stuckwhy r = Freshq k
⊢
r = SomeFreshq k

destruct r ; simpl in H ; congruence

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros why r q k H
destruct r ; simpl in H ; congruence

A tactic: where the hypothesis H says an or_stuck gave a step, split on the result it was given.

401Ltac unstuck H ≔
lazymatch type of H withor_stuck_ _ = Next_⇒apply or_stuck_next in H ; cases Hor_stuck_ _ = Fresh_ _⇒apply or_stuck_fresh in H ; cases H_⇒idtacend

A return changes memory as kept allows: it only ends the invocation's locals.

410Lemma return_step_kept
∀ c o c′
return_stepc o = Nextc′
Explore proof 5 tactics

Initial goal

⊢
∀c : config o : outcome c′ : config, return_stepc o = Nextc′ → keptc_memc c_memc′

unfold return_step

⊢
∀ c : config o : outcome c′ : config  ,
or_stuck"return"
match c_callersc with
[ ]
⇒
SomeDoneo
caller, pd :: callers
⇒
let* o′ ≔
match pd_convpd with
Somecw, kw
⇒
None
⇒
Someo
in
let* e ≔ returned_envpd_respd o′ fr_envcaller in
SomeNextc_frame ≔ fr_fn ≔ fr_fncaller; fr_env ≔ e; fr_locals ≔ fr_localscaller; fr_doomed ≔ fr_doomedcaller; fr_at ≔ fr_atcaller; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ c_fuelc
=
Nextc′
→

intros c o c′ H

c′ :
H :
or_stuck"return"
match c_callersc with
[ ]
⇒
SomeDoneo
caller, pd :: callers
⇒
let* o′ ≔
match pd_convpd with
Somecw, kw
⇒
None
⇒
Someo
in
let* e ≔ returned_envpd_respd o′ fr_envcaller in
SomeNextc_frame ≔ fr_fn ≔ fr_fncaller; fr_env ≔ e; fr_locals ≔ fr_localscaller; fr_doomed ≔ fr_doomedcaller; fr_at ≔ fr_atcaller; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ c_fuelc
=
Nextc′

apply or_stuck_next in H

c′ :
H :
match c_callersc with
[ ]
⇒
SomeDoneo
caller, pd :: callers
⇒
let* o′ ≔
match pd_convpd with
Somecw, kw
⇒
None
⇒
Someo
in
let* e ≔ returned_envpd_respd o′ fr_envcaller in
SomeNextc_frame ≔ fr_fn ≔ fr_fncaller; fr_env ≔ e; fr_locals ≔ fr_localscaller; fr_doomed ≔ fr_doomedcaller; fr_at ≔ fr_atcaller; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ c_fuelc
=
SomeNextc′

cases H ; inversion H ; subst ; simpl

m :
l :
listframe × pending
Heql :
c_callersc = f, p0 :: l
Heqo1 :
match pd_convp0 with
Somecw, kw
⇒
None
⇒
Someo
=
Someo0
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_kept_ _ _ Eend

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
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_kept_ _ _ Eend

A jump changes memory as kept allows: only a return changes it at all.

419Lemma jump_step_kept
∀ ge c l j c′
jump_stepge c l j = Nextc′
Explore proof 4 tactics

Initial goal

⊢
∀ge : genv c : config l : name j : jump c′ : config, jump_stepge c l j = Nextc′ → keptc_memc c_memc′

unfold jump_step , edge_step

⊢
∀ ge : genv c : config l : name j : jump c′ : config  ,
match fr_doomedc_framec with
Somewhy
⇒
match j with
JBranchv t1 t2
⇒
or_stuck"branch"
match value_xge fr_envc_framec W v with
SomeWIntn
⇒
Some
match if n =? 0 then t2 else t1 with
_
⇒
None
None
⇒
match j with
JBranchv t1 t2
⇒
or_stuck"branch"
match value_xge fr_envc_framec W v with
SomeWIntn
⇒
Some
match if n =? 0 then t2 else t1 with
_
⇒
None
⇒
match fn_retfr_fnc_framec with
⇒
let* x ≔ value_xge fr_envc_framec k v in
_
⇒
None
⇒
or_stuck"rets"
match fn_retfr_fnc_framec with
⇒
let* xs ≔ map2_optionvalue_xge fr_envc_framec ks vs in
_
⇒
None
=
Nextc′
→

intros ge c l j c′ H

ge :
l :
j :
c′ :
H :
match fr_doomedc_framec with
Somewhy
⇒
match j with
JBranchv t1 t2
⇒
or_stuck"branch"
match value_xge fr_envc_framec W v with
SomeWIntn
⇒
Some
match if n =? 0 then t2 else t1 with
_
⇒
None
None
⇒
match j with
JBranchv t1 t2
⇒
or_stuck"branch"
match value_xge fr_envc_framec W v with
SomeWIntn
⇒
Some
match if n =? 0 then t2 else t1 with
_
⇒
None
⇒
match fn_retfr_fnc_framec with
⇒
let* x ≔ value_xge fr_envc_framec k v in
_
⇒
None
⇒
or_stuck"rets"
match fn_retfr_fnc_framec with
⇒
let* xs ≔ map2_optionvalue_xge fr_envc_framec ks vs in
_
⇒
None
=
Nextc′

cases H ; unstuck H

9 open

ge :
l :
j :
c′ :
Heqo :
l0 :
Heqt0 :
t = Tol0
Heqj0 :
j = JGotoTol0
focused goal
ge :
l :
j :
c′ :
Heqo :
t1, t2 :
Heqj0 :
j = JBranchv t1 t2
w :
n :
Z
Heqw0 :
w = WIntn
Heqo0 :
l0 :
Heqt :
n =? 0
→
t2
else
t1
=
Tol0
focused goal
ge :
l :
j :
c′ :
Heqo :
l0 :
Heqt0 :
t = Tol0
Heqj0 :
j = JGotoTol0
focused goal
ge :
l :
j :
c′ :
Heqo :
l0 :
Heqt0 :
t = Polll0
Heqj0 :
j = JGotoPolll0
focused goal
ge :
l :
j :
c′ :
Heqo :
t1, t2 :
Heqj0 :
j = JBranchv t1 t2
w :
n :
Z
Heqw0 :
w = WIntn
Heqo0 :
l0 :
Heqt :
n =? 0
→
t2
else
t1
=
Tol0
focused goal
ge :
l :
j :
c′ :
Heqo :
t1, t2 :
Heqj0 :
j = JBranchv t1 t2
w :
n :
Z
Heqw0 :
w = WIntn
Heqo0 :
l0 :
Heqt :
n =? 0
→
t2
else
t1
=
focused goal
ge :
l :
j :
c′ :
Heqo :
Heqj0 :
j = JRetv
w :
Heqo0 :
value_xge fr_envc_framec k v = Somew
H :
Somereturn_stepc Retw = SomeNextc′
focused goal
ge :
l :
j :
c′ :
Heqo :
vs :
listvalue
Heqj0 :
j = JRetsvs
ks :
listclass
l0 :
listword
Heqo0 :
H :
Somereturn_stepc Retsl0 = SomeNextc′
focused goal
ge :
l :
j :
c′ :
Heqo :
Heqj0 :

all: first|match goal withE : return_step_ _ = Next_ |- _⇒exact return_step_kept_ _ _ Eend|inversion H ; subst;first|exact kept_refl_|match goal withE : return_step_ _ = Next_ |- _⇒exact return_step_kept_ _ _ Eend

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros ge c l j c′ H
all: first|match goal withE : return_step_ _ = Next_ |- _⇒exact return_step_kept_ _ _ Eend|inversion H ; subst;first|exact kept_refl_|match goal withE : return_step_ _ = Next_ |- _⇒exact return_step_kept_ _ _ Eend

A return never allocates.

431Lemma return_step_not_fresh
∀ c o q k
return_stepc o ≠ Freshq k
Explore proof 4 tactics

Initial goal

⊢
∀c : config o : outcome q : alloc_req k : Z → config, return_stepc o ≠ Freshq k

unfold return_step

⊢
∀ c : config o : outcome q : alloc_req k : Z → config  ,
or_stuck"return"
match c_callersc with
[ ]
⇒
SomeDoneo
caller, pd :: callers
⇒
let* o′ ≔
match pd_convpd with
Somecw, kw
⇒
None
⇒
Someo
in
let* e ≔ returned_envpd_respd o′ fr_envcaller in
SomeNextc_frame ≔ fr_fn ≔ fr_fncaller; fr_env ≔ e; fr_locals ≔ fr_localscaller; fr_doomed ≔ fr_doomedcaller; fr_at ≔ fr_atcaller; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ c_fuelc
≠

intros c o q k H

k :
Z → config
H :
or_stuck"return"
match c_callersc with
[ ]
⇒
SomeDoneo
caller, pd :: callers
⇒
let* o′ ≔
match pd_convpd with
Somecw, kw
⇒
None
⇒
Someo
in
let* e ≔ returned_envpd_respd o′ fr_envcaller in
SomeNextc_frame ≔ fr_fn ≔ fr_fncaller; fr_env ≔ e; fr_locals ≔ fr_localscaller; fr_doomed ≔ fr_doomedcaller; fr_at ≔ fr_atcaller; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ c_fuelc
=
⊢
False

apply or_stuck_fresh in H

k :
Z → config
H :
match c_callersc with
[ ]
⇒
SomeDoneo
caller, pd :: callers
⇒
let* o′ ≔
match pd_convpd with
Somecw, kw
⇒
None
⇒
Someo
in
let* e ≔ returned_envpd_respd o′ fr_envcaller in
SomeNextc_frame ≔ fr_fn ≔ fr_fncaller; fr_env ≔ e; fr_locals ≔ fr_localscaller; fr_doomed ≔ fr_doomedcaller; fr_at ≔ fr_atcaller; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ c_fuelc
=
SomeFreshq k
⊢
False

cases H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros c o q k H
apply or_stuck_fresh in H

A jump never allocates.

435Lemma jump_step_not_fresh
∀ ge c l j q k
jump_stepge c l j ≠ Freshq k
Explore proof 4 tactics

Initial goal

⊢
∀ge : genv c : config l : name j : jump q : alloc_req k : Z → config, jump_stepge c l j ≠ Freshq k

unfold jump_step , edge_step

⊢
∀ ge : genv c : config l : name j : jump q : alloc_req k : Z → config  ,
match fr_doomedc_framec with
Somewhy
⇒
match j with
JBranchv t1 t2
⇒
or_stuck"branch"
match value_xge fr_envc_framec W v with
SomeWIntn
⇒
Some
match if n =? 0 then t2 else t1 with
_
⇒
None
None
⇒
match j with
JBranchv t1 t2
⇒
or_stuck"branch"
match value_xge fr_envc_framec W v with
SomeWIntn
⇒
Some
match if n =? 0 then t2 else t1 with
_
⇒
None
⇒
match fn_retfr_fnc_framec with
⇒
let* x ≔ value_xge fr_envc_framec k0 v in
_
⇒
None
⇒
or_stuck"rets"
match fn_retfr_fnc_framec with
⇒
let* xs ≔ map2_optionvalue_xge fr_envc_framec ks vs in
_
⇒
None
≠

intros ge c l j q k H

ge :
l :
j :
k :
Z → config
H :
match fr_doomedc_framec with
Somewhy
⇒
match j with
JBranchv t1 t2
⇒
or_stuck"branch"
match value_xge fr_envc_framec W v with
SomeWIntn
⇒
Some
match if n =? 0 then t2 else t1 with
_
⇒
None
None
⇒
match j with
JBranchv t1 t2
⇒
or_stuck"branch"
match value_xge fr_envc_framec W v with
SomeWIntn
⇒
Some
match if n =? 0 then t2 else t1 with
_
⇒
None
⇒
match fn_retfr_fnc_framec with
⇒
let* x ≔ value_xge fr_envc_framec k v in
_
⇒
None
⇒
or_stuck"rets"
match fn_retfr_fnc_framec with
⇒
let* xs ≔ map2_optionvalue_xge fr_envc_framec ks vs in
_
⇒
None
=
⊢
False

cases H ; unstuck H ; first exact return_step_not_fresh_ _ _ _ H | discriminate H | idtac

2 open

ge :
l :
j :
k :
Z → config
Heqo :
Heqj0 :
j = JRetv
k0 :
w :
Heqo0 :
value_xge fr_envc_framec k0 v = Somew
H :
Somereturn_stepc Retw = SomeFreshq k
⊢
False
focused goal
ge :
l :
j :
k :
Z → config
Heqo :
vs :
listvalue
Heqj0 :
j = JRetsvs
ks :
listclass
l0 :
listword
Heqo0 :
H :
Somereturn_stepc Retsl0 = SomeFreshq k
⊢
False

all: injection H as H ; exact return_step_not_fresh_ _ _ _ H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros ge c l j q k H
cases H ; unstuck H ; first exact return_step_not_fresh_ _ _ _ H | discriminate H | idtac
all: injection H as H ; exact return_step_not_fresh_ _ _ _ H

A tactic for the goal that memory is kept: an instruction's result after doomed_result, if it continues, continues as the instruction did, or with the memory unchanged. Hfree says the genv's free is kept.

446Ltac doomed_continue Hfree ≔
match goal withE : doomed_result_ _ _ _ _ = Some?od , Hc : fst?od = IContinue_ _ _ |- _⇒destruct doomed_result_out_ _ _ _ _ _ E as Ho | e′ & l′ & Ho | o′ & Ho ; rewrite Ho in Hc ; try discriminate Hc;|subst;match goal withE2 : inst_step_ _ _ _ = SomeIContinue_ _ _ |- _⇒exact inst_step_kept_ _ _ _ _ _ _ Hfree E2end|inversion Hc ; subst ; apply kept_reflend

A step that allocates nothing changes memory as kept allows, where the genv's free does: its writes pass an access check, so they are inside an object, and it ends objects (free, and an invocation's locals) without moving one.

461Lemma step_next_kept
∀ ge c c′
Explore proof 4 tactics

Initial goal

⊢
∀ge : genv c c′ : config, free_keepsge_freege → stepge c = Nextc′ → keptc_memc c_memc′

unfold step , inst_next

⊢
∀ ge : genv c c′ : config  ,
→
match fr_atc_framec with
Snapshot_ :: _ as xs l
⇒
negbforallbsnapshot_word xs
→
Stuck"snapshot"
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
Enterl from
⇒
else
or_stuck"block"
Execl [ ] j
⇒
jump_stepge c l j
Execl i :: rest j
⇒
match let* why ≔ fr_doomedc_framec in if ahead_transparenti then None else Somewhy with
Somewhy
⇒
None
⇒
or_stuck"instruction"
let* out0 ≔ inst_stepge c_framec c_memc i in
let* od ≔ doomed_resultge c_framec c_memc i out0 in
Some
match fstod with
IContinuee locals m′
⇒
Nextc_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndod; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc
ICallg xs pd
⇒
match call_frameg xs with
Somecallee
⇒
Nextc_frame ≔ callee; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ sndod; fr_at ≔ Execl rest j, pd :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc
None
⇒
Stuck"call"
⇒
λ base : Z  ⇒
let p, m′ ≔ kbase in
let e, locals ≔ p in
c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndod; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc
⇒
Stuck"outside the core subset"
=
Nextc′
→

intros ge c c′ Hfree H

ge :
c, c′ :
H :
match fr_atc_framec with
Snapshot_ :: _ as xs l
⇒
negbforallbsnapshot_word xs
→
Stuck"snapshot"
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
Enterl from
⇒
else
or_stuck"block"
Execl [ ] j
⇒
jump_stepge c l j
Execl i :: rest j
⇒
match let* why ≔ fr_doomedc_framec in if ahead_transparenti then None else Somewhy with
Somewhy
⇒
None
⇒
or_stuck"instruction"
let* out0 ≔ inst_stepge c_framec c_memc i in
let* od ≔ doomed_resultge c_framec c_memc i out0 in
Some
match fstod with
IContinuee locals m′
⇒
Nextc_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndod; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc
ICallg xs pd
⇒
match call_frameg xs with
Somecallee
⇒
Nextc_frame ≔ callee; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ sndod; fr_at ≔ Execl rest j, pd :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc
None
⇒
Stuck"call"
⇒
λ base : Z  ⇒
let p, m′ ≔ kbase in
let e, locals ≔ p in
c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndod; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc
⇒
Stuck"outside the core subset"
=
Nextc′

cases H ; unstuck H

5 open

ge :
c, c′ :
xs :
listword
l :
Heql0 :
xs = [ ]
Heqp :
focused goal
ge :
c, c′ :
l :
from :
optionname
Heqp :
Heqb :
c_fuelc =? 0 = false
e :
Heqo0 :
phis_envge b_phisb from fr_envc_framec = Somee
H :
SomeNextc_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc − 1 = SomeNextc′
focused goal
ge :
c, c′ :
l :
insts :
listinst
j :
Heql0 :
insts = [ ]
Heqp :
fr_atc_framec = Execl [ ] j
H :
jump_stepge c l j = Nextc′
focused goal
ge :
c, c′ :
l :
insts :
listinst
j :
i :
l0 :
listinst
Heql0 :
insts = i :: l0
Heqp :
fr_atc_framec = Execl i :: l0 j
Heqo :
let* why ≔ fr_doomedc_framec in
else
Somewhy
=
None
Heqo0 :
inst_stepge c_framec c_memc i = Somei0
p :
inst_out × optionreason
Heqo1 :
doomed_resultge c_framec c_memc i i0 = Somep
e :
locals :
listname × optionZ
m :
Heqi1 :
fstp = IContinuee locals m
H :
SomeNextc_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndp; fr_at ≔ Execl l0 j; c_callers ≔ c_callersc; c_mem ≔ m; c_fuel ≔ c_fuelc = SomeNextc′
focused goal
ge :
c, c′ :
l :
insts :
listinst
j :
i :
l0 :
listinst
Heql0 :
insts = i :: l0
Heqp :
fr_atc_framec = Execl i :: l0 j
Heqo :
let* why ≔ fr_doomedc_framec in
else
Somewhy
=
None
Heqo0 :
inst_stepge c_framec c_memc i = Somei0
p :
inst_out × optionreason
Heqo1 :
doomed_resultge c_framec c_memc i i0 = Somep
f :
xs :
listword
Heqi1 :
fstp = ICallf xs pd
f0 :
Heqo2 :
call_framef xs = Somef0
H :
SomeNextc_frame ≔ f0; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ sndp; fr_at ≔ Execl l0 j, pd :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc = SomeNextc′

all: first|match goal withE : jump_step_ _ _ _ = Next_ |- _⇒exact jump_step_kept_ _ _ _ _ Eend|inversion H ; subst ; simpl ; first exact kept_refl_ | doomed_continue Hfree

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
unfold step , inst_next
intros ge c c′ Hfree H
all: first|match goal withE : jump_step_ _ _ _ = Next_ |- _⇒exact jump_step_kept_ _ _ _ _ Eend|inversion H ; subst ; simpl ; first exact kept_refl_ | doomed_continue Hfree

An allocation step: its request has a positive alignment, and what the step then writes, such as a variadic callee's argument snapshot, is inside the new object.

474Lemma step_fresh_kept
∀ ge c q k
stepge c = Freshq k
0 < req_alignq ∧ ∀base, keptallocatedc_memc q base c_memkbase
Explore proof 16 tactics

Initial goal

⊢
∀ge : genv c : config q : alloc_req k : Z → config, stepge c = Freshq k → 0 < req_alignq ∧ ∀base : Z, keptallocatedc_memc q base c_memkbase

unfold step , inst_next

⊢
∀ ge : genv c : config q : alloc_req k : Z → config  ,
match fr_atc_framec with
Snapshot_ :: _ as xs l
⇒
negbforallbsnapshot_word xs
→
Stuck"snapshot"
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
Enterl from
⇒
else
or_stuck"block"
Execl [ ] j
⇒
jump_stepge c l j
Execl i :: rest j
⇒
match let* why ≔ fr_doomedc_framec in if ahead_transparenti then None else Somewhy with
Somewhy
⇒
None
⇒
or_stuck"instruction"
let* out0 ≔ inst_stepge c_framec c_memc i in
let* od ≔ doomed_resultge c_framec c_memc i out0 in
Some
match fstod with
IContinuee locals m′
⇒
Nextc_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndod; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc
ICallg xs pd
⇒
match call_frameg xs with
Somecallee
⇒
Nextc_frame ≔ callee; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ sndod; fr_at ≔ Execl rest j, pd :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc
None
⇒
Stuck"call"
IFreshq0 k0
⇒
λ base : Z  ⇒
let p, m′ ≔ k0base in
let e, locals ≔ p in
c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndod; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc
⇒
Stuck"outside the core subset"
=
→
0 < req_alignq ∧ ∀base : Z, keptallocatedc_memc q base c_memkbase

intros ge c q k H

ge :
k :
Z → config
H :
match fr_atc_framec with
Snapshot_ :: _ as xs l
⇒
negbforallbsnapshot_word xs
→
Stuck"snapshot"
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
Enterl from
⇒
else
or_stuck"block"
Execl [ ] j
⇒
jump_stepge c l j
Execl i :: rest j
⇒
match let* why ≔ fr_doomedc_framec in if ahead_transparenti then None else Somewhy with
Somewhy
⇒
None
⇒
or_stuck"instruction"
let* out0 ≔ inst_stepge c_framec c_memc i in
let* od ≔ doomed_resultge c_framec c_memc i out0 in
Some
match fstod with
IContinuee locals m′
⇒
Nextc_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndod; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc
ICallg xs pd
⇒
match call_frameg xs with
Somecallee
⇒
Nextc_frame ≔ callee; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ sndod; fr_at ≔ Execl rest j, pd :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc
None
⇒
Stuck"call"
⇒
λ base : Z  ⇒
let p, m′ ≔ kbase in
let e, locals ≔ p in
c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndod; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc
⇒
Stuck"outside the core subset"
=
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedc_memc q base c_memkbase

cases H ; unstuck H ; try exfalso ; exact jump_step_not_fresh_ _ _ _ _ _ H

2 open

ge :
k :
Z → config
xs :
listword
l :
w :
l0 :
listword
Heql0 :
xs = w :: l0
Heqp :
fr_atc_framec = Snapshotw :: l0 l
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
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedc_memc q base c_memkbase
focused goal
ge :
k :
Z → config
l :
insts :
listinst
j :
i :
l0 :
listinst
Heql0 :
insts = i :: l0
Heqp :
fr_atc_framec = Execl i :: l0 j
Heqo :
let* why ≔ fr_doomedc_framec in
else
Somewhy
=
None
Heqo0 :
inst_stepge c_framec c_memc i = Somei0
p :
inst_out × optionreason
Heqo1 :
doomed_resultge c_framec c_memc i i0 = Somep
k0 :
Z → env × listname × optionZ × mem
Heqi1 :
fstp = IFreshq0 k0
H :
Some
λ base : Z  ⇒
let p0, m′ ≔ k0base in
let e, locals ≔ p0 in
c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndp; fr_at ≔ Execl l0 j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc
=
SomeFreshq k
⊢
0 < req_alignq ∧ ∀base : Z, keptallocatedc_memc q base c_memkbase

all: injection H as Hq Hk ; subst q k

2 open

ge :
xs :
listword
l :
w :
l0 :
listword
Heql0 :
xs = w :: l0
Heqp :
fr_atc_framec = Snapshotw :: l0 l
Heqb :
negbforallbsnapshot_word w :: l0 = false
⊢
0 < req_alignheap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthl0~0~0~0 ∧ ∀base : Z, keptallocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthl0~0~0~0 base c_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
focused goal
ge :
l :
insts :
listinst
j :
i :
l0 :
listinst
Heql0 :
insts = i :: l0
Heqp :
fr_atc_framec = Execl i :: l0 j
Heqo :
let* why ≔ fr_doomedc_framec in
else
Somewhy
=
None
Heqo0 :
inst_stepge c_framec c_memc i = Somei0
p :
inst_out × optionreason
Heqo1 :
doomed_resultge c_framec c_memc i i0 = Somep
k0 :
Z → env × listname × optionZ × mem
Heqi1 :
fstp = IFreshq0 k0
⊢
0 < req_alignq0
∧
∀ base : Z  ,
let p0, m′ ≔ k0base in
let e, locals ≔ p0 in
c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndp; fr_at ≔ Execl l0 j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc

–split ; simpl ; lia |

2 open

ge :
xs :
listword
l :
w :
l0 :
listword
Heql0 :
xs = w :: l0
Heqp :
fr_atc_framec = Snapshotw :: l0 l
Heqb :
negbforallbsnapshot_word w :: l0 = false
⊢
∀base : Z, keptallocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthl0~0~0~0 base c_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
deferred goal
ge :
l :
insts :
listinst
j :
i :
l0 :
listinst
Heql0 :
insts = i :: l0
Heqp :
fr_atc_framec = Execl i :: l0 j
Heqo :
let* why ≔ fr_doomedc_framec in
else
Somewhy
=
None
Heqo0 :
inst_stepge c_framec c_memc i = Somei0
p :
inst_out × optionreason
Heqo1 :
doomed_resultge c_framec c_memc i i0 = Somep
k0 :
Z → env × listname × optionZ × mem
Heqi1 :
fstp = IFreshq0 k0
⊢
0 < req_alignq0
∧
∀ base : Z  ,
let p0, m′ ≔ k0base in
let e, locals ≔ p0 in
c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndp; fr_at ≔ Execl l0 j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc

intros base

2 open

ge :
xs :
listword
l :
w :
l0 :
listword
Heql0 :
xs = w :: l0
Heqp :
fr_atc_framec = Snapshotw :: l0 l
Heqb :
negbforallbsnapshot_word w :: l0 = false
base :
Z
⊢
keptallocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthl0~0~0~0 base c_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
deferred goal
ge :
l :
insts :
listinst
j :
i :
l0 :
listinst
Heql0 :
insts = i :: l0
Heqp :
fr_atc_framec = Execl i :: l0 j
Heqo :
let* why ≔ fr_doomedc_framec in
else
Somewhy
=
None
Heqo0 :
inst_stepge c_framec c_memc i = Somei0
p :
inst_out × optionreason
Heqo1 :
doomed_resultge c_framec c_memc i i0 = Somep
k0 :
Z → env × listname × optionZ × mem
Heqi1 :
fstp = IFreshq0 k0
⊢
0 < req_alignq0
∧
∀ base : Z  ,
let p0, m′ ≔ k0base in
let e, locals ≔ p0 in
c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndp; fr_at ≔ Execl l0 j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc

match goal withHp : fr_at_ = Snapshot?xs _ |- _⇒exact snapshot_alloc_keptxs c_memc baseend

deferred goal
ge :
l :
insts :
listinst
j :
i :
l0 :
listinst
Heql0 :
insts = i :: l0
Heqp :
fr_atc_framec = Execl i :: l0 j
Heqo :
let* why ≔ fr_doomedc_framec in
else
Somewhy
=
None
Heqo0 :
inst_stepge c_framec c_memc i = Somei0
p :
inst_out × optionreason
Heqo1 :
doomed_resultge c_framec c_memc i i0 = Somep
k0 :
Z → env × listname × optionZ × mem
Heqi1 :
fstp = IFreshq0 k0
⊢
0 < req_alignq0
∧
∀ base : Z  ,
let p0, m′ ≔ k0base in
let e, locals ≔ p0 in
c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndp; fr_at ≔ Execl l0 j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc

–match goal withE : doomed_result_ _ _ _ _ = Some?od , Hc : fst?od = IFresh_ _ |- _⇒destruct doomed_result_out_ _ _ _ _ _ E as Ho | e′ & l′ & Ho | o′ & Ho ; rewrite Ho in Hc ; try discriminate Hcend

ge :
l :
insts :
listinst
j :
i :
l0 :
listinst
Heql0 :
insts = i :: l0
Heqp :
fr_atc_framec = Execl i :: l0 j
Heqo :
let* why ≔ fr_doomedc_framec in
else
Somewhy
=
None
Heqo0 :
inst_stepge c_framec c_memc i = Somei0
p :
inst_out × optionreason
Heqo1 :
doomed_resultge c_framec c_memc i i0 = Somep
k0 :
Z → env × listname × optionZ × mem
Heqi1 :
i0 = IFreshq0 k0
Ho :
fstp = i0
⊢
0 < req_alignq0
∧
∀ base : Z  ,
let p0, m′ ≔ k0base in
let e, locals ≔ p0 in
c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndp; fr_at ≔ Execl l0 j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc

subst

ge :
l :
j :
i :
l0 :
listinst
Heqp :
fr_atc_framec = Execl i :: l0 j
Heqo :
let* why ≔ fr_doomedc_framec in
else
Somewhy
=
None
k0 :
Z → env × listname × optionZ × mem
Heqo0 :
inst_stepge c_framec c_memc i = SomeIFreshq0 k0
p :
inst_out × optionreason
Heqo1 :
doomed_resultge c_framec c_memc i IFreshq0 k0 = Somep
Ho :
fstp = IFreshq0 k0
⊢
0 < req_alignq0
∧
∀ base : Z  ,
let p0, m′ ≔ k0base in
let e, locals ≔ p0 in
c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndp; fr_at ≔ Execl l0 j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc

match goal withE2 : inst_step_ _ _ _ = SomeIFresh_ _ |- _⇒destruct inst_step_fresh_ _ _ _ _ _ E2 as Ha Hkend

ge :
l :
j :
i :
l0 :
listinst
Heqp :
fr_atc_framec = Execl i :: l0 j
Heqo :
let* why ≔ fr_doomedc_framec in
else
Somewhy
=
None
k0 :
Z → env × listname × optionZ × mem
Heqo0 :
inst_stepge c_framec c_memc i = SomeIFreshq0 k0
p :
inst_out × optionreason
Heqo1 :
doomed_resultge c_framec c_memc i IFreshq0 k0 = Somep
Ho :
fstp = IFreshq0 k0
Ha :
0 < req_alignq0
Hk :
∀base : Z, keptallocatedc_memc q0 base sndk0base
⊢
0 < req_alignq0
∧
∀ base : Z  ,
let p0, m′ ≔ k0base in
let e, locals ≔ p0 in
c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndp; fr_at ≔ Execl l0 j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc

split ; auto

ge :
l :
j :
i :
l0 :
listinst
Heqp :
fr_atc_framec = Execl i :: l0 j
Heqo :
let* why ≔ fr_doomedc_framec in
else
Somewhy
=
None
k0 :
Z → env × listname × optionZ × mem
Heqo0 :
inst_stepge c_framec c_memc i = SomeIFreshq0 k0
p :
inst_out × optionreason
Heqo1 :
doomed_resultge c_framec c_memc i IFreshq0 k0 = Somep
Ho :
fstp = IFreshq0 k0
Ha :
0 < req_alignq0
Hk :
∀base : Z, keptallocatedc_memc q0 base sndk0base
⊢
∀ base : Z  ,
let p0, m′ ≔ k0base in
let e, locals ≔ p0 in
c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndp; fr_at ≔ Execl l0 j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc

intros base

ge :
l :
j :
i :
l0 :
listinst
Heqp :
fr_atc_framec = Execl i :: l0 j
Heqo :
let* why ≔ fr_doomedc_framec in
else
Somewhy
=
None
k0 :
Z → env × listname × optionZ × mem
Heqo0 :
inst_stepge c_framec c_memc i = SomeIFreshq0 k0
p :
inst_out × optionreason
Heqo1 :
doomed_resultge c_framec c_memc i IFreshq0 k0 = Somep
Ho :
fstp = IFreshq0 k0
Ha :
0 < req_alignq0
Hk :
∀base : Z, keptallocatedc_memc q0 base sndk0base
base :
Z
⊢
let p0, m′ ≔ k0base in
let e, locals ≔ p0 in
c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndp; fr_at ≔ Execl l0 j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc

specialize Hkbase

ge :
l :
j :
i :
l0 :
listinst
Heqp :
fr_atc_framec = Execl i :: l0 j
Heqo :
let* why ≔ fr_doomedc_framec in
else
Somewhy
=
None
k0 :
Z → env × listname × optionZ × mem
Heqo0 :
inst_stepge c_framec c_memc i = SomeIFreshq0 k0
p :
inst_out × optionreason
Heqo1 :
doomed_resultge c_framec c_memc i IFreshq0 k0 = Somep
Ho :
fstp = IFreshq0 k0
Ha :
0 < req_alignq0
base :
Z
Hk :
keptallocatedc_memc q0 base sndk0base
⊢
let p0, m′ ≔ k0base in
let e, locals ≔ p0 in
c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndp; fr_at ≔ Execl l0 j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc

simpl

ge :
l :
j :
i :
l0 :
listinst
Heqp :
fr_atc_framec = Execl i :: l0 j
Heqo :
let* why ≔ fr_doomedc_framec in
else
Somewhy
=
None
k0 :
Z → env × listname × optionZ × mem
Heqo0 :
inst_stepge c_framec c_memc i = SomeIFreshq0 k0
p :
inst_out × optionreason
Heqo1 :
doomed_resultge c_framec c_memc i IFreshq0 k0 = Somep
Ho :
fstp = IFreshq0 k0
Ha :
0 < req_alignq0
base :
Z
Hk :
keptallocatedc_memc q0 base sndk0base
⊢
let p0, m′ ≔ k0base in
let e, locals ≔ p0 in
c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ sndp; fr_at ≔ Execl l0 j; c_callers ≔ c_callersc; c_mem ≔ m′; c_fuel ≔ c_fuelc

match goal withHk : kept_ snd?t |- _⇒destruct t as e1 l1 m1end

ge :
l :
j :
i :
l0 :
listinst
Heqp :
fr_atc_framec = Execl i :: l0 j
Heqo :
let* why ≔ fr_doomedc_framec in
else
Somewhy
=
None
k0 :
Z → env × listname × optionZ × mem
Heqo0 :
inst_stepge c_framec c_memc i = SomeIFreshq0 k0
p :
inst_out × optionreason
Heqo1 :
doomed_resultge c_framec c_memc i IFreshq0 k0 = Somep
Ho :
fstp = IFreshq0 k0
Ha :
0 < req_alignq0
base :
Z
e1 :
l1 :
listname × optionZ
m1 :
Hk :
keptallocatedc_memc q0 base snde1, l1, m1
⊢
keptallocatedc_memc q0 base c_memc_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e1; fr_locals ≔ l1; fr_doomed ≔ sndp; fr_at ≔ Execl l0 j; c_callers ≔ c_callersc; c_mem ≔ m1; c_fuel ≔ c_fuelc

exact Hk

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
unfold step , inst_next
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
–split ; simpl ; lia |
intros base
match goal withHp : fr_at_ = Snapshot?xs _ |- _⇒exact snapshot_alloc_keptxs c_memc baseend
–match goal withE : doomed_result_ _ _ _ _ = Some?od , Hc : fst?od = 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_ _ |- _⇒destruct inst_step_fresh_ _ _ _ _ _ E2 as Ha Hkend
split ; auto
intros base
specialize Hkbase
simpl
match goal withHk : kept_ snd?t |- _⇒destruct t as e1 l1 m1end
exact Hk

The machine of a runtime

The machine of a runtime R: one thread's program run under R, and the proof that R stays ready in every state of a run.

501Module Machine R : Runtime

A machine state: the configuration and the runtime's state.

504Definition mstate: Type ≔
config × R.state%type

The configuration c with its memory replaced by m.

507Definition with_memc : config m : mem : config ≔

The edge the jump j of the frame fr takes, read as jump_step reads it; None for a return or unreachable.

512Definition taken_targetge : genv fr : frame j : jump : optiontarget ≔
match j with
⇒
Somet
JBranchv t1 t2
⇒
match value_xge fr_envfr W v with
SomeWIntn
⇒
Some
n =? 0
→
t2
else
t1
_
⇒
None
_
⇒
None

The runtime may act now, in the configuration c: before c's next instruction where R.at_safepoint holds, or before a poll edge is taken.

526Definition safepoint_duege : genv c : config : bool ≔
match fr_atc_framec with
Exec_ i :: _ _
⇒
R.at_safepointi
Exec_ [ ] j
⇒
match taken_targetge c_framec j with
SomePoll_
⇒
true
_
⇒
false
_
⇒
false

A machine step:

  • mstep_next: a step that allocates nothing;
  • mstep_alloc: an allocation at R's alloc, taking its base and R's next state; where R refuses (out of memory) there is no step, and the run traps;
  • mstep_safepoint: R's action at a safepoint, where one is due: R.safepoint may change memory and R's state.
541Inductive mstepge : genv : mstate → mstate → Prop ≔
∀ c c′ s
stepge c = Nextc′
mstep_next
mstepge c, s c′, s
∀ c q k s base s′
stepge c = Freshq k
0 ≤ req_extentq
R.allocs q = Somebase, s′
mstep_alloc
mstepge c, s kbase, s′
∀ c s s′ m′
safepoint_duege c = true
R.safepoints c_memc s′ m′
mstep_safepoint
mstepge c, s with_memc m′, s′

The machine state st' follows st after any number of machine steps.

557Definition mreachablege : genv : mstate → mstate → Prop ≔
clos_refl_transmstate mstepge

The runtime is ready to allocate in the memory: R.ready of the runtime's state and the configuration's memory.

562Definition ready_statest : mstate : Prop ≔
R.readysndst c_memfstst

R's free changes memory as kept allows, by R's free_lifetime and retention.

566Lemma free_kept
Explore proof 7 tactics

Initial goal

⊢

intros x m r m′ H

x :
m :
r :
resunit
m′ :
H :
R.freex m = Somer, m′
⊢
keptm m′

split

2 open

x :
m :
r :
resunit
m′ :
H :
R.freex m = Somer, m′
⊢
focused goal
x :
m :
r :
resunit
m′ :
H :
R.freex m = Somer, m′
⊢
∀a : Z, ¬in_objectm a → m_bytesm′ a = m_bytesm a ∧ m_auxm′ a = m_auxm a

–apply lifetime_region_step

2 open

x :
m :
r :
resunit
m′ :
H :
R.freex m = Somer, m′
⊢
deferred goal
x :
m :
r :
resunit
m′ :
H :
R.freex m = Somer, m′
⊢
∀a : Z, ¬in_objectm a → m_bytesm′ a = m_bytesm a ∧ m_auxm′ a = m_auxm a

eapply R.free_lifetime ; eauto

deferred goal
x :
m :
r :
resunit
m′ :
H :
R.freex m = Somer, m′
⊢
∀a : Z, ¬in_objectm a → m_bytesm′ a = m_bytesm a ∧ m_auxm′ a = m_auxm a

–intros a _

x :
m :
r :
resunit
m′ :
H :
R.freex m = Somer, m′
a :
Z
⊢
m_bytesm′ a = m_bytesm a ∧ m_auxm′ a = m_auxm a

destruct R.retention_ _ _ _ H as → →

x :
m :
r :
resunit
m′ :
H :
R.freex m = Somer, m′
a :
Z
⊢
m_bytesm a = m_bytesm a ∧ m_auxm a = m_auxm a

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros x m r m′ H
split
eapply R.free_lifetime ; eauto
–intros a _
destruct R.retention_ _ _ _ H as → →
auto

Every machine step keeps the runtime ready, where the genv's free is R's:

  • a step that allocates nothing changes memory only as kept allows (step_next_kept), so R's ready_kept applies;
  • an allocation is R's fresh_allocation, and what the step then writes is inside the new object (step_fresh_kept);
  • a safepoint is R's safepoint_ready.
580Theorem mstep_ready
∀ ge st st′
ge_freege = R.free
mstepge st st′
Explore proof 14 tactics

Initial goal

⊢
∀ge : genv st st′ : mstate, ge_freege = R.free → mstepge st st′ → ready_statest → ready_statest′

unfold ready_state

⊢
∀ge : genv st st′ : mstate, ge_freege = R.free → mstepge st st′ → R.readysndst c_memfstst → R.readysndst′ c_memfstst′

intros ge st st′ Hge Hs Hr

ge :
st, st′ :
Hge :
ge_freege = R.free
Hs :
mstepge st st′
Hr :
R.readysndst c_memfstst
⊢
R.readysndst′ c_memfstst′

destruct Hs as c c′ s E | c q k s base s′ E He Hal | c s s′ m′ _ Hsp

3 open

ge :
Hge :
ge_freege = R.free
c, c′ :
s :
R.state
E :
stepge c = Nextc′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndc′, s c_memfstc′, s
focused goal
ge :
Hge :
ge_freege = R.free
k :
Z → config
s :
R.state
base :
Z
s′ :
R.state
E :
stepge c = Freshq k
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndkbase, s′ c_memfstkbase, s′
focused goal
ge :
Hge :
ge_freege = R.free
s, s′ :
R.state
m′ :
Hsp :
R.safepoints c_memc s′ m′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndwith_memc m′, s′ c_memfstwith_memc m′, s′

–simpl in *

3 open

ge :
Hge :
ge_freege = R.free
c, c′ :
s :
R.state
E :
stepge c = Nextc′
Hr :
R.readys c_memc
⊢
R.readys c_memc′
deferred goal
ge :
Hge :
ge_freege = R.free
k :
Z → config
s :
R.state
base :
Z
s′ :
R.state
E :
stepge c = Freshq k
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndkbase, s′ c_memfstkbase, s′
deferred goal
ge :
Hge :
ge_freege = R.free
s, s′ :
R.state
m′ :
Hsp :
R.safepoints c_memc s′ m′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndwith_memc m′, s′ c_memfstwith_memc m′, s′

eapply R.ready_kept ; exact Hr |

3 open

ge :
Hge :
ge_freege = R.free
c, c′ :
s :
R.state
E :
stepge c = Nextc′
Hr :
R.readys c_memc
deferred goal
ge :
Hge :
ge_freege = R.free
k :
Z → config
s :
R.state
base :
Z
s′ :
R.state
E :
stepge c = Freshq k
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndkbase, s′ c_memfstkbase, s′
deferred goal
ge :
Hge :
ge_freege = R.free
s, s′ :
R.state
m′ :
Hsp :
R.safepoints c_memc s′ m′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndwith_memc m′, s′ c_memfstwith_memc m′, s′

eapply step_next_kept ; | exact E

3 open

ge :
Hge :
ge_freege = R.free
c, c′ :
s :
R.state
E :
stepge c = Nextc′
Hr :
R.readys c_memc
deferred goal
ge :
Hge :
ge_freege = R.free
k :
Z → config
s :
R.state
base :
Z
s′ :
R.state
E :
stepge c = Freshq k
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndkbase, s′ c_memfstkbase, s′
deferred goal
ge :
Hge :
ge_freege = R.free
s, s′ :
R.state
m′ :
Hsp :
R.safepoints c_memc s′ m′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndwith_memc m′, s′ c_memfstwith_memc m′, s′

rewrite Hge

3 open

ge :
Hge :
ge_freege = R.free
c, c′ :
s :
R.state
E :
stepge c = Nextc′
Hr :
R.readys c_memc
⊢
deferred goal
ge :
Hge :
ge_freege = R.free
k :
Z → config
s :
R.state
base :
Z
s′ :
R.state
E :
stepge c = Freshq k
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndkbase, s′ c_memfstkbase, s′
deferred goal
ge :
Hge :
ge_freege = R.free
s, s′ :
R.state
m′ :
Hsp :
R.safepoints c_memc s′ m′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndwith_memc m′, s′ c_memfstwith_memc m′, s′

exact free_kept

2 open

deferred goal
ge :
Hge :
ge_freege = R.free
k :
Z → config
s :
R.state
base :
Z
s′ :
R.state
E :
stepge c = Freshq k
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndkbase, s′ c_memfstkbase, s′
deferred goal
ge :
Hge :
ge_freege = R.free
s, s′ :
R.state
m′ :
Hsp :
R.safepoints c_memc s′ m′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndwith_memc m′, s′ c_memfstwith_memc m′, s′

–simpl in *

2 open

ge :
Hge :
ge_freege = R.free
k :
Z → config
s :
R.state
base :
Z
s′ :
R.state
E :
stepge c = Freshq k
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
Hr :
R.readys c_memc
⊢
R.readys′ c_memkbase
deferred goal
ge :
Hge :
ge_freege = R.free
s, s′ :
R.state
m′ :
Hsp :
R.safepoints c_memc s′ m′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndwith_memc m′, s′ c_memfstwith_memc m′, s′

destruct step_fresh_kept_ _ _ _ E as Ha Hk

2 open

ge :
Hge :
ge_freege = R.free
k :
Z → config
s :
R.state
base :
Z
s′ :
R.state
E :
stepge c = Freshq k
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
Hr :
R.readys c_memc
Ha :
0 < req_alignq
Hk :
∀base : Z, keptallocatedc_memc q base c_memkbase
⊢
R.readys′ c_memkbase
deferred goal
ge :
Hge :
ge_freege = R.free
s, s′ :
R.state
m′ :
Hsp :
R.safepoints c_memc s′ m′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndwith_memc m′, s′ c_memfstwith_memc m′, s′

destruct R.fresh_allocation_ _ _ _ _ Hr Ha He Hal as _ Hr′

2 open

ge :
Hge :
ge_freege = R.free
k :
Z → config
s :
R.state
base :
Z
s′ :
R.state
E :
stepge c = Freshq k
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
Hr :
R.readys c_memc
Ha :
0 < req_alignq
Hk :
∀base : Z, keptallocatedc_memc q base c_memkbase
Hr′ :
R.readys′ allocatedc_memc q base
⊢
R.readys′ c_memkbase
deferred goal
ge :
Hge :
ge_freege = R.free
s, s′ :
R.state
m′ :
Hsp :
R.safepoints c_memc s′ m′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndwith_memc m′, s′ c_memfstwith_memc m′, s′

eapply R.ready_kept ; exact Hr′ | apply Hk

deferred goal
ge :
Hge :
ge_freege = R.free
s, s′ :
R.state
m′ :
Hsp :
R.safepoints c_memc s′ m′
Hr :
R.readysndc, s c_memfstc, s
⊢
R.readysndwith_memc m′, s′ c_memfstwith_memc m′, s′

–simpl in *

ge :
Hge :
ge_freege = R.free
s, s′ :
R.state
m′ :
Hsp :
R.safepoints c_memc s′ m′
Hr :
R.readys c_memc
⊢
R.readys′ m′

eapply R.safepoint_ready ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros ge st st′ Hge Hs Hr
destruct Hs as c c′ s E | c q k s base s′ E He Hal | c s s′ m′ _ Hsp
–simpl in *
eapply R.ready_kept ; exact Hr |
eapply step_next_kept ; | exact E
rewrite Hge
exact free_kept
–simpl in *
destruct step_fresh_kept_ _ _ _ E as Ha Hk
destruct R.fresh_allocation_ _ _ _ _ Hr Ha He Hal as _ Hr′
eapply R.ready_kept ; exact Hr′ | apply Hk
–simpl in *
eapply R.safepoint_ready ; eauto

Ready initially, ready ever after: if the runtime is ready in st and the genv's free is R's, it is ready in every state a run from st reaches.

595Theorem mreachable_ready
∀ ge st st′
ge_freege = R.free
mreachablege st st′
Explore proof 3 tactics

Initial goal

⊢
∀ge : genv st st′ : mstate, ge_freege = R.free → mreachablege st st′ → ready_statest → ready_statest′

intros ge st st′ Hge H

ge :
st, st′ :
Hge :
ge_freege = R.free
H :
mreachablege st st′
⊢

induction H as st st′ Hs | st | st1 st2 st3 _ IH1 _ IH2 ; auto

ge :
Hge :
ge_freege = R.free
st, st′ :
Hs :
mstepge st st′
⊢

eapply mstep_ready ; eauto

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 _ IH1 _ IH2 ; auto
eapply mstep_ready ; eauto

Ready initially, no object of any state a run reaches ends past 2^48 (R's address_space): the coverage lemma's objects_fit hypothesis (Coverage.v) holds in every state of a run that starts ready.

606Corollary mreachable_objects_fit
∀ ge st st′
ge_freege = R.free
mreachablege st st′
Explore proof 3 tactics

Initial goal

⊢
∀ge : genv st st′ : mstate, ge_freege = R.free → mreachablege st st′ → ready_statest → objects_fitm_regionsc_memfstst′

intros ge st st′ Hge H Hr

ge :
st, st′ :
Hge :
ge_freege = R.free
H :
mreachablege st st′

apply R.address_spacesndst′

ge :
st, st′ :
Hge :
ge_freege = R.free
H :
mreachablege st st′
⊢
R.readysndst′ c_memfstst′

exact mreachable_ready_ _ _ Hge H Hr

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros ge st st′ Hge H Hr
apply R.address_spacesndst′
exact mreachable_ready_ _ _ Hge H Hr

The machine refines the step relation: from a ready state, a machine step is a step of step_rel, its allocation's base fresh, or the runtime's action at a safepoint that was due. So whatever the soundness theorem proves of step_rel and the safepoint relation holds of every run of every runtime.

619Theorem mstep_refines
∀ ge c s c′ s′
mstepge c, s c′, s′
step_relge c c′ ∨ safepoint_duege c = true ∧ ∃m′, c′ = with_memc m′ ∧ R.safepoints c_memc s′ m′
Explore proof 13 tactics

Initial goal

⊢
∀ge : genv c : config s : R.state c′ : config s′ : R.state, ready_statec, s → mstepge c, s c′, s′ → step_relge c c′ ∨ safepoint_duege c = true ∧ ∃m′ : mem, c′ = with_memc m′ ∧ R.safepoints c_memc s′ m′

unfold ready_state

⊢
∀ge : genv c : config s : R.state c′ : config s′ : R.state, R.readysndc, s c_memfstc, s → mstepge c, s c′, s′ → step_relge c c′ ∨ safepoint_duege c = true ∧ ∃m′ : mem, c′ = with_memc m′ ∧ R.safepoints c_memc s′ m′

simpl

⊢
∀ge : genv c : config s : R.state c′ : config s′ : R.state, R.readys c_memc → mstepge c, s c′, s′ → step_relge c c′ ∨ safepoint_duege c = true ∧ ∃m′ : mem, c′ = with_memc m′ ∧ R.safepoints c_memc s′ m′

intros ge c s c′ s′ Hr Hs

ge :
s :
R.state
c′ :
s′ :
R.state
Hr :
R.readys c_memc
Hs :
mstepge c, s c′, s′
⊢
step_relge c c′ ∨ safepoint_duege c = true ∧ ∃m′ : mem, c′ = with_memc m′ ∧ R.safepoints c_memc s′ m′

inversion Hs as c0 c1 s0 E | c0 q k s0 base s1 E He Hal | c0 s0 s1 m′ Hd Hsp ; subst

3 open

ge :
c, c′ :
s′ :
R.state
Hs :
mstepge c, s′ c′, s′
Hr :
R.readys′ c_memc
E :
stepge c = Nextc′
⊢
step_relge c c′ ∨ safepoint_duege c = true ∧ ∃m′ : mem, c′ = with_memc m′ ∧ R.safepoints′ c_memc s′ m′
focused goal
ge :
s, s′ :
R.state
Hr :
R.readys c_memc
k :
Z → config
base :
Z
Hs :
mstepge c, s kbase, s′
E :
stepge c = Freshq k
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
⊢
step_relge c kbase ∨ safepoint_duege c = true ∧ ∃m′ : mem, kbase = with_memc m′ ∧ R.safepoints c_memc s′ m′
focused goal
ge :
s, s′ :
R.state
Hr :
R.readys c_memc
m′ :
Hs :
mstepge c, s with_memc m′, s′
Hd :
safepoint_duege c = true
Hsp :
R.safepoints c_memc s′ m′
⊢
step_relge c with_memc m′ ∨ safepoint_duege c = true ∧ ∃m'0 : mem, with_memc m′ = with_memc m'0 ∧ R.safepoints c_memc s′ m'0

–left

3 open

ge :
c, c′ :
s′ :
R.state
Hs :
mstepge c, s′ c′, s′
Hr :
R.readys′ c_memc
E :
stepge c = Nextc′
⊢
step_relge c c′
deferred goal
ge :
s, s′ :
R.state
Hr :
R.readys c_memc
k :
Z → config
base :
Z
Hs :
mstepge c, s kbase, s′
E :
stepge c = Freshq k
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
⊢
step_relge c kbase ∨ safepoint_duege c = true ∧ ∃m′ : mem, kbase = with_memc m′ ∧ R.safepoints c_memc s′ m′
deferred goal
ge :
s, s′ :
R.state
Hr :
R.readys c_memc
m′ :
Hs :
mstepge c, s with_memc m′, s′
Hd :
safepoint_duege c = true
Hsp :
R.safepoints c_memc s′ m′
⊢
step_relge c with_memc m′ ∨ safepoint_duege c = true ∧ ∃m'0 : mem, with_memc m′ = with_memc m'0 ∧ R.safepoints c_memc s′ m'0

apply step_next

3 open

ge :
c, c′ :
s′ :
R.state
Hs :
mstepge c, s′ c′, s′
Hr :
R.readys′ c_memc
E :
stepge c = Nextc′
⊢
stepge c = Nextc′
deferred goal
ge :
s, s′ :
R.state
Hr :
R.readys c_memc
k :
Z → config
base :
Z
Hs :
mstepge c, s kbase, s′
E :
stepge c = Freshq k
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
⊢
step_relge c kbase ∨ safepoint_duege c = true ∧ ∃m′ : mem, kbase = with_memc m′ ∧ R.safepoints c_memc s′ m′
deferred goal
ge :
s, s′ :
R.state
Hr :
R.readys c_memc
m′ :
Hs :
mstepge c, s with_memc m′, s′
Hd :
safepoint_duege c = true
Hsp :
R.safepoints c_memc s′ m′
⊢
step_relge c with_memc m′ ∨ safepoint_duege c = true ∧ ∃m'0 : mem, with_memc m′ = with_memc m'0 ∧ R.safepoints c_memc s′ m'0

exact E

2 open

deferred goal
ge :
s, s′ :
R.state
Hr :
R.readys c_memc
k :
Z → config
base :
Z
Hs :
mstepge c, s kbase, s′
E :
stepge c = Freshq k
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
⊢
step_relge c kbase ∨ safepoint_duege c = true ∧ ∃m′ : mem, kbase = with_memc m′ ∧ R.safepoints c_memc s′ m′
deferred goal
ge :
s, s′ :
R.state
Hr :
R.readys c_memc
m′ :
Hs :
mstepge c, s with_memc m′, s′
Hd :
safepoint_duege c = true
Hsp :
R.safepoints c_memc s′ m′
⊢
step_relge c with_memc m′ ∨ safepoint_duege c = true ∧ ∃m'0 : mem, with_memc m′ = with_memc m'0 ∧ R.safepoints c_memc s′ m'0

–left

2 open

ge :
s, s′ :
R.state
Hr :
R.readys c_memc
k :
Z → config
base :
Z
Hs :
mstepge c, s kbase, s′
E :
stepge c = Freshq k
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
⊢
step_relge c kbase
deferred goal
ge :
s, s′ :
R.state
Hr :
R.readys c_memc
m′ :
Hs :
mstepge c, s with_memc m′, s′
Hd :
safepoint_duege c = true
Hsp :
R.safepoints c_memc s′ m′
⊢
step_relge c with_memc m′ ∨ safepoint_duege c = true ∧ ∃m'0 : mem, with_memc m′ = with_memc m'0 ∧ R.safepoints c_memc s′ m'0

destruct step_fresh_kept_ _ _ _ E as Ha _

2 open

ge :
s, s′ :
R.state
Hr :
R.readys c_memc
k :
Z → config
base :
Z
Hs :
mstepge c, s kbase, s′
E :
stepge c = Freshq k
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
Ha :
0 < req_alignq
⊢
step_relge c kbase
deferred goal
ge :
s, s′ :
R.state
Hr :
R.readys c_memc
m′ :
Hs :
mstepge c, s with_memc m′, s′
Hd :
safepoint_duege c = true
Hsp :
R.safepoints c_memc s′ m′
⊢
step_relge c with_memc m′ ∨ safepoint_duege c = true ∧ ∃m'0 : mem, with_memc m′ = with_memc m'0 ∧ R.safepoints c_memc s′ m'0

destruct R.fresh_allocation_ _ _ _ _ Hr Ha He Hal as Hf _

2 open

ge :
s, s′ :
R.state
Hr :
R.readys c_memc
k :
Z → config
base :
Z
Hs :
mstepge c, s kbase, s′
E :
stepge c = Freshq k
He :
0 ≤ req_extentq
Hal :
R.allocs q = Somebase, s′
Ha :
0 < req_alignq
Hf :
freshc_memc q base
⊢
step_relge c kbase
deferred goal
ge :
s, s′ :
R.state
Hr :
R.readys c_memc
m′ :
Hs :
mstepge c, s with_memc m′, s′
Hd :
safepoint_duege c = true
Hsp :
R.safepoints c_memc s′ m′
⊢
step_relge c with_memc m′ ∨ safepoint_duege c = true ∧ ∃m'0 : mem, with_memc m′ = with_memc m'0 ∧ R.safepoints c_memc s′ m'0

eapply step_fresh ; eauto

deferred goal
ge :
s, s′ :
R.state
Hr :
R.readys c_memc
m′ :
Hs :
mstepge c, s with_memc m′, s′
Hd :
safepoint_duege c = true
Hsp :
R.safepoints c_memc s′ m′
⊢
step_relge c with_memc m′ ∨ safepoint_duege c = true ∧ ∃m'0 : mem, with_memc m′ = with_memc m'0 ∧ R.safepoints c_memc s′ m'0

–right

ge :
s, s′ :
R.state
Hr :
R.readys c_memc
m′ :
Hs :
mstepge c, s with_memc m′, s′
Hd :
safepoint_duege c = true
Hsp :
R.safepoints c_memc s′ m′
⊢
safepoint_duege c = true ∧ ∃m'0 : mem, with_memc m′ = with_memc m'0 ∧ R.safepoints c_memc s′ m'0

eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
simpl
intros ge c s c′ s′ Hr Hs
inversion Hs as c0 c1 s0 E | c0 q k s0 base s1 E He Hal | c0 s0 s1 m′ Hd Hsp ; subst
–left
apply step_next
exact E
–left
destruct step_fresh_kept_ _ _ _ E as Ha _
destruct R.fresh_allocation_ _ _ _ _ Hr Ha He Hal as Hf _
eapply step_fresh ; eauto
–right
eauto