Filnix wiki

all_agreem stream_psd pending fifo

Explore proof 3 tactics

Initial goal

⊢

∀m : mem d : stream_token pending : Z fifo : listZ, live_atm token_based token_regiond → all_agreem stream_psd pending fifo

intros

m :

d :

pending :

fifo :

listZ

H :

⊢

all_agreem stream_psd pending fifo

split ; exact H |

m :

d :

pending :

fifo :

listZ

H :

⊢

all_agreem PNametoken_keyd, VStreamtoken_handled Somepending, fifo

split ; exact I

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros

split ; exact H |

split ; exact I

72Lemma closed_ps_agree

∀ m d

all_agreem closed_psd

Explore proof 3 tactics

Initial goal

⊢

∀m : mem d : stream_token, live_atm token_based token_regiond → all_agreem closed_psd

intros

m :

d :

H :

⊢

all_agreem closed_psd

split ; exact H |

m :

d :

H :

⊢

all_agreem PNametoken_keyd, VStreamtoken_handled None

split ; exact I

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros

split ; exact H |

split ; exact I

76Lemma stream_open_current

∀ d w h pending fifo

∀l v, l, v ∈ stream_psd pending fifo → h !! l = Somev

∃info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo

Explore proof 8 tactics

Initial goal

⊢

∀d : stream_token w : libc_world h : gmappiece pval pending : Z fifo : listZ, stream_currentd w h → ∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev → ∃info : stream_info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo

intros d w h pending fifo Hcurrent Howned

d :

w :

h :

gmappiece pval

pending :

fifo :

listZ

Hcurrent :

Howned :

∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev

⊢

∃info : stream_info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo

assert Hl : h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo

2 open

d :

w :

h :

gmappiece pval

pending :

fifo :

listZ

Hcurrent :

Howned :

∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev

⊢

h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo

focused goal

d :

w :

h :

gmappiece pval

pending :

fifo :

listZ

Hcurrent :

Howned :

∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev

Hl :

h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo

⊢

∃info : stream_info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo

{apply Howned

2 open

d :

w :

h :

gmappiece pval

pending :

fifo :

listZ

Hcurrent :

Howned :

∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev

⊢

PNametoken_keyd, VStreamtoken_handled Somepending, fifo ∈ stream_psd pending fifo

deferred goal

d :

w :

h :

gmappiece pval

pending :

fifo :

listZ

Hcurrent :

Howned :

∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev

Hl :

h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo

⊢

∃info : stream_info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo

unfold stream_ps

2 open

d :

w :

h :

gmappiece pval

pending :

fifo :

listZ

Hcurrent :

Howned :

∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev

⊢

PNametoken_keyd, VStreamtoken_handled Somepending, fifo ∈ PLivetoken_based, VLivetoken_regiond; PNametoken_keyd, VStreamtoken_handled Somepending, fifo

deferred goal

d :

w :

h :

gmappiece pval

pending :

fifo :

listZ

Hcurrent :

Howned :

∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev

Hl :

h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo

⊢

∃info : stream_info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo

set_solver

deferred goal

d :

w :

h :

gmappiece pval

pending :

fifo :

listZ

Hcurrent :

Howned :

∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev

Hl :

h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo

⊢

∃info : stream_info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo

unfold stream_current in Hcurrent

d :

w :

h :

gmappiece pval

pending :

fifo :

listZ

Hcurrent :

match h !! PNametoken_keyd with

SomeVStreamp snapshot

⇒

p = token_handled ∧ stream_observationw p snapshot

None

⇒

True

⇒

False

Howned :

∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev

Hl :

h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo

⊢

∃info : stream_info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo

rewrite Hl in Hcurrent

d :

w :

h :

gmappiece pval

pending :

fifo :

listZ

Howned :

∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev

Hl :

h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo

Hcurrent :

token_handled = token_handled ∧ stream_observationw token_handled Somepending, fifo

⊢

∃info : stream_info, libc_stream_atw token_handled = Someinfo ∧ stream_pendinginfo = pending ∧ outstandingstream_protocolinfo = fifo

exact proj2Hcurrent

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros d w h pending fifo Hcurrent Howned

assert Hl : h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo

{apply Howned

unfold stream_ps

set_solver

unfold stream_current in Hcurrent

rewrite Hl in Hcurrent

exact proj2Hcurrent

88Lemma stream_closed_current

∀ d w h

∀l v, l, v ∈ closed_psd → h !! l = Somev

libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]

Explore proof 8 tactics

Initial goal

⊢

∀d : stream_token w : libc_world h : gmappiece pval, stream_currentd w h → ∀l : piece v : pval, l, v ∈ closed_psd → h !! l = Somev → libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]

intros d w h Hcurrent Howned

d :

w :

h :

gmappiece pval

Hcurrent :

Howned :

∀l : piece v : pval, l, v ∈ closed_psd → h !! l = Somev

⊢

libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]

assert Hl : h !! PNametoken_keyd = SomeVStreamtoken_handled None

2 open

d :

w :

h :

gmappiece pval

Hcurrent :

Howned :

∀l : piece v : pval, l, v ∈ closed_psd → h !! l = Somev

⊢

h !! PNametoken_keyd = SomeVStreamtoken_handled None

focused goal

d :

w :

h :

gmappiece pval

Hcurrent :

Howned :

∀l : piece v : pval, l, v ∈ closed_psd → h !! l = Somev

Hl :

h !! PNametoken_keyd = SomeVStreamtoken_handled None

⊢

libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]

{apply Howned

2 open

d :

w :

h :

gmappiece pval

Hcurrent :

Howned :

∀l : piece v : pval, l, v ∈ closed_psd → h !! l = Somev

⊢

PNametoken_keyd, VStreamtoken_handled None ∈ closed_psd

deferred goal

d :

w :

h :

gmappiece pval

Hcurrent :

Howned :

∀l : piece v : pval, l, v ∈ closed_psd → h !! l = Somev

Hl :

h !! PNametoken_keyd = SomeVStreamtoken_handled None

⊢

libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]

unfold closed_ps

2 open

d :

w :

h :

gmappiece pval

Hcurrent :

Howned :

∀l : piece v : pval, l, v ∈ closed_psd → h !! l = Somev

⊢

PNametoken_keyd, VStreamtoken_handled None ∈ PLivetoken_based, VLivetoken_regiond; PNametoken_keyd, VStreamtoken_handled None

deferred goal

d :

w :

h :

gmappiece pval

Hcurrent :

Howned :

∀l : piece v : pval, l, v ∈ closed_psd → h !! l = Somev

Hl :

h !! PNametoken_keyd = SomeVStreamtoken_handled None

⊢

libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]

set_solver

deferred goal

d :

w :

h :

gmappiece pval

Hcurrent :

Howned :

∀l : piece v : pval, l, v ∈ closed_psd → h !! l = Somev

Hl :

h !! PNametoken_keyd = SomeVStreamtoken_handled None

⊢

libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]

unfold stream_current in Hcurrent

d :

w :

h :

gmappiece pval

Hcurrent :

match h !! PNametoken_keyd with

SomeVStreamp snapshot

⇒

p = token_handled ∧ stream_observationw p snapshot

None

⇒

True

⇒

False

Howned :

∀l : piece v : pval, l, v ∈ closed_psd → h !! l = Somev

Hl :

h !! PNametoken_keyd = SomeVStreamtoken_handled None

⊢

libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]

rewrite Hl in Hcurrent

d :

w :

h :

gmappiece pval

Howned :

∀l : piece v : pval, l, v ∈ closed_psd → h !! l = Somev

Hl :

h !! PNametoken_keyd = SomeVStreamtoken_handled None

Hcurrent :

token_handled = token_handled ∧ stream_observationw token_handled None

⊢

libc_stream_atw token_handled = None ∧ outstandinglibc_stream_statew token_handled = [ ]

exact proj2Hcurrent

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros d w h Hcurrent Howned

assert Hl : h !! PNametoken_keyd = SomeVStreamtoken_handled None

{apply Howned

unfold closed_ps

set_solver

unfold stream_current in Hcurrent

rewrite Hl in Hcurrent

exact proj2Hcurrent

99Section snapshot_allocation

100Context `{!gen_heapGSpiece pval Σ}

Callback entry allocates the reserved snapshot key, while retaining an already owned life piece. Neither the life nor a fresh ghost resource can be fabricated by the pure interpretation.

105Lemma stream_snapshot_alloc

∀ d pending fifo w h

h !! PNametoken_keyd = None

stream_observationw token_handled Somepending, fifo

gen_heap_interph ∗ ptsPLivetoken_based, VLivetoken_regiond ⇛ gen_heap_interp<[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h ∗ ptsstream_psd pending fifo ∗ ⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝

Explore proof 13 tactics

Initial goal

Σ :

gFunctors

gen_heapGS₀ :

gen_heapGSpiece pval Σ

d :

pending :

fifo :

listZ

w :

h :

gmappiece pval

⊢

h !! PNametoken_keyd = None → stream_observationw token_handled Somepending, fifo → gen_heap_interph ∗ ptsPLivetoken_based, VLivetoken_regiond ⇛ gen_heap_interp<[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h ∗ ptsstream_psd pending fifo ∗ ⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝

intros Hfresh Hobs

Σ :

gFunctors

gen_heapGS₀ :

gen_heapGSpiece pval Σ

d :

pending :

fifo :

listZ

w :

h :

gmappiece pval

Hfresh :

h !! PNametoken_keyd = None

Hobs :

stream_observationw token_handled Somepending, fifo

⊢

iIntros [Hh Hlife]

Σ :

gFunctors

gen_heapGS₀ :

gen_heapGSpiece pval Σ

d :

pending :

fifo :

listZ

w :

h :

gmappiece pval

Hfresh :

h !! PNametoken_keyd = None

Hobs :

stream_observationw token_handled Somepending, fifo

Hh :

gen_heap_interph

Hlife :

∗

|⇛ gen_heap_interp<[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h ∗ ptsstream_psd pending fifo ∗ ⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝

iMod gen_heap_alloc_ PNametoken_keyd VStreamtoken_handled Somepending, fifo with Hh as (Hh & Hname & _) ; exact Hfresh |

Σ :

gFunctors

gen_heapGS₀ :

gen_heapGSpiece pval Σ

d :

pending :

fifo :

listZ

w :

h :

gmappiece pval

Hfresh :

h !! PNametoken_keyd = None

Hobs :

stream_observationw token_handled Somepending, fifo

Hlife :

Hh :

gen_heap_interp<[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h

Hname :

pointstoPNametoken_keyd DfracOwn1 VStreamtoken_handled Somepending, fifo

∗

iModIntro

Σ :

gFunctors

gen_heapGS₀ :

gen_heapGSpiece pval Σ

d :

pending :

fifo :

listZ

w :

h :

gmappiece pval

Hfresh :

h !! PNametoken_keyd = None

Hobs :

stream_observationw token_handled Somepending, fifo

Hlife :

Hh :

gen_heap_interp<[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h

Hname :

pointstoPNametoken_keyd DfracOwn1 VStreamtoken_handled Somepending, fifo

∗

gen_heap_interp<[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h ∗ ptsstream_psd pending fifo ∗ ⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝

iSplitL Hh ; iExact Hh |

Σ :

gFunctors

gen_heapGS₀ :

gen_heapGSpiece pval Σ

d :

pending :

fifo :

listZ

w :

h :

gmappiece pval

Hfresh :

h !! PNametoken_keyd = None

Hobs :

stream_observationw token_handled Somepending, fifo

Hlife :

Hname :

pointstoPNametoken_keyd DfracOwn1 VStreamtoken_handled Somepending, fifo

∗

ptsstream_psd pending fifo ∗ ⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝

iSplitL Hlife Hname

2 open

Σ :

gFunctors

gen_heapGS₀ :

gen_heapGSpiece pval Σ

d :

pending :

fifo :

listZ

w :

h :

gmappiece pval

Hfresh :

h !! PNametoken_keyd = None

Hobs :

stream_observationw token_handled Somepending, fifo

Hlife :

Hname :

pointstoPNametoken_keyd DfracOwn1 VStreamtoken_handled Somepending, fifo

∗

ptsstream_psd pending fifo

focused goal

Σ :

gFunctors

gen_heapGS₀ :

gen_heapGSpiece pval Σ

d :

pending :

fifo :

listZ

w :

h :

gmappiece pval

Hfresh :

h !! PNametoken_keyd = None

Hobs :

stream_observationw token_handled Somepending, fifo

∗

⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝

–rewrite / stream_ps / pts /=

2 open

Σ :

gFunctors

gen_heapGS₀ :

gen_heapGSpiece pval Σ

d :

pending :

fifo :

listZ

w :

h :

gmappiece pval

Hfresh :

h !! PNametoken_keyd = None

Hobs :

stream_observationw token_handled Somepending, fifo

Hlife :

pointstoPLivetoken_based DfracOwn1 VLivetoken_regiond ∗ emp

Hname :

pointstoPNametoken_keyd DfracOwn1 VStreamtoken_handled Somepending, fifo

∗

pointstoPLivetoken_based DfracOwn1 VLivetoken_regiond ∗ pointstoPNametoken_keyd DfracOwn1 VStreamtoken_handled Somepending, fifo ∗ emp

deferred goal

Σ :

gFunctors

gen_heapGS₀ :

gen_heapGSpiece pval Σ

d :

pending :

fifo :

listZ

w :

h :

gmappiece pval

Hfresh :

h !! PNametoken_keyd = None

Hobs :

stream_observationw token_handled Somepending, fifo

∗

⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝

iDestruct Hlife as [Hlife _]

2 open

Σ :

gFunctors

gen_heapGS₀ :

gen_heapGSpiece pval Σ

d :

pending :

fifo :

listZ

w :

h :

gmappiece pval

Hfresh :

h !! PNametoken_keyd = None

Hobs :

stream_observationw token_handled Somepending, fifo

Hlife :

pointstoPLivetoken_based DfracOwn1 VLivetoken_regiond

Hname :

pointstoPNametoken_keyd DfracOwn1 VStreamtoken_handled Somepending, fifo

∗

pointstoPLivetoken_based DfracOwn1 VLivetoken_regiond ∗ pointstoPNametoken_keyd DfracOwn1 VStreamtoken_handled Somepending, fifo ∗ emp

deferred goal

Σ :

gFunctors

gen_heapGS₀ :

gen_heapGSpiece pval Σ

d :

pending :

fifo :

listZ

w :

h :

gmappiece pval

Hfresh :

h !! PNametoken_keyd = None

Hobs :

stream_observationw token_handled Somepending, fifo

∗

⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝

iFrame

deferred goal

Σ :

gFunctors

gen_heapGS₀ :

gen_heapGSpiece pval Σ

d :

pending :

fifo :

listZ

w :

h :

gmappiece pval

Hfresh :

h !! PNametoken_keyd = None

Hobs :

stream_observationw token_handled Somepending, fifo

∗

⌜stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h⌝

–iPureIntro

Σ :

gFunctors

gen_heapGS₀ :

gen_heapGSpiece pval Σ

d :

pending :

fifo :

listZ

w :

h :

gmappiece pval

Hfresh :

h !! PNametoken_keyd = None

Hobs :

stream_observationw token_handled Somepending, fifo

⊢

stream_currentd w <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h

unfold stream_current

Σ :

gFunctors

gen_heapGS₀ :

gen_heapGSpiece pval Σ

d :

pending :

fifo :

listZ

w :

h :

gmappiece pval

Hfresh :

h !! PNametoken_keyd = None

Hobs :

stream_observationw token_handled Somepending, fifo

⊢

match <[PNametoken_keyd ≔ VStreamtoken_handled Somepending, fifo]>h !! PNametoken_keyd with

SomeVStreamp snapshot

⇒

p = token_handled ∧ stream_observationw p snapshot

None

⇒

True

⇒

False

rewrite lookup_insert_eq

Σ :

gFunctors

gen_heapGS₀ :

gen_heapGSpiece pval Σ

d :

pending :

fifo :

listZ

w :

h :

gmappiece pval

Hfresh :

h !! PNametoken_keyd = None

Hobs :

stream_observationw token_handled Somepending, fifo

⊢

token_handled = token_handled ∧ stream_observationw token_handled Somepending, fifo

exact conjeq_refl Hobs

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros Hfresh Hobs

iIntros [Hh Hlife]

iMod gen_heap_alloc_ PNametoken_keyd VStreamtoken_handled Somepending, fifo with Hh as (Hh & Hname & _) ; exact Hfresh |

iModIntro

iSplitL Hh ; iExact Hh |

iSplitL Hlife Hname

–rewrite / stream_ps / pts /=

iDestruct Hlife as [Hlife _]

iFrame

–iPureIntro

unfold stream_current

rewrite lookup_insert_eq

exact conjeq_refl Hobs

The other registered stream keeps its observable state and private inventory. Distinct addresses rule out stdout-priority aliasing.

126Lemma stream_other_frame

∀ p q w w′

p = libc_stdoutw ∧ q = libc_stderrw ∨ p = libc_stderrw ∧ q = libc_stdoutw

ptr_addrlibc_stdoutw ≠ ptr_addrlibc_stderrw

libc_stream_framep w w′

libc_file_atw′ q = libc_file_atw q ∧ libc_stream_atw′ q = libc_stream_atw q ∧ libc_stream_statew′ q = libc_stream_statew q

Proof 38 steps Qed

intros p q w w′ Hwhich Hdistinct Hout & Herr & _ & _ & _ & _ & _ & _ & Hother

assert Hne : same_filelibc_stderrw libc_stdoutw = false

{unfold same_file

apply andb_false_iff

left

apply Z.eqb_neq

congruence

destruct Hwhich as → → | → →

–rewrite same_file_refl in Hother

destruct Hother as Hfile & Hopen & Hstate

assert Hlookup : libc_file_atw' libc_stderrw = libc_file_atw libc_stderrw

{unfold libc_file_at

rewrite Hout Herr Hne same_file_refl Hopen Hfile

reflexivity

assert Hprotocol : libc_stream_statew' libc_stderrw = libc_stream_statew libc_stderrw

{unfold libc_stream_state

rewrite Hout Herr Hne same_file_refl Hstate

reflexivity

split ; exact Hlookup |

split ; | exact Hprotocol

unfold libc_stream_at

rewrite Hlookup Hout Hprotocol

reflexivity

–rewrite Hne in Hother

destruct Hother as Hfile & Hopen & Hstate

assert Hlookup : libc_file_atw' libc_stdoutw = libc_file_atw libc_stdoutw

{unfold libc_file_at

rewrite Hout same_file_refl Hopen Hfile

reflexivity

assert Hprotocol : libc_stream_statew' libc_stdoutw = libc_stream_statew libc_stdoutw

{unfold libc_stream_state

rewrite Hout same_file_refl Hstate

reflexivity

split ; exact Hlookup |

split ; | exact Hprotocol

unfold libc_stream_at

rewrite Hlookup Hout Hprotocol

reflexivity

156Module LibcStreamAdapterOn R : Runtime LG : StreamFrameLogicR

157Module M ≔ LG.L.M

158Module T ≔ LibcStreamTokensOn R LG

Query contracts permit no allocation; in particular delegation cannot add a newly born release identity to either FILE.

162Lemma effects_no_alloc

∀ sources roots releases s m born s′ m′ born′

M.E.effectssources roots releases λ_ _ ⇒ False s m born s′ m′ born′

born′ = born

Explore proof 2 tactics

Initial goal

⊢

∀sources roots : listspan releases : listZ s : R.state m : mem born : listZ s′ : R.state m′ : mem born′ : listZ, M.E.effectssources roots releases λ_ _ : Z ⇒ False s m born s′ m′ born′ → born′ = born

intros sources roots releases s m born s′ m′ born′ He

sources, roots :

listspan

releases :

listZ

s :

R.state

m :

born :

listZ

s′ :

R.state

m′ :

born′ :

listZ

He :

M.E.effectssources roots releases λ_ _ : Z ⇒ False s m born s′ m′ born′

⊢

born′ = born

induction He ; reflexivity | exact IHHe | contradiction

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros sources roots releases s m born s′ m′ born′ He

induction He ; reflexivity | exact IHHe | contradiction

Both mirrors and both private-memory frames survive either query. No unchanged-memory premise rules out the native locking writes.

172Theorem query_frame

∀ rep requests wide out err b o d spec r args s m w trace ending s′ m′ w′ h

d = out ∨ d = err

spec = ferror_contractlibc_stream_modelrep requests wide ∨ spec = fpending_contractlibc_stream_modelrep requests wide

M.E.invokespec r args WPtrtoken_handled s m w trace ending s′ m′ w′

agreesm h

live_disjointm

R.readys m

stream_tokens_wirep out err b o m w h

agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ stream_tokens_wirep out err b o m′ w′ h

Proof 71 steps Qed

intros rep requests wide out err b o d spec r args s m w trace ending s′ m′ w′ h Hd Hspec Hcall Ha Hdis Hr Houtwf & Herrwf & Hbase & Hkey & Hout & Herr & Houtcurrent & Herrcurrent & Hprivate

destruct Hprivated Hd as Hselected Hrelease

destruct T.query_framerep requests wide token_baseout token_baseerr token_handled b o spec r args s m w trace ending s' m' w' h Hspec Hcall Ha Hdis Hr Hselected as Ha′ & Hdis′ & Hr′ & Hselected′

split ; exact Ha' |

split ; exact Hdis' |

split ; exact Hr' |

destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & Hp

destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as _ Hpers

assert Hborn : born = [ ]

{destruct Hp as He _

destruct Hspec as → | → ; eapply effects_no_alloc ; exact He

subst born

assert Hprefix : query_prefixlibc_stream_modelrep requests wide WPtrtoken_handled m w [ ] trace m' w'

{destruct Hspec as → | → ; exact proj2Hp

destruct Hprefix as p & info & Hxs & Hinfo & Hopen & Hframe & Hdelegate & _

injection Hxs as ←

cbn [ stream_open stream_at stream_state_at stream_rep libc_stream_model ] in Hinfo , Hopen

assert Hready′ := proj1Hopen

assert Hdistinct : ptr_addrlibc_stdoutw ≠ ptr_addrlibc_stderrw

{destruct proj1Hselected as _ & _ & _ & _ & _ & _ & _ & _ & Hdistinct & _

exact Hdistinct

assert Hother : ∀q, q = out ∨ q = err → q ≠ d → libc_file_atw' token_handleq = libc_file_atw token_handleq ∧ libc_stream_atw' token_handleq = libc_stream_atw token_handleq ∧ libc_stream_statew' token_handleq = libc_stream_statew token_handleq

{intros q Hq Hne

apply stream_other_frame with p := token_handled ; | exact Hdistinct | exact Hframe

destruct Hd as → | → ; destruct Hq as → | → ; try contradiction ; left | right ; split ; congruence

assert Hchoice : ∀q, q = out ∨ q = err → q = d ∨ q ≠ d

{intros q Hq

destruct Hd as → | → ; destruct Hq as → | → ; try left ; reflexivity ; right ; intros Heq ; apply Hbase ; congruence

assert Hviews : ∀q, q = out ∨ q = err → libc_stream_atw' token_handleq = libc_stream_atw token_handleq ∧ libc_stream_statew' token_handleq = libc_stream_statew token_handleq

{intros q Hq

destruct Hchoiceq Hq as [ ->| Hne ]

–split ; rewrite Hinfo ; exact proj1proj2Hopen |

pose proof proj1proj2proj2Hopen as Hprotocol

change stream_protocolinfo = libc_stream_statew' token_handled in Hprotocol

rewrite <- Hprotocol

unfold libc_stream_at in Hinfo

destruct libc_file_atw token_handled ; injection Hinfo as ← ; reflexivity | discriminate

–exact proj2Hotherq Hq Hne

assert Hcurrent : ∀q, q = out ∨ q = err → stream_currentq w' h

{intros q Hq

assert Hc : stream_currentq w h by destruct Hq as → | → ; assumption

destruct Hviewsq Hq as Hlookup Hstate

unfold stream_current in *

destruct h !! PNametoken_keyq as v | ; | exact I

destruct v ; try contradiction

destruct Hc as → Hobs

split ; reflexivity |

unfold stream_observation in *

destruct pending as physical fifo | ; rewrite Hlookup ; exact Hobs | rewrite Hstate ; exact Hobs

split ; exact Houtwf |

split ; exact Herrwf |

split ; exact Hbase |

split ; exact Hkey |

split ; rewrite proj1Hframe ; exact Hout |

split ; rewrite proj1proj2Hframe ; exact Herr |

split ; apply Hcurrent ; left ; reflexivity |

split ; apply Hcurrent ; right ; reflexivity |

intros q Hq

destruct Hchoiceq Hq as [ ->| Hne ]

–split ; exact Hselected' |

intros base l v Hin Hl Hmem

destruct proj2proj2Hdelegate base Hin as Hold | Hnil ; exact Hreleasebase l v Hold Hl Hmem | contradiction

–destruct Hotherq Hq Hne as Hfile _

destruct Hprivateq Hq as Hwi Hrel

assert Hroots : libc_stream_aux_rootsw' token_handleq = libc_stream_aux_rootsw token_handleq by unfold libc_stream_aux_roots ; rewrite Hfile ; reflexivity

assert Hrels : libc_stream_releasesw' token_handleq = libc_stream_releasesw token_handleq by unfold libc_stream_releases ; rewrite Hfile ; reflexivity

split ; | rewrite Hrels ; exact Hrel

+apply stream_data_agrees

exact Ha

+exact proj1proj2proj2proj2Hframe

Only an ordinary return establishes completed closure. Sample all four endpoint errno bytes, update the selected name, and retain the opposite snapshot and both native lives. This is a pure heap frame; updating an owned name in Iris still requires its points-to resource.

256Theorem close_frame

∀ rep requests wide out err b o d r args s m w trace values s′ m′ w′ h xs

d = out ∨ d = err

M.E.invokefclose_contractlibc_stream_modelrep requests wide r args WPtrtoken_handled s m w trace CallReturnvalues s′ m′ w′

agreesm h

live_disjointm

R.readys m

stream_tokens_wirep out err b o m w h

lengthxs = 4%nat

∀l v, l, v ∈ byte_psb o xs → h !! l = Somev

∃ys, lengthys = 4%nat ∧ byte_psb o ys.*1 = byte_psb o xs.*1 ∧ agreesm′ <[PNametoken_keyd ≔ VStreamtoken_handled None]>overwritebyte_psb o ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ stream_tokens_wirep out err b o m′ w′ <[PNametoken_keyd ≔ VStreamtoken_handled None]>overwritebyte_psb o ys h

Proof 122 steps Qed

intros rep requests wide out err b o d r args s m w trace values s′ m′ w′ h xs Hd Hcall Ha Hdis Hr Houtwf & Herrwf & Hbase & Hkey & Hout & Herr & Houtcurrent & Herrcurrent & Hprivate Hlen Howned

destruct Hprivated Hd as Hselected Hrelease

destruct T.close_framerep requests wide token_baseout token_baseerr token_handled b o r args s m w trace CallReturnvalues s' m' w' h xs ltac:rewrite Hout ; exact proj1Houtwf ltac:rewrite Herr ; exact proj1Herrwf Hcall Ha Hdis Hr Hselected Hlen Howned as ys & Hys & Hkeys & Ha′ & Hdis′ & Hr′ & Hselected′

set h₀ := overwritebyte_psb o ys h in *

set h₁ := <[PNametoken_keyd ≔ VStreamtoken_handled None]>h0

assert Hkeys₀ : memory_keys_fromh0 h

{intros l v Hl Hmem

unfold h0 in Hl

destruct lookup_overwrite_ _ _ _ Hl as Hin | _ Hold ; | eauto

assert Hkey₀ : l ∈ byte_psb o xs.*1

{rewrite <- Hkeys

apply list_elem_of_fmap

exists l, v

auto

apply list_elem_of_fmap in Hkey0 as l₀ old & E & Hinold

simpl in E

subst l0

exists old

exact Hownedl old Hinold

assert Hkeys₁ : memory_keys_fromh1 h0

{intros l v Hl Hmem

unfold h1 in Hl

apply lookup_insert_Some in Hl as He Hv | _ Hold ; subst l ; contradiction | eauto

assert Hdata₁ : memory_keys_fromstream_data_heaptoken_baseout token_baseerr h1 stream_data_heaptoken_baseout token_baseerr h0

{intros l v Hl Hmem

apply stream_data_lookup in Hl as Hl & Hno & Hne

destruct Hkeys1l v Hl Hmem as old Hold

exists old

rewrite stream_data_lookup_ne ; assumption

assert Hdata₀ : memory_keys_fromstream_data_heaptoken_baseout token_baseerr h1 stream_data_heaptoken_baseout token_baseerr h

{intros l v Hl Hmem

apply stream_data_lookup in Hl as Hl & Hno & Hne

destruct Hkeys1l v Hl Hmem as old Hold

destruct Hkeys0l old Hold Hmem as entry Hentry

exists entry

rewrite stream_data_lookup_ne ; assumption

exists ys

split ; exact Hys |

split ; exact Hkeys |

split

{intros l v Hl

unfold h1 in Hl

apply lookup_insert_Some in Hl as He Hv | _ Hold ; subst l v ; exact I | exact Ha'l v Hold

split ; exact Hdis' |

split ; exact Hr' |

destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & Hp

destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as _ Hpers

destruct Hp as _ & p & info & final & Hxs & _ & _ & _ & Hready′ & Hframe & _

injection Hxs as ←

destruct T.EL.S.fclose_invocation_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born₀ & p & info₀ & final₀ & n & Hxs & _ & Hsettle & Hstate & _ & Hclosed & _ | why & Hbad & _ ; | discriminate Hbad

injection Hxs as ←

change libc_stream_atw' token_handled = None in Hclosed

assert Hfifo : outstandinglibc_stream_statew' token_handled = [ ]

{change libc_stream_statew' token_handled = final0 in Hstate

rewrite Hstate

eapply stream_settlement_complete ; exact Hsettle

assert Hdistinct : ptr_addrlibc_stdoutw ≠ ptr_addrlibc_stderrw

{destruct proj1Hselected as _ & _ & _ & _ & _ & _ & _ & _ & Hdistinct & _

exact Hdistinct

assert Hchoice : ∀q, q = out ∨ q = err → q = d ∨ q ≠ d

{intros q Hq

destruct Hd as → | → ; destruct Hq as → | → ; try left ; reflexivity ; right ; intros Heq ; apply Hbase ; congruence

{intros q Hq Hne

apply stream_other_frame with p := token_handled ; | exact Hdistinct | exact Hframe

destruct Hd as → | → ; destruct Hq as → | → ; try contradiction ; left | right ; split ; congruence

assert Hcurrent : ∀q, q = out ∨ q = err → stream_currentq w' h1

{intros q Hq

destruct Hchoiceq Hq as [ ->| Hne ]

–unfold stream_current , h1

rewrite lookup_insert_eq

exact conjeq_refl conjHclosed Hfifo

–assert Hkeyne : token_keyd ≠ token_keyq

{destruct Hd as → | → ; destruct Hq as → | → ; congruence

assert Hc : stream_currentq w h by destruct Hq as → | → ; assumption

destruct Hotherq Hq Hne as _ & Hlookup & Hprotocol

unfold stream_current in *

unfold h1

rewrite lookup_insert_ne ; | congruence

unfold h0

rewrite overwrite_out

+destruct h !! PNametoken_keyq as v | ; | exact I

destruct v ; try contradiction

destruct Hc as → Hobs

split ; reflexivity |

unfold stream_observation in *

destruct pending as physical fifo | ; rewrite Hlookup ; exact Hobs | rewrite Hprotocol ; exact Hobs

+rewrite byte_ps_keys

intros Hin

apply list_elem_of_fmap in Hin as i & E & _

discriminate E

split ; exact Houtwf |

split ; exact Herrwf |

split ; exact Hbase |

split ; exact Hkey |

split ; rewrite proj1Hframe ; exact Hout |

split ; rewrite proj1proj2Hframe ; exact Herr |

split ; apply Hcurrent ; left ; reflexivity |

split ; apply Hcurrent ; right ; reflexivity |

intros q Hq

destruct Hchoiceq Hq as [ ->| Hne ]

–split ; eapply errno_wi_heap ; exact Hselected' | exact Hdata1 |

unfold libc_stream_at in Hclosed

unfold libc_stream_releases

destruct libc_file_atw' token_handled ; discriminate Hclosed |

intros base l v Hin

contradiction

–destruct Hotherq Hq Hne as Hfile _

destruct Hprivateq Hq as Hwi Hrel

assert Hroots : libc_stream_aux_rootsw' token_handleq = libc_stream_aux_rootsw token_handleq by unfold libc_stream_aux_roots ; rewrite Hfile ; reflexivity

assert Hrels : libc_stream_releasesw' token_handleq = libc_stream_releasesw token_handleq by unfold libc_stream_releases ; rewrite Hfile ; reflexivity

split

+eapply errno_wi_heap ; | exact Hdata0

∗apply stream_data_agrees

exact Ha

∗exact proj1proj2proj2proj2Hframe

+rewrite Hrels

intros base l v Hin Hl Hmem

destruct Hkeys1l v Hl Hmem as old Hold

destruct Hkeys0l old Hold Hmem as entry Hentry

exact Hrelbase l entry Hin Hentry Hmem

Token ownership plus the current world interpretation admits the concrete libc call; openness is not another consumer assumption.

380Theorem open_admitted

∀ rep requests wide out err b o d pending fifo m w h

d = out ∨ d = err

stream_tokens_wirep out err b o m w h

∀l v, l, v ∈ stream_psd pending fifo → h !! l = Somev

stream_call_prelibc_stream_modelrep requests wide WPtrtoken_handled m w

Explore proof 6 tactics

Initial goal

⊢

∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop out err : stream_token b o : Z d : stream_token pending : Z fifo : listZ m : mem w : libc_world h : gmappiece pval, d = out ∨ d = err → stream_tokens_wirep out err b o m w h → ∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev → stream_call_prelibc_stream_modelrep requests wide WPtrtoken_handled m w

intros rep requests wide out err b o d pending fifo m w h Hd _ & _ & _ & _ & _ & _ & Hout & Herr & Hprivate Howned

rep :

mem → libc_world → Prop

requests :

libc_world → ptr → Z → Z → Prop

wide :

libc_world → ptr → stream_state → stream_state → bool → Prop

out, err :

b, o :

d :

pending :

fifo :

listZ

m :

w :

h :

gmappiece pval

Hd :

d = out ∨ d = err

Hout :

stream_currentout w h

Herr :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

Howned :

∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev

⊢

stream_call_prelibc_stream_modelrep requests wide WPtrtoken_handled m w

pose proof proj1proj1Hprivated Hd as Hready

rep :

mem → libc_world → Prop

requests :

libc_world → ptr → Z → Z → Prop

wide :

libc_world → ptr → stream_state → stream_state → bool → Prop

out, err :

b, o :

d :

pending :

fifo :

listZ

m :

w :

h :

gmappiece pval

Hd :

d = out ∨ d = err

Hout :

stream_currentout w h

Herr :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

Howned :

∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev

Hready :

⊢

stream_call_prelibc_stream_modelrep requests wide WPtrtoken_handled m w

assert Hcurrent : stream_currentd w h by destruct Hd as → | → ; assumption

rep :

mem → libc_world → Prop

requests :

libc_world → ptr → Z → Z → Prop

wide :

libc_world → ptr → stream_state → stream_state → bool → Prop

out, err :

b, o :

d :

pending :

fifo :

listZ

m :

w :

h :

gmappiece pval

Hd :

d = out ∨ d = err

Hout :

stream_currentout w h

Herr :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

Howned :

∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev

Hready :

Hcurrent :

⊢

stream_call_prelibc_stream_modelrep requests wide WPtrtoken_handled m w

destruct stream_open_currentd w h pending fifo Hcurrent Howned as info & Hinfo & _

rep :

mem → libc_world → Prop

requests :

libc_world → ptr → Z → Z → Prop

wide :

libc_world → ptr → stream_state → stream_state → bool → Prop

out, err :

b, o :

d :

pending :

fifo :

listZ

m :

w :

h :

gmappiece pval

Hd :

d = out ∨ d = err

Hout :

stream_currentout w h

Herr :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

Howned :

∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev

Hready :

Hcurrent :

info :

Hinfo :

libc_stream_atw token_handled = Someinfo

⊢

stream_call_prelibc_stream_modelrep requests wide WPtrtoken_handled m w

unfold libc_stream_at in Hinfo

rep :

mem → libc_world → Prop

requests :

libc_world → ptr → Z → Z → Prop

wide :

libc_world → ptr → stream_state → stream_state → bool → Prop

out, err :

b, o :

d :

pending :

fifo :

listZ

m :

w :

h :

gmappiece pval

Hd :

d = out ∨ d = err

Hout :

stream_currentout w h

Herr :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

Howned :

∀l : piece v : pval, l, v ∈ stream_psd pending fifo → h !! l = Somev

Hready :

Hcurrent :

info :

Hinfo :

match libc_file_atw token_handled with

Somefile

⇒

Somestream_identifier ≔ if same_filetoken_handled libc_stdoutw then 1 else 2; stream_protocol ≔ libc_stream_statew token_handled; stream_pending ≔ file_pendingfile

None

⇒

None

Someinfo

⊢

stream_call_prelibc_stream_modelrep requests wide WPtrtoken_handled m w

destruct libc_file_atw token_handled as file | eqn: Hfile ; eapply libc_stream_admitted ; eauto | discriminate

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros rep requests wide out err b o d pending fifo m w h Hd _ & _ & _ & _ & _ & _ & Hout & Herr & Hprivate Howned

pose proof proj1proj1Hprivated Hd as Hready

assert Hcurrent : stream_currentd w h by destruct Hd as → | → ; assumption

destruct stream_open_currentd w h pending fifo Hcurrent Howned as info & Hinfo & _

unfold libc_stream_at in Hinfo

destruct libc_file_atw token_handled as file | eqn: Hfile ; eapply libc_stream_admitted ; eauto | discriminate

The native representation's poll stability remains an explicit realization premise. Everything else follows from unchanged regions.

396Lemma errno_wi_safepoint

∀ rep p b o

∀s m s′ m′ w, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w

LG.SafepointStablelibc_errno_wirep p b o

Explore proof 18 tactics

Initial goal

⊢

∀rep : mem → libc_world → Prop p : ptr b o : Z, ∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w → LG.SafepointStablelibc_errno_wirep p b o

intros rep p b o Hstable

rep :

mem → libc_world → Prop

p :

b, o :

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w

⊢

LG.SafepointStablelibc_errno_wirep p b o

split

rep :

mem → libc_world → Prop

p :

b, o :

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w

⊢

∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world h : gmappiece pval, R.safepoints m s′ m′ → libc_errno_wirep p b o m w h → libc_errno_wirep p b o m′ w h

intros s m s′ m′ w h Hsp Hready & He & Hroots & Hrelease & Hoff

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

⊢

libc_errno_wirep p b o m′ w h

split ; eapply Hstable ; eauto |

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

⊢

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb ∧ roots_apartlibc_stream_aux_rootsw p h m′ ∧ ids_apartlibc_stream_releasesw p h ∧ pieces_offerrno_keysb o h m′ span_containserrno_spanb o

split ; exact He |

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

⊢

roots_apartlibc_stream_aux_rootsw p h m′ ∧ ids_apartlibc_stream_releasesw p h ∧ pieces_offerrno_keysb o h m′ span_containserrno_spanb o

split ; | split ; exact Hrelease |

2 open

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

⊢

roots_apartlibc_stream_aux_rootsw p h m′

focused goal

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

⊢

pieces_offerrno_keysb o h m′ span_containserrno_spanb o

–intros root a Hin Hspan l & v & reg & Hl & Hmem & E Hlive & Hrange

2 open

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

root :

a :

Hin :

Inroot libc_stream_aux_rootsw p

Hspan :

span_containsroot a

l :

v :

reg :

Hl :

h !! l = Somev

Hmem :

E :

object_regionpiece_idl m_regionsm′ = Somereg

Hlive :

r_lifereg = Live

Hrange :

piece_idl ≤ a < r_endreg

⊢

False

deferred goal

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

⊢

pieces_offerrno_keysb o h m′ span_containserrno_spanb o

apply Hrootsroot a Hin Hspan

2 open

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

root :

a :

Hin :

Inroot libc_stream_aux_rootsw p

Hspan :

span_containsroot a

l :

v :

reg :

Hl :

h !! l = Somev

Hmem :

E :

object_regionpiece_idl m_regionsm′ = Somereg

Hlive :

r_lifereg = Live

Hrange :

piece_idl ≤ a < r_endreg

⊢

owned_liveh m a

deferred goal

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

⊢

pieces_offerrno_keysb o h m′ span_containserrno_spanb o

exists l, v, reg

2 open

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

root :

a :

Hin :

Inroot libc_stream_aux_rootsw p

Hspan :

span_containsroot a

l :

v :

reg :

Hl :

h !! l = Somev

Hmem :

E :

object_regionpiece_idl m_regionsm′ = Somereg

Hlive :

r_lifereg = Live

Hrange :

piece_idl ≤ a < r_endreg

⊢

h !! l = Somev ∧ mem_piecel ∧ live_atm piece_idl reg ∧ piece_idl ≤ a < r_endreg

deferred goal

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

⊢

pieces_offerrno_keysb o h m′ span_containserrno_spanb o

split ; exact Hl |

2 open

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

root :

a :

Hin :

Inroot libc_stream_aux_rootsw p

Hspan :

span_containsroot a

l :

v :

reg :

Hl :

h !! l = Somev

Hmem :

E :

object_regionpiece_idl m_regionsm′ = Somereg

Hlive :

r_lifereg = Live

Hrange :

piece_idl ≤ a < r_endreg

⊢

mem_piecel ∧ live_atm piece_idl reg ∧ piece_idl ≤ a < r_endreg

deferred goal

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

⊢

pieces_offerrno_keysb o h m′ span_containserrno_spanb o

split ; exact Hmem |

2 open

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

root :

a :

Hin :

Inroot libc_stream_aux_rootsw p

Hspan :

span_containsroot a

l :

v :

reg :

Hl :

h !! l = Somev

Hmem :

E :

object_regionpiece_idl m_regionsm′ = Somereg

Hlive :

r_lifereg = Live

Hrange :

piece_idl ≤ a < r_endreg

⊢

live_atm piece_idl reg ∧ piece_idl ≤ a < r_endreg

deferred goal

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

⊢

pieces_offerrno_keysb o h m′ span_containserrno_spanb o

split ; | exact Hrange

2 open

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

root :

a :

Hin :

Inroot libc_stream_aux_rootsw p

Hspan :

span_containsroot a

l :

v :

reg :

Hl :

h !! l = Somev

Hmem :

E :

object_regionpiece_idl m_regionsm′ = Somereg

Hlive :

r_lifereg = Live

Hrange :

piece_idl ≤ a < r_endreg

⊢

live_atm piece_idl reg

deferred goal

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

⊢

pieces_offerrno_keysb o h m′ span_containserrno_spanb o

split ; | exact Hlive

2 open

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

root :

a :

Hin :

Inroot libc_stream_aux_rootsw p

Hspan :

span_containsroot a

l :

v :

reg :

Hl :

h !! l = Somev

Hmem :

E :

object_regionpiece_idl m_regionsm′ = Somereg

Hlive :

r_lifereg = Live

Hrange :

piece_idl ≤ a < r_endreg

⊢

object_regionpiece_idl m_regionsm = Somereg

deferred goal

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

⊢

pieces_offerrno_keysb o h m′ span_containserrno_spanb o

rewrite R.collector_live_ _ _ _ Hsp in E

2 open

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

root :

a :

Hin :

Inroot libc_stream_aux_rootsw p

Hspan :

span_containsroot a

l :

v :

reg :

Hl :

h !! l = Somev

Hmem :

Hlive :

r_lifereg = Live

Hrange :

piece_idl ≤ a < r_endreg

E :

object_regionpiece_idl m_regionsm = Somereg

⊢

object_regionpiece_idl m_regionsm = Somereg

deferred goal

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

⊢

pieces_offerrno_keysb o h m′ span_containserrno_spanb o

exact E

deferred goal

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

⊢

pieces_offerrno_keysb o h m′ span_containserrno_spanb o

–intros l v Hl Hnot

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

l :

v :

Hl :

h !! l = Somev

Hnot :

l ∉ errno_keysb o

⊢

match l with

PByteb₀ o₀ | PAuxb₀ o₀

⇒

∀reg : region, live_atm′ b₀ reg → 0 ≤ o₀ → b₀ + o₀ < r_endreg → ¬span_containserrno_spanb o b₀ + o₀

⇒

True

destruct l as base | base off | base off | key ; try exact I

2 open

rep :

mem → libc_world → Prop

p :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

base, off :

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 :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Hready :

He :

libc_errnow.1 = ptr_addr ≔ b + o; ptr_cap ≔ Objb

Hroots :

Hrelease :

Hoff :

pieces_offerrno_keysb o h m span_containserrno_spanb o

base, off :

v :

Hl :

h !! PAuxbase off = Somev

Hnot :

PAuxbase off ∉ errno_keysb o

⊢

∀reg : region, live_atm′ base reg → 0 ≤ off → base + off < r_endreg → ¬span_containserrno_spanb o base + off

all: intros reg E Hlive Ho Hend Hout ; rewrite R.collector_live_ _ _ _ Hsp in E ; exact Hoff_ v Hl Hnot reg conjE Hlive Ho Hend Hout

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros rep p b o Hstable

split

intros s m s′ m′ w h Hsp Hready & He & Hroots & Hrelease & Hoff

split ; eapply Hstable ; eauto |

split ; exact He |

split ; | split ; exact Hrelease |

–intros root a Hin Hspan l & v & reg & Hl & Hmem & E Hlive & Hrange

apply Hrootsroot a Hin Hspan

exists l, v, reg

split ; exact Hl |

split ; exact Hmem |

split ; | exact Hrange

split ; | exact Hlive

rewrite R.collector_live_ _ _ _ Hsp in E

exact E

–intros l v Hl Hnot

destruct l as base | base off | base off | key ; try exact I

all: intros reg E Hlive Ho Hend Hout ; rewrite R.collector_live_ _ _ _ Hsp in E ; exact Hoff_ v Hl Hnot reg conjE Hlive Ho Hend Hout

414Theorem tokens_safepoint

∀ rep out err b o

∀s m s′ m′ w, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w

LG.SafepointStablestream_tokens_wirep out err b o

Explore proof 16 tactics

Initial goal

⊢

∀rep : mem → libc_world → Prop out err : stream_token b o : Z, ∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w → LG.SafepointStablestream_tokens_wirep out err b o

intros rep out err b o Hstable

rep :

mem → libc_world → Prop

out, err :

b, o :

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w

⊢

LG.SafepointStablestream_tokens_wirep out err b o

split

rep :

mem → libc_world → Prop

out, err :

b, o :

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world, R.safepoints m s′ m′ → libc_stream_readyrep m w → libc_stream_readyrep m′ w

⊢

∀s : R.state m : mem s′ : R.state m′ : mem w : libc_world h : gmappiece pval, R.safepoints m s′ m′ → stream_tokens_wirep out err b o m w h → stream_tokens_wirep out err b o m′ w h

intros s m s′ m′ w h Hsp Houtwf & Herrwf & Hbase & Hkey & Hout & Herr & Houtcurrent & Herrcurrent & Hprivate

rep :

mem → libc_world → Prop

out, err :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Houtwf :

Herrwf :

Hbase :

token_baseout ≠ token_baseerr

Hkey :

token_keyout ≠ token_keyerr

Hout :

Herr :

Houtcurrent :

stream_currentout w h

Herrcurrent :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

⊢

stream_tokens_wirep out err b o m′ w h

split ; exact Houtwf |

rep :

mem → libc_world → Prop

out, err :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Houtwf :

Herrwf :

Hbase :

token_baseout ≠ token_baseerr

Hkey :

token_keyout ≠ token_keyerr

Hout :

Herr :

Houtcurrent :

stream_currentout w h

Herrcurrent :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

⊢

token_wferr ∧ token_baseout ≠ token_baseerr ∧ token_keyout ≠ token_keyerr ∧ libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

split ; exact Herrwf |

rep :

mem → libc_world → Prop

out, err :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Houtwf :

Herrwf :

Hbase :

token_baseout ≠ token_baseerr

Hkey :

token_keyout ≠ token_keyerr

Hout :

Herr :

Houtcurrent :

stream_currentout w h

Herrcurrent :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

⊢

token_baseout ≠ token_baseerr ∧ token_keyout ≠ token_keyerr ∧ libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

split ; exact Hbase |

rep :

mem → libc_world → Prop

out, err :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Houtwf :

Herrwf :

Hbase :

token_baseout ≠ token_baseerr

Hkey :

token_keyout ≠ token_keyerr

Hout :

Herr :

Houtcurrent :

stream_currentout w h

Herrcurrent :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

⊢

token_keyout ≠ token_keyerr ∧ libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

split ; exact Hkey |

rep :

mem → libc_world → Prop

out, err :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Houtwf :

Herrwf :

Hbase :

token_baseout ≠ token_baseerr

Hkey :

token_keyout ≠ token_keyerr

Hout :

Herr :

Houtcurrent :

stream_currentout w h

Herrcurrent :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

⊢

libc_stdoutw = token_handleout ∧ libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

split ; exact Hout |

rep :

mem → libc_world → Prop

out, err :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Houtwf :

Herrwf :

Hbase :

token_baseout ≠ token_baseerr

Hkey :

token_keyout ≠ token_keyerr

Hout :

Herr :

Houtcurrent :

stream_currentout w h

Herrcurrent :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

⊢

libc_stderrw = token_handleerr ∧ stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

split ; exact Herr |

rep :

mem → libc_world → Prop

out, err :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Houtwf :

Herrwf :

Hbase :

token_baseout ≠ token_baseerr

Hkey :

token_keyout ≠ token_keyerr

Hout :

Herr :

Houtcurrent :

stream_currentout w h

Herrcurrent :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

⊢

stream_currentout w h ∧ stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

split ; exact Houtcurrent |

rep :

mem → libc_world → Prop

out, err :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Houtwf :

Herrwf :

Hbase :

token_baseout ≠ token_baseerr

Hkey :

token_keyout ≠ token_keyerr

Hout :

Herr :

Houtcurrent :

stream_currentout w h

Herrcurrent :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

⊢

stream_currenterr w h ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

split ; exact Herrcurrent |

rep :

mem → libc_world → Prop

out, err :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Houtwf :

Herrwf :

Hbase :

token_baseout ≠ token_baseerr

Hkey :

token_keyout ≠ token_keyerr

Hout :

Herr :

Houtcurrent :

stream_currentout w h

Herrcurrent :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

⊢

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

intros d Hd

rep :

mem → libc_world → Prop

out, err :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Houtwf :

Herrwf :

Hbase :

token_baseout ≠ token_baseerr

Hkey :

token_keyout ≠ token_keyerr

Hout :

Herr :

Houtcurrent :

stream_currentout w h

Herrcurrent :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

d :

Hd :

d = out ∨ d = err

⊢

libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

destruct Hprivated Hd as Hwi Hrelease

rep :

mem → libc_world → Prop

out, err :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Houtwf :

Herrwf :

Hbase :

token_baseout ≠ token_baseerr

Hkey :

token_keyout ≠ token_keyerr

Hout :

Herr :

Houtcurrent :

stream_currentout w h

Herrcurrent :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

d :

Hd :

d = out ∨ d = err

Hwi :

libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h

Hrelease :

ids_apartlibc_stream_releasesw token_handled h

⊢

libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

split ; | exact Hrelease

rep :

mem → libc_world → Prop

out, err :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Houtwf :

Herrwf :

Hbase :

token_baseout ≠ token_baseerr

Hkey :

token_keyout ≠ token_keyerr

Hout :

Herr :

Houtcurrent :

stream_currentout w h

Herrcurrent :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

d :

Hd :

d = out ∨ d = err

Hwi :

libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h

Hrelease :

ids_apartlibc_stream_releasesw token_handled h

⊢

libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h

pose proof errno_wi_safepointrep token_handled b o Hstable as Hpoll

rep :

mem → libc_world → Prop

out, err :

b, o :

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 :

h :

gmappiece pval

Hsp :

R.safepoints m s′ m′

Houtwf :

Herrwf :

Hbase :

token_baseout ≠ token_baseerr

Hkey :

token_keyout ≠ token_keyerr

Hout :

Herr :

Houtcurrent :

stream_currentout w h

Herrcurrent :

stream_currenterr w h

Hprivate :

∀d : stream_token, d = out ∨ d = err → libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h ∧ ids_apartlibc_stream_releasesw token_handled h

d :

Hd :

d = out ∨ d = err

Hwi :

libc_errno_wirep token_handled b o m w stream_data_heaptoken_baseout token_baseerr h

Hrelease :

ids_apartlibc_stream_releasesw token_handled h

Hpoll :

LG.SafepointStablelibc_errno_wirep token_handled b o

⊢

libc_errno_wirep token_handled b o m′ w stream_data_heaptoken_baseout token_baseerr h

exact @LG.wi_safepoint_ _ Hpoll s m s′ m′ w _ Hsp Hwi

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros rep out err b o Hstable

split

intros s m s′ m′ w h Hsp Houtwf & Herrwf & Hbase & Hkey & Hout & Herr & Houtcurrent & Herrcurrent & Hprivate

split ; exact Houtwf |

split ; exact Herrwf |

split ; exact Hbase |

split ; exact Hkey |

split ; exact Hout |

split ; exact Herr |

split ; exact Houtcurrent |

split ; exact Herrcurrent |

intros d Hd

destruct Hprivated Hd as Hwi Hrelease

split ; | exact Hrelease

pose proof errno_wi_safepointrep token_handled b o Hstable as Hpoll

exact @LG.wi_safepoint_ _ Hpoll s m s′ m′ w _ Hsp Hwi

Discriminating world observations: physical pending is seven, the logical FIFO has two bytes, and a completed close consumes both.

432Module StreamTokenChecks

433Module F ≔ LibcStreamChecks

434Module A ≔ LibcStreamAdapterOn InterpRuntime StreamHandleChecks.LG

436Definition out ≔

mkStreamTokenfile_handleF.out_file 1024 mkRegion1024 1056 GlobalData Live −2

438Definition err ≔

mkStreamTokenfile_handleF.err_file 2048 mkRegion2048 2056 Stack Live −3

440Definition open_heap: gmappiece pval ≔

<[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap

444Example open_snapshots_current: stream_currentout F.worldtrue open_heap ∧ stream_currenterr F.worldtrue open_heap

Explore proof 10 tactics

Initial goal

⊢

stream_currentout F.worldtrue open_heap ∧ stream_currenterr F.worldtrue open_heap

unfold stream_current , open_heap

⊢

match <[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! PNametoken_keyout with

SomeVStreamp snapshot

⇒

p = token_handleout ∧ stream_observationF.worldtrue p snapshot

None

⇒

True

⇒

False

∧

match <[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! PNametoken_keyerr with

SomeVStreamp snapshot

⇒

p = token_handleerr ∧ stream_observationF.worldtrue p snapshot

None

⇒

True

⇒

False

cbn [ out err token_key ]

⊢

match <[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! PName−2 with

SomeVStreamp snapshot

⇒

p = token_handleout ∧ stream_observationF.worldtrue p snapshot

None

⇒

True

⇒

False

∧

match <[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! PName−3 with

SomeVStreamp snapshot

⇒

p = token_handleerr ∧ stream_observationF.worldtrue p snapshot

None

⇒

True

⇒

False

rewrite lookup_insert_eq

⊢

token_handleout = token_handleout ∧ stream_observationF.worldtrue token_handleout Some7, 65; 66

∧

match <[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! PName−3 with

SomeVStreamp snapshot

⇒

p = token_handleerr ∧ stream_observationF.worldtrue p snapshot

None

⇒

True

⇒

False

rewrite lookup_insert_ne ; | discriminate

⊢

token_handleout = token_handleout ∧ stream_observationF.worldtrue token_handleout Some7, 65; 66

∧

match <[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! PName−3 with

SomeVStreamp snapshot

⇒

p = token_handleerr ∧ stream_observationF.worldtrue p snapshot

None

⇒

True

⇒

False

rewrite lookup_insert_eq

⊢

token_handleout = token_handleout ∧ stream_observationF.worldtrue token_handleout Some7, 65; 66 ∧ token_handleerr = token_handleerr ∧ stream_observationF.worldtrue token_handleerr Some3, [ ]

split ; split ; reflexivity |

2 open

⊢

stream_observationF.worldtrue token_handleout Some7, 65; 66

focused goal

⊢

stream_observationF.worldtrue token_handleerr Some3, [ ]

–exists mkStreamInfo1 mkStreamByteOriented 65; 66 true 7

2 open

⊢

libc_stream_atF.worldtrue token_handleout = Somestream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 ∧ stream_pendingstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 = 7 ∧ outstandingstream_protocolstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 = 65; 66

deferred goal

⊢

stream_observationF.worldtrue token_handleerr Some3, [ ]

repeat split ; reflexivity

deferred goal

⊢

stream_observationF.worldtrue token_handleerr Some3, [ ]

–exists mkStreamInfo2 stdout_initial 3

⊢

libc_stream_atF.worldtrue token_handleerr = Somestream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ∧ stream_pendingstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 = 3 ∧ outstandingstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 = [ ]

repeat split ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold stream_current , open_heap

cbn [ out err token_key ]

rewrite lookup_insert_eq

rewrite lookup_insert_ne ; | discriminate

rewrite lookup_insert_eq

split ; split ; reflexivity |

–exists mkStreamInfo1 mkStreamByteOriented 65; 66 true 7

repeat split ; reflexivity

–exists mkStreamInfo2 stdout_initial 3

repeat split ; reflexivity

454Example stale_physical_count_rejected: ¬stream_currentout F.worldtrue <[PName−2 ≔ VStreamtoken_handleout Some2, 65; 66]>open_heap

Explore proof 7 tactics

Initial goal

⊢

¬stream_currentout F.worldtrue <[PName−2 ≔ VStreamtoken_handleout Some2, 65; 66]>open_heap

unfold stream_current

⊢

¬match <[PName−2 ≔ VStreamtoken_handleout Some2, 65; 66]>open_heap !! PNametoken_keyout with SomeVStreamp snapshot ⇒ p = token_handleout ∧ stream_observationF.worldtrue p snapshot | None ⇒ True | _ ⇒ False end

cbn [ out token_key ]

⊢

¬match <[PName−2 ≔ VStreamtoken_handleout Some2, 65; 66]>open_heap !! PName−2 with SomeVStreamp snapshot ⇒ p = token_handleout ∧ stream_observationF.worldtrue p snapshot | None ⇒ True | _ ⇒ False end

rewrite lookup_insert_eq

⊢

¬token_handleout = token_handleout ∧ stream_observationF.worldtrue token_handleout Some2, 65; 66

intros _ & info & Hinfo & Hpending & _

info :

Hinfo :

libc_stream_atF.worldtrue token_handleout = Someinfo

Hpending :

stream_pendinginfo = 2

⊢

False

change SomemkStreamInfo1 mkStreamByteOriented 65; 66 true 7 = Someinfo in Hinfo

info :

Hinfo :

Somestream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 = Someinfo

Hpending :

stream_pendinginfo = 2

⊢

False

injection Hinfo as ←

Hpending :

stream_pendingstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 = 2

⊢

False

discriminate Hpending

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold stream_current

cbn [ out token_key ]

rewrite lookup_insert_eq

intros _ & info & Hinfo & Hpending & _

change SomemkStreamInfo1 mkStreamByteOriented 65; 66 true 7 = Someinfo in Hinfo

injection Hinfo as ←

discriminate Hpending

464Example stale_fifo_rejected: ¬stream_currentout F.worldtrue <[PName−2 ≔ VStreamtoken_handleout Some7, 66; 65]>open_heap

Explore proof 7 tactics

Initial goal

⊢

¬stream_currentout F.worldtrue <[PName−2 ≔ VStreamtoken_handleout Some7, 66; 65]>open_heap

unfold stream_current

⊢

¬match <[PName−2 ≔ VStreamtoken_handleout Some7, 66; 65]>open_heap !! PNametoken_keyout with SomeVStreamp snapshot ⇒ p = token_handleout ∧ stream_observationF.worldtrue p snapshot | None ⇒ True | _ ⇒ False end

cbn [ out token_key ]

⊢

¬match <[PName−2 ≔ VStreamtoken_handleout Some7, 66; 65]>open_heap !! PName−2 with SomeVStreamp snapshot ⇒ p = token_handleout ∧ stream_observationF.worldtrue p snapshot | None ⇒ True | _ ⇒ False end

rewrite lookup_insert_eq

⊢

¬token_handleout = token_handleout ∧ stream_observationF.worldtrue token_handleout Some7, 66; 65

intros _ & info & Hinfo & _ & Hfifo

info :

Hinfo :

libc_stream_atF.worldtrue token_handleout = Someinfo

Hfifo :

outstandingstream_protocolinfo = 66; 65

⊢

False

change SomemkStreamInfo1 mkStreamByteOriented 65; 66 true 7 = Someinfo in Hinfo

info :

Hinfo :

Somestream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 = Someinfo

Hfifo :

outstandingstream_protocolinfo = 66; 65

⊢

False

injection Hinfo as ←

Hfifo :

outstandingstream_protocolstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 = 66; 65

⊢

False

discriminate Hfifo

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold stream_current

cbn [ out token_key ]

rewrite lookup_insert_eq

intros _ & info & Hinfo & _ & Hfifo

change SomemkStreamInfo1 mkStreamByteOriented 65; 66 true 7 = Someinfo in Hinfo

injection Hinfo as ←

discriminate Hfifo

474Example completed_closed_snapshot: stream_currentout F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>open_heap

Explore proof 5 tactics

Initial goal

⊢

stream_currentout F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>open_heap

unfold stream_current

⊢

match <[PName−2 ≔ VStreamtoken_handleout None]>open_heap !! PNametoken_keyout with

SomeVStreamp snapshot

⇒

p = token_handleout ∧ stream_observationF.worldfalse p snapshot

None

⇒

True

⇒

False

cbn [ out token_key ]

⊢

match <[PName−2 ≔ VStreamtoken_handleout None]>open_heap !! PName−2 with

SomeVStreamp snapshot

⇒

p = token_handleout ∧ stream_observationF.worldfalse p snapshot

None

⇒

True

⇒

False

rewrite lookup_insert_eq

⊢

token_handleout = token_handleout ∧ stream_observationF.worldfalse token_handleout None

split ; reflexivity |

⊢

stream_observationF.worldfalse token_handleout None

split ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold stream_current

cbn [ out token_key ]

rewrite lookup_insert_eq

split ; reflexivity |

split ; reflexivity

482Example closed_token_rejected_while_open: ¬stream_currentout F.worldtrue <[PName−2 ≔ VStreamtoken_handleout None]>open_heap

Explore proof 5 tactics

Initial goal

⊢

¬stream_currentout F.worldtrue <[PName−2 ≔ VStreamtoken_handleout None]>open_heap

unfold stream_current

⊢

¬match <[PName−2 ≔ VStreamtoken_handleout None]>open_heap !! PNametoken_keyout with SomeVStreamp snapshot ⇒ p = token_handleout ∧ stream_observationF.worldtrue p snapshot | None ⇒ True | _ ⇒ False end

cbn [ out token_key ]

⊢

¬match <[PName−2 ≔ VStreamtoken_handleout None]>open_heap !! PName−2 with SomeVStreamp snapshot ⇒ p = token_handleout ∧ stream_observationF.worldtrue p snapshot | None ⇒ True | _ ⇒ False end

rewrite lookup_insert_eq

⊢

¬token_handleout = token_handleout ∧ stream_observationF.worldtrue token_handleout None

intros _ & Hclosed & _

Hclosed :

libc_stream_atF.worldtrue token_handleout = None

⊢

False

discriminate Hclosed

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold stream_current

cbn [ out token_key ]

rewrite lookup_insert_eq

intros _ & Hclosed & _

discriminate Hclosed

490Example malformed_snapshot_rejected: ¬stream_currentout F.worldtrue <[PName−2 ≔ VNametoken_handleout 65]>open_heap

Explore proof 4 tactics

Initial goal

⊢

¬stream_currentout F.worldtrue <[PName−2 ≔ VNametoken_handleout 65]>open_heap

unfold stream_current

⊢

¬match <[PName−2 ≔ VNametoken_handleout 65]>open_heap !! PNametoken_keyout with SomeVStreamp snapshot ⇒ p = token_handleout ∧ stream_observationF.worldtrue p snapshot | None ⇒ True | _ ⇒ False end

cbn [ out token_key ]

⊢

¬match <[PName−2 ≔ VNametoken_handleout 65]>open_heap !! PName−2 with SomeVStreamp snapshot ⇒ p = token_handleout ∧ stream_observationF.worldtrue p snapshot | None ⇒ True | _ ⇒ False end

rewrite lookup_insert_eq

⊢

¬False

exact λH ⇒ H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

unfold stream_current

cbn [ out token_key ]

rewrite lookup_insert_eq

exact λH ⇒ H

The entire interpretation has an inhabitant with both open tokens, both native lives and owned errno, not merely each mirror alone.

496Lemma private_lookup

∀ l v

stream_data_heap1024 2048 open_heap !! l = Somev

HelloErrnoChecks.heap !! l = Somev

Explore proof 9 tactics

Initial goal

⊢

∀l : piece v : pval, mem_piecel → stream_data_heap1024 2048 open_heap !! l = Somev → HelloErrnoChecks.heap !! l = Somev

intros l v Hmem Hl

l :

v :

Hmem :

Hl :

stream_data_heap1024 2048 open_heap !! l = Somev

⊢

HelloErrnoChecks.heap !! l = Somev

apply stream_data_lookup in Hl as Hl & Hout & Herr

l :

v :

Hmem :

Hl :

open_heap !! l = Somev

Hout :

l ≠ PLive1024

Herr :

l ≠ PLive2048

⊢

HelloErrnoChecks.heap !! l = Somev

unfold open_heap in Hl

l :

v :

Hmem :

Hl :

<[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! l = Somev

Hout :

l ≠ PLive1024

Herr :

l ≠ PLive2048

⊢

HelloErrnoChecks.heap !! l = Somev

apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |

l :

v :

Hmem :

Hl :

<[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! l = Somev

Hout :

l ≠ PLive1024

Herr :

l ≠ PLive2048

⊢

HelloErrnoChecks.heap !! l = Somev

apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |

l :

v :

Hmem :

Hl :

StreamHandleChecks.heap !! l = Somev

Hout :

l ≠ PLive1024

Herr :

l ≠ PLive2048

⊢

HelloErrnoChecks.heap !! l = Somev

unfold StreamHandleChecks.heap in Hl

l :

v :

Hmem :

Hl :

<[PLive1024 ≔ VLiver_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live]><[PLive2048 ≔ VLiver_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live]>StreamHandleChecks.E.heap !! l = Somev

Hout :

l ≠ PLive1024

Herr :

l ≠ PLive2048

⊢

HelloErrnoChecks.heap !! l = Somev

apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |

l :

v :

Hmem :

Hl :

<[PLive2048 ≔ VLiver_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live]>StreamHandleChecks.E.heap !! l = Somev

Hout :

l ≠ PLive1024

Herr :

l ≠ PLive2048

⊢

HelloErrnoChecks.heap !! l = Somev

apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |

l :

v :

Hmem :

Hl :

StreamHandleChecks.E.heap !! l = Somev

Hout :

l ≠ PLive1024

Herr :

l ≠ PLive2048

⊢

HelloErrnoChecks.heap !! l = Somev

exact Hl

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros l v Hmem Hl

apply stream_data_lookup in Hl as Hl & Hout & Herr

unfold open_heap in Hl

apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |

unfold StreamHandleChecks.heap in Hl

apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |

exact Hl

510Lemma full_wi

stream_tokens_wiλ_ _ ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

Explore proof 25 tactics

Initial goal

⊢

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

assert Hkeys : ∀l v, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

2 open

⊢

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

focused goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

{intros l v Hl Hmem

2 open

l :

v :

Hl :

stream_data_heap1024 2048 open_heap !! l = Somev

Hmem :

⊢

l ∈ errno_keys5120 0

deferred goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

apply private_lookupl v Hmem in Hl

2 open

l :

v :

Hl :

HelloErrnoChecks.heap !! l = Somev

Hmem :

⊢

l ∈ errno_keys5120 0

deferred goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

unfold HelloErrnoChecks.heap in Hl

2 open

l :

v :

Hl :

list_to_mapbyte_ps5120 0 0; 0; 0; 0 !! l = Somev

Hmem :

⊢

l ∈ errno_keys5120 0

deferred goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

apply elem_of_list_to_map_2 in Hl

2 open

l :

v :

Hl :

l, v ∈ byte_ps5120 0 0; 0; 0; 0

Hmem :

⊢

l ∈ errno_keys5120 0

deferred goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

change l ∈ byte_ps5120 0 0; 0; 0; 0.*1

2 open

l :

v :

Hl :

l, v ∈ byte_ps5120 0 0; 0; 0; 0

Hmem :

⊢

l ∈ byte_ps5120 0 0; 0; 0; 0.*1

deferred goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

apply list_elem_of_fmap

2 open

l :

v :

Hl :

l, v ∈ byte_ps5120 0 0; 0; 0; 0

Hmem :

⊢

∃x : piece × pval, l = x.1 ∧ x ∈ byte_ps5120 0 0; 0; 0; 0

deferred goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

exists l, v

2 open

l :

v :

Hl :

l, v ∈ byte_ps5120 0 0; 0; 0; 0

Hmem :

⊢

l = l, v.1 ∧ l, v ∈ byte_ps5120 0 0; 0; 0; 0

deferred goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

auto

deferred goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

split ; split ; reflexivity | simpl ; lia |

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

token_wferr ∧ token_baseout ≠ token_baseerr ∧ token_keyout ≠ token_keyerr ∧ libc_stdoutF.worldtrue = token_handleout ∧ libc_stderrF.worldtrue = token_handleerr ∧ stream_currentout F.worldtrue open_heap ∧ stream_currenterr F.worldtrue open_heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled open_heap

split ; split ; reflexivity | simpl ; lia |

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

token_baseout ≠ token_baseerr ∧ token_keyout ≠ token_keyerr ∧ libc_stdoutF.worldtrue = token_handleout ∧ libc_stderrF.worldtrue = token_handleerr ∧ stream_currentout F.worldtrue open_heap ∧ stream_currenterr F.worldtrue open_heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled open_heap

split ; discriminate |

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

token_keyout ≠ token_keyerr ∧ libc_stdoutF.worldtrue = token_handleout ∧ libc_stderrF.worldtrue = token_handleerr ∧ stream_currentout F.worldtrue open_heap ∧ stream_currenterr F.worldtrue open_heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled open_heap

split ; discriminate |

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

libc_stdoutF.worldtrue = token_handleout ∧ libc_stderrF.worldtrue = token_handleerr ∧ stream_currentout F.worldtrue open_heap ∧ stream_currenterr F.worldtrue open_heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled open_heap

split ; reflexivity |

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

libc_stderrF.worldtrue = token_handleerr ∧ stream_currentout F.worldtrue open_heap ∧ stream_currenterr F.worldtrue open_heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled open_heap

split ; reflexivity |

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

stream_currentout F.worldtrue open_heap ∧ stream_currenterr F.worldtrue open_heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled open_heap

split ; exact proj1open_snapshots_current |

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

stream_currenterr F.worldtrue open_heap ∧ ∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled open_heap

split ; exact proj2open_snapshots_current |

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

∀d : stream_token, d = out ∨ d = err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handled open_heap

intros d → | →

2 open

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handleout 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handleout open_heap

focused goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handleerr 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap ∧ ids_apartlibc_stream_releasesF.worldtrue token_handleerr open_heap

all: split ; | intros base l v Hin ; change Inbase [ ] in Hin ; contradiction

2 open

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handleout 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap

focused goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handleerr 5120 0 conversion_mem F.worldtrue stream_data_heaptoken_baseout token_baseerr open_heap

all: split ; apply F.ready |

2 open

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

libc_errnoF.worldtrue.1 = ptr_addr ≔ 5120 + 0; ptr_cap ≔ Obj5120 ∧ roots_apartlibc_stream_aux_rootsF.worldtrue token_handleout stream_data_heaptoken_baseout token_baseerr open_heap conversion_mem ∧ ids_apartlibc_stream_releasesF.worldtrue token_handleout stream_data_heaptoken_baseout token_baseerr open_heap ∧ pieces_offerrno_keys5120 0 stream_data_heaptoken_baseout token_baseerr open_heap conversion_mem span_containserrno_span5120 0

focused goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

libc_errnoF.worldtrue.1 = ptr_addr ≔ 5120 + 0; ptr_cap ≔ Obj5120 ∧ roots_apartlibc_stream_aux_rootsF.worldtrue token_handleerr stream_data_heaptoken_baseout token_baseerr open_heap conversion_mem ∧ ids_apartlibc_stream_releasesF.worldtrue token_handleerr stream_data_heaptoken_baseout token_baseerr open_heap ∧ pieces_offerrno_keys5120 0 stream_data_heaptoken_baseout token_baseerr open_heap conversion_mem span_containserrno_span5120 0

all: split ; reflexivity |

2 open

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

focused goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

all: split ; intros root a Hin ; change Inroot [ ] in Hin ; contradiction |

2 open

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

focused goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

all: split ; intros base l v Hin ; change Inbase [ ] in Hin ; contradiction |

2 open

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

pieces_offerrno_keys5120 0 stream_data_heaptoken_baseout token_baseerr open_heap conversion_mem span_containserrno_span5120 0

focused goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

⊢

pieces_offerrno_keys5120 0 stream_data_heaptoken_baseout token_baseerr open_heap conversion_mem span_containserrno_span5120 0

all: intros l v Hl Hnot ; destruct l as base | base off | base off | key ; try exact I

4 open

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

base, off :

v :

Hl :

stream_data_heaptoken_baseout token_baseerr open_heap !! PBytebase off = Somev

Hnot :

PBytebase off ∉ errno_keys5120 0

⊢

∀reg : region, live_atconversion_mem base reg → 0 ≤ off → base + off < r_endreg → ¬span_containserrno_span5120 0 base + off

focused goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

base, off :

v :

Hl :

stream_data_heaptoken_baseout token_baseerr open_heap !! PAuxbase off = Somev

Hnot :

PAuxbase off ∉ errno_keys5120 0

⊢

∀reg : region, live_atconversion_mem base reg → 0 ≤ off → base + off < r_endreg → ¬span_containserrno_span5120 0 base + off

focused goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

base, off :

v :

Hl :

stream_data_heaptoken_baseout token_baseerr open_heap !! PBytebase off = Somev

Hnot :

PBytebase off ∉ errno_keys5120 0

⊢

∀reg : region, live_atconversion_mem base reg → 0 ≤ off → base + off < r_endreg → ¬span_containserrno_span5120 0 base + off

focused goal

Hkeys :

∀l : piece v : pval, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

base, off :

v :

Hl :

stream_data_heaptoken_baseout token_baseerr open_heap !! PAuxbase off = Somev

Hnot :

PAuxbase off ∉ errno_keys5120 0

⊢

∀reg : region, live_atconversion_mem base reg → 0 ≤ off → base + off < r_endreg → ¬span_containserrno_span5120 0 base + off

all: exfalso ; apply Hnot ; eapply Hkeys ; exact Hl | exact I

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

assert Hkeys : ∀l v, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0

{intros l v Hl Hmem

apply private_lookupl v Hmem in Hl

unfold HelloErrnoChecks.heap in Hl

apply elem_of_list_to_map_2 in Hl

change l ∈ byte_ps5120 0 0; 0; 0; 0.*1

apply list_elem_of_fmap

exists l, v

auto

split ; split ; reflexivity | simpl ; lia |

split ; discriminate |

split ; reflexivity |

split ; exact proj1open_snapshots_current |

split ; exact proj2open_snapshots_current |

intros d → | →

all: split ; | intros base l v Hin ; change Inbase [ ] in Hin ; contradiction

all: split ; apply F.ready |

all: split ; reflexivity |

all: split ; intros root a Hin ; change Inroot [ ] in Hin ; contradiction |

all: split ; intros base l v Hin ; change Inbase [ ] in Hin ; contradiction |

all: intros l v Hl Hnot ; destruct l as base | base off | base off | key ; try exact I

all: exfalso ; apply Hnot ; eapply Hkeys ; exact Hl | exact I

532Example full_open_admitted: stream_call_preF.model WPtrtoken_handleout conversion_mem F.worldtrue

Explore proof 15 tactics

Initial goal

⊢

stream_call_preF.model WPtrtoken_handleout conversion_mem F.worldtrue

eapply A.open_admitted with out := out err := err b := 5120 o := 0 pending := 7 fifo := 65; 66 h := open_heap ; left ; reflexivity | exact full_wi |

⊢

∀l : piece v : pval, l, v ∈ stream_psout 7 65; 66 → open_heap !! l = Somev

intros l v Hin

l :

v :

Hin :

l, v ∈ stream_psout 7 65; 66

⊢

open_heap !! l = Somev

unfold stream_ps in Hin

l :

v :

Hin :

l, v ∈ PLivetoken_baseout, VLivetoken_regionout; PNametoken_keyout, VStreamtoken_handleout Some7, 65; 66

⊢

open_heap !! l = Somev

apply elem_of_cons in Hin as He | Hin

2 open

l :

v :

He :

l, v = PLivetoken_baseout, VLivetoken_regionout

⊢

open_heap !! l = Somev

focused goal

l :

v :

Hin :

l, v ∈ PNametoken_keyout, VStreamtoken_handleout Some7, 65; 66

⊢

open_heap !! l = Somev

–injection He as He Hv

2 open

l :

v :

He :

l = PLive1024

Hv :

v = VLiver_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live

⊢

open_heap !! l = Somev

deferred goal

l :

v :

Hin :

l, v ∈ PNametoken_keyout, VStreamtoken_handleout Some7, 65; 66

⊢

open_heap !! l = Somev

subst l v

2 open

⊢

open_heap !! PLive1024 = SomeVLiver_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live

deferred goal

l :

v :

Hin :

l, v ∈ PNametoken_keyout, VStreamtoken_handleout Some7, 65; 66

⊢

open_heap !! l = Somev

unfold open_heap , StreamHandleChecks.heap

2 open

⊢

<[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]><[PLive1024 ≔ VLiver_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live]><[PLive2048 ≔ VLiver_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live]>StreamHandleChecks.E.heap !! PLive1024 = SomeVLiver_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live

deferred goal

l :

v :

Hin :

l, v ∈ PNametoken_keyout, VStreamtoken_handleout Some7, 65; 66

⊢

open_heap !! l = Somev

rewrite lookup_insert_ne ; | discriminate

2 open

⊢

<[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]><[PLive1024 ≔ VLiver_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live]><[PLive2048 ≔ VLiver_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live]>StreamHandleChecks.E.heap !! PLive1024 = SomeVLiver_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live

deferred goal

l :

v :

Hin :

l, v ∈ PNametoken_keyout, VStreamtoken_handleout Some7, 65; 66

⊢

open_heap !! l = Somev

rewrite lookup_insert_ne ; | discriminate

2 open

⊢

deferred goal

l :

v :

Hin :

l, v ∈ PNametoken_keyout, VStreamtoken_handleout Some7, 65; 66

⊢

open_heap !! l = Somev

apply lookup_insert_eq

deferred goal

l :

v :

Hin :

l, v ∈ PNametoken_keyout, VStreamtoken_handleout Some7, 65; 66

⊢

open_heap !! l = Somev

–apply elem_of_cons in Hin as He | Hin ; | apply not_elem_of_nil in Hin ; contradiction

l :

v :

He :

l, v = PNametoken_keyout, VStreamtoken_handleout Some7, 65; 66

⊢

open_heap !! l = Somev

injection He as He Hv

l :

v :

agreesconversion_mem open_heap

He :

l = PName−2

Hv :

v = VStreamptr_addr ≔ 1024; ptr_cap ≔ Obj1024 Some7, 65; 66

⊢

open_heap !! l = Somev

subst l v

⊢

open_heap !! PName−2 = SomeVStreamptr_addr ≔ 1024; ptr_cap ≔ Obj1024 Some7, 65; 66

unfold open_heap

⊢

<[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! PName−2 = SomeVStreamptr_addr ≔ 1024; ptr_cap ≔ Obj1024 Some7, 65; 66

apply lookup_insert_eq

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

eapply A.open_admitted with out := out err := err b := 5120 o := 0 pending := 7 fifo := 65; 66 h := open_heap ; left ; reflexivity | exact full_wi |

intros l v Hin

unfold stream_ps in Hin

apply elem_of_cons in Hin as He | Hin

–injection He as He Hv

subst l v

unfold open_heap , StreamHandleChecks.heap

rewrite lookup_insert_ne ; | discriminate

apply lookup_insert_eq

–apply elem_of_cons in Hin as He | Hin ; | apply not_elem_of_nil in Hin ; contradiction

injection He as He Hv

subst l v

unfold open_heap

apply lookup_insert_eq

546Lemma open_heap_agrees

Explore proof 5 tactics

Initial goal

⊢

agreesconversion_mem open_heap

intros l v Hl

l :

v :

Hl :

open_heap !! l = Somev

⊢

unfold open_heap in Hl

l :

v :

Hl :

<[PName−2 ≔ VStreamtoken_handleout Some7, 65; 66]><[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! l = Somev

⊢

apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l v ; exact I |

l :

v :

Hl :

<[PName−3 ≔ VStreamtoken_handleerr Some3, [ ]]>StreamHandleChecks.heap !! l = Somev

⊢

apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l v ; exact I |

l :

v :

Hl :

StreamHandleChecks.heap !! l = Somev

⊢

exact StreamHandleChecks.heap_agreesl v Hl

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros l v Hl

unfold open_heap in Hl

apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l v ; exact I |

exact StreamHandleChecks.heap_agreesl v Hl

An actual stderr query frames the paired interpretation even though stdout's physical count and outstanding FIFO differ from stderr's.

556Example stderr_query_preserves_pair: A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ _ ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

Explore proof 10 tactics

Initial goal

⊢

A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

assert Hcall : A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue

2 open

⊢

A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue

focused goal

Hcall :

A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue

⊢

{apply StreamHandleChecks.C.fpending_unchanged with file := F.err_file

4 open

⊢

stream_query_abiL CVoid ArgP Const0

focused goal

⊢

libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue

focused goal

⊢

libc_file_atF.worldtrue token_handleerr = SomeF.err_file

deferred goal

Hcall :

A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue

⊢

–split ; left ; reflexivity |

4 open

⊢

∃v : value, ArgP Const0 = ArgP v

deferred goal

⊢

libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue

deferred goal

⊢

libc_file_atF.worldtrue token_handleerr = SomeF.err_file

deferred goal

Hcall :

A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue

⊢

exists Const0

4 open

⊢

ArgP Const0 = ArgP Const0

deferred goal

⊢

libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue

deferred goal

⊢

libc_file_atF.worldtrue token_handleerr = SomeF.err_file

deferred goal

Hcall :

A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue

⊢

reflexivity

3 open

deferred goal

⊢

libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue

deferred goal

⊢

libc_file_atF.worldtrue token_handleerr = SomeF.err_file

deferred goal

Hcall :

A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue

⊢

–apply F.ready

2 open

deferred goal

⊢

libc_file_atF.worldtrue token_handleerr = SomeF.err_file

deferred goal

Hcall :

A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue

⊢

–reflexivity

deferred goal

Hcall :

A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue

⊢

split ; exact Hcall |

Hcall :

A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue

⊢

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

destruct A.query_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False out err 5120 0 err _ _ _ _ _ _ _ _ _ _ _ open_heap or_introreq_refl or_introreq_refl Hcall open_heap_agrees HelloErrnoChecks.disjoint HelloErrnoChecks.ready full_wi as _ & _ & _ & Hw

Hcall :

A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue

Hw :

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

⊢

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

exact Hw

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

assert Hcall : A.M.E.invokefpending_contractF.model CVoid ArgP Const0 WPtrtoken_handleerr InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt3 InterpRuntime.start conversion_mem F.worldtrue

{apply StreamHandleChecks.C.fpending_unchanged with file := F.err_file

–split ; left ; reflexivity |

exists Const0

reflexivity

–apply F.ready

–reflexivity

split ; exact Hcall |

destruct A.query_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False out err 5120 0 err _ _ _ _ _ _ _ _ _ _ _ open_heap or_introreq_refl or_introreq_refl Hcall open_heap_agrees HelloErrnoChecks.disjoint HelloErrnoChecks.ready full_wi as _ & _ & _ & Hw

exact Hw

The other query contract and stdout selection use the same frame.

578Example stdout_error_preserves_pair: A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ _ ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

Explore proof 10 tactics

Initial goal

⊢

A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

assert Hcall : A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue

2 open

⊢

A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue

focused goal

Hcall :

A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue

⊢

{apply StreamHandleChecks.C.ferror_unchanged with file := F.out_file

4 open

⊢

stream_query_abiW CVoid ArgP Const0

focused goal

⊢

libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue

focused goal

⊢

libc_file_atF.worldtrue token_handleout = SomeF.out_file

deferred goal

Hcall :

A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue

⊢

–split ; left ; reflexivity |

4 open

⊢

∃v : value, ArgP Const0 = ArgP v

deferred goal

⊢

libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue

deferred goal

⊢

libc_file_atF.worldtrue token_handleout = SomeF.out_file

deferred goal

Hcall :

A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue

⊢

exists Const0

4 open

⊢

ArgP Const0 = ArgP Const0

deferred goal

⊢

libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue

deferred goal

⊢

libc_file_atF.worldtrue token_handleout = SomeF.out_file

deferred goal

Hcall :

A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue

⊢

reflexivity

3 open

deferred goal

⊢

libc_stream_readyλ_ : mem _ : libc_world ⇒ True conversion_mem F.worldtrue

deferred goal

⊢

libc_file_atF.worldtrue token_handleout = SomeF.out_file

deferred goal

Hcall :

A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue

⊢

–apply F.ready

2 open

deferred goal

⊢

libc_file_atF.worldtrue token_handleout = SomeF.out_file

deferred goal

Hcall :

A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue

⊢

–reflexivity

deferred goal

Hcall :

A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue

⊢

split ; exact Hcall |

Hcall :

A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue

⊢

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

destruct A.query_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False out err 5120 0 out _ _ _ _ _ _ _ _ _ _ _ open_heap or_introleq_refl or_introleq_refl Hcall open_heap_agrees HelloErrnoChecks.disjoint HelloErrnoChecks.ready full_wi as _ & _ & _ & Hw

Hcall :

A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue

Hw :

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

⊢

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 conversion_mem F.worldtrue open_heap

exact Hw

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

assert Hcall : A.M.E.invokeferror_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWInt1 InterpRuntime.start conversion_mem F.worldtrue

{apply StreamHandleChecks.C.ferror_unchanged with file := F.out_file

–split ; left ; reflexivity |

exists Const0

reflexivity

–apply F.ready

–reflexivity

split ; exact Hcall |

destruct A.query_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False out err 5120 0 out _ _ _ _ _ _ _ _ _ _ _ open_heap or_introleq_refl or_introleq_refl Hcall open_heap_agrees HelloErrnoChecks.disjoint HelloErrnoChecks.ready full_wi as _ & _ & _ & Hw

exact Hw

An actual authorized scalar write changes every errno byte, including the last one. It changes neither FILE storage nor locale strings.

601Definition changed_errno: mem ≔

store_bytesconversion_mem 5120 4 16909060

603Lemma changed_files_ready

libc_file_readychanged_errno mkPtr5120 Obj5120 F.out_file ∧ libc_file_readychanged_errno mkPtr5120 Obj5120 F.err_file

Explore proof 9 tactics

Initial goal

⊢

libc_file_readychanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file ∧ libc_file_readychanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file

destruct F.files_ready as Hout Herr

Hout :

libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file

Herr :

libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file

⊢

libc_file_readychanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file ∧ libc_file_readychanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file

split ; clear Herr | clear Hout

2 open

Hout :

libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file

⊢

libc_file_readychanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file

focused goal

Herr :

libc_file_readyconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file

⊢

libc_file_readychanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file

all: destruct Hout as Hnon & Hn & Hreg & Haccess & Hbytes & Hrest || destruct Herr as Hnon & Hn & Hreg & Haccess & Hbytes & Hrest

2 open

Hnon :

Hn :

0 ≤ 1 < 2 ^ 64

Hreg :

∃base : Z reg : region, ptr_capfile_handleF.out_file = Objbase ∨ ptr_capfile_handleF.out_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live

Haccess :

access_resconversion_mem ptr_addrfile_handleF.out_file ptr_capfile_handleF.out_file 1 Read 1 = Someok

Hbytes :

∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.out_file + i < 256

Hrest :

0 ≤ file_pendingF.out_file < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsF.out_file ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsF.out_file ∧ ForallLocale.locale_heapconversion_mem file_ownedF.out_file ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file

⊢

libc_file_readychanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file

focused goal

Hnon :

Hn :

0 ≤ 1 < 2 ^ 64

Hreg :

∃base : Z reg : region, ptr_capfile_handleF.err_file = Objbase ∨ ptr_capfile_handleF.err_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live

Haccess :

access_resconversion_mem ptr_addrfile_handleF.err_file ptr_capfile_handleF.err_file 1 Read 1 = Someok

Hbytes :

∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.err_file + i < 256

Hrest :

0 ≤ file_pendingF.err_file < 2 ^ 64 ∧ Forallwritable_spanconversion_mem file_rootsF.err_file ∧ Forallλsource : span ⇒ readable_bytesconversion_mem span_ptrsource span_sizesource file_readsF.err_file ∧ ForallLocale.locale_heapconversion_mem file_ownedF.err_file ∧ file_errno_apartconversion_mem ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file

⊢

libc_file_readychanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file

all: split ; exact Hnon |

2 open

Hnon :

Hn :

0 ≤ 1 < 2 ^ 64

Hreg :

∃base : Z reg : region, ptr_capfile_handleF.out_file = Objbase ∨ ptr_capfile_handleF.out_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live

Haccess :

access_resconversion_mem ptr_addrfile_handleF.out_file ptr_capfile_handleF.out_file 1 Read 1 = Someok

Hbytes :

∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.out_file + i < 256

Hrest :

⊢

readable_byteschanged_errno file_handleF.out_file 1 ∧ 0 ≤ file_pendingF.out_file < 2 ^ 64 ∧ Forallwritable_spanchanged_errno file_rootsF.out_file ∧ Forallλsource : span ⇒ readable_byteschanged_errno span_ptrsource span_sizesource file_readsF.out_file ∧ ForallLocale.locale_heapchanged_errno file_ownedF.out_file ∧ file_errno_apartchanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.out_file

focused goal

Hnon :

Hn :

0 ≤ 1 < 2 ^ 64

Hreg :

∃base : Z reg : region, ptr_capfile_handleF.err_file = Objbase ∨ ptr_capfile_handleF.err_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live

Haccess :

access_resconversion_mem ptr_addrfile_handleF.err_file ptr_capfile_handleF.err_file 1 Read 1 = Someok

Hbytes :

∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.err_file + i < 256

Hrest :

⊢

readable_byteschanged_errno file_handleF.err_file 1 ∧ 0 ≤ file_pendingF.err_file < 2 ^ 64 ∧ Forallwritable_spanchanged_errno file_rootsF.err_file ∧ Forallλsource : span ⇒ readable_byteschanged_errno span_ptrsource span_sizesource file_readsF.err_file ∧ ForallLocale.locale_heapchanged_errno file_ownedF.err_file ∧ file_errno_apartchanged_errno ptr_addr ≔ 5120; ptr_cap ≔ Obj5120 F.err_file

all: split ; | destruct Hrest as Hp & _ & _ & _ & Ha ; split ; exact Hp | ; split ; constructor | ; split ; constructor | ; split ; constructor | exact Ha

2 open

Hnon :

readable_byteschanged_errno file_handleF.out_file 1

Hn :

0 ≤ 1 < 2 ^ 64

Hreg :

∃base : Z reg : region, ptr_capfile_handleF.out_file = Objbase ∨ ptr_capfile_handleF.out_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live

Haccess :

access_resconversion_mem ptr_addrfile_handleF.out_file ptr_capfile_handleF.out_file 1 Read 1 = Someok

Hbytes :

∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.out_file + i < 256

Hrest :

⊢

focused goal

Hnon :

readable_byteschanged_errno file_handleF.err_file 1

Hn :

0 ≤ 1 < 2 ^ 64

Hreg :

∃base : Z reg : region, ptr_capfile_handleF.err_file = Objbase ∨ ptr_capfile_handleF.err_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live

Haccess :

access_resconversion_mem ptr_addrfile_handleF.err_file ptr_capfile_handleF.err_file 1 Read 1 = Someok

Hbytes :

∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.err_file + i < 256

Hrest :

⊢

all: split ; exact Hn |

2 open

Hnon :

Hn :

0 ≤ 1 < 2 ^ 64

Hreg :

∃base : Z reg : region, ptr_capfile_handleF.out_file = Objbase ∨ ptr_capfile_handleF.out_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live

Haccess :

access_resconversion_mem ptr_addrfile_handleF.out_file ptr_capfile_handleF.out_file 1 Read 1 = Someok

Hbytes :

∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.out_file + i < 256

Hrest :

⊢

∃base : Z reg : region, ptr_capfile_handleF.out_file = Objbase ∨ ptr_capfile_handleF.out_file = Robase ∧ object_regionbase m_regionschanged_errno = Somereg ∧ r_lifereg = Live ∧ access_reschanged_errno ptr_addrfile_handleF.out_file ptr_capfile_handleF.out_file 1 Read 1 = Someok ∧ ∀i : Z, 0 ≤ i < 1 → 0 ≤ m_byteschanged_errno ptr_addrfile_handleF.out_file + i < 256

focused goal

Hnon :

Hn :

0 ≤ 1 < 2 ^ 64

Hreg :

∃base : Z reg : region, ptr_capfile_handleF.err_file = Objbase ∨ ptr_capfile_handleF.err_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live

Haccess :

access_resconversion_mem ptr_addrfile_handleF.err_file ptr_capfile_handleF.err_file 1 Read 1 = Someok

Hbytes :

∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.err_file + i < 256

Hrest :

⊢

∃base : Z reg : region, ptr_capfile_handleF.err_file = Objbase ∨ ptr_capfile_handleF.err_file = Robase ∧ object_regionbase m_regionschanged_errno = Somereg ∧ r_lifereg = Live ∧ access_reschanged_errno ptr_addrfile_handleF.err_file ptr_capfile_handleF.err_file 1 Read 1 = Someok ∧ ∀i : Z, 0 ≤ i < 1 → 0 ≤ m_byteschanged_errno ptr_addrfile_handleF.err_file + i < 256

all: split ; exact Hreg |

2 open

Hnon :

Hn :

0 ≤ 1 < 2 ^ 64

Hreg :

∃base : Z reg : region, ptr_capfile_handleF.out_file = Objbase ∨ ptr_capfile_handleF.out_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live

Haccess :

access_resconversion_mem ptr_addrfile_handleF.out_file ptr_capfile_handleF.out_file 1 Read 1 = Someok

Hbytes :

∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.out_file + i < 256

Hrest :

⊢

access_reschanged_errno ptr_addrfile_handleF.out_file ptr_capfile_handleF.out_file 1 Read 1 = Someok ∧ ∀i : Z, 0 ≤ i < 1 → 0 ≤ m_byteschanged_errno ptr_addrfile_handleF.out_file + i < 256

focused goal

Hnon :

Hn :

0 ≤ 1 < 2 ^ 64

Hreg :

∃base : Z reg : region, ptr_capfile_handleF.err_file = Objbase ∨ ptr_capfile_handleF.err_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live

Haccess :

access_resconversion_mem ptr_addrfile_handleF.err_file ptr_capfile_handleF.err_file 1 Read 1 = Someok

Hbytes :

∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.err_file + i < 256

Hrest :

⊢

access_reschanged_errno ptr_addrfile_handleF.err_file ptr_capfile_handleF.err_file 1 Read 1 = Someok ∧ ∀i : Z, 0 ≤ i < 1 → 0 ≤ m_byteschanged_errno ptr_addrfile_handleF.err_file + i < 256

all: split ; exact Haccess |

2 open

Hnon :

Hn :

0 ≤ 1 < 2 ^ 64

Hreg :

∃base : Z reg : region, ptr_capfile_handleF.out_file = Objbase ∨ ptr_capfile_handleF.out_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live

Haccess :

access_resconversion_mem ptr_addrfile_handleF.out_file ptr_capfile_handleF.out_file 1 Read 1 = Someok

Hbytes :

∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.out_file + i < 256

Hrest :

⊢

∀i : Z, 0 ≤ i < 1 → 0 ≤ m_byteschanged_errno ptr_addrfile_handleF.out_file + i < 256

focused goal

Hnon :

Hn :

0 ≤ 1 < 2 ^ 64

Hreg :

∃base : Z reg : region, ptr_capfile_handleF.err_file = Objbase ∨ ptr_capfile_handleF.err_file = Robase ∧ object_regionbase m_regionsconversion_mem = Somereg ∧ r_lifereg = Live

Haccess :

access_resconversion_mem ptr_addrfile_handleF.err_file ptr_capfile_handleF.err_file 1 Read 1 = Someok

Hbytes :

∀i : Z, 0 ≤ i < 1 → 0 ≤ m_bytesconversion_mem ptr_addrfile_handleF.err_file + i < 256

Hrest :

⊢

∀i : Z, 0 ≤ i < 1 → 0 ≤ m_byteschanged_errno ptr_addrfile_handleF.err_file + i < 256

all: intros i Hi ; assert i = 0 as → by lia ; vm_compute ; split ; congruence

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

destruct F.files_ready as Hout Herr

split ; clear Herr | clear Hout

all: destruct Hout as Hnon & Hn & Hreg & Haccess & Hbytes & Hrest || destruct Herr as Hnon & Hn & Hreg & Haccess & Hbytes & Hrest

all: split ; exact Hnon |

all: split ; exact Hn |

all: split ; exact Hreg |

all: split ; exact Haccess |

all: intros i Hi ; assert i = 0 as → by lia ; vm_compute ; split ; congruence

620Lemma changed_ready

∀ opened

libc_stream_readyλ_ _ ⇒ True changed_errno F.worldopened

Explore proof 26 tactics

Initial goal

⊢

∀opened : bool, libc_stream_readyλ_ : mem _ : libc_world ⇒ True changed_errno F.worldopened

intros opened

opened :

bool

⊢

libc_stream_readyλ_ : mem _ : libc_world ⇒ True changed_errno F.worldopened

destruct F.readyopened as Hrep & Hlocale & He & Hout & Herr & Hu & Hstatus & Hphase & Hdistinct & Hroots & _

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

libc_stream_readyλ_ : mem _ : libc_world ⇒ True changed_errno F.worldopened

split ; exact Hrep |

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True changed_errno libc_localeF.worldopened.1

∧

errno_cellchanged_errno libc_errnoF.worldopened.1

∧

stream_wfshutdown_stdoutF.worldopened.2

∧

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

∧

shutdown_uniqueF.worldopened.2

∧

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

∧

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

∧

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened ∧ stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened ∧ stdout_usablelibc_stdioF.worldopened.1 = true → libc_file_readychanged_errno libc_errnoF.worldopened.1 libc_stdout_filelibc_streamsF.worldopened.1 ∧ libc_stderr_openlibc_streamsF.worldopened.1 = true → libc_file_readychanged_errno libc_errnoF.worldopened.1 libc_stderr_filelibc_streamsF.worldopened.1 ∧ libc_release_separatedchanged_errno F.worldopened

split

2 open

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True changed_errno libc_localeF.worldopened.1

focused goal

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

errno_cellchanged_errno libc_errnoF.worldopened.1

∧

stream_wfshutdown_stdoutF.worldopened.2

∧

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

∧

shutdown_uniqueF.worldopened.2

∧

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

∧

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

∧

–destruct Hlocale as _ & _ & _ & _ & _ & Haligned

2 open

opened :

bool

Hrep :

True

Haligned :

Locale.locale_names_alignedlibc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True changed_errno libc_localeF.worldopened.1

deferred goal

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

errno_cellchanged_errno libc_errnoF.worldopened.1

∧

stream_wfshutdown_stdoutF.worldopened.2

∧

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

∧

shutdown_uniqueF.worldopened.2

∧

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

∧

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

∧

split ; exact I |

2 open

opened :

bool

Hrep :

True

Haligned :

Locale.locale_names_alignedlibc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

Forallwritable_spanchanged_errno Locale.locale_rootslibc_localeF.worldopened.1 ∧ ∀category : Z, Incategory Locale.locale_categories → ptr_addrLocale.locale_namelibc_localeF.worldopened.1 category ≠ 0 ∧ c_stringchanged_errno Locale.locale_namelibc_localeF.worldopened.1 category Locale.locale_textlibc_localeF.worldopened.1 category ∧ Forallλsource : span ⇒ readable_byteschanged_errno span_ptrsource span_sizesource Locale.locale_readslibc_localeF.worldopened.1 ∧ ForallLocale.locale_heapchanged_errno Locale.locale_ownedlibc_localeF.worldopened.1 ∧ Locale.locale_names_alignedlibc_localeF.worldopened.1

deferred goal

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

errno_cellchanged_errno libc_errnoF.worldopened.1

∧

stream_wfshutdown_stdoutF.worldopened.2

∧

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

∧

shutdown_uniqueF.worldopened.2

∧

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

∧

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

∧

split ; constructor |

2 open

opened :

bool

Hrep :

True

Haligned :

Locale.locale_names_alignedlibc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

∀category : Z, Incategory Locale.locale_categories → ptr_addrLocale.locale_namelibc_localeF.worldopened.1 category ≠ 0 ∧ c_stringchanged_errno Locale.locale_namelibc_localeF.worldopened.1 category Locale.locale_textlibc_localeF.worldopened.1 category ∧ Forallλsource : span ⇒ readable_byteschanged_errno span_ptrsource span_sizesource Locale.locale_readslibc_localeF.worldopened.1 ∧ ForallLocale.locale_heapchanged_errno Locale.locale_ownedlibc_localeF.worldopened.1 ∧ Locale.locale_names_alignedlibc_localeF.worldopened.1

deferred goal

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

errno_cellchanged_errno libc_errnoF.worldopened.1

∧

stream_wfshutdown_stdoutF.worldopened.2

∧

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

∧

shutdown_uniqueF.worldopened.2

∧

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

∧

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

∧

split

3 open

opened :

bool

Hrep :

True

Haligned :

Locale.locale_names_alignedlibc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

focused goal

opened :

bool

Hrep :

True

Haligned :

Locale.locale_names_alignedlibc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

Forallλsource : span ⇒ readable_byteschanged_errno span_ptrsource span_sizesource Locale.locale_readslibc_localeF.worldopened.1 ∧ ForallLocale.locale_heapchanged_errno Locale.locale_ownedlibc_localeF.worldopened.1 ∧ Locale.locale_names_alignedlibc_localeF.worldopened.1

deferred goal

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

errno_cellchanged_errno libc_errnoF.worldopened.1

∧

stream_wfshutdown_stdoutF.worldopened.2

∧

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

∧

shutdown_uniqueF.worldopened.2

∧

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

∧

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

∧

+intros category _

3 open

opened :

bool

Hrep :

True

Haligned :

Locale.locale_names_alignedlibc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

category :

⊢

ptr_addrLocale.locale_namelibc_localeF.worldopened.1 category ≠ 0 ∧ c_stringchanged_errno Locale.locale_namelibc_localeF.worldopened.1 category Locale.locale_textlibc_localeF.worldopened.1 category

deferred goal

opened :

bool

Hrep :

True

Haligned :

Locale.locale_names_alignedlibc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

deferred goal

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

errno_cellchanged_errno libc_errnoF.worldopened.1

∧

stream_wfshutdown_stdoutF.worldopened.2

∧

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

∧

shutdown_uniqueF.worldopened.2

∧

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

∧

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

∧

vm_compute

3 open

opened :

bool

Hrep :

True

Haligned :

Locale.locale_names_alignedlibc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

category :

⊢

4096 = 0 → False ∧ Someok = Someok ∧ Datatypes.Lt = Datatypes.Lt ∧ Datatypes.Lt = Datatypes.Lt ∧ 67 = 67 ∧ 0 = 0

deferred goal

opened :

bool

Hrep :

True

Haligned :

Locale.locale_names_alignedlibc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

deferred goal

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

errno_cellchanged_errno libc_errnoF.worldopened.1

∧

stream_wfshutdown_stdoutF.worldopened.2

∧

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

∧

shutdown_uniqueF.worldopened.2

∧

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

∧

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

∧

repeat split ; congruence

2 open

deferred goal

opened :

bool

Hrep :

True

Haligned :

Locale.locale_names_alignedlibc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

deferred goal

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

errno_cellchanged_errno libc_errnoF.worldopened.1

∧

stream_wfshutdown_stdoutF.worldopened.2

∧

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

∧

shutdown_uniqueF.worldopened.2

∧

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

∧

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

∧

+split ; constructor |

2 open

opened :

bool

Hrep :

True

Haligned :

Locale.locale_names_alignedlibc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

ForallLocale.locale_heapchanged_errno Locale.locale_ownedlibc_localeF.worldopened.1 ∧ Locale.locale_names_alignedlibc_localeF.worldopened.1

deferred goal

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

errno_cellchanged_errno libc_errnoF.worldopened.1

∧

stream_wfshutdown_stdoutF.worldopened.2

∧

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

∧

shutdown_uniqueF.worldopened.2

∧

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

∧

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

∧

split ; constructor | exact Haligned

deferred goal

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

errno_cellchanged_errno libc_errnoF.worldopened.1

∧

stream_wfshutdown_stdoutF.worldopened.2

∧

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

∧

shutdown_uniqueF.worldopened.2

∧

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

∧

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

∧

–split ; exact He |

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

stream_wfshutdown_stdoutF.worldopened.2

∧

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

∧

shutdown_uniqueF.worldopened.2

∧

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

∧

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

∧

split ; exact Hout |

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

∧

shutdown_uniqueF.worldopened.2

∧

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

∧

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

∧

split ; exact Herr |

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

shutdown_uniqueF.worldopened.2

∧

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

∧

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

∧

split ; exact Hu |

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

∧

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

∧

split ; exact Hstatus |

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

∧

split ; exact Hphase |

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

split ; exact Hdistinct |

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened ∧ stdout_usablelibc_stdioF.worldopened.1 = true → libc_file_readychanged_errno libc_errnoF.worldopened.1 libc_stdout_filelibc_streamsF.worldopened.1 ∧ libc_stderr_openlibc_streamsF.worldopened.1 = true → libc_file_readychanged_errno libc_errnoF.worldopened.1 libc_stderr_filelibc_streamsF.worldopened.1 ∧ libc_release_separatedchanged_errno F.worldopened

split ; exact Hroots |

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

stdout_usablelibc_stdioF.worldopened.1 = true → libc_file_readychanged_errno libc_errnoF.worldopened.1 libc_stdout_filelibc_streamsF.worldopened.1 ∧ libc_stderr_openlibc_streamsF.worldopened.1 = true → libc_file_readychanged_errno libc_errnoF.worldopened.1 libc_stderr_filelibc_streamsF.worldopened.1 ∧ libc_release_separatedchanged_errno F.worldopened

split ; intros _ ; exact proj1changed_files_ready |

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

libc_stderr_openlibc_streamsF.worldopened.1 = true → libc_file_readychanged_errno libc_errnoF.worldopened.1 libc_stderr_filelibc_streamsF.worldopened.1 ∧ libc_release_separatedchanged_errno F.worldopened

split ; intros _ ; exact proj2changed_files_ready |

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

⊢

libc_release_separatedchanged_errno F.worldopened

intros p file Hfile base Hin

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

p :

file :

libc_file

Hfile :

libc_file_atF.worldopened p = Somefile

base :

Hin :

Inbase file_ownedfile

⊢

¬Inbase Locale.locale_ownedlibc_localeF.worldopened.1 ∧ ∀q : ptr other : libc_file, libc_file_atF.worldopened q = Someother → file_handleother ≠ file_handlefile → ¬Inbase file_ownedother ∧ ¬available_capspan_ptr ≔ libc_stdoutF.worldopened; span_size ≔ 0 :: span_ptr ≔ libc_stderrF.worldopened; span_size ≔ 0 :: Locale.locale_private_sourceslibc_localeF.worldopened.1 ++ if same_filep libc_stdoutF.worldopened then match libc_file_atF.worldopened libc_stderrF.worldopened with Someother ⇒ file_sourcesother | None ⇒ [ ] end else match libc_file_atF.worldopened libc_stdoutF.worldopened with Someother ⇒ file_sourcesother | None ⇒ [ ] end [ ] changed_errno Objbase ∧ ¬available_capspan_ptr ≔ libc_stdoutF.worldopened; span_size ≔ 0 :: span_ptr ≔ libc_stderrF.worldopened; span_size ≔ 0 :: Locale.locale_private_sourceslibc_localeF.worldopened.1 ++ if same_filep libc_stdoutF.worldopened then match libc_file_atF.worldopened libc_stderrF.worldopened with Someother ⇒ file_sourcesother | None ⇒ [ ] end else match libc_file_atF.worldopened libc_stdoutF.worldopened with Someother ⇒ file_sourcesother | None ⇒ [ ] end [ ] changed_errno Robase

unfold libc_file_at in Hfile

opened :

bool

Hrep :

True

Hlocale :

Locale.locale_readyλ_ : mem _ : Locale.locale_world ⇒ True conversion_mem libc_localeF.worldopened.1

He :

errno_cellconversion_mem libc_errnoF.worldopened.1

Hout :

stream_wfshutdown_stdoutF.worldopened.2

Herr :

stream_wflibc_stderr_statelibc_streamsF.worldopened.1

Hu :

shutdown_uniqueF.worldopened.2

Hstatus :

−2 ^ 31 ≤ shutdown_statusF.worldopened.2 < 2 ^ 31

Hphase :

match shutdown_atF.worldopened.2 with

InCallbackactive

⇒

Inregistration_tokenactive shutdown_consumedF.worldopened.2

⇒

True

Hdistinct :

ptr_addrlibc_stdoutF.worldopened ≠ ptr_addrlibc_stderrF.worldopened

Hroots :

stdio_rootslibc_stdioF.worldopened.1 = libc_active_rootsF.worldopened

p :

file :

libc_file

Hfile :

same_filep libc_stdoutF.worldopened

→

stdout_usablelibc_stdioF.worldopened.1

→

Somelibc_stdout_filelibc_streamsF.worldopened.1

else

None

same_filep libc_stderrF.worldopened

→

libc_stderr_openlibc_streamsF.worldopened.1

→

Somelibc_stderr_filelibc_streamsF.worldopened.1

else

None

else

None

Somefile

base :

Hin :

Inbase file_ownedfile

⊢

destruct same_filep libc_stdoutF.worldopened ; destruct opened | destruct same_filep libc_stderrF.worldopened ; try discriminate ; injection Hfile as ← ; contradiction

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros opened

destruct F.readyopened as Hrep & Hlocale & He & Hout & Herr & Hu & Hstatus & Hphase & Hdistinct & Hroots & _

split ; exact Hrep |

split

–destruct Hlocale as _ & _ & _ & _ & _ & Haligned

split ; exact I |

split ; constructor |

split

+intros category _

vm_compute

repeat split ; congruence

+split ; constructor |

split ; constructor | exact Haligned

–split ; exact He |

split ; exact Hout |

split ; exact Herr |

split ; exact Hu |

split ; exact Hstatus |

split ; exact Hphase |

split ; exact Hdistinct |

split ; exact Hroots |

split ; intros _ ; exact proj1changed_files_ready |

split ; intros _ ; exact proj2changed_files_ready |

intros p file Hfile base Hin

unfold libc_file_at in Hfile

destruct same_filep libc_stdoutF.worldopened ; destruct opened | destruct same_filep libc_stderrF.worldopened ; try discriminate ; injection Hfile as ← ; contradiction

The contract allows success or EOF after settling the old FIFO. Both controls use the supplied HelloClose machine, not F.M.

643Lemma changed_close

∀ n

n = 0 ∨ n = stream_eof

A.M.E.invokefclose_contractF.model CVoid ArgP Const0 WPtrtoken_handleout InterpRuntime.start conversion_mem F.worldtrue [ ] CallReturnWIntn InterpRuntime.start changed_errno F.worldfalse

Proof 51 steps Qed

intros n Hn

eapply A.M.E.invoke_normal with born := [ ]

–split ; left ; reflexivity |

exists Const0

reflexivity

–apply full_open_admitted

–split

+eapply A.M.E.effects_local ; apply local_store_bytes | constructor

intros a Ha

left

exists errno_span5120 0

split ; left ; reflexivity |

split

∗exact proj1proj2proj1proj2proj2F.readytrue

∗unfold span_contains , errno_span

simpl

lia

+exists token_handleout, mkStreamInfo1 mkStreamByteOriented 65; 66 true 7, mkStreamByteOriented [ ] true

split ; reflexivity |

split ; apply F.close_settles |

split ; reflexivity |

split ; apply changed_ready |

split ; apply F.close_frame |

split ; split ; intros root | split ; intros x ; contradiction |

split ; reflexivity |

split ; left ; reflexivity |

intros a Hin Houtside

reflexivity

–exists token_handleout, mkStreamInfo1 mkStreamByteOriented 65; 66 true 7, mkStreamByteOriented [ ] true, n

split ; reflexivity |

split ; apply F.close_settles |

split ; reflexivity |

split ; exact Hn |

split ; reflexivity |

split ; intros base |

split ; apply changed_ready |

split ; apply F.close_frame |

auto

–intros why Hbad

discriminate

–intros values Hvalues

injection Hvalues as ←

split

+exists WIntn

split ; reflexivity |

destruct Hn as → | → ; reflexivity

+repeat constructor

–intros status Hbad

discriminate

675Example completed_close_preserves_pair: ∀n, n = 0 ∨ n = stream_eof → ∃ys, ys = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ _ ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap

Explore proof 37 tactics

Initial goal

⊢

∀n : Z, n = 0 ∨ n = stream_eof → ∃ys : listZ, ys = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap

intros n Hn

n :

Hn :

n = 0 ∨ n = stream_eof

⊢

∃ys : listZ, ys = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap

destruct A.close_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False out err 5120 0 out _ _ _ _ _ _ _ _ _ _ open_heap 0; 0; 0; 0 or_introleq_refl changed_closen Hn open_heap_agrees HelloErrnoChecks.disjoint HelloErrnoChecks.ready full_wi eq_refl as ys & Hlen & Hkeys & Hagree & _ & _ & Hwi

2 open

n :

Hn :

n = 0 ∨ n = stream_eof

⊢

∀l : piece v : pval, l, v ∈ byte_ps5120 0 0; 0; 0; 0 → open_heap !! l = Somev

focused goal

n :

Hn :

n = 0 ∨ n = stream_eof

ys :

listZ

Hlen :

lengthys = 4%nat

Hkeys :

byte_ps5120 0 ys.*1 = byte_ps5120 0 0; 0; 0; 0.*1

Hagree :

agreeschanged_errno <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap

Hwi :

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap

⊢

∃ys₀ : listZ, ys₀ = 4; 3; 2; 1 ∧ stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys₀ open_heap

–intros l v Hin

2 open

n :

Hn :

n = 0 ∨ n = stream_eof

l :

v :

Hin :

l, v ∈ byte_ps5120 0 0; 0; 0; 0

⊢

open_heap !! l = Somev

deferred goal

n :

Hn :

n = 0 ∨ n = stream_eof

ys :

listZ

Hlen :

lengthys = 4%nat

Hkeys :

byte_ps5120 0 ys.*1 = byte_ps5120 0 0; 0; 0; 0.*1

Hagree :

agreeschanged_errno <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap

Hwi :

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap

⊢

unfold open_heap , StreamHandleChecks.heap

2 open

n :

Hn :

n = 0 ∨ n = stream_eof

l :

v :

Hin :

l, v ∈ byte_ps5120 0 0; 0; 0; 0

⊢

deferred goal

n :

Hn :

n = 0 ∨ n = stream_eof

ys :

listZ

Hlen :

lengthys = 4%nat

Hkeys :

byte_ps5120 0 ys.*1 = byte_ps5120 0 0; 0; 0; 0.*1

Hagree :

agreeschanged_errno <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap

Hwi :

stream_tokens_wiλ_ : mem _ : libc_world ⇒ True out err 5120 0 changed_errno F.worldfalse <[PNametoken_keyout ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 ys open_heap

⊢

pose proof MemLogic.byte_ps_elem_ _ _ _ _ Hin as i & x & Hi & El & Ev

2 open

n :

Hn :

n = 0 ∨ n = stream_eof

l :

v :