rocq/theories/Composition.v
A trusted puts contract with one continuous logical stdout and registration inventory. The additional guarantees are libc obligations, not a FILE implementation or a native coverage proof.
From Stdlib Require Import String ZArith List Lia
From Nanofil Require Import Term Syntax Values Memory Runtime Ops Semantics ExternalCalls Stdio Shutdown ExternalMachine Hi
Import ListNotations
Open Scope Z_scope
Open Scope list_scope
Keep the capability-backed stdio world, output obligations and exit registrations together; shutdown must not choose a new stdout state.
| program_stdio | ||
| program_stdout | ||
| program_pending | : listregistration |
Entry supplies well-formed logical output and distinct registration instances.
stream_wfprogram_stdoutw ∧ NoDupmapregistration_token program_pendingw
A prefix has either no acceptance observation or one cumulative summary. An empty trace must not hide accepted bytes. It is not an incremental sequence that can be concatenated with another cumulative summary.
trace = [ ] ∧ acceptedactions = [ ] ∨ trace = puts_observationactions
Original argument memory fixes this call's source string. Its finite stream evolution may settle old output but accepts only a prefix of this string and newline. No eventual return or resumability is asserted.
34Definition puts_stream_prefixxs : listword m : mem q : stream_state trace : listevent q′ : stream_state : Prop ≔
∃p bytes actions tail, xs = WPtrp ∧ c_stringm p bytes ∧ stream_runq actions q′ ∧ bytes ++ 10 = acceptedactions ++ tail ∧ prefix_observationtrace actions
Returning puts couples the exact before/after stdout states to its result. The ordinary contract still owns memory authority and ABI.
43Definition puts_stream_postxs : listword m : mem q : stream_state trace : listevent ending : call_end q′ : stream_state : Prop ≔
∃p bytes actions result, xs = WPtrp ∧ c_stringm p bytes ∧ puts_protocolbytes q actions result q′ ∧ trace = puts_observationactions ∧ ending = CallReturnWIntresult
This strengthened contract retains puts' original capabilities, memory footprints and requests. Trusted prefix guarantees connect every normal, resource or unfinished endpoint to stdout and preserve registrations.
54Definition program_putsrep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop : contractprogram_world ≔
mkContractprogram_world RClassW puts_abi λxs m w ⇒ puts_prerep xs m program_stdiow ∧ program_world_wfw ∧ orientationprogram_stdoutw ≠ WideOriented λ_ _ w ⇒ stdio_rootsprogram_stdiow λ_ _ w ⇒ stdio_rootsprogram_stdiow λ_ _ _ ⇒ [ ] λxs m w ⇒ requestsxs m program_stdiow λxs m w born trace m′ w′ ⇒ puts_prefixrep xs m program_stdiow born trace m′ program_stdiow′ ∧ program_pendingw′ = program_pendingw ∧ puts_stream_prefixxs m program_stdoutw trace program_stdoutw′ λxs m w born trace ending m′ w′ ⇒ puts_postxs m program_stdiow born trace ending m′ program_stdiow′ ∧ puts_stream_postxs m program_stdoutw trace ending program_stdoutw′ resource_reason puts_panic
Every observed prefix carries an exact accounting witness, including prefixes which block or end for lack of resources.
∀ xs m q trace q′
puts_stream_prefixxs m q trace q′
∃actions, stream_runq actions q′ ∧ prefix_observationtrace actions ∧ outstandingq ++ acceptedactions = resolvedactions ++ outstandingq′
Explore proof 5 tactics
Initial goal
⊢
∀xs : listword m : mem q : stream_state trace : listevent q′ : stream_state, puts_stream_prefixxs m q trace q′ → ∃actions : liststream_action, stream_runq actions q′ ∧ prefix_observationtrace actions ∧ outstandingq ++ acceptedactions = resolvedactions ++ outstandingq′
intros xs m q trace q′ p & bytes & actions & tail & Hx & Hstr & Hrun & Hb & Hobs
xs :
listword
m :
q :
trace :
listevent
q′ :
p :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hx :
xs = WPtrp
Hstr :
c_stringm p bytes
Hrun :
stream_runq actions q′
Hb :
bytes ++ 10 = acceptedactions ++ tail
Hobs :
prefix_observationtrace actions
⊢
∃actions0 : liststream_action, stream_runq actions0 q′ ∧ prefix_observationtrace actions0 ∧ outstandingq ++ acceptedactions0 = resolvedactions0 ++ outstandingq′
exists actions
xs :
listword
m :
q :
trace :
listevent
q′ :
p :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hx :
xs = WPtrp
Hstr :
c_stringm p bytes
Hrun :
stream_runq actions q′
Hb :
bytes ++ 10 = acceptedactions ++ tail
Hobs :
prefix_observationtrace actions
⊢
stream_runq actions q′ ∧ prefix_observationtrace actions ∧ outstandingq ++ acceptedactions = resolvedactions ++ outstandingq′
repeat split ; auto
xs :
listword
m :
q :
trace :
listevent
q′ :
p :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hx :
xs = WPtrp
Hstr :
c_stringm p bytes
Hrun :
stream_runq actions q′
Hb :
bytes ++ 10 = acceptedactions ++ tail
Hobs :
prefix_observationtrace actions
⊢
outstandingq ++ acceptedactions = resolvedactions ++ outstandingq′
apply stream_accounting
xs :
listword
m :
q :
trace :
listevent
q′ :
p :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hx :
xs = WPtrp
Hstr :
c_stringm p bytes
Hrun :
stream_runq actions q′
Hb :
bytes ++ 10 = acceptedactions ++ tail
Hobs :
prefix_observationtrace actions
⊢
stream_runq actions q′
exact Hrun
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros xs m q trace q′ p & bytes & actions & tail & Hx & Hstr & Hrun & Hb & Hobs
exists actions
repeat split ; auto
apply stream_accounting
exact Hrun
Stream well-formedness is derived from actual protocol steps, not stipulated independently at a prefix endpoint.
Explore proof 2 tactics
Initial goal
⊢
∀xs : listword m : mem q : stream_state trace : listevent q′ : stream_state, puts_stream_prefixxs m q trace q′ → stream_wfq → stream_wfq′
intros xs m q trace q′ p & bytes & actions & tail & _ & _ & Hrun & _ Hwf
xs :
listword
m :
q :
trace :
listevent
q′ :
p :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hrun :
stream_runq actions q′
Hwf :
⊢
eapply stream_run_wf ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros xs m q trace q′ p & bytes & actions & tail & _ & _ & Hrun & _ Hwf
eapply stream_run_wf ; eauto
No stream action turns a nonwide stream into a wide one.
Explore proof 5 tactics
Initial goal
⊢
∀q : stream_state actions : liststream_action q′ : stream_state, stream_runq actions q′ → orientationq ≠ WideOriented → orientationq′ ≠ WideOriented
intros q actions q′ H
⊢
orientationq ≠ WideOriented → orientationq′ ≠ WideOriented
induction H ; auto |
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
H0 :
stream_runq1 actions q′
IHstream_run :
orientationq1 ≠ WideOriented → orientationq′ ≠ WideOriented
⊢
orientationq ≠ WideOriented → orientationq′ ≠ WideOriented
intros Ho
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
H0 :
stream_runq1 actions q′
IHstream_run :
orientationq1 ≠ WideOriented → orientationq′ ≠ WideOriented
Ho :
⊢
apply IHstream_run
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
H0 :
stream_runq1 actions q′
IHstream_run :
orientationq1 ≠ WideOriented → orientationq′ ≠ WideOriented
Ho :
⊢
destruct H ; simpl ; discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros q actions q′ H
induction H ; auto |
intros Ho
apply IHstream_run
destruct H ; simpl ; discriminate
Prefix output errors remain set; normal completion is not required.
Explore proof 2 tactics
Initial goal
⊢
∀xs : listword m : mem q : stream_state trace : listevent q′ : stream_state, puts_stream_prefixxs m q trace q′ → stream_errorq = true → stream_errorq′ = true
intros xs m q trace q′ p & bytes & actions & tail & _ & _ & Hrun & _ Herr
xs :
listword
m :
q :
trace :
listevent
q′ :
p :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hrun :
stream_runq actions q′
Herr :
stream_errorq = true
⊢
stream_errorq′ = true
eapply stream_error_sticky ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros xs m q trace q′ p & bytes & actions & tail & _ & _ & Hrun & _ Herr
eapply stream_error_sticky ; eauto
Neither normal nor unfinished puts prefixes can report process exit.
Explore proof 2 tactics
Initial goal
⊢
∀xs : listword m : mem q : stream_state trace : listevent q′ : stream_state status : Z, puts_stream_prefixxs m q trace q′ → ¬InProcessExitstatus trace
intros xs m q trace q′ status p & bytes & actions & tail & _ & _ & _ & _ & Hobs
xs :
listword
m :
q :
trace :
listevent
q′ :
status :
Z
p :
bytes :
listZ
actions :
liststream_action
tail :
listZ
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 xs m q trace q′ status p & bytes & actions & tail & _ & _ & _ & _ & Hobs
destruct Hobs as → _ | → ; simpl ; intuition discriminate
The strengthened contract is conservative over the existing memory/effect boundary: forgetting logical output and registrations gives ordinary puts.
Projection does not re-run the call or change its exact effect path.
∀ rep requests xs s m w born trace s′ m′ w′
E.prefixprogram_putsrep requests xs s m w born trace s′ m′ w′
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
Explore proof 2 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop xs : listword s : R.state m : mem w : program_world born : listZ trace : listevent s′ : R.state m′ : mem w′ : program_world, E.prefixprogram_putsrep requests xs s m w born trace s′ m′ w′ → E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
intros rep requests xs s m w born trace s′ m′ w′ He Hp _
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
xs :
listword
s :
R.state
m :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
He :
E.effectscontract_sourcesprogram_putsrep requests xs m w contract_writesprogram_putsrep requests xs m w contract_releasesprogram_putsrep requests xs m w contract_requestsprogram_putsrep requests xs m w s m [ ] s′ m′ born
Hp :
puts_prefixrep xs m program_stdiow born trace m′ program_stdiow′
⊢
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
split ; assumption
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests xs s m w born trace s′ m′ w′ He Hp _
split ; assumption
Raw prefixes do not include contract preconditions: entry well-formedness is an explicit premise, even when the call never returns.
∀ rep requests xs s m w born trace s′ m′ w′
E.prefixprogram_putsrep requests xs s m w born trace s′ m′ w′
program_pendingw′ = program_pendingw ∧ puts_stream_prefixxs m program_stdoutw trace program_stdoutw′ ∧ program_world_wfw′
Explore proof 7 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop xs : listword s : R.state m : mem w : program_world born : listZ trace : listevent s′ : R.state m′ : mem w′ : program_world, E.prefixprogram_putsrep requests xs s m w born trace s′ m′ w′ → program_world_wfw → program_pendingw′ = program_pendingw ∧ puts_stream_prefixxs m program_stdoutw trace program_stdoutw′ ∧ program_world_wfw′
intros rep requests xs s m w born trace s′ m′ w′ He Hp Hpending Hstream Hwf Hnd
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
xs :
listword
s :
R.state
m :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
He :
E.effectscontract_sourcesprogram_putsrep requests xs m w contract_writesprogram_putsrep requests xs m w contract_releasesprogram_putsrep requests xs m w contract_requestsprogram_putsrep requests xs m w s m [ ] s′ m′ born
Hp :
puts_prefixrep xs m program_stdiow born trace m′ program_stdiow′
Hpending :
Hstream :
puts_stream_prefixxs m program_stdoutw trace program_stdoutw′
Hwf :
Hnd :
NoDupmapregistration_token program_pendingw
⊢
program_pendingw′ = program_pendingw ∧ puts_stream_prefixxs m program_stdoutw trace program_stdoutw′ ∧ program_world_wfw′
split ; exact Hpending |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
xs :
listword
s :
R.state
m :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
He :
E.effectscontract_sourcesprogram_putsrep requests xs m w contract_writesprogram_putsrep requests xs m w contract_releasesprogram_putsrep requests xs m w contract_requestsprogram_putsrep requests xs m w s m [ ] s′ m′ born
Hp :
puts_prefixrep xs m program_stdiow born trace m′ program_stdiow′
Hpending :
Hstream :
puts_stream_prefixxs m program_stdoutw trace program_stdoutw′
Hwf :
Hnd :
NoDupmapregistration_token program_pendingw
⊢
puts_stream_prefixxs m program_stdoutw trace program_stdoutw′ ∧ program_world_wfw′
split ; exact Hstream |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
xs :
listword
s :
R.state
m :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
He :
E.effectscontract_sourcesprogram_putsrep requests xs m w contract_writesprogram_putsrep requests xs m w contract_releasesprogram_putsrep requests xs m w contract_requestsprogram_putsrep requests xs m w s m [ ] s′ m′ born
Hp :
puts_prefixrep xs m program_stdiow born trace m′ program_stdiow′
Hpending :
Hstream :
puts_stream_prefixxs m program_stdoutw trace program_stdoutw′
Hwf :
Hnd :
NoDupmapregistration_token program_pendingw
split
2 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
xs :
listword
s :
R.state
m :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
He :
E.effectscontract_sourcesprogram_putsrep requests xs m w contract_writesprogram_putsrep requests xs m w contract_releasesprogram_putsrep requests xs m w contract_requestsprogram_putsrep requests xs m w s m [ ] s′ m′ born
Hp :
puts_prefixrep xs m program_stdiow born trace m′ program_stdiow′
Hpending :
Hstream :
puts_stream_prefixxs m program_stdoutw trace program_stdoutw′
Hwf :
Hnd :
NoDupmapregistration_token program_pendingw
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
xs :
listword
s :
R.state
m :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
He :
E.effectscontract_sourcesprogram_putsrep requests xs m w contract_writesprogram_putsrep requests xs m w contract_releasesprogram_putsrep requests xs m w contract_requestsprogram_putsrep requests xs m w s m [ ] s′ m′ born
Hp :
puts_prefixrep xs m program_stdiow born trace m′ program_stdiow′
Hpending :
Hstream :
puts_stream_prefixxs m program_stdoutw trace program_stdoutw′
Hwf :
Hnd :
NoDupmapregistration_token program_pendingw
⊢
NoDupmapregistration_token program_pendingw′
–eapply puts_stream_prefix_wf ; eauto
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
xs :
listword
s :
R.state
m :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
He :
E.effectscontract_sourcesprogram_putsrep requests xs m w contract_writesprogram_putsrep requests xs m w contract_releasesprogram_putsrep requests xs m w contract_requestsprogram_putsrep requests xs m w s m [ ] s′ m′ born
Hp :
puts_prefixrep xs m program_stdiow born trace m′ program_stdiow′
Hpending :
Hstream :
puts_stream_prefixxs m program_stdoutw trace program_stdoutw′
Hwf :
Hnd :
NoDupmapregistration_token program_pendingw
⊢
NoDupmapregistration_token program_pendingw′
–rewrite Hpending
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
xs :
listword
s :
R.state
m :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
He :
E.effectscontract_sourcesprogram_putsrep requests xs m w contract_writesprogram_putsrep requests xs m w contract_releasesprogram_putsrep requests xs m w contract_requestsprogram_putsrep requests xs m w s m [ ] s′ m′ born
Hp :
puts_prefixrep xs m program_stdiow born trace m′ program_stdiow′
Hpending :
Hstream :
puts_stream_prefixxs m program_stdoutw trace program_stdoutw′
Hwf :
Hnd :
NoDupmapregistration_token program_pendingw
⊢
NoDupmapregistration_token program_pendingw
exact Hnd
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests xs s m w born trace s′ m′ w′ He Hp Hpending Hstream Hwf Hnd
split ; exact Hpending |
split ; exact Hstream |
split
–eapply puts_stream_prefix_wf ; eauto
–rewrite Hpending
exact Hnd
Every strengthened completion is an existing puts completion; the additional world cannot mint capabilities or escape resource checks.
∀ rep requests r args xs s m w trace ending s′ m′ w′
E.invokeprogram_putsrep requests r args xs s m w trace ending s′ m′ w′
E.invokeputs_contractrep requests r args xs s m program_stdiow trace ending s′ m′ program_stdiow′
Explore proof 4 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop r : call_result args : listarg xs : listword s : R.state m : mem w : program_world trace : listevent ending : call_end s′ : R.state m′ : mem w′ : program_world, E.invokeprogram_putsrep requests r args xs s m w trace ending s′ m′ w′ → E.invokeputs_contractrep requests r args xs s m program_stdiow trace ending s′ m′ program_stdiow′
intros rep requests r args xs s m w trace ending s′ m′ w′ H
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
H :
E.invokeprogram_putsrep requests r args xs s m w trace ending s′ m′ w′
⊢
E.invokeputs_contractrep requests r args xs s m program_stdiow trace ending s′ m′ program_stdiow′
destruct H as trace ending s′ m′ w′ born Ha Hpre _ Hp Hpost _ Hnot Hret Hexit | why trace s′ m′ w′ born Ha Hpre _ Hp Hfailure Hresource
2 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
born :
listZ
Ha :
contract_abiprogram_putsrep requests r args
Hpre :
puts_prerep xs m program_stdiow
Hp :
E.prefixprogram_putsrep requests xs s m w born trace s′ m′ w′
Hpost :
puts_postxs m program_stdiow born trace ending m′ program_stdiow′
Hnot :
∀why : reason, ending ≠ CallResourcewhy
Hret :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnsprogram_putsrep requests values ∧ Forallword_authoritycontract_sourcesprogram_putsrep requests xs m w born m′ values
Hexit :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
E.invokeputs_contractrep requests r args xs s m program_stdiow trace ending s′ m′ program_stdiow′
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
why :
trace :
listevent
s′ :
R.state
m′ :
w′ :
born :
listZ
Ha :
contract_abiprogram_putsrep requests r args
Hpre :
puts_prerep xs m program_stdiow
Hp :
E.prefixprogram_putsrep requests xs s m w born trace s′ m′ w′
Hfailure :
E.resource_failurecontract_requestsprogram_putsrep requests xs m w s′ why
Hresource :
contract_resourceprogram_putsrep requests why
⊢
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallResourcewhy s′ m′ program_stdiow′
–eapply E.invoke_normal with born := born ; eauto using program_prefix_projects
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
why :
trace :
listevent
s′ :
R.state
m′ :
w′ :
born :
listZ
Ha :
contract_abiprogram_putsrep requests r args
Hpre :
puts_prerep xs m program_stdiow
Hp :
E.prefixprogram_putsrep requests xs s m w born trace s′ m′ w′
Hfailure :
E.resource_failurecontract_requestsprogram_putsrep requests xs m w s′ why
Hresource :
contract_resourceprogram_putsrep requests why
⊢
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallResourcewhy s′ m′ program_stdiow′
–eapply E.invoke_resource with born := born ; eauto using program_prefix_projects
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests r args xs s m w trace ending s′ m′ w′ H
destruct H as trace ending s′ m′ w′ born Ha Hpre _ Hp Hpost _ Hnot Hret Hexit | why trace s′ m′ w′ born Ha Hpre _ Hp Hfailure Hresource
–eapply E.invoke_normal with born := born ; eauto using program_prefix_projects
–eapply E.invoke_resource with born := born ; eauto using program_prefix_projects
Normal and resource completions preserve the inventory and provide the same stdout continuity witness as an unfinished call observation.
∀ rep requests r args xs s m w trace ending s′ m′ w′
E.invokeprogram_putsrep requests r args xs s m w trace ending s′ m′ w′
program_pendingw′ = program_pendingw ∧ puts_stream_prefixxs m program_stdoutw trace program_stdoutw′ ∧ program_world_wfw′
Explore proof 3 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop r : call_result args : listarg xs : listword s : R.state m : mem w : program_world trace : listevent ending : call_end s′ : R.state m′ : mem w′ : program_world, E.invokeprogram_putsrep requests r args xs s m w trace ending s′ m′ w′ → program_pendingw′ = program_pendingw ∧ puts_stream_prefixxs m program_stdoutw trace program_stdoutw′ ∧ program_world_wfw′
intros rep requests r args xs s m w trace ending s′ m′ w′ H
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
H :
E.invokeprogram_putsrep requests r args xs s m w trace ending s′ m′ w′
⊢
program_pendingw′ = program_pendingw ∧ puts_stream_prefixxs m program_stdoutw trace program_stdoutw′ ∧ program_world_wfw′
destruct H
2 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
born :
listZ
H :
contract_abiprogram_putsrep requests r args
H0 :
contract_preprogram_putsrep requests xs m w
H1 :
E.prefixprogram_putsrep requests xs s m w born trace s′ m′ w′
H2 :
contract_postprogram_putsrep requests xs m w born trace ending m′ w′
H3 :
∀why : reason, ending ≠ CallResourcewhy
H4 :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnsprogram_putsrep requests values ∧ Forallword_authoritycontract_sourcesprogram_putsrep requests xs m w born m′ values
H5 :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
program_pendingw′ = program_pendingw ∧ puts_stream_prefixxs m program_stdoutw trace program_stdoutw′ ∧ program_world_wfw′
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
why :
trace :
listevent
s′ :
R.state
m′ :
w′ :
born :
listZ
H :
contract_abiprogram_putsrep requests r args
H0 :
contract_preprogram_putsrep requests xs m w
H1 :
E.prefixprogram_putsrep requests xs s m w born trace s′ m′ w′
H2 :
E.resource_failurecontract_requestsprogram_putsrep requests xs m w s′ why
H3 :
contract_resourceprogram_putsrep requests why
⊢
program_pendingw′ = program_pendingw ∧ puts_stream_prefixxs m program_stdoutw trace program_stdoutw′ ∧ program_world_wfw′
all: eapply program_prefix_continuity ; eassumption | exact proj1proj2H0
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests r args xs s m w trace ending s′ m′ w′ H
destruct H
all: eapply program_prefix_continuity ; eassumption | exact proj1proj2H0
A normal protocol execution is also a finite stream prefix, using the same actions, source memory, observations and endpoint.
Explore proof 8 tactics
Initial goal
⊢
∀xs : listword m : mem q : stream_state trace : listevent ending : call_end q′ : stream_state, puts_stream_postxs m q trace ending q′ → puts_stream_prefixxs m q trace q′
intros xs m q trace ending q′ p & bytes & actions & result & Hx & Hstr & Ho Hrun tail Hb Hr & Htrace & Hend
xs :
listword
m :
q :
trace :
listevent
ending :
q′ :
p :
bytes :
listZ
actions :
liststream_action
result :
Z
Hx :
xs = WPtrp
Hstr :
c_stringm p bytes
Ho :
Hrun :
stream_runq actions q′
tail :
listZ
Hb :
bytes ++ 10 = acceptedactions ++ tail
Hr :
tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1
Htrace :
trace = puts_observationactions
Hend :
ending = CallReturnWIntresult
⊢
puts_stream_prefixxs m q trace q′
exists p, bytes, actions, tail
xs :
listword
m :
q :
trace :
listevent
ending :
q′ :
p :
bytes :
listZ
actions :
liststream_action
result :
Z
Hx :
xs = WPtrp
Hstr :
c_stringm p bytes
Ho :
Hrun :
stream_runq actions q′
tail :
listZ
Hb :
bytes ++ 10 = acceptedactions ++ tail
Hr :
tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1
Htrace :
trace = puts_observationactions
Hend :
ending = CallReturnWIntresult
⊢
xs = WPtrp ∧ c_stringm p bytes ∧ stream_runq actions q′ ∧ bytes ++ 10 = acceptedactions ++ tail ∧ prefix_observationtrace actions
split ; exact Hx |
xs :
listword
m :
q :
trace :
listevent
ending :
q′ :
p :
bytes :
listZ
actions :
liststream_action
result :
Z
Hx :
xs = WPtrp
Hstr :
c_stringm p bytes
Ho :
Hrun :
stream_runq actions q′
tail :
listZ
Hb :
bytes ++ 10 = acceptedactions ++ tail
Hr :
tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1
Htrace :
trace = puts_observationactions
Hend :
ending = CallReturnWIntresult
⊢
c_stringm p bytes ∧ stream_runq actions q′ ∧ bytes ++ 10 = acceptedactions ++ tail ∧ prefix_observationtrace actions
split ; exact Hstr |
xs :
listword
m :
q :
trace :
listevent
ending :
q′ :
p :
bytes :
listZ
actions :
liststream_action
result :
Z
Hx :
xs = WPtrp
Hstr :
c_stringm p bytes
Ho :
Hrun :
stream_runq actions q′
tail :
listZ
Hb :
bytes ++ 10 = acceptedactions ++ tail
Hr :
tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1
Htrace :
trace = puts_observationactions
Hend :
ending = CallReturnWIntresult
⊢
stream_runq actions q′ ∧ bytes ++ 10 = acceptedactions ++ tail ∧ prefix_observationtrace actions
split ; exact Hrun |
xs :
listword
m :
q :
trace :
listevent
ending :
q′ :
p :
bytes :
listZ
actions :
liststream_action
result :
Z
Hx :
xs = WPtrp
Hstr :
c_stringm p bytes
Ho :
Hrun :
stream_runq actions q′
tail :
listZ
Hb :
bytes ++ 10 = acceptedactions ++ tail
Hr :
tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1
Htrace :
trace = puts_observationactions
Hend :
ending = CallReturnWIntresult
⊢
bytes ++ 10 = acceptedactions ++ tail ∧ prefix_observationtrace actions
split ; exact Hb |
xs :
listword
m :
q :
trace :
listevent
ending :
q′ :
p :
bytes :
listZ
actions :
liststream_action
result :
Z
Hx :
xs = WPtrp
Hstr :
c_stringm p bytes
Ho :
Hrun :
stream_runq actions q′
tail :
listZ
Hb :
bytes ++ 10 = acceptedactions ++ tail
Hr :
tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1
Htrace :
trace = puts_observationactions
Hend :
ending = CallReturnWIntresult
⊢
prefix_observationtrace actions
right
xs :
listword
m :
q :
trace :
listevent
ending :
q′ :
p :
bytes :
listZ
actions :
liststream_action
result :
Z
Hx :
xs = WPtrp
Hstr :
c_stringm p bytes
Ho :
Hrun :
stream_runq actions q′
tail :
listZ
Hb :
bytes ++ 10 = acceptedactions ++ tail
Hr :
tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1
Htrace :
trace = puts_observationactions
Hend :
ending = CallReturnWIntresult
⊢
trace = puts_observationactions
exact Htrace
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros xs m q trace ending q′ p & bytes & actions & result & Hx & Hstr & Ho Hrun tail Hb Hr & Htrace & Hend
exists p, bytes, actions, tail
split ; exact Hx |
split ; exact Hstr |
split ; exact Hrun |
split ; exact Hb |
right
exact Htrace
Existing memory/effect evidence can be enriched by an explicit protocol witness; this does not conjure a native puts execution from stream actions.
∀ rep requests r args xs s m w trace values s′ m′ w′
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
E.invokeprogram_putsrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
Explore proof 10 tactics
Initial goal
⊢
∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop r : call_result args : listarg xs : listword s : R.state m : mem w : program_world trace : listevent values : listword s′ : R.state m′ : mem w′ : program_world, E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′ → program_world_wfw → orientationprogram_stdoutw ≠ WideOriented → program_pendingw′ = program_pendingw → puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′ → E.invokeprogram_putsrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
intros rep requests r args xs s m w trace values s′ m′ w′ H Hwf Ho Hpending Hstream
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
⊢
E.invokeprogram_putsrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
inversion H ; subst
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
born :
listZ
H0 :
contract_abiputs_contractrep requests r args
H1 :
contract_preputs_contractrep requests xs m program_stdiow
H2 :
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
H3 :
contract_postputs_contractrep requests xs m program_stdiow born trace CallReturnvalues m′ program_stdiow′
H4 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H5 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m program_stdiow born m′ values0
H6 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
E.invokeprogram_putsrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
eapply E.invoke_normal ; eassumption | | | | eassumption | eassumption | eassumption
3 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
born :
listZ
H0 :
contract_abiputs_contractrep requests r args
H1 :
contract_preputs_contractrep requests xs m program_stdiow
H2 :
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
H3 :
contract_postputs_contractrep requests xs m program_stdiow born trace CallReturnvalues m′ program_stdiow′
H4 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H5 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m program_stdiow born m′ values0
H6 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
contract_preprogram_putsrep requests xs m w
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
born :
listZ
H0 :
contract_abiputs_contractrep requests r args
H1 :
contract_preputs_contractrep requests xs m program_stdiow
H2 :
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
H3 :
contract_postputs_contractrep requests xs m program_stdiow born trace CallReturnvalues m′ program_stdiow′
H4 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H5 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m program_stdiow born m′ values0
H6 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
E.prefixprogram_putsrep requests xs s m w born trace s′ m′ w′
focused goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
born :
listZ
H0 :
contract_abiputs_contractrep requests r args
H1 :
contract_preputs_contractrep requests xs m program_stdiow
H2 :
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
H3 :
contract_postputs_contractrep requests xs m program_stdiow born trace CallReturnvalues m′ program_stdiow′
H4 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H5 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m program_stdiow born m′ values0
H6 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
contract_postprogram_putsrep requests xs m w born trace CallReturnvalues m′ w′
–split ; eassumption |
3 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
born :
listZ
H0 :
contract_abiputs_contractrep requests r args
H1 :
contract_preputs_contractrep requests xs m program_stdiow
H2 :
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
H3 :
contract_postputs_contractrep requests xs m program_stdiow born trace CallReturnvalues m′ program_stdiow′
H4 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H5 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m program_stdiow born m′ values0
H6 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
born :
listZ
H0 :
contract_abiputs_contractrep requests r args
H1 :
contract_preputs_contractrep requests xs m program_stdiow
H2 :
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
H3 :
contract_postputs_contractrep requests xs m program_stdiow born trace CallReturnvalues m′ program_stdiow′
H4 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H5 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m program_stdiow born m′ values0
H6 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
E.prefixprogram_putsrep requests xs s m w born trace s′ m′ w′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
born :
listZ
H0 :
contract_abiputs_contractrep requests r args
H1 :
contract_preputs_contractrep requests xs m program_stdiow
H2 :
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
H3 :
contract_postputs_contractrep requests xs m program_stdiow born trace CallReturnvalues m′ program_stdiow′
H4 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H5 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m program_stdiow born m′ values0
H6 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
contract_postprogram_putsrep requests xs m w born trace CallReturnvalues m′ w′
auto
2 opendeferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
born :
listZ
H0 :
contract_abiputs_contractrep requests r args
H1 :
contract_preputs_contractrep requests xs m program_stdiow
H2 :
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
H3 :
contract_postputs_contractrep requests xs m program_stdiow born trace CallReturnvalues m′ program_stdiow′
H4 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H5 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m program_stdiow born m′ values0
H6 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
E.prefixprogram_putsrep requests xs s m w born trace s′ m′ w′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
born :
listZ
H0 :
contract_abiputs_contractrep requests r args
H1 :
contract_preputs_contractrep requests xs m program_stdiow
H2 :
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
H3 :
contract_postputs_contractrep requests xs m program_stdiow born trace CallReturnvalues m′ program_stdiow′
H4 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H5 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m program_stdiow born m′ values0
H6 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
contract_postprogram_putsrep requests xs m w born trace CallReturnvalues m′ w′
–split ; exact proj1H2 |
2 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
born :
listZ
H0 :
contract_abiputs_contractrep requests r args
H1 :
contract_preputs_contractrep requests xs m program_stdiow
H2 :
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
H3 :
contract_postputs_contractrep requests xs m program_stdiow born trace CallReturnvalues m′ program_stdiow′
H4 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H5 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m program_stdiow born m′ values0
H6 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
contract_prefixprogram_putsrep requests xs m w born trace m′ w′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
born :
listZ
H0 :
contract_abiputs_contractrep requests r args
H1 :
contract_preputs_contractrep requests xs m program_stdiow
H2 :
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
H3 :
contract_postputs_contractrep requests xs m program_stdiow born trace CallReturnvalues m′ program_stdiow′
H4 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H5 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m program_stdiow born m′ values0
H6 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
contract_postprogram_putsrep requests xs m w born trace CallReturnvalues m′ w′
split ; exact proj2H2 |
2 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
born :
listZ
H0 :
contract_abiputs_contractrep requests r args
H1 :
contract_preputs_contractrep requests xs m program_stdiow
H2 :
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
H3 :
contract_postputs_contractrep requests xs m program_stdiow born trace CallReturnvalues m′ program_stdiow′
H4 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H5 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m program_stdiow born m′ values0
H6 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
program_pendingw′ = program_pendingw ∧ puts_stream_prefixxs m program_stdoutw trace program_stdoutw′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
born :
listZ
H0 :
contract_abiputs_contractrep requests r args
H1 :
contract_preputs_contractrep requests xs m program_stdiow
H2 :
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
H3 :
contract_postputs_contractrep requests xs m program_stdiow born trace CallReturnvalues m′ program_stdiow′
H4 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H5 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m program_stdiow born m′ values0
H6 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
contract_postprogram_putsrep requests xs m w born trace CallReturnvalues m′ w′
split ; exact Hpending |
2 openrep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
born :
listZ
H0 :
contract_abiputs_contractrep requests r args
H1 :
contract_preputs_contractrep requests xs m program_stdiow
H2 :
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
H3 :
contract_postputs_contractrep requests xs m program_stdiow born trace CallReturnvalues m′ program_stdiow′
H4 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H5 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m program_stdiow born m′ values0
H6 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
puts_stream_prefixxs m program_stdoutw trace program_stdoutw′
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
born :
listZ
H0 :
contract_abiputs_contractrep requests r args
H1 :
contract_preputs_contractrep requests xs m program_stdiow
H2 :
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
H3 :
contract_postputs_contractrep requests xs m program_stdiow born trace CallReturnvalues m′ program_stdiow′
H4 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H5 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m program_stdiow born m′ values0
H6 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
contract_postprogram_putsrep requests xs m w born trace CallReturnvalues m′ w′
eapply program_post_prefix ; eauto
deferred goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeputs_contractrep requests r args xs s m program_stdiow trace CallReturnvalues s′ m′ program_stdiow′
Hwf :
Hpending :
Hstream :
puts_stream_postxs m program_stdoutw trace CallReturnvalues program_stdoutw′
born :
listZ
H0 :
contract_abiputs_contractrep requests r args
H1 :
contract_preputs_contractrep requests xs m program_stdiow
H2 :
E.prefixputs_contractrep requests xs s m program_stdiow born trace s′ m′ program_stdiow′
H3 :
contract_postputs_contractrep requests xs m program_stdiow born trace CallReturnvalues m′ program_stdiow′
H4 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H5 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m program_stdiow born m′ values0
H6 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
contract_postprogram_putsrep requests xs m w born trace CallReturnvalues m′ w′
–split ; eassumption
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests r args xs s m w trace values s′ m′ w′ H Hwf Ho Hpending Hstream
inversion H ; subst
eapply E.invoke_normal ; eassumption | | | | eassumption | eassumption | eassumption
–split ; eassumption |
auto
–split ; exact proj1H2 |
split ; exact proj2H2 |
split ; exact Hpending |
eapply program_post_prefix ; eauto
–split ; eassumption
Inhabited protocol boundaries, not native coverage
The same real main literal and libc root as the body checks, with one actual registration instance retained across puts.
This entry inventory has distinct tokens and the initial stdout is ready.
Explore proof 2 tactics
Initial goal
split ; exact stdout_initial_wf |
repeat constructor ; simpl ; tauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; exact stdout_initial_wf |
repeat constructor ; simpl ; tauto
A returning EOF can leave exactly its accepted prefix outstanding.
∀ acc tail
hello_bytes ++ 10 = acc ++ tail
Forallλb ⇒ 0 ≤ b < 256 acc
Proof 58 steps Qed
intros acc tail Hb Hbytes
destruct HiChecks.entry_pre as Hr Hw Hl
pose proof C.H.hi_literal_checkedHiChecks.memory Hl as Hstr
apply C.program_return_lift
–eapply C.E.invoke_normal with born := [ ]
+split ; constructor |
split ; exact Hr |
split ; exact Hw |
split
∗apply stdio_delegates_refl ; reflexivity | exact proj2Hw
+exists hi_literal, hello_bytes, acc, tail, 2 ^ 32 − 1
split ; reflexivity |
split ; exact Hstr |
split ; exact Hb |
split ; right ; reflexivity |
split ; reflexivity |
split ; reflexivity | exact Hw
+intros why Hbad
discriminate
+intros values Heq
injection Heq as ←
split
∗exists WInt2 ^ 32 − 1
split ; reflexivity
∗constructor ; exact I | constructor
+intros status Hbad
discriminate
–exact initial_world_wf
–discriminate
–reflexivity
–exists hi_literal, hello_bytes, Acceptacc, 2 ^ 32 − 1
split ; reflexivity |
split
exact proj2proj2HiChecks.entry_pre
+split
∗split ; discriminate |
split
--eapply stream_next ; apply stream_accept ; discriminate | exact Hbytes | constructor
--exists tail
split ; simpl ; rewrite app_nil_r ; exact Hb |
right
reflexivity
Partial acceptance is not dropped or replaced by an unrelated shutdown state.
263Example partial_eof_keeps_exact_output: C.E.invokeprogram_putsfixture_rep fixture_requests site_resulthi_site site_argshi_site WPtrhi_literal InterpRuntime.start HiChecks.memory worldstdout_initial StreamBytes1 104; 101 CallReturnWInt2 ^ 32 − 1 InterpRuntime.start HiChecks.memory worldmkStreamByteOriented 104; 101 false
Explore proof 1 tactics
Initial goal
⊢
C.E.invokeprogram_putsfixture_rep fixture_requests site_resulthi_site site_argshi_site WPtrhi_literal InterpRuntime.start HiChecks.memory worldstdout_initial StreamBytes1 104; 101 CallReturnWInt2 ^ 32 − 1 InterpRuntime.start HiChecks.memory worldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
apply eof_buffered_ 108; 108; 111; 10 ; reflexivity | repeat constructor ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
apply eof_buffered_ 108; 108; 111; 10 ; reflexivity | repeat constructor ; lia
EOF permits both no acceptance and acceptance of the complete newline.
272Example eof_empty_and_full: ∃w′, C.E.invokeprogram_putsfixture_rep fixture_requests site_resulthi_site site_argshi_site WPtrhi_literal InterpRuntime.start HiChecks.memory worldstdout_initial StreamBytes1 [ ] CallReturnWInt2 ^ 32 − 1 InterpRuntime.start HiChecks.memory w′ ∧ ∃w′, C.E.invokeprogram_putsfixture_rep fixture_requests site_resulthi_site site_argshi_site WPtrhi_literal InterpRuntime.start HiChecks.memory worldstdout_initial StreamBytes1 hello_bytes ++ 10 CallReturnWInt2 ^ 32 − 1 InterpRuntime.start HiChecks.memory w′
Explore proof 3 tactics
Initial goal
⊢
∃w′ : program_world, C.E.invokeprogram_putsfixture_rep fixture_requests site_resulthi_site site_argshi_site WPtrhi_literal InterpRuntime.start HiChecks.memory worldstdout_initial StreamBytes1 [ ] CallReturnWInt2 ^ 32 − 1 InterpRuntime.start HiChecks.memory w′ ∧ ∃w′ : program_world, C.E.invokeprogram_putsfixture_rep fixture_requests site_resulthi_site site_argshi_site WPtrhi_literal InterpRuntime.start HiChecks.memory worldstdout_initial StreamBytes1 hello_bytes ++ 10 CallReturnWInt2 ^ 32 − 1 InterpRuntime.start HiChecks.memory w′
split ; eexists
4 openfocused goal
shelved goal
shelved goal
–apply eof_buffered_ hello_bytes ++ 10 ; reflexivity | constructor
2 opendeferred goal
shelved goal
–apply eof_buffered_ [ ] ; reflexivity | repeat constructor ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; eexists
–apply eof_buffered_ hello_bytes ++ 10 ; reflexivity | constructor
–apply eof_buffered_ [ ] ; reflexivity | repeat constructor ; lia
Oversize refusal remains a resource outcome, not a normal puts result.
align = 16 ∧ size = 2 ^ 48
This is an actual completed resource invocation AFTER partial acceptance. It retains output and the registration list without invoking normal exit.
293Example resource_after_partial_acceptance: C.E.invokeprogram_putsfixture_rep big_requests site_resulthi_site site_argshi_site WPtrhi_literal InterpRuntime.start HiChecks.memory worldstdout_initial StreamBytes1 104; 101 CallResourceTooBig InterpRuntime.start HiChecks.memory worldmkStreamByteOriented 104; 101 false
Explore proof 37 tactics
Initial goal
⊢
C.E.invokeprogram_putsfixture_rep big_requests site_resulthi_site site_argshi_site WPtrhi_literal InterpRuntime.start HiChecks.memory worldstdout_initial StreamBytes1 104; 101 CallResourceTooBig InterpRuntime.start HiChecks.memory worldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
destruct HiChecks.entry_pre as Hr Hw Hl
⊢
C.E.invokeprogram_putsfixture_rep big_requests site_resulthi_site site_argshi_site WPtrhi_literal InterpRuntime.start HiChecks.memory worldstdout_initial StreamBytes1 104; 101 CallResourceTooBig InterpRuntime.start HiChecks.memory worldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
pose proof C.H.hi_literal_checkedHiChecks.memory Hl as Hstr
⊢
C.E.invokeprogram_putsfixture_rep big_requests site_resulthi_site site_argshi_site WPtrhi_literal InterpRuntime.start HiChecks.memory worldstdout_initial StreamBytes1 104; 101 CallResourceTooBig InterpRuntime.start HiChecks.memory worldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
eapply C.E.invoke_resource with born := [ ]
5 openfocused goal
focused goal
focused goal
–split ; right ; exists TAtom"v1" ; reflexivity |
5 opendeferred goal
deferred goal
deferred goal
exists TmpTAtom"v0"
5 opendeferred goal
deferred goal
deferred goal
reflexivity
4 opendeferred goal
deferred goal
deferred goal
–split
5 openfocused goal
deferred goal
deferred goal
+split ; exact Hr |
5 open⊢
stdio_readyHiChecks.memory program_stdioworldstdout_initial ∧ ∃p : ptr bytes : listZ, WPtrhi_literal = WPtrp ∧ c_stringHiChecks.memory p bytes
deferred goal
deferred goal
deferred goal
split ; exact Hw |
5 open⊢
∃p : ptr bytes : listZ, WPtrhi_literal = WPtrp ∧ c_stringHiChecks.memory p bytes
deferred goal
deferred goal
deferred goal
exists hi_literal, hello_bytes
5 opendeferred goal
deferred goal
deferred goal
auto
4 opendeferred goal
deferred goal
deferred goal
+split ; exact initial_world_wf | discriminate
3 opendeferred goal
deferred goal
–split ; constructor |
3 open⊢
contract_prefixprogram_putsfixture_rep big_requests WPtrhi_literal HiChecks.memory worldstdout_initial [ ] StreamBytes1 104; 101 HiChecks.memory worldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
deferred goal
split
4 open⊢
puts_prefixfixture_rep WPtrhi_literal HiChecks.memory program_stdioworldstdout_initial [ ] StreamBytes1 104; 101 HiChecks.memory program_stdioworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
focused goal
⊢
program_pendingworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false = program_pendingworldstdout_initial ∧ puts_stream_prefixWPtrhi_literal HiChecks.memory program_stdoutworldstdout_initial StreamBytes1 104; 101 program_stdoutworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
deferred goal
+split ; exact Hr |
4 open⊢
stdio_readyHiChecks.memory program_stdioworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false ∧ stdio_delegatesstdio_rootsprogram_stdioworldstdout_initial [ ] HiChecks.memory program_stdioworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false ∧ StreamBytes1 104; 101 = [ ] ∨ ∃p : ptr bytes accepted tail : listZ, WPtrhi_literal = WPtrp ∧ c_stringHiChecks.memory p bytes ∧ bytes ++ 10 = accepted ++ tail ∧ StreamBytes1 104; 101 = StreamBytes1 accepted
deferred goal
⊢
program_pendingworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false = program_pendingworldstdout_initial ∧ puts_stream_prefixWPtrhi_literal HiChecks.memory program_stdoutworldstdout_initial StreamBytes1 104; 101 program_stdoutworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
deferred goal
split ; exact Hw |
4 open⊢
stdio_delegatesstdio_rootsprogram_stdioworldstdout_initial [ ] HiChecks.memory program_stdioworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false ∧ StreamBytes1 104; 101 = [ ] ∨ ∃p : ptr bytes accepted tail : listZ, WPtrhi_literal = WPtrp ∧ c_stringHiChecks.memory p bytes ∧ bytes ++ 10 = accepted ++ tail ∧ StreamBytes1 104; 101 = StreamBytes1 accepted
deferred goal
⊢
program_pendingworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false = program_pendingworldstdout_initial ∧ puts_stream_prefixWPtrhi_literal HiChecks.memory program_stdoutworldstdout_initial StreamBytes1 104; 101 program_stdoutworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
deferred goal
split
5 openfocused goal
⊢
StreamBytes1 104; 101 = [ ] ∨ ∃p : ptr bytes accepted tail : listZ, WPtrhi_literal = WPtrp ∧ c_stringHiChecks.memory p bytes ∧ bytes ++ 10 = accepted ++ tail ∧ StreamBytes1 104; 101 = StreamBytes1 accepted
deferred goal
⊢
program_pendingworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false = program_pendingworldstdout_initial ∧ puts_stream_prefixWPtrhi_literal HiChecks.memory program_stdoutworldstdout_initial StreamBytes1 104; 101 program_stdoutworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
deferred goal
∗apply stdio_delegates_refl ; reflexivity | exact proj2Hw
4 opendeferred goal
⊢
StreamBytes1 104; 101 = [ ] ∨ ∃p : ptr bytes accepted tail : listZ, WPtrhi_literal = WPtrp ∧ c_stringHiChecks.memory p bytes ∧ bytes ++ 10 = accepted ++ tail ∧ StreamBytes1 104; 101 = StreamBytes1 accepted
deferred goal
⊢
program_pendingworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false = program_pendingworldstdout_initial ∧ puts_stream_prefixWPtrhi_literal HiChecks.memory program_stdoutworldstdout_initial StreamBytes1 104; 101 program_stdoutworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
deferred goal
∗right
4 open⊢
∃p : ptr bytes accepted tail : listZ, WPtrhi_literal = WPtrp ∧ c_stringHiChecks.memory p bytes ∧ bytes ++ 10 = accepted ++ tail ∧ StreamBytes1 104; 101 = StreamBytes1 accepted
deferred goal
⊢
program_pendingworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false = program_pendingworldstdout_initial ∧ puts_stream_prefixWPtrhi_literal HiChecks.memory program_stdoutworldstdout_initial StreamBytes1 104; 101 program_stdoutworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
deferred goal
exists hi_literal, hello_bytes, 104; 101, 108; 108; 111; 10
4 open⊢
WPtrhi_literal = WPtrhi_literal ∧ c_stringHiChecks.memory hi_literal hello_bytes ∧ hello_bytes ++ 10 = 104; 101 ++ 108; 108; 111; 10 ∧ StreamBytes1 104; 101 = StreamBytes1 104; 101
deferred goal
⊢
program_pendingworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false = program_pendingworldstdout_initial ∧ puts_stream_prefixWPtrhi_literal HiChecks.memory program_stdoutworldstdout_initial StreamBytes1 104; 101 program_stdoutworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
deferred goal
split ; reflexivity |
4 open⊢
c_stringHiChecks.memory hi_literal hello_bytes ∧ hello_bytes ++ 10 = 104; 101 ++ 108; 108; 111; 10 ∧ StreamBytes1 104; 101 = StreamBytes1 104; 101
deferred goal
⊢
program_pendingworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false = program_pendingworldstdout_initial ∧ puts_stream_prefixWPtrhi_literal HiChecks.memory program_stdoutworldstdout_initial StreamBytes1 104; 101 program_stdoutworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
deferred goal
split ; exact Hstr |
4 open⊢
hello_bytes ++ 10 = 104; 101 ++ 108; 108; 111; 10 ∧ StreamBytes1 104; 101 = StreamBytes1 104; 101
deferred goal
⊢
program_pendingworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false = program_pendingworldstdout_initial ∧ puts_stream_prefixWPtrhi_literal HiChecks.memory program_stdoutworldstdout_initial StreamBytes1 104; 101 program_stdoutworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
deferred goal
split ; reflexivity
3 opendeferred goal
⊢
program_pendingworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false = program_pendingworldstdout_initial ∧ puts_stream_prefixWPtrhi_literal HiChecks.memory program_stdoutworldstdout_initial StreamBytes1 104; 101 program_stdoutworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
deferred goal
+split ; reflexivity |
3 open⊢
puts_stream_prefixWPtrhi_literal HiChecks.memory program_stdoutworldstdout_initial StreamBytes1 104; 101 program_stdoutworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
deferred goal
exists hi_literal, hello_bytes, Accept104; 101, 108; 108; 111; 10
3 open⊢
WPtrhi_literal = WPtrhi_literal ∧ c_stringHiChecks.memory hi_literal hello_bytes ∧ stream_runprogram_stdoutworldstdout_initial Accept104; 101 program_stdoutworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false ∧ hello_bytes ++ 10 = acceptedAccept104; 101 ++ 108; 108; 111; 10 ∧ prefix_observationStreamBytes1 104; 101 Accept104; 101
deferred goal
split ; reflexivity |
3 open⊢
c_stringHiChecks.memory hi_literal hello_bytes ∧ stream_runprogram_stdoutworldstdout_initial Accept104; 101 program_stdoutworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false ∧ hello_bytes ++ 10 = acceptedAccept104; 101 ++ 108; 108; 111; 10 ∧ prefix_observationStreamBytes1 104; 101 Accept104; 101
deferred goal
split ; exact Hstr |
3 open⊢
stream_runprogram_stdoutworldstdout_initial Accept104; 101 program_stdoutworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false ∧ hello_bytes ++ 10 = acceptedAccept104; 101 ++ 108; 108; 111; 10 ∧ prefix_observationStreamBytes1 104; 101 Accept104; 101
deferred goal
split
4 open⊢
stream_runprogram_stdoutworldstdout_initial Accept104; 101 program_stdoutworldorientation ≔ ByteOriented; outstanding ≔ 104; 101; stream_error ≔ false
focused goal
⊢
hello_bytes ++ 10 = acceptedAccept104; 101 ++ 108; 108; 111; 10 ∧ prefix_observationStreamBytes1 104; 101 Accept104; 101
deferred goal
∗eapply stream_next ; apply stream_accept ; discriminate | repeat constructor ; lia | constructor
3 opendeferred goal
⊢
hello_bytes ++ 10 = acceptedAccept104; 101 ++ 108; 108; 111; 10 ∧ prefix_observationStreamBytes1 104; 101 Accept104; 101
deferred goal
∗split ; reflexivity |
3 open⊢
prefix_observationStreamBytes1 104; 101 Accept104; 101
deferred goal
right
3 open⊢
StreamBytes1 104; 101 = puts_observationAccept104; 101
deferred goal
reflexivity
2 opendeferred goal
–apply C.E.failure_big with align := 16 size := 2 ^ 48 ; split ; reflexivity |
2 open⊢
max_allocation_size < 2 ^ 48
unfold max_allocation_size
2 open⊢
2 ^ 48 − 1 < 2 ^ 48
lia
–right
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
destruct HiChecks.entry_pre as Hr Hw Hl
pose proof C.H.hi_literal_checkedHiChecks.memory Hl as Hstr
eapply C.E.invoke_resource with born := [ ]
–split
+split ; exact initial_world_wf | discriminate
–split ; constructor |
split
+split ; exact Hr |
split ; exact Hw |
split
∗apply stdio_delegates_refl ; reflexivity | exact proj2Hw
∗right
exists hi_literal, hello_bytes, 104; 101, 108; 108; 111; 10
split ; reflexivity |
split ; exact Hstr |
split ; reflexivity
+split ; reflexivity |
exists hi_literal, hello_bytes, Accept104; 101, 108; 108; 111; 10
split ; reflexivity |
split ; exact Hstr |
split
∗eapply stream_next ; apply stream_accept ; discriminate | repeat constructor ; lia | constructor
∗split ; reflexivity |
right
reflexivity
–apply C.E.failure_big with align := 16 size := 2 ^ 48 ; split ; reflexivity |
unfold max_allocation_size
lia
–right
reflexivity
Empty observations can deliver OLD pending bytes without new acceptance.
322Example silent_prefix_can_deliver: puts_stream_prefixWPtrhi_literal HiChecks.memory mkStreamByteOriented 65; 66 false [ ] mkStreamByteOriented [ ] false
Explore proof 10 tactics
Initial goal
⊢
puts_stream_prefixWPtrhi_literal HiChecks.memory orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false [ ] orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false
exists hi_literal, hello_bytes, Deliver65; 66, hello_bytes ++ 10
⊢
WPtrhi_literal = WPtrhi_literal ∧ c_stringHiChecks.memory hi_literal hello_bytes ∧ stream_runorientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false ∧ hello_bytes ++ 10 = acceptedDeliver65; 66 ++ hello_bytes ++ 10 ∧ prefix_observation[ ] Deliver65; 66
split ; reflexivity |
⊢
c_stringHiChecks.memory hi_literal hello_bytes ∧ stream_runorientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false ∧ hello_bytes ++ 10 = acceptedDeliver65; 66 ++ hello_bytes ++ 10 ∧ prefix_observation[ ] Deliver65; 66
split
2 openfocused goal
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false ∧ hello_bytes ++ 10 = acceptedDeliver65; 66 ++ hello_bytes ++ 10 ∧ prefix_observation[ ] Deliver65; 66
–apply HiChecks.H.hi_literal_checked
2 opendeferred goal
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false ∧ hello_bytes ++ 10 = acceptedDeliver65; 66 ++ hello_bytes ++ 10 ∧ prefix_observation[ ] Deliver65; 66
exact proj2proj2HiChecks.entry_pre
deferred goal
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false ∧ hello_bytes ++ 10 = acceptedDeliver65; 66 ++ hello_bytes ++ 10 ∧ prefix_observation[ ] Deliver65; 66
–split
2 open⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false Deliver65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ false
focused goal
⊢
hello_bytes ++ 10 = acceptedDeliver65; 66 ++ hello_bytes ++ 10 ∧ prefix_observation[ ] Deliver65; 66
+eapply stream_next ; apply stream_deliver65; 66 [ ] false ; discriminate | constructor
deferred goal
⊢
hello_bytes ++ 10 = acceptedDeliver65; 66 ++ hello_bytes ++ 10 ∧ prefix_observation[ ] Deliver65; 66
+split ; reflexivity |
⊢
prefix_observation[ ] Deliver65; 66
left
split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
exists hi_literal, hello_bytes, Deliver65; 66, hello_bytes ++ 10
split ; reflexivity |
split
exact proj2proj2HiChecks.entry_pre
–split
+eapply stream_next ; apply stream_deliver65; 66 [ ] false ; discriminate | constructor
+split ; reflexivity |
left
split ; reflexivity
A silent summary cannot hide any newly accepted bytes.
Explore proof 1 tactics
Initial goal
⊢
¬prefix_observation[ ] Accept104
intros _ Hb | Ht ; discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros _ Hb | Ht ; discriminate
Changing the inventory violates the strengthened prefix even if all memory and byte observations could satisfy the ordinary contract.
340Example inventory_mutation_rejected: ∀born trace m′ q, ¬contract_prefixprogram_putsfixture_rep fixture_requests WPtrhi_literal HiChecks.memory worldstdout_initial born trace m′ mkProgramWorldhello_world q [ ]
Explore proof 2 tactics
Initial goal
⊢
∀born : listZ trace : listevent m′ : mem q : stream_state, ¬contract_prefixprogram_putsfixture_rep fixture_requests WPtrhi_literal HiChecks.memory worldstdout_initial born trace m′ program_stdio ≔ hello_world; program_stdout ≔ q; program_pending ≔ [ ]
intros born trace m′ q _ Hpending _
⊢
False
discriminate Hpending
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros born trace m′ q _ Hpending _
discriminate Hpending
A wide-oriented stream cannot enter this strengthened contract, even EOF.
347Example wide_entry_rejected: ¬contract_preprogram_putsfixture_rep fixture_requests WPtrhi_literal HiChecks.memory worldmkStreamWideOriented [ ] false
Explore proof 3 tactics
Initial goal
intros _ _ Hwide
Hwide :
orientationprogram_stdoutworldorientation ≔ WideOriented; outstanding ≔ [ ]; stream_error ≔ false ≠ WideOriented
⊢
False
apply Hwide
Hwide :
orientationprogram_stdoutworldorientation ≔ WideOriented; outstanding ≔ [ ]; stream_error ≔ false ≠ WideOriented
⊢
orientationprogram_stdoutworldorientation ≔ WideOriented; outstanding ≔ [ ]; stream_error ≔ false = WideOriented
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros _ _ Hwide
apply Hwide
reflexivity
Endpoint equality does not identify a unique delivery history: when error is already set, delivery and error-discard can end identically.
354Example histories_not_unique: stream_runmkStreamByteOriented 65 true Deliver65 mkStreamByteOriented [ ] true ∧ stream_runmkStreamByteOriented 65 true Discard65 mkStreamByteOriented [ ] true
Explore proof 1 tactics
Initial goal
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ true Deliver65 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_runorientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ true Discard65 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
split ; eapply stream_next ; apply stream_deliver65 [ ] true ; discriminate | constructor | apply stream_discard65 [ ] true ; discriminate | constructor
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; eapply stream_next ; apply stream_deliver65 [ ] true ; discriminate | constructor | apply stream_discard65 [ ] true ; discriminate | constructor