rocq/theories/LibcExit.v
Hard exit as a trusted nonreturning external-call summary over the consumer's exact machine. This does not replace Ending's request interceptor or execute its soft-exit loop. Host completion remains independent of the request; no callback or stdout obligation is silently settled by _exit.
From Stdlib Require Import String ZArith List Bool Lia
From Nanofil Require Import Term Maps Syntax Values Memory Runtime Ops Semantics ExternalCalls ExternalMachine Startup Stdio Shutdown Ending Libc
Import ListNotations
Open Scope Z_scope
Open Scope list_scope
Canonical C int bits, before signed shutdown status and low-byte host status are distinguished.
A hard request changes only the shutdown phase/status. Payload, registrations, consumed history and stdout all retain their identity.
hard_exit_wordsxs bits ∧ fstw′ = fstw ∧ exit_requestHardExit main_statusbits sndw sndw′
Readiness alone does not exclude an already completed handoff.
libc_readyrep m w ∧ ∃bits, hard_exit_wordsxs bits ∧ ∀kind, shutdown_atsndw ≠ HandedOffkind
Finite prefixes may be before the request, after the request but blocked in the host, or host-completed. Only the last emits exit. Observable termination leaves no mutable caller-memory continuation.
32Definition hard_exit_prefixhost : mem → libc_world → Prop xs m w born : listZ trace m′ w′ : Prop ≔
born = [ ] ∧ m′ = m ∧ trace = [ ] ∧ w′ = w ∨ ∃bits, hard_exit_endpointxs w w′ bits ∧ trace = [ ] ∨ trace = ProcessExitprocess_statusmain_statusbits ∧ hostm′ w′
A completed host exit is not a synthetic ordinary void return.
40Definition hard_exit_posthost : mem → libc_world → Prop xs m : mem w born : listZ trace ending m′ w′ : Prop ≔
∃bits, hard_exit_endpointxs w w′ bits ∧ trace = ProcessExitprocess_statusmain_statusbits ∧ ending = CallExitprocess_statusmain_statusbits ∧ hostm′ w′
The host witness is trusted behind this contract, not assumed to exist for each admitted call. No allocation or resource leaf is added.
mkContractlibc_world RVoid exit_abi hard_exit_prerep λ_ _ _ ⇒ [ ] λ_ _ _ ⇒ [ ] λ_ _ _ ⇒ [ ] λ_ _ _ _ _ ⇒ False hard_exit_prefixhost hard_exit_posthost λ_ ⇒ False puts_panic
Only the two hard-exit aliases are summarized here. Soft exit stays with the explicit lifecycle, callback execution and cleanup boundary.
55Definition libc_hard_exit_registryrep host fallback : name → optioncontractlibc_world symbol : optioncontractlibc_world ≔
else
fallbacksymbol
Admission needs no host-completion promise.
∀ rep host xs bits m w
contract_prelibc_hard_exit_contractrep host xs m w
Explore proof 4 tactics
Initial goal
⊢
∀rep host : mem → libc_world → Prop xs : listword bits : Z m : mem w : libc_world, libc_readyrep m w → hard_exit_wordsxs bits → ∀kind : handoff_kind, shutdown_atsndw ≠ HandedOffkind → contract_prelibc_hard_exit_contractrep host xs m w
intros
rep, host :
mem → libc_world → Prop
xs :
listword
bits :
Z
m :
w :
H :
libc_readyrep m w
H0 :
hard_exit_wordsxs bits
H1 :
∀kind : handoff_kind, shutdown_atsndw ≠ HandedOffkind
⊢
contract_prelibc_hard_exit_contractrep host xs m w
split ; exact H |
rep, host :
mem → libc_world → Prop
xs :
listword
bits :
Z
m :
w :
H :
libc_readyrep m w
H0 :
hard_exit_wordsxs bits
H1 :
∀kind : handoff_kind, shutdown_atsndw ≠ HandedOffkind
⊢
∃bits0 : Z, hard_exit_wordsxs bits0 ∧ ∀kind : handoff_kind, shutdown_atsndw ≠ HandedOffkind
exists bits
rep, host :
mem → libc_world → Prop
xs :
listword
bits :
Z
m :
w :
H :
libc_readyrep m w
H0 :
hard_exit_wordsxs bits
H1 :
∀kind : handoff_kind, shutdown_atsndw ≠ HandedOffkind
⊢
hard_exit_wordsxs bits ∧ ∀kind : handoff_kind, shutdown_atsndw ≠ HandedOffkind
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
split ; exact H |
exists bits
auto
All invocation and step facts use the supplied machine's inductives.
An admitted call has an unchanged unfinished prefix even with a false host witness. There is no completion/progress theorem here.
∀ rep host xs s m w
hard_exit_prerep xs m w
E.prefixlibc_hard_exit_contractrep host xs s m w [ ] [ ] s m w
Explore proof 6 tactics
Initial goal
⊢
∀rep host : mem → libc_world → Prop xs : listword s : R.state m : mem w : libc_world, hard_exit_prerep xs m w → E.prefixlibc_hard_exit_contractrep host xs s m w [ ] [ ] s m w
intros
⊢
E.prefixlibc_hard_exit_contractrep host xs s m w [ ] [ ] s m w
split ; constructor |
⊢
contract_prefixlibc_hard_exit_contractrep host xs m w [ ] [ ] m w
split ; reflexivity |
⊢
m = m ∧ [ ] = [ ] ∧ w = w ∨ ∃bits : Z, hard_exit_endpointxs w w bits ∧ [ ] = [ ] ∨ [ ] = ProcessExitprocess_statusmain_statusbits ∧ hostm w
split ; reflexivity |
⊢
[ ] = [ ] ∧ w = w ∨ ∃bits : Z, hard_exit_endpointxs w w bits ∧ [ ] = [ ] ∨ [ ] = ProcessExitprocess_statusmain_statusbits ∧ hostm w
left
⊢
[ ] = [ ] ∧ w = w
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
split ; constructor |
split ; reflexivity |
split ; reflexivity |
left
auto
The explicit request cutpoint also needs no host completion.
∀ rep host xs bits s m w w′
hard_exit_endpointxs w w′ bits
E.prefixlibc_hard_exit_contractrep host xs s m w [ ] [ ] s m w′
Explore proof 9 tactics
Initial goal
⊢
∀rep host : mem → libc_world → Prop xs : listword bits : Z s : R.state m : mem w w′ : libc_world, hard_exit_endpointxs w w′ bits → E.prefixlibc_hard_exit_contractrep host xs s m w [ ] [ ] s m w′
intros
rep, host :
mem → libc_world → Prop
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
H :
hard_exit_endpointxs w w′ bits
⊢
E.prefixlibc_hard_exit_contractrep host xs s m w [ ] [ ] s m w′
split ; constructor |
rep, host :
mem → libc_world → Prop
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
H :
hard_exit_endpointxs w w′ bits
⊢
contract_prefixlibc_hard_exit_contractrep host xs m w [ ] [ ] m w′
split ; reflexivity |
rep, host :
mem → libc_world → Prop
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
H :
hard_exit_endpointxs w w′ bits
⊢
m = m ∧ [ ] = [ ] ∧ w′ = w ∨ ∃bits0 : Z, hard_exit_endpointxs w w′ bits0 ∧ [ ] = [ ] ∨ [ ] = ProcessExitprocess_statusmain_statusbits0 ∧ hostm w′
split ; reflexivity |
rep, host :
mem → libc_world → Prop
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
H :
hard_exit_endpointxs w w′ bits
⊢
[ ] = [ ] ∧ w′ = w ∨ ∃bits0 : Z, hard_exit_endpointxs w w′ bits0 ∧ [ ] = [ ] ∨ [ ] = ProcessExitprocess_statusmain_statusbits0 ∧ hostm w′
right
rep, host :
mem → libc_world → Prop
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
H :
hard_exit_endpointxs w w′ bits
⊢
∃bits0 : Z, hard_exit_endpointxs w w′ bits0 ∧ [ ] = [ ] ∨ [ ] = ProcessExitprocess_statusmain_statusbits0 ∧ hostm w′
exists bits
rep, host :
mem → libc_world → Prop
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
H :
hard_exit_endpointxs w w′ bits
⊢
hard_exit_endpointxs w w′ bits ∧ [ ] = [ ] ∨ [ ] = ProcessExitprocess_statusmain_statusbits ∧ hostm w′
split ; exact H |
rep, host :
mem → libc_world → Prop
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
H :
hard_exit_endpointxs w w′ bits
⊢
[ ] = [ ] ∨ [ ] = ProcessExitprocess_statusmain_statusbits ∧ hostm w′
left
rep, host :
mem → libc_world → Prop
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
H :
hard_exit_endpointxs w w′ bits
⊢
[ ] = [ ]
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
split ; constructor |
split ; reflexivity |
split ; reflexivity |
right
exists bits
split ; exact H |
left
reflexivity
Construct a completed invocation only from an independent endpoint host witness; arguments and phase admission are checked separately.
∀ rep host r args xs bits s m w w′
E.invokelibc_hard_exit_contractrep host r args xs s m w ProcessExitprocess_statusmain_statusbits CallExitprocess_statusmain_statusbits s m w′
Explore proof 22 tactics
Initial goal
⊢
∀rep host : mem → libc_world → Prop r : call_result args : listarg xs : listword bits : Z s : R.state m : mem w w′ : libc_world, exit_abir args → hard_exit_prerep xs m w → hard_exit_endpointxs w w′ bits → hostm w′ → E.invokelibc_hard_exit_contractrep host r args xs s m w ProcessExitprocess_statusmain_statusbits CallExitprocess_statusmain_statusbits s m w′
intros rep host r args xs bits s m w w′ Habi Hpre Hend Hhost
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
E.invokelibc_hard_exit_contractrep host r args xs s m w ProcessExitprocess_statusmain_statusbits CallExitprocess_statusmain_statusbits s m w′
eapply E.invoke_normal with born := [ ]
7 openrep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
contract_abilibc_hard_exit_contractrep host r args
focused goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
contract_prelibc_hard_exit_contractrep host xs m w
focused goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
E.prefixlibc_hard_exit_contractrep host xs s m w [ ] ProcessExitprocess_statusmain_statusbits s m w′
focused goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
contract_postlibc_hard_exit_contractrep host xs m w [ ] ProcessExitprocess_statusmain_statusbits CallExitprocess_statusmain_statusbits m w′
focused goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀why : reason, CallExitprocess_statusmain_statusbits ≠ CallResourcewhy
focused goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀values : listword, CallExitprocess_statusmain_statusbits = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
focused goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
–exact Habi
6 opendeferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
contract_prelibc_hard_exit_contractrep host xs m w
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
E.prefixlibc_hard_exit_contractrep host xs s m w [ ] ProcessExitprocess_statusmain_statusbits s m w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
contract_postlibc_hard_exit_contractrep host xs m w [ ] ProcessExitprocess_statusmain_statusbits CallExitprocess_statusmain_statusbits m w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀why : reason, CallExitprocess_statusmain_statusbits ≠ CallResourcewhy
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀values : listword, CallExitprocess_statusmain_statusbits = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
–exact Hpre
5 opendeferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
E.prefixlibc_hard_exit_contractrep host xs s m w [ ] ProcessExitprocess_statusmain_statusbits s m w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
contract_postlibc_hard_exit_contractrep host xs m w [ ] ProcessExitprocess_statusmain_statusbits CallExitprocess_statusmain_statusbits m w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀why : reason, CallExitprocess_statusmain_statusbits ≠ CallResourcewhy
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀values : listword, CallExitprocess_statusmain_statusbits = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
–split ; constructor |
5 openrep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
contract_prefixlibc_hard_exit_contractrep host xs m w [ ] ProcessExitprocess_statusmain_statusbits m w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
contract_postlibc_hard_exit_contractrep host xs m w [ ] ProcessExitprocess_statusmain_statusbits CallExitprocess_statusmain_statusbits m w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀why : reason, CallExitprocess_statusmain_statusbits ≠ CallResourcewhy
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀values : listword, CallExitprocess_statusmain_statusbits = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
split ; reflexivity |
5 openrep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
m = m ∧ ProcessExitprocess_statusmain_statusbits = [ ] ∧ w′ = w ∨ ∃bits0 : Z, hard_exit_endpointxs w w′ bits0 ∧ ProcessExitprocess_statusmain_statusbits = [ ] ∨ ProcessExitprocess_statusmain_statusbits = ProcessExitprocess_statusmain_statusbits0 ∧ hostm w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
contract_postlibc_hard_exit_contractrep host xs m w [ ] ProcessExitprocess_statusmain_statusbits CallExitprocess_statusmain_statusbits m w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀why : reason, CallExitprocess_statusmain_statusbits ≠ CallResourcewhy
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀values : listword, CallExitprocess_statusmain_statusbits = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
split ; reflexivity |
5 openrep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
ProcessExitprocess_statusmain_statusbits = [ ] ∧ w′ = w ∨ ∃bits0 : Z, hard_exit_endpointxs w w′ bits0 ∧ ProcessExitprocess_statusmain_statusbits = [ ] ∨ ProcessExitprocess_statusmain_statusbits = ProcessExitprocess_statusmain_statusbits0 ∧ hostm w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
contract_postlibc_hard_exit_contractrep host xs m w [ ] ProcessExitprocess_statusmain_statusbits CallExitprocess_statusmain_statusbits m w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀why : reason, CallExitprocess_statusmain_statusbits ≠ CallResourcewhy
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀values : listword, CallExitprocess_statusmain_statusbits = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
right
5 openrep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∃bits0 : Z, hard_exit_endpointxs w w′ bits0 ∧ ProcessExitprocess_statusmain_statusbits = [ ] ∨ ProcessExitprocess_statusmain_statusbits = ProcessExitprocess_statusmain_statusbits0 ∧ hostm w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
contract_postlibc_hard_exit_contractrep host xs m w [ ] ProcessExitprocess_statusmain_statusbits CallExitprocess_statusmain_statusbits m w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀why : reason, CallExitprocess_statusmain_statusbits ≠ CallResourcewhy
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀values : listword, CallExitprocess_statusmain_statusbits = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
exists bits
5 openrep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
hard_exit_endpointxs w w′ bits ∧ ProcessExitprocess_statusmain_statusbits = [ ] ∨ ProcessExitprocess_statusmain_statusbits = ProcessExitprocess_statusmain_statusbits ∧ hostm w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
contract_postlibc_hard_exit_contractrep host xs m w [ ] ProcessExitprocess_statusmain_statusbits CallExitprocess_statusmain_statusbits m w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀why : reason, CallExitprocess_statusmain_statusbits ≠ CallResourcewhy
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀values : listword, CallExitprocess_statusmain_statusbits = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
split ; exact Hend |
5 openrep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
ProcessExitprocess_statusmain_statusbits = [ ] ∨ ProcessExitprocess_statusmain_statusbits = ProcessExitprocess_statusmain_statusbits ∧ hostm w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
contract_postlibc_hard_exit_contractrep host xs m w [ ] ProcessExitprocess_statusmain_statusbits CallExitprocess_statusmain_statusbits m w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀why : reason, CallExitprocess_statusmain_statusbits ≠ CallResourcewhy
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀values : listword, CallExitprocess_statusmain_statusbits = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
right
5 openrep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
ProcessExitprocess_statusmain_statusbits = ProcessExitprocess_statusmain_statusbits ∧ hostm w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
contract_postlibc_hard_exit_contractrep host xs m w [ ] ProcessExitprocess_statusmain_statusbits CallExitprocess_statusmain_statusbits m w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀why : reason, CallExitprocess_statusmain_statusbits ≠ CallResourcewhy
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀values : listword, CallExitprocess_statusmain_statusbits = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
auto
4 opendeferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
contract_postlibc_hard_exit_contractrep host xs m w [ ] ProcessExitprocess_statusmain_statusbits CallExitprocess_statusmain_statusbits m w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀why : reason, CallExitprocess_statusmain_statusbits ≠ CallResourcewhy
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀values : listword, CallExitprocess_statusmain_statusbits = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
–exists bits
4 openrep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
hard_exit_endpointxs w w′ bits ∧ ProcessExitprocess_statusmain_statusbits = ProcessExitprocess_statusmain_statusbits ∧ CallExitprocess_statusmain_statusbits = CallExitprocess_statusmain_statusbits ∧ hostm w′
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀why : reason, CallExitprocess_statusmain_statusbits ≠ CallResourcewhy
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀values : listword, CallExitprocess_statusmain_statusbits = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
auto
3 opendeferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀why : reason, CallExitprocess_statusmain_statusbits ≠ CallResourcewhy
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀values : listword, CallExitprocess_statusmain_statusbits = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
–intros why Hbad
3 openrep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
why :
Hbad :
⊢
False
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀values : listword, CallExitprocess_statusmain_statusbits = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
discriminate
2 opendeferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀values : listword, CallExitprocess_statusmain_statusbits = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
–intros values Hbad
2 openrep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
values :
listword
Hbad :
CallExitprocess_statusmain_statusbits = CallReturnvalues
⊢
return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
discriminate
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∀status : Z, CallExitprocess_statusmain_statusbits = CallExitstatus → ∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
–intros status Hstatus
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
status :
Z
Hstatus :
CallExitprocess_statusmain_statusbits = CallExitstatus
⊢
∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitstatus
injection Hstatus as ←
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
∃before : listevent, ProcessExitprocess_statusmain_statusbits = before ++ ProcessExitprocess_statusmain_statusbits
exists [ ]
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
bits :
Z
s :
R.state
m :
w, w′ :
Habi :
exit_abir args
Hpre :
hard_exit_prerep xs m w
Hend :
hard_exit_endpointxs w w′ bits
Hhost :
hostm w′
⊢
ProcessExitprocess_statusmain_statusbits = [ ] ++ ProcessExitprocess_statusmain_statusbits
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep host r args xs bits s m w w′ Habi Hpre Hend Hhost
eapply E.invoke_normal with born := [ ]
–exact Habi
–exact Hpre
–split ; constructor |
split ; reflexivity |
split ; reflexivity |
right
exists bits
split ; exact Hend |
right
auto
–exists bits
auto
–intros why Hbad
discriminate
–intros values Hbad
discriminate
–intros status Hstatus
injection Hstatus as ←
exists [ ]
reflexivity
No normal or resource rule can produce an ordinary return.
∀ rep host r args xs s m w trace values s′ m′ w′
¬E.invokelibc_hard_exit_contractrep host r args xs s m w trace CallReturnvalues s′ m′ w′
Explore proof 3 tactics
Initial goal
⊢
∀rep host : mem → libc_world → Prop r : call_result args : listarg xs : listword s : R.state m : mem w : libc_world trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, ¬E.invokelibc_hard_exit_contractrep host r args xs s m w trace CallReturnvalues s′ m′ w′
intros rep host r args xs s m w trace values s′ m′ w′ Hcall
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hcall :
E.invokelibc_hard_exit_contractrep host r args xs s m w trace CallReturnvalues s′ m′ w′
⊢
False
inversion Hcall ; subst
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hcall :
E.invokelibc_hard_exit_contractrep host r args xs s m w trace CallReturnvalues s′ m′ w′
born :
listZ
H :
contract_abilibc_hard_exit_contractrep host r args
H0 :
contract_prelibc_hard_exit_contractrep host xs m w
H1 :
E.prefixlibc_hard_exit_contractrep host xs s m w born trace s′ m′ w′
H2 :
contract_postlibc_hard_exit_contractrep host xs m w born trace CallReturnvalues m′ w′
H3 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H4 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnslibc_hard_exit_contractrep host values0 ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w born m′ values0
H5 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
False
match goal withHpost : contract_post_ _ _ _ _ _ _ _ _ |- _⇒destruct Hpost as bits & _ & _ & Hbad & _ ; discriminate Hbadend
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep host r args xs s m w trace values s′ m′ w′ Hcall
inversion Hcall ; subst
match goal withHpost : contract_post_ _ _ _ _ _ _ _ _ |- _⇒destruct Hpost as bits & _ & _ & Hbad & _ ; discriminate Hbadend
An actual completed call supplies the exact current snapshot and the global request relation used by Ending, not a sibling invoke.
∀ rep host r args xs s m w trace ending s′ m′ w′
E.invokelibc_hard_exit_contractrep host r args xs s m w trace ending s′ m′ w′
s′ = s ∧ m′ = m ∧ ∃bits, hard_exit_endpointxs w w′ bits ∧ trace = ProcessExitprocess_statusmain_statusbits ∧ ending = CallExitprocess_statusmain_statusbits ∧ hostm′ w′
Explore proof 8 tactics
Initial goal
⊢
∀rep host : mem → libc_world → Prop r : call_result args : listarg xs : listword s : R.state m : mem w : libc_world trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, E.invokelibc_hard_exit_contractrep host r args xs s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ ∃bits : Z, hard_exit_endpointxs w w′ bits ∧ trace = ProcessExitprocess_statusmain_statusbits ∧ ending = CallExitprocess_statusmain_statusbits ∧ hostm′ w′
intros rep host r args xs s m w trace ending s′ m′ w′ Hcall
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
E.invokelibc_hard_exit_contractrep host r args xs s m w trace ending s′ m′ w′
⊢
s′ = s ∧ m′ = m ∧ ∃bits : Z, hard_exit_endpointxs w w′ bits ∧ trace = ProcessExitprocess_statusmain_statusbits ∧ ending = CallExitprocess_statusmain_statusbits ∧ hostm′ w′
destruct Hcall as trace ending s′ m′ w′ born Habi Hpre He Hp Hpost Hresource Hvalues Hexit | why trace s′ m′ w′ born Habi Hpre Hp Hfailure Hresource ; | contradiction
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
born :
listZ
Habi :
contract_abilibc_hard_exit_contractrep host r args
Hpre :
contract_prelibc_hard_exit_contractrep host xs m w
He :
E.effectscontract_sourceslibc_hard_exit_contractrep host xs m w contract_writeslibc_hard_exit_contractrep host xs m w contract_releaseslibc_hard_exit_contractrep host xs m w contract_requestslibc_hard_exit_contractrep host xs m w s m [ ] s′ m′ born
Hp :
contract_prefixlibc_hard_exit_contractrep host xs m w born trace m′ w′
Hpost :
contract_postlibc_hard_exit_contractrep host xs m w born trace ending m′ w′
Hresource :
∀why : reason, ending ≠ CallResourcewhy
Hvalues :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w born m′ values
Hexit :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
s′ = s ∧ m′ = m ∧ ∃bits : Z, hard_exit_endpointxs w w′ bits ∧ trace = ProcessExitprocess_statusmain_statusbits ∧ ending = CallExitprocess_statusmain_statusbits ∧ hostm′ w′
destruct Hp as Hborn Hm _
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
born :
listZ
Habi :
contract_abilibc_hard_exit_contractrep host r args
Hpre :
contract_prelibc_hard_exit_contractrep host xs m w
He :
E.effectscontract_sourceslibc_hard_exit_contractrep host xs m w contract_writeslibc_hard_exit_contractrep host xs m w contract_releaseslibc_hard_exit_contractrep host xs m w contract_requestslibc_hard_exit_contractrep host xs m w s m [ ] s′ m′ born
Hborn :
born = [ ]
Hm :
m′ = m
Hpost :
contract_postlibc_hard_exit_contractrep host xs m w born trace ending m′ w′
Hresource :
∀why : reason, ending ≠ CallResourcewhy
Hvalues :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w born m′ values
Hexit :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
s′ = s ∧ m′ = m ∧ ∃bits : Z, hard_exit_endpointxs w w′ bits ∧ trace = ProcessExitprocess_statusmain_statusbits ∧ ending = CallExitprocess_statusmain_statusbits ∧ hostm′ w′
subst born m′
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
w′ :
Habi :
contract_abilibc_hard_exit_contractrep host r args
Hpre :
contract_prelibc_hard_exit_contractrep host xs m w
He :
E.effectscontract_sourceslibc_hard_exit_contractrep host xs m w contract_writeslibc_hard_exit_contractrep host xs m w contract_releaseslibc_hard_exit_contractrep host xs m w contract_requestslibc_hard_exit_contractrep host xs m w s m [ ] s′ m [ ]
Hpost :
contract_postlibc_hard_exit_contractrep host xs m w [ ] trace ending m w′
Hresource :
∀why : reason, ending ≠ CallResourcewhy
Hvalues :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
Hexit :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
s′ = s ∧ m = m ∧ ∃bits : Z, hard_exit_endpointxs w w′ bits ∧ trace = ProcessExitprocess_statusmain_statusbits ∧ ending = CallExitprocess_statusmain_statusbits ∧ hostm w′
split
2 openrep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
w′ :
Habi :
contract_abilibc_hard_exit_contractrep host r args
Hpre :
contract_prelibc_hard_exit_contractrep host xs m w
He :
E.effectscontract_sourceslibc_hard_exit_contractrep host xs m w contract_writeslibc_hard_exit_contractrep host xs m w contract_releaseslibc_hard_exit_contractrep host xs m w contract_requestslibc_hard_exit_contractrep host xs m w s m [ ] s′ m [ ]
Hpost :
contract_postlibc_hard_exit_contractrep host xs m w [ ] trace ending m w′
Hresource :
∀why : reason, ending ≠ CallResourcewhy
Hvalues :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
Hexit :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
s′ = s
focused goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
w′ :
Habi :
contract_abilibc_hard_exit_contractrep host r args
Hpre :
contract_prelibc_hard_exit_contractrep host xs m w
He :
E.effectscontract_sourceslibc_hard_exit_contractrep host xs m w contract_writeslibc_hard_exit_contractrep host xs m w contract_releaseslibc_hard_exit_contractrep host xs m w contract_requestslibc_hard_exit_contractrep host xs m w s m [ ] s′ m [ ]
Hpost :
contract_postlibc_hard_exit_contractrep host xs m w [ ] trace ending m w′
Hresource :
∀why : reason, ending ≠ CallResourcewhy
Hvalues :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
Hexit :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
m = m ∧ ∃bits : Z, hard_exit_endpointxs w w′ bits ∧ trace = ProcessExitprocess_statusmain_statusbits ∧ ending = CallExitprocess_statusmain_statusbits ∧ hostm w′
–clear - He
2 openrep, host :
mem → libc_world → Prop
xs :
listword
s :
R.state
m :
w :
s′ :
R.state
He :
E.effectscontract_sourceslibc_hard_exit_contractrep host xs m w contract_writeslibc_hard_exit_contractrep host xs m w contract_releaseslibc_hard_exit_contractrep host xs m w contract_requestslibc_hard_exit_contractrep host xs m w s m [ ] s′ m [ ]
⊢
s′ = s
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
w′ :
Habi :
contract_abilibc_hard_exit_contractrep host r args
Hpre :
contract_prelibc_hard_exit_contractrep host xs m w
He :
E.effectscontract_sourceslibc_hard_exit_contractrep host xs m w contract_writeslibc_hard_exit_contractrep host xs m w contract_releaseslibc_hard_exit_contractrep host xs m w contract_requestslibc_hard_exit_contractrep host xs m w s m [ ] s′ m [ ]
Hpost :
contract_postlibc_hard_exit_contractrep host xs m w [ ] trace ending m w′
Hresource :
∀why : reason, ending ≠ CallResourcewhy
Hvalues :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
Hexit :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
m = m ∧ ∃bits : Z, hard_exit_endpointxs w w′ bits ∧ trace = ProcessExitprocess_statusmain_statusbits ∧ ending = CallExitprocess_statusmain_statusbits ∧ hostm w′
induction He ; reflexivity | exact IHHe | contradiction
deferred goal
rep, host :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
w′ :
Habi :
contract_abilibc_hard_exit_contractrep host r args
Hpre :
contract_prelibc_hard_exit_contractrep host xs m w
He :
E.effectscontract_sourceslibc_hard_exit_contractrep host xs m w contract_writeslibc_hard_exit_contractrep host xs m w contract_releaseslibc_hard_exit_contractrep host xs m w contract_requestslibc_hard_exit_contractrep host xs m w s m [ ] s′ m [ ]
Hpost :
contract_postlibc_hard_exit_contractrep host xs m w [ ] trace ending m w′
Hresource :
∀why : reason, ending ≠ CallResourcewhy
Hvalues :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnslibc_hard_exit_contractrep host values ∧ Forallword_authoritycontract_sourceslibc_hard_exit_contractrep host xs m w [ ] m values
Hexit :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
m = m ∧ ∃bits : Z, hard_exit_endpointxs w w′ bits ∧ trace = ProcessExitprocess_statusmain_statusbits ∧ ending = CallExitprocess_statusmain_statusbits ∧ hostm w′
–split ; reflexivity | exact Hpost
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep host r args xs s m w trace ending s′ m′ w′ Hcall
destruct Hcall as trace ending s′ m′ w′ born Habi Hpre He Hp Hpost Hresource Hvalues Hexit | why trace s′ m′ w′ born Habi Hpre Hp Hfailure Hresource ; | contradiction
destruct Hp as Hborn Hm _
subst born m′
split
–clear - He
induction He ; reflexivity | exact IHHe | contradiction
–split ; reflexivity | exact Hpost
Ordinary-machine dispatch preserves external-site precedence and terminates in this very machine. Ending separately intercepts these symbols; relating its host/representation predicates is a further compatibility obligation, not an automatic executor equivalence.
∀ rep host registry ge c site xs s w trace status s′ m′ w′
external_sitege c site
registrysite_namesite = Somelibc_hard_exit_contractrep host
map_optionarg_xge fr_envc_framec site_argssite = Somexs
E.invokelibc_hard_exit_contractrep host site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
M.stepregistry ge M.Runningc, s w trace M.StoppedExternalExitstatus M.P.I.RM.with_memc m′, s′ w′
Explore proof 2 tactics
Initial goal
⊢
∀rep host : mem → libc_world → Prop registry : name → optioncontractlibc_world ge : genv c : config site : call_site xs : listword s : R.state w : libc_world trace : listevent status : Z s′ : R.state m′ : mem w′ : libc_world, external_sitege c site → registrysite_namesite = Somelibc_hard_exit_contractrep host → map_optionarg_xge fr_envc_framec site_argssite = Somexs → E.invokelibc_hard_exit_contractrep host site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′ → M.stepregistry ge M.Runningc, s w trace M.StoppedExternalExitstatus M.P.I.RM.with_memc m′, s′ w′
intros
rep, host :
mem → libc_world → Prop
registry :
name → optioncontractlibc_world
ge :
c :
site :
xs :
listword
s :
R.state
w :
trace :
listevent
status :
Z
s′ :
R.state
m′ :
w′ :
H :
external_sitege c site
H0 :
registrysite_namesite = Somelibc_hard_exit_contractrep host
H1 :
map_optionarg_xge fr_envc_framec site_argssite = Somexs
H2 :
E.invokelibc_hard_exit_contractrep host site_resultsite site_argssite xs s c_memc w trace CallExitstatus s′ m′ w′
⊢
M.stepregistry ge M.Runningc, s w trace M.StoppedExternalExitstatus M.P.I.RM.with_memc m′, s′ w′
eapply M.step_exit ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
eapply M.step_exit ; eauto
Controls distinguish full signed shutdown status from the host byte, and requests from completed termination.
fstconversion_world, mkShutdownHandlers 0 mkRegistration9 AtExitTAtom"cleanup" 8%nat mkStreamByteOriented 65; 66 false
Explore proof 6 tactics
Initial goal
⊢
hard_exit_endpointWInt2 ^ 32 − 257 before after 2 ^ 32 − 257
split ; split ; reflexivity | lia |
⊢
fstafter = fstbefore ∧ exit_requestHardExit main_status2 ^ 32 − 257 sndbefore sndafter
split ; reflexivity |
⊢
exit_requestHardExit main_status2 ^ 32 − 257 sndbefore sndafter
change exit_requestHardExit −257 sndbefore sndafter
⊢
exit_requestHardExit −257 sndbefore sndafter
apply request_hard
⊢
∀kind : handoff_kind, shutdown_atsndbefore ≠ HandedOffkind
intros kind
kind :
⊢
shutdown_atsndbefore ≠ HandedOffkind
discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; split ; reflexivity | lia |
split ; reflexivity |
change exit_requestHardExit −257 sndbefore sndafter
apply request_hard
intros kind
discriminate
Explore proof 2 tactics
Initial goal
⊢
process_statusmain_status2 ^ 32 − 257 = 255
vm_compute
⊢
255 = 255
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
vm_compute
reflexivity
Pending callbacks, consumed history and outstanding bytes survive; no hard-exit summary pretends to run callbacks or flush.
180Example hard_request_retains_obligations: shutdown_pendingsndafter = mkRegistration9 AtExitTAtom"cleanup" ∧ shutdown_consumedsndafter = 8%nat ∧ outstandingshutdown_stdoutsndafter = 65; 66
Explore proof 1 tactics
Initial goal
⊢
shutdown_pendingsndafter = registration_token ≔ 9; registration_callback ≔ AtExitTAtom"cleanup" ∧ shutdown_consumedsndafter = 8%nat ∧ outstandingshutdown_stdoutsndafter = 65; 66
repeat split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
repeat split ; reflexivity
185Example blocked_host_prefix: M.E.prefixlibc_hard_exit_contractλ_ _ ⇒ True λ_ _ ⇒ False WInt2 ^ 32 − 257 InterpRuntime.start conversion_mem before [ ] [ ] InterpRuntime.start conversion_mem after
Explore proof 2 tactics
Initial goal
⊢
M.E.prefixlibc_hard_exit_contractλ_ : mem _ : libc_world ⇒ True λ_ : mem _ : libc_world ⇒ False WInt2 ^ 32 − 257 InterpRuntime.start conversion_mem before [ ] [ ] InterpRuntime.start conversion_mem after
eapply X.hard_exit_requested
2 open⊢
hard_exit_endpointWInt2 ^ 32 − 257 before after
shelved goal
⊢
Z
exact signed_status_endpoint
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
eapply X.hard_exit_requested
exact signed_status_endpoint
191Example false_host_no_completion: ∀rep r args xs s m w trace ending s′ m′ w′, ¬M.E.invokelibc_hard_exit_contractrep λ_ _ ⇒ False r args xs s m w trace ending s′ m′ w′
Explore proof 3 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop r : call_result args : listarg xs : listword s : InterpRuntime.state m : mem w : libc_world trace : listevent ending : call_end s′ : InterpRuntime.state m′ : mem w′ : libc_world, ¬M.E.invokelibc_hard_exit_contractrep λ_ : mem _ : libc_world ⇒ False r args xs s m w trace ending s′ m′ w′
intros rep r args xs s m w trace ending s′ m′ w′ Hcall
rep :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
m :
w :
trace :
listevent
ending :
m′ :
w′ :
Hcall :
M.E.invokelibc_hard_exit_contractrep λ_ : mem _ : libc_world ⇒ False r args xs s m w trace ending s′ m′ w′
⊢
False
destruct X.hard_exit_exact_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as _ & _ & bits & _ & _ & _ & Hfalse
rep :
mem → libc_world → Prop
r :
args :
listarg
xs :
listword
m :
w :
trace :
listevent
ending :
m′ :
w′ :
Hcall :
M.E.invokelibc_hard_exit_contractrep λ_ : mem _ : libc_world ⇒ False r args xs s m w trace ending s′ m′ w′
bits :
Z
Hfalse :
False
⊢
False
exact Hfalse
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep r args xs s m w trace ending s′ m′ w′ Hcall
destruct X.hard_exit_exact_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as _ & _ & bits & _ & _ & _ & Hfalse
exact Hfalse
Explore proof 3 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop m : mem, ¬hard_exit_prerep WInt0 m after
intros rep m _ & bits & _ & Hphase
rep :
mem → libc_world → Prop
m :
bits :
Z
Hphase :
∀kind : handoff_kind, shutdown_atsndafter ≠ HandedOffkind
⊢
False
apply HphaseHardExit
rep :
mem → libc_world → Prop
m :
bits :
Z
Hphase :
∀kind : handoff_kind, shutdown_atsndafter ≠ HandedOffkind
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.