rocq/theories/StepRules.v
What one step gives, rule by rule: for each instruction form of the core subset and each jump, the configuration step reaches from a frame at it, under premises small enough to compute on their own. They are the forward reading of Steps.v, whose lemmas say what a step that happened must have been.
A program proof that reduces step itself carries the whole function and memory through every reduction; Cycle.v and Buffer.v spend most of their time there (proof, docs/logic.md). With these rules, a proof names the instruction, checks the premises (a temporary's value, an operation on words, an access check against an object's region) and gets the next configuration as a term. They are the instruction rules of the program logic (docs/logic.md): its weakest-precondition rules are these, lifted.
Every rule is for a frame that is not doomed.
From Stdlib Require Import String ZArith List Bool Lia
From Nanofil Require Import Term Syntax Values Memory Ops Semantics
Import ListNotations
Open Scope Z_scope
Operations
match o with
_
⇒
true
An instruction's result that continues keeps a frame that is not doomed undoomed.
∀ ge fr m i e ls m′
fr_doomedfr = None
doomed_resultge fr m i IContinuee ls m′ = SomeIContinuee ls m′, None
Explore proof 7 tactics
Initial goal
intros ge fr m i e ls m′ Hd
unfold doomed_result
rewrite Hd
destruct i as d k o args | | | | | | | ; try reflexivity
destruct k ; try reflexivity
destruct o ; try reflexivity
destruct args as | a | a′ args ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge fr m i e ls m′ Hd
unfold doomed_result
rewrite Hd
destruct i as d k o args | | | | | | | ; try reflexivity
destruct k ; try reflexivity
destruct o ; try reflexivity
destruct args as | a | a′ args ; reflexivity
An instruction's result that allocates keeps a frame that is not doomed undoomed.
Explore proof 7 tactics
Initial goal
intros ge fr m i q kk Hd
unfold doomed_result
rewrite Hd
destruct i as d k o args | | | | | | | ; try reflexivity
destruct k ; try reflexivity
destruct o ; try reflexivity
destruct args as | a | a′ args ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge fr m i q kk Hd
unfold doomed_result
rewrite Hd
destruct i as d k o args | | | | | | | ; try reflexivity
destruct k ; try reflexivity
destruct o ; try reflexivity
destruct args as | a | a′ args ; reflexivity
An instruction's result that calls keeps a frame that is not doomed undoomed.
Explore proof 7 tactics
Initial goal
intros ge fr m i g xs pd Hd
unfold doomed_result
rewrite Hd
destruct i as d k o args | | | | | | | ; try reflexivity
destruct k ; try reflexivity
destruct o ; try reflexivity
destruct args as | a | a′ args ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge fr m i g xs pd Hd
unfold doomed_result
rewrite Hd
destruct i as d k o args | | | | | | | ; try reflexivity
destruct k ; try reflexivity
destruct o ; try reflexivity
destruct args as | a | a′ args ; reflexivity
∀ ge f e ls l i rest j cs m fuel out
doomed_resultge mkFramef e ls None Execl i :: rest j m i out = Someout, None
Explore proof 5 tactics
Initial goal
⊢
∀ge : genv f : func e : env ls : listname × optionZ l : name i : inst rest : listinst j : jump cs : listframe × pending m : mem fuel : Z out : inst_out, inst_stepge fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl i :: rest j m i = Someout → doomed_resultge fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl i :: rest j m i out = Someout, None → stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl i :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = inst_nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl i :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel l rest j out None
intros ge f e ls l i rest j cs m fuel out Hi Hd
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl i :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = inst_nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl i :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel l rest j out None
unfold step ; cbn [ fr_at c_frame c_mem fr_doomed ]
rewrite Hi
rewrite Hd
⊢
or_stuck"instruction" Someinst_nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl i :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel l rest j fstout, None sndout, None = inst_nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl i :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel l rest j out None
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
A let of a general op whose arguments read as the words xs and whose op_res is the word w, in the memory m': the frame binds w to d and goes on, in m'.
∀ ge f e ls l d k o args rest j cs m fuel classes xs w m′
Explore proof 12 tactics
Initial goal
⊢
∀ge : genv f : func e : env ls : listname × optionZ l d : name k : class o : op args : listvalue rest : listinst j : jump cs : listframe × pending m : mem fuel : Z classes : listclass xs : listword w : word m′ : mem, general_opo = true → op_arg_classeso k = Someclasses → map2_optionvalue_xge e classes args = Somexs → op_reso k xs m = SomeOpResRValw m′ → stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd k o args :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ putd w e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
intros ge f e ls l d k o args rest j cs m fuel classes xs w m′ Hg Hc Hx Ho
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
assert Hi : inst_stepge mkFramef e ls None Execl Letd k o args :: rest j m Letd k o args = SomeIContinueputd w e ls m′
2 openge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
focused goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
{transitivity let* classes ≔ op_arg_classeso k in let* xs ≔ map2_optionvalue_xge e classes args in let* out ≔ op_reso k xs m in match out with OpResr m′ ⇒ Somebind_resd r e ls m′ OpUBwhy ⇒ SomeIStopUBwhy OpAllocq kont ⇒ SomeIFreshq λbase ⇒ let x, m′ ≔ kontbase in putd x e, ls, m′ end
3 openge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
focused goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
–destruct o ; try discriminate Hg ; destruct k ; reflexivity
2 opendeferred goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
–rewrite Hc
2 openge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
cbn - [ op_res map2_option ]
2 openge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
rewrite Hx
2 openge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
cbn - [ op_res ]
2 openge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
rewrite Ho
2 openge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
reflexivity
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
rewrite rule_inst_ _ _ _ _ _ _ _ _ _ _ _ Hi by apply doomed_result_continue ; reflexivity
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
o :
args :
listvalue
rest :
listinst
j :
m :
fuel :
Z
classes :
listclass
xs :
listword
w :
m′ :
Hg :
general_opo = true
Hc :
op_arg_classeso k = Someclasses
Hx :
map2_optionvalue_xge e classes args = Somexs
⊢
inst_nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd k o args :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel l rest j IContinueputd w e ls m′ None = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ putd w e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge f e ls l d k o args rest j cs m fuel classes xs w m′ Hg Hc Hx Ho
assert Hi : inst_stepge mkFramef e ls None Execl Letd k o args :: rest j m Letd k o args = SomeIContinueputd w e ls m′
{transitivity let* classes ≔ op_arg_classeso k in let* xs ≔ map2_optionvalue_xge e classes args in let* out ≔ op_reso k xs m in match out with OpResr m′ ⇒ Somebind_resd r e ls m′ OpUBwhy ⇒ SomeIStopUBwhy OpAllocq kont ⇒ SomeIFreshq λbase ⇒ let x, m′ ≔ kontbase in putd x e, ls, m′ end
–destruct o ; try discriminate Hg ; destruct k ; reflexivity
rewrite rule_inst_ _ _ _ _ _ _ _ _ _ _ _ Hi by apply doomed_result_continue ; reflexivity
reflexivity
∀ ge f e ls l d k al args rest j cs m fuel size
map2_optionvalue_xge e L args = SomeWIntsize
size ≤ max_allocation_size
Explore proof 5 tactics
Initial goal
⊢
∀ge : genv f : func e : env ls : listname × optionZ l d : name k : class al : Z args : listvalue rest : listinst j : jump cs : listframe × pending m : mem fuel size : Z, map2_optionvalue_xge e L args = SomeWIntsize → size ≤ max_allocation_size → stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd k Allocal args :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Freshheap_reqal size λbase : Z ⇒ c_frame ≔ fr_fn ≔ f; fr_env ≔ putd WPtrptr_addr ≔ base; ptr_cap ≔ Objbase e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ allocatedm heap_reqal size base; c_fuel ≔ fuel
intros ge f e ls l d k al args rest j cs m fuel size Hx Hs
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
al :
Z
args :
listvalue
rest :
listinst
j :
m :
fuel, size :
Z
Hx :
map2_optionvalue_xge e L args = SomeWIntsize
Hs :
size ≤ max_allocation_size
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd k Allocal args :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Freshheap_reqal size λbase : Z ⇒ c_frame ≔ fr_fn ≔ f; fr_env ≔ putd WPtrptr_addr ≔ base; ptr_cap ≔ Objbase e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ allocatedm heap_reqal size base; c_fuel ≔ fuel
assert Hi : inst_stepge mkFramef e ls None Execl Letd k Allocal args :: rest j m Letd k Allocal args = SomeIFreshheap_reqal size λbase ⇒ putd WPtrmkPtrbase Objbase e, ls, allocatedm heap_reqal size base
2 openge :
f :
e :
ls :
listname × optionZ
l, d :
k :
al :
Z
args :
listvalue
rest :
listinst
j :
m :
fuel, size :
Z
Hx :
map2_optionvalue_xge e L args = SomeWIntsize
Hs :
size ≤ max_allocation_size
focused goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
al :
Z
args :
listvalue
rest :
listinst
j :
m :
fuel, size :
Z
Hx :
map2_optionvalue_xge e L args = SomeWIntsize
Hs :
size ≤ max_allocation_size
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd k Allocal args :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Freshheap_reqal size λbase : Z ⇒ c_frame ≔ fr_fn ≔ f; fr_env ≔ putd WPtrptr_addr ≔ base; ptr_cap ≔ Objbase e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ allocatedm heap_reqal size base; c_fuel ≔ fuel
{destruct k ; cbn - [ map2_option heap_req allocated max_allocation_size ] ; rewrite Hx ; cbn - [ heap_req allocated max_allocation_size ] ; replace max_allocation_size <? size with false by symmetry ; apply Z.ltb_ge ; exact Hs ; reflexivity
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
al :
Z
args :
listvalue
rest :
listinst
j :
m :
fuel, size :
Z
Hx :
map2_optionvalue_xge e L args = SomeWIntsize
Hs :
size ≤ max_allocation_size
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd k Allocal args :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Freshheap_reqal size λbase : Z ⇒ c_frame ≔ fr_fn ≔ f; fr_env ≔ putd WPtrptr_addr ≔ base; ptr_cap ≔ Objbase e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ allocatedm heap_reqal size base; c_fuel ≔ fuel
rewrite rule_inst_ _ _ _ _ _ _ _ _ _ _ _ Hi by apply doomed_result_fresh_none ; reflexivity
ge :
f :
e :
ls :
listname × optionZ
l, d :
k :
al :
Z
args :
listvalue
rest :
listinst
j :
m :
fuel, size :
Z
Hx :
map2_optionvalue_xge e L args = SomeWIntsize
Hs :
size ≤ max_allocation_size
⊢
inst_nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd k Allocal args :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel l rest j IFreshheap_reqal size λbase : Z ⇒ putd WPtrptr_addr ≔ base; ptr_cap ≔ Objbase e, ls, allocatedm heap_reqal size base None = Freshheap_reqal size λbase : Z ⇒ c_frame ≔ fr_fn ≔ f; fr_env ≔ putd WPtrptr_addr ≔ base; ptr_cap ≔ Objbase e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ allocatedm heap_reqal size base; c_fuel ≔ fuel
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge f e ls l d k al args rest j cs m fuel size Hx Hs
assert Hi : inst_stepge mkFramef e ls None Execl Letd k Allocal args :: rest j m Letd k Allocal args = SomeIFreshheap_reqal size λbase ⇒ putd WPtrmkPtrbase Objbase e, ls, allocatedm heap_reqal size base
{destruct k ; cbn - [ map2_option heap_req allocated max_allocation_size ] ; rewrite Hx ; cbn - [ heap_req allocated max_allocation_size ] ; replace max_allocation_size <? size with false by symmetry ; apply Z.ltb_ge ; exact Hs ; reflexivity
rewrite rule_inst_ _ _ _ _ _ _ _ _ _ _ _ Hi by apply doomed_result_fresh_none ; reflexivity
reflexivity
Flights and stores
Explore proof 7 tactics
Initial goal
⊢
∀ge : genv f : func e : env ls : listname × optionZ l d : name o : op args : listflight_arg lw : flight_lower rest : listinst j : jump cs : listframe × pending m : mem fuel : Z xs : listword n : Z c : cap, map_optionflight_arg_xge e args = Somexs → aluo L xs = SomeWIntn → flight_capge e lw = Somec → stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Flightd o args lw :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ putd WPtrptr_addr ≔ n; ptr_cap ≔ c e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel
intros ge f e ls l d o args lw rest j cs m fuel xs n c Hx Ha Hc
ge :
f :
e :
ls :
listname × optionZ
l, d :
o :
args :
listflight_arg
lw :
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
n :
Z
c :
Hx :
map_optionflight_arg_xge e args = Somexs
Hc :
flight_capge e lw = Somec
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Flightd o args lw :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ putd WPtrptr_addr ≔ n; ptr_cap ≔ c e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel
assert Hi : inst_stepge mkFramef e ls None Execl Flightd o args lw :: rest j m Flightd o args lw = SomeIContinueputd WPtrmkPtrn c e ls m
2 openge :
f :
e :
ls :
listname × optionZ
l, d :
o :
args :
listflight_arg
lw :
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
n :
Z
c :
Hx :
map_optionflight_arg_xge e args = Somexs
Hc :
flight_capge e lw = Somec
focused goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
o :
args :
listflight_arg
lw :
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
n :
Z
c :
Hx :
map_optionflight_arg_xge e args = Somexs
Hc :
flight_capge e lw = Somec
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Flightd o args lw :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ putd WPtrptr_addr ≔ n; ptr_cap ≔ c e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel
{cbn - [ map_option alu flight_cap ]
2 openge :
f :
e :
ls :
listname × optionZ
l, d :
o :
args :
listflight_arg
lw :
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
n :
Z
c :
Hx :
map_optionflight_arg_xge e args = Somexs
Hc :
flight_capge e lw = Somec
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
o :
args :
listflight_arg
lw :
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
n :
Z
c :
Hx :
map_optionflight_arg_xge e args = Somexs
Hc :
flight_capge e lw = Somec
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Flightd o args lw :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ putd WPtrptr_addr ≔ n; ptr_cap ≔ c e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel
rewrite Hx , Ha , Hc
2 openge :
f :
e :
ls :
listname × optionZ
l, d :
o :
args :
listflight_arg
lw :
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
n :
Z
c :
Hx :
map_optionflight_arg_xge e args = Somexs
Hc :
flight_capge e lw = Somec
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
o :
args :
listflight_arg
lw :
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
n :
Z
c :
Hx :
map_optionflight_arg_xge e args = Somexs
Hc :
flight_capge e lw = Somec
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Flightd o args lw :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ putd WPtrptr_addr ≔ n; ptr_cap ≔ c e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel
reflexivity
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l, d :
o :
args :
listflight_arg
lw :
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
n :
Z
c :
Hx :
map_optionflight_arg_xge e args = Somexs
Hc :
flight_capge e lw = Somec
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Flightd o args lw :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ putd WPtrptr_addr ≔ n; ptr_cap ≔ c e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel
rewrite rule_inst_ _ _ _ _ _ _ _ _ _ _ _ Hi by apply doomed_result_continue ; reflexivity
ge :
f :
e :
ls :
listname × optionZ
l, d :
o :
args :
listflight_arg
lw :
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
n :
Z
c :
Hx :
map_optionflight_arg_xge e args = Somexs
Hc :
flight_capge e lw = Somec
⊢
inst_nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Flightd o args lw :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel l rest j IContinueputd WPtrptr_addr ≔ n; ptr_cap ≔ c e ls m None = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ putd WPtrptr_addr ≔ n; ptr_cap ≔ c e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A raw store of width w of the value v, which reads as x, through the proven pointer a, which reads as p, at offset off, where the store passes and leaves the memory m': the frame goes on in m'.
∀ ge f e ls l w off v a rest j cs m fuel vk x p m′
width_value_classw = Somevk
value_xge e vk v = Somex
store_resw m raw_addressptr_addrp off ptr_capp x = Someok, m′
Explore proof 7 tactics
Initial goal
⊢
∀ge : genv f : func e : env ls : listname × optionZ l : name w : width off : Z v a : value rest : listinst j : jump cs : listframe × pending m : mem fuel : Z vk : class x : word p : ptr m′ : mem, width_value_classw = Somevk → value_xge e vk v = Somex → value_xge e A a = SomeWPtrp → store_resw m raw_addressptr_addrp off ptr_capp x = Someok, m′ → stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorew off v a :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
intros ge f e ls l w off v a rest j cs m fuel vk x p m′ Hw Hv Ha Hs
ge :
f :
e :
ls :
listname × optionZ
l :
w :
off :
Z
v, a :
rest :
listinst
j :
m :
fuel :
Z
vk :
x :
p :
m′ :
Hw :
width_value_classw = Somevk
Hv :
value_xge e vk v = Somex
Hs :
store_resw m raw_addressptr_addrp off ptr_capp x = Someok, m′
assert Hi : inst_stepge mkFramef e ls None Execl RawStorew off v a :: rest j m RawStorew off v a = SomeIContinuee ls m′
2 openge :
f :
e :
ls :
listname × optionZ
l :
w :
off :
Z
v, a :
rest :
listinst
j :
m :
fuel :
Z
vk :
x :
p :
m′ :
Hw :
width_value_classw = Somevk
Hv :
value_xge e vk v = Somex
Hs :
store_resw m raw_addressptr_addrp off ptr_capp x = Someok, m′
focused goal
ge :
f :
e :
ls :
listname × optionZ
l :
w :
off :
Z
v, a :
rest :
listinst
j :
m :
fuel :
Z
vk :
x :
p :
m′ :
Hw :
width_value_classw = Somevk
Hv :
value_xge e vk v = Somex
Hs :
store_resw m raw_addressptr_addrp off ptr_capp x = Someok, m′
{cbn - [ width_value_class value_x store_res raw_address ]
2 openge :
f :
e :
ls :
listname × optionZ
l :
w :
off :
Z
v, a :
rest :
listinst
j :
m :
fuel :
Z
vk :
x :
p :
m′ :
Hw :
width_value_classw = Somevk
Hv :
value_xge e vk v = Somex
Hs :
store_resw m raw_addressptr_addrp off ptr_capp x = Someok, m′
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
w :
off :
Z
v, a :
rest :
listinst
j :
m :
fuel :
Z
vk :
x :
p :
m′ :
Hw :
width_value_classw = Somevk
Hv :
value_xge e vk v = Somex
Hs :
store_resw m raw_addressptr_addrp off ptr_capp x = Someok, m′
rewrite Hw , Hv , Ha , Hs
2 openge :
f :
e :
ls :
listname × optionZ
l :
w :
off :
Z
v, a :
rest :
listinst
j :
m :
fuel :
Z
vk :
x :
p :
m′ :
Hw :
width_value_classw = Somevk
Hv :
value_xge e vk v = Somex
Hs :
store_resw m raw_addressptr_addrp off ptr_capp x = Someok, m′
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
w :
off :
Z
v, a :
rest :
listinst
j :
m :
fuel :
Z
vk :
x :
p :
m′ :
Hw :
width_value_classw = Somevk
Hv :
value_xge e vk v = Somex
Hs :
store_resw m raw_addressptr_addrp off ptr_capp x = Someok, m′
reflexivity
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
w :
off :
Z
v, a :
rest :
listinst
j :
m :
fuel :
Z
vk :
x :
p :
m′ :
Hw :
width_value_classw = Somevk
Hv :
value_xge e vk v = Somex
Hs :
store_resw m raw_addressptr_addrp off ptr_capp x = Someok, m′
rewrite rule_inst_ _ _ _ _ _ _ _ _ _ _ _ Hi by apply doomed_result_continue ; reflexivity
ge :
f :
e :
ls :
listname × optionZ
l :
w :
off :
Z
v, a :
rest :
listinst
j :
m :
fuel :
Z
vk :
x :
p :
m′ :
Hw :
width_value_classw = Somevk
Hv :
value_xge e vk v = Somex
Hs :
store_resw m raw_addressptr_addrp off ptr_capp x = Someok, m′
⊢
inst_nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorew off v a :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel l rest j IContinuee ls m′ None = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
A raw store of the pointer v, which reads as xp, through the proven pointer a, which reads as p, at offset off: where the 8-byte write access there passes and the protocol es leaves the memory m', the frame goes on in m'.
∀ ge f e ls l off v a es rest j cs m fuel xp p m′
access_resm raw_addressptr_addrp off ptr_capp 8 Write 8 = Someok
pointer_store_effectsraw_addressptr_addrp off xp m es = Somem′
Explore proof 9 tactics
Initial goal
⊢
∀ge : genv f : func e : env ls : listname × optionZ l : name off : Z v a : value es : listeffect rest : listinst j : jump cs : listframe × pending m : mem fuel : Z xp p : ptr m′ : mem, value_xge e P v = SomeWPtrxp → value_xge e A a = SomeWPtrp → access_resm raw_addressptr_addrp off ptr_capp 8 Write 8 = Someok → pointer_store_effectsraw_addressptr_addrp off xp m es = Somem′ → stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
intros ge f e ls l off v a es rest j cs m fuel xp p m′ Hv Ha Hc Hs
ge :
f :
e :
ls :
listname × optionZ
l :
off :
Z
v, a :
es :
listeffect
rest :
listinst
j :
m :
fuel :
Z
xp, p :
m′ :
Hc :
access_resm raw_addressptr_addrp off ptr_capp 8 Write 8 = Someok
Hs :
pointer_store_effectsraw_addressptr_addrp off xp m es = Somem′
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
assert Hi : inst_stepge mkFramef e ls None Execl RawStorePointeroff v a es :: rest j m RawStorePointeroff v a es = SomeIContinuee ls m′
2 openge :
f :
e :
ls :
listname × optionZ
l :
off :
Z
v, a :
es :
listeffect
rest :
listinst
j :
m :
fuel :
Z
xp, p :
m′ :
Hc :
access_resm raw_addressptr_addrp off ptr_capp 8 Write 8 = Someok
Hs :
pointer_store_effectsraw_addressptr_addrp off xp m es = Somem′
⊢
inst_stepge fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j m RawStorePointeroff v a es = SomeIContinuee ls m′
focused goal
ge :
f :
e :
ls :
listname × optionZ
l :
off :
Z
v, a :
es :
listeffect
rest :
listinst
j :
m :
fuel :
Z
xp, p :
m′ :
Hc :
access_resm raw_addressptr_addrp off ptr_capp 8 Write 8 = Someok
Hs :
pointer_store_effectsraw_addressptr_addrp off xp m es = Somem′
Hi :
inst_stepge fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j m RawStorePointeroff v a es = SomeIContinuee ls m′
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
{cbn - [ value_x access_res pointer_store_effects raw_address ]
2 openge :
f :
e :
ls :
listname × optionZ
l :
off :
Z
v, a :
es :
listeffect
rest :
listinst
j :
m :
fuel :
Z
xp, p :
m′ :
Hc :
access_resm raw_addressptr_addrp off ptr_capp 8 Write 8 = Someok
Hs :
pointer_store_effectsraw_addressptr_addrp off xp m es = Somem′
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
off :
Z
v, a :
es :
listeffect
rest :
listinst
j :
m :
fuel :
Z
xp, p :
m′ :
Hc :
access_resm raw_addressptr_addrp off ptr_capp 8 Write 8 = Someok
Hs :
pointer_store_effectsraw_addressptr_addrp off xp m es = Somem′
Hi :
inst_stepge fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j m RawStorePointeroff v a es = SomeIContinuee ls m′
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
rewrite Hv , Ha , Hc
2 openge :
f :
e :
ls :
listname × optionZ
l :
off :
Z
v, a :
es :
listeffect
rest :
listinst
j :
m :
fuel :
Z
xp, p :
m′ :
Hc :
access_resm raw_addressptr_addrp off ptr_capp 8 Write 8 = Someok
Hs :
pointer_store_effectsraw_addressptr_addrp off xp m es = Somem′
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
off :
Z
v, a :
es :
listeffect
rest :
listinst
j :
m :
fuel :
Z
xp, p :
m′ :
Hc :
access_resm raw_addressptr_addrp off ptr_capp 8 Write 8 = Someok
Hs :
pointer_store_effectsraw_addressptr_addrp off xp m es = Somem′
Hi :
inst_stepge fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j m RawStorePointeroff v a es = SomeIContinuee ls m′
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
cbn - [ pointer_store_effects raw_address ]
2 openge :
f :
e :
ls :
listname × optionZ
l :
off :
Z
v, a :
es :
listeffect
rest :
listinst
j :
m :
fuel :
Z
xp, p :
m′ :
Hc :
access_resm raw_addressptr_addrp off ptr_capp 8 Write 8 = Someok
Hs :
pointer_store_effectsraw_addressptr_addrp off xp m es = Somem′
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
off :
Z
v, a :
es :
listeffect
rest :
listinst
j :
m :
fuel :
Z
xp, p :
m′ :
Hc :
access_resm raw_addressptr_addrp off ptr_capp 8 Write 8 = Someok
Hs :
pointer_store_effectsraw_addressptr_addrp off xp m es = Somem′
Hi :
inst_stepge fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j m RawStorePointeroff v a es = SomeIContinuee ls m′
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
rewrite Hs
2 openge :
f :
e :
ls :
listname × optionZ
l :
off :
Z
v, a :
es :
listeffect
rest :
listinst
j :
m :
fuel :
Z
xp, p :
m′ :
Hc :
access_resm raw_addressptr_addrp off ptr_capp 8 Write 8 = Someok
Hs :
pointer_store_effectsraw_addressptr_addrp off xp m es = Somem′
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
off :
Z
v, a :
es :
listeffect
rest :
listinst
j :
m :
fuel :
Z
xp, p :
m′ :
Hc :
access_resm raw_addressptr_addrp off ptr_capp 8 Write 8 = Someok
Hs :
pointer_store_effectsraw_addressptr_addrp off xp m es = Somem′
Hi :
inst_stepge fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j m RawStorePointeroff v a es = SomeIContinuee ls m′
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
reflexivity
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
off :
Z
v, a :
es :
listeffect
rest :
listinst
j :
m :
fuel :
Z
xp, p :
m′ :
Hc :
access_resm raw_addressptr_addrp off ptr_capp 8 Write 8 = Someok
Hs :
pointer_store_effectsraw_addressptr_addrp off xp m es = Somem′
Hi :
inst_stepge fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j m RawStorePointeroff v a es = SomeIContinuee ls m′
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
rewrite rule_inst_ _ _ _ _ _ _ _ _ _ _ _ Hi by apply doomed_result_continue ; reflexivity
ge :
f :
e :
ls :
listname × optionZ
l :
off :
Z
v, a :
es :
listeffect
rest :
listinst
j :
m :
fuel :
Z
xp, p :
m′ :
Hc :
access_resm raw_addressptr_addrp off ptr_capp 8 Write 8 = Someok
Hs :
pointer_store_effectsraw_addressptr_addrp off xp m es = Somem′
Hi :
inst_stepge fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j m RawStorePointeroff v a es = SomeIContinuee ls m′
⊢
inst_nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl RawStorePointeroff v a es :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel l rest j IContinuee ls m′ None = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge f e ls l off v a es rest j cs m fuel xp p m′ Hv Ha Hc Hs
assert Hi : inst_stepge mkFramef e ls None Execl RawStorePointeroff v a es :: rest j m RawStorePointeroff v a es = SomeIContinuee ls m′
{cbn - [ value_x access_res pointer_store_effects raw_address ]
rewrite Hv , Ha , Hc
cbn - [ pointer_store_effects raw_address ]
rewrite Hs
reflexivity
rewrite rule_inst_ _ _ _ _ _ _ _ _ _ _ _ Hi by apply doomed_result_continue ; reflexivity
reflexivity
Calls
A direct call of the function g, defined in the module, with arguments that read as xs and make its frame callee: the callee runs on top, and the caller waits at the rest of its block for the result r.
∀ ge f e ls l r g args rest j cs m fuel xs gf callee
Explore proof 9 tactics
Initial goal
⊢
∀ge : genv f : func e : env ls : listname × optionZ l : name r : call_result g : name args : listarg rest : listinst j : jump cs : listframe × pending m : mem fuel : Z xs : listword gf : func callee : frame, map_optionarg_xge e args = Somexs → find_fnge g = SomeDefinedgf → call_framegf xs = Somecallee → stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Callr Globalg args :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ callee; c_callers ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j, pd_res ≔ r; pd_conv ≔ None :: cs; c_mem ≔ m; c_fuel ≔ fuel
intros ge f e ls l r g args rest j cs m fuel xs gf callee Hx Hf Hc
ge :
f :
e :
ls :
listname × optionZ
l :
r :
g :
args :
listarg
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
gf :
callee :
Hx :
map_optionarg_xge e args = Somexs
Hc :
call_framegf xs = Somecallee
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Callr Globalg args :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ callee; c_callers ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j, pd_res ≔ r; pd_conv ≔ None :: cs; c_mem ≔ m; c_fuel ≔ fuel
assert Hi : inst_stepge mkFramef e ls None Execl Callr Globalg args :: rest j m Callr Globalg args = SomeICallgf xs mkPendingr None
2 openge :
f :
e :
ls :
listname × optionZ
l :
r :
g :
args :
listarg
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
gf :
callee :
Hx :
map_optionarg_xge e args = Somexs
Hc :
call_framegf xs = Somecallee
focused goal
ge :
f :
e :
ls :
listname × optionZ
l :
r :
g :
args :
listarg
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
gf :
callee :
Hx :
map_optionarg_xge e args = Somexs
Hc :
call_framegf xs = Somecallee
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Callr Globalg args :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ callee; c_callers ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j, pd_res ≔ r; pd_conv ≔ None :: cs; c_mem ≔ m; c_fuel ≔ fuel
{cbn - [ map_option find_fn ]
2 openge :
f :
e :
ls :
listname × optionZ
l :
r :
g :
args :
listarg
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
gf :
callee :
Hx :
map_optionarg_xge e args = Somexs
Hc :
call_framegf xs = Somecallee
⊢
=
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
r :
g :
args :
listarg
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
gf :
callee :
Hx :
map_optionarg_xge e args = Somexs
Hc :
call_framegf xs = Somecallee
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Callr Globalg args :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ callee; c_callers ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j, pd_res ≔ r; pd_conv ≔ None :: cs; c_mem ≔ m; c_fuel ≔ fuel
rewrite Hx , Hf
2 openge :
f :
e :
ls :
listname × optionZ
l :
r :
g :
args :
listarg
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
gf :
callee :
Hx :
map_optionarg_xge e args = Somexs
Hc :
call_framegf xs = Somecallee
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
r :
g :
args :
listarg
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
gf :
callee :
Hx :
map_optionarg_xge e args = Somexs
Hc :
call_framegf xs = Somecallee
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Callr Globalg args :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ callee; c_callers ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j, pd_res ≔ r; pd_conv ≔ None :: cs; c_mem ≔ m; c_fuel ≔ fuel
reflexivity
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
r :
g :
args :
listarg
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
gf :
callee :
Hx :
map_optionarg_xge e args = Somexs
Hc :
call_framegf xs = Somecallee
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Callr Globalg args :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ callee; c_callers ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j, pd_res ≔ r; pd_conv ≔ None :: cs; c_mem ≔ m; c_fuel ≔ fuel
rewrite rule_inst_ _ _ _ _ _ _ _ _ _ _ _ Hi by apply doomed_result_call ; reflexivity
ge :
f :
e :
ls :
listname × optionZ
l :
r :
g :
args :
listarg
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
gf :
callee :
Hx :
map_optionarg_xge e args = Somexs
Hc :
call_framegf xs = Somecallee
⊢
inst_nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Callr Globalg args :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel l rest j ICallgf xs pd_res ≔ r; pd_conv ≔ None None = Nextc_frame ≔ callee; c_callers ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j, pd_res ≔ r; pd_conv ≔ None :: cs; c_mem ≔ m; c_fuel ≔ fuel
cbn [ inst_next c_frame fr_fn fr_env fr_locals c_callers c_mem c_fuel ]
ge :
f :
e :
ls :
listname × optionZ
l :
r :
g :
args :
listarg
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
gf :
callee :
Hx :
map_optionarg_xge e args = Somexs
Hc :
call_framegf xs = Somecallee
⊢
=
rewrite Hc
ge :
f :
e :
ls :
listname × optionZ
l :
r :
g :
args :
listarg
rest :
listinst
j :
m :
fuel :
Z
xs :
listword
gf :
callee :
Hx :
map_optionarg_xge e args = Somexs
Hc :
call_framegf xs = Somecallee
⊢
Nextc_frame ≔ callee; c_callers ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j, pd_res ≔ r; pd_conv ≔ None :: cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ callee; c_callers ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j, pd_res ≔ r; pd_conv ≔ None :: cs; c_mem ≔ m; c_fuel ≔ fuel
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge f e ls l r g args rest j cs m fuel xs gf callee Hx Hf Hc
assert Hi : inst_stepge mkFramef e ls None Execl Callr Globalg args :: rest j m Callr Globalg args = SomeICallgf xs mkPendingr None
rewrite rule_inst_ _ _ _ _ _ _ _ _ _ _ _ Hi by apply doomed_result_call ; reflexivity
rewrite Hc
reflexivity
A call of libc's void free(p), a name the module neither defines nor holds as data, whose argument v reads as x, where the genv's free frees x without a trap and leaves the memory m': the frame goes on in m' (external_call).
Explore proof 11 tactics
Initial goal
⊢
∀ge : genv f : func e : env ls : listname × optionZ l : name v : value rest : listinst j : jump cs : listframe × pending m : mem fuel : Z x : word m′ : mem, find_fnge free_name = None → lookupfree_name ge_globalsge = None → arg_xge e ArgP v = Somex → ge_freege x m = Someok, m′ → stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
intros ge f e ls l v rest j cs m fuel x m′ Hf Hd Hx Hfree
ge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
assert Hi : inst_stepge mkFramef e ls None Execl CallCVoid Globalfree_name ArgP v :: rest j m CallCVoid Globalfree_name ArgP v = SomeIContinuee ls m′
2 openge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
focused goal
ge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
{cbn - [ arg_x find_fn lookup ge_free ]
2 openge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
rewrite Hx , Hf
2 openge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
unfold external_call
2 openge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
rewrite Hd
2 openge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
cbn - [ ge_free ]
2 openge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
rewrite Hfree
2 openge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
reflexivity
deferred goal
ge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
rewrite rule_inst_ _ _ _ _ _ _ _ _ _ _ _ Hi by apply doomed_result_continue ; reflexivity
ge :
f :
e :
ls :
listname × optionZ
l :
v :
rest :
listinst
j :
m :
fuel :
Z
x :
m′ :
Hd :
lookupfree_name ge_globalsge = None
⊢
inst_nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl CallCVoid Globalfree_name ArgP v :: rest j; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel l rest j IContinuee ls m′ None = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge f e ls l v rest j cs m fuel x m′ Hf Hd Hx Hfree
assert Hi : inst_stepge mkFramef e ls None Execl CallCVoid Globalfree_name ArgP v :: rest j m CallCVoid Globalfree_name ArgP v = SomeIContinuee ls m′
rewrite rule_inst_ _ _ _ _ _ _ _ _ _ _ _ Hi by apply doomed_result_continue ; reflexivity
reflexivity
Blocks and jumps
Entering the block l of f, found as b, from the edge from, with fuel left: its phis bind the environment e', and the frame goes on at its instructions with one fuel less.
Explore proof 7 tactics
Initial goal
⊢
∀ge : genv f : func e : env ls : listname × optionZ l : name from : optionname cs : listframe × pending m : mem fuel : Z b : block e′ : env, fuel ≠ 0 → find_blockl fn_blocksf = Someb → phis_envge b_phisb from e = Somee′ → stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e′; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel − 1
intros ge f e ls l from cs m fuel b e′ Hf Hb Hp
ge :
f :
e :
ls :
listname × optionZ
l :
from :
optionname
m :
fuel :
Z
b :
e′ :
Hf :
fuel ≠ 0
Hb :
find_blockl fn_blocksf = Someb
unfold step ; cbn [ fr_at c_frame c_fuel fr_fn fr_env ]
ge :
f :
e :
ls :
listname × optionZ
l :
from :
optionname
m :
fuel :
Z
b :
e′ :
Hf :
fuel ≠ 0
Hb :
find_blockl fn_blocksf = Someb
⊢
else
or_stuck"block"
SomeNextc_frame ≔ fr_fn ≔ f; fr_env ≔ e0; fr_locals ≔ fr_localsfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; fr_doomed ≔ fr_doomedfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; fr_at ≔ Execl b_instsb0 b_jumpb0; c_callers ≔ c_callersc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel; c_mem ≔ c_memc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel; c_fuel ≔ fuel − 1
=
replace fuel =? 0 with false by symmetry ; apply Z.eqb_neq ; exact Hf
ge :
f :
e :
ls :
listname × optionZ
l :
from :
optionname
m :
fuel :
Z
b :
e′ :
Hf :
fuel ≠ 0
Hb :
find_blockl fn_blocksf = Someb
⊢
or_stuck"block"
SomeNextc_frame ≔ fr_fn ≔ f; fr_env ≔ e0; fr_locals ≔ fr_localsfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; fr_doomed ≔ fr_doomedfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; fr_at ≔ Execl b_instsb0 b_jumpb0; c_callers ≔ c_callersc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel; c_mem ≔ c_memc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel; c_fuel ≔ fuel − 1
=
rewrite Hb
ge :
f :
e :
ls :
listname × optionZ
l :
from :
optionname
m :
fuel :
Z
b :
e′ :
Hf :
fuel ≠ 0
Hb :
find_blockl fn_blocksf = Someb
⊢
or_stuck"block"
SomeNextc_frame ≔ fr_fn ≔ f; fr_env ≔ e0; fr_locals ≔ fr_localsfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; fr_doomed ≔ fr_doomedfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ c_callersc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel; c_mem ≔ c_memc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel; c_fuel ≔ fuel − 1
=
cbn [ b_phis ]
ge :
f :
e :
ls :
listname × optionZ
l :
from :
optionname
m :
fuel :
Z
b :
e′ :
Hf :
fuel ≠ 0
Hb :
find_blockl fn_blocksf = Someb
⊢
or_stuck"block"
SomeNextc_frame ≔ fr_fn ≔ f; fr_env ≔ e0; fr_locals ≔ fr_localsfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; fr_doomed ≔ fr_doomedfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ c_callersc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel; c_mem ≔ c_memc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel; c_fuel ≔ fuel − 1
=
rewrite Hp
ge :
f :
e :
ls :
listname × optionZ
l :
from :
optionname
m :
fuel :
Z
b :
e′ :
Hf :
fuel ≠ 0
Hb :
find_blockl fn_blocksf = Someb
⊢
or_stuck"block" SomeNextc_frame ≔ fr_fn ≔ f; fr_env ≔ e′; fr_locals ≔ fr_localsfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; fr_doomed ≔ fr_doomedfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ c_callersc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel; c_mem ≔ c_memc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enterl from; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel; c_fuel ≔ fuel − 1 = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e′; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel − 1
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Entering a block with no fuel left ends the run, out of fuel.
Explore proof 1 tactics
Initial goal
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
reflexivity
A goto to the target t, polling or not, enters its block from l.
Explore proof 2 tactics
Initial goal
⊢
∀ge : genv f : func e : env ls : listname × optionZ l : name t : target cs : listframe × pending m : mem fuel : Z, stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl [ ] JGotot; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enteredge_labelt Somel; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel
intros
destruct t ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
destruct t ; reflexivity
A branch on v, which reads as the integer n, enters t2's block from l if n is 0, else t1's.
Explore proof 5 tactics
Initial goal
⊢
∀ge : genv f : func e : env ls : listname × optionZ l : name v : value t1 t2 : target cs : listframe × pending m : mem fuel n : Z, value_xge e W v = SomeWIntn → stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl [ ] JBranchv t1 t2; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enteredge_labelif n =? 0 then t2 else t1 Somel; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel
intros ge f e ls l v t1 t2 cs m fuel n Hv
⊢
stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl [ ] JBranchv t1 t2; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Enteredge_labelif n =? 0 then t2 else t1 Somel; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel
unfold step ; cbn [ fr_at c_frame fr_doomed jump_step fr_env ]
rewrite Hv
cbn [ or_stuck ]
destruct n =? 0 , t1 , t2 ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
A return of v, which reads as x at f's return class k: the invocation ends with Retx (return_step).
Explore proof 4 tactics
Initial goal
⊢
∀ge : genv f : func e : env ls : listname × optionZ l : name v : value cs : listframe × pending m : mem fuel : Z k : class x : word, fn_retf = RClassk → value_xge e k v = Somex → stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl [ ] JRetv; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = return_stepc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl [ ] JRetv; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel Retx
intros ge f e ls l v cs m fuel k x Hk Hv
unfold step ; cbn [ fr_at c_frame fr_doomed jump_step fr_env fr_fn ]
rewrite Hk , Hv
⊢
or_stuck"ret" Somereturn_stepc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl [ ] JRetv; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel Retx = return_stepc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl [ ] JRetv; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel Retx
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
A return from a void function: the invocation ends with RetVoid (return_step).
Explore proof 2 tactics
Initial goal
⊢
∀ge : genv f : func e : env ls : listname × optionZ l : name cs : listframe × pending m : mem fuel : Z, stepge c_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl [ ] JRetVoid; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel = return_stepc_frame ≔ fr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl [ ] JRetVoid; c_callers ≔ cs; c_mem ≔ m; c_fuel ≔ fuel RetVoid
intros
⊢
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
reflexivity
An invocation whose named locals end, leaving the memory m', and that has no caller: the run's outcome is o.
Explore proof 4 tactics
Initial goal
intros fr m fuel o m′ H
unfold return_step ; cbn [ c_frame c_mem c_callers ]
rewrite H
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An invocation whose named locals end, leaving the memory m', and whose caller cf reads the result as pd says, binding its environment e': the caller goes on, in m'.
∀ fr cf pd cs m fuel o m′ e′
Explore proof 4 tactics
Initial goal
⊢
∀fr cf : frame pd : pending cs : listframe × pending m : mem fuel : Z o : outcome m′ : mem e′ : env, invalidate_localsfr_localsfr m = Somem′ → pd_convpd = None → returned_envpd_respd o fr_envcf = Somee′ → return_stepc_frame ≔ fr; c_callers ≔ cf, pd :: cs; c_mem ≔ m; c_fuel ≔ fuel o = Nextc_frame ≔ fr_fn ≔ fr_fncf; fr_env ≔ e′; fr_locals ≔ fr_localscf; fr_doomed ≔ fr_doomedcf; fr_at ≔ fr_atcf; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
intros fr cf pd cs m fuel o m′ e′ H Hc He
fr, cf :
pd :
m :
fuel :
Z
o :
m′ :
e′ :
H :
invalidate_localsfr_localsfr m = Somem′
Hc :
pd_convpd = None
He :
returned_envpd_respd o fr_envcf = Somee′
unfold return_step ; cbn [ c_frame c_mem c_callers c_fuel ]
fr, cf :
pd :
m :
fuel :
Z
o :
m′ :
e′ :
H :
invalidate_localsfr_localsfr m = Somem′
Hc :
pd_convpd = None
He :
returned_envpd_respd o fr_envcf = Somee′
⊢
or_stuck"return"
=
rewrite H , Hc , He
fr, cf :
pd :
m :
fuel :
Z
o :
m′ :
e′ :
H :
invalidate_localsfr_localsfr m = Somem′
Hc :
pd_convpd = None
He :
returned_envpd_respd o fr_envcf = Somee′
⊢
or_stuck"return" SomeNextc_frame ≔ fr_fn ≔ fr_fncf; fr_env ≔ e′; fr_locals ≔ fr_localscf; fr_doomed ≔ fr_doomedcf; fr_at ≔ fr_atcf; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel = Nextc_frame ≔ fr_fn ≔ fr_fncf; fr_env ≔ e′; fr_locals ≔ fr_localscf; fr_doomed ≔ fr_doomedcf; fr_at ≔ fr_atcf; c_callers ≔ cs; c_mem ≔ m′; c_fuel ≔ fuel
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros fr cf pd cs m fuel o m′ e′ H Hc He
unfold return_step ; cbn [ c_frame c_mem c_callers c_fuel ]
rewrite H , Hc , He
reflexivity
An invocation with no named locals ends without changing memory.
∀ m
invalidate_locals[ ] m = Somem
Explore proof 1 tactics
Initial goal
⊢
∀m : mem, invalidate_locals[ ] m = Somem
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
reflexivity
Access checks
An access of size bytes at the address a through the capability of the object b, live or not, with the region reg: it passes where the bytes lie in its bounds and a is aligned.
∀ m b reg a size r al
access_resm a Objb size r al = Someok
Explore proof 7 tactics
Initial goal
⊢
∀m : mem b : Z reg : region a size : Z r : rights al : Z, object_regionb m_regionsm = Somereg → b ≤ a → a + size ≤ r_endreg → a mod al = 0 → access_resm a Objb size r al = Someok
intros m b reg a size r al Hr H1 H2 H3
m :
b :
Z
reg :
a, size :
Z
r :
al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
access_resm a Objb size r al = Someok
unfold access_res , cap_access_res
m :
b :
Z
reg :
a, size :
Z
r :
al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
rewrite Hr
m :
b :
Z
reg :
a, size :
Z
r :
al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
replace b ≤? a && a + size ≤? r_endreg with true by symmetry ; apply andb_true_iff ; split ; apply Z.leb_le | apply Z.leb_le ; lia
m :
b :
Z
reg :
a, size :
Z
r :
al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
Somealigned_resa al = Someok
unfold aligned_res
m :
b :
Z
reg :
a, size :
Z
r :
al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
rewrite H3
m :
b :
Z
reg :
a, size :
Z
r :
al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m b reg a size r al Hr H1 H2 H3
unfold access_res , cap_access_res
rewrite Hr
replace b ≤? a && a + size ≤? r_endreg with true by symmetry ; apply andb_true_iff ; split ; apply Z.leb_le | apply Z.leb_le ; lia
unfold aligned_res
rewrite H3
reflexivity
A read through a read-write or read-only capability for the object b with the region reg, of size bytes at a within its bounds and aligned, passes.
∀ m b reg c a size al
access_resm a c size Read al = Someok
Explore proof 8 tactics
Initial goal
intros m b reg c a size al [ ->| -> ] Hr H1 H2 H3 ; exact access_obj_ _ _ _ _ _ _ Hr H1 H2 H3 |
m :
b :
Z
reg :
a, size, al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
access_resm a Rob size Read al = Someok
unfold access_res , cap_access_res
m :
b :
Z
reg :
a, size, al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
rewrite Hr
m :
b :
Z
reg :
a, size, al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
replace b ≤? a && a + size ≤? r_endreg with true by symmetry ; apply andb_true_iff ; split ; apply Z.leb_le | apply Z.leb_le ; lia
m :
b :
Z
reg :
a, size, al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
Somereadonly_access_resRead a al = Someok
cbn [ readonly_access_res ]
m :
b :
Z
reg :
a, size, al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
Somealigned_resa al = Someok
unfold aligned_res
m :
b :
Z
reg :
a, size, al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
rewrite H3
m :
b :
Z
reg :
a, size, al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m b reg c a size al [ ->| -> ] Hr H1 H2 H3 ; exact access_obj_ _ _ _ _ _ _ Hr H1 H2 H3 |
unfold access_res , cap_access_res
rewrite Hr
replace b ≤? a && a + size ≤? r_endreg with true by symmetry ; apply andb_true_iff ; split ; apply Z.leb_le | apply Z.leb_le ; lia
cbn [ readonly_access_res ]
unfold aligned_res
rewrite H3
reflexivity
A check of the pointer p whose access passes: p, proven.
Explore proof 4 tactics
Initial goal
intros m p lo hi r al H
cbn - [ access_res raw_address ]
⊢
SomeOpReschecked_reschk WPtrp m
=
rewrite H
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A half_check of the pointer p, against the proof p1 of the same capability, at a live object b whose bounds hold the bytes, which are aligned, and which ends at or below 2^63: p, proven. Both the full check and the half check's native test pass.
∀ m p1 p bd lo hi r al b reg
object_regionb m_regionsm = Somereg
b ≤ raw_addressptr_addrp lo
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
lo < hi
r_endreg ≤ 2 ^ 63
raw_addressptr_addrp lo mod al = 0
Explore proof 22 tactics
Initial goal
⊢
∀m : mem p1 p : ptr bd : bound lo hi : Z r : rights al b : Z reg : region, ptr_capp1 = Objb → ptr_capp = Objb → object_regionb m_regionsm = Somereg → r_lifereg = Live → b ≤ raw_addressptr_addrp lo → raw_addressptr_addrp lo + hi − lo ≤ r_endreg → lo < hi → r_endreg ≤ 2 ^ 63 → raw_addressptr_addrp lo mod al = 0 → op_resHalfCheckbd lo hi r al A WPtrp1; WPtrp m = SomeOpResRValWPtrp m
intros m p1 p bd lo hi r al b reg H1 H2 Hr Hl Hlo Hhi Hlh Hend Hal
m :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
assert Hacc : access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok by eapply access_obj ; eauto
m :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
cbn - [ access_res raw_address half_passes ]
m :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
⊢
→
else
SomeOpResRUncheckedAlias m
=
rewrite H1 , H2
m :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
⊢
→
else
SomeOpResRUncheckedAlias m
=
cbn [ cap_eqb ]
m :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
⊢
b =? b
→
else
SomeOpResRUncheckedAlias m
=
rewrite Z.eqb_refl , Hacc
m :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
⊢
=
unfold half_passes
m :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
⊢
match let* reg0 ≔ object_regionb m_regionsm in SomeSomehalf_boundbd raw_addressptr_addrp lo hi − lo b r_endreg0 r_lifereg0 && negbrights_eqbr Write && false && raw_addressptr_addrp lo mod al =? 0 with
=
rewrite Hr
m :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
⊢
SomeOpReshalf_resok half_boundbd raw_addressptr_addrp lo hi − lo b r_endreg r_lifereg && negbrights_eqbr Write && false && raw_addressptr_addrp lo mod al =? 0 WPtrp m = SomeOpResRValWPtrp m
cbn [ option_map ]
m :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
⊢
SomeOpReshalf_resok half_boundbd raw_addressptr_addrp lo hi − lo b r_endreg r_lifereg && negbrights_eqbr Write && false && raw_addressptr_addrp lo mod al =? 0 WPtrp m = SomeOpResRValWPtrp m
replace half_boundbd raw_addressptr_addrp lo hi − lo b r_endreg r_lifereg with true
2 openm :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
focused goal
m :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
⊢
true = half_boundbd raw_addressptr_addrp lo hi − lo b r_endreg r_lifereg
–rewrite Hal , Z.eqb_refl
2 openm :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
deferred goal
m :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
⊢
true = half_boundbd raw_addressptr_addrp lo hi − lo b r_endreg r_lifereg
destruct r ; reflexivity
deferred goal
m :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
⊢
true = half_boundbd raw_addressptr_addrp lo hi − lo b r_endreg r_lifereg
–symmetry
m :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
⊢
half_boundbd raw_addressptr_addrp lo hi − lo b r_endreg r_lifereg = true
unfold half_bound
m :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
⊢
match bd with
⇒
⇒
=
true
rewrite Hl
m :
p1, p :
bd :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
⊢
match bd with
⇒
=
true
destruct bd ; apply Z.leb_le ; lia |
m :
p1, p :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
⊢
=
true
assert Hn : 0 ≤ raw_addressptr_addrp lo < 2 ^ 63
2 openm :
p1, p :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
⊢
0 ≤ raw_addressptr_addrp lo < 2 ^ 63
focused goal
m :
p1, p :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
Hn :
0 ≤ raw_addressptr_addrp lo < 2 ^ 63
⊢
=
true
{pose proof Z.mod_pos_boundptr_addrp + lo 2 ^ 64 ltac:lia as Hm
2 openm :
p1, p :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
Hm :
0 ≤ ptr_addrp + lo mod 2 ^ 64 < 2 ^ 64
⊢
0 ≤ raw_addressptr_addrp lo < 2 ^ 63
deferred goal
m :
p1, p :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
Hn :
0 ≤ raw_addressptr_addrp lo < 2 ^ 63
⊢
=
true
fold raw_addressptr_addrp lo in Hm
2 openm :
p1, p :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
Hm :
0 ≤ raw_addressptr_addrp lo < 2 ^ 64
⊢
0 ≤ raw_addressptr_addrp lo < 2 ^ 63
deferred goal
m :
p1, p :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
Hn :
0 ≤ raw_addressptr_addrp lo < 2 ^ 63
⊢
=
true
lia
deferred goal
m :
p1, p :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
Hn :
0 ≤ raw_addressptr_addrp lo < 2 ^ 63
⊢
=
true
replace 2 ^ 63 ≤? raw_addressptr_addrp lo with false by symmetry ; apply Z.leb_gt ; lia
m :
p1, p :
lo, hi :
Z
r :
al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok
Hn :
0 ≤ raw_addressptr_addrp lo < 2 ^ 63
⊢
b ≤? raw_addressptr_addrp lo = true
apply Z.leb_le ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m p1 p bd lo hi r al b reg H1 H2 Hr Hl Hlo Hhi Hlh Hend Hal
assert Hacc : access_resm raw_addressptr_addrp lo Objb hi − lo r al = Someok by eapply access_obj ; eauto
cbn - [ access_res raw_address half_passes ]
rewrite H1 , H2
cbn [ cap_eqb ]
rewrite Z.eqb_refl , Hacc
unfold half_passes
rewrite Hr
cbn [ option_map ]
replace half_boundbd raw_addressptr_addrp lo hi − lo b r_endreg r_lifereg with true
–rewrite Hal , Z.eqb_refl
destruct r ; reflexivity
–symmetry
unfold half_bound
rewrite Hl
destruct bd ; apply Z.leb_le ; lia |
assert Hn : 0 ≤ raw_addressptr_addrp lo < 2 ^ 63
{pose proof Z.mod_pos_boundptr_addrp + lo 2 ^ 64 ltac:lia as Hm
fold raw_addressptr_addrp lo in Hm
lia
replace 2 ^ 63 ≤? raw_addressptr_addrp lo with false by symmetry ; apply Z.leb_gt ; lia
apply Z.leb_le ; lia
A read half_check of the pointer p, against the proof p1 of the same capability, an object's or a read-only object's, at a live object b whose bounds hold the bytes, which are aligned, and which ends at or below 2^63: p, proven. A read-only capability passes a read's native test as an object's does.
∀ m p1 p bd lo hi al b reg
object_regionb m_regionsm = Somereg
b ≤ raw_addressptr_addrp lo
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
lo < hi
r_endreg ≤ 2 ^ 63
raw_addressptr_addrp lo mod al = 0
Explore proof 23 tactics
Initial goal
⊢
∀m : mem p1 p : ptr bd : bound lo hi al b : Z reg : region, ptr_capp1 = ptr_capp → ptr_capp = Objb ∨ ptr_capp = Rob → object_regionb m_regionsm = Somereg → r_lifereg = Live → b ≤ raw_addressptr_addrp lo → raw_addressptr_addrp lo + hi − lo ≤ r_endreg → lo < hi → r_endreg ≤ 2 ^ 63 → raw_addressptr_addrp lo mod al = 0 → op_resHalfCheckbd lo hi Read al A WPtrp1; WPtrp m = SomeOpResRValWPtrp m
intros m p1 p bd lo hi al b reg E Hc Hr Hl Hlo Hhi Hlh Hend Hal
m :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
destruct Hc as Hc | Hc ; rewrite Hc in E ; exact op_half_check_ _ _ _ _ _ Read _ _ _ E Hc Hr Hl Hlo Hhi Hlh Hend Hal |
m :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
assert Hacc : access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok by eapply access_read ; eauto
m :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
cbn - [ access_res raw_address half_passes ]
m :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
⊢
→
else
SomeOpResRUncheckedAlias m
=
rewrite E , Hc
m :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
⊢
→
else
SomeOpResRUncheckedAlias m
=
cbn [ cap_eqb ]
m :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
⊢
b =? b
→
else
SomeOpResRUncheckedAlias m
=
rewrite Z.eqb_refl , Hacc
m :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
⊢
=
unfold half_passes
m :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
⊢
match let* reg0 ≔ object_regionb m_regionsm in SomeSomehalf_boundbd raw_addressptr_addrp lo hi − lo b r_endreg0 r_lifereg0 && negbrights_eqbRead Write && true && raw_addressptr_addrp lo mod al =? 0 with
=
rewrite Hr
m :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
⊢
SomeOpReshalf_resok half_boundbd raw_addressptr_addrp lo hi − lo b r_endreg r_lifereg && negbrights_eqbRead Write && true && raw_addressptr_addrp lo mod al =? 0 WPtrp m = SomeOpResRValWPtrp m
cbn [ option_map ]
m :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
⊢
SomeOpReshalf_resok half_boundbd raw_addressptr_addrp lo hi − lo b r_endreg r_lifereg && negbrights_eqbRead Write && true && raw_addressptr_addrp lo mod al =? 0 WPtrp m = SomeOpResRValWPtrp m
replace half_boundbd raw_addressptr_addrp lo hi − lo b r_endreg r_lifereg with true
2 openm :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
focused goal
m :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
⊢
true = half_boundbd raw_addressptr_addrp lo hi − lo b r_endreg r_lifereg
–rewrite Hal , Z.eqb_refl
2 openm :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
deferred goal
m :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
⊢
true = half_boundbd raw_addressptr_addrp lo hi − lo b r_endreg r_lifereg
reflexivity
deferred goal
m :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
⊢
true = half_boundbd raw_addressptr_addrp lo hi − lo b r_endreg r_lifereg
–symmetry
m :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
⊢
half_boundbd raw_addressptr_addrp lo hi − lo b r_endreg r_lifereg = true
unfold half_bound
m :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
⊢
match bd with
⇒
⇒
=
true
rewrite Hl
m :
p1, p :
bd :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
⊢
match bd with
⇒
=
true
destruct bd ; apply Z.leb_le ; lia |
m :
p1, p :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
⊢
=
true
assert Hn : 0 ≤ raw_addressptr_addrp lo < 2 ^ 63
2 openm :
p1, p :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
⊢
0 ≤ raw_addressptr_addrp lo < 2 ^ 63
focused goal
m :
p1, p :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
Hn :
0 ≤ raw_addressptr_addrp lo < 2 ^ 63
⊢
=
true
{pose proof Z.mod_pos_boundptr_addrp + lo 2 ^ 64 ltac:lia as Hm
2 openm :
p1, p :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
Hm :
0 ≤ ptr_addrp + lo mod 2 ^ 64 < 2 ^ 64
⊢
0 ≤ raw_addressptr_addrp lo < 2 ^ 63
deferred goal
m :
p1, p :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
Hn :
0 ≤ raw_addressptr_addrp lo < 2 ^ 63
⊢
=
true
fold raw_addressptr_addrp lo in Hm
2 openm :
p1, p :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
Hm :
0 ≤ raw_addressptr_addrp lo < 2 ^ 64
⊢
0 ≤ raw_addressptr_addrp lo < 2 ^ 63
deferred goal
m :
p1, p :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
Hn :
0 ≤ raw_addressptr_addrp lo < 2 ^ 63
⊢
=
true
lia
deferred goal
m :
p1, p :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
Hn :
0 ≤ raw_addressptr_addrp lo < 2 ^ 63
⊢
=
true
replace 2 ^ 63 ≤? raw_addressptr_addrp lo with false by symmetry ; apply Z.leb_gt ; lia
m :
p1, p :
lo, hi, al, b :
Z
reg :
Hr :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ raw_addressptr_addrp lo
Hhi :
raw_addressptr_addrp lo + hi − lo ≤ r_endreg
Hlh :
lo < hi
Hend :
r_endreg ≤ 2 ^ 63
Hal :
raw_addressptr_addrp lo mod al = 0
Hacc :
access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok
Hn :
0 ≤ raw_addressptr_addrp lo < 2 ^ 63
⊢
b ≤? raw_addressptr_addrp lo = true
apply Z.leb_le ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m p1 p bd lo hi al b reg E Hc Hr Hl Hlo Hhi Hlh Hend Hal
destruct Hc as Hc | Hc ; rewrite Hc in E ; exact op_half_check_ _ _ _ _ _ Read _ _ _ E Hc Hr Hl Hlo Hhi Hlh Hend Hal |
assert Hacc : access_resm raw_addressptr_addrp lo Rob hi − lo Read al = Someok by eapply access_read ; eauto
cbn - [ access_res raw_address half_passes ]
rewrite E , Hc
cbn [ cap_eqb ]
rewrite Z.eqb_refl , Hacc
unfold half_passes
rewrite Hr
cbn [ option_map ]
replace half_boundbd raw_addressptr_addrp lo hi − lo b r_endreg r_lifereg with true
–rewrite Hal , Z.eqb_refl
reflexivity
–symmetry
unfold half_bound
rewrite Hl
destruct bd ; apply Z.leb_le ; lia |
assert Hn : 0 ≤ raw_addressptr_addrp lo < 2 ^ 63
{pose proof Z.mod_pos_boundptr_addrp + lo 2 ^ 64 ltac:lia as Hm
fold raw_addressptr_addrp lo in Hm
lia
replace 2 ^ 63 ≤? raw_addressptr_addrp lo with false by symmetry ; apply Z.leb_gt ; lia
apply Z.leb_le ; lia
A renew of the pointer p, against the proof p1 of the same capability, whose own access check passes: p, proven, as the check it replaced would have proven it.
Explore proof 6 tactics
Initial goal
intros m p1 p lo hi r al E H
cbn - [ access_res raw_address cap_eqb ]
⊢
→
else
SomeOpResRUncheckedAlias m
=
rewrite E
⊢
→
else
SomeOpResRUncheckedAlias m
=
replace cap_eqbptr_capp ptr_capp with true by symmetry ; destruct ptr_capp ; cbn ; try apply Z.eqb_refl ; try apply term_eqb_refl ; reflexivity
⊢
=
rewrite H
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m p1 p lo hi r al E H
cbn - [ access_res raw_address cap_eqb ]
rewrite E
replace cap_eqbptr_capp ptr_capp with true by symmetry ; destruct ptr_capp ; cbn ; try apply Z.eqb_refl ; try apply term_eqb_refl ; reflexivity
rewrite H
reflexivity
A raw load of 8 bytes at offset off from the proven pointer p, whose read access passes: the little-endian integer there.
∀ m k p off
access_resm raw_addressptr_addrp off ptr_capp 8 Read 1 = Someok
op_resRawLoadLdL off k WPtrp m = SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 8 m
Explore proof 8 tactics
Initial goal
⊢
∀m : mem k : class p : ptr off : Z, access_resm raw_addressptr_addrp off ptr_capp 8 Read 1 = Someok → op_resRawLoadLdL off k WPtrp m = SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 8 m
intros m k p off H
⊢
op_resRawLoadLdL off k WPtrp m = SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 8 m
assert E : op_resRawLoadLdL off k WPtrp m = op_res_intRawLoadLdL off k WPtrp m by destruct k ; reflexivity
rewrite E
⊢
op_res_intRawLoadLdL off k WPtrp m = SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 8 m
cbn - [ access_res raw_address load_bytes ]
⊢
unfold int_load_res
⊢
cbn - [ access_res raw_address load_bytes ]
⊢
rewrite H
⊢
SomeOpResraw_resRValWIntload_bytesm raw_addressptr_addrp off 8 m = SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 8 m
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m k p off H
assert E : op_resRawLoadLdL off k WPtrp m = op_res_intRawLoadLdL off k WPtrp m by destruct k ; reflexivity
rewrite E
cbn - [ access_res raw_address load_bytes ]
unfold int_load_res
cbn - [ access_res raw_address load_bytes ]
rewrite H
reflexivity
A raw load of the one-byte narrow type n at offset off from the proven pointer p, whose read access passes: the byte there, extended to the class k.
∀ m k n p off
fstnarrow_typen = 1
access_resm raw_addressptr_addrp off ptr_capp 1 Read 1 = Someok
Explore proof 12 tactics
Initial goal
intros m k n p off Hn H
assert E : op_resRawLoadLdNarrown off k WPtrp m = op_res_intRawLoadLdNarrown off k WPtrp m by destruct k ; reflexivity
m :
k :
n :
p :
off :
Z
Hn :
fstnarrow_typen = 1
H :
access_resm raw_addressptr_addrp off ptr_capp 1 Read 1 = Someok
assert Hl : load_bytesm raw_addressptr_addrp off 1 = m_bytesm raw_addressptr_addrp off
2 openm :
k :
n :
p :
off :
Z
Hn :
fstnarrow_typen = 1
H :
access_resm raw_addressptr_addrp off ptr_capp 1 Read 1 = Someok
⊢
load_bytesm raw_addressptr_addrp off 1 = m_bytesm raw_addressptr_addrp off
focused goal
m :
k :
n :
p :
off :
Z
Hn :
fstnarrow_typen = 1
H :
access_resm raw_addressptr_addrp off ptr_capp 1 Read 1 = Someok
Hl :
load_bytesm raw_addressptr_addrp off 1 = m_bytesm raw_addressptr_addrp off
{unfold load_bytes
2 openm :
k :
n :
p :
off :
Z
Hn :
fstnarrow_typen = 1
H :
access_resm raw_addressptr_addrp off ptr_capp 1 Read 1 = Someok
⊢
fix go n0 : nat acc : Z {struct n0} : Z ≔
match n0 with
0%nat
⇒
acc
Z.to_nat1 0
=
m_bytesm raw_addressptr_addrp off
deferred goal
m :
k :
n :
p :
off :
Z
Hn :
fstnarrow_typen = 1
H :
access_resm raw_addressptr_addrp off ptr_capp 1 Read 1 = Someok
Hl :
load_bytesm raw_addressptr_addrp off 1 = m_bytesm raw_addressptr_addrp off
change Z.to_nat1 with 1%nat
2 openm :
k :
n :
p :
off :
Z
Hn :
fstnarrow_typen = 1
H :
access_resm raw_addressptr_addrp off ptr_capp 1 Read 1 = Someok
⊢
fix go n0 : nat acc : Z {struct n0} : Z ≔
match n0 with
0%nat
⇒
acc
1%nat 0
=
m_bytesm raw_addressptr_addrp off
deferred goal
m :
k :
n :
p :
off :
Z
Hn :
fstnarrow_typen = 1
H :
access_resm raw_addressptr_addrp off ptr_capp 1 Read 1 = Someok
Hl :
load_bytesm raw_addressptr_addrp off 1 = m_bytesm raw_addressptr_addrp off
cbn - [ raw_address ]
2 openm :
k :
n :
p :
off :
Z
Hn :
fstnarrow_typen = 1
H :
access_resm raw_addressptr_addrp off ptr_capp 1 Read 1 = Someok
⊢
m_bytesm raw_addressptr_addrp off + 0 = m_bytesm raw_addressptr_addrp off
deferred goal
m :
k :
n :
p :
off :
Z
Hn :
fstnarrow_typen = 1
H :
access_resm raw_addressptr_addrp off ptr_capp 1 Read 1 = Someok
Hl :
load_bytesm raw_addressptr_addrp off 1 = m_bytesm raw_addressptr_addrp off
now rewrite Z.add_0_r
deferred goal
m :
k :
n :
p :
off :
Z
Hn :
fstnarrow_typen = 1
H :
access_resm raw_addressptr_addrp off ptr_capp 1 Read 1 = Someok
Hl :
load_bytesm raw_addressptr_addrp off 1 = m_bytesm raw_addressptr_addrp off
rewrite E
m :
k :
n :
p :
off :
Z
Hn :
fstnarrow_typen = 1
H :
access_resm raw_addressptr_addrp off ptr_capp 1 Read 1 = Someok
Hl :
load_bytesm raw_addressptr_addrp off 1 = m_bytesm raw_addressptr_addrp off
cbn - [ access_res raw_address load_bytes narrow_type extended ]
m :
k :
n :
p :
off :
Z
Hn :
fstnarrow_typen = 1
H :
access_resm raw_addressptr_addrp off ptr_capp 1 Read 1 = Someok
Hl :
load_bytesm raw_addressptr_addrp off 1 = m_bytesm raw_addressptr_addrp off
⊢
=
unfold int_load_res
m :
k :
n :
p :
off :
Z
Hn :
fstnarrow_typen = 1
H :
access_resm raw_addressptr_addrp off ptr_capp 1 Read 1 = Someok
Hl :
load_bytesm raw_addressptr_addrp off 1 = m_bytesm raw_addressptr_addrp off
⊢
let* r ≔
None
⇒
None
in
=
rewrite Hn , H , Hl
m :
k :
n :
p :
off :
Z
Hn :
fstnarrow_typen = 1
H :
access_resm raw_addressptr_addrp off ptr_capp 1 Read 1 = Someok
Hl :
load_bytesm raw_addressptr_addrp off 1 = m_bytesm raw_addressptr_addrp off
destruct extendedn k _ ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m k n p off Hn H
assert E : op_resRawLoadLdNarrown off k WPtrp m = op_res_intRawLoadLdNarrown off k WPtrp m by destruct k ; reflexivity
assert Hl : load_bytesm raw_addressptr_addrp off 1 = m_bytesm raw_addressptr_addrp off
rewrite E
cbn - [ access_res raw_address load_bytes narrow_type extended ]
unfold int_load_res
rewrite Hn , H , Hl
destruct extendedn k _ ; reflexivity
A raw pointer load at offset off from the proven pointer p, whose 8-byte read access passes and whose protocol es loads x: x.
∀ m p off es x
access_resm raw_addressptr_addrp off ptr_capp 8 Read 8 = Someok
pointer_load_effectsm raw_addressptr_addrp off es = Somex
Explore proof 6 tactics
Initial goal
⊢
∀m : mem p : ptr off : Z es : listeffect x : ptr, access_resm raw_addressptr_addrp off ptr_capp 8 Read 8 = Someok → pointer_load_effectsm raw_addressptr_addrp off es = Somex → op_resRawLoadPointeroff es P WPtrp m = SomeOpResRValWPtrx m
intros m p off es x H He
m :
p :
off :
Z
es :
listeffect
x :
H :
access_resm raw_addressptr_addrp off ptr_capp 8 Read 8 = Someok
He :
pointer_load_effectsm raw_addressptr_addrp off es = Somex
cbn - [ access_res raw_address pointer_load_effects ]
m :
p :
off :
Z
es :
listeffect
x :
H :
access_resm raw_addressptr_addrp off ptr_capp 8 Read 8 = Someok
He :
pointer_load_effectsm raw_addressptr_addrp off es = Somex
⊢
None
⇒
None
=
rewrite H
m :
p :
off :
Z
es :
listeffect
x :
H :
access_resm raw_addressptr_addrp off ptr_capp 8 Read 8 = Someok
He :
pointer_load_effectsm raw_addressptr_addrp off es = Somex
⊢
=
cbn - [ raw_address pointer_load_effects ]
m :
p :
off :
Z
es :
listeffect
x :
H :
access_resm raw_addressptr_addrp off ptr_capp 8 Read 8 = Someok
He :
pointer_load_effectsm raw_addressptr_addrp off es = Somex
⊢
=
rewrite He
m :
p :
off :
Z
es :
listeffect
x :
H :
access_resm raw_addressptr_addrp off ptr_capp 8 Read 8 = Someok
He :
pointer_load_effectsm raw_addressptr_addrp off es = Somex
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m p off es x H He
cbn - [ access_res raw_address pointer_load_effects ]
rewrite H
cbn - [ raw_address pointer_load_effects ]
rewrite He
reflexivity
∀ m a
pointer_load_effectsm a AuxRead; LowerResolve; AddressRead = SomemkPtrload_bytesm a 8 aux_atm a
Explore proof 1 tactics
Initial goal
⊢
∀m : mem a : Z, pointer_load_effectsm a AuxRead; LowerResolve; AddressRead = Someptr_addr ≔ load_bytesm a 8; ptr_cap ≔ aux_atm a
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
reflexivity
The store protocol nanofil emits for a plain pointer store writes the capability to the aux, then the address to the bytes.
∀ m a x
pointer_store_effectsa x m AuxEnsure; LowerBarrier; RootedReload; LowerWrite; AddressWrite = Somestore_bytesstore_auxm a ptr_capx a 8 ptr_addrx
Explore proof 1 tactics
Initial goal
⊢
∀m : mem a : Z x : ptr, pointer_store_effectsa x m AuxEnsure; LowerBarrier; RootedReload; LowerWrite; AddressWrite = Somestore_bytesstore_auxm a ptr_capx a 8 ptr_addrx
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
reflexivity
A read of size bytes at the address a through the read-only capability of the object b, with the region reg: it passes where the bytes lie in its bounds and a is aligned, as access_obj for a read.
∀ m b reg a size al
access_resm a Rob size Read al = Someok
Explore proof 7 tactics
Initial goal
⊢
∀m : mem b : Z reg : region a size al : Z, object_regionb m_regionsm = Somereg → b ≤ a → a + size ≤ r_endreg → a mod al = 0 → access_resm a Rob size Read al = Someok
intros m b reg a size al Hr H1 H2 H3
m :
b :
Z
reg :
a, size, al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
access_resm a Rob size Read al = Someok
unfold access_res , cap_access_res
m :
b :
Z
reg :
a, size, al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
rewrite Hr
m :
b :
Z
reg :
a, size, al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
replace b ≤? a && a + size ≤? r_endreg with true by symmetry ; apply andb_true_iff ; split ; apply Z.leb_le | apply Z.leb_le ; lia
m :
b :
Z
reg :
a, size, al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
Somereadonly_access_resRead a al = Someok
unfold readonly_access_res , aligned_res
m :
b :
Z
reg :
a, size, al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
rewrite H3
m :
b :
Z
reg :
a, size, al :
Z
Hr :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + size ≤ r_endreg
H3 :
a mod al = 0
⊢
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m b reg a size al Hr H1 H2 H3
unfold access_res , cap_access_res
rewrite Hr
replace b ≤? a && a + size ≤? r_endreg with true by symmetry ; apply andb_true_iff ; split ; apply Z.leb_le | apply Z.leb_le ; lia
unfold readonly_access_res , aligned_res
rewrite H3
reflexivity
A store of the integer v as a long at the address a through the capability c, whose 8-byte write access passes: its bytes.
Explore proof 4 tactics
Initial goal
⊢
∀m : mem a : Z c : cap v : Z, access_resm a c 8 Write 1 = Someok → store_resWl m a c WIntv = Someok, store_bytesm a 8 v
intros m a c v H
⊢
store_resWl m a c WIntv = Someok, store_bytesm a 8 v
cbn - [ access_res store_bytes ]
⊢
rewrite H
⊢
Someok, store_bytesm a 8 v = Someok, store_bytesm a 8 v
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.