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.
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 HelloConv HelloName HelloProgName
Open Scope Z_scope
Open Scope list_scope
Main's function, read from the linked module.
A block of main.
A 16-aligned base is 8-aligned.
∀ b
b mod 16 = 0
b mod 8 = 0
Explore proof 6 tactics
Initial goal
b :
Z
⊢
b mod 16 = 0 → b mod 8 = 0
intros H
b :
Z
H :
b mod 16 = 0
⊢
b mod 8 = 0
apply Z.mod_divide in H ; | lia
b :
Z
H :
16 b
⊢
b mod 8 = 0
destruct H as k →
k :
Z
⊢
k × 16 mod 8 = 0
replace k × 16 with 2 × k × 8 by lia
k :
Z
⊢
2 × k × 8 mod 8 = 0
apply Z.mod_mul
k :
Z
⊢
8 ≠ 0
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
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
The literals main copies: "" for setlocale, the default greeting, read-only, and close_stdout's function pointer.
"Hello, world!".
Its bytes.
72; 101; 108; 108; 111; 44; 32; 119; 111; 114; 108; 100; 33
close_stdout, as a function pointer.
Hello's symbols put them there.
lookupTAtom"hello#str.80" hello_globals = Someempty_ptr ∧ lookupTAtom"hello#str.81" hello_globals = Somegreeting_ptr ∧ lookupTAtom"close_stdout" hello_globals = Someclose_stdout_ptr
Explore proof 2 tactics
Initial goal
⊢
lookupTAtom"hello#str.80" hello_globals = Someempty_ptr ∧ lookupTAtom"hello#str.81" hello_globals = Somegreeting_ptr ∧ lookupTAtom"close_stdout" hello_globals = Someclose_stdout_ptr
vm_compute
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
vm_compute
auto
Main's entry binds argc and argv.
Explore proof 1 tactics
Main's proof over one Logic instance shared by every layer.
Import L LG SL ML LL HL
74Context registry : name → optioncontractlibc_world wi : mem → libc_world → gmappiece pval → Prop `{!SafepointStablewi} ge : genv
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.
93Context 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, 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.
116Context 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
116Context 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
116Context 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
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.
∀ f e ls lab d vc vp rest j c p b reg bytes old c0 Φ
∗k∈locale_categoriesLL.namedk oldk.1 oldk.2 −∗ ptscodec_psc0 −∗ stringp b reg bytes −∗ ▷∀q new : Z → ptr × listZ c′, ⌜q = mkPtr0 CNone ∨ q = newc.1⌝ −∗ stringp b reg bytes −∗ ptscodec_psc′ −∗ ∗k∈locale_categoriesLL.lentk newk.1 newk.2 −∗ WPERunmkFramef putd WPtrq e ls None Execlab rest j : mexpr {Φ} −∗ WPERunmkFramef e ls None Execlab CallCResultd P GlobalTAtom"setlocale" ArgW vc; ArgP vp :: rest j : mexpr {Φ}
Proof 33 steps Qed
intros Hc Hp Hcat
iIntros Hks Hcodec Hs HK
pose proof Hlinked as _ & _ & Hext
iApply LL.wp_lendregistry wi ge Hlent f e ls lab d TAtom"setlocale" ArgW vc; ArgP vp rest j libc_setlocale_contractrep requests WIntc; WPtrp locale_categories old codec_psc0 λq new gs′ ⇒ q = mkPtr0 CNone ∨ q = newc.1 ∧ ∃c′, gs′ = codec_psc′ with Hks Hcodec Hs [HK] ; exact Hsetlocale | reflexivity | apply linked_outside ; first exact Hlinked | reflexivity | apply linked_unbound ; first exact Hlinked | reflexivity | reflexivity | cbn [ map_option ] ; rewrite Hc Hp ; reflexivity | | | | |
–split ; right ; eexists ; reflexivity | do 2 eexists ; reflexivity
–apply List.Forall_forall
intros k Hk
cbn
rewrite list_elem_of_singleton
intros E
injection E as →
unfold codec_key , locale_categories in Hk
cbn in Hk
intuition lia
–iIntros σ Hσ Hs
iDestruct Hs as [%Hok Hps]
iDestruct pts_facts with Hσ Hps as %Hag & _
iDestruct Hσ as h [_ %Hf]
destruct Hf as _ & _ & _ & Hw
iPureIntro
–intros s m w h trace values s′ m′ w′ Hw Ha Hd Hr Hi
destruct Kset_ _ _ _ _ _ _ _ _ _ _ _ _ Hw Ha Hd Hr Hi as q & new & c′ & Hv & Hq & Ha′ & Hd′ & Hr′ & Hw′
exists q, new, codec_psc'
split ; exact Hv |
split ; split ; exact Hq | eauto |
split ; reflexivity |
split ; cbn ; repeat constructor |
auto
–iNext
iIntros q new gs′ Hq c′ → Hs Hcodec Hl
iApply HK with [%] Hs Hcodec Hl
exact Hq
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.
183Context 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
Eight zero bytes and an empty slot at offset 0 are a null pointer cell.
Explore proof 8 tactics
Initial goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
rewrite / bytes / auxes / pcell - pts_app
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
assert E : byte_psb 0 replicate8 0 ++ aux_psb 0 CNone = cellb 0 0 ++ PAuxb 0, VAuxCNone
2 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
focused goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
{vm_compute
2 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
⊢
PByteb 0, VByte0; PByteb 1, VByte0; PByteb 2, VByte0; PByteb 3, VByte0; PByteb 4, VByte0; PByteb 5, VByte0; PByteb 6, VByte0; PByteb 7, VByte0; PAuxb 0, VAuxCNone = PByteb 0, VByte0; PByteb 1, VByte0; PByteb 2, VByte0; PByteb 3, VByte0; PByteb 4, VByte0; PByteb 5, VByte0; PByteb 6, VByte0; PByteb 7, VByte0; PAuxb 0, VAuxCNone
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
reflexivity
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
rewrite E pts_app
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
cbn [ ptr_addr ptr_cap ]
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
rewrite / pts ! big_sepL_cons big_sepL_nil
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
⊢
pointstoPByteb 0 + 0, VBytebyte_of0 0.1 DfracOwn1 PByteb 0 + 0, VBytebyte_of0 0.2 ∗ pointstoPByteb 0 + 1, VBytebyte_of0 1.1 DfracOwn1 PByteb 0 + 1, VBytebyte_of0 1.2 ∗ pointstoPByteb 0 + 2, VBytebyte_of0 2.1 DfracOwn1 PByteb 0 + 2, VBytebyte_of0 2.2 ∗ pointstoPByteb 0 + 3, VBytebyte_of0 3.1 DfracOwn1 PByteb 0 + 3, VBytebyte_of0 3.2 ∗ pointstoPByteb 0 + 4, VBytebyte_of0 4.1 DfracOwn1 PByteb 0 + 4, VBytebyte_of0 4.2 ∗ pointstoPByteb 0 + 5, VBytebyte_of0 5.1 DfracOwn1 PByteb 0 + 5, VBytebyte_of0 5.2 ∗ pointstoPByteb 0 + 6, VBytebyte_of0 6.1 DfracOwn1 PByteb 0 + 6, VBytebyte_of0 6.2 ∗ pointstoPByteb 0 + 7, VBytebyte_of0 7.1 DfracOwn1 PByteb 0 + 7, VBytebyte_of0 7.2 ∗ emp ∗ pointstoPAuxb 0, VAuxCNone.1 DfracOwn1 PAuxb 0, VAuxCNone.2 ∗ emp ⊣⊢ pointstoPAuxb 0, VAuxCNone.1 DfracOwn1 PAuxb 0, VAuxCNone.2 ∗ pointstoPByteb 0 + 0, VBytebyte_of0 0.1 DfracOwn1 PByteb 0 + 0, VBytebyte_of0 0.2 ∗ pointstoPByteb 0 + 1, VBytebyte_of0 1.1 DfracOwn1 PByteb 0 + 1, VBytebyte_of0 1.2 ∗ pointstoPByteb 0 + 2, VBytebyte_of0 2.1 DfracOwn1 PByteb 0 + 2, VBytebyte_of0 2.2 ∗ pointstoPByteb 0 + 3, VBytebyte_of0 3.1 DfracOwn1 PByteb 0 + 3, VBytebyte_of0 3.2 ∗ pointstoPByteb 0 + 4, VBytebyte_of0 4.1 DfracOwn1 PByteb 0 + 4, VBytebyte_of0 4.2 ∗ pointstoPByteb 0 + 5, VBytebyte_of0 5.1 DfracOwn1 PByteb 0 + 5, VBytebyte_of0 5.2 ∗ pointstoPByteb 0 + 6, VBytebyte_of0 6.1 DfracOwn1 PByteb 0 + 6, VBytebyte_of0 6.2 ∗ pointstoPByteb 0 + 7, VBytebyte_of0 7.1 DfracOwn1 PByteb 0 + 7, VBytebyte_of0 7.2 ∗ emp
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.
iApply wp_enter_ _ _ _ _ _ _ _ main_blocks ; vm_compute ; reflexivity | word_premise | ; iNext ; cbn [ b_insts b_jump main_block hblk ]
mbszero at the start of an object: mbszero_spec at offset 0.
∀ b reg xs cs Φ
liveb reg −∗ bytesb 0 xs −∗ auxesb 0 cs −∗ ▷liveb reg −∗ bytesb 0 replicate8 0 −∗ auxesb 0 clear_slots0 cs −∗ ΦRetVoid −∗ WPERuninvocationmbszero_fn WPtrmkPtrb Objb : mexpr {Φ}
Explore proof 8 tactics
Initial goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
reg :
xs :
listZ
cs :
listcap
Φ :
outcome → iPropIΣ
intros Lx Lc Hb8 Hend
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
reg :
xs :
listZ
cs :
listcap
Φ :
outcome → iPropIΣ
Lx :
lengthxs = 8%nat
Lc :
lengthcs = 8%nat
Hb8 :
b mod 8 = 0
Hend :
b + 8 ≤ r_endreg
⊢
liveb reg −∗ bytesb 0 xs −∗ auxesb 0 cs −∗ ▷liveb reg −∗ bytesb 0 replicate8 0 −∗ auxesb 0 clear_slots0 cs −∗ ΦRetVoid −∗ WPERuninvocationmbszero_fn WPtrptr_addr ≔ b; ptr_cap ≔ Objb : mexpr {v. Φv}
pose proof mbszero_specregistry wi ge Hlinked b reg 0 xs cs Φ as H
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
reg :
xs :
listZ
cs :
listcap
Φ :
outcome → iPropIΣ
Lx :
lengthxs = 8%nat
Lc :
lengthcs = 8%nat
Hb8 :
b mod 8 = 0
Hend :
b + 8 ≤ r_endreg
H :
registryTAtom"memset" = Somememset_contractlibc_world → lengthxs = 8%nat → lengthcs = 8%nat → b mod 8 = 0 → 0 mod 8 = 0 → 0 ≤ 0 → b + 0 + 8 ≤ r_endreg → ∀m m′ : mem wd : libc_world h : gmappiece pval, memset_resultm ptr_addr ≔ b + 0; ptr_cap ≔ Objb 0 8 m′ → ∀l : piece v : pval, l, v ∈ block_psb reg 0 xs cs → h !! l = Somev → wim wd h → wim′ wd overwriteblock_psb reg 0 replicate8 0 clear_slots0 cs h → LG.liveb reg −∗ ML.bytesb 0 xs −∗ ML.auxesb 0 cs −∗ ▷LG.liveb reg −∗ ML.bytesb 0 replicate8 0 −∗ ML.auxesb 0 clear_slots0 cs −∗ ΦRetVoid −∗ WPL.ERuninvocationmbszero_fn WPtrptr_addr ≔ b + 0; ptr_cap ≔ Objb : mexpr {v. Φv}
⊢
liveb reg −∗ bytesb 0 xs −∗ auxesb 0 cs −∗ ▷liveb reg −∗ bytesb 0 replicate8 0 −∗ auxesb 0 clear_slots0 cs −∗ ΦRetVoid −∗ WPERuninvocationmbszero_fn WPtrptr_addr ≔ b; ptr_cap ≔ Objb : mexpr {v. Φv}
rewrite ! Z.add_0_r in H
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
reg :
xs :
listZ
cs :
listcap
Φ :
outcome → iPropIΣ
Lx :
lengthxs = 8%nat
Lc :
lengthcs = 8%nat
Hb8 :
b mod 8 = 0
Hend :
b + 8 ≤ r_endreg
H :
registryTAtom"memset" = Somememset_contractlibc_world → lengthxs = 8%nat → lengthcs = 8%nat → b mod 8 = 0 → 0 mod 8 = 0 → 0 ≤ 0 → b + 8 ≤ r_endreg → ∀m m′ : mem wd : libc_world h : gmappiece pval, memset_resultm ptr_addr ≔ b; ptr_cap ≔ Objb 0 8 m′ → ∀l : piece v : pval, l, v ∈ block_psb reg 0 xs cs → h !! l = Somev → wim wd h → wim′ wd overwriteblock_psb reg 0 replicate8 0 clear_slots0 cs h → LG.liveb reg −∗ ML.bytesb 0 xs −∗ ML.auxesb 0 cs −∗ ▷LG.liveb reg −∗ ML.bytesb 0 replicate8 0 −∗ ML.auxesb 0 clear_slots0 cs −∗ ΦRetVoid −∗ WPL.ERuninvocationmbszero_fn WPtrptr_addr ≔ b; ptr_cap ≔ Objb {v. Φv}
⊢
liveb reg −∗ bytesb 0 xs −∗ auxesb 0 cs −∗ ▷liveb reg −∗ bytesb 0 replicate8 0 −∗ auxesb 0 clear_slots0 cs −∗ ΦRetVoid −∗ WPERuninvocationmbszero_fn WPtrptr_addr ≔ b; ptr_cap ≔ Objb : mexpr {v. Φv}
iApply H ; exact Hmemset | exact Lx | exact Lc | exact Hb8 | reflexivity | lia | exact Hend |
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
reg :
xs :
listZ
cs :
listcap
Φ :
outcome → iPropIΣ
Lx :
lengthxs = 8%nat
Lc :
lengthcs = 8%nat
Hb8 :
b mod 8 = 0
Hend :
b + 8 ≤ r_endreg
H :
registryTAtom"memset" = Somememset_contractlibc_world → lengthxs = 8%nat → lengthcs = 8%nat → b mod 8 = 0 → 0 mod 8 = 0 → 0 ≤ 0 → b + 8 ≤ r_endreg → ∀m m′ : mem wd : libc_world h : gmappiece pval, memset_resultm ptr_addr ≔ b; ptr_cap ≔ Objb 0 8 m′ → ∀l : piece v : pval, l, v ∈ block_psb reg 0 xs cs → h !! l = Somev → wim wd h → wim′ wd overwriteblock_psb reg 0 replicate8 0 clear_slots0 cs h → LG.liveb reg −∗ ML.bytesb 0 xs −∗ ML.auxesb 0 cs −∗ ▷LG.liveb reg −∗ ML.bytesb 0 replicate8 0 −∗ ML.auxesb 0 clear_slots0 cs −∗ ΦRetVoid −∗ WPL.ERuninvocationmbszero_fn WPtrptr_addr ≔ b; ptr_cap ≔ Objb {v. Φv}
⊢
∀m m′ : mem wd : libc_world h : gmappiece pval, memset_resultm ptr_addr ≔ b; ptr_cap ≔ Objb 0 8 m′ → ∀l : piece v : pval, l, v ∈ block_psb reg 0 xs cs → h !! l = Somev → wim wd h → wim′ wd overwriteblock_psb reg 0 replicate8 0 clear_slots0 cs h
intros m m′ wd h Hr Hin Hw
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
reg :
xs :
listZ
cs :
listcap
Φ :
outcome → iPropIΣ
Lx :
lengthxs = 8%nat
Lc :
lengthcs = 8%nat
Hb8 :
b mod 8 = 0
Hend :
b + 8 ≤ r_endreg
H :
registryTAtom"memset" = Somememset_contractlibc_world → lengthxs = 8%nat → lengthcs = 8%nat → b mod 8 = 0 → 0 mod 8 = 0 → 0 ≤ 0 → b + 8 ≤ r_endreg → ∀m m′ : mem wd : libc_world h : gmappiece pval, memset_resultm ptr_addr ≔ b; ptr_cap ≔ Objb 0 8 m′ → ∀l : piece v : pval, l, v ∈ block_psb reg 0 xs cs → h !! l = Somev → wim wd h → wim′ wd overwriteblock_psb reg 0 replicate8 0 clear_slots0 cs h → LG.liveb reg −∗ ML.bytesb 0 xs −∗ ML.auxesb 0 cs −∗ ▷LG.liveb reg −∗ ML.bytesb 0 replicate8 0 −∗ ML.auxesb 0 clear_slots0 cs −∗ ΦRetVoid −∗ WPL.ERuninvocationmbszero_fn WPtrptr_addr ≔ b; ptr_cap ≔ Objb {v. Φv}
m, m′ :
wd :
Hr :
memset_resultm ptr_addr ≔ b; ptr_cap ≔ Objb 0 8 m′
Hw :
wim wd h
⊢
wim′ wd overwriteblock_psb reg 0 replicate8 0 clear_slots0 cs h
pose proof Kmemsetb reg 0 xs cs m m′ wd h as K
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
reg :
xs :
listZ
cs :
listcap
Φ :
outcome → iPropIΣ
Lx :
lengthxs = 8%nat
Lc :
lengthcs = 8%nat
Hb8 :
b mod 8 = 0
Hend :
b + 8 ≤ r_endreg
H :
registryTAtom"memset" = Somememset_contractlibc_world → lengthxs = 8%nat → lengthcs = 8%nat → b mod 8 = 0 → 0 mod 8 = 0 → 0 ≤ 0 → b + 8 ≤ r_endreg → ∀m m′ : mem wd : libc_world h : gmappiece pval, memset_resultm ptr_addr ≔ b; ptr_cap ≔ Objb 0 8 m′ → ∀l : piece v : pval, l, v ∈ block_psb reg 0 xs cs → h !! l = Somev → wim wd h → wim′ wd overwriteblock_psb reg 0 replicate8 0 clear_slots0 cs h → LG.liveb reg −∗ ML.bytesb 0 xs −∗ ML.auxesb 0 cs −∗ ▷LG.liveb reg −∗ ML.bytesb 0 replicate8 0 −∗ ML.auxesb 0 clear_slots0 cs −∗ ΦRetVoid −∗ WPL.ERuninvocationmbszero_fn WPtrptr_addr ≔ b; ptr_cap ≔ Objb {v. Φv}
m, m′ :
wd :
Hr :
memset_resultm ptr_addr ≔ b; ptr_cap ≔ Objb 0 8 m′
Hw :
wim wd h
K :
memset_resultm ptr_addr ≔ b + 0; ptr_cap ≔ Objb 0 8 m′ → ∀l : piece v : pval, l, v ∈ block_psb reg 0 xs cs → h !! l = Somev → wim wd h → wim′ wd overwriteblock_psb reg 0 replicate8 0 clear_slots0 cs h
⊢
wim′ wd overwriteblock_psb reg 0 replicate8 0 clear_slots0 cs h
rewrite ! Z.add_0_r in K
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
Hlinked :
Kalloc :
Hmemset :
registryTAtom"memset" = Somememset_contractlibc_world
Kmemset :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractlibc_world
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractlibc_world
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractlibc_world
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
HP.HN.store_keepswi nb nreg
Ksb :
HP.HN.store_keepswi sb sreg
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hsetlocale :
registryTAtom"setlocale" = Somelibc_setlocale_contractrep requests
Hlent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval c : Z p : ptr b : Z reg : region bytes : listZ, 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
Kset :
∀r : call_result args : listarg c : Z p : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : ptr new : Z → ptr × listZ c′ : term, values = WPtrq ∧ q = ptr_addr ≔ 0; ptr_cap ≔ CNone ∨ q = newc.1 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritecodec_psc′ renameh locale_categories new
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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_spec :
Hatexit :
registryTAtom"atexit" = Someatexit_spec
Hatexit_ret :
contract_returnsatexit_spec = RClassW
Hatexit_pre :
∀m : mem w : libc_world h : gmappiece pval, wim w h → contract_preatexit_spec WPtrclose_stdout_ptr m w
Katexit :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, 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 : Z, values = WIntx ∧ 0 ≤ x < 2 ^ 32 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
b :
Z
reg :
xs :
listZ
cs :
listcap
Φ :
outcome → iPropIΣ
Lx :
lengthxs = 8%nat
Lc :
lengthcs = 8%nat
Hb8 :
b mod 8 = 0
Hend :
b + 8 ≤ r_endreg
H :
registryTAtom"memset" = Somememset_contractlibc_world → lengthxs = 8%nat → lengthcs = 8%nat → b mod 8 = 0 → 0 mod 8 = 0 → 0 ≤ 0 → b + 8 ≤ r_endreg → ∀m m′ : mem wd : libc_world h : gmappiece pval, memset_resultm ptr_addr ≔ b; ptr_cap ≔ Objb 0 8 m′ → ∀l : piece v : pval, l, v ∈ block_psb reg 0 xs cs → h !! l = Somev → wim wd h → wim′ wd overwriteblock_psb reg 0 replicate8 0 clear_slots0 cs h → LG.liveb reg −∗ ML.bytesb 0 xs −∗ ML.auxesb 0 cs −∗ ▷LG.liveb reg −∗ ML.bytesb 0 replicate8 0 −∗ ML.auxesb 0 clear_slots0 cs −∗ ΦRetVoid −∗ WPL.ERuninvocationmbszero_fn WPtrptr_addr ≔ b; ptr_cap ≔ Objb {v. Φv}
m, m′ :
wd :
Hr :
memset_resultm ptr_addr ≔ b; ptr_cap ≔ Objb 0 8 m′
Hw :
wim wd h
K :
memset_resultm ptr_addr ≔ b; ptr_cap ≔ Objb 0 8 m′ → ∀l : piece v : pval, l, v ∈ block_psb reg 0 xs cs → h !! l = Somev → wim wd h → wim′ wd overwriteblock_psb reg 0 replicate8 0 clear_slots0 cs h
⊢
wim′ wd overwriteblock_psb reg 0 replicate8 0 clear_slots0 cs h
exact KHr Hin Hw
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
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
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.
0 < b ∧ b mod 16 = 0 ∧ b + 16 ≤ 2 ^ 48
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.
∀ argc av ar a0 b0 r0 ys0 r3 r4 x0 x1 y0 Φ
liveav ar −∗ pcellav 0 a0 −∗ stringa0 b0 r0 ys0 −∗ HP.HN.literalsr3 r4 −∗ HP.HN.name_cellspn nreg sreg nb sb x0 x1 y0 −∗ ▷∀e b4 b6 i k : nat, ⌜start_varse argc av b4 b6 ∧ fresh_okb4 ∧ fresh_okb6 ∧ i ≤ lengthys0%nat ∧ k ≤ lengthys0%nat⌝ −∗ liveav ar −∗ pcellav 0 a0 −∗ stringa0 b0 r0 ys0 −∗ HP.HN.literalsr3 r4 −∗ HP.HN.name_cellspn nreg sreg nb sb mkPtrptr_addra0 + Z.of_nati ptr_capa0 mkPtrptr_addra0 + Z.of_nati ptr_capa0 mkPtrptr_addra0 + Z.of_natk ptr_capa0 −∗ liveb4 mkRegionb4 b4 + 16 Heap Live −∗ bytesb4 0 replicate16 0 −∗ auxesb4 0 replicate16 CNone −∗ liveb6 mkRegionb6 b6 + 16 Heap Live −∗ bytesb6 0 replicate8 0 −∗ bytesb6 8 replicate8 0 −∗ auxesb6 0 clear_slots0 replicate8 CNone −∗ auxesb6 8 replicate8 CNone −∗ WPERunmkFramemain_fn e [ ] None ExecTAtom"start" start_rest b_jumpmain_block"start" : mexpr {Φ} −∗ WPERuninvocationmain_fn WIntargc; WPtrmkPtrav Objav : mexpr {Φ}
Proof 66 steps Qed
intros Hav Hav8 Haend Har48
iIntros Hal Ha0 Hs0 Hlit Hcells HK
pose proof Hlinked as Hm & _ & Hext
rewrite main_entry
mn_enter "start"
iApply wp_alloc_ _ _ _ _ _ _ _ _ _ _ _ _ 8 ; reflexivity | lia | unfold max_allocation_size ; lia | intros m wd h base Hf Hw ; exact Kalloc_ _ _ _ _ Hf Hw |
iNext
iIntros b4 Hb4 Hb4
iApply wp_alloc_ _ _ _ _ _ _ _ _ _ _ _ _ 8 ; reflexivity | lia | unfold max_allocation_size ; lia | intros m wd h base Hf Hw ; exact Kalloc_ _ _ _ _ Hf Hw |
iNext
iIntros b6 Hb6 Hb6
The state is zeroed.
iEval rewrite obj_zero_blockb6 _ ; | compute ; congruence in Hb6
iDestruct Hb6 as (Hl6 & Hy6 & Hc6)
cbn [ req_extent heap_req Z.to_nat Pos.to_nat ] in *
iEval rewrite HC.bytes_split_ _ _ 8 ; | rewrite length_replicate ; vm_compute ; lia in Hy6
iEval rewrite HC.auxes_split_ _ _ 8 ; | rewrite length_replicate ; vm_compute ; lia in Hc6
iDestruct Hy6 as [Hy6 Hy6′]
iDestruct Hc6 as [Hc6 Hc6′]
iApply wp_call_bind_ _ _ _ _ _ _ _ _ _ _ _ _ mbszero_fn invocationmbszero_fn WPtrmkPtrb6 Objb6 ; word_premise | unfold find_fn ; rewrite Hm ; vm_compute ; reflexivity | reflexivity |
iNext
iApply mbszero_at with Hl6 Hy6 Hc6 ; rewrite length_take length_replicate ; vm_compute ; lia | rewrite length_take length_replicate ; vm_compute ; lia | destruct Hb6 as _ & H16 & _ ; apply mod16_mod8 ; exact H16 | change b6 + 8 ≤ b6 + 16 ; lia |
iNext
iIntros Hl6 Hy6 Hc6
iExists _
iSplit ; iPureIntro ; reflexivity |
iNext
argv0, the program's name.
iApply wp_check_read with Hal ; reflexivity | word_premise | left ; reflexivity | addr_premise | addr_premise | addr_premise |
iNext
iIntros Hal
iDestruct Hs0 as [%Hok0 Hps0]
pose proof Hok0 as Hc0 & Hb0 & Hbp0 & Hsend0 & H480 & Hbs0
iApply wp_raw_load_pointer_in with Hal Ha0 Hps0 ; reflexivity | word_premise | left ; reflexivity | addr_premise | addr_premise | lia | intros xb Hxb ; exists r0 ; destruct Hc0 as Hc0 | Hc0 ; rewrite Hc0 in Hxb ; destruct Hxb as Hxb | Hxb ; try discriminate Hxb ; injection Hxb as ← ; apply elem_of_cons ; left ; reflexivity |
iNext
iIntros Hal Ha0 Hps0
iApply wp_call_bind_ _ _ _ _ _ _ _ _ _ _ _ _ set_program_name_fn invocationset_program_name_fn WPtra0 ; word_premise | unfold find_fn ; rewrite Hm ; vm_compute ; reflexivity | reflexivity |
iNext
iApply HP.set_program_name_string_specregistry wi ge Hlinked Hstrrchr Hmemcmp Hstrncmp pn nreg sreg nb sb Hnb Hsb Hpn_end Hnb_cell Hsb_cell Kpn Knb Ksb with Hs0 Hlit Hcells
iNext
iIntros i k Hi Hk Hsuf Hback Hlit Hcells
iExists _
iSplit ; iPureIntro ; reflexivity |
iNext
iDestruct Hback with Hsuf as Hs0
setlocale(LC_ALL, "").
destruct main_globals as G80 & G81 & Gcs
destruct Hlinked as _ & Hg & _
iApply wp_let ; reflexivity | reflexivity | cbn ; rewrite Hg_ _ G80 ; reflexivity | intros ; word_premise |
iNext
iEval rewrite obj_zero_blockb4 _ ; | compute ; congruence in Hb4
iDestruct Hb4 as (Hl4 & Hy4 & Hc4)
destruct Hb4 as Hb40 & Hb416 & Hb448
destruct Hb6 as Hb60 & Hb616 & Hb648
iApply HK $! _ b4 b6 i k with [%] Hal Ha0 Hs0 Hlit Hcells Hl4 Hy4 Hc4 Hl6 Hy6 Hy6′ Hc6 Hc6′
split ; repeat split ; assumption |
split ; split ; exact Hb40 | split ; exact Hb416 | exact Hb448 |
split ; split ; exact Hb60 | split ; exact Hb616 | exact Hb648 |
auto
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.
∀ e argc av b4 b6 old c0 r80 Φ
start_varse argc av b4 b6
fresh_okb4
∗k∈locale_categoriesLL.namedk oldk.1 oldk.2 −∗ ptscodec_psc0 −∗ stringempty_ptr 69968 r80 [ ] −∗ liveb4 mkRegionb4 b4 + 16 Heap Live −∗ bytesb4 0 replicate16 0 −∗ auxesb4 0 replicate16 CNone −∗ ▷∀e′ q new : Z → ptr × listZ c′, ⌜start_varse′ argc av b4 b6 ∧ lookupTAtom"chk1" e′ = SomeWPtrmkPtrb4 Objb4 ∧ q = mkPtr0 CNone ∨ q = new6.1⌝ −∗ ∗k∈locale_categoriesLL.lentk newk.1 newk.2 −∗ ptscodec_psc′ −∗ stringempty_ptr 69968 r80 [ ] −∗ liveb4 mkRegionb4 b4 + 16 Heap Live −∗ pcellb4 0 greeting_ptr −∗ bytesb4 8 replicate8 0 −∗ auxesb4 1 replicate15 CNone −∗ WPERunmkFramemain_fn e′ [ ] None EnterTAtom"iw_1.L8" SomeTAtom"start" : mexpr {Φ} −∗ WPERunmkFramemain_fn e [ ] None ExecTAtom"start" start_rest b_jumpmain_block"start" : mexpr {Φ}
Proof 55 steps Qed
intros H0 & H2 & H4 & H6 & H11 Hb40 & Hb416 & Hb448
iIntros Hks Hcod Hs80 Hl4 Hy4 Hc4 HK
destruct main_globals as G80 & G81 & Gcs
pose proof Hlinked as Hm & Hg & _
rewrite / start_rest
cbn [ b_jump main_block hblk ]
setlocale(LC_ALL, "").
iApply wp_main_setlocale with Hks Hcod Hs80 ; word_premise | word_premise | cbn ; tauto |
iNext
iIntros q new c′ Hq Hs80 Hcod Hlent
The default greeting, stored in b4's cell.
iApply wp_let ; reflexivity | reflexivity | cbn ; rewrite Hg_ _ G81 ; reflexivity | intros ; word_premise |
iNext
iApply wp_check with Hl4 ; reflexivity | word_premise | reflexivity | addr_premise | cbn [ ptr_addr r_end ] ; unfold raw_address ; drop_wraps_goal ; lia | cbn [ ptr_addr ] ; unfold raw_address ; drop_wraps_goal ; rewrite Z.add_0_r ; apply mod16_mod8 ; exact Hb416 |
iNext
iIntros Hl4
iEval rewrite HC.bytes_split_ _ _ 8 ; | rewrite length_replicate ; lia in Hy4
iEval rewrite HC.auxes_split_ _ _ 1 ; | rewrite length_replicate ; lia in Hc4
iDestruct Hy4 as [Hy4 Hy4′]
iDestruct Hc4 as [Hc4 Hc4′]
iAssert pcellb4 0 mkPtr0 CNone with [Hy4 Hc4] as Hp4 ; iApply zero_pcell ; iFrame |
iApply wp_raw_store_pointer with Hl4 Hp4 ; word_premise | word_premise | reflexivity | addr_premise | rewrite Z.add_0_r ; apply mod16_mod8 ; exact Hb416 | intros m wd h Hin Hw ; exact Kpstore_ _ _ _ _ _ _ _ Hin Hw |
iNext
iIntros Hl4 Hp4
atexit(close_stdout).
iApply wp_let ; reflexivity | reflexivity | cbn ; rewrite Hg_ _ Gcs ; reflexivity | intros ; word_premise |
iNext
iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ atexit_spec WPtrclose_stdout_ptr emp%I with [//] [-] ; apply linked_outside ; first exact Hlinked | reflexivity | apply linked_unbound ; first exact Hlinked | reflexivity | reflexivity | exact Hatexit | cbn [ map_option ] ; word_premise | exact Hatexit_abi | |
–iIntros σ Hσ _
iDestruct Hσ as h [_ %Hf]
destruct Hf as _ & _ & _ & Hw
iPureIntro
exact Hatexit_pre_ _ _ Hw
–iNext
iIntros σ trace values s′ m′ w′ Hi Hσ _
iDestruct Hσ as h [Hh %Hf]
destruct Hf as Ha & Hd & Hr & Hw
iModIntro
iExists _
iSplit
+iSplitL Hh ; iExists h ; iFrame ; iPureIntro ; auto |
iApply wp_goto
iNext
cbn [ edge_label ]
iApply HK $! _ q new c' with [%] Hlent Hcod Hs80 Hl4 Hp4 Hy4′ Hc4′
split ; repeat split ; assumption |
split ; assumption | exact Hq
Main's start block, from its entry to the option loop: the two segments above.
∀ argc av ar a0 b0 r0 ys0 r3 r4 x0 x1 y0 old c0 r80 Φ
liveav ar −∗ pcellav 0 a0 −∗ stringa0 b0 r0 ys0 −∗ HP.HN.literalsr3 r4 −∗ HP.HN.name_cellspn nreg sreg nb sb x0 x1 y0 −∗ ∗k∈locale_categoriesLL.namedk oldk.1 oldk.2 −∗ ptscodec_psc0 −∗ stringempty_ptr 69968 r80 [ ] −∗ ▷∀e b4 b6 i k : nat q new : Z → ptr × listZ c′, ⌜start_varse argc av b4 b6 ∧ lookupTAtom"chk1" e = SomeWPtrmkPtrb4 Objb4 ∧ fresh_okb4 ∧ fresh_okb6 ∧ i ≤ lengthys0%nat ∧ k ≤ lengthys0%nat ∧ q = mkPtr0 CNone ∨ q = new6.1⌝ −∗ liveav ar −∗ pcellav 0 a0 −∗ stringa0 b0 r0 ys0 −∗ HP.HN.literalsr3 r4 −∗ HP.HN.name_cellspn nreg sreg nb sb mkPtrptr_addra0 + Z.of_nati ptr_capa0 mkPtrptr_addra0 + Z.of_nati ptr_capa0 mkPtrptr_addra0 + Z.of_natk ptr_capa0 −∗ ∗k∈locale_categoriesLL.lentk newk.1 newk.2 −∗ ptscodec_psc′ −∗ stringempty_ptr 69968 r80 [ ] −∗ liveb4 mkRegionb4 b4 + 16 Heap Live −∗ pcellb4 0 greeting_ptr −∗ bytesb4 8 replicate8 0 −∗ auxesb4 1 replicate15 CNone −∗ liveb6 mkRegionb6 b6 + 16 Heap Live −∗ bytesb6 0 replicate8 0 −∗ bytesb6 8 replicate8 0 −∗ auxesb6 0 clear_slots0 replicate8 CNone −∗ auxesb6 8 replicate8 CNone −∗ WPERunmkFramemain_fn e [ ] None EnterTAtom"iw_1.L8" SomeTAtom"start" : mexpr {Φ} −∗ WPERuninvocationmain_fn WIntargc; WPtrmkPtrav Objav : mexpr {Φ}
Proof 10 steps Qed
intros Hav Hav8 Haend Har48
iIntros Hal Ha0 Hs0 Hlit Hcells Hks Hcod Hs80 HK
iApply main_to_setlocale with Hal Ha0 Hs0 Hlit Hcells ; exact Hav | exact Hav8 | exact Haend | exact Har48 |
iNext
iIntros e b4 b6 i k Hv & Hf4 & Hf6 & Hi & Hk Hal Ha0 Hs0 Hlit Hcells Hl4 Hy4 Hc4 Hl6 Hy6 Hy6′ Hc6 Hc6′
iApply main_start_rest with Hks Hcod Hs80 Hl4 Hy4 Hc4 ; exact Hv | exact Hf4 |
iNext
iIntros e′ q new c′ Hv′ & Hc1 & Hq Hlent Hcod Hs80 Hl4 Hp4 Hy4 Hc4
iApply HK $! e' b4 b6 i k q new c' with [%] Hal Ha0 Hs0 Hlit Hcells Hlent Hcod Hs80 Hl4 Hp4 Hy4 Hc4 Hl6 Hy6 Hy6′ Hc6 Hc6′
auto 10