Filnix wiki

n :

⊢

invocationsnru_fn WIntk; WPtrp; WIntn = fr_fn ≔ snru_fn; fr_env ≔ TAtom"v4", WIntn; TAtom"v2", WPtrp; TAtom"v0", WIntk; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"start" None

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

reflexivity

setlocale_null_r's entry binds its category, buffer and size.

138Lemma snr_entry

∀ k p n

invocationsnr_fn WIntk; WPtrp; WIntn = mkFramesnr_fn TAtom"v4", WIntn; TAtom"v2", WPtrp; TAtom"v0", WIntk [ ] None EnterTAtom"start" None

Explore proof 1 tactics

Initial goal

k :

p :

n :

⊢

invocationsnr_fn WIntk; WPtrp; WIntn = fr_fn ≔ snr_fn; fr_env ≔ TAtom"v4", WIntn; TAtom"v2", WPtrp; TAtom"v0", WIntk; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"start" None

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

reflexivity

hard_locale's entry binds its category.

144Lemma hard_locale_entry

∀ k

invocationhard_locale_fn WIntk = mkFramehard_locale_fn TAtom"v0", WIntk [ ] None EnterTAtom"start" None

Explore proof 1 tactics

Initial goal

k :

⊢

invocationhard_locale_fn WIntk = fr_fn ≔ hard_locale_fn; fr_env ≔ TAtom"v0", WIntk; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"start" None

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

reflexivity

The genv's functions, for a genv with Hello's module.

150Lemma locale_fns

∀ ge

find_fnge TAtom"setlocale_null_unlocked" = SomeDefinedsnu_fn ∧ find_fnge TAtom"setlocale_null_r_unlocked" = SomeDefinedsnru_fn ∧ find_fnge TAtom"setlocale_null_r" = SomeDefinedsnr_fn

Explore proof 5 tactics

Initial goal

ge :

⊢

ge_modulege = hello_module → find_fnge TAtom"setlocale_null_unlocked" = SomeDefinedsnu_fn ∧ find_fnge TAtom"setlocale_null_r_unlocked" = SomeDefinedsnru_fn ∧ find_fnge TAtom"setlocale_null_r" = SomeDefinedsnr_fn

intros Hm

ge :

Hm :

⊢

find_fnge TAtom"setlocale_null_unlocked" = SomeDefinedsnu_fn ∧ find_fnge TAtom"setlocale_null_r_unlocked" = SomeDefinedsnru_fn ∧ find_fnge TAtom"setlocale_null_r" = SomeDefinedsnr_fn

unfold find_fn

ge :

Hm :

⊢

match find_directTAtom"setlocale_null_unlocked" ge_modulege with

Somed

⇒

Somed

None

⇒

let* t ≔ find_aliasTAtom"setlocale_null_unlocked" ge_modulege in

find_directt ge_modulege

SomeDefinedsnu_fn

∧

match find_directTAtom"setlocale_null_r_unlocked" ge_modulege with

Somed

⇒

Somed

None

⇒

let* t ≔ find_aliasTAtom"setlocale_null_r_unlocked" ge_modulege in

find_directt ge_modulege

SomeDefinedsnru_fn

∧

match find_directTAtom"setlocale_null_r" ge_modulege with

Somed

⇒

Somed

None

⇒

let* t ≔ find_aliasTAtom"setlocale_null_r" ge_modulege in

find_directt ge_modulege

SomeDefinedsnr_fn

rewrite Hm

ge :

Hm :

find_directt hello_module

⊢

match find_directTAtom"setlocale_null_unlocked" hello_module with

Somed

⇒

Somed

None

⇒

let* t ≔ find_aliasTAtom"setlocale_null_unlocked" hello_module in

SomeDefinedsnu_fn

∧

match find_directTAtom"setlocale_null_r_unlocked" hello_module with

Somed

⇒

Somed

None

⇒

let* t ≔ find_aliasTAtom"setlocale_null_r_unlocked" hello_module in

find_directt hello_module

SomeDefinedsnru_fn

∧

match find_directTAtom"setlocale_null_r" hello_module with

Somed

⇒

Somed

None

⇒

let* t ≔ find_aliasTAtom"setlocale_null_r" hello_module in

find_directt hello_module

SomeDefinedsnr_fn

vm_compute

ge :

Hm :

⊢

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros Hm

unfold find_fn

rewrite Hm

vm_compute

auto

The literals "C" and "POSIX" of hard-locale.c, read-only.

157Definition c_ptr: ptr ≔

mkPtr65824 Ro65824

Its bytes.

159Definition c_bytes: listZ ≔

"POSIX".

161Definition posix_ptr: ptr ≔

mkPtr65856 Ro65856

Its bytes.

163Definition posix_bytes: listZ ≔

80; 79; 83; 73; 88

Hello's symbols put the two literals there.

166Lemma locale_globals

lookupTAtom"hard-locale#str.31" hello_globals = Somec_ptr ∧ lookupTAtom"hard-locale#str.32" hello_globals = Someposix_ptr

Explore proof 2 tactics

Initial goal

⊢

lookupTAtom"hard-locale#str.31" hello_globals = Somec_ptr ∧ lookupTAtom"hard-locale#str.32" hello_globals = Someposix_ptr

vm_compute

⊢

Someptr_addr ≔ 65824; ptr_cap ≔ Ro65824 = Someptr_addr ≔ 65824; ptr_cap ≔ Ro65824 ∧ Someptr_addr ≔ 65856; ptr_cap ≔ Ro65856 = Someptr_addr ≔ 65856; ptr_cap ≔ Ro65856

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

vm_compute

auto

What setlocale_null_r_unlocked leaves in an n-byte buffer for the name t: the result r, the string u now at the buffer's start and the buffer's bytes ys. A name shorter than the buffer is copied with its NUL and r is 0; a longer one is cut to n - 1 bytes and a NUL, and r is ERANGE (34).

176Definition snru_resultt : listZ n : nat r : Z u ys : listZ : Prop ≔

lengtht < n%nat ∧ r = 0 ∧ u = t ∨ n ≤ lengtht%nat ∧ r = 34 ∧ u = taken − 1 t ∧ lengthys = n ∧ takeSlengthu ys = u ++ 0

Take every branch of the goal's conditions: each path is safe.

181Ltac all_cases ≔

repeat match goal with|- context [if ?t then _ else _]⇒destruct tend;cbn [ edge_label ]

The triples

The locale helpers over any runtime R.

187Module HelloLocaleOn R : Runtime LG₀ : LogicSigR

188Module HL ≔ HelloLeafOn R LG0

189Module LL ≔ HL.LL

190Module ML ≔ HL.ML

191Module SL ≔ ML.SL

192Module LG ≔ ML.LG

193Module L ≔ LG.L

Import L LG SL ML LL HL

196Section locale

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

198Context world : Type registry : name → optioncontractworld wi : mem → world → gmappiece pval → Prop `{!SafepointStablewi} ge : genv

The genv links Hello, whose world interpretation keeps every lent string where lent_at says.

203Context Hlinked : hello_linkedge

203Context 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 contract spec answers a query, of a category whose name the world lends, with that name, changing nothing; the query's arguments are admitted wherever the name is lent.

210Context set_spec : contractworld

210Context Hset : registryTAtom"setlocale" = Someset_spec

210Context Hset_ret : contract_returnsset_spec = RClassP

210Context Hset_abi : ∀d c v, contract_abiset_spec CResultd P ArgW c; ArgP v

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

210Context 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 and memcpy have their contracts.

221Context Hstrlen : registryTAtom"strlen" = Somestrlen_contractworld

221Context Hmemcpy : registryTAtom"memcpy" = Somememcpy_contractworld

The world interpretation survives a copy into a block the program owns, whatever bytes it leaves there, and a byte store into one.

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

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

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

strcmp has its contract, for streq.

239Context Hstrcmp : registryTAtom"strcmp" = Somestrcmp_contractworld

The Iris instance of the registry and wi.

242Instance locale_irisGS: irisGS_genhlc nanofil_langregistry ge Σ ≔

nanofil_irisGSregistry wi ge

The expressions of the language.

246Notation hexpr ≔ language.exprnanofil_langregistry ge

setlocale_null_unlocked(k) returns the name the world lends for k.

249Lemma snu_spec

∀ k p t Φ

0 ≤ k < 2 ^ 32

lentk p t −∗ ▷ΦRetWPtrp −∗ WPERuninvocationsnu_fn WIntk : hexpr {Φ}

Explore proof 11 tactics

Initial goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

world :

Type

registry :

name → optioncontractworld

wi :

mem → world → gmappiece pval → Prop

SafepointStable₀ :

ge :

Hlinked :

wi_lent :

∀m : mem w : 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 :

contractworld

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 : 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 : world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : 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_contractworld

Hmemcpy :

registryTAtom"memcpy" = Somememcpy_contractworld

Kcopy :

∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : 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 : 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

Kalloc :

∀q : alloc_req m : mem wd : world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Hstrcmp :

registryTAtom"strcmp" = Somestrcmp_contractworld

k :

p :

t :

listZ

Φ :

outcome → iPropIΣ

⊢

0 ≤ k < 2 ^ 32 → lentk p t −∗ ▷ΦRetWPtrp −∗ WPERuninvocationsnu_fn WIntk : hexpr {v. Φv}

intros Hk₃₂

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

world :

Type

registry :

name → optioncontractworld

wi :

mem → world → gmappiece pval → Prop

SafepointStable₀ :

ge :

Hlinked :

wi_lent :

∀m : mem w : 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 :

contractworld

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 : 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 :

Hstrlen :

registryTAtom"strlen" = Somestrlen_contractworld

Hmemcpy :

registryTAtom"memcpy" = Somememcpy_contractworld

Kcopy :

Kbyte :

Kalloc :

∀q : alloc_req m : mem wd : world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Hstrcmp :

registryTAtom"strcmp" = Somestrcmp_contractworld

k :

p :

t :

listZ

Φ :

outcome → iPropIΣ

Hk₃₂ :

0 ≤ k < 2 ^ 32

⊢

lentk p t −∗ ▷ΦRetWPtrp −∗ WPERuninvocationsnu_fn WIntk : hexpr {v. Φv}

iIntros #Hk HΦ

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

world :

Type

registry :

name → optioncontractworld

wi :

mem → world → gmappiece pval → Prop

SafepointStable₀ :

ge :

Hlinked :

wi_lent :

∀m : mem w : 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 :

contractworld

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 : 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 :

Hstrlen :

registryTAtom"strlen" = Somestrlen_contractworld

Hmemcpy :

registryTAtom"memcpy" = Somememcpy_contractworld

Kcopy :

Kbyte :

Kalloc :

∀q : alloc_req m : mem wd : world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Hstrcmp :

registryTAtom"strcmp" = Somestrcmp_contractworld

k :

p :

t :

listZ

Φ :

outcome → iPropIΣ

Hk₃₂ :

0 ≤ k < 2 ^ 32

Hk :

lentk p t

□

HΦ :

▷ΦRetWPtrp

∗

WPERuninvocationsnu_fn WIntk {v. Φv}

rewrite snu_entry

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

world :

Type

registry :

name → optioncontractworld

wi :

mem → world → gmappiece pval → Prop

SafepointStable₀ :

ge :

Hlinked :

wi_lent :

∀m : mem w : 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 :

contractworld

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 : 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 :

Hstrlen :

registryTAtom"strlen" = Somestrlen_contractworld

Hmemcpy :

registryTAtom"memcpy" = Somememcpy_contractworld

Kcopy :

Kbyte :

Kalloc :

∀q : alloc_req m : mem wd : world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Hstrcmp :

registryTAtom"strcmp" = Somestrcmp_contractworld

k :

p :

t :

listZ

Φ :

outcome → iPropIΣ

Hk₃₂ :

0 ≤ k < 2 ^ 32

Hk :

lentk p t

□

HΦ :

▷ΦRetWPtrp

∗

WPERunfr_fn ≔ snu_fn; fr_env ≔ TAtom"v0", WIntk; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"start" None {v. Φv}

iApply wp_enter ; exact find_u_start | reflexivity |

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

world :

Type

registry :

name → optioncontractworld

wi :

mem → world → gmappiece pval → Prop

SafepointStable₀ :

ge :

Hlinked :

wi_lent :

∀m : mem w : 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 :

contractworld

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 : 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 :

Hstrlen :

registryTAtom"strlen" = Somestrlen_contractworld

Hmemcpy :

registryTAtom"memcpy" = Somememcpy_contractworld

Kcopy :

Kbyte :

Kalloc :

∀q : alloc_req m : mem wd : world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Hstrcmp :

registryTAtom"strcmp" = Somestrcmp_contractworld

k :

p :

t :

listZ

Φ :

outcome → iPropIΣ

Hk₃₂ :

0 ≤ k < 2 ^ 32

Hk :

lentk p t

□

HΦ :

▷ΦRetWPtrp

∗

▷WPHelloLocaleOn.LG.L.ERunfr_fn ≔ snu_fn; fr_env ≔ TAtom"v0", WIntk; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" b_instsu_start b_jumpu_start {v. Φv}

iNext

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

world :

Type

registry :

name → optioncontractworld

wi :

mem → world → gmappiece pval → Prop

SafepointStable₀ :

ge :

Hlinked :

wi_lent :

∀m : mem w : 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 :

contractworld

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 : 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 :

Hstrlen :

registryTAtom"strlen" = Somestrlen_contractworld

Hmemcpy :

registryTAtom"memcpy" = Somememcpy_contractworld

Kcopy :

Kbyte :

Kalloc :

∀q : alloc_req m : mem wd : world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Hstrcmp :

registryTAtom"strcmp" = Somestrcmp_contractworld

k :

p :

t :

listZ

Φ :

outcome → iPropIΣ

Hk₃₂ :

0 ≤ k < 2 ^ 32

Hk :

lentk p t

□

HΦ :

∗

WPHelloLocaleOn.LG.L.ERunfr_fn ≔ snu_fn; fr_env ≔ TAtom"v0", WIntk; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" b_instsu_start b_jumpu_start {v. Φv}

cbn [ b_insts b_jump u_start ]

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

world :

Type

registry :

name → optioncontractworld

wi :

mem → world → gmappiece pval → Prop

SafepointStable₀ :

ge :

Hlinked :

wi_lent :

∀m : mem w : 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 :

contractworld

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 : 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 :

Hstrlen :

registryTAtom"strlen" = Somestrlen_contractworld

Hmemcpy :

registryTAtom"memcpy" = Somememcpy_contractworld

Kcopy :

Kbyte :

Kalloc :

∀q : alloc_req m : mem wd : world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Hstrcmp :

registryTAtom"strcmp" = Somestrcmp_contractworld

k :

p :

t :

listZ

Φ :

outcome → iPropIΣ

Hk₃₂ :

0 ≤ k < 2 ^ 32

Hk :

lentk p t

□

HΦ :

∗

WPHelloLocaleOn.LG.L.ERunfr_fn ≔ snu_fn; fr_env ≔ TAtom"v0", WIntk; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" CallCResultTAtom"v4" P GlobalTAtom"setlocale" ArgW TmpTAtom"v0"; ArgP Const0 JRetTmpTAtom"v4" {v. Φv}

iApply wp_lent_query_ _ _ _ _ _ _ _ _ _ _ _ set_spec WIntk; WPtrmkPtr0 CNone k p t with Hk ; exact Hset | exact Hset_ret | apply linked_outside ; exact Hlinked | reflexivity | apply linked_unbound ; exact Hlinked | reflexivity | reflexivity | cbn ; rewrite Z.mod_small ; reflexivity | exact Hk₃₂ | apply Hset_abi | intros m w h Hw Hl ; exact Hset_prem w h k p t mkPtr0 CNone Hw Hl eq_refl | intros s m w h tr en s′ m′ w′ Hw Hl Hi ; exact Hset_query_ _ s m w h k p t mkPtr0 CNone tr en s' m' w' Hw Hl eq_refl Hi |

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

world :

Type

registry :

name → optioncontractworld

wi :

mem → world → gmappiece pval → Prop

SafepointStable₀ :

ge :

Hlinked :

wi_lent :

∀m : mem w : 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 :

contractworld

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 : 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 :

Hstrlen :

registryTAtom"strlen" = Somestrlen_contractworld

Hmemcpy :

registryTAtom"memcpy" = Somememcpy_contractworld

Kcopy :

Kbyte :

Kalloc :

∀q : alloc_req m : mem wd : world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Hstrcmp :

registryTAtom"strcmp" = Somestrcmp_contractworld

k :

p :

t :

listZ

Φ :

outcome → iPropIΣ

Hk₃₂ :

0 ≤ k < 2 ^ 32

Hk :

lentk p t

□

HΦ :

∗

▷WPHelloLocaleOn.LL.L.ERunfr_fn ≔ snu_fn; fr_env ≔ putTAtom"v4" WPtrp TAtom"v0", WIntk; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JRetTmpTAtom"v4" {v. Φv}

iNext

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

world :

Type

registry :

name → optioncontractworld

wi :

mem → world → gmappiece pval → Prop

SafepointStable₀ :

ge :

Hlinked :

wi_lent :

∀m : mem w : 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 :

contractworld

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 : 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 :

Hstrlen :

registryTAtom"strlen" = Somestrlen_contractworld

Hmemcpy :

registryTAtom"memcpy" = Somememcpy_contractworld

Kcopy :

Kbyte :

Kalloc :

∀q : alloc_req m : mem wd : world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Hstrcmp :

registryTAtom"strcmp" = Somestrcmp_contractworld

k :

p :

t :

listZ

Φ :

outcome → iPropIΣ

Hk₃₂ :

0 ≤ k < 2 ^ 32

Hk :

lentk p t

□

HΦ :

∗

WPHelloLocaleOn.LL.L.ERunfr_fn ≔ snu_fn; fr_env ≔ putTAtom"v4" WPtrp TAtom"v0", WIntk; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JRetTmpTAtom"v4" {v. Φv}

iApply wp_ret ; reflexivity | reflexivity |

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

world :

Type

registry :

name → optioncontractworld

wi :

mem → world → gmappiece pval → Prop

SafepointStable₀ :

ge :

Hlinked :

wi_lent :

∀m : mem w : 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 :

contractworld

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 : 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 :

Hstrlen :

registryTAtom"strlen" = Somestrlen_contractworld

Hmemcpy :

registryTAtom"memcpy" = Somememcpy_contractworld

Kcopy :

Kbyte :

Kalloc :

∀q : alloc_req m : mem wd : world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Hstrcmp :

registryTAtom"strcmp" = Somestrcmp_contractworld

k :

p :

t :

listZ

Φ :

outcome → iPropIΣ

Hk₃₂ :

0 ≤ k < 2 ^ 32

Hk :

lentk p t

□

HΦ :

∗

▷ΦRetWPtrp

iNext

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

world :

Type

registry :

name → optioncontractworld

wi :

mem → world → gmappiece pval → Prop

SafepointStable₀ :

ge :

Hlinked :

wi_lent :

∀m : mem w : 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 :

contractworld

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 : 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 :

Hstrlen :

registryTAtom"strlen" = Somestrlen_contractworld

Hmemcpy :

registryTAtom"memcpy" = Somememcpy_contractworld

Kcopy :

Kbyte :

Kalloc :

∀q : alloc_req m : mem wd : world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Hstrcmp :

registryTAtom"strcmp" = Somestrcmp_contractworld

k :

p :

t :

listZ

Φ :

outcome → iPropIΣ

Hk₃₂ :

0 ≤ k < 2 ^ 32

Hk :

lentk p t

□

HΦ :

∗

iExact HΦ

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros Hk₃₂

iIntros #Hk HΦ

rewrite snu_entry

iApply wp_enter ; exact find_u_start | reflexivity |

iNext

cbn [ b_insts b_jump u_start ]

iNext

iApply wp_ret ; reflexivity | reflexivity |

iNext

iExact HΦ

setlocale_null_r_unlocked(k, buf, n), for the n-byte block of the bytes xs and the slots cs at the start of the live object b, at a multiple of 8, and the name t the world lends for k: it leaves snru_result in the block and returns its r.

268Lemma snru_spec

∀ k p t b reg xs cs Φ

0 ≤ k < 2 ^ 32

0 < b

b mod 8 = 0

lengthcs = lengthxs

0 < lengthxs%nat

b + Z.of_natlengthxs ≤ r_endreg

r_endreg ≤ 2 ^ 48

lentk p t −∗ liveb reg −∗ bytesb 0 xs −∗ auxesb 0 cs −∗ ▷∀r u ys cs′, ⌜snru_resultt lengthxs r u ys ∧ lengthcs′ = lengthxs⌝ −∗ liveb reg −∗ bytesb 0 ys −∗ auxesb 0 cs′ −∗ ΦRetWIntr −∗ WPERuninvocationsnru_fn WIntk; WPtrmkPtrb Objb; WIntZ.of_natlengthxs : hexpr {Φ}

Proof 147 steps Qed

intros Hk₃₂ Hb₀ Hb₈ Hlc Hn Hend H₄₈

iIntros #Hk Hl Hx Hcs HΦ

iPoseProof Hk as [%Hp _]

destruct Hp as Hp & Hpt & Ht

destruct locale_fnsge proj1Hlinked as Hsnu & _ & _

rewrite snru_entry

iApply wp_enter ; exact find_r_start | reflexivity |

iNext

cbn [ b_insts b_jump r_start ]

iApply wp_call_bind_ _ _ _ _ _ _ _ _ _ _ _ _ snu_fn invocationsnu_fn WIntk ; cbn ; rewrite Z.mod_small ; reflexivity | exact Hk32 | exact Hsnu | reflexivity |

iNext

iApply snu_spec with Hk ; exact Hk32 |

iNext

iExists _

iSplit ; iPureIntro ; reflexivity |

iNext

cbn [ fr_fn fr_env fr_locals fr_doomed fr_at ]

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

iNext

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

iNext

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

iNext

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

iNext

cbn [ Z.eqb edge_label ]

iApply wp_enter ; exact find_r_L10 | reflexivity |

iNext

cbn [ b_insts b_jump r_L10 ]

iNext

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

iNext

destruct decidelengtht < lengthxs%nat as Hfit | Hlong

The name fits: copy it with its NUL.

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

iNext

cbn [ Z.eqb edge_label ]

iApply wp_enter ; exact find_r_L27 | reflexivity |

iNext

cbn [ b_insts b_jump r_L27 ]

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

iNext

set c := Slengtht

iAssert bytesb 0 takec xs ∗ bytesb 0 + Z.of_natlengthtakec xs dropc xs%I with [Hx] as [Hx₁ Hx₂] ; rewrite - bytes_app take_drop ; iExact Hx |

iAssert auxesb 0 takec cs ∗ auxesb 0 + Z.of_natlengthtakec cs dropc cs%I with [Hcs] as [Hc₁ Hc₂] ; rewrite - auxes_app take_drop ; iExact Hcs |

assert Hc : lengthtakec xs = c by rewrite length_take ; lia

assert Hcc : lengthtakec cs = c by rewrite length_take ; lia

iNext

iIntros cs₁ Hcs₁ Hl Hx₁ Hc₁

iApply wp_ret ; reflexivity | reflexivity |

iNext

assert Ec : takelengthtakec xs t ++ 0 = t ++ 0 by rewrite Hc take_ge ; reflexivity | rewrite length_app ; cbn [ length ] ; unfold c ; lia

rewrite Ec Hc Hcc

rewrite Hc in Hcs1

iApply HΦ $! 0 t t ++ 0 ++ dropc xs cs1 ++ dropc cs with [%] Hl [Hx₁ Hx₂] [Hc₁ Hc₂]

+split ; | rewrite length_app length_drop ; lia

split ; left ; auto |

split

∗rewrite ! length_app length_drop

cbn [ length ]

unfold c

lia

∗replace Slengtht with lengtht ++ 0 by rewrite length_app ; cbn [ length ] ; lia

apply take_app_length

+iApply bytes_app

rewrite length_app

cbn [ length ]

replace 0 + Z.of_natlengtht + 1 with 0 + Z.of_natc by unfold c ; lia

iFrame

+iApply auxes_app

rewrite Hcs1

iFrame

The name does not fit: copy n - 1 bytes of it and end them with a NUL.

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

iNext

cbn [ Z.eqb edge_label ]

iApply wp_enter ; exact find_r_L28 | reflexivity |

iNext

cbn [ b_insts b_jump r_L28 ]

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

iNext

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

iNext

cbn [ Z.eqb edge_label ]

iApply wp_enter ; exact find_r_L39 | reflexivity |

iNext

cbn [ b_insts b_jump r_L39 ]

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

iNext

set c := lengthxs − 1%nat

assert Hc : lengthtakec xs = c by rewrite length_take ; lia

assert Hcc : lengthtakec cs = c by rewrite length_take ; lia

destruct dropc xs as | x | x′ rest eqn: Ed ; apply f_equallength in Ed ; rewrite length_drop in Ed ; cbn in Ed ; lia | | apply f_equallength in Ed ; rewrite length_drop in Ed ; cbn in Ed ; lia

assert Eb : ∀y, byte_psb Z.of_natc y = PByteb Z.of_natc, VBytey by intros y ; rewrite byte_ps_cons ; reflexivity

iAssert bytesb 0 takec xs ∗ bytesb 0 + Z.of_natlengthtakec xs dropc xs%I with [Hx] as [Hx₁ Hx₂] ; rewrite - bytes_app take_drop ; iExact Hx |

rewrite Ed Hc Z.add_0_l / bytes Eb

iEval ( rewrite -/ ibyteb Z.of_natc x ) in Hx₂

rewrite -/ bytesb 0 takec xs

iAssert auxesb 0 takec cs ∗ auxesb 0 + Z.of_natlengthtakec cs dropc cs%I with [Hcs] as [Hc₁ Hc₂] ; rewrite - auxes_app take_drop ; iExact Hcs |

rewrite Hcc

iNext

iIntros cs₁ Hcs₁ Hl Hx₁ Hc₁

rewrite Hc in Hcs1

iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ b + Z.of_natc ; word_premise | cbn ; f_equal ; f_equal ; unfold c ; addr_premise | word_premise |

iNext

iNext

iIntros Hl

iNext

iIntros Hl Hx₂

iApply wp_goto

iNext

iApply wp_enter ; exact find_r_L41 | reflexivity |

iNext

cbn [ b_insts b_jump r_L41 ]

iApply wp_ret ; reflexivity | reflexivity |

iNext

assert Ec : takelengthtakec xs t ++ 0 = takec t by rewrite Hc take_app_le ; reflexivity | lia

rewrite Ec

iApply HΦ $! 34 takec t takec t ++ 0 cs1 ++ dropc cs with [%] Hl [Hx₁ Hx₂] [Hc₁ Hc₂]

+split ; | rewrite length_app length_drop ; lia

split ; right ; split ; lia | ; split ; reflexivity | ; reflexivity |

split

∗rewrite length_app length_take

cbn [ length ]

unfold c

lia

∗apply take_ge

rewrite length_app

cbn [ length ]

lia

+iApply bytes_app

rewrite length_take Nat.min_l ; | unfold c ; lia

rewrite Z.add_0_l / bytes Eb

iFrame Hx₁

iExact Hx₂

+iApply auxes_app

rewrite Hcs1

iFrame

setlocale_null_r(k, buf, n) is setlocale_null_r_unlocked's call (snru_spec): this build takes no lock.

388Lemma snr_spec

∀ k p t b reg xs cs Φ

0 ≤ k < 2 ^ 32

0 < b

b mod 8 = 0

lengthcs = lengthxs

0 < lengthxs%nat

b + Z.of_natlengthxs ≤ r_endreg

r_endreg ≤ 2 ^ 48

lentk p t −∗ liveb reg −∗ bytesb 0 xs −∗ auxesb 0 cs −∗ ▷∀r u ys cs′, ⌜snru_resultt lengthxs r u ys ∧ lengthcs′ = lengthxs⌝ −∗ liveb reg −∗ bytesb 0 ys −∗ auxesb 0 cs′ −∗ ΦRetWIntr −∗ WPERuninvocationsnr_fn WIntk; WPtrmkPtrb Objb; WIntZ.of_natlengthxs : hexpr {Φ}

Proof 18 steps Qed

intros Hk₃₂ Hb₀ Hb₈ Hlc Hn Hend H₄₈

iIntros #Hk Hl Hx Hcs HΦ

destruct locale_fnsge proj1Hlinked as _ & Hsnru & _

rewrite snr_entry

iApply wp_enter ; exact find_n_start | reflexivity |

iNext

cbn [ b_insts b_jump n_start ]

iNext

iNext

iIntros r u ys cs′ Hr Hl Hx Hcs

iExists _

iSplit ; iPureIntro ; reflexivity |

iNext

cbn [ fr_fn fr_env fr_locals fr_doomed fr_at ]

assert Hr₃₂ : r = 0 ∨ r = 34 by destruct Hr as _ & → & _ | _ & → & _ & _ & _ ; auto

destruct Hr32 as → | → ; iApply wp_ret ; reflexivity | reflexivity | ; iNext ; iApply HΦ with [%] Hl Hx Hcs ; exact Hr

The genv's literals are Hello's, and streq and setlocale_null_r are its functions.

416Lemma hard_locale_lookups

lookupTAtom"hard-locale#str.31" ge_globalsge = Somec_ptr ∧ lookupTAtom"hard-locale#str.32" ge_globalsge = Someposix_ptr ∧ find_fnge TAtom"streq" = SomeDefinedstreq_fn ∧ find_fnge TAtom"setlocale_null_r" = SomeDefinedsnr_fn

Explore proof 5 tactics

Initial goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

world :

Type

registry :

name → optioncontractworld

wi :

mem → world → gmappiece pval → Prop

SafepointStable₀ :

ge :

Hlinked :

wi_lent :

∀m : mem w : 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 :

contractworld

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 : 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 :

Hstrlen :

registryTAtom"strlen" = Somestrlen_contractworld

Hmemcpy :

registryTAtom"memcpy" = Somememcpy_contractworld

Kcopy :

Kbyte :

Kalloc :

∀q : alloc_req m : mem wd : world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Hstrcmp :

registryTAtom"strcmp" = Somestrcmp_contractworld

⊢

destruct locale_globals as H₁ & H₂

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

world :

Type

registry :

name → optioncontractworld

wi :

mem → world → gmappiece pval → Prop

SafepointStable₀ :

ge :

Hlinked :

wi_lent :

∀m : mem w : 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 :

contractworld

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 : 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 :

Hstrlen :

registryTAtom"strlen" = Somestrlen_contractworld

Hmemcpy :

registryTAtom"memcpy" = Somememcpy_contractworld

Kcopy :

Kbyte :

Kalloc :

∀q : alloc_req m : mem wd : world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Hstrcmp :

registryTAtom"strcmp" = Somestrcmp_contractworld

H₁ :

lookupTAtom"hard-locale#str.31" hello_globals = Somec_ptr

H₂ :

lookupTAtom"hard-locale#str.32" hello_globals = Someposix_ptr

⊢

destruct Hlinked as Hm & Hg & _

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

world :

Type

registry :

name → optioncontractworld

wi :

mem → world → gmappiece pval → Prop

SafepointStable₀ :

ge :

Hlinked :

wi_lent :

∀m : mem w : 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 :

contractworld

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 : 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 :

Hstrlen :

registryTAtom"strlen" = Somestrlen_contractworld

Hmemcpy :

registryTAtom"memcpy" = Somememcpy_contractworld

Kcopy :

Kbyte :

Kalloc :

∀q : alloc_req m : mem wd : world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Hstrcmp :

registryTAtom"strcmp" = Somestrcmp_contractworld

H₁ :

lookupTAtom"hard-locale#str.31" hello_globals = Somec_ptr

H₂ :

lookupTAtom"hard-locale#str.32" hello_globals = Someposix_ptr

Hm :

Hg :

∀n : name p : ptr, lookupn hello_globals = Somep → lookupn ge_globalsge = Somep

⊢

split ; exact Hg_ _ H₁ |

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

world :

Type

registry :

name → optioncontractworld

wi :

mem → world → gmappiece pval → Prop

SafepointStable₀ :

ge :

Hlinked :

wi_lent :

∀m : mem w : 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 :

contractworld

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 : 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 :

Hstrlen :

registryTAtom"strlen" = Somestrlen_contractworld

Hmemcpy :

registryTAtom"memcpy" = Somememcpy_contractworld

Kcopy :

Kbyte :

Kalloc :

∀q : alloc_req m : mem wd : world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Hstrcmp :

registryTAtom"strcmp" = Somestrcmp_contractworld

H₁ :

lookupTAtom"hard-locale#str.31" hello_globals = Somec_ptr

H₂ :

lookupTAtom"hard-locale#str.32" hello_globals = Someposix_ptr

Hm :

Hg :

∀n : name p : ptr, lookupn hello_globals = Somep → lookupn ge_globalsge = Somep

⊢

lookupTAtom"hard-locale#str.32" ge_globalsge = Someposix_ptr ∧ find_fnge TAtom"streq" = SomeDefinedstreq_fn ∧ find_fnge TAtom"setlocale_null_r" = SomeDefinedsnr_fn

split ; exact Hg_ _ H₂ |

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

world :

Type

registry :

name → optioncontractworld

wi :

mem → world → gmappiece pval → Prop

SafepointStable₀ :

ge :

Hlinked :

wi_lent :

∀m : mem w : 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 :

contractworld

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 : 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 :

Hstrlen :

registryTAtom"strlen" = Somestrlen_contractworld

Hmemcpy :

registryTAtom"memcpy" = Somememcpy_contractworld

Kcopy :

Kbyte :

Kalloc :

∀q : alloc_req m : mem wd : world h : gmappiece pval base : Z, freshm q base → wim wd h → wiallocatedm q base wd overwriteobj_psbase q h

Hstrcmp :

registryTAtom"strcmp" = Somestrcmp_contractworld

H₁ :

lookupTAtom"hard-locale#str.31" hello_globals = Somec_ptr

H₂ :

lookupTAtom"hard-locale#str.32" hello_globals = Someposix_ptr

Hm :