rocq/theories/Program.v
Application execution over the coupled libc world. Extra preconditions are proved at reached calls, not assumed from invocation existence.
From Stdlib Require Import String ZArith List Lia
From Nanofil Require Import Term Syntax Values Memory Runtime Ops Semantics Identity ExternalCalls Startup Stdio Shutdown ExternalMachine Hi Composition Panics
Import ListNotations
Open Scope Z_scope
Open Scope list_scope
This outer development leaves every core module and terminal unchanged.
The same explicit environment restriction as the body theorem.
Only puts is linked through this richer registry.
else
None
Forget logical stdout and callbacks without changing machine snapshots.
match st with
The richer world stays attached to running and stopped states alike.
The old body facts plus the extra independent caller obligations.
No rich-world precondition is hidden behind a successful invoke.
Explore proof 12 tactics
Initial goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
⊢
∀c : config s : R.state w : program_world site : call_site, body_invM.Runningc, s w → external_siteH.hi_genv c site → M.admissibleregistry H.hi_genv c w site
intros c s w site Hbody Hwf Ho Hsite
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
Hbody :
H.hi_body_staterep projectM.Runningc, s w
Hwf :
Hsite :
external_siteH.hi_genv c site
⊢
M.admissibleregistry H.hi_genv c w site
destruct H.hi_reached_call_admissiblerep requests _ _ _ _ Hbody Hsite as Heq Hadmit
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
Hbody :
H.hi_body_staterep projectM.Runningc, s w
Hwf :
Hsite :
external_siteH.hi_genv c site
Heq :
site = hi_site
Hadmit :
H.M.admissibleH.hi_registryrep requests H.hi_genv c program_stdiow site
⊢
M.admissibleregistry H.hi_genv c w site
subst site
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
Hbody :
H.hi_body_staterep projectM.Runningc, s w
Hwf :
Hsite :
Hadmit :
H.M.admissibleH.hi_registryrep requests H.hi_genv c program_stdiow hi_site
destruct Hadmit as spec & xs & Hreg & Hargs & Habi & Hpre
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
Hbody :
H.hi_body_staterep projectM.Runningc, s w
Hwf :
Hsite :
spec :
xs :
listword
Hreg :
H.hi_registryrep requests site_namehi_site = Somespec
Habi :
Hpre :
contract_prespec xs c_memc program_stdiow
change Someputs_contractrep requests = Somespec in Hreg
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
Hbody :
H.hi_body_staterep projectM.Runningc, s w
Hwf :
Hsite :
spec :
xs :
listword
Hreg :
Someputs_contractrep requests = Somespec
Habi :
Hpre :
contract_prespec xs c_memc program_stdiow
injection Hreg as ←
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
Hbody :
H.hi_body_staterep projectM.Runningc, s w
Hwf :
Hsite :
xs :
listword
Hpre :
contract_preputs_contractrep requests xs c_memc program_stdiow
Habi :
exists program_putsrep requests, xs
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
Hbody :
H.hi_body_staterep projectM.Runningc, s w
Hwf :
Hsite :
xs :
listword
Hpre :
contract_preputs_contractrep requests xs c_memc program_stdiow
Habi :
⊢
registrysite_namehi_site = Someprogram_putsrep requests ∧ map_optionarg_xH.hi_genv fr_envc_framec site_argshi_site = Somexs ∧ contract_abiprogram_putsrep requests site_resulthi_site site_argshi_site ∧ contract_preprogram_putsrep requests xs c_memc w
split ; reflexivity |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
Hbody :
H.hi_body_staterep projectM.Runningc, s w
Hwf :
Hsite :
xs :
listword
Hpre :
contract_preputs_contractrep requests xs c_memc program_stdiow
Habi :
⊢
map_optionarg_xH.hi_genv fr_envc_framec site_argshi_site = Somexs ∧ contract_abiprogram_putsrep requests site_resulthi_site site_argshi_site ∧ contract_preprogram_putsrep requests xs c_memc w
split ; exact Hargs |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
Hbody :
H.hi_body_staterep projectM.Runningc, s w
Hwf :
Hsite :
xs :
listword
Hpre :
contract_preputs_contractrep requests xs c_memc program_stdiow
Habi :
⊢
contract_abiprogram_putsrep requests site_resulthi_site site_argshi_site ∧ contract_preprogram_putsrep requests xs c_memc w
split ; exact Habi |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
Hbody :
H.hi_body_staterep projectM.Runningc, s w
Hwf :
Hsite :
xs :
listword
Hpre :
contract_preputs_contractrep requests xs c_memc program_stdiow
Habi :
⊢
contract_preprogram_putsrep requests xs c_memc w
split ; exact Hpre |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
Hbody :
H.hi_body_staterep projectM.Runningc, s w
Hwf :
Hsite :
xs :
listword
Hpre :
contract_preputs_contractrep requests xs c_memc program_stdiow
Habi :
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros c s w site Hbody Hwf Ho Hsite
destruct H.hi_reached_call_admissiblerep requests _ _ _ _ Hbody Hsite as Heq Hadmit
subst site
destruct Hadmit as spec & xs & Hreg & Hargs & Habi & Hpre
change Someputs_contractrep requests = Somespec in Hreg
injection Hreg as ←
exists program_putsrep requests, xs
split ; reflexivity |
split ; exact Hargs |
split ; exact Habi |
split ; exact Hpre |
auto
Exact call syntax selects the coupled contract, not an arbitrary registry entry.
Explore proof 5 tactics
Initial goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
⊢
∀c : config s : R.state w : program_world site : call_site spec : contractprogram_world xs : listword, body_invM.Runningc, s w → external_siteH.hi_genv c site → registrysite_namesite = Somespec → map_optionarg_xH.hi_genv fr_envc_framec site_argssite = Somexs → site = hi_site ∧ spec = program_putsrep requests
intros c s w site spec xs Hbody _ Hsite Hreg Hargs
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
Hbody :
H.hi_body_staterep projectM.Runningc, s w
Hsite :
external_siteH.hi_genv c site
⊢
site = hi_site ∧ spec = program_putsrep requests
destruct H.hi_reached_call_admissiblerep requests _ _ _ _ Hbody Hsite as → _
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
spec :
xs :
listword
Hbody :
H.hi_body_staterep projectM.Runningc, s w
Hsite :
⊢
hi_site = hi_site ∧ spec = program_putsrep requests
split ; reflexivity |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
spec :
xs :
listword
Hbody :
H.hi_body_staterep projectM.Runningc, s w
Hsite :
⊢
spec = program_putsrep requests
change Someprogram_putsrep requests = Somespec in Hreg
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
spec :
xs :
listword
Hbody :
H.hi_body_staterep projectM.Runningc, s w
Hreg :
Someprogram_putsrep requests = Somespec
Hsite :
⊢
spec = program_putsrep requests
congruence
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros c s w site spec xs Hbody _ Hsite Hreg Hargs
destruct H.hi_reached_call_admissiblerep requests _ _ _ _ Hbody Hsite as → _
split ; reflexivity |
change Someprogram_putsrep requests = Somespec in Hreg
congruence
Projection includes rejected-call cases: independently proved rich admissibility rules them out rather than silently deleting them.
Proof 21 steps Qed
intros st trace st′ Hstep Hinv
destruct Hstep as ms ms′ w Hcore | c s w o Hnone Hdone | c s w why Hnone Hstuck | c s w q k Hnone Hfresh Hsize Hrefuse | c s w site spec xs trace values s′ m′ w′ e Hsite Hreg Hargs Hcall Henv | c s w site spec xs trace status s′ m′ w′ Hsite Hreg Hargs Hcall | c s w site spec xs trace why s′ m′ w′ Hsite Hreg Hargs Hcall | c s w site why Hsite Hreject | c s w site spec xs trace values s′ m′ w′ Hsite Hreg Hargs Hcall Henv ; simpl
–apply M.step_core
exact Hcore
–apply M.step_core_end ; assumption
–apply M.step_core_stuck ; assumption
–eapply M.step_core_refusal ; eauto
–destruct selected_call_ _ _ _ _ _ Hinv Hsite Hreg Hargs as → →
eapply M.step_return ; exact Hsite | reflexivity | exact Hargs | | exact Henv
eapply C.program_invoke_projects ; eauto
–destruct selected_call_ _ _ _ _ _ Hinv Hsite Hreg Hargs as → →
eapply M.step_exit ; exact Hsite | reflexivity | exact Hargs |
eapply C.program_invoke_projects ; eauto
–destruct selected_call_ _ _ _ _ _ Hinv Hsite Hreg Hargs as → →
eapply M.step_resource ; exact Hsite | reflexivity | exact Hargs |
eapply C.program_invoke_projects ; eauto
–exfalso
eapply M.admissible_not_rejected ; eapply reached_admissible ; eauto | exact Hreject
–destruct selected_call_ _ _ _ _ _ Hinv Hsite Hreg Hargs as → →
eapply M.step_bad_return ; exact Hsite | reflexivity | exact Hargs | | exact Henv
eapply C.program_invoke_projects ; eauto
Stream evolution also preserves the extra world obligations.
Explore proof 13 tactics
Initial goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
⊢
∀st : M.stateprogram_world trace : listevent st′ : M.stateprogram_world, M.stepregistry H.hi_genv st trace st′ → body_invst → body_invst′
intros st trace st′ Hstep Hinv
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
st′ :
Hinv :
body_invst
⊢
body_invst′
pose proof step_projects_ _ _ Hstep Hinv as Hproject
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
st′ :
Hinv :
body_invst
Hproject :
M.stepH.hi_registryrep requests H.hi_genv projectst trace projectst′
⊢
body_invst′
destruct Hinv as Hbody Hwf Ho
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
st′ :
Hbody :
H.hi_body_staterep projectst
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv projectst trace projectst′
⊢
body_invst′
split
2 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
st′ :
Hbody :
H.hi_body_staterep projectst
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv projectst trace projectst′
⊢
H.hi_body_staterep projectst′
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
st′ :
Hbody :
H.hi_body_staterep projectst
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv projectst trace projectst′
–eapply H.hi_body_step ; exact stdio_stable | exact Hproject | exact Hbody
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
st′ :
Hbody :
H.hi_body_staterep projectst
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv projectst trace projectst′
–destruct Hstep ; simpl in * ; try split ; assumption
4 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
e :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = Somee
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.Runningresume_externalc site e m′, s′ program_stdiow′
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
status :
Z
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedExternalExitstatus M.P.I.RM.with_memc m′, s′ program_stdiow′
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
why :
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedCoreEndTrapwhy M.P.I.RM.with_memc m′, s′ program_stdiow′
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedContractViolationsite_namesite BadReturn M.P.I.RM.with_memc m′, s′ program_stdiow′
all: assert Hselected : spec = program_putsrep requests
8 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
e :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = Somee
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.Runningresume_externalc site e m′, s′ program_stdiow′
⊢
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
e :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = Somee
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.Runningresume_externalc site e m′, s′ program_stdiow′
Hselected :
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
status :
Z
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedExternalExitstatus M.P.I.RM.with_memc m′, s′ program_stdiow′
⊢
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
status :
Z
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedExternalExitstatus M.P.I.RM.with_memc m′, s′ program_stdiow′
Hselected :
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
why :
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedCoreEndTrapwhy M.P.I.RM.with_memc m′, s′ program_stdiow′
⊢
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
why :
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedCoreEndTrapwhy M.P.I.RM.with_memc m′, s′ program_stdiow′
Hselected :
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedContractViolationsite_namesite BadReturn M.P.I.RM.with_memc m′, s′ program_stdiow′
⊢
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedContractViolationsite_namesite BadReturn M.P.I.RM.with_memc m′, s′ program_stdiow′
Hselected :
spec = program_putsrep requests
all: try destruct H.hi_reached_call_admissiblerep requests _ _ _ _ Hbody H as Heq _ ; rewrite Heq in H0 ; change Someprogram_putsrep requests = Somespec in H0 ; congruence
4 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
e :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = Somee
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.Runningresume_externalc site e m′, s′ program_stdiow′
Hselected :
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
status :
Z
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedExternalExitstatus M.P.I.RM.with_memc m′, s′ program_stdiow′
Hselected :
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
why :
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedCoreEndTrapwhy M.P.I.RM.with_memc m′, s′ program_stdiow′
Hselected :
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedContractViolationsite_namesite BadReturn M.P.I.RM.with_memc m′, s′ program_stdiow′
Hselected :
spec = program_putsrep requests
all: subst spec
4 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
e :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H3 :
external_envprogram_putsrep requests site values fr_envc_framec = Somee
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.Runningresume_externalc site e m′, s′ program_stdiow′
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
status :
Z
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedExternalExitstatus M.P.I.RM.with_memc m′, s′ program_stdiow′
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
why :
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedCoreEndTrapwhy M.P.I.RM.with_memc m′, s′ program_stdiow′
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H3 :
external_envprogram_putsrep requests site values fr_envc_framec = None
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedContractViolationsite_namesite BadReturn M.P.I.RM.with_memc m′, s′ program_stdiow′
all: destruct C.program_invoke_continuity_ _ _ _ _ _ _ _ _ _ _ _ _ H2 as _ Hstream Hwf′
4 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
e :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H3 :
external_envprogram_putsrep requests site values fr_envc_framec = Somee
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.Runningresume_externalc site e m′, s′ program_stdiow′
Hstream :
puts_stream_prefixxs c_memc program_stdoutw trace program_stdoutw′
Hwf′ :
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
status :
Z
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedExternalExitstatus M.P.I.RM.with_memc m′, s′ program_stdiow′
Hstream :
puts_stream_prefixxs c_memc program_stdoutw trace program_stdoutw′
Hwf′ :
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
why :
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedCoreEndTrapwhy M.P.I.RM.with_memc m′, s′ program_stdiow′
Hstream :
puts_stream_prefixxs c_memc program_stdoutw trace program_stdoutw′
Hwf′ :
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H3 :
external_envprogram_putsrep requests site values fr_envc_framec = None
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedContractViolationsite_namesite BadReturn M.P.I.RM.with_memc m′, s′ program_stdiow′
Hstream :
puts_stream_prefixxs c_memc program_stdoutw trace program_stdoutw′
Hwf′ :
all: split ; exact Hwf′ |
4 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
e :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H3 :
external_envprogram_putsrep requests site values fr_envc_framec = Somee
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.Runningresume_externalc site e m′, s′ program_stdiow′
Hstream :
puts_stream_prefixxs c_memc program_stdoutw trace program_stdoutw′
Hwf′ :
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
status :
Z
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedExternalExitstatus M.P.I.RM.with_memc m′, s′ program_stdiow′
Hstream :
puts_stream_prefixxs c_memc program_stdoutw trace program_stdoutw′
Hwf′ :
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
why :
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedCoreEndTrapwhy M.P.I.RM.with_memc m′, s′ program_stdiow′
Hstream :
puts_stream_prefixxs c_memc program_stdoutw trace program_stdoutw′
Hwf′ :
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H3 :
external_envprogram_putsrep requests site values fr_envc_framec = None
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedContractViolationsite_namesite BadReturn M.P.I.RM.with_memc m′, s′ program_stdiow′
Hstream :
puts_stream_prefixxs c_memc program_stdoutw trace program_stdoutw′
Hwf′ :
all: destruct Hstream as p & bytes & actions & tail & _ & _ & Hrun & _
4 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
e :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H3 :
external_envprogram_putsrep requests site values fr_envc_framec = Somee
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.Runningresume_externalc site e m′, s′ program_stdiow′
p :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hrun :
stream_runprogram_stdoutw actions program_stdoutw′
Hwf′ :
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
status :
Z
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedExternalExitstatus M.P.I.RM.with_memc m′, s′ program_stdiow′
p :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hrun :
stream_runprogram_stdoutw actions program_stdoutw′
Hwf′ :
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
why :
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedCoreEndTrapwhy M.P.I.RM.with_memc m′, s′ program_stdiow′
p :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hrun :
stream_runprogram_stdoutw actions program_stdoutw′
Hwf′ :
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H3 :
external_envprogram_putsrep requests site values fr_envc_framec = None
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hwf :
Hproject :
M.stepH.hi_registryrep requests H.hi_genv M.Runningc, s program_stdiow trace M.StoppedContractViolationsite_namesite BadReturn M.P.I.RM.with_memc m′, s′ program_stdiow′
p :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hrun :
stream_runprogram_stdoutw actions program_stdoutw′
Hwf′ :
all: eapply stream_run_nonwide ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros st trace st′ Hstep Hinv
pose proof step_projects_ _ _ Hstep Hinv as Hproject
destruct Hinv as Hbody Hwf Ho
split
–eapply H.hi_body_step ; exact stdio_stable | exact Hproject | exact Hbody
–destruct Hstep ; simpl in * ; try split ; assumption
all: assert Hselected : spec = program_putsrep requests
all: try destruct H.hi_reached_call_admissiblerep requests _ _ _ _ Hbody H as Heq _ ; rewrite Heq in H0 ; change Someprogram_putsrep requests = Somespec in H0 ; congruence
all: subst spec
all: destruct C.program_invoke_continuity_ _ _ _ _ _ _ _ _ _ _ _ _ H2 as _ Hstream Hwf′
all: split ; exact Hwf′ |
all: destruct Hstream as p & bytes & actions & tail & _ & _ & Hrun & _
all: eapply stream_run_nonwide ; eauto
Every finite richer run retains the old safety facts and the new obligations. This is not inferred from invoke projection alone.
Explore proof 5 tactics
Initial goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
⊢
∀st : M.stateprogram_world trace : listevent st′ : M.stateprogram_world, M.runregistry H.hi_genv st trace st′ → body_invst → body_invst′
intros st trace st′ H
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
st′ :
induction H ; auto |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
mid :
tail :
listevent
last :
intros Hinv
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
mid :
tail :
listevent
last :
Hinv :
body_invst
⊢
body_invlast
apply IHrun
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
mid :
tail :
listevent
last :
Hinv :
body_invst
⊢
body_invmid
eapply body_step ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The application cannot replace the entry's callback inventory with a different list merely because the replacement has distinct tokens.
∀ st trace st′
Explore proof 7 tactics
Initial goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
⊢
∀st : M.stateprogram_world trace : listevent st′ : M.stateprogram_world, M.stepregistry H.hi_genv st trace st′ → body_invst → program_pendingworld_ofst′ = program_pendingworld_ofst
intros st trace st′ Hstep Hinv
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
st′ :
Hinv :
body_invst
destruct Hinv as Hbody _
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
st′ :
Hbody :
H.hi_body_staterep projectst
destruct Hstep ; simpl in * ; try reflexivity
4 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
e :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = Somee
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
status :
Z
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
why :
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
all: assert Hselected : spec = program_putsrep requests
8 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
e :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = Somee
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
⊢
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
e :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = Somee
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hselected :
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
status :
Z
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
⊢
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
status :
Z
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hselected :
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
why :
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
⊢
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
why :
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hselected :
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
⊢
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hselected :
spec = program_putsrep requests
all: try destruct H.hi_reached_call_admissiblerep requests _ _ _ _ Hbody H as Heq _ ; rewrite Heq in H0 ; change Someprogram_putsrep requests = Somespec in H0 ; congruence
4 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
e :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = Somee
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hselected :
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
status :
Z
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hselected :
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
why :
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hselected :
spec = program_putsrep requests
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
Hselected :
spec = program_putsrep requests
all: subst spec
4 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
e :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H3 :
external_envprogram_putsrep requests site values fr_envc_framec = Somee
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
status :
Z
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
why :
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
c :
s :
site :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
registrysite_namesite = Someprogram_putsrep requests
H3 :
external_envprogram_putsrep requests site values fr_envc_framec = None
H2 :
M.E.invokeprogram_putsrep requests site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
Hbody :
H.hi_body_staterep M.Runningc, s program_stdiow
all: exact proj1C.program_invoke_continuity_ _ _ _ _ _ _ _ _ _ _ _ _ H2
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros st trace st′ Hstep Hinv
destruct Hinv as Hbody _
destruct Hstep ; simpl in * ; try reflexivity
all: assert Hselected : spec = program_putsrep requests
all: try destruct H.hi_reached_call_admissiblerep requests _ _ _ _ Hbody H as Heq _ ; rewrite Heq in H0 ; change Someprogram_putsrep requests = Somespec in H0 ; congruence
all: subst spec
all: exact proj1C.program_invoke_continuity_ _ _ _ _ _ _ _ _ _ _ _ _ H2
Every reached call keeps the actual initial registration list, not an arbitrary well-formed inventory admitted by the raw contract.
∀ st trace st′
Explore proof 5 tactics
Initial goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
⊢
∀st : M.stateprogram_world trace : listevent st′ : M.stateprogram_world, M.runregistry H.hi_genv st trace st′ → body_invst → program_pendingworld_ofst′ = program_pendingworld_ofst
intros st trace st′ Hrun
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
st′ :
⊢
induction Hrun ; reflexivity |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
mid :
tail :
listevent
last :
IHHrun :
body_invmid → program_pendingworld_oflast = program_pendingworld_ofmid
⊢
body_invst → program_pendingworld_oflast = program_pendingworld_ofst
intros Hinv
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
mid :
tail :
listevent
last :
IHHrun :
body_invmid → program_pendingworld_oflast = program_pendingworld_ofmid
Hinv :
body_invst
rewrite IHHrun by eapply body_step ; eauto
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
mid :
tail :
listevent
last :
IHHrun :
body_invmid → program_pendingworld_oflast = program_pendingworld_ofmid
Hinv :
body_invst
eapply body_step_inventory ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros st trace st′ Hrun
induction Hrun ; reflexivity |
intros Hinv
rewrite IHHrun by eapply body_step ; eauto
eapply body_step_inventory ; eauto
Every reachable rich-world external call meets all additional premises.
∀ st trace c s w site
M.admissibleregistry H.hi_genv c w site
Explore proof 2 tactics
Initial goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
⊢
∀st : M.stateprogram_world trace : listevent c : config s : R.state w : program_world site : call_site, body_invst → M.runregistry H.hi_genv st trace M.Runningc, s w → external_siteH.hi_genv c site → M.admissibleregistry H.hi_genv c w site
intros st trace c s w site Hinv Hrun Hsite
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
c :
s :
site :
Hinv :
body_invst
Hsite :
external_siteH.hi_genv c site
⊢
M.admissibleregistry H.hi_genv c w site
eapply reached_admissible ; eapply body_run ; eauto | exact Hsite
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros st trace c s w site Hinv Hrun Hsite
eapply reached_admissible ; eapply body_run ; eauto | exact Hsite
Additional contract premises do not introduce specification-violation terminals. Finite safety remains conditional, without native totality.
Explore proof 4 tactics
Initial goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
⊢
∀st : M.stateprogram_world trace : listevent why : ending ms : M.P.I.RM.mstate w : program_world, body_invst → M.runregistry H.hi_genv st trace M.Stoppedwhy ms w → H.hi_endingwhy
intros st trace why ms w Hinv Hrun
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
why :
ms :
Hinv :
body_invst
⊢
H.hi_endingwhy
destruct body_run_ _ _ Hrun Hinv as Hbody _
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
why :
ms :
Hinv :
body_invst
Hbody :
H.hi_body_staterep projectM.Stoppedwhy ms w
⊢
H.hi_endingwhy
inversion Hbody
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
why :
ms :
Hinv :
body_invst
Hbody :
H.hi_body_staterep projectM.Stoppedwhy ms w
why0 :
ms0 :
w0 :
H0 :
H.hi_endingwhy
H :
why0 = why
H1 :
ms0 = ms
H2 :
w0 = program_stdiow
⊢
H.hi_endingwhy
assumption
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros st trace why ms w Hinv Hrun
destruct body_run_ _ _ Hrun Hinv as Hbody _
inversion Hbody
assumption
Campaign 3's shared failure classification, not a competing definition of panic for the labelled machine. Resource refusal remains nonfailure.
Explore proof 1 tactics
Initial goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
⊢
∀why : ending, H.hi_endingwhy → ¬failure_endingwhy
intros why [ ->| [ ->| ( resource & -> & Hr ) ] ] ; simpl ; tauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros why [ ->| [ ->| ( resource & -> & Hr ) ] ] ; simpl ; tauto
Labelled application safety uses the same failure_ending predicate as the closed-module never_panics statement in Panics.v.
Explore proof 3 tactics
Initial goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
⊢
∀st : M.stateprogram_world trace : listevent why : ending ms : M.P.I.RM.mstate w : program_world, body_invst → M.runregistry H.hi_genv st trace M.Stoppedwhy ms w → ¬failure_endingwhy
intros st trace why ms w Hinv Hrun
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
why :
ms :
Hinv :
body_invst
⊢
¬failure_endingwhy
apply hi_ending_not_failure
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
why :
ms :
Hinv :
body_invst
⊢
H.hi_endingwhy
eapply finite_safety ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Every application observation is exit-free, including resource leaves.
Explore proof 5 tactics
Initial goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
⊢
∀st : M.stateprogram_world trace : listevent st′ : M.stateprogram_world status : Z, M.stepregistry H.hi_genv st trace st′ → body_invst → ¬InProcessExitstatus trace
intros st trace st′ status Hstep Hinv
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
st′ :
status :
Z
Hinv :
body_invst
⊢
¬InProcessExitstatus trace
destruct Hstep ; simpl ; try tauto
4 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
status :
Z
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
e :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = Somee
⊢
¬InProcessExitstatus trace
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
status :
Z
c :
s :
site :
spec :
xs :
listword
trace :
listevent
status0 :
Z
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallExitstatus0 s′ m′ w′
⊢
¬InProcessExitstatus trace
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
status :
Z
c :
s :
site :
spec :
xs :
listword
trace :
listevent
why :
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′
⊢
¬InProcessExitstatus trace
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
status :
Z
c :
s :
site :
spec :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H2 :
M.E.invokespec site_resultsite site_argssite xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envspec site values fr_envc_framec = None
⊢
¬InProcessExitstatus trace
all: destruct selected_call_ _ _ _ _ _ Hinv H H0 H1 as → →
4 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
status :
Z
c :
s :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
e :
H2 :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envprogram_putsrep requests hi_site values fr_envc_framec = Somee
H0 :
registrysite_namehi_site = Someprogram_putsrep requests
⊢
¬InProcessExitstatus trace
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
status :
Z
c :
s :
xs :
listword
trace :
listevent
status0 :
Z
s′ :
m′ :
w′ :
H2 :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site xs s c_memc w trace CallExitstatus0 s′ m′ w′
H0 :
registrysite_namehi_site = Someprogram_putsrep requests
⊢
¬InProcessExitstatus trace
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
status :
Z
c :
s :
xs :
listword
trace :
listevent
why :
s′ :
m′ :
w′ :
H2 :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site xs s c_memc w trace CallResourcewhy s′ m′ w′
H0 :
registrysite_namehi_site = Someprogram_putsrep requests
⊢
¬InProcessExitstatus trace
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
status :
Z
c :
s :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
H2 :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envprogram_putsrep requests hi_site values fr_envc_framec = None
H0 :
registrysite_namehi_site = Someprogram_putsrep requests
⊢
¬InProcessExitstatus trace
all: destruct C.program_invoke_continuity_ _ _ _ _ _ _ _ _ _ _ _ _ H2 as _ Hstream _
4 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
status :
Z
c :
s :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
e :
H2 :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envprogram_putsrep requests hi_site values fr_envc_framec = Somee
H0 :
registrysite_namehi_site = Someprogram_putsrep requests
Hstream :
puts_stream_prefixxs c_memc program_stdoutw trace program_stdoutw′
⊢
¬InProcessExitstatus trace
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
status :
Z
c :
s :
xs :
listword
trace :
listevent
status0 :
Z
s′ :
m′ :
w′ :
H2 :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site xs s c_memc w trace CallExitstatus0 s′ m′ w′
H0 :
registrysite_namehi_site = Someprogram_putsrep requests
Hstream :
puts_stream_prefixxs c_memc program_stdoutw trace program_stdoutw′
⊢
¬InProcessExitstatus trace
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
status :
Z
c :
s :
xs :
listword
trace :
listevent
why :
s′ :
m′ :
w′ :
H2 :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site xs s c_memc w trace CallResourcewhy s′ m′ w′
H0 :
registrysite_namehi_site = Someprogram_putsrep requests
Hstream :
puts_stream_prefixxs c_memc program_stdoutw trace program_stdoutw′
⊢
¬InProcessExitstatus trace
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
stdio_stable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
status :
Z
c :
s :
xs :
listword
trace :
listevent
values :
listword
s′ :
m′ :
w′ :
H2 :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site xs s c_memc w trace CallReturnvalues s′ m′ w′
H3 :
external_envprogram_putsrep requests hi_site values fr_envc_framec = None
H0 :
registrysite_namehi_site = Someprogram_putsrep requests
Hstream :
puts_stream_prefixxs c_memc program_stdoutw trace program_stdoutw′
⊢
¬InProcessExitstatus trace
all: eapply puts_stream_prefix_exit_free ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros st trace st′ status Hstep Hinv
destruct Hstep ; simpl ; try tauto
all: destruct selected_call_ _ _ _ _ _ Hinv H H0 H1 as → →
all: destruct C.program_invoke_continuity_ _ _ _ _ _ _ _ _ _ _ _ _ H2 as _ Hstream _
all: eapply puts_stream_prefix_exit_free ; eauto
Pure control actions observe no new stdout acceptance; starting a callback is not an atomic execution of its entire printing body.
match action with
_
⇒
[ ]
Only host completion may report process exit.
∀ action status
¬InProcessExitstatus action_eventsaction
Explore proof 3 tactics
Initial goal
⊢
∀action : shutdown_action status : Z, ¬InProcessExitstatus action_eventsaction
intros action status
action :
status :
Z
⊢
¬InProcessExitstatus action_eventsaction
destruct action ; simpl ; try tauto
action :
status :
Z
⊢
¬InProcessExitstatus match action with Acceptbytes ⇒ StreamBytes1 bytes _ ⇒ [ ] end
destruct action ; simpl ; intuition discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros action status
destruct action ; simpl ; try tauto
destruct action ; simpl ; intuition discriminate
A conservative partial segment stays in its selected output family and byte budget. Control actions, including callback entry, print nothing. This does not claim coverage of mixed native segments.
match action with
A terminal summary of one original segment, not a resumable trace. Delivery and discard remain distinct in the retained action history; only acceptance can produce a cumulative stdout observation.
Partial actions cannot smuggle a process-exit event into a leaf.
Explore proof 4 tactics
Initial goal
⊢
∀action : shutdown_action q : stream_state trace : listevent actions : liststream_action q′ : stream_state status : Z, partial_outputaction q trace actions q′ → ¬InProcessExitstatus trace
intros action q trace actions q′ status _ & _ & Hobs
action :
q :
trace :
listevent
actions :
liststream_action
q′ :
status :
Z
Hobs :
match action with
_
⇒
trace = [ ]
⊢
¬InProcessExitstatus trace
destruct action ; simpl in Hobs ; try subst trace ; simpl ; tauto
action :
q :
trace :
listevent
actions :
liststream_action
q′ :
status :
Z
Hobs :
match action with
_
⇒
trace = [ ]
⊢
¬InProcessExitstatus trace
destruct action ; simpl in Hobs ; try subst trace ; simpl ; tauto
bytes :
listZ
q :
trace :
listevent
actions :
liststream_action
q′ :
status :
Z
Hobs :
prefix_observationtrace actions
⊢
¬InProcessExitstatus trace
destruct Hobs as → _ | → ; simpl ; intuition discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros action q trace actions q′ status _ & _ & Hobs
destruct action ; simpl in Hobs ; try subst trace ; simpl ; tauto
destruct action ; simpl in Hobs ; try subst trace ; simpl ; tauto
destruct Hobs as → _ | → ; simpl ; intuition discriminate
The actual stream path, not a successful lifecycle endpoint, gives FIFO accounting, well-formedness and sticky error at partial leaves.
∀ action q trace actions q′
partial_outputaction q trace actions q′
outstandingq ++ acceptedactions = resolvedactions ++ outstandingq′ ∧ stream_wfq → stream_wfq′ ∧ stream_errorq = true → stream_errorq′ = true
Explore proof 5 tactics
Initial goal
⊢
∀action : shutdown_action q : stream_state trace : listevent actions : liststream_action q′ : stream_state, partial_outputaction q trace actions q′ → outstandingq ++ acceptedactions = resolvedactions ++ outstandingq′ ∧ stream_wfq → stream_wfq′ ∧ stream_errorq = true → stream_errorq′ = true
intros action q trace actions q′ _ & Hrun & _
⊢
outstandingq ++ acceptedactions = resolvedactions ++ outstandingq′ ∧ stream_wfq → stream_wfq′ ∧ stream_errorq = true → stream_errorq′ = true
split
2 open⊢
outstandingq ++ acceptedactions = resolvedactions ++ outstandingq′
focused goal
⊢
stream_wfq → stream_wfq′ ∧ stream_errorq = true → stream_errorq′ = true
–apply stream_accounting
2 open⊢
stream_runq actions q′
deferred goal
⊢
stream_wfq → stream_wfq′ ∧ stream_errorq = true → stream_errorq′ = true
exact Hrun
deferred goal
⊢
stream_wfq → stream_wfq′ ∧ stream_errorq = true → stream_errorq′ = true
–split ; eapply stream_run_wf | eapply stream_error_sticky ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros action q trace actions q′ _ & Hrun & _
split
–apply stream_accounting
exact Hrun
–split ; eapply stream_run_wf | eapply stream_error_sticky ; eauto
Trusted segment selection is independent of successful execution. ABI/arguments describe the selected segment boundary, not a proof of native callback calling conventions or retained-argument validity.
| shutdown_ready | : R.state → mem → stdio_world → shutdown_state → Prop | |
| action_contract | ||
| action_result | ||
| action_arguments | : shutdown_state → shutdown_action → listarg | |
| action_words | : shutdown_state → shutdown_action → listword | |
| action_post | : shutdown_state → shutdown_action → R.state → mem → stdio_world → listZ → listevent → R.state → mem → stdio_world → shutdown_state → Prop |
Obligations can fail even when no effect or completion witness exists.
282Definition shutdown_admissibleb : shutdown_boundary s : R.state m : mem w : stdio_world sh : shutdown_state action : shutdown_action : Prop ≔
contract_abiaction_contractb sh action action_resultb sh action action_argumentsb sh action ∧ contract_preaction_contractb sh action action_wordsb sh action m w
An actual successful action segment must carry its memory effects, exact endpoints and compatible output; logical lifecycle edges alone neither grant memory authority nor prove readiness.
290Inductive realizesb : shutdown_boundary : R.state → mem → stdio_world → shutdown_state → shutdown_action → listevent → R.state → mem → stdio_world → shutdown_state → Prop ≔
∀ s m w sh action trace s′ m′ w′ sh′ born
shutdown_stepsh action sh′
shutdown_readyb s m w sh
shutdown_admissibleb s m w sh action
M.E.prefixaction_contractb sh action action_wordsb sh action s m w born trace s′ m′ w′
action_postb sh action s m w born trace s′ m′ w′ sh′
trace = action_eventsaction
shutdown_readyb s′ m′ w′ sh′
realize_action
realizesb s m w sh action trace s′ m′ w′ sh′
The actual effect witness, rather than a readiness postulate about the logical protocol, preserves runtime readiness and every object identity.
Explore proof 3 tactics
Initial goal
⊢
∀b : shutdown_boundary s : R.state m : mem w : stdio_world sh : shutdown_state action : shutdown_action trace : listevent s′ : R.state m′ : mem w′ : stdio_world sh′ : shutdown_state, realizesb s m w sh action trace s′ m′ w′ sh′ → R.readys m → R.readys′ m′ ∧ persistsm m′
intros b s m w sh action trace s′ m′ w′ sh′ H Hr
destruct H
s :
m :
w :
sh :
action :
trace :
listevent
s′ :
m′ :
w′ :
sh′ :
born :
listZ
H :
shutdown_stepsh action sh′
H0 :
shutdown_readyb s m w sh
H1 :
shutdown_admissibleb s m w sh action
H2 :
M.E.prefixaction_contractb sh action action_wordsb sh action s m w born trace s′ m′ w′
H3 :
action_postb sh action s m w born trace s′ m′ w′ sh′
H4 :
trace = action_eventsaction
H5 :
shutdown_readyb s′ m′ w′ sh′
Hr :
R.readys m
⊢
R.readys′ m′ ∧ persistsm m′
eapply M.E.prefix_preserve ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Each realized segment obeys the same FIFO accounting as its selected lifecycle action, without equating delivery with error-discard.
∀ b s m w sh action trace s′ m′ w′ sh′
realizesb s m w sh action trace s′ m′ w′ sh′
outstandingshutdown_stdoutsh ++ acceptedshutdown_outputaction = resolvedshutdown_outputaction ++ outstandingshutdown_stdoutsh′
Explore proof 5 tactics
Initial goal
⊢
∀b : shutdown_boundary s : R.state m : mem w : stdio_world sh : shutdown_state action : shutdown_action trace : listevent s′ : R.state m′ : mem w′ : stdio_world sh′ : shutdown_state, realizesb s m w sh action trace s′ m′ w′ sh′ → outstandingshutdown_stdoutsh ++ acceptedshutdown_outputaction = resolvedshutdown_outputaction ++ outstandingshutdown_stdoutsh′
intros b s m w sh action trace s′ m′ w′ sh′ H
s :
m :
w :
sh :
action :
trace :
listevent
s′ :
m′ :
w′ :
sh′ :
H :
realizesb s m w sh action trace s′ m′ w′ sh′
⊢
outstandingshutdown_stdoutsh ++ acceptedshutdown_outputaction = resolvedshutdown_outputaction ++ outstandingshutdown_stdoutsh′
destruct H
s :
m :
w :
sh :
action :
trace :
listevent
s′ :
m′ :
w′ :
sh′ :
born :
listZ
H :
shutdown_stepsh action sh′
H0 :
shutdown_readyb s m w sh
H1 :
shutdown_admissibleb s m w sh action
H2 :
M.E.prefixaction_contractb sh action action_wordsb sh action s m w born trace s′ m′ w′
H3 :
action_postb sh action s m w born trace s′ m′ w′ sh′
H4 :
trace = action_eventsaction
H5 :
shutdown_readyb s′ m′ w′ sh′
⊢
outstandingshutdown_stdoutsh ++ acceptedshutdown_outputaction = resolvedshutdown_outputaction ++ outstandingshutdown_stdoutsh′
destruct H ; simpl ; try apply app_nil_r
2 opens :
m :
w :
trace :
listevent
s′ :
m′ :
w′ :
born :
listZ
status :
Z
active :
pending :
listregistration
consumed :
listnat
q :
action :
q′ :
H :
stream_stepq action q′
H0 :
shutdown_readyb s m w shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
H1 :
shutdown_admissibleb s m w shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction
H2 :
M.E.prefixaction_contractb shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction action_wordsb shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction s m w born trace s′ m′ w′
H3 :
action_postb shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction s m w born trace s′ m′ w′ shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q′
H4 :
trace = action_eventsShutdownOutputaction
H5 :
shutdown_readyb s′ m′ w′ shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q′
⊢
outstandingq ++ accepted_byaction ++ [ ] = resolved_byaction ++ [ ] ++ outstandingq′
focused goal
s :
m :
w :
trace :
listevent
s′ :
m′ :
w′ :
born :
listZ
status :
Z
consumed :
listnat
q :
action :
q′ :
H :
∀bytes : listZ, action ≠ Acceptbytes
H6 :
stream_stepq action q′
H0 :
shutdown_readyb s m w shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
H1 :
shutdown_admissibleb s m w shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction
H2 :
M.E.prefixaction_contractb shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction action_wordsb shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction s m w born trace s′ m′ w′
H3 :
action_postb shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction s m w born trace s′ m′ w′ shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q′
H4 :
trace = action_eventsShutdownOutputaction
H5 :
shutdown_readyb s′ m′ w′ shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q′
⊢
outstandingq ++ accepted_byaction ++ [ ] = resolved_byaction ++ [ ] ++ outstandingq′
all: repeat rewrite app_nil_r
2 opens :
m :
w :
trace :
listevent
s′ :
m′ :
w′ :
born :
listZ
status :
Z
active :
pending :
listregistration
consumed :
listnat
q :
action :
q′ :
H :
stream_stepq action q′
H0 :
shutdown_readyb s m w shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
H1 :
shutdown_admissibleb s m w shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction
H2 :
M.E.prefixaction_contractb shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction action_wordsb shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction s m w born trace s′ m′ w′
H3 :
action_postb shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction s m w born trace s′ m′ w′ shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q′
H4 :
trace = action_eventsShutdownOutputaction
H5 :
shutdown_readyb s′ m′ w′ shutdown_at ≔ InCallbackactive; shutdown_status ≔ status; shutdown_pending ≔ pending; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q′
⊢
outstandingq ++ accepted_byaction = resolved_byaction ++ outstandingq′
focused goal
s :
m :
w :
trace :
listevent
s′ :
m′ :
w′ :
born :
listZ
status :
Z
consumed :
listnat
q :
action :
q′ :
H :
∀bytes : listZ, action ≠ Acceptbytes
H6 :
stream_stepq action q′
H0 :
shutdown_readyb s m w shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q
H1 :
shutdown_admissibleb s m w shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction
H2 :
M.E.prefixaction_contractb shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction action_wordsb shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction s m w born trace s′ m′ w′
H3 :
action_postb shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q ShutdownOutputaction s m w born trace s′ m′ w′ shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q′
H4 :
trace = action_eventsShutdownOutputaction
H5 :
shutdown_readyb s′ m′ w′ shutdown_at ≔ Cleanup; shutdown_status ≔ status; shutdown_pending ≔ [ ]; shutdown_consumed ≔ consumed; shutdown_stdout ≔ q′
⊢
outstandingq ++ accepted_byaction = resolved_byaction ++ outstandingq′
all: eapply stream_step_accounting ; eassumption
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros b s m w sh action trace s′ m′ w′ sh′ H
destruct H
destruct H ; simpl ; try apply app_nil_r
all: repeat rewrite app_nil_r
all: eapply stream_step_accounting ; eassumption
The outer sum consumes completion once; neither resource leaves nor unfinished observations acquire a normal-exit continuation. Shutdown leaves retain original snapshots as provenance, not endpoint phases or inventories; their memory/world and observed stdout are separate.
| | | Application | body : M.stateprogram_world | |
| | | ShuttingDown | ||
| | | Unfinished | ||
| | | ShutdownUnfinished | runtime : R.state memory : mem stdio : stdio_world original : shutdown_state action : shutdown_action observed : liststream_action stdout : stream_state | |
| | | ShutdownResource | why : reason runtime : R.state memory : mem stdio : stdio_world original : shutdown_state action : shutdown_action observed : liststream_action stdout : stream_state | |
| | | Finished |
Host completion is explicitly tied to the entire handoff snapshot.
R.state → mem → stdio_world → shutdown_state → Prop
A separate outer interpreter: existing Stopped states remain terminal. An unfinished prefix is observed once at its original admissible call, never restarted at its endpoint.
347Inductive steprep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary : state → listevent → state → Prop ≔
∀ c s w bits
main_return_siteH.hi_genv c bits
program_main_return
steprep requests b host ApplicationM.Runningc, s w [ ] ShuttingDowns c_memc program_stdiow mkShutdownTls main_statusbits program_pendingw [ ] program_stdoutw
∀ c s w site born trace s′ m′ w′
external_siteH.hi_genv c site
site = hi_site
M.admissibleregistryrep requests H.hi_genv c w site
M.E.prefixprogram_putsrep requests WPtrhi_literal s c_memc w born trace s′ m′ w′
program_unfinished
steprep requests b host ApplicationM.Runningc, s w trace Unfinisheds′ m′ w′
∀ s m w sh action trace s′ m′ w′ sh′
realizesb s m w sh action trace s′ m′ w′ sh′
program_shutdown
steprep requests b host ShuttingDowns m w sh trace ShuttingDowns′ m′ w′ sh′
∀ s m w sh action full born trace s′ m′ w′ actions q′
shutdown_stepsh action full
shutdown_readyb s m w sh
shutdown_admissibleb s m w sh action
M.E.prefixaction_contractb sh action action_wordsb sh action s m w born trace s′ m′ w′
partial_outputaction shutdown_stdoutsh trace actions q′
program_shutdown_unfinished
steprep requests b host ShuttingDowns m w sh trace ShutdownUnfinisheds′ m′ w′ sh action actions q′
∀ s m w sh action full why trace s′ m′ w′ actions q′
shutdown_stepsh action full
shutdown_readyb s m w sh
shutdown_admissibleb s m w sh action
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s m w trace CallResourcewhy s′ m′ w′
partial_outputaction shutdown_stdoutsh trace actions q′
program_shutdown_resource
steprep requests b host ShuttingDowns m w sh trace ShutdownResourcewhy s′ m′ w′ sh action actions q′
∀ s m w kind status pending consumed q
hosts m w mkShutdownHandedOffkind status pending consumed q
program_complete
steprep requests b host ShuttingDowns m w mkShutdownHandedOffkind status pending consumed q ProcessExitprocess_statusstatus Finisheds m w mkShutdownHandedOffkind status pending consumed q
Finite observations, with no eventual-termination assertion.
Compose actual finite runs through their shared exact snapshot.
Explore proof 4 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary st : state first : listevent mid : state last : listevent final : state, runrep requests b host st first mid → runrep requests b host mid last final → runrep requests b host st first ++ last final
intros rep requests b host st first mid last final H
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
st :
first :
listevent
mid :
last :
listevent
final :
H :
runrep requests b host st first mid
induction H ; intros Htail ; simpl ; auto
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
last :
listevent
final, st :
trace :
listevent
mid :
tail :
listevent
last0 :
H :
steprep requests b host st trace mid
H0 :
runrep requests b host mid tail last0
Htail :
runrep requests b host last0 last final
⊢
runrep requests b host st trace ++ tail ++ last final
rewrite <- app_assoc
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
last :
listevent
final, st :
trace :
listevent
mid :
tail :
listevent
last0 :
H :
steprep requests b host st trace mid
H0 :
runrep requests b host mid tail last0
Htail :
runrep requests b host last0 last final
⊢
runrep requests b host st trace ++ tail ++ last final
eapply program_next ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests b host st first mid last final H
induction H ; intros Htail ; simpl ; auto
rewrite <- app_assoc
eapply program_next ; eauto
A consumed host completion cannot be reused by this outer machine.
Explore proof 2 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary s : R.state m : mem w : stdio_world sh : shutdown_state trace : listevent st : state, ¬steprep requests b host Finisheds m w sh trace st
intros rep requests b host s m w sh trace st Hstep
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
trace :
listevent
st :
⊢
False
inversion Hstep
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests b host s m w sh trace st Hstep
inversion Hstep
An unfinished observation does not assert that the call can resume.
∀ rep requests b host s m w trace st
¬steprep requests b host Unfinisheds m w trace st
Explore proof 2 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary s : R.state m : mem w : program_world trace : listevent st : state, ¬steprep requests b host Unfinisheds m w trace st
intros rep requests b host s m w trace st Hstep
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
trace :
listevent
st :
Hstep :
steprep requests b host Unfinisheds m w trace st
⊢
False
inversion Hstep
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests b host s m w trace st Hstep
inversion Hstep
A partial shutdown snapshot is provenance, not a resumed lifecycle state. No host rule can complete either kind of terminal leaf.
∀ rep requests b host s m w sh action actions q trace st
¬steprep requests b host ShutdownUnfinisheds m w sh action actions q trace st ∧ ∀why, ¬steprep requests b host ShutdownResourcewhy s m w sh action actions q trace st
Explore proof 2 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary s : R.state m : mem w : stdio_world sh : shutdown_state action : shutdown_action actions : liststream_action q : stream_state trace : listevent st : state, ¬steprep requests b host ShutdownUnfinisheds m w sh action actions q trace st ∧ ∀why : reason, ¬steprep requests b host ShutdownResourcewhy s m w sh action actions q trace st
intros
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
action :
actions :
liststream_action
q :
trace :
listevent
st :
⊢
¬steprep requests b host ShutdownUnfinisheds m w sh action actions q trace st ∧ ∀why : reason, ¬steprep requests b host ShutdownResourcewhy s m w sh action actions q trace st
split ; intros ; intro Hstep ; inversion Hstep
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
split ; intros ; intro Hstep ; inversion Hstep
Even without successful endpoint readiness, an unfinished observation keeps allocator readiness and all old object identities through effects.
∀ rep requests b host s m w sh trace s′ m′ w′ action actions q
steprep requests b host ShuttingDowns m w sh trace ShutdownUnfinisheds′ m′ w′ sh action actions q
R.readys m
R.readys′ m′ ∧ persistsm m′
Explore proof 3 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary s : R.state m : mem w : stdio_world sh : shutdown_state trace : listevent s′ : R.state m′ : mem w′ : stdio_world action : shutdown_action actions : liststream_action q : stream_state, steprep requests b host ShuttingDowns m w sh trace ShutdownUnfinisheds′ m′ w′ sh action actions q → R.readys m → R.readys′ m′ ∧ persistsm m′
intros rep requests b host s m w sh trace s′ m′ w′ action actions q Hstep Hr
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
trace :
listevent
s′ :
m′ :
w′ :
action :
actions :
liststream_action
q :
Hstep :
steprep requests b host ShuttingDowns m w sh trace ShutdownUnfinisheds′ m′ w′ sh action actions q
Hr :
R.readys m
⊢
R.readys′ m′ ∧ persistsm m′
inversion Hstep ; subst
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
trace :
listevent
s′ :
m′ :
w′ :
action :
actions :
liststream_action
q :
Hstep :
steprep requests b host ShuttingDowns m w sh trace ShutdownUnfinisheds′ m′ w′ sh action actions q
Hr :
R.readys m
full :
born :
listZ
H6 :
shutdown_stepsh action full
H11 :
shutdown_readyb s m w sh
H12 :
shutdown_admissibleb s m w sh action
H13 :
M.E.prefixaction_contractb sh action action_wordsb sh action s m w born trace s′ m′ w′
H14 :
partial_outputaction shutdown_stdoutsh trace actions q
⊢
R.readys′ m′ ∧ persistsm m′
eapply M.E.prefix_preserve ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests b host s m w sh trace s′ m′ w′ action actions q Hstep Hr
inversion Hstep ; subst
eapply M.E.prefix_preserve ; eauto
A resource endpoint carries the same preservation evidence as its actual invocation, not merely a resource label or logical edge.
∀ rep requests b host s m w sh trace why s′ m′ w′ action actions q
steprep requests b host ShuttingDowns m w sh trace ShutdownResourcewhy s′ m′ w′ sh action actions q
R.readys m
R.readys′ m′ ∧ persistsm m′
Explore proof 3 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary s : R.state m : mem w : stdio_world sh : shutdown_state trace : listevent why : reason s′ : R.state m′ : mem w′ : stdio_world action : shutdown_action actions : liststream_action q : stream_state, steprep requests b host ShuttingDowns m w sh trace ShutdownResourcewhy s′ m′ w′ sh action actions q → R.readys m → R.readys′ m′ ∧ persistsm m′
intros rep requests b host s m w sh trace why s′ m′ w′ action actions q Hstep Hr
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
trace :
listevent
why :
s′ :
m′ :
w′ :
action :
actions :
liststream_action
q :
Hstep :
steprep requests b host ShuttingDowns m w sh trace ShutdownResourcewhy s′ m′ w′ sh action actions q
Hr :
R.readys m
⊢
R.readys′ m′ ∧ persistsm m′
inversion Hstep ; subst
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
trace :
listevent
why :
s′ :
m′ :
w′ :
action :
actions :
liststream_action
q :
Hstep :
steprep requests b host ShuttingDowns m w sh trace ShutdownResourcewhy s′ m′ w′ sh action actions q
Hr :
R.readys m
full :
H6 :
shutdown_stepsh action full
H12 :
shutdown_readyb s m w sh
H13 :
shutdown_admissibleb s m w sh action
H14 :
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s m w trace CallResourcewhy s′ m′ w′
H15 :
partial_outputaction shutdown_stdoutsh trace actions q
⊢
R.readys′ m′ ∧ persistsm m′
eapply M.E.invoke_preserve ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests b host s m w sh trace why s′ m′ w′ action actions q Hstep Hr
inversion Hstep ; subst
eapply M.E.invoke_preserve ; eauto
A reached resource leaf carries a genuine requested refusal. The shared classification excludes it from capability panics.
∀ rep requests b host st trace why s m w sh action actions q
steprep requests b host st trace ShutdownResourcewhy s m w sh action actions q
resource_reasonwhy ∧ ¬failure_endingCoreEndTrapwhy
Explore proof 9 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary st : state trace : listevent why : reason s : R.state m : mem w : stdio_world sh : shutdown_state action : shutdown_action actions : liststream_action q : stream_state, steprep requests b host st trace ShutdownResourcewhy s m w sh action actions q → resource_reasonwhy ∧ ¬failure_endingCoreEndTrapwhy
intros rep requests b host st trace why s m w sh action actions q Hstep
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
st :
trace :
listevent
why :
s :
m :
w :
sh :
action :
actions :
liststream_action
q :
Hstep :
steprep requests b host st trace ShutdownResourcewhy s m w sh action actions q
⊢
resource_reasonwhy ∧ ¬failure_endingCoreEndTrapwhy
inversion Hstep ; subst
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
trace :
listevent
why :
s :
m :
w :
sh :
action :
actions :
liststream_action
q :
s0 :
m0 :
w0 :
Hstep :
steprep requests b host ShuttingDowns0 m0 w0 sh trace ShutdownResourcewhy s m w sh action actions q
full :
H6 :
shutdown_stepsh action full
H10 :
shutdown_readyb s0 m0 w0 sh
H11 :
shutdown_admissibleb s0 m0 w0 sh action
H12 :
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s0 m0 w0 trace CallResourcewhy s m w
H13 :
partial_outputaction shutdown_stdoutsh trace actions q
⊢
resource_reasonwhy ∧ ¬failure_endingCoreEndTrapwhy
match goal withHcall : M.E.invoke_ _ _ _ _ _ _ _ _ _ _ _ |- _⇒inversion Hcall ; substend
2 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
trace :
listevent
why :
s :
m :
w :
sh :
action :
actions :
liststream_action
q :
s0 :
m0 :
w0 :
Hstep :
steprep requests b host ShuttingDowns0 m0 w0 sh trace ShutdownResourcewhy s m w sh action actions q
full :
H6 :
shutdown_stepsh action full
H10 :
shutdown_readyb s0 m0 w0 sh
H11 :
shutdown_admissibleb s0 m0 w0 sh action
H12 :
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s0 m0 w0 trace CallResourcewhy s m w
H13 :
partial_outputaction shutdown_stdoutsh trace actions q
born :
listZ
H :
contract_abiaction_contractb sh action action_resultb sh action action_argumentsb sh action
H0 :
contract_preaction_contractb sh action action_wordsb sh action m0 w0
H1 :
M.E.prefixaction_contractb sh action action_wordsb sh action s0 m0 w0 born trace s m w
H2 :
contract_postaction_contractb sh action action_wordsb sh action m0 w0 born trace CallResourcewhy m w
H3 :
∀why0 : reason, CallResourcewhy ≠ CallResourcewhy0
H4 :
∀values : listword, CallResourcewhy = CallReturnvalues → return_shapecontract_returnsaction_contractb sh action values ∧ Forallword_authoritycontract_sourcesaction_contractb sh action action_wordsb sh action m0 w0 born m values
H5 :
∀status : Z, CallResourcewhy = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
resource_reasonwhy ∧ ¬failure_endingCoreEndTrapwhy
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
trace :
listevent
why :
s :
m :
w :
sh :
action :
actions :
liststream_action
q :
s0 :
m0 :
w0 :
Hstep :
steprep requests b host ShuttingDowns0 m0 w0 sh trace ShutdownResourcewhy s m w sh action actions q
full :
H6 :
shutdown_stepsh action full
H10 :
shutdown_readyb s0 m0 w0 sh
H11 :
shutdown_admissibleb s0 m0 w0 sh action
H12 :
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s0 m0 w0 trace CallResourcewhy s m w
H13 :
partial_outputaction shutdown_stdoutsh trace actions q
born :
listZ
H0 :
contract_abiaction_contractb sh action action_resultb sh action action_argumentsb sh action
H1 :
contract_preaction_contractb sh action action_wordsb sh action m0 w0
H2 :
M.E.prefixaction_contractb sh action action_wordsb sh action s0 m0 w0 born trace s m w
H3 :
M.E.resource_failurecontract_requestsaction_contractb sh action action_wordsb sh action m0 w0 s why
H5 :
contract_resourceaction_contractb sh action why
⊢
resource_reasonwhy ∧ ¬failure_endingCoreEndTrapwhy
match goal withHnormal : ∀why, CallResource_ ≠ CallResourcewhy |- _⇒exfalso ; apply Hnormalwhy ; reflexivityend
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
trace :
listevent
why :
s :
m :
w :
sh :
action :
actions :
liststream_action
q :
s0 :
m0 :
w0 :
Hstep :
steprep requests b host ShuttingDowns0 m0 w0 sh trace ShutdownResourcewhy s m w sh action actions q
full :
H6 :
shutdown_stepsh action full
H10 :
shutdown_readyb s0 m0 w0 sh
H11 :
shutdown_admissibleb s0 m0 w0 sh action
H12 :
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s0 m0 w0 trace CallResourcewhy s m w
H13 :
partial_outputaction shutdown_stdoutsh trace actions q
born :
listZ
H0 :
contract_abiaction_contractb sh action action_resultb sh action action_argumentsb sh action
H1 :
contract_preaction_contractb sh action action_wordsb sh action m0 w0
H2 :
M.E.prefixaction_contractb sh action action_wordsb sh action s0 m0 w0 born trace s m w
H3 :
M.E.resource_failurecontract_requestsaction_contractb sh action action_wordsb sh action m0 w0 s why
H5 :
contract_resourceaction_contractb sh action why
⊢
resource_reasonwhy ∧ ¬failure_endingCoreEndTrapwhy
assert Hr : resource_reasonwhy
2 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
trace :
listevent
why :
s :
m :
w :
sh :
action :
actions :
liststream_action
q :
s0 :
m0 :
w0 :
Hstep :
steprep requests b host ShuttingDowns0 m0 w0 sh trace ShutdownResourcewhy s m w sh action actions q
full :
H6 :
shutdown_stepsh action full
H10 :
shutdown_readyb s0 m0 w0 sh
H11 :
shutdown_admissibleb s0 m0 w0 sh action
H12 :
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s0 m0 w0 trace CallResourcewhy s m w
H13 :
partial_outputaction shutdown_stdoutsh trace actions q
born :
listZ
H0 :
contract_abiaction_contractb sh action action_resultb sh action action_argumentsb sh action
H1 :
contract_preaction_contractb sh action action_wordsb sh action m0 w0
H2 :
M.E.prefixaction_contractb sh action action_wordsb sh action s0 m0 w0 born trace s m w
H3 :
M.E.resource_failurecontract_requestsaction_contractb sh action action_wordsb sh action m0 w0 s why
H5 :
contract_resourceaction_contractb sh action why
⊢
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
trace :
listevent
why :
s :
m :
w :
sh :
action :
actions :
liststream_action
q :
s0 :
m0 :
w0 :
Hstep :
steprep requests b host ShuttingDowns0 m0 w0 sh trace ShutdownResourcewhy s m w sh action actions q
full :
H6 :
shutdown_stepsh action full
H10 :
shutdown_readyb s0 m0 w0 sh
H11 :
shutdown_admissibleb s0 m0 w0 sh action
H12 :
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s0 m0 w0 trace CallResourcewhy s m w
H13 :
partial_outputaction shutdown_stdoutsh trace actions q
born :
listZ
H0 :
contract_abiaction_contractb sh action action_resultb sh action action_argumentsb sh action
H1 :
contract_preaction_contractb sh action action_wordsb sh action m0 w0
H2 :
M.E.prefixaction_contractb sh action action_wordsb sh action s0 m0 w0 born trace s m w
H3 :
M.E.resource_failurecontract_requestsaction_contractb sh action action_wordsb sh action m0 w0 s why
H5 :
contract_resourceaction_contractb sh action why
Hr :
⊢
resource_reasonwhy ∧ ¬failure_endingCoreEndTrapwhy
{match goal withHrefuse : M.E.resource_failure_ _ _ |- _⇒inversion Hrefuseend;unfold resource_reason;auto
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
trace :
listevent
why :
s :
m :
w :
sh :
action :
actions :
liststream_action
q :
s0 :
m0 :
w0 :
Hstep :
steprep requests b host ShuttingDowns0 m0 w0 sh trace ShutdownResourcewhy s m w sh action actions q
full :
H6 :
shutdown_stepsh action full
H10 :
shutdown_readyb s0 m0 w0 sh
H11 :
shutdown_admissibleb s0 m0 w0 sh action
H12 :
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s0 m0 w0 trace CallResourcewhy s m w
H13 :
partial_outputaction shutdown_stdoutsh trace actions q
born :
listZ
H0 :
contract_abiaction_contractb sh action action_resultb sh action action_argumentsb sh action
H1 :
contract_preaction_contractb sh action action_wordsb sh action m0 w0
H2 :
M.E.prefixaction_contractb sh action action_wordsb sh action s0 m0 w0 born trace s m w
H3 :
M.E.resource_failurecontract_requestsaction_contractb sh action action_wordsb sh action m0 w0 s why
H5 :
contract_resourceaction_contractb sh action why
Hr :
⊢
resource_reasonwhy ∧ ¬failure_endingCoreEndTrapwhy
split ; exact Hr |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
trace :
listevent
why :
s :
m :
w :
sh :
action :
actions :
liststream_action
q :
s0 :
m0 :
w0 :
Hstep :
steprep requests b host ShuttingDowns0 m0 w0 sh trace ShutdownResourcewhy s m w sh action actions q
full :
H6 :
shutdown_stepsh action full
H10 :
shutdown_readyb s0 m0 w0 sh
H11 :
shutdown_admissibleb s0 m0 w0 sh action
H12 :
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s0 m0 w0 trace CallResourcewhy s m w
H13 :
partial_outputaction shutdown_stdoutsh trace actions q
born :
listZ
H0 :
contract_abiaction_contractb sh action action_resultb sh action action_argumentsb sh action
H1 :
contract_preaction_contractb sh action action_wordsb sh action m0 w0
H2 :
M.E.prefixaction_contractb sh action action_wordsb sh action s0 m0 w0 born trace s m w
H3 :
M.E.resource_failurecontract_requestsaction_contractb sh action action_wordsb sh action m0 w0 s why
H5 :
contract_resourceaction_contractb sh action why
Hr :
apply resource_not_failure
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
trace :
listevent
why :
s :
m :
w :
sh :
action :
actions :
liststream_action
q :
s0 :
m0 :
w0 :
Hstep :
steprep requests b host ShuttingDowns0 m0 w0 sh trace ShutdownResourcewhy s m w sh action actions q
full :
H6 :
shutdown_stepsh action full
H10 :
shutdown_readyb s0 m0 w0 sh
H11 :
shutdown_admissibleb s0 m0 w0 sh action
H12 :
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s0 m0 w0 trace CallResourcewhy s m w
H13 :
partial_outputaction shutdown_stdoutsh trace actions q
born :
listZ
H0 :
contract_abiaction_contractb sh action action_resultb sh action action_argumentsb sh action
H1 :
contract_preaction_contractb sh action action_wordsb sh action m0 w0
H2 :
M.E.prefixaction_contractb sh action action_wordsb sh action s0 m0 w0 born trace s m w
H3 :
M.E.resource_failurecontract_requestsaction_contractb sh action action_wordsb sh action m0 w0 s why
H5 :
contract_resourceaction_contractb sh action why
Hr :
⊢
exact Hr
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests b host st trace why s m w sh action actions q Hstep
inversion Hstep ; subst
match goal withHcall : M.E.invoke_ _ _ _ _ _ _ _ _ _ _ _ |- _⇒inversion Hcall ; substend
match goal withHnormal : ∀why, CallResource_ ≠ CallResourcewhy |- _⇒exfalso ; apply Hnormalwhy ; reflexivityend
assert Hr : resource_reasonwhy
{match goal withHrefuse : M.E.resource_failure_ _ _ |- _⇒inversion Hrefuseend;unfold resource_reason;auto
split ; exact Hr |
apply resource_not_failure
exact Hr
No continuation is added to the inner machine's stopped observations.
∀ rep requests b host why ms w trace st
¬steprep requests b host ApplicationM.Stoppedwhy ms w trace st
Explore proof 3 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary why : ending ms : M.P.I.RM.mstate w : program_world trace : listevent st : state, ¬steprep requests b host ApplicationM.Stoppedwhy ms w trace st
intros rep requests b host why ms w trace st Hstep
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
why :
ms :
trace :
listevent
st :
Hstep :
steprep requests b host ApplicationM.Stoppedwhy ms w trace st
⊢
False
inversion Hstep ; subst
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
why :
ms :
trace :
listevent
st′ :
Hstep :
steprep requests b host ApplicationM.Stoppedwhy ms w trace Applicationst′
⊢
False
eapply M.stopped_no_step ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests b host why ms w trace st Hstep
inversion Hstep ; subst
eapply M.stopped_no_step ; eauto
Inner application runs lift unchanged, including their stopped outcomes.
∀ rep requests b host st trace st′
runrep requests b host Applicationst trace Applicationst′
Explore proof 4 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary st : M.stateprogram_world trace : listevent st′ : M.stateprogram_world, M.runregistryrep requests H.hi_genv st trace st′ → runrep requests b host Applicationst trace Applicationst′
intros rep requests b host st trace st′ Hrun
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
trace :
listevent
st′ :
⊢
runrep requests b host Applicationst trace Applicationst′
induction Hrun
2 open⊢
runrep requests b host Applicationst [ ] Applicationst
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
trace :
listevent
mid :
tail :
listevent
last :
IHHrun :
runrep requests b host Applicationmid tail Applicationlast
⊢
runrep requests b host Applicationst trace ++ tail Applicationlast
–constructor
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
trace :
listevent
mid :
tail :
listevent
last :
IHHrun :
runrep requests b host Applicationmid tail Applicationlast
⊢
runrep requests b host Applicationst trace ++ tail Applicationlast
–eapply program_next ; apply program_application ; eassumption | exact IHHrun
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests b host st trace st′ Hrun
induction Hrun
–constructor
–eapply program_next ; apply program_application ; eassumption | exact IHHrun
Native entry/libc closure covers every returning call reached from this exact entry, not arbitrary token-distinct callback inventories. Readiness at the exact endpoint is not inferred from equal tokens or stipulated only on an enabled bridge edge.
487Definition puts_shutdown_closedrep requests b : shutdown_boundary start : M.stateprogram_world : Prop ≔
∀first s m w fuel trace n s′ m′ w′, M.runregistryrep requests H.hi_genv start first M.Runninghi_callm fuel, s w → M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′ → shutdown_readyb s′ m′ program_stdiow′ mkShutdownTls 0 program_pendingw′ [ ] program_stdoutw′
Every returning puts reached from the selected entry has the real return-zero bridge. Its original prefix is retained, not replayed from an independently selected call snapshot.
∀ rep requests b host start first s m w fuel trace n s′ m′ w′
puts_shutdown_closedrep requests b start
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
runrep requests b host Applicationstart first ++ trace ShuttingDowns′ m′ program_stdiow′ mkShutdownTls 0 program_pendingw′ [ ] program_stdoutw′
Explore proof 11 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary start : M.stateprogram_world first : listevent s : R.state m : mem w : program_world fuel : Z trace : listevent n : Z s′ : R.state m′ : mem w′ : program_world, puts_shutdown_closedrep requests b start → M.runregistryrep requests H.hi_genv start first M.Runninghi_callm fuel, s w → M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′ → runrep requests b host Applicationstart first ++ trace ShuttingDowns′ m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′
intros rep requests b host start first s m w fuel trace n s′ m′ w′ Hclosed Hreach Hcall
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
⊢
runrep requests b host Applicationstart first ++ trace ShuttingDowns′ m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′
eapply run_trans ; apply application_run ; exact Hreach |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
⊢
runrep requests b host ApplicationM.Runninghi_callm fuel, s w trace ShuttingDowns′ m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′
rewrite <- app_nil_rtrace
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
⊢
runrep requests b host ApplicationM.Runninghi_callm fuel, s w trace ++ [ ] ShuttingDowns′ m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′
eapply program_next with trace := trace tail := [ ] mid := ApplicationM.Runningresume_externalhi_callm fuel hi_site TAtom"v1", WIntn mod 2 ^ 32; TAtom"v0", WPtrhi_literal m′, s′ w′
2 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
⊢
steprep requests b host ApplicationM.Runninghi_callm fuel, s w trace ApplicationM.Runningresume_externalhi_callm fuel hi_site TAtom"v1", WIntn mod 2 ^ 32; TAtom"v0", WPtrhi_literal m′, s′ w′
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
⊢
runrep requests b host ApplicationM.Runningresume_externalhi_callm fuel hi_site TAtom"v1", WIntn mod 2 ^ 32; TAtom"v0", WPtrhi_literal m′, s′ w′ [ ] ShuttingDowns′ m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′
–apply program_application
2 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
⊢
runrep requests b host ApplicationM.Runningresume_externalhi_callm fuel hi_site TAtom"v1", WIntn mod 2 ^ 32; TAtom"v0", WPtrhi_literal m′, s′ w′ [ ] ShuttingDowns′ m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′
eapply M.step_return ; apply H.hi_external_site | reflexivity | reflexivity | exact Hcall | reflexivity
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
⊢
runrep requests b host ApplicationM.Runningresume_externalhi_callm fuel hi_site TAtom"v1", WIntn mod 2 ^ 32; TAtom"v0", WPtrhi_literal m′, s′ w′ [ ] ShuttingDowns′ m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′
–eapply program_next with trace := [ ] tail := [ ]
3 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
⊢
steprep requests b host ApplicationM.Runningresume_externalhi_callm fuel hi_site TAtom"v1", WIntn mod 2 ^ 32; TAtom"v0", WPtrhi_literal m′, s′ w′ [ ]
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
⊢
runrep requests b host [ ] ShuttingDowns′ m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′
shelved goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
+apply program_main_return with bits := 0
3 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
⊢
main_return_siteH.hi_genv resume_externalhi_callm fuel hi_site TAtom"v1", WIntn mod 2 ^ 32; TAtom"v0", WPtrhi_literal m′ 0
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
⊢
shutdown_readyb s′ c_memresume_externalhi_callm fuel hi_site TAtom"v1", WIntn mod 2 ^ 32; TAtom"v0", WPtrhi_literal m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ main_status0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
⊢
runrep requests b host ShuttingDowns′ c_memresume_externalhi_callm fuel hi_site TAtom"v1", WIntn mod 2 ^ 32; TAtom"v0", WPtrhi_literal m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ main_status0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′ [ ] ShuttingDowns′ m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′
∗apply H.hi_after_puts_return
2 opendeferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
⊢
shutdown_readyb s′ c_memresume_externalhi_callm fuel hi_site TAtom"v1", WIntn mod 2 ^ 32; TAtom"v0", WPtrhi_literal m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ main_status0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
⊢
runrep requests b host ShuttingDowns′ c_memresume_externalhi_callm fuel hi_site TAtom"v1", WIntn mod 2 ^ 32; TAtom"v0", WPtrhi_literal m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ main_status0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′ [ ] ShuttingDowns′ m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′
∗eapply Hclosed ; eauto
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
start :
first :
listevent
s :
m :
fuel :
Z
trace :
listevent
n :
Z
s′ :
m′ :
w′ :
Hclosed :
puts_shutdown_closedrep requests b start
Hcall :
M.E.invokeprogram_putsrep requests site_resulthi_site site_argshi_site WPtrhi_literal s m w trace CallReturnWIntn s′ m′ w′
⊢
runrep requests b host ShuttingDowns′ c_memresume_externalhi_callm fuel hi_site TAtom"v1", WIntn mod 2 ^ 32; TAtom"v0", WPtrhi_literal m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ main_status0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′ [ ] ShuttingDowns′ m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′
+constructor
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests b host start first s m w fuel trace n s′ m′ w′ Hclosed Hreach Hcall
eapply run_trans ; apply application_run ; exact Hreach |
rewrite <- app_nil_rtrace
eapply program_next with trace := trace tail := [ ] mid := ApplicationM.Runningresume_externalhi_callm fuel hi_site TAtom"v1", WIntn mod 2 ^ 32; TAtom"v0", WPtrhi_literal m′, s′ w′
–apply program_application
eapply M.step_return ; apply H.hi_external_site | reflexivity | reflexivity | exact Hcall | reflexivity
–eapply program_next with trace := [ ] tail := [ ]
+constructor
Logical readiness must independently justify the selected action's arguments and ABI even when that action has no successful realization.
∀s m w sh action sh′, shutdown_readyb s m w sh → shutdown_stepsh action sh′ → shutdown_admissibleb s m w sh action
Runtime readiness is proved through actual effects for every outer transition, including unfinished calls. Host completion retains its snapshot.
match st with
No ready outer step can lose allocator readiness.
∀ rep requests b host st trace st′
steprep requests b host st trace st′
Explore proof 8 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary st : state trace : listevent st′ : state, steprep requests b host st trace st′ → runtime_readyst → runtime_readyst′
intros rep requests b host st trace st′ Hstep Hr
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
st :
trace :
listevent
st′ :
Hstep :
steprep requests b host st trace st′
Hr :
⊢
destruct Hstep ; simpl in * ; auto
5 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
trace :
listevent
st′ :
Hr :
M.state_readyprogram_world st
⊢
M.state_readyprogram_world st′
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
c :
s :
site :
born :
listZ
trace :
listevent
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
site = hi_site
H1 :
M.admissibleregistryrep requests H.hi_genv c w site
H2 :
H3 :
M.E.prefixprogram_putsrep requests WPtrhi_literal s c_memc w born trace s′ m′ w′
Hr :
M.state_readyprogram_world M.Runningc, s w
⊢
R.readys′ m′
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
action :
trace :
listevent
s′ :
m′ :
w′ :
sh′ :
H :
realizesb s m w sh action trace s′ m′ w′ sh′
Hr :
R.readys m
⊢
R.readys′ m′
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
action :
full :
born :
listZ
trace :
listevent
s′ :
m′ :
w′ :
actions :
liststream_action
q′ :
H :
shutdown_stepsh action full
H0 :
shutdown_readyb s m w sh
H1 :
shutdown_admissibleb s m w sh action
H2 :
M.E.prefixaction_contractb sh action action_wordsb sh action s m w born trace s′ m′ w′
H3 :
partial_outputaction shutdown_stdoutsh trace actions q′
Hr :
R.readys m
⊢
R.readys′ m′
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
action :
full :
why :
trace :
listevent
s′ :
m′ :
w′ :
actions :
liststream_action
q′ :
H :
shutdown_stepsh action full
H0 :
shutdown_readyb s m w sh
H1 :
shutdown_admissibleb s m w sh action
H2 :
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s m w trace CallResourcewhy s′ m′ w′
H3 :
partial_outputaction shutdown_stdoutsh trace actions q′
Hr :
R.readys m
⊢
R.readys′ m′
–eapply M.step_ready ; | exact H | exact Hr
5 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
trace :
listevent
st′ :
Hr :
M.state_readyprogram_world st
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
c :
s :
site :
born :
listZ
trace :
listevent
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
site = hi_site
H1 :
M.admissibleregistryrep requests H.hi_genv c w site
H2 :
H3 :
M.E.prefixprogram_putsrep requests WPtrhi_literal s c_memc w born trace s′ m′ w′
Hr :
M.state_readyprogram_world M.Runningc, s w
⊢
R.readys′ m′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
action :
trace :
listevent
s′ :
m′ :
w′ :
sh′ :
H :
realizesb s m w sh action trace s′ m′ w′ sh′
Hr :
R.readys m
⊢
R.readys′ m′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
action :
full :
born :
listZ
trace :
listevent
s′ :
m′ :
w′ :
actions :
liststream_action
q′ :
H :
shutdown_stepsh action full
H0 :
shutdown_readyb s m w sh
H1 :
shutdown_admissibleb s m w sh action
H2 :
M.E.prefixaction_contractb sh action action_wordsb sh action s m w born trace s′ m′ w′
H3 :
partial_outputaction shutdown_stdoutsh trace actions q′
Hr :
R.readys m
⊢
R.readys′ m′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
action :
full :
why :
trace :
listevent
s′ :
m′ :
w′ :
actions :
liststream_action
q′ :
H :
shutdown_stepsh action full
H0 :
shutdown_readyb s m w sh
H1 :
shutdown_admissibleb s m w sh action
H2 :
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s m w trace CallResourcewhy s′ m′ w′
H3 :
partial_outputaction shutdown_stdoutsh trace actions q′
Hr :
R.readys m
⊢
R.readys′ m′
reflexivity
4 opendeferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
c :
s :
site :
born :
listZ
trace :
listevent
s′ :
m′ :
w′ :
H :
external_siteH.hi_genv c site
H0 :
site = hi_site
H1 :
M.admissibleregistryrep requests H.hi_genv c w site
H2 :
H3 :
M.E.prefixprogram_putsrep requests WPtrhi_literal s c_memc w born trace s′ m′ w′
Hr :
M.state_readyprogram_world M.Runningc, s w
⊢
R.readys′ m′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
action :
trace :
listevent
s′ :
m′ :
w′ :
sh′ :
H :
realizesb s m w sh action trace s′ m′ w′ sh′
Hr :
R.readys m
⊢
R.readys′ m′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
action :
full :
born :
listZ
trace :
listevent
s′ :
m′ :
w′ :
actions :
liststream_action
q′ :
H :
shutdown_stepsh action full
H0 :
shutdown_readyb s m w sh
H1 :
shutdown_admissibleb s m w sh action
H2 :
M.E.prefixaction_contractb sh action action_wordsb sh action s m w born trace s′ m′ w′
H3 :
partial_outputaction shutdown_stdoutsh trace actions q′
Hr :
R.readys m
⊢
R.readys′ m′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
action :
full :
why :
trace :
listevent
s′ :
m′ :
w′ :
actions :
liststream_action
q′ :
H :
shutdown_stepsh action full
H0 :
shutdown_readyb s m w sh
H1 :
shutdown_admissibleb s m w sh action
H2 :
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s m w trace CallResourcewhy s′ m′ w′
H3 :
partial_outputaction shutdown_stdoutsh trace actions q′
Hr :
R.readys m
⊢
R.readys′ m′
–exact proj1M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ H3 Hr
3 opendeferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
action :
trace :
listevent
s′ :
m′ :
w′ :
sh′ :
H :
realizesb s m w sh action trace s′ m′ w′ sh′
Hr :
R.readys m
⊢
R.readys′ m′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
action :
full :
born :
listZ
trace :
listevent
s′ :
m′ :
w′ :
actions :
liststream_action
q′ :
H :
shutdown_stepsh action full
H0 :
shutdown_readyb s m w sh
H1 :
shutdown_admissibleb s m w sh action
H2 :
M.E.prefixaction_contractb sh action action_wordsb sh action s m w born trace s′ m′ w′
H3 :
partial_outputaction shutdown_stdoutsh trace actions q′
Hr :
R.readys m
⊢
R.readys′ m′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
action :
full :
why :
trace :
listevent
s′ :
m′ :
w′ :
actions :
liststream_action
q′ :
H :
shutdown_stepsh action full
H0 :
shutdown_readyb s m w sh
H1 :
shutdown_admissibleb s m w sh action
H2 :
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s m w trace CallResourcewhy s′ m′ w′
H3 :
partial_outputaction shutdown_stdoutsh trace actions q′
Hr :
R.readys m
⊢
R.readys′ m′
–exact proj1realizes_preserve_ _ _ _ _ _ _ _ _ _ _ H Hr
2 opendeferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
action :
full :
born :
listZ
trace :
listevent
s′ :
m′ :
w′ :
actions :
liststream_action
q′ :
H :
shutdown_stepsh action full
H0 :
shutdown_readyb s m w sh
H1 :
shutdown_admissibleb s m w sh action
H2 :
M.E.prefixaction_contractb sh action action_wordsb sh action s m w born trace s′ m′ w′
H3 :
partial_outputaction shutdown_stdoutsh trace actions q′
Hr :
R.readys m
⊢
R.readys′ m′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
action :
full :
why :
trace :
listevent
s′ :
m′ :
w′ :
actions :
liststream_action
q′ :
H :
shutdown_stepsh action full
H0 :
shutdown_readyb s m w sh
H1 :
shutdown_admissibleb s m w sh action
H2 :
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s m w trace CallResourcewhy s′ m′ w′
H3 :
partial_outputaction shutdown_stdoutsh trace actions q′
Hr :
R.readys m
⊢
R.readys′ m′
–exact proj1M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ H2 Hr
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
action :
full :
why :
trace :
listevent
s′ :
m′ :
w′ :
actions :
liststream_action
q′ :
H :
shutdown_stepsh action full
H0 :
shutdown_readyb s m w sh
H1 :
shutdown_admissibleb s m w sh action
H2 :
M.E.invokeaction_contractb sh action action_resultb sh action action_argumentsb sh action action_wordsb sh action s m w trace CallResourcewhy s′ m′ w′
H3 :
partial_outputaction shutdown_stdoutsh trace actions q′
Hr :
R.readys m
⊢
R.readys′ m′
–exact proj1M.E.invoke_preserve_ _ _ _ _ _ _ _ _ _ _ _ _ H2 Hr
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests b host st trace st′ Hstep Hr
destruct Hstep ; simpl in * ; auto
–eapply M.step_ready ; | exact H | exact Hr
reflexivity
–exact proj1M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ H3 Hr
–exact proj1realizes_preserve_ _ _ _ _ _ _ _ _ _ _ H Hr
–exact proj1M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ H2 Hr
–exact proj1M.E.invoke_preserve_ _ _ _ _ _ _ _ _ _ _ _ _ H2 Hr
Runtime readiness holds at every finite endpoint.
∀ rep requests b host st trace st′
runrep requests b host st trace st′
Explore proof 5 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary st : state trace : listevent st′ : state, runrep requests b host st trace st′ → runtime_readyst → runtime_readyst′
intros rep requests b host st trace st′ Hrun
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
st :
trace :
listevent
st′ :
Hrun :
runrep requests b host st trace st′
⊢
runtime_readyst → runtime_readyst′
induction Hrun ; auto |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
st :
trace :
listevent
mid :
tail :
listevent
last :
H :
steprep requests b host st trace mid
Hrun :
runrep requests b host mid tail last
IHHrun :
runtime_readymid → runtime_readylast
⊢
runtime_readyst → runtime_readylast
intros Hr
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
st :
trace :
listevent
mid :
tail :
listevent
last :
H :
steprep requests b host st trace mid
Hrun :
runrep requests b host mid tail last
IHHrun :
runtime_readymid → runtime_readylast
Hr :
⊢
runtime_readylast
apply IHHrun
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
st :
trace :
listevent
mid :
tail :
listevent
last :
H :
steprep requests b host st trace mid
Hrun :
runrep requests b host mid tail last
IHHrun :
runtime_readymid → runtime_readylast
Hr :
⊢
eapply step_ready ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests b host st trace st′ Hrun
induction Hrun ; auto |
intros Hr
apply IHHrun
eapply step_ready ; eauto
Only application states need the body invariant for the exit-count theorem.
match st with
_
⇒
True
Outer phase changes cannot manufacture an unsafe application state.
∀ rep requests b host st trace st′
∀s m s′ m′ w, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
steprep requests b host st trace st′
application_saferep st
application_saferep st′
Explore proof 3 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary st : state trace : listevent st′ : state, ∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w → steprep requests b host st trace st′ → application_saferep st → application_saferep st′
intros rep requests b host st trace st′ Hstable Hstep Hsafe
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
st :
trace :
listevent
st′ :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
Hstep :
steprep requests b host st trace st′
Hsafe :
application_saferep st
⊢
application_saferep st′
destruct Hstep ; simpl in * ; auto
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
trace :
listevent
st′ :
Hsafe :
body_invrep st
⊢
body_invrep st′
eapply body_step ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests b host st trace st′ Hstable Hstep Hsafe
destruct Hstep ; simpl in * ; auto
eapply body_step ; eauto
Outer transitions cannot leave application execution and later re-enter it with facts that bypass the body invariant.
∀ rep requests b host st trace st′
∀s m s′ m′ w, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
runrep requests b host st trace st′
application_saferep st
application_saferep st′
Explore proof 5 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary st : state trace : listevent st′ : state, ∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w → runrep requests b host st trace st′ → application_saferep st → application_saferep st′
intros rep requests b host st trace st′ Hstable Hrun
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
st :
trace :
listevent
st′ :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
Hrun :
runrep requests b host st trace st′
⊢
application_saferep st → application_saferep st′
induction Hrun ; auto |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace :
listevent
mid :
tail :
listevent
last :
H :
steprep requests b host st trace mid
Hrun :
runrep requests b host mid tail last
IHHrun :
application_saferep mid → application_saferep last
⊢
application_saferep st → application_saferep last
intros Hsafe
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace :
listevent
mid :
tail :
listevent
last :
H :
steprep requests b host st trace mid
Hrun :
runrep requests b host mid tail last
IHHrun :
application_saferep mid → application_saferep last
Hsafe :
application_saferep st
⊢
application_saferep last
apply IHHrun
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace :
listevent
mid :
tail :
listevent
last :
H :
steprep requests b host st trace mid
Hrun :
runrep requests b host mid tail last
IHHrun :
application_saferep mid → application_saferep last
Hsafe :
application_saferep st
⊢
application_saferep mid
eapply step_application_safe ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests b host st trace st′ Hstable Hrun
induction Hrun ; auto |
intros Hsafe
apply IHHrun
eapply step_application_safe ; eauto
The outer machine's reachable application stops use the shared panic classification too. Shutdown coverage and native realization remain independent obligations, not consequences of this finite theorem.
∀ rep requests b host st trace why ms w
∀s m s′ m′ w, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
application_saferep st
runrep requests b host st trace ApplicationM.Stoppedwhy ms w
¬failure_endingwhy
Explore proof 6 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary st : state trace : listevent why : ending ms : M.P.I.RM.mstate w : program_world, ∀s : R.state m : mem s′ : R.state m′ : mem w0 : stdio_world, R.safepoints m s′ m′ → repm w0 → stdio_readym w0 → repm′ w0 ∧ stdio_readym′ w0 → application_saferep st → runrep requests b host st trace ApplicationM.Stoppedwhy ms w → ¬failure_endingwhy
intros rep requests b host st trace why ms w Hstable Hsafe Hrun
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
st :
trace :
listevent
why :
ms :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
Hsafe :
application_saferep st
Hrun :
runrep requests b host st trace ApplicationM.Stoppedwhy ms w
⊢
¬failure_endingwhy
pose proof run_application_safe_ _ _ _ _ _ _ Hstable Hrun Hsafe as Hbody
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
st :
trace :
listevent
why :
ms :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
Hsafe :
application_saferep st
Hrun :
runrep requests b host st trace ApplicationM.Stoppedwhy ms w
Hbody :
application_saferep ApplicationM.Stoppedwhy ms w
⊢
¬failure_endingwhy
destruct Hbody as Hbody _
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
st :
trace :
listevent
why :
ms :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
Hsafe :
application_saferep st
Hrun :
runrep requests b host st trace ApplicationM.Stoppedwhy ms w
Hbody :
H.hi_body_staterep projectM.Stoppedwhy ms w
⊢
¬failure_endingwhy
apply hi_ending_not_failure
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
st :
trace :
listevent
why :
ms :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
Hsafe :
application_saferep st
Hrun :
runrep requests b host st trace ApplicationM.Stoppedwhy ms w
Hbody :
H.hi_body_staterep projectM.Stoppedwhy ms w
⊢
H.hi_endingwhy
inversion Hbody
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
st :
trace :
listevent
why :
ms :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
Hsafe :
application_saferep st
Hrun :
runrep requests b host st trace ApplicationM.Stoppedwhy ms w
Hbody :
H.hi_body_staterep projectM.Stoppedwhy ms w
why0 :
ms0 :
w0 :
H0 :
H.hi_endingwhy
H :
why0 = why
H1 :
ms0 = ms
H2 :
w0 = program_stdiow
⊢
H.hi_endingwhy
assumption
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests b host st trace why ms w Hstable Hsafe Hrun
pose proof run_application_safe_ _ _ _ _ _ _ Hstable Hrun Hsafe as Hbody
destruct Hbody as Hbody _
apply hi_ending_not_failure
inversion Hbody
assumption
Process-exit observations, separated from stdout acceptance summaries.
match trace with
Counts compose along actual runs, not by reusing cumulative puts summaries.
∀ first last
exit_countfirst ++ last = exit_countfirst + exit_countlast%nat
Explore proof 2 tactics
Initial goal
⊢
∀first last : listevent, exit_countfirst ++ last = exit_countfirst + exit_countlast%nat
induction first as | e rest IH ; intros last ; reflexivity |
e :
rest :
listevent
IH :
∀last : listevent, exit_countrest ++ last = exit_countrest + exit_countlast%nat
last :
listevent
⊢
exit_counte :: rest ++ last = exit_counte :: rest + exit_countlast%nat
destruct e ; simpl ; rewrite IH ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
induction first as | e rest IH ; intros last ; reflexivity |
destruct e ; simpl ; rewrite IH ; reflexivity
Exit-free observations contribute no process-exit count.
Explore proof 11 tactics
Initial goal
⊢
∀trace : listevent, ∀status : Z, ¬InProcessExitstatus trace → exit_counttrace = 0%nat
induction trace as | e rest IH ; intros Hfree ; reflexivity |
e :
rest :
listevent
IH :
∀status : Z, ¬InProcessExitstatus rest → exit_countrest = 0%nat
Hfree :
∀status : Z, ¬InProcessExitstatus e :: rest
⊢
exit_counte :: rest = 0%nat
destruct e ; simpl
2 openstream :
Z
bytes :
listZ
rest :
listevent
IH :
∀status : Z, ¬InProcessExitstatus rest → exit_countrest = 0%nat
Hfree :
∀status : Z, ¬InProcessExitstatus StreamBytesstream bytes :: rest
⊢
exit_countrest = 0%nat
focused goal
status :
Z
rest :
listevent
IH :
∀status : Z, ¬InProcessExitstatus rest → exit_countrest = 0%nat
Hfree :
∀status0 : Z, ¬InProcessExitstatus0 ProcessExitstatus :: rest
⊢
Sexit_countrest = 0%nat
–apply IH
2 openstream :
Z
bytes :
listZ
rest :
listevent
IH :
∀status : Z, ¬InProcessExitstatus rest → exit_countrest = 0%nat
Hfree :
∀status : Z, ¬InProcessExitstatus StreamBytesstream bytes :: rest
⊢
∀status : Z, ¬InProcessExitstatus rest
deferred goal
status :
Z
rest :
listevent
IH :
∀status : Z, ¬InProcessExitstatus rest → exit_countrest = 0%nat
Hfree :
∀status0 : Z, ¬InProcessExitstatus0 ProcessExitstatus :: rest
⊢
Sexit_countrest = 0%nat
intros status Hin
2 openstream :
Z
bytes :
listZ
rest :
listevent
IH :
∀status : Z, ¬InProcessExitstatus rest → exit_countrest = 0%nat
Hfree :
∀status : Z, ¬InProcessExitstatus StreamBytesstream bytes :: rest
status :
Z
Hin :
InProcessExitstatus rest
⊢
False
deferred goal
status :
Z
rest :
listevent
IH :
∀status : Z, ¬InProcessExitstatus rest → exit_countrest = 0%nat
Hfree :
∀status0 : Z, ¬InProcessExitstatus0 ProcessExitstatus :: rest
⊢
Sexit_countrest = 0%nat
apply Hfreestatus
2 openstream :
Z
bytes :
listZ
rest :
listevent
IH :
∀status : Z, ¬InProcessExitstatus rest → exit_countrest = 0%nat
Hfree :
∀status : Z, ¬InProcessExitstatus StreamBytesstream bytes :: rest
status :
Z
Hin :
InProcessExitstatus rest
⊢
InProcessExitstatus StreamBytesstream bytes :: rest
deferred goal
status :
Z
rest :
listevent
IH :
∀status : Z, ¬InProcessExitstatus rest → exit_countrest = 0%nat
Hfree :
∀status0 : Z, ¬InProcessExitstatus0 ProcessExitstatus :: rest
⊢
Sexit_countrest = 0%nat
right
2 openstream :
Z
bytes :
listZ
rest :
listevent
IH :
∀status : Z, ¬InProcessExitstatus rest → exit_countrest = 0%nat
Hfree :
∀status : Z, ¬InProcessExitstatus StreamBytesstream bytes :: rest
status :
Z
Hin :
InProcessExitstatus rest
⊢
InProcessExitstatus rest
deferred goal
status :
Z
rest :
listevent
IH :
∀status : Z, ¬InProcessExitstatus rest → exit_countrest = 0%nat
Hfree :
∀status0 : Z, ¬InProcessExitstatus0 ProcessExitstatus :: rest
⊢
Sexit_countrest = 0%nat
exact Hin
deferred goal
status :
Z
rest :
listevent
IH :
∀status : Z, ¬InProcessExitstatus rest → exit_countrest = 0%nat
Hfree :
∀status0 : Z, ¬InProcessExitstatus0 ProcessExitstatus :: rest
⊢
Sexit_countrest = 0%nat
–exfalso
status :
Z
rest :
listevent
IH :
∀status : Z, ¬InProcessExitstatus rest → exit_countrest = 0%nat
Hfree :
∀status0 : Z, ¬InProcessExitstatus0 ProcessExitstatus :: rest
⊢
False
apply Hfreestatus
status :
Z
rest :
listevent
IH :
∀status : Z, ¬InProcessExitstatus rest → exit_countrest = 0%nat
Hfree :
∀status0 : Z, ¬InProcessExitstatus0 ProcessExitstatus :: rest
⊢
InProcessExitstatus ProcessExitstatus :: rest
left
status :
Z
rest :
listevent
IH :
∀status : Z, ¬InProcessExitstatus rest → exit_countrest = 0%nat
Hfree :
∀status0 : Z, ¬InProcessExitstatus0 ProcessExitstatus :: rest
⊢
ProcessExitstatus = ProcessExitstatus
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
induction trace as | e rest IH ; intros Hfree ; reflexivity |
destruct e ; simpl
–apply IH
intros status Hin
apply Hfreestatus
right
exact Hin
–exfalso
apply Hfreestatus
left
reflexivity
Any exit-bearing step is exactly a one-shot transition into Finished.
∀ rep requests b host st trace st′
steprep requests b host st trace st′
application_saferep st
exit_counttrace = O ∨ ∃s m w sh, st′ = Finisheds m w sh ∧ exit_counttrace = 1%nat
Proof 29 steps Qed
intros rep requests b host st trace st′ Hstep Hsafe
destruct Hstep ; simpl in *
–left
reflexivity
–right
do 4 eexists
split ; reflexivity
Finite runs from Finished are empty: the host witness cannot be replayed.
Explore proof 4 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary s : R.state m : mem w : stdio_world sh : shutdown_state trace : listevent st : state, runrep requests b host Finisheds m w sh trace st → trace = [ ]
intros rep requests b host s m w sh trace st Hrun
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
trace :
listevent
st :
⊢
trace = [ ]
inversion Hrun ; subst ; auto
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
st :
trace0, tail :
listevent
mid :
H0 :
runrep requests b host mid tail st
⊢
trace0 ++ tail = [ ]
exfalso
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
s :
m :
w :
sh :
st :
trace0, tail :
listevent
mid :
H0 :
runrep requests b host mid tail st
⊢
False
eapply finished_terminal ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests b host s m w sh trace st Hrun
inversion Hrun ; subst ; auto
exfalso
eapply finished_terminal ; eauto
Every represented finite execution has at most one process-exit event. This is not a promise that a handoff or process exit is ever reached.
∀ rep requests b host st trace st′
∀s m s′ m′ w, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
runrep requests b host st trace st′
application_saferep st
exit_counttrace ≤ 1%nat
Explore proof 12 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop b : shutdown_boundary host : host_boundary st : state trace : listevent st′ : state, ∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w → runrep requests b host st trace st′ → application_saferep st → exit_counttrace ≤ 1%nat
intros rep requests b host st trace st′ Hstable Hrun
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
st :
trace :
listevent
st′ :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
Hrun :
runrep requests b host st trace st′
⊢
application_saferep st → exit_counttrace ≤ 1%nat
induction Hrun ; simpl ; lia |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace :
listevent
mid :
tail :
listevent
last :
H :
steprep requests b host st trace mid
Hrun :
runrep requests b host mid tail last
IHHrun :
application_saferep mid → exit_counttail ≤ 1%nat
⊢
application_saferep st → exit_counttrace ++ tail ≤ 1%nat
intros Hsafe
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace :
listevent
mid :
tail :
listevent
last :
H :
steprep requests b host st trace mid
Hrun :
runrep requests b host mid tail last
IHHrun :
application_saferep mid → exit_counttail ≤ 1%nat
Hsafe :
application_saferep st
⊢
exit_counttrace ++ tail ≤ 1%nat
rewrite exit_count_app
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace :
listevent
mid :
tail :
listevent
last :
H :
steprep requests b host st trace mid
Hrun :
runrep requests b host mid tail last
IHHrun :
application_saferep mid → exit_counttail ≤ 1%nat
Hsafe :
application_saferep st
⊢
exit_counttrace + exit_counttail ≤ 1%nat
destruct step_exit_shape_ _ _ _ _ _ _ H Hsafe as Hz | s & m & w & sh & → & Hone
2 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace :
listevent
mid :
tail :
listevent
last :
H :
steprep requests b host st trace mid
Hrun :
runrep requests b host mid tail last
IHHrun :
application_saferep mid → exit_counttail ≤ 1%nat
Hsafe :
application_saferep st
Hz :
exit_counttrace = 0%nat
⊢
exit_counttrace + exit_counttail ≤ 1%nat
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace, tail :
listevent
last :
s :
m :
w :
sh :
IHHrun :
application_saferep Finisheds m w sh → exit_counttail ≤ 1%nat
Hsafe :
application_saferep st
Hone :
exit_counttrace = 1%nat
⊢
exit_counttrace + exit_counttail ≤ 1%nat
–rewrite Hz
2 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace :
listevent
mid :
tail :
listevent
last :
H :
steprep requests b host st trace mid
Hrun :
runrep requests b host mid tail last
IHHrun :
application_saferep mid → exit_counttail ≤ 1%nat
Hsafe :
application_saferep st
Hz :
exit_counttrace = 0%nat
⊢
0 + exit_counttail ≤ 1%nat
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace, tail :
listevent
last :
s :
m :
w :
sh :
IHHrun :
application_saferep Finisheds m w sh → exit_counttail ≤ 1%nat
Hsafe :
application_saferep st
Hone :
exit_counttrace = 1%nat
⊢
exit_counttrace + exit_counttail ≤ 1%nat
simpl
2 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace :
listevent
mid :
tail :
listevent
last :
H :
steprep requests b host st trace mid
Hrun :
runrep requests b host mid tail last
IHHrun :
application_saferep mid → exit_counttail ≤ 1%nat
Hsafe :
application_saferep st
Hz :
exit_counttrace = 0%nat
⊢
exit_counttail ≤ 1%nat
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace, tail :
listevent
last :
s :
m :
w :
sh :
IHHrun :
application_saferep Finisheds m w sh → exit_counttail ≤ 1%nat
Hsafe :
application_saferep st
Hone :
exit_counttrace = 1%nat
⊢
exit_counttrace + exit_counttail ≤ 1%nat
apply IHHrun
2 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace :
listevent
mid :
tail :
listevent
last :
H :
steprep requests b host st trace mid
Hrun :
runrep requests b host mid tail last
IHHrun :
application_saferep mid → exit_counttail ≤ 1%nat
Hsafe :
application_saferep st
Hz :
exit_counttrace = 0%nat
⊢
application_saferep mid
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace, tail :
listevent
last :
s :
m :
w :
sh :
IHHrun :
application_saferep Finisheds m w sh → exit_counttail ≤ 1%nat
Hsafe :
application_saferep st
Hone :
exit_counttrace = 1%nat
⊢
exit_counttrace + exit_counttail ≤ 1%nat
eapply step_application_safe ; eauto
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace, tail :
listevent
last :
s :
m :
w :
sh :
IHHrun :
application_saferep Finisheds m w sh → exit_counttail ≤ 1%nat
Hsafe :
application_saferep st
Hone :
exit_counttrace = 1%nat
⊢
exit_counttrace + exit_counttail ≤ 1%nat
–rewrite Hone , finished_run_ _ _ _ _ _ _ _ _ _ Hrun
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace, tail :
listevent
last :
s :
m :
w :
sh :
IHHrun :
application_saferep Finisheds m w sh → exit_counttail ≤ 1%nat
Hsafe :
application_saferep st
Hone :
exit_counttrace = 1%nat
⊢
1 + exit_count[ ] ≤ 1%nat
simpl
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
st :
trace, tail :
listevent
last :
s :
m :
w :
sh :
IHHrun :
application_saferep Finisheds m w sh → exit_counttail ≤ 1%nat
Hsafe :
application_saferep st
Hone :
exit_counttrace = 1%nat
⊢
1 ≤ 1%nat
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests b host st trace st′ Hstable Hrun
induction Hrun ; simpl ; lia |
intros Hsafe
rewrite exit_count_app
destruct step_exit_shape_ _ _ _ _ _ _ H Hsafe as Hz | s & m & w & sh & → & Hone
Public conditional-composition checks
These fixtures realize only identity memory segments, not native libc.
Initial logical stdout with no user exit registrations in this fixture.
The actual initialized main body inhabits the stronger application invariant.
Explore proof 2 tactics
Initial goal
split ; apply P.H.hi_body_entry ; exact HiChecks.entry_pre |
split ; split ; exact stdout_initial_wf | constructor | discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; apply P.H.hi_body_entry ; exact HiChecks.entry_pre |
split ; split ; exact stdout_initial_wf | constructor | discriminate
Stronger preconditions remain independently admissible for every reached call.
681Example all_rich_calls_admissible: ∀trace c s w site, P.M.runP.registryfixture_rep fixture_requests P.H.hi_genv P.M.Runninghi_entryHiChecks.memory 10, InterpRuntime.start initial_world trace P.M.Runningc, s w → external_siteP.H.hi_genv c site → P.M.admissibleP.registryfixture_rep fixture_requests P.H.hi_genv c w site
Explore proof 2 tactics
Initial goal
⊢
∀trace : listevent c : config s : InterpRuntime.state w : program_world site : call_site, P.M.runP.registryfixture_rep fixture_requests P.H.hi_genv P.M.Runninghi_entryHiChecks.memory 10, InterpRuntime.start initial_world trace P.M.Runningc, s w → external_siteP.H.hi_genv c site → P.M.admissibleP.registryfixture_rep fixture_requests P.H.hi_genv c w site
intros trace c s w site Hrun Hsite
eapply P.all_calls_admissible ; apply HiChecks.interpreter_stdio_stable | exact initial_body | exact Hrun | exact Hsite
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros trace c s w site Hrun Hsite
eapply P.all_calls_admissible ; apply HiChecks.interpreter_stdio_stable | exact initial_body | exact Hrun | exact Hsite
Even a single distinct-token callback cannot appear at a reached call when this selected entry supplied no registrations.
693Example changed_inventory_not_reached: ∀trace m fuel s w entry, program_pendingw = entry → ¬P.M.runP.registryfixture_rep fixture_requests P.H.hi_genv P.M.Runninghi_entryHiChecks.memory 10, InterpRuntime.start initial_world trace P.M.Runninghi_callm fuel, s w
Explore proof 5 tactics
Initial goal
⊢
∀trace : listevent m : mem fuel : Z s : InterpRuntime.state w : program_world entry : registration, program_pendingw = entry → ¬P.M.runP.registryfixture_rep fixture_requests P.H.hi_genv P.M.Runninghi_entryHiChecks.memory 10, InterpRuntime.start initial_world trace P.M.Runninghi_callm fuel, s w
intros trace m fuel s w entry Hp Hrun
⊢
False
pose proof P.body_run_inventory_ _ HiChecks.interpreter_stdio_stablefixture_rep _ _ _ Hrun initial_body as Hsame
⊢
False
simpl in Hsame
⊢
False
rewrite Hp in Hsame
⊢
False
discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros trace m fuel s w entry Hp Hrun
pose proof P.body_run_inventory_ _ HiChecks.interpreter_stdio_stablefixture_rep _ _ _ Hrun initial_body as Hsame
simpl in Hsame
rewrite Hp in Hsame
discriminate
Zero fuel stops at entry, without calling puts or starting shutdown.
706Example zero_fuel_leaf: ∀b host, P.stepfixture_rep fixture_requests b host P.ApplicationP.M.Runninghi_entryHiChecks.memory 0, InterpRuntime.start initial_world [ ] P.ApplicationP.M.StoppedCoreEndOutOfFuel hi_entryHiChecks.memory 0, InterpRuntime.start initial_world
Explore proof 6 tactics
Initial goal
intros b host
apply P.program_application
apply P.M.step_core_end ; | reflexivity
host :
⊢
∀site : call_site, ¬external_siteP.H.hi_genv hi_entryHiChecks.memory 0 site
intros site Hsite
host :
site :
Hsite :
⊢
False
pose proof external_site_stuck_ _ _ Hsite as Hbad
⊢
False
discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros b host
apply P.program_application
apply P.M.step_core_end ; | reflexivity
intros site Hsite
pose proof external_site_stuck_ _ _ Hsite as Hbad
discriminate
With any fuel, every stopped application endpoint of this actual entry is nonfailure, including return, fuel and resource leaves.
718Example all_outer_application_stops_safe: ∀fuel b host trace why ms w, P.runfixture_rep fixture_requests b host P.ApplicationP.M.Runninghi_entryHiChecks.memory fuel, InterpRuntime.start initial_world trace P.ApplicationP.M.Stoppedwhy ms w → ¬failure_endingwhy
Explore proof 4 tactics
Initial goal
⊢
∀fuel : Z b : P.shutdown_boundary host : P.host_boundary trace : listevent why : ending ms : P.M.P.I.RM.mstate w : program_world, P.runfixture_rep fixture_requests b host P.ApplicationP.M.Runninghi_entryHiChecks.memory fuel, InterpRuntime.start initial_world trace P.ApplicationP.M.Stoppedwhy ms w → ¬failure_endingwhy
intros fuel b host trace why ms w Hrun
⊢
¬failure_endingwhy
eapply P.application_stopped_never_panics ; apply HiChecks.interpreter_stdio_stable | | exact Hrun
split ; apply P.H.hi_body_entry ; exact HiChecks.entry_pre |
split ; split ; exact stdout_initial_wf | constructor | discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros fuel b host trace why ms w Hrun
eapply P.application_stopped_never_panics ; apply HiChecks.interpreter_stdio_stable | | exact Hrun
split ; apply P.H.hi_body_entry ; exact HiChecks.entry_pre |
split ; split ; exact stdout_initial_wf | constructor | discriminate
A segment with no memory authority; endpoint relations are deliberately trivial only for this logical fixture. Native realization remains open.
mkContractstdio_world RVoid λ_ _ ⇒ True λ_ _ _ ⇒ True λ_ _ _ ⇒ [ ] λ_ _ _ ⇒ [ ] λ_ _ _ ⇒ [ ] λ_ _ _ _ _ ⇒ False λ_ _ _ _ _ _ _ ⇒ True λ_ _ _ _ _ _ _ _ ⇒ True λ_ ⇒ False λ_ ⇒ False
Fixture readiness does not assert the validity of any native callback.
P.mkShutdownBoundaryλ_ _ _ _ ⇒ True λ_ _ ⇒ segment λ_ _ ⇒ CVoid λ_ _ ⇒ [ ] λ_ _ ⇒ [ ] λ_ _ _ _ _ _ _ _ _ _ _ ⇒ True
The selected fixture segments are admissible independently of effects.
Explore proof 2 tactics
Initial goal
intros s m w sh action sh′ Hr Hstep
⊢
P.shutdown_admissibleboundary s m w sh action
split ; exact I
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros s m w sh action sh′ Hr Hstep
split ; exact I
A lifecycle edge with no acceptance is realized with an actual empty effect path and the exact same runtime/memory/stdio snapshot.
∀ s m w sh action sh′
shutdown_stepsh action sh′
P.action_eventsaction = [ ]
P.realizesboundary s m w sh action [ ] s m w sh′
Explore proof 3 tactics
Initial goal
⊢
∀s : InterpRuntime.state m : mem w : stdio_world sh : shutdown_state action : shutdown_action sh′ : shutdown_state, shutdown_stepsh action sh′ → P.action_eventsaction = [ ] → P.realizesboundary s m w sh action [ ] s m w sh′
intros s m w sh action sh′ Hstep Htrace
⊢
P.realizesboundary s m w sh action [ ] s m w sh′
eapply P.realize_action with born := [ ] ; exact Hstep | exact I | split ; exact I | | exact I | symmetry ; exact Htrace | exact I
⊢
P.M.E.prefixP.action_contractboundary sh action P.action_wordsboundary sh action s m w [ ] [ ] s m w
split ; constructor | exact I
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros s m w sh action sh′ Hstep Htrace
eapply P.realize_action with born := [ ] ; exact Hstep | exact I | split ; exact I | | exact I | symmetry ; exact Htrace | exact I
split ; constructor | exact I
No callbacks: the exact pending bytes survive TLS/handlers/cleanup to soft handoff. This fixture does not promise lossless flushing.
∀ s m w q host
P.runfixture_rep fixture_requests boundary host P.ShuttingDowns m w mkShutdownTls 0 [ ] [ ] q [ ] P.ShuttingDowns m w mkShutdownHandedOffSoftExit 0 [ ] [ ] q
Explore proof 5 tactics
Initial goal
⊢
∀s : InterpRuntime.state m : mem w : stdio_world q : stream_state host : P.host_boundary, P.runfixture_rep fixture_requests boundary host P.ShuttingDowns m w shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q [ ] P.ShuttingDowns m w shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q
intros s m w q host
⊢
P.runfixture_rep fixture_requests boundary host P.ShuttingDowns m w shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q [ ] P.ShuttingDowns m w shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q
eapply P.program_next with trace := [ ] tail := [ ] ; apply P.program_shutdown with action := EmptyTls ; apply silent_realization ; constructor | reflexivity |
⊢
P.runfixture_rep fixture_requests boundary host P.ShuttingDowns m w shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q [ ] P.ShuttingDowns m w shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q
eapply P.program_next with trace := [ ] tail := [ ] ; apply P.program_shutdown with action := StartCleanup ; apply silent_realization ; constructor | reflexivity |
⊢
P.runfixture_rep fixture_requests boundary host P.ShuttingDowns m w shutdown_at ≔ Cleanup; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q [ ] P.ShuttingDowns m w shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q
eapply P.program_next with trace := [ ] tail := [ ] ; apply P.program_shutdown with action := HandoffSoftExit 0 ; apply silent_realization ; constructor | reflexivity |
⊢
P.runfixture_rep fixture_requests boundary host P.ShuttingDowns m w shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q [ ] P.ShuttingDowns m w shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q
constructor
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros s m w q host
eapply P.program_next with trace := [ ] tail := [ ] ; apply P.program_shutdown with action := EmptyTls ; apply silent_realization ; constructor | reflexivity |
eapply P.program_next with trace := [ ] tail := [ ] ; apply P.program_shutdown with action := StartCleanup ; apply silent_realization ; constructor | reflexivity |
eapply P.program_next with trace := [ ] tail := [ ] ; apply P.program_shutdown with action := HandoffSoftExit 0 ; apply silent_realization ; constructor | reflexivity |
constructor
Returning main transfers the same stdout obligations, not a fresh stream.
778Example main_to_exact_shutdown: ∀s m q host, P.stepfixture_rep fixture_requests boundary host P.ApplicationP.M.RunningP.H.hi_returnm 9 [ ], s mkProgramWorldhello_world q [ ] [ ] P.ShuttingDowns m hello_world mkShutdownTls 0 [ ] [ ] q
Explore proof 4 tactics
Initial goal
⊢
∀s : InterpRuntime.state m : mem q : stream_state host : P.host_boundary, P.stepfixture_rep fixture_requests boundary host P.ApplicationP.M.RunningP.H.hi_returnm 9 [ ], s program_stdio ≔ hello_world; program_stdout ≔ q; program_pending ≔ [ ] [ ] P.ShuttingDowns m hello_world shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q
intros s m q host
⊢
P.stepfixture_rep fixture_requests boundary host P.ApplicationP.M.RunningP.H.hi_returnm 9 [ ], s program_stdio ≔ hello_world; program_stdout ≔ q; program_pending ≔ [ ] [ ] P.ShuttingDowns m hello_world shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q
apply P.program_main_return with bits := 0 ; | exact I
⊢
main_return_siteP.H.hi_genv P.H.hi_returnm 9 [ ] 0
exists TAtom"start", Const0
⊢
fr_atc_frameP.H.hi_returnm 9 [ ] = ExecTAtom"start" [ ] JRetConst0 ∧ fr_doomedc_frameP.H.hi_returnm 9 [ ] = None ∧ fr_localsc_frameP.H.hi_returnm 9 [ ] = [ ] ∧ c_callersP.H.hi_returnm 9 [ ] = [ ] ∧ fn_retfr_fnc_frameP.H.hi_returnm 9 [ ] = RClassW ∧ value_xP.H.hi_genv fr_envc_frameP.H.hi_returnm 9 [ ] W Const0 = SomeWInt0
repeat split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Host completion is consumed into an outer terminal, even when its logical witness remains reusable as a proposition.
789Example complete_once: ∀s m w q, P.stepfixture_rep fixture_requests boundary λ_ _ _ _ ⇒ True P.ShuttingDowns m w mkShutdownHandedOffSoftExit 0 [ ] [ ] q ProcessExit0 P.Finisheds m w mkShutdownHandedOffSoftExit 0 [ ] [ ] q ∧ ∀trace st, ¬P.stepfixture_rep fixture_requests boundary λ_ _ _ _ ⇒ True P.Finisheds m w mkShutdownHandedOffSoftExit 0 [ ] [ ] q trace st
Explore proof 2 tactics
Initial goal
⊢
∀s : InterpRuntime.state m : mem w : stdio_world q : stream_state, P.stepfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.ShuttingDowns m w shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q ProcessExit0 P.Finisheds m w shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q ∧ ∀trace : listevent st : P.state, ¬P.stepfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.Finisheds m w shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q trace st
intros s m w q
⊢
P.stepfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.ShuttingDowns m w shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q ProcessExit0 P.Finisheds m w shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q ∧ ∀trace : listevent st : P.state, ¬P.stepfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.Finisheds m w shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q trace st
split ; apply P.program_complete ; exact I | apply P.finished_terminal
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros s m w q
split ; apply P.program_complete ; exact I | apply P.finished_terminal
Accepting output in a callback cannot be realized by a silent trace.
Explore proof 3 tactics
Initial goal
⊢
∀s : InterpRuntime.state m : mem w : stdio_world sh : shutdown_state s′ : InterpRuntime.state m′ : mem w′ : stdio_world sh′ : shutdown_state, ¬P.realizesboundary s m w sh ShutdownOutputAccept65 [ ] s′ m′ w′ sh′
intros s m w sh s′ m′ w′ sh′ H
⊢
False
inversion H
m :
w :
sh :
m′ :
w′ :
sh′ :
H :
P.realizesboundary s m w sh ShutdownOutputAccept65 [ ] s′ m′ w′ sh′
m0 :
w0 :
sh0 :
action :
trace :
listevent
s'0 :
m'0 :
w'0 :
sh'0 :
born :
listZ
H0 :
shutdown_stepsh ShutdownOutputAccept65 sh′
H1 :
P.shutdown_readyboundary s m w sh
H2 :
H3 :
P.M.E.prefixP.action_contractboundary sh ShutdownOutputAccept65 P.action_wordsboundary sh ShutdownOutputAccept65 s m w born [ ] s′ m′ w′
H4 :
P.action_postboundary sh ShutdownOutputAccept65 s m w born [ ] s′ m′ w′ sh′
H5 :
H6 :
P.shutdown_readyboundary s′ m′ w′ sh′
H7 :
s0 = s
H8 :
m0 = m
H9 :
w0 = w
H10 :
sh0 = sh
H11 :
action = ShutdownOutputAccept65
H12 :
trace = [ ]
H13 :
s'0 = s′
H14 :
m'0 = m′
H15 :
w'0 = w′
H16 :
sh'0 = sh′
⊢
False
discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros s m w sh s′ m′ w′ sh′ H
inversion H
discriminate
This fixture keeps accepted hello bytes outstanding; delivery is a separate obligation even if the host-completion predicate is granted.
mkStreamByteOriented hello_bytes ++ 10 false
An inhabited returning puts with the exact logical endpoint used below.
Proof 42 steps Qed
destruct HiChecks.entry_pre as Hr Hw Hl
pose proof P.H.hi_literal_checkedHiChecks.memory Hl as Hstr
assert Hpost : puts_stream_postWPtrhi_literal HiChecks.memory stdout_initial StreamBytes1 hello_bytes ++ 10 CallReturnWInt6 buffered
{exists hi_literal, hello_bytes, Accepthello_bytes ++ 10, 6
split ; reflexivity |
split ; exact Hstr |
split ; exact puts_buffered_acceptance | split ; reflexivity
eapply P.M.E.invoke_normal with born := [ ]
–split
+split ; split ; exact stdout_initial_wf | constructor | discriminate
–split ; constructor |
split
+split ; exact Hr |
split ; exact Hw |
split
∗apply stdio_delegates_refl ; reflexivity | exact proj2Hw
∗right
exists hi_literal, hello_bytes, hello_bytes ++ 10, [ ] : listZ
split ; reflexivity |
split ; exact Hstr |
split ; reflexivity
+split ; reflexivity |
eapply P.C.program_post_prefix ; exact Hpost
–split ; | exact Hpost
–intros why Hbad
discriminate
–intros values Heq
injection Heq as ←
split
+exists WInt6
split ; reflexivity
+constructor ; exact I | constructor
–intros status Hbad
discriminate
A complete represented path through actual main entry/copy/call/return, logical shutdown and one host-completion event. This is not native adequacy.
845Example hi_entry_to_host: P.runfixture_rep fixture_requests boundary λ_ _ _ _ ⇒ True P.ApplicationP.M.Runninghi_entryHiChecks.memory 10, InterpRuntime.start initial_world StreamBytes1 hello_bytes ++ 10; ProcessExit0 P.FinishedInterpRuntime.start HiChecks.memory hello_world mkShutdownHandedOffSoftExit 0 [ ] [ ] buffered
Explore proof 11 tactics
Initial goal
⊢
P.runfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.ApplicationP.M.Runninghi_entryHiChecks.memory 10, InterpRuntime.start initial_world StreamBytes1 hello_bytes ++ 10; ProcessExit0 P.FinishedInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered
eapply P.run_trans with first := StreamBytes1 hello_bytes ++ 10 last := ProcessExit0 mid := P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world mkShutdownTls 0 [ ] [ ] buffered
2 open⊢
P.runfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.ApplicationP.M.Runninghi_entryHiChecks.memory 10, InterpRuntime.start initial_world StreamBytes1 hello_bytes ++ 10 P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered
focused goal
⊢
P.runfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered ProcessExit0 P.FinishedInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered
–change P.runfixture_rep fixture_requests boundary λ_ _ _ _ ⇒ True P.ApplicationP.M.Runninghi_entryHiChecks.memory 10, InterpRuntime.start initial_world [ ] ++ StreamBytes1 hello_bytes ++ 10 P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world mkShutdownTls 0 [ ] [ ] buffered
2 open⊢
P.runfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.ApplicationP.M.Runninghi_entryHiChecks.memory 10, InterpRuntime.start initial_world [ ] ++ StreamBytes1 hello_bytes ++ 10 P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered
deferred goal
⊢
P.runfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered ProcessExit0 P.FinishedInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered
eapply P.returning_puts_shutdown with first := [ ] w′ := mkProgramWorldhello_world buffered [ ]
9 openfocused goal
focused goal
deferred goal
⊢
P.runfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered ProcessExit0 P.FinishedInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered
shelved goal
shelved goal
⊢
shelved goal
shelved goal
⊢
Z
shelved goal
⊢
Z
+intros first s m w fuel trace n s′ m′ w′ Hreach Hcall
9 open⊢
P.shutdown_readyboundary s′ m′ program_stdiow′ shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ program_pendingw′; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ program_stdoutw′
deferred goal
deferred goal
deferred goal
⊢
P.runfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered ProcessExit0 P.FinishedInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered
shelved goal
shelved goal
⊢
shelved goal
shelved goal
⊢
Z
shelved goal
⊢
Z
exact I
8 opendeferred goal
deferred goal
deferred goal
⊢
P.runfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered ProcessExit0 P.FinishedInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered
shelved goal
shelved goal
⊢
shelved goal
shelved goal
⊢
Z
shelved goal
⊢
Z
+apply P.H.hi_reaches_call
4 open⊢
10 ≠ 0
deferred goal
⊢
P.M.E.invokeprogram_putsfixture_rep fixture_requests site_resulthi_site site_argshi_site WPtrhi_literal InterpRuntime.start HiChecks.memory initial_world StreamBytes1 hello_bytes ++ 10 CallReturnWInt InterpRuntime.start HiChecks.memory program_stdio ≔ hello_world; program_stdout ≔ buffered; program_pending ≔ [ ]
deferred goal
⊢
P.runfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered ProcessExit0 P.FinishedInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered
shelved goal
⊢
Z
lia
3 opendeferred goal
⊢
P.M.E.invokeprogram_putsfixture_rep fixture_requests site_resulthi_site site_argshi_site WPtrhi_literal InterpRuntime.start HiChecks.memory initial_world StreamBytes1 hello_bytes ++ 10 CallReturnWInt InterpRuntime.start HiChecks.memory program_stdio ≔ hello_world; program_stdout ≔ buffered; program_pending ≔ [ ]
deferred goal
⊢
P.runfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered ProcessExit0 P.FinishedInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered
shelved goal
⊢
Z
+exact buffered_puts
deferred goal
⊢
P.runfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered ProcessExit0 P.FinishedInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered
–eapply P.run_trans with first := [ ] last := ProcessExit0
3 open⊢
P.runfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered [ ]
focused goal
⊢
P.runfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True ProcessExit0 P.FinishedInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered
shelved goal
+apply fixture_shutdown
deferred goal
⊢
P.runfixture_rep fixture_requests boundary λ_ : InterpRuntime.state _ : mem _ : stdio_world _ : shutdown_state ⇒ True P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered ProcessExit0 P.FinishedInterpRuntime.start HiChecks.memory hello_world shutdown_at ≔ HandedOffSoftExit; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ buffered
+eapply P.program_next with trace := ProcessExit0 tail := [ ] ; apply P.program_complete ; exact I | constructor
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
eapply P.run_trans with first := StreamBytes1 hello_bytes ++ 10 last := ProcessExit0 mid := P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world mkShutdownTls 0 [ ] [ ] buffered
–change P.runfixture_rep fixture_requests boundary λ_ _ _ _ ⇒ True P.ApplicationP.M.Runninghi_entryHiChecks.memory 10, InterpRuntime.start initial_world [ ] ++ StreamBytes1 hello_bytes ++ 10 P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world mkShutdownTls 0 [ ] [ ] buffered
eapply P.returning_puts_shutdown with first := [ ] w′ := mkProgramWorldhello_world buffered [ ]
+intros first s m w fuel trace n s′ m′ w′ Hreach Hcall
exact I
+apply P.H.hi_reaches_call
lia
+exact buffered_puts
–eapply P.run_trans with first := [ ] last := ProcessExit0
+apply fixture_shutdown
+eapply P.program_next with trace := ProcessExit0 tail := [ ] ; apply P.program_complete ; exact I | constructor
Partial controls have no successful endpoint premise. This fixture deliberately makes Handlers unready and every action post false.
P.mkShutdownBoundaryλ_ _ _ sh ⇒ shutdown_atsh = Tls λ_ _ ⇒ segment λ_ _ ⇒ CVoid λ_ _ ⇒ [ ] λ_ _ ⇒ [ ] λ_ _ _ _ _ _ _ _ _ _ _ ⇒ False
An empty unfinished TLS segment exists although the complete target is unready and cannot satisfy the selected action's postcondition.
880Example unfinished_without_completion: ∀s m w q host, P.stepfixture_rep fixture_requests prefix_boundary host P.ShuttingDowns m w mkShutdownTls 0 [ ] [ ] q [ ] P.ShutdownUnfinisheds m w mkShutdownTls 0 [ ] [ ] q EmptyTls [ ] q ∧ ¬P.shutdown_readyprefix_boundary s m w mkShutdownHandlers 0 [ ] [ ] q
Explore proof 9 tactics
Initial goal
⊢
∀s : InterpRuntime.state m : mem w : stdio_world q : stream_state host : P.host_boundary, P.stepfixture_rep fixture_requests prefix_boundary host P.ShuttingDowns m w shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q [ ] P.ShutdownUnfinisheds m w shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls [ ] q ∧ ¬P.shutdown_readyprefix_boundary s m w shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q
intros s m w q host
⊢
P.stepfixture_rep fixture_requests prefix_boundary host P.ShuttingDowns m w shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q [ ] P.ShutdownUnfinisheds m w shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls [ ] q ∧ ¬P.shutdown_readyprefix_boundary s m w shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q
split ; | discriminate
⊢
P.stepfixture_rep fixture_requests prefix_boundary host P.ShuttingDowns m w shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q [ ] P.ShutdownUnfinisheds m w shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls [ ] q
eapply P.program_shutdown_unfinished with born := [ ] full := mkShutdownHandlers 0 [ ] [ ] q
5 open⊢
shutdown_stepshutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls shutdown_at ≔ Handlers; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q
focused goal
⊢
P.shutdown_readyprefix_boundary s m w shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q
focused goal
⊢
P.shutdown_admissibleprefix_boundary s m w shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls
focused goal
⊢
P.M.E.prefixP.action_contractprefix_boundary shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls P.action_wordsprefix_boundary shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls s m w [ ] [ ] s m w
focused goal
⊢
P.partial_outputEmptyTls shutdown_stdoutshutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q [ ] [ ] q
–constructor
4 opendeferred goal
⊢
P.shutdown_readyprefix_boundary s m w shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q
deferred goal
⊢
P.shutdown_admissibleprefix_boundary s m w shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls
deferred goal
⊢
P.M.E.prefixP.action_contractprefix_boundary shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls P.action_wordsprefix_boundary shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls s m w [ ] [ ] s m w
deferred goal
⊢
P.partial_outputEmptyTls shutdown_stdoutshutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q [ ] [ ] q
–reflexivity
3 opendeferred goal
⊢
P.shutdown_admissibleprefix_boundary s m w shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls
deferred goal
⊢
P.M.E.prefixP.action_contractprefix_boundary shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls P.action_wordsprefix_boundary shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls s m w [ ] [ ] s m w
deferred goal
⊢
P.partial_outputEmptyTls shutdown_stdoutshutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q [ ] [ ] q
–split ; exact I
2 opendeferred goal
⊢
P.M.E.prefixP.action_contractprefix_boundary shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls P.action_wordsprefix_boundary shutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q EmptyTls s m w [ ] [ ] s m w
deferred goal
⊢
P.partial_outputEmptyTls shutdown_stdoutshutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q [ ] [ ] q
–split ; constructor | exact I
deferred goal
⊢
P.partial_outputEmptyTls shutdown_stdoutshutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q [ ] [ ] q
–split ; reflexivity |
⊢
stream_runshutdown_stdoutshutdown_at ≔ Tls; shutdown_status ≔ 0; shutdown_pending ≔ [ ]; shutdown_consumed ≔ [ ]; shutdown_stdout ≔ q [ ] q ∧ [ ] = [ ]
split ; constructor | reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros s m w q host
split ; | discriminate
eapply P.program_shutdown_unfinished with born := [ ] full := mkShutdownHandlers 0 [ ] [ ] q
–constructor
–reflexivity
–split ; exact I
–split ; constructor | exact I
–split ; reflexivity |
split ; constructor | reflexivity
A partial delivery settles only the oldest selected bytes and preserves an existing error, without claiming the action completed.
898Example partial_delivery_exact: P.partial_outputShutdownOutputDeliver65; 66 mkStreamByteOriented 65; 66; 67 true [ ] Deliver65 mkStreamByteOriented 66; 67 true
Explore proof 4 tactics
Initial goal
⊢
P.partial_outputShutdownOutputDeliver65; 66 orientation ≔ ByteOriented; outstanding ≔ 65; 66; 67; stream_error ≔ true [ ] Deliver65 orientation ≔ ByteOriented; outstanding ≔ 66; 67; stream_error ≔ true
split
2 openfocused goal
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; 66; 67; stream_error ≔ true Deliver65 orientation ≔ ByteOriented; outstanding ≔ 66; 67; stream_error ≔ true ∧ [ ] = [ ]
–split ; constructor ; exists 65 ; reflexivity | constructor | exists 66 ; reflexivity
deferred goal
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; 66; 67; stream_error ≔ true Deliver65 orientation ≔ ByteOriented; outstanding ≔ 66; 67; stream_error ≔ true ∧ [ ] = [ ]
–split ; | reflexivity
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; 66; 67; stream_error ≔ true Deliver65 orientation ≔ ByteOriented; outstanding ≔ 66; 67; stream_error ≔ true
eapply stream_next ; exact stream_deliver65 66; 67 true ltac:discriminate | constructor
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split
–split ; constructor ; exists 65 ; reflexivity | constructor | exists 66 ; reflexivity
–split ; | reflexivity
eapply stream_next ; exact stream_deliver65 66; 67 true ltac:discriminate | constructor
Control/hidden output, excess acceptance, non-FIFO delivery and delivery/discard substitution are not admitted partial observations.
911Example incompatible_partial_output: ¬P.partial_outputEmptyTls stdout_initial StreamBytes1 65 Accept65 mkStreamByteOriented 65 false ∧ ¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial StreamBytes1 65; 66; 67 Accept65; 66; 67 mkStreamByteOriented 65; 66; 67 false ∧ ¬P.partial_outputShutdownOutputDeliver66; 65 mkStreamByteOriented 65; 66 false [ ] Deliver66 mkStreamByteOriented 65 false ∧ ¬P.partial_outputShutdownOutputDeliver65; 66 mkStreamByteOriented 65; 66 false [ ] Discard65 mkStreamByteOriented 66 true ∧ ¬P.partial_outputShutdownOutputDeliver65 mkStreamByteOriented 65; 66 false [ ] Deliver65; 66 mkStreamByteOriented [ ] false ∧ ¬P.partial_outputShutdownOutputDiscard65 mkStreamByteOriented 65; 66 false [ ] Discard65; 66 mkStreamByteOriented [ ] true ∧ ¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 mkStreamByteOriented 65 false
Explore proof 17 tactics
Initial goal
⊢
¬P.partial_outputEmptyTls stdout_initial StreamBytes1 65 Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false ∧ ¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial StreamBytes1 65; 66; 67 Accept65; 66; 67 orientation ≔ ByteOriented; outstanding ≔ 65; 66; 67; stream_error ≔ false ∧ ¬P.partial_outputShutdownOutputDeliver66; 65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver66 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false ∧ ¬P.partial_outputShutdownOutputDeliver65; 66 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65 orientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ true ∧ ¬P.partial_outputShutdownOutputDeliver65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false ∧ ¬P.partial_outputShutdownOutputDiscard65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ ¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
repeat split
7 open⊢
¬P.partial_outputEmptyTls stdout_initial StreamBytes1 65 Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
focused goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial StreamBytes1 65; 66; 67 Accept65; 66; 67 orientation ≔ ByteOriented; outstanding ≔ 65; 66; 67; stream_error ≔ false
focused goal
⊢
¬P.partial_outputShutdownOutputDeliver66; 65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver66 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
focused goal
⊢
¬P.partial_outputShutdownOutputDeliver65; 66 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65 orientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ true
focused goal
⊢
¬P.partial_outputShutdownOutputDeliver65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false
focused goal
⊢
¬P.partial_outputShutdownOutputDiscard65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
focused goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
–intros Hactions _
7 openHactions :
⊢
False
deferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial StreamBytes1 65; 66; 67 Accept65; 66; 67 orientation ≔ ByteOriented; outstanding ≔ 65; 66; 67; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver66; 65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver66 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65; 66 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65 orientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDiscard65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
discriminate
6 opendeferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial StreamBytes1 65; 66; 67 Accept65; 66; 67 orientation ≔ ByteOriented; outstanding ≔ 65; 66; 67; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver66; 65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver66 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65; 66 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65 orientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDiscard65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
–intros _ tail Hbad _
6 opendeferred goal
⊢
¬P.partial_outputShutdownOutputDeliver66; 65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver66 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65; 66 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65 orientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDiscard65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
discriminate
5 opendeferred goal
⊢
¬P.partial_outputShutdownOutputDeliver66; 65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver66 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65; 66 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65 orientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDiscard65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
–intros _ Hrun _
5 openHrun :
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false Deliver66 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
⊢
False
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65; 66 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65 orientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDiscard65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
inversion Hrun ; subst
5 openHrun :
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false Deliver66 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
q1 :
H2 :
stream_steporientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false Deliver66 q1
H4 :
stream_runq1 [ ] orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
⊢
False
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65; 66 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65 orientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDiscard65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
match goal withHstep : stream_step_ _ _ |- _⇒inversion Hstep ; substend
5 openHrun :
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false Deliver66 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
rest :
listZ
H4 :
stream_runorientation ≔ ByteOriented; outstanding ≔ rest; stream_error ≔ false [ ] orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
H2 :
stream_steporientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false Deliver66 orientation ≔ ByteOriented; outstanding ≔ rest; stream_error ≔ false
H5 :
66 ≠ [ ]
H :
66 ++ rest = 65; 66
⊢
False
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65; 66 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65 orientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDiscard65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
discriminate
4 opendeferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65; 66 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65 orientation ≔ ByteOriented; outstanding ≔ 66; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDiscard65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
–intros Hfamily _ _
4 openHfamily :
Forallλa : stream_action ⇒ ∃bytes : listZ, a = Deliverbytes Discard65
⊢
False
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDiscard65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
inversion Hfamily as | a rest bytes Hbad Hrest ; subst
4 openHfamily :
Forallλa : stream_action ⇒ ∃bytes : listZ, a = Deliverbytes Discard65
bytes :
listZ
Hrest :
Forallλa : stream_action ⇒ ∃bytes : listZ, a = Deliverbytes [ ]
⊢
False
deferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDiscard65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
discriminate
3 opendeferred goal
⊢
¬P.partial_outputShutdownOutputDeliver65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false
deferred goal
⊢
¬P.partial_outputShutdownOutputDiscard65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
–intros _ tail Hbad _
3 opendeferred goal
⊢
¬P.partial_outputShutdownOutputDiscard65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
discriminate
2 opendeferred goal
⊢
¬P.partial_outputShutdownOutputDiscard65 orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
deferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
–intros _ tail Hbad _
2 opendeferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
discriminate
deferred goal
⊢
¬P.partial_outputShutdownOutputAccept65; 66 stdout_initial [ ] Accept65 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false
–intros _ _ _ Hhidden | Hhidden ; discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
repeat split
–intros Hactions _
discriminate
–intros _ tail Hbad _
discriminate
–intros _ Hrun _
inversion Hrun ; subst
match goal withHstep : stream_step_ _ _ |- _⇒inversion Hstep ; substend
discriminate
–intros Hfamily _ _
inversion Hfamily as | a rest bytes Hbad Hrest ; subst
discriminate
–intros _ tail Hbad _
discriminate
–intros _ tail Hbad _
discriminate
–intros _ _ _ Hhidden | Hhidden ; discriminate
A logical test contract can first allocate and accept a byte, then genuinely refuse an oversized request. It has no normal completion.
mkContractstdio_world RVoid λ_ _ ⇒ True λ_ _ _ ⇒ True λ_ _ _ ⇒ [ ] λ_ _ _ ⇒ [ ] λ_ _ _ ⇒ [ ] λ_ _ _ align size ⇒ align = 16 ∧ size = 16 ∨ size = 2 ^ 48 λ_ _ _ _ _ _ _ ⇒ True λ_ _ _ _ _ _ _ _ ⇒ False resource_reason λ_ ⇒ False
This fixture grants source readiness but no successful action post.
P.mkShutdownBoundaryλ_ _ _ _ ⇒ True λ_ _ ⇒ resource_segment λ_ _ ⇒ CVoid λ_ _ ⇒ [ ] λ_ _ ⇒ [ ] λ_ _ _ _ _ _ _ _ _ _ _ ⇒ False
The refusal leaf keeps nonempty memory and output progress, rather than rolling back to the selected action's original snapshot.
961Example resource_after_progress: ∀host entry, P.stepfixture_rep fixture_requests resource_boundary host P.ShuttingDownInterpRuntime.start HiChecks.memory hello_world mkShutdownInCallbackentry 0 [ ] [ ] stdout_initial StreamBytes1 65 P.ShutdownResourceTooBig InterpRuntime.start + 32 allocatedHiChecks.memory heap_req16 16 InterpRuntime.start hello_world mkShutdownInCallbackentry 0 [ ] [ ] stdout_initial ShutdownOutputAccept65; 66 Accept65 mkStreamByteOriented 65 false
Proof 28 steps Qed
intros host entry
eapply P.program_shutdown_resource with full := mkShutdownInCallbackentry 0 [ ] [ ] mkStreamByteOriented 65; 66 false
–apply shutdown_callback_output
apply stream_accept ; discriminate | repeat constructor ; lia
–exact I
–split ; exact I
–eapply P.M.E.invoke_resource with born := InterpRuntime.start
+exact I
+exact I
+split ; | exact I
eapply P.M.E.effects_alloc with align := 16 size := 16 base := InterpRuntime.start s1 := InterpRuntime.start + 32
∗split ; reflexivity | left ; reflexivity
∗unfold max_allocation_size
lia
∗reflexivity
∗constructor
+eapply P.M.E.failure_big with align := 16 size := 2 ^ 48
∗split ; reflexivity | right ; reflexivity
∗unfold max_allocation_size
lia
+right
reflexivity
–split
+split ; constructor ; exists 65 ; reflexivity | constructor | exists 66 ; reflexivity
+split
∗eapply stream_next ; apply stream_accept ; discriminate | repeat constructor ; lia | constructor
∗right
reflexivity
Without a permitted request there is no resource endpoint, even when the logical action and its empty prefix are available.
1001Example unrequested_refusal_rejected: ∀rep requests host s m w sh trace why s′ m′ w′ action actions q, ¬P.steprep requests boundary host P.ShuttingDowns m w sh trace P.ShutdownResourcewhy s′ m′ w′ sh action actions q
Explore proof 5 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop host : P.host_boundary s : InterpRuntime.state m : mem w : stdio_world sh : shutdown_state trace : listevent why : reason s′ : InterpRuntime.state m′ : mem w′ : stdio_world action : shutdown_action actions : liststream_action q : stream_state, ¬P.steprep requests boundary host P.ShuttingDowns m w sh trace P.ShutdownResourcewhy s′ m′ w′ sh action actions q
intros rep requests host s m w sh trace why s′ m′ w′ action actions q Hstep
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
m :
w :
sh :
trace :
listevent
why :
m′ :
w′ :
action :
actions :
liststream_action
q :
Hstep :
P.steprep requests boundary host P.ShuttingDowns m w sh trace P.ShutdownResourcewhy s′ m′ w′ sh action actions q
⊢
False
inversion Hstep ; subst
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
m :
w :
sh :
trace :
listevent
why :
m′ :
w′ :
action :
actions :
liststream_action
q :
Hstep :
P.steprep requests boundary host P.ShuttingDowns m w sh trace P.ShutdownResourcewhy s′ m′ w′ sh action actions q
full :
H6 :
shutdown_stepsh action full
H12 :
P.shutdown_readyboundary s m w sh
H13 :
P.shutdown_admissibleboundary s m w sh action
H14 :
P.M.E.invokeP.action_contractboundary sh action P.action_resultboundary sh action P.action_argumentsboundary sh action P.action_wordsboundary sh action s m w trace CallResourcewhy s′ m′ w′
H15 :
P.partial_outputaction shutdown_stdoutsh trace actions q
⊢
False
match goal withHcall : P.M.E.invoke_ _ _ _ _ _ _ _ _ _ _ _ |- _⇒inversion Hcall ; substend
2 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
m :
w :
sh :
trace :
listevent
why :
m′ :
w′ :
action :
actions :
liststream_action
q :
Hstep :
P.steprep requests boundary host P.ShuttingDowns m w sh trace P.ShutdownResourcewhy s′ m′ w′ sh action actions q
full :
H6 :
shutdown_stepsh action full
H12 :
P.shutdown_readyboundary s m w sh
H13 :
P.shutdown_admissibleboundary s m w sh action
H14 :
P.M.E.invokeP.action_contractboundary sh action P.action_resultboundary sh action P.action_argumentsboundary sh action P.action_wordsboundary sh action s m w trace CallResourcewhy s′ m′ w′
H15 :
P.partial_outputaction shutdown_stdoutsh trace actions q
born :
listZ
H :
contract_abiP.action_contractboundary sh action P.action_resultboundary sh action P.action_argumentsboundary sh action
H0 :
contract_preP.action_contractboundary sh action P.action_wordsboundary sh action m w
H1 :
P.M.E.prefixP.action_contractboundary sh action P.action_wordsboundary sh action s m w born trace s′ m′ w′
H2 :
contract_postP.action_contractboundary sh action P.action_wordsboundary sh action m w born trace CallResourcewhy m′ w′
H3 :
∀why0 : reason, CallResourcewhy ≠ CallResourcewhy0
H4 :
∀values : listword, CallResourcewhy = CallReturnvalues → return_shapecontract_returnsP.action_contractboundary sh action values ∧ Forallword_authoritycontract_sourcesP.action_contractboundary sh action P.action_wordsboundary sh action m w born m′ values
H5 :
∀status : Z, CallResourcewhy = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
False
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
m :
w :
sh :
trace :
listevent
why :
m′ :
w′ :
action :
actions :
liststream_action
q :
Hstep :
P.steprep requests boundary host P.ShuttingDowns m w sh trace P.ShutdownResourcewhy s′ m′ w′ sh action actions q
full :
H6 :
shutdown_stepsh action full
H12 :
P.shutdown_readyboundary s m w sh
H13 :
P.shutdown_admissibleboundary s m w sh action
H14 :
P.M.E.invokeP.action_contractboundary sh action P.action_resultboundary sh action P.action_argumentsboundary sh action P.action_wordsboundary sh action s m w trace CallResourcewhy s′ m′ w′
H15 :
P.partial_outputaction shutdown_stdoutsh trace actions q
born :
listZ
H0 :
contract_abiP.action_contractboundary sh action P.action_resultboundary sh action P.action_argumentsboundary sh action
H1 :
contract_preP.action_contractboundary sh action P.action_wordsboundary sh action m w
H2 :
P.M.E.prefixP.action_contractboundary sh action P.action_wordsboundary sh action s m w born trace s′ m′ w′
H3 :
P.M.E.resource_failurecontract_requestsP.action_contractboundary sh action P.action_wordsboundary sh action m w s′ why
H5 :
contract_resourceP.action_contractboundary sh action why
⊢
False
–match goal withHnormal : ∀why, CallResource_ ≠ CallResourcewhy |- _⇒apply Hnormalwhy ; reflexivityend
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
host :
m :
w :
sh :
trace :
listevent
why :
m′ :
w′ :
action :
actions :
liststream_action
q :
Hstep :
P.steprep requests boundary host P.ShuttingDowns m w sh trace P.ShutdownResourcewhy s′ m′ w′ sh action actions q
full :
H6 :
shutdown_stepsh action full
H12 :
P.shutdown_readyboundary s m w sh
H13 :
P.shutdown_admissibleboundary s m w sh action
H14 :
P.M.E.invokeP.action_contractboundary sh action P.action_resultboundary sh action P.action_argumentsboundary sh action P.action_wordsboundary sh action s m w trace CallResourcewhy s′ m′ w′
H15 :
P.partial_outputaction shutdown_stdoutsh trace actions q
born :
listZ
H0 :
contract_abiP.action_contractboundary sh action P.action_resultboundary sh action P.action_argumentsboundary sh action
H1 :
contract_preP.action_contractboundary sh action P.action_wordsboundary sh action m w
H2 :
P.M.E.prefixP.action_contractboundary sh action P.action_wordsboundary sh action s m w born trace s′ m′ w′
H3 :
P.M.E.resource_failurecontract_requestsP.action_contractboundary sh action P.action_wordsboundary sh action m w s′ why
H5 :
contract_resourceP.action_contractboundary sh action why
⊢
False
–match goal withHrefuse : P.M.E.resource_failure_ _ _ |- _⇒inversion Hrefuse ; substend;contradiction
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests host s m w sh trace why s′ m′ w′ action actions q Hstep
inversion Hstep ; subst
match goal withHcall : P.M.E.invoke_ _ _ _ _ _ _ _ _ _ _ _ |- _⇒inversion Hcall ; substend
–match goal withHnormal : ∀why, CallResource_ ≠ CallResourcewhy |- _⇒apply Hnormalwhy ; reflexivityend
–match goal withHrefuse : P.M.E.resource_failure_ _ _ |- _⇒inversion Hrefuse ; substend;contradiction