rocq/theories/LibcErrnoLogic.v
Selected FILE calls with program-owned errno bytes. Private FILE storage remains separate; only the four scalar bytes are handed to close. Query frames restore those bytes without a ghost update.
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 MemLogic LentLogic LocaleLogic LibcStreamLogic HelloClose
Open Scope Z_scope
Open Scope list_scope
∀ m b o
byte_psb o errno_bytesm b o.*1 = errno_keysb o
Explore proof 4 tactics
Initial goal
⊢
∀m : mem b o : Z, byte_psb o errno_bytesm b o.*1 = errno_keysb o
intros
m :
b, o :
Z
⊢
byte_psb o errno_bytesm b o.*1 = errno_keysb o
unfold errno_keys , errno_bytes
rewrite ! byte_ps_keys length_map length_seq
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 22 tactics
Initial goal
⊢
∀m : mem b o : Z, errno_cellm ptr_addr ≔ b + o; ptr_cap ≔ Objb → all_agreem byte_psb o errno_bytesm b o
intros m b o _ & _ & base & reg & Hcap & E & L & Haccess & _
⊢
all_agreem byte_psb o errno_bytesm b o
injection Hcap as ←
⊢
all_agreem byte_psb o errno_bytesm b o
destruct access_regionm b + o Objb b 4 Write 1 or_introleq_refl Haccess as reg0 & E0 & Hlo & Hhi
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
reg0 :
E0 :
object_regionb m_regionsm = Somereg0
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg0
⊢
all_agreem byte_psb o errno_bytesm b o
rewrite E in E0
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
reg0 :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg0
E0 :
Somereg = Somereg0
⊢
all_agreem byte_psb o errno_bytesm b o
injection E0 as ←
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
⊢
all_agreem byte_psb o errno_bytesm b o
apply all_agree_intro
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
⊢
∀l : piece v : pval, l, v ∈ byte_psb o errno_bytesm b o → agree_piecem l v
intros l v Hin
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
l :
v :
Hin :
l, v ∈ byte_psb o errno_bytesm b o
⊢
agree_piecem l v
destruct byte_ps_elem_ _ _ _ _ Hin as i & x & Hxi & → & →
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
errno_bytesm b o !! i = Somex
⊢
agree_piecem PByteb o + i VBytex
assert Hi : i < 4%nat
2 openm :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
errno_bytesm b o !! i = Somex
⊢
i < 4%nat
focused goal
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
errno_bytesm b o !! i = Somex
Hi :
i < 4%nat
⊢
agree_piecem PByteb o + i VBytex
{apply lookup_lt_Some in Hxi
2 openm :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
i < lengtherrno_bytesm b o%nat
⊢
i < 4%nat
deferred goal
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
errno_bytesm b o !! i = Somex
Hi :
i < 4%nat
⊢
agree_piecem PByteb o + i VBytex
unfold errno_bytes in Hxi
2 openm :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
i < lengthmapλi : nat ⇒ m_bytesm b + o + i seq0 4%nat
⊢
i < 4%nat
deferred goal
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
errno_bytesm b o !! i = Somex
Hi :
i < 4%nat
⊢
agree_piecem PByteb o + i VBytex
rewrite length_map length_seq in Hxi
2 openm :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
i < 4%nat
⊢
i < 4%nat
deferred goal
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
errno_bytesm b o !! i = Somex
Hi :
i < 4%nat
⊢
agree_piecem PByteb o + i VBytex
exact Hxi
deferred goal
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
errno_bytesm b o !! i = Somex
Hi :
i < 4%nat
⊢
agree_piecem PByteb o + i VBytex
assert Hx : x = m_bytesm b + o + Z.of_nati
2 openm :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
errno_bytesm b o !! i = Somex
Hi :
i < 4%nat
⊢
x = m_bytesm b + o + i
focused goal
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
errno_bytesm b o !! i = Somex
Hi :
i < 4%nat
Hx :
x = m_bytesm b + o + i
⊢
agree_piecem PByteb o + i VBytex
{destruct i as | | | | i ; try lia ; injection Hxi as ← ; reflexivity
deferred goal
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
errno_bytesm b o !! i = Somex
Hi :
i < 4%nat
Hx :
x = m_bytesm b + o + i
⊢
agree_piecem PByteb o + i VBytex
cbn [ agree_piece ]
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
errno_bytesm b o !! i = Somex
Hi :
i < 4%nat
Hx :
x = m_bytesm b + o + i
⊢
registeredm b ∧ in_livem b o + i m_bytesm b + o + i = x
split ; unfold registered ; congruence |
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
errno_bytesm b o !! i = Somex
Hi :
i < 4%nat
Hx :
x = m_bytesm b + o + i
intros reg′ E′ _
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
errno_bytesm b o !! i = Somex
Hi :
i < 4%nat
Hx :
x = m_bytesm b + o + i
reg′ :
E′ :
object_regionb m_regionsm = Somereg′
rewrite E in E′
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
errno_bytesm b o !! i = Somex
Hi :
i < 4%nat
Hx :
x = m_bytesm b + o + i
reg′ :
E′ :
Somereg = Somereg′
injection E′ as ←
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
errno_bytesm b o !! i = Somex
Hi :
i < 4%nat
Hx :
x = m_bytesm b + o + i
split ; lia |
m :
b, o :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Haccess :
Hlo :
b ≤ b + o
Hhi :
b + o + 4 ≤ r_endreg
i :
nat
x :
Z
Hin :
PByteb o + i, VBytex ∈ byte_psb o errno_bytesm b o
Hxi :
errno_bytesm b o !! i = Somex
Hi :
i < 4%nat
Hx :
x = m_bytesm b + o + i
split ; lia | symmetry ; exact Hx
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m b o _ & _ & base & reg & Hcap & E & L & Haccess & _
injection Hcap as ←
destruct access_regionm b + o Objb b 4 Write 1 or_introleq_refl Haccess as reg0 & E0 & Hlo & Hhi
rewrite E in E0
injection E0 as ←
apply all_agree_intro
intros l v Hin
destruct byte_ps_elem_ _ _ _ _ Hin as i & x & Hxi & → & →
assert Hi : i < 4%nat
assert Hx : x = m_bytesm b + o + Z.of_nati
{destruct i as | | | | i ; try lia ; injection Hxi as ← ; reflexivity
cbn [ agree_piece ]
split ; unfold registered ; congruence |
intros reg′ E′ _
rewrite E in E′
injection E′ as ←
split ; lia |
split ; lia | symmetry ; exact Hx
Other byte/aux pieces must not alias the four handed-over bytes. In particular no errno aux slot is handed over. FILE roots and release identities remain private, even though errno is owned.
libc_stream_readyrep m w ∧ libc_errnofstw = mkPtrb + o 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
∀ p b o m w h
libc_errnofstw = mkPtrb + o Objb
Explore proof 8 tactics
Initial goal
⊢
∀p : ptr b o : Z m : mem w : libc_payload × shutdown_state h : gmappiece pval, libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb → roots_apartlibc_stream_aux_rootsw p h m → roots_outlibc_stream_writesw p h m span_containserrno_spanb o
intros p b o m w h He Hr root a Hin Hspan Hown
p :
b, o :
Z
m :
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hr :
root :
a :
Z
Hin :
Inroot libc_stream_writesw p
Hspan :
span_containsroot a
Hown :
owned_liveh m a
⊢
unfold libc_stream_writes in Hin
p :
b, o :
Z
m :
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hr :
root :
a :
Z
Hin :
Inroot
None
⇒
[ ]
Hspan :
span_containsroot a
Hown :
owned_liveh m a
⊢
destruct libc_file_atw p as file | eqn: Hfile ; | contradiction
p :
b, o :
Z
m :
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hr :
root :
a :
Z
file :
Hfile :
libc_file_atw p = Somefile
Hin :
Inroot file_rootsfile ++ span_ptr ≔ libc_errnow.1; span_size ≔ 4
Hspan :
span_containsroot a
Hown :
owned_liveh m a
⊢
apply in_app_or in Hin as [ Hin | [ <-| [ ] ] ]
2 openp :
b, o :
Z
m :
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hr :
root :
a :
Z
file :
Hfile :
libc_file_atw p = Somefile
Hin :
Inroot file_rootsfile
Hspan :
span_containsroot a
Hown :
owned_liveh m a
⊢
focused goal
p :
b, o :
Z
m :
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hr :
a :
Z
file :
Hfile :
libc_file_atw p = Somefile
Hspan :
span_containsspan_ptr ≔ libc_errnow.1; span_size ≔ 4 a
Hown :
owned_liveh m a
⊢
–exfalso
2 openp :
b, o :
Z
m :
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hr :
root :
a :
Z
file :
Hfile :
libc_file_atw p = Somefile
Hin :
Inroot file_rootsfile
Hspan :
span_containsroot a
Hown :
owned_liveh m a
⊢
False
deferred goal
p :
b, o :
Z
m :
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hr :
a :
Z
file :
Hfile :
libc_file_atw p = Somefile
Hspan :
span_containsspan_ptr ≔ libc_errnow.1; span_size ≔ 4 a
Hown :
owned_liveh m a
⊢
apply Hrroot a ; unfold libc_stream_aux_roots ; rewrite Hfile ; exact Hin | assumption | assumption
deferred goal
p :
b, o :
Z
m :
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hr :
a :
Z
file :
Hfile :
libc_file_atw p = Somefile
Hspan :
span_containsspan_ptr ≔ libc_errnow.1; span_size ≔ 4 a
Hown :
owned_liveh m a
⊢
–rewrite He in Hspan
p :
b, o :
Z
m :
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hr :
a :
Z
file :
Hfile :
libc_file_atw p = Somefile
Hown :
owned_liveh m a
⊢
exact Hspan
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros p b o m w h He Hr root a Hin Hspan Hown
unfold libc_stream_writes in Hin
destruct libc_file_atw p as file | eqn: Hfile ; | contradiction
apply in_app_or in Hin as [ Hin | [ <-| [ ] ] ]
–exfalso
apply Hrroot a ; unfold libc_stream_aux_roots ; rewrite Hfile ; exact Hin | assumption | assumption
–rewrite He in Hspan
exact Hspan
An old registered object's live endpoint is its old region: an effects path cannot resurrect or replace the identity.
Explore proof 9 tactics
Initial goal
intros m m′ b reg Hp Hreg E L
⊢
live_atm b reg
unfold registered in Hreg
m, m′ :
b :
Z
reg :
Hp :
persistsm m′
Hreg :
object_regionb m_regionsm ≠ None
E :
object_regionb m_regionsm′ = Somereg
⊢
live_atm b reg
destruct object_regionb m_regionsm as old | eqn: E0 ; | contradiction
destruct Hpb old E0 as E′ | E′ ; rewrite E in E' ; injection E' as Hsame
2 openm, m′ :
b :
Z
reg :
Hp :
persistsm m′
old :
E0 :
object_regionb m_regionsm = Someold
Hreg :
Someold ≠ None
E :
object_regionb m_regionsm′ = Somereg
Hsame :
reg = old
⊢
live_atm b reg
focused goal
m, m′ :
b :
Z
reg :
Hp :
persistsm m′
old :
E0 :
object_regionb m_regionsm = Someold
Hreg :
Someold ≠ None
E :
object_regionb m_regionsm′ = Somereg
Hsame :
reg = freed_regionold
⊢
live_atm b reg
–subst old
2 openm, m′ :
b :
Z
reg :
Hp :
persistsm m′
Hreg :
Somereg ≠ None
E0 :
object_regionb m_regionsm = Somereg
E :
object_regionb m_regionsm′ = Somereg
⊢
live_atm b reg
deferred goal
m, m′ :
b :
Z
reg :
Hp :
persistsm m′
old :
E0 :
object_regionb m_regionsm = Someold
Hreg :
Someold ≠ None
E :
object_regionb m_regionsm′ = Somereg
Hsame :
reg = freed_regionold
⊢
live_atm b reg
split ; assumption
deferred goal
m, m′ :
b :
Z
reg :
Hp :
persistsm m′
old :
E0 :
object_regionb m_regionsm = Someold
Hreg :
Someold ≠ None
E :
object_regionb m_regionsm′ = Somereg
Hsame :
reg = freed_regionold
⊢
live_atm b reg
–apply f_equalr_life in Hsame
m, m′ :
b :
Z
reg :
Hp :
persistsm m′
old :
E0 :
object_regionb m_regionsm = Someold
Hreg :
Someold ≠ None
E :
object_regionb m_regionsm′ = Somereg
Hsame :
r_lifereg = r_lifefreed_regionold
⊢
live_atm b reg
cbn [ freed_region r_life ] in Hsame
congruence
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m m′ b reg Hp Hreg E L
unfold registered in Hreg
destruct object_regionb m_regionsm as old | eqn: E0 ; | contradiction
destruct Hpb old E0 as E′ | E′ ; rewrite E in E' ; injection E' as Hsame
–subst old
split ; assumption
A ghost update may replace values of existing memory keys, but cannot introduce a new program-owned object identity.
∀l v, h′ !! l = Somev → mem_piecel → ∃old, h !! l = Someold
Separation depends on memory keys, not their stored ghost values. This transports it across sampled errno and stream-name updates.
Explore proof 15 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop p : ptr b o : Z m : mem w : libc_world h h′ : gmappiece pval, libc_errno_wirep p b o m w h → memory_keys_fromh′ h → libc_errno_wirep p b o m w h′
intros rep p b o m w h h′ Hr & He & Hroots & Hrelease & Hoff Hkeys
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
⊢
libc_errno_wirep p b o m w h′
split ; exact Hr |
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
⊢
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
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
⊢
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
3 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
⊢
roots_apartlibc_stream_aux_rootsw p h′ m
focused goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
focused goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
⊢
pieces_offerrno_keysb o h′ m span_containserrno_spanb o
–intros root a Hin Hspan l & v & reg & Hl & Hmem & Hlive & Hrange
3 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h′ !! l = Somev
Hmem :
⊢
False
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
⊢
pieces_offerrno_keysb o h′ m span_containserrno_spanb o
destruct Hkeysl v Hl Hmem as old Hold
3 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h′ !! l = Somev
Hmem :
old :
Hold :
h !! l = Someold
⊢
False
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
⊢
pieces_offerrno_keysb o h′ m span_containserrno_spanb o
apply Hrootsroot a Hin Hspan
3 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h′ !! l = Somev
Hmem :
old :
Hold :
h !! l = Someold
⊢
owned_liveh m a
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
⊢
pieces_offerrno_keysb o h′ m span_containserrno_spanb o
exists l, old, reg
3 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h′ !! l = Somev
Hmem :
old :
Hold :
h !! l = Someold
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
⊢
pieces_offerrno_keysb o h′ m span_containserrno_spanb o
exact conjHold conjHmem conjHlive Hrange
2 opendeferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
⊢
pieces_offerrno_keysb o h′ m span_containserrno_spanb o
–intros base l v Hin Hl Hmem
2 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
base :
Z
l :
v :
Hin :
Inbase libc_stream_releasesw p
Hl :
h′ !! l = Somev
Hmem :
⊢
piece_idl ≠ base
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
⊢
pieces_offerrno_keysb o h′ m span_containserrno_spanb o
destruct Hkeysl v Hl Hmem as old Hold
2 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
base :
Z
l :
v :
Hin :
Inbase libc_stream_releasesw p
Hl :
h′ !! l = Somev
Hmem :
old :
Hold :
h !! l = Someold
⊢
piece_idl ≠ base
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
⊢
pieces_offerrno_keysb o h′ m span_containserrno_spanb o
exact Hreleasebase l old Hin Hold Hmem
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
⊢
pieces_offerrno_keysb o h′ m span_containserrno_spanb o
–intros l v Hl Hnot
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
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
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
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
m :
w :
Hr :
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
Hkeys :
memory_keys_fromh′ h
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: destruct Hkeys_ _ Hl I as old Hold ; exact Hoff_ old Hold Hnot
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep p b o m w h h′ Hr & He & Hroots & Hrelease & Hoff Hkeys
split ; exact Hr |
split ; exact He |
split ; | split
–intros root a Hin Hspan l & v & reg & Hl & Hmem & Hlive & Hrange
destruct Hkeysl v Hl Hmem as old Hold
apply Hrootsroot a Hin Hspan
exists l, old, reg
exact conjHold conjHmem conjHlive Hrange
–intros base l v Hin Hl Hmem
destruct Hkeysl v Hl Hmem as old Hold
exact Hreleasebase l old Hin Hold Hmem
–intros l v Hl Hnot
destruct l as base | base off | base off | key ; try exact I
all: destruct Hkeys_ _ Hl I as old Hold ; exact Hoff_ old Hold Hnot
∀ rep requests wide p b o m w born m′ w′ h h′
libc_errno_wirep p b o m w h
agreesm h
persistsm m′
libc_stream_readyrep m′ w′
libc_errnofstw′ = libc_errnofstw
stream_delegateslibc_stream_modelrep requests wide w p born m′ w′
ids_apartborn h
memory_keys_fromh′ h
libc_errno_wirep p b o m′ w′ h′
Proof 50 steps Qed
intros rep requests wide p b o m w born m′ w′ h h′ Hready & He & Hroots & Hrel & Hoff Ha Hp Hd Hready′ Herrno Hdelegate & _ & Hrelease Hb Hkeys
assert He′ : libc_errnofstw' = mkPtrb + o Objb
{rewrite Herrno
exact He
assert Hown : ∀a, owned_liveh' m' a → owned_liveh m a ∧ owned_liveh m' a
{intros a l & v & reg & Hl & Hmem & Hlive & Hrange
assert Hreg : registeredm piece_idl by eapply agree_piece_registered ; exact Hmem | exact Hal old Hold
split
split ; exact Hready' |
split ; exact He' |
split ; | split
–intros root a Hroot Hspan Howned
destruct Howna Howned as Hentry Hend
unfold libc_stream_aux_roots in Hroot
destruct libc_file_atw' p as file | eqn: Hfile ; | contradiction
destruct libc_file_at_readyrep m' w' p file Hready' Hfile as _ & _ & _ & _ & _ & _ & Hapart & _
assert Hnoterrno : ¬span_containserrno_spanb o a
{specialize Hapartroot Hroot
rewrite He' in Hapart
unfold spans_apart , span_contains , errno_span in *
simpl in *
lia
assert Hin : Inroot libc_stream_writesw' p
destruct Hautha Hspan as old & Hold & _ & Haold | Hborn
+change Inold libc_stream_writesw p in Hold
unfold libc_stream_writes in Hold
destruct libc_file_atw p as oldfile | eqn: Holdfile ; | contradiction
apply in_app_or in Hold as [ Hold | [ <-| [ ] ] ]
∗apply Hrootsold a ; unfold libc_stream_aux_roots ; rewrite Holdfile ; exact Hold | assumption | assumption
∗apply Hnoterrno
rewrite He in Haold
exact Haold
+exact owned_not_authority[ ] born h m' a Hd λroot a Hnil ⇒ match Hnil with end Hb Hend or_introrHborn
–intros base l v Hin Hl Hmem
–intros l v Hl Hnot
destruct l as base | base off | base off | key ; try exact I
all: intros reg E L Ho Hend Hout ; destruct Hkeys_ _ Hl I as old Hold ; pose proof Ha_ old Hold as Hreg ; apply agree_piece_registered in Hreg ; | exact I ; destruct registered_live_backm m' base reg Hp Hreg conjE L as E0 L0 ; exact Hoff_ old Hold Hnot reg conjE0 L0 Ho Hend Hout
The unselected FILE keeps its inventory. Its private frame transports through old-object persistence even when the selected FILE writes.
∀ rep p b o m w m′ w′ h
libc_errno_wirep p b o m w h
agreesm h
persistsm m′
libc_stream_readyrep m′ w′
libc_errnofstw′ = libc_errnofstw
libc_stream_releasesw′ p = libc_stream_releasesw p
libc_errno_wirep p b o m′ w′ h
Explore proof 18 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop p : ptr b o : Z m : mem w : libc_world m′ : mem w′ : libc_world h : gmappiece pval, libc_errno_wirep p b o m w h → agreesm h → persistsm m′ → libc_stream_readyrep m′ w′ → libc_errnow′.1 = libc_errnow.1 → libc_stream_aux_rootsw′ p = libc_stream_aux_rootsw p → libc_stream_releasesw′ p = libc_stream_releasesw p → libc_errno_wirep p b o m′ w′ h
intros rep p b o m w m′ w′ h Hready & He & Hroots & Hrelease & Hoff Ha Hp Hready′ He′ Hroots′ Hrelease′
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
libc_errno_wirep p b o m′ w′ h
split ; exact Hready′ |
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
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 ; congruence |
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
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
3 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
roots_apartlibc_stream_aux_rootsw′ p h m′
focused goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
focused goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
–rewrite Hroots′
3 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
roots_apartlibc_stream_aux_rootsw p h m′
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
intros root a Hin Hspan l & v & reg & Hl & Hmem & Hlive & Hrange
3 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
⊢
False
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
apply Hrootsroot a Hin Hspan
3 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
⊢
owned_liveh m a
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
exists l, v, reg
3 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
split ; exact Hl |
3 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
split ; exact Hmem |
3 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
split ; | exact Hrange
3 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
eapply registered_live_back ; exact Hp | | exact Hlive
3 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
root :
a :
Z
Hin :
Inroot libc_stream_aux_rootsw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
eapply agree_piece_registered ; exact Hmem | exact Hal v Hl
2 opendeferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
–rewrite Hrelease′
2 openrep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
exact Hrelease
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
⊢
pieces_offerrno_keysb o h m′ span_containserrno_spanb o
–intros l v Hl Hnot
rep :
mem → libc_world → Prop
p :
b, o :
Z
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
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
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
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
m :
w :
m′ :
w′ :
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
Ha :
agreesm h
Hp :
persistsm m′
Hready′ :
libc_stream_readyrep m′ w′
He′ :
libc_errnow′.1 = libc_errnow.1
Hroots′ :
Hrelease′ :
libc_stream_releasesw′ p = libc_stream_releasesw p
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 Hlive Ho Hend Hout ; apply Hoff_ v Hl Hnot reg ; | exact Ho | exact Hend | exact Hout ; pose proof Ha_ v Hl as Hreg ; apply agree_piece_registered in Hreg ; | exact I ; eapply registered_live_back ; exact Hp | | exact Hlive ; exact Hreg
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep p b o m w m′ w′ h Hready & He & Hroots & Hrelease & Hoff Ha Hp Hready′ He′ Hroots′ Hrelease′
split ; exact Hready′ |
split ; congruence |
split ; | split
–rewrite Hroots′
intros root a Hin Hspan l & v & reg & Hl & Hmem & Hlive & Hrange
apply Hrootsroot a Hin Hspan
exists l, v, reg
split ; exact Hl |
split ; exact Hmem |
split ; | exact Hrange
eapply registered_live_back ; exact Hp | | exact Hlive
eapply agree_piece_registered ; exact Hmem | exact Hal v Hl
–rewrite Hrelease′
exact Hrelease
–intros l v Hl Hnot
destruct l as base | base off | base off | key ; try exact I
all: intros reg Hlive Ho Hend Hout ; apply Hoff_ v Hl Hnot reg ; | exact Ho | exact Hend | exact Hout ; pose proof Ha_ v Hl as Hreg ; apply agree_piece_registered in Hreg ; | exact I ; eapply registered_live_back ; exact Hp | | exact Hlive ; exact Hreg
Explore proof 2 tactics
Initial goal
intros ps
induction ps as | l v ps IH ; intros qs h ; simpl ; reflexivity | rewrite IH ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros ps
induction ps as | l v ps IH ; intros qs h ; simpl ; reflexivity | rewrite IH ; reflexivity
This frame accepts owned errno, unlike the all-roots-apart frame. It applies to finite prefixes, not just successful close results.
∀ rep p b o spec xs s m w born trace s′ m′ w′ h
M.E.prefixspec xs s m w born trace s′ m′ w′
contract_writesspec xs m w = libc_stream_writesw p
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
agreesm h
R.readys m
libc_errno_wirep p b o m w h
agrees_excepterrno_keysb o m′ h ∧ LG.ids_registeredh m′ ∧ live_disjointm′ ∧ ids_apartborn h ∧ R.readys′ m′ ∧ persistsm m′
Explore proof 12 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop p : ptr b o : Z spec : contractlibc_world xs : listword s : R.state m : mem w : libc_world born : listZ trace : listevent s′ : R.state m′ : mem w′ : libc_world h : gmappiece pval, M.E.prefixspec xs s m w born trace s′ m′ w′ → contract_writesspec xs m w = libc_stream_writesw p → contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p → agreesm h → live_disjointm → R.readys m → libc_errno_wirep p b o m w h → agrees_excepterrno_keysb o m′ h ∧ LG.ids_registeredh m′ ∧ live_disjointm′ ∧ ids_apartborn h ∧ R.readys′ m′ ∧ persistsm m′
intros rep p b o spec xs s m w born trace s′ m′ w′ h Hp Hw Hrelease Ha Hd Hr Hready & He & Hroots & Hrel & Hoff
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
agrees_excepterrno_keysb o m′ h ∧ LG.ids_registeredh m′ ∧ live_disjointm′ ∧ ids_apartborn h ∧ R.readys′ m′ ∧ persistsm m′
destruct LG.prefix_agrees_out_ _ _ _ _ _ _ _ _ _ _ h errno_keysb o span_containserrno_spanb o Hp Hr Hd as Ha′ & Hids′ & Hd′ & Hb
6 openrep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
agrees_excepterrno_keysb o m h
focused goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
focused goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
roots_outcontract_writesspec xs m w h m span_containserrno_spanb o
focused goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m span_containserrno_spanb o
focused goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
ids_apartcontract_releasesspec xs m w h
focused goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
Ha′ :
agrees_excepterrno_keysb o m′ h
Hids′ :
Hd′ :
Hb :
ids_apartborn h
⊢
agrees_excepterrno_keysb o m′ h ∧ LG.ids_registeredh m′ ∧ live_disjointm′ ∧ ids_apartborn h ∧ R.readys′ m′ ∧ persistsm m′
–intros l v Hl _
6 openrep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
l :
v :
Hl :
h !! l = Somev
⊢
agree_piecem l v
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
roots_outcontract_writesspec xs m w h m span_containserrno_spanb o
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m span_containserrno_spanb o
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
ids_apartcontract_releasesspec xs m w h
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
Ha′ :
agrees_excepterrno_keysb o m′ h
Hids′ :
Hd′ :
Hb :
ids_apartborn h
⊢
agrees_excepterrno_keysb o m′ h ∧ LG.ids_registeredh m′ ∧ live_disjointm′ ∧ ids_apartborn h ∧ R.readys′ m′ ∧ persistsm m′
exact Hal v Hl
5 opendeferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
roots_outcontract_writesspec xs m w h m span_containserrno_spanb o
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m span_containserrno_spanb o
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
ids_apartcontract_releasesspec xs m w h
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
Ha′ :
agrees_excepterrno_keysb o m′ h
Hids′ :
Hd′ :
Hb :
ids_apartborn h
⊢
agrees_excepterrno_keysb o m′ h ∧ LG.ids_registeredh m′ ∧ live_disjointm′ ∧ ids_apartborn h ∧ R.readys′ m′ ∧ persistsm m′
–intros l v Hl Hmem
5 openrep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
l :
v :
Hl :
h !! l = Somev
Hmem :
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
roots_outcontract_writesspec xs m w h m span_containserrno_spanb o
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m span_containserrno_spanb o
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
ids_apartcontract_releasesspec xs m w h
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
Ha′ :
agrees_excepterrno_keysb o m′ h
Hids′ :
Hd′ :
Hb :
ids_apartborn h
⊢
agrees_excepterrno_keysb o m′ h ∧ LG.ids_registeredh m′ ∧ live_disjointm′ ∧ ids_apartborn h ∧ R.readys′ m′ ∧ persistsm m′
eapply agree_piece_registered ; exact Hmem | exact Hal v Hl
4 opendeferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
roots_outcontract_writesspec xs m w h m span_containserrno_spanb o
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m span_containserrno_spanb o
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
ids_apartcontract_releasesspec xs m w h
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
Ha′ :
agrees_excepterrno_keysb o m′ h
Hids′ :
Hd′ :
Hb :
ids_apartborn h
⊢
agrees_excepterrno_keysb o m′ h ∧ LG.ids_registeredh m′ ∧ live_disjointm′ ∧ ids_apartborn h ∧ R.readys′ m′ ∧ persistsm m′
–rewrite Hw
4 openrep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m span_containserrno_spanb o
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
ids_apartcontract_releasesspec xs m w h
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
Ha′ :
agrees_excepterrno_keysb o m′ h
Hids′ :
Hd′ :
Hb :
ids_apartborn h
⊢
agrees_excepterrno_keysb o m′ h ∧ LG.ids_registeredh m′ ∧ live_disjointm′ ∧ ids_apartborn h ∧ R.readys′ m′ ∧ persistsm m′
eapply errno_roots_out ; eauto
3 opendeferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
pieces_offerrno_keysb o h m span_containserrno_spanb o
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
ids_apartcontract_releasesspec xs m w h
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
Ha′ :
agrees_excepterrno_keysb o m′ h
Hids′ :
Hd′ :
Hb :
ids_apartborn h
⊢
agrees_excepterrno_keysb o m′ h ∧ LG.ids_registeredh m′ ∧ live_disjointm′ ∧ ids_apartborn h ∧ R.readys′ m′ ∧ persistsm m′
–exact Hoff
2 opendeferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
⊢
ids_apartcontract_releasesspec xs m w h
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
Ha′ :
agrees_excepterrno_keysb o m′ h
Hids′ :
Hd′ :
Hb :
ids_apartborn h
⊢
agrees_excepterrno_keysb o m′ h ∧ LG.ids_registeredh m′ ∧ live_disjointm′ ∧ ids_apartborn h ∧ R.readys′ m′ ∧ persistsm m′
–destruct Hrelease as → | → ; intros base l v | exact Hrel
deferred goal
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
Ha′ :
agrees_excepterrno_keysb o m′ h
Hids′ :
Hd′ :
Hb :
ids_apartborn h
⊢
agrees_excepterrno_keysb o m′ h ∧ LG.ids_registeredh m′ ∧ live_disjointm′ ∧ ids_apartborn h ∧ R.readys′ m′ ∧ persistsm m′
–destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as Hr′ Hpers
rep :
mem → libc_world → Prop
p :
b, o :
Z
spec :
xs :
listword
s :
R.state
m :
w :
born :
listZ
trace :
listevent
s′ :
R.state
m′ :
w′ :
Hp :
M.E.prefixspec xs s m w born trace s′ m′ w′
Hw :
contract_writesspec xs m w = libc_stream_writesw p
Hrelease :
contract_releasesspec xs m w = [ ] ∨ contract_releasesspec xs m w = libc_stream_releasesw p
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
He :
libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb
Hroots :
Hrel :
Hoff :
pieces_offerrno_keysb o h m span_containserrno_spanb o
Ha′ :
agrees_excepterrno_keysb o m′ h
Hids′ :
Hd′ :
Hb :
ids_apartborn h
Hr′ :
R.readys′ m′
Hpers :
persistsm m′
⊢
agrees_excepterrno_keysb o m′ h ∧ LG.ids_registeredh m′ ∧ live_disjointm′ ∧ ids_apartborn h ∧ R.readys′ m′ ∧ persistsm m′
exact conjHa′ conjHids′ conjHd′ conjHb conjHr′ Hpers
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep p b o spec xs s m w born trace s′ m′ w′ h Hp Hw Hrelease Ha Hd Hr Hready & He & Hroots & Hrel & Hoff
destruct LG.prefix_agrees_out_ _ _ _ _ _ _ _ _ _ _ h errno_keysb o span_containserrno_spanb o Hp Hr Hd as Ha′ & Hids′ & Hd′ & Hb
–intros l v Hl _
exact Hal v Hl
–intros l v Hl Hmem
eapply agree_piece_registered ; exact Hmem | exact Hal v Hl
–rewrite Hw
eapply errno_roots_out ; eauto
–exact Hoff
–destruct Hrelease as → | → ; intros base l v | exact Hrel
–destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as Hr′ Hpers
exact conjHa′ conjHids′ conjHd′ conjHb conjHr′ Hpers
The query's byte frame restores its original owned errno pieces. The rest of the heap was already preserved by the effects frame.
∀ rep requests wide 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 h
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′
Explore proof 4 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop 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 h → agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′
intros rep requests wide 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
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 h
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′
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
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 h
born :
listZ
Hp :
M.E.prefixspec WPtrp s m w born trace s′ m′ w′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′
destruct Hspec as → | →
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
p :
b, o :
Z
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokeferror_contractlibc_stream_modelrep requests wide 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 h
born :
listZ
Hp :
M.E.prefixferror_contractlibc_stream_modelrep requests wide WPtrp s m w born trace s′ m′ w′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′
focused goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
p :
b, o :
Z
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokefpending_contractlibc_stream_modelrep requests wide 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 h
born :
listZ
Hp :
M.E.prefixfpending_contractlibc_stream_modelrep requests wide WPtrp s m w born trace s′ m′ w′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′
all: destruct errno_prefix_framerep p b o _ _ _ _ _ _ _ _ _ _ h Hp eq_refl or_introleq_refl Ha Hd Hr Hwi as Hexcept & Hids & Hd′ & Hb & Hr′ & Hpers ; split ; | auto ; destruct Hwi as Hready & He & Hroots & Hrel & Hoff ; destruct Hp as _ & p0 & info & Hxs & Hinfo & Hopen & Hframe & Hdelegate & Htrace & Haux & Hbytes ; injection Hxs as ← ; intros l v Hl ; destruct decidel ∈ errno_keysb o as Hkey | Hkey ; | exact Hexceptl v Hl Hkey ; unfold errno_keys in Hkey ; rewrite byte_ps_keys in Hkey ; apply list_elem_of_fmap in Hkey as i & → & Hi ; apply elem_of_seqZ in Hi ; pose proof Ha_ _ Hl as Hag ; destruct v ; cbn [ agree_piece ] in Hag |- * ; try contradiction ; destruct Hag as Hreg Hin ; split ; exact Hids_ _ Hl I | ; intros reg E L ; destruct registered_live_backm m′ b reg Hpers Hreg conjE L as E0 L0 ; destruct Hinreg E0 L0 as Ho & Hend & Hval ; split ; exact Ho | ; split ; exact Hend | ; assert Hobject : in_objectm b + i by exists b, reg ; split ; exact E0 | lia ; assert Hown : owned_liveh m b + i by exists PByteb i, VBytev, reg ; repeat split ; try assumption ; simpl ; lia ; assert Houtside : ¬write_authoritylibc_stream_aux_rootsw p [ ] m b + i by eapply owned_not_authority ; exact Hd | exact Hroots | intros base l0 v0 | exact Hown ; rewrite Hbytesb + i Hobject Houtside ; exact Hval
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide p b o spec r args s m w trace ending s′ m′ w′ h Hspec Hcall Ha Hd Hr Hwi
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & Hp
destruct Hspec as → | →
all: destruct errno_prefix_framerep p b o _ _ _ _ _ _ _ _ _ _ h Hp eq_refl or_introleq_refl Ha Hd Hr Hwi as Hexcept & Hids & Hd′ & Hb & Hr′ & Hpers ; split ; | auto ; destruct Hwi as Hready & He & Hroots & Hrel & Hoff ; destruct Hp as _ & p0 & info & Hxs & Hinfo & Hopen & Hframe & Hdelegate & Htrace & Haux & Hbytes ; injection Hxs as ← ; intros l v Hl ; destruct decidel ∈ errno_keysb o as Hkey | Hkey ; | exact Hexceptl v Hl Hkey ; unfold errno_keys in Hkey ; rewrite byte_ps_keys in Hkey ; apply list_elem_of_fmap in Hkey as i & → & Hi ; apply elem_of_seqZ in Hi ; pose proof Ha_ _ Hl as Hag ; destruct v ; cbn [ agree_piece ] in Hag |- * ; try contradiction ; destruct Hag as Hreg Hin ; split ; exact Hids_ _ Hl I | ; intros reg E L ; destruct registered_live_backm m′ b reg Hpers Hreg conjE L as E0 L0 ; destruct Hinreg E0 L0 as Ho & Hend & Hval ; split ; exact Ho | ; split ; exact Hend | ; assert Hobject : in_objectm b + i by exists b, reg ; split ; exact E0 | lia ; assert Hown : owned_liveh m b + i by exists PByteb i, VBytev, reg ; repeat split ; try assumption ; simpl ; lia ; assert Houtside : ¬write_authoritylibc_stream_aux_rootsw p [ ] m b + i by eapply owned_not_authority ; exact Hd | exact Hroots | intros base l0 v0 | exact Hown ; rewrite Hbytesb + i Hobject Houtside ; exact Hval
Both queries re-establish the same owned-errno world interpretation, not merely the result shape or memory agreement.
∀ rep requests wide 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 h
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ h
Explore proof 8 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop p : ptr 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 h → agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ h
intros rep requests wide 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
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 h
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ h
destruct query_agreesrep requests wide p b o spec r args s m w trace ending s′ m′ w′ h Hspec Hcall Ha Hd Hr Hwi as Ha′ & Hd′ & Hr′
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
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 h
Ha′ :
agreesm′ h
Hd′ :
Hr′ :
R.readys′ m′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ h
split ; exact Ha′ |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
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 h
Ha′ :
agreesm′ h
Hd′ :
Hr′ :
R.readys′ m′
⊢
live_disjointm′ ∧ R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ h
split ; exact Hd′ |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
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 h
Ha′ :
agreesm′ h
Hd′ :
Hr′ :
R.readys′ m′
⊢
R.readys′ m′ ∧ libc_errno_wirep p b o m′ w′ h
split ; exact Hr′ |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
p :
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 h
Ha′ :
agreesm′ h
Hd′ :
Hr′ :
R.readys′ m′
⊢
libc_errno_wirep p b o m′ w′ 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
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 h
Ha′ :
agreesm′ h
Hd′ :
Hr′ :
R.readys′ m′
born :
listZ
Hp :
M.E.prefixspec WPtrp s m w born trace s′ m′ w′
⊢
libc_errno_wirep p b o m′ w′ h
destruct Hspec as → | →
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
p :
b, o :
Z
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokeferror_contractlibc_stream_modelrep requests wide 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 h
Ha′ :
agreesm′ h
Hd′ :
Hr′ :
R.readys′ m′
born :
listZ
Hp :
M.E.prefixferror_contractlibc_stream_modelrep requests wide WPtrp s m w born trace s′ m′ w′
⊢
libc_errno_wirep p b o m′ w′ h
focused goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
p :
b, o :
Z
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokefpending_contractlibc_stream_modelrep requests wide 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 h
Ha′ :
agreesm′ h
Hd′ :
Hr′ :
R.readys′ m′
born :
listZ
Hp :
M.E.prefixfpending_contractlibc_stream_modelrep requests wide WPtrp s m w born trace s′ m′ w′
⊢
libc_errno_wirep p b o m′ w′ h
all: destruct errno_prefix_framerep p b o _ _ _ _ _ _ _ _ _ _ h Hp eq_refl or_introleq_refl Ha Hd Hr Hwi as _ & _ & _ & Hb & _ & Hpers ; destruct Hp as _ & p0 & info & Hxs & Hinfo & Hopen & Hframe & Hdelegate & _ ; injection Hxs as ← ; eapply errno_wi_endpoint ; exact Hwi | exact Ha | exact Hpers | exact Hd′ | exact proj1Hopen | exact proj1proj2proj2proj2Hframe | exact Hdelegate | exact Hb | ; intros l v Hl _ ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide p b o spec r args s m w trace ending s′ m′ w′ h Hspec Hcall Ha Hd Hr Hwi
destruct query_agreesrep requests wide p b o spec r args s m w trace ending s′ m′ w′ h Hspec Hcall Ha Hd Hr Hwi as Ha′ & Hd′ & Hr′
split ; exact Ha′ |
split ; exact Hd′ |
split ; exact Hr′ |
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & Hp
destruct Hspec as → | →
all: destruct errno_prefix_framerep p b o _ _ _ _ _ _ _ _ _ _ h Hp eq_refl or_introleq_refl Ha Hd Hr Hwi as _ & _ & _ & Hb & _ & Hpers ; destruct Hp as _ & p0 & info & Hxs & Hinfo & Hopen & Hframe & Hdelegate & _ ; injection Hxs as ← ; eapply errno_wi_endpoint ; exact Hwi | exact Ha | exact Hpers | exact Hd′ | exact proj1Hopen | exact proj1proj2proj2proj2Hframe | exact Hdelegate | exact Hb | ; intros l v Hl _ ; eauto
Close can write owned errno while framing everything else. The bytes returned to the logic are read from the actual final memory; no errno value is guessed from EOF or from a host syscall.
∀ rep requests wide p b o r args s m w trace ending s′ m′ w′ h xs
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 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′ overwritebyte_psb o ys h
Proof 43 steps Qed
intros rep requests wide p b o r args s m w trace ending s′ m′ w′ h xs Hcall Ha Hd Hr Hwi Hlen Howned
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & Hp
destruct errno_prefix_framerep p b o _ _ _ _ _ _ _ _ _ _ h Hp eq_refl or_introreq_refl Ha Hd Hr Hwi as Hexcept & Hids & Hd′ & Hb & Hr′ & Hpers
destruct Hp as _ & p0 & info & final & Hxs & Hinfo & Hsettle & Hstate & Hready & Hframe & Hdelegate & _
injection Hxs as ←
assert He : libc_errnofstw' = mkPtrb + o Objb
{rewrite proj1proj2proj2proj2Hframe
exact proj1proj2Hwi
exists errno_bytesm' b o
split ; unfold errno_bytes ; rewrite length_map length_seq ; reflexivity |
split ; exact Hkeys |
split
–intros l v Hl
destruct lookup_overwrite_ _ _ _ Hl as Hin | Hnot Hold
+exact all_agree_elem_ _ _ _ Hbytes Hin
–split ; exact Hd' |
split ; exact Hr' |
eapply errno_wi_endpoint ; exact Hwi | exact Ha | exact Hpers | exact Hd' | exact Hready | exact proj1proj2proj2proj2Hframe | exact Hdelegate | exact Hb |
intros l v Hl Hmem
destruct lookup_overwrite_ _ _ _ Hl as Hin | _ Hold ; | eauto
apply list_elem_of_fmap in Hkey as l0 old & E & Hinold
simpl in E
subst l0
exists old
apply Howned
exact Hinold
The stream assertion may also change logical values at close. Its memory pieces must remain the same, and its keys must not overlap errno. The supplied replacement law is pure ghost bookkeeping, not an assumption about what the native call did to memory.
∀ rep requests wide p b o r args s m w trace values s′ m′ w′ h xs before after
after.*1 = before.*1
∀l, l ∈ before.*1 → l ∉ errno_keysb o
M.E.invokefclose_contractlibc_stream_modelrep requests wide r args WPtrp s m w trace CallReturnvalues s′ m′ w′
agreesm h
R.readys m
libc_errno_wirep p b o m w h
lengthxs = 4%nat
∀l v, l, v ∈ before ++ byte_psb o xs → h !! l = Somev
Proof 56 steps Qed
intros rep requests wide p b o r args s m w trace values s′ m′ w′ h xs before after Hsame Hapart Hreplace Hcall Ha Hd Hr Hwi Hlen Howned
destruct close_framerep requests wide p b o r args s m w trace CallReturnvalues s' m' w' h xs Hcall Ha Hd Hr Hwi Hlen as ys & Hys & Hkeys & Ha′ & Hd′ & Hr′ & Hwi′
–intros l v Hin
apply Howned , elem_of_app
auto
{intros l v Hin
rewrite overwrite_out ; apply Howned , elem_of_app ; auto |
rewrite Hkeys byte_ps_keys Hlen
change l ∉ errno_keysb o
apply Hapart
apply list_elem_of_fmap
exists l, v
auto
destruct S.fclose_invocation_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & q & info & final & n & Hxs & _ & _ & _ & Hn & _ & _ & _ & _ & _ & Hvalues | why & Hbad & _ ; | discriminate Hbad
injection Hvalues as Hvalues
exists n, ys
split ; exact Hvalues |
split ; destruct Hn as → | → ; unfold stream_eof ; lia |
split ; exact Hys |
split ; rewrite ! fmap_app Hsame Hkeys ; reflexivity |
rewrite overwrite_app
split
+intros l v Hl
destruct lookup_overwrite_ _ _ _ Hl as Hin | _ Hold ; exact all_agree_elem_ _ _ _ Hafter Hin | exact Ha'l v Hold
+split ; exact Hd' |
split ; exact Hr' |
destruct Hwi' as Hready & He & Hroots & Hrel & Hoff
{intros l v Hl _
destruct lookup_overwrite_ _ _ _ Hl as Hin | _ Hold ; | eauto
assert Hkey : l ∈ before.*1
apply list_elem_of_fmap in Hkey as l0 old & E & Hinold
simpl in E
subst l0
exists old
exact Hbeforel old Hinold
split ; exact Hready |
split ; exact He |
split ; | split
∗intros root a Hin Hspan l & v & reg & Hl & Hmem & Hlive & Hrange
exact conjHold conjHmem conjHlive Hrange
∗intros base l v Hin Hl Hmem
Nonvacuity through the actual HelloClose logic instance. This heap really owns errno, so the previous all-write-roots frame rejects it.
∀ b reg
object_regionb m_regionsconversion_mem = Somereg
Explore proof 3 tactics
Initial goal
⊢
∀b : Z reg : region, object_regionb m_regionsconversion_mem = Somereg → b = 1024 ∧ reg = r_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live ∨ b = 2048 ∧ reg = r_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live ∨ b = 3072 ∧ reg = r_base ≔ 3072; r_end ≔ 3080; r_kind ≔ Stack; r_life ≔ Live ∨ b = 4096 ∧ reg = r_base ≔ 4096; r_end ≔ 4104; r_kind ≔ GlobalData; r_life ≔ Live ∨ b = 5120 ∧ reg = r_base ≔ 5120; r_end ≔ 5128; r_kind ≔ Heap; r_life ≔ Live
intros b reg Hreg
⊢
b = 1024 ∧ reg = r_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live ∨ b = 2048 ∧ reg = r_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live ∨ b = 3072 ∧ reg = r_base ≔ 3072; r_end ≔ 3080; r_kind ≔ Stack; r_life ≔ Live ∨ b = 4096 ∧ reg = r_base ≔ 4096; r_end ≔ 4104; r_kind ≔ GlobalData; r_life ≔ Live ∨ b = 5120 ∧ reg = r_base ≔ 5120; r_end ≔ 5128; r_kind ≔ Heap; r_life ≔ Live
cbn [ conversion_mem m_regions object_region r_base ] in Hreg
b :
Z
reg :
Hreg :
else
None
=
Somereg
⊢
b = 1024 ∧ reg = r_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live ∨ b = 2048 ∧ reg = r_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live ∨ b = 3072 ∧ reg = r_base ≔ 3072; r_end ≔ 3080; r_kind ≔ Stack; r_life ≔ Live ∨ b = 4096 ∧ reg = r_base ≔ 4096; r_end ≔ 4104; r_kind ≔ GlobalData; r_life ≔ Live ∨ b = 5120 ∧ reg = r_base ≔ 5120; r_end ≔ 5128; r_kind ≔ Heap; r_life ≔ Live
repeat destruct _ =? _ eqn :? in Hreg ; try discriminate ; injection Hreg as ←;repeat match goal withH : _ =? _ = true |- _⇒apply Z.eqb_eq in Hend;subst;auto 10
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros b reg Hreg
cbn [ conversion_mem m_regions object_region r_base ] in Hreg
repeat destruct _ =? _ eqn :? in Hreg ; try discriminate ; injection Hreg as ←;repeat match goal withH : _ =? _ = true |- _⇒apply Z.eqb_eq in Hend;subst;auto 10
Explore proof 3 tactics
Initial goal
intros b1 r1 b2 r2 E1 L1 E2 L2 Hne
b1 :
Z
r1 :
b2 :
Z
r2 :
E1 :
object_regionb1 m_regionsconversion_mem = Somer1
E2 :
object_regionb2 m_regionsconversion_mem = Somer2
Hne :
b1 ≠ b2
apply regions in E1 , E2
b1 :
Z
r1 :
b2 :
Z
r2 :
E1 :
b1 = 1024 ∧ r1 = r_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live ∨ b1 = 2048 ∧ r1 = r_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live ∨ b1 = 3072 ∧ r1 = r_base ≔ 3072; r_end ≔ 3080; r_kind ≔ Stack; r_life ≔ Live ∨ b1 = 4096 ∧ r1 = r_base ≔ 4096; r_end ≔ 4104; r_kind ≔ GlobalData; r_life ≔ Live ∨ b1 = 5120 ∧ r1 = r_base ≔ 5120; r_end ≔ 5128; r_kind ≔ Heap; r_life ≔ Live
E2 :
b2 = 1024 ∧ r2 = r_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live ∨ b2 = 2048 ∧ r2 = r_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live ∨ b2 = 3072 ∧ r2 = r_base ≔ 3072; r_end ≔ 3080; r_kind ≔ Stack; r_life ≔ Live ∨ b2 = 4096 ∧ r2 = r_base ≔ 4096; r_end ≔ 4104; r_kind ≔ GlobalData; r_life ≔ Live ∨ b2 = 5120 ∧ r2 = r_base ≔ 5120; r_end ≔ 5128; r_kind ≔ Heap; r_life ≔ Live
Hne :
b1 ≠ b2
repeat destruct E1 as E1 | E1 ; destruct E1 as → → ; repeat destruct E2 as E2 | E2 ; destruct E2 as → → ; simpl in * ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros b1 r1 b2 r2 E1 L1 E2 L2 Hne
apply regions in E1 , E2
repeat destruct E1 as E1 | E1 ; destruct E1 as → → ; repeat destruct E2 as E2 | E2 ; destruct E2 as → → ; simpl in * ; lia
Explore proof 10 tactics
Initial goal
split ; change 0 < 4294967296 ≤ 281474976710656 ; lia |
⊢
∀b : Z reg : region, object_regionb m_regionsconversion_mem = Somereg → 0 ≤ b < InterpRuntime.start ∧ r_endreg ≤ InterpRuntime.start ∧ r_lifereg = Freed → r_endreg = b ∧ ∀a : Z, InterpRuntime.start ≤ a → m_bytesconversion_mem a = 0 ∧ m_auxconversion_mem a = CNone
split
2 open⊢
∀b : Z reg : region, object_regionb m_regionsconversion_mem = Somereg → 0 ≤ b < InterpRuntime.start ∧ r_endreg ≤ InterpRuntime.start ∧ r_lifereg = Freed → r_endreg = b
focused goal
⊢
∀a : Z, InterpRuntime.start ≤ a → m_bytesconversion_mem a = 0 ∧ m_auxconversion_mem a = CNone
–intros b reg E
2 open⊢
0 ≤ b < InterpRuntime.start ∧ r_endreg ≤ InterpRuntime.start ∧ r_lifereg = Freed → r_endreg = b
deferred goal
⊢
∀a : Z, InterpRuntime.start ≤ a → m_bytesconversion_mem a = 0 ∧ m_auxconversion_mem a = CNone
apply regions in E
2 openb :
Z
reg :
E :
b = 1024 ∧ reg = r_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live ∨ b = 2048 ∧ reg = r_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live ∨ b = 3072 ∧ reg = r_base ≔ 3072; r_end ≔ 3080; r_kind ≔ Stack; r_life ≔ Live ∨ b = 4096 ∧ reg = r_base ≔ 4096; r_end ≔ 4104; r_kind ≔ GlobalData; r_life ≔ Live ∨ b = 5120 ∧ reg = r_base ≔ 5120; r_end ≔ 5128; r_kind ≔ Heap; r_life ≔ Live
⊢
0 ≤ b < InterpRuntime.start ∧ r_endreg ≤ InterpRuntime.start ∧ r_lifereg = Freed → r_endreg = b
deferred goal
⊢
∀a : Z, InterpRuntime.start ≤ a → m_bytesconversion_mem a = 0 ∧ m_auxconversion_mem a = CNone
change 0 ≤ b < 4294967296 ∧ r_endreg ≤ 4294967296 ∧ r_lifereg = Freed → r_endreg = b
2 openb :
Z
reg :
E :
b = 1024 ∧ reg = r_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live ∨ b = 2048 ∧ reg = r_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live ∨ b = 3072 ∧ reg = r_base ≔ 3072; r_end ≔ 3080; r_kind ≔ Stack; r_life ≔ Live ∨ b = 4096 ∧ reg = r_base ≔ 4096; r_end ≔ 4104; r_kind ≔ GlobalData; r_life ≔ Live ∨ b = 5120 ∧ reg = r_base ≔ 5120; r_end ≔ 5128; r_kind ≔ Heap; r_life ≔ Live
deferred goal
⊢
∀a : Z, InterpRuntime.start ≤ a → m_bytesconversion_mem a = 0 ∧ m_auxconversion_mem a = CNone
repeat destruct E as E | E ; destruct E as → → ; simpl ; intuition try discriminate ; lia
deferred goal
⊢
∀a : Z, InterpRuntime.start ≤ a → m_bytesconversion_mem a = 0 ∧ m_auxconversion_mem a = CNone
–intros a Ha
a :
Z
Ha :
⊢
m_bytesconversion_mem a = 0 ∧ m_auxconversion_mem a = CNone
change 4294967296 ≤ a in Ha
a :
Z
Ha :
4294967296 ≤ a
⊢
m_bytesconversion_mem a = 0 ∧ m_auxconversion_mem a = CNone
cbn [ conversion_mem m_bytes m_aux ]
repeat match goal with|- context [a =? ]⇒destruct Z.eqb_speca b ; subst ; lia | end;auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; change 0 < 4294967296 ≤ 281474976710656 ; lia |
split
–intros b reg E
apply regions in E
repeat destruct E as E | E ; destruct E as → → ; simpl ; intuition try discriminate ; lia
–intros a Ha
change 4294967296 ≤ a in Ha
cbn [ conversion_mem m_bytes m_aux ]
repeat match goal with|- context [a =? ]⇒destruct Z.eqb_speca b ; subst ; lia | end;auto
Explore proof 6 tactics
Initial goal
intros l v Hl
apply elem_of_list_to_map_2 in Hl
eapply all_agree_elem ; | exact Hl
change all_agreeconversion_mem byte_ps5120 0 errno_bytesconversion_mem 5120 0
⊢
all_agreeconversion_mem byte_ps5120 0 errno_bytesconversion_mem 5120 0
apply errno_bytes_agree
⊢
errno_cellconversion_mem ptr_addr ≔ 5120 + 0; ptr_cap ≔ Obj5120
exact proj1proj2proj2F.readytrue
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros l v Hl
apply elem_of_list_to_map_2 in Hl
eapply all_agree_elem ; | exact Hl
change all_agreeconversion_mem byte_ps5120 0 errno_bytesconversion_mem 5120 0
apply errno_bytes_agree
exact proj1proj2proj2F.readytrue
libc_errno_wiλ_ _ ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue heap
Explore proof 12 tactics
Initial goal
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue heap
split ; apply F.ready |
⊢
libc_errnoF.worldtrue.1 = ptr_addr ≔ 5120 + 0; ptr_cap ≔ Obj5120 ∧ roots_apartlibc_stream_aux_rootsF.worldtrue file_handleF.out_file heap conversion_mem ∧ ids_apartlibc_stream_releasesF.worldtrue file_handleF.out_file heap ∧ pieces_offerrno_keys5120 0 heap conversion_mem span_containserrno_span5120 0
split ; reflexivity |
⊢
roots_apartlibc_stream_aux_rootsF.worldtrue file_handleF.out_file heap conversion_mem ∧ ids_apartlibc_stream_releasesF.worldtrue file_handleF.out_file heap ∧ pieces_offerrno_keys5120 0 heap conversion_mem span_containserrno_span5120 0
split ; intros root a |
⊢
ids_apartlibc_stream_releasesF.worldtrue file_handleF.out_file heap ∧ pieces_offerrno_keys5120 0 heap conversion_mem span_containserrno_span5120 0
split ; intros base l v |
⊢
intros l v Hl Hnot
⊢
match l with
⇒
∀reg : region, live_atconversion_mem b reg → 0 ≤ o → b + o < r_endreg → ¬span_containserrno_span5120 0 b + o
_
⇒
True
apply elem_of_list_to_map_2 in Hl
⊢
match l with
⇒
∀reg : region, live_atconversion_mem b reg → 0 ≤ o → b + o < r_endreg → ¬span_containserrno_span5120 0 b + o
_
⇒
True
exfalso
⊢
False
apply Hnot
⊢
l ∈ errno_keys5120 0
change l ∈ byte_ps5120 0 0; 0; 0; 0.*1
⊢
l ∈ byte_ps5120 0 0; 0; 0; 0.*1
apply list_elem_of_fmap
exists l, v
⊢
l = l, v.1 ∧ l, v ∈ byte_ps5120 0 0; 0; 0; 0
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
438Example owned_errno_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 heap
Explore proof 13 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 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 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 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 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 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 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 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 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 heap
destruct E.query_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False file_handleF.out_file 5120 0 _ _ _ _ _ _ _ _ _ _ _ heap or_introreq_refl Hcall heap_agrees as Ha & _ & _ & Hw
4 openHcall :
focused goal
focused goal
Hcall :
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue heap
focused goal
Hcall :
Hw :
libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue heap
⊢
agreesconversion_mem heap ∧ libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue heap
–exact disjoint
3 opendeferred goal
deferred goal
Hcall :
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue heap
deferred goal
Hcall :
Hw :
libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue heap
⊢
agreesconversion_mem heap ∧ libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue heap
–exact ready
2 opendeferred goal
Hcall :
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue heap
deferred goal
Hcall :
Hw :
libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue heap
⊢
agreesconversion_mem heap ∧ libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue heap
–exact heap_wi
deferred goal
Hcall :
Hw :
libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue heap
⊢
agreesconversion_mem heap ∧ libc_errno_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file 5120 0 conversion_mem F.worldtrue 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 E.query_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False file_handleF.out_file 5120 0 _ _ _ _ _ _ _ _ _ _ _ heap or_introreq_refl Hcall heap_agrees as Ha & _ & _ & Hw
–exact disjoint
–exact ready
–exact heap_wi
–auto
463Example old_all_roots_frame_rejects_owned_errno: ¬libc_stream_wiλ_ _ ⇒ True file_handleF.out_file conversion_mem F.worldtrue heap
Explore proof 19 tactics
Initial goal
⊢
¬libc_stream_wiλ_ : mem _ : libc_world ⇒ True file_handleF.out_file conversion_mem F.worldtrue heap
intros _ & Hroots & _
Hroots :
⊢
False
apply HrootsmkSpanmkPtr5120 Obj5120 4 5123
3 openHroots :
⊢
Inspan_ptr ≔ ptr_addr ≔ 5120; ptr_cap ≔ Obj5120; span_size ≔ 4 libc_stream_writesF.worldtrue file_handleF.out_file
focused goal
Hroots :
focused goal
Hroots :
⊢
–left
3 openHroots :
deferred goal
Hroots :
deferred goal
Hroots :
⊢
reflexivity
2 opendeferred goal
Hroots :
deferred goal
Hroots :
⊢
–unfold span_contains
2 openHroots :
deferred goal
Hroots :
⊢
simpl
2 openHroots :
⊢
5120 ≤ 5123 < 5120 + 4
deferred goal
Hroots :
⊢
lia
deferred goal
Hroots :
⊢
–exists PByte5120 3, VByte0, mkRegion5120 5128 Heap Live
Hroots :
split
2 openHroots :
focused goal
Hroots :
+unfold heap
2 openHroots :
deferred goal
Hroots :
apply elem_of_list_to_map_1
3 openHroots :
⊢
base.NoDupbyte_ps5120 0 0; 0; 0; 0.*1
focused goal
Hroots :
deferred goal
Hroots :
∗change base.NoDupPByte5120 0; PByte5120 1; PByte5120 2; PByte5120 3
3 openHroots :
deferred goal
Hroots :
deferred goal
Hroots :
repeat apply base.NoDup_cons_2 ; set_solver |
3 openHroots :
⊢
base.NoDup[ ]
deferred goal
Hroots :
deferred goal
Hroots :
apply base.NoDup_nil_2
2 opendeferred goal
Hroots :
deferred goal
Hroots :
∗apply list_elem_of_In
2 openHroots :
deferred goal
Hroots :
simpl
2 openHroots :
deferred goal
Hroots :
auto 10
deferred goal
Hroots :
+split ; exact I |
Hroots :
split ; split ; reflexivity | simpl ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros _ & Hroots & _
–left
reflexivity
split
+unfold heap
apply elem_of_list_to_map_1
repeat apply base.NoDup_cons_2 ; set_solver |
apply base.NoDup_nil_2
∗apply list_elem_of_In
simpl
auto 10
+split ; exact I |
split ; split ; reflexivity | simpl ; lia