Filnix wiki

cs₁, cs₂ :

listcap

IH :
  ∀ o : Z,
    aux_ps b o (cs1 ++ cs2)
    ≡ₚ aux_ps b o cs1 ++ aux_ps b (o + length cs1) cs2

o :

⊢

aux_ps b o ((c :: cs1) ++ cs2)
≡ₚ aux_ps b o (c :: cs1) ++ aux_ps b (o + length (c :: cs1)) cs2

–cbn

2 open

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

b :

cs₂ :

listcap

o :

⊢

aux_ps b o cs2 ≡ₚ aux_ps b o [] ++ aux_ps b (o + 0%nat) cs2

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

b :

c :

cs₁, cs₂ :

listcap

IH :
  ∀ o : Z,
    aux_ps b o (cs1 ++ cs2)
    ≡ₚ aux_ps b o cs1 ++ aux_ps b (o + length cs1) cs2

o :

⊢

aux_ps b o ((c :: cs1) ++ cs2)
≡ₚ aux_ps b o (c :: cs1) ++ aux_ps b (o + length (c :: cs1)) cs2

rewrite Z.add_0_r

2 open

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

b :

cs₂ :

listcap

o :

⊢

aux_ps b o cs2 ≡ₚ aux_ps b o [] ++ aux_ps b o cs2

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

b :

c :

cs₁, cs₂ :

listcap

IH :
  ∀ o : Z,
    aux_ps b o (cs1 ++ cs2)
    ≡ₚ aux_ps b o cs1 ++ aux_ps b (o + length cs1) cs2

o :

⊢

aux_ps b o ((c :: cs1) ++ cs2)
≡ₚ aux_ps b o (c :: cs1) ++ aux_ps b (o + length (c :: cs1)) cs2

reflexivity

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

b :

c :

cs₁, cs₂ :

listcap

IH :
  ∀ o : Z,
    aux_ps b o (cs1 ++ cs2)
    ≡ₚ aux_ps b o cs1 ++ aux_ps b (o + length cs1) cs2

o :

⊢

aux_ps b o ((c :: cs1) ++ cs2)
≡ₚ aux_ps b o (c :: cs1) ++ aux_ps b (o + length (c :: cs1)) cs2

–cbn [ app ]

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

b :

c :

cs₁, cs₂ :

listcap

IH :
  ∀ o : Z,
    aux_ps b o (cs1 ++ cs2)
    ≡ₚ aux_ps b o cs1 ++ aux_ps b (o + length cs1) cs2

o :

⊢

aux_ps b o (c :: cs1 ++ cs2)
≡ₚ aux_ps b o (c :: cs1) ++ aux_ps b (o + length (c :: cs1)) cs2

rewrite ! aux_ps_cons IH

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

b :

c :

cs₁, cs₂ :

listcap

IH :
  ∀ o : Z,
    aux_ps b o (cs1 ++ cs2)
    ≡ₚ aux_ps b o cs1 ++ aux_ps b (o + length cs1) cs2

o :

⊢

(PAux b o, VAux c)
:: aux_ps b (o + 1) cs1 ++ aux_ps b (o + 1 + length cs1) cs2
≡ₚ ((PAux b o, VAux c) :: aux_ps b (o + 1) cs1) ++
   aux_ps b (o + length (c :: cs1)) cs2

cbn [ app length ]

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

b :

c :

cs₁, cs₂ :

listcap

IH :
  ∀ o : Z,
    aux_ps b o (cs1 ++ cs2)
    ≡ₚ aux_ps b o cs1 ++ aux_ps b (o + length cs1) cs2

o :

⊢

(PAux b o, VAux c)
:: aux_ps b (o + 1) cs1 ++ aux_ps b (o + 1 + length cs1) cs2
≡ₚ (PAux b o, VAux c)
   :: aux_ps b (o + 1) cs1 ++ aux_ps b (o + S (length cs1)) cs2

replace o + Z.of_natSlengthcs₁ with o + 1 + Z.of_natlengthcs₁ by lia

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

b :

c :

cs₁, cs₂ :

listcap

IH :
  ∀ o : Z,
    aux_ps b o (cs1 ++ cs2)
    ≡ₚ aux_ps b o cs1 ++ aux_ps b (o + length cs1) cs2

o :

⊢

(PAux b o, VAux c)
:: aux_ps b (o + 1) cs1 ++ aux_ps b (o + 1 + length cs1) cs2
≡ₚ (PAux b o, VAux c)
   :: aux_ps b (o + 1) cs1 ++ aux_ps b (o + 1 + length cs1) cs2

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

rewrite / auxes / pts - big_sepL_app

f_equiv

revert o

induction cs₁ as | c cs₁ IH ; intros o

–cbn

rewrite Z.add_0_r

reflexivity

–cbn [ app ]

rewrite ! aux_ps_cons IH

cbn [ app length ]

replace o + Z.of_natSlengthcs₁ with o + 1 + Z.of_natlengthcs₁ by lia

reflexivity

The bytes xs lend their i-th, x, and take it back.

252Lemma bytes_byte

∀ b o xs i x

xs !! i = Somex

bytesb o xs −∗ ibyteb o + Z.of_nati x ∗ ibyteb o + Z.of_nati x −∗ bytesb o xs

Explore proof 7 tactics

Initial goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

b, o :

xs :

listZ

i :

nat

x :

⊢

xs !! i = Somex → bytesb o xs −∗ ibyteb o + i x ∗ ibyteb o + i x −∗ bytesb o xs

intros Hx

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

b, o :

xs :

listZ

i :

nat

x :

Hx :

xs !! i = Somex

⊢

bytesb o xs −∗ ibyteb o + i x ∗ ibyteb o + i x −∗ bytesb o xs

rewrite / bytes / ibyte / pts big_sepL_singleton

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

b, o :

xs :

listZ

i :

nat

x :

Hx :

xs !! i = Somex

⊢

∗_{lv∈byte_psb o xs}pointstolv.1 DfracOwn1 lv.2 −∗ pointstoPByteb o + i, VBytex.1 DfracOwn1 PByteb o + i, VBytex.2 ∗ pointstoPByteb o + i, VBytex.1 DfracOwn1 PByteb o + i, VBytex.2 −∗ ∗_{lv∈byte_psb o xs}pointstolv.1 DfracOwn1 lv.2

iIntros Hs

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

b, o :

xs :

listZ

i :

nat

x :

Hx :

xs !! i = Somex

Hs :

∗_{lv∈byte_psb o xs}pointstolv.1 DfracOwn1 lv.2

∗

pointstoPByteb o + i, VBytex.1 DfracOwn1 PByteb o + i, VBytex.2 ∗ pointstoPByteb o + i, VBytex.1 DfracOwn1 PByteb o + i, VBytex.2 −∗ ∗_{lv∈byte_psb o xs}pointstolv.1 DfracOwn1 lv.2

iDestruct big_sepL_lookup_acc with Hs as [Hb Hk] ; exact byte_ps_lookup_ _ _ _ _ Hx |

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

b, o :

xs :

listZ

i :

nat

x :

Hx :

xs !! i = Somex

Hb :

pointstoPByteb o + i, VBytex.1 DfracOwn1 PByteb o + i, VBytex.2

Hk :

pointstoPByteb o + i, VBytex.1 DfracOwn1 PByteb o + i, VBytex.2 −∗ ∗_{y∈byte_psb o xs}pointstoy.1 DfracOwn1 y.2

∗

pointstoPByteb o + i, VBytex.1 DfracOwn1 PByteb o + i, VBytex.2 ∗ pointstoPByteb o + i, VBytex.1 DfracOwn1 PByteb o + i, VBytex.2 −∗ ∗_{lv∈byte_psb o xs}pointstolv.1 DfracOwn1 lv.2

iSplitL Hb ; iExact Hb |

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

b, o :

xs :

listZ

i :

nat

x :

Hx :

xs !! i = Somex

Hk :

pointstoPByteb o + i, VBytex.1 DfracOwn1 PByteb o + i, VBytex.2 −∗ ∗_{y∈byte_psb o xs}pointstoy.1 DfracOwn1 y.2

∗

pointstoPByteb o + i, VBytex.1 DfracOwn1 PByteb o + i, VBytex.2 −∗ ∗_{lv∈byte_psb o xs}pointstolv.1 DfracOwn1 lv.2

iIntros Hb

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

b, o :

xs :

listZ

i :

nat

x :

Hx :

xs !! i = Somex

Hk :

pointstoPByteb o + i, VBytex.1 DfracOwn1 PByteb o + i, VBytex.2 −∗ ∗_{y∈byte_psb o xs}pointstoy.1 DfracOwn1 y.2

Hb :

pointstoPByteb o + i, VBytex.1 DfracOwn1 PByteb o + i, VBytex.2

∗

∗_{lv∈byte_psb o xs}pointstolv.1 DfracOwn1 lv.2

iApply Hk with Hb

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros Hx

rewrite / bytes / ibyte / pts big_sepL_singleton

iIntros Hs

iDestruct big_sepL_lookup_acc with Hs as [Hb Hk] ; exact byte_ps_lookup_ _ _ _ _ Hx |

iSplitL Hb ; iExact Hb |

iIntros Hb

iApply Hk with Hb

The buffer

The buffer lends the life of the object its pointer's capability names, if any (live_cap), and takes it back; its pointer's address is in range.

266Lemma buffer_cap

∀ p sz

bufferp sz −∗ ∃reg′, ⌜0 ≤ ptr_addrp < 2 ^ 64⌝ ∗ live_capptr_capp reg′ ∗ live_capptr_capp reg′ −∗ bufferp sz

Explore proof 17 tactics

Initial goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

sz :

⊢

bufferp sz −∗ ∃reg′ : region, ⌜0 ≤ ptr_addrp < 2 ^ 64⌝ ∗ live_capptr_capp reg′ ∗ live_capptr_capp reg′ −∗ bufferp sz

iIntros [[%Hp %Hz] | (%b & %reg & %xs & %cs & %Hf & Hl & Hx & Hcs)]

2 open

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

sz :

Hp :

p = null

Hz :

sz = 0

∗

∃reg′ : region, ⌜0 ≤ ptr_addrp < 2 ^ 64⌝ ∗ live_capptr_capp reg′ ∗ live_capptr_capp reg′ −∗ bufferp sz

focused goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

sz, b :

reg :

xs :

listZ

cs :

listcap

Hf :

p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b mod 16 = 0 ∧ r_kindreg = Heap ∧ 0 < sz ≤ lengthxs ∧ lengthcs = lengthxs ∧ b + lengthxs ≤ r_endreg ≤ 2 ^ 48

Hl :

liveb reg

Hx :

bytesb 0 xs

Hcs :

auxesb 0 cs

∗

∃reg′ : region, ⌜0 ≤ ptr_addrp < 2 ^ 64⌝ ∗ live_capptr_capp reg′ ∗ live_capptr_capp reg′ −∗ bufferp sz

–iExists slot_reg

2 open

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

sz :

Hp :

p = null

Hz :

sz = 0

∗

⌜0 ≤ ptr_addrp < 2 ^ 64⌝ ∗ live_capptr_capp slot_reg ∗ live_capptr_capp slot_reg −∗ bufferp sz

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

sz, b :

reg :

xs :

listZ

cs :

listcap

Hf :

p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b mod 16 = 0 ∧ r_kindreg = Heap ∧ 0 < sz ≤ lengthxs ∧ lengthcs = lengthxs ∧ b + lengthxs ≤ r_endreg ≤ 2 ^ 48

Hl :

liveb reg

Hx :

bytesb 0 xs

Hcs :

auxesb 0 cs

∗

∃reg′ : region, ⌜0 ≤ ptr_addrp < 2 ^ 64⌝ ∗ live_capptr_capp reg′ ∗ live_capptr_capp reg′ −∗ bufferp sz

subst p

2 open

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

sz :

Hz :

sz = 0

∗

⌜0 ≤ ptr_addrnull < 2 ^ 64⌝ ∗ live_capptr_capnull slot_reg ∗ live_capptr_capnull slot_reg −∗ buffernull sz

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

sz, b :

reg :

xs :

listZ

cs :

listcap

Hf :

p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b mod 16 = 0 ∧ r_kindreg = Heap ∧ 0 < sz ≤ lengthxs ∧ lengthcs = lengthxs ∧ b + lengthxs ≤ r_endreg ≤ 2 ^ 48

Hl :

liveb reg

Hx :

bytesb 0 xs

Hcs :

auxesb 0 cs

∗

∃reg′ : region, ⌜0 ≤ ptr_addrp < 2 ^ 64⌝ ∗ live_capptr_capp reg′ ∗ live_capptr_capp reg′ −∗ bufferp sz

iSplit ; iPureIntro ; cbn ; lia |

2 open

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

sz :

Hz :

sz = 0

∗

live_capptr_capnull slot_reg ∗ live_capptr_capnull slot_reg −∗ buffernull sz

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

sz, b :

reg :

xs :

listZ

cs :

listcap

Hf :

p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b mod 16 = 0 ∧ r_kindreg = Heap ∧ 0 < sz ≤ lengthxs ∧ lengthcs = lengthxs ∧ b + lengthxs ≤ r_endreg ≤ 2 ^ 48

Hl :

liveb reg

Hx :

bytesb 0 xs

Hcs :

auxesb 0 cs

∗

∃reg′ : region, ⌜0 ≤ ptr_addrp < 2 ^ 64⌝ ∗ live_capptr_capp reg′ ∗ live_capptr_capp reg′ −∗ bufferp sz

iSplit ; done |

2 open

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

sz :

Hz :

sz = 0

∗

live_capptr_capnull slot_reg −∗ buffernull sz

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

sz, b :

reg :

xs :

listZ

cs :

listcap

Hf :

p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b mod 16 = 0 ∧ r_kindreg = Heap ∧ 0 < sz ≤ lengthxs ∧ lengthcs = lengthxs ∧ b + lengthxs ≤ r_endreg ≤ 2 ^ 48

Hl :

liveb reg

Hx :

bytesb 0 xs

Hcs :

auxesb 0 cs

∗

∃reg′ : region, ⌜0 ≤ ptr_addrp < 2 ^ 64⌝ ∗ live_capptr_capp reg′ ∗ live_capptr_capp reg′ −∗ bufferp sz

iIntros _

2 open

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

sz :

Hz :

sz = 0

∗

buffernull sz

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

sz, b :

reg :

xs :

listZ

cs :

listcap

Hf :

p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b mod 16 = 0 ∧ r_kindreg = Heap ∧ 0 < sz ≤ lengthxs ∧ lengthcs = lengthxs ∧ b + lengthxs ≤ r_endreg ≤ 2 ^ 48

Hl :

liveb reg

Hx :

bytesb 0 xs

Hcs :

auxesb 0 cs

∗

∃reg′ : region, ⌜0 ≤ ptr_addrp < 2 ^ 64⌝ ∗ live_capptr_capp reg′ ∗ live_capptr_capp reg′ −∗ bufferp sz

iLeft

2 open

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

sz :

Hz :

sz = 0

∗

⌜null = null ∧ sz = 0⌝

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

sz, b :

reg :

xs :

listZ

cs :

listcap

Hf :

p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b mod 16 = 0 ∧ r_kindreg = Heap ∧ 0 < sz ≤ lengthxs ∧ lengthcs = lengthxs ∧ b + lengthxs ≤ r_endreg ≤ 2 ^ 48

Hl :

liveb reg

Hx :

bytesb 0 xs

Hcs :

auxesb 0 cs

∗

∃reg′ : region, ⌜0 ≤ ptr_addrp < 2 ^ 64⌝ ∗ live_capptr_capp reg′ ∗ live_capptr_capp reg′ −∗ bufferp sz

done

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

sz, b :

reg :

xs :

listZ

cs :

listcap

Hf :

p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b mod 16 = 0 ∧ r_kindreg = Heap ∧ 0 < sz ≤ lengthxs ∧ lengthcs = lengthxs ∧ b + lengthxs ≤ r_endreg ≤ 2 ^ 48

Hl :

liveb reg

Hx :

bytesb 0 xs

Hcs :

auxesb 0 cs

∗

∃reg′ : region, ⌜0 ≤ ptr_addrp < 2 ^ 64⌝ ∗ live_capptr_capp reg′ ∗ live_capptr_capp reg′ −∗ bufferp sz

–pose proof Hf as Hpe & Hb & _ & _ & _ & _ & Hend & Hend₄₈

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

p :

sz, b :

reg :

xs :

listZ

cs :

listcap

Hf :

p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b mod 16 = 0 ∧ r_kindreg = Heap ∧ 0 < sz ≤ lengthxs ∧ lengthcs = lengthxs ∧ b + lengthxs ≤ r_endreg ≤ 2 ^ 48

Hpe :

p = ptr_addr ≔ b; ptr_cap ≔ Objb

Hb :

0 < b

Hend :

b + lengthxs ≤ r_endreg

Hend₄₈ :

r_endreg ≤ 2 ^ 48

Hl :

liveb reg

Hx :

bytesb 0 xs

Hcs :

auxesb 0 cs

∗

∃reg′ : region, ⌜0 ≤ ptr_addrp < 2 ^ 64⌝ ∗ live_capptr_capp reg′ ∗ live_capptr_capp reg′ −∗ bufferp sz

subst p

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

sz, b :

reg :

xs :

listZ

cs :

listcap

Hf :

ptr_addr ≔ b; ptr_cap ≔ Objb = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b mod 16 = 0 ∧ r_kindreg = Heap ∧ 0 < sz ≤ lengthxs ∧ lengthcs = lengthxs ∧ b + lengthxs ≤ r_endreg ≤ 2 ^ 48

Hb :

0 < b

Hend :

b + lengthxs ≤ r_endreg

Hend₄₈ :

r_endreg ≤ 2 ^ 48

Hl :

liveb reg

Hx :

bytesb 0 xs

Hcs :

auxesb 0 cs

∗

∃reg′ : region, ⌜0 ≤ ptr_addrptr_addr ≔ b; ptr_cap ≔ Objb < 2 ^ 64⌝ ∗ live_capptr_capptr_addr ≔ b; ptr_cap ≔ Objb reg′ ∗ live_capptr_capptr_addr ≔ b; ptr_cap ≔ Objb reg′ −∗ bufferptr_addr ≔ b; ptr_cap ≔ Objb sz

iExists reg

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

sz, b :

reg :

xs :

listZ

cs :

listcap

Hf :

Hb :

0 < b

Hend :

b + lengthxs ≤ r_endreg

Hend₄₈ :

r_endreg ≤ 2 ^ 48

Hl :

liveb reg

Hx :

bytesb 0 xs

Hcs :

auxesb 0 cs

∗

⌜0 ≤ ptr_addrptr_addr ≔ b; ptr_cap ≔ Objb < 2 ^ 64⌝ ∗ live_capptr_capptr_addr ≔ b; ptr_cap ≔ Objb reg ∗ live_capptr_capptr_addr ≔ b; ptr_cap ≔ Objb reg −∗ bufferptr_addr ≔ b; ptr_cap ≔ Objb sz

iSplit ; iPureIntro ; cbn ; lia |

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

sz, b :

reg :

xs :

listZ

cs :

listcap

Hf :

Hb :

0 < b

Hend :

b + lengthxs ≤ r_endreg

Hend₄₈ :

r_endreg ≤ 2 ^ 48

Hl :

liveb reg

Hx :

bytesb 0 xs

Hcs :

auxesb 0 cs

∗

live_capptr_capptr_addr ≔ b; ptr_cap ≔ Objb reg ∗ live_capptr_capptr_addr ≔ b; ptr_cap ≔ Objb reg −∗ bufferptr_addr ≔ b; ptr_cap ≔ Objb sz

iFrame Hl

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

sz, b :

reg :

xs :

listZ

cs :

listcap

Hf :

Hb :

0 < b

Hend :

b + lengthxs ≤ r_endreg

Hend₄₈ :

r_endreg ≤ 2 ^ 48

Hx :

bytesb 0 xs

Hcs :

auxesb 0 cs

∗

live_capptr_capptr_addr ≔ b; ptr_cap ≔ Objb reg −∗ bufferptr_addr ≔ b; ptr_cap ≔ Objb sz

iIntros Hl

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

sz, b :

reg :

xs :

listZ

cs :

listcap

Hf :

Hb :

0 < b

Hend :

b + lengthxs ≤ r_endreg

Hend₄₈ :

r_endreg ≤ 2 ^ 48

Hx :

bytesb 0 xs

Hcs :

auxesb 0 cs

Hl :

live_capptr_capptr_addr ≔ b; ptr_cap ≔ Objb reg

∗

bufferptr_addr ≔ b; ptr_cap ≔ Objb sz

iRight

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

sz, b :

reg :

xs :

listZ

cs :

listcap

Hf :

Hb :

0 < b

Hend :

b + lengthxs ≤ r_endreg

Hend₄₈ :

r_endreg ≤ 2 ^ 48

Hx :

bytesb 0 xs

Hcs :

auxesb 0 cs

Hl :

live_capptr_capptr_addr ≔ b; ptr_cap ≔ Objb reg

∗

∃b₀ : Z reg₀ : region xs₀ : listZ cs₀ : listcap, ⌜ptr_addr ≔ b; ptr_cap ≔ Objb = ptr_addr ≔ b₀; ptr_cap ≔ Objb₀ ∧ 0 < b₀ ∧ b₀ mod 16 = 0 ∧ r_kindreg₀ = Heap ∧ 0 < sz ≤ lengthxs₀ ∧ lengthcs₀ = lengthxs₀ ∧ b₀ + lengthxs₀ ≤ r_endreg₀ ≤ 2 ^ 48⌝ ∗ liveb₀ reg₀ ∗ bytesb₀ 0 xs₀ ∗ auxesb₀ 0 cs₀

iExists b, reg, xs, cs

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

sz, b :

reg :

xs :

listZ

cs :

listcap

Hf :

Hb :

0 < b

Hend :

b + lengthxs ≤ r_endreg

Hend₄₈ :

r_endreg ≤ 2 ^ 48

Hx :

bytesb 0 xs

Hcs :

auxesb 0 cs

Hl :

live_capptr_capptr_addr ≔ b; ptr_cap ≔ Objb reg

∗

⌜ptr_addr ≔ b; ptr_cap ≔ Objb = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b mod 16 = 0 ∧ r_kindreg = Heap ∧ 0 < sz ≤ lengthxs ∧ lengthcs = lengthxs ∧ b + lengthxs ≤ r_endreg ≤ 2 ^ 48⌝ ∗ liveb reg ∗ bytesb 0 xs ∗ auxesb 0 cs

by iFrame

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

iIntros [[%Hp %Hz] | (%b & %reg & %xs & %cs & %Hf & Hl & Hx & Hcs)]

–iExists slot_reg

subst p

iSplit ; iPureIntro ; cbn ; lia |

iSplit ; done |

iIntros _

iLeft

done

–pose proof Hf as Hpe & Hb & _ & _ & _ & _ & Hend & Hend₄₈

subst p

iExists reg

iSplit ; iPureIntro ; cbn ; lia |

iFrame Hl

iIntros Hl

iRight

iExists b, reg, xs, cs

by iFrame

A call of free on the buffer's pointer, which v reads as, frees it if it is not null, and gives up the whole buffer.

278Lemma wp_free_buffer

∀ f e ls l v rest j p sz Φ

arg_xslot_ge e ArgP v = SomeWPtrp

bufferp sz −∗ ▷WPERunmkFramef e ls None Execl rest j : sexpr {Φ} −∗ WPERunmkFramef e ls None Execl CallCVoid Globalfree_name ArgP v :: rest j : sexpr {Φ}

Explore proof 6 tactics

Initial goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

f :

e :

ls :

listname × optionZ

l :

v :

rest :

listinst

j :

p :

sz :

Φ :

valnanofil_langslot_registry slot_ge → iPropIΣ

⊢

arg_xslot_ge e ArgP v = SomeWPtrp → bufferp sz −∗ ▷WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j : sexpr {v. Φv} −∗ WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j : sexpr {v. Φv}

intros Hv

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

f :

e :

ls :

listname × optionZ

l :

v :

rest :

listinst

j :

p :

sz :

Φ :

valnanofil_langslot_registry slot_ge → iPropIΣ

Hv :

arg_xslot_ge e ArgP v = SomeWPtrp

⊢

bufferp sz −∗ ▷WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j : sexpr {v. Φv} −∗ WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j : sexpr {v. Φv}

iIntros [[%Hp _] | (%b & %reg & %xs & %cs & %Hf & Hl & _ & _)] HK

2 open

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

f :

e :

ls :

listname × optionZ

l :

v :

rest :

listinst

j :

p :

sz :

Φ :

valnanofil_langslot_registry slot_ge → iPropIΣ

Hv :

arg_xslot_ge e ArgP v = SomeWPtrp

Hp :

p = null

HK :

▷WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

∗

WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j {v. Φv}

focused goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

f :

e :

ls :

listname × optionZ

l :

v :

rest :

listinst

j :

p :

sz :

Φ :

valnanofil_langslot_registry slot_ge → iPropIΣ

Hv :

arg_xslot_ge e ArgP v = SomeWPtrp

b :

reg :

xs :

listZ

cs :

listcap

Hf :

p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b mod 16 = 0 ∧ r_kindreg = Heap ∧ 0 < sz ≤ lengthxs ∧ lengthcs = lengthxs ∧ b + lengthxs ≤ r_endreg ≤ 2 ^ 48

Hl :

liveb reg

HK :

▷WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

∗

WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j {v. Φv}

–subst p

2 open

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

f :

e :

ls :

listname × optionZ

l :

v :

rest :

listinst

j :

sz :

Φ :

valnanofil_langslot_registry slot_ge → iPropIΣ

Hv :

arg_xslot_ge e ArgP v = SomeWPtrnull

HK :

▷WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

∗

WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j {v. Φv}

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

f :

e :

ls :

listname × optionZ

l :

v :

rest :

listinst

j :

p :

sz :

Φ :

valnanofil_langslot_registry slot_ge → iPropIΣ

Hv :

arg_xslot_ge e ArgP v = SomeWPtrp

b :

reg :

xs :

listZ

cs :

listcap

Hf :

p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b mod 16 = 0 ∧ r_kindreg = Heap ∧ 0 < sz ≤ lengthxs ∧ lengthcs = lengthxs ∧ b + lengthxs ≤ r_endreg ≤ 2 ^ 48

Hl :

liveb reg

HK :

▷WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

∗

WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j {v. Φv}

iApply wp_free_null with HK ; exact R.free_succeeds | reflexivity | reflexivity | exact Hv

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

f :

e :

ls :

listname × optionZ

l :

v :

rest :

listinst

j :

p :

sz :

Φ :

valnanofil_langslot_registry slot_ge → iPropIΣ

Hv :

arg_xslot_ge e ArgP v = SomeWPtrp

b :

reg :

xs :

listZ

cs :

listcap

Hf :

p = ptr_addr ≔ b; ptr_cap ≔ Objb ∧ 0 < b ∧ b mod 16 = 0 ∧ r_kindreg = Heap ∧ 0 < sz ≤ lengthxs ∧ lengthcs = lengthxs ∧ b + lengthxs ≤ r_endreg ≤ 2 ^ 48

Hl :

liveb reg

HK :

▷WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

∗

WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j {v. Φv}

–destruct Hf as → & Hb & _ & Hk & _

hlc :

has_lc

Σ :

gFunctors

invGS_gen₀ :

invGS_genhlc Σ

gen_heapGS₀ :

gen_heapGSpiece pval Σ

f :

e :

ls :

listname × optionZ

l :

v :

rest :

listinst

j :

sz :

Φ :

valnanofil_langslot_registry slot_ge → iPropIΣ

b :

Hv :

arg_xslot_ge e ArgP v = SomeWPtrptr_addr ≔ b; ptr_cap ≔ Objb

reg :

xs :

listZ

cs :

listcap

Hb :

0 < b

Hk :

r_kindreg = Heap

Hl :

liveb reg

HK :

▷WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

∗

WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j {v. Φv}

iApply wp_free with Hl HK ; exact R.free_succeeds | reflexivity | reflexivity | exact Hv | exact Hk | lia | intros ; exact I

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros Hv

iIntros [[%Hp _] | (%b & %reg & %xs & %cs & %Hf & Hl & _ & _)] HK

–subst p

iApply wp_free_null with HK ; exact R.free_succeeds | reflexivity | reflexivity | exact Hv

–destruct Hf as → & Hb & _ & Hk & _

`fill`

The fill, from L6's instructions: owning the static objects holding the buffer b and its size sz, more than n, and the buffer's bytes xs and slots cs: memset its first n bytes, terminate them, and return the buffer, lending the bytes.

297Lemma fill_L6

∀ e c n b reg xs cs sz Φ

lookupTAtom"v0" e = SomeWIntc

lookupTAtom"v2" e = SomeWIntn

0 ≤ c < 2 ^ 32

0 ≤ n < sz

sz < 2 ^ 48

0 < b

b mod 16 = 0

r_kindreg = Heap

sz ≤ Z.of_natlengthxs

lengthcs = lengthxs

b + Z.of_natlengthxs ≤ r_endreg

r_endreg ≤ 2 ^ 48

liveslot_b slot_reg −∗ livesize_b size_reg −∗ pcellslot_b 0 mkPtrb Objb −∗ icellsize_b 0 sz −∗ liveb reg −∗ bytesb 0 xs −∗ auxesb 0 cs −∗ ▷∀b reg, lentb reg n c −∗ ΦRetWPtrmkPtrb Objb −∗ WPERunmkFramefill_fn e [ ] None ExecTAtom"L6" b_instsf_L6 b_jumpf_L6 : sexpr {Φ}

Proof 87 steps Qed

intros Hc Hn Hc₃₂ Hnsz Hsz Hb₀ Hb₁₆ Hk Hxs Hcs Hend Hend₄₈

iIntros Hls Hlz Hp Hz Hl Hx Hcs HΦ

cbn [ b_insts b_jump f_L6 ]

Split the buffer at n: the n bytes memset fills, the terminator, the rest.

assert Hnx : Z.to_natn < lengthxs%nat by lia

destruct lookup_lt_is_Some_2xs _ Hnx as x Hx

rewrite <- take_drop_middlexs Z.to_natn x Hx

rewrite <- take_dropZ.to_natn cs

iDestruct bytes_split with Hx as (Hx & Hx₀ & Hxr)

iDestruct auxes_app with Hcs as [Hcs Hcr]

assert Ht : lengthtakeZ.to_natn xs = Z.to_natn by rewrite length_take ; lia

assert Htc : lengthtakeZ.to_natn cs = lengthtakeZ.to_natn xs by rewrite ! length_take ; lia

rewrite Ht

assert Hb₈ : b mod 8 = 0

{pose proof Z.div_modb 16 ltac:lia

pose proof Z.div_modb 8 ltac:lia

pose proof Z.mod_pos_boundb 8 ltac:lia

lia

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

iNext

iNext

iIntros Hls

iNext

iIntros Hls Hp Hl

iNext

iIntros Hl Hx Hcs

rewrite Z.add_0_r

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

iNext

iNext

iIntros Hls

iNext

iIntros Hls Hp Hl

iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ b + n ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |

iNext

iNext

iIntros Hl

iNext

iIntros Hl Hx₀

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

iNext

iNext

iIntros Hls

iNext

iIntros Hls Hp Hl

iApply wp_ret ; reflexivity | word_premise |

iNext

rewrite Ht

iApply HΦ $! b reg

iSplit ; iPureIntro ; lia |

iFrame Hl Hx

iIntros Hl Hx

iFrame Hls Hlz

iExists _, sz

iFrame Hp Hz

iSplit ; iPureIntro ; lia |

iRight

iExists b, reg, replicateZ.to_natn c mod 256 ++ 0 mod 256 :: dropSZ.to_natn xs, clear_slots0 takeZ.to_natn cs ++ dropZ.to_natn cs

rewrite bytes_split auxes_app length_replicate length_clear_slots Htc Ht

iFrame Hl Hx Hx₀ Hxr Hcs Hcr

iPureIntro

rewrite ! length_app

cbn [ length ]

rewrite ! length_replicate length_clear_slots ! length_drop ! length_take

split ; reflexivity |

repeat split ; first assumption | lia

fill's triple: with the module invariant, called with an int c and a size n below 2^47, it returns the buffer, lending its first n bytes, each c's low byte (lent). From the entry: load the size, and if it is at most n, free the old buffer (wp_free_buffer), malloc n + 1 bytes (wp_malloc) and store the new buffer and its size; then fill_L6.

371Lemma fill_spec

∀ c n Φ

0 ≤ c < 2 ^ 32

0 ≤ n < 2 ^ 47

slot_inv −∗ ▷∀b reg, lentb reg n c −∗ ΦRetWPtrmkPtrb Objb −∗ WPERunfill_entryc n : sexpr {Φ}

Proof 93 steps Qed

intros Hc Hn

iIntros (Hls & Hlz & %p & %sz & %Hsz & Hp & Hz & Hbuf) HΦ

unfold fill_entry

remember putTAtom"v2" WIntn putTAtom"v0" WIntc [ ] as e eqn: Ee

assert Hv₀ : lookupTAtom"v0" e = SomeWIntc by subst e ; reflexivity

assert Hv₂ : lookupTAtom"v2" e = SomeWIntn by subst e ; reflexivity

clear Ee

iApply wp_enter ; exact find_f_start | reflexivity |

iNext

cbn [ b_insts b_jump f_start ]

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

iNext

iNext

iIntros Hlz

iApply wp_raw_load with Hlz Hz ; reflexivity | word_premise | reflexivity | static_premise |

iNext

iIntros Hlz Hz

destruct Z.le_gt_casessz n as Hle | Hgt

Too small: free the buffer, malloc n + 1 bytes, and store them.

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

iNext

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

iNext

cbn [ Z.eqb edge_label ]

iApply wp_enter ; exact find_f_L4 | reflexivity |

iNext

cbn [ b_insts b_jump f_L4 ]

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

iNext

iNext

iIntros Hls

iDestruct buffer_cap with Hbuf as reg′ (%Hpa & Hcap & Hbuf)

iNext

iIntros Hls Hp Hcap

iDestruct Hbuf with Hcap as Hbuf

iApply wp_free_buffer with Hbuf ; word_premise |

iNext

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

iNext

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

iNext

iNext

iIntros base Hpos & Hmod & Hend & Hmax Hobj

iNext

iIntros Hls

iNext

iIntros Hls Hp

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

iNext

iNext

iIntros Hlz

iNext

iIntros Hlz Hz

iApply wp_goto

iNext

iApply wp_enter ; exact find_f_L6 | reflexivity |

iNext

pose proof malloc_extentn + 1 ltac:lia as Hext

rewrite / obj obj_block ; | lia

rewrite block_pts

iDestruct Hobj as (Hl & Hx & Hcs)

Big enough: the buffer is not null; fill it.

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

iNext

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

iNext

cbn [ Z.eqb edge_label ]

iApply wp_enter ; exact find_f_L6 | reflexivity |

iNext

iDestruct Hbuf as [[_ %Hz₀] | (%b & %reg & %xs & %cs & %Hf & Hl & Hx & Hcs)] ; lia |

destruct Hf as → & Hb & Hb₁₆ & Hk & Hszx & Hcx & Hend & Hend₄₈

use is safe and returns an int: it calls fill three times through fill_spec, each time reading a byte of the bytes lent (bytes_byte) and handing them back for the next call.

440Lemma use_spec

slot_inv −∗ WPERunuse_entry : sexpr {o. ⌜∃k, o = RetWIntk⌝}

Proof 69 steps Qed

iIntros Hinv

iApply wp_enter ; exact find_u_start | reflexivity |

iNext

cbn [ b_insts b_jump u_start ]

fill('a', 8), then a7.

iApply wp_call_bind ; reflexivity | exact find_fill | reflexivity |

iNext

iApply fill_spec97 8 with Hinv ; lia | lia |

iNext

iIntros b reg (%Hb & Hl & Hx & Hback)

iExists _

iSplit ; iPureIntro ; reflexivity |

iNext

cbn [ fr_fn fr_env fr_locals fr_doomed fr_at ]

iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ b + 7 ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |

iNext

iNext

iIntros Hl

iDestruct bytes_byte_ _ _ 7 with Hx as [Hb Hx] ; reflexivity |

iNext

iIntros Hl Hb

iDestruct Hx with Hb as Hx

iDestruct Hback with Hl Hx as Hinv

fill('b', 3), then b0.

iApply wp_call_bind ; reflexivity | exact find_fill | reflexivity |

iNext

iApply fill_spec98 3 with Hinv ; lia | lia |

iNext

iIntros b₂ reg₂ (%Hb₂ & Hl & Hx & Hback)

iExists _

iSplit ; iPureIntro ; reflexivity |

iNext

cbn [ fr_fn fr_env fr_locals fr_doomed fr_at ]

iNext

iIntros Hl

iDestruct bytes_byte_ _ _ 0 with Hx as [Hb Hx] ; reflexivity |

iNext

iIntros Hl Hb

iDestruct Hx with Hb as Hx

iDestruct Hback with Hl Hx as Hinv

fill('c', 16), then c15, and the sum.

iApply wp_call_bind ; reflexivity | exact find_fill | reflexivity |

iNext

iApply fill_spec99 16 with Hinv ; lia | lia |

iNext

iIntros b₃ reg₃ (%Hb₃ & Hl & Hx & _)

iExists _

iSplit ; iPureIntro ; reflexivity |

iNext

cbn [ fr_fn fr_env fr_locals fr_doomed fr_at ]

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

iNext

iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ b3 + 15 ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |

iNext

iNext

iIntros Hl

iDestruct bytes_byte_ _ _ 15 with Hx as [Hb _] ; reflexivity |

iNext

iIntros _ _

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

iNext

iApply wp_ret ; reflexivity | word_premise |

iNext

iPureIntro

eexists

reflexivity

use is safe: from a ready runtime, live objects apart, and a memory whose static objects hold null and 0, with any fuel, no labelled run stops with a failure_ending, and a run that returns returns an int. By heap_labelled_safe from use_spec, the ghost heap starting with slot_ps0.

481Theorem slot_logic_safe

∀ Σ HinvP : invGpreSΣ HheapP : gen_heapGpreSpiece pval Σ m s fuel

R.readys m

labelled_safeslot_registry slot_ge use_entry m s tt fuel λo ⇒ ∃k, o = RetWIntk

Explore proof 21 tactics

Initial goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

⊢

R.readys m → live_disjointm → all_agreem slot_ps0 → labelled_safeslot_registry slot_ge use_entry m s () fuel λo : outcome ⇒ ∃k : Z, o = RetWIntk

intros Hr Hd Ha

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

labelled_safeslot_registry slot_ge use_entry m s () fuel λo : outcome ⇒ ∃k : Z, o = RetWIntk

apply heap_labelled_safeΣ slot_registry no_world slot_ge use_entry m s tt list_to_mapslot_ps0

5 open

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

R.readys m

focused goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

focused goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

agreesm list_to_mapslot_ps0

focused goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

no_worldm () list_to_mapslot_ps0

focused goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapslot_ps0}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSslot_registry no_world slot_ge in

WPSlotLogic.LG.L.ERunuse_entry {o. ⌜∃k : Z, o = RetWIntk⌝}

–exact Hr

4 open

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

agreesm list_to_mapslot_ps0

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

no_worldm () list_to_mapslot_ps0

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapslot_ps0}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSslot_registry no_world slot_ge in

WPSlotLogic.LG.L.ERunuse_entry {o. ⌜∃k : Z, o = RetWIntk⌝}

–exact Hd

3 open

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

agreesm list_to_mapslot_ps0

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

no_worldm () list_to_mapslot_ps0

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapslot_ps0}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSslot_registry no_world slot_ge in

WPSlotLogic.LG.L.ERunuse_entry {o. ⌜∃k : Z, o = RetWIntk⌝}

–intros l v Hl

3 open

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

l :

v :

Hl :

list_to_mapslot_ps0 !! l = Somev

⊢

agree_piecem l v

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

no_worldm () list_to_mapslot_ps0

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapslot_ps0}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSslot_registry no_world slot_ge in

WPSlotLogic.LG.L.ERunuse_entry {o. ⌜∃k : Z, o = RetWIntk⌝}

exact all_agree_elem_ _ _ _ Ha elem_of_list_to_map_2_ _ _ Hl

2 open

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

no_worldm () list_to_mapslot_ps0

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapslot_ps0}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSslot_registry no_world slot_ge in

WPSlotLogic.LG.L.ERunuse_entry {o. ⌜∃k : Z, o = RetWIntk⌝}

–exact I

deferred goal

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

⊢

∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ ,

∗_{l↦v∈list_to_mapslot_ps0}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSslot_registry no_world slot_ge in

WPSlotLogic.LG.L.ERunuse_entry {o. ⌜∃k : Z, o = RetWIntk⌝}

–intros HinvG HheapG

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

⊢

∗_{l↦v∈list_to_mapslot_ps0}pointstol DfracOwn1 v

⊢

let H ≔ nanofil_irisGSslot_registry no_world slot_ge in

WPSlotLogic.LG.L.ERunuse_entry {o. ⌜∃k : Z, o = RetWIntk⌝}

rewrite big_sepM_list_to_map ; | exact slot_ps0_nodup

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

⊢

∗_{xk∈slot_ps0}pointstoxk.1 DfracOwn1 xk.2

⊢

let H ≔ nanofil_irisGSslot_registry no_world slot_ge in

WPSlotLogic.LG.L.ERunuse_entry {o. ⌜∃k : Z, o = RetWIntk⌝}

iIntros Hps

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

Hps :

∗_{xk∈slot_ps0}pointstoxk.1 DfracOwn1 xk.2

∗

WPSlotLogic.LG.L.ERunuse_entry {o. ⌜∃k : Z, o = RetWIntk⌝}

iApply use_spec

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

Hps :

∗_{xk∈slot_ps0}pointstoxk.1 DfracOwn1 xk.2

∗

slot_inv

rewrite / slot_ps0 / pts big_sepL_cons big_sepL_cons big_sepL_app

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

Hps :

pointstoPLiveslot_b, VLiveslot_reg.1 DfracOwn1 PLiveslot_b, VLiveslot_reg.2 ∗ pointstoPLivesize_b, VLivesize_reg.1 DfracOwn1 PLivesize_b, VLivesize_reg.2 ∗ ∗_{y∈PAuxslot_b 0, VAuxCNone :: cellslot_b 0 0}pointstoy.1 DfracOwn1 y.2 ∗ ∗_{y∈cellsize_b 0 0}pointstoy.1 DfracOwn1 y.2

∗

slot_inv

iDestruct Hps as (Hls & Hlz & Hp & Hz)

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

Hls :

pointstoPLiveslot_b, VLiveslot_reg.1 DfracOwn1 PLiveslot_b, VLiveslot_reg.2

Hlz :

pointstoPLivesize_b, VLivesize_reg.1 DfracOwn1 PLivesize_b, VLivesize_reg.2

Hp :

∗_{y∈PAuxslot_b 0, VAuxCNone :: cellslot_b 0 0}pointstoy.1 DfracOwn1 y.2

Hz :

∗_{y∈cellsize_b 0 0}pointstoy.1 DfracOwn1 y.2

∗

slot_inv

rewrite / slot_inv / live / pts ! big_sepL_singleton

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

Hls :

pointstoPLiveslot_b, VLiveslot_reg.1 DfracOwn1 PLiveslot_b, VLiveslot_reg.2

Hlz :

pointstoPLivesize_b, VLivesize_reg.1 DfracOwn1 PLivesize_b, VLivesize_reg.2

Hp :

∗_{y∈PAuxslot_b 0, VAuxCNone :: cellslot_b 0 0}pointstoy.1 DfracOwn1 y.2

Hz :

∗_{y∈cellsize_b 0 0}pointstoy.1 DfracOwn1 y.2

∗

pointstoPLiveslot_b, VLiveslot_reg.1 DfracOwn1 PLiveslot_b, VLiveslot_reg.2 ∗ pointstoPLivesize_b, VLivesize_reg.1 DfracOwn1 PLivesize_b, VLivesize_reg.2 ∗ ∃p : ptr sz : Z, ⌜0 ≤ sz < 2 ^ 48⌝ ∗ pcellslot_b 0 p ∗ icellsize_b 0 sz ∗ bufferp sz

iFrame Hls Hlz

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

Hp :

∗_{y∈PAuxslot_b 0, VAuxCNone :: cellslot_b 0 0}pointstoy.1 DfracOwn1 y.2

Hz :

∗_{y∈cellsize_b 0 0}pointstoy.1 DfracOwn1 y.2

∗

∃p : ptr sz : Z, ⌜0 ≤ sz < 2 ^ 48⌝ ∗ pcellslot_b 0 p ∗ icellsize_b 0 sz ∗ bufferp sz

iExists null, 0

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

Hp :

∗_{y∈PAuxslot_b 0, VAuxCNone :: cellslot_b 0 0}pointstoy.1 DfracOwn1 y.2

Hz :

∗_{y∈cellsize_b 0 0}pointstoy.1 DfracOwn1 y.2

∗

⌜0 ≤ 0 < 2 ^ 48⌝ ∗ pcellslot_b 0 null ∗ icellsize_b 0 0 ∗ buffernull 0

iSplit ; iPureIntro ; lia |

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

Hp :

∗_{y∈PAuxslot_b 0, VAuxCNone :: cellslot_b 0 0}pointstoy.1 DfracOwn1 y.2

Hz :

∗_{y∈cellsize_b 0 0}pointstoy.1 DfracOwn1 y.2

∗

pcellslot_b 0 null ∗ icellsize_b 0 0 ∗ buffernull 0

iSplitL Hp ; iExact Hp |

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

Hz :

∗_{y∈cellsize_b 0 0}pointstoy.1 DfracOwn1 y.2

∗

icellsize_b 0 0 ∗ buffernull 0

iSplitL Hz ; iExact Hz |

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

∗

buffernull 0

iLeft

Σ :

gFunctors

HinvP :

invGpreSΣ

HheapP :

gen_heapGpreSpiece pval Σ

m :

s :

R.state

fuel :

Hr :

R.readys m

Hd :

Ha :

InterpRuntime.readyInterpRuntime.start slot_memory

HinvG :

invGS_genHasNoLc Σ

HheapG :

gen_heapGSpiece pval Σ

∗

⌜null = null ∧ 0 = 0⌝

done

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros Hr Hd Ha

apply heap_labelled_safeΣ slot_registry no_world slot_ge use_entry m s tt list_to_mapslot_ps0

–exact Hr

–exact Hd

–intros l v Hl

exact all_agree_elem_ _ _ _ Ha elem_of_list_to_map_2_ _ _ Hl

–exact I

–intros HinvG HheapG

rewrite big_sepM_list_to_map ; | exact slot_ps0_nodup

iIntros Hps

iApply use_spec

rewrite / slot_ps0 / pts big_sepL_cons big_sepL_cons big_sepL_app

iDestruct Hps as (Hls & Hlz & Hp & Hz)

rewrite / slot_inv / live / pts ! big_sepL_singleton

iFrame Hls Hlz

iExists null, 0

iSplit ; iPureIntro ; lia |

iSplitL Hp ; iExact Hp |

iSplitL Hz ; iExact Hz |

iLeft

done

The interpreter's runtime

slot.c over the interpreter's runtime.

504Module InterpSlotLogic ≔ SlotLogic InterpRuntime

The module's initial memory: the two static objects, every byte 0 and every aux slot empty.

508Definition slot_memory: mem ≔

mkMemλ_ ⇒ 0 size_reg; slot_reg λ_ ⇒ CNone

Laying out the module gives slot_memory.

512Lemma slot_initial

initial_memoryslot_module = Someslot_globals, slot_memory

Explore proof 2 tactics

Initial goal

⊢

initial_memoryslot_module = Someslot_globals, slot_memory

vm_compute

⊢

SomeTAtom"slot_size", ptr_addr ≔ 65600; ptr_cap ≔ Obj65600; TAtom"slot", ptr_addr ≔ 65568; ptr_cap ≔ Obj65568; TAtom"use", ptr_addr ≔ 65552; ptr_cap ≔ FnTAtom"use"; TAtom"fill", ptr_addr ≔ 65536; ptr_cap ≔ FnTAtom"fill", m_bytes ≔ λ_ : Z ⇒ 0; m_regions ≔ r_base ≔ 65600; r_end ≔ 65608; r_kind ≔ GlobalData; r_life ≔ Live; r_base ≔ 65568; r_end ≔ 65576; r_kind ≔ GlobalData; r_life ≔ Live; m_aux ≔ λ_ : Z ⇒ CNone = SomeTAtom"slot_size", ptr_addr ≔ 65600; ptr_cap ≔ Obj65600; TAtom"slot", ptr_addr ≔ 65568; ptr_cap ≔ Obj65568; TAtom"use", ptr_addr ≔ 65552; ptr_cap ≔ FnTAtom"use"; TAtom"fill", ptr_addr ≔ 65536; ptr_cap ≔ FnTAtom"fill", m_bytes ≔ λ_ : Z ⇒ 0; m_regions ≔ r_base ≔ 65600; r_end ≔ 65608; r_kind ≔ GlobalData; r_life ≔ Live; r_base ≔ 65568; r_end ≔ 65576; r_kind ≔ GlobalData; r_life ≔ Live; m_aux ≔ λ_ : Z ⇒ CNone

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

vm_compute

reflexivity

The interpreter is ready in slot_memory at its start: both objects lie below it.

517Lemma slot_memory_ready

Explore proof 6 tactics

Initial goal

⊢

InterpRuntime.readyInterpRuntime.start slot_memory

split ; vm_compute ; split ; congruence |

E :

65600 =? b

→

Somesize_reg

65568 =? b

→

Someslot_reg

else

None

Somereg

⊢

0 ≤ b < InterpRuntime.start ∧ r_endreg ≤ InterpRuntime.start ∧ r_lifereg = Freed → r_endreg = b

destruct 65600 =? b eqn: E1 ; | destruct 65568 =? b eqn: E2 ; | discriminate E ; apply Z.eqb_eq in E1 || apply Z.eqb_eq in E2 ; subst b ; injection E as ← ; split ; vm_compute ; split ; congruence | ; split ; vm_compute ; congruence | discriminate

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

split ; vm_compute ; split ; congruence |

split ; | intros a _ ; split ; reflexivity

intros b reg E

change object_regionb size_reg; slot_reg = Somereg in E

cbn - [ Z.eqb ] in E

destruct 65600 =? b eqn: E1 ; | destruct 65568 =? b eqn: E2 ; | discriminate E ; apply Z.eqb_eq in E1 || apply Z.eqb_eq in E2 ; subst b ; injection E as ← ; split ; vm_compute ; split ; congruence | ; split ; vm_compute ; congruence | discriminate

The two static objects are apart.

527Lemma slot_memory_disjoint

live_disjointslot_memory

Explore proof 5 tactics

Initial goal

⊢

live_disjointslot_memory

intros b₁ r₁ b₂ r₂ E₁ _ E₂ _ Hne

b₁ :

r₁ :

b₂ :

r₂ :

E₁ :

object_regionb₁ m_regionsslot_memory = Somer₁

E₂ :

object_regionb₂ m_regionsslot_memory = Somer₂

Hne :

b₁ ≠ b₂

⊢

r_endr₁ ≤ b₂ ∨ r_endr₂ ≤ b₁

change object_regionb₁ size_reg; slot_reg = Somer₁ in E₁

b₁ :

r₁ :

b₂ :

r₂ :

E₁ :

object_regionb₁ size_reg; slot_reg = Somer₁

E₂ :

object_regionb₂ m_regionsslot_memory = Somer₂

Hne :

b₁ ≠ b₂

⊢

r_endr₁ ≤ b₂ ∨ r_endr₂ ≤ b₁

change object_regionb₂ size_reg; slot_reg = Somer₂ in E₂

b₁ :

r₁ :

b₂ :

r₂ :

E₁ :

object_regionb₁ size_reg; slot_reg = Somer₁

E₂ :

object_regionb₂ size_reg; slot_reg = Somer₂

Hne :

b₁ ≠ b₂

⊢

r_endr₁ ≤ b₂ ∨ r_endr₂ ≤ b₁

cbn - [ Z.eqb ] in E₁ , E₂

b₁ :

r₁ :

b₂ :

r₂ :