Filnix wiki

s :

R.state

m :

w :

sh :

action :

full :

Hvalid :

libc_validspecs m w sh

Hselect :

selected_actionspecs m w sh action

Hstep :

shutdown_stepsh action full

⊢

P.shutdown_admissibleboundaryspecs s m w sh action

split ; split ; reflexivity |

specs :

s :

R.state

m :

w :

sh :

action :

full :

Hvalid :

libc_validspecs m w sh

Hselect :

selected_actionspecs m w sh action

Hstep :

shutdown_stepsh action full

⊢

contract_preP.action_contractboundaryspecs sh action P.action_wordsboundaryspecs sh action m w

split ; reflexivity |

specs :

s :

R.state

m :

w :

sh :

action :

full :

Hvalid :

libc_validspecs m w sh

Hselect :

selected_actionspecs m w sh action

Hstep :

shutdown_stepsh action full

⊢

libc_validspecs m w sh ∧ selected_actionspecs m w sh action ∧ ∃full₀ : shutdown_state, shutdown_stepsh action full₀

split ; exact Hvalid |

specs :

s :

R.state

m :

w :

sh :

action :

full :

Hvalid :

libc_validspecs m w sh

Hselect :

selected_actionspecs m w sh action

Hstep :

shutdown_stepsh action full

⊢

selected_actionspecs m w sh action ∧ ∃full₀ : shutdown_state, shutdown_stepsh action full₀

split ; exact Hselect |

specs :

s :

R.state

m :

w :

sh :

action :

full :

Hvalid :

libc_validspecs m w sh

Hselect :

selected_actionspecs m w sh action

Hstep :

shutdown_stepsh action full

⊢

∃full₀ : shutdown_state, shutdown_stepsh action full₀

exists full

specs :

s :

R.state

m :

w :

sh :

action :

full :

Hvalid :

libc_validspecs m w sh

Hselect :

selected_actionspecs m w sh action

Hstep :

shutdown_stepsh action full

⊢

shutdown_stepsh action full

exact Hstep

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros specs s m w sh action full _ Hvalid Hselect Hstep

split ; split ; reflexivity |

split ; reflexivity |

split ; exact Hvalid |

split ; exact Hselect |

exists full

exact Hstep

The born list, prefix and normal post all come from the SAME invocation. Runtime readiness follows its effect path; logical validity follows its post. Resource endings and unfinished prefixes do not take this rule.

87Theorem invocation_realizes

∀ specs s m w sh action trace s′ m′ w′

R.readys m

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s′ m′ w′

∃sh′, P.realizesboundaryspecs s m w sh action trace s′ m′ w′ sh′

Explore proof 4 tactics

Initial goal

⊢

∀specs : segments s : R.state m : mem w : stdio_world sh : shutdown_state action : shutdown_action trace : listevent s′ : R.state m′ : mem w′ : stdio_world, R.readys m → E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s′ m′ w′ → ∃sh′ : shutdown_state, P.realizesboundaryspecs s m w sh action trace s′ m′ w′ sh′

intros specs s m w sh action trace s′ m′ w′ Hr Hcall

specs :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s′ :

R.state

m′ :

w′ :

Hr :

R.readys m

Hcall :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s′ m′ w′

⊢

∃sh′ : shutdown_state, P.realizesboundaryspecs s m w sh action trace s′ m′ w′ sh′

pose proof E.invoke_preserve_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall Hr as Hr′ _

specs :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s′ :

R.state

m′ :

w′ :

Hr :

R.readys m

Hcall :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s′ m′ w′

Hr′ :

R.readys′ m′

⊢

∃sh′ : shutdown_state, P.realizesboundaryspecs s m w sh action trace s′ m′ w′ sh′

inversion Hcall ; subst

specs :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s′ :

R.state

m′ :

w′ :

Hr :

R.readys m

Hcall :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s′ m′ w′

Hr′ :

R.readys′ m′

born :

listZ

H :

contract_abiselected_contractspecs sh action CVoid [ ]

H₀ :

contract_preselected_contractspecs sh action [ ] m w

H₁ :

E.prefixselected_contractspecs sh action [ ] s m w born trace s′ m′ w′

H₂ :

contract_postselected_contractspecs sh action [ ] m w born trace CallReturn[ ] m′ w′

H₃ :

∀why : reason, CallReturn[ ] ≠ CallResourcewhy

H₄ :

∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsselected_contractspecs sh action values ∧ Forallword_authoritycontract_sourcesselected_contractspecs sh action [ ] m w born m′ values

H₅ :

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus

⊢

∃sh′ : shutdown_state, P.realizesboundaryspecs s m w sh action trace s′ m′ w′ sh′

match goal withHpre : contract_pre_ _ _ _ , Hpost : contract_post_ _ _ _ _ _ _ _ _ |- _⇒destruct Hpre as _ Hvalid Hselect Henabled ; destruct Hpost as _ target Hstep Htrace Hvalid′ ; exists target ; eapply P.realize_action ; simpl ; exact Hstep | split ; assumption | eapply selected_admits ; split ; assumption | exact Hselect | exact Hstep | eassumption | repeat split ; assumption | exact Htrace | split ; assumptionend

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros specs s m w sh action trace s′ m′ w′ Hr Hcall

pose proof E.invoke_preserve_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall Hr as Hr′ _

inversion Hcall ; subst

The body may carry a stronger opaque invariant for its ACTUAL entry inventory. This conservative form accepts every well-formed logical output queue; queues are obligations, not a claim about physical FILE buffers. Native puts preservation of this stronger invariant remains part of the trusted contract, not a new runtime axiom.

112Definition entry_repspecs : segments inventory : listregistration m : mem w : stdio_world : Prop ≔

∀q, stream_wfq → libc_validspecs m w mkShutdownTls 0 inventory [ ] q

Exact entry readiness survives a finite application run through the existing step theorem, without resetting to R.start after startup.

118Lemma body_ready

∀ specs inventory requests st trace st′

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv st trace st′

P.M.state_ready_ st

P.M.state_ready_ st′

Explore proof 6 tactics

Initial goal

⊢

∀specs : segments inventory : listregistration requests : listword → mem → stdio_world → Z → Z → Prop st : P.M.stateprogram_world trace : listevent st′ : P.M.stateprogram_world, P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv st trace st′ → P.M.state_readyprogram_world st → P.M.state_readyprogram_world st′

intros specs inventory requests st trace st′ Hrun

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

st :

P.M.stateprogram_world

trace :

listevent

st′ :

P.M.stateprogram_world

Hrun :

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv st trace st′

⊢

P.M.state_readyprogram_world st → P.M.state_readyprogram_world st′

induction Hrun ; auto |

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

st :

P.M.stateprogram_world

trace :

listevent

mid :

P.M.stateprogram_world

tail :

listevent

last :

P.M.stateprogram_world

H :

P.M.stepP.registryentry_repspecs inventory requests P.H.hi_genv st trace mid

Hrun :

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv mid tail last

IHHrun :

P.M.state_readyprogram_world mid → P.M.state_readyprogram_world last

⊢

P.M.state_readyprogram_world st → P.M.state_readyprogram_world last

intros Hr

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

st :

P.M.stateprogram_world

trace :

listevent

mid :

P.M.stateprogram_world

tail :

listevent

last :

P.M.stateprogram_world

H :

P.M.stepP.registryentry_repspecs inventory requests P.H.hi_genv st trace mid

Hrun :

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv mid tail last

IHHrun :

P.M.state_readyprogram_world mid → P.M.state_readyprogram_world last

Hr :

P.M.state_readyprogram_world st

⊢

P.M.state_readyprogram_world last

apply IHHrun

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

st :

P.M.stateprogram_world

trace :

listevent

mid :

P.M.stateprogram_world

tail :

listevent

last :

P.M.stateprogram_world

H :

P.M.stepP.registryentry_repspecs inventory requests P.H.hi_genv st trace mid

Hrun :

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv mid tail last

IHHrun :

P.M.state_readyprogram_world mid → P.M.state_readyprogram_world last

Hr :

P.M.state_readyprogram_world st

⊢

P.M.state_readyprogram_world mid

eapply P.M.step_ready ; | exact H | exact Hr

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

st :

P.M.stateprogram_world

trace :

listevent

mid :

P.M.stateprogram_world

tail :

listevent

last :

P.M.stateprogram_world

H :

P.M.stepP.registryentry_repspecs inventory requests P.H.hi_genv st trace mid

Hrun :

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv mid tail last

IHHrun :

P.M.state_readyprogram_world mid → P.M.state_readyprogram_world last

Hr :

P.M.state_readyprogram_world st

⊢

ge_freeP.H.hi_genv = R.free

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros specs inventory requests st trace st′ Hrun

induction Hrun ; auto |

intros Hr

apply IHHrun

eapply P.M.step_ready ; | exact H | exact Hr

reflexivity

Reached returning puts retains the selected entry's inventory AND its callback-validity representation. The former alone would be insufficient. This discharges the existing reached-call closure, not native coverage.

129Theorem reached_puts_closed

∀ specs inventory requests start

∀s m s′ m′ w, R.safepoints m s′ m′ → entry_repspecs inventory m w → stdio_readym w → entry_repspecs inventory m′ w ∧ stdio_readym′ w

P.body_inventry_repspecs inventory start

P.M.state_ready_ start

program_pendingP.world_ofstart = inventory

P.puts_shutdown_closedentry_repspecs inventory requests boundaryspecs start

Explore proof 12 tactics

Initial goal

⊢

∀specs : segments inventory : listregistration requests : listword → mem → stdio_world → Z → Z → Prop start : P.M.stateprogram_world, ∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → entry_repspecs inventory m w → stdio_readym w → entry_repspecs inventory m′ w ∧ stdio_readym′ w → P.body_inventry_repspecs inventory start → P.M.state_readyprogram_world start → program_pendingP.world_ofstart = inventory → P.puts_shutdown_closedentry_repspecs inventory requests boundaryspecs start

intros specs inventory requests start Hstable Hinv Hr Hinitial

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

start :

P.M.stateprogram_world

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → entry_repspecs inventory m w → stdio_readym w → entry_repspecs inventory m′ w ∧ stdio_readym′ w

Hinv :

P.body_inventry_repspecs inventory start

Hr :

P.M.state_readyprogram_world start

Hinitial :

program_pendingP.world_ofstart = inventory

⊢

P.puts_shutdown_closedentry_repspecs inventory requests boundaryspecs start

intros first s m w fuel trace n s′ m′ w′ Hrun Hcall

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

start :

P.M.stateprogram_world

Hstable :

Hinv :

P.body_inventry_repspecs inventory start

Hr :

P.M.state_readyprogram_world start

Hinitial :

program_pendingP.world_ofstart = inventory

first :

listevent

s :

R.state

m :

w :

fuel :

trace :

listevent

n :

s′ :

R.state

m′ :

w′ :

Hrun :

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv start first P.M.Runninghi_callm fuel, s w

Hcall :

P.M.E.invokeprogram_putsentry_repspecs inventory requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′

⊢

P.shutdown_readyboundaryspecs s′ m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′

pose proof P.body_run_inventory_ _ Hstable _ _ _ Hrun Hinv as Hpending

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

start :

P.M.stateprogram_world

Hstable :

Hinv :

P.body_inventry_repspecs inventory start

Hr :

P.M.state_readyprogram_world start

Hinitial :

program_pendingP.world_ofstart = inventory

first :

listevent

s :

R.state

m :

w :

fuel :

trace :

listevent

n :

s′ :

R.state

m′ :

w′ :

Hrun :

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv start first P.M.Runninghi_callm fuel, s w

Hcall :

P.M.E.invokeprogram_putsentry_repspecs inventory requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′

Hpending :

program_pendingP.world_ofP.M.Runninghi_callm fuel, s w = program_pendingP.world_ofstart

⊢

simpl in Hpending

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

start :

P.M.stateprogram_world

Hstable :

Hinv :

P.body_inventry_repspecs inventory start

Hr :

P.M.state_readyprogram_world start

Hinitial :

program_pendingP.world_ofstart = inventory

first :

listevent

s :

R.state

m :

w :

fuel :

trace :

listevent

n :

s′ :

R.state

m′ :

w′ :

Hrun :

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv start first P.M.Runninghi_callm fuel, s w

Hcall :

P.M.E.invokeprogram_putsentry_repspecs inventory requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′

Hpending :

program_pendingw = program_pendingP.world_ofstart

⊢

rewrite Hinitial in Hpending

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

start :

P.M.stateprogram_world

Hstable :

Hinv :

P.body_inventry_repspecs inventory start

Hr :

P.M.state_readyprogram_world start

Hinitial :

program_pendingP.world_ofstart = inventory

first :

listevent

s :

R.state

m :

w :

fuel :

trace :

listevent

n :

s′ :

R.state

m′ :

w′ :

Hrun :

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv start first P.M.Runninghi_callm fuel, s w

Hcall :

P.M.E.invokeprogram_putsentry_repspecs inventory requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′

Hpending :

program_pendingw = inventory

⊢

destruct P.C.program_invoke_continuity_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as Hpending′ _ Hwf _

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

start :

P.M.stateprogram_world

Hstable :

Hinv :

P.body_inventry_repspecs inventory start

Hr :

P.M.state_readyprogram_world start

Hinitial :

program_pendingP.world_ofstart = inventory

first :

listevent

s :

R.state

m :

w :

fuel :

trace :

listevent

n :

s′ :

R.state

m′ :

w′ :

Hrun :

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv start first P.M.Runninghi_callm fuel, s w

Hcall :

P.M.E.invokeprogram_putsentry_repspecs inventory requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′

Hpending :

program_pendingw = inventory

Hpending′ :

Hwf :

⊢

destruct E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born _ Hrep _ _

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

start :

P.M.stateprogram_world

Hstable :

Hinv :

P.body_inventry_repspecs inventory start

Hr :

P.M.state_readyprogram_world start

Hinitial :

program_pendingP.world_ofstart = inventory

first :

listevent

s :

R.state

m :

w :

fuel :

trace :

listevent

n :

s′ :

R.state

m′ :

w′ :

Hrun :

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv start first P.M.Runninghi_callm fuel, s w

Hcall :

P.M.E.invokeprogram_putsentry_repspecs inventory requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′

Hpending :

program_pendingw = inventory

Hpending′ :

Hwf :

born :

listZ

Hrep :

entry_repspecs inventory m′ program_stdiow′

⊢

split

2 open

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

start :

P.M.stateprogram_world

Hstable :

Hinv :

P.body_inventry_repspecs inventory start

Hr :

P.M.state_readyprogram_world start

Hinitial :

program_pendingP.world_ofstart = inventory

first :

listevent

s :

R.state

m :

w :

fuel :

trace :

listevent

n :

s′ :

R.state

m′ :

w′ :

Hrun :

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv start first P.M.Runninghi_callm fuel, s w

Hcall :

P.M.E.invokeprogram_putsentry_repspecs inventory requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′

Hpending :

program_pendingw = inventory

Hpending′ :

Hwf :

born :

listZ

Hrep :

entry_repspecs inventory m′ program_stdiow′

⊢

R.readys′ m′

focused goal

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

start :

P.M.stateprogram_world

Hstable :

Hinv :

P.body_inventry_repspecs inventory start

Hr :

P.M.state_readyprogram_world start

Hinitial :

program_pendingP.world_ofstart = inventory

first :

listevent

s :

R.state

m :

w :

fuel :

trace :

listevent

n :

s′ :

R.state

m′ :

w′ :

Hrun :

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv start first P.M.Runninghi_callm fuel, s w

Hcall :

P.M.E.invokeprogram_putsentry_repspecs inventory requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′

Hpending :

program_pendingw = inventory

Hpending′ :

Hwf :

born :

listZ

Hrep :

entry_repspecs inventory m′ program_stdiow′

⊢

libc_validspecs m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′

–exact proj1E.invoke_preserve_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall body_ready_ _ _ _ _ _ Hrun Hr

deferred goal

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

start :

P.M.stateprogram_world

Hstable :

Hinv :

P.body_inventry_repspecs inventory start

Hr :

P.M.state_readyprogram_world start

Hinitial :

program_pendingP.world_ofstart = inventory

first :

listevent

s :

R.state

m :

w :

fuel :

trace :

listevent

n :

s′ :

R.state

m′ :

w′ :

Hrun :

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv start first P.M.Runninghi_callm fuel, s w

Hcall :

P.M.E.invokeprogram_putsentry_repspecs inventory requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′

Hpending :

program_pendingw = inventory

Hpending′ :

Hwf :

born :

listZ

Hrep :

entry_repspecs inventory m′ program_stdiow′

⊢

libc_validspecs m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′

–rewrite Hpending′ , Hpending

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

start :

P.M.stateprogram_world

Hstable :

Hinv :

P.body_inventry_repspecs inventory start

Hr :

P.M.state_readyprogram_world start

Hinitial :

program_pendingP.world_ofstart = inventory

first :

listevent

s :

R.state

m :

w :

fuel :

trace :

listevent

n :

s′ :

R.state

m′ :

w′ :

Hrun :

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv start first P.M.Runninghi_callm fuel, s w

Hcall :

P.M.E.invokeprogram_putsentry_repspecs inventory requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′

Hpending :

program_pendingw = inventory

Hpending′ :

Hwf :

born :

listZ

Hrep :

entry_repspecs inventory m′ program_stdiow′

⊢

libc_validspecs m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ inventory; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′

apply Hrep

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

start :

P.M.stateprogram_world

Hstable :

Hinv :

P.body_inventry_repspecs inventory start

Hr :

P.M.state_readyprogram_world start

Hinitial :

program_pendingP.world_ofstart = inventory

first :

listevent

s :

R.state

m :

w :

fuel :

trace :

listevent

n :

s′ :

R.state

m′ :

w′ :

Hrun :

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv start first P.M.Runninghi_callm fuel, s w

Hcall :

P.M.E.invokeprogram_putsentry_repspecs inventory requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′

Hpending :

program_pendingw = inventory

Hpending′ :

Hwf :

born :

listZ

Hrep :

entry_repspecs inventory m′ program_stdiow′

⊢

exact Hwf

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros specs inventory requests start Hstable Hinv Hr Hinitial

intros first s m w fuel trace n s′ m′ w′ Hrun Hcall

pose proof P.body_run_inventory_ _ Hstable _ _ _ Hrun Hinv as Hpending

simpl in Hpending

rewrite Hinitial in Hpending

destruct P.C.program_invoke_continuity_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as Hpending′ _ Hwf _

destruct E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born _ Hrep _ _

split

–exact proj1E.invoke_preserve_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall body_ready_ _ _ _ _ _ Hrun Hr

–rewrite Hpending′ , Hpending

apply Hrep

exact Hwf

A finite chain of actual normal invocations at exact shared snapshots. Logical edges name the targets; their validity and runtime readiness are extracted from those same calls, not supplied for each endpoint. This is not coverage of unfinished, refused or native executions.

154Inductive normal_runspecs : segments : R.state → mem → stdio_world → shutdown_state → listevent → R.state → mem → stdio_world → shutdown_state → Prop ≔

∀ s m w sh

normal_runspecs s m w sh [ ] s m w sh

normal_refl

∀ s m w sh action trace s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

shutdown_stepsh action sh₁

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s₁ m₁ w₁

normal_runspecs s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

normal_next

normal_runspecs s m w sh trace ++ tail s′ m′ w′ sh′

Lift the invocation chain through the existing adapter. Logical target uniqueness identifies its extracted endpoint with the named cutpoint.

167Theorem normal_run_lifts

∀ specs s m w sh trace s′ m′ w′ sh′ rep requests host

normal_runspecs s m w sh trace s′ m′ w′ sh′

R.readys m

P.runrep requests boundaryspecs host P.ShuttingDowns m w sh trace P.ShuttingDowns′ m′ w′ sh′ ∧ stream_wfshutdown_stdoutsh → stream_wfshutdown_stdoutsh′

Explore proof 14 tactics

Initial goal

⊢

∀specs : segments s : R.state m : mem w : stdio_world sh : shutdown_state trace : listevent s′ : R.state m′ : mem w′ : stdio_world sh′ : shutdown_state rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop host : P.host_boundary, normal_runspecs s m w sh trace s′ m′ w′ sh′ → R.readys m → P.runrep requests boundaryspecs host P.ShuttingDowns m w sh trace P.ShuttingDowns′ m′ w′ sh′ ∧ stream_wfshutdown_stdoutsh → stream_wfshutdown_stdoutsh′

intros specs s m w sh trace s′ m′ w′ sh′ rep requests host Hrun

specs :

s :

R.state

m :

w :

sh :

trace :

listevent

s′ :

R.state

m′ :

w′ :

sh′ :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

Hrun :

normal_runspecs s m w sh trace s′ m′ w′ sh′

⊢

R.readys m → P.runrep requests boundaryspecs host P.ShuttingDowns m w sh trace P.ShuttingDowns′ m′ w′ sh′ ∧ stream_wfshutdown_stdoutsh → stream_wfshutdown_stdoutsh′

induction Hrun ; intros Hr

2 open

specs :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

s :

R.state

m :

w :

sh :

Hr :

R.readys m

⊢

P.runrep requests boundaryspecs host P.ShuttingDowns m w sh [ ] P.ShuttingDowns m w sh ∧ stream_wfshutdown_stdoutsh → stream_wfshutdown_stdoutsh

focused goal

specs :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s₁ :

R.state

m₁ :

w₁ :

sh₁ :

tail :

listevent

s′ :

R.state

m′ :

w′ :

sh′ :

H :

shutdown_stepsh action sh₁

H₀ :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s₁ m₁ w₁

Hrun :

normal_runspecs s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

IHHrun :

R.readys₁ m₁ → P.runrep requests boundaryspecs host P.ShuttingDowns₁ m₁ w₁ sh₁ tail P.ShuttingDowns′ m′ w′ sh′ ∧ stream_wfshutdown_stdoutsh₁ → stream_wfshutdown_stdoutsh′

Hr :

R.readys m

⊢

P.runrep requests boundaryspecs host P.ShuttingDowns m w sh trace ++ tail P.ShuttingDowns′ m′ w′ sh′ ∧ stream_wfshutdown_stdoutsh → stream_wfshutdown_stdoutsh′

–split ; constructor | auto

deferred goal

specs :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s₁ :

R.state

m₁ :

w₁ :

sh₁ :

tail :

listevent

s′ :

R.state

m′ :

w′ :

sh′ :

H :

shutdown_stepsh action sh₁

H₀ :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s₁ m₁ w₁

Hrun :

normal_runspecs s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

IHHrun :

Hr :

R.readys m

⊢

P.runrep requests boundaryspecs host P.ShuttingDowns m w sh trace ++ tail P.ShuttingDowns′ m′ w′ sh′ ∧ stream_wfshutdown_stdoutsh → stream_wfshutdown_stdoutsh′

–destruct invocation_realizes_ _ _ _ _ _ _ _ _ _ Hr H₀ as target Hreal

specs :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s₁ :

R.state

m₁ :

w₁ :

sh₁ :

tail :

listevent

s′ :

R.state

m′ :

w′ :

sh′ :

H :

shutdown_stepsh action sh₁

H₀ :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s₁ m₁ w₁

Hrun :

normal_runspecs s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

IHHrun :

Hr :

R.readys m

target :

Hreal :

P.realizesboundaryspecs s m w sh action trace s₁ m₁ w₁ target

⊢

P.runrep requests boundaryspecs host P.ShuttingDowns m w sh trace ++ tail P.ShuttingDowns′ m′ w′ sh′ ∧ stream_wfshutdown_stdoutsh → stream_wfshutdown_stdoutsh′

assert Htarget : target = sh₁

2 open

specs :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s₁ :

R.state

m₁ :

w₁ :

sh₁ :

tail :

listevent

s′ :

R.state

m′ :

w′ :

sh′ :

H :

shutdown_stepsh action sh₁

H₀ :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s₁ m₁ w₁

Hrun :

normal_runspecs s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

IHHrun :

Hr :

R.readys m

target :

Hreal :

P.realizesboundaryspecs s m w sh action trace s₁ m₁ w₁ target

⊢

target = sh₁

focused goal

specs :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s₁ :

R.state

m₁ :

w₁ :

sh₁ :

tail :

listevent

s′ :

R.state

m′ :

w′ :

sh′ :

H :

shutdown_stepsh action sh₁

H₀ :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s₁ m₁ w₁

Hrun :

normal_runspecs s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

IHHrun :

Hr :

R.readys m

target :

Hreal :

P.realizesboundaryspecs s m w sh action trace s₁ m₁ w₁ target

Htarget :

target = sh₁

⊢

P.runrep requests boundaryspecs host P.ShuttingDowns m w sh trace ++ tail P.ShuttingDowns′ m′ w′ sh′ ∧ stream_wfshutdown_stdoutsh → stream_wfshutdown_stdoutsh′

{inversion Hreal ; subst

2 open

specs :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

s :

R.state

m :

w :

sh :

action :

s₁ :

R.state

m₁ :

w₁ :

sh₁ :

tail :

listevent

s′ :

R.state

m′ :

w′ :

sh′ :

H :

shutdown_stepsh action sh₁

H₀ :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w P.action_eventsaction CallReturn[ ] s₁ m₁ w₁

Hrun :

normal_runspecs s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

IHHrun :

Hr :

R.readys m

target :

Hreal :

P.realizesboundaryspecs s m w sh action P.action_eventsaction s₁ m₁ w₁ target

born :

listZ

H₁ :

shutdown_stepsh action target

H₂ :

P.shutdown_readyboundaryspecs s m w sh

H₃ :

P.shutdown_admissibleboundaryspecs s m w sh action

H₅ :

P.action_postboundaryspecs sh action s m w born P.action_eventsaction s₁ m₁ w₁ target

H₄ :

P.M.E.prefixP.action_contractboundaryspecs sh action P.action_wordsboundaryspecs sh action s m w born P.action_eventsaction s₁ m₁ w₁

H₇ :

P.shutdown_readyboundaryspecs s₁ m₁ w₁ target

⊢

target = sh₁

deferred goal

specs :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s₁ :

R.state

m₁ :

w₁ :

sh₁ :

tail :

listevent

s′ :

R.state

m′ :

w′ :

sh′ :

H :

shutdown_stepsh action sh₁

H₀ :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s₁ m₁ w₁

Hrun :

normal_runspecs s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

IHHrun :

Hr :

R.readys m

target :

Hreal :

P.realizesboundaryspecs s m w sh action trace s₁ m₁ w₁ target

Htarget :

target = sh₁

⊢

P.runrep requests boundaryspecs host P.ShuttingDowns m w sh trace ++ tail P.ShuttingDowns′ m′ w′ sh′ ∧ stream_wfshutdown_stdoutsh → stream_wfshutdown_stdoutsh′

eapply shutdown_step_target ; eauto

deferred goal

specs :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s₁ :

R.state

m₁ :

w₁ :

sh₁ :

tail :

listevent

s′ :

R.state

m′ :

w′ :

sh′ :

H :

shutdown_stepsh action sh₁

H₀ :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s₁ m₁ w₁

Hrun :

normal_runspecs s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

IHHrun :

Hr :

R.readys m

target :

Hreal :

P.realizesboundaryspecs s m w sh action trace s₁ m₁ w₁ target

Htarget :

target = sh₁

⊢

P.runrep requests boundaryspecs host P.ShuttingDowns m w sh trace ++ tail P.ShuttingDowns′ m′ w′ sh′ ∧ stream_wfshutdown_stdoutsh → stream_wfshutdown_stdoutsh′

subst target

specs :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s₁ :

R.state

m₁ :

w₁ :

sh₁ :

tail :

listevent

s′ :

R.state

m′ :

w′ :

sh′ :

H :

shutdown_stepsh action sh₁

H₀ :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s₁ m₁ w₁

Hrun :

normal_runspecs s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

IHHrun :

Hr :

R.readys m

Hreal :

P.realizesboundaryspecs s m w sh action trace s₁ m₁ w₁ sh₁

⊢

P.runrep requests boundaryspecs host P.ShuttingDowns m w sh trace ++ tail P.ShuttingDowns′ m′ w′ sh′ ∧ stream_wfshutdown_stdoutsh → stream_wfshutdown_stdoutsh′

destruct IHHrunproj1E.invoke_preserve_ _ _ _ _ _ _ _ _ _ _ _ _ H₀ Hr as Htail Hwf

specs :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s₁ :

R.state

m₁ :

w₁ :

sh₁ :

tail :

listevent

s′ :

R.state

m′ :

w′ :

sh′ :

H :

shutdown_stepsh action sh₁

H₀ :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s₁ m₁ w₁

Hrun :

normal_runspecs s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

IHHrun :

Hr :

R.readys m

Hreal :

P.realizesboundaryspecs s m w sh action trace s₁ m₁ w₁ sh₁

Htail :

P.runrep requests boundaryspecs host P.ShuttingDowns₁ m₁ w₁ sh₁ tail P.ShuttingDowns′ m′ w′ sh′

Hwf :

stream_wfshutdown_stdoutsh₁ → stream_wfshutdown_stdoutsh′

⊢

P.runrep requests boundaryspecs host P.ShuttingDowns m w sh trace ++ tail P.ShuttingDowns′ m′ w′ sh′ ∧ stream_wfshutdown_stdoutsh → stream_wfshutdown_stdoutsh′

split

2 open

specs :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s₁ :

R.state

m₁ :

w₁ :

sh₁ :

tail :

listevent

s′ :

R.state

m′ :

w′ :

sh′ :

H :

shutdown_stepsh action sh₁

H₀ :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s₁ m₁ w₁

Hrun :

normal_runspecs s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

IHHrun :

Hr :

R.readys m

Hreal :

P.realizesboundaryspecs s m w sh action trace s₁ m₁ w₁ sh₁

Htail :

P.runrep requests boundaryspecs host P.ShuttingDowns₁ m₁ w₁ sh₁ tail P.ShuttingDowns′ m′ w′ sh′

Hwf :

stream_wfshutdown_stdoutsh₁ → stream_wfshutdown_stdoutsh′

⊢

P.runrep requests boundaryspecs host P.ShuttingDowns m w sh trace ++ tail P.ShuttingDowns′ m′ w′ sh′

focused goal

specs :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s₁ :

R.state

m₁ :

w₁ :

sh₁ :

tail :

listevent

s′ :

R.state

m′ :

w′ :

sh′ :

H :

shutdown_stepsh action sh₁

H₀ :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s₁ m₁ w₁

Hrun :

normal_runspecs s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

IHHrun :

Hr :

R.readys m

Hreal :

P.realizesboundaryspecs s m w sh action trace s₁ m₁ w₁ sh₁

Htail :

P.runrep requests boundaryspecs host P.ShuttingDowns₁ m₁ w₁ sh₁ tail P.ShuttingDowns′ m′ w′ sh′

Hwf :

stream_wfshutdown_stdoutsh₁ → stream_wfshutdown_stdoutsh′

⊢

stream_wfshutdown_stdoutsh → stream_wfshutdown_stdoutsh′

+eapply P.program_next ; apply P.program_shutdown with action := action ; exact Hreal | exact Htail

deferred goal

specs :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s₁ :

R.state

m₁ :

w₁ :

sh₁ :

tail :

listevent

s′ :

R.state

m′ :

w′ :

sh′ :

H :

shutdown_stepsh action sh₁

H₀ :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s₁ m₁ w₁

Hrun :

normal_runspecs s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

IHHrun :

Hr :

R.readys m

Hreal :

P.realizesboundaryspecs s m w sh action trace s₁ m₁ w₁ sh₁

Htail :

P.runrep requests boundaryspecs host P.ShuttingDowns₁ m₁ w₁ sh₁ tail P.ShuttingDowns′ m′ w′ sh′

Hwf :

stream_wfshutdown_stdoutsh₁ → stream_wfshutdown_stdoutsh′

⊢

stream_wfshutdown_stdoutsh → stream_wfshutdown_stdoutsh′

+intros Hq

specs :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s₁ :

R.state

m₁ :

w₁ :

sh₁ :

tail :

listevent

s′ :

R.state

m′ :

w′ :

sh′ :

stream_wfshutdown_stdoutsh

H :

shutdown_stepsh action sh₁

H₀ :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s₁ m₁ w₁

Hrun :

normal_runspecs s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

IHHrun :

Hr :

R.readys m

Hreal :

P.realizesboundaryspecs s m w sh action trace s₁ m₁ w₁ sh₁

Htail :

P.runrep requests boundaryspecs host P.ShuttingDowns₁ m₁ w₁ sh₁ tail P.ShuttingDowns′ m′ w′ sh′

Hwf :

stream_wfshutdown_stdoutsh₁ → stream_wfshutdown_stdoutsh′

Hq :

⊢

stream_wfshutdown_stdoutsh′

apply Hwf

specs :

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

s :

R.state

m :

w :

sh :

action :

trace :

listevent

s₁ :

R.state

m₁ :

w₁ :

sh₁ :

tail :

listevent

s′ :

R.state

m′ :

w′ :

sh′ :

stream_wfshutdown_stdoutsh

H :

shutdown_stepsh action sh₁

H₀ :

E.invokeselected_contractspecs sh action CVoid [ ] [ ] s m w trace CallReturn[ ] s₁ m₁ w₁

Hrun :

normal_runspecs s₁ m₁ w₁ sh₁ tail s′ m′ w′ sh′

IHHrun :

Hr :

R.readys m

Hreal :

P.realizesboundaryspecs s m w sh action trace s₁ m₁ w₁ sh₁

Htail :

P.runrep requests boundaryspecs host P.ShuttingDowns₁ m₁ w₁ sh₁ tail P.ShuttingDowns′ m′ w′ sh′

Hwf :

stream_wfshutdown_stdoutsh₁ → stream_wfshutdown_stdoutsh′

Hq :

⊢

stream_wfshutdown_stdoutsh₁

destruct H ; simpl in * ; try exact Hq ; eapply stream_step_wf ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros specs s m w sh trace s′ m′ w′ sh′ rep requests host Hrun

induction Hrun ; intros Hr

–split ; constructor | auto

–destruct invocation_realizes_ _ _ _ _ _ _ _ _ _ Hr H₀ as target Hreal

assert Htarget : target = sh₁

{inversion Hreal ; subst

eapply shutdown_step_target ; eauto

subst target

destruct IHHrunproj1E.invoke_preserve_ _ _ _ _ _ _ _ _ _ _ _ _ H₀ Hr as Htail Hwf

split

+eapply P.program_next ; apply P.program_shutdown with action := action ; exact Hreal | exact Htail

+intros Hq

apply Hwf

destruct H ; simpl in * ; try exact Hq ; eapply stream_step_wf ; eauto

Conditional hi composition under the selected trusted libc contracts: exact successful entry, reached returning puts, normal shutdown calls, and an explicit completion witness at the resulting handoff. Nothing here claims that native execution supplies these witnesses or terminates.

192Theorem trusted_hi_completion

∀ specs inventory requests s₀ m₀ w₀ argc argv envp args environment fuel first s m w callfuel calltrace n s₁ m₁ w₁ tail s₂ m₂ w₂ kind status pending consumed q completed : P.host_boundary

∀s m s′ m′ w, R.safepoints m s′ m′ → entry_repspecs inventory m w → stdio_readym w → entry_repspecs inventory m′ w ∧ stdio_readym′ w

A.trusted_entry_contractentry_repspecs inventory s₀ m₀ w₀ argc argv envp args environment

program_pendingw₀ = inventory

P.M.runP.registryentry_repspecs inventory requests P.H.hi_genv P.M.Runninghi_entrym₀ fuel, s₀ w₀ first P.M.Runninghi_callm callfuel, s w

E.invokeprogram_putsentry_repspecs inventory requests site_resulthi_site site_argshi_site WPtrhi_literal s m w calltrace CallReturnWIntn s₁ m₁ w₁

normal_runspecs s₁ m₁ program_stdiow₁ mkShutdownTls 0 program_pendingw₁ [ ] program_stdoutw₁ tail s₂ m₂ w₂ mkShutdownHandedOffkind status pending consumed q

completeds₂ m₂ w₂ mkShutdownHandedOffkind status pending consumed q

P.runentry_repspecs inventory requests boundaryspecs A.trusted_host_contractcompleted P.ApplicationP.M.Runninghi_entrym₀ fuel, s₀ w₀ first ++ calltrace ++ tail ++ ProcessExitprocess_statusstatus P.Finisheds₂ m₂ w₂ mkShutdownHandedOffkind status pending consumed q

Proof 17 steps Qed

intros specs inventory requests s₀ m₀ w₀ argc argv envp args environment fuel first s m w callfuel calltrace n s₁ m₁ w₁ tail s₂ m₂ w₂ kind status pending consumed q completed Hstable Hentry Hinitial Hreach Hcall Hshutdown Hcomplete

pose proof A.trusted_entry_bodyentry_repspecs inventory s0 m0 w0 argc argv envp args environment fuel Hentry as Hbody

destruct Hentry as _ & Hr & _

assert Hclosed := reached_puts_closedspecs inventory requests _ Hstable Hbody Hr Hinitial

pose proof P.returning_puts_shutdownentry_repspecs inventory requests boundaryspecs A.trusted_host_contractcompleted P.M.Runninghi_entrym0 fuel, s0 w0 first s m w callfuel calltrace n s1 m1 w1 Hclosed Hreach Hcall as Hbridge

pose proof E.invoke_preserve_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall body_ready_ _ _ _ _ _ Hreach Hr as Hr₁ _

destruct normal_run_liftsspecs _ _ _ _ _ _ _ _ _ entry_repspecs inventory requests A.trusted_host_contractcompleted Hshutdown Hr1 as Hsegments Hwf

assert Hr₂ : R.readys2 m2

{exact P.run_ready_ _ _ _ _ _ _ Hsegments Hr1

assert Hq : stream_wfq

{apply Hwf

exact proj1proj2proj2P.C.program_invoke_continuity_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall

replace first ++ calltrace ++ tail ++ ProcessExitprocess_statusstatus with first ++ calltrace ++ tail ++ ProcessExitprocess_statusstatus by repeat rewrite app_assoc ; reflexivity

eapply P.run_trans ; exact Hbridge |

eapply P.run_trans ; exact Hsegments |

eapply P.program_next with trace := ProcessExitprocess_statusstatus tail := [ ] ; | constructor

apply A.trusted_host_completion_step ; assumption

Finite-observation safety is separate from witnessed completion. It includes unfinished/resource leaves, promises at most one exit event, and retains the shared nonfailure classification for application stops. It does not establish native coverage of the outer relation.

245Theorem trusted_hi_observations

∀ specs inventory requests completed s m w argc argv envp args environment fuel trace last

∀s m s′ m′ w, R.safepoints m s′ m′ → entry_repspecs inventory m w → stdio_readym w → entry_repspecs inventory m′ w ∧ stdio_readym′ w

A.trusted_entry_contractentry_repspecs inventory s m w argc argv envp args environment

P.runentry_repspecs inventory requests boundaryspecs A.trusted_host_contractcompleted P.ApplicationP.M.Runninghi_entrym fuel, s w trace last

P.runtime_readylast ∧ P.exit_counttrace ≤ 1%nat ∧ ∀why ms w′, last = P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

Explore proof 9 tactics

Initial goal

⊢

∀specs : segments inventory : listregistration requests : listword → mem → stdio_world → Z → Z → Prop completed : A.P.host_boundary s : R.state m : mem w : program_world argc : Z argv envp : ptr args environment : listlistZ fuel : Z trace : listevent last : P.state, ∀s₀ : R.state m₀ : mem s′ : R.state m′ : mem w₀ : stdio_world, R.safepoints₀ m₀ s′ m′ → entry_repspecs inventory m₀ w₀ → stdio_readym₀ w₀ → entry_repspecs inventory m′ w₀ ∧ stdio_readym′ w₀ → A.trusted_entry_contractentry_repspecs inventory s m w argc argv envp args environment → P.runentry_repspecs inventory requests boundaryspecs A.trusted_host_contractcompleted P.ApplicationP.M.Runninghi_entrym fuel, s w trace last → P.runtime_readylast ∧ P.exit_counttrace ≤ 1%nat ∧ ∀why : ending ms : P.M.P.I.RM.mstate w′ : program_world, last = P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

intros specs inventory requests completed s m w argc argv envp args environment fuel trace last Hstable Hentry Hrun

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

completed :

s :

R.state

m :

w :

argc :

argv, envp :

args, environment :

listlistZ

fuel :

trace :

listevent

last :

P.state

Hstable :

Hentry :

A.trusted_entry_contractentry_repspecs inventory s m w argc argv envp args environment

Hrun :

P.runentry_repspecs inventory requests boundaryspecs A.trusted_host_contractcompleted P.ApplicationP.M.Runninghi_entrym fuel, s w trace last

⊢

P.runtime_readylast ∧ P.exit_counttrace ≤ 1%nat ∧ ∀why : ending ms : P.M.P.I.RM.mstate w′ : program_world, last = P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

pose proof A.trusted_entry_bodyentry_repspecs inventory s m w argc argv envp args environment fuel Hentry as Hbody

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

completed :

s :

R.state

m :

w :

argc :

argv, envp :

args, environment :

listlistZ

fuel :

trace :

listevent

last :

P.state

Hstable :

Hentry :

A.trusted_entry_contractentry_repspecs inventory s m w argc argv envp args environment

Hrun :

P.runentry_repspecs inventory requests boundaryspecs A.trusted_host_contractcompleted P.ApplicationP.M.Runninghi_entrym fuel, s w trace last

Hbody :

A.P.body_inventry_repspecs inventory A.P.M.Runninghi_entrym fuel, s w

⊢

P.runtime_readylast ∧ P.exit_counttrace ≤ 1%nat ∧ ∀why : ending ms : P.M.P.I.RM.mstate w′ : program_world, last = P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

destruct Hentry as _ & Hr & _

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

completed :

s :

R.state

m :

w :

argc :

argv, envp :

args, environment :

listlistZ

fuel :

trace :

listevent

last :

P.state

Hstable :

Hr :

R.readys m

Hrun :

P.runentry_repspecs inventory requests boundaryspecs A.trusted_host_contractcompleted P.ApplicationP.M.Runninghi_entrym fuel, s w trace last

Hbody :

A.P.body_inventry_repspecs inventory A.P.M.Runninghi_entrym fuel, s w

⊢

P.runtime_readylast ∧ P.exit_counttrace ≤ 1%nat ∧ ∀why : ending ms : P.M.P.I.RM.mstate w′ : program_world, last = P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

split ; eapply P.run_ready ; eauto |

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

completed :

s :

R.state

m :

w :

argc :

argv, envp :

args, environment :

listlistZ

fuel :

trace :

listevent

last :

P.state

Hstable :

Hr :

R.readys m

Hrun :

P.runentry_repspecs inventory requests boundaryspecs A.trusted_host_contractcompleted P.ApplicationP.M.Runninghi_entrym fuel, s w trace last

Hbody :

A.P.body_inventry_repspecs inventory A.P.M.Runninghi_entrym fuel, s w

⊢

P.exit_counttrace ≤ 1%nat ∧ ∀why : ending ms : P.M.P.I.RM.mstate w′ : program_world, last = P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

split

2 open

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

completed :

s :

R.state

m :

w :

argc :

argv, envp :

args, environment :

listlistZ

fuel :

trace :

listevent

last :

P.state

Hstable :

Hr :

R.readys m

Hrun :

P.runentry_repspecs inventory requests boundaryspecs A.trusted_host_contractcompleted P.ApplicationP.M.Runninghi_entrym fuel, s w trace last

Hbody :

A.P.body_inventry_repspecs inventory A.P.M.Runninghi_entrym fuel, s w

⊢

P.exit_counttrace ≤ 1%nat

focused goal

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

completed :

s :

R.state

m :

w :

argc :

argv, envp :

args, environment :

listlistZ

fuel :

trace :

listevent

last :

P.state

Hstable :

Hr :

R.readys m

Hrun :

P.runentry_repspecs inventory requests boundaryspecs A.trusted_host_contractcompleted P.ApplicationP.M.Runninghi_entrym fuel, s w trace last

Hbody :

A.P.body_inventry_repspecs inventory A.P.M.Runninghi_entrym fuel, s w

⊢

∀why : ending ms : P.M.P.I.RM.mstate w′ : program_world, last = P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

–eapply P.at_most_one_exit ; eauto

deferred goal

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

completed :

s :

R.state

m :

w :

argc :

argv, envp :

args, environment :

listlistZ

fuel :

trace :

listevent

last :

P.state

Hstable :

Hr :

R.readys m

Hrun :

P.runentry_repspecs inventory requests boundaryspecs A.trusted_host_contractcompleted P.ApplicationP.M.Runninghi_entrym fuel, s w trace last

Hbody :

A.P.body_inventry_repspecs inventory A.P.M.Runninghi_entrym fuel, s w

⊢

∀why : ending ms : P.M.P.I.RM.mstate w′ : program_world, last = P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

–intros why ms w′ →

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

completed :

s :

R.state

m :

w :

argc :

argv, envp :

args, environment :

listlistZ

fuel :

trace :

listevent

Hstable :

Hr :

R.readys m

why :

ending

ms :

P.M.P.I.RM.mstate

w′ :

Hrun :

P.runentry_repspecs inventory requests boundaryspecs A.trusted_host_contractcompleted P.ApplicationP.M.Runninghi_entrym fuel, s w trace P.ApplicationP.M.Stoppedwhy ms w′

Hbody :

A.P.body_inventry_repspecs inventory A.P.M.Runninghi_entrym fuel, s w

⊢

¬failure_endingwhy

eapply P.application_stopped_never_panics ; eauto

specs :

inventory :

requests :

listword → mem → stdio_world → Z → Z → Prop

completed :

s :

R.state

m :

w :

argc :

argv, envp :

args, environment :

listlistZ

fuel :

trace :

listevent

Hstable :

Hr :

R.readys m

why :

ending

ms :

P.M.P.I.RM.mstate

w′ :

Hrun :

P.runentry_repspecs inventory requests boundaryspecs A.trusted_host_contractcompleted P.ApplicationP.M.Runninghi_entrym fuel, s w trace P.ApplicationP.M.Stoppedwhy ms w′

Hbody :

A.P.body_inventry_repspecs inventory A.P.M.Runninghi_entrym fuel, s w

⊢

P.application_safeentry_repspecs inventory P.ApplicationP.M.Runninghi_entrym fuel, s w

exact Hbody

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros specs inventory requests completed s m w argc argv envp args environment fuel trace last Hstable Hentry Hrun

pose proof A.trusted_entry_bodyentry_repspecs inventory s m w argc argv envp args environment fuel Hentry as Hbody

destruct Hentry as _ & Hr & _

split ; eapply P.run_ready ; eauto |

split

–eapply P.at_most_one_exit ; eauto

–intros why ms w′ →

eapply P.application_stopped_never_panics ; eauto

exact Hbody

Logical instances exercise admission and cutpoints, not native libc. In particular the named callback below is a fixture, not an assertion that arbitrary user callbacks belong to the trusted libc boundary.

269Module SelectedChecks

270Module S ≔ Selected InterpRuntime

271Module P ≔ S.P

One admitted callback retains an actual readable object capability.

274Definition callback_validm : mem entry : registration : Prop ≔

registration_callbackentry = OnExitTAtom"fixture_cleanup" WPtrmkPtr3072 Obj3072 ∧ access_resm 3072 Obj3072 8 Read 8 = Someok

The pending inventory and currently running callback need valid arguments; consumed history alone does not retain dead argument objects.

281Definition callbacks_validm sh : Prop ≔

Forallcallback_validm shutdown_pendingsh

∧

match shutdown_atsh with

InCallbackactive

⇒

callback_validm active

⇒

True

Selection of a new registration is checked independently of token freshness.

286Definition action_selectedm action : shutdown_action : Prop ≔

match action with

InvokeCallbackentry _ | RegisterCallbackentry

⇒

callback_validm entry

⇒

True

A memory-backed fixture with separate readable argument and writable stdout roots. Neither root may be released; no allocations are authorized.

294Definition specs: S.segments ≔

S.mkSegmentsλm w sh ⇒ fixture_repm w ∧ callbacks_validm sh ∧ stream_wfshutdown_stdoutsh ∧ shutdown_uniquesh λm _ _ action ⇒ action_selectedm action λ_ _ _ _ ⇒ stdout_span; mkSpanmkPtr3072 Obj3072 8 λ_ _ _ _ ⇒ stdout_span λ_ _ _ _ ⇒ [ ] λ_ _ _ _ _ _ ⇒ False λ_ _ _ w _ _ _ w′ ⇒ w′ = w λ_ _ ⇒ puts_panic

A nonempty inventory, with a retained capability rather than an integer address.

306Definition entry: registration ≔

mkRegistration0 OnExitTAtom"fixture_cleanup" WPtrmkPtr3072 Obj3072

2 open

q :

Hwf :

⊢

callbacks_validhello_mem shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q

focused goal

q :

Hwf :

⊢

stream_wfshutdown_stdoutshutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q ∧ shutdown_uniqueshutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q

–split ; | exact I

2 open

q :

Hwf :

⊢

Forallcallback_validhello_mem shutdown_pendingshutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q

deferred goal

q :

Hwf :

⊢

constructor ; split ; reflexivity | constructor

deferred goal

q :

Hwf :

⊢

–split ; exact Hwf |

q :

Hwf :

⊢

shutdown_uniqueshutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q

repeat constructor

q :

Hwf :

⊢

¬Inregistration_tokenentry [ ]

simpl

q :

Hwf :

⊢

¬False

tauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros q Hwf

split ; split ; reflexivity |

split

–split ; | exact I

constructor ; split ; reflexivity | constructor

–split ; exact Hwf |

repeat constructor

simpl

tauto

Change only behavioral coverage: the same valid, selected source keeps its ABI/preconditions, permissions and post, but has no possible prefix. This is not a pinned native instance or a safe implementation.

320Definition uncovered_specs: S.segments ≔

S.mkSegmentsS.libc_validspecs S.selected_actionspecs S.segment_sourcesspecs S.segment_writesspecs S.segment_releasesspecs S.segment_requestsspecs λ_ _ _ _ _ _ _ _ ⇒ False S.segment_panicsspecs

Independent admission survives deleting every behavior. Thus neither admission nor absence of invocations can establish native coverage.

327Example admitted_without_behavior: let sh ≔ mkShutdownHandlers 0 entry [ ] stdout_initial in let action ≔ InvokeCallbackentry 0 in P.shutdown_admissibleS.boundaryuncovered_specs InterpRuntime.start hello_mem hello_world sh action ∧ ∀born trace s′ m′ w′, ¬S.E.prefixS.selected_contractuncovered_specs sh action [ ] InterpRuntime.start hello_mem hello_world born trace s′ m′ w′ ∧ ∀trace ending s′ m′ w′, ¬S.E.invokeS.selected_contractuncovered_specs sh action CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world trace ending s′ m′ w′

Explore proof 14 tactics

Initial goal

⊢

let sh ≔ shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial in

let action ≔ InvokeCallbackentry 0 in

P.shutdown_admissibleS.boundaryuncovered_specs InterpRuntime.start hello_mem hello_world sh action ∧ ∀born : listZ trace : listevent s′ : InterpRuntime.state m′ : mem w′ : stdio_world, ¬S.E.prefixS.selected_contractuncovered_specs sh action [ ] InterpRuntime.start hello_mem hello_world born trace s′ m′ w′ ∧ ∀trace : listevent ending : call_end s′ : InterpRuntime.state m′ : mem w′ : stdio_world, ¬S.E.invokeS.selected_contractuncovered_specs sh action CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world trace ending s′ m′ w′

intros sh action

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

⊢

assert Hnone : ∀born trace s′ m′ w′, ¬S.E.prefixS.selected_contractuncovered_specs sh action [ ] InterpRuntime.start hello_mem hello_world born trace s′ m′ w′

2 open

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

⊢

focused goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

{intros born trace s′ m′ w′ _ Hfalse

2 open

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

born :

listZ

trace :

listevent

s′ :

m′ :

w′ :

Hfalse :

contract_prefixS.selected_contractuncovered_specs sh action [ ] hello_mem hello_world born trace m′ w′

⊢

False

deferred goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

exact Hfalse

deferred goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

split

2 open

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

P.shutdown_admissibleS.boundaryuncovered_specs InterpRuntime.start hello_mem hello_world sh action

focused goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

∀born : listZ trace : listevent s′ : InterpRuntime.state m′ : mem w′ : stdio_world, ¬S.E.prefixS.selected_contractuncovered_specs sh action [ ] InterpRuntime.start hello_mem hello_world born trace s′ m′ w′ ∧ ∀trace : listevent ending : call_end s′ : InterpRuntime.state m′ : mem w′ : stdio_world, ¬S.E.invokeS.selected_contractuncovered_specs sh action CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world trace ending s′ m′ w′

–eapply S.selected_admits

5 open

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

S.selected_readyuncovered_specs InterpRuntime.start hello_mem hello_world sh

Hnone :

⊢

focused goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

S.selected_actionuncovered_specs hello_mem hello_world sh action

focused goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

shutdown_stepsh action ?full

deferred goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

shelved goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

+split ; apply hello_ready ; split ; vm_compute ; congruence |

5 open

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

S.libc_validuncovered_specs hello_mem hello_world sh

Hnone :

⊢

deferred goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

S.selected_actionuncovered_specs hello_mem hello_world sh action

deferred goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

shutdown_stepsh action ?full

deferred goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

shelved goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

exact nonempty_entrystdout_initial stdout_initial_wf

4 open

deferred goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

S.selected_actionuncovered_specs hello_mem hello_world sh action

deferred goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

shutdown_stepsh action ?full

deferred goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

shelved goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

+split ; reflexivity

3 open

deferred goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

shutdown_stepsh action ?full

deferred goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

shelved goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

+constructor

deferred goal

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

–split ; exact Hnone |

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

⊢

∀trace : listevent ending : call_end s′ : InterpRuntime.state m′ : mem w′ : stdio_world, ¬S.E.invokeS.selected_contractuncovered_specs sh action CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world trace ending s′ m′ w′

intros trace ending s′ m′ w′ Hcall

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

trace :

listevent

ending :

s′ :

m′ :

w′ :

Hcall :

S.E.invokeS.selected_contractuncovered_specs sh action CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world trace ending s′ m′ w′

⊢

False

destruct S.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born Hprefix

sh :=

shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial : shutdown_state

action :=

Hnone :

trace :

listevent

ending :

s′ :

m′ :

w′ :

Hcall :

S.E.invokeS.selected_contractuncovered_specs sh action CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world trace ending s′ m′ w′

born :

listZ

Hprefix :

S.E.prefixS.selected_contractuncovered_specs sh action [ ] InterpRuntime.start hello_mem hello_world born trace s′ m′ w′

⊢

False

exact Hnoneborn trace s′ m′ w′ Hprefix

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros sh action

assert Hnone : ∀born trace s′ m′ w′, ¬S.E.prefixS.selected_contractuncovered_specs sh action [ ] InterpRuntime.start hello_mem hello_world born trace s′ m′ w′

{intros born trace s′ m′ w′ _ Hfalse

exact Hfalse

split

–eapply S.selected_admits

+split ; apply hello_ready ; split ; vm_compute ; congruence |

exact nonempty_entrystdout_initial stdout_initial_wf

+split ; reflexivity

+constructor

–split ; exact Hnone |

intros trace ending s′ m′ w′ Hcall

destruct S.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born Hprefix

exact Hnoneborn trace s′ m′ w′ Hprefix

A fresh token cannot authorize an unknown callback, even where the logical register rule permits it. No invocation witness is needed for rejection.

357Example unknown_callback_rejected: ∀s, let sh ≔ mkShutdownInCallbackentry 0 [ ] 0%nat stdout_initial in let unknown ≔ mkRegistration1 AtExitTAtom"unknown" in ¬P.shutdown_admissibleS.boundaryspecs s hello_mem hello_world sh RegisterCallbackunknown

Explore proof 2 tactics

Initial goal

⊢

∀ s : InterpRuntime.state ,

let sh ≔ shutdown_at ≔ InCallbackentry; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 0%nat; shutdown_stdout ≔ stdout_initial in

let unknown ≔ registration_token ≔ 1; registration_callback ≔ AtExitTAtom"unknown" in

¬P.shutdown_admissibleS.boundaryspecs s hello_mem hello_world sh RegisterCallbackunknown

intros s sh unknown _ _ _ Hname _ _

s :

sh :=

shutdown_at ≔ InCallbackentry; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 0%nat; shutdown_stdout ≔ stdout_initial : shutdown_state

unknown :=

registration_token ≔ 1; registration_callback ≔ AtExitTAtom"unknown" : registration

Hname :

registration_callbackunknown = OnExitTAtom"fixture_cleanup" WPtrptr_addr ≔ 3072; ptr_cap ≔ Obj3072

⊢

False

discriminate Hname

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros s sh unknown _ _ _ Hname _ _

discriminate Hname

Keeping the token and address while losing the retained capability's live bounds invalidates the entry, rather than silently removing its behavior.

367Example expired_argument_rejected: ∀s, let dead ≔ mkMemm_byteshello_mem mkRegion1024 1030 GlobalData Live; mkRegion2048 2064 Heap Live; mkRegion3072 3072 Heap Freed m_auxhello_mem in ¬P.shutdown_admissibleS.boundaryspecs s dead hello_world mkShutdownHandlers 0 entry [ ] stdout_initial InvokeCallbackentry 0

Explore proof 2 tactics

Initial goal

⊢

∀ s : InterpRuntime.state ,

let dead ≔ m_bytes ≔ m_byteshello_mem; m_regions ≔ r_base ≔ 1024; r_end ≔ 1030; r_kind ≔ GlobalData; r_life ≔ Live; r_base ≔ 2048; r_end ≔ 2064; r_kind ≔ Heap; r_life ≔ Live; r_base ≔ 3072; r_end ≔ 3072; r_kind ≔ Heap; r_life ≔ Freed; m_aux ≔ m_auxhello_mem in

¬P.shutdown_admissibleS.boundaryspecs s dead hello_world shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial InvokeCallbackentry 0

intros s dead _ _ _ _ Hread _

s :

dead :=

m_bytes ≔ m_byteshello_mem; m_regions ≔ r_base ≔ 1024; r_end ≔ 1030; r_kind ≔ GlobalData; r_life ≔ Live; r_base ≔ 2048; r_end ≔ 2064; r_kind ≔ Heap; r_life ≔ Live; r_base ≔ 3072; r_end ≔ 3072; r_kind ≔ Heap; r_life ≔ Freed; m_aux ≔ m_auxhello_mem : mem

Hread :

access_resdead 3072 Obj3072 8 Read 8 = Someok

⊢

False

discriminate Hread

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros s dead _ _ _ _ Hread _

discriminate Hread

A selected segment really has no release ownership, even of its readable callback argument. Reuse the existing asymmetric footprint regression.

379Example argument_release_rejected: ¬local_effectS.segment_sourcesspecs mkShutdownTls 0 entry [ ] stdout_initial EmptyTls hello_mem hello_world S.segment_writesspecs mkShutdownTls 0 entry [ ] stdout_initial EmptyTls hello_mem hello_world S.segment_releasesspecs mkShutdownTls 0 entry [ ] stdout_initial EmptyTls hello_mem hello_world [ ] hello_mem mkMemm_byteshello_mem mkRegion1024 1030 GlobalData Live; mkRegion2048 2064 Heap Live; mkRegion3072 3072 Heap Freed m_auxhello_mem

Explore proof 5 tactics

Initial goal

r_base ≔ 3072; r_end ≔ 3072; r_kind ≔ Heap; r_life ≔ Freed = r_base ≔ 3072; r_end ≔ 3080; r_kind ≔ Heap; r_life ≔ Live

⊢

False

discriminate H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros _ & Hr & _

destruct Hr3072 mkRegion3072 3072 Heap Freed eq_refl as reg & Hreg & H | & _

change SomemkRegion3072 3080 Heap Live = Somereg in Hreg

injection Hreg as ←

discriminate H

Read authority for the argument is not write authority for its bytes.

396Example argument_write_rejected: ¬local_effectS.segment_sourcesspecs mkShutdownTls 0 entry [ ] stdout_initial EmptyTls hello_mem hello_world S.segment_writesspecs mkShutdownTls 0 entry [ ] stdout_initial EmptyTls hello_mem hello_world [ ] [ ] hello_mem store_byteshello_mem 3072 1 7

Explore proof 5 tactics

Initial goal

⊢

intros _ & _ & Hw & _

Hw :

∀a : Z, ¬write_authorityS.segment_writesspecs shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial EmptyTls hello_mem hello_world [ ] hello_mem a → m_bytesstore_byteshello_mem 3072 1 7 a = m_byteshello_mem a ∧ m_auxstore_byteshello_mem 3072 1 7 a = m_auxhello_mem a

⊢

False

assert Hn : ¬write_authoritystdout_span [ ] hello_mem 3072

2 open

Hw :

⊢

focused goal

Hw :

Hn :

⊢

False

{intros root & ← | & _ & Hin | base & reg & & _ ; unfold span_contains in Hin ; simpl in Hin ; lia

deferred goal

Hw :

Hn :

⊢

False

destruct Hw_ Hn as Hb _

Hw :

Hn :

Hb :

m_bytesstore_byteshello_mem 3072 1 7 3072 = m_byteshello_mem 3072

⊢

False

discriminate Hb

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros _ & _ & Hw & _

assert Hn : ¬write_authoritystdout_span [ ] hello_mem 3072

{intros root & ← | & _ & Hin | base & reg & & _ ; unfold span_contains in Hin ; simpl in Hin ; lia

destruct Hw_ Hn as Hb _

discriminate Hb

An identity-memory fixture completes a selected, independently admissible logical action. Its full invocation—not merely a prefix—supplies the post.

411Lemma fixture_invocation

∀ m w sh action sh′

action_selectedm action

shutdown_stepsh action sh′

S.libc_validspecs m w sh′

S.E.invokeS.selected_contractspecs sh action CVoid [ ] [ ] InterpRuntime.start m w P.action_eventsaction CallReturn[ ] InterpRuntime.start m w

Explore proof 20 tactics

Initial goal

⊢

∀m : mem w : stdio_world sh : shutdown_state action : shutdown_action sh′ : shutdown_state, S.libc_validspecs m w sh → action_selectedm action → shutdown_stepsh action sh′ → S.libc_validspecs m w sh′ → S.E.invokeS.selected_contractspecs sh action CVoid [ ] [ ] InterpRuntime.start m w P.action_eventsaction CallReturn[ ] InterpRuntime.start m w

intros m w sh action sh′ Hvalid Hselect Hstep Hvalid′

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

S.E.invokeS.selected_contractspecs sh action CVoid [ ] [ ] InterpRuntime.start m w P.action_eventsaction CallReturn[ ] InterpRuntime.start m w

eapply S.E.invoke_normal with born := [ ]

7 open

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

contract_abiS.selected_contractspecs sh action CVoid [ ]

focused goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

contract_preS.selected_contractspecs sh action [ ] m w

focused goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

S.E.prefixS.selected_contractspecs sh action [ ] InterpRuntime.start m w [ ] P.action_eventsaction InterpRuntime.start m w

focused goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

contract_postS.selected_contractspecs sh action [ ] m w [ ] P.action_eventsaction CallReturn[ ] m w

focused goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀why : reason, CallReturn[ ] ≠ CallResourcewhy

focused goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsS.selected_contractspecs sh action values ∧ Forallword_authoritycontract_sourcesS.selected_contractspecs sh action [ ] m w [ ] m values

focused goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

–split ; reflexivity

6 open

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

contract_preS.selected_contractspecs sh action [ ] m w

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

S.E.prefixS.selected_contractspecs sh action [ ] InterpRuntime.start m w [ ] P.action_eventsaction InterpRuntime.start m w

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

contract_postS.selected_contractspecs sh action [ ] m w [ ] P.action_eventsaction CallReturn[ ] m w

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀why : reason, CallReturn[ ] ≠ CallResourcewhy

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

–split ; reflexivity |

6 open

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

S.libc_validspecs m w sh ∧ S.selected_actionspecs m w sh action ∧ ∃full : shutdown_state, shutdown_stepsh action full

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

S.E.prefixS.selected_contractspecs sh action [ ] InterpRuntime.start m w [ ] P.action_eventsaction InterpRuntime.start m w

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

contract_postS.selected_contractspecs sh action [ ] m w [ ] P.action_eventsaction CallReturn[ ] m w

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀why : reason, CallReturn[ ] ≠ CallResourcewhy

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

split ; exact Hvalid |

6 open

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

S.selected_actionspecs m w sh action ∧ ∃full : shutdown_state, shutdown_stepsh action full

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

S.E.prefixS.selected_contractspecs sh action [ ] InterpRuntime.start m w [ ] P.action_eventsaction InterpRuntime.start m w

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

contract_postS.selected_contractspecs sh action [ ] m w [ ] P.action_eventsaction CallReturn[ ] m w

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀why : reason, CallReturn[ ] ≠ CallResourcewhy

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

split ; exact Hselect |

6 open

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∃full : shutdown_state, shutdown_stepsh action full

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

S.E.prefixS.selected_contractspecs sh action [ ] InterpRuntime.start m w [ ] P.action_eventsaction InterpRuntime.start m w

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

contract_postS.selected_contractspecs sh action [ ] m w [ ] P.action_eventsaction CallReturn[ ] m w

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀why : reason, CallReturn[ ] ≠ CallResourcewhy

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

exists sh′

6 open

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

shutdown_stepsh action sh′

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

S.E.prefixS.selected_contractspecs sh action [ ] InterpRuntime.start m w [ ] P.action_eventsaction InterpRuntime.start m w

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

contract_postS.selected_contractspecs sh action [ ] m w [ ] P.action_eventsaction CallReturn[ ] m w

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀why : reason, CallReturn[ ] ≠ CallResourcewhy

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

exact Hstep

5 open

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

S.E.prefixS.selected_contractspecs sh action [ ] InterpRuntime.start m w [ ] P.action_eventsaction InterpRuntime.start m w

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

contract_postS.selected_contractspecs sh action [ ] m w [ ] P.action_eventsaction CallReturn[ ] m w

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀why : reason, CallReturn[ ] ≠ CallResourcewhy

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

–split ; constructor | reflexivity

4 open

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

contract_postS.selected_contractspecs sh action [ ] m w [ ] P.action_eventsaction CallReturn[ ] m w

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀why : reason, CallReturn[ ] ≠ CallResourcewhy

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

–split ; reflexivity |

4 open

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∃sh'₀ : shutdown_state, S.segment_finishspecs sh action P.action_eventsaction m w sh'₀

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀why : reason, CallReturn[ ] ≠ CallResourcewhy

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

exists sh′

4 open

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

S.segment_finishspecs sh action P.action_eventsaction m w sh′

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀why : reason, CallReturn[ ] ≠ CallResourcewhy

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

split ; exact Hstep |

4 open

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

P.action_eventsaction = S.P.action_eventsaction ∧ S.libc_validspecs m w sh′

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀why : reason, CallReturn[ ] ≠ CallResourcewhy

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

auto

3 open

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀why : reason, CallReturn[ ] ≠ CallResourcewhy

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

–intros why Hbad

3 open

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

why :

reason

Hbad :

CallReturn[ ] = CallResourcewhy

⊢

False

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

discriminate Hbad

2 open

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

–intros values Heq

2 open

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

values :

listword

Heq :

CallReturn[ ] = CallReturnvalues

⊢

return_shapecontract_returnsS.selected_contractspecs sh action values ∧ Forallword_authoritycontract_sourcesS.selected_contractspecs sh action [ ] m w [ ] m values

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

injection Heq as ←

2 open

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

return_shapecontract_returnsS.selected_contractspecs sh action [ ] ∧ Forallword_authoritycontract_sourcesS.selected_contractspecs sh action [ ] m w [ ] m [ ]

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

split ; constructor

deferred goal

m :

w :

sh :

action :

sh′ :

Hvalid :

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

⊢

∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

–intros status Hbad

m :

w :

sh :

action :

sh′ :

Hvalid :

action_selectedhello_mem InvokeCallbackentry 0

Hselect :

action_selectedm action

Hstep :

shutdown_stepsh action sh′

Hvalid′ :

S.libc_validspecs m w sh′

status :

Hbad :

CallReturn[ ] = CallExitstatus

⊢

∃before : listevent, P.action_eventsaction = before ++ ProcessExitstatus

discriminate Hbad

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros m w sh action sh′ Hvalid Hselect Hstep Hvalid′

eapply S.E.invoke_normal with born := [ ]

–split ; reflexivity

–split ; reflexivity |

split ; exact Hvalid |

split ; exact Hselect |

exists sh′

exact Hstep

–split ; constructor | reflexivity

–split ; reflexivity |

exists sh′

split ; exact Hstep |

auto

–intros why Hbad

discriminate Hbad

–intros values Heq

injection Heq as ←

split ; constructor

–intros status Hbad

discriminate Hbad

The adapter's successful-invocation theorem is inhabited with a nonempty admitted inventory and retains the active callback's readable argument.

431Example nonempty_callback_realizes: ∃target, P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world mkShutdownHandlers 0 entry [ ] stdout_initial InvokeCallbackentry 0 [ ] InterpRuntime.start hello_mem hello_world target

Explore proof 12 tactics

Initial goal

⊢

∃target : shutdown_state, P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial InvokeCallbackentry 0 [ ] InterpRuntime.start hello_mem hello_world target

apply S.invocation_realizes ; apply hello_ready ; split ; vm_compute ; congruence |

⊢

S.E.invokeS.selected_contractspecs shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial InvokeCallbackentry 0 CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

eapply fixture_invocation with sh′ := mkShutdownInCallbackentry 0 [ ] 0%nat stdout_initial

4 open

⊢

S.libc_validspecs hello_mem hello_world shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial

focused goal

⊢

focused goal

⊢

shutdown_stepshutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ stdout_initial InvokeCallbackentry 0 shutdown_at ≔ InCallbackentry; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 0%nat; shutdown_stdout ≔ stdout_initial

focused goal

⊢

S.libc_validspecs hello_mem hello_world shutdown_at ≔ InCallbackentry; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 0%nat; shutdown_stdout ≔ stdout_initial

–exact nonempty_entrystdout_initial stdout_initial_wf

3 open

deferred goal

⊢

action_selectedhello_mem InvokeCallbackentry 0

deferred goal

⊢

deferred goal

⊢

S.libc_validspecs hello_mem hello_world shutdown_at ≔ InCallbackentry; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 0%nat; shutdown_stdout ≔ stdout_initial

–split ; reflexivity

2 open

deferred goal

⊢

deferred goal

⊢

S.libc_validspecs hello_mem hello_world shutdown_at ≔ InCallbackentry; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 0%nat; shutdown_stdout ≔ stdout_initial

–constructor

deferred goal

⊢

S.libc_validspecs hello_mem hello_world shutdown_at ≔ InCallbackentry; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 0%nat; shutdown_stdout ≔ stdout_initial

–split ; split ; reflexivity |

⊢

callbacks_validhello_mem shutdown_at ≔ InCallbackentry; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 0%nat; shutdown_stdout ≔ stdout_initial ∧ stream_wfshutdown_stdoutshutdown_at ≔ InCallbackentry; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 0%nat; shutdown_stdout ≔ stdout_initial ∧ shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 0%nat; shutdown_stdout ≔ stdout_initial

split

2 open

⊢

callbacks_validhello_mem shutdown_at ≔ InCallbackentry; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 0%nat; shutdown_stdout ≔ stdout_initial

focused goal

⊢

stream_wfshutdown_stdoutshutdown_at ≔ InCallbackentry; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 0%nat; shutdown_stdout ≔ stdout_initial ∧ shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 0%nat; shutdown_stdout ≔ stdout_initial

+split ; constructor | split ; reflexivity

deferred goal

⊢

+split ; exact stdout_initial_wf |

⊢

shutdown_uniqueshutdown_at ≔ InCallbackentry; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 0%nat; shutdown_stdout ≔ stdout_initial

repeat constructor

⊢

¬In0%nat mapregistration_token shutdown_pendingshutdown_at ≔ InCallbackentry; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ 0%nat; shutdown_stdout ≔ stdout_initial

simpl

⊢

¬False

tauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

apply S.invocation_realizes ; apply hello_ready ; split ; vm_compute ; congruence |

eapply fixture_invocation with sh′ := mkShutdownInCallbackentry 0 [ ] 0%nat stdout_initial

–exact nonempty_entrystdout_initial stdout_initial_wf

–split ; reflexivity

–constructor

–split ; split ; reflexivity |

split

+split ; constructor | split ; reflexivity

+split ; exact stdout_initial_wf |

repeat constructor

simpl

tauto

Valid completed cleanup cutpoints retain the same memory and consumed inventory while output obligations evolve. No terminal leaf is resumed.

449Definition cleanupq : stream_state : shutdown_state ≔

mkShutdownCleanup 0 [ ] 0%nat q

All well-formed fixture cleanup snapshots satisfy the logical post.

452Lemma cleanup_valid

∀ q

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros q Hwf

split ; split ; reflexivity |

split ; split ; constructor |

split ; exact Hwf |

repeat constructor

simpl

tauto

Each completed cutpoint comes from a real contract invocation.

459Lemma cleanup_realized

∀ q action q′

∀bytes, action ≠ Acceptbytes

stream_stepq action q′

P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world cleanupq′

Explore proof 25 tactics

Initial goal

⊢

∀q : stream_state action : stream_action q′ : stream_state, ∀bytes : listZ, action ≠ Acceptbytes → stream_stepq action q′ → stream_wfq → P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world cleanupq′

intros q action q′ Hnot Hstream Hwf

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

⊢

P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world cleanupq′

assert Hstep : shutdown_stepcleanupq ShutdownOutputaction cleanupq′ by apply shutdown_cleanup_output ; assumption

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

⊢

P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world cleanupq′

assert Hcall := fixture_invocationhello_mem hello_world cleanupq ShutdownOutputaction cleanupq′ cleanup_valid_ Hwf I Hstep cleanup_valid_ stream_step_wf_ _ _ Hstream Hwf

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world P.action_eventsShutdownOutputaction CallReturn[ ] InterpRuntime.start hello_mem hello_world

⊢

P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world cleanupq′

assert Hevents : P.action_eventsShutdownOutputaction = [ ]

2 open

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

⊢

P.action_eventsShutdownOutputaction = [ ]

focused goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

Hevents :

P.action_eventsShutdownOutputaction = [ ]

⊢

P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world cleanupq′

{destruct action ; try reflexivity

2 open

q :

bytes :

listZ

q′ :

Hnot :

∀bytes₀ : listZ, Acceptbytes ≠ Acceptbytes₀

Hstream :

stream_stepq Acceptbytes q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputAcceptbytes cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputAcceptbytes CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world P.action_eventsShutdownOutputAcceptbytes CallReturn[ ] InterpRuntime.start hello_mem hello_world

⊢

P.action_eventsShutdownOutputAcceptbytes = [ ]

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

Hevents :

P.action_eventsShutdownOutputaction = [ ]

⊢

P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world cleanupq′

exfalso

2 open

q :

bytes :

listZ

q′ :

Hnot :

∀bytes₀ : listZ, Acceptbytes ≠ Acceptbytes₀

Hstream :

stream_stepq Acceptbytes q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputAcceptbytes cleanupq′

Hcall :

⊢

False

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

Hevents :

P.action_eventsShutdownOutputaction = [ ]

⊢

P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world cleanupq′

apply Hnotbytes

2 open

q :

bytes :

listZ

q′ :

Hnot :

∀bytes₀ : listZ, Acceptbytes ≠ Acceptbytes₀

Hstream :

stream_stepq Acceptbytes q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputAcceptbytes cleanupq′

Hcall :

⊢

Acceptbytes = Acceptbytes

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

Hevents :

P.action_eventsShutdownOutputaction = [ ]

⊢

P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world cleanupq′

reflexivity

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

Hevents :

P.action_eventsShutdownOutputaction = [ ]

⊢

P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world cleanupq′

rewrite Hevents in Hcall

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

⊢

P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world cleanupq′

destruct S.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born Hprefix

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

⊢

P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world cleanupq′

assert Hr := hello_readyInterpRuntime.start ltac:split ; vm_compute ; congruence

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world cleanupq′

eapply P.realize_action with born := born

7 open

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

focused goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

P.shutdown_readyS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq

⊢

focused goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

P.shutdown_admissibleS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq ShutdownOutputaction

focused goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

P.M.E.prefixP.action_contractS.boundaryspecs cleanupq ShutdownOutputaction P.action_wordsS.boundaryspecs cleanupq ShutdownOutputaction InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

focused goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

P.action_postS.boundaryspecs cleanupq ShutdownOutputaction InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world cleanupq′

focused goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

[ ] = P.action_eventsShutdownOutputaction

focused goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

P.shutdown_readyS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq′

⊢

–exact Hstep

6 open

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

P.shutdown_readyS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq

⊢

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

P.shutdown_admissibleS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq ShutdownOutputaction

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

P.action_postS.boundaryspecs cleanupq ShutdownOutputaction InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world cleanupq′

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

[ ] = P.action_eventsShutdownOutputaction

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

P.shutdown_readyS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq′

⊢

–split ; exact Hr | apply cleanup_valid ; exact Hwf

5 open

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

P.shutdown_admissibleS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq ShutdownOutputaction

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

P.action_postS.boundaryspecs cleanupq ShutdownOutputaction InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world cleanupq′

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

[ ] = P.action_eventsShutdownOutputaction

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

P.shutdown_readyS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq′

⊢

–eapply S.selected_admits ; split ; exact Hr | apply cleanup_valid ; exact Hwf | exact I | exact Hstep

4 open

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

P.action_postS.boundaryspecs cleanupq ShutdownOutputaction InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world cleanupq′

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

[ ] = P.action_eventsShutdownOutputaction

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

P.shutdown_readyS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq′

⊢

–exact Hprefix

3 open

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

P.action_postS.boundaryspecs cleanupq ShutdownOutputaction InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world cleanupq′

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

[ ] = P.action_eventsShutdownOutputaction

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

P.shutdown_readyS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq′

⊢

–split ; exact Hstep |

3 open

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

[ ] = S.P.action_eventsShutdownOutputaction ∧ S.libc_validspecs hello_mem hello_world cleanupq′

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

[ ] = P.action_eventsShutdownOutputaction

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

P.shutdown_readyS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq′

⊢

split ; symmetry ; exact Hevents |

3 open

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

S.libc_validspecs hello_mem hello_world cleanupq′

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

[ ] = P.action_eventsShutdownOutputaction

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

P.shutdown_readyS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq′

⊢

apply cleanup_valid

3 open

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

stream_wfq′

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

[ ] = P.action_eventsShutdownOutputaction

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

P.shutdown_readyS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq′

⊢

eapply stream_step_wf ; eauto

2 open

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

[ ] = P.action_eventsShutdownOutputaction

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

P.shutdown_readyS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq′

⊢

–symmetry

2 open

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

P.action_eventsShutdownOutputaction = [ ]

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

P.shutdown_readyS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq′

⊢

exact Hevents

deferred goal

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

P.shutdown_readyS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanupq′

⊢

–split ; exact Hr |

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

S.libc_validspecs hello_mem hello_world cleanupq′

apply cleanup_valid

q :

action :

q′ :

Hnot :

∀bytes : listZ, action ≠ Acceptbytes

Hstream :

stream_stepq action q′

Hwf :

Hstep :

shutdown_stepcleanupq ShutdownOutputaction cleanupq′

Hcall :

S.E.invokeS.selected_contractspecs cleanupq ShutdownOutputaction CVoid [ ] [ ] InterpRuntime.start hello_mem hello_world [ ] CallReturn[ ] InterpRuntime.start hello_mem hello_world

Hevents :

P.action_eventsShutdownOutputaction = [ ]

born :

listZ

Hprefix :

S.E.prefixS.selected_contractspecs cleanupq ShutdownOutputaction [ ] InterpRuntime.start hello_mem hello_world born [ ] InterpRuntime.start hello_mem hello_world

Hr :

⊢

stream_wfq′

eapply stream_step_wf ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros q action q′ Hnot Hstream Hwf

assert Hstep : shutdown_stepcleanupq ShutdownOutputaction cleanupq′ by apply shutdown_cleanup_output ; assumption

assert Hcall := fixture_invocationhello_mem hello_world cleanupq ShutdownOutputaction cleanupq′ cleanup_valid_ Hwf I Hstep cleanup_valid_ stream_step_wf_ _ _ Hstream Hwf

assert Hevents : P.action_eventsShutdownOutputaction = [ ]

{destruct action ; try reflexivity

exfalso

apply Hnotbytes

reflexivity

rewrite Hevents in Hcall

destruct S.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born Hprefix

assert Hr := hello_readyInterpRuntime.start ltac:split ; vm_compute ; congruence

eapply P.realize_action with born := born

–exact Hstep

–split ; exact Hr | apply cleanup_valid ; exact Hwf

–eapply S.selected_admits ; split ; exact Hr | apply cleanup_valid ; exact Hwf | exact I | exact Hstep

–exact Hprefix

–split ; exact Hstep |

split ; symmetry ; exact Hevents |

apply cleanup_valid

eapply stream_step_wf ; eauto

–symmetry

exact Hevents

–split ; exact Hr |

apply cleanup_valid

eapply stream_step_wf ; eauto

Delivery, a zero-progress error, and discard are three completed segments with exact intermediate queues. Silent observations do not mean delivery and discard are the same operation.

489Example completed_mixed_cleanup: ∀rep requests host, P.runrep requests S.boundaryspecs host P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanupmkStreamByteOriented 65; 66 false [ ] P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanupmkStreamByteOriented [ ] true

Explore proof 14 tactics

Initial goal

⊢

∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop host : P.host_boundary, P.runrep requests S.boundaryspecs host P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true

intros rep requests host

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

P.runrep requests S.boundaryspecs host P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true

eapply P.program_next with trace := [ ] tail := [ ] mid := P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanupmkStreamByteOriented 66 false

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

P.steprep requests S.boundaryspecs host P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ false

focused goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

P.runrep requests S.boundaryspecs host P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ false [ ] P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true

–apply P.program_shutdown with action := ShutdownOutputDeliver65

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false ShutdownOutputDeliver65 [ ] InterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ false

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

apply cleanup_realized ; discriminate | apply stream_deliver65 66 false ; discriminate |

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

stream_wforientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

split ; repeat constructor ; lia | reflexivity

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

–eapply P.program_next with trace := [ ] tail := [ ] mid := P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanupmkStreamByteOriented 66 true

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

P.steprep requests S.boundaryspecs host P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ false [ ] P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ true

focused goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

P.runrep requests S.boundaryspecs host P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ true [ ] P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true

+apply P.program_shutdown with action := ShutdownOutputOutputError

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ false ShutdownOutputOutputError [ ] InterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ true

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

apply cleanup_realized ; discriminate | constructor |

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

stream_wforientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ false

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

split ; repeat constructor ; lia | reflexivity

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

+eapply P.program_next with trace := [ ] tail := [ ]

3 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

P.steprep requests S.boundaryspecs host P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ true [ ] ?mid

focused goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

P.runrep requests S.boundaryspecs host ?mid [ ] P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true

shelved goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

P.state

∗apply P.program_shutdown with action := ShutdownOutputDiscard66

6 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

P.realizesS.boundaryspecs InterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ true ShutdownOutputDiscard66 [ ] ?s′ ?m′ ?w′ ?sh′

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

P.runrep requests S.boundaryspecs host P.ShuttingDown?s′ ?m′ ?w′ ?sh′ [ ] P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true

shelved goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

shelved goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

shelved goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

shelved goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

apply cleanup_realized ; discriminate | apply stream_discard66 [ ] true ; discriminate |

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

stream_wforientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ true

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

P.runrep requests S.boundaryspecs host P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true [ ] P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanuporientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true

split ; repeat constructor ; lia | reflexivity

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

host :

⊢

∗constructor

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros rep requests host

eapply P.program_next with trace := [ ] tail := [ ] mid := P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanupmkStreamByteOriented 66 false

–apply P.program_shutdown with action := ShutdownOutputDeliver65

apply cleanup_realized ; discriminate | apply stream_deliver65 66 false ; discriminate |

split ; repeat constructor ; lia | reflexivity

–eapply P.program_next with trace := [ ] tail := [ ] mid := P.ShuttingDownInterpRuntime.start hello_mem hello_world cleanupmkStreamByteOriented 66 true

+apply P.program_shutdown with action := ShutdownOutputOutputError

apply cleanup_realized ; discriminate | constructor |

split ; repeat constructor ; lia | reflexivity

+eapply P.program_next with trace := [ ] tail := [ ]

∗apply P.program_shutdown with action := ShutdownOutputDiscard66

apply cleanup_realized ; discriminate | apply stream_discard66 [ ] true ; discriminate |

split ; repeat constructor ; lia | reflexivity

∗constructor

A successful logical entry with argv, environment, the generated hi literal, stdout storage and the nonempty admitted callback inventory.

517Definition completion_memory: mem ≔

startup_storecopy_c_bytesmkMemm_byteshello_mem mkRegion65552 65560 GlobalData Live :: mkRegion4096 4112 Heap Live :: mkRegion4200 4208 Heap Live :: m_regionshello_mem m_auxhello_mem 65552 hello_bytes 4096 hi_literal

The concrete startup vectors and retained callback argument are genuine readable capabilities; a logical queue is not a physical FILE claim.

2 open

deferred goal

⊢

string_vectorcompletion_memory entry_envp [ ]

3 open

q :

Hwf :

⊢

callbacks_validcompletion_memory shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q

focused goal

q :

Hwf :

stdio_readycompletion_memory hello_world ∧ P.H.hi_literal_validcompletion_memory

⊢

deferred goal

⊢

∗split ; | exact I

3 open

q :

Hwf :

⊢

Forallcallback_validcompletion_memory shutdown_pendingshutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q

deferred goal

q :

Hwf :

stdio_readycompletion_memory hello_world ∧ P.H.hi_literal_validcompletion_memory

⊢

deferred goal

⊢

constructor ; split ; reflexivity | constructor

2 open

deferred goal

q :

Hwf :

stdio_readycompletion_memory hello_world ∧ P.H.hi_literal_validcompletion_memory

⊢

deferred goal

⊢

∗split ; exact Hwf |

2 open

q :

Hwf :

stdio_readycompletion_memory hello_world ∧ P.H.hi_literal_validcompletion_memory

⊢

shutdown_uniqueshutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ entry; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q

deferred goal

⊢

repeat constructor

2 open

q :

Hwf :

stdio_readycompletion_memory hello_world ∧ P.H.hi_literal_validcompletion_memory

⊢

¬Inregistration_tokenentry [ ]

deferred goal

⊢

simpl

2 open

q :

Hwf :