rocq/theories/LibcStreamTokens.v
Callback stream tokens retain native handle lives but do not own private FILE bytes. The projection here is pure proof bookkeeping; it never deletes authoritative Iris resources.
From iris.proofmode Require Import proofmode
From Stdlib Require Import ZArith List Lia
From Nanofil Require Import Term Syntax Values Memory Runtime Identity ExternalCalls ExternalMachine Stdio Shutdown Streams Formatting Libc LibcStreams Pieces Heap ContractFrame Logic StringLogic LentLogic LibcStreamLogic LibcErrnoLogic
Open Scope Z_scope
Open Scope list_scope
Only designated life keys disappear. Byte and auxiliary pieces in either FILE object remain, so private-root separation still rejects caller ownership of FILE storage.
∀ out_base err_base h l v
stream_data_heapout_base err_base h !! l = Somev
Explore proof 5 tactics
Initial goal
intros out_base err_base h l v Hl
unfold stream_data_heap in Hl
apply lookup_delete_Some in Hl as Hout Hl
apply lookup_delete_Some in Hl as Herr Hl
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros out_base err_base h l v Hl
unfold stream_data_heap in Hl
apply lookup_delete_Some in Hl as Hout Hl
apply lookup_delete_Some in Hl as Herr Hl
auto
∀ out_base err_base h l
stream_data_heapout_base err_base h !! l = h !! l
Explore proof 3 tactics
Initial goal
intros out_base err_base h l Hout Herr
unfold stream_data_heap
rewrite ! lookup_delete_ne ; congruence
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros out_base err_base h l Hout Herr
unfold stream_data_heap
rewrite ! lookup_delete_ne ; congruence
Explore proof 3 tactics
Initial goal
intros out_base err_base m h Ha l v Hl
⊢
agree_piecem l v
apply stream_data_lookup in Hl as Hl _
exact Hal v Hl
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Restore exactly the removed lives, including their original region. Registration/persistence alone would also permit a freed handle.
Explore proof 15 tactics
Initial goal
⊢
∀out_base err_base : Z m m′ : mem h h′ : gmappiece pval, agreesm h → agreesm′ stream_data_heapout_base err_base h′ → persistsm m′ → h′ !! PLiveout_base = h !! PLiveout_base → h′ !! PLiveerr_base = h !! PLiveerr_base → ∀reg : region, live_atm out_base reg → live_atm′ out_base reg → ∀reg : region, live_atm err_base reg → live_atm′ err_base reg → agreesm′ h′
intros out_base err_base m m′ h h′ Ha Hdata Hp Houtkey Herrkey Hout Herr l v Hl
out_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
l :
v :
Hl :
h′ !! l = Somev
⊢
agree_piecem′ l v
destruct decidel = PLiveout_base as [ ->| Hneout ]
2 openout_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
v :
Hl :
h′ !! PLiveout_base = Somev
⊢
agree_piecem′ PLiveout_base v
focused goal
out_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
l :
v :
Hl :
h′ !! l = Somev
Hneout :
l ≠ PLiveout_base
⊢
agree_piecem′ l v
–rewrite Houtkey in Hl
2 openout_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
v :
Hl :
h !! PLiveout_base = Somev
⊢
agree_piecem′ PLiveout_base v
deferred goal
out_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
l :
v :
Hl :
h′ !! l = Somev
Hneout :
l ≠ PLiveout_base
⊢
agree_piecem′ l v
pose proof Ha_ _ Hl as Hag
2 openout_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
v :
Hl :
h !! PLiveout_base = Somev
Hag :
agree_piecem PLiveout_base v
⊢
agree_piecem′ PLiveout_base v
deferred goal
out_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
l :
v :
Hl :
h′ !! l = Somev
Hneout :
l ≠ PLiveout_base
⊢
agree_piecem′ l v
destruct v ; cbn [ agree_piece ] in Hag |- * ; try contradiction ; apply Hout ; exact Hag |
2 openout_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
Hag :
registeredm out_base
⊢
registeredm′ out_base
deferred goal
out_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
l :
v :
Hl :
h′ !! l = Somev
Hneout :
l ≠ PLiveout_base
⊢
agree_piecem′ l v
unfold registered in *
2 openout_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
Hag :
object_regionout_base m_regionsm ≠ None
⊢
object_regionout_base m_regionsm′ ≠ None
deferred goal
out_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
l :
v :
Hl :
h′ !! l = Somev
Hneout :
l ≠ PLiveout_base
⊢
agree_piecem′ l v
destruct object_regionout_base m_regionsm as reg | eqn: E ; destruct Hp_ _ E as E′ | E′ ; rewrite E' ; discriminate | contradiction
deferred goal
out_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
l :
v :
Hl :
h′ !! l = Somev
Hneout :
l ≠ PLiveout_base
⊢
agree_piecem′ l v
–destruct decidel = PLiveerr_base as [ ->| Hneerr ]
2 openout_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
v :
Hl :
h′ !! PLiveerr_base = Somev
⊢
agree_piecem′ PLiveerr_base v
focused goal
out_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
l :
v :
Hl :
h′ !! l = Somev
Hneout :
l ≠ PLiveout_base
Hneerr :
l ≠ PLiveerr_base
⊢
agree_piecem′ l v
+rewrite Herrkey in Hl
2 openout_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
v :
Hl :
h !! PLiveerr_base = Somev
⊢
agree_piecem′ PLiveerr_base v
deferred goal
out_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
l :
v :
Hl :
h′ !! l = Somev
Hneout :
l ≠ PLiveout_base
Hneerr :
l ≠ PLiveerr_base
⊢
agree_piecem′ l v
pose proof Ha_ _ Hl as Hag
2 openout_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
v :
Hl :
h !! PLiveerr_base = Somev
Hag :
agree_piecem PLiveerr_base v
⊢
agree_piecem′ PLiveerr_base v
deferred goal
out_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
l :
v :
Hl :
h′ !! l = Somev
Hneout :
l ≠ PLiveout_base
Hneerr :
l ≠ PLiveerr_base
⊢
agree_piecem′ l v
destruct v ; cbn [ agree_piece ] in Hag |- * ; try contradiction ; apply Herr ; exact Hag |
2 openout_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
Hag :
registeredm err_base
⊢
registeredm′ err_base
deferred goal
out_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
l :
v :
Hl :
h′ !! l = Somev
Hneout :
l ≠ PLiveout_base
Hneerr :
l ≠ PLiveerr_base
⊢
agree_piecem′ l v
unfold registered in *
2 openout_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
Hag :
object_regionerr_base m_regionsm ≠ None
⊢
object_regionerr_base m_regionsm′ ≠ None
deferred goal
out_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
l :
v :
Hl :
h′ !! l = Somev
Hneout :
l ≠ PLiveout_base
Hneerr :
l ≠ PLiveerr_base
⊢
agree_piecem′ l v
destruct object_regionerr_base m_regionsm as reg | eqn: E ; destruct Hp_ _ E as E′ | E′ ; rewrite E' ; discriminate | contradiction
deferred goal
out_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
l :
v :
Hl :
h′ !! l = Somev
Hneout :
l ≠ PLiveout_base
Hneerr :
l ≠ PLiveerr_base
⊢
agree_piecem′ l v
+apply Hdata
out_base, err_base :
Z
m, m′ :
Ha :
agreesm h
Hdata :
agreesm′ stream_data_heapout_base err_base h′
Hp :
persistsm m′
l :
v :
Hl :
h′ !! l = Somev
Hneout :
l ≠ PLiveout_base
Hneerr :
l ≠ PLiveerr_base
⊢
stream_data_heapout_base err_base h′ !! l = Somev
rewrite stream_data_lookup_ne ; assumption
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros out_base err_base m m′ h h′ Ha Hdata Hp Houtkey Herrkey Hout Herr l v Hl
destruct decidel = PLiveout_base as [ ->| Hneout ]
–rewrite Houtkey in Hl
pose proof Ha_ _ Hl as Hag
destruct v ; cbn [ agree_piece ] in Hag |- * ; try contradiction ; apply Hout ; exact Hag |
unfold registered in *
destruct object_regionout_base m_regionsm as reg | eqn: E ; destruct Hp_ _ E as E′ | E′ ; rewrite E' ; discriminate | contradiction
–destruct decidel = PLiveerr_base as [ ->| Hneerr ]
+rewrite Herrkey in Hl
pose proof Ha_ _ Hl as Hag
destruct v ; cbn [ agree_piece ] in Hag |- * ; try contradiction ; apply Herr ; exact Hag |
unfold registered in *
destruct object_regionerr_base m_regionsm as reg | eqn: E ; destruct Hp_ _ E as E′ | E′ ; rewrite E' ; discriminate | contradiction
+apply Hdata
rewrite stream_data_lookup_ne ; assumption
Updating data/ghost values commutes with the pure life projection, but updating one of the two erased life keys does not.
∀ ps out_base err_base h
stream_data_heapout_base err_base overwriteps h = overwriteps stream_data_heapout_base err_base h
Explore proof 9 tactics
Initial goal
⊢
∀ps : listpiece × pval out_base err_base : Z h : gmappiece pval, PLiveout_base ∉ ps.*1 → PLiveerr_base ∉ ps.*1 → stream_data_heapout_base err_base overwriteps h = overwriteps stream_data_heapout_base err_base h
induction ps as | l v ps IH ; intros out_base err_base h Hout Herr ; reflexivity |
l :
v :
IH :
∀out_base err_base : Z h : gmappiece pval, PLiveout_base ∉ ps.*1 → PLiveerr_base ∉ ps.*1 → stream_data_heapout_base err_base overwriteps h = overwriteps stream_data_heapout_base err_base h
out_base, err_base :
Z
Hout :
PLiveout_base ∉ l, v :: ps.*1
Herr :
PLiveerr_base ∉ l, v :: ps.*1
⊢
stream_data_heapout_base err_base overwritel, v :: ps h = overwritel, v :: ps stream_data_heapout_base err_base h
cbn [ fmap fst ] in Hout , Herr
l :
v :
IH :
∀out_base err_base : Z h : gmappiece pval, PLiveout_base ∉ ps.*1 → PLiveerr_base ∉ ps.*1 → stream_data_heapout_base err_base overwriteps h = overwriteps stream_data_heapout_base err_base h
out_base, err_base :
Z
⊢
stream_data_heapout_base err_base overwritel, v :: ps h = overwritel, v :: ps stream_data_heapout_base err_base h
apply not_elem_of_cons in Hout as Hout Houts
l :
v :
IH :
∀out_base err_base : Z h : gmappiece pval, PLiveout_base ∉ ps.*1 → PLiveerr_base ∉ ps.*1 → stream_data_heapout_base err_base overwriteps h = overwriteps stream_data_heapout_base err_base h
out_base, err_base :
Z
Hout :
PLiveout_base ≠ l, v.1
Houts :
⊢
stream_data_heapout_base err_base overwritel, v :: ps h = overwritel, v :: ps stream_data_heapout_base err_base h
apply not_elem_of_cons in Herr as Herr Herrs
l :
v :
IH :
∀out_base err_base : Z h : gmappiece pval, PLiveout_base ∉ ps.*1 → PLiveerr_base ∉ ps.*1 → stream_data_heapout_base err_base overwriteps h = overwriteps stream_data_heapout_base err_base h
out_base, err_base :
Z
Hout :
PLiveout_base ≠ l, v.1
Houts :
Herr :
PLiveerr_base ≠ l, v.1
⊢
stream_data_heapout_base err_base overwritel, v :: ps h = overwritel, v :: ps stream_data_heapout_base err_base h
cbn [ overwrite ]
l :
v :
IH :
∀out_base err_base : Z h : gmappiece pval, PLiveout_base ∉ ps.*1 → PLiveerr_base ∉ ps.*1 → stream_data_heapout_base err_base overwriteps h = overwriteps stream_data_heapout_base err_base h
out_base, err_base :
Z
Hout :
PLiveout_base ≠ l, v.1
Houts :
Herr :
PLiveerr_base ≠ l, v.1
⊢
stream_data_heapout_base err_base <[l, v.1 ≔ l, v.2]>overwriteps h = <[l, v.1 ≔ l, v.2]>overwriteps stream_data_heapout_base err_base h
unfold stream_data_heap at 1
l :
v :
IH :
∀out_base err_base : Z h : gmappiece pval, PLiveout_base ∉ ps.*1 → PLiveerr_base ∉ ps.*1 → stream_data_heapout_base err_base overwriteps h = overwriteps stream_data_heapout_base err_base h
out_base, err_base :
Z
Hout :
PLiveout_base ≠ l, v.1
Houts :
Herr :
PLiveerr_base ≠ l, v.1
⊢
deletePLiveout_base deletePLiveerr_base <[l, v.1 ≔ l, v.2]>overwriteps h = <[l, v.1 ≔ l, v.2]>overwriteps stream_data_heapout_base err_base h
rewrite ! delete_insert_ne ; try congruence
l :
v :
IH :
∀out_base err_base : Z h : gmappiece pval, PLiveout_base ∉ ps.*1 → PLiveerr_base ∉ ps.*1 → stream_data_heapout_base err_base overwriteps h = overwriteps stream_data_heapout_base err_base h
out_base, err_base :
Z
Hout :
PLiveout_base ≠ l, v.1
Houts :
Herr :
PLiveerr_base ≠ l, v.1
⊢
<[l, v.1 ≔ l, v.2]>deletePLiveout_base deletePLiveerr_base overwriteps h = <[l, v.1 ≔ l, v.2]>overwriteps stream_data_heapout_base err_base h
change <[l ≔ v]>stream_data_heapout_base err_base overwriteps h = <[l ≔ v]>overwriteps stream_data_heapout_base err_base h
l :
v :
IH :
∀out_base err_base : Z h : gmappiece pval, PLiveout_base ∉ ps.*1 → PLiveerr_base ∉ ps.*1 → stream_data_heapout_base err_base overwriteps h = overwriteps stream_data_heapout_base err_base h
out_base, err_base :
Z
Hout :
PLiveout_base ≠ l, v.1
Houts :
Herr :
PLiveerr_base ≠ l, v.1
⊢
<[l ≔ v]>stream_data_heapout_base err_base overwriteps h = <[l ≔ v]>overwriteps stream_data_heapout_base err_base h
rewrite IH ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
induction ps as | l v ps IH ; intros out_base err_base h Hout Herr ; reflexivity |
cbn [ fmap fst ] in Hout , Herr
apply not_elem_of_cons in Hout as Hout Houts
apply not_elem_of_cons in Herr as Herr Herrs
cbn [ overwrite ]
unfold stream_data_heap at 1
rewrite ! delete_insert_ne ; try congruence
change <[l ≔ v]>stream_data_heapout_base err_base overwriteps h = <[l ≔ v]>overwriteps stream_data_heapout_base err_base h
rewrite IH ; auto
Native readiness excludes BOTH stable FILE identities from every active release pool, not just the selected handle's identity.
∀ rep m w p q base
¬Inbase libc_stream_releasesw p
Explore proof 13 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop m : mem w : libc_world p q : ptr base : Z, libc_stream_readyrep m w → q = libc_stdoutw ∨ q = libc_stderrw → ptr_capq = Objbase → ¬Inbase libc_stream_releasesw p
intros rep m w p q base _ & _ & _ & _ & _ & _ & _ & _ & _ & _ & _ & _ & Hsep Hq Hcap Hin
rep :
mem → libc_world → Prop
m :
w :
p, q :
base :
Z
Hsep :
Hq :
q = libc_stdoutw ∨ q = libc_stderrw
Hin :
Inbase libc_stream_releasesw p
⊢
False
unfold libc_stream_releases in Hin
rep :
mem → libc_world → Prop
m :
w :
p, q :
base :
Z
Hsep :
Hq :
q = libc_stdoutw ∨ q = libc_stderrw
Hin :
Inbase
None
⇒
[ ]
⊢
False
destruct libc_file_atw p as file | eqn: Hfile ; | contradiction
rep :
mem → libc_world → Prop
m :
w :
p, q :
base :
Z
Hsep :
Hq :
q = libc_stdoutw ∨ q = libc_stderrw
file :
Hfile :
libc_file_atw p = Somefile
Hin :
Inbase file_ownedfile
⊢
False
destruct Hsepp file Hfile base Hin as _ & _ & Hnot & _
rep :
mem → libc_world → Prop
m :
w :
p, q :
base :
Z
Hsep :
Hq :
q = libc_stdoutw ∨ q = libc_stderrw
file :
Hfile :
libc_file_atw p = Somefile
Hin :
Inbase file_ownedfile
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: Locale.locale_private_sourceslibc_localew.1 ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
⊢
False
apply Hnot
rep :
mem → libc_world → Prop
m :
w :
p, q :
base :
Z
Hsep :
Hq :
q = libc_stdoutw ∨ q = libc_stderrw
file :
Hfile :
libc_file_atw p = Somefile
Hin :
Inbase file_ownedfile
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: Locale.locale_private_sourceslibc_localew.1 ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
⊢
[ ]
m
Objbase
right
rep :
mem → libc_world → Prop
m :
w :
p, q :
base :
Z
Hsep :
Hq :
q = libc_stdoutw ∨ q = libc_stderrw
file :
Hfile :
libc_file_atw p = Somefile
Hin :
Inbase file_ownedfile
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: Locale.locale_private_sourceslibc_localew.1 ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
⊢
Ins
∧
∨
Ins
∧
∨
left
rep :
mem → libc_world → Prop
m :
w :
p, q :
base :
Z
Hsep :
Hq :
q = libc_stdoutw ∨ q = libc_stderrw
file :
Hfile :
libc_file_atw p = Somefile
Hin :
Inbase file_ownedfile
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: Locale.locale_private_sourceslibc_localew.1 ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
⊢
Ins
∧
exists mkSpanq 0
rep :
mem → libc_world → Prop
m :
w :
p, q :
base :
Z
Hsep :
Hq :
q = libc_stdoutw ∨ q = libc_stderrw
file :
Hfile :
libc_file_atw p = Somefile
Hin :
Inbase file_ownedfile
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: Locale.locale_private_sourceslibc_localew.1 ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
⊢
∧
split
2 openrep :
mem → libc_world → Prop
m :
w :
p, q :
base :
Z
Hsep :
Hq :
q = libc_stdoutw ∨ q = libc_stderrw
file :
Hfile :
libc_file_atw p = Somefile
Hin :
Inbase file_ownedfile
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: Locale.locale_private_sourceslibc_localew.1 ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
⊢
focused goal
rep :
mem → libc_world → Prop
m :
w :
p, q :
base :
Z
Hsep :
Hq :
q = libc_stdoutw ∨ q = libc_stderrw
file :
Hfile :
libc_file_atw p = Somefile
Hin :
Inbase file_ownedfile
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: Locale.locale_private_sourceslibc_localew.1 ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
–destruct Hq as → | → ; left ; reflexivity | right ; left ; reflexivity
deferred goal
rep :
mem → libc_world → Prop
m :
w :
p, q :
base :
Z
Hsep :
Hq :
q = libc_stdoutw ∨ q = libc_stderrw
file :
Hfile :
libc_file_atw p = Somefile
Hin :
Inbase file_ownedfile
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: Locale.locale_private_sourceslibc_localew.1 ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
–simpl
rep :
mem → libc_world → Prop
m :
w :
p, q :
base :
Z
Hsep :
Hq :
q = libc_stdoutw ∨ q = libc_stderrw
file :
Hfile :
libc_file_atw p = Somefile
Hin :
Inbase file_ownedfile
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: Locale.locale_private_sourceslibc_localew.1 ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
symmetry
rep :
mem → libc_world → Prop
m :
w :
p, q :
base :
Z
Hsep :
Hq :
q = libc_stdoutw ∨ q = libc_stderrw
file :
Hfile :
libc_file_atw p = Somefile
Hin :
Inbase file_ownedfile
Hnot :
¬available_capspan_ptr ≔ libc_stdoutw; span_size ≔ 0 :: span_ptr ≔ libc_stderrw; span_size ≔ 0 :: Locale.locale_private_sourceslibc_localew.1 ++ if same_filep libc_stdoutw then match libc_file_atw libc_stderrw with Someother ⇒ file_sourcesother None ⇒ [ ] end else match libc_file_atw libc_stdoutw with Someother ⇒ file_sourcesother None ⇒ [ ] end [ ] m Objbase
exact Hcap
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep m w p q base _ & _ & _ & _ & _ & _ & _ & _ & _ & _ & _ & _ & Hsep Hq Hcap Hin
unfold libc_stream_releases in Hin
destruct libc_file_atw p as file | eqn: Hfile ; | contradiction
destruct Hsepp file Hfile base Hin as _ & _ & Hnot & _
apply Hnot
right
left
exists mkSpanq 0
split
–destruct Hq as → | → ; left ; reflexivity | right ; left ; reflexivity
–simpl
symmetry
exact Hcap
The existing effects frame proves stable handle life independently of byte-write roots. It may mutate locks inside the FILE object; only releasing that object's identity is excluded. Fresh allocation cannot turn the old handle into a born identity.
M.E.prefixspec xs s m w born trace s′ m′ w′
R.readys m
live_atm b reg
¬Inb contract_releasesspec xs m w
live_atm′ b reg
Explore proof 26 tactics
Initial goal
⊢
∀world : Type spec : contractworld xs : listword s : R.state m : mem w : world born : listZ trace : listevent s′ : R.state m′ : mem w′ : world b : Z reg : region, M.E.prefixspec xs s m w born trace s′ m′ w′ → R.readys m → live_disjointm → live_atm b reg → ¬Inb contract_releasesspec xs m w → live_atm′ b reg
intros world spec xs s m w born trace s′ m′ w′ b reg Hp Hr Hd Hlive Hrelease
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
⊢
live_atm′ b reg
assert Ha : agreesm singletonMPLiveb VLivereg : gmappiece pval
2 openworld :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
⊢
agrees m {[PLive b := VLive reg]}focused goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
live_atm′ b reg
{intros l v Hl
2 openworld :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
l :
v :
Hl : {[PLive b := VLive reg]} !! l = Some v⊢
agree_piecem l v
deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
live_atm′ b reg
apply lookup_singleton_Some in Hl as Hl Hv
2 openworld :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
l :
v :
Hl :
PLiveb = l
Hv :
VLivereg = v
⊢
agree_piecem l v
deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
live_atm′ b reg
subst l v
2 openworld :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
⊢
agree_piecem PLiveb VLivereg
deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
live_atm′ b reg
exact Hlive
deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
live_atm′ b reg
destruct LG.prefix_agrees_out_ _ _ _ _ _ _ _ _ _ _ singletonMPLiveb VLivereg : gmappiece pval [ ] λ_ ⇒ True Hp Hr Hd as Hafter & _
6 openworld :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
agrees_except [] m {[PLive b := VLive reg]}focused goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
LG.ids_registered {[PLive b := VLive reg]} mfocused goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
roots_out (contract_writes spec xs m w) {[PLive b := VLive reg]} m
(λ _ : Z, True)focused goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
pieces_off [] {[PLive b := VLive reg]} m (λ _ : Z, True)focused goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
ids_apart (contract_releases spec xs m w) {[PLive b := VLive reg]}focused goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
–intros l v Hl _
6 openworld :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)l :
v :
Hl : {[PLive b := VLive reg]} !! l = Some v⊢
agree_piecem l v
deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
LG.ids_registered {[PLive b := VLive reg]} mdeferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
roots_out (contract_writes spec xs m w) {[PLive b := VLive reg]} m
(λ _ : Z, True)deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
pieces_off [] {[PLive b := VLive reg]} m (λ _ : Z, True)deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
ids_apart (contract_releases spec xs m w) {[PLive b := VLive reg]}deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
exact Hal v Hl
5 opendeferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
LG.ids_registered {[PLive b := VLive reg]} mdeferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
roots_out (contract_writes spec xs m w) {[PLive b := VLive reg]} m
(λ _ : Z, True)deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
pieces_off [] {[PLive b := VLive reg]} m (λ _ : Z, True)deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
ids_apart (contract_releases spec xs m w) {[PLive b := VLive reg]}deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
–intros l v Hl Hmem
5 openworld :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)l :
v :
Hl : {[PLive b := VLive reg]} !! l = Some vHmem :
deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
roots_out (contract_writes spec xs m w) {[PLive b := VLive reg]} m
(λ _ : Z, True)deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
pieces_off [] {[PLive b := VLive reg]} m (λ _ : Z, True)deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
ids_apart (contract_releases spec xs m w) {[PLive b := VLive reg]}deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
eapply agree_piece_registered ; exact Hmem | exact Hal v Hl
4 opendeferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
roots_out (contract_writes spec xs m w) {[PLive b := VLive reg]} m
(λ _ : Z, True)deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
pieces_off [] {[PLive b := VLive reg]} m (λ _ : Z, True)deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
ids_apart (contract_releases spec xs m w) {[PLive b := VLive reg]}deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
–intros root a Hin Hspan Howned
4 openworld :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)root :
a :
Z
Hin :
Inroot contract_writesspec xs m w
Hspan :
span_containsroot a
Howned : owned_live {[PLive b := VLive reg]} m a⊢
True
deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
pieces_off [] {[PLive b := VLive reg]} m (λ _ : Z, True)deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
ids_apart (contract_releases spec xs m w) {[PLive b := VLive reg]}deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
exact I
3 opendeferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
pieces_off [] {[PLive b := VLive reg]} m (λ _ : Z, True)deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
ids_apart (contract_releases spec xs m w) {[PLive b := VLive reg]}deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
–intros l v Hl _
3 openworld :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)l :
v :
Hl : {[PLive b := VLive reg]} !! l = Some vdeferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
ids_apart (contract_releases spec xs m w) {[PLive b := VLive reg]}deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
apply lookup_singleton_Some in Hl as Hl Hv
3 openworld :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)l :
v :
Hl :
PLiveb = l
Hv :
VLivereg = v
deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
ids_apart (contract_releases spec xs m w) {[PLive b := VLive reg]}deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
subst l v
3 openworld :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
True
deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
ids_apart (contract_releases spec xs m w) {[PLive b := VLive reg]}deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
exact I
2 opendeferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)⊢
ids_apart (contract_releases spec xs m w) {[PLive b := VLive reg]}deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
–intros base l v Hin Hl Hmem
2 openworld :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)base :
Z
l :
v :
Hin :
Inbase contract_releasesspec xs m w
Hl : {[PLive b := VLive reg]} !! l = Some vHmem :
⊢
piece_idl ≠ base
deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
apply lookup_singleton_Some in Hl as Hl Hv
2 openworld :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)base :
Z
l :
v :
Hin :
Inbase contract_releasesspec xs m w
Hl :
PLiveb = l
Hv :
VLivereg = v
Hmem :
⊢
piece_idl ≠ base
deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
subst l v
2 openworld :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)base :
Z
Hin :
Inbase contract_releasesspec xs m w
deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
simpl
2 openworld :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)base :
Z
Hin :
Inbase contract_releasesspec xs m w
⊢
b ≠ base
deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
intros →
2 openworld :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
base :
Z
Ha : agrees m {[PLive base := VLive reg]}Hrelease :
¬Inbase contract_releasesspec xs m w
Hlive :
live_atm base reg
Hin :
Inbase contract_releasesspec xs m w
⊢
False
deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
contradiction
deferred goal
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
live_atm′ b reg
–apply HafterPLiveb VLivereg ; apply lookup_singleton_Some ; auto |
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}⊢
PLiveb ∉ [ ]
intros Hnil
world :
Type
spec :
contractworld
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
b :
Z
reg :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hr :
R.readys m
Hd :
Hlive :
live_atm b reg
Hrelease :
¬Inb contract_releasesspec xs m w
Ha : agrees m ({[PLive b := VLive reg]} : gmap piece pval)Hafter : agrees_except [] m' {[PLive b := VLive reg]}Hnil :
PLiveb ∈ [ ]
⊢
False
inversion Hnil
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros world spec xs s m w born trace s′ m′ w′ b reg Hp Hr Hd Hlive Hrelease
{intros l v Hl
apply lookup_singleton_Some in Hl as Hl Hv
subst l v
exact Hlive
destruct LG.prefix_agrees_out_ _ _ _ _ _ _ _ _ _ _ singletonMPLiveb VLivereg : gmappiece pval [ ] λ_ ⇒ True Hp Hr Hd as Hafter & _
–intros l v Hl _
exact Hal v Hl
–intros l v Hl Hmem
eapply agree_piece_registered ; exact Hmem | exact Hal v Hl
–intros root a Hin Hspan Howned
exact I
–intros l v Hl _
apply lookup_singleton_Some in Hl as Hl Hv
subst l v
exact I
–intros base l v Hin Hl Hmem
apply lookup_singleton_Some in Hl as Hl Hv
subst l v
simpl
intros →
contradiction
A query may write private locks inside either stable handle. The data frame deliberately omits only their life keys, then the no-release effects frame restores those exact original regions.
∀ rep requests wide out_base err_base p b o spec r args s m w trace ending s′ m′ w′ h
spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide
M.E.invokespec r args WPtrp s m w trace ending s′ m′ w′
agreesm h
R.readys m
libc_errno_wirep p b o m w stream_data_heapout_base err_base h
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
Explore proof 11 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop out_base err_base : Z p : ptr b o : Z spec : contractlibc_world r : call_result args : listarg s : R.state m : mem w : libc_world trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world h : gmappiece pval, spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide → M.E.invokespec r args WPtrp s m w trace ending s′ m′ w′ → agreesm h → live_disjointm → R.readys m → libc_errno_wirep p b o m w stream_data_heapout_base err_base h → agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
intros rep requests wide out_base err_base p b o spec r args s m w trace ending s′ m′ w′ h Hspec Hcall Ha Hd Hr Hwi
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out_base, err_base :
Z
p :
b, o :
Z
spec :
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hspec :
spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide
Hcall :
M.E.invokespec r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hwi :
libc_errno_wirep p b o m w stream_data_heapout_base err_base h
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
pose proof stream_data_agreesout_base err_base m h Ha as Hdata
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out_base, err_base :
Z
p :
b, o :
Z
spec :
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hspec :
spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide
Hcall :
M.E.invokespec r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hwi :
libc_errno_wirep p b o m w stream_data_heapout_base err_base h
Hdata :
agreesm stream_data_heapout_base err_base h
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
destruct EL.query_framerep requests wide p b o spec r args s m w trace ending s′ m′ w′ stream_data_heapout_base err_base h Hspec Hcall Hdata Hd Hr Hwi as Hdata′ & Hd′ & Hr′ & Hwi′
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out_base, err_base :
Z
p :
b, o :
Z
spec :
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hspec :
spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide
Hcall :
M.E.invokespec r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hwi :
libc_errno_wirep p b o m w stream_data_heapout_base err_base h
Hdata :
agreesm stream_data_heapout_base err_base h
Hdata′ :
agreesm′ stream_data_heapout_base err_base h
Hd′ :
Hr′ :
R.readys′ m′
Hwi′ :
libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & Hp
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out_base, err_base :
Z
p :
b, o :
Z
spec :
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hspec :
spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide
Hcall :
M.E.invokespec r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hwi :
libc_errno_wirep p b o m w stream_data_heapout_base err_base h
Hdata :
agreesm stream_data_heapout_base err_base h
Hdata′ :
agreesm′ stream_data_heapout_base err_base h
Hd′ :
Hr′ :
R.readys′ m′
Hwi′ :
libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
born :
listZ
Hp :
M.E.prefixspec WPtrp s m w born trace s′ m′ w′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as _ Hpers
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out_base, err_base :
Z
p :
b, o :
Z
spec :
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hspec :
spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide
Hcall :
M.E.invokespec r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hwi :
libc_errno_wirep p b o m w stream_data_heapout_base err_base h
Hdata :
agreesm stream_data_heapout_base err_base h
Hdata′ :
agreesm′ stream_data_heapout_base err_base h
Hd′ :
Hr′ :
R.readys′ m′
Hwi′ :
libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
born :
listZ
Hp :
M.E.prefixspec WPtrp s m w born trace s′ m′ w′
Hpers :
persistsm m′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
assert Hrelease : ∀base, ¬Inbase contract_releasesspec WPtrp m w
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out_base, err_base :
Z
p :
b, o :
Z
spec :
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hspec :
spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide
Hcall :
M.E.invokespec r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hwi :
libc_errno_wirep p b o m w stream_data_heapout_base err_base h
Hdata :
agreesm stream_data_heapout_base err_base h
Hdata′ :
agreesm′ stream_data_heapout_base err_base h
Hd′ :
Hr′ :
R.readys′ m′
Hwi′ :
libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
born :
listZ
Hp :
M.E.prefixspec WPtrp s m w born trace s′ m′ w′
Hpers :
persistsm m′
⊢
∀base : Z, ¬Inbase contract_releasesspec WPtrp m w
focused goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out_base, err_base :
Z
p :
b, o :
Z
spec :
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hspec :
spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide
Hcall :
M.E.invokespec r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hwi :
libc_errno_wirep p b o m w stream_data_heapout_base err_base h
Hdata :
agreesm stream_data_heapout_base err_base h
Hdata′ :
agreesm′ stream_data_heapout_base err_base h
Hd′ :
Hr′ :
R.readys′ m′
Hwi′ :
libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
born :
listZ
Hp :
M.E.prefixspec WPtrp s m w born trace s′ m′ w′
Hpers :
persistsm m′
Hrelease :
∀base : Z, ¬Inbase contract_releasesspec WPtrp m w
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
{intros base
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out_base, err_base :
Z
p :
b, o :
Z
spec :
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hspec :
spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide
Hcall :
M.E.invokespec r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hwi :
libc_errno_wirep p b o m w stream_data_heapout_base err_base h
Hdata :
agreesm stream_data_heapout_base err_base h
Hdata′ :
agreesm′ stream_data_heapout_base err_base h
Hd′ :
Hr′ :
R.readys′ m′
Hwi′ :
libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
born :
listZ
Hp :
M.E.prefixspec WPtrp s m w born trace s′ m′ w′
Hpers :
persistsm m′
base :
Z
⊢
¬Inbase contract_releasesspec WPtrp m w
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out_base, err_base :
Z
p :
b, o :
Z
spec :
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hspec :
spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide
Hcall :
M.E.invokespec r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hwi :
libc_errno_wirep p b o m w stream_data_heapout_base err_base h
Hdata :
agreesm stream_data_heapout_base err_base h
Hdata′ :
agreesm′ stream_data_heapout_base err_base h
Hd′ :
Hr′ :
R.readys′ m′
Hwi′ :
libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
born :
listZ
Hp :
M.E.prefixspec WPtrp s m w born trace s′ m′ w′
Hpers :
persistsm m′
Hrelease :
∀base : Z, ¬Inbase contract_releasesspec WPtrp m w
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
destruct Hspec as → | → ; cbn [ ferror_contract fpending_contract contract_releases ] ; tauto
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out_base, err_base :
Z
p :
b, o :
Z
spec :
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hspec :
spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide
Hcall :
M.E.invokespec r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hwi :
libc_errno_wirep p b o m w stream_data_heapout_base err_base h
Hdata :
agreesm stream_data_heapout_base err_base h
Hdata′ :
agreesm′ stream_data_heapout_base err_base h
Hd′ :
Hr′ :
R.readys′ m′
Hwi′ :
libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
born :
listZ
Hp :
M.E.prefixspec WPtrp s m w born trace s′ m′ w′
Hpers :
persistsm m′
Hrelease :
∀base : Z, ¬Inbase contract_releasesspec WPtrp m w
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
split ; | auto
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out_base, err_base :
Z
p :
b, o :
Z
spec :
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hspec :
spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide
Hcall :
M.E.invokespec r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hwi :
libc_errno_wirep p b o m w stream_data_heapout_base err_base h
Hdata :
agreesm stream_data_heapout_base err_base h
Hdata′ :
agreesm′ stream_data_heapout_base err_base h
Hd′ :
Hr′ :
R.readys′ m′
Hwi′ :
libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
born :
listZ
Hp :
M.E.prefixspec WPtrp s m w born trace s′ m′ w′
Hpers :
persistsm m′
Hrelease :
∀base : Z, ¬Inbase contract_releasesspec WPtrp m w
⊢
agreesm′ h
eapply stream_data_restore ; exact Ha | exact Hdata′ | exact Hpers | reflexivity | reflexivity | |
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out_base, err_base :
Z
p :
b, o :
Z
spec :
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hspec :
spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide
Hcall :
M.E.invokespec r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hwi :
libc_errno_wirep p b o m w stream_data_heapout_base err_base h
Hdata :
agreesm stream_data_heapout_base err_base h
Hdata′ :
agreesm′ stream_data_heapout_base err_base h
Hd′ :
Hr′ :
R.readys′ m′
Hwi′ :
libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
born :
listZ
Hp :
M.E.prefixspec WPtrp s m w born trace s′ m′ w′
Hpers :
persistsm m′
Hrelease :
∀base : Z, ¬Inbase contract_releasesspec WPtrp m w
focused goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
out_base, err_base :
Z
p :
b, o :
Z
spec :
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hspec :
spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide
Hcall :
M.E.invokespec r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hwi :
libc_errno_wirep p b o m w stream_data_heapout_base err_base h
Hdata :
agreesm stream_data_heapout_base err_base h
Hdata′ :
agreesm′ stream_data_heapout_base err_base h
Hd′ :
Hr′ :
R.readys′ m′
Hwi′ :
libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base h
born :
listZ
Hp :
M.E.prefixspec WPtrp s m w born trace s′ m′ w′
Hpers :
persistsm m′
Hrelease :
∀base : Z, ¬Inbase contract_releasesspec WPtrp m w
all: intros reg Hlive ; eapply prefix_handle_live ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide out_base err_base p b o spec r args s m w trace ending s′ m′ w′ h Hspec Hcall Ha Hd Hr Hwi
pose proof stream_data_agreesout_base err_base m h Ha as Hdata
destruct EL.query_framerep requests wide p b o spec r args s m w trace ending s′ m′ w′ stream_data_heapout_base err_base h Hspec Hcall Hdata Hd Hr Hwi as Hdata′ & Hd′ & Hr′ & Hwi′
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & Hp
destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as _ Hpers
assert Hrelease : ∀base, ¬Inbase contract_releasesspec WPtrp m w
{intros base
destruct Hspec as → | → ; cbn [ ferror_contract fpending_contract contract_releases ] ; tauto
split ; | auto
eapply stream_data_restore ; exact Ha | exact Hdata′ | exact Hpers | reflexivity | reflexivity | |
all: intros reg Hlive ; eapply prefix_handle_live ; eauto
Close updates actual endpoint errno bytes and retains both native handle lives, including on a resource-ending prefix. This theorem deliberately makes no closed-token claim on that prefix.
∀ rep requests wide out_base err_base p b o r args s m w trace ending s′ m′ w′ h xs
ptr_caplibc_stdoutw = Objout_base
ptr_caplibc_stderrw = Objerr_base
M.E.invokefclose_contractlibc_stream_modelrep requests wide r args WPtrp s m w trace ending s′ m′ w′
agreesm h
R.readys m
libc_errno_wirep p b o m w stream_data_heapout_base err_base 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′ overwritebyte_psb o ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ stream_data_heapout_base err_base overwritebyte_psb o ys h
Proof 40 steps Qed
intros rep requests wide out_base err_base p b o r args s m w trace ending s′ m′ w′ h xs Houtcap Herrcap Hcall Ha Hd Hr Hwi Hlen Howned
{intros base zs Hkey
rewrite byte_ps_keys in Hkey
apply list_elem_of_fmap in Hkey as i & E & _
discriminate E
destruct EL.close_framerep requests wide p b o r args s m w trace ending s' m' w' stream_data_heapout_base err_base h xs Hcall stream_data_agreesout_base err_base m h Ha Hd Hr Hwi Hlen as ys & Hys & Hkeys & Hdata′ & Hd′ & Hr′ & Hwi′
–intros l v Hin
rewrite stream_data_lookup_ne ; exact Hownedl v Hin | |
–assert Hcommute := stream_data_overwritebyte_psb o ys out_base err_base h Hlife_offout_base ys Hlife_offerr_base ys
rewrite <- Hcommute in Hdata' , Hwi'
exists ys
split ; exact Hys |
split ; exact Hkeys |
split ; | auto
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & Hp
destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as _ Hpers
eapply stream_data_restore ; exact Ha | exact Hdata' | exact Hpers | | | |
+apply overwrite_out , Hlife_off
+apply overwrite_out , Hlife_off
+intros reg Hlive
eapply prefix_handle_live ; exact Hp | exact Hr | exact Hd | exact Hlive |
change ¬Inout_base libc_stream_releasesw p
eapply libc_handle_not_released ; exact proj1Hwi | left ; reflexivity | exact Houtcap
+intros reg Hlive
eapply prefix_handle_live ; exact Hp | exact Hr | exact Hd | exact Hlive |
change ¬Inerr_base libc_stream_releasesw p
eapply libc_handle_not_released ; exact proj1Hwi | right ; reflexivity | exact Herrcap
Logical controls use HelloClose's actual machine. The tiny fixture objects are not claimed to be native FILE representations.
stream_data_heap1024 2048 heap = E.heap
Explore proof 12 tactics
Initial goal
⊢
stream_data_heap1024 2048 heap = E.heap
assert Hnone : ∀base, E.heap !! PLivebase = None
2 openfocused goal
⊢
stream_data_heap1024 2048 heap = E.heap
{intros base
2 opendeferred goal
⊢
stream_data_heap1024 2048 heap = E.heap
apply eq_None_not_Some
2 opendeferred goal
⊢
stream_data_heap1024 2048 heap = E.heap
intros v Hl
2 opendeferred goal
⊢
stream_data_heap1024 2048 heap = E.heap
unfold E.heap in Hl
2 opendeferred goal
⊢
stream_data_heap1024 2048 heap = E.heap
apply elem_of_list_to_map_2 in Hl
2 opendeferred goal
⊢
stream_data_heap1024 2048 heap = E.heap
destruct MemLogic.byte_ps_elem_ _ _ _ _ Hl as i & x & Hi & He & Hv
2 open⊢
False
deferred goal
⊢
stream_data_heap1024 2048 heap = E.heap
discriminate He
deferred goal
⊢
stream_data_heap1024 2048 heap = E.heap
unfold stream_data_heap , heap
rewrite delete_insert_ne ; | discriminate
rewrite ! delete_insert_eq
rewrite ! delete_id ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
{intros base
apply eq_None_not_Some
intros v Hl
unfold E.heap in Hl
apply elem_of_list_to_map_2 in Hl
destruct MemLogic.byte_ps_elem_ _ _ _ _ Hl as i & x & Hi & He & Hv
discriminate He
unfold stream_data_heap , heap
rewrite delete_insert_ne ; | discriminate
rewrite ! delete_insert_eq
rewrite ! delete_id ; auto
Explore proof 5 tactics
Initial goal
intros l v Hl
unfold heap in Hl
apply lookup_insert_Some in Hl as He Hv | Hne Hl ; subst l v ; split ; reflexivity |
apply lookup_insert_Some in Hl as He Hv | Hne′ Hl ; subst l v ; split ; reflexivity |
exact E.heap_agreesl v Hl
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros l v Hl
unfold heap in Hl
apply lookup_insert_Some in Hl as He Hv | Hne Hl ; subst l v ; split ; reflexivity |
apply lookup_insert_Some in Hl as He Hv | Hne′ Hl ; subst l v ; split ; reflexivity |
exact E.heap_agreesl v Hl
Owned errno plus BOTH stable native lives coexist with the query frame; this is not an empty ghost heap or a sibling logic.
238Example held_handles_query: LG.L.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrfile_handleF.out_file InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt7 InterpRuntime.start conversion_mem F.worldtrue ∧ agreesconversion_mem heap ∧ libc_errno_wiλ_ _ ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
Explore proof 12 tactics
Initial goal
⊢
LG.L.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrfile_handleF.out_file InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt7 InterpRuntime.start conversion_mem F.worldtrue ∧ agreesconversion_mem heap ∧ libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
assert Hcall : LG.L.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrfile_handleF.out_file InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt7 InterpRuntime.start conversion_mem F.worldtrue
2 open⊢
focused goal
Hcall :
⊢
LG.L.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrfile_handleF.out_file InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt7 InterpRuntime.start conversion_mem F.worldtrue ∧ agreesconversion_mem heap ∧ libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
{apply C.fpending_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 file_handleF.out_file = SomeF.out_file
deferred goal
Hcall :
⊢
LG.L.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrfile_handleF.out_file InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt7 InterpRuntime.start conversion_mem F.worldtrue ∧ agreesconversion_mem heap ∧ libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
–split ; left ; reflexivity |
4 opendeferred goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue
deferred goal
⊢
libc_file_atF.worldtrue file_handleF.out_file = SomeF.out_file
deferred goal
Hcall :
⊢
LG.L.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrfile_handleF.out_file InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt7 InterpRuntime.start conversion_mem F.worldtrue ∧ agreesconversion_mem heap ∧ libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
exists Const0
4 opendeferred goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue
deferred goal
⊢
libc_file_atF.worldtrue file_handleF.out_file = SomeF.out_file
deferred goal
Hcall :
⊢
LG.L.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrfile_handleF.out_file InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt7 InterpRuntime.start conversion_mem F.worldtrue ∧ agreesconversion_mem heap ∧ libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
reflexivity
3 opendeferred goal
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue
deferred goal
⊢
libc_file_atF.worldtrue file_handleF.out_file = SomeF.out_file
deferred goal
Hcall :
⊢
LG.L.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrfile_handleF.out_file InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt7 InterpRuntime.start conversion_mem F.worldtrue ∧ agreesconversion_mem heap ∧ libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
–apply F.ready
2 opendeferred goal
⊢
libc_file_atF.worldtrue file_handleF.out_file = SomeF.out_file
deferred goal
Hcall :
⊢
LG.L.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrfile_handleF.out_file InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt7 InterpRuntime.start conversion_mem F.worldtrue ∧ agreesconversion_mem heap ∧ libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
–reflexivity
deferred goal
Hcall :
⊢
LG.L.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrfile_handleF.out_file InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt7 InterpRuntime.start conversion_mem F.worldtrue ∧ agreesconversion_mem heap ∧ libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
split ; exact Hcall |
Hcall :
⊢
agreesconversion_mem heap ∧ libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
destruct T.query_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False 1024 2048 file_handleF.out_file 5120 0 _ _ _ _ _ _ _ _ _ _ _ heap or_introreq_refl Hcall heap_agrees E.disjoint E.ready as Ha & _ & _ & Hw
2 openHcall :
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
focused goal
Hcall :
Hw :
libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
⊢
agreesconversion_mem heap ∧ libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
–rewrite data_heap
2 openHcall :
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue E.heap
deferred goal
Hcall :
Hw :
libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
⊢
agreesconversion_mem heap ∧ libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
exact E.heap_wi
deferred goal
Hcall :
Hw :
libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
⊢
agreesconversion_mem heap ∧ libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue stream_data_heap1024 2048 heap
–auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
assert Hcall : LG.L.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrfile_handleF.out_file InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt7 InterpRuntime.start conversion_mem F.worldtrue
split ; exact Hcall |
destruct T.query_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False 1024 2048 file_handleF.out_file 5120 0 _ _ _ _ _ _ _ _ _ _ _ heap or_introreq_refl Hcall heap_agrees E.disjoint E.ready as Ha & _ & _ & Hw
–auto
Erasing a life is not erasing caller ownership of the FILE's bytes or auxiliary slots. Either kind still excludes a private root.
264Example private_byte_rejected: ∀m h v, h !! PByte1024 0 = Somev → live_atm 1024 mkRegion1024 1056 GlobalData Live → ¬roots_apartmkSpanmkPtr1024 Obj1024 1 stream_data_heap1024 2048 h m
Explore proof 13 tactics
Initial goal
intros m h v Hl Hlive Hr
apply HrmkSpanmkPtr1024 Obj1024 1 1024
3 openm :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
focused goal
m :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
focused goal
m :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
⊢
owned_livestream_data_heap1024 2048 h m 1024
–left
3 openm :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
deferred goal
m :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
deferred goal
m :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
⊢
owned_livestream_data_heap1024 2048 h m 1024
reflexivity
2 opendeferred goal
m :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
deferred goal
m :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
⊢
owned_livestream_data_heap1024 2048 h m 1024
–unfold span_contains
2 openm :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
deferred goal
m :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
⊢
owned_livestream_data_heap1024 2048 h m 1024
simpl
2 openm :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
⊢
1024 ≤ 1024 < 1024 + 1
deferred goal
m :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
⊢
owned_livestream_data_heap1024 2048 h m 1024
lia
deferred goal
m :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
⊢
owned_livestream_data_heap1024 2048 h m 1024
–exists PByte1024 0, v, mkRegion1024 1056 GlobalData Live
m :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
split ; rewrite stream_data_lookup_ne ; congruence |
m :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
split ; exact I |
m :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
split ; exact Hlive |
m :
v :
Hl :
h !! PByte1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
simpl
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m h v Hl Hlive Hr
–left
reflexivity
–exists PByte1024 0, v, mkRegion1024 1056 GlobalData Live
split ; rewrite stream_data_lookup_ne ; congruence |
split ; exact I |
split ; exact Hlive |
simpl
lia
276Example private_aux_rejected: ∀m h v, h !! PAux1024 0 = Somev → live_atm 1024 mkRegion1024 1056 GlobalData Live → ¬roots_apartmkSpanmkPtr1024 Obj1024 1 stream_data_heap1024 2048 h m
Explore proof 13 tactics
Initial goal
intros m h v Hl Hlive Hr
apply HrmkSpanmkPtr1024 Obj1024 1 1024
3 openm :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
focused goal
m :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
focused goal
m :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
⊢
owned_livestream_data_heap1024 2048 h m 1024
–left
3 openm :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
deferred goal
m :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
deferred goal
m :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
⊢
owned_livestream_data_heap1024 2048 h m 1024
reflexivity
2 opendeferred goal
m :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
deferred goal
m :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
⊢
owned_livestream_data_heap1024 2048 h m 1024
–unfold span_contains
2 openm :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
deferred goal
m :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
⊢
owned_livestream_data_heap1024 2048 h m 1024
simpl
2 openm :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
⊢
1024 ≤ 1024 < 1024 + 1
deferred goal
m :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
⊢
owned_livestream_data_heap1024 2048 h m 1024
lia
deferred goal
m :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
⊢
owned_livestream_data_heap1024 2048 h m 1024
–exists PAux1024 0, v, mkRegion1024 1056 GlobalData Live
m :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
split ; rewrite stream_data_lookup_ne ; congruence |
m :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
split ; exact I |
m :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
split ; exact Hlive |
m :
v :
Hl :
h !! PAux1024 0 = Somev
Hr :
roots_apartspan_ptr ≔ ptr_addr ≔ 1024; ptr_cap ≔ Obj1024; span_size ≔ 1 stream_data_heap1024 2048 h m
simpl
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m h v Hl Hlive Hr
–left
reflexivity
–exists PAux1024 0, v, mkRegion1024 1056 GlobalData Live
split ; rewrite stream_data_lookup_ne ; congruence |
split ; exact I |
split ; exact Hlive |
simpl
lia