Filnix wiki

action :

left, right :

Hl :

shutdown_stepsh action left

Hr :

shutdown_stepsh action right

⊢

left = right

inversion Hl ; subst ; inversion Hr ; subst ; try reflexivity

2 open

status :

active :

pending :

consumed :

listnat

q :

action₀ :

q′ :

Hl :

shutdown_stepshutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction₀ shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q′

q'₀ :

Hr :

H :

stream_stepq action₀ q′

H₇ :

stream_stepq action₀ q'₀

⊢

shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q′ = shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q'₀

focused goal

status :

consumed :

listnat

q :

action₀ :

q′ :

Hl :

shutdown_stepshutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction₀ shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q′

q'₀ :

Hr :

H :

∀bytes : listZ, action₀ ≠ Acceptbytes

H₀ :

stream_stepq action₀ q′

H₆ :

∀bytes : listZ, action₀ ≠ Acceptbytes

H₇ :

stream_stepq action₀ q'₀

⊢

shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q′ = shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q'₀

all: match goal withH₁ : stream_step?q ?a ?q₁ , H₂ : stream_step?q ?a ?q₂ |- _⇒assert q₁ = q₂ by eapply stream_step_target ; eauto ; subst ; reflexivityend

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros sh action left right Hl Hr

inversion Hl ; subst ; inversion Hr ; subst ; try reflexivity

all: match goal withH₁ : stream_step?q ?a ?q₁ , H₂ : stream_step?q ?a ?q₂ |- _⇒assert q₁ = q₂ by eapply stream_step_target ; eauto ; subst ; reflexivityend

A finite shutdown prefix; no rule promises eventual completion.

105Inductive shutdown_run: shutdown_state → listshutdown_action → shutdown_state → Prop ≔

∀ s

shutdown_runs [ ] s

shutdown_refl

∀ s action s₁ actions s′

shutdown_steps action s₁

shutdown_runs₁ actions s′

shutdown_next

shutdown_runs action :: actions s′

All pending and consumed registration-instance tokens are distinct.

112Definition shutdown_uniques : shutdown_state : Prop ≔

NoDupshutdown_consumeds ++ mapregistration_token shutdown_pendings

Moving a fresh registration token into the pending stack preserves uniqueness.

116Lemma shutdown_unique_insert

∀ before after : listnat token

NoDupbefore ++ after

¬Intoken before ++ after

NoDupbefore ++ token :: after

Explore proof 3 tactics

Initial goal

⊢

∀before after : listnat token : nat, NoDupbefore ++ after → ¬Intoken before ++ after → NoDupbefore ++ token :: after

intros before after token Hnd Hfresh

before, after :

listnat

token :

nat

Hnd :

NoDupbefore ++ after

Hfresh :

¬Intoken before ++ after

⊢

NoDupbefore ++ token :: after

apply Permutation_NoDupPermutation_middlebefore after token

before, after :

listnat

token :

nat

Hnd :

NoDupbefore ++ after

Hfresh :

¬Intoken before ++ after

⊢

NoDuptoken :: before ++ after

constructor ; assumption

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros before after token Hnd Hfresh

apply Permutation_NoDupPermutation_middlebefore after token

constructor ; assumption

Pop-before-call and fresh successful registration preserve instance uniqueness.

126Lemma shutdown_step_unique

∀ s action s′

shutdown_steps action s′

Explore proof 5 tactics

Initial goal

⊢

∀s : shutdown_state action : shutdown_action s′ : shutdown_state, shutdown_steps action s′ → shutdown_uniques → shutdown_uniques′

intros s action s′ H Hunique

s :

action :

s′ :

H :

shutdown_steps action s′

Hunique :

⊢

destruct H ; unfold shutdown_unique in * ; simpl in * ; auto

2 open

status :

entry :

pending :

consumed :

listnat

q :

Hunique :

NoDupconsumed ++ registration_tokenentry :: mapregistration_token pending

⊢

NoDupconsumed ++ registration_tokenentry ++ mapregistration_token pending

focused goal

status :

active, entry :

pending :

consumed :

listnat

q :

H :

¬Inregistration_tokenentry consumed ++ mapregistration_token pending

Hunique :

NoDupconsumed ++ mapregistration_token pending

⊢

NoDupconsumed ++ registration_tokenentry :: mapregistration_token pending

–rewrite <- app_assoc

2 open

status :

entry :

pending :

consumed :

listnat

q :

Hunique :

NoDupconsumed ++ registration_tokenentry :: mapregistration_token pending

⊢

NoDupconsumed ++ registration_tokenentry ++ mapregistration_token pending

deferred goal

status :

active, entry :

pending :

consumed :

listnat

q :

H :

¬Inregistration_tokenentry consumed ++ mapregistration_token pending

Hunique :

NoDupconsumed ++ mapregistration_token pending

⊢

NoDupconsumed ++ registration_tokenentry :: mapregistration_token pending

exact Hunique

deferred goal

status :

active, entry :

pending :

consumed :

listnat

q :

H :

¬Inregistration_tokenentry consumed ++ mapregistration_token pending

Hunique :

NoDupconsumed ++ mapregistration_token pending

⊢

NoDupconsumed ++ registration_tokenentry :: mapregistration_token pending

–apply shutdown_unique_insert ; assumption

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros s action s′ H Hunique

destruct H ; unfold shutdown_unique in * ; simpl in * ; auto

–rewrite <- app_assoc

exact Hunique

–apply shutdown_unique_insert ; assumption

No registration instance is invoked twice, even across recursive exit.

135Theorem shutdown_run_unique

∀ s actions s′

shutdown_runs actions s′

Explore proof 5 tactics

Initial goal

⊢

∀s : shutdown_state actions : listshutdown_action s′ : shutdown_state, shutdown_runs actions s′ → shutdown_uniques → shutdown_uniques′

intros s actions s′ H

s :

actions :

s′ :

H :

shutdown_runs actions s′

⊢

shutdown_uniques → shutdown_uniques′

induction H ; auto |

s :

action :

s₁ :

actions :

s′ :

H :

shutdown_steps action s₁

H₀ :

shutdown_runs₁ actions s′

IHshutdown_run :

shutdown_uniques₁ → shutdown_uniques′

⊢

shutdown_uniques → shutdown_uniques′

intros Hu

s :

action :

s₁ :

actions :

s′ :

H :

shutdown_steps action s₁

H₀ :

shutdown_runs₁ actions s′

IHshutdown_run :

shutdown_uniques₁ → shutdown_uniques′

Hu :

⊢

apply IHshutdown_run

s :

action :

s₁ :

actions :

s′ :

H :

shutdown_steps action s₁

H₀ :

shutdown_runs₁ actions s′

IHshutdown_run :

shutdown_uniques₁ → shutdown_uniques′

Hu :

⊢

shutdown_uniques₁

eapply shutdown_step_unique ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros s actions s′ H

induction H ; auto |

intros Hu

apply IHshutdown_run

eapply shutdown_step_unique ; eauto

Tokens invoked by one action; registering and returning invoke none.

143Definition invoked_byaction : shutdown_action : listnat ≔

match action with

InvokeCallbackentry _

⇒

registration_tokenentry

⇒

[ ]

Consumed history grows by exactly the invoked instances, in invocation order.

147Lemma shutdown_step_consumed

∀ s action s′

shutdown_steps action s′

shutdown_consumeds′ = shutdown_consumeds ++ invoked_byaction

Explore proof 2 tactics

Initial goal

⊢

∀s : shutdown_state action : shutdown_action s′ : shutdown_state, shutdown_steps action s′ → shutdown_consumeds′ = shutdown_consumeds ++ invoked_byaction

intros s action s′ H

s :

action :

s′ :

H :

shutdown_steps action s′

⊢

shutdown_consumeds′ = shutdown_consumeds ++ invoked_byaction

destruct H ; simpl ; try reflexivity ; symmetry ; apply app_nil_r

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros s action s′ H

destruct H ; simpl ; try reflexivity ; symmetry ; apply app_nil_r

The history accounts for every callback invocation in a finite run.

155Theorem shutdown_consumption

∀ s actions s′

shutdown_runs actions s′

shutdown_consumeds′ = shutdown_consumeds ++ flat_mapinvoked_by actions

Explore proof 4 tactics

Initial goal

⊢

∀s : shutdown_state actions : listshutdown_action s′ : shutdown_state, shutdown_runs actions s′ → shutdown_consumeds′ = shutdown_consumeds ++ flat_mapinvoked_by actions

intros s actions s′ H

s :

actions :

s′ :

H :

shutdown_runs actions s′

⊢

shutdown_consumeds′ = shutdown_consumeds ++ flat_mapinvoked_by actions

induction H ; simpl ; symmetry ; apply app_nil_r |

s :

action :

s₁ :

actions :

s′ :

H :

shutdown_steps action s₁

H₀ :

shutdown_runs₁ actions s′

IHshutdown_run :

shutdown_consumeds′ = shutdown_consumeds₁ ++ flat_mapinvoked_by actions

⊢

shutdown_consumeds′ = shutdown_consumeds ++ invoked_byaction ++ flat_mapinvoked_by actions

rewrite IHshutdown_run , shutdown_step_consumed_ _ _ H , app_assoc

s :

action :

s₁ :

actions :

s′ :

H :

shutdown_steps action s₁

H₀ :

shutdown_runs₁ actions s′

IHshutdown_run :

shutdown_consumeds′ = shutdown_consumeds₁ ++ flat_mapinvoked_by actions

⊢

shutdown_consumeds ++ invoked_byaction ++ flat_mapinvoked_by actions = shutdown_consumeds ++ invoked_byaction ++ flat_mapinvoked_by actions

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros s actions s′ H

induction H ; simpl ; symmetry ; apply app_nil_r |

rewrite IHshutdown_run , shutdown_step_consumed_ _ _ H , app_assoc

reflexivity

Every invoked token occurs once in the trace, not merely in final pending state.

164Theorem shutdown_invocations_unique

∀ s actions s′

shutdown_runs actions s′

NoDupflat_mapinvoked_by actions

Explore proof 7 tactics

Initial goal

⊢

∀s : shutdown_state actions : listshutdown_action s′ : shutdown_state, shutdown_runs actions s′ → shutdown_uniques → NoDupflat_mapinvoked_by actions

intros s actions s′ H Hu

s :

actions :

s′ :

H :

shutdown_runs actions s′

Hu :

⊢

NoDupflat_mapinvoked_by actions

pose proof shutdown_run_unique_ _ _ H Hu as Hfinal

s :

actions :

s′ :

H :

shutdown_runs actions s′

Hu :

Hfinal :

⊢

NoDupflat_mapinvoked_by actions

unfold shutdown_unique in Hfinal

s :

actions :

s′ :

H :

shutdown_runs actions s′

Hu :

Hfinal :

NoDupshutdown_consumeds′ ++ mapregistration_token shutdown_pendings′

⊢

NoDupflat_mapinvoked_by actions

apply NoDup_app_remove_r in Hfinal

s :

actions :

s′ :

H :

shutdown_runs actions s′

Hu :

Hfinal :

NoDupshutdown_consumeds′

⊢

NoDupflat_mapinvoked_by actions

rewrite shutdown_consumption_ _ _ H in Hfinal

s :

actions :

s′ :

H :

shutdown_runs actions s′

Hu :

Hfinal :

NoDupshutdown_consumeds ++ flat_mapinvoked_by actions

⊢

NoDupflat_mapinvoked_by actions

apply NoDup_app_remove_l in Hfinal

s :

actions :

s′ :

H :

shutdown_runs actions s′

Hu :

Hfinal :

NoDupflat_mapinvoked_by actions

⊢

NoDupflat_mapinvoked_by actions

exact Hfinal

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros s actions s′ H Hu

pose proof shutdown_run_unique_ _ _ H Hu as Hfinal

unfold shutdown_unique in Hfinal

apply NoDup_app_remove_r in Hfinal

rewrite shutdown_consumption_ _ _ H in Hfinal

apply NoDup_app_remove_l in Hfinal

exact Hfinal

Recursive exit and _exit install their own signed status, not the old exit's.

177Lemma shutdown_step_status

∀ s action s′

shutdown_steps action s′

shutdown_statuss′ = shutdown_statuss ∨ action = RecursiveExitshutdown_statuss′ ∨ action = HandoffHardExit shutdown_statuss′

Explore proof 2 tactics

Initial goal

⊢

∀s : shutdown_state action : shutdown_action s′ : shutdown_state, shutdown_steps action s′ → shutdown_statuss′ = shutdown_statuss ∨ action = RecursiveExitshutdown_statuss′ ∨ action = HandoffHardExit shutdown_statuss′

intros s action s′ H

s :

action :

s′ :

shutdown_closedshutdown_ats

H :

shutdown_steps action s′

⊢

shutdown_statuss′ = shutdown_statuss ∨ action = RecursiveExitshutdown_statuss′ ∨ action = HandoffHardExit shutdown_statuss′

destruct H ; simpl ; auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros s action s′ H

destruct H ; simpl ; auto

Cleanup and either handoff have closed registration.

184Definition shutdown_closedphase : shutdown_phase : Prop ≔

match phase with

Cleanup | HandedOff_

⇒

True

⇒

False

Closing registration is permanent through every remaining finite prefix.

188Theorem shutdown_closed_sticky

∀ s actions s′

shutdown_runs actions s′

shutdown_closedshutdown_ats′

Explore proof 5 tactics

Initial goal

⊢

∀s : shutdown_state actions : listshutdown_action s′ : shutdown_state, shutdown_runs actions s′ → shutdown_closedshutdown_ats → shutdown_closedshutdown_ats′

intros s actions s′ H

s :

actions :

s′ :

H :

shutdown_runs actions s′

⊢

shutdown_closedshutdown_ats → shutdown_closedshutdown_ats′

induction H ; auto |

s :

action :

s₁ :

actions :

s′ :

H :

shutdown_steps action s₁

H₀ :

shutdown_runs₁ actions s′

IHshutdown_run :

shutdown_closedshutdown_ats₁ → shutdown_closedshutdown_ats′

⊢

shutdown_closedshutdown_ats → shutdown_closedshutdown_ats′

intros Hclosed

s :

action :

s₁ :

actions :

s′ :

shutdown_closedshutdown_ats

H :

shutdown_steps action s₁

H₀ :

shutdown_runs₁ actions s′

IHshutdown_run :

shutdown_closedshutdown_ats₁ → shutdown_closedshutdown_ats′

Hclosed :

⊢

shutdown_closedshutdown_ats′

apply IHshutdown_run

s :

action :

s₁ :

actions :

s′ :

shutdown_closedshutdown_ats

H :

shutdown_steps action s₁

H₀ :

shutdown_runs₁ actions s′

IHshutdown_run :

shutdown_closedshutdown_ats₁ → shutdown_closedshutdown_ats′

Hclosed :

⊢

shutdown_closedshutdown_ats₁

destruct H ; simpl in * ; tauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros s actions s′ H

induction H ; auto |

intros Hclosed

apply IHshutdown_run

destruct H ; simpl in * ; tauto

A user-glibc handoff has no further lifecycle step.

197Theorem shutdown_handoff_stopped

∀ s kind action s′

shutdown_ats = HandedOffkind

¬shutdown_steps action s′

Explore proof 4 tactics

Initial goal

⊢

∀s : shutdown_state kind : handoff_kind action : shutdown_action s′ : shutdown_state, shutdown_ats = HandedOffkind → ¬shutdown_steps action s′

intros s kind action s′ Hat H

s :

kind :

action :

s′ :

Hat :

shutdown_ats = HandedOffkind

H :

shutdown_steps action s′

⊢

False

destruct H ; simpl in Hat ; try discriminate

kind :

s :

Hat :

shutdown_ats = HandedOffkind

status :

H :

∀kind : handoff_kind, shutdown_ats ≠ HandedOffkind

⊢

False

apply Hkind

kind :

s :

Hat :

shutdown_ats = HandedOffkind

status :

H :

∀kind : handoff_kind, shutdown_ats ≠ HandedOffkind

⊢

shutdown_ats = HandedOffkind

exact Hat

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros s kind action s′ Hat H

destruct H ; simpl in Hat ; try discriminate

apply Hkind

exact Hat

Once cleanup starts, registration cannot succeed.

205Theorem shutdown_done_no_registration

∀ s entry s′

shutdown_ats = Cleanup

¬shutdown_steps RegisterCallbackentry s′

Explore proof 3 tactics

Initial goal

⊢

∀s : shutdown_state entry : registration s′ : shutdown_state, shutdown_ats = Cleanup → ¬shutdown_steps RegisterCallbackentry s′

intros s entry s′ Hat H

s :

entry :

s′ :

Hat :

shutdown_ats = Cleanup

H :

shutdown_steps RegisterCallbackentry s′

⊢

False

inversion H ; subst

entry :

status :

active :

pending :

consumed :

listnat

q :

H :

shutdown_stepshutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q RegisterCallbackentry shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ entry :: pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q

Hat :

shutdown_atshutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q = Cleanup

H₂ :

¬Inregistration_tokenentry consumed ++ mapregistration_token pending

⊢

False

discriminate

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros s entry s′ Hat H

inversion H ; subst

discriminate

Project only the stdout actions; handoff is not an output error/discard.

210Definition shutdown_outputaction : shutdown_action : liststream_action ≔

match action with

ShutdownOutputa

⇒

[ ]

The stdout projection is exactly a stream run, including unfinished obligations.

214Theorem shutdown_stream_run

∀ s actions s′

shutdown_runs actions s′

stream_runshutdown_stdouts flat_mapshutdown_output actions shutdown_stdouts′

Explore proof 5 tactics

Initial goal

⊢

∀s : shutdown_state actions : listshutdown_action s′ : shutdown_state, shutdown_runs actions s′ → stream_runshutdown_stdouts flat_mapshutdown_output actions shutdown_stdouts′

intros s actions s′ H

s :

actions :

s′ :

H :

shutdown_runs actions s′

⊢

stream_runshutdown_stdouts flat_mapshutdown_output actions shutdown_stdouts′

induction H ; constructor |

s :

action :

s₁ :

actions :

s′ :

H :

shutdown_steps action s₁

H₀ :

shutdown_runs₁ actions s′

IHshutdown_run :

stream_runshutdown_stdouts₁ flat_mapshutdown_output actions shutdown_stdouts′

⊢

stream_runshutdown_stdouts flat_mapshutdown_output action :: actions shutdown_stdouts′

destruct H ; simpl in * ; try exact IHshutdown_run

2 open

actions :

s′ :

status :

active :

pending :

consumed :

listnat

q :

action :

q′ :

H :

stream_stepq action q′

H₀ :

shutdown_runshutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q′ actions s′

IHshutdown_run :

stream_runq′ flat_mapshutdown_output actions shutdown_stdouts′

⊢

stream_runq action :: flat_mapshutdown_output actions shutdown_stdouts′

focused goal

actions :

s′ :

status :

consumed :

listnat

q :

action :

q′ :

H :

∀bytes : listZ, action ≠ Acceptbytes

H₁ :

stream_stepq action q′

H₀ :

shutdown_runshutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q′ actions s′

IHshutdown_run :

stream_runq′ flat_mapshutdown_output actions shutdown_stdouts′

⊢

stream_runq action :: flat_mapshutdown_output actions shutdown_stdouts′

–eapply stream_next ; eassumption | exact IHshutdown_run

deferred goal

actions :

s′ :

status :

consumed :

listnat

q :

action :

q′ :

H :

∀bytes : listZ, action ≠ Acceptbytes

H₁ :

stream_stepq action q′

H₀ :

shutdown_runshutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q′ actions s′

IHshutdown_run :

stream_runq′ flat_mapshutdown_output actions shutdown_stdouts′

⊢

stream_runq action :: flat_mapshutdown_output actions shutdown_stdouts′

–eapply stream_next ; eassumption | exact IHshutdown_run

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros s actions s′ H

induction H ; constructor |

destruct H ; simpl in * ; try exact IHshutdown_run

–eapply stream_next ; eassumption | exact IHshutdown_run

Shutdown neither loses accepted bytes nor mistakes error discard for delivery.

225Theorem shutdown_output_accounting

∀ s actions s′

shutdown_runs actions s′

outstandingshutdown_stdouts ++ acceptedflat_mapshutdown_output actions = resolvedflat_mapshutdown_output actions ++ outstandingshutdown_stdouts′

Explore proof 4 tactics

Initial goal

⊢

∀s : shutdown_state actions : listshutdown_action s′ : shutdown_state, shutdown_runs actions s′ → outstandingshutdown_stdouts ++ acceptedflat_mapshutdown_output actions = resolvedflat_mapshutdown_output actions ++ outstandingshutdown_stdouts′

intros

s :

actions :

s′ :

H :

shutdown_runs actions s′

⊢

outstandingshutdown_stdouts ++ acceptedflat_mapshutdown_output actions = resolvedflat_mapshutdown_output actions ++ outstandingshutdown_stdouts′

apply stream_accounting

s :

actions :

s′ :

H :

shutdown_runs actions s′

⊢

stream_runshutdown_stdouts flat_mapshutdown_output actions shutdown_stdouts′

apply shutdown_stream_run

s :

actions :

s′ :

H :

shutdown_runs actions s′

⊢

shutdown_runs actions s′

assumption

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros

apply stream_accounting

apply shutdown_stream_run

assumption

Host completion is a separate, uninstantiated contract. Requiring its witness does not claim native host handlers or loader finalization safe.

233Inductive shutdown_observationhost_complete : handoff_kind → Z → stream_state → Prop : shutdown_state → listevent → Prop ≔

∀ kind status pending consumed q

host_completekind status q

observe_host_exit

shutdown_observationhost_complete mkShutdownHandedOffkind status pending consumed q ProcessExitprocess_statusstatus

Completion contributes exactly one exit observation, never a callback trace.

241Theorem shutdown_observation_single

∀ host s events

shutdown_observationhost s events

events = ProcessExitprocess_statusshutdown_statuss

Explore proof 3 tactics

Initial goal

⊢

∀host : handoff_kind → Z → stream_state → Prop s : shutdown_state events : listevent, shutdown_observationhost s events → events = ProcessExitprocess_statusshutdown_statuss

intros host s events H

host :

handoff_kind → Z → stream_state → Prop

s :

events :

listevent

H :

shutdown_observationhost s events

⊢

events = ProcessExitprocess_statusshutdown_statuss

destruct H

host :

handoff_kind → Z → stream_state → Prop

kind :

status :

pending :

consumed :

listnat

q :

H :

hostkind status q

⊢

ProcessExitprocess_statusstatus = ProcessExitprocess_statusshutdown_statusshutdown_at ≔ HandedOffkind; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros host s events H

destruct H

reflexivity

Read main's W-class return as a signed C int, before callbacks see it.

247Definition main_statusbits : Z : Z ≔

sign_extension2 ^ 32 2 ^ 31 bits

Signed interpretation does not change the final process low byte.

250Lemma main_status_low_byte

∀ bits

process_statusmain_statusbits = process_statusbits

Explore proof 11 tactics

Initial goal

⊢

∀bits : Z, process_statusmain_statusbits = process_statusbits

intros bits

bits :

⊢

process_statusmain_statusbits = process_statusbits

unfold main_status , sign_extension , process_status

bits :

⊢

2 ^ 31 ≤? bits mod 2 ^ 32

→

bits mod 2 ^ 32 − 2 ^ 32

else

bits mod 2 ^ 32

mod

256

bits mod 256

assert Hmod : bits mod 2 ^ 32 mod 256 = bits mod 256

2 open

bits :

⊢

bits mod 2 ^ 32 mod 256 = bits mod 256

focused goal

bits :

Hmod :

bits mod 2 ^ 32 mod 256 = bits mod 256

⊢

2 ^ 31 ≤? bits mod 2 ^ 32

→

bits mod 2 ^ 32 − 2 ^ 32

else

bits mod 2 ^ 32

mod

256

bits mod 256

{apply Z.mod_mod_divide

2 open

bits :

⊢

256 | 2 ^ 32

deferred goal

bits :

Hmod :

bits mod 2 ^ 32 mod 256 = bits mod 256

⊢

2 ^ 31 ≤? bits mod 2 ^ 32

→

bits mod 2 ^ 32 − 2 ^ 32

else

bits mod 2 ^ 32

mod

256

bits mod 256

exists 2 ^ 24

2 open

bits :

⊢

2 ^ 32 = 2 ^ 24 × 256

deferred goal

bits :

Hmod :

bits mod 2 ^ 32 mod 256 = bits mod 256

⊢

2 ^ 31 ≤? bits mod 2 ^ 32

→

bits mod 2 ^ 32 − 2 ^ 32

else

bits mod 2 ^ 32

mod

256

bits mod 256

reflexivity

deferred goal

bits :

Hmod :

bits mod 2 ^ 32 mod 256 = bits mod 256

⊢

2 ^ 31 ≤? bits mod 2 ^ 32

→

bits mod 2 ^ 32 − 2 ^ 32

else

bits mod 2 ^ 32

mod

256

bits mod 256

destruct 2 ^ 31 ≤? bits mod 2 ^ 32 ; | exact Hmod

bits :

Hmod :

bits mod 2 ^ 32 mod 256 = bits mod 256

⊢

bits mod 2 ^ 32 − 2 ^ 32 mod 256 = bits mod 256

rewrite Zminus_mod , Hmod

bits :

Hmod :

bits mod 2 ^ 32 mod 256 = bits mod 256

⊢

bits mod 256 − 2 ^ 32 mod 256 mod 256 = bits mod 256

replace 2 ^ 32 mod 256 with 0 by reflexivity

bits :

Hmod :

bits mod 2 ^ 32 mod 256 = bits mod 256

⊢

bits mod 256 − 0 mod 256 = bits mod 256

rewrite Z.sub_0_r , Z.mod_mod by lia

bits :

Hmod :

bits mod 2 ^ 32 mod 256 = bits mod 256

⊢

bits mod 256 = bits mod 256

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros bits

unfold main_status , sign_extension , process_status

assert Hmod : bits mod 2 ^ 32 mod 256 = bits mod 256

{apply Z.mod_mod_divide

exists 2 ^ 24

reflexivity

destruct 2 ^ 31 ≤? bits mod 2 ^ 32 ; | exact Hmod

rewrite Zminus_mod , Hmod

replace 2 ^ 32 mod 256 with 0 by reflexivity

rewrite Z.sub_0_r , Z.mod_mod by lia

reflexivity

No locals means the core return invalidates exactly nothing.

263Lemma return_no_locals_memory

∀ c

fr_localsc_framec = [ ]

invalidate_localsfr_localsc_framec c_memc = Somec_memc

Explore proof 3 tactics

Initial goal

⊢

∀c : config, fr_localsc_framec = [ ] → invalidate_localsfr_localsc_framec c_memc = Somec_memc

intros c H

c :

H :

fr_localsc_framec = [ ]

⊢

invalidate_localsfr_localsc_framec c_memc = Somec_memc

rewrite H

c :

H :

fr_localsc_framec = [ ]

⊢

invalidate_locals[ ] c_memc = Somec_memc

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros c H

rewrite H

reflexivity

Evidence for the narrow main-return bridge: no callers or locals, non-doomed W return, and an actual evaluated integer at the return site.

270Definition main_return_sitege : genv c : config bits : Z : Prop ≔

∃label value, fr_atc_framec = Execlabel [ ] JRetvalue ∧ fr_doomedc_framec = None ∧ fr_localsc_framec = [ ] ∧ c_callersc = [ ] ∧ fn_retfr_fnc_framec = RClassW ∧ value_xge fr_envc_framec W value = SomeWIntbits

This return really produces the core terminal, and its retained snapshot is final memory. No successor is added to ExternalMachine.Stopped.

279Theorem main_return_step

∀ ge c bits

main_return_sitege c bits

Semantics.stepge c = DoneRetWIntbits ∧ invalidate_localsfr_localsc_framec c_memc = Somec_memc

Explore proof 9 tactics

Initial goal

⊢

∀ge : genv c : config bits : Z, main_return_sitege c bits → stepge c = DoneRetWIntbits ∧ invalidate_localsfr_localsc_framec c_memc = Somec_memc

intros ge c bits label & value & Hat & Hd & Hl & Hc & Hr & Hv

ge :

c :

bits :

label :

value :

value

Hat :

fr_atc_framec = Execlabel [ ] JRetvalue

Hd :

fr_doomedc_framec = None

Hl :

fr_localsc_framec = [ ]

Hc :

c_callersc = [ ]

Hr :

Hv :

value_xge fr_envc_framec W value = SomeWIntbits

⊢

stepge c = DoneRetWIntbits ∧ invalidate_localsfr_localsc_framec c_memc = Somec_memc

split ; | apply return_no_locals_memory ; assumption

ge :

c :

bits :

label :

value :

value

Hat :

fr_atc_framec = Execlabel [ ] JRetvalue

Hd :

fr_doomedc_framec = None

Hl :

fr_localsc_framec = [ ]

Hc :

c_callersc = [ ]

Hr :

Hv :

value_xge fr_envc_framec W value = SomeWIntbits

⊢

stepge c = DoneRetWIntbits

unfold Semantics.step

ge :

c :

bits :

label :

value :

value

Hat :

fr_atc_framec = Execlabel [ ] JRetvalue

Hd :

fr_doomedc_framec = None

Hl :

fr_localsc_framec = [ ]

Hc :

c_callersc = [ ]

Hr :

Hv :

value_xge fr_envc_framec W value = SomeWIntbits

⊢

match fr_atc_framec with

Snapshot[ ] l

⇒

Nextc_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ 0; ptr_cap ≔ CNone fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc

Snapshot_ :: _ as xs l

⇒

negbforallbsnapshot_word xs

→

StuckString.StringAscii.Asciitrue true false false true true true false String.StringAscii.Asciifalse true true true false true true false String.StringAscii.Asciitrue false false false false true true false String.StringAscii.Asciifalse false false false true true true false String.StringAscii.Asciitrue true false false true true true false String.StringAscii.Asciifalse false false true false true true false String.StringAscii.Asciitrue true true true false true true false String.StringAscii.Asciifalse false true false true true true false String.EmptyString

else

Freshheap_req16 8 × Z.of_natlengthxs λbase : Z ⇒ c_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ putva_snapshot WPtrptr_addr ≔ base; ptr_cap ≔ Robase fr_envc_framec; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Enterl None; c_callers ≔ c_callersc; c_mem ≔ snapshot_valuesxs base allocatedc_memc heap_req16 8 × Z.of_natlengthxs base; c_fuel ≔ c_fuelc

Enterl from

⇒

c_fuelc =? 0

→

DoneOutOfFuel

else

or_stuckString.StringAscii.Asciifalse true false false false true true false String.StringAscii.Asciifalse false true true false true true false String.StringAscii.Asciitrue true true true false true true false String.StringAscii.Asciitrue true false false false true true false String.StringAscii.Asciitrue true false true false true true false String.EmptyString

let* b ≔ find_blockl fn_blocksfr_fnc_framec in

let* e ≔ phis_envge b_phisb from fr_envc_framec in

SomeNextc_frame ≔ fr_fn ≔ fr_fnc_framec; fr_env ≔ e; fr_locals ≔ fr_localsc_framec; fr_doomed ≔ fr_doomedc_framec; fr_at ≔ Execl b_instsb b_jumpb; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc − 1

Execl [ ] j

⇒

jump_stepge c l j

Execl i :: rest j

⇒

match let* why ≔ fr_doomedc_framec in if ahead_transparenti then None else Somewhy with

Somewhy

⇒

DoneUncheckedAheadwhy

None

⇒

or_stuckString.StringAscii.Asciitrue false false true false true true false String.StringAscii.Asciifalse true true true false true true false String.StringAscii.Asciitrue true false false true true true false String.StringAscii.Asciifalse false true false true true true false String.StringAscii.Asciifalse true false false true true true false String.StringAscii.Asciitrue false true false true true true false String.StringAscii.Asciitrue true false false false true true false String.StringAscii.Asciifalse false true false true true true false String.StringAscii.Asciitrue false false true false true true false String.StringAscii.Asciitrue true true true false true true false String.StringAscii.Asciifalse true true true false true true false String.EmptyString

let* out₀ ≔ inst_stepge c_framec c_memc i in

let* od ≔ doomed_resultge c_framec c_memc i out₀ in

Someinst_nextc l rest j fstod sndod

rewrite Hat

ge :

c :

bits :

label :

value :

value

Hat :

fr_atc_framec = Execlabel [ ] JRetvalue

Hd :

fr_doomedc_framec = None

Hl :

fr_localsc_framec = [ ]

Hc :

c_callersc = [ ]

Hr :

Hv :

value_xge fr_envc_framec W value = SomeWIntbits

⊢

jump_stepge c label JRetvalue = DoneRetWIntbits

unfold jump_step

ge :

c :

bits :

label :

value :

value

Hat :

fr_atc_framec = Execlabel [ ] JRetvalue

Hd :

fr_doomedc_framec = None

Hl :

fr_localsc_framec = [ ]

Hc :

c_callersc = [ ]

Hr :

Hv :

value_xge fr_envc_framec W value = SomeWIntbits

⊢

match fr_doomedc_framec with

Somewhy

⇒

DoneUncheckedAheadwhy

None

⇒

match fn_retfr_fnc_framec with

RClassk

⇒

let* x ≔ value_xge fr_envc_framec k value in

Somereturn_stepc Retx

⇒

None

rewrite Hd , Hr , Hv

ge :

c :

bits :

label :

value :

value

Hat :

fr_atc_framec = Execlabel [ ] JRetvalue

Hd :

fr_doomedc_framec = None

Hl :

fr_localsc_framec = [ ]

Hc :

c_callersc = [ ]

Hr :

Hv :

value_xge fr_envc_framec W value = SomeWIntbits

⊢

unfold return_step

ge :

c :

bits :

label :

value :

value

Hat :

fr_atc_framec = Execlabel [ ] JRetvalue

Hd :

fr_doomedc_framec = None

Hl :

fr_localsc_framec = [ ]

Hc :

c_callersc = [ ]

Hr :

Hv :

value_xge fr_envc_framec W value = SomeWIntbits

⊢

Some

or_stuckString.StringAscii.Asciifalse true false false true true true false String.StringAscii.Asciitrue false true false false true true false String.StringAscii.Asciifalse false true false true true true false String.StringAscii.Asciitrue false true false true true true false String.StringAscii.Asciifalse true false false true true true false String.StringAscii.Asciifalse true true true false true true false String.EmptyString

let* m ≔ invalidate_localsfr_localsc_framec c_memc in

match c_callersc with

[ ]

⇒

SomeDoneRetWIntbits

caller, pd :: callers

⇒

let* o′ ≔

match pd_convpd with

Somecw, kw

⇒

converted_outcomecw kw RetWIntbits

None

⇒

SomeRetWIntbits

let* e ≔ returned_envpd_respd o′ fr_envcaller in

SomeNextc_frame ≔ fr_fn ≔ fr_fncaller; fr_env ≔ e; fr_locals ≔ fr_localscaller; fr_doomed ≔ fr_doomedcaller; fr_at ≔ fr_atcaller; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ c_fuelc

rewrite Hl , Hc

ge :

c :

bits :

label :

value :

value

Hat :

fr_atc_framec = Execlabel [ ] JRetvalue

Hd :

fr_doomedc_framec = None

Hl :

fr_localsc_framec = [ ]

Hc :

c_callersc = [ ]

Hr :

Hv :

value_xge fr_envc_framec W value = SomeWIntbits

⊢

Some

let* _ ≔ invalidate_locals[ ] c_memc in

SomeDoneRetWIntbits

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros ge c bits label & value & Hat & Hd & Hl & Hc & Hr & Hv

split ; | apply return_no_locals_memory ; assumption

unfold Semantics.step

rewrite Hat

unfold jump_step

rewrite Hd , Hr , Hv

unfold return_step

rewrite Hl , Hc

reflexivity

A doomed return cannot use this bridge, regardless of its evaluated word.

291Lemma main_return_not_doomed

∀ ge c bits why

main_return_sitege c bits

fr_doomedc_framec ≠ Somewhy

Explore proof 3 tactics

Initial goal

⊢

∀ge : genv c : config bits : Z why : reason, main_return_sitege c bits → fr_doomedc_framec ≠ Somewhy

intros ge c bits why _ & _ & _ & Hd & _

ge :

c :

bits :

why :

reason

Hd :

fr_doomedc_framec = None

⊢

fr_doomedc_framec ≠ Somewhy

rewrite Hd

ge :

c :

bits :

why :

reason

Hd :

fr_doomedc_framec = None

⊢

None ≠ Somewhy

discriminate

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros ge c bits why _ & _ & _ & Hd & _

rewrite Hd

discriminate

A live-local return needs a different final-memory argument.

296Lemma main_return_no_live_locals

∀ ge c bits

main_return_sitege c bits

fr_localsc_framec = [ ]

Explore proof 2 tactics

Initial goal

⊢

∀ge : genv c : config bits : Z, main_return_sitege c bits → fr_localsc_framec = [ ]

intros ge c bits _ & _ & _ & _ & Hl & _

ge :

c :

bits :

Hl :

fr_localsc_framec = [ ]

⊢

fr_localsc_framec = [ ]

exact Hl

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros ge c bits _ & _ & _ & _ & Hl & _

exact Hl

Main initializes the lifecycle only with actual return-site evidence.

301Definition main_shutdownge : genv c : config bits : Z pending : listregistration q : stream_state s : shutdown_state : Prop ≔

main_return_sitege c bits ∧ s = mkShutdownTls main_statusbits pending [ ] q

The two's-complement -1 reaches callbacks as -1, and the host reports 255.

307Example main_minus_one: main_status4294967295 = −1 ∧ process_statusmain_status4294967295 = 255

Explore proof 2 tactics

Initial goal

⊢

main_status4294967295 = −1 ∧ process_statusmain_status4294967295 = 255

vm_compute

⊢

−1 = −1 ∧ 255 = 255

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

vm_compute

auto

Public lifecycle boundaries

Two registrations of the same function remain distinct instances.

314Definition exit_first: registration ≔

mkRegistration1 AtExitTInt42

The second registration deliberately repeats the function, not its token.

316Definition exit_second: registration ≔

mkRegistration2 AtExitTInt42

A handler dynamically registered by the newest callback.

318Definition exit_added: registration ≔

mkRegistration3 AtExitTInt43

A dynamically added callback runs before the older pending registration.

321Example shutdown_dynamic_lifo: ∀q, shutdown_runmkShutdownTls 31 exit_second; exit_first [ ] q EmptyTls; InvokeCallbackexit_second 31; RegisterCallbackexit_added; ReturnCallback; InvokeCallbackexit_added 31; ReturnCallback; InvokeCallbackexit_first 31; ReturnCallback; StartCleanup; HandoffSoftExit 31 mkShutdownHandedOffSoftExit 31 [ ] 2; 3; 1%nat q

Explore proof 12 tactics

Initial goal

⊢

∀q : stream_state, shutdown_runshutdown_at ≔ Tls; shutdown_status ≔ 31; shutdown_pending ≔ exit_second; exit_first; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls; InvokeCallbackexit_second 31; RegisterCallbackexit_added; ReturnCallback; InvokeCallbackexit_added 31; ReturnCallback; InvokeCallbackexit_first 31; ReturnCallback; StartCleanup; HandoffSoftExit 31 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 3%nat; 1%nat; shutdown_stdout ≔ q

intros q

q :

⊢

shutdown_runshutdown_at ≔ Tls; shutdown_status ≔ 31; shutdown_pending ≔ exit_second; exit_first; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls; InvokeCallbackexit_second 31; RegisterCallbackexit_added; ReturnCallback; InvokeCallbackexit_added 31; ReturnCallback; InvokeCallbackexit_first 31; ReturnCallback; StartCleanup; HandoffSoftExit 31 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 3%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_tls |

q :

⊢

shutdown_runshutdown_at ≔ Handlers; shutdown_status ≔ 31; shutdown_pending ≔ exit_second; exit_first; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q InvokeCallbackexit_second 31; RegisterCallbackexit_added; ReturnCallback; InvokeCallbackexit_added 31; ReturnCallback; InvokeCallbackexit_first 31; ReturnCallback; StartCleanup; HandoffSoftExit 31 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 3%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_invoke |

q :

⊢

shutdown_runshutdown_at ≔ InCallbackexit_second; shutdown_status ≔ 31; shutdown_pending ≔ exit_first; shutdown_consumed ≔ [ ] ++ registration_tokenexit_second; shutdown_stdout ≔ q RegisterCallbackexit_added; ReturnCallback; InvokeCallbackexit_added 31; ReturnCallback; InvokeCallbackexit_first 31; ReturnCallback; StartCleanup; HandoffSoftExit 31 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 3%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_register ; simpl ; intuition congruence |

q :

⊢

shutdown_runshutdown_at ≔ InCallbackexit_second; shutdown_status ≔ 31; shutdown_pending ≔ exit_added; exit_first; shutdown_consumed ≔ [ ] ++ registration_tokenexit_second; shutdown_stdout ≔ q ReturnCallback; InvokeCallbackexit_added 31; ReturnCallback; InvokeCallbackexit_first 31; ReturnCallback; StartCleanup; HandoffSoftExit 31 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 3%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_return |

q :

⊢

shutdown_runshutdown_at ≔ Handlers; shutdown_status ≔ 31; shutdown_pending ≔ exit_added; exit_first; shutdown_consumed ≔ [ ] ++ registration_tokenexit_second; shutdown_stdout ≔ q InvokeCallbackexit_added 31; ReturnCallback; InvokeCallbackexit_first 31; ReturnCallback; StartCleanup; HandoffSoftExit 31 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 3%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_invoke |

q :

⊢

shutdown_runshutdown_at ≔ InCallbackexit_added; shutdown_status ≔ 31; shutdown_pending ≔ exit_first; shutdown_consumed ≔ [ ] ++ registration_tokenexit_second ++ registration_tokenexit_added; shutdown_stdout ≔ q ReturnCallback; InvokeCallbackexit_first 31; ReturnCallback; StartCleanup; HandoffSoftExit 31 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 3%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_return |

q :

⊢

shutdown_runshutdown_at ≔ Handlers; shutdown_status ≔ 31; shutdown_pending ≔ exit_first; shutdown_consumed ≔ [ ] ++ registration_tokenexit_second ++ registration_tokenexit_added; shutdown_stdout ≔ q InvokeCallbackexit_first 31; ReturnCallback; StartCleanup; HandoffSoftExit 31 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 3%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_invoke |

q :

⊢

shutdown_runshutdown_at ≔ InCallbackexit_first; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ] ++ registration_tokenexit_second ++ registration_tokenexit_added ++ registration_tokenexit_first; shutdown_stdout ≔ q ReturnCallback; StartCleanup; HandoffSoftExit 31 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 3%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_return |

q :

⊢

shutdown_runshutdown_at ≔ Handlers; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ] ++ registration_tokenexit_second ++ registration_tokenexit_added ++ registration_tokenexit_first; shutdown_stdout ≔ q StartCleanup; HandoffSoftExit 31 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 3%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_cleanup |

q :

⊢

shutdown_runshutdown_at ≔ Cleanup; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ] ++ registration_tokenexit_second ++ registration_tokenexit_added ++ registration_tokenexit_first; shutdown_stdout ≔ q HandoffSoftExit 31 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 3%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_soft |

q :

⊢

shutdown_runshutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ] ++ registration_tokenexit_second ++ registration_tokenexit_added ++ registration_tokenexit_first; shutdown_stdout ≔ q [ ] shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 3%nat; 1%nat; shutdown_stdout ≔ q

constructor

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros q

eapply shutdown_next ; apply shutdown_tls |

eapply shutdown_next ; apply shutdown_invoke |

eapply shutdown_next ; apply shutdown_register ; simpl ; intuition congruence |

eapply shutdown_next ; apply shutdown_return |

eapply shutdown_next ; apply shutdown_invoke |

eapply shutdown_next ; apply shutdown_return |

eapply shutdown_next ; apply shutdown_invoke |

eapply shutdown_next ; apply shutdown_return |

eapply shutdown_next ; apply shutdown_cleanup |

eapply shutdown_next ; apply shutdown_soft |

constructor

Recursive exit abandons the active callback and supplies -1 to older ones.

342Example shutdown_recursive_status: ∀q, shutdown_runmkShutdownTls 31 exit_second; exit_first [ ] q EmptyTls; InvokeCallbackexit_second 31; RecursiveExit−1; EmptyTls; InvokeCallbackexit_first −1; ReturnCallback; StartCleanup; HandoffSoftExit −1 mkShutdownHandedOffSoftExit −1 [ ] 2; 1%nat q

Explore proof 10 tactics

Initial goal

⊢

∀q : stream_state, shutdown_runshutdown_at ≔ Tls; shutdown_status ≔ 31; shutdown_pending ≔ exit_second; exit_first; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls; InvokeCallbackexit_second 31; RecursiveExit−1; EmptyTls; InvokeCallbackexit_first −1; ReturnCallback; StartCleanup; HandoffSoftExit −1 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ −1; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 1%nat; shutdown_stdout ≔ q

intros q

q :

⊢

shutdown_runshutdown_at ≔ Tls; shutdown_status ≔ 31; shutdown_pending ≔ exit_second; exit_first; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls; InvokeCallbackexit_second 31; RecursiveExit−1; EmptyTls; InvokeCallbackexit_first −1; ReturnCallback; StartCleanup; HandoffSoftExit −1 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ −1; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_tls |

q :

⊢

shutdown_runshutdown_at ≔ Handlers; shutdown_status ≔ 31; shutdown_pending ≔ exit_second; exit_first; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q InvokeCallbackexit_second 31; RecursiveExit−1; EmptyTls; InvokeCallbackexit_first −1; ReturnCallback; StartCleanup; HandoffSoftExit −1 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ −1; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_invoke |

q :

⊢

shutdown_runshutdown_at ≔ InCallbackexit_second; shutdown_status ≔ 31; shutdown_pending ≔ exit_first; shutdown_consumed ≔ [ ] ++ registration_tokenexit_second; shutdown_stdout ≔ q RecursiveExit−1; EmptyTls; InvokeCallbackexit_first −1; ReturnCallback; StartCleanup; HandoffSoftExit −1 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ −1; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_recursive |

q :

⊢

shutdown_runshutdown_at ≔ Tls; shutdown_status ≔ −1; shutdown_pending ≔ exit_first; shutdown_consumed ≔ [ ] ++ registration_tokenexit_second; shutdown_stdout ≔ q EmptyTls; InvokeCallbackexit_first −1; ReturnCallback; StartCleanup; HandoffSoftExit −1 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ −1; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_tls |

q :

⊢

shutdown_runshutdown_at ≔ Handlers; shutdown_status ≔ −1; shutdown_pending ≔ exit_first; shutdown_consumed ≔ [ ] ++ registration_tokenexit_second; shutdown_stdout ≔ q InvokeCallbackexit_first −1; ReturnCallback; StartCleanup; HandoffSoftExit −1 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ −1; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_invoke |

q :

⊢

shutdown_runshutdown_at ≔ InCallbackexit_first; shutdown_status ≔ −1; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ] ++ registration_tokenexit_second ++ registration_tokenexit_first; shutdown_stdout ≔ q ReturnCallback; StartCleanup; HandoffSoftExit −1 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ −1; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_return |

q :

⊢

shutdown_runshutdown_at ≔ Handlers; shutdown_status ≔ −1; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ] ++ registration_tokenexit_second ++ registration_tokenexit_first; shutdown_stdout ≔ q StartCleanup; HandoffSoftExit −1 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ −1; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_cleanup |

q :

⊢

shutdown_runshutdown_at ≔ Cleanup; shutdown_status ≔ −1; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ] ++ registration_tokenexit_second ++ registration_tokenexit_first; shutdown_stdout ≔ q HandoffSoftExit −1 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ −1; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 1%nat; shutdown_stdout ≔ q

eapply shutdown_next ; apply shutdown_soft |

q :

⊢

shutdown_runshutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ −1; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ] ++ registration_tokenexit_second ++ registration_tokenexit_first; shutdown_stdout ≔ q [ ] shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ −1; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 1%nat; shutdown_stdout ≔ q

constructor

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros q

eapply shutdown_next ; apply shutdown_tls |

eapply shutdown_next ; apply shutdown_invoke |

eapply shutdown_next ; apply shutdown_recursive |

eapply shutdown_next ; apply shutdown_tls |

eapply shutdown_next ; apply shutdown_invoke |

eapply shutdown_next ; apply shutdown_return |

eapply shutdown_next ; apply shutdown_cleanup |

eapply shutdown_next ; apply shutdown_soft |

constructor

An active registration instance cannot be registered again with its old token.

360Example shutdown_no_instance_reuse: ∀q s′, ¬shutdown_stepmkShutdownInCallbackexit_second 31 exit_first 2%nat q RegisterCallbackexit_second s′

Explore proof 4 tactics

Initial goal

⊢

∀q : stream_state s′ : shutdown_state, ¬shutdown_stepshutdown_at ≔ InCallbackexit_second; shutdown_status ≔ 31; shutdown_pending ≔ exit_first; shutdown_consumed ≔ 2%nat; shutdown_stdout ≔ q RegisterCallbackexit_second s′

intros q s′ H

q :

s′ :

H :

shutdown_stepshutdown_at ≔ InCallbackexit_second; shutdown_status ≔ 31; shutdown_pending ≔ exit_first; shutdown_consumed ≔ 2%nat; shutdown_stdout ≔ q RegisterCallbackexit_second s′

⊢

False

inversion H ; subst

q :

H :

shutdown_stepshutdown_at ≔ InCallbackexit_second; shutdown_status ≔ 31; shutdown_pending ≔ exit_first; shutdown_consumed ≔ 2%nat; shutdown_stdout ≔ q RegisterCallbackexit_second shutdown_at ≔ InCallbackexit_second; shutdown_status ≔ 31; shutdown_pending ≔ exit_second; exit_first; shutdown_consumed ≔ 2%nat; shutdown_stdout ≔ q

H₇ :

¬Inregistration_tokenexit_second 2%nat ++ mapregistration_token exit_first

⊢

False

simpl in *

q :

H :

H₇ :

¬2%nat = 2%nat ∨ 1%nat = 2%nat ∨ False

⊢

False

tauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros q s′ H

inversion H ; subst

simpl in *

tauto

A callback's _exit(98) replaces exit(31), leaving handlers and output untouched.

366Example shutdown_hard_no_flush: shutdown_stepmkShutdownInCallbackexit_second 31 exit_first 2%nat mkStreamByteOriented 65; 90 false HandoffHardExit 98 mkShutdownHandedOffHardExit 98 exit_first 2%nat mkStreamByteOriented 65; 90 false

Explore proof 3 tactics

Initial goal

⊢

shutdown_stepshutdown_at ≔ InCallbackexit_second; shutdown_status ≔ 31; shutdown_pending ≔ exit_first; shutdown_consumed ≔ 2%nat; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 90; stream_error ≔ false HandoffHardExit 98 shutdown_at ≔ HandedOffHardExit; shutdown_status ≔ 98; shutdown_pending ≔ exit_first; shutdown_consumed ≔ 2%nat; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 90; stream_error ≔ false

apply shutdown_hard

⊢

∀kind : handoff_kind, shutdown_atshutdown_at ≔ InCallbackexit_second; shutdown_status ≔ 31; shutdown_pending ≔ exit_first; shutdown_consumed ≔ 2%nat; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 90; stream_error ≔ false ≠ HandedOffkind

intros kind H

kind :

H :

shutdown_atshutdown_at ≔ InCallbackexit_second; shutdown_status ≔ 31; shutdown_pending ≔ exit_first; shutdown_consumed ≔ 2%nat; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 90; stream_error ≔ false = HandedOffkind

⊢

False

discriminate

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

apply shutdown_hard

intros kind H

discriminate

Hard exit can replace status after cleanup has closed registration too.

376Example shutdown_cleanup_hard: ∀q, shutdown_stepmkShutdownCleanup 31 [ ] 2; 1%nat q HandoffHardExit 98 mkShutdownHandedOffHardExit 98 [ ] 2; 1%nat q

Explore proof 4 tactics

Initial goal

⊢

∀q : stream_state, shutdown_stepshutdown_at ≔ Cleanup; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 1%nat; shutdown_stdout ≔ q HandoffHardExit 98 shutdown_at ≔ HandedOffHardExit; shutdown_status ≔ 98; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 1%nat; shutdown_stdout ≔ q

intros q

q :

⊢

shutdown_stepshutdown_at ≔ Cleanup; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 1%nat; shutdown_stdout ≔ q HandoffHardExit 98 shutdown_at ≔ HandedOffHardExit; shutdown_status ≔ 98; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 1%nat; shutdown_stdout ≔ q

apply shutdown_hard

q :

⊢

∀kind : handoff_kind, shutdown_atshutdown_at ≔ Cleanup; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 1%nat; shutdown_stdout ≔ q ≠ HandedOffkind

intros kind H

q :

kind :

H :

shutdown_atshutdown_at ≔ Cleanup; shutdown_status ≔ 31; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 2%nat; 1%nat; shutdown_stdout ≔ q = HandedOffkind

⊢

False

discriminate

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros q

apply shutdown_hard

intros kind H

discriminate

Its conditional host observation reports the hard exit's own status.

382Example shutdown_hard_observation: ∀host q, hostHardExit 98 q → shutdown_observationhost mkShutdownHandedOffHardExit 98 exit_first 2%nat q ProcessExit98

Explore proof 3 tactics

Initial goal

⊢

∀host : handoff_kind → Z → stream_state → Prop q : stream_state, hostHardExit 98 q → shutdown_observationhost shutdown_at ≔ HandedOffHardExit; shutdown_status ≔ 98; shutdown_pending ≔ exit_first; shutdown_consumed ≔ 2%nat; shutdown_stdout ≔ q ProcessExit98

intros host q H

host :

handoff_kind → Z → stream_state → Prop

q :

H :

hostHardExit 98 q

⊢

shutdown_observationhost shutdown_at ≔ HandedOffHardExit; shutdown_status ≔ 98; shutdown_pending ≔ exit_first; shutdown_consumed ≔ 2%nat; shutdown_stdout ≔ q ProcessExit98

apply observe_host_exit

host :

handoff_kind → Z → stream_state → Prop

q :

H :

hostHardExit 98 q

⊢

hostHardExit 98 q

exact H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros host q H

apply observe_host_exit

exact H

Partial delivery followed by output error can leave a byte outstanding at handoff.

389Example shutdown_partial_error: shutdown_runmkShutdownCleanup 0 [ ] [ ] mkStreamByteOriented 65; 66; 90 false ShutdownOutputDeliver65; ShutdownOutputDiscard66; HandoffSoftExit 0 mkShutdownHandedOffSoftExit 0 [ ] [ ] mkStreamByteOriented 90 true

Explore proof 10 tactics

Initial goal

⊢

shutdown_runshutdown_at ≔ Cleanup; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; 90; stream_error ≔ false ShutdownOutputDeliver65; ShutdownOutputDiscard66; HandoffSoftExit 0 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 90; stream_error ≔ true

eapply shutdown_next

3 open

⊢

shutdown_stepshutdown_at ≔ Cleanup; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; 90; stream_error ≔ false ShutdownOutputDeliver65 ?s₁

focused goal

⊢

shutdown_run?s₁ ShutdownOutputDiscard66; HandoffSoftExit 0 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 90; stream_error ≔ true

shelved goal

⊢

–apply shutdown_cleanup_output ; intros bytes H ; discriminate |

3 open

⊢

stream_steporientation ≔ ByteOriented; outstanding ≔ 65; 66; 90; stream_error ≔ false Deliver65 ?q′

deferred goal

⊢

shutdown_runshutdown_at ≔ Cleanup; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ ?q′ ShutdownOutputDiscard66; HandoffSoftExit 0 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 90; stream_error ≔ true

shelved goal

⊢

apply stream_deliver65 66; 90 false

2 open

⊢

65 ≠ [ ]

deferred goal

⊢

shutdown_runshutdown_at ≔ Cleanup; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 66; 90; stream_error ≔ false ShutdownOutputDiscard66; HandoffSoftExit 0 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 90; stream_error ≔ true

discriminate

deferred goal

⊢

–eapply shutdown_next

3 open

⊢

shutdown_stepshutdown_at ≔ Cleanup; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 66; 90; stream_error ≔ false ShutdownOutputDiscard66 ?s₁

focused goal

⊢

shutdown_run?s₁ HandoffSoftExit 0 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 90; stream_error ≔ true

shelved goal

⊢

+apply shutdown_cleanup_output ; intros bytes H ; discriminate |

3 open

⊢

stream_steporientation ≔ ByteOriented; outstanding ≔ 66; 90; stream_error ≔ false Discard66 ?q′

deferred goal

⊢

shutdown_runshutdown_at ≔ Cleanup; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ ?q′ HandoffSoftExit 0 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 90; stream_error ≔ true

shelved goal

⊢

apply stream_discard66 90 false

2 open

⊢

66 ≠ [ ]

deferred goal

⊢

shutdown_runshutdown_at ≔ Cleanup; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 90; stream_error ≔ true HandoffSoftExit 0 shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 90; stream_error ≔ true

discriminate

deferred goal

⊢

+eapply shutdown_next ; apply shutdown_soft |

⊢

shutdown_runshutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 90; stream_error ≔ true [ ] shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ orientation ≔ ByteOriented; outstanding ≔ 90; stream_error ≔ true

constructor

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

eapply shutdown_next

–apply shutdown_cleanup_output ; intros bytes H ; discriminate |

apply stream_deliver65 66; 90 false

discriminate

–eapply shutdown_next

+apply shutdown_cleanup_output ; intros bytes H ; discriminate |

apply stream_discard66 90 false

discriminate

+eapply shutdown_next ; apply shutdown_soft |

constructor

A concrete no-locals main return: there is no invented stopped-state evidence.

404Definition returning_mainm : mem : config ≔

let f ≔ mkFuncTInt0 TInt0 RClassW [ ] [ ] in

mkConfigmkFramef [ ] [ ] None ExecTInt1 [ ] JRetConst4294967295 [ ] m 10

The return-site predicate checks the concrete return value and core transition.

409Example returning_main_bridge: ∀ge m, main_return_sitege returning_mainm 4294967295

Explore proof 3 tactics

Initial goal

⊢

∀ge : genv m : mem, main_return_sitege returning_mainm 4294967295

intros ge m

ge :

m :

mem

⊢

main_return_sitege returning_mainm 4294967295

exists TInt1, Const4294967295

ge :