rocq/theories/Stdio.v
A logical stdout protocol, not a native FILE representation (milestone 3b).
Accepted bytes become ordered output obligations. Delivery and error-induced discard settle exact prefixes, preserving their interleaving. Outstanding obligations are NOT physical buffer contents: a direct-output path can accept and deliver in succession. Delivery means descriptor acceptance, not device durability. The error flag is not yet connected to native ferror.
This protocol has no memory effects or allocator. Native buffering, allocation/fallback, capability roots and shutdown require separate realization obligations. In particular, a protocol step cannot mint write authority or establish effects.
From Stdlib Require Import ZArith List Bool Lia
From Nanofil Require Import Values Memory ExternalCalls
Import ListNotations
Open Scope Z_scope
Open Scope list_scope
A C stream's orientation: not yet chosen, bytes, or wide characters. The first output fixes it.
| | | Unoriented | ||
| | | ByteOriented | ||
| | | WideOriented |
The logical state of stdout: its orientation, the outstanding output obligations (bytes accepted but not yet delivered or discarded, in order), and the sticky error flag.
| orientation | ||
| outstanding | : listZ | |
| stream_error | : bool |
A well-formed stream state q: every outstanding obligation is a byte, and a stream with any is byte-oriented.
Forallλb ⇒ 0 ≤ b < 256 outstandingq ∧ outstandingq ≠ [ ] → orientationq = ByteOriented
One protocol action: accept bytes as new obligations, deliver bytes to the descriptor, discard bytes after an output error, or record an output error that settled nothing.
| | | Accept | bytes : listZ | |
| | | Deliver | bytes : listZ | |
| | | Discard | bytes : listZ | |
| | | OutputError |
One protocol step, from state q by an action:
- accept appends bytes to the obligations of a stream that is not wide, orienting it to bytes;
- deliver and discard consume a nonempty exact prefix of the obligations, discard also setting the error flag;
- an output error only sets the error flag.
The error indicator is sticky, not a ban on later output. Discard here means output-error abandonment, not seek/purge or fclose. A zero-progress failure records an error without settling any bytes.
∀ q bytes
Forallλb ⇒ 0 ≤ b < 256 bytes
stream_accept
stream_stepq Acceptbytes mkStreamByteOriented outstandingq ++ bytes stream_errorq
∀ bytes rest err
bytes ≠ [ ]
stream_deliver
stream_stepmkStreamByteOriented bytes ++ rest err Deliverbytes mkStreamByteOriented rest err
∀ bytes rest err
bytes ≠ [ ]
stream_discard
stream_stepmkStreamByteOriented bytes ++ rest err Discardbytes mkStreamByteOriented rest true
∀ pending err
stream_stepmkStreamByteOriented pending err OutputError mkStreamByteOriented pending true
stream_output_errorA fixed action has one logical target; an exact consumed prefix fixes the remaining queue, without promising that the action occurs.
Explore proof 3 tactics
Initial goal
⊢
∀q : stream_state action : stream_action left right : stream_state, stream_stepq action left → stream_stepq action right → left = right
intros q action left right Hl Hr
⊢
left = right
inversion Hl ; subst ; inversion Hr ; subst ; try reflexivity
2 openbytes, rest :
listZ
err :
bool
Hl :
stream_steporientation ≔ ByteOriented; outstanding ≔ bytes ++ rest; stream_error ≔ err Deliverbytes orientation ≔ ByteOriented; outstanding ≔ rest; stream_error ≔ err
rest0 :
listZ
Hr :
stream_steporientation ≔ ByteOriented; outstanding ≔ bytes ++ rest; stream_error ≔ err Deliverbytes orientation ≔ ByteOriented; outstanding ≔ rest0; stream_error ≔ err
H, H4 :
bytes ≠ [ ]
H0 :
bytes ++ rest0 = bytes ++ rest
⊢
orientation ≔ ByteOriented; outstanding ≔ rest; stream_error ≔ err = orientation ≔ ByteOriented; outstanding ≔ rest0; stream_error ≔ err
focused goal
bytes, rest :
listZ
err :
bool
Hl :
stream_steporientation ≔ ByteOriented; outstanding ≔ bytes ++ rest; stream_error ≔ err Discardbytes orientation ≔ ByteOriented; outstanding ≔ rest; stream_error ≔ true
rest0 :
listZ
Hr :
stream_steporientation ≔ ByteOriented; outstanding ≔ bytes ++ rest; stream_error ≔ err Discardbytes orientation ≔ ByteOriented; outstanding ≔ rest0; stream_error ≔ true
H, H4 :
bytes ≠ [ ]
H0 :
bytes ++ rest0 = bytes ++ rest
⊢
orientation ≔ ByteOriented; outstanding ≔ rest; stream_error ≔ true = orientation ≔ ByteOriented; outstanding ≔ rest0; stream_error ≔ true
all: match goal withH : ++ = ++ |- _⇒apply app_inv_head in H ; subst ; reflexivityend
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros q action left right Hl Hr
inversion Hl ; subst ; inversion Hr ; subst ; try reflexivity
all: match goal withH : ++ = ++ |- _⇒apply app_inv_head in H ; subst ; reflexivityend
A finite sequence of stream_steps, from q by actions to q'.
∀ q
stream_runq [ ] q
stream_refl∀ q action q1 actions q′
stream_stepq action q1
stream_runq1 actions q′
stream_next
stream_runq action :: actions q′
The bytes an action accepts: an accept's, otherwise none.
match action with
_
⇒
[ ]
The bytes an action settles: a delivery's or a discard's, otherwise none.
All bytes the actions accept, in order.
flat_mapaccepted_by actions
All bytes the actions settle, delivered or discarded, in order.
flat_mapresolved_by actions
One step's accounting: the old obligations followed by what the action accepts equal what it settles followed by the new obligations.
∀ q action q′
stream_stepq action q′
outstandingq ++ accepted_byaction = resolved_byaction ++ outstandingq′
Explore proof 2 tactics
Initial goal
⊢
∀q : stream_state action : stream_action q′ : stream_state, stream_stepq action q′ → outstandingq ++ accepted_byaction = resolved_byaction ++ outstandingq′
intros q action q′ H
⊢
outstandingq ++ accepted_byaction = resolved_byaction ++ outstandingq′
destruct H ; simpl ; try reflexivity ; apply app_nil_r
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros q action q′ H
destruct H ; simpl ; try reflexivity ; apply app_nil_r
For a whole stream_run, the old obligations followed by all accepted bytes equal all resolved bytes followed by the remaining obligations. Every old or new obligation is either resolved in first-in, first-out order or still outstanding. Resolutions include BOTH delivery and abandonment; replacing them by delivery alone would promise lossless output.
∀ q actions q′
stream_runq actions q′
outstandingq ++ acceptedactions = resolvedactions ++ outstandingq′
Explore proof 9 tactics
Initial goal
⊢
∀q : stream_state actions : liststream_action q′ : stream_state, stream_runq actions q′ → outstandingq ++ acceptedactions = resolvedactions ++ outstandingq′
intros q actions q′ H
⊢
outstandingq ++ acceptedactions = resolvedactions ++ outstandingq′
induction H
2 openq :
⊢
outstandingq ++ accepted[ ] = resolved[ ] ++ outstandingq
focused goal
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
H0 :
stream_runq1 actions q′
IHstream_run :
outstandingq1 ++ acceptedactions = resolvedactions ++ outstandingq′
⊢
outstandingq ++ acceptedaction :: actions = resolvedaction :: actions ++ outstandingq′
–simpl
2 openq :
⊢
outstandingq ++ [ ] = outstandingq
deferred goal
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
H0 :
stream_runq1 actions q′
IHstream_run :
outstandingq1 ++ acceptedactions = resolvedactions ++ outstandingq′
⊢
outstandingq ++ acceptedaction :: actions = resolvedaction :: actions ++ outstandingq′
apply app_nil_r
deferred goal
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
H0 :
stream_runq1 actions q′
IHstream_run :
outstandingq1 ++ acceptedactions = resolvedactions ++ outstandingq′
⊢
outstandingq ++ acceptedaction :: actions = resolvedaction :: actions ++ outstandingq′
–unfold accepted , resolved in *
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
H0 :
stream_runq1 actions q′
IHstream_run :
outstandingq1 ++ flat_mapaccepted_by actions = flat_mapresolved_by actions ++ outstandingq′
⊢
outstandingq ++ flat_mapaccepted_by action :: actions = flat_mapresolved_by action :: actions ++ outstandingq′
simpl
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
H0 :
stream_runq1 actions q′
IHstream_run :
outstandingq1 ++ flat_mapaccepted_by actions = flat_mapresolved_by actions ++ outstandingq′
⊢
outstandingq ++ accepted_byaction ++ flat_mapaccepted_by actions = resolved_byaction ++ flat_mapresolved_by actions ++ outstandingq′
rewrite app_assoc , stream_step_accounting_ _ _ H
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
H0 :
stream_runq1 actions q′
IHstream_run :
outstandingq1 ++ flat_mapaccepted_by actions = flat_mapresolved_by actions ++ outstandingq′
⊢
resolved_byaction ++ outstandingq1 ++ flat_mapaccepted_by actions = resolved_byaction ++ flat_mapresolved_by actions ++ outstandingq′
rewrite <- app_assoc , IHstream_run , app_assoc
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
H0 :
stream_runq1 actions q′
IHstream_run :
outstandingq1 ++ flat_mapaccepted_by actions = flat_mapresolved_by actions ++ outstandingq′
⊢
resolved_byaction ++ flat_mapresolved_by actions ++ outstandingq′ = resolved_byaction ++ flat_mapresolved_by actions ++ outstandingq′
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros q actions q′ H
induction H
–simpl
apply app_nil_r
simpl
rewrite app_assoc , stream_step_accounting_ _ _ H
rewrite <- app_assoc , IHstream_run , app_assoc
reflexivity
A step keeps the stream state well formed (stream_wf).
Explore proof 8 tactics
Initial goal
⊢
∀q : stream_state action : stream_action q′ : stream_state, stream_stepq action q′ → stream_wfq → stream_wfq′
intros q action q′ H Hbytes Horient
q :
action :
q′ :
H :
stream_stepq action q′
Hbytes :
Forallλb : Z ⇒ 0 ≤ b < 256 outstandingq
Horient :
outstandingq ≠ [ ] → orientationq = ByteOriented
⊢
destruct H ; split ; simpl in * ; auto
3 openq :
bytes :
listZ
H :
H0 :
Forallλb : Z ⇒ 0 ≤ b < 256 bytes
Hbytes :
Forallλb : Z ⇒ 0 ≤ b < 256 outstandingq
Horient :
outstandingq ≠ [ ] → orientationq = ByteOriented
⊢
Forallλb : Z ⇒ 0 ≤ b < 256 outstandingq ++ bytes
focused goal
bytes, rest :
listZ
err :
bool
H :
bytes ≠ [ ]
Hbytes :
Forallλb : Z ⇒ 0 ≤ b < 256 bytes ++ rest
Horient :
bytes ++ rest ≠ [ ] → ByteOriented = ByteOriented
⊢
Forallλb : Z ⇒ 0 ≤ b < 256 rest
focused goal
bytes, rest :
listZ
err :
bool
H :
bytes ≠ [ ]
Hbytes :
Forallλb : Z ⇒ 0 ≤ b < 256 bytes ++ rest
Horient :
bytes ++ rest ≠ [ ] → ByteOriented = ByteOriented
⊢
Forallλb : Z ⇒ 0 ≤ b < 256 rest
–apply Forall_app
3 openq :
bytes :
listZ
H :
H0 :
Forallλb : Z ⇒ 0 ≤ b < 256 bytes
Hbytes :
Forallλb : Z ⇒ 0 ≤ b < 256 outstandingq
Horient :
outstandingq ≠ [ ] → orientationq = ByteOriented
⊢
Forallλb : Z ⇒ 0 ≤ b < 256 outstandingq ∧ Forallλb : Z ⇒ 0 ≤ b < 256 bytes
deferred goal
bytes, rest :
listZ
err :
bool
H :
bytes ≠ [ ]
Hbytes :
Forallλb : Z ⇒ 0 ≤ b < 256 bytes ++ rest
Horient :
bytes ++ rest ≠ [ ] → ByteOriented = ByteOriented
⊢
Forallλb : Z ⇒ 0 ≤ b < 256 rest
deferred goal
bytes, rest :
listZ
err :
bool
H :
bytes ≠ [ ]
Hbytes :
Forallλb : Z ⇒ 0 ≤ b < 256 bytes ++ rest
Horient :
bytes ++ rest ≠ [ ] → ByteOriented = ByteOriented
⊢
Forallλb : Z ⇒ 0 ≤ b < 256 rest
auto
2 opendeferred goal
bytes, rest :
listZ
err :
bool
H :
bytes ≠ [ ]
Hbytes :
Forallλb : Z ⇒ 0 ≤ b < 256 bytes ++ rest
Horient :
bytes ++ rest ≠ [ ] → ByteOriented = ByteOriented
⊢
Forallλb : Z ⇒ 0 ≤ b < 256 rest
deferred goal
bytes, rest :
listZ
err :
bool
H :
bytes ≠ [ ]
Hbytes :
Forallλb : Z ⇒ 0 ≤ b < 256 bytes ++ rest
Horient :
bytes ++ rest ≠ [ ] → ByteOriented = ByteOriented
⊢
Forallλb : Z ⇒ 0 ≤ b < 256 rest
–apply Forall_app in Hbytes
2 openbytes, rest :
listZ
err :
bool
H :
bytes ≠ [ ]
Hbytes :
Forallλb : Z ⇒ 0 ≤ b < 256 bytes ∧ Forallλb : Z ⇒ 0 ≤ b < 256 rest
Horient :
bytes ++ rest ≠ [ ] → ByteOriented = ByteOriented
⊢
Forallλb : Z ⇒ 0 ≤ b < 256 rest
deferred goal
bytes, rest :
listZ
err :
bool
H :
bytes ≠ [ ]
Hbytes :
Forallλb : Z ⇒ 0 ≤ b < 256 bytes ++ rest
Horient :
bytes ++ rest ≠ [ ] → ByteOriented = ByteOriented
⊢
Forallλb : Z ⇒ 0 ≤ b < 256 rest
tauto
deferred goal
bytes, rest :
listZ
err :
bool
H :
bytes ≠ [ ]
Hbytes :
Forallλb : Z ⇒ 0 ≤ b < 256 bytes ++ rest
Horient :
bytes ++ rest ≠ [ ] → ByteOriented = ByteOriented
⊢
Forallλb : Z ⇒ 0 ≤ b < 256 rest
–apply Forall_app in Hbytes
bytes, rest :
listZ
err :
bool
H :
bytes ≠ [ ]
Hbytes :
Forallλb : Z ⇒ 0 ≤ b < 256 bytes ∧ Forallλb : Z ⇒ 0 ≤ b < 256 rest
Horient :
bytes ++ rest ≠ [ ] → ByteOriented = ByteOriented
⊢
Forallλb : Z ⇒ 0 ≤ b < 256 rest
tauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros q action q′ H Hbytes Horient
destruct H ; split ; simpl in * ; auto
–apply Forall_app
auto
–apply Forall_app in Hbytes
tauto
–apply Forall_app in Hbytes
tauto
So does a whole run.
Explore proof 5 tactics
Initial goal
⊢
∀q : stream_state actions : liststream_action q′ : stream_state, stream_runq actions q′ → stream_wfq → stream_wfq′
intros q actions q′ H
induction H ; auto |
intros Hwf
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
H0 :
stream_runq1 actions q′
Hwf :
⊢
apply IHstream_run
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
H0 :
stream_runq1 actions q′
Hwf :
⊢
eapply stream_step_wf ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Once set, the error flag stays set through any run.
Explore proof 5 tactics
Initial goal
⊢
∀q : stream_state actions : liststream_action q′ : stream_state, stream_runq actions q′ → stream_errorq = true → stream_errorq′ = true
intros q actions q′ H
⊢
stream_errorq = true → stream_errorq′ = true
induction H ; auto
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
H0 :
stream_runq1 actions q′
IHstream_run :
stream_errorq1 = true → stream_errorq′ = true
⊢
stream_errorq = true → stream_errorq′ = true
intros Herr
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
H0 :
stream_runq1 actions q′
IHstream_run :
stream_errorq1 = true → stream_errorq′ = true
Herr :
stream_errorq = true
⊢
stream_errorq′ = true
apply IHstream_run
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
H0 :
stream_runq1 actions q′
IHstream_run :
stream_errorq1 = true → stream_errorq′ = true
Herr :
stream_errorq = true
⊢
stream_errorq1 = true
destruct H ; simpl in * ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros q actions q′ H
induction H ; auto
intros Herr
apply IHstream_run
destruct H ; simpl in * ; auto
The events of one puts call that took the actions: one cumulative StreamBytes event on stdout with all the bytes accepted, even when that is none. Delivery and discard actions remain internal observations; no descriptor-write event is added.
StreamBytes1 acceptedactions
A puts of the string bytes, from stream state q, runs the actions to q' and returns result: the stream is not wide; the actions accept a prefix of the string and its newline; and the result is a nonnegative int if all was accepted, or else EOF (2^32 - 1), which is also allowed after full acceptance.
173Definition puts_protocolbytes : listZ q : stream_state actions : liststream_action result : Z q′ : stream_state : Prop ≔
orientationq ≠ WideOriented ∧ stream_runq actions q′ ∧ ∃tail, bytes ++ 10 = acceptedactions ++ tail ∧ tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1
A puts_protocol run, given a c_string argument and a final stdio_ready world, meets puts_post with puts_observation as its trace. This proves only the existing acceptance and result postcondition. String memory and final stdio readiness are independent premises; the native representation, footprints and effects are NOT derived from this pure protocol. Nor is native execution coverage claimed.
∀ bytes q actions result q′ m p w born m′ w′
puts_postWPtrp m w born puts_observationactions CallReturnWIntresult m′ w′
Explore proof 8 tactics
Initial goal
⊢
∀bytes : listZ q : stream_state actions : liststream_action result : Z q′ : stream_state m : mem p : ptr w : stdio_world born : listZ m′ : mem w′ : stdio_world, puts_protocolbytes q actions result q′ → c_stringm p bytes → stdio_readym′ w′ → puts_postWPtrp m w born puts_observationactions CallReturnWIntresult m′ w′
intros bytes q actions result q′ m p w born m′ w′ _ & _ & tail & Hbytes & Hresult Hstr Hready
bytes :
listZ
q :
actions :
liststream_action
result :
Z
q′ :
m :
p :
w :
born :
listZ
m′ :
w′ :
tail :
listZ
Hbytes :
bytes ++ 10 = acceptedactions ++ tail
Hresult :
tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1
Hstr :
c_stringm p bytes
Hready :
stdio_readym′ w′
⊢
puts_postWPtrp m w born puts_observationactions CallReturnWIntresult m′ w′
exists p, bytes, acceptedactions, tail, result
bytes :
listZ
q :
actions :
liststream_action
result :
Z
q′ :
m :
p :
w :
born :
listZ
m′ :
w′ :
tail :
listZ
Hbytes :
bytes ++ 10 = acceptedactions ++ tail
Hresult :
tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1
Hstr :
c_stringm p bytes
Hready :
stdio_readym′ w′
⊢
WPtrp = WPtrp ∧ c_stringm p bytes ∧ bytes ++ 10 = acceptedactions ++ tail ∧ tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1 ∧ puts_observationactions = StreamBytes1 acceptedactions ∧ CallReturnWIntresult = CallReturnWIntresult ∧ stdio_readym′ w′
split ; reflexivity |
bytes :
listZ
q :
actions :
liststream_action
result :
Z
q′ :
m :
p :
w :
born :
listZ
m′ :
w′ :
tail :
listZ
Hbytes :
bytes ++ 10 = acceptedactions ++ tail
Hresult :
tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1
Hstr :
c_stringm p bytes
Hready :
stdio_readym′ w′
⊢
c_stringm p bytes ∧ bytes ++ 10 = acceptedactions ++ tail ∧ tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1 ∧ puts_observationactions = StreamBytes1 acceptedactions ∧ CallReturnWIntresult = CallReturnWIntresult ∧ stdio_readym′ w′
split ; exact Hstr |
bytes :
listZ
q :
actions :
liststream_action
result :
Z
q′ :
m :
p :
w :
born :
listZ
m′ :
w′ :
tail :
listZ
Hbytes :
bytes ++ 10 = acceptedactions ++ tail
Hresult :
tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1
Hstr :
c_stringm p bytes
Hready :
stdio_readym′ w′
⊢
bytes ++ 10 = acceptedactions ++ tail ∧ tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1 ∧ puts_observationactions = StreamBytes1 acceptedactions ∧ CallReturnWIntresult = CallReturnWIntresult ∧ stdio_readym′ w′
split ; exact Hbytes |
bytes :
listZ
q :
actions :
liststream_action
result :
Z
q′ :
m :
p :
w :
born :
listZ
m′ :
w′ :
tail :
listZ
Hbytes :
bytes ++ 10 = acceptedactions ++ tail
Hresult :
tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1
Hstr :
c_stringm p bytes
Hready :
stdio_readym′ w′
⊢
tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1 ∧ puts_observationactions = StreamBytes1 acceptedactions ∧ CallReturnWIntresult = CallReturnWIntresult ∧ stdio_readym′ w′
split ; exact Hresult |
bytes :
listZ
q :
actions :
liststream_action
result :
Z
q′ :
m :
p :
w :
born :
listZ
m′ :
w′ :
tail :
listZ
Hbytes :
bytes ++ 10 = acceptedactions ++ tail
Hresult :
tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1
Hstr :
c_stringm p bytes
Hready :
stdio_readym′ w′
⊢
puts_observationactions = StreamBytes1 acceptedactions ∧ CallReturnWIntresult = CallReturnWIntresult ∧ stdio_readym′ w′
split ; reflexivity |
bytes :
listZ
q :
actions :
liststream_action
result :
Z
q′ :
m :
p :
w :
born :
listZ
m′ :
w′ :
tail :
listZ
Hbytes :
bytes ++ 10 = acceptedactions ++ tail
Hresult :
tail = [ ] ∧ 0 ≤ result < 2 ^ 31 ∨ result = 2 ^ 32 − 1
Hstr :
c_stringm p bytes
Hready :
stdio_readym′ w′
⊢
CallReturnWIntresult = CallReturnWIntresult ∧ stdio_readym′ w′
split ; reflexivity | exact Hready
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros bytes q actions result q′ m p w born m′ w′ _ & _ & tail & Hbytes & Hresult Hstr Hready
exists p, bytes, acceptedactions, tail, result
split ; reflexivity |
split ; exact Hstr |
split ; exact Hbytes |
split ; exact Hresult |
split ; reflexivity |
split ; reflexivity | exact Hready
Observable protocol boundaries
stdout at startup: unoriented, nothing outstanding, no error.
mkStreamUnoriented [ ] false
The initial stdout is well formed.
Explore proof 3 tactics
Initial goal
unfold stream_wf , stdout_initial
⊢
Forallλb : Z ⇒ 0 ≤ b < 256 outstandingorientation ≔ Unoriented; outstanding ≔ [ ]; stream_error ≔ false ∧ outstandingorientation ≔ Unoriented; outstanding ≔ [ ]; stream_error ≔ false ≠ [ ] → orientationorientation ≔ Unoriented; outstanding ≔ [ ]; stream_error ≔ false = ByteOriented
simpl
⊢
Forallλb : Z ⇒ 0 ≤ b < 256 [ ] ∧ [ ] ≠ [ ] → Unoriented = ByteOriented
split ; constructor | congruence
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
puts of hello from the initial stdout may accept hello and its newline and return 6, delivering nothing yet: they stay outstanding.
209Example puts_buffered_acceptance: puts_protocolhello_bytes stdout_initial Accepthello_bytes ++ 10 6 mkStreamByteOriented hello_bytes ++ 10 false
Explore proof 8 tactics
Initial goal
⊢
puts_protocolhello_bytes stdout_initial Accepthello_bytes ++ 10 6 orientation ≔ ByteOriented; outstanding ≔ hello_bytes ++ 10; stream_error ≔ false
split ; discriminate |
⊢
stream_runstdout_initial Accepthello_bytes ++ 10 orientation ≔ ByteOriented; outstanding ≔ hello_bytes ++ 10; stream_error ≔ false ∧ ∃tail : listZ, hello_bytes ++ 10 = acceptedAccepthello_bytes ++ 10 ++ tail ∧ tail = [ ] ∧ 0 ≤ 6 < 2 ^ 31 ∨ 6 = 2 ^ 32 − 1
split
2 open⊢
stream_runstdout_initial Accepthello_bytes ++ 10 orientation ≔ ByteOriented; outstanding ≔ hello_bytes ++ 10; stream_error ≔ false
focused goal
⊢
∃tail : listZ, hello_bytes ++ 10 = acceptedAccepthello_bytes ++ 10 ++ tail ∧ tail = [ ] ∧ 0 ≤ 6 < 2 ^ 31 ∨ 6 = 2 ^ 32 − 1
–eapply stream_next ; apply stream_accept ; discriminate | | constructor
2 open⊢
Forallλb : Z ⇒ 0 ≤ b < 256 hello_bytes ++ 10
deferred goal
⊢
∃tail : listZ, hello_bytes ++ 10 = acceptedAccepthello_bytes ++ 10 ++ tail ∧ tail = [ ] ∧ 0 ≤ 6 < 2 ^ 31 ∨ 6 = 2 ^ 32 − 1
repeat constructor ; lia
deferred goal
⊢
∃tail : listZ, hello_bytes ++ 10 = acceptedAccepthello_bytes ++ 10 ++ tail ∧ tail = [ ] ∧ 0 ≤ 6 < 2 ^ 31 ∨ 6 = 2 ^ 32 − 1
–exists [ ]
⊢
hello_bytes ++ 10 = acceptedAccepthello_bytes ++ 10 ++ [ ] ∧ [ ] = [ ] ∧ 0 ≤ 6 < 2 ^ 31 ∨ 6 = 2 ^ 32 − 1
split ; reflexivity |
⊢
[ ] = [ ] ∧ 0 ≤ 6 < 2 ^ 31 ∨ 6 = 2 ^ 32 − 1
left
⊢
[ ] = [ ] ∧ 0 ≤ 6 < 2 ^ 31
split ; reflexivity | lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; discriminate |
split
–eapply stream_next ; apply stream_accept ; discriminate | | constructor
repeat constructor ; lia
–exists [ ]
split ; reflexivity |
left
split ; reflexivity | lia
Its observation is the one event of hello and a newline.
220Example puts_buffered_observation: puts_observationAccepthello_bytes ++ 10 = StreamBytes1 104; 101; 108; 108; 111; 10
Explore proof 1 tactics
Initial goal
⊢
puts_observationAccepthello_bytes ++ 10 = StreamBytes1 104; 101; 108; 108; 111; 10
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
reflexivity
Prior output precedes this call; some is delivered, some discarded on error, and later output still succeeds with the error flag set.
226Example partial_delivery_discard_later_output: stream_runmkStreamByteOriented 65; 66 false Accept67; 68; Deliver65; Discard66; 67; Accept69; Deliver68; 69 mkStreamByteOriented [ ] true
Explore proof 5 tactics
Initial goal
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false Accept67; 68; Deliver65; Discard66; 67; Accept69; Deliver68; 69 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
eapply stream_next ; apply stream_accept ; discriminate | repeat constructor ; lia |
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ outstandingorientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false ++ 67; 68; stream_error ≔ stream_errororientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false Deliver65; Discard66; 67; Accept69; Deliver68; 69 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
eapply stream_next ; apply stream_deliver65 66; 67; 68 false ; discriminate |
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 66; 67; 68; stream_error ≔ false Discard66; 67; Accept69; Deliver68; 69 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
eapply stream_next ; apply stream_discard66; 67 68 false ; discriminate |
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 68; stream_error ≔ true Accept69; Deliver68; 69 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
eapply stream_next ; apply stream_accept ; discriminate | repeat constructor ; lia |
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ outstandingorientation ≔ ByteOriented; outstanding ≔ 68; stream_error ≔ true ++ 69; stream_error ≔ stream_errororientation ≔ ByteOriented; outstanding ≔ 68; stream_error ≔ true Deliver68; 69 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
eapply stream_next ; apply stream_deliver68; 69 [ ] true ; discriminate | constructor
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
eapply stream_next ; apply stream_accept ; discriminate | repeat constructor ; lia |
eapply stream_next ; apply stream_deliver65 66; 67; 68 false ; discriminate |
eapply stream_next ; apply stream_discard66; 67 68 false ; discriminate |
eapply stream_next ; apply stream_accept ; discriminate | repeat constructor ; lia |
eapply stream_next ; apply stream_deliver68; 69 [ ] true ; discriminate | constructor
Output errors that settle nothing leave the obligations in place and set the error flag.
240Example error_without_progress: stream_runmkStreamByteOriented 65 false OutputError; OutputError mkStreamByteOriented 65 true
Explore proof 2 tactics
Initial goal
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false OutputError; OutputError orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ true
eapply stream_next ; constructor |
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ true OutputError orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ true
eapply stream_next ; constructor
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
eapply stream_next ; constructor |
eapply stream_next ; constructor
puts may return EOF having accepted nothing, after an output error.
247Example puts_eof_without_acceptance: puts_protocol[ ] mkStreamByteOriented 65 false OutputError 2 ^ 32 − 1 mkStreamByteOriented 65 true
Explore proof 7 tactics
Initial goal
⊢
puts_protocol[ ] orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false OutputError 2 ^ 32 − 1 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ true
split ; discriminate |
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false OutputError orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ true ∧ ∃tail : listZ, [ ] ++ 10 = acceptedOutputError ++ tail ∧ tail = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
split
2 open⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ false OutputError orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ true
focused goal
⊢
∃tail : listZ, [ ] ++ 10 = acceptedOutputError ++ tail ∧ tail = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
–eapply stream_next ; constructor
deferred goal
⊢
∃tail : listZ, [ ] ++ 10 = acceptedOutputError ++ tail ∧ tail = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
–exists 10
⊢
[ ] ++ 10 = acceptedOutputError ++ 10 ∧ 10 = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
split ; reflexivity |
⊢
10 = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
right
⊢
2 ^ 32 − 1 = 2 ^ 32 − 1
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; discriminate |
split
–eapply stream_next ; constructor
–exists 10
split ; reflexivity |
right
reflexivity
puts cannot succeed having accepted the string without its newline.
258Example puts_success_requires_newline: ¬puts_protocolhello_bytes stdout_initial Accepthello_bytes 5 mkStreamByteOriented hello_bytes false
Explore proof 1 tactics
Initial goal
intros _ & _ & tail & Hbytes & → _ | Hresult ; discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros _ & _ & tail & Hbytes & → _ | Hresult ; discriminate
A wide-oriented stream accepts no bytes.
266Example no_wide_acceptance: ∀pending err bytes q′, ¬stream_stepmkStreamWideOriented pending err Acceptbytes q′
Explore proof 3 tactics
Initial goal
⊢
∀pending : listZ err : bool bytes : listZ q′ : stream_state, ¬stream_steporientation ≔ WideOriented; outstanding ≔ pending; stream_error ≔ err Acceptbytes q′
intros pending err bytes q′ H
pending :
listZ
err :
bool
bytes :
listZ
q′ :
H :
stream_steporientation ≔ WideOriented; outstanding ≔ pending; stream_error ≔ err Acceptbytes q′
⊢
False
inversion H
pending :
listZ
err :
bool
bytes :
listZ
q′ :
H :
stream_steporientation ≔ WideOriented; outstanding ≔ pending; stream_error ≔ err Acceptbytes q′
q :
bytes0 :
listZ
H1 :
orientationorientation ≔ WideOriented; outstanding ≔ pending; stream_error ≔ err ≠ WideOriented
H3 :
Forallλb : Z ⇒ 0 ≤ b < 256 bytes
H2 :
q = orientation ≔ WideOriented; outstanding ≔ pending; stream_error ≔ err
H0 :
bytes0 = bytes
H4 :
orientation ≔ ByteOriented; outstanding ≔ outstandingorientation ≔ WideOriented; outstanding ≔ pending; stream_error ≔ err ++ bytes; stream_error ≔ stream_errororientation ≔ WideOriented; outstanding ≔ pending; stream_error ≔ err = q′
⊢
False
contradiction
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros pending err bytes q′ H
inversion H
contradiction
Delivery must start with the oldest obligation.
271Example no_out_of_order_delivery: ∀q′, ¬stream_stepmkStreamByteOriented 65; 66 false Deliver66 q′
Explore proof 2 tactics
Initial goal
⊢
∀q′ : stream_state, ¬stream_steporientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false Deliver66 q′
intros q′ H
q′ :
H :
stream_steporientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false Deliver66 q′
⊢
False
inversion H ; subst ; simpl in * ; discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros q′ H
inversion H ; subst ; simpl in * ; discriminate
A value that is not a byte cannot be accepted.
Explore proof 4 tactics
Initial goal
⊢
∀q q′ : stream_state, ¬stream_stepq Accept256 q′
intros q q′ H
q, q′ :
H :
stream_stepq Accept256 q′
⊢
False
inversion H as q0 bytes Ho Hb | | |
q, q′ :
H :
stream_stepq Accept256 q′
q0 :
bytes :
listZ
Ho :
Hb :
Forallλb : Z ⇒ 0 ≤ b < 256 256
H0 :
q0 = q
H1 :
bytes = 256
H2 :
orientation ≔ ByteOriented; outstanding ≔ outstandingq ++ 256; stream_error ≔ stream_errorq = q′
⊢
False
inversion Hb
q, q′ :
H :
stream_stepq Accept256 q′
q0 :
bytes :
listZ
Ho :
Hb :
Forallλb : Z ⇒ 0 ≤ b < 256 256
H0 :
q0 = q
H1 :
bytes = 256
H2 :
orientation ≔ ByteOriented; outstanding ≔ outstandingq ++ 256; stream_error ≔ stream_errorq = q′
x :
Z
l :
listZ
H5 :
0 ≤ 256 < 256
H6 :
Forallλb : Z ⇒ 0 ≤ b < 256 [ ]
H3 :
x = 256
H4 :
l = [ ]
⊢
False
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros q q′ H
inversion H as q0 bytes Ho Hb | | |
inversion Hb
lia
puts on a wide-oriented stream is no protocol run, even one that does nothing and returns EOF.
282Example no_wide_eof_summary: ∀bytes, ¬puts_protocolbytes mkStreamWideOriented [ ] false [ ] 2 ^ 32 − 1 mkStreamWideOriented [ ] false
Explore proof 3 tactics
Initial goal
⊢
∀bytes : listZ, ¬puts_protocolbytes orientation ≔ WideOriented; outstanding ≔ [ ]; stream_error ≔ false [ ] 2 ^ 32 − 1 orientation ≔ WideOriented; outstanding ≔ [ ]; stream_error ≔ false
intros bytes Ho _
bytes :
listZ
Ho :
orientationorientation ≔ WideOriented; outstanding ≔ [ ]; stream_error ≔ false ≠ WideOriented
⊢
False
apply Ho
bytes :
listZ
Ho :
orientationorientation ≔ WideOriented; outstanding ≔ [ ]; stream_error ≔ false ≠ WideOriented
⊢
orientationorientation ≔ WideOriented; outstanding ≔ [ ]; stream_error ≔ false = WideOriented
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros bytes Ho _
apply Ho
reflexivity
puts may return EOF having accepted part of its string.
288Example puts_partial_eof: puts_protocol65; 66 stdout_initial Accept65; OutputError 2 ^ 32 − 1 mkStreamByteOriented 65 true
Explore proof 8 tactics
Initial goal
⊢
puts_protocol65; 66 stdout_initial Accept65; OutputError 2 ^ 32 − 1 orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ true
split ; discriminate |
⊢
stream_runstdout_initial Accept65; OutputError orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ true ∧ ∃tail : listZ, 65; 66 ++ 10 = acceptedAccept65; OutputError ++ tail ∧ tail = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
split
2 open⊢
stream_runstdout_initial Accept65; OutputError orientation ≔ ByteOriented; outstanding ≔ 65; stream_error ≔ true
focused goal
⊢
∃tail : listZ, 65; 66 ++ 10 = acceptedAccept65; OutputError ++ tail ∧ tail = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
–eapply stream_next ; apply stream_accept ; discriminate | repeat constructor ; lia |
2 open⊢
deferred goal
⊢
∃tail : listZ, 65; 66 ++ 10 = acceptedAccept65; OutputError ++ tail ∧ tail = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
eapply stream_next ; constructor
deferred goal
⊢
∃tail : listZ, 65; 66 ++ 10 = acceptedAccept65; OutputError ++ tail ∧ tail = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
–exists 66; 10
⊢
65; 66 ++ 10 = acceptedAccept65; OutputError ++ 66; 10 ∧ 66; 10 = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
split ; reflexivity |
⊢
66; 10 = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
right
⊢
2 ^ 32 − 1 = 2 ^ 32 − 1
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; discriminate |
split
–eapply stream_next ; apply stream_accept ; discriminate | repeat constructor ; lia |
eapply stream_next ; constructor
–exists 66; 10
split ; reflexivity |
right
reflexivity
puts may return EOF having accepted its whole string and newline.
299Example puts_full_eof: puts_protocol65 stdout_initial Accept65; Accept10; OutputError 2 ^ 32 − 1 mkStreamByteOriented 65; 10 true
Explore proof 9 tactics
Initial goal
⊢
puts_protocol65 stdout_initial Accept65; Accept10; OutputError 2 ^ 32 − 1 orientation ≔ ByteOriented; outstanding ≔ 65; 10; stream_error ≔ true
split ; discriminate |
⊢
stream_runstdout_initial Accept65; Accept10; OutputError orientation ≔ ByteOriented; outstanding ≔ 65; 10; stream_error ≔ true ∧ ∃tail : listZ, 65 ++ 10 = acceptedAccept65; Accept10; OutputError ++ tail ∧ tail = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
split
2 open⊢
stream_runstdout_initial Accept65; Accept10; OutputError orientation ≔ ByteOriented; outstanding ≔ 65; 10; stream_error ≔ true
focused goal
⊢
∃tail : listZ, 65 ++ 10 = acceptedAccept65; Accept10; OutputError ++ tail ∧ tail = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
–eapply stream_next ; apply stream_accept ; discriminate | repeat constructor ; lia |
2 open⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ outstandingstdout_initial ++ 65; stream_error ≔ stream_errorstdout_initial Accept10; OutputError orientation ≔ ByteOriented; outstanding ≔ 65; 10; stream_error ≔ true
deferred goal
⊢
∃tail : listZ, 65 ++ 10 = acceptedAccept65; Accept10; OutputError ++ tail ∧ tail = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
eapply stream_next ; apply stream_accept ; discriminate | repeat constructor ; lia |
2 open⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ outstandingorientation ≔ ByteOriented; outstanding ≔ outstandingstdout_initial ++ 65; stream_error ≔ stream_errorstdout_initial ++ 10; stream_error ≔ stream_errororientation ≔ ByteOriented; outstanding ≔ outstandingstdout_initial ++ 65; stream_error ≔ stream_errorstdout_initial OutputError orientation ≔ ByteOriented; outstanding ≔ 65; 10; stream_error ≔ true
deferred goal
⊢
∃tail : listZ, 65 ++ 10 = acceptedAccept65; Accept10; OutputError ++ tail ∧ tail = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
eapply stream_next ; constructor
deferred goal
⊢
∃tail : listZ, 65 ++ 10 = acceptedAccept65; Accept10; OutputError ++ tail ∧ tail = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
–exists [ ]
⊢
65 ++ 10 = acceptedAccept65; Accept10; OutputError ++ [ ] ∧ [ ] = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
split ; reflexivity |
⊢
[ ] = [ ] ∧ 0 ≤ 2 ^ 32 − 1 < 2 ^ 31 ∨ 2 ^ 32 − 1 = 2 ^ 32 − 1
right
⊢
2 ^ 32 − 1 = 2 ^ 32 − 1
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; discriminate |
split
–eapply stream_next ; apply stream_accept ; discriminate | repeat constructor ; lia |
eapply stream_next ; apply stream_accept ; discriminate | repeat constructor ; lia |
eapply stream_next ; constructor
–exists [ ]
split ; reflexivity |
right
reflexivity
The observation gathers all accepted bytes into one event, skipping deliveries, and is one empty event when nothing was accepted.
312Example cumulative_acceptance_observation: puts_observationAccept65; Deliver65; Accept66; 10 = StreamBytes1 65; 66; 10 ∧ puts_observationOutputError = StreamBytes1 [ ]
Explore proof 1 tactics
Initial goal
⊢
puts_observationAccept65; Deliver65; Accept66; 10 = StreamBytes1 65; 66; 10 ∧ puts_observationOutputError = StreamBytes1 [ ]
split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; reflexivity
Resolutions keep discards in their place among deliveries: moving the discarded bytes after the delivered ones gives another order.