rocq/theories/LibcStreamAdapter.v
World-owned callback snapshots, separate from locale string names. Main's output rules do not own/update these snapshots: callers must allocate or transfer them at callback entry.
A stable native handle and a reserved ghost key. The life region is separate from the mutable observations of FILE state.
The actual argument is recorded, including its capability. This permission observes openness, not a fixed pending count or FIFO. Use distinct descriptors/keys from exact snapshots; the native life piece is still exclusive and cannot be owned twice.
Even the fallback contains the actual argument, never an empty assertion or an unchanged stdout token for an unrelated pointer.
Ordinary completed closure does not freeze orientation or error. A resource prefix is not enough to establish this observation.
Absent keys impose no snapshot requirement. A present key rejects wrong handles, malformed values and stale observations. This reads the current heap, never a fixed callback-entry snapshot.
Both kinds preserve their meaning when the views they actually observe are unchanged. Open-only permissions do not observe FIFO.
Explore proof 12 tactics
Initial goal
intros d w w′ h Hlookup Hstate Hc
unfold stream_current in *
destruct h !! PNametoken_keyd as v | ; | exact I
destruct v ; try contradiction
2 openfocused goal
–destruct Hc as → Hobs
2 opendeferred goal
split ; reflexivity |
2 opendeferred goal
unfold stream_observation in *
2 opendeferred goal
destruct pending as physical fifo | ; rewrite Hlookup ; exact Hobs | rewrite Hstate ; exact Hobs
deferred goal
–destruct Hc as → Hopen
split ; reflexivity |
rewrite Hlookup
exact Hopen
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Keys below the codec key (-1) do not overlap locale categories. Actual freshness against other adapters is still required by allocation.
Explore proof 1 tactics
Initial goal
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 3 tactics
Initial goal
intros
split ; exact H |
split ; exact I
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 3 tactics
Initial goal
intros
split ; exact H |
split ; exact I
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 8 tactics
Initial goal
intros d w h pending fifo Hcurrent Howned
assert Hl : h !! PNametoken_keyd = SomeVStreamtoken_handled Somepending, fifo
2 openfocused goal
{apply Howned
2 opendeferred goal
unfold stream_ps
2 opendeferred goal
set_solver
deferred goal
unfold stream_current in Hcurrent
rewrite Hl in Hcurrent
exact proj2Hcurrent
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 8 tactics
Initial goal
intros d w h Hcurrent Howned
assert Hl : h !! PNametoken_keyd = SomeVStreamtoken_handled None
2 openfocused goal
{apply Howned
2 opendeferred goal
unfold closed_ps
2 opendeferred goal
set_solver
deferred goal
unfold stream_current in Hcurrent
rewrite Hl in Hcurrent
exact proj2Hcurrent
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 12 tactics
Initial goal
intros d p w h Hcurrent Howned
assert Hl : h !! PNametoken_keyd = SomeVStreamOpenp
2 openfocused goal
{apply Howned
2 opendeferred goal
unfold open_permission_ps
2 opendeferred goal
apply elem_of_cons
2 opendeferred goal
right
2 opendeferred goal
apply elem_of_cons
2 opendeferred goal
left
2 opendeferred goal
reflexivity
deferred goal
unfold stream_current in Hcurrent
rewrite Hl in Hcurrent
exact Hcurrent
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 3 tactics
Initial goal
intros
unfold permission_descriptor
destruct same_filep token_handleout ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Pure owned lookups already reject unknown and wrong-capability arguments, as required by HelloClose's pointer-universal premises.
Explore proof 7 tactics
Initial goal
intros rep out err b o p m w h _ & _ & _ & _ & _ & _ & Ho & He & _ Hl
assert Hc : stream_currentpermission_descriptorout err p w h
2 openfocused goal
{destruct permission_selectedout err p as → | → ; assumption
deferred goal
destruct stream_permission_current_ _ _ _ Hc Hl as Hp _
split ; exact Hp |
rewrite Hp
destruct permission_selectedout err p as → | → ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Recording independently live handles and CURRENT observations preserves the complete entry envelope. It does not recover unavailable fragments or change the world interpretation used by an existing WP.
Proof 57 steps Qed
Recording open-only permissions uses the same private/release frame as exact entry, but never installs an exact pending/FIFO observation.
Proof 57 steps Qed
Updating an unrelated ghost name changes no memory keys or stream lookups. Full-heap release separation remains intact.
Explore proof 28 tactics
Initial goal
intros rep out err b o m w h key value Hko Hke Howf & Hewf & Hbase & Hkey & Hout & Herr & Ho & He & Hprivate
assert Hmem : memory_keys_from<[PNamekey ≔ value]>h h
2 openfocused goal
{intros l v Hl Hmem
2 opendeferred goal
apply lookup_insert_Some in Hl as E _ | _ Hold ; subst l ; contradiction | eauto
deferred goal
assert Hdata : memory_keys_fromstream_data_heaptoken_baseout token_baseerr <[PNamekey ≔ value]>h stream_data_heaptoken_baseout token_baseerr h
2 openfocused goal
{intros l v Hl Hm
2 opendeferred goal
apply stream_data_lookup in Hl as Hl & Hno & Hne
2 opendeferred goal
destruct Hmeml v Hl Hm as old Hold
2 opendeferred goal
exists old
2 opendeferred goal
rewrite stream_data_lookup_ne ; assumption
deferred goal
split ; exact Howf |
split ; exact Hewf |
split ; exact Hbase |
split ; exact Hkey |
split ; exact Hout |
split ; exact Herr |
split
2 openfocused goal
{unfold stream_current in *
2 opendeferred goal
rewrite lookup_insert_ne ; exact Ho | congruence
deferred goal
split
2 openfocused goal
{unfold stream_current in *
2 opendeferred goal
rewrite lookup_insert_ne ; exact He | congruence
deferred goal
intros d Hd
destruct Hprivated Hd as Hwi Hrel
split ; eapply errno_wi_heap ; eauto |
intros base l v Hin Hl Hm
destruct Hmeml v Hl Hm as old Hold
exact Hrelbase l old Hin Hold Hm
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 14 tactics
Initial goal
intros Ha Hw Hol Hel Hoo Heo Hfresh
iIntros Hh
destruct Hw as Howf & Hewf & Hbase & Hkey & Hrest eqn: E
iMod pts_alloch open_permission_psout token_handleout ++ open_permission_pserr token_handleerr with Hh as [Hh Hps]
3 openfocused goal
focused goal
–clear - Hbase Hkey
3 opendeferred goal
deferred goal
cbn [ open_permission_ps app fmap fst ]
3 opendeferred goal
deferred goal
repeat constructor ; set_solver
2 opendeferred goal
deferred goal
–exact Hfresh
deferred goal
–rewrite pts_app
iDestruct Hps as [Ho He]
iModIntro
iFrame
iPureIntro
eapply permission_entry_frame ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Fresh ghost recording is not native allocation: both live_at facts and both current observations are independent premises. Freshness is against the authoritative heap, so no existing life is duplicated.
Explore proof 14 tactics
Initial goal
intros Ha Hw Hol Hel Hoo Heo Hfresh
iIntros Hh
destruct Hw as Howf & Hewf & Hbase & Hkey & Hrest eqn: E
iMod pts_alloch stream_psout op oq ++ stream_pserr ep eq with Hh as [Hh Hps]
3 openfocused goal
focused goal
–clear - Hbase Hkey
3 opendeferred goal
deferred goal
cbn [ stream_ps app fmap fst ]
3 opendeferred goal
deferred goal
repeat constructor ; set_solver
2 opendeferred goal
deferred goal
–exact Hfresh
deferred goal
–rewrite pts_app
iDestruct Hps as [Ho He]
iModIntro
iFrame
iPureIntro
eapply stream_entry_frame ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
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.
Explore proof 13 tactics
Initial goal
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
2 openfocused goal
–rewrite / stream_ps / pts /=
2 opendeferred goal
iDestruct Hlife as [Hlife _]
2 opendeferred goal
iFrame
deferred goal
–iPureIntro
unfold stream_current
rewrite lookup_insert_eq
exact conjeq_refl Hobs
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The other registered stream keeps its observable state and private inventory. Distinct addresses rule out stdout-priority aliasing.
Proof 38 steps Qed
Query contracts permit no allocation; in particular delegation cannot add a newly born release identity to either FILE.
Explore proof 2 tactics
Initial goal
intros sources roots releases s m born s′ m′ born′ He
induction He ; reflexivity | exact IHHe | contradiction
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Both mirrors and both private-memory frames survive either query. No unchanged-memory premise rules out the native locking writes.
Proof 65 steps Qed
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.
Proof 118 steps Qed
Token ownership plus the current world interpretation admits the concrete libc call; openness is not another consumer assumption.
Explore proof 6 tactics
Initial goal
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
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
This is pointer-universal admission from owned permission pieces, not an assumed choice of a registered handle.
Explore proof 8 tactics
Initial goal
intros rep requests wide out err b o p m w h Hw Hl
pose proof permission_selectedout err p as Hd
destruct Hw as _ & _ & _ & _ & _ & _ & Ho & He & Hprivate
assert Hc : stream_currentpermission_descriptorout err p w h by destruct Hd as → | → ; assumption
destruct stream_permission_current_ _ _ _ Hc Hl as Hp info Hinfo
pose proof proj1proj1Hprivate_ Hd as Hready
unfold libc_stream_at in Hinfo
destruct libc_file_atw p as file | eqn: Hfile ; eapply libc_stream_admitted ; eauto | discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The native representation's poll stability remains an explicit realization premise. Everything else follows from unchanged regions.
Explore proof 18 tactics
Initial goal
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 |
2 openfocused goal
–intros root a Hin Hspan l & v & reg & Hl & Hmem & E Hlive & Hrange
2 opendeferred goal
apply Hrootsroot a Hin Hspan
2 opendeferred goal
exists l, v, reg
2 opendeferred goal
split ; exact Hl |
2 opendeferred goal
split ; exact Hmem |
2 opendeferred goal
split ; | exact Hrange
2 opendeferred goal
split ; | exact Hlive
2 opendeferred goal
rewrite R.collector_live_ _ _ _ Hsp in E
2 opendeferred goal
exact E
deferred goal
–intros l v Hl Hnot
destruct l as base | base off | base off | key ; try exact I
2 openfocused goal
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
Explore proof 16 tactics
Initial goal
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
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Discriminating world observations: physical pending is seven, the logical FIFO has two bytes, and a completed close consumes both.
Explore proof 10 tactics
Initial goal
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 |
2 openfocused goal
–exists mkStreamInfo1 mkStreamByteOriented 65; 66 true 7
2 opendeferred goal
repeat split ; reflexivity
deferred goal
–exists mkStreamInfo2 stdout_initial 3
repeat split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 7 tactics
Initial goal
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
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 7 tactics
Initial goal
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
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 5 tactics
Initial goal
unfold stream_current
cbn [ out token_key ]
rewrite lookup_insert_eq
split ; reflexivity |
split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 5 tactics
Initial goal
unfold stream_current
cbn [ out token_key ]
rewrite lookup_insert_eq
intros _ & Hclosed & _
discriminate Hclosed
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 4 tactics
Initial goal
unfold stream_current
cbn [ out token_key ]
rewrite lookup_insert_eq
exact λH ⇒ H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The entire interpretation has an inhabitant with both open tokens, both native lives and owned errno, not merely each mirror alone.
Explore proof 9 tactics
Initial goal
intros l v Hmem Hl
apply stream_data_lookup in Hl as Hl & Hout & Herr
unfold open_heap in Hl
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |
unfold StreamHandleChecks.heap in Hl
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l ; contradiction |
exact Hl
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 25 tactics
Initial goal
assert Hkeys : ∀l v, stream_data_heap1024 2048 open_heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
2 openfocused goal
{intros l v Hl Hmem
2 opendeferred goal
apply private_lookupl v Hmem in Hl
2 opendeferred goal
unfold HelloErrnoChecks.heap in Hl
2 opendeferred goal
apply elem_of_list_to_map_2 in Hl
2 opendeferred goal
change l ∈ byte_ps5120 0 0; 0; 0; 0.*1
2 opendeferred goal
apply list_elem_of_fmap
2 opendeferred goal
exists l, v
2 opendeferred goal
auto
deferred goal
split ; split ; reflexivity | simpl ; lia |
split ; split ; reflexivity | simpl ; lia |
split ; discriminate |
split ; discriminate |
split ; reflexivity |
split ; reflexivity |
split ; exact proj1open_snapshots_current |
split ; exact proj2open_snapshots_current |
intros d → | →
2 openfocused goal
all: split ; | intros base l v Hin ; change Inbase [ ] in Hin ; contradiction
2 openfocused goal
all: split ; apply F.ready |
2 openfocused goal
all: split ; reflexivity |
2 openfocused goal
all: split ; intros root a Hin ; change Inroot [ ] in Hin ; contradiction |
2 openfocused goal
all: split ; intros base l v Hin ; change Inbase [ ] in Hin ; contradiction |
2 openfocused goal
all: intros l v Hl Hnot ; destruct l as base | base off | base off | key ; try exact I
4 openfocused goal
focused goal
focused goal
all: exfalso ; apply Hnot ; eapply Hkeys ; exact Hl | exact I
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 15 tactics
Initial goal
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
2 open–injection He as He Hv
2 opensubst l v
2 openunfold open_heap , StreamHandleChecks.heap
2 openrewrite lookup_insert_ne ; | discriminate
2 openrewrite lookup_insert_ne ; | discriminate
2 openapply lookup_insert_eq
–apply elem_of_cons in Hin as He | Hin ; | apply not_elem_of_nil in Hin ; contradiction
injection He as He Hv
subst l v
unfold open_heap
apply lookup_insert_eq
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 5 tactics
Initial goal
intros l v Hl
unfold open_heap in Hl
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l v ; exact I |
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l v ; exact I |
exact StreamHandleChecks.heap_agreesl v Hl
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An actual stderr query frames the paired interpretation even though stdout's physical count and outstanding FIFO differ from stderr's.
Explore proof 10 tactics
Initial goal
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 openfocused goal
{apply StreamHandleChecks.C.fpending_unchanged with file := F.err_file
4 openfocused goal
focused goal
deferred goal
–split ; left ; reflexivity |
4 opendeferred goal
deferred goal
deferred goal
exists Const0
4 opendeferred goal
deferred goal
deferred goal
reflexivity
3 opendeferred goal
deferred goal
deferred goal
–apply F.ready
2 opendeferred goal
deferred goal
–reflexivity
deferred goal
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
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The other query contract and stdout selection use the same frame.
Explore proof 10 tactics
Initial goal
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 openfocused goal
{apply StreamHandleChecks.C.ferror_unchanged with file := F.out_file
4 openfocused goal
focused goal
deferred goal
–split ; left ; reflexivity |
4 opendeferred goal
deferred goal
deferred goal
exists Const0
4 opendeferred goal
deferred goal
deferred goal
reflexivity
3 opendeferred goal
deferred goal
deferred goal
–apply F.ready
2 opendeferred goal
deferred goal
–reflexivity
deferred goal
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
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An actual authorized scalar write changes every errno byte, including the last one. It changes neither FILE storage nor locale strings.
Explore proof 9 tactics
Initial goal
destruct F.files_ready as Hout Herr
split ; clear Herr | clear Hout
2 openfocused goal
all: destruct Hout as Hnon & Hn & Hreg & Haccess & Hbytes & Hrest || destruct Herr as Hnon & Hn & Hreg & Haccess & Hbytes & Hrest
2 openfocused goal
all: split ; exact Hnon |
2 openfocused goal
all: split ; | destruct Hrest as Hp & _ & _ & _ & Ha ; split ; exact Hp | ; split ; constructor | ; split ; constructor | ; split ; constructor | exact Ha
2 openfocused goal
all: split ; exact Hn |
2 openfocused goal
all: split ; exact Hreg |
2 openfocused goal
all: split ; exact Haccess |
2 openfocused goal
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
Proof 26 steps Qed
The contract allows success or EOF after settling the old FIFO. Both controls use the supplied HelloClose machine, not F.M.
Proof 51 steps Qed
Explore proof 37 tactics
Initial goal
intros n Hn
destruct A.close_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False out err 5120 0 out _ _ _ _ _ _ _ _ _ _ open_heap 0; 0; 0; 0 or_introleq_refl changed_closen Hn open_heap_agrees HelloErrnoChecks.disjoint HelloErrnoChecks.ready full_wi eq_refl as ys & Hlen & Hkeys & Hagree & _ & _ & Hwi
2 openfocused goal
–intros l v Hin
2 opendeferred goal
unfold open_heap , StreamHandleChecks.heap
2 opendeferred goal
pose proof MemLogic.byte_ps_elem_ _ _ _ _ Hin as i & x & Hi & El & Ev
2 opendeferred goal
subst l v
2 opendeferred goal
rewrite lookup_insert_ne ; | discriminate
2 opendeferred goal
rewrite lookup_insert_ne ; | discriminate
2 opendeferred goal
rewrite lookup_insert_ne ; | discriminate
2 opendeferred goal
rewrite lookup_insert_ne ; | discriminate
2 opendeferred goal
unfold HelloErrnoChecks.heap
2 opendeferred goal
apply elem_of_list_to_map_1 ; | exact Hin
2 opendeferred goal
change base.NoDupPByte5120 0; PByte5120 1; PByte5120 2; PByte5120 3
2 opendeferred goal
repeat apply base.NoDup_cons_2 ; set_solver |
2 opendeferred goal
apply base.NoDup_nil_2
deferred goal
–exists ys
split ; | exact Hwi
destruct ys as | a | b | c | d rest ; try discriminate Hlen
assert rest = [ ] as → by destruct rest ; reflexivity | discriminate Hlen
assert Hbyte : ∀i x, PByte5120 i, VBytex ∈ byte_ps5120 0 a; b; c; d → x = m_byteschanged_errno 5120 + i
2 openfocused goal
{intros i x Hin
2 opendeferred goal
assert Hl : <[PName−2 ≔ VStreamtoken_handleout None]>overwritebyte_ps5120 0 a; b; c; d open_heap !! PByte5120 i = SomeVBytex
3 openfocused goal
deferred goal
{rewrite lookup_insert_ne ; | discriminate
3 opendeferred goal
deferred goal
change PByte5120 i, VBytex ∈ PByte5120 0, VBytea; PByte5120 1, VByteb; PByte5120 2, VBytec; PByte5120 3, VByted in Hin
3 opendeferred goal
deferred goal
repeat apply elem_of_cons in Hin as E | Hin ; injection E as Ei Ex ; subst i x ; cbn [ byte_ps overwrite fst snd ] ; repeat rewrite lookup_insert_ne ; | discriminate ; apply lookup_insert_eq |
3 opendeferred goal
deferred goal
apply not_elem_of_nil in Hin
3 opendeferred goal
deferred goal
contradiction
2 opendeferred goal
deferred goal
destruct Hagree_ _ Hl as _ Hvalue
2 opendeferred goal
destruct HvaluemkRegion5120 5128 Heap Live eq_refl eq_refl as _ & _ & Hv
2 opendeferred goal
symmetry
2 opendeferred goal
exact Hv
deferred goal
assert Ha : a = 4 by apply Hbyte0 a ; change PByte5120 0, VBytea ∈ PByte5120 0, VBytea; PByte5120 1, VByteb; PByte5120 2, VBytec; PByte5120 3, VByted ; apply list_elem_of_In ; simpl ; auto 10
assert Hb : b = 3 by apply Hbyte1 b ; change PByte5120 1, VByteb ∈ PByte5120 0, VBytea; PByte5120 1, VByteb; PByte5120 2, VBytec; PByte5120 3, VByted ; apply list_elem_of_In ; simpl ; auto 10
assert Hc : c = 2 by apply Hbyte2 c ; change PByte5120 2, VBytec ∈ PByte5120 0, VBytea; PByte5120 1, VByteb; PByte5120 2, VBytec; PByte5120 3, VByted ; apply list_elem_of_In ; simpl ; auto 10
assert Hd : d = 1 by apply Hbyte3 d ; change PByte5120 3, VByted ∈ PByte5120 0, VBytea; PByte5120 1, VByteb; PByte5120 2, VBytec; PByte5120 3, VByted ; apply list_elem_of_In ; simpl ; auto 10
subst
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Updating only the stream name would leave stale owned errno. The last byte alone distinguishes that incorrect replacement.
Explore proof 8 tactics
Initial goal
intros Ha
assert Hl : <[PName−2 ≔ VStreamtoken_handleout None]>open_heap !! PByte5120 3 = SomeVByte0
2 openfocused goal
{unfold open_heap , StreamHandleChecks.heap , HelloErrnoChecks.heap
2 opendeferred goal
repeat rewrite lookup_insert_ne ; | discriminate
2 opendeferred goal
apply lookup_insert_eq
deferred goal
destruct Ha_ _ Hl as _ Hbyte
destruct HbytemkRegion5120 5128 Heap Live eq_refl eq_refl as _ & _ & Hvalue
discriminate Hvalue
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Entry begins with actual errno ownership, but no recorded FILE lives or observations. The observations are selected from the current world.
Explore proof 5 tactics
Initial goal
intros l v Hl
unfold HelloErrnoChecks.heap in Hl
apply elem_of_list_to_map_2 in Hl
destruct MemLogic.byte_ps_elem_ _ _ _ _ Hl as i & x & _ & → & _
eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 29 tactics
Initial goal
assert Hkeys : ∀l v, stream_data_heap1024 2048 HelloErrnoChecks.heap !! l = Somev → mem_piecel → l ∈ errno_keys5120 0
2 openfocused goal
{intros l v Hl _
2 opendeferred goal
apply stream_data_lookup in Hl as Hl _
2 opendeferred goal
unfold HelloErrnoChecks.heap in Hl
2 opendeferred goal
apply elem_of_list_to_map_2 in Hl
2 opendeferred goal
change l ∈ byte_ps5120 0 0; 0; 0; 0.*1
2 opendeferred goal
apply list_elem_of_fmap
2 opendeferred goal
exists l, v
2 opendeferred goal
auto
deferred goal
split ; split ; reflexivity | simpl ; lia |
split ; split ; reflexivity | simpl ; lia |
split ; discriminate |
split ; discriminate |
split ; reflexivity |
split ; reflexivity |
split
2 openfocused goal
{unfold stream_current
2 opendeferred goal
destruct HelloErrnoChecks.heap !! PNametoken_keyout as v | eqn: E ; destruct entry_keys_ _ E as i Hbad ; discriminate Hbad | exact I
deferred goal
split
2 openfocused goal
{unfold stream_current
2 opendeferred goal
destruct HelloErrnoChecks.heap !! PNametoken_keyerr as v | eqn: E ; destruct entry_keys_ _ E as i Hbad ; discriminate Hbad | exact I
deferred goal
intros d → | →
2 openfocused goal
all: split ; | intros base l v Hin ; change Inbase [ ] in Hin ; contradiction
2 openfocused goal
all: split ; apply F.ready |
2 openfocused goal
all: split ; reflexivity |
2 openfocused goal
all: split ; intros root a Hin ; change Inroot [ ] in Hin ; contradiction |
2 openfocused goal
all: split ; intros base l v Hin ; change Inbase [ ] in Hin ; contradiction |
2 openfocused goal
all: intros l v Hl Hnot ; destruct l as base | base off | base off | key ; try exact I
4 openfocused goal
focused goal
focused goal
all: exfalso ; apply Hnot ; eapply Hkeys ; exact Hl | exact I
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 6 tactics
Initial goal
intros l v Hin
destruct HelloErrnoChecks.heap !! l as old | eqn: E ; | reflexivity
destruct entry_keys_ _ E as i →
apply list_elem_of_In in Hin
cbn [ stream_ps app out err token_base token_key ] in Hin
destruct Hin as Hbad | Hbad | Hbad | Hbad | ; discriminate Hbad
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Both real tokens are produced while independently owned errno is retained. This is not just a construction of a pure endpoint map.
Explore proof 13 tactics
Initial goal
iIntros [Hh Herrno]
iMod stream_entry_allocλ_ _ ⇒ True out err 5120 0 conversion_mem F.worldtrue HelloErrnoChecks.heap 7 65; 66 3 [ ] HelloErrnoChecks.heap_agrees entry_wi with Hh as (Hh & Ho & He & %Hnew)
6 openfocused goal
focused goal
focused goal
focused goal
focused goal
–split ; reflexivity
5 opendeferred goal
deferred goal
deferred goal
deferred goal
deferred goal
–split ; reflexivity
4 opendeferred goal
deferred goal
deferred goal
deferred goal
–exists mkStreamInfo1 mkStreamByteOriented 65; 66 true 7
4 opendeferred goal
deferred goal
deferred goal
repeat split ; reflexivity
3 opendeferred goal
deferred goal
deferred goal
–exists mkStreamInfo2 stdout_initial 3
3 opendeferred goal
deferred goal
repeat split ; reflexivity
2 opendeferred goal
deferred goal
–exact entry_fresh
deferred goal
–iModIntro
iExists _
2 openshelved goal
iFrame
done
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
An existing key cannot be freshly recorded, even if its native object is live and the caller has no fragment for the old value.
Explore proof 7 tactics
Initial goal
intros Hfresh
specialize HfreshPLive1024 VLivetoken_regionout
assert Hin : PLive1024, VLivetoken_regionout ∈ stream_psout 7 65; 66 ++ stream_pserr 3 [ ] by apply list_elem_of_In ; simpl ; auto
specialize HfreshHin
unfold StreamHandleChecks.heap in Hfresh
rewrite lookup_insert_eq in Hfresh
discriminate Hfresh
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 6 tactics
Initial goal
intros Hfresh
specialize HfreshPName−2 VStreamtoken_handleout Some7, 65; 66
assert Hin : PName−2, VStreamtoken_handleout Some7, 65; 66 ∈ stream_psout 7 65; 66 ++ stream_pserr 3 [ ] by apply list_elem_of_In ; simpl ; auto
specialize HfreshHin
rewrite lookup_insert_eq in Hfresh
discriminate Hfresh
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 3 tactics
Initial goal
intros rep b o m w h _ & _ & Hbad & _
apply Hbad
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 3 tactics
Initial goal
intros p & info & Hargs & _ & Hopen & _
injection Hargs as ←
discriminate Hopen
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Open-only callback permissions use separate keys from the exact -2/-3 snapshots, codec -1, locale 0..12 and getopt 64. The fixture contains NO exact snapshot names; two interpretations must not be conjoined to hide stale observations after diagnostics.
Explore proof 3 tactics
Initial goal
intros l Hmem
destruct l ; try contradiction
3 openall: unfold heap , T.open_heap ; repeat rewrite lookup_insert_ne ; | discriminate ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 5 tactics
Initial goal
intros l v Hl
unfold heap in Hl
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l v ; exact I |
apply lookup_insert_Some in Hl as He Hv | _ Hl ; subst l v ; exact I |
exact StreamHandleChecks.heap_agreesl v Hl
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 10 tactics
Initial goal
unfold stream_current , heap
cbn [ out err token_key ]
rewrite lookup_insert_eq
rewrite lookup_insert_ne ; | discriminate
rewrite lookup_insert_eq
split ; split ; reflexivity |
2 openfocused goal
–exists mkStreamInfo1 mkStreamByteOriented 65; 66 true 7
2 opendeferred goal
reflexivity
deferred goal
–exists mkStreamInfo2 stdout_initial 3
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 23 tactics
Initial goal
destruct T.full_wi as _ & _ & _ & _ & _ & _ & _ & _ & Hprivate
assert Hdata : memory_keys_fromstream_data_heap1024 2048 heap stream_data_heap1024 2048 T.open_heap
2 openfocused goal
{intros l v Hl Hmem
2 opendeferred goal
apply stream_data_lookup in Hl as Hl & Ho & He
2 opendeferred goal
exists v
2 opendeferred goal
rewrite stream_data_lookup_ne ; rewrite <- memory_lookup ; assumption | assumption | assumption
deferred goal
split ; split ; reflexivity | simpl ; lia |
split ; split ; reflexivity | simpl ; lia |
split ; discriminate |
split ; discriminate |
split ; reflexivity |
split ; reflexivity |
split ; exact proj1currents |
split ; exact proj2currents |
intros d → | →
2 openfocused goal
–destruct HprivateT.out or_introleq_refl as Hwi Hrel
2 opendeferred goal
split ; eapply errno_wi_heap ; exact Hwi | exact Hdata |
2 opendeferred goal
intros base l v Hin Hl Hmem
2 opendeferred goal
apply Hrelbase l v Hin ; rewrite <- memory_lookup ; assumption | exact Hmem
deferred goal
–destruct HprivateT.err or_introreq_refl as Hwi Hrel
split ; eapply errno_wi_heap ; exact Hwi | exact Hdata |
intros base l v Hin Hl Hmem
apply Hrelbase l v Hin ; rewrite <- memory_lookup ; assumption | exact Hmem
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Rejection follows from the PURE interface, without Iris falsehood.
Explore proof 2 tactics
Initial goal
intros rep b o m w h Hw Hl
destruct proj2permission_known_ _ _ _ _ _ _ _ _ Hw Hl as Hbad | Hbad ; discriminate Hbad
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 2 tactics
Initial goal
intros rep b o m w h Hw Hl
destruct proj2permission_known_ _ _ _ _ _ _ _ _ Hw Hl as Hbad | Hbad ; discriminate Hbad
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A new pending count/FIFO invalidates the old exact snapshot, while the open-only permission is still current. This is a world-view control, not a native diagnostic execution.
Explore proof 14 tactics
Initial goal
split
2 openfocused goal
–unfold stream_current , heap
2 opendeferred goal
cbn [ out token_key ]
2 opendeferred goal
rewrite lookup_insert_eq
2 opendeferred goal
split ; reflexivity |
2 opendeferred goal
exists mkStreamInfo1 mkStreamByteOriented 65; 66; 67 true 9
2 opendeferred goal
reflexivity
deferred goal
–unfold stream_current
cbn [ out token_key ]
rewrite lookup_insert_eq
intros _ & info & Hinfo & Hpending & _
change SomemkStreamInfo1 mkStreamByteOriented 65; 66; 67 true 9 = Someinfo in Hinfo
injection Hinfo as ←
discriminate Hpending
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 5 tactics
Initial goal
unfold stream_current , heap
cbn [ out token_key ]
rewrite lookup_insert_eq
intros _ & info & Hinfo
discriminate Hinfo
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 3 tactics
Initial goal
destruct T.stdout_error_preserves_pair as Hcall _
destruct A.query_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False out err 5120 0 out _ _ _ _ _ _ _ _ _ _ _ heap or_introleq_refl or_introleq_refl Hcall heap_agrees HelloErrnoChecks.disjoint HelloErrnoChecks.ready full_wi as _ & _ & _ & Hw
exact Hw
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.