rocq/spikes/Sep.v
A small separation logic over the model's memory, hand-rolled: the first of the two spikes of docs/logic.md. Nothing outside nanofil/rocq/spikes depends on it.
An assertion is a predicate on a footprint and a memory: the footprint is the set of pieces of memory the assertion owns, and the assertion may speak of the memory only through those pieces and through facts that no step can take back. Pieces are keyed by identity, not by address: an object's life (PLive), one of its bytes (PByte) and one of its aux slots (PAux), each named by the object's base and an offset. Keying by address would not do: the model's fresh lets a new object take the addresses of a freed one, so a byte at an address may belong to two identities in turn. A byte piece speaks only while its object is live and the offset is in bounds, and then nothing else can write it.
The separating conjunction star splits the footprint in two disjoint parts. The frame property is stable: an assertion still holds after any change that keeps its pieces (same_on) and only moves objects forward in life (grows). Each kind of step that changes memory keeps every footprint that does not own what it writes (store_same_on, pointer_store_same_on, alloc_same_on), given one fact about the whole memory, that live objects do not overlap (live_disjoint): that fact is this logic's state interpretation.
A safepoint is the one step that may change memory nobody in the program wrote. It frees no object (Runtime.v's collector_live, so the premise Buffer.v once took is Pieces.v's lemma keeps_live) and changes nothing an assertion owns except an aux slot whose stored capability names a freed object, and the list predicate lst never stores one (lst_safepoint). An assertion that survives that is sp_stable.
An assertion that owns only pieces of objects (owns_registered) can be dropped into htrue, the affine assertion of anything owned: a walk of the list drops each node it has passed. A write is a rule for the owner of what it writes (writes: icell_writes, pcell_writes) and a fact for everyone else (keeps), and the two combine under star (writes_star_l, writes_star_r); an allocation adds a node no one else owned (alloc_frame). Footprints are predicates compared piece by piece, with no extensionality assumed, so emp is a unit only up to the same pieces (star_emp_elim).
Footprints
A footprint: a set of pieces.
An assertion: a predicate on the footprint it owns and the memory.
The footprint S is exactly the pieces ps.
How memory may change
From m to m', every object moved forward in life only: it is still there unchanged, or it was live and is now freed and empty. New objects may appear. Every step of a run does this.
From m to m', the pieces of S are kept: an owned object's region, and, while the object is live and the offset in bounds, an owned byte or aux slot; a name is no memory.
The assertion P is stable: it survives any change that keeps its pieces and moves objects only forward. Every assertion built here is.
Every piece of S belongs to an object of m. Every assertion built here owns only such pieces, so a fresh identity is owned by no one.
Assertions
Owns nothing.
Owns nothing, and phi holds.
P and Q hold of disjoint parts of the footprint.
P x holds for some x.
The persistent fact that b is an object of kind k whose bounds, while it is live, are n bytes: the meta of docs/logic.md. Owns nothing, and no step takes it back.
The object b is live, and only the owner of this may end it: the live token.
The eight bytes at offset o of the object b.
The eight bytes at offset o of b hold the integer v, while b is live; b is an object, and o is in its bounds.
The pointer slot at offset o of b holds the pointer x, its address in the bytes and its capability in the aux (aux_holds), while b is live.
A list node at b: a 16-byte heap object, live, whose first slot points to next and whose second holds v (C's struct node {struct node *next; long v;}).
The list at p holds the values xs: null for none, else a pointer to a node with its own capability, at an 8-aligned address (a pointer load checks the alignment of its slot), whose next pointer is the rest.
One node of a nonempty list at p: its value v, its next pointer next and the rest xs, the body of lst's second case.
More ways memory may change
The assertion P survives what a safepoint may do (safepoint_shape): the same objects, the same bytes, and aux slots changed only as aux_moves allows.
The assertion P owns only pieces of objects of the memory.
Anything owned: the affine assertion into which pieces no longer needed are dropped.
The pieces a pointer slot at offset o of b owns.
The pieces a node at b owns.
From m to m', every footprint owning nothing of W is kept: what a write of the pieces W does to everyone else.
From m to m', P becomes P' on the same footprint, which owns the written pieces W: the rule of one write for the owner of what it writes.
Facts about objects and bytes
The region object_region finds for b has b for its base.
Explore proof 3 tactics
Initial goal
intros b rs reg
induction rs as | r rs IH ; cbn ; discriminate |
destruct Z.eqb_specr_baser b as E | _ ; intros H ; injection H as ← ; exact E | exact IH
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An object live after a change that moves objects only forward was live, with the same region, before it.
Explore proof 5 tactics
Initial goal
intros m m′ b reg Hg Hb E L
destruct object_regionb m_regionsm as reg0 | eqn: E0 ; | congruence
destruct Hgb reg0 E0 as E1 | L0 & E1 ; rewrite E1 in E ; injection E as ←
2 openfocused goal
–split ; assumption
deferred goal
–discriminate L
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A footprint of objects stays one when objects move only forward.
Explore proof 4 tactics
Initial goal
intros m m′ S Hg Hr p Hp
specialize Hrp Hp
destruct object_regionpiece_idp m_regionsm as reg | eqn: E ; | congruence
destruct Hg_ _ E as E′ | _ & E′ ; rewrite E' ; discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A footprint of objects stays one while objects keep their regions.
Explore proof 3 tactics
Initial goal
intros m m′ S Hr H p Hp
rewrite Hr
exact Hp Hp
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A freed object stays freed when objects move only forward.
Explore proof 4 tactics
Initial goal
intros m m′ c Hg b & reg & Hc & E & L
exists b, reg
split ; exact Hc |
destruct Hgb reg E as E′ | L′ & _ ; split ; assumption | congruence
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A capability that traps as a freed one keeps doing so when objects move only forward: an object that ends has no bounds left.
Explore proof 3 tactics
Initial goal
intros m m′ c Hg H a size r align Hs
specialize Ha size r align Hs
destruct c as | b | b | f | n ; cbn in H |- * ; try exact H ; destruct object_regionb m_regionsm as reg | eqn: E ; try discriminate H ; destruct Hgb reg E as E′ | _ & E′ ; rewrite E' ; try exact H ; cbn [ r_end ] ; destruct Z.leb_specb a ; rewrite proj2Z.leb_gta + size b by lia | ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The eight bytes at a read the same where each of them is the same.
Explore proof 5 tactics
Initial goal
intros m m′ a H
unfold load_bytes
simpl
rewrite ! H by lia
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Bytes read the same in a memory with the same bytes.
Explore proof 4 tactics
Initial goal
intros m m′ a n H
unfold load_bytes
rewrite H
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Eight zero bytes read as zero.
Explore proof 5 tactics
Initial goal
intros m a H
unfold load_bytes
simpl
rewrite ! H by lia
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Live objects stay apart while objects keep their regions.
Explore proof 4 tactics
Initial goal
intros m m′ E H b1 r1 b2 r2
unfold live_at
rewrite E
apply H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A memory with the same objects only moves them forward.
Explore proof 4 tactics
Initial goal
intros m m′ E b reg H
left
rewrite E
exact H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A footprint's parts are kept where it is.
Explore proof 2 tactics
Initial goal
intros S S′ m m′ H Hs p Hp
exact Hsp Hp Hp
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Kept through two changes is kept through both, when the second keeps every object's region.
Explore proof 19 tactics
Initial goal
intros S m1 m2 m3 Hr H12 H23 p Hp
specialize H12p Hp
specialize H23p Hp
destruct p ; cbn iota beta in H12 , H23 |- *
4 openfocused goal
focused goal
–intros reg E
4 opendeferred goal
deferred goal
apply H23 , H12 , E
3 opendeferred goal
deferred goal
–intros reg Hl Ho He
3 opendeferred goal
rewrite H23reg Hl Ho He
3 opendeferred goal
apply H12reg ; | assumption | assumption
3 opendeferred goal
unfold live_at in *
3 opendeferred goal
rewrite <- Hr
3 opendeferred goal
exact Hl
2 opendeferred goal
–intros reg Hl Ho He
2 openrewrite H23reg Hl Ho He
2 openapply H12reg ; | assumption | assumption
2 openunfold live_at in *
2 openrewrite <- Hr
2 openexact Hl
–exact I
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The algebra of star
star commutes.
Explore proof 5 tactics
Initial goal
intros P Q S m S1 & S2 & HS & Hd & H1 & H2
exists S2, S1
split ; intros p ; specialize HSp ; tauto |
split ; intros p ; specialize Hdp ; tauto |
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
star associates, to the left.
Explore proof 9 tactics
Initial goal
intros P Q R S m S1 & S23 & HS & Hd & H1 & S2 & S3 & HS23 & Hd23 & H2 & H3
exists λp ⇒ S1p ∨ S2p, S3
split ; intros p ; specialize HSp ; specialize HS23p ; tauto |
split ; intros p ; specialize Hdp ; specialize Hd23p ; specialize HS23p ; tauto |
split ; | exact H3
exists S1, S2
split ; intros p ; tauto |
split ; intros p ; specialize Hdp ; specialize HS23p ; tauto |
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
star associates, to the right.
Explore proof 9 tactics
Initial goal
intros P Q R S m S12 & S3 & HS & Hd & S1 & S2 & HS12 & Hd12 & H1 & H2 & H3
exists S1, λp ⇒ S2p ∨ S3p
split ; intros p ; specialize HSp ; specialize HS12p ; tauto |
split ; intros p ; specialize Hdp ; specialize Hd12p ; specialize HS12p ; tauto |
split ; exact H1 |
exists S2, S3
split ; intros p ; tauto |
split ; intros p ; specialize Hdp ; specialize HS12p ; tauto |
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The frame rule's monotonicity, on the left.
Explore proof 3 tactics
Initial goal
intros P P′ Q S m H S1 & S2 & HS & Hd & H1 & H2
exists S1, S2
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The frame rule's monotonicity, on the right.
Explore proof 3 tactics
Initial goal
intros P Q Q′ S m H S1 & S2 & HS & Hd & H1 & H2
exists S1, S2
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The first two parts of a star trade places.
Explore proof 6 tactics
Initial goal
intros P Q R S m H
apply star_assoc_r
apply star_assoc_l in H
revert H
apply star_mono_l
apply star_comm
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
emp is a unit, on the right.
Explore proof 5 tactics
Initial goal
intros P S m H
exists S, λ_ ⇒ False
split ; intros p ; tauto |
split ; intros p ; tauto |
split ; exact H | intros p ; tauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
emp is a unit, on the left.
Explore proof 2 tactics
And back: without emp, P holds of a footprint with the same pieces. Footprints are predicates, so this is as close as the logic gets to equality of footprints without extensionality.
Explore proof 7 tactics
Initial goal
intros P S m S1 & S2 & HS & _ & H1 & H2
exists S2
split ; | exact H2
intros p
specialize HSp
specialize H1p
tauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A pure fact on no footprint may be added.
Explore proof 8 tactics
Initial goal
intros phi Q S m Hp H
apply star_comm
destruct star_emp_rQ S m H as S1 & S2 & HS & Hd & H1 & H2
exists S1, S2
split ; exact HS |
split ; exact Hd |
split ; exact H1 |
split ; exact H2 | exact Hp
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The left part of a star holds of part of the footprint.
Explore proof 3 tactics
Initial goal
intros P Q S m S1 & S2 & _ & _ & H1 & _
exists S1
exact H1
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The right part of a star holds of part of the footprint.
Explore proof 3 tactics
Initial goal
intros P Q S m S1 & S2 & _ & _ & _ & H2
exists S2
exact H2
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An existential on the left of a star comes out.
Explore proof 10 tactics
Initial goal
intros A P Q S m
split
2 open–intros S1 & S2 & HS & Hd & x & H1 & H2
2 openexists x, S1, S2
2 openauto
–intros x & S1 & S2 & HS & Hd & H1 & H2
exists S1, S2
split ; exact HS |
split ; exact Hd |
split ; exists x ; exact H1 | exact H2
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
htrue holds of no footprint, so it may be added.
Explore proof 9 tactics
Initial goal
intros Q S m H
apply star_comm
destruct star_emp_rQ S m H as S1 & S2 & HS & Hd & H1 & H2
exists S1, S2
split ; exact HS |
split ; exact Hd |
split ; exact H1 |
intros p Hp
destruct proj1H2p Hp
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
What owns only pieces of objects can be dropped into htrue.
Explore proof 3 tactics
Initial goal
intros P Q S m HP
apply star_mono_l
exact HP
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
htrue absorbs what owns only pieces of objects.
Explore proof 6 tactics
Initial goal
intros P R S m HP H
apply star_assoc_l in H
revert H
apply star_mono_l
intros S0 m0 S1 & S2 & HS & _ & H1 & H2 p Hp
apply HS in Hp as Hp | Hp ; exact HP_ _ H1 p Hp | exact H2p Hp
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
htrue absorbs a part that owns only pieces of objects from in front of another.
Explore proof 6 tactics
Initial goal
intros P Q R S m HP H
apply star_swap in H
revert H
apply star_mono_r
intros S0 m0
apply htrue_absorb , HP
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Stability of each assertion
A star is stable if its parts are.
Explore proof 9 tactics
Initial goal
intros P Q HP HQ S m m′ S1 & S2 & HS & Hd & H1 & H2 Hs Hg
exists S1, S2
split ; exact HS |
split ; exact Hd |
split
2 open–apply HPS1 m m′ H1 ; | exact Hg
2 openapply same_on_subS ; intros p Hp ; apply HS ; left ; exact Hp | exact Hs
–apply HQS2 m m′ H2 ; | exact Hg
apply same_on_subS ; intros p Hp ; apply HS ; right ; exact Hp | exact Hs
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A star survives a safepoint if its parts do.
Explore proof 5 tactics
Initial goal
intros P Q HP HQ S m m′ S1 & S2 & HS & Hd & H1 & H2 Hr Hb Ha
exists S1, S2
split ; exact HS |
split ; exact Hd |
split ; exact HP_ _ _ H1 Hr Hb Ha | exact HQ_ _ _ H2 Hr Hb Ha
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A star owns pieces of objects if its parts do.
Explore proof 2 tactics
Initial goal
intros P Q HP HQ S m S1 & S2 & HS & Hd & H1 & H2 p Hp
apply HS in Hp as Hp | Hp ; exact HP_ _ H1 p Hp | exact HQ_ _ H2 p Hp
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
hex is stable if each instance is.
Explore proof 3 tactics
Initial goal
intros A P HP S m m′ x & H Hs Hg
exists x
exact HPx _ _ _ H Hs Hg
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
hex survives a safepoint if each instance does.
Explore proof 3 tactics
Initial goal
intros A P HP S m m′ x & H Hr Hb Ha
exists x
exact HPx _ _ _ H Hr Hb Ha
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
hex owns pieces of objects if each instance does.
Explore proof 2 tactics
Initial goal
intros A P HP S m x & H
exact HPx _ _ H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
emp is stable.
Explore proof 2 tactics
emp survives a safepoint.
Explore proof 2 tactics
emp owns nothing.
Explore proof 2 tactics
Initial goal
intros S m H p Hp
destruct proj1Hp Hp
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
pure is stable.
Explore proof 2 tactics
pure survives a safepoint.
Explore proof 2 tactics
pure owns nothing.
Explore proof 2 tactics
Initial goal
intros phi S m H _ p Hp
destruct proj1Hp Hp
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
htrue is stable.
Explore proof 2 tactics
Source script
htrue survives a safepoint.
Explore proof 2 tactics
Initial goal
intros S m m′ H Hr _ _
exact registered_same_ _ _ Hr H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
htrue owns pieces of objects.
Explore proof 2 tactics
Initial goal
intros S m H
exact H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
meta is stable: an object that ends keeps its kind, and has no bounds to speak of.
Explore proof 8 tactics
Initial goal
intros b n k S m m′ HS & reg & E & Hk & Hl _ Hg
split ; exact HS |
destruct Hgb reg E as E′ | L & E′
2 openfocused goal
–exists reg
2 opendeferred goal
auto
deferred goal
–eexists
2 openshelved goal
split ; exact E′ |
split ; exact Hk | discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
meta survives a safepoint.
Explore proof 5 tactics
Initial goal
intros b n k S m m′ HS & reg & E & Hk & Hl Hr _ _
split ; exact HS |
exists reg
rewrite Hr
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
meta owns nothing.
Explore proof 2 tactics
Source script
live is stable: its owner keeps the object's region.
Explore proof 5 tactics
Initial goal
intros b S m m′ HS & reg & E & L Hs _
split ; exact HS |
exists reg
split ; | exact L
exact HsPLiveb proj2HS_ eq_refl reg E
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
live survives a safepoint.
Explore proof 6 tactics
Initial goal
intros b S m m′ HS & reg & E & L Hr _ _
split ; exact HS |
exists reg
unfold live_at
rewrite Hr
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
live owns a piece of its object.
Explore proof 5 tactics
Initial goal
intros b S m HS & reg & E & L p Hp
apply HS in Hp
subst p
cbn
congruence
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
icell is stable: while the object is live it is the same object, and its owned bytes are kept.
Explore proof 17 tactics
Initial goal
intros b o v S m m′ HS & Hb & H Hs Hg
split ; exact HS |
split
2 openfocused goal
–destruct object_regionb m_regionsm as reg | eqn: E0 ; | congruence
2 opendeferred goal
destruct Hg_ _ E0 as E1 | _ & E1 ; congruence
deferred goal
–intros reg Hl
destruct Hreg grows_live_at_ _ _ _ Hg Hb Hl as Ho & He & Hv
split ; exact Ho |
split ; exact He |
rewrite <- Hv
apply load_bytes_ext8
intros i Hi
assert Hp : SPByteb o + i by apply HS ; exists i ; split ; exact Hi | reflexivity
pose proof Hs_ Hp as Hs′
cbn iota beta in Hs′
rewrite <- Z.add_assoc
apply Hs′reg ; exact Hl | lia | lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
icell survives a safepoint.
Explore proof 11 tactics
Initial goal
intros b o v S m m′ HS & Hb & H Hr Hbytes _
split ; exact HS |
split ; rewrite Hr ; exact Hb |
intros reg Hl
unfold live_at in Hl
rewrite Hr in Hl
destruct Hreg Hl as Ho & He & Hv
split ; exact Ho |
split ; exact He |
rewrite load_bytes_samem m′ _ _ Hbytes
exact Hv
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
icell owns pieces of its object.
Explore proof 3 tactics
Initial goal
intros b o v S m HS & Hb & _ p Hp
apply HS in Hp as i & _ & →
exact Hb
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 26 tactics
Initial goal
intros b o x S m m′ HS & Hb & H Hs Hg
split ; exact HS |
split
2 openfocused goal
–destruct object_regionb m_regionsm as reg | eqn: E0 ; | congruence
2 opendeferred goal
destruct Hg_ _ E0 as E1 | _ & E1 ; congruence
deferred goal
–intros reg Hl
destruct Hreg grows_live_at_ _ _ _ Hg Hb Hl as Ho & He & Hv & Ha
split ; exact Ho |
split ; exact He |
split
2 openfocused goal
+rewrite <- Hv
2 opendeferred goal
apply load_bytes_ext8
2 opendeferred goal
intros i Hi
2 opendeferred goal
assert Hp : SPByteb o + i by apply HS ; left ; exists i ; split ; exact Hi | reflexivity
2 opendeferred goal
pose proof Hs_ Hp as Hs′
2 opendeferred goal
cbn iota beta in Hs′
2 opendeferred goal
rewrite <- Z.add_assoc
2 opendeferred goal
apply Hs′reg ; exact Hl | lia | lia
deferred goal
+assert Hp : SPAuxb o by apply HS ; right ; reflexivity
pose proof Hs_ Hp as Hs′
cbn iota beta in Hs′
unfold aux_holds
rewrite Hs′reg Hl Ho ltac:lia
destruct Ha as E | Hf & Ht ; left ; exact E |
right
split ; exact freed_in_grows_ _ _ Hg Hf | exact traps_as_freed_grows_ _ _ Hg Ht
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
pcell survives a safepoint (aux_holds_moves).
Explore proof 11 tactics
Initial goal
intros b o x S m m′ HS & Hb & H Hr Hbytes Ha
split ; exact HS |
split ; rewrite Hr ; exact Hb |
intros reg Hl
unfold live_at in Hl
rewrite Hr in Hl
destruct Hreg Hl as Ho & He & Hv & Hx
split ; exact Ho |
split ; exact He |
split ; rewrite load_bytes_samem m′ _ _ Hbytes ; exact Hv |
exact aux_holds_moves_ _ _ _ Hr Ha Hx
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
pcell owns pieces of its object.
Explore proof 2 tactics
Initial goal
intros b o x S m HS & Hb & _ p Hp
apply HS in Hp as i & _ & → | → ; exact Hb
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
node is stable.
Explore proof 3 tactics
Initial goal
intros
unfold node
repeat apply star_stable ; auto using meta_stable , live_stable , pcell_stable , icell_stable
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
node survives a safepoint.
Explore proof 3 tactics
Initial goal
intros
unfold node
repeat apply star_sp_stable ; auto using meta_sp_stable , live_sp_stable , pcell_sp_stable , icell_sp_stable
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
node owns pieces of its object.
Explore proof 3 tactics
Initial goal
intros
unfold node
repeat apply star_registered ; auto using meta_registered , live_registered , pcell_registered , icell_registered
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
lst is stable.
Explore proof 5 tactics
Initial goal
induction xs as | v xs IH ; intros p ; cbn [ lst ] ; apply pure_stable |
apply hex_stable
intros next
apply star_stable ; apply pure_stable |
apply star_stable ; apply node_stable | apply IH
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
lst survives a safepoint: the list never stores the capability of a freed object, and what it stores is known up to the collector's rewriting anyway.
Explore proof 5 tactics
Initial goal
induction xs as | v xs IH ; intros p ; cbn [ lst ] ; apply pure_sp_stable |
apply hex_sp_stable
intros next
apply star_sp_stable ; apply pure_sp_stable |
apply star_sp_stable ; apply node_sp_stable | apply IH
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
lst owns pieces of objects.
Explore proof 5 tactics
Initial goal
induction xs as | v xs IH ; intros p ; cbn [ lst ] ; apply pure_registered |
apply hex_registered
intros next
apply star_registered ; apply pure_registered |
apply star_registered ; apply node_registered | apply IH
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The steps that change memory
An 8-byte store at offset o of the live object b, in bounds, keeps every footprint that owns none of those bytes: other live objects do not overlap b.
Explore proof 19 tactics
Initial goal
intros m b o reg x Hd Hl Ho He S HS p Hp
specialize HSp Hp
destruct p as b′ | b′ o′ | b′ o′ | k ; cbn iota beta ; | | | exact I
3 openfocused goal
focused goal
–intros reg′ E
3 opendeferred goal
deferred goal
exact E
2 opendeferred goal
deferred goal
–intros reg′ Hl′ Ho′ He′
2 opendeferred goal
apply store_bytes_other
2 opendeferred goal
intros Ha
2 opendeferred goal
change live_atm b′ reg′ in Hl′
2 opendeferred goal
destruct Z.eq_decb′ b as [ ->| Hne ]
3 openfocused goal
deferred goal
+assert reg′ = reg as → by destruct Hl , Hl′ ; congruence
3 opendeferred goal
deferred goal
apply HS
3 opendeferred goal
deferred goal
exists o′ − o
3 opendeferred goal
deferred goal
split ; lia |
3 opendeferred goal
deferred goal
f_equal
3 opendeferred goal
deferred goal
lia
2 opendeferred goal
deferred goal
+destruct Hdb′ reg′ b reg Hl′ Hl Hne ; lia
deferred goal
–intros
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An aux store at offset o of the live object b, in bounds, keeps every footprint that does not own that slot.
Explore proof 16 tactics
Initial goal
intros m b o reg c Hd Hl Ho He S HS p Hp
specialize HSp Hp
destruct p as b′ | b′ o′ | b′ o′ | k ; cbn iota beta ; | | | exact I
3 openfocused goal
focused goal
–intros reg′ E
3 opendeferred goal
deferred goal
exact E
2 opendeferred goal
deferred goal
–intros
2 opendeferred goal
reflexivity
deferred goal
–intros reg′ Hl′ Ho′ He′
change live_atm b′ reg′ in Hl′
cbn [ m_aux store_aux ]
destruct Z.eqb_specb′ + o′ b + o as Ha | _ ; exfalso | reflexivity
destruct Z.eq_decb′ b as [ ->| Hne ]
2 open+apply HS
2 openf_equal
2 openlia
+destruct Hdb′ reg′ b reg Hl′ Hl Hne ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The pointer store's protocol in listsum.c (ensure, barrier, reload, then the capability and the address) is an aux store and then an 8-byte store.
Explore proof 1 tactics
Initial goal
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
That pointer store at offset o of the live object b, in bounds, keeps every footprint that owns none of the slot's pieces.
Explore proof 14 tactics
Initial goal
intros m b o reg c v Hd Hl Ho He S HS
apply same_on_trans with store_auxm b + o c ; reflexivity | |
2 openfocused goal
–apply aux_store_same_onm b o reg c Hd Hl Ho He
2 opendeferred goal
intros p Hp E
2 opendeferred goal
apply HSp Hp
2 opendeferred goal
right
2 opendeferred goal
symmetry
2 opendeferred goal
exact E
deferred goal
–apply store_same_onstore_auxm b + o c b o reg v ; | exact Hl | exact Ho | exact He |
2 open+exact live_disjoint_samem _ eq_refl Hd
+intros p Hp E
apply HSp Hp
left
exact E
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Allocating at a fresh base keeps every footprint: no one owns the new identity, and no byte changes.
Explore proof 9 tactics
Initial goal
intros S m q base _ & _ & _ & Hn & _ p _
destruct p as b | b o | b o | k ; cbn iota beta ; | | | exact I
3 openfocused goal
–intros reg E
3 opendeferred goal
rewrite object_region_allocated
3 opendeferred goal
destruct Z.eqb_specbase b as [ <-| _ ] ; congruence | exact E
2 opendeferred goal
–intros
2 openreflexivity
–intros
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Allocating at a fresh base moves no object.
Explore proof 4 tactics
Initial goal
intros m q base _ & _ & _ & Hn & _ b reg E
left
rewrite object_region_allocated
destruct Z.eqb_specbase b as [ <-| _ ] ; congruence | exact E
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A footprint of objects of m owns nothing of a fresh base.
Explore proof 4 tactics
Initial goal
intros S m q base p Hr _ & _ & _ & Hn & _ Hp E
apply Hrp Hp
rewrite E
exact Hn
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Updating the owned cell
A write rule carries over a frame on the right that does not own what is written.
Explore proof 16 tactics
Initial goal
intros W m m′ P P′ Q Hk Hg HQ HP S S1 & S2 & HS & Hd & H1 & H2
destruct HPS1 H1 as H1′ HW
split
2 open–exists S1, S2
2 opensplit ; exact HS |
2 opensplit ; exact Hd |
2 opensplit ; exact H1′ |
2 openapply HQS2 m m′ H2 ; | exact Hg
2 openapply Hk
2 openintros p Hp Hw
2 openapply Hdp
2 opensplit ; apply HW , Hw | exact Hp
–intros p Hw
apply HS
left
apply HW , Hw
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A write rule carries over a frame on the left.
Explore proof 16 tactics
Initial goal
intros W m m′ P P′ Q Hk Hg HQ HP S S1 & S2 & HS & Hd & H1 & H2
destruct HPS2 H2 as H2′ HW
split
2 open–exists S1, S2
2 opensplit ; exact HS |
2 opensplit ; exact Hd |
2 opensplit ; | exact H2′
2 openapply HQS1 m m′ H1 ; | exact Hg
2 openapply Hk
2 openintros p Hp Hw
2 openapply Hdp
2 opensplit ; exact Hp | apply HW , Hw
–intros p Hw
apply HS
right
apply HW , Hw
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
After an 8-byte store of an unsigned x at offset o of b, the owned cell there holds x.
Explore proof 9 tactics
Initial goal
intros m b o v x Hx S HS & Hb & H
split ; | intros p Hp ; apply HS , Hp
split ; exact HS |
split ; exact Hb |
intros reg Hl
destruct Hreg Hl as Ho & He & _
split ; exact Ho |
split ; exact He |
apply load_store_bytes , Hx
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
After the pointer store of x' at offset o of b, the owned slot there holds x'.
Explore proof 13 tactics
Initial goal
intros m b o x x′ Hx S HS & Hb & H
split ; | intros p Hp ; apply HS , Hp
split ; exact HS |
split ; exact Hb |
intros reg Hl
destruct Hreg Hl as Ho & He & _
split ; exact Ho |
split ; exact He |
split ; apply load_store_bytes , Hx |
left
cbn [ m_aux store_bytes store_aux ]
rewrite Z.eqb_refl
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A node's object is live, a heap object of 16 bytes.
Explore proof 8 tactics
Initial goal
intros b x v S m S1 & S2 & _ & _ & _ & reg & E & Hk & Hl & S3 & S4 & _ & _ & _ & reg′ & E′ & L′ & _
rewrite E in E′
injection E′ as ←
specialize HlL′
pose proof object_region_base_ _ _ E as Hb
rewrite E
destruct reg as rb re rk rl ; cbn in * ; subst
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A node's next slot reads as its next pointer.
Explore proof 6 tactics
Initial goal
intros b x v S m H
pose proof node_region_ _ _ _ _ H as Hr
destruct H as S1 & S2 & _ & _ & _ & S3 & S4 & _ & _ & _ & S5 & S6 & _ & _ & _ & _ & Hp & _
destruct Hp_ conjHr eq_refl as _ & _ & Hv & Ha
rewrite Z.add_0_r in Hv , Ha
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The pointer store of x' into the next slot of the node at b, which the assertion owns, makes x' its next pointer, and keeps the frame Q.
Explore proof 17 tactics
Initial goal
intros m b x x′ v Q S Hd HQ Hx H
destruct star_elim_l_ _ _ _ H as S0 & H0
pose proof node_region_ _ _ _ _ H0 as Hr
set m′ := store_bytesstore_auxm b ptr_capx′ b 8 ptr_addrx′
assert Hk : keepspcell_piecesb 0 m m′
2 open{pose proof pointer_store_same_onm b 0 _ ptr_capx′ ptr_addrx′ Hd conjHr eq_refl as K
2 openrewrite Z.add_0_r in K
2 openapply K ; cbn ; lia
assert Hg : growsm m′ by apply grows_same ; reflexivity
refine proj1writes_star_l_ _ _ _ _ Q Hk Hg HQ _ S H
unfold node
apply writes_star_r ; exact Hk | exact Hg | apply meta_stable |
apply writes_star_r ; exact Hk | exact Hg | apply live_stable |
apply writes_star_l ; exact Hk | exact Hg | apply icell_stable |
pose proof pcell_writesm b 0 x x′ Hx as W
rewrite Z.add_0_r in W
exact W
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The 8-byte store of an unsigned x into the value slot of the node at b, which the assertion owns, makes x its value, and keeps the frame Q.
Explore proof 11 tactics
Initial goal
intros m b next v x Q S Hd HQ Hx H
destruct star_elim_l_ _ _ _ H as S0 & H0
pose proof node_region_ _ _ _ _ H0 as Hr
assert Hk : keepsbytes8b 8 m store_bytesm b + 8 8 x by apply store_same_onm b 8 _ x Hd conjHr eq_refl ; cbn ; lia
assert Hg : growsm store_bytesm b + 8 8 x by apply grows_same ; reflexivity
refine proj1writes_star_l_ _ _ _ _ Q Hk Hg HQ _ S H
unfold node
apply writes_star_r ; exact Hk | exact Hg | apply meta_stable |
apply writes_star_r ; exact Hk | exact Hg | apply live_stable |
apply writes_star_r ; exact Hk | exact Hg | apply pcell_stable |
apply icell_writes , Hx
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
After allocating a 16-byte heap object at a fresh base b, the pieces node_pieces of b make a node with a null next pointer and the value 0: Fil-C's allocation reads as zero, with no stored capability.
Explore proof 49 tactics
Initial goal
intros m b Hf
pose proof Hf as _ & _ & _ & _ & _ & Hz
cbn [ req_extent heap_req ] in Hz
change 16 + 15 / 16 × 16 with 16 in Hz
set m′ := allocatedm heap_req16 16 b
assert Hr : object_regionb m_regionsm′ = SomemkRegionb b + 16 Heap Live by cbn ; rewrite Z.eqb_refl ; reflexivity
assert Hl : ∀reg, live_atm′ b reg → reg = mkRegionb b + 16 Heap Live by intros reg E _ ; rewrite Hr in E ; injection E as ← ; reflexivity
assert Hn : object_regionb m_regionsm′ ≠ None by rewrite Hr ; discriminate
exists λ_ ⇒ False, node_piecesb
split ; intros p ; tauto |
split ; intros p ; tauto |
split
2 openfocused goal
{split ; intros p ; tauto |
2 opendeferred goal
exists mkRegionb b + 16 Heap Live
2 opendeferred goal
split ; exact Hr |
2 opendeferred goal
split ; reflexivity
deferred goal
exists eqPLiveb, λp ⇒ pcell_piecesb 0 p ∨ bytes8b 8 p
split ; intros p ; unfold node_pieces , pcell_pieces ; split ; intros H ; destruct H as [ <-| [ H | [ H | H ] ] ] | destruct H as [ <-| [ [ H | H ] | H ] ] ; tauto |
split ; intros p ← i & _ & E | E | i & _ & E ; discriminate |
split ; split ; intros p ; tauto | exists mkRegionb b + 16 Heap Live ; split ; exact Hr | reflexivity |
exists pcell_piecesb 0, bytes8b 8
split ; intros p ; tauto |
split ; intros p i & Hi & → | → j & Hj & E′ ; assert 0 + i = 8 + j by congruence ; lia | discriminate |
split
2 openfocused goal
–split ; intros p ; apply iff_refl |
2 opendeferred goal
split ; exact Hn |
2 opendeferred goal
intros reg Hreg
2 opendeferred goal
apply Hl in Hreg as →
2 opendeferred goal
split ; lia |
2 opendeferred goal
split ; cbn ; lia |
2 opendeferred goal
rewrite Z.add_0_r
2 opendeferred goal
split
3 openfocused goal
deferred goal
+apply load_bytes_zero
3 opendeferred goal
deferred goal
intros i Hi
3 opendeferred goal
deferred goal
apply Hzb + i
3 opendeferred goal
deferred goal
lia
2 opendeferred goal
deferred goal
+left
2 opendeferred goal
exact proj2Hzb ltac:lia
deferred goal
–split ; intros p ; tauto |
split ; exact Hn |
intros reg Hreg
apply Hl in Hreg as →
split ; lia |
split ; cbn ; lia |
apply load_bytes_zero
intros i Hi
rewrite <- Z.add_assoc
apply Hzb + 8 + i
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Allocating a node at a fresh base adds it to any stable assertion P of pieces of objects: the new pieces are disjoint from P's, since no one owned the new identity.
Explore proof 9 tactics
Initial goal
intros m b P S Hf HP Hreg H
exists node_piecesb, S
split ; intros p ; tauto |
split
2 open–intros p Hn Hs
2 openapply registered_freshS m _ b p Hreg_ _ H Hf Hs
2 opendestruct Hn as [ ->| [ ( i & _ & -> ) | [ ->| ( i & _ & -> ) ] ] ] ; reflexivity
–split ; exact alloc_nodem b Hf |
exact HPS m _ H alloc_same_onS m _ b Hf alloc_growsm _ b Hf
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The list
The empty list at null owns nothing.
Explore proof 2 tactics
A nonempty list is a lst_cons for some next pointer.
Explore proof 2 tactics
Source script
A list's pointer is null, or a live object's capability.
Explore proof 11 tactics
Initial goal
intros | v xs p S m H ; cbn [ lst ] in H
2 open–destruct H as _ →
2 openleft
2 openreflexivity
–destruct H as next & S1 & S2 & _ & _ & _ & Hp & _ & H2
right
destruct star_elim_l_ _ _ _ H2 as S3 & H3
exists ptr_addrp, mkRegionptr_addrp ptr_addrp + 16 Heap Live
rewrite Hp at 1
split ; reflexivity |
split ; exact node_region_ _ _ _ _ H3 | reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A list's address is 0 or a node's, inside the address space when every object is (objects_fit).
Explore proof 9 tactics
Initial goal
intros | v xs p S m Hfit H ; cbn [ lst ] in H
2 open–destruct H as _ →
2 opencbn
2 openlia
–destruct H as next & S1 & S2 & _ & _ & _ & _ & Hpos & _ & H2
destruct star_elim_l_ _ _ _ H2 as S3 & H3
destruct Hfit_ _ node_region_ _ _ _ _ H3
cbn in *
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A list at a nonzero address is a node and the rest.
Explore proof 8 tactics
Initial goal
intros | v xs p R S m Hp H
2 open–destruct star_elim_l_ _ _ _ H as S1 & _ & →
2 opencbn in Hp
2 openlia
–cbn [ lst ] in H
apply star_hex_l in H as next & H
exists v, next, xs
exact H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
What a node of a list gives a step that reads it: its address a, aligned, inside the address space, a live 16-byte heap object whose next slot holds next, address in the bytes and capability, exactly, in the aux.
Explore proof 15 tactics
Initial goal
intros p v next xs R S m Hfit H
destruct star_elim_l_ _ _ _ H as S0 & S1 & S2 & _ & _ & _ & Hp & Hpos & Hal & H2
destruct star_elim_l_ _ _ _ H2 as S3 & H3
destruct star_elim_r_ _ _ _ H2 as S4 & H4
pose proof node_region_ _ _ _ _ H3 as Hr
destruct node_next_ _ _ _ _ H3 as Hv Ha
exists ptr_addrp
split ; exact Hp |
split ; exact Hpos |
split ; exact Hal |
split ; destruct Hfit_ _ Hr ; cbn in * ; lia |
split ; exact Hr |
split ; exact Hv |
apply aux_holds_live_ _ _ Ha
exact lst_cap_ _ _ _ H4
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A node and the rest of a list make a list one longer.
Explore proof 6 tactics
Initial goal
intros b h v xs S m Hb Hal H
cbn [ lst ]
exists h
apply star_pure_intro ; | exact H
cbn
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Walking past a node drops it, and its pure facts, into htrue.
Explore proof 11 tactics
Initial goal
intros p v next xs F S m H
unfold lst_cons in H
apply star_assoc_r in H
apply star_mono_r_ _ _ _ _ star_assoc_r_ _ _ in H
apply star_mono_r_ _ _ _ _ star_swap_ _ _ in H
apply star_swap in H
revert H
apply star_mono_r
intros S0 m0 H
apply star_mono_r_ _ _ _ _ λS1 m1 ⇒ htrue_absorb_ _ S1 m1 node_registered_ _ _ in H
exact htrue_absorb_ _ _ _ pure_registered_ H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.