rocq/theories/LibcDiagnosticLogic.v
Returning diagnostics on the consumer's same libc world and machine. Native diagnostic representation stays trusted. The frame below owns no diagnostic pool: it separates future write roots, not all retained sources or future release rights.
From iris.proofmode Require Import proofmode
From Stdlib Require Import String ZArith List Lia
From Nanofil Require Import Term Syntax Values Memory Runtime Identity ExternalCalls ExternalMachine Stdio Shutdown Streams Formatting Diagnostics Libc LibcStreams Pieces Heap ContractFrame Logic StringLogic LentLogic LibcStreamLogic LibcErrnoLogic LibcStreamTokens LibcStreamAdapter
Import ListNotations
Open Scope Z_scope
Open Scope list_scope
Preserve callback inventory, not the whole shutdown record: flushing stdout changes its authoritative protocol. Neither FILE inventory is frozen, and parser compatibility (including sampled errno) is separate.
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
Keep the native sources, writes, requests and segment interpretation. Readiness at both endpoints includes the independent FILE envelope.
mkDiagnosticContextlibc_world λm w ⇒ diagnostic_readynative m w ∧ libc_stream_readyrep m w diagnostic_sourcesnative diagnostic_writesnative diagnostic_requestsnative diagnostic_segmentsnative λw w′ ⇒ diagnostic_framenative w w′ ∧ libc_diagnostic_framew w′
Only this status-zero wrapper is an ordinary returning error symbol. Nonzero diagnostics still belong to the separate ending protocol.
error_contracterror_format_contractlibc_stream_modelrep requests wide libc_stdout libc_stderr libc_diagnostic_contextrep native
Exact open observations cannot be framed unchanged through acceptance or settlement. Open-only and completed-closed names can.
Some_
⇒
False
stream_tokens_wirep out err b o m w h ∧ roots_apartdiagnostic_writesnative w stream_data_heaptoken_baseout token_baseerr h m ∧ diagnostic_nameout h ∧ diagnostic_nameerr h
Transport only what the permitted name constructors actually observe.
∀ d w w′ h h′
stream_currentd w h
∃info, libc_stream_atw token_handled = Someinfo → ∃info, libc_stream_atw′ token_handled = Someinfo
libc_stream_atw token_handled = None → libc_stream_atw′ token_handled = None ∧ libc_stream_statew′ token_handled = libc_stream_statew token_handled
stream_currentd w′ h′ ∧ diagnostic_named h′
Explore proof 11 tactics
Initial goal
⊢
∀d : stream_token w w′ : libc_world h h′ : gmappiece pval, h′ !! PNametoken_keyd = h !! PNametoken_keyd → diagnostic_named h → stream_currentd w h → ∃info : stream_info, libc_stream_atw token_handled = Someinfo → ∃info : stream_info, libc_stream_atw′ token_handled = Someinfo → libc_stream_atw token_handled = None → libc_stream_atw′ token_handled = None ∧ libc_stream_statew′ token_handled = libc_stream_statew token_handled → stream_currentd w′ h′ ∧ diagnostic_named h′
intros d w w′ h h′ Hkey Hname Hcurrent Hopen Hclosed
d :
w, w′ :
Hname :
Hcurrent :
stream_currentd w h
Hopen :
∃info : stream_info, libc_stream_atw token_handled = Someinfo → ∃info : stream_info, libc_stream_atw′ token_handled = Someinfo
Hclosed :
libc_stream_atw token_handled = None → libc_stream_atw′ token_handled = None ∧ libc_stream_statew′ token_handled = libc_stream_statew token_handled
⊢
stream_currentd w′ h′ ∧ diagnostic_named h′
unfold stream_current , diagnostic_name in *
d :
w, w′ :
Hname :
_
⇒
False
Hcurrent :
None
⇒
True
_
⇒
False
Hopen :
∃info : stream_info, libc_stream_atw token_handled = Someinfo → ∃info : stream_info, libc_stream_atw′ token_handled = Someinfo
Hclosed :
libc_stream_atw token_handled = None → libc_stream_atw′ token_handled = None ∧ libc_stream_statew′ token_handled = libc_stream_statew token_handled
⊢
None
⇒
True
_
⇒
False
∧
_
⇒
False
rewrite Hkey
d :
w, w′ :
Hname :
_
⇒
False
Hcurrent :
None
⇒
True
_
⇒
False
Hopen :
∃info : stream_info, libc_stream_atw token_handled = Someinfo → ∃info : stream_info, libc_stream_atw′ token_handled = Someinfo
Hclosed :
libc_stream_atw token_handled = None → libc_stream_atw′ token_handled = None ∧ libc_stream_statew′ token_handled = libc_stream_statew token_handled
⊢
None
⇒
True
_
⇒
False
∧
_
⇒
False
destruct h !! PNametoken_keyd as v | ; | auto
d :
w, w′ :
v :
Hname :
match v with
_
⇒
False
Hcurrent :
match v with
_
⇒
False
Hopen :
∃info : stream_info, libc_stream_atw token_handled = Someinfo → ∃info : stream_info, libc_stream_atw′ token_handled = Someinfo
Hclosed :
libc_stream_atw token_handled = None → libc_stream_atw′ token_handled = None ∧ libc_stream_statew′ token_handled = libc_stream_statew token_handled
⊢
match v with
_
⇒
False
∧
match v with
_
⇒
False
destruct v ; try contradiction
2 opend :
w, w′ :
p :
pending :
optionZ × listZ
Hname :
match pending with
Some_
⇒
False
None
⇒
True
Hcurrent :
p = token_handled ∧ stream_observationw p pending
Hopen :
∃info : stream_info, libc_stream_atw token_handled = Someinfo → ∃info : stream_info, libc_stream_atw′ token_handled = Someinfo
Hclosed :
libc_stream_atw token_handled = None → libc_stream_atw′ token_handled = None ∧ libc_stream_statew′ token_handled = libc_stream_statew token_handled
⊢
focused goal
d :
w, w′ :
p :
Hkey :
h′ !! PNametoken_keyd = SomeVStreamOpenp
Hname :
True
Hcurrent :
p = token_handled ∧ ∃info : stream_info, libc_stream_atw p = Someinfo
Hopen :
∃info : stream_info, libc_stream_atw token_handled = Someinfo → ∃info : stream_info, libc_stream_atw′ token_handled = Someinfo
Hclosed :
libc_stream_atw token_handled = None → libc_stream_atw′ token_handled = None ∧ libc_stream_statew′ token_handled = libc_stream_statew token_handled
⊢
p = token_handled ∧ ∃info : stream_info, libc_stream_atw′ p = Someinfo ∧ True
–destruct pending as physical fifo | ; contradiction |
2 opend :
w, w′ :
p :
Hname :
True
Hcurrent :
p = token_handled ∧ stream_observationw p None
Hopen :
∃info : stream_info, libc_stream_atw token_handled = Someinfo → ∃info : stream_info, libc_stream_atw′ token_handled = Someinfo
Hclosed :
libc_stream_atw token_handled = None → libc_stream_atw′ token_handled = None ∧ libc_stream_statew′ token_handled = libc_stream_statew token_handled
⊢
p = token_handled ∧ stream_observationw′ p None ∧ True
deferred goal
d :
w, w′ :
p :
Hkey :
h′ !! PNametoken_keyd = SomeVStreamOpenp
Hname :
True
Hcurrent :
p = token_handled ∧ ∃info : stream_info, libc_stream_atw p = Someinfo
Hopen :
∃info : stream_info, libc_stream_atw token_handled = Someinfo → ∃info : stream_info, libc_stream_atw′ token_handled = Someinfo
Hclosed :
libc_stream_atw token_handled = None → libc_stream_atw′ token_handled = None ∧ libc_stream_statew′ token_handled = libc_stream_statew token_handled
⊢
p = token_handled ∧ ∃info : stream_info, libc_stream_atw′ p = Someinfo ∧ True
destruct Hcurrent as → Hlookup Hfifo
2 opend :
w, w′ :
Hkey :
h′ !! PNametoken_keyd = SomeVStreamtoken_handled None
Hname :
True
Hlookup :
libc_stream_atw token_handled = None
Hfifo :
Hopen :
∃info : stream_info, libc_stream_atw token_handled = Someinfo → ∃info : stream_info, libc_stream_atw′ token_handled = Someinfo
Hclosed :
libc_stream_atw token_handled = None → libc_stream_atw′ token_handled = None ∧ libc_stream_statew′ token_handled = libc_stream_statew token_handled
⊢
token_handled = token_handled ∧ stream_observationw′ token_handled None ∧ True
deferred goal
d :
w, w′ :
p :
Hkey :
h′ !! PNametoken_keyd = SomeVStreamOpenp
Hname :
True
Hcurrent :
p = token_handled ∧ ∃info : stream_info, libc_stream_atw p = Someinfo
Hopen :
∃info : stream_info, libc_stream_atw token_handled = Someinfo → ∃info : stream_info, libc_stream_atw′ token_handled = Someinfo
Hclosed :
libc_stream_atw token_handled = None → libc_stream_atw′ token_handled = None ∧ libc_stream_statew′ token_handled = libc_stream_statew token_handled
⊢
p = token_handled ∧ ∃info : stream_info, libc_stream_atw′ p = Someinfo ∧ True
destruct HclosedHlookup as Hlookup′ Hstate
2 opend :
w, w′ :
Hkey :
h′ !! PNametoken_keyd = SomeVStreamtoken_handled None
Hname :
True
Hlookup :
libc_stream_atw token_handled = None
Hfifo :
Hopen :
∃info : stream_info, libc_stream_atw token_handled = Someinfo → ∃info : stream_info, libc_stream_atw′ token_handled = Someinfo
Hclosed :
libc_stream_atw token_handled = None → libc_stream_atw′ token_handled = None ∧ libc_stream_statew′ token_handled = libc_stream_statew token_handled
Hlookup′ :
libc_stream_atw′ token_handled = None
Hstate :
⊢
token_handled = token_handled ∧ stream_observationw′ token_handled None ∧ True
deferred goal
d :
w, w′ :
p :
Hkey :
h′ !! PNametoken_keyd = SomeVStreamOpenp
Hname :
True
Hcurrent :
p = token_handled ∧ ∃info : stream_info, libc_stream_atw p = Someinfo
Hopen :
∃info : stream_info, libc_stream_atw token_handled = Someinfo → ∃info : stream_info, libc_stream_atw′ token_handled = Someinfo
Hclosed :
libc_stream_atw token_handled = None → libc_stream_atw′ token_handled = None ∧ libc_stream_statew′ token_handled = libc_stream_statew token_handled
⊢
p = token_handled ∧ ∃info : stream_info, libc_stream_atw′ p = Someinfo ∧ True
split ; split ; reflexivity | split ; exact Hlookup′ | rewrite Hstate ; exact Hfifo | exact I
deferred goal
d :
w, w′ :
p :
Hkey :
h′ !! PNametoken_keyd = SomeVStreamOpenp
Hname :
True
Hcurrent :
p = token_handled ∧ ∃info : stream_info, libc_stream_atw p = Someinfo
Hopen :
∃info : stream_info, libc_stream_atw token_handled = Someinfo → ∃info : stream_info, libc_stream_atw′ token_handled = Someinfo
Hclosed :
libc_stream_atw token_handled = None → libc_stream_atw′ token_handled = None ∧ libc_stream_statew′ token_handled = libc_stream_statew token_handled
⊢
p = token_handled ∧ ∃info : stream_info, libc_stream_atw′ p = Someinfo ∧ True
–destruct Hcurrent as → Hlookup
d :
w, w′ :
Hkey :
h′ !! PNametoken_keyd = SomeVStreamOpentoken_handled
Hname :
True
Hlookup :
∃info : stream_info, libc_stream_atw token_handled = Someinfo
Hopen :
∃info : stream_info, libc_stream_atw token_handled = Someinfo → ∃info : stream_info, libc_stream_atw′ token_handled = Someinfo
Hclosed :
libc_stream_atw token_handled = None → libc_stream_atw′ token_handled = None ∧ libc_stream_statew′ token_handled = libc_stream_statew token_handled
⊢
token_handled = token_handled ∧ ∃info : stream_info, libc_stream_atw′ token_handled = Someinfo ∧ True
split ; split ; reflexivity | auto | exact I
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros d w w′ h h′ Hkey Hname Hcurrent Hopen Hclosed
unfold stream_current , diagnostic_name in *
rewrite Hkey
destruct v ; try contradiction
–destruct pending as physical fifo | ; contradiction |
destruct Hcurrent as → Hlookup Hfifo
destruct HclosedHlookup as Hlookup′ Hstate
split ; split ; reflexivity | split ; exact Hlookup′ | rewrite Hstate ; exact Hfifo | exact I
–destruct Hcurrent as → Hlookup
split ; split ; reflexivity | auto | exact I
The empty return list comes from the supplied machine's normal branch, never from a resource prefix. The same invocation also supplies the formatting observations and both FILE delegations.
∀ rep requests wide native r args xs s m w trace values s′ m′ w′
M.E.invokelibc_error_contractrep requests wide native r args xs s m w trace CallReturnvalues s′ m′ w′
values = [ ] ∧ ∃born, M.E.prefixlibc_error_contractrep requests wide native xs s m w born trace s′ m′ w′
Explore proof 5 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 native : diagnostic_contextlibc_world 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, M.E.invokelibc_error_contractrep requests wide native r args xs s m w trace CallReturnvalues s′ m′ w′ → values = [ ] ∧ ∃born : listZ, M.E.prefixlibc_error_contractrep requests wide native xs s m w born trace s′ m′ w′
intros rep requests wide native r args xs s m w trace values s′ m′ w′ Hi
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
native :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokelibc_error_contractrep requests wide native r args xs s m w trace CallReturnvalues s′ m′ w′
⊢
values = [ ] ∧ ∃born : listZ, M.E.prefixlibc_error_contractrep requests wide native xs s m w born trace s′ m′ w′
split
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
native :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokelibc_error_contractrep requests wide native r args xs s m w trace CallReturnvalues s′ m′ w′
⊢
values = [ ]
focused goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
native :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokelibc_error_contractrep requests wide native r args xs s m w trace CallReturnvalues s′ m′ w′
⊢
∃born : listZ, M.E.prefixlibc_error_contractrep requests wide native xs s m w born trace s′ m′ w′
–inversion Hi ; subst
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
native :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokelibc_error_contractrep requests wide native r args xs s m w trace CallReturnvalues s′ m′ w′
born :
listZ
H :
contract_abilibc_error_contractrep requests wide native r args
H0 :
contract_prelibc_error_contractrep requests wide native xs m w
H1 :
M.E.prefixlibc_error_contractrep requests wide native xs s m w born trace s′ m′ w′
H2 :
contract_postlibc_error_contractrep requests wide native xs m w born trace CallReturnvalues m′ w′
H3 :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
H4 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnslibc_error_contractrep requests wide native values0 ∧ Forallword_authoritycontract_sourceslibc_error_contractrep requests wide native xs m w born m′ values0
H5 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
values = [ ]
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
native :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokelibc_error_contractrep requests wide native r args xs s m w trace CallReturnvalues s′ m′ w′
⊢
∃born : listZ, M.E.prefixlibc_error_contractrep requests wide native xs s m w born trace s′ m′ w′
match goal withHpost : contract_post_ _ _ _ _ _ _ _ _ |- _⇒apply error_post_void in Hpost ; injection Hpost ; autoend
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
native :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokelibc_error_contractrep requests wide native r args xs s m w trace CallReturnvalues s′ m′ w′
⊢
∃born : listZ, M.E.prefixlibc_error_contractrep requests wide native xs s m w born trace s′ m′ w′
–eapply M.E.invoke_prefix ; exact Hi
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide native r args xs s m w trace values s′ m′ w′ Hi
split
–inversion Hi ; subst
match goal withHpost : contract_post_ _ _ _ _ _ _ _ _ |- _⇒apply error_post_void in Hpost ; injection Hpost ; autoend
–eapply M.E.invoke_prefix ; exact Hi
Sample only the already-owned errno byte keys. Life projection omits neither private bytes nor auxiliary pieces. Future FILE release separation is restored against the FULL heap, including both lives.
∀ rep requests wide native out err b o r args xs s m w trace values s′ m′ w′ h old
M.E.invokelibc_error_contractrep requests wide native r args xs s m w trace CallReturnvalues s′ m′ w′
agreesm h
R.readys m
libc_diagnostic_wirep native out err b o m w h
lengthold = 4%nat
∀l v, l, v ∈ byte_psb o old → h !! l = Somev
∃ys, values = [ ] ∧ lengthys = 4%nat ∧ byte_psb o ys.*1 = byte_psb o old.*1 ∧ agreesm′ overwritebyte_psb o ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_diagnostic_wirep native out err b o m′ w′ overwritebyte_psb o ys h
Proof 190 steps Qed
intros rep requests wide native out err b o r args xs s m w trace values s′ m′ w′ h old Hi Ha Hd Hr Hpair Hroots Honame Hename Hlen Howned
destruct Hpair as Howf & Hewf & Hbase & Hkey & Hout & Herr & Hoc & Hec & Hprivate
destruct Hprivateout or_introleq_refl as Howi Horelease
destruct Hprivateerr or_introreq_refl as Hewi Herelease
set dh := stream_data_heaptoken_baseout token_baseerr h
pose proof stream_data_agreestoken_baseout token_baseerr m h Ha as Hdata
destruct error_returnedrep requests wide native r args xs s m w trace values s' m' w' Hi as Hvalues born Hp
pose proof M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as Hr′ Hpers
destruct LG.prefix_agrees_out_ _ _ _ _ _ _ _ _ _ _ dh errno_keysb o span_containserrno_spanb o Hp Hr Hd as Hexcept & Hids & Hd′ & Hborn
–intros l v Hl Hmem
eapply agree_piece_registered ; exact Hmem | exact Hdatal v Hl
–change roots_outlibc_stream_writesw libc_stdoutw ++ libc_stream_writesw libc_stderrw ++ diagnostic_writesnative w dh m span_containserrno_spanb o
intros root a Hin Hspan Hown
apply in_app_or in Hin as Hin | Hin
eapply errno_roots_out ; exact proj1proj2Howi | exact proj1proj2proj2Howi | exact Hin | exact Hspan | exact Hown
–exact proj2proj2proj2proj2Howi
–intros base l v Hin
contradiction
–destruct proj2Hp as Hformat Htrace
destruct Hformat as status & errnum & fmt & rest & text & body & info & info′ & segments & pieces & actions & Hxs & Hstring & Hformat & Hsegments & Hpieces & Hinfo & Hopen & Hid & Hid′ & Hrun & Haccepted & Hflush & Hready & Hframe & Houtdel & Herrdel & Hrootdel & Htrace′ & Haux
destruct Hready as Hnative Hready
destruct Hframe as Hnativeframe Hframe
change libc_diagnostic_framew w' in Hframe
destruct Hframe as Hout′ & Herr′ & Hlocale & Herrno & Hphase & Hstatus & Hpending & Hconsumed
assert He : libc_errnofstw' = mkPtrb + o Objb
{rewrite Herrno
exact proj1proj2Howi
set ys := errno_bytesm' b o
set dh′ := stream_data_heaptoken_baseout token_baseerr h'
{intros base Hin
rewrite byte_ps_keys in Hin
apply list_elem_of_fmap in Hin as i & E & _
discriminate E
{unfold dh' , h' , dh
apply stream_data_overwrite ; apply Hlifeoff
assert Hkeysfull : memory_keys_fromh' h
{intros l v Hl Hmem
destruct lookup_overwrite_ _ _ _ Hl as Hin | _ Hold ; | eauto
apply list_elem_of_fmap in Hinold as key oldv & E & Hinold
simpl in E
subst key
exists oldv
exact Howned_ _ Hinold
assert Hkeysdata : memory_keys_fromdh' dh
{intros l v Hl Hmem
apply stream_data_lookup in Hl as Hl & Hno & Hne
exists oldv
unfold dh
rewrite stream_data_lookup_ne ; assumption
–exact all_agree_elem_ _ _ _ Hbytes Hin
{eapply stream_data_restore ; exact Ha | exact Hdata' | exact Hpers | | | |
–apply overwrite_out , Hlifeoff
–apply overwrite_out , Hlifeoff
–intros reg Hlive
eapply T.prefix_handle_live ; exact Hp | exact Hr | exact Hd | exact Hlive |
intros Hnil
contradiction
–intros reg Hlive
eapply T.prefix_handle_live ; exact Hp | exact Hr | exact Hd | exact Hlive |
intros Hnil
contradiction
{intros d
apply overwrite_out
rewrite byte_ps_keys
intros Hin
apply list_elem_of_fmap in Hin as i & E & _
discriminate E
assert Hcurrent : stream_currentout w' h' ∧ diagnostic_nameout h'
{eapply diagnostic_current ; apply Hnamekeys | exact Honame | exact Hoc | |
–intros i Hi0
unfold diagnostic_flush in Hflush
cbn [ stream_at stream_state_at libc_stream_model ] in Hflush
rewrite Hout Hi0 in Hflush
destruct Hflush as i′ & Hi′ & _
exists i'
exact Hi'
–intros Hclosed
unfold diagnostic_flush in Hflush
cbn [ stream_at stream_state_at libc_stream_model ] in Hflush
rewrite Hout Hclosed in Hflush
exact Hflush
assert Hcurrenterr : stream_currenterr w' h' ∧ diagnostic_nameerr h'
{eapply diagnostic_current ; apply Hnamekeys | exact Hename | exact Hec | |
–intros _
exists info'
rewrite <- Herr
exact proj1proj2Hopen
–intros Hclosed
change libc_stream_atw libc_stderrw = Someinfo in Hinfo
rewrite Herr Hclosed in Hinfo
discriminate Hinfo
assert Hprivate′ : ∀d, d = out ∨ d = err → libc_errno_wirep token_handled b o m' w' dh' ∧ ids_apartlibc_stream_releasesw' token_handled h'
{intros d Hdsel
destruct Hprivated Hdsel as Hwi Hrel
assert Hdelegate : stream_delegateslibc_stream_modelrep requests wide w token_handled born m' w'
{destruct Hdsel as → | → ; rewrite <- Hout | rewrite <- Herr ; assumption
assert Hwi′ : libc_errno_wirep token_handled b o m' w' dh'
{eapply errno_wi_endpoint ; exact Hwi | exact Hdata | exact Hpers | exact Hd' | exact Hready | exact Herrno | exact Hdelegate | exact Hborn | exact Hkeysdata
split ; exact Hwi' |
intros base l v Hin Hl Hmem
destruct decidel = PLivetoken_baseout as [ ->| Hno ]
–simpl
intros E
subst base
eapply libc_handle_not_released ; exact Hready | left ; reflexivity | | exact Hin
rewrite Hout' Hout
exact proj1Howf
–destruct decidel = PLivetoken_baseerr as [ ->| Hne ]
+simpl
intros E
subst base
eapply libc_handle_not_released ; exact Hready | right ; reflexivity | | exact Hin
rewrite Herr' Herr
exact proj1Hewf
unfold dh'
rewrite stream_data_lookup_ne ; assumption
assert Hroots′ : roots_apartdiagnostic_writesnative w' dh' m'
{intros root a Hin Hspan l & v & reg & Hl & Hmem & Hlive & Hrange
assert Howned′ : owned_livedh m' a
assert Hapart : roots_apartdiagnostic_writesnative w dh m'
{intros oldroot addr Holdroot Holdspan key & val & rr & Hlookup & Hmemory & Hlive′ & Hbounds
apply Hrootsoldroot addr Holdroot Holdspan
exists key, val, rr
split ; exact Hlookup |
split ; exact Hmemory |
split ; | exact Hbounds
eapply registered_live_back ; exact Hpers | | exact Hlive'
eapply agree_piece_registered ; exact Hmemory | exact Hdatakey val Hlookup
exact owned_not_authoritydiagnostic_writesnative w born dh m' a Hd' Hapart Hborn Howned' Hautha Hspan
exists ys
split ; exact Hvalues |
split
split ; exact Hkeys |
split ; exact Ha' |
split ; exact Hd' |
split ; exact Hr' |
split
+split ; exact Howf |
split ; exact Hewf |
split ; exact Hbase |
split ; exact Hkey |
split ; rewrite Hout' ; exact Hout |
split ; rewrite Herr' ; exact Herr |
split ; exact proj1Hcurrent |
split ; exact proj1Hcurrenterr | exact Hprivate'
+exact conjHroots' conjproj2Hcurrent proj2Hcurrenterr
Caller-owned diagnostic strings are returned with their old values. Separation is checked against the sampled errno keys, not merely at entry: a diagnostic prefix must not overwrite the new errno bytes.
∀ rep requests wide native out err b o ps r args xs s m w trace values s′ m′ w′ h old
M.E.invokelibc_error_contractrep requests wide native r args xs s m w trace CallReturnvalues s′ m′ w′
agreesm h
R.readys m
libc_diagnostic_wirep native out err b o m w h
lengthold = 4%nat
∀l v, l, v ∈ ps ++ byte_psb o old → h !! l = Somev
∀l v, l, v ∈ ps → l ∉ errno_keysb o
∃ys, values = [ ] ∧ lengthys = 4%nat ∧ ps ++ byte_psb o ys.*1 = ps ++ byte_psb o old.*1 ∧ agreesm′ overwriteps ++ byte_psb o ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_diagnostic_wirep native out err b o m′ w′ overwriteps ++ byte_psb o ys h
Proof 29 steps Qed
intros rep requests wide native out err b o ps r args xs s m w tr vs s′ m′ w′ h old Hi Ha Hd Hr Hw Hlen Howned Hoff
destruct error_framerep requests wide native out err b o r args xs s m w tr vs s' m' w' h old Hi Ha Hd Hr Hw Hlen as ys & Hvs & Hys & Hkeys & Ha′ & Hd′ & Hr′ & Hw′
{rewrite overwrite_app
apply LG.overwrite_id
intros l v Hin
rewrite overwrite_out
exists ys
split ; exact Hvs |
split ; exact Hys |
split
{rewrite ! fmap_app Hkeys
reflexivity
rewrite Heq
auto
Logical contract controls, not native FILEs or native diagnostic-pool realization. Both initial stdout states have actual admitted calls.
mkDiagnosticContextlibc_world λ_ _ ⇒ True λ_ _ ⇒ [ ] λ_ ⇒ [ ] λ_ _ _ ⇒ False λ_ _ _ body segments ⇒ segments = body; 10 λ_ _ ⇒ True
libc_diagnostic_contextλ_ _ ⇒ True native
libc_error_contractλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False native
mkLibcPayloadlibc_localefstconversion_world mkStdioWorldopened mkSpanlibc_errnofstconversion_world 4 libc_errnofstconversion_world mkLibcStreamsF.out_file F.err_file true mkStreamByteOriented 67; 10 false libc_getoptfstconversion_world, mkShutdownHandlers 0 [ ] [ ] mkStreamByteOriented [ ] true
∀ opened
libc_stream_readyλ_ _ ⇒ True T.changed_errno final_worldopened
Explore proof 20 tactics
Initial goal
⊢
∀opened : bool, libc_stream_readyλ_ : mem _ : libc_world ⇒ True T.changed_errno final_worldopened
intros opened
opened :
bool
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True T.changed_errno final_worldopened
destruct T.changed_readyopened as Hrep & Hlocale & He & _ & _ & Hu & Hstatus & Hphase & Hdistinct & Hroots & Hout & Herr & Hsep
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True T.changed_errno final_worldopened
split ; exact Hrep |
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localefinal_worldopened.1
∧
∧
∧
∧
shutdown_uniquefinal_worldopened.2
∧
−2 ^ 31 ≤ shutdown_statusfinal_worldopened.2 < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutfinal_worldopened ≠ ptr_addrlibc_stderrfinal_worldopened ∧ stdio_rootslibc_stdiofinal_worldopened.1 = libc_active_rootsfinal_worldopened ∧ stdout_usablelibc_stdiofinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stdout_filelibc_streamsfinal_worldopened.1 ∧ libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
split ; exact Hlocale |
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
∧
∧
∧
shutdown_uniquefinal_worldopened.2
∧
−2 ^ 31 ≤ shutdown_statusfinal_worldopened.2 < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutfinal_worldopened ≠ ptr_addrlibc_stderrfinal_worldopened ∧ stdio_rootslibc_stdiofinal_worldopened.1 = libc_active_rootsfinal_worldopened ∧ stdout_usablelibc_stdiofinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stdout_filelibc_streamsfinal_worldopened.1 ∧ libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
split ; exact He |
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
∧
∧
shutdown_uniquefinal_worldopened.2
∧
−2 ^ 31 ≤ shutdown_statusfinal_worldopened.2 < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutfinal_worldopened ≠ ptr_addrlibc_stderrfinal_worldopened ∧ stdio_rootslibc_stdiofinal_worldopened.1 = libc_active_rootsfinal_worldopened ∧ stdout_usablelibc_stdiofinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stdout_filelibc_streamsfinal_worldopened.1 ∧ libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
split
2 openopened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
focused goal
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
∧
shutdown_uniquefinal_worldopened.2
∧
−2 ^ 31 ≤ shutdown_statusfinal_worldopened.2 < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutfinal_worldopened ≠ ptr_addrlibc_stderrfinal_worldopened ∧ stdio_rootslibc_stdiofinal_worldopened.1 = libc_active_rootsfinal_worldopened ∧ stdout_usablelibc_stdiofinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stdout_filelibc_streamsfinal_worldopened.1 ∧ libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
{change stream_wfmkStreamByteOriented [ ] true
2 openopened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
stream_wforientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
deferred goal
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
∧
shutdown_uniquefinal_worldopened.2
∧
−2 ^ 31 ≤ shutdown_statusfinal_worldopened.2 < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutfinal_worldopened ≠ ptr_addrlibc_stderrfinal_worldopened ∧ stdio_rootslibc_stdiofinal_worldopened.1 = libc_active_rootsfinal_worldopened ∧ stdout_usablelibc_stdiofinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stdout_filelibc_streamsfinal_worldopened.1 ∧ libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
cbn [ stream_wf outstanding orientation ]
2 openopened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
stream_wforientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true
deferred goal
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
∧
shutdown_uniquefinal_worldopened.2
∧
−2 ^ 31 ≤ shutdown_statusfinal_worldopened.2 < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutfinal_worldopened ≠ ptr_addrlibc_stderrfinal_worldopened ∧ stdio_rootslibc_stdiofinal_worldopened.1 = libc_active_rootsfinal_worldopened ∧ stdout_usablelibc_stdiofinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stdout_filelibc_streamsfinal_worldopened.1 ∧ libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
split ; apply Forall_nil | intros _ ; reflexivity
deferred goal
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
∧
shutdown_uniquefinal_worldopened.2
∧
−2 ^ 31 ≤ shutdown_statusfinal_worldopened.2 < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutfinal_worldopened ≠ ptr_addrlibc_stderrfinal_worldopened ∧ stdio_rootslibc_stdiofinal_worldopened.1 = libc_active_rootsfinal_worldopened ∧ stdout_usablelibc_stdiofinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stdout_filelibc_streamsfinal_worldopened.1 ∧ libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
split
2 openopened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
focused goal
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
shutdown_uniquefinal_worldopened.2
∧
−2 ^ 31 ≤ shutdown_statusfinal_worldopened.2 < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutfinal_worldopened ≠ ptr_addrlibc_stderrfinal_worldopened ∧ stdio_rootslibc_stdiofinal_worldopened.1 = libc_active_rootsfinal_worldopened ∧ stdout_usablelibc_stdiofinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stdout_filelibc_streamsfinal_worldopened.1 ∧ libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
{change stream_wfmkStreamByteOriented 67; 10 false
2 openopened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
stream_wforientation ≔ ByteOriented; outstanding ≔ 67; 10; stream_error ≔ false
deferred goal
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
shutdown_uniquefinal_worldopened.2
∧
−2 ^ 31 ≤ shutdown_statusfinal_worldopened.2 < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutfinal_worldopened ≠ ptr_addrlibc_stderrfinal_worldopened ∧ stdio_rootslibc_stdiofinal_worldopened.1 = libc_active_rootsfinal_worldopened ∧ stdout_usablelibc_stdiofinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stdout_filelibc_streamsfinal_worldopened.1 ∧ libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
cbn [ stream_wf outstanding orientation ]
2 openopened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
stream_wforientation ≔ ByteOriented; outstanding ≔ 67; 10; stream_error ≔ false
deferred goal
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
shutdown_uniquefinal_worldopened.2
∧
−2 ^ 31 ≤ shutdown_statusfinal_worldopened.2 < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutfinal_worldopened ≠ ptr_addrlibc_stderrfinal_worldopened ∧ stdio_rootslibc_stdiofinal_worldopened.1 = libc_active_rootsfinal_worldopened ∧ stdout_usablelibc_stdiofinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stdout_filelibc_streamsfinal_worldopened.1 ∧ libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
split ; repeat constructor ; lia | intros _ ; reflexivity
deferred goal
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
shutdown_uniquefinal_worldopened.2
∧
−2 ^ 31 ≤ shutdown_statusfinal_worldopened.2 < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutfinal_worldopened ≠ ptr_addrlibc_stderrfinal_worldopened ∧ stdio_rootslibc_stdiofinal_worldopened.1 = libc_active_rootsfinal_worldopened ∧ stdout_usablelibc_stdiofinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stdout_filelibc_streamsfinal_worldopened.1 ∧ libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
split ; exact Hu |
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
−2 ^ 31 ≤ shutdown_statusfinal_worldopened.2 < 2 ^ 31
∧
_
⇒
True
∧
ptr_addrlibc_stdoutfinal_worldopened ≠ ptr_addrlibc_stderrfinal_worldopened ∧ stdio_rootslibc_stdiofinal_worldopened.1 = libc_active_rootsfinal_worldopened ∧ stdout_usablelibc_stdiofinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stdout_filelibc_streamsfinal_worldopened.1 ∧ libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
split ; exact Hstatus |
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
_
⇒
True
∧
ptr_addrlibc_stdoutfinal_worldopened ≠ ptr_addrlibc_stderrfinal_worldopened ∧ stdio_rootslibc_stdiofinal_worldopened.1 = libc_active_rootsfinal_worldopened ∧ stdout_usablelibc_stdiofinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stdout_filelibc_streamsfinal_worldopened.1 ∧ libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
split ; exact Hphase |
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
ptr_addrlibc_stdoutfinal_worldopened ≠ ptr_addrlibc_stderrfinal_worldopened ∧ stdio_rootslibc_stdiofinal_worldopened.1 = libc_active_rootsfinal_worldopened ∧ stdout_usablelibc_stdiofinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stdout_filelibc_streamsfinal_worldopened.1 ∧ libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
split ; exact Hdistinct |
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
stdio_rootslibc_stdiofinal_worldopened.1 = libc_active_rootsfinal_worldopened ∧ stdout_usablelibc_stdiofinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stdout_filelibc_streamsfinal_worldopened.1 ∧ libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
split ; exact Hroots |
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
stdout_usablelibc_stdiofinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stdout_filelibc_streamsfinal_worldopened.1 ∧ libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
split ; exact Hout |
opened :
bool
Hrep :
True
Hlocale :
Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True T.changed_errno libc_localeT.F.worldopened.1
He :
errno_cellT.changed_errno libc_errnoT.F.worldopened.1
Hu :
shutdown_uniqueT.F.worldopened.2
Hstatus :
−2 ^ 31 ≤ shutdown_statusT.F.worldopened.2 < 2 ^ 31
Hphase :
_
⇒
True
Hdistinct :
ptr_addrlibc_stdoutT.F.worldopened ≠ ptr_addrlibc_stderrT.F.worldopened
Hroots :
stdio_rootslibc_stdioT.F.worldopened.1 = libc_active_rootsT.F.worldopened
Hout :
stdout_usablelibc_stdioT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stdout_filelibc_streamsT.F.worldopened.1
Herr :
libc_stderr_openlibc_streamsT.F.worldopened.1 = true → libc_file_readyT.changed_errno libc_errnoT.F.worldopened.1 libc_stderr_filelibc_streamsT.F.worldopened.1
Hsep :
libc_release_separatedT.changed_errno T.F.worldopened
⊢
libc_stderr_openlibc_streamsfinal_worldopened.1 = true → libc_file_readyT.changed_errno libc_errnofinal_worldopened.1 libc_stderr_filelibc_streamsfinal_worldopened.1 ∧ libc_release_separatedT.changed_errno final_worldopened
split ; exact Herr | exact Hsep
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros opened
destruct T.changed_readyopened as Hrep & Hlocale & He & _ & _ & Hu & Hstatus & Hphase & Hdistinct & Hroots & Hout & Herr & Hsep
split ; exact Hrep |
split ; exact Hlocale |
split ; exact He |
split
{change stream_wfmkStreamByteOriented [ ] true
cbn [ stream_wf outstanding orientation ]
split ; apply Forall_nil | intros _ ; reflexivity
split
{change stream_wfmkStreamByteOriented 67; 10 false
cbn [ stream_wf outstanding orientation ]
split ; repeat constructor ; lia | intros _ ; reflexivity
split ; exact Hu |
split ; exact Hstatus |
split ; exact Hphase |
split ; exact Hdistinct |
split ; exact Hroots |
split ; exact Hout |
split ; exact Herr | exact Hsep
<[PName−2 ≔ if opened then VStreamOpentoken_handleT.out else VStreamtoken_handleT.out None]><[PName−3 ≔ VStreamOpentoken_handleT.err]>StreamHandleChecks.heap
∀ opened
agreesconversion_mem heapopened
Explore proof 7 tactics
Initial goal
⊢
∀opened : bool, agreesconversion_mem heapopened
intros opened l v Hl
unfold heap in Hl
opened :
bool
l :
v :
Hl :
<[PName−2 ≔ if opened then VStreamOpentoken_handleT.out else VStreamtoken_handleT.out None]><[PName−3 ≔ VStreamOpentoken_handleT.err]>StreamHandleChecks.heap !! l = Somev
apply lookup_insert_Some in Hl as El Ev | _ Hl
2 openfocused goal
opened :
bool
l :
v :
Hl :
<[PName−3 ≔ VStreamOpentoken_handleT.err]>StreamHandleChecks.heap !! l = Somev
–subst l v
2 openopened :
bool
⊢
else
VStreamtoken_handleT.out None
deferred goal
opened :
bool
l :
v :
Hl :
<[PName−3 ≔ VStreamOpentoken_handleT.err]>StreamHandleChecks.heap !! l = Somev
destruct opened ; exact I
deferred goal
opened :
bool
l :
v :
Hl :
<[PName−3 ≔ VStreamOpentoken_handleT.err]>StreamHandleChecks.heap !! l = Somev
–apply lookup_insert_Some in Hl as El Ev | _ Hl ; subst l v ; exact I |
exact StreamHandleChecks.heap_agreesl v Hl
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros opened l v Hl
unfold heap in Hl
apply lookup_insert_Some in Hl as El Ev | _ Hl
–subst l v
destruct opened ; exact I
–apply lookup_insert_Some in Hl as El Ev | _ Hl ; subst l v ; exact I |
exact StreamHandleChecks.heap_agreesl v Hl
∀ opened
libc_diagnostic_wiλ_ _ ⇒ True native T.out T.err 5120 0 conversion_mem F.worldopened heapopened
Proof 56 steps Qed
intros opened
assert Hkeys : ∀l v, stream_data_heap1024 2048 heapopened !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
{intros l v Hl Hmem
apply stream_data_lookup in Hl as Hl & Hno & Hne
unfold StreamHandleChecks.heap in Hl
unfold HelloErrnoChecks.heap in Hl
apply elem_of_list_to_map_2 in Hl
apply list_elem_of_fmap
exists l, v
auto
split
–split ; split ; reflexivity | simpl ; lia |
split ; split ; reflexivity | simpl ; lia |
split ; discriminate |
split ; discriminate |
split ; reflexivity |
split ; reflexivity |
split
–split ; reflexivity |
split ; reflexivity
split
{unfold stream_current , heap
cbn [ T.err token_key ]
rewrite lookup_insert_ne ; | discriminate
rewrite lookup_insert_eq
split ; reflexivity |
exists mkStreamInfo2 stdout_initial 3
destruct opened ; reflexivity
intros d → | →
all: split ; | intros base l v Hin ; destruct opened ; contradiction
all: split ; apply F.ready |
all: split ; reflexivity |
all: split ; intros root a Hin ; destruct opened ; contradiction |
all: split ; intros base l v Hin ; destruct opened ; contradiction |
all: intros l v Hl Hnot ; destruct l as base | base off | base off | key ; try exact I
all: exfalso ; apply Hnot ; eapply Hkeys ; exact Hl | exact I
–split ; intros root a |
unfold diagnostic_name , heap
cbn [ T.out T.err token_key ]
rewrite lookup_insert_eq
rewrite lookup_insert_ne ; | discriminate
rewrite lookup_insert_eq
destruct opened ; auto
∀ opened
contract_prespec words conversion_mem F.worldopened
Explore proof 24 tactics
Initial goal
⊢
∀opened : bool, contract_prespec words conversion_mem F.worldopened
intros opened
opened :
bool
⊢
contract_prespec words conversion_mem F.worldopened
split
2 openopened :
bool
⊢
contract_prediagnostic_contracterror_format_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False libc_stdout libc_stderr libc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native words conversion_mem F.worldopened
focused goal
opened :
bool
–split
3 openopened :
bool
⊢
contract_preerror_format_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False libc_stdout libc_stderr libc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native words conversion_mem F.worldopened
focused goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
+exists 0, 0, fmt, [ ], 67, 67, mkStreamInfo2 stdout_initial 3
3 openopened :
bool
⊢
words = WInt0; WInt0; WPtrfmt ∧ 0 ≤ 0 < 2 ^ 32 ∧ 0 ≤ 0 < 2 ^ 32 ∧ c_stringconversion_mem fmt 67 ∧ narrow_formatconversion_mem 67 [ ] 67 ∧ diagnostic_readylibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native conversion_mem F.worldopened ∧ Forallwritable_spanconversion_mem diagnostic_writeslibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native F.worldopened ∧ stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened libc_stderrF.worldopened stream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ∧ orientationstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ≠ WideOriented ∧ libc_stdoutF.worldopened ≠ libc_stderrF.worldopened
deferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
split ; reflexivity |
3 openopened :
bool
⊢
0 ≤ 0 < 2 ^ 32 ∧ 0 ≤ 0 < 2 ^ 32 ∧ c_stringconversion_mem fmt 67 ∧ narrow_formatconversion_mem 67 [ ] 67 ∧ diagnostic_readylibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native conversion_mem F.worldopened ∧ Forallwritable_spanconversion_mem diagnostic_writeslibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native F.worldopened ∧ stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened libc_stderrF.worldopened stream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ∧ orientationstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ≠ WideOriented ∧ libc_stdoutF.worldopened ≠ libc_stderrF.worldopened
deferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
split ; lia |
3 openopened :
bool
⊢
0 ≤ 0 < 2 ^ 32 ∧ c_stringconversion_mem fmt 67 ∧ narrow_formatconversion_mem 67 [ ] 67 ∧ diagnostic_readylibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native conversion_mem F.worldopened ∧ Forallwritable_spanconversion_mem diagnostic_writeslibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native F.worldopened ∧ stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened libc_stderrF.worldopened stream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ∧ orientationstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ≠ WideOriented ∧ libc_stdoutF.worldopened ≠ libc_stderrF.worldopened
deferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
split ; lia |
3 openopened :
bool
⊢
c_stringconversion_mem fmt 67 ∧ narrow_formatconversion_mem 67 [ ] 67 ∧ diagnostic_readylibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native conversion_mem F.worldopened ∧ Forallwritable_spanconversion_mem diagnostic_writeslibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native F.worldopened ∧ stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened libc_stderrF.worldopened stream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ∧ orientationstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ≠ WideOriented ∧ libc_stdoutF.worldopened ≠ libc_stderrF.worldopened
deferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
split
4 openopened :
bool
focused goal
opened :
bool
⊢
narrow_formatconversion_mem 67 [ ] 67 ∧ diagnostic_readylibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native conversion_mem F.worldopened ∧ Forallwritable_spanconversion_mem diagnostic_writeslibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native F.worldopened ∧ stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened libc_stderrF.worldopened stream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ∧ orientationstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ≠ WideOriented ∧ libc_stdoutF.worldopened ≠ libc_stderrF.worldopened
deferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
∗vm_compute
4 openopened :
bool
⊢
Someok = Someok ∧ Datatypes.Lt = Datatypes.Lt ∧ Datatypes.Lt = Datatypes.Lt ∧ 67 = 67 ∧ 0 = 0
deferred goal
opened :
bool
⊢
narrow_formatconversion_mem 67 [ ] 67 ∧ diagnostic_readylibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native conversion_mem F.worldopened ∧ Forallwritable_spanconversion_mem diagnostic_writeslibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native F.worldopened ∧ stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened libc_stderrF.worldopened stream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ∧ orientationstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ≠ WideOriented ∧ libc_stdoutF.worldopened ≠ libc_stderrF.worldopened
deferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
repeat split ; congruence
3 opendeferred goal
opened :
bool
⊢
narrow_formatconversion_mem 67 [ ] 67 ∧ diagnostic_readylibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native conversion_mem F.worldopened ∧ Forallwritable_spanconversion_mem diagnostic_writeslibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native F.worldopened ∧ stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened libc_stderrF.worldopened stream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ∧ orientationstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ≠ WideOriented ∧ libc_stdoutF.worldopened ≠ libc_stderrF.worldopened
deferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
∗split ; apply format_literal ; lia | discriminate | constructor |
3 openopened :
bool
⊢
diagnostic_readylibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native conversion_mem F.worldopened ∧ Forallwritable_spanconversion_mem diagnostic_writeslibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native F.worldopened ∧ stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened libc_stderrF.worldopened stream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ∧ orientationstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ≠ WideOriented ∧ libc_stdoutF.worldopened ≠ libc_stderrF.worldopened
deferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
split ; split ; exact I | apply F.ready |
3 openopened :
bool
⊢
Forallwritable_spanconversion_mem diagnostic_writeslibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native F.worldopened ∧ stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened libc_stderrF.worldopened stream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ∧ orientationstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ≠ WideOriented ∧ libc_stdoutF.worldopened ≠ libc_stderrF.worldopened
deferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
split ; constructor |
3 openopened :
bool
⊢
stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened libc_stderrF.worldopened stream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ∧ orientationstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ≠ WideOriented ∧ libc_stdoutF.worldopened ≠ libc_stderrF.worldopened
deferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
split
4 openopened :
bool
⊢
stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened libc_stderrF.worldopened stream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3
focused goal
opened :
bool
⊢
orientationstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ≠ WideOriented ∧ libc_stdoutF.worldopened ≠ libc_stderrF.worldopened
deferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
--destruct libc_stream_openλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False conversion_mem F.worldopened file_handleF.err_file F.err_file F.readyopened ltac:destruct opened ; reflexivity as info Hopen
4 openopened :
bool
info :
Hopen :
stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened file_handleF.err_file info
⊢
stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened libc_stderrF.worldopened stream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3
deferred goal
opened :
bool
⊢
orientationstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ≠ WideOriented ∧ libc_stdoutF.worldopened ≠ libc_stderrF.worldopened
deferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
destruct Hopen as Hr Hlookup Hrest
4 openopened :
bool
info :
Hr :
stream_replibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened
Hlookup :
stream_atlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False F.worldopened file_handleF.err_file = Someinfo
Hrest :
stream_protocolinfo = stream_state_atlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False F.worldopened file_handleF.err_file ∧ stream_info_wfinfo ∧ Forallwritable_spanconversion_mem stream_writeslibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False F.worldopened file_handleF.err_file
⊢
stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened libc_stderrF.worldopened stream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3
deferred goal
opened :
bool
⊢
orientationstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ≠ WideOriented ∧ libc_stdoutF.worldopened ≠ libc_stderrF.worldopened
deferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
assert info = mkStreamInfo2 stdout_initial 3 as →
5 openopened :
bool
info :
Hr :
stream_replibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened
Hlookup :
stream_atlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False F.worldopened file_handleF.err_file = Someinfo
Hrest :
stream_protocolinfo = stream_state_atlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False F.worldopened file_handleF.err_file ∧ stream_info_wfinfo ∧ Forallwritable_spanconversion_mem stream_writeslibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False F.worldopened file_handleF.err_file
⊢
info = stream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3
focused goal
opened :
bool
Hr :
stream_replibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened
Hrest :
stream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 = stream_state_atlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False F.worldopened file_handleF.err_file ∧ stream_info_wfstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ∧ Forallwritable_spanconversion_mem stream_writeslibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False F.worldopened file_handleF.err_file
Hlookup :
stream_atlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False F.worldopened file_handleF.err_file = Somestream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3
⊢
stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened libc_stderrF.worldopened stream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3
deferred goal
opened :
bool
⊢
orientationstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ≠ WideOriented ∧ libc_stdoutF.worldopened ≠ libc_stderrF.worldopened
deferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
{destruct opened ; injection Hlookup ; auto
4 opendeferred goal
opened :
bool
Hr :
stream_replibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened
Hrest :
stream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 = stream_state_atlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False F.worldopened file_handleF.err_file ∧ stream_info_wfstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ∧ Forallwritable_spanconversion_mem stream_writeslibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False F.worldopened file_handleF.err_file
Hlookup :
stream_atlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False F.worldopened file_handleF.err_file = Somestream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3
⊢
stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False conversion_mem F.worldopened libc_stderrF.worldopened stream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3
deferred goal
opened :
bool
⊢
orientationstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ≠ WideOriented ∧ libc_stdoutF.worldopened ≠ libc_stderrF.worldopened
deferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
exact conjHr conjHlookup Hrest
3 opendeferred goal
opened :
bool
⊢
orientationstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ≠ WideOriented ∧ libc_stdoutF.worldopened ≠ libc_stderrF.worldopened
deferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
--split ; discriminate | destruct opened ; discriminate
2 opendeferred goal
opened :
bool
⊢
∃status : Z, error_wordswords status
deferred goal
opened :
bool
+exists 0, 0, fmt, [ ]
2 opendeferred goal
opened :
bool
split ; reflexivity | lia
deferred goal
opened :
bool
–exists 0, fmt, [ ]
split ; reflexivity | lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros opened
split
–split
+exists 0, 0, fmt, [ ], 67, 67, mkStreamInfo2 stdout_initial 3
split ; reflexivity |
split ; lia |
split ; lia |
split
∗vm_compute
repeat split ; congruence
∗split ; apply format_literal ; lia | discriminate | constructor |
split ; split ; exact I | apply F.ready |
split ; constructor |
split
--destruct libc_stream_openλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False conversion_mem F.worldopened file_handleF.err_file F.err_file F.readyopened ltac:destruct opened ; reflexivity as info Hopen
destruct Hopen as Hr Hlookup Hrest
assert info = mkStreamInfo2 stdout_initial 3 as →
{destruct opened ; injection Hlookup ; auto
exact conjHr conjHlookup Hrest
--split ; discriminate | destruct opened ; discriminate
+exists 0, 0, fmt, [ ]
split ; reflexivity | lia
–exists 0, fmt, [ ]
split ; reflexivity | lia
∀ opened
error_format_prefixF.model libc_stdout libc_stderr context words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 T.changed_errno final_worldopened
Proof 84 steps Qed
intros opened
exists 0, 0, fmt, [ ], 67, 67, mkStreamInfo2 stdout_initial 3, mkStreamInfo2 mkStreamByteOriented 67; 10 false 3, 67; 10, 67; 10, Accept67; 10
split ; reflexivity |
split ; vm_compute ; repeat split ; congruence |
split ; apply format_literal ; lia | discriminate | constructor |
split ; reflexivity |
split
–repeat constructor ; exists [ ] ; reflexivity |
constructor
–split ; destruct opened ; reflexivity |
split
+split ; apply final_ready |
split ; destruct opened ; reflexivity |
split ; reflexivity |
split
∗split ; split ; repeat constructor ; lia | reflexivity | simpl ; lia
∗change Forallwritable_spanT.changed_errno errno_span5120 0
constructor ; exact proj1proj2proj1proj2proj2final_readyopened | constructor
+split ; reflexivity |
split ; reflexivity |
split
∗eapply stream_next ; apply stream_accept ; discriminate | repeat constructor ; lia | constructor
∗split ; reflexivity |
split
--destruct opened
++exists mkStreamInfo1 mkStreamByteOriented [ ] true 7
split ; reflexivity |
split ; reflexivity |
split ; reflexivity |
split ; reflexivity | apply F.close_settles
++split ; reflexivity
--split ; split ; exact I | apply final_ready |
split ; split ; exact I | repeat split ; reflexivity |
split
++destruct opened
**split
---intros root E |
subst root
split
+++intros a Ha
left
exists errno_span5120 0
split ; left ; reflexivity |
split
***exact proj1proj2proj1proj2proj2final_readytrue
***exact Ha
**split ; intros root |
split ; intros x ; contradiction
++split
**split
---intros root E |
subst root
split
+++intros a Ha
left
exists errno_span5120 0
split ; left ; reflexivity |
split
***exact proj1proj2proj1proj2proj2final_readyopened
***exact Ha
**split ; intros root |
split ; right ; reflexivity |
intros a _ _
reflexivity
∀ opened
D.M.E.invokespec CVoid args words InterpRuntime.start conversion_mem F.worldopened StreamBytes2 67; 10 CallReturn[ ] InterpRuntime.start T.changed_errno final_worldopened
Explore proof 30 tactics
Initial goal
⊢
∀opened : bool, D.M.E.invokespec CVoid args words InterpRuntime.start conversion_mem F.worldopened StreamBytes2 67; 10 CallReturn[ ] InterpRuntime.start T.changed_errno final_worldopened
intros opened
opened :
bool
⊢
D.M.E.invokespec CVoid args words InterpRuntime.start conversion_mem F.worldopened StreamBytes2 67; 10 CallReturn[ ] InterpRuntime.start T.changed_errno final_worldopened
eapply D.M.E.invoke_normal with born := [ ]
7 openopened :
bool
focused goal
opened :
bool
⊢
contract_prespec words conversion_mem F.worldopened
focused goal
opened :
bool
⊢
D.M.E.prefixspec words InterpRuntime.start conversion_mem F.worldopened [ ] StreamBytes2 67; 10 InterpRuntime.start T.changed_errno final_worldopened
focused goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
focused goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
focused goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
focused goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
–split ; reflexivity |
7 openopened :
bool
⊢
contract_abierror_format_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False libc_stdout libc_stderr libc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native CVoid args ∧ ∃status errnum format : value rest : listarg, args = ArgW status :: ArgW errnum :: ArgP format :: rest
deferred goal
opened :
bool
⊢
contract_prespec words conversion_mem F.worldopened
deferred goal
opened :
bool
⊢
D.M.E.prefixspec words InterpRuntime.start conversion_mem F.worldopened [ ] StreamBytes2 67; 10 InterpRuntime.start T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
split
8 openopened :
bool
⊢
contract_abierror_format_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False libc_stdout libc_stderr libc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native CVoid args
focused goal
deferred goal
opened :
bool
⊢
contract_prespec words conversion_mem F.worldopened
deferred goal
opened :
bool
⊢
D.M.E.prefixspec words InterpRuntime.start conversion_mem F.worldopened [ ] StreamBytes2 67; 10 InterpRuntime.start T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
+split ; reflexivity |
8 openopened :
bool
deferred goal
deferred goal
opened :
bool
⊢
contract_prespec words conversion_mem F.worldopened
deferred goal
opened :
bool
⊢
D.M.E.prefixspec words InterpRuntime.start conversion_mem F.worldopened [ ] StreamBytes2 67; 10 InterpRuntime.start T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
exists Const0, Const0, Const0, [ ]
8 opendeferred goal
deferred goal
opened :
bool
⊢
contract_prespec words conversion_mem F.worldopened
deferred goal
opened :
bool
⊢
D.M.E.prefixspec words InterpRuntime.start conversion_mem F.worldopened [ ] StreamBytes2 67; 10 InterpRuntime.start T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
split ; reflexivity | constructor
7 opendeferred goal
deferred goal
opened :
bool
⊢
contract_prespec words conversion_mem F.worldopened
deferred goal
opened :
bool
⊢
D.M.E.prefixspec words InterpRuntime.start conversion_mem F.worldopened [ ] StreamBytes2 67; 10 InterpRuntime.start T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
+exists Const0, Const0, Const0, [ ]
7 opendeferred goal
opened :
bool
⊢
contract_prespec words conversion_mem F.worldopened
deferred goal
opened :
bool
⊢
D.M.E.prefixspec words InterpRuntime.start conversion_mem F.worldopened [ ] StreamBytes2 67; 10 InterpRuntime.start T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
reflexivity
6 opendeferred goal
opened :
bool
⊢
contract_prespec words conversion_mem F.worldopened
deferred goal
opened :
bool
⊢
D.M.E.prefixspec words InterpRuntime.start conversion_mem F.worldopened [ ] StreamBytes2 67; 10 InterpRuntime.start T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
–apply admitted
5 opendeferred goal
opened :
bool
⊢
D.M.E.prefixspec words InterpRuntime.start conversion_mem F.worldopened [ ] StreamBytes2 67; 10 InterpRuntime.start T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
–split
6 openopened :
bool
⊢
D.M.E.effectscontract_sourcesspec words conversion_mem F.worldopened contract_writesspec words conversion_mem F.worldopened contract_releasesspec words conversion_mem F.worldopened contract_requestsspec words conversion_mem F.worldopened InterpRuntime.start conversion_mem [ ] InterpRuntime.start T.changed_errno [ ]
focused goal
opened :
bool
⊢
contract_prefixspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
+eapply D.M.E.effects_local ; apply local_store_bytes | constructor
6 openopened :
bool
⊢
∀b : Z, 5120 ≤ b < 5120 + 4 → write_authoritycontract_writesspec words conversion_mem F.worldopened [ ] conversion_mem b
deferred goal
opened :
bool
⊢
contract_prefixspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
intros a Ha
6 openopened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
⊢
write_authoritycontract_writesspec words conversion_mem F.worldopened [ ] conversion_mem a
deferred goal
opened :
bool
⊢
contract_prefixspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
left
6 openopened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
⊢
∃s : span, Ins contract_writesspec words conversion_mem F.worldopened ∧ writable_spanconversion_mem s ∧ span_containss a
deferred goal
opened :
bool
⊢
contract_prefixspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
exists errno_span5120 0
6 openopened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
⊢
Inerrno_span5120 0 contract_writesspec words conversion_mem F.worldopened ∧ writable_spanconversion_mem errno_span5120 0 ∧ span_containserrno_span5120 0 a
deferred goal
opened :
bool
⊢
contract_prefixspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
split ; apply in_or_app ; right ; apply in_or_app ; left ; destruct opened ; left ; reflexivity |
6 openopened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
⊢
writable_spanconversion_mem errno_span5120 0 ∧ span_containserrno_span5120 0 a
deferred goal
opened :
bool
⊢
contract_prefixspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
split
7 openopened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
focused goal
opened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
⊢
span_containserrno_span5120 0 a
deferred goal
opened :
bool
⊢
contract_prefixspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
∗exact proj1proj2proj1proj2proj2F.readyopened
6 opendeferred goal
opened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
⊢
span_containserrno_span5120 0 a
deferred goal
opened :
bool
⊢
contract_prefixspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
∗unfold span_contains , errno_span
6 openopened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
deferred goal
opened :
bool
⊢
contract_prefixspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
simpl
6 openopened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
⊢
5120 + 0 ≤ a < 5120 + 0 + 4
deferred goal
opened :
bool
⊢
contract_prefixspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
lia
5 opendeferred goal
opened :
bool
⊢
contract_prefixspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
+split ; apply format_prefix | constructor ; reflexivity | constructor
4 opendeferred goal
opened :
bool
⊢
contract_postspec words conversion_mem F.worldopened [ ] StreamBytes2 67; 10 CallReturn[ ] T.changed_errno final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
–split ; split ; apply format_prefix | reflexivity | reflexivity
3 opendeferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
–intros why Hbad
3 open⊢
False
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
discriminate Hbad
2 opendeferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
–intros vs Hvs
2 open⊢
return_shapecontract_returnsspec vs ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno vs
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
injection Hvs as ←
2 openopened :
bool
⊢
return_shapecontract_returnsspec [ ] ∧ Forallword_authoritycontract_sourcesspec words conversion_mem F.worldopened [ ] T.changed_errno [ ]
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
split ; reflexivity | constructor
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
–intros status Hbad
⊢
∃before : listevent, StreamBytes2 67; 10 = before ++ ProcessExitstatus
discriminate Hbad
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros opened
eapply D.M.E.invoke_normal with born := [ ]
–split ; reflexivity |
split
–apply admitted
–split
+eapply D.M.E.effects_local ; apply local_store_bytes | constructor
intros a Ha
left
exists errno_span5120 0
split ; apply in_or_app ; right ; apply in_or_app ; left ; destruct opened ; left ; reflexivity |
split
∗exact proj1proj2proj1proj2proj2F.readyopened
+split ; apply format_prefix | constructor ; reflexivity | constructor
–split ; split ; apply format_prefix | reflexivity | reflexivity
–intros why Hbad
discriminate Hbad
–intros vs Hvs
injection Hvs as ←
split ; reflexivity | constructor
–intros status Hbad
discriminate Hbad
Apply the actual frame with both lives/names and all errno bytes. The last sampled byte is one, not its old zero. Closed stdout stays a completed-closed observation; open stderr survives FIFO acceptance.
485Example framed_return: ∀opened, ∃ys, lengthys = 4%nat ∧ agreesT.changed_errno overwritebyte_ps5120 0 ys heapopened ∧ libc_diagnostic_wiλ_ _ ⇒ True native T.out T.err 5120 0 T.changed_errno final_worldopened overwritebyte_ps5120 0 ys heapopened ∧ overwritebyte_ps5120 0 ys heapopened !! PByte5120 3 = SomeVByte1 ∧ overwritebyte_ps5120 0 ys heapopened !! PName−2 = Someif opened then VStreamOpentoken_handleT.out else VStreamtoken_handleT.out None ∧ overwritebyte_ps5120 0 ys heapopened !! PName−3 = SomeVStreamOpentoken_handleT.err
Proof 41 steps Qed
intros opened
destruct D.error_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False native T.out T.err 5120 0 CVoid args words InterpRuntime.start conversion_mem F.worldopened StreamBytes2 67; 10 [ ] InterpRuntime.start T.changed_errno final_worldopened heapopened 0; 0; 0; 0 returning_callopened heap_agreesopened HelloErrnoChecks.disjoint HelloErrnoChecks.ready entry_wiopened eq_refl as ys & _ & Hlen & Hkeys & Ha & Hd & Hr & Hw
–intros l v Hin
destruct MemLogic.byte_ps_elem_ _ _ _ _ Hin as i & x & Hi & → & →
unfold heap , StreamHandleChecks.heap
repeat rewrite lookup_insert_ne ; | discriminate
unfold HelloErrnoChecks.heap
apply elem_of_list_to_map_1 ; | exact Hin
repeat apply base.NoDup_cons_2 ; set_solver |
apply base.NoDup_nil_2
–exists ys
split ; exact Hlen |
split ; exact Ha |
split ; exact Hw |
split
+destruct ys as | a | b | c | d rest ; try discriminate Hlen
destruct Ha_ _ Hl as _ Hbyte
change 1 = d in Hvalue
rewrite Hvalue
exact Hl
+split
∗rewrite overwrite_out ; unfold heap ; apply lookup_insert_eq |
rewrite byte_ps_keys
intros Hin
apply list_elem_of_fmap in Hin as i & E & _
discriminate E
∗rewrite overwrite_out
526Example evolving_protocols: libc_diagnostic_frameF.worldtrue final_worldtrue ∧ shutdown_pendingsndfinal_worldtrue = shutdown_pendingsndF.worldtrue ∧ sndfinal_worldtrue ≠ sndF.worldtrue ∧ outstandinglibc_stream_statefinal_worldtrue token_handleT.err = 67; 10
Explore proof 6 tactics
Initial goal
⊢
libc_diagnostic_frameF.worldtrue final_worldtrue ∧ shutdown_pendingfinal_worldtrue.2 = shutdown_pendingF.worldtrue.2 ∧ final_worldtrue.2 ≠ F.worldtrue.2 ∧ outstandinglibc_stream_statefinal_worldtrue token_handleT.err = 67; 10
split ; repeat split ; reflexivity |
⊢
shutdown_pendingfinal_worldtrue.2 = shutdown_pendingF.worldtrue.2 ∧ final_worldtrue.2 ≠ F.worldtrue.2 ∧ outstandinglibc_stream_statefinal_worldtrue token_handleT.err = 67; 10
split ; reflexivity |
⊢
final_worldtrue.2 ≠ F.worldtrue.2 ∧ outstandinglibc_stream_statefinal_worldtrue token_handleT.err = 67; 10
split ; | reflexivity
⊢
final_worldtrue.2 ≠ F.worldtrue.2
intros H
H :
final_worldtrue.2 = F.worldtrue.2
⊢
False
apply f_equalshutdown_stdout in H
H :
shutdown_stdoutfinal_worldtrue.2 = shutdown_stdoutF.worldtrue.2
⊢
False
discriminate H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; repeat split ; reflexivity |
split ; reflexivity |
split ; | reflexivity
intros H
apply f_equalshutdown_stdout in H
discriminate H
536Example exact_snapshot_rejected: ∀pending fifo, ¬diagnostic_nameT.out <[PName−2 ≔ VStreamtoken_handleT.out Somepending, fifo]>heaptrue
Explore proof 5 tactics
Initial goal
⊢
∀pending : Z fifo : listZ, ¬diagnostic_nameT.out <[PName−2 ≔ VStreamtoken_handleT.out Somepending, fifo]>heaptrue
intros
pending :
Z
fifo :
listZ
⊢
¬diagnostic_nameT.out <[PName−2 ≔ VStreamtoken_handleT.out Somepending, fifo]>heaptrue
unfold diagnostic_name
pending :
Z
fifo :
listZ
⊢
¬match <[PName−2 ≔ VStreamtoken_handleT.out Somepending, fifo]>heaptrue !! PNametoken_keyT.out with SomeVStream_ None SomeVStreamOpen_ None ⇒ True _ ⇒ False end
cbn [ T.out token_key ]
pending :
Z
fifo :
listZ
⊢
¬match <[PName−2 ≔ VStreamtoken_handleT.out Somepending, fifo]>heaptrue !! PName−2 with SomeVStream_ None SomeVStreamOpen_ None ⇒ True _ ⇒ False end
rewrite lookup_insert_eq
pending :
Z
fifo :
listZ
⊢
¬False
exact λH ⇒ H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
541Example exact_open_becomes_stale: stream_currentT.out F.worldtrue T.open_heap ∧ ¬stream_currentT.out final_worldtrue T.open_heap
Explore proof 8 tactics
Initial goal
⊢
stream_currentT.out F.worldtrue T.open_heap ∧ ¬stream_currentT.out final_worldtrue T.open_heap
split ; exact proj1T.open_snapshots_current |
⊢
¬stream_currentT.out final_worldtrue T.open_heap
unfold stream_current , T.open_heap
⊢
¬match <[PName−2 ≔ VStreamtoken_handleT.out Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleT.err Some3, [ ]]>StreamHandleChecks.heap !! PNametoken_keyT.out with SomeVStreamp snapshot ⇒ p = token_handleT.out ∧ stream_observationfinal_worldtrue p snapshot SomeVStreamOpenp ⇒ p = token_handleT.out ∧ ∃info : stream_info, libc_stream_atfinal_worldtrue p = Someinfo None ⇒ True _ ⇒ False end
cbn [ T.out token_key ]
⊢
¬match <[PName−2 ≔ VStreamtoken_handleT.out Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleT.err Some3, [ ]]>StreamHandleChecks.heap !! PName−2 with SomeVStreamp snapshot ⇒ p = token_handleT.out ∧ stream_observationfinal_worldtrue p snapshot SomeVStreamOpenp ⇒ p = token_handleT.out ∧ ∃info : stream_info, libc_stream_atfinal_worldtrue p = Someinfo None ⇒ True _ ⇒ False end
rewrite lookup_insert_eq
⊢
¬token_handleT.out = token_handleT.out ∧ stream_observationfinal_worldtrue token_handleT.out Some7, 65; 66
intros _ info Hlookup _ Hfifo
info :
Hlookup :
libc_stream_atfinal_worldtrue token_handleT.out = Someinfo
Hfifo :
outstandingstream_protocolinfo = 65; 66
⊢
False
change SomemkStreamInfo1 mkStreamByteOriented [ ] true 7 = Someinfo in Hlookup
info :
Hlookup :
Somestream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true; stream_pending ≔ 7 = Someinfo
Hfifo :
outstandingstream_protocolinfo = 65; 66
⊢
False
injection Hlookup as ←
Hfifo :
outstandingstream_protocolstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ [ ]; stream_error ≔ true; stream_pending ≔ 7 = 65; 66
⊢
False
discriminate Hfifo
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; exact proj1T.open_snapshots_current |
unfold stream_current , T.open_heap
cbn [ T.out token_key ]
rewrite lookup_insert_eq
intros _ info Hlookup _ Hfifo
change SomemkStreamInfo1 mkStreamByteOriented [ ] true 7 = Someinfo in Hlookup
injection Hlookup as ←
discriminate Hfifo
557Example private_byte_rejected: ∀m w h v, h !! PByte1024 0 = Somev → live_atm 1024 token_regionT.out → ¬libc_diagnostic_wiλ_ _ ⇒ True writing_native T.out T.err 5120 0 m w h
Explore proof 2 tactics
Initial goal
⊢
∀m : mem w : libc_world h : gmappiece pval v : pval, h !! PByte1024 0 = Somev → live_atm 1024 token_regionT.out → ¬libc_diagnostic_wiλ_ : mem _ : libc_world ⇒ True writing_native T.out T.err 5120 0 m w h
intros m w h v Hl Hlive _ Hroots _
⊢
False
exact StreamHandleChecks.private_byte_rejectedm h v Hl Hlive Hroots
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m w h v Hl Hlive _ Hroots _
exact StreamHandleChecks.private_byte_rejectedm h v Hl Hlive Hroots
565Example private_aux_rejected: ∀m w h v, h !! PAux1024 0 = Somev → live_atm 1024 token_regionT.out → ¬libc_diagnostic_wiλ_ _ ⇒ True writing_native T.out T.err 5120 0 m w h
Explore proof 2 tactics
Initial goal
⊢
∀m : mem w : libc_world h : gmappiece pval v : pval, h !! PAux1024 0 = Somev → live_atm 1024 token_regionT.out → ¬libc_diagnostic_wiλ_ : mem _ : libc_world ⇒ True writing_native T.out T.err 5120 0 m w h
intros m w h v Hl Hlive _ Hroots _
⊢
False
exact StreamHandleChecks.private_aux_rejectedm h v Hl Hlive Hroots
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m w h v Hl Hlive _ Hroots _
exact StreamHandleChecks.private_aux_rejectedm h v Hl Hlive Hroots
Explore proof 5 tactics
Initial goal
⊢
∀m : mem w : libc_world, ¬contract_prespec WInt1; WInt0; WPtrfmt m w
intros m w
m :
w :
apply nonzero_error_not_returning with status := 1
2 openm :
w :
⊢
error_wordsWInt1; WInt0; WPtrfmt 1
focused goal
m :
w :
⊢
1 ≠ 0
–exists 0, fmt, [ ]
2 opendeferred goal
m :
w :
⊢
1 ≠ 0
split ; reflexivity | lia
deferred goal
m :
w :
⊢
1 ≠ 0
–lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m w
apply nonzero_error_not_returning with status := 1
–exists 0, fmt, [ ]
split ; reflexivity | lia
–lia