rocq/theories/Chain.v
Campaign 3's reuse forms, part one: what a frame may read off the single definitions that dominate its point (formal.md, Campaign 3; rocq.md, Reading single definitions).
Single.v proves that every replayable single definition whose site dominates a frame's point replays: the name still holds what its instruction made. This file turns that into the facts the reuse forms' rules need: offset intervals, the elements of a guard chain, and the distance between two pointers. From them it proves the first reuse form, a raw access covered by the hull of two live facts, never unchecked along any run.
Decisions
| Decision | Why |
|---|---|
| "dominates the point" is the predicate Interval.v walks | it is closed under single-definition operands (use_dominated), and what dominates replays (scope_holds) |
Interval.v's hypothesis speaks of iv_op lets at an integer class | a check's proof or a float sum does not compute by alu; no derivation walks through one |
guard_chain and pointer_distance are rewritten by equations, never unfolded in a hypothesis | unfolding makes the kernel compare two 64-deep unfoldings, and Qed takes minutes |
| a write through the hull needs some write check of the capability, not of the two bounding spans | hull_covered/7 takes write rights from any span; a passed write check means the capability is not read-only |
the facts' pointers dominating the point is Invariant.v's (live_dom), not a hypothesis | inside a block it is use_dominated; over a block's entry it is dom_meet |
HullR carries runs between two instances of MachineR | Persistence.v and Single.v each instantiate it, and mstep is an inductive, new in each instance |
From Stdlib Require Import String ZArith List Bool Lia Relations
From Nanofil Require Import Term Maps Syntax Cfg Values Memory Runtime Ops Semantics Machine Validate Dominance Interval Sites Identity Coverage Walk Invariant Persistence Single Evidence
Import ListNotations
Open Scope Z_scope
A replayed definition holds
A let n of an op o that intervals walk through (iv_op), at an integer class k, that steps and continues, computed its result from its operands as let_holds says, reading them in the frame where it ran (inst_result/5, op_res/7).
Explore proof 17 tactics
Initial goal
intros ge fr m n k o args e1 l1 m1 Ho Hk H
assert Hs : special_leto = false by destruct o ; try discriminate Ho ; reflexivity
rewrite inst_step_let_ _ _ _ _ _ _ Hs in H
ge :
fr :
m :
Memory.mem
n :
k :
o :
args :
listvalue
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
Ho :
iv_opo = true
Hk :
class_bitsk ≠ None
H :
Hs :
special_leto = false
cbv zeta in H
ge :
fr :
m :
Memory.mem
n :
k :
o :
args :
listvalue
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
Ho :
iv_opo = true
Hk :
class_bitsk ≠ None
H :
Hs :
special_leto = false
destruct op_arg_classeso k as cls | eqn: Ec ; | discriminate H
ge :
fr :
m :
Memory.mem
n :
k :
o :
args :
listvalue
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
Ho :
iv_opo = true
Hk :
class_bitsk ≠ None
cls :
listclass
Ec :
op_arg_classeso k = Somecls
H :
Hs :
special_leto = false
destruct map2_option_ cls args as xs | eqn: Ex ; | discriminate H
ge :
fr :
m :
Memory.mem
n :
k :
o :
args :
listvalue
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
Ho :
iv_opo = true
Hk :
class_bitsk ≠ None
cls :
listclass
Ec :
op_arg_classeso k = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
H :
Hs :
special_leto = false
destruct op_reso k xs m as r m′ | why | q kont | eqn: Er ; try discriminate H
ge :
fr :
m :
Memory.mem
n :
k :
o :
args :
listvalue
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
Ho :
iv_opo = true
Hk :
class_bitsk ≠ None
cls :
listclass
Ec :
op_arg_classeso k = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
m′ :
Memory.mem
Hs :
special_leto = false
destruct r as x | why | why ; simpl in H ; try discriminate H
ge :
fr :
m :
Memory.mem
n :
k :
o :
args :
listvalue
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
Ho :
iv_opo = true
Hk :
class_bitsk ≠ None
cls :
listclass
Ec :
op_arg_classeso k = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Hs :
special_leto = false
injection H as ← _ _
ge :
fr :
m :
Memory.mem
n :
k :
o :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Ho :
iv_opo = true
Hk :
class_bitsk ≠ None
cls :
listclass
Ec :
op_arg_classeso k = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Hs :
special_leto = false
assert Hn : lookupn putn x fr_envfr = Somex by rewrite lookup_put , name_eqb_refl ; reflexivity
ge :
fr :
m :
Memory.mem
n :
k :
o :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Ho :
iv_opo = true
Hk :
class_bitsk ≠ None
cls :
listclass
Ec :
op_arg_classeso k = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Hs :
special_leto = false
destruct k ; try exfalso ; apply Hk ; reflexivity ; destruct o ; try discriminate Ho ; unfold op_res , op_res_int in Er ; simpl in Er ; cases Er ; inversion Er ; subst
18 openge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesAdd W = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letAdd = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesSub W = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letSub = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesMul W = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letMul = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesUrem W = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letUrem = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesAnd W = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letAnd = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesShl W = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letShl = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesCopy W = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
match xs with
[ ]
⇒
None
x
⇒
Somex
x :: _ :: _
⇒
None
=
Somex
Hs :
special_letCopy = false
focused goal
ge :
fr :
n :
t :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesExtt W = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Hs :
special_letExtt = false
focused goal
ge :
fr :
n :
t :
off :
Z
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesRawLoadt off W = Somecls
p :
Ex :
map2_optionvalue_xge fr_envfr cls args = SomeWPtrp
x :
m′ :
Memory.mem
Heqo :
int_load_rest W m′ raw_addressptr_addrp off ptr_capp = Somer
Hs :
special_letRawLoadt off = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesAdd L = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letAdd = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesSub L = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letSub = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesMul L = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letMul = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesUrem L = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letUrem = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesAnd L = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letAnd = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesShl L = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letShl = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesCopy L = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
match xs with
[ ]
⇒
None
x
⇒
Somex
x :: _ :: _
⇒
None
=
Somex
Hs :
special_letCopy = false
focused goal
ge :
fr :
n :
t :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesExtt L = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Hs :
special_letExtt = false
focused goal
ge :
fr :
n :
t :
off :
Z
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesRawLoadt off L = Somecls
p :
Ex :
map2_optionvalue_xge fr_envfr cls args = SomeWPtrp
x :
m′ :
Memory.mem
Heqo :
int_load_rest L m′ raw_addressptr_addrp off ptr_capp = Somer
Hs :
special_letRawLoadt off = false
all: unfold let_holds
18 openge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesAdd W = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letAdd = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesSub W = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letSub = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesMul W = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letMul = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesUrem W = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letUrem = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesAnd W = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letAnd = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesShl W = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letShl = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesCopy W = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
match xs with
[ ]
⇒
None
x
⇒
Somex
x :: _ :: _
⇒
None
=
Somex
Hs :
special_letCopy = false
focused goal
ge :
fr :
n :
t :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesExtt W = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Hs :
special_letExtt = false
focused goal
ge :
fr :
n :
t :
off :
Z
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesRawLoadt off W = Somecls
p :
Ex :
map2_optionvalue_xge fr_envfr cls args = SomeWPtrp
x :
m′ :
Memory.mem
Heqo :
int_load_rest W m′ raw_addressptr_addrp off ptr_capp = Somer
Hs :
special_letRawLoadt off = false
⊢
match t with
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesAdd L = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letAdd = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesSub L = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letSub = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesMul L = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letMul = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesUrem L = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letUrem = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesAnd L = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letAnd = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesShl L = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
Hs :
special_letShl = false
focused goal
ge :
fr :
n :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesCopy L = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Heqo :
match xs with
[ ]
⇒
None
x
⇒
Somex
x :: _ :: _
⇒
None
=
Somex
Hs :
special_letCopy = false
focused goal
ge :
fr :
n :
t :
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesExtt L = Somecls
xs :
listword
Ex :
map2_optionvalue_xge fr_envfr cls args = Somexs
x :
m′ :
Memory.mem
Hs :
special_letExtt = false
focused goal
ge :
fr :
n :
t :
off :
Z
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesRawLoadt off L = Somecls
p :
Ex :
map2_optionvalue_xge fr_envfr cls args = SomeWPtrp
x :
m′ :
Memory.mem
Heqo :
int_load_rest L m′ raw_addressptr_addrp off ptr_capp = Somer
Hs :
special_letRawLoadt off = false
⊢
match t with
all: first exists cls, xs, x ; auto | idtac
2 openge :
fr :
n :
t :
off :
Z
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesRawLoadt off W = Somecls
p :
Ex :
map2_optionvalue_xge fr_envfr cls args = SomeWPtrp
x :
m′ :
Memory.mem
Heqo :
int_load_rest W m′ raw_addressptr_addrp off ptr_capp = Somer
Hs :
special_letRawLoadt off = false
⊢
match t with
focused goal
ge :
fr :
n :
t :
off :
Z
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesRawLoadt off L = Somecls
p :
Ex :
map2_optionvalue_xge fr_envfr cls args = SomeWPtrp
x :
m′ :
Memory.mem
Heqo :
int_load_rest L m′ raw_addressptr_addrp off ptr_capp = Somer
Hs :
special_letRawLoadt off = false
⊢
match t with
all: destruct t ; try discriminate Ho
2 openge :
fr :
n :
t :
off :
Z
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesRawLoadLdNarrowt off W = Somecls
p :
Ex :
map2_optionvalue_xge fr_envfr cls args = SomeWPtrp
x :
m′ :
Memory.mem
Heqo :
int_load_resLdNarrowt W m′ raw_addressptr_addrp off ptr_capp = Somer
Hs :
special_letRawLoadLdNarrowt off = false
focused goal
ge :
fr :
n :
t :
off :
Z
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesRawLoadLdNarrowt off L = Somecls
p :
Ex :
map2_optionvalue_xge fr_envfr cls args = SomeWPtrp
x :
m′ :
Memory.mem
Heqo :
int_load_resLdNarrowt L m′ raw_addressptr_addrp off ptr_capp = Somer
Hs :
special_letRawLoadLdNarrowt off = false
all: match goal withHl : int_load_res_ _ _ _ _ = Some_ |- _⇒unfold int_load_res in Hl ; cases Hl ; inversion Hl ; substend
6 openge :
fr :
n :
t :
off :
Z
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesRawLoadLdNarrowt off W = Somecls
p :
Ex :
map2_optionvalue_xge fr_envfr cls args = SomeWPtrp
x :
m′ :
Memory.mem
w :
x0 :
unit
Heqo0 :
access_resm′ raw_addressptr_addrp off ptr_capp fstnarrow_typet Read 1 = SomeRValx0
Heqo1 :
extendedt W load_bytesm′ raw_addressptr_addrp off fstnarrow_typet = Somew
Hs :
special_letRawLoadLdNarrowt off = false
focused goal
ge :
fr :
n :
t :
off :
Z
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesRawLoadLdNarrowt off W = Somecls
p :
Ex :
map2_optionvalue_xge fr_envfr cls args = SomeWPtrp
x :
m′ :
Memory.mem
r1 :
Heqo0 :
access_resm′ raw_addressptr_addrp off ptr_capp fstnarrow_typet Read 1 = SomeRTrapr1
Hs :
special_letRawLoadLdNarrowt off = false
focused goal
ge :
fr :
n :
t :
off :
Z
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsW ≠ None
cls :
listclass
Ec :
op_arg_classesRawLoadLdNarrowt off W = Somecls
p :
Ex :
map2_optionvalue_xge fr_envfr cls args = SomeWPtrp
x :
m′ :
Memory.mem
r1 :
Er :
SomeOpResraw_resRUncheckedr1 m′ = SomeOpResRValx m′
Heqo0 :
access_resm′ raw_addressptr_addrp off ptr_capp fstnarrow_typet Read 1 = SomeRUncheckedr1
Heqo :
SomeRUncheckedr1 = SomeRUncheckedr1
Hs :
special_letRawLoadLdNarrowt off = false
H0 :
raw_resRUncheckedr1 = RValx
focused goal
ge :
fr :
n :
t :
off :
Z
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesRawLoadLdNarrowt off L = Somecls
p :
Ex :
map2_optionvalue_xge fr_envfr cls args = SomeWPtrp
x :
m′ :
Memory.mem
w :
x0 :
unit
Heqo0 :
access_resm′ raw_addressptr_addrp off ptr_capp fstnarrow_typet Read 1 = SomeRValx0
Heqo1 :
extendedt L load_bytesm′ raw_addressptr_addrp off fstnarrow_typet = Somew
Hs :
special_letRawLoadLdNarrowt off = false
focused goal
ge :
fr :
n :
t :
off :
Z
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesRawLoadLdNarrowt off L = Somecls
p :
Ex :
map2_optionvalue_xge fr_envfr cls args = SomeWPtrp
x :
m′ :
Memory.mem
r1 :
Heqo0 :
access_resm′ raw_addressptr_addrp off ptr_capp fstnarrow_typet Read 1 = SomeRTrapr1
Hs :
special_letRawLoadLdNarrowt off = false
focused goal
ge :
fr :
n :
t :
off :
Z
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Hk :
class_bitsL ≠ None
cls :
listclass
Ec :
op_arg_classesRawLoadLdNarrowt off L = Somecls
p :
Ex :
map2_optionvalue_xge fr_envfr cls args = SomeWPtrp
x :
m′ :
Memory.mem
r1 :
Er :
SomeOpResraw_resRUncheckedr1 m′ = SomeOpResRValx m′
Heqo0 :
access_resm′ raw_addressptr_addrp off ptr_capp fstnarrow_typet Read 1 = SomeRUncheckedr1
Heqo :
SomeRUncheckedr1 = SomeRUncheckedr1
Hs :
special_letRawLoadLdNarrowt off = false
H0 :
raw_resRUncheckedr1 = RValx
all: simpl in * ; try discriminate
2 openge :
fr :
n :
t :
off :
Z
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Ho :
true = true
Hk :
Some32 ≠ None
cls :
listclass
Ec :
SomeA = Somecls
p :
Ex :
map2_optionvalue_xge fr_envfr cls args = SomeWPtrp
x :
m′ :
Memory.mem
w :
x0 :
unit
Heqo0 :
access_resm′ raw_addressptr_addrp off ptr_capp fstnarrow_typet Read 1 = SomeRValx0
Heqo1 :
extendedt W load_bytesm′ raw_addressptr_addrp off fstnarrow_typet = Somew
Hs :
false = false
focused goal
ge :
fr :
n :
t :
off :
Z
args :
listvalue
l1 :
listname × optionZ
m1 :
Memory.mem
Ho :
true = true
Hk :
Some64 ≠ None
cls :
listclass
Ec :
SomeA = Somecls
p :
Ex :
map2_optionvalue_xge fr_envfr cls args = SomeWPtrp
x :
m′ :
Memory.mem
w :
x0 :
unit
Heqo0 :
access_resm′ raw_addressptr_addrp off ptr_capp fstnarrow_typet Read 1 = SomeRValx0
Heqo1 :
extendedt L load_bytesm′ raw_addressptr_addrp off fstnarrow_typet = Somew
Hs :
false = false
all: match goal withH0 : RVal_ = RVal_ |- _⇒injection H0 as ←end;eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge fr m n k o args e1 l1 m1 Ho Hk H
assert Hs : special_leto = false by destruct o ; try discriminate Ho ; reflexivity
rewrite inst_step_let_ _ _ _ _ _ _ Hs in H
cbv zeta in H
destruct op_arg_classeso k as cls | eqn: Ec ; | discriminate H
destruct map2_option_ cls args as xs | eqn: Ex ; | discriminate H
destruct op_reso k xs m as r m′ | why | q kont | eqn: Er ; try discriminate H
destruct r as x | why | why ; simpl in H ; try discriminate H
injection H as ← _ _
assert Hn : lookupn putn x fr_envfr = Somex by rewrite lookup_put , name_eqb_refl ; reflexivity
destruct k ; try exfalso ; apply Hk ; reflexivity ; destruct o ; try discriminate Ho ; unfold op_res , op_res_int in Er ; simpl in Er ; cases Er ; inversion Er ; subst
all: unfold let_holds
all: first exists cls, xs, x ; auto | idtac
all: destruct t ; try discriminate Ho
all: match goal withHl : int_load_res_ _ _ _ _ = Some_ |- _⇒unfold int_load_res in Hl ; cases Hl ; inversion Hl ; substend
all: simpl in * ; try discriminate
let_holds reads the defined name n only in the later environment, so it survives a change of environment that keeps n.
Explore proof 4 tactics
Initial goal
intros ge e0 e e′ n k o args E H
unfold let_holds in *
ge :
e0 :
n :
k :
o :
args :
listvalue
H :
match o with
CheckLocal_ _ _ _ _
⇒
∃classes : listclass xs : listword x0 : word, op_arg_classeso k = Someclasses ∧ map2_optionvalue_xge e0 classes args = Somexs ∧ aluo k xs = Somex0 ∧ lookupn e = Somex0
_
⇒
∃classes : listclass xs : listword x : word, op_arg_classeso k = Someclasses ∧ map2_optionvalue_xge e0 classes args = Somexs ∧ aluo k xs = Somex ∧ lookupn e = Somex
⊢
match o with
CheckLocal_ _ _ _ _
⇒
∃classes : listclass xs : listword x0 : word, op_arg_classeso k = Someclasses ∧ map2_optionvalue_xge e0 classes args = Somexs ∧ aluo k xs = Somex0 ∧ lookupn e′ = Somex0
_
⇒
∃classes : listclass xs : listword x : word, op_arg_classeso k = Someclasses ∧ map2_optionvalue_xge e0 classes args = Somexs ∧ aluo k xs = Somex ∧ lookupn e′ = Somex
rewrite E
ge :
e0 :
n :
k :
o :
args :
listvalue
H :
match o with
CheckLocal_ _ _ _ _
⇒
∃classes : listclass xs : listword x0 : word, op_arg_classeso k = Someclasses ∧ map2_optionvalue_xge e0 classes args = Somexs ∧ aluo k xs = Somex0 ∧ lookupn e = Somex0
_
⇒
∃classes : listclass xs : listword x : word, op_arg_classeso k = Someclasses ∧ map2_optionvalue_xge e0 classes args = Somexs ∧ aluo k xs = Somex ∧ lookupn e = Somex
⊢
match o with
CheckLocal_ _ _ _ _
⇒
∃classes : listclass xs : listword x0 : word, op_arg_classeso k = Someclasses ∧ map2_optionvalue_xge e0 classes args = Somexs ∧ aluo k xs = Somex0 ∧ lookupn e = Somex0
_
⇒
∃classes : listclass xs : listword x : word, op_arg_classeso k = Someclasses ∧ map2_optionvalue_xge e0 classes args = Somexs ∧ aluo k xs = Somex ∧ lookupn e = Somex
exact H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Definitions that dominate a point
Dominance of sites composes: a site s that dominates index j of block d, where that site dominates index k of block l, dominates index k of block l.
∀ b0 rest doms l k d j s
block_intervalsb0 :: rest = Somedoms
site_dominatesdoms l k SAtd j = true
site_dominatesdoms d j s = true
site_dominatesdoms l k s = true
Explore proof 23 tactics
Initial goal
⊢
∀b0 : block rest : listblock doms : nmapZ × Z l : name k : Z d : name j : Z s : site, block_intervalsb0 :: rest = Somedoms → site_dominatesdoms l k SAtd j = true → site_dominatesdoms d j s = true → site_dominatesdoms l k s = true
intros b0 rest doms l k d j s Hd H1 H2
b0 :
rest :
listblock
doms :
nmapZ × Z
l :
k :
Z
d :
j :
Z
s :
Hd :
block_intervalsb0 :: rest = Somedoms
H1 :
site_dominatesdoms l k SAtd j = true
H2 :
site_dominatesdoms d j s = true
⊢
site_dominatesdoms l k s = true
destruct s as | d′ j′ ; reflexivity |
b0 :
rest :
listblock
doms :
nmapZ × Z
l :
k :
Z
d :
j :
Z
d′ :
j′ :
Z
Hd :
block_intervalsb0 :: rest = Somedoms
H1 :
site_dominatesdoms l k SAtd j = true
H2 :
site_dominatesdoms d j SAtd′ j′ = true
⊢
site_dominatesdoms l k SAtd′ j′ = true
simpl in *
destruct name_eqbd l eqn: Edl ; destruct name_eqbd′ d eqn: Edd
4 openb0 :
rest :
listblock
doms :
nmapZ × Z
l :
k :
Z
d :
j :
Z
d′ :
j′ :
Z
Hd :
block_intervalsb0 :: rest = Somedoms
Edl :
name_eqbd l = true
H1 :
j <? k = true
Edd :
name_eqbd′ d = true
H2 :
j′ <? j = true
focused goal
focused goal
–apply name_eqb_true in Edl , Edd
4 openb0 :
rest :
listblock
doms :
nmapZ × Z
l :
k :
Z
d :
j :
Z
d′ :
j′ :
Z
Hd :
block_intervalsb0 :: rest = Somedoms
Edl :
d = l
H1 :
j <? k = true
Edd :
d′ = d
H2 :
j′ <? j = true
deferred goal
deferred goal
subst
4 openb0 :
rest :
listblock
doms :
nmapZ × Z
l :
k, j, j′ :
Z
Hd :
block_intervalsb0 :: rest = Somedoms
H1 :
j <? k = true
H2 :
j′ <? j = true
deferred goal
deferred goal
rewrite name_eqb_refl
4 openb0 :
rest :
listblock
doms :
nmapZ × Z
l :
k, j, j′ :
Z
Hd :
block_intervalsb0 :: rest = Somedoms
H1 :
j <? k = true
H2 :
j′ <? j = true
⊢
j′ <? k = true
deferred goal
deferred goal
apply Z.ltb_lt in H1 , H2
4 openb0 :
rest :
listblock
doms :
nmapZ × Z
l :
k, j, j′ :
Z
Hd :
block_intervalsb0 :: rest = Somedoms
H1 :
j < k
H2 :
j′ < j
⊢
j′ <? k = true
deferred goal
deferred goal
apply Z.ltb_lt
4 openb0 :
rest :
listblock
doms :
nmapZ × Z
l :
k, j, j′ :
Z
Hd :
block_intervalsb0 :: rest = Somedoms
H1 :
j < k
H2 :
j′ < j
⊢
j′ < k
deferred goal
deferred goal
lia
3 opendeferred goal
deferred goal
–apply name_eqb_true in Edl
3 openb0 :
rest :
listblock
doms :
nmapZ × Z
l :
k :
Z
d :
j :
Z
d′ :
j′ :
Z
Hd :
block_intervalsb0 :: rest = Somedoms
Edl :
d = l
H1 :
j <? k = true
Edd :
name_eqbd′ d = false
H2 :
dominatesdoms d′ d = true
deferred goal
subst
3 openb0 :
rest :
listblock
doms :
nmapZ × Z
l :
k, j :
Z
d′ :
j′ :
Z
Hd :
block_intervalsb0 :: rest = Somedoms
H1 :
j <? k = true
H2 :
dominatesdoms d′ l = true
Edd :
name_eqbd′ l = false
deferred goal
rewrite Edd
3 openb0 :
rest :
listblock
doms :
nmapZ × Z
l :
k, j :
Z
d′ :
j′ :
Z
Hd :
block_intervalsb0 :: rest = Somedoms
H1 :
j <? k = true
H2 :
dominatesdoms d′ l = true
Edd :
name_eqbd′ l = false
⊢
dominatesdoms d′ l = true
deferred goal
exact H2
2 opendeferred goal
–apply name_eqb_true in Edd
2 openb0 :
rest :
listblock
doms :
nmapZ × Z
l :
k :
Z
d :
j :
Z
d′ :
j′ :
Z
Hd :
block_intervalsb0 :: rest = Somedoms
Edl :
name_eqbd l = false
H1 :
dominatesdoms d l = true
Edd :
d′ = d
H2 :
j′ <? j = true
subst
2 openb0 :
rest :
listblock
doms :
nmapZ × Z
l :
k :
Z
d :
j, j′ :
Z
Hd :
block_intervalsb0 :: rest = Somedoms
Edl :
name_eqbd l = false
H1 :
dominatesdoms d l = true
H2 :
j′ <? j = true
rewrite Edl
2 openexact H1
–destruct name_eqbd′ l eqn: Edl′ ; exfalso | exact dominates_trans_ _ _ Hd _ _ _ H2 H1
apply name_eqb_true in Edl′
subst d′
rewrite dom_antisym_ _ _ Hd _ _ H1 H2 , name_eqb_refl in Edl
discriminate Edl
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros b0 rest doms l k d j s Hd H1 H2
destruct s as | d′ j′ ; reflexivity |
simpl in *
–apply name_eqb_true in Edl , Edd
subst
rewrite name_eqb_refl
apply Z.ltb_lt in H1 , H2
apply Z.ltb_lt
lia
–destruct name_eqbd′ l eqn: Edl′ ; exfalso | exact dominates_trans_ _ _ Hd _ _ _ H2 H1
apply name_eqb_true in Edl′
subst d′
rewrite dom_antisym_ _ _ Hd _ _ H1 H2 , name_eqb_refl in Edl
discriminate Edl
In a checked_module md, a single-definition operand a of the instruction i that defines n, where n dominates index k of a reachable block l, dominates it too: the validator requires an operand's definition to dominate its use.
∀ md f l k n i a
InIFuncf md
is_reachablefn_domsf l = true
lookupn single_definitionsf = SomeDInsti
dominatingf l k n
Ina inst_usesi
once_hassingle_definitionsf a = true
dominatingf l k a
Explore proof 19 tactics
Initial goal
⊢
∀md : module f : func l : name k : Z n : name i : inst a : name, checked_modulemd → InIFuncf md → is_reachablefn_domsf l = true → lookupn single_definitionsf = SomeDInsti → dominatingf l k n → Ina inst_usesi → once_hassingle_definitionsf a = true → dominatingf l k a
intros md f l k n i a Hmd Hin Hr Hn s & D & Hn′ & Hpos & Hsd Hu Ho
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
s :
D :
Hn′ :
lookupn single_definitionsf = SomeD
Hpos :
Inn, s, D def_positionsf
Hsd :
site_dominatesfn_domsf l k s = true
Hu :
Ina inst_usesi
Ho :
once_hassingle_definitionsf a = true
⊢
dominatingf l k a
rewrite Hn in Hn′
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
s :
D :
Hn′ :
SomeDInsti = SomeD
Hpos :
Inn, s, D def_positionsf
Hsd :
site_dominatesfn_domsf l k s = true
Hu :
Ina inst_usesi
Ho :
once_hassingle_definitionsf a = true
⊢
dominatingf l k a
injection Hn′ as ←
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
s :
Hpos :
Inn, s, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k s = true
Hu :
Ina inst_usesi
Ho :
once_hassingle_definitionsf a = true
⊢
dominatingf l k a
destruct func_facts_ _ Hmd Hin as b0 & rest & Hf & Hd & _ & Hdd
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
s :
Hpos :
Inn, s, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k s = true
Hu :
Ina inst_usesi
Ho :
once_hassingle_definitionsf a = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
⊢
dominatingf l k a
destruct dinst_site_ _ _ _ Hpos as d & j & →
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
j :
Z
Hsd :
site_dominatesfn_domsf l k SAtd j = true
Hpos :
Inn, SAtd j, DInsti def_positionsf
Hu :
Ina inst_usesi
Ho :
once_hassingle_definitionsf a = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
⊢
dominatingf l k a
destruct position_inst_ _ _ _ _ Hpos as b & kk & Hb & Hl & Hk & → & _
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k SAtd Z.of_natkk = true
Hu :
Ina inst_usesi
Ho :
once_hassingle_definitionsf a = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
⊢
dominatingf l k a
unfold once_has in Ho
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k SAtd Z.of_natkk = true
Hu :
Ina inst_usesi
Ho :
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
⊢
dominatingf l k a
destruct lookupa single_definitionsf as Da | eqn: Ea ; | discriminate Ho
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k SAtd Z.of_natkk = true
Hu :
Ina inst_usesi
Da :
Ea :
lookupa single_definitionsf = SomeDa
Ho :
true = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
⊢
dominatingf l k a
assert Hrb : is_reachablefn_domsf b_labelb = true
2 openmd :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k SAtd Z.of_natkk = true
Hu :
Ina inst_usesi
Da :
Ea :
lookupa single_definitionsf = SomeDa
Ho :
true = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
⊢
is_reachablefn_domsf b_labelb = true
focused goal
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k SAtd Z.of_natkk = true
Hu :
Ina inst_usesi
Da :
Ea :
lookupa single_definitionsf = SomeDa
Ho :
true = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
Hrb :
is_reachablefn_domsf b_labelb = true
⊢
dominatingf l k a
{rewrite Hl
2 openmd :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k SAtd Z.of_natkk = true
Hu :
Ina inst_usesi
Da :
Ea :
lookupa single_definitionsf = SomeDa
Ho :
true = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
⊢
is_reachablefn_domsf d = true
deferred goal
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k SAtd Z.of_natkk = true
Hu :
Ina inst_usesi
Da :
Ea :
lookupa single_definitionsf = SomeDa
Ho :
true = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
Hrb :
is_reachablefn_domsf b_labelb = true
⊢
dominatingf l k a
simpl in Hsd
2 openmd :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hu :
Ina inst_usesi
Da :
Ea :
lookupa single_definitionsf = SomeDa
Ho :
true = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
⊢
is_reachablefn_domsf d = true
deferred goal
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k SAtd Z.of_natkk = true
Hu :
Ina inst_usesi
Da :
Ea :
lookupa single_definitionsf = SomeDa
Ho :
true = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
Hrb :
is_reachablefn_domsf b_labelb = true
⊢
dominatingf l k a
destruct name_eqbd l eqn: E ; apply name_eqb_true in E ; subst ; exact Hr |
2 openmd :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
E :
name_eqbd l = false
Hu :
Ina inst_usesi
Da :
Ea :
lookupa single_definitionsf = SomeDa
Ho :
true = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
⊢
is_reachablefn_domsf d = true
deferred goal
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k SAtd Z.of_natkk = true
Hu :
Ina inst_usesi
Da :
Ea :
lookupa single_definitionsf = SomeDa
Ho :
true = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
Hrb :
is_reachablefn_domsf b_labelb = true
⊢
dominatingf l k a
exact proj1dominates_reachable_ _ _ Hd _ _ Hsd
deferred goal
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k SAtd Z.of_natkk = true
Hu :
Ina inst_usesi
Da :
Ea :
lookupa single_definitionsf = SomeDa
Ho :
true = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
Hrb :
is_reachablefn_domsf b_labelb = true
⊢
dominatingf l k a
destruct use_dominated_ _ _ _ _ _ _ Hdd Hb Hrb Hk Hu Ea as sa & Hsa & Hsda
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k SAtd Z.of_natkk = true
Hu :
Ina inst_usesi
Da :
Ea :
lookupa single_definitionsf = SomeDa
Ho :
true = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
Hrb :
is_reachablefn_domsf b_labelb = true
sa :
Hsa :
Ina, sa, Da def_positionsf
Hsda :
site_dominatesfn_domsf b_labelb Z.of_natkk sa = true
⊢
dominatingf l k a
exists sa, Da
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k SAtd Z.of_natkk = true
Hu :
Ina inst_usesi
Da :
Ea :
lookupa single_definitionsf = SomeDa
Ho :
true = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
Hrb :
is_reachablefn_domsf b_labelb = true
sa :
Hsa :
Ina, sa, Da def_positionsf
Hsda :
site_dominatesfn_domsf b_labelb Z.of_natkk sa = true
⊢
lookupa single_definitionsf = SomeDa ∧ Ina, sa, Da def_positionsf ∧ site_dominatesfn_domsf l k sa = true
split ; exact Ea |
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k SAtd Z.of_natkk = true
Hu :
Ina inst_usesi
Da :
Ea :
lookupa single_definitionsf = SomeDa
Ho :
true = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
Hrb :
is_reachablefn_domsf b_labelb = true
sa :
Hsa :
Ina, sa, Da def_positionsf
Hsda :
site_dominatesfn_domsf b_labelb Z.of_natkk sa = true
⊢
Ina, sa, Da def_positionsf ∧ site_dominatesfn_domsf l k sa = true
split ; exact Hsa |
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k SAtd Z.of_natkk = true
Hu :
Ina inst_usesi
Da :
Ea :
lookupa single_definitionsf = SomeDa
Ho :
true = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
Hrb :
is_reachablefn_domsf b_labelb = true
sa :
Hsa :
Ina, sa, Da def_positionsf
Hsda :
site_dominatesfn_domsf b_labelb Z.of_natkk sa = true
⊢
site_dominatesfn_domsf l k sa = true
rewrite Hl in Hsda
md :
f :
l :
k :
Z
n :
i :
a :
Hmd :
Hin :
InIFuncf md
Hr :
is_reachablefn_domsf l = true
Hn :
lookupn single_definitionsf = SomeDInsti
d :
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hsd :
site_dominatesfn_domsf l k SAtd Z.of_natkk = true
Hu :
Ina inst_usesi
Da :
Ea :
lookupa single_definitionsf = SomeDa
Ho :
true = true
b0 :
rest :
listblock
Hf :
fn_blocksf = b0 :: rest
Hd :
block_intervalsb0 :: rest = Somefn_domsf
Hdd :
definitions_dominatef fn_domsf = true
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hk :
nth_errorb_instsb kk = Somei
Hrb :
is_reachablefn_domsf b_labelb = true
sa :
Hsa :
Ina, sa, Da def_positionsf
Hsda :
site_dominatesfn_domsf d Z.of_natkk sa = true
⊢
site_dominatesfn_domsf l k sa = true
exact site_dominates_trans_ _ _ _ _ _ _ _ Hd Hsd Hsda
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros md f l k n i a Hmd Hin Hr Hn s & D & Hn′ & Hpos & Hsd Hu Ho
rewrite Hn in Hn′
injection Hn′ as ←
destruct func_facts_ _ Hmd Hin as b0 & rest & Hf & Hd & _ & Hdd
destruct dinst_site_ _ _ _ Hpos as d & j & →
destruct position_inst_ _ _ _ _ Hpos as b & kk & Hb & Hl & Hk & → & _
unfold once_has in Ho
destruct lookupa single_definitionsf as Da | eqn: Ea ; | discriminate Ho
assert Hrb : is_reachablefn_domsf b_labelb = true
{rewrite Hl
simpl in Hsd
destruct name_eqbd l eqn: E ; apply name_eqb_true in E ; subst ; exact Hr |
exact proj1dominates_reachable_ _ _ Hd _ _ Hsd
destruct use_dominated_ _ _ _ _ _ _ Hdd Hb Hrb Hk Hu Ea as sa & Hsa & Hsda
exists sa, Da
split ; exact Ea |
split ; exact Hsa |
rewrite Hl in Hsda
exact site_dominates_trans_ _ _ _ _ _ _ _ Hd Hsd Hsda
Where every replayable single definition in scope replays (scope_holds), a replayable definition i of n that dominates the frame's point replays: scope_holds read at one name.
∀ ge fr m l k n i
scope_holdsge fr m
point_sitefr_fnfr fr_atfr = Somel, k
lookupn single_definitionsfr_fnfr = SomeDInsti
replayablei = true
dominatingfr_fnfr l k n
replaysge single_definitionsfr_fnfr fr_envfr m n i
Explore proof 4 tactics
Initial goal
⊢
∀ge : genv fr : frame m : Memory.mem l : name k : Z n : name i : inst, scope_holdsge fr m → point_sitefr_fnfr fr_atfr = Somel, k → lookupn single_definitionsfr_fnfr = SomeDInsti → replayablei = true → dominatingfr_fnfr l k n → replaysge single_definitionsfr_fnfr fr_envfr m n i
intros ge fr m l k n i Hs Hpt Hn Hrp s & D & Hn′ & Hpos & Hsd
ge :
fr :
m :
Memory.mem
l :
k :
Z
n :
i :
Hs :
scope_holdsge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hn :
lookupn single_definitionsfr_fnfr = SomeDInsti
Hrp :
replayablei = true
s :
D :
Hn′ :
lookupn single_definitionsfr_fnfr = SomeD
Hpos :
Inn, s, D def_positionsfr_fnfr
Hsd :
site_dominatesfn_domsfr_fnfr l k s = true
⊢
replaysge single_definitionsfr_fnfr fr_envfr m n i
rewrite Hn in Hn′
ge :
fr :
m :
Memory.mem
l :
k :
Z
n :
i :
Hs :
scope_holdsge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hn :
lookupn single_definitionsfr_fnfr = SomeDInsti
Hrp :
replayablei = true
s :
D :
Hn′ :
SomeDInsti = SomeD
Hpos :
Inn, s, D def_positionsfr_fnfr
Hsd :
site_dominatesfn_domsfr_fnfr l k s = true
⊢
replaysge single_definitionsfr_fnfr fr_envfr m n i
injection Hn′ as ←
ge :
fr :
m :
Memory.mem
l :
k :
Z
n :
i :
Hs :
scope_holdsge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hn :
lookupn single_definitionsfr_fnfr = SomeDInsti
Hrp :
replayablei = true
s :
Hpos :
Inn, s, DInsti def_positionsfr_fnfr
Hsd :
site_dominatesfn_domsfr_fnfr l k s = true
⊢
replaysge single_definitionsfr_fnfr fr_envfr m n i
exact Hs_ _ _ _ _ Hpt Hn Hrp Hpos Hsd
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge fr m l k n i Hs Hpt Hn Hrp s & D & Hn′ & Hpos & Hsd
rewrite Hn in Hn′
injection Hn′ as ←
exact Hs_ _ _ _ _ Hpt Hn Hrp Hpos Hsd
dominating_replays where only definitions that are not a check_ahead need to replay (scope_plain), for a definition that is not one (ahead_free).
∀ ge fr m l k n i
scope_plainge fr m
point_sitefr_fnfr fr_atfr = Somel, k
lookupn single_definitionsfr_fnfr = SomeDInsti
replayablei = true
ahead_freei = true
dominatingfr_fnfr l k n
replaysge single_definitionsfr_fnfr fr_envfr m n i
Explore proof 4 tactics
Initial goal
⊢
∀ge : genv fr : frame m : Memory.mem l : name k : Z n : name i : inst, scope_plainge fr m → point_sitefr_fnfr fr_atfr = Somel, k → lookupn single_definitionsfr_fnfr = SomeDInsti → replayablei = true → ahead_freei = true → dominatingfr_fnfr l k n → replaysge single_definitionsfr_fnfr fr_envfr m n i
intros ge fr m l k n i Hs Hpt Hn Hrp Ha s & D & Hn′ & Hpos & Hsd
ge :
fr :
m :
Memory.mem
l :
k :
Z
n :
i :
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hn :
lookupn single_definitionsfr_fnfr = SomeDInsti
Hrp :
replayablei = true
Ha :
ahead_freei = true
s :
D :
Hn′ :
lookupn single_definitionsfr_fnfr = SomeD
Hpos :
Inn, s, D def_positionsfr_fnfr
Hsd :
site_dominatesfn_domsfr_fnfr l k s = true
⊢
replaysge single_definitionsfr_fnfr fr_envfr m n i
rewrite Hn in Hn′
ge :
fr :
m :
Memory.mem
l :
k :
Z
n :
i :
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hn :
lookupn single_definitionsfr_fnfr = SomeDInsti
Hrp :
replayablei = true
Ha :
ahead_freei = true
s :
D :
Hn′ :
SomeDInsti = SomeD
Hpos :
Inn, s, D def_positionsfr_fnfr
Hsd :
site_dominatesfn_domsfr_fnfr l k s = true
⊢
replaysge single_definitionsfr_fnfr fr_envfr m n i
injection Hn′ as ←
ge :
fr :
m :
Memory.mem
l :
k :
Z
n :
i :
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hn :
lookupn single_definitionsfr_fnfr = SomeDInsti
Hrp :
replayablei = true
Ha :
ahead_freei = true
s :
Hpos :
Inn, s, DInsti def_positionsfr_fnfr
Hsd :
site_dominatesfn_domsfr_fnfr l k s = true
⊢
replaysge single_definitionsfr_fnfr fr_envfr m n i
exact Hs_ _ _ _ _ Hpt Hn Hrp Hpos Hsd Ha
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge fr m l k n i Hs Hpt Hn Hrp Ha s & D & Hn′ & Hpos & Hsd
rewrite Hn in Hn′
injection Hn′ as ←
exact Hs_ _ _ _ _ Hpt Hn Hrp Hpos Hsd Ha
Offset intervals at a point
An offset interval from lo to hi that the validator derives for a value v at class k' (iv, offset_interval/8) holds of the value the frame reads (in_iv), where v's name dominates the frame's point and every single definition in scope but a check_ahead replays.
∀ ge md fr m l k v k′ lo hi
is_reachablefn_domsfr_fnfr l = true
scope_plainge fr m
point_sitefr_fnfr fr_atfr = Somel, k
ivsingle_definitionsfr_fnfr v k′ lo hi
∀n, v = Tmpn → dominatingfr_fnfr l k n
Explore proof 15 tactics
Initial goal
⊢
∀ge : genv md : module fr : frame m : Memory.mem l : name k : Z v : value k′ : class lo hi : Z, checked_modulemd → InIFuncfr_fnfr md → is_reachablefn_domsfr_fnfr l = true → scope_plainge fr m → point_sitefr_fnfr fr_atfr = Somel, k → ivsingle_definitionsfr_fnfr v k′ lo hi → ∀n : name, v = Tmpn → dominatingfr_fnfr l k n → in_ivge fr_envfr k′ v lo hi
intros ge md fr m l k v k′ lo hi Hmd Hin Hr Hs Hpt Hiv Hv
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
v :
k′ :
lo, hi :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hiv :
ivsingle_definitionsfr_fnfr v k′ lo hi
Hv :
∀n : name, v = Tmpn → dominatingfr_fnfr l k n
refine iv_sound_ ge fr_envfr dominatingfr_fnfr l k _ _ _ _ _ Hiv Hv
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
v :
k′ :
lo, hi :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hiv :
ivsingle_definitionsfr_fnfr v k′ lo hi
Hv :
∀n : name, v = Tmpn → dominatingfr_fnfr l k n
⊢
∀n : name k0 : class o : op args : listvalue, definedsingle_definitionsfr_fnfr n k0 o args → iv_opo = true → class_bitsk0 ≠ None → dominatingfr_fnfr l k n → ∃e0 : env, let_holdsge e0 fr_envfr n k0 o args ∧ ∀a : name, InTmpa args → once_hassingle_definitionsfr_fnfr a = true → dominatingfr_fnfr l k a ∧ lookupa e0 = lookupa fr_envfr
intros n k0 o args n′ & Hn & Ene Hop Hk Hdom
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
v :
k′ :
lo, hi :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hiv :
ivsingle_definitionsfr_fnfr v k′ lo hi
Hv :
∀n : name, v = Tmpn → dominatingfr_fnfr l k n
n :
k0 :
o :
args :
listvalue
n′ :
Hn :
lookupn single_definitionsfr_fnfr = SomeDInstLetn′ k0 o args
Ene :
name_eqbn′ n = true
Hop :
iv_opo = true
Hk :
class_bitsk0 ≠ None
Hdom :
dominatingfr_fnfr l k n
apply name_eqb_true in Ene
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
v :
k′ :
lo, hi :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hiv :
ivsingle_definitionsfr_fnfr v k′ lo hi
Hv :
∀n : name, v = Tmpn → dominatingfr_fnfr l k n
n :
k0 :
o :
args :
listvalue
n′ :
Hn :
lookupn single_definitionsfr_fnfr = SomeDInstLetn′ k0 o args
Ene :
n′ = n
Hop :
iv_opo = true
Hk :
class_bitsk0 ≠ None
Hdom :
dominatingfr_fnfr l k n
subst n′
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
v :
k′ :
lo, hi :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hiv :
ivsingle_definitionsfr_fnfr v k′ lo hi
Hv :
∀n : name, v = Tmpn → dominatingfr_fnfr l k n
n :
k0 :
o :
args :
listvalue
Hn :
lookupn single_definitionsfr_fnfr = SomeDInstLetn k0 o args
Hop :
iv_opo = true
Hk :
class_bitsk0 ≠ None
Hdom :
dominatingfr_fnfr l k n
assert Hrp : replayableLetn k0 o args = true by destruct o ; try discriminate Hop ; reflexivity
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
v :
k′ :
lo, hi :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hiv :
ivsingle_definitionsfr_fnfr v k′ lo hi
Hv :
∀n : name, v = Tmpn → dominatingfr_fnfr l k n
n :
k0 :
o :
args :
listvalue
Hn :
lookupn single_definitionsfr_fnfr = SomeDInstLetn k0 o args
Hop :
iv_opo = true
Hk :
class_bitsk0 ≠ None
Hdom :
dominatingfr_fnfr l k n
Hrp :
replayableLetn k0 o args = true
assert Haf : ahead_freeLetn k0 o args = true by destruct o ; try discriminate Hop ; reflexivity
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
v :
k′ :
lo, hi :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hiv :
ivsingle_definitionsfr_fnfr v k′ lo hi
Hv :
∀n : name, v = Tmpn → dominatingfr_fnfr l k n
n :
k0 :
o :
args :
listvalue
Hn :
lookupn single_definitionsfr_fnfr = SomeDInstLetn k0 o args
Hop :
iv_opo = true
Hk :
class_bitsk0 ≠ None
Hdom :
dominatingfr_fnfr l k n
Hrp :
replayableLetn k0 o args = true
Haf :
ahead_freeLetn k0 o args = true
destruct plain_replays_ _ _ _ _ _ _ Hs Hpt Hn Hrp Haf Hdom as fr0 & m0 & e1 & l1 & m1 & Hst & Hn1 & Ha & _
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
v :
k′ :
lo, hi :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hiv :
ivsingle_definitionsfr_fnfr v k′ lo hi
Hv :
∀n : name, v = Tmpn → dominatingfr_fnfr l k n
n :
k0 :
o :
args :
listvalue
Hn :
lookupn single_definitionsfr_fnfr = SomeDInstLetn k0 o args
Hop :
iv_opo = true
Hk :
class_bitsk0 ≠ None
Hdom :
dominatingfr_fnfr l k n
Hrp :
replayableLetn k0 o args = true
Haf :
ahead_freeLetn k0 o args = true
fr0 :
m0 :
Memory.mem
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
exists fr_envfr0
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
v :
k′ :
lo, hi :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hiv :
ivsingle_definitionsfr_fnfr v k′ lo hi
Hv :
∀n : name, v = Tmpn → dominatingfr_fnfr l k n
n :
k0 :
o :
args :
listvalue
Hn :
lookupn single_definitionsfr_fnfr = SomeDInstLetn k0 o args
Hop :
iv_opo = true
Hk :
class_bitsk0 ≠ None
Hdom :
dominatingfr_fnfr l k n
Hrp :
replayableLetn k0 o args = true
Haf :
ahead_freeLetn k0 o args = true
fr0 :
m0 :
Memory.mem
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
split
2 openge :
md :
fr :
m :
Memory.mem
l :
k :
Z
v :
k′ :
lo, hi :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hiv :
ivsingle_definitionsfr_fnfr v k′ lo hi
Hv :
∀n : name, v = Tmpn → dominatingfr_fnfr l k n
n :
k0 :
o :
args :
listvalue
Hn :
lookupn single_definitionsfr_fnfr = SomeDInstLetn k0 o args
Hop :
iv_opo = true
Hk :
class_bitsk0 ≠ None
Hdom :
dominatingfr_fnfr l k n
Hrp :
replayableLetn k0 o args = true
Haf :
ahead_freeLetn k0 o args = true
fr0 :
m0 :
Memory.mem
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
focused goal
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
v :
k′ :
lo, hi :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hiv :
ivsingle_definitionsfr_fnfr v k′ lo hi
Hv :
∀n : name, v = Tmpn → dominatingfr_fnfr l k n
n :
k0 :
o :
args :
listvalue
Hn :
lookupn single_definitionsfr_fnfr = SomeDInstLetn k0 o args
Hop :
iv_opo = true
Hk :
class_bitsk0 ≠ None
Hdom :
dominatingfr_fnfr l k n
Hrp :
replayableLetn k0 o args = true
Haf :
ahead_freeLetn k0 o args = true
fr0 :
m0 :
Memory.mem
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
–exact let_holds_name_ _ _ _ _ _ _ _ eq_symHn1 step_let_holds_ _ _ _ _ _ _ _ _ _ Hop Hk Hst
deferred goal
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
v :
k′ :
lo, hi :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hiv :
ivsingle_definitionsfr_fnfr v k′ lo hi
Hv :
∀n : name, v = Tmpn → dominatingfr_fnfr l k n
n :
k0 :
o :
args :
listvalue
Hn :
lookupn single_definitionsfr_fnfr = SomeDInstLetn k0 o args
Hop :
iv_opo = true
Hk :
class_bitsk0 ≠ None
Hdom :
dominatingfr_fnfr l k n
Hrp :
replayableLetn k0 o args = true
Haf :
ahead_freeLetn k0 o args = true
fr0 :
m0 :
Memory.mem
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
–intros a Hin′ Ho
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
v :
k′ :
lo, hi :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hiv :
ivsingle_definitionsfr_fnfr v k′ lo hi
Hv :
∀n : name, v = Tmpn → dominatingfr_fnfr l k n
n :
k0 :
o :
args :
listvalue
Hn :
lookupn single_definitionsfr_fnfr = SomeDInstLetn k0 o args
Hop :
iv_opo = true
Hk :
class_bitsk0 ≠ None
Hdom :
dominatingfr_fnfr l k n
Hrp :
replayableLetn k0 o args = true
Haf :
ahead_freeLetn k0 o args = true
fr0 :
m0 :
Memory.mem
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
Ha :
a :
Hin′ :
InTmpa args
Ho :
once_hassingle_definitionsfr_fnfr a = true
split
2 openge :
md :
fr :
m :
Memory.mem
l :
k :
Z
v :
k′ :
lo, hi :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hiv :
ivsingle_definitionsfr_fnfr v k′ lo hi
Hv :
∀n : name, v = Tmpn → dominatingfr_fnfr l k n
n :
k0 :
o :
args :
listvalue
Hn :
lookupn single_definitionsfr_fnfr = SomeDInstLetn k0 o args
Hop :
iv_opo = true
Hk :
class_bitsk0 ≠ None
Hdom :
dominatingfr_fnfr l k n
Hrp :
replayableLetn k0 o args = true
Haf :
ahead_freeLetn k0 o args = true
fr0 :
m0 :
Memory.mem
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
Ha :
a :
Hin′ :
InTmpa args
Ho :
once_hassingle_definitionsfr_fnfr a = true
⊢
dominatingfr_fnfr l k a
focused goal
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
v :
k′ :
lo, hi :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hiv :
ivsingle_definitionsfr_fnfr v k′ lo hi
Hv :
∀n : name, v = Tmpn → dominatingfr_fnfr l k n
n :
k0 :
o :
args :
listvalue
Hn :
lookupn single_definitionsfr_fnfr = SomeDInstLetn k0 o args
Hop :
iv_opo = true
Hk :
class_bitsk0 ≠ None
Hdom :
dominatingfr_fnfr l k n
Hrp :
replayableLetn k0 o args = true
Haf :
ahead_freeLetn k0 o args = true
fr0 :
m0 :
Memory.mem
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
Ha :
a :
Hin′ :
InTmpa args
Ho :
once_hassingle_definitionsfr_fnfr a = true
+exact operand_dominating_ _ _ _ _ _ _ Hmd Hin Hr Hn Hdom value_temps_in_ _ Hin′ Ho
deferred goal
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
v :
k′ :
lo, hi :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
Hiv :
ivsingle_definitionsfr_fnfr v k′ lo hi
Hv :
∀n : name, v = Tmpn → dominatingfr_fnfr l k n
n :
k0 :
o :
args :
listvalue
Hn :
lookupn single_definitionsfr_fnfr = SomeDInstLetn k0 o args
Hop :
iv_opo = true
Hk :
class_bitsk0 ≠ None
Hdom :
dominatingfr_fnfr l k n
Hrp :
replayableLetn k0 o args = true
Haf :
ahead_freeLetn k0 o args = true
fr0 :
m0 :
Memory.mem
e1 :
l1 :
listname × optionZ
m1 :
Memory.mem
Ha :
a :
Hin′ :
InTmpa args
Ho :
once_hassingle_definitionsfr_fnfr a = true
+exact Ha_ value_temps_in_ _ Hin′ Ho
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge md fr m l k v k′ lo hi Hmd Hin Hr Hs Hpt Hiv Hv
refine iv_sound_ ge fr_envfr dominatingfr_fnfr l k _ _ _ _ _ Hiv Hv
intros n k0 o args n′ & Hn & Ene Hop Hk Hdom
apply name_eqb_true in Ene
subst n′
assert Hrp : replayableLetn k0 o args = true by destruct o ; try discriminate Hop ; reflexivity
assert Haf : ahead_freeLetn k0 o args = true by destruct o ; try discriminate Hop ; reflexivity
destruct plain_replays_ _ _ _ _ _ _ Hs Hpt Hn Hrp Haf Hdom as fr0 & m0 & e1 & l1 & m1 & Hst & Hn1 & Ha & _
exists fr_envfr0
split
–exact let_holds_name_ _ _ _ _ _ _ _ eq_symHn1 step_let_holds_ _ _ _ _ _ _ _ _ _ Hop Hk Hst
–intros a Hin′ Ho
split
+exact operand_dominating_ _ _ _ _ _ _ Hmd Hin Hr Hn Hdom value_temps_in_ _ Hin′ Ho
+exact Ha_ value_temps_in_ _ Hin′ Ho
The hull of two checks
An access check that passes (cap_access_res) is at an address aligned to its alignment al.
Explore proof 5 tactics
Initial goal
⊢
∀c : cap rs : listregion a size : Z r : rights al : Z, cap_access_resc rs a size r al = Someok → a mod al = 0
unfold cap_access_res
intros c rs a size r al H
destruct c as | base | base | f | n ; try discriminate H ; destruct object_regionbase rs as reg | ; try discriminate H ; destruct base ≤? a && a + size ≤? r_endreg ; try discriminate H ; injection H as H
2 open⊢
a mod al = 0
focused goal
⊢
a mod al = 0
–exact aligned_res_mod_ _ H
deferred goal
⊢
a mod al = 0
–destruct r ; exact aligned_res_mod_ _ H | discriminate H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold cap_access_res
intros c rs a size r al H
destruct c as | base | base | f | n ; try discriminate H ; destruct object_regionbase rs as reg | ; try discriminate H ; destruct base ≤? a && a + size ≤? r_endreg ; try discriminate H ; injection H as H
–exact aligned_res_mod_ _ H
–destruct r ; exact aligned_res_mod_ _ H | discriminate H
Every raw access's alignment divides 2^64, so an address modulo 2^64 is aligned as the address is.
∀ x
sndaccess_size_alignx 2 ^ 64
Explore proof 1 tactics
Initial goal
⊢
∀x : access_type, sndaccess_size_alignx 2 ^ 64
intros | | | | t | w | ; try destruct w ; simpl ; first exists 2 ^ 64 ; reflexivity | exists 2 ^ 61 ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros | | | | t | w | ; try destruct w ; simpl ; first exists 2 ^ 64 ; reflexivity | exists 2 ^ 61 ; reflexivity
An access between two passed checks of one capability c, at addresses of one pointer A that are near offsets apart, passes too (the arithmetic of hull_covered/7). The first check's span ends at or above -2^62 and starts at or below the access; the second's starts at or below 2^62 and ends at or above it. A read needs nothing more; a write needs some write check of the capability to have passed.
The two checks compare addresses taken modulo 2^64. They are A+l1 and A+l2 exactly, not merely congruent to them, only because the object ends at or below 2^48 (objects_fit): addresses inside it that are congruent and less than 2^63 apart are equal.
∀ c rs A l1 s1 r1 al1 l2 s2 r2 al2 off size need aa
cap_access_resc rs raw_addressA l1 s1 r1 al1 = Someok
cap_access_resc rs raw_addressA l2 s2 r2 al2 = Someok
−2 ^ 62 ≤ l1 + s1
l2 ≤ 2 ^ 62
l1 ≤ off
off + size ≤ l2 + s2
0 < size
raw_addressA off mod aa = 0
need = Read ∨ ∃a3 s3 al3, cap_access_resc rs a3 s3 Write al3 = Someok
cap_access_resc rs raw_addressA off size need aa = Someok
Explore proof 16 tactics
Initial goal
⊢
∀c : cap rs : listregion A l1 s1 : Z r1 : rights al1 l2 s2 : Z r2 : rights al2 off size : Z need : rights aa : Z, objects_fitrs → cap_access_resc rs raw_addressA l1 s1 r1 al1 = Someok → cap_access_resc rs raw_addressA l2 s2 r2 al2 = Someok → −2 ^ 62 ≤ l1 + s1 → l2 ≤ 2 ^ 62 → l1 ≤ off → off + size ≤ l2 + s2 → 0 < size → raw_addressA off mod aa = 0 → need = Read ∨ ∃a3 s3 al3 : Z, cap_access_resc rs a3 s3 Write al3 = Someok → cap_access_resc rs raw_addressA off size need aa = Someok
intros c rs A l1 s1 r1 al1 l2 s2 r2 al2 off size need aa Hfit H1 H2 Hh1 Hl2 Hoff Hend Hs Hal Hr
c :
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
H1 :
cap_access_resc rs raw_addressA l1 s1 r1 al1 = Someok
H2 :
cap_access_resc rs raw_addressA l2 s2 r2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
need = Read ∨ ∃a3 s3 al3 : Z, cap_access_resc rs a3 s3 Write al3 = Someok
⊢
cap_access_resc rs raw_addressA off size need aa = Someok
assert Hpos : ∀a, 0 ≤ raw_addressA a < 2 ^ 64 by intros a ; apply Z.mod_pos_bound ; lia
c :
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
H1 :
cap_access_resc rs raw_addressA l1 s1 r1 al1 = Someok
H2 :
cap_access_resc rs raw_addressA l2 s2 r2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
need = Read ∨ ∃a3 s3 al3 : Z, cap_access_resc rs a3 s3 Write al3 = Someok
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
⊢
cap_access_resc rs raw_addressA off size need aa = Someok
assert Hdiv : ∀a, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a by intros a ; apply Z.div_mod ; lia
c :
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
H1 :
cap_access_resc rs raw_addressA l1 s1 r1 al1 = Someok
H2 :
cap_access_resc rs raw_addressA l2 s2 r2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
need = Read ∨ ∃a3 s3 al3 : Z, cap_access_resc rs a3 s3 Write al3 = Someok
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
⊢
cap_access_resc rs raw_addressA off size need aa = Someok
unfold cap_access_res in *
c :
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
H1 :
match c with
Robase
⇒
Some
base ≤? raw_addressA l1 && raw_addressA l1 + s1 ≤? r_endreg
→
readonly_access_resr1 raw_addressA l1 al1
else
=
Someok
H2 :
match c with
Robase
⇒
Some
base ≤? raw_addressA l2 && raw_addressA l2 + s2 ≤? r_endreg
→
readonly_access_resr2 raw_addressA l2 al2
else
=
Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
⊢
match c with
Robase
⇒
Some
base ≤? raw_addressA off && raw_addressA off + size ≤? r_endreg
→
readonly_access_resneed raw_addressA off aa
else
=
Someok
destruct c as | base | base | f | n ; try discriminate H1
2 openbase :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
H1 :
H2 :
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
⊢
focused goal
base :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
H1 :
Some
base ≤? raw_addressA l1 && raw_addressA l1 + s1 ≤? r_endreg
→
readonly_access_resr1 raw_addressA l1 al1
else
=
Someok
H2 :
Some
base ≤? raw_addressA l2 && raw_addressA l2 + s2 ≤? r_endreg
→
readonly_access_resr2 raw_addressA l2 al2
else
=
Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
⊢
Some
base ≤? raw_addressA off && raw_addressA off + size ≤? r_endreg
→
readonly_access_resneed raw_addressA off aa
else
=
Someok
all: destruct object_regionbase rs as reg | eqn: E ; try discriminate H1
2 openbase :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
reg :
E :
object_regionbase rs = Somereg
H1 :
H2 :
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
⊢
focused goal
base :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
reg :
E :
object_regionbase rs = Somereg
H1 :
Some
base ≤? raw_addressA l1 && raw_addressA l1 + s1 ≤? r_endreg
→
readonly_access_resr1 raw_addressA l1 al1
else
=
Someok
H2 :
Some
base ≤? raw_addressA l2 && raw_addressA l2 + s2 ≤? r_endreg
→
readonly_access_resr2 raw_addressA l2 al2
else
=
Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
⊢
Some
base ≤? raw_addressA off && raw_addressA off + size ≤? r_endreg
→
readonly_access_resneed raw_addressA off aa
else
=
Someok
all: pose proof Hfit_ _ E as Hend′ ; destruct base ≤? raw_addressA l1 && raw_addressA l1 + s1 ≤? r_endreg eqn: B1 ; | discriminate H1 ; destruct base ≤? raw_addressA l2 && raw_addressA l2 + s2 ≤? r_endreg eqn: B2 ; | discriminate H2 ; apply andb_true_iff in B1 as B1 B1′ ; apply andb_true_iff in B2 as B2 B2′ ; apply Z.leb_le in B1 , B1′ , B2 , B2′
2 openbase :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
reg :
E :
object_regionbase rs = Somereg
B1 :
base ≤ raw_addressA l1
B1′ :
raw_addressA l1 + s1 ≤ r_endreg
H1 :
Somealigned_resraw_addressA l1 al1 = Someok
B2 :
base ≤ raw_addressA l2
B2′ :
raw_addressA l2 + s2 ≤ r_endreg
H2 :
Somealigned_resraw_addressA l2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
Hend′ :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
⊢
focused goal
base :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
reg :
E :
object_regionbase rs = Somereg
B1 :
base ≤ raw_addressA l1
B1′ :
raw_addressA l1 + s1 ≤ r_endreg
H1 :
Somereadonly_access_resr1 raw_addressA l1 al1 = Someok
B2 :
base ≤ raw_addressA l2
B2′ :
raw_addressA l2 + s2 ≤ r_endreg
H2 :
Somereadonly_access_resr2 raw_addressA l2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
Hend′ :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
⊢
Some
base ≤? raw_addressA off && raw_addressA off + size ≤? r_endreg
→
readonly_access_resneed raw_addressA off aa
else
=
Someok
all: pose proof Hposl1 ; pose proof Hposl2 ; pose proof Hposoff ; pose proof Hdivl1 ; pose proof Hdivl2 ; pose proof Hdivoff
2 openbase :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
reg :
E :
object_regionbase rs = Somereg
B1 :
base ≤ raw_addressA l1
B1′ :
raw_addressA l1 + s1 ≤ r_endreg
H1 :
Somealigned_resraw_addressA l1 al1 = Someok
B2 :
base ≤ raw_addressA l2
B2′ :
raw_addressA l2 + s2 ≤ r_endreg
H2 :
Somealigned_resraw_addressA l2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
Hend′ :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
H :
0 ≤ raw_addressA l1 < 2 ^ 64
H0 :
0 ≤ raw_addressA l2 < 2 ^ 64
H3 :
0 ≤ raw_addressA off < 2 ^ 64
H4 :
A + l1 = 2 ^ 64 × A + l1 / 2 ^ 64 + raw_addressA l1
H5 :
A + l2 = 2 ^ 64 × A + l2 / 2 ^ 64 + raw_addressA l2
H6 :
A + off = 2 ^ 64 × A + off / 2 ^ 64 + raw_addressA off
⊢
focused goal
base :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
reg :
E :
object_regionbase rs = Somereg
B1 :
base ≤ raw_addressA l1
B1′ :
raw_addressA l1 + s1 ≤ r_endreg
H1 :
Somereadonly_access_resr1 raw_addressA l1 al1 = Someok
B2 :
base ≤ raw_addressA l2
B2′ :
raw_addressA l2 + s2 ≤ r_endreg
H2 :
Somereadonly_access_resr2 raw_addressA l2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
Hend′ :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
H :
0 ≤ raw_addressA l1 < 2 ^ 64
H0 :
0 ≤ raw_addressA l2 < 2 ^ 64
H3 :
0 ≤ raw_addressA off < 2 ^ 64
H4 :
A + l1 = 2 ^ 64 × A + l1 / 2 ^ 64 + raw_addressA l1
H5 :
A + l2 = 2 ^ 64 × A + l2 / 2 ^ 64 + raw_addressA l2
H6 :
A + off = 2 ^ 64 × A + off / 2 ^ 64 + raw_addressA off
⊢
Some
base ≤? raw_addressA off && raw_addressA off + size ≤? r_endreg
→
readonly_access_resneed raw_addressA off aa
else
=
Someok
all: replace base ≤? raw_addressA off && raw_addressA off + size ≤? r_endreg with true by symmetry ; apply andb_true_iff ; split ; apply Z.leb_le ; lia
2 openbase :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
reg :
E :
object_regionbase rs = Somereg
B1 :
base ≤ raw_addressA l1
B1′ :
raw_addressA l1 + s1 ≤ r_endreg
H1 :
Somealigned_resraw_addressA l1 al1 = Someok
B2 :
base ≤ raw_addressA l2
B2′ :
raw_addressA l2 + s2 ≤ r_endreg
H2 :
Somealigned_resraw_addressA l2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
Hend′ :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
H :
0 ≤ raw_addressA l1 < 2 ^ 64
H0 :
0 ≤ raw_addressA l2 < 2 ^ 64
H3 :
0 ≤ raw_addressA off < 2 ^ 64
H4 :
A + l1 = 2 ^ 64 × A + l1 / 2 ^ 64 + raw_addressA l1
H5 :
A + l2 = 2 ^ 64 × A + l2 / 2 ^ 64 + raw_addressA l2
H6 :
A + off = 2 ^ 64 × A + off / 2 ^ 64 + raw_addressA off
⊢
Somealigned_resraw_addressA off aa = Someok
focused goal
base :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
reg :
E :
object_regionbase rs = Somereg
B1 :
base ≤ raw_addressA l1
B1′ :
raw_addressA l1 + s1 ≤ r_endreg
H1 :
Somereadonly_access_resr1 raw_addressA l1 al1 = Someok
B2 :
base ≤ raw_addressA l2
B2′ :
raw_addressA l2 + s2 ≤ r_endreg
H2 :
Somereadonly_access_resr2 raw_addressA l2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
Hend′ :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
H :
0 ≤ raw_addressA l1 < 2 ^ 64
H0 :
0 ≤ raw_addressA l2 < 2 ^ 64
H3 :
0 ≤ raw_addressA off < 2 ^ 64
H4 :
A + l1 = 2 ^ 64 × A + l1 / 2 ^ 64 + raw_addressA l1
H5 :
A + l2 = 2 ^ 64 × A + l2 / 2 ^ 64 + raw_addressA l2
H6 :
A + off = 2 ^ 64 × A + off / 2 ^ 64 + raw_addressA off
⊢
Somereadonly_access_resneed raw_addressA off aa = Someok
–f_equal
2 openbase :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
reg :
E :
object_regionbase rs = Somereg
B1 :
base ≤ raw_addressA l1
B1′ :
raw_addressA l1 + s1 ≤ r_endreg
H1 :
Somealigned_resraw_addressA l1 al1 = Someok
B2 :
base ≤ raw_addressA l2
B2′ :
raw_addressA l2 + s2 ≤ r_endreg
H2 :
Somealigned_resraw_addressA l2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
Hend′ :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
H :
0 ≤ raw_addressA l1 < 2 ^ 64
H0 :
0 ≤ raw_addressA l2 < 2 ^ 64
H3 :
0 ≤ raw_addressA off < 2 ^ 64
H4 :
A + l1 = 2 ^ 64 × A + l1 / 2 ^ 64 + raw_addressA l1
H5 :
A + l2 = 2 ^ 64 × A + l2 / 2 ^ 64 + raw_addressA l2
H6 :
A + off = 2 ^ 64 × A + off / 2 ^ 64 + raw_addressA off
⊢
aligned_resraw_addressA off aa = ok
deferred goal
base :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
reg :
E :
object_regionbase rs = Somereg
B1 :
base ≤ raw_addressA l1
B1′ :
raw_addressA l1 + s1 ≤ r_endreg
H1 :
Somereadonly_access_resr1 raw_addressA l1 al1 = Someok
B2 :
base ≤ raw_addressA l2
B2′ :
raw_addressA l2 + s2 ≤ r_endreg
H2 :
Somereadonly_access_resr2 raw_addressA l2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
Hend′ :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
H :
0 ≤ raw_addressA l1 < 2 ^ 64
H0 :
0 ≤ raw_addressA l2 < 2 ^ 64
H3 :
0 ≤ raw_addressA off < 2 ^ 64
H4 :
A + l1 = 2 ^ 64 × A + l1 / 2 ^ 64 + raw_addressA l1
H5 :
A + l2 = 2 ^ 64 × A + l2 / 2 ^ 64 + raw_addressA l2
H6 :
A + off = 2 ^ 64 × A + off / 2 ^ 64 + raw_addressA off
⊢
Somereadonly_access_resneed raw_addressA off aa = Someok
apply aligned_res_ok
2 openbase :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
reg :
E :
object_regionbase rs = Somereg
B1 :
base ≤ raw_addressA l1
B1′ :
raw_addressA l1 + s1 ≤ r_endreg
H1 :
Somealigned_resraw_addressA l1 al1 = Someok
B2 :
base ≤ raw_addressA l2
B2′ :
raw_addressA l2 + s2 ≤ r_endreg
H2 :
Somealigned_resraw_addressA l2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
Hend′ :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
H :
0 ≤ raw_addressA l1 < 2 ^ 64
H0 :
0 ≤ raw_addressA l2 < 2 ^ 64
H3 :
0 ≤ raw_addressA off < 2 ^ 64
H4 :
A + l1 = 2 ^ 64 × A + l1 / 2 ^ 64 + raw_addressA l1
H5 :
A + l2 = 2 ^ 64 × A + l2 / 2 ^ 64 + raw_addressA l2
H6 :
A + off = 2 ^ 64 × A + off / 2 ^ 64 + raw_addressA off
⊢
raw_addressA off mod aa = 0
deferred goal
base :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
reg :
E :
object_regionbase rs = Somereg
B1 :
base ≤ raw_addressA l1
B1′ :
raw_addressA l1 + s1 ≤ r_endreg
H1 :
Somereadonly_access_resr1 raw_addressA l1 al1 = Someok
B2 :
base ≤ raw_addressA l2
B2′ :
raw_addressA l2 + s2 ≤ r_endreg
H2 :
Somereadonly_access_resr2 raw_addressA l2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
Hend′ :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
H :
0 ≤ raw_addressA l1 < 2 ^ 64
H0 :
0 ≤ raw_addressA l2 < 2 ^ 64
H3 :
0 ≤ raw_addressA off < 2 ^ 64
H4 :
A + l1 = 2 ^ 64 × A + l1 / 2 ^ 64 + raw_addressA l1
H5 :
A + l2 = 2 ^ 64 × A + l2 / 2 ^ 64 + raw_addressA l2
H6 :
A + off = 2 ^ 64 × A + off / 2 ^ 64 + raw_addressA off
⊢
Somereadonly_access_resneed raw_addressA off aa = Someok
exact Hal
deferred goal
base :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size :
Z
need :
aa :
Z
Hfit :
reg :
E :
object_regionbase rs = Somereg
B1 :
base ≤ raw_addressA l1
B1′ :
raw_addressA l1 + s1 ≤ r_endreg
H1 :
Somereadonly_access_resr1 raw_addressA l1 al1 = Someok
B2 :
base ≤ raw_addressA l2
B2′ :
raw_addressA l2 + s2 ≤ r_endreg
H2 :
Somereadonly_access_resr2 raw_addressA l2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
Hend′ :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
H :
0 ≤ raw_addressA l1 < 2 ^ 64
H0 :
0 ≤ raw_addressA l2 < 2 ^ 64
H3 :
0 ≤ raw_addressA off < 2 ^ 64
H4 :
A + l1 = 2 ^ 64 × A + l1 / 2 ^ 64 + raw_addressA l1
H5 :
A + l2 = 2 ^ 64 × A + l2 / 2 ^ 64 + raw_addressA l2
H6 :
A + off = 2 ^ 64 × A + off / 2 ^ 64 + raw_addressA off
⊢
Somereadonly_access_resneed raw_addressA off aa = Someok
–destruct need ; simpl ; f_equal ; apply aligned_res_ok ; exact Hal |
base :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size, aa :
Z
Hfit :
reg :
E :
object_regionbase rs = Somereg
B1 :
base ≤ raw_addressA l1
B1′ :
raw_addressA l1 + s1 ≤ r_endreg
H1 :
Somereadonly_access_resr1 raw_addressA l1 al1 = Someok
B2 :
base ≤ raw_addressA l2
B2′ :
raw_addressA l2 + s2 ≤ r_endreg
H2 :
Somereadonly_access_resr2 raw_addressA l2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
∨
∃ a3 s3 al3 : Z ,
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
Hend′ :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
H :
0 ≤ raw_addressA l1 < 2 ^ 64
H0 :
0 ≤ raw_addressA l2 < 2 ^ 64
H3 :
0 ≤ raw_addressA off < 2 ^ 64
H4 :
A + l1 = 2 ^ 64 × A + l1 / 2 ^ 64 + raw_addressA l1
H5 :
A + l2 = 2 ^ 64 × A + l2 / 2 ^ 64 + raw_addressA l2
H6 :
A + off = 2 ^ 64 × A + off / 2 ^ 64 + raw_addressA off
exfalso
base :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size, aa :
Z
Hfit :
reg :
E :
object_regionbase rs = Somereg
B1 :
base ≤ raw_addressA l1
B1′ :
raw_addressA l1 + s1 ≤ r_endreg
H1 :
Somereadonly_access_resr1 raw_addressA l1 al1 = Someok
B2 :
base ≤ raw_addressA l2
B2′ :
raw_addressA l2 + s2 ≤ r_endreg
H2 :
Somereadonly_access_resr2 raw_addressA l2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
Hr :
∨
∃ a3 s3 al3 : Z ,
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
Hend′ :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
H :
0 ≤ raw_addressA l1 < 2 ^ 64
H0 :
0 ≤ raw_addressA l2 < 2 ^ 64
H3 :
0 ≤ raw_addressA off < 2 ^ 64
H4 :
A + l1 = 2 ^ 64 × A + l1 / 2 ^ 64 + raw_addressA l1
H5 :
A + l2 = 2 ^ 64 × A + l2 / 2 ^ 64 + raw_addressA l2
H6 :
A + off = 2 ^ 64 × A + off / 2 ^ 64 + raw_addressA off
⊢
False
destruct Hr as Hr | a3 & s3 & al3 & Hw ; discriminate Hr |
base :
Z
rs :
listregion
A, l1, s1 :
Z
r1 :
al1, l2, s2 :
Z
r2 :
al2, off, size, aa :
Z
Hfit :
reg :
E :
object_regionbase rs = Somereg
B1 :
base ≤ raw_addressA l1
B1′ :
raw_addressA l1 + s1 ≤ r_endreg
H1 :
Somereadonly_access_resr1 raw_addressA l1 al1 = Someok
B2 :
base ≤ raw_addressA l2
B2′ :
raw_addressA l2 + s2 ≤ r_endreg
H2 :
Somereadonly_access_resr2 raw_addressA l2 al2 = Someok
Hh1 :
−2 ^ 62 ≤ l1 + s1
Hl2 :
l2 ≤ 2 ^ 62
Hoff :
l1 ≤ off
Hend :
off + size ≤ l2 + s2
Hs :
0 < size
Hal :
raw_addressA off mod aa = 0
a3, s3, al3 :
Z
Hw :
Hpos :
∀a : Z, 0 ≤ raw_addressA a < 2 ^ 64
Hdiv :
∀a : Z, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a
Hend′ :
0 ≤ base ∧ r_endreg ≤ 2 ^ 48
H :
0 ≤ raw_addressA l1 < 2 ^ 64
H0 :
0 ≤ raw_addressA l2 < 2 ^ 64
H3 :
0 ≤ raw_addressA off < 2 ^ 64
H4 :
A + l1 = 2 ^ 64 × A + l1 / 2 ^ 64 + raw_addressA l1
H5 :
A + l2 = 2 ^ 64 × A + l2 / 2 ^ 64 + raw_addressA l2
H6 :
A + off = 2 ^ 64 × A + off / 2 ^ 64 + raw_addressA off
⊢
False
destruct _ && _ ; discriminate Hw
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros c rs A l1 s1 r1 al1 l2 s2 r2 al2 off size need aa Hfit H1 H2 Hh1 Hl2 Hoff Hend Hs Hal Hr
assert Hpos : ∀a, 0 ≤ raw_addressA a < 2 ^ 64 by intros a ; apply Z.mod_pos_bound ; lia
assert Hdiv : ∀a, A + a = 2 ^ 64 × A + a / 2 ^ 64 + raw_addressA a by intros a ; apply Z.div_mod ; lia
unfold cap_access_res in *
destruct c as | base | base | f | n ; try discriminate H1
all: destruct object_regionbase rs as reg | eqn: E ; try discriminate H1
all: pose proof Hfit_ _ E as Hend′ ; destruct base ≤? raw_addressA l1 && raw_addressA l1 + s1 ≤? r_endreg eqn: B1 ; | discriminate H1 ; destruct base ≤? raw_addressA l2 && raw_addressA l2 + s2 ≤? r_endreg eqn: B2 ; | discriminate H2 ; apply andb_true_iff in B1 as B1 B1′ ; apply andb_true_iff in B2 as B2 B2′ ; apply Z.leb_le in B1 , B1′ , B2 , B2′
all: pose proof Hposl1 ; pose proof Hposl2 ; pose proof Hposoff ; pose proof Hdivl1 ; pose proof Hdivl2 ; pose proof Hdivoff
all: replace base ≤? raw_addressA off && raw_addressA off + size ≤? r_endreg with true by symmetry ; apply andb_true_iff ; split ; apply Z.leb_le ; lia
–destruct need ; simpl ; f_equal ; apply aligned_res_ok ; exact Hal |
exfalso
destruct Hr as Hr | a3 & s3 & al3 & Hw ; discriminate Hr |
destruct _ && _ ; discriminate Hw
Guard chains
What first_some finds is f of some element of the list.
Explore proof 3 tactics
Initial goal
⊢
∀X Y : Type f : X → optionY xs : listX y : Y, first_somef xs = Somey → ∃x : X, Inx xs ∧ fx = Somey
intros X Y f xs y
X :
Type
Y :
Type
f :
X → optionY
xs :
listX
y :
Y
⊢
first_somef xs = Somey → ∃x : X, Inx xs ∧ fx = Somey
induction xs as | x xs IH ; simpl ; intros H ; discriminate H |
X :
Type
Y :
Type
f :
X → optionY
x :
X
xs :
listX
y :
Y
IH :
first_somef xs = Somey → ∃x : X, Inx xs ∧ fx = Somey
H :
⊢
∃x0 : X, x = x0 ∨ Inx0 xs ∧ fx0 = Somey
destruct fx eqn: E ; injection H as ← ; eauto | destruct IHH as x′ & Hin & Hx ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros X Y f xs y
induction xs as | x xs IH ; simpl ; intros H ; discriminate H |
destruct fx eqn: E ; injection H as ← ; eauto | destruct IHH as x′ & Hin & Hx ; eauto
A flight that is the single definition of y defines y.
Explore proof 7 tactics
Initial goal
⊢
∀f : func y d : name o : op args : listflight_arg lw : flight_lower, lookupy single_definitionsf = SomeDInstFlightd o args lw → d = y
intros f y d o args lw H
⊢
d = y
destruct once_position_ _ _ H as s & Hpos & _
f :
y, d :
o :
args :
listflight_arg
lw :
H :
lookupy single_definitionsf = SomeDInstFlightd o args lw
s :
Hpos :
Iny, s, DInstFlightd o args lw def_positionsf
⊢
d = y
destruct dinst_site_ _ _ _ Hpos as dd & j & →
f :
y, d :
o :
args :
listflight_arg
lw :
H :
lookupy single_definitionsf = SomeDInstFlightd o args lw
dd :
j :
Z
Hpos :
Iny, SAtdd j, DInstFlightd o args lw def_positionsf
⊢
d = y
destruct position_inst_ _ _ _ _ Hpos as _ & _ & _ & _ & _ & _ & Hy
f :
y, d :
o :
args :
listflight_arg
lw :
H :
lookupy single_definitionsf = SomeDInstFlightd o args lw
dd :
j :
Z
Hpos :
Iny, SAtdd j, DInstFlightd o args lw def_positionsf
Hy :
Iny mapfst inst_temp_defsFlightd o args lw
⊢
d = y
simpl in Hy
f :
y, d :
o :
args :
listflight_arg
lw :
H :
lookupy single_definitionsf = SomeDInstFlightd o args lw
dd :
j :
Z
Hpos :
Iny, SAtdd j, DInstFlightd o args lw def_positionsf
Hy :
d = y ∨ False
⊢
d = y
destruct Hy as → |
f :
y :
o :
args :
listflight_arg
lw :
H :
lookupy single_definitionsf = SomeDInstFlighty o args lw
dd :
j :
Z
Hpos :
Iny, SAtdd j, DInstFlighty o args lw def_positionsf
⊢
y = y
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros f y d o args lw H
destruct once_position_ _ _ H as s & Hpos & _
destruct dinst_site_ _ _ _ Hpos as dd & j & →
destruct position_inst_ _ _ _ _ Hpos as _ & _ & _ & _ & _ & _ & Hy
simpl in Hy
destruct Hy as → |
reflexivity
A value v reads alike (value_x) in two environments e0 and e that agree on its name.
Explore proof 2 tactics
Initial goal
intros ge e0 e k v H
destruct v as y | c | g ; simpl ; rewrite Hy eq_refl | | ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge e0 e k v H
destruct v as y | c | g ; simpl ; rewrite Hy eq_refl | | ; reflexivity
What a guard chain element (b, lo, hi) says of a pointer pp0: the value b reads in the environment e as a pointer with pp0's capability, and pp0's address is b's plus some x between lo and hi, modulo 2^64.
A value v is not a name defined more than once: a constant, a global, or a single-definition name in once.
The address arithmetic of an add flight: shifting by z and then by xo is shifting by xo + z, modulo 2^64.
∀ a z xo
a mod 2 ^ 64 + z mod 2 ^ 64 mod 2 ^ 64 + xo mod 2 ^ 64 = a + xo + z mod 2 ^ 64
Explore proof 4 tactics
Initial goal
⊢
∀a z xo : Z, a mod 2 ^ 64 + z mod 2 ^ 64 mod 2 ^ 64 + xo mod 2 ^ 64 = a + xo + z mod 2 ^ 64
intros a z xo
a, z, xo :
Z
⊢
a mod 2 ^ 64 + z mod 2 ^ 64 mod 2 ^ 64 + xo mod 2 ^ 64 = a + xo + z mod 2 ^ 64
rewrite <- Z.add_mod , Z.add_mod_idemp_l by lia
a, z, xo :
Z
⊢
a + z + xo mod 2 ^ 64 = a + xo + z mod 2 ^ 64
f_equal
a, z, xo :
Z
⊢
a + z + xo = a + xo + z
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros a z xo
rewrite <- Z.add_mod , Z.add_mod_idemp_l by lia
f_equal
lia
The same for a sub flight: shifting by -z and then xo.
∀ a z xo
a mod 2 ^ 64 − z mod 2 ^ 64 mod 2 ^ 64 + xo mod 2 ^ 64 = a + xo − z mod 2 ^ 64
Explore proof 4 tactics
Initial goal
⊢
∀a z xo : Z, a mod 2 ^ 64 − z mod 2 ^ 64 mod 2 ^ 64 + xo mod 2 ^ 64 = a + xo − z mod 2 ^ 64
intros a z xo
a, z, xo :
Z
⊢
a mod 2 ^ 64 − z mod 2 ^ 64 mod 2 ^ 64 + xo mod 2 ^ 64 = a + xo − z mod 2 ^ 64
rewrite <- Zminus_mod , Z.add_mod_idemp_l by lia
a, z, xo :
Z
⊢
a − z + xo mod 2 ^ 64 = a + xo − z mod 2 ^ 64
f_equal
a, z, xo :
Z
⊢
a − z + xo = a + xo − z
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros a z xo
rewrite <- Zminus_mod , Z.add_mod_idemp_l by lia
f_equal
lia
The same for a copy flight, whose shift z is 0 modulo 2^64.
∀ a z xo
z mod 2 ^ 64 = 0
a mod 2 ^ 64 + xo mod 2 ^ 64 = a + xo + z mod 2 ^ 64
Explore proof 4 tactics
Initial goal
⊢
∀a z xo : Z, z mod 2 ^ 64 = 0 → a mod 2 ^ 64 + xo mod 2 ^ 64 = a + xo + z mod 2 ^ 64
intros a z xo Hz
a, z, xo :
Z
Hz :
z mod 2 ^ 64 = 0
⊢
a mod 2 ^ 64 + xo mod 2 ^ 64 = a + xo + z mod 2 ^ 64
replace a + xo + z with a + xo + z by lia
a, z, xo :
Z
Hz :
z mod 2 ^ 64 = 0
⊢
a mod 2 ^ 64 + xo mod 2 ^ 64 = a + xo + z mod 2 ^ 64
rewrite Z.add_moda + xo z , Hz , Z.add_0_r , Z.mod_mod , Z.add_mod_idemp_l by lia
a, z, xo :
Z
Hz :
z mod 2 ^ 64 = 0
⊢
a + xo mod 2 ^ 64 = a + xo mod 2 ^ 64
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros a z xo Hz
replace a + xo + z with a + xo + z by lia
rewrite Z.add_moda + xo z , Hz , Z.add_0_r , Z.mod_mod , Z.add_mod_idemp_l by lia
reflexivity
Lemmas for a frame fr of a checked_module md, in memory m, at index k of a reachable block l, where every single definition in scope but a check_ahead replays (scope_plain).
Every stable element of a guard chain walked from p with fuel steps (guard_chain/3) holds of the pointer pp0 (offset_rel), where p's single definition dominates the point and p's own element holds. The induction behind guard_chain_sound.
∀ fuel p lo hi pp0 b blo bhi
∀y, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
stablesingle_definitionsfr_fnfr p → offset_relge fr_envfr pp0 p lo hi
Inb, blo, bhi guard_chain_gosingle_definitionsfr_fnfr fuel p lo hi
offset_relge fr_envfr pp0 b blo bhi
Proof 76 steps Qed
induction fuel as | fuel IH ; intros p lo hi pp0 Hdom Hrel b blo bhi Hb Hst ; simpl in Hb
–destruct Hb as E |
injection E as → → →
exact HrelHst
–destruct Hb as E | Hb ; injection E as → → → ; exact HrelHst |
destruct p as x | c | g ; try contradiction
destruct lookupx single_definitionsfr_fnfr as | ph | i | eqn: Ex ; try contradiction
destruct i as | d o args lw | | | | | | ; try contradiction
destruct lw as | b′ ; try contradiction
destruct flight_termo args b' as ov sign | eqn: Ef ; | contradiction
destruct offset_interval_ ov L as olo ohi | eqn: Eo ; | contradiction
pose proof flight_def_name_ _ _ _ _ _ Ex as →
assert Hox : once_hassingle_definitionsfr_fnfr x = true by unfold once_has ; rewrite Ex ; reflexivity
pose proof Hdomx eq_refl Hox as Hdx
destruct Hrelltac:intros y E ; injection E as ← ; exact Hox as pp & xo & Hpp & Hcap & Hxo & Haddr
destruct plain_replays_ _ _ _ _ _ _ Hs Hpt Ex eq_refl eq_refl Hdx as fr0 & m0 & e1 & l1 & m1 & Hst′ & Hx1 & Hops & _
assert Hop : ∀y, InTmpy mapflight_arg_value args ++ b' → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y ∧ lookupy fr_envfr0 = lookupy fr_envfr
{intros y Hy Ho
split
–exact operand_dominating_ _ _ _ _ _ _ Hmd Hin Hr Ex Hdx value_temps_in_ _ Hy Ho
–exact Hops_ value_temps_in_ _ Hy Ho
assert Hov : ∀y, ov = Tmpy → InTmpy mapflight_arg_value args ++ b' → ∃z, olo ≤ z ≤ ohi ∧ value_xge fr_envfr0 L ov = SomeWIntz mod 2 ^ 64
{intros Hin′
pose proof offset_interval_iv_ _ _ _ _ Eo as Hiv
assert Hdv : ∀y, ov = Tmpy → dominatingfr_fnfr l k y ∧ lookupy fr_envfr0 = lookupy fr_envfr by intros y E ; exact Hopy Hin'y E iv_once_ _ _ _ _ Hiv _ E
destruct interval_at_ _ _ _ _ _ _ _ _ _ Hmd Hin Hr Hs Hpt Hiv λy E ⇒ proj1Hdvy E as bits & u′ & z & Hbits & Hu & Hz & →
injection Hbits as ←
exists z
split ; exact Hz |
rewrite <- Hu
apply value_x_agree
intros y E
exact proj2Hdvy E
assert Hdb : ∀y, b' = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y ∧ lookupy fr_envfr0 = lookupy fr_envfr by intros y E Ho ; subst b' ; apply Hop ; apply in_or_app ; right ; left ; reflexivity | exact Ho
simpl in Hst'
unfold flight_cap in Hst'
unfold flight_term in Ef
cases Ef ; injection Ef as ← ←;match goal withE : value_eqb_ _ = true |- _⇒apply value_eqb_eq in E ; substend
all: simpl in Hst'
all: destruct value_xge fr_envfr0 P b' as u0 | pb0 | c0 s0 | eqn: Eb ; simpl in Hst' ; try discriminate Hst'
all: try (match type of Hst' withcontext [value_x_ _ L ]⇒destruct value_xge fr_envfr0 L w as u | | | eqn: Evend;simpl in Hst';try discriminate Hst')
all: injection Hst' as ← _ _
all: rewrite lookup_put , name_eqb_refl in Hx1
all: simpl in Hpp ; rewrite <- Hx1 in Hpp ; simpl in Hpp ; injection Hpp as ← ; simpl in Hcap
all: change Z.pow_pos2 64 with 2 ^ 64 in *
all: assert Hb′ : stablesingle_definitionsfr_fnfr b' → value_xge fr_envfr P b' = SomeWPtrpb0 by intros Hsb ; rewrite <- Eb ; symmetry ; apply value_x_agree ; intros y E ; exact proj2Hdby E Hsby E
all: simpl in Hb
all: refine IHb' _ _ pp0 λy E Ho ⇒ proj1Hdby E Ho _ b blo bhi Hb Hst ; intros Hsb
all: destruct Hovltac:intros y E ; first discriminate E | subst ; simpl ; auto 10 as z & Hz & Ez ; injection Ez as Ez
+exists pb0, xo + z
split ; exact Hb'Hsb |
split ; exact Hcap |
split ; lia |
rewrite Haddr
simpl
change Z.pow_pos2 64 with 2 ^ 64 in *
rewrite Ez
apply mod_shift_add
+exists pb0, xo − z
split ; exact Hb'Hsb |
split ; exact Hcap |
split ; lia |
rewrite Haddr
simpl
rewrite Ez
apply mod_shift_sub
+exists pb0, xo + z
split ; exact Hb'Hsb |
split ; exact Hcap |
split ; lia |
rewrite Haddr
simpl
apply mod_shift_zero
change Z.pow_pos2 64 with 2 ^ 64 in *
rewrite <- Ez
reflexivity
guard_chain as an equation. Unfolding it in a hypothesis instead makes the kernel compare two unfoldings of guard_chain_go, which recurses twice per level, 64 levels deep.
∀ once p
guard_chainonce p = guard_chain_goonce 64 p 0 0
Explore proof 2 tactics
Initial goal
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
⊢
∀once : listname × def p : value, guard_chainonce p = guard_chain_goonce 64 p 0 0
intros once p
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p :
⊢
guard_chainonce p = guard_chain_goonce 64 p 0 0
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros once p
reflexivity
Each stable element of the guard chain of a value p (guard_chain/3) holds of the pointer pp that p reads (offset_rel), where p's single definition dominates the point.
∀ p pp b blo bhi
∀y, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Inb, blo, bhi guard_chainsingle_definitionsfr_fnfr p
offset_relge fr_envfr pp b blo bhi
Explore proof 10 tactics
Initial goal
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
⊢
∀p : value pp : ptr b : value blo bhi : Z, value_xge fr_envfr P p = SomeWPtrpp → ∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y → Inb, blo, bhi guard_chainsingle_definitionsfr_fnfr p → stablesingle_definitionsfr_fnfr b → offset_relge fr_envfr pp b blo bhi
intros p pp b blo bhi Hp Hdom Hb Hst
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p :
pp :
b :
blo, bhi :
Z
Hdom :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hb :
Inb, blo, bhi guard_chainsingle_definitionsfr_fnfr p
Hst :
⊢
offset_relge fr_envfr pp b blo bhi
rewrite guard_chain_eq in Hb
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p :
pp :
b :
blo, bhi :
Z
Hdom :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hb :
Inb, blo, bhi guard_chain_gosingle_definitionsfr_fnfr 64 p 0 0
Hst :
⊢
offset_relge fr_envfr pp b blo bhi
refine chain_go_sound64 p 0 0 pp Hdom _ b blo bhi Hb Hst
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p :
pp :
b :
blo, bhi :
Z
Hdom :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hb :
Inb, blo, bhi guard_chain_gosingle_definitionsfr_fnfr 64 p 0 0
Hst :
⊢
stablesingle_definitionsfr_fnfr p → offset_relge fr_envfr pp p 0 0
intros _
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p :
pp :
b :
blo, bhi :
Z
Hdom :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hb :
Inb, blo, bhi guard_chain_gosingle_definitionsfr_fnfr 64 p 0 0
Hst :
⊢
offset_relge fr_envfr pp p 0 0
exists pp, 0
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p :
pp :
b :
blo, bhi :
Z
Hdom :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hb :
Inb, blo, bhi guard_chain_gosingle_definitionsfr_fnfr 64 p 0 0
Hst :
split ; exact Hp |
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p :
pp :
b :
blo, bhi :
Z
Hdom :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hb :
Inb, blo, bhi guard_chain_gosingle_definitionsfr_fnfr 64 p 0 0
Hst :
split ; reflexivity |
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p :
pp :
b :
blo, bhi :
Z
Hdom :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hb :
Inb, blo, bhi guard_chain_gosingle_definitionsfr_fnfr 64 p 0 0
Hst :
split ; lia |
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p :
pp :
b :
blo, bhi :
Z
Hdom :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hb :
Inb, blo, bhi guard_chain_gosingle_definitionsfr_fnfr 64 p 0 0
Hst :
rewrite Z.add_0_r
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p :
pp :
b :
blo, bhi :
Z
Hdom :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hb :
Inb, blo, bhi guard_chain_gosingle_definitionsfr_fnfr 64 p 0 0
Hst :
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros p pp b blo bhi Hp Hdom Hb Hst
rewrite guard_chain_eq in Hb
refine chain_go_sound64 p 0 0 pp Hdom _ b blo bhi Hb Hst
intros _
exists pp, 0
split ; exact Hp |
split ; reflexivity |
split ; lia |
rewrite Z.add_0_r
reflexivity
pointer_distance as an equation, for the same reason as guard_chain_eq.
∀ once p p1
Explore proof 2 tactics
Initial goal
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
⊢
intros once p p1
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
⊢
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros once p p1
reflexivity
Two values p and p1 that read as pointers pp and pp1, whose guard chains share an exact base d apart (pointer_distance/4), have one capability, and addresses d apart, modulo 2^64, where their single definitions dominate the point. The reuse forms use it to give a renewed pointer its source's capability.
∀ p p1 pp pp1 d
∀y, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
∀y, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
pointer_distancesingle_definitionsfr_fnfr p p1 = Somed
Explore proof 28 tactics
Initial goal
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
⊢
∀p p1 : value pp pp1 : ptr d : Z, value_xge fr_envfr P p = SomeWPtrpp → value_xge fr_envfr P p1 = SomeWPtrpp1 → ∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y → ∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y → pointer_distancesingle_definitionsfr_fnfr p p1 = Somed → ptr_cappp = ptr_cappp1 ∧ ptr_addrpp mod 2 ^ 64 = ptr_addrpp1 + d mod 2 ^ 64
intros p p1 pp pp1 d Hp Hp1 Hd Hd1 H
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
d :
Z
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
H :
pointer_distancesingle_definitionsfr_fnfr p p1 = Somed
rewrite pointer_distance_eq in H
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
d :
Z
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
H :
Somen, k
⇒
None
⇒
None
=
Somed
destruct first_some_in_ _ _ _ _ H as el & Hel & Hf
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
d :
Z
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
H :
Somen, k
⇒
None
⇒
None
=
Somed
el :
value × Z × Z
Hel :
Inel guard_chainsingle_definitionsfr_fnfr p
Hf :
Somen, k
⇒
None
⇒
None
=
Somed
destruct el as n0 | c0 | g0 k0 k0′ ; unfold exact_base in Hf ; try discriminate Hf
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
d :
Z
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
H :
Somen, k
⇒
None
⇒
None
=
Somed
n0 :
k0, k0′ :
Z
Hel :
InTmpn0, k0, k0′ guard_chainsingle_definitionsfr_fnfr p
Hf :
Somen, k
⇒
None
⇒
None
=
Somed
destruct k0 =? k0′ && once_hassingle_definitionsfr_fnfr n0 eqn: E0 ; | discriminate Hf
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
d :
Z
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
H :
Somen, k
⇒
None
⇒
None
=
Somed
n0 :
k0, k0′ :
Z
Hel :
InTmpn0, k0, k0′ guard_chainsingle_definitionsfr_fnfr p
E0 :
k0 =? k0′ && once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somed
apply andb_true_iff in E0 as Ek0 Ho
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
d :
Z
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
H :
Somen, k
⇒
None
⇒
None
=
Somed
n0 :
k0, k0′ :
Z
Hel :
InTmpn0, k0, k0′ guard_chainsingle_definitionsfr_fnfr p
Ek0 :
k0 =? k0′ = true
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somed
apply Z.eqb_eq in Ek0
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
d :
Z
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
H :
Somen, k
⇒
None
⇒
None
=
Somed
n0 :
k0, k0′ :
Z
Hel :
InTmpn0, k0, k0′ guard_chainsingle_definitionsfr_fnfr p
Ek0 :
k0 = k0′
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somed
subst k0′
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
d :
Z
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
H :
Somen, k
⇒
None
⇒
None
=
Somed
n0 :
k0 :
Z
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somed
destruct first_some_in_ _ _ _ _ Hf as el1 & Hel1 & Hf1
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
d :
Z
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
H :
Somen, k
⇒
None
⇒
None
=
Somed
n0 :
k0 :
Z
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somed
el1 :
value × Z × Z
Hel1 :
Inel1 guard_chainsingle_definitionsfr_fnfr p1
destruct el1 as n1 | c1 | g1 k1 k1′ ; try discriminate Hf1
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
d :
Z
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
H :
Somen, k
⇒
None
⇒
None
=
Somed
n0 :
k0 :
Z
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somed
n1 :
k1, k1′ :
Z
Hel1 :
InTmpn1, k1, k1′ guard_chainsingle_definitionsfr_fnfr p1
Hf1 :
destruct name_eqbn1 n0 && k1 =? k1′ eqn: E1 ; | discriminate Hf1
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
d :
Z
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
H :
Somen, k
⇒
None
⇒
None
=
Somed
n0 :
k0 :
Z
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somed
n1 :
k1, k1′ :
Z
Hel1 :
InTmpn1, k1, k1′ guard_chainsingle_definitionsfr_fnfr p1
E1 :
name_eqbn1 n0 && k1 =? k1′ = true
Hf1 :
Somek0 − k1 = Somed
injection Hf1 as ←
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
k0, k1 :
Z
H :
Somen, k
⇒
None
⇒
None
=
Somek0 − k1
n0 :
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somek0 − k1
n1 :
k1′ :
Z
Hel1 :
InTmpn1, k1, k1′ guard_chainsingle_definitionsfr_fnfr p1
E1 :
name_eqbn1 n0 && k1 =? k1′ = true
apply andb_true_iff in E1 as En Ek
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
k0, k1 :
Z
H :
Somen, k
⇒
None
⇒
None
=
Somek0 − k1
n0 :
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somek0 − k1
n1 :
k1′ :
Z
Hel1 :
InTmpn1, k1, k1′ guard_chainsingle_definitionsfr_fnfr p1
En :
name_eqbn1 n0 = true
Ek :
k1 =? k1′ = true
apply name_eqb_true in En
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
k0, k1 :
Z
H :
Somen, k
⇒
None
⇒
None
=
Somek0 − k1
n0 :
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somek0 − k1
n1 :
k1′ :
Z
Hel1 :
InTmpn1, k1, k1′ guard_chainsingle_definitionsfr_fnfr p1
En :
n1 = n0
Ek :
k1 =? k1′ = true
apply Z.eqb_eq in Ek
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
k0, k1 :
Z
H :
Somen, k
⇒
None
⇒
None
=
Somek0 − k1
n0 :
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somek0 − k1
n1 :
k1′ :
Z
Hel1 :
InTmpn1, k1, k1′ guard_chainsingle_definitionsfr_fnfr p1
En :
n1 = n0
Ek :
k1 = k1′
subst n1 k1′
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
k0, k1 :
Z
H :
Somen, k
⇒
None
⇒
None
=
Somek0 − k1
n0 :
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somek0 − k1
Hel1 :
InTmpn0, k1, k1 guard_chainsingle_definitionsfr_fnfr p1
assert Hst : stablesingle_definitionsfr_fnfr Tmpn0 by intros y E ; injection E as ← ; exact Ho
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
k0, k1 :
Z
H :
Somen, k
⇒
None
⇒
None
=
Somek0 − k1
n0 :
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somek0 − k1
Hel1 :
InTmpn0, k1, k1 guard_chainsingle_definitionsfr_fnfr p1
Hst :
destruct guard_chain_sound_ _ _ _ _ Hp Hd Hel Hst as pb & x & Hpb & Hc & Hx & Ha
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
k0, k1 :
Z
H :
Somen, k
⇒
None
⇒
None
=
Somek0 − k1
n0 :
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somek0 − k1
Hel1 :
InTmpn0, k1, k1 guard_chainsingle_definitionsfr_fnfr p1
Hst :
pb :
x :
Z
Hx :
k0 ≤ x ≤ k0
destruct guard_chain_sound_ _ _ _ _ Hp1 Hd1 Hel1 Hst as pb′ & x1 & Hpb′ & Hc1 & Hx1 & Ha1
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
k0, k1 :
Z
H :
Somen, k
⇒
None
⇒
None
=
Somek0 − k1
n0 :
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somek0 − k1
Hel1 :
InTmpn0, k1, k1 guard_chainsingle_definitionsfr_fnfr p1
Hst :
pb :
x :
Z
Hx :
k0 ≤ x ≤ k0
pb′ :
x1 :
Z
Hx1 :
k1 ≤ x1 ≤ k1
rewrite Hpb in Hpb′
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
k0, k1 :
Z
H :
Somen, k
⇒
None
⇒
None
=
Somek0 − k1
n0 :
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somek0 − k1
Hel1 :
InTmpn0, k1, k1 guard_chainsingle_definitionsfr_fnfr p1
Hst :
pb :
x :
Z
Hx :
k0 ≤ x ≤ k0
pb′ :
x1 :
Z
Hx1 :
k1 ≤ x1 ≤ k1
injection Hpb′ as ←
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
k0, k1 :
Z
H :
Somen, k
⇒
None
⇒
None
=
Somek0 − k1
n0 :
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somek0 − k1
Hel1 :
InTmpn0, k1, k1 guard_chainsingle_definitionsfr_fnfr p1
Hst :
pb :
x :
Z
Hx :
k0 ≤ x ≤ k0
x1 :
Z
Hx1 :
k1 ≤ x1 ≤ k1
assert x = k0 by lia
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
k0, k1 :
Z
H :
Somen, k
⇒
None
⇒
None
=
Somek0 − k1
n0 :
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somek0 − k1
Hel1 :
InTmpn0, k1, k1 guard_chainsingle_definitionsfr_fnfr p1
Hst :
pb :
x :
Z
Hx :
k0 ≤ x ≤ k0
x1 :
Z
Hx1 :
k1 ≤ x1 ≤ k1
H0 :
x = k0
assert x1 = k1 by lia
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
k0, k1 :
Z
H :
Somen, k
⇒
None
⇒
None
=
Somek0 − k1
n0 :
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somek0 − k1
Hel1 :
InTmpn0, k1, k1 guard_chainsingle_definitionsfr_fnfr p1
Hst :
pb :
x :
Z
Hx :
k0 ≤ x ≤ k0
x1 :
Z
Hx1 :
k1 ≤ x1 ≤ k1
H0 :
x = k0
H1 :
x1 = k1
subst x x1
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
k0, k1 :
Z
H :
Somen, k
⇒
None
⇒
None
=
Somek0 − k1
n0 :
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somek0 − k1
Hel1 :
InTmpn0, k1, k1 guard_chainsingle_definitionsfr_fnfr p1
Hst :
pb :
Hx :
k0 ≤ k0 ≤ k0
Hx1 :
k1 ≤ k1 ≤ k1
split ; congruence |
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
k0, k1 :
Z
H :
Somen, k
⇒
None
⇒
None
=
Somek0 − k1
n0 :
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somek0 − k1
Hel1 :
InTmpn0, k1, k1 guard_chainsingle_definitionsfr_fnfr p1
Hst :
pb :
Hx :
k0 ≤ k0 ≤ k0
Hx1 :
k1 ≤ k1 ≤ k1
rewrite Ha , <- Z.add_mod_idemp_lptr_addrpp1 , Ha1 , Z.add_mod_idemp_l by lia
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
k0, k1 :
Z
H :
Somen, k
⇒
None
⇒
None
=
Somek0 − k1
n0 :
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somek0 − k1
Hel1 :
InTmpn0, k1, k1 guard_chainsingle_definitionsfr_fnfr p1
Hst :
pb :
Hx :
k0 ≤ k0 ≤ k0
Hx1 :
k1 ≤ k1 ≤ k1
f_equal
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
p, p1 :
pp, pp1 :
Hd :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hd1 :
∀y : name, p1 = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
k0, k1 :
Z
H :
Somen, k
⇒
None
⇒
None
=
Somek0 − k1
n0 :
Hel :
InTmpn0, k0, k0 guard_chainsingle_definitionsfr_fnfr p
Ho :
once_hassingle_definitionsfr_fnfr n0 = true
Hf :
=
Somek0 − k1
Hel1 :
InTmpn0, k1, k1 guard_chainsingle_definitionsfr_fnfr p1
Hst :
pb :
Hx :
k0 ≤ k0 ≤ k0
Hx1 :
k1 ≤ k1 ≤ k1
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros p p1 pp pp1 d Hp Hp1 Hd Hd1 H
rewrite pointer_distance_eq in H
destruct first_some_in_ _ _ _ _ H as el & Hel & Hf
destruct el as n0 | c0 | g0 k0 k0′ ; unfold exact_base in Hf ; try discriminate Hf
destruct k0 =? k0′ && once_hassingle_definitionsfr_fnfr n0 eqn: E0 ; | discriminate Hf
apply andb_true_iff in E0 as Ek0 Ho
apply Z.eqb_eq in Ek0
subst k0′
destruct first_some_in_ _ _ _ _ Hf as el1 & Hel1 & Hf1
destruct el1 as n1 | c1 | g1 k1 k1′ ; try discriminate Hf1
destruct name_eqbn1 n0 && k1 =? k1′ eqn: E1 ; | discriminate Hf1
injection Hf1 as ←
apply andb_true_iff in E1 as En Ek
apply name_eqb_true in En
apply Z.eqb_eq in Ek
subst n1 k1′
assert Hst : stablesingle_definitionsfr_fnfr Tmpn0 by intros y E ; injection E as ← ; exact Ho
destruct guard_chain_sound_ _ _ _ _ Hp Hd Hel Hst as pb & x & Hpb & Hc & Hx & Ha
destruct guard_chain_sound_ _ _ _ _ Hp1 Hd1 Hel1 Hst as pb′ & x1 & Hpb′ & Hc1 & Hx1 & Ha1
rewrite Hpb in Hpb′
injection Hpb′ as ←
assert x = k0 by lia
assert x1 = k1 by lia
subst x x1
split ; congruence |
rewrite Ha , <- Z.add_mod_idemp_lptr_addrpp1 , Ha1 , Z.add_mod_idemp_l by lia
f_equal
lia
The hull of a pointer's live facts
Each span from l1 to h1 that hull_covered/7 reads off a live fact is a check that passed, of the capability of the access pointer pp, at its address plus the span's bounds, where the live facts hold (facts_hold) and their pointers dominate the point. The fact's pointer and the access's are a known distance apart (pointer_distance_sound).
∀ live p pp l1 h1 r1
facts_holdge m fr_envfr live
∀fb y, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
∀y, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Inl1, h1, r1
flat_map
λ f ⇒
Somed
⇒
else
[ ]
None
⇒
[ ]
live
near_offsetl1 = true ∧ near_offseth1 = true ∧ ∃al1, access_resm raw_addressptr_addrpp l1 ptr_cappp h1 − l1 r1 al1 = Someok
Explore proof 23 tactics
Initial goal
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
⊢
facts_holdge m fr_envfr live
→
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
→
→
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
→
Inl1, h1, r1
flat_map
Somed
⇒
else
[ ]
None
⇒
[ ]
live
→
near_offsetl1 = true ∧ near_offseth1 = true ∧ ∃al1 : Z, access_resm raw_addressptr_addrpp l1 ptr_cappp h1 − l1 r1 al1 = Someok
intros live p pp l1 h1 r1 Hl Hdom Hp Hdp Hsp
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
l1, h1 :
Z
r1 :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hsp :
Inl1, h1, r1
flat_map
Somed
⇒
else
[ ]
None
⇒
[ ]
live
⊢
near_offsetl1 = true ∧ near_offseth1 = true ∧ ∃al1 : Z, access_resm raw_addressptr_addrpp l1 ptr_cappp h1 − l1 r1 al1 = Someok
apply in_flat_map in Hsp as f & Hf & Hsp
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
l1, h1 :
Z
r1 :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
Hsp :
Inl1, h1, r1
Somed
⇒
else
[ ]
None
⇒
[ ]
⊢
near_offsetl1 = true ∧ near_offseth1 = true ∧ ∃al1 : Z, access_resm raw_addressptr_addrpp l1 ptr_cappp h1 − l1 r1 al1 = Someok
destruct pointer_distancesingle_definitionsfr_fnfr f_pf p as d | eqn: Ed ; | contradiction
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
l1, h1 :
Z
r1 :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
Hsp :
Inl1, h1, r1
else
[ ]
⊢
near_offsetl1 = true ∧ near_offseth1 = true ∧ ∃al1 : Z, access_resm raw_addressptr_addrpp l1 ptr_cappp h1 − l1 r1 al1 = Someok
cbv zeta in Hsp
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
l1, h1 :
Z
r1 :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
Hsp :
Inl1, h1, r1
else
[ ]
⊢
near_offsetl1 = true ∧ near_offseth1 = true ∧ ∃al1 : Z, access_resm raw_addressptr_addrpp l1 ptr_cappp h1 − l1 r1 al1 = Someok
destruct near_offsetd && near_offsetf_lof + d && near_offsetf_hif + d eqn: En ; | contradiction
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
l1, h1 :
Z
r1 :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
En :
near_offsetd && near_offsetf_lof + d && near_offsetf_hif + d = true
⊢
near_offsetl1 = true ∧ near_offseth1 = true ∧ ∃al1 : Z, access_resm raw_addressptr_addrpp l1 ptr_cappp h1 − l1 r1 al1 = Someok
destruct Hsp as E |
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
l1, h1 :
Z
r1 :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
En :
near_offsetd && near_offsetf_lof + d && near_offsetf_hif + d = true
⊢
near_offsetl1 = true ∧ near_offseth1 = true ∧ ∃al1 : Z, access_resm raw_addressptr_addrpp l1 ptr_cappp h1 − l1 r1 al1 = Someok
injection E as ← ← ←
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
En :
near_offsetd && near_offsetf_lof + d && near_offsetf_hif + d = true
⊢
near_offsetf_lof + d = true ∧ near_offsetf_hif + d = true ∧ ∃al1 : Z, access_resm raw_addressptr_addrpp f_lof + d ptr_cappp f_hif + d − f_lof + d f_rf al1 = Someok
apply andb_true_iff in En as En Eh
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
En :
near_offsetd && near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
⊢
near_offsetf_lof + d = true ∧ near_offsetf_hif + d = true ∧ ∃al1 : Z, access_resm raw_addressptr_addrpp f_lof + d ptr_cappp f_hif + d − f_lof + d f_rf al1 = Someok
apply andb_true_iff in En as _ El
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
El :
near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
⊢
near_offsetf_lof + d = true ∧ near_offsetf_hif + d = true ∧ ∃al1 : Z, access_resm raw_addressptr_addrpp f_lof + d ptr_cappp f_hif + d − f_lof + d f_rf al1 = Someok
split ; exact El |
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
El :
near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
⊢
near_offsetf_hif + d = true ∧ ∃al1 : Z, access_resm raw_addressptr_addrpp f_lof + d ptr_cappp f_hif + d − f_lof + d f_rf al1 = Someok
split ; exact Eh |
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
El :
near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
⊢
∃al1 : Z, access_resm raw_addressptr_addrpp f_lof + d ptr_cappp f_hif + d − f_lof + d f_rf al1 = Someok
destruct Hlf Hf as pf & _ & Hpf & Hc
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
El :
near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
pf :
Hc :
check_passesm pf f_lof f_hif f_rf f_alf
⊢
∃al1 : Z, access_resm raw_addressptr_addrpp f_lof + d ptr_cappp f_hif + d − f_lof + d f_rf al1 = Someok
destruct pointer_distance_sound_ _ _ _ _ Hpf Hp λy ⇒ Hdomf y Hf Hdp Ed as Hcap Haddr
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
El :
near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
pf :
Hc :
check_passesm pf f_lof f_hif f_rf f_alf
⊢
∃al1 : Z, access_resm raw_addressptr_addrpp f_lof + d ptr_cappp f_hif + d − f_lof + d f_rf al1 = Someok
exists f_alf
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
El :
near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
pf :
Hc :
check_passesm pf f_lof f_hif f_rf f_alf
⊢
access_resm raw_addressptr_addrpp f_lof + d ptr_cappp f_hif + d − f_lof + d f_rf f_alf = Someok
unfold check_passes in Hc
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
El :
near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
pf :
Hc :
access_resm raw_addressptr_addrpf f_lof ptr_cappf f_hif − f_lof f_rf f_alf = Someok
⊢
access_resm raw_addressptr_addrpp f_lof + d ptr_cappp f_hif + d − f_lof + d f_rf f_alf = Someok
replace f_hif + d − f_lof + d with f_hif − f_lof by lia
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
El :
near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
pf :
Hc :
access_resm raw_addressptr_addrpf f_lof ptr_cappf f_hif − f_lof f_rf f_alf = Someok
⊢
access_resm raw_addressptr_addrpp f_lof + d ptr_cappp f_hif − f_lof f_rf f_alf = Someok
replace raw_addressptr_addrpp f_lof + d with raw_addressptr_addrpf f_lof
2 openge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
El :
near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
pf :
Hc :
access_resm raw_addressptr_addrpf f_lof ptr_cappf f_hif − f_lof f_rf f_alf = Someok
⊢
access_resm raw_addressptr_addrpf f_lof ptr_cappp f_hif − f_lof f_rf f_alf = Someok
focused goal
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
El :
near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
pf :
Hc :
access_resm raw_addressptr_addrpf f_lof ptr_cappf f_hif − f_lof f_rf f_alf = Someok
⊢
raw_addressptr_addrpf f_lof = raw_addressptr_addrpp f_lof + d
–rewrite <- Hcap
2 openge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
El :
near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
pf :
Hc :
access_resm raw_addressptr_addrpf f_lof ptr_cappf f_hif − f_lof f_rf f_alf = Someok
⊢
access_resm raw_addressptr_addrpf f_lof ptr_cappf f_hif − f_lof f_rf f_alf = Someok
deferred goal
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
El :
near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
pf :
Hc :
access_resm raw_addressptr_addrpf f_lof ptr_cappf f_hif − f_lof f_rf f_alf = Someok
⊢
raw_addressptr_addrpf f_lof = raw_addressptr_addrpp f_lof + d
exact Hc
deferred goal
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
El :
near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
pf :
Hc :
access_resm raw_addressptr_addrpf f_lof ptr_cappf f_hif − f_lof f_rf f_alf = Someok
⊢
raw_addressptr_addrpf f_lof = raw_addressptr_addrpp f_lof + d
–unfold raw_address
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
El :
near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
pf :
Hc :
access_resm raw_addressptr_addrpf f_lof ptr_cappf f_hif − f_lof f_rf f_alf = Someok
rewrite <- Z.add_mod_idemp_l , Haddr , Z.add_mod_idemp_l by lia
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
El :
near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
pf :
Hc :
access_resm raw_addressptr_addrpf f_lof ptr_cappf f_hif − f_lof f_rf f_alf = Someok
f_equal
ge :
md :
fr :
m :
Memory.mem
l :
k :
Z
Hmd :
Hr :
is_reachablefn_domsfr_fnfr l = true
Hs :
scope_plainge fr m
Hpt :
point_sitefr_fnfr fr_atfr = Somel, k
live :
listfact
p :
pp :
Hl :
facts_holdge m fr_envfr live
Hdom :
∀fb : fact y : name, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
Hdp :
∀y : name, p = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
f :
Hf :
Inf live
d :
Z
Ed :
pointer_distancesingle_definitionsfr_fnfr f_pf p = Somed
El :
near_offsetf_lof + d = true
Eh :
near_offsetf_hif + d = true
pf :
Hc :
access_resm raw_addressptr_addrpf f_lof ptr_cappf f_hif − f_lof f_rf f_alf = Someok
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros live p pp l1 h1 r1 Hl Hdom Hp Hdp Hsp
apply in_flat_map in Hsp as f & Hf & Hsp
destruct pointer_distancesingle_definitionsfr_fnfr f_pf p as d | eqn: Ed ; | contradiction
cbv zeta in Hsp
destruct near_offsetd && near_offsetf_lof + d && near_offsetf_hif + d eqn: En ; | contradiction
destruct Hsp as E |
injection E as ← ← ←
apply andb_true_iff in En as En Eh
apply andb_true_iff in En as _ El
split ; exact El |
split ; exact Eh |
destruct Hlf Hf as pf & _ & Hpf & Hc
destruct pointer_distance_sound_ _ _ _ _ Hpf Hp λy ⇒ Hdomf y Hf Hdp Ed as Hcap Haddr
exists f_alf
unfold check_passes in Hc
replace raw_addressptr_addrpp f_lof + d with raw_addressptr_addrpf f_lof
–rewrite <- Hcap
exact Hc
A raw access i through the proof q that the pass accepts by hull_covered/7 does not step to unchecked, where memory lies in the address space, the live facts hold and their pointers' single definitions dominate the point. The span starting at or below the access and the span ending at or above it are checks of one capability that passed (hull_span_passes), so the access's own check passes (cap_access_hull).
∀ i q fa live why
facts_holdge m fr_envfr live
∀fb y, Infb live → f_pfb = Tmpy → once_hassingle_definitionsfr_fnfr y = true → dominatingfr_fnfr l k y
fact_ofq live = Somefa
hull_coveredi q f_pfa f_lofa f_alfa live single_definitionsfr_fnfr = true
Proof 45 steps Qed
intros i q fa live why Hfit Hl Hdom Hf H
destruct fact_of_in_ _ _ Hf as Hfa Hq
destruct Hlfa Hfa as pp & Eq & Hp & Hc
rewrite Hq in Eq
pose proof λy ⇒ Hdomfa y Hfa as Hdp
unfold hull_covered in H
destruct raw_accessi as q′ x off need | eqn: Ei ; | discriminate H
pose proof access_size_align_posx as Hsz Haa
pose proof access_align_dividesx as Hdv
destruct access_size_alignx as size aa eqn: Ex
simpl in Hsz , Haa , Hdv
cbv zeta in H
repeat rewrite andb_true_iff in H
destruct H as Hq′ & Hal & Hoa & _ & _ & H1 & H2 & Hneed
apply name_eqb_true in Hq'
subst q'
apply Z.eqb_eq in Hal
apply Z.eqb_eq in Hoa
apply existsb_exists in H1 as l1 h1 r1 & Hs1 & Hl1
apply Z.leb_le in Hl1
apply existsb_exists in H2 as l2 h2 r2 & Hs2 & Hh2
apply Z.leb_le in Hh2
destruct hull_span_passes_ _ _ _ _ _ Hl Hdom Hp Hdp Hs1 as _ & Hn1 & al1 & Hc1
destruct hull_span_passes_ _ _ _ _ _ Hl Hdom Hp Hdp Hs2 as Hn2 & _ & al2 & Hc2
unfold near_offset in Hn1 , Hn2
apply andb_true_iff in Hn1 as Hn1 _ , Hn2 as _ Hn2
apply Z.leb_le in Hn1 , Hn2
apply access_ok_not_uncheckedge fr m i q x off need pp why Ei Eq
rewrite Ex
simpl
unfold access_res in *
refine cap_access_hull_ _ _ l1 h1 − l1 r1 al1 l2 h2 − l2 r2 al2 _ _ _ _ Hfit Hc1 Hc2 _ Hn2 Hl1 _ Hsz _ _ ; lia | lia | |
The access is aligned: the fact's check was, at an alignment aa divides.
–unfold check_passes , access_res in Hc
apply cap_access_aligned in Hc
unfold raw_address in *
rewrite <- Znumtheory.Zmod_div_modaa 2 ^ 64 by auto ; lia
apply aligned_add ; exact Haa | | exact Hoa
rewrite Znumtheory.Zmod_div_modaa 2 ^ 64 by auto ; lia
exact aligned_divisor_ _ _ Haa Hc Hal
The rights: a read, or a write some span's write check allows.
–destruct need ; left ; reflexivity | right
apply existsb_exists in Hneed as l3 h3 r3 & Hs3 & Hr3
destruct r3 ; discriminate Hr3 |
destruct hull_span_passes_ _ _ _ _ _ Hl Hdom Hp Hdp Hs3 as _ & _ & al3 & Hc3
eauto
No unchecked access through the hull, along every run
The frame lemmas carried along every run of the machine of a runtime R. It joins Persistence.v's invariant, which says the hull's facts hold and dominate the point, with Single.v's, which says the single definitions there replay. Each instantiates MachineR on its own, and an instance's mstep is an inductive of its own, so a run of one is carried over to the other (mreachable_same).
A step of Persistence.v's machine instance is a step of Single.v's.
Explore proof 2 tactics
Initial goal
⊢
∀ge : genv st st′ : P.I.RM.mstate, P.I.RM.mstepge st st′ → S.ID.RM.mstepge st st′
intros ge st st′ H
⊢
S.ID.RM.mstepge st st′
destruct H ; econstructor ; eassumption
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge st st′ H
destruct H ; econstructor ; eassumption
A run of Persistence.v's machine instance is a run of Single.v's, so both invariants hold of every state it reaches.
Explore proof 6 tactics
Initial goal
⊢
∀ge : genv st st′ : P.I.RM.mstate, P.I.RM.mreachablege st st′ → S.ID.RM.mreachablege st st′
intros ge st st′ H
⊢
S.ID.RM.mreachablege st st′
induction H as st st′ H | st | st1 st2 st3 _ IH1 _ IH2
3 open⊢
S.ID.RM.mreachablege st st′
focused goal
ge :
st :
⊢
S.ID.RM.mreachablege st st
focused goal
⊢
S.ID.RM.mreachablege st1 st3
–apply rt_step
3 open⊢
S.ID.RM.mstepge st st′
deferred goal
ge :
st :
⊢
S.ID.RM.mreachablege st st
deferred goal
⊢
S.ID.RM.mreachablege st1 st3
exact mstep_same_ _ _ H
2 opendeferred goal
ge :
st :
⊢
S.ID.RM.mreachablege st st
deferred goal
⊢
S.ID.RM.mreachablege st1 st3
–apply rt_refl
deferred goal
⊢
S.ID.RM.mreachablege st1 st3
–exact rt_trans_ _ _ _ _ IH1 IH2
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge st st′ H
induction H as st st′ H | st | st1 st2 st3 _ IH1 _ IH2
–apply rt_step
exact mstep_same_ _ _ H
–apply rt_refl
–exact rt_trans_ _ _ _ _ IH1 IH2
In every state c a run reaches from a call of a function f of a checked_module md, started in a memory where the runtime is ready, a frame that is not doomed runs no raw access, and no raw call, to an unchecked outcome, hull_covered/7 included. Every runtime spares the pass's facts at safepoints (spares_any; see The evidence invariant over runs).
∀ ge md f xs fr m fuel s0 c s l i rest j why
ge_modulege = md
ge_freege = R.free
InIFuncf md
call_framef xs = Somefr
R.readys0 m
P.I.RM.mreachablege mkConfigfr [ ] m fuel, s0 c, s
raw_accessi ≠ None ∨ ∃r cl args, i = RawCallr cl args
Explore proof 13 tactics
Initial goal
⊢
∀ge : genv md : module f : func xs : listword fr : frame m : Memory.mem fuel : Z s0 : R.state c : config s : R.state l : name i : inst rest : listinst j : jump why : reason, checked_modulemd → ge_modulege = md → ge_freege = R.free → InIFuncf md → call_framef xs = Somefr → R.readys0 m → P.I.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s0 c, s → fr_doomedc_framec = None → fr_atc_framec = Execl i :: rest j → raw_accessi ≠ None ∨ ∃r : call_result cl : value args : listarg, i = RawCallr cl args → inst_stepge c_framec c_memc i ≠ SomeIStopUncheckedwhy
intros ge md f xs fr m fuel s0 c s l i rest j why Hmd Hge Hfree Hin Hcf H0 Hreach Hd Ha Hi
ge :
md :
f :
xs :
listword
fr :
m :
Memory.mem
fuel :
Z
s0 :
R.state
c :
s :
R.state
l :
i :
rest :
listinst
j :
why :
Hmd :
Hge :
ge_modulege = md
Hfree :
ge_freege = R.free
Hin :
InIFuncf md
Hcf :
call_framef xs = Somefr
H0 :
R.readys0 m
Hreach :
P.I.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s0 c, s
Hi :
raw_accessi ≠ None ∨ ∃r : call_result cl : value args : listarg, i = RawCallr cl args
destruct P.run_access_not_unchecked_ _ _ _ _ _ _ _ _ _ _ _ _ _ why Hmd Hge Hfree Hin Hcf H0 Hreach Hd Ha Hi as Hn | b & k & live & fa & q & Hb & Hk & Hl & Hdom & Hfa & Hh ; exact Hn |
ge :
md :
f :
xs :
listword
fr :
m :
Memory.mem
fuel :
Z
s0 :
R.state
c :
s :
R.state
l :
i :
rest :
listinst
j :
why :
Hmd :
Hge :
ge_modulege = md
Hfree :
ge_freege = R.free
Hin :
InIFuncf md
Hcf :
call_framef xs = Somefr
H0 :
R.readys0 m
Hreach :
P.I.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s0 c, s
Hi :
raw_accessi ≠ None ∨ ∃r : call_result cl : value args : listarg, i = RawCallr cl args
b :
k :
nat
live :
listfact
fa :
q :
Hb :
find_blockl fn_blocksfr_fnc_framec = Someb
Hk :
i :: rest = skipnk b_instsb
Hl :
facts_holdge c_memc fr_envc_framec live
Hfa :
fact_ofq live = Somefa
pose proof S.run_sinv_ _ _ _ _ _ _ _ _ Hmd Hge Hfree Hin Hcf H0 mreachable_same_ _ _ Hreach as Hsh Hsc _
ge :
md :
f :
xs :
listword
fr :
m :
Memory.mem
fuel :
Z
s0 :
R.state
c :
s :
R.state
l :
i :
rest :
listinst
j :
why :
Hmd :
Hge :
ge_modulege = md
Hfree :
ge_freege = R.free
Hin :
InIFuncf md
Hcf :
call_framef xs = Somefr
H0 :
R.readys0 m
Hreach :
P.I.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s0 c, s
Hi :
raw_accessi ≠ None ∨ ∃r : call_result cl : value args : listarg, i = RawCallr cl args
b :
k :
nat
live :
listfact
fa :
q :
Hb :
find_blockl fn_blocksfr_fnc_framec = Someb
Hk :
i :: rest = skipnk b_instsb
Hl :
facts_holdge c_memc fr_envc_framec live
Hfa :
fact_ofq live = Somefa
Hsc :
fr_doomedc_framefstc, s ≠ None ∨ scope_holdsge c_framefstc, s c_memfstc, s
simpl in Hsh , Hsc
ge :
md :
f :
xs :
listword
fr :
m :
Memory.mem
fuel :
Z
s0 :
R.state
c :
s :
R.state
l :
i :
rest :
listinst
j :
why :
Hmd :
Hge :
ge_modulege = md
Hfree :
ge_freege = R.free
Hin :
InIFuncf md
Hcf :
call_framef xs = Somefr
H0 :
R.readys0 m
Hreach :
P.I.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s0 c, s
Hi :
raw_accessi ≠ None ∨ ∃r : call_result cl : value args : listarg, i = RawCallr cl args
b :
k :
nat
live :
listfact
fa :
q :
Hb :
find_blockl fn_blocksfr_fnc_framec = Someb
Hk :
i :: rest = skipnk b_instsb
Hl :
facts_holdge c_memc fr_envc_framec live
Hfa :
fact_ofq live = Somefa
Hsc :
fr_doomedc_framec ≠ None ∨ scope_holdsge c_framec c_memc
destruct Hsc as Hsc | Hsc ; congruence |
ge :
md :
f :
xs :
listword
fr :
m :
Memory.mem
fuel :
Z
s0 :
R.state
c :
s :
R.state
l :
i :
rest :
listinst
j :
why :
Hmd :
Hge :
ge_modulege = md
Hfree :
ge_freege = R.free
Hin :
InIFuncf md
Hcf :
call_framef xs = Somefr
H0 :
R.readys0 m
Hreach :
P.I.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s0 c, s
Hi :
raw_accessi ≠ None ∨ ∃r : call_result cl : value args : listarg, i = RawCallr cl args
b :
k :
nat
live :
listfact
fa :
q :
Hb :
find_blockl fn_blocksfr_fnc_framec = Someb
Hk :
i :: rest = skipnk b_instsb
Hl :
facts_holdge c_memc fr_envc_framec live
Hfa :
fact_ofq live = Somefa
Hsc :
scope_holdsge c_framec c_memc
destruct Hsh as Hinf Hsh
ge :
md :
f :
xs :
listword
fr :
m :
Memory.mem
fuel :
Z
s0 :
R.state
c :
s :
R.state
l :
i :
rest :
listinst
j :
why :
Hmd :
Hge :
ge_modulege = md
Hfree :
ge_freege = R.free
Hin :
InIFuncf md
Hcf :
call_framef xs = Somefr
H0 :
R.readys0 m
Hreach :
P.I.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s0 c, s
Hi :
raw_accessi ≠ None ∨ ∃r : call_result cl : value args : listarg, i = RawCallr cl args
b :
k :
nat
live :
listfact
fa :
q :
Hb :
find_blockl fn_blocksfr_fnc_framec = Someb
Hk :
i :: rest = skipnk b_instsb
Hl :
facts_holdge c_memc fr_envc_framec live
Hfa :
fact_ofq live = Somefa
Hsh :
Enterl from
⇒
is_reachablefn_domsfr_fnc_framec l = true ∧ from = None → entry_labelfr_fnc_framec = Somel
Hsc :
scope_holdsge c_framec c_memc
rewrite Ha in Hsh
ge :
md :
f :
xs :
listword
fr :
m :
Memory.mem
fuel :
Z
s0 :
R.state
c :
s :
R.state
l :
i :
rest :
listinst
j :
why :
Hmd :
Hge :
ge_modulege = md
Hfree :
ge_freege = R.free
Hin :
InIFuncf md
Hcf :
call_framef xs = Somefr
H0 :
R.readys0 m
Hreach :
P.I.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s0 c, s
Hi :
raw_accessi ≠ None ∨ ∃r : call_result cl : value args : listarg, i = RawCallr cl args
b :
k :
nat
live :
listfact
fa :
q :
Hb :
find_blockl fn_blocksfr_fnc_framec = Someb
Hk :
i :: rest = skipnk b_instsb
Hl :
facts_holdge c_memc fr_envc_framec live
Hfa :
fact_ofq live = Somefa
Hsh :
Hsc :
scope_holdsge c_framec c_memc
destruct Hsh as Hr _
ge :
md :
f :
xs :
listword
fr :
m :
Memory.mem
fuel :
Z
s0 :
R.state
c :
s :
R.state
l :
i :
rest :
listinst
j :
why :
Hmd :
Hge :
ge_modulege = md
Hfree :
ge_freege = R.free
Hin :
InIFuncf md
Hcf :
call_framef xs = Somefr
H0 :
R.readys0 m
Hreach :
P.I.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s0 c, s
Hi :
raw_accessi ≠ None ∨ ∃r : call_result cl : value args : listarg, i = RawCallr cl args
b :
k :
nat
live :
listfact
fa :
q :
Hb :
find_blockl fn_blocksfr_fnc_framec = Someb
Hk :
i :: rest = skipnk b_instsb
Hl :
facts_holdge c_memc fr_envc_framec live
Hfa :
fact_ofq live = Somefa
Hr :
is_reachablefn_domsfr_fnc_framec l = true
Hsc :
scope_holdsge c_framec c_memc
pose proof P.I.RM.mreachable_ready_ _ _ Hfree Hreach H0 as Hready
ge :
md :
f :
xs :
listword
fr :
m :
Memory.mem
fuel :
Z
s0 :
R.state
c :
s :
R.state
l :
i :
rest :
listinst
j :
why :
Hmd :
Hge :
ge_modulege = md
Hfree :
ge_freege = R.free
Hin :
InIFuncf md
Hcf :
call_framef xs = Somefr
H0 :
R.readys0 m
Hreach :
P.I.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s0 c, s
Hi :
raw_accessi ≠ None ∨ ∃r : call_result cl : value args : listarg, i = RawCallr cl args
b :
k :
nat
live :
listfact
fa :
q :
Hb :
find_blockl fn_blocksfr_fnc_framec = Someb
Hk :
i :: rest = skipnk b_instsb
Hl :
facts_holdge c_memc fr_envc_framec live
Hfa :
fact_ofq live = Somefa
Hr :
is_reachablefn_domsfr_fnc_framec l = true
Hsc :
scope_holdsge c_framec c_memc
Hready :
pose proof R.address_space_ _ Hready as Hfit
ge :
md :
f :
xs :
listword
fr :
m :
Memory.mem
fuel :
Z
s0 :
R.state
c :
s :
R.state
l :
i :
rest :
listinst
j :
why :
Hmd :
Hge :
ge_modulege = md
Hfree :
ge_freege = R.free
Hin :
InIFuncf md
Hcf :
call_framef xs = Somefr
H0 :
R.readys0 m
Hreach :
P.I.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s0 c, s
Hi :
raw_accessi ≠ None ∨ ∃r : call_result cl : value args : listarg, i = RawCallr cl args
b :
k :
nat
live :
listfact
fa :
q :
Hb :
find_blockl fn_blocksfr_fnc_framec = Someb
Hk :
i :: rest = skipnk b_instsb
Hl :
facts_holdge c_memc fr_envc_framec live
Hfa :
fact_ofq live = Somefa
Hr :
is_reachablefn_domsfr_fnc_framec l = true
Hsc :
scope_holdsge c_framec c_memc
Hready :
Hfit :
objects_fitm_regionsc_memfstc, s
destruct skipn_cons_ _ _ _ _ eq_symHk as _ & _ & Hlen
ge :
md :
f :
xs :
listword
fr :
m :
Memory.mem
fuel :
Z
s0 :
R.state
c :
s :
R.state
l :
i :
rest :
listinst
j :
why :
Hmd :
Hge :
ge_modulege = md
Hfree :
ge_freege = R.free
Hin :
InIFuncf md
Hcf :
call_framef xs = Somefr
H0 :
R.readys0 m
Hreach :
P.I.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s0 c, s
Hi :
raw_accessi ≠ None ∨ ∃r : call_result cl : value args : listarg, i = RawCallr cl args
b :
k :
nat
live :
listfact
fa :
q :
Hb :
find_blockl fn_blocksfr_fnc_framec = Someb
Hk :
i :: rest = skipnk b_instsb
Hl :
facts_holdge c_memc fr_envc_framec live
Hfa :
fact_ofq live = Somefa
Hr :
is_reachablefn_domsfr_fnc_framec l = true
Hsc :
scope_holdsge c_framec c_memc
Hready :
Hfit :
objects_fitm_regionsc_memfstc, s
Hlen :
Sk ≤ Datatypes.lengthb_instsb%nat
assert Hpt : point_sitefr_fnc_framec fr_atc_framec = Somel, Z.of_natk by rewrite Ha , Hk ; apply point_site_exec ; exact Hb | lia
ge :
md :
f :
xs :
listword
fr :
m :
Memory.mem
fuel :
Z
s0 :
R.state
c :
s :
R.state
l :
i :
rest :
listinst
j :
why :
Hmd :
Hge :
ge_modulege = md
Hfree :
ge_freege = R.free
Hin :
InIFuncf md
Hcf :
call_framef xs = Somefr
H0 :
R.readys0 m
Hreach :
P.I.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s0 c, s
Hi :
raw_accessi ≠ None ∨ ∃r : call_result cl : value args : listarg, i = RawCallr cl args
b :
k :
nat
live :
listfact
fa :
q :
Hb :
find_blockl fn_blocksfr_fnc_framec = Someb
Hk :
i :: rest = skipnk b_instsb
Hl :
facts_holdge c_memc fr_envc_framec live
Hfa :
fact_ofq live = Somefa
Hr :
is_reachablefn_domsfr_fnc_framec l = true
Hsc :
scope_holdsge c_framec c_memc
Hready :
Hfit :
objects_fitm_regionsc_memfstc, s
Hlen :
Sk ≤ Datatypes.lengthb_instsb%nat
Hpt :
point_sitefr_fnc_framec fr_atc_framec = Somel, Z.of_natk
exact hull_access_not_uncheckedge md c_framec c_memc l Z.of_natk Hmd Hinf Hr scope_plain_of_ _ _ Hsc Hpt i q fa live why Hfit Hl HdomHr Hfa Hh
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ge md f xs fr m fuel s0 c s l i rest j why Hmd Hge Hfree Hin Hcf H0 Hreach Hd Ha Hi
destruct P.run_access_not_unchecked_ _ _ _ _ _ _ _ _ _ _ _ _ _ why Hmd Hge Hfree Hin Hcf H0 Hreach Hd Ha Hi as Hn | b & k & live & fa & q & Hb & Hk & Hl & Hdom & Hfa & Hh ; exact Hn |
pose proof S.run_sinv_ _ _ _ _ _ _ _ _ Hmd Hge Hfree Hin Hcf H0 mreachable_same_ _ _ Hreach as Hsh Hsc _
simpl in Hsh , Hsc
destruct Hsc as Hsc | Hsc ; congruence |
destruct Hsh as Hinf Hsh
rewrite Ha in Hsh
destruct Hsh as Hr _
pose proof P.I.RM.mreachable_ready_ _ _ Hfree Hreach H0 as Hready
pose proof R.address_space_ _ Hready as Hfit
destruct skipn_cons_ _ _ _ _ eq_symHk as _ & _ & Hlen
assert Hpt : point_sitefr_fnc_framec fr_atc_framec = Somel, Z.of_natk by rewrite Ha , Hk ; apply point_site_exec ; exact Hb | lia
exact hull_access_not_uncheckedge md c_framec c_memc l Z.of_natk Hmd Hinf Hr scope_plain_of_ _ _ Hsc Hpt i q fa live why Hfit Hl HdomHr Hfa Hh
The interpreter's runtime
run_access_checked for the interpreter's runtime: in every state of a run of a checked module's function that starts ready, a frame that is not doomed runs no raw access or raw call to unchecked. No hypothesis remains but the ready start.
∀ md globals f xs fr m fuel s0 c s l i rest j why
checked_modulemd → InIFuncf md → call_framef xs = Somefr → InterpRuntime.readys0 m → InterpHull.P.I.RM.mreachablege mkConfigfr [ ] m fuel, s0 c, s → fr_doomedc_framec = None → fr_atc_framec = Execl i :: rest j → raw_accessi ≠ None ∨ ∃r cl args, i = RawCallr cl args → inst_stepge c_framec c_memc i ≠ SomeIStopUncheckedwhy
Explore proof 2 tactics
Initial goal
⊢
∀ md : module globals : listname × ptr f : func xs : listword fr : frame m : Memory.mem fuel : Z s0 : InterpRuntime.state c : config s : InterpRuntime.state l : name i : inst rest : listinst j : jump why : reason ,
checked_modulemd → InIFuncf md → call_framef xs = Somefr → InterpRuntime.readys0 m → InterpHull.P.I.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s0 c, s → fr_doomedc_framec = None → fr_atc_framec = Execl i :: rest j → raw_accessi ≠ None ∨ ∃r : call_result cl : value args : listarg, i = RawCallr cl args → inst_stepge c_framec c_memc i ≠ SomeIStopUncheckedwhy
intros md globals f xs fr m fuel s0 c s l i rest j why ge Hmd Hin Hcf H0 Hreach Hd Ha Hi
md :
f :
xs :
listword
fr :
m :
Memory.mem
fuel :
Z
c :
l :
i :
rest :
listinst
j :
why :
ge :=
ge_module ≔ md; ge_globals ≔ globals; ge_free ≔ InterpRuntime.free : genv
Hmd :
Hin :
InIFuncf md
Hcf :
call_framef xs = Somefr
H0 :
Hreach :
InterpHull.P.I.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s0 c, s
Hi :
raw_accessi ≠ None ∨ ∃r : call_result cl : value args : listarg, i = RawCallr cl args
exact InterpHull.run_access_checkedge md f xs fr m fuel s0 c s l i rest j why Hmd eq_refl eq_refl Hin Hcf H0 Hreach Hd Ha Hi
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros md globals f xs fr m fuel s0 c s l i rest j why ge Hmd Hin Hcf H0 Hreach Hd Ha Hi
exact InterpHull.run_access_checkedge md f xs fr m fuel s0 c s l i rest j why Hmd eq_refl eq_refl Hin Hcf H0 Hreach Hd Ha Hi