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
| Decision | Why |
|---|---|
the runtime acts *before* an at_safepoint instruction or a poll edge | the instruction then runs on what the runtime left, as native code does after a pollcheck |
| an allocation with a negative extent has no machine step | fresh_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 free | Runtime.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 |
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.
What the program does to memory
Leaving memory as it is is kept.
Explore proof 2 tactics
Two kept changes in a row, from m1 to m2 and m2 to m3, are one kept change.
Explore proof 20 tactics
Initial goal
intros m1 m2 m3 R12 & O12 R23 & O23
split
2 openfocused goal
–intros b reg3 E3
2 opendeferred goal
destruct R23_ _ E3 as reg2 & E2 & H23
2 opendeferred goal
destruct R12_ _ E2 as reg1 & E1 & H12
2 opendeferred goal
exists reg1
2 opendeferred goal
split ; auto
2 opendeferred goal
destruct H23 as → | L2 & → ; destruct H12 as → | L1 & → ; auto
deferred goal
–intros a Hn
assert Hn2 : ¬in_objectm2 a
2 openfocused goal
{intros b & reg2 & E2 & Hr
2 opendeferred goal
destruct R12_ _ E2 as reg1 & E1 & → | _ & →
3 openfocused goal
deferred goal
–apply Hn
3 opendeferred goal
deferred goal
exists b, reg1
3 opendeferred goal
deferred goal
auto
2 opendeferred goal
deferred goal
–simpl in Hr
2 opendeferred goal
lia
deferred goal
destruct O12a Hn as B1 A1
destruct O23a Hn2 as B2 A2
split ; congruence
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A change the runtime's free may make (lifetime_step) is one the program may make (region_step): it ends only live objects.
Explore proof 5 tactics
Initial goal
intros m m′ H b reg′ E
destruct H_ _ E as reg & E0 & → | Hk & Hl & → ; exists reg ; split ; auto
right
rewrite Hk
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Every memory change the function free makes is kept: what a free that meets the lifetime and retention axioms does.
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.
Explore proof 3 tactics
Initial goal
unfold access_res , cap_access_res
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
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Writing size bytes at a is kept if they are all inside objects.
Explore proof 15 tactics
Initial goal
intros m a size x Hin
split
2 openfocused goal
–intros b reg′ E
2 opendeferred goal
exists reg′
2 opendeferred goal
split ; exact E | auto
deferred goal
–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
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Storing a capability in the aux at a is kept if a is inside an object.
Explore proof 12 tactics
Initial goal
intros m a c Hin
split
2 open–intros b reg′ E
2 openexists reg′
2 opensplit ; exact E | auto
–intros b Hn
simpl
split ; auto
destruct Z.eqbb a eqn: E ; auto
apply Z.eqb_eq in E
subst
contradiction
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Writes leave the objects where they were: an address inside an object before a byte write is inside one after it.
Explore proof 1 tactics
Initial goal
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The same for a capability stored in the aux.
Explore proof 1 tactics
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.
Explore proof 3 tactics
Initial goal
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
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A fold of memory changes that starts from no memory ends with none.
Explore proof 2 tactics
Initial goal
intros A f xs
induction xs ; simpl ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
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.
Explore proof 10 tactics
Initial goal
intros A P f xs
induction xs as | x xs IH ; simpl ; intros m0 m′ H0 Hf H
2 open–inversion H ; subst
2 openapply kept_refl
–destruct fm0 x as m1 | eqn: E
2 open+destruct Hf_ _ _ H0 E as H1 K1
2 openeapply kept_trans ; exact K1 |
2 openeapply IH ; eauto
+rewrite fold_left_none in H
discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
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.
Explore proof 20 tactics
Initial goal
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
2 openfocused goal
{intros b Hb
2 opendeferred goal
unfold in_object
2 opendeferred goal
rewrite Hr
2 opendeferred goal
apply Hin
2 opendeferred goal
auto
deferred goal
destruct e ; simpl in E ; try discriminate ; inversion E ; subst ; split ; auto using kept_refl
3 openfocused goal
focused goal
–apply store_aux_kept , Hin1
3 opendeferred goal
deferred goal
lia
2 opendeferred goal
deferred goal
–apply store_bytes_kept
2 opendeferred goal
exact Hin1
deferred goal
–eapply kept_trans ; | apply store_bytes_kept
2 openfocused goal
+apply store_aux_kept , Hin1
2 opendeferred goal
lia
deferred goal
+intros b Hb
apply in_object_store_aux , Hin1
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Reading a variadic argument (va_arg_res/4) is kept: its one write is a checked store.
Explore proof 3 tactics
Initial goal
unfold va_arg_res
intros k p m r m′ H
cases H;match type of H withSome_, = Some_, ⇒assert x = y as ← by congruenceend;first
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
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.
Explore proof 3 tactics
Initial goal
unfold op_res_int
intros o k xs m r m′ H
destruct o ; cases H ; inversion H ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An op that gives a result changes memory as kept allows.
Explore proof 3 tactics
Initial goal
unfold op_res , float_integer
intros o k xs m r m′ H
destruct o ; cases H ; inversion H ; subst;first
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Only the op alloc allocates: a heap object with a positive alignment, and it writes nothing into the new memory.
Proof 4 steps Qed
Ending an invocation's locals (invalidate_locals/3) is kept: it ends live stack objects, and writes nothing.
Explore proof 20 tactics
Initial goal
unfold invalidate_locals
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 _ _ = 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
2 openfocused goal
–apply Z.eqb_eq in Ez
2 opendeferred goal
subst
2 opendeferred goal
inversion Eb ; subst
2 opendeferred goal
eexists
3 opendeferred goal
shelved goal
split ; eassumption |
2 opendeferred goal
right
2 opendeferred goal
split ; assumption |
2 opendeferred goal
f_equal
2 opendeferred goal
symmetry
2 opendeferred goal
assumption
deferred goal
–exists reg′
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
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.
Explore proof 26 tactics
Initial goal
induction xs as | x xs IH ; simpl ; intros a m Hin
2 open–apply kept_refl
–destruct x as n | p | c size
3 openfocused goal
focused goal
+eapply kept_trans ; | apply IH
4 openfocused goal
deferred goal
deferred goal
∗apply store_bytes_kept
4 opendeferred goal
deferred goal
deferred goal
intros b Hb
4 opendeferred goal
deferred goal
deferred goal
apply Hin
4 opendeferred goal
deferred goal
deferred goal
lia
3 opendeferred goal
deferred goal
deferred goal
∗intros b Hb
3 opendeferred goal
deferred goal
apply in_object_store_bytes , Hin
3 opendeferred goal
deferred goal
lia
2 opendeferred goal
deferred goal
+eapply kept_trans ; | apply IH
3 openfocused goal
deferred goal
∗eapply kept_trans ; | apply store_aux_kept
4 openfocused goal
deferred goal
deferred goal
--apply store_bytes_kept
4 opendeferred goal
deferred goal
deferred goal
intros b Hb
4 opendeferred goal
deferred goal
deferred goal
apply Hin
4 opendeferred goal
deferred goal
deferred goal
lia
3 opendeferred goal
deferred goal
deferred goal
--apply in_object_store_bytes , Hin
3 opendeferred goal
deferred goal
lia
2 opendeferred goal
deferred goal
∗intros b Hb
2 opendeferred goal
apply in_object_store_aux , in_object_store_bytes , Hin
2 opendeferred goal
lia
deferred goal
+apply IH
intros b Hb
apply Hin
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A heap request's extent covers its size: the runtime is asked for at least as many bytes as the object needs.
Explore proof 5 tactics
Initial goal
intros align size
simpl
pose proof Z.div_modsize + 15 16 ltac:lia
pose proof Z.mod_pos_boundsize + 15 16 ltac:lia
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
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.
Explore proof 5 tactics
Initial goal
intros m q base b Hb
exists base, mkRegionbase base + req_extentq req_kindq Live
simpl
rewrite Z.eqb_refl
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A variadic callee's snapshot is written into its new object.
Explore proof 7 tactics
Initial goal
intros xs m base q
apply snapshot_kept
intros b Hb
apply in_allocated
pose proof heap_req_extent16 8 × Z.of_natlengthxs
unfold q
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The instruction i is the one doomed_result/5 reads: a check_ahead.
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.
Explore proof 6 tactics
Initial goal
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
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
doomed_result (doomed_result/5) passes the instruction's result on, or continues with the memory unchanged, or stops.
Explore proof 10 tactics
Initial goal
intros ge fr m i out od H
destruct ahead_insti eqn: Ea
2 open–destruct i ; try discriminate Ea
2 opendestruct k ; try discriminate Ea
2 opendestruct o ; try discriminate Ea
2 opendestruct args as | v | v′ args ; try discriminate Ea
2 openunfold doomed_result in H
2 opencases H ; inversion H ; subst ; simpl ; eauto
–rewrite doomed_result_other_ _ _ _ _ Ea in H
cases H ; inversion H ; subst ; simpl ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
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.
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.
Explore proof 2 tactics
Initial goal
intros ge fr m d k o args Es
destruct o ; try discriminate Es ; destruct k ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An instruction that continues changes memory as kept allows, where the genv's free does (free_keeps).
Explore proof 4 tactics
Initial goal
intros ge fr m i e l m′ Hfree H
destruct i
8 openfocused goal
focused goal
focused goal
focused goal
focused goal
focused goal
1: destruct special_leto eqn: Es ; destruct o ; try discriminate Es | rewrite inst_step_let_ _ _ _ _ _ _ Es in H
11 openfocused goal
focused goal
focused goal
focused goal
focused goal
focused goal
focused goal
focused goal
focused goal
all: unfold inst_step , external_call , bind_res , store_out in H ; cases H ; inversion H ; subst;first
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An instruction that allocates asks for a positive alignment, and writes nothing yet into the memory with the new object.
Explore proof 5 tactics
Initial goal
intros ge fr m i q k H
destruct i
8 openfocused goal
focused goal
focused goal
focused goal
focused goal
focused goal
1: destruct special_leto eqn: Es ; destruct o ; try discriminate Es | rewrite inst_step_let_ _ _ _ _ _ _ Es in H
11 openfocused goal
focused goal
focused goal
focused goal
focused goal
focused goal
focused goal
focused goal
focused goal
all: unfold inst_step , external_call , bind_res , store_out in H ; cases H ; inversion H ; subst
2 openfocused goal
all: first
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
or_stuck gives a next configuration only if it was given one.
Explore proof 2 tactics
Source script
or_stuck gives an allocation only if it was given one.
Explore proof 2 tactics
Initial goal
intros why r q k H
destruct r ; simpl in H ; congruence
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A tactic: where the hypothesis H says an or_stuck gave a step, split on the result it was given.
A return changes memory as kept allows: it only ends the invocation's locals.
Explore proof 5 tactics
Initial goal
unfold return_step
intros c o c′ H
apply or_stuck_next in H
cases H ; inversion H ; subst ; simpl
match goal withE : invalidate_locals_ _ = Some_ |- _⇒exact invalidate_locals_kept_ _ _ Eend
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A jump changes memory as kept allows: only a return changes it at all.
Explore proof 4 tactics
Initial goal
unfold jump_step , edge_step
intros ge c l j c′ H
cases H ; unstuck H
9 openfocused goal
focused goal
focused goal
focused goal
focused goal
focused goal
focused goal
all: first
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
A return never allocates.
Explore proof 4 tactics
Initial goal
unfold return_step
intros c o q k H
apply or_stuck_fresh in H
cases H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A jump never allocates.
Explore proof 4 tactics
Initial goal
unfold jump_step , edge_step
intros ge c l j q k H
cases H ; unstuck H ; first exact return_step_not_fresh_ _ _ _ H | discriminate H | idtac
2 openall: injection H as H ; exact return_step_not_fresh_ _ _ _ H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
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.
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.
Explore proof 4 tactics
Initial goal
unfold step , inst_next
intros ge c c′ Hfree H
cases H ; unstuck H
5 openfocused goal
focused goal
focused goal
focused goal
all: first
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
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.
Explore proof 16 tactics
Initial goal
unfold step , inst_next
intros ge c q k H
cases H ; unstuck H ; try exfalso ; exact jump_step_not_fresh_ _ _ _ _ _ H
2 openall: injection H as Hq Hk ; subst q k
2 open–split ; simpl ; lia |
2 openintros base
2 openmatch goal withHp : fr_at_ = Snapshot _ |- _⇒exact snapshot_alloc_keptxs c_memc baseend
–match goal withE : doomed_result_ _ _ _ _ = Some , Hc : fst = IFresh_ _ |- _⇒destruct doomed_result_out_ _ _ _ _ _ E as Ho | e′ & l′ & Ho | o′ & Ho ; rewrite Ho in Hc ; try discriminate Hcend
subst
match goal withE2 : inst_step_ _ _ _ = SomeIFresh_ _ |- _⇒destruct inst_step_fresh_ _ _ _ _ _ E2 as Ha Hkend
split ; auto
intros base
specialize Hkbase
simpl
match goal withHk : kept_ snd |- _⇒destruct t as e1 l1 m1end
exact Hk
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The machine of a runtime
A machine state: the configuration and the runtime's state.
The configuration c with its memory replaced by m.
The edge the jump j of the frame fr takes, read as jump_step reads it; None for a return or unreachable.
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.
A machine step:
mstep_next: astepthat allocates nothing;mstep_alloc: an allocation at R'salloc, 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.safepointmay change memory and R's state.
The machine state st' follows st after any number of machine steps.
The runtime is ready to allocate in the memory: R.ready of the runtime's state and the configuration's memory.
R's free changes memory as kept allows, by R's free_lifetime and retention.
Explore proof 7 tactics
Initial goal
intros x m r m′ H
split
2 open–apply lifetime_region_step
2 openeapply R.free_lifetime ; eauto
–intros a _
destruct R.retention_ _ _ _ H as → →
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Every machine step keeps the runtime ready, where the genv's free is R's:
- a step that allocates nothing changes memory only as
keptallows (step_next_kept), so R'sready_keptapplies; - 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.
Explore proof 14 tactics
Initial goal
unfold ready_state
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
3 openfocused goal
–simpl in *
3 opendeferred goal
eapply R.ready_kept ; exact Hr |
3 opendeferred goal
eapply step_next_kept ; | exact E
3 opendeferred goal
rewrite Hge
3 opendeferred goal
exact free_kept
2 opendeferred goal
–simpl in *
2 opendestruct step_fresh_kept_ _ _ _ E as Ha Hk
2 opendestruct R.fresh_allocation_ _ _ _ _ Hr Ha He Hal as _ Hr′
2 openeapply R.ready_kept ; exact Hr′ | apply Hk
–simpl in *
eapply R.safepoint_ready ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
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.
Explore proof 3 tactics
Initial goal
intros ge st st′ Hge H
induction H as st st′ Hs | st | st1 st2 st3 _ IH1 _ IH2 ; auto
eapply mstep_ready ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
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.
Explore proof 3 tactics
Initial goal
intros ge st st′ Hge H Hr
apply R.address_spacesndst′
exact mreachable_ready_ _ _ Hge H Hr
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 13 tactics
Initial goal
unfold ready_state
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
3 openfocused goal
–left
3 opendeferred goal
apply step_next
3 opendeferred goal
exact E
2 opendeferred goal
–left
2 opendestruct step_fresh_kept_ _ _ _ E as Ha _
2 opendestruct R.fresh_allocation_ _ _ _ _ Hr Ha He Hal as Hf _
2 openeapply step_fresh ; eauto
–right
eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.