Filnix wiki

s :

R.state

p :

xs :

listZ

⊢

heap_interpm, s −∗ lstp xs −∗ ⌜ptr_capp = CNone ∧ ptr_addrp = 0 ∨ ∃b : Z, p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b + 16 ≤ 2 ^ 48 ∧ live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live⌝

destruct xs as | x xs ; cbn [ lst ]

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

p :

⊢

heap_interpm, s −∗ ⌜p = null⌝ −∗ ⌜ptr_capp = CNone ∧ ptr_addrp = 0 ∨ ∃b : Z, p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b + 16 ≤ 2 ^ 48 ∧ live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live⌝

focused goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

p :

x :

xs :

listZ

⊢

heap_interpm, s −∗ ∃b : Z nx : ptr, ⌜p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b + 16 ≤ 2 ^ 48 ∧ b mod 16 = 0⌝ ∗ ptsnode_psb nx x ∗ lstnx xs −∗ ⌜ptr_capp = CNone ∧ ptr_addrp = 0 ∨ ∃b : Z, p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b + 16 ≤ 2 ^ 48 ∧ live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live⌝

–iIntros _ ->

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

∗

⌜ptr_capnull = CNone ∧ ptr_addrnull = 0 ∨ ∃b : Z, null = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b + 16 ≤ 2 ^ 48 ∧ live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live⌝

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

p :

x :

xs :

listZ

⊢

iPureIntro

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

⊢

ptr_capnull = CNone ∧ ptr_addrnull = 0 ∨ ∃b : Z, null = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b + 16 ≤ 2 ^ 48 ∧ live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

p :

x :

xs :

listZ

⊢

left

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

⊢

ptr_capnull = CNone ∧ ptr_addrnull = 0

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

p :

x :

xs :

listZ

⊢

split ; reflexivity

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

p :

x :

xs :

listZ

⊢

–iIntros Hσ Hl

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

p :

x :

xs :

listZ

Hσ :

heap_interpm, s

Hl :

∃b : Z nx : ptr, ⌜p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b + 16 ≤ 2 ^ 48 ∧ b mod 16 = 0⌝ ∗ ptsnode_psb nx x ∗ lstnx xs

∗

⌜ptr_capp = CNone ∧ ptr_addrp = 0 ∨ ∃b : Z, p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b + 16 ≤ 2 ^ 48 ∧ live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live⌝

iDestruct Hl as b nx → & Hb₀ & Hb₁ & _ [Hn _]

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

x :

xs :

listZ

b :

nx :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hσ :

heap_interpm, s

Hn :

ptsnode_psb nx x

∗

⌜ptr_capptr_addr ≔ b; ptr_cap ≔ Objb = CNone ∧ ptr_addrptr_addr ≔ b; ptr_cap ≔ Objb = 0 ∨ ∃b₀ : Z, ptr_addr ≔ b; ptr_cap ≔ Objb = ptr_addr ≔ b₀; ptr_cap ≔ Objb₀ ∧ 0 < b₀ ∧ b₀ + 16 ≤ 2 ^ 48 ∧ live_atm b₀ r_base ≔ b₀; r_end ≔ b₀ + 16; r_kind ≔ Heap; r_life ≔ Live⌝

iDestruct pts_facts with Hσ Hn as %Hf & _

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

x :

xs :

listZ

b :

nx :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hf :

all_agreem node_psb nx x

Hσ :

heap_interpm, s

Hn :

ptsnode_psb nx x

∗

iPureIntro

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

x :

xs :

listZ

b :

nx :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hf :

all_agreem node_psb nx x

⊢

ptr_capptr_addr ≔ b; ptr_cap ≔ Objb = CNone ∧ ptr_addrptr_addr ≔ b; ptr_cap ≔ Objb = 0 ∨ ∃b₀ : Z, ptr_addr ≔ b; ptr_cap ≔ Objb = ptr_addr ≔ b₀; ptr_cap ≔ Objb₀ ∧ 0 < b₀ ∧ b₀ + 16 ≤ 2 ^ 48 ∧ live_atm b₀ r_base ≔ b₀; r_end ≔ b₀ + 16; r_kind ≔ Heap; r_life ≔ Live

right

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

x :

xs :

listZ

b :

nx :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hf :

all_agreem node_psb nx x

⊢

∃b₀ : Z, ptr_addr ≔ b; ptr_cap ≔ Objb = ptr_addr ≔ b₀; ptr_cap ≔ Objb₀ ∧ 0 < b₀ ∧ b₀ + 16 ≤ 2 ^ 48 ∧ live_atm b₀ r_base ≔ b₀; r_end ≔ b₀ + 16; r_kind ≔ Heap; r_life ≔ Live

exists b

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

x :

xs :

listZ

b :

nx :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hf :

all_agreem node_psb nx x

⊢

ptr_addr ≔ b; ptr_cap ≔ Objb = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b + 16 ≤ 2 ^ 48 ∧ live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

split ; reflexivity |

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

x :

xs :

listZ

b :

nx :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hf :

all_agreem node_psb nx x

⊢

0 < b ∧ b + 16 ≤ 2 ^ 48 ∧ live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

split ; exact Hb₀ |

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

x :

xs :

listZ

b :

nx :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hf :

all_agreem node_psb nx x

⊢

b + 16 ≤ 2 ^ 48 ∧ live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

split ; exact Hb₁ |

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

x :

xs :

listZ

b :

nx :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hf :

all_agreem node_psb nx x

⊢

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

unfold node_ps in Hf

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

x :

xs :

listZ

b :

nx :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hf :

all_agreem PLiveb, VLiver_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live ++ PAuxb 0, VAuxptr_capnx ++ cellb 0 ptr_addrnx ++ cellb 8 x

⊢

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

apply all_agree_app in Hf as Hf _

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

x :

xs :

listZ

b :

nx :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hf :

all_agreem PLiveb, VLiver_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

⊢

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

cbn [ all_agree fst snd agree_piece ] in Hf

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

x :

xs :

listZ

b :

nx :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hf :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live ∧ True

⊢

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

exact proj1Hf

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

destruct xs as | x xs ; cbn [ lst ]

–iIntros _ ->

iPureIntro

left

split ; reflexivity

–iIntros Hσ Hl

iDestruct Hl as b nx → & Hb₀ & Hb₁ & _ [Hn _]

iDestruct pts_facts with Hσ Hn as %Hf & _

iPureIntro

right

exists b

split ; reflexivity |

split ; exact Hb₀ |

split ; exact Hb₁ |

unfold node_ps in Hf

apply all_agree_app in Hf as Hf _

cbn [ all_agree fst snd agree_piece ] in Hf

exact proj1Hf

What a node at b and the list after it tell a step: b's region, the value's and the next address's bytes, and the next pointer's capability in the aux slot, exactly, since its object is live.

257Lemma node_view

∀ m s b nx x xs

heap_interpm, s −∗ ptsnode_psb nx x −∗ lstnx xs −∗ ⌜object_regionb m_regionsm = SomemkRegionb b + 16 Heap Live ∧ ∀a : Z, a = b + 8%Z → load_bytesm a 8 = x mod 2 ^ 64%Z ∧ ∀a : Z, a = b → load_bytesm a 8 = ptr_addrnx ∧ ∀a : Z, a = b → m_auxm a = ptr_capnx⌝

Explore proof 28 tactics

Initial goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

⊢

heap_interpm, s −∗ ptsnode_psb nx x −∗ lstnx xs −∗ ⌜object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live ∧ ∀a : Z, a = b + 8%Z → load_bytesm a 8 = x mod 2 ^ 64 ∧ ∀a : Z, a = b → load_bytesm a 8 = ptr_addrnx ∧ ∀a : Z, a = b → m_auxm a = ptr_capnx⌝

iIntros Hσ Hn Hl

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hσ :

heap_interpm, s

Hn :

ptsnode_psb nx x

Hl :

lstnx xs

∗

⌜object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live ∧ ∀a : Z, a = b + 8%Z → load_bytesm a 8 = x mod 2 ^ 64 ∧ ∀a : Z, a = b → load_bytesm a 8 = ptr_addrnx ∧ ∀a : Z, a = b → m_auxm a = ptr_capnx⌝

iDestruct pts_facts with Hσ Hn as %Hf & _

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hf :

all_agreem node_psb nx x

Hσ :

heap_interpm, s

Hn :

ptsnode_psb nx x

Hl :

lstnx xs

∗

iDestruct lst_head with Hσ Hl as %Hh

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hf :

all_agreem node_psb nx x

Hh :

ptr_capnx = CNone ∧ ptr_addrnx = 0 ∨ ∃b : Z, nx = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b + 16 ≤ 2 ^ 48 ∧ live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hσ :

heap_interpm, s

Hn :

ptsnode_psb nx x

Hl :

lstnx xs

∗

iPureIntro

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hf :

all_agreem node_psb nx x

Hh :

⊢

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live ∧ ∀a : Z, a = b + 8 → load_bytesm a 8 = x mod 2 ^ 64 ∧ ∀a : Z, a = b → load_bytesm a 8 = ptr_addrnx ∧ ∀a : Z, a = b → m_auxm a = ptr_capnx

unfold node_ps in Hf

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hf :

all_agreem PLiveb, VLiver_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live ++ PAuxb 0, VAuxptr_capnx ++ cellb 0 ptr_addrnx ++ cellb 8 x

Hh :

⊢

apply all_agree_app in Hf as Hla Hf

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hla :

all_agreem PLiveb, VLiver_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hf :

all_agreem PAuxb 0, VAuxptr_capnx ++ cellb 0 ptr_addrnx ++ cellb 8 x

Hh :

⊢

apply all_agree_app in Hf as Hax Hf

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hla :

all_agreem PLiveb, VLiver_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

all_agreem PAuxb 0, VAuxptr_capnx

Hf :

all_agreem cellb 0 ptr_addrnx ++ cellb 8 x

Hh :

⊢

apply all_agree_app in Hf as Hc₀ Hc₈

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hla :

all_agreem PLiveb, VLiver_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

all_agreem PAuxb 0, VAuxptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

⊢

cbn [ all_agree fst snd agree_piece ] in Hla , Hax

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hla :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live ∧ True

Hax :

registeredm b ∧ in_livem b 0 aux_holdsm b + 0 ptr_capnx ∧ True

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

⊢

destruct Hla as Hlive _

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

registeredm b ∧ in_livem b 0 aux_holdsm b + 0 ptr_capnx ∧ True

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

⊢

destruct Hax as _ & Hax _

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

⊢

pose proof Hlive as E L

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

split ; exact E |

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

∀a : Z, a = b + 8 → load_bytesm a 8 = x mod 2 ^ 64 ∧ ∀a : Z, a = b → load_bytesm a 8 = ptr_addrnx ∧ ∀a : Z, a = b → m_auxm a = ptr_capnx

split ; | split

3 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

∀a : Z, a = b + 8 → load_bytesm a 8 = x mod 2 ^ 64

focused goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

∀a : Z, a = b → load_bytesm a 8 = ptr_addrnx

focused goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

∀a : Z, a = b → m_auxm a = ptr_capnx

–intros a →

3 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

load_bytesm b + 8 8 = x mod 2 ^ 64

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

∀a : Z, a = b → load_bytesm a 8 = ptr_addrnx

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

∀a : Z, a = b → m_auxm a = ptr_capnx

exact cell_loadm b _ 8 x b + 8 Hlive Hc₈ eq_refl

2 open

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

∀a : Z, a = b → load_bytesm a 8 = ptr_addrnx

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

∀a : Z, a = b → m_auxm a = ptr_capnx

–intros a →

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

load_bytesm b 8 = ptr_addrnx

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

∀a : Z, a = b → m_auxm a = ptr_capnx

rewrite cell_loadm b _ 0 ptr_addrnx b Hlive Hc₀ ; | lia

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

ptr_addrnx mod 2 ^ 64 = ptr_addrnx

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

∀a : Z, a = b → m_auxm a = ptr_capnx

apply Z.mod_small

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

0 ≤ ptr_addrnx < 2 ^ 64

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

∀a : Z, a = b → m_auxm a = ptr_capnx

destruct Hh as _ → | nb & → & ? & ? & _ ; cbn ; lia

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

∀a : Z, a = b → m_auxm a = ptr_capnx

–intros a →

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

⊢

m_auxm b = ptr_capnx

destruct Hax_ E L as _ & _ & Hx

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

Hx :

aux_holdsm b + 0 ptr_capnx

⊢

m_auxm b = ptr_capnx

replace b + 0 with b in Hx by lia

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

Hx :

aux_holdsm b ptr_capnx

⊢

m_auxm b = ptr_capnx

apply aux_holds_live ; exact Hx |

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b :

nx :

x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capnx

Hc₀ :

Hc₈ :

all_agreem cellb 8 x

Hh :

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

Hx :

aux_holdsm b ptr_capnx

⊢

ptr_capnx = CNone ∨ ∃b₀ : Z reg : region, ptr_capnx = Objb₀ ∧ live_atm b₀ reg

destruct Hh as → _ | nb & → & _ & _ & Hl ; left ; reflexivity |

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b, x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

nb :

Hc₀ :

all_agreem cellb 0 ptr_addrptr_addr ≔ nb; ptr_cap ≔ Objnb

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capptr_addr ≔ nb; ptr_cap ≔ Objnb

Hc₈ :

all_agreem cellb 8 x

Hl :

live_atm nb r_base ≔ nb; r_end ≔ nb + 16; r_kind ≔ Heap; r_life ≔ Live

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

Hx :

aux_holdsm b ptr_capptr_addr ≔ nb; ptr_cap ≔ Objnb

⊢

ptr_capptr_addr ≔ nb; ptr_cap ≔ Objnb = CNone ∨ ∃b₀ : Z reg : region, ptr_capptr_addr ≔ nb; ptr_cap ≔ Objnb = Objb₀ ∧ live_atm b₀ reg

right

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b, x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

nb :

Hc₀ :

all_agreem cellb 0 ptr_addrptr_addr ≔ nb; ptr_cap ≔ Objnb

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capptr_addr ≔ nb; ptr_cap ≔ Objnb

Hc₈ :

all_agreem cellb 8 x

Hl :

live_atm nb r_base ≔ nb; r_end ≔ nb + 16; r_kind ≔ Heap; r_life ≔ Live

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

Hx :

aux_holdsm b ptr_capptr_addr ≔ nb; ptr_cap ≔ Objnb

⊢

∃b₀ : Z reg : region, ptr_capptr_addr ≔ nb; ptr_cap ≔ Objnb = Objb₀ ∧ live_atm b₀ reg

exists nb, mkRegionnb nb + 16 Heap Live

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

m :

s :

R.state

b, x :

xs :

listZ

Hlive :

live_atm b r_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

nb :

Hc₀ :

all_agreem cellb 0 ptr_addrptr_addr ≔ nb; ptr_cap ≔ Objnb

Hax :

in_livem b 0 aux_holdsm b + 0 ptr_capptr_addr ≔ nb; ptr_cap ≔ Objnb

Hc₈ :

all_agreem cellb 8 x

Hl :

live_atm nb r_base ≔ nb; r_end ≔ nb + 16; r_kind ≔ Heap; r_life ≔ Live

E :

object_regionb m_regionsm = Somer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live

L :

r_lifer_base ≔ b; r_end ≔ b + 16; r_kind ≔ Heap; r_life ≔ Live = Live

Hx :

aux_holdsm b ptr_capptr_addr ≔ nb; ptr_cap ≔ Objnb

⊢

ptr_capptr_addr ≔ nb; ptr_cap ≔ Objnb = Objnb ∧ live_atm nb r_base ≔ nb; r_end ≔ nb + 16; r_kind ≔ Heap; r_life ≔ Live

split ; reflexivity | exact Hl

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

iIntros Hσ Hn Hl

iDestruct pts_facts with Hσ Hn as %Hf & _

iDestruct lst_head with Hσ Hl as %Hh

iPureIntro

unfold node_ps in Hf

apply all_agree_app in Hf as Hla Hf

apply all_agree_app in Hf as Hax Hf

apply all_agree_app in Hf as Hc₀ Hc₈

cbn [ all_agree fst snd agree_piece ] in Hla , Hax

destruct Hla as Hlive _

destruct Hax as _ & Hax _

pose proof Hlive as E L

split ; exact E |

split ; | split

–intros a →

exact cell_loadm b _ 8 x b + 8 Hlive Hc₈ eq_refl

–intros a →

rewrite cell_loadm b _ 0 ptr_addrnx b Hlive Hc₀ ; | lia

apply Z.mod_small

destruct Hh as _ → | nb & → & ? & ? & _ ; cbn ; lia

–intros a →

destruct Hax_ E L as _ & _ & Hx

replace b + 0 with b in Hx by lia

apply aux_holds_live ; exact Hx |

destruct Hh as → _ | nb & → & _ & _ & Hl ; left ; reflexivity |

right

exists nb, mkRegionnb nb + 16 Heap Live

split ; reflexivity | exact Hl

A step of sum's loop body that may read the node at b.

280Ltac wp_node b nx x xs ≔

iApply wpc_next_ ptsnode_psb nx x ∗ lstnx xs%I with [$Hn $Hl] ; let m ≔ fresh "m" in let s ≔ fresh "s" in iIntros m s Hσ [Hn Hl] ; iDestruct node_view with Hσ Hn Hl as %? & ? & ? & ? ; iPureIntro ; compute_eq | iNext ; iIntros [Hn Hl] ; gen_env

The continuation of a call of sum from the caller frame cf, whose result is bound to d: cf resumed with any result and any fuel.

289Notation cont cf d callers ≔ ∀y fuel′, wpclge EConfmkFramefr_fncf putd WInty fr_envcf fr_localscf fr_doomedcf fr_atcf callers fuel′%I

sum's loop, from the point after its head's phis: with pr.1 the list's pointer p and pr.2 an integer, owning the list and the continuation, the run is safe. By Löb induction.

296Lemma sum_loop

∀ cf d callers

⊢ ∀e p xs fuel, ⌜lookupTAtom"pr.1" e = SomeWPtrp⌝ −∗ ⌜∃s, lookupTAtom"pr.2" e = SomeWInts⌝ −∗ lstp xs −∗ contcf d callers −∗ wpclge EConfmkFramels_fn"sum" e [ ] None ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, mkPendingCResultd L None :: callers fuel

Explore proof 26 tactics

Initial goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

⊢

⊢ ∀e : listname × word p : ptr xs : listZ fuel : Z, ⌜lookupTAtom"pr.1" e = SomeWPtrp⌝ −∗ ⌜∃s : Z, lookupTAtom"pr.2" e = SomeWInts⌝ −∗ lstp xs −∗ contcf d callers −∗ wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

iLöb as IH

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

IH :

▷∀e : listname × word p : ptr xs : listZ fuel : Z, ⌜lookupTAtom"pr.1" e = SomeWPtrp⌝ −∗ ⌜∃s : Z, lookupTAtom"pr.2" e = SomeWInts⌝ −∗ lstp xs −∗ contcf d callers −∗ wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

□

∀e : listname × word p : ptr xs : listZ fuel : Z, ⌜lookupTAtom"pr.1" e = SomeWPtrp⌝ −∗ ⌜∃s : Z, lookupTAtom"pr.2" e = SomeWInts⌝ −∗ lstp xs −∗ contcf d callers −∗ wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

iIntros e p xs fuel Hp s₀ Hs Hl HK

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

e :

listname × word

p :

xs :

listZ

fuel :

Hp :

lookupTAtom"pr.1" e = SomeWPtrp

s₀ :

Hs :

lookupTAtom"pr.2" e = SomeWInts₀

IH :

▷∀e₀ : listname × word p₀ : ptr xs₀ : listZ fuel₀ : Z, ⌜lookupTAtom"pr.1" e₀ = SomeWPtrp₀⌝ −∗ ⌜∃s : Z, lookupTAtom"pr.2" e₀ = SomeWInts⌝ −∗ lstp₀ xs₀ −∗ contcf d callers −∗ wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel₀

□

Hl :

lstp xs

HK :

contcf d callers

∗

wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

destruct xs as | x xs

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

e :

listname × word

p :

fuel :

Hp :

lookupTAtom"pr.1" e = SomeWPtrp

s₀ :

Hs :

lookupTAtom"pr.2" e = SomeWInts₀

IH :

▷∀e₀ : listname × word p₀ : ptr xs : listZ fuel₀ : Z, ⌜lookupTAtom"pr.1" e₀ = SomeWPtrp₀⌝ −∗ ⌜∃s : Z, lookupTAtom"pr.2" e₀ = SomeWInts⌝ −∗ lstp₀ xs −∗ contcf d callers −∗ wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel₀

□

Hl :

lstp [ ]

HK :

contcf d callers

∗

wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

focused goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

e :

listname × word

p :

x :

xs :

listZ

fuel :

Hp :

lookupTAtom"pr.1" e = SomeWPtrp

s₀ :

Hs :

lookupTAtom"pr.2" e = SomeWInts₀

IH :

□

Hl :

lstp x :: xs

HK :

contcf d callers

∗

wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

–iDestruct Hl as %→

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

e :

listname × word

fuel :

Hp :

lookupTAtom"pr.1" e = SomeWPtrnull

s₀ :

Hs :

lookupTAtom"pr.2" e = SomeWInts₀

IH :

▷∀e₀ : listname × word p : ptr xs : listZ fuel₀ : Z, ⌜lookupTAtom"pr.1" e₀ = SomeWPtrp⌝ −∗ ⌜∃s : Z, lookupTAtom"pr.2" e₀ = SomeWInts⌝ −∗ lstp xs −∗ contcf d callers −∗ wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel₀

□

HK :

contcf d callers

∗

wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

e :

listname × word

p :

x :

xs :

listZ

fuel :

Hp :

lookupTAtom"pr.1" e = SomeWPtrp

s₀ :

Hs :

lookupTAtom"pr.2" e = SomeWInts₀

IH :

□

Hl :

lstp x :: xs

HK :

contcf d callers

∗

wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

wp_emp

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

fuel, s₀ :

e₀ :

listname × word

Hput :

lookupTAtom"v7" e₀ = SomeWInt0

H :

lookupTAtom"pr.2" e₀ = SomeWInts₀

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrnull

IH :

∀e : listname × word p : ptr xs : listZ fuel₀ : Z, ⌜lookupTAtom"pr.1" e = SomeWPtrp⌝ −∗ ⌜∃s : Z, lookupTAtom"pr.2" e = SomeWInts⌝ −∗ lstp xs −∗ contcf d callers −∗ wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel₀

□

HK :

contcf d callers

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" LetTAtom"v8" W CmpNe L TmpTAtom"v7"; Const0 JBranchTmpTAtom"v8" ToTAtom"L4" ToTAtom"L5" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

e :

listname × word

p :

x :

xs :

listZ

fuel :

Hp :

lookupTAtom"pr.1" e = SomeWPtrp

s₀ :

Hs :

lookupTAtom"pr.2" e = SomeWInts₀

IH :

□

Hl :

lstp x :: xs

HK :

contcf d callers

∗

wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

wp_emp

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

fuel, s₀ :

e :

listname × word

Hput₀ :

lookupTAtom"v8" e = SomeWInt0

H₁ :

lookupTAtom"pr.1" e = SomeWPtrnull

H₀ :

lookupTAtom"pr.2" e = SomeWInts₀

H :

lookupTAtom"v7" e = SomeWInt0

IH :

∀e₀ : listname × word p : ptr xs : listZ fuel₀ : Z, ⌜lookupTAtom"pr.1" e₀ = SomeWPtrp⌝ −∗ ⌜∃s : Z, lookupTAtom"pr.2" e₀ = SomeWInts⌝ −∗ lstp xs −∗ contcf d callers −∗ wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel₀

□

HK :

contcf d callers

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" [ ] JBranchTmpTAtom"v8" ToTAtom"L4" ToTAtom"L5" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

e :

listname × word

p :

x :

xs :

listZ

fuel :

Hp :

lookupTAtom"pr.1" e = SomeWPtrp

s₀ :

Hs :

lookupTAtom"pr.2" e = SomeWInts₀

IH :

□

Hl :

lstp x :: xs

HK :

contcf d callers

∗

wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

wp_emp

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

fuel, s₀ :

e :

listname × word

Hput₀ :

lookupTAtom"v8" e = SomeWInt0

H₁ :

lookupTAtom"pr.1" e = SomeWPtrnull

H₀ :

lookupTAtom"pr.2" e = SomeWInts₀

H :

lookupTAtom"v7" e = SomeWInt0

IH :

□

HK :

contcf d callers

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"L5" SomeTAtom"L3" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

e :

listname × word

p :

x :

xs :

listZ

fuel :

Hp :

lookupTAtom"pr.1" e = SomeWPtrp

s₀ :

Hs :

lookupTAtom"pr.2" e = SomeWInts₀

IH :

□

Hl :

lstp x :: xs

HK :

contcf d callers

∗

wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

wp_fuel

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

fuel, s₀ :

e :

listname × word

Hput₀ :

lookupTAtom"v8" e = SomeWInt0

H₁ :

lookupTAtom"pr.1" e = SomeWPtrnull

H₀ :

lookupTAtom"pr.2" e = SomeWInts₀

H :

lookupTAtom"v7" e = SomeWInt0

Hz :

fuel ≠ 0

IH :

□

HK :

contcf d callers

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"L5" SomeTAtom"L3" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

e :

listname × word

p :

x :

xs :

listZ

fuel :

Hp :

lookupTAtom"pr.1" e = SomeWPtrp

s₀ :

Hs :

lookupTAtom"pr.2" e = SomeWInts₀

IH :

□

Hl :

lstp x :: xs

HK :

contcf d callers

∗

wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

wp_emp

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

fuel, s₀ :

e :

listname × word

Hput₀ :

lookupTAtom"v8" e = SomeWInt0

H₁ :

lookupTAtom"pr.1" e = SomeWPtrnull

H₀ :

lookupTAtom"pr.2" e = SomeWInts₀

H :

lookupTAtom"v7" e = SomeWInt0

Hz :

fuel ≠ 0

IH :

□

HK :

contcf d callers

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L5" [ ] JRetTmpTAtom"pr.2" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel − 1

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

e :

listname × word

p :

x :

xs :

listZ

fuel :

Hp :

lookupTAtom"pr.1" e = SomeWPtrp

s₀ :

Hs :

lookupTAtom"pr.2" e = SomeWInts₀

IH :

□

Hl :

lstp x :: xs

HK :

contcf d callers

∗

wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

iApply wpc_next_ emp%I with [//] ; let m ≔ fresh "m" in let s ≔ fresh "s" in iIntros m s _ _ ; iPureIntro ; compute_eq | iNext ; iIntros _ ; iApply HK

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

e :

listname × word

p :

x :

xs :

listZ

fuel :

Hp :

lookupTAtom"pr.1" e = SomeWPtrp

s₀ :

Hs :

lookupTAtom"pr.2" e = SomeWInts₀

IH :

□

Hl :

lstp x :: xs

HK :

contcf d callers

∗

wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

–iDestruct Hl as b na nc → & Hb₀ & Hb₁ & Hb₂ [Hn Hl]

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

e :

listname × word

x :

xs :

listZ

fuel, b :

Hp :

lookupTAtom"pr.1" e = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

s₀ :

Hs :

lookupTAtom"pr.2" e = SomeWInts₀

na :

nc :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hb₂ :

b mod 16 = 0

IH :

▷∀e₀ : listname × word p : ptr xs₀ : listZ fuel₀ : Z, ⌜lookupTAtom"pr.1" e₀ = SomeWPtrp⌝ −∗ ⌜∃s : Z, lookupTAtom"pr.2" e₀ = SomeWInts⌝ −∗ lstp xs₀ −∗ contcf d callers −∗ wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel₀

□

Hn :

ptsnode_psb ptr_addr ≔ na; ptr_cap ≔ nc x

Hl :

fix lst p : ptr xs₀ : listZ {struct xs0} : iPropΣ ≔

match xs₀ with

[ ]

⇒

⌜p = null⌝

x₀ :: xs′

⇒

∃b₀ : Z nx : ptr, ⌜p = ptr_addr ≔ b₀; ptr_cap ≔ Objb₀ ∧ 0 < b₀ ∧ b₀ + 16 ≤ 2 ^ 48 ∧ b₀ mod 16 = 0⌝ ∗ ptsnode_psb₀ nx x₀ ∗ lstnx xs′

ptr_addr ≔ na; ptr_cap ≔ nc xs

HK :

contcf d callers

∗

wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

wp_node b mkPtrna nc x xs

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

x :

xs :

listZ

fuel, b, s₀, na :

nc :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hb₂ :

b mod 16 = 0

e₀ :

listname × word

Hput :

lookupTAtom"v7" e₀ = SomeWIntb

H :

lookupTAtom"pr.2" e₀ = SomeWInts₀

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

IH :

∀e : listname × word p : ptr xs₀ : listZ fuel₀ : Z, ⌜lookupTAtom"pr.1" e = SomeWPtrp⌝ −∗ ⌜∃s : Z, lookupTAtom"pr.2" e = SomeWInts⌝ −∗ lstp xs₀ −∗ contcf d callers −∗ wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel₀

□

HK :

contcf d callers

Hn :

ptsnode_psb ptr_addr ≔ na; ptr_cap ≔ nc x

Hl :

lstptr_addr ≔ na; ptr_cap ≔ nc xs

∗

wp_node b mkPtrna nc x xs

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

x :

xs :

listZ

fuel, b, s₀, na :

nc :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hb₂ :

b mod 16 = 0

e :

listname × word

Hput₀ :

lookupTAtom"v8" e = SomeWInt1

H₁ :

lookupTAtom"pr.1" e = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

H₀ :

lookupTAtom"pr.2" e = SomeWInts₀

H :

lookupTAtom"v7" e = SomeWIntb

IH :

∀e₀ : listname × word p : ptr xs₀ : listZ fuel₀ : Z, ⌜lookupTAtom"pr.1" e₀ = SomeWPtrp⌝ −∗ ⌜∃s : Z, lookupTAtom"pr.2" e₀ = SomeWInts⌝ −∗ lstp xs₀ −∗ contcf d callers −∗ wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" b_instssum_L3 b_jumpsum_L3 cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel₀

□

HK :

contcf d callers

Hn :

ptsnode_psb ptr_addr ≔ na; ptr_cap ≔ nc x

Hl :

lstptr_addr ≔ na; ptr_cap ≔ nc xs

∗

wp_node b mkPtrna nc x xs

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

x :

xs :

listZ

fuel, b, s₀, na :

nc :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hb₂ :

b mod 16 = 0

e :

listname × word

Hput₀ :

lookupTAtom"v8" e = SomeWInt1

H₁ :

lookupTAtom"pr.1" e = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

H₀ :

lookupTAtom"pr.2" e = SomeWInts₀

H :

lookupTAtom"v7" e = SomeWIntb

IH :

□

HK :

contcf d callers

Hn :

ptsnode_psb ptr_addr ≔ na; ptr_cap ≔ nc x

Hl :

lstptr_addr ≔ na; ptr_cap ≔ nc xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"L4" SomeTAtom"L3" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

wp_fuel

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

x :

xs :

listZ

fuel, b, s₀, na :

nc :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hb₂ :

b mod 16 = 0

e :

listname × word

Hput₀ :

lookupTAtom"v8" e = SomeWInt1

H₁ :

lookupTAtom"pr.1" e = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

H₀ :

lookupTAtom"pr.2" e = SomeWInts₀

H :

lookupTAtom"v7" e = SomeWIntb

Hz :

fuel ≠ 0

IH :

□

HK :

contcf d callers

Hn :

ptsnode_psb ptr_addr ≔ na; ptr_cap ≔ nc x

Hl :

lstptr_addr ≔ na; ptr_cap ≔ nc xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"L4" SomeTAtom"L3" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

wp_node b mkPtrna nc x xs

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

x :

xs :

listZ

fuel, b, s₀, na :

nc :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hb₂ :

b mod 16 = 0

e :

listname × word

Hput₀ :

lookupTAtom"v8" e = SomeWInt1

H₁ :

lookupTAtom"pr.1" e = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

H₀ :

lookupTAtom"pr.2" e = SomeWInts₀

H :

lookupTAtom"v7" e = SomeWIntb

Hz :

fuel ≠ 0

IH :

□

HK :

contcf d callers

Hn :

ptsnode_psb ptr_addr ≔ na; ptr_cap ≔ nc x

Hl :

lstptr_addr ≔ na; ptr_cap ≔ nc xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" FlightTAtom"v11" Add FAddressTmpTAtom"pr.1"; FValueConst8 LowerOfTmpTAtom"pr.1"; LetTAtom"chk0" A Check0 8 Read 1 TmpTAtom"v11"; LetTAtom"v12" L RawLoadLdL 0 TmpTAtom"chk0"; LetTAtom"v13" L Add TmpTAtom"pr.2"; TmpTAtom"v12"; LetTAtom"chk1" A HalfCheckLower 0 8 Read 8 TmpTAtom"chk0"; TmpTAtom"pr.1"; LetTAtom"v15" P RawLoadPointer0 AuxRead; LowerResolve; AddressRead TmpTAtom"chk1" JGotoPollTAtom"L3" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel − 1

wp_node b mkPtrna nc x xs

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

x :

xs :

listZ

fuel, b, s₀, na :

nc :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hb₂ :

b mod 16 = 0

Hz :

fuel ≠ 0

e₀ :

listname × word

Hput :

lookupTAtom"v11" e₀ = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

H₂ :

lookupTAtom"v7" e₀ = SomeWIntb

H :

lookupTAtom"pr.2" e₀ = SomeWInts₀

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

H₁ :

lookupTAtom"v8" e₀ = SomeWInt1

IH :

□

HK :

contcf d callers

Hn :

ptsnode_psb ptr_addr ≔ na; ptr_cap ≔ nc x

Hl :

lstptr_addr ≔ na; ptr_cap ≔ nc xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" LetTAtom"chk0" A Check0 8 Read 1 TmpTAtom"v11"; LetTAtom"v12" L RawLoadLdL 0 TmpTAtom"chk0"; LetTAtom"v13" L Add TmpTAtom"pr.2"; TmpTAtom"v12"; LetTAtom"chk1" A HalfCheckLower 0 8 Read 8 TmpTAtom"chk0"; TmpTAtom"pr.1"; LetTAtom"v15" P RawLoadPointer0 AuxRead; LowerResolve; AddressRead TmpTAtom"chk1" JGotoPollTAtom"L3" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel − 1

wp_node b mkPtrna nc x xs

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

x :

xs :

listZ

fuel, b, s₀, na :

nc :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hb₂ :

b mod 16 = 0

Hz :

fuel ≠ 0

e :

listname × word

Hput₀ :

lookupTAtom"chk0" e = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

H₃ :

lookupTAtom"v8" e = SomeWInt1

H₁ :

lookupTAtom"pr.1" e = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

H₀ :

lookupTAtom"pr.2" e = SomeWInts₀

H :

lookupTAtom"v7" e = SomeWIntb

H₂ :

lookupTAtom"v11" e = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

IH :

□

HK :

contcf d callers

Hn :

ptsnode_psb ptr_addr ≔ na; ptr_cap ≔ nc x

Hl :

lstptr_addr ≔ na; ptr_cap ≔ nc xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" LetTAtom"v12" L RawLoadLdL 0 TmpTAtom"chk0"; LetTAtom"v13" L Add TmpTAtom"pr.2"; TmpTAtom"v12"; LetTAtom"chk1" A HalfCheckLower 0 8 Read 8 TmpTAtom"chk0"; TmpTAtom"pr.1"; LetTAtom"v15" P RawLoadPointer0 AuxRead; LowerResolve; AddressRead TmpTAtom"chk1" JGotoPollTAtom"L3" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel − 1

wp_node b mkPtrna nc x xs

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

x :

xs :

listZ

fuel, b, s₀, na :

nc :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hb₂ :

b mod 16 = 0

Hz :

fuel ≠ 0

e₀ :

listname × word

Hput :

lookupTAtom"v12" e₀ = SomeWIntx mod 2 ^ 64

H₄ :

lookupTAtom"v11" e₀ = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

H₂ :

lookupTAtom"v7" e₀ = SomeWIntb

H :

lookupTAtom"pr.2" e₀ = SomeWInts₀

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

H₁ :

lookupTAtom"v8" e₀ = SomeWInt1

H₃ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

IH :

□

HK :

contcf d callers

Hn :

ptsnode_psb ptr_addr ≔ na; ptr_cap ≔ nc x

Hl :

lstptr_addr ≔ na; ptr_cap ≔ nc xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" LetTAtom"v13" L Add TmpTAtom"pr.2"; TmpTAtom"v12"; LetTAtom"chk1" A HalfCheckLower 0 8 Read 8 TmpTAtom"chk0"; TmpTAtom"pr.1"; LetTAtom"v15" P RawLoadPointer0 AuxRead; LowerResolve; AddressRead TmpTAtom"chk1" JGotoPollTAtom"L3" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel − 1

wp_node b mkPtrna nc x xs

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

x :

xs :

listZ

fuel, b, s₀, na :

nc :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hb₂ :

b mod 16 = 0

Hz :

fuel ≠ 0

e :

listname × word

Hput₀ :

lookupTAtom"v13" e = SomeWInts₀ mod 2 ^ 64 + x mod 2 ^ 64 mod 2 ^ 64 mod 2 ^ 64

H₅ :

lookupTAtom"chk0" e = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

H₃ :

lookupTAtom"v8" e = SomeWInt1

H₁ :

lookupTAtom"pr.1" e = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

H₀ :

lookupTAtom"pr.2" e = SomeWInts₀

H :

lookupTAtom"v7" e = SomeWIntb

H₂ :

lookupTAtom"v11" e = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

H₄ :

lookupTAtom"v12" e = SomeWIntx mod 2 ^ 64

IH :

□

HK :

contcf d callers

Hn :

ptsnode_psb ptr_addr ≔ na; ptr_cap ≔ nc x

Hl :

lstptr_addr ≔ na; ptr_cap ≔ nc xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" LetTAtom"chk1" A HalfCheckLower 0 8 Read 8 TmpTAtom"chk0"; TmpTAtom"pr.1"; LetTAtom"v15" P RawLoadPointer0 AuxRead; LowerResolve; AddressRead TmpTAtom"chk1" JGotoPollTAtom"L3" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel − 1

wp_node b mkPtrna nc x xs

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

x :

xs :

listZ

fuel, b, s₀, na :

nc :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hb₂ :

b mod 16 = 0

Hz :

fuel ≠ 0

e₀ :

listname × word

Hput :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

H₆ :

lookupTAtom"v12" e₀ = SomeWIntx mod 2 ^ 64

H₄ :

lookupTAtom"v11" e₀ = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

H₂ :

lookupTAtom"v7" e₀ = SomeWIntb

H :

lookupTAtom"pr.2" e₀ = SomeWInts₀

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

H₁ :

lookupTAtom"v8" e₀ = SomeWInt1

H₃ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

H₅ :

lookupTAtom"v13" e₀ = SomeWInts₀ mod 2 ^ 64 + x mod 2 ^ 64 mod 2 ^ 64 mod 2 ^ 64

IH :

□

HK :

contcf d callers

Hn :

ptsnode_psb ptr_addr ≔ na; ptr_cap ≔ nc x

Hl :

lstptr_addr ≔ na; ptr_cap ≔ nc xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" LetTAtom"v15" P RawLoadPointer0 AuxRead; LowerResolve; AddressRead TmpTAtom"chk1" JGotoPollTAtom"L3" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel − 1

wp_node b mkPtrna nc x xs

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

x :

xs :

listZ

fuel, b, s₀, na :

nc :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hb₂ :

b mod 16 = 0

Hz :

fuel ≠ 0

e :

listname × word

Hput₀ :

lookupTAtom"v15" e = SomeWPtrptr_addr ≔ na; ptr_cap ≔ nc

H₇ :

lookupTAtom"v13" e = SomeWInts₀ mod 2 ^ 64 + x mod 2 ^ 64 mod 2 ^ 64 mod 2 ^ 64

H₅ :

lookupTAtom"chk0" e = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

H₃ :

lookupTAtom"v8" e = SomeWInt1

H₁ :

lookupTAtom"pr.1" e = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

H₀ :

lookupTAtom"pr.2" e = SomeWInts₀

H :

lookupTAtom"v7" e = SomeWIntb

H₂ :

lookupTAtom"v11" e = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

H₄ :

lookupTAtom"v12" e = SomeWIntx mod 2 ^ 64

H₆ :

lookupTAtom"chk1" e = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

IH :

□

HK :

contcf d callers

Hn :

ptsnode_psb ptr_addr ≔ na; ptr_cap ≔ nc x

Hl :

lstptr_addr ≔ na; ptr_cap ≔ nc xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JGotoPollTAtom"L3" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel − 1

wp_node b mkPtrna nc x xs

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

x :

xs :

listZ

fuel, b, s₀, na :

nc :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hb₂ :

b mod 16 = 0

Hz :

fuel ≠ 0

e :

listname × word

Hput₀ :

lookupTAtom"v15" e = SomeWPtrptr_addr ≔ na; ptr_cap ≔ nc

H₇ :

lookupTAtom"v13" e = SomeWInts₀ mod 2 ^ 64 + x mod 2 ^ 64 mod 2 ^ 64 mod 2 ^ 64

H₅ :

lookupTAtom"chk0" e = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

H₃ :

lookupTAtom"v8" e = SomeWInt1

H₁ :

lookupTAtom"pr.1" e = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

H₀ :

lookupTAtom"pr.2" e = SomeWInts₀

H :

lookupTAtom"v7" e = SomeWIntb

H₂ :

lookupTAtom"v11" e = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

H₄ :

lookupTAtom"v12" e = SomeWIntx mod 2 ^ 64

H₆ :

lookupTAtom"chk1" e = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

IH :

□

HK :

contcf d callers

Hn :

ptsnode_psb ptr_addr ≔ na; ptr_cap ≔ nc x

Hl :

lstptr_addr ≔ na; ptr_cap ≔ nc xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"L3" SomeTAtom"L4" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel − 1

wp_fuel

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

x :

xs :

listZ

fuel, b, s₀, na :

nc :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hb₂ :

b mod 16 = 0

Hz :

fuel ≠ 0

e :

listname × word

Hput₀ :

lookupTAtom"v15" e = SomeWPtrptr_addr ≔ na; ptr_cap ≔ nc

H₇ :

lookupTAtom"v13" e = SomeWInts₀ mod 2 ^ 64 + x mod 2 ^ 64 mod 2 ^ 64 mod 2 ^ 64

H₅ :

lookupTAtom"chk0" e = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

H₃ :

lookupTAtom"v8" e = SomeWInt1

H₁ :

lookupTAtom"pr.1" e = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

H₀ :

lookupTAtom"pr.2" e = SomeWInts₀

H :

lookupTAtom"v7" e = SomeWIntb

H₂ :

lookupTAtom"v11" e = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

H₄ :

lookupTAtom"v12" e = SomeWIntx mod 2 ^ 64

H₆ :

lookupTAtom"chk1" e = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

Hz₀ :

fuel − 1 ≠ 0

IH :

□

HK :

contcf d callers

Hn :

ptsnode_psb ptr_addr ≔ na; ptr_cap ≔ nc x

Hl :

lstptr_addr ≔ na; ptr_cap ≔ nc xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"L3" SomeTAtom"L4" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel − 1

wp_node b mkPtrna nc x xs

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

x :

xs :

listZ

fuel, b, s₀, na :

nc :

Hb₀ :

0 < b

Hb₁ :

b + 16 ≤ 2 ^ 48

Hb₂ :

b mod 16 = 0

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

e :

listname × word

Hput₀ :

lookupTAtom"pr.1" e = SomeWPtrptr_addr ≔ na; ptr_cap ≔ nc

H₇ :

lookupTAtom"v15" e = SomeWPtrptr_addr ≔ na; ptr_cap ≔ nc

H₅ :

lookupTAtom"v13" e = SomeWInts₀ mod 2 ^ 64 + x mod 2 ^ 64 mod 2 ^ 64 mod 2 ^ 64

H₃ :

lookupTAtom"chk0" e = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

H₁ :

lookupTAtom"v8" e = SomeWInt1

H :

lookupTAtom"v7" e = SomeWIntb

H₀ :

lookupTAtom"v11" e = SomeWPtrptr_addr ≔ b + 8; ptr_cap ≔ Objb

H₂ :

lookupTAtom"v12" e = SomeWIntx mod 2 ^ 64

H₄ :

lookupTAtom"chk1" e = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

H₆ :

lookupTAtom"pr.2" e = SomeWInts₀ mod 2 ^ 64 + x mod 2 ^ 64 mod 2 ^ 64 mod 2 ^ 64 mod 2 ^ 64

IH :

□

HK :

contcf d callers

Hn :

ptsnode_psb ptr_addr ≔ na; ptr_cap ≔ nc x

Hl :

lstptr_addr ≔ na; ptr_cap ≔ nc xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" LetTAtom"v7" L Ptoi TmpTAtom"pr.1"; LetTAtom"v8" W CmpNe L TmpTAtom"v7"; Const0 JBranchTmpTAtom"v8" ToTAtom"L4" ToTAtom"L5" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel − 1 − 1

iApply IH $! _ mkPtrna nc xs with [%] [%] Hl HK ; eassumption | eexists ; eassumption

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

iLöb as IH

iIntros e p xs fuel Hp s₀ Hs Hl HK

destruct xs as | x xs

–iDestruct Hl as %→

iApply wpc_next_ emp%I with [//] ; let m ≔ fresh "m" in let s ≔ fresh "s" in iIntros m s _ _ ; iPureIntro ; compute_eq | iNext ; iIntros _ ; iApply HK

–iDestruct Hl as b na nc → & Hb₀ & Hb₁ & Hb₂ [Hn Hl]

wp_node b mkPtrna nc x xs

wp_node b mkPtrna nc x xs

wp_node b mkPtrna nc x xs

iApply IH $! _ mkPtrna nc xs with [%] [%] Hl HK ; eassumption | eexists ; eassumption

sum's specification, the rule for calling it: from any caller frame cf whose call binds the result to d, over any callers stack, owning the list from p and the continuation, the call is safe.

327Lemma sum_spec

∀ cf d callers p xs fuel

⊢ lstp xs −∗ contcf d callers −∗ wpclge EConfmkFramels_fn"sum" TAtom"v0", WPtrp [ ] None EnterTAtom"start" None cf, mkPendingCResultd L None :: callers fuel

Explore proof 7 tactics

Initial goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

p :

xs :

listZ

fuel :

⊢

lstp xs −∗ contcf d callers −∗ wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"start" None cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

iIntros Hl HK

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

p :

xs :

listZ

fuel :

Hl :

lstp xs

HK :

contcf d callers

∗

wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"start" None cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

wp_fuel

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

p :

xs :

listZ

fuel :

Hz :

fuel ≠ 0

Hl :

lstp xs

HK :

contcf d callers

∗

wpclge EConffr_fn ≔ ls_fn"sum"; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"start" None cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel

wp_emp

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

p :

xs :

listZ

fuel :

Hz :

fuel ≠ 0

Hl :

lstp xs

HK :

contcf d callers

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L3" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel − 1

wp_emp

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

p :

xs :

listZ

fuel :

Hz :

fuel ≠ 0

Hl :

lstp xs

HK :

contcf d callers

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"L3" SomeTAtom"start" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel − 1

wp_fuel

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

p :

xs :

listZ

fuel :

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

Hl :

lstp xs

HK :

contcf d callers

∗

wp_emp

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

cf :

d :

callers :

listframe × pending

p :

xs :

listZ

fuel :

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

Hl :

lstp xs

HK :

contcf d callers

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ putTAtom"pr.1" WPtrp putTAtom"pr.2" WInt0 TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L3" LetTAtom"v7" L Ptoi TmpTAtom"pr.1"; LetTAtom"v8" W CmpNe L TmpTAtom"v7"; Const0 JBranchTmpTAtom"v8" ToTAtom"L4" ToTAtom"L5" cf, pd_res ≔ CResultd L; pd_conv ≔ None :: callers fuel − 1 − 1

iApply sum_loop with [%] [%] Hl HK ; reflexivity | eexists ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

iIntros Hl HK

iApply sum_loop with [%] [%] Hl HK ; reflexivity | eexists ; reflexivity

A new node's object, split into the pieces the loop body uses: its life, its first aux slot, and its two cells; the other aux slots are dropped.

340Lemma obj_split

∀ base

ptsobj_psbase heap_req16 16 −∗ ptsPLivebase, VLivemkRegionbase base + 16 Heap Live ∗ ptsPAuxbase 0, VAuxCNone ∗ ptscellbase 0 0 ∗ ptscellbase 8 0

Explore proof 4 tactics

Initial goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

base :

⊢

ptsobj_psbase heap_req16 16 −∗ ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live ∗ ptsPAuxbase 0, VAuxCNone ∗ ptscellbase 0 0 ∗ ptscellbase 8 0

assert E : obj_psbase heap_req16 16 = PLivebase, VLivemkRegionbase base + 16 Heap Live ++ cellbase 0 0 ++ cellbase 8 0 ++ PAuxbase 0, VAuxCNone ++ λi ⇒ PAuxbase i, VAuxCNone <$> seqZ1 15 by reflexivity

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

base :

E :

obj_psbase heap_req16 16 = PLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live ++ cellbase 0 0 ++ cellbase 8 0 ++ PAuxbase 0, VAuxCNone ++ λi : Z ⇒ PAuxbase i, VAuxCNone <$> seqZ1 15

⊢

ptsobj_psbase heap_req16 16 −∗ ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live ∗ ptsPAuxbase 0, VAuxCNone ∗ ptscellbase 0 0 ∗ ptscellbase 8 0

rewrite E ! pts_app

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

base :

E :

⊢

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live ∗ ptscellbase 0 0 ∗ ptscellbase 8 0 ∗ ptsPAuxbase 0, VAuxCNone ∗ ptsλi : Z ⇒ PAuxbase i, VAuxCNone <$> seqZ1 15 −∗ ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live ∗ ptsPAuxbase 0, VAuxCNone ∗ ptscellbase 0 0 ∗ ptscellbase 8 0

iIntros (Hl & H₀ & H₈ & Ha & _)

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

base :

E :

Hl :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

H₀ :

ptscellbase 0 0

H₈ :

ptscellbase 8 0

Ha :

ptsPAuxbase 0, VAuxCNone

∗

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live ∗ ptsPAuxbase 0, VAuxCNone ∗ ptscellbase 0 0 ∗ ptscellbase 8 0

iFrame

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

assert E : obj_psbase heap_req16 16 = PLivebase, VLivemkRegionbase base + 16 Heap Live ++ cellbase 0 0 ++ cellbase 8 0 ++ PAuxbase 0, VAuxCNone ++ λi ⇒ PAuxbase i, VAuxCNone <$> seqZ1 15 by reflexivity

rewrite E ! pts_app

iIntros (Hl & H₀ & H₈ & Ha & _)

iFrame

A step of listsum's loop body that may read the new object's region.

353Ltac wp_live ≔

iApply wpc_next_ pts_ with Hlv;|let m ≔ fresh "m" inlet s ≔ fresh "s" iniIntros m s Hσ Hlv ; iDestruct pts_facts with Hσ Hlv as %? ; iPureIntro;match goal withH : owned_facts_ _ |- _⇒let H₁ ≔ fresh in destruct H as H₁ _ ; cbn [ all_agree fst snd agree_piece ] in H₁ ; destruct H₁ as ? _ _end;compute_eq|iNext ; iIntros Hlv ; gen_env

listsum's loop, from the point after its head's phis: with pr.2 an int i in range, pr.1 the list's pointer h and v0 the input, owning the list, the run is safe. By Löb induction; each iteration allocates a node, stores h and i in it, and the loop goes on with i + 1 and the longer list; at the end sum is called with the list.

369Lemma ls_loop

∀ n

⊢ ∀e i h xs fuel, ⌜lookupTAtom"pr.2" e = SomeWInti ∧ 0 ≤ i < 2 ^ 31 ∧ lookupTAtom"pr.1" e = SomeWPtrh ∧ lookupTAtom"v0" e = SomeWIntn⌝ −∗ lsth xs −∗ wpclge EConfmkFramels_fn"listsum" e [ ] None ExecTAtom"L4" b_instsls_L4 b_jumpls_L4 [ ] fuel

Explore proof 48 tactics

Initial goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n :

⊢

⊢ ∀e : listname × word i : Z h : ptr xs : listZ fuel : Z, ⌜lookupTAtom"pr.2" e = SomeWInti ∧ 0 ≤ i < 2 ^ 31 ∧ lookupTAtom"pr.1" e = SomeWPtrh ∧ lookupTAtom"v0" e = SomeWIntn⌝ −∗ lsth xs −∗ wpclge EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" b_instsls_L4 b_jumpls_L4 [ ] fuel

iLöb as IH

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n :

IH :

▷∀e : listname × word i : Z h : ptr xs : listZ fuel : Z, ⌜lookupTAtom"pr.2" e = SomeWInti ∧ 0 ≤ i < 2 ^ 31 ∧ lookupTAtom"pr.1" e = SomeWPtrh ∧ lookupTAtom"v0" e = SomeWIntn⌝ −∗ lsth xs −∗ wpclge EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" b_instsls_L4 b_jumpls_L4 [ ] fuel

□

∀e : listname × word i : Z h : ptr xs : listZ fuel : Z, ⌜lookupTAtom"pr.2" e = SomeWInti ∧ 0 ≤ i < 2 ^ 31 ∧ lookupTAtom"pr.1" e = SomeWPtrh ∧ lookupTAtom"v0" e = SomeWIntn⌝ −∗ lsth xs −∗ wpclge EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" b_instsls_L4 b_jumpls_L4 [ ] fuel

iIntros e i h xs fuel Hi & Hir & Hh & Hn Hl

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n :

e :

listname × word

i :

h :

xs :

listZ

fuel :

Hi :

lookupTAtom"pr.2" e = SomeWInti

Hir :

0 ≤ i < 2 ^ 31

Hh :

lookupTAtom"pr.1" e = SomeWPtrh

Hn :

lookupTAtom"v0" e = SomeWIntn

IH :

▷∀e₀ : listname × word i₀ : Z h₀ : ptr xs₀ : listZ fuel₀ : Z, ⌜lookupTAtom"pr.2" e₀ = SomeWInti₀ ∧ 0 ≤ i₀ < 2 ^ 31 ∧ lookupTAtom"pr.1" e₀ = SomeWPtrh₀ ∧ lookupTAtom"v0" e₀ = SomeWIntn⌝ −∗ lsth₀ xs₀ −∗ wpclge EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" b_instsls_L4 b_jumpls_L4 [ ] fuel₀

□

Hl :

lsth xs

∗

wpclge EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" b_instsls_L4 b_jumpls_L4 [ ] fuel

wp_emp

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hput :

lookupTAtom"v10" e₀

Some

WInt

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

→

else

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

∀e : listname × word i₀ : Z h₀ : ptr xs₀ : listZ fuel₀ : Z, ⌜lookupTAtom"pr.2" e = SomeWInti₀ ∧ 0 ≤ i₀ < 2 ^ 31 ∧ lookupTAtom"pr.1" e = SomeWPtrh₀ ∧ lookupTAtom"v0" e = SomeWIntn⌝ −∗ lsth₀ xs₀ −∗ wpclge EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" b_instsls_L4 b_jumpls_L4 [ ] fuel₀

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

match goal withH : lookupTAtom"v10" _ = SomeWIntif ?c then 1 else 0 |- _⇒destruct c eqn: Hcend

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

focused goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

–assert Hi₁ : i + 1 < 2 ^ 31

3 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

⊢

i + 1 < 2 ^ 31

focused goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hi₁ :

i + 1 < 2 ^ 31

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

{apply Z.ltb_lt in Hc

3 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

⊢

i + 1 < 2 ^ 31

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hi₁ :

i + 1 < 2 ^ 31

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

revert Hc

3 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

⊢

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

→

i + 1 < 2 ^ 31

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hi₁ :

i + 1 < 2 ^ 31

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

repeat match goal with|- context [if ?b then _ else _]⇒let Hb ≔ fresh in destruct b eqn: Hb ; apply Z.leb_le in Hb | apply Z.leb_gt in Hbend;intros;pose proof Z.mod_pos_boundn 2 ^ 32 ltac:lia;pose proof Z.mod_pos_boundn mod 2 ^ 32 2 ^ 32 ltac:lia;lia

2 open

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hi₁ :

i + 1 < 2 ^ 31

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

wp_emp

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hi₁ :

i + 1 < 2 ^ 31

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"L5" SomeTAtom"L4" [ ] fuel

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

wp_fuel

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"L5" SomeTAtom"L4" [ ] fuel

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

wp_emp

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L5" LetTAtom"v12" P Alloc16 Const16; LetTAtom"chk0" A Check0 8 Write 8 TmpTAtom"v12"; RawStorePointer0 TmpTAtom"pr.1" TmpTAtom"chk0" AuxEnsure; LowerBarrier; RootedReload; LowerWrite; AddressWrite; FlightTAtom"v16" Add FAddressTmpTAtom"v12"; FValueConst8 LowerOfTmpTAtom"v12"; LetTAtom"v18" L ExtSw TmpTAtom"pr.2"; LetTAtom"chk1" A HalfCheckUpper 0 8 Write 1 TmpTAtom"chk0"; TmpTAtom"v16"; RawStoreWl 0 TmpTAtom"v18" TmpTAtom"chk1"; LetTAtom"v21" W Add TmpTAtom"pr.2"; Const1 JGotoPollTAtom"L4" [ ] fuel − 1

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

iApply wpc_alloc_ heap_req16 16 ; vm_compute ; reflexivity | vm_compute ; discriminate | let m ≔ fresh "m" in intros m ; compute_eq |

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

IH :

□

Hl :

lsth xs

∗

▷∀base : Z, ⌜0 < base ∧ base mod req_alignheap_req16 16 = 0 ∧ base + req_extentheap_req16 16 ≤ 2 ^ 48⌝ −∗ ptsobj_psbase heap_req16 16 −∗ wpclge IM.EConfλbase₀ : Z ⇒ fr_fn ≔ ls_fn"listsum"; fr_env ≔ putTAtom"v12" WPtrptr_addr ≔ base₀; ptr_cap ≔ Objbase₀ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L5" LetTAtom"chk0" A Check0 8 Write 8 TmpTAtom"v12"; RawStorePointer0 TmpTAtom"pr.1" TmpTAtom"chk0" AuxEnsure; LowerBarrier; RootedReload; LowerWrite; AddressWrite; FlightTAtom"v16" Add FAddressTmpTAtom"v12"; FValueConst8 LowerOfTmpTAtom"v12"; LetTAtom"v18" L ExtSw TmpTAtom"pr.2"; LetTAtom"chk1" A HalfCheckUpper 0 8 Write 1 TmpTAtom"chk0"; TmpTAtom"v16"; RawStoreWl 0 TmpTAtom"v18" TmpTAtom"chk1"; LetTAtom"v21" W Add TmpTAtom"pr.2"; Const1 JGotoPollTAtom"L4"base [ ] fuel − 1

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

iNext

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

IH :

□

Hl :

lsth xs

∗

∀base : Z, ⌜0 < base ∧ base mod req_alignheap_req16 16 = 0 ∧ base + req_extentheap_req16 16 ≤ 2 ^ 48⌝ −∗ ptsobj_psbase heap_req16 16 −∗ wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ putTAtom"v12" WPtrptr_addr ≔ base; ptr_cap ≔ Objbase e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L5" LetTAtom"chk0" A Check0 8 Write 8 TmpTAtom"v12"; RawStorePointer0 TmpTAtom"pr.1" TmpTAtom"chk0" AuxEnsure; LowerBarrier; RootedReload; LowerWrite; AddressWrite; FlightTAtom"v16" Add FAddressTmpTAtom"v12"; FValueConst8 LowerOfTmpTAtom"v12"; LetTAtom"v18" L ExtSw TmpTAtom"pr.2"; LetTAtom"chk1" A HalfCheckUpper 0 8 Write 1 TmpTAtom"chk0"; TmpTAtom"v16"; RawStoreWl 0 TmpTAtom"v18" TmpTAtom"chk1"; LetTAtom"v21" W Add TmpTAtom"pr.2"; Const1 JGotoPollTAtom"L4" [ ] fuel − 1

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

iIntros base Hb₀ & Hb₁ & Hb₂ Hobj

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod req_alignheap_req16 16 = 0

Hb₂ :

base + req_extentheap_req16 16 ≤ 2 ^ 48

IH :

□

Hl :

lsth xs

Hobj :

ptsobj_psbase heap_req16 16

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ putTAtom"v12" WPtrptr_addr ≔ base; ptr_cap ≔ Objbase e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L5" LetTAtom"chk0" A Check0 8 Write 8 TmpTAtom"v12"; RawStorePointer0 TmpTAtom"pr.1" TmpTAtom"chk0" AuxEnsure; LowerBarrier; RootedReload; LowerWrite; AddressWrite; FlightTAtom"v16" Add FAddressTmpTAtom"v12"; FValueConst8 LowerOfTmpTAtom"v12"; LetTAtom"v18" L ExtSw TmpTAtom"pr.2"; LetTAtom"chk1" A HalfCheckUpper 0 8 Write 1 TmpTAtom"chk0"; TmpTAtom"v16"; RawStoreWl 0 TmpTAtom"v18" TmpTAtom"chk1"; LetTAtom"v21" W Add TmpTAtom"pr.2"; Const1 JGotoPollTAtom"L4" [ ] fuel − 1

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

cbv beta

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod req_alignheap_req16 16 = 0

Hb₂ :

base + req_extentheap_req16 16 ≤ 2 ^ 48

IH :

□

Hl :

lsth xs

Hobj :

ptsobj_psbase heap_req16 16

∗

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

change req_alignheap_req16 16 with 16 in Hb₁

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + req_extentheap_req16 16 ≤ 2 ^ 48

IH :

□

Hl :

lsth xs

Hobj :

ptsobj_psbase heap_req16 16

∗

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

change req_extentheap_req16 16 with 16 in Hb₂

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

IH :

□

Hl :

lsth xs

Hobj :

ptsobj_psbase heap_req16 16

∗

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

iDestruct obj_split with Hobj as (Hlv & Hax & Hc₀ & Hc₈)

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hput :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

IH :

□

Hl :

lsth xs

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

ptsPAuxbase 0, VAuxCNone

Hc₀ :

ptscellbase 0 0

Hc₈ :

ptscellbase 8 0

∗

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

gen_env

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

e :

listname × word

Hput₀ :

lookupTAtom"v12" e = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"pr.2" e = SomeWInti

H₁ :

lookupTAtom"pr.1" e = SomeWPtrh

H₀ :

lookupTAtom"v0" e = SomeWIntn

H :

lookupTAtom"v10" e = SomeWInt1

IH :

∀e₀ : listname × word i₀ : Z h₀ : ptr xs₀ : listZ fuel₀ : Z, ⌜lookupTAtom"pr.2" e₀ = SomeWInti₀ ∧ 0 ≤ i₀ < 2 ^ 31 ∧ lookupTAtom"pr.1" e₀ = SomeWPtrh₀ ∧ lookupTAtom"v0" e₀ = SomeWIntn⌝ −∗ lsth₀ xs₀ −∗ wpclge EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" b_instsls_L4 b_jumpls_L4 [ ] fuel₀

□

Hl :

lsth xs

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

ptsPAuxbase 0, VAuxCNone

Hc₀ :

ptscellbase 0 0

Hc₈ :

ptscellbase 8 0

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L5" LetTAtom"chk0" A Check0 8 Write 8 TmpTAtom"v12"; RawStorePointer0 TmpTAtom"pr.1" TmpTAtom"chk0" AuxEnsure; LowerBarrier; RootedReload; LowerWrite; AddressWrite; FlightTAtom"v16" Add FAddressTmpTAtom"v12"; FValueConst8 LowerOfTmpTAtom"v12"; LetTAtom"v18" L ExtSw TmpTAtom"pr.2"; LetTAtom"chk1" A HalfCheckUpper 0 8 Write 1 TmpTAtom"chk0"; TmpTAtom"v16"; RawStoreWl 0 TmpTAtom"v18" TmpTAtom"chk1"; LetTAtom"v21" W Add TmpTAtom"pr.2"; Const1 JGotoPollTAtom"L4" [ ] fuel − 1

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

wp_live

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

e₀ :

listname × word

Hput :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₃ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

H₂ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

IH :

□

Hl :

lsth xs

Hax :

ptsPAuxbase 0, VAuxCNone

Hc₀ :

ptscellbase 0 0

Hc₈ :

ptscellbase 8 0

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L5" RawStorePointer0 TmpTAtom"pr.1" TmpTAtom"chk0" AuxEnsure; LowerBarrier; RootedReload; LowerWrite; AddressWrite; FlightTAtom"v16" Add FAddressTmpTAtom"v12"; FValueConst8 LowerOfTmpTAtom"v12"; LetTAtom"v18" L ExtSw TmpTAtom"pr.2"; LetTAtom"chk1" A HalfCheckUpper 0 8 Write 1 TmpTAtom"chk0"; TmpTAtom"v16"; RawStoreWl 0 TmpTAtom"v18" TmpTAtom"chk1"; LetTAtom"v21" W Add TmpTAtom"pr.2"; Const1 JGotoPollTAtom"L4" [ ] fuel − 1

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

iApply wpc_write_ PLivebase, VLivemkRegionbase base + 16 Heap Live ++ PAuxbase 0, VAuxCNone ++ cellbase 0 0 PLivebase, VLivemkRegionbase base + 16 Heap Live ++ PAuxbase 0, VAuxptr_caph ++ cellbase 0 ptr_addrh with [Hlv Hax Hc₀] ; reflexivity | reflexivity | let m ≔ fresh "m" in intros m Hf & Hd & _ ; apply all_agree_app in Hf as Hf _ ; cbn [ all_agree fst snd agree_piece ] in Hf ; destruct Hf as Hlive _ ; pose proof Hlive as Hor _ ; split ; compute_eq | ; cbv beta ; eapply ptr_store_ok ; exact Hd | exact Hlive | cbn ; lia | lia | rewrite ! pts_app ; iFrame | iNext ; iIntros Hps ; iDestruct pts_app with Hps as [Hlv Hps] ; iDestruct pts_app with Hps as [Hax Hc₀] ; gen_env

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

e₀ :

listname × word

Hput :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₃ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

H₂ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

IH :

□

Hl :

lsth xs

Hc₈ :

ptscellbase 8 0

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L5" FlightTAtom"v16" Add FAddressTmpTAtom"v12"; FValueConst8 LowerOfTmpTAtom"v12"; LetTAtom"v18" L ExtSw TmpTAtom"pr.2"; LetTAtom"chk1" A HalfCheckUpper 0 8 Write 1 TmpTAtom"chk0"; TmpTAtom"v16"; RawStoreWl 0 TmpTAtom"v18" TmpTAtom"chk1"; LetTAtom"v21" W Add TmpTAtom"pr.2"; Const1 JGotoPollTAtom"L4" [ ] fuel − 1

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

wp_emp

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

e :

listname × word

Hput₀ :

lookupTAtom"v16" e = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"v12" e = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"pr.2" e = SomeWInti

H₁ :

lookupTAtom"pr.1" e = SomeWPtrh

H₀ :

lookupTAtom"v0" e = SomeWIntn

H :

lookupTAtom"v10" e = SomeWInt1

H₃ :

lookupTAtom"chk0" e = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

IH :

□

Hl :

lsth xs

Hc₈ :

ptscellbase 8 0

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L5" LetTAtom"v18" L ExtSw TmpTAtom"pr.2"; LetTAtom"chk1" A HalfCheckUpper 0 8 Write 1 TmpTAtom"chk0"; TmpTAtom"v16"; RawStoreWl 0 TmpTAtom"v18" TmpTAtom"chk1"; LetTAtom"v21" W Add TmpTAtom"pr.2"; Const1 JGotoPollTAtom"L4" [ ] fuel − 1

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

wp_emp

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

e₀ :

listname × word

Hput :

lookupTAtom"v18" e₀ = SomeWInti

H₅ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₃ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

H₂ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

IH :

□

Hl :

lsth xs

Hc₈ :

ptscellbase 8 0

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L5" LetTAtom"chk1" A HalfCheckUpper 0 8 Write 1 TmpTAtom"chk0"; TmpTAtom"v16"; RawStoreWl 0 TmpTAtom"v18" TmpTAtom"chk1"; LetTAtom"v21" W Add TmpTAtom"pr.2"; Const1 JGotoPollTAtom"L4" [ ] fuel − 1

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

wp_live

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

e :

listname × word

Hput₀ :

lookupTAtom"chk1" e = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"v16" e = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"v12" e = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"pr.2" e = SomeWInti

H₁ :

lookupTAtom"pr.1" e = SomeWPtrh

H₀ :

lookupTAtom"v0" e = SomeWIntn

H :

lookupTAtom"v10" e = SomeWInt1

H₃ :

lookupTAtom"chk0" e = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₅ :

lookupTAtom"v18" e = SomeWInti

IH :

□

Hl :

lsth xs

Hc₈ :

ptscellbase 8 0

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L5" RawStoreWl 0 TmpTAtom"v18" TmpTAtom"chk1"; LetTAtom"v21" W Add TmpTAtom"pr.2"; Const1 JGotoPollTAtom"L4" [ ] fuel − 1

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

iApply wpc_write_ PLivebase, VLivemkRegionbase base + 16 Heap Live ++ cellbase 8 0 PLivebase, VLivemkRegionbase base + 16 Heap Live ++ cellbase 8 i with [Hlv Hc₈];|reflexivity|reflexivity|let m ≔ fresh "m" inintros m Hf & Hd & _ ; apply all_agree_app in Hf as Hf _ ; cbn [ all_agree fst snd agree_piece ] in Hf ; destruct Hf as Hlive _ ; pose proof Hlive as Hor _ ; split ; compute_eq | ; cbv beta ; split ; reflexivity | ;match goal with|- context [store_bytesm ?a 8 _]⇒destruct cell_store_okm base _ 8 a i Hd Hlive ltac:lia ltac:cbn ; lia ltac:lia as Hcs Hfrend;split;|apply all_agree_app ; split ; | exact Hcs ; cbn [ all_agree fst snd agree_piece ] ; split ; apply live_at_regionsm ; reflexivity | exact Hlive | exact I|eapply frame_ok_mono ; | exact Hfr ; intros l Hin ; rewrite fmap_app ; apply elem_of_app ; right ; exact Hin|rewrite ! pts_app ; iFrame|iNext ; iIntros Hps ; iDestruct pts_app with Hps as [Hlv Hc₈] ; gen_env

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

e :

listname × word

Hput₀ :

lookupTAtom"chk1" e = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"v16" e = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"v12" e = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"pr.2" e = SomeWInti

H₁ :

lookupTAtom"pr.1" e = SomeWPtrh

H₀ :

lookupTAtom"v0" e = SomeWIntn

H :

lookupTAtom"v10" e = SomeWInt1

H₃ :

lookupTAtom"chk0" e = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₅ :

lookupTAtom"v18" e = SomeWInti

IH :

□

Hl :

lsth xs

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hc₈ :

ptscellbase 8 i

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L5" LetTAtom"v21" W Add TmpTAtom"pr.2"; Const1 JGotoPollTAtom"L4" [ ] fuel − 1

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

wp_emp

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

e₀ :

listname × word

Hput :

lookupTAtom"v21" e₀ = SomeWInti + 1

H₇ :

lookupTAtom"v18" e₀ = SomeWInti

H₅ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₃ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

H₂ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

IH :

□

Hl :

lsth xs

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hc₈ :

ptscellbase 8 i

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L5" [ ] JGotoPollTAtom"L4" [ ] fuel − 1

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

wp_emp

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

e₀ :

listname × word

Hput :

lookupTAtom"v21" e₀ = SomeWInti + 1

H₇ :

lookupTAtom"v18" e₀ = SomeWInti

H₅ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₃ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

H₂ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

IH :

□

Hl :

lsth xs

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hc₈ :

ptscellbase 8 i

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"L4" SomeTAtom"L5" [ ] fuel − 1

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

wp_fuel

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

e₀ :

listname × word

Hput :

lookupTAtom"v21" e₀ = SomeWInti + 1

H₇ :

lookupTAtom"v18" e₀ = SomeWInti

H₅ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₃ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

H₂ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

Hz₀ :

fuel − 1 ≠ 0

IH :

□

Hl :

lsth xs

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hc₈ :

ptscellbase 8 i

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"L4" SomeTAtom"L5" [ ] fuel − 1

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

wp_emp

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

Hz₀ :

fuel − 1 ≠ 0

e₀ :

listname × word

Hput :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₇ :

lookupTAtom"v21" e₀ = SomeWInti + 1

H₅ :

lookupTAtom"v18" e₀ = SomeWInti

H₃ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₁ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"pr.2" e₀ = SomeWInti + 1

IH :

□

Hl :

lsth xs

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hc₈ :

ptscellbase 8 i

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" LetTAtom"v10" W CmpSlt W TmpTAtom"pr.2"; TmpTAtom"v0" JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel − 1 − 1

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

iApply IH $! _ i + 1 mkPtrbase Objbase i :: xs with [%] [Hlv Hax Hc₀ Hc₈ Hl]

3 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

Hz₀ :

fuel − 1 ≠ 0

e₀ :

listname × word

Hput :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₇ :

lookupTAtom"v21" e₀ = SomeWInti + 1

H₅ :

lookupTAtom"v18" e₀ = SomeWInti

H₃ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₁ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"pr.2" e₀ = SomeWInti + 1

⊢

lookupTAtom"pr.2" e₀ = SomeWInti + 1 ∧ 0 ≤ i + 1 < 2 ^ 31 ∧ lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase ∧ lookupTAtom"v0" e₀ = SomeWIntn

focused goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

Hz₀ :

fuel − 1 ≠ 0

e₀ :

listname × word

Hput :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₇ :

lookupTAtom"v21" e₀ = SomeWInti + 1

H₅ :

lookupTAtom"v18" e₀ = SomeWInti

H₃ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₁ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"pr.2" e₀ = SomeWInti + 1

IH :

□

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

Hc₈ :

ptscellbase 8 i

Hl :

lsth xs

∗

lstptr_addr ≔ base; ptr_cap ≔ Objbase i :: xs

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

{split ; eassumption |

3 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

Hz₀ :

fuel − 1 ≠ 0

e₀ :

listname × word

Hput :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₇ :

lookupTAtom"v21" e₀ = SomeWInti + 1

H₅ :

lookupTAtom"v18" e₀ = SomeWInti

H₃ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₁ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"pr.2" e₀ = SomeWInti + 1

⊢

0 ≤ i + 1 < 2 ^ 31 ∧ lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase ∧ lookupTAtom"v0" e₀ = SomeWIntn

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

Hz₀ :

fuel − 1 ≠ 0

e₀ :

listname × word

Hput :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₇ :

lookupTAtom"v21" e₀ = SomeWInti + 1

H₅ :

lookupTAtom"v18" e₀ = SomeWInti

H₃ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₁ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"pr.2" e₀ = SomeWInti + 1

IH :

□

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

Hc₈ :

ptscellbase 8 i

Hl :

lsth xs

∗

lstptr_addr ≔ base; ptr_cap ≔ Objbase i :: xs

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

split ; lia |

3 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

Hz₀ :

fuel − 1 ≠ 0

e₀ :

listname × word

Hput :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₇ :

lookupTAtom"v21" e₀ = SomeWInti + 1

H₅ :

lookupTAtom"v18" e₀ = SomeWInti

H₃ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₁ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"pr.2" e₀ = SomeWInti + 1

⊢

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase ∧ lookupTAtom"v0" e₀ = SomeWIntn

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

Hz₀ :

fuel − 1 ≠ 0

e₀ :

listname × word

Hput :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₇ :

lookupTAtom"v21" e₀ = SomeWInti + 1

H₅ :

lookupTAtom"v18" e₀ = SomeWInti

H₃ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₁ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"pr.2" e₀ = SomeWInti + 1

IH :

□

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

Hc₈ :

ptscellbase 8 i

Hl :

lsth xs

∗

lstptr_addr ≔ base; ptr_cap ≔ Objbase i :: xs

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

split ; eassumption

2 open

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

Hz₀ :

fuel − 1 ≠ 0

e₀ :

listname × word

Hput :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₇ :

lookupTAtom"v21" e₀ = SomeWInti + 1

H₅ :

lookupTAtom"v18" e₀ = SomeWInti

H₃ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₁ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"pr.2" e₀ = SomeWInti + 1

IH :

□

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

Hc₈ :

ptscellbase 8 i

Hl :

lsth xs

∗

lstptr_addr ≔ base; ptr_cap ≔ Objbase i :: xs

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

{cbn [ lst ]

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

Hz₀ :

fuel − 1 ≠ 0

e₀ :

listname × word

Hput :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₇ :

lookupTAtom"v21" e₀ = SomeWInti + 1

H₅ :

lookupTAtom"v18" e₀ = SomeWInti

H₃ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₁ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"pr.2" e₀ = SomeWInti + 1

IH :

□

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

Hc₈ :

ptscellbase 8 i

Hl :

lsth xs

∗

∃b : Z nx : ptr, ⌜ptr_addr ≔ base; ptr_cap ≔ Objbase = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b + 16 ≤ 2 ^ 48 ∧ b mod 16 = 0⌝ ∗ ptsnode_psb nx i ∗ lstnx xs

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

iExists base, h

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

Hz₀ :

fuel − 1 ≠ 0

e₀ :

listname × word

Hput :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₇ :

lookupTAtom"v21" e₀ = SomeWInti + 1

H₅ :

lookupTAtom"v18" e₀ = SomeWInti

H₃ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₁ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"pr.2" e₀ = SomeWInti + 1

IH :

□

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

Hc₈ :

ptscellbase 8 i

Hl :

lsth xs

∗

⌜ptr_addr ≔ base; ptr_cap ≔ Objbase = ptr_addr ≔ base; ptr_cap ≔ Objbase ∧ 0 < base ∧ base + 16 ≤ 2 ^ 48 ∧ base mod 16 = 0⌝ ∗ ptsnode_psbase h i ∗ lsth xs

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

iSplitR ; iPureIntro ; split ; reflexivity | ; lia |

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

Hz₀ :

fuel − 1 ≠ 0

e₀ :

listname × word

Hput :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₇ :

lookupTAtom"v21" e₀ = SomeWInti + 1

H₅ :

lookupTAtom"v18" e₀ = SomeWInti

H₃ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₁ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"pr.2" e₀ = SomeWInti + 1

IH :

□

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

Hc₈ :

ptscellbase 8 i

Hl :

lsth xs

∗

ptsnode_psbase h i ∗ lsth xs

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

iFrame Hl

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

Hz₀ :

fuel − 1 ≠ 0

e₀ :

listname × word

Hput :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₇ :

lookupTAtom"v21" e₀ = SomeWInti + 1

H₅ :

lookupTAtom"v18" e₀ = SomeWInti

H₃ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₁ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"pr.2" e₀ = SomeWInti + 1

IH :

□

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

Hc₈ :

ptscellbase 8 i

∗

ptsnode_psbase h i

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

rewrite / node_ps ! pts_app

2 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

true

Hi₁ :

i + 1 < 2 ^ 31

Hz :

fuel ≠ 0

base :

Hb₀ :

0 < base

Hb₁ :

base mod 16 = 0

Hb₂ :

base + 16 ≤ 2 ^ 48

Hz₀ :

fuel − 1 ≠ 0

e₀ :

listname × word

Hput :

lookupTAtom"pr.1" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₇ :

lookupTAtom"v21" e₀ = SomeWInti + 1

H₅ :

lookupTAtom"v18" e₀ = SomeWInti

H₃ :

lookupTAtom"chk0" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₂ :

lookupTAtom"v10" e₀ = SomeWInt1

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"v12" e₀ = SomeWPtrptr_addr ≔ base; ptr_cap ≔ Objbase

H₁ :

lookupTAtom"v16" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₄ :

lookupTAtom"chk1" e₀ = SomeWPtrptr_addr ≔ base + 8; ptr_cap ≔ Objbase

H₆ :

lookupTAtom"pr.2" e₀ = SomeWInti + 1

IH :

□

Hlv :

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live

Hax :

ptsPAuxbase 0, VAuxptr_caph

Hc₀ :

ptscellbase 0 ptr_addrh

Hc₈ :

ptscellbase 8 i

∗

ptsPLivebase, VLiver_base ≔ base; r_end ≔ base + 16; r_kind ≔ Heap; r_life ≔ Live ∗ ptsPAuxbase 0, VAuxptr_caph ∗ ptscellbase 0 ptr_addrh ∗ ptscellbase 8 i

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

iFrame

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" [ ] JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel

–wp_emp

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"L7" SomeTAtom"L4" [ ] fuel

wp_fuel

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hz :

fuel ≠ 0

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"L7" SomeTAtom"L4" [ ] fuel

wp_emp

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hz :

fuel ≠ 0

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L7" CallCResultTAtom"v23" L GlobalTAtom"sum" ArgP TmpTAtom"pr.1" JRetTmpTAtom"v23" [ ] fuel − 1

wp_emp

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hz :

fuel ≠ 0

IH :

□

Hl :

lsth xs

∗

wpclge IM.EConffr_fn ≔ ls_fn"sum"; fr_env ≔ TAtom"v0", WPtrh; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"start" None fr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L7" [ ] JRetTmpTAtom"v23", pd_res ≔ CResultTAtom"v23" L; pd_conv ≔ None fuel − 1

iApply sum_spec with Hl

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hz :

fuel ≠ 0

IH :

□

contfr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L7" [ ] JRetTmpTAtom"v23" TAtom"v23" [ ]

iIntros y fuel′

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hz :

fuel ≠ 0

y, fuel′ :

IH :

□

wpclge EConffr_fn ≔ fr_fnfr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L7" [ ] JRetTmpTAtom"v23"; fr_env ≔ putTAtom"v23" WInty fr_envfr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L7" [ ] JRetTmpTAtom"v23"; fr_locals ≔ fr_localsfr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L7" [ ] JRetTmpTAtom"v23"; fr_doomed ≔ fr_doomedfr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L7" [ ] JRetTmpTAtom"v23"; fr_at ≔ fr_atfr_fn ≔ ls_fn"listsum"; fr_env ≔ e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L7" [ ] JRetTmpTAtom"v23" [ ] fuel′

cbn [ fr_fn fr_env fr_locals fr_doomed fr_at ]

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

e₀ :

listname × word

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hput :

lookupTAtom"v10" e₀ = SomeWInt0

H :

lookupTAtom"v0" e₀ = SomeWIntn

H₀ :

lookupTAtom"pr.1" e₀ = SomeWPtrh

H₁ :

lookupTAtom"pr.2" e₀ = SomeWInti

Hz :

fuel ≠ 0

y, fuel′ :

IH :

□

wpclge EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ putTAtom"v23" WInty e₀; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L7" [ ] JRetTmpTAtom"v23" [ ] fuel′

gen_env

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, i :

h :

xs :

listZ

fuel :

Hir :

0 ≤ i < 2 ^ 31

Hc :

2 ^ 31 ≤? n mod 2 ^ 32 mod 2 ^ 32

→

n mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32

else

n mod 2 ^ 32 mod 2 ^ 32

false

Hz :

fuel ≠ 0

y, fuel′ :

e :

listname × word

Hput₀ :

lookupTAtom"v23" e = SomeWInty

H₂ :

lookupTAtom"pr.2" e = SomeWInti

H₁ :

lookupTAtom"pr.1" e = SomeWPtrh

H₀ :

lookupTAtom"v0" e = SomeWIntn

H :

lookupTAtom"v10" e = SomeWInt0

IH :

□

wpclge EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ e; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L7" [ ] JRetTmpTAtom"v23" [ ] fuel′

iApply wpc_done_ emp%I _ _ _ Ret_ with [//] ; intros | let m ≔ fresh "m" in let s ≔ fresh "s" in iIntros m s _ _ ; iPureIntro ; compute_eq

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

iLöb as IH

iIntros e i h xs fuel Hi & Hir & Hh & Hn Hl

match goal withH : lookupTAtom"v10" _ = SomeWIntif ?c then 1 else 0 |- _⇒destruct c eqn: Hcend

–assert Hi₁ : i + 1 < 2 ^ 31

{apply Z.ltb_lt in Hc

revert Hc

repeat match goal with|- context [if ?b then _ else _]⇒let Hb ≔ fresh in destruct b eqn: Hb ; apply Z.leb_le in Hb | apply Z.leb_gt in Hbend;intros;pose proof Z.mod_pos_boundn 2 ^ 32 ltac:lia;pose proof Z.mod_pos_boundn mod 2 ^ 32 2 ^ 32 ltac:lia;lia

iApply wpc_alloc_ heap_req16 16 ; vm_compute ; reflexivity | vm_compute ; discriminate | let m ≔ fresh "m" in intros m ; compute_eq |

iNext

iIntros base Hb₀ & Hb₁ & Hb₂ Hobj

cbv beta

change req_alignheap_req16 16 with 16 in Hb₁

change req_extentheap_req16 16 with 16 in Hb₂

iDestruct obj_split with Hobj as (Hlv & Hax & Hc₀ & Hc₈)

gen_env

wp_live

iApply wpc_write_ PLivebase, VLivemkRegionbase base + 16 Heap Live ++ PAuxbase 0, VAuxCNone ++ cellbase 0 0 PLivebase, VLivemkRegionbase base + 16 Heap Live ++ PAuxbase 0, VAuxptr_caph ++ cellbase 0 ptr_addrh with [Hlv Hax Hc₀] ; reflexivity | reflexivity | let m ≔ fresh "m" in intros m Hf & Hd & _ ; apply all_agree_app in Hf as Hf _ ; cbn [ all_agree fst snd agree_piece ] in Hf ; destruct Hf as Hlive _ ; pose proof Hlive as Hor _ ; split ; compute_eq | ; cbv beta ; eapply ptr_store_ok ; exact Hd | exact Hlive | cbn ; lia | lia | rewrite ! pts_app ; iFrame | iNext ; iIntros Hps ; iDestruct pts_app with Hps as [Hlv Hps] ; iDestruct pts_app with Hps as [Hax Hc₀] ; gen_env

wp_live

iApply wpc_write_ PLivebase, VLivemkRegionbase base + 16 Heap Live ++ cellbase 8 0 PLivebase, VLivemkRegionbase base + 16 Heap Live ++ cellbase 8 i with [Hlv Hc₈];|reflexivity|reflexivity|let m ≔ fresh "m" inintros m Hf & Hd & _ ; apply all_agree_app in Hf as Hf _ ; cbn [ all_agree fst snd agree_piece ] in Hf ; destruct Hf as Hlive _ ; pose proof Hlive as Hor _ ; split ; compute_eq | ; cbv beta ; split ; reflexivity | ;match goal with|- context [store_bytesm ?a 8 _]⇒destruct cell_store_okm base _ 8 a i Hd Hlive ltac:lia ltac:cbn ; lia ltac:lia as Hcs Hfrend;split;|apply all_agree_app ; split ; | exact Hcs ; cbn [ all_agree fst snd agree_piece ] ; split ; apply live_at_regionsm ; reflexivity | exact Hlive | exact I|eapply frame_ok_mono ; | exact Hfr ; intros l Hin ; rewrite fmap_app ; apply elem_of_app ; right ; exact Hin|rewrite ! pts_app ; iFrame|iNext ; iIntros Hps ; iDestruct pts_app with Hps as [Hlv Hc₈] ; gen_env

iApply IH $! _ i + 1 mkPtrbase Objbase i :: xs with [%] [Hlv Hax Hc₀ Hc₈ Hl]

{split ; eassumption |

split ; lia |

split ; eassumption

{cbn [ lst ]

iExists base, h

iSplitR ; iPureIntro ; split ; reflexivity | ; lia |

iFrame Hl

rewrite / node_ps ! pts_app

iFrame

–wp_emp

iApply sum_spec with Hl

iIntros y fuel′

cbn [ fr_fn fr_env fr_locals fr_doomed fr_at ]

gen_env

iApply wpc_done_ emp%I _ _ _ Ret_ with [//] ; intros | let m ≔ fresh "m" in let s ≔ fresh "s" in iIntros m s _ _ ; iPureIntro ; compute_eq

listsum called with the int n is safe, with any fuel.

443Lemma listsum_spec

∀ n fuel

⊢ wpclge EConfmkFramels_fn"listsum" TAtom"v0", WIntn [ ] None EnterTAtom"start" None [ ] fuel

Explore proof 12 tactics

Initial goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

⊢

⊢ wpclge EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ TAtom"v0", WIntn; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"start" None [ ] fuel

iStartProof

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

∗

wpclge EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ TAtom"v0", WIntn; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"start" None [ ] fuel

wp_fuel

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

∗

wpclge EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ TAtom"v0", WIntn; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"start" None [ ] fuel

wp_emp

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ TAtom"v0", WIntn; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"start" [ ] JGotoToTAtom"L4" [ ] fuel − 1

wp_emp

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ TAtom"v0", WIntn; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"L4" SomeTAtom"start" [ ] fuel − 1

wp_fuel

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ TAtom"v0", WIntn; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"L4" SomeTAtom"start" [ ] fuel − 1

wp_emp

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

∗

wpclge IM.EConffr_fn ≔ ls_fn"listsum"; fr_env ≔ putTAtom"pr.1" WPtrptr_addr ≔ 0; ptr_cap ≔ CNone putTAtom"pr.2" WInt0 TAtom"v0", WIntn; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"L4" LetTAtom"v10" W CmpSlt W TmpTAtom"pr.2"; TmpTAtom"v0" JBranchTmpTAtom"v10" ToTAtom"L5" ToTAtom"L7" [ ] fuel − 1 − 1

iApply ls_loopn $! _ _ _ [ ] with [%] []

4 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

⊢

lookupTAtom"pr.2" putTAtom"pr.1" WPtrptr_addr ≔ 0; ptr_cap ≔ CNone putTAtom"pr.2" WInt0 TAtom"v0", WIntn = SomeWInt?z ∧ 0 ≤ ?z < 2 ^ 31 ∧ lookupTAtom"pr.1" putTAtom"pr.1" WPtrptr_addr ≔ 0; ptr_cap ≔ CNone putTAtom"pr.2" WInt0 TAtom"v0", WIntn = SomeWPtr?p ∧ lookupTAtom"v0" putTAtom"pr.1" WPtrptr_addr ≔ 0; ptr_cap ≔ CNone putTAtom"pr.2" WInt0 TAtom"v0", WIntn = SomeWIntn

focused goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

∗

lst?p [ ]

shelved goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

⊢

shelved goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

⊢

–split ; reflexivity |

3 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

⊢

0 ≤ 0 < 2 ^ 31 ∧ lookupTAtom"pr.1" putTAtom"pr.1" WPtrptr_addr ≔ 0; ptr_cap ≔ CNone putTAtom"pr.2" WInt0 TAtom"v0", WIntn = SomeWPtr?p ∧ lookupTAtom"v0" putTAtom"pr.1" WPtrptr_addr ≔ 0; ptr_cap ≔ CNone putTAtom"pr.2" WInt0 TAtom"v0", WIntn = SomeWIntn

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

∗

lst?p [ ]

shelved goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

⊢

split ; lia |

3 open

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

⊢

lookupTAtom"pr.1" putTAtom"pr.1" WPtrptr_addr ≔ 0; ptr_cap ≔ CNone putTAtom"pr.2" WInt0 TAtom"v0", WIntn = SomeWPtr?p ∧ lookupTAtom"v0" putTAtom"pr.1" WPtrptr_addr ≔ 0; ptr_cap ≔ CNone putTAtom"pr.2" WInt0 TAtom"v0", WIntn = SomeWIntn

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

∗

lst?p [ ]

shelved goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

⊢

split ; reflexivity

deferred goal

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

∗

lstptr_addr ≔ 0; ptr_cap ≔ CNone [ ]

–cbn [ lst ]

hlc :

has_lc

Σ :

gFunctors

HinvG :

invGS_genhlc Σ

HheapG :

gen_heapGSpiece pval Σ

n, fuel :

Hz :

fuel ≠ 0

Hz₀ :

fuel − 1 ≠ 0

∗

⌜ptr_addr ≔ 0; ptr_cap ≔ CNone = null⌝

done

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

iStartProof

iApply ls_loopn $! _ _ _ [ ] with [%] []

–split ; reflexivity |

split ; lia |

split ; reflexivity

–cbn [ lst ]

done

The resources the proof uses: invariants and the ghost heap.

457Definition lsΣ: gFunctors ≔

#invΣ; gen_heapΣpiece pval

lsΣ has invariants.

460Instance lsΣ_inv: invGpreSlsΣ

Explore proof 2 tactics

Initial goal

⊢

invGpreSlsΣ

apply subG_invΣ

⊢

subGinvΣ lsΣ

apply _

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

apply subG_invΣ

apply _

lsΣ has the ghost heap of pieces.

464Instance lsΣ_heap: gen_heapGpreSpiece pval lsΣ

Explore proof 2 tactics

Initial goal

⊢

gen_heapGpreSpiece pval lsΣ

apply subG_gen_heapGpreS

⊢

subGgen_heapΣpiece pval lsΣ

apply _

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

apply subG_gen_heapGpreS

apply _

listsum never panics: for every input whose first word is an int, with any fuel, no state of its run fails, whatever bases its nodes get. Proved by Iris adequacy (heap_never_panics) from listsum_spec.

471Theorem listsum_never_panics

P.never_panicsls_module TAtom"listsum" λxs ⇒ ∃n rest, xs = WIntn :: rest

Explore proof 11 tactics

Initial goal

⊢

P.never_panicsls_module TAtom"listsum" λxs : listword ⇒ ∃n : Z rest : listword, xs = WIntn :: rest

apply heap_never_panicslsΣ ls_module TAtom"listsum" _ ls_globals ls_mem ls_fn"listsum"

4 open

⊢

initial_memoryls_module = Somels_globals, ls_mem

focused goal

⊢

find_fnlge TAtom"listsum" = SomeDefinedls_fn"listsum"

focused goal

⊢

live_disjointls_mem

focused goal

⊢

∀xs : listword, ∃n : Z rest : listword, xs = WIntn :: rest → ∃fr : frame, call_framels_fn"listsum" xs = Somefr ∧ ∀fuel : Z HinvG : invGS_genHasNoLc lsΣ HheapG : gen_heapGSpiece pval lsΣ, ⊢ wpclge IM.EConffr [ ] fuel

–exact ls_initial

3 open

deferred goal

⊢

find_fnlge TAtom"listsum" = SomeDefinedls_fn"listsum"

deferred goal

⊢

live_disjointls_mem

deferred goal

⊢

–exact ls_find_listsumR.free

2 open

deferred goal

⊢

live_disjointls_mem

deferred goal

⊢

–intros b₁ r₁ b₂ r₂ E _

2 open

b₁ :

r₁ :

b₂ :

r₂ :

E :

object_regionb₁ m_regionsls_mem = Somer₁

⊢

live_atls_mem b₂ r₂ → b₁ ≠ b₂ → r_endr₁ ≤ b₂ ∨ r_endr₂ ≤ b₁

deferred goal

⊢

vm_compute in E

2 open

b₁ :

r₁ :

b₂ :

r₂ :

E :

None = Somer₁

⊢

live_atls_mem b₂ r₂ → b₁ ≠ b₂ → r_endr₁ ≤ b₂ ∨ r_endr₂ ≤ b₁

deferred goal

⊢

discriminate E

deferred goal

⊢

–intros xs n & rest & →

n :

rest :

listword

⊢

∃fr : frame, call_framels_fn"listsum" WIntn :: rest = Somefr ∧ ∀fuel : Z HinvG : invGS_genHasNoLc lsΣ HheapG : gen_heapGSpiece pval lsΣ, ⊢ wpclge IM.EConffr [ ] fuel

eexists

2 open

n :

rest :

listword

⊢

call_framels_fn"listsum" WIntn :: rest = Some?fr ∧ ∀fuel : Z HinvG : invGS_genHasNoLc lsΣ HheapG : gen_heapGSpiece pval lsΣ, ⊢ wpclge IM.EConf?fr [ ] fuel

shelved goal

n :

rest :

listword

⊢