rocq/theories/Streams.v
Selected stream queries and close, over explicit projections of the application's libc world. stream_protocol is a projection, not a second stdout queue: the composite world must use its authoritative shutdown stdout. Physical buffering and ownership are separate. These are trusted libc contracts, not a native adequacy proof.
From Stdlib Require Import ZArith List Bool Lia
From Nanofil Require Import Syntax Values Memory Runtime ExternalCalls ExternalMachine Stdio
Import ListNotations
Open Scope Z_scope
An open stream's identifier, logical protocol and physical buffered count. In wide mode the count is in wide characters, not bytes.
| stream_identifier | : Z | |
| stream_protocol | ||
| stream_pending | : Z |
The integration obligations for a selected native stream. stream_rep includes native FILE validity, lock/TLS sources, orientation, physical buffering, and exclusive close ownership. Releases name only owned heap objects, never caller-owned setvbuf storage or static FILEs. stream_frame preserves unrelated state, including the shutdown callback inventory, but may change errno. Effects separately frame caller memory. stream_state_at survives handle consumption and MUST project the same authoritative shutdown stdout, not store a copy. Wide realization must cover physical buffering and shared conversion cache mutations; a reference-count decrement is not an owned free. No projection grants authority merely by its address.
| stream_at | : world → ptr → optionstream_info | |
| stream_state_at | : world → ptr → stream_state | |
| stream_rep | : mem → world → Prop | |
| stream_sources | ||
| stream_writes | ||
| stream_aux_roots | ||
| stream_releases | : world → ptr → listZ | |
| stream_requests | : world → ptr → Z → Z → Prop | |
| stream_frame | : ptr → world → world → Prop | |
| stream_wide_settlement | : world → ptr → stream_state → stream_state → bool → Prop |
Arguments stream_at { world }
Arguments stream_state_at { world }
Arguments stream_rep { world }
Arguments stream_sources { world }
Arguments stream_writes { world }
Arguments stream_aux_roots { world }
Arguments stream_releases { world }
Arguments stream_requests { world }
Arguments stream_frame { world }
Arguments stream_wide_settlement { world }
Scalar-only roots (notably errno) need not authorize aux mutation. Test entry memory, not historical born objects after a release. The ordinary effects path still bounds all writes independently.
56Definition stream_aux_frameworld model : stream_modelworld m : mem w : world p : ptr m′ : mem : Prop ≔
∀a, in_objectm a → ¬write_authoritystream_aux_rootsmodel w p [ ] m a → m_auxm′ a = m_auxm a
Canonical physical size_t and a well-formed logical protocol. A physical count is deliberately not equated with outstanding output.
stream_wfstream_protocolinfo ∧ 0 ≤ stream_pendinginfo < 2 ^ 64
A selected handle is open, represented and has writable stream roots. The stronger native representation is an independent premise.
68Definition stream_openworld model : stream_modelworld m : mem w : world p : ptr info : stream_info : Prop ≔
stream_repmodel m w ∧ stream_atmodel w p = Someinfo ∧ stream_protocolinfo = stream_state_atmodel w p ∧ stream_info_wfinfo ∧ Forallwritable_spanm stream_writesmodel w p
Canonical signed int results are carried as unsigned W bits.
2 ^ 31 ≤ result < 2 ^ 32
EOF at this glibc pin, not a mathematical negative machine word.
2 ^ 32 − 1
One pointer argument and a discarded or correctly classed result.
Readable caller arguments cannot delegate new persistent writable roots: only the old stream roots and fresh allocations may do so. Future private sources retain old source capabilities or born ones; future release rights retain old ownership or fresh allocation. A writable root alone is not evidence of exclusive release ownership.
89Definition stream_delegatesworld model : stream_modelworld w : world p : ptr born : listZ m′ : mem w′ : world : Prop ≔
∀root, Inroot stream_writesmodel w′ p → available_capstream_sourcesmodel w p born m′ ptr_capspan_ptrroot ∧ ∀a, span_containsroot a → write_authoritystream_writesmodel w p born m′ a ∧ ∀source, Insource stream_sourcesmodel w′ p → ∃old, Inold stream_sourcesmodel w p ∧ ptr_capspan_ptrsource = ptr_capspan_ptrold ∨ ∃base, Inbase born ∧ ptr_capspan_ptrsource = Objbase ∨ ptr_capspan_ptrsource = Robase ∧ ∀base, Inbase stream_releasesmodel w′ p → Inbase stream_releasesmodel w p ∨ Inbase born
Admission to queries and close is independent of the chosen result.
103Definition stream_call_preworld model : stream_modelworld xs : listword m : mem w : world : Prop ≔
∃p info, xs = WPtrp ∧ stream_openmodel m w p info
ferror observes the error flag without changing the stream. Its nonzero return is not specified as one. Locks may still mutate.
109Definition ferror_postworld model : stream_modelworld xs : listword m : mem w : world born : listZ trace : listevent ending : call_end m′ : mem w′ : world : Prop ≔
∃p info result, xs = WPtrp ∧ stream_atmodel w p = Someinfo ∧ stream_openmodel m′ w′ p info ∧ stream_framemodel p w w′ ∧ stream_delegatesmodel w p born m′ w′ ∧ trace = [ ] ∧ ending = CallReturnWIntresult ∧ 0 ≤ result < 2 ^ 32 ∧ result = 0 ↔ stream_errorstream_protocolinfo = false
__fpending returns the physical count, preserving stream state.
119Definition fpending_postworld model : stream_modelworld xs : listword m : mem w : world born : listZ trace : listevent ending : call_end m′ : mem w′ : world : Prop ≔
∃p info, xs = WPtrp ∧ stream_atmodel w p = Someinfo ∧ stream_openmodel m′ w′ p info ∧ stream_framemodel p w w′ ∧ stream_delegatesmodel w p born m′ w′ ∧ trace = [ ] ∧ ending = CallReturnWIntstream_pendinginfo
Query prefixes preserve the selected open stream and have no output. Queries may lock private FILE storage, but preserve caller bytes and scalar errno. This is a trusted entry-memory frame, not a consequence of the larger ordinary write footprint. Queries do not allocate, hence have no modeled resource ending.
132Definition query_prefixworld model : stream_modelworld xs : listword m : mem w : world born : listZ trace : listevent m′ : mem w′ : world : Prop ≔
∃p info, xs = WPtrp ∧ stream_atmodel w p = Someinfo ∧ stream_openmodel m′ w′ p info ∧ stream_framemodel p w w′ ∧ stream_delegatesmodel w p born m′ w′ ∧ trace = [ ] ∧ stream_aux_framemodel m w p m′ ∧ ∀a, in_objectm a → ¬write_authoritystream_aux_rootsmodel w p [ ] m a → m_bytesm′ a = m_bytesm a
ferror's exact P-to-W contract.
mkContractworld RClassW stream_query_abiW stream_call_premodel
λ xs _ w ⇒
match xs with
_
⇒
[ ]
λ xs _ w ⇒
match xs with
_
⇒
[ ]
λ_ _ _ ⇒ [ ]
λ_ _ _ _ _ ⇒ False
query_prefixmodel
ferror_postmodel
λ_ ⇒ False
__fpending's exact P-to-L contract; its C symbol has two underscores.
mkContractworld RClassL stream_query_abiL stream_call_premodel
λ xs _ w ⇒
match xs with
_
⇒
[ ]
λ xs _ w ⇒
match xs with
_
⇒
[ ]
λ_ _ _ ⇒ [ ]
λ_ _ _ _ _ ⇒ False
query_prefixmodel
fpending_postmodel
λ_ ⇒ False
An owned release has consumed a heap object's lifetime, including on EOF. The capability remains an identity, but is no longer live.
∀base, Inbase bases → object_regionbase m_regionsm = SomemkRegionbase base Heap Freed
Byte settlement uses the existing FIFO without new acceptance. Wide settlement instead requires independent selected native coverage of conversion and physical buffering, including completion when complete is true. It uses the same orientation/error projection; there is no wide queue hidden in the byte protocol.
168Definition stream_settlementworld model : stream_modelworld w : world p : ptr old final : stream_state complete : bool : Prop ≔
⇒
stream_wide_settlementmodel w p old final complete ∧ orientationfinal = WideOriented ∧ outstandingfinal = [ ] ∧ stream_errorold = true → stream_errorfinal = true
_
⇒
∃actions, stream_runold actions final ∧ acceptedactions = [ ] ∧ complete = true → outstandingfinal = [ ]
Completed settlement empties the authoritative protocol; wide physical settlement additionally needs the supplied realization.
stream_settlementmodel w p old final true
outstandingfinal = [ ]
Explore proof 8 tactics
Initial goal
⊢
∀world : Type model : stream_modelworld w : world p : ptr old final : stream_state, stream_settlementmodel w p old final true → outstandingfinal = [ ]
intros world model w p old final H
world :
Type
model :
stream_modelworld
w :
world
p :
old, final :
H :
stream_settlementmodel w p old final true
⊢
outstandingfinal = [ ]
unfold stream_settlement in H
world :
Type
model :
stream_modelworld
w :
world
p :
old, final :
H :
⇒
stream_wide_settlementmodel w p old final true ∧ orientationfinal = WideOriented ∧ outstandingfinal = [ ] ∧ stream_errorold = true → stream_errorfinal = true
_
⇒
∃actions : liststream_action, stream_runold actions final ∧ acceptedactions = [ ] ∧ true = true → outstandingfinal = [ ]
⊢
outstandingfinal = [ ]
destruct orientationold
3 openworld :
Type
model :
stream_modelworld
w :
world
p :
old, final :
H :
∃actions : liststream_action, stream_runold actions final ∧ acceptedactions = [ ] ∧ true = true → outstandingfinal = [ ]
⊢
outstandingfinal = [ ]
focused goal
world :
Type
model :
stream_modelworld
w :
world
p :
old, final :
H :
∃actions : liststream_action, stream_runold actions final ∧ acceptedactions = [ ] ∧ true = true → outstandingfinal = [ ]
⊢
outstandingfinal = [ ]
focused goal
world :
Type
model :
stream_modelworld
w :
world
p :
old, final :
H :
stream_wide_settlementmodel w p old final true ∧ orientationfinal = WideOriented ∧ outstandingfinal = [ ] ∧ stream_errorold = true → stream_errorfinal = true
⊢
outstandingfinal = [ ]
–destruct H as actions & _ & _ & Hdone
3 openworld :
Type
model :
stream_modelworld
w :
world
p :
old, final :
actions :
liststream_action
Hdone :
true = true → outstandingfinal = [ ]
⊢
outstandingfinal = [ ]
deferred goal
world :
Type
model :
stream_modelworld
w :
world
p :
old, final :
H :
∃actions : liststream_action, stream_runold actions final ∧ acceptedactions = [ ] ∧ true = true → outstandingfinal = [ ]
⊢
outstandingfinal = [ ]
deferred goal
world :
Type
model :
stream_modelworld
w :
world
p :
old, final :
H :
stream_wide_settlementmodel w p old final true ∧ orientationfinal = WideOriented ∧ outstandingfinal = [ ] ∧ stream_errorold = true → stream_errorfinal = true
⊢
outstandingfinal = [ ]
auto
2 opendeferred goal
world :
Type
model :
stream_modelworld
w :
world
p :
old, final :
H :
∃actions : liststream_action, stream_runold actions final ∧ acceptedactions = [ ] ∧ true = true → outstandingfinal = [ ]
⊢
outstandingfinal = [ ]
deferred goal
world :
Type
model :
stream_modelworld
w :
world
p :
old, final :
H :
stream_wide_settlementmodel w p old final true ∧ orientationfinal = WideOriented ∧ outstandingfinal = [ ] ∧ stream_errorold = true → stream_errorfinal = true
⊢
outstandingfinal = [ ]
–destruct H as actions & _ & _ & Hdone
2 openworld :
Type
model :
stream_modelworld
w :
world
p :
old, final :
actions :
liststream_action
Hdone :
true = true → outstandingfinal = [ ]
⊢
outstandingfinal = [ ]
deferred goal
world :
Type
model :
stream_modelworld
w :
world
p :
old, final :
H :
stream_wide_settlementmodel w p old final true ∧ orientationfinal = WideOriented ∧ outstandingfinal = [ ] ∧ stream_errorold = true → stream_errorfinal = true
⊢
outstandingfinal = [ ]
auto
deferred goal
world :
Type
model :
stream_modelworld
w :
world
p :
old, final :
H :
stream_wide_settlementmodel w p old final true ∧ orientationfinal = WideOriented ∧ outstandingfinal = [ ] ∧ stream_errorold = true → stream_errorfinal = true
⊢
outstandingfinal = [ ]
–tauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros world model w p old final H
unfold stream_settlement in H
destruct orientationold
–destruct H as actions & _ & _ & Hdone
auto
–destruct H as actions & _ & _ & Hdone
auto
–tauto
A close prefix may settle old output but never accept new output. A resource stop need not have closed the stream or released storage. Wide-stream settlement remains an explicit integration obligation.
195Definition fclose_prefixworld model : stream_modelworld xs : listword m : mem w : world born : listZ trace : listevent m′ : mem w′ : world : Prop ≔
∃p info final, xs = WPtrp ∧ stream_atmodel w p = Someinfo ∧ stream_settlementmodel w p stream_protocolinfo final false ∧ stream_state_atmodel w′ p = final ∧ stream_repmodel m′ w′ ∧ stream_framemodel p w w′ ∧ stream_delegatesmodel w p born m′ w′ ∧ trace = [ ] ∧ stream_atmodel w′ p = None ∨ ∃info′, stream_atmodel w′ p = Someinfo′ ∧ stream_protocolinfo′ = final ∧ stream_aux_framemodel m w p m′
Close settles all old obligations in FIFO order (delivery OR error discard), consumes the handle and owned heaps on both result paths. A descriptor close failure can return EOF after all output delivered.
211Definition fclose_postworld model : stream_modelworld xs : listword m : mem w : world born : listZ trace : listevent ending : call_end m′ : mem w′ : world : Prop ≔
∃p info final result, xs = WPtrp ∧ stream_atmodel w p = Someinfo ∧ stream_settlementmodel w p stream_protocolinfo final true ∧ stream_state_atmodel w′ p = final ∧ result = 0 ∨ result = stream_eof ∧ stream_atmodel w′ p = None ∧ stream_consumedm′ stream_releasesmodel w p ∧ stream_repmodel m′ w′ ∧ stream_framemodel p w w′ ∧ trace = [ ] ∧ ending = CallReturnWIntresult
P-to-W close with separate ownership and request footprints.
mkContractworld RClassW stream_query_abiW stream_call_premodel
λ xs _ w ⇒
match xs with
_
⇒
[ ]
λ xs _ w ⇒
match xs with
_
⇒
[ ]
λ xs _ w ⇒
match xs with
_
⇒
[ ]
λ xs _ w ⇒
match xs with
_
⇒
λ_ _ ⇒ False
fclose_prefixmodel
fclose_postmodel
Consequences of trusted calls over any runtime, without changing the supplied machine or adding runtime axioms.
Construct a normal query from independently established effects and postconditions. Prefix and native representation are not inferred.
stream_query_abiW r args
stream_call_premodel xs m w
E.prefixferror_contractmodel xs s m w born trace s′ m′ w′
ferror_postmodel xs m w born trace CallReturnWIntresult m′ w′
E.invokeferror_contractmodel r args xs s m w trace CallReturnWIntresult s′ m′ w′
Explore proof 12 tactics
Initial goal
⊢
∀world : Type model : stream_modelworld r : call_result args : listarg xs : listword s : R.state m : mem w : world born : listZ trace : listevent result : Z s′ : R.state m′ : mem w′ : world, stream_query_abiW r args → stream_call_premodel xs m w → E.prefixferror_contractmodel xs s m w born trace s′ m′ w′ → ferror_postmodel xs m w born trace CallReturnWIntresult m′ w′ → E.invokeferror_contractmodel r args xs s m w trace CallReturnWIntresult s′ m′ w′
intros world model r args xs s m w born trace result s′ m′ w′ Habi Hpre Hprefix Hpost
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
stream_query_abiW r args
Hpre :
stream_call_premodel xs m w
Hprefix :
E.prefixferror_contractmodel xs s m w born trace s′ m′ w′
Hpost :
ferror_postmodel xs m w born trace CallReturnWIntresult m′ w′
⊢
E.invokeferror_contractmodel r args xs s m w trace CallReturnWIntresult s′ m′ w′
eapply E.invoke_normal with born := born ; try exact Habi ; try exact Hpre ; try exact Hprefix ; try exact Hpost ; try discriminate
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
stream_query_abiW r args
Hpre :
stream_call_premodel xs m w
Hprefix :
E.prefixferror_contractmodel xs s m w born trace s′ m′ w′
Hpost :
ferror_postmodel xs m w born trace CallReturnWIntresult m′ w′
⊢
∀values : listword, CallReturnWIntresult = CallReturnvalues → return_shapecontract_returnsferror_contractmodel values ∧ Forallword_authoritycontract_sourcesferror_contractmodel xs m w born m′ values
intros values Heq
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
stream_query_abiW r args
Hpre :
stream_call_premodel xs m w
Hprefix :
E.prefixferror_contractmodel xs s m w born trace s′ m′ w′
Hpost :
ferror_postmodel xs m w born trace CallReturnWIntresult m′ w′
values :
listword
Heq :
CallReturnWIntresult = CallReturnvalues
⊢
return_shapecontract_returnsferror_contractmodel values ∧ Forallword_authoritycontract_sourcesferror_contractmodel xs m w born m′ values
injection Heq as ←
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
stream_query_abiW r args
Hpre :
stream_call_premodel xs m w
Hprefix :
E.prefixferror_contractmodel xs s m w born trace s′ m′ w′
Hpost :
ferror_postmodel xs m w born trace CallReturnWIntresult m′ w′
⊢
return_shapecontract_returnsferror_contractmodel WIntresult ∧ Forallword_authoritycontract_sourcesferror_contractmodel xs m w born m′ WIntresult
split ; | constructor ; exact I | constructor
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
stream_query_abiW r args
Hpre :
stream_call_premodel xs m w
Hprefix :
E.prefixferror_contractmodel xs s m w born trace s′ m′ w′
Hpost :
ferror_postmodel xs m w born trace CallReturnWIntresult m′ w′
⊢
return_shapecontract_returnsferror_contractmodel WIntresult
exists WIntresult
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
stream_query_abiW r args
Hpre :
stream_call_premodel xs m w
Hprefix :
E.prefixferror_contractmodel xs s m w born trace s′ m′ w′
Hpost :
ferror_postmodel xs m w born trace CallReturnWIntresult m′ w′
split ; reflexivity |
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
stream_query_abiW r args
Hpre :
stream_call_premodel xs m w
Hprefix :
E.prefixferror_contractmodel xs s m w born trace s′ m′ w′
Hpost :
ferror_postmodel xs m w born trace CallReturnWIntresult m′ w′
⊢
word_at_classW WIntresult = SomeWIntresult
simpl
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
stream_query_abiW r args
Hpre :
stream_call_premodel xs m w
Hprefix :
E.prefixferror_contractmodel xs s m w born trace s′ m′ w′
Hpost :
ferror_postmodel xs m w born trace CallReturnWIntresult m′ w′
destruct Hpost as p & info & n & _ & _ & _ & _ & _ & _ & Hend & Hrange & _
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
stream_query_abiW r args
Hpre :
stream_call_premodel xs m w
Hprefix :
E.prefixferror_contractmodel xs s m w born trace s′ m′ w′
p :
info :
n :
Z
Hend :
CallReturnWIntresult = CallReturnWIntn
Hrange :
0 ≤ n < 2 ^ 32
injection Hend as ←
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
stream_query_abiW r args
Hpre :
stream_call_premodel xs m w
Hprefix :
E.prefixferror_contractmodel xs s m w born trace s′ m′ w′
p :
info :
Hrange :
0 ≤ result < 2 ^ 32
rewrite Z.mod_small by exact Hrange
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
stream_query_abiW r args
Hpre :
stream_call_premodel xs m w
Hprefix :
E.prefixferror_contractmodel xs s m w born trace s′ m′ w′
p :
info :
Hrange :
0 ≤ result < 2 ^ 32
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros world model r args xs s m w born trace result s′ m′ w′ Habi Hpre Hprefix Hpost
eapply E.invoke_normal with born := born ; try exact Habi ; try exact Hpre ; try exact Hprefix ; try exact Hpost ; try discriminate
intros values Heq
injection Heq as ←
split ; | constructor ; exact I | constructor
exists WIntresult
split ; reflexivity |
simpl
destruct Hpost as p & info & n & _ & _ & _ & _ & _ & _ & Hend & Hrange & _
injection Hend as ←
rewrite Z.mod_small by exact Hrange
reflexivity
ferror cannot take the resource rule: its request set is empty.
E.invokeferror_contractmodel r args xs s m w trace ending s′ m′ w′
∃born, ferror_postmodel xs m w born trace ending m′ w′
Explore proof 4 tactics
Initial goal
⊢
∀world : Type model : stream_modelworld r : call_result args : listarg xs : listword s : R.state m : mem w : world trace : listevent ending : call_end s′ : R.state m′ : mem w′ : world, E.invokeferror_contractmodel r args xs s m w trace ending s′ m′ w′ → ∃born : listZ, ferror_postmodel xs m w born trace ending m′ w′
intros world model r args xs s m w trace ending s′ m′ w′ Hcall
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokeferror_contractmodel r args xs s m w trace ending s′ m′ w′
⊢
∃born : listZ, ferror_postmodel xs m w born trace ending m′ w′
inversion Hcall ; subst
2 openworld :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokeferror_contractmodel r args xs s m w trace ending s′ m′ w′
born :
listZ
H :
contract_abiferror_contractmodel r args
H0 :
contract_preferror_contractmodel xs m w
H1 :
E.prefixferror_contractmodel xs s m w born trace s′ m′ w′
H2 :
contract_postferror_contractmodel xs m w born trace ending m′ w′
H3 :
∀why : reason, ending ≠ CallResourcewhy
H4 :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnsferror_contractmodel values ∧ Forallword_authoritycontract_sourcesferror_contractmodel xs m w born m′ values
H5 :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
∃born0 : listZ, ferror_postmodel xs m w born0 trace ending m′ w′
focused goal
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
why :
Hcall :
E.invokeferror_contractmodel r args xs s m w trace CallResourcewhy s′ m′ w′
born :
listZ
H :
contract_abiferror_contractmodel r args
H0 :
contract_preferror_contractmodel xs m w
H1 :
E.prefixferror_contractmodel xs s m w born trace s′ m′ w′
H2 :
E.resource_failurecontract_requestsferror_contractmodel xs m w s′ why
H3 :
contract_resourceferror_contractmodel why
⊢
∃born0 : listZ, ferror_postmodel xs m w born0 trace CallResourcewhy m′ w′
–match goal withHpost : contract_post_ _ _ _ _ _ _ _ |- _⇒exists born ; exact Hpostend
deferred goal
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
why :
Hcall :
E.invokeferror_contractmodel r args xs s m w trace CallResourcewhy s′ m′ w′
born :
listZ
H :
contract_abiferror_contractmodel r args
H0 :
contract_preferror_contractmodel xs m w
H1 :
E.prefixferror_contractmodel xs s m w born trace s′ m′ w′
H2 :
E.resource_failurecontract_requestsferror_contractmodel xs m w s′ why
H3 :
contract_resourceferror_contractmodel why
⊢
∃born0 : listZ, ferror_postmodel xs m w born0 trace CallResourcewhy m′ w′
–contradiction
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros world model r args xs s m w trace ending s′ m′ w′ Hcall
inversion Hcall ; subst
–match goal withHpost : contract_post_ _ _ _ _ _ _ _ |- _⇒exists born ; exact Hpostend
–contradiction
__fpending likewise has only ordinary query completions.
E.invokefpending_contractmodel r args xs s m w trace ending s′ m′ w′
∃born, fpending_postmodel xs m w born trace ending m′ w′
Explore proof 4 tactics
Initial goal
⊢
∀world : Type model : stream_modelworld r : call_result args : listarg xs : listword s : R.state m : mem w : world trace : listevent ending : call_end s′ : R.state m′ : mem w′ : world, E.invokefpending_contractmodel r args xs s m w trace ending s′ m′ w′ → ∃born : listZ, fpending_postmodel xs m w born trace ending m′ w′
intros world model r args xs s m w trace ending s′ m′ w′ Hcall
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokefpending_contractmodel r args xs s m w trace ending s′ m′ w′
⊢
∃born : listZ, fpending_postmodel xs m w born trace ending m′ w′
inversion Hcall ; subst
2 openworld :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokefpending_contractmodel r args xs s m w trace ending s′ m′ w′
born :
listZ
H :
contract_abifpending_contractmodel r args
H0 :
contract_prefpending_contractmodel xs m w
H1 :
E.prefixfpending_contractmodel xs s m w born trace s′ m′ w′
H2 :
contract_postfpending_contractmodel xs m w born trace ending m′ w′
H3 :
∀why : reason, ending ≠ CallResourcewhy
H4 :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnsfpending_contractmodel values ∧ Forallword_authoritycontract_sourcesfpending_contractmodel xs m w born m′ values
H5 :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
∃born0 : listZ, fpending_postmodel xs m w born0 trace ending m′ w′
focused goal
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
why :
Hcall :
E.invokefpending_contractmodel r args xs s m w trace CallResourcewhy s′ m′ w′
born :
listZ
H :
contract_abifpending_contractmodel r args
H0 :
contract_prefpending_contractmodel xs m w
H1 :
E.prefixfpending_contractmodel xs s m w born trace s′ m′ w′
H2 :
E.resource_failurecontract_requestsfpending_contractmodel xs m w s′ why
H3 :
contract_resourcefpending_contractmodel why
⊢
∃born0 : listZ, fpending_postmodel xs m w born0 trace CallResourcewhy m′ w′
–match goal withHpost : contract_post_ _ _ _ _ _ _ _ |- _⇒exists born ; exact Hpostend
deferred goal
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
why :
Hcall :
E.invokefpending_contractmodel r args xs s m w trace CallResourcewhy s′ m′ w′
born :
listZ
H :
contract_abifpending_contractmodel r args
H0 :
contract_prefpending_contractmodel xs m w
H1 :
E.prefixfpending_contractmodel xs s m w born trace s′ m′ w′
H2 :
E.resource_failurecontract_requestsfpending_contractmodel xs m w s′ why
H3 :
contract_resourcefpending_contractmodel why
⊢
∃born0 : listZ, fpending_postmodel xs m w born0 trace CallResourcewhy m′ w′
–contradiction
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros world model r args xs s m w trace ending s′ m′ w′ Hcall
inversion Hcall ; subst
–match goal withHpost : contract_post_ _ _ _ _ _ _ _ |- _⇒exists born ; exact Hpostend
–contradiction
A resource-ending close has no ordinary-return postcondition.
E.invokefclose_contractmodel r args xs s m w trace ending s′ m′ w′
∃born, fclose_postmodel xs m w born trace ending m′ w′ ∨ ∃why, ending = CallResourcewhy ∧ resource_reasonwhy
Explore proof 6 tactics
Initial goal
⊢
∀world : Type model : stream_modelworld r : call_result args : listarg xs : listword s : R.state m : mem w : world trace : listevent ending : call_end s′ : R.state m′ : mem w′ : world, E.invokefclose_contractmodel r args xs s m w trace ending s′ m′ w′ → ∃born : listZ, fclose_postmodel xs m w born trace ending m′ w′ ∨ ∃why : reason, ending = CallResourcewhy ∧ resource_reasonwhy
intros world model r args xs s m w trace ending s′ m′ w′ Hcall
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokefclose_contractmodel r args xs s m w trace ending s′ m′ w′
⊢
∃born : listZ, fclose_postmodel xs m w born trace ending m′ w′ ∨ ∃why : reason, ending = CallResourcewhy ∧ resource_reasonwhy
inversion Hcall ; subst
2 openworld :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokefclose_contractmodel r args xs s m w trace ending s′ m′ w′
born :
listZ
H :
contract_abifclose_contractmodel r args
H0 :
contract_prefclose_contractmodel xs m w
H1 :
E.prefixfclose_contractmodel xs s m w born trace s′ m′ w′
H2 :
contract_postfclose_contractmodel xs m w born trace ending m′ w′
H3 :
∀why : reason, ending ≠ CallResourcewhy
H4 :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel xs m w born m′ values
H5 :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
∃born0 : listZ, fclose_postmodel xs m w born0 trace ending m′ w′ ∨ ∃why : reason, ending = CallResourcewhy ∧ resource_reasonwhy
focused goal
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
why :
Hcall :
E.invokefclose_contractmodel r args xs s m w trace CallResourcewhy s′ m′ w′
born :
listZ
H :
contract_abifclose_contractmodel r args
H0 :
contract_prefclose_contractmodel xs m w
H1 :
E.prefixfclose_contractmodel xs s m w born trace s′ m′ w′
H2 :
E.resource_failurecontract_requestsfclose_contractmodel xs m w s′ why
H3 :
contract_resourcefclose_contractmodel why
⊢
∃born0 : listZ, fclose_postmodel xs m w born0 trace CallResourcewhy m′ w′ ∨ ∃why0 : reason, CallResourcewhy = CallResourcewhy0 ∧ resource_reasonwhy0
–left
2 openworld :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokefclose_contractmodel r args xs s m w trace ending s′ m′ w′
born :
listZ
H :
contract_abifclose_contractmodel r args
H0 :
contract_prefclose_contractmodel xs m w
H1 :
E.prefixfclose_contractmodel xs s m w born trace s′ m′ w′
H2 :
contract_postfclose_contractmodel xs m w born trace ending m′ w′
H3 :
∀why : reason, ending ≠ CallResourcewhy
H4 :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel xs m w born m′ values
H5 :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
∃born0 : listZ, fclose_postmodel xs m w born0 trace ending m′ w′
deferred goal
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
why :
Hcall :
E.invokefclose_contractmodel r args xs s m w trace CallResourcewhy s′ m′ w′
born :
listZ
H :
contract_abifclose_contractmodel r args
H0 :
contract_prefclose_contractmodel xs m w
H1 :
E.prefixfclose_contractmodel xs s m w born trace s′ m′ w′
H2 :
E.resource_failurecontract_requestsfclose_contractmodel xs m w s′ why
H3 :
contract_resourcefclose_contractmodel why
⊢
∃born0 : listZ, fclose_postmodel xs m w born0 trace CallResourcewhy m′ w′ ∨ ∃why0 : reason, CallResourcewhy = CallResourcewhy0 ∧ resource_reasonwhy0
match goal withHpost : contract_post_ _ _ _ _ _ _ _ |- _⇒exists born ; exact Hpostend
deferred goal
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
why :
Hcall :
E.invokefclose_contractmodel r args xs s m w trace CallResourcewhy s′ m′ w′
born :
listZ
H :
contract_abifclose_contractmodel r args
H0 :
contract_prefclose_contractmodel xs m w
H1 :
E.prefixfclose_contractmodel xs s m w born trace s′ m′ w′
H2 :
E.resource_failurecontract_requestsfclose_contractmodel xs m w s′ why
H3 :
contract_resourcefclose_contractmodel why
⊢
∃born0 : listZ, fclose_postmodel xs m w born0 trace CallResourcewhy m′ w′ ∨ ∃why0 : reason, CallResourcewhy = CallResourcewhy0 ∧ resource_reasonwhy0
–right
world :
Type
model :
stream_modelworld
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
why :
Hcall :
E.invokefclose_contractmodel r args xs s m w trace CallResourcewhy s′ m′ w′
born :
listZ
H :
contract_abifclose_contractmodel r args
H0 :
contract_prefclose_contractmodel xs m w
H1 :
E.prefixfclose_contractmodel xs s m w born trace s′ m′ w′
H2 :
E.resource_failurecontract_requestsfclose_contractmodel xs m w s′ why
H3 :
contract_resourcefclose_contractmodel why
⊢
∃why0 : reason, CallResourcewhy = CallResourcewhy0 ∧ resource_reasonwhy0
eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros world model r args xs s m w trace ending s′ m′ w′ Hcall
inversion Hcall ; subst
–left
match goal withHpost : contract_post_ _ _ _ _ _ _ _ |- _⇒exists born ; exact Hpostend
–right
eauto
A returning close consumes its handle and owned heap storage and settles the surviving authoritative protocol, on both 0 and EOF.
E.invokefclose_contractmodel r args WPtrp s m w trace CallReturnWIntresult s′ m′ w′
stream_atmodel w′ p = None ∧ stream_consumedm′ stream_releasesmodel w p ∧ outstandingstream_state_atmodel w′ p = [ ] ∧ result = 0 ∨ result = stream_eof
Explore proof 7 tactics
Initial goal
⊢
∀world : Type model : stream_modelworld r : call_result args : listarg p : ptr s : R.state m : mem w : world trace : listevent result : Z s′ : R.state m′ : mem w′ : world, E.invokefclose_contractmodel r args WPtrp s m w trace CallReturnWIntresult s′ m′ w′ → stream_atmodel w′ p = None ∧ stream_consumedm′ stream_releasesmodel w p ∧ outstandingstream_state_atmodel w′ p = [ ] ∧ result = 0 ∨ result = stream_eof
intros world model r args p s m w trace result s′ m′ w′ Hcall
world :
Type
model :
stream_modelworld
r :
args :
listarg
p :
s :
R.state
m :
w :
world
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokefclose_contractmodel r args WPtrp s m w trace CallReturnWIntresult s′ m′ w′
⊢
stream_atmodel w′ p = None ∧ stream_consumedm′ stream_releasesmodel w p ∧ outstandingstream_state_atmodel w′ p = [ ] ∧ result = 0 ∨ result = stream_eof
destruct fclose_invocation_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & q & info & final & n & Hargs & _ & Hsettle & Hfinal & Hresult & Hclosed & Hfree & _ & _ & _ & Hend | why & Hbad & _ ; | discriminate Hbad
world :
Type
model :
stream_modelworld
r :
args :
listarg
p :
s :
R.state
m :
w :
world
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokefclose_contractmodel r args WPtrp s m w trace CallReturnWIntresult s′ m′ w′
born :
listZ
q :
info :
final :
n :
Z
Hsettle :
stream_settlementmodel w q stream_protocolinfo final true
Hfinal :
stream_state_atmodel w′ q = final
Hresult :
n = 0 ∨ n = stream_eof
Hclosed :
stream_atmodel w′ q = None
Hfree :
stream_consumedm′ stream_releasesmodel w q
Hend :
CallReturnWIntresult = CallReturnWIntn
⊢
stream_atmodel w′ p = None ∧ stream_consumedm′ stream_releasesmodel w p ∧ outstandingstream_state_atmodel w′ p = [ ] ∧ result = 0 ∨ result = stream_eof
injection Hargs as ←
world :
Type
model :
stream_modelworld
r :
args :
listarg
p :
s :
R.state
m :
w :
world
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokefclose_contractmodel r args WPtrp s m w trace CallReturnWIntresult s′ m′ w′
born :
listZ
info :
final :
n :
Z
Hfinal :
stream_state_atmodel w′ p = final
Hsettle :
stream_settlementmodel w p stream_protocolinfo final true
Hresult :
n = 0 ∨ n = stream_eof
Hfree :
stream_consumedm′ stream_releasesmodel w p
Hclosed :
stream_atmodel w′ p = None
Hend :
CallReturnWIntresult = CallReturnWIntn
⊢
stream_atmodel w′ p = None ∧ stream_consumedm′ stream_releasesmodel w p ∧ outstandingstream_state_atmodel w′ p = [ ] ∧ result = 0 ∨ result = stream_eof
injection Hend as ←
world :
Type
model :
stream_modelworld
r :
args :
listarg
p :
s :
R.state
m :
w :
world
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokefclose_contractmodel r args WPtrp s m w trace CallReturnWIntresult s′ m′ w′
born :
listZ
info :
final :
Hfinal :
stream_state_atmodel w′ p = final
Hsettle :
stream_settlementmodel w p stream_protocolinfo final true
Hresult :
result = 0 ∨ result = stream_eof
Hfree :
stream_consumedm′ stream_releasesmodel w p
Hclosed :
stream_atmodel w′ p = None
⊢
stream_atmodel w′ p = None ∧ stream_consumedm′ stream_releasesmodel w p ∧ outstandingstream_state_atmodel w′ p = [ ] ∧ result = 0 ∨ result = stream_eof
rewrite Hfinal
world :
Type
model :
stream_modelworld
r :
args :
listarg
p :
s :
R.state
m :
w :
world
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokefclose_contractmodel r args WPtrp s m w trace CallReturnWIntresult s′ m′ w′
born :
listZ
info :
final :
Hfinal :
stream_state_atmodel w′ p = final
Hsettle :
stream_settlementmodel w p stream_protocolinfo final true
Hresult :
result = 0 ∨ result = stream_eof
Hfree :
stream_consumedm′ stream_releasesmodel w p
Hclosed :
stream_atmodel w′ p = None
⊢
stream_atmodel w′ p = None ∧ stream_consumedm′ stream_releasesmodel w p ∧ outstandingfinal = [ ] ∧ result = 0 ∨ result = stream_eof
repeat split ; try assumption
world :
Type
model :
stream_modelworld
r :
args :
listarg
p :
s :
R.state
m :
w :
world
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokefclose_contractmodel r args WPtrp s m w trace CallReturnWIntresult s′ m′ w′
born :
listZ
info :
final :
Hfinal :
stream_state_atmodel w′ p = final
Hsettle :
stream_settlementmodel w p stream_protocolinfo final true
Hresult :
result = 0 ∨ result = stream_eof
Hfree :
stream_consumedm′ stream_releasesmodel w p
Hclosed :
stream_atmodel w′ p = None
⊢
outstandingfinal = [ ]
eapply stream_settlement_complete ; exact Hsettle
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros world model r args p s m w trace result s′ m′ w′ Hcall
destruct fclose_invocation_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & q & info & final & n & Hargs & _ & Hsettle & Hfinal & Hresult & Hclosed & Hfree & _ & _ & _ & Hend | why & Hbad & _ ; | discriminate Hbad
injection Hargs as ←
injection Hend as ←
rewrite Hfinal
repeat split ; try assumption
eapply stream_settlement_complete ; exact Hsettle
Standalone compatibility wrapper; logic clients supply their own machine to StreamsOn so its invocation type is exactly theirs.
Include StreamsOn R M
Physical buffering and protocol outstanding bytes are independent.
322Example pending_is_not_outstanding: stream_info_wfmkStreamInfo1 mkStreamByteOriented 65; 66 false 0
Explore proof 3 tactics
Initial goal
⊢
stream_info_wfstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false; stream_pending ≔ 0
unfold stream_info_wf , stream_wf
⊢
Forallλb : Z ⇒ 0 ≤ b < 256 outstandingstream_protocolstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false; stream_pending ≔ 0 ∧ outstandingstream_protocolstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false; stream_pending ≔ 0 ≠ [ ] → orientationstream_protocolstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false; stream_pending ≔ 0 = ByteOriented ∧ 0 ≤ stream_pendingstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ false; stream_pending ≔ 0 < 2 ^ 64
simpl
⊢
Forallλb : Z ⇒ 0 ≤ b < 256 65; 66 ∧ 65; 66 ≠ [ ] → ByteOriented = ByteOriented ∧ 0 ≤ 0 < Z.pow_pos2 64
split ; split ; repeat constructor ; lia | auto | lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A canonical non-one error result is admitted by the result relation.
Explore proof 1 tactics
Initial goal
⊢
0 ≤ 32 < 2 ^ 32 ∧ 32 = 0 ↔ true = false
split ; lia | split ; discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; lia | split ; discriminate