rocq/theories/Steps.v
What one step of Semantics.v's step does to the running frame, as Campaign 3's run-level invariant (Persistence.v) reads it.
step is one function over every point of a frame; the invariant asks, point by point, what the frame looks like after it: after a variadic callee's snapshot (step_snapshot), at a block's entry (step_enter), at an instruction (step_exec_cons) and at a return (return_step_next). The other lemmas say which instructions allocate, call or keep the locals, and how a doomed frame comes about and stays.
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 Walk
Import ListNotations
Open Scope Z_scope
What a step does to the frame
A function that find_direct finds by the name n among the items of a module is one of its functions.
Explore proof 5 tactics
Initial goal
induction items as | it items IH ; simpl ; intros g H ; discriminate H |
destruct it ; try right ; apply IH ; exact H;match type of H withcontext [if name_eqb n then _ else _]⇒destruct name_eqbx nend;try right ; apply IH ; exact H;try discriminate H
injection H as ←
left
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
A function that find_fn finds by name, directly or through an alias, is a function of the running module.
Explore proof 6 tactics
Initial goal
unfold find_fn
⊢
→
intros ge n g H
destruct find_directn ge_modulege eqn: E
2 openfocused goal
–injection H as →
2 opendeferred goal
eapply find_direct_in ; eauto
deferred goal
–destruct find_aliasn ge_modulege ; eapply find_direct_in ; eauto | discriminate H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold find_fn
intros ge n g H
destruct find_directn ge_modulege eqn: E
–injection H as →
eapply find_direct_in ; eauto
–destruct find_aliasn ge_modulege ; eapply find_direct_in ; eauto | discriminate H
An instruction i that continues (IContinue) keeps the locals l of the frame fr, its invocation's named locals.
Explore proof 4 tactics
Initial goal
intros ge fr m i e l m′ H
destruct i
8 openfocused goal
focused goal
focused goal
focused goal
focused goal
focused goal
1: destruct special_leto eqn: Es ; destruct o ; try discriminate Es | rewrite inst_step_let_ _ _ _ _ _ _ Es in H
11 openge :
fr :
m :
Memory.mem
d :
k :
x :
off, bytes :
Z
r :
align :
Z
args :
listvalue
e :
l :
listname × optionZ
m′ :
Memory.mem
H :
inst_stepge fr m Letd k CheckLocalx off bytes r align args = SomeIContinuee l m′
Es :
special_letCheckLocalx off bytes r align = true
⊢
l = fr_localsfr
focused goal
ge :
fr :
m :
Memory.mem
d :
k :
args :
listvalue
e :
l :
listname × optionZ
m′ :
Memory.mem
H :
inst_stepge fr m Letd k CheckFunction args = SomeIContinuee l m′
Es :
special_letCheckFunction = true
⊢
l = fr_localsfr
focused goal
focused goal
ge :
fr :
m :
Memory.mem
d :
k :
o :
args :
listvalue
e :
l :
listname × optionZ
m′ :
Memory.mem
H :
Es :
special_leto = false
⊢
l = fr_localsfr
focused goal
focused goal
focused goal
focused goal
focused goal
focused goal
all: unfold inst_step , external_call , bind_res , store_out in H ; cases H ; inversion H ; subst ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge fr m i e l m′ H
destruct i
1: destruct special_leto eqn: Es ; destruct o ; try discriminate Es | rewrite inst_step_let_ _ _ _ _ _ _ Es in H
all: unfold inst_step , external_call , bind_res , store_out in H ; cases H ; inversion H ; subst ; reflexivity
Explore proof 2 tactics
Initial goal
intros o k xs m q kont H
destruct o ; unfold op_res , op_res_int , float_integer in H ; cases H ; inversion H ; subst ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros o k xs m q kont H
destruct o ; unfold op_res , op_res_int , float_integer in H ; cases H ; inversion H ; subst ; eauto
Explore proof 17 tactics
Initial goal
⊢
∀ge : genv fr : frame m : Memory.mem i : inst q : alloc_req k : Z → env × listname × optionZ × Memory.mem, inst_stepge fr m i = SomeIFreshq k → ∃d : name c : class al : Z args : listvalue, i = Letd c Allocal args ∧ ∀base : Z, sndfstkbase = fr_localsfr ∨ ∃x : name size : Z, i = LocalAllocx size ∧ ∀base : Z, sndfstkbase = putx Somebase fr_localsfr
intros ge fr m i q k H
ge :
fr :
m :
Memory.mem
i :
q :
destruct i
8 openfocused goal
focused goal
ge :
fr :
m :
Memory.mem
w :
off :
Z
v, a :
q :
focused goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
es :
listeffect
q :
H :
inst_stepge fr m RawStorePointeroff v a es = SomeIFreshq k
⊢
∃d : name c : class al : Z args : listvalue, RawStorePointeroff v a es = Letd c Allocal args ∧ ∀base : Z, sndfstkbase = fr_localsfr ∨ ∃x : name size : Z, RawStorePointeroff v a es = LocalAllocx size ∧ ∀base : Z, sndfstkbase = putx Somebase fr_localsfr
focused goal
focused goal
focused goal
⊢
∃d : name c : class al : Z args : listvalue, LocalAllocx size = Letd c Allocal args ∧ ∀base : Z, sndfstkbase = fr_localsfr ∨ ∃x0 : name size0 : Z, LocalAllocx size = LocalAllocx0 size0 ∧ ∀base : Z, sndfstkbase = putx0 Somebase fr_localsfr
focused goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
q :
1: destruct special_leto eqn: Es ; destruct o ; try discriminate Es | rewrite inst_step_let_ _ _ _ _ _ _ Es in H
11 openge :
fr :
m :
Memory.mem
d :
k0 :
x :
off, bytes :
Z
r :
align :
Z
args :
listvalue
q :
H :
inst_stepge fr m Letd k0 CheckLocalx off bytes r align args = SomeIFreshq k
Es :
special_letCheckLocalx off bytes r align = true
⊢
∃d0 : name c : class al : Z args0 : listvalue, Letd k0 CheckLocalx off bytes r align args = Letd0 c Allocal args0 ∧ ∀base : Z, sndfstkbase = fr_localsfr ∨ ∃x0 : name size : Z, Letd k0 CheckLocalx off bytes r align args = LocalAllocx0 size ∧ ∀base : Z, sndfstkbase = putx0 Somebase fr_localsfr
focused goal
ge :
fr :
m :
Memory.mem
d :
k0 :
args :
listvalue
q :
H :
inst_stepge fr m Letd k0 CheckFunction args = SomeIFreshq k
Es :
special_letCheckFunction = true
⊢
∃d0 : name c : class al : Z args0 : listvalue, Letd k0 CheckFunction args = Letd0 c Allocal args0 ∧ ∀base : Z, sndfstkbase = fr_localsfr ∨ ∃x : name size : Z, Letd k0 CheckFunction args = LocalAllocx size ∧ ∀base : Z, sndfstkbase = putx Somebase fr_localsfr
focused goal
focused goal
focused goal
focused goal
ge :
fr :
m :
Memory.mem
w :
off :
Z
v, a :
q :
focused goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
es :
listeffect
q :
H :
inst_stepge fr m RawStorePointeroff v a es = SomeIFreshq k
⊢
∃d : name c : class al : Z args : listvalue, RawStorePointeroff v a es = Letd c Allocal args ∧ ∀base : Z, sndfstkbase = fr_localsfr ∨ ∃x : name size : Z, RawStorePointeroff v a es = LocalAllocx size ∧ ∀base : Z, sndfstkbase = putx Somebase fr_localsfr
focused goal
focused goal
focused goal
⊢
∃d : name c : class al : Z args : listvalue, LocalAllocx size = Letd c Allocal args ∧ ∀base : Z, sndfstkbase = fr_localsfr ∨ ∃x0 : name size0 : Z, LocalAllocx size = LocalAllocx0 size0 ∧ ∀base : Z, sndfstkbase = putx0 Somebase fr_localsfr
focused goal
ge :
fr :
m :
Memory.mem
file :
line :
Z
q :
all: unfold inst_step , external_call , bind_res , store_out in H ; cases H ; inversion H ; subst
2 openge :
fr :
m :
Memory.mem
d :
k0 :
o :
args :
listvalue
q :
l :
listclass
Heqo0 :
op_arg_classeso k0 = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
k1 :
Z → word × Memory.mem
H :
Es :
special_leto = false
⊢
∨
focused goal
ge :
fr :
m :
Memory.mem
x :
size :
Z
⊢
∃d : name c : class al : Z args : listvalue, LocalAllocx size = Letd c Allocal args ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = fr_localsfr ∨ ∃x0 : name size0 : Z, LocalAllocx size = LocalAllocx0 size0 ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = putx0 Somebase fr_localsfr
–match goal withE : op_res_ _ _ _ = SomeOpAlloc_ _ |- _⇒destruct op_res_alloc_op_ _ _ _ _ _ E as al →end
2 openge :
fr :
m :
Memory.mem
d :
k0 :
args :
listvalue
q :
l :
listclass
al :
Z
Heqo0 :
op_arg_classesAllocal k0 = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
k1 :
Z → word × Memory.mem
H :
Es :
special_letAllocal = false
⊢
∨
deferred goal
ge :
fr :
m :
Memory.mem
x :
size :
Z
⊢
∃d : name c : class al : Z args : listvalue, LocalAllocx size = Letd c Allocal args ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = fr_localsfr ∨ ∃x0 : name size0 : Z, LocalAllocx size = LocalAllocx0 size0 ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = putx0 Somebase fr_localsfr
left
2 openge :
fr :
m :
Memory.mem
d :
k0 :
args :
listvalue
q :
l :
listclass
al :
Z
Heqo0 :
op_arg_classesAllocal k0 = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
k1 :
Z → word × Memory.mem
H :
Es :
special_letAllocal = false
deferred goal
ge :
fr :
m :
Memory.mem
x :
size :
Z
⊢
∃d : name c : class al : Z args : listvalue, LocalAllocx size = Letd c Allocal args ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = fr_localsfr ∨ ∃x0 : name size0 : Z, LocalAllocx size = LocalAllocx0 size0 ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = putx0 Somebase fr_localsfr
eexists ; eexists ; eexists ; eexists
6 openge :
fr :
m :
Memory.mem
d :
k0 :
args :
listvalue
q :
l :
listclass
al :
Z
Heqo0 :
op_arg_classesAllocal k0 = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
k1 :
Z → word × Memory.mem
H :
Es :
special_letAllocal = false
deferred goal
ge :
fr :
m :
Memory.mem
x :
size :
Z
⊢
∃d : name c : class al : Z args : listvalue, LocalAllocx size = Letd c Allocal args ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = fr_localsfr ∨ ∃x0 : name size0 : Z, LocalAllocx size = LocalAllocx0 size0 ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = putx0 Somebase fr_localsfr
shelved goal
ge :
fr :
m :
Memory.mem
d :
k0 :
args :
listvalue
q :
l :
listclass
al :
Z
Heqo0 :
op_arg_classesAllocal k0 = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
k1 :
Z → word × Memory.mem
H :
Es :
special_letAllocal = false
⊢
shelved goal
ge :
fr :
m :
Memory.mem
d :
k0 :
args :
listvalue
q :
l :
listclass
al :
Z
Heqo0 :
op_arg_classesAllocal k0 = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
k1 :
Z → word × Memory.mem
H :
Es :
special_letAllocal = false
shelved goal
ge :
fr :
m :
Memory.mem
d :
k0 :
args :
listvalue
q :
l :
listclass
al :
Z
Heqo0 :
op_arg_classesAllocal k0 = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
k1 :
Z → word × Memory.mem
H :
Es :
special_letAllocal = false
⊢
Z
shelved goal
ge :
fr :
m :
Memory.mem
d :
k0 :
args :
listvalue
q :
l :
listclass
al :
Z
Heqo0 :
op_arg_classesAllocal k0 = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
k1 :
Z → word × Memory.mem
H :
Es :
special_letAllocal = false
⊢
listvalue
split ; reflexivity |
2 openge :
fr :
m :
Memory.mem
d :
k0 :
args :
listvalue
q :
l :
listclass
al :
Z
Heqo0 :
op_arg_classesAllocal k0 = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
k1 :
Z → word × Memory.mem
H :
Es :
special_letAllocal = false
deferred goal
ge :
fr :
m :
Memory.mem
x :
size :
Z
⊢
∃d : name c : class al : Z args : listvalue, LocalAllocx size = Letd c Allocal args ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = fr_localsfr ∨ ∃x0 : name size0 : Z, LocalAllocx size = LocalAllocx0 size0 ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = putx0 Somebase fr_localsfr
intros base
2 openge :
fr :
m :
Memory.mem
d :
k0 :
args :
listvalue
q :
l :
listclass
al :
Z
Heqo0 :
op_arg_classesAllocal k0 = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
k1 :
Z → word × Memory.mem
H :
Es :
special_letAllocal = false
base :
Z
deferred goal
ge :
fr :
m :
Memory.mem
x :
size :
Z
⊢
∃d : name c : class al : Z args : listvalue, LocalAllocx size = Letd c Allocal args ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = fr_localsfr ∨ ∃x0 : name size0 : Z, LocalAllocx size = LocalAllocx0 size0 ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = putx0 Somebase fr_localsfr
simpl
2 openge :
fr :
m :
Memory.mem
d :
k0 :
args :
listvalue
q :
l :
listclass
al :
Z
Heqo0 :
op_arg_classesAllocal k0 = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
k1 :
Z → word × Memory.mem
H :
Es :
special_letAllocal = false
base :
Z
deferred goal
ge :
fr :
m :
Memory.mem
x :
size :
Z
⊢
∃d : name c : class al : Z args : listvalue, LocalAllocx size = Letd c Allocal args ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = fr_localsfr ∨ ∃x0 : name size0 : Z, LocalAllocx size = LocalAllocx0 size0 ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = putx0 Somebase fr_localsfr
match goal with|- sndfstlet _, _ ≔ in _ = _⇒destruct tend
2 openge :
fr :
m :
Memory.mem
d :
k0 :
args :
listvalue
q :
l :
listclass
al :
Z
Heqo0 :
op_arg_classesAllocal k0 = Somel
l0 :
listword
Heqo1 :
map2_optionvalue_xge fr_envfr l args = Somel0
k1 :
Z → word × Memory.mem
H :
Es :
special_letAllocal = false
base :
Z
w :
m0 :
Memory.mem
deferred goal
ge :
fr :
m :
Memory.mem
x :
size :
Z
⊢
∃d : name c : class al : Z args : listvalue, LocalAllocx size = Letd c Allocal args ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = fr_localsfr ∨ ∃x0 : name size0 : Z, LocalAllocx size = LocalAllocx0 size0 ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = putx0 Somebase fr_localsfr
reflexivity
deferred goal
ge :
fr :
m :
Memory.mem
x :
size :
Z
⊢
∃d : name c : class al : Z args : listvalue, LocalAllocx size = Letd c Allocal args ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = fr_localsfr ∨ ∃x0 : name size0 : Z, LocalAllocx size = LocalAllocx0 size0 ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = putx0 Somebase fr_localsfr
–right
ge :
fr :
m :
Memory.mem
x :
size :
Z
⊢
∃x0 : name size0 : Z, LocalAllocx size = LocalAllocx0 size0 ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = putx0 Somebase fr_localsfr
eexists ; eexists
3 openge :
fr :
m :
Memory.mem
x :
size :
Z
⊢
LocalAllocx size = LocalAlloc ∧ ∀base : Z, sndfstfr_envfr, putx Somebase fr_localsfr, allocatedm local_reqsize base = put Somebase fr_localsfr
shelved goal
shelved goal
split ; reflexivity |
ge :
fr :
m :
Memory.mem
x :
size :
Z
intros base
ge :
fr :
m :
Memory.mem
x :
size :
Z
H :
base :
Z
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge fr m i q k H
destruct i
1: destruct special_leto eqn: Es ; destruct o ; try discriminate Es | rewrite inst_step_let_ _ _ _ _ _ _ Es in H
all: unfold inst_step , external_call , bind_res , store_out in H ; cases H ; inversion H ; subst
–match goal withE : op_res_ _ _ _ = SomeOpAlloc_ _ |- _⇒destruct op_res_alloc_op_ _ _ _ _ _ E as al →end
left
eexists ; eexists ; eexists ; eexists
split ; reflexivity |
intros base
simpl
match goal with|- sndfstlet _, _ ≔ in _ = _⇒destruct tend
reflexivity
–right
eexists ; eexists
split ; reflexivity |
intros base
reflexivity
An instruction that calls (ICall) the function g is a call or a raw call, and g is a function of the module.
Explore proof 5 tactics
Initial goal
intros ge fr m i g xs pd H
destruct i
8 openfocused goal
focused goal
focused goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
es :
listeffect
g :
xs :
listword
pd :
H :
inst_stepge fr m RawStorePointeroff v a es = SomeICallg xs pd
⊢
InIFuncg ge_modulege ∧ ∃r : call_result callee : value args : listarg, RawStorePointeroff v a es = Callr callee args ∨ ∃r : call_result callee : value args : listarg, RawStorePointeroff v a es = RawCallr callee args
focused goal
ge :
fr :
m :
Memory.mem
x :
size :
Z
g :
xs :
listword
pd :
H :
inst_stepge fr m LocalAllocx size = SomeICallg xs pd
⊢
InIFuncg ge_modulege ∧ ∃r : call_result callee : value args : listarg, LocalAllocx size = Callr callee args ∨ ∃r : call_result callee : value args : listarg, LocalAllocx size = RawCallr callee args
focused goal
1: destruct special_leto eqn: Es ; destruct o ; try discriminate Es | rewrite inst_step_let_ _ _ _ _ _ _ Es in H
11 openge :
fr :
m :
Memory.mem
d :
k :
x :
off, bytes :
Z
r :
align :
Z
args :
listvalue
g :
xs :
listword
pd :
H :
inst_stepge fr m Letd k CheckLocalx off bytes r align args = SomeICallg xs pd
Es :
special_letCheckLocalx off bytes r align = true
⊢
InIFuncg ge_modulege ∧ ∃r0 : call_result callee : value args0 : listarg, Letd k CheckLocalx off bytes r align args = Callr0 callee args0 ∨ ∃r0 : call_result callee : value args0 : listarg, Letd k CheckLocalx off bytes r align args = RawCallr0 callee args0
focused goal
ge :
fr :
m :
Memory.mem
d :
k :
args :
listvalue
g :
xs :
listword
pd :
H :
inst_stepge fr m Letd k CheckFunction args = SomeICallg xs pd
Es :
special_letCheckFunction = true
⊢
InIFuncg ge_modulege ∧ ∃r : call_result callee : value args0 : listarg, Letd k CheckFunction args = Callr callee args0 ∨ ∃r : call_result callee : value args0 : listarg, Letd k CheckFunction args = RawCallr callee args0
focused goal
focused goal
ge :
fr :
m :
Memory.mem
d :
k :
o :
args :
listvalue
g :
xs :
listword
pd :
H :
Es :
special_leto = false
focused goal
focused goal
focused goal
ge :
fr :
m :
Memory.mem
off :
Z
v, a :
es :
listeffect
g :
xs :
listword
pd :
H :
inst_stepge fr m RawStorePointeroff v a es = SomeICallg xs pd
⊢
InIFuncg ge_modulege ∧ ∃r : call_result callee : value args : listarg, RawStorePointeroff v a es = Callr callee args ∨ ∃r : call_result callee : value args : listarg, RawStorePointeroff v a es = RawCallr callee args
focused goal
ge :
fr :
m :
Memory.mem
x :
size :
Z
g :
xs :
listword
pd :
H :
inst_stepge fr m LocalAllocx size = SomeICallg xs pd
⊢
InIFuncg ge_modulege ∧ ∃r : call_result callee : value args : listarg, LocalAllocx size = Callr callee args ∨ ∃r : call_result callee : value args : listarg, LocalAllocx size = RawCallr callee args
focused goal
all: unfold inst_step , external_call , bind_res , store_out in H ; cases H ; inversion H ; subst
3 openge :
fr :
m :
Memory.mem
r :
args :
listarg
g :
xs :
listword
s :
Heqo :
map_optionarg_xge fr_envfr args = Somexs
focused goal
ge :
fr :
m :
Memory.mem
r :
callee :
args :
listarg
g :
p :
l :
listword
Heqo0 :
map_optionarg_xge fr_envfr args = Somel
r0 :
resunit
Heqo1 :
function_check_resge p = Somer0
x :
unit
f :
ys :
listword
H :
Heqb :
variadic_funcg = true
Heqo3 :
indirect_call_convg r args l = SomeConvertedys words
focused goal
ge :
fr :
m :
Memory.mem
r :
callee :
args :
listarg
g :
p :
l :
listword
Heqo0 :
map_optionarg_xge fr_envfr args = Somel
r0 :
resunit
Heqo1 :
function_check_resge p = Somer0
x :
unit
f :
ys :
listword
H :
Heqb :
variadic_funcg = false
Heqo3 :
indirect_call_convg r args l = SomeConvertedys words
all: split ; eapply find_fn_in ; eassumption | eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge fr m i g xs pd H
destruct i
1: destruct special_leto eqn: Es ; destruct o ; try discriminate Es | rewrite inst_step_let_ _ _ _ _ _ _ Es in H
all: unfold inst_step , external_call , bind_res , store_out in H ; cases H ; inversion H ; subst
all: split ; eapply find_fn_in ; eassumption | eauto
The evidence pass keeps no facts before a call (relies).
Explore proof 1 tactics
The pass keeps no facts before a raw call.
Explore proof 1 tactics
The pass keeps no facts before an alloc.
Explore proof 2 tactics
Source script
intros s d c al args
destruct c ; reflexivity
The pass keeps no facts before a named local's allocation.
∀ s x size
reliess LocalAllocx size = false
Explore proof 1 tactics
Initial goal
⊢
∀s : src x : name size : Z, reliess LocalAllocx size = false
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
reflexivity
The pass keeps its facts before every ahead-transparent instruction, one that may come between a check_ahead and its access.
Explore proof 5 tactics
Initial goal
⊢
∀s : src i : inst, ahead_transparenti = true → reliess i = true
unfold ahead_transparent , relies
⊢
intros s i H
s :
i :
⊢
apply andb_true_iff in H as H _
⊢
rewrite H
⊢
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
As doomed_result/5 in a frame fr that is not doomed: the result od is the instruction's result out as it is, or, for a doomed check_ahead, one that goes on with its pointer and dooms the frame.
∀ ge fr m i out od
fr_doomedfr = None
doomed_resultge fr m i out = Someod
Explore proof 12 tactics
Initial goal
intros ge fr m i out od Hd H
destruct ahead_insti eqn: Ea
2 openge :
fr :
m :
Memory.mem
i :
out :
Hd :
fr_doomedfr = None
H :
doomed_resultge fr m i out = Someod
Ea :
ahead_insti = true
–destruct i as d k o args | | | | | | | ; try discriminate Ea
2 openge :
fr :
m :
Memory.mem
d :
k :
o :
args :
listvalue
out :
Hd :
fr_doomedfr = None
H :
doomed_resultge fr m Letd k o args out = Someod
Ea :
ahead_instLetd k o args = true
destruct k ; try discriminate Ea
2 openge :
fr :
m :
Memory.mem
d :
o :
args :
listvalue
out :
Hd :
fr_doomedfr = None
H :
doomed_resultge fr m Letd A o args out = Someod
Ea :
ahead_instLetd A o args = true
destruct o ; try discriminate Ea
2 openge :
fr :
m :
Memory.mem
d :
lo, hi :
Z
r :
align, ahi :
Z
args :
listvalue
out :
Hd :
fr_doomedfr = None
H :
doomed_resultge fr m Letd A CheckAheadlo hi r align ahi args out = Someod
Ea :
ahead_instLetd A CheckAheadlo hi r align ahi args = true
destruct args as | v | v′ args ; try discriminate Ea
2 openge :
fr :
m :
Memory.mem
d :
lo, hi :
Z
r :
align, ahi :
Z
v :
out :
Hd :
fr_doomedfr = None
H :
doomed_resultge fr m Letd A CheckAheadlo hi r align ahi v out = Someod
Ea :
ahead_instLetd A CheckAheadlo hi r align ahi v = true
unfold doomed_result in H
2 openge :
fr :
m :
Memory.mem
d :
lo, hi :
Z
r :
align, ahi :
Z
v :
out :
Hd :
fr_doomedfr = None
H :
match out with
⇒
⇒
=
Someod
Ea :
ahead_instLetd A CheckAheadlo hi r align ahi v = true
rewrite Hd in H
2 openge :
fr :
m :
Memory.mem
d :
lo, hi :
Z
r :
align, ahi :
Z
v :
out :
Hd :
fr_doomedfr = None
H :
Ea :
ahead_instLetd A CheckAheadlo hi r align ahi v = true
cases H ; inversion H ; subst ; eauto
–rewrite doomed_result_other_ _ _ _ _ Ea in H
rewrite Hd in H
cases H ; inversion H ; subst ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge fr m i out od Hd H
destruct ahead_insti eqn: Ea
–destruct i as d k o args | | | | | | | ; try discriminate Ea
destruct k ; try discriminate Ea
destruct o ; try discriminate Ea
destruct args as | v | v′ args ; try discriminate Ea
unfold doomed_result in H
rewrite Hd in H
cases H ; inversion H ; subst ; eauto
In a doomed frame, doomed_result/5 keeps it doomed, and the result is the instruction's own, a check_ahead that goes on, or an outcome.
∀ ge fr m i out od
fr_doomedfr ≠ None
doomed_resultge fr m i out = Someod
Explore proof 13 tactics
Initial goal
intros ge fr m i out od Hd H
destruct fr_doomedfr as w0 | eqn: Ew ; | congruence
destruct ahead_insti eqn: Ea
2 openge :
fr :
m :
Memory.mem
i :
out :
w0 :
Ew :
fr_doomedfr = Somew0
Hd :
Somew0 ≠ None
H :
doomed_resultge fr m i out = Someod
Ea :
ahead_insti = true
focused goal
–destruct i as d k o args | | | | | | | ; try discriminate Ea
2 openge :
fr :
m :
Memory.mem
d :
k :
o :
args :
listvalue
out :
w0 :
Ew :
fr_doomedfr = Somew0
Hd :
Somew0 ≠ None
H :
doomed_resultge fr m Letd k o args out = Someod
Ea :
ahead_instLetd k o args = true
deferred goal
destruct k ; try discriminate Ea
2 openge :
fr :
m :
Memory.mem
d :
o :
args :
listvalue
out :
w0 :
Ew :
fr_doomedfr = Somew0
Hd :
Somew0 ≠ None
H :
doomed_resultge fr m Letd A o args out = Someod
Ea :
ahead_instLetd A o args = true
deferred goal
destruct o ; try discriminate Ea
2 openge :
fr :
m :
Memory.mem
d :
lo, hi :
Z
r :
align, ahi :
Z
args :
listvalue
out :
w0 :
Ew :
fr_doomedfr = Somew0
Hd :
Somew0 ≠ None
H :
doomed_resultge fr m Letd A CheckAheadlo hi r align ahi args out = Someod
Ea :
ahead_instLetd A CheckAheadlo hi r align ahi args = true
deferred goal
destruct args as | v | v′ args ; try discriminate Ea
2 openge :
fr :
m :
Memory.mem
d :
lo, hi :
Z
r :
align, ahi :
Z
v :
out :
w0 :
Ew :
fr_doomedfr = Somew0
Hd :
Somew0 ≠ None
H :
doomed_resultge fr m Letd A CheckAheadlo hi r align ahi v out = Someod
Ea :
ahead_instLetd A CheckAheadlo hi r align ahi v = true
deferred goal
unfold doomed_result in H
2 openge :
fr :
m :
Memory.mem
d :
lo, hi :
Z
r :
align, ahi :
Z
v :
out :
w0 :
Ew :
fr_doomedfr = Somew0
Hd :
Somew0 ≠ None
H :
match out with
⇒
⇒
=
Someod
Ea :
ahead_instLetd A CheckAheadlo hi r align ahi v = true
deferred goal
rewrite Ew in H
2 openge :
fr :
m :
Memory.mem
d :
lo, hi :
Z
r :
align, ahi :
Z
v :
out :
w0 :
Ew :
fr_doomedfr = Somew0
Hd :
Somew0 ≠ None
H :
match out with
⇒
IStopUncheckedNullCapability IStopUncheckedOutOfBounds IStopUncheckedMisaligned IStopUncheckedReadonly IStopUncheckedNotAFunction IStopUncheckedArgumentSize IStopUncheckedReturnSize IStopUncheckedInvalidFree IStopUncheckedDoubleFree IStopUncheckedTooBig IStopUncheckedOutOfMemory IStopUncheckedSpan IStopUncheckedHalf IStopUncheckedEarly_ IStopUncheckedAhead_
⇒
_
⇒
Someout, Somew0
=
Someod
Ea :
ahead_instLetd A CheckAheadlo hi r align ahi v = true
deferred goal
cases H ; inversion H ; subst ; simpl ; split ; discriminate | eauto
deferred goal
–rewrite doomed_result_other_ _ _ _ _ Ea in H
ge :
fr :
m :
Memory.mem
i :
out :
w0 :
Ew :
fr_doomedfr = Somew0
Hd :
Somew0 ≠ None
H :
Ea :
ahead_insti = false
rewrite Ew in H
ge :
fr :
m :
Memory.mem
i :
out :
w0 :
Ew :
fr_doomedfr = Somew0
Hd :
Somew0 ≠ None
H :
Ea :
ahead_insti = false
cases H ; inversion H ; subst ; simpl ; split ; discriminate | eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge fr m i out od Hd H
destruct fr_doomedfr as w0 | eqn: Ew ; | congruence
destruct ahead_insti eqn: Ea
–destruct i as d k o args | | | | | | | ; try discriminate Ea
destruct k ; try discriminate Ea
destruct o ; try discriminate Ea
destruct args as | v | v′ args ; try discriminate Ea
unfold doomed_result in H
rewrite Ew in H
cases H ; inversion H ; subst ; simpl ; split ; discriminate | eauto
–rewrite doomed_result_other_ _ _ _ _ Ea in H
rewrite Ew in H
cases H ; inversion H ; subst ; simpl ; split ; discriminate | eauto
The next configuration after an instruction's result that is not an outcome: the same frame, at the instructions rest, with the new environment, locals and memory of a result that continues, or the callee's frame on top of the caller's, waiting at rest, for a call.
∀ c l rest j out d c′
∃e1 l1 m1, out = IContinuee1 l1 m1 ∧ c′ = mkConfigmkFramefr_fnc_framec e1 l1 d Execl rest j c_callersc m1 c_fuelc ∨ ∃g xs pd callee, out = ICallg xs pd ∧ call_frameg xs = Somecallee ∧ c′ = mkConfigcallee mkFramefr_fnc_framec fr_envc_framec fr_localsc_framec d Execl rest j, pd :: c_callersc c_memc c_fuelc
Explore proof 10 tactics
Initial goal
⊢
∀c : config l : name rest : listinst j : jump out : inst_out d : optionreason c′ : config, inst_nextc l rest j out d = Nextc′ → ∃e1 : env l1 : listname × optionZ m1 : Memory.mem, out = IContinuee1 l1 m1 ∧ c′ = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e1; fr_locals ≔ l1; fr_doomed ≔ d; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m1; c_fuel ≔ c_fuelc ∨ ∃g : func xs : listword pd : pending callee : frame, out = ICallg xs pd ∧ call_frameg xs = Somecallee ∧ c′ = c_frame ≔ callee; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ d; fr_at ≔ Execl rest j, pd :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc
unfold inst_next
⊢
→
∃e1 : env l1 : listname × optionZ m1 : Memory.mem, out = IContinuee1 l1 m1 ∧ c′ = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e1; fr_locals ≔ l1; fr_doomed ≔ d; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m1; c_fuel ≔ c_fuelc ∨ ∃g : func xs : listword pd : pending callee : frame, out = ICallg xs pd ∧ call_frameg xs = Somecallee ∧ c′ = c_frame ≔ callee; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ d; fr_at ≔ Execl rest j, pd :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc
intros c l rest j out d c′ H
c :
l :
rest :
listinst
j :
out :
d :
optionreason
c′ :
⊢
∃e1 : env l1 : listname × optionZ m1 : Memory.mem, out = IContinuee1 l1 m1 ∧ c′ = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e1; fr_locals ≔ l1; fr_doomed ≔ d; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m1; c_fuel ≔ c_fuelc ∨ ∃g : func xs : listword pd : pending callee : frame, out = ICallg xs pd ∧ call_frameg xs = Somecallee ∧ c′ = c_frame ≔ callee; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ d; fr_at ≔ Execl rest j, pd :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc
destruct out ; try discriminate H
2 open⊢
∃e1 : env l1 : listname × optionZ m1 : Memory.mem, IContinuee locals m = IContinuee1 l1 m1 ∧ c′ = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e1; fr_locals ≔ l1; fr_doomed ≔ d; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m1; c_fuel ≔ c_fuelc ∨ ∃g : func xs : listword pd : pending callee : frame, IContinuee locals m = ICallg xs pd ∧ call_frameg xs = Somecallee ∧ c′ = c_frame ≔ callee; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ d; fr_at ≔ Execl rest j, pd :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc
focused goal
⊢
∃e1 : env l1 : listname × optionZ m1 : Memory.mem, ICallf xs pd = IContinuee1 l1 m1 ∧ c′ = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e1; fr_locals ≔ l1; fr_doomed ≔ d; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m1; c_fuel ≔ c_fuelc ∨ ∃g : func xs0 : listword pd0 : pending callee : frame, ICallf xs pd = ICallg xs0 pd0 ∧ call_frameg xs0 = Somecallee ∧ c′ = c_frame ≔ callee; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ d; fr_at ≔ Execl rest j, pd0 :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc
–injection H as ←
2 open⊢
∃e1 : env l1 : listname × optionZ m1 : Memory.mem, IContinuee locals m = IContinuee1 l1 m1 ∧ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ d; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m; c_fuel ≔ c_fuelc = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e1; fr_locals ≔ l1; fr_doomed ≔ d; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m1; c_fuel ≔ c_fuelc ∨ ∃g : func xs : listword pd : pending callee : frame, IContinuee locals m = ICallg xs pd ∧ call_frameg xs = Somecallee ∧ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ d; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m; c_fuel ≔ c_fuelc = c_frame ≔ callee; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ d; fr_at ≔ Execl rest j, pd :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc
deferred goal
⊢
∃e1 : env l1 : listname × optionZ m1 : Memory.mem, ICallf xs pd = IContinuee1 l1 m1 ∧ c′ = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e1; fr_locals ≔ l1; fr_doomed ≔ d; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m1; c_fuel ≔ c_fuelc ∨ ∃g : func xs0 : listword pd0 : pending callee : frame, ICallf xs pd = ICallg xs0 pd0 ∧ call_frameg xs0 = Somecallee ∧ c′ = c_frame ≔ callee; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ d; fr_at ≔ Execl rest j, pd0 :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc
left
2 open⊢
∃e1 : env l1 : listname × optionZ m1 : Memory.mem, IContinuee locals m = IContinuee1 l1 m1 ∧ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ locals; fr_doomed ≔ d; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m; c_fuel ≔ c_fuelc = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e1; fr_locals ≔ l1; fr_doomed ≔ d; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m1; c_fuel ≔ c_fuelc
deferred goal
⊢
∃e1 : env l1 : listname × optionZ m1 : Memory.mem, ICallf xs pd = IContinuee1 l1 m1 ∧ c′ = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e1; fr_locals ≔ l1; fr_doomed ≔ d; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m1; c_fuel ≔ c_fuelc ∨ ∃g : func xs0 : listword pd0 : pending callee : frame, ICallf xs pd = ICallg xs0 pd0 ∧ call_frameg xs0 = Somecallee ∧ c′ = c_frame ≔ callee; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ d; fr_at ≔ Execl rest j, pd0 :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc
eauto
deferred goal
⊢
∃e1 : env l1 : listname × optionZ m1 : Memory.mem, ICallf xs pd = IContinuee1 l1 m1 ∧ c′ = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e1; fr_locals ≔ l1; fr_doomed ≔ d; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m1; c_fuel ≔ c_fuelc ∨ ∃g : func xs0 : listword pd0 : pending callee : frame, ICallf xs pd = ICallg xs0 pd0 ∧ call_frameg xs0 = Somecallee ∧ c′ = c_frame ≔ callee; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ d; fr_at ≔ Execl rest j, pd0 :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc
–destruct call_framef xs eqn: E ; | discriminate H
⊢
∃e1 : env l1 : listname × optionZ m1 : Memory.mem, ICallf xs pd = IContinuee1 l1 m1 ∧ c′ = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e1; fr_locals ≔ l1; fr_doomed ≔ d; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m1; c_fuel ≔ c_fuelc ∨ ∃g : func xs0 : listword pd0 : pending callee : frame, ICallf xs pd = ICallg xs0 pd0 ∧ call_frameg xs0 = Somecallee ∧ c′ = c_frame ≔ callee; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ d; fr_at ≔ Execl rest j, pd0 :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc
injection H as ←
⊢
∃e1 : env l1 : listname × optionZ m1 : Memory.mem, ICallf xs pd = IContinuee1 l1 m1 ∧ c_frame ≔ f0; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ d; fr_at ≔ Execl rest j, pd :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e1; fr_locals ≔ l1; fr_doomed ≔ d; fr_at ≔ Execl rest j; c_callers ≔ c_callersc; c_mem ≔ m1; c_fuel ≔ c_fuelc ∨ ∃g : func xs0 : listword pd0 : pending callee : frame, ICallf xs pd = ICallg xs0 pd0 ∧ call_frameg xs0 = Somecallee ∧ c_frame ≔ f0; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ d; fr_at ≔ Execl rest j, pd :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc = c_frame ≔ callee; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ d; fr_at ≔ Execl rest j, pd0 :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc
right
⊢
∃g : func xs0 : listword pd0 : pending callee : frame, ICallf xs pd = ICallg xs0 pd0 ∧ call_frameg xs0 = Somecallee ∧ c_frame ≔ f0; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ d; fr_at ≔ Execl rest j, pd :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc = c_frame ≔ callee; c_callers ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ d; fr_at ≔ Execl rest j, pd0 :: c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc
eauto 7
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold inst_next
intros c l rest j out d c′ H
destruct out ; try discriminate H
–injection H as ←
left
eauto
After a result that allocates, the next configuration for each base the object can get is the same frame, at the instructions rest, with what the instruction makes of that base.
Explore proof 8 tactics
Initial goal
unfold inst_next
intros c l rest j out d q k H
destruct out ; try discriminate H;
injection H as ← ←
eexists
2 opensplit ; reflexivity |
intros base
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold inst_next
intros c l rest j out d q k H
destruct out ; try discriminate H;
injection H as ← ←
eexists
split ; reflexivity |
intros base
reflexivity
A step at the instruction i that neither ends the run nor gets stuck runs in a frame that is not doomed or at an ahead-transparent i, and is inst_step, then doomed_result/5, then inst_next.
Explore proof 15 tactics
Initial goal
⊢
∀ge : genv c : config l : name i : inst rest : listinst j : jump r : step_result, fr_atc_framec = Execl i :: rest j → stepge c = r → ∀o : outcome, r ≠ Doneo → ∀why : string, r ≠ Stuckwhy → fr_doomedc_framec = None ∨ ahead_transparenti = true ∧ ∃out0 : inst_out od : inst_out × optionreason, inst_stepge c_framec c_memc i = Someout0 ∧ doomed_resultge c_framec c_memc i out0 = Someod ∧ inst_nextc l rest j fstod sndod = r
intros ge c l i rest j r Ha Hs Hd Hst
unfold step in Hs
ge :
c :
l :
i :
rest :
listinst
j :
r :
Hs :
Snapshot[ ] l
⇒
Snapshot_ :: _ as xs l
⇒
else
Freshheap_req16 8 × Z.of_natDatatypes.lengthxs λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesxs base allocatedc_memc heap_req16 8 × Z.of_natDatatypes.lengthxs base; c_fuel ≔ c_fuelc
=
r
rewrite Ha in Hs
destruct fr_doomedc_framec as w | eqn: Ew
2 openfocused goal
–destruct ahead_transparenti eqn: Et ; | subst r ; exfalso ; eapply Hd ; reflexivity
2 opendeferred goal
split ; right ; reflexivity |
2 opendeferred goal
destruct inst_stepge c_framec c_memc i as out0 | eqn: Ei ; | subst r ; exfalso ; eapply Hst ; reflexivity
2 openge :
c :
l :
i :
rest :
listinst
j :
r :
w :
Et :
ahead_transparenti = true
out0 :
deferred goal
destruct doomed_resultge c_framec c_memc i out0 as od | eqn: Eo ; | subst r ; exfalso ; eapply Hst ; reflexivity
2 openge :
c :
l :
i :
rest :
listinst
j :
r :
w :
Et :
ahead_transparenti = true
out0 :
Eo :
doomed_resultge c_framec c_memc i out0 = Someod
deferred goal
exists out0, od
2 openge :
c :
l :
i :
rest :
listinst
j :
r :
w :
Et :
ahead_transparenti = true
out0 :
Eo :
doomed_resultge c_framec c_memc i out0 = Someod
⊢
Someout0 = Someout0 ∧ doomed_resultge c_framec c_memc i out0 = Someod ∧ inst_nextc l rest j fstod sndod = r
deferred goal
split ; first exact Ei | reflexivity | split ; first exact Eo | reflexivity | exact Hs
deferred goal
–split ; left ; reflexivity |
destruct inst_stepge c_framec c_memc i as out0 | eqn: Ei ; | subst r ; exfalso ; eapply Hst ; reflexivity
destruct doomed_resultge c_framec c_memc i out0 as od | eqn: Eo ; | subst r ; exfalso ; eapply Hst ; reflexivity
exists out0, od
⊢
Someout0 = Someout0 ∧ doomed_resultge c_framec c_memc i out0 = Someod ∧ inst_nextc l rest j fstod sndod = r
split ; first exact Ei | reflexivity | split ; first exact Eo | reflexivity | exact Hs
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge c l i rest j r Ha Hs Hd Hst
unfold step in Hs
rewrite Ha in Hs
–destruct ahead_transparenti eqn: Et ; | subst r ; exfalso ; eapply Hd ; reflexivity
split ; right ; reflexivity |
destruct inst_stepge c_framec c_memc i as out0 | eqn: Ei ; | subst r ; exfalso ; eapply Hst ; reflexivity
destruct doomed_resultge c_framec c_memc i out0 as od | eqn: Eo ; | subst r ; exfalso ; eapply Hst ; reflexivity
exists out0, od
split ; first exact Ei | reflexivity | split ; first exact Eo | reflexivity | exact Hs
–split ; left ; reflexivity |
destruct inst_stepge c_framec c_memc i as out0 | eqn: Ei ; | subst r ; exfalso ; eapply Hst ; reflexivity
destruct doomed_resultge c_framec c_memc i out0 as od | eqn: Eo ; | subst r ; exfalso ; eapply Hst ; reflexivity
exists out0, od
split ; first exact Ei | reflexivity | split ; first exact Eo | reflexivity | exact Hs
Explore proof 9 tactics
Initial goal
⊢
∀ge : genv c : config l : name from : optionname c′ : config, fr_atc_framec = Enterl from → stepge c = Nextc′ → ∃b : block e : env, find_blockl fn_blocksfr_fnc_framec = Someb ∧ phis_envge b_phisb from fr_envc_framec = Somee ∧ c′ = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc − 1
intros ge c l from c′ Ha H
⊢
∃b : block e : env, find_blockl fn_blocksfr_fnc_framec = Someb ∧ phis_envge b_phisb from fr_envc_framec = Somee ∧ c′ = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc − 1
unfold step in H
ge :
c :
l :
from :
optionname
c′ :
H :
Snapshot[ ] l
⇒
Snapshot_ :: _ as xs l
⇒
else
Freshheap_req16 8 × Z.of_natDatatypes.lengthxs λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesxs base allocatedc_memc heap_req16 8 × Z.of_natDatatypes.lengthxs base; c_fuel ≔ c_fuelc
=
Nextc′
⊢
∃b : block e : env, find_blockl fn_blocksfr_fnc_framec = Someb ∧ phis_envge b_phisb from fr_envc_framec = Somee ∧ c′ = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc − 1
rewrite Ha in H
⊢
∃b : block e : env, find_blockl fn_blocksfr_fnc_framec = Someb ∧ phis_envge b_phisb from fr_envc_framec = Somee ∧ c′ = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc − 1
destruct c_fuelc =? 0 ; discriminate H |
⊢
∃b : block e : env, find_blockl fn_blocksfr_fnc_framec = Someb ∧ phis_envge b_phisb from fr_envc_framec = Somee ∧ c′ = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc − 1
apply or_stuck_next in H
⊢
∃b : block e : env, find_blockl fn_blocksfr_fnc_framec = Someb ∧ phis_envge b_phisb from fr_envc_framec = Somee ∧ c′ = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc − 1
destruct find_block_ _ as b | ; | discriminate H
destruct phis_envge b_phisb from fr_envc_framec as e | eqn: Ep ; | discriminate H
injection H as ←
⊢
∃b0 : block e0 : env, Someb = Someb0 ∧ phis_envge b_phisb0 from fr_envc_framec = Somee0 ∧ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc − 1 = c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e0; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Execl b_instsb0 b_jumpb0; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc − 1
eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge c l from c′ Ha H
unfold step in H
rewrite Ha in H
destruct c_fuelc =? 0 ; discriminate H |
apply or_stuck_next in H
destruct find_block_ _ as b | ; | discriminate H
injection H as ←
eauto
Entering a block never allocates.
Explore proof 9 tactics
Initial goal
intros ge c l from q k Ha H
unfold step in H
ge :
c :
l :
from :
optionname
q :
k :
Z → config
H :
Snapshot[ ] l
⇒
Snapshot_ :: _ as xs l
⇒
else
Freshheap_req16 8 × Z.of_natDatatypes.lengthxs λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesxs base allocatedc_memc heap_req16 8 × Z.of_natDatatypes.lengthxs base; c_fuel ≔ c_fuelc
=
Freshq k
⊢
False
rewrite Ha in H
destruct c_fuelc =? 0 ; discriminate H |
apply or_stuck_fresh in H
destruct find_block_ _ as b | ; simpl in H ; | discriminate H
unfold phis_env in H
destruct from ; | destruct b_phisb ; simpl in H ; try discriminate H
destruct fold_left_ _ _ ; discriminate H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge c l from q k Ha H
unfold step in H
rewrite Ha in H
destruct c_fuelc =? 0 ; discriminate H |
apply or_stuck_fresh in H
destruct find_block_ _ as b | ; simpl in H ; | discriminate H
unfold phis_env in H
destruct from ; | destruct b_phisb ; simpl in H ; try discriminate H
destruct fold_left_ _ _ ; discriminate H
A variadic callee's snapshot of its arguments xs enters the entry block l, with the same callers, function, locals and doom.
Explore proof 5 tactics
Initial goal
intros ge c xs l c′ Ha H
unfold step in H
ge :
c :
xs :
listword
l :
c′ :
H :
Snapshot[ ] l
⇒
Snapshot_ :: _ as xs l
⇒
else
Freshheap_req16 8 × Z.of_natDatatypes.lengthxs λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesxs base allocatedc_memc heap_req16 8 × Z.of_natDatatypes.lengthxs base; c_fuel ≔ c_fuelc
=
Nextc′
rewrite Ha in H
ge :
c :
xs :
listword
l :
c′ :
H :
match xs with
[ ]
⇒
_ :: _
⇒
else
Freshheap_req16 8 × Z.of_natDatatypes.lengthxs λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesxs base allocatedc_memc heap_req16 8 × Z.of_natDatatypes.lengthxs base; c_fuel ≔ c_fuelc
=
Nextc′
destruct xs ; injection H as ← ; simpl ; auto |
ge :
c :
w :
xs :
listword
l :
c′ :
H :
else
Freshheap_req16 8 × Z.of_natDatatypes.lengthw :: xs λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesw :: xs base allocatedc_memc heap_req16 8 × Z.of_natDatatypes.lengthw :: xs base; c_fuel ≔ c_fuelc
=
Nextc′
destruct negb_ ; discriminate H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge c xs l c′ Ha H
unfold step in H
rewrite Ha in H
destruct xs ; injection H as ← ; simpl ; auto |
destruct negb_ ; discriminate H
Where a snapshot allocates, it enters the entry block l with the same callers, function, locals and doom, whatever base the object gets.
Explore proof 8 tactics
Initial goal
⊢
∀ge : genv c : config xs : listword l : name q : alloc_req k : Z → config, fr_atc_framec = Snapshotxs l → stepge c = Freshq k → ∀base : Z, c_callerskbase = c_callersc ∧ fr_fnc_framekbase = fr_fnc_framec ∧ fr_localsc_framekbase = fr_localsc_framec ∧ fr_doomedc_framekbase = fr_doomedc_framec ∧ fr_atc_framekbase = Enterl None
intros ge c xs l q k Ha H base
unfold step in H
ge :
c :
xs :
listword
l :
q :
k :
Z → config
H :
Snapshot[ ] l
⇒
Snapshot_ :: _ as xs l
⇒
else
Freshheap_req16 8 × Z.of_natDatatypes.lengthxs λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesxs base allocatedc_memc heap_req16 8 × Z.of_natDatatypes.lengthxs base; c_fuel ≔ c_fuelc
=
Freshq k
base :
Z
rewrite Ha in H
ge :
c :
xs :
listword
l :
q :
k :
Z → config
H :
match xs with
[ ]
⇒
_ :: _
⇒
else
Freshheap_req16 8 × Z.of_natDatatypes.lengthxs λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesxs base allocatedc_memc heap_req16 8 × Z.of_natDatatypes.lengthxs base; c_fuel ≔ c_fuelc
=
Freshq k
base :
Z
destruct xs ; discriminate H |
ge :
c :
w :
xs :
listword
l :
q :
k :
Z → config
H :
else
Freshheap_req16 8 × Z.of_natDatatypes.lengthw :: xs λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesw :: xs base allocatedc_memc heap_req16 8 × Z.of_natDatatypes.lengthw :: xs base; c_fuel ≔ c_fuelc
=
Freshq k
base :
Z
destruct negb_ ; discriminate H |
ge :
c :
w :
xs :
listword
l :
q :
k :
Z → config
H :
Freshheap_req16 8 × Z.of_natDatatypes.lengthw :: xs λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesw :: xs base allocatedc_memc heap_req16 8 × Z.of_natDatatypes.lengthw :: xs base; c_fuel ≔ c_fuelc = Freshq k
base :
Z
injection H as _ ←
⊢
c_callersc_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ match w with WIntn ⇒ snapshot_valuesxs base + 8 store_bytesallocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 base base 8 n WPtrp ⇒ snapshot_valuesxs base + 8 store_auxstore_bytesallocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 base base 8 ptr_addrp base ptr_capp WLimit_ _ ⇒ snapshot_valuesxs base + 8 allocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 base end; c_fuel ≔ c_fuelc = c_callersc ∧ fr_fnc_framec_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ match w with WIntn ⇒ snapshot_valuesxs base + 8 store_bytesallocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 base base 8 n WPtrp ⇒ snapshot_valuesxs base + 8 store_auxstore_bytesallocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 base base 8 ptr_addrp base ptr_capp WLimit_ _ ⇒ snapshot_valuesxs base + 8 allocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 base end; c_fuel ≔ c_fuelc = fr_fnc_framec ∧ fr_localsc_framec_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ match w with WIntn ⇒ snapshot_valuesxs base + 8 store_bytesallocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 base base 8 n WPtrp ⇒ snapshot_valuesxs base + 8 store_auxstore_bytesallocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 base base 8 ptr_addrp base ptr_capp WLimit_ _ ⇒ snapshot_valuesxs base + 8 allocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 base end; c_fuel ≔ c_fuelc = fr_localsc_framec ∧ fr_doomedc_framec_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ match w with WIntn ⇒ snapshot_valuesxs base + 8 store_bytesallocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 base base 8 n WPtrp ⇒ snapshot_valuesxs base + 8 store_auxstore_bytesallocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 base base 8 ptr_addrp base ptr_capp WLimit_ _ ⇒ snapshot_valuesxs base + 8 allocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 base end; c_fuel ≔ c_fuelc = fr_doomedc_framec ∧ fr_atc_framec_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ match w with WIntn ⇒ snapshot_valuesxs base + 8 store_bytesallocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 base base 8 n WPtrp ⇒ snapshot_valuesxs base + 8 store_auxstore_bytesallocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 base base 8 ptr_addrp base ptr_capp WLimit_ _ ⇒ snapshot_valuesxs base + 8 allocatedc_memc heap_req16 Z.posPosDef.Pos.of_succ_natDatatypes.lengthxs~0~0~0 base end; c_fuel ≔ c_fuelc = Enterl None
simpl
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge c xs l q k Ha H base
unfold step in H
rewrite Ha in H
destruct xs ; discriminate H |
destruct negb_ ; discriminate H |
injection H as _ ←
simpl
auto
A return of the outcome o resumes the caller where it was waiting, with its function, locals, doom and point, and an environment given the callee's result.
Explore proof 9 tactics
Initial goal
⊢
∀c : config o : outcome c′ : config, return_stepc o = Nextc′ → ∃caller : frame pd : pending callers : listframe × pending e : env m′ : Memory.mem, c_callersc = caller, pd :: callers ∧ c′ = c_frame ≔ fr_fn ≔ fr_fncaller; fr_env ≔ e; fr_locals ≔ fr_localscaller; fr_doomed ≔ fr_doomedcaller; fr_at ≔ fr_atcaller; c_callers ≔ callers; c_mem ≔ m′; c_fuel ≔ c_fuelc
unfold return_step
intros c o c′ H
apply or_stuck_next in H
destruct invalidate_locals_ _ as m | ; | discriminate H
destruct c_callersc as | caller pd callers ; discriminate H |
⊢
∃caller0 : frame pd0 : pending callers0 : listframe × pending e : env m′ : Memory.mem, caller, pd :: callers = caller0, pd0 :: callers0 ∧ c′ = c_frame ≔ fr_fn ≔ fr_fncaller0; fr_env ≔ e; fr_locals ≔ fr_localscaller0; fr_doomed ≔ fr_doomedcaller0; fr_at ≔ fr_atcaller0; c_callers ≔ callers0; c_mem ≔ m′; c_fuel ≔ c_fuelc
destruct match pd_convpd with None ⇒ Someo Somecw, kw ⇒ converted_outcomecw kw o end ; | discriminate H
c :
o :
c′ :
m :
Memory.mem
caller :
pd :
o0 :
⊢
∃caller0 : frame pd0 : pending callers0 : listframe × pending e : env m′ : Memory.mem, caller, pd :: callers = caller0, pd0 :: callers0 ∧ c′ = c_frame ≔ fr_fn ≔ fr_fncaller0; fr_env ≔ e; fr_locals ≔ fr_localscaller0; fr_doomed ≔ fr_doomedcaller0; fr_at ≔ fr_atcaller0; c_callers ≔ callers0; c_mem ≔ m′; c_fuel ≔ c_fuelc
destruct returned_env_ _ _ as e | ; | discriminate H
c :
o :
c′ :
m :
Memory.mem
caller :
pd :
o0 :
e :
⊢
∃caller0 : frame pd0 : pending callers0 : listframe × pending e0 : env m′ : Memory.mem, caller, pd :: callers = caller0, pd0 :: callers0 ∧ c′ = c_frame ≔ fr_fn ≔ fr_fncaller0; fr_env ≔ e0; fr_locals ≔ fr_localscaller0; fr_doomed ≔ fr_doomedcaller0; fr_at ≔ fr_atcaller0; c_callers ≔ callers0; c_mem ≔ m′; c_fuel ≔ c_fuelc
injection H as ←
c :
o :
m :
Memory.mem
caller :
pd :
o0 :
e :
⊢
∃caller0 : frame pd0 : pending callers0 : listframe × pending e0 : env m′ : Memory.mem, caller, pd :: callers = caller0, pd0 :: callers0 ∧ c_frame ≔ fr_fn ≔ fr_fncaller; fr_env ≔ e; fr_locals ≔ fr_localscaller; fr_doomed ≔ fr_doomedcaller; fr_at ≔ fr_atcaller; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ c_fuelc = c_frame ≔ fr_fn ≔ fr_fncaller0; fr_env ≔ e0; fr_locals ≔ fr_localscaller0; fr_doomed ≔ fr_doomedcaller0; fr_at ≔ fr_atcaller0; c_callers ≔ callers0; c_mem ≔ m′; c_fuel ≔ c_fuelc
eauto 8
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold return_step
intros c o c′ H
apply or_stuck_next in H
destruct invalidate_locals_ _ as m | ; | discriminate H
destruct c_callersc as | caller pd callers ; discriminate H |
destruct match pd_convpd with None ⇒ Someo Somecw, kw ⇒ converted_outcomecw kw o end ; | discriminate H
destruct returned_env_ _ _ as e | ; | discriminate H
injection H as ←
eauto 8
A raw call through q, whose pointer p passed its function check (function_check_res), does not stop as unchecked.
Explore proof 9 tactics
Initial goal
intros ge fr m r q args p why Hq Hc H
unfold inst_step , value_x in H
rewrite Hq in H
cbn [ word_at_class ] in H
destruct map_option_ args ; | discriminate H
cbv beta iota zeta in H
rewrite Hc in H
cbn [ raw_res ] in H
cases H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge fr m r q args p why Hq Hc H
rewrite Hq in H
cbn [ word_at_class ] in H
destruct map_option_ args ; | discriminate H
cbv beta iota zeta in H
rewrite Hc in H
cbn [ raw_res ] in H
cases H