rocq/theories/LibcStreams.v
Composite stdout/stderr contracts. FILE metadata and physical counts live in libc_streams; stdout's only logical protocol lives in shutdown_stdout. Native representation and exclusive ownership remain trusted premises, not consequences of writable addresses. Closed handles retain identity and protocol, but grant no authority.
From Stdlib Require Import String ZArith List Bool Lia
From Nanofil Require Import Term Syntax Values Memory Runtime ExternalCalls ExternalMachine Locale Stdio Shutdown Streams Formatting Libc
Import ListNotations
Open Scope Z_scope
Open Scope list_scope
Exact handle comparison includes capability, not merely address.
Stdout's stable represented handle.
Stderr's stable represented handle.
Selection is capability-sensitive even for a consumed handle.
→
else
None
else
None
Lookup survives consumption and never restores a saved stdout FIFO.
Only active handles expose physical counts and ordinary stream calls.
None
⇒
None
These sources belong to FILE state, not to a caller's format strings. A zero-length handle span supplies its capability, not extra bytes.
mkSpanfile_handlefile 0 :: file_readsfile ++ file_rootsfile
Errno's fixed capability supports its scalar write root in generic delegation. It grants no readable aux slot and is excluded from the private FILE pools by file_errno_apart.
None
⇒
[ ]
Active roots only; closing retires historical buffer authority.
None
⇒
[ ]
Only FILE-private spans may change pointer aux; the extra scalar errno root in libc_stream_writes may not do so.
None
⇒
[ ]
Exclusive heaps are not inferred from the handle or its roots.
None
⇒
[ ]
Errno is a fixed scalar output, not FILE-private retained authority. Entry and endpoint representations independently establish this, including complete aux-loaded capabilities in private sources.
∀root, Inroot file_rootsfile → spans_apartroot mkSpancell 4 ∧ ∀base, ptr_capcell = Objbase ∨ ptr_capcell = Robase → ¬Inbase file_ownedfile ∧ ¬available_capfile_sourcesfile [ ] m Objbase ∧ ¬available_capfile_sourcesfile [ ] m Robase
Structural obligations for an ACTIVE FILE. The supplied native representation additionally owns close rights and excludes caller setvbuf storage and static FILE identities from file_owned.
ptr_addrfile_handlefile ≠ 0 ∧ readable_bytesm file_handlefile 1 ∧ 0 ≤ file_pendingfile < 2 ^ 64 ∧ Forallwritable_spanm file_rootsfile ∧ Forallλsource ⇒ readable_bytesm span_ptrsource span_sizesource file_readsfile ∧ Foralllocale_heapm file_ownedfile ∧ file_errno_apartm cell file
Legacy puts roots are the same active stdout inventory, not a second grant. Historical roots in closed FILE records are deliberately omitted.
A selected close cannot release either stable FILE, locale storage, or authority retained by the other active FILE. Exclusive ownership against caller storage still belongs to the native representation.
∀p file, libc_file_atw p = Somefile → ∀base, Inbase file_ownedfile → ¬Inbase locale_ownedlibc_localefstw ∧ ∀q other, libc_file_atw q = Someother → file_handleother ≠ file_handlefile → ¬Inbase file_ownedother ∧ ¬available_capmkSpanlibc_stdoutw 0 :: mkSpanlibc_stderrw 0 :: locale_private_sourceslibc_localefstw ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase ∧ ¬available_capmkSpanlibc_stdoutw 0 :: mkSpanlibc_stderrw 0 :: locale_private_sourceslibc_localefstw ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Robase
Endpoint readiness permits either FILE closed. It keeps locale/errno and shutdown structure coherent; it does not establish native representation, exclusive ownership or progress.
repm w
∧
locale_readyλ_ _ ⇒ True m libc_localefstw
∧
errno_cellm libc_errnofstw
∧
∧
∧
shutdown_uniquesndw
∧
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutw ≠ ptr_addrlibc_stderrw ∧ stdio_rootslibc_stdiofstw = libc_active_rootsw ∧ stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw ∧ libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw ∧ libc_release_separatedm w
Stream calls preserve current locale, errno identity and lifecycle inventory. Only the selected FILE's state may change. Shared native metadata still needs the independent memory frame, not disjoint locks.
libc_stdoutw′ = libc_stdoutw
∧
libc_stderrw′ = libc_stderrw
∧
libc_localefstw′ = libc_localefstw
∧
libc_errnofstw′ = libc_errnofstw
∧
shutdown_atsndw′ = shutdown_atsndw
∧
shutdown_statussndw′ = shutdown_statussndw
∧
shutdown_pendingsndw′ = shutdown_pendingsndw
∧
shutdown_consumedsndw′ = shutdown_consumedsndw
∧
→
else
libc_stdout_filelibc_streamsfstw′ = libc_stdout_filelibc_streamsfstw ∧ stdout_usablelibc_stdiofstw′ = stdout_usablelibc_stdiofstw ∧ shutdown_stdoutsndw′ = shutdown_stdoutsndw
Concrete projections, with only native allocation policy and wide settlement remaining realization parameters. Wide conversion needs its own effects/representation witness even if settlement succeeds.
mkStreamModellibc_world libc_stream_at libc_stream_state libc_stream_readyrep libc_stream_sources libc_stream_writes libc_stream_aux_roots libc_stream_releases λw p align size ⇒ ∃file, libc_file_atw p = Somefile ∧ requestsw p align size libc_stream_frame wide
Reached ordinary entries. The fallback composes with the remaining libc registry; it cannot override these six actual plain symbols.
177Definition libc_stream_registryrep requests wide fallback : name → optioncontractlibc_world symbol : name : optioncontractlibc_world ≔
else
fallbacksymbol
Lookup laws are definitional, independent of the fallback registry.
∀ rep requests wide fallback
registryTAtom"ferror" = Someferror_contractmodel ∧ registryTAtom"__fpending" = Somefpending_contractmodel ∧ registryTAtom"fclose" = Somefclose_contractmodel ∧ registryTAtom"printf" = Someprintf_contractmodel libc_stdout ∧ registryTAtom"fprintf" = Somefprintf_contractmodel ∧ registryTAtom"fputs" = Somefputs_contractmodel
Explore proof 2 tactics
Initial goal
⊢
∀ rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop fallback : name → optioncontractlibc_world ,
registryTAtom"ferror" = Someferror_contractmodel ∧ registryTAtom"__fpending" = Somefpending_contractmodel ∧ registryTAtom"fclose" = Somefclose_contractmodel ∧ registryTAtom"printf" = Someprintf_contractmodel libc_stdout ∧ registryTAtom"fprintf" = Somefprintf_contractmodel ∧ registryTAtom"fputs" = Somefputs_contractmodel
intros
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
fallback :
name → optioncontractlibc_world
model :=
libc_stream_modelrep requests wide : stream_modellibc_world
registry :=
libc_stream_registryrep requests wide fallback : name → optioncontractlibc_world
⊢
registryTAtom"ferror" = Someferror_contractmodel ∧ registryTAtom"__fpending" = Somefpending_contractmodel ∧ registryTAtom"fclose" = Somefclose_contractmodel ∧ registryTAtom"printf" = Someprintf_contractmodel libc_stdout ∧ registryTAtom"fprintf" = Somefprintf_contractmodel ∧ registryTAtom"fputs" = Somefputs_contractmodel
repeat split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
repeat split ; reflexivity
Exact comparison accepts a retained handle with its own capability.
Explore proof 5 tactics
Initial goal
intros a c
unfold same_file
simpl
rewrite Z.eqb_refl
destruct c ; simpl ; try apply Z.eqb_refl ; try apply term_eqb_refl ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros a c
unfold same_file
simpl
rewrite Z.eqb_refl
destruct c ; simpl ; try apply Z.eqb_refl ; try apply term_eqb_refl ; reflexivity
Stdout always projects the authoritative shutdown protocol, closed or open; there is no pre-close snapshot to restore.
∀ w
Explore proof 4 tactics
Initial goal
⊢
∀w : libc_world, libc_stream_statew libc_stdoutw = shutdown_stdoutsndw
intros
w :
⊢
unfold libc_stream_state
rewrite same_file_refl
w :
⊢
shutdown_stdoutsndw = shutdown_stdoutsndw
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A forged capability at the very same address is not the FILE.
∀ w a
same_filemkPtra CNone libc_stdoutw = false
same_filemkPtra CNone libc_stderrw = false
libc_stream_atw mkPtra CNone = None
Explore proof 4 tactics
Initial goal
⊢
∀w : libc_world a : Z, same_fileptr_addr ≔ a; ptr_cap ≔ CNone libc_stdoutw = false → same_fileptr_addr ≔ a; ptr_cap ≔ CNone libc_stderrw = false → libc_stream_atw ptr_addr ≔ a; ptr_cap ≔ CNone = None
intros w a Ho He
w :
a :
Z
Ho :
same_fileptr_addr ≔ a; ptr_cap ≔ CNone libc_stdoutw = false
He :
same_fileptr_addr ≔ a; ptr_cap ≔ CNone libc_stderrw = false
⊢
libc_stream_atw ptr_addr ≔ a; ptr_cap ≔ CNone = None
unfold libc_stream_at , libc_file_at
w :
a :
Z
Ho :
same_fileptr_addr ≔ a; ptr_cap ≔ CNone libc_stdoutw = false
He :
same_fileptr_addr ≔ a; ptr_cap ≔ CNone libc_stderrw = false
⊢
match if same_fileptr_addr ≔ a; ptr_cap ≔ CNone libc_stdoutw then if stdout_usablelibc_stdiofstw then Somelibc_stdout_filelibc_streamsfstw else None else if same_fileptr_addr ≔ a; ptr_cap ≔ CNone libc_stderrw then if libc_stderr_openlibc_streamsfstw then Somelibc_stderr_filelibc_streamsfstw else None else None with
Somefile
⇒
Somestream_identifier ≔ if same_fileptr_addr ≔ a; ptr_cap ≔ CNone libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew ptr_addr ≔ a; ptr_cap ≔ CNone; stream_pending ≔ file_pendingfile
None
⇒
None
=
None
rewrite Ho , He
w :
a :
Z
Ho :
same_fileptr_addr ≔ a; ptr_cap ≔ CNone libc_stdoutw = false
He :
same_fileptr_addr ≔ a; ptr_cap ≔ CNone libc_stderrw = false
⊢
None = None
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An active selected FILE has the structural representation obligations of its own inventory entry, not those of a sibling handle.
∀ rep m w p file
libc_stream_readyrep m w
libc_file_atw p = Somefile
libc_file_readym libc_errnofstw file
Explore proof 3 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop m : mem w : libc_world p : ptr file : libc_file, libc_stream_readyrep m w → libc_file_atw p = Somefile → libc_file_readym libc_errnofstw file
intros rep m w p file _ & _ & _ & _ & _ & _ & _ & _ & _ & _ & Hro & Hre & _ Hfile
rep :
mem → libc_world → Prop
m :
w :
p :
file :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hfile :
libc_file_atw p = Somefile
⊢
libc_file_readym libc_errnofstw file
unfold libc_file_at in Hfile
rep :
mem → libc_world → Prop
m :
w :
p :
file :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hfile :
→
else
None
else
None
=
Somefile
⊢
libc_file_readym libc_errnofstw file
destruct same_filep libc_stdoutw ; destruct stdout_usablelibc_stdiofstw eqn: Ho | destruct same_filep libc_stderrw ; destruct libc_stderr_openlibc_streamsfstw eqn: He | ; try discriminate ; injection Hfile as ← ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep m w p file _ & _ & _ & _ & _ & _ & _ & _ & _ & _ & Hro & Hre & _ Hfile
unfold libc_file_at in Hfile
destruct same_filep libc_stdoutw ; destruct stdout_usablelibc_stdiofstw eqn: Ho | destruct same_filep libc_stderrw ; destruct libc_stderr_openlibc_streamsfstw eqn: He | ; try discriminate ; injection Hfile as ← ; auto
Admission follows from represented endpoint structure and an active exact handle; no output success or chosen query result is assumed.
∀ rep requests wide m w p file
libc_stream_readyrep m w
libc_file_atw p = Somefile
∃info, stream_openlibc_stream_modelrep requests wide m w p info
Explore proof 23 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop m : mem w : libc_world p : ptr file : libc_file, libc_stream_readyrep m w → libc_file_atw p = Somefile → ∃info : stream_info, stream_openlibc_stream_modelrep requests wide m w p info
intros rep requests wide m w p file Hready Hfile
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
⊢
∃info : stream_info, stream_openlibc_stream_modelrep requests wide m w p info
pose proof Hready as _ & _ & Herrno & Hout & Herr & _ & _ & _ & _ & _ & Hro & Hre & _
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
⊢
∃info : stream_info, stream_openlibc_stream_modelrep requests wide m w p info
pose proof libc_file_at_readyrep m w p file Hready Hfile as Hfile_ready
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hfile_ready :
libc_file_readym libc_errnofstw file
⊢
∃info : stream_info, stream_openlibc_stream_modelrep requests wide m w p info
destruct Hfile_ready as _ & _ & Hpending & Hroots & _
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
∃info : stream_info, stream_openlibc_stream_modelrep requests wide m w p info
exists mkStreamInfoif same_filep libc_stdoutw then 1 else 2 libc_stream_statew p file_pendingfile
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
stream_openlibc_stream_modelrep requests wide m w p stream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile
split ; exact Hready |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
stream_atlibc_stream_modelrep requests wide w p = Somestream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile ∧ stream_protocolstream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile = stream_state_atlibc_stream_modelrep requests wide w p ∧ stream_info_wfstream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile ∧ Forallwritable_spanm stream_writeslibc_stream_modelrep requests wide w p
split
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
stream_atlibc_stream_modelrep requests wide w p = Somestream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile
focused goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
stream_protocolstream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile = stream_state_atlibc_stream_modelrep requests wide w p ∧ stream_info_wfstream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile ∧ Forallwritable_spanm stream_writeslibc_stream_modelrep requests wide w p
–unfold stream_at , libc_stream_model , libc_stream_at
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
Somefile0
⇒
Somestream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile0
None
⇒
None
=
Somestream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
stream_protocolstream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile = stream_state_atlibc_stream_modelrep requests wide w p ∧ stream_info_wfstream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile ∧ Forallwritable_spanm stream_writeslibc_stream_modelrep requests wide w p
rewrite Hfile
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
Somestream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile = Somestream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
stream_protocolstream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile = stream_state_atlibc_stream_modelrep requests wide w p ∧ stream_info_wfstream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile ∧ Forallwritable_spanm stream_writeslibc_stream_modelrep requests wide w p
reflexivity
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
stream_protocolstream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile = stream_state_atlibc_stream_modelrep requests wide w p ∧ stream_info_wfstream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile ∧ Forallwritable_spanm stream_writeslibc_stream_modelrep requests wide w p
–split ; reflexivity |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
stream_info_wfstream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile ∧ Forallwritable_spanm stream_writeslibc_stream_modelrep requests wide w p
split
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
stream_info_wfstream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile
focused goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
Forallwritable_spanm stream_writeslibc_stream_modelrep requests wide w p
+split ; | exact Hpending
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
stream_wfstream_protocolstream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
Forallwritable_spanm stream_writeslibc_stream_modelrep requests wide w p
unfold libc_stream_state
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
stream_wfstream_protocolstream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ if same_filep libc_stdoutw then shutdown_stdoutsndw else if same_filep libc_stderrw then libc_stderr_statelibc_streamsfstw else stdout_initial; stream_pending ≔ file_pendingfile
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
Forallwritable_spanm stream_writeslibc_stream_modelrep requests wide w p
destruct same_filep libc_stdoutw ; exact Hout |
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
stream_wfstream_protocolstream_identifier ≔ 2; stream_protocol ≔ if same_filep libc_stderrw then libc_stderr_statelibc_streamsfstw else stdout_initial; stream_pending ≔ file_pendingfile
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
Forallwritable_spanm stream_writeslibc_stream_modelrep requests wide w p
destruct same_filep libc_stderrw eqn: He ; exact Herr |
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
He :
same_filep libc_stderrw = false
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
Forallwritable_spanm stream_writeslibc_stream_modelrep requests wide w p
apply stdout_initial_wf
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
Forallwritable_spanm stream_writeslibc_stream_modelrep requests wide w p
+change Forallwritable_spanm libc_stream_writesw p
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
Forallwritable_spanm libc_stream_writesw p
unfold libc_stream_writes
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
Forallwritable_spanm
None
⇒
[ ]
rewrite Hfile
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
Forallwritable_spanm file_rootsfile ++ span_ptr ≔ libc_errnofstw; span_size ≔ 4
apply Forall_app
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
Forallwritable_spanm file_rootsfile ∧ Forallwritable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
split ; exact Hroots |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
Hready :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hpending :
0 ≤ file_pendingfile < 2 ^ 64
Hroots :
Forallwritable_spanm file_rootsfile
⊢
Forallwritable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
constructor ; exact proj1proj2Herrno | constructor
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide m w p file Hready Hfile
pose proof Hready as _ & _ & Herrno & Hout & Herr & _ & _ & _ & _ & _ & Hro & Hre & _
pose proof libc_file_at_readyrep m w p file Hready Hfile as Hfile_ready
destruct Hfile_ready as _ & _ & Hpending & Hroots & _
exists mkStreamInfoif same_filep libc_stdoutw then 1 else 2 libc_stream_statew p file_pendingfile
split ; exact Hready |
split
–split ; reflexivity |
split
+split ; | exact Hpending
unfold libc_stream_state
destruct same_filep libc_stdoutw ; exact Hout |
destruct same_filep libc_stderrw eqn: He ; exact Herr |
apply stdout_initial_wf
+change Forallwritable_spanm libc_stream_writesw p
unfold libc_stream_writes
rewrite Hfile
apply Forall_app
split ; exact Hroots |
constructor ; exact proj1proj2Herrno | constructor
Query/close admission is shared and independent of their outcomes.
∀ rep requests wide m w p file
libc_stream_readyrep m w
libc_file_atw p = Somefile
stream_call_prelibc_stream_modelrep requests wide WPtrp m w
Explore proof 4 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop m : mem w : libc_world p : ptr file : libc_file, libc_stream_readyrep m w → libc_file_atw p = Somefile → stream_call_prelibc_stream_modelrep requests wide WPtrp m w
intros
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
H :
libc_stream_readyrep m w
H0 :
libc_file_atw p = Somefile
⊢
stream_call_prelibc_stream_modelrep requests wide WPtrp m w
destruct libc_stream_openrep requests wide m w p file H H0 as info Ho
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
H :
libc_stream_readyrep m w
H0 :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
stream_call_prelibc_stream_modelrep requests wide WPtrp m w
exists p, info
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
H :
libc_stream_readyrep m w
H0 :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
WPtrp = WPtrp ∧ stream_openlibc_stream_modelrep requests wide m w p info
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Narrow literal/vararg interpretation is separate from the selected FILE representation. All errors and partial acceptance stay admitted.
∀ rep requests wide api xs m w file bytes
libc_stream_readyrep m w
libc_file_atw output_targetapi libc_stdout w xs = Somefile
output_textapi m xs bytes
output_preapi libc_stream_modelrep requests wide libc_stdout xs m w
Explore proof 7 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop api : narrow_api xs : listword m : mem w : libc_world file : libc_file bytes : listZ, libc_stream_readyrep m w → libc_file_atw output_targetapi libc_stdout w xs = Somefile → orientationlibc_stream_statew output_targetapi libc_stdout w xs ≠ WideOriented → output_textapi m xs bytes → output_preapi libc_stream_modelrep requests wide libc_stdout xs m w
intros rep requests wide api xs m w file bytes Hr Hfile Ho Htext
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
xs :
listword
m :
w :
file :
bytes :
listZ
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw output_targetapi libc_stdout w xs = Somefile
Ho :
Htext :
output_textapi m xs bytes
⊢
output_preapi libc_stream_modelrep requests wide libc_stdout xs m w
destruct libc_stream_openrep requests wide m w _ file Hr Hfile as info Hopen
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
xs :
listword
m :
w :
file :
bytes :
listZ
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw output_targetapi libc_stdout w xs = Somefile
Ho :
Htext :
output_textapi m xs bytes
info :
Hopen :
stream_openlibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs info
⊢
output_preapi libc_stream_modelrep requests wide libc_stdout xs m w
exists info, bytes
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
xs :
listword
m :
w :
file :
bytes :
listZ
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw output_targetapi libc_stdout w xs = Somefile
Ho :
Htext :
output_textapi m xs bytes
info :
Hopen :
stream_openlibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs info
⊢
stream_openlibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs info ∧ orientationstream_protocolinfo ≠ WideOriented ∧ output_textapi m xs bytes
split ; exact Hopen |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
xs :
listword
m :
w :
file :
bytes :
listZ
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw output_targetapi libc_stdout w xs = Somefile
Ho :
Htext :
output_textapi m xs bytes
info :
Hopen :
stream_openlibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs info
⊢
orientationstream_protocolinfo ≠ WideOriented ∧ output_textapi m xs bytes
destruct Hopen as _ & _ & Hstate & _
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
xs :
listword
m :
w :
file :
bytes :
listZ
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw output_targetapi libc_stdout w xs = Somefile
Ho :
Htext :
output_textapi m xs bytes
info :
Hstate :
stream_protocolinfo = stream_state_atlibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs
⊢
orientationstream_protocolinfo ≠ WideOriented ∧ output_textapi m xs bytes
rewrite Hstate
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
xs :
listword
m :
w :
file :
bytes :
listZ
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw output_targetapi libc_stdout w xs = Somefile
Ho :
Htext :
output_textapi m xs bytes
info :
Hstate :
stream_protocolinfo = stream_state_atlibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs
⊢
orientationstream_state_atlibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs ≠ WideOriented ∧ output_textapi m xs bytes
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide api xs m w file bytes Hr Hfile Ho Htext
destruct libc_stream_openrep requests wide m w _ file Hr Hfile as info Hopen
exists info, bytes
split ; exact Hopen |
destruct Hopen as _ & _ & Hstate & _
rewrite Hstate
auto
An unchanged active endpoint delegates its fixed scalar errno root as well as its private roots; it needs no new allocation or owner.
∀ rep requests wide m w p
libc_stream_readyrep m w
stream_delegateslibc_stream_modelrep requests wide w p [ ] m w
Proof 49 steps Qed
intros rep requests wide m w p Hr
unfold stream_delegates
split
–intros root Hin
destruct libc_file_atw p as file | eqn: Hfile
destruct libc_stream_openrep requests wide m w p file Hr Hfile as info & _ & _ & _ & _ & Hw
change Forallwritable_spanm libc_stream_writesw p in Hw
assert Hwr : writable_spanm root by rewrite Forall_forall in Hw ; exact Hwroot Hin
split
+right
left
unfold libc_stream_writes in Hin
rewrite Hfile in Hin
unfold libc_stream_sources
rewrite Hfile
apply in_app_or in Hin as Hin | Hin
∗exists root
split ; | reflexivity
apply in_or_app
left
unfold file_sources
right
apply in_or_app
right
exact Hin
∗simpl in Hin
destruct Hin as [ <-| [ ] ]
exists mkSpanlibc_errnofstw 0
split ; | reflexivity
apply in_or_app
right
simpl
auto
+intros a Ha
left
exists root
auto
The same libc errno/locale/conversion registry stays usable after closing stdout; writable retired roots are not required.
Explore proof 13 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop m : mem w : libc_world, libc_stream_readyrep m w → libc_readyrep m w
intros rep m w Hrep & Hlocale & Herrno & Hout & Herr & Hu & Hstatus & Hphase & Hdistinct & Hroots & Hro & Hre & Hrelease
rep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
libc_readyrep m w
split ; exact Hrep |
rep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
∧
Forallwritable_spanm stdio_rootslibc_stdiofstw
∧
split ; exact Hlocale |
rep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
Forallwritable_spanm stdio_rootslibc_stdiofstw
∧
split
2 openrep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
Forallwritable_spanm stdio_rootslibc_stdiofstw
focused goal
rep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
–rewrite Hroots
2 openrep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
Forallwritable_spanm libc_active_rootsw
deferred goal
rep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
unfold libc_active_roots
2 openrep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
Forallwritable_spanm
deferred goal
rep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
apply Forall_app
2 openrep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
deferred goal
rep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
split
3 openrep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
Forallwritable_spanm
else
[ ]
focused goal
rep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
Forallwritable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
deferred goal
rep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
+destruct stdout_usablelibc_stdiofstw eqn: Ho ; | constructor
3 openrep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Ho :
stdout_usablelibc_stdiofstw = true
Hro :
true = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
deferred goal
rep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
Forallwritable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
deferred goal
rep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
destruct Hroeq_refl as _ & _ & _ & Hr & _
3 openrep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Ho :
stdout_usablelibc_stdiofstw = true
Hro :
true = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
Hr :
⊢
deferred goal
rep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
Forallwritable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
deferred goal
rep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
exact Hr
2 opendeferred goal
rep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
Forallwritable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
deferred goal
rep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
+constructor ; exact proj1proj2Herrno | constructor
deferred goal
rep :
mem → libc_world → Prop
m :
w :
Hrep :
repm w
Hlocale :
locale_readyλ_ : mem _ : locale_world ⇒ True m libc_localefstw
Herrno :
errno_cellm libc_errnofstw
Hout :
Herr :
Hu :
shutdown_uniquesndw
Hstatus :
−2 ^ 31 ≤ shutdown_statussndw < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
Hroots :
Hro :
stdout_usablelibc_stdiofstw = true → libc_file_readym libc_errnofstw libc_stdout_filelibc_streamsfstw
Hre :
libc_stderr_openlibc_streamsfstw = true → libc_file_readym libc_errnofstw libc_stderr_filelibc_streamsfstw
Hrelease :
⊢
–auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep m w Hrep & Hlocale & Herrno & Hout & Herr & Hu & Hstatus & Hphase & Hdistinct & Hroots & Hro & Hre & Hrelease
split ; exact Hrep |
split ; exact Hlocale |
split
–rewrite Hroots
unfold libc_active_roots
apply Forall_app
split
+destruct stdout_usablelibc_stdiofstw eqn: Ho ; | constructor
destruct Hroeq_refl as _ & _ & _ & Hr & _
exact Hr
+constructor ; exact proj1proj2Herrno | constructor
–auto
Keeping the world unchanged is a valid logical frame.
∀ p w
libc_stream_framep w w
Explore proof 3 tactics
Initial goal
⊢
∀p : ptr w : libc_world, libc_stream_framep w w
intros
p :
w :
⊢
libc_stream_framep w w
unfold libc_stream_frame
p :
w :
⊢
∧
∧
libc_localefstw = libc_localefstw
∧
libc_errnofstw = libc_errnofstw
∧
shutdown_atsndw = shutdown_atsndw
∧
shutdown_statussndw = shutdown_statussndw
∧
shutdown_pendingsndw = shutdown_pendingsndw
∧
shutdown_consumedsndw = shutdown_consumedsndw
∧
→
else
libc_stdout_filelibc_streamsfstw = libc_stdout_filelibc_streamsfstw ∧ stdout_usablelibc_stdiofstw = stdout_usablelibc_stdiofstw ∧ shutdown_stdoutsndw = shutdown_stdoutsndw
repeat split ; destruct same_filep libc_stdoutw ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Errno is scalar-only even when its entry aux is nonempty. The frame is required at all call prefixes, including resource stops.
∀ rep requests wide m w p file m′
libc_stream_readyrep m w
libc_file_atw p = Somefile
stream_aux_framelibc_stream_modelrep requests wide m w p m′
m_auxm′ ptr_addrlibc_errnofstw = m_auxm ptr_addrlibc_errnofstw
Explore proof 20 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop m : mem w : libc_world p : ptr file : libc_file m′ : mem, libc_stream_readyrep m w → libc_file_atw p = Somefile → stream_aux_framelibc_stream_modelrep requests wide m w p m′ → m_auxm′ ptr_addrlibc_errnofstw = m_auxm ptr_addrlibc_errnofstw
intros rep requests wide m w p file m′ Hr Hfile Hframe
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
⊢
m_auxm′ ptr_addrlibc_errnofstw = m_auxm ptr_addrlibc_errnofstw
pose proof libc_file_at_readyrep m w p file Hr Hfile as _ & _ & _ & _ & _ & _ & Hapart & _
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
m_auxm′ ptr_addrlibc_errnofstw = m_auxm ptr_addrlibc_errnofstw
pose proof Hr as _ & _ & _ & Hcell & _ & _
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
m_auxm′ ptr_addrlibc_errnofstw = m_auxm ptr_addrlibc_errnofstw
apply Hframe
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
focused goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
¬write_authoritystream_aux_rootslibc_stream_modelrep requests wide w p [ ] m ptr_addrlibc_errnofstw
–eapply write_authority_in with roots := mkSpanlibc_errnofstw 4 born := [ ]
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
write_authorityspan_ptr ≔ libc_errnofstw; span_size ≔ 4 [ ] m ptr_addrlibc_errnofstw
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
¬write_authoritystream_aux_rootslibc_stream_modelrep requests wide w p [ ] m ptr_addrlibc_errnofstw
left
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
∃s : span, Ins span_ptr ≔ libc_errnofstw; span_size ≔ 4 ∧ writable_spanm s ∧ span_containss ptr_addrlibc_errnofstw
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
¬write_authoritystream_aux_rootslibc_stream_modelrep requests wide w p [ ] m ptr_addrlibc_errnofstw
exists mkSpanlibc_errnofstw 4
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
Inspan_ptr ≔ libc_errnofstw; span_size ≔ 4 span_ptr ≔ libc_errnofstw; span_size ≔ 4 ∧ writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4 ∧ span_containsspan_ptr ≔ libc_errnofstw; span_size ≔ 4 ptr_addrlibc_errnofstw
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
¬write_authoritystream_aux_rootslibc_stream_modelrep requests wide w p [ ] m ptr_addrlibc_errnofstw
split ; simpl ; auto |
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4 ∧ span_containsspan_ptr ≔ libc_errnofstw; span_size ≔ 4 ptr_addrlibc_errnofstw
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
¬write_authoritystream_aux_rootslibc_stream_modelrep requests wide w p [ ] m ptr_addrlibc_errnofstw
split ; exact Hcell |
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
span_containsspan_ptr ≔ libc_errnofstw; span_size ≔ 4 ptr_addrlibc_errnofstw
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
¬write_authoritystream_aux_rootslibc_stream_modelrep requests wide w p [ ] m ptr_addrlibc_errnofstw
unfold span_contains
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
ptr_addrspan_ptrspan_ptr ≔ libc_errnofstw; span_size ≔ 4 ≤ ptr_addrlibc_errnofstw < ptr_addrspan_ptrspan_ptr ≔ libc_errnofstw; span_size ≔ 4 + span_sizespan_ptr ≔ libc_errnofstw; span_size ≔ 4
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
¬write_authoritystream_aux_rootslibc_stream_modelrep requests wide w p [ ] m ptr_addrlibc_errnofstw
simpl
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
ptr_addrlibc_errnofstw ≤ ptr_addrlibc_errnofstw < ptr_addrlibc_errnofstw + 4
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
¬write_authoritystream_aux_rootslibc_stream_modelrep requests wide w p [ ] m ptr_addrlibc_errnofstw
lia
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
¬write_authoritystream_aux_rootslibc_stream_modelrep requests wide w p [ ] m ptr_addrlibc_errnofstw
–change ¬write_authoritylibc_stream_aux_rootsw p [ ] m ptr_addrlibc_errnofstw
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
¬write_authoritylibc_stream_aux_rootsw p [ ] m ptr_addrlibc_errnofstw
unfold libc_stream_aux_roots
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
¬write_authoritymatch libc_file_atw p with Somefile0 ⇒ file_rootsfile0 None ⇒ [ ] end [ ] m ptr_addrlibc_errnofstw
rewrite Hfile
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
⊢
¬write_authorityfile_rootsfile [ ] m ptr_addrlibc_errnofstw
intros root & Hin & _ & Ha | base & reg & & _
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hapart :
∀root : span, Inroot file_rootsfile → spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
root :
Hin :
Inroot file_rootsfile
Ha :
span_containsroot ptr_addrlibc_errnofstw
⊢
False
specialize Hapartroot Hin
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
root :
Hapart :
spans_apartroot span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hin :
Inroot file_rootsfile
Ha :
span_containsroot ptr_addrlibc_errnofstw
⊢
False
unfold spans_apart , span_contains in *
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
root :
Hapart :
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hin :
Inroot file_rootsfile
⊢
False
simpl in *
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
m :
w :
p :
file :
m′ :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
Hframe :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
root :
Hapart :
ptr_addrspan_ptrroot + span_sizeroot ≤ ptr_addrlibc_errnofstw ∨ ptr_addrlibc_errnofstw + 4 ≤ ptr_addrspan_ptrroot
Hcell :
writable_spanm span_ptr ≔ libc_errnofstw; span_size ≔ 4
Hin :
Inroot file_rootsfile
⊢
False
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide m w p file m′ Hr Hfile Hframe
pose proof libc_file_at_readyrep m w p file Hr Hfile as _ & _ & _ & _ & _ & _ & Hapart & _
pose proof Hr as _ & _ & _ & Hcell & _ & _
apply Hframe
–eapply write_authority_in with roots := mkSpanlibc_errnofstw 4 born := [ ]
left
exists mkSpanlibc_errnofstw 4
split ; simpl ; auto |
split ; exact Hcell |
unfold span_contains
simpl
lia
–change ¬write_authoritylibc_stream_aux_rootsw p [ ] m ptr_addrlibc_errnofstw
unfold libc_stream_aux_roots
rewrite Hfile
intros root & Hin & _ & Ha | base & reg & & _
specialize Hapartroot Hin
unfold spans_apart , span_contains in *
simpl in *
lia
The registry and projections use the consumer's actual machine.
A logical unchanged query has an independently admitted prefix. This is nonvacuity, not a claim that native locking changes nothing.
∀ rep requests wide p file s m w
libc_stream_readyrep m w
libc_file_atw p = Somefile
E.prefixferror_contractlibc_stream_modelrep requests wide WPtrp s m w [ ] [ ] s m w
Explore proof 11 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop p : ptr file : libc_file s : R.state m : mem w : libc_world, libc_stream_readyrep m w → libc_file_atw p = Somefile → E.prefixferror_contractlibc_stream_modelrep requests wide WPtrp s m w [ ] [ ] s m w
intros rep requests wide p file s m w Hr Hfile
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
p :
file :
s :
R.state
m :
w :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
⊢
E.prefixferror_contractlibc_stream_modelrep requests wide WPtrp s m w [ ] [ ] s m w
destruct libc_stream_openrep requests wide m w p file Hr Hfile as info Ho
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
p :
file :
s :
R.state
m :
w :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
E.prefixferror_contractlibc_stream_modelrep requests wide WPtrp s m w [ ] [ ] s m w
split ; constructor |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
p :
file :
s :
R.state
m :
w :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
contract_prefixferror_contractlibc_stream_modelrep requests wide WPtrp m w [ ] [ ] m w
exists p, info
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
p :
file :
s :
R.state
m :
w :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
WPtrp = WPtrp ∧ stream_atlibc_stream_modelrep requests wide w p = Someinfo ∧ stream_openlibc_stream_modelrep requests wide m w p info ∧ stream_framelibc_stream_modelrep requests wide p w w ∧ stream_delegateslibc_stream_modelrep requests wide w p [ ] m w ∧ [ ] = [ ] ∧ stream_aux_framelibc_stream_modelrep requests wide m w p m ∧ ∀a : Z, in_objectm a → ¬write_authoritystream_aux_rootslibc_stream_modelrep requests wide w p [ ] m a → m_bytesm a = m_bytesm a
split ; reflexivity |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
p :
file :
s :
R.state
m :
w :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
stream_atlibc_stream_modelrep requests wide w p = Someinfo ∧ stream_openlibc_stream_modelrep requests wide m w p info ∧ stream_framelibc_stream_modelrep requests wide p w w ∧ stream_delegateslibc_stream_modelrep requests wide w p [ ] m w ∧ [ ] = [ ] ∧ stream_aux_framelibc_stream_modelrep requests wide m w p m ∧ ∀a : Z, in_objectm a → ¬write_authoritystream_aux_rootslibc_stream_modelrep requests wide w p [ ] m a → m_bytesm a = m_bytesm a
split ; exact proj1proj2Ho |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
p :
file :
s :
R.state
m :
w :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
stream_openlibc_stream_modelrep requests wide m w p info ∧ stream_framelibc_stream_modelrep requests wide p w w ∧ stream_delegateslibc_stream_modelrep requests wide w p [ ] m w ∧ [ ] = [ ] ∧ stream_aux_framelibc_stream_modelrep requests wide m w p m ∧ ∀a : Z, in_objectm a → ¬write_authoritystream_aux_rootslibc_stream_modelrep requests wide w p [ ] m a → m_bytesm a = m_bytesm a
split ; exact Ho |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
p :
file :
s :
R.state
m :
w :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
stream_framelibc_stream_modelrep requests wide p w w ∧ stream_delegateslibc_stream_modelrep requests wide w p [ ] m w ∧ [ ] = [ ] ∧ stream_aux_framelibc_stream_modelrep requests wide m w p m ∧ ∀a : Z, in_objectm a → ¬write_authoritystream_aux_rootslibc_stream_modelrep requests wide w p [ ] m a → m_bytesm a = m_bytesm a
split ; apply libc_stream_frame_refl |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
p :
file :
s :
R.state
m :
w :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
stream_delegateslibc_stream_modelrep requests wide w p [ ] m w ∧ [ ] = [ ] ∧ stream_aux_framelibc_stream_modelrep requests wide m w p m ∧ ∀a : Z, in_objectm a → ¬write_authoritystream_aux_rootslibc_stream_modelrep requests wide w p [ ] m a → m_bytesm a = m_bytesm a
split ; apply libc_stream_delegates_refl ; exact Hr |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
p :
file :
s :
R.state
m :
w :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
[ ] = [ ] ∧ stream_aux_framelibc_stream_modelrep requests wide m w p m ∧ ∀a : Z, in_objectm a → ¬write_authoritystream_aux_rootslibc_stream_modelrep requests wide w p [ ] m a → m_bytesm a = m_bytesm a
split ; reflexivity |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
p :
file :
s :
R.state
m :
w :
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
stream_aux_framelibc_stream_modelrep requests wide m w p m ∧ ∀a : Z, in_objectm a → ¬write_authoritystream_aux_rootslibc_stream_modelrep requests wide w p [ ] m a → m_bytesm a = m_bytesm a
split ; unfold stream_aux_frame | ; intros ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide p file s m w Hr Hfile
destruct libc_stream_openrep requests wide m w p file Hr Hfile as info Ho
split ; constructor |
exists p, info
split ; reflexivity |
split ; exact proj1proj2Ho |
split ; exact Ho |
split ; apply libc_stream_frame_refl |
split ; apply libc_stream_delegates_refl ; exact Hr |
split ; reflexivity |
split ; unfold stream_aux_frame | ; intros ; reflexivity
The concrete ferror query admits either sticky-error value without assuming that the caller sees a successful output history.
∀ rep requests wide r args p file s m w
E.invokeferror_contractlibc_stream_modelrep requests wide r args WPtrp s m w [ ] CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0 s m w
Explore proof 19 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop r : call_result args : listarg p : ptr file : libc_file s : R.state m : mem w : libc_world, stream_query_abiW r args → libc_stream_readyrep m w → libc_file_atw p = Somefile → E.invokeferror_contractlibc_stream_modelrep requests wide r args WPtrp s m w [ ] CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0 s m w
intros rep requests wide r args p file s m w Habi Hr Hfile
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
⊢
E.invokeferror_contractlibc_stream_modelrep requests wide r args WPtrp s m w [ ] CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0 s m w
destruct libc_stream_openrep requests wide m w p file Hr Hfile as info Ho
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
E.invokeferror_contractlibc_stream_modelrep requests wide r args WPtrp s m w [ ] CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0 s m w
eapply S.ferror_return with born := [ ]
4 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
stream_query_abiW r args
focused goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
stream_call_prelibc_stream_modelrep requests wide WPtrp m w
focused goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
S.E.prefixferror_contractlibc_stream_modelrep requests wide WPtrp s m w [ ] [ ] s m w
focused goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
ferror_postlibc_stream_modelrep requests wide WPtrp m w [ ] [ ] CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0 m w
–exact Habi
3 opendeferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
stream_call_prelibc_stream_modelrep requests wide WPtrp m w
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
S.E.prefixferror_contractlibc_stream_modelrep requests wide WPtrp s m w [ ] [ ] s m w
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
ferror_postlibc_stream_modelrep requests wide WPtrp m w [ ] [ ] CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0 m w
–exists p, info
3 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
WPtrp = WPtrp ∧ stream_openlibc_stream_modelrep requests wide m w p info
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
S.E.prefixferror_contractlibc_stream_modelrep requests wide WPtrp s m w [ ] [ ] s m w
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
ferror_postlibc_stream_modelrep requests wide WPtrp m w [ ] [ ] CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0 m w
auto
2 opendeferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
S.E.prefixferror_contractlibc_stream_modelrep requests wide WPtrp s m w [ ] [ ] s m w
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
ferror_postlibc_stream_modelrep requests wide WPtrp m w [ ] [ ] CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0 m w
–eapply query_unchanged_prefix ; eauto
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
ferror_postlibc_stream_modelrep requests wide WPtrp m w [ ] [ ] CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0 m w
–exists p, info, if stream_errorlibc_stream_statew p then 1 else 0
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
∧
stream_atlibc_stream_modelrep requests wide w p = Someinfo
∧
stream_openlibc_stream_modelrep requests wide m w p info
∧
stream_framelibc_stream_modelrep requests wide p w w
∧
stream_delegateslibc_stream_modelrep requests wide w p [ ] m w
∧
[ ] = [ ]
∧
CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0 = CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0
∧
0 ≤ if stream_errorlibc_stream_statew p then 1 else 0 < 2 ^ 32
∧
split ; reflexivity |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
stream_atlibc_stream_modelrep requests wide w p = Someinfo
∧
stream_openlibc_stream_modelrep requests wide m w p info
∧
stream_framelibc_stream_modelrep requests wide p w w
∧
stream_delegateslibc_stream_modelrep requests wide w p [ ] m w
∧
[ ] = [ ]
∧
CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0 = CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0
∧
0 ≤ if stream_errorlibc_stream_statew p then 1 else 0 < 2 ^ 32
∧
split ; exact proj1proj2Ho |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
stream_openlibc_stream_modelrep requests wide m w p info
∧
stream_framelibc_stream_modelrep requests wide p w w
∧
stream_delegateslibc_stream_modelrep requests wide w p [ ] m w
∧
[ ] = [ ]
∧
CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0 = CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0
∧
0 ≤ if stream_errorlibc_stream_statew p then 1 else 0 < 2 ^ 32
∧
split ; exact Ho |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
stream_framelibc_stream_modelrep requests wide p w w
∧
stream_delegateslibc_stream_modelrep requests wide w p [ ] m w
∧
[ ] = [ ]
∧
CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0 = CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0
∧
0 ≤ if stream_errorlibc_stream_statew p then 1 else 0 < 2 ^ 32
∧
split ; apply libc_stream_frame_refl |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
stream_delegateslibc_stream_modelrep requests wide w p [ ] m w
∧
[ ] = [ ]
∧
CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0 = CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0
∧
0 ≤ if stream_errorlibc_stream_statew p then 1 else 0 < 2 ^ 32
∧
split ; apply libc_stream_delegates_refl ; exact Hr |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
[ ] = [ ]
∧
CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0 = CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0
∧
0 ≤ if stream_errorlibc_stream_statew p then 1 else 0 < 2 ^ 32
∧
split ; reflexivity |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0 = CallReturnWIntif stream_errorlibc_stream_statew p then 1 else 0
∧
0 ≤ if stream_errorlibc_stream_statew p then 1 else 0 < 2 ^ 32
∧
split ; reflexivity |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Ho :
stream_openlibc_stream_modelrep requests wide m w p info
⊢
0 ≤ if stream_errorlibc_stream_statew p then 1 else 0 < 2 ^ 32
∧
destruct Ho as _ & _ & Hstate & _
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Hstate :
stream_protocolinfo = stream_state_atlibc_stream_modelrep requests wide w p
⊢
0 ≤ if stream_errorlibc_stream_statew p then 1 else 0 < 2 ^ 32
∧
rewrite Hstate
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Hstate :
stream_protocolinfo = stream_state_atlibc_stream_modelrep requests wide w p
⊢
0 ≤ if stream_errorlibc_stream_statew p then 1 else 0 < 2 ^ 32
∧
↔
stream_errorstream_state_atlibc_stream_modelrep requests wide w p = false
cbn [ stream_state_at libc_stream_model ]
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
file :
s :
R.state
m :
w :
Habi :
stream_query_abiW r args
Hr :
libc_stream_readyrep m w
Hfile :
libc_file_atw p = Somefile
info :
Hstate :
stream_protocolinfo = stream_state_atlibc_stream_modelrep requests wide w p
⊢
0 ≤ if stream_errorlibc_stream_statew p then 1 else 0 < 2 ^ 32
∧
destruct stream_errorlibc_stream_statew p ; split ; lia | split ; congruence | lia | split ; congruence
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide r args p file s m w Habi Hr Hfile
destruct libc_stream_openrep requests wide m w p file Hr Hfile as info Ho
eapply S.ferror_return with born := [ ]
–exact Habi
–exists p, info
auto
–eapply query_unchanged_prefix ; eauto
–exists p, info, if stream_errorlibc_stream_statew p then 1 else 0
split ; reflexivity |
split ; exact proj1proj2Ho |
split ; exact Ho |
split ; apply libc_stream_frame_refl |
split ; apply libc_stream_delegates_refl ; exact Hr |
split ; reflexivity |
split ; reflexivity |
destruct Ho as _ & _ & Hstate & _
rewrite Hstate
cbn [ stream_state_at libc_stream_model ]
destruct stream_errorlibc_stream_statew p ; split ; lia | split ; congruence | lia | split ; congruence
Physical pending, not the logical FIFO length, is the query result.
∀ rep requests wide r args p file s m w
E.invokefpending_contractlibc_stream_modelrep requests wide r args WPtrp s m w [ ] CallReturnWIntfile_pendingfile s m w
Proof 40 steps Qed
intros rep requests wide r args p file s m w Habi Hr Hfile
destruct libc_stream_openrep requests wide m w p file Hr Hfile as info Ho
assert Hpending : stream_pendinginfo = file_pendingfile
{destruct Ho as _ & Hinfo & _
change libc_stream_atw p = Someinfo in Hinfo
unfold libc_stream_at in Hinfo
rewrite Hfile in Hinfo
injection Hinfo as ←
reflexivity
assert Hrange : 0 ≤ file_pendingfile < 2 ^ 64
{destruct Ho as _ & _ & _ & _ Hrange & _
rewrite Hpending in Hrange
exact Hrange
eapply E.invoke_normal with born := [ ]
–exact Habi
–exists p, info
auto
–exact query_unchanged_prefixrep requests wide p file s m w Hr Hfile
–exists p, info
split ; reflexivity |
split ; exact proj1proj2Ho |
split ; exact Ho |
split ; apply libc_stream_frame_refl |
split ; apply libc_stream_delegates_refl ; exact Hr |
split ; reflexivity |
rewrite Hpending
reflexivity
–intros why Hbad
discriminate
–intros values Hvalues
injection Hvalues as ←
split
+exists WIntfile_pendingfile
split ; reflexivity |
simpl
rewrite Z.mod_small by exact Hrange
reflexivity
+constructor ; exact I | constructor
–intros status Hbad
discriminate
The old exact errno lookup is still admitted with closed stdout.
∀ rep r args s m w
errno_location_abir args
libc_stream_readyrep m w
E.invokeC.errno_contractrep r args [ ] s m w [ ] CallReturnWPtrlibc_errnofstw s m w
Explore proof 4 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop r : call_result args : listarg s : R.state m : mem w : libc_world, errno_location_abir args → libc_stream_readyrep m w → E.invokeC.errno_contractrep r args [ ] s m w [ ] CallReturnWPtrlibc_errnofstw s m w
intros
rep :
mem → libc_world → Prop
r :
args :
listarg
s :
R.state
m :
w :
H :
errno_location_abir args
H0 :
libc_stream_readyrep m w
⊢
E.invokeC.errno_contractrep r args [ ] s m w [ ] CallReturnWPtrlibc_errnofstw s m w
apply C.errno_admitted ; exact H |
rep :
mem → libc_world → Prop
r :
args :
listarg
s :
R.state
m :
w :
H :
errno_location_abir args
H0 :
libc_stream_readyrep m w
⊢
libc_readyrep m w
apply libc_stream_ready_libc
rep :
mem → libc_world → Prop
r :
args :
listarg
s :
R.state
m :
w :
H :
errno_location_abir args
H0 :
libc_stream_readyrep m w
⊢
libc_stream_readyrep m w
exact H0
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Returning and resource-ending output expose the same represented world/frame/provenance cutpoint. Normal-result facts are separate.
∀ rep requests wide api r args xs s m w trace ending s′ m′ w′
E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
libc_stream_readyrep m′ w′ ∧ libc_stream_frameoutput_targetapi libc_stdout w xs w w′ ∧ ∃born, stream_delegateslibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs born m′ w′ ∧ stream_aux_framelibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs m′
Explore proof 6 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop api : narrow_api r : call_result args : listarg xs : listword s : R.state m : mem w : libc_world trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′ → libc_stream_readyrep m′ w′ ∧ libc_stream_frameoutput_targetapi libc_stdout w xs w w′ ∧ ∃born : listZ, stream_delegateslibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs born m′ w′ ∧ stream_aux_framelibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs m′
intros rep requests wide api r args xs s m w trace ending s′ m′ w′ Hcall
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
⊢
libc_stream_readyrep m′ w′ ∧ libc_stream_frameoutput_targetapi libc_stdout w xs w w′ ∧ ∃born : listZ, stream_delegateslibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs born m′ w′ ∧ stream_aux_framelibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs m′
destruct E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & He & info & info′ & bytes & actions & tail & Hinfo & Htext & Hbytes & Hrun & Hopen & Hid & Hframe & Hdelegate & Htrace & Haux
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
He :
E.effectscontract_sourcesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w contract_writesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w contract_releasesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w contract_requestsoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w s m [ ] s′ m′ born
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
stream_atlibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hopen :
stream_openlibc_stream_modelrep requests wide m′ w′ output_targetapi libc_stdout w xs info′
Hid :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
Hdelegate :
stream_delegateslibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs born m′ w′
Htrace :
trace = [ ] ∧ acceptedactions = [ ] ∨ trace = StreamBytesstream_identifierinfo acceptedactions
Haux :
stream_aux_framelibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs m′
⊢
libc_stream_readyrep m′ w′ ∧ libc_stream_frameoutput_targetapi libc_stdout w xs w w′ ∧ ∃born0 : listZ, stream_delegateslibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs born0 m′ w′ ∧ stream_aux_framelibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs m′
split ; exact proj1Hopen |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
He :
E.effectscontract_sourcesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w contract_writesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w contract_releasesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w contract_requestsoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w s m [ ] s′ m′ born
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
stream_atlibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hopen :
stream_openlibc_stream_modelrep requests wide m′ w′ output_targetapi libc_stdout w xs info′
Hid :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
Hdelegate :
stream_delegateslibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs born m′ w′
Htrace :
trace = [ ] ∧ acceptedactions = [ ] ∨ trace = StreamBytesstream_identifierinfo acceptedactions
Haux :
stream_aux_framelibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs m′
⊢
libc_stream_frameoutput_targetapi libc_stdout w xs w w′ ∧ ∃born0 : listZ, stream_delegateslibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs born0 m′ w′ ∧ stream_aux_framelibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs m′
split ; exact Hframe |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
He :
E.effectscontract_sourcesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w contract_writesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w contract_releasesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w contract_requestsoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w s m [ ] s′ m′ born
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
stream_atlibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hopen :
stream_openlibc_stream_modelrep requests wide m′ w′ output_targetapi libc_stdout w xs info′
Hid :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
Hdelegate :
stream_delegateslibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs born m′ w′
Htrace :
trace = [ ] ∧ acceptedactions = [ ] ∨ trace = StreamBytesstream_identifierinfo acceptedactions
Haux :
stream_aux_framelibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs m′
⊢
∃born0 : listZ, stream_delegateslibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs born0 m′ w′ ∧ stream_aux_framelibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs m′
exists born
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
He :
E.effectscontract_sourcesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w contract_writesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w contract_releasesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w contract_requestsoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w s m [ ] s′ m′ born
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
stream_atlibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hopen :
stream_openlibc_stream_modelrep requests wide m′ w′ output_targetapi libc_stdout w xs info′
Hid :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
Hdelegate :
stream_delegateslibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs born m′ w′
Htrace :
trace = [ ] ∧ acceptedactions = [ ] ∨ trace = StreamBytesstream_identifierinfo acceptedactions
Haux :
stream_aux_framelibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs m′
⊢
stream_delegateslibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs born m′ w′ ∧ stream_aux_framelibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs m′
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide api r args xs s m w trace ending s′ m′ w′ Hcall
destruct E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & He & info & info′ & bytes & actions & tail & Hinfo & Htext & Hbytes & Hrun & Hopen & Hid & Hframe & Hdelegate & Htrace & Haux
split ; exact proj1Hopen |
split ; exact Hframe |
exists born
auto
Ordinary narrow output results remain canonical, including errors.
∀ rep requests wide api r args xs s m w trace values s′ m′ w′
E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace CallReturnvalues s′ m′ w′
∃result, values = WIntresult ∧ 0 ≤ result < 2 ^ 32
Explore proof 2 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop api : narrow_api r : call_result args : listarg xs : listword s : R.state m : mem w : libc_world trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace CallReturnvalues s′ m′ w′ → ∃result : Z, values = WIntresult ∧ 0 ≤ result < 2 ^ 32
intros
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace CallReturnvalues s′ m′ w′
⊢
∃result : Z, values = WIntresult ∧ 0 ≤ result < 2 ^ 32
eapply F.output_returned ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
eapply F.output_returned ; eauto
Logical controls, not a claim that these tiny objects are native FILEs. Physical pending counts deliberately differ from FIFO length.
Static handles live in separate existing fixture objects.
mkLibcFilemkPtr1024 Obj1024 7 [ ] [ ] [ ]
Stderr has a different physical count.
mkLibcFilemkPtr2048 Obj2048 3 [ ] [ ] [ ]
Close retires stdout after settling its two logical obligations; physical pending is deliberately not the FIFO length.
mkShutdownHandlers 0 [ ] [ ]
opened
→
65; 66
else
[ ]
true
Neither stream's private zero-length source exposes errno authority.
Explore proof 5 tactics
Initial goal
⊢
∀a n : Z, a ≠ 5120 → file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 file_handle ≔ ptr_addr ≔ a; ptr_cap ≔ Obja; file_pending ≔ n; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ]
intros a n Hne
a, n :
Z
Hne :
a ≠ 5120
⊢
file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 file_handle ≔ ptr_addr ≔ a; ptr_cap ≔ Obja; file_pending ≔ n; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ]
split ; intros root |
a, n :
Z
Hne :
a ≠ 5120
⊢
∀base : Z, ptr_capptr_addr ≔ 5120; ptr_cap ≔ Obj5120 = Objbase ∨ ptr_capptr_addr ≔ 5120; ptr_cap ≔ Obj5120 = Robase → ¬Inbase file_ownedfile_handle ≔ ptr_addr ≔ a; ptr_cap ≔ Obja; file_pending ≔ n; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ ¬available_capfile_sourcesfile_handle ≔ ptr_addr ≔ a; ptr_cap ≔ Obja; file_pending ≔ n; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] [ ] conversion_mem Objbase ∧ ¬available_capfile_sourcesfile_handle ≔ ptr_addr ≔ a; ptr_cap ≔ Obja; file_pending ≔ n; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] [ ] conversion_mem Robase
intros base Hbase | Hbase ; injection Hbase as <-| discriminate
a, n :
Z
Hne :
a ≠ 5120
⊢
¬In5120 file_ownedfile_handle ≔ ptr_addr ≔ a; ptr_cap ≔ Obja; file_pending ≔ n; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ ¬available_capfile_sourcesfile_handle ≔ ptr_addr ≔ a; ptr_cap ≔ Obja; file_pending ≔ n; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] [ ] conversion_mem Obj5120 ∧ ¬available_capfile_sourcesfile_handle ≔ ptr_addr ≔ a; ptr_cap ≔ Obja; file_pending ≔ n; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] [ ] conversion_mem Ro5120
split ; intros |
a, n :
Z
Hne :
a ≠ 5120
⊢
¬available_capfile_sourcesfile_handle ≔ ptr_addr ≔ a; ptr_cap ≔ Obja; file_pending ≔ n; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] [ ] conversion_mem Obj5120 ∧ ¬available_capfile_sourcesfile_handle ≔ ptr_addr ≔ a; ptr_cap ≔ Obja; file_pending ≔ n; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] [ ] conversion_mem Ro5120
split ; intros Hnone | source & Hin & Hcap | source & addr & Hin & Ha & Hsize & _ | b & & _ ; try discriminate ; simpl in Hin ; destruct Hin as [ <-| [ ] ] ; simpl in * ; congruence | unfold span_contains in Ha ; simpl in Ha ; lia | discriminate | unfold span_contains in Ha ; simpl in Ha ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros a n Hne
split ; intros root |
intros base Hbase | Hbase ; injection Hbase as <-| discriminate
split ; intros |
split ; intros Hnone | source & Hin & Hcap | source & addr & Hin & Ha & Hsize & _ | b & & _ ; try discriminate ; simpl in Hin ; destruct Hin as [ <-| [ ] ] ; simpl in * ; congruence | unfold span_contains in Ha ; simpl in Ha ; lia | discriminate | unfold span_contains in Ha ; simpl in Ha ; lia
Both represented open FILE entries satisfy their structural slice.
libc_file_readyconversion_mem mkPtr5120 Obj5120 out_file ∧ libc_file_readyconversion_mem mkPtr5120 Obj5120 err_file
Explore proof 15 tactics
Initial goal
⊢
libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 out_file ∧ libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 err_file
assert Hread : ∀a, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem mkPtra Obja 1
2 open⊢
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
focused goal
Hread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 out_file ∧ libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 err_file
{intros a → | → ; split ; simpl ; lia | | simpl ; lia |
3 open⊢
∃base : Z reg : region, ptr_capptr_addr ≔ 1024; ptr_cap ≔ Obj1024 = Objbase ∨ ptr_capptr_addr ≔ 1024; ptr_cap ≔ Obj1024 = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live ∧ access_resconversion_mem ptr_addrptr_addr ≔ 1024; ptr_cap ≔ Obj1024 ptr_capptr_addr ≔ 1024; ptr_cap ≔ Obj1024 1 Read 1 = Someok ∧ ∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrptr_addr ≔ 1024; ptr_cap ≔ Obj1024 + i < 256
focused goal
⊢
∃base : Z reg : region, ptr_capptr_addr ≔ 2048; ptr_cap ≔ Obj2048 = Objbase ∨ ptr_capptr_addr ≔ 2048; ptr_cap ≔ Obj2048 = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live ∧ access_resconversion_mem ptr_addrptr_addr ≔ 2048; ptr_cap ≔ Obj2048 ptr_capptr_addr ≔ 2048; ptr_cap ≔ Obj2048 1 Read 1 = Someok ∧ ∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrptr_addr ≔ 2048; ptr_cap ≔ Obj2048 + i < 256
deferred goal
Hread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 out_file ∧ libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 err_file
all: split
5 openfocused goal
focused goal
focused goal
deferred goal
Hread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 out_file ∧ libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 err_file
1: {exists 1024, mkRegion1024 1056 GlobalData Live
5 opendeferred goal
deferred goal
deferred goal
deferred goal
Hread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 out_file ∧ libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 err_file
auto
4 opendeferred goal
deferred goal
deferred goal
deferred goal
Hread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 out_file ∧ libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 err_file
2: {exists 2048, mkRegion2048 2056 Stack Live
4 opendeferred goal
deferred goal
deferred goal
Hread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 out_file ∧ libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 err_file
auto
3 opendeferred goal
deferred goal
deferred goal
Hread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 out_file ∧ libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 err_file
all: split ; reflexivity |
3 openfocused goal
deferred goal
Hread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 out_file ∧ libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 err_file
all: intros i Hi ; assert i = 0 as → by lia ; vm_compute ; split ; congruence
deferred goal
Hread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 out_file ∧ libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 err_file
split ; unfold out_file , err_file , libc_file_ready ; split ; discriminate | | discriminate |
2 openHread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
readable_bytesconversion_mem file_handlefile_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] 1 ∧ 0 ≤ file_pendingfile_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsfile_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsfile_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ Foralllocale_heapconversion_mem file_ownedfile_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 file_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ]
focused goal
Hread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
readable_bytesconversion_mem file_handlefile_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] 1 ∧ 0 ≤ file_pendingfile_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsfile_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsfile_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ Foralllocale_heapconversion_mem file_ownedfile_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 file_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ]
all: split ; apply Hread ; auto |
2 openHread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
0 ≤ file_pendingfile_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsfile_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsfile_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ Foralllocale_heapconversion_mem file_ownedfile_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 file_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ]
focused goal
Hread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
0 ≤ file_pendingfile_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsfile_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsfile_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ Foralllocale_heapconversion_mem file_ownedfile_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 file_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ]
all: split ; simpl ; lia |
2 openHread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
Forallwritable_spanconversion_mem file_rootsfile_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsfile_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ Foralllocale_heapconversion_mem file_ownedfile_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 file_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ]
focused goal
Hread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
Forallwritable_spanconversion_mem file_rootsfile_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsfile_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ Foralllocale_heapconversion_mem file_ownedfile_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 file_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ]
all: split ; constructor |
2 openHread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsfile_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ Foralllocale_heapconversion_mem file_ownedfile_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 file_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ]
focused goal
Hread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsfile_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ Foralllocale_heapconversion_mem file_ownedfile_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 file_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ]
all: split ; constructor |
2 openHread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
Foralllocale_heapconversion_mem file_ownedfile_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 file_handle ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; file_pending ≔ 7; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ]
focused goal
Hread :
∀a : Z, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem ptr_addr ≔ a; ptr_cap ≔ Obja 1
⊢
Foralllocale_heapconversion_mem file_ownedfile_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ] ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 file_handle ≔ ptr_addr ≔ 2048; ptr_cap ≔ Obj2048; file_pending ≔ 3; file_reads ≔ [ ]; file_roots ≔ [ ]; file_owned ≔ [ ]
all: split ; constructor | apply empty_file_errno ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
assert Hread : ∀a, a = 1024 ∨ a = 2048 → readable_bytesconversion_mem mkPtra Obja 1
{intros a → | → ; split ; simpl ; lia | | simpl ; lia |
all: split
1: {exists 1024, mkRegion1024 1056 GlobalData Live
auto
all: split ; reflexivity |
all: intros i Hi ; assert i = 0 as → by lia ; vm_compute ; split ; congruence
split ; unfold out_file , err_file , libc_file_ready ; split ; discriminate | | discriminate |
all: split ; apply Hread ; auto |
all: split ; simpl ; lia |
all: split ; constructor |
all: split ; constructor |
all: split ; constructor | apply empty_file_errno ; lia
Closed stdout is a nonempty represented state, not a vacuous pre.
∀ opened
libc_stream_readyλ_ _ ⇒ True conversion_mem worldopened
Explore proof 17 tactics
Initial goal
⊢
∀opened : bool, libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem worldopened
intros opened
opened :
bool
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem worldopened
pose proof proj1conversion_pre1 ltac:lia as _ & Hl & _ & He & _
opened :
bool
Hl :
locale_readyλ_ : mem _ : locale_world ⇒ True conversion_mem libc_localefstconversion_world
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem worldopened
split ; exact I |
opened :
bool
Hl :
locale_readyλ_ : mem _ : locale_world ⇒ True conversion_mem libc_localefstconversion_world
⊢
locale_readyλ_ : mem _ : locale_world ⇒ True conversion_mem libc_localefstworldopened
∧
errno_cellconversion_mem libc_errnofstworldopened
∧
stream_wfshutdown_stdoutsndworldopened
∧
∧
shutdown_uniquesndworldopened
∧
−2 ^ 31 ≤ shutdown_statussndworldopened < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutworldopened ≠ ptr_addrlibc_stderrworldopened ∧ stdio_rootslibc_stdiofstworldopened = libc_active_rootsworldopened ∧ stdout_usablelibc_stdiofstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stdout_filelibc_streamsfstworldopened ∧ libc_stderr_openlibc_streamsfstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stderr_filelibc_streamsfstworldopened ∧ libc_release_separatedconversion_mem worldopened
split ; exact Hl |
opened :
bool
Hl :
locale_readyλ_ : mem _ : locale_world ⇒ True conversion_mem libc_localefstconversion_world
⊢
errno_cellconversion_mem libc_errnofstworldopened
∧
stream_wfshutdown_stdoutsndworldopened
∧
∧
shutdown_uniquesndworldopened
∧
−2 ^ 31 ≤ shutdown_statussndworldopened < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutworldopened ≠ ptr_addrlibc_stderrworldopened ∧ stdio_rootslibc_stdiofstworldopened = libc_active_rootsworldopened ∧ stdout_usablelibc_stdiofstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stdout_filelibc_streamsfstworldopened ∧ libc_stderr_openlibc_streamsfstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stderr_filelibc_streamsfstworldopened ∧ libc_release_separatedconversion_mem worldopened
split ; exact He |
opened :
bool
Hl :
locale_readyλ_ : mem _ : locale_world ⇒ True conversion_mem libc_localefstconversion_world
⊢
stream_wfshutdown_stdoutsndworldopened
∧
∧
shutdown_uniquesndworldopened
∧
−2 ^ 31 ≤ shutdown_statussndworldopened < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutworldopened ≠ ptr_addrlibc_stderrworldopened ∧ stdio_rootslibc_stdiofstworldopened = libc_active_rootsworldopened ∧ stdout_usablelibc_stdiofstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stdout_filelibc_streamsfstworldopened ∧ libc_stderr_openlibc_streamsfstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stderr_filelibc_streamsfstworldopened ∧ libc_release_separatedconversion_mem worldopened
split ; split ; destruct opened ; repeat constructor ; lia | reflexivity |
opened :
bool
Hl :
locale_readyλ_ : mem _ : locale_world ⇒ True conversion_mem libc_localefstconversion_world
⊢
∧
shutdown_uniquesndworldopened
∧
−2 ^ 31 ≤ shutdown_statussndworldopened < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutworldopened ≠ ptr_addrlibc_stderrworldopened ∧ stdio_rootslibc_stdiofstworldopened = libc_active_rootsworldopened ∧ stdout_usablelibc_stdiofstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stdout_filelibc_streamsfstworldopened ∧ libc_stderr_openlibc_streamsfstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stderr_filelibc_streamsfstworldopened ∧ libc_release_separatedconversion_mem worldopened
split ; apply stdout_initial_wf |
opened :
bool
Hl :
locale_readyλ_ : mem _ : locale_world ⇒ True conversion_mem libc_localefstconversion_world
⊢
shutdown_uniquesndworldopened
∧
−2 ^ 31 ≤ shutdown_statussndworldopened < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutworldopened ≠ ptr_addrlibc_stderrworldopened ∧ stdio_rootslibc_stdiofstworldopened = libc_active_rootsworldopened ∧ stdout_usablelibc_stdiofstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stdout_filelibc_streamsfstworldopened ∧ libc_stderr_openlibc_streamsfstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stderr_filelibc_streamsfstworldopened ∧ libc_release_separatedconversion_mem worldopened
split ; constructor |
opened :
bool
Hl :
locale_readyλ_ : mem _ : locale_world ⇒ True conversion_mem libc_localefstconversion_world
⊢
−2 ^ 31 ≤ shutdown_statussndworldopened < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutworldopened ≠ ptr_addrlibc_stderrworldopened ∧ stdio_rootslibc_stdiofstworldopened = libc_active_rootsworldopened ∧ stdout_usablelibc_stdiofstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stdout_filelibc_streamsfstworldopened ∧ libc_stderr_openlibc_streamsfstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stderr_filelibc_streamsfstworldopened ∧ libc_release_separatedconversion_mem worldopened
split ; simpl ; lia |
opened :
bool
Hl :
locale_readyλ_ : mem _ : locale_world ⇒ True conversion_mem libc_localefstconversion_world
⊢
_
⇒
True
∧
ptr_addrlibc_stdoutworldopened ≠ ptr_addrlibc_stderrworldopened ∧ stdio_rootslibc_stdiofstworldopened = libc_active_rootsworldopened ∧ stdout_usablelibc_stdiofstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stdout_filelibc_streamsfstworldopened ∧ libc_stderr_openlibc_streamsfstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stderr_filelibc_streamsfstworldopened ∧ libc_release_separatedconversion_mem worldopened
split ; exact I |
opened :
bool
Hl :
locale_readyλ_ : mem _ : locale_world ⇒ True conversion_mem libc_localefstconversion_world
⊢
ptr_addrlibc_stdoutworldopened ≠ ptr_addrlibc_stderrworldopened ∧ stdio_rootslibc_stdiofstworldopened = libc_active_rootsworldopened ∧ stdout_usablelibc_stdiofstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stdout_filelibc_streamsfstworldopened ∧ libc_stderr_openlibc_streamsfstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stderr_filelibc_streamsfstworldopened ∧ libc_release_separatedconversion_mem worldopened
split ; simpl ; lia |
opened :
bool
Hl :
locale_readyλ_ : mem _ : locale_world ⇒ True conversion_mem libc_localefstconversion_world
⊢
stdio_rootslibc_stdiofstworldopened = libc_active_rootsworldopened ∧ stdout_usablelibc_stdiofstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stdout_filelibc_streamsfstworldopened ∧ libc_stderr_openlibc_streamsfstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stderr_filelibc_streamsfstworldopened ∧ libc_release_separatedconversion_mem worldopened
split ; destruct opened ; reflexivity |
opened :
bool
Hl :
locale_readyλ_ : mem _ : locale_world ⇒ True conversion_mem libc_localefstconversion_world
⊢
stdout_usablelibc_stdiofstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stdout_filelibc_streamsfstworldopened ∧ libc_stderr_openlibc_streamsfstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stderr_filelibc_streamsfstworldopened ∧ libc_release_separatedconversion_mem worldopened
split ; intros _ ; exact proj1files_ready |
opened :
bool
Hl :
locale_readyλ_ : mem _ : locale_world ⇒ True conversion_mem libc_localefstconversion_world
⊢
libc_stderr_openlibc_streamsfstworldopened = true → libc_file_readyconversion_mem libc_errnofstworldopened libc_stderr_filelibc_streamsfstworldopened ∧ libc_release_separatedconversion_mem worldopened
split ; intros _ ; exact proj2files_ready |
opened :
bool
Hl :
locale_readyλ_ : mem _ : locale_world ⇒ True conversion_mem libc_localefstconversion_world
intros p file Hfile base Hin
opened :
bool
Hl :
locale_readyλ_ : mem _ : locale_world ⇒ True conversion_mem libc_localefstconversion_world
p :
file :
Hfile :
libc_file_atworldopened p = Somefile
base :
Z
Hin :
Inbase file_ownedfile
⊢
¬Inbase locale_ownedlibc_localefstworldopened ∧ ∀q : ptr other : libc_file, libc_file_atworldopened q = Someother → file_handleother ≠ file_handlefile → ¬Inbase file_ownedother ∧ ¬available_capspan_ptr ≔ libc_stdoutworldopened; span_size ≔ 0 :: span_ptr ≔ libc_stderrworldopened; span_size ≔ 0 :: locale_private_sourceslibc_localefstworldopened ++ if same_filep libc_stdoutworldopened then match libc_file_atworldopened libc_stderrworldopened with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atworldopened libc_stdoutworldopened with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] conversion_mem Objbase ∧ ¬available_capspan_ptr ≔ libc_stdoutworldopened; span_size ≔ 0 :: span_ptr ≔ libc_stderrworldopened; span_size ≔ 0 :: locale_private_sourceslibc_localefstworldopened ++ if same_filep libc_stdoutworldopened then match libc_file_atworldopened libc_stderrworldopened with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atworldopened libc_stdoutworldopened with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] conversion_mem Robase
unfold libc_file_at in Hfile
opened :
bool
Hl :
locale_readyλ_ : mem _ : locale_world ⇒ True conversion_mem libc_localefstconversion_world
p :
file :
Hfile :
=
Somefile
base :
Z
Hin :
Inbase file_ownedfile
⊢
¬Inbase locale_ownedlibc_localefstworldopened ∧ ∀q : ptr other : libc_file, libc_file_atworldopened q = Someother → file_handleother ≠ file_handlefile → ¬Inbase file_ownedother ∧ ¬available_capspan_ptr ≔ libc_stdoutworldopened; span_size ≔ 0 :: span_ptr ≔ libc_stderrworldopened; span_size ≔ 0 :: locale_private_sourceslibc_localefstworldopened ++ if same_filep libc_stdoutworldopened then match libc_file_atworldopened libc_stderrworldopened with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atworldopened libc_stdoutworldopened with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] conversion_mem Objbase ∧ ¬available_capspan_ptr ≔ libc_stdoutworldopened; span_size ≔ 0 :: span_ptr ≔ libc_stderrworldopened; span_size ≔ 0 :: locale_private_sourceslibc_localefstworldopened ++ if same_filep libc_stdoutworldopened then match libc_file_atworldopened libc_stderrworldopened with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atworldopened libc_stdoutworldopened with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] conversion_mem Robase
destruct same_filep libc_stdoutworldopened ; destruct opened | destruct same_filep libc_stderrworldopened ; try discriminate ; injection Hfile as ← ; contradiction
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros opened
pose proof proj1conversion_pre1 ltac:lia as _ & Hl & _ & He & _
split ; exact I |
split ; exact Hl |
split ; exact He |
split ; split ; destruct opened ; repeat constructor ; lia | reflexivity |
split ; apply stdout_initial_wf |
split ; constructor |
split ; simpl ; lia |
split ; exact I |
split ; simpl ; lia |
split ; destruct opened ; reflexivity |
split ; intros _ ; exact proj1files_ready |
split ; intros _ ; exact proj2files_ready |
intros p file Hfile base Hin
unfold libc_file_at in Hfile
destruct same_filep libc_stdoutworldopened ; destruct opened | destruct same_filep libc_stderrworldopened ; try discriminate ; injection Hfile as ← ; contradiction
Same registered errno contract, after stdout closes, returns exactly the original capability and snapshot.
536Example closed_errno: M.E.invokeC.C.errno_contractλ_ _ ⇒ True CVoid [ ] [ ] InterpRuntime.start conversion_mem worldfalse [ ] CallReturnWPtrmkPtr5120 Obj5120 InterpRuntime.start conversion_mem worldfalse
Explore proof 1 tactics
Initial goal
⊢
M.E.invokeC.C.errno_contractλ_ : mem _ : libc_world ⇒ True CVoid [ ] [ ] InterpRuntime.start conversion_mem worldfalse [ ] CallReturnWPtrptr_addr ≔ 5120; ptr_cap ≔ Obj5120 InterpRuntime.start conversion_mem worldfalse
apply C.errno_after_close ; split ; left ; reflexivity | reflexivity | apply ready
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
apply C.errno_after_close ; split ; left ; reflexivity | reflexivity | apply ready
After stdout closes, stderr remains queryable with its own count.
544Example stderr_pending_after_close: M.E.invokefpending_contractlibc_stream_modelλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False CVoid ArgP Const0 WPtrfile_handleerr_file InterpRuntime.start conversion_mem worldfalse [ ] CallReturnWInt3 InterpRuntime.start conversion_mem worldfalse
Explore proof 6 tactics
Initial goal
⊢
M.E.invokefpending_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False CVoid ArgP Const0 WPtrfile_handleerr_file InterpRuntime.start conversion_mem worldfalse [ ] CallReturnWInt3 InterpRuntime.start conversion_mem worldfalse
apply C.fpending_unchanged with file := err_file
3 openfocused goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem worldfalse
focused goal
⊢
libc_file_atworldfalse file_handleerr_file = Someerr_file
–split ; left ; reflexivity |
3 opendeferred goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem worldfalse
deferred goal
⊢
libc_file_atworldfalse file_handleerr_file = Someerr_file
exists Const0
3 opendeferred goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem worldfalse
deferred goal
⊢
libc_file_atworldfalse file_handleerr_file = Someerr_file
reflexivity
2 opendeferred goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem worldfalse
deferred goal
⊢
libc_file_atworldfalse file_handleerr_file = Someerr_file
–apply ready
deferred goal
⊢
libc_file_atworldfalse file_handleerr_file = Someerr_file
–reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Seven physical pending bytes are not the two logical obligations.
557Example stdout_pending_not_fifo: M.E.invokefpending_contractlibc_stream_modelλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False CVoid ArgP Const0 WPtrfile_handleout_file InterpRuntime.start conversion_mem worldtrue [ ] CallReturnWInt7 InterpRuntime.start conversion_mem worldtrue
Explore proof 6 tactics
Initial goal
⊢
M.E.invokefpending_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False CVoid ArgP Const0 WPtrfile_handleout_file InterpRuntime.start conversion_mem worldtrue [ ] CallReturnWInt7 InterpRuntime.start conversion_mem worldtrue
apply C.fpending_unchanged with file := out_file
3 openfocused goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem worldtrue
focused goal
⊢
libc_file_atworldtrue file_handleout_file = Someout_file
–split ; left ; reflexivity |
3 opendeferred goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem worldtrue
deferred goal
⊢
libc_file_atworldtrue file_handleout_file = Someout_file
exists Const0
3 opendeferred goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem worldtrue
deferred goal
⊢
libc_file_atworldtrue file_handleout_file = Someout_file
reflexivity
2 opendeferred goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem worldtrue
deferred goal
⊢
libc_file_atworldtrue file_handleout_file = Someout_file
–apply ready
deferred goal
⊢
libc_file_atworldtrue file_handleout_file = Someout_file
–reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A closed handle cannot be queried again, regardless of the registry.
570Example closed_query_rejected: ∀rep requests wide, ¬stream_call_prelibc_stream_modelrep requests wide WPtrfile_handleout_file conversion_mem worldfalse
Explore proof 3 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop, ¬stream_call_prelibc_stream_modelrep requests wide WPtrfile_handleout_file conversion_mem worldfalse
intros rep requests wide p & info & Hxs & _ & Hinfo & _
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
p :
info :
Hxs :
Hinfo :
stream_atlibc_stream_modelrep requests wide worldfalse p = Someinfo
⊢
False
injection Hxs as ←
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
info :
⊢
False
discriminate Hinfo
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide p & info & Hxs & _ & Hinfo & _
injection Hxs as ←
discriminate Hinfo
A genuine completed fclose, not merely a chosen closed fixture: error-discard settles the old FIFO and EOF still consumes the handle.
libc_stream_modelλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False
∀ complete
stream_settlementmodel worldtrue file_handleout_file mkStreamByteOriented 65; 66 true mkStreamByteOriented [ ] true complete
Explore proof 5 tactics
Initial goal
⊢
∀complete : bool, stream_settlementmodel worldtrue file_handleout_file orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true complete
intros
complete :
bool
⊢
stream_settlementmodel worldtrue file_handleout_file orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true complete
exists Discard65; 66
complete :
bool
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ acceptedDiscard65; 66 = [ ] ∧ complete = true → outstandingorientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true = [ ]
split
2 opencomplete :
bool
⊢
stream_runorientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true Discard65; 66 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
focused goal
complete :
bool
⊢
acceptedDiscard65; 66 = [ ] ∧ complete = true → outstandingorientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true = [ ]
–eapply stream_next ; exact stream_discard65; 66 [ ] true ltac:discriminate | constructor
deferred goal
complete :
bool
⊢
acceptedDiscard65; 66 = [ ] ∧ complete = true → outstandingorientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true = [ ]
–split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
exists Discard65; 66
split
–eapply stream_next ; exact stream_discard65; 66 [ ] true ltac:discriminate | constructor
–split ; reflexivity
Explore proof 1 tactics
Initial goal
⊢
repeat split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
repeat split ; reflexivity
stream_delegatesmodel worldtrue file_handleout_file [ ] conversion_mem worldfalse
Explore proof 2 tactics
Initial goal
⊢
stream_delegatesmodel worldtrue file_handleout_file [ ] conversion_mem worldfalse
split ; intros root |
⊢
∀source : span, Insource stream_sourcesmodel worldfalse file_handleout_file → ∃old : span, Inold stream_sourcesmodel worldtrue file_handleout_file ∧ ptr_capspan_ptrsource = ptr_capspan_ptrold ∨ ∃base : Z, Inbase [ ] ∧ ptr_capspan_ptrsource = Objbase ∨ ptr_capspan_ptrsource = Robase ∧ ∀base : Z, Inbase stream_releasesmodel worldfalse file_handleout_file → Inbase stream_releasesmodel worldtrue file_handleout_file ∨ Inbase [ ]
split ; intros x ; contradiction
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; intros root |
split ; intros x ; contradiction
599Example close_then_errno: M.E.invokefclose_contractmodel CVoid ArgP Const0 WPtrfile_handleout_file InterpRuntime.start conversion_mem worldtrue [ ] CallReturnWIntstream_eof InterpRuntime.start conversion_mem worldfalse ∧ M.E.invokeC.C.errno_contractλ_ _ ⇒ True CVoid [ ] [ ] InterpRuntime.start conversion_mem worldfalse [ ] CallReturnWPtrmkPtr5120 Obj5120 InterpRuntime.start conversion_mem worldfalse
Explore proof 40 tactics
Initial goal
⊢
M.E.invokefclose_contractmodel CVoid ArgP Const0 WPtrfile_handleout_file InterpRuntime.start conversion_mem worldtrue [ ] CallReturnWIntstream_eof InterpRuntime.start conversion_mem worldfalse ∧ M.E.invokeC.C.errno_contractλ_ : mem _ : libc_world ⇒ True CVoid [ ] [ ] InterpRuntime.start conversion_mem worldfalse [ ] CallReturnWPtrptr_addr ≔ 5120; ptr_cap ≔ Obj5120 InterpRuntime.start conversion_mem worldfalse
split ; | exact closed_errno
eapply M.E.invoke_normal with born := [ ]
7 openfocused goal
focused goal
focused goal
focused goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
focused goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
focused goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
–split ; left ; reflexivity |
7 opendeferred goal
deferred goal
deferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
exists Const0
7 opendeferred goal
deferred goal
deferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
reflexivity
6 opendeferred goal
deferred goal
deferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
–apply libc_stream_admitted with file := out_file ; apply ready | reflexivity
5 opendeferred goal
deferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
–split ; constructor |
5 opendeferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
exists file_handleout_file, mkStreamInfo1 mkStreamByteOriented 65; 66 true 7, mkStreamByteOriented [ ] true
5 open⊢
WPtrfile_handleout_file = WPtrfile_handleout_file ∧ stream_atmodel worldtrue file_handleout_file = Somestream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 ∧ stream_settlementmodel worldtrue file_handleout_file stream_protocolstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true false ∧ stream_state_atmodel worldfalse file_handleout_file = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_repmodel conversion_mem worldfalse ∧ stream_framemodel file_handleout_file worldtrue worldfalse ∧ stream_delegatesmodel worldtrue file_handleout_file [ ] conversion_mem worldfalse ∧ [ ] = [ ] ∧ stream_atmodel worldfalse file_handleout_file = None ∨ ∃info′ : stream_info, stream_atmodel worldfalse file_handleout_file = Someinfo′ ∧ stream_protocolinfo′ = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_aux_framemodel conversion_mem worldtrue file_handleout_file conversion_mem
deferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; reflexivity |
5 open⊢
stream_atmodel worldtrue file_handleout_file = Somestream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 ∧ stream_settlementmodel worldtrue file_handleout_file stream_protocolstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true false ∧ stream_state_atmodel worldfalse file_handleout_file = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_repmodel conversion_mem worldfalse ∧ stream_framemodel file_handleout_file worldtrue worldfalse ∧ stream_delegatesmodel worldtrue file_handleout_file [ ] conversion_mem worldfalse ∧ [ ] = [ ] ∧ stream_atmodel worldfalse file_handleout_file = None ∨ ∃info′ : stream_info, stream_atmodel worldfalse file_handleout_file = Someinfo′ ∧ stream_protocolinfo′ = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_aux_framemodel conversion_mem worldtrue file_handleout_file conversion_mem
deferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; reflexivity |
5 open⊢
stream_settlementmodel worldtrue file_handleout_file stream_protocolstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true false ∧ stream_state_atmodel worldfalse file_handleout_file = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_repmodel conversion_mem worldfalse ∧ stream_framemodel file_handleout_file worldtrue worldfalse ∧ stream_delegatesmodel worldtrue file_handleout_file [ ] conversion_mem worldfalse ∧ [ ] = [ ] ∧ stream_atmodel worldfalse file_handleout_file = None ∨ ∃info′ : stream_info, stream_atmodel worldfalse file_handleout_file = Someinfo′ ∧ stream_protocolinfo′ = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_aux_framemodel conversion_mem worldtrue file_handleout_file conversion_mem
deferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; apply close_settles |
5 open⊢
stream_state_atmodel worldfalse file_handleout_file = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_repmodel conversion_mem worldfalse ∧ stream_framemodel file_handleout_file worldtrue worldfalse ∧ stream_delegatesmodel worldtrue file_handleout_file [ ] conversion_mem worldfalse ∧ [ ] = [ ] ∧ stream_atmodel worldfalse file_handleout_file = None ∨ ∃info′ : stream_info, stream_atmodel worldfalse file_handleout_file = Someinfo′ ∧ stream_protocolinfo′ = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_aux_framemodel conversion_mem worldtrue file_handleout_file conversion_mem
deferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; reflexivity |
5 open⊢
stream_repmodel conversion_mem worldfalse ∧ stream_framemodel file_handleout_file worldtrue worldfalse ∧ stream_delegatesmodel worldtrue file_handleout_file [ ] conversion_mem worldfalse ∧ [ ] = [ ] ∧ stream_atmodel worldfalse file_handleout_file = None ∨ ∃info′ : stream_info, stream_atmodel worldfalse file_handleout_file = Someinfo′ ∧ stream_protocolinfo′ = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_aux_framemodel conversion_mem worldtrue file_handleout_file conversion_mem
deferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; apply ready |
5 open⊢
stream_framemodel file_handleout_file worldtrue worldfalse ∧ stream_delegatesmodel worldtrue file_handleout_file [ ] conversion_mem worldfalse ∧ [ ] = [ ] ∧ stream_atmodel worldfalse file_handleout_file = None ∨ ∃info′ : stream_info, stream_atmodel worldfalse file_handleout_file = Someinfo′ ∧ stream_protocolinfo′ = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_aux_framemodel conversion_mem worldtrue file_handleout_file conversion_mem
deferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; apply close_frame |
5 open⊢
stream_delegatesmodel worldtrue file_handleout_file [ ] conversion_mem worldfalse ∧ [ ] = [ ] ∧ stream_atmodel worldfalse file_handleout_file = None ∨ ∃info′ : stream_info, stream_atmodel worldfalse file_handleout_file = Someinfo′ ∧ stream_protocolinfo′ = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_aux_framemodel conversion_mem worldtrue file_handleout_file conversion_mem
deferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; apply close_delegates |
5 open⊢
[ ] = [ ] ∧ stream_atmodel worldfalse file_handleout_file = None ∨ ∃info′ : stream_info, stream_atmodel worldfalse file_handleout_file = Someinfo′ ∧ stream_protocolinfo′ = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_aux_framemodel conversion_mem worldtrue file_handleout_file conversion_mem
deferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; reflexivity |
5 open⊢
stream_atmodel worldfalse file_handleout_file = None ∨ ∃info′ : stream_info, stream_atmodel worldfalse file_handleout_file = Someinfo′ ∧ stream_protocolinfo′ = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_aux_framemodel conversion_mem worldtrue file_handleout_file conversion_mem
deferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; left ; reflexivity |
5 opendeferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
unfold stream_aux_frame
5 open⊢
∀a : Z, in_objectconversion_mem a → ¬write_authoritystream_aux_rootsmodel worldtrue file_handleout_file [ ] conversion_mem a → m_auxconversion_mem a = m_auxconversion_mem a
deferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
intros ; reflexivity
4 opendeferred goal
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
–exists file_handleout_file, mkStreamInfo1 mkStreamByteOriented 65; 66 true 7, mkStreamByteOriented [ ] true, stream_eof
4 open⊢
WPtrfile_handleout_file = WPtrfile_handleout_file ∧ stream_atmodel worldtrue file_handleout_file = Somestream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 ∧ stream_settlementmodel worldtrue file_handleout_file stream_protocolstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true true ∧ stream_state_atmodel worldfalse file_handleout_file = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_eof = 0 ∨ stream_eof = stream_eof ∧ stream_atmodel worldfalse file_handleout_file = None ∧ stream_consumedconversion_mem stream_releasesmodel worldtrue file_handleout_file ∧ stream_repmodel conversion_mem worldfalse ∧ stream_framemodel file_handleout_file worldtrue worldfalse ∧ [ ] = [ ] ∧ CallReturnWIntstream_eof = CallReturnWIntstream_eof
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; reflexivity |
4 open⊢
stream_atmodel worldtrue file_handleout_file = Somestream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 ∧ stream_settlementmodel worldtrue file_handleout_file stream_protocolstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true true ∧ stream_state_atmodel worldfalse file_handleout_file = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_eof = 0 ∨ stream_eof = stream_eof ∧ stream_atmodel worldfalse file_handleout_file = None ∧ stream_consumedconversion_mem stream_releasesmodel worldtrue file_handleout_file ∧ stream_repmodel conversion_mem worldfalse ∧ stream_framemodel file_handleout_file worldtrue worldfalse ∧ [ ] = [ ] ∧ CallReturnWIntstream_eof = CallReturnWIntstream_eof
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; reflexivity |
4 open⊢
stream_settlementmodel worldtrue file_handleout_file stream_protocolstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true true ∧ stream_state_atmodel worldfalse file_handleout_file = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_eof = 0 ∨ stream_eof = stream_eof ∧ stream_atmodel worldfalse file_handleout_file = None ∧ stream_consumedconversion_mem stream_releasesmodel worldtrue file_handleout_file ∧ stream_repmodel conversion_mem worldfalse ∧ stream_framemodel file_handleout_file worldtrue worldfalse ∧ [ ] = [ ] ∧ CallReturnWIntstream_eof = CallReturnWIntstream_eof
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; apply close_settles |
4 open⊢
stream_state_atmodel worldfalse file_handleout_file = orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true ∧ stream_eof = 0 ∨ stream_eof = stream_eof ∧ stream_atmodel worldfalse file_handleout_file = None ∧ stream_consumedconversion_mem stream_releasesmodel worldtrue file_handleout_file ∧ stream_repmodel conversion_mem worldfalse ∧ stream_framemodel file_handleout_file worldtrue worldfalse ∧ [ ] = [ ] ∧ CallReturnWIntstream_eof = CallReturnWIntstream_eof
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; reflexivity |
4 open⊢
stream_eof = 0 ∨ stream_eof = stream_eof ∧ stream_atmodel worldfalse file_handleout_file = None ∧ stream_consumedconversion_mem stream_releasesmodel worldtrue file_handleout_file ∧ stream_repmodel conversion_mem worldfalse ∧ stream_framemodel file_handleout_file worldtrue worldfalse ∧ [ ] = [ ] ∧ CallReturnWIntstream_eof = CallReturnWIntstream_eof
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; right ; reflexivity |
4 open⊢
stream_atmodel worldfalse file_handleout_file = None ∧ stream_consumedconversion_mem stream_releasesmodel worldtrue file_handleout_file ∧ stream_repmodel conversion_mem worldfalse ∧ stream_framemodel file_handleout_file worldtrue worldfalse ∧ [ ] = [ ] ∧ CallReturnWIntstream_eof = CallReturnWIntstream_eof
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; reflexivity |
4 open⊢
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; intros base |
4 open⊢
stream_repmodel conversion_mem worldfalse ∧ stream_framemodel file_handleout_file worldtrue worldfalse ∧ [ ] = [ ] ∧ CallReturnWIntstream_eof = CallReturnWIntstream_eof
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; apply ready |
4 open⊢
stream_framemodel file_handleout_file worldtrue worldfalse ∧ [ ] = [ ] ∧ CallReturnWIntstream_eof = CallReturnWIntstream_eof
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; apply close_frame |
4 open⊢
[ ] = [ ] ∧ CallReturnWIntstream_eof = CallReturnWIntstream_eof
deferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
auto
3 opendeferred goal
⊢
∀why : reason, CallReturnWIntstream_eof ≠ CallResourcewhy
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
–intros why Hbad
3 openwhy :
Hbad :
⊢
False
deferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
discriminate
2 opendeferred goal
⊢
∀values : listword, CallReturnWIntstream_eof = CallReturnvalues → return_shapecontract_returnsfclose_contractmodel values ∧ Forallword_authoritycontract_sourcesfclose_contractmodel WPtrfile_handleout_file conversion_mem worldtrue [ ] conversion_mem values
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
–intros values Hvalues
2 openvalues :
listword
Hvalues :
CallReturnWIntstream_eof = CallReturnvalues
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
injection Hvalues as ←
2 opendeferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split
3 openfocused goal
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
+exists WIntstream_eof
3 opendeferred goal
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
split ; reflexivity
2 opendeferred goal
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
+repeat constructor
deferred goal
⊢
∀status : Z, CallReturnWIntstream_eof = CallExitstatus → ∃before : listevent, [ ] = before ++ ProcessExitstatus
–intros status Hbad
status :
Z
Hbad :
CallReturnWIntstream_eof = CallExitstatus
⊢
∃before : listevent, [ ] = before ++ ProcessExitstatus
discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; | exact closed_errno
eapply M.E.invoke_normal with born := [ ]
–apply libc_stream_admitted with file := out_file ; apply ready | reflexivity
–split ; constructor |
exists file_handleout_file, mkStreamInfo1 mkStreamByteOriented 65; 66 true 7, mkStreamByteOriented [ ] true
split ; reflexivity |
split ; reflexivity |
split ; apply close_settles |
split ; reflexivity |
split ; apply ready |
split ; apply close_frame |
split ; apply close_delegates |
split ; reflexivity |
split ; left ; reflexivity |
unfold stream_aux_frame
intros ; reflexivity
–exists file_handleout_file, mkStreamInfo1 mkStreamByteOriented 65; 66 true 7, mkStreamByteOriented [ ] true, stream_eof
split ; reflexivity |
split ; reflexivity |
split ; apply close_settles |
split ; reflexivity |
split ; right ; reflexivity |
split ; reflexivity |
split ; intros base |
split ; apply ready |
split ; apply close_frame |
auto
–intros why Hbad
discriminate
–intros values Hvalues
injection Hvalues as ←
split
+exists WIntstream_eof
split ; reflexivity
+repeat constructor
–intros status Hbad
discriminate
The private-aux frame rejects clobbering a nontrivial errno aux, independently of the scalar byte-write permission.
Explore proof 6 tactics
Initial goal
intros m m′ Hin Hold Hnew Hframe
assert Houtside : ¬write_authoritystream_aux_rootsmodel worldtrue file_handleout_file [ ] m 5120
2 open⊢
¬write_authoritystream_aux_rootsmodel worldtrue file_handleout_file [ ] m 5120
focused goal
m, m′ :
Hin :
in_objectm 5120
Hframe :
Houtside :
¬write_authoritystream_aux_rootsmodel worldtrue file_handleout_file [ ] m 5120
⊢
False
{intros root & & _ | base & reg & & _
deferred goal
m, m′ :
Hin :
in_objectm 5120
Hframe :
Houtside :
¬write_authoritystream_aux_rootsmodel worldtrue file_handleout_file [ ] m 5120
⊢
False
specialize Hframe5120 Hin Houtside
m, m′ :
Hin :
in_objectm 5120
Houtside :
¬write_authoritystream_aux_rootsmodel worldtrue file_handleout_file [ ] m 5120
⊢
False
rewrite Hold , Hnew in Hframe
m, m′ :
Hin :
in_objectm 5120
Houtside :
¬write_authoritystream_aux_rootsmodel worldtrue file_handleout_file [ ] m 5120
⊢
False
discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m m′ Hin Hold Hnew Hframe
assert Houtside : ¬write_authoritystream_aux_rootsmodel worldtrue file_handleout_file [ ] m 5120
{intros root & & _ | base & reg & & _
specialize Hframe5120 Hin Houtside
rewrite Hold , Hnew in Hframe
discriminate
Query-only byte framing protects the last errno byte too, even though ordinary effects authorize all four scalar errno writes.
645Example query_errno_byte_clobber_rejected: ∀spec s m′ s′ trace ending, spec = ferror_contractmodel ∨ spec = fpending_contractmodel → m_bytesm′ 5123 ≠ m_bytesconversion_mem 5123 → ¬M.E.invokespec CVoid ArgP Const0 WPtrfile_handleout_file s conversion_mem worldtrue trace ending s′ m′ worldtrue
Explore proof 3 tactics
Initial goal
⊢
∀spec : contractlibc_world s : InterpRuntime.state m′ : mem s′ : InterpRuntime.state trace : listevent ending : call_end, spec = ferror_contractmodel ∨ spec = fpending_contractmodel → m_bytesm′ 5123 ≠ m_bytesconversion_mem 5123 → ¬M.E.invokespec CVoid ArgP Const0 WPtrfile_handleout_file s conversion_mem worldtrue trace ending s′ m′ worldtrue
intros spec s m′ s′ trace ending Hspec Hchanged Hcall
spec :
m′ :
trace :
listevent
ending :
Hspec :
spec = ferror_contractmodel ∨ spec = fpending_contractmodel
Hchanged :
m_bytesm′ 5123 ≠ m_bytesconversion_mem 5123
Hcall :
M.E.invokespec CVoid ArgP Const0 WPtrfile_handleout_file s conversion_mem worldtrue trace ending s′ m′ worldtrue
⊢
False
destruct Hspec as → | →
2 openm′ :
trace :
listevent
ending :
Hchanged :
m_bytesm′ 5123 ≠ m_bytesconversion_mem 5123
Hcall :
M.E.invokeferror_contractmodel CVoid ArgP Const0 WPtrfile_handleout_file s conversion_mem worldtrue trace ending s′ m′ worldtrue
⊢
False
focused goal
m′ :
trace :
listevent
ending :
Hchanged :
m_bytesm′ 5123 ≠ m_bytesconversion_mem 5123
Hcall :
M.E.invokefpending_contractmodel CVoid ArgP Const0 WPtrfile_handleout_file s conversion_mem worldtrue trace ending s′ m′ worldtrue
⊢
False
all: destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & _ & p & info & Hxs & _ & _ & _ & _ & _ & _ & Hbytes ; injection Hxs as ← ; apply Hchanged , Hbytes ; exists 5120, mkRegion5120 5128 Heap Live ; split ; reflexivity | simpl ; lia | intros root & & _ | base & reg & & _
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros spec s m′ s′ trace ending Hspec Hchanged Hcall
destruct Hspec as → | →
all: destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & _ & p & info & Hxs & _ & _ & _ & _ & _ & _ & Hbytes ; injection Hxs as ← ; apply Hchanged , Hbytes ; exists 5120, mkRegion5120 5128 Heap Live ; split ; reflexivity | simpl ; lia | intros root & & _ | base & reg & & _
Two active, different FILEs may not both own the same release.
663Example overlapping_release_rejected: ∀m w p file q other base, libc_file_atw p = Somefile → libc_file_atw q = Someother → file_handleother ≠ file_handlefile → Inbase file_ownedfile → Inbase file_ownedother → ¬libc_release_separatedm w
Explore proof 3 tactics
Initial goal
⊢
∀m : mem w : libc_world p : ptr file : libc_file q : ptr other : libc_file base : Z, libc_file_atw p = Somefile → libc_file_atw q = Someother → file_handleother ≠ file_handlefile → Inbase file_ownedfile → Inbase file_ownedother → ¬libc_release_separatedm w
intros m w p file q other base Hp Hq Hne Hin Hother Hsep
m :
w :
p :
file :
q :
other :
base :
Z
Hp :
libc_file_atw p = Somefile
Hq :
libc_file_atw q = Someother
Hne :
file_handleother ≠ file_handlefile
Hin :
Inbase file_ownedfile
Hother :
Inbase file_ownedother
Hsep :
⊢
False
destruct Hsepp file Hp base Hin as _ & Howners & _
m :
w :
p :
file :
q :
other :
base :
Z
Hp :
libc_file_atw p = Somefile
Hq :
libc_file_atw q = Someother
Hne :
file_handleother ≠ file_handlefile
Hin :
Inbase file_ownedfile
Hother :
Inbase file_ownedother
Hsep :
Howners :
∀q : ptr other : libc_file, libc_file_atw q = Someother → file_handleother ≠ file_handlefile → ¬Inbase file_ownedother
⊢
False
exact Hownersq other Hq Hne Hother
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m w p file q other base Hp Hq Hne Hin Hother Hsep
destruct Hsepp file Hp base Hin as _ & Howners & _
exact Hownersq other Hq Hne Hother
Stable FILE capability identities cannot enter an active release pool, even when the memory happens to classify them as Heap.
676Example static_handle_release_rejected: ∀m w p file base, libc_file_atw p = Somefile → ptr_caplibc_stdoutw = Objbase → Inbase file_ownedfile → ¬libc_release_separatedm w
Explore proof 10 tactics
Initial goal
⊢
∀m : mem w : libc_world p : ptr file : libc_file base : Z, libc_file_atw p = Somefile → ptr_caplibc_stdoutw = Objbase → Inbase file_ownedfile → ¬libc_release_separatedm w
intros m w p file base Hp Hcap Hin Hsep
m :
w :
p :
file :
base :
Z
Hp :
libc_file_atw p = Somefile
Hcap :
ptr_caplibc_stdoutw = Objbase
Hin :
Inbase file_ownedfile
Hsep :
⊢
False
destruct Hsepp file Hp base Hin as _ & _ & Hnot & _
m :
w :
p :
file :
base :
Z
Hp :
libc_file_atw p = Somefile
Hcap :
ptr_caplibc_stdoutw = Objbase
Hin :
Inbase file_ownedfile
Hsep :
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: locale_private_sourceslibc_localefstw ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
⊢
False
apply Hnot
m :
w :
p :
file :
base :
Z
Hp :
libc_file_atw p = Somefile
Hcap :
ptr_caplibc_stdoutw = Objbase
Hin :
Inbase file_ownedfile
Hsep :
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: locale_private_sourceslibc_localefstw ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
⊢
[ ]
m
Objbase
right
m :
w :
p :
file :
base :
Z
Hp :
libc_file_atw p = Somefile
Hcap :
ptr_caplibc_stdoutw = Objbase
Hin :
Inbase file_ownedfile
Hsep :
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: locale_private_sourceslibc_localefstw ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
⊢
Ins
∧
∨
Ins
∧
∨
left
m :
w :
p :
file :
base :
Z
Hp :
libc_file_atw p = Somefile
Hcap :
ptr_caplibc_stdoutw = Objbase
Hin :
Inbase file_ownedfile
Hsep :
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: locale_private_sourceslibc_localefstw ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
⊢
Ins
∧
exists mkSpanlibc_stdoutw 0
m :
w :
p :
file :
base :
Z
Hp :
libc_file_atw p = Somefile
Hcap :
ptr_caplibc_stdoutw = Objbase
Hin :
Inbase file_ownedfile
Hsep :
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: locale_private_sourceslibc_localefstw ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
⊢
Inspan_ptr ≔ libc_stdoutw; span_size ≔ 0
∧
split ; left ; reflexivity |
m :
w :
p :
file :
base :
Z
Hp :
libc_file_atw p = Somefile
Hcap :
ptr_caplibc_stdoutw = Objbase
Hin :
Inbase file_ownedfile
Hsep :
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: locale_private_sourceslibc_localefstw ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
simpl
m :
w :
p :
file :
base :
Z
Hp :
libc_file_atw p = Somefile
Hcap :
ptr_caplibc_stdoutw = Objbase
Hin :
Inbase file_ownedfile
Hsep :
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: locale_private_sourceslibc_localefstw ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
⊢
Objbase = ptr_caplibc_stdoutw
symmetry
m :
w :
p :
file :
base :
Z
Hp :
libc_file_atw p = Somefile
Hcap :
ptr_caplibc_stdoutw = Objbase
Hin :
Inbase file_ownedfile
Hsep :
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: locale_private_sourceslibc_localefstw ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
⊢
ptr_caplibc_stdoutw = Objbase
exact Hcap
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m w p file base Hp Hcap Hin Hsep
destruct Hsepp file Hp base Hin as _ & _ & Hnot & _
apply Hnot
right
left
exists mkSpanlibc_stdoutw 0
split ; left ; reflexivity |
simpl
symmetry
exact Hcap