Filnix wiki

⇒

False

trace

No diagnostic prefix contains a host-termination observation.

34Lemma diagnostic_trace_exit_free

∀ trace status

¬InProcessExitstatus trace

Explore proof 4 tactics

Initial goal

⊢

∀trace : listevent, diagnostic_tracetrace → ∀status : Z, ¬InProcessExitstatus trace

intros trace H status Hin

trace :

listevent

H :

status :

Hin :

InProcessExitstatus trace

⊢

False

unfold diagnostic_trace in H

trace :

listevent

H :

Forall

λ observation : event ⇒

match observation with

StreamBytesstream _

⇒

stream = 2

⇒

False

trace

status :

Hin :

InProcessExitstatus trace

⊢

False

rewrite Forall_forall in H

trace :

listevent

H :

∀ x : event ,

Inx trace

→

match x with

StreamBytesstream _

⇒

stream = 2

⇒

False

status :

Hin :

InProcessExitstatus trace

⊢

False

exact H_ Hin

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros trace H status Hin

unfold diagnostic_trace in H

rewrite Forall_forall in H

exact H_ Hin

In particular stderr output never becomes stdout acceptance.

42Lemma diagnostic_trace_not_stdout

∀ trace bytes

¬InStreamBytes1 bytes trace

Explore proof 5 tactics

Initial goal

⊢

∀trace : listevent bytes : listZ, diagnostic_tracetrace → ¬InStreamBytes1 bytes trace

intros trace bytes H Hin

trace :

listevent

bytes :

listZ

H :

Hin :

InStreamBytes1 bytes trace

⊢

False

unfold diagnostic_trace in H

trace :

listevent

bytes :

listZ

H :

Forall

λ observation : event ⇒

match observation with

StreamBytesstream _

⇒

stream = 2

⇒

False

trace

Hin :

InStreamBytes1 bytes trace

⊢

False

rewrite Forall_forall in H

trace :

listevent

bytes :

listZ

H :

∀ x : event ,

Inx trace

→

match x with

StreamBytesstream _

⇒

stream = 2

⇒

False

Hin :

InStreamBytes1 bytes trace

⊢

False

specialize H_ Hin

trace :

listevent

bytes :

listZ

H :

match StreamBytes1 bytes with

StreamBytesstream _

⇒

stream = 2

⇒

False

Hin :

InStreamBytes1 bytes trace

⊢

False

discriminate H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros trace bytes H Hin

unfold diagnostic_trace in H

rewrite Forall_forall in H

specialize H_ Hin

discriminate H

This contract summarizes only the diagnostic stage, before the status branch. Its virtual void result is NOT a normal return from error when status is nonzero; do not register it as error's ordinary contract. Resource prefixes retain no normal-completion facts. All capability sources, writes, releases, allocations and panic policy come from fmt.

54Definition diagnostic_contractworld : Type fmt : contractworld : contractworld ≔

mkContractworld RVoid error_abicontract_abifmt λxs m w ⇒ contract_prefmt xs m w ∧ ∃status, error_wordsxs status contract_sourcesfmt contract_writesfmt contract_releasesfmt contract_requestsfmt λxs m w born trace m′ w′ ⇒ contract_prefixfmt xs m w born trace m′ w′ ∧ diagnostic_tracetrace λxs m w born trace ending m′ w′ ⇒ contract_postfmt xs m w born trace ending m′ w′ ∧ ending = CallReturn[ ] contract_resourcefmt contract_panicsfmt

Only status-zero error may use ordinary ExternalMachine dispatch. The caller's frame/locals/continuation are preserved by resume_external; libc state, errno and stream settlement may change under fmt's effects.

67Definition error_contractworld : Type fmt : contractworld : contractworld ≔

let spec ≔ diagnostic_contractfmt in

mkContractworld RVoid contract_abispec λxs m w ⇒ contract_prespec xs m w ∧ error_wordsxs 0 contract_sourcesspec contract_writesspec contract_releasesspec contract_requestsspec contract_prefixspec contract_postspec contract_resourcespec contract_panicsspec

The normal-return shape is available without choosing a runtime instance.

75Lemma error_post_void

∀ world fmt : contractworld xs m w born trace ending m′ w′

contract_posterror_contractfmt xs m w born trace ending m′ w′

ending = CallReturn[ ]

Explore proof 2 tactics

Initial goal

⊢

∀world : Type fmt : contractworld xs : listword m : mem w : world born : listZ trace : listevent ending : call_end m′ : mem w′ : world, contract_posterror_contractfmt xs m w born trace ending m′ w′ → ending = CallReturn[ ]

intros world fmt xs m w born trace ending m′ w′ _ H

world :

Type

fmt :

contractworld

xs :

listword

m :

w :

world

born :

listZ

trace :

listevent

ending :

call_end

m′ :

w′ :

world

H :

ending = CallReturn[ ]

⊢

ending = CallReturn[ ]

exact H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros world fmt xs m w born trace ending m′ w′ _ H

exact H

Canonical argument lists determine status independently of behavior.

80Lemma error_words_status

∀ xs left right

error_wordsxs left

error_wordsxs right

left = right

Explore proof 4 tactics

Initial goal

⊢

∀xs : listword left right : Z, error_wordsxs left → error_wordsxs right → left = right

intros xs left right e & p & rest & Hl & _ e′ & p′ & rest′ & Hr & _

xs :

listword

left, right, e :

p :

rest :

listword

Hl :

xs = WIntleft :: WInte :: WPtrp :: rest

e′ :

p′ :

rest′ :

listword

Hr :

xs = WIntright :: WInte′ :: WPtrp′ :: rest′

⊢

left = right

rewrite Hl in Hr

xs :

listword

left, right, e :

p :

rest :

listword

Hl :

xs = WIntleft :: WInte :: WPtrp :: rest

e′ :

p′ :

rest′ :

listword

Hr :

WIntleft :: WInte :: WPtrp :: rest = WIntright :: WInte′ :: WPtrp′ :: rest′

⊢

left = right

injection Hr

xs :

listword

left, right, e :

p :

rest :

listword

Hl :

xs = WIntleft :: WInte :: WPtrp :: rest

e′ :

p′ :

rest′ :

listword

Hr :

WIntleft :: WInte :: WPtrp :: rest = WIntright :: WInte′ :: WPtrp′ :: rest′

⊢

rest = rest′ → p = p′ → e = e′ → left = right → left = right

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros xs left right e & p & rest & Hl & _ e′ & p′ & rest′ & Hr & _

rewrite Hl in Hr

injection Hr

auto

A nonzero diagnostic is never admitted as an ordinary returning error.

88Lemma nonzero_error_not_returning

∀ world fmt : contractworld xs m w status

error_wordsxs status

status ≠ 0

¬contract_preerror_contractfmt xs m w

Explore proof 3 tactics

Initial goal

⊢

∀world : Type fmt : contractworld xs : listword m : mem w : world status : Z, error_wordsxs status → status ≠ 0 → ¬contract_preerror_contractfmt xs m w

intros world fmt xs m w status Hstatus Hnonzero _ Hzero

world :

Type

fmt :

contractworld

xs :

listword

m :

w :

world

status :

Hstatus :

error_wordsxs status

Hnonzero :

status ≠ 0

Hzero :

error_wordsxs 0

⊢

False

apply Hnonzero

world :

Type

fmt :

contractworld

xs :

listword

m :

w :

world

status :

Hstatus :

error_wordsxs status

Hnonzero :

status ≠ 0

Hzero :

error_wordsxs 0

⊢

status = 0

eapply error_words_status ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros world fmt xs m w status Hstatus Hnonzero _ Hzero

apply Hnonzero

eapply error_words_status ; eauto

Diagnostics reuse the exact runtime, effects and current Linked world.

96Module Diagnostics R : Runtime L : LinkedSigR

97Module N ≔ Ending R L

98Module M ≔ N.M

99Module E ≔ N.E

100Module RM ≔ N.RM

102Section World

103Variable payload : Type

104Variable fmt : contractN.worldpayload

The selected error call is independently admitted even if no diagnostic invocation completes. This premise does not promise termination.

108Definition error_sitege c site xs : Prop ≔

external_sitege c site ∧ site_namesite = TAtom"error" ∧ map_optionarg_xge fr_envc_framec site_argssite = Somexs ∧ contract_abidiagnostic_contractfmt site_resultsite site_argssite

Caller admission is independent of a completed formatting stage.

114Definition error_admittedge c w site : Prop ≔

∃xs, error_sitege c site xs ∧ contract_prediagnostic_contractfmt xs c_memc w

A nonzero completed diagnostic requests exit with its CURRENT world, including any stdout flush/error and stderr settlement. It never reuses registration-time state, resumes the caller or emits ProcessExit.

120Inductive error_requestge : config → R.state → N.worldpayload → listevent → RM.mstate → N.worldpayload → Prop ≔

∀ c s w site xs status trace s′ m′ w′ sh′

error_sitege c site xs

error_wordsxs status

status ≠ 0

E.invokediagnostic_contractfmt site_resultsite site_argssite xs s c_memc w trace CallReturn[ ] s′ m′ w′

shutdown_uniquesndw′

exit_requestSoftExit main_statusstatus sndw′ sh′

error_requests_exit

error_requestge c s w trace RM.with_memc m′, s′ fstw′, sh′

Extension rules are disjoint from Ending's ordinary error dispatch. Status-zero returns and resources remain ordinary external outcomes; nonzero diagnostics have an exit-request edge or a resource leaf.

132Inductive stepregistry ge b : N.boundarypayload admitted : N.statepayload → listevent → N.statepayload → Prop ≔

∀ st trace st′

N.steppayload registry ge λsymbol ⇒ name_eqbsymbol TAtom"error" b admitted st trace st′

diagnostic_ending

stepregistry ge b admitted st trace st′

∀ c s w site xs trace result s′ m′ w′ e

error_sitege c site xs

E.invokeerror_contractfmt site_resultsite site_argssite xs s c_memc w trace CallReturnresult s′ m′ w′

external_enverror_contractfmt site result fr_envc_framec = Somee

diagnostic_zero

stepregistry ge b admitted N.Executingpayload M.Runningc, s w trace N.Executingpayload M.Runningresume_externalc site e m′, s′ w′

∀ c s w trace ms′ w′

error_requestge c s w trace ms′ w′

diagnostic_request

stepregistry ge b admitted N.Executingpayload M.Runningc, s w trace N.Drainingpayload ms′ w′

∀ c s w site xs trace why s′ m′ w′

error_sitege c site xs

E.invokediagnostic_contractfmt site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′

diagnostic_resource

stepregistry ge b admitted N.Executingpayload M.Runningc, s w trace N.Executingpayload M.StoppedCoreEndTrapwhy RM.with_memc m′, s′ w′

∀ c s w site xs born trace s′ m′ w′

error_sitege c site xs

contract_prediagnostic_contractfmt xs c_memc w

E.prefixdiagnostic_contractfmt xs s c_memc w born trace s′ m′ w′

diagnostic_prefix

stepregistry ge b admitted N.Executingpayload M.Runningc, s w trace N.Partialpayload RM.with_memc m′, s′ w′

∀ c s w site

external_sitege c site

site_namesite = TAtom"error"

¬error_admittedge c w site

diagnostic_rejected

stepregistry ge b admitted N.Executingpayload M.Runningc, s w [ ] N.Executingpayload M.StoppedContractViolationTAtom"error" BadPrecondition c, s w

A diagnostic request carries only diagnostic events, not host exit.

166Theorem error_request_exit_free

∀ ge c s w trace ms′ w′

error_requestge c s w trace ms′ w′

Explore proof 4 tactics

Initial goal

payload :

Type

fmt :

contractN.worldpayload

⊢

∀ge : genv c : config s : R.state w : N.worldpayload trace : listevent ms′ : RM.mstate w′ : N.worldpayload, error_requestge c s w trace ms′ w′ → diagnostic_tracetrace

intros ge c s w trace ms′ w′ H

payload :

Type

fmt :

contractN.worldpayload

ge :

c :

s :

R.state

w :

N.worldpayload

trace :

listevent

ms′ :

w′ :

N.worldpayload

H :

error_requestge c s w trace ms′ w′

⊢

destruct H

payload :

Type

fmt :

contractN.worldpayload

ge :

c :

s :

R.state

w :

N.worldpayload

site :

xs :

listword

status :

trace :

listevent

s′ :

R.state

m′ :

w′ :

N.worldpayload

sh′ :

H :

error_sitege c site xs

H₀ :

error_wordsxs status

H₁ :

status ≠ 0

H₂ :

E.invokediagnostic_contractfmt site_resultsite site_argssite xs s c_memc w trace CallReturn[ ] s′ m′ w′

H₃ :

shutdown_uniquesndw′

H₄ :

exit_requestSoftExit main_statusstatus sndw′ sh′

⊢

destruct E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ H₂ as born _ _ Htrace

payload :

Type

fmt :

contractN.worldpayload

ge :

c :

s :

R.state

w :

N.worldpayload

site :

xs :

listword

status :

trace :

listevent

s′ :

R.state

m′ :

w′ :

N.worldpayload

sh′ :

H :

error_sitege c site xs

H₀ :

error_wordsxs status

H₁ :

status ≠ 0

H₂ :

E.invokediagnostic_contractfmt site_resultsite site_argssite xs s c_memc w trace CallReturn[ ] s′ m′ w′

H₃ :

shutdown_uniquesndw′

H₄ :

exit_requestSoftExit main_statusstatus sndw′ sh′

born :

listZ

Htrace :

⊢

exact Htrace

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros ge c s w trace ms′ w′ H

destruct H

destruct E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ H₂ as born _ _ Htrace

exact Htrace

Every request keeps readiness and identities through the formatter's actual effect path; no final-return state is assumed for resources.

176Theorem error_request_preserve

∀ ge c s w trace ms′ w′

error_requestge c s w trace ms′ w′

R.readys c_memc

RM.ready_statems′ ∧ persistsc_memc c_memfstms′

Explore proof 4 tactics

Initial goal

payload :

Type

fmt :

contractN.worldpayload

⊢

∀ge : genv c : config s : R.state w : N.worldpayload trace : listevent ms′ : RM.mstate w′ : N.worldpayload, error_requestge c s w trace ms′ w′ → R.readys c_memc → RM.ready_statems′ ∧ persistsc_memc c_memfstms′

intros ge c s w trace ms′ w′ H Hr

payload :

Type

fmt :

contractN.worldpayload

ge :

c :

s :

R.state

w :

N.worldpayload

trace :

listevent

ms′ :

w′ :

N.worldpayload

H :

error_requestge c s w trace ms′ w′

Hr :

R.readys c_memc

⊢

RM.ready_statems′ ∧ persistsc_memc c_memfstms′

destruct H

payload :

Type

fmt :

contractN.worldpayload

ge :

c :

s :

R.state

w :

N.worldpayload

site :

xs :

listword

status :

trace :

listevent

s′ :

R.state

m′ :

w′ :

N.worldpayload

sh′ :

H :

error_sitege c site xs

H₀ :

error_wordsxs status

H₁ :

status ≠ 0

H₂ :

E.invokediagnostic_contractfmt site_resultsite site_argssite xs s c_memc w trace CallReturn[ ] s′ m′ w′

H₃ :

shutdown_uniquesndw′

H₄ :

exit_requestSoftExit main_statusstatus sndw′ sh′

Hr :

R.readys c_memc

⊢

RM.ready_stateRM.with_memc m′, s′ ∧ persistsc_memc c_memfstRM.with_memc m′, s′

simpl

payload :

Type

fmt :

contractN.worldpayload

ge :

c :

s :

R.state

w :

N.worldpayload

site :

xs :

listword

status :

trace :

listevent

s′ :

R.state

m′ :

w′ :

N.worldpayload

sh′ :

H :

error_sitege c site xs

H₀ :

error_wordsxs status

H₁ :

status ≠ 0

H₂ :

E.invokediagnostic_contractfmt site_resultsite site_argssite xs s c_memc w trace CallReturn[ ] s′ m′ w′

H₃ :

shutdown_uniquesndw′

H₄ :

exit_requestSoftExit main_statusstatus sndw′ sh′

Hr :

R.readys c_memc

⊢

RM.ready_stateRM.with_memc m′, s′ ∧ persistsc_memc m′

eapply E.invoke_preserve ; eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros ge c s w trace ms′ w′ H Hr

destruct H

simpl

eapply E.invoke_preserve ; eauto

Both diagnostic branches and their resource/unfinished leaves retain readiness and identities, using the imported formatter's exact effects.

186Theorem step_preserve

∀ registry ge b admitted st trace st′

ge_freege = R.free

stepregistry ge b admitted st trace st′

N.state_readypayload st

N.state_readypayload st′ ∧ persistsc_memfstN.machine_ofpayload st c_memfstN.machine_ofpayload st′

Explore proof 8 tactics

Initial goal

payload :

Type

fmt :

contractN.worldpayload

⊢

∀registry : name → optioncontractN.worldpayload ge : genv b : N.boundarypayload admitted : registration → R.state → mem → N.worldpayload → Prop st : N.statepayload trace : listevent st′ : N.statepayload, ge_freege = R.free → stepregistry ge b admitted st trace st′ → N.state_readypayload st → N.state_readypayload st′ ∧ persistsc_memfstN.machine_ofpayload st c_memfstN.machine_ofpayload st′

intros registry ge b admitted st trace st′ Hfree H

payload :

Type

fmt :

contractN.worldpayload

registry :

name → optioncontractN.worldpayload

ge :

b :

N.boundarypayload

admitted :

registration → R.state → mem → N.worldpayload → Prop

st :

N.statepayload

trace :

listevent

st′ :

N.statepayload

Hfree :

ge_freege = R.free

H :

stepregistry ge b admitted st trace st′

⊢

N.state_readypayload st → N.state_readypayload st′ ∧ persistsc_memfstN.machine_ofpayload st c_memfstN.machine_ofpayload st′

destruct H ; intros Hr

6 open

payload :

Type

fmt :

contractN.worldpayload

registry :

name → optioncontractN.worldpayload

ge :

b :

N.boundarypayload

admitted :

registration → R.state → mem → N.worldpayload → Prop

Hfree :

ge_freege = R.free

st :

N.statepayload

trace :

listevent

st′ :

N.statepayload

H :

N.steppayload registry ge λsymbol : name ⇒ name_eqbsymbol TAtom"error" b admitted st trace st′

Hr :

N.state_readypayload st

⊢

N.state_readypayload st′ ∧ persistsc_memfstN.machine_ofpayload st c_memfstN.machine_ofpayload st′

focused goal

payload :

Type

fmt :

contractN.worldpayload

registry :

name → optioncontractN.worldpayload

ge :

b :

N.boundarypayload

admitted :

registration → R.state → mem → N.worldpayload → Prop

Hfree :

ge_freege = R.free

c :

s :

R.state

w :

N.worldpayload

site :

xs :

listword

trace :

listevent

result :

listword

s′ :

R.state

m′ :

w′ :

N.worldpayload

e :

env

H :

error_sitege c site xs

H₀ :

E.invokeerror_contractfmt site_resultsite site_argssite xs s c_memc w trace CallReturnresult s′ m′ w′

H₁ :

external_enverror_contractfmt site result fr_envc_framec = Somee

Hr :

N.state_readypayload N.Executingpayload M.Runningc, s w

⊢

N.state_readypayload N.Executingpayload M.Runningresume_externalc site e m′, s′ w′ ∧ persistsc_memfstN.machine_ofpayload N.Executingpayload M.Runningc, s w c_memfstN.machine_ofpayload N.Executingpayload M.Runningresume_externalc site e m′, s′ w′

focused goal

payload :

Type

fmt :

contractN.worldpayload

registry :

name → optioncontractN.worldpayload

ge :

b :

N.boundarypayload

admitted :

registration → R.state → mem → N.worldpayload → Prop

Hfree :

ge_freege = R.free

c :

s :

R.state

w :

N.worldpayload

trace :

listevent

ms′ :

w′ :

N.worldpayload

H :

error_requestge c s w trace ms′ w′

Hr :

N.state_readypayload N.Executingpayload M.Runningc, s w

⊢

N.state_readypayload N.Drainingpayload ms′ w′ ∧ persistsc_memfstN.machine_ofpayload N.Executingpayload M.Runningc, s w c_memfstN.machine_ofpayload N.Drainingpayload ms′ w′

focused goal

payload :

Type

fmt :

contractN.worldpayload

registry :

name → optioncontractN.worldpayload

ge :

b :

N.boundarypayload

admitted :

registration → R.state → mem → N.worldpayload → Prop

Hfree :

ge_freege = R.free

c :

s :

R.state

w :

N.worldpayload

site :

xs :

listword

trace :

listevent

why :

reason

s′ :

R.state

m′ :

w′ :

N.worldpayload

H :

error_sitege c site xs

H₀ :

E.invokediagnostic_contractfmt site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′

Hr :

N.state_readypayload N.Executingpayload M.Runningc, s w

⊢

N.state_readypayload N.Executingpayload M.StoppedCoreEndTrapwhy RM.with_memc m′, s′ w′ ∧ persistsc_memfstN.machine_ofpayload N.Executingpayload M.Runningc, s w c_memfstN.machine_ofpayload N.Executingpayload M.StoppedCoreEndTrapwhy RM.with_memc m′, s′ w′

focused goal

payload :

Type

fmt :

contractN.worldpayload

registry :

name → optioncontractN.worldpayload

ge :

b :

N.boundarypayload

admitted :

registration → R.state → mem → N.worldpayload → Prop

Hfree :

ge_freege = R.free

c :

s :

R.state

w :

N.worldpayload

site :

xs :

listword

born :

listZ

trace :

listevent

s′ :

R.state

m′ :

w′ :

N.worldpayload

H :

error_sitege c site xs

H₀ :

contract_prediagnostic_contractfmt xs c_memc w

H₁ :

E.prefixdiagnostic_contractfmt xs s c_memc w born trace s′ m′ w′

Hr :

N.state_readypayload N.Executingpayload M.Runningc, s w

⊢

N.state_readypayload N.Partialpayload RM.with_memc m′, s′ w′ ∧ persistsc_memfstN.machine_ofpayload N.Executingpayload M.Runningc, s w c_memfstN.machine_ofpayload N.Partialpayload RM.with_memc m′, s′ w′

focused goal

payload :

Type

fmt :

contractN.worldpayload

registry :

name → optioncontractN.worldpayload

ge :

b :

N.boundarypayload

admitted :

registration → R.state → mem → N.worldpayload → Prop

Hfree :

ge_freege = R.free

c :

s :

R.state

w :

N.worldpayload

site :

H :

external_sitege c site

H₀ :

site_namesite = TAtom"error"

H₁ :

¬error_admittedge c w site

Hr :

N.state_readypayload N.Executingpayload M.Runningc, s w

⊢

N.state_readypayload N.Executingpayload M.StoppedContractViolationTAtom"error" BadPrecondition c, s w ∧ persistsc_memfstN.machine_ofpayload N.Executingpayload M.Runningc, s w c_memfstN.machine_ofpayload N.Executingpayload M.StoppedContractViolationTAtom"error" BadPrecondition c, s w

–eapply N.step_preserve ; eauto

5 open

deferred goal

payload :

Type

fmt :

contractN.worldpayload

registry :

name → optioncontractN.worldpayload

ge :

b :

N.boundarypayload

admitted :

registration → R.state → mem → N.worldpayload → Prop

Hfree :

ge_freege = R.free

c :

s :

R.state

w :

N.worldpayload

site :

xs :

listword

trace :

listevent

result :

listword

s′ :

R.state

m′ :

w′ :

N.worldpayload

e :

env

H :

error_sitege c site xs

H₀ :

E.invokeerror_contractfmt site_resultsite site_argssite xs s c_memc w trace CallReturnresult s′ m′ w′

H₁ :

external_enverror_contractfmt site result fr_envc_framec = Somee

Hr :

N.state_readypayload N.Executingpayload M.Runningc, s w

⊢

deferred goal

payload :

Type

fmt :

contractN.worldpayload

registry :

name → optioncontractN.worldpayload

ge :

b :

N.boundarypayload

admitted :

registration → R.state → mem → N.worldpayload → Prop

Hfree :

ge_freege = R.free

c :

s :

R.state

w :

N.worldpayload

trace :

listevent

ms′ :

w′ :

N.worldpayload

H :

error_requestge c s w trace ms′ w′

Hr :

N.state_readypayload N.Executingpayload M.Runningc, s w

⊢

N.state_readypayload N.Drainingpayload ms′ w′ ∧ persistsc_memfstN.machine_ofpayload N.Executingpayload M.Runningc, s w c_memfstN.machine_ofpayload N.Drainingpayload ms′ w′

deferred goal

payload :

Type

fmt :

contractN.worldpayload

registry :

name → optioncontractN.worldpayload

ge :

b :

N.boundarypayload

admitted :

registration → R.state → mem → N.worldpayload → Prop

Hfree :

ge_freege = R.free

c :

s :

R.state

w :

N.worldpayload

site :

xs :

listword

trace :

listevent

why :

reason

s′ :

R.state

m′ :

w′ :

N.worldpayload

H :

error_sitege c site xs

H₀ :

E.invokediagnostic_contractfmt site_resultsite site_argssite xs s c_memc w trace CallResourcewhy s′ m′ w′

Hr :

N.state_readypayload N.Executingpayload M.Runningc, s w

⊢

deferred goal

payload :

Type

fmt :

contractN.worldpayload

registry :

name → optioncontractN.worldpayload

ge :

b :

N.boundarypayload

admitted :

registration → R.state → mem → N.worldpayload → Prop

Hfree :

ge_freege = R.free

c :

s :

R.state

w :

N.worldpayload

site :

xs :

listword

born :

listZ

trace :

listevent

s′ :

R.state

m′ :

w′ :

N.worldpayload

H :

error_sitege c site xs

H₀ :

contract_prediagnostic_contractfmt xs c_memc w

H₁ :

E.prefixdiagnostic_contractfmt xs s c_memc w born trace s′ m′ w′

Hr :

N.state_readypayload N.Executingpayload M.Runningc, s w

⊢

deferred goal

payload :

Type

fmt :

contractN.worldpayload

registry :

name → optioncontractN.worldpayload

ge :

b :

N.boundarypayload

admitted :

registration → R.state → mem → N.worldpayload → Prop

Hfree :

ge_freege = R.free

c :

s :

R.state

w :

N.worldpayload

site :

H :

external_sitege c site

H₀ :

site_namesite = TAtom"error"

H₁ :

¬error_admittedge c w site

Hr :

N.state_readypayload N.Executingpayload M.Runningc, s w

⊢

–eapply E.invoke_preserve ; eauto

4 open

deferred goal

payload :

Type

fmt :

contractN.worldpayload

registry :

name → optioncontractN.worldpayload

ge :

b :

N.boundarypayload

admitted :

registration → R.state → mem → N.worldpayload → Prop

Hfree :

ge_freege = R.free

c :

s :

R.state

w :

N.worldpayload

trace :

listevent

ms′ :

w′ :

N.worldpayload

H :

error_requestge c s w trace ms′ w′

Hr :

N.state_readypayload N.Executingpayload M.Runningc, s w

⊢

N.state_readypayload N.Drainingpayload ms′ w′ ∧ persistsc_memfstN.machine_ofpayload N.Executingpayload M.Runningc, s w c_memfstN.machine_ofpayload N.Drainingpayload ms′ w′

deferred goal

payload :

Type

fmt :

contractN.worldpayload

registry :

name → optioncontractN.worldpayload

ge :