Fil-C on Nix

Filnix wiki

the formal campaign

rocq/theories/HelloConv.v

GNU Hello's conversion of its greeting through the program logic of Logic.v (docs/logic.md): libc's mbrtowc, and gnulib's rpl_mbrtowc and rpl_mbsrtowcs around it, which main calls to turn the greeting into wide characters.

mbrtowc(out, src, n, state) writes three cells the program owns: the wide character at out, the conversion state and errno. Its triple (wp_mbrtowc) takes the three as whole blocks, with their life, bytes and aux slots, and hands them back holding whatever the memory holds after the call, which conv_result describes: Campaign 4's mbrtowc_result read through the owned bytes, under the audited codec. ContractFrame.v's prefix_agrees_out keeps every other piece agreeing, though the call's roots now meet the program's objects.

The world is Libc.v's libc_world. The triple is generic in the world interpretation wi, given that wi makes libc ready, fixes the codec and the errno cell, keeps libc's private roots, releases and capabilities apart from the program's objects (libc_private), and survives the call's writes into the three blocks. The audited codec premise (Haudit) stays explicit, as docs/logic.md records: it is not derived from the locale.

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
Open Scope Z_scope
Open Scope list_scope
35Module HelloConvOn R : Runtime LG0 : LogicSigR
36Module HLo ≔ HelloLocaleOn R LG0
37Module HL ≔ HLo.HL
38Module LL ≔ HL.LL
39Module ML ≔ HL.ML
40Module SL ≔ ML.SL
41Module LG ≔ ML.LG
42Module L ≔ LG.L
43Module LB ≔ LibcOn R L.M
Import L LG SL ML LL HL HLo

mbrtowc's triple

48Section mbrtowc
49Context `{!invGS_genhlc Σ, !gen_heapGSpiece pval Σ}
50Context registry : name → optioncontractlibc_world wi : mem → libc_world → gmappiece pval → Prop `{!SafepointStablewi} ge : genv

The Iris instance of the registry and wi.

54Instance conv_irisGS: irisGS_genhlc nanofil_langregistry ge Σ ≔
nanofil_irisGSregistry wi ge

The expressions of the language.

58Notation cexpr ≔ language.exprnanofil_langregistry ge

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

62Context valid : term → listZ → Prop
62Context audit : term → optionaudited_codec
62Context rep : mem → libc_world → Prop
62Context requests : listword → mem → libc_world → Z → Z → Prop
62Context Hmbrtowc : registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
62Context Hvalid0 : mbstate_zero_validvalid
62Context 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).

71Context errno : ptr
71Context 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.

78Context 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.

83Context 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

Owning two blocks, they are of different objects: each life is owned once.

96Lemma block_ne
∀ b reg o xs cs b′ reg′ o′ xs′ cs′
ptsblock_psb reg o xs cs −∗ ptsblock_psb′ reg′ o′ xs′ cs′ −∗ ⌜b ≠ b′⌝
Explore proof 7 tactics

Initial goal

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
ptr
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, 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
b :
Z
reg :
region
o :
Z
xs :
listZ
cs :
listcap
b′ :
Z
reg′ :
region
o′ :
Z
xs′ :
listZ
cs′ :
listcap
⊢
ptsblock_psb reg o xs cs −∗ ptsblock_psb′ reg′ o′ xs′ cs′ −∗ ⌜b ≠ b′⌝

rewrite / block_ps / pts ! big_sepL_cons

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
ptr
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, 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
b :
Z
reg :
region
o :
Z
xs :
listZ
cs :
listcap
b′ :
Z
reg′ :
region
o′ :
Z
xs′ :
listZ
cs′ :
listcap
⊢
pointstoPLiveb, VLivereg.1 DfracOwn1 PLiveb, VLivereg.2 ∗ ∗y∈byte_psb o xs ++ aux_psb o cspointstoy.1 DfracOwn1 y.2 −∗ pointstoPLiveb′, VLivereg′.1 DfracOwn1 PLiveb′, VLivereg′.2 ∗ ∗y∈byte_psb′ o′ xs′ ++ aux_psb′ o′ cs′pointstoy.1 DfracOwn1 y.2 −∗ ⌜b ≠ b′⌝

iIntros [Hl _] [Hl′ _]

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
ptr
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, 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
b :
Z
reg :
region
o :
Z
xs :
listZ
cs :
listcap
b′ :
Z
reg′ :
region
o′ :
Z
xs′ :
listZ
cs′ :
listcap
Hl :
pointstoPLiveb, VLivereg.1 DfracOwn1 PLiveb, VLivereg.2
Hl′ :
pointstoPLiveb′, VLivereg′.1 DfracOwn1 PLiveb′, VLivereg′.2
∗
⌜b ≠ b′⌝

iDestruct pointsto_ne with Hl Hl′ as %Hne

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
ptr
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, 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
b :
Z
reg :
region
o :
Z
xs :
listZ
cs :
listcap
b′ :
Z
reg′ :
region
o′ :
Z
xs′ :
listZ
cs′ :
listcap
Hne :
PLiveb, VLivereg.1 ≠ PLiveb′, VLivereg′.1
Hl :
pointstoPLiveb, VLivereg.1 DfracOwn1 PLiveb, VLivereg.2
Hl′ :
pointstoPLiveb′, VLivereg′.1 DfracOwn1 PLiveb′, VLivereg′.2
∗
⌜b ≠ b′⌝

iPureIntro

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
ptr
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, 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
b :
Z
reg :
region
o :
Z
xs :
listZ
cs :
listcap
b′ :
Z
reg′ :
region
o′ :
Z
xs′ :
listZ
cs′ :
listcap
Hne :
PLiveb, VLivereg.1 ≠ PLiveb′, VLivereg′.1
⊢
b ≠ b′

intros ←

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
ptr
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, 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
b :
Z
reg :
region
o :
Z
xs :
listZ
cs :
listcap
reg′ :
region
o′ :
Z
xs′ :
listZ
cs′ :
listcap
Hne :
PLiveb, VLivereg.1 ≠ PLiveb, VLivereg′.1
⊢
False

apply Hne

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
ptr
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, 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
b :
Z
reg :
region
o :
Z
xs :
listZ
cs :
listcap
reg′ :
region
o′ :
Z
xs′ :
listZ
cs′ :
listcap
Hne :
PLiveb, VLivereg.1 ≠ PLiveb, VLivereg′.1
⊢
PLiveb, VLivereg.1 = PLiveb, VLivereg′.1

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
rewrite / block_ps / pts ! big_sepL_cons
iIntros [Hl _] [Hl′ _]
iDestruct pointsto_ne with Hl Hl′ as %Hne
iPureIntro
intros ←
apply Hne
reflexivity

The arguments are admitted (mbrtowc_pre) where the program owns the output, state and errno blocks and the source's life and bytes, of four different objects, the state's bytes valid.

106Lemma mbrtowc_admitted
∀ codec m w h out src n state bo ro oo xo co bs rs os ys cs be re oe xe ce bsrc rsrc osrc ss
wim w h
agreesm h
live_disjointm
objects_fitm_regionsm
h !! PNamecodec_key = SomeVCodeccodec
∀l v, l, v ∈ block_psbo ro oo xo co → h !! l = Somev
∀l v, l, v ∈ block_psbs rs os ys cs → h !! l = Somev
∀l v, l, v ∈ block_psbe re oe xe ce → h !! l = Somev
∀l v, l, v ∈ block_psbsrc rsrc osrc ss [ ] → h !! l = Somev
bo ≠ bs
bo ≠ be
bo ≠ bsrc
bs ≠ be
bs ≠ bsrc
be ≠ bsrc
out = mkPtrbo + oo Objbo
state = mkPtrbs + os Objbs
errno = mkPtrbe + oe Objbe
ptr_capsrc = Objbsrc ∨ ptr_capsrc = Robsrc
ptr_addrsrc = bsrc + osrc
0 < bo
0 < bs
0 < bsrc
bo + oo mod 4 = 0
bs + os mod 4 = 0
lengthxo = 4%nat
lengthys = 8%nat
lengthxe = 4%nat
0 < n ≤ Z.of_natlengthss
Forallλx ⇒ 0 ≤ x < 256 ss
validcodec ys
mbrtowc_prevalid rep WPtrout; WPtrsrc; WIntn; WPtrstate m w
Proof 125 steps Qed
intros Hw Ha Hd Hfit Hcod Ho Hs He Hsr Nos Noe Nosr Nse Nssr Nesr → → Herr Hcap Haddr Hbo Hbs Hbsrc Hoal Hsal Lxo Lys Lxe Hn Hss Hval
pose proof Hbytes_ _ Hval as Hyb
destruct Hlibcm w h Hw as Hready & Hcur & Herrno & Hown & Hpriv
pose proof Hcur_ Hcod as Hcodec
destruct block_factsm h bo ro oo xo co Ha Ho nonempty_of_lengthxo 3 Lxo as Lo & Oo & Eo & _
destruct block_factsm h bs rs os ys cs Ha Hs nonempty_of_lengthys 7 Lys as Ls & Os & Es & Vs
destruct block_factsm h be re oe xe ce Ha He nonempty_of_lengthxe 3 Lxe as Le & Oe & Ee & _
destruct block_factsm h bsrc rsrc osrc ss [ ] Ha Hsr ltac:intros E ; rewrite E in Hn ; cbn in Hn ; lia as Lsr & Osr & Esr & Vsr
rewrite Lxo in Eo
rewrite Lys in Es
rewrite Lxe in Ee
assert Hkey : ∀b reg o zs ds, ∀l v, l, v ∈ block_psb reg o zs ds → h !! l = Somev → h !! PLiveb = SomeVLivereg
{intros b reg o zs ds H
apply H
apply elem_of_cons
left
reflexivity
destruct Hpriv_ _ _ Hkey_ _ _ _ _ Ho I Lo as Ro & Co1 & Co2
destruct Hpriv_ _ _ Hkey_ _ _ _ _ Hs I Ls as Rs & Cs1 & Cs2
destruct Hpriv_ _ _ Hkey_ _ _ _ _ He I Le as Re & Ce1 & Ce2
destruct Hpriv_ _ _ Hkey_ _ _ _ _ Hsr I Lsr as Rsr & Csr1 & Csr2
cbn [ piece_id ] in Ro , Co1 , Co2 , Rs , Cs1 , Cs2 , Re , Ce1 , Ce2 , Rsr , Csr1 , Csr2
pose proof Hfit_ _ proj1Lsr as Fsr0 Fsr1
assert Hsrc_bytes : ∀i, 0 ≤ i < n → ∃x, ss !! Z.to_nati = Somex ∧ m_bytesm ptr_addrsrc + i = x ∧ 0 ≤ x < 256
{intros i Hi
destruct lookup_lt_is_Some_2ss Z.to_nati ltac:lia as x Hx
exists x
split ; exact Hx |
split ; | exact proj1Forall_lookup_ _ Hss _ _ Hx
rewrite Haddr
rewrite <- Vsr_ _ Hx
f_equal
lia
unfold mbrtowc_pre
rewrite Herrno Herr
split ; exact Hready |
split ; exact Hvalid0 |
split ; exact Hbytes |
exists mkPtrbo + oo Objbo, src, n, mkPtrbs + os Objbs
split ; reflexivity |
cbn [ ptr_addr ptr_cap ]
split ; lia |
split ; lia |
split ; lia |
split
{split ; lia |
split ; exists bsrc, rsrc ; split ; exact Hcap | exact Lsr |
split
–destruct Hcap as Hc | Hc ; rewrite Hc Haddr ; apply access_obj_ _ rsrc _ _ Read | apply access_ro_read_ _ rsrc ; solve exact proj1Lsr | lia | apply Z.mod_1_r
–intros i Hi
destruct Hsrc_bytesi Hi as x & _ & → & Hx
exact Hx
split
{unfold writable_span
cbn [ span_size span_ptr ptr_addr ptr_cap ]
split ; lia |
exists bo, ro
split ; reflexivity |
split ; exact proj1Lo |
split ; exact proj2Lo |
apply access_obj_ _ ro _ _ Write ; exact proj1Lo | lia | lia | apply Z.mod_1_r
split ; exact Hoal |
split
{unfold writable_span
cbn [ span_size span_ptr ptr_addr ptr_cap ]
split ; lia |
exists bs, rs
split ; reflexivity |
split ; exact proj1Ls |
split ; exact proj2Ls |
apply access_obj_ _ rs _ _ Write ; exact proj1Ls | lia | lia | apply Z.mod_1_r
split
{split ; lia |
split ; exists bs, rs ; split ; left ; reflexivity | exact Ls |
split
–cbn [ ptr_addr ptr_cap ]
apply access_obj_ _ rs _ _ Read ; exact proj1Ls | lia | lia | apply Z.mod_1_r
–intros i Hi
cbn [ ptr_addr ]
destruct lookup_lt_is_Some_2ys Z.to_nati ltac:lia as x Hx
replace bs + os + i with bs + os + Z.of_natZ.to_nati by lia
rewrite Vs_ _ Hx
exact proj1Forall_lookup_ _ Hyb _ _ Hx
split ; exact Hsal |
split
{rewrite Hcodec mbstate_mem_bytes
cbn [ ptr_addr ]
rewrite <- Lys , mem_bytes_of ; exact Hval |
intros i x Hx
exact Vsi x Hx
split ; apply spans_apart_objectsm bsrc rsrc bo ro ; cbn [ ptr_addr ] ; auto ; lia |
split ; apply spans_apart_objectsm bsrc rsrc bs rs ; cbn [ ptr_addr ] ; auto ; lia |
split ; apply spans_apart_objectsm bo ro bs rs ; cbn [ ptr_addr ] ; auto ; lia |
split
{intros p size Hin
cbn in Hin
destruct Hin as E | E | E | ; injection E as ← ← ; split
–apply spans_apart_objectsm be re bsrc rsrc ; cbn [ ptr_addr ] ; auto ; lia
–intros root Hroot
apply spans_apart_withinroot bsrc rsrc ; exact Rsrroot Hroot | lia | lia
–apply spans_apart_objectsm be re bo ro ; cbn [ ptr_addr ] ; auto ; lia
–intros root Hroot
apply spans_apart_withinroot bo ro ; exact Roroot Hroot | cbn ; lia | cbn ; lia
–apply spans_apart_objectsm be re bs rs ; cbn [ ptr_addr ] ; auto ; lia
–intros root Hroot
apply spans_apart_withinroot bs rs ; exact Rsroot Hroot | cbn ; lia | cbn ; lia
split
{intros base Hbase p Hp
cbn in Hp
pose proof Hownbase _ _ Hbase Hkey_ _ _ _ _ Ho I as N1
pose proof Hownbase _ _ Hbase Hkey_ _ _ _ _ Hs I as N2
pose proof Hownbase _ _ Hbase Hkey_ _ _ _ _ He I as N3
pose proof Hownbase _ _ Hbase Hkey_ _ _ _ _ Hsr I as N4
cbn [ piece_id ] in N1 , N2 , N3 , N4
destruct Hp as [ <-| [ <-| [ <-| [ <-| [ ] ] ] ] ] ; cbn [ ptr_cap ] ; | destruct Hcap as Hc | Hc ; rewrite Hc | | ; split ; congruence
split
{intros root Hroot
apply spans_apart_withinroot be re ; exact Reroot Hroot | cbn ; lia | cbn ; lia
intros p Hp base Hc
cbn in Hp
destruct Hp as [ <-| [ <-| [ <-| [ <-| [ ] ] ] ] ] ; cbn [ ptr_cap ] in Hc
–destruct Hc as E | E ; injection E as ← ; auto | discriminate E
–destruct Hcap as Hc′ | Hc′ ; rewrite Hc' in Hc ; destruct Hc as E | E ; first discriminate E | injection E as ← ; auto
–destruct Hc as E | E ; injection E as ← ; auto | discriminate E
–destruct Hc as E | E ; injection E as ← ; auto | discriminate E

A return of the call keeps every piece but the three blocks' bytes and slots agreeing (prefix_agrees_out), so that, the blocks holding what the memory holds after it, the ghost heap agrees; the live objects stay apart and the runtime ready.

213Lemma mbrtowc_frame
∀ r args s m w h trace values s′ m′ w′ out src n state 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′
wim w h
agreesm h
live_disjointm
R.readys m
∀l v, l, v ∈ block_psbo ro oo xo co → h !! l = Somev
∀l v, l, v ∈ block_psbs rs os ys cs → h !! l = Somev
∀l v, l, v ∈ block_psbe re oe xe ce → h !! l = Somev
out = mkPtrbo + oo Objbo
state = mkPtrbs + os Objbs
errno = mkPtrbe + oe Objbe
lengthxo = 4%nat
lengthco = 4%nat
lengthys = 8%nat
lengthcs = 8%nat
lengthxe = 4%nat
lengthce = 4%nat
n ≠ 0
agreesm′ 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 ∧ live_disjointm′ ∧ R.readys′ m′
Proof 65 steps Qed
intros Hi Hw Ha Hd Hr Ho Hs He → → Herr Lxo Lco Lys Lcs Lxe Lce Hn
destruct Hlibcm w h Hw as _ & _ & Herrno & Hown & Hpriv
destruct block_factsm h bo ro oo xo co Ha Ho nonempty_of_lengthxo 3 Lxo as Lo & Oo & Eo & _
destruct block_factsm h bs rs os ys cs Ha Hs nonempty_of_lengthys 7 Lys as Ls & Os & Es & _
destruct block_factsm h be re oe xe ce Ha He nonempty_of_lengthxe 3 Lxe as Le & Oe & Ee & _
rewrite Lxo in Eo
rewrite Lys in Es
rewrite Lxe in Ee
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hi as born & Hp
destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as Hr′ _
set ks := byte_psbo oo xo ++ aux_psbo oo co.*1 ++ byte_psbs os ys ++ aux_psbs os cs.*1 ++ byte_psbe oe xe ++ aux_psbe oe ce.*1
set outs := λa ⇒ span_containsmkSpanmkPtrbo + oo Objbo 4 a ∨ span_containsmkSpanmkPtrbs + os Objbs 8 a ∨ span_containsmkSpanmkPtrbe + oe Objbe 4 a
assert Hwr : contract_writesmbrtowc_contractvalid audit rep requests WPtrmkPtrbo + oo Objbo; WPtrsrc; WIntn; WPtrmkPtrbs + os Objbs m w = locale_rootslibc_localefstw ++ mkSpanmkPtrbo + oo Objbo 4; mkSpanmkPtrbs + os Objbs 8; mkSpanmkPtrbe + oe Objbe 4
{cbn [ contract_writes mbrtowc_contract mbrtowc_writes ]
rewrite proj2Z.eqb_neqn 0 Hn Herrno Herr
reflexivity
assert Hrel : contract_releasesmbrtowc_contractvalid audit rep requests WPtrmkPtrbo + oo Objbo; WPtrsrc; WIntn; WPtrmkPtrbs + os Objbs m w = locale_ownedlibc_localefstw
{cbn [ contract_releases mbrtowc_contract mbrtowc_releases ]
rewrite proj2Z.eqb_neqn 0 Hn
reflexivity
destruct prefix_agrees_out_ _ _ _ _ _ _ _ _ _ _ h ks outs Hp Hr Hd as Ha′ & _ & Hd′ & _
–intros l v Hl _
exact Hal v Hl
–intros l v Hl Hm
exact agree_piece_registered_ _ _ Hm Hal v Hl
–rewrite Hwr
intros sp a Hin Hsp Hol
apply in_app_or in Hin as Hin | Hin
+exfalso
destruct Hol as l & v & reg & Hl & Hm & Hlv & Hb
destruct Hprivl v reg Hl Hm Hlv as Hroots & _
pose proof Hrootssp Hin as Hap
unfold spans_apart , span_contains in Hap , Hsp
cbn in Hap
lia
+unfold outs
destruct Hin as [ <-| [ <-| [ <-| [ ] ] ] ] ; auto
–intros l v Hl Hk
destruct l as b | b o | b o | k ; try exact I ; intros reg Hlv Ho′ He′ Hout ; apply Hk ; unfold ks ; rewrite ! elem_of_app ; destruct Hout as Hout | Hout | Hout ; unfold span_contains in Hout ; cbn in Hout ; left | right ; left | right ; right ; solve eapply block_keym bo ro oo xo co ; eauto ; lia | eapply block_keym bs rs os ys cs ; eauto ; lia | eapply block_keym be re oe xe ce ; eauto ; lia
–rewrite Hrel
exact Hown
–assert Hlive : ∀b reg o zs ds, ∀l v, l, v ∈ block_psb reg o zs ds → h !! l = Somev → live_atm' b reg
{intros b reg o zs ds H
apply Ha'PLiveb VLivereg ; apply H ; apply elem_of_cons ; left ; reflexivity |
unfold ks
rewrite ! elem_of_app
intros Hk | Hk | Hk ; exact live_not_key_ _ _ _ _ Hk
split ; | split ; exact Hd' | exact Hr'
intros l v Hl
apply lookup_overwrite in Hl as Hin | Hnk Hh
+rewrite ! elem_of_app in Hin
destruct Hin as Hin | Hin | Hin
∗exact block_afterm' bo ro oo 4 l v Hlive_ _ _ _ _ Ho Oo Eo Hin
∗exact block_afterm' bs rs os 8 l v Hlive_ _ _ _ _ Hs Os Es Hin
∗exact block_afterm' be re oe 4 l v Hlive_ _ _ _ _ He Oe Ee Hin
+apply Ha'l v Hh
intros Hk
apply Hnk
unfold ks in Hk
rewrite ! fmap_app ! elem_of_app
rewrite ! elem_of_app in Hk
destruct Hk as Hk | Hk | Hk ; left | right ; left | right ; right
∗exact block_keys_afterm' bo ro oo xo co 4 l Lxo Lco Hk
∗exact block_keys_afterm' bs rs os ys cs 8 l Lys Lcs Hk
∗exact block_keys_afterm' be re oe xe ce 4 l Lxe Lce Hk

Campaign 4's mbrtowc_result, for 0 < n and the audited codec, read through the owned bytes: conv_result.

289Lemma conv_of_result
∀ codec m w out src n state res m′ bo oo xo bs os ys be oe bsrc osrc ss
mbrtowc_resultvalid audit m w out src n state res m′
hello_codec_profileaudit w
locale_codeclibc_localefstw = codec
libc_errnofstw = mkPtrbe + oe Objbe
out = mkPtrbo + oo Objbo
state = mkPtrbs + os Objbs
ptr_addrsrc = bsrc + osrc
lengthxo = 4%nat
∀i x, xo !! i = Somex → m_bytesm bo + oo + Z.of_nati = x
lengthys = 8%nat
∀i x, ys !! i = Somex → m_bytesm bs + os + Z.of_nati = x
0 < n ≤ Z.of_natlengthss
∀i x, ss !! i = Somex → m_bytesm bsrc + osrc + Z.of_nati = x
conv_resultvalid auditcodec = SomeCodecC codec n ss xo ys mem_bytesm′ bo + oo 4 mem_bytesm′ bs + os 8 mem_bytesm′ be + oe 4 res
Proof 106 steps Qed
intros Hfull Hprof Hcodec Herrno Eout Est Haddr Lxo Vo Lys Vs Hn Vss
pose proof Hfull as _ & Hres
subst out state
assert Hst4 : take4 mem_bytesm' bs + os 8 = mem_bytesm' bs + os 4 by reflexivity
assert Hsrc : ∀i, 0 ≤ i < n → ∃x, ss !! Z.to_nati = Somex ∧ m_bytesm ptr_addrsrc + i = x
{intros i Hi
destruct lookup_lt_is_Some_2ss Z.to_nati ltac:lia as x Hx
exists x
split ; exact Hx |
rewrite Haddr
rewrite <- Vss_ _ Hx
f_equal
lia
assert Hnz : ∀k, k ≤ n → ∀i, 0 ≤ i < k → m_bytesm ptr_addrsrc + i ≠ 0 → Forallλx ⇒ x ≠ 0 takeZ.to_natk ss
{intros k Hk H
apply Forall_lookup
intros i x Hx
apply lookup_take_Some in Hx as Hx Hi
destruct HsrcZ.of_nati ltac:lia as x′ & Hx′ & Hb
rewrite Nat2Z.id Hx in Hx'
injection Hx' as ←
rewrite <- Hb
apply H
lia
assert Hkept : ∀a, span_containsmkSpanmkPtrbo + oo Objbo 4 a → m_bytesm' a = m_bytesm a → mem_bytesm' bo + oo 4 = xo
{intros H
rewrite <- Lxo
apply mem_bytes_of
intros i x Hx
pose proof lookup_lt_Some_ _ _ Hx as Hi
rewrite Lxo in Hi
rewrite H ; exact Voi x Hx |
unfold span_contains
cbn
lia
destruct Hres as → & Hv & Hp | Hr & Hr2 & Hv & Hp | → & He & Hk & _ | → & Hv & Hk & Hp
–left
destruct HpHprof as i & Hi & Hz & Ho & Hs
split ; reflexivity |
split ; rewrite <- Hcodec ; exact Hv |
split
+destruct Hsrci Hi as x & Hx & Hb
exists Z.to_nati
split ; lia |
rewrite Hx
congruence
+rewrite Hst4
rewrite <- ! load_bytes_4
split ; exact Ho | exact Hs
–right ; left
destruct HpHprof as Ho & Hs & Hb
split ; exact Hr |
split ; exact Hr2 |
split ; rewrite <- Hcodec ; exact Hv |
rewrite Hst4
rewrite <- ! load_bytes_4
split ; exact Ho |
split ; exact Hs |
apply Hnz ; lia | exact Hb
–right ; right ; left
split ; reflexivity |
split ; rewrite <- load_bytes_4 ; rewrite Herrno in He ; exact He |
split ; exact HkeptHk |
split
{intros Hc
rewrite <- Hcodec in Hc
destruct mbrtowc_c_error_ _ _ _ _ _ _ _ _ Hfull Hc as Hst Hsrc0
split
+rewrite <- mem_bytes_ofm bs + os ys Vs
rewrite Lys
exact Hst
+destruct Hsrc0 ltac:lia as x & Hx & Hb
exists x
split ; exact Hx |
rewrite <- Hb , Z.add_0_r
exact Hsrc0
{intros Hv0 Hz0
rewrite <- Hcodec in Hv0
assert Ey : mem_bytesm bs + os 8 = ys
{rewrite <- mem_bytes_ofm bs + os ys Vs
rewrite Lys
reflexivity
assert Hl0 : load_bytesm ptr_addrmkPtrbs + os Objbs 4 = 0
{cbn [ ptr_addr ]
rewrite load_bytes_4
rewrite <- Ey in Hz0
exact Hz0
rewrite <- Ey in Hv0
destruct mbrtowc_initial_error_ _ _ _ _ _ _ _ _ Hfull Hprof Hl0 Hv0 as Hv′ & Hc′ & Hs0
split ; rewrite <- Hcodec ; exact Hv' |
split
+rewrite Hst4
rewrite <- load_bytes_4
exact Hc'
+destruct Hsrc0 ltac:lia as x & Hx & Hb
exists x
split ; exact Hx |
rewrite <- Hb , Z.add_0_r
exact Hs0
–right ; right ; right
destruct HpHprof as Hn16 Hb
split ; reflexivity |
split ; rewrite <- Hcodec ; exact Hv |
split ; exact HkeptHk |
split ; exact Hn16 |
apply Hnz ; lia | exact Hb

mbrtowc(out, src, n, state)'s triple, from mbrtowc_contract: owning the output, state and errno blocks, of 4, 8 and 4 bytes with their slots, and the source's life and bytes ss, of four different objects, where vo, vs, vn and vt read as out, src, n and state, n is positive and within ss, and the state's bytes are valid, the call binds d to its result r and hands the blocks back holding new bytes and slots, which conv_result describes.

354Lemma wp_mbrtowc
∀ f e ls lab d vo vs vn vt rest j out src n state bo ro oo xo co bs rs os ys cs be re oe xe ce bsrc rsrc osrc ss codec dq Φ
find_fnge TAtom"mbrtowc" = None
lookupTAtom"mbrtowc" ge_globalsge = None
arg_xge e ArgP vo = SomeWPtrout
arg_xge e ArgP vs = SomeWPtrsrc
arg_xge e ArgL vn = SomeWIntn
arg_xge e ArgP vt = SomeWPtrstate
out = mkPtrbo + oo Objbo
state = mkPtrbs + os Objbs
errno = mkPtrbe + oe Objbe
ptr_capsrc = Objbsrc ∨ ptr_capsrc = Robsrc
ptr_addrsrc = bsrc + osrc
0 < bo
0 < bs
0 < bsrc
bo + oo mod 4 = 0
bs + os mod 4 = 0
lengthxo = 4%nat
lengthco = 4%nat
lengthys = 8%nat
lengthcs = 8%nat
lengthxe = 4%nat
lengthce = 4%nat
0 < n ≤ Z.of_natlengthss
Forallλx ⇒ 0 ≤ x < 256 ss
validcodec ys
pointstoPNamecodec_key dq VCodeccodec −∗ ptsblock_psbo ro oo xo co −∗ ptsblock_psbs rs os ys cs −∗ ptsblock_psbe re oe xe ce −∗ ptsblock_psbsrc rsrc osrc ss [ ] −∗ ▷∀r xo′ ys′ xe′ co′ cs′ ce′, ⌜conv_resultvalid auditcodec = SomeCodecC codec n ss xo ys xo′ ys′ xe′ r ∧ lengthxo′ = 4%nat ∧ lengthys′ = 8%nat ∧ lengthxe′ = 4%nat ∧ lengthco′ = 4%nat ∧ lengthcs′ = 8%nat ∧ lengthce′ = 4%nat⌝ −∗ pointstoPNamecodec_key dq VCodeccodec −∗ ptsblock_psbo ro oo xo′ co′ −∗ ptsblock_psbs rs os ys′ cs′ −∗ ptsblock_psbe re oe xe′ ce′ −∗ ptsblock_psbsrc rsrc osrc ss [ ] −∗ WPERunmkFramef putd WIntr e ls None Execlab rest j : cexpr {Φ} −∗ WPERunmkFramef e ls None Execlab CallCResultd L GlobalTAtom"mbrtowc" ArgP vo; ArgP vs; ArgL vn; ArgP vt :: rest j : cexpr {Φ}
Proof 71 steps Qed
intros Hfn Hdata Hvo Hvs Hvn Hvt Eout Est Herr Hcap Haddr Hbo Hbs Hbsrc Hoal Hsal Lxo Lco Lys Lcs Lxe Lce Hn Hss Hval
iIntros Hcod HBo HBs HBe HBsrc HK
iDestruct block_ne with HBo HBs as %N1
iDestruct block_ne with HBo HBe as %N2
iDestruct block_ne with HBo HBsrc as %N3
iDestruct block_ne with HBs HBe as %N4
iDestruct block_ne with HBs HBsrc as %N5
iDestruct block_ne with HBe HBsrc as %N6
iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ mbrtowc_contractvalid audit rep requests WPtrout; WPtrsrc; WIntn; WPtrstate pointstoPNamecodec_key dq VCodeccodec ∗ ptsblock_psbo ro oo xo co ∗ ptsblock_psbs rs os ys cs ∗ ptsblock_psbe re oe xe ce ∗ ptsblock_psbsrc rsrc osrc ss [ ] with [$Hcod $HBo $HBs $HBe $HBsrc] [HK] ; exact Hfn | exact Hdata | reflexivity | exact Hmbrtowc | cbn [ map_option ] ; rewrite Hvo Hvs Hvn Hvt ; reflexivity | | |
–split ; right ; eexists ; reflexivity | do 4 eexists ; reflexivity
–iIntros σ Hσ (Hc & Ho & Hs & He & Hsr)
iDestruct Hσ as h [Hh %Hf]
destruct Hf as Ha & Hd & Hr & Hw
iDestruct gen_heap_valid with Hh Hc as %Kc
iDestruct pts_lookup with Hh Ho as %Ko
iDestruct pts_lookup with Hh Hs as %Ks
iDestruct pts_lookup with Hh He as %Ke
iDestruct pts_lookup with Hh Hsr as %Ksr
iPureIntro
exact mbrtowc_admitted_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hw Ha Hd R.address_space_ _ Hr Kc Ko Ks Ke Ksr N1 N2 N3 N4 N5 N6 Eout Est Herr Hcap Haddr Hbo Hbs Hbsrc Hoal Hsal Lxo Lys Lxe Hn Hss Hval
–iNext
iIntros σ trace values s′ m′ w′ Hinv (%h & Hh & %Hf) (Hc & Ho & Hs & He & Hsr)
destruct Hf as Ha & Hd & Hr & Hw
iDestruct gen_heap_valid with Hh Hc as %Kc
iDestruct pts_lookup with Hh Ho as %Ko
iDestruct pts_lookup with Hh Hs as %Ks
iDestruct pts_lookup with Hh He as %Ke
iDestruct pts_lookup with Hh Hsr as %Ksr
destruct Hlibc_ _ _ Hw as _ & Hcur & Herrno & _
pose proof Hcur_ Kc as Hcodec
destruct block_facts_ h bo ro oo xo co Ha Ko nonempty_of_lengthxo 3 Lxo as _ & _ & _ & Vo
destruct block_facts_ h bs rs os ys cs Ha Ks nonempty_of_lengthys 7 Lys as _ & _ & _ & Vs
destruct block_facts_ h bsrc rsrc osrc ss [ ] Ha Ksr ltac:intros E ; rewrite E in Hn ; cbn in Hn ; lia as _ & _ & _ & Vsr
destruct LB.mbrtowc_returned_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hinv as res & → & Hres
rewrite proj2Z.eqb_neqn 0 ltac:lia in Hres
assert Hnl : 0 < n ≤ Z.of_natlengthss by lia
assert Hn0 : n ≠ 0 by lia
pose proof conv_of_result_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hres Haudit_ _ _ Hw Hcodec eq_transHerrno Herr Eout Est Haddr Lxo Vo Lys Vs Hnl Vsr as Hconv
destruct mbrtowc_frame_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hinv Hw Ha Hd Hr Ko Ks Ke Eout Est Herr Lxo Lco Lys Lcs Lxe Lce Hn0 as Ha′ & Hd′ & Hr′
assert Hlk : ∀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
{intros l v Hin
rewrite ! elem_of_app in Hin
destruct Hin as Hin | Hin | Hin ; auto
pose proof Kmbrtowc_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hinv Hlk Hw as Hw′
iMod pts_update_ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce block_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 with Hh [Ho Hs He] as [Hh Hn]
{rewrite ! fmap_app
rewrite block_ps_keysbo ro oo xo co ; | rewrite length_mem_bytes ; auto | rewrite length_mem_auxes ; auto
rewrite block_ps_keysbs rs os ys cs ; | rewrite length_mem_bytes ; auto | rewrite length_mem_auxes ; auto
rewrite block_ps_keysbe re oe xe ce ; | rewrite length_mem_bytes ; auto | rewrite length_mem_auxes ; auto
reflexivity
{rewrite ! pts_app
iFrame
iModIntro
iExists _
iSplit
{iPureIntro
unfold external_env
cbn
rewrite Z.mod_small ; reflexivity | exact proj1Hres
iSplitL Hh
+iExists _
iFrame Hh
iPureIntro
cbn [ ls_mem ls_rt ls_world ]
auto
+rewrite ! pts_app
iDestruct Hn as (Ho & Hs & He)
iApply HK $! res with [%] Hc Ho Hs He Hsr
rewrite ! length_mem_bytes ! length_mem_auxes
split ; exact Hconv |
repeat split

rpl_mbrtowc's triple

The genv links Hello, whose world interpretation keeps every lent string where lent_at says: hard_locale's premises (HelloLocale.v).

444Context Hlinked : hello_linkedge
444Context wi_lent : ∀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

setlocale's query, as hard_locale needs it.

449Context set_spec : contractlibc_world
449Context Hset : registryTAtom"setlocale" = Someset_spec
449Context Hset_ret : contract_returnsset_spec = RClassP
449Context Hset_abi : ∀d c v, contract_abiset_spec CResultd P ArgW c; ArgP v
449Context Hset_pre : ∀m w h k p t z, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → contract_preset_spec WIntk; WPtrz m w
449Context 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.invokeset_spec 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.

460Context Hstrlen : registryTAtom"strlen" = Somestrlen_contractlibc_world
460Context Hmemcpy : registryTAtom"memcpy" = Somememcpy_contractlibc_world
460Context 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, and an allocation.

466Context 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
466Context 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
466Context 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
466Context Kalloc : ∀q m wd h base, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Enter a block of rpl_mbrtowc.

482Ltac rm_enter s ≔
iApply wp_enter_ _ _ _ _ _ _ _ rpl_blocks ; vm_compute ; reflexivity | word_premise | ; iNext ; cbn [ b_insts b_jump rpl_block hblk ]

A pure instruction.

488Ltac rm_let  ≔
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ?m ; word_premise | ; iNext

rpl_mbrtowc from its block L11, where pr.1 is the output pointer out, whichever entry chose it: the call to mbrtowc, then the fallback outside a hard locale.

494Lemma rpl_tail
∀ pwc b8 b13 b15 out src n state bo ro oo xo co bs rs os ys cs be re oe xe ce bsrc rsrc osrc ss codec dq p t rc rp Φ
out = mkPtrbo + oo Objbo
state = mkPtrbs + os Objbs
errno = mkPtrbe + oe Objbe
ptr_capsrc = Objbsrc ∨ ptr_capsrc = Robsrc
ptr_addrsrc = bsrc + osrc
0 < bo
0 < bs
0 < bsrc
0 ≤ oo
0 ≤ osrc
bo + oo + 4 ≤ r_endro
bsrc + osrc + Z.of_natlengthss ≤ r_endrsrc
r_endro ≤ 2 ^ 48
r_endrsrc ≤ 2 ^ 48
bo + oo mod 4 = 0
bs + os mod 4 = 0
lengthxo = 4%nat
lengthco = 4%nat
lengthys = 8%nat
lengthcs = 8%nat
lengthxe = 4%nat
lengthce = 4%nat
0 < n ≤ Z.of_natlengthss
Forallλx ⇒ 0 ≤ x < 256 ss
validcodec ys
LL.lent0 p t −∗ SL.stringc_ptr 65824 rc c_bytes −∗ SL.stringposix_ptr 65856 rp posix_bytes −∗ pointstoPNamecodec_key dq VCodeccodec −∗ ptsblock_psbo ro oo xo co −∗ ptsblock_psbs rs os ys cs −∗ ptsblock_psbe re oe xe ce −∗ ptsblock_psbsrc rsrc osrc ss [ ] −∗ ▷∀r xo′ ys′ xe′ co′ cs′ ce′, ⌜rpl_resultvalid auditcodec = SomeCodecC codec n ss xo ys xo′ ys′ xe′ r ∧ lengthxo′ = 4%nat ∧ lengthys′ = 8%nat ∧ lengthxe′ = 4%nat ∧ lengthco′ = 4%nat ∧ lengthcs′ = 8%nat ∧ lengthce′ = 4%nat⌝ −∗ SL.stringc_ptr 65824 rc c_bytes −∗ SL.stringposix_ptr 65856 rp posix_bytes −∗ pointstoPNamecodec_key dq VCodeccodec −∗ ptsblock_psbo ro oo xo′ co′ −∗ ptsblock_psbs rs os ys′ cs′ −∗ ptsblock_psbe re oe xe′ ce′ −∗ ptsblock_psbsrc rsrc osrc ss [ ] −∗ ΦRetWIntr −∗ WPERunmkFramerpl_fn putTAtom"pr.1" WPtrout putTAtom"v15" b15 putTAtom"v13" b13 putTAtom"v8" b8 TAtom"v6", WPtrstate; TAtom"v4", WIntn; TAtom"v2", WPtrsrc; TAtom"v0", pwc [ ] None ExecTAtom"L11" b_instsrpl_block"L11" b_jumprpl_block"L11" : cexpr {Φ}
Proof 119 steps Qed
intros Eout Est Herr Hcap Haddr Hbo Hbs Hbsrc Hoo Hosrc Heo Hesrc Ho48 Hs48 Hoal Hsal Lxo Lco Lys Lcs Lxe Lce Hn Hss Hval
iIntros #Hk Hc Hposix Hcod HBo HBs HBe HBsrc HΦ
assert Hn64 : n mod 2 ^ 64 = n by apply Z.mod_small ; lia
pose proof Hlinked as Hm & _ & Hext
cbn [ b_insts b_jump rpl_block hblk ]
iApply wp_mbrtowc with Hcod HBo HBs HBe HBsrc ; apply hello_outside ; exact Hm | reflexivity | apply Hext ; reflexivity | word_premise | word_premise | word_premise | word_premise | exact Eout | exact Est | exact Herr | exact Hcap | exact Haddr | exact Hbo | exact Hbs | exact Hbsrc | exact Hoal | exact Hsal | exact Lxo | exact Lco | exact Lys | exact Lcs | exact Lxe | exact Lce | rewrite Hn64 ; exact Hn | exact Hss | exact Hval |
iNext
iIntros res xo1 ys1 xe1 co1 cs1 ce1 Hconv & Lxo1 & Lys1 & Lxe1 & Lco1 & Lcs1 & Lce1 Hcod HBo HBs HBe HBsrc
rewrite Hn64 in Hconv
destruct conv_result_range_ _ _ _ _ _ _ _ _ _ _ Hconv as Hres Hkeep
destruct Z.le_gt_cases2 ^ 64 − 2 res as Hge | Hlt

An invalid or incomplete sequence.

–rm_let
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
rm_enter "L29"
rm_let
iApply wp_goto
iNext
rm_enter "L30"
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
rm_enter "L35"
iApply wp_call_bind_ _ _ _ _ _ _ _ _ _ _ _ _ hard_locale_fn invocationhard_locale_fn WInt0 ; word_premise | unfold find_fn ; rewrite Hm ; vm_compute ; reflexivity | reflexivity |
iNext
iApply HLo.hard_locale_specregistry wi ge Hlinked wi_lent set_spec Hset Hset_ret Hset_abi Hset_pre Hset_query Hstrlen Hmemcpy Kcopy Kbyte Kalloc Hstrcmp with Hk Hc Hposix ; lia |
iNext
iIntros hr Hc Hposix
iExists _
iSplit ; iPureIntro ; reflexivity |
iNext
cbn [ fr_fn fr_env fr_locals fr_doomed fr_at ]
rm_let
rm_let
iApply wp_goto
iNext
rm_enter "L36"
iApply wp_branch ; word_premise |
iNext
lazymatch goal with|- context [if ?t then 1 else 0]⇒destruct tend
all: change 1 mod 2 ^ 32 with 1 ; change 0 mod 2 ^ 32 with 0 ; cbn [ Z.eqb edge_label ]

Not a hard locale: the first byte stands for itself.

+rm_enter "L22"
destruct ss as | x0 ss′ ; cbn in Hn ; lia |
pose proof Forall_invHss as Hx0
cbv beta in Hx0
iEval rewrite / block_ps ; rewrite / pts big_sepL_cons big_sepL_app byte_ps_cons big_sepL_cons in HBsrc
iEval rewrite / block_ps ; rewrite / pts big_sepL_cons big_sepL_app in HBo
iDestruct HBsrc as (Hls & (Hb0 & Hbs) & Has)
iDestruct HBo as (Hlo & Hbo & Hao)
iAssert livebsrc rsrc with [Hls] as Hls ; rewrite / live / pts big_sepL_singleton ; iExact Hls |
iAssert ibytebsrc osrc x0 with [Hb0] as Hb0 ; rewrite / ibyte / pts big_sepL_singleton ; iExact Hb0 |
iAssert livebo ro with [Hlo] as Hlo ; rewrite / live / pts big_sepL_singleton ; iExact Hlo |
iAssert bytesbo oo xo1 with [Hbo] as Hbo ; rewrite / bytes / pts ; iExact Hbo |
iApply wp_check_read with Hls ; reflexivity | word_premise | exact Hcap | rewrite Haddr ; addr_premise | rewrite Haddr ; cbn [ length ] in Hesrc ; addr_premise | apply Z.mod_1_r |
iNext
iIntros Hls
gen_env
iApply wp_raw_load_byte with Hls Hb0 ; reflexivity | word_premise | reflexivity | reflexivity | exact Hcap | rewrite Haddr ; addr_premise |
iNext
iIntros Hls Hb0
gen_env
iApply wp_let_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ WIntx0 ; reflexivity | reflexivity | word_premise | intros m′ ; cbn ; rewrite Zmod_modsign_extension256 128 x0 2 ^ 32 ; exact f_equalλz ⇒ SomeOpResRValWIntz m' ub_of_sbx0 Hx0 |
iNext
gen_env
iApply wp_check with Hlo ; reflexivity | word_premise | rewrite Eout ; reflexivity | rewrite Eout ; addr_premise | rewrite Eout ; addr_premise | apply Z.mod_1_r |
iNext
iIntros Hlo
gen_env
iApply wp_raw_store_w with Hlo Hbo ; word_premise | word_premise | rewrite Eout ; reflexivity | rewrite Eout ; addr_premise | exact Lxo1 | intros m′ wd h Hl Hw ; exact Kstore_ _ _ _ _ _ _ _ Hl Hw |
iNext
iIntros Hlo Hbo
assert Hx32 : x0 mod 2 ^ 32 = x0 by apply Z.mod_small ; lia
iEval rewriteHx32 in Hbo
iApply wp_ret ; reflexivity | reflexivity |
iNext
iApply HΦ $! 1 le_bytesx0 4 ys1 xe1 co1 cs1 ce1 with [%] Hc Hposix Hcod [Hlo Hbo Hao] HBs HBe [Hls Hb0 Hbs Has]
∗split ; | rewrite length_le_bytes ; repeat split ; first assumption | reflexivity
right
split ; reflexivity |
split
{exists res
split ; exact Hge |
rewrite HkeepHge in Hconv
exact Hconv
exists x0
split ; reflexivity
∗rewrite / block_ps / pts big_sepL_cons big_sepL_app
rewrite / live / bytes / pts big_sepL_singleton
iFrame
∗rewrite / block_ps / pts big_sepL_cons big_sepL_app byte_ps_cons big_sepL_cons
rewrite / live / ibyte / pts ! big_sepL_singleton
iFrame

A hard locale: mbrtowc's answer.

+rm_enter "L24"
iApply wp_ret ; reflexivity | word_premise |
iNext
rewrite Z.mod_smallres 2 ^ 64 ; | lia
iApply HΦ $! res xo1 ys1 xe1 co1 cs1 ce1 with [%] Hc Hposix Hcod HBo HBs HBe HBsrc
split ; left ; exact Hconv |
repeat split ; assumption

A character, a NUL or nothing to stand for: mbrtowc's answer.

–rm_let
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
rm_enter "L30"
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
rm_enter "L36"
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
rm_enter "L24"
iApply wp_ret ; reflexivity | word_premise |
iNext
rewrite Z.mod_smallres 2 ^ 64 ; | lia
iApply HΦ $! res xo1 ys1 xe1 co1 cs1 ce1 with [%] Hc Hposix Hcod HBo HBs HBe HBsrc
split ; left ; exact Hconv |
repeat split ; assumption

rpl_mbrtowc(out, src, n, state) for a non-null out, from wp_mbrtowc and HelloLocale.v's hard_locale_spec: owning the output, state and errno blocks, the source's n bytes or more, the codec piece, the literals "C" and "POSIX", and the name of LC_CTYPE (category 0) lent, the call returns what rpl_result says, and hands every block back.

620Lemma rpl_mbrtowc_spec
∀ out src n state bo ro oo xo co bs rs os ys cs be re oe xe ce bsrc rsrc osrc ss codec dq p t rc rp Φ
out = mkPtrbo + oo Objbo
state = mkPtrbs + os Objbs
errno = mkPtrbe + oe Objbe
ptr_capsrc = Objbsrc ∨ ptr_capsrc = Robsrc
ptr_addrsrc = bsrc + osrc
0 < bo
0 < bs
0 < bsrc
0 ≤ oo
0 ≤ osrc
bo + oo + 4 ≤ r_endro
bsrc + osrc + Z.of_natlengthss ≤ r_endrsrc
r_endro ≤ 2 ^ 48
r_endrsrc ≤ 2 ^ 48
bo + oo mod 4 = 0
bs + os mod 4 = 0
lengthxo = 4%nat
lengthco = 4%nat
lengthys = 8%nat
lengthcs = 8%nat
lengthxe = 4%nat
lengthce = 4%nat
0 < n ≤ Z.of_natlengthss
Forallλx ⇒ 0 ≤ x < 256 ss
validcodec ys
LL.lent0 p t −∗ SL.stringc_ptr 65824 rc c_bytes −∗ SL.stringposix_ptr 65856 rp posix_bytes −∗ pointstoPNamecodec_key dq VCodeccodec −∗ ptsblock_psbo ro oo xo co −∗ ptsblock_psbs rs os ys cs −∗ ptsblock_psbe re oe xe ce −∗ ptsblock_psbsrc rsrc osrc ss [ ] −∗ ▷∀r xo′ ys′ xe′ co′ cs′ ce′, ⌜rpl_resultvalid auditcodec = SomeCodecC codec n ss xo ys xo′ ys′ xe′ r ∧ lengthxo′ = 4%nat ∧ lengthys′ = 8%nat ∧ lengthxe′ = 4%nat ∧ lengthco′ = 4%nat ∧ lengthcs′ = 8%nat ∧ lengthce′ = 4%nat⌝ −∗ SL.stringc_ptr 65824 rc c_bytes −∗ SL.stringposix_ptr 65856 rp posix_bytes −∗ pointstoPNamecodec_key dq VCodeccodec −∗ ptsblock_psbo ro oo xo′ co′ −∗ ptsblock_psbs rs os ys′ cs′ −∗ ptsblock_psbe re oe xe′ ce′ −∗ ptsblock_psbsrc rsrc osrc ss [ ] −∗ ΦRetWIntr −∗ WPERuninvocationrpl_fn WPtrout; WPtrsrc; WIntn; WPtrstate : cexpr {Φ}
Proof 17 steps Qed
intros Eout Est Herr Hcap Haddr Hbo Hbs Hbsrc Hoo Hosrc Heo Hesrc Ho48 Hs48 Hoal Hsal Lxo Lco Lys Lcs Lxe Lce Hn Hss Hval
iIntros #Hk Hc Hposix Hcod HBo HBs HBe HBsrc HΦ
rewrite rpl_entry
rm_enter "start"
iApply wp_alloc_ _ _ _ _ _ _ _ _ _ _ _ _ 4 ; reflexivity | lia | unfold max_allocation_size ; lia | intros m wd h base Hf Hw ; exact Kalloc_ _ _ _ _ Hf Hw |
iNext
iIntros base _ _
rm_let
rm_let
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; subst out ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
rm_enter "L10"
iApply wp_goto
iNext
rm_enter "L11"
iApply rpl_tail with Hk Hc Hposix Hcod HBo HBs HBe HBsrc HΦ ; assumption

rpl_mbsrtowcs's window

The memchr contract, for strnlen1.

661Context Hmemchr : registryTAtom"memchr" = Somememchr_contractlibc_world

Enter a block of rpl_mbsrtowcs.

664Ltac ms_enter s ≔
iApply wp_enter_ _ _ _ _ _ _ _ mbs_blocks ; vm_compute ; reflexivity | word_premise | ; iNext ; cbn [ b_insts b_jump mbs_block hblk ]

Read byte k of the window in block blk, after the first: a flight to q + k, a half check against the first check, a load and its test. Leaves the branch on the test, with the byte named x.

672Ltac mid_read blk q bs k Hc x Hx Hxr Hz Hn Hbs ≔
ms_enter blk ; iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ ptr_addrq + Z.of_natk ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise | ; iNext ; gen_env ; destruct lookup_lt_is_Some_2bs ++ 0 k as x Hx ; rewrite length_app ; cbn ; lia | ; destruct nul_index_ _ _ Hbs Hx as Hxr & Hz & Hn ; iDestruct string_byte_ _ _ _ k x with Hs as (_ & Hl & Hb & Hk) ; exact Hx | ; iApply wp_half_check_read with Hl ; reflexivity | word_premise | reflexivity | exact Hc | addr_premise | addr_premise | lia | lia | apply Z.mod_1_r | ; iNext ; iIntros Hl ; gen_env ; iApply wp_raw_load_byte with Hl Hb ; reflexivity | word_premise | reflexivity | reflexivity | exact Hc | addr_premise | ; iNext ; iIntros Hl Hb ; iDestruct Hk with Hl Hb as Hs ; gen_env ; iApply wp_let ; reflexivity | reflexivity | word_premise | intros ?m ; word_premise | ; iNext ; gen_env

The temporaries the converting loop keeps, and their values: the destination cursor, the source cursor, the count left, the state, srcp, its check, and the destination's address.

691Definition mbs_varse : env q : ptr dst len st sp c0 d0 : word : Prop ≔
lookupTAtom"pr.5" e = SomeWPtrq ∧ lookupTAtom"pr.7" e = Somedst ∧ lookupTAtom"pr.1" e = Somelen ∧ lookupTAtom"pr.2" e = Somest ∧ lookupTAtom"v2" e = Somesp ∧ lookupTAtom"chk0" e = Somec0 ∧ lookupTAtom"v23" e = Somed0

End the window at L37, with the window's length n in pr.8.

698Ltac close_window L ≔
ms_enter "L37" ; gen_env ; iApply HK with [%] Hs ; split ; repeat split ; assumption | ;match goal withH : lookupTAtom"pr.8" _ = Some_ |- _⇒rewrite Hend;rewrite <- L;reflexivity

rpl_mbsrtowcs's window, blocks L29 to L57: with the source cursor q at a string bs, the loop reads up to four bytes, stopping at the NUL, and then asks strnlen1 for at most 12 more; pr.8 is then min(len + 1, 16), and the loop's other temporaries are as they were.

709Lemma mbs_window
∀ e q dst len st sp c0 d0 b reg bs Φ
mbs_varse q dst len st sp c0 d0
SL.stringq b reg bs −∗ ▷∀e′, ⌜mbs_varse′ q dst len st sp c0 d0 ∧ lookupTAtom"pr.8" e′ = SomeWIntZ.minZ.of_natlengthbs + 1 16⌝ −∗ SL.stringq b reg bs −∗ WPERunmkFramembs_fn e′ [ ] None ExecTAtom"L37" b_instsmbs_block"L37" b_jumpmbs_block"L37" : cexpr {Φ} −∗ WPERunmkFramembs_fn e [ ] None ExecTAtom"L29" b_instsmbs_block"L29" b_jumpmbs_block"L29" : cexpr {Φ}
Proof 119 steps Qed
intros Hq & H7 & H1 & H2 & Hv2 & Hc0 & H23
iIntros Hs HK
iDestruct Hs as [%Hok Hps]
iAssert SL.stringq b reg bs with [$Hps] as Hs ; done |
pose proof Hok as Hc & Hb0 & Hbq & Hend & H48 & Hbs
pose proof Hm := proj1Hlinked
cbn [ b_insts b_jump mbs_block hblk ]

The first byte, through a check.

destruct lookup_lt_is_Some_2bs ++ 0 0 as x0 Hx0 ; rewrite length_app ; cbn ; lia |
destruct nul_index_ _ _ Hbs Hx0 as Hx0r & Hz0 & Hn0
iDestruct string_byte_ _ _ _ 0 x0 with Hs as (_ & Hl & Hb & Hk) ; exact Hx0 |
iApply wp_check_read with Hl ; reflexivity | word_premise | exact Hc | addr_premise | addr_premise | apply Z.mod_1_r |
iNext
iIntros Hl
gen_env
iApply wp_raw_load_byte with Hl Hb ; reflexivity | word_premise | reflexivity | reflexivity | exact Hc | addr_premise |
iNext
iIntros Hl Hb
iDestruct Hk with Hl Hb as Hs
gen_env
iApply wp_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise |
iNext
gen_env
destruct Z.eqb_specx0 0 as E0 | E0
{subst x0
The NUL first: a window of one byte.
pose proof Hz0eq_refl as L0
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
close_window L0
pose proof Hn0E0 as L0
match goal withH : lookupTAtom"v41" _ = _ |- _⇒rewrite sb_nex0 in H ; | liaend
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]

The second byte.

ms_enter "L36"
iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ ptr_addrq + Z.of_nat1 ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |
iNext
gen_env
destruct lookup_lt_is_Some_2bs ++ 0 1 as x1 Hx1 ; rewrite length_app ; cbn ; lia |
destruct nul_index_ _ _ Hbs Hx1 as Hx1r & Hz1 & Hn1
iDestruct string_byte_ _ _ _ 1 x1 with Hs as (_ & Hl & Hb & Hk) ; exact Hx1 |
iApply wp_half_check_read with Hl ; reflexivity | word_premise | reflexivity | exact Hc | addr_premise | addr_premise | lia | lia | apply Z.mod_1_r |
iNext
iIntros Hl
gen_env
iApply wp_raw_load_byte with Hl Hb ; reflexivity | word_premise | reflexivity | reflexivity | exact Hc | addr_premise |
iNext
iIntros Hl Hb
iDestruct Hk with Hl Hb as Hs
gen_env
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ?m ; word_premise |
iNext
gen_env
destruct Z.eqb_specx1 0 as E1 | E1
{subst x1
pose proof Hz1eq_refl as L1
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
close_window L1
pose proof Hn1E1 as L1
match goal withH : lookupTAtom"v48" _ = _ |- _⇒rewrite sb_nex1 in H ; | liaend
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]

The third byte.

mid_read "L43" q bs 2%nat Hc x2 Hx2 Hx2r Hz2 Hn2 Hbs
destruct Z.eqb_specx2 0 as E2 | E2
{subst x2
pose proof Hz2eq_refl as L2
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
close_window L2
pose proof Hn2E2 as L2
match goal withH : lookupTAtom"v55" _ = _ |- _⇒rewrite sb_nex2 in H ; | liaend
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]

The fourth byte.

mid_read "L60" q bs 3%nat Hc x3 Hx3 Hx3r Hz3 Hn3 Hbs
destruct Z.eqb_specx3 0 as E3 | E3
{subst x3
pose proof Hz3eq_refl as L3
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
close_window L3
pose proof Hn3E3 as L3
match goal withH : lookupTAtom"v65" _ = _ |- _⇒rewrite sb_nex3 in H ; | liaend
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]

Four bytes before the NUL: strnlen1 counts the rest, up to 12.

ms_enter "L57"
iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ ptr_addrq + Z.of_nat4 ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |
iNext
gen_env
iDestruct string_suffix_ _ _ _ 4 with Hs as [Hs4 Hback] ; lia |
iApply wp_call_bind_ _ _ _ _ _ _ _ _ _ _ _ _ strnlen1_fn invocationstrnlen1_fn WPtrmkPtrptr_addrq + Z.of_nat4 ptr_capq; WInt12 ; word_premise | unfold find_fn ; rewrite Hm ; vm_compute ; reflexivity | reflexivity |
iNext
iApply HL.strnlen1_specregistry wi ge Hlinked with Hs4 ; exact Hmemchr | lia |
iNext
iIntros Hs4
iDestruct Hback with Hs4 as Hs
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
iApply wp_goto
iNext
ms_enter "L37"
gen_env
iApply HK with [%] Hs
split ; repeat split ; assumption |
match goal withH : lookupTAtom"pr.8" _ = Some_ |- _⇒rewrite Hend
rewrite length_drop
rewrite window_min ; reflexivity | lia

A string's pieces are a block from its offset: its life and its bytes with the NUL, and no aux slots.

801Lemma string_block
∀ q b reg bs
SL.stringq b reg bs ⊣⊢ ⌜string_okq b reg bs⌝ ∗ ptsblock_psb reg ptr_addrq − b bs ++ 0 [ ]
Explore proof 4 tactics

Initial goal

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
ptr
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, 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
Hlinked :
hello_linkedge
wi_lent :
∀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
set_spec :
contractlibc_world
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_abi :
∀d : name c v : value, contract_abiset_spec CResultd P ArgW c; ArgP v
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → contract_preset_spec WIntk; WPtrz m w
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, 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
Kbyte :
∀b : Z reg : region o x y : Z m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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
Kstore :
∀b : Z reg : region o : Z xs : listZ y : Z m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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
Kalloc :
∀q : alloc_req m : mem wd : libc_world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
q :
ptr
b :
Z
reg :
region
bs :
listZ
⊢
SL.stringq b reg bs ⊣⊢ ⌜string_okq b reg bs⌝ ∗ ptsblock_psb reg ptr_addrq − b bs ++ 0 [ ]

rewrite / SL.string / string_ps / block_ps

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
ptr
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, 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
Hlinked :
hello_linkedge
wi_lent :
∀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
set_spec :
contractlibc_world
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_abi :
∀d : name c v : value, contract_abiset_spec CResultd P ArgW c; ArgP v
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → contract_preset_spec WIntk; WPtrz m w
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, 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
Kbyte :
∀b : Z reg : region o x y : Z m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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
Kstore :
∀b : Z reg : region o : Z xs : listZ y : Z m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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
Kalloc :
∀q : alloc_req m : mem wd : libc_world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
q :
ptr
b :
Z
reg :
region
bs :
listZ
⊢
⌜string_okq b reg bs⌝ ∗ ptsPLiveb, VLivereg :: byte_psb ptr_addrq − b bs ++ 0 ⊣⊢ ⌜string_okq b reg bs⌝ ∗ ptsPLiveb, VLivereg :: byte_psb ptr_addrq − b bs ++ 0 ++ aux_psb ptr_addrq − b [ ]

cbn [ aux_ps ]

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
ptr
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, 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
Hlinked :
hello_linkedge
wi_lent :
∀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
set_spec :
contractlibc_world
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_abi :
∀d : name c v : value, contract_abiset_spec CResultd P ArgW c; ArgP v
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → contract_preset_spec WIntk; WPtrz m w
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, 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
Kbyte :
∀b : Z reg : region o x y : Z m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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
Kstore :
∀b : Z reg : region o : Z xs : listZ y : Z m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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
Kalloc :
∀q : alloc_req m : mem wd : libc_world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
q :
ptr
b :
Z
reg :
region
bs :
listZ
⊢
⌜string_okq b reg bs⌝ ∗ ptsPLiveb, VLivereg :: byte_psb ptr_addrq − b bs ++ 0 ⊣⊢ ⌜string_okq b reg bs⌝ ∗ ptsPLiveb, VLivereg :: byte_psb ptr_addrq − b bs ++ 0 ++ aux_psb ptr_addrq − b [ ]

rewrite app_nil_r

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
ptr
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, 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
Hlinked :
hello_linkedge
wi_lent :
∀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
set_spec :
contractlibc_world
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_abi :
∀d : name c v : value, contract_abiset_spec CResultd P ArgW c; ArgP v
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → contract_preset_spec WIntk; WPtrz m w
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, 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
Kbyte :
∀b : Z reg : region o x y : Z m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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
Kstore :
∀b : Z reg : region o : Z xs : listZ y : Z m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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
Kalloc :
∀q : alloc_req m : mem wd : libc_world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
q :
ptr
b :
Z
reg :
region
bs :
listZ
⊢
⌜string_okq b reg bs⌝ ∗ ptsPLiveb, VLivereg :: byte_psb ptr_addrq − b bs ++ 0 ⊣⊢ ⌜string_okq b reg bs⌝ ∗ ptsPLiveb, VLivereg :: byte_psb ptr_addrq − b bs ++ 0

done

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
rewrite / SL.string / string_ps / block_ps
cbn [ aux_ps ]
rewrite app_nil_r
done

An object's life, bytes and aux slots from offset o are its block from o.

807Lemma dest_block
∀ b reg o xs cs
liveb reg ∗ bytesb o xs ∗ auxesb o cs ⊣⊢ ptsblock_psb reg o xs cs
Explore proof 2 tactics

Initial goal

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
ptr
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, 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
Hlinked :
hello_linkedge
wi_lent :
∀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
set_spec :
contractlibc_world
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_abi :
∀d : name c v : value, contract_abiset_spec CResultd P ArgW c; ArgP v
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → contract_preset_spec WIntk; WPtrz m w
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, 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
Kbyte :
∀b : Z reg : region o x y : Z m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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
Kstore :
∀b : Z reg : region o : Z xs : listZ y : Z m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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
Kalloc :
∀q : alloc_req m : mem wd : libc_world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
b :
Z
reg :
region
o :
Z
xs :
listZ
cs :
listcap
⊢
liveb reg ∗ bytesb o xs ∗ auxesb o cs ⊣⊢ ptsblock_psb reg o xs cs

rewrite / block_ps / pts big_sepL_cons big_sepL_app / live / bytes / auxes / pts big_sepL_singleton

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
ptr
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, 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
Hlinked :
hello_linkedge
wi_lent :
∀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
set_spec :
contractlibc_world
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_abi :
∀d : name c v : value, contract_abiset_spec CResultd P ArgW c; ArgP v
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → contract_preset_spec WIntk; WPtrz m w
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, 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
Kbyte :
∀b : Z reg : region o x y : Z m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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
Kstore :
∀b : Z reg : region o : Z xs : listZ y : Z m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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
Kalloc :
∀q : alloc_req m : mem wd : libc_world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
b :
Z
reg :
region
o :
Z
xs :
listZ
cs :
listcap
⊢
pointstoPLiveb, VLivereg.1 DfracOwn1 PLiveb, VLivereg.2 ∗ ∗lv∈byte_psb o xspointstolv.1 DfracOwn1 lv.2 ∗ ∗lv∈aux_psb o cspointstolv.1 DfracOwn1 lv.2 ⊣⊢ pointstoPLiveb, VLivereg.1 DfracOwn1 PLiveb, VLivereg.2 ∗ ∗y∈byte_psb o xspointstoy.1 DfracOwn1 y.2 ∗ ∗y∈aux_psb o cspointstoy.1 DfracOwn1 y.2

done

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
rewrite / block_ps / pts big_sepL_cons big_sepL_app / live / bytes / auxes / pts big_sepL_singleton
done

errno's lookup has Campaign 4's contract.

811Context Herrno_reg : registryTAtom"__errno_location" = SomeLB.errno_contractrep

The world interpretation survives a pointer store into a cell the program owns.

815Context 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

__errno_location() returns the errno cell and changes nothing: HelloClose.v's wp_close_errno over libc_world. A local rule, for promotion to a libc logic module.

825Lemma wp_conv_errno
∀ f e ls lab d rest j Φ
▷WPERunmkFramef putd WPtrerrno e ls None Execlab rest j : cexpr {Φ} −∗ WPERunmkFramef e ls None Execlab CallCResultd P GlobalTAtom"__errno_location" [ ] :: rest j : cexpr {Φ}
Proof 30 steps Qed
iIntros HK
iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ LB.errno_contractrep [ ] True%I with [] [HK]
–apply linked_outside ; exact Hlinked | reflexivity
–apply linked_unbound ; exact Hlinked | reflexivity
–reflexivity
–exact Herrno_reg
–reflexivity
–split ; right ; eexists ; reflexivity | reflexivity
–iIntros σ Hσ _
iDestruct Hσ as h [_ %Hσ]
destruct Hlibc_ _ _ proj2proj2proj2Hσ as Hr & _
iPureIntro
split ; reflexivity |
split ; exact Hr | exact proj1proj2proj2proj2Hr
–done
–iNext
iIntros σ tr vs s′ m′ w′ Hi Hσ _
destruct LB.errno_exact_ _ _ _ _ _ _ _ _ _ _ _ Hi as → & → & → & → & He
injection He as →
iDestruct Hσ as h [Hh %Hσ]
destruct Hlibc_ _ _ proj2proj2proj2Hσ as _ & _ & Ec & _
iModIntro
iExists _
iSplit
+iPureIntro
cbn [ external_env external_outcome contract_returns site_result returned_env ]
rewrite Ec
reflexivity
+iSplitL Hh ; iExists h ; iFrame ; done |
iExact HK

What rpl_mbsrtowcs's caller learns when it returns r, with dest's final bytes ws, errno's bytes xe and the length l of the source: EILSEQ, -1 with 84 in errno; or r wide characters, none zero, then a zero one.

857Definition mbs_postl : nat r : Z ws xe : listZ : Prop ≔
r = 2 ^ 64 − 1 ∧ le_valuexe = 84 ∨ ∃k : nat, r = Z.of_natk ∧ k ≤ l%nat ∧ wide_oktake4 × k ws ∧ le_valuetake4 drop4 × k ws = 0

rpl_mbsrtowcs's converting loop, from block L28, by Löb induction: after i wide characters from the first j bytes of the string at p, with the state valid and in its initial shift state, every path returns what mbs_post says; the abort after an incomplete sequence is never reached.

867Lemma mbs_loop
∀ p b reg bs bd rd sb sr so be re oe spb spr spo codec dq p0 t0 rc rp Φ
errno = mkPtrbe + oe Objbe
0 < bd
bd mod 4 = 0
bd + 4 × Z.of_natlengthbs + 1 ≤ r_endrd
r_endrd ≤ 2 ^ 48
0 < sb
sb + so mod 4 = 0
0 < spb
0 ≤ spo
spb + spo mod 8 = 0
spb + spo + 8 ≤ r_endspr
r_endspr ≤ 2 ^ 48
0 < be
0 ≤ oe
be + oe + 4 ≤ r_endre
r_endre ≤ 2 ^ 48
⊢ ∀e i j : nat wpre cpre wrest crest ys cs xe ce x, ⌜mbs_varse mkPtrptr_addrp + Z.of_natj ptr_capp WPtrmkPtrbd + Z.of_nat4 × i Objbd WIntZ.of_natlengthbs + 1 − Z.of_nati WPtrmkPtrsb + so Objsb WPtrmkPtrspb + spo Objspb WPtrmkPtrspb + spo Objspb WIntbd ∧ i ≤ j ≤ lengthbs%nat ∧ lengthwpre = 4 × i%nat ∧ lengthcpre = 4 × i%nat ∧ lengthwrest = 4 × lengthbs + 1 − i%nat ∧ lengthcrest = 4 × lengthbs + 1 − i%nat ∧ wide_okwpre ∧ validcodec ys ∧ le_valuetake4 ys = 0 ∧ lengthys = 8%nat ∧ lengthcs = 8%nat ∧ lengthxe = 4%nat ∧ lengthce = 4%nat⌝ −∗ LL.lent0 p0 t0 −∗ SL.stringc_ptr 65824 rc c_bytes −∗ SL.stringposix_ptr 65856 rp posix_bytes −∗ pointstoPNamecodec_key dq VCodeccodec −∗ SL.stringp b reg bs −∗ livebd rd −∗ bytesbd 0 wpre −∗ auxesbd 0 cpre −∗ bytesbd Z.of_nat4 × i wrest −∗ auxesbd Z.of_nat4 × i crest −∗ ptsblock_pssb sr so ys cs −∗ ptsblock_psbe re oe xe ce −∗ livespb spr −∗ pcellspb spo x −∗ ∀r ws cws ys′ cs′ xe′ ce′ x′, ⌜mbs_postlengthbs r ws xe′ ∧ lengthws = 4 × lengthbs + 1%nat ∧ lengthxe′ = 4%nat⌝ −∗ SL.stringc_ptr 65824 rc c_bytes −∗ SL.stringposix_ptr 65856 rp posix_bytes −∗ pointstoPNamecodec_key dq VCodeccodec −∗ SL.stringp b reg bs −∗ livebd rd −∗ bytesbd 0 ws −∗ auxesbd 0 cws −∗ ptsblock_pssb sr so ys′ cs′ −∗ ptsblock_psbe re oe xe′ ce′ −∗ livespb spr −∗ pcellspb spo x′ −∗ ΦRetWIntr −∗ WPERunmkFramembs_fn e [ ] None ExecTAtom"L28" b_instsmbs_block"L28" b_jumpmbs_block"L28" : cexpr {Φ}
Proof 188 steps Qed
intros Herr Hbd Hbd4 Hdend Hd48 Hsb Hsal Hspb Hspo Hspal Hspend Hsp48 Hbe Hoe Heend He48
pose proof Hlinked as Hm & _ & Hext
iLöb as IH
iIntros e i j wpre cpre wrest crest ys cs xe ce x Hq & H7 & H1 & H2 & Hv2 & Hc0 & H23 & Hij & Lwp & Lcp & Lwr & Lcr & Hwide & Hval & Hinit & Lys & Lcs & Lxe & Lce #Hk Hc Hposix Hcod Hs Hdl Hdw Hda Hrw Hra HBs HBe Hspl Hsp HΦ
iDestruct Hs as [%Hok Hps]
iAssert SL.stringp b reg bs with [$Hps] as Hs ; done |
pose proof Hok as Hc & Hb0 & Hbp & Hsend & H48 & Hbs
cbn [ b_insts b_jump mbs_block hblk ]

Characters are left to write.

iApply wp_let ; reflexivity | reflexivity | word_premise | intros ?m ; word_premise |
iNext
gen_env
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
ms_enter "L29"

The window over the suffix from byte j.

iDestruct string_suffix_ _ _ _ j with Hs as [Hsuf Hback] ; lia |
iApply mbs_window with Hsuf ; repeat split ; eassumption |
iNext
iIntros e′ Hq′ & H7′ & H1′ & H2′ & Hv2′ & Hc0′ & H23′ & Hn8 Hsuf

The next output word, and the source as a block.

assert Lr4 : 4 ≤ lengthwrest%nat by lia
assert Lc4 : 4 ≤ lengthcrest%nat by lia
iEval rewritebytes_take_drop_ _ _ 4 Lr4 in Hrw
iDestruct Hrw as [Hw0 Hw1]
iEval rewriteauxes_take_drop_ _ _ 4 Lc4 in Hra
iDestruct Hra as [Ha0 Ha1]
iAssert ptsblock_psbd rd Z.of_nat4 × i take4 wrest take4 crest with [Hdl Hw0 Ha0] as HBo ; rewrite - dest_block ; iFrame |
iEval rewritestring_block in Hsuf
iDestruct Hsuf as [%Hok′ HBsrc]
iApply wp_call_bind_ _ _ _ _ _ _ _ _ _ _ _ _ rpl_fn invocationrpl_fn WPtrmkPtrbd + Z.of_nat4 × i Objbd; WPtrmkPtrptr_addrp + Z.of_natj ptr_capp; WIntZ.minZ.of_natlengthdropj bs + 1 16; WPtrmkPtrsb + so Objsb ; word_premise | unfold find_fn ; rewrite Hm ; vm_compute ; reflexivity | reflexivity |
iNext
pose proof Hok' as Hc′ & _ & Hbq′ & Hsend′ & _ & Hbs′
assert Hal : bd + Z.of_nat4 × i mod 4 = 0
{replace bd + Z.of_nat4 × i with bd + Z.of_nati × 4 by lia
rewrite Z.mod_add ; exact Hbd4 | lia
assert Hss : Forallλx ⇒ 0 ≤ x < 256 dropj bs ++ 0
{apply Forall_app
split ; | repeat constructor ; lia
apply Forall_drop
eapply Forall_impl ; exact Hbs | intros y Hy ; cbv beta in Hy |- * ; lia
iApply rpl_mbrtowc_spec_ _ _ _ bd rd Z.of_nat4 × i take4 wrest take4 crest sb sr so ys cs be re oe xe ce b reg ptr_addrp + Z.of_natj − b dropj bs ++ 0 with Hk Hc Hposix Hcod HBo HBs HBe [HBsrc]
all: try first reflexivity | assumption | exact Herr | lia | cbn [ ptr_addr ptr_cap ] ; lia | rewrite length_take ; lia | rewrite length_app length_drop ; cbn [ length ] ; lia
{iEval cbnptr_addr in HBsrc
iExact HBsrc
iNext
iIntros r xo′ ys′ xe′ co′ cs′ ce′ Hres & Lxo′ & Lys′ & Lxe′ & Lco′ & Lcs′ & Lce′ Hc Hposix Hcod HBo HBs HBe HBsrc
iExists _
iSplit ; iPureIntro ; reflexivity |
iNext
cbn [ fr_fn fr_env fr_locals fr_doomed fr_at ]
gen_env
iDestruct Hback with [HBsrc] as Hs
{iApply string_block
iSplit ; done |
iEval cbnptr_addr in HBsrc
iExact HBsrc
destruct rpl_step_ _ _ dropj bs _ _ _ _ _ _ Forall_drop_ _ _ Hbs Hval Hinit Hres as Hr64 & Hn2 & Hm1 & Hz & Hpos
iEval rewrite − dest_block in HBo
iDestruct HBo as (Hdl & Hw0 & Ha0)

Never incomplete: the abort is not reached.

iApply wp_let ; reflexivity | reflexivity | word_premise | intros ?m ; word_premise |
iNext
gen_env
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
ms_enter "L82"
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ?m ; word_premise |
iNext
gen_env
destruct Z.eqb_specr 2 ^ 64 − 1 as Er | Er

EILSEQ: the cursor goes back through srcp, errno gets 84, and -1 returns.

{iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
ms_enter "L94"
iApply wp_renew with Hspl ; reflexivity | word_premise | reflexivity | reflexivity | addr_premise | addr_premise | cbn [ ptr_addr ] ; unfold raw_address ; drop_wraps_goal ; rewrite Z.add_0_r ; exact Hspal |
iNext
iIntros Hspl
gen_env
iApply wp_raw_store_pointer with Hspl Hsp ; word_premise | word_premise | reflexivity | addr_premise | exact Hspal | intros ?m ?wd ?h Hl Hw ; exact Kpstore_ _ _ _ _ _ _ _ Hl Hw |
iNext
iIntros Hspl Hsp
iApply wp_goto
iNext
ms_enter "L196"
iApply wp_conv_errno
iNext
gen_env
iEval rewrite − dest_block in HBe
iDestruct HBe as (Hel & Hew & Hea)
iApply wp_check with Hel ; reflexivity | word_premise | rewrite Herr ; reflexivity | rewrite Herr ; addr_premise | rewrite Herr ; addr_premise | apply Z.mod_1_r |
iNext
iIntros Hel
gen_env
iApply wp_raw_store_w with Hel Hew ; word_premise | word_premise | rewrite Herr ; reflexivity | rewrite Herr ; addr_premise | exact Lxe' | intros ?m ?wd ?h Hl Hw ; exact Kstore_ _ _ _ _ _ _ _ Hl Hw |
iNext
iIntros Hel Hew
iApply wp_ret ; reflexivity | word_premise |
iNext
change 18446744073709551615 mod 2 ^ 64 with 2 ^ 64 − 1
iApply HΦ $! _ wpre ++ xo' ++ drop4 wrest cpre ++ co' ++ drop4 crest ys' cs' le_bytes84 4 ce' with [%] Hc Hposix Hcod Hs Hdl [Hdw Hw0 Hw1] [Hda Ha0 Ha1] HBs [Hel Hew Hea] Hspl Hsp
–split ; left ; split ; reflexivity | apply le_value_byte ; lia |
split ; rewrite ! length_app length_drop ; lia | apply length_le_bytes
–rewrite bytes_app bytes_app Lwp Lxo' Z.add_0_l
iFrame
–rewrite auxes_app auxes_app Lcp Lco' Z.add_0_l
iFrame
–rewrite - dest_block
iFrame
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
ms_enter "L89"
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ?m ; word_premise |
iNext
gen_env
destruct Z.eqb_specr 0 as Ez | Ez

The NUL: null goes back through srcp, and the count of characters returns.

{subst r
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
ms_enter "L31"
gen_env
iApply wp_renew with Hspl ; reflexivity | word_premise | reflexivity | reflexivity | addr_premise | addr_premise | cbn [ ptr_addr ] ; unfold raw_address ; drop_wraps_goal ; rewrite Z.add_0_r ; exact Hspal |
iNext
iIntros Hspl
gen_env
iApply wp_raw_store_pointer with Hspl Hsp ; word_premise | word_premise | reflexivity | addr_premise | exact Hspal | intros ?m ?wd ?h Hl Hw ; exact Kpstore_ _ _ _ _ _ _ _ Hl Hw |
iNext
iIntros Hspl Hsp
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
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ?m ; word_premise |
iNext
gen_env
iApply wp_ret ; reflexivity | word_premise |
iNext
assert E4 : bd + Z.of_nati + i + i + i + 0 − bd = Z.of_nati × 4 by lia
rewrite E4
rewrite Z.div_mul ; | lia
rewrite Z.mod_small ; | lia
iApply HΦ $! _ wpre ++ xo' ++ drop4 wrest cpre ++ co' ++ drop4 crest ys' cs' xe' ce' with [%] Hc Hposix Hcod Hs Hdl [Hdw Hw0 Hw1] [Hda Ha0 Ha1] HBs HBe Hspl Hsp
–split ; right ; exists i ; split ; reflexivity | ; split ; lia | ; split |
+rewrite <- Lwp
rewrite take_app_length
exact Hwide
+rewrite <- Lwp
rewrite drop_app_length
rewrite take_app_le ; | lia
rewrite take_ge ; | lia
exact Hzeq_refl
+split ; rewrite ! length_app length_drop ; lia | exact Lxe'
–rewrite bytes_app bytes_app Lwp Lxo' Z.add_0_l
iFrame
–rewrite auxes_app auxes_app Lcp Lco' Z.add_0_l
iFrame

A character: both cursors move on, and the loop goes round.

destruct HposEz Er as Hr0 & Hxo & Hv′ & Hi′
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
ms_enter "L102"
rewrite length_drop in Hr0
iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ ptr_addrp + Z.of_natj + Z.to_natr ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |
iNext
gen_env
iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ bd + Z.of_nat4 × Si ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |
iNext
gen_env
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ?m ; word_premise |
iNext
gen_env
iApply wp_goto
iNext
ms_enter "L28"
gen_env
iAssert bytesbd 0 wpre ++ xo' with [Hdw Hw0] as Hdw ; rewrite bytes_app Lwp Z.add_0_l ; iFrame |
iAssert auxesbd 0 cpre ++ co' with [Hda Ha0] as Hda ; rewrite auxes_app Lcp Z.add_0_l ; iFrame |
assert Eo : Z.of_nat4 × i + Z.of_nat4 = Z.of_nat4 × Si by lia
iEval rewriteEo in Hw1
iEval rewriteEo in Ha1
iApply IH $! _ Si j + Z.to_natr%nat wpre ++ xo' cpre ++ co' drop4 wrest drop4 crest ys' cs' xe' ce' x with [%] Hk Hc Hposix Hcod Hs Hdl Hdw Hda Hw1 Ha1 HBs HBe Hspl Hsp HΦ
pose proof wide_ok_app_ _ i Hwide Lwp Lxo' Hxo as Hw′
unfold mbs_vars
repeat match goal with|- _ ∧ _⇒splitend
all: try assumption ; try lia ; try rewrite length_app ; lia ; try rewrite length_drop ; lia
match goal withH : lookupTAtom"pr.1" _ = Some_ |- _⇒rewrite H ; f_equal ; f_equal ; liaend

rpl_mbsrtowcs

rpl_mbsrtowcs's entry binds its four arguments.

1040Lemma mbs_entry
∀ dst src len ps
invocationmbs_fn WPtrdst; WPtrsrc; WIntlen; WPtrps = mkFramembs_fn TAtom"v6", WPtrps; TAtom"v4", WIntlen; TAtom"v2", WPtrsrc; TAtom"v0", WPtrdst [ ] None EnterTAtom"start" None
Explore proof 1 tactics

Initial goal

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
ptr
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, 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
Hlinked :
hello_linkedge
wi_lent :
∀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
set_spec :
contractlibc_world
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_abi :
∀d : name c v : value, contract_abiset_spec CResultd P ArgW c; ArgP v
Hset_pre :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → contract_preset_spec WIntk; WPtrz m w
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, 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
Kbyte :
∀b : Z reg : region o x y : Z m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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
Kstore :
∀b : Z reg : region o : Z xs : listZ y : Z m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, 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
Kalloc :
∀q : alloc_req m : mem wd : libc_world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
Herrno_reg :
registryTAtom"__errno_location" = SomeLB.errno_contractrep
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
dst, src :
ptr
len :
Z
ps :
ptr
⊢
invocationmbs_fn WPtrdst; WPtrsrc; WIntlen; WPtrps = fr_fn ≔ mbs_fn; fr_env ≔ TAtom"v6", WPtrps; TAtom"v4", WIntlen; TAtom"v2", WPtrsrc; TAtom"v0", WPtrdst; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"start" None

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
reflexivity

rpl_mbsrtowcs(dest, srcp, len, ps) as main calls it: dest a fresh buffer of len wide characters, srcp a cell holding the string p, len the string's length and its NUL, and ps a non-null state, valid and in its initial shift state. The entry allocates a local it never uses, keeps ps, loads the string through srcp, a read-only literal or not, and goes to the converting loop (mbs_loop) with nothing written yet; the counting loop, for a null dest, is not reached. The call returns what mbs_post says.

1054Lemma rpl_mbsrtowcs_spec
∀ p b reg bs bd rd ws cws sb sr so ys cs be re oe xe ce spb spr spo codec dq p0 t0 rc rp Φ
errno = mkPtrbe + oe Objbe
0 < bd
bd mod 4 = 0
bd + 4 × Z.of_natlengthbs + 1 ≤ r_endrd
r_endrd ≤ 2 ^ 48
0 < sb
0 ≤ so
sb + so mod 4 = 0
sb + so + 8 ≤ r_endsr
r_endsr ≤ 2 ^ 48
0 < spb
0 ≤ spo
spb + spo mod 8 = 0
spb + spo + 8 ≤ r_endspr
r_endspr ≤ 2 ^ 48
0 < be
0 ≤ oe
be + oe + 4 ≤ r_endre
r_endre ≤ 2 ^ 48
lengthws = 4 × lengthbs + 1%nat
lengthcws = 4 × lengthbs + 1%nat
validcodec ys
le_valuetake4 ys = 0
lengthys = 8%nat
lengthcs = 8%nat
lengthxe = 4%nat
lengthce = 4%nat
LL.lent0 p0 t0 −∗ SL.stringc_ptr 65824 rc c_bytes −∗ SL.stringposix_ptr 65856 rp posix_bytes −∗ pointstoPNamecodec_key dq VCodeccodec −∗ SL.stringp b reg bs −∗ livebd rd −∗ bytesbd 0 ws −∗ auxesbd 0 cws −∗ ptsblock_pssb sr so ys cs −∗ ptsblock_psbe re oe xe ce −∗ livespb spr −∗ pcellspb spo p −∗ ∀r ws′ cws′ ys′ cs′ xe′ ce′ x′, ⌜mbs_postlengthbs r ws′ xe′ ∧ lengthws′ = 4 × lengthbs + 1%nat ∧ lengthxe′ = 4%nat⌝ −∗ SL.stringc_ptr 65824 rc c_bytes −∗ SL.stringposix_ptr 65856 rp posix_bytes −∗ pointstoPNamecodec_key dq VCodeccodec −∗ SL.stringp b reg bs −∗ livebd rd −∗ bytesbd 0 ws′ −∗ auxesbd 0 cws′ −∗ ptsblock_pssb sr so ys′ cs′ −∗ ptsblock_psbe re oe xe′ ce′ −∗ livespb spr −∗ pcellspb spo x′ −∗ ΦRetWIntr −∗ WPERuninvocationmbs_fn WPtrmkPtrbd Objbd; WPtrmkPtrspb + spo Objspb; WIntZ.of_natlengthbs + 1; WPtrmkPtrsb + so Objsb : cexpr {Φ}
Proof 54 steps Qed
intros Herr Hbd Hbd4 Hdend Hd48 Hsb Hso Hsal Hsend′ Hs48 Hspb Hspo Hspal Hspend Hsp48 Hbe Hoe Heend He48 Lws Lcws Hval Hinit Lys Lcs Lxe Lce
iIntros #Hk Hc Hposix Hcod Hs Hdl Hdw Hda HBs HBe Hspl Hsp HΦ
iDestruct Hs as [%Hok Hps]
pose proof Hok as Hcp & Hb0 & Hbp & Hsend & H48 & Hbs
rewrite mbs_entry
iApply wp_enter_ _ _ _ _ _ _ _ mbs_block"start" ; vm_compute ; reflexivity | word_premise | ; iNext
cbn [ b_insts b_jump mbs_block hblk ]

The local for the counting loop, never used here.

iApply wp_alloc_ _ _ _ _ _ _ _ _ _ _ _ _ 8 ; reflexivity | lia | unfold max_allocation_size ; lia | intros m wd h base Hf Hw ; exact Kalloc_ _ _ _ _ Hf Hw |
iNext
iIntros base _ _
rm_let
rm_let
rm_let

ps is not null.

iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; cbn ; rewrite Z.mod_smallsb + so ; | lia ; rewrite proj2Z.eqb_neqsb + so _ ; reflexivity | change 0 mod 2 ^ 64 mod 2 ^ 64 with 0 ; lia |
iNext
cbn [ Z.eqb edge_label ]
ms_enter "L10"
gen_env

The string through srcp.

iApply wp_check_read with Hspl ; reflexivity | word_premise | left ; reflexivity | addr_premise | addr_premise | addr_premise |
iNext
iIntros Hspl
gen_env
iApply wp_raw_load_pointer_in with Hspl Hsp Hps ; reflexivity | word_premise | left ; reflexivity | addr_premise | addr_premise | lia | intros xb Hxb ; exists reg ; destruct Hcp as Hcp | Hcp ; rewrite Hcp in Hxb ; destruct Hxb as Hxb | Hxb ; try discriminate Hxb ; injection Hxb as ← ; apply elem_of_cons ; left ; reflexivity |
iNext
iIntros Hspl Hsp Hps
gen_env
iAssert SL.stringp b reg bs with [$Hps] as Hs ; done |

dest is not null: the converting loop.

rm_let
gen_env
rm_let
gen_env
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; cbn ; rewrite Z.mod_smallbd ; | lia ; rewrite proj2Z.eqb_neqbd _ ; reflexivity | change 0 mod 2 ^ 64 mod 2 ^ 64 with 0 ; lia |
iNext
cbn [ Z.eqb edge_label ]
iApply wp_enter_ _ _ _ _ _ _ _ mbs_block"L28" ; vm_compute ; reflexivity | word_premise | ; iNext
gen_env
iPoseProof mbs_loopp b reg bs bd rd sb sr so be re oe spb spr spo codec dq p0 t0 rc rp Φ Herr Hbd Hbd4 Hdend Hd48 Hsb Hsal Hspb Hspo Hspal Hspend Hsp48 Hbe Hoe Heend He48 as L
iApply L $! _ 0%nat 0%nat [ ] [ ] ws cws ys cs xe ce p with [%] Hk Hc Hposix Hcod Hs Hdl [] [] Hdw Hda HBs HBe Hspl Hsp HΦ
–assert Ep : mkPtrptr_addrp + Z.of_nat0 ptr_capp = p by destruct p ; cbn ; f_equal ; lia
rewrite Ep
replace bd + Z.of_nat4 × 0 with bd by lia
replace Z.of_natlengthbs + 1 − Z.of_nat0 with Z.of_natlengthbs + 1 by lia
split ; unfold mbs_vars ; repeat split ; cbn ; first reflexivity | rewrite Z.mod_small ; reflexivity | lia |
split ; lia |
split ; reflexivity |
split ; reflexivity |
split ; rewrite Lws ; lia |
split ; rewrite Lcws ; lia |
split ; exact wide_ok_nil |
repeat split ; assumption
–rewrite / bytes / byte_ps / pts /=
done
–rewrite / auxes / aux_ps / pts /=
done

HelloConvOn over a Logic instance of its own.

1136Module HelloConv R : Runtime
1137Module LG0 ≔ Logic R
Include HelloConvOn R LG0