rocq/theories/HelloVersion.v
GNU Hello's version and help helpers through the program logic. The output contracts are supplied by the caller's stdio world; stdout remains world-owned.
Keep symbolic address arithmetic folded while computing IR operands.
Keep symbolic offsets folded while computing IR operands.
Keep symbolic scaled indices folded while computing IR operands.
The compiled proper-name helper returns its argument unchanged.
Its empty entry block returns the pointer.
The entry block is present in the compiled function.
Explore proof 2 tactics
Initial goal
vm_compute
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Its call frame binds the sole pointer argument.
Explore proof 1 tactics
Initial goal
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The help footer prints the bug-reporting addresses.
Its single block loads stdout and makes four output calls.
The footer's entry block is present.
Explore proof 2 tactics
Initial goal
vm_compute
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A version-etc literal's pointer in the linked fixture.
The array-based version helper reached by Hello's single version call.
Its entry selects the format with a command name.
The command-name version heading.
The copyright and license lines precede author dispatch.
The first dispatch compares the count with two.
The second dispatch tests for two authors.
The third dispatch tests for three authors.
The last reachable dispatch tests for four authors.
The four-author output reads four cells of the array.
The shared return after author output.
Every block on the reachable four-author path occurs in the fixture.
Proof 2 steps Qed
The array helper's entry for main's three heading literals and four authors. The count is the result the variadic loop must prove.
Explore proof 1 tactics
Initial goal
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The six exact output calls on the four-author path; the copyright year is a promoted W argument, not a pointer or a 64-bit integer.
The promoted classes at these output sites: pointers and int words.
The four exact output argument lists in the help footer: the newline, bug address, home-page line, and general-help line.
Explore proof 7 tactics
Initial goal
intros Hp
apply rule_instge f e ls l Letd P VaArgs Constoff rest j cs m fuel IContinueputd WPtrmkPtrptr_addrp + off mod 2 ^ 64 ptr_capp e ls m
2 openfocused goal
–cbn [ inst_step fr_env fr_locals ]
2 opendeferred goal
rewrite Hp
2 opendeferred goal
reflexivity
deferred goal
–apply doomed_result_continue
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
For promotion: a successful variadic read updates the cursor's memory and binds its result. This is rule_let specialized to va_arg_res; the cursor is not frame-only state.
Explore proof 5 tactics
Initial goal
intros Hargs Hread
apply rule_let with classes := P xs := WPtrp ; reflexivity | reflexivity | exact Hargs |
cbn [ op_res ]
rewrite Hread
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
For promotion: taking the pointer argument at an aligned cursor reads its bytes and capability after advancing the cursor. The hypotheses expose both checked reads and the checked cursor write, including the case where the write overlaps the argument cell.
Explore proof 14 tactics
Initial goal
intros Hp Ha Hc Hal Hcell Hstore Haddr Hcap
assert Halign : a + 8 − 1 / 8 × 8 = a
2 openfocused goal
{pose proof Z.div_moda 8 ltac:lia as Hdiv
2 opendeferred goal
rewrite Hal in Hdiv
2 opendeferred goal
replace a + 8 − 1 with 7 + a / 8 × 8 by lia
2 opendeferred goal
rewrite Z.div_add ; | lia
2 opendeferred goal
replace 7 / 8 with 0 by reflexivity
2 opendeferred goal
lia
deferred goal
unfold va_arg_res
rewrite Hp Ha Hc
cbn [ va_cell class_width width_bytes ptr_addr ptr_cap ]
rewrite Halign Hcell Hstore Haddr Hcap
destruct x
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
For promotion: snapshot stores at an address depend only on the bytes and capability already at that address, not on other memory.
Explore proof 3 tactics
Initial goal
revert a m1 m2
induction xs as | x xs IH ; intros a m1 m2 Hb Ha ; exact conjHb Ha |
destruct x ; cbn [ snapshot_values ] ; apply IH ; cbn [ store_bytes store_aux m_bytes m_aux ] ; try rewrite Hb ; try rewrite Ha ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
For promotion: taking the snapshot changes no address outside its eight-byte argument cells, even for words the snapshot skips.
Explore proof 19 tactics
Initial goal
revert a m
induction xs as | x xs IH ; intros a m Hout ; split ; reflexivity |
cbn [ length ] in Hout
rewrite Nat2Z.inj_succ in Hout
assert Htail : t < a + 8 ∨ a + 8 + 8 × Z.of_natlengthxs ≤ t
2 openfocused goal
{lia
deferred goal
assert Hbyte : a ≤? t && t <? a + 8 = false
2 openfocused goal
{apply andb_false_iff
2 opendeferred goal
destruct Hout as Hout | Hout
3 openfocused goal
deferred goal
–left
3 opendeferred goal
deferred goal
apply Z.leb_gt
3 opendeferred goal
deferred goal
lia
2 opendeferred goal
deferred goal
–right
2 opendeferred goal
apply Z.ltb_ge
2 opendeferred goal
lia
deferred goal
assert Haux : t =? a = false
2 openfocused goal
{apply Z.eqb_neq
2 opendeferred goal
destruct Hout as Hout | Hout ; rewrite in Hout ; lia
deferred goal
destruct x ; cbn [ snapshot_values ];match goal with|- m_bytessnapshot_valuesxs t = _ ∧ _⇒destruct IHa′ m′ Htail as Hb Haend;rewrite Hb Ha;cbn [ store_bytes store_aux m_bytes m_aux ];rewrite ;split;reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A pointer argument's bytes survive all the later snapshot stores.
Explore proof 16 tactics
Initial goal
revert xs a m
induction i as | i IH ; intros | x xs a m Hnth Hj ; try discriminate
2 openfocused goal
–cbn [ lookup list_lookup ] in Hnth
2 opendeferred goal
injection Hnth as →
2 opendeferred goal
cbn [ snapshot_values ]
2 opendeferred goal
rewrite Z.mul_0_r Z.add_0_r
2 opendeferred goal
rewrite proj1snapshot_values_outsidexs a + 8 _ a + j ltac:left ; lia
2 opendeferred goal
cbn [ store_aux store_bytes m_bytes ]
2 opendeferred goal
rewrite proj2Z.leb_lea a + j ltac:lia
2 opendeferred goal
rewrite proj2Z.ltb_lta + j a + 8 ltac:lia
2 opendeferred goal
cbn [ andb ]
2 opendeferred goal
replace a + j − a with j by lia
2 opendeferred goal
reflexivity
deferred goal
–cbn [ lookup list_lookup ] in Hnth
replace a + 8 × Z.of_natSi + j with a + 8 + 8 × Z.of_nati + j by rewrite Nat2Z.inj_succ ; lia
destruct x ; cbn [ snapshot_values ] ; apply IH ; assumption
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A pointer argument's capability survives all later snapshot stores.
Explore proof 13 tactics
Initial goal
revert xs a m
induction i as | i IH ; intros | x xs a m Hnth ; try discriminate
2 open–cbn [ lookup list_lookup ] in Hnth
2 openinjection Hnth as →
2 opencbn [ snapshot_values ]
2 openrewrite Z.mul_0_r Z.add_0_r
2 openrewrite proj2snapshot_values_outsidexs a + 8 _ a ltac:left ; lia
2 opencbn [ store_aux m_aux ]
2 openrewrite Z.eqb_refl
2 openreflexivity
–cbn [ lookup list_lookup ] in Hnth
replace a + 8 × Z.of_natSi with a + 8 + 8 × Z.of_nati by rewrite Nat2Z.inj_succ ; lia
destruct x ; cbn [ snapshot_values ] ; apply IH ; assumption
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
For promotion: values for a snapshot's pieces can be computed from empty memory. Freshness guarantees the actual allocated cells start with the same zero bytes and empty capability slots.
For promotion: a snapshot owns the same keys as the new object, populated with the snapshot's bytes and capabilities.
For promotion: populating a snapshot leaves its ownership keys unchanged, so their distinctness follows from obj_ps_nodup.
Explore proof 5 tactics
Initial goal
unfold snapshot_ps
rewrite - list_fmap_compose
apply list_fmap_ext
intros i l v Hi
destruct l ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The snapshot pieces contain an argument's complete pointer cell.
Explore proof 46 tactics
Initial goal
intros Hnth Hextent l v Hin
unfold snapshot_ps
apply elem_of_cons in Hin as = → → | Hin
2 open–apply list_elem_of_fmap
2 openexists PAuxbase 8 × Z.of_nati, VAuxCNone
2 opensplit
3 openfocused goal
+unfold snapshot_piece
3 opendeferred goal
cbn [ fst snd ]
3 opendeferred goal
rewrite snapshot_pointer_aux_ _ _ _ _ Hnth
3 opendeferred goal
reflexivity
2 opendeferred goal
+unfold obj_ps
2 openapply elem_of_cons
2 openright
2 openapply elem_of_app
2 openright
2 openapply list_elem_of_fmap
2 openexists 8 × Z.of_nati
2 opensplit ; reflexivity |
2 openapply elem_of_seqZ
2 openrewrite Nat2Z.inj_succ in Hextent
2 openlia
–unfold cell in Hin
apply list_elem_of_fmap in Hin as j & = → → & Hj
assert Hjrange : 0 ≤ j < 8
2 open{apply list_elem_of_In in Hj
2 opencbn in Hj
2 openrepeat destruct Hj as ← | Hj ; try contradiction ; lia
apply list_elem_of_fmap
exists PBytebase 8 × Z.of_nati + j, VByte0
split
2 open+unfold snapshot_piece
2 opencbn [ fst snd ]
2 openreplace base + 8 × Z.of_nati + j with base + 8 × Z.of_nati + j by lia
2 openrewrite snapshot_pointer_byte_ _ _ _ _ _ Hnth Hjrange
2 openreflexivity
+unfold obj_ps
apply elem_of_cons
right
apply elem_of_app
left
apply list_elem_of_fmap
exists 8 × Z.of_nati + j
split ; reflexivity |
apply elem_of_seqZ
rewrite Nat2Z.inj_succ in Hextent
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
For promotion: each snapshot piece names its fresh object.
Explore proof 8 tactics
Initial goal
unfold snapshot_ps
intros Hin
apply list_elem_of_fmap in Hin as k u & Hkv & Hin
assert Hkey : l = k
2 open{apply f_equalfst in Hkv
2 opendestruct k ; exact Hkv
subst l
exact obj_ps_id_ _ _ _ Hin
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
For promotion: all snapshot keys are memory pieces, so an old agreeing heap cannot already own a key of the fresh object.
Explore proof 8 tactics
Initial goal
unfold snapshot_ps
intros Hin
apply list_elem_of_fmap in Hin as k u & Hkv & Hin
assert Hkey : l = k
2 open{apply f_equalfst in Hkv
2 opendestruct k ; exact Hkv
subst l
exact obj_ps_mem_ _ _ _ Hin
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
For promotion: freshness makes the computed snapshot pieces agree with the real allocation after its argument stores.
Explore proof 22 tactics
Initial goal
intros _ & _ & _ & _ & _ & Hz
assert Hsame : ∀i, 0 ≤ i < req_extentq → m_bytessnapshot_valuesxs base allocatedm q base base + i = m_bytessnapshot_valuesxs base allocatedempty_mem q base base + i ∧ m_auxsnapshot_valuesxs base allocatedm q base base + i = m_auxsnapshot_valuesxs base allocatedempty_mem q base base + i
2 openfocused goal
{intros i Hi
2 opendeferred goal
destruct Hzbase + i ltac:lia as Hb Ha
2 opendeferred goal
apply snapshot_values_pointwise ; exact Hb | exact Ha
deferred goal
apply all_agree_intro
intros l v Hin
unfold snapshot_ps in Hin
apply list_elem_of_fmap in Hin as k u & Hlv & Hin
change agree_piecesnapshot_valuesxs base allocatedm q base l, v.1 l, v.2
rewrite Hlv
unfold obj_ps in Hin
apply elem_of_cons in Hin as = → → | Hin
2 openfocused goal
–unfold snapshot_piece
2 opendeferred goal
cbn [ fst snd agree_piece ]
2 opendeferred goal
unfold live_at
2 opendeferred goal
rewrite snapshot_values_regions object_region_allocated Z.eqb_refl
2 opendeferred goal
split ; reflexivity
deferred goal
–apply elem_of_app in Hin as Hin | Hin ; apply list_elem_of_fmap in Hin as i & = → → & Hi ; apply elem_of_seqZ in Hi ; unfold snapshot_piece ; cbn [ fst snd agree_piece ] ; unfold registered , in_live ; rewrite snapshot_values_regions object_region_allocated Z.eqb_refl ; split ; discriminate | ; intros reg = ← _ ; cbn [ r_end ] ; split ; lia | ; split ; lia |
2 openfocused goal
+exact proj1Hsamei ltac:lia
deferred goal
+left
exact proj2Hsamei ltac:lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
For promotion: snapshot stores frame every piece outside the fresh object's keys. The proof uses frame_within and the exact store range, not a promise about the caller's memory.
Explore proof 37 tactics
Initial goal
intros Hd Hsize
apply frame_within_ _ _ base mkRegionbase base + req_extentq req_kindq Live ; apply snapshot_values_regions | exact Hd | | |
3 openfocused goal
focused goal
–split ; rewrite object_region_allocated Z.eqb_refl ; reflexivity | reflexivity
2 opendeferred goal
deferred goal
–intros t Hnot
2 opendeferred goal
destruct Z_le_gt_decbase t as Hlo | Hlo ; destruct Z_lt_ge_dect base + req_extentq as Hhi | Hhi ; try apply proj1snapshot_values_outsidexs base _ t ltac:lia
2 opendeferred goal
exfalso
2 opendeferred goal
apply Hnotltac:cbn ; lia
2 opendeferred goal
apply list_elem_of_fmap
2 opendeferred goal
exists PBytebase t − base, VByte0
2 opendeferred goal
split ; reflexivity |
2 opendeferred goal
unfold obj_ps
2 opendeferred goal
apply elem_of_cons
2 opendeferred goal
right
2 opendeferred goal
apply elem_of_app
2 opendeferred goal
left
2 opendeferred goal
apply list_elem_of_fmap
2 opendeferred goal
exists t − base
2 opendeferred goal
split ; reflexivity |
2 opendeferred goal
apply elem_of_seqZ
2 opendeferred goal
lia
deferred goal
–intros t Hnot
destruct Z_le_gt_decbase t as Hlo | Hlo ; destruct Z_lt_ge_dect base + req_extentq as Hhi | Hhi ; try apply proj2snapshot_values_outsidexs base _ t ltac:lia
exfalso
apply Hnotltac:cbn ; lia
apply list_elem_of_fmap
exists PAuxbase t − base, VAuxCNone
split ; reflexivity |
unfold obj_ps
apply elem_of_cons
right
apply elem_of_app
right
apply list_elem_of_fmap
exists t − base
split ; reflexivity |
apply elem_of_seqZ
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
For promotion: the nonempty snapshot equation of Semantics.step. The read-only pointer goes in the frame; the argument cells are allocated and populated in memory by that same step.
Explore proof 5 tactics
Initial goal
intros Hne Hwords q
destruct xs ; contradiction |
cbn [ Semantics.step c_frame c_mem c_callers c_fuel fr_at fr_fn fr_env fr_locals fr_doomed ]
rewrite Hwords
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
For promotion: the collector cannot rewrite a stored read-only capability while its object is live. This is the read-only case of aux_holds_live, derived directly from freed_in.
Explore proof 6 tactics
Initial goal
intros Heq | b′ & reg′ & Hcap & Hreg & Hfreed & _ Hlive Hlife ; exact Heq |
destruct Hcap as Hcap | Hcap ; discriminate |
injection Hcap as ←
rewrite Hlive in Hreg
injection Hreg as ←
congruence
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Writing concatenated piece lists is their two overwrites in order.
Explore proof 1 tactics
Source script
Rewriting already-owned values leaves the authoritative map unchanged.
Explore proof 13 tactics
Initial goal
induction ps as | l v ps IH ; intros Hown ; reflexivity |
cbn
rewrite IH
2 open–apply insert_id
2 openapply Hown
2 openapply elem_of_cons
2 openleft
2 openreflexivity
–intros k u Hin
apply Hown
apply elem_of_cons
right
exact Hin
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The mutable va_list cell: its life, pointer capability, and cursor bytes. Advancing the cursor keeps the capability unchanged.
The helpers over any runtime and caller-supplied world.
The Iris instance uses exactly the caller's registry and world.
Expressions in that language.
Full ownership cannot contain two pieces with the same key. This supplies the disjointness needed when a cursor read also owns its snapshot and literal frames.
Explore proof 14 tactics
Initial goal
induction ps as | l v ps IH ; iIntros _ ; iPureIntro ; constructor |
rewrite / pts big_sepL_cons
iIntros [Hl Hps]
iDestruct IH with Hps as %Hnd
destruct decidel ∈ ps.*1 as Hin | Hnot
2 openfocused goal
–apply list_elem_of_fmap in Hin as k u & Hkey & Hin
2 opendeferred goal
cbn in Hkey
2 opendeferred goal
subst k
2 opendeferred goal
iDestruct big_sepL_elem_of_ _ _ Hin with Hps as Hk
2 opendeferred goal
iDestruct pointsto_ne with Hl Hk as %Hne
2 opendeferred goal
contradiction
deferred goal
–iPureIntro
apply NoDup_cons
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
For promotion: allocating a nonempty variadic snapshot yields its populated pieces, with the read-only pointer installed in the frame. This lifts rule_snapshot through wp_lift_run; only preservation of the caller's world interpretation remains a premise.
Proof 66 steps Qed
For promotion: the Iris rule for VaArgs, lifted directly from rule_va_args through wp_pure_next.
Explore proof 5 tactics
Initial goal
intros Hp
apply wp_pure_nextregistry wi ge _ _ [ ]
intros m fuel
apply rule_va_args
exact Hp
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
For promotion: a variadic argument read is a heap write, not a pure read of the frame. Owned pieces justify va_arg_res and retain exactly their keys after the cursor update. This lifts rule_va_arg through wp_write, including its world-frame premise.
Explore proof 6 tactics
Initial goal
intros Hargs Hkeys Hread Hwi
iIntros Hps HK
iApply wp_writeregistry wi ge ps ps′ _ _ [ ] upd with Hps HK ; exact Hkeys | | exact Hwi
intros m fuel Hfacts
destruct Hreadm Hfacts as Hres & Hrest
split ; exact rule_va_arg_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hargs Hres | exact Hrest
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
For promotion: a pointer va_arg reads its snapshot cell and advances only the mutable cursor. The source and literal pieces are framed, including when the argument is the terminating null pointer.
Proof 152 steps Qed
For promotion: a pointer load can return a read-only literal. Its life comes from the caller's existing pieces rather than a new token. This lifts rule_let and op_raw_load_pointer through wp_read_with, and preserves those pieces.
Proof 28 steps Qed
For promotion: a memory-reading operation justified by the world interpretation, without claiming ownership of a world-owned cell. It is rule_let lifted through wp_read_with.
Explore proof 13 tactics
Initial goal
intros Hg Hc Hargs Hop
iIntros HK
iApply wp_read_with_ _ _ emp λm ⇒ op_reso k xs m = SomeOpResRValx m _ _ [ ] with [] [HK]
5 openfocused goal
focused goal
focused goal
shelved goal
–iIntros σ (%h & _ & %Hf) _
5 opendeferred goal
deferred goal
deferred goal
shelved goal
destruct Hf as _ & _ & _ & Hw
5 opendeferred goal
deferred goal
deferred goal
shelved goal
iPureIntro
5 opendeferred goal
deferred goal
deferred goal
shelved goal
exact Hop_ _ _ Hw
4 opendeferred goal
deferred goal
deferred goal
shelved goal
–intros m fuel Hm
4 opendeferred goal
deferred goal
shelved goal
exact rule_let_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hg Hc Hargs Hm
2 opendeferred goal
deferred goal
–done
deferred goal
–iNext
iIntros _
iExact HK
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The compiled proper-name helper preserves every framed resource: it never dereferences the pointer or calls an external function.
Explore proof 8 tactics
Initial goal
iIntros HΦ
rewrite proper_name_entry
iApply wp_enter ; exact find_proper_name_start | reflexivity |
iNext
cbn [ b_insts b_jump proper_name_start ]
iApply wp_ret ; reflexivity | reflexivity |
iNext
iExact HΦ
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The footer links the fixture's literals, but libc supplies stdout.
The stdio world owns the stdout cell and guarantees its read, not an Iris piece owned by the program.
The program-owned pieces containing the footer's format and string literals. The stdio precondition reads them through pts_lookup; the world does not have to own them.
Output specs supplied by the stdio package. The preconditions are required for these four exact calls, including the NUL-terminated format and string arguments; output failure cannot waive them.
The footer's pure symbol copies find the same literal in ge.
Explore proof 3 tactics
Initial goal
intros Hin
apply proj1proj2Hlinked
repeat destruct Hin as ← | Hin ; try contradiction ; vm_compute ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The output call is safe and returns an arbitrary canonical int, retaining the caller's heap and stdio interpretation on errors too.
Proof 32 steps Qed
The complete help footer, including failed and partial output: every stdio result is ignored and every framed resource survives.
Proof 62 steps Qed
The reachable version path uses the linked heading, author, and format literals; the stream itself belongs to the stdio world.
The existing literal resources include each author's live object; this prevents the collector from rewriting its read-only capability.
The four initialized array cells that the counting loop passes on.
The pure literal copies in the reachable array helper are linked.
Explore proof 3 tactics
Initial goal
intros Hin
apply proj1proj2Hlinked
repeat destruct Hin as ← | Hin ; try contradiction ; vm_compute ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Advance one memory-independent IR let on the fixed version path.
These are the stdio contracts for the six exact version calls. The mixed pointer/int classes are checked before any output result; partial output and negative results retain the caller's resources.
The reachable version calls preserve their literals and ignore every canonical int result, including negative and partial output.
Proof 32 steps Qed
The reachable array helper prints the heading and four authors, preserving the array and literal resources for every stdio result. Its fixed count is discharged by version_etc_va, not assumed by main.
Proof 161 steps Qed
The variadic counting helper in the linked program.
The allocation block of the counting helper.
The loop header binds the current author count.
The loop body consumes and stores one variadic pointer.
The null test selects another iteration or the array helper.
The back edge increments the count of non-null authors.
The exit block passes the derived count to the array helper.
Zero pointer bytes coincide with the eight-byte string block.
Proof 17 steps Qed
Split off one zero pointer cell without expanding the rest of its allocation into individually searched heap pieces.
Explore proof 4 tactics
Initial goal
rewrite ! replicate_add bytes_app auxes_app
iIntros [Hx Hrest] [Ha Htail]
iFrame Hrest Htail
iApply version_zero_cell with Hx Ha
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Five zero cells suffice for the four authors and their terminator; the rest of the allocated array is unused.
Explore proof 9 tactics
Initial goal
iIntros Hobj
iDestruct obj_zero_block with Hobj as (Hl & Hx & Ha) ; compute ; discriminate |
iSplitL Hl ; iExact Hl |
iDestruct version_zero_cell_prefixb 0 72 with Hx Ha as (H0 & Hx & Ha)
iDestruct version_zero_cell_prefixb 8 64 with Hx Ha as (H1 & Hx & Ha)
iDestruct version_zero_cell_prefixb 16 56 with Hx Ha as (H2 & Hx & Ha)
iDestruct version_zero_cell_prefixb 24 48 with Hx Ha as (H3 & Hx & Ha)
iDestruct version_zero_cell_prefixb 32 40 with Hx Ha as (H4 & _ & _)
iFrame H0 H1 H2 H3 H4
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The entry binds the heading literals and the caller's va_list.
Explore proof 1 tactics
Initial goal
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Program-local allocations preserve the caller's opaque world.
Storing a pointer in an owned program cell preserves that world; no ownership of the output stream is introduced.
Advancing an owned va_list cursor preserves the caller's world.
The heading, cursor and array registers survive every loop round.
The common loop body begins after the scalar index and flight.
Check the non-null body once, with an abstract incoming and outgoing environment, rather than expanding its proof at every author.
Proof 41 steps Qed
Select the concrete index, then reuse the opaque non-null body.
The counting loop reads four literal authors and the actual null terminator, then calls the array helper with the derived count four. It returns the caller's literals, snapshot cells, and advanced cursor.
Proof 97 steps Qed
The only version invocation in main: four literal author pointers, followed by the pointer-class interpretation of const zero.
The five pointer cells selected from main's actual snapshot.
The selected cells have distinct life, byte, and capability keys.
Explore proof 3 tactics
Initial goal
unfold version_snapshot_cells , cell
cbn
repeat constructor ; intros Hin ; repeat apply elem_of_cons in Hin ; destruct Hin as Hin | Hin ; inversion Hin
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The selected cells are populated by argument indices four through eight of the actual snapshot, not supplied as new initial memory.
Proof 15 steps Qed
Extracting only the used cells discards unused snapshot padding.
Proof 9 steps Qed
The public variadic wrapper in the linked program.
Its single block constructs a va_list and calls the counting helper.
The variadic entry retains every actual argument for Snapshot.
Explore proof 1 tactics
Initial goal
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The local va_list begins with one zero pointer cell.
Explore proof 5 tactics
Initial goal
iIntros Hobj
iDestruct obj_zero_block with Hobj as (Hl & Hx & Ha) ; compute ; discriminate |
iSplitL Hl ; iExact Hl |
iDestruct version_zero_cell_prefixcb 0 24 with Hx Ha as (Hc & _ & _)
iExact Hc
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Snapshot population preserves the same opaque world under the already proved fresh-object and exact-store frame facts.
Main can apply this triple directly after the four proper_name identities. The snapshot and the counting loop derive the count; neither the count nor the array contents are caller premises.
Proof 48 steps Qed
HelloVersionOn over a Logic instance of its own.