rocq/theories/HelloJoin.v

GNU Hello's greeting, and the whole program

HelloMain proves main from its entry up to the greeting at iw_1.join (main_to_join). This file proves the rest: the greeting block, which measures the greeting, allocates a wide buffer with xmalloc, converts the greeting into it with gnulib's rpl_mbsrtowcs (HelloConv's rpl_mbsrtowcs_spec), prints it with wprintf, frees it and exits, or reports a failed conversion with error(1, ...). It lives apart from HelloMain so that HelloMain does not wait for HelloConv: the two compile side by side, and this file after both.

The premises are those of the conversion, as HelloConv states them, and of the greeting's own calls. Like HelloMain's, each is what one call needs of the world interpretation wi, which stays abstract.

From iris.proofmode Require Import proofmode

From iris.base_logic.lib Require Import gen_heap

From iris.program_logic Require Import language weakestpre

From Stdlib Require Import ZArith Lia

From Stdlib Require String

From Nanofil Require Import Term Syntax Values Memory Runtime Ops Semantics Run StepRules Symbolic ExternalCalls ExternalMachine Pieces Heap ContractFrame Language Logic StringLogic MemLogic LentLogic Locale LocaleLogic Libc HelloModule HelloLeaf HelloLocale HelloConvDefs HelloConv HelloName HelloProgName HelloClose HelloVersion Startup Getopt GetoptLogic HelloMain

Open Scope Z_scope

Open Scope list_scope

xmalloc's function, read from the linked module.

29Definition xmalloc_fn: func ≔

Eval vm_compute in hello_fn"xmalloc"

A block of xmalloc.

32Definition xmalloc_blocks : String.string : block ≔

hblkxmalloc_fn s

A 16-aligned address is 4-aligned.

35Lemma mod16_mod4

∀ b

b mod 16 = 0

b mod 4 = 0

Explore proof 6 tactics

Initial goal

b :

⊢

b mod 16 = 0 → b mod 4 = 0

intros H

b :

H :

b mod 16 = 0

⊢

b mod 4 = 0

apply Z.mod_divide ; lia |

b :

H :

b mod 16 = 0

⊢

4 | b

apply Z.divide_trans4 16 b

2 open

b :

H :

b mod 16 = 0

⊢

4 | 16

focused goal

b :

H :

b mod 16 = 0

⊢

16 | b

–exists 4

2 open

b :

H :

b mod 16 = 0

⊢

16 = 4 × 4

deferred goal

b :

H :

b mod 16 = 0

⊢

16 | b

reflexivity

deferred goal

b :

H :

b mod 16 = 0

⊢

16 | b

–apply Z.mod_divide ; lia | exact H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros H

apply Z.mod_divide ; lia |

apply Z.divide_trans4 16 b

–exists 4

reflexivity

–apply Z.mod_divide ; lia | exact H

The traditional greeting's bytes, "hello, world".

43Definition traditional_bytes: listZ ≔

104; 101; 108; 108; 111; 44; 32; 119; 111; 114; 108; 100

setlocale returns a pointer.

46Lemma setlocale_returns

∀ rep requests

contract_returnslibc_setlocale_contractrep requests = RClassP

Explore proof 1 tactics

Initial goal

rep :

mem → libc_world → Prop

requests :

listword → mem → libc_world → Z → Z → Prop

⊢

contract_returnslibc_setlocale_contractrep requests = RClassP

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

reflexivity

setlocale(c, v), binding a pointer, fits setlocale's ABI.

50Lemma setlocale_query_abi

∀ rep requests d c v

contract_abilibc_setlocale_contractrep requests CResultd P ArgW c; ArgP v

Explore proof 1 tactics

Initial goal

rep :

mem → libc_world → Prop

requests :

listword → mem → libc_world → Z → Z → Prop

d :

name

c, v :

value

⊢

contract_abilibc_setlocale_contractrep requests CResultd P ArgW c; ArgP v

split ; right ; exists d ; reflexivity | exists c, v ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

split ; right ; exists d ; reflexivity | exists c, v ; reflexivity

54Module HelloJoin R : Runtime

55Module HM ≔ HelloMain R

56Module LG0 ≔ HM.LG0

57Module HC ≔ HelloConvOn R LG0

58Module HCl ≔ HelloCloseOn R LG0

59Module HP ≔ HM.HP

60Module HV ≔ HM.HV

61Module HLo ≔ HM.HLo

62Module HL ≔ HM.HL

63Module LL ≔ HM.LL

64Module ML ≔ HM.ML

65Module SL ≔ HM.SL

66Module LG ≔ LG0

67Module L ≔ LG.L

Import L LG SL ML LL HL

70Section join

71Context registry : name → optioncontractlibc_world wi : mem → libc_world → gmappiece pval → Prop `{!SafepointStablewi} ge : genv

The genv links Hello.

75Context Hlinked : hello_linkedge

An allocation of a fresh object, with its pieces added, keeps wi.

78Context Kalloc : ∀q m wd h base, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

memset has its contract, and zeroing eight bytes of a block the program owns keeps wi.

83Context Hmemset : registryTAtom"memset" = Somememset_contractlibc_world

83Context Kmemset : ∀b reg o xs cs m m′ wd h, memset_resultm mkPtrb + o Objb 0 8 m′ → ∀l v, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → wim′ wd overwriteblock_psb reg o replicate8 0 clear_slotso cs h

set_program_name's contracts.

89Context Hstrrchr : registryTAtom"strrchr" = Somestrrchr_contractlibc_world

89Context Hmemcmp : registryTAtom"memcmp" = Somememcmp_contractlibc_world

89Context Hstrncmp : registryTAtom"strncmp" = Somestrncmp_contractlibc_world

set_program_name's cells: their layout and store premises.

94Context pn nreg sreg : region

94Context nb sb : Z

94Context Hnb : lookupTAtom"program_invocation_name" ge_globalsge = SomemkPtrnb Objnb

94Context Hsb : lookupTAtom"program_invocation_short_name" ge_globalsge = SomemkPtrsb Objsb

94Context Hpn_end : program_name_b + 8 ≤ r_endpn

94Context Hnb_cell : 0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ∧ r_endnreg ≤ 2 ^ 48

94Context Hsb_cell : 0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ∧ r_endsreg ≤ 2 ^ 48

94Context Kpn : HP.HN.store_keepswi program_name_b pn

94Context Knb : HP.HN.store_keepswi nb nreg

94Context Ksb : HP.HN.store_keepswi sb sreg

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.

107Context rep : mem → libc_world → Prop

107Context requests : listword → mem → libc_world → Z → Z → Prop

107Context Hsetlocale : registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests

107Context Hlent : ∀m w h k p t, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t

107Context Hset_pre : ∀m w h c p b reg bytes, wim w h → Inc locale_categories → string_okp b reg bytes → all_agreem string_psp b reg bytes → libc_setlocale_prerep WIntc; WPtrp m w

107Context Kset : ∀r args c p s m w h trace values s′ m′ w′, wim w h → agreesm h → live_disjointm → R.readys m → M.E.invokelibc_setlocale_contractrep requests r args WIntc; WPtrp s m w trace CallReturnvalues s′ m′ w′ → ∃q new : Z → ptr × listZ c′, values = WPtrq ∧ q = mkPtr0 CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new

A pointer store into a cell the program owns keeps wi.

122Context Kpstore : ∀b reg o x xp m wd h, ∀l v, l, v ∈ PLiveb, VLivereg ++ PAuxb o, VAuxptr_capx :: cellb o ptr_addrx → h !! l = Somev → wim wd h → wistore_bytesstore_auxm b + o ptr_capxp b + o 8 ptr_addrxp wd overwritePLiveb, VLivereg ++ PAuxb o, VAuxptr_capxp :: cellb o ptr_addrxp h

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.

132Context atexit_spec : contractlibc_world

132Context Hatexit : registryTAtom"atexit" = Someatexit_spec

132Context Hatexit_ret : contract_returnsatexit_spec = RClassW

132Context Hatexit_abi : contract_abiatexit_spec CResultTAtom"v15" W ArgP TmpTAtom"v14"

132Context Hatexit_pre : ∀m w h, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w

132Context Katexit : ∀r args s m w h trace values s′ m′ w′, wim w h → agreesm h → live_disjointm → R.readys m → M.E.invokeatexit_spec r args WPtrclose_stdout_ptr s m w trace CallReturnvalues s′ m′ w′ → ∃x, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h

argv: aligned, its argc + 1 slots in its region, argc a positive C int, each argument a C string.

145Context av : Z

145Context ar : region

145Context sargs : listargument

145Context Hav : 0 < av ∧ av mod 8 = 0 ∧ av + 8 × Z.of_natlengthsargs + 1 ≤ r_endar ∧ r_endar ≤ 2 ^ 48

145Context Hargc : 1 ≤ Z.of_natlengthsargs < 2 ^ 31

145Context Hargs : Forallλs ⇒ string_okarg_ptrs arg_bases arg_regions arg_texts sargs

getopt_long has libc's refined contract for this run's input, over the native parser's initialized and running representations, its allocation requests and the transition an ordinary return makes. Every path is proved whatever the transition, so the safety contract's own returns are the case of a transition that always holds.

156Context initialized running : mem → libc_world → Prop

156Context grequests : listword → mem → libc_world → Z → Z → Prop

156Context transition : listword → mem → libc_world → listZ → listevent → listword → mem → libc_world → Prop

156Context Hgetopt : registryTAtom"getopt_long" = Somelibc_getopt_refined_contracthello_inputav sargs initialized running grequests transition

wi ties libc's optarg and optind cells to the parser's state and the getopt token, as GetoptLogic.v's reads need.

164Context optarg_cell optind_cell : ptr

164Context Hgetopt_wi : ∀m w h, wim w h → getopt_state_atm libc_getopt_vieww ∧ getopt_optarg_celllibc_getopt_vieww = optarg_cell ∧ getopt_optind_celllibc_getopt_vieww = optind_cell ∧ getopt_currentlibc_getopt_vieww h

wi keeps Hello's option literals in memory.

170Context Htable : ∀m w h, wim w h → hello_table_atm

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.

175Context Hgetopt_env : ∀m w h xs cs, wim w h → agreesm h → live_disjointm → ∀l v, l, v ∈ block_psav ar 0 xs cs ++ flat_maparg_ps sargs → h !! l = Somev → getopt_input_atm hello_inputav sargs → libc_getopt_repinitialized m w ∧ Forallwritable_spanm getopt_rootslibc_getopt_vieww ∧ Forallλs ⇒ readable_bytesm span_ptrs span_sizes getopt_readslibc_getopt_vieww ∧ getopt_separatedhello_inputav sargs libc_getopt_vieww ∧ getopt_disjointgetopt_public_writeshello_inputav sargs libc_getopt_vieww ∧ getopt_private_ownedm hello_inputav sargs libc_getopt_vieww

getopt_long's private roots and libc's cells are apart from the program's objects, and it releases none of them.

187Context Hgetopt_apart : ∀m w h, wim w h → ∀s a, Ins getopt_rootslibc_getopt_vieww ++ getopt_cellslibc_getopt_vieww → span_containss a → ¬owned_liveh m a ∧ ids_apartgetopt_ownedlibc_getopt_vieww h

A return of getopt_long from a memory that agrees with the ghost heap, with its live objects apart and the runtime ready, keeps wi, with argv's block holding what the memory then holds and the token naming the new optarg and optind.

196Context Kgetopt : ∀r args xs s m w h trace values s′ m′ w′ bs cs, M.E.invokelibc_getopt_refined_contracthello_inputav sargs initialized running grequests transition r args xs s m w trace CallReturnvalues s′ m′ w′ → ∀l v, l, v ∈ block_psav ar 0 bs cs → h !! l = Somev → wim w h → agreesm h → live_disjointm → R.readys m → wim′ w′ overwriteblock_psav ar 0 mem_bytesm′ av 8 × lengthsargs + 1 mem_auxesm′ av 8 × lengthsargs + 1 ++ getopt_psgetopt_optarglibc_getopt_vieww′ getopt_optindlibc_getopt_vieww′ h

libc's optarg cell is the global optarg, and both cells are at word addresses.

206Context Hoptarg_g : lookupTAtom"optarg" ge_globalsge = Someoptarg_cell

206Context Hcells : 0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64

libc's optind cell is the global optind.

210Context Hoptind_g : lookupTAtom"optind" ge_globalsge = Someoptind_cell

exit has a contract that admits any canonical status and never returns to main. The handlers it runs, close_stdout among them, are the ending's, not main's: in this language the call stalls.

215Context exit_spec : contractlibc_world

215Context Hexit : registryTAtom"exit" = Someexit_spec

215Context Hexit_abi : ∀v, contract_abiexit_spec CVoid ArgW v

215Context Hexit_pre : ∀n m w h, 0 ≤ n < 2 ^ 32 → wim w h → contract_preexit_spec WIntn m w

215Context Hexit_post : ∀args n s m w tr vs s′ m′ w′, M.E.invokeexit_spec CVoid args WIntn s m w tr CallReturnvs s′ m′ w′ → False

libc's stdout: the world keeps its cell readable and holding the stream, as HelloVersion's footer assumes.

224Context stdout_cell stream : ptr

224Context Hstdout_g : lookupTAtom"stdout" ge_globalsge = Somestdout_cell

224Context wi_stdout : ∀m w h, wim w h → access_resm raw_addressptr_addrstdout_cell 0 ptr_capstdout_cell 8 Read 8 = Someok ∧ pointer_load_effectsm raw_addressptr_addrstdout_cell 0 AuxRead; LowerResolve; AddressRead = Somestream

version_etc's premises, as HelloVersion's version_etc_spec takes them: the literal pieces main owns, the authors' lives among them, the six output contracts and the frame of its allocations, stores and snapshot.

235Context version_ps : listpiece × pval

235Context author_reg : String.string → region

235Context Hauthor_live : ∀s, Ins "hello#str.72"; "hello#str.73"; "hello#str.74"; "hello#str.75" → PLiveptr_addrversion_literals, VLiveauthor_regs ∈ version_ps

235Context version_spec : name → contractlibc_world

235Context Hversion_reg : ∀g xs, Ing, xs version_output_argsstream → registryg = Someversion_specg

235Context Hversion_ret : ∀g xs, Ing, xs version_output_argsstream → contract_returnsversion_specg = RClassW

235Context Hversion_abi : ∀g xs d args, Ing, xs version_output_argsstream → mapλa ⇒ match a with Argk _ ⇒ k end args = version_output_classesxs → contract_abiversion_specg CResultd W args

235Context Hversion_pre : ∀g xs m w h, Ing, xs version_output_argsstream → ∀l v, l, v ∈ version_ps → h !! l = Somev → agreesm h → wim w h → contract_preversion_specg xs m w

235Context Hversion_frame : ∀g xs r args s m w h trace values s′ m′ w′, Ing, xs version_output_argsstream → agreesm h → live_disjointm → R.readys m → wim w h → M.E.invokeversion_specg r args xs s m w trace CallReturnvalues s′ m′ w′ → agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h ∧ ∃n, values = WIntn ∧ 0 ≤ n < 2 ^ 32

235Context Kversion_alloc : ∀size m wd h base, Insize 24; 80 → freshm heap_req8 size base → wim wd h → wiallocatedm heap_req8 size base wd overwriteobj_psbase heap_req8 size h

235Context Kversion_store : ∀b reg o x xp m wd h, ∀k v, k, v ∈ PLiveb, VLivereg ++ PAuxb o, VAuxptr_capx :: cellb o ptr_addrx → h !! k = Somev → wim wd h → wistore_bytesstore_auxm b + o ptr_capxp b + o 8 ptr_addrxp wd overwritePLiveb, VLivereg ++ PAuxb o, VAuxptr_capxp :: cellb o ptr_addrxp h

235Context Kversion_cursor : ∀cb cr sb off m wd h, ∀k v, k, v ∈ va_cursor_pscb cr mkPtrsb + off Rosb → h !! k = Somev → wim wd h → wistore_bytesm cb 8 sb + off + 8 wd overwriteva_cursor_pscb cr mkPtrsb + off + 8 Rosb h

235Context Kversion_snapshot : ∀m wd h sb, freshm heap_req16 72 sb → wim wd h → wisnapshot_valuesHV.version_main_argsstream sb allocatedm heap_req16 72 sb wd overwritesnapshot_psHV.version_main_argsstream sb heap_req16 72 h

libc's stderr: the world keeps its cell readable and holding the stream, as for stdout.

276Context stderr_cell errstream : ptr

276Context Hstderr_g : lookupTAtom"stderr" ge_globalsge = Somestderr_cell

276Context wi_stderr : ∀m w h, wim w h → access_resm raw_addressptr_addrstderr_cell 0 ptr_capstderr_cell 8 Read 8 = Someok ∧ pointer_load_effectsm raw_addressptr_addrstderr_cell 0 AuxRead; LowerResolve; AddressRead = Someerrstream

The output contracts of main's own calls and of the footer, as HelloVersion states the footer's: each is admitted with the literals' pieces (and, for a line naming the program, the arguments' strings, one of which holds its name), returns a canonical int and keeps the world interpretation, whether its output succeeded or not.

289Context help_ps : listpiece × pval

289Context output_spec : name → contractlibc_world

289Context Hhelp_reg : ∀pname g xs, Ing, xs main_output_argsstream errstream pname → registryg = Someoutput_specg

289Context Hhelp_ret : ∀pname g xs, Ing, xs main_output_argsstream errstream pname → contract_returnsoutput_specg = RClassW

289Context Hhelp_abi : ∀pname g xs d args, Ing, xs main_output_argsstream errstream pname → mapλa ⇒ match a with Argk _ ⇒ k end args = replicatelengthxs P → contract_abioutput_specg CResultd W args

289Context Hhelp_pre : ∀pname g xs m w h, name_oksargs pname → Ing, xs main_output_argsstream errstream pname → ∀l v, l, v ∈ help_ps ++ flat_maparg_ps sargs → h !! l = Somev → agreesm h → wim w h → contract_preoutput_specg xs m w

289Context Hhelp_frame : ∀pname g xs r args s m w h trace values s′ m′ w′, Ing, xs main_output_argsstream errstream pname → agreesm h → live_disjointm → R.readys m → wim w h → M.E.invokeoutput_specg r args xs s m w trace CallReturnvalues s′ m′ w′ → agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h ∧ ∃n, values = WIntn ∧ 0 ≤ n < 2 ^ 32

289Context Houtput_reg : ∀g xs, Ing, xs emit_output_argsstream → registryg = Someoutput_specg

289Context Houtput_ret : ∀g xs, Ing, xs emit_output_argsstream → contract_returnsoutput_specg = RClassW

289Context Houtput_abi : ∀g xs d args, Ing, xs emit_output_argsstream → mapλa ⇒ match a with Argk _ ⇒ k end args = replicatelengthxs P → contract_abioutput_specg CResultd W args

289Context Houtput_pre : ∀g xs m w h, Ing, xs emit_output_argsstream → ∀l v, l, v ∈ help_ps → h !! l = Somev → agreesm h → wim w h → contract_preoutput_specg xs m w

289Context Houtput_frame : ∀g xs r args s m w h trace values s′ m′ w′, Ing, xs emit_output_argsstream → agreesm h → live_disjointm → R.readys m → wim w h → M.E.invokeoutput_specg r args xs s m w trace CallReturnvalues s′ m′ w′ → agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h ∧ ∃n, values = WIntn ∧ 0 ≤ n < 2 ^ 32

error(0, 0, fmt, text, arg), the diagnostic for an extra operand, has a contract that returns: admitted with the literals' and the arguments' pieces for an argument's string, it keeps the world interpretation and every piece main owns.

326Context diag_spec : contractlibc_world

326Context Hdiag_reg : registryTAtom"error" = Somediag_spec

326Context Hdiag_ret : contract_returnsdiag_spec = RVoid

326Context Hdiag_abi : ∀args, mapλa ⇒ match a with Argk _ ⇒ k end args = W; W; P; P; P → contract_abidiag_spec CVoid args

326Context Hdiag_pre : ∀q m w h, Inq maparg_ptr sargs → ∀l v, l, v ∈ help_ps ++ flat_maparg_ps sargs → h !! l = Somev → agreesm h → wim w h → contract_prediag_spec WInt0; WInt0; WPtrversion_literal"hello#str.77"; WPtrversion_literal"hello#str.78"; WPtrq m w

326Context Hdiag_post : ∀q args s m w h tr vs s′ m′ w′, Inq maparg_ptr sargs → agreesm h → live_disjointm → R.readys m → wim w h → M.E.invokediag_spec CVoid args WInt0; WInt0; WPtrversion_literal"hello#str.77"; WPtrversion_literal"hello#str.78"; WPtrq s m w tr CallReturnvs s′ m′ w′ → vs = [ ] ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h

mbrtowc has Campaign 4's contract, whose state predicate valid admits the zero state and holds only of bytes.

345Context valid : term → listZ → Prop

345Context audit : term → optionaudited_codec

345Context Hmbrtowc : registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests

345Context Hvalid0 : mbstate_zero_validvalid

345Context Hbytes : mbstate_valid_bytesvalid

The world interpretation makes libc ready, with the errno cell errno, keeps the codec piece current (codec_current) and libc's private state apart. A conversion learns the codec from the codec piece, which setlocale's setter set (wp_setlocale_set).

353Context errno : ptr

353Context Hlibc : ∀m w h, wim w h → libc_readyrep m w ∧ codec_currentlibc_localefstw h ∧ libc_errnofstw = errno ∧ libc_privatem w h

The audited codec premise: the world's codec is one of the audited profiles, C or C.UTF-8.

360Context Haudit : ∀m w h, wim w h → hello_codec_profileaudit w

The world interpretation survives a return of mbrtowc into the output, state and errno blocks the program owns, holding whatever the memory holds there afterwards.

365Context Kmbrtowc : ∀r args out src n state s m w h trace values s′ m′ w′ bo ro oo xo co bs rs os ys cs be re oe xe ce, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l v, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h

setlocale's query of a category whose name is lent, by a pointer whose address is null, as hard_locale and main's --help make it: admitted, it returns that name and changes nothing (LocaleLogic's locale_wi_pre and locale_wi_query, for libc's world).

380Context Hset_query_pre : ∀m w h k p t z, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → contract_prelibc_setlocale_contractrep requests WIntk; WPtrz m w

380Context Hset_query : ∀r args s m w h k p t z trace ending s′ m′ w′, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokelibc_setlocale_contractrep requests r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp

strlen, memcpy and strcmp have their contracts.

388Context Hstrlen : registryTAtom"strlen" = Somestrlen_contractlibc_world

388Context Hmemcpy : registryTAtom"memcpy" = Somememcpy_contractlibc_world

388Context Hstrcmp : registryTAtom"strcmp" = Somestrcmp_contractlibc_world

The world interpretation survives a copy, a byte store and a four-byte store into a block the program owns.

394Context Kcopy : ∀b reg o xs cs s n m m′ wd h ys, copy_resultm mkPtrb + o Objb s n m′ → ∀l v, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h

394Context Kbyte : ∀b reg o x y m wd h, ∀l v, l, v ∈ PLiveb, VLivereg; PByteb o, VBytex → h !! l = Somev → wim wd h → wistore_bytesm b + o 1 y wd overwritePLiveb, VLivereg; PByteb o, VBytey mod 256 h

394Context Kstore : ∀b reg o xs y m wd h, ∀l v, l, v ∈ PLiveb, VLivereg :: byte_psb o xs → h !! l = Somev → wim wd h → wistore_bytesm b + o 4 y wd overwritePLiveb, VLivereg :: byte_psb o le_bytesy 4 h

The memchr contract, for strnlen1.

408Context Hmemchr : registryTAtom"memchr" = Somememchr_contractlibc_world

errno's lookup has Campaign 4's contract.

411Context Herrno_reg : registryTAtom"__errno_location" = SomeHC.LB.errno_contractrep

malloc has its contract.

414Context Hmalloc : registryTAtom"malloc" = Somemalloc_contractlibc_world

The errno cell is at offset eo of an object eb that main owns, in the address space.

418Context eb eo : Z

418Context er : region

418Context Herrno_at : errno = mkPtreb + eo Objeb

418Context Herrno_range : 0 < eb ∧ 0 ≤ eo ∧ eb + eo + 4 ≤ r_ender ∧ r_ender ≤ 2 ^ 48

The greeting's literals: the format of the failed conversion's diagnostic and the wide format of the greeting's line. Main owns their pieces, join_ps.

424Context join_ps : listpiece × pval

424Context Hjoin_lookup : ∀s, Ins "hello#str.82"; "hello#str.83" → lookupTAtoms ge_globalsge = Someversion_literals

error(1, errno, fmt), the diagnostic of a failed conversion, has the same contract as main's extra-operand diagnostic, error being one function: it is admitted with the literals' pieces and never returns, as its status is nonzero.

432Context Herror_abi : ∀args, mapλa ⇒ match a with Argk _ ⇒ k end args = W; W; P → contract_abidiag_spec CVoid args

432Context Herror_pre : ∀n m w h, wim w h → ∀l v, l, v ∈ join_ps → h !! l = Somev → agreesm h → contract_prediag_spec WInt1; WIntn; WPtrversion_literal"hello#str.82" m w

432Context Herror_fatal : ∀n args s m w tr vs s′ m′ w′, M.E.invokediag_spec CVoid args WInt1; WIntn; WPtrversion_literal"hello#str.82" s m w tr CallReturnvs s′ m′ w′ → False

errno's lookup returns the errno cell, whose bytes main owns.

441Context Herrno_cell : ∀m w h, wim w h → errno_cellm errno

wprintf(fmt, buffer) is admitted where main owns the literals and a buffer holding a terminated wide string, returns a canonical int and keeps the world interpretation, whether its output succeeded or not.

447Context wprintf_spec : contractlibc_world

447Context Hwprintf_reg : registryTAtom"wprintf" = Somewprintf_spec

447Context Hwprintf_ret : contract_returnswprintf_spec = RClassW

447Context Hwprintf_abi : ∀d args, mapλa ⇒ match a with Argk _ ⇒ k end args = P; P → contract_abiwprintf_spec CResultd W args

447Context Hwprintf_pre : ∀bd rd ws k m w h, wide_oktake4 × k ws → le_valuetake4 drop4 × k ws = 0 → 4 × k + 4 ≤ lengthws%nat → ∀l v, l, v ∈ join_ps ++ PLivebd, VLiverd :: byte_psbd 0 ws → h !! l = Somev → agreesm h → wim w h → contract_prewprintf_spec WPtrversion_literal"hello#str.83"; WPtrmkPtrbd Objbd m w

447Context Hwprintf_frame : ∀bd r args s m w h tr values s′ m′ w′, agreesm h → live_disjointm → R.readys m → wim w h → M.E.invokewprintf_spec r args WPtrversion_literal"hello#str.83"; WPtrmkPtrbd Objbd s m w tr CallReturnvalues s′ m′ w′ → agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h ∧ ∃n, values = WIntn ∧ 0 ≤ n < 2 ^ 32

free releases a heap object main owns, keeping the world interpretation.

465Context Hfree : frees_heapge_freege

465Context Kfree : ∀b reg m wd h rs, h !! PLiveb = SomeVLivereg → replace_regionb mkRegionb b Heap Freed m_regionsm = Somers → wim wd h → wimkMemm_bytesm rs m_auxm wd overwritePLiveb, VFreed h

The Iris proofs, under any invariant and ghost heap instance.

471Section iris

472Context `{!invGS_genhlc Σ, !gen_heapGSpiece pval Σ}

The Iris instance of the registry and wi.

475Instance join_irisGS: irisGS_genhlc nanofil_langregistry ge Σ ≔

nanofil_irisGSregistry wi ge

The expressions of the language.

479Notation jexpr ≔ language.exprnanofil_langregistry ge

Enter a block of a function f, read from the linked module.

482Ltac jn_enter blk ≔

iApply wp_enter_ _ _ _ _ _ _ _ blk ; vm_compute ; reflexivity | word_premise | ; iNext ; cbn [ b_insts b_jump main_block xmalloc_block hblk ]

xmalloc(n): malloc's contract has no null return, as running out of memory is a resource ending, so xmalloc's call of xalloc_die, and the abort behind it, is never reached: xmalloc returns a fresh heap object of n bytes.

491Lemma xmalloc_spec

∀ n Φ

0 ≤ n < 2 ^ 64

▷∀base, ⌜0 < base ∧ base mod 16 = 0 ∧ base + req_extentheap_req16 n ≤ 2 ^ 48⌝ −∗ objbase heap_req16 n −∗ ΦRetWPtrmkPtrbase Objbase −∗ WPERuninvocationxmalloc_fn WIntn : jexpr {Φ}

Proof 31 steps Qed

intros Hn

iIntros HK

change invocationxmalloc_fn WIntn with mkFramexmalloc_fn TAtom"v0", WIntn [ ] None EnterTAtom"start" None

jn_enter xmalloc_block"start"

iNext

iIntros base Hb₀ & Hb₁₆ & Hbend & _ Hobj

gen_env

iApply wp_let ; reflexivity | reflexivity | word_premise | intros ?m ; word_premise |

iNext

gen_env

iApply wp_let ; reflexivity | reflexivity | word_premise | intros ?m ; word_premise |

iNext

gen_env

The base is not null: on to the join, not to xalloc_die.

assert Hq : 0 ≤ req_extentheap_req16 n

{cbn

apply Z.mul_nonneg_nonneg ; apply Z.div_pos | ; lia

assert Eb : base mod 2 ^ 64 =? 0 mod 2 ^ 64 = false

{apply Z.eqb_neq

rewrite Zmod_0_l

rewrite Z.mod_smallbase ; lia

cbn [ ptr_addr ]

rewrite Eb

iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |

iNext

cbn [ Z.eqb edge_label ]

jn_enter xmalloc_block"iw_1.join"

iApply wp_ret ; reflexivity | reflexivity |

iNext

iApply HK with [%] Hobj

auto

One argument's string out of all of them, and back.

522Lemma arg_string_split

∀ args s

Ins args

string_okarg_ptrs arg_bases arg_regions arg_texts

ptsflat_maparg_ps args −∗ stringarg_ptrs arg_bases arg_regions arg_texts ∗ stringarg_ptrs arg_bases arg_regions arg_texts −∗ ptsflat_maparg_ps args

Proof 9 steps Qed

intros Hin Hok

destruct in_split_ _ Hin as l₁ & l₂ & →

rewrite flat_map_app

cbn [ flat_map ]

rewrite ! pts_app

iIntros (H₁ & Hs & H₂)

iSplitL Hs ; iSplit ; iPureIntro ; exact Hok | iExact Hs |

iIntros [_ Hs]

iFrame

The greeting b4's cell holds in the loop is a string main owns: the default literal, the traditional one, or a suffix of an argument that getopt lent as optarg. It is given back after use.

537Lemma greeting_string

∀ g rg rt

HM.greeting_okav sargs g

ptsflat_maparg_ps sargs −∗ stringgreeting_ptr 70000 rg greeting_bytes −∗ stringtraditional_ptr 69808 rt traditional_bytes −∗ ∃b reg bs, stringg b reg bs ∗ stringg b reg bs −∗ ptsflat_maparg_ps sargs ∗ stringgreeting_ptr 70000 rg greeting_bytes ∗ stringtraditional_ptr 69808 rt traditional_bytes

Proof 23 steps Qed

intros → | → | q & text & off & Hin & Hoff & → _ ; iIntros Ha Hg Ht

–iExists _, _, _

iFrame Hg

iIntros Hg

iFrame

–iExists _, _, _

iFrame Ht

iIntros Ht

iFrame

–cbn [ hello_input getopt_arguments ] in Hin

apply in_map_iff in Hin as s & E & Hs

injection E as ← ←

pose proof proj1List.Forall_forall_ _ Hargs s Hs as Hok

iDestruct arg_string_splitsargs s Hs Hok with Ha as [Hs Hback]

iDestruct string_suffix_ _ _ _ Z.to_natoff with Hs as [Hsuf Hsback] ; lia |

rewrite Z2Nat.id ; | lia

iExists _, _, _

iFrame Hsuf

iIntros Hsuf

iFrame Hg Ht

iApply Hback

iApply Hsback

iExact Hsuf

A heap request's extent covers its size.

559Lemma heap_req_covers

∀ n

0 ≤ n

n ≤ req_extentheap_req16 n

Proof 5 steps Qed

intros Hn

cbn

pose proof Z.div_modn + 15 16 ltac:lia

pose proof Z.mod_pos_boundn + 15 16 ltac:lia

lia

iw_1.join, the greeting: entered with pr.2 clear and optind at argc, main loads the greeting from b4's cell, measures it, allocates a buffer of that many wide characters and the NUL, and converts the greeting into it.

569Lemma main_join

∀ b₄ b₆ new : Z → ptr × listZ c′ rg rt rc rp xe ce Φ

HM.fresh_okb₆

lengthxe = 4%nat

lengthce = 4%nat

∗_{k∈locale_categories}LL.lentk newk.1 newk.2 −∗ ptscodec_psc′ −∗ liveb₆ mkRegionb₆ b₆ + 16 Heap Live −∗ bytesb₆ 0 replicate8 0 −∗ auxesb₆ 0 clear_slots0 replicate8 CNone −∗ stringc_ptr 65824 rc c_bytes −∗ stringposix_ptr 65856 rp posix_bytes −∗ ptsblock_pseb er eo xe ce −∗ ptsjoin_ps −∗ stringgreeting_ptr 70000 rg greeting_bytes −∗ stringtraditional_ptr 69808 rt traditional_bytes −∗ HM.operand_exitregistry wi ge av ar sargs b₄ b₆ "iw_1.join"%string "iw_1.L60"%string λlose i ⇒ lose = 0 ∧ i = Z.of_natlengthsargs Φ

Proof 156 steps Qed

intros Hb₆₀ & Hb₆₁₆ & Hb₆₄₈ Lxe Lce

iIntros #Hlent Hcod Hl₆ Hy₆ Hc₆ Hcs Hps Herr Hjs Hgr Htr

rewrite / HM.operand_exit

iIntros e ps cs a i g lose Hf & Hpr & Hlose & Hi (Hb & Has & Ht & Hl₄ & Hp₄)

pose proof Hf as H₀ & H₂ & H₄ & H₆ & H₁₁ & Hc₁ & Hb₄₀ & Hb₄₁₆ & Hb₄₄₈ & Ho & Hc & Hix & Hg

iDestruct greeting_stringg rg rt Hg with Has Hgr Htr as gb greg gbs [Hgs Hgback]

iDestruct Hgs as [%Hgok Hgps]

pose proof Hgok as Hgcap & Hgb₀ & Hgbp & Hgend & Hg₄₈ & Hgf

jn_enter main_block"iw_1.join"

The greeting, from b4's cell.

iNext

iIntros Hl₄

gen_env

{intros xb Hxb

exists greg

assert xb = gb as →

{destruct Hgcap as E₁ | E₁ ; rewrite E1 in Hxb ; destruct Hxb as E₂ | E₂ ; congruence

unfold string_ps

left

iNext

iIntros Hl₄ Hp₄ Hgps

gen_env

Its length, and the buffer's: four bytes per character and the NUL.

iNext

iIntros Hgs

gen_env

iApply wp_let ; reflexivity | reflexivity | word_premise | intros ?m ; word_premise |

iNext

gen_env

iApply wp_let ; reflexivity | reflexivity | word_premise | intros ?m ; word_premise |

iNext

gen_env

set len := Z.of_natlengthgbs in *

assert Hlen : 0 ≤ len ∧ len + 1 < 2 ^ 48 by unfold len ; lia

assert E₂₂ : len + 1 × 2 ^ 2 mod 64 mod 2 ^ 64 = 4 × len + 1

{change 2 ^ 2 mod 64 with 4

rewrite Z.mod_small ; lia

match goal withH : lookupTAtom"v22" _ = _ |- _⇒rewrite E22 in Hend

xmalloc(4 * (len + 1)).

iApply wp_call_bind_ _ _ _ _ _ _ _ _ _ _ _ _ xmalloc_fn invocationxmalloc_fn WInt4 × len + 1 ; word_premise | unfold find_fn ; rewrite proj1Hlinked ; vm_compute ; reflexivity | reflexivity |

iNext

iApply xmalloc_spec ; lia |

iNext

iIntros bd Hbd₀ & Hbd₁₆ & Hbdend Hobj

iExists _

iSplit ; iPureIntro ; reflexivity |

iNext

cbn [ fr_fn fr_env fr_locals fr_doomed fr_at ]

gen_env

The buffer: its first 4 * (len + 1) bytes and slots.

pose proof heap_req_covers4 × len + 1 ltac:lia as Hcov

iEval rewrite obj_zero_blockbd _ ; | lia in Hobj

iDestruct Hobj as (Hbdl & Hbdw & Hbda)

iEval rewrite bytes_take_drop_ _ _ Z.to_nat4 × len + 1 ; | rewrite length_replicate ; lia in Hbdw

iEval rewrite auxes_take_drop_ _ _ Z.to_nat4 × len + 1 ; | rewrite length_replicate ; lia in Hbda

iDestruct Hbdw as [Hbdw _]

iDestruct Hbda as [Hbda _]

rpl_mbsrtowcs(buffer, b4's cell, len + 1, b6's state).

iDestruct big_sepL_elem_of_ _ 0 with Hlent as Hk₀ ; apply list_elem_of_In ; unfold locale_categories ; cbn ; left ; reflexivity |

iEval rewrite / codec_ps in Hcod

iEval rewrite / pts in Hcod

iEval rewritebig_sepL_singleton in Hcod

iAssert ptsblock_psb6 mkRegionb6 b6 + 16 Heap Live 0 replicate8 0 clear_slots0 replicate8 CNone with [Hl₆ Hy₆ Hc₆] as Hst

{rewrite block_pts

iFrame

iApply wp_call_bind_ _ _ _ _ _ _ _ _ _ _ _ _ mbs_fn invocationmbs_fn WPtrmkPtrbd Objbd; WPtrmkPtrb4 + 0 Objb4; WIntlen + 1; WPtrmkPtrb6 + 0 Objb6 ; word_premise | unfold find_fn ; rewrite proj1Hlinked ; vm_compute ; reflexivity | rewrite ! Z.add_0_r ; reflexivity |

iNext

iApply HC.rpl_mbsrtowcs_specregistry wi ge valid audit rep requests Hmbrtowc Hvalid0 Hbytes errno Hlibc Haudit Kmbrtowc Hlinked Hlent libc_setlocale_contractrep requests Hsetlocale setlocale_returnsrep requests setlocale_query_abirep requests Hset_query_pre Hset_query Hstrlen Hmemcpy Hstrcmp Kcopy Kbyte Kstore Kalloc Hmemchr Herrno_reg Kpstore g gb greg gbs bd _ _ _ b6 _ 0 _ _ eb er eo xe ce b4 _ 0 c' DfracOwn1 new0.1 new0.2 rc rp with Hk₀ Hcs Hps Hcod Hgs Hbdl Hbdw Hbda Hst Herr Hl₄ Hp₄

iIntros r ws′ cws′ ys′ cs′ xe′ ce′ x′ Hpost & Lws′ & Lxe′ Hcs Hps Hcod Hgs Hbdl Hbdw Hbda Hst Herr Hl₄ Hp₄

iExists _

iSplit ; iPureIntro ; reflexivity |

iNext

cbn [ fr_fn fr_env fr_locals fr_doomed fr_at ]

gen_env

iApply wp_let ; reflexivity | reflexivity | word_premise | intros ?m ; word_premise |

iNext

gen_env

pose proof Hjoin_lookup"hello#str.82" or_introleq_refl as H₈₂

pose proof Hjoin_lookup"hello#str.83" or_introror_introleq_refl as H₈₃

destruct Hpost as → Hxe | k & → & Hk & Hwide & Hnul

The conversion failed: error(1, errno, ...), which never returns.

–iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |

iNext

cbn [ Z.eqb edge_label ]

jn_enter main_block"L34"

iApply HCl.wp_close_errnoregistry wi ge eb eo λw ⇒ libc_errnofstw libc_readyrep Herrno_reg Hlinked ; intros m w h Hw ; rewrite <- Herrno_at ; exact proj1proj2proj2Hlibc_ _ _ Hw | intros m w h Hw ; split ; exact proj1Hlibc_ _ _ Hw | ; rewrite proj1proj2proj2Hlibc_ _ _ Hw ; exact Herrno_cell_ _ _ Hw |

iNext

gen_env

iEval rewriteblock_pts in Herr

iDestruct Herr as (Hel & Hew & Hea)

iNext

iIntros Hel

gen_env

iApply HCl.wp_close_load_wregistry wi ge with Hel Hew ; word_premise | lia | exact Lxe' |

iNext

iIntros Hel Hew

gen_env

iApply wp_let ; reflexivity | reflexivity | cbn ; rewrite H82 ; reflexivity | intros ?m ; word_premise |

iNext

gen_env

iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ diag_spec WInt1; WIntclose_wxe'; WPtrversion_literal"hello#str.82" ptsjoin_ps with Hjs [];|apply linked_outside ; first exact Hlinked | reflexivity|apply linked_unbound ; first exact Hlinked | reflexivity|reflexivity|exact Hdiag_reg|cbn;match goal withH : lookupTAtom"v38" _ = _ |- _⇒rewrite Hend;match goal withH : lookupTAtom"v39" _ = _ |- _⇒rewrite Hend;cbn;rewrite Z.mod_smallclose_wxe';|reflexivity|apply close_w_range|apply Herror_abi ; reflexivity||

+iIntros σ (%h & Hh & %Hσ) Hjs

destruct Hσ as Ha & _ & _ & Hw

iDestruct pts_lookup with Hh Hjs as %Hl

iPureIntro

exact Herror_pre_ _ _ _ Hw Hl Ha

+iNext

iIntros σ tr vs s′ m′ w′ Hinv _ _

exfalso

exact Herror_fatal_ _ _ _ _ _ _ _ _ _ Hinv

The conversion succeeded: wprintf, free, exit(0).

–assert Hk₄₈ : Z.of_natk < 2 ^ 48 by unfold len in Hlen ; lia

iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0;|cbn;match goal withH : lookupTAtom"v33" _ = _ |- _⇒rewrite Hend;rewrite Z.mod_smallZ.of_natk;||lia;rewrite proj2Z.eqb_neq_ _;|reflexivity|lia|

iNext

cbn [ Z.eqb edge_label ]

jn_enter main_block"L29"

iApply wp_let ; reflexivity | reflexivity | cbn ; rewrite H83 ; reflexivity | intros ?m ; word_premise |

iNext

gen_env

iAssert ptsjoin_ps ++ PLivebd, VLivemkRegionbd bd + req_extentheap_req16 4 × len + 1 req_kindheap_req16 4 × len + 1 Live ++ byte_psbd 0 ws' with [Hjs Hbdl Hbdw] as Hwp

{rewrite ! pts_app

iFrame Hjs

rewrite / live / bytes

iFrame

iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ wprintf_spec WPtrversion_literal"hello#str.83"; WPtrmkPtrbd Objbd _ with Hwp [Herr Hgs Hgback Hbda Hcs Hps Hcod Hst Hl₄ Hp₄];|apply linked_outside ; first exact Hlinked | reflexivity|apply linked_unbound ; first exact Hlinked | reflexivity|reflexivity|exact Hwprintf_reg|cbn;match goal withH : lookupTAtom"v56" _ = _ |- _⇒rewrite Hend;match goal withH : lookupTAtom"v23" _ = _ |- _⇒rewrite Hend;reflexivity|apply Hwprintf_abi ; reflexivity||

+iIntros σ (%h & Hh & %Hσ) Hwp

destruct Hσ as Ha & _ & _ & Hw

iDestruct pts_lookup with Hh Hwp as %Hl

iPureIntro

eapply Hwprintf_pre_ _ _ k _ _ h Hwide Hnul ; unfold len in Lws' ; lia | exact Hl | exact Ha | exact Hw

+iNext

iIntros σ trace values s′ m′ w′ Hinv (%h & Hh & %Hσ) Hwp

destruct Hσ as Ha & Hd & Hr & Hw

destruct Hwprintf_frame_ _ _ _ _ _ _ _ _ _ _ _ Ha Hd Hr Hw Hinv as Ha′ & Hd′ & Hr′ & Hw′ & n & → & Hn

iModIntro

iExists putTAtom"v58" WIntn _

iSplit

{iPureIntro

unfold external_env

cbn [ site_result ]

rewrite Hwprintf_ret

cbn

rewrite Z.mod_small ; reflexivity | exact Hn

iSplitL Hh ; iExists h ; iFrame ; iPureIntro ; auto |

rewrite ! pts_app

iDestruct Hwp as (Hjs & Hbdl & Hbdw)

gen_env

iNext

∗iIntros σ′ (%h′ & _ & %Hσ′) _

destruct Hσ' as _ & _ & _ & Hw′′

iPureIntro

exact Hexit_pre0 _ _ h' ltac:lia Hw''

∗iNext

iIntros σ′ tr vs s′′ m′′ w′′ Hinv′ _ _

exfalso

exact Hexit_post_ _ _ _ _ _ _ _ _ _ Hinv'

Main, every path: from its entry through the loop (HelloMain's main_to_join) to the greeting (main_join), owning what both need. Every path ends in a call that does not return, exit or a fatal error, or loops for good; none reaches abort.

737Lemma main_full

∀ s₀ srest r₃ r₄ x₀ x₁ y₀ old c₀ r₈₀ cs₀ a ix b₆₁ r₆₁ rg rt rc rp xe ce Φ

sargs = s₀ :: srest

argv_capscs₀ maparg_ptr sargs

0 ≤ ix ≤ Z.of_natlengthsargs

lengthxe = 4%nat

lengthce = 4%nat

ptsblock_psav ar 0 argv_bytesmaparg_ptr sargs cs₀ −∗ ptsflat_maparg_ps sargs −∗ ptsgetopt_psa ix −∗ HP.HN.literalsr₃ r₄ −∗ HP.HN.name_cellspn nreg sreg nb sb x₀ x₁ y₀ −∗ ∗_{k∈locale_categories}LL.namedk oldk.1 oldk.2 −∗ ptscodec_psc₀ −∗ stringempty_ptr 69968 r₈₀ [ ] −∗ ptsversion_ps −∗ ptshelp_ps −∗ stringversion_literal"hello#str.61" b₆₁ r₆₁ 101; 110; 95 −∗ stringc_ptr 65824 rc c_bytes −∗ stringposix_ptr 65856 rp posix_bytes −∗ ptsblock_pseb er eo xe ce −∗ ptsjoin_ps −∗ stringgreeting_ptr 70000 rg greeting_bytes −∗ stringtraditional_ptr 69808 rt traditional_bytes −∗ WPERuninvocationmain_fn WIntZ.of_natlengthsargs; WPtrmkPtrav Objav : jexpr {Φ}

Proof 10 steps Qed

intros Hhd Hcs Hix Lxe Lce

iIntros Hb Has Ht Hlit Hcells Hks Hcod Hs₈₀ Hv Hh H₆₁ Hc Hp Herr Hjs Hgr Htr

iApply HM.main_to_join with Hb Has Ht Hlit Hcells Hks Hcod Hs₈₀ Hv Hh H₆₁

all: try eassumption

--help's query of LC_MESSAGES, from the general query premise.

1: intros ?m ?w ?h ?p ?t Hw Hk ; eapply Hset_query_pre ; exact Hw | exact Hk | reflexivity

1: intros ?r ?args ?s ?m ?w ?h ?p ?t ?tr ?en ?s′ ?m′ ?w′ Hw Hk Hi ; eapply Hset_query_ _ _ _ _ _ _ _ _ null ; exact Hw | exact Hk | reflexivity | exact Hi

iNext

iIntros e b₄ b₆ i k q new c′ Hf Hlit #Hl Hcod Hs₈₀ Hy₄ Hc₄ Hl₆ Hy₆ Hy₆′ Hc₆ Hc₆′

pose proof Hf as _ & _ & _ & Hb₆ & _

iApply main_joinb4 b6 new c' rg rt rc rp xe ce Φ Hb6 Lxe Lce with Hl Hcod Hl₆ Hy₆ Hc₆ Hc Hp Herr Hjs Hgr Htr

GNU Hello's main never fails: from a memory m, runtime state s and world w where R is ready, the live objects are apart, and an initial ghost heap h0 that agrees with m, satisfies wi with w and holds the pieces main_full needs, no labelled run of main, at any fuel, stops with a failure_ending: no panic, no stuck step, no contract violation, and so no abort. By heap_labelled_safe from main_full. The premises are the section's, the audited codec premise Haudit among them.

775Theorem hello_main_safe

∀ Σ HinvP : invGpreSΣ HheapP : gen_heapGpreSpiece pval Σ m s w h₀ s₀ srest r₃ r₄ x₀ x₁ y₀ old c₀ r₈₀ cs₀ a ix b₆₁ r₆₁ rg rt rc rp xe ce fuel

R.readys m

live_disjointm

agreesm h₀

wim w h₀

sargs = s₀ :: srest

argv_capscs₀ maparg_ptr sargs

0 ≤ ix ≤ Z.of_natlengthsargs

lengthxe = 4%nat

lengthce = 4%nat

∀HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ, ∗_l↦v∈h₀pointstol DfracOwn1 v ⊢ ptsblock_psav ar 0 argv_bytesmaparg_ptr sargs cs₀ ∗ ptsflat_maparg_ps sargs ∗ ptsgetopt_psa ix ∗ HP.HN.literalsr₃ r₄ ∗ HP.HN.name_cellspn nreg sreg nb sb x₀ x₁ y₀ ∗ ∗_{k∈locale_categories}LL.namedk oldk.1 oldk.2 ∗ ptscodec_psc₀ ∗ stringempty_ptr 69968 r₈₀ [ ] ∗ ptsversion_ps ∗ ptshelp_ps ∗ stringversion_literal"hello#str.61" b₆₁ r₆₁ 101; 110; 95 ∗ stringc_ptr 65824 rc c_bytes ∗ stringposix_ptr 65856 rp posix_bytes ∗ ptsblock_pseb er eo xe ce ∗ ptsjoin_ps ∗ stringgreeting_ptr 70000 rg greeting_bytes ∗ stringtraditional_ptr 69808 rt traditional_bytes

labelled_saferegistry ge invocationmain_fn WIntZ.of_natlengthsargs; WPtrmkPtrav Objav m s w fuel λ_ ⇒ True

Proof 6 steps Qed

intros Hr Hd Ha Hw Hhd Hcs Hix Lxe Lce Hstart

apply heap_labelled_safeΣ registry wi ge _ m s w h0 λ_ ⇒ True Hr Hd Ha Hw

intros HinvG HheapG

rewrite HstartHinvG HheapG

iIntros (Hb & Has & Ht & Hlit & Hcells & Hks & Hcod & Hs₈₀ & Hv & Hh & H₆₁ & Hc & Hp & Herr & Hjs & Hgr & Htr)

iApply main_fulls0 srest r3 r4 x0 x1 y0 old c0 r80 cs0 a ix b61 r61 rg rt rc rp xe ce with Hb Has Ht Hlit Hcells Hks Hcod Hs₈₀ Hv Hh H₆₁ Hc Hp Herr Hjs Hgr Htr ; auto