rocq/theories/Ending.v
Exit requests precede terminal external dispatch. This additive bridge shares Linked's current payload and authoritative shutdown inventory. Native registration, administrative effects and host completion remain explicit trusted obligations; no native coverage or termination follows.
From Stdlib Require Import String ZArith List Bool Lia
From Nanofil Require Import Term Maps Syntax Values Memory Runtime Ops Semantics Machine Identity ExternalCalls Startup Stdio Shutdown ExitMemory ExternalMachine Linked
Import ListNotations
Open Scope Z_scope
Open Scope list_scope
Only these unresolved direct symbols are plain exit requests. An already stopped ExternalExit is never decoded as another request.
A C int argument has W class and a nonreturning void call site.
Initial and nested soft requests retain the CURRENT inventory and stdout. Initial application execution uses Tls as its dormant phase. No soft request reopens closed cleanup. Hard exit never flushes.
∀ status old pending consumed q
exit_requestSoftExit status mkShutdownTls old pending consumed q mkShutdownTls status pending consumed q
request_initial∀ status old active pending consumed q
exit_requestSoftExit status mkShutdownInCallbackactive old pending consumed q mkShutdownTls status pending consumed q
request_recursive∀ status sh
∀kind, shutdown_atsh ≠ HandedOffkind
request_hard
exit_requestHardExit status sh mkShutdownHandedOffHardExit status shutdown_pendingsh shutdown_consumedsh shutdown_stdoutsh
Requests preserve all registration instances and output obligations.
∀ kind status sh sh′
exit_requestkind status sh sh′
shutdown_pendingsh′ = shutdown_pendingsh ∧ shutdown_consumedsh′ = shutdown_consumedsh ∧ shutdown_stdoutsh′ = shutdown_stdoutsh ∧ shutdown_statussh′ = status
Explore proof 2 tactics
Initial goal
⊢
∀kind : handoff_kind status : Z sh sh′ : shutdown_state, exit_requestkind status sh sh′ → shutdown_pendingsh′ = shutdown_pendingsh ∧ shutdown_consumedsh′ = shutdown_consumedsh ∧ shutdown_stdoutsh′ = shutdown_stdoutsh ∧ shutdown_statussh′ = status
intros kind status sh sh′ H
⊢
shutdown_pendingsh′ = shutdown_pendingsh ∧ shutdown_consumedsh′ = shutdown_consumedsh ∧ shutdown_stdoutsh′ = shutdown_stdoutsh ∧ shutdown_statussh′ = status
destruct H ; repeat split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros kind status sh sh′ H
destruct H ; repeat split ; reflexivity
Uniqueness survives recursive and hard exit without a new inventory.
Explore proof 2 tactics
Initial goal
⊢
∀kind : handoff_kind status : Z sh sh′ : shutdown_state, exit_requestkind status sh sh′ → shutdown_uniquesh → shutdown_uniquesh′
intros kind status sh sh′ H
⊢
shutdown_uniquesh → shutdown_uniquesh′
destruct H ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros kind status sh sh′ H
destruct H ; auto
Successful registration is permitted before exit or inside a callback, never after cleanup. Tokens are fresh even for repeated function names.
∀ status pending consumed q
¬Inregistration_tokenentry consumed ++ mapregistration_token pending
registration_before_exit
registration_updateentry mkShutdownTls status pending consumed q mkShutdownTls status entry :: pending consumed q
∀ status active pending consumed q
¬Inregistration_tokenentry consumed ++ mapregistration_token pending
registration_in_callback
registration_updateentry mkShutdownInCallbackactive status pending consumed q mkShutdownInCallbackactive status entry :: pending consumed q
Registration does not alter the active status, consumed history or stdout.
Explore proof 2 tactics
Initial goal
⊢
∀entry : registration sh sh′ : shutdown_state, registration_updateentry sh sh′ → shutdown_uniquesh → shutdown_uniquesh′
intros entry sh sh′ H Hu
⊢
destruct H ; unfold shutdown_unique in * ; simpl in * ; apply shutdown_unique_insert ; assumption
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros entry sh sh′ H Hu
destruct H ; unfold shutdown_unique in * ; simpl in * ; apply shutdown_unique_insert ; assumption
This pin implements atexit with a cxa slot, null argument and null DSO. Physical representation and callback semantic admission are independent.
∃token symbol, entry = mkRegistrationtoken CxaExitsymbol WPtrmkPtr0 CNone ∧ ptr_capfunction = Fnsymbol ∧ InCxaSlottoken symbol function mkPtr0 CNone mkPtr0 CNone flat_mapblock_slots blocks ∧ exit_registry_memorym head blocks
Even resource/unfinished prefixes retain the current inventory or add exactly one freshly installed instance. Reserved physical slots do not yet add a logical callback. No completion result is asserted here.
86Definition atexit_progresspayload : Type represented : mem → payload → ptr → listexit_block → Prop xs w : payload × shutdown_state m′ w′ : payload × shutdown_state : Prop ≔
∃head blocks, representedm′ fstw′ head blocks ∧ exit_registry_memorym′ head blocks ∧ exit_registry_pendingblocks = shutdown_pendingsndw′ ∧ sndw′ = sndw ∨ ∃function entry, xs = WPtrfunction ∧ atexit_installedm′ head blocks function entry ∧ registration_updateentry sndw sndw′
The native contract supplies effects, allocation and private registry authority. This overlay supplies the exact public API and couples its successful result to physical installation and the single inventory. Callback admission must be supplied independently at entry.
100Definition atexit_contractpayload : Type ge : genv native : contractpayload × shutdown_state represented : mem → payload → ptr → listexit_block → Prop : contractpayload × shutdown_state ≔
mkContract_ RClassW λr args ⇒ r = CVoid ∨ ∃d, r = CResultd W ∧ ∃value, args = ArgP value ∧ contract_abinative r args λxs m w ⇒ contract_prenative xs m w ∧ shutdown_uniquesndw ∧ atexit_progressrepresented xs w m w ∧ ∃function, xs = WPtrfunction ∧ function_check_resge function = Someok contract_sourcesnative contract_writesnative contract_releasesnative contract_requestsnative λxs m w born trace m′ w′ ⇒ contract_prefixnative xs m w born trace m′ w′ ∧ trace = [ ] ∧ atexit_progressrepresented xs w m′ w′ λxs m w born trace ending m′ w′ ⇒ contract_postnative xs m w born trace ending m′ w′ ∧ ∃function result, xs = WPtrfunction ∧ ending = CallReturnWIntresult ∧ trace = [ ] ∧ result = 0 ∧ ∃head blocks entry, representedm′ fstw′ head blocks ∧ atexit_installedm′ head blocks function entry ∧ exit_registry_pendingblocks = shutdown_pendingsndw′ ∧ registration_updateentry sndw sndw′ ∨ result = 2 ^ 32 − 1 ∧ sndw′ = sndw contract_resourcenative contract_panicsnative
Only administrative actions may be delegated wholesale. Callback pop, execution and return use the separate, memory-backed rules below.
match action with
_
⇒
False
Requests and callbacks extend the labelled machine, never Machine.v.
One payload and one authoritative lifecycle, as in Linked.
Running application/callback code, a suspended exit loop, and completed host termination retain exact machine snapshots. Stopped remains stopped.
| | | Executing | ||
| | | Draining | ||
| | | Partial | ||
| | | Finished |
Every mode retains its exact machine snapshot, including partial leaves.
match st with
Readiness does not assert contract admission, progress or native coverage.
Administrative libc effects use the existing capability/effects boundary. Readiness/representation at both endpoints is an explicit obligation, not a native satisfaction theorem. A synthetic CallReturn marks a completed internal cutpoint, not a native return from host handoff. registry_rep identifies the authoritative physical chain in the payload; use this same projection as atexit_contract's represented argument.
| ending_rep | ||
| registry_rep | : mem → payload → ptr → listexit_block → Prop | |
| registry_owned | : payload → listZ | |
| action_spec | ||
| action_args | : shutdown_action → listarg | |
| action_values | : shutdown_action → listword | |
| host_complete |
The selected request syntax, evaluated independently of any invocation.
external_sitege c site ∧ exit_symbolsite_namesite = Somekind ∧ exit_abisite_resultsite site_argssite ∧ map_optionarg_xge fr_envc_framec site_argssite = SomeWIntbits
Admission is independent of successful execution. Reached-call proofs must establish it again after safepoints; its failure is visible below.
ending_repb s c_memc w ∧ shutdown_uniquesndw ∧ ∃bits sh′, request_sitege c site kind bits ∧ exit_requestkind main_statusbits sndw sh′
A single dispatcher: reserved names (e.g. error) are handled by a further explicit bridge, not ordinary terminal external dispatch. Safepoints at intercepted calls still run and recheck admission later.
197Inductive stepregistry : name → optioncontractworld ge reserved : name → bool b : boundary admitted : registration → R.state → mem → world → Prop : state → listevent → state → Prop ≔
∀ st trace st′
∀c s w site, st = M.Runningc, s w → external_sitege c site → exit_symbolsite_namesite = None ∧ reservedsite_namesite = false
M.stepregistry ge st trace st′
ending_ordinary
∀ c s w site kind bits sh′
request_sitege c site kind bits
ending_repb s c_memc w
shutdown_uniquesndw
exit_requestkind main_statusbits sndw sh′
ending_request
∀ c s w site kind
ending_rejected
stepregistry ge reserved b admitted ExecutingM.Runningc, s w [ ] ExecutingM.StoppedContractViolationsite_namesite BadPrecondition c, s w
∀ c s w action trace s′ m′ w′
administrativeaction
shutdown_stepsndw action sndw′
ending_repb s c_memc w
contract_abiaction_specb action CVoid action_argsb action
contract_preaction_specb action action_valuesb action c_memc w
E.invokeaction_specb action CVoid action_argsb action action_valuesb action s c_memc w trace CallReturn[ ] s′ m′ w′
ending_repb s′ m′ w′
ending_action
stepregistry ge reserved b admitted Drainingc, s w trace DrainingRM.with_memc m′, s′ w′
∀ c s w action born trace s′ m′ w′
administrativeaction
ending_repb s c_memc w
contract_abiaction_specb action CVoid action_argsb action
contract_preaction_specb action action_valuesb action c_memc w
E.prefixaction_specb action action_valuesb action s c_memc w born trace s′ m′ w′
∀status, ¬InProcessExitstatus trace
ending_action_prefix
stepregistry ge reserved b admitted Drainingc, s w trace PartialRM.with_memc m′, s′ w′
∀ c s w action trace why s′ m′ w′
administrativeaction
ending_repb s c_memc w
E.invokeaction_specb action CVoid action_argsb action action_valuesb action s c_memc w trace CallResourcewhy s′ m′ w′
∀status, ¬InProcessExitstatus trace
ending_action_resource
∀ c s data status consumed q head p older slot rest entry fuel callback
registry_repb c_memc data head mkExitBlockp older ++ slot :: rest
exit_registry_memoryc_memc head mkExitBlockp older ++ slot :: rest
exit_pop_separatedhead p rest
exit_slot_pendingslot = entry
Forallwritable_spanc_memc exit_pop_writesp older slot
shutdown_uniquemkShutdownHandlers status exit_registry_pendingmkExitBlockp older ++ slot :: rest consumed q
L.callback_entrypayload admitted ge slot entry s exit_pop_memoryc_memc p older slot data, mkShutdownInCallbackentry status exit_registry_pendingmkExitBlockp older :: rest consumed ++ registration_tokenentry q fuel callback
fuel = c_fuelc
registry_repb exit_pop_memoryc_memc p older slot data head mkExitBlockp older :: rest
ending_pop
stepregistry ge reserved b admitted Drainingc, s data, mkShutdownHandlers status exit_registry_pendingmkExitBlockp older ++ slot :: rest consumed q [ ] ExecutingM.Runningcallback, s data, mkShutdownInCallbackentry status exit_registry_pendingmkExitBlockp older :: rest consumed ++ registration_tokenentry q
∀ c s data status consumed q head p older slot rest
registry_repb c_memc data head mkExitBlockp older ++ slot :: rest
exit_registry_memoryc_memc head mkExitBlockp older ++ slot :: rest
exit_pop_separatedhead p rest
slot = FreeSlot ∨ slot = ReservedSlot
Forallwritable_spanc_memc exit_pop_writesp older slot
registry_repb exit_pop_memoryc_memc p older slot data head mkExitBlockp older :: rest
ending_skip
stepregistry ge reserved b admitted Drainingc, s data, mkShutdownHandlers status exit_registry_pendingmkExitBlockp older ++ slot :: rest consumed q [ ] DrainingRM.with_memc exit_pop_memoryc_memc p older slot, s data, mkShutdownHandlers status exit_registry_pendingmkExitBlockp older :: rest consumed q
∀ c s data status consumed q head p rest
registry_repb c_memc data head mkExitBlockp [ ] :: rest
exit_registry_memoryc_memc head mkExitBlockp [ ] :: rest
exit_unlink_separatedhead mkExitBlockp [ ] :: rest
writable_spanc_memc mkSpanhead 8
registry_repb exit_unlink_memoryc_memc head rest data head rest
ending_unlink
stepregistry ge reserved b admitted Drainingc, s data, mkShutdownHandlers status exit_registry_pendingmkExitBlockp [ ] :: rest consumed q [ ] DrainingRM.with_memc exit_unlink_memoryc_memc head rest, s data, mkShutdownHandlers status exit_registry_pendingrest consumed q
∀ c s data sh head block rest m′
shutdown_atsh = Handlers
registry_repb c_memc data head rest
exit_block_releasableregistry_ownedb data c_memc head block rest
registry_repb m′ data head rest
ending_retire
stepregistry ge reserved b admitted Drainingc, s data, sh [ ] DrainingRM.with_memc m′, s data, sh
∀ c s data kind status pending consumed q
host_completeb s c_memc data, mkShutdownHandedOffkind status pending consumed q
ending_complete
stepregistry ge reserved b admitted Drainingc, s data, mkShutdownHandedOffkind status pending consumed q ProcessExitprocess_statusstatus Finishedc, s data, mkShutdownHandedOffkind status pending consumed q
Entry uses the actual post-pop memory, not a second chosen snapshot.
∀ admitted ge slot entry s m w fuel callback
L.callback_entrypayload admitted ge slot entry s m w fuel callback
c_memcallback = m
Explore proof 2 tactics
Initial goal
payload :
Type
⊢
∀admitted : registration → R.state → mem → L.callback_worldpayload → Prop ge : genv slot : exit_slot entry : registration s : R.state m : mem w : payload × shutdown_state fuel : Z callback : config, L.callback_entrypayload admitted ge slot entry s m w fuel callback → c_memcallback = m
intros admitted ge slot entry s m w fuel callback _ & _ & _ & _ & _ & _ & fr & _ & →
payload :
Type
admitted :
registration → R.state → mem → L.callback_worldpayload → Prop
ge :
slot :
entry :
s :
m :
w :
payload × shutdown_state
fuel :
Z
fr :
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros admitted ge slot entry s m w fuel callback _ & _ & _ & _ & _ & _ & fr & _ & →
reflexivity
Every new edge preserves readiness and identities by its existing effect path or local teardown. This is structural preservation, not safety.
∀ registry ge reserved b admitted st trace st′
state_readyst′ ∧ persistsc_memfstmachine_ofst c_memfstmachine_ofst′
Proof 23 steps Qed
intros registry ge reserved b admitted st trace st′ Hfree H
destruct H ; unfold state_ready , machine_of , RM.ready_state ; simpl ; intros Hr
–split ; eapply M.step_ready | eapply M.step_persists ; eauto
{apply M.step_core
eapply RM.mstep_safepoint ; eauto
split
–split ; auto using persists_refl
–split ; auto using persists_refl
–eapply E.invoke_preserve ; eauto
–eapply E.prefix_preserve ; eauto
–eapply E.invoke_preserve ; eauto
–match goal withHentry : L.callback_entry_ _ _ _ _ _ _ _ _ _ |- _⇒rewrite callback_entry_memory_ _ _ _ _ _ _ _ _ Hentryend
exact proj2Pop.pop_preserves_ _ _ _ _ H3 Hr
–exact proj2Pop.pop_preserves_ _ _ _ _ H3 Hr
–eapply Unlink.unlink_preserves ; eauto
match goal withHregistry : exit_registry_memory_ _ _ |- _⇒exact proj1proj1proj2proj2Hregistryend
–eapply E.effects_preserve ; eauto
–destruct L.callback_return_preserve_ _ _ _ _ H Hr as Hr′ Hp _
auto
–split ; auto using persists_refl
Finite prefixes need not finish a handler or reach host completion.
Finite execution retains readiness and every starting identity.
∀ registry ge reserved b admitted st trace st′
state_readyst′ ∧ persistsc_memfstmachine_ofst c_memfstmachine_ofst′
Explore proof 7 tactics
Initial goal
payload :
Type
⊢
∀registry : name → optioncontractworld ge : genv reserved : name → bool b : boundary admitted : registration → R.state → mem → world → Prop st : state trace : listevent st′ : state, ge_freege = R.free → runregistry ge reserved b admitted st trace st′ → state_readyst → state_readyst′ ∧ persistsc_memfstmachine_ofst c_memfstmachine_ofst′
intros registry ge reserved b admitted st trace st′ Hfree H
payload :
Type
ge :
reserved :
name → bool
b :
admitted :
registration → R.state → mem → world → Prop
st :
trace :
listevent
st′ :
Hfree :
ge_freege = R.free
H :
runregistry ge reserved b admitted st trace st′
⊢
state_readyst → state_readyst′ ∧ persistsc_memfstmachine_ofst c_memfstmachine_ofst′
induction H ; intros Hr
2 openpayload :
Type
ge :
reserved :
name → bool
b :
admitted :
registration → R.state → mem → world → Prop
Hfree :
ge_freege = R.free
st :
Hr :
⊢
state_readyst ∧ persistsc_memfstmachine_ofst c_memfstmachine_ofst
focused goal
payload :
Type
ge :
reserved :
name → bool
b :
admitted :
registration → R.state → mem → world → Prop
Hfree :
ge_freege = R.free
st :
trace :
listevent
mid :
tail :
listevent
st′ :
H :
stepregistry ge reserved b admitted st trace mid
H0 :
runregistry ge reserved b admitted mid tail st′
IHrun :
state_readymid → state_readyst′ ∧ persistsc_memfstmachine_ofmid c_memfstmachine_ofst′
Hr :
⊢
state_readyst′ ∧ persistsc_memfstmachine_ofst c_memfstmachine_ofst′
–split ; auto using persists_refl
deferred goal
payload :
Type
ge :
reserved :
name → bool
b :
admitted :
registration → R.state → mem → world → Prop
Hfree :
ge_freege = R.free
st :
trace :
listevent
mid :
tail :
listevent
st′ :
H :
stepregistry ge reserved b admitted st trace mid
H0 :
runregistry ge reserved b admitted mid tail st′
IHrun :
state_readymid → state_readyst′ ∧ persistsc_memfstmachine_ofmid c_memfstmachine_ofst′
Hr :
⊢
state_readyst′ ∧ persistsc_memfstmachine_ofst c_memfstmachine_ofst′
–destruct step_preserve_ _ _ _ _ _ _ _ Hfree H Hr as Hr1 Hp1
payload :
Type
ge :
reserved :
name → bool
b :
admitted :
registration → R.state → mem → world → Prop
Hfree :
ge_freege = R.free
st :
trace :
listevent
mid :
tail :
listevent
st′ :
H :
stepregistry ge reserved b admitted st trace mid
H0 :
runregistry ge reserved b admitted mid tail st′
IHrun :
state_readymid → state_readyst′ ∧ persistsc_memfstmachine_ofmid c_memfstmachine_ofst′
Hr :
Hr1 :
state_readymid
Hp1 :
persistsc_memfstmachine_ofst c_memfstmachine_ofmid
⊢
state_readyst′ ∧ persistsc_memfstmachine_ofst c_memfstmachine_ofst′
destruct IHrunHr1 as Hr′ Hp2
payload :
Type
ge :
reserved :
name → bool
b :
admitted :
registration → R.state → mem → world → Prop
Hfree :
ge_freege = R.free
st :
trace :
listevent
mid :
tail :
listevent
st′ :
H :
stepregistry ge reserved b admitted st trace mid
H0 :
runregistry ge reserved b admitted mid tail st′
IHrun :
state_readymid → state_readyst′ ∧ persistsc_memfstmachine_ofmid c_memfstmachine_ofst′
Hr :
Hr1 :
state_readymid
Hp1 :
persistsc_memfstmachine_ofst c_memfstmachine_ofmid
Hr′ :
state_readyst′
Hp2 :
persistsc_memfstmachine_ofmid c_memfstmachine_ofst′
⊢
state_readyst′ ∧ persistsc_memfstmachine_ofst c_memfstmachine_ofst′
split ; exact Hr′ |
payload :
Type
ge :
reserved :
name → bool
b :
admitted :
registration → R.state → mem → world → Prop
Hfree :
ge_freege = R.free
st :
trace :
listevent
mid :
tail :
listevent
st′ :
H :
stepregistry ge reserved b admitted st trace mid
H0 :
runregistry ge reserved b admitted mid tail st′
IHrun :
state_readymid → state_readyst′ ∧ persistsc_memfstmachine_ofmid c_memfstmachine_ofst′
Hr :
Hr1 :
state_readymid
Hp1 :
persistsc_memfstmachine_ofst c_memfstmachine_ofmid
Hr′ :
state_readyst′
Hp2 :
persistsc_memfstmachine_ofmid c_memfstmachine_ofst′
⊢
persistsc_memfstmachine_ofst c_memfstmachine_ofst′
eapply persists_trans ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros registry ge reserved b admitted st trace st′ Hfree H
induction H ; intros Hr
–split ; auto using persists_refl
–destruct step_preserve_ _ _ _ _ _ _ _ Hfree H Hr as Hr1 Hp1
destruct IHrunHr1 as Hr′ Hp2
split ; exact Hr′ |
eapply persists_trans ; eauto
A request is silent and never takes the caller's ordinary continuation.
∀ registry ge reserved b admitted c s w site kind bits sh′
request_sitege c site kind bits
ending_repb s c_memc w
shutdown_uniquesndw
exit_requestkind main_statusbits sndw sh′
Explore proof 2 tactics
Initial goal
payload :
Type
⊢
∀registry : name → optioncontractworld ge : genv reserved : name → bool b : boundary admitted : registration → R.state → mem → world → Prop c : config s : R.state w : world site : call_site kind : handoff_kind bits : Z sh′ : shutdown_state, request_sitege c site kind bits → ending_repb s c_memc w → shutdown_uniquesndw → exit_requestkind main_statusbits sndw sh′ → stepregistry ge reserved b admitted ExecutingM.Runningc, s w [ ] Drainingc, s fstw, sh′
intros
payload :
Type
ge :
reserved :
name → bool
b :
admitted :
registration → R.state → mem → world → Prop
c :
s :
w :
site :
kind :
bits :
Z
sh′ :
H :
request_sitege c site kind bits
H0 :
ending_repb s c_memc w
H1 :
shutdown_uniquesndw
H2 :
exit_requestkind main_statusbits sndw sh′
eapply ending_request ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
eapply ending_request ; eauto
Partial cutpoints cannot resume shutdown or inherit a completed action.
Explore proof 2 tactics
Initial goal
intros registry ge reserved b admitted ms w trace st′ H
inversion H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros registry ge reserved b admitted ms w trace st′ H
inversion H
Completed external exits cannot resume a callback or request shutdown.
∀ registry ge reserved b admitted status ms w trace st′
¬stepregistry ge reserved b admitted ExecutingM.StoppedExternalExitstatus ms w trace st′
Explore proof 4 tactics
Initial goal
payload :
Type
⊢
∀registry : name → optioncontractworld ge : genv reserved : name → bool b : boundary admitted : registration → R.state → mem → world → Prop status : Z ms : M.P.I.RM.mstate w : world trace : listevent st′ : state, ¬stepregistry ge reserved b admitted ExecutingM.StoppedExternalExitstatus ms w trace st′
intros registry ge reserved b admitted status ms w trace st′ H
payload :
Type
ge :
reserved :
name → bool
b :
admitted :
registration → R.state → mem → world → Prop
status :
Z
ms :
w :
trace :
listevent
st′ :
H :
stepregistry ge reserved b admitted ExecutingM.StoppedExternalExitstatus ms w trace st′
⊢
False
inversion H ; subst
2 openpayload :
Type
ge :
reserved :
name → bool
b :
admitted :
registration → R.state → mem → world → Prop
status :
Z
ms :
w :
trace :
listevent
H :
stepregistry ge reserved b admitted ExecutingM.StoppedExternalExitstatus ms w trace Executingst'0
H1 :
∀c : config s : R.state w0 : world site : call_site, M.StoppedExternalExitstatus ms w = M.Runningc, s w0 → external_sitege c site → exit_symbolsite_namesite = None ∧ reservedsite_namesite = false
H2 :
M.stepregistry ge M.StoppedExternalExitstatus ms w trace st'0
⊢
False
focused goal
payload :
Type
ge :
reserved :
name → bool
b :
admitted :
registration → R.state → mem → world → Prop
status :
Z
ms :
w :
ms′ :
w′ :
L.callback_worldpayload
H :
stepregistry ge reserved b admitted ExecutingM.StoppedExternalExitstatus ms w [ ] Drainingms′ w′
entry :
H1 :
L.callback_returnpayload entry M.StoppedExternalExitstatus ms w ms′ w′
⊢
False
–eapply M.stopped_no_step ; eauto
deferred goal
payload :
Type
ge :
reserved :
name → bool
b :
admitted :
registration → R.state → mem → world → Prop
status :
Z
ms :
w :
ms′ :
w′ :
L.callback_worldpayload
H :
stepregistry ge reserved b admitted ExecutingM.StoppedExternalExitstatus ms w [ ] Drainingms′ w′
entry :
H1 :
L.callback_returnpayload entry M.StoppedExternalExitstatus ms w ms′ w′
⊢
False
–match goal withHreturn : L.callback_return_ _ _ _ _ |- _⇒apply L.callback_return_only_void in Hreturn ; discriminateend
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros registry ge reserved b admitted status ms w trace st′ H
inversion H ; subst
–eapply M.stopped_no_step ; eauto
–match goal withHreturn : L.callback_return_ _ _ _ _ |- _⇒apply L.callback_return_only_void in Hreturn ; discriminateend
abort is deliberately not mapped to soft exit. A whole-program safety proof must exclude every reached abort call or provide another boundary.
Explore proof 1 tactics
Initial goal
payload :
Type
⊢
exit_symbolTAtom"abort" = None
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
reflexivity
Signed status replacement retains partially outstanding output.
407Example request_nested_current: ∀q, exit_requestSoftExit −257 mkShutdownInCallbackexit_second 31 exit_added; exit_first 2%nat q mkShutdownTls −257 exit_added; exit_first 2%nat q
Explore proof 2 tactics
Initial goal
⊢
∀q : stream_state, exit_requestSoftExit −257 shutdown_at ≔ InCallbackexit_second; shutdown_status ≔ 31; shutdown_pending ≔ exit_added; exit_first; shutdown_consumed ≔ 2%nat; shutdown_stdout ≔ q shutdown_at ≔ Tls; shutdown_status ≔ −257; shutdown_pending ≔ exit_added; exit_first; shutdown_consumed ≔ 2%nat; shutdown_stdout ≔ q
intros
q :
⊢
exit_requestSoftExit −257 shutdown_at ≔ InCallbackexit_second; shutdown_status ≔ 31; shutdown_pending ≔ exit_added; exit_first; shutdown_consumed ≔ 2%nat; shutdown_stdout ≔ q shutdown_at ≔ Tls; shutdown_status ≔ −257; shutdown_pending ≔ exit_added; exit_first; shutdown_consumed ≔ 2%nat; shutdown_stdout ≔ q
constructor
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
constructor
Neither cleanup nor an already completed handoff can restart soft exit.
414Example request_closed: ∀status old pending consumed q sh′, ¬exit_requestSoftExit status mkShutdownCleanup old pending consumed q sh′ ∧ ¬exit_requestSoftExit status mkShutdownHandedOffSoftExit old pending consumed q sh′
Explore proof 2 tactics
Initial goal
⊢
∀status old : Z pending : listregistration consumed : listnat q : stream_state sh′ : shutdown_state, ¬exit_requestSoftExit status shutdown_at ≔ Cleanup; shutdown_status ≔ old; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q sh′ ∧ ¬exit_requestSoftExit status shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ old; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q sh′
intros
⊢
¬exit_requestSoftExit status shutdown_at ≔ Cleanup; shutdown_status ≔ old; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q sh′ ∧ ¬exit_requestSoftExit status shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ old; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q sh′
split ; intro H ; inversion H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
split ; intro H ; inversion H