Fil-C on Nix

Filnix wiki

the formal campaign

rocq/theories/CallbackLogic.v

Exact-state adequacy for retained void callbacks. The return postcondition observes the actual local teardown memory and CURRENT world, before ReturnCallback changes only the shutdown phase.

From iris.proofmode Require Import proofmode
From iris.base_logic.lib Require Import gen_heap
From iris.program_logic Require Import language weakestpre adequacy
From Stdlib Require Import ZArith List
From Nanofil Require Import Term Syntax Values Memory Runtime Semantics Machine ExternalCalls ExternalMachine Shutdown Linked Pieces Heap Panics Language Logic
Import ListNotations
Open Scope Z_scope

Callback proofs over any runtime, independently of libc's representation.

15Module CallbackLogicOn R : Runtime LG0 : LogicSigR
16Module LG ≔ LG0
17Module L ≔ LG.L
18Module LK ≔ Linked R
Import L LG L.RM

Short local spelling of Linked's unchanged callback world type.

22Notation cworld ≔ LK.callback_world

Linked and Language instantiate generative machine types separately; this changes only their constructor names, never their snapshots.

26Definition logic_stateworld : Type st : LK.M.stateworld : M.stateworld ≔
match st with
LK.M.Runningms w
⇒
M.Runningms w
LK.M.Stoppedwhy ms w
⇒
M.Stoppedwhy ms w

Local transport for promotion: the two runtime instances admit the same external effects, with the same intermediate memories.

34Lemma linked_effects
∀ sources roots releases requests s m born s′ m′ born′
LK.M.E.effectssources roots releases requests s m born s′ m′ born′
M.E.effectssources roots releases requests s m born s′ m′ born′
Explore proof 5 tactics

Initial goal

sources, roots :
listspan
releases :
listZ
requests :
Z → Z → Prop
s :
R.state
m :
mem
born :
listZ
s′ :
R.state
m′ :
mem
born′ :
listZ
⊢
LK.M.E.effectssources roots releases requests s m born s′ m′ born′ → M.E.effectssources roots releases requests s m born s′ m′ born′

intros H

sources, roots :
listspan
releases :
listZ
requests :
Z → Z → Prop
s :
R.state
m :
mem
born :
listZ
s′ :
R.state
m′ :
mem
born′ :
listZ
H :
LK.M.E.effectssources roots releases requests s m born s′ m′ born′
⊢
M.E.effectssources roots releases requests s m born s′ m′ born′

induction H

3 open

sources, roots :
listspan
releases :
listZ
requests :
Z → Z → Prop
s :
R.state
m :
mem
born :
listZ
⊢
M.E.effectssources roots releases requests s m born s m born
focused goal
sources, roots :
listspan
releases :
listZ
requests :
Z → Z → Prop
s :
R.state
m :
mem
born :
listZ
m1 :
mem
s′ :
R.state
m′ :
mem
born′ :
listZ
H :
local_effectsources roots releases born m m1
H0 :
LK.M.E.effectssources roots releases requests s m1 born s′ m′ born′
IHeffects :
M.E.effectssources roots releases requests s m1 born s′ m′ born′
⊢
M.E.effectssources roots releases requests s m born s′ m′ born′
focused goal
sources, roots :
listspan
releases :
listZ
requests :
Z → Z → Prop
s :
R.state
m :
mem
born :
listZ
align, size, base :
Z
s1, s′ :
R.state
m′ :
mem
born′ :
listZ
H :
requestsalign size
H0 :
0 ≤ size ≤ max_allocation_size
H1 :
R.allocs heap_reqalign size = Somebase, s1
H2 :
LK.M.E.effectssources roots releases requests s1 allocatedm heap_reqalign size base base :: born s′ m′ born′
IHeffects :
M.E.effectssources roots releases requests s1 allocatedm heap_reqalign size base base :: born s′ m′ born′
⊢
M.E.effectssources roots releases requests s m born s′ m′ born′

–constructor

2 open

deferred goal
sources, roots :
listspan
releases :
listZ
requests :
Z → Z → Prop
s :
R.state
m :
mem
born :
listZ
m1 :
mem
s′ :
R.state
m′ :
mem
born′ :
listZ
H :
local_effectsources roots releases born m m1
H0 :
LK.M.E.effectssources roots releases requests s m1 born s′ m′ born′
IHeffects :
M.E.effectssources roots releases requests s m1 born s′ m′ born′
⊢
M.E.effectssources roots releases requests s m born s′ m′ born′
deferred goal
sources, roots :
listspan
releases :
listZ
requests :
Z → Z → Prop
s :
R.state
m :
mem
born :
listZ
align, size, base :
Z
s1, s′ :
R.state
m′ :
mem
born′ :
listZ
H :
requestsalign size
H0 :
0 ≤ size ≤ max_allocation_size
H1 :
R.allocs heap_reqalign size = Somebase, s1
H2 :
LK.M.E.effectssources roots releases requests s1 allocatedm heap_reqalign size base base :: born s′ m′ born′
IHeffects :
M.E.effectssources roots releases requests s1 allocatedm heap_reqalign size base base :: born s′ m′ born′
⊢
M.E.effectssources roots releases requests s m born s′ m′ born′

–eapply M.E.effects_local ; eauto

deferred goal
sources, roots :
listspan
releases :
listZ
requests :
Z → Z → Prop
s :
R.state
m :
mem
born :
listZ
align, size, base :
Z
s1, s′ :
R.state
m′ :
mem
born′ :
listZ
H :
requestsalign size
H0 :
0 ≤ size ≤ max_allocation_size
H1 :
R.allocs heap_reqalign size = Somebase, s1
H2 :
LK.M.E.effectssources roots releases requests s1 allocatedm heap_reqalign size base base :: born s′ m′ born′
IHeffects :
M.E.effectssources roots releases requests s1 allocatedm heap_reqalign size base base :: born s′ m′ born′
⊢
M.E.effectssources roots releases requests s m born s′ m′ born′

–eapply M.E.effects_alloc ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros H
induction H
–constructor
–eapply M.E.effects_local ; eauto
–eapply M.E.effects_alloc ; eauto

Local transport for promotion: invocations keep their exact arguments, observations, runtime, memory and world across the module boundary.

46Lemma linked_invoke
∀ world : Type spec : contractworld r args xs s m w trace ending s′ m′ w′
LK.M.E.invokespec r args xs s m w trace ending s′ m′ w′
M.E.invokespec r args xs s m w trace ending s′ m′ w′
Explore proof 7 tactics

Initial goal

world :
Type
spec :
contractworld
r :
call_result
args :
listarg
xs :
listword
s :
R.state
m :
mem
w :
world
trace :
listevent
ending :
call_end
s′ :
R.state
m′ :
mem
w′ :
world
⊢
LK.M.E.invokespec r args xs s m w trace ending s′ m′ w′ → M.E.invokespec r args xs s m w trace ending s′ m′ w′

intros H

world :
Type
spec :
contractworld
r :
call_result
args :
listarg
xs :
listword
s :
R.state
m :
mem
w :
world
trace :
listevent
ending :
call_end
s′ :
R.state
m′ :
mem
w′ :
world
H :
LK.M.E.invokespec r args xs s m w trace ending s′ m′ w′
⊢
M.E.invokespec r args xs s m w trace ending s′ m′ w′

destruct H as trace ending s′ m′ w′ born Habi Hpre He Hp Hpost Hresource Hshape Hexit | why trace s′ m′ w′ born Habi Hpre He Hp Hfailure Hresource

2 open

world :
Type
spec :
contractworld
r :
call_result
args :
listarg
xs :
listword
s :
R.state
m :
mem
w :
world
trace :
listevent
ending :
call_end
s′ :
R.state
m′ :
mem
w′ :
world
born :
listZ
Habi :
contract_abispec r args
Hpre :
contract_prespec xs m w
He :
LK.M.E.effectscontract_sourcesspec xs m w contract_writesspec xs m w contract_releasesspec xs m w contract_requestsspec xs m w s m [ ] s′ m′ born
Hp :
contract_prefixspec xs m w born trace m′ w′
Hpost :
contract_postspec xs m w born trace ending m′ w′
Hresource :
∀why : reason, ending ≠ CallResourcewhy
Hshape :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec xs m w born m′ values
Hexit :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
M.E.invokespec r args xs s m w trace ending s′ m′ w′
focused goal
world :
Type
spec :
contractworld
r :
call_result
args :
listarg
xs :
listword
s :
R.state
m :
mem
w :
world
why :
reason
trace :
listevent
s′ :
R.state
m′ :
mem
w′ :
world
born :
listZ
Habi :
contract_abispec r args
Hpre :
contract_prespec xs m w
He :
LK.M.E.effectscontract_sourcesspec xs m w contract_writesspec xs m w contract_releasesspec xs m w contract_requestsspec xs m w s m [ ] s′ m′ born
Hp :
contract_prefixspec xs m w born trace m′ w′
Hfailure :
LK.M.E.resource_failurecontract_requestsspec xs m w s′ why
Hresource :
contract_resourcespec why
⊢
M.E.invokespec r args xs s m w trace CallResourcewhy s′ m′ w′

–eapply M.E.invoke_normal ; eauto

2 open

world :
Type
spec :
contractworld
r :
call_result
args :
listarg
xs :
listword
s :
R.state
m :
mem
w :
world
trace :
listevent
ending :
call_end
s′ :
R.state
m′ :
mem
w′ :
world
born :
listZ
Habi :
contract_abispec r args
Hpre :
contract_prespec xs m w
He :
LK.M.E.effectscontract_sourcesspec xs m w contract_writesspec xs m w contract_releasesspec xs m w contract_requestsspec xs m w s m [ ] s′ m′ born
Hp :
contract_prefixspec xs m w born trace m′ w′
Hpost :
contract_postspec xs m w born trace ending m′ w′
Hresource :
∀why : reason, ending ≠ CallResourcewhy
Hshape :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec xs m w born m′ values
Hexit :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
M.E.prefixspec xs s m w born trace s′ m′ w′
deferred goal
world :
Type
spec :
contractworld
r :
call_result
args :
listarg
xs :
listword
s :
R.state
m :
mem
w :
world
why :
reason
trace :
listevent
s′ :
R.state
m′ :
mem
w′ :
world
born :
listZ
Habi :
contract_abispec r args
Hpre :
contract_prespec xs m w
He :
LK.M.E.effectscontract_sourcesspec xs m w contract_writesspec xs m w contract_releasesspec xs m w contract_requestsspec xs m w s m [ ] s′ m′ born
Hp :
contract_prefixspec xs m w born trace m′ w′
Hfailure :
LK.M.E.resource_failurecontract_requestsspec xs m w s′ why
Hresource :
contract_resourcespec why
⊢
M.E.invokespec r args xs s m w trace CallResourcewhy s′ m′ w′

split ; eapply linked_effects ; exact He | exact Hp

deferred goal
world :
Type
spec :
contractworld
r :
call_result
args :
listarg
xs :
listword
s :
R.state
m :
mem
w :
world
why :
reason
trace :
listevent
s′ :
R.state
m′ :
mem
w′ :
world
born :
listZ
Habi :
contract_abispec r args
Hpre :
contract_prespec xs m w
He :
LK.M.E.effectscontract_sourcesspec xs m w contract_writesspec xs m w contract_releasesspec xs m w contract_requestsspec xs m w s m [ ] s′ m′ born
Hp :
contract_prefixspec xs m w born trace m′ w′
Hfailure :
LK.M.E.resource_failurecontract_requestsspec xs m w s′ why
Hresource :
contract_resourcespec why
⊢
M.E.invokespec r args xs s m w trace CallResourcewhy s′ m′ w′

–eapply M.E.invoke_resource ; eauto

3 open

world :
Type
spec :
contractworld
r :
call_result
args :
listarg
xs :
listword
s :
R.state
m :
mem
w :
world
why :
reason
trace :
listevent
s′ :
R.state
m′ :
mem
w′ :
world
born :
listZ
Habi :
contract_abispec r args
Hpre :
contract_prespec xs m w
He :
LK.M.E.effectscontract_sourcesspec xs m w contract_writesspec xs m w contract_releasesspec xs m w contract_requestsspec xs m w s m [ ] s′ m′ born
Hp :
contract_prefixspec xs m w born trace m′ w′
Hfailure :
LK.M.E.resource_failurecontract_requestsspec xs m w s′ why
Hresource :
contract_resourcespec why
⊢
M.E.prefixspec xs s m w ?born trace s′ m′ w′
focused goal
world :
Type
spec :
contractworld
r :
call_result
args :
listarg
xs :
listword
s :
R.state
m :
mem
w :
world
why :
reason
trace :
listevent
s′ :
R.state
m′ :
mem
w′ :
world
born :
listZ
Habi :
contract_abispec r args
Hpre :
contract_prespec xs m w
He :
LK.M.E.effectscontract_sourcesspec xs m w contract_writesspec xs m w contract_releasesspec xs m w contract_requestsspec xs m w s m [ ] s′ m′ born
Hp :
contract_prefixspec xs m w born trace m′ w′
Hfailure :
LK.M.E.resource_failurecontract_requestsspec xs m w s′ why
Hresource :
contract_resourcespec why
⊢
M.E.resource_failurecontract_requestsspec xs m w s′ why
shelved goal
world :
Type
spec :
contractworld
r :
call_result
args :
listarg
xs :
listword
s :
R.state
m :
mem
w :
world
why :
reason
trace :
listevent
s′ :
R.state
m′ :
mem
w′ :
world
born :
listZ
Habi :
contract_abispec r args
Hpre :
contract_prespec xs m w
He :
LK.M.E.effectscontract_sourcesspec xs m w contract_writesspec xs m w contract_releasesspec xs m w contract_requestsspec xs m w s m [ ] s′ m′ born
Hp :
contract_prefixspec xs m w born trace m′ w′
Hfailure :
LK.M.E.resource_failurecontract_requestsspec xs m w s′ why
Hresource :
contract_resourcespec why
⊢
listZ

+split ; eapply linked_effects ; exact He | exact Hp

deferred goal
world :
Type
spec :
contractworld
r :
call_result
args :
listarg
xs :
listword
s :
R.state
m :
mem
w :
world
why :
reason
trace :
listevent
s′ :
R.state
m′ :
mem
w′ :
world
born :
listZ
Habi :
contract_abispec r args
Hpre :
contract_prespec xs m w
He :
LK.M.E.effectscontract_sourcesspec xs m w contract_writesspec xs m w contract_releasesspec xs m w contract_requestsspec xs m w s m [ ] s′ m′ born
Hp :
contract_prefixspec xs m w born trace m′ w′
Hfailure :
LK.M.E.resource_failurecontract_requestsspec xs m w s′ why
Hresource :
contract_resourcespec why
⊢
M.E.resource_failurecontract_requestsspec xs m w s′ why

+destruct Hfailure ; eapply M.E.failure_oom | eapply M.E.failure_big ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros H
destruct H as trace ending s′ m′ w′ born Habi Hpre He Hp Hpost Hresource Hshape Hexit | why trace s′ m′ w′ born Habi Hpre He Hp Hfailure Hresource
–eapply M.E.invoke_normal ; eauto
split ; eapply linked_effects ; exact He | exact Hp
–eapply M.E.invoke_resource ; eauto
+split ; eapply linked_effects ; exact He | exact Hp
+destruct Hfailure ; eapply M.E.failure_oom | eapply M.E.failure_big ; eauto

Local transport for promotion: a labelled step is unchanged except for the generative state constructors.

62Lemma linked_step
∀ world : Type registry ge st : LK.M.stateworld trace st′
LK.M.stepregistry ge st trace st′
M.stepregistry ge logic_statest trace logic_statest′
Explore proof 13 tactics

Initial goal

world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
LK.M.stateworld
trace :
listevent
st′ :
LK.M.stateworld
⊢
LK.M.stepregistry ge st trace st′ → M.stepregistry ge logic_statest trace logic_statest′

intros H

world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
LK.M.stateworld
trace :
listevent
st′ :
LK.M.stateworld
H :
LK.M.stepregistry ge st trace st′
⊢
M.stepregistry ge logic_statest trace logic_statest′

destruct H ; cbn [ logic_state ]

9 open

world :
Type
registry :
name → optioncontractworld
ge :
genv
ms, ms′ :
LK.M.P.I.RM.mstate
w :
world
H :
LK.M.P.I.RM.mstepge ms ms′
⊢
M.stepregistry ge M.Runningms w [ ] M.Runningms′ w
focused goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
o :
outcome
H :
∀site : call_site, ¬external_sitege c site
H0 :
stepge c = Doneo
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedCoreEndo c, s w
focused goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
why :
string
H :
∀site : call_site, ¬external_sitege c site
H0 :
stepge c = Stuckwhy
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedCoreStuckwhy c, s w
focused goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
q :
alloc_req
k :
Z → config
H :
∀site : call_site, ¬external_sitege c site
H0 :
stepge c = Freshq k
H1 :
0 ≤ req_extentq
H2 :
R.allocs q = None
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedCoreEndTrapOutOfMemory c, s w
focused goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
e :
env
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = Somee
⊢
M.stepregistry ge M.Runningc, s w trace M.Runningresume_externalc site e m′, s′ w′
focused goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
status :
Z
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedExternalExitstatus LK.M.P.I.RM.with_memc m′, s′ w′
focused goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
why :
reason
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedCoreEndTrapwhy LK.M.P.I.RM.with_memc m′, s′ w′
focused goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
why :
violation
H :
external_sitege c site
H0 :
LK.M.rejectedworld registry ge c w site why
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedContractViolationsite_namesite why c, s w
focused goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedContractViolationsite_namesite BadReturn LK.M.P.I.RM.with_memc m′, s′ w′

–apply M.step_core

9 open

world :
Type
registry :
name → optioncontractworld
ge :
genv
ms, ms′ :
LK.M.P.I.RM.mstate
w :
world
H :
LK.M.P.I.RM.mstepge ms ms′
⊢
M.P.I.RM.mstepge ms ms′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
o :
outcome
H :
∀site : call_site, ¬external_sitege c site
H0 :
stepge c = Doneo
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedCoreEndo c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
why :
string
H :
∀site : call_site, ¬external_sitege c site
H0 :
stepge c = Stuckwhy
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedCoreStuckwhy c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
q :
alloc_req
k :
Z → config
H :
∀site : call_site, ¬external_sitege c site
H0 :
stepge c = Freshq k
H1 :
0 ≤ req_extentq
H2 :
R.allocs q = None
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedCoreEndTrapOutOfMemory c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
e :
env
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = Somee
⊢
M.stepregistry ge M.Runningc, s w trace M.Runningresume_externalc site e m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
status :
Z
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedExternalExitstatus LK.M.P.I.RM.with_memc m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
why :
reason
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedCoreEndTrapwhy LK.M.P.I.RM.with_memc m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
why :
violation
H :
external_sitege c site
H0 :
LK.M.rejectedworld registry ge c w site why
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedContractViolationsite_namesite why c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedContractViolationsite_namesite BadReturn LK.M.P.I.RM.with_memc m′, s′ w′

destruct H ; eapply M.P.I.RM.mstep_next | eapply M.P.I.RM.mstep_alloc | eapply M.P.I.RM.mstep_safepoint ; eauto

8 open

deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
o :
outcome
H :
∀site : call_site, ¬external_sitege c site
H0 :
stepge c = Doneo
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedCoreEndo c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
why :
string
H :
∀site : call_site, ¬external_sitege c site
H0 :
stepge c = Stuckwhy
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedCoreStuckwhy c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
q :
alloc_req
k :
Z → config
H :
∀site : call_site, ¬external_sitege c site
H0 :
stepge c = Freshq k
H1 :
0 ≤ req_extentq
H2 :
R.allocs q = None
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedCoreEndTrapOutOfMemory c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
e :
env
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = Somee
⊢
M.stepregistry ge M.Runningc, s w trace M.Runningresume_externalc site e m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
status :
Z
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedExternalExitstatus LK.M.P.I.RM.with_memc m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
why :
reason
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedCoreEndTrapwhy LK.M.P.I.RM.with_memc m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
why :
violation
H :
external_sitege c site
H0 :
LK.M.rejectedworld registry ge c w site why
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedContractViolationsite_namesite why c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedContractViolationsite_namesite BadReturn LK.M.P.I.RM.with_memc m′, s′ w′

–eapply M.step_core_end ; eauto

7 open

deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
why :
string
H :
∀site : call_site, ¬external_sitege c site
H0 :
stepge c = Stuckwhy
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedCoreStuckwhy c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
q :
alloc_req
k :
Z → config
H :
∀site : call_site, ¬external_sitege c site
H0 :
stepge c = Freshq k
H1 :
0 ≤ req_extentq
H2 :
R.allocs q = None
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedCoreEndTrapOutOfMemory c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
e :
env
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = Somee
⊢
M.stepregistry ge M.Runningc, s w trace M.Runningresume_externalc site e m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
status :
Z
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedExternalExitstatus LK.M.P.I.RM.with_memc m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
why :
reason
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedCoreEndTrapwhy LK.M.P.I.RM.with_memc m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
why :
violation
H :
external_sitege c site
H0 :
LK.M.rejectedworld registry ge c w site why
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedContractViolationsite_namesite why c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedContractViolationsite_namesite BadReturn LK.M.P.I.RM.with_memc m′, s′ w′

–eapply M.step_core_stuck ; eauto

6 open

deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
q :
alloc_req
k :
Z → config
H :
∀site : call_site, ¬external_sitege c site
H0 :
stepge c = Freshq k
H1 :
0 ≤ req_extentq
H2 :
R.allocs q = None
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedCoreEndTrapOutOfMemory c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
e :
env
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = Somee
⊢
M.stepregistry ge M.Runningc, s w trace M.Runningresume_externalc site e m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
status :
Z
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedExternalExitstatus LK.M.P.I.RM.with_memc m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
why :
reason
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedCoreEndTrapwhy LK.M.P.I.RM.with_memc m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
why :
violation
H :
external_sitege c site
H0 :
LK.M.rejectedworld registry ge c w site why
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedContractViolationsite_namesite why c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedContractViolationsite_namesite BadReturn LK.M.P.I.RM.with_memc m′, s′ w′

–eapply M.step_core_refusal ; eauto

5 open

deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
e :
env
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = Somee
⊢
M.stepregistry ge M.Runningc, s w trace M.Runningresume_externalc site e m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
status :
Z
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedExternalExitstatus LK.M.P.I.RM.with_memc m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
why :
reason
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedCoreEndTrapwhy LK.M.P.I.RM.with_memc m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
why :
violation
H :
external_sitege c site
H0 :
LK.M.rejectedworld registry ge c w site why
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedContractViolationsite_namesite why c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedContractViolationsite_namesite BadReturn LK.M.P.I.RM.with_memc m′, s′ w′

–eapply M.step_return ; eauto using linked_invoke

4 open

deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
status :
Z
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedExternalExitstatus LK.M.P.I.RM.with_memc m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
why :
reason
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedCoreEndTrapwhy LK.M.P.I.RM.with_memc m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
why :
violation
H :
external_sitege c site
H0 :
LK.M.rejectedworld registry ge c w site why
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedContractViolationsite_namesite why c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedContractViolationsite_namesite BadReturn LK.M.P.I.RM.with_memc m′, s′ w′

–eapply M.step_exit ; eauto using linked_invoke

3 open

deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
why :
reason
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedCoreEndTrapwhy LK.M.P.I.RM.with_memc m′, s′ w′
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
why :
violation
H :
external_sitege c site
H0 :
LK.M.rejectedworld registry ge c w site why
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedContractViolationsite_namesite why c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedContractViolationsite_namesite BadReturn LK.M.P.I.RM.with_memc m′, s′ w′

–eapply M.step_resource ; eauto using linked_invoke

2 open

deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
why :
violation
H :
external_sitege c site
H0 :
LK.M.rejectedworld registry ge c w site why
⊢
M.stepregistry ge M.Runningc, s w [ ] M.StoppedContractViolationsite_namesite why c, s w
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedContractViolationsite_namesite BadReturn LK.M.P.I.RM.with_memc m′, s′ w′

–eapply M.step_rejected ; eauto

2 open

world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
why :
violation
H :
external_sitege c site
H0 :
LK.M.rejectedworld registry ge c w site why
⊢
M.rejectedworld registry ge c w site why
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedContractViolationsite_namesite BadReturn LK.M.P.I.RM.with_memc m′, s′ w′

destruct H0 ; eapply M.reject_missing | eapply M.reject_arguments | eapply M.reject_abi | eapply M.reject_pre ; eauto

deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
c :
config
s :
R.state
w :
world
site :
call_site
spec :
contractworld
xs :
listword
trace :
listevent
values :
listword
s′ :
R.state
m′ :
mem
w′ :
world
H :
external_sitege c site
H0 :
registrysite_namesite = Somespec
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
LK.M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedContractViolationsite_namesite BadReturn LK.M.P.I.RM.with_memc m′, s′ w′

–eapply M.step_bad_return ; eauto using linked_invoke

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros H
destruct H ; cbn [ logic_state ]
–apply M.step_core
destruct H ; eapply M.P.I.RM.mstep_next | eapply M.P.I.RM.mstep_alloc | eapply M.P.I.RM.mstep_safepoint ; eauto
–eapply M.step_core_end ; eauto
–eapply M.step_core_stuck ; eauto
–eapply M.step_core_refusal ; eauto
–eapply M.step_return ; eauto using linked_invoke
–eapply M.step_exit ; eauto using linked_invoke
–eapply M.step_resource ; eauto using linked_invoke
–eapply M.step_rejected ; eauto
destruct H0 ; eapply M.reject_missing | eapply M.reject_arguments | eapply M.reject_abi | eapply M.reject_pre ; eauto
–eapply M.step_bad_return ; eauto using linked_invoke

Local transport for promotion: every Linked run has the identical Language run, including its full trace and endpoint snapshots.

86Lemma linked_run
∀ world : Type registry ge st : LK.M.stateworld trace st′
LK.M.runregistry ge st trace st′
M.runregistry ge logic_statest trace logic_statest′
Explore proof 3 tactics

Initial goal

world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
LK.M.stateworld
trace :
listevent
st′ :
LK.M.stateworld
⊢
LK.M.runregistry ge st trace st′ → M.runregistry ge logic_statest trace logic_statest′

intros H

world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
LK.M.stateworld
trace :
listevent
st′ :
LK.M.stateworld
H :
LK.M.runregistry ge st trace st′
⊢
M.runregistry ge logic_statest trace logic_statest′

induction H ; constructor |

world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
LK.M.stateworld
trace :
listevent
mid :
LK.M.stateworld
tail :
listevent
last :
LK.M.stateworld
H :
LK.M.stepregistry ge st trace mid
H0 :
LK.M.runregistry ge mid tail last
IHrun :
M.runregistry ge logic_statemid tail logic_statelast
⊢
M.runregistry ge logic_statest trace ++ tail logic_statelast

econstructor ; eapply linked_step ; eauto | exact IHrun

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros H
induction H ; constructor |
econstructor ; eapply linked_step ; eauto | exact IHrun

Local rule for promotion: unlike outcome-only heap_labelled_safe, this keeps the final state interpretation together with the WP post. The existential heap in heap_interp is the one surviving execution.

97Lemma heap_exact_adequacy
∀ Σ HinvP : invGpreSΣ HheapP : gen_heapGpreSpiece pval Σ world : Type registry : name → optioncontractworld wi : mem → world → gmappiece pval → Prop ge fr m s w : world h0 fuel Q : outcome → lstateworld → Prop
R.readys m
live_disjointm
agreesm h0
wim w h0
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let _ : irisGS_genHasNoLc nanofil_langregistry ge Σ ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {Ψ}
∧
∀o σ, heap_interpwi σ ∗ Ψo ⊢ ⌜Qo σ⌝
@adequatenanofil_langregistry ge NotStuck ERunfr mkLstatem s fuel w Q
Proof 32 steps Qed
intros Hr Hd Ha Hw Hwp
apply adequate_alt
intros t2 σ2 Hsteps
apply erased_steps_nsteps in Hsteps
destruct Hsteps as n κs Hn
eapply wp_strong_adequacy_genHasNoLc Σ _ NotStuck with num_laters_per_step := λ_ ⇒ 0%nat ; | exact Hn
intros HinvG
iMod gen_heap_inith0 as HheapG (Hh & Hpts & _)
destruct HwpHinvG HheapG as Ψ & Hbody & Hpost
iExists λσ _ _ _ ⇒ heap_interpwi σ, Ψ, λ_ ⇒ True%I, _
iSplitL Hh
–iExists h0
iFrame Hh
iPureIntro
exact conjHa conjHd conjHr Hw
–iSplitL Hpts
+cbn
iSplitL ; iApply Hbody ; iExact Hpts | done
+iModIntro
iIntros es′ t2′ → Hlen Hsafe Hσ Hvals _
destruct es' as | e es′ ; discriminate Hlen |
destruct es' ; | discriminate Hlen
iApply fupd_mask_intro_discard ; set_solver |
iSplit
∗iIntros v t He
injection He as He Ht
subst e
iEval rewritebig_sepL2_cons to_of_val in Hvals
iDestruct Hvals as [Hv _]
iApply Hpost with [$Hσ $Hv]
∗iPureIntro
exact Hsafe

Local rule for promotion: any nonempty run has a final step and its actual prefix; this introduces no execution or termination premise.

139Lemma run_last
∀ world : Type registry ge start : M.stateworld trace last
M.runregistry ge start trace last
start = last ∨ ∃prefix mid tail, M.runregistry ge start prefix mid ∧ M.stepregistry ge mid tail last
Explore proof 10 tactics

Initial goal

world :
Type
registry :
name → optioncontractworld
ge :
genv
start :
M.stateworld
trace :
listevent
last :
M.stateworld
⊢
M.runregistry ge start trace last → start = last ∨ ∃prefix0 : listevent mid : M.stateworld tail : listevent, M.runregistry ge start prefix0 mid ∧ M.stepregistry ge mid tail last

intros Hrun

world :
Type
registry :
name → optioncontractworld
ge :
genv
start :
M.stateworld
trace :
listevent
last :
M.stateworld
Hrun :
M.runregistry ge start trace last
⊢
start = last ∨ ∃prefix0 : listevent mid : M.stateworld tail : listevent, M.runregistry ge start prefix0 mid ∧ M.stepregistry ge mid tail last

induction Hrun as st | st tr mid tail last Hstep Hrun IH

2 open

world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
M.stateworld
⊢
st = st ∨ ∃prefix0 : listevent mid : M.stateworld tail : listevent, M.runregistry ge st prefix0 mid ∧ M.stepregistry ge mid tail st
focused goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
M.stateworld
tr :
listevent
mid :
M.stateworld
tail :
listevent
last :
M.stateworld
Hstep :
M.stepregistry ge st tr mid
Hrun :
M.runregistry ge mid tail last
IH :
mid = last ∨ ∃prefix : listevent mid0 : M.stateworld tail : listevent, M.runregistry ge mid prefix mid0 ∧ M.stepregistry ge mid0 tail last
⊢
st = last ∨ ∃prefix0 : listevent mid0 : M.stateworld tail0 : listevent, M.runregistry ge st prefix0 mid0 ∧ M.stepregistry ge mid0 tail0 last

–left

2 open

world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
M.stateworld
⊢
st = st
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
M.stateworld
tr :
listevent
mid :
M.stateworld
tail :
listevent
last :
M.stateworld
Hstep :
M.stepregistry ge st tr mid
Hrun :
M.runregistry ge mid tail last
IH :
mid = last ∨ ∃prefix : listevent mid0 : M.stateworld tail : listevent, M.runregistry ge mid prefix mid0 ∧ M.stepregistry ge mid0 tail last
⊢
st = last ∨ ∃prefix0 : listevent mid0 : M.stateworld tail0 : listevent, M.runregistry ge st prefix0 mid0 ∧ M.stepregistry ge mid0 tail0 last

reflexivity

deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
M.stateworld
tr :
listevent
mid :
M.stateworld
tail :
listevent
last :
M.stateworld
Hstep :
M.stepregistry ge st tr mid
Hrun :
M.runregistry ge mid tail last
IH :
mid = last ∨ ∃prefix : listevent mid0 : M.stateworld tail : listevent, M.runregistry ge mid prefix mid0 ∧ M.stepregistry ge mid0 tail last
⊢
st = last ∨ ∃prefix0 : listevent mid0 : M.stateworld tail0 : listevent, M.runregistry ge st prefix0 mid0 ∧ M.stepregistry ge mid0 tail0 last

–right

world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
M.stateworld
tr :
listevent
mid :
M.stateworld
tail :
listevent
last :
M.stateworld
Hstep :
M.stepregistry ge st tr mid
Hrun :
M.runregistry ge mid tail last
IH :
mid = last ∨ ∃prefix : listevent mid0 : M.stateworld tail : listevent, M.runregistry ge mid prefix mid0 ∧ M.stepregistry ge mid0 tail last
⊢
∃prefix0 : listevent mid0 : M.stateworld tail0 : listevent, M.runregistry ge st prefix0 mid0 ∧ M.stepregistry ge mid0 tail0 last

destruct IH as [ ->| ( prefix & before & ending & Hp & Hs ) ]

2 open

world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
M.stateworld
tr, tail :
listevent
last :
M.stateworld
Hrun :
M.runregistry ge last tail last
Hstep :
M.stepregistry ge st tr last
⊢
∃prefix0 : listevent mid : M.stateworld tail0 : listevent, M.runregistry ge st prefix0 mid ∧ M.stepregistry ge mid tail0 last
focused goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
M.stateworld
tr :
listevent
mid :
M.stateworld
tail :
listevent
last :
M.stateworld
Hstep :
M.stepregistry ge st tr mid
Hrun :
M.runregistry ge mid tail last
prefix :
listevent
before :
M.stateworld
ending :
listevent
Hp :
M.runregistry ge mid prefix before
Hs :
M.stepregistry ge before ending last
⊢
∃prefix0 : listevent mid0 : M.stateworld tail0 : listevent, M.runregistry ge st prefix0 mid0 ∧ M.stepregistry ge mid0 tail0 last

+exists [ ], st, tr

2 open

world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
M.stateworld
tr, tail :
listevent
last :
M.stateworld
Hrun :
M.runregistry ge last tail last
Hstep :
M.stepregistry ge st tr last
⊢
M.runregistry ge st [ ] st ∧ M.stepregistry ge st tr last
deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
M.stateworld
tr :
listevent
mid :
M.stateworld
tail :
listevent
last :
M.stateworld
Hstep :
M.stepregistry ge st tr mid
Hrun :
M.runregistry ge mid tail last
prefix :
listevent
before :
M.stateworld
ending :
listevent
Hp :
M.runregistry ge mid prefix before
Hs :
M.stepregistry ge before ending last
⊢
∃prefix0 : listevent mid0 : M.stateworld tail0 : listevent, M.runregistry ge st prefix0 mid0 ∧ M.stepregistry ge mid0 tail0 last

split ; constructor | exact Hstep

deferred goal
world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
M.stateworld
tr :
listevent
mid :
M.stateworld
tail :
listevent
last :
M.stateworld
Hstep :
M.stepregistry ge st tr mid
Hrun :
M.runregistry ge mid tail last
prefix :
listevent
before :
M.stateworld
ending :
listevent
Hp :
M.runregistry ge mid prefix before
Hs :
M.stepregistry ge before ending last
⊢
∃prefix0 : listevent mid0 : M.stateworld tail0 : listevent, M.runregistry ge st prefix0 mid0 ∧ M.stepregistry ge mid0 tail0 last

+exists tr ++ prefix, before, ending

world :
Type
registry :
name → optioncontractworld
ge :
genv
st :
M.stateworld
tr :
listevent
mid :
M.stateworld
tail :
listevent
last :
M.stateworld
Hstep :
M.stepregistry ge st tr mid
Hrun :
M.runregistry ge mid tail last
prefix :
listevent
before :
M.stateworld
ending :
listevent
Hp :
M.runregistry ge mid prefix before
Hs :
M.stepregistry ge before ending last
⊢
M.runregistry ge st tr ++ prefix before ∧ M.stepregistry ge before ending last

split ; econstructor ; eauto | exact Hs

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros Hrun
induction Hrun as st | st tr mid tail last Hstep Hrun IH
–left
reflexivity
–right
destruct IH as [ ->| ( prefix & before & ending & Hp & Hs ) ]
+exists [ ], st, tr
split ; constructor | exact Hstep
+exists tr ++ prefix, before, ending
split ; econstructor ; eauto | exact Hs

Local rule for promotion: a stopped top-level void return reaches exactly the Iris state whose memory invalidate_locals produced.

153Lemma callback_return_reachable
∀ payload : Type registry ge fr m s w : cworldpayload fuel Q trace stopped entry ms′ w′
@adequatenanofil_langregistry ge NotStuck ERunfr mkLstatem s fuel w Q
LK.M.runregistry ge LK.M.RunningmkConfigfr [ ] m fuel, s w trace stopped
LK.callback_returnpayload entry stopped ms′ w′
∃c sr wr m_return, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ c_callersc = [ ] ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ fstw′ = fstwr ∧ shutdown_stepsndwr ReturnCallback sndw′ ∧ rtc@erased_stepnanofil_langregistry ge ERunfr, mkLstatem s fuel w EEndRetVoid, mkLstatem_return sr c_fuelc wr
Explore proof 16 tactics

Initial goal

payload :
Type
registry :
name → optioncontractcworldpayload
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
fuel :
Z
Q :
valnanofil_langregistry ge → statenanofil_langregistry ge → Prop
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
⊢
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w Q → LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped → LK.callback_returnpayload entry stopped ms′ w′ → ∃c : config sr : R.state wr : cworldpayload m_return : mem, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ c_callersc = [ ] ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ m_return; ls_rt ≔ sr; ls_fuel ≔ c_fuelc; ls_world ≔ wr

intros Had Hrun Hreturn

payload :
Type
registry :
name → optioncontractcworldpayload
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
fuel :
Z
Q :
valnanofil_langregistry ge → statenanofil_langregistry ge → Prop
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w Q
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
⊢
∃c : config sr : R.state wr : cworldpayload m_return : mem, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ c_callersc = [ ] ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ m_return; ls_rt ≔ sr; ls_fuel ≔ c_fuelc; ls_world ≔ wr

destruct LK.callback_return_endpointpayload _ _ _ _ Hreturn as c & sr & wr & mr & → & Hcs & Hi & Hms & Hw & Hshutdown

payload :
Type
registry :
name → optioncontractcworldpayload
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
fuel :
Z
Q :
valnanofil_langregistry ge → statenanofil_langregistry ge → Prop
trace :
listevent
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w Q
c :
config
sr :
R.state
wr :
cworldpayload
Hreturn :
LK.callback_returnpayload entry LK.M.StoppedCoreEndRetVoid c, sr wr ms′ w′
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace LK.M.StoppedCoreEndRetVoid c, sr wr
mr :
mem
Hcs :
c_callersc = [ ]
Hi :
invalidate_localsfr_localsc_framec c_memc = Somemr
Hms :
ms′ = LK.RM.with_memc mr, sr
Hw :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
⊢
∃c0 : config sr0 : R.state wr0 : cworldpayload m_return : mem, LK.M.StoppedCoreEndRetVoid c, sr wr = LK.M.StoppedCoreEndRetVoid c0, sr0 wr0 ∧ c_callersc0 = [ ] ∧ invalidate_localsfr_localsc_framec0 c_memc0 = Somem_return ∧ ms′ = with_memc0 m_return, sr0 ∧ w′.1 = wr0.1 ∧ shutdown_stepwr0.2 ReturnCallback w′.2 ∧ rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ m_return; ls_rt ≔ sr0; ls_fuel ≔ c_fuelc0; ls_world ≔ wr0

exists c, sr, wr, mr

payload :
Type
registry :
name → optioncontractcworldpayload
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
fuel :
Z
Q :
valnanofil_langregistry ge → statenanofil_langregistry ge → Prop
trace :
listevent
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w Q
c :
config
sr :
R.state
wr :
cworldpayload
Hreturn :
LK.callback_returnpayload entry LK.M.StoppedCoreEndRetVoid c, sr wr ms′ w′
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace LK.M.StoppedCoreEndRetVoid c, sr wr
mr :
mem
Hcs :
c_callersc = [ ]
Hi :
invalidate_localsfr_localsc_framec c_memc = Somemr
Hms :
ms′ = LK.RM.with_memc mr, sr
Hw :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
⊢
LK.M.StoppedCoreEndRetVoid c, sr wr = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ c_callersc = [ ] ∧ invalidate_localsfr_localsc_framec c_memc = Somemr ∧ ms′ = with_memc mr, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ mr; ls_rt ≔ sr; ls_fuel ≔ c_fuelc; ls_world ≔ wr

repeat split ; try assumption ; try reflexivity

payload :
Type
registry :
name → optioncontractcworldpayload
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
fuel :
Z
Q :
valnanofil_langregistry ge → statenanofil_langregistry ge → Prop
trace :
listevent
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w Q
c :
config
sr :
R.state
wr :
cworldpayload
Hreturn :
LK.callback_returnpayload entry LK.M.StoppedCoreEndRetVoid c, sr wr ms′ w′
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace LK.M.StoppedCoreEndRetVoid c, sr wr
mr :
mem
Hcs :
c_callersc = [ ]
Hi :
invalidate_localsfr_localsc_framec c_memc = Somemr
Hms :
ms′ = LK.RM.with_memc mr, sr
Hw :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
⊢
rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ mr; ls_rt ≔ sr; ls_fuel ≔ c_fuelc; ls_world ≔ wr

apply linked_run in Hrun

payload :
Type
registry :
name → optioncontractcworldpayload
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
fuel :
Z
Q :
valnanofil_langregistry ge → statenanofil_langregistry ge → Prop
trace :
listevent
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w Q
c :
config
sr :
R.state
wr :
cworldpayload
Hreturn :
LK.callback_returnpayload entry LK.M.StoppedCoreEndRetVoid c, sr wr ms′ w′
Hrun :
M.runregistry ge logic_stateLK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace logic_stateLK.M.StoppedCoreEndRetVoid c, sr wr
mr :
mem
Hcs :
c_callersc = [ ]
Hi :
invalidate_localsfr_localsc_framec c_memc = Somemr
Hms :
ms′ = LK.RM.with_memc mr, sr
Hw :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
⊢
rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ mr; ls_rt ≔ sr; ls_fuel ≔ c_fuelc; ls_world ≔ wr

cbn [ logic_state ] in Hrun

payload :
Type
registry :
name → optioncontractcworldpayload
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
fuel :
Z
Q :
valnanofil_langregistry ge → statenanofil_langregistry ge → Prop
trace :
listevent
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w Q
c :
config
sr :
R.state
wr :
cworldpayload
Hreturn :
LK.callback_returnpayload entry LK.M.StoppedCoreEndRetVoid c, sr wr ms′ w′
Hrun :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace M.StoppedCoreEndRetVoid c, sr wr
mr :
mem
Hcs :
c_callersc = [ ]
Hi :
invalidate_localsfr_localsc_framec c_memc = Somemr
Hms :
ms′ = LK.RM.with_memc mr, sr
Hw :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
⊢
rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ mr; ls_rt ≔ sr; ls_fuel ≔ c_fuelc; ls_world ≔ wr

destruct run_last_ _ _ _ _ Hrun as Heq | prefix & mid & tail & Hp & Hs ; discriminate Heq |

payload :
Type
registry :
name → optioncontractcworldpayload
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
fuel :
Z
Q :
valnanofil_langregistry ge → statenanofil_langregistry ge → Prop
trace :
listevent
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w Q
c :
config
sr :
R.state
wr :
cworldpayload
Hreturn :
LK.callback_returnpayload entry LK.M.StoppedCoreEndRetVoid c, sr wr ms′ w′
Hrun :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace M.StoppedCoreEndRetVoid c, sr wr
mr :
mem
Hcs :
c_callersc = [ ]
Hi :
invalidate_localsfr_localsc_framec c_memc = Somemr
Hms :
ms′ = LK.RM.with_memc mr, sr
Hw :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
prefix :
listevent
mid :
M.statecworldpayload
tail :
listevent
Hp :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w prefix mid
Hs :
M.stepregistry ge mid tail M.StoppedCoreEndRetVoid c, sr wr
⊢
rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ mr; ls_rt ≔ sr; ls_fuel ≔ c_fuelc; ls_world ≔ wr

inversion Hs ; subst

payload :
Type
registry :
name → optioncontractcworldpayload
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
fuel :
Z
Q :
valnanofil_langregistry ge → statenanofil_langregistry ge → Prop
trace :
listevent
entry :
registration
w′ :
cworldpayload
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w Q
c :
config
sr :
R.state
wr :
cworldpayload
mr :
mem
Hreturn :
LK.callback_returnpayload entry LK.M.StoppedCoreEndRetVoid c, sr wr LK.RM.with_memc mr, sr w′
Hrun :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace M.StoppedCoreEndRetVoid c, sr wr
Hcs :
c_callersc = [ ]
Hi :
invalidate_localsfr_localsc_framec c_memc = Somemr
Hw :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
prefix :
listevent
Hp :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w prefix M.Runningc, sr wr
Hs :
M.stepregistry ge M.Runningc, sr wr [ ] M.StoppedCoreEndRetVoid c, sr wr
H3 :
∀site : call_site, ¬external_sitege c site
H6 :
stepge c = DoneRetVoid
⊢
rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ mr; ls_rt ≔ sr; ls_fuel ≔ c_fuelc; ls_world ≔ wr

match goal withE : Semantics.stepge c = DoneRetVoid |- _⇒pose proof E as Hendend

payload :
Type
registry :
name → optioncontractcworldpayload
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
fuel :
Z
Q :
valnanofil_langregistry ge → statenanofil_langregistry ge → Prop
trace :
listevent
entry :
registration
w′ :
cworldpayload
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w Q
c :
config
sr :
R.state
wr :
cworldpayload
mr :
mem
Hreturn :
LK.callback_returnpayload entry LK.M.StoppedCoreEndRetVoid c, sr wr LK.RM.with_memc mr, sr w′
Hrun :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace M.StoppedCoreEndRetVoid c, sr wr
Hcs :
c_callersc = [ ]
Hi :
invalidate_localsfr_localsc_framec c_memc = Somemr
Hw :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
prefix :
listevent
Hp :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w prefix M.Runningc, sr wr
Hs :
M.stepregistry ge M.Runningc, sr wr [ ] M.StoppedCoreEndRetVoid c, sr wr
H3 :
∀site : call_site, ¬external_sitege c site
H6, Hend :
stepge c = DoneRetVoid
⊢
rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ mr; ls_rt ≔ sr; ls_fuel ≔ c_fuelc; ls_world ≔ wr

destruct adequate_labelledregistry ge fr m s fuel w Q Had _ _ Hp as Hreach _

payload :
Type
registry :
name → optioncontractcworldpayload
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
fuel :
Z
Q :
valnanofil_langregistry ge → statenanofil_langregistry ge → Prop
trace :
listevent
entry :
registration
w′ :
cworldpayload
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w Q
c :
config
sr :
R.state
wr :
cworldpayload
mr :
mem
Hreturn :
LK.callback_returnpayload entry LK.M.StoppedCoreEndRetVoid c, sr wr LK.RM.with_memc mr, sr w′
Hrun :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace M.StoppedCoreEndRetVoid c, sr wr
Hcs :
c_callersc = [ ]
Hi :
invalidate_localsfr_localsc_framec c_memc = Somemr
Hw :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
prefix :
listevent
Hp :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w prefix M.Runningc, sr wr
Hs :
M.stepregistry ge M.Runningc, sr wr [ ] M.StoppedCoreEndRetVoid c, sr wr
H3 :
∀site : call_site, ¬external_sitege c site
H6, Hend :
stepge c = DoneRetVoid
Hreach :
∀c0 : config s0 : R.state w0 : cworldpayload, M.Runningc, sr wr = M.Runningc0, s0 w0 → iris_reachregistry ge fr m s fuel w c0 s0 w0
⊢
rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ mr; ls_rt ≔ sr; ls_fuel ≔ c_fuelc; ls_world ≔ wr

pose proof Hreachc sr wr eq_refl as Hiris

payload :
Type
registry :
name → optioncontractcworldpayload
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
fuel :
Z
Q :
valnanofil_langregistry ge → statenanofil_langregistry ge → Prop
trace :
listevent
entry :
registration
w′ :
cworldpayload
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w Q
c :
config
sr :
R.state
wr :
cworldpayload
mr :
mem
Hreturn :
LK.callback_returnpayload entry LK.M.StoppedCoreEndRetVoid c, sr wr LK.RM.with_memc mr, sr w′
Hrun :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace M.StoppedCoreEndRetVoid c, sr wr
Hcs :
c_callersc = [ ]
Hi :
invalidate_localsfr_localsc_framec c_memc = Somemr
Hw :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
prefix :
listevent
Hp :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w prefix M.Runningc, sr wr
Hs :
M.stepregistry ge M.Runningc, sr wr [ ] M.StoppedCoreEndRetVoid c, sr wr
H3 :
∀site : call_site, ¬external_sitege c site
H6, Hend :
stepge c = DoneRetVoid
Hreach :
∀c0 : config s0 : R.state w0 : cworldpayload, M.Runningc, sr wr = M.Runningc0, s0 w0 → iris_reachregistry ge fr m s fuel w c0 s0 w0
Hiris :
iris_reachregistry ge fr m s fuel w c sr wr
⊢
rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ mr; ls_rt ≔ sr; ls_fuel ≔ c_fuelc; ls_world ≔ wr

destruct c as cf cs cm cfuel

payload :
Type
registry :
name → optioncontractcworldpayload
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
fuel :
Z
Q :
valnanofil_langregistry ge → statenanofil_langregistry ge → Prop
trace :
listevent
entry :
registration
w′ :
cworldpayload
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w Q
cf :
frame
cs :
listframe × pending
cm :
mem
cfuel :
Z
sr :
R.state
wr :
cworldpayload
mr :
mem
Hreturn :
LK.callback_returnpayload entry LK.M.StoppedCoreEndRetVoid c_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr LK.RM.with_memc_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel mr, sr w′
Hrun :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace M.StoppedCoreEndRetVoid c_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr
Hcs :
c_callersc_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel = [ ]
Hi :
invalidate_localsfr_localsc_framec_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel c_memc_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel = Somemr
Hw :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
prefix :
listevent
Hp :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w prefix M.Runningc_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr
Hs :
M.stepregistry ge M.Runningc_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr [ ] M.StoppedCoreEndRetVoid c_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr
H3 :
∀site : call_site, ¬external_sitege c_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel site
H6, Hend :
stepge c_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel = DoneRetVoid
Hreach :
∀c : config s0 : R.state w0 : cworldpayload, M.Runningc_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr = M.Runningc, s0 w0 → iris_reachregistry ge fr m s fuel w c s0 w0
Hiris :
iris_reachregistry ge fr m s fuel w c_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel sr wr
⊢
rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ mr; ls_rt ≔ sr; ls_fuel ≔ c_fuelc_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel; ls_world ≔ wr

cbn in Hcs

payload :
Type
registry :
name → optioncontractcworldpayload
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
fuel :
Z
Q :
valnanofil_langregistry ge → statenanofil_langregistry ge → Prop
trace :
listevent
entry :
registration
w′ :
cworldpayload
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w Q
cf :
frame
cs :
listframe × pending
cm :
mem
cfuel :
Z
sr :
R.state
wr :
cworldpayload
mr :
mem
Hreturn :
LK.callback_returnpayload entry LK.M.StoppedCoreEndRetVoid c_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr LK.RM.with_memc_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel mr, sr w′
Hrun :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace M.StoppedCoreEndRetVoid c_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr
Hcs :
cs = [ ]
Hi :
invalidate_localsfr_localsc_framec_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel c_memc_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel = Somemr
Hw :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
prefix :
listevent
Hp :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w prefix M.Runningc_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr
Hs :
M.stepregistry ge M.Runningc_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr [ ] M.StoppedCoreEndRetVoid c_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr
H3 :
∀site : call_site, ¬external_sitege c_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel site
H6, Hend :
stepge c_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel = DoneRetVoid
Hreach :
∀c : config s0 : R.state w0 : cworldpayload, M.Runningc_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr = M.Runningc, s0 w0 → iris_reachregistry ge fr m s fuel w c s0 w0
Hiris :
iris_reachregistry ge fr m s fuel w c_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel sr wr
⊢
rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ mr; ls_rt ≔ sr; ls_fuel ≔ c_fuelc_frame ≔ cf; c_callers ≔ cs; c_mem ≔ cm; c_fuel ≔ cfuel; ls_world ≔ wr

subst cs

payload :
Type
registry :
name → optioncontractcworldpayload
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
fuel :
Z
Q :
valnanofil_langregistry ge → statenanofil_langregistry ge → Prop
trace :
listevent
entry :
registration
w′ :
cworldpayload
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w Q
cf :
frame
cm :
mem
cfuel :
Z
sr :
R.state
wr :
cworldpayload
mr :
mem
Hrun :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace M.StoppedCoreEndRetVoid c_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr
Hreturn :
LK.callback_returnpayload entry LK.M.StoppedCoreEndRetVoid c_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr LK.RM.with_memc_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel mr, sr w′
Hi :
invalidate_localsfr_localsc_framec_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel c_memc_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel = Somemr
Hw :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
prefix :
listevent
Hiris :
iris_reachregistry ge fr m s fuel w c_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel sr wr
Hreach :
∀c : config s0 : R.state w0 : cworldpayload, M.Runningc_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr = M.Runningc, s0 w0 → iris_reachregistry ge fr m s fuel w c s0 w0
Hend, H6 :
stepge c_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel = DoneRetVoid
H3 :
∀site : call_site, ¬external_sitege c_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel site
Hs :
M.stepregistry ge M.Runningc_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr [ ] M.StoppedCoreEndRetVoid c_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr
Hp :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w prefix M.Runningc_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr
⊢
rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ mr; ls_rt ≔ sr; ls_fuel ≔ c_fuelc_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel; ls_world ≔ wr

eapply rtc_r ; exact Hiris |

payload :
Type
registry :
name → optioncontractcworldpayload
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
fuel :
Z
Q :
valnanofil_langregistry ge → statenanofil_langregistry ge → Prop
trace :
listevent
entry :
registration
w′ :
cworldpayload
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w Q
cf :
frame
cm :
mem
cfuel :
Z
sr :
R.state
wr :
cworldpayload
mr :
mem
Hrun :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace M.StoppedCoreEndRetVoid c_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr
Hreturn :
LK.callback_returnpayload entry LK.M.StoppedCoreEndRetVoid c_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr LK.RM.with_memc_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel mr, sr w′
Hi :
invalidate_localsfr_localsc_framec_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel c_memc_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel = Somemr
Hw :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
prefix :
listevent
Hiris :
iris_reachregistry ge fr m s fuel w c_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel sr wr
Hreach :
∀c : config s0 : R.state w0 : cworldpayload, M.Runningc_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr = M.Runningc, s0 w0 → iris_reachregistry ge fr m s fuel w c s0 w0
Hend, H6 :
stepge c_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel = DoneRetVoid
H3 :
∀site : call_site, ¬external_sitege c_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel site
Hs :
M.stepregistry ge M.Runningc_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr [ ] M.StoppedCoreEndRetVoid c_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr
Hp :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w prefix M.Runningc_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel, sr wr
⊢
erased_stepconf_exprc_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel, conf_statec_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel sr wr EEndRetVoid, ls_mem ≔ mr; ls_rt ≔ sr; ls_fuel ≔ c_fuelc_frame ≔ cf; c_callers ≔ [ ]; c_mem ≔ cm; c_fuel ≔ cfuel; ls_world ≔ wr

exact head_erasedregistry ge [ ] _ _ _ _ hs_returnregistry ge cf cm sr cfuel wr RetVoid mr Hend I Hi

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros Had Hrun Hreturn
destruct LK.callback_return_endpointpayload _ _ _ _ Hreturn as c & sr & wr & mr & → & Hcs & Hi & Hms & Hw & Hshutdown
exists c, sr, wr, mr
repeat split ; try assumption ; try reflexivity
apply linked_run in Hrun
cbn [ logic_state ] in Hrun
destruct run_last_ _ _ _ _ Hrun as Heq | prefix & mid & tail & Hp & Hs ; discriminate Heq |
inversion Hs ; subst
match goal withE : Semantics.stepge c = DoneRetVoid |- _⇒pose proof E as Hendend
destruct adequate_labelledregistry ge fr m s fuel w Q Had _ _ Hp as Hreach _
pose proof Hreachc sr wr eq_refl as Hiris
destruct c as cf cs cm cfuel
cbn in Hcs
subst cs
eapply rtc_r ; exact Hiris |
exact head_erasedregistry ge [ ] _ _ _ _ hs_returnregistry ge cf cm sr cfuel wr RetVoid mr Hend I Hi

Failure freedom is independent of a normal return: outcome-only heap_labelled_safe also covers callbacks that exit or never return.

189Theorem callback_wp_safe
∀ Σ HinvP : invGpreSΣ HheapP : gen_heapGpreSpiece pval Σ payload : Type registry : name → optioncontractcworldpayload wi : mem → cworldpayload → gmappiece pval → Prop ge fr m s w h0 fuel trace why ms′ w′
R.readys m
live_disjointm
agreesm h0
wim w h0
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let _ : irisGS_genHasNoLc nanofil_langregistry ge Σ ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {_. True}
LK.M.runregistry ge LK.M.RunningmkConfigfr [ ] m fuel, s w trace LK.M.Stoppedwhy ms′ w′
¬failure_endingwhy
Explore proof 5 tactics

Initial goal

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
⊢
R.readys m
→
live_disjointm
→
agreesm h0
→
wim w h0
→
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {_. True}
→
∀fuel : Z trace : listevent why : ending ms′ : LK.M.P.I.RM.mstate w′ : cworldpayload, LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace LK.M.Stoppedwhy ms′ w′ → ¬failure_endingwhy

intros Hr Hd Ha Hw Hwp fuel trace why ms′ w′ Hrun

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {_. True}
fuel :
Z
trace :
listevent
why :
ending
ms′ :
LK.M.P.I.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace LK.M.Stoppedwhy ms′ w′
⊢
¬failure_endingwhy

pose proof heap_labelled_safeΣ registry wi ge fr m s w h0 λ_ ⇒ True Hr Hd Ha Hw Hwp fuel as Hsafe

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {_. True}
fuel :
Z
trace :
listevent
why :
ending
ms′ :
LK.M.P.I.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace LK.M.Stoppedwhy ms′ w′
Hsafe :
L.labelled_saferegistry ge fr m s w fuel λ_ : outcome ⇒ True
⊢
¬failure_endingwhy

apply linked_run in Hrun

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {_. True}
fuel :
Z
trace :
listevent
why :
ending
ms′ :
LK.M.P.I.RM.mstate
w′ :
cworldpayload
Hrun :
M.runregistry ge logic_stateLK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace logic_stateLK.M.Stoppedwhy ms′ w′
Hsafe :
L.labelled_saferegistry ge fr m s w fuel λ_ : outcome ⇒ True
⊢
¬failure_endingwhy

cbn [ logic_state ] in Hrun

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {_. True}
fuel :
Z
trace :
listevent
why :
ending
ms′ :
LK.M.P.I.RM.mstate
w′ :
cworldpayload
Hrun :
M.runregistry ge M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace M.Stoppedwhy ms′ w′
Hsafe :
L.labelled_saferegistry ge fr m s w fuel λ_ : outcome ⇒ True
⊢
¬failure_endingwhy

exact proj1Hsafe_ _ _ _ Hrun

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros Hr Hd Ha Hw Hwp fuel trace why ms′ w′ Hrun
pose proof heap_labelled_safeΣ registry wi ge fr m s w h0 λ_ ⇒ True Hr Hd Ha Hw Hwp fuel as Hsafe
apply linked_run in Hrun
cbn [ logic_state ] in Hrun
exact proj1Hsafe_ _ _ _ Hrun

A handler's WP yields its pure postcondition at Linked's actual return memory and current world. No old payload, registry or status is restored, and no return is required of nonreturning executions.

214Theorem callback_wp_return
∀ Σ HinvP : invGpreSΣ HheapP : gen_heapGpreSpiece pval Σ payload : Type registry : name → optioncontractcworldpayload wi : mem → cworldpayload → gmappiece pval → Prop ge fr m s w h0 Q : mem → cworldpayload → Prop fuel trace stopped entry ms′ w′
R.readys m
live_disjointm
agreesm h0
wim w h0
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let _ : irisGS_genHasNoLc nanofil_langregistry ge Σ ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {Ψ}
∧
∀σ, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
LK.M.runregistry ge LK.M.RunningmkConfigfr [ ] m fuel, s w trace stopped
LK.callback_returnpayload entry stopped ms′ w′
∃c sr wr m_return, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ fstw′ = fstwr ∧ shutdown_stepsndwr ReturnCallback sndw′ ∧ Qm_return wr
Explore proof 16 tactics

Initial goal

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
⊢
R.readys m
→
live_disjointm
→
agreesm h0
→
wim w h0
→
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
→
∀fuel : Z trace : listevent stopped : LK.M.statecworldpayload entry : registration ms′ : LK.RM.mstate w′ : cworldpayload, LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped → LK.callback_returnpayload entry stopped ms′ w′ → ∃c : config sr : R.state wr : cworldpayload m_return : mem, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ Qm_return wr

intros Hr Hd Ha Hw Hwp fuel trace stopped entry ms′ w′ Hrun Hreturn

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
⊢
∃c : config sr : R.state wr : cworldpayload m_return : mem, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ Qm_return wr

assert Had : @adequatenanofil_langregistry ge NotStuck ERunfr mkLstatem s fuel w λo σ ⇒ o = RetVoid → Qls_memσ ls_worldσ

2 open

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
⊢
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w λo : valnanofil_langregistry ge σ : statenanofil_langregistry ge ⇒ o = RetVoid → Qls_memσ ls_worldσ
focused goal
Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w λo : valnanofil_langregistry ge σ : statenanofil_langregistry ge ⇒ o = RetVoid → Qls_memσ ls_worldσ
⊢
∃c : config sr : R.state wr : cworldpayload m_return : mem, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ Qm_return wr

{eapply heap_exact_adequacyΣ registry wi ge fr m s w h0 fuel ; exact Hr | exact Hd | exact Ha | exact Hw |

2 open

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
⊢
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr {v. Ψv}
∧
∀o : outcome σ : L.lstatecworldpayload, heap_interpwi σ ∗ Ψo ⊢ ⌜o = RetVoid → Qls_memσ ls_worldσ⌝
deferred goal
Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w λo : valnanofil_langregistry ge σ : statenanofil_langregistry ge ⇒ o = RetVoid → Qls_memσ ls_worldσ
⊢
∃c : config sr : R.state wr : cworldpayload m_return : mem, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ Qm_return wr

intros HinvG HheapG

2 open

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
HinvG :
invGS_genHasNoLc Σ
HheapG :
gen_heapGSpiece pval Σ
⊢
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr {v. Ψv}
∧
∀o : outcome σ : L.lstatecworldpayload, heap_interpwi σ ∗ Ψo ⊢ ⌜o = RetVoid → Qls_memσ ls_worldσ⌝
deferred goal
Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w λo : valnanofil_langregistry ge σ : statenanofil_langregistry ge ⇒ o = RetVoid → Qls_memσ ls_worldσ
⊢
∃c : config sr : R.state wr : cworldpayload m_return : mem, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ Qm_return wr

destruct HwpHinvG HheapG as Ψ & Hbody & Hpost

2 open

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
HinvG :
invGS_genHasNoLc Σ
HheapG :
gen_heapGSpiece pval Σ
Ψ :
outcome → iPropΣ
Hbody :
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr {v. Ψv}
Hpost :
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
⊢
∃ Ψ0 : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr {v. Ψ0v}
∧
∀o : outcome σ : L.lstatecworldpayload, heap_interpwi σ ∗ Ψ0o ⊢ ⌜o = RetVoid → Qls_memσ ls_worldσ⌝
deferred goal
Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w λo : valnanofil_langregistry ge σ : statenanofil_langregistry ge ⇒ o = RetVoid → Qls_memσ ls_worldσ
⊢
∃c : config sr : R.state wr : cworldpayload m_return : mem, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ Qm_return wr

exists Ψ

2 open

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
HinvG :
invGS_genHasNoLc Σ
HheapG :
gen_heapGSpiece pval Σ
Ψ :
outcome → iPropΣ
Hbody :
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr {v. Ψv}
Hpost :
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
⊢
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr {v. Ψv}
∧
∀o : outcome σ : L.lstatecworldpayload, heap_interpwi σ ∗ Ψo ⊢ ⌜o = RetVoid → Qls_memσ ls_worldσ⌝
deferred goal
Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w λo : valnanofil_langregistry ge σ : statenanofil_langregistry ge ⇒ o = RetVoid → Qls_memσ ls_worldσ
⊢
∃c : config sr : R.state wr : cworldpayload m_return : mem, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ Qm_return wr

split ; exact Hbody |

2 open

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
HinvG :
invGS_genHasNoLc Σ
HheapG :
gen_heapGSpiece pval Σ
Ψ :
outcome → iPropΣ
Hbody :
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr {v. Ψv}
Hpost :
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
⊢
∀o : outcome σ : L.lstatecworldpayload, heap_interpwi σ ∗ Ψo ⊢ ⌜o = RetVoid → Qls_memσ ls_worldσ⌝
deferred goal
Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w λo : valnanofil_langregistry ge σ : statenanofil_langregistry ge ⇒ o = RetVoid → Qls_memσ ls_worldσ
⊢
∃c : config sr : R.state wr : cworldpayload m_return : mem, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ Qm_return wr

intros o σ

2 open

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
HinvG :
invGS_genHasNoLc Σ
HheapG :
gen_heapGSpiece pval Σ
Ψ :
outcome → iPropΣ
Hbody :
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr {v. Ψv}
Hpost :
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
o :
outcome
σ :
L.lstatecworldpayload
⊢
heap_interpwi σ ∗ Ψo ⊢ ⌜o = RetVoid → Qls_memσ ls_worldσ⌝
deferred goal
Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w λo : valnanofil_langregistry ge σ : statenanofil_langregistry ge ⇒ o = RetVoid → Qls_memσ ls_worldσ
⊢
∃c : config sr : R.state wr : cworldpayload m_return : mem, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ Qm_return wr

iIntros H

2 open

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
HinvG :
invGS_genHasNoLc Σ
HheapG :
gen_heapGSpiece pval Σ
Ψ :
outcome → iPropΣ
Hbody :
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr {v. Ψv}
Hpost :
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
o :
outcome
σ :
L.lstatecworldpayload
H :
heap_interpwi σ ∗ Ψo
∗
⌜o = RetVoid → Qls_memσ ls_worldσ⌝
deferred goal
Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w λo : valnanofil_langregistry ge σ : statenanofil_langregistry ge ⇒ o = RetVoid → Qls_memσ ls_worldσ
⊢
∃c : config sr : R.state wr : cworldpayload m_return : mem, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ Qm_return wr

iIntros →

2 open

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
HinvG :
invGS_genHasNoLc Σ
HheapG :
gen_heapGSpiece pval Σ
Ψ :
outcome → iPropΣ
Hbody :
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr {v. Ψv}
Hpost :
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
σ :
L.lstatecworldpayload
H :
heap_interpwi σ ∗ ΨRetVoid
∗
⌜Qls_memσ ls_worldσ⌝
deferred goal
Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w λo : valnanofil_langregistry ge σ : statenanofil_langregistry ge ⇒ o = RetVoid → Qls_memσ ls_worldσ
⊢
∃c : config sr : R.state wr : cworldpayload m_return : mem, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ Qm_return wr

iApply Hpost

2 open

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
HinvG :
invGS_genHasNoLc Σ
HheapG :
gen_heapGSpiece pval Σ
Ψ :
outcome → iPropΣ
Hbody :
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr {v. Ψv}
Hpost :
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
σ :
L.lstatecworldpayload
H :
heap_interpwi σ ∗ ΨRetVoid
∗
heap_interpwi σ ∗ ΨRetVoid
deferred goal
Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w λo : valnanofil_langregistry ge σ : statenanofil_langregistry ge ⇒ o = RetVoid → Qls_memσ ls_worldσ
⊢
∃c : config sr : R.state wr : cworldpayload m_return : mem, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ Qm_return wr

iExact H

deferred goal
Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w λo : valnanofil_langregistry ge σ : statenanofil_langregistry ge ⇒ o = RetVoid → Qls_memσ ls_worldσ
⊢
∃c : config sr : R.state wr : cworldpayload m_return : mem, stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ Qm_return wr

destruct callback_return_reachable_ _ _ _ _ _ _ _ _ _ _ _ _ Had Hrun Hreturn as c & sr & wr & mr & Hst & Hcs & Hi & Hms & Hworld & Hshutdown & Hreach

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w λo : valnanofil_langregistry ge σ : statenanofil_langregistry ge ⇒ o = RetVoid → Qls_memσ ls_worldσ
c :
config
sr :
R.state
wr :
cworldpayload
mr :
mem
Hst :
stopped = LK.M.StoppedCoreEndRetVoid c, sr wr
Hcs :
c_callersc = [ ]
Hi :
invalidate_localsfr_localsc_framec c_memc = Somemr
Hms :
ms′ = with_memc mr, sr
Hworld :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
Hreach :
rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ mr; ls_rt ≔ sr; ls_fuel ≔ c_fuelc; ls_world ≔ wr
⊢
∃c0 : config sr0 : R.state wr0 : cworldpayload m_return : mem, stopped = LK.M.StoppedCoreEndRetVoid c0, sr0 wr0 ∧ invalidate_localsfr_localsc_framec0 c_memc0 = Somem_return ∧ ms′ = with_memc0 m_return, sr0 ∧ w′.1 = wr0.1 ∧ shutdown_stepwr0.2 ReturnCallback w′.2 ∧ Qm_return wr0

exists c, sr, wr, mr

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w λo : valnanofil_langregistry ge σ : statenanofil_langregistry ge ⇒ o = RetVoid → Qls_memσ ls_worldσ
c :
config
sr :
R.state
wr :
cworldpayload
mr :
mem
Hst :
stopped = LK.M.StoppedCoreEndRetVoid c, sr wr
Hcs :
c_callersc = [ ]
Hi :
invalidate_localsfr_localsc_framec c_memc = Somemr
Hms :
ms′ = with_memc mr, sr
Hworld :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
Hreach :
rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ mr; ls_rt ≔ sr; ls_fuel ≔ c_fuelc; ls_world ≔ wr
⊢
stopped = LK.M.StoppedCoreEndRetVoid c, sr wr ∧ invalidate_localsfr_localsc_framec c_memc = Somemr ∧ ms′ = with_memc mr, sr ∧ w′.1 = wr.1 ∧ shutdown_stepwr.2 ReturnCallback w′.2 ∧ Qmr wr

repeat split ; try assumption

Σ :
gFunctors
HinvP :
invGpreSΣ
HheapP :
gen_heapGpreSpiece pval Σ
payload :
Type
registry :
name → optioncontractcworldpayload
wi :
mem → cworldpayload → gmappiece pval → Prop
ge :
genv
fr :
frame
m :
mem
s :
R.state
w :
cworldpayload
h0 :
gmappiece pval
Q :
mem → cworldpayload → Prop
Hr :
R.readys m
Hd :
live_disjointm
Ha :
agreesm h0
Hw :
wim w h0
Hwp :
∀ HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ  ,
∃ Ψ : outcome → iPropΣ  ,
∗l↦v∈h0pointstol DfracOwn1 v
⊢
let H ≔ nanofil_irisGSregistry wi ge in
WPERunfr : language.exprnanofil_langregistry ge {v. Ψv}
∧
∀σ : L.lstatecworldpayload, heap_interpwi σ ∗ ΨRetVoid ⊢ ⌜Qls_memσ ls_worldσ⌝
fuel :
Z
trace :
listevent
stopped :
LK.M.statecworldpayload
entry :
registration
ms′ :
LK.RM.mstate
w′ :
cworldpayload
Hrun :
LK.M.runregistry ge LK.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s w trace stopped
Hreturn :
LK.callback_returnpayload entry stopped ms′ w′
Had :
adequateNotStuck ERunfr ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w λo : valnanofil_langregistry ge σ : statenanofil_langregistry ge ⇒ o = RetVoid → Qls_memσ ls_worldσ
c :
config
sr :
R.state
wr :
cworldpayload
mr :
mem
Hst :
stopped = LK.M.StoppedCoreEndRetVoid c, sr wr
Hcs :
c_callersc = [ ]
Hi :
invalidate_localsfr_localsc_framec c_memc = Somemr
Hms :
ms′ = with_memc mr, sr
Hworld :
w′.1 = wr.1
Hshutdown :
shutdown_stepwr.2 ReturnCallback w′.2
Hreach :
rtcerased_step ERunfr, ls_mem ≔ m; ls_rt ≔ s; ls_fuel ≔ fuel; ls_world ≔ w EEndRetVoid, ls_mem ≔ mr; ls_rt ≔ sr; ls_fuel ≔ c_fuelc; ls_world ≔ wr
⊢
Qmr wr

exact adequate_result_ _ _ _ Had [ ] _ _ Hreach eq_refl

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros Hr Hd Ha Hw Hwp fuel trace stopped entry ms′ w′ Hrun Hreturn
assert Had : @adequatenanofil_langregistry ge NotStuck ERunfr mkLstatem s fuel w λo σ ⇒ o = RetVoid → Qls_memσ ls_worldσ
{eapply heap_exact_adequacyΣ registry wi ge fr m s w h0 fuel ; exact Hr | exact Hd | exact Ha | exact Hw |
intros HinvG HheapG
destruct HwpHinvG HheapG as Ψ & Hbody & Hpost
exists Ψ
split ; exact Hbody |
intros o σ
iIntros H
iIntros →
iApply Hpost
iExact H
destruct callback_return_reachable_ _ _ _ _ _ _ _ _ _ _ _ _ Had Hrun Hreturn as c & sr & wr & mr & Hst & Hcs & Hi & Hms & Hworld & Hshutdown & Hreach
exists c, sr, wr, mr
repeat split ; try assumption
exact adequate_result_ _ _ _ Had [ ] _ _ Hreach eq_refl

CallbackLogicOn over a Logic instance of its own.

254Module CallbackLogic R : Runtime
255Module LG0 ≔ Logic R
Include CallbackLogicOn R LG0