rocq/theories/HelloMain.v
GNU Hello's main through the program logic
Main's proof calls the triples of every Hello layer, so it applies each layer's functor to one Logic instance: two applications of Logic have distinct expressions, and their triples could not be combined. The world is libc's, and its interpretation wi stays abstract: each premise below is what one call needs of it, so a concrete interpretation discharges them once.
Main's function, read from the linked module.
A block of main.
A 16-aligned base is 8-aligned.
Explore proof 6 tactics
Initial goal
intros H
apply Z.mod_divide in H ; | lia
destruct H as k →
replace k × 16 with 2 × k × 8 by lia
apply Z.mod_mul
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The literals main copies: "" for setlocale, the default greeting, read-only, and close_stdout's function pointer.
"Hello, world!".
Its bytes.
close_stdout, as a function pointer.
Hello's symbols put them there.
Explore proof 2 tactics
Initial goal
vm_compute
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Main's entry binds argc and argv.
Explore proof 1 tactics
getopt_long's literals
Main parses its options with getopt_long(argc, argv, "g:t", longopts, NULL). The option string and the table are Hello's read-only literals; every option's flag is null, so getopt_long returns its value.
"g:t".
The long options table.
The traditional greeting, "hello, world".
Hello's long options: greeting, taking an argument, as 'g'; traditional as 't'; help and version as 128 and 129.
Hello's symbols put them there.
Explore proof 2 tactics
Initial goal
vm_compute
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
One of main's arguments: the C string at arg_ptr, in the object arg_base with the region arg_region, with contents arg_text.
Its pieces: the string's.
getopt_long's input for one run of main, whose argv is at av and whose arguments are sargs: the same at every call, as the registry is fixed for the run.
Argv's order is that of the arguments.
Explore proof 3 tactics
Initial goal
cbn
rewrite map_map
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The literals getopt_long reads are in memory: the option string, the table's bounds and its records.
What main learns from getopt_long's code: a C int, and 'g' ('g' or --greeting) comes with a nonnull borrow of an argument, as both take one.
Explore proof 21 tactics
Initial goal
unfold getopt_int
intros → & _ | → | → & _ | byte & mode & Hb & _ & _ & → & Hmode & Harg | rest & Hs & _ | i & o & Hi & Hflag & _ & Harg
6 openfocused goal
focused goal
focused goal
focused goal
focused goal
–split ; lia | intros E ; discriminate E
5 opendeferred goal
deferred goal
deferred goal
deferred goal
deferred goal
–split ; lia | intros E ; discriminate E
4 opendeferred goal
deferred goal
deferred goal
deferred goal
–split ; lia | intros E ; discriminate E
3 opendeferred goal
deferred goal
deferred goal
–destruct Z.ltb_specbyte 128 as Hlt | Hge
4 openfocused goal
deferred goal
deferred goal
+split ; lia |
4 opendeferred goal
deferred goal
deferred goal
intros →
4 opendeferred goal
deferred goal
deferred goal
cbn in Hmode
4 opendeferred goal
deferred goal
deferred goal
assert mode = 1 as → by congruence
4 opendeferred goal
deferred goal
deferred goal
exact getopt_required_argument_ _ Harg
3 opendeferred goal
deferred goal
deferred goal
+split ; lia | lia
2 opendeferred goal
deferred goal
–cbn in Hs
2 opendeferred goal
discriminate Hs
deferred goal
–destruct i as | | | | i ; | | | | destruct i ; discriminate Hi ; unfold hello_options in Hi ; cbn in Hi ; injection Hi as ← ; cbn in Hflag ; rewrite Hflag
4 openfocused goal
focused goal
focused goal
+split ; lia |
4 opendeferred goal
deferred goal
deferred goal
intros _
4 opendeferred goal
deferred goal
deferred goal
exact getopt_required_argument_ _ Harg
3 opendeferred goal
deferred goal
deferred goal
+split ; lia | intros E ; discriminate E
2 opendeferred goal
deferred goal
+split ; lia | intros E ; discriminate E
deferred goal
+split ; lia | intros E ; discriminate E
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
argv as one block
Main hands argv to getopt_long whole, as HelloConv.v hands mbrtowc its cells: its life, the bytes of its argc + 1 pointer slots and every aux slot of them (block_ps). The bytes are those of the pointers ps argv holds, then null (argv_bytes); the aux slot at the start of each holds its capability (argv_caps). getopt_long may permute the arguments, and Campaign 4's getopt_slots says each slot's bytes are a byte each, so the block it hands back is of the same form.
The eight bytes of the address x, least significant first.
The bytes of the slots holding the pointers L.
argv's bytes, holding ps and the null sentinel.
The aux slots cs of argv holding ps: as many as its bytes, the first of each pointer's eight holding its capability.
The memory m holds the pointer q at a: a word address, its eight bytes, and its capability in the aux slot.
Eight bytes per pointer.
Explore proof 5 tactics
Initial goal
induction L as | q L IH ; reflexivity |
cbn [ slots_bytes flat_map ]
rewrite length_app IH
cbn
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The j-th byte of the k-th slot.
Explore proof 13 tactics
Initial goal
revert k
induction L as | x L IH ; intros k Hk Hj ; discriminate Hk |
cbn [ slots_bytes flat_map ]
destruct k as | k
2 openfocused goal
–cbn in Hk
2 opendeferred goal
injection Hk as →
2 opendeferred goal
rewrite lookup_app_l ; | cbn ; lia
2 opendeferred goal
do 8 destruct j as | j ; reflexivity |
2 opendeferred goal
lia
deferred goal
–rewrite lookup_app_r ; | cbn ; lia
change lengthslot_bytesptr_addrx with 8%nat
replace 8 × Sk + j − 8%nat with 8 × k + j%nat by lia
exact IHk Hk Hj
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Eight canonical bytes are determined by their little-endian value.
Explore proof 17 tactics
Initial goal
intros H H′ E i Hi
unfold load_bytes in E
change Z.to_nat8 with 8%nat in E
simpl in E
pose proof H0 ltac:lia as H0 ; pose proof H1 ltac:lia as H1 ; pose proof H2 ltac:lia as H2 ; pose proof H3 ltac:lia as H3 ; pose proof H4 ltac:lia as H4 ; pose proof H5 ltac:lia as H5 ; pose proof H6 ltac:lia as H6 ; pose proof H7 ltac:lia as H7
pose proof H′0 ltac:lia as H0′ ; pose proof H′1 ltac:lia as H1′ ; pose proof H′2 ltac:lia as H2′ ; pose proof H′3 ltac:lia as H3′ ; pose proof H′4 ltac:lia as H4′ ; pose proof H′5 ltac:lia as H5′ ; pose proof H′6 ltac:lia as H6′ ; pose proof H′7 ltac:lia as H7′
change Z.of_nat0 with 0 in E ; change Z.of_nat1 with 1 in E ; change Z.of_nat2 with 2 in E ; change Z.of_nat3 with 3 in E ; change Z.of_nat4 with 4 in E ; change Z.of_nat5 with 5 in E ; change Z.of_nat6 with 6 in E ; change Z.of_nat7 with 7 in E
assert m_bytesm a + 7 = m_bytesm′ a + 7 by lia
assert m_bytesm a + 6 = m_bytesm′ a + 6 by lia
assert m_bytesm a + 5 = m_bytesm′ a + 5 by lia
assert m_bytesm a + 4 = m_bytesm′ a + 4 by lia
assert m_bytesm a + 3 = m_bytesm′ a + 3 by lia
assert m_bytesm a + 2 = m_bytesm′ a + 2 by lia
assert m_bytesm a + 1 = m_bytesm′ a + 1 by lia
assert m_bytesm a + 0 = m_bytesm′ a + 0 by lia
assert i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7 as Hc by lia
destruct Hc as [ ->| [ ->| [ ->| [ ->| [ ->| [ ->| [ ->| -> ] ] ] ] ] ] ] ; assumption
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A slot is Campaign 4's: a pointer_slot of canonical bytes.
Explore proof 14 tactics
Initial goal
intros Hr & Hb & Hc
split ; split ; exact Hr | split ; | exact Hc |
2 open–rewrite <- Z.mod_smallptr_addrq 2 ^ 64 ; | exact Hr
2 openchange 2 ^ 64 with 256 ^ 8
2 openrewrite <- stored_bytes_valuem a 8 ptr_addrq ; | lia
2 openapply load_bytes_agree ; lia |
2 openintros i Hi
2 openrewrite stored_byte ; | exact Hi
2 openexact Hbi Hi
–intros k Hk
rewrite Hbk Hk
unfold byte_of
apply Z.mod_pos_bound
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
And back.
Explore proof 17 tactics
Initial goal
intros Hr & Hl & Hc Hb
split ; exact Hr |
split ; | exact Hc
intros i Hi
rewrite <- stored_bytem a 8 ptr_addrq i Hi
apply load_bytes_canonicalm store_bytesm a 8 ptr_addrq a ; exact Hb | | | exact Hi
2 openfocused goal
–intros k Hk
2 opendeferred goal
rewrite stored_byte ; | exact Hk
2 opendeferred goal
unfold byte_of
2 opendeferred goal
apply Z.mod_pos_bound
2 opendeferred goal
lia
deferred goal
–rewrite Hl
rewrite stored_bytes_value ; | lia
change 256 ^ 8 with 2 ^ 64
symmetry
apply Z.mod_small
exact Hr
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
getopt_slots is a slot at each eighth byte, for each pointer and the sentinel.
Explore proof 17 tactics
Initial goal
revert a
induction ps as | p ps IH ; intros a H
2 open–cbn [ getopt_slots ]
2 openapply slot_pointer
2 openpose proof H0%nat null eq_refl as H0
2 openreplace a + 8 × Z.of_nat0 with a in H0 by lia
2 openexact H0
–cbn [ getopt_slots ]
pose proof H0%nat p eq_refl as H0
replace a + 8 × Z.of_nat0 with a in H0 by lia
destruct slot_pointer_ _ _ H0 as Hp Hb
split ; exact Hp |
split ; exact Hb |
apply IH
intros k q Hk
replace a + 8 + 8 × Z.of_natk with a + 8 × Z.of_natSk by lia
exact HSk q Hk
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
And back.
Explore proof 14 tactics
Initial goal
revert a
induction ps as | p ps IH ; intros a Hs k q Hk
2 open–destruct k as | k ; | destruct k ; discriminate Hk
2 openinjection Hk as ←
2 openreplace a + 8 × Z.of_nat0 with a by lia
2 opendestruct Hs as Hp Hb
2 openexact pointer_slot_at_ _ _ Hp Hb
–destruct Hs as Hp & Hb & Hr
destruct k as | k
2 openfocused goal
+injection Hk as ←
2 opendeferred goal
replace a + 8 × Z.of_nat0 with a by lia
2 opendeferred goal
exact pointer_slot_at_ _ _ Hp Hb
deferred goal
+replace a + 8 × Z.of_natSk with a + 8 + 8 × Z.of_natk by lia
exact IH_ Hr k q Hk
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Memory whose slots hold ps holds argv's bytes and slots for ps.
Explore proof 36 tactics
Initial goal
intros Hs
pose proof at_of_slotsm a ps Hs as H
split
2 open–apply list_eq
2 openintros i
2 openunfold mem_bytes , argv_bytes
2 openrewrite list_lookup_fmap
2 opendestruct decidei < 8 × lengthps ++ null%nat as Hi | Hi
3 openfocused goal
+rewrite lookup_seq_lt ; | exact Hi
3 opendeferred goal
cbn [ fmap option_fmap option_map ]
3 opendeferred goal
pose proof Nat.div_mod_eqi 8 as Ei
3 opendeferred goal
pose proof Nat.mod_upper_boundi 8 ltac:lia as Ej
3 opendeferred goal
destruct lookup_lt_is_Some_2ps ++ null i / 8 as q Hq ; lia |
3 opendeferred goal
rewrite Ei slots_bytes_lookup_ _ _ _ Hq Ej
3 opendeferred goal
destruct H_ _ Hq as _ & Hb & _
3 opendeferred goal
f_equal
3 opendeferred goal
rewrite <- Hb ; | lia
3 opendeferred goal
f_equal
3 opendeferred goal
lia
2 opendeferred goal
+rewrite lookup_seq_ge ; | lia
2 opensymmetry
2 openapply lookup_ge_None_2
2 openrewrite length_slots_bytes
2 openlia
–split ; apply length_mem_auxes |
intros k q Hk
pose proof lookup_lt_Some_ _ _ Hk as Hlt
unfold mem_auxes
rewrite list_lookup_fmap
rewrite lookup_seq_lt ; | lia
cbn
destruct H_ _ Hk as _ & _ & Hc
rewrite <- Hc
f_equal
f_equal
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The i-th aux piece is the i-th slot's.
Explore proof 10 tactics
Initial goal
revert o i
induction cs as | y cs IH ; intros o i H ; discriminate |
rewrite aux_ps_cons
destruct i as | i ; cbn in H |- *
2 open–injection H as →
2 openrewrite Z.add_0_r
2 openreflexivity
–rewrite IHo + 1 i H
do 3 f_equal
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A pointer of a permitted order of argv is one of the arguments'.
Explore proof 4 tactics
Initial goal
intros H Hq
apply Permutation_in_ Permutation_symgetopt_order_inventory_ _ H in Hq
apply in_map_iff in Hq as s & ← & Hs
eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A C int cut to 32 bits: itself if nonnegative, else 2^32 more.
Explore proof 7 tactics
Initial goal
unfold getopt_int
intros Hx
destruct Z.ltb_specx 0
2 openfocused goal
–symmetry
2 opendeferred goal
apply Z.mod_uniquex 2 ^ 32 −1 ; left ; lia | lia
deferred goal
–apply Z.mod_small
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A C int's 32 bits are those of a nonnegative C int k just if it is k.
Explore proof 4 tactics
Initial goal
intros Hx Hk
rewrite int32_modx Hx
unfold getopt_int in Hx
destruct Z.ltb_specx 0 ; split ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A C int's 32 bits are all ones just if it is -1, getopt's end.
Explore proof 4 tactics
Initial goal
intros Hx
rewrite int32_modx Hx
unfold getopt_int in Hx
destruct Z.ltb_specx 0 ; split ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Main's proof over one Logic instance shared by every layer.
The Iris instance of the registry and wi.
The expressions of the language.
The genv links Hello.
An allocation of a fresh object, with its pieces added, keeps wi.
memset has its contract, and zeroing eight bytes of a block the program owns keeps wi.
set_program_name's contracts, and the layout and store premises of its three cells, as HelloName states them.
setlocale has libc's contract. The world interpretation keeps every lent name where lent_at says, admits setlocale's precondition for a category and a string the program owns, and survives its return, which lends every category's new name and sets the codec piece.
setlocale(c, p) over libc's world, from wp_lend: owning every category's name, the codec piece and the string at p, the call lends every category's new name for good, gives the codec piece a new codec and binds d to null or c's new name.
Proof 33 steps Qed
A pointer store into a cell the program owns keeps wi.
atexit has a contract returning an int, which admits the call main makes, registering close_stdout, and whose return keeps the program's pieces and wi: the registration is libc's state.
Eight zero bytes and an empty slot at offset 0 are a null pointer cell.
Explore proof 8 tactics
Initial goal
rewrite / bytes / auxes / pcell - pts_app
assert E : byte_psb 0 replicate8 0 ++ aux_psb 0 CNone = cellb 0 0 ++ PAuxb 0, VAuxCNone
2 openfocused goal
{vm_compute
2 opendeferred goal
reflexivity
deferred goal
rewrite E pts_app
cbn [ ptr_addr ptr_cap ]
rewrite / pts ! big_sepL_cons big_sepL_nil
iSplit ; iIntros [H [A _]] ; iFrame | iIntros [A H] ; iFrame
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Enter a block of main.
mbszero at the start of an object: mbszero_spec at offset 0.
Explore proof 8 tactics
Initial goal
intros Lx Lc Hb8 Hend
pose proof mbszero_specregistry wi ge Hlinked b reg 0 xs cs Φ as H
rewrite ! Z.add_0_r in H
iApply H ; exact Hmemset | exact Lx | exact Lc | exact Hb8 | reflexivity | lia | exact Hend |
intros m m′ wd h Hr Hin Hw
pose proof Kmemsetb reg 0 xs cs m m′ wd h as K
rewrite ! Z.add_0_r in K
exact KHr Hin Hw
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The instructions of main's start block from setlocale's call on.
The temporaries main has bound before setlocale: argc, argv, the greeting's cell b4, the state b6, and the literal "".
A fresh heap object of main: positive, 16-aligned, in the address space.
Main's start block up to setlocale: two fresh objects, b4 for the greeting's cell and b6 for the conversion state, which mbszero zeroes; argv0 loaded and handed to set_program_name, which leaves the name cells at a suffix of it; the literal "" copied.
Proof 66 steps Qed
The state is zeroed.
argv0, the program's name.
setlocale(LC_ALL, "").
The rest of main's start block, from setlocale's call: setlocale lends every category's new name and sets the codec; the default greeting is stored in b4's cell; atexit registers close_stdout; and the option loop is entered.
Proof 55 steps Qed
setlocale(LC_ALL, "").
The default greeting, stored in b4's cell.
atexit(close_stdout).
Main's start block, from its entry to the option loop: the two segments above.
Proof 10 steps Qed
getopt_long's call
The run's argv is at av, in an object of the region ar, and holds the arguments sargs; the launcher copies each into an object of its own. getopt_long's registry entry is Campaign 4's libc_getopt_contract for this run's input, fixed for the run. Main owns argv as one block, the arguments' strings and the getopt token; the call hands argv back permuted, the strings unchanged and the token naming the new optarg and optind.
argv: aligned, its argc + 1 slots in its region, argc a positive C int, each argument a C string.
The number of argv's bytes and aux slots.
getopt_long has libc's contract for this run's input, over the native parser's initialized and running representations and its allocation requests.
The contract.
wi ties libc's optarg and optind cells to the parser's state and the getopt token, as GetoptLogic.v's reads need.
wi keeps Hello's option literals in memory.
wi admits getopt_long's libc side where main owns argv and the arguments: the parser's representation, its private roots and reads, and their separation from the call's inputs and outputs.
getopt_long's private roots and libc's cells are apart from the program's objects, and it releases none of them.
A return of getopt_long keeps wi, with argv's block holding what the memory then holds and the token naming the new optarg and optind.
A permitted order of argv has argc pointers.
Explore proof 5 tactics
Initial goal
intros H
rewrite <- length_maparg_ptr sargs
symmetry
apply Permutation_length
map arg_ptr sargs ≡ₚ psexact getopt_order_inventory_ _ H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Owning argv's block holding ps, and the arguments, the memory's slots hold ps: getopt_slots.
Proof 58 steps Qed
The arguments are admitted (getopt_pre) where main owns argv's block, holding a permitted order ps, the arguments' strings and the token, whose optind i is at most argc.
Proof 64 steps Qed
A return of getopt_long satisfies its postcondition.
Explore proof 4 tactics
Initial goal
intros H
inversion H as trace′ ending s0 m0 w0 born Habi Hpre Hp Hpost | ; subst
exists born
exact Hpost
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A return of the call keeps every piece but argv's bytes and slots agreeing (prefix_agrees_out): its roots and libc's cells are apart from the program's objects, and argv is the one block of the program's it writes. So with argv's block holding what the memory then holds, and any token, the ghost heap agrees; the live objects stay apart and the runtime ready.
Proof 52 steps Qed
getopt_long(argc, argv, "g:t", longopts, NULL)'s triple, from libc_getopt_contract: owning argv's block, holding a permitted order ps of the arguments, their strings, and the token, whose optind is at most argc, the call binds d to its code, a C int, and hands back argv holding another permitted order, the strings, and the token naming the new optarg and optind, in range; a 'g' comes with a nonnull borrow of an argument.
Proof 77 steps Qed
The option loop
Main calls getopt_long until it returns -1, at block iw_1.L8. A 'g' stores optarg in the greeting's cell b4 (iw_1.L35), a 't' the traditional greeting (iw_1.L42); any other code but --help and --version sets pr.2, the "lose" flag (iw_1.L52). Each goes back round. getopt_long promises no bound on its calls, so the loop is proved by Löb induction: each round enters a block, which takes a step. Its exits are the version and help blocks, iw_1.L21 and iw_1.L39, and the end of options, iw_1.L10, which the proof leaves to continuations.
libc's optarg cell is the global optarg, and both cells are at word addresses.
The greetings b4's cell may hold in the loop: the default, the traditional one, or a nonnull borrow of an argument.
What main owns in the loop: argv's block holding ps, the arguments' strings, the getopt token, and the greeting's cell b4 holding g.
What main knows in the loop: its temporaries, argv's order, the token's optind in range and the greeting.
The loop's entry by the edge from: from start with pr.2 0, from iw_1.L52 with 1, and from iw_1.L35 or iw_1.L42 with what pr.2 was.
An exit of the loop: entering the block lab from the block from, with the loop's facts and pieces and pr.2 bound to 0 or 1.
The option loop, from its entry by any edge to one of its exits.
Proof 168 steps Qed
Enter iw_1.L8: pr.2 is lose.
getopt_long(argc, argv, "g:t", longopts, NULL).
-1: the end of options.
--version.
'g': the greeting is optarg.
--help.
't': the traditional greeting.
Any other code: an unknown option; pr.2 is 1.
argv's block, holding q first: its life, q's cell, and the rest's bytes and slots.
Proof 12 steps Qed
Main from its entry to the option loop's exits: main_start, with argv's first slot and string out of argv's block and the arguments, then main_loop from start. The continuation is given everything the start block leaves outside the loop, and builds the exits.