Filnix wiki

v :

ps :

listname × A

⊢

lookupk putk v ps = Somev

simpl

A :

Type

k :

v :

ps :

listname × A

⊢

name_eqbk k

→

Somev

else

lookupk filterλp : name × A ⇒ negbname_eqbk fstp ps

Somev

unfold name_eqb

A :

Type

k :

v :

ps :

listname × A

⊢

term_eqbk k

→

Somev

else

lookupk filterλp : name × A ⇒ negbterm_eqbk fstp ps

Somev

rewrite term_eqb_refl

A :

Type

k :

v :

ps :

listname × A

⊢

Somev = Somev

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros A k v ps

simpl

unfold name_eqb

rewrite term_eqb_refl

reflexivity

Putting a value for the name d leaves the value of every other name k.

37Lemma lookup_put_other

∀ A : Type k d v : A ps

name_eqbk d = false

lookupk putd v ps = lookupk ps

Explore proof 10 tactics

Initial goal

⊢

∀A : Type k d : name v : A ps : listname × A, name_eqbk d = false → lookupk putd v ps = lookupk ps

intros A k d v ps H

A :

Type

k, d :

v :

ps :

listname × A

H :

name_eqbk d = false

⊢

lookupk putd v ps = lookupk ps

simpl

A :

Type

k, d :

v :

ps :

listname × A

H :

name_eqbk d = false

⊢

name_eqbk d

→

Somev

else

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps

lookupk ps

rewrite H

A :

Type

k, d :

v :

ps :

listname × A

H :

name_eqbk d = false

⊢

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps = lookupk ps

induction ps as | k′ v′ ps IH ; simpl ; auto

A :

Type

k, d :

v :

k′ :

v′ :

ps :

listname × A

H :

name_eqbk d = false

IH :

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps = lookupk ps

⊢

lookupk

negbname_eqbd k′

→

k′, v′ :: filterλp : name × A ⇒ negbname_eqbd fstp ps

else

filterλp : name × A ⇒ negbname_eqbd fstp ps

name_eqbk k′

→

Somev′

else

lookupk ps

destruct name_eqbd k′ eqn: E ; simpl

2 open

A :

Type

k, d :

v :

k′ :

v′ :

ps :

listname × A

H :

name_eqbk d = false

IH :

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps = lookupk ps

E :

name_eqbd k′ = true

⊢

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps

name_eqbk k′

→

Somev′

else

lookupk ps

focused goal

A :

Type

k, d :

v :

k′ :

v′ :

ps :

listname × A

H :

name_eqbk d = false

IH :

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps = lookupk ps

E :

name_eqbd k′ = false

⊢

name_eqbk k′

→

Somev′

else

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps

name_eqbk k′

→

Somev′

else

lookupk ps

–apply term_eqb_eq in E

2 open

A :

Type

k, d :

v :

k′ :

v′ :

ps :

listname × A

H :

name_eqbk d = false

IH :

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps = lookupk ps

E :

d = k′

⊢

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps

name_eqbk k′

→

Somev′

else

lookupk ps

deferred goal

A :

Type

k, d :

v :

k′ :

v′ :

ps :

listname × A

H :

name_eqbk d = false

IH :

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps = lookupk ps

E :

name_eqbd k′ = false

⊢

name_eqbk k′

→

Somev′

else

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps

name_eqbk k′

→

Somev′

else

lookupk ps

subst k′

2 open

A :

Type

k, d :

v, v′ :

ps :

listname × A

H :

name_eqbk d = false

IH :

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps = lookupk ps

⊢

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps

name_eqbk d

→

Somev′

else

lookupk ps

deferred goal

A :

Type

k, d :

v :

k′ :

v′ :

ps :

listname × A

H :

name_eqbk d = false

IH :

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps = lookupk ps

E :

name_eqbd k′ = false

⊢

name_eqbk k′

→

Somev′

else

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps

name_eqbk k′

→

Somev′

else

lookupk ps

rewrite H

2 open

A :

Type

k, d :

v, v′ :

ps :

listname × A

H :

name_eqbk d = false

IH :

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps = lookupk ps

⊢

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps = lookupk ps

deferred goal

A :

Type

k, d :

v :

k′ :

v′ :

ps :

listname × A

H :

name_eqbk d = false

IH :

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps = lookupk ps

E :

name_eqbd k′ = false

⊢

name_eqbk k′

→

Somev′

else

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps

name_eqbk k′

→

Somev′

else

lookupk ps

exact IH

deferred goal

A :

Type

k, d :

v :

k′ :

v′ :

ps :

listname × A

H :

name_eqbk d = false

IH :

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps = lookupk ps

E :

name_eqbd k′ = false

⊢

name_eqbk k′

→

Somev′

else

lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps

name_eqbk k′

→

Somev′

else

lookupk ps

–destruct name_eqbk k′ ; auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros A k d v ps H

simpl

rewrite H

induction ps as | k′ v′ ps IH ; simpl ; auto

destruct name_eqbd k′ eqn: E ; simpl

–apply term_eqb_eq in E

subst k′

rewrite H

exact IH

–destruct name_eqbk k′ ; auto

What a fact means

The environment e' gives every name but d what the environment e gives it, as after a step that defines only d.

50Definition env_agreed : name e e′ : env : Prop ≔

∀n, name_eqbn d = false → lookupn e′ = lookupn e

The live fact fa, live(Q, P, Lo, Hi, Rights, Align), holds in memory m and environment e: the temporary Q holds a pointer word, P evaluates to the same word (a check yields its operand), and the access check of that pointer from Lo up to Hi passes in m (check_passes).

58Definition fact_holdsge : genv m : Memory.mem e : env fa : fact : Prop ≔

∃p, lookupf_qfa e = SomeWPtrp ∧ value_xge e P f_pfa = SomeWPtrp ∧ check_passesm p f_lofa f_hifa f_rfa f_alfa

Every fact of the list fs holds.

65Definition facts_holdge : genv m : Memory.mem e : env fs : listfact : Prop ≔

∀fa, Infa fs → fact_holdsge m e fa

A check reads only the region list, so one that passes in m passes in any memory m' with the same regions.

70Lemma check_passes_regions

∀ m m′ p lo hi r al

m_regionsm′ = m_regionsm

check_passesm p lo hi r al

check_passesm′ p lo hi r al

Explore proof 4 tactics

Initial goal

⊢

∀m m′ : Memory.mem p : ptr lo hi : Z r : rights al : Z, m_regionsm′ = m_regionsm → check_passesm p lo hi r al → check_passesm′ p lo hi r al

unfold check_passes , access_res

⊢

∀m m′ : Memory.mem p : ptr lo hi : Z r : rights al : Z, m_regionsm′ = m_regionsm → cap_access_resptr_capp m_regionsm raw_addressptr_addrp lo hi − lo r al = Someok → cap_access_resptr_capp m_regionsm′ raw_addressptr_addrp lo hi − lo r al = Someok

intros m m′ p lo hi r al E H

m, m′ :

Memory.mem

p :

lo, hi :

r :

al :

E :

m_regionsm′ = m_regionsm

H :

cap_access_resptr_capp m_regionsm raw_addressptr_addrp lo hi − lo r al = Someok

⊢

cap_access_resptr_capp m_regionsm′ raw_addressptr_addrp lo hi − lo r al = Someok

rewrite E

m, m′ :

Memory.mem

p :

lo, hi :

r :

al :

E :

m_regionsm′ = m_regionsm

H :

cap_access_resptr_capp m_regionsm raw_addressptr_addrp lo hi − lo r al = Someok

⊢

cap_access_resptr_capp m_regionsm raw_addressptr_addrp lo hi − lo r al = Someok

exact H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold check_passes , access_res

intros m m′ p lo hi r al E H

rewrite E

exact H

A fact that names neither d as its Q nor the temporary d (tmp(d)) as its P survives a step that changes no region and no temporary but d (env_agree).

77Lemma fact_holds_kill

∀ ge m m′ e e′ d fa

m_regionsm′ = m_regionsm

env_agreed e e′

name_eqbf_qfa d = false

value_eqbf_pfa Tmpd = false

fact_holdsge m e fa

fact_holdsge m′ e′ fa

Explore proof 9 tactics

Initial goal

⊢

∀ge : genv m m′ : Memory.mem e e′ : env d : name fa : fact, m_regionsm′ = m_regionsm → env_agreed e e′ → name_eqbf_qfa d = false → value_eqbf_pfa Tmpd = false → fact_holdsge m e fa → fact_holdsge m′ e′ fa

intros ge m m′ e e′ d fa Hr He Hq Hp p & Eq & Ep & Hc

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fa :

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

Hq :

name_eqbf_qfa d = false

Hp :

value_eqbf_pfa Tmpd = false

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

value_xge e P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

fact_holdsge m′ e′ fa

exists p

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fa :

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

Hq :

name_eqbf_qfa d = false

Hp :

value_eqbf_pfa Tmpd = false

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

value_xge e P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

lookupf_qfa e′ = SomeWPtrp ∧ value_xge e′ P f_pfa = SomeWPtrp ∧ check_passesm′ p f_lofa f_hifa f_rfa f_alfa

split ; | split

3 open

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fa :

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

Hq :

name_eqbf_qfa d = false

Hp :

value_eqbf_pfa Tmpd = false

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

value_xge e P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

lookupf_qfa e′ = SomeWPtrp

focused goal

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fa :

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

Hq :

name_eqbf_qfa d = false

Hp :

value_eqbf_pfa Tmpd = false

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

value_xge e P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

value_xge e′ P f_pfa = SomeWPtrp

focused goal

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fa :

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

Hq :

name_eqbf_qfa d = false

Hp :

value_eqbf_pfa Tmpd = false

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

value_xge e P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

check_passesm′ p f_lofa f_hifa f_rfa f_alfa

–rewrite He by exact Hq

3 open

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fa :

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

Hq :

name_eqbf_qfa d = false

Hp :

value_eqbf_pfa Tmpd = false

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

value_xge e P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

lookupf_qfa e = SomeWPtrp

deferred goal

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fa :

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

Hq :

name_eqbf_qfa d = false

Hp :

value_eqbf_pfa Tmpd = false

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

value_xge e P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

value_xge e′ P f_pfa = SomeWPtrp

deferred goal

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fa :

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

Hq :

name_eqbf_qfa d = false

Hp :

value_eqbf_pfa Tmpd = false

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

value_xge e P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

check_passesm′ p f_lofa f_hifa f_rfa f_alfa

exact Eq

2 open

deferred goal

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fa :

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

Hq :

name_eqbf_qfa d = false

Hp :

value_eqbf_pfa Tmpd = false

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

value_xge e P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

value_xge e′ P f_pfa = SomeWPtrp

deferred goal

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fa :

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

Hq :

name_eqbf_qfa d = false

Hp :

value_eqbf_pfa Tmpd = false

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

value_xge e P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

check_passesm′ p f_lofa f_hifa f_rfa f_alfa

–destruct f_pfa as n | c | g ; simpl in * ; auto

2 open

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fa :

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

Hq :

name_eqbf_qfa d = false

n :

Hp :

name_eqbn d = false

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

let* x ≔ lookupn e in

Somex

SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

let* x ≔ lookupn e′ in

Somex

SomeWPtrp

deferred goal

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fa :

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

Hq :

name_eqbf_qfa d = false

Hp :

value_eqbf_pfa Tmpd = false

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

value_xge e P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

check_passesm′ p f_lofa f_hifa f_rfa f_alfa

rewrite He by exact Hp

2 open

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fa :

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

Hq :

name_eqbf_qfa d = false

n :

Hp :

name_eqbn d = false

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

let* x ≔ lookupn e in

Somex

SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

let* x ≔ lookupn e in

Somex

SomeWPtrp

deferred goal

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fa :

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

Hq :

name_eqbf_qfa d = false

Hp :

value_eqbf_pfa Tmpd = false

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

value_xge e P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

check_passesm′ p f_lofa f_hifa f_rfa f_alfa

exact Ep

deferred goal

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fa :

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

Hq :

name_eqbf_qfa d = false

Hp :

value_eqbf_pfa Tmpd = false

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

value_xge e P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

check_passesm′ p f_lofa f_hifa f_rfa f_alfa

–eapply check_passes_regions ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros ge m m′ e e′ d fa Hr He Hq Hp p & Eq & Ep & Hc

exists p

split ; | split

–rewrite He by exact Hq

exact Eq

–destruct f_pfa as n | c | g ; simpl in * ; auto

rewrite He by exact Hp

exact Ep

–eapply check_passes_regions ; eauto

So the facts the pass keeps when d is defined, those kill d leaves (evidence_kill/3), hold after such a step.

90Lemma facts_hold_kill

∀ ge m m′ e e′ d fs

m_regionsm′ = m_regionsm

env_agreed e e′

facts_holdge m e fs

facts_holdge m′ e′ killd fs

Explore proof 5 tactics

Initial goal

⊢

∀ge : genv m m′ : Memory.mem e e′ : env d : name fs : listfact, m_regionsm′ = m_regionsm → env_agreed e e′ → facts_holdge m e fs → facts_holdge m′ e′ killd fs

unfold kill

⊢

∀ge : genv m m′ : Memory.mem e e′ : env d : name fs : listfact, m_regionsm′ = m_regionsm → env_agreed e e′ → facts_holdge m e fs → facts_holdge m′ e′ filterλf : fact ⇒ negbname_eqbf_qf d || value_eqbf_pf Tmpd fs

intros ge m m′ e e′ d fs Hr He H fa Hin

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fs :

listfact

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

H :

facts_holdge m e fs

fa :

Hin :

Infa filterλf : fact ⇒ negbname_eqbf_qf d || value_eqbf_pf Tmpd fs

⊢

fact_holdsge m′ e′ fa

apply filter_In in Hin as Hin Hk

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fs :

listfact

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

H :

facts_holdge m e fs

fa :

Hin :

Infa fs

Hk :

negbname_eqbf_qfa d || value_eqbf_pfa Tmpd = true

⊢

fact_holdsge m′ e′ fa

apply negb_true_iff , orb_false_iff in Hk as Hq Hp

ge :

m, m′ :

Memory.mem

e, e′ :

d :

fs :

listfact

Hr :

m_regionsm′ = m_regionsm

He :

env_agreed e e′

H :

facts_holdge m e fs

fa :

Hin :

Infa fs

Hq :

name_eqbf_qfa d = false

Hp :

value_eqbf_pfa Tmpd = false

⊢

fact_holdsge m′ e′ fa

eapply fact_holds_kill ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold kill

intros ge m m′ e e′ d fs Hr He H fa Hin

apply filter_In in Hin as Hin Hk

apply negb_true_iff , orb_false_iff in Hk as Hq Hp

eapply fact_holds_kill ; eauto

Facts that hold in m hold in any memory with the same regions.

100Lemma facts_hold_same

∀ ge m m′ e fs

m_regionsm′ = m_regionsm

facts_holdge m e fs

facts_holdge m′ e fs

Explore proof 5 tactics

Initial goal

⊢

∀ge : genv m m′ : Memory.mem e : env fs : listfact, m_regionsm′ = m_regionsm → facts_holdge m e fs → facts_holdge m′ e fs

intros ge m m′ e fs Hr H fa Hin

ge :

m, m′ :

Memory.mem

e :

fs :

listfact

Hr :

m_regionsm′ = m_regionsm

H :

facts_holdge m e fs

fa :

Hin :

Infa fs

⊢

fact_holdsge m′ e fa

destruct Hfa Hin as p & Eq & Ep & Hc

ge :

m, m′ :

Memory.mem

e :

fs :

listfact

Hr :

m_regionsm′ = m_regionsm

H :

facts_holdge m e fs

fa :

Hin :

Infa fs

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

value_xge e P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

fact_holdsge m′ e fa

exists p

ge :

m, m′ :

Memory.mem

e :

fs :

listfact

Hr :

m_regionsm′ = m_regionsm

H :

facts_holdge m e fs

fa :

Hin :

Infa fs

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

value_xge e P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

lookupf_qfa e = SomeWPtrp ∧ value_xge e P f_pfa = SomeWPtrp ∧ check_passesm′ p f_lofa f_hifa f_rfa f_alfa

repeat split ; auto

ge :

m, m′ :

Memory.mem

e :

fs :

listfact

Hr :

m_regionsm′ = m_regionsm

H :

facts_holdge m e fs

fa :

Hin :

Infa fs

p :

Eq :

lookupf_qfa e = SomeWPtrp

Ep :

value_xge e P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

check_passesm′ p f_lofa f_hifa f_rfa f_alfa

eapply check_passes_regions ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros ge m m′ e fs Hr H fa Hin

destruct Hfa Hin as p & Eq & Ep & Hc

exists p

repeat split ; auto

eapply check_passes_regions ; eauto

Steps that keep evidence

A store (store_res, store_res/7) writes bytes but leaves the region list unchanged.

111Lemma store_res_regions

∀ w m a c x r m′

store_resw m a c x = Somer, m′

m_regionsm′ = m_regionsm

Explore proof 3 tactics

Initial goal

⊢

∀w : width m : Memory.mem a : Z c : cap x : word r : resunit m′ : Memory.mem, store_resw m a c x = Somer, m′ → m_regionsm′ = m_regionsm

unfold store_res

⊢

∀ w : width m : Memory.mem a : Z c : cap x : word r : resunit m′ : Memory.mem ,

match w with

⇒

match x with

WPtrv

⇒

let* chk ≔ access_resm a c width_bytesw Write 8 in

Some

chk

match chk with

⇒

store_auxstore_bytesm a width_bytesw ptr_addrv a ptr_capv

⇒

None

⇒

match x with

WIntv

⇒

let* chk ≔

access_resm a c width_bytesw Write

match w with

⇒

Some

chk

match chk with

⇒

store_bytesm a width_bytesw v

⇒

None

Somer, m′

→

m_regionsm′ = m_regionsm

intros w m a c x r m′ H

w :

width

m :

Memory.mem

a :

c :

cap

x :

r :

resunit

m′ :

Memory.mem

H :

match w with

⇒

match x with

WPtrv

⇒

let* chk ≔ access_resm a c width_bytesw Write 8 in

Some

chk

match chk with

⇒

store_auxstore_bytesm a width_bytesw ptr_addrv a ptr_capv

⇒

None

⇒

match x with

WIntv

⇒

let* chk ≔

access_resm a c width_bytesw Write

match w with

⇒

Some

chk

match chk with

⇒

store_bytesm a width_bytesw v

⇒

None

Somer, m′

⊢

m_regionsm′ = m_regionsm

destruct w , x ; try discriminate ; cases H ; inversion H ; subst ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold store_res

intros w m a c x r m′ H

destruct w , x ; try discriminate ; cases H ; inversion H ; subst ; reflexivity

Reading a variadic argument through the argument pointer p (va_arg_res) leaves the region list unchanged, though it may write memory.

121Lemma va_arg_res_regions

∀ k p m r m′

va_arg_resk p m = Somer, m′

m_regionsm′ = m_regionsm

Explore proof 3 tactics

Initial goal

⊢

∀k : class p : ptr m : Memory.mem r : resword m′ : Memory.mem, va_arg_resk p m = Somer, m′ → m_regionsm′ = m_regionsm

unfold va_arg_res

⊢

∀ k : class p : ptr m : Memory.mem r : resword m′ : Memory.mem ,

match access_resm ptr_addrp ptr_capp 8 Read 8 with

SomeRVal_

⇒

match va_cellk with

Somestep, align

⇒

let* w ≔ class_widthk in

match access_resm ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align ptr_capptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp step Read 8 with

SomeRVal_

⇒

match store_resWl m ptr_addrp ptr_capp WIntptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align + step with

SomeRVal_, m₁

⇒

match k with

⇒

SomeRValWPtrptr_addr ≔ load_bytesm₁ ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align 8; ptr_cap ≔ aux_atm₁ ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align, m₁

⇒

SomeRValWIntload_bytesm₁ ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align width_bytesw, m₁

SomeRTrapwhy, m₁

⇒

SomeRTrapwhy, m₁

⇒

None

SomeRTrapwhy

⇒

SomeRTrapwhy, m

⇒

None

⇒

None

SomeRTrapwhy

⇒

SomeRTrapwhy, m

⇒

None

Somer, m′

→

m_regionsm′ = m_regionsm

intros k p m r m′ H

k :

p :

m :

Memory.mem

r :

m′ :

Memory.mem

H :

match access_resm ptr_addrp ptr_capp 8 Read 8 with

SomeRVal_

⇒

match va_cellk with

Somestep, align

⇒

let* w ≔ class_widthk in

SomeRVal_

⇒

match store_resWl m ptr_addrp ptr_capp WIntptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align + step with

SomeRVal_, m₁

⇒

match k with

⇒

SomeRValWIntload_bytesm₁ ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align width_bytesw, m₁

SomeRTrapwhy, m₁

⇒

SomeRTrapwhy, m₁

⇒

None

SomeRTrapwhy

⇒

SomeRTrapwhy, m

⇒

None

⇒

None

SomeRTrapwhy

⇒

SomeRTrapwhy, m

⇒

None

Somer, m′

⊢

m_regionsm′ = m_regionsm

cases H;match type of H withSome_, ?x = Some_, ?y⇒assert x = y as ← by congruenceend;first|reflexivity|match goal withE : store_res_ _ _ _ _ = Some_ |- _⇒exact store_res_regions_ _ _ _ _ _ _ Eend

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold va_arg_res

intros k p m r m′ H

cases H;match type of H withSome_, ?x = Some_, ?y⇒assert x = y as ← by congruenceend;first|reflexivity|match goal withE : store_res_ _ _ _ _ = Some_ |- _⇒exact store_res_regions_ _ _ _ _ _ _ Eend

No op with a result (op_res returning OpRes) changes a region: only alloc, free and the end of an invocation do.

132Lemma op_res_regions

∀ o k xs m r m′

op_reso k xs m = SomeOpResr m′

m_regionsm′ = m_regionsm

Explore proof 3 tactics

Initial goal

⊢

∀o : op k : class xs : listword m : Memory.mem r : resword m′ : Memory.mem, op_reso k xs m = SomeOpResr m′ → m_regionsm′ = m_regionsm

unfold op_res , float_integer

⊢

∀ o : op k : class xs : listword m : Memory.mem r : resword m′ : Memory.mem ,

match o with

Add | Sub | Mul | Div | Neg | Copy

⇒

match fmt_ofk with

Somef

⇒

let* r₀ ≔ float_arithmetico f xs in

SomeOpResRValWIntr₀ m

None

⇒

op_res_into k xs m

Cmpc ck

⇒

match xs with

WInta; WIntb

⇒

match fmt_ofck with

Somef

⇒

SomeOpResRValWIntfloat_comparec f a b m

None

⇒

op_res_into k xs m

WInta :: WIntb :: _ :: _

⇒

match fmt_ofck with

Some_

⇒

None

⇒

op_res_into k xs m

WInta | WInta :: WPtr_ :: _ | WInta :: WLimit_ _ :: _

⇒

match fmt_ofck with

Some_

⇒

None

⇒

op_res_into k xs m

⇒

match fmt_ofck with

Some_

⇒

None

⇒

op_res_into k xs m

FloatToIntfk sg

⇒

match xs with

⇒

let* from ≔ fmt_offk in

let* m₀ ≔ modulusk in

let 'lo, hi ≔

match sg with

Signed

⇒

−m₀ / 2, m₀ / 2 − 1

Unsigned

⇒

0, m₀ − 1

match Ieee.ieee_to_intfrom x with

Somen

⇒

lo ≤? n && n ≤? hi

→

SomeOpResRValWIntn mod m₀ m

else

SomeOpUBTAtom"float_conversion"

None

⇒

SomeOpUBTAtom"float_conversion"

WIntx :: _ :: _

⇒

op_res_into k xs m

⇒

op_res_into k xs m

IntToFloatik sg

⇒

match fmt_ofk with

Somef

⇒

match xs with

⇒

let* n ≔ integer_sourceik sg x in

SomeOpResRValWIntIeee.ieee_from_intf n m

WIntx :: _ :: _

⇒

op_res_into k xs m

⇒

op_res_into k xs m

None

⇒

op_res_into k xs m

Cast

⇒

match xs with

⇒

SomeOpResRValWIntx m

WIntx :: _ :: _

⇒

op_res_into k xs m

⇒

op_res_into k xs m

ExtF_ | Truncd | Truncx | Sqrt

⇒

match xs with

⇒

let* r₀ ≔ float_converto k x in

SomeOpResRValWIntr₀ m

WIntx :: _ :: _

⇒

op_res_into k xs m

⇒

op_res_into k xs m

VaArg

⇒

match xs with

WPtrp

⇒

let* rm ≔ va_arg_resk p m in

SomeOpResfstrm sndrm

WPtrp :: _ :: _

⇒

op_res_into k xs m

⇒

op_res_into k xs m

⇒

op_res_into k xs m

SomeOpResr m′

→

m_regionsm′ = m_regionsm

intros o k xs m r m′ H

o :

k :

xs :

listword

m :

Memory.mem

r :

m′ :

Memory.mem

H :

match o with

Add | Sub | Mul | Div | Neg | Copy

⇒

match fmt_ofk with

Somef

⇒

let* r ≔ float_arithmetico f xs in

SomeOpResRValWIntr m

None

⇒

op_res_into k xs m

Cmpc ck

⇒

match xs with

WInta; WIntb

⇒

match fmt_ofck with

Somef

⇒

SomeOpResRValWIntfloat_comparec f a b m

None

⇒

op_res_into k xs m

WInta :: WIntb :: _ :: _

⇒

match fmt_ofck with

Some_

⇒

None

⇒

op_res_into k xs m

WInta | WInta :: WPtr_ :: _ | WInta :: WLimit_ _ :: _

⇒

match fmt_ofck with

Some_

⇒

None

⇒

op_res_into k xs m

⇒

match fmt_ofck with

Some_

⇒

None

⇒

op_res_into k xs m

FloatToIntfk sg

⇒

match xs with

⇒

let* from ≔ fmt_offk in

let* m₀ ≔ modulusk in

let 'lo, hi ≔

match sg with

Signed

⇒

−m₀ / 2, m₀ / 2 − 1

Unsigned

⇒

0, m₀ − 1

match Ieee.ieee_to_intfrom x with

Somen

⇒

lo ≤? n && n ≤? hi

→

SomeOpResRValWIntn mod m₀ m

else

SomeOpUBTAtom"float_conversion"

None

⇒

SomeOpUBTAtom"float_conversion"

WIntx :: _ :: _

⇒

op_res_into k xs m

⇒

op_res_into k xs m

IntToFloatik sg

⇒

match fmt_ofk with

Somef

⇒

match xs with

⇒

let* n ≔ integer_sourceik sg x in

SomeOpResRValWIntIeee.ieee_from_intf n m

WIntx :: _ :: _

⇒

op_res_into k xs m

⇒

op_res_into k xs m

None

⇒

op_res_into k xs m

Cast

⇒

match xs with

⇒

SomeOpResRValWIntx m

WIntx :: _ :: _

⇒

op_res_into k xs m

⇒

op_res_into k xs m

ExtF_ | Truncd | Truncx | Sqrt

⇒

match xs with

⇒

let* r ≔ float_converto k x in

SomeOpResRValWIntr m

WIntx :: _ :: _

⇒

op_res_into k xs m

⇒

op_res_into k xs m

VaArg

⇒

match xs with

WPtrp

⇒

let* rm ≔ va_arg_resk p m in

SomeOpResfstrm sndrm

WPtrp :: _ :: _

⇒

op_res_into k xs m

⇒

op_res_into k xs m

⇒

op_res_into k xs m

SomeOpResr m′

⊢

m_regionsm′ = m_regionsm

destruct o ; cases H ; inversion H ; subst;first|reflexivity|match goal withE : op_res_int_ _ _ _ = Some_ |- _⇒rewrite op_res_int_mem_ _ _ _ _ _ E ; reflexivityend|match goal withE : va_arg_res_ _ _ = Some?rm |- _⇒destruct rm ; exact va_arg_res_regions_ _ _ _ _ Eend

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold op_res , float_integer

intros o k xs m r m′ H

destruct o ; cases H ; inversion H ; subst;first|reflexivity|match goal withE : op_res_int_ _ _ _ = Some_ |- _⇒rewrite op_res_int_mem_ _ _ _ _ _ E ; reflexivityend|match goal withE : va_arg_res_ _ _ = Some?rm |- _⇒destruct rm ; exact va_arg_res_regions_ _ _ _ _ Eend

Binding the result r to the name d (bind_res) continues only with a value x: the environment gains d bound to x, and memory is unchanged.

147Lemma bind_res_continue

∀ d r e l m e′ l′ m′

bind_resd r e l m = IContinuee′ l′ m′

∃x, r = RValx ∧ e′ = putd x e ∧ m′ = m

Explore proof 3 tactics

Initial goal

⊢

∀d : name r : resword e : env l : listname × optionZ m : Memory.mem e′ : env l′ : listname × optionZ m′ : Memory.mem, bind_resd r e l m = IContinuee′ l′ m′ → ∃x : word, r = RValx ∧ e′ = putd x e ∧ m′ = m

unfold bind_res

⊢

∀ d : name r : resword e : env l : listname × optionZ m : Memory.mem e′ : env l′ : listname × optionZ m′ : Memory.mem ,

match r with

RValx

⇒

IContinueputd x e l m

RTrapwhy

⇒

IStopTrapwhy

RUncheckedwhy

⇒

IStopUncheckedwhy

IContinuee′ l′ m′

→

∃x : word, r = RValx ∧ e′ = putd x e ∧ m′ = m

intros d r e l m e′ l′ m′ H

d :

r :

e :

l :

listname × optionZ

m :

Memory.mem

e′ :

l′ :

listname × optionZ

m′ :

Memory.mem

H :

match r with

RValx

⇒

IContinueputd x e l m

RTrapwhy

⇒

IStopTrapwhy

RUncheckedwhy

⇒

IStopUncheckedwhy

IContinuee′ l′ m′

⊢

∃x : word, r = RValx ∧ e′ = putd x e ∧ m′ = m

destruct r ; inversion H ; subst ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold bind_res

intros d r e l m e′ l′ m′ H

destruct r ; inversion H ; subst ; eauto

Putting a value for d changes no other name.

152Lemma env_agree_put

∀ d x e

env_agreed e putd x e

Explore proof 3 tactics

Initial goal

⊢

∀d : name x : word e : env, env_agreed e putd x e

intros d x e n H

d :

x :

e :

n :

H :

name_eqbn d = false

⊢

lookupn putd x e = lookupn e

apply lookup_put_other

d :

x :

e :

n :

H :

name_eqbn d = false

⊢

name_eqbn d = false

exact H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros d x e n H

apply lookup_put_other

exact H

An evidence-preserving instruction i (evidence_preserving/1) that continues changes no region, and no temporary but the one it defines (inst_def_first); one that defines none leaves the environment as it was.

159Lemma preserving_step

∀ ge fr m i e′ l′ m′

evidence_preservingi = true

inst_stepge fr m i = SomeIContinuee′ l′ m′

m_regionsm′ = m_regionsm

∧

match inst_def_firsti with

Somed

⇒

env_agreed fr_envfr e′

None

⇒

e′ = fr_envfr

Proof 28 steps Qed

intros ge fr m i e′ l′ m′ Hp H

destruct i ; simpl in Hp ; try discriminate Hp

let

–destruct special_leto eqn: Es

+destruct o ; try discriminate Es ; destruct k ; discriminate Hp

+rewrite inst_step_let_ _ _ _ _ _ _ Es in H

simpl

cbn zeta in H

injection H as Hb

destruct bind_res_continue_ _ _ _ _ _ _ _ Hb as x & → & → & →

split ; eapply op_res_regions ; eauto | apply env_agree_put

flight

–simpl in H

injection H as ← ← ←

split ; reflexivity | apply env_agree_put

raw_store, not of a pointer

–simpl in H

injection H as Hs

destruct raw_res_ eqn: Er in Hs ; inversion Hs ; subst

split ; eapply store_res_regions ; eauto | reflexivity

loc

–simpl in H

injection H as ← ← ←

simpl

auto

touch

–simpl in H

injection H as ← ← ←

simpl

auto

The pass's bookkeeping

Where the facts fs hold before the instruction i of the frame fr and i continues, the facts evidence_after/3 keeps after it hold: a preserving instruction kills what it redefines, any other keeps nothing. The pass's kill is exactly what the proof needs.

194Theorem evidence_after_holds

∀ ge fr m i e′ l′ m′ fs

facts_holdge m fr_envfr fs

inst_stepge fr m i = SomeIContinuee′ l′ m′

facts_holdge m′ e′ evidence_afteri fs

Explore proof 8 tactics

Initial goal

⊢

∀ge : genv fr : frame m : Memory.mem i : inst e′ : env l′ : listname × optionZ m′ : Memory.mem fs : listfact, facts_holdge m fr_envfr fs → inst_stepge fr m i = SomeIContinuee′ l′ m′ → facts_holdge m′ e′ evidence_afteri fs

unfold evidence_after

⊢

∀ ge : genv fr : frame m : Memory.mem i : inst e′ : env l′ : listname × optionZ m′ : Memory.mem fs : listfact ,

facts_holdge m fr_envfr fs

→

inst_stepge fr m i = SomeIContinuee′ l′ m′

→

facts_holdge m′ e′

evidence_preservingi

→

match inst_def_firsti with

Somed

⇒

killd fs

None

⇒

else

[ ]

intros ge fr m i e′ l′ m′ fs H Hs

ge :

fr :

m :

Memory.mem

i :

e′ :

l′ :

listname × optionZ

m′ :

Memory.mem

fs :

listfact

H :

facts_holdge m fr_envfr fs

Hs :

inst_stepge fr m i = SomeIContinuee′ l′ m′

⊢

facts_holdge m′ e′

evidence_preservingi

→

match inst_def_firsti with

Somed

⇒

killd fs

None

⇒

else

[ ]

destruct evidence_preservingi eqn: Hp ; | intros fa

ge :

fr :

m :

Memory.mem

i :

e′ :

l′ :

listname × optionZ

m′ :

Memory.mem

fs :

listfact

H :

facts_holdge m fr_envfr fs

Hs :

inst_stepge fr m i = SomeIContinuee′ l′ m′

Hp :

evidence_preservingi = true

⊢

facts_holdge m′ e′

match inst_def_firsti with

Somed

⇒

killd fs

None

⇒

destruct preserving_step_ _ _ _ _ _ _ Hp Hs as Hr Hd

ge :

fr :

m :

Memory.mem

i :

e′ :

l′ :

listname × optionZ

m′ :

Memory.mem

fs :

listfact

H :

facts_holdge m fr_envfr fs

Hs :

inst_stepge fr m i = SomeIContinuee′ l′ m′

Hp :

evidence_preservingi = true

Hr :

m_regionsm′ = m_regionsm

Hd :

match inst_def_firsti with

Somed

⇒

env_agreed fr_envfr e′

None

⇒

e′ = fr_envfr

⊢

facts_holdge m′ e′

match inst_def_firsti with

Somed

⇒

killd fs

None

⇒

destruct inst_def_firsti as d |

2 open

ge :

fr :

m :

Memory.mem

i :

e′ :

l′ :

listname × optionZ

m′ :

Memory.mem

fs :

listfact

H :

facts_holdge m fr_envfr fs

Hs :

inst_stepge fr m i = SomeIContinuee′ l′ m′

Hp :

evidence_preservingi = true

Hr :

m_regionsm′ = m_regionsm

d :

Hd :

env_agreed fr_envfr e′

⊢

facts_holdge m′ e′ killd fs

focused goal

ge :

fr :

m :

Memory.mem

i :

e′ :

l′ :

listname × optionZ

m′ :

Memory.mem

fs :

listfact

H :

facts_holdge m fr_envfr fs

Hs :

inst_stepge fr m i = SomeIContinuee′ l′ m′

Hp :

evidence_preservingi = true

Hr :

m_regionsm′ = m_regionsm

Hd :

e′ = fr_envfr

⊢

facts_holdge m′ e′ fs

–eapply facts_hold_kill ; eauto

deferred goal

ge :

fr :

m :

Memory.mem

i :

e′ :

l′ :

listname × optionZ

m′ :

Memory.mem

fs :

listfact

H :

facts_holdge m fr_envfr fs

Hs :

inst_stepge fr m i = SomeIContinuee′ l′ m′

Hp :

evidence_preservingi = true

Hr :

m_regionsm′ = m_regionsm

Hd :

e′ = fr_envfr

⊢

facts_holdge m′ e′ fs

–subst e′

ge :

fr :

m :

Memory.mem

i :

l′ :

listname × optionZ

m′ :

Memory.mem

fs :

listfact

H :

facts_holdge m fr_envfr fs

Hs :

inst_stepge fr m i = SomeIContinuefr_envfr l′ m′

Hp :

evidence_preservingi = true

Hr :

m_regionsm′ = m_regionsm

⊢

facts_holdge m′ fr_envfr fs

eapply facts_hold_same ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold evidence_after

intros ge fr m i e′ l′ m′ fs H Hs

destruct evidence_preservingi eqn: Hp ; | intros fa

destruct preserving_step_ _ _ _ _ _ _ Hp Hs as Hr Hd

destruct inst_def_firsti as d |

–eapply facts_hold_kill ; eauto

–subst e′

eapply facts_hold_same ; eauto

Accesses through a live fact

The newest live fact of q (fact_of) is one of the facts, and is q's.

211Lemma fact_of_in

∀ q fs fa

fact_ofq fs = Somefa

Infa fs ∧ f_qfa = q

Explore proof 9 tactics

Initial goal

⊢

∀q : name fs : listfact fa : fact, fact_ofq fs = Somefa → Infa fs ∧ f_qfa = q

intros q fs fa

q :

fs :

listfact

fa :

⊢

fact_ofq fs = Somefa → Infa fs ∧ f_qfa = q

induction fs as | f fs IH ; simpl ; discriminate |

q :

f :

fs :

listfact

fa :

IH :

fact_ofq fs = Somefa → Infa fs ∧ f_qfa = q

⊢

name_eqbf_qf q

→

Somef

else

fact_ofq fs

Somefa

→

f = fa ∨ Infa fs ∧ f_qfa = q

destruct name_eqbf_qf q eqn: E

2 open

q :

f :

fs :

listfact

fa :

IH :

fact_ofq fs = Somefa → Infa fs ∧ f_qfa = q

E :

name_eqbf_qf q = true

⊢

Somef = Somefa → f = fa ∨ Infa fs ∧ f_qfa = q

focused goal

q :

f :

fs :

listfact

fa :

IH :

fact_ofq fs = Somefa → Infa fs ∧ f_qfa = q

E :

name_eqbf_qf q = false

⊢

fact_ofq fs = Somefa → f = fa ∨ Infa fs ∧ f_qfa = q

–intros H

2 open

q :

f :

fs :

listfact

fa :

IH :

fact_ofq fs = Somefa → Infa fs ∧ f_qfa = q

E :

name_eqbf_qf q = true

H :

Somef = Somefa

⊢

f = fa ∨ Infa fs ∧ f_qfa = q

deferred goal

q :

f :

fs :

listfact

fa :

IH :

fact_ofq fs = Somefa → Infa fs ∧ f_qfa = q

E :

name_eqbf_qf q = false

⊢

fact_ofq fs = Somefa → f = fa ∨ Infa fs ∧ f_qfa = q

injection H as ←

2 open

q :

f :

fs :

listfact

IH :

fact_ofq fs = Somef → Inf fs ∧ f_qf = q

E :

name_eqbf_qf q = true

⊢

f = f ∨ Inf fs ∧ f_qf = q

deferred goal

q :

f :

fs :

listfact

fa :

IH :

fact_ofq fs = Somefa → Infa fs ∧ f_qfa = q

E :

name_eqbf_qf q = false

⊢

fact_ofq fs = Somefa → f = fa ∨ Infa fs ∧ f_qfa = q

split ; left ; reflexivity | apply term_eqb_eq ; exact E

deferred goal

q :

f :

fs :

listfact

fa :

IH :

fact_ofq fs = Somefa → Infa fs ∧ f_qfa = q

E :

name_eqbf_qf q = false

⊢

fact_ofq fs = Somefa → f = fa ∨ Infa fs ∧ f_qfa = q

–intros H

q :

f :

fs :

listfact

fa :

IH :

fact_ofq fs = Somefa → Infa fs ∧ f_qfa = q

E :

name_eqbf_qf q = false

H :

fact_ofq fs = Somefa

⊢

f = fa ∨ Infa fs ∧ f_qfa = q

destruct IHH

q :

f :

fs :

listfact

fa :

IH :

fact_ofq fs = Somefa → Infa fs ∧ f_qfa = q

E :

name_eqbf_qf q = false

H :

fact_ofq fs = Somefa

H₀ :

Infa fs

H₁ :

f_qfa = q

⊢

f = fa ∨ Infa fs ∧ f_qfa = q

split ; right | ; auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros q fs fa

induction fs as | f fs IH ; simpl ; discriminate |

destruct name_eqbf_qf q eqn: E

–intros H

injection H as ←

split ; left ; reflexivity | apply term_eqb_eq ; exact E

–intros H

destruct IHH

split ; right | ; auto

Where objects fit the address space (objects_fit) and the facts fs hold, a raw access i that the newest live fact fa of its address operand q covers (covered_access), as the pass's reusing case asks, gives no unchecked. With evidence_after_holds and check_like_holds this is proof persistence within a block.

224Theorem live_access_not_unchecked

∀ ge fr m i q fs fa why

facts_holdge m fr_envfr fs

fact_ofq fs = Somefa

covered_accessi q f_lofa f_hifa f_rfa f_alfa = true

inst_stepge fr m i ≠ SomeIStopUncheckedwhy

Explore proof 5 tactics

Initial goal

⊢

∀ge : genv fr : frame m : Memory.mem i : inst q : name fs : listfact fa : fact why : reason, objects_fitm_regionsm → facts_holdge m fr_envfr fs → fact_ofq fs = Somefa → covered_accessi q f_lofa f_hifa f_rfa f_alfa = true → inst_stepge fr m i ≠ SomeIStopUncheckedwhy

intros ge fr m i q fs fa why Hfit H Hf Hc

ge :

fr :

m :

Memory.mem

i :

q :

fs :

listfact

fa :

why :

Hfit :

H :

facts_holdge m fr_envfr fs

Hf :

fact_ofq fs = Somefa

Hc :

covered_accessi q f_lofa f_hifa f_rfa f_alfa = true

⊢

inst_stepge fr m i ≠ SomeIStopUncheckedwhy

destruct fact_of_in_ _ _ Hf as Hin Hq

ge :

fr :

m :

Memory.mem

i :

q :

fs :

listfact

fa :

why :

Hfit :

H :

facts_holdge m fr_envfr fs

Hf :

fact_ofq fs = Somefa

Hc :

covered_accessi q f_lofa f_hifa f_rfa f_alfa = true

Hin :

Infa fs

Hq :

f_qfa = q

⊢

inst_stepge fr m i ≠ SomeIStopUncheckedwhy

destruct Hfa Hin as p & Eq & _ & Hp

ge :

fr :

m :

Memory.mem

i :

q :

fs :

listfact

fa :

why :

Hfit :

H :

facts_holdge m fr_envfr fs

Hf :

fact_ofq fs = Somefa

Hc :

covered_accessi q f_lofa f_hifa f_rfa f_alfa = true

Hin :

Infa fs

Hq :

f_qfa = q

p :

Eq :

lookupf_qfa fr_envfr = SomeWPtrp

Hp :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

inst_stepge fr m i ≠ SomeIStopUncheckedwhy

rewrite Hq in Eq

ge :

fr :

m :

Memory.mem

i :

q :

fs :

listfact

fa :

why :

Hfit :

H :

facts_holdge m fr_envfr fs

Hf :

fact_ofq fs = Somefa

Hc :

covered_accessi q f_lofa f_hifa f_rfa f_alfa = true

Hin :

Infa fs

Hq :

f_qfa = q

p :

Eq :

lookupq fr_envfr = SomeWPtrp

Hp :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

inst_stepge fr m i ≠ SomeIStopUncheckedwhy

exact covered_access_not_unchecked_ _ _ _ _ _ _ _ _ _ _ Hfit Hc Eq Hp

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros ge fr m i q fs fa why Hfit H Hf Hc

destruct fact_of_in_ _ _ Hf as Hin Hq

destruct Hfa Hin as p & Eq & _ & Hp

rewrite Hq in Eq

exact covered_access_not_unchecked_ _ _ _ _ _ _ _ _ _ _ Hfit Hc Eq Hp

A fact that holds, put before a list of facts that hold.

238Lemma facts_hold_cons

∀ ge m e fa fs

fact_holdsge m e fa

facts_holdge m e fs

facts_holdge m e fa :: fs

Explore proof 1 tactics

Initial goal

⊢

∀ge : genv m : Memory.mem e : env fa : fact fs : listfact, fact_holdsge m e fa → facts_holdge m e fs → facts_holdge m e fa :: fs

intros ge m e fa fs H Hs fb ← | Hin ; auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros ge m e fa fs H Hs fb ← | Hin ; auto

Every form the pass adds a fact for

Each check-like op, check, check_ahead, renew, renew_hull, half_check, renew_if and check_limit, continues only where the access check of its pointer operand passed: a renew's renew_res/4, a half check's half_res/4 and a limit's checked result are values only then. So the fact the pass adds after any of them (after_check) holds, and so does the wider range a check_ahead asks of the access it is checked for.

The fact checked_inst_rest/7 adds after the check-like instruction i, live(Q, P, Lo, Hi, Rights, Align), read off its op and its pointer operand P; None for any other instruction.

255Definition check_facti : inst : optionfact ≔

match i with

⇒

SomemkFactq p lo hi r al

⇒

None

The range the access after the check-like instruction i must lie in (proof_use/6): its fact's, except that a check_ahead's reaches to its wider end AHi.

270Definition access_facti : inst : optionfact ≔

match i with

Letq A CheckAheadlo _ r al ahi p

⇒

SomemkFactq p lo ahi r al

⇒

check_facti

Where P evaluates to the pointer pp in e (value_x), it still does once Q is bound to pp too, even if P is the temporary Q itself.

278Lemma value_x_put_same

∀ ge e q p pp

value_xge e P p = SomeWPtrpp

value_xge putq WPtrpp e P p = SomeWPtrpp

Explore proof 11 tactics

Initial goal

⊢

∀ge : genv e : env q : name p : value pp : ptr, value_xge e P p = SomeWPtrpp → value_xge putq WPtrpp e P p = SomeWPtrpp

intros ge e q p pp Ex

ge :

e :

q :

p :

pp :

Ex :

value_xge e P p = SomeWPtrpp

⊢

value_xge putq WPtrpp e P p = SomeWPtrpp

destruct p as n | c | g ; | exact Ex | exact Ex

ge :

e :

q, n :

pp :

Ex :

value_xge e P Tmpn = SomeWPtrpp

⊢

value_xge putq WPtrpp e P Tmpn = SomeWPtrpp

unfold value_x in *

ge :

e :

q, n :

pp :

Ex :

let* x ≔ lookupn e in

SomeWPtrpp

⊢

let* x ≔ lookupn putq WPtrpp e in

SomeWPtrpp

destruct name_eqbn q eqn: E

2 open

ge :

e :

q, n :

pp :

Ex :

let* x ≔ lookupn e in

SomeWPtrpp

E :

name_eqbn q = true

⊢

let* x ≔ lookupn putq WPtrpp e in

SomeWPtrpp

focused goal

ge :

e :

q, n :

pp :

Ex :

let* x ≔ lookupn e in

SomeWPtrpp

E :

name_eqbn q = false

⊢

let* x ≔ lookupn putq WPtrpp e in

SomeWPtrpp

–apply term_eqb_eq in E

2 open

ge :

e :

q, n :

pp :

Ex :

let* x ≔ lookupn e in

SomeWPtrpp

E :

n = q

⊢

let* x ≔ lookupn putq WPtrpp e in

SomeWPtrpp

deferred goal

ge :

e :

q, n :

pp :

Ex :

let* x ≔ lookupn e in

SomeWPtrpp

E :

name_eqbn q = false

⊢

let* x ≔ lookupn putq WPtrpp e in

SomeWPtrpp

subst n

2 open

ge :

e :

q :

pp :

Ex :

let* x ≔ lookupq e in

SomeWPtrpp

⊢

let* x ≔ lookupq putq WPtrpp e in

SomeWPtrpp

deferred goal

ge :

e :

q, n :

pp :

Ex :

let* x ≔ lookupn e in

SomeWPtrpp

E :

name_eqbn q = false

⊢

let* x ≔ lookupn putq WPtrpp e in

SomeWPtrpp

rewrite lookup_put_same

2 open

ge :

e :

q :

pp :

Ex :

let* x ≔ lookupq e in

SomeWPtrpp

⊢

word_at_classP WPtrpp = SomeWPtrpp

deferred goal

ge :

e :

q, n :

pp :

Ex :

let* x ≔ lookupn e in

SomeWPtrpp

E :

name_eqbn q = false

⊢

let* x ≔ lookupn putq WPtrpp e in

SomeWPtrpp

destruct lookupq e as w | ; simpl in Ex ; | discriminate Ex

2 open

ge :

e :

q :

pp :

w :

Ex :

Somew = SomeWPtrpp

⊢

word_at_classP WPtrpp = SomeWPtrpp

deferred goal

ge :

e :

q, n :

pp :

Ex :

let* x ≔ lookupn e in

SomeWPtrpp

E :

name_eqbn q = false

⊢

let* x ≔ lookupn putq WPtrpp e in

SomeWPtrpp

reflexivity

deferred goal

ge :

e :

q, n :

pp :

Ex :

let* x ≔ lookupn e in

SomeWPtrpp

E :

name_eqbn q = false

⊢

let* x ≔ lookupn putq WPtrpp e in

SomeWPtrpp

–rewrite lookup_put_other by exact E

ge :

e :

q, n :

pp :

Ex :

let* x ≔ lookupn e in

SomeWPtrpp

E :

name_eqbn q = false

⊢

let* x ≔ lookupn e in

SomeWPtrpp

exact Ex

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros ge e q p pp Ex

destruct p as n | c | g ; | exact Ex | exact Ex

unfold value_x in *

destruct name_eqbn q eqn: E

–apply term_eqb_eq in E

subst n

rewrite lookup_put_same

destruct lookupq e as w | ; simpl in Ex ; | discriminate Ex

reflexivity

–rewrite lookup_put_other by exact E

exact Ex

Splits on every match a hypothesis is stuck on, and uses every equation between constructors: the case analysis behind check_like_continue and let_step.

291Ltac crush ≔

repeat (match goal withH : ?x = ?x |- _⇒clear HH : _ = _ |- _⇒injection H ; clear H ; intros ; substH : _ |- _⇒match type of H withcontext [match ?x with _ ⇒ _ end]⇒destruct x eqn :? ; try discriminate H ; cbn beta iota zeta in *endend;try subst)

An access check (cap_access_res, cap_access_res/7) traps or passes; it is never unchecked.

304Lemma cap_access_res_checked

∀ c rs a size r al why

cap_access_resc rs a size r al ≠ SomeRUncheckedwhy

Explore proof 3 tactics

Initial goal

⊢

∀c : cap rs : listregion a size : Z r : rights al : Z why : reason, cap_access_resc rs a size r al ≠ SomeRUncheckedwhy

unfold cap_access_res , readonly_access_res , aligned_res

⊢

∀ c : cap rs : listregion a size : Z r : rights al : Z why : reason ,

match c with

CNone

⇒

SomeRTrapNullCapability

Objbase

⇒

let* reg ≔ object_regionbase rs in

Some

base ≤? a && a + size ≤? r_endreg

→

a mod al =? 0

→

else

RTrapMisaligned

else

RTrapOutOfBounds

Robase

⇒

let* reg ≔ object_regionbase rs in

Some

base ≤? a && a + size ≤? r_endreg

→

match r with

Read

⇒

a mod al =? 0

→

else

⇒

else

Fn_

⇒

SomeRTrapOutOfBounds

External_

⇒

None

≠

SomeRUncheckedwhy

intros c rs a size r al why H

c :

cap

rs :

listregion

a, size :

r :

al :

why :

H :

match c with

CNone

⇒

SomeRTrapNullCapability

Objbase

⇒

let* reg ≔ object_regionbase rs in

Some

base ≤? a && a + size ≤? r_endreg

→

a mod al =? 0

→

else

RTrapMisaligned

else

RTrapOutOfBounds

Robase

⇒

let* reg ≔ object_regionbase rs in

Some

base ≤? a && a + size ≤? r_endreg

→

match r with

Read

⇒

a mod al =? 0

→

else

⇒

else

Fn_

⇒

SomeRTrapOutOfBounds

External_

⇒

None

SomeRUncheckedwhy

⊢

False

destruct c ; try discriminate H ; destruct object_region_ _ ; try discriminate H ; destruct _ && _ ; try discriminate H ; try destruct r ; try discriminate H ; destruct _ =? 0 ; discriminate H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold cap_access_res , readonly_access_res , aligned_res

intros c rs a size r al why H

destruct c ; try discriminate H ; destruct object_region_ _ ; try discriminate H ; destruct _ && _ ; try discriminate H ; try destruct r ; try discriminate H ; destruct _ =? 0 ; discriminate H

What every check-like op i that continues leaves: Q bound to P's pointer pp, memory as it was, and its checks passed: that of its fact fa (check_fact), and that of the range fb its access must lie in (access_fact), which has the same Q and P.

318Lemma check_like_continue

∀ ge fr m i fa fb e′ l′ m′

check_facti = Somefa

access_facti = Somefb

inst_stepge fr m i = SomeIContinuee′ l′ m′

m′ = m ∧ f_qfb = f_qfa ∧ f_pfb = f_pfa ∧ ∃pp, e′ = putf_qfa WPtrpp fr_envfr ∧ value_xge fr_envfr P f_pfa = SomeWPtrpp ∧ check_passesm pp f_lofa f_hifa f_rfa f_alfa ∧ check_passesm pp f_lofb f_hifb f_rfb f_alfb

Proof 11 steps Qed

unfold check_passes , access_res

intros ge fr m i fa fb e′ l′ m′ Hf Hg H

destruct k ; try destruct o ; discriminate Hf

destruct o ; try discriminate Hf ; rewrite inst_step_let in H by reflexivity ; cbn zeta in H

all: destruct args as | a₁ | a₂ | a₃ | a₄ args ; simpl in Hf , Hg ; try discriminate Hf ; injection Hf as ← ; injection Hg as ← ; cbn [ f_q f_p f_lo f_hi f_r f_al ]

all: simpl in H ; unfold op_res , op_res_int , checked_res , renew_res , half_res , bind_res in H

all: crush

all: repeat match goal withu : unit |- _⇒destruct uend;unfold access_res in *

all: try refine conjeq_refl conjeq_refl conjeq_refl _ ; eexists ; split ; reflexivity | split ; reflexivity | split ; eassumption

all: exfalso ; eapply cap_access_res_checked ; eassumption

After a check-like op that continues, its fact fa holds, and so does fb, the range its access must lie in.

346Theorem check_like_holds

∀ ge fr m i fa fb e′ l′ m′

check_facti = Somefa

access_facti = Somefb

inst_stepge fr m i = SomeIContinuee′ l′ m′

fact_holdsge m′ e′ fa ∧ fact_holdsge m′ e′ fb

Explore proof 3 tactics

Initial goal

⊢

∀ge : genv fr : frame m : Memory.mem i : inst fa fb : fact e′ : env l′ : listname × optionZ m′ : Memory.mem, check_facti = Somefa → access_facti = Somefb → inst_stepge fr m i = SomeIContinuee′ l′ m′ → fact_holdsge m′ e′ fa ∧ fact_holdsge m′ e′ fb

intros ge fr m i fa fb e′ l′ m′ Hf Hg H

ge :

fr :

m :

Memory.mem

i :

fa, fb :

e′ :

l′ :

listname × optionZ

m′ :

Memory.mem

Hf :

check_facti = Somefa

Hg :

access_facti = Somefb

H :

inst_stepge fr m i = SomeIContinuee′ l′ m′

⊢

fact_holdsge m′ e′ fa ∧ fact_holdsge m′ e′ fb

destruct check_like_continue_ _ _ _ _ _ _ _ _ Hf Hg H as → & Hq & Hp & pp & → & Ex & Ha & Hb

ge :

fr :

m :

Memory.mem

i :

fa, fb :

l′ :

listname × optionZ

Hf :

check_facti = Somefa

Hg :

access_facti = Somefb

pp :

H :

inst_stepge fr m i = SomeIContinueputf_qfa WPtrpp fr_envfr l′ m

Hq :

f_qfb = f_qfa

Hp :

f_pfb = f_pfa

Ex :

value_xge fr_envfr P f_pfa = SomeWPtrpp

Ha :

check_passesm pp f_lofa f_hifa f_rfa f_alfa

Hb :

check_passesm pp f_lofb f_hifb f_rfb f_alfb

⊢

fact_holdsge m putf_qfa WPtrpp fr_envfr fa ∧ fact_holdsge m putf_qfa WPtrpp fr_envfr fb

split ; exists pp ; | rewrite Hq , Hp ; split ; apply lookup_put_same | split ; apply value_x_put_same ; exact Ex | assumption

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros ge fr m i fa fb e′ l′ m′ Hf Hg H

destruct check_like_continue_ _ _ _ _ _ _ _ _ Hf Hg H as → & Hq & Hp & pp & → & Ex & Ha & Hb

split ; exists pp ; | rewrite Hq , Hp ; split ; apply lookup_put_same | split ; apply value_x_put_same ; exact Ex | assumption

Every `let`

A let of the name d that continues changes no region and no temporary but d.

361Lemma let_step

∀ ge fr m d k o args e′ l′ m′

inst_stepge fr m Letd k o args = SomeIContinuee′ l′ m′

m_regionsm′ = m_regionsm ∧ env_agreed fr_envfr e′

Explore proof 9 tactics

Initial goal

⊢

∀ge : genv fr : frame m : Memory.mem d : name k : class o : op args : listvalue e′ : env l′ : listname × optionZ m′ : Memory.mem, inst_stepge fr m Letd k o args = SomeIContinuee′ l′ m′ → m_regionsm′ = m_regionsm ∧ env_agreed fr_envfr e′

intros ge fr m d k o args e′ l′ m′ H

ge :

fr :

m :

Memory.mem

d :

k :

o :

args :

listvalue

e′ :

l′ :

listname × optionZ

m′ :

Memory.mem

H :

inst_stepge fr m Letd k o args = SomeIContinuee′ l′ m′

⊢

m_regionsm′ = m_regionsm ∧ env_agreed fr_envfr e′

destruct special_leto eqn: Es

2 open

ge :

fr :

m :

Memory.mem

d :

k :

o :

args :

listvalue

e′ :

l′ :

listname × optionZ

m′ :

Memory.mem

H :

inst_stepge fr m Letd k o args = SomeIContinuee′ l′ m′

Es :

special_leto = true

⊢

m_regionsm′ = m_regionsm ∧ env_agreed fr_envfr e′

focused goal

ge :

fr :

m :

Memory.mem

d :

k :

o :

args :

listvalue

e′ :

l′ :

listname × optionZ

m′ :

Memory.mem

H :

inst_stepge fr m Letd k o args = SomeIContinuee′ l′ m′

Es :

special_leto = false

⊢

m_regionsm′ = m_regionsm ∧ env_agreed fr_envfr e′

–destruct o ; try discriminate Es ; unfold inst_step in H ; cbn zeta in H ; crush ; unfold bind_res in * ; crush ; split ; try reflexivity ; apply env_agree_put

deferred goal

ge :

fr :

m :

Memory.mem

d :

k :

o :

args :

listvalue

e′ :

l′ :

listname × optionZ

m′ :

Memory.mem

H :

inst_stepge fr m Letd k o args = SomeIContinuee′ l′ m′

Es :

special_leto = false

⊢

m_regionsm′ = m_regionsm ∧ env_agreed fr_envfr e′

–rewrite inst_step_let_ _ _ _ _ _ _ Es in H

ge :

fr :

m :

Memory.mem

d :

k :

o :

args :

listvalue

e′ :

l′ :

listname × optionZ

m′ :

Memory.mem

H :

let e ≔ fr_envfr in

let locals ≔ fr_localsfr in

let* classes ≔ op_arg_classeso k in

let* xs ≔ map2_optionvalue_xge e classes args in

match op_reso k xs m with

SomeOpResr m′

⇒

Somebind_resd r e locals m′

SomeOpUBwhy

⇒

SomeIStopUBwhy

SomeOpAllocq kont

⇒

Some

IFreshq

λ base : Z ⇒

let x, m′ ≔ kontbase in

putd x e, locals, m′

None

⇒

None

SomeIContinuee′ l′ m′

Es :

special_leto = false

⊢

m_regionsm′ = m_regionsm ∧ env_agreed fr_envfr e′

cbn zeta in H

ge :

fr :

m :

Memory.mem

d :

k :

o :

args :

listvalue

e′ :

l′ :

listname × optionZ

m′ :

Memory.mem

H :

let* classes ≔ op_arg_classeso k in

let* xs ≔ map2_optionvalue_xge fr_envfr classes args in

match op_reso k xs m with

SomeOpResr m′

⇒

Somebind_resd r fr_envfr fr_localsfr m′

SomeOpUBwhy

⇒

SomeIStopUBwhy

SomeOpAllocq kont

⇒

Some

IFreshq

λ base : Z ⇒

let x, m′ ≔ kontbase in

putd x fr_envfr, fr_localsfr, m′

None

⇒

None

SomeIContinuee′ l′ m′

Es :

special_leto = false

⊢

m_regionsm′ = m_regionsm ∧ env_agreed fr_envfr e′

cases H

ge :

fr :

m :

Memory.mem

d :

k :

o :

args :

listvalue

e′ :

l′ :

listname × optionZ

m′ :

Memory.mem

l :

listclass

Heqo₀ :

op_arg_classeso k = Somel

l₀ :

listword

Heqo₁ :

map2_optionvalue_xge fr_envfr l args = Somel₀

o₀ :

op_out

r :

m₀ :

Memory.mem

Heqo₃ :

o₀ = OpResr m₀

Heqo₂ :

op_reso k l₀ m = SomeOpResr m₀

H :

Somebind_resd r fr_envfr fr_localsfr m₀ = SomeIContinuee′ l′ m′

Es :

special_leto = false

⊢

m_regionsm′ = m_regionsm ∧ env_agreed fr_envfr e′

injection H as Hb

ge :

fr :

m :

Memory.mem

d :

k :

o :

args :

listvalue

e′ :

l′ :

listname × optionZ

m′ :

Memory.mem

l :

listclass

Heqo₀ :

op_arg_classeso k = Somel

l₀ :

listword

Heqo₁ :

map2_optionvalue_xge fr_envfr l args = Somel₀

o₀ :

op_out

r :

m₀ :

Memory.mem

Heqo₃ :

o₀ = OpResr m₀

Heqo₂ :

op_reso k l₀ m = SomeOpResr m₀

Hb :

bind_resd r fr_envfr fr_localsfr m₀ = IContinuee′ l′ m′

Es :

special_leto = false

⊢

m_regionsm′ = m_regionsm ∧ env_agreed fr_envfr e′

destruct bind_res_continue_ _ _ _ _ _ _ _ Hb as x & → & → & →

ge :

fr :

m :

Memory.mem

d :

k :

o :

args :

listvalue

l′ :

listname × optionZ

l :

listclass

Heqo₀ :

op_arg_classeso k = Somel

l₀ :

listword

Heqo₁ :

map2_optionvalue_xge fr_envfr l args = Somel₀

o₀ :

op_out

m₀ :

Memory.mem

x :

Hb :

bind_resd RValx fr_envfr fr_localsfr m₀ = IContinueputd x fr_envfr l′ m₀

Heqo₂ :

op_reso k l₀ m = SomeOpResRValx m₀

Heqo₃ :

o₀ = OpResRValx m₀

Es :

special_leto = false

⊢

m_regionsm₀ = m_regionsm ∧ env_agreed fr_envfr putd x fr_envfr

split ; eapply op_res_regions ; eauto | apply env_agree_put

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros ge fr m d k o args e′ l′ m′ H

destruct special_leto eqn: Es

–destruct o ; try discriminate Es ; unfold inst_step in H ; cbn zeta in H ; crush ; unfold bind_res in * ; crush ; split ; try reflexivity ; apply env_agree_put

–rewrite inst_step_let_ _ _ _ _ _ _ Es in H

cbn zeta in H

injection H as Hb

destruct bind_res_continue_ _ _ _ _ _ _ _ Hb as x & → & → & →

split ; eapply op_res_regions ; eauto | apply env_agree_put

Block entry

A block is entered by an edge from the block before it, and its phis bind their temporaries. An unpolled edge changes nothing; the entry facts of ir.pl's pass are the meet of the exit facts of the blocks it may come from, less those that name a phi's temporary (Validate.v's evidence_pass).

The facts fs less those that name a temporary of the phis phs as Q or P: what Validate.v's evidence_pass keeps at a block's entry of the meet of the facts that reach it.

384Definition entry_killphs : listphi fs : listfact : listfact ≔

fold_left

λ fs : listfact ph : phi ⇒

match ph with

Phid _ _

⇒

filterλfa ⇒ negbname_eqbf_qfa d || value_eqbf_pfa Tmpd fs

phs

The temporary a phi defines.

390Definition phi_destph : phi : name ≔

match ph with

Phid _ _

⇒

A fact entry_kill keeps is one of fs and names no phi's temporary, as Q or as P.

394Lemma entry_kill_in

∀ phs fs fa

Infa entry_killphs fs

Infa fs ∧ ∀ph, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

Explore proof 6 tactics

Initial goal

⊢

∀phs : listphi fs : listfact fa : fact, Infa entry_killphs fs → Infa fs ∧ ∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

induction phs as | d k ps phs IH ; simpl ; intros fs fa H ; split ; exact H | tauto |

d :

k :

ps :

listname × value

phs :

listphi

IH :

∀fs : listfact fa : fact, Infa entry_killphs fs → Infa fs ∧ ∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

fs :

listfact

fa :

H :

Infa entry_killphs filterλfa : fact ⇒ negbname_eqbf_qfa d || value_eqbf_pfa Tmpd fs

⊢

Infa fs ∧ ∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

destruct IH_ _ H as Hin Hph

d :

k :

ps :

listname × value

phs :

listphi

IH :

∀fs : listfact fa : fact, Infa entry_killphs fs → Infa fs ∧ ∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

fs :

listfact

fa :

H :

Infa entry_killphs filterλfa : fact ⇒ negbname_eqbf_qfa d || value_eqbf_pfa Tmpd fs

Hin :

Infa filterλfa : fact ⇒ negbname_eqbf_qfa d || value_eqbf_pfa Tmpd fs

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

⊢

Infa fs ∧ ∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

apply filter_In in Hin as Hin Hk

d :

k :

ps :

listname × value

phs :

listphi

IH :

∀fs : listfact fa : fact, Infa entry_killphs fs → Infa fs ∧ ∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

fs :

listfact

fa :

H :

Infa entry_killphs filterλfa : fact ⇒ negbname_eqbf_qfa d || value_eqbf_pfa Tmpd fs

Hin :

Infa fs

Hk :

negbname_eqbf_qfa d || value_eqbf_pfa Tmpd = true

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

⊢

Infa fs ∧ ∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

apply negb_true_iff , orb_false_iff in Hk

d :

k :

ps :

listname × value

phs :

listphi

IH :

∀fs : listfact fa : fact, Infa entry_killphs fs → Infa fs ∧ ∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

fs :

listfact

fa :

H :

Infa entry_killphs filterλfa : fact ⇒ negbname_eqbf_qfa d || value_eqbf_pfa Tmpd fs

Hin :

Infa fs

Hk :

name_eqbf_qfa d = false ∧ value_eqbf_pfa Tmpd = false

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

⊢

Infa fs ∧ ∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

split ; exact Hin |

d :

k :

ps :

listname × value

phs :

listphi

IH :

∀fs : listfact fa : fact, Infa entry_killphs fs → Infa fs ∧ ∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

fs :

listfact

fa :

H :

Infa entry_killphs filterλfa : fact ⇒ negbname_eqbf_qfa d || value_eqbf_pfa Tmpd fs

Hin :

Infa fs

Hk :

name_eqbf_qfa d = false ∧ value_eqbf_pfa Tmpd = false

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

⊢

∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

intros ph ← | Hp ; exact Hk | auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

induction phs as | d k ps phs IH ; simpl ; intros fs fa H ; split ; exact H | tauto |

destruct IH_ _ H as Hin Hph

apply filter_In in Hin as Hin Hk

apply negb_true_iff , orb_false_iff in Hk

split ; exact Hin |

intros ph ← | Hp ; exact Hk | auto

Once one phi fails to find its value, the fold over the rest fails too.

406Lemma phis_fold_none

∀ ge phs pred e₀

fold_left

λ acc ph ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

None

Explore proof 2 tactics

Initial goal

⊢

∀ ge : genv phs : listphi pred : name e₀ : env ,

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

None

intros ge phs pred e₀

ge :

phs :

listphi

pred :

e₀ :

⊢

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

None

induction phs ; simpl ; auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros ge phs pred e₀

induction phs ; simpl ; auto

Running the phis phs on entry from the block pred changes only their own temporaries: every other name n keeps its value.

419Lemma phis_env_agree

∀ ge phs pred e₀ e₁ e n

fold_left

λ acc ph ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₁

Somee

∀ph, Inph phs → name_eqbn phi_destph = false

lookupn e = lookupn e₁

Explore proof 9 tactics

Initial goal

⊢

∀ ge : genv phs : listphi pred : name e₀ : env e₁ e : listname × word ,

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e₂ ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e₂

phs

Somee₁

Somee

→

∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e₁

induction phs as | d k ps phs IH ; simpl ; intros pred e₀ e₁ e H n Hn

2 open

ge :

pred :

e₀ :

e₁, e :

listname × word

H :

Somee₁ = Somee

n :

Hn :

∀ph : phi, False → name_eqbn phi_destph = false

⊢

lookupn e = lookupn e₁

focused goal

ge :

d :

k :

ps :

listname × value

phs :

listphi

IH :

∀ pred : name e₀ : env e₁ e : listname × word ,

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e₂ ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e₂

phs

Somee₁

Somee

→

∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e₁

pred :

e₀ :

e₁, e :

listname × word

H :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

let* v ≔ lookuppred ps in

let* x ≔ value_xge e₀ k v in

Someputd x e₁

Somee

n :

Hn :

∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbn phi_destph = false

⊢

lookupn e = lookupn e₁

–injection H as ←

2 open

ge :

pred :

e₀ :

e₁ :

listname × word

n :

Hn :

∀ph : phi, False → name_eqbn phi_destph = false

⊢

lookupn e₁ = lookupn e₁

deferred goal

ge :

d :

k :

ps :

listname × value

phs :

listphi

IH :

∀ pred : name e₀ : env e₁ e : listname × word ,

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e₂ ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e₂

phs

Somee₁

Somee

→

∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e₁

pred :

e₀ :

e₁, e :

listname × word

H :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

let* v ≔ lookuppred ps in

let* x ≔ value_xge e₀ k v in

Someputd x e₁

Somee

n :

Hn :

∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbn phi_destph = false

⊢

lookupn e = lookupn e₁

reflexivity

deferred goal

ge :

d :

k :

ps :

listname × value

phs :

listphi

IH :

∀ pred : name e₀ : env e₁ e : listname × word ,

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e₂ ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e₂

phs

Somee₁

Somee

→

∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e₁

pred :

e₀ :

e₁, e :

listname × word

H :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

let* v ≔ lookuppred ps in

let* x ≔ value_xge e₀ k v in

Someputd x e₁

Somee

n :

Hn :

∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbn phi_destph = false

⊢

lookupn e = lookupn e₁

–destruct lookuppred ps as v | ; simpl in H ; | rewrite phis_fold_none in H ; discriminate H

ge :

d :

k :

ps :

listname × value

phs :

listphi

IH :

∀ pred : name e₀ : env e₁ e : listname × word ,

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e₂ ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e₂

phs

Somee₁

Somee

→

∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e₁

pred :

e₀ :

e₁, e :

listname × word

v :

H :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

let* x ≔ value_xge e₀ k v in

Someputd x e₁

Somee

n :

Hn :

∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbn phi_destph = false

⊢

lookupn e = lookupn e₁

destruct value_xge e₀ k v as x | ; simpl in H ; | rewrite phis_fold_none in H ; discriminate H

ge :

d :

k :

ps :

listname × value

phs :

listphi

IH :

∀ pred : name e₀ : env e₁ e : listname × word ,

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e₂ ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e₂

phs

Somee₁

Somee

→

∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e₁

pred :

e₀ :

e₁, e :

listname × word

v :

x :

H :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Someputd x e₁

Somee

n :

Hn :

∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbn phi_destph = false

⊢

lookupn e = lookupn e₁

rewrite IH_ _ _ _ H n by auto

ge :

d :

k :

ps :

listname × value

phs :

listphi

IH :

∀ pred : name e₀ : env e₁ e : listname × word ,

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e₂ ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e₂

phs

Somee₁

Somee

→

∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e₁

pred :

e₀ :

e₁, e :

listname × word

v :

x :

H :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Someputd x e₁

Somee

n :

Hn :

∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbn phi_destph = false

⊢

lookupn putd x e₁ = lookupn e₁

apply lookup_put_other

ge :

d :

k :

ps :

listname × value

phs :

listphi

IH :

∀ pred : name e₀ : env e₁ e : listname × word ,

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e₂ ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e₂

phs

Somee₁

Somee

→

∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e₁

pred :

e₀ :

e₁, e :

listname × word

v :

x :

H :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Someputd x e₁

Somee

n :

Hn :

∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbn phi_destph = false

⊢

name_eqbn d = false

apply HnPhid k ps

ge :

d :

k :

ps :

listname × value

phs :

listphi

IH :

∀ pred : name e₀ : env e₁ e : listname × word ,

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e₂ ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e₂

phs

Somee₁

Somee

→

∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e₁

pred :

e₀ :

e₁, e :

listname × word

v :

x :

H :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Someputd x e₁

Somee

n :

Hn :

∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbn phi_destph = false

⊢

Phid k ps = Phid k ps ∨ InPhid k ps phs

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

induction phs as | d k ps phs IH ; simpl ; intros pred e₀ e₁ e H n Hn

–injection H as ←

reflexivity

–destruct lookuppred ps as v | ; simpl in H ; | rewrite phis_fold_none in H ; discriminate H

destruct value_xge e₀ k v as x | ; simpl in H ; | rewrite phis_fold_none in H ; discriminate H

rewrite IH_ _ _ _ H n by auto

apply lookup_put_other

apply HnPhid k ps

auto

Entering a block from the block pred, where its phis bind (phis_env, phis_env/6) and the facts fs held before them, the facts that name no phi temporary (entry_kill) hold after.

440Theorem phis_facts_hold

∀ ge m phs pred e₀ e fs

phis_envge phs Somepred e₀ = Somee

facts_holdge m e₀ fs

facts_holdge m e entry_killphs fs

Explore proof 16 tactics

Initial goal

⊢

∀ge : genv m : Memory.mem phs : listphi pred : name e₀ e : env fs : listfact, phis_envge phs Somepred e₀ = Somee → facts_holdge m e₀ fs → facts_holdge m e entry_killphs fs

unfold phis_env

⊢

∀ ge : genv m : Memory.mem phs : listphi pred : name e₀ e : env fs : listfact ,

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e₁ ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e₁

phs

Somee₀

Somee

→

facts_holdge m e₀ fs → facts_holdge m e entry_killphs fs

intros ge m phs pred e₀ e fs Hp H fa Hin

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

⊢

fact_holdsge m e fa

destruct entry_kill_in_ _ _ Hin as Hin′ Hph

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

Hin′ :

Infa fs

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

⊢

fact_holdsge m e fa

destruct Hfa Hin′ as p & Eq & Ep & Hc

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

Hin′ :

Infa fs

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

p :

Eq :

lookupf_qfa e₀ = SomeWPtrp

Ep :

value_xge e₀ P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

fact_holdsge m e fa

exists p

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

Hin′ :

Infa fs

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

p :

Eq :

lookupf_qfa e₀ = SomeWPtrp

Ep :

value_xge e₀ P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

lookupf_qfa e = SomeWPtrp ∧ value_xge e P f_pfa = SomeWPtrp ∧ check_passesm p f_lofa f_hifa f_rfa f_alfa

split ; | split ; | exact Hc

2 open

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

Hin′ :

Infa fs

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

p :

Eq :

lookupf_qfa e₀ = SomeWPtrp

Ep :

value_xge e₀ P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

lookupf_qfa e = SomeWPtrp

focused goal

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

Hin′ :

Infa fs

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

p :

Eq :

lookupf_qfa e₀ = SomeWPtrp

Ep :

value_xge e₀ P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

value_xge e P f_pfa = SomeWPtrp

–rewrite phis_env_agree_ _ _ _ _ _ Hp ; exact Eq |

2 open

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

Hin′ :

Infa fs

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

p :

Eq :

lookupf_qfa e₀ = SomeWPtrp

Ep :

value_xge e₀ P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false

deferred goal

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

Hin′ :

Infa fs

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

p :

Eq :

lookupf_qfa e₀ = SomeWPtrp

Ep :

value_xge e₀ P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

value_xge e P f_pfa = SomeWPtrp

intros ph Hi

2 open

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

Hin′ :

Infa fs

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

p :

Eq :

lookupf_qfa e₀ = SomeWPtrp

Ep :

value_xge e₀ P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

ph :

Hi :

Inph phs

⊢

name_eqbf_qfa phi_destph = false

deferred goal

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

Hin′ :

Infa fs

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

p :

Eq :

lookupf_qfa e₀ = SomeWPtrp

Ep :

value_xge e₀ P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

value_xge e P f_pfa = SomeWPtrp

apply Hphph Hi

deferred goal

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

Hin′ :

Infa fs

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbf_pfa Tmpphi_destph = false

p :

Eq :

lookupf_qfa e₀ = SomeWPtrp

Ep :

value_xge e₀ P f_pfa = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

value_xge e P f_pfa = SomeWPtrp

–destruct f_pfa as n | c | g eqn: Ef ; | exact Ep | exact Ep

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

Hin′ :

Infa fs

n :

Ef :

f_pfa = Tmpn

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ value_eqbTmpn Tmpphi_destph = false

p :

Eq :

lookupf_qfa e₀ = SomeWPtrp

Ep :

value_xge e₀ P Tmpn = SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

value_xge e P Tmpn = SomeWPtrp

simpl in *

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

Hin′ :

Infa fs

n :

Ef :

f_pfa = Tmpn

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ name_eqbn phi_destph = false

p :

Eq :

lookupf_qfa e₀ = SomeWPtrp

Ep :

let* x ≔ lookupn e₀ in

Somex

SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

let* x ≔ lookupn e in

Somex

SomeWPtrp

rewrite phis_env_agree_ _ _ _ _ _ Hp ; exact Ep |

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

Hin′ :

Infa fs

n :

Ef :

f_pfa = Tmpn

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ name_eqbn phi_destph = false

p :

Eq :

lookupf_qfa e₀ = SomeWPtrp

Ep :

let* x ≔ lookupn e₀ in

Somex

SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

⊢

∀ph : phi, Inph phs → name_eqbn phi_destph = false

intros ph Hi

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

Hin′ :

Infa fs

n :

Ef :

f_pfa = Tmpn

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ name_eqbn phi_destph = false

p :

Eq :

lookupf_qfa e₀ = SomeWPtrp

Ep :

let* x ≔ lookupn e₀ in

Somex

SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

ph :

Hi :

Inph phs

⊢

name_eqbn phi_destph = false

pose proof proj2Hphph Hi as Hv

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

Hin′ :

Infa fs

n :

Ef :

f_pfa = Tmpn

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ name_eqbn phi_destph = false

p :

Eq :

lookupf_qfa e₀ = SomeWPtrp

Ep :

let* x ≔ lookupn e₀ in

Somex

SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

ph :

Hi :

Inph phs

Hv :

name_eqbn phi_destph = false

⊢

name_eqbn phi_destph = false

simpl in Hv

ge :

m :

Memory.mem

phs :

listphi

pred :

e₀, e :

fs :

listfact

Hp :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge e₀ k v in

Someputd x e

phs

Somee₀

Somee

H :

facts_holdge m e₀ fs

fa :

Hin :

Infa entry_killphs fs

Hin′ :

Infa fs

n :

Ef :

f_pfa = Tmpn

Hph :

∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false ∧ name_eqbn phi_destph = false

p :

Eq :

lookupf_qfa e₀ = SomeWPtrp

Ep :

let* x ≔ lookupn e₀ in

Somex

SomeWPtrp

Hc :

check_passesm p f_lofa f_hifa f_rfa f_alfa

ph :

Hi :

Inph phs

Hv :

name_eqbn phi_destph = false

⊢

name_eqbn phi_destph = false

exact Hv

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold phis_env

intros ge m phs pred e₀ e fs Hp H fa Hin

destruct entry_kill_in_ _ _ Hin as Hin′ Hph

destruct Hfa Hin′ as p & Eq & Ep & Hc

exists p

split ; | split ; | exact Hc

–rewrite phis_env_agree_ _ _ _ _ _ Hp ; exact Eq |

intros ph Hi

apply Hphph Hi

–destruct f_pfa as n | c | g eqn: Ef ; | exact Ep | exact Ep

simpl in *

rewrite phis_env_agree_ _ _ _ _ _ Hp ; exact Ep |

intros ph Hi

pose proof proj2Hphph Hi as Hv

simpl in Hv

exact Hv

value_eqb is equality of values.

454Lemma value_eqb_eq

∀ v w

value_eqbv w = true

v = w

Explore proof 1 tactics

Initial goal

⊢

∀v w : value, value_eqbv w = true → v = w

intros a | a | a b | b | b H ; simpl in H ; try discriminate H ; f_equal ; first apply Z.eqb_eq | apply term_eqb_eq ; exact H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros a | a | a b | b | b H ; simpl in H ; try discriminate H ; f_equal ; first apply Z.eqb_eq | apply term_eqb_eq ; exact H

fact_eqb is equality of facts.

461Lemma fact_eqb_eq

∀ a b

fact_eqba b = true

a = b

Explore proof 10 tactics

Initial goal

⊢

∀a b : fact, fact_eqba b = true → a = b

intros q p lo hi r al q′ p′ lo′ hi′ r′ al′ H

q :

p :

lo, hi :

r :

al :

q′ :

p′ :

lo′, hi′ :

r′ :

al′ :

H :

fact_eqbf_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ al f_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ r′; f_al ≔ al′ = true

⊢

f_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ al = f_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ r′; f_al ≔ al′

unfold fact_eqb in H

q :

p :

lo, hi :

r :

al :

q′ :

p′ :

lo′, hi′ :

r′ :

al′ :

H :

name_eqbf_qf_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ al f_qf_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ r′; f_al ≔ al′ && value_eqbf_pf_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ al f_pf_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ r′; f_al ≔ al′ && f_lof_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ al =? f_lof_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ r′; f_al ≔ al′ && f_hif_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ al =? f_hif_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ r′; f_al ≔ al′ && rights_eqbf_rf_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ al f_rf_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ r′; f_al ≔ al′ && f_alf_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ al =? f_alf_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ r′; f_al ≔ al′ = true

⊢

f_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ al = f_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ r′; f_al ≔ al′

simpl in H

q :

p :

lo, hi :

r :

al :

q′ :

p′ :

lo′, hi′ :

r′ :

al′ :

H :

name_eqbq q′ && value_eqbp p′ && lo =? lo′ && hi =? hi′ && rights_eqbr r′ && al =? al′ = true

⊢

f_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ al = f_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ r′; f_al ≔ al′

repeat rewrite andb_true_iff in H

q :

p :

lo, hi :

r :

al :

q′ :

p′ :

lo′, hi′ :

r′ :

al′ :

H :

name_eqbq q′ = true ∧ value_eqbp p′ = true ∧ lo =? lo′ = true ∧ hi =? hi′ = true ∧ rights_eqbr r′ = true ∧ al =? al′ = true

⊢

f_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ al = f_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ r′; f_al ≔ al′

destruct H as Hq & Hp & Hl & Hh & Hr & Ha

q :

p :

lo, hi :

r :

al :

q′ :

p′ :

lo′, hi′ :

r′ :

al′ :

Hq :

name_eqbq q′ = true

Hp :

value_eqbp p′ = true

Hl :

lo =? lo′ = true

Hh :

hi =? hi′ = true

Hr :

rights_eqbr r′ = true

Ha :

al =? al′ = true

⊢

f_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ al = f_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ r′; f_al ≔ al′

apply term_eqb_eq in Hq

q :

p :

lo, hi :

r :

al :

q′ :

p′ :

lo′, hi′ :

r′ :

al′ :

Hq :

q = q′

Hp :

value_eqbp p′ = true

Hl :

lo =? lo′ = true

Hh :

hi =? hi′ = true

Hr :

rights_eqbr r′ = true

Ha :

al =? al′ = true

⊢

f_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ al = f_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ r′; f_al ≔ al′

apply value_eqb_eq in Hp

q :

p :

lo, hi :

r :

al :

q′ :

p′ :

lo′, hi′ :

r′ :

al′ :

Hq :

q = q′

Hp :

p = p′

Hl :

lo =? lo′ = true

Hh :

hi =? hi′ = true

Hr :

rights_eqbr r′ = true

Ha :

al =? al′ = true

⊢

f_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ al = f_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ r′; f_al ≔ al′

apply Z.eqb_eq in Hl , Hh , Ha

q :

p :

lo, hi :

r :

al :

q′ :

p′ :

lo′, hi′ :

r′ :

al′ :

Hq :

q = q′

Hp :

p = p′

Hl :

lo = lo′

Hh :

hi = hi′

Hr :

rights_eqbr r′ = true

Ha :

al = al′

⊢

f_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ al = f_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ r′; f_al ≔ al′

destruct r , r′ ; try discriminate Hr

2 open

q :

p :

lo, hi, al :

q′ :

p′ :

lo′, hi′, al′ :

Hq :

q = q′

Hp :

p = p′

Hl :

lo = lo′

Hh :

hi = hi′

Hr :

rights_eqbRead Read = true

Ha :

al = al′

⊢

f_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ Read; f_al ≔ al = f_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ Read; f_al ≔ al′

focused goal

q :

p :

lo, hi, al :

q′ :

p′ :

lo′, hi′, al′ :

Hq :

q = q′

Hp :

p = p′

Hl :

lo = lo′

Hh :

hi = hi′

Hr :

rights_eqbWrite Write = true

Ha :

al = al′

⊢

f_q ≔ q; f_p ≔ p; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ Write; f_al ≔ al = f_q ≔ q′; f_p ≔ p′; f_lo ≔ lo′; f_hi ≔ hi′; f_r ≔ Write; f_al ≔ al′

all: subst ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros q p lo hi r al q′ p′ lo′ hi′ r′ al′ H

unfold fact_eqb in H

simpl in H

repeat rewrite andb_true_iff in H

destruct H as Hq & Hp & Hl & Hh & Hr & Ha

apply term_eqb_eq in Hq

apply value_eqb_eq in Hp

apply Z.eqb_eq in Hl , Hh , Ha

destruct r , r′ ; try discriminate Hr

all: subst ; reflexivity

A fact of the meet (evidence_meet, evidence_meet/2) of the sets of facts that reach a block is a fact of every set it meets.

472Lemma evidence_meet_in

∀ sets s fa

Infa evidence_meetsets

Ins sets

Infa s

Explore proof 10 tactics

Initial goal

⊢

∀sets : listlistfact s : listfact fa : fact, Infa evidence_meetsets → Ins sets → Infa s

unfold evidence_meet

⊢

∀ sets : listlistfact s : listfact fa : fact ,

Infa

match sets with

[ ]

⇒

[ ]

s₀ :: ss

⇒

filterλf : fact ⇒ forallbλs′ : listfact ⇒ existsbfact_eqbf s′ ss s₀

→

Ins sets → Infa s

intros | s₀ ss s fa H Hs ; destruct H |

s₀ :

listfact

ss :

listlistfact

s :

listfact

fa :

H :

Infa filterλf : fact ⇒ forallbλs′ : listfact ⇒ existsbfact_eqbf s′ ss s₀

Hs :

Ins s₀ :: ss

⊢

Infa s

apply filter_In in H as H₀ Hall

s₀ :

listfact

ss :

listlistfact

s :

listfact

fa :

H₀ :

Infa s₀

Hall :

forallbλs′ : listfact ⇒ existsbfact_eqbfa s′ ss = true

Hs :

Ins s₀ :: ss

⊢

Infa s

destruct Hs as ← | Hs ; exact H₀ |

s₀ :

listfact

ss :

listlistfact

s :

listfact

fa :

H₀ :

Infa s₀

Hall :

forallbλs′ : listfact ⇒ existsbfact_eqbfa s′ ss = true

Hs :

Ins ss

⊢

Infa s

rewrite forallb_forall in Hall

s₀ :

listfact

ss :

listlistfact

s :

listfact

fa :

H₀ :

Infa s₀

Hall :

∀x : listfact, Inx ss → existsbfact_eqbfa x = true

Hs :

Ins ss

⊢

Infa s

pose proof Halls Hs as Ex

s₀ :

listfact

ss :

listlistfact

s :

listfact

fa :

H₀ :

Infa s₀

Hall :

∀x : listfact, Inx ss → existsbfact_eqbfa x = true

Hs :

Ins ss

Ex :

existsbfact_eqbfa s = true

⊢

Infa s

apply existsb_exists in Ex as y & Hy & E

s₀ :

listfact

ss :

listlistfact

s :

listfact

fa :

H₀ :

Infa s₀

Hall :

∀x : listfact, Inx ss → existsbfact_eqbfa x = true

Hs :

Ins ss

y :

Hy :

Iny s

E :

fact_eqbfa y = true

⊢

Infa s

apply fact_eqb_eq in E

s₀ :

listfact

ss :

listlistfact

s :

listfact

fa :

H₀ :

Infa s₀

Hall :

∀x : listfact, Inx ss → existsbfact_eqbfa x = true

Hs :

Ins ss

y :

Hy :

Iny s

E :

fa = y

⊢

Infa s

subst y

s₀ :

listfact

ss :

listlistfact

s :

listfact

fa :

H₀ :

Infa s₀

Hall :

∀x : listfact, Inx ss → existsbfact_eqbfa x = true

Hs :

Ins ss

Hy :

Infa s

⊢

Infa s

exact Hy

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold evidence_meet

intros | s₀ ss s fa H Hs ; destruct H |

apply filter_In in H as H₀ Hall

destruct Hs as ← | Hs ; exact H₀ |

rewrite forallb_forall in Hall

pose proof Halls Hs as Ex

apply existsb_exists in Ex as y & Hy & E

apply fact_eqb_eq in E

subst y

exact Hy

A taken edge t from the block from (edge_step) changes neither memory nor temporaries; it leaves the frame at the entry of t's label, entered from from.

483Lemma edge_step_next

∀ c from t c′

edge_stepc from t = Nextc′

c_memc′ = c_memc ∧ fr_envc_framec′ = fr_envc_framec ∧ fr_atc_framec′ = Enteredge_labelt Somefrom

Explore proof 3 tactics

Initial goal

⊢

∀c : config from : name t : target c′ : config, edge_stepc from t = Nextc′ → c_memc′ = c_memc ∧ fr_envc_framec′ = fr_envc_framec ∧ fr_atc_framec′ = Enteredge_labelt Somefrom

unfold edge_step

⊢

∀ c : config from : name t : target c′ : config ,

match t with

To_

⇒

Nextcontinue_atc with_pointc_framec Enteredge_labelt Somefrom c_memc c_fuelc

Poll_

⇒

match fr_doomedc_framec with

Somewhy

⇒

DoneUncheckedAheadwhy

None

⇒

Nextcontinue_atc with_pointc_framec Enteredge_labelt Somefrom c_memc c_fuelc

Nextc′

→

c_memc′ = c_memc ∧ fr_envc_framec′ = fr_envc_framec ∧ fr_atc_framec′ = Enteredge_labelt Somefrom

intros c from t c′ H

c :

from :

t :

c′ :

H :

match t with

To_

⇒

Nextcontinue_atc with_pointc_framec Enteredge_labelt Somefrom c_memc c_fuelc

Poll_

⇒

match fr_doomedc_framec with

Somewhy

⇒

DoneUncheckedAheadwhy

None

⇒

Nextcontinue_atc with_pointc_framec Enteredge_labelt Somefrom c_memc c_fuelc

Nextc′

⊢

c_memc′ = c_memc ∧ fr_envc_framec′ = fr_envc_framec ∧ fr_atc_framec′ = Enteredge_labelt Somefrom

destruct t , fr_doomedc_framec ; try discriminate H ; injection H as ← ; auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold edge_step

intros c from t c′ H

destruct t , fr_doomedc_framec ; try discriminate H ; injection H as ← ; auto

Entering the block l from pred runs its phis on what the edge left: memory is unchanged, and the frame goes on to the block's instructions and jump.

495Lemma enter_step

∀ ge c l pred c′

fr_atc_framec = Enterl Somepred

stepge c = Nextc′

c_memc′ = c_memc ∧ ∃b, find_blockl fn_blocksfr_fnc_framec = Someb ∧ phis_envge b_phisb Somepred fr_envc_framec = Somefr_envc_framec′ ∧ fr_atc_framec′ = Execl b_instsb b_jumpb

Explore proof 12 tactics

Initial goal

⊢

∀ge : genv c : config l pred : name c′ : config, fr_atc_framec = Enterl Somepred → stepge c = Nextc′ → c_memc′ = c_memc ∧ ∃b : block, find_blockl fn_blocksfr_fnc_framec = Someb ∧ phis_envge b_phisb Somepred fr_envc_framec = Somefr_envc_framec′ ∧ fr_atc_framec′ = Execl b_instsb b_jumpb

intros ge c l pred c′ Ha H

ge :

c :

l, pred :

c′ :

Ha :

fr_atc_framec = Enterl Somepred

H :

stepge c = Nextc′

⊢

c_memc′ = c_memc ∧ ∃b : block, find_blockl fn_blocksfr_fnc_framec = Someb ∧ phis_envge b_phisb Somepred fr_envc_framec = Somefr_envc_framec′ ∧ fr_atc_framec′ = Execl b_instsb b_jumpb

unfold step in H

ge :

c :

l, pred :

c′ :

Ha :

fr_atc_framec = Enterl Somepred

H :

match fr_atc_framec with

Snapshot[ ] l

⇒

Nextc_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ 0; ptr_cap ≔ CNone fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc

Snapshot_ :: _ as xs l

⇒

negbforallbsnapshot_word xs

→

Stuck"snapshot"

else

Freshheap_req16 8 × Z.of_natDatatypes.lengthxs λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesxs base allocatedc_memc heap_req16 8 × Z.of_natDatatypes.lengthxs base; c_fuel ≔ c_fuelc

Enterl from

⇒

c_fuelc =? 0

→

DoneOutOfFuel

else

or_stuck"block"

let* b ≔ find_blockl fn_blocksfr_fnc_framec in

let* e ≔ phis_envge b_phisb from fr_envc_framec in

SomeNextc_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc − 1

Execl [ ] j

⇒

jump_stepge c l j

Execl i :: rest j

⇒

match let* why ≔ fr_doomedc_framec in if ahead_transparenti then None else Somewhy with

Somewhy

⇒

DoneUncheckedAheadwhy

None

⇒

or_stuck"instruction"

let* out₀ ≔ inst_stepge c_framec c_memc i in

let* od ≔ doomed_resultge c_framec c_memc i out₀ in

Someinst_nextc l rest j fstod sndod

Nextc′

⊢

c_memc′ = c_memc ∧ ∃b : block, find_blockl fn_blocksfr_fnc_framec = Someb ∧ phis_envge b_phisb Somepred fr_envc_framec = Somefr_envc_framec′ ∧ fr_atc_framec′ = Execl b_instsb b_jumpb

rewrite Ha in H

ge :

c :

l, pred :

c′ :

Ha :

fr_atc_framec = Enterl Somepred

H :

c_fuelc =? 0

→

DoneOutOfFuel

else

or_stuck"block"

let* b ≔ find_blockl fn_blocksfr_fnc_framec in

let* e ≔ phis_envge b_phisb Somepred fr_envc_framec in

Nextc′

⊢

c_memc′ = c_memc ∧ ∃b : block, find_blockl fn_blocksfr_fnc_framec = Someb ∧ phis_envge b_phisb Somepred fr_envc_framec = Somefr_envc_framec′ ∧ fr_atc_framec′ = Execl b_instsb b_jumpb

destruct c_fuelc =? 0 ; discriminate H |

ge :

c :

l, pred :

c′ :

Ha :

fr_atc_framec = Enterl Somepred

H :

or_stuck"block"

let* b ≔ find_blockl fn_blocksfr_fnc_framec in

let* e ≔ phis_envge b_phisb Somepred fr_envc_framec in

Nextc′

⊢

c_memc′ = c_memc ∧ ∃b : block, find_blockl fn_blocksfr_fnc_framec = Someb ∧ phis_envge b_phisb Somepred fr_envc_framec = Somefr_envc_framec′ ∧ fr_atc_framec′ = Execl b_instsb b_jumpb

apply or_stuck_next in H

ge :

c :

l, pred :

c′ :

Ha :

fr_atc_framec = Enterl Somepred

H :

let* b ≔ find_blockl fn_blocksfr_fnc_framec in

let* e ≔ phis_envge b_phisb Somepred fr_envc_framec in

SomeNextc′

⊢

c_memc′ = c_memc ∧ ∃b : block, find_blockl fn_blocksfr_fnc_framec = Someb ∧ phis_envge b_phisb Somepred fr_envc_framec = Somefr_envc_framec′ ∧ fr_atc_framec′ = Execl b_instsb b_jumpb

destruct find_block_ _ as b | ; simpl in H ; | discriminate H

ge :

c :

l, pred :

c′ :

Ha :

fr_atc_framec = Enterl Somepred

b :

H :

let* e ≔

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge fr_envc_framec k v in

Someputd x e

SomeNextc′

⊢

c_memc′ = c_memc ∧ ∃b₀ : block, Someb = Someb₀ ∧ phis_envge b_phisb₀ Somepred fr_envc_framec = Somefr_envc_framec′ ∧ fr_atc_framec′ = Execl b_instsb₀ b_jumpb₀

destruct phis_envge b_phisb Somepred fr_envc_framec as e | eqn: Ep ; unfold phis_env in Ep ; rewrite Ep in H ; simpl in H ; | discriminate H

ge :

c :

l, pred :

c′ :

Ha :

fr_atc_framec = Enterl Somepred

b :

e :

H :

Ep :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge fr_envc_framec k v in

Someputd x e

Somee

⊢

c_memc′ = c_memc ∧ ∃b₀ : block, Someb = Someb₀ ∧ phis_envge b_phisb₀ Somepred fr_envc_framec = Somefr_envc_framec′ ∧ fr_atc_framec′ = Execl b_instsb₀ b_jumpb₀

injection H as ←

ge :

c :

l, pred :

Ha :

fr_atc_framec = Enterl Somepred

b :

e :

Ep :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge fr_envc_framec k v in

Someputd x e

Somee

⊢

c_memc_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc − 1 = c_memc ∧ ∃b₀ : block, Someb = Someb₀ ∧ phis_envge b_phisb₀ Somepred fr_envc_framec = Somefr_envc_framec_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc − 1 ∧ fr_atc_framec_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc − 1 = Execl b_instsb₀ b_jumpb₀

simpl

ge :

c :

l, pred :

Ha :

fr_atc_framec = Enterl Somepred

b :

e :

Ep :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge fr_envc_framec k v in

Someputd x e

Somee

⊢

c_memc = c_memc

∧

∃ b₀ : block ,

Someb = Someb₀

∧

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e₀ ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge fr_envc_framec k v in

Someputd x e₀

b_phisb₀

Somee

∧

Execl b_instsb b_jumpb = Execl b_instsb₀ b_jumpb₀

split ; reflexivity |

ge :

c :

l, pred :

Ha :

fr_atc_framec = Enterl Somepred

b :

e :

Ep :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge fr_envc_framec k v in

Someputd x e

Somee

⊢

∃ b₀ : block ,

Someb = Someb₀

∧

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e₀ ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge fr_envc_framec k v in

Someputd x e₀

b_phisb₀

Somee

∧

Execl b_instsb b_jumpb = Execl b_instsb₀ b_jumpb₀

exists b

ge :

c :

l, pred :

Ha :

fr_atc_framec = Enterl Somepred

b :

e :

Ep :

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge fr_envc_framec k v in

Someputd x e

Somee

⊢

Someb = Someb

∧

fold_left

λ acc : optionlistname × word ph : phi ⇒

let* e₀ ≔ acc in

match ph with

Phid k pairs

⇒

let* v ≔ lookuppred pairs in

let* x ≔ value_xge fr_envc_framec k v in

Someputd x e₀

Somee

∧

Execl b_instsb b_jumpb = Execl b_instsb b_jumpb

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros ge c l pred c′ Ha H

unfold step in H

rewrite Ha in H

destruct c_fuelc =? 0 ; discriminate H |

apply or_stuck_next in H

destruct find_block_ _ as b | ; simpl in H ; | discriminate H

destruct phis_envge b_phisb Somepred fr_envc_framec as e | eqn: Ep ; unfold phis_env in Ep ; rewrite Ep in H ; simpl in H ; | discriminate H

injection H as ←

simpl

split ; reflexivity |

exists b

auto

Where the facts fs hold as a block is left by the edge t (edge_step), and fs is one of the sets the pass meets at the entry of t's block b, the pass's entry facts of b (entry_kill of the meet) hold once its phis have run.

514Theorem entry_holds

∀ ge c c₁ c₂ from t sets fs b

edge_stepc from t = Nextc₁

stepge c₁ = Nextc₂

find_blockedge_labelt fn_blocksfr_fnc_framec₁ = Someb

Infs sets

facts_holdge c_memc₂ fr_envc_framec₂ entry_killb_phisb evidence_meetsets

Explore proof 11 tactics

Initial goal

⊢

∀ge : genv c c₁ c₂ : config from : name t : target sets : listlistfact fs : listfact b : block, edge_stepc from t = Nextc₁ → stepge c₁ = Nextc₂ → find_blockedge_labelt fn_blocksfr_fnc_framec₁ = Someb → facts_holdge c_memc fr_envc_framec fs → Infs sets → facts_holdge c_memc₂ fr_envc_framec₂ entry_killb_phisb evidence_meetsets

intros ge c c₁ c₂ from t sets fs b He Hs Hb H Hin

ge :

c, c₁, c₂ :

from :

t :

sets :

listlistfact

fs :

listfact

b :

He :

edge_stepc from t = Nextc₁

Hs :

stepge c₁ = Nextc₂

Hb :

find_blockedge_labelt fn_blocksfr_fnc_framec₁ = Someb

H :

Hin :

Infs sets

⊢

facts_holdge c_memc₂ fr_envc_framec₂ entry_killb_phisb evidence_meetsets

destruct edge_step_next_ _ _ _ He as Hm₁ & He₁ & Ha₁

ge :

c, c₁, c₂ :

from :

t :

sets :

listlistfact

fs :

listfact

b :

He :

edge_stepc from t = Nextc₁

Hs :

stepge c₁ = Nextc₂

Hb :

find_blockedge_labelt fn_blocksfr_fnc_framec₁ = Someb

H :

Hin :

Infs sets

Hm₁ :

c_memc₁ = c_memc

He₁ :

Ha₁ :

fr_atc_framec₁ = Enteredge_labelt Somefrom

⊢

facts_holdge c_memc₂ fr_envc_framec₂ entry_killb_phisb evidence_meetsets

destruct enter_step_ _ _ _ _ Ha₁ Hs as Hm₂ & b′ & Hb′ & Hp & _

ge :

c, c₁, c₂ :

from :

t :

sets :

listlistfact

fs :

listfact

b :

He :

edge_stepc from t = Nextc₁

Hs :

stepge c₁ = Nextc₂

Hb :

find_blockedge_labelt fn_blocksfr_fnc_framec₁ = Someb

H :

Hin :

Infs sets

Hm₁ :

c_memc₁ = c_memc

He₁ :

Ha₁ :

fr_atc_framec₁ = Enteredge_labelt Somefrom

Hm₂ :

c_memc₂ = c_memc₁

b′ :

Hb′ :

find_blockedge_labelt fn_blocksfr_fnc_framec₁ = Someb′

Hp :

phis_envge b_phisb′ Somefrom fr_envc_framec₁ = Somefr_envc_framec₂

⊢

facts_holdge c_memc₂ fr_envc_framec₂ entry_killb_phisb evidence_meetsets

rewrite Hb in Hb′

ge :

c, c₁, c₂ :

from :

t :

sets :

listlistfact

fs :

listfact

b :

He :

edge_stepc from t = Nextc₁

Hs :

stepge c₁ = Nextc₂

Hb :

find_blockedge_labelt fn_blocksfr_fnc_framec₁ = Someb

H :

Hin :

Infs sets

Hm₁ :

c_memc₁ = c_memc

He₁ :

Ha₁ :

fr_atc_framec₁ = Enteredge_labelt Somefrom

Hm₂ :

c_memc₂ = c_memc₁

b′ :

Hb′ :

Someb = Someb′

Hp :

phis_envge b_phisb′ Somefrom fr_envc_framec₁ = Somefr_envc_framec₂

⊢

facts_holdge c_memc₂ fr_envc_framec₂ entry_killb_phisb evidence_meetsets

injection Hb′ as ←

ge :

c, c₁, c₂ :

from :

t :

sets :

listlistfact

fs :

listfact

b :

He :

edge_stepc from t = Nextc₁

Hs :

stepge c₁ = Nextc₂

Hb :

find_blockedge_labelt fn_blocksfr_fnc_framec₁ = Someb

H :

Hin :

Infs sets

Hm₁ :

c_memc₁ = c_memc

He₁ :

Ha₁ :

fr_atc_framec₁ = Enteredge_labelt Somefrom

Hm₂ :

c_memc₂ = c_memc₁

Hp :

phis_envge b_phisb Somefrom fr_envc_framec₁ = Somefr_envc_framec₂

⊢

facts_holdge c_memc₂ fr_envc_framec₂ entry_killb_phisb evidence_meetsets

rewrite Hm₂ , Hm₁

ge :

c, c₁, c₂ :

from :

t :

sets :

listlistfact

fs :

listfact

b :

He :

edge_stepc from t = Nextc₁

Hs :

stepge c₁ = Nextc₂

Hb :

find_blockedge_labelt fn_blocksfr_fnc_framec₁ = Someb

H :

Hin :

Infs sets

Hm₁ :

c_memc₁ = c_memc

He₁ :

Ha₁ :

fr_atc_framec₁ = Enteredge_labelt Somefrom

Hm₂ :

c_memc₂ = c_memc₁

Hp :

phis_envge b_phisb Somefrom fr_envc_framec₁ = Somefr_envc_framec₂

⊢

facts_holdge c_memc fr_envc_framec₂ entry_killb_phisb evidence_meetsets

eapply phis_facts_hold ; exact Hp |

ge :

c, c₁, c₂ :

from :

t :

sets :

listlistfact

fs :

listfact

b :

He :

edge_stepc from t = Nextc₁

Hs :

stepge c₁ = Nextc₂

Hb :

find_blockedge_labelt fn_blocksfr_fnc_framec₁ = Someb

H :

Hin :

Infs sets

Hm₁ :

c_memc₁ = c_memc

He₁ :

Ha₁ :

fr_atc_framec₁ = Enteredge_labelt Somefrom

Hm₂ :

c_memc₂ = c_memc₁

Hp :

phis_envge b_phisb Somefrom fr_envc_framec₁ = Somefr_envc_framec₂

⊢

facts_holdge c_memc fr_envc_framec₁ evidence_meetsets

rewrite He₁

ge :

c, c₁, c₂ :

from :

t :

sets :

listlistfact

fs :

listfact

b :

He :

edge_stepc from t = Nextc₁

Hs :

stepge c₁ = Nextc₂

Hb :

find_blockedge_labelt fn_blocksfr_fnc_framec₁ = Someb

H :

Hin :

Infs sets

Hm₁ :

c_memc₁ = c_memc

He₁ :

Ha₁ :

fr_atc_framec₁ = Enteredge_labelt Somefrom

Hm₂ :

c_memc₂ = c_memc₁

Hp :

phis_envge b_phisb Somefrom fr_envc_framec₁ = Somefr_envc_framec₂

⊢

facts_holdge c_memc fr_envc_framec evidence_meetsets

intros fa Hfa

ge :

c, c₁, c₂ :

from :

t :

sets :

listlistfact

fs :

listfact

b :

He :

edge_stepc from t = Nextc₁

Hs :

stepge c₁ = Nextc₂

Hb :

find_blockedge_labelt fn_blocksfr_fnc_framec₁ = Someb

H :

Hin :

Infs sets

Hm₁ :

c_memc₁ = c_memc

He₁ :

Ha₁ :

fr_atc_framec₁ = Enteredge_labelt Somefrom

Hm₂ :

c_memc₂ = c_memc₁

Hp :

phis_envge b_phisb Somefrom fr_envc_framec₁ = Somefr_envc_framec₂

fa :

Hfa :

Infa evidence_meetsets

⊢

fact_holdsge c_memc fr_envc_framec fa

apply H

ge :

c, c₁, c₂ :

from :

t :

sets :

listlistfact

fs :

listfact

b :

He :

edge_stepc from t = Nextc₁

Hs :

stepge c₁ = Nextc₂

Hb :

find_blockedge_labelt fn_blocksfr_fnc_framec₁ = Someb

H :

Hin :

Infs sets

Hm₁ :

c_memc₁ = c_memc

He₁ :

Ha₁ :

fr_atc_framec₁ = Enteredge_labelt Somefrom

Hm₂ :

c_memc₂ = c_memc₁

Hp :

phis_envge b_phisb Somefrom fr_envc_framec₁ = Somefr_envc_framec₂

fa :

Hfa :

Infa evidence_meetsets

⊢

Infa fs

eapply evidence_meet_in ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros ge c c₁ c₂ from t sets fs b He Hs Hb H Hin

destruct edge_step_next_ _ _ _ He as Hm₁ & He₁ & Ha₁

destruct enter_step_ _ _ _ _ Ha₁ Hs as Hm₂ & b′ & Hb′ & Hp & _

rewrite Hb in Hb′

injection Hb′ as ←

rewrite Hm₂ , Hm₁

eapply phis_facts_hold ; exact Hp |

rewrite He₁

intros fa Hfa

apply H

eapply evidence_meet_in ; eauto

The pass, instruction by instruction

checked_inst_rest/7 takes the check-like instructions together with the access they are checked for, ends the facts at a check_local or check_function, and otherwise keeps evidence_after/3 of the facts (or kills a repeated getter's temporary). pass_special names the instructions it treats apart; generic_rest is its last case, copied.

The instructions checked_inst_rest/7 treats apart: a check_local, a check_function, and every check-like op (check_fact).

540Definition pass_speciali : inst : bool ≔

match i with

Let_ A CheckLocal_ _ _ _ _ [ ] | Let_ F CheckFunction _

⇒

true

⇒

match check_facti with

Some_

⇒

true

None

⇒

false

The last case of checked_inst_rest/7, copied for the proof. It gives the facts after the instruction i (evidence_after, or a repeated gettergetter Fil-CA getter is the function that returns a global's or function's address with its capability, initializing it on first use. Upstream every symbol is renamed pizlonated_ plus its name, and that symbol is its getter, returning a flight pointer; the program checks the result like any pointer. In IR a getter call is let(tmp(D), p, copy, [global(G)]); calling one is a safepoint (filc_amd64:object_getter//2), so it ends every live fact, except a repeated getter.'s temporary killed) and accepts i unless i is a raw access with no live fact of its operand that covers it (covered_access or hull_covered), a raw call, a call through a temporary, or pointer arithmetic or a pointer copy outside a flight.

553Definition generic_rests : src i : inst rest : listinst live : listfact : optionlistinst × listfact ≔

let once ≔ s_onces in

let live′ ≔

match i with

⇒

match lookupd s_getterss with

Someg₁

⇒

name_eqbg₁ g

→

killd live

else

None

⇒

⇒

let ok ≔

match raw_accessi with

Someq, x, _, _

⇒

match fact_ofq live with

Somefa

⇒

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live once

None

⇒

false

None

⇒

match i with

RawCall_ _ _

⇒

false

Touch_

⇒

false

not right after its check

Call_ Tmp_ _

⇒

false

unchecked_access

Let_ P Add | Sub | Itop _

⇒

false

implicit_flight

Let_ P Copy Tmp_ | Let_ P Copy Const_

⇒

false

⇒

true

→

Somerest, live′

else

None

For an instruction it does not treat apart, checked_inst_rest/7 is generic_rest, by computation. So Validate.v, the transcription the gates compare, needs no refactoring for the proof.

589Lemma checked_inst_rest_generic

∀ s i rest live

pass_speciali = false

checked_inst_rests i rest live = generic_rests i rest live

Explore proof 3 tactics

Initial goal

⊢

∀s : src i : inst rest : listinst live : listfact, pass_speciali = false → checked_inst_rests i rest live = generic_rests i rest live

intros s i rest live H

s :

i :

rest :

listinst

live :

listfact

H :

pass_speciali = false

⊢

checked_inst_rests i rest live = generic_rests i rest live

destruct i as q k o args | | | | | | | | ; try reflexivity

s :

q :

k :

o :

args :

listvalue

rest :

listinst

live :

listfact

H :

pass_specialLetq k o args = false

⊢

checked_inst_rests Letq k o args rest live = generic_rests Letq k o args rest live

destruct k ; try reflexivity ; destruct o ; try reflexivity ; destruct args as | a₁ | a₂ | a₃ | a₄ args ; try reflexivity ; discriminate H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros s i rest live H

destruct k ; try reflexivity ; destruct o ; try reflexivity ; destruct args as | a₁ | a₂ | a₃ | a₄ args ; try reflexivity ; discriminate H

What generic_rest answers: the same remaining instructions; the facts evidence_after keeps, or a getter copy's temporary killed; and, for a raw access through q, a live fact of q that covers it by covered_access or hull_covered.

601Lemma generic_rest_shape

∀ s i rest live rest′ live′

generic_rests i rest live = Somerest′, live′

rest′ = rest ∧ live′ = evidence_afteri live ∨ ∃d g, i = Letd P Copy Globalg ∧ live′ = killd live ∧ ∀q x off need, raw_accessi = Someq, x, off, need → ∃fa, fact_ofq live = Somefa ∧ covered_accessi q f_lofa f_hifa f_rfa f_alfa = true ∨ hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

Explore proof 19 tactics

Initial goal

⊢

∀s : src i : inst rest : listinst live : listfact rest′ : listinst live′ : listfact, generic_rests i rest live = Somerest′, live′ → rest′ = rest ∧ live′ = evidence_afteri live ∨ ∃d g : name, i = Letd P Copy Globalg ∧ live′ = killd live ∧ ∀q : name x : access_type off : Z need : rights, raw_accessi = Someq, x, off, need → ∃fa : fact, fact_ofq live = Somefa ∧ covered_accessi q f_lofa f_hifa f_rfa f_alfa = true ∨ hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

unfold generic_rest

⊢

∀ s : src i : inst rest : listinst live : listfact rest′ : listinst live′ : listfact ,

match raw_accessi with

Someq, x, _, _

⇒

match fact_ofq live with

Somefa

⇒

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

None

⇒

match i with

⇒

false

⇒

true

→

Some

rest

match i with

⇒

match lookupd s_getterss with

Someg₁

⇒

name_eqbg₁ g

→

killd live

else

None

⇒

Letd P Copy Globalg :: _ :: _

⇒

⇒

⇒

else

None

Somerest′, live′

→

rest′ = rest ∧ live′ = evidence_afteri live ∨ ∃d g : name, i = Letd P Copy Globalg ∧ live′ = killd live ∧ ∀q : name x : access_type off : Z need : rights, raw_accessi = Someq, x, off, need → ∃fa : fact, fact_ofq live = Somefa ∧ covered_accessi q f_lofa f_hifa f_rfa f_alfa = true ∨ hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

intros s i rest live rest′ live′ H

s :

i :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

match raw_accessi with

Someq, x, _, _

⇒

match fact_ofq live with

Somefa

⇒

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

None

⇒

match i with

⇒

false

⇒

true

→

Some

rest

match i with

⇒

match lookupd s_getterss with

Someg₁

⇒

name_eqbg₁ g

→

killd live

else

None

⇒

Letd P Copy Globalg :: _ :: _

⇒

⇒

⇒

else

None

Somerest′, live′

⊢

cbn zeta in H

s :

i :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

match raw_accessi with

Someq, x, _, _

⇒

match fact_ofq live with

Somefa

⇒

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

None

⇒

match i with

⇒

false

⇒

true

→

Some

rest

match i with

⇒

match lookupd s_getterss with

Someg₁

⇒

name_eqbg₁ g

→

killd live

else

None

⇒

Letd P Copy Globalg :: _ :: _

⇒

⇒

⇒

else

None

Somerest′, live′

⊢

match type of H withif ?b then _ else _ = _⇒destruct b eqn: Hok ; | discriminate Hend

s :

i :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

Hok :

match raw_accessi with

Someq, x, _, _

⇒

match fact_ofq live with

Somefa

⇒

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

None

⇒

match i with

⇒

false

⇒

true

H :

Some

rest

match i with

⇒

match lookupd s_getterss with

Someg₁

⇒

name_eqbg₁ g

→

killd live

else

None

⇒

Letd P Copy Globalg :: _ :: _

⇒

⇒

⇒

Somerest′, live′

⊢

injection H as ← ←

s :

i :

rest :

listinst

live :

listfact

Hok :

match raw_accessi with

Someq, x, _, _

⇒

match fact_ofq live with

Somefa

⇒

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

None

⇒

match i with

⇒

false

⇒

true

⊢

rest = rest

∧

match i with

⇒

match lookupd s_getterss with

Someg₁

⇒

name_eqbg₁ g

→

killd live

else

None

⇒

Letd P Copy Globalg :: _ :: _

⇒

⇒

⇒

∨

∃ d g : name ,

i = Letd P Copy Globalg

∧

match i with

Letd₀ P Copy Globalg₀

⇒

match lookupd₀ s_getterss with

Someg₁

⇒

name_eqbg₁ g₀

→

killd₀ live

else

None

⇒

Letd₀ P Copy Globalg₀ :: _ :: _

⇒

⇒

⇒

killd live

∧

∀q : name x : access_type off : Z need : rights, raw_accessi = Someq, x, off, need → ∃fa : fact, fact_ofq live = Somefa ∧ covered_accessi q f_lofa f_hifa f_rfa f_alfa = true ∨ hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

split ; reflexivity |

s :

i :

rest :

listinst

live :

listfact

Hok :

match raw_accessi with

Someq, x, _, _

⇒

match fact_ofq live with

Somefa

⇒

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

None

⇒

match i with

⇒

false

⇒

true

⊢

match i with

⇒

match lookupd s_getterss with

Someg₁

⇒

name_eqbg₁ g

→

killd live

else

None

⇒

Letd P Copy Globalg :: _ :: _

⇒

⇒

⇒

∨

∃ d g : name ,

i = Letd P Copy Globalg

∧

match i with

Letd₀ P Copy Globalg₀

⇒

match lookupd₀ s_getterss with

Someg₁

⇒

name_eqbg₁ g₀

→

killd₀ live

else

None

⇒

Letd₀ P Copy Globalg₀ :: _ :: _

⇒

⇒

⇒

killd live

∧

split

2 open

s :

i :

rest :

listinst

live :

listfact

Hok :

match raw_accessi with

Someq, x, _, _

⇒

match fact_ofq live with

Somefa

⇒

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

None

⇒

match i with

⇒

false

⇒

true

⊢

match i with

⇒

match lookupd s_getterss with

Someg₁

⇒

name_eqbg₁ g

→

killd live

else

None

⇒

Letd P Copy Globalg :: _ :: _

⇒

⇒

⇒

∨

∃ d g : name ,

i = Letd P Copy Globalg

∧

match i with

Letd₀ P Copy Globalg₀

⇒

match lookupd₀ s_getterss with

Someg₁

⇒

name_eqbg₁ g₀

→

killd₀ live

else

None

⇒

Letd₀ P Copy Globalg₀ :: _ :: _

⇒

⇒

⇒

killd live

focused goal

s :

i :

rest :

listinst

live :

listfact

Hok :

match raw_accessi with

Someq, x, _, _

⇒

match fact_ofq live with

Somefa

⇒

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

None

⇒

match i with

⇒

false

⇒

true

⊢

–destruct i as d k o args | | | | | | | | ; auto

2 open

s :

d :

k :

o :

args :

listvalue

rest :

listinst

live :

listfact

Hok :

match raw_accessLetd k o args with

Someq, x, _, _

⇒

reusing_accessLetd k o args x

match fact_ofq live with

Somefa

⇒

covered_accessLetd k o args q f_lofa f_hifa f_rfa f_alfa || hull_coveredLetd k o args q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

None

⇒

match k with

⇒

match o with

Copy

⇒

match args with

Tmp_ | Const_

⇒

false

⇒

true

Add | Sub | Itop

⇒

false

⇒

true

⇒

true

⊢

match k with

⇒

match o with

Copy

⇒

match args with

Globalg

⇒

match lookupd s_getterss with

Someg₁

⇒

name_eqbg₁ g

→

killd live

else

evidence_afterLetd k o args live

None

⇒

evidence_afterLetd k o args live

Globalg :: _ :: _

⇒

evidence_afterLetd k o args live

⇒

evidence_afterLetd k o args live

⇒

evidence_afterLetd k o args live

⇒

evidence_afterLetd k o args live

∨

∃ d₀ g : name ,

Letd k o args = Letd₀ P Copy Globalg

∧

match k with

⇒

match o with

Copy

⇒

match args with

Globalg₀

⇒

match lookupd s_getterss with

Someg₁

⇒

name_eqbg₁ g₀

→

killd live

else

evidence_afterLetd k o args live

None

⇒

evidence_afterLetd k o args live

Globalg₀ :: _ :: _

⇒

evidence_afterLetd k o args live

⇒

evidence_afterLetd k o args live

⇒

evidence_afterLetd k o args live

⇒

evidence_afterLetd k o args live

killd₀ live

deferred goal

s :

i :

rest :

listinst

live :

listfact

Hok :

match raw_accessi with

Someq, x, _, _

⇒

match fact_ofq live with

Somefa

⇒

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

None

⇒

match i with

⇒

false

⇒

true

⊢

destruct k , o ; auto ; destruct args as | n | c | g | a₂ args ; auto

2 open

s :

d, g :

rest :

listinst

live :

listfact

Hok :

match raw_accessLetd P Copy Globalg with

Someq, x, _, _

⇒

reusing_accessLetd P Copy Globalg x

match fact_ofq live with

Somefa

⇒

covered_accessLetd P Copy Globalg q f_lofa f_hifa f_rfa f_alfa || hull_coveredLetd P Copy Globalg q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

None

⇒

true

⊢

match lookupd s_getterss with

Someg₁

⇒

name_eqbg₁ g

→

killd live

else

None

⇒

∨

∃ d₀ g₀ : name ,

Letd P Copy Globalg = Letd₀ P Copy Globalg₀

∧

match lookupd s_getterss with

Someg₁

⇒

name_eqbg₁ g

→

killd live

else

None

⇒

killd₀ live

deferred goal

s :

i :

rest :

listinst

live :

listfact

Hok :

match raw_accessi with

Someq, x, _, _

⇒

match fact_ofq live with

Somefa

⇒

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

None

⇒

match i with

⇒

false

⇒

true

⊢

destruct lookupd s_getterss ; auto

2 open

s :

d, g :

rest :

listinst

live :

listfact

Hok :

match raw_accessLetd P Copy Globalg with

Someq, x, _, _

⇒

reusing_accessLetd P Copy Globalg x

match fact_ofq live with

Somefa

⇒

covered_accessLetd P Copy Globalg q f_lofa f_hifa f_rfa f_alfa || hull_coveredLetd P Copy Globalg q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

None

⇒

true

n :

⊢

name_eqbn g

→

killd live

else

∨

∃ d₀ g₀ : name ,

Letd P Copy Globalg = Letd₀ P Copy Globalg₀

∧

name_eqbn g

→

killd live

else

killd₀ live

deferred goal

s :

i :

rest :

listinst

live :

listfact

Hok :

match raw_accessi with

Someq, x, _, _

⇒

match fact_ofq live with

Somefa

⇒

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

None

⇒

match i with

⇒

false

⇒

true

⊢

destruct name_eqb_ _ ; eauto

deferred goal

s :

i :

rest :

listinst

live :

listfact

Hok :

match raw_accessi with

Someq, x, _, _

⇒

match fact_ofq live with

Somefa

⇒

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

None

⇒

match i with

⇒

false

⇒

true

⊢

–intros q x off need Hr

s :

i :

rest :

listinst

live :

listfact

Hok :

match raw_accessi with

Someq, x, _, _

⇒

match fact_ofq live with

Somefa

⇒

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

None

⇒

match i with

⇒

false

⇒

true

q :

x :

off :

need :

Hr :

raw_accessi = Someq, x, off, need

⊢

∃fa : fact, fact_ofq live = Somefa ∧ covered_accessi q f_lofa f_hifa f_rfa f_alfa = true ∨ hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

rewrite Hr in Hok

s :

i :

rest :

listinst

live :

listfact

q :

x :

Hok :

match fact_ofq live with

Somefa

⇒

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

true

off :

need :

Hr :

raw_accessi = Someq, x, off, need

⊢

∃fa : fact, fact_ofq live = Somefa ∧ covered_accessi q f_lofa f_hifa f_rfa f_alfa = true ∨ hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

apply andb_true_iff in Hok as _ Hok

s :

i :

rest :

listinst

live :

listfact

q :

x :

Hok :

match fact_ofq live with

Somefa

⇒

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces

None

⇒

false

true

off :

need :

Hr :

raw_accessi = Someq, x, off, need

⊢

∃fa : fact, fact_ofq live = Somefa ∧ covered_accessi q f_lofa f_hifa f_rfa f_alfa = true ∨ hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

destruct fact_ofq live as fa | ; | discriminate Hok

s :

i :

rest :

listinst

live :

listfact

q :

x :

fa :

Hok :

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

off :

need :

Hr :

raw_accessi = Someq, x, off, need

⊢

∃fa₀ : fact, Somefa = Somefa₀ ∧ covered_accessi q f_lofa₀ f_hifa₀ f_rfa₀ f_alfa₀ = true ∨ hull_coveredi q f_pfa₀ f_lofa₀ f_alfa₀ live s_onces = true

exists fa

s :

i :

rest :

listinst

live :

listfact

q :

x :

fa :

Hok :

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

off :

need :

Hr :

raw_accessi = Someq, x, off, need

⊢

Somefa = Somefa ∧ covered_accessi q f_lofa f_hifa f_rfa f_alfa = true ∨ hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

split ; reflexivity |

s :

i :

rest :

listinst

live :

listfact

q :

x :

fa :

Hok :

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

off :

need :

Hr :

raw_accessi = Someq, x, off, need

⊢

covered_accessi q f_lofa f_hifa f_rfa f_alfa = true ∨ hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

apply orb_true_iff

s :

i :

rest :

listinst

live :

listfact

q :

x :

fa :

Hok :

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

off :

need :

Hr :

raw_accessi = Someq, x, off, need

⊢

covered_accessi q f_lofa f_hifa f_rfa f_alfa || hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

exact Hok

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold generic_rest

intros s i rest live rest′ live′ H

cbn zeta in H

match type of H withif ?b then _ else _ = _⇒destruct b eqn: Hok ; | discriminate Hend

injection H as ← ←

split ; reflexivity |

split

destruct k , o ; auto ; destruct args as | n | c | g | a₂ args ; auto

destruct lookupd s_getterss ; auto

destruct name_eqb_ _ ; eauto

–intros q x off need Hr

rewrite Hr in Hok

apply andb_true_iff in Hok as _ Hok

destruct fact_ofq live as fa | ; | discriminate Hok

exists fa

split ; reflexivity |

apply orb_true_iff

exact Hok

A check-like instruction has an access range too.

622Lemma access_fact_some

∀ i fa

check_facti = Somefa

∃fb, access_facti = Somefb

Explore proof 3 tactics

Initial goal

⊢

∀i : inst fa : fact, check_facti = Somefa → ∃fb : fact, access_facti = Somefb

intros i fa H

i :

fa :

H :

check_facti = Somefa

⊢

∃fb : fact, access_facti = Somefb

destruct i as q k o args | | | | | | | | ; try discriminate H

q :

k :

o :

args :

listvalue

fa :

H :

check_factLetq k o args = Somefa

⊢

∃fb : fact, access_factLetq k o args = Somefb

destruct k , o ; try discriminate H ; destruct args as | a₁ | a₂ | a₃ | a₄ args ; simpl in * ; try discriminate H ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros i fa H

destruct k , o ; try discriminate H ; destruct args as | a₁ | a₂ | a₃ | a₄ args ; simpl in * ; try discriminate H ; eauto

The pass takes a check-like instruction i together with the next instruction, its access: the access must lie in i's range (proof_use, proof_use/6), and the facts after both are those evidence_after keeps across the access, from i's fact put before the facts kept across i.

634Lemma checked_inst_rest_check

∀ s i rest live rest′ live′ fa fb

check_facti = Somefa

access_facti = Somefb

checked_inst_rests i rest live = Somerest′, live′

∃access, rest = access :: rest′ ∧ proof_useaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true ∧ live′ = evidence_afteraccess fa :: evidence_afteri live

Explore proof 9 tactics

Initial goal

⊢

∀s : src i : inst rest : listinst live : listfact rest′ : listinst live′ : listfact fa fb : fact, check_facti = Somefa → access_facti = Somefb → checked_inst_rests i rest live = Somerest′, live′ → ∃access : inst, rest = access :: rest′ ∧ proof_useaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true ∧ live′ = evidence_afteraccess fa :: evidence_afteri live

intros s i rest live rest′ live′ fa fb Hf Hg H

s :

i :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

fa, fb :

Hf :

check_facti = Somefa

Hg :

access_facti = Somefb

H :

checked_inst_rests i rest live = Somerest′, live′

⊢

∃access : inst, rest = access :: rest′ ∧ proof_useaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true ∧ live′ = evidence_afteraccess fa :: evidence_afteri live

destruct i as q k o args | | | | | | | | ; try discriminate Hf

s :

q :

k :

o :

args :

listvalue

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

fa, fb :

Hf :

check_factLetq k o args = Somefa

Hg :

access_factLetq k o args = Somefb

H :

checked_inst_rests Letq k o args rest live = Somerest′, live′

⊢

∃access : inst, rest = access :: rest′ ∧ proof_useaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true ∧ live′ = evidence_afteraccess fa :: evidence_afterLetq k o args live

destruct k ; try destruct o ; discriminate Hf

s :

q :

o :

args :

listvalue

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

fa, fb :

Hf :

check_factLetq A o args = Somefa

Hg :

access_factLetq A o args = Somefb

H :

checked_inst_rests Letq A o args rest live = Somerest′, live′

⊢

∃access : inst, rest = access :: rest′ ∧ proof_useaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true ∧ live′ = evidence_afteraccess fa :: evidence_afterLetq A o args live

destruct o ; try discriminate Hf ; destruct args as | a₁ | a₂ | a₃ | a₄ args ; simpl in Hf , Hg ; try discriminate Hf ; injection Hf as ← ; injection Hg as ← ; cbn [ f_q f_p f_lo f_hi f_r f_al ]

7 open

s :

q :

lo, hi :

r :

align :

a₁ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

checked_inst_rests Letq A Checklo hi r align a₁ rest live = Somerest′, live′

⊢

∃access : inst, rest = access :: rest′ ∧ proof_useaccess q lo hi r align = true ∧ live′ = evidence_afteraccess f_q ≔ q; f_p ≔ a₁; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A Checklo hi r align a₁ live

focused goal

s :

q :

lo, hi :

r :

align, ahi :

a₁ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

checked_inst_rests Letq A CheckAheadlo hi r align ahi a₁ rest live = Somerest′, live′

⊢

∃access : inst, rest = access :: rest′ ∧ proof_useaccess q lo ahi r align = true ∧ live′ = evidence_afteraccess f_q ≔ q; f_p ≔ a₁; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A CheckAheadlo hi r align ahi a₁ live

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

checked_inst_rests Letq A Renewlo hi r align a₁; a₂ rest live = Somerest′, live′

⊢

∃access : inst, rest = access :: rest′ ∧ proof_useaccess q lo hi r align = true ∧ live′ = evidence_afteraccess f_q ≔ q; f_p ≔ a₂; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A Renewlo hi r align a₁; a₂ live

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂, a₃ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

checked_inst_rests Letq A RenewHulllo hi r align a₁; a₂; a₃ rest live = Somerest′, live′

⊢

∃access : inst, rest = access :: rest′ ∧ proof_useaccess q lo hi r align = true ∧ live′ = evidence_afteraccess f_q ≔ q; f_p ≔ a₃; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A RenewHulllo hi r align a₁; a₂; a₃ live

focused goal

s :

q :

b :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

checked_inst_rests Letq A HalfCheckb lo hi r align a₁; a₂ rest live = Somerest′, live′

⊢

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

checked_inst_rests Letq A RenewIflo hi r align a₁; a₂ rest live = Somerest′, live′

⊢

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

checked_inst_rests Letq A CheckLimitlo hi r align a₁; a₂ rest live = Somerest′, live′

⊢

all: unfold checked_inst_rest in H ; cbn zeta in H

7 open

s :

q :

lo, hi :

r :

align :

a₁ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

negbtrue

→

None

else

match rest with

[ ]

⇒

None

access :: rest′

⇒

proof_useaccess q lo hi r align

→

Somerest′, after_checkLetq A Checklo hi r align a₁ access q a₁ lo hi r align live

else

None

Somerest′, live′

⊢

focused goal

s :

q :

lo, hi :

r :

align, ahi :

a₁ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

negbmemq s_aheads

→

None

else

match rest with

[ ]

⇒

None

access :: rest′

⇒

proof_useaccess q lo ahi r align && ahead_transparentaccess

→

Somerest′, after_checkLetq A CheckAheadlo hi r align ahi a₁ access q a₁ lo hi r align live

else

None

Somerest′, live′

⊢

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

match a₁ with

Tmpn₁

⇒

match lookupn₁ s_renewss with

Somep₁, lo₁, hi₁, al₁

⇒

let* d ≔ pointer_distances_onces a₂ Tmpp₁ in

negblo₁ ≤? lo + d && hi + d ≤? hi₁ && al₁ mod align =? 0 && lo + d − lo₁ mod align =? 0

→

None

else

match rest with

[ ]

⇒

None

access :: rest′

⇒

proof_useaccess q lo hi r align

→

Somerest′, after_checkLetq A Renewlo hi r align a₁; a₂ access q a₂ lo hi r align live

else

None

⇒

None

⇒

None

Somerest′, live′

⊢

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂, a₃ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

negbhull_renewables_renewss s_onces a₃ lo hi align a₁ a₂

→

None

else

match rest with

[ ]

⇒

None

access :: rest′

⇒

proof_useaccess q lo hi r align

→

Somerest′, after_checkLetq A RenewHulllo hi r align a₁; a₂; a₃ access q a₃ lo hi r align live

else

None

Somerest′, live′

⊢

focused goal

s :

q :

b :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

negb

match a₁ with

Tmpn₁

⇒

match lookupn₁ s_renewss with

Somep₁, lo₁, hi₁, _

⇒

match pointer_distances_onces a₂ Tmpp₁ with

Somed₀

⇒

half_knownb lo hi d₀ lo₁ hi₁

None

⇒

false

None

⇒

false

⇒

false

→

None

else

match rest with

[ ]

⇒

None

access :: rest′

⇒

proof_useaccess q lo hi r align

→

Somerest′, after_checkLetq A HalfCheckb lo hi r align a₁; a₂ access q a₂ lo hi r align live

else

None

Somerest′, live′

⊢

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

negbguard_coverss_onces a₁ a₂ lo hi

→

None

else

match rest with

[ ]

⇒

None

access :: rest′

⇒

proof_useaccess q lo hi r align

→

Somerest′, after_checkLetq A RenewIflo hi r align a₁; a₂ access q a₁ lo hi r align live

else

None

Somerest′, live′

⊢

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

negblimit_coverss_onces a₁ a₂ lo hi

→

None

else

match rest with

[ ]

⇒

None

access :: rest′

⇒

proof_useaccess q lo hi r align

→

Somerest′, after_checkLetq A CheckLimitlo hi r align a₁; a₂ access q a₁ lo hi r align live

else

None

Somerest′, live′

⊢

all: repeat match type of H withcontext [match ?x with _ ⇒ _ end]⇒destruct x eqn :? ; try discriminate Hend

7 open

s :

q :

lo, hi :

r :

align :

a₁ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

Heqb :

negbtrue = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo hi r align = true

H :

Somel, after_checkLetq A Checklo hi r align a₁ i q a₁ lo hi r align live = Somerest′, live′

⊢

∃access : inst, i :: l = access :: rest′ ∧ proof_useaccess q lo hi r align = true ∧ live′ = evidence_afteraccess f_q ≔ q; f_p ≔ a₁; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A Checklo hi r align a₁ live

focused goal

s :

q :

lo, hi :

r :

align, ahi :

a₁ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

Heqb :

negbmemq s_aheads = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo ahi r align && ahead_transparenti = true

H :

Somel, after_checkLetq A CheckAheadlo hi r align ahi a₁ i q a₁ lo hi r align live = Somerest′, live′

⊢

∃access : inst, i :: l = access :: rest′ ∧ proof_useaccess q lo ahi r align = true ∧ live′ = evidence_afteraccess f_q ≔ q; f_p ≔ a₁; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A CheckAheadlo hi r align ahi a₁ live

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

n :

Heqv :

a₁ = Tmpn

p :

name × Z × Z × Z

p₀ :

name × Z × Z

z :

p₁ :

name × Z

z₀ :

n₀ :

z₁ :

Heqp₂ :

p₁ = n₀, z₁

Heqp₁ :

p₀ = n₀, z₁, z₀

Heqp₀ :

p = n₀, z₁, z₀, z

Heqo :

lookupn s_renewss = Somen₀, z₁, z₀, z

z₂ :

Heqo₀ :

pointer_distances_onces a₂ Tmpn₀ = Somez₂

Heqb :

negbz₁ ≤? lo + z₂ && hi + z₂ ≤? z₀ && z mod align =? 0 && lo + z₂ − z₁ mod align =? 0 = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo hi r align = true

H :

Somel, after_checkLetq A Renewlo hi r align Tmpn; a₂ i q a₂ lo hi r align live = Somerest′, live′

⊢

∃access : inst, i :: l = access :: rest′ ∧ proof_useaccess q lo hi r align = true ∧ live′ = evidence_afteraccess f_q ≔ q; f_p ≔ a₂; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A Renewlo hi r align Tmpn; a₂ live

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂, a₃ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

Heqb :

negbhull_renewables_renewss s_onces a₃ lo hi align a₁ a₂ = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo hi r align = true

H :

Somel, after_checkLetq A RenewHulllo hi r align a₁; a₂; a₃ i q a₃ lo hi r align live = Somerest′, live′

⊢

∃access : inst, i :: l = access :: rest′ ∧ proof_useaccess q lo hi r align = true ∧ live′ = evidence_afteraccess f_q ≔ q; f_p ≔ a₃; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A RenewHulllo hi r align a₁; a₂; a₃ live

focused goal

s :

q :

b :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

Heqb₀ :

negb

match a₁ with

Tmpn₁

⇒

match lookupn₁ s_renewss with

Somep₁, lo₁, hi₁, _

⇒

match pointer_distances_onces a₂ Tmpp₁ with

Somed₀

⇒

half_knownb lo hi d₀ lo₁ hi₁

None

⇒

false

None

⇒

false

⇒

false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₁ :

proof_usei q lo hi r align = true

H :

Somel, after_checkLetq A HalfCheckb lo hi r align a₁; a₂ i q a₂ lo hi r align live = Somerest′, live′

⊢

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

Heqb :

negbguard_coverss_onces a₁ a₂ lo hi = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo hi r align = true

H :

Somel, after_checkLetq A RenewIflo hi r align a₁; a₂ i q a₁ lo hi r align live = Somerest′, live′

⊢

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

Heqb :

negblimit_coverss_onces a₁ a₂ lo hi = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo hi r align = true

H :

Somel, after_checkLetq A CheckLimitlo hi r align a₁; a₂ i q a₁ lo hi r align live = Somerest′, live′

⊢

all: injection H as ← ← ; eexists ; split ; reflexivity |

7 open

s :

q :

lo, hi :

r :

align :

a₁ :

rest :

listinst

live :

listfact

Heqb :

negbtrue = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo hi r align = true

⊢

proof_usei q lo hi r align = true ∧ after_checkLetq A Checklo hi r align a₁ i q a₁ lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a₁; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A Checklo hi r align a₁ live

focused goal

s :

q :

lo, hi :

r :

align, ahi :

a₁ :

rest :

listinst

live :

listfact

Heqb :

negbmemq s_aheads = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo ahi r align && ahead_transparenti = true

⊢

proof_usei q lo ahi r align = true ∧ after_checkLetq A CheckAheadlo hi r align ahi a₁ i q a₁ lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a₁; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A CheckAheadlo hi r align ahi a₁ live

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

n :

Heqv :

a₁ = Tmpn

p :

name × Z × Z × Z

p₀ :

name × Z × Z

z :

p₁ :

name × Z

z₀ :

n₀ :

z₁ :

Heqp₂ :

p₁ = n₀, z₁

Heqp₁ :

p₀ = n₀, z₁, z₀

Heqp₀ :

p = n₀, z₁, z₀, z

Heqo :

lookupn s_renewss = Somen₀, z₁, z₀, z

z₂ :

Heqo₀ :

pointer_distances_onces a₂ Tmpn₀ = Somez₂

Heqb :

negbz₁ ≤? lo + z₂ && hi + z₂ ≤? z₀ && z mod align =? 0 && lo + z₂ − z₁ mod align =? 0 = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo hi r align = true

⊢

proof_usei q lo hi r align = true ∧ after_checkLetq A Renewlo hi r align Tmpn; a₂ i q a₂ lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a₂; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A Renewlo hi r align Tmpn; a₂ live

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂, a₃ :

rest :

listinst

live :

listfact

Heqb :

negbhull_renewables_renewss s_onces a₃ lo hi align a₁ a₂ = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo hi r align = true

⊢

proof_usei q lo hi r align = true ∧ after_checkLetq A RenewHulllo hi r align a₁; a₂; a₃ i q a₃ lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a₃; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A RenewHulllo hi r align a₁; a₂; a₃ live

focused goal

s :

q :

b :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

Heqb₀ :

negb

match a₁ with

Tmpn₁

⇒

match lookupn₁ s_renewss with

Somep₁, lo₁, hi₁, _

⇒

match pointer_distances_onces a₂ Tmpp₁ with

Somed₀

⇒

half_knownb lo hi d₀ lo₁ hi₁

None

⇒

false

None

⇒

false

⇒

false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₁ :

proof_usei q lo hi r align = true

⊢

proof_usei q lo hi r align = true ∧ after_checkLetq A HalfCheckb lo hi r align a₁; a₂ i q a₂ lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a₂; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A HalfCheckb lo hi r align a₁; a₂ live

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

Heqb :

negbguard_coverss_onces a₁ a₂ lo hi = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo hi r align = true

⊢

proof_usei q lo hi r align = true ∧ after_checkLetq A RenewIflo hi r align a₁; a₂ i q a₁ lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a₁; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A RenewIflo hi r align a₁; a₂ live

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

Heqb :

negblimit_coverss_onces a₁ a₂ lo hi = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo hi r align = true

⊢

proof_usei q lo hi r align = true ∧ after_checkLetq A CheckLimitlo hi r align a₁; a₂ i q a₁ lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a₁; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A CheckLimitlo hi r align a₁; a₂ live

all: repeat match goal withE : _ && _ = true |- _⇒apply andb_true_iff in E as ? ?end

7 open

s :

q :

lo, hi :

r :

align :

a₁ :

rest :

listinst

live :

listfact

Heqb :

negbtrue = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo hi r align = true

⊢

focused goal

s :

q :

lo, hi :

r :

align, ahi :

a₁ :

rest :

listinst

live :

listfact

Heqb :

negbmemq s_aheads = false

i :

l :

listinst

Heql :

rest = i :: l

H :

proof_usei q lo ahi r align = true

H₀ :

ahead_transparenti = true

⊢

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

n :

Heqv :

a₁ = Tmpn

p :

name × Z × Z × Z

p₀ :

name × Z × Z

z :

p₁ :

name × Z

z₀ :

n₀ :

z₁ :

Heqp₂ :

p₁ = n₀, z₁

Heqp₁ :

p₀ = n₀, z₁, z₀

Heqp₀ :

p = n₀, z₁, z₀, z

Heqo :

lookupn s_renewss = Somen₀, z₁, z₀, z

z₂ :

Heqo₀ :

pointer_distances_onces a₂ Tmpn₀ = Somez₂

Heqb :

negbz₁ ≤? lo + z₂ && hi + z₂ ≤? z₀ && z mod align =? 0 && lo + z₂ − z₁ mod align =? 0 = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo hi r align = true

⊢

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂, a₃ :

rest :

listinst

live :

listfact

Heqb :

negbhull_renewables_renewss s_onces a₃ lo hi align a₁ a₂ = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo hi r align = true

⊢

focused goal

s :

q :

b :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

Heqb₀ :

negb

match a₁ with

Tmpn₁

⇒

match lookupn₁ s_renewss with

Somep₁, lo₁, hi₁, _

⇒

match pointer_distances_onces a₂ Tmpp₁ with

Somed₀

⇒

half_knownb lo hi d₀ lo₁ hi₁

None

⇒

false

None

⇒

false

⇒

false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₁ :

proof_usei q lo hi r align = true

⊢

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

Heqb :

negbguard_coverss_onces a₁ a₂ lo hi = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo hi r align = true

⊢

focused goal

s :

q :

lo, hi :

r :

align :

a₁, a₂ :

rest :

listinst

live :

listfact

Heqb :

negblimit_coverss_onces a₁ a₂ lo hi = false

i :

l :

listinst

Heql :

rest = i :: l

Heqb₀ :

proof_usei q lo hi r align = true

⊢

all: split ; assumption | reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros s i rest live rest′ live′ fa fb Hf Hg H

destruct k ; try destruct o ; discriminate Hf

destruct o ; try discriminate Hf ; destruct args as | a₁ | a₂ | a₃ | a₄ args ; simpl in Hf , Hg ; try discriminate Hf ; injection Hf as ← ; injection Hg as ← ; cbn [ f_q f_p f_lo f_hi f_r f_al ]

all: unfold checked_inst_rest in H ; cbn zeta in H

all: repeat match type of H withcontext [match ?x with _ ⇒ _ end]⇒destruct x eqn :? ; try discriminate Hend

all: injection H as ← ← ; eexists ; split ; reflexivity |

all: repeat match goal withE : _ && _ = true |- _⇒apply andb_true_iff in E as ? ?end

all: split ; assumption | reflexivity

The pass takes a check_local with its access too, and keeps after the access the facts it had with q killed.

658Lemma checked_inst_rest_local

∀ s q x off bytes r al rest live rest′ live′

checked_inst_rests Letq A CheckLocalx off bytes r al [ ] rest live = Somerest′, live′

∃access, rest = access :: rest′ ∧ live′ = evidence_afteraccess killq live

Explore proof 6 tactics

Initial goal

⊢

∀s : src q x : name off bytes : Z r : rights al : Z rest : listinst live : listfact rest′ : listinst live′ : listfact, checked_inst_rests Letq A CheckLocalx off bytes r al [ ] rest live = Somerest′, live′ → ∃access : inst, rest = access :: rest′ ∧ live′ = evidence_afteraccess killq live

intros s q x off bytes r al rest live rest′ live′ H

s :

q, x :

off, bytes :

r :

al :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

checked_inst_rests Letq A CheckLocalx off bytes r al [ ] rest live = Somerest′, live′

⊢

∃access : inst, rest = access :: rest′ ∧ live′ = evidence_afteraccess killq live

unfold checked_inst_rest in H

s :

q, x :

off, bytes :

r :

al :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

match rest with

[ ]

⇒

None

access :: rest′

⇒

match raw_accessaccess with

Someq′, _, 0, _

⇒

name_eqbq′ q && covered_accessaccess q 0 bytes r al && storage_effectsaccess Local'

→

Somerest′, evidence_afteraccess killq live

else

None

Someq′, _, Z.pos_, _ | Someq′, _, Z.neg_, _

⇒

None

⇒

None

Somerest′, live′

⊢

∃access : inst, rest = access :: rest′ ∧ live′ = evidence_afteraccess killq live

cbn zeta in H

s :

q, x :

off, bytes :

r :

al :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

match rest with

[ ]

⇒

None

access :: rest′

⇒

match raw_accessaccess with

Someq′, _, 0, _

⇒

name_eqbq′ q && covered_accessaccess q 0 bytes r al && storage_effectsaccess Local'

→

Somerest′, evidence_afteraccess killq live

else

None

Someq′, _, Z.pos_, _ | Someq′, _, Z.neg_, _

⇒

None

⇒

None

Somerest′, live′

⊢

∃access : inst, rest = access :: rest′ ∧ live′ = evidence_afteraccess killq live

repeat match type of H withcontext [match ?y with _ ⇒ _ end]⇒destruct y eqn :? ; try discriminate Hend

s :

q, x :

off, bytes :

r :

al :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

i :

l :

listinst

Heql :

rest = i :: l

p :

name × access_type × Z × rights

p₀ :

name × access_type × Z

r₀ :

p₁ :

name × access_type

z :

n :

a :

Heqp₂ :

p₁ = n, a

Heqz₀ :

z = 0

Heqp₁ :

p₀ = n, a, 0

Heqp₀ :

p = n, a, 0, r₀

Heqo :

raw_accessi = Somen, a, 0, r₀

Heqb :

name_eqbn q && covered_accessi q 0 bytes r al && storage_effectsi Local' = true

H :

Somel, evidence_afteri killq live = Somerest′, live′

⊢

∃access : inst, i :: l = access :: rest′ ∧ live′ = evidence_afteraccess killq live

injection H as ← ←

s :

q, x :

off, bytes :

r :

al :

rest :

listinst

live :

listfact

i :

l :

listinst

Heql :

rest = i :: l

p :

name × access_type × Z × rights

p₀ :

name × access_type × Z

r₀ :

p₁ :

name × access_type

z :

n :

a :

Heqp₂ :

p₁ = n, a

Heqz₀ :

z = 0

Heqp₁ :

p₀ = n, a, 0

Heqp₀ :

p = n, a, 0, r₀

Heqo :

raw_accessi = Somen, a, 0, r₀

Heqb :

name_eqbn q && covered_accessi q 0 bytes r al && storage_effectsi Local' = true

⊢

∃access : inst, i :: l = access :: l ∧ evidence_afteri killq live = evidence_afteraccess killq live

eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros s q x off bytes r al rest live rest′ live′ H

unfold checked_inst_rest in H

cbn zeta in H

repeat match type of H withcontext [match ?y with _ ⇒ _ end]⇒destruct y eqn :? ; try discriminate Hend

injection H as ← ←

eauto

After a check_function and its call, the pass keeps no fact.

670Lemma checked_inst_rest_function

∀ s q args rest live rest′ live′

checked_inst_rests Letq F CheckFunction args rest live = Somerest′, live′

live′ = [ ]

Explore proof 5 tactics

Initial goal

⊢

∀s : src q : name args : listvalue rest : listinst live : listfact rest′ : listinst live′ : listfact, checked_inst_rests Letq F CheckFunction args rest live = Somerest′, live′ → live′ = [ ]

intros s q args rest live rest′ live′ H

s :

q :

args :

listvalue

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

checked_inst_rests Letq F CheckFunction args rest live = Somerest′, live′

⊢

live′ = [ ]

unfold checked_inst_rest in H

s :

q :

args :

listvalue

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

match rest with

RawCall_ Tmpq′ _ :: rest′

⇒

name_eqbq′ q

→

Somerest′, [ ]

else

None

⇒

None

Somerest′, live′

⊢

live′ = [ ]

destruct rest as | rest ; try discriminate H ; simpl in H ; destruct callee ; try discriminate H ; destruct name_eqb_ _ ; try discriminate H

s :

q :

args :

listvalue

r :

call_result

n :

args₀ :

listarg

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

H :

Somerest, [ ] = Somerest′, live′

⊢

live′ = [ ]

injection H as _ ←

s :

q :

args :

listvalue

r :

call_result

n :

args₀ :

listarg

rest :

listinst

live :

listfact

rest′ :

listinst

⊢

[ ] = [ ]

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros s q args rest live rest′ live′ H

unfold checked_inst_rest in H

destruct rest as | rest ; try discriminate H ; simpl in H ; destruct callee ; try discriminate H ; destruct name_eqb_ _ ; try discriminate H

injection H as _ ←

reflexivity

Where the facts live hold before an instruction i the pass accepts and i continues, the pass's facts after it hold; or, for an instruction the pass takes with its access, they hold after that access, whatever frame fr1 with i's environment runs it.

683Theorem checked_inst_holds

∀ ge s fr m i rest live rest′ live′ e₁ l₁ m₁

facts_holdge m fr_envfr live

checked_inst_rests i rest live = Somerest′, live′

inst_stepge fr m i = SomeIContinuee₁ l₁ m₁

rest′ = rest ∧ facts_holdge m₁ e₁ live′ ∨ ∃access, rest = access :: rest′ ∧ ∀fr₁ e₂ l₂ m₂, fr_envfr₁ = e₁ → inst_stepge fr₁ m₁ access = SomeIContinuee₂ l₂ m₂ → facts_holdge m₂ e₂ live′

Proof 43 steps Qed

intros ge s fr m i rest live rest′ live′ e₁ l₁ m₁ Hl Hc Hs

destruct check_facti as fa | eqn: Hf

–assert ∃fb, access_facti = Somefb as fb Hg by eapply access_fact_some ; eauto

destruct checked_inst_rest_check_ _ _ _ _ _ _ _ Hf Hg Hc as access & → & _ & →

right

exists access

split ; reflexivity |

intros fr₁ e₂ l₂ m₂ He Ha

eapply evidence_after_holds ; | exact Ha

rewrite He

apply facts_hold_cons

+exact proj1check_like_holds_ _ _ _ _ _ _ _ _ Hf Hg Hs

+eapply evidence_after_holds ; eauto

–destruct pass_speciali eqn: Hp

+right

unfold pass_special in Hp

rewrite Hf in Hp

destruct k ; try discriminate Hp ; destruct o ; try discriminate Hp

∗destruct args ; | discriminate Hp

destruct checked_inst_rest_local_ _ _ _ _ _ _ _ _ _ _ Hc as access & → & →

exists access

split ; reflexivity |

intros fr₁ e₂ l₂ m₂ He Ha

eapply evidence_after_holds ; | exact Ha

rewrite He

destruct let_step_ _ _ _ _ _ _ _ _ _ Hs as Hr Ha′

eapply facts_hold_kill ; eauto

∗rewrite checked_inst_rest_function_ _ _ _ _ _ _ Hc

unfold checked_inst_rest in Hc

destruct rest as | access rest₀ ; discriminate Hc |

exists access

split

{destruct access ; try discriminate Hc ; destruct callee ; try discriminate Hc ; destruct name_eqb_ _ ; try discriminate Hc ; injection Hc as ← _ ; reflexivity

intros fr₁ e₂ l₂ m₂ _ _ fa′

+left

rewrite checked_inst_rest_generic_ _ _ _ Hp in Hc

destruct generic_rest_shape_ _ _ _ _ _ Hc as → & → | d & g & → & → & _

∗split ; reflexivity |

eapply evidence_after_holds ; eauto

∗split ; reflexivity |

destruct let_step_ _ _ _ _ _ _ _ _ _ Hs as Hr He

eapply facts_hold_kill ; eauto

As proof_use/6's two clauses: an instruction that uses the proof q right after its check is a touch of q, which accesses nothing, or an access q's range covers.

727Lemma proof_use_cases

∀ i q lo hi r al

proof_usei q lo hi r al = true

i = Touchq ∨ covered_accessi q lo hi r al = true

Explore proof 7 tactics

Initial goal

⊢

∀i : inst q : name lo hi : Z r : rights al : Z, proof_usei q lo hi r al = true → i = Touchq ∨ covered_accessi q lo hi r al = true

intros i q lo hi r al H

i :

q :

lo, hi :

r :

al :

H :

proof_usei q lo hi r al = true

⊢

i = Touchq ∨ covered_accessi q lo hi r al = true

destruct i as d k o args | | | | | | | | q′ ; try right ; unfold proof_use in H ; apply andb_true_iff in H as H _ ; exact H

q′, q :

lo, hi :

r :

al :

H :

proof_useTouchq′ q lo hi r al = true

⊢

Touchq′ = Touchq ∨ covered_accessTouchq′ q lo hi r al = true

left

q′, q :

lo, hi :

r :

al :

H :

proof_useTouchq′ q lo hi r al = true

⊢

Touchq′ = Touchq

unfold proof_use in H

q′, q :

lo, hi :

r :

al :

H :

name_eqbq′ q = true

⊢

Touchq′ = Touchq

apply term_eqb_eq in H

q′, q :

lo, hi :

r :

al :

H :

q′ = q

⊢

Touchq′ = Touchq

subst q′

q :

lo, hi :

r :

al :

⊢

Touchq = Touchq

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros i q lo hi r al H

destruct i as d k o args | | | | | | | | q′ ; try right ; unfold proof_use in H ; apply andb_true_iff in H as H _ ; exact H

left

unfold proof_use in H

apply term_eqb_eq in H

subst q′

reflexivity

The access a check-like instruction i is checked for, run right after it, gives no unchecked, where objects fit the address space.

738Theorem checked_access_not_unchecked

∀ ge s fr m i rest live rest′ live′ e₁ l₁ m₁ fr₁ access why

check_facti ≠ None

checked_inst_rests i access :: rest live = Somerest′, live′

inst_stepge fr m i = SomeIContinuee₁ l₁ m₁

fr_envfr₁ = e₁

inst_stepge fr₁ m₁ access ≠ SomeIStopUncheckedwhy

Explore proof 11 tactics

Initial goal

⊢

∀ge : genv s : src fr : frame m : Memory.mem i : inst rest : listinst live : listfact rest′ : listinst live′ : listfact e₁ : env l₁ : listname × optionZ m₁ : Memory.mem fr₁ : frame access : inst why : reason, objects_fitm_regionsm₁ → check_facti ≠ None → checked_inst_rests i access :: rest live = Somerest′, live′ → inst_stepge fr m i = SomeIContinuee₁ l₁ m₁ → fr_envfr₁ = e₁ → inst_stepge fr₁ m₁ access ≠ SomeIStopUncheckedwhy

intros ge s fr m i rest live rest′ live′ e₁ l₁ m₁ fr₁ access why Hfit Hf Hc Hs He

ge :

s :

fr :

m :

Memory.mem

i :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

e₁ :

l₁ :

listname × optionZ

m₁ :

Memory.mem

fr₁ :

access :

why :

Hfit :

Hf :

check_facti ≠ None

Hc :

checked_inst_rests i access :: rest live = Somerest′, live′

Hs :

inst_stepge fr m i = SomeIContinuee₁ l₁ m₁

He :

fr_envfr₁ = e₁

⊢

inst_stepge fr₁ m₁ access ≠ SomeIStopUncheckedwhy

destruct check_facti as fa | eqn: Ef ; | contradiction

ge :

s :

fr :

m :

Memory.mem

i :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

e₁ :

l₁ :

listname × optionZ

m₁ :

Memory.mem

fr₁ :

access :

why :

Hfit :

fa :

Ef :

check_facti = Somefa

Hf :

Somefa ≠ None

Hc :

checked_inst_rests i access :: rest live = Somerest′, live′

Hs :

inst_stepge fr m i = SomeIContinuee₁ l₁ m₁

He :

fr_envfr₁ = e₁

⊢

inst_stepge fr₁ m₁ access ≠ SomeIStopUncheckedwhy

assert ∃fb, access_facti = Somefb as fb Hg by eapply access_fact_some ; eauto

ge :

s :

fr :

m :

Memory.mem

i :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

e₁ :

l₁ :

listname × optionZ

m₁ :

Memory.mem

fr₁ :

access :

why :

Hfit :

fa :

Ef :

check_facti = Somefa

Hf :

Somefa ≠ None

Hc :

checked_inst_rests i access :: rest live = Somerest′, live′

Hs :

inst_stepge fr m i = SomeIContinuee₁ l₁ m₁

He :

fr_envfr₁ = e₁

fb :

Hg :

access_facti = Somefb

⊢

inst_stepge fr₁ m₁ access ≠ SomeIStopUncheckedwhy

destruct checked_inst_rest_check_ _ _ _ _ _ _ _ Ef Hg Hc as access′ & E & Hu & _

ge :

s :

fr :

m :

Memory.mem

i :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

e₁ :

l₁ :

listname × optionZ

m₁ :

Memory.mem

fr₁ :

access :

why :

Hfit :

fa :

Ef :

check_facti = Somefa

Hf :

Somefa ≠ None

Hc :

checked_inst_rests i access :: rest live = Somerest′, live′

Hs :

inst_stepge fr m i = SomeIContinuee₁ l₁ m₁

He :

fr_envfr₁ = e₁

fb :

Hg :

access_facti = Somefb

access′ :

E :

access :: rest = access′ :: rest′

Hu :

proof_useaccess′ f_qfb f_lofb f_hifb f_rfb f_alfb = true

⊢

inst_stepge fr₁ m₁ access ≠ SomeIStopUncheckedwhy

injection E as ← _

ge :

s :

fr :

m :

Memory.mem

i :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

e₁ :

l₁ :

listname × optionZ

m₁ :

Memory.mem

fr₁ :

access :

why :

Hfit :

fa :

Ef :

check_facti = Somefa

Hf :

Somefa ≠ None

Hc :

checked_inst_rests i access :: rest live = Somerest′, live′

Hs :

inst_stepge fr m i = SomeIContinuee₁ l₁ m₁

He :

fr_envfr₁ = e₁

fb :

Hg :

access_facti = Somefb

Hu :

proof_useaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true

⊢

inst_stepge fr₁ m₁ access ≠ SomeIStopUncheckedwhy

destruct proof_use_cases_ _ _ _ _ _ Hu as → | Hcov

2 open

ge :

s :

fr :

m :

Memory.mem

i :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

e₁ :

l₁ :

listname × optionZ

m₁ :

Memory.mem

fr₁ :

why :

Hfit :

fa :

Ef :

check_facti = Somefa

Hf :

Somefa ≠ None

fb :

Hc :

checked_inst_rests i Touchf_qfb :: rest live = Somerest′, live′

Hs :

inst_stepge fr m i = SomeIContinuee₁ l₁ m₁

He :

fr_envfr₁ = e₁

Hg :

access_facti = Somefb

Hu :

proof_useTouchf_qfb f_qfb f_lofb f_hifb f_rfb f_alfb = true

⊢

inst_stepge fr₁ m₁ Touchf_qfb ≠ SomeIStopUncheckedwhy

focused goal

ge :

s :

fr :

m :

Memory.mem

i :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

e₁ :

l₁ :

listname × optionZ

m₁ :

Memory.mem

fr₁ :

access :

why :

Hfit :

fa :

Ef :

check_facti = Somefa

Hf :

Somefa ≠ None

Hc :

checked_inst_rests i access :: rest live = Somerest′, live′

Hs :

inst_stepge fr m i = SomeIContinuee₁ l₁ m₁

He :

fr_envfr₁ = e₁

fb :

Hg :

access_facti = Somefb

Hu :

proof_useaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true

Hcov :

covered_accessaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true

⊢

inst_stepge fr₁ m₁ access ≠ SomeIStopUncheckedwhy

{cbn

2 open

ge :

s :

fr :

m :

Memory.mem

i :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

e₁ :

l₁ :

listname × optionZ

m₁ :

Memory.mem

fr₁ :

why :

Hfit :

fa :

Ef :

check_facti = Somefa

Hf :

Somefa ≠ None

fb :

Hc :

checked_inst_rests i Touchf_qfb :: rest live = Somerest′, live′

Hs :

inst_stepge fr m i = SomeIContinuee₁ l₁ m₁

He :

fr_envfr₁ = e₁

Hg :

access_facti = Somefb

Hu :

proof_useTouchf_qfb f_qfb f_lofb f_hifb f_rfb f_alfb = true

⊢

SomeIContinuefr_envfr₁ fr_localsfr₁ m₁ ≠ SomeIStopUncheckedwhy

deferred goal

ge :

s :

fr :

m :

Memory.mem

i :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

e₁ :

l₁ :

listname × optionZ

m₁ :

Memory.mem

fr₁ :

access :

why :

Hfit :

fa :

Ef :

check_facti = Somefa

Hf :

Somefa ≠ None

Hc :

checked_inst_rests i access :: rest live = Somerest′, live′

Hs :

inst_stepge fr m i = SomeIContinuee₁ l₁ m₁

He :

fr_envfr₁ = e₁

fb :

Hg :

access_facti = Somefb

Hu :

proof_useaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true

Hcov :

covered_accessaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true

⊢

inst_stepge fr₁ m₁ access ≠ SomeIStopUncheckedwhy

discriminate

deferred goal

ge :

s :

fr :

m :

Memory.mem

i :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

e₁ :

l₁ :

listname × optionZ

m₁ :

Memory.mem

fr₁ :

access :

why :

Hfit :

fa :

Ef :

check_facti = Somefa

Hf :

Somefa ≠ None

Hc :

checked_inst_rests i access :: rest live = Somerest′, live′

Hs :

inst_stepge fr m i = SomeIContinuee₁ l₁ m₁

He :

fr_envfr₁ = e₁

fb :

Hg :

access_facti = Somefb

Hu :

proof_useaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true

Hcov :

covered_accessaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true

⊢

inst_stepge fr₁ m₁ access ≠ SomeIStopUncheckedwhy

destruct proj2check_like_holds_ _ _ _ _ _ _ _ _ Ef Hg Hs as p & Eq & _ & Hp

ge :

s :

fr :

m :

Memory.mem

i :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

e₁ :

l₁ :

listname × optionZ

m₁ :

Memory.mem

fr₁ :

access :

why :

Hfit :

fa :

Ef :

check_facti = Somefa

Hf :

Somefa ≠ None

Hc :

checked_inst_rests i access :: rest live = Somerest′, live′

Hs :

inst_stepge fr m i = SomeIContinuee₁ l₁ m₁

He :

fr_envfr₁ = e₁

fb :

Hg :

access_facti = Somefb

Hu :

proof_useaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true

Hcov :

covered_accessaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true

p :

Eq :

lookupf_qfb e₁ = SomeWPtrp

Hp :

check_passesm₁ p f_lofb f_hifb f_rfb f_alfb

⊢

inst_stepge fr₁ m₁ access ≠ SomeIStopUncheckedwhy

rewrite <- He in Eq

ge :

s :

fr :

m :

Memory.mem

i :

rest :

listinst

live :

listfact

rest′ :

listinst

live′ :

listfact

e₁ :

l₁ :

listname × optionZ

m₁ :

Memory.mem

fr₁ :

access :

why :

Hfit :

fa :

Ef :

check_facti = Somefa

Hf :

Somefa ≠ None

Hc :

checked_inst_rests i access :: rest live = Somerest′, live′

Hs :

inst_stepge fr m i = SomeIContinuee₁ l₁ m₁

He :

fr_envfr₁ = e₁

fb :

Hg :

access_facti = Somefb

Hu :

proof_useaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true

Hcov :

covered_accessaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true

p :

Eq :

lookupf_qfb fr_envfr₁ = SomeWPtrp

Hp :

check_passesm₁ p f_lofb f_hifb f_rfb f_alfb

⊢

inst_stepge fr₁ m₁ access ≠ SomeIStopUncheckedwhy

exact covered_access_not_unchecked_ _ _ _ _ _ _ _ _ _ _ Hfit Hcov Eq Hp

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros ge s fr m i rest live rest′ live′ e₁ l₁ m₁ fr₁ access why Hfit Hf Hc Hs He

destruct check_facti as fa | eqn: Ef ; | contradiction

assert ∃fb, access_facti = Somefb as fb Hg by eapply access_fact_some ; eauto

destruct checked_inst_rest_check_ _ _ _ _ _ _ _ Ef Hg Hc as access′ & E & Hu & _

injection E as ← _

destruct proof_use_cases_ _ _ _ _ _ Hu as → | Hcov

{cbn

discriminate

destruct proj2check_like_holds_ _ _ _ _ _ _ _ _ Ef Hg Hs as p & Eq & _ & Hp

rewrite <- He in Eq

exact covered_access_not_unchecked_ _ _ _ _ _ _ _ _ _ _ Hfit Hcov Eq Hp

A raw access i that the pass accepts on its own (not with a check) gives no unchecked where the facts hold and objects fit the address space, unless the pass accepted it by hull_covered/7, whose case Chain.v's hull_access_not_unchecked closes.

763Theorem generic_access_not_unchecked

∀ ge s fr m i rest live rest′ live′ q x off need why