rocq/theories/LibcStreamAdapter.v
World-owned callback snapshots, separate from locale string names. Main's output rules do not own/update these snapshots: callers must allocate or transfer them at callback entry.
From iris.proofmode Require Import proofmode
From iris.base_logic.lib Require Import gen_heap
From Stdlib Require Import ZArith List Lia
From Nanofil Require Import Term Syntax Values Memory Runtime Identity ExternalCalls ExternalMachine Stdio Shutdown Streams Libc LibcStreams Pieces Heap ContractFrame Logic StringLogic LentLogic LibcStreamLogic LibcErrnoLogic LibcStreamTokens
Open Scope Z_scope
Open Scope list_scope
A stable native handle and a reserved ghost key. The life region is separate from the mutable observations of FILE state.
PLivetoken_based, VLivetoken_regiond; PNametoken_keyd, VStreamtoken_handled Somepending, fifo
Ordinary completed closure does not freeze orientation or error. A resource prefix is not enough to establish this observation.
match snapshot with
Somepending, fifo
⇒
∃info, libc_stream_atw p = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo
Absent keys impose no snapshot requirement. A present key rejects wrong handles, malformed values and stale observations. This reads the current heap, never a fixed callback-entry snapshot.
Keys below the codec key (-1) do not overlap locale categories. Actual freshness against other adapters is still required by allocation.
ptr_captoken_handled = Objtoken_based ∧ token_keyd < −1
token_wfout ∧ token_wferr ∧ token_baseout ≠ token_baseerr ∧ token_keyout ≠ token_keyerr ∧ libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
Explore proof 1 tactics
Initial goal
⊢
∀d : stream_token pending : Z fifo : listZ, closed_psd.*1 = stream_psd pending fifo.*1
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
reflexivity
Explore proof 3 tactics
Initial goal
⊢
∀m : mem d : stream_token pending : Z fifo : listZ, live_atm token_based token_regiond → all_agreem stream_psd pending fifo
intros
split ; exact H |
⊢
all_agreem PNametoken_keyd, VStreamtoken_handled Somepending, fifo
split ; exact I
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
split ; exact H |
split ; exact I
Explore proof 3 tactics
Initial goal
⊢
∀m : mem d : stream_token, live_atm token_based token_regiond → all_agreem closed_psd
intros
split ; exact H |
⊢
all_agreem PNametoken_keyd, VStreamtoken_handled None
split ; exact I
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
split ; exact H |
split ; exact I
∀ d w h pending fifo
stream_currentd w h
∀l v, l, v ∈ stream_psd pending fifo → h !! l = Somev
∃info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo
Explore proof 8 tactics
Initial goal
⊢
∀d : stream_token w : libc_world h : gmappiece pval pending : Z fifo : listZ, stream_currentd w h → ∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev → ∃info : stream_info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo
intros d w h pending fifo Hcurrent Howned
⊢
∃info : stream_info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo
assert Hl : h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo
2 open⊢
h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo
focused goal
d :
w :
pending :
Z
fifo :
listZ
Hcurrent :
stream_currentd w h
Hl :
h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo
⊢
∃info : stream_info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo
{apply Howned
2 open⊢
PNametoken_keyd, VStreamtoken_handled Somepending, fifo ∈ stream_psd pending fifo
deferred goal
d :
w :
pending :
Z
fifo :
listZ
Hcurrent :
stream_currentd w h
Hl :
h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo
⊢
∃info : stream_info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo
unfold stream_ps
2 open⊢
PNametoken_keyd, VStreamtoken_handled Somepending, fifo ∈ PLivetoken_based, VLivetoken_regiond; PNametoken_keyd, VStreamtoken_handled Somepending, fifo
deferred goal
d :
w :
pending :
Z
fifo :
listZ
Hcurrent :
stream_currentd w h
Hl :
h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo
⊢
∃info : stream_info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo
set_solver
deferred goal
d :
w :
pending :
Z
fifo :
listZ
Hcurrent :
stream_currentd w h
Hl :
h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo
⊢
∃info : stream_info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo
unfold stream_current in Hcurrent
d :
w :
pending :
Z
fifo :
listZ
Hcurrent :
Hl :
h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo
⊢
∃info : stream_info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo
rewrite Hl in Hcurrent
d :
w :
pending :
Z
fifo :
listZ
Hl :
h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo
Hcurrent :
token_handled = token_handled ∧ stream_observationw token_handled Somepending, fifo
⊢
∃info : stream_info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo
exact proj2Hcurrent
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros d w h pending fifo Hcurrent Howned
assert Hl : h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo
unfold stream_current in Hcurrent
rewrite Hl in Hcurrent
exact proj2Hcurrent
∀ d w h
stream_currentd w h
∀l v, l, v ∈ closed_psd → h !! l = Somev
libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]
Explore proof 8 tactics
Initial goal
⊢
∀d : stream_token w : libc_world h : gmappiece pval, stream_currentd w h → ∀l : piece v : pval, l, v ∈ closed_psd → h !! l = Somev → libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]
intros d w h Hcurrent Howned
⊢
libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]
assert Hl : h !! PNametoken_keyd = SomeVStreamtoken_handled None
2 open⊢
h !! PNametoken_keyd = SomeVStreamtoken_handled None
focused goal
⊢
libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]
{apply Howned
2 open⊢
PNametoken_keyd, VStreamtoken_handled None ∈ closed_psd
deferred goal
⊢
libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]
unfold closed_ps
2 open⊢
PNametoken_keyd, VStreamtoken_handled None ∈ PLivetoken_based, VLivetoken_regiond; PNametoken_keyd, VStreamtoken_handled None
deferred goal
⊢
libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]
set_solver
deferred goal
⊢
libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]
unfold stream_current in Hcurrent
⊢
libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]
rewrite Hl in Hcurrent
d :
w :
Hl :
h !! PNametoken_keyd = SomeVStreamtoken_handled None
Hcurrent :
token_handled = token_handled ∧ stream_observationw token_handled None
⊢
libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]
exact proj2Hcurrent
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros d w h Hcurrent Howned
assert Hl : h !! PNametoken_keyd = SomeVStreamtoken_handled None
unfold stream_current in Hcurrent
rewrite Hl in Hcurrent
exact proj2Hcurrent
Recording independently live handles and CURRENT observations preserves the complete entry envelope. It does not recover unavailable fragments or change the world interpretation used by an existing WP.
∀ rep out err b o m w h op oq ep eq
agreesm h
stream_tokens_wirep out err b o m w h
live_atm token_baseout token_regionout
live_atm token_baseerr token_regionerr
stream_observationw token_handleout Someop, oq
stream_observationw token_handleerr Someep, eq
agreesm h′ ∧ stream_tokens_wirep out err b o m w h′
Proof 57 steps Qed
intros rep out err b o m w h op oq ep eq Ha Howf & Hewf & Hbase & Hkey & Hout & Herr & _ & _ & Hprivate Hol Hel Hoo Heo h′
assert Hdata : memory_keys_fromstream_data_heaptoken_baseout token_baseerr h' stream_data_heaptoken_baseout token_baseerr h
{intros l v Hl Hmem
apply stream_data_lookup in Hl as Hl & Hno & Hne
unfold h' in Hl
apply lookup_overwrite in Hl as Hin | _ Hold
–exists v
rewrite stream_data_lookup_ne ; assumption
split
{intros l v Hl
unfold h' in Hl
apply lookup_overwrite in Hl as Hin | _ Hold ; | exact Hal v Hold
eapply all_agree_elem ; | exact Hin
apply all_agree_app
split ; apply stream_ps_agree ; assumption
split ; exact Howf |
split ; exact Hewf |
split ; exact Hbase |
split ; exact Hkey |
split ; exact Hout |
split ; exact Herr |
split
{unfold stream_current , h'
rewrite lookup_insert_ne ; | discriminate
rewrite lookup_insert_eq
exact conjeq_refl Hoo
split
{unfold stream_current , h'
rewrite lookup_insert_ne ; | discriminate
rewrite lookup_insert_ne ; | congruence
rewrite lookup_insert_ne ; | discriminate
rewrite lookup_insert_eq
exact conjeq_refl Heo
intros d Hd
destruct Hprivated Hd as Hwi Hrel
split ; eapply errno_wi_heap ; eauto |
intros base l v Hin Hl Hmem
unfold h' in Hl
apply lookup_overwrite in Hl as Hnew | _ Hold ; | exact Hrelbase l v Hin Hold Hmem
apply list_elem_of_In in Hnew
cbn [ stream_ps app ] in Hnew
destruct Hnew as E | E | E | E | ; injection E as ← ← ; try contradiction
–intros E
subst base
eapply libc_handle_not_released ; exact proj1Hwi | left ; reflexivity | | exact Hin
rewrite Hout
exact proj1Howf
–intros E
subst base
eapply libc_handle_not_released ; exact proj1Hwi | right ; reflexivity | | exact Hin
rewrite Herr
exact proj1Hewf
Fresh ghost recording is not native allocation: both live_at facts and both current observations are independent premises. Freshness is against the authoritative heap, so no existing life is duplicated.
∀ rep out err b o m w h op oq ep eq
agreesm h
stream_tokens_wirep out err b o m w h
live_atm token_baseout token_regionout
live_atm token_baseerr token_regionerr
stream_observationw token_handleout Someop, oq
stream_observationw token_handleerr Someep, eq
Explore proof 14 tactics
Initial goal
⊢
agreesm h → stream_tokens_wirep out err b o m w h → live_atm token_baseout token_regionout → live_atm token_baseerr token_regionerr → stream_observationw token_handleout Someop, oq → stream_observationw token_handleerr Someep, eq → ∀l : piece v : pval, l, v ∈ stream_psout op oq ++ stream_pserr ep eq → h !! l = None → gen_heap_interph ⇛ gen_heap_interpoverwritestream_psout op oq ++ stream_pserr ep eq h ∗ ptsstream_psout op oq ∗ ptsstream_pserr ep eq ∗ ⌜agreesm overwritestream_psout op oq ++ stream_pserr ep eq h ∧ stream_tokens_wirep out err b o m w overwritestream_psout op oq ++ stream_pserr ep eq h⌝
intros Ha Hw Hol Hel Hoo Heo Hfresh
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
iIntros Hh
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Hh :
gen_heap_interph
∗
destruct Hw as Howf & Hewf & Hbase & Hkey & Hrest eqn: E
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Howf :
token_wfout
Hewf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hrest :
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
E :
Hw = conjHowf conjHewf conjHbase conjHkey Hrest
Hh :
gen_heap_interph
∗
iMod pts_alloch stream_psout op oq ++ stream_pserr ep eq with Hh as [Hh Hps]
3 openΣ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Howf :
token_wfout
Hewf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hrest :
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
E :
Hw = conjHowf conjHewf conjHbase conjHkey Hrest
focused goal
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Howf :
token_wfout
Hewf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hrest :
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
E :
Hw = conjHowf conjHewf conjHbase conjHkey Hrest
focused goal
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Howf :
token_wfout
Hewf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hrest :
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
E :
Hw = conjHowf conjHewf conjHbase conjHkey Hrest
∗
–clear - Hbase Hkey
3 opendeferred goal
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Howf :
token_wfout
Hewf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hrest :
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
E :
Hw = conjHowf conjHewf conjHbase conjHkey Hrest
deferred goal
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Howf :
token_wfout
Hewf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hrest :
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
E :
Hw = conjHowf conjHewf conjHbase conjHkey Hrest
∗
cbn [ stream_ps app fmap fst ]
3 open⊢
base.NoDuplist_fmappiece × pval%type piece fst PLivetoken_baseout, VLivetoken_regionout :: PNametoken_keyout, VStreamtoken_handleout Someop, oq :: stream_pserr ep eq
deferred goal
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Howf :
token_wfout
Hewf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hrest :
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
E :
Hw = conjHowf conjHewf conjHbase conjHkey Hrest
deferred goal
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Howf :
token_wfout
Hewf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hrest :
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
E :
Hw = conjHowf conjHewf conjHbase conjHkey Hrest
∗
repeat constructor ; set_solver
2 opendeferred goal
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Howf :
token_wfout
Hewf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hrest :
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
E :
Hw = conjHowf conjHewf conjHbase conjHkey Hrest
deferred goal
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Howf :
token_wfout
Hewf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hrest :
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
E :
Hw = conjHowf conjHewf conjHbase conjHkey Hrest
∗
–exact Hfresh
deferred goal
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Howf :
token_wfout
Hewf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hrest :
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
E :
Hw = conjHowf conjHewf conjHbase conjHkey Hrest
∗
–rewrite pts_app
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Howf :
token_wfout
Hewf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hrest :
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
E :
Hw = conjHowf conjHewf conjHbase conjHkey Hrest
∗
iDestruct Hps as [Ho He]
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Howf :
token_wfout
Hewf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hrest :
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
E :
Hw = conjHowf conjHewf conjHbase conjHkey Hrest
∗
iModIntro
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Howf :
token_wfout
Hewf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hrest :
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
E :
Hw = conjHowf conjHewf conjHbase conjHkey Hrest
∗
iFrame
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Howf :
token_wfout
Hewf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hrest :
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
E :
Hw = conjHowf conjHewf conjHbase conjHkey Hrest
∗
iPureIntro
Σ :
gFunctors
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
m :
w :
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Ha :
agreesm h
Hw :
stream_tokens_wirep out err b o m w h
Hol :
live_atm token_baseout token_regionout
Hel :
live_atm token_baseerr token_regionerr
Hoo :
stream_observationw token_handleout Someop, oq
Heo :
stream_observationw token_handleerr Someep, eq
Howf :
token_wfout
Hewf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hrest :
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
E :
Hw = conjHowf conjHewf conjHbase conjHkey Hrest
eapply stream_entry_frame ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Ha Hw Hol Hel Hoo Heo Hfresh
iIntros Hh
destruct Hw as Howf & Hewf & Hbase & Hkey & Hrest eqn: E
–exact Hfresh
Callback entry allocates the reserved snapshot key, while retaining an already owned life piece. Neither the life nor a fresh ghost resource can be fabricated by the pure interpretation.
∀ d pending fifo w h
stream_observationw token_handled Somepending, fifo
gen_heap_interph ∗ ptsPLivetoken_based, VLivetoken_regiond ⇛ gen_heap_interp<[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h ∗ ptsstream_psd pending fifo ∗ ⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝
Explore proof 13 tactics
Initial goal
Σ :
gFunctors
d :
pending :
Z
fifo :
listZ
w :
⊢
h !! PNametoken_keyd = None → stream_observationw token_handled Somepending, fifo → gen_heap_interph ∗ ptsPLivetoken_based, VLivetoken_regiond ⇛ gen_heap_interp<[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h ∗ ptsstream_psd pending fifo ∗ ⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝
intros Hfresh Hobs
⊢
gen_heap_interph ∗ ptsPLivetoken_based, VLivetoken_regiond ⇛ gen_heap_interp<[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h ∗ ptsstream_psd pending fifo ∗ ⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝
iIntros [Hh Hlife]
Hh :
gen_heap_interph
Hlife :
∗
|⇛ gen_heap_interp<[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h ∗ ptsstream_psd pending fifo ∗ ⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝
iMod gen_heap_alloc_ PNametoken_keyd VStreamtoken_handled Somepending, fifo with Hh as (Hh & Hname & _) ; exact Hfresh |
Hlife :
Hh :
gen_heap_interp<[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h
Hname :
pointstoPNametoken_keyd DfracOwn1 VStreamtoken_handled Somepending, fifo
∗
|⇛ gen_heap_interp<[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h ∗ ptsstream_psd pending fifo ∗ ⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝
iModIntro
Hlife :
Hh :
gen_heap_interp<[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h
Hname :
pointstoPNametoken_keyd DfracOwn1 VStreamtoken_handled Somepending, fifo
∗
gen_heap_interp<[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h ∗ ptsstream_psd pending fifo ∗ ⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝
iSplitL Hh ; iExact Hh |
Hlife :
Hname :
pointstoPNametoken_keyd DfracOwn1 VStreamtoken_handled Somepending, fifo
∗
ptsstream_psd pending fifo ∗ ⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝
iSplitL Hlife Hname
2 openHlife :
Hname :
pointstoPNametoken_keyd DfracOwn1 VStreamtoken_handled Somepending, fifo
∗
focused goal
∗
⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝
–rewrite / stream_ps / pts /=
2 openHlife :
pointstoPLivetoken_based DfracOwn1 VLivetoken_regiond ∗ emp
Hname :
pointstoPNametoken_keyd DfracOwn1 VStreamtoken_handled Somepending, fifo
∗
pointstoPLivetoken_based DfracOwn1 VLivetoken_regiond ∗ pointstoPNametoken_keyd DfracOwn1 VStreamtoken_handled Somepending, fifo ∗ emp
deferred goal
∗
⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝
iDestruct Hlife as [Hlife _]
2 openHlife :
pointstoPLivetoken_based DfracOwn1 VLivetoken_regiond
Hname :
pointstoPNametoken_keyd DfracOwn1 VStreamtoken_handled Somepending, fifo
∗
pointstoPLivetoken_based DfracOwn1 VLivetoken_regiond ∗ pointstoPNametoken_keyd DfracOwn1 VStreamtoken_handled Somepending, fifo ∗ emp
deferred goal
∗
⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝
iFrame
deferred goal
∗
⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝
–iPureIntro
⊢
stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h
unfold stream_current
⊢
rewrite lookup_insert_eq
⊢
token_handled = token_handled ∧ stream_observationw token_handled Somepending, fifo
exact conjeq_refl Hobs
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hfresh Hobs
iIntros [Hh Hlife]
iMod gen_heap_alloc_ PNametoken_keyd VStreamtoken_handled Somepending, fifo with Hh as (Hh & Hname & _) ; exact Hfresh |
iModIntro
iSplitL Hh ; iExact Hh |
iSplitL Hlife Hname
The other registered stream keeps its observable state and private inventory. Distinct addresses rule out stdout-priority aliasing.
∀ p q w w′
p = libc_stdoutw ∧ q = libc_stderrw ∨ p = libc_stderrw ∧ q = libc_stdoutw
libc_stream_framep w w′
libc_file_atw′ q = libc_file_atw q ∧ libc_stream_atw′ q = libc_stream_atw q ∧ libc_stream_statew′ q = libc_stream_statew q
Proof 38 steps Qed
intros p q w w′ Hwhich Hdistinct Hout & Herr & _ & _ & _ & _ & _ & _ & Hother
assert Hne : same_filelibc_stderrw libc_stdoutw = false
destruct Hwhich as → → | → →
–rewrite same_file_refl in Hother
destruct Hother as Hfile & Hopen & Hstate
assert Hlookup : libc_file_atw' libc_stderrw = libc_file_atw libc_stderrw
assert Hprotocol : libc_stream_statew' libc_stderrw = libc_stream_statew libc_stderrw
split ; exact Hlookup |
split ; | exact Hprotocol
unfold libc_stream_at
rewrite Hlookup Hout Hprotocol
reflexivity
–rewrite Hne in Hother
destruct Hother as Hfile & Hopen & Hstate
assert Hlookup : libc_file_atw' libc_stdoutw = libc_file_atw libc_stdoutw
assert Hprotocol : libc_stream_statew' libc_stdoutw = libc_stream_statew libc_stdoutw
split ; exact Hlookup |
split ; | exact Hprotocol
unfold libc_stream_at
rewrite Hlookup Hout Hprotocol
reflexivity
Query contracts permit no allocation; in particular delegation cannot add a newly born release identity to either FILE.
∀ sources roots releases s m born s′ m′ born′
M.E.effectssources roots releases λ_ _ ⇒ False s m born s′ m′ born′
born′ = born
Explore proof 2 tactics
Initial goal
⊢
∀sources roots : listspan releases : listZ s : R.state m : mem born : listZ s′ : R.state m′ : mem born′ : listZ, M.E.effectssources roots releases λ_ _ : Z ⇒ False s m born s′ m′ born′ → born′ = born
intros sources roots releases s m born s′ m′ born′ He
sources, roots :
listspan
releases :
listZ
s :
R.state
m :
born :
listZ
s′ :
R.state
m′ :
born′ :
listZ
He :
M.E.effectssources roots releases λ_ _ : Z ⇒ False s m born s′ m′ born′
⊢
born′ = born
induction He ; reflexivity | exact IHHe | contradiction
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros sources roots releases s m born s′ m′ born′ He
induction He ; reflexivity | exact IHHe | contradiction
Both mirrors and both private-memory frames survive either query. No unchanged-memory premise rules out the native locking writes.
∀ rep requests wide out err b o d spec r args s m w trace ending s′ m′ w′ h
d = out ∨ d = err
spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide
M.E.invokespec r args WPtrtoken_handled s m w trace ending s′ m′ w′
agreesm h
R.readys m
stream_tokens_wirep out err b o m w h
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ stream_tokens_wirep out err b o m′ w′ h
Proof 71 steps Qed
intros rep requests wide out err b o d spec r args s m w trace ending s′ m′ w′ h Hd Hspec Hcall Ha Hdis Hr Houtwf & Herrwf & Hbase & Hkey & Hout & Herr & Houtcurrent & Herrcurrent & Hprivate
destruct Hprivated Hd as Hselected Hrelease
destruct T.query_framerep requests wide token_baseout token_baseerr token_handled b o spec r args s m w trace ending s' m' w' h Hspec Hcall Ha Hdis Hr Hselected as Ha′ & Hdis′ & Hr′ & Hselected′
split ; exact Ha' |
split ; exact Hdis' |
split ; exact Hr' |
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & Hp
destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as _ Hpers
assert Hborn : born = [ ]
{destruct Hp as He _
destruct Hspec as → | → ; eapply effects_no_alloc ; exact He
subst born
assert Hprefix : query_prefixlibc_stream_modelrep requests wide WPtrtoken_handled m w [ ] trace m' w'
{destruct Hspec as → | → ; exact proj2Hp
destruct Hprefix as p & info & Hxs & Hinfo & Hopen & Hframe & Hdelegate & _
injection Hxs as ←
cbn [ stream_open stream_at stream_state_at stream_rep libc_stream_model ] in Hinfo , Hopen
assert Hready′ := proj1Hopen
assert Hdistinct : ptr_addrlibc_stdoutw ≠ ptr_addrlibc_stderrw
{destruct proj1Hselected as _ & _ & _ & _ & _ & _ & _ & _ & Hdistinct & _
exact Hdistinct
assert Hother : ∀q, q = out ∨ q = err → q ≠ d → libc_file_atw' token_handleq = libc_file_atw token_handleq ∧ libc_stream_atw' token_handleq = libc_stream_atw token_handleq ∧ libc_stream_statew' token_handleq = libc_stream_statew token_handleq
{intros q Hq Hne
apply stream_other_frame with p := token_handled ; | exact Hdistinct | exact Hframe
destruct Hd as → | → ; destruct Hq as → | → ; try contradiction ; left | right ; split ; congruence
{intros q Hq
destruct Hd as → | → ; destruct Hq as → | → ; try left ; reflexivity ; right ; intros Heq ; apply Hbase ; congruence
assert Hviews : ∀q, q = out ∨ q = err → libc_stream_atw' token_handleq = libc_stream_atw token_handleq ∧ libc_stream_statew' token_handleq = libc_stream_statew token_handleq
{intros q Hq
destruct Hchoiceq Hq as [ ->| Hne ]
–split ; rewrite Hinfo ; exact proj1proj2Hopen |
pose proof proj1proj2proj2Hopen as Hprotocol
change stream_protocolinfo = libc_stream_statew' token_handled in Hprotocol
rewrite <- Hprotocol
unfold libc_stream_at in Hinfo
destruct libc_file_atw token_handled ; injection Hinfo as ← ; reflexivity | discriminate
–exact proj2Hotherq Hq Hne
assert Hcurrent : ∀q, q = out ∨ q = err → stream_currentq w' h
{intros q Hq
assert Hc : stream_currentq w h by destruct Hq as → | → ; assumption
destruct Hviewsq Hq as Hlookup Hstate
unfold stream_current in *
destruct v ; try contradiction
destruct Hc as → Hobs
split ; reflexivity |
unfold stream_observation in *
destruct pending as physical fifo | ; rewrite Hlookup ; exact Hobs | rewrite Hstate ; exact Hobs
split ; exact Houtwf |
split ; exact Herrwf |
split ; exact Hbase |
split ; exact Hkey |
split ; rewrite proj1Hframe ; exact Hout |
split ; rewrite proj1proj2Hframe ; exact Herr |
split ; apply Hcurrent ; left ; reflexivity |
split ; apply Hcurrent ; right ; reflexivity |
intros q Hq
destruct Hchoiceq Hq as [ ->| Hne ]
–split ; exact Hselected' |
intros base l v Hin Hl Hmem
–destruct Hotherq Hq Hne as Hfile _
destruct Hprivateq Hq as Hwi Hrel
assert Hroots : libc_stream_aux_rootsw' token_handleq = libc_stream_aux_rootsw token_handleq by unfold libc_stream_aux_roots ; rewrite Hfile ; reflexivity
assert Hrels : libc_stream_releasesw' token_handleq = libc_stream_releasesw token_handleq by unfold libc_stream_releases ; rewrite Hfile ; reflexivity
split ; | rewrite Hrels ; exact Hrel
eapply errno_wi_fixed ; exact Hwi | | exact Hpers | exact Hready' | | exact Hroots | exact Hrels
+apply stream_data_agrees
exact Ha
+exact proj1proj2proj2proj2Hframe
Only an ordinary return establishes completed closure. Sample all four endpoint errno bytes, update the selected name, and retain the opposite snapshot and both native lives. This is a pure heap frame; updating an owned name in Iris still requires its points-to resource.
∀ rep requests wide out err b o d r args s m w trace values s′ m′ w′ h xs
d = out ∨ d = err
M.E.invokefclose_contractlibc_stream_modelrep requests wide r args WPtrtoken_handled s m w trace CallReturnvalues s′ m′ w′
agreesm h
R.readys m
stream_tokens_wirep out err b o m w h
lengthxs = 4%nat
∀l v, l, v ∈ byte_psb o xs → h !! l = Somev
∃ys, lengthys = 4%nat ∧ byte_psb o ys.*1 = byte_psb o xs.*1 ∧ agreesm′ <[PNametoken_keyd ≔ VStreamtoken_handled None]>overwritebyte_psb o ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ stream_tokens_wirep out err b o m′ w′ <[PNametoken_keyd ≔ VStreamtoken_handled None]>overwritebyte_psb o ys h
Proof 122 steps Qed
intros rep requests wide out err b o d r args s m w trace values s′ m′ w′ h xs Hd Hcall Ha Hdis Hr Houtwf & Herrwf & Hbase & Hkey & Hout & Herr & Houtcurrent & Herrcurrent & Hprivate Hlen Howned
destruct Hprivated Hd as Hselected Hrelease
destruct T.close_framerep requests wide token_baseout token_baseerr token_handled b o r args s m w trace CallReturnvalues s' m' w' h xs ltac:rewrite Hout ; exact proj1Houtwf ltac:rewrite Herr ; exact proj1Herrwf Hcall Ha Hdis Hr Hselected Hlen Howned as ys & Hys & Hkeys & Ha′ & Hdis′ & Hr′ & Hselected′
set h1 := <[PNametoken_keyd ≔ VStreamtoken_handled None]>h0
assert Hkeys0 : memory_keys_fromh0 h
{intros l v Hl Hmem
unfold h0 in Hl
destruct lookup_overwrite_ _ _ _ Hl as Hin | _ Hold ; | eauto
apply list_elem_of_fmap in Hkey0 as l0 old & E & Hinold
simpl in E
subst l0
exists old
exact Hownedl old Hinold
assert Hkeys1 : memory_keys_fromh1 h0
{intros l v Hl Hmem
unfold h1 in Hl
assert Hdata1 : memory_keys_fromstream_data_heaptoken_baseout token_baseerr h1 stream_data_heaptoken_baseout token_baseerr h0
{intros l v Hl Hmem
apply stream_data_lookup in Hl as Hl & Hno & Hne
exists old
rewrite stream_data_lookup_ne ; assumption
assert Hdata0 : memory_keys_fromstream_data_heaptoken_baseout token_baseerr h1 stream_data_heaptoken_baseout token_baseerr h
{intros l v Hl Hmem
apply stream_data_lookup in Hl as Hl & Hno & Hne
destruct Hkeys0l old Hold Hmem as entry Hentry
exists entry
rewrite stream_data_lookup_ne ; assumption
exists ys
split ; exact Hys |
split ; exact Hkeys |
split
{intros l v Hl
unfold h1 in Hl
split ; exact Hdis' |
split ; exact Hr' |
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & Hp
destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as _ Hpers
destruct Hp as _ & p & info & final & Hxs & _ & _ & _ & Hready′ & Hframe & _
injection Hxs as ←
destruct T.EL.S.fclose_invocation_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born0 & p & info0 & final0 & n & Hxs & _ & Hsettle & Hstate & _ & Hclosed & _ | why & Hbad & _ ; | discriminate Hbad
injection Hxs as ←
change libc_stream_atw' token_handled = None in Hclosed
assert Hfifo : outstandinglibc_stream_statew' token_handled = [ ]
{change libc_stream_statew' token_handled = final0 in Hstate
rewrite Hstate
eapply stream_settlement_complete ; exact Hsettle
assert Hdistinct : ptr_addrlibc_stdoutw ≠ ptr_addrlibc_stderrw
{destruct proj1Hselected as _ & _ & _ & _ & _ & _ & _ & _ & Hdistinct & _
exact Hdistinct
{intros q Hq
destruct Hd as → | → ; destruct Hq as → | → ; try left ; reflexivity ; right ; intros Heq ; apply Hbase ; congruence
assert Hother : ∀q, q = out ∨ q = err → q ≠ d → libc_file_atw' token_handleq = libc_file_atw token_handleq ∧ libc_stream_atw' token_handleq = libc_stream_atw token_handleq ∧ libc_stream_statew' token_handleq = libc_stream_statew token_handleq
{intros q Hq Hne
apply stream_other_frame with p := token_handled ; | exact Hdistinct | exact Hframe
destruct Hd as → | → ; destruct Hq as → | → ; try contradiction ; left | right ; split ; congruence
assert Hcurrent : ∀q, q = out ∨ q = err → stream_currentq w' h1
{intros q Hq
destruct Hchoiceq Hq as [ ->| Hne ]
{destruct Hd as → | → ; destruct Hq as → | → ; congruence
assert Hc : stream_currentq w h by destruct Hq as → | → ; assumption
destruct Hotherq Hq Hne as _ & Hlookup & Hprotocol
unfold stream_current in *
unfold h1
rewrite lookup_insert_ne ; | congruence
unfold h0
rewrite overwrite_out
destruct v ; try contradiction
destruct Hc as → Hobs
split ; reflexivity |
unfold stream_observation in *
destruct pending as physical fifo | ; rewrite Hlookup ; exact Hobs | rewrite Hprotocol ; exact Hobs
split ; exact Houtwf |
split ; exact Herrwf |
split ; exact Hbase |
split ; exact Hkey |
split ; rewrite proj1Hframe ; exact Hout |
split ; rewrite proj1proj2Hframe ; exact Herr |
split ; apply Hcurrent ; left ; reflexivity |
split ; apply Hcurrent ; right ; reflexivity |
intros q Hq
destruct Hchoiceq Hq as [ ->| Hne ]
–split ; eapply errno_wi_heap ; exact Hselected' | exact Hdata1 |
unfold libc_stream_at in Hclosed
unfold libc_stream_releases
destruct libc_file_atw' token_handled ; discriminate Hclosed |
intros base l v Hin
contradiction
–destruct Hotherq Hq Hne as Hfile _
destruct Hprivateq Hq as Hwi Hrel
assert Hroots : libc_stream_aux_rootsw' token_handleq = libc_stream_aux_rootsw token_handleq by unfold libc_stream_aux_roots ; rewrite Hfile ; reflexivity
assert Hrels : libc_stream_releasesw' token_handleq = libc_stream_releasesw token_handleq by unfold libc_stream_releases ; rewrite Hfile ; reflexivity
split
+eapply errno_wi_heap ; | exact Hdata0
eapply errno_wi_fixed ; exact Hwi | | exact Hpers | exact Hready' | | exact Hroots | exact Hrels
∗apply stream_data_agrees
exact Ha
∗exact proj1proj2proj2proj2Hframe
Token ownership plus the current world interpretation admits the concrete libc call; openness is not another consumer assumption.
∀ rep requests wide out err b o d pending fifo m w h
d = out ∨ d = err
stream_tokens_wirep out err b o m w h
∀l v, l, v ∈ stream_psd pending fifo → h !! l = Somev
stream_call_prelibc_stream_modelrep requests wide WPtrtoken_handled m w
Explore proof 6 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop out err : stream_token b o : Z d : stream_token pending : Z fifo : listZ m : mem w : libc_world h : gmappiece pval, d = out ∨ d = err → stream_tokens_wirep out err b o m w h → ∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev → stream_call_prelibc_stream_modelrep requests wide WPtrtoken_handled m w
intros rep requests wide out err b o d pending fifo m w h Hd _ & _ & _ & _ & _ & _ & Hout & Herr & Hprivate Howned
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out, err :
b, o :
Z
d :
pending :
Z
fifo :
listZ
m :
w :
Hd :
d = out ∨ d = err
Hout :
stream_currentout w h
Herr :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
⊢
stream_call_prelibc_stream_modelrep requests wide WPtrtoken_handled m w
pose proof proj1proj1Hprivated Hd as Hready
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out, err :
b, o :
Z
d :
pending :
Z
fifo :
listZ
m :
w :
Hd :
d = out ∨ d = err
Hout :
stream_currentout w h
Herr :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
Hready :
libc_stream_readyrep m w
⊢
stream_call_prelibc_stream_modelrep requests wide WPtrtoken_handled m w
assert Hcurrent : stream_currentd w h by destruct Hd as → | → ; assumption
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out, err :
b, o :
Z
d :
pending :
Z
fifo :
listZ
m :
w :
Hd :
d = out ∨ d = err
Hout :
stream_currentout w h
Herr :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
Hready :
libc_stream_readyrep m w
Hcurrent :
stream_currentd w h
⊢
stream_call_prelibc_stream_modelrep requests wide WPtrtoken_handled m w
destruct stream_open_currentd w h pending fifo Hcurrent Howned as info & Hinfo & _
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out, err :
b, o :
Z
d :
pending :
Z
fifo :
listZ
m :
w :
Hd :
d = out ∨ d = err
Hout :
stream_currentout w h
Herr :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
Hready :
libc_stream_readyrep m w
Hcurrent :
stream_currentd w h
info :
Hinfo :
libc_stream_atw token_handled = Someinfo
⊢
stream_call_prelibc_stream_modelrep requests wide WPtrtoken_handled m w
unfold libc_stream_at in Hinfo
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out, err :
b, o :
Z
d :
pending :
Z
fifo :
listZ
m :
w :
Hd :
d = out ∨ d = err
Hout :
stream_currentout w h
Herr :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
Hready :
libc_stream_readyrep m w
Hcurrent :
stream_currentd w h
info :
Hinfo :
Somefile
⇒
Somestream_identifier ≔ if same_filetoken_handled libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew token_handled; stream_pending ≔ file_pendingfile
None
⇒
None
=
Someinfo
⊢
stream_call_prelibc_stream_modelrep requests wide WPtrtoken_handled m w
destruct libc_file_atw token_handled as file | eqn: Hfile ; eapply libc_stream_admitted ; eauto | discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide out err b o d pending fifo m w h Hd _ & _ & _ & _ & _ & _ & Hout & Herr & Hprivate Howned
pose proof proj1proj1Hprivated Hd as Hready
assert Hcurrent : stream_currentd w h by destruct Hd as → | → ; assumption
destruct stream_open_currentd w h pending fifo Hcurrent Howned as info & Hinfo & _
unfold libc_stream_at in Hinfo
destruct libc_file_atw token_handled as file | eqn: Hfile ; eapply libc_stream_admitted ; eauto | discriminate
The native representation's poll stability remains an explicit realization premise. Everything else follows from unchanged regions.
∀ rep p b o
∀s m s′ m′ w, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
LG.SafepointStablelibc_errno_wirep p b o
Explore proof 18 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop p : ptr b o : Z, ∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w → LG.SafepointStablelibc_errno_wirep p b o
intros rep p b o Hstable
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
⊢
LG.SafepointStablelibc_errno_wirep p b o
split
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
⊢
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world h : gmappiece pval, R.safepoints m s′ m′ → libc_errno_wirep p b o m w h → libc_errno_wirep p b o m′ w h
intros s m s′ m′ w h Hsp Hready & He & Hroots & Hrelease & Hoff
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
libc_errno_wirep p b o m′ w h
split ; eapply Hstable ; eauto |
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb ∧ roots_apartlibc_stream_aux_rootsw p h m′ ∧ ids_apartlibc_stream_releasesw p h ∧ pieces_offerrno_keysb o h m′ span_containserrno_spanb o
split ; exact He |
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
roots_apartlibc_stream_aux_rootsw p h m′ ∧ ids_apartlibc_stream_releasesw p h ∧ pieces_offerrno_keysb o h m′ span_containserrno_spanb o
split ; | split ; exact Hrelease |
2 openrep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
roots_apartlibc_stream_aux_rootsw p h m′
focused goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
–intros root a Hin Hspan l & v & reg & Hl & Hmem & E Hlive & Hrange
2 openrep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
E :
object_regionpiece_idl m_regionsm′ = Somereg
⊢
False
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
apply Hrootsroot a Hin Hspan
2 openrep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
E :
object_regionpiece_idl m_regionsm′ = Somereg
⊢
owned_liveh m a
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
exists l, v, reg
2 openrep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
E :
object_regionpiece_idl m_regionsm′ = Somereg
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
split ; exact Hl |
2 openrep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
E :
object_regionpiece_idl m_regionsm′ = Somereg
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
split ; exact Hmem |
2 openrep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
E :
object_regionpiece_idl m_regionsm′ = Somereg
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
split ; | exact Hrange
2 openrep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
E :
object_regionpiece_idl m_regionsm′ = Somereg
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
split ; | exact Hlive
2 openrep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
E :
object_regionpiece_idl m_regionsm′ = Somereg
⊢
object_regionpiece_idl m_regionsm = Somereg
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
rewrite R.collector_live_ _ _ _ Hsp in E
2 openrep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
E :
object_regionpiece_idl m_regionsm = Somereg
⊢
object_regionpiece_idl m_regionsm = Somereg
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
exact E
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
–intros l v Hl Hnot
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
l :
v :
Hl :
h !! l = Somev
Hnot :
l ∉ errno_keysb o
⊢
match l with
⇒
∀reg : region, live_atm′ b0 reg → 0 ≤ o0 → b0 + o0 < r_endreg → ¬span_containserrno_spanb o b0 + o0
_
⇒
True
destruct l as base | base off | base off | key ; try exact I
2 openrep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
base, off :
Z
v :
Hl :
h !! PBytebase off = Somev
Hnot :
PBytebase off ∉ errno_keysb o
⊢
∀reg : region, live_atm′ base reg → 0 ≤ off → base + off < r_endreg → ¬span_containserrno_spanb o base + off
focused goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrelease :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
base, off :
Z
v :
Hl :
h !! PAuxbase off = Somev
Hnot :
PAuxbase off ∉ errno_keysb o
⊢
∀reg : region, live_atm′ base reg → 0 ≤ off → base + off < r_endreg → ¬span_containserrno_spanb o base + off
all: intros reg E Hlive Ho Hend Hout ; rewrite R.collector_live_ _ _ _ Hsp in E ; exact Hoff_ v Hl Hnot reg conjE Hlive Ho Hend Hout
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep p b o Hstable
split
intros s m s′ m′ w h Hsp Hready & He & Hroots & Hrelease & Hoff
split ; eapply Hstable ; eauto |
split ; exact He |
split ; | split ; exact Hrelease |
–intros root a Hin Hspan l & v & reg & Hl & Hmem & E Hlive & Hrange
apply Hrootsroot a Hin Hspan
exists l, v, reg
split ; exact Hl |
split ; exact Hmem |
split ; | exact Hrange
split ; | exact Hlive
rewrite R.collector_live_ _ _ _ Hsp in E
exact E
–intros l v Hl Hnot
destruct l as base | base off | base off | key ; try exact I
all: intros reg E Hlive Ho Hend Hout ; rewrite R.collector_live_ _ _ _ Hsp in E ; exact Hoff_ v Hl Hnot reg conjE Hlive Ho Hend Hout
∀ rep out err b o
∀s m s′ m′ w, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
LG.SafepointStablestream_tokens_wirep out err b o
Explore proof 16 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop out err : stream_token b o : Z, ∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w → LG.SafepointStablestream_tokens_wirep out err b o
intros rep out err b o Hstable
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
⊢
LG.SafepointStablestream_tokens_wirep out err b o
split
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
⊢
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world h : gmappiece pval, R.safepoints m s′ m′ → stream_tokens_wirep out err b o m w h → stream_tokens_wirep out err b o m′ w h
intros s m s′ m′ w h Hsp Houtwf & Herrwf & Hbase & Hkey & Hout & Herr & Houtcurrent & Herrcurrent & Hprivate
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Houtwf :
token_wfout
Herrwf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hout :
libc_stdoutw = token_handleout
Herr :
libc_stderrw = token_handleerr
Houtcurrent :
stream_currentout w h
Herrcurrent :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
⊢
stream_tokens_wirep out err b o m′ w h
split ; exact Houtwf |
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Houtwf :
token_wfout
Herrwf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hout :
libc_stdoutw = token_handleout
Herr :
libc_stderrw = token_handleerr
Houtcurrent :
stream_currentout w h
Herrcurrent :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
⊢
token_wferr ∧ token_baseout ≠ token_baseerr ∧ token_keyout ≠ token_keyerr ∧ libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
split ; exact Herrwf |
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Houtwf :
token_wfout
Herrwf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hout :
libc_stdoutw = token_handleout
Herr :
libc_stderrw = token_handleerr
Houtcurrent :
stream_currentout w h
Herrcurrent :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
⊢
token_baseout ≠ token_baseerr ∧ token_keyout ≠ token_keyerr ∧ libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
split ; exact Hbase |
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Houtwf :
token_wfout
Herrwf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hout :
libc_stdoutw = token_handleout
Herr :
libc_stderrw = token_handleerr
Houtcurrent :
stream_currentout w h
Herrcurrent :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
⊢
token_keyout ≠ token_keyerr ∧ libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
split ; exact Hkey |
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Houtwf :
token_wfout
Herrwf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hout :
libc_stdoutw = token_handleout
Herr :
libc_stderrw = token_handleerr
Houtcurrent :
stream_currentout w h
Herrcurrent :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
⊢
libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
split ; exact Hout |
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Houtwf :
token_wfout
Herrwf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hout :
libc_stdoutw = token_handleout
Herr :
libc_stderrw = token_handleerr
Houtcurrent :
stream_currentout w h
Herrcurrent :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
⊢
libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
split ; exact Herr |
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Houtwf :
token_wfout
Herrwf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hout :
libc_stdoutw = token_handleout
Herr :
libc_stderrw = token_handleerr
Houtcurrent :
stream_currentout w h
Herrcurrent :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
⊢
stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
split ; exact Houtcurrent |
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Houtwf :
token_wfout
Herrwf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hout :
libc_stdoutw = token_handleout
Herr :
libc_stderrw = token_handleerr
Houtcurrent :
stream_currentout w h
Herrcurrent :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
⊢
stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
split ; exact Herrcurrent |
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Houtwf :
token_wfout
Herrwf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hout :
libc_stdoutw = token_handleout
Herr :
libc_stderrw = token_handleerr
Houtcurrent :
stream_currentout w h
Herrcurrent :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
⊢
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
intros d Hd
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Houtwf :
token_wfout
Herrwf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hout :
libc_stdoutw = token_handleout
Herr :
libc_stderrw = token_handleerr
Houtcurrent :
stream_currentout w h
Herrcurrent :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
d :
Hd :
d = out ∨ d = err
⊢
libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
destruct Hprivated Hd as Hwi Hrelease
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Houtwf :
token_wfout
Herrwf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hout :
libc_stdoutw = token_handleout
Herr :
libc_stderrw = token_handleerr
Houtcurrent :
stream_currentout w h
Herrcurrent :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
d :
Hd :
d = out ∨ d = err
Hwi :
libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h
Hrelease :
⊢
libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
split ; | exact Hrelease
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Houtwf :
token_wfout
Herrwf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hout :
libc_stdoutw = token_handleout
Herr :
libc_stderrw = token_handleerr
Houtcurrent :
stream_currentout w h
Herrcurrent :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
d :
Hd :
d = out ∨ d = err
Hwi :
libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h
Hrelease :
⊢
libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h
pose proof errno_wi_safepointrep token_handled b o Hstable as Hpoll
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Houtwf :
token_wfout
Herrwf :
token_wferr
Hbase :
token_baseout ≠ token_baseerr
Hout :
libc_stdoutw = token_handleout
Herr :
libc_stderrw = token_handleerr
Houtcurrent :
stream_currentout w h
Herrcurrent :
stream_currenterr w h
Hprivate :
∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h
d :
Hd :
d = out ∨ d = err
Hwi :
libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h
Hrelease :
Hpoll :
⊢
libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h
exact @LG.wi_safepoint_ _ Hpoll s m s′ m′ w _ Hsp Hwi
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep out err b o Hstable
split
intros s m s′ m′ w h Hsp Houtwf & Herrwf & Hbase & Hkey & Hout & Herr & Houtcurrent & Herrcurrent & Hprivate
split ; exact Houtwf |
split ; exact Herrwf |
split ; exact Hbase |
split ; exact Hkey |
split ; exact Hout |
split ; exact Herr |
split ; exact Houtcurrent |
split ; exact Herrcurrent |
intros d Hd
destruct Hprivated Hd as Hwi Hrelease
split ; | exact Hrelease
pose proof errno_wi_safepointrep token_handled b o Hstable as Hpoll
exact @LG.wi_safepoint_ _ Hpoll s m s′ m′ w _ Hsp Hwi
Discriminating world observations: physical pending is seven, the logical FIFO has two bytes, and a completed close consumes both.
mkStreamTokenfile_handleF.out_file 1024 mkRegion1024 1056 GlobalData Live −2
mkStreamTokenfile_handleF.err_file 2048 mkRegion2048 2056 Stack Live −3
<[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap
518Example open_snapshots_current: stream_currentout F.worldtrue open_heap ∧ stream_currenterr F.worldtrue open_heap
Explore proof 10 tactics
Initial goal
⊢
stream_currentout F.worldtrue open_heap ∧ stream_currenterr F.worldtrue open_heap
unfold stream_current , open_heap
⊢
match <[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! PNametoken_keyout with
None
⇒
True
_
⇒
False
∧
match <[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! PNametoken_keyerr with
None
⇒
True
_
⇒
False
cbn [ out err token_key ]
⊢
match <[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! PName−2 with
None
⇒
True
_
⇒
False
∧
match <[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! PName−3 with
None
⇒
True
_
⇒
False
rewrite lookup_insert_eq
⊢
token_handleout = token_handleout ∧ stream_observationF.worldtrue token_handleout Some7, 65; 66
∧
match <[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! PName−3 with
None
⇒
True
_
⇒
False
rewrite lookup_insert_ne ; | discriminate
⊢
token_handleout = token_handleout ∧ stream_observationF.worldtrue token_handleout Some7, 65; 66
∧
None
⇒
True
_
⇒
False
rewrite lookup_insert_eq
⊢
token_handleout = token_handleout ∧ stream_observationF.worldtrue token_handleout Some7, 65; 66 ∧ token_handleerr = token_handleerr ∧ stream_observationF.worldtrue token_handleerr Some3, [ ]
split ; split ; reflexivity |
2 open⊢
stream_observationF.worldtrue token_handleout Some7, 65; 66
focused goal
⊢
stream_observationF.worldtrue token_handleerr Some3, [ ]
–exists mkStreamInfo1 mkStreamByteOriented 65; 66 true 7
2 open⊢
libc_stream_atF.worldtrue token_handleout = Somestream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 ∧ stream_pendingstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 = 7 ∧ outstandingstream_protocolstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 = 65; 66
deferred goal
⊢
stream_observationF.worldtrue token_handleerr Some3, [ ]
repeat split ; reflexivity
deferred goal
⊢
stream_observationF.worldtrue token_handleerr Some3, [ ]
–exists mkStreamInfo2 stdout_initial 3
⊢
libc_stream_atF.worldtrue token_handleerr = Somestream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ∧ stream_pendingstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 = 3 ∧ outstandingstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 = [ ]
repeat split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold stream_current , open_heap
rewrite lookup_insert_eq
rewrite lookup_insert_ne ; | discriminate
rewrite lookup_insert_eq
split ; split ; reflexivity |
–exists mkStreamInfo1 mkStreamByteOriented 65; 66 true 7
repeat split ; reflexivity
–exists mkStreamInfo2 stdout_initial 3
repeat split ; reflexivity
528Example stale_physical_count_rejected: ¬stream_currentout F.worldtrue <[PName−2 ≔ VStreamtoken_handleout Some2, 65; 66]>open_heap
Explore proof 7 tactics
Initial goal
⊢
¬stream_currentout F.worldtrue <[PName−2 ≔ VStreamtoken_handleout Some2, 65; 66]>open_heap
unfold stream_current
⊢
¬match <[PName−2 ≔ VStreamtoken_handleout Some2, 65; 66]>open_heap !! PNametoken_keyout with SomeVStreamp snapshot ⇒ p = token_handleout ∧ stream_observationF.worldtrue p snapshot None ⇒ True _ ⇒ False end
cbn [ out token_key ]
⊢
¬match <[PName−2 ≔ VStreamtoken_handleout Some2, 65; 66]>open_heap !! PName−2 with SomeVStreamp snapshot ⇒ p = token_handleout ∧ stream_observationF.worldtrue p snapshot None ⇒ True _ ⇒ False end
rewrite lookup_insert_eq
⊢
¬token_handleout = token_handleout ∧ stream_observationF.worldtrue token_handleout Some2, 65; 66
intros _ & info & Hinfo & Hpending & _
⊢
False
change SomemkStreamInfo1 mkStreamByteOriented 65; 66 true 7 = Someinfo in Hinfo
info :
Hinfo :
Somestream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 = Someinfo
Hpending :
stream_pendinginfo = 2
⊢
False
injection Hinfo as ←
Hpending :
stream_pendingstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 = 2
⊢
False
discriminate Hpending
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold stream_current
rewrite lookup_insert_eq
intros _ & info & Hinfo & Hpending & _
change SomemkStreamInfo1 mkStreamByteOriented 65; 66 true 7 = Someinfo in Hinfo
injection Hinfo as ←
discriminate Hpending
538Example stale_fifo_rejected: ¬stream_currentout F.worldtrue <[PName−2 ≔ VStreamtoken_handleout Some7, 66; 65]>open_heap
Explore proof 7 tactics
Initial goal
⊢
¬stream_currentout F.worldtrue <[PName−2 ≔ VStreamtoken_handleout Some7, 66; 65]>open_heap
unfold stream_current
⊢
¬match <[PName−2 ≔ VStreamtoken_handleout Some7, 66; 65]>open_heap !! PNametoken_keyout with SomeVStreamp snapshot ⇒ p = token_handleout ∧ stream_observationF.worldtrue p snapshot None ⇒ True _ ⇒ False end
cbn [ out token_key ]
⊢
¬match <[PName−2 ≔ VStreamtoken_handleout Some7, 66; 65]>open_heap !! PName−2 with SomeVStreamp snapshot ⇒ p = token_handleout ∧ stream_observationF.worldtrue p snapshot None ⇒ True _ ⇒ False end
rewrite lookup_insert_eq
⊢
¬token_handleout = token_handleout ∧ stream_observationF.worldtrue token_handleout Some7, 66; 65
intros _ & info & Hinfo & _ & Hfifo
info :
Hinfo :
libc_stream_atF.worldtrue token_handleout = Someinfo
Hfifo :
outstandingstream_protocolinfo = 66; 65
⊢
False
change SomemkStreamInfo1 mkStreamByteOriented 65; 66 true 7 = Someinfo in Hinfo
info :
Hinfo :
Somestream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 = Someinfo
Hfifo :
outstandingstream_protocolinfo = 66; 65
⊢
False
injection Hinfo as ←
Hfifo :
outstandingstream_protocolstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 = 66; 65
⊢
False
discriminate Hfifo
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold stream_current
rewrite lookup_insert_eq
intros _ & info & Hinfo & _ & Hfifo
change SomemkStreamInfo1 mkStreamByteOriented 65; 66 true 7 = Someinfo in Hinfo
injection Hinfo as ←
discriminate Hfifo
548Example completed_closed_snapshot: stream_currentout F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>open_heap
Explore proof 5 tactics
Initial goal
⊢
stream_currentout F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>open_heap
unfold stream_current
⊢
None
⇒
True
_
⇒
False
cbn [ out token_key ]
⊢
None
⇒
True
_
⇒
False
rewrite lookup_insert_eq
⊢
token_handleout = token_handleout ∧ stream_observationF.worldfalse token_handleout None
split ; reflexivity |
⊢
stream_observationF.worldfalse token_handleout None
split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
556Example closed_token_rejected_while_open: ¬stream_currentout F.worldtrue <[PName−2 ≔ VStreamtoken_handleout None]>open_heap
Explore proof 5 tactics
Initial goal
⊢
¬stream_currentout F.worldtrue <[PName−2 ≔ VStreamtoken_handleout None]>open_heap
unfold stream_current
⊢
¬match <[PName−2 ≔ VStreamtoken_handleout None]>open_heap !! PNametoken_keyout with SomeVStreamp snapshot ⇒ p = token_handleout ∧ stream_observationF.worldtrue p snapshot None ⇒ True _ ⇒ False end
cbn [ out token_key ]
⊢
¬match <[PName−2 ≔ VStreamtoken_handleout None]>open_heap !! PName−2 with SomeVStreamp snapshot ⇒ p = token_handleout ∧ stream_observationF.worldtrue p snapshot None ⇒ True _ ⇒ False end
rewrite lookup_insert_eq
⊢
¬token_handleout = token_handleout ∧ stream_observationF.worldtrue token_handleout None
intros _ & Hclosed & _
Hclosed :
libc_stream_atF.worldtrue token_handleout = None
⊢
False
discriminate Hclosed
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
564Example malformed_snapshot_rejected: ¬stream_currentout F.worldtrue <[PName−2 ≔ VNametoken_handleout 65]>open_heap
Explore proof 4 tactics
Initial goal
⊢
¬stream_currentout F.worldtrue <[PName−2 ≔ VNametoken_handleout 65]>open_heap
unfold stream_current
⊢
¬match <[PName−2 ≔ VNametoken_handleout 65]>open_heap !! PNametoken_keyout with SomeVStreamp snapshot ⇒ p = token_handleout ∧ stream_observationF.worldtrue p snapshot None ⇒ True _ ⇒ False end
cbn [ out token_key ]
⊢
¬match <[PName−2 ≔ VNametoken_handleout 65]>open_heap !! PName−2 with SomeVStreamp snapshot ⇒ p = token_handleout ∧ stream_observationF.worldtrue p snapshot None ⇒ True _ ⇒ False end
rewrite lookup_insert_eq
⊢
¬False
exact λH ⇒ H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The entire interpretation has an inhabitant with both open tokens, both native lives and owned errno, not merely each mirror alone.
Explore proof 9 tactics
Initial goal
⊢
∀l : piece v : pval, mem_piecel → stream_data_heap1024 2048 open_heap !! l = Somev → HelloErrnoChecks.heap !! l = Somev
intros l v Hmem Hl
⊢
HelloErrnoChecks.heap !! l = Somev
apply stream_data_lookup in Hl as Hl & Hout & Herr
unfold open_heap in Hl
l :
v :
Hmem :
Hl :
<[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! l = Somev
Hout :
l ≠ PLive1024
Herr :
l ≠ PLive2048
⊢
HelloErrnoChecks.heap !! l = Somev
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |
l :
v :
Hmem :
Hl :
<[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! l = Somev
Hout :
l ≠ PLive1024
Herr :
l ≠ PLive2048
⊢
HelloErrnoChecks.heap !! l = Somev
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |
⊢
HelloErrnoChecks.heap !! l = Somev
unfold StreamHandleChecks.heap in Hl
⊢
HelloErrnoChecks.heap !! l = Somev
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |
exact Hl
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros l v Hmem Hl
apply stream_data_lookup in Hl as Hl & Hout & Herr
unfold open_heap in Hl
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |
unfold StreamHandleChecks.heap in Hl
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |
exact Hl
stream_tokens_wiλ_ _ ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
Explore proof 25 tactics
Initial goal
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
assert Hkeys : ∀l v, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
2 open⊢
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
{intros l v Hl Hmem
2 open⊢
l ∈ errno_keys5120 0
deferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
apply private_lookupl v Hmem in Hl
2 open⊢
l ∈ errno_keys5120 0
deferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
unfold HelloErrnoChecks.heap in Hl
2 open⊢
l ∈ errno_keys5120 0
deferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
apply elem_of_list_to_map_2 in Hl
2 open⊢
l ∈ errno_keys5120 0
deferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
change l ∈ byte_ps5120 0 0; 0; 0; 0.*1
2 opendeferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
apply list_elem_of_fmap
2 opendeferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
exists l, v
2 open⊢
l = l, v.1 ∧ l, v ∈ byte_ps5120 0 0; 0; 0; 0
deferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
auto
deferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
split ; split ; reflexivity | simpl ; lia |
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
token_wferr ∧ token_baseout ≠ token_baseerr ∧ token_keyout ≠ token_keyerr ∧ libc_stdoutF.worldtrue = token_handleout ∧ libc_stderrF.worldtrue = token_handleerr ∧ stream_currentout F.worldtrue open_heap ∧ stream_currenterr F.worldtrue open_heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled open_heap
split ; split ; reflexivity | simpl ; lia |
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
token_baseout ≠ token_baseerr ∧ token_keyout ≠ token_keyerr ∧ libc_stdoutF.worldtrue = token_handleout ∧ libc_stderrF.worldtrue = token_handleerr ∧ stream_currentout F.worldtrue open_heap ∧ stream_currenterr F.worldtrue open_heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled open_heap
split ; discriminate |
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
token_keyout ≠ token_keyerr ∧ libc_stdoutF.worldtrue = token_handleout ∧ libc_stderrF.worldtrue = token_handleerr ∧ stream_currentout F.worldtrue open_heap ∧ stream_currenterr F.worldtrue open_heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled open_heap
split ; discriminate |
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
libc_stdoutF.worldtrue = token_handleout ∧ libc_stderrF.worldtrue = token_handleerr ∧ stream_currentout F.worldtrue open_heap ∧ stream_currenterr F.worldtrue open_heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled open_heap
split ; reflexivity |
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
libc_stderrF.worldtrue = token_handleerr ∧ stream_currentout F.worldtrue open_heap ∧ stream_currenterr F.worldtrue open_heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled open_heap
split ; reflexivity |
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_currentout F.worldtrue open_heap ∧ stream_currenterr F.worldtrue open_heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled open_heap
split ; exact proj1open_snapshots_current |
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_currenterr F.worldtrue open_heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled open_heap
split ; exact proj2open_snapshots_current |
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled open_heap
intros d → | →
2 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handleout 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handleout open_heap
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handleerr 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handleerr open_heap
all: split ; | intros base l v Hin ; change Inbase [ ] in Hin ; contradiction
2 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handleout 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handleerr 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap
all: split ; apply F.ready |
2 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
libc_errnoF.worldtrue.1 = ptr_addr ≔ 5120 + 0; ptr_cap ≔ Obj5120 ∧ roots_apartlibc_stream_aux_rootsF.worldtrue token_handleout stream_data_heaptoken_baseout token_baseerr open_heap conversion_mem ∧ ids_apartlibc_stream_releasesF.worldtrue token_handleout stream_data_heaptoken_baseout token_baseerr open_heap ∧ pieces_offerrno_keys5120 0 stream_data_heaptoken_baseout token_baseerr open_heap conversion_mem span_containserrno_span5120 0
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
libc_errnoF.worldtrue.1 = ptr_addr ≔ 5120 + 0; ptr_cap ≔ Obj5120 ∧ roots_apartlibc_stream_aux_rootsF.worldtrue token_handleerr stream_data_heaptoken_baseout token_baseerr open_heap conversion_mem ∧ ids_apartlibc_stream_releasesF.worldtrue token_handleerr stream_data_heaptoken_baseout token_baseerr open_heap ∧ pieces_offerrno_keys5120 0 stream_data_heaptoken_baseout token_baseerr open_heap conversion_mem span_containserrno_span5120 0
all: split ; reflexivity |
2 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
roots_apartlibc_stream_aux_rootsF.worldtrue token_handleout stream_data_heaptoken_baseout token_baseerr open_heap conversion_mem ∧ ids_apartlibc_stream_releasesF.worldtrue token_handleout stream_data_heaptoken_baseout token_baseerr open_heap ∧ pieces_offerrno_keys5120 0 stream_data_heaptoken_baseout token_baseerr open_heap conversion_mem span_containserrno_span5120 0
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
roots_apartlibc_stream_aux_rootsF.worldtrue token_handleerr stream_data_heaptoken_baseout token_baseerr open_heap conversion_mem ∧ ids_apartlibc_stream_releasesF.worldtrue token_handleerr stream_data_heaptoken_baseout token_baseerr open_heap ∧ pieces_offerrno_keys5120 0 stream_data_heaptoken_baseout token_baseerr open_heap conversion_mem span_containserrno_span5120 0
all: split ; intros root a Hin ; change Inroot [ ] in Hin ; contradiction |
2 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
all: split ; intros base l v Hin ; change Inbase [ ] in Hin ; contradiction |
2 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
all: intros l v Hl Hnot ; destruct l as base | base off | base off | key ; try exact I
4 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
base, off :
Z
v :
Hl :
stream_data_heaptoken_baseout token_baseerr open_heap !! PBytebase off = Somev
Hnot :
PBytebase off ∉ errno_keys5120 0
⊢
∀reg : region, live_atconversion_mem base reg → 0 ≤ off → base + off < r_endreg → ¬span_containserrno_span5120 0 base + off
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
base, off :
Z
v :
Hl :
stream_data_heaptoken_baseout token_baseerr open_heap !! PAuxbase off = Somev
Hnot :
PAuxbase off ∉ errno_keys5120 0
⊢
∀reg : region, live_atconversion_mem base reg → 0 ≤ off → base + off < r_endreg → ¬span_containserrno_span5120 0 base + off
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
base, off :
Z
v :
Hl :
stream_data_heaptoken_baseout token_baseerr open_heap !! PBytebase off = Somev
Hnot :
PBytebase off ∉ errno_keys5120 0
⊢
∀reg : region, live_atconversion_mem base reg → 0 ≤ off → base + off < r_endreg → ¬span_containserrno_span5120 0 base + off
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
base, off :
Z
v :
Hl :
stream_data_heaptoken_baseout token_baseerr open_heap !! PAuxbase off = Somev
Hnot :
PAuxbase off ∉ errno_keys5120 0
⊢
∀reg : region, live_atconversion_mem base reg → 0 ≤ off → base + off < r_endreg → ¬span_containserrno_span5120 0 base + off
all: exfalso ; apply Hnot ; eapply Hkeys ; exact Hl | exact I
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
assert Hkeys : ∀l v, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
{intros l v Hl Hmem
apply private_lookupl v Hmem in Hl
unfold HelloErrnoChecks.heap in Hl
apply elem_of_list_to_map_2 in Hl
change l ∈ byte_ps5120 0 0; 0; 0; 0.*1
apply list_elem_of_fmap
exists l, v
auto
split ; split ; reflexivity | simpl ; lia |
split ; split ; reflexivity | simpl ; lia |
split ; discriminate |
split ; discriminate |
split ; reflexivity |
split ; reflexivity |
split ; exact proj1open_snapshots_current |
split ; exact proj2open_snapshots_current |
intros d → | →
all: split ; | intros base l v Hin ; change Inbase [ ] in Hin ; contradiction
all: split ; apply F.ready |
all: split ; reflexivity |
all: split ; intros root a Hin ; change Inroot [ ] in Hin ; contradiction |
all: split ; intros base l v Hin ; change Inbase [ ] in Hin ; 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
606Example full_open_admitted: stream_call_preF.model WPtrtoken_handleout conversion_mem F.worldtrue
Explore proof 15 tactics
Initial goal
⊢
stream_call_preF.model WPtrtoken_handleout conversion_mem F.worldtrue
eapply A.open_admitted with out := out err := err b := 5120 o := 0 pending := 7 fifo := 65; 66 h := open_heap ; left ; reflexivity | exact full_wi |
intros l v Hin
unfold stream_ps in Hin
l :
v :
Hin :
l, v ∈ PLivetoken_baseout, VLivetoken_regionout; PNametoken_keyout, VStreamtoken_handleout Some7, 65; 66
⊢
open_heap !! l = Somev
apply elem_of_cons in Hin as He | Hin
2 open⊢
open_heap !! l = Somev
–injection He as He Hv
2 opensubst l v
2 openunfold open_heap , StreamHandleChecks.heap
2 open⊢
<[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]><[PLive1024 ≔ VLiver_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live]><[PLive2048 ≔ VLiver_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live]>StreamHandleChecks.E.heap !! PLive1024 = SomeVLiver_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live
rewrite lookup_insert_ne ; | discriminate
2 open⊢
<[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]><[PLive1024 ≔ VLiver_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live]><[PLive2048 ≔ VLiver_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live]>StreamHandleChecks.E.heap !! PLive1024 = SomeVLiver_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live
rewrite lookup_insert_ne ; | discriminate
2 openapply lookup_insert_eq
–apply elem_of_cons in Hin as He | Hin ; | apply not_elem_of_nil in Hin ; contradiction
injection He as He Hv
subst l v
unfold open_heap
⊢
<[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! PName−2 = SomeVStreamptr_addr ≔ 1024; ptr_cap ≔ Obj1024 Some7, 65; 66
apply lookup_insert_eq
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
eapply A.open_admitted with out := out err := err b := 5120 o := 0 pending := 7 fifo := 65; 66 h := open_heap ; left ; reflexivity | exact full_wi |
intros l v Hin
unfold stream_ps in Hin
apply elem_of_cons in Hin as He | Hin
–injection He as He Hv
subst l v
unfold open_heap , StreamHandleChecks.heap
rewrite lookup_insert_ne ; | discriminate
rewrite lookup_insert_ne ; | discriminate
apply lookup_insert_eq
–apply elem_of_cons in Hin as He | Hin ; | apply not_elem_of_nil in Hin ; contradiction
injection He as He Hv
subst l v
unfold open_heap
apply lookup_insert_eq
Explore proof 5 tactics
Initial goal
intros l v Hl
unfold open_heap in Hl
l :
v :
Hl :
<[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! l = Somev
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l v ; exact I |
apply lookup_insert_Some in Hl as He Hv | _ 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 l v Hl
unfold open_heap in Hl
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l v ; exact I |
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l v ; exact I |
exact StreamHandleChecks.heap_agreesl v Hl
An actual stderr query frames the paired interpretation even though stdout's physical count and outstanding FIFO differ from stderr's.
630Example stderr_query_preserves_pair: A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ _ ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
Explore proof 10 tactics
Initial goal
⊢
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
assert Hcall : A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue
2 open⊢
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue
focused goal
Hcall :
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue
⊢
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
{apply StreamHandleChecks.C.fpending_unchanged with file := F.err_file
4 openfocused goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue
focused goal
⊢
libc_file_atF.worldtrue token_handleerr = SomeF.err_file
deferred goal
Hcall :
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue
⊢
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
–split ; left ; reflexivity |
4 opendeferred goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue
deferred goal
⊢
libc_file_atF.worldtrue token_handleerr = SomeF.err_file
deferred goal
Hcall :
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue
⊢
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
exists Const0
4 opendeferred goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue
deferred goal
⊢
libc_file_atF.worldtrue token_handleerr = SomeF.err_file
deferred goal
Hcall :
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue
⊢
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
reflexivity
3 opendeferred goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue
deferred goal
⊢
libc_file_atF.worldtrue token_handleerr = SomeF.err_file
deferred goal
Hcall :
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue
⊢
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
–apply F.ready
2 opendeferred goal
⊢
libc_file_atF.worldtrue token_handleerr = SomeF.err_file
deferred goal
Hcall :
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue
⊢
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
–reflexivity
deferred goal
Hcall :
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue
⊢
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
split ; exact Hcall |
Hcall :
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
destruct A.query_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False out err 5120 0 err _ _ _ _ _ _ _ _ _ _ _ open_heap or_introreq_refl or_introreq_refl Hcall open_heap_agrees HelloErrnoChecks.disjoint HelloErrnoChecks.ready full_wi as _ & _ & _ & Hw
Hcall :
A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue
Hw :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
exact Hw
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
assert Hcall : A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue
split ; exact Hcall |
destruct A.query_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False out err 5120 0 err _ _ _ _ _ _ _ _ _ _ _ open_heap or_introreq_refl or_introreq_refl Hcall open_heap_agrees HelloErrnoChecks.disjoint HelloErrnoChecks.ready full_wi as _ & _ & _ & Hw
exact Hw
The other query contract and stdout selection use the same frame.
652Example stdout_error_preserves_pair: A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ _ ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
Explore proof 10 tactics
Initial goal
⊢
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
assert Hcall : A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue
2 open⊢
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue
focused goal
Hcall :
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue
⊢
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
{apply StreamHandleChecks.C.ferror_unchanged with file := F.out_file
4 openfocused goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue
focused goal
⊢
libc_file_atF.worldtrue token_handleout = SomeF.out_file
deferred goal
Hcall :
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue
⊢
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
–split ; left ; reflexivity |
4 opendeferred goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue
deferred goal
⊢
libc_file_atF.worldtrue token_handleout = SomeF.out_file
deferred goal
Hcall :
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue
⊢
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
exists Const0
4 opendeferred goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue
deferred goal
⊢
libc_file_atF.worldtrue token_handleout = SomeF.out_file
deferred goal
Hcall :
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue
⊢
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
reflexivity
3 opendeferred goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue
deferred goal
⊢
libc_file_atF.worldtrue token_handleout = SomeF.out_file
deferred goal
Hcall :
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue
⊢
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
–apply F.ready
2 opendeferred goal
⊢
libc_file_atF.worldtrue token_handleout = SomeF.out_file
deferred goal
Hcall :
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue
⊢
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
–reflexivity
deferred goal
Hcall :
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue
⊢
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
split ; exact Hcall |
Hcall :
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
destruct A.query_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False out err 5120 0 out _ _ _ _ _ _ _ _ _ _ _ open_heap or_introleq_refl or_introleq_refl Hcall open_heap_agrees HelloErrnoChecks.disjoint HelloErrnoChecks.ready full_wi as _ & _ & _ & Hw
Hcall :
A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue
Hw :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap
exact Hw
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
assert Hcall : A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue
split ; exact Hcall |
destruct A.query_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False out err 5120 0 out _ _ _ _ _ _ _ _ _ _ _ open_heap or_introleq_refl or_introleq_refl Hcall open_heap_agrees HelloErrnoChecks.disjoint HelloErrnoChecks.ready full_wi as _ & _ & _ & Hw
exact Hw
An actual authorized scalar write changes every errno byte, including the last one. It changes neither FILE storage nor locale strings.
store_bytesconversion_mem 5120 4 16909060
libc_file_readychanged_errno mkPtr5120 Obj5120 F.out_file ∧ libc_file_readychanged_errno mkPtr5120 Obj5120 F.err_file
Explore proof 9 tactics
Initial goal
⊢
libc_file_readychanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file ∧ libc_file_readychanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file
destruct F.files_ready as Hout Herr
Hout :
libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file
Herr :
libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file
⊢
libc_file_readychanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file ∧ libc_file_readychanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file
split ; clear Herr | clear Hout
2 openHout :
libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file
⊢
libc_file_readychanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file
focused goal
Herr :
libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file
⊢
libc_file_readychanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file
all: destruct Hout as Hnon & Hn & Hreg & Haccess & Hbytes & Hrest || destruct Herr as Hnon & Hn & Hreg & Haccess & Hbytes & Hrest
2 openHnon :
Hn :
0 ≤ 1 < 2 ^ 64
Hreg :
∃base : Z reg : region, ptr_capfile_handleF.out_file = Objbase ∨ ptr_capfile_handleF.out_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live
Haccess :
Hbytes :
∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.out_file + i < 256
Hrest :
0 ≤ file_pendingF.out_file < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsF.out_file ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsF.out_file ∧ ForallLocale.locale_heapconversion_mem file_ownedF.out_file ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file
⊢
libc_file_readychanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file
focused goal
Hnon :
Hn :
0 ≤ 1 < 2 ^ 64
Hreg :
∃base : Z reg : region, ptr_capfile_handleF.err_file = Objbase ∨ ptr_capfile_handleF.err_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live
Haccess :
Hbytes :
∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.err_file + i < 256
Hrest :
0 ≤ file_pendingF.err_file < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsF.err_file ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsF.err_file ∧ ForallLocale.locale_heapconversion_mem file_ownedF.err_file ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file
⊢
libc_file_readychanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file
all: split ; exact Hnon |
2 openHnon :
Hn :
0 ≤ 1 < 2 ^ 64
Hreg :
∃base : Z reg : region, ptr_capfile_handleF.out_file = Objbase ∨ ptr_capfile_handleF.out_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live
Haccess :
Hbytes :
∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.out_file + i < 256
Hrest :
0 ≤ file_pendingF.out_file < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsF.out_file ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsF.out_file ∧ ForallLocale.locale_heapconversion_mem file_ownedF.out_file ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file
⊢
readable_byteschanged_errno file_handleF.out_file 1 ∧ 0 ≤ file_pendingF.out_file < 2 ^ 64 ∧ Forallwritable_spanchanged_errno file_rootsF.out_file ∧ Forallλsource : span ⇒ readable_byteschanged_errno span_ptrsource span_sizesource file_readsF.out_file ∧ ForallLocale.locale_heapchanged_errno file_ownedF.out_file ∧ file_errno_apartchanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file
focused goal
Hnon :
Hn :
0 ≤ 1 < 2 ^ 64
Hreg :
∃base : Z reg : region, ptr_capfile_handleF.err_file = Objbase ∨ ptr_capfile_handleF.err_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live
Haccess :
Hbytes :
∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.err_file + i < 256
Hrest :
0 ≤ file_pendingF.err_file < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsF.err_file ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsF.err_file ∧ ForallLocale.locale_heapconversion_mem file_ownedF.err_file ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file
⊢
readable_byteschanged_errno file_handleF.err_file 1 ∧ 0 ≤ file_pendingF.err_file < 2 ^ 64 ∧ Forallwritable_spanchanged_errno file_rootsF.err_file ∧ Forallλsource : span ⇒ readable_byteschanged_errno span_ptrsource span_sizesource file_readsF.err_file ∧ ForallLocale.locale_heapchanged_errno file_ownedF.err_file ∧ file_errno_apartchanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file
all: split ; | destruct Hrest as Hp & _ & _ & _ & Ha ; split ; exact Hp | ; split ; constructor | ; split ; constructor | ; split ; constructor | exact Ha
2 openHnon :
Hn :
0 ≤ 1 < 2 ^ 64
Hreg :
∃base : Z reg : region, ptr_capfile_handleF.out_file = Objbase ∨ ptr_capfile_handleF.out_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live
Haccess :
Hbytes :
∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.out_file + i < 256
Hrest :
0 ≤ file_pendingF.out_file < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsF.out_file ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsF.out_file ∧ ForallLocale.locale_heapconversion_mem file_ownedF.out_file ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file
focused goal
Hnon :
Hn :
0 ≤ 1 < 2 ^ 64
Hreg :
∃base : Z reg : region, ptr_capfile_handleF.err_file = Objbase ∨ ptr_capfile_handleF.err_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live
Haccess :
Hbytes :
∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.err_file + i < 256
Hrest :
0 ≤ file_pendingF.err_file < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsF.err_file ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsF.err_file ∧ ForallLocale.locale_heapconversion_mem file_ownedF.err_file ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file
all: split ; exact Hn |
2 openHnon :
Hn :
0 ≤ 1 < 2 ^ 64
Hreg :
∃base : Z reg : region, ptr_capfile_handleF.out_file = Objbase ∨ ptr_capfile_handleF.out_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live
Haccess :
Hbytes :
∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.out_file + i < 256
Hrest :
0 ≤ file_pendingF.out_file < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsF.out_file ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsF.out_file ∧ ForallLocale.locale_heapconversion_mem file_ownedF.out_file ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file
⊢
∃base : Z reg : region, ptr_capfile_handleF.out_file = Objbase ∨ ptr_capfile_handleF.out_file = Robase ∧ object_regionbase m_regionschanged_errno = Somereg ∧ r_lifereg = Live ∧ access_reschanged_errno ptr_addrfile_handleF.out_file ptr_capfile_handleF.out_file 1 Read 1 = Someok ∧ ∀i : Z, 0 ≤ i < 1 → 0 ≤ m_byteschanged_errno ptr_addrfile_handleF.out_file + i < 256
focused goal
Hnon :
Hn :
0 ≤ 1 < 2 ^ 64
Hreg :
∃base : Z reg : region, ptr_capfile_handleF.err_file = Objbase ∨ ptr_capfile_handleF.err_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live
Haccess :
Hbytes :
∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.err_file + i < 256
Hrest :
0 ≤ file_pendingF.err_file < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsF.err_file ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsF.err_file ∧ ForallLocale.locale_heapconversion_mem file_ownedF.err_file ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file
⊢
∃base : Z reg : region, ptr_capfile_handleF.err_file = Objbase ∨ ptr_capfile_handleF.err_file = Robase ∧ object_regionbase m_regionschanged_errno = Somereg ∧ r_lifereg = Live ∧ access_reschanged_errno ptr_addrfile_handleF.err_file ptr_capfile_handleF.err_file 1 Read 1 = Someok ∧ ∀i : Z, 0 ≤ i < 1 → 0 ≤ m_byteschanged_errno ptr_addrfile_handleF.err_file + i < 256
all: split ; exact Hreg |
2 openHnon :
Hn :
0 ≤ 1 < 2 ^ 64
Hreg :
∃base : Z reg : region, ptr_capfile_handleF.out_file = Objbase ∨ ptr_capfile_handleF.out_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live
Haccess :
Hbytes :
∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.out_file + i < 256
Hrest :
0 ≤ file_pendingF.out_file < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsF.out_file ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsF.out_file ∧ ForallLocale.locale_heapconversion_mem file_ownedF.out_file ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file
⊢
access_reschanged_errno ptr_addrfile_handleF.out_file ptr_capfile_handleF.out_file 1 Read 1 = Someok ∧ ∀i : Z, 0 ≤ i < 1 → 0 ≤ m_byteschanged_errno ptr_addrfile_handleF.out_file + i < 256
focused goal
Hnon :
Hn :
0 ≤ 1 < 2 ^ 64
Hreg :
∃base : Z reg : region, ptr_capfile_handleF.err_file = Objbase ∨ ptr_capfile_handleF.err_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live
Haccess :
Hbytes :
∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.err_file + i < 256
Hrest :
0 ≤ file_pendingF.err_file < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsF.err_file ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsF.err_file ∧ ForallLocale.locale_heapconversion_mem file_ownedF.err_file ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file
⊢
access_reschanged_errno ptr_addrfile_handleF.err_file ptr_capfile_handleF.err_file 1 Read 1 = Someok ∧ ∀i : Z, 0 ≤ i < 1 → 0 ≤ m_byteschanged_errno ptr_addrfile_handleF.err_file + i < 256
all: split ; exact Haccess |
2 openHnon :
Hn :
0 ≤ 1 < 2 ^ 64
Hreg :
∃base : Z reg : region, ptr_capfile_handleF.out_file = Objbase ∨ ptr_capfile_handleF.out_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live
Haccess :
Hbytes :
∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.out_file + i < 256
Hrest :
0 ≤ file_pendingF.out_file < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsF.out_file ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsF.out_file ∧ ForallLocale.locale_heapconversion_mem file_ownedF.out_file ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file
⊢
∀i : Z, 0 ≤ i < 1 → 0 ≤ m_byteschanged_errno ptr_addrfile_handleF.out_file + i < 256
focused goal
Hnon :
Hn :
0 ≤ 1 < 2 ^ 64
Hreg :
∃base : Z reg : region, ptr_capfile_handleF.err_file = Objbase ∨ ptr_capfile_handleF.err_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live
Haccess :
Hbytes :
∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.err_file + i < 256
Hrest :
0 ≤ file_pendingF.err_file < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsF.err_file ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsF.err_file ∧ ForallLocale.locale_heapconversion_mem file_ownedF.err_file ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file
⊢
∀i : Z, 0 ≤ i < 1 → 0 ≤ m_byteschanged_errno ptr_addrfile_handleF.err_file + i < 256
all: intros i Hi ; assert i = 0 as → by lia ; vm_compute ; split ; congruence
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
destruct F.files_ready as Hout Herr
split ; clear Herr | clear Hout
all: destruct Hout as Hnon & Hn & Hreg & Haccess & Hbytes & Hrest || destruct Herr as Hnon & Hn & Hreg & Haccess & Hbytes & Hrest
all: split ; exact Hnon |
all: split ; | destruct Hrest as Hp & _ & _ & _ & Ha ; split ; exact Hp | ; split ; constructor | ; split ; constructor | ; split ; constructor | exact Ha
all: split ; exact Hn |
all: split ; exact Hreg |
all: split ; exact Haccess |
all: intros i Hi ; assert i = 0 as → by lia ; vm_compute ; split ; congruence
∀ opened
libc_stream_readyλ_ _ ⇒ True changed_errno F.worldopened
Proof 26 steps Qed
intros opened
destruct F.readyopened as Hrep & Hlocale & He & Hout & Herr & Hu & Hstatus & Hphase & Hdistinct & Hroots & _
split ; exact Hrep |
split
–destruct Hlocale as _ & _ & _ & _ & _ & Haligned
split ; exact I |
split ; constructor |
split
+intros category _
vm_compute
repeat split ; congruence
+split ; constructor |
split ; constructor | exact Haligned
–split ; exact He |
split ; exact Hout |
split ; exact Herr |
split ; exact Hu |
split ; exact Hstatus |
split ; exact Hphase |
split ; exact Hdistinct |
split ; exact Hroots |
split ; intros _ ; exact proj1changed_files_ready |
split ; intros _ ; exact proj2changed_files_ready |
intros p file Hfile base Hin
unfold libc_file_at in Hfile
destruct same_filep libc_stdoutF.worldopened ; destruct opened | destruct same_filep libc_stderrF.worldopened ; try discriminate ; injection Hfile as ← ; contradiction
The contract allows success or EOF after settling the old FIFO. Both controls use the supplied HelloClose machine, not F.M.
∀ n
n = 0 ∨ n = stream_eof
A.M.E.invokefclose_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWIntn InterpRuntime.start changed_errno F.worldfalse
Proof 51 steps Qed
intros n Hn
eapply A.M.E.invoke_normal with born := [ ]
–apply full_open_admitted
–split
+eapply A.M.E.effects_local ; apply local_store_bytes | constructor
intros a Ha
left
exists errno_span5120 0
split ; left ; reflexivity |
split
∗exact proj1proj2proj1proj2proj2F.readytrue
+exists token_handleout, mkStreamInfo1 mkStreamByteOriented 65; 66 true 7, mkStreamByteOriented [ ] true
split ; reflexivity |
split ; reflexivity |
split ; apply F.close_settles |
split ; reflexivity |
split ; apply changed_ready |
split ; apply F.close_frame |
split ; split ; intros root | split ; intros x ; contradiction |
split ; reflexivity |
split ; left ; reflexivity |
intros a Hin Houtside
reflexivity
–exists token_handleout, mkStreamInfo1 mkStreamByteOriented 65; 66 true 7, mkStreamByteOriented [ ] true, n
split ; reflexivity |
split ; reflexivity |
split ; apply F.close_settles |
split ; reflexivity |
split ; exact Hn |
split ; reflexivity |
split ; intros base |
split ; apply changed_ready |
split ; apply F.close_frame |
auto
–intros why Hbad
discriminate
–intros values Hvalues
injection Hvalues as ←
split
+repeat constructor
–intros status Hbad
discriminate
749Example completed_close_preserves_pair: ∀n, n = 0 ∨ n = stream_eof → ∃ys, ys = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ _ ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
Explore proof 37 tactics
Initial goal
⊢
∀n : Z, n = 0 ∨ n = stream_eof → ∃ys : listZ, ys = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
intros n Hn
n :
Z
Hn :
n = 0 ∨ n = stream_eof
⊢
∃ys : listZ, ys = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
destruct A.close_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False out err 5120 0 out _ _ _ _ _ _ _ _ _ _ open_heap 0; 0; 0; 0 or_introleq_refl changed_closen Hn open_heap_agrees HelloErrnoChecks.disjoint HelloErrnoChecks.ready full_wi eq_refl as ys & Hlen & Hkeys & Hagree & _ & _ & Hwi
2 openn :
Z
Hn :
n = 0 ∨ n = stream_eof
focused goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
ys :
listZ
Hlen :
lengthys = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
⊢
∃ys0 : listZ, ys0 = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys0 open_heap
–intros l v Hin
2 open⊢
open_heap !! l = Somev
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
ys :
listZ
Hlen :
lengthys = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
⊢
∃ys0 : listZ, ys0 = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys0 open_heap
unfold open_heap , StreamHandleChecks.heap
2 opendeferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
ys :
listZ
Hlen :
lengthys = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
⊢
∃ys0 : listZ, ys0 = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys0 open_heap
pose proof MemLogic.byte_ps_elem_ _ _ _ _ Hin as i & x & Hi & El & Ev
2 openn :
Z
Hn :
n = 0 ∨ n = stream_eof
l :
v :
Hin :
l, v ∈ byte_ps5120 0 0; 0; 0; 0
i :
nat
x :
Z
Hi :
0; 0; 0; 0 !! i = Somex
El :
l = PByte5120 0 + i
Ev :
v = VBytex
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
ys :
listZ
Hlen :
lengthys = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
⊢
∃ys0 : listZ, ys0 = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys0 open_heap
subst l v
2 open⊢
<[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]><[PLive1024 ≔ VLiver_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live]><[PLive2048 ≔ VLiver_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live]>StreamHandleChecks.E.heap !! PByte5120 0 + i = SomeVBytex
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
ys :
listZ
Hlen :
lengthys = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
⊢
∃ys0 : listZ, ys0 = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys0 open_heap
rewrite lookup_insert_ne ; | discriminate
2 opendeferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
ys :
listZ
Hlen :
lengthys = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
⊢
∃ys0 : listZ, ys0 = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys0 open_heap
rewrite lookup_insert_ne ; | discriminate
2 opendeferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
ys :
listZ
Hlen :
lengthys = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
⊢
∃ys0 : listZ, ys0 = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys0 open_heap
rewrite lookup_insert_ne ; | discriminate
2 opendeferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
ys :
listZ
Hlen :
lengthys = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
⊢
∃ys0 : listZ, ys0 = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys0 open_heap
rewrite lookup_insert_ne ; | discriminate
2 opendeferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
ys :
listZ
Hlen :
lengthys = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
⊢
∃ys0 : listZ, ys0 = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys0 open_heap
unfold HelloErrnoChecks.heap
2 opendeferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
ys :
listZ
Hlen :
lengthys = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
⊢
∃ys0 : listZ, ys0 = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys0 open_heap
apply elem_of_list_to_map_1 ; | exact Hin
2 open⊢
base.NoDupbyte_ps5120 0 0; 0; 0; 0.*1
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
ys :
listZ
Hlen :
lengthys = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
⊢
∃ys0 : listZ, ys0 = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys0 open_heap
change base.NoDupPByte5120 0; PByte5120 1; PByte5120 2; PByte5120 3
2 opendeferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
ys :
listZ
Hlen :
lengthys = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
⊢
∃ys0 : listZ, ys0 = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys0 open_heap
repeat apply base.NoDup_cons_2 ; set_solver |
2 open⊢
base.NoDup[ ]
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
ys :
listZ
Hlen :
lengthys = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
⊢
∃ys0 : listZ, ys0 = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys0 open_heap
apply base.NoDup_nil_2
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
ys :
listZ
Hlen :
lengthys = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
⊢
∃ys0 : listZ, ys0 = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys0 open_heap
–exists ys
n :
Z
Hn :
n = 0 ∨ n = stream_eof
ys :
listZ
Hlen :
lengthys = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
⊢
ys = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
split ; | exact Hwi
n :
Z
Hn :
n = 0 ∨ n = stream_eof
ys :
listZ
Hlen :
lengthys = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap
⊢
ys = 4; 3; 2; 1
destruct ys as | a | b | c | d rest ; try discriminate Hlen
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
rest :
listZ
Hlen :
lengtha :: b :: c :: d :: rest = 4%nat
Hagree :
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a :: b :: c :: d :: rest open_heap
⊢
a :: b :: c :: d :: rest = 4; 3; 2; 1
assert rest = [ ] as → by destruct rest ; reflexivity | discriminate Hlen
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
⊢
a; b; c; d = 4; 3; 2; 1
assert Hbyte : ∀i x, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
2 openn :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
⊢
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
focused goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
⊢
a; b; c; d = 4; 3; 2; 1
{intros i x Hin
2 openn :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
i, x :
Z
⊢
x = m_byteschanged_errno 5120 + i
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
⊢
a; b; c; d = 4; 3; 2; 1
assert Hl : <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap !! PByte5120 i = SomeVBytex
3 openn :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
i, x :
Z
focused goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
i, x :
Z
⊢
x = m_byteschanged_errno 5120 + i
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
⊢
a; b; c; d = 4; 3; 2; 1
{rewrite lookup_insert_ne ; | discriminate
3 openn :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
i, x :
Z
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
i, x :
Z
⊢
x = m_byteschanged_errno 5120 + i
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
⊢
a; b; c; d = 4; 3; 2; 1
change PByte5120 i, VBytex ∈ PByte5120 0, VBytea; PByte5120 1, VByteb; PByte5120 2, VBytec; PByte5120 3, VByted in Hin
3 openn :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
i, x :
Z
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
i, x :
Z
⊢
x = m_byteschanged_errno 5120 + i
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
⊢
a; b; c; d = 4; 3; 2; 1
repeat apply elem_of_cons in Hin as E | Hin ; injection E as Ei Ex ; subst i x ; cbn [ byte_ps overwrite fst snd ] ; repeat rewrite lookup_insert_ne ; | discriminate ; apply lookup_insert_eq |
3 openn :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
i, x :
Z
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
i, x :
Z
⊢
x = m_byteschanged_errno 5120 + i
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
⊢
a; b; c; d = 4; 3; 2; 1
apply not_elem_of_nil in Hin
3 openn :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
i, x :
Z
Hin :
False
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
i, x :
Z
⊢
x = m_byteschanged_errno 5120 + i
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
⊢
a; b; c; d = 4; 3; 2; 1
contradiction
2 opendeferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
i, x :
Z
⊢
x = m_byteschanged_errno 5120 + i
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
⊢
a; b; c; d = 4; 3; 2; 1
destruct Hagree_ _ Hl as _ Hvalue
2 openn :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
i, x :
Z
Hl :
Hvalue :
in_livechanged_errno 5120 i m_byteschanged_errno 5120 + i = x
⊢
x = m_byteschanged_errno 5120 + i
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
⊢
a; b; c; d = 4; 3; 2; 1
destruct HvaluemkRegion5120 5128 Heap Live eq_refl eq_refl as _ & _ & Hv
2 openn :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
i, x :
Z
Hl :
Hvalue :
in_livechanged_errno 5120 i m_byteschanged_errno 5120 + i = x
Hv :
m_byteschanged_errno 5120 + i = x
⊢
x = m_byteschanged_errno 5120 + i
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
⊢
a; b; c; d = 4; 3; 2; 1
symmetry
2 openn :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
i, x :
Z
Hl :
Hvalue :
in_livechanged_errno 5120 i m_byteschanged_errno 5120 + i = x
Hv :
m_byteschanged_errno 5120 + i = x
⊢
m_byteschanged_errno 5120 + i = x
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
⊢
a; b; c; d = 4; 3; 2; 1
exact Hv
deferred goal
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
⊢
a; b; c; d = 4; 3; 2; 1
assert Ha : a = 4 by apply Hbyte0 a ; change PByte5120 0, VBytea ∈ PByte5120 0, VBytea; PByte5120 1, VByteb; PByte5120 2, VBytec; PByte5120 3, VByted ; apply list_elem_of_In ; simpl ; auto 10
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
Ha :
a = 4
⊢
a; b; c; d = 4; 3; 2; 1
assert Hb : b = 3 by apply Hbyte1 b ; change PByte5120 1, VByteb ∈ PByte5120 0, VBytea; PByte5120 1, VByteb; PByte5120 2, VBytec; PByte5120 3, VByted ; apply list_elem_of_In ; simpl ; auto 10
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
Ha :
a = 4
Hb :
b = 3
⊢
a; b; c; d = 4; 3; 2; 1
assert Hc : c = 2 by apply Hbyte2 c ; change PByte5120 2, VBytec ∈ PByte5120 0, VBytea; PByte5120 1, VByteb; PByte5120 2, VBytec; PByte5120 3, VByted ; apply list_elem_of_In ; simpl ; auto 10
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
Ha :
a = 4
Hb :
b = 3
Hc :
c = 2
⊢
a; b; c; d = 4; 3; 2; 1
assert Hd : d = 1 by apply Hbyte3 d ; change PByte5120 3, VByted ∈ PByte5120 0, VBytea; PByte5120 1, VByteb; PByte5120 2, VBytec; PByte5120 3, VByted ; apply list_elem_of_In ; simpl ; auto 10
n :
Z
Hn :
n = 0 ∨ n = stream_eof
a, b, c, d :
Z
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap
Hagree :
Hlen :
lengtha; b; c; d = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
Ha :
a = 4
Hb :
b = 3
Hc :
c = 2
Hd :
d = 1
⊢
a; b; c; d = 4; 3; 2; 1
subst
n :
Z
Hn :
n = 0 ∨ n = stream_eof
Hwi :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 4; 3; 2; 1 open_heap
Hagree :
Hlen :
length4; 3; 2; 1 = 4%nat
Hbyte :
∀i x : Z, PByte5120 i, VBytex ∈ byte_ps5120 0 4; 3; 2; 1 → x = m_byteschanged_errno 5120 + i
⊢
4; 3; 2; 1 = 4; 3; 2; 1
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros n Hn
destruct A.close_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False out err 5120 0 out _ _ _ _ _ _ _ _ _ _ open_heap 0; 0; 0; 0 or_introleq_refl changed_closen Hn open_heap_agrees HelloErrnoChecks.disjoint HelloErrnoChecks.ready full_wi eq_refl as ys & Hlen & Hkeys & Hagree & _ & _ & Hwi
–intros l v Hin
unfold open_heap , StreamHandleChecks.heap
pose proof MemLogic.byte_ps_elem_ _ _ _ _ Hin as i & x & Hi & El & Ev
subst l v
rewrite lookup_insert_ne ; | discriminate
rewrite lookup_insert_ne ; | discriminate
rewrite lookup_insert_ne ; | discriminate
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 Hwi
destruct ys as | a | b | c | d rest ; try discriminate Hlen
assert rest = [ ] as → by destruct rest ; reflexivity | discriminate Hlen
assert Hbyte : ∀i x, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
{intros i x Hin
assert Hl : <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap !! PByte5120 i = SomeVBytex
{rewrite lookup_insert_ne ; | discriminate
change PByte5120 i, VBytex ∈ PByte5120 0, VBytea; PByte5120 1, VByteb; PByte5120 2, VBytec; PByte5120 3, VByted in Hin
repeat apply elem_of_cons in Hin as E | Hin ; injection E as Ei Ex ; subst i x ; cbn [ byte_ps overwrite fst snd ] ; repeat rewrite lookup_insert_ne ; | discriminate ; apply lookup_insert_eq |
apply not_elem_of_nil in Hin
contradiction
destruct Hagree_ _ Hl as _ Hvalue
symmetry
exact Hv
assert Ha : a = 4 by apply Hbyte0 a ; change PByte5120 0, VBytea ∈ PByte5120 0, VBytea; PByte5120 1, VByteb; PByte5120 2, VBytec; PByte5120 3, VByted ; apply list_elem_of_In ; simpl ; auto 10
assert Hb : b = 3 by apply Hbyte1 b ; change PByte5120 1, VByteb ∈ PByte5120 0, VBytea; PByte5120 1, VByteb; PByte5120 2, VBytec; PByte5120 3, VByted ; apply list_elem_of_In ; simpl ; auto 10
assert Hc : c = 2 by apply Hbyte2 c ; change PByte5120 2, VBytec ∈ PByte5120 0, VBytea; PByte5120 1, VByteb; PByte5120 2, VBytec; PByte5120 3, VByted ; apply list_elem_of_In ; simpl ; auto 10
assert Hd : d = 1 by apply Hbyte3 d ; change PByte5120 3, VByted ∈ PByte5120 0, VBytea; PByte5120 1, VByteb; PByte5120 2, VBytec; PByte5120 3, VByted ; apply list_elem_of_In ; simpl ; auto 10
subst
reflexivity
Updating only the stream name would leave stale owned errno. The last byte alone distinguishes that incorrect replacement.
805Example stale_errno_close_heap_rejected: ¬agreeschanged_errno <[PName−2 ≔ VStreamtoken_handleout None]>open_heap
Explore proof 8 tactics
Initial goal
⊢
¬agreeschanged_errno <[PName−2 ≔ VStreamtoken_handleout None]>open_heap
intros Ha
Ha :
agreeschanged_errno <[PName−2 ≔ VStreamtoken_handleout None]>open_heap
⊢
False
assert Hl : <[PName−2 ≔ VStreamtoken_handleout None]>open_heap !! PByte5120 3 = SomeVByte0
2 openHa :
agreeschanged_errno <[PName−2 ≔ VStreamtoken_handleout None]>open_heap
focused goal
Ha :
agreeschanged_errno <[PName−2 ≔ VStreamtoken_handleout None]>open_heap
⊢
False
{unfold open_heap , StreamHandleChecks.heap , HelloErrnoChecks.heap
2 openHa :
agreeschanged_errno <[PName−2 ≔ VStreamtoken_handleout None]>open_heap
⊢
<[PName−2 ≔ VStreamtoken_handleout None]><[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]><[PLive1024 ≔ VLiver_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live]><[PLive2048 ≔ VLiver_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live]>list_to_mapbyte_ps5120 0 0; 0; 0; 0 !! PByte5120 3 = SomeVByte0
deferred goal
Ha :
agreeschanged_errno <[PName−2 ≔ VStreamtoken_handleout None]>open_heap
⊢
False
repeat rewrite lookup_insert_ne ; | discriminate
2 openHa :
agreeschanged_errno <[PName−2 ≔ VStreamtoken_handleout None]>open_heap
deferred goal
Ha :
agreeschanged_errno <[PName−2 ≔ VStreamtoken_handleout None]>open_heap
⊢
False
apply lookup_insert_eq
deferred goal
Ha :
agreeschanged_errno <[PName−2 ≔ VStreamtoken_handleout None]>open_heap
⊢
False
destruct Ha_ _ Hl as _ Hbyte
Ha :
agreeschanged_errno <[PName−2 ≔ VStreamtoken_handleout None]>open_heap
Hbyte :
in_livechanged_errno 5120 3 m_byteschanged_errno 5120 + 3 = 0
⊢
False
destruct HbytemkRegion5120 5128 Heap Live eq_refl eq_refl as _ & _ & Hvalue
Ha :
agreeschanged_errno <[PName−2 ≔ VStreamtoken_handleout None]>open_heap
Hbyte :
in_livechanged_errno 5120 3 m_byteschanged_errno 5120 + 3 = 0
Hvalue :
m_byteschanged_errno 5120 + 3 = 0
⊢
False
discriminate Hvalue
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Ha
{unfold open_heap , StreamHandleChecks.heap , HelloErrnoChecks.heap
repeat rewrite lookup_insert_ne ; | discriminate
apply lookup_insert_eq
destruct Ha_ _ Hl as _ Hbyte
discriminate Hvalue
Entry begins with actual errno ownership, but no recorded FILE lives or observations. The observations are selected from the current world.
Explore proof 5 tactics
Initial goal
⊢
∀l : piece v : pval, HelloErrnoChecks.heap !! l = Somev → ∃i : Z, l = PByte5120 i
intros l v Hl
⊢
∃i : Z, l = PByte5120 i
unfold HelloErrnoChecks.heap in Hl
apply elem_of_list_to_map_2 in Hl
destruct MemLogic.byte_ps_elem_ _ _ _ _ Hl as i & x & _ & → & _
eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros l v Hl
unfold HelloErrnoChecks.heap in Hl
apply elem_of_list_to_map_2 in Hl
destruct MemLogic.byte_ps_elem_ _ _ _ _ Hl as i & x & _ & → & _
eauto
stream_tokens_wiλ_ _ ⇒ True out err 5120 0 conversion_mem F.worldtrue HelloErrnoChecks.heap
Explore proof 29 tactics
Initial goal
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue HelloErrnoChecks.heap
assert Hkeys : ∀l v, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
2 open⊢
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue HelloErrnoChecks.heap
{intros l v Hl _
2 open⊢
l ∈ errno_keys5120 0
deferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue HelloErrnoChecks.heap
apply stream_data_lookup in Hl as Hl _
2 open⊢
l ∈ errno_keys5120 0
deferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue HelloErrnoChecks.heap
unfold HelloErrnoChecks.heap in Hl
2 open⊢
l ∈ errno_keys5120 0
deferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue HelloErrnoChecks.heap
apply elem_of_list_to_map_2 in Hl
2 open⊢
l ∈ errno_keys5120 0
deferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue HelloErrnoChecks.heap
change l ∈ byte_ps5120 0 0; 0; 0; 0.*1
2 opendeferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue HelloErrnoChecks.heap
apply list_elem_of_fmap
2 opendeferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue HelloErrnoChecks.heap
exists l, v
2 opendeferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue HelloErrnoChecks.heap
auto
deferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue HelloErrnoChecks.heap
split ; split ; reflexivity | simpl ; lia |
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
token_wferr ∧ token_baseout ≠ token_baseerr ∧ token_keyout ≠ token_keyerr ∧ libc_stdoutF.worldtrue = token_handleout ∧ libc_stderrF.worldtrue = token_handleerr ∧ stream_currentout F.worldtrue HelloErrnoChecks.heap ∧ stream_currenterr F.worldtrue HelloErrnoChecks.heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled HelloErrnoChecks.heap
split ; split ; reflexivity | simpl ; lia |
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
token_baseout ≠ token_baseerr ∧ token_keyout ≠ token_keyerr ∧ libc_stdoutF.worldtrue = token_handleout ∧ libc_stderrF.worldtrue = token_handleerr ∧ stream_currentout F.worldtrue HelloErrnoChecks.heap ∧ stream_currenterr F.worldtrue HelloErrnoChecks.heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled HelloErrnoChecks.heap
split ; discriminate |
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
token_keyout ≠ token_keyerr ∧ libc_stdoutF.worldtrue = token_handleout ∧ libc_stderrF.worldtrue = token_handleerr ∧ stream_currentout F.worldtrue HelloErrnoChecks.heap ∧ stream_currenterr F.worldtrue HelloErrnoChecks.heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled HelloErrnoChecks.heap
split ; discriminate |
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
libc_stdoutF.worldtrue = token_handleout ∧ libc_stderrF.worldtrue = token_handleerr ∧ stream_currentout F.worldtrue HelloErrnoChecks.heap ∧ stream_currenterr F.worldtrue HelloErrnoChecks.heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled HelloErrnoChecks.heap
split ; reflexivity |
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
libc_stderrF.worldtrue = token_handleerr ∧ stream_currentout F.worldtrue HelloErrnoChecks.heap ∧ stream_currenterr F.worldtrue HelloErrnoChecks.heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled HelloErrnoChecks.heap
split ; reflexivity |
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_currentout F.worldtrue HelloErrnoChecks.heap ∧ stream_currenterr F.worldtrue HelloErrnoChecks.heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled HelloErrnoChecks.heap
split
2 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_currentout F.worldtrue HelloErrnoChecks.heap
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_currenterr F.worldtrue HelloErrnoChecks.heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled HelloErrnoChecks.heap
{unfold stream_current
2 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
None
⇒
True
_
⇒
False
deferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_currenterr F.worldtrue HelloErrnoChecks.heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled HelloErrnoChecks.heap
destruct HelloErrnoChecks.heap !! PNametoken_keyout as v | eqn: E ; destruct entry_keys_ _ E as i Hbad ; discriminate Hbad | exact I
deferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_currenterr F.worldtrue HelloErrnoChecks.heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled HelloErrnoChecks.heap
split
2 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
stream_currenterr F.worldtrue HelloErrnoChecks.heap
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled HelloErrnoChecks.heap
{unfold stream_current
2 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
None
⇒
True
_
⇒
False
deferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled HelloErrnoChecks.heap
destruct HelloErrnoChecks.heap !! PNametoken_keyerr as v | eqn: E ; destruct entry_keys_ _ E as i Hbad ; discriminate Hbad | exact I
deferred goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled HelloErrnoChecks.heap
intros d → | →
2 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handleout 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handleout HelloErrnoChecks.heap
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handleerr 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handleerr HelloErrnoChecks.heap
all: split ; | intros base l v Hin ; change Inbase [ ] in Hin ; contradiction
2 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handleout 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handleerr 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap
all: split ; apply F.ready |
2 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
libc_errnoF.worldtrue.1 = ptr_addr ≔ 5120 + 0; ptr_cap ≔ Obj5120 ∧ roots_apartlibc_stream_aux_rootsF.worldtrue token_handleout stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap conversion_mem ∧ ids_apartlibc_stream_releasesF.worldtrue token_handleout stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ pieces_offerrno_keys5120 0 stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap conversion_mem span_containserrno_span5120 0
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
libc_errnoF.worldtrue.1 = ptr_addr ≔ 5120 + 0; ptr_cap ≔ Obj5120 ∧ roots_apartlibc_stream_aux_rootsF.worldtrue token_handleerr stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap conversion_mem ∧ ids_apartlibc_stream_releasesF.worldtrue token_handleerr stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ pieces_offerrno_keys5120 0 stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap conversion_mem span_containserrno_span5120 0
all: split ; reflexivity |
2 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
roots_apartlibc_stream_aux_rootsF.worldtrue token_handleout stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap conversion_mem ∧ ids_apartlibc_stream_releasesF.worldtrue token_handleout stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ pieces_offerrno_keys5120 0 stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap conversion_mem span_containserrno_span5120 0
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
⊢
roots_apartlibc_stream_aux_rootsF.worldtrue token_handleerr stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap conversion_mem ∧ ids_apartlibc_stream_releasesF.worldtrue token_handleerr stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap ∧ pieces_offerrno_keys5120 0 stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap conversion_mem span_containserrno_span5120 0
all: split ; intros root a Hin ; change Inroot [ ] in Hin ; contradiction |
2 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
all: split ; intros base l v Hin ; change Inbase [ ] in Hin ; contradiction |
2 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
all: intros l v Hl Hnot ; destruct l as base | base off | base off | key ; try exact I
4 openHkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
base, off :
Z
v :
Hl :
stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap !! PBytebase off = Somev
Hnot :
PBytebase off ∉ errno_keys5120 0
⊢
∀reg : region, live_atconversion_mem base reg → 0 ≤ off → base + off < r_endreg → ¬span_containserrno_span5120 0 base + off
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
base, off :
Z
v :
Hl :
stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap !! PAuxbase off = Somev
Hnot :
PAuxbase off ∉ errno_keys5120 0
⊢
∀reg : region, live_atconversion_mem base reg → 0 ≤ off → base + off < r_endreg → ¬span_containserrno_span5120 0 base + off
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
base, off :
Z
v :
Hl :
stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap !! PBytebase off = Somev
Hnot :
PBytebase off ∉ errno_keys5120 0
⊢
∀reg : region, live_atconversion_mem base reg → 0 ≤ off → base + off < r_endreg → ¬span_containserrno_span5120 0 base + off
focused goal
Hkeys :
∀l : piece v : pval, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
base, off :
Z
v :
Hl :
stream_data_heaptoken_baseout token_baseerr HelloErrnoChecks.heap !! PAuxbase off = Somev
Hnot :
PAuxbase off ∉ errno_keys5120 0
⊢
∀reg : region, live_atconversion_mem base reg → 0 ≤ off → base + off < r_endreg → ¬span_containserrno_span5120 0 base + off
all: exfalso ; apply Hnot ; eapply Hkeys ; exact Hl | exact I
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
assert Hkeys : ∀l v, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
{intros l v Hl _
apply stream_data_lookup in Hl as Hl _
unfold HelloErrnoChecks.heap in Hl
apply elem_of_list_to_map_2 in Hl
change l ∈ byte_ps5120 0 0; 0; 0; 0.*1
apply list_elem_of_fmap
exists l, v
auto
split ; split ; reflexivity | simpl ; lia |
split ; split ; reflexivity | simpl ; lia |
split ; discriminate |
split ; discriminate |
split ; reflexivity |
split ; reflexivity |
split
{unfold stream_current
destruct HelloErrnoChecks.heap !! PNametoken_keyout as v | eqn: E ; destruct entry_keys_ _ E as i Hbad ; discriminate Hbad | exact I
split
{unfold stream_current
destruct HelloErrnoChecks.heap !! PNametoken_keyerr as v | eqn: E ; destruct entry_keys_ _ E as i Hbad ; discriminate Hbad | exact I
intros d → | →
all: split ; | intros base l v Hin ; change Inbase [ ] in Hin ; contradiction
all: split ; apply F.ready |
all: split ; reflexivity |
all: split ; intros root a Hin ; change Inroot [ ] in Hin ; contradiction |
all: split ; intros base l v Hin ; change Inbase [ ] in Hin ; 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
Explore proof 6 tactics
Initial goal
intros l v Hin
destruct HelloErrnoChecks.heap !! l as old | eqn: E ; | reflexivity
destruct entry_keys_ _ E as i →
apply list_elem_of_In in Hin
cbn [ stream_ps app out err token_base token_key ] in Hin
⊢
Someold = None
destruct Hin as Hbad | Hbad | Hbad | Hbad | ; discriminate Hbad
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros l v Hin
destruct HelloErrnoChecks.heap !! l as old | eqn: E ; | reflexivity
destruct entry_keys_ _ E as i →
apply list_elem_of_In in Hin
cbn [ stream_ps app out err token_base token_key ] in Hin
destruct Hin as Hbad | Hbad | Hbad | Hbad | ; discriminate Hbad
Both real tokens are produced while independently owned errno is retained. This is not just a construction of a pure endpoint map.
868Example entry_produces_pair: gen_heap_interpHelloErrnoChecks.heap ∗ ptsbyte_ps5120 0 0; 0; 0; 0 ⇛ ∃h, gen_heap_interph ∗ ptsstream_psout 7 65; 66 ∗ ptsstream_pserr 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0 ∗ ⌜agreesconversion_mem h ∧ stream_tokens_wiλ_ _ ⇒ True out err 5120 0 conversion_mem F.worldtrue h⌝
Explore proof 13 tactics
Initial goal
⊢
gen_heap_interpHelloErrnoChecks.heap ∗ ptsbyte_ps5120 0 0; 0; 0; 0 ⇛ ∃h : gmappiece pval, gen_heap_interph ∗ ptsstream_psout 7 65; 66 ∗ ptsstream_pserr 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0 ∗ ⌜agreesconversion_mem h ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue h⌝
iIntros [Hh Herrno]
Hh :
gen_heap_interpHelloErrnoChecks.heap
∗
|⇛ ∃h : gmappiece pval, gen_heap_interph ∗ ptsstream_psout 7 65; 66 ∗ ptsstream_pserr 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0 ∗ ⌜agreesconversion_mem h ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue h⌝
iMod stream_entry_allocλ_ _ ⇒ True out err 5120 0 conversion_mem F.worldtrue HelloErrnoChecks.heap 7 65; 66 3 [ ] HelloErrnoChecks.heap_agrees entry_wi with Hh as (Hh & Ho & He & %Hnew)
6 openfocused goal
focused goal
⊢
stream_observationF.worldtrue token_handleout Some7, 65; 66
focused goal
⊢
stream_observationF.worldtrue token_handleerr Some3, [ ]
focused goal
focused goal
Σ :
gFunctors
Hnew :
agreesconversion_mem overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap
∗
|⇛ ∃h : gmappiece pval, gen_heap_interph ∗ ptsstream_psout 7 65; 66 ∗ ptsstream_pserr 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0 ∗ ⌜agreesconversion_mem h ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue h⌝
–split ; reflexivity
5 opendeferred goal
deferred goal
⊢
stream_observationF.worldtrue token_handleout Some7, 65; 66
deferred goal
⊢
stream_observationF.worldtrue token_handleerr Some3, [ ]
deferred goal
deferred goal
Σ :
gFunctors
Hnew :
agreesconversion_mem overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap
∗
|⇛ ∃h : gmappiece pval, gen_heap_interph ∗ ptsstream_psout 7 65; 66 ∗ ptsstream_pserr 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0 ∗ ⌜agreesconversion_mem h ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue h⌝
–split ; reflexivity
4 opendeferred goal
⊢
stream_observationF.worldtrue token_handleout Some7, 65; 66
deferred goal
⊢
stream_observationF.worldtrue token_handleerr Some3, [ ]
deferred goal
deferred goal
Σ :
gFunctors
Hnew :
agreesconversion_mem overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap
∗
|⇛ ∃h : gmappiece pval, gen_heap_interph ∗ ptsstream_psout 7 65; 66 ∗ ptsstream_pserr 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0 ∗ ⌜agreesconversion_mem h ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue h⌝
–exists mkStreamInfo1 mkStreamByteOriented 65; 66 true 7
4 open⊢
libc_stream_atF.worldtrue token_handleout = Somestream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 ∧ stream_pendingstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 = 7 ∧ outstandingstream_protocolstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 = 65; 66
deferred goal
⊢
stream_observationF.worldtrue token_handleerr Some3, [ ]
deferred goal
deferred goal
Σ :
gFunctors
Hnew :
agreesconversion_mem overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap
∗
|⇛ ∃h : gmappiece pval, gen_heap_interph ∗ ptsstream_psout 7 65; 66 ∗ ptsstream_pserr 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0 ∗ ⌜agreesconversion_mem h ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue h⌝
repeat split ; reflexivity
3 opendeferred goal
⊢
stream_observationF.worldtrue token_handleerr Some3, [ ]
deferred goal
deferred goal
Σ :
gFunctors
Hnew :
agreesconversion_mem overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap
∗
|⇛ ∃h : gmappiece pval, gen_heap_interph ∗ ptsstream_psout 7 65; 66 ∗ ptsstream_pserr 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0 ∗ ⌜agreesconversion_mem h ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue h⌝
–exists mkStreamInfo2 stdout_initial 3
3 open⊢
libc_stream_atF.worldtrue token_handleerr = Somestream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ∧ stream_pendingstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 = 3 ∧ outstandingstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 = [ ]
deferred goal
deferred goal
Σ :
gFunctors
Hnew :
agreesconversion_mem overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap
∗
|⇛ ∃h : gmappiece pval, gen_heap_interph ∗ ptsstream_psout 7 65; 66 ∗ ptsstream_pserr 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0 ∗ ⌜agreesconversion_mem h ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue h⌝
repeat split ; reflexivity
2 opendeferred goal
deferred goal
Σ :
gFunctors
Hnew :
agreesconversion_mem overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap
∗
|⇛ ∃h : gmappiece pval, gen_heap_interph ∗ ptsstream_psout 7 65; 66 ∗ ptsstream_pserr 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0 ∗ ⌜agreesconversion_mem h ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue h⌝
–exact entry_fresh
deferred goal
Σ :
gFunctors
Hnew :
agreesconversion_mem overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap
∗
|⇛ ∃h : gmappiece pval, gen_heap_interph ∗ ptsstream_psout 7 65; 66 ∗ ptsstream_pserr 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0 ∗ ⌜agreesconversion_mem h ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue h⌝
–iModIntro
Σ :
gFunctors
Hnew :
agreesconversion_mem overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap
∗
∃h : gmappiece pval, gen_heap_interph ∗ ptsstream_psout 7 65; 66 ∗ ptsstream_pserr 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0 ∗ ⌜agreesconversion_mem h ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue h⌝
iExists _
2 openΣ :
gFunctors
Hnew :
agreesconversion_mem overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap
∗
gen_heap_interp ∗ ptsstream_psout 7 65; 66 ∗ ptsstream_pserr 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0 ∗ ⌜agreesconversion_mem ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue ⌝
shelved goal
Σ :
gFunctors
Hnew :
agreesconversion_mem overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap
iFrame
Σ :
gFunctors
Hnew :
agreesconversion_mem overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap
∗
⌜agreesconversion_mem overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue overwritestream_psout 7 65; 66 ++ stream_pserr 3 [ ] HelloErrnoChecks.heap⌝
done
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
iIntros [Hh Herrno]
iMod stream_entry_allocλ_ _ ⇒ True out err 5120 0 conversion_mem F.worldtrue HelloErrnoChecks.heap 7 65; 66 3 [ ] HelloErrnoChecks.heap_agrees entry_wi with Hh as (Hh & Ho & He & %Hnew)
–split ; reflexivity
–split ; reflexivity
–exists mkStreamInfo1 mkStreamByteOriented 65; 66 true 7
repeat split ; reflexivity
–exists mkStreamInfo2 stdout_initial 3
repeat split ; reflexivity
–exact entry_fresh
–iModIntro
iExists _
iFrame
done
An existing key cannot be freshly recorded, even if its native object is live and the caller has no fragment for the old value.
Explore proof 7 tactics
Initial goal
intros Hfresh
specialize HfreshPLive1024 VLivetoken_regionout
Hfresh :
PLive1024, VLivetoken_regionout ∈ stream_psout 7 65; 66 ++ stream_pserr 3 [ ] → StreamHandleChecks.heap !! PLive1024 = None
⊢
False
assert Hin : PLive1024, VLivetoken_regionout ∈ stream_psout 7 65; 66 ++ stream_pserr 3 [ ] by apply list_elem_of_In ; simpl ; auto
specialize HfreshHin
Hfresh :
StreamHandleChecks.heap !! PLive1024 = None
⊢
False
unfold StreamHandleChecks.heap in Hfresh
Hfresh :
⊢
False
rewrite lookup_insert_eq in Hfresh
discriminate Hfresh
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hfresh
specialize HfreshPLive1024 VLivetoken_regionout
assert Hin : PLive1024, VLivetoken_regionout ∈ stream_psout 7 65; 66 ++ stream_pserr 3 [ ] by apply list_elem_of_In ; simpl ; auto
specialize HfreshHin
unfold StreamHandleChecks.heap in Hfresh
rewrite lookup_insert_eq in Hfresh
discriminate Hfresh
Explore proof 6 tactics
Initial goal
intros Hfresh
specialize HfreshPName−2 VStreamtoken_handleout Some7, 65; 66
assert Hin : PName−2, VStreamtoken_handleout Some7, 65; 66 ∈ stream_psout 7 65; 66 ++ stream_pserr 3 [ ] by apply list_elem_of_In ; simpl ; auto
specialize HfreshHin
rewrite lookup_insert_eq in Hfresh
discriminate Hfresh
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 3 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop b o : Z m : mem w : libc_world h : gmappiece pval, ¬stream_tokens_wirep out out b o m w h
intros rep b o m w h _ & _ & Hbad & _
⊢
False
apply Hbad
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep b o m w h _ & _ & Hbad & _
apply Hbad
reflexivity
918Example completed_close_not_readmitted: ¬stream_call_preF.model WPtrtoken_handleout changed_errno F.worldfalse
Explore proof 3 tactics
Initial goal
⊢
¬stream_call_preF.model WPtrtoken_handleout changed_errno F.worldfalse
intros p & info & Hargs & _ & Hopen & _
p :
info :
Hargs :
⊢
False
injection Hargs as ←
discriminate Hopen
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros p & info & Hargs & _ & Hopen & _
injection Hargs as ←
discriminate Hopen