rocq/theories/Linked.v
Retained void callbacks at the labelled program boundary. Entry is independently admitted AFTER the exit-registry pop; execution uses ordinary ExternalMachine steps. A stopped return snapshot precedes local teardown, so the shutdown endpoint reconstructs that memory. This slice does not intercept exit requests or claim native coverage.
From Stdlib Require Import String ZArith List Bool Lia
From Nanofil Require Import Term Syntax Values Memory Runtime Ops Semantics Machine Identity ExternalCalls Startup Stdio Shutdown ExitMemory Walk ExternalMachine
Import ListNotations
Open Scope Z_scope
Open Scope list_scope
A detached installed slot retains its callable address AND capability. Free/reserved slots cannot select callback code.
Native argument classes, not re-evaluated IR operands. The dummy constants are immaterial to indirect_call_conv, which reads only these classes and the separately retained words.
The current signed status is passed as full canonical int bits, not the host's low-byte wait status. This pin calls cxa(arg,status).
The exact selected defined code and generic calling convention. Module checking and semantic admission are not consequences of a retained Fn capability or of a successful call_frame. Only void, nonvariadic callbacks are covered by this first bridge.
exit_slot_pendingslot = entry ∧ checked_modulege_modulege ∧ ∃symbol function f converted, callback_targetslot = Somesymbol, function ∧ ptr_capfunction = Fnsymbol ∧ function_check_resge function = Someok ∧ find_fnge symbol = SomeDefinedf ∧ fn_retf = RVoid ∧ variadic_funcf = false ∧ indirect_call_convf CVoid callback_argsslot callback_wordsslot status = SomeConvertedconverted None ∧ call_framef converted = Somefr
Local teardown changes only region lifetimes, never bytes or aux, including a global slot retaining a pointer into the ended frame.
Explore proof 10 tactics
Initial goal
unfold invalidate_locals
⊢
fold_left
let* m0 ≔ acc in
match sndl with
locals
Somem
=
Somem′
→
intros locals
locals :
listname × optionZ
⊢
fold_left
let* m0 ≔ acc in
match sndl with
locals
Somem
=
Somem′
→
induction locals as | x slot locals IH ; simpl ; intros m m′ H
2 openfocused goal
x :
slot :
optionZ
locals :
listname × optionZ
IH :
fold_left
let* m0 ≔ acc in
match sndl with
locals
Somem
=
Somem′
→
m, m′ :
H :
fold_left
let* m ≔ acc in
locals
=
Somem′
–injection H as ←
2 opendeferred goal
x :
slot :
optionZ
locals :
listname × optionZ
IH :
fold_left
let* m0 ≔ acc in
match sndl with
locals
Somem
=
Somem′
→
m, m′ :
H :
fold_left
let* m ≔ acc in
locals
=
Somem′
auto
deferred goal
x :
slot :
optionZ
locals :
listname × optionZ
IH :
fold_left
let* m0 ≔ acc in
match sndl with
locals
Somem
=
Somem′
→
m, m′ :
H :
fold_left
let* m ≔ acc in
locals
=
Somem′
–destruct slot as base | ; | exact IH_ _ H
x :
base :
Z
locals :
listname × optionZ
IH :
fold_left
let* m0 ≔ acc in
match sndl with
locals
Somem
=
Somem′
→
m, m′ :
H :
fold_left
let* m ≔ acc in
locals
=
Somem′
destruct object_regionbase m_regionsm as reg | eqn: Er ; | rewrite fold_left_none in H ; discriminate H
x :
base :
Z
locals :
listname × optionZ
IH :
fold_left
let* m0 ≔ acc in
match sndl with
locals
Somem
=
Somem′
→
m, m′ :
reg :
Er :
object_regionbase m_regionsm = Somereg
H :
fold_left
let* m ≔ acc in
locals
=
Somem′
destruct r_kindreg , r_lifereg ; simpl in H ; try rewrite fold_left_none in H ; discriminate H
x :
base :
Z
locals :
listname × optionZ
IH :
fold_left
let* m0 ≔ acc in
match sndl with
locals
Somem
=
Somem′
→
m, m′ :
reg :
Er :
object_regionbase m_regionsm = Somereg
H :
fold_left
let* m ≔ acc in
locals
=
Somem′
destruct replace_regionbase _ m_regionsm as rs | eqn: Ers ; | rewrite fold_left_none in H ; discriminate H
x :
base :
Z
locals :
listname × optionZ
IH :
fold_left
let* m0 ≔ acc in
match sndl with
locals
Somem
=
Somem′
→
m, m′ :
reg :
Er :
object_regionbase m_regionsm = Somereg
rs :
listregion
Ers :
H :
fold_left
let* m ≔ acc in
locals
=
Somem′
exact IH_ _ H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold invalidate_locals
intros locals
induction locals as | x slot locals IH ; simpl ; intros m m′ H
–injection H as ←
auto
–destruct slot as base | ; | exact IH_ _ H
destruct object_regionbase m_regionsm as reg | eqn: Er ; | rewrite fold_left_none in H ; discriminate H
destruct r_kindreg , r_lifereg ; simpl in H ; try rewrite fold_left_none in H ; discriminate H
destruct replace_regionbase _ m_regionsm as rs | eqn: Ers ; | rewrite fold_left_none in H ; discriminate H
exact IH_ _ H
This additive boundary changes neither machine nor runtime.
Import RM
One authoritative shutdown inventory accompanies arbitrary libc state. Callback effects update this very world; return never restores a registration-time snapshot.
payload × shutdown_state%type
Entry is checked at the current post-pop memory/runtime/world. The physical pop/mark and its effects remain ExitMemory's separate boundary; this relation does not claim them from a decoded slot alone. No run, successful callback or return is hidden inside admission.
91Definition callback_entryadmitted : registration → R.state → mem → callback_world → Prop ge slot entry s m w fuel c : Prop ≔
R.readys m ∧ shutdown_atsndw = InCallbackentry ∧ shutdown_uniquesndw ∧ Inregistration_tokenentry shutdown_consumedsndw ∧ −2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31 ∧ admittedentry s m w ∧ ∃fr, callback_codege slot entry shutdown_statussndw fr ∧ c = mkConfigfr [ ] m fuel
Successful return reconstructs the memory that Semantics computed but did not retain in Done. It keeps the CURRENT libc payload, status, pending list, consumed history, output state, runtime and fuel. Other terminals, including an already completed ExternalExit, do not resume.
105Inductive callback_returnentry : registration : M.statecallback_world → mstate → callback_world → Prop ≔
∀ c s data status pending consumed q m_return
c_callersc = [ ]
shutdown_uniquemkShutdownInCallbackentry status pending consumed q
Inregistration_tokenentry consumed
invalidate_localsfr_localsc_framec c_memc = Somem_return
callback_return_void
callback_returnentry M.StoppedCoreEndRetVoid c, s data, mkShutdownInCallbackentry status pending consumed q with_memc m_return, s data, mkShutdownHandlers status pending consumed q
The endpoint exposes the very same m_return needed by the handler's Iris return postcondition, not merely an existential outcome state.
∀ entry st ms′ w′
callback_returnentry st ms′ w′
∃c s w m_return, st = M.StoppedCoreEndRetVoid c, s w ∧ c_callersc = [ ] ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, s ∧ fstw′ = fstw ∧ shutdown_stepsndw ReturnCallback sndw′
Explore proof 5 tactics
Initial goal
payload :
Type
⊢
∀entry : registration st : M.statecallback_world ms′ : mstate w′ : callback_world, callback_returnentry st ms′ w′ → ∃c : config s : R.state w : callback_world m_return : mem, st = M.StoppedCoreEndRetVoid c, s w ∧ c_callersc = [ ] ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, s ∧ fstw′ = fstw ∧ shutdown_stepsndw ReturnCallback sndw′
intros entry st ms′ w′ H
⊢
∃c : config s : R.state w : callback_world m_return : mem, st = M.StoppedCoreEndRetVoid c, s w ∧ c_callersc = [ ] ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ ms′ = with_memc m_return, s ∧ fstw′ = fstw ∧ shutdown_stepsndw ReturnCallback sndw′
destruct H
payload :
Type
entry :
c :
s :
R.state
data :
payload
status :
Z
pending :
listregistration
consumed :
listnat
q :
m_return :
H :
c_callersc = [ ]
H0 :
shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
H1 :
Inregistration_tokenentry consumed
H2 :
invalidate_localsfr_localsc_framec c_memc = Somem_return
⊢
∃c0 : config s0 : R.state w : callback_world m_return0 : mem, M.StoppedCoreEndRetVoid c, s data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q = M.StoppedCoreEndRetVoid c0, s0 w ∧ c_callersc0 = [ ] ∧ invalidate_localsfr_localsc_framec0 c_memc0 = Somem_return0 ∧ with_memc m_return, s = with_memc0 m_return0, s0 ∧ fstdata, shutdown_at ≔ Handlers; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q = fstw ∧ shutdown_stepsndw ReturnCallback snddata, shutdown_at ≔ Handlers; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
exists c, s, data, mkShutdownInCallbackentry status pending consumed q, m_return
payload :
Type
entry :
c :
s :
R.state
data :
payload
status :
Z
pending :
listregistration
consumed :
listnat
q :
m_return :
H :
c_callersc = [ ]
H0 :
shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
H1 :
Inregistration_tokenentry consumed
H2 :
invalidate_localsfr_localsc_framec c_memc = Somem_return
⊢
M.StoppedCoreEndRetVoid c, s data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q = M.StoppedCoreEndRetVoid c, s data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ∧ c_callersc = [ ] ∧ invalidate_localsfr_localsc_framec c_memc = Somem_return ∧ with_memc m_return, s = with_memc m_return, s ∧ fstdata, shutdown_at ≔ Handlers; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q = fstdata, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ∧ shutdown_stepsnddata, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ReturnCallback snddata, shutdown_at ≔ Handlers; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
repeat split ; auto
payload :
Type
entry :
c :
s :
R.state
data :
payload
status :
Z
pending :
listregistration
consumed :
listnat
q :
m_return :
H :
c_callersc = [ ]
H0 :
shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
H1 :
Inregistration_tokenentry consumed
H2 :
invalidate_localsfr_localsc_framec c_memc = Somem_return
⊢
shutdown_stepsnddata, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ReturnCallback snddata, shutdown_at ≔ Handlers; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
constructor
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros entry st ms′ w′ H
destruct H
exists c, s, data, mkShutdownInCallbackentry status pending consumed q, m_return
repeat split ; auto
constructor
Readiness and object persistence along ordinary labelled callback prefixes; this makes no return, termination or failure-freedom claim.
Explore proof 7 tactics
Initial goal
payload :
Type
⊢
∀registry : name → optioncontractcallback_world ge : genv st : M.statecallback_world trace : listevent st′ : M.statecallback_world, ge_freege = R.free → M.runregistry ge st trace st′ → M.state_readycallback_world st → M.state_readycallback_world st′ ∧ persistsc_memfstM.machine_ofcallback_world st c_memfstM.machine_ofcallback_world st′
intros registry ge st trace st′ Hfree H
payload :
Type
registry :
name → optioncontractcallback_world
ge :
st :
M.statecallback_world
trace :
listevent
st′ :
M.statecallback_world
Hfree :
ge_freege = R.free
H :
M.runregistry ge st trace st′
⊢
M.state_readycallback_world st → M.state_readycallback_world st′ ∧ persistsc_memfstM.machine_ofcallback_world st c_memfstM.machine_ofcallback_world st′
induction H ; intros Hr
2 openpayload :
Type
registry :
name → optioncontractcallback_world
ge :
Hfree :
ge_freege = R.free
st :
M.statecallback_world
Hr :
M.state_readycallback_world st
⊢
M.state_readycallback_world st ∧ persistsc_memfstM.machine_ofcallback_world st c_memfstM.machine_ofcallback_world st
focused goal
payload :
Type
registry :
name → optioncontractcallback_world
ge :
Hfree :
ge_freege = R.free
st :
M.statecallback_world
trace :
listevent
mid :
M.statecallback_world
tail :
listevent
last :
M.statecallback_world
H :
M.stepregistry ge st trace mid
H0 :
M.runregistry ge mid tail last
IHrun :
M.state_readycallback_world mid → M.state_readycallback_world last ∧ persistsc_memfstM.machine_ofcallback_world mid c_memfstM.machine_ofcallback_world last
Hr :
M.state_readycallback_world st
⊢
M.state_readycallback_world last ∧ persistsc_memfstM.machine_ofcallback_world st c_memfstM.machine_ofcallback_world last
–split ; exact Hr | apply persists_refl
deferred goal
payload :
Type
registry :
name → optioncontractcallback_world
ge :
Hfree :
ge_freege = R.free
st :
M.statecallback_world
trace :
listevent
mid :
M.statecallback_world
tail :
listevent
last :
M.statecallback_world
H :
M.stepregistry ge st trace mid
H0 :
M.runregistry ge mid tail last
IHrun :
M.state_readycallback_world mid → M.state_readycallback_world last ∧ persistsc_memfstM.machine_ofcallback_world mid c_memfstM.machine_ofcallback_world last
Hr :
M.state_readycallback_world st
⊢
M.state_readycallback_world last ∧ persistsc_memfstM.machine_ofcallback_world st c_memfstM.machine_ofcallback_world last
–pose proof M.step_ready_ _ _ _ _ _ Hfree H Hr as Hr1
payload :
Type
registry :
name → optioncontractcallback_world
ge :
Hfree :
ge_freege = R.free
st :
M.statecallback_world
trace :
listevent
mid :
M.statecallback_world
tail :
listevent
last :
M.statecallback_world
H :
M.stepregistry ge st trace mid
H0 :
M.runregistry ge mid tail last
IHrun :
M.state_readycallback_world mid → M.state_readycallback_world last ∧ persistsc_memfstM.machine_ofcallback_world mid c_memfstM.machine_ofcallback_world last
Hr :
M.state_readycallback_world st
Hr1 :
M.state_readycallback_world mid
⊢
M.state_readycallback_world last ∧ persistsc_memfstM.machine_ofcallback_world st c_memfstM.machine_ofcallback_world last
destruct IHrunHr1 as Hr′ Hp
payload :
Type
registry :
name → optioncontractcallback_world
ge :
Hfree :
ge_freege = R.free
st :
M.statecallback_world
trace :
listevent
mid :
M.statecallback_world
tail :
listevent
last :
M.statecallback_world
H :
M.stepregistry ge st trace mid
H0 :
M.runregistry ge mid tail last
IHrun :
M.state_readycallback_world mid → M.state_readycallback_world last ∧ persistsc_memfstM.machine_ofcallback_world mid c_memfstM.machine_ofcallback_world last
Hr :
M.state_readycallback_world st
Hr1 :
M.state_readycallback_world mid
Hr′ :
M.state_readycallback_world last
Hp :
persistsc_memfstM.machine_ofcallback_world mid c_memfstM.machine_ofcallback_world last
⊢
M.state_readycallback_world last ∧ persistsc_memfstM.machine_ofcallback_world st c_memfstM.machine_ofcallback_world last
split ; exact Hr′ |
payload :
Type
registry :
name → optioncontractcallback_world
ge :
Hfree :
ge_freege = R.free
st :
M.statecallback_world
trace :
listevent
mid :
M.statecallback_world
tail :
listevent
last :
M.statecallback_world
H :
M.stepregistry ge st trace mid
H0 :
M.runregistry ge mid tail last
IHrun :
M.state_readycallback_world mid → M.state_readycallback_world last ∧ persistsc_memfstM.machine_ofcallback_world mid c_memfstM.machine_ofcallback_world last
Hr :
M.state_readycallback_world st
Hr1 :
M.state_readycallback_world mid
Hr′ :
M.state_readycallback_world last
Hp :
persistsc_memfstM.machine_ofcallback_world mid c_memfstM.machine_ofcallback_world last
⊢
persistsc_memfstM.machine_ofcallback_world st c_memfstM.machine_ofcallback_world last
eapply persists_trans ; eapply M.step_persists ; eauto | exact Hp
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros registry ge st trace st′ Hfree H
induction H ; intros Hr
–split ; exact Hr | apply persists_refl
–pose proof M.step_ready_ _ _ _ _ _ Hfree H Hr as Hr1
destruct IHrunHr1 as Hr′ Hp
split ; exact Hr′ |
eapply persists_trans ; eapply M.step_persists ; eauto | exact Hp
A return remains ready and retains every identity after invalidating locals; exact byte/aux preservation is stronger than mere keptness.
Explore proof 10 tactics
Initial goal
payload :
Type
⊢
∀entry : registration st : M.statecallback_world ms′ : mstate w′ : callback_world, callback_returnentry st ms′ w′ → M.state_readycallback_world st → ready_statems′ ∧ persistsc_memfstM.machine_ofcallback_world st c_memfstms′ ∧ m_bytesc_memfstms′ = m_bytesc_memfstM.machine_ofcallback_world st ∧ m_auxc_memfstms′ = m_auxc_memfstM.machine_ofcallback_world st
intros entry st ms′ w′ H
⊢
M.state_readycallback_world st → ready_statems′ ∧ persistsc_memfstM.machine_ofcallback_world st c_memfstms′ ∧ m_bytesc_memfstms′ = m_bytesc_memfstM.machine_ofcallback_world st ∧ m_auxc_memfstms′ = m_auxc_memfstM.machine_ofcallback_world st
destruct H as c s data status pending consumed q m_return Hcallers Hunique Htoken Hlocals
payload :
Type
entry :
c :
s :
R.state
data :
payload
status :
Z
pending :
listregistration
consumed :
listnat
q :
m_return :
Hcallers :
c_callersc = [ ]
Hunique :
shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
Htoken :
Inregistration_tokenentry consumed
Hlocals :
invalidate_localsfr_localsc_framec c_memc = Somem_return
⊢
M.state_readycallback_world M.StoppedCoreEndRetVoid c, s data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q → ready_statewith_memc m_return, s ∧ persistsc_memfstM.machine_ofcallback_world M.StoppedCoreEndRetVoid c, s data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q c_memfstwith_memc m_return, s ∧ m_bytesc_memfstwith_memc m_return, s = m_bytesc_memfstM.machine_ofcallback_world M.StoppedCoreEndRetVoid c, s data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ∧ m_auxc_memfstwith_memc m_return, s = m_auxc_memfstM.machine_ofcallback_world M.StoppedCoreEndRetVoid c, s data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
simpl
payload :
Type
entry :
c :
s :
R.state
data :
payload
status :
Z
pending :
listregistration
consumed :
listnat
q :
m_return :
Hcallers :
c_callersc = [ ]
Hunique :
shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
Htoken :
Inregistration_tokenentry consumed
Hlocals :
invalidate_localsfr_localsc_framec c_memc = Somem_return
⊢
M.state_readycallback_world M.StoppedCoreEndRetVoid c, s data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q → ready_statewith_memc m_return, s ∧ persistsc_memc m_return ∧ m_bytesm_return = m_bytesc_memc ∧ m_auxm_return = m_auxc_memc
intros Hr
payload :
Type
entry :
c :
s :
R.state
data :
payload
status :
Z
pending :
listregistration
consumed :
listnat
q :
m_return :
Hcallers :
c_callersc = [ ]
Hunique :
shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
Htoken :
Inregistration_tokenentry consumed
Hlocals :
invalidate_localsfr_localsc_framec c_memc = Somem_return
Hr :
M.state_readycallback_world M.StoppedCoreEndRetVoid c, s data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
pose proof invalidate_locals_kept_ _ _ Hlocals as Hkept
payload :
Type
entry :
c :
s :
R.state
data :
payload
status :
Z
pending :
listregistration
consumed :
listnat
q :
m_return :
Hcallers :
c_callersc = [ ]
Hunique :
shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
Htoken :
Inregistration_tokenentry consumed
Hlocals :
invalidate_localsfr_localsc_framec c_memc = Somem_return
Hr :
M.state_readycallback_world M.StoppedCoreEndRetVoid c, s data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
split ; eapply R.ready_kept ; eauto |
payload :
Type
entry :
c :
s :
R.state
data :
payload
status :
Z
pending :
listregistration
consumed :
listnat
q :
m_return :
Hcallers :
c_callersc = [ ]
Hunique :
shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
Htoken :
Inregistration_tokenentry consumed
Hlocals :
invalidate_localsfr_localsc_framec c_memc = Somem_return
Hr :
M.state_readycallback_world M.StoppedCoreEndRetVoid c, s data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
split
2 openpayload :
Type
entry :
c :
s :
R.state
data :
payload
status :
Z
pending :
listregistration
consumed :
listnat
q :
m_return :
Hcallers :
c_callersc = [ ]
Hunique :
shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
Htoken :
Inregistration_tokenentry consumed
Hlocals :
invalidate_localsfr_localsc_framec c_memc = Somem_return
Hr :
M.state_readycallback_world M.StoppedCoreEndRetVoid c, s data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
focused goal
payload :
Type
entry :
c :
s :
R.state
data :
payload
status :
Z
pending :
listregistration
consumed :
listnat
q :
m_return :
Hcallers :
c_callersc = [ ]
Hunique :
shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
Htoken :
Inregistration_tokenentry consumed
Hlocals :
invalidate_localsfr_localsc_framec c_memc = Somem_return
Hr :
M.state_readycallback_world M.StoppedCoreEndRetVoid c, s data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
–eapply kept_ids_persists ; exact Hkept |
2 openpayload :
Type
entry :
c :
s :
R.state
data :
payload
status :
Z
pending :
listregistration
consumed :
listnat
q :
m_return :
Hcallers :
c_callersc = [ ]
Hunique :
shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
Htoken :
Inregistration_tokenentry consumed
Hlocals :
invalidate_localsfr_localsc_framec c_memc = Somem_return
Hr :
M.state_readycallback_world M.StoppedCoreEndRetVoid c, s data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
deferred goal
payload :
Type
entry :
c :
s :
R.state
data :
payload
status :
Z
pending :
listregistration
consumed :
listnat
q :
m_return :
Hcallers :
c_callersc = [ ]
Hunique :
shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
Htoken :
Inregistration_tokenentry consumed
Hlocals :
invalidate_localsfr_localsc_framec c_memc = Somem_return
Hr :
M.state_readycallback_world M.StoppedCoreEndRetVoid c, s data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
eapply invalidate_locals_ids ; eauto
deferred goal
payload :
Type
entry :
c :
s :
R.state
data :
payload
status :
Z
pending :
listregistration
consumed :
listnat
q :
m_return :
Hcallers :
c_callersc = [ ]
Hunique :
shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
Htoken :
Inregistration_tokenentry consumed
Hlocals :
invalidate_localsfr_localsc_framec c_memc = Somem_return
Hr :
M.state_readycallback_world M.StoppedCoreEndRetVoid c, s data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
–eapply callback_locals_contents ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros entry st ms′ w′ H
destruct H as c s data status pending consumed q m_return Hcallers Hunique Htoken Hlocals
simpl
intros Hr
pose proof invalidate_locals_kept_ _ _ Hlocals as Hkept
split ; eapply R.ready_kept ; eauto |
split
–eapply kept_ids_persists ; exact Hkept |
eapply invalidate_locals_ids ; eauto
–eapply callback_locals_contents ; eauto
Existing stopped outcomes cannot silently become returned callbacks.
Explore proof 3 tactics
Initial goal
payload :
Type
⊢
∀entry : registration why : ending ms : M.P.I.RM.mstate w : callback_world ms′ : mstate w′ : callback_world, callback_returnentry M.Stoppedwhy ms w ms′ w′ → why = CoreEndRetVoid
intros
inversion H
payload :
Type
entry :
why :
ms :
ms′ :
w′ :
H :
callback_returnentry M.Stoppedwhy ms w ms′ w′
c :
s :
R.state
data :
payload
status :
Z
pending :
listregistration
consumed :
listnat
q :
m_return :
H3 :
c_callersc = [ ]
H4 :
shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
H7 :
Inregistration_tokenentry consumed
H8 :
invalidate_localsfr_localsc_framec c_memc = Somem_return
H1 :
c, s = ms
H2 :
data, shutdown_at ≔ InCallbackentry; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q = w
H5 :
with_memc m_return, s = ms′
H6 :
data, shutdown_at ≔ Handlers; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q = w′
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
inversion H
reflexivity
A completed ordinary run followed by local teardown preserves readiness and every starting identity, with no reset of the runtime or fuel.
∀ registry ge start trace stopped entry ms′ w′
ge_freege = R.free
M.runregistry ge start trace stopped
callback_returnentry stopped ms′ w′
M.state_ready_ start
ready_statems′ ∧ persistsc_memfstM.machine_of_ start c_memfstms′
Explore proof 5 tactics
Initial goal
payload :
Type
⊢
∀registry : name → optioncontractcallback_world ge : genv start : M.statecallback_world trace : listevent stopped : M.statecallback_world entry : registration ms′ : mstate w′ : callback_world, ge_freege = R.free → M.runregistry ge start trace stopped → callback_returnentry stopped ms′ w′ → M.state_readycallback_world start → ready_statems′ ∧ persistsc_memfstM.machine_ofcallback_world start c_memfstms′
intros registry ge start trace stopped entry ms′ w′ Hfree Hrun Hreturn Hr
payload :
Type
registry :
name → optioncontractcallback_world
ge :
start :
M.statecallback_world
trace :
listevent
stopped :
M.statecallback_world
entry :
ms′ :
w′ :
Hfree :
ge_freege = R.free
Hrun :
M.runregistry ge start trace stopped
Hreturn :
callback_returnentry stopped ms′ w′
Hr :
M.state_readycallback_world start
⊢
ready_statems′ ∧ persistsc_memfstM.machine_ofcallback_world start c_memfstms′
destruct callback_prefix_preserve_ _ _ _ _ Hfree Hrun Hr as Hr1 Hp1
payload :
Type
registry :
name → optioncontractcallback_world
ge :
start :
M.statecallback_world
trace :
listevent
stopped :
M.statecallback_world
entry :
ms′ :
w′ :
Hfree :
ge_freege = R.free
Hrun :
M.runregistry ge start trace stopped
Hreturn :
callback_returnentry stopped ms′ w′
Hr :
M.state_readycallback_world start
Hr1 :
M.state_readycallback_world stopped
Hp1 :
persistsc_memfstM.machine_ofcallback_world start c_memfstM.machine_ofcallback_world stopped
⊢
ready_statems′ ∧ persistsc_memfstM.machine_ofcallback_world start c_memfstms′
destruct callback_return_preserve_ _ _ _ Hreturn Hr1 as Hr2 & Hp2 & _
payload :
Type
registry :
name → optioncontractcallback_world
ge :
start :
M.statecallback_world
trace :
listevent
stopped :
M.statecallback_world
entry :
ms′ :
w′ :
Hfree :
ge_freege = R.free
Hrun :
M.runregistry ge start trace stopped
Hreturn :
callback_returnentry stopped ms′ w′
Hr :
M.state_readycallback_world start
Hr1 :
M.state_readycallback_world stopped
Hp1 :
persistsc_memfstM.machine_ofcallback_world start c_memfstM.machine_ofcallback_world stopped
Hr2 :
ready_statems′
Hp2 :
persistsc_memfstM.machine_ofcallback_world stopped c_memfstms′
⊢
ready_statems′ ∧ persistsc_memfstM.machine_ofcallback_world start c_memfstms′
split ; exact Hr2 |
payload :
Type
registry :
name → optioncontractcallback_world
ge :
start :
M.statecallback_world
trace :
listevent
stopped :
M.statecallback_world
entry :
ms′ :
w′ :
Hfree :
ge_freege = R.free
Hrun :
M.runregistry ge start trace stopped
Hreturn :
callback_returnentry stopped ms′ w′
Hr :
M.state_readycallback_world start
Hr1 :
M.state_readycallback_world stopped
Hp1 :
persistsc_memfstM.machine_ofcallback_world start c_memfstM.machine_ofcallback_world stopped
Hr2 :
ready_statems′
Hp2 :
persistsc_memfstM.machine_ofcallback_world stopped c_memfstms′
⊢
persistsc_memfstM.machine_ofcallback_world start c_memfstms′
eapply persists_trans ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros registry ge start trace stopped entry ms′ w′ Hfree Hrun Hreturn Hr
destruct callback_prefix_preserve_ _ _ _ _ Hfree Hrun Hr as Hr1 Hp1
destruct callback_return_preserve_ _ _ _ Hreturn Hr1 as Hr2 & Hp2 & _
split ; exact Hr2 |
eapply persists_trans ; eauto
Consumers accept an existing callback bridge and its exact machine inductives, rather than instantiate a generatively distinct machine.
Include Linked R
Independent execution controls, not native exit-registry memory.
Adversarial core code makes a local escape into a global, calls another ordinary function, then returns. It deliberately uses an A word as P: it is NOT claimed to pass checking or callback admission. Finalization must still invalidate its locals, not restore a live pre-return snapshot. Checked code selection is exercised separately.
mkFuncTAtom"escape" TAtom"local" RVoid [ ] mkBlockTAtom"entry" [ ] LocalAllocTAtom"local" 8; LetTAtom"p" A CheckLocalTAtom"local" 0 1 Read 1 [ ]; LetTAtom"dst" A Check0 8 Write 8 GlobalTAtom"sink"; RawStorePointer0 TmpTAtom"p" TmpTAtom"dst" AuxEnsure; LowerBarrier; RootedReload; LowerWrite; AddressWrite; CallCVoid GlobalTAtom"helper" [ ] JRetVoid
A genuine nested call, with its own enter and return steps. Its harmless null-pointer flight makes the separate module checked-stage.
The handwritten symbol map supplies callable addresses and a writable global cell. Checking code is separate from that memory image.
IFuncescape_function; IFuncescape_helper; IDataTAtom"sink" LLocal 8 Zero8
All three bindings are deliberately independent of the allocator.
The writable global cell initially stores canonical null.
Registration instances, not callback names, determine consumption.
The current world already contains a consumed active token and an older pending handler. Payload and signed status must survive return.
19%nat, mkShutdownInCallbackescape_registration −257 exit_first 7%nat stdout_initial
Entry retains the shared memory and an explicit finite fuel budget.
mkConfigmkFrameescape_function [ ] TAtom"local", None None EnterTAtom"entry" None [ ] escape_memory 23
The actual allocation and pointer-store endpoint, before return.
store_bytesstore_auxallocatedescape_memory local_req8 4294967296 2048 Obj4294967296 2048 8 4294967296
Parent entry and helper entry each consumed one unit of fuel.
This independently named memory is NOT the stopped observation snapshot.
mkMemm_bytesescape_written mkRegion4294967296 4294967296 Stack Freed; mkRegion2048 2056 GlobalData Live m_auxescape_written
A separately checked handler makes address rejection nonvacuous.
mkGenvIFuncescape_helper TAtom"helper", mkPtr1040 FnTAtom"helper" InterpRuntime.free
Cxa's unused extras go through generic conversion before call_frame in a separately checked module; they do not add parameters to the public void(void) handler. The adversarial escape code is excluded.
Explore proof 5 tactics
Initial goal
⊢
∀status : Z, callback_codevoid_ge CxaSlot8 TAtom"helper" ptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" ptr_addr ≔ 0; ptr_cap ≔ CNone ptr_addr ≔ 0; ptr_cap ≔ CNone registration_token ≔ 8; registration_callback ≔ CxaExitTAtom"helper" WPtrptr_addr ≔ 0; ptr_cap ≔ CNone status fr_fn ≔ escape_helper; fr_env ≔ [ ]; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"entry" None
intros status
status :
Z
⊢
callback_codevoid_ge CxaSlot8 TAtom"helper" ptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" ptr_addr ≔ 0; ptr_cap ≔ CNone ptr_addr ≔ 0; ptr_cap ≔ CNone registration_token ≔ 8; registration_callback ≔ CxaExitTAtom"helper" WPtrptr_addr ≔ 0; ptr_cap ≔ CNone status fr_fn ≔ escape_helper; fr_env ≔ [ ]; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"entry" None
split ; reflexivity |
status :
Z
⊢
checked_modulege_modulevoid_ge ∧ ∃symbol : name function : ptr f : func converted : listword, callback_targetCxaSlot8 TAtom"helper" ptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" ptr_addr ≔ 0; ptr_cap ≔ CNone ptr_addr ≔ 0; ptr_cap ≔ CNone = Somesymbol, function ∧ ptr_capfunction = Fnsymbol ∧ function_check_resvoid_ge function = Someok ∧ find_fnvoid_ge symbol = SomeDefinedf ∧ fn_retf = RVoid ∧ variadic_funcf = false ∧ indirect_call_convf CVoid callback_argsCxaSlot8 TAtom"helper" ptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" ptr_addr ≔ 0; ptr_cap ≔ CNone ptr_addr ≔ 0; ptr_cap ≔ CNone callback_wordsCxaSlot8 TAtom"helper" ptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" ptr_addr ≔ 0; ptr_cap ≔ CNone ptr_addr ≔ 0; ptr_cap ≔ CNone status = SomeConvertedconverted None ∧ call_framef converted = Somefr_fn ≔ escape_helper; fr_env ≔ [ ]; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"entry" None
split ; vm_compute ; auto |
status :
Z
⊢
∃symbol : name function : ptr f : func converted : listword, callback_targetCxaSlot8 TAtom"helper" ptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" ptr_addr ≔ 0; ptr_cap ≔ CNone ptr_addr ≔ 0; ptr_cap ≔ CNone = Somesymbol, function ∧ ptr_capfunction = Fnsymbol ∧ function_check_resvoid_ge function = Someok ∧ find_fnvoid_ge symbol = SomeDefinedf ∧ fn_retf = RVoid ∧ variadic_funcf = false ∧ indirect_call_convf CVoid callback_argsCxaSlot8 TAtom"helper" ptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" ptr_addr ≔ 0; ptr_cap ≔ CNone ptr_addr ≔ 0; ptr_cap ≔ CNone callback_wordsCxaSlot8 TAtom"helper" ptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" ptr_addr ≔ 0; ptr_cap ≔ CNone ptr_addr ≔ 0; ptr_cap ≔ CNone status = SomeConvertedconverted None ∧ call_framef converted = Somefr_fn ≔ escape_helper; fr_env ≔ [ ]; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"entry" None
exists TAtom"helper", mkPtr1040 FnTAtom"helper", escape_helper, [ ]
status :
Z
⊢
callback_targetCxaSlot8 TAtom"helper" ptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" ptr_addr ≔ 0; ptr_cap ≔ CNone ptr_addr ≔ 0; ptr_cap ≔ CNone = SomeTAtom"helper", ptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" ∧ ptr_capptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" = FnTAtom"helper" ∧ function_check_resvoid_ge ptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" = Someok ∧ find_fnvoid_ge TAtom"helper" = SomeDefinedescape_helper ∧ fn_retescape_helper = RVoid ∧ variadic_funcescape_helper = false ∧ indirect_call_convescape_helper CVoid callback_argsCxaSlot8 TAtom"helper" ptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" ptr_addr ≔ 0; ptr_cap ≔ CNone ptr_addr ≔ 0; ptr_cap ≔ CNone callback_wordsCxaSlot8 TAtom"helper" ptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" ptr_addr ≔ 0; ptr_cap ≔ CNone ptr_addr ≔ 0; ptr_cap ≔ CNone status = SomeConverted[ ] None ∧ call_frameescape_helper [ ] = Somefr_fn ≔ escape_helper; fr_env ≔ [ ]; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"entry" None
repeat split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros status
split ; reflexivity |
split ; vm_compute ; auto |
exists TAtom"helper", mkPtr1040 FnTAtom"helper", escape_helper, [ ]
repeat split ; reflexivity
The adversarial entry-to-return core run really allocates the local and stores its pointer. No opaque callback-success action is used; no validation or native reachability is claimed for this control.
284Example escape_runs: M.runλ_ ⇒ None escape_ge M.Runningescape_start, InterpRuntime.start escape_world [ ] M.StoppedCoreEndRetVoid escape_terminal, 4294967328 escape_world
Proof 9 steps Qed
eapply M.run_cons with trace := [ ] tail := [ ] ; apply M.step_core ; eapply RM.mstep_next ; reflexivity |
eapply M.run_cons with trace := [ ] tail := [ ] ; apply M.step_core ; eapply RM.mstep_alloc with base := 4294967296 q := local_req8 ; reflexivity | simpl ; lia | reflexivity |
Normalize each endpoint, but keep symbolic byte/aux functions folded.
do 7 cbv - [ store_bytes store_aux ] ; eapply M.run_cons with trace := [ ] tail := [ ] ; apply M.step_core ; eapply RM.mstep_next ; cbv - [ store_bytes store_aux ] ; reflexivity |
eapply M.run_cons with trace := [ ] tail := [ ]
–constructor
The escaped identity is live in the stopped snapshot, freed at the reconstructed endpoint, and still present in the global's aux slot.
307Example escape_lifetime_boundary: object_region4294967296 m_regionsc_memescape_terminal = SomemkRegion4294967296 4294967304 Stack Live ∧ invalidate_localsfr_localsc_frameescape_terminal c_memescape_terminal = Someescape_returned ∧ pointer_slotescape_returned 2048 mkPtr4294967296 Obj4294967296 ∧ object_region4294967296 m_regionsescape_returned = SomemkRegion4294967296 4294967296 Stack Freed ∧ access_resescape_returned 4294967296 Obj4294967296 1 Read 1 = SomeRTrapOutOfBounds
Explore proof 1 tactics
Initial goal
⊢
object_region4294967296 m_regionsc_memescape_terminal = Somer_base ≔ 4294967296; r_end ≔ 4294967304; r_kind ≔ Stack; r_life ≔ Live ∧ invalidate_localsfr_localsc_frameescape_terminal c_memescape_terminal = Someescape_returned ∧ pointer_slotescape_returned 2048 ptr_addr ≔ 4294967296; ptr_cap ≔ Obj4294967296 ∧ object_region4294967296 m_regionsescape_returned = Somer_base ≔ 4294967296; r_end ≔ 4294967296; r_kind ≔ Stack; r_life ≔ Freed ∧ access_resescape_returned 4294967296 Obj4294967296 1 Read 1 = SomeRTrapOutOfBounds
repeat split ; try reflexivity ; simpl ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
repeat split ; try reflexivity ; simpl ; lia
Normal finalization resumes Handlers with the current pending list, status, payload, consumed token and remaining fuel, not the entry frame.
319Example escape_resumes: L.callback_returnnat escape_registration M.StoppedCoreEndRetVoid escape_terminal, 4294967328 escape_world RM.with_memescape_terminal escape_returned, 4294967328 19%nat, mkShutdownHandlers −257 exit_first 7%nat stdout_initial
Explore proof 4 tactics
Initial goal
⊢
L.callback_returnnat escape_registration M.StoppedCoreEndRetVoid escape_terminal, 4294967328 escape_world RM.with_memescape_terminal escape_returned, 4294967328 19%nat, shutdown_at ≔ Handlers; shutdown_status ≔ −257; shutdown_pending ≔ exit_first; shutdown_consumed ≔ 7%nat; shutdown_stdout ≔ stdout_initial
constructor ; reflexivity | | left ; reflexivity | reflexivity
unfold shutdown_unique
⊢
NoDupshutdown_consumedshutdown_at ≔ InCallbackescape_registration; shutdown_status ≔ −257; shutdown_pending ≔ exit_first; shutdown_consumed ≔ 7%nat; shutdown_stdout ≔ stdout_initial ++ mapregistration_token shutdown_pendingshutdown_at ≔ InCallbackescape_registration; shutdown_status ≔ −257; shutdown_pending ≔ exit_first; shutdown_consumed ≔ 7%nat; shutdown_stdout ≔ stdout_initial
simpl
⊢
NoDup7%nat; 1%nat
repeat constructor ; simpl ; intuition discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
constructor ; reflexivity | | left ; reflexivity | reflexivity
unfold shutdown_unique
simpl
repeat constructor ; simpl ; intuition discriminate
Correct Fn authority with a wrong callable address cannot be admitted.
Explore proof 4 tactics
Initial goal
⊢
function_check_resvoid_ge ptr_addr ≔ 1041; ptr_cap ≔ FnTAtom"helper" = SomeRTrapNotAFunction ∧ ∀fr : frame, ¬callback_codevoid_ge CxaSlot8 TAtom"helper" ptr_addr ≔ 1041; ptr_cap ≔ FnTAtom"helper" ptr_addr ≔ 0; ptr_cap ≔ CNone ptr_addr ≔ 0; ptr_cap ≔ CNone registration_token ≔ 8; registration_callback ≔ CxaExitTAtom"helper" WPtrptr_addr ≔ 0; ptr_cap ≔ CNone −257 fr
split ; reflexivity |
intros fr _ & _ & symbol & function & f & converted & Htarget & _ & Hcheck & _
injection Htarget as ← ←
discriminate Hcheck
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; reflexivity |
intros fr _ & _ & symbol & function & f & converted & Htarget & _ & Hcheck & _
injection Htarget as ← ←
discriminate Hcheck
Native flavor order and signed status differ from the host wait byte.
341Example callback_native_words: callback_wordsAtSlot8 TAtom"helper" mkPtr1040 FnTAtom"helper" −257 = [ ] ∧ callback_wordsOnSlot8 TAtom"helper" mkPtr1040 FnTAtom"helper" mkPtr2049 Ro2048 −257 = WInt4294967039; WPtrmkPtr2049 Ro2048 ∧ callback_wordsCxaSlot8 TAtom"helper" mkPtr1040 FnTAtom"helper" mkPtr2049 Ro2048 mkPtr4096 Obj4096 −257 = WPtrmkPtr2049 Ro2048; WInt4294967039
Explore proof 1 tactics
Initial goal
⊢
callback_wordsAtSlot8 TAtom"helper" ptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" −257 = [ ] ∧ callback_wordsOnSlot8 TAtom"helper" ptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" ptr_addr ≔ 2049; ptr_cap ≔ Ro2048 −257 = WInt4294967039; WPtrptr_addr ≔ 2049; ptr_cap ≔ Ro2048 ∧ callback_wordsCxaSlot8 TAtom"helper" ptr_addr ≔ 1040; ptr_cap ≔ FnTAtom"helper" ptr_addr ≔ 2049; ptr_cap ≔ Ro2048 ptr_addr ≔ 4096; ptr_cap ≔ Obj4096 −257 = WPtrptr_addr ≔ 2049; ptr_cap ≔ Ro2048; WInt4294967039
repeat split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
repeat split ; reflexivity
Already completed external exits and fuel/resource endings do not acquire a normal callback return edge.
352Example callback_terminal_controls: ∀ms′ w′, ¬L.callback_returnnat escape_registration M.StoppedExternalExit9 escape_terminal, 4294967328 escape_world ms′ w′ ∧ ¬L.callback_returnnat escape_registration M.StoppedCoreEndOutOfFuel escape_terminal, 4294967328 escape_world ms′ w′
Explore proof 2 tactics
Initial goal
⊢
∀ms′ : L.RM.mstate w′ : L.callback_worldnat, ¬L.callback_returnnat escape_registration M.StoppedExternalExit9 escape_terminal, 4294967328 escape_world ms′ w′ ∧ ¬L.callback_returnnat escape_registration M.StoppedCoreEndOutOfFuel escape_terminal, 4294967328 escape_world ms′ w′
intros
ms′ :
w′ :
⊢
¬L.callback_returnnat escape_registration M.StoppedExternalExit9 escape_terminal, 4294967328 escape_world ms′ w′ ∧ ¬L.callback_returnnat escape_registration M.StoppedCoreEndOutOfFuel escape_terminal, 4294967328 escape_world ms′ w′
split ; intro H ; inversion H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
split ; intro H ; inversion H