Filnix wiki

bytes :

listZ

c :

q :

⊢

strchr_foundp bytes c q → found_fromp bytes q

intros i & x & Hx & _ & _ & → | _ & → ; right | left ; reflexivity

p :

bytes :

listZ

c :

i :

nat

x :

Hx :

bytes !! i = Somex

⊢

∃j : nat, j < lengthbytes%nat ∧ ptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp = ptr_addr ≔ ptr_addrp + j; ptr_cap ≔ ptr_capp

exists i

p :

bytes :

listZ

c :

i :

nat

x :

Hx :

bytes !! i = Somex

⊢

i < lengthbytes%nat ∧ ptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp = ptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp

split ; exact lookup_lt_Some_ _ _ Hx | reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros i & x & Hx & _ & _ & → | _ & → ; right | left ; reflexivity

exists i

split ; exact lookup_lt_Some_ _ _ Hx | reflexivity

What strchr finds in the suffix just past the j-th byte of the string, before its NUL, is null or before the string's NUL.

145Lemma found_next

∀ p bytes c q j

j < lengthbytes%nat

strchr_foundmkPtrptr_addrp + Z.of_natSj ptr_capp dropSj bytes c q

found_fromp bytes q

Explore proof 7 tactics

Initial goal

p :

bytes :

listZ

c :

q :

j :

nat

⊢

j < lengthbytes%nat → strchr_foundptr_addr ≔ ptr_addrp + Sj; ptr_cap ≔ ptr_capp dropSj bytes c q → found_fromp bytes q

intros Hj i & x & Hx & _ & _ & → | _ & → ; right | left ; reflexivity

p :

bytes :

listZ

c :

j :

nat

Hj :

j < lengthbytes%nat

i :

nat

x :

Hx :

dropSj bytes !! i = Somex

⊢

∃j₀ : nat, j₀ < lengthbytes%nat ∧ ptr_addr ≔ ptr_addrptr_addr ≔ ptr_addrp + Sj; ptr_cap ≔ ptr_capp + i; ptr_cap ≔ ptr_capptr_addr ≔ ptr_addrp + Sj; ptr_cap ≔ ptr_capp = ptr_addr ≔ ptr_addrp + j₀; ptr_cap ≔ ptr_capp

rewrite lookup_drop in Hx

p :

bytes :

listZ

c :

j :

nat

Hj :

j < lengthbytes%nat

i :

nat

x :

Hx :

bytes !! Sj + i%nat = Somex

⊢

exists Sj + i%nat

p :

bytes :

listZ

c :

j :

nat

Hj :

j < lengthbytes%nat

i :

nat

x :

Hx :

bytes !! Sj + i%nat = Somex

⊢

Sj + i < lengthbytes%nat ∧ ptr_addr ≔ ptr_addrptr_addr ≔ ptr_addrp + Sj; ptr_cap ≔ ptr_capp + i; ptr_cap ≔ ptr_capptr_addr ≔ ptr_addrp + Sj; ptr_cap ≔ ptr_capp = ptr_addr ≔ ptr_addrp + Sj + i%nat; ptr_cap ≔ ptr_capp

split ; exact lookup_lt_Some_ _ _ Hx |

p :

bytes :

listZ

c :

j :

nat

Hj :

j < lengthbytes%nat

i :

nat

x :

Hx :

bytes !! Sj + i%nat = Somex

⊢

ptr_addr ≔ ptr_addrptr_addr ≔ ptr_addrp + Sj; ptr_cap ≔ ptr_capp + i; ptr_cap ≔ ptr_capptr_addr ≔ ptr_addrp + Sj; ptr_cap ≔ ptr_capp = ptr_addr ≔ ptr_addrp + Sj + i%nat; ptr_cap ≔ ptr_capp

cbn [ ptr_addr ptr_cap ]

p :

bytes :

listZ

c :

j :

nat

Hj :

j < lengthbytes%nat

i :

nat

x :

Hx :

bytes !! Sj + i%nat = Somex

⊢

ptr_addr ≔ ptr_addrp + Sj + i; ptr_cap ≔ ptr_capp = ptr_addr ≔ ptr_addrp + Sj + i%nat; ptr_cap ≔ ptr_capp

f_equal

p :

bytes :

listZ

c :

j :

nat

Hj :

j < lengthbytes%nat

i :

nat

x :

Hx :

bytes !! Sj + i%nat = Somex

⊢

ptr_addrp + Sj + i = ptr_addrp + Sj + i%nat

lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros Hj i & x & Hx & _ & _ & → | _ & → ; right | left ; reflexivity

rewrite lookup_drop in Hx

exists Sj + i%nat

split ; exact lookup_lt_Some_ _ _ Hx |

cbn [ ptr_addr ptr_cap ]

f_equal

lia

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

155Definition count_ge: genv ≔

mkGenvcount_module count_globals R.free

next_l is a function of the module.

158Lemma find_next_l

find_fncount_ge TAtom"next_l" = SomeDefinednext_l_fn

Explore proof 2 tactics

Initial goal

⊢

find_fncount_ge TAtom"next_l" = SomeDefinednext_l_fn

vm_compute

⊢

SomeDefinedfn_name ≔ TAtom"next_l"; fn_linkage ≔ TAtom"export"; fn_ret ≔ RClassP; fn_params ≔ P, TAtom"v0"; fn_blocks ≔ b_label ≔ TAtom"start"; b_phis ≔ [ ]; b_insts ≔ CallCResultTAtom"v3" P GlobalTAtom"strchr" ArgP TmpTAtom"v0"; ArgW Const108; b_jump ≔ JRetTmpTAtom"v3" = SomeDefinedfn_name ≔ TAtom"next_l"; fn_linkage ≔ TAtom"export"; fn_ret ≔ RClassP; fn_params ≔ P, TAtom"v0"; fn_blocks ≔ b_label ≔ TAtom"start"; b_phis ≔ [ ]; b_insts ≔ CallCResultTAtom"v3" P GlobalTAtom"strchr" ArgP TmpTAtom"v0"; ArgW Const108; b_jump ≔ JRetTmpTAtom"v3"

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

vm_compute

reflexivity

161Section wp

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

The Iris instance of count.c: strchr's contract, no world.

165Instance count_irisGS: irisGS_genhlc nanofil_langcount_registry count_ge Σ ≔

nanofil_irisGScount_registry no_world count_ge

The expressions of count.c's language.

169Notation cexpr ≔ language.exprnanofil_langcount_registry count_ge

next_l's triple: owning the string at p, it returns what strchr finds of l, and hands the string back.

173Lemma next_l_spec

∀ p b reg bytes Φ

stringp b reg bytes −∗ ▷∀q, ⌜strchr_foundp bytes 108 q⌝ −∗ stringp b reg bytes −∗ ΦRetWPtrq −∗ WPERunentrynext_l_fn p : cexpr {Φ}

Explore proof 11 tactics

Initial goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Φ :

outcome → iPropIΣ

⊢

stringp b reg bytes −∗ ▷∀q : ptr, ⌜strchr_foundp bytes 108 q⌝ −∗ stringp b reg bytes −∗ ΦRetWPtrq −∗ WPERunentrynext_l_fn p : cexpr {v. Φv}

iIntros Hs HΦ

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Φ :

outcome → iPropIΣ

Hs :

stringp b reg bytes

HΦ :

▷∀q : ptr, ⌜strchr_foundp bytes 108 q⌝ −∗ stringp b reg bytes −∗ ΦRetWPtrq

∗

WPERunentrynext_l_fn p {v. Φv}

iApply wp_enter ; exact find_n_start | reflexivity |

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Φ :

outcome → iPropIΣ

Hs :

stringp b reg bytes

HΦ :

▷∀q : ptr, ⌜strchr_foundp bytes 108 q⌝ −∗ stringp b reg bytes −∗ ΦRetWPtrq

∗

▷WPCountLogic.LG.L.ERunfr_fn ≔ next_l_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" b_instsn_start b_jumpn_start {v. Φv}

iNext

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Φ :

outcome → iPropIΣ

Hs :

stringp b reg bytes

HΦ :

∀q : ptr, ⌜strchr_foundp bytes 108 q⌝ −∗ stringp b reg bytes −∗ ΦRetWPtrq

∗

WPCountLogic.LG.L.ERunfr_fn ≔ next_l_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" b_instsn_start b_jumpn_start {v. Φv}

cbn [ b_insts b_jump n_start ]

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Φ :

outcome → iPropIΣ

Hs :

stringp b reg bytes

HΦ :

∀q : ptr, ⌜strchr_foundp bytes 108 q⌝ −∗ stringp b reg bytes −∗ ΦRetWPtrq

∗

WPCountLogic.LG.L.ERunfr_fn ≔ next_l_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" CallCResultTAtom"v3" P GlobalTAtom"strchr" ArgP TmpTAtom"v0"; ArgW Const108 JRetTmpTAtom"v3" {v. Φv}

iApply wp_strchr with Hs ; reflexivity | reflexivity | reflexivity | reflexivity | reflexivity | vm_compute ; intuition congruence | vm_compute ; intuition congruence |

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Φ :

outcome → iPropIΣ

HΦ :

∀q : ptr, ⌜strchr_foundp bytes 108 q⌝ −∗ stringp b reg bytes −∗ ΦRetWPtrq

∗

▷∀q : ptr, ⌜strchr_foundp bytes 108 mod 2 ^ 32 q⌝ −∗ stringp b reg bytes −∗ WPL.ERunfr_fn ≔ next_l_fn; fr_env ≔ putTAtom"v3" WPtrq TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JRetTmpTAtom"v3" {v. Φv}

iNext

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Φ :

outcome → iPropIΣ

HΦ :

∀q : ptr, ⌜strchr_foundp bytes 108 q⌝ −∗ stringp b reg bytes −∗ ΦRetWPtrq

∗

∀q : ptr, ⌜strchr_foundp bytes 108 mod 2 ^ 32 q⌝ −∗ stringp b reg bytes −∗ WPL.ERunfr_fn ≔ next_l_fn; fr_env ≔ putTAtom"v3" WPtrq TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JRetTmpTAtom"v3" {v. Φv}

iIntros q Hq Hs

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Φ :

outcome → iPropIΣ

q :

Hq :

strchr_foundp bytes 108 mod 2 ^ 32 q

HΦ :

∀q₀ : ptr, ⌜strchr_foundp bytes 108 q₀⌝ −∗ stringp b reg bytes −∗ ΦRetWPtrq₀

Hs :

stringp b reg bytes

∗

WPL.ERunfr_fn ≔ next_l_fn; fr_env ≔ putTAtom"v3" WPtrq TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JRetTmpTAtom"v3" {v. Φv}

iApply wp_ret ; reflexivity | reflexivity |

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Φ :

outcome → iPropIΣ

q :

Hq :

strchr_foundp bytes 108 mod 2 ^ 32 q

HΦ :

∀q₀ : ptr, ⌜strchr_foundp bytes 108 q₀⌝ −∗ stringp b reg bytes −∗ ΦRetWPtrq₀

Hs :

stringp b reg bytes

∗

▷ΦRetWPtrq

iNext

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Φ :

outcome → iPropIΣ

q :

Hq :

strchr_foundp bytes 108 mod 2 ^ 32 q

HΦ :

∀q₀ : ptr, ⌜strchr_foundp bytes 108 q₀⌝ −∗ stringp b reg bytes −∗ ΦRetWPtrq₀

Hs :

stringp b reg bytes

∗

ΦRetWPtrq

iApply HΦ with [%] Hs

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Φ :

outcome → iPropIΣ

q :

Hq :

strchr_foundp bytes 108 mod 2 ^ 32 q

⊢

strchr_foundp bytes 108 q

exact Hq

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

iIntros Hs HΦ

iApply wp_enter ; exact find_n_start | reflexivity |

iNext

cbn [ b_insts b_jump n_start ]

iNext

iIntros q Hq Hs

iApply wp_ret ; reflexivity | reflexivity |

iNext

iApply HΦ with [%] Hs

exact Hq

The loop, from the point after its head's phis: with pr.2 a pointer null or before the NUL of the string at p, which it owns, and pr.1 an int, the run is safe and returns an int. By Löb induction; each iteration reads the byte at the pointer and calls next_l on the suffix past it.

192Lemma count_loop

∀ p b reg bytes

⊢ ∀e q n, ⌜lookupTAtom"pr.2" e = SomeWPtrq ∧ lookupTAtom"pr.1" e = SomeWIntn ∧ found_fromp bytes q⌝ −∗ stringp b reg bytes −∗ WPERunmkFramecount_fn e [ ] None ExecTAtom"L6" b_instsc_L6 b_jumpc_L6 : cexpr {o. ⌜∃k, o = RetWIntk⌝}

Proof 76 steps Qed

iLöb as IH

iIntros e q n Hq & Hn & Hf 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₃ & _

cbn [ b_insts b_jump c_L6 ]

destruct Hf as → | j & Hj & →

Null: the loop ends and returns the count.

–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_c_L9 | reflexivity |

iNext

cbn [ b_insts b_jump c_L9 ]

iApply wp_ret ; reflexivity | word_premise |

iNext

iPureIntro

eexists

reflexivity

A hit at j: read its byte, count it, and call next_l past it.

–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_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |

iNext

cbn [ Z.eqb edge_label ]

iApply wp_enter ; exact find_c_L7 | reflexivity |

iNext

cbn [ b_insts b_jump c_L7 ]

destruct lookup_lt_is_Some_2bytes j Hj as x Hx

iDestruct string_byte_ _ _ _ j x with Hs as (_ & Hl & Hb & Hk) ; by apply lookup_app_l_Some |

iNext

iIntros Hl

iNext

iIntros Hl Hb

iDestruct Hk with Hl Hb as Hs

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_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ ptr_addrp + Z.of_natSj ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |

iNext

iApply wp_call_bind ; word_premise | exact find_next_l | reflexivity |

iNext

iDestruct string_suffix_ _ _ _ Sj with Hs as [Hs Hback] ; lia |

iApply next_l_spec with Hs

iNext

iIntros q′ Hq′ Hs

iDestruct Hback with Hs as Hs

iExists _

iSplit ; iPureIntro ; reflexivity |

iNext

cbn [ fr_fn fr_env fr_locals fr_doomed fr_at ]

iApply wp_goto

iNext

iApply wp_enter ; exact find_c_L6 | word_premise |

iNext

iApply IH with [%] Hs

split ; reflexivity |

exact found_nextp bytes 108 q' j Hj Hq'

count_l, owning the string at p, is safe and returns an int: it calls next_l on the whole string and enters the loop.

241Lemma count_spec

∀ p b reg bytes

stringp b reg bytes −∗ WPERunentrycount_fn p : cexpr {o. ⌜∃k, o = RetWIntk⌝}

Explore proof 21 tactics

Initial goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

⊢

stringp b reg bytes −∗ WPERunentrycount_fn p : cexpr {o. ⌜∃k : Z, o = RetWIntk⌝}

iIntros Hs

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Hs :

stringp b reg bytes

∗

WPERunentrycount_fn p {o. ⌜∃k : Z, o = RetWIntk⌝}

iApply wp_enter ; exact find_c_start | reflexivity |

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Hs :

stringp b reg bytes

∗

▷WPCountLogic.LG.L.ERunfr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" b_instsc_start b_jumpc_start {o. ⌜∃k : Z, o = RetWIntk⌝}

iNext

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Hs :

stringp b reg bytes

∗

WPCountLogic.LG.L.ERunfr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" b_instsc_start b_jumpc_start {o. ⌜∃k : Z, o = RetWIntk⌝}

cbn [ b_insts b_jump c_start ]

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Hs :

stringp b reg bytes

∗

WPCountLogic.LG.L.ERunfr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" CallCResultTAtom"v5" P GlobalTAtom"next_l" ArgP TmpTAtom"v0" JGotoToTAtom"L6" {o. ⌜∃k : Z, o = RetWIntk⌝}

iApply wp_call_bind ; reflexivity | exact find_next_l | reflexivity |

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Hs :

stringp b reg bytes

∗

▷WPCountLogic.LG.L.ERunfr_fn ≔ next_l_fn; fr_env ≔ fold_leftλe : listname × word px : class × name × word ⇒ putpx.1.2 px.2 e combinefn_paramsnext_l_fn takelengthfn_paramsnext_l_fn WPtrp [ ]; fr_locals ≔ mapλxs : name × Z ⇒ xs.1, None local_objectsnext_l_fn; fr_doomed ≔ None; fr_at ≔ if variadic_funcnext_l_fn then SnapshotWPtrp b_labelb_label ≔ TAtom"start"; b_phis ≔ [ ]; b_insts ≔ CallCResultTAtom"v3" P GlobalTAtom"strchr" ArgP TmpTAtom"v0"; ArgW Const108; b_jump ≔ JRetTmpTAtom"v3" else Enterb_labelb_label ≔ TAtom"start"; b_phis ≔ [ ]; b_insts ≔ CallCResultTAtom"v3" P GlobalTAtom"strchr" ArgP TmpTAtom"v0"; ArgW Const108; b_jump ≔ JRetTmpTAtom"v3" None {o. ∃cf′ : frame, ⌜CountLogic.LG.L.resumefr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6" pd_res ≔ CResultTAtom"v5" P; pd_conv ≔ None o = Somecf′⌝ ∗ ▷WPCountLogic.LG.L.ERuncf′ {o₀. ⌜∃k : Z, o₀ = RetWIntk⌝}}

iNext

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

Hs :

stringp b reg bytes

∗

WPCountLogic.LG.L.ERunfr_fn ≔ next_l_fn; fr_env ≔ fold_leftλe : listname × word px : class × name × word ⇒ putpx.1.2 px.2 e combinefn_paramsnext_l_fn takelengthfn_paramsnext_l_fn WPtrp [ ]; fr_locals ≔ mapλxs : name × Z ⇒ xs.1, None local_objectsnext_l_fn; fr_doomed ≔ None; fr_at ≔ if variadic_funcnext_l_fn then SnapshotWPtrp b_labelb_label ≔ TAtom"start"; b_phis ≔ [ ]; b_insts ≔ CallCResultTAtom"v3" P GlobalTAtom"strchr" ArgP TmpTAtom"v0"; ArgW Const108; b_jump ≔ JRetTmpTAtom"v3" else Enterb_labelb_label ≔ TAtom"start"; b_phis ≔ [ ]; b_insts ≔ CallCResultTAtom"v3" P GlobalTAtom"strchr" ArgP TmpTAtom"v0"; ArgW Const108; b_jump ≔ JRetTmpTAtom"v3" None {o. ∃cf′ : frame, ⌜CountLogic.LG.L.resumefr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6" pd_res ≔ CResultTAtom"v5" P; pd_conv ≔ None o = Somecf′⌝ ∗ ▷WPCountLogic.LG.L.ERuncf′ {o₀. ⌜∃k : Z, o₀ = RetWIntk⌝}}

iApply next_l_spec with Hs

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

∗

▷∀q : ptr, ⌜strchr_foundp bytes 108 q⌝ −∗ stringp b reg bytes −∗ ∃cf′ : frame, ⌜CountLogic.LG.L.resumefr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6" pd_res ≔ CResultTAtom"v5" P; pd_conv ≔ None RetWPtrq = Somecf′⌝ ∗ ▷WPCountLogic.LG.L.ERuncf′ {o. ⌜∃k : Z, o = RetWIntk⌝}

iNext

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

∗

∀q : ptr, ⌜strchr_foundp bytes 108 q⌝ −∗ stringp b reg bytes −∗ ∃cf′ : frame, ⌜CountLogic.LG.L.resumefr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6" pd_res ≔ CResultTAtom"v5" P; pd_conv ≔ None RetWPtrq = Somecf′⌝ ∗ ▷WPCountLogic.LG.L.ERuncf′ {o. ⌜∃k : Z, o = RetWIntk⌝}

iIntros q Hq Hs

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

q :

Hq :

strchr_foundp bytes 108 q

Hs :

stringp b reg bytes

∗

∃cf′ : frame, ⌜CountLogic.LG.L.resumefr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6" pd_res ≔ CResultTAtom"v5" P; pd_conv ≔ None RetWPtrq = Somecf′⌝ ∗ ▷WPCountLogic.LG.L.ERuncf′ {o. ⌜∃k : Z, o = RetWIntk⌝}

iExists _

2 open

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

q :

Hq :

strchr_foundp bytes 108 q

Hs :

stringp b reg bytes

∗

⌜CountLogic.LG.L.resumefr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6" pd_res ≔ CResultTAtom"v5" P; pd_conv ≔ None RetWPtrq = Some?f⌝ ∗ ▷WPCountLogic.LG.L.ERun?f {o. ⌜∃k : Z, o = RetWIntk⌝}

shelved goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

q :

Hq :

strchr_foundp bytes 108 q

⊢

frame

iSplit ; iPureIntro ; reflexivity |

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

q :

Hq :

strchr_foundp bytes 108 q

Hs :

stringp b reg bytes

∗

▷WPCountLogic.LG.L.ERunfr_fn ≔ fr_fnfr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6"; fr_env ≔ putTAtom"v5" WPtrq fr_envfr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6"; fr_locals ≔ fr_localsfr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6"; fr_doomed ≔ fr_doomedfr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6"; fr_at ≔ fr_atfr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6" {o. ⌜∃k : Z, o = RetWIntk⌝}

iNext

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

q :

Hq :

strchr_foundp bytes 108 q

Hs :

stringp b reg bytes

∗

WPCountLogic.LG.L.ERunfr_fn ≔ fr_fnfr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6"; fr_env ≔ putTAtom"v5" WPtrq fr_envfr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6"; fr_locals ≔ fr_localsfr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6"; fr_doomed ≔ fr_doomedfr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6"; fr_at ≔ fr_atfr_fn ≔ count_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6" {o. ⌜∃k : Z, o = RetWIntk⌝}

cbn [ fr_fn fr_env fr_locals fr_doomed fr_at ]

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

q :

Hq :

strchr_foundp bytes 108 q

Hs :

stringp b reg bytes

∗

WPCountLogic.LG.L.ERunfr_fn ≔ count_fn; fr_env ≔ putTAtom"v5" WPtrq TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L6" {o. ⌜∃k : Z, o = RetWIntk⌝}

iApply wp_goto

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

q :

Hq :

strchr_foundp bytes 108 q

Hs :

stringp b reg bytes

∗

▷WPCountLogic.LG.L.ERunfr_fn ≔ count_fn; fr_env ≔ putTAtom"v5" WPtrq TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ Enteredge_labelToTAtom"L6" SomeTAtom"start" {o. ⌜∃k : Z, o = RetWIntk⌝}

iNext

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

q :

Hq :

strchr_foundp bytes 108 q

Hs :

stringp b reg bytes

∗

WPCountLogic.LG.L.ERunfr_fn ≔ count_fn; fr_env ≔ putTAtom"v5" WPtrq TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ Enteredge_labelToTAtom"L6" SomeTAtom"start" {o. ⌜∃k : Z, o = RetWIntk⌝}

iApply wp_enter ; exact find_c_L6 | reflexivity |

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

q :

Hq :

strchr_foundp bytes 108 q

Hs :

stringp b reg bytes

∗

▷WPCountLogic.LG.L.ERunfr_fn ≔ count_fn; fr_env ≔ putTAtom"pr.1" WInt0 mod 2 ^ 32 putTAtom"pr.2" WPtrq putTAtom"v5" WPtrq TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ Execedge_labelToTAtom"L6" b_instsc_L6 b_jumpc_L6 {o. ⌜∃k : Z, o = RetWIntk⌝}

iNext

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

q :

Hq :

strchr_foundp bytes 108 q

Hs :

stringp b reg bytes

∗

WPCountLogic.LG.L.ERunfr_fn ≔ count_fn; fr_env ≔ putTAtom"pr.1" WInt0 mod 2 ^ 32 putTAtom"pr.2" WPtrq putTAtom"v5" WPtrq TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ Execedge_labelToTAtom"L6" b_instsc_L6 b_jumpc_L6 {o. ⌜∃k : Z, o = RetWIntk⌝}

iApply count_loopp b reg bytes with [%] Hs

3 open

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

q :

Hq :

strchr_foundp bytes 108 q

⊢

lookupTAtom"pr.2" putTAtom"pr.1" WInt0 mod 2 ^ 32 putTAtom"pr.2" WPtrq putTAtom"v5" WPtrq TAtom"v0", WPtrp = SomeWPtr?x ∧ lookupTAtom"pr.1" putTAtom"pr.1" WInt0 mod 2 ^ 32 putTAtom"pr.2" WPtrq putTAtom"v5" WPtrq TAtom"v0", WPtrp = SomeWInt?x₀ ∧ found_fromp bytes ?x

shelved goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

q :

Hq :

strchr_foundp bytes 108 q

⊢

shelved goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

q :

Hq :

strchr_foundp bytes 108 q

⊢

split ; reflexivity |

2 open

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

q :

Hq :

strchr_foundp bytes 108 q

⊢

lookupTAtom"pr.1" putTAtom"pr.1" WInt0 mod 2 ^ 32 putTAtom"pr.2" WPtrq putTAtom"v5" WPtrq TAtom"v0", WPtrp = SomeWInt?x ∧ found_fromp bytes q

shelved goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

q :

Hq :

strchr_foundp bytes 108 q

⊢

split ; reflexivity |

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

b :

reg :

bytes :

listZ

q :

Hq :

strchr_foundp bytes 108 q

⊢

found_fromp bytes q

exact found_firstp bytes 108 q Hq

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

iIntros Hs

iApply wp_enter ; exact find_c_start | reflexivity |

iNext

cbn [ b_insts b_jump c_start ]

iApply wp_call_bind ; reflexivity | exact find_next_l | reflexivity |

iNext

iApply next_l_spec with Hs

iNext

iIntros q Hq Hs

iExists _

iSplit ; iPureIntro ; reflexivity |

iNext

cbn [ fr_fn fr_env fr_locals fr_doomed fr_at ]

iApply wp_goto

iNext

iApply wp_enter ; exact find_c_L6 | reflexivity |

iNext

iApply count_loopp b reg bytes with [%] Hs

split ; reflexivity |

exact found_firstp bytes 108 q Hq

count_l is safe: from a ready runtime, live objects apart, and a string at p, with any fuel, no labelled run stops with a failure_ending, and a run that returns returns an int. By heap_labelled_safe from count_spec, the ghost heap starting with the string's pieces.

263Theorem count_logic_safe

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

R.readys m

string_okp b reg bytes

all_agreem string_psp b reg bytes

labelled_safecount_registry count_ge entrycount_fn p m s tt fuel λo ⇒ ∃k, o = RetWIntk

Explore proof 12 tactics

Initial goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

⊢

R.readys m → live_disjointm → string_okp b reg bytes → all_agreem string_psp b reg bytes → labelled_safecount_registry count_ge entrycount_fn p m s () fuel λo : outcome ⇒ ∃k : Z, o = RetWIntk

intros Hr Hd Hok Ha

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

labelled_safecount_registry count_ge entrycount_fn p m s () fuel λo : outcome ⇒ ∃k : Z, o = RetWIntk

apply heap_labelled_safeΣ count_registry no_world count_ge entrycount_fn p m s tt list_to_mapstring_psp b reg bytes

5 open

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

R.readys m

focused goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

focused goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

agreesm list_to_mapstring_psp b reg bytes

focused goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

no_worldm () list_to_mapstring_psp b reg bytes

focused goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

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

⊢

let H ≔ nanofil_irisGScount_registry no_world count_ge in

WPCountLogic.LG.L.ERunentrycount_fn p {o. ⌜∃k : Z, o = RetWIntk⌝}

–exact Hr

4 open

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

agreesm list_to_mapstring_psp b reg bytes

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

no_worldm () list_to_mapstring_psp b reg bytes

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

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

⊢

let H ≔ nanofil_irisGScount_registry no_world count_ge in

WPCountLogic.LG.L.ERunentrycount_fn p {o. ⌜∃k : Z, o = RetWIntk⌝}

–exact Hd

3 open

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

agreesm list_to_mapstring_psp b reg bytes

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

no_worldm () list_to_mapstring_psp b reg bytes

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

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

⊢

let H ≔ nanofil_irisGScount_registry no_world count_ge in

WPCountLogic.LG.L.ERunentrycount_fn p {o. ⌜∃k : Z, o = RetWIntk⌝}

–intros l v Hl

3 open

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

l :

piece

v :

pval

Hl :

list_to_mapstring_psp b reg bytes !! l = Somev

⊢

agree_piecem l v

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

no_worldm () list_to_mapstring_psp b reg bytes

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

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

⊢

let H ≔ nanofil_irisGScount_registry no_world count_ge in

WPCountLogic.LG.L.ERunentrycount_fn p {o. ⌜∃k : Z, o = RetWIntk⌝}

exact all_agree_elem_ _ _ _ Ha elem_of_list_to_map_2_ _ _ Hl

2 open

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

no_worldm () list_to_mapstring_psp b reg bytes

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

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

⊢

let H ≔ nanofil_irisGScount_registry no_world count_ge in

WPCountLogic.LG.L.ERunentrycount_fn p {o. ⌜∃k : Z, o = RetWIntk⌝}

–exact I

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

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

⊢

let H ≔ nanofil_irisGScount_registry no_world count_ge in

WPCountLogic.LG.L.ERunentrycount_fn p {o. ⌜∃k : Z, o = RetWIntk⌝}

–intros HinvG HheapG

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

⊢

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

⊢

let H ≔ nanofil_irisGScount_registry no_world count_ge in

WPCountLogic.LG.L.ERunentrycount_fn p {o. ⌜∃k : Z, o = RetWIntk⌝}

rewrite big_sepM_list_to_map ; | exact string_ps_nodupp b reg bytes

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

⊢

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

⊢

let H ≔ nanofil_irisGScount_registry no_world count_ge in

WPCountLogic.LG.L.ERunentrycount_fn p {o. ⌜∃k : Z, o = RetWIntk⌝}

iIntros Hs

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

Hs :

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

∗

WPCountLogic.LG.L.ERunentrycount_fn p {o. ⌜∃k : Z, o = RetWIntk⌝}

iApply count_specp b reg bytes with [$Hs]

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

p :

b :

reg :

bytes :

listZ

Hr :

R.readys m

Hd :

Hok :

string_okp b reg bytes

Ha :

all_agreem string_psp b reg bytes

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 Hok Ha

apply heap_labelled_safeΣ count_registry no_world count_ge entrycount_fn p m s tt 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

–exact I

–intros HinvG HheapG

rewrite big_sepM_list_to_map ; | exact string_ps_nodupp b reg bytes

iIntros Hs

iApply count_specp b reg bytes with [$Hs]

done

The interpreter's runtime

count.c over the interpreter's runtime.

285Module InterpCountLogic ≔ CountLogic InterpRuntime

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

289Theorem interp_count_logic_safe

∀ fuel

InterpCountLogic.L.labelled_safecount_registry InterpCountLogic.count_ge entrycount_fn hi_literal HiChecks.memory InterpRuntime.start tt fuel λo ⇒ ∃k, o = RetWIntk

Explore proof 9 tactics

Initial goal

⊢

∀fuel : Z, InterpCountLogic.L.labelled_safecount_registry InterpCountLogic.count_ge entrycount_fn hi_literal HiChecks.memory InterpRuntime.start () fuel λo : outcome ⇒ ∃k : Z, o = RetWIntk

intros fuel

fuel :

⊢

InterpCountLogic.L.labelled_safecount_registry InterpCountLogic.count_ge entrycount_fn hi_literal HiChecks.memory InterpRuntime.start () fuel λo : outcome ⇒ ∃k : Z, o = RetWIntk

destruct HiChecks.entry_pre as _ & _ & Hv

fuel :

Hv :

⊢

InterpCountLogic.L.labelled_safecount_registry InterpCountLogic.count_ge entrycount_fn hi_literal HiChecks.memory InterpRuntime.start () fuel λo : outcome ⇒ ∃k : Z, o = RetWIntk

apply InterpCountLogic.count_logic_safehiΣ _ _ _ _ 65552 lit_reg hello_bytes

4 open

fuel :

Hv :

InterpRuntime.readyInterpRuntime.start HiChecks.memory

⊢

focused goal

fuel :

Hv :

live_disjointHiChecks.memory

⊢

focused goal

fuel :

Hv :

⊢

string_okhi_literal 65552 lit_reg hello_bytes

focused goal

fuel :

Hv :

⊢

all_agreeHiChecks.memory string_pshi_literal 65552 lit_reg hello_bytes

–exact hi_memory_ready

3 open

deferred goal

fuel :

Hv :

live_disjointHiChecks.memory

⊢

deferred goal

fuel :

Hv :

⊢

string_okhi_literal 65552 lit_reg hello_bytes

deferred goal

fuel :

Hv :

⊢

all_agreeHiChecks.memory string_pshi_literal 65552 lit_reg hello_bytes

–exact hi_memory_disjoint

2 open

deferred goal

fuel :

Hv :

⊢

string_okhi_literal 65552 lit_reg hello_bytes

deferred goal

fuel :

Hv :

⊢

all_agreeHiChecks.memory string_pshi_literal 65552 lit_reg hello_bytes

–exact lit_ok

deferred goal

fuel :

Hv :

⊢

all_agreeHiChecks.memory string_pshi_literal 65552 lit_reg hello_bytes

–apply all_agree_intro

fuel :

Hv :

⊢

∀l : piece v : pval, l, v ∈ string_pshi_literal 65552 lit_reg hello_bytes → agree_pieceHiChecks.memory l v

intros l v Hl

fuel :

Hv :