rocq/theories/LibcStreamLogic.v
Program-memory and selected-FILE world frames over the logic's exact machine. Private FILE representation is trusted; separation from program pieces is explicit and propagated, not assumed at return.
From iris.proofmode Require Import proofmode
From Stdlib Require Import ZArith List Lia
From Nanofil Require Import Term Syntax Values Memory Runtime ExternalCalls ExternalMachine Stdio Shutdown Streams Formatting Libc LibcStreams Pieces Heap ContractFrame Logic
Open Scope Z_scope
Open Scope list_scope
A fixed FILE handle's authority is apart from the program heap. This predicate intentionally does not promise that the handle is open: errno and hard-exit boundaries must remain usable after close.
libc_stream_readyrep m w ∧ roots_apartlibc_stream_writesw p h m ∧ ids_apartlibc_stream_releasesw p h
A close-callback boundary may have a closed FILE, but must not yet have handed control to the host. Readiness alone does not say this.
libc_stream_wirep p m w h ∧ ∀kind, shutdown_atsndw ≠ HandedOffkind
stream_delegatesmodel w p born m w′
roots_apartstream_writesmodel w p h m
ids_apartstream_releasesmodel w p h
ids_apartborn h
roots_apartstream_writesmodel w′ p h m ∧ ids_apartstream_releasesmodel w′ p h
Explore proof 9 tactics
Initial goal
⊢
∀world : Type model : stream_modelworld w : world p : ptr born : listZ m : mem w′ : world h : gmappiece pval, stream_delegatesmodel w p born m w′ → roots_apartstream_writesmodel w p h m → ids_apartstream_releasesmodel w p h → ids_apartborn h → live_disjointm → roots_apartstream_writesmodel w′ p h m ∧ ids_apartstream_releasesmodel w′ p h
intros world model w p born m w′ h Hroots & _ & Hrelease Hra Hrel Hb Hd
world :
Type
model :
stream_modelworld
w :
world
p :
born :
listZ
m :
w′ :
world
Hroots :
∀root : span, Inroot stream_writesmodel w′ p → available_capstream_sourcesmodel w p born m ptr_capspan_ptrroot ∧ ∀a : Z, span_containsroot a → write_authoritystream_writesmodel w p born m a
Hrelease :
∀base : Z, Inbase stream_releasesmodel w′ p → Inbase stream_releasesmodel w p ∨ Inbase born
Hra :
roots_apartstream_writesmodel w p h m
Hrel :
ids_apartstream_releasesmodel w p h
Hb :
ids_apartborn h
Hd :
⊢
roots_apartstream_writesmodel w′ p h m ∧ ids_apartstream_releasesmodel w′ p h
split
2 openworld :
Type
model :
stream_modelworld
w :
world
p :
born :
listZ
m :
w′ :
world
Hroots :
∀root : span, Inroot stream_writesmodel w′ p → available_capstream_sourcesmodel w p born m ptr_capspan_ptrroot ∧ ∀a : Z, span_containsroot a → write_authoritystream_writesmodel w p born m a
Hrelease :
∀base : Z, Inbase stream_releasesmodel w′ p → Inbase stream_releasesmodel w p ∨ Inbase born
Hra :
roots_apartstream_writesmodel w p h m
Hrel :
ids_apartstream_releasesmodel w p h
Hb :
ids_apartborn h
Hd :
⊢
roots_apartstream_writesmodel w′ p h m
focused goal
world :
Type
model :
stream_modelworld
w :
world
p :
born :
listZ
m :
w′ :
world
Hroots :
∀root : span, Inroot stream_writesmodel w′ p → available_capstream_sourcesmodel w p born m ptr_capspan_ptrroot ∧ ∀a : Z, span_containsroot a → write_authoritystream_writesmodel w p born m a
Hrelease :
∀base : Z, Inbase stream_releasesmodel w′ p → Inbase stream_releasesmodel w p ∨ Inbase born
Hra :
roots_apartstream_writesmodel w p h m
Hrel :
ids_apartstream_releasesmodel w p h
Hb :
ids_apartborn h
Hd :
⊢
ids_apartstream_releasesmodel w′ p h
–intros root a Hin Hspan Hown
2 openworld :
Type
model :
stream_modelworld
w :
world
p :
born :
listZ
m :
w′ :
world
Hroots :
∀root : span, Inroot stream_writesmodel w′ p → available_capstream_sourcesmodel w p born m ptr_capspan_ptrroot ∧ ∀a : Z, span_containsroot a → write_authoritystream_writesmodel w p born m a
Hrelease :
∀base : Z, Inbase stream_releasesmodel w′ p → Inbase stream_releasesmodel w p ∨ Inbase born
Hra :
roots_apartstream_writesmodel w p h m
Hrel :
ids_apartstream_releasesmodel w p h
Hb :
ids_apartborn h
Hd :
root :
a :
Z
Hin :
Inroot stream_writesmodel w′ p
Hspan :
span_containsroot a
Hown :
owned_liveh m a
⊢
False
deferred goal
world :
Type
model :
stream_modelworld
w :
world
p :
born :
listZ
m :
w′ :
world
Hroots :
∀root : span, Inroot stream_writesmodel w′ p → available_capstream_sourcesmodel w p born m ptr_capspan_ptrroot ∧ ∀a : Z, span_containsroot a → write_authoritystream_writesmodel w p born m a
Hrelease :
∀base : Z, Inbase stream_releasesmodel w′ p → Inbase stream_releasesmodel w p ∨ Inbase born
Hra :
roots_apartstream_writesmodel w p h m
Hrel :
ids_apartstream_releasesmodel w p h
Hb :
ids_apartborn h
Hd :
⊢
ids_apartstream_releasesmodel w′ p h
destruct Hrootsroot Hin as _ Hauth
2 openworld :
Type
model :
stream_modelworld
w :
world
p :
born :
listZ
m :
w′ :
world
Hroots :
∀root : span, Inroot stream_writesmodel w′ p → available_capstream_sourcesmodel w p born m ptr_capspan_ptrroot ∧ ∀a : Z, span_containsroot a → write_authoritystream_writesmodel w p born m a
Hrelease :
∀base : Z, Inbase stream_releasesmodel w′ p → Inbase stream_releasesmodel w p ∨ Inbase born
Hra :
roots_apartstream_writesmodel w p h m
Hrel :
ids_apartstream_releasesmodel w p h
Hb :
ids_apartborn h
Hd :
root :
a :
Z
Hin :
Inroot stream_writesmodel w′ p
Hspan :
span_containsroot a
Hown :
owned_liveh m a
Hauth :
∀a : Z, span_containsroot a → write_authoritystream_writesmodel w p born m a
⊢
False
deferred goal
world :
Type
model :
stream_modelworld
w :
world
p :
born :
listZ
m :
w′ :
world
Hroots :
∀root : span, Inroot stream_writesmodel w′ p → available_capstream_sourcesmodel w p born m ptr_capspan_ptrroot ∧ ∀a : Z, span_containsroot a → write_authoritystream_writesmodel w p born m a
Hrelease :
∀base : Z, Inbase stream_releasesmodel w′ p → Inbase stream_releasesmodel w p ∨ Inbase born
Hra :
roots_apartstream_writesmodel w p h m
Hrel :
ids_apartstream_releasesmodel w p h
Hb :
ids_apartborn h
Hd :
⊢
ids_apartstream_releasesmodel w′ p h
exact owned_not_authority_ _ _ _ _ Hd Hra Hb Hown Hautha Hspan
deferred goal
world :
Type
model :
stream_modelworld
w :
world
p :
born :
listZ
m :
w′ :
world
Hroots :
∀root : span, Inroot stream_writesmodel w′ p → available_capstream_sourcesmodel w p born m ptr_capspan_ptrroot ∧ ∀a : Z, span_containsroot a → write_authoritystream_writesmodel w p born m a
Hrelease :
∀base : Z, Inbase stream_releasesmodel w′ p → Inbase stream_releasesmodel w p ∨ Inbase born
Hra :
roots_apartstream_writesmodel w p h m
Hrel :
ids_apartstream_releasesmodel w p h
Hb :
ids_apartborn h
Hd :
⊢
ids_apartstream_releasesmodel w′ p h
–intros base l v Hin Hlookup Hmem
world :
Type
model :
stream_modelworld
w :
world
p :
born :
listZ
m :
w′ :
world
Hroots :
∀root : span, Inroot stream_writesmodel w′ p → available_capstream_sourcesmodel w p born m ptr_capspan_ptrroot ∧ ∀a : Z, span_containsroot a → write_authoritystream_writesmodel w p born m a
Hrelease :
∀base : Z, Inbase stream_releasesmodel w′ p → Inbase stream_releasesmodel w p ∨ Inbase born
Hra :
roots_apartstream_writesmodel w p h m
Hrel :
ids_apartstream_releasesmodel w p h
Hb :
ids_apartborn h
Hd :
base :
Z
l :
v :
Hin :
Inbase stream_releasesmodel w′ p
Hlookup :
h !! l = Somev
Hmem :
⊢
piece_idl ≠ base
destruct Hreleasebase Hin as Hold | Hnew
2 openworld :
Type
model :
stream_modelworld
w :
world
p :
born :
listZ
m :
w′ :
world
Hroots :
∀root : span, Inroot stream_writesmodel w′ p → available_capstream_sourcesmodel w p born m ptr_capspan_ptrroot ∧ ∀a : Z, span_containsroot a → write_authoritystream_writesmodel w p born m a
Hrelease :
∀base : Z, Inbase stream_releasesmodel w′ p → Inbase stream_releasesmodel w p ∨ Inbase born
Hra :
roots_apartstream_writesmodel w p h m
Hrel :
ids_apartstream_releasesmodel w p h
Hb :
ids_apartborn h
Hd :
base :
Z
l :
v :
Hin :
Inbase stream_releasesmodel w′ p
Hlookup :
h !! l = Somev
Hmem :
Hold :
Inbase stream_releasesmodel w p
⊢
piece_idl ≠ base
focused goal
world :
Type
model :
stream_modelworld
w :
world
p :
born :
listZ
m :
w′ :
world
Hroots :
∀root : span, Inroot stream_writesmodel w′ p → available_capstream_sourcesmodel w p born m ptr_capspan_ptrroot ∧ ∀a : Z, span_containsroot a → write_authoritystream_writesmodel w p born m a
Hrelease :
∀base : Z, Inbase stream_releasesmodel w′ p → Inbase stream_releasesmodel w p ∨ Inbase born
Hra :
roots_apartstream_writesmodel w p h m
Hrel :
ids_apartstream_releasesmodel w p h
Hb :
ids_apartborn h
Hd :
base :
Z
l :
v :
Hin :
Inbase stream_releasesmodel w′ p
Hlookup :
h !! l = Somev
Hmem :
Hnew :
Inbase born
⊢
piece_idl ≠ base
+exact Hrelbase l v Hold Hlookup Hmem
deferred goal
world :
Type
model :
stream_modelworld
w :
world
p :
born :
listZ
m :
w′ :
world
Hroots :
∀root : span, Inroot stream_writesmodel w′ p → available_capstream_sourcesmodel w p born m ptr_capspan_ptrroot ∧ ∀a : Z, span_containsroot a → write_authoritystream_writesmodel w p born m a
Hrelease :
∀base : Z, Inbase stream_releasesmodel w′ p → Inbase stream_releasesmodel w p ∨ Inbase born
Hra :
roots_apartstream_writesmodel w p h m
Hrel :
ids_apartstream_releasesmodel w p h
Hb :
ids_apartborn h
Hd :
base :
Z
l :
v :
Hin :
Inbase stream_releasesmodel w′ p
Hlookup :
h !! l = Somev
Hmem :
Hnew :
Inbase born
⊢
piece_idl ≠ base
+exact Hbbase l v Hnew Hlookup Hmem
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros world model w p born m w′ h Hroots & _ & Hrelease Hra Hrel Hb Hd
split
–intros root a Hin Hspan Hown
destruct Hrootsroot Hin as _ Hauth
exact owned_not_authority_ _ _ _ _ Hd Hra Hb Hown Hautha Hspan
–intros base l v Hin Hlookup Hmem
destruct Hreleasebase Hin as Hold | Hnew
+exact Hrelbase l v Hold Hlookup Hmem
+exact Hbbase l v Hnew Hlookup Hmem
Use the consumer's logic and its inductive call relations, not a separately instantiated sibling machine. No new runtime law.
Include Logic R
Native represented readiness at a collector poll is an explicit realization law. Region identity then proves the heap-separation part, rather than requiring a separate separation assumption.
∀ rep p
∀s m s′ m′ w, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
Explore proof 14 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop p : ptr, ∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w → LG.SafepointStablelibc_stream_wirep p
intros rep p Hstable
rep :
mem → libc_world → Prop
p :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
split
rep :
mem → libc_world → Prop
p :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
⊢
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world h : gmappiece pval, R.safepoints m s′ m′ → libc_stream_wirep p m w h → libc_stream_wirep p m′ w h
intros s m s′ m′ w h Hsp Hr & Hapart & Hrel
rep :
mem → libc_world → Prop
p :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
libc_stream_readyrep m w
Hapart :
Hrel :
⊢
libc_stream_wirep p m′ w h
split ; eapply Hstable ; eauto |
rep :
mem → libc_world → Prop
p :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
libc_stream_readyrep m w
Hapart :
Hrel :
⊢
roots_apartlibc_stream_writesw p h m′ ∧ ids_apartlibc_stream_releasesw p h
split ; | exact Hrel
rep :
mem → libc_world → Prop
p :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
libc_stream_readyrep m w
Hapart :
Hrel :
⊢
roots_apartlibc_stream_writesw p h m′
intros root a Hin Hspan l & v & reg & Hl & Hmem & E Hlive & Hrange
rep :
mem → libc_world → Prop
p :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
libc_stream_readyrep m w
Hapart :
Hrel :
root :
a :
Z
Hin :
Inroot libc_stream_writesw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
E :
object_regionpiece_idl m_regionsm′ = Somereg
⊢
False
apply Hapartroot a Hin Hspan
rep :
mem → libc_world → Prop
p :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
libc_stream_readyrep m w
Hapart :
Hrel :
root :
a :
Z
Hin :
Inroot libc_stream_writesw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
E :
object_regionpiece_idl m_regionsm′ = Somereg
⊢
owned_liveh m a
exists l, v, reg
rep :
mem → libc_world → Prop
p :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
libc_stream_readyrep m w
Hapart :
Hrel :
root :
a :
Z
Hin :
Inroot libc_stream_writesw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
E :
object_regionpiece_idl m_regionsm′ = Somereg
split ; exact Hl |
rep :
mem → libc_world → Prop
p :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
libc_stream_readyrep m w
Hapart :
Hrel :
root :
a :
Z
Hin :
Inroot libc_stream_writesw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
E :
object_regionpiece_idl m_regionsm′ = Somereg
split ; exact Hmem |
rep :
mem → libc_world → Prop
p :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
libc_stream_readyrep m w
Hapart :
Hrel :
root :
a :
Z
Hin :
Inroot libc_stream_writesw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
E :
object_regionpiece_idl m_regionsm′ = Somereg
split ; | exact Hrange
rep :
mem → libc_world → Prop
p :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
libc_stream_readyrep m w
Hapart :
Hrel :
root :
a :
Z
Hin :
Inroot libc_stream_writesw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
E :
object_regionpiece_idl m_regionsm′ = Somereg
split ; | exact Hlive
rep :
mem → libc_world → Prop
p :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
libc_stream_readyrep m w
Hapart :
Hrel :
root :
a :
Z
Hin :
Inroot libc_stream_writesw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
E :
object_regionpiece_idl m_regionsm′ = Somereg
⊢
object_regionpiece_idl m_regionsm = Somereg
rewrite R.collector_live_ _ _ _ Hsp in E
rep :
mem → libc_world → Prop
p :
Hstable :
∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
libc_stream_readyrep m w
Hapart :
Hrel :
root :
a :
Z
Hin :
Inroot libc_stream_writesw p
Hspan :
span_containsroot a
l :
v :
reg :
Hl :
h !! l = Somev
Hmem :
E :
object_regionpiece_idl m_regionsm = Somereg
⊢
object_regionpiece_idl m_regionsm = Somereg
exact E
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep p Hstable
split
intros s m s′ m′ w h Hsp Hr & Hapart & Hrel
split ; eapply Hstable ; eauto |
split ; | exact Hrel
intros root a Hin Hspan l & v & reg & Hl & Hmem & E Hlive & Hrange
apply Hapartroot a Hin Hspan
exists l, v, reg
split ; exact Hl |
split ; exact Hmem |
split ; | exact Hrange
split ; | exact Hlive
rewrite R.collector_live_ _ _ _ Hsp in E
exact E
Narrow actions cannot turn a non-wide stream into a wide one.
Explore proof 5 tactics
Initial goal
⊢
∀q : stream_state actions : liststream_action q′ : stream_state, stream_runq actions q′ → orientationq ≠ WideOriented → orientationq′ ≠ WideOriented
intros q actions q′ Hrun
⊢
orientationq ≠ WideOriented → orientationq′ ≠ WideOriented
induction Hrun ; auto |
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
Hrun :
stream_runq1 actions q′
IHHrun :
orientationq1 ≠ WideOriented → orientationq′ ≠ WideOriented
⊢
orientationq ≠ WideOriented → orientationq′ ≠ WideOriented
intros Hn
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
Hrun :
stream_runq1 actions q′
IHHrun :
orientationq1 ≠ WideOriented → orientationq′ ≠ WideOriented
Hn :
⊢
apply IHHrun
q :
action :
q1 :
actions :
liststream_action
q′ :
H :
stream_stepq action q1
Hrun :
stream_runq1 actions q′
IHHrun :
orientationq1 ≠ WideOriented → orientationq′ ≠ WideOriented
Hn :
⊢
inversion H ; subst ; simpl ; congruence
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros q actions q′ Hrun
induction Hrun ; auto |
intros Hn
apply IHHrun
inversion H ; subst ; simpl ; congruence
Active lookup is consistent with the sole authoritative protocol.
Explore proof 3 tactics
Initial goal
⊢
∀w : libc_world p : ptr info : stream_info, libc_stream_atw p = Someinfo → libc_stream_statew p = stream_protocolinfo
intros w p info Hinfo
⊢
libc_stream_statew p = stream_protocolinfo
unfold libc_stream_at in Hinfo
w :
p :
info :
Hinfo :
Somefile
⇒
Somestream_identifier ≔ if same_filep libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew p; stream_pending ≔ file_pendingfile
None
⇒
None
=
Someinfo
⊢
libc_stream_statew p = stream_protocolinfo
destruct libc_file_atw p ; injection Hinfo as ← ; reflexivity | discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros w p info Hinfo
unfold libc_stream_at in Hinfo
destruct libc_file_atw p ; injection Hinfo as ← ; reflexivity | discriminate
Output does not close its selected handle or switch it to wide. This holds even when the accepted prefix ends in a resource failure.
∀ rep requests wide api r args xs p s m w trace ending s′ m′ w′
p = output_targetapi libc_stdout w xs
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
∃file, libc_file_atw′ p = Somefile ∧ orientationlibc_stream_statew′ p ≠ WideOriented ∧ libc_stdoutw′ = libc_stdoutw
Explore proof 15 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop api : narrow_api r : call_result args : listarg xs : listword p : ptr s : R.state m : mem w : libc_world trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, p = output_targetapi libc_stdout w xs → orientationlibc_stream_statew p ≠ WideOriented → M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′ → ∃file : libc_file, libc_file_atw′ p = Somefile ∧ orientationlibc_stream_statew′ p ≠ WideOriented ∧ libc_stdoutw′ = libc_stdoutw
intros rep requests wide api r args xs p s m w trace ending s′ m′ w′ → Hn Hcall
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
⊢
∃file : libc_file, libc_file_atw′ output_targetapi libc_stdout w xs = Somefile ∧ orientationlibc_stream_statew′ output_targetapi libc_stdout w xs ≠ WideOriented ∧ libc_stdoutw′ = libc_stdoutw
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & _ & info & info′ & bytes & actions & tail & Hinfo & Htext & Hbytes & Hrun & Hready & Hinfo′ & Hframe & _
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
stream_atlibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hready :
stream_openlibc_stream_modelrep requests wide m′ w′ output_targetapi libc_stdout w xs info′
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
∃file : libc_file, libc_file_atw′ output_targetapi libc_stdout w xs = Somefile ∧ orientationlibc_stream_statew′ output_targetapi libc_stdout w xs ≠ WideOriented ∧ libc_stdoutw′ = libc_stdoutw
destruct Hready as _ & Hactive & Hstate & _
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
stream_atlibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = stream_state_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
∃file : libc_file, libc_file_atw′ output_targetapi libc_stdout w xs = Somefile ∧ orientationlibc_stream_statew′ output_targetapi libc_stdout w xs ≠ WideOriented ∧ libc_stdoutw′ = libc_stdoutw
change stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs in Hstate
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
stream_atlibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
∃file : libc_file, libc_file_atw′ output_targetapi libc_stdout w xs = Somefile ∧ orientationlibc_stream_statew′ output_targetapi libc_stdout w xs ≠ WideOriented ∧ libc_stdoutw′ = libc_stdoutw
change libc_stream_atw output_targetapi libc_stdout w xs = Someinfo in Hinfo
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
∃file : libc_file, libc_file_atw′ output_targetapi libc_stdout w xs = Somefile ∧ orientationlibc_stream_statew′ output_targetapi libc_stdout w xs ≠ WideOriented ∧ libc_stdoutw′ = libc_stdoutw
split
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
∃file : libc_file, libc_file_atw′ output_targetapi libc_stdout w xs = Somefile
focused goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
orientationlibc_stream_statew′ output_targetapi libc_stdout w xs ≠ WideOriented ∧ libc_stdoutw′ = libc_stdoutw
–change libc_stream_atw′ output_targetapi libc_stdout w xs = Someinfo′ in Hactive
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
libc_stream_atw′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
∃file : libc_file, libc_file_atw′ output_targetapi libc_stdout w xs = Somefile
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
orientationlibc_stream_statew′ output_targetapi libc_stdout w xs ≠ WideOriented ∧ libc_stdoutw′ = libc_stdoutw
unfold libc_stream_at in Hactive
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
Somefile
⇒
Somestream_identifier ≔ if same_fileoutput_targetapi libc_stdout w xs libc_stdoutw′ then 1 else 2; stream_protocol ≔ libc_stream_statew′ output_targetapi libc_stdout w xs; stream_pending ≔ file_pendingfile
None
⇒
None
=
Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
∃file : libc_file, libc_file_atw′ output_targetapi libc_stdout w xs = Somefile
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
orientationlibc_stream_statew′ output_targetapi libc_stdout w xs ≠ WideOriented ∧ libc_stdoutw′ = libc_stdoutw
destruct libc_file_atw′ _ as file | ; exists file ; reflexivity | discriminate
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
orientationlibc_stream_statew′ output_targetapi libc_stdout w xs ≠ WideOriented ∧ libc_stdoutw′ = libc_stdoutw
–split
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
focused goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
libc_stdoutw′ = libc_stdoutw
+rewrite <- Hstate
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
libc_stdoutw′ = libc_stdoutw
eapply narrow_run ; exact Hrun |
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
libc_stdoutw′ = libc_stdoutw
rewrite <- active_protocol_ _ _ Hinfo
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
libc_stdoutw′ = libc_stdoutw
exact Hn
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hn :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
libc_stream_atw output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hactive :
stream_atlibc_stream_modelrep requests wide w′ output_targetapi libc_stdout w xs = Someinfo′
Hstate :
stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs
Hinfo′ :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
⊢
libc_stdoutw′ = libc_stdoutw
+exact proj1Hframe
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide api r args xs p s m w trace ending s′ m′ w′ → Hn Hcall
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & _ & info & info′ & bytes & actions & tail & Hinfo & Htext & Hbytes & Hrun & Hready & Hinfo′ & Hframe & _
destruct Hready as _ & Hactive & Hstate & _
change stream_protocolinfo′ = libc_stream_statew′ output_targetapi libc_stdout w xs in Hstate
change libc_stream_atw output_targetapi libc_stdout w xs = Someinfo in Hinfo
split
–change libc_stream_atw′ output_targetapi libc_stdout w xs = Someinfo′ in Hactive
unfold libc_stream_at in Hactive
destruct libc_file_atw′ _ as file | ; exists file ; reflexivity | discriminate
–split
+exact proj1Hframe
Returning or resource-ending output preserves the program heap and re-establishes selected-FILE separation for the next call.
∀ rep requests wide api r args xs p s m w trace ending s′ m′ w′ h
p = output_targetapi libc_stdout w xs
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
agreesm h
R.readys m
libc_stream_wirep p m w h
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h
Explore proof 10 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop api : narrow_api r : call_result args : listarg xs : listword p : ptr s : R.state m : mem w : libc_world trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world h : gmappiece pval, p = output_targetapi libc_stdout w xs → M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′ → agreesm h → live_disjointm → R.readys m → libc_stream_wirep p m w h → agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h
intros rep requests wide api r args xs p s m w trace ending s′ m′ w′ h → Hcall Ha Hd Hr Hready & Hra & Hrel
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
roots_apartlibc_stream_writesw output_targetapi libc_stdout w xs h m
Hrel :
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep output_targetapi libc_stdout w xs 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
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
roots_apartlibc_stream_writesw output_targetapi libc_stdout w xs h m
Hrel :
born :
listZ
Hp :
M.E.prefixoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs s m w born trace s′ m′ w′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep output_targetapi libc_stdout w xs m′ w′ h
destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as Hr′ _
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
roots_apartlibc_stream_writesw output_targetapi libc_stdout w xs h m
Hrel :
born :
listZ
Hp :
M.E.prefixoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs s m w born trace s′ m′ w′
Hr′ :
R.readys′ m′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep output_targetapi libc_stdout w xs m′ w′ h
destruct LG.prefix_agrees_ _ _ _ _ _ _ _ _ _ _ h Hp Hr Hd Ha Hra ltac:intros base l v as Ha′ & Hd′ & Hb & Hra′
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
roots_apartlibc_stream_writesw output_targetapi libc_stdout w xs h m
Hrel :
born :
listZ
Hp :
M.E.prefixoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs s m w born trace s′ m′ w′
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hra′ :
roots_apartcontract_writesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w h m′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep output_targetapi libc_stdout w xs m′ w′ h
destruct Hp as _ & info & info′ & bytes & actions & tail & Hinfo & Htext & Hbytes & Hrun & Hopen & Hid & Hframe & Hdelegate & Htrace & Haux
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
roots_apartlibc_stream_writesw output_targetapi libc_stdout w xs h m
Hrel :
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
stream_atlibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hopen :
stream_openlibc_stream_modelrep requests wide m′ w′ output_targetapi libc_stdout w xs info′
Hid :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
Hdelegate :
stream_delegateslibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs born m′ w′
Htrace :
trace = [ ] ∧ acceptedactions = [ ] ∨ trace = StreamBytesstream_identifierinfo acceptedactions
Haux :
stream_aux_framelibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs m′
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hra′ :
roots_apartcontract_writesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w h m′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep output_targetapi libc_stdout w xs 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
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
roots_apartlibc_stream_writesw output_targetapi libc_stdout w xs h m
Hrel :
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
stream_atlibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hopen :
stream_openlibc_stream_modelrep requests wide m′ w′ output_targetapi libc_stdout w xs info′
Hid :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
Hdelegate :
stream_delegateslibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs born m′ w′
Htrace :
trace = [ ] ∧ acceptedactions = [ ] ∨ trace = StreamBytesstream_identifierinfo acceptedactions
Haux :
stream_aux_framelibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs m′
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hra′ :
roots_apartcontract_writesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w h m′
⊢
live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep output_targetapi libc_stdout w xs 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
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
roots_apartlibc_stream_writesw output_targetapi libc_stdout w xs h m
Hrel :
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
stream_atlibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hopen :
stream_openlibc_stream_modelrep requests wide m′ w′ output_targetapi libc_stdout w xs info′
Hid :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
Hdelegate :
stream_delegateslibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs born m′ w′
Htrace :
trace = [ ] ∧ acceptedactions = [ ] ∨ trace = StreamBytesstream_identifierinfo acceptedactions
Haux :
stream_aux_framelibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs m′
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hra′ :
roots_apartcontract_writesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w h m′
⊢
R.readys′ m′ ∧ libc_stream_wirep output_targetapi libc_stdout w xs 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
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
roots_apartlibc_stream_writesw output_targetapi libc_stdout w xs h m
Hrel :
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
stream_atlibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hopen :
stream_openlibc_stream_modelrep requests wide m′ w′ output_targetapi libc_stdout w xs info′
Hid :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
Hdelegate :
stream_delegateslibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs born m′ w′
Htrace :
trace = [ ] ∧ acceptedactions = [ ] ∨ trace = StreamBytesstream_identifierinfo acceptedactions
Haux :
stream_aux_framelibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs m′
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hra′ :
roots_apartcontract_writesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w h m′
⊢
libc_stream_wirep output_targetapi libc_stdout w xs m′ w′ h
split ; exact proj1Hopen |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
roots_apartlibc_stream_writesw output_targetapi libc_stdout w xs h m
Hrel :
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hinfo :
stream_atlibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs = Someinfo
Htext :
output_textapi m xs bytes
Hbytes :
bytes = acceptedactions ++ tail
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Hopen :
stream_openlibc_stream_modelrep requests wide m′ w′ output_targetapi libc_stdout w xs info′
Hid :
stream_identifierinfo′ = stream_identifierinfo
Hframe :
stream_framelibc_stream_modelrep requests wide output_targetapi libc_stdout w xs w w′
Hdelegate :
stream_delegateslibc_stream_modelrep requests wide w output_targetapi libc_stdout w xs born m′ w′
Htrace :
trace = [ ] ∧ acceptedactions = [ ] ∨ trace = StreamBytesstream_identifierinfo acceptedactions
Haux :
stream_aux_framelibc_stream_modelrep requests wide m w output_targetapi libc_stdout w xs m′
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hra′ :
roots_apartcontract_writesoutput_contractapi libc_stream_modelrep requests wide libc_stdout xs m w h m′
⊢
roots_apartlibc_stream_writesw′ output_targetapi libc_stdout w xs h m′ ∧ ids_apartlibc_stream_releasesw′ output_targetapi libc_stdout w xs h
exact stream_delegates_apartlibc_world libc_stream_modelrep requests wide w _ born m′ w′ h Hdelegate Hra′ Hrel Hb Hd′
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide api r args xs p s m w trace ending s′ m′ w′ h → Hcall Ha Hd Hr Hready & Hra & Hrel
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & Hp
destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as Hr′ _
destruct LG.prefix_agrees_ _ _ _ _ _ _ _ _ _ _ h Hp Hr Hd Ha Hra ltac:intros base l v as Ha′ & Hd′ & Hb & Hra′
destruct Hp as _ & info & info′ & bytes & actions & tail & Hinfo & Htext & Hbytes & Hrun & Hopen & Hid & Hframe & Hdelegate & Htrace & Haux
split ; exact Ha′ |
split ; exact Hd′ |
split ; exact Hr′ |
split ; exact proj1Hopen |
exact stream_delegates_apartlibc_world libc_stream_modelrep requests wide w _ born m′ w′ h Hdelegate Hra′ Hrel Hb Hd′
The result part of HelloVersion's frame is obtained independently from the normal contract result; no output-success premise is used.
∀ rep requests wide api r args xs p s m w trace values s′ m′ w′ h
p = output_targetapi libc_stdout w xs
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace CallReturnvalues s′ m′ w′
agreesm h
R.readys m
libc_stream_wirep p m w h
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h ∧ ∃n, values = WIntn ∧ 0 ≤ n < 2 ^ 32
Explore proof 7 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop api : narrow_api r : call_result args : listarg xs : listword p : ptr s : R.state m : mem w : libc_world trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world h : gmappiece pval, p = output_targetapi libc_stdout w xs → M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace CallReturnvalues s′ m′ w′ → agreesm h → live_disjointm → R.readys m → libc_stream_wirep p m w h → agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
intros
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
p :
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
p = output_targetapi libc_stdout w xs
H0 :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace CallReturnvalues s′ m′ w′
H1 :
agreesm h
H2 :
H3 :
R.readys m
H4 :
libc_stream_wirep p m w h
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
destruct output_frame_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H H0 H1 H2 H3 H4 as Ha & Hd & Hr & Hw
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
p :
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
p = output_targetapi libc_stdout w xs
H0 :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace CallReturnvalues s′ m′ w′
H1 :
agreesm h
H2 :
H3 :
R.readys m
H4 :
libc_stream_wirep p m w h
Ha :
agreesm′ h
Hd :
Hr :
R.readys′ m′
Hw :
libc_stream_wirep p m′ w′ h
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
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
api :
r :
args :
listarg
xs :
listword
p :
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
p = output_targetapi libc_stdout w xs
H0 :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace CallReturnvalues s′ m′ w′
H1 :
agreesm h
H2 :
H3 :
R.readys m
H4 :
libc_stream_wirep p m w h
Ha :
agreesm′ h
Hd :
Hr :
R.readys′ m′
Hw :
libc_stream_wirep p m′ w′ h
⊢
live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
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
api :
r :
args :
listarg
xs :
listword
p :
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
p = output_targetapi libc_stdout w xs
H0 :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace CallReturnvalues s′ m′ w′
H1 :
agreesm h
H2 :
H3 :
R.readys m
H4 :
libc_stream_wirep p m w h
Ha :
agreesm′ h
Hd :
Hr :
R.readys′ m′
Hw :
libc_stream_wirep p m′ w′ h
⊢
R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
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
api :
r :
args :
listarg
xs :
listword
p :
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
p = output_targetapi libc_stdout w xs
H0 :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace CallReturnvalues s′ m′ w′
H1 :
agreesm h
H2 :
H3 :
R.readys m
H4 :
libc_stream_wirep p m w h
Ha :
agreesm′ h
Hd :
Hr :
R.readys′ m′
Hw :
libc_stream_wirep p m′ w′ h
⊢
libc_stream_wirep p m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
split ; exact Hw |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
api :
r :
args :
listarg
xs :
listword
p :
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
p = output_targetapi libc_stdout w xs
H0 :
M.E.invokeoutput_contractapi libc_stream_modelrep requests wide libc_stdout r args xs s m w trace CallReturnvalues s′ m′ w′
H1 :
agreesm h
H2 :
H3 :
R.readys m
H4 :
libc_stream_wirep p m w h
Ha :
agreesm′ h
Hd :
Hr :
R.readys′ m′
Hw :
libc_stream_wirep p m′ w′ h
⊢
∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
eapply S.output_returned ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
destruct output_frame_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H H0 H1 H2 H3 H4 as Ha & Hd & Hr & Hw
split ; exact Ha |
split ; exact Hd |
split ; exact Hr |
split ; exact Hw |
eapply S.output_returned ; eauto
Close may consume its own heaps, but never program-owned identities. Endpoint readiness and retired authority come from the close prefix, including on EOF and resource stops.
∀ rep requests wide r args p s m w trace ending s′ m′ w′ h
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_stream_wirep p m w h
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h
Explore proof 11 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop r : call_result args : listarg p : ptr s : R.state m : mem w : libc_world trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world h : gmappiece pval, M.E.invokefclose_contractlibc_stream_modelrep requests wide r args WPtrp s m w trace ending s′ m′ w′ → agreesm h → live_disjointm → R.readys m → libc_stream_wirep p m w h → agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h
intros rep requests wide r args p s m w trace ending s′ m′ w′ h Hcall Ha Hd Hr Hready & Hra & Hrel
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokefclose_contractlibc_stream_modelrep requests wide r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
Hrel :
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p 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
r :
args :
listarg
p :
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokefclose_contractlibc_stream_modelrep requests wide r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
Hrel :
born :
listZ
Hp :
M.E.prefixfclose_contractlibc_stream_modelrep requests wide WPtrp s m w born trace s′ m′ w′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h
destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as Hr′ _
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokefclose_contractlibc_stream_modelrep requests wide r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
Hrel :
born :
listZ
Hp :
M.E.prefixfclose_contractlibc_stream_modelrep requests wide WPtrp s m w born trace s′ m′ w′
Hr′ :
R.readys′ m′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h
destruct LG.prefix_agrees_ _ _ _ _ _ _ _ _ _ _ h Hp Hr Hd Ha Hra Hrel as Ha′ & Hd′ & Hb & Hra′
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokefclose_contractlibc_stream_modelrep requests wide r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
Hrel :
born :
listZ
Hp :
M.E.prefixfclose_contractlibc_stream_modelrep requests wide WPtrp s m w born trace s′ m′ w′
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hra′ :
roots_apartcontract_writesfclose_contractlibc_stream_modelrep requests wide WPtrp m w h m′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h
destruct Hp as _ & p0 & info & final & Hxs & Hinfo & Hsettled & Hstate & Hready′ & Hframe & Hdelegate & Htrace & Hclosed & Haux
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokefclose_contractlibc_stream_modelrep requests wide r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
Hrel :
born :
listZ
p0 :
info :
final :
Hinfo :
stream_atlibc_stream_modelrep requests wide w p0 = Someinfo
Hsettled :
stream_settlementlibc_stream_modelrep requests wide w p0 stream_protocolinfo final false
Hstate :
stream_state_atlibc_stream_modelrep requests wide w′ p0 = final
Hready′ :
stream_replibc_stream_modelrep requests wide m′ w′
Hframe :
stream_framelibc_stream_modelrep requests wide p0 w w′
Hdelegate :
stream_delegateslibc_stream_modelrep requests wide w p0 born m′ w′
Htrace :
trace = [ ]
Hclosed :
stream_atlibc_stream_modelrep requests wide w′ p0 = None ∨ ∃info′ : stream_info, stream_atlibc_stream_modelrep requests wide w′ p0 = Someinfo′ ∧ stream_protocolinfo′ = final
Haux :
stream_aux_framelibc_stream_modelrep requests wide m w p0 m′
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hra′ :
roots_apartcontract_writesfclose_contractlibc_stream_modelrep requests wide WPtrp m w h m′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h
injection Hxs as ←
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokefclose_contractlibc_stream_modelrep requests wide r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
Hrel :
born :
listZ
info :
final :
Hstate :
stream_state_atlibc_stream_modelrep requests wide w′ p = final
Hsettled :
stream_settlementlibc_stream_modelrep requests wide w p stream_protocolinfo final false
Hinfo :
stream_atlibc_stream_modelrep requests wide w p = Someinfo
Hready′ :
stream_replibc_stream_modelrep requests wide m′ w′
Hdelegate :
stream_delegateslibc_stream_modelrep requests wide w p born m′ w′
Hframe :
stream_framelibc_stream_modelrep requests wide p w w′
Htrace :
trace = [ ]
Haux :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hclosed :
stream_atlibc_stream_modelrep requests wide w′ p = None ∨ ∃info′ : stream_info, stream_atlibc_stream_modelrep requests wide w′ p = Someinfo′ ∧ stream_protocolinfo′ = final
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hra′ :
roots_apartcontract_writesfclose_contractlibc_stream_modelrep requests wide WPtrp m w h m′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p 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
r :
args :
listarg
p :
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokefclose_contractlibc_stream_modelrep requests wide r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
Hrel :
born :
listZ
info :
final :
Hstate :
stream_state_atlibc_stream_modelrep requests wide w′ p = final
Hsettled :
stream_settlementlibc_stream_modelrep requests wide w p stream_protocolinfo final false
Hinfo :
stream_atlibc_stream_modelrep requests wide w p = Someinfo
Hready′ :
stream_replibc_stream_modelrep requests wide m′ w′
Hdelegate :
stream_delegateslibc_stream_modelrep requests wide w p born m′ w′
Hframe :
stream_framelibc_stream_modelrep requests wide p w w′
Htrace :
trace = [ ]
Haux :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hclosed :
stream_atlibc_stream_modelrep requests wide w′ p = None ∨ ∃info′ : stream_info, stream_atlibc_stream_modelrep requests wide w′ p = Someinfo′ ∧ stream_protocolinfo′ = final
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hra′ :
roots_apartcontract_writesfclose_contractlibc_stream_modelrep requests wide WPtrp m w h m′
⊢
live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p 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
r :
args :
listarg
p :
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokefclose_contractlibc_stream_modelrep requests wide r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
Hrel :
born :
listZ
info :
final :
Hstate :
stream_state_atlibc_stream_modelrep requests wide w′ p = final
Hsettled :
stream_settlementlibc_stream_modelrep requests wide w p stream_protocolinfo final false
Hinfo :
stream_atlibc_stream_modelrep requests wide w p = Someinfo
Hready′ :
stream_replibc_stream_modelrep requests wide m′ w′
Hdelegate :
stream_delegateslibc_stream_modelrep requests wide w p born m′ w′
Hframe :
stream_framelibc_stream_modelrep requests wide p w w′
Htrace :
trace = [ ]
Haux :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hclosed :
stream_atlibc_stream_modelrep requests wide w′ p = None ∨ ∃info′ : stream_info, stream_atlibc_stream_modelrep requests wide w′ p = Someinfo′ ∧ stream_protocolinfo′ = final
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hra′ :
roots_apartcontract_writesfclose_contractlibc_stream_modelrep requests wide WPtrp m w h m′
⊢
R.readys′ m′ ∧ libc_stream_wirep p 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
r :
args :
listarg
p :
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokefclose_contractlibc_stream_modelrep requests wide r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
Hrel :
born :
listZ
info :
final :
Hstate :
stream_state_atlibc_stream_modelrep requests wide w′ p = final
Hsettled :
stream_settlementlibc_stream_modelrep requests wide w p stream_protocolinfo final false
Hinfo :
stream_atlibc_stream_modelrep requests wide w p = Someinfo
Hready′ :
stream_replibc_stream_modelrep requests wide m′ w′
Hdelegate :
stream_delegateslibc_stream_modelrep requests wide w p born m′ w′
Hframe :
stream_framelibc_stream_modelrep requests wide p w w′
Htrace :
trace = [ ]
Haux :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hclosed :
stream_atlibc_stream_modelrep requests wide w′ p = None ∨ ∃info′ : stream_info, stream_atlibc_stream_modelrep requests wide w′ p = Someinfo′ ∧ stream_protocolinfo′ = final
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hra′ :
roots_apartcontract_writesfclose_contractlibc_stream_modelrep requests wide WPtrp m w h m′
⊢
libc_stream_wirep p m′ w′ h
split ; exact Hready′ |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
r :
args :
listarg
p :
s :
R.state
m :
w :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcall :
M.E.invokefclose_contractlibc_stream_modelrep requests wide r args WPtrp s m w trace ending s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hready :
libc_stream_readyrep m w
Hra :
Hrel :
born :
listZ
info :
final :
Hstate :
stream_state_atlibc_stream_modelrep requests wide w′ p = final
Hsettled :
stream_settlementlibc_stream_modelrep requests wide w p stream_protocolinfo final false
Hinfo :
stream_atlibc_stream_modelrep requests wide w p = Someinfo
Hready′ :
stream_replibc_stream_modelrep requests wide m′ w′
Hdelegate :
stream_delegateslibc_stream_modelrep requests wide w p born m′ w′
Hframe :
stream_framelibc_stream_modelrep requests wide p w w′
Htrace :
trace = [ ]
Haux :
stream_aux_framelibc_stream_modelrep requests wide m w p m′
Hclosed :
stream_atlibc_stream_modelrep requests wide w′ p = None ∨ ∃info′ : stream_info, stream_atlibc_stream_modelrep requests wide w′ p = Someinfo′ ∧ stream_protocolinfo′ = final
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hra′ :
roots_apartcontract_writesfclose_contractlibc_stream_modelrep requests wide WPtrp m w h m′
⊢
roots_apartlibc_stream_writesw′ p h m′ ∧ ids_apartlibc_stream_releasesw′ p h
exact stream_delegates_apartlibc_world libc_stream_modelrep requests wide w p born m′ w′ h Hdelegate Hra′ Hrel Hb Hd′
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide r args p s m w trace ending s′ m′ w′ h Hcall Ha Hd Hr Hready & Hra & Hrel
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & Hp
destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as Hr′ _
destruct LG.prefix_agrees_ _ _ _ _ _ _ _ _ _ _ h Hp Hr Hd Ha Hra Hrel as Ha′ & Hd′ & Hb & Hra′
destruct Hp as _ & p0 & info & final & Hxs & Hinfo & Hsettled & Hstate & Hready′ & Hframe & Hdelegate & Htrace & Hclosed & Haux
injection Hxs as ←
split ; exact Ha′ |
split ; exact Hd′ |
split ; exact Hr′ |
split ; exact Hready′ |
exact stream_delegates_apartlibc_world libc_stream_modelrep requests wide w p born m′ w′ h Hdelegate Hra′ Hrel Hb Hd′
Both pure queries can lock/mutate private metadata; their actual effects, rather than an assumed unchanged memory, carry the frame.
∀ rep requests wide spec r args p 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_stream_wirep p m w h
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h
Explore proof 3 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop spec : contractlibc_world r : call_result args : listarg p : ptr 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_stream_wirep p m w h → agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h
intros rep requests wide spec r args p s m w trace ending s′ m′ w′ h Hspec Hcall Ha Hd Hr Hready & Hra & Hrel
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
spec :
r :
args :
listarg
p :
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
Hready :
libc_stream_readyrep m w
Hra :
Hrel :
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p 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
r :
args :
listarg
p :
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
Hready :
libc_stream_readyrep m w
Hra :
Hrel :
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p 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
r :
args :
listarg
p :
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
Hready :
libc_stream_readyrep m w
Hra :
Hrel :
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ libc_stream_wirep p m′ w′ h
all: destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & Hp ; destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as Hr′ _ ; destruct LG.prefix_agrees_ _ _ _ _ _ _ _ _ _ _ h Hp Hr Hd Ha Hra ltac:intros base l v as Ha′ & Hd′ & Hb & Hra′ ; destruct Hp as _ & p0 & info & Hxs & Hinfo & Hopen & Hframe & Hdelegate & Htrace & Haux ; injection Hxs as ← ; split ; exact Ha' | ; split ; exact Hd' | ; split ; exact Hr' | ; split ; exact proj1Hopen | ; exact stream_delegates_apartlibc_world libc_stream_modelrep requests wide w p born m′ w′ h Hdelegate Hra' Hrel Hb Hd'
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide spec r args p s m w trace ending s′ m′ w′ h Hspec Hcall Ha Hd Hr Hready & Hra & Hrel
destruct Hspec as → | →
all: destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & Hp ; destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as Hr′ _ ; destruct LG.prefix_agrees_ _ _ _ _ _ _ _ _ _ _ h Hp Hr Hd Ha Hra ltac:intros base l v as Ha′ & Hd′ & Hb & Hra′ ; destruct Hp as _ & p0 & info & Hxs & Hinfo & Hopen & Hframe & Hdelegate & Htrace & Haux ; injection Hxs as ← ; split ; exact Ha' | ; split ; exact Hd' | ; split ; exact Hr' | ; split ; exact proj1Hopen | ; exact stream_delegates_apartlibc_world libc_stream_modelrep requests wide w p born m′ w′ h Hdelegate Hra' Hrel Hb Hd'