Filnix wiki

⊢

call_framescan_fn WPtrp = Somescan_entryp

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

reflexivity

The contracts scan is linked with: strlen, strchr and puts, the last with the trusted stream representation rep.

96Definition scan_registryrep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop symbol : name : optioncontractstdio_world ≔

name_eqbsymbol TAtom"strlen"

→

Somestrlen_contractstdio_world

name_eqbsymbol TAtom"strchr"

→

Somestrchr_contractstdio_world

name_eqbsymbol TAtom"puts"

→

Someputs_contractrep requests

else

None

The raw address of a at offset 0 is a, inside the address space.

105Lemma raw_address_0

∀ a

0 ≤ a < 2 ^ 64

raw_addressa 0 = a

rewrite Z.add_0_r

apply Z.mod_small

exact H

Prove an address premise: drop the wraps of raw_address and of the flight's sum where arithmetic shows them the identity, then arithmetic.

111Ltac addr_premise ≔

cbn [ ptr_addr ] ; unfold raw_address ; drop_wraps_goal ; arith

scan over any runtime R.

114Module ScanLogic R : Runtime

115Module SL ≔ StringLogic R

116Module LG ≔ SL.LG

117Module L ≔ LG.L

Import L LG SL

The linked genv: the module, its symbol, R's free.

121Definition scan_ge: genv ≔

mkGenvscan_module scan_globals R.free

123Section proof

puts's trusted stream representation and allocation requests.

125Variable rep : mem → stdio_world → Prop

126Variable requests : listword → mem → stdio_world → Z → Z → Prop

Hi.v's premise: a safepoint keeps rep and readiness.

129Hypothesis stdio_stable

∀ s m s′ m′ w

R.safepoints m s′ m′

repm w

stdio_wi_safepointrep stdio_stable

repm′ w ∧ stdio_readym′ w

stdio_wi survives safepoints, by stdio_stable.

133Instance scan_wi_stable: SafepointStablestdio_wirep ≔

135Section wp

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

The Iris instance of scan: its contracts and stdio_wi.

139Instance scan_irisGS: irisGS_genhlc nanofil_langscan_registryrep requests scan_ge Σ ≔

nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge

The expressions of scan's language.

143Notation sexpr ≔ language.exprnanofil_langscan_registryrep requests scan_ge

scan, owning the string at p, is safe and returns an int.

146Lemma scan_spec

∀ p b reg bytes

stringp b reg bytes −∗ WPERunscan_entryp : sexpr {o. ⌜∃n, o = RetWIntn⌝}

Proof 70 steps Qed

iIntros Hs

iDestruct Hs as [%Hok Hps]

iAssert stringp b reg bytes with [$Hps] as Hs ; done |

pose proof Hok as Hc & Hb₀ & Hb₁ & Hb₂ & Hb₃ & _

iApply wp_enter ; exact find_start | reflexivity |

iNext

cbn [ b_insts b_jump s_start ]

iApply wp_strlen with Hs ; reflexivity | reflexivity | reflexivity | reflexivity |

iNext

iIntros Hs

iNext

iIntros q Hq Hs

destruct Hq as i & x & Hx & Hxc & _ & → | _ & →

A hit at i, before the NUL.

–assert Hi : i < lengthbytes%nat by apply lookup_lt_Some in Hx ; exact Hx

assert Hz : ptr_addrp + Z.of_nati =? 0 = false by apply Z.eqb_neq ; lia

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

iNext

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

iNext

iApply wp_branch ; reflexivity |

iNext

rewrite Z.mod_smallptr_addrp + Z.of_nati ; | lia

rewrite Hz

cbn [ Z.eqb edge_label ]

iApply wp_enter ; exact find_L10 | reflexivity |

iNext

cbn [ b_insts b_jump s_L10 ]

iDestruct string_suffix_ _ _ _ i with Hs as [Hq _] ; lia |

iApply wp_puts with Hq ; reflexivity | reflexivity | reflexivity | reflexivity |

iNext

iIntros n Hq

iApply wp_flight ; reflexivity | reflexivity | reflexivity |

iNext

destruct dropi bytes as | x₀ rest eqn: Ed

{exfalso

apply f_equallength in Ed

rewrite length_drop in Ed

cbn in Ed

lia

iDestruct string_byte_ _ _ _ 1 nth0 rest ++ 0 0 with Hq as (%Hok′ & Hl & Hb & _)

{destruct rest ; reflexivity

iNext

iIntros Hl

iNext

iIntros _ _

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

iNext

iApply wp_ret ; exact scan_ret | reflexivity |

iNext

iPureIntro

eexists

reflexivity

A miss: return 0.

–iApply wp_let ; reflexivity | reflexivity | reflexivity | intros m ; reflexivity |

iNext

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

iNext

iApply wp_branch ; reflexivity |

iNext

cbn [ Z.eqb edge_label ]

iApply wp_enter ; exact find_L8 | reflexivity |

iNext

cbn [ b_insts b_jump s_L8 ]

iApply wp_ret ; exact scan_ret | reflexivity |

iNext

iPureIntro

eexists

reflexivity

scan is safe: from a ready runtime, live objects apart, puts's rep and readiness of the world, and a string at p, in an object no root of the world reaches into, with any fuel, no labelled run stops with a failure_ending, and a run that returns returns an int. By heap_labelled_safe from scan_spec, the ghost heap starting with the string's pieces.

198Theorem scan_logic_safe

∀ Σ HinvP : invGpreSΣ HheapP : gen_heapGpreSpiece pval Σ m s w fuel p b reg bytes

R.readys m

repm w

string_okp b reg bytes

all_agreem string_psp b reg bytes

∀sp a, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

labelled_safescan_registryrep requests scan_ge scan_entryp m s w fuel λo ⇒ ∃n, o = RetWIntn

Explore proof 21 tactics

Initial goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

⊢

R.readys m → live_disjointm → repm w → stdio_readym w → string_okp b reg bytes → all_agreem string_psp b reg bytes → ∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg → labelled_safescan_registryrep requests scan_ge scan_entryp m s w fuel λo : outcome ⇒ ∃n : Z, o = RetWIntn

intros Hr Hd Hrep Hw Hok Ha Hapart

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

labelled_safescan_registryrep requests scan_ge scan_entryp m s w fuel λo : outcome ⇒ ∃n : Z, o = RetWIntn

apply heap_labelled_safeΣ scan_registryrep requests stdio_wirep scan_ge scan_entryp m s w list_to_mapstring_psp b reg bytes

5 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

R.readys m

focused goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

focused goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

agreesm list_to_mapstring_psp b reg bytes

focused goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

stdio_wirep m w list_to_mapstring_psp b reg bytes

focused goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapstring_psp b reg bytes}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

–exact Hr

4 open

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

agreesm list_to_mapstring_psp b reg bytes

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

stdio_wirep m w list_to_mapstring_psp b reg bytes

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapstring_psp b reg bytes}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

–exact Hd

3 open

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

agreesm list_to_mapstring_psp b reg bytes

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

stdio_wirep m w list_to_mapstring_psp b reg bytes

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapstring_psp b reg bytes}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

–intros l v Hl

3 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

l :

v :

Hl :

list_to_mapstring_psp b reg bytes !! l = Somev

⊢

agree_piecem l v

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

stdio_wirep m w list_to_mapstring_psp b reg bytes

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapstring_psp b reg bytes}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

exact all_agree_elem_ _ _ _ Ha elem_of_list_to_map_2_ _ _ Hl

2 open

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

stdio_wirep m w list_to_mapstring_psp b reg bytes

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapstring_psp b reg bytes}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

–split ; exact Hrep |

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

stdio_readym w ∧ roots_apartstdio_rootsw list_to_mapstring_psp b reg bytes m

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapstring_psp b reg bytes}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

split ; exact Hw |

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

roots_apartstdio_rootsw list_to_mapstring_psp b reg bytes m

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapstring_psp b reg bytes}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

intros sp a Hin Hs l & v & reg′ & Hl & _ & E _ & Hb

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

sp :

a :

Hin :

Insp stdio_rootsw

Hs :

l :

v :

reg′ :

Hl :

list_to_mapstring_psp b reg bytes !! l = Somev

E :

object_regionpiece_idl m_regionsm = Somereg′

Hb :

piece_idl ≤ a < r_endreg′

⊢

False

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapstring_psp b reg bytes}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

apply elem_of_list_to_map_2 in Hl

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

sp :

a :

Hin :

Insp stdio_rootsw

Hs :

l :

v :

reg′ :

Hl :

l, v ∈ string_psp b reg bytes

E :

object_regionpiece_idl m_regionsm = Somereg′

Hb :

piece_idl ≤ a < r_endreg′

⊢

False

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapstring_psp b reg bytes}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

rewrite string_ps_id_ _ _ _ _ _ Hl in E , Hb

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

sp :

a :

Hin :

Insp stdio_rootsw

Hs :

l :

v :

reg′ :

Hl :

l, v ∈ string_psp b reg bytes

E :

object_regionb m_regionsm = Somereg′

Hb :

b ≤ a < r_endreg′

⊢

False

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapstring_psp b reg bytes}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

destruct Ha as E′ _ _

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

E′ :

object_regionb m_regionsm = Somereg

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

sp :

a :

Hin :

Insp stdio_rootsw

Hs :

l :

v :

reg′ :

Hl :

l, v ∈ string_psp b reg bytes

E :

object_regionb m_regionsm = Somereg′

Hb :

b ≤ a < r_endreg′

⊢

False

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapstring_psp b reg bytes}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

cbn [ fst snd ] in E′

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

E′ :

object_regionb m_regionsm = Somereg

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

sp :

a :

Hin :

Insp stdio_rootsw

Hs :

l :

v :

reg′ :

Hl :

l, v ∈ string_psp b reg bytes

E :

object_regionb m_regionsm = Somereg′

Hb :

b ≤ a < r_endreg′

⊢

False

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapstring_psp b reg bytes}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

rewrite E′ in E

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

E′ :

object_regionb m_regionsm = Somereg

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

sp :

a :

Hin :

Insp stdio_rootsw

Hs :

l :

v :

reg′ :

Hl :

l, v ∈ string_psp b reg bytes

Hb :

b ≤ a < r_endreg′

E :

Somereg = Somereg′

⊢

False

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapstring_psp b reg bytes}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

injection E as ←

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

E′ :

object_regionb m_regionsm = Somereg

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

sp :

a :

Hin :

Insp stdio_rootsw

Hs :

l :

v :

Hl :

l, v ∈ string_psp b reg bytes

Hb :

b ≤ a < r_endreg

⊢

False

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapstring_psp b reg bytes}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

exact Hapartsp a Hin Hs Hb

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapstring_psp b reg bytes}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

–intros HinvG HheapG

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

⊢

∗_{l↦v∈list_to_mapstring_psp b reg bytes}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

rewrite big_sepM_list_to_map ; | exact string_ps_nodupp b reg bytes

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

⊢

∗_{xk∈string_psp b reg bytes}pointstoxk.1 DfracOwn1 xk.2

⊢

let H ≔ nanofil_irisGSscan_registryrep requests stdio_wirep scan_ge in

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

iIntros Hs

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

Hs :

∗_{xk∈string_psp b reg bytes}pointstoxk.1 DfracOwn1 xk.2

∗

WPScanLogic.LG.L.ERunscan_entryp {o. ⌜∃n : Z, o = RetWIntn⌝}

iApply scan_specp b reg bytes with [$Hs]

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

stdio_stable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

w :

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hrep :

repm w

Hw :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

Hapart :

∀sp : span a : Z, Insp stdio_rootsw → span_containssp a → ¬b ≤ a < r_endreg

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

∗

⌜string_okp b reg bytes⌝

done

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros Hr Hd Hrep Hw Hok Ha Hapart

apply heap_labelled_safeΣ scan_registryrep requests stdio_wirep scan_ge scan_entryp m s w list_to_mapstring_psp b reg bytes

–exact Hr

–exact Hd

–intros l v Hl

exact all_agree_elem_ _ _ _ Ha elem_of_list_to_map_2_ _ _ Hl

–split ; exact Hrep |

split ; exact Hw |

intros sp a Hin Hs l & v & reg′ & Hl & _ & E _ & Hb

apply elem_of_list_to_map_2 in Hl

rewrite string_ps_id_ _ _ _ _ _ Hl in E , Hb

destruct Ha as E′ _ _

cbn [ fst snd ] in E′

rewrite E′ in E

injection E as ←

exact Hapartsp a Hin Hs Hb

–intros HinvG HheapG

rewrite big_sepM_list_to_map ; | exact string_ps_nodupp b reg bytes

iIntros Hs

iApply scan_specp b reg bytes with [$Hs]

done

The interpreter's runtime

scan over the interpreter's runtime.

226Module InterpScanLogic ≔ ScanLogic InterpRuntime

scan is safe under the interpreter's runtime, called with Hi.v's literal "hello" in Hi.v's fixture memory, with the fixture's stream representation.

231Theorem interp_scan_logic_safe

∀ fuel

InterpScanLogic.L.labelled_safescan_registryfixture_rep fixture_requests InterpScanLogic.scan_ge scan_entryhi_literal HiChecks.memory InterpRuntime.start hello_world fuel λo ⇒ ∃n, o = RetWIntn

Explore proof 19 tactics

Initial goal

⊢

∀fuel : Z, InterpScanLogic.L.labelled_safescan_registryfixture_rep fixture_requests InterpScanLogic.scan_ge scan_entryhi_literal HiChecks.memory InterpRuntime.start hello_world fuel λo : outcome ⇒ ∃n : Z, o = RetWIntn

intros fuel

fuel :

⊢

InterpScanLogic.L.labelled_safescan_registryfixture_rep fixture_requests InterpScanLogic.scan_ge scan_entryhi_literal HiChecks.memory InterpRuntime.start hello_world fuel λo : outcome ⇒ ∃n : Z, o = RetWIntn

destruct HiChecks.entry_pre as Hrep & Hw & Hv

fuel :

Hrep :

Hw :

Hv :

⊢

apply InterpScanLogic.scan_logic_safefixture_rep fixture_requests HiChecks.interpreter_stdio_stablefixture_rep hiΣ _ _ _ _ _ 65552 lit_reg hello_bytes

7 open

fuel :

Hrep :

Hw :

Hv :

InterpRuntime.readyInterpRuntime.start HiChecks.memory

⊢

focused goal

fuel :

Hrep :

Hw :

Hv :

live_disjointHiChecks.memory

⊢

focused goal

fuel :

Hrep :

Hw :

Hv :

⊢

focused goal

fuel :

Hrep :

Hw :

Hv :

⊢

focused goal

fuel :

Hrep :

Hw :

Hv :

⊢

focused goal

fuel :

Hrep :

Hw :

Hv :

⊢

all_agreeHiChecks.memory string_pshi_literal 65552 lit_reg hello_bytes

focused goal

fuel :

Hrep :

Hw :

Hv :

⊢

∀sp : span a : Z, Insp stdio_rootshello_world → span_containssp a → ¬65552 ≤ a < r_endlit_reg

–exact hi_memory_ready

6 open

deferred goal

fuel :

Hrep :

Hw :

Hv :

live_disjointHiChecks.memory

⊢

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

all_agreeHiChecks.memory string_pshi_literal 65552 lit_reg hello_bytes

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

∀sp : span a : Z, Insp stdio_rootshello_world → span_containssp a → ¬65552 ≤ a < r_endlit_reg

–exact hi_memory_disjoint

5 open

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

all_agreeHiChecks.memory string_pshi_literal 65552 lit_reg hello_bytes

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

∀sp : span a : Z, Insp stdio_rootshello_world → span_containssp a → ¬65552 ≤ a < r_endlit_reg

–exact Hrep

4 open

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

all_agreeHiChecks.memory string_pshi_literal 65552 lit_reg hello_bytes

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

∀sp : span a : Z, Insp stdio_rootshello_world → span_containssp a → ¬65552 ≤ a < r_endlit_reg

–exact Hw

3 open

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

all_agreeHiChecks.memory string_pshi_literal 65552 lit_reg hello_bytes

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

∀sp : span a : Z, Insp stdio_rootshello_world → span_containssp a → ¬65552 ≤ a < r_endlit_reg

–unfold string_ok

3 open

fuel :

Hrep :

Hw :

Hv :

⊢

ptr_caphi_literal = Obj65552 ∨ ptr_caphi_literal = Ro65552 ∧ 0 < 65552 ∧ 65552 ≤ ptr_addrhi_literal ∧ ptr_addrhi_literal + lengthhello_bytes + 1 ≤ r_endlit_reg ∧ r_endlit_reg ≤ 2 ^ 48 ∧ Forallλx : Z ⇒ 0 < x < 256 hello_bytes

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

all_agreeHiChecks.memory string_pshi_literal 65552 lit_reg hello_bytes

deferred goal

fuel :

Hrep :

Hw :

Hv :

⊢

∀sp : span a : Z, Insp stdio_rootshello_world → span_containssp a → ¬65552 ≤ a < r_endlit_reg

cbn

3 open

fuel :

Hrep :

Hw :

Hv :

⊢

Ro65552 = Obj65552 ∨ Ro65552 = Ro65552 ∧ 0 < 65552 ∧ 65552 ≤ 65552 ∧ 65552 + 5%nat + 1 ≤ 65560 ∧ 65560 ≤ 2 ^ 48 ∧ Forallλx : Z ⇒ 0 < x < 256 hello_bytes

deferred goal

fuel :

Hrep :

Hw :

Hv :