Filnix wiki

find_fnge TAtom"memeq" = SomeDefinedmemeq_fn

Explore proof 5 tactics

Initial goal

ge :

⊢

ge_modulege = hello_module → find_fnge TAtom"memeq" = SomeDefinedmemeq_fn

intros Hm

ge :

Hm :

⊢

find_fnge TAtom"memeq" = SomeDefinedmemeq_fn

unfold find_fn

ge :

Hm :

⊢

match find_directTAtom"memeq" ge_modulege with

Somed

⇒

Somed

None

⇒

let* t ≔ find_aliasTAtom"memeq" ge_modulege in

find_directt ge_modulege

SomeDefinedmemeq_fn

rewrite Hm

ge :

Hm :

find_directt hello_module

⊢

match find_directTAtom"memeq" hello_module with

Somed

⇒

Somed

None

⇒

let* t ≔ find_aliasTAtom"memeq" hello_module in

SomeDefinedmemeq_fn

vm_compute

ge :

Hm :

⊢

SomeDefinedfn_name ≔ TAtom"memeq"; fn_linkage ≔ TAtom"export"; fn_ret ≔ RClassW; fn_params ≔ P, TAtom"v0"; P, TAtom"v2"; L, TAtom"v4"; fn_blocks ≔ b_label ≔ TAtom"start"; b_phis ≔ [ ]; b_insts ≔ CallCResultTAtom"v9" W GlobalTAtom"memcmp" ArgP TmpTAtom"v0"; ArgP TmpTAtom"v2"; ArgL TmpTAtom"v4"; LetTAtom"v10" W CmpEq W TmpTAtom"v9"; Const0; b_jump ≔ JRetTmpTAtom"v10" = SomeDefinedfn_name ≔ TAtom"memeq"; fn_linkage ≔ TAtom"export"; fn_ret ≔ RClassW; fn_params ≔ P, TAtom"v0"; P, TAtom"v2"; L, TAtom"v4"; fn_blocks ≔ b_label ≔ TAtom"start"; b_phis ≔ [ ]; b_insts ≔ CallCResultTAtom"v9" W GlobalTAtom"memcmp" ArgP TmpTAtom"v0"; ArgP TmpTAtom"v2"; ArgL TmpTAtom"v4"; LetTAtom"v10" W CmpEq W TmpTAtom"v9"; Const0; b_jump ≔ JRetTmpTAtom"v10"

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros Hm

unfold find_fn

rewrite Hm

vm_compute

reflexivity

Hello's program_name: an 8-byte cell at 66080.

98Definition program_name_b: Z ≔

66080

The literal "/.libs/" of progname.c, read-only at 66112.

100Definition libs_ptr: ptr ≔

mkPtr66112 Ro66112

Its bytes.

102Definition libs_bytes: listZ ≔

47; 46; 108; 105; 98; 115; 47

The literal "lt-" of progname.c, read-only at 66144.

104Definition lt_ptr: ptr ≔

mkPtr66144 Ro66144

Its bytes.

106Definition lt_bytes: listZ ≔

108; 116; 45

Hello's symbols put program_name and the two literals there.

109Lemma progname_globals

lookupTAtom"program_name" hello_globals = SomemkPtrprogram_name_b Objprogram_name_b ∧ lookupTAtom"progname#str.3" hello_globals = Somelibs_ptr ∧ lookupTAtom"progname#str.4" hello_globals = Somelt_ptr

Explore proof 2 tactics

Initial goal

⊢

lookupTAtom"program_name" hello_globals = Someptr_addr ≔ program_name_b; ptr_cap ≔ Objprogram_name_b ∧ lookupTAtom"progname#str.3" hello_globals = Somelibs_ptr ∧ lookupTAtom"progname#str.4" hello_globals = Somelt_ptr

vm_compute

⊢

Someptr_addr ≔ 66080; ptr_cap ≔ Obj66080 = Someptr_addr ≔ 66080; ptr_cap ≔ Obj66080 ∧ Someptr_addr ≔ 66112; ptr_cap ≔ Ro66112 = Someptr_addr ≔ 66112; ptr_cap ≔ Ro66112 ∧ Someptr_addr ≔ 66144; ptr_cap ≔ Ro66144 = Someptr_addr ≔ 66144; ptr_cap ≔ Ro66144

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

vm_compute

auto

set_program_name over any runtime R.

116Module HelloNameOn R : Runtime LG₀ : LogicSigR

117Module HL ≔ HelloLeafOn R LG0

118Module ML ≔ HL.ML

119Module SL ≔ ML.SL

120Module LG ≔ ML.LG

121Module L ≔ LG.L

Import L LG SL ML HL

124Section name

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

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

The genv links Hello, with the contracts the function calls.

130Context Hlinked : hello_linkedge

130Context Hstrrchr : registryTAtom"strrchr" = Somestrrchr_contractworld

130Context Hmemcmp : registryTAtom"memcmp" = Somememcmp_contractworld

130Context Hstrncmp : registryTAtom"strncmp" = Somestrncmp_contractworld

A pointer store into the cell at offset 0 of the object b, with the region reg, keeps the world interpretation, whatever it held and whatever it now holds (wp_raw_store_pointer's premise).

138Definition store_keepsb : Z reg : region : Prop ≔

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

The three cells: program_name in the object 66080 with the region pn, libc's program_invocation_name in the object nb with nreg, and program_invocation_short_name in sb with sreg, each its own object, as each Fil-C global is.

150Context pn nreg sreg : region

150Context nb sb : Z

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

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

150Context Hpn_end : program_name_b + 8 ≤ r_endpn

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

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

150Context Kpn : store_keepsprogram_name_b pn

150Context Knb : store_keepsnb nreg

150Context Ksb : store_keepssb sreg

The Iris instance of the registry and wi.

159Instance name_irisGS: irisGS_genhlc nanofil_langregistry ge Σ ≔

nanofil_irisGSregistry wi ge

The expressions of the language.

163Notation nexpr ≔ language.exprnanofil_langregistry ge

The three cells, holding x, x and y.

166Definition name_cellsx₀ x₁ y : ptr : iPropΣ ≔

liveprogram_name_b pn ∗ pcellprogram_name_b 0 x₀ ∗ livenb nreg ∗ pcellnb 0 x₁ ∗ livesb sreg ∗ pcellsb 0 y

The two literals, as strings.

171Definition literalsr₃ r₄ : region : iPropΣ ≔

stringlibs_ptr 66112 r₃ libs_bytes ∗ stringlt_ptr 66144 r₄ lt_bytes

The genv's program_name and literals are Hello's.

175Lemma name_lookups

lookupTAtom"program_name" ge_globalsge = SomemkPtrprogram_name_b Objprogram_name_b ∧ lookupTAtom"progname#str.3" ge_globalsge = Somelibs_ptr ∧ lookupTAtom"progname#str.4" ge_globalsge = Somelt_ptr

Explore proof 4 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 :

Hstrrchr :

registryTAtom"strrchr" = Somestrrchr_contractworld

Hmemcmp :

registryTAtom"memcmp" = Somememcmp_contractworld

Hstrncmp :

registryTAtom"strncmp" = Somestrncmp_contractworld

pn, nreg, sreg :

nb, sb :

Hnb :

lookupTAtom"program_invocation_name" ge_globalsge = Someptr_addr ≔ nb; ptr_cap ≔ Objnb

Hsb :

lookupTAtom"program_invocation_short_name" ge_globalsge = Someptr_addr ≔ sb; ptr_cap ≔ Objsb

Hpn_end :

program_name_b + 8 ≤ r_endpn

Hnb_cell :

0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48

Hsb_cell :

0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48

Kpn :

Knb :

store_keepsnb nreg

Ksb :

store_keepssb sreg

⊢

lookupTAtom"program_name" ge_globalsge = Someptr_addr ≔ program_name_b; ptr_cap ≔ Objprogram_name_b ∧ lookupTAtom"progname#str.3" ge_globalsge = Somelibs_ptr ∧ lookupTAtom"progname#str.4" ge_globalsge = Somelt_ptr

destruct progname_globals as H₁ & 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 :

Hstrrchr :

registryTAtom"strrchr" = Somestrrchr_contractworld

Hmemcmp :

registryTAtom"memcmp" = Somememcmp_contractworld

Hstrncmp :

registryTAtom"strncmp" = Somestrncmp_contractworld

pn, nreg, sreg :

nb, sb :

Hnb :

lookupTAtom"program_invocation_name" ge_globalsge = Someptr_addr ≔ nb; ptr_cap ≔ Objnb

Hsb :

lookupTAtom"program_invocation_short_name" ge_globalsge = Someptr_addr ≔ sb; ptr_cap ≔ Objsb

Hpn_end :

program_name_b + 8 ≤ r_endpn

Hnb_cell :

0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48

Hsb_cell :

0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48

Kpn :

Knb :

store_keepsnb nreg

Ksb :

store_keepssb sreg

H₁ :

lookupTAtom"program_name" hello_globals = Someptr_addr ≔ program_name_b; ptr_cap ≔ Objprogram_name_b

H₂ :

lookupTAtom"progname#str.3" hello_globals = Somelibs_ptr

H₃ :

lookupTAtom"progname#str.4" hello_globals = Somelt_ptr

⊢

destruct Hlinked as _ & 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 :

Hstrrchr :

registryTAtom"strrchr" = Somestrrchr_contractworld

Hmemcmp :

registryTAtom"memcmp" = Somememcmp_contractworld

Hstrncmp :

registryTAtom"strncmp" = Somestrncmp_contractworld

pn, nreg, sreg :

nb, sb :

Hnb :

lookupTAtom"program_invocation_name" ge_globalsge = Someptr_addr ≔ nb; ptr_cap ≔ Objnb

Hsb :

lookupTAtom"program_invocation_short_name" ge_globalsge = Someptr_addr ≔ sb; ptr_cap ≔ Objsb

Hpn_end :

program_name_b + 8 ≤ r_endpn

Hnb_cell :

0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48

Hsb_cell :

0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48

Kpn :

Knb :

store_keepsnb nreg

Ksb :

store_keepssb sreg

H₁ :

lookupTAtom"program_name" hello_globals = Someptr_addr ≔ program_name_b; ptr_cap ≔ Objprogram_name_b

H₂ :

lookupTAtom"progname#str.3" hello_globals = Somelibs_ptr

H₃ :

lookupTAtom"progname#str.4" hello_globals = Somelt_ptr

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 :

Hstrrchr :

registryTAtom"strrchr" = Somestrrchr_contractworld

Hmemcmp :

registryTAtom"memcmp" = Somememcmp_contractworld

Hstrncmp :

registryTAtom"strncmp" = Somestrncmp_contractworld

pn, nreg, sreg :

nb, sb :

Hnb :

lookupTAtom"program_invocation_name" ge_globalsge = Someptr_addr ≔ nb; ptr_cap ≔ Objnb

Hsb :

lookupTAtom"program_invocation_short_name" ge_globalsge = Someptr_addr ≔ sb; ptr_cap ≔ Objsb

Hpn_end :

program_name_b + 8 ≤ r_endpn

Hnb_cell :

0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48

Hsb_cell :

0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48

Kpn :

Knb :

store_keepsnb nreg

Ksb :

store_keepssb sreg

H₁ :

lookupTAtom"program_name" hello_globals = Someptr_addr ≔ program_name_b; ptr_cap ≔ Objprogram_name_b

H₂ :

lookupTAtom"progname#str.3" hello_globals = Somelibs_ptr

H₃ :

lookupTAtom"progname#str.4" hello_globals = Somelt_ptr

Hg :

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

⊢

lookupTAtom"progname#str.3" ge_globalsge = Somelibs_ptr ∧ lookupTAtom"progname#str.4" ge_globalsge = Somelt_ptr

split ; exact Hg_ _ H₂ | exact Hg_ _ H₃

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

destruct progname_globals as H₁ & H₂ & H₃

destruct Hlinked as _ & Hg & _

split ; exact Hg_ _ H₁ |

split ; exact Hg_ _ H₂ | exact Hg_ _ H₃

The stores, from L18 after its phis, where pr.1 reads as x and pr.3 as y: each cell's check passes and its store keeps the world interpretation.

187Lemma spn_L18

∀ e x y x₀ x₁ y₀ Φ

lookupTAtom"pr.1" e = SomeWPtrx

lookupTAtom"pr.3" e = SomeWPtry

name_cellsx₀ x₁ y₀ −∗ ▷name_cellsx x y −∗ ΦRetVoid −∗ WPERunmkFrameset_program_name_fn e [ ] None ExecTAtom"L18" b_instss_L18 b_jumps_L18 : nexpr {Φ}

Proof 38 steps Qed

intros Hx Hy

destruct name_lookups as Hpn & _ & _

destruct Hnb_cell as Hn₀ & Hn₈ & Hnend & Hn₄₈

destruct Hsb_cell as Hs₀ & Hs₈ & Hsend & Hs₄₈

iIntros (Hlp & Hcp & Hln & Hcn & Hls & Hcs) HΦ

cbn [ b_insts b_jump s_L18 ]

unfold program_name_b in *

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

iNext

iNext

iIntros Hlp

iNext

iIntros Hlp Hcp

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

iNext

iNext

iIntros Hln

iNext

iIntros Hln Hcn

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

iNext

iNext

iIntros Hls

iNext

iIntros Hls Hcs

iApply wp_ret_void

iNext

iApply HΦ

iFrame

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

222Ltac all_cases ≔

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

The "lt-" test, from L16, with v15 reading as the base name, the suffix of argv0 from its j-th byte: strncmp of it and "lt-", and either answer goes on to the stores, past "lt-" or not.

228Lemma spn_L16

∀ e p b reg ys j r₃ r₄ x₀ x₁ y₀ Φ

lookupTAtom"v15" e = SomeWPtrmkPtrptr_addrp + Z.of_natj ptr_capp

j ≤ lengthys%nat

stringp b reg ys −∗ literalsr₃ r₄ −∗ name_cellsx₀ x₁ y₀ −∗ ▷∀x y, ⌜ptr_capx = ptr_capp ∧ ptr_capy = ptr_capp⌝ −∗ stringp b reg ys −∗ literalsr₃ r₄ −∗ name_cellsx x y −∗ ΦRetVoid −∗ WPERunmkFrameset_program_name_fn e [ ] None ExecTAtom"L16" b_instss_L16 b_jumps_L16 : nexpr {Φ}

Proof 44 steps Qed

intros Hv₁₅ Hj

destruct name_lookups as _ & _ & Hlt

iIntros Hs [Hlibs Hlt] Hc HΦ

iDestruct Hs as [%Hok Hps]

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

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

cbn [ b_insts b_jump s_L16 ]

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

iNext

iDestruct string_suffix_ _ _ _ j with Hs as [Hsuf Hback] ; exact Hj |

iNext

iIntros bits Hsuf Hlt

iDestruct Hback with Hsuf as Hs

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

iNext

iApply wp_branch ; word_premise |

iNext

all_cases

–iApply wp_enter ; exact find_s_L18 | word_premise |

iNext

iApply spn_L18 with Hc ; reflexivity | reflexivity |

iNext

iIntros Hc

iApply HΦ with [%] Hs [$Hlibs $Hlt] Hc

split ; reflexivity

–iApply wp_enter ; exact find_s_L35 | reflexivity |

iNext

cbn [ b_insts b_jump s_L35 ]

iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ ptr_addrp + Z.of_natj + 3 ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |

iNext

iApply wp_goto

iNext

iApply wp_enter ; exact find_s_L18 | word_premise |

iNext

iApply spn_L18 with Hc ; reflexivity | reflexivity |

iNext

iIntros Hc

iApply HΦ with [%] Hs [$Hlibs $Hlt] Hc

split ; reflexivity

From L8, with v15 reading as the base name, the suffix of argv0 from its j-th byte, and v0 as argv0: if seven bytes precede the base name, memeq compares them with "/.libs/"; whatever it says, the run goes on to the "lt-" test or to the stores.

266Lemma spn_L8

∀ e p b reg ys j r₃ r₄ x₀ x₁ y₀ Φ

lookupTAtom"v15" e = SomeWPtrmkPtrptr_addrp + Z.of_natj ptr_capp

lookupTAtom"v0" e = SomeWPtrp

j ≤ lengthys%nat

Proof 93 steps Qed

intros Hv₁₅ Hv₀ Hj

destruct name_lookups as _ & Hlibs & _

iIntros Hs [Hl₃ Hl₄] Hc HΦ

iDestruct Hs as [%Hok Hps]

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

pose proof Hok as Hcap & Hb₀ & Hb₁ & Hb₂ & Hb₃ & Hys

cbn [ b_insts b_jump s_L8 ]

assert Hjz : Z.of_natj ≤ Z.of_natlengthys by lia

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_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise |

iNext

destruct Nat.lt_ge_casesj 7 as Hj₇ | Hj₇

Fewer than seven bytes precede the base name.

–assert Hz₇ : Z.of_natj < 7 by lia

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

iNext

cbn [ Z.eqb edge_label ]

iApply wp_enter ; exact find_s_L26 | reflexivity |

iNext

cbn [ b_insts b_jump s_L26 ]

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

iNext

cbn [ Z.eqb edge_label ]

iApply wp_enter ; exact find_s_L18 | word_premise |

iNext

iApply spn_L18 with Hc ; word_premise | word_premise |

iNext

iIntros Hc

iApply HΦ with [%] Hs [$Hl₃ $Hl₄] Hc

split ; reflexivity

Compare the seven bytes before it with "/.libs/".

–assert Hz₇ : 7 ≤ Z.of_natj by lia

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

iNext

cbn [ Z.eqb edge_label ]

iApply wp_enter ; exact find_s_L25 | reflexivity |

iNext

cbn [ b_insts b_jump s_L25 ]

iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ b + ptr_addrp − b + Z.of_natj − 7 ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |

iNext

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

iNext

iDestruct string_window_ _ _ _ j − 7 7 with Hs as (_ & Hl & Hw & Hback) ; lia |

iDestruct string_window_ _ _ _ 0 7 with Hl₃ as (%Hok₃ & Hl₃ & Hw₃ & Hback₃) ; cbn ; lia |

pose proof Hok3 as _ & _ & _ & H3end & _

iApply wp_call_bind_ _ _ _ _ _ _ _ _ _ _ _ _ memeq_fn invocationmemeq_fn WPtrmkPtrb + ptr_addrp − b + Z.of_natj − 7 ptr_capp; WPtrlibs_ptr; WInt7 ; word_premise | apply find_memeq ; exact proj1Hlinked | reflexivity |

iNext

iApply memeq_specregistry wi ge Hlinked b reg ptr_addrp − b + Z.of_natj − 7 _ ptr_capp 66112 r3 ptr_addrlibs_ptr − 66112 + Z.of_nat0 _ Ro66112 with Hl Hw Hl₃ Hw₃ ; exact Hmemcmp | rewrite length_take length_drop ; lia | exact Hcap | right ; reflexivity | rewrite ! length_take ! length_drop ; cbn [ length libs_bytes ] ; lia | lia | cbn ; lia | rewrite length_take length_drop ; lia | rewrite length_take length_drop ; cbn [ ptr_addr libs_ptr length libs_bytes ] in H3end |- * ; lia | rewrite length_take length_drop ; lia | apply Forall_take , Forall_drop ; eapply Forall_impl ; exact Hys | intros x Hx ; cbn in Hx ; lia | vm_compute ; repeat constructor ; discriminate |

iNext

iIntros k Hl Hw Hl₃ Hw₃

iDestruct Hback with Hl Hw as Hs

iDestruct Hback₃ with Hl₃ Hw₃ as Hl₃

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_goto

iNext

iApply wp_enter ; exact find_s_L26 | word_premise |

iNext

cbn [ b_insts b_jump s_L26 ]