Fil-C on Nix

Filnix wiki

the formal campaign

rocq/theories/Evidence.v

Campaign 3's evidence invariant, at one instruction (docs/formal.md, Campaign 3, Proof persistence; docs/rocq.md, The evidence invariant, instruction by instruction).

ir.pl's evidence pass (checked_inst_rest/7, Validate.v's checked_inst_rest) keeps a list of live facts as it walks a block: a fact live(Q, P, Lo, Hi, Rights, Align) is added where a check let(Q, a, check(Lo, Hi, Rights, Align), [P]) passes, and a raw access through Q is accepted where a live fact of Q covers it (covered_access/6). This file says what a fact means at run time (fact_holds) and proves that the pass's bookkeeping keeps it true across one instruction or one edge. A check reads only the regions of memory, so a step that changes no region keeps it passing; and the facts the pass drops at a definition (evidence_kill/3) are exactly those whose Q or P it redefines.

Persistence.v carries this along the runs of Machine R. A check_ahead whose wider check failed dooms its frame (doomed), and its fact then does not hold; that, and the reuse forms' own rules (that a renew finds its bounds, and hull_covered/7), are Campaign 3's corollaries.

From Stdlib Require Import String ZArith List Bool Lia
From Nanofil Require Import Term Syntax Values Memory Runtime Ops Semantics Machine Validate Coverage
Import ListNotations
Open Scope Z_scope

Names

Looking up the name k right after putting the value v for it gives v.

32Lemma lookup_put_same
∀ A : Type k v : A ps
lookupk putk v ps = Somev
Explore proof 5 tactics

Initial goal

⊢
∀A : Type k : name v : A ps : listname × A, lookupk putk v ps = Somev

intros A k v ps

A :
Type
k :
v :
A
ps :
listname × A
⊢
lookupk putk v ps = Somev

simpl

A :
Type
k :
v :
A
ps :
listname × A
⊢
→
Somev
else
lookupk filterλp : name × A ⇒ negbname_eqbk fstp ps
=
Somev

unfold name_eqb

A :
Type
k :
v :
A
ps :
listname × A
⊢
→
Somev
else
lookupk filterλp : name × A ⇒ negbterm_eqbk fstp ps
=
Somev

rewrite term_eqb_refl

A :
Type
k :
v :
A
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
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 :
A
ps :
listname × A
H :
name_eqbk d = false
⊢
lookupk putd v ps = lookupk ps

simpl

A :
Type
k, d :
v :
A
ps :
listname × A
H :
name_eqbk d = false
⊢
→
Somev
else
lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps
=
lookupk ps

rewrite H

A :
Type
k, d :
v :
A
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 :
A
k′ :
v′ :
A
ps :
listname × A
H :
name_eqbk d = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbd fstp ps = lookupk ps
⊢
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 :
A
k′ :
v′ :
A
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 :
A
k′ :
v′ :
A
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 :
A
k′ :
v′ :
A
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 :
A
k′ :
v′ :
A
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′ :
A
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
=
→
Somev′
else
lookupk ps
deferred goal
A :
Type
k, d :
v :
A
k′ :
v′ :
A
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′ :
A
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 :
A
k′ :
v′ :
A
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 :
A
k′ :
v′ :
A
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
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 :
Z
al :
Z
E :
H :
⊢
cap_access_resptr_capp m_regionsm′ raw_addressptr_addrp lo hi − lo r al = Someok

rewrite E

m, m′ :
Memory.mem
p :
lo, hi :
Z
al :
Z
E :
H :
⊢

exact H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
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
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 :
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 :
⊢
fact_holdsge m′ e′ fa

exists p

ge :
m, m′ :
Memory.mem
e, e′ :
d :
fa :
Hr :
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 :
⊢
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 :
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 :
⊢
lookupf_qfa e′ = SomeWPtrp
focused goal
ge :
m, m′ :
Memory.mem
e, e′ :
d :
fa :
Hr :
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 :
⊢
value_xge e′ P f_pfa = SomeWPtrp
focused goal
ge :
m, m′ :
Memory.mem
e, e′ :
d :
fa :
Hr :
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

–rewrite He by exact Hq

3 open

ge :
m, m′ :
Memory.mem
e, e′ :
d :
fa :
Hr :
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 :
⊢
lookupf_qfa e = SomeWPtrp
deferred goal
ge :
m, m′ :
Memory.mem
e, e′ :
d :
fa :
Hr :
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 :
⊢
value_xge e′ P f_pfa = SomeWPtrp
deferred goal
ge :
m, m′ :
Memory.mem
e, e′ :
d :
fa :
Hr :
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

exact Eq

2 open

deferred goal
ge :
m, m′ :
Memory.mem
e, e′ :
d :
fa :
Hr :
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 :
⊢
value_xge e′ P f_pfa = SomeWPtrp
deferred goal
ge :
m, m′ :
Memory.mem
e, e′ :
d :
fa :
Hr :
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

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

2 open

ge :
m, m′ :
Memory.mem
e, e′ :
d :
fa :
Hr :
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 :
⊢
let* x ≔ lookupn e′ in
Somex
=
SomeWPtrp
deferred goal
ge :
m, m′ :
Memory.mem
e, e′ :
d :
fa :
Hr :
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

rewrite He by exact Hp

2 open

ge :
m, m′ :
Memory.mem
e, e′ :
d :
fa :
Hr :
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 :
⊢
let* x ≔ lookupn e in
Somex
=
SomeWPtrp
deferred goal
ge :
m, m′ :
Memory.mem
e, e′ :
d :
fa :
Hr :
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

exact Ep

deferred goal
ge :
m, m′ :
Memory.mem
e, e′ :
d :
fa :
Hr :
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

–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
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 :
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 :
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 :
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
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 :
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 :
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 :
⊢
fact_holdsge m′ e fa

exists p

ge :
m, m′ :
Memory.mem
e :
fs :
listfact
Hr :
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 :
⊢
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 :
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

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′
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
⇒
let* chk ≔ access_resm a c width_bytesw Write 8 in
Some
chk
match chk with
_
⇒
None
_
⇒
match x with
⇒
let* chk ≔
match w with
⇒
8
_
⇒
1
in
Some
chk
match chk with
_
⇒
None
=
Somer, m′
→

intros w m a c x r m′ H

m :
Memory.mem
a :
Z
c :
x :
r :
resunit
m′ :
Memory.mem
H :
match w with
⇒
match x with
⇒
let* chk ≔ access_resm a c width_bytesw Write 8 in
Some
chk
match chk with
_
⇒
None
_
⇒
match x with
⇒
let* chk ≔
match w with
⇒
8
_
⇒
1
in
Some
chk
match chk with
_
⇒
None
=
Somer, m′
⊢

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′
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_, m1
⇒
match k with
⇒
SomeRValWPtrptr_addr ≔ load_bytesm1 ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align 8; ptr_cap ≔ aux_atm1 ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align, m1
_
⇒
SomeRValWIntload_bytesm1 ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align width_bytesw, m1
SomeRTrapwhy, m1
⇒
SomeRTrapwhy, m1
_
⇒
None
SomeRTrapwhy
⇒
SomeRTrapwhy, m
_
⇒
None
None
⇒
None
SomeRTrapwhy
⇒
SomeRTrapwhy, m
_
⇒
None
=
Somer, m′
→

intros k p m r m′ H

p :
m :
Memory.mem
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
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_, m1
⇒
match k with
⇒
SomeRValWPtrptr_addr ≔ load_bytesm1 ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align 8; ptr_cap ≔ aux_atm1 ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align, m1
_
⇒
SomeRValWIntload_bytesm1 ptr_addrptr_addr ≔ load_bytesm ptr_addrp 8; ptr_cap ≔ aux_atm ptr_addrp + align − 1 / align × align width_bytesw, m1
SomeRTrapwhy, m1
⇒
SomeRTrapwhy, m1
_
⇒
None
SomeRTrapwhy
⇒
SomeRTrapwhy, m
_
⇒
None
None
⇒
None
SomeRTrapwhy
⇒
SomeRTrapwhy, m
_
⇒
None
=
Somer, m′
⊢

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′
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* r0 ≔ float_arithmetico f xs in
None
⇒
op_res_into k xs m
Cmpc ck
⇒
match xs with
⇒
match fmt_ofck with
Somef
⇒
None
⇒
op_res_into k xs m
WInta :: WIntb :: _ :: _
⇒
match fmt_ofck with
Some_
⇒
None
None
⇒
op_res_into k xs m
WInta | WInta :: WPtr_ :: _ | WInta :: WLimit_ _ :: _
⇒
match fmt_ofck with
Some_
⇒
None
None
⇒
op_res_into k xs m
_
⇒
match fmt_ofck with
Some_
⇒
None
None
⇒
op_res_into k xs m
⇒
match xs with
⇒
let* r0 ≔ float_converto k x in
WIntx :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
⇒
match xs with
⇒
let* from ≔ fmt_offk in
let* m0 ≔ modulusk in
let 'lo, hi ≔
match sg with
⇒
−m0 / 2, m0 / 2 − 1
⇒
0, m0 − 1
in
match Ieee.ieee_to_intfrom x with
Somen
⇒
lo ≤? n && n ≤? hi
→
SomeOpResRValWIntn mod m0 m
else
SomeOpUBTAtom"float_conversion"
None
⇒
SomeOpUBTAtom"float_conversion"
WIntx :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
⇒
match fmt_ofk with
Somef
⇒
match xs with
⇒
let* n ≔ integer_sourceik sg x in
WIntx :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
None
⇒
op_res_into k xs m
⇒
match xs with
WIntx :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
⇒
match xs with
⇒
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′
→

intros o k xs m r m′ H

o :
xs :
listword
m :
Memory.mem
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
None
⇒
op_res_into k xs m
Cmpc ck
⇒
match xs with
⇒
match fmt_ofck with
Somef
⇒
None
⇒
op_res_into k xs m
WInta :: WIntb :: _ :: _
⇒
match fmt_ofck with
Some_
⇒
None
None
⇒
op_res_into k xs m
WInta | WInta :: WPtr_ :: _ | WInta :: WLimit_ _ :: _
⇒
match fmt_ofck with
Some_
⇒
None
None
⇒
op_res_into k xs m
_
⇒
match fmt_ofck with
Some_
⇒
None
None
⇒
op_res_into k xs m
⇒
match xs with
⇒
let* r ≔ float_converto k x in
WIntx :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
⇒
match xs with
⇒
let* from ≔ fmt_offk in
let* m0 ≔ modulusk in
let 'lo, hi ≔
match sg with
⇒
−m0 / 2, m0 / 2 − 1
⇒
0, m0 − 1
in
match Ieee.ieee_to_intfrom x with
Somen
⇒
lo ≤? n && n ≤? hi
→
SomeOpResRValWIntn mod m0 m
else
SomeOpUBTAtom"float_conversion"
None
⇒
SomeOpUBTAtom"float_conversion"
WIntx :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
⇒
match fmt_ofk with
Somef
⇒
match xs with
⇒
let* n ≔ integer_sourceik sg x in
WIntx :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
None
⇒
op_res_into k xs m
⇒
match xs with
WIntx :: _ :: _
⇒
op_res_into k xs m
_
⇒
op_res_into k xs m
⇒
match xs with
⇒
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′
⊢

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
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
=
IContinuee′ l′ m′
→
∃x : word, r = RValx ∧ e′ = putd x e ∧ m′ = m

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

d :
e :
l :
listname × optionZ
m :
Memory.mem
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
H :
match r with
=
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
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′
inst_stepge fr m i = SomeIContinuee′ l′ m′
∧
match inst_def_firsti with
Somed
⇒
None
⇒
e′ = fr_envfr
Explore proof 24 tactics

Initial goal

⊢
∀ ge : genv fr : frame m : Memory.mem i : inst e′ : env l′ : listname × optionZ m′ : Memory.mem  ,
→
inst_stepge fr m i = SomeIContinuee′ l′ m′
→
∧
match inst_def_firsti with
Somed
⇒
None
⇒
e′ = fr_envfr

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

ge :
fr :
m :
Memory.mem
i :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
H :
inst_stepge fr m i = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firsti with
Somed
⇒
None
⇒
e′ = fr_envfr

destruct i ; simpl in Hp ; try discriminate Hp

4 open

ge :
fr :
m :
Memory.mem
d :
o :
args :
listvalue
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match k with
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
⇒
false
_
⇒
true
_
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m Letd k o args = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLetd k o args with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
focused goal
ge :
fr :
m :
Memory.mem
d :
o :
args :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Flightd o args lower = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstFlightd o args lower with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
focused goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m RawStorew off v a = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
focused goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

–destruct special_leto eqn: Es

5 open

ge :
fr :
m :
Memory.mem
d :
o :
args :
listvalue
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match k with
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
⇒
false
_
⇒
true
_
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m Letd k o args = SomeIContinuee′ l′ m′
Es :
special_leto = true
⊢
∧
match inst_def_firstLetd k o args with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
focused goal
ge :
fr :
m :
Memory.mem
d :
o :
args :
listvalue
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match k with
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
⇒
false
_
⇒
true
_
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m Letd k o args = SomeIContinuee′ l′ m′
Es :
special_leto = false
⊢
∧
match inst_def_firstLetd k o args with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
d :
o :
args :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Flightd o args lower = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstFlightd o args lower with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m RawStorew off v a = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

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

4 open

deferred goal
ge :
fr :
m :
Memory.mem
d :
o :
args :
listvalue
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match k with
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
⇒
false
_
⇒
true
_
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m Letd k o args = SomeIContinuee′ l′ m′
Es :
special_leto = false
⊢
∧
match inst_def_firstLetd k o args with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
d :
o :
args :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Flightd o args lower = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstFlightd o args lower with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m RawStorew off v a = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

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

4 open

ge :
fr :
m :
Memory.mem
d :
o :
args :
listvalue
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match k with
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
⇒
false
_
⇒
true
_
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
=
true
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
λ base : Z  ⇒
let x, m′ ≔ kontbase in
putd x e, locals, m′
None
⇒
None
=
SomeIContinuee′ l′ m′
Es :
special_leto = false
⊢
∧
match inst_def_firstLetd k o args with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
d :
o :
args :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Flightd o args lower = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstFlightd o args lower with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m RawStorew off v a = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

simpl

4 open

ge :
fr :
m :
Memory.mem
d :
o :
args :
listvalue
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match k with
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
⇒
false
_
⇒
true
_
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
=
true
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
λ 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′
deferred goal
ge :
fr :
m :
Memory.mem
d :
o :
args :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Flightd o args lower = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstFlightd o args lower with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m RawStorew off v a = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

cbn zeta in H

4 open

ge :
fr :
m :
Memory.mem
d :
o :
args :
listvalue
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match k with
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
⇒
false
_
⇒
true
_
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
=
true
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
λ 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′
deferred goal
ge :
fr :
m :
Memory.mem
d :
o :
args :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Flightd o args lower = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstFlightd o args lower with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m RawStorew off v a = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

cases H

4 open

ge :
fr :
m :
Memory.mem
d :
o :
args :
listvalue
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match k with
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
⇒
false
_
⇒
true
_
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
=
true
l :
listclass
Heqo0 :
op_arg_classeso k = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
o0 :
m0 :
Memory.mem
Heqo3 :
o0 = OpResr m0
Heqo2 :
op_reso k l0 m = SomeOpResr m0
H :
Somebind_resd r fr_envfr fr_localsfr m0 = SomeIContinuee′ l′ m′
Es :
special_leto = false
⊢
m_regionsm′ = m_regionsm ∧ env_agreed fr_envfr e′
deferred goal
ge :
fr :
m :
Memory.mem
d :
o :
args :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Flightd o args lower = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstFlightd o args lower with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m RawStorew off v a = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

injection H as Hb

4 open

ge :
fr :
m :
Memory.mem
d :
o :
args :
listvalue
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match k with
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
⇒
false
_
⇒
true
_
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
=
true
l :
listclass
Heqo0 :
op_arg_classeso k = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
o0 :
m0 :
Memory.mem
Heqo3 :
o0 = OpResr m0
Heqo2 :
op_reso k l0 m = SomeOpResr m0
Hb :
bind_resd r fr_envfr fr_localsfr m0 = IContinuee′ l′ m′
Es :
special_leto = false
⊢
m_regionsm′ = m_regionsm ∧ env_agreed fr_envfr e′
deferred goal
ge :
fr :
m :
Memory.mem
d :
o :
args :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Flightd o args lower = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstFlightd o args lower with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m RawStorew off v a = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

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

4 open

ge :
fr :
m :
Memory.mem
d :
o :
args :
listvalue
l′ :
listname × optionZ
Hp :
match k with
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | VaArgs | VaArg
⇒
false
_
⇒
true
⇒
match o with
⇒
negbexistsbis_global args
⇒
false
_
⇒
true
_
⇒
match o with
⇒
negbexistsbis_global args
Itop | Alloc_ | Check_ _ _ _ | CheckAhead_ _ _ _ _ | Renew_ _ _ _ | RenewHull_ _ _ _ | HalfCheck_ _ _ _ _ | SpanTest_ _ | RenewIf_ _ _ _ | Limit_ | CheckLimit_ _ _ _ | CheckLocal_ _ _ _ _ | CheckFunction | RawLoadPointer_ _ | VaArgs | VaArg
⇒
false
_
⇒
true
=
true
l :
listclass
Heqo0 :
op_arg_classeso k = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
o0 :
m0 :
Memory.mem
x :
Hb :
bind_resd RValx fr_envfr fr_localsfr m0 = IContinueputd x fr_envfr l′ m0
Heqo2 :
op_reso k l0 m = SomeOpResRValx m0
Heqo3 :
o0 = OpResRValx m0
Es :
special_leto = false
deferred goal
ge :
fr :
m :
Memory.mem
d :
o :
args :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Flightd o args lower = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstFlightd o args lower with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m RawStorew off v a = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

split ; eapply op_res_regions ; eauto | apply env_agree_put

3 open

deferred goal
ge :
fr :
m :
Memory.mem
d :
o :
args :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Flightd o args lower = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstFlightd o args lower with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m RawStorew off v a = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

–simpl in H

3 open

ge :
fr :
m :
Memory.mem
d :
o :
args :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
let* xs ≔ map_optionflight_arg_xge fr_envfr args in
let* a ≔ aluo L xs in
let* c ≔ flight_capge fr_envfr lower in
match a with
⇒
_
⇒
None
=
SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstFlightd o args lower with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m RawStorew off v a = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

cases H

3 open

ge :
fr :
m :
Memory.mem
d :
o :
args :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
l :
listword
Heqo0 :
map_optionflight_arg_xge fr_envfr args = Somel
w :
n :
Z
Heqw0 :
w = WIntn
Heqo1 :
aluo L l = SomeWIntn
c :
Heqo2 :
flight_capge fr_envfr lower = Somec
H :
SomeIContinueputd WPtrptr_addr ≔ n; ptr_cap ≔ c fr_envfr fr_localsfr m = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstFlightd o args lower with
Somed0
⇒
env_agreed0 fr_envfr e′
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m RawStorew off v a = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

injection H as ← ← ←

3 open

ge :
fr :
m :
Memory.mem
d :
o :
args :
Hp :
true = true
l :
listword
Heqo0 :
map_optionflight_arg_xge fr_envfr args = Somel
w :
n :
Z
Heqw0 :
w = WIntn
Heqo1 :
aluo L l = SomeWIntn
c :
Heqo2 :
flight_capge fr_envfr lower = Somec
⊢
∧
match inst_def_firstFlightd o args lower with
Somed0
⇒
None
⇒
putd WPtrptr_addr ≔ n; ptr_cap ≔ c fr_envfr = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m RawStorew off v a = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

split ; reflexivity | apply env_agree_put

2 open

deferred goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
H :
inst_stepge fr m RawStorew off v a = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

–simpl in H

2 open

ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
H :
let* vk ≔ width_value_classw in
let* x ≔ value_xge fr_envfr vk v in
match value_xge fr_envfr A a with
SomeWPtrp
⇒
match store_resw m raw_addressptr_addrp off ptr_capp x with
Somer, m′
⇒
None
⇒
None
_
⇒
None
=
SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

cases H

2 open

ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
Heqo :
w0 :
Heqo0 :
value_xge fr_envfr c v = Somew0
w1 :
p :
Heqw2 :
w1 = WPtrp
Heqo1 :
value_xge fr_envfr A a = SomeWPtrp
p0 :
resunit × Memory.mem
r :
resunit
m0 :
Memory.mem
Heqp1 :
p0 = r, m0
Heqo2 :
store_resw m raw_addressptr_addrp off ptr_capp w0 = Somer, m0
H :
Somestore_outraw_resr fr_envfr fr_localsfr m0 = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

injection H as Hs

2 open

ge :
fr :
m :
Memory.mem
off :
Z
v, a :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
Heqo :
w0 :
Heqo0 :
value_xge fr_envfr c v = Somew0
w1 :
p :
Heqw2 :
w1 = WPtrp
Heqo1 :
value_xge fr_envfr A a = SomeWPtrp
p0 :
resunit × Memory.mem
r :
resunit
m0 :
Memory.mem
Heqp1 :
p0 = r, m0
Heqo2 :
store_resw m raw_addressptr_addrp off ptr_capp w0 = Somer, m0
Hs :
store_outraw_resr fr_envfr fr_localsfr m0 = IContinuee′ l′ m′
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
e′ = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

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

2 open

ge :
fr :
m :
Memory.mem
off :
Z
v, a :
m′ :
Memory.mem
Hp :
match w with
⇒
false
_
⇒
true
=
true
Heqo :
w0 :
Heqo0 :
value_xge fr_envfr c v = Somew0
p :
Heqo1 :
value_xge fr_envfr A a = SomeWPtrp
r :
resunit
Heqo2 :
store_resw m raw_addressptr_addrp off ptr_capp w0 = Somer, m′
x :
unit
Er :
⊢
∧
match inst_def_firstRawStorew off v a with
Somed
⇒
None
⇒
fr_envfr = fr_envfr
deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

split ; eapply store_res_regions ; eauto | reflexivity

deferred goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
inst_stepge fr m Locfile line = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

–simpl in H

ge :
fr :
m :
Memory.mem
file :
line :
Z
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
Hp :
true = true
H :
SomeIContinuefr_envfr fr_localsfr m = SomeIContinuee′ l′ m′
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
e′ = fr_envfr

injection H as ← ← ←

ge :
fr :
m :
Memory.mem
file :
line :
Z
Hp :
true = true
⊢
∧
match inst_def_firstLocfile line with
Somed
⇒
None
⇒
fr_envfr = fr_envfr

simpl

ge :
fr :
m :
Memory.mem
file :
line :
Z
Hp :
true = true
⊢
m_regionsm = m_regionsm ∧ fr_envfr = fr_envfr

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
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

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.

192Theorem evidence_after_holds
∀ ge fr m i e′ l′ m′ 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  ,
→
inst_stepge fr m i = SomeIContinuee′ l′ m′
→
facts_holdge m′ e′
→
match inst_def_firsti with
Somed
⇒
killd fs
None
⇒
fs
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 :
Hs :
inst_stepge fr m i = SomeIContinuee′ l′ m′
⊢
facts_holdge m′ e′
→
match inst_def_firsti with
Somed
⇒
killd fs
None
⇒
fs
else
[ ]

destruct evidence_preservingi eqn: Hp ; | intros fa

ge :
fr :
m :
Memory.mem
i :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
fs :
listfact
H :
Hs :
inst_stepge fr m i = SomeIContinuee′ l′ m′
Hp :
⊢
facts_holdge m′ e′
match inst_def_firsti with
Somed
⇒
killd fs
None
⇒
fs

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

ge :
fr :
m :
Memory.mem
i :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
fs :
listfact
H :
Hs :
inst_stepge fr m i = SomeIContinuee′ l′ m′
Hp :
Hr :
Hd :
match inst_def_firsti with
Somed
⇒
None
⇒
e′ = fr_envfr
⊢
facts_holdge m′ e′
match inst_def_firsti with
Somed
⇒
killd fs
None
⇒
fs

destruct inst_def_firsti as d |

2 open

ge :
fr :
m :
Memory.mem
i :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
fs :
listfact
H :
Hs :
inst_stepge fr m i = SomeIContinuee′ l′ m′
Hp :
Hr :
d :
Hd :
⊢
facts_holdge m′ e′ killd fs
focused goal
ge :
fr :
m :
Memory.mem
i :
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
fs :
listfact
H :
Hs :
inst_stepge fr m i = SomeIContinuee′ l′ m′
Hp :
Hr :
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 :
Hs :
inst_stepge fr m i = SomeIContinuee′ l′ m′
Hp :
Hr :
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 :
Hs :
inst_stepge fr m i = SomeIContinuefr_envfr l′ m′
Hp :
Hr :
⊢
facts_holdge m′ fr_envfr fs

eapply facts_hold_same ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
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.

209Lemma 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
⊢
→
Somef
else
=
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
H0 :
Infa fs
H1 :
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.

222Theorem live_access_not_unchecked
∀ ge fr m i q fs fa why
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 :
H :
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 :
H :
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 :
H :
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 :
⊢
inst_stepge fr m i ≠ SomeIStopUncheckedwhy

rewrite Hq in Eq

ge :
fr :
m :
Memory.mem
i :
q :
fs :
listfact
fa :
why :
H :
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 :
⊢
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.

236Lemma 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.

253Definition check_facti : inst : optionfact ≔
match i with
Letq A Checklo hi r al p | Letq A CheckAheadlo hi r al _ p | Letq A Renewlo hi r al _; p | Letq A RenewHulllo hi r al _; _; p | Letq A HalfCheck_ lo hi r al _; p | Letq A RenewIflo hi r al p; _ | Letq A CheckLimitlo hi r al p; _
⇒
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.

268Definition access_facti : inst : optionfact ≔
match i with
Letq A CheckAheadlo _ r al ahi p
⇒
SomemkFactq p lo ahi r al

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.

276Lemma 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 :
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
⊢
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
⊢
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
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.

289Ltac 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.

302Lemma 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
Objbase
⇒
let* reg ≔ object_regionbase rs in
Some
base ≤? a && a + size ≤? r_endreg
→
a mod al =? 0
→
Robase
⇒
let* reg ≔ object_regionbase rs in
Some
base ≤? a && a + size ≤? r_endreg
→
match r with
⇒
a mod al =? 0
→
⇒
None
≠
SomeRUncheckedwhy

intros c rs a size r al why H

c :
rs :
listregion
a, size :
Z
al :
Z
why :
H :
match c with
Objbase
⇒
let* reg ≔ object_regionbase rs in
Some
base ≤? a && a + size ≤? r_endreg
→
a mod al =? 0
→
Robase
⇒
let* reg ≔ object_regionbase rs in
Some
base ≤? a && a + size ≤? r_endreg
→
match r with
⇒
a mod al =? 0
→
⇒
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
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.

316Lemma 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
intros ge fr m i fa fb e′ l′ m′ Hf Hg H
destruct i as q k o args | | | | | | | ; try discriminate Hf
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 | a1 | a2 | a3 | a4 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.

344Theorem 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 :
Hb :
⊢
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.

359Lemma 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 :
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 :
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 :
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 :
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 :
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
λ 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 :
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
λ 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 :
o :
args :
listvalue
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
l :
listclass
Heqo0 :
op_arg_classeso k = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
o0 :
m0 :
Memory.mem
Heqo3 :
o0 = OpResr m0
Heqo2 :
op_reso k l0 m = SomeOpResr m0
H :
Somebind_resd r fr_envfr fr_localsfr m0 = 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 :
o :
args :
listvalue
e′ :
l′ :
listname × optionZ
m′ :
Memory.mem
l :
listclass
Heqo0 :
op_arg_classeso k = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
o0 :
m0 :
Memory.mem
Heqo3 :
o0 = OpResr m0
Heqo2 :
op_reso k l0 m = SomeOpResr m0
Hb :
bind_resd r fr_envfr fr_localsfr m0 = 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 :
o :
args :
listvalue
l′ :
listname × optionZ
l :
listclass
Heqo0 :
op_arg_classeso k = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
o0 :
m0 :
Memory.mem
x :
Hb :
bind_resd RValx fr_envfr fr_localsfr m0 = IContinueputd x fr_envfr l′ m0
Heqo2 :
op_reso k l0 m = SomeOpResRValx m0
Heqo3 :
o0 = OpResRValx m0
Es :
special_leto = false

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.

382Definition 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
fs

The temporary a phi defines.

388Definition phi_destph : phi : name ≔
match ph with
Phid _ _
⇒
d

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

392Lemma 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 :
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 :
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 :
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 :
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 :
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.

404Lemma phis_fold_none
∀ ge phs pred e0
fold_left
λ acc ph  ⇒
let* e ≔ acc in
match ph with
Phid k pairs
⇒
let* v ≔ lookuppred pairs in
let* x ≔ value_xge e0 k v in
Someputd x e
phs
None
=
None
Explore proof 2 tactics

Initial goal

⊢
∀ ge : genv phs : listphi pred : name e0 : 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 e0 k v in
Someputd x e
phs
None
=
None

intros ge phs pred e0

ge :
phs :
listphi
pred :
e0 :
⊢
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 e0 k v in
Someputd x e
phs
None
=
None

induction phs ; simpl ; auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros ge phs pred e0
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.

417Lemma phis_env_agree
∀ ge phs pred e0 e1 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 e0 k v in
Someputd x e
phs
Somee1
=
Somee
∀ph, Inph phs → name_eqbn phi_destph = false
lookupn e = lookupn e1
Explore proof 9 tactics

Initial goal

⊢
∀ ge : genv phs : listphi pred : name e0 : env e1 e : listname × word  ,
fold_left
λ acc : optionlistname × word ph : phi  ⇒
let* e2 ≔ acc in
match ph with
Phid k pairs
⇒
let* v ≔ lookuppred pairs in
let* x ≔ value_xge e0 k v in
Someputd x e2
phs
Somee1
=
Somee
→
∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e1

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

2 open

ge :
pred :
e0 :
e1, e :
listname × word
H :
Somee1 = Somee
n :
Hn :
∀ph : phi, False → name_eqbn phi_destph = false
⊢
lookupn e = lookupn e1
focused goal
ge :
d :
ps :
listname × value
phs :
listphi
IH :
∀ pred : name e0 : env e1 e : listname × word  ,
fold_left
λ acc : optionlistname × word ph : phi  ⇒
let* e2 ≔ acc in
match ph with
Phid k pairs
⇒
let* v ≔ lookuppred pairs in
let* x ≔ value_xge e0 k v in
Someputd x e2
phs
Somee1
=
Somee
→
∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e1
pred :
e0 :
e1, 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 e0 k v in
Someputd x e
phs
let* v ≔ lookuppred ps in
let* x ≔ value_xge e0 k v in
Someputd x e1
=
Somee
n :
Hn :
∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbn phi_destph = false
⊢
lookupn e = lookupn e1

–injection H as ←

2 open

ge :
pred :
e0 :
e1 :
listname × word
n :
Hn :
∀ph : phi, False → name_eqbn phi_destph = false
⊢
lookupn e1 = lookupn e1
deferred goal
ge :
d :
ps :
listname × value
phs :
listphi
IH :
∀ pred : name e0 : env e1 e : listname × word  ,
fold_left
λ acc : optionlistname × word ph : phi  ⇒
let* e2 ≔ acc in
match ph with
Phid k pairs
⇒
let* v ≔ lookuppred pairs in
let* x ≔ value_xge e0 k v in
Someputd x e2
phs
Somee1
=
Somee
→
∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e1
pred :
e0 :
e1, 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 e0 k v in
Someputd x e
phs
let* v ≔ lookuppred ps in
let* x ≔ value_xge e0 k v in
Someputd x e1
=
Somee
n :
Hn :
∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbn phi_destph = false
⊢
lookupn e = lookupn e1

reflexivity

deferred goal
ge :
d :
ps :
listname × value
phs :
listphi
IH :
∀ pred : name e0 : env e1 e : listname × word  ,
fold_left
λ acc : optionlistname × word ph : phi  ⇒
let* e2 ≔ acc in
match ph with
Phid k pairs
⇒
let* v ≔ lookuppred pairs in
let* x ≔ value_xge e0 k v in
Someputd x e2
phs
Somee1
=
Somee
→
∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e1
pred :
e0 :
e1, 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 e0 k v in
Someputd x e
phs
let* v ≔ lookuppred ps in
let* x ≔ value_xge e0 k v in
Someputd x e1
=
Somee
n :
Hn :
∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbn phi_destph = false
⊢
lookupn e = lookupn e1

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

ge :
d :
ps :
listname × value
phs :
listphi
IH :
∀ pred : name e0 : env e1 e : listname × word  ,
fold_left
λ acc : optionlistname × word ph : phi  ⇒
let* e2 ≔ acc in
match ph with
Phid k pairs
⇒
let* v ≔ lookuppred pairs in
let* x ≔ value_xge e0 k v in
Someputd x e2
phs
Somee1
=
Somee
→
∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e1
pred :
e0 :
e1, 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 e0 k v in
Someputd x e
phs
let* x ≔ value_xge e0 k v in
Someputd x e1
=
Somee
n :
Hn :
∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbn phi_destph = false
⊢
lookupn e = lookupn e1

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

ge :
d :
ps :
listname × value
phs :
listphi
IH :
∀ pred : name e0 : env e1 e : listname × word  ,
fold_left
λ acc : optionlistname × word ph : phi  ⇒
let* e2 ≔ acc in
match ph with
Phid k pairs
⇒
let* v ≔ lookuppred pairs in
let* x ≔ value_xge e0 k v in
Someputd x e2
phs
Somee1
=
Somee
→
∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e1
pred :
e0 :
e1, e :
listname × word
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 e0 k v in
Someputd x e
phs
Someputd x e1
=
Somee
n :
Hn :
∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbn phi_destph = false
⊢
lookupn e = lookupn e1

rewrite IH_ _ _ _ H n by auto

ge :
d :
ps :
listname × value
phs :
listphi
IH :
∀ pred : name e0 : env e1 e : listname × word  ,
fold_left
λ acc : optionlistname × word ph : phi  ⇒
let* e2 ≔ acc in
match ph with
Phid k pairs
⇒
let* v ≔ lookuppred pairs in
let* x ≔ value_xge e0 k v in
Someputd x e2
phs
Somee1
=
Somee
→
∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e1
pred :
e0 :
e1, e :
listname × word
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 e0 k v in
Someputd x e
phs
Someputd x e1
=
Somee
n :
Hn :
∀ph : phi, Phid k ps = ph ∨ Inph phs → name_eqbn phi_destph = false
⊢
lookupn putd x e1 = lookupn e1

apply lookup_put_other

ge :
d :
ps :
listname × value
phs :
listphi
IH :
∀ pred : name e0 : env e1 e : listname × word  ,
fold_left
λ acc : optionlistname × word ph : phi  ⇒
let* e2 ≔ acc in
match ph with
Phid k pairs
⇒
let* v ≔ lookuppred pairs in
let* x ≔ value_xge e0 k v in
Someputd x e2
phs
Somee1
=
Somee
→
∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e1
pred :
e0 :
e1, e :
listname × word
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 e0 k v in
Someputd x e
phs
Someputd x e1
=
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 :
ps :
listname × value
phs :
listphi
IH :
∀ pred : name e0 : env e1 e : listname × word  ,
fold_left
λ acc : optionlistname × word ph : phi  ⇒
let* e2 ≔ acc in
match ph with
Phid k pairs
⇒
let* v ≔ lookuppred pairs in
let* x ≔ value_xge e0 k v in
Someputd x e2
phs
Somee1
=
Somee
→
∀n : name, ∀ph : phi, Inph phs → name_eqbn phi_destph = false → lookupn e = lookupn e1
pred :
e0 :
e1, e :
listname × word
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 e0 k v in
Someputd x e
phs
Someputd x e1
=
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 e0 e1 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 e0 k v as x | ; simpl in H ; | rewrite phis_fold_none in H ; discriminate H
rewrite IH_ _ _ _ H n by auto
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.

438Theorem phis_facts_hold
∀ ge m phs pred e0 e fs
phis_envge phs Somepred e0 = Somee
facts_holdge m e0 fs
Explore proof 16 tactics

Initial goal

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

unfold phis_env

⊢
∀ ge : genv m : Memory.mem phs : listphi pred : name e0 e : env fs : listfact  ,
fold_left
λ acc : optionlistname × word ph : phi  ⇒
let* e1 ≔ acc in
match ph with
Phid k pairs
⇒
let* v ≔ lookuppred pairs in
let* x ≔ value_xge e0 k v in
Someputd x e1
phs
Somee0
=
Somee
→
facts_holdge m e0 fs → facts_holdge m e entry_killphs fs

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

ge :
m :
Memory.mem
phs :
listphi
pred :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 e0 = SomeWPtrp
Ep :
value_xge e0 P f_pfa = SomeWPtrp
Hc :
⊢
fact_holdsge m e fa

exists p

ge :
m :
Memory.mem
phs :
listphi
pred :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 e0 = SomeWPtrp
Ep :
value_xge e0 P f_pfa = SomeWPtrp
Hc :
⊢
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 :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 e0 = SomeWPtrp
Ep :
value_xge e0 P f_pfa = SomeWPtrp
Hc :
⊢
lookupf_qfa e = SomeWPtrp
focused goal
ge :
m :
Memory.mem
phs :
listphi
pred :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 e0 = SomeWPtrp
Ep :
value_xge e0 P f_pfa = SomeWPtrp
Hc :
⊢
value_xge e P f_pfa = SomeWPtrp

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

2 open

ge :
m :
Memory.mem
phs :
listphi
pred :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 e0 = SomeWPtrp
Ep :
value_xge e0 P f_pfa = SomeWPtrp
Hc :
⊢
∀ph : phi, Inph phs → name_eqbf_qfa phi_destph = false
deferred goal
ge :
m :
Memory.mem
phs :
listphi
pred :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 e0 = SomeWPtrp
Ep :
value_xge e0 P f_pfa = SomeWPtrp
Hc :
⊢
value_xge e P f_pfa = SomeWPtrp

intros ph Hi

2 open

ge :
m :
Memory.mem
phs :
listphi
pred :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 e0 = SomeWPtrp
Ep :
value_xge e0 P f_pfa = SomeWPtrp
Hc :
ph :
Hi :
Inph phs
⊢
name_eqbf_qfa phi_destph = false
deferred goal
ge :
m :
Memory.mem
phs :
listphi
pred :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 e0 = SomeWPtrp
Ep :
value_xge e0 P f_pfa = SomeWPtrp
Hc :
⊢
value_xge e P f_pfa = SomeWPtrp

apply Hphph Hi

deferred goal
ge :
m :
Memory.mem
phs :
listphi
pred :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 e0 = SomeWPtrp
Ep :
value_xge e0 P f_pfa = SomeWPtrp
Hc :
⊢
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 :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 e0 = SomeWPtrp
Ep :
value_xge e0 P Tmpn = SomeWPtrp
Hc :
⊢
value_xge e P Tmpn = SomeWPtrp

simpl in *

ge :
m :
Memory.mem
phs :
listphi
pred :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 e0 = SomeWPtrp
Ep :
let* x ≔ lookupn e0 in
Somex
=
SomeWPtrp
Hc :
⊢
let* x ≔ lookupn e in
Somex
=
SomeWPtrp

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

ge :
m :
Memory.mem
phs :
listphi
pred :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 e0 = SomeWPtrp
Ep :
let* x ≔ lookupn e0 in
Somex
=
SomeWPtrp
Hc :
⊢
∀ph : phi, Inph phs → name_eqbn phi_destph = false

intros ph Hi

ge :
m :
Memory.mem
phs :
listphi
pred :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 e0 = SomeWPtrp
Ep :
let* x ≔ lookupn e0 in
Somex
=
SomeWPtrp
Hc :
ph :
Hi :
Inph phs
⊢
name_eqbn phi_destph = false

pose proof proj2Hphph Hi as Hv

ge :
m :
Memory.mem
phs :
listphi
pred :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 e0 = SomeWPtrp
Ep :
let* x ≔ lookupn e0 in
Somex
=
SomeWPtrp
Hc :
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 :
e0, 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 e0 k v in
Someputd x e
phs
Somee0
=
Somee
H :
facts_holdge m e0 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 e0 = SomeWPtrp
Ep :
let* x ≔ lookupn e0 in
Somex
=
SomeWPtrp
Hc :
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 e0 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.

452Lemma 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.

459Lemma 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 :
lo, hi :
Z
al :
Z
q′ :
p′ :
lo′, hi′ :
Z
r′ :
al′ :
Z
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 :
lo, hi :
Z
al :
Z
q′ :
p′ :
lo′, hi′ :
Z
r′ :
al′ :
Z
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 :
lo, hi :
Z
al :
Z
q′ :
p′ :
lo′, hi′ :
Z
r′ :
al′ :
Z
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 :
lo, hi :
Z
al :
Z
q′ :
p′ :
lo′, hi′ :
Z
r′ :
al′ :
Z
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 :
lo, hi :
Z
al :
Z
q′ :
p′ :
lo′, hi′ :
Z
r′ :
al′ :
Z
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 :
lo, hi :
Z
al :
Z
q′ :
p′ :
lo′, hi′ :
Z
r′ :
al′ :
Z
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 :
lo, hi :
Z
al :
Z
q′ :
p′ :
lo′, hi′ :
Z
r′ :
al′ :
Z
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 :
lo, hi :
Z
al :
Z
q′ :
p′ :
lo′, hi′ :
Z
r′ :
al′ :
Z
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 :
lo, hi, al :
Z
q′ :
p′ :
lo′, hi′, al′ :
Z
Hq :
q = q′
Hp :
p = p′
Hl :
lo = lo′
Hh :
hi = hi′
Hr :
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 :
lo, hi, al :
Z
q′ :
p′ :
lo′, hi′, al′ :
Z
Hq :
q = q′
Hp :
p = p′
Hl :
lo = lo′
Hh :
hi = hi′
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.

470Lemma 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
[ ]
⇒
[ ]
s0 :: ss
⇒
filterλf : fact ⇒ forallbλs′ : listfact ⇒ existsbfact_eqbf s′ ss s0
→
Ins sets → Infa s

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

s0 :
listfact
ss :
listlistfact
s :
listfact
fa :
H :
Infa filterλf : fact ⇒ forallbλs′ : listfact ⇒ existsbfact_eqbf s′ ss s0
Hs :
Ins s0 :: ss
⊢
Infa s

apply filter_In in H as H0 Hall

s0 :
listfact
ss :
listlistfact
s :
listfact
fa :
H0 :
Infa s0
Hall :
forallbλs′ : listfact ⇒ existsbfact_eqbfa s′ ss = true
Hs :
Ins s0 :: ss
⊢
Infa s

destruct Hs as ← | Hs ; exact H0 |

s0 :
listfact
ss :
listlistfact
s :
listfact
fa :
H0 :
Infa s0
Hall :
forallbλs′ : listfact ⇒ existsbfact_eqbfa s′ ss = true
Hs :
Ins ss
⊢
Infa s

rewrite forallb_forall in Hall

s0 :
listfact
ss :
listlistfact
s :
listfact
fa :
H0 :
Infa s0
Hall :
∀x : listfact, Inx ss → existsbfact_eqbfa x = true
Hs :
Ins ss
⊢
Infa s

pose proof Halls Hs as Ex

s0 :
listfact
ss :
listlistfact
s :
listfact
fa :
H0 :
Infa s0
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

s0 :
listfact
ss :
listlistfact
s :
listfact
fa :
H0 :
Infa s0
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

s0 :
listfact
ss :
listlistfact
s :
listfact
fa :
H0 :
Infa s0
Hall :
∀x : listfact, Inx ss → existsbfact_eqbfa x = true
Hs :
Ins ss
y :
Hy :
Iny s
E :
fa = y
⊢
Infa s

subst y

s0 :
listfact
ss :
listlistfact
s :
listfact
fa :
H0 :
Infa s0
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
intros | s0 ss s fa H Hs ; destruct H |
apply filter_In in H as H0 Hall
destruct Hs as ← | Hs ; exact H0 |
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.

481Lemma 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  ,

intros c from t c′ H

⊢
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.

493Lemma 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 :
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 :
l, pred :
c′ :
Ha :
fr_atc_framec = Enterl Somepred
H :
match fr_atc_framec with
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
⇒
else
or_stuck"block"
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
⇒
None
⇒
or_stuck"instruction"
let* out0 ≔ inst_stepge c_framec c_memc i in
let* od ≔ doomed_resultge c_framec c_memc i out0 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 :
l, pred :
c′ :
Ha :
fr_atc_framec = Enterl Somepred
H :
else
or_stuck"block"
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 :
l, pred :
c′ :
Ha :
fr_atc_framec = Enterl Somepred
H :
or_stuck"block"
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 :
l, pred :
c′ :
Ha :
fr_atc_framec = Enterl Somepred
H :
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 :
l, pred :
c′ :
Ha :
fr_atc_framec = Enterl Somepred
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
in
=
SomeNextc′
⊢
c_memc′ = c_memc ∧ ∃b0 : block, Someb = Someb0 ∧ phis_envge b_phisb0 Somepred fr_envc_framec = Somefr_envc_framec′ ∧ fr_atc_framec′ = Execl b_instsb0 b_jumpb0

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 :
l, pred :
c′ :
Ha :
fr_atc_framec = Enterl Somepred
e :
H :
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 = SomeNextc′
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 ∧ ∃b0 : block, Someb = Someb0 ∧ phis_envge b_phisb0 Somepred fr_envc_framec = Somefr_envc_framec′ ∧ fr_atc_framec′ = Execl b_instsb0 b_jumpb0

injection H as ←

ge :
l, pred :
Ha :
fr_atc_framec = Enterl Somepred
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 ∧ ∃b0 : block, Someb = Someb0 ∧ phis_envge b_phisb0 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_instsb0 b_jumpb0

simpl

ge :
l, pred :
Ha :
fr_atc_framec = Enterl Somepred
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
⊢
∧
∃ b0 : block  ,
Someb = Someb0
∧
fold_left
λ acc : optionlistname × word ph : phi  ⇒
let* e0 ≔ 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 e0
=
Somee
∧

split ; reflexivity |

ge :
l, pred :
Ha :
fr_atc_framec = Enterl Somepred
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
⊢
∃ b0 : block  ,
Someb = Someb0
∧
fold_left
λ acc : optionlistname × word ph : phi  ⇒
let* e0 ≔ 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 e0
=
Somee
∧

exists b

ge :
l, pred :
Ha :
fr_atc_framec = Enterl Somepred
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* e0 ≔ 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 e0
=
Somee
∧

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.

512Theorem entry_holds
∀ ge c c1 c2 from t sets fs b
Explore proof 11 tactics

Initial goal

⊢
∀ge : genv c c1 c2 : config from : name t : target sets : listlistfact fs : listfact b : block, edge_stepc from t = Nextc1 → stepge c1 = Nextc2 → find_blockedge_labelt fn_blocksfr_fnc_framec1 = Someb → facts_holdge c_memc fr_envc_framec fs → Infs sets → facts_holdge c_memc2 fr_envc_framec2 entry_killb_phisb evidence_meetsets

intros ge c c1 c2 from t sets fs b He Hs Hb H Hin

ge :
c, c1, c2 :
from :
sets :
listlistfact
fs :
listfact
He :
edge_stepc from t = Nextc1
Hs :
stepge c1 = Nextc2
Hin :
Infs sets

destruct edge_step_next_ _ _ _ He as Hm1 & He1 & Ha1

ge :
c, c1, c2 :
from :
sets :
listlistfact
fs :
listfact
He :
edge_stepc from t = Nextc1
Hs :
stepge c1 = Nextc2
Hin :
Infs sets
Hm1 :
c_memc1 = c_memc
Ha1 :

destruct enter_step_ _ _ _ _ Ha1 Hs as Hm2 & b′ & Hb′ & Hp & _

ge :
c, c1, c2 :
from :
sets :
listlistfact
fs :
listfact
He :
edge_stepc from t = Nextc1
Hs :
stepge c1 = Nextc2
Hin :
Infs sets
Hm1 :
c_memc1 = c_memc
Ha1 :
Hm2 :
c_memc2 = c_memc1
b′ :
Hp :
phis_envge b_phisb′ Somefrom fr_envc_framec1 = Somefr_envc_framec2

rewrite Hb in Hb′

ge :
c, c1, c2 :
from :
sets :
listlistfact
fs :
listfact
He :
edge_stepc from t = Nextc1
Hs :
stepge c1 = Nextc2
Hin :
Infs sets
Hm1 :
c_memc1 = c_memc
Ha1 :
Hm2 :
c_memc2 = c_memc1
b′ :
Hb′ :
Someb = Someb′
Hp :
phis_envge b_phisb′ Somefrom fr_envc_framec1 = Somefr_envc_framec2

injection Hb′ as ←

ge :
c, c1, c2 :
from :
sets :
listlistfact
fs :
listfact
He :
edge_stepc from t = Nextc1
Hs :
stepge c1 = Nextc2
Hin :
Infs sets
Hm1 :
c_memc1 = c_memc
Ha1 :
Hm2 :
c_memc2 = c_memc1
Hp :

rewrite Hm2 , Hm1

ge :
c, c1, c2 :
from :
sets :
listlistfact
fs :
listfact
He :
edge_stepc from t = Nextc1
Hs :
stepge c1 = Nextc2
Hin :
Infs sets
Hm1 :
c_memc1 = c_memc
Ha1 :
Hm2 :
c_memc2 = c_memc1
Hp :

eapply phis_facts_hold ; exact Hp |

ge :
c, c1, c2 :
from :
sets :
listlistfact
fs :
listfact
He :
edge_stepc from t = Nextc1
Hs :
stepge c1 = Nextc2
Hin :
Infs sets
Hm1 :
c_memc1 = c_memc
Ha1 :
Hm2 :
c_memc2 = c_memc1
Hp :

rewrite He1

ge :
c, c1, c2 :
from :
sets :
listlistfact
fs :
listfact
He :
edge_stepc from t = Nextc1
Hs :
stepge c1 = Nextc2
Hin :
Infs sets
Hm1 :
c_memc1 = c_memc
Ha1 :
Hm2 :
c_memc2 = c_memc1
Hp :

intros fa Hfa

ge :
c, c1, c2 :
from :
sets :
listlistfact
fs :
listfact
He :
edge_stepc from t = Nextc1
Hs :
stepge c1 = Nextc2
Hin :
Infs sets
Hm1 :
c_memc1 = c_memc
Ha1 :
Hm2 :
c_memc2 = c_memc1
Hp :
fa :
Hfa :
Infa evidence_meetsets

apply H

ge :
c, c1, c2 :
from :
sets :
listlistfact
fs :
listfact
He :
edge_stepc from t = Nextc1
Hs :
stepge c1 = Nextc2
Hin :
Infs sets
Hm1 :
c_memc1 = c_memc
Ha1 :
Hm2 :
c_memc2 = c_memc1
Hp :
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 c1 c2 from t sets fs b He Hs Hb H Hin
destruct edge_step_next_ _ _ _ He as Hm1 & He1 & Ha1
destruct enter_step_ _ _ _ _ Ha1 Hs as Hm2 & b′ & Hb′ & Hp & _
rewrite Hb in Hb′
injection Hb′ as ←
rewrite Hm2 , Hm1
eapply phis_facts_hold ; exact Hp |
rewrite He1
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).

538Definition 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 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.

551Definition 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
Someg1
⇒
→
killd live
else
None
⇒
_
⇒
in
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
Call_ Tmp_ _
⇒
false
unchecked_access
Let_ P Add | Sub | Itop _
⇒
false
implicit_flight
⇒
false
_
⇒
true
in
ok
→
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.

586Lemma 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 :
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 | a1 | a2 | a3 | a4 args ; try reflexivity ; discriminate H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros s i rest live H
destruct i as q k o args | | | | | | | ; try reflexivity
destruct k ; try reflexivity ; destruct o ; try reflexivity ; destruct args as | a1 | a2 | a3 | a4 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.

598Lemma 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
Let_ P Add _ | Let_ P Sub _ | Let_ P Copy Tmp_ | Let_ P Copy Const_ | Let_ P Itop _ | Call_ Tmp_ _ | RawCall_ _ _
⇒
false
_
⇒
true
→
Some
rest
match i with
⇒
match lookupd s_getterss with
Someg1
⇒
→
killd live
else
None
⇒
Letd P Copy Globalg :: _ :: _
⇒
Letd W _ _ | Letd L _ _ | Letd P Add _ | Letd P Sub _ | Letd P Mul _ | Letd P Div _ | Letd P Udiv _ | Letd P Rem _ | Letd P Urem _ | Letd P And _ | Letd P Or _ | Letd P Xor _ | Letd P Sar _ | Letd P Shr _ | Letd P Shl _ | Letd P Neg _ | Letd P Copy [ ] | Letd P Copy Tmp_ :: _ | Letd P Copy Const_ :: _ | Letd P Ptoi _ | Letd P Itop _ | Letd P Cmp_ _ _ | Letd P Ext_ _ | Letd P ExtF_ _ | Letd P Truncd _ | Letd P Truncx _ | Letd P FloatToInt_ _ _ | Letd P IntToFloat_ _ _ | Letd P Cast _ | Letd P Alloc_ _ | Letd P Check_ _ _ _ _ | Letd P CheckAhead_ _ _ _ _ _ | Letd P Renew_ _ _ _ _ | Letd P RenewHull_ _ _ _ _ | Letd P HalfCheck_ _ _ _ _ _ | Letd P SpanTest_ _ _ | Letd P RenewIf_ _ _ _ _ | Letd P Limit_ _ | Letd P CheckLimit_ _ _ _ _ | Letd P CheckLocal_ _ _ _ _ _ | Letd P CheckFunction _ | Letd P RawLoad_ _ _ | Letd P RawLoadPointer_ _ _ | Letd P VaArgs _ | Letd P VaArg _ | Letd A _ _ | Letd F _ _ | Letd Single _ _ | Letd Double _ _ | Letd Extended _ _
⇒
_
⇒
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
Let_ P Add _ | Let_ P Sub _ | Let_ P Copy Tmp_ | Let_ P Copy Const_ | Let_ P Itop _ | Call_ Tmp_ _ | RawCall_ _ _
⇒
false
_
⇒
true
→
Some
rest
match i with
⇒
match lookupd s_getterss with
Someg1
⇒
→
killd live
else
None
⇒
Letd P Copy Globalg :: _ :: _
⇒
Letd W _ _ | Letd L _ _ | Letd P Add _ | Letd P Sub _ | Letd P Mul _ | Letd P Div _ | Letd P Udiv _ | Letd P Rem _ | Letd P Urem _ | Letd P And _ | Letd P Or _ | Letd P Xor _ | Letd P Sar _ | Letd P Shr _ | Letd P Shl _ | Letd P Neg _ | Letd P Copy [ ] | Letd P Copy Tmp_ :: _ | Letd P Copy Const_ :: _ | Letd P Ptoi _ | Letd P Itop _ | Letd P Cmp_ _ _ | Letd P Ext_ _ | Letd P ExtF_ _ | Letd P Truncd _ | Letd P Truncx _ | Letd P FloatToInt_ _ _ | Letd P IntToFloat_ _ _ | Letd P Cast _ | Letd P Alloc_ _ | Letd P Check_ _ _ _ _ | Letd P CheckAhead_ _ _ _ _ _ | Letd P Renew_ _ _ _ _ | Letd P RenewHull_ _ _ _ _ | Letd P HalfCheck_ _ _ _ _ _ | Letd P SpanTest_ _ _ | Letd P RenewIf_ _ _ _ _ | Letd P Limit_ _ | Letd P CheckLimit_ _ _ _ _ | Letd P CheckLocal_ _ _ _ _ _ | Letd P CheckFunction _ | Letd P RawLoad_ _ _ | Letd P RawLoadPointer_ _ _ | Letd P VaArgs _ | Letd P VaArg _ | Letd A _ _ | Letd F _ _ | Letd Single _ _ | Letd Double _ _ | Letd Extended _ _
⇒
_
⇒
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

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
Let_ P Add _ | Let_ P Sub _ | Let_ P Copy Tmp_ | Let_ P Copy Const_ | Let_ P Itop _ | Call_ Tmp_ _ | RawCall_ _ _
⇒
false
_
⇒
true
→
Some
rest
match i with
⇒
match lookupd s_getterss with
Someg1
⇒
→
killd live
else
None
⇒
Letd P Copy Globalg :: _ :: _
⇒
Letd W _ _ | Letd L _ _ | Letd P Add _ | Letd P Sub _ | Letd P Mul _ | Letd P Div _ | Letd P Udiv _ | Letd P Rem _ | Letd P Urem _ | Letd P And _ | Letd P Or _ | Letd P Xor _ | Letd P Sar _ | Letd P Shr _ | Letd P Shl _ | Letd P Neg _ | Letd P Copy [ ] | Letd P Copy Tmp_ :: _ | Letd P Copy Const_ :: _ | Letd P Ptoi _ | Letd P Itop _ | Letd P Cmp_ _ _ | Letd P Ext_ _ | Letd P ExtF_ _ | Letd P Truncd _ | Letd P Truncx _ | Letd P FloatToInt_ _ _ | Letd P IntToFloat_ _ _ | Letd P Cast _ | Letd P Alloc_ _ | Letd P Check_ _ _ _ _ | Letd P CheckAhead_ _ _ _ _ _ | Letd P Renew_ _ _ _ _ | Letd P RenewHull_ _ _ _ _ | Letd P HalfCheck_ _ _ _ _ _ | Letd P SpanTest_ _ _ | Letd P RenewIf_ _ _ _ _ | Letd P Limit_ _ | Letd P CheckLimit_ _ _ _ _ | Letd P CheckLocal_ _ _ _ _ _ | Letd P CheckFunction _ | Letd P RawLoad_ _ _ | Letd P RawLoadPointer_ _ _ | Letd P VaArgs _ | Letd P VaArg _ | Letd A _ _ | Letd F _ _ | Letd Single _ _ | Letd Double _ _ | Letd Extended _ _
⇒
_
⇒
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

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
Let_ P Add _ | Let_ P Sub _ | Let_ P Copy Tmp_ | Let_ P Copy Const_ | Let_ P Itop _ | Call_ Tmp_ _ | RawCall_ _ _
⇒
false
_
⇒
true
=
true
H :
Some
rest
match i with
⇒
match lookupd s_getterss with
Someg1
⇒
→
killd live
else
None
⇒
Letd P Copy Globalg :: _ :: _
⇒
Letd W _ _ | Letd L _ _ | Letd P Add _ | Letd P Sub _ | Letd P Mul _ | Letd P Div _ | Letd P Udiv _ | Letd P Rem _ | Letd P Urem _ | Letd P And _ | Letd P Or _ | Letd P Xor _ | Letd P Sar _ | Letd P Shr _ | Letd P Shl _ | Letd P Neg _ | Letd P Copy [ ] | Letd P Copy Tmp_ :: _ | Letd P Copy Const_ :: _ | Letd P Ptoi _ | Letd P Itop _ | Letd P Cmp_ _ _ | Letd P Ext_ _ | Letd P ExtF_ _ | Letd P Truncd _ | Letd P Truncx _ | Letd P FloatToInt_ _ _ | Letd P IntToFloat_ _ _ | Letd P Cast _ | Letd P Alloc_ _ | Letd P Check_ _ _ _ _ | Letd P CheckAhead_ _ _ _ _ _ | Letd P Renew_ _ _ _ _ | Letd P RenewHull_ _ _ _ _ | Letd P HalfCheck_ _ _ _ _ _ | Letd P SpanTest_ _ _ | Letd P RenewIf_ _ _ _ _ | Letd P Limit_ _ | Letd P CheckLimit_ _ _ _ _ | Letd P CheckLocal_ _ _ _ _ _ | Letd P CheckFunction _ | Letd P RawLoad_ _ _ | Letd P RawLoadPointer_ _ _ | Letd P VaArgs _ | Letd P VaArg _ | Letd A _ _ | Letd F _ _ | Letd Single _ _ | Letd Double _ _ | Letd Extended _ _
⇒
_
⇒
=
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

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
Let_ P Add _ | Let_ P Sub _ | Let_ P Copy Tmp_ | Let_ P Copy Const_ | Let_ P Itop _ | Call_ Tmp_ _ | RawCall_ _ _
⇒
false
_
⇒
true
=
true
⊢
rest = rest
∧
match i with
⇒
match lookupd s_getterss with
Someg1
⇒
→
killd live
else
None
⇒
Letd P Copy Globalg :: _ :: _
⇒
Letd W _ _ | Letd L _ _ | Letd P Add _ | Letd P Sub _ | Letd P Mul _ | Letd P Div _ | Letd P Udiv _ | Letd P Rem _ | Letd P Urem _ | Letd P And _ | Letd P Or _ | Letd P Xor _ | Letd P Sar _ | Letd P Shr _ | Letd P Shl _ | Letd P Neg _ | Letd P Copy [ ] | Letd P Copy Tmp_ :: _ | Letd P Copy Const_ :: _ | Letd P Ptoi _ | Letd P Itop _ | Letd P Cmp_ _ _ | Letd P Ext_ _ | Letd P ExtF_ _ | Letd P Truncd _ | Letd P Truncx _ | Letd P FloatToInt_ _ _ | Letd P IntToFloat_ _ _ | Letd P Cast _ | Letd P Alloc_ _ | Letd P Check_ _ _ _ _ | Letd P CheckAhead_ _ _ _ _ _ | Letd P Renew_ _ _ _ _ | Letd P RenewHull_ _ _ _ _ | Letd P HalfCheck_ _ _ _ _ _ | Letd P SpanTest_ _ _ | Letd P RenewIf_ _ _ _ _ | Letd P Limit_ _ | Letd P CheckLimit_ _ _ _ _ | Letd P CheckLocal_ _ _ _ _ _ | Letd P CheckFunction _ | Letd P RawLoad_ _ _ | Letd P RawLoadPointer_ _ _ | Letd P VaArgs _ | Letd P VaArg _ | Letd A _ _ | Letd F _ _ | Letd Single _ _ | Letd Double _ _ | Letd Extended _ _
⇒
_
⇒
=
∨
∃ d g : name  ,
i = Letd P Copy Globalg
∧
match i with
⇒
match lookupd0 s_getterss with
Someg1
⇒
→
killd0 live
else
None
⇒
Letd0 P Copy Globalg0 :: _ :: _
⇒
Letd0 W _ _ | Letd0 L _ _ | Letd0 P Add _ | Letd0 P Sub _ | Letd0 P Mul _ | Letd0 P Div _ | Letd0 P Udiv _ | Letd0 P Rem _ | Letd0 P Urem _ | Letd0 P And _ | Letd0 P Or _ | Letd0 P Xor _ | Letd0 P Sar _ | Letd0 P Shr _ | Letd0 P Shl _ | Letd0 P Neg _ | Letd0 P Copy [ ] | Letd0 P Copy Tmp_ :: _ | Letd0 P Copy Const_ :: _ | Letd0 P Ptoi _ | Letd0 P Itop _ | Letd0 P Cmp_ _ _ | Letd0 P Ext_ _ | Letd0 P ExtF_ _ | Letd0 P Truncd _ | Letd0 P Truncx _ | Letd0 P FloatToInt_ _ _ | Letd0 P IntToFloat_ _ _ | Letd0 P Cast _ | Letd0 P Alloc_ _ | Letd0 P Check_ _ _ _ _ | Letd0 P CheckAhead_ _ _ _ _ _ | Letd0 P Renew_ _ _ _ _ | Letd0 P RenewHull_ _ _ _ _ | Letd0 P HalfCheck_ _ _ _ _ _ | Letd0 P SpanTest_ _ _ | Letd0 P RenewIf_ _ _ _ _ | Letd0 P Limit_ _ | Letd0 P CheckLimit_ _ _ _ _ | Letd0 P CheckLocal_ _ _ _ _ _ | Letd0 P CheckFunction _ | Letd0 P RawLoad_ _ _ | Letd0 P RawLoadPointer_ _ _ | Letd0 P VaArgs _ | Letd0 P VaArg _ | Letd0 A _ _ | Letd0 F _ _ | Letd0 Single _ _ | Letd0 Double _ _ | Letd0 Extended _ _
⇒
_
⇒
=
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
Let_ P Add _ | Let_ P Sub _ | Let_ P Copy Tmp_ | Let_ P Copy Const_ | Let_ P Itop _ | Call_ Tmp_ _ | RawCall_ _ _
⇒
false
_
⇒
true
=
true
⊢
match i with
⇒
match lookupd s_getterss with
Someg1
⇒
→
killd live
else
None
⇒
Letd P Copy Globalg :: _ :: _
⇒
Letd W _ _ | Letd L _ _ | Letd P Add _ | Letd P Sub _ | Letd P Mul _ | Letd P Div _ | Letd P Udiv _ | Letd P Rem _ | Letd P Urem _ | Letd P And _ | Letd P Or _ | Letd P Xor _ | Letd P Sar _ | Letd P Shr _ | Letd P Shl _ | Letd P Neg _ | Letd P Copy [ ] | Letd P Copy Tmp_ :: _ | Letd P Copy Const_ :: _ | Letd P Ptoi _ | Letd P Itop _ | Letd P Cmp_ _ _ | Letd P Ext_ _ | Letd P ExtF_ _ | Letd P Truncd _ | Letd P Truncx _ | Letd P FloatToInt_ _ _ | Letd P IntToFloat_ _ _ | Letd P Cast _ | Letd P Alloc_ _ | Letd P Check_ _ _ _ _ | Letd P CheckAhead_ _ _ _ _ _ | Letd P Renew_ _ _ _ _ | Letd P RenewHull_ _ _ _ _ | Letd P HalfCheck_ _ _ _ _ _ | Letd P SpanTest_ _ _ | Letd P RenewIf_ _ _ _ _ | Letd P Limit_ _ | Letd P CheckLimit_ _ _ _ _ | Letd P CheckLocal_ _ _ _ _ _ | Letd P CheckFunction _ | Letd P RawLoad_ _ _ | Letd P RawLoadPointer_ _ _ | Letd P VaArgs _ | Letd P VaArg _ | Letd A _ _ | Letd F _ _ | Letd Single _ _ | Letd Double _ _ | Letd Extended _ _
⇒
_
⇒
=
∨
∃ d g : name  ,
i = Letd P Copy Globalg
∧
match i with
⇒
match lookupd0 s_getterss with
Someg1
⇒
→
killd0 live
else
None
⇒
Letd0 P Copy Globalg0 :: _ :: _
⇒
Letd0 W _ _ | Letd0 L _ _ | Letd0 P Add _ | Letd0 P Sub _ | Letd0 P Mul _ | Letd0 P Div _ | Letd0 P Udiv _ | Letd0 P Rem _ | Letd0 P Urem _ | Letd0 P And _ | Letd0 P Or _ | Letd0 P Xor _ | Letd0 P Sar _ | Letd0 P Shr _ | Letd0 P Shl _ | Letd0 P Neg _ | Letd0 P Copy [ ] | Letd0 P Copy Tmp_ :: _ | Letd0 P Copy Const_ :: _ | Letd0 P Ptoi _ | Letd0 P Itop _ | Letd0 P Cmp_ _ _ | Letd0 P Ext_ _ | Letd0 P ExtF_ _ | Letd0 P Truncd _ | Letd0 P Truncx _ | Letd0 P FloatToInt_ _ _ | Letd0 P IntToFloat_ _ _ | Letd0 P Cast _ | Letd0 P Alloc_ _ | Letd0 P Check_ _ _ _ _ | Letd0 P CheckAhead_ _ _ _ _ _ | Letd0 P Renew_ _ _ _ _ | Letd0 P RenewHull_ _ _ _ _ | Letd0 P HalfCheck_ _ _ _ _ _ | Letd0 P SpanTest_ _ _ | Letd0 P RenewIf_ _ _ _ _ | Letd0 P Limit_ _ | Letd0 P CheckLimit_ _ _ _ _ | Letd0 P CheckLocal_ _ _ _ _ _ | Letd0 P CheckFunction _ | Letd0 P RawLoad_ _ _ | Letd0 P RawLoadPointer_ _ _ | Letd0 P VaArgs _ | Letd0 P VaArg _ | Letd0 A _ _ | Letd0 F _ _ | Letd0 Single _ _ | Letd0 Double _ _ | Letd0 Extended _ _
⇒
_
⇒
=
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

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
Let_ P Add _ | Let_ P Sub _ | Let_ P Copy Tmp_ | Let_ P Copy Const_ | Let_ P Itop _ | Call_ Tmp_ _ | RawCall_ _ _
⇒
false
_
⇒
true
=
true
⊢
match i with
⇒
match lookupd s_getterss with
Someg1
⇒
→
killd live
else
None
⇒
Letd P Copy Globalg :: _ :: _
⇒
Letd W _ _ | Letd L _ _ | Letd P Add _ | Letd P Sub _ | Letd P Mul _ | Letd P Div _ | Letd P Udiv _ | Letd P Rem _ | Letd P Urem _ | Letd P And _ | Letd P Or _ | Letd P Xor _ | Letd P Sar _ | Letd P Shr _ | Letd P Shl _ | Letd P Neg _ | Letd P Copy [ ] | Letd P Copy Tmp_ :: _ | Letd P Copy Const_ :: _ | Letd P Ptoi _ | Letd P Itop _ | Letd P Cmp_ _ _ | Letd P Ext_ _ | Letd P ExtF_ _ | Letd P Truncd _ | Letd P Truncx _ | Letd P FloatToInt_ _ _ | Letd P IntToFloat_ _ _ | Letd P Cast _ | Letd P Alloc_ _ | Letd P Check_ _ _ _ _ | Letd P CheckAhead_ _ _ _ _ _ | Letd P Renew_ _ _ _ _ | Letd P RenewHull_ _ _ _ _ | Letd P HalfCheck_ _ _ _ _ _ | Letd P SpanTest_ _ _ | Letd P RenewIf_ _ _ _ _ | Letd P Limit_ _ | Letd P CheckLimit_ _ _ _ _ | Letd P CheckLocal_ _ _ _ _ _ | Letd P CheckFunction _ | Letd P RawLoad_ _ _ | Letd P RawLoadPointer_ _ _ | Letd P VaArgs _ | Letd P VaArg _ | Letd A _ _ | Letd F _ _ | Letd Single _ _ | Letd Double _ _ | Letd Extended _ _
⇒
_
⇒
=
∨
∃ d g : name  ,
i = Letd P Copy Globalg
∧
match i with
⇒
match lookupd0 s_getterss with
Someg1
⇒
→
killd0 live
else
None
⇒
Letd0 P Copy Globalg0 :: _ :: _
⇒
Letd0 W _ _ | Letd0 L _ _ | Letd0 P Add _ | Letd0 P Sub _ | Letd0 P Mul _ | Letd0 P Div _ | Letd0 P Udiv _ | Letd0 P Rem _ | Letd0 P Urem _ | Letd0 P And _ | Letd0 P Or _ | Letd0 P Xor _ | Letd0 P Sar _ | Letd0 P Shr _ | Letd0 P Shl _ | Letd0 P Neg _ | Letd0 P Copy [ ] | Letd0 P Copy Tmp_ :: _ | Letd0 P Copy Const_ :: _ | Letd0 P Ptoi _ | Letd0 P Itop _ | Letd0 P Cmp_ _ _ | Letd0 P Ext_ _ | Letd0 P ExtF_ _ | Letd0 P Truncd _ | Letd0 P Truncx _ | Letd0 P FloatToInt_ _ _ | Letd0 P IntToFloat_ _ _ | Letd0 P Cast _ | Letd0 P Alloc_ _ | Letd0 P Check_ _ _ _ _ | Letd0 P CheckAhead_ _ _ _ _ _ | Letd0 P Renew_ _ _ _ _ | Letd0 P RenewHull_ _ _ _ _ | Letd0 P HalfCheck_ _ _ _ _ _ | Letd0 P SpanTest_ _ _ | Letd0 P RenewIf_ _ _ _ _ | Letd0 P Limit_ _ | Letd0 P CheckLimit_ _ _ _ _ | Letd0 P CheckLocal_ _ _ _ _ _ | Letd0 P CheckFunction _ | Letd0 P RawLoad_ _ _ | Letd0 P RawLoadPointer_ _ _ | Letd0 P VaArgs _ | Letd0 P VaArg _ | Letd0 A _ _ | Letd0 F _ _ | Letd0 Single _ _ | Letd0 Double _ _ | Letd0 Extended _ _
⇒
_
⇒
=
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
Let_ P Add _ | Let_ P Sub _ | Let_ P Copy Tmp_ | Let_ P Copy Const_ | Let_ P Itop _ | Call_ Tmp_ _ | RawCall_ _ _
⇒
false
_
⇒
true
=
true
⊢
∀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

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

2 open

s :
d :
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
⇒
match args with
⇒
false
_
⇒
true
⇒
false
_
⇒
true
_
⇒
true
=
true
⊢
match k with
⇒
match o with
⇒
match args with
⇒
match lookupd s_getterss with
Someg1
⇒
→
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
=
evidence_afterLetd k o args live
∨
∃ d0 g : name  ,
Letd k o args = Letd0 P Copy Globalg
∧
match k with
⇒
match o with
⇒
match args with
⇒
match lookupd s_getterss with
Someg1
⇒
→
killd live
else
evidence_afterLetd k o args live
None
⇒
evidence_afterLetd k o args live
Globalg0 :: _ :: _
⇒
evidence_afterLetd k o args live
_
⇒
evidence_afterLetd k o args live
_
⇒
evidence_afterLetd k o args live
_
⇒
evidence_afterLetd k o args live
=
killd0 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
Let_ P Add _ | Let_ P Sub _ | Let_ P Copy Tmp_ | Let_ P Copy Const_ | Let_ P Itop _ | Call_ Tmp_ _ | RawCall_ _ _
⇒
false
_
⇒
true
=
true
⊢
∀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

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

2 open

s :
d, g :
rest :
listinst
live :
listfact
Hok :
match raw_accessLetd P Copy Globalg with
Someq, x, _, _
⇒
&&
match fact_ofq live with
None
⇒
false
None
⇒
true
=
true
⊢
match lookupd s_getterss with
Someg1
⇒
→
killd live
=
∨
∃ d0 g0 : name  ,
∧
match lookupd s_getterss with
Someg1
⇒
→
killd live
=
killd0 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
Let_ P Add _ | Let_ P Sub _ | Let_ P Copy Tmp_ | Let_ P Copy Const_ | Let_ P Itop _ | Call_ Tmp_ _ | RawCall_ _ _
⇒
false
_
⇒
true
=
true
⊢
∀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

destruct lookupd s_getterss ; auto

2 open

s :
d, g :
rest :
listinst
live :
listfact
Hok :
match raw_accessLetd P Copy Globalg with
Someq, x, _, _
⇒
&&
match fact_ofq live with
None
⇒
false
None
⇒
true
=
true
n :
⊢
∨
∃ d0 g0 : name  ,
∧
=
killd0 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
Let_ P Add _ | Let_ P Sub _ | Let_ P Copy Tmp_ | Let_ P Copy Const_ | Let_ P Itop _ | Call_ Tmp_ _ | RawCall_ _ _
⇒
false
_
⇒
true
=
true
⊢
∀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

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
Let_ P Add _ | Let_ P Sub _ | Let_ P Copy Tmp_ | Let_ P Copy Const_ | Let_ P Itop _ | Call_ Tmp_ _ | RawCall_ _ _
⇒
false
_
⇒
true
=
true
⊢
∀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 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
Let_ P Add _ | Let_ P Sub _ | Let_ P Copy Tmp_ | Let_ P Copy Const_ | Let_ P Itop _ | Call_ Tmp_ _ | RawCall_ _ _
⇒
false
_
⇒
true
=
true
q :
off :
Z
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 :
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 :
Z
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 :
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 :
Z
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 :
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 :
Z
need :
Hr :
raw_accessi = Someq, x, off, need
⊢
∃fa0 : fact, Somefa = Somefa0 ∧ covered_accessi q f_lofa0 f_hifa0 f_rfa0 f_alfa0 = true ∨ hull_coveredi q f_pfa0 f_lofa0 f_alfa0 live s_onces = true

exists fa

s :
i :
rest :
listinst
live :
listfact
q :
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 :
Z
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 :
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 :
Z
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 :
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 :
Z
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
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 i as d k o args | | | | | | | ; auto
destruct k , o ; auto ; destruct args as | n | c | g | a2 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.

619Lemma 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 :
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 | a1 | a2 | a3 | a4 args ; simpl in * ; try discriminate H ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros i fa H
destruct i as q k o args | | | | | | | ; try discriminate H
destruct k , o ; try discriminate H ; destruct args as | a1 | a2 | a3 | a4 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.

631Lemma 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 :
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 | a1 | a2 | a3 | a4 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 :
Z
align :
Z
a1 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
checked_inst_rests Letq A Checklo hi r align a1 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 ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A Checklo hi r align a1 live
focused goal
s :
q :
lo, hi :
Z
align, ahi :
Z
a1 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
checked_inst_rests Letq A CheckAheadlo hi r align ahi a1 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 ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A CheckAheadlo hi r align ahi a1 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
checked_inst_rests Letq A Renewlo hi r align a1; a2 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 ≔ a2; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A Renewlo hi r align a1; a2 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2, a3 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
checked_inst_rests Letq A RenewHulllo hi r align a1; a2; a3 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 ≔ a3; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A RenewHulllo hi r align a1; a2; a3 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
checked_inst_rests Letq A HalfCheckb lo hi r align a1; a2 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 ≔ a2; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A HalfCheckb lo hi r align a1; a2 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
checked_inst_rests Letq A RenewIflo hi r align a1; a2 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 ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A RenewIflo hi r align a1; a2 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
checked_inst_rests Letq A CheckLimitlo hi r align a1; a2 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 ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A CheckLimitlo hi r align a1; a2 live

all: unfold checked_inst_rest in H ; cbn zeta in H

7 open

s :
q :
lo, hi :
Z
align :
Z
a1 :
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 a1 access q a1 lo hi r align live
else
None
=
Somerest′, live′
⊢
∃access : inst, rest = access :: rest′ ∧ proof_useaccess q lo hi r align = true ∧ live′ = evidence_afteraccess f_q ≔ q; f_p ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A Checklo hi r align a1 live
focused goal
s :
q :
lo, hi :
Z
align, ahi :
Z
a1 :
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 a1 access q a1 lo hi r align live
else
None
=
Somerest′, live′
⊢
∃access : inst, rest = access :: rest′ ∧ proof_useaccess q lo ahi r align = true ∧ live′ = evidence_afteraccess f_q ≔ q; f_p ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A CheckAheadlo hi r align ahi a1 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
match a1 with
Tmpn1
⇒
match lookupn1 s_renewss with
Somep1, lo1, hi1, al1
⇒
let* d ≔ pointer_distances_onces a2 Tmpp1 in
negblo1 ≤? lo + d && hi + d ≤? hi1 && al1 mod align =? 0 && lo + d − lo1 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 a1; a2 access q a2 lo hi r align live
else
None
None
⇒
None
_
⇒
None
=
Somerest′, live′
⊢
∃access : inst, rest = access :: rest′ ∧ proof_useaccess q lo hi r align = true ∧ live′ = evidence_afteraccess f_q ≔ q; f_p ≔ a2; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A Renewlo hi r align a1; a2 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2, a3 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
negbhull_renewables_renewss s_onces a3 lo hi align a1 a2
→
None
else
match rest with
[ ]
⇒
None
access :: rest′
⇒
proof_useaccess q lo hi r align
→
Somerest′, after_checkLetq A RenewHulllo hi r align a1; a2; a3 access q a3 lo hi r align live
else
None
=
Somerest′, live′
⊢
∃access : inst, rest = access :: rest′ ∧ proof_useaccess q lo hi r align = true ∧ live′ = evidence_afteraccess f_q ≔ q; f_p ≔ a3; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A RenewHulllo hi r align a1; a2; a3 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
negb
match a1 with
Tmpn1
⇒
match lookupn1 s_renewss with
Somep1, lo1, hi1, _
⇒
match pointer_distances_onces a2 Tmpp1 with
Somed0
⇒
half_knownb lo hi d0 lo1 hi1
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 a1; a2 access q a2 lo hi r align live
else
None
=
Somerest′, live′
⊢
∃access : inst, rest = access :: rest′ ∧ proof_useaccess q lo hi r align = true ∧ live′ = evidence_afteraccess f_q ≔ q; f_p ≔ a2; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A HalfCheckb lo hi r align a1; a2 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
negbguard_coverss_onces a1 a2 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 a1; a2 access q a1 lo hi r align live
else
None
=
Somerest′, live′
⊢
∃access : inst, rest = access :: rest′ ∧ proof_useaccess q lo hi r align = true ∧ live′ = evidence_afteraccess f_q ≔ q; f_p ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A RenewIflo hi r align a1; a2 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
negblimit_coverss_onces a1 a2 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 a1; a2 access q a1 lo hi r align live
else
None
=
Somerest′, live′
⊢
∃access : inst, rest = access :: rest′ ∧ proof_useaccess q lo hi r align = true ∧ live′ = evidence_afteraccess f_q ≔ q; f_p ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A CheckLimitlo hi r align a1; a2 live

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

7 open

s :
q :
lo, hi :
Z
align :
Z
a1 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Heqb :
negbtrue = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
proof_usei q lo hi r align = true
H :
Somel, after_checkLetq A Checklo hi r align a1 i q a1 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 ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A Checklo hi r align a1 live
focused goal
s :
q :
lo, hi :
Z
align, ahi :
Z
a1 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Heqb :
negbmemq s_aheads = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
proof_usei q lo ahi r align && ahead_transparenti = true
H :
Somel, after_checkLetq A CheckAheadlo hi r align ahi a1 i q a1 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 ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A CheckAheadlo hi r align ahi a1 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
n :
Heqv :
a1 = Tmpn
p :
name × Z × Z × Z
p0 :
name × Z × Z
z :
Z
p1 :
name × Z
z0 :
Z
n0 :
z1 :
Z
Heqp2 :
p1 = n0, z1
Heqp1 :
p0 = n0, z1, z0
Heqp0 :
p = n0, z1, z0, z
Heqo :
lookupn s_renewss = Somen0, z1, z0, z
z2 :
Z
Heqo0 :
pointer_distances_onces a2 Tmpn0 = Somez2
Heqb :
negbz1 ≤? lo + z2 && hi + z2 ≤? z0 && z mod align =? 0 && lo + z2 − z1 mod align =? 0 = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
proof_usei q lo hi r align = true
H :
Somel, after_checkLetq A Renewlo hi r align Tmpn; a2 i q a2 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 ≔ a2; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A Renewlo hi r align Tmpn; a2 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2, a3 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Heqb :
negbhull_renewables_renewss s_onces a3 lo hi align a1 a2 = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
proof_usei q lo hi r align = true
H :
Somel, after_checkLetq A RenewHulllo hi r align a1; a2; a3 i q a3 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 ≔ a3; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A RenewHulllo hi r align a1; a2; a3 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Heqb0 :
negb
match a1 with
Tmpn1
⇒
match lookupn1 s_renewss with
Somep1, lo1, hi1, _
⇒
match pointer_distances_onces a2 Tmpp1 with
Somed0
⇒
half_knownb lo hi d0 lo1 hi1
None
⇒
false
None
⇒
false
_
⇒
false
=
false
i :
l :
listinst
Heql :
rest = i :: l
Heqb1 :
proof_usei q lo hi r align = true
H :
Somel, after_checkLetq A HalfCheckb lo hi r align a1; a2 i q a2 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 ≔ a2; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A HalfCheckb lo hi r align a1; a2 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Heqb :
negbguard_coverss_onces a1 a2 lo hi = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
proof_usei q lo hi r align = true
H :
Somel, after_checkLetq A RenewIflo hi r align a1; a2 i q a1 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 ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A RenewIflo hi r align a1; a2 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Heqb :
negblimit_coverss_onces a1 a2 lo hi = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
proof_usei q lo hi r align = true
H :
Somel, after_checkLetq A CheckLimitlo hi r align a1; a2 i q a1 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 ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A CheckLimitlo hi r align a1; a2 live

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

7 open

s :
q :
lo, hi :
Z
align :
Z
a1 :
rest :
listinst
live :
listfact
Heqb :
negbtrue = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
proof_usei q lo hi r align = true
⊢
proof_usei q lo hi r align = true ∧ after_checkLetq A Checklo hi r align a1 i q a1 lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A Checklo hi r align a1 live
focused goal
s :
q :
lo, hi :
Z
align, ahi :
Z
a1 :
rest :
listinst
live :
listfact
Heqb :
negbmemq s_aheads = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
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 a1 i q a1 lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A CheckAheadlo hi r align ahi a1 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
n :
Heqv :
a1 = Tmpn
p :
name × Z × Z × Z
p0 :
name × Z × Z
z :
Z
p1 :
name × Z
z0 :
Z
n0 :
z1 :
Z
Heqp2 :
p1 = n0, z1
Heqp1 :
p0 = n0, z1, z0
Heqp0 :
p = n0, z1, z0, z
Heqo :
lookupn s_renewss = Somen0, z1, z0, z
z2 :
Z
Heqo0 :
pointer_distances_onces a2 Tmpn0 = Somez2
Heqb :
negbz1 ≤? lo + z2 && hi + z2 ≤? z0 && z mod align =? 0 && lo + z2 − z1 mod align =? 0 = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
proof_usei q lo hi r align = true
⊢
proof_usei q lo hi r align = true ∧ after_checkLetq A Renewlo hi r align Tmpn; a2 i q a2 lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a2; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A Renewlo hi r align Tmpn; a2 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2, a3 :
rest :
listinst
live :
listfact
Heqb :
negbhull_renewables_renewss s_onces a3 lo hi align a1 a2 = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
proof_usei q lo hi r align = true
⊢
proof_usei q lo hi r align = true ∧ after_checkLetq A RenewHulllo hi r align a1; a2; a3 i q a3 lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a3; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A RenewHulllo hi r align a1; a2; a3 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
Heqb0 :
negb
match a1 with
Tmpn1
⇒
match lookupn1 s_renewss with
Somep1, lo1, hi1, _
⇒
match pointer_distances_onces a2 Tmpp1 with
Somed0
⇒
half_knownb lo hi d0 lo1 hi1
None
⇒
false
None
⇒
false
_
⇒
false
=
false
i :
l :
listinst
Heql :
rest = i :: l
Heqb1 :
proof_usei q lo hi r align = true
⊢
proof_usei q lo hi r align = true ∧ after_checkLetq A HalfCheckb lo hi r align a1; a2 i q a2 lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a2; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A HalfCheckb lo hi r align a1; a2 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
Heqb :
negbguard_coverss_onces a1 a2 lo hi = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
proof_usei q lo hi r align = true
⊢
proof_usei q lo hi r align = true ∧ after_checkLetq A RenewIflo hi r align a1; a2 i q a1 lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A RenewIflo hi r align a1; a2 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
Heqb :
negblimit_coverss_onces a1 a2 lo hi = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
proof_usei q lo hi r align = true
⊢
proof_usei q lo hi r align = true ∧ after_checkLetq A CheckLimitlo hi r align a1; a2 i q a1 lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A CheckLimitlo hi r align a1; a2 live

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

7 open

s :
q :
lo, hi :
Z
align :
Z
a1 :
rest :
listinst
live :
listfact
Heqb :
negbtrue = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
proof_usei q lo hi r align = true
⊢
proof_usei q lo hi r align = true ∧ after_checkLetq A Checklo hi r align a1 i q a1 lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A Checklo hi r align a1 live
focused goal
s :
q :
lo, hi :
Z
align, ahi :
Z
a1 :
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
H0 :
⊢
proof_usei q lo ahi r align = true ∧ after_checkLetq A CheckAheadlo hi r align ahi a1 i q a1 lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A CheckAheadlo hi r align ahi a1 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
n :
Heqv :
a1 = Tmpn
p :
name × Z × Z × Z
p0 :
name × Z × Z
z :
Z
p1 :
name × Z
z0 :
Z
n0 :
z1 :
Z
Heqp2 :
p1 = n0, z1
Heqp1 :
p0 = n0, z1, z0
Heqp0 :
p = n0, z1, z0, z
Heqo :
lookupn s_renewss = Somen0, z1, z0, z
z2 :
Z
Heqo0 :
pointer_distances_onces a2 Tmpn0 = Somez2
Heqb :
negbz1 ≤? lo + z2 && hi + z2 ≤? z0 && z mod align =? 0 && lo + z2 − z1 mod align =? 0 = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
proof_usei q lo hi r align = true
⊢
proof_usei q lo hi r align = true ∧ after_checkLetq A Renewlo hi r align Tmpn; a2 i q a2 lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a2; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A Renewlo hi r align Tmpn; a2 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2, a3 :
rest :
listinst
live :
listfact
Heqb :
negbhull_renewables_renewss s_onces a3 lo hi align a1 a2 = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
proof_usei q lo hi r align = true
⊢
proof_usei q lo hi r align = true ∧ after_checkLetq A RenewHulllo hi r align a1; a2; a3 i q a3 lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a3; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A RenewHulllo hi r align a1; a2; a3 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
Heqb0 :
negb
match a1 with
Tmpn1
⇒
match lookupn1 s_renewss with
Somep1, lo1, hi1, _
⇒
match pointer_distances_onces a2 Tmpp1 with
Somed0
⇒
half_knownb lo hi d0 lo1 hi1
None
⇒
false
None
⇒
false
_
⇒
false
=
false
i :
l :
listinst
Heql :
rest = i :: l
Heqb1 :
proof_usei q lo hi r align = true
⊢
proof_usei q lo hi r align = true ∧ after_checkLetq A HalfCheckb lo hi r align a1; a2 i q a2 lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a2; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A HalfCheckb lo hi r align a1; a2 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
Heqb :
negbguard_coverss_onces a1 a2 lo hi = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
proof_usei q lo hi r align = true
⊢
proof_usei q lo hi r align = true ∧ after_checkLetq A RenewIflo hi r align a1; a2 i q a1 lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A RenewIflo hi r align a1; a2 live
focused goal
s :
q :
lo, hi :
Z
align :
Z
a1, a2 :
rest :
listinst
live :
listfact
Heqb :
negblimit_coverss_onces a1 a2 lo hi = false
i :
l :
listinst
Heql :
rest = i :: l
Heqb0 :
proof_usei q lo hi r align = true
⊢
proof_usei q lo hi r align = true ∧ after_checkLetq A CheckLimitlo hi r align a1; a2 i q a1 lo hi r align live = evidence_afteri f_q ≔ q; f_p ≔ a1; f_lo ≔ lo; f_hi ≔ hi; f_r ≔ r; f_al ≔ align :: evidence_afterLetq A CheckLimitlo hi r align a1; a2 live

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 i as q k o args | | | | | | | ; try discriminate Hf
destruct k ; try destruct o ; discriminate Hf
destruct o ; try discriminate Hf ; destruct args as | a1 | a2 | a3 | a4 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.

655Lemma 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 :
Z
al :
Z
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 :
Z
al :
Z
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
⇒
None
=
Somerest′, live′
⊢
∃access : inst, rest = access :: rest′ ∧ live′ = evidence_afteraccess killq live

cbn zeta in H

s :
q, x :
off, bytes :
Z
al :
Z
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
⇒
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 :
Z
al :
Z
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
i :
l :
listinst
Heql :
rest = i :: l
p :
name × access_type × Z × rights
p0 :
name × access_type × Z
r0 :
z :
Z
n :
Heqp2 :
p1 = n, a
Heqz0 :
z = 0
Heqp1 :
p0 = n, a, 0
Heqp0 :
p = n, a, 0, r0
Heqo :
raw_accessi = Somen, a, 0, r0
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 :
Z
al :
Z
rest :
listinst
live :
listfact
i :
l :
listinst
Heql :
rest = i :: l
p :
name × access_type × Z × rights
p0 :
name × access_type × Z
r0 :
z :
Z
n :
Heqp2 :
p1 = n, a
Heqz0 :
z = 0
Heqp1 :
p0 = n, a, 0
Heqp0 :
p = n, a, 0, r0
Heqo :
raw_accessi = Somen, a, 0, r0
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.

667Lemma 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
n :
args0 :
listarg
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
Somerest, [ ] = Somerest′, live′
⊢
live′ = [ ]

injection H as _ ←

s :
q :
args :
listvalue
n :
args0 :
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.

680Theorem checked_inst_holds
∀ ge s fr m i rest live rest′ live′ e1 l1 m1
facts_holdge m fr_envfr live
checked_inst_rests i rest live = Somerest′, live′
inst_stepge fr m i = SomeIContinuee1 l1 m1
rest′ = rest ∧ facts_holdge m1 e1 live′ ∨ ∃access, rest = access :: rest′ ∧ ∀fr1 e2 l2 m2, fr_envfr1 = e1 → inst_stepge fr1 m1 access = SomeIContinuee2 l2 m2 → facts_holdge m2 e2 live′
Proof 43 steps Qed
intros ge s fr m i rest live rest′ live′ e1 l1 m1 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 fr1 e2 l2 m2 He Ha
eapply evidence_after_holds ; | exact Ha
rewrite He
+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 i as q k o args | | | | | | | ; try discriminate 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 fr1 e2 l2 m2 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 rest0 ; 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 fr1 e2 l2 m2 _ _ 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

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

724Theorem checked_access_not_unchecked
∀ ge s fr m i rest live rest′ live′ e1 l1 m1 fr1 access why
check_facti ≠ None
checked_inst_rests i access :: rest live = Somerest′, live′
inst_stepge fr m i = SomeIContinuee1 l1 m1
fr_envfr1 = e1
inst_stepge fr1 m1 access ≠ SomeIStopUncheckedwhy
Explore proof 9 tactics

Initial goal

⊢
∀ge : genv s : src fr : frame m : Memory.mem i : inst rest : listinst live : listfact rest′ : listinst live′ : listfact e1 : env l1 : listname × optionZ m1 : Memory.mem fr1 : frame access : inst why : reason, objects_fitm_regionsm1 → check_facti ≠ None → checked_inst_rests i access :: rest live = Somerest′, live′ → inst_stepge fr m i = SomeIContinuee1 l1 m1 → fr_envfr1 = e1 → inst_stepge fr1 m1 access ≠ SomeIStopUncheckedwhy

intros ge s fr m i rest live rest′ live′ e1 l1 m1 fr1 access why Hfit Hf Hc Hs He

ge :
s :
fr :
m :
Memory.mem
i :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
fr1 :
access :
why :
Hf :
check_facti ≠ None
Hc :
checked_inst_rests i access :: rest live = Somerest′, live′
Hs :
inst_stepge fr m i = SomeIContinuee1 l1 m1
He :
fr_envfr1 = e1
⊢
inst_stepge fr1 m1 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
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
fr1 :
access :
why :
fa :
Ef :
check_facti = Somefa
Hf :
Somefa ≠ None
Hc :
checked_inst_rests i access :: rest live = Somerest′, live′
Hs :
inst_stepge fr m i = SomeIContinuee1 l1 m1
He :
fr_envfr1 = e1
⊢
inst_stepge fr1 m1 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
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
fr1 :
access :
why :
fa :
Ef :
check_facti = Somefa
Hf :
Somefa ≠ None
Hc :
checked_inst_rests i access :: rest live = Somerest′, live′
Hs :
inst_stepge fr m i = SomeIContinuee1 l1 m1
He :
fr_envfr1 = e1
fb :
Hg :
access_facti = Somefb
⊢
inst_stepge fr1 m1 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
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
fr1 :
access :
why :
fa :
Ef :
check_facti = Somefa
Hf :
Somefa ≠ None
Hc :
checked_inst_rests i access :: rest live = Somerest′, live′
Hs :
inst_stepge fr m i = SomeIContinuee1 l1 m1
He :
fr_envfr1 = e1
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 fr1 m1 access ≠ SomeIStopUncheckedwhy

injection E as ← _

ge :
s :
fr :
m :
Memory.mem
i :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
fr1 :
access :
why :
fa :
Ef :
check_facti = Somefa
Hf :
Somefa ≠ None
Hc :
checked_inst_rests i access :: rest live = Somerest′, live′
Hs :
inst_stepge fr m i = SomeIContinuee1 l1 m1
He :
fr_envfr1 = e1
fb :
Hg :
access_facti = Somefb
Hu :
proof_useaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true
⊢
inst_stepge fr1 m1 access ≠ SomeIStopUncheckedwhy

apply andb_true_iff in Hu as Hcov _

ge :
s :
fr :
m :
Memory.mem
i :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
fr1 :
access :
why :
fa :
Ef :
check_facti = Somefa
Hf :
Somefa ≠ None
Hc :
checked_inst_rests i access :: rest live = Somerest′, live′
Hs :
inst_stepge fr m i = SomeIContinuee1 l1 m1
He :
fr_envfr1 = e1
fb :
Hg :
access_facti = Somefb
Hcov :
covered_accessaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true
⊢
inst_stepge fr1 m1 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
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
fr1 :
access :
why :
fa :
Ef :
check_facti = Somefa
Hf :
Somefa ≠ None
Hc :
checked_inst_rests i access :: rest live = Somerest′, live′
Hs :
inst_stepge fr m i = SomeIContinuee1 l1 m1
He :
fr_envfr1 = e1
fb :
Hg :
access_facti = Somefb
Hcov :
covered_accessaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true
p :
Eq :
lookupf_qfb e1 = SomeWPtrp
Hp :
⊢
inst_stepge fr1 m1 access ≠ SomeIStopUncheckedwhy

rewrite <- He in Eq

ge :
s :
fr :
m :
Memory.mem
i :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
fr1 :
access :
why :
fa :
Ef :
check_facti = Somefa
Hf :
Somefa ≠ None
Hc :
checked_inst_rests i access :: rest live = Somerest′, live′
Hs :
inst_stepge fr m i = SomeIContinuee1 l1 m1
He :
fr_envfr1 = e1
fb :
Hg :
access_facti = Somefb
Hcov :
covered_accessaccess f_qfb f_lofb f_hifb f_rfb f_alfb = true
p :
Eq :
lookupf_qfb fr_envfr1 = SomeWPtrp
Hp :
⊢
inst_stepge fr1 m1 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′ e1 l1 m1 fr1 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 ← _
apply andb_true_iff in Hu as Hcov _
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.

748Theorem generic_access_not_unchecked
∀ ge s fr m i rest live rest′ live′ q x off need why
facts_holdge m fr_envfr live
pass_speciali = false
checked_inst_rests i rest live = Somerest′, live′
raw_accessi = Someq, x, off, need
inst_stepge fr m i ≠ SomeIStopUncheckedwhy ∨ ∃fa, fact_ofq live = Somefa ∧ hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true
Explore proof 5 tactics

Initial goal

⊢
∀ge : genv s : src fr : frame m : Memory.mem i : inst rest : listinst live : listfact rest′ : listinst live′ : listfact q : name x : access_type off : Z need : rights why : reason, objects_fitm_regionsm → facts_holdge m fr_envfr live → pass_speciali = false → checked_inst_rests i rest live = Somerest′, live′ → raw_accessi = Someq, x, off, need → inst_stepge fr m i ≠ SomeIStopUncheckedwhy ∨ ∃fa : fact, fact_ofq live = Somefa ∧ hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

intros ge s fr m i rest live rest′ live′ q x off need why Hfit Hl Hp Hc Hr

ge :
s :
fr :
m :
Memory.mem
i :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
q :
off :
Z
need :
why :
Hl :
facts_holdge m fr_envfr live
Hp :
pass_speciali = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hr :
raw_accessi = Someq, x, off, need
⊢
inst_stepge fr m i ≠ SomeIStopUncheckedwhy ∨ ∃fa : fact, fact_ofq live = Somefa ∧ hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

rewrite checked_inst_rest_generic_ _ _ _ Hp in Hc

ge :
s :
fr :
m :
Memory.mem
i :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
q :
off :
Z
need :
why :
Hl :
facts_holdge m fr_envfr live
Hp :
pass_speciali = false
Hc :
generic_rests i rest live = Somerest′, live′
Hr :
raw_accessi = Someq, x, off, need
⊢
inst_stepge fr m i ≠ SomeIStopUncheckedwhy ∨ ∃fa : fact, fact_ofq live = Somefa ∧ hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

destruct generic_rest_shape_ _ _ _ _ _ Hc as _ & _ & Ha

ge :
s :
fr :
m :
Memory.mem
i :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
q :
off :
Z
need :
why :
Hl :
facts_holdge m fr_envfr live
Hp :
pass_speciali = false
Hc :
generic_rests i rest live = Somerest′, live′
Hr :
raw_accessi = Someq, x, off, need
Ha :
∀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
⊢
inst_stepge fr m i ≠ SomeIStopUncheckedwhy ∨ ∃fa : fact, fact_ofq live = Somefa ∧ hull_coveredi q f_pfa f_lofa f_alfa live s_onces = true

destruct Ha_ _ _ _ Hr as fa & Hfa & Hcov | Hh ; left | right ; eauto

ge :
s :
fr :
m :
Memory.mem
i :
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
q :
off :
Z
need :
why :
Hl :
facts_holdge m fr_envfr live
Hp :
pass_speciali = false
Hc :
generic_rests i rest live = Somerest′, live′
Hr :
raw_accessi = Someq, x, off, need
Ha :
∀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
fa :
Hfa :
fact_ofq live = Somefa
Hcov :
covered_accessi q f_lofa f_hifa f_rfa f_alfa = true
⊢
inst_stepge fr m i ≠ SomeIStopUncheckedwhy

eapply live_access_not_unchecked ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros ge s fr m i rest live rest′ live′ q x off need why Hfit Hl Hp Hc Hr
rewrite checked_inst_rest_generic_ _ _ _ Hp in Hc
destruct generic_rest_shape_ _ _ _ _ _ Hc as _ & _ & Ha
destruct Ha_ _ _ _ Hr as fa & Hfa & Hcov | Hh ; left | right ; eauto