Fil-C on Nix

Filnix wiki

the formal campaign

rocq/theories/Walk.v

The evidence pass read back for Campaign 3's run-level invariant (Persistence.v; rocq.md, The evidence invariant over runs).

Validate.v's evidence_pass transcribes ir.pl's pass as it runs: a fold over the blocks, and within each block checked_insts/5. The invariant needs to know what the pass said at each point a run can reach, so this file reads the pass back: the facts each block was passed from (pass_fold), where the pass is within a block (walks), and the instructions before which it keeps its facts (relies).

A block reached by a back edge saw nothing on that edge (the fold had not reached its source), and the meet over an empty set is empty: a back edge without a poll gives no fact the proof must justify.

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

Names

Every name equals itself by name_eqb.

26Lemma name_eqb_refl
∀ n
name_eqbn n = true
Explore proof 1 tactics

Initial goal

⊢
∀n : name, name_eqbn n = true

exact term_eqb_refl

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
exact term_eqb_refl

name_eqb is symmetric.

30Lemma name_eqb_sym
∀ a b
name_eqba b = name_eqbb a
Explore proof 10 tactics

Initial goal

⊢
∀a b : name, name_eqba b = name_eqbb a

intros a b

a, b :
name
⊢
name_eqba b = name_eqbb a

destruct name_eqba b eqn: E , name_eqbb a eqn: E′ ; auto

2 open

a, b :
name
E :
name_eqba b = true
E′ :
name_eqbb a = false
⊢
true = false
focused goal
a, b :
name
E :
name_eqba b = false
E′ :
name_eqbb a = true
⊢
false = true

–apply term_eqb_eq in E

2 open

a, b :
name
E :
a = b
E′ :
name_eqbb a = false
⊢
true = false
deferred goal
a, b :
name
E :
name_eqba b = false
E′ :
name_eqbb a = true
⊢
false = true

subst

2 open

b :
name
E′ :
name_eqbb b = false
⊢
true = false
deferred goal
a, b :
name
E :
name_eqba b = false
E′ :
name_eqbb a = true
⊢
false = true

rewrite name_eqb_refl in E′

2 open

b :
name
E′ :
true = false
⊢
true = false
deferred goal
a, b :
name
E :
name_eqba b = false
E′ :
name_eqbb a = true
⊢
false = true

discriminate E′

deferred goal
a, b :
name
E :
name_eqba b = false
E′ :
name_eqbb a = true
⊢
false = true

–apply term_eqb_eq in E′

a, b :
name
E :
name_eqba b = false
E′ :
b = a
⊢
false = true

subst

a :
name
E :
name_eqba a = false
⊢
false = true

rewrite name_eqb_refl in E

a :
name
E :
true = false
⊢
false = true

discriminate E

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros a b
destruct name_eqba b eqn: E , name_eqbb a eqn: E′ ; auto
–apply term_eqb_eq in E
subst
rewrite name_eqb_refl in E′
discriminate E′
–apply term_eqb_eq in E′
subst
rewrite name_eqb_refl in E
discriminate E

If n is not in the list ns by mem, name_eqb finds n different from every name of ns.

39Lemma mem_false
∀ n ns n′
memn ns = false
Inn′ ns
name_eqbn n′ = false
Explore proof 7 tactics

Initial goal

⊢
∀n : name ns : listname, memn ns = false → ∀n′ : name, Inn′ ns → name_eqbn n′ = false

unfold mem

⊢
∀n : name ns : listname, existsbname_eqbn ns = false → ∀n′ : name, Inn′ ns → name_eqbn n′ = false

intros n ns H n′ Hin

n :
name
ns :
listname
H :
existsbname_eqbn ns = false
n′ :
name
Hin :
Inn′ ns
⊢
name_eqbn n′ = false

destruct name_eqbn n′ eqn: E ; auto

n :
name
ns :
listname
H :
existsbname_eqbn ns = false
n′ :
name
Hin :
Inn′ ns
E :
name_eqbn n′ = true
⊢
true = false

rewrite <- H

n :
name
ns :
listname
H :
existsbname_eqbn ns = false
n′ :
name
Hin :
Inn′ ns
E :
name_eqbn n′ = true
⊢
true = existsbname_eqbn ns

symmetry

n :
name
ns :
listname
H :
existsbname_eqbn ns = false
n′ :
name
Hin :
Inn′ ns
E :
name_eqbn n′ = true
⊢
existsbname_eqbn ns = true

apply existsb_exists

n :
name
ns :
listname
H :
existsbname_eqbn ns = false
n′ :
name
Hin :
Inn′ ns
E :
name_eqbn n′ = true
⊢
∃x : name, Inx ns ∧ name_eqbn x = true

eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
unfold mem
intros n ns H n′ Hin
destruct name_eqbn n′ eqn: E ; auto
rewrite <- H
symmetry
apply existsb_exists
eauto

Looking k up after put k' v answers v if k is k', and otherwise what it answered before.

47Lemma lookup_put
∀ A : Type k k′ v : A ps
lookupk putk′ v ps
=
name_eqbk k′
→
Somev
else
lookupk ps
Explore proof 7 tactics

Initial goal

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

intros A k k′ v ps

A :
Type
k, k′ :
name
v :
A
ps :
listname × A
⊢
lookupk putk′ v ps
=
name_eqbk k′
→
Somev
else
lookupk ps

destruct name_eqbk k′ eqn: E

2 open

A :
Type
k, k′ :
name
v :
A
ps :
listname × A
E :
name_eqbk k′ = true
⊢
lookupk putk′ v ps = Somev
focused goal
A :
Type
k, k′ :
name
v :
A
ps :
listname × A
E :
name_eqbk k′ = false
⊢
lookupk putk′ v ps = lookupk ps

–apply term_eqb_eq in E

2 open

A :
Type
k, k′ :
name
v :
A
ps :
listname × A
E :
k = k′
⊢
lookupk putk′ v ps = Somev
deferred goal
A :
Type
k, k′ :
name
v :
A
ps :
listname × A
E :
name_eqbk k′ = false
⊢
lookupk putk′ v ps = lookupk ps

subst

2 open

A :
Type
k′ :
name
v :
A
ps :
listname × A
⊢
lookupk′ putk′ v ps = Somev
deferred goal
A :
Type
k, k′ :
name
v :
A
ps :
listname × A
E :
name_eqbk k′ = false
⊢
lookupk putk′ v ps = lookupk ps

apply lookup_put_same

deferred goal
A :
Type
k, k′ :
name
v :
A
ps :
listname × A
E :
name_eqbk k′ = false
⊢
lookupk putk′ v ps = lookupk ps

–apply lookup_put_other

A :
Type
k, k′ :
name
v :
A
ps :
listname × A
E :
name_eqbk k′ = false
⊢
name_eqbk k′ = false

exact E

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros A k k′ v ps
destruct name_eqbk k′ eqn: E
–apply term_eqb_eq in E
subst
apply lookup_put_same
–apply lookup_put_other
exact E

The block that the label l finds in the blocks bs (find_block) is one of bs and is labelled l.

57Lemma find_block_in
∀ l bs b
find_blockl bs = Someb
Inb bs ∧ b_labelb = l
Explore proof 6 tactics

Initial goal

⊢
∀l : name bs : listblock b : block, find_blockl bs = Someb → Inb bs ∧ b_labelb = l

induction bs as | b0 bs IH ; simpl ; intros b H ; discriminate H |

l :
name
b0 :
block
bs :
listblock
IH :
∀b : block, find_blockl bs = Someb → Inb bs ∧ b_labelb = l
b :
block
H :
name_eqbb_labelb0 l
→
Someb0
else
find_blockl bs
=
Someb
⊢
b0 = b ∨ Inb bs ∧ b_labelb = l

destruct name_eqbb_labelb0 l eqn: E

2 open

l :
name
b0 :
block
bs :
listblock
IH :
∀b : block, find_blockl bs = Someb → Inb bs ∧ b_labelb = l
b :
block
E :
name_eqbb_labelb0 l = true
H :
Someb0 = Someb
⊢
b0 = b ∨ Inb bs ∧ b_labelb = l
focused goal
l :
name
b0 :
block
bs :
listblock
IH :
∀b : block, find_blockl bs = Someb → Inb bs ∧ b_labelb = l
b :
block
E :
name_eqbb_labelb0 l = false
H :
find_blockl bs = Someb
⊢
b0 = b ∨ Inb bs ∧ b_labelb = l

–injection H as ←

2 open

l :
name
b0 :
block
bs :
listblock
IH :
∀b : block, find_blockl bs = Someb → Inb bs ∧ b_labelb = l
E :
name_eqbb_labelb0 l = true
⊢
b0 = b0 ∨ Inb0 bs ∧ b_labelb0 = l
deferred goal
l :
name
b0 :
block
bs :
listblock
IH :
∀b : block, find_blockl bs = Someb → Inb bs ∧ b_labelb = l
b :
block
E :
name_eqbb_labelb0 l = false
H :
find_blockl bs = Someb
⊢
b0 = b ∨ Inb bs ∧ b_labelb = l

split ; left ; reflexivity | apply term_eqb_eq ; exact E

deferred goal
l :
name
b0 :
block
bs :
listblock
IH :
∀b : block, find_blockl bs = Someb → Inb bs ∧ b_labelb = l
b :
block
E :
name_eqbb_labelb0 l = false
H :
find_blockl bs = Someb
⊢
b0 = b ∨ Inb bs ∧ b_labelb = l

–destruct IH_ H

l :
name
b0 :
block
bs :
listblock
IH :
∀b : block, find_blockl bs = Someb → Inb bs ∧ b_labelb = l
b :
block
E :
name_eqbb_labelb0 l = false
H :
find_blockl bs = Someb
H0 :
Inb bs
H1 :
b_labelb = l
⊢
b0 = b ∨ Inb bs ∧ b_labelb = l

split ; right | ; auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
induction bs as | b0 bs IH ; simpl ; intros b H ; discriminate H |
destruct name_eqbb_labelb0 l eqn: E
–injection H as ←
split ; left ; reflexivity | apply term_eqb_eq ; exact E
–destruct IH_ H
split ; right | ; auto

The pass, block by block

evidence_pass folds pass_block over the blocks in order. Each block's entry facts are the meet of the sets on its incoming edges (edge_set): nothing over a poll edge, the exit facts of a block the fold has passed, and nothing for one it has not reached yet, a back edge.

The facts the pass carries along the incoming edge e, a source label and whether it is a poll edge: none over a poll edge, else the exit facts exits gives the source, or none if the fold has not passed the source yet.

77Definition edge_setexits : listname × listfact e : name × bool : listfact ≔
snde
→
[ ]
else
match lookupfste exits with
Somefs
⇒
fs
None
⇒
[ ]

The live facts at the entry of the block b of f, given the exit facts so far: the meet of the sets on b's incoming edges (evidence_meet), less the facts about b's phi temporaries (entry_kill).

84Definition entry_livef : func exits : listname × listfact b : block : listfact ≔
entry_killb_phisb evidence_meetmapedge_setexits incomingfn_blocksf b_labelb

One step of the pass's fold over the blocks: run checked_insts/5 over b's instructions from b's entry facts, and record what it ends with as b's exit facts. Fails where the pass fails.

90Definition pass_blocks : src f : func acc : optionlistname × listfact b : block : optionlistname × listfact ≔
let* exits ≔ acc in
let* out ≔ checked_instss Slengthb_instsb b_instsb entry_livef exits b in
Someputb_labelb out exits

The exit facts of every block of the function f, as the pass, with the sources s of the function, leaves them.

98Definition pass_exitss : src f : func : optionlistname × listfact ≔
fold_leftpass_blocks f fn_blocksf Some[ ]

The evidence pass accepts a function exactly when pass_exits computes its exit facts.

103Lemma evidence_pass_exits
∀ s f
evidence_passs f
=
match pass_exitss f with
Some_
⇒
true
None
⇒
false
Explore proof 1 tactics

Initial goal

⊢
∀ s : src f : func  ,
evidence_passs f
=
match pass_exitss f with
Some_
⇒
true
None
⇒
false

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
reflexivity

A failed fold of pass_block stays failed.

108Lemma pass_fold_none
∀ s f bs
fold_leftpass_blocks f bs None = None
Explore proof 2 tactics

Initial goal

⊢
∀s : src f : func bs : listblock, fold_leftpass_blocks f bs None = None

intros s f bs

s :
src
f :
func
bs :
listblock
⊢
fold_leftpass_blocks f bs None = None

induction bs ; simpl ; auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros s f bs
induction bs ; simpl ; auto

One unfolding of pass_block from the exit facts ex.

112Lemma pass_block_some
∀ s f ex b
pass_blocks f Someex b
=
match checked_instss Slengthb_instsb b_instsb entry_livef ex b with
Someout
⇒
Someputb_labelb out ex
None
⇒
None
Explore proof 1 tactics

Initial goal

⊢
∀ s : src f : func ex : listname × listfact b : block  ,
pass_blocks f Someex b
=
let* out ≔ checked_instss SDatatypes.lengthb_instsb b_instsb entry_livef ex b in
Someputb_labelb out ex

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
reflexivity

The exit facts the fold ends with, E, give a label n that no block of bs carries what they gave it before the fold, in ex.

122Lemma pass_fold_keeps
∀ s f bs ex E n
fold_leftpass_blocks f bs Someex = SomeE
∀b, Inb bs → name_eqbn b_labelb = false
lookupn E = lookupn ex
Explore proof 9 tactics

Initial goal

⊢
∀s : src f : func bs : listblock ex E : listname × listfact n : name, fold_leftpass_blocks f bs Someex = SomeE → ∀b : block, Inb bs → name_eqbn b_labelb = false → lookupn E = lookupn ex

intros s f

s :
src
f :
func
⊢
∀bs : listblock ex E : listname × listfact n : name, fold_leftpass_blocks f bs Someex = SomeE → ∀b : block, Inb bs → name_eqbn b_labelb = false → lookupn E = lookupn ex

induction bs as | b bs IH ; cbn [ fold_left ] ; intros ex E n H Hn

2 open

s :
src
f :
func
ex, E :
listname × listfact
n :
name
H :
Someex = SomeE
Hn :
∀b : block, Inb [ ] → name_eqbn b_labelb = false
⊢
lookupn E = lookupn ex
focused goal
s :
src
f :
func
b :
block
bs :
listblock
IH :
∀ex E : listname × listfact n : name, fold_leftpass_blocks f bs Someex = SomeE → ∀b : block, Inb bs → name_eqbn b_labelb = false → lookupn E = lookupn ex
ex, E :
listname × listfact
n :
name
H :
fold_leftpass_blocks f bs pass_blocks f Someex b = SomeE
Hn :
∀b0 : block, Inb0 b :: bs → name_eqbn b_labelb0 = false
⊢
lookupn E = lookupn ex

–injection H as ←

2 open

s :
src
f :
func
ex :
listname × listfact
n :
name
Hn :
∀b : block, Inb [ ] → name_eqbn b_labelb = false
⊢
lookupn ex = lookupn ex
deferred goal
s :
src
f :
func
b :
block
bs :
listblock
IH :
∀ex E : listname × listfact n : name, fold_leftpass_blocks f bs Someex = SomeE → ∀b : block, Inb bs → name_eqbn b_labelb = false → lookupn E = lookupn ex
ex, E :
listname × listfact
n :
name
H :
fold_leftpass_blocks f bs pass_blocks f Someex b = SomeE
Hn :
∀b0 : block, Inb0 b :: bs → name_eqbn b_labelb0 = false
⊢
lookupn E = lookupn ex

reflexivity

deferred goal
s :
src
f :
func
b :
block
bs :
listblock
IH :
∀ex E : listname × listfact n : name, fold_leftpass_blocks f bs Someex = SomeE → ∀b : block, Inb bs → name_eqbn b_labelb = false → lookupn E = lookupn ex
ex, E :
listname × listfact
n :
name
H :
fold_leftpass_blocks f bs pass_blocks f Someex b = SomeE
Hn :
∀b0 : block, Inb0 b :: bs → name_eqbn b_labelb0 = false
⊢
lookupn E = lookupn ex

–rewrite pass_block_some in H

s :
src
f :
func
b :
block
bs :
listblock
IH :
∀ex E : listname × listfact n : name, fold_leftpass_blocks f bs Someex = SomeE → ∀b : block, Inb bs → name_eqbn b_labelb = false → lookupn E = lookupn ex
ex, E :
listname × listfact
n :
name
H :
fold_leftpass_blocks f bs
let* out ≔ checked_instss SDatatypes.lengthb_instsb b_instsb entry_livef ex b in
Someputb_labelb out ex
=
SomeE
Hn :
∀b0 : block, Inb0 b :: bs → name_eqbn b_labelb0 = false
⊢
lookupn E = lookupn ex

destruct checked_insts_ _ _ _ as out | ; | rewrite pass_fold_none in H ; discriminate H

s :
src
f :
func
b :
block
bs :
listblock
IH :
∀ex E : listname × listfact n : name, fold_leftpass_blocks f bs Someex = SomeE → ∀b : block, Inb bs → name_eqbn b_labelb = false → lookupn E = lookupn ex
ex, E :
listname × listfact
n :
name
out :
listfact
H :
fold_leftpass_blocks f bs Someputb_labelb out ex = SomeE
Hn :
∀b0 : block, Inb0 b :: bs → name_eqbn b_labelb0 = false
⊢
lookupn E = lookupn ex

rewrite IH_ _ _ H by intros b′ Hb′ ; apply Hn ; right ; exact Hb'

s :
src
f :
func
b :
block
bs :
listblock
IH :
∀ex E : listname × listfact n : name, fold_leftpass_blocks f bs Someex = SomeE → ∀b : block, Inb bs → name_eqbn b_labelb = false → lookupn E = lookupn ex
ex, E :
listname × listfact
n :
name
out :
listfact
H :
fold_leftpass_blocks f bs Someputb_labelb out ex = SomeE
Hn :
∀b0 : block, Inb0 b :: bs → name_eqbn b_labelb0 = false
⊢
lookupn putb_labelb out ex = lookupn ex

rewrite lookup_put , Hnb by left ; reflexivity

s :
src
f :
func
b :
block
bs :
listblock
IH :
∀ex E : listname × listfact n : name, fold_leftpass_blocks f bs Someex = SomeE → ∀b : block, Inb bs → name_eqbn b_labelb = false → lookupn E = lookupn ex
ex, E :
listname × listfact
n :
name
out :
listfact
H :
fold_leftpass_blocks f bs Someputb_labelb out ex = SomeE
Hn :
∀b0 : block, Inb0 b :: bs → name_eqbn b_labelb0 = false
⊢
lookupn ex = lookupn ex

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros s f
induction bs as | b bs IH ; cbn [ fold_left ] ; intros ex E n H Hn
–injection H as ←
reflexivity
–rewrite pass_block_some in H
destruct checked_insts_ _ _ _ as out | ; | rewrite pass_fold_none in H ; discriminate H
rewrite IH_ _ _ H by intros b′ Hb′ ; apply Hn ; right ; exact Hb'
rewrite lookup_put , Hnb by left ; reflexivity
reflexivity

Folding pass_block over blocks bs with distinct labels, none of which had exit facts in ex yet, passes each block b of bs from the exit facts the fold had when it reached b, all of which it keeps to the end E, and records b's exit facts out in E.

138Lemma pass_fold
∀ s f bs ex E b
fold_leftpass_blocks f bs Someex = SomeE
no_dupsmapb_label bs = true
∀b, Inb bs → lookupb_labelb ex = None
Inb bs
∃exits out, ∀n v, lookupn exits = Somev → lookupn E = Somev ∧ lookupb_labelb E = Someout ∧ checked_instss Slengthb_instsb b_instsb entry_livef exits b = Someout
Proof 39 steps Qed
intros s f
induction bs as | b0 bs IH ; cbn [ fold_left ] ; intros ex E H Hd Hex b Hb ; destruct Hb |
cbn [ map no_dups ] in Hd
apply andb_true_iff in Hd as Hd0 Hd
apply negb_true_iff in Hd0
rewrite pass_block_some in H
destruct checked_insts_ _ _ entry_livef ex b0 as out | eqn: Ec ; | rewrite pass_fold_none in H ; discriminate H
assert Hlater : ∀b′, Inb′ bs → name_eqbb_labelb0 b_labelb′ = false
{intros b′ Hb′
eapply mem_false ; exact Hd0 |
apply in_map
exact Hb'
destruct Hb as ← | Hb
–exists ex, out
split ; | split ; | exact Ec
+intros n v Hv
rewrite pass_fold_keeps_ _ _ _ _ _ H
∗rewrite lookup_put
destruct name_eqbn b_labelb0 eqn: E0 ; | exact Hv
apply term_eqb_eq in E0
subst
rewrite Hex in Hv by left ; reflexivity
discriminate Hv
∗intros b′ Hb′
destruct name_eqbn b_labelb' eqn: E1 ; auto
apply term_eqb_eq in E1
subst
rewrite Hex in Hv by right ; exact Hb'
discriminate Hv
+rewrite pass_fold_keeps_ _ _ _ _ _ H Hlater
rewrite lookup_put , name_eqb_refl
reflexivity
–apply IH_ _ H Hd ; | exact Hb
intros b′ Hb′
rewrite lookup_put
rewrite name_eqb_sym , Hlaterb' Hb'
apply Hex
right
exact Hb'

A jump of the block bp of bs to the block labelled l gives l an incoming edge from bp, marked as a poll edge where the target is one (is_poll).

170Lemma incoming_in
∀ bs bp t
Inbp bs
Int jump_targetsb_jumpbp
Inb_labelbp, is_pollt incomingbs edge_labelt
Explore proof 12 tactics

Initial goal

⊢
∀bs : listblock bp : block t : target, Inbp bs → Int jump_targetsb_jumpbp → Inb_labelbp, is_pollt incomingbs edge_labelt

unfold incoming

⊢
∀ bs : listblock bp : block t : target  ,
Inbp bs
→
Int jump_targetsb_jumpbp
→
Inb_labelbp, is_pollt
rev
flat_map
λ b : block  ⇒
flat_map
λ t0 : target  ⇒
name_eqbedge_labelt0 edge_labelt
→
b_labelb, is_pollt0
else
[ ]
jump_targetsb_jumpb
bs

intros bs bp t Hb Ht

bs :
listblock
bp :
block
t :
target
Hb :
Inbp bs
Ht :
Int jump_targetsb_jumpbp
⊢
Inb_labelbp, is_pollt
rev
flat_map
λ b : block  ⇒
flat_map
λ t0 : target  ⇒
name_eqbedge_labelt0 edge_labelt
→
b_labelb, is_pollt0
else
[ ]
jump_targetsb_jumpb
bs

apply proj1in_rev_ _

bs :
listblock
bp :
block
t :
target
Hb :
Inbp bs
Ht :
Int jump_targetsb_jumpbp
⊢
Inb_labelbp, is_pollt
flat_map
λ b : block  ⇒
flat_map
λ t0 : target  ⇒
name_eqbedge_labelt0 edge_labelt
→
b_labelb, is_pollt0
else
[ ]
jump_targetsb_jumpb
bs

apply proj2in_flat_map_ _ _

bs :
listblock
bp :
block
t :
target
Hb :
Inbp bs
Ht :
Int jump_targetsb_jumpbp
⊢
∃ x : block  ,
Inx bs
∧
Inb_labelbp, is_pollt
flat_map
λ t0 : target  ⇒
name_eqbedge_labelt0 edge_labelt
→
b_labelx, is_pollt0
else
[ ]
jump_targetsb_jumpx

exists bp

bs :
listblock
bp :
block
t :
target
Hb :
Inbp bs
Ht :
Int jump_targetsb_jumpbp
⊢
Inbp bs
∧
Inb_labelbp, is_pollt
flat_map
λ t0 : target  ⇒
name_eqbedge_labelt0 edge_labelt
→
b_labelbp, is_pollt0
else
[ ]
jump_targetsb_jumpbp

split ; exact Hb |

bs :
listblock
bp :
block
t :
target
Hb :
Inbp bs
Ht :
Int jump_targetsb_jumpbp
⊢
Inb_labelbp, is_pollt
flat_map
λ t0 : target  ⇒
name_eqbedge_labelt0 edge_labelt
→
b_labelbp, is_pollt0
else
[ ]
jump_targetsb_jumpbp

apply proj2in_flat_map_ _ _

bs :
listblock
bp :
block
t :
target
Hb :
Inbp bs
Ht :
Int jump_targetsb_jumpbp
⊢
∃ x : target  ,
Inx jump_targetsb_jumpbp
∧
Inb_labelbp, is_pollt
name_eqbedge_labelx edge_labelt
→
b_labelbp, is_pollx
else
[ ]

exists t

bs :
listblock
bp :
block
t :
target
Hb :
Inbp bs
Ht :
Int jump_targetsb_jumpbp
⊢
Int jump_targetsb_jumpbp
∧
Inb_labelbp, is_pollt
name_eqbedge_labelt edge_labelt
→
b_labelbp, is_pollt
else
[ ]

split ; exact Ht |

bs :
listblock
bp :
block
t :
target
Hb :
Inbp bs
Ht :
Int jump_targetsb_jumpbp
⊢
Inb_labelbp, is_pollt
name_eqbedge_labelt edge_labelt
→
b_labelbp, is_pollt
else
[ ]

rewrite name_eqb_refl

bs :
listblock
bp :
block
t :
target
Hb :
Inbp bs
Ht :
Int jump_targetsb_jumpbp
⊢
Inb_labelbp, is_pollt b_labelbp, is_pollt

left

bs :
listblock
bp :
block
t :
target
Hb :
Inbp bs
Ht :
Int jump_targetsb_jumpbp
⊢
b_labelbp, is_pollt = b_labelbp, is_pollt

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
unfold incoming
intros bs bp t Hb Ht
apply proj1in_rev_ _
apply proj2in_flat_map_ _ _
exists bp
split ; exact Hb |
apply proj2in_flat_map_ _ _
exists t
split ; exact Ht |
rewrite name_eqb_refl
left
reflexivity

A label that no jump of bs can go to has no incoming edges; the entry is such a label.

181Lemma incoming_nil
∀ bs l
existsbλb ⇒ meml succ_labelsb_jumpb bs = false
incomingbs l = [ ]
Explore proof 15 tactics

Initial goal

⊢
∀bs : listblock l : name, existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false → incomingbs l = [ ]

unfold incoming

⊢
∀ bs : listblock l : name  ,
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
→
rev
flat_map
λ b : block  ⇒
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
bs
=
[ ]

intros bs l H

bs :
listblock
l :
name
H :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
⊢
rev
flat_map
λ b : block  ⇒
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
bs
=
[ ]

assert flat_mapλb ⇒ flat_mapλt ⇒ if name_eqbedge_labelt l then b_labelb, is_pollt else [ ] jump_targetsb_jumpb bs = [ ] as → ; | reflexivity

bs :
listblock
l :
name
H :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
⊢
flat_map
λ b : block  ⇒
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
bs
=
[ ]

induction bs as | b bs IH ; simpl in * ; auto

b :
block
bs :
listblock
l :
name
H :
meml succ_labelsb_jumpb || existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
IH :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
→
flat_map
λ b : block  ⇒
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
bs
=
[ ]
⊢
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
++
flat_map
λ b0 : block  ⇒
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb0, is_pollt
else
[ ]
jump_targetsb_jumpb0
bs
=
[ ]

apply orb_false_iff in H as Hb Hbs

b :
block
bs :
listblock
l :
name
Hb :
meml succ_labelsb_jumpb = false
Hbs :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
IH :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
→
flat_map
λ b : block  ⇒
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
bs
=
[ ]
⊢
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
++
flat_map
λ b0 : block  ⇒
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb0, is_pollt
else
[ ]
jump_targetsb_jumpb0
bs
=
[ ]

rewrite IH by exact Hbs

b :
block
bs :
listblock
l :
name
Hb :
meml succ_labelsb_jumpb = false
Hbs :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
IH :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
→
flat_map
λ b : block  ⇒
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
bs
=
[ ]
⊢
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
++
[ ]
=
[ ]

rewrite app_nil_r

b :
block
bs :
listblock
l :
name
Hb :
meml succ_labelsb_jumpb = false
Hbs :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
IH :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
→
flat_map
λ b : block  ⇒
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
bs
=
[ ]
⊢
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
=
[ ]

unfold succ_labels in Hb

b :
block
bs :
listblock
l :
name
Hb :
meml mapedge_label jump_targetsb_jumpb = false
Hbs :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
IH :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
→
flat_map
λ b : block  ⇒
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
bs
=
[ ]
⊢
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
=
[ ]

induction jump_targetsb_jumpb as | t ts IHt ; simpl in * ; auto

b :
block
bs :
listblock
l :
name
t :
target
ts :
listtarget
Hb :
name_eqbl edge_labelt || meml mapedge_label ts = false
Hbs :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
IH :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
→
flat_map
λ b : block  ⇒
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
bs
=
[ ]
IHt :
meml mapedge_label ts = false
→
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
ts
=
[ ]
⊢
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
++
flat_map
λ t0 : target  ⇒
name_eqbedge_labelt0 l
→
b_labelb, is_pollt0
else
[ ]
ts
=
[ ]

unfold mem in Hb

b :
block
bs :
listblock
l :
name
t :
target
ts :
listtarget
Hb :
name_eqbl edge_labelt || existsbname_eqbl mapedge_label ts = false
Hbs :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
IH :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
→
flat_map
λ b : block  ⇒
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
bs
=
[ ]
IHt :
meml mapedge_label ts = false
→
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
ts
=
[ ]
⊢
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
++
flat_map
λ t0 : target  ⇒
name_eqbedge_labelt0 l
→
b_labelb, is_pollt0
else
[ ]
ts
=
[ ]

simpl in Hb

b :
block
bs :
listblock
l :
name
t :
target
ts :
listtarget
Hb :
name_eqbl edge_labelt || existsbname_eqbl mapedge_label ts = false
Hbs :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
IH :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
→
flat_map
λ b : block  ⇒
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
bs
=
[ ]
IHt :
meml mapedge_label ts = false
→
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
ts
=
[ ]
⊢
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
++
flat_map
λ t0 : target  ⇒
name_eqbedge_labelt0 l
→
b_labelb, is_pollt0
else
[ ]
ts
=
[ ]

apply orb_false_iff in Hb as Ht Hts

b :
block
bs :
listblock
l :
name
t :
target
ts :
listtarget
Ht :
name_eqbl edge_labelt = false
Hts :
existsbname_eqbl mapedge_label ts = false
Hbs :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
IH :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
→
flat_map
λ b : block  ⇒
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
bs
=
[ ]
IHt :
meml mapedge_label ts = false
→
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
ts
=
[ ]
⊢
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
++
flat_map
λ t0 : target  ⇒
name_eqbedge_labelt0 l
→
b_labelb, is_pollt0
else
[ ]
ts
=
[ ]

rewrite name_eqb_sym , Ht

b :
block
bs :
listblock
l :
name
t :
target
ts :
listtarget
Ht :
name_eqbl edge_labelt = false
Hts :
existsbname_eqbl mapedge_label ts = false
Hbs :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
IH :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
→
flat_map
λ b : block  ⇒
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
bs
=
[ ]
IHt :
meml mapedge_label ts = false
→
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
ts
=
[ ]
⊢
[ ]
++
flat_map
λ t0 : target  ⇒
name_eqbedge_labelt0 l
→
b_labelb, is_pollt0
else
[ ]
ts
=
[ ]

apply IHt

b :
block
bs :
listblock
l :
name
t :
target
ts :
listtarget
Ht :
name_eqbl edge_labelt = false
Hts :
existsbname_eqbl mapedge_label ts = false
Hbs :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
IH :
existsbλb : block ⇒ meml succ_labelsb_jumpb bs = false
→
flat_map
λ b : block  ⇒
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
jump_targetsb_jumpb
bs
=
[ ]
IHt :
meml mapedge_label ts = false
→
flat_map
λ t : target  ⇒
name_eqbedge_labelt l
→
b_labelb, is_pollt
else
[ ]
ts
=
[ ]
⊢
meml mapedge_label ts = false

exact Hts

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
unfold incoming
intros bs l H
assert flat_mapλb ⇒ flat_mapλt ⇒ if name_eqbedge_labelt l then b_labelb, is_pollt else [ ] jump_targetsb_jumpb bs = [ ] as → ; | reflexivity
induction bs as | b bs IH ; simpl in * ; auto
apply orb_false_iff in H as Hb Hbs
rewrite IH by exact Hbs
rewrite app_nil_r
unfold succ_labels in Hb
induction jump_targetsb_jumpb as | t ts IHt ; simpl in * ; auto
unfold mem in Hb
simpl in Hb
apply orb_false_iff in Hb as Ht Hts
rewrite name_eqb_sym , Ht
apply IHt
exact Hts

Where the pass is within a block

From the facts live before the instructions is, the pass, with fuel enough, reaches the block's end with the facts out (checked_insts/5).

199Definition walkss : src is : listinst live out : listfact : Prop ≔
∃n, checked_instss n is live = Someout

With no instructions left, the pass ends with the facts it had.

203Lemma walks_nil
∀ s live out
walkss [ ] live out
out = live
Explore proof 2 tactics

Initial goal

⊢
∀s : src live out : listfact, walkss [ ] live out → out = live

intros s live out n H

s :
src
live, out :
listfact
n :
nat
H :
checked_instss n [ ] live = Someout
⊢
out = live

destruct n ; cbn [ checked_insts ] in H ; congruence

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros s live out n H
destruct n ; cbn [ checked_insts ] in H ; congruence

A walk over i :: rest takes i with what follows it by checked_inst_rest/7, which may consume the next instructions too, and walks on over what is left.

209Lemma walks_cons
∀ s i rest live out
walkss i :: rest live out
∃rest′ live′, checked_inst_rests i rest live = Somerest′, live′ ∧ walkss rest′ live′ out
Explore proof 5 tactics

Initial goal

⊢
∀s : src i : inst rest : listinst live out : listfact, walkss i :: rest live out → ∃rest′ : listinst live′ : listfact, checked_inst_rests i rest live = Somerest′, live′ ∧ walkss rest′ live′ out

intros s i rest live out n H

s :
src
i :
inst
rest :
listinst
live, out :
listfact
n :
nat
H :
checked_instss n i :: rest live = Someout
⊢
∃rest′ : listinst live′ : listfact, checked_inst_rests i rest live = Somerest′, live′ ∧ walkss rest′ live′ out

destruct n as | n ; cbn [ checked_insts ] in H ; discriminate H |

s :
src
i :
inst
rest :
listinst
live, out :
listfact
n :
nat
H :
let* rl ≔ checked_inst_rests i rest live in
checked_instss n fstrl sndrl
=
Someout
⊢
∃rest′ : listinst live′ : listfact, checked_inst_rests i rest live = Somerest′, live′ ∧ walkss rest′ live′ out

destruct checked_inst_rests i rest live as rest′ live′ | ; | discriminate H

s :
src
i :
inst
rest :
listinst
live, out :
listfact
n :
nat
rest′ :
listinst
live′ :
listfact
H :
checked_instss n fstrest′, live′ sndrest′, live′ = Someout
⊢
∃rest'0 : listinst live'0 : listfact, Somerest′, live′ = Somerest'0, live'0 ∧ walkss rest'0 live'0 out

exists rest′, live′

s :
src
i :
inst
rest :
listinst
live, out :
listfact
n :
nat
rest′ :
listinst
live′ :
listfact
H :
checked_instss n fstrest′, live′ sndrest′, live′ = Someout
⊢
Somerest′, live′ = Somerest′, live′ ∧ walkss rest′ live′ out

split ; reflexivity | exists n ; exact H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros s i rest live out n H
destruct n as | n ; cbn [ checked_insts ] in H ; discriminate H |
destruct checked_inst_rests i rest live as rest′ live′ | ; | discriminate H
exists rest′, live′
split ; reflexivity | exists n ; exact H

Where the pass relies on facts

The pass reads its live facts at a raw access (its coverage), and keeps them across an evidence-preserving instruction, a check_local and a repeated getter. Before any other instruction it keeps none: what it says after does not depend on them.

The instruction i copies a global g into a temporary d that the sources s record as a getter of g (getter): a repeated getter, after which the pass keeps its facts.

228Definition repeated_getters : src i : inst : bool ≔
match i with
Letd P Copy Globalg
⇒
match lookupd s_getterss with
Someg1
⇒
name_eqbg1 g
None
⇒
false
_
⇒
false

The instruction i is a check_local, an access check of a named local.

236Definition is_check_locali : inst : bool ≔
match i with
Let_ A CheckLocal_ _ _ _ _ [ ]
⇒
true
_
⇒
false

The instructions before which the pass keeps its live facts: an evidence-preserving one (evidence_preserving), a check_local, a repeated getter, or a raw access, which reads them as its coverage.

242Definition reliess : src i : inst : bool ≔
evidence_preservingi || is_check_locali || repeated_getters i
||
match raw_accessi with
Some_
⇒
true
None
⇒
false

An instruction after which the pass adds a fact (check_fact) is evidence preserving.

248Lemma check_fact_preserving
∀ i fa
check_facti = Somefa
evidence_preservingi = true
Explore proof 3 tactics

Initial goal

⊢
∀i : inst fa : fact, check_facti = Somefa → evidence_preservingi = true

intros i fa H

i :
inst
fa :
fact
H :
check_facti = Somefa
⊢
evidence_preservingi = true

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

q :
name
k :
class
o :
op
args :
listvalue
fa :
fact
H :
check_factLetq k o args = Somefa
⊢
evidence_preservingLetq k o args = true

destruct o ; try destruct k ; discriminate H ; destruct k ; try discriminate H ; destruct args as | a1 | a2 | a3 | a4 args ; try discriminate H ; reflexivity

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 o ; try destruct k ; discriminate H ; destruct k ; try discriminate H ; destruct args as | a1 | a2 | a3 | a4 args ; try discriminate H ; reflexivity

Before an instruction it does not rely on facts for (relies), the pass keeps none: it goes on with no live facts.

257Lemma relies_false
∀ s i rest live rest′ live′
reliess i = false
checked_inst_rests i rest live = Somerest′, live′
live′ = [ ]
Explore proof 28 tactics

Initial goal

⊢
∀s : src i : inst rest : listinst live : listfact rest′ : listinst live′ : listfact, reliess i = false → checked_inst_rests i rest live = Somerest′, live′ → live′ = [ ]

intros s i rest live rest′ live′ Hr Hc

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
⊢
live′ = [ ]

unfold relies in Hr

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
evidence_preservingi || is_check_locali || repeated_getters i
||
match raw_accessi with
Some_
⇒
true
None
⇒
false
=
false
Hc :
checked_inst_rests i rest live = Somerest′, live′
⊢
live′ = [ ]

apply orb_false_iff in Hr as Hr _

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
evidence_preservingi || is_check_locali || repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
⊢
live′ = [ ]

apply orb_false_iff in Hr as Hr Hg

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
evidence_preservingi || is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
⊢
live′ = [ ]

apply orb_false_iff in Hr as Hp Hl

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
⊢
live′ = [ ]

destruct check_facti as fa | eqn: Hf

2 open

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
fa :
fact
Hf :
check_facti = Somefa
⊢
live′ = [ ]
focused goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
⊢
live′ = [ ]

–rewrite check_fact_preserving_ _ Hf in Hp

2 open

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
true = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
fa :
fact
Hf :
check_facti = Somefa
⊢
live′ = [ ]
deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
⊢
live′ = [ ]

discriminate Hp

deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
⊢
live′ = [ ]

–destruct pass_speciali eqn: Hs

2 open

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = true
⊢
live′ = [ ]
focused goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
live′ = [ ]

+unfold pass_special in Hs

2 open

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
match i with
Let_ A CheckLocal_ _ _ _ _ [ ] | Let_ F CheckFunction _
⇒
true
_
⇒
match check_facti with
Some_
⇒
true
None
⇒
false
=
true
⊢
live′ = [ ]
deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
live′ = [ ]

rewrite Hf in Hs

2 open

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
match i with
Let_ A CheckLocal_ _ _ _ _ [ ] | Let_ F CheckFunction _
⇒
true
_
⇒
false
=
true
⊢
live′ = [ ]
deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
live′ = [ ]

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

2 open

s :
src
q :
name
k :
class
o :
op
args :
listvalue
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingLetq k o args = false
Hl :
is_check_localLetq k o args = false
Hg :
repeated_getters Letq k o args = false
Hc :
checked_inst_rests Letq k o args rest live = Somerest′, live′
Hf :
check_factLetq k o args = None
Hs :
match k with
A
⇒
match o with
CheckLocal_ _ _ _ _
⇒
match args with
[ ]
⇒
true
_ :: _
⇒
false
_
⇒
false
F
⇒
match o with
CheckFunction
⇒
true
_
⇒
false
_
⇒
false
=
true
⊢
live′ = [ ]
deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
live′ = [ ]

destruct k ; try discriminate Hs ; destruct o ; try discriminate Hs

3 open

s :
src
q, x :
name
off, bytes :
Z
r :
rights
align :
Z
args :
listvalue
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingLetq A CheckLocalx off bytes r align args = false
Hl :
is_check_localLetq A CheckLocalx off bytes r align args = false
Hg :
repeated_getters Letq A CheckLocalx off bytes r align args = false
Hc :
checked_inst_rests Letq A CheckLocalx off bytes r align args rest live = Somerest′, live′
Hf :
check_factLetq A CheckLocalx off bytes r align args = None
Hs :
match args with
[ ]
⇒
true
_ :: _
⇒
false
=
true
⊢
live′ = [ ]
focused goal
s :
src
q :
name
args :
listvalue
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingLetq F CheckFunction args = false
Hl :
is_check_localLetq F CheckFunction args = false
Hg :
repeated_getters Letq F CheckFunction args = false
Hc :
checked_inst_rests Letq F CheckFunction args rest live = Somerest′, live′
Hf :
check_factLetq F CheckFunction args = None
Hs :
true = true
⊢
live′ = [ ]
deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
live′ = [ ]

∗destruct args ; discriminate Hl | discriminate Hs

2 open

deferred goal
s :
src
q :
name
args :
listvalue
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingLetq F CheckFunction args = false
Hl :
is_check_localLetq F CheckFunction args = false
Hg :
repeated_getters Letq F CheckFunction args = false
Hc :
checked_inst_rests Letq F CheckFunction args rest live = Somerest′, live′
Hf :
check_factLetq F CheckFunction args = None
Hs :
true = true
⊢
live′ = [ ]
deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
live′ = [ ]

∗exact checked_inst_rest_function_ _ _ _ _ _ _ Hc

deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
live′ = [ ]

+rewrite checked_inst_rest_generic_ _ _ _ Hs in Hc

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
generic_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
live′ = [ ]

unfold generic_rest in Hc

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
match raw_accessi with
Someq, x, _, _
⇒
reusing_accessi 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
Letd P Copy Globalg
⇒
match lookupd s_getterss with
Someg1
⇒
name_eqbg1 g
→
killd live
else
evidence_afteri live
None
⇒
evidence_afteri live
Letd P Copy Globalg :: _ :: _
⇒
evidence_afteri live
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 _ _
⇒
evidence_afteri live
_
⇒
evidence_afteri live
else
None
=
Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
live′ = [ ]

cbn zeta in Hc

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
match raw_accessi with
Someq, x, _, _
⇒
reusing_accessi 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
Letd P Copy Globalg
⇒
match lookupd s_getterss with
Someg1
⇒
name_eqbg1 g
→
killd live
else
evidence_afteri live
None
⇒
evidence_afteri live
Letd P Copy Globalg :: _ :: _
⇒
evidence_afteri live
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 _ _
⇒
evidence_afteri live
_
⇒
evidence_afteri live
else
None
=
Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
live′ = [ ]

match type of Hc withif ?b then _ else _ = _⇒destruct b ; | discriminate Hcend

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hc :
Some
rest
match i with
Letd P Copy Globalg
⇒
match lookupd s_getterss with
Someg1
⇒
name_eqbg1 g
→
killd live
else
evidence_afteri live
None
⇒
evidence_afteri live
Letd P Copy Globalg :: _ :: _
⇒
evidence_afteri live
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 _ _
⇒
evidence_afteri live
_
⇒
evidence_afteri live
=
Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
live′ = [ ]

injection Hc as _ ←

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
match i with
Letd P Copy Globalg
⇒
match lookupd s_getterss with
Someg1
⇒
name_eqbg1 g
→
killd live
else
evidence_afteri live
None
⇒
evidence_afteri live
Letd P Copy Globalg :: _ :: _
⇒
evidence_afteri live
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 _ _
⇒
evidence_afteri live
_
⇒
evidence_afteri live
=
[ ]

unfold evidence_after

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
match i with
Letd P Copy Globalg
⇒
match lookupd s_getterss with
Someg1
⇒
name_eqbg1 g
→
killd live
evidence_preservingi
→
match inst_def_firsti with
Somed0
⇒
killd0 live
None
⇒
live
else
[ ]
None
⇒
evidence_preservingi
→
match inst_def_firsti with
Somed0
⇒
killd0 live
None
⇒
live
else
[ ]
Letd P Copy Globalg :: _ :: _
⇒
evidence_preservingi
→
match inst_def_firsti with
Somed0
⇒
killd0 live
None
⇒
live
else
[ ]
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 _ _
⇒
evidence_preservingi
→
match inst_def_firsti with
Somed0
⇒
killd0 live
None
⇒
live
else
[ ]
Flight_ _ _ _
⇒
evidence_preservingi
→
match inst_def_firsti with
Somed0
⇒
killd0 live
None
⇒
live
else
[ ]
_
⇒
evidence_preservingi
→
match inst_def_firsti with
Somed
⇒
killd live
None
⇒
live
else
[ ]
=
[ ]

rewrite Hp

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
Hp :
evidence_preservingi = false
Hl :
is_check_locali = false
Hg :
repeated_getters i = false
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
match i with
Letd P Copy Globalg
⇒
match lookupd s_getterss with
Someg1
⇒
name_eqbg1 g
→
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 _ _
⇒
[ ]
_
⇒
[ ]
=
[ ]

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

s :
src
d :
name
k :
class
o :
op
args :
listvalue
rest :
listinst
live :
listfact
rest′ :
listinst
Hp :
evidence_preservingLetd k o args = false
Hl :
is_check_localLetd k o args = false
Hg :
repeated_getters Letd k o args = false
Hf :
check_factLetd k o args = None
Hs :
pass_specialLetd k o args = false
⊢
match k with
P
⇒
match o with
Copy
⇒
match args with
Globalg
⇒
match lookupd s_getterss with
Someg1
⇒
name_eqbg1 g
→
killd live
else
[ ]
None
⇒
[ ]
Globalg :: _ :: _
⇒
[ ]
_
⇒
[ ]
_
⇒
[ ]
_
⇒
[ ]
=
[ ]

destruct o ; try reflexivity ; destruct k ; try reflexivity ; destruct args as | n | c | g | a2 args ; try reflexivity

s :
src
d, g :
name
rest :
listinst
live :
listfact
rest′ :
listinst
Hp :
evidence_preservingLetd P Copy Globalg = false
Hl :
is_check_localLetd P Copy Globalg = false
Hg :
repeated_getters Letd P Copy Globalg = false
Hf :
check_factLetd P Copy Globalg = None
Hs :
pass_specialLetd P Copy Globalg = false
⊢
match lookupd s_getterss with
Someg1
⇒
name_eqbg1 g
→
killd live
else
[ ]
None
⇒
[ ]
=
[ ]

unfold repeated_getter in Hg

s :
src
d, g :
name
rest :
listinst
live :
listfact
rest′ :
listinst
Hp :
evidence_preservingLetd P Copy Globalg = false
Hl :
is_check_localLetd P Copy Globalg = false
Hg :
match lookupd s_getterss with
Someg1
⇒
name_eqbg1 g
None
⇒
false
=
false
Hf :
check_factLetd P Copy Globalg = None
Hs :
pass_specialLetd P Copy Globalg = false
⊢
match lookupd s_getterss with
Someg1
⇒
name_eqbg1 g
→
killd live
else
[ ]
None
⇒
[ ]
=
[ ]

destruct lookupd s_getterss as g1 | ; | reflexivity

s :
src
d, g :
name
rest :
listinst
live :
listfact
rest′ :
listinst
Hp :
evidence_preservingLetd P Copy Globalg = false
Hl :
is_check_localLetd P Copy Globalg = false
g1 :
name
Hg :
name_eqbg1 g = false
Hf :
check_factLetd P Copy Globalg = None
Hs :
pass_specialLetd P Copy Globalg = false
⊢
name_eqbg1 g
→
killd live
else
[ ]
=
[ ]

rewrite Hg

s :
src
d, g :
name
rest :
listinst
live :
listfact
rest′ :
listinst
Hp :
evidence_preservingLetd P Copy Globalg = false
Hl :
is_check_localLetd P Copy Globalg = false
g1 :
name
Hg :
name_eqbg1 g = false
Hf :
check_factLetd P Copy Globalg = None
Hs :
pass_specialLetd P Copy Globalg = false
⊢
[ ] = [ ]

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros s i rest live rest′ live′ Hr Hc
unfold relies in Hr
apply orb_false_iff in Hr as Hr _
apply orb_false_iff in Hr as Hr Hg
apply orb_false_iff in Hr as Hp Hl
destruct check_facti as fa | eqn: Hf
–rewrite check_fact_preserving_ _ Hf in Hp
discriminate Hp
–destruct pass_speciali eqn: Hs
+unfold pass_special in Hs
rewrite Hf in Hs
destruct i as q k o args | | | | | | | ; try discriminate Hs
destruct k ; try discriminate Hs ; destruct o ; try discriminate Hs
∗destruct args ; discriminate Hl | discriminate Hs
∗exact checked_inst_rest_function_ _ _ _ _ _ _ Hc
+rewrite checked_inst_rest_generic_ _ _ _ Hs in Hc
unfold generic_rest in Hc
cbn zeta in Hc
match type of Hc withif ?b then _ else _ = _⇒destruct b ; | discriminate Hcend
injection Hc as _ ←
unfold evidence_after
rewrite Hp
destruct i as d k o args | | | | | | | ; try reflexivity
destruct o ; try reflexivity ; destruct k ; try reflexivity ; destruct args as | n | c | g | a2 args ; try reflexivity
unfold repeated_getter in Hg
destruct lookupd s_getterss as g1 | ; | reflexivity
rewrite Hg
reflexivity

The forms the pass pairs with their access

A check_local of the local x that continues binds its result q to the pointer at offset off of x's object, changes no memory, and its access check passed (access_res).

287Lemma check_local_step
∀ ge fr m q x off bytes r al e1 l1 m1
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinuee1 l1 m1
∃base, lookupx fr_localsfr = SomeSomebase ∧ m1 = m ∧ e1 = putq WPtrmkPtrbase + off Objbase fr_envfr ∧ access_resm base + off Objbase bytes r al = Someok
Explore proof 7 tactics

Initial goal

⊢
∀ge : genv fr : frame m : Memory.mem q x : name off bytes : Z r : rights al : Z e1 : env l1 : listname × optionZ m1 : Memory.mem, inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinuee1 l1 m1 → ∃base : Z, lookupx fr_localsfr = SomeSomebase ∧ m1 = m ∧ e1 = putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr ∧ access_resm base + off Objbase bytes r al = Someok

intros ge fr m q x off bytes r al e1 l1 m1 H

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
e1 :
env
l1 :
listname × optionZ
m1 :
Memory.mem
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinuee1 l1 m1
⊢
∃base : Z, lookupx fr_localsfr = SomeSomebase ∧ m1 = m ∧ e1 = putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr ∧ access_resm base + off Objbase bytes r al = Someok

unfold inst_step in H

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
e1 :
env
l1 :
listname × optionZ
m1 :
Memory.mem
H :
match lookupx fr_localsfr with
SomeSomebase
⇒
let* chk ≔ access_resm base + off Objbase bytes r al in
Somebind_resq checked_reschk WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr fr_localsfr m
_
⇒
None
=
SomeIContinuee1 l1 m1
⊢
∃base : Z, lookupx fr_localsfr = SomeSomebase ∧ m1 = m ∧ e1 = putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr ∧ access_resm base + off Objbase bytes r al = Someok

cbn iota beta zeta in H

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
e1 :
env
l1 :
listname × optionZ
m1 :
Memory.mem
H :
match lookupx fr_localsfr with
SomeSomebase
⇒
let* chk ≔ access_resm base + off Objbase bytes r al in
Somebind_resq checked_reschk WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr fr_localsfr m
_
⇒
None
=
SomeIContinuee1 l1 m1
⊢
∃base : Z, lookupx fr_localsfr = SomeSomebase ∧ m1 = m ∧ e1 = putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr ∧ access_resm base + off Objbase bytes r al = Someok

destruct lookupx fr_localsfr as base | | ; try discriminate H

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
e1 :
env
l1 :
listname × optionZ
m1 :
Memory.mem
base :
Z
H :
let* chk ≔ access_resm base + off Objbase bytes r al in
Somebind_resq checked_reschk WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr fr_localsfr m
=
SomeIContinuee1 l1 m1
⊢
∃base0 : Z, SomeSomebase = SomeSomebase0 ∧ m1 = m ∧ e1 = putq WPtrptr_addr ≔ base0 + off; ptr_cap ≔ Objbase0 fr_envfr ∧ access_resm base0 + off Objbase0 bytes r al = Someok

destruct access_resm base + off Objbase bytes r al as | w | w | eqn: E ; try discriminate H

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
e1 :
env
l1 :
listname × optionZ
m1 :
Memory.mem
base :
Z
E :
access_resm base + off Objbase bytes r al = Someok
H :
Somebind_resq checked_resok WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr fr_localsfr m = SomeIContinuee1 l1 m1
⊢
∃base0 : Z, SomeSomebase = SomeSomebase0 ∧ m1 = m ∧ e1 = putq WPtrptr_addr ≔ base0 + off; ptr_cap ≔ Objbase0 fr_envfr ∧ access_resm base0 + off Objbase0 bytes r al = Someok

injection H as ← ← ←

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al, base :
Z
E :
access_resm base + off Objbase bytes r al = Someok
⊢
∃base0 : Z, SomeSomebase = SomeSomebase0 ∧ m = m ∧ putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr = putq WPtrptr_addr ≔ base0 + off; ptr_cap ≔ Objbase0 fr_envfr ∧ access_resm base0 + off Objbase0 bytes r al = Someok

eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros ge fr m q x off bytes r al e1 l1 m1 H
unfold inst_step in H
cbn iota beta zeta in H
destruct lookupx fr_localsfr as base | | ; try discriminate H
destruct access_resm base + off Objbase bytes r al as | w | w | eqn: E ; try discriminate H
injection H as ← ← ←
eauto

A check_function that continues binds its result q to a pointer p whose function check passed (function_check_res).

302Lemma check_function_step
∀ ge fr m q args e1 l1 m1
inst_stepge fr m Letq F CheckFunction args = SomeIContinuee1 l1 m1
∃p, function_check_resge p = Someok ∧ e1 = putq WPtrp fr_envfr
Explore proof 6 tactics

Initial goal

⊢
∀ge : genv fr : frame m : Memory.mem q : name args : listvalue e1 : env l1 : listname × optionZ m1 : Memory.mem, inst_stepge fr m Letq F CheckFunction args = SomeIContinuee1 l1 m1 → ∃p : ptr, function_check_resge p = Someok ∧ e1 = putq WPtrp fr_envfr

intros ge fr m q args e1 l1 m1 H

ge :
genv
fr :
frame
m :
Memory.mem
q :
name
args :
listvalue
e1 :
env
l1 :
listname × optionZ
m1 :
Memory.mem
H :
inst_stepge fr m Letq F CheckFunction args = SomeIContinuee1 l1 m1
⊢
∃p : ptr, function_check_resge p = Someok ∧ e1 = putq WPtrp fr_envfr

destruct args as | v | v′ args ; unfold inst_step in H ; cbn iota beta zeta in H ; try discriminate H

ge :
genv
fr :
frame
m :
Memory.mem
q :
name
v :
value
e1 :
env
l1 :
listname × optionZ
m1 :
Memory.mem
H :
match value_xge fr_envfr P v with
SomeWPtrp as x
⇒
let* chk ≔ function_check_resge p in
Somebind_resq checked_reschk x fr_envfr fr_localsfr m
_
⇒
None
=
SomeIContinuee1 l1 m1
⊢
∃p : ptr, function_check_resge p = Someok ∧ e1 = putq WPtrp fr_envfr

destruct value_xge fr_envfr P v as n | p | c size | ; try discriminate H

ge :
genv
fr :
frame
m :
Memory.mem
q :
name
v :
value
e1 :
env
l1 :
listname × optionZ
m1 :
Memory.mem
p :
ptr
H :
let* chk ≔ function_check_resge p in
Somebind_resq checked_reschk WPtrp fr_envfr fr_localsfr m
=
SomeIContinuee1 l1 m1
⊢
∃p0 : ptr, function_check_resge p0 = Someok ∧ e1 = putq WPtrp0 fr_envfr

destruct function_check_resge p as | w | w | eqn: E ; try discriminate H

ge :
genv
fr :
frame
m :
Memory.mem
q :
name
v :
value
e1 :
env
l1 :
listname × optionZ
m1 :
Memory.mem
p :
ptr
E :
function_check_resge p = Someok
H :
Somebind_resq checked_resok WPtrp fr_envfr fr_localsfr m = SomeIContinuee1 l1 m1
⊢
∃p0 : ptr, function_check_resge p0 = Someok ∧ e1 = putq WPtrp0 fr_envfr

injection H as ← ← ←

ge :
genv
fr :
frame
m :
Memory.mem
q :
name
v :
value
p :
ptr
E :
function_check_resge p = Someok
⊢
∃p0 : ptr, function_check_resge p0 = Someok ∧ putq WPtrp fr_envfr = putq WPtrp0 fr_envfr

eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros ge fr m q args e1 l1 m1 H
destruct args as | v | v′ args ; unfold inst_step in H ; cbn iota beta zeta in H ; try discriminate H
destruct value_xge fr_envfr P v as n | p | c size | ; try discriminate H
destruct function_check_resge p as | w | w | eqn: E ; try discriminate H
injection H as ← ← ←
eauto

An access check that passes on the object at base, for size bytes at address a, finds base's region in memory and the bytes inside it, from base up to its end.

316Lemma access_res_obj
∀ m a base size r al
access_resm a Objbase size r al = Someok
∃reg, object_regionbase m_regionsm = Somereg ∧ base ≤ a ∧ a + size ≤ r_endreg
Explore proof 8 tactics

Initial goal

⊢
∀m : Memory.mem a base size : Z r : rights al : Z, access_resm a Objbase size r al = Someok → ∃reg : region, object_regionbase m_regionsm = Somereg ∧ base ≤ a ∧ a + size ≤ r_endreg

unfold access_res , cap_access_res

⊢
∀ m : Memory.mem a base size : Z  ,
rights
→
∀ al : Z  ,
let* reg ≔ object_regionbase m_regionsm in
Some
base ≤? a && a + size ≤? r_endreg
→
aligned_resa al
else
RTrapOutOfBounds
=
Someok
→
∃reg : region, object_regionbase m_regionsm = Somereg ∧ base ≤ a ∧ a + size ≤ r_endreg

intros m a base size r al H

m :
Memory.mem
a, base, size :
Z
r :
rights
al :
Z
H :
let* reg ≔ object_regionbase m_regionsm in
Some
base ≤? a && a + size ≤? r_endreg
→
aligned_resa al
else
RTrapOutOfBounds
=
Someok
⊢
∃reg : region, object_regionbase m_regionsm = Somereg ∧ base ≤ a ∧ a + size ≤ r_endreg

destruct object_regionbase m_regionsm as reg | ; | discriminate H

m :
Memory.mem
a, base, size :
Z
r :
rights
al :
Z
reg :
region
H :
Some
base ≤? a && a + size ≤? r_endreg
→
aligned_resa al
else
RTrapOutOfBounds
=
Someok
⊢
∃reg0 : region, Somereg = Somereg0 ∧ base ≤ a ∧ a + size ≤ r_endreg0

destruct base ≤? a && a + size ≤? r_endreg eqn: E ; | discriminate H

m :
Memory.mem
a, base, size :
Z
r :
rights
al :
Z
reg :
region
E :
base ≤? a && a + size ≤? r_endreg = true
H :
Somealigned_resa al = Someok
⊢
∃reg0 : region, Somereg = Somereg0 ∧ base ≤ a ∧ a + size ≤ r_endreg0

apply andb_true_iff in E as E1 E2

m :
Memory.mem
a, base, size :
Z
r :
rights
al :
Z
reg :
region
E1 :
base ≤? a = true
E2 :
a + size ≤? r_endreg = true
H :
Somealigned_resa al = Someok
⊢
∃reg0 : region, Somereg = Somereg0 ∧ base ≤ a ∧ a + size ≤ r_endreg0

apply Z.leb_le in E1

m :
Memory.mem
a, base, size :
Z
r :
rights
al :
Z
reg :
region
E1 :
base ≤ a
E2 :
a + size ≤? r_endreg = true
H :
Somealigned_resa al = Someok
⊢
∃reg0 : region, Somereg = Somereg0 ∧ base ≤ a ∧ a + size ≤ r_endreg0

apply Z.leb_le in E2

m :
Memory.mem
a, base, size :
Z
r :
rights
al :
Z
reg :
region
E1 :
base ≤ a
E2 :
a + size ≤ r_endreg
H :
Somealigned_resa al = Someok
⊢
∃reg0 : region, Somereg = Somereg0 ∧ base ≤ a ∧ a + size ≤ r_endreg0

eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
unfold access_res , cap_access_res
intros m a base size r al H
destruct object_regionbase m_regionsm as reg | ; | discriminate H
destruct base ≤? a && a + size ≤? r_endreg eqn: E ; | discriminate H
apply andb_true_iff in E as E1 E2
apply Z.leb_le in E1
apply Z.leb_le in E2
eauto

A covered access lies inside the checked range, from lo up to hi, so that range is not empty.

328Lemma covered_nonempty
∀ i q lo hi r al
covered_accessi q lo hi r al = true
lo < hi
Explore proof 9 tactics

Initial goal

⊢
∀i : inst q : name lo hi : Z r : rights al : Z, covered_accessi q lo hi r al = true → lo < hi

unfold covered_access

⊢
∀ i : inst q : name lo hi : Z r : rights al : Z  ,
match raw_accessi with
Someq′, x, off, need
⇒
let size, aa ≔ access_size_alignx in
name_eqbq′ q && lo ≤? off && off + size ≤? hi && al mod aa =? 0 && off − lo mod aa =? 0 && rights_allowr need
None
⇒
false
=
true
→
lo < hi

intros i q lo hi r al H

i :
inst
q :
name
lo, hi :
Z
r :
rights
al :
Z
H :
match raw_accessi with
Someq′, x, off, need
⇒
let size, aa ≔ access_size_alignx in
name_eqbq′ q && lo ≤? off && off + size ≤? hi && al mod aa =? 0 && off − lo mod aa =? 0 && rights_allowr need
None
⇒
false
=
true
⊢
lo < hi

destruct raw_accessi as q′ x off need | ; | discriminate H

i :
inst
q :
name
lo, hi :
Z
r :
rights
al :
Z
q′ :
name
x :
access_type
off :
Z
need :
rights
H :
let size, aa ≔ access_size_alignx in
name_eqbq′ q && lo ≤? off && off + size ≤? hi && al mod aa =? 0 && off − lo mod aa =? 0 && rights_allowr need
=
true
⊢
lo < hi

pose proof access_size_align_posx as Hs _

i :
inst
q :
name
lo, hi :
Z
r :
rights
al :
Z
q′ :
name
x :
access_type
off :
Z
need :
rights
H :
let size, aa ≔ access_size_alignx in
name_eqbq′ q && lo ≤? off && off + size ≤? hi && al mod aa =? 0 && off − lo mod aa =? 0 && rights_allowr need
=
true
Hs :
0 < fstaccess_size_alignx
⊢
lo < hi

destruct access_size_alignx as size aa

i :
inst
q :
name
lo, hi :
Z
r :
rights
al :
Z
q′ :
name
x :
access_type
off :
Z
need :
rights
size, aa :
Z
H :
name_eqbq′ q && lo ≤? off && off + size ≤? hi && al mod aa =? 0 && off − lo mod aa =? 0 && rights_allowr need = true
Hs :
0 < fstsize, aa
⊢
lo < hi

simpl in Hs

i :
inst
q :
name
lo, hi :
Z
r :
rights
al :
Z
q′ :
name
x :
access_type
off :
Z
need :
rights
size, aa :
Z
H :
name_eqbq′ q && lo ≤? off && off + size ≤? hi && al mod aa =? 0 && off − lo mod aa =? 0 && rights_allowr need = true
Hs :
0 < size
⊢
lo < hi

repeat match goal withHb : _ && _ = true |- _⇒apply andb_true_iff in Hb as ? ?end

i :
inst
q :
name
lo, hi :
Z
r :
rights
al :
Z
q′ :
name
x :
access_type
off :
Z
need :
rights
size, aa :
Z
H :
name_eqbq′ q = true
H4 :
lo ≤? off = true
H3 :
off + size ≤? hi = true
H2 :
al mod aa =? 0 = true
H1 :
off − lo mod aa =? 0 = true
H0 :
rights_allowr need = true
Hs :
0 < size
⊢
lo < hi

repeat match goal withHb : _ ≤? _ = true |- _⇒apply Z.leb_le in Hbend

i :
inst
q :
name
lo, hi :
Z
r :
rights
al :
Z
q′ :
name
x :
access_type
off :
Z
need :
rights
size, aa :
Z
H :
name_eqbq′ q = true
H4 :
lo ≤ off
H3 :
off + size ≤ hi
H2 :
al mod aa =? 0 = true
H1 :
off − lo mod aa =? 0 = true
H0 :
rights_allowr need = true
Hs :
0 < size
⊢
lo < hi

lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
unfold covered_access
intros i q lo hi r al H
destruct raw_accessi as q′ x off need | ; | discriminate H
pose proof access_size_align_posx as Hs _
destruct access_size_alignx as size aa
simpl in Hs
repeat match goal withHb : _ && _ = true |- _⇒apply andb_true_iff in Hb as ? ?end
repeat match goal withHb : _ ≤? _ = true |- _⇒apply Z.leb_le in Hbend
lia

The pass takes a check_local together with the access after it: that access is covered by the check's range, from 0 up to bytes, and the facts after are what the access (evidence_after) leaves of the live facts less those about q (kill).

342Lemma checked_inst_rest_local_cov
∀ 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′ ∧ covered_accessaccess q 0 bytes r al = true ∧ live′ = evidence_afteraccess killq live
Explore proof 11 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′ ∧ covered_accessaccess q 0 bytes r al = true ∧ live′ = evidence_afteraccess killq live

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

s :
src
q, x :
name
off, bytes :
Z
r :
rights
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′ ∧ covered_accessaccess q 0 bytes r al = true ∧ live′ = evidence_afteraccess killq live

unfold checked_inst_rest in H

s :
src
q, x :
name
off, bytes :
Z
r :
rights
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′ ∧ covered_accessaccess q 0 bytes r al = true ∧ live′ = evidence_afteraccess killq live

cbn zeta in H

s :
src
q, x :
name
off, bytes :
Z
r :
rights
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′ ∧ covered_accessaccess q 0 bytes r al = true ∧ live′ = evidence_afteraccess killq live

destruct rest as | access rest0 ; discriminate H |

s :
src
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
access :
inst
rest0 :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
match raw_accessaccess with
Someq′, _, 0, _
⇒
name_eqbq′ q && covered_accessaccess q 0 bytes r al && storage_effectsaccess Local'
→
Somerest0, evidence_afteraccess killq live
else
None
Someq′, _, Z.pos_, _ | Someq′, _, Z.neg_, _
⇒
None
None
⇒
None
=
Somerest′, live′
⊢
∃access0 : inst, access :: rest0 = access0 :: rest′ ∧ covered_accessaccess0 q 0 bytes r al = true ∧ live′ = evidence_afteraccess0 killq live

destruct raw_accessaccess as q′ xa o need | ; | discriminate H

s :
src
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
access :
inst
rest0 :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
q′ :
name
xa :
access_type
o :
Z
need :
rights
H :
match o with
0
⇒
name_eqbq′ q && covered_accessaccess q 0 bytes r al && storage_effectsaccess Local'
→
Somerest0, evidence_afteraccess killq live
else
None
_
⇒
None
=
Somerest′, live′
⊢
∃access0 : inst, access :: rest0 = access0 :: rest′ ∧ covered_accessaccess0 q 0 bytes r al = true ∧ live′ = evidence_afteraccess0 killq live

destruct o ; try discriminate H

s :
src
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
access :
inst
rest0 :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
q′ :
name
xa :
access_type
need :
rights
H :
name_eqbq′ q && covered_accessaccess q 0 bytes r al && storage_effectsaccess Local'
→
Somerest0, evidence_afteraccess killq live
else
None
=
Somerest′, live′
⊢
∃access0 : inst, access :: rest0 = access0 :: rest′ ∧ covered_accessaccess0 q 0 bytes r al = true ∧ live′ = evidence_afteraccess0 killq live

destruct name_eqbq′ q && covered_accessaccess q 0 bytes r al && storage_effectsaccess Local' eqn: E ; | discriminate H

s :
src
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
access :
inst
rest0 :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
q′ :
name
xa :
access_type
need :
rights
E :
name_eqbq′ q && covered_accessaccess q 0 bytes r al && storage_effectsaccess Local' = true
H :
Somerest0, evidence_afteraccess killq live = Somerest′, live′
⊢
∃access0 : inst, access :: rest0 = access0 :: rest′ ∧ covered_accessaccess0 q 0 bytes r al = true ∧ live′ = evidence_afteraccess0 killq live

injection H as ← ←

s :
src
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
access :
inst
rest0 :
listinst
live :
listfact
q′ :
name
xa :
access_type
need :
rights
E :
name_eqbq′ q && covered_accessaccess q 0 bytes r al && storage_effectsaccess Local' = true
⊢
∃access0 : inst, access :: rest0 = access0 :: rest0 ∧ covered_accessaccess0 q 0 bytes r al = true ∧ evidence_afteraccess killq live = evidence_afteraccess0 killq live

apply andb_true_iff in E as E _

s :
src
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
access :
inst
rest0 :
listinst
live :
listfact
q′ :
name
xa :
access_type
need :
rights
E :
name_eqbq′ q && covered_accessaccess q 0 bytes r al = true
⊢
∃access0 : inst, access :: rest0 = access0 :: rest0 ∧ covered_accessaccess0 q 0 bytes r al = true ∧ evidence_afteraccess killq live = evidence_afteraccess0 killq live

apply andb_true_iff in E as _ E

s :
src
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
access :
inst
rest0 :
listinst
live :
listfact
q′ :
name
xa :
access_type
need :
rights
E :
covered_accessaccess q 0 bytes r al = true
⊢
∃access0 : inst, access :: rest0 = access0 :: rest0 ∧ covered_accessaccess0 q 0 bytes r al = true ∧ evidence_afteraccess killq live = evidence_afteraccess0 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
destruct rest as | access rest0 ; discriminate H |
destruct raw_accessaccess as q′ xa o need | ; | discriminate H
destruct o ; try discriminate H
destruct name_eqbq′ q && covered_accessaccess q 0 bytes r al && storage_effectsaccess Local' eqn: E ; | discriminate H
injection H as ← ←
apply andb_true_iff in E as E _
apply andb_true_iff in E as _ E
eauto

After a check_local q of the local x that continues, in a memory whose objects fit (objects_fit) and a frame whose locals lie above address 0, the memory is unchanged, the environment changed only at q, and the check's access holds as a fact of q (fact_holds).

360Lemma check_local_fact
∀ ge fr m q x off bytes r al e1 l1 m1 access
objects_fitm_regionsm
∀y base, lookupy fr_localsfr = SomeSomebase → 0 < base
covered_accessaccess q 0 bytes r al = true
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinuee1 l1 m1
m1 = m ∧ env_agreeq fr_envfr e1 ∧ fact_holdsge m1 e1 mkFactq Tmpq 0 bytes r al
Explore proof 17 tactics

Initial goal

⊢
∀ge : genv fr : frame m : Memory.mem q x : name off bytes : Z r : rights al : Z e1 : env l1 : listname × optionZ m1 : Memory.mem access : inst, objects_fitm_regionsm → ∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base → covered_accessaccess q 0 bytes r al = true → inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinuee1 l1 m1 → m1 = m ∧ env_agreeq fr_envfr e1 ∧ fact_holdsge m1 e1 f_q ≔ q; f_p ≔ Tmpq; f_lo ≔ 0; f_hi ≔ bytes; f_r ≔ r; f_al ≔ al

intros ge fr m q x off bytes r al e1 l1 m1 access Hfit Hpos Hcov H

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
e1 :
env
l1 :
listname × optionZ
m1 :
Memory.mem
access :
inst
Hfit :
objects_fitm_regionsm
Hpos :
∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base
Hcov :
covered_accessaccess q 0 bytes r al = true
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinuee1 l1 m1
⊢
m1 = m ∧ env_agreeq fr_envfr e1 ∧ fact_holdsge m1 e1 f_q ≔ q; f_p ≔ Tmpq; f_lo ≔ 0; f_hi ≔ bytes; f_r ≔ r; f_al ≔ al

destruct check_local_step_ _ _ _ _ _ _ _ _ _ _ _ H as base & Hl & → & → & Hc

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
l1 :
listname × optionZ
access :
inst
Hfit :
objects_fitm_regionsm
Hpos :
∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base
Hcov :
covered_accessaccess q 0 bytes r al = true
base :
Z
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinueputq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr l1 m
Hl :
lookupx fr_localsfr = SomeSomebase
Hc :
access_resm base + off Objbase bytes r al = Someok
⊢
m = m ∧ env_agreeq fr_envfr putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr ∧ fact_holdsge m putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr f_q ≔ q; f_p ≔ Tmpq; f_lo ≔ 0; f_hi ≔ bytes; f_r ≔ r; f_al ≔ al

split ; reflexivity |

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
l1 :
listname × optionZ
access :
inst
Hfit :
objects_fitm_regionsm
Hpos :
∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base
Hcov :
covered_accessaccess q 0 bytes r al = true
base :
Z
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinueputq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr l1 m
Hl :
lookupx fr_localsfr = SomeSomebase
Hc :
access_resm base + off Objbase bytes r al = Someok
⊢
env_agreeq fr_envfr putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr ∧ fact_holdsge m putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr f_q ≔ q; f_p ≔ Tmpq; f_lo ≔ 0; f_hi ≔ bytes; f_r ≔ r; f_al ≔ al

split ; apply env_agree_put |

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
l1 :
listname × optionZ
access :
inst
Hfit :
objects_fitm_regionsm
Hpos :
∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base
Hcov :
covered_accessaccess q 0 bytes r al = true
base :
Z
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinueputq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr l1 m
Hl :
lookupx fr_localsfr = SomeSomebase
Hc :
access_resm base + off Objbase bytes r al = Someok
⊢
fact_holdsge m putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr f_q ≔ q; f_p ≔ Tmpq; f_lo ≔ 0; f_hi ≔ bytes; f_r ≔ r; f_al ≔ al

pose proof covered_nonempty_ _ _ _ _ _ Hcov as Hb

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
l1 :
listname × optionZ
access :
inst
Hfit :
objects_fitm_regionsm
Hpos :
∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base
Hcov :
covered_accessaccess q 0 bytes r al = true
base :
Z
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinueputq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr l1 m
Hl :
lookupx fr_localsfr = SomeSomebase
Hc :
access_resm base + off Objbase bytes r al = Someok
Hb :
0 < bytes
⊢
fact_holdsge m putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr f_q ≔ q; f_p ≔ Tmpq; f_lo ≔ 0; f_hi ≔ bytes; f_r ≔ r; f_al ≔ al

pose proof Hpos_ _ Hl as Hbase

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
l1 :
listname × optionZ
access :
inst
Hfit :
objects_fitm_regionsm
Hpos :
∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base
Hcov :
covered_accessaccess q 0 bytes r al = true
base :
Z
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinueputq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr l1 m
Hl :
lookupx fr_localsfr = SomeSomebase
Hc :
access_resm base + off Objbase bytes r al = Someok
Hb :
0 < bytes
Hbase :
0 < base
⊢
fact_holdsge m putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr f_q ≔ q; f_p ≔ Tmpq; f_lo ≔ 0; f_hi ≔ bytes; f_r ≔ r; f_al ≔ al

destruct access_res_obj_ _ _ _ _ _ Hc as reg & Er & H1 & H2

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
l1 :
listname × optionZ
access :
inst
Hfit :
objects_fitm_regionsm
Hpos :
∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base
Hcov :
covered_accessaccess q 0 bytes r al = true
base :
Z
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinueputq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr l1 m
Hl :
lookupx fr_localsfr = SomeSomebase
Hc :
access_resm base + off Objbase bytes r al = Someok
Hb :
0 < bytes
Hbase :
0 < base
reg :
region
Er :
object_regionbase m_regionsm = Somereg
H1 :
base ≤ base + off
H2 :
base + off + bytes ≤ r_endreg
⊢
fact_holdsge m putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr f_q ≔ q; f_p ≔ Tmpq; f_lo ≔ 0; f_hi ≔ bytes; f_r ≔ r; f_al ≔ al

pose proof Hfit_ _ Er as Hend

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
l1 :
listname × optionZ
access :
inst
Hfit :
objects_fitm_regionsm
Hpos :
∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base
Hcov :
covered_accessaccess q 0 bytes r al = true
base :
Z
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinueputq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr l1 m
Hl :
lookupx fr_localsfr = SomeSomebase
Hc :
access_resm base + off Objbase bytes r al = Someok
Hb :
0 < bytes
Hbase :
0 < base
reg :
region
Er :
object_regionbase m_regionsm = Somereg
H1 :
base ≤ base + off
H2 :
base + off + bytes ≤ r_endreg
Hend :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
⊢
fact_holdsge m putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr f_q ≔ q; f_p ≔ Tmpq; f_lo ≔ 0; f_hi ≔ bytes; f_r ≔ r; f_al ≔ al

exists mkPtrbase + off Objbase

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
l1 :
listname × optionZ
access :
inst
Hfit :
objects_fitm_regionsm
Hpos :
∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base
Hcov :
covered_accessaccess q 0 bytes r al = true
base :
Z
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinueputq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr l1 m
Hl :
lookupx fr_localsfr = SomeSomebase
Hc :
access_resm base + off Objbase bytes r al = Someok
Hb :
0 < bytes
Hbase :
0 < base
reg :
region
Er :
object_regionbase m_regionsm = Somereg
H1 :
base ≤ base + off
H2 :
base + off + bytes ≤ r_endreg
Hend :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
⊢
lookupf_qf_q ≔ q; f_p ≔ Tmpq; f_lo ≔ 0; f_hi ≔ bytes; f_r ≔ r; f_al ≔ al putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr = SomeWPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase ∧ value_xge putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr P f_pf_q ≔ q; f_p ≔ Tmpq; f_lo ≔ 0; f_hi ≔ bytes; f_r ≔ r; f_al ≔ al = SomeWPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase ∧ check_passesm ptr_addr ≔ base + off; ptr_cap ≔ Objbase f_lof_q ≔ q; f_p ≔ Tmpq; f_lo ≔ 0; f_hi ≔ bytes; f_r ≔ r; f_al ≔ al f_hif_q ≔ q; f_p ≔ Tmpq; f_lo ≔ 0; f_hi ≔ bytes; f_r ≔ r; f_al ≔ al f_rf_q ≔ q; f_p ≔ Tmpq; f_lo ≔ 0; f_hi ≔ bytes; f_r ≔ r; f_al ≔ al f_alf_q ≔ q; f_p ≔ Tmpq; f_lo ≔ 0; f_hi ≔ bytes; f_r ≔ r; f_al ≔ al

cbn [ f_q f_p f_lo f_hi f_r f_al ]

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
l1 :
listname × optionZ
access :
inst
Hfit :
objects_fitm_regionsm
Hpos :
∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base
Hcov :
covered_accessaccess q 0 bytes r al = true
base :
Z
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinueputq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr l1 m
Hl :
lookupx fr_localsfr = SomeSomebase
Hc :
access_resm base + off Objbase bytes r al = Someok
Hb :
0 < bytes
Hbase :
0 < base
reg :
region
Er :
object_regionbase m_regionsm = Somereg
H1 :
base ≤ base + off
H2 :
base + off + bytes ≤ r_endreg
Hend :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
⊢
lookupq putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr = SomeWPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase ∧ value_xge putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr P Tmpq = SomeWPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase ∧ check_passesm ptr_addr ≔ base + off; ptr_cap ≔ Objbase 0 bytes r al

split ; apply lookup_put_same |

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
l1 :
listname × optionZ
access :
inst
Hfit :
objects_fitm_regionsm
Hpos :
∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base
Hcov :
covered_accessaccess q 0 bytes r al = true
base :
Z
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinueputq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr l1 m
Hl :
lookupx fr_localsfr = SomeSomebase
Hc :
access_resm base + off Objbase bytes r al = Someok
Hb :
0 < bytes
Hbase :
0 < base
reg :
region
Er :
object_regionbase m_regionsm = Somereg
H1 :
base ≤ base + off
H2 :
base + off + bytes ≤ r_endreg
Hend :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
⊢
value_xge putq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr P Tmpq = SomeWPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase ∧ check_passesm ptr_addr ≔ base + off; ptr_cap ≔ Objbase 0 bytes r al

split ; unfold value_x ; rewrite lookup_put_same ; reflexivity |

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
l1 :
listname × optionZ
access :
inst
Hfit :
objects_fitm_regionsm
Hpos :
∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base
Hcov :
covered_accessaccess q 0 bytes r al = true
base :
Z
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinueputq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr l1 m
Hl :
lookupx fr_localsfr = SomeSomebase
Hc :
access_resm base + off Objbase bytes r al = Someok
Hb :
0 < bytes
Hbase :
0 < base
reg :
region
Er :
object_regionbase m_regionsm = Somereg
H1 :
base ≤ base + off
H2 :
base + off + bytes ≤ r_endreg
Hend :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
⊢
check_passesm ptr_addr ≔ base + off; ptr_cap ≔ Objbase 0 bytes r al

unfold check_passes , raw_address

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
l1 :
listname × optionZ
access :
inst
Hfit :
objects_fitm_regionsm
Hpos :
∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base
Hcov :
covered_accessaccess q 0 bytes r al = true
base :
Z
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinueputq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr l1 m
Hl :
lookupx fr_localsfr = SomeSomebase
Hc :
access_resm base + off Objbase bytes r al = Someok
Hb :
0 < bytes
Hbase :
0 < base
reg :
region
Er :
object_regionbase m_regionsm = Somereg
H1 :
base ≤ base + off
H2 :
base + off + bytes ≤ r_endreg
Hend :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
⊢
access_resm ptr_addrptr_addr ≔ base + off; ptr_cap ≔ Objbase + 0 mod 2 ^ 64 ptr_capptr_addr ≔ base + off; ptr_cap ≔ Objbase bytes − 0 r al = Someok

simpl ptr_addr

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
l1 :
listname × optionZ
access :
inst
Hfit :
objects_fitm_regionsm
Hpos :
∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base
Hcov :
covered_accessaccess q 0 bytes r al = true
base :
Z
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinueputq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr l1 m
Hl :
lookupx fr_localsfr = SomeSomebase
Hc :
access_resm base + off Objbase bytes r al = Someok
Hb :
0 < bytes
Hbase :
0 < base
reg :
region
Er :
object_regionbase m_regionsm = Somereg
H1 :
base ≤ base + off
H2 :
base + off + bytes ≤ r_endreg
Hend :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
⊢
access_resm base + off + 0 mod 2 ^ 64 ptr_capptr_addr ≔ base + off; ptr_cap ≔ Objbase bytes − 0 r al = Someok

simpl ptr_cap

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
l1 :
listname × optionZ
access :
inst
Hfit :
objects_fitm_regionsm
Hpos :
∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base
Hcov :
covered_accessaccess q 0 bytes r al = true
base :
Z
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinueputq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr l1 m
Hl :
lookupx fr_localsfr = SomeSomebase
Hc :
access_resm base + off Objbase bytes r al = Someok
Hb :
0 < bytes
Hbase :
0 < base
reg :
region
Er :
object_regionbase m_regionsm = Somereg
H1 :
base ≤ base + off
H2 :
base + off + bytes ≤ r_endreg
Hend :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
⊢
access_resm base + off + 0 mod 2 ^ 64 Objbase bytes − 0 r al = Someok

rewrite Z.sub_0_r , Z.add_0_r , Z.mod_small by lia

ge :
genv
fr :
frame
m :
Memory.mem
q, x :
name
off, bytes :
Z
r :
rights
al :
Z
l1 :
listname × optionZ
access :
inst
Hfit :
objects_fitm_regionsm
Hpos :
∀y : name base : Z, lookupy fr_localsfr = SomeSomebase → 0 < base
Hcov :
covered_accessaccess q 0 bytes r al = true
base :
Z
H :
inst_stepge fr m Letq A CheckLocalx off bytes r al [ ] = SomeIContinueputq WPtrptr_addr ≔ base + off; ptr_cap ≔ Objbase fr_envfr l1 m
Hl :
lookupx fr_localsfr = SomeSomebase
Hc :
access_resm base + off Objbase bytes r al = Someok
Hb :
0 < bytes
Hbase :
0 < base
reg :
region
Er :
object_regionbase m_regionsm = Somereg
H1 :
base ≤ base + off
H2 :
base + off + bytes ≤ r_endreg
Hend :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
⊢
access_resm base + off Objbase bytes r al = Someok

exact Hc

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros ge fr m q x off bytes r al e1 l1 m1 access Hfit Hpos Hcov H
destruct check_local_step_ _ _ _ _ _ _ _ _ _ _ _ H as base & Hl & → & → & Hc
split ; reflexivity |
split ; apply env_agree_put |
pose proof covered_nonempty_ _ _ _ _ _ Hcov as Hb
pose proof Hpos_ _ Hl as Hbase
destruct access_res_obj_ _ _ _ _ _ Hc as reg & Er & H1 & H2
pose proof Hfit_ _ Er as Hend
exists mkPtrbase + off Objbase
cbn [ f_q f_p f_lo f_hi f_r f_al ]
split ; apply lookup_put_same |
split ; unfold value_x ; rewrite lookup_put_same ; reflexivity |
unfold check_passes , raw_address
simpl ptr_addr
simpl ptr_cap
rewrite Z.sub_0_r , Z.add_0_r , Z.mod_small by lia
exact Hc

The pass's sources of a function

The sources (src) the pass reads for the function f of the module md: what stage_sources/4 computes from f's dominator intervals, or from no intervals where there are none.

386Definition fn_srcmd : module f : func : src ≔
stage_sourcesmd f
match block_intervalsfn_blocksf with
Somedoms
⇒
doms
None
⇒
nm_empty

The label of the function f's entry block, its first, if it has blocks.

390Definition entry_labelf : func : optionname ≔
match fn_blocksf with
b :: _
⇒
Someb_labelb
[ ]
⇒
None

md is valid and in the checked stage, so each of its functions passed the evidence pass.

395Definition checked_modulemd : module : Prop ≔
validmd = Sometrue ∧ module_checkedmd = true

Every function f of a checked_module md has distinct block labels and an entry block that no jump goes to, and the pass computes its exit facts.

400Lemma module_func
∀ md f
checked_modulemd
InIFuncf md
no_dupsmapb_label fn_blocksf = true ∧ ∃b0 bs, fn_blocksf = b0 :: bs ∧ existsbλb ⇒ memb_labelb0 succ_labelsb_jumpb fn_blocksf = false ∧ ∃E, pass_exitsfn_srcmd f f = SomeE
Explore proof 24 tactics

Initial goal

⊢
∀md : module f : func, checked_modulemd → InIFuncf md → no_dupsmapb_label fn_blocksf = true ∧ ∃b0 : block bs : listblock, fn_blocksf = b0 :: bs ∧ existsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb fn_blocksf = false ∧ ∃E : listname × listfact, pass_exitsfn_srcmd f f = SomeE

unfold checked_module , valid

⊢
∀ md : module f : func  ,
existsb
λ it : item  ⇒
match it with
IOutside_ _
⇒
true
_
⇒
false
md
→
None
else
Somevalid_itemsmd
=
Sometrue
∧
module_checkedmd = true
→
InIFuncf md → no_dupsmapb_label fn_blocksf = true ∧ ∃b0 : block bs : listblock, fn_blocksf = b0 :: bs ∧ existsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb fn_blocksf = false ∧ ∃E : listname × listfact, pass_exitsfn_srcmd f f = SomeE

intros md f Hv Hc Hin

md :
module
f :
func
Hv :
existsb
λ it : item  ⇒
match it with
IOutside_ _
⇒
true
_
⇒
false
md
→
None
else
Somevalid_itemsmd
=
Sometrue
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
no_dupsmapb_label fn_blocksf = true ∧ ∃b0 : block bs : listblock, fn_blocksf = b0 :: bs ∧ existsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb fn_blocksf = false ∧ ∃E : listname × listfact, pass_exitsfn_srcmd f f = SomeE

destruct existsb_ md ; discriminate Hv |

md :
module
f :
func
Hv :
Somevalid_itemsmd = Sometrue
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
no_dupsmapb_label fn_blocksf = true ∧ ∃b0 : block bs : listblock, fn_blocksf = b0 :: bs ∧ existsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb fn_blocksf = false ∧ ∃E : listname × listfact, pass_exitsfn_srcmd f f = SomeE

injection Hv as Hv

md :
module
f :
func
Hv :
valid_itemsmd = true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
no_dupsmapb_label fn_blocksf = true ∧ ∃b0 : block bs : listblock, fn_blocksf = b0 :: bs ∧ existsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb fn_blocksf = false ∧ ∃E : listname × listfact, pass_exitsfn_srcmd f f = SomeE

unfold valid_items in Hv

md :
module
f :
func
Hv :
unique_namesmd
&&
forallb
λ it : item  ⇒
match it with
IFuncf
⇒
valid_funcmd f
IOutside_ _
⇒
true
IDatan lk al its
⇒
valid_datamd n lk al its
IAliasn lk t
⇒
valid_aliasmd n lk t
md
=
true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
no_dupsmapb_label fn_blocksf = true ∧ ∃b0 : block bs : listblock, fn_blocksf = b0 :: bs ∧ existsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb fn_blocksf = false ∧ ∃E : listname × listfact, pass_exitsfn_srcmd f f = SomeE

apply andb_true_iff in Hv as _ Hv

md :
module
f :
func
Hv :
forallb
λ it : item  ⇒
match it with
IFuncf
⇒
valid_funcmd f
IOutside_ _
⇒
true
IDatan lk al its
⇒
valid_datamd n lk al its
IAliasn lk t
⇒
valid_aliasmd n lk t
md
=
true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
no_dupsmapb_label fn_blocksf = true ∧ ∃b0 : block bs : listblock, fn_blocksf = b0 :: bs ∧ existsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb fn_blocksf = false ∧ ∃E : listname × listfact, pass_exitsfn_srcmd f f = SomeE

rewrite forallb_forall in Hv

md :
module
f :
func
Hv :
∀ x : item  ,
Inx md
→
match x with
IFuncf
⇒
valid_funcmd f
IOutside_ _
⇒
true
IDatan lk al its
⇒
valid_datamd n lk al its
IAliasn lk t
⇒
valid_aliasmd n lk t
=
true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
no_dupsmapb_label fn_blocksf = true ∧ ∃b0 : block bs : listblock, fn_blocksf = b0 :: bs ∧ existsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb fn_blocksf = false ∧ ∃E : listname × listfact, pass_exitsfn_srcmd f f = SomeE

specialize Hv_ Hin

md :
module
f :
func
Hv :
match IFuncf with
IFuncf
⇒
valid_funcmd f
IOutside_ _
⇒
true
IDatan lk al its
⇒
valid_datamd n lk al its
IAliasn lk t
⇒
valid_aliasmd n lk t
=
true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
no_dupsmapb_label fn_blocksf = true ∧ ∃b0 : block bs : listblock, fn_blocksf = b0 :: bs ∧ existsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb fn_blocksf = false ∧ ∃E : listname × listfact, pass_exitsfn_srcmd f f = SomeE

simpl in Hv

md :
module
f :
func
Hv :
valid_funcmd f = true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
no_dupsmapb_label fn_blocksf = true ∧ ∃b0 : block bs : listblock, fn_blocksf = b0 :: bs ∧ existsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb fn_blocksf = false ∧ ∃E : listname × listfact, pass_exitsfn_srcmd f f = SomeE

unfold valid_func , fn_src in *

md :
module
f :
func
Hv :
match fn_blocksf with
[ ]
⇒
false
entry :: l
⇒
match block_intervalsentry :: l with
Somedoms
⇒
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
&&
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
&&
negbextended_crossesf
&&
no_dupsmapb_label fn_blocksf
&&
temp_classes_oktemp_defsf
&&
negbexistsbλb : block ⇒ memb_labelentry succ_labelsb_jumpb fn_blocksf
&&
proof_class_defsf
&&
definitions_dominatef doms
&&
valid_localsf
&&
forallbvalid_blockmd f temp_defsf fn_blocksf
&&
negbmodule_checkedmd || stage_funcmd f doms
None
⇒
false
=
true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
no_dupsmapb_label fn_blocksf = true
∧
∃b0 : block bs : listblock, fn_blocksf = b0 :: bs ∧ existsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb fn_blocksf = false
∧
∃ E : listname × listfact  ,
pass_exits
stage_sourcesmd f
match block_intervalsfn_blocksf with
Somedoms
⇒
doms
None
⇒
nm_empty
f
=
SomeE

destruct fn_blocksf as | b0 bs eqn: Eb ; discriminate Hv |

md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
Hv :
match block_intervalsb0 :: bs with
Somedoms
⇒
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
&&
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
&&
negbextended_crossesf
&&
no_dupsmapb_label b0 :: bs
&&
temp_classes_oktemp_defsf
&&
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs
&&
proof_class_defsf
&&
definitions_dominatef doms
&&
valid_localsf
&&
forallbvalid_blockmd f temp_defsf b0 :: bs
&&
negbmodule_checkedmd || stage_funcmd f doms
None
⇒
false
=
true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
no_dupsmapb_label b0 :: bs = true
∧
∃b1 : block bs0 : listblock, b0 :: bs = b1 :: bs0 ∧ existsbλb : block ⇒ memb_labelb1 succ_labelsb_jumpb b0 :: bs = false
∧
∃ E : listname × listfact  ,
pass_exits
stage_sourcesmd f
match block_intervalsb0 :: bs with
Somedoms
⇒
doms
None
⇒
nm_empty
f
=
SomeE

destruct block_intervalsb0 :: bs as doms | ; | discriminate Hv

md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
doms :
nmapZ × Z
Hv :
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
&&
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
&&
negbextended_crossesf
&&
no_dupsmapb_label b0 :: bs
&&
temp_classes_oktemp_defsf
&&
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs
&&
proof_class_defsf
&&
definitions_dominatef doms
&&
valid_localsf
&&
forallbvalid_blockmd f temp_defsf b0 :: bs
&&
negbmodule_checkedmd || stage_funcmd f doms
=
true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
no_dupsmapb_label b0 :: bs = true ∧ ∃b1 : block bs0 : listblock, b0 :: bs = b1 :: bs0 ∧ existsbλb : block ⇒ memb_labelb1 succ_labelsb_jumpb b0 :: bs = false ∧ ∃E : listname × listfact, pass_exitsstage_sourcesmd f doms f = SomeE

rewrite Hc in Hv

md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
doms :
nmapZ × Z
Hv :
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
&&
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
&&
negbextended_crossesf
&&
no_dupsmapb_label b0 :: bs
&&
temp_classes_oktemp_defsf
&&
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs
&&
proof_class_defsf
&&
definitions_dominatef doms
&&
valid_localsf
&&
forallbvalid_blockmd f temp_defsf b0 :: bs
&&
negbtrue || stage_funcmd f doms
=
true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
no_dupsmapb_label b0 :: bs = true ∧ ∃b1 : block bs0 : listblock, b0 :: bs = b1 :: bs0 ∧ existsbλb : block ⇒ memb_labelb1 succ_labelsb_jumpb b0 :: bs = false ∧ ∃E : listname × listfact, pass_exitsstage_sourcesmd f doms f = SomeE

unfold stage_func in Hv

md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
doms :
nmapZ × Z
Hv :
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
&&
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
&&
negbextended_crossesf
&&
no_dupsmapb_label b0 :: bs
&&
temp_classes_oktemp_defsf
&&
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs
&&
proof_class_defsf
&&
definitions_dominatef doms
&&
valid_localsf
&&
forallbvalid_blockmd f temp_defsf b0 :: bs
&&
negbtrue || evidence_passstage_sourcesmd f doms f && limit_readsf && polls_every_cyclef
=
true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
no_dupsmapb_label b0 :: bs = true ∧ ∃b1 : block bs0 : listblock, b0 :: bs = b1 :: bs0 ∧ existsbλb : block ⇒ memb_labelb1 succ_labelsb_jumpb b0 :: bs = false ∧ ∃E : listname × listfact, pass_exitsstage_sourcesmd f doms f = SomeE

cbn [ negb orb ] in Hv

md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
doms :
nmapZ × Z
Hv :
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
&&
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
&&
negbextended_crossesf
&&
no_dupsmapb_label b0 :: bs
&&
temp_classes_oktemp_defsf
&&
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs
&&
proof_class_defsf
&&
definitions_dominatef doms
&&
valid_localsf
&&
forallbvalid_blockmd f temp_defsf b0 :: bs
&&
evidence_passstage_sourcesmd f doms f && limit_readsf && polls_every_cyclef
=
true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
no_dupsmapb_label b0 :: bs = true ∧ ∃b1 : block bs0 : listblock, b0 :: bs = b1 :: bs0 ∧ existsbλb : block ⇒ memb_labelb1 succ_labelsb_jumpb b0 :: bs = false ∧ ∃E : listname × listfact, pass_exitsstage_sourcesmd f doms f = SomeE

repeat match goal withHb : _ && _ = true |- _⇒apply andb_true_iff in Hb as ? ?end

md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
doms :
nmapZ × Z
H :
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
=
true
H11 :
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
=
true
H10 :
negbextended_crossesf = true
H9 :
no_dupsmapb_label b0 :: bs = true
H8 :
temp_classes_oktemp_defsf = true
H7 :
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs = true
H6 :
proof_class_defsf = true
H5 :
definitions_dominatef doms = true
H4 :
valid_localsf = true
H3 :
forallbvalid_blockmd f temp_defsf b0 :: bs = true
H0 :
evidence_passstage_sourcesmd f doms f = true
H2 :
limit_readsf = true
H1 :
polls_every_cyclef = true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
no_dupsmapb_label b0 :: bs = true ∧ ∃b1 : block bs0 : listblock, b0 :: bs = b1 :: bs0 ∧ existsbλb : block ⇒ memb_labelb1 succ_labelsb_jumpb b0 :: bs = false ∧ ∃E : listname × listfact, pass_exitsstage_sourcesmd f doms f = SomeE

split ; assumption |

md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
doms :
nmapZ × Z
H :
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
=
true
H11 :
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
=
true
H10 :
negbextended_crossesf = true
H9 :
no_dupsmapb_label b0 :: bs = true
H8 :
temp_classes_oktemp_defsf = true
H7 :
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs = true
H6 :
proof_class_defsf = true
H5 :
definitions_dominatef doms = true
H4 :
valid_localsf = true
H3 :
forallbvalid_blockmd f temp_defsf b0 :: bs = true
H0 :
evidence_passstage_sourcesmd f doms f = true
H2 :
limit_readsf = true
H1 :
polls_every_cyclef = true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
∃b1 : block bs0 : listblock, b0 :: bs = b1 :: bs0 ∧ existsbλb : block ⇒ memb_labelb1 succ_labelsb_jumpb b0 :: bs = false ∧ ∃E : listname × listfact, pass_exitsstage_sourcesmd f doms f = SomeE

split

2 open

md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
doms :
nmapZ × Z
H :
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
=
true
H11 :
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
=
true
H10 :
negbextended_crossesf = true
H9 :
no_dupsmapb_label b0 :: bs = true
H8 :
temp_classes_oktemp_defsf = true
H7 :
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs = true
H6 :
proof_class_defsf = true
H5 :
definitions_dominatef doms = true
H4 :
valid_localsf = true
H3 :
forallbvalid_blockmd f temp_defsf b0 :: bs = true
H0 :
evidence_passstage_sourcesmd f doms f = true
H2 :
limit_readsf = true
H1 :
polls_every_cyclef = true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
∃b1 : block bs0 : listblock, b0 :: bs = b1 :: bs0 ∧ existsbλb : block ⇒ memb_labelb1 succ_labelsb_jumpb b0 :: bs = false
focused goal
md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
doms :
nmapZ × Z
H :
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
=
true
H11 :
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
=
true
H10 :
negbextended_crossesf = true
H9 :
no_dupsmapb_label b0 :: bs = true
H8 :
temp_classes_oktemp_defsf = true
H7 :
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs = true
H6 :
proof_class_defsf = true
H5 :
definitions_dominatef doms = true
H4 :
valid_localsf = true
H3 :
forallbvalid_blockmd f temp_defsf b0 :: bs = true
H0 :
evidence_passstage_sourcesmd f doms f = true
H2 :
limit_readsf = true
H1 :
polls_every_cyclef = true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
∃E : listname × listfact, pass_exitsstage_sourcesmd f doms f = SomeE

–exists b0, bs

2 open

md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
doms :
nmapZ × Z
H :
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
=
true
H11 :
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
=
true
H10 :
negbextended_crossesf = true
H9 :
no_dupsmapb_label b0 :: bs = true
H8 :
temp_classes_oktemp_defsf = true
H7 :
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs = true
H6 :
proof_class_defsf = true
H5 :
definitions_dominatef doms = true
H4 :
valid_localsf = true
H3 :
forallbvalid_blockmd f temp_defsf b0 :: bs = true
H0 :
evidence_passstage_sourcesmd f doms f = true
H2 :
limit_readsf = true
H1 :
polls_every_cyclef = true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
b0 :: bs = b0 :: bs ∧ existsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs = false
deferred goal
md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
doms :
nmapZ × Z
H :
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
=
true
H11 :
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
=
true
H10 :
negbextended_crossesf = true
H9 :
no_dupsmapb_label b0 :: bs = true
H8 :
temp_classes_oktemp_defsf = true
H7 :
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs = true
H6 :
proof_class_defsf = true
H5 :
definitions_dominatef doms = true
H4 :
valid_localsf = true
H3 :
forallbvalid_blockmd f temp_defsf b0 :: bs = true
H0 :
evidence_passstage_sourcesmd f doms f = true
H2 :
limit_readsf = true
H1 :
polls_every_cyclef = true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
∃E : listname × listfact, pass_exitsstage_sourcesmd f doms f = SomeE

split ; reflexivity |

2 open

md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
doms :
nmapZ × Z
H :
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
=
true
H11 :
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
=
true
H10 :
negbextended_crossesf = true
H9 :
no_dupsmapb_label b0 :: bs = true
H8 :
temp_classes_oktemp_defsf = true
H7 :
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs = true
H6 :
proof_class_defsf = true
H5 :
definitions_dominatef doms = true
H4 :
valid_localsf = true
H3 :
forallbvalid_blockmd f temp_defsf b0 :: bs = true
H0 :
evidence_passstage_sourcesmd f doms f = true
H2 :
limit_readsf = true
H1 :
polls_every_cyclef = true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
existsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs = false
deferred goal
md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
doms :
nmapZ × Z
H :
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
=
true
H11 :
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
=
true
H10 :
negbextended_crossesf = true
H9 :
no_dupsmapb_label b0 :: bs = true
H8 :
temp_classes_oktemp_defsf = true
H7 :
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs = true
H6 :
proof_class_defsf = true
H5 :
definitions_dominatef doms = true
H4 :
valid_localsf = true
H3 :
forallbvalid_blockmd f temp_defsf b0 :: bs = true
H0 :
evidence_passstage_sourcesmd f doms f = true
H2 :
limit_readsf = true
H1 :
polls_every_cyclef = true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
∃E : listname × listfact, pass_exitsstage_sourcesmd f doms f = SomeE

apply negb_true_iff

2 open

md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
doms :
nmapZ × Z
H :
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
=
true
H11 :
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
=
true
H10 :
negbextended_crossesf = true
H9 :
no_dupsmapb_label b0 :: bs = true
H8 :
temp_classes_oktemp_defsf = true
H7 :
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs = true
H6 :
proof_class_defsf = true
H5 :
definitions_dominatef doms = true
H4 :
valid_localsf = true
H3 :
forallbvalid_blockmd f temp_defsf b0 :: bs = true
H0 :
evidence_passstage_sourcesmd f doms f = true
H2 :
limit_readsf = true
H1 :
polls_every_cyclef = true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs = true
deferred goal
md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
doms :
nmapZ × Z
H :
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
=
true
H11 :
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
=
true
H10 :
negbextended_crossesf = true
H9 :
no_dupsmapb_label b0 :: bs = true
H8 :
temp_classes_oktemp_defsf = true
H7 :
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs = true
H6 :
proof_class_defsf = true
H5 :
definitions_dominatef doms = true
H4 :
valid_localsf = true
H3 :
forallbvalid_blockmd f temp_defsf b0 :: bs = true
H0 :
evidence_passstage_sourcesmd f doms f = true
H2 :
limit_readsf = true
H1 :
polls_every_cyclef = true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
∃E : listname × listfact, pass_exitsstage_sourcesmd f doms f = SomeE

assumption

deferred goal
md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
doms :
nmapZ × Z
H :
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
=
true
H11 :
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
=
true
H10 :
negbextended_crossesf = true
H9 :
no_dupsmapb_label b0 :: bs = true
H8 :
temp_classes_oktemp_defsf = true
H7 :
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs = true
H6 :
proof_class_defsf = true
H5 :
definitions_dominatef doms = true
H4 :
valid_localsf = true
H3 :
forallbvalid_blockmd f temp_defsf b0 :: bs = true
H0 :
evidence_passstage_sourcesmd f doms f = true
H2 :
limit_readsf = true
H1 :
polls_every_cyclef = true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
∃E : listname × listfact, pass_exitsstage_sourcesmd f doms f = SomeE

–match goal withHb : evidence_pass_ _ = true |- _⇒rewrite evidence_pass_exits in Hbend

md :
module
f :
func
b0 :
block
bs :
listblock
Eb :
fn_blocksf = b0 :: bs
doms :
nmapZ × Z
H :
match fn_linkagef with
TAtom"weak" | TAtom"export" | TAtom"local"
⇒
true
_
⇒
false
=
true
H11 :
match fn_retf with
RClassk
⇒
any_classk
RVoid
⇒
true
RTupleks
⇒
Datatypes.lengthks =? 2%nat && forallbλk : class ⇒ existsbclass_eqbk L; P; Single; Double ks
=
true
H10 :
negbextended_crossesf = true
H9 :
no_dupsmapb_label b0 :: bs = true
H8 :
temp_classes_oktemp_defsf = true
H7 :
negbexistsbλb : block ⇒ memb_labelb0 succ_labelsb_jumpb b0 :: bs = true
H6 :
proof_class_defsf = true
H5 :
definitions_dominatef doms = true
H4 :
valid_localsf = true
H3 :
forallbvalid_blockmd f temp_defsf b0 :: bs = true
H0 :
match pass_exitsstage_sourcesmd f doms f with
Some_
⇒
true
None
⇒
false
=
true
H2 :
limit_readsf = true
H1 :
polls_every_cyclef = true
Hc :
module_checkedmd = true
Hin :
InIFuncf md
⊢
∃E : listname × listfact, pass_exitsstage_sourcesmd f doms f = SomeE

destruct pass_exits_ _ ; eauto | discriminate

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
unfold checked_module , valid
intros md f Hv Hc Hin
destruct existsb_ md ; discriminate Hv |
injection Hv as Hv
unfold valid_items in Hv
apply andb_true_iff in Hv as _ Hv
rewrite forallb_forall in Hv
specialize Hv_ Hin
simpl in Hv
unfold valid_func , fn_src in *
destruct fn_blocksf as | b0 bs eqn: Eb ; discriminate Hv |
destruct block_intervalsb0 :: bs as doms | ; | discriminate Hv
rewrite Hc in Hv
unfold stage_func in Hv
cbn [ negb orb ] in Hv
repeat match goal withHb : _ && _ = true |- _⇒apply andb_true_iff in Hb as ? ?end
split ; assumption |
split
–exists b0, bs
split ; reflexivity |
apply negb_true_iff
assumption
–match goal withHb : evidence_pass_ _ = true |- _⇒rewrite evidence_pass_exits in Hbend
destruct pass_exits_ _ ; eauto | discriminate

A local of a frame's starting locals, each object paired with none, has no base: none is allocated yet.

424Lemma lookup_unallocated
∀ x base objs : listname × Z
lookupx mapλxs ⇒ fstxs, @NoneZ objs ≠ SomeSomebase
Explore proof 3 tactics

Initial goal

⊢
∀x : name base : Z objs : listname × Z, lookupx mapλxs : name × Z ⇒ fstxs, None objs ≠ SomeSomebase

intros x base

x :
name
base :
Z
⊢
∀objs : listname × Z, lookupx mapλxs : name × Z ⇒ fstxs, None objs ≠ SomeSomebase

induction objs as | y z objs IH ; simpl ; discriminate |

x :
name
base :
Z
y :
name
z :
Z
objs :
listname × Z
IH :
lookupx mapλxs : name × Z ⇒ fstxs, None objs ≠ SomeSomebase
⊢
name_eqbx y
→
SomeNone
else
lookupx mapλxs : name × Z ⇒ fstxs, None objs
≠
SomeSomebase

destruct name_eqbx y ; discriminate | exact IH

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros x base
induction objs as | y z objs IH ; simpl ; discriminate |
destruct name_eqbx y ; discriminate | exact IH

The pass's own forms

The instruction i is a check_function, the check that a pointer designates a function.

435Definition is_check_functioni : inst : bool ≔
match i with
Let_ F CheckFunction _
⇒
true
_
⇒
false

An instruction the pass treats apart (pass_special) that adds no fact is a check_local or a check_function.

440Lemma pass_special_cases
∀ i
pass_speciali = true
check_facti = None
is_check_locali = true ∨ is_check_functioni = true
Explore proof 3 tactics

Initial goal

⊢
∀i : inst, pass_speciali = true → check_facti = None → is_check_locali = true ∨ is_check_functioni = true

intros i H Hf

i :
inst
H :
pass_speciali = true
Hf :
check_facti = None
⊢
is_check_locali = true ∨ is_check_functioni = true

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

q :
name
k :
class
o :
op
args :
listvalue
H :
pass_specialLetq k o args = true
Hf :
check_factLetq k o args = None
⊢
is_check_localLetq k o args = true ∨ is_check_functionLetq k o args = true

destruct o ; destruct k ; try discriminate H ; try discriminate Hf ; auto ; destruct args as | a1 | a2 | a3 | a4 args ; auto ; discriminate

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros i H Hf
destruct i as q k o args | | | | | | | ; try discriminate H
destruct o ; destruct k ; try discriminate H ; try discriminate Hf ; auto ; destruct args as | a1 | a2 | a3 | a4 args ; auto ; discriminate

An instruction the pass does not rely on facts for is not evidence preserving.

450Lemma relies_preserving
∀ s i
reliess i = false
evidence_preservingi = false
Explore proof 6 tactics

Initial goal

⊢
∀s : src i : inst, reliess i = false → evidence_preservingi = false

unfold relies

⊢
∀ s : src i : inst  ,
evidence_preservingi || is_check_locali || repeated_getters i
||
match raw_accessi with
Some_
⇒
true
None
⇒
false
=
false
→
evidence_preservingi = false

intros s i H

s :
src
i :
inst
H :
evidence_preservingi || is_check_locali || repeated_getters i
||
match raw_accessi with
Some_
⇒
true
None
⇒
false
=
false
⊢
evidence_preservingi = false

apply orb_false_iff in H as H _

s :
src
i :
inst
H :
evidence_preservingi || is_check_locali || repeated_getters i = false
⊢
evidence_preservingi = false

apply orb_false_iff in H as H _

s :
src
i :
inst
H :
evidence_preservingi || is_check_locali = false
⊢
evidence_preservingi = false

apply orb_false_iff in H as H _

s :
src
i :
inst
H :
evidence_preservingi = false
⊢
evidence_preservingi = false

exact H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
unfold relies
intros s i H
apply orb_false_iff in H as H _
apply orb_false_iff in H as H _
apply orb_false_iff in H as H _
exact H

An instruction the pass does not rely on facts for is not a check_local.

458Lemma relies_local
∀ s i
reliess i = false
is_check_locali = false
Explore proof 6 tactics

Initial goal

⊢
∀s : src i : inst, reliess i = false → is_check_locali = false

unfold relies

⊢
∀ s : src i : inst  ,
evidence_preservingi || is_check_locali || repeated_getters i
||
match raw_accessi with
Some_
⇒
true
None
⇒
false
=
false
→
is_check_locali = false

intros s i H

s :
src
i :
inst
H :
evidence_preservingi || is_check_locali || repeated_getters i
||
match raw_accessi with
Some_
⇒
true
None
⇒
false
=
false
⊢
is_check_locali = false

apply orb_false_iff in H as H _

s :
src
i :
inst
H :
evidence_preservingi || is_check_locali || repeated_getters i = false
⊢
is_check_locali = false

apply orb_false_iff in H as H _

s :
src
i :
inst
H :
evidence_preservingi || is_check_locali = false
⊢
is_check_locali = false

apply orb_false_iff in H as _ H

s :
src
i :
inst
H :
is_check_locali = false
⊢
is_check_locali = false

exact H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
unfold relies
intros s i H
apply orb_false_iff in H as H _
apply orb_false_iff in H as H _
apply orb_false_iff in H as _ H
exact H

Where the pass relies on nothing, it goes on to the next instruction with no facts, but after a check_function, which takes the raw call after it too.

467Lemma relies_false_rest
∀ s i rest live rest′ live′
reliess i = false
is_check_functioni = false
checked_inst_rests i rest live = Somerest′, live′
rest′ = rest ∧ live′ = [ ]
Explore proof 14 tactics

Initial goal

⊢
∀s : src i : inst rest : listinst live : listfact rest′ : listinst live′ : listfact, reliess i = false → is_check_functioni = false → checked_inst_rests i rest live = Somerest′, live′ → rest′ = rest ∧ live′ = [ ]

intros s i rest live rest′ live′ Hr Hcf Hc

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
⊢
rest′ = rest ∧ live′ = [ ]

split ; | exact relies_false_ _ _ _ _ _ Hr Hc

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
⊢
rest′ = rest

destruct check_facti as fa | eqn: Hf

2 open

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
fa :
fact
Hf :
check_facti = Somefa
⊢
rest′ = rest
focused goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
⊢
rest′ = rest

{pose proof check_fact_preserving_ _ Hf as Hp

2 open

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
fa :
fact
Hf :
check_facti = Somefa
Hp :
evidence_preservingi = true
⊢
rest′ = rest
deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
⊢
rest′ = rest

rewrite relies_preserving_ _ Hr in Hp

2 open

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
fa :
fact
Hf :
check_facti = Somefa
Hp :
false = true
⊢
rest′ = rest
deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
⊢
rest′ = rest

discriminate Hp

deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
⊢
rest′ = rest

destruct pass_speciali eqn: Hs

2 open

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = true
⊢
rest′ = rest
focused goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
rest′ = rest

–destruct pass_special_cases_ Hs Hf as Hl | Hl

3 open

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = true
Hl :
is_check_locali = true
⊢
rest′ = rest
focused goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = true
Hl :
is_check_functioni = true
⊢
rest′ = rest
deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
rest′ = rest

+rewrite relies_local_ _ Hr in Hl

3 open

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = true
Hl :
false = true
⊢
rest′ = rest
deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = true
Hl :
is_check_functioni = true
⊢
rest′ = rest
deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
rest′ = rest

discriminate Hl

2 open

deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = true
Hl :
is_check_functioni = true
⊢
rest′ = rest
deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
rest′ = rest

+rewrite Hcf in Hl

2 open

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = true
Hl :
false = true
⊢
rest′ = rest
deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
rest′ = rest

discriminate Hl

deferred goal
s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
checked_inst_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
rest′ = rest

–rewrite checked_inst_rest_generic_ _ _ _ Hs in Hc

s :
src
i :
inst
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
Hr :
reliess i = false
Hcf :
is_check_functioni = false
Hc :
generic_rests i rest live = Somerest′, live′
Hf :
check_facti = None
Hs :
pass_speciali = false
⊢
rest′ = rest

exact proj1generic_rest_shape_ _ _ _ _ _ Hc

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros s i rest live rest′ live′ Hr Hcf Hc
split ; | exact relies_false_ _ _ _ _ _ Hr Hc
destruct check_facti as fa | eqn: Hf
{pose proof check_fact_preserving_ _ Hf as Hp
rewrite relies_preserving_ _ Hr in Hp
discriminate Hp
destruct pass_speciali eqn: Hs
–destruct pass_special_cases_ Hs Hf as Hl | Hl
+rewrite relies_local_ _ Hr in Hl
discriminate Hl
+rewrite Hcf in Hl
discriminate Hl
–rewrite checked_inst_rest_generic_ _ _ _ Hs in Hc
exact proj1generic_rest_shape_ _ _ _ _ _ Hc

The pass takes a check_function q together with the raw call through q after it, and goes on with no facts.

484Lemma checked_inst_rest_function_rest
∀ s q args rest live rest′ live′
checked_inst_rests Letq F CheckFunction args rest live = Somerest′, live′
live′ = [ ] ∧ ∃r cargs, rest = RawCallr Tmpq cargs :: rest′
Explore proof 9 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′ = [ ] ∧ ∃r : call_result cargs : listarg, rest = RawCallr Tmpq cargs :: rest′

intros s q args rest live rest′ live′ H

s :
src
q :
name
args :
listvalue
rest :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
checked_inst_rests Letq F CheckFunction args rest live = Somerest′, live′
⊢
live′ = [ ] ∧ ∃r : call_result cargs : listarg, rest = RawCallr Tmpq cargs :: rest′

unfold checked_inst_rest in H

s :
src
q :
name
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′ = [ ] ∧ ∃r : call_result cargs : listarg, rest = RawCallr Tmpq cargs :: rest′

destruct rest as | rest0 ; try discriminate H ; cbn iota beta in H

s :
src
q :
name
args :
listvalue
r :
call_result
callee :
value
args0 :
listarg
rest0 :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
match callee with
Tmpq′
⇒
name_eqbq′ q
→
Somerest0, [ ]
else
None
_
⇒
None
=
Somerest′, live′
⊢
live′ = [ ] ∧ ∃r0 : call_result cargs : listarg, RawCallr callee args0 :: rest0 = RawCallr0 Tmpq cargs :: rest′

destruct callee as q′ | | ; try discriminate H

s :
src
q :
name
args :
listvalue
r :
call_result
q′ :
name
args0 :
listarg
rest0 :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
H :
name_eqbq′ q
→
Somerest0, [ ]
else
None
=
Somerest′, live′
⊢
live′ = [ ] ∧ ∃r0 : call_result cargs : listarg, RawCallr Tmpq′ args0 :: rest0 = RawCallr0 Tmpq cargs :: rest′

destruct name_eqbq′ q eqn: E ; | discriminate H

s :
src
q :
name
args :
listvalue
r :
call_result
q′ :
name
args0 :
listarg
rest0 :
listinst
live :
listfact
rest′ :
listinst
live′ :
listfact
E :
name_eqbq′ q = true
H :
Somerest0, [ ] = Somerest′, live′
⊢
live′ = [ ] ∧ ∃r0 : call_result cargs : listarg, RawCallr Tmpq′ args0 :: rest0 = RawCallr0 Tmpq cargs :: rest′

injection H as ← ←

s :
src
q :
name
args :
listvalue
r :
call_result
q′ :
name
args0 :
listarg
rest0 :
listinst
live :
listfact
E :
name_eqbq′ q = true
⊢
[ ] = [ ] ∧ ∃r0 : call_result cargs : listarg, RawCallr Tmpq′ args0 :: rest0 = RawCallr0 Tmpq cargs :: rest0

apply term_eqb_eq in E

s :
src
q :
name
args :
listvalue
r :
call_result
q′ :
name
args0 :
listarg
rest0 :
listinst
live :
listfact
E :
q′ = q
⊢
[ ] = [ ] ∧ ∃r0 : call_result cargs : listarg, RawCallr Tmpq′ args0 :: rest0 = RawCallr0 Tmpq cargs :: rest0

subst q′

s :
src
q :
name
args :
listvalue
r :
call_result
args0 :
listarg
rest0 :
listinst
live :
listfact
⊢
[ ] = [ ] ∧ ∃r0 : call_result cargs : listarg, RawCallr Tmpq args0 :: rest0 = RawCallr0 Tmpq cargs :: rest0

eauto

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 | rest0 ; try discriminate H ; cbn iota beta in H
destruct callee as q′ | | ; try discriminate H
destruct name_eqbq′ q eqn: E ; | discriminate H
injection H as ← ←
apply term_eqb_eq in E
subst q′
eauto

A raw access is not one of the instructions the pass treats apart.

495Lemma raw_access_not_special
∀ i a
raw_accessi = Somea
pass_speciali = false
Explore proof 3 tactics

Initial goal

⊢
∀i : inst a : name × access_type × Z × rights, raw_accessi = Somea → pass_speciali = false

intros i a H

i :
inst
a :
name × access_type × Z × rights
H :
raw_accessi = Somea
⊢
pass_speciali = false

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

q :
name
k :
class
o :
op
args :
listvalue
a :
name × access_type × Z × rights
H :
raw_accessLetq k o args = Somea
⊢
pass_specialLetq k o args = false

destruct o ; simpl in H ; try discriminate H ; destruct k ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros i a H
destruct i as q k o args | | | | | | | ; try reflexivity
destruct o ; simpl in H ; try discriminate H ; destruct k ; reflexivity

The pass never takes a raw call on its own: only after the check_function of its callee.

503Lemma raw_call_alone
∀ s r cl args rest live
checked_inst_rests RawCallr cl args rest live = None
Explore proof 3 tactics

Initial goal

⊢
∀s : src r : call_result cl : value args : listarg rest : listinst live : listfact, checked_inst_rests RawCallr cl args rest live = None

intros s r cl args rest live

s :
src
r :
call_result
cl :
value
args :
listarg
rest :
listinst
live :
listfact
⊢
checked_inst_rests RawCallr cl args rest live = None

rewrite checked_inst_rest_generic by reflexivity

s :
src
r :
call_result
cl :
value
args :
listarg
rest :
listinst
live :
listfact
⊢
generic_rests RawCallr cl args rest live = None

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros s r cl args rest live
rewrite checked_inst_rest_generic by reflexivity
reflexivity