rocq/theories/HelloClose.v
GNU Hello's closeout helpers through the separation logic. Module statics and the four errno bytes are owned pieces. Stream operations are premise triples, including their frame obligations; the null file name excludes the named-file diagnostic.
From iris.proofmode Require Import proofmode
From iris.base_logic.lib Require Import gen_heap
From iris.program_logic Require Import language weakestpre
From Stdlib Require Import ZArith Lia
From Stdlib Require String
From Nanofil Require Import Term Syntax Values Memory Runtime Ops Semantics Run StepRules Symbolic ExternalCalls ExternalMachine Pieces Heap ContractFrame Language Logic StringLogic MemLogic HelloModule HelloLeaf
Open Scope Z_scope
Open Scope list_scope
Arguments Z.add : simpl nomatch
Arguments Z.sub : simpl nomatch
Arguments Z.mul : simpl nomatch
Keep unknown arithmetic folded in computed instruction premises.
The stream-closing helper from the linked IR.
The exit callback from the linked IR.
A close_stream block.
A close_stdout block.
The canonical W loaded from four owned bytes, signed or unsigned.
A canonical W value fits its return channel.
Explore proof 4 tactics
close_stream binds its stream argument.
∀ p
invocationclose_stream_fn WPtrp = mkFrameclose_stream_fn TAtom"v0", WPtrp [ ] None EnterTAtom"start" None
Explore proof 1 tactics
Initial goal
p :
⊢
invocationclose_stream_fn WPtrp = fr_fn ≔ close_stream_fn; fr_env ≔ TAtom"v0", WPtrp; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ EnterTAtom"start" None
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
reflexivity
The stream helper over any runtime.
Import L LG SL ML HL
The instance used by all closeout triples.
Expressions in the linked program.
The represented errno cell is fixed in this thread.
The errno pointer used in the IR.
Errno lookup exports the represented cell without changing any pieces. Local rule for promotion to a libc logic module.
Proof 30 steps Qed
iIntros HK
iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ errno_location_contractworld cell rep [ ] True%I with [] [HK]
–apply linked_outside ; exact Hlinked | reflexivity
–apply linked_unbound ; exact Hlinked | reflexivity
–reflexivity
–exact Herrno
–reflexivity
–split ; right ; eexists ; reflexivity | reflexivity
–iIntros σ Hσ _
iDestruct Hσ as h [_ %Hσ]
iPureIntro
split ; reflexivity |
exact proj2proj2proj2Hσ
–done
–iNext
iIntros σ tr vs s′ m′ w′ Hi Hσ _
destruct M.E.errno_location_invocation_ _ _ _ _ _ _ _ _ _ _ _ _ _ Hi as _ & _ & _ & _ & _ & → & → & → & He
injection He as →
iDestruct Hσ as h [Hh %Hσ]
pose proof Hcell_ _ _ proj2proj2proj2Hσ as Ec
iModIntro
iExists _
iSplit
+iPureIntro
rewrite Ec
reflexivity
+iSplitL Hh ; iExists h ; iFrame ; done |
iExact HK
A four-byte load from owned memory. Local rule for promotion to MemLogic.v; it needs neither a world fact nor eight-byte ownership.
∀ f e ls lab d v rest j b reg o xs Φ
Proof 36 steps Qed
intros Hv Ha Hlen
iIntros Hl Hx HK
–intros m fuel Hag & _
destruct Hag as Hl Hx
cbn [ agree_piece fst snd ] in Hl
destruct xs as | a | c | dd | z | u xs ; try discriminate Hlen
pose proof byte_ps_agree_ _ _ _ _ 0%nat a Hl Hx eq_refl as E0 & H0 & _
pose proof byte_ps_agree_ _ _ _ _ 1%nat c Hl Hx eq_refl as E1 & _
pose proof byte_ps_agree_ _ _ _ _ 2%nat dd Hl Hx eq_refl as E2 & _
pose proof byte_ps_agree_ _ _ _ _ 3%nat z Hl Hx eq_refl as E3 & _ & H3
apply rule_let with classes := A xs := WPtrmkPtrb + o Objb w := WIntclose_wa; c; dd; z ; reflexivity | reflexivity | cbn [ map2_option ] ; rewrite Hv ; reflexivity |
assert Er : raw_addressb + o 0 = b + o by unfold raw_address ; rewrite Z.add_0_r ; apply Z.mod_small ; exact Ha
{apply access_obj_ _ reg ; exact proj1Hl | lia | cbn in H3 ; lia | apply Z.mod_1_r
cbn - [ access_res raw_address load_bytes extension ]
rewrite Er
unfold int_load_res
cbn - [ access_res load_bytes extension ]
rewrite Ea
change SomeOpResRValWIntextensionSw load_bytesm b + o 4 mod 2 ^ 32 m = SomeOpResRValWIntclose_wa; c; dd; z m
change SomeOpResRValWIntextensionSw m_bytesm b + o + 3 × 256 + m_bytesm b + o + 2 × 256 + m_bytesm b + o + 1 × 256 + m_bytesm b + o + 0 mod 2 ^ 32 m = SomeOpResRValWIntclose_wa; c; dd; z m
cbn [ Z.of_nat ] in E0 , E1 , E2 , E3
rewrite E0 E1 E2 E3
reflexivity
An invocation frame, promoted locally to an Iris call rule. The pure endpoint premise describes the whole authoritative heap after the call, including updates to pieces the caller handed over. Local bridge for promotion to Logic.v.
∀ f e ls lab d k g args rest j spec xs ps after : listZ → listpiece × pval good : Z → listZ → Prop Φ
lookupg ge_globalsge = None
registryg = Somespec
contract_returnsspec = RClassk
map_optionarg_xge e args = Somexs
contract_abispec CResultd k args
∀m w h, wim w h → ∀l v, l, v ∈ ps → h !! l = Somev → contract_prespec xs m w
∀s m w h tr vs s′ m′ w′, agreesm h → live_disjointm → R.readys m → wim w h → ∀l v, l, v ∈ ps → h !! l = Somev → M.E.invokespec CResultd k args xs s m w tr CallReturnvs s′ m′ w′ → ∃n ys, vs = WIntn ∧ 0 ≤ n < 2 ^ if class_eqbk W then 32 else 64 ∧ goodn ys ∧ afterys.*1 = ps.*1 ∧ agreesm′ overwriteafterys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwriteafterys h
Proof 25 steps Qed
intros Hfn Hg Hfree Hreg Hret Hk Hargs Habi Hpre Hpost
iIntros Hps HK
iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ spec xs ptsps with Hps [HK] ; exact Hfn | exact Hg | exact Hfree | exact Hreg | exact Hargs | exact Habi | |
–iNext
iIntros σ tr vs s′ m′ w′ Hi Hσ Hps
iDestruct Hσ as h [Hh %Hσ]
destruct Hσ as Ha & Hd & Hr & Hw
iDestruct pts_lookup with Hh Hps as %Hl
destruct Hpost_ _ _ _ _ _ _ _ _ Ha Hd Hr Hw Hl Hi as n & ys & → & Hn & Hgood & Hkeys & Ha′ & Hd′ & Hr′ & Hw′
iMod pts_update with Hh Hps as [Hh Hps] ; exact Hkeys |
iModIntro
iExists _
iSplit
+iPureIntro
unfold external_env
rewrite Hret
destruct Hk as → | → ; cbn [ external_outcome returned_env site_result word_at_class modulus ] ; rewrite Z.mod_small ; reflexivity | exact Hn | reflexivity | exact Hn
Stream admission and consumption are represented by ghost pieces; fclose replaces their values with closed-state pieces of the same keys, rather than restoring usability of the stream.
Ownership of a usable stream's represented pieces.
Query specs, including their exact ABI and pure frame obligations. The query preserves the original owned pieces and libc world.
208Context Hquery_ret : ∀g k, g = TAtom"__fpending" ∧ k = L ∨ g = TAtom"ferror" ∧ k = W → contract_returnsquery_specg = RClassk
208Context Hquery_abi : ∀g k d v, g = TAtom"__fpending" ∧ k = L ∨ g = TAtom"ferror" ∧ k = W → contract_abiquery_specg CResultd k ArgP v
208Context Hquery_post : ∀g k d v p xs s m w h tr vs s′ m′ w′, g = TAtom"__fpending" ∧ k = L ∨ g = TAtom"ferror" ∧ k = W → agreesm h → live_disjointm → R.readys m → wim w h → ∀l v, l, v ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev → M.E.invokequery_specg CResultd k ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n, vs = WIntn ∧ 0 ≤ n < 2 ^ if class_eqbk W then 32 else 64 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
fclose's spec consumes usable stream pieces, returning closed pieces and arbitrary four-byte errno contents. Its frame premise includes readiness, separation and libc's world, not just the returned value.
230Context Hfclose_pre : ∀p xs m w h, wim w h → ∀l v, l, v ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev → lengthxs = 4%nat → contract_prefclose_spec WPtrp m w
230Context Hfclose_post : ∀d v p xs s m w h tr vs s′ m′ w′, agreesm h → live_disjointm → R.readys m → wim w h → ∀l v, l, v ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev → M.E.invokefclose_spec CResultd W ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n ys, vs = WIntn ∧ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat ∧ closed_psp ++ byte_pseb eo ys.*1 = stream_psp ++ byte_pseb eo xs.*1 ∧ agreesm′ overwriteclosed_psp ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwriteclosed_psp ++ byte_pseb eo ys h
Derive the two query call-site triples from their raw contracts.
∀ g k f e ls lab d v rest j p xs Φ
lengthxs = 4%nat
Proof 31 steps Qed
intros Hwhich f e ls lab d v rest j p xs Φ Hv Hlen
iIntros Hs Hx HK
iApply wp_close_contract_ _ _ _ _ k g _ _ _ query_specg WPtrp stream_psp ++ byte_pseb eo xs λ_ ⇒ stream_psp ++ byte_pseb eo xs λn _ ⇒ 0 ≤ n < 2 ^ if class_eqbk W then 32 else 64 with [Hs Hx] [HK]
–destruct Hwhich as → → | → → ; apply linked_outside ; exact Hlinked | reflexivity | exact Hlinked | reflexivity
–destruct Hwhich as → → | → → ; apply linked_unbound ; exact Hlinked | reflexivity | exact Hlinked | reflexivity
–destruct Hwhich as → → | → → ; reflexivity
–apply Hquery_reg with k
exact Hwhich
–apply Hquery_ret
exact Hwhich
–destruct Hwhich as _ → | _ → ; auto
–apply Hquery_abi
exact Hwhich
–intros m w h Hw Hl
exact Hquery_pre_ _ _ _ _ _ _ Hwhich Hw Hl Hlen
–intros s m w h tr vs s′ m′ w′ Ha Hd Hr Hw Hl Hi
destruct Hquery_post_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hwhich Ha Hd Hr Hw Hl Hi as n & Hvs & Hn & Ha′ & Hd′ & Hr′ & Hw′
exists n, xs
rewrite overwrite_id_ h Hl
repeat split ; try assumption ; try reflexivity ; tauto
–rewrite pts_app
iFrame
Derive the consuming close call-site triple from its raw contract.
∀ f e ls lab d v rest j p xs Φ
Proof 28 steps Qed
intros f e ls lab d v rest j p xs Φ Hv Hlen
iIntros Hs Hx HK
iApply wp_close_contract_ _ _ _ _ W TAtom"fclose" _ _ _ fclose_spec WPtrp stream_psp ++ byte_pseb eo xs λys ⇒ closed_psp ++ byte_pseb eo ys λn ys ⇒ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat with [Hs Hx] [HK]
–apply linked_outside ; exact Hlinked | reflexivity
–apply linked_unbound ; exact Hlinked | reflexivity
–reflexivity
–exact Hfclose_reg
–exact Hfclose_ret
–auto
–apply Hfclose_abi
–intros m w h Hw Hl
exact Hfclose_pre_ _ _ _ _ Hw Hl Hlen
–intros s m w h tr vs s′ m′ w′ Ha Hd Hr Hw Hl Hi
destruct Hfclose_post_ _ _ _ _ _ _ _ _ _ _ _ _ Ha Hd Hr Hw Hl Hi as n & ys & Hvs & Hn & Hys & Hkeys & Ha′ & Hd′ & Hr′ & Hw′
exists n, ys
cbn [ class_eqb ]
repeat split ; try assumption ; try reflexivity ; tauto
–rewrite pts_app
iFrame
Storing zero into owned errno preserves libc's world interpretation.
The errno cell is inside the represented address space.
Find a stream-close block without unfolding the module in a proof.
A pure instruction, with the environment kept abstract.
iApply wp_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise | ; iNext ; gen_env
After the error decision, close_stream returns zero or EOF, clearing errno only when an earlier error accompanies a successful fclose.
∀ e n t xs Φ
0 ≤ n < 2 ^ 32
t = 0 ∨ t = 1
lengthxs = 4%nat
Proof 47 steps Qed
intros Hn Ht Hrange Ht01 Hlen
iIntros Hl Hx HΦ
destruct Ht01 as → | →
–iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
cs_enter "L19"
iApply wp_ret ; reflexivity | reflexivity |
iNext
iApply HΦ $! 0 xs with [%] Hl Hx
auto
–iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
cs_enter "L17"
destruct Z.eq_decn 0 as [ ->| Hnz ]
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
cs_enter "L38"
iApply wp_close_errno
iNext
iApply wp_check with Hl ; reflexivity | word_premise | reflexivity | unfold ep ; addr_premise | unfold ep ; addr_premise | unfold ep ; addr_premise |
iNext
iIntros Hl
iApply wp_raw_store_w with Hl Hx ; word_premise | word_premise | reflexivity | unfold ep ; addr_premise | exact Hlen | apply Kerrno |
iNext
iIntros Hl Hx
iApply wp_goto
iNext
cs_enter "L40"
iApply wp_ret ; reflexivity | reflexivity |
iNext
iApply HΦ $! 4294967295 le_bytes0 4 with [%] Hl Hx
split ; auto | apply length_le_bytes
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
cs_enter "L40"
iApply wp_ret ; reflexivity | reflexivity |
iNext
iApply HΦ $! 4294967295 xs with [%] Hl Hx
auto
Hand the merged error flag to the shared return blocks.
cs_enter "L22" ; gen_env ; iApply close_stream_L22_ n t with Hl Hx HΦ ; word_premise | word_premise | exact Hn | auto | exact Hlen
close_stream consumes a usable stream and returns zero or EOF. It returns ownership of errno, whose contents may have changed. Sticky error, pending data, fclose failure and EBADF take distinct paths.
Proof 63 steps Qed
intros Hlen
iIntros Hs Hl Hx HΦ
rewrite close_stream_entry
cs_enter "start"
iApply HqueryTAtom"__fpending" L with Hs Hx ; left ; auto | word_premise | exact Hlen |
iNext
iIntros pending Hpending Hs Hx
cbn [ class_eqb ] in Hpending
iApply HqueryTAtom"ferror" W with Hs Hx ; right ; auto | word_premise | exact Hlen |
iNext
iIntros err Herr Hs Hx
cbn [ class_eqb ] in Herr
iApply Hfclose with Hs Hx ; word_premise | exact Hlen |
iNext
iIntros n ys Hn Hys Hx
destruct Z.eq_decerr 0 as Herr0 | Herr0
–iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
cs_enter "L21"
destruct Z.eq_decn 0 as Hn0 | Hn0
+iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
cs_finish n 0 Hn Hys
+iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
cs_enter "L24"
destruct Z.eq_decpending 0 as Hp0 | Hp0
∗iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
cs_enter "L27"
iApply wp_close_errno
iNext
iApply wp_check with Hl ; reflexivity | word_premise | reflexivity | unfold ep ; addr_premise | unfold ep ; addr_premise | unfold ep ; addr_premise |
iNext
iIntros Hl
iApply wp_close_load_w with Hl Hx ; word_premise | exact Herange | exact Hys |
iNext
iIntros Hl Hx
pose proof close_w_rangeys as Hwr
--cs_finish n 0 Hn Hys
--cs_finish n 1 Hn Hys
∗iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
cs_finish n 1 Hn Hys
–iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
cs_finish n 1 Hn Hys
Hello's read-only unnamed-file diagnostic strings.
The write-error text.
The caller hands the diagnostic's represented string pieces to error; they return unchanged while errno may change.
421Context Herror_post : ∀v fmtv txtv n xs s m w h tr vs s′ m′ w′, lengthxs = 4%nat → agreesm h → live_disjointm → R.readys m → wim w h → ∀l v, l, v ∈ diag_ps ++ byte_pseb eo xs → h !! l = Somev → M.E.invokeerror_spec CVoid ArgW Const0; ArgW v; ArgP fmtv; ArgP txtv WInt0; WIntn; WPtrfmt; WPtrtext s m w tr CallReturnvs s′ m′ w′ → ∃ys, vs = [ ] ∧ lengthys = 4%nat ∧ diag_ps ++ byte_pseb eo ys.*1 = diag_ps ++ byte_pseb eo xs.*1 ∧ agreesm′ overwritediag_ps ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritediag_ps ++ byte_pseb eo ys h
error with zero status returns void; it never substitutes an exit for the following _exit. Resource terminals need no continuation.
∀ f e ls lab v fmtv txtv rest j n xs Φ
0 ≤ n < 2 ^ 32
lengthxs = 4%nat
Proof 37 steps Qed
intros Hv Hfmt Htext Hn Hlen
iIntros Hd Hx HK
iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ error_spec WInt0; WIntn; WPtrfmt; WPtrtext ptsdiag_ps ++ byte_pseb eo xs with [Hd Hx] [HK]
–apply linked_outside ; exact Hlinked | reflexivity
–apply linked_unbound ; exact Hlinked | reflexivity
–reflexivity
–exact Herror_reg
–apply Herror_abi
–iIntros σ Hσ Hps
iDestruct Hσ as h [Hh %Hσ]
iDestruct pts_lookup with Hh Hps as %Hl
iPureIntro
apply Herror_pre_ _ _ _ _ Hn Hlen proj1Hσ proj2proj2proj2Hσ Hl
–rewrite pts_app
iFrame
–iNext
iIntros σ tr vs s′ m′ w′ Hi Hσ Hps
iDestruct Hσ as h [Hh %Hσ]
destruct Hσ as Ha & Hd & Hr & Hw
iDestruct pts_lookup with Hh Hps as %Hl
destruct Herror_post_ _ _ _ _ _ _ _ _ _ _ _ _ _ Hlen Ha Hd Hr Hw Hl Hi as ys & → & Hys & Hkeys & Ha′ & Hd′ & Hr′ & Hw′
iMod pts_update with Hh Hps as [Hh Hps] ; exact Hkeys |
iModIntro
iExists e
iSplit
_exit's raw contract admits a canonical status and has no ordinary return endpoint. Its actual process-exit semantics belong to Ending.
479Context Hexit_post : ∀args n s m w tr vs s′ m′ w′, M.E.invokeexit_spec CVoid args WIntn s m w tr CallReturnvs s′ m′ w′ → False
An admissible _exit call is safe under every postcondition.
Proof 19 steps Qed
intros Hv Hn
iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ exit_spec WIntn True%I with [] []
–apply linked_outside ; exact Hlinked | reflexivity
–apply linked_unbound ; exact Hlinked | reflexivity
–reflexivity
–exact Hexit_reg
–apply Hexit_abi
–done
Load a stream pointer while borrowing its life from the stream's represented pieces, without duplicating that linear life token.
∀ f e ls lab d v rest j b reg p Φ
Proof 26 steps Qed
intros pb & pr & ps & Hcap & Hps Hv Hb Hb8 Hp
iIntros Hl Hc Hs HK
iApply wp_raw_load_pointer_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ pr with Hl Hc [Hpl] [HK Hrest]
–reflexivity
–reflexivity
–rewrite Z.add_0_r
exact Hb8
–exact Hp
–rewrite / live_cap Hcap
iExact Hpl
The null file-name pointer is eight owned zero bytes and a null aux slot. This is a module invariant, not a fact about libc's world.
Explore proof 3 tactics
Initial goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
eb, eo :
Z
er :
cell :
world → ptr
rep :
mem → world → Prop
Herrno :
registryTAtom"__errno_location" = Someerrno_location_contractworld cell rep
Hlinked :
Hrep :
∀m : mem w : world h : gmappiece pval, wim w h → repm w ∧ errno_cellm cellw
Hquery_reg :
Hquery_ret :
Hquery_abi :
Hquery_pre :
Hquery_post :
∀g : term k : class d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, g = TAtom"__fpending" ∧ k = L ∨ g = TAtom"ferror" ∧ k = W → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokequery_specg CResultd k ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z, vs = WIntn ∧ 0 ≤ n < 2 ^ if class_eqbk W then 32 else 64 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
fclose_spec :
contractworld
Hfclose_reg :
registryTAtom"fclose" = Somefclose_spec
Hfclose_ret :
contract_returnsfclose_spec = RClassW
Hfclose_pre :
Hfclose_post :
∀d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokefclose_spec CResultd W ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z ys : listZ, vs = WIntn ∧ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat ∧ closed_psp ++ byte_pseb eo ys.*1 = stream_psp ++ byte_pseb eo xs.*1 ∧ agreesm′ overwriteclosed_psp ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwriteclosed_psp ++ byte_pseb eo ys h
Kerrno :
Heo :
0 ≤ eo
Herange :
0 ≤ eb + eo < 2 ^ 64
Heend :
eb + eo + 4 ≤ r_ender
He48 :
r_ender ≤ 2 ^ 48
error_spec :
contractworld
Herror_reg :
registryTAtom"error" = Someerror_spec
Herror_ret :
contract_returnserror_spec = RVoid
Herror_abi :
Herror_pre :
Herror_post :
∀v fmtv txtv : value n : Z xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, lengthxs = 4%nat → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ diag_ps ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokeerror_spec CVoid ArgW Const0; ArgW v; ArgP fmtv; ArgP txtv WInt0; WIntn; WPtrfmt; WPtrtext s m w tr CallReturnvs s′ m′ w′ → ∃ys : listZ, vs = [ ] ∧ lengthys = 4%nat ∧ diag_ps ++ byte_pseb eo ys.*1 = diag_ps ++ byte_pseb eo xs.*1 ∧ agreesm′ overwritediag_ps ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritediag_ps ++ byte_pseb eo ys h
exit_spec :
contractworld
Hexit_reg :
registryTAtom"_exit" = Someexit_spec
Hexit_ret :
contract_returnsexit_spec = RVoid
Hexit_abi :
∀v : value, contract_abiexit_spec CVoid ArgW v
Hexit_pre :
∀n : Z m : mem w : world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → wim w h → contract_preexit_spec WIntn m w
Hexit_post :
∀args : listarg n : Z s : R.state m : mem w : world tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, M.E.invokeexit_spec CVoid args WIntn s m w tr CallReturnvs s′ m′ w′ → False
change ptsHeap.cell65584 0 0 ∗ ptsPAux65584 0, VAuxCNone ⊣⊢ ptsPAux65584 0, VAuxCNone ++ Heap.cell65584 0 0
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
eb, eo :
Z
er :
cell :
world → ptr
rep :
mem → world → Prop
Herrno :
registryTAtom"__errno_location" = Someerrno_location_contractworld cell rep
Hlinked :
Hrep :
∀m : mem w : world h : gmappiece pval, wim w h → repm w ∧ errno_cellm cellw
Hquery_reg :
Hquery_ret :
Hquery_abi :
Hquery_pre :
Hquery_post :
∀g : term k : class d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, g = TAtom"__fpending" ∧ k = L ∨ g = TAtom"ferror" ∧ k = W → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokequery_specg CResultd k ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z, vs = WIntn ∧ 0 ≤ n < 2 ^ if class_eqbk W then 32 else 64 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
fclose_spec :
contractworld
Hfclose_reg :
registryTAtom"fclose" = Somefclose_spec
Hfclose_ret :
contract_returnsfclose_spec = RClassW
Hfclose_pre :
Hfclose_post :
∀d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokefclose_spec CResultd W ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z ys : listZ, vs = WIntn ∧ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat ∧ closed_psp ++ byte_pseb eo ys.*1 = stream_psp ++ byte_pseb eo xs.*1 ∧ agreesm′ overwriteclosed_psp ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwriteclosed_psp ++ byte_pseb eo ys h
Kerrno :
Heo :
0 ≤ eo
Herange :
0 ≤ eb + eo < 2 ^ 64
Heend :
eb + eo + 4 ≤ r_ender
He48 :
r_ender ≤ 2 ^ 48
error_spec :
contractworld
Herror_reg :
registryTAtom"error" = Someerror_spec
Herror_ret :
contract_returnserror_spec = RVoid
Herror_abi :
Herror_pre :
Herror_post :
∀v fmtv txtv : value n : Z xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, lengthxs = 4%nat → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ diag_ps ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokeerror_spec CVoid ArgW Const0; ArgW v; ArgP fmtv; ArgP txtv WInt0; WIntn; WPtrfmt; WPtrtext s m w tr CallReturnvs s′ m′ w′ → ∃ys : listZ, vs = [ ] ∧ lengthys = 4%nat ∧ diag_ps ++ byte_pseb eo ys.*1 = diag_ps ++ byte_pseb eo xs.*1 ∧ agreesm′ overwritediag_ps ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritediag_ps ++ byte_pseb eo ys h
exit_spec :
contractworld
Hexit_reg :
registryTAtom"_exit" = Someexit_spec
Hexit_ret :
contract_returnsexit_spec = RVoid
Hexit_abi :
∀v : value, contract_abiexit_spec CVoid ArgW v
Hexit_pre :
∀n : Z m : mem w : world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → wim w h → contract_preexit_spec WIntn m w
Hexit_post :
∀args : listarg n : Z s : R.state m : mem w : world tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, M.E.invokeexit_spec CVoid args WIntn s m w tr CallReturnvs s′ m′ w′ → False
rewrite pts_app
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
eb, eo :
Z
er :
cell :
world → ptr
rep :
mem → world → Prop
Herrno :
registryTAtom"__errno_location" = Someerrno_location_contractworld cell rep
Hlinked :
Hrep :
∀m : mem w : world h : gmappiece pval, wim w h → repm w ∧ errno_cellm cellw
Hquery_reg :
Hquery_ret :
Hquery_abi :
Hquery_pre :
Hquery_post :
∀g : term k : class d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, g = TAtom"__fpending" ∧ k = L ∨ g = TAtom"ferror" ∧ k = W → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokequery_specg CResultd k ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z, vs = WIntn ∧ 0 ≤ n < 2 ^ if class_eqbk W then 32 else 64 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
fclose_spec :
contractworld
Hfclose_reg :
registryTAtom"fclose" = Somefclose_spec
Hfclose_ret :
contract_returnsfclose_spec = RClassW
Hfclose_pre :
Hfclose_post :
∀d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokefclose_spec CResultd W ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z ys : listZ, vs = WIntn ∧ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat ∧ closed_psp ++ byte_pseb eo ys.*1 = stream_psp ++ byte_pseb eo xs.*1 ∧ agreesm′ overwriteclosed_psp ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwriteclosed_psp ++ byte_pseb eo ys h
Kerrno :
Heo :
0 ≤ eo
Herange :
0 ≤ eb + eo < 2 ^ 64
Heend :
eb + eo + 4 ≤ r_ender
He48 :
r_ender ≤ 2 ^ 48
error_spec :
contractworld
Herror_reg :
registryTAtom"error" = Someerror_spec
Herror_ret :
contract_returnserror_spec = RVoid
Herror_abi :
Herror_pre :
Herror_post :
∀v fmtv txtv : value n : Z xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, lengthxs = 4%nat → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ diag_ps ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokeerror_spec CVoid ArgW Const0; ArgW v; ArgP fmtv; ArgP txtv WInt0; WIntn; WPtrfmt; WPtrtext s m w tr CallReturnvs s′ m′ w′ → ∃ys : listZ, vs = [ ] ∧ lengthys = 4%nat ∧ diag_ps ++ byte_pseb eo ys.*1 = diag_ps ++ byte_pseb eo xs.*1 ∧ agreesm′ overwritediag_ps ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritediag_ps ++ byte_pseb eo ys h
exit_spec :
contractworld
Hexit_reg :
registryTAtom"_exit" = Someexit_spec
Hexit_ret :
contract_returnsexit_spec = RVoid
Hexit_abi :
∀v : value, contract_abiexit_spec CVoid ArgW v
Hexit_pre :
∀n : Z m : mem w : world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → wim w h → contract_preexit_spec WIntn m w
Hexit_post :
∀args : listarg n : Z s : R.state m : mem w : world tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, M.E.invokeexit_spec CVoid args WIntn s m w tr CallReturnvs s′ m′ w′ → False
apply bi.sep_comm
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
The concrete module cells; libc supplies only stdout and stderr's pointer-cell locations. All these pieces are handed back on return.
Closeout's owned module memory and the imported pointer cells.
The module's symbols put closeout's statics and literals there.
lookupTAtom"closeout#file_name" ge_globalsge = SomemkPtr65584 Obj65584 ∧ lookupTAtom"closeout#ignore_EPIPE" ge_globalsge = SomemkPtr65616 Obj65616 ∧ lookupTAtom"exit_failure" ge_globalsge = SomemkPtr65776 Obj65776 ∧ lookupTAtom"closeout#str.55" ge_globalsge = Somefmt ∧ lookupTAtom"closeout#str.53" ge_globalsge = Sometext ∧ ∃p, lookupTAtom"closeout#str.52" ge_globalsge = Somep
Explore proof 6 tactics
Initial goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
eb, eo :
Z
er :
cell :
world → ptr
rep :
mem → world → Prop
Herrno :
registryTAtom"__errno_location" = Someerrno_location_contractworld cell rep
Hlinked :
Hrep :
∀m : mem w : world h : gmappiece pval, wim w h → repm w ∧ errno_cellm cellw
Hquery_reg :
Hquery_ret :
Hquery_abi :
Hquery_pre :
Hquery_post :
∀g : term k : class d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, g = TAtom"__fpending" ∧ k = L ∨ g = TAtom"ferror" ∧ k = W → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokequery_specg CResultd k ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z, vs = WIntn ∧ 0 ≤ n < 2 ^ if class_eqbk W then 32 else 64 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
fclose_spec :
contractworld
Hfclose_reg :
registryTAtom"fclose" = Somefclose_spec
Hfclose_ret :
contract_returnsfclose_spec = RClassW
Hfclose_pre :
Hfclose_post :
∀d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokefclose_spec CResultd W ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z ys : listZ, vs = WIntn ∧ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat ∧ closed_psp ++ byte_pseb eo ys.*1 = stream_psp ++ byte_pseb eo xs.*1 ∧ agreesm′ overwriteclosed_psp ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwriteclosed_psp ++ byte_pseb eo ys h
Kerrno :
Heo :
0 ≤ eo
Herange :
0 ≤ eb + eo < 2 ^ 64
Heend :
eb + eo + 4 ≤ r_ender
He48 :
r_ender ≤ 2 ^ 48
error_spec :
contractworld
Herror_reg :
registryTAtom"error" = Someerror_spec
Herror_ret :
contract_returnserror_spec = RVoid
Herror_abi :
Herror_pre :
Herror_post :
∀v fmtv txtv : value n : Z xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, lengthxs = 4%nat → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ diag_ps ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokeerror_spec CVoid ArgW Const0; ArgW v; ArgP fmtv; ArgP txtv WInt0; WIntn; WPtrfmt; WPtrtext s m w tr CallReturnvs s′ m′ w′ → ∃ys : listZ, vs = [ ] ∧ lengthys = 4%nat ∧ diag_ps ++ byte_pseb eo ys.*1 = diag_ps ++ byte_pseb eo xs.*1 ∧ agreesm′ overwritediag_ps ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritediag_ps ++ byte_pseb eo ys h
exit_spec :
contractworld
Hexit_reg :
registryTAtom"_exit" = Someexit_spec
Hexit_ret :
contract_returnsexit_spec = RVoid
Hexit_abi :
∀v : value, contract_abiexit_spec CVoid ArgW v
Hexit_pre :
∀n : Z m : mem w : world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → wim w h → contract_preexit_spec WIntn m w
Hexit_post :
∀args : listarg n : Z s : R.state m : mem w : world tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, M.E.invokeexit_spec CVoid args WIntn s m w tr CallReturnvs s′ m′ w′ → False
ob, sb :
Z
oreg, sreg, freg, ireg, xreg :
outp, errp :
Hout_live :
Herr_live :
Hob :
0 ≤ ob < 2 ^ 64
Hob8 :
ob mod 8 = 0
Hoend :
ob + 8 ≤ r_endoreg
Hsb :
0 ≤ sb < 2 ^ 64
Hsb8 :
sb mod 8 = 0
Hsend :
sb + 8 ≤ r_endsreg
Hout :
0 ≤ ptr_addroutp < 2 ^ 64
Herrp :
0 ≤ ptr_addrerrp < 2 ^ 64
Hfend :
65584 + 8 ≤ r_endfreg
Hiend :
65616 + 1 ≤ r_endireg
Hxend :
65776 + 4 ≤ r_endxreg
⊢
lookupTAtom"closeout#file_name" ge_globalsge = Someptr_addr ≔ 65584; ptr_cap ≔ Obj65584 ∧ lookupTAtom"closeout#ignore_EPIPE" ge_globalsge = Someptr_addr ≔ 65616; ptr_cap ≔ Obj65616 ∧ lookupTAtom"exit_failure" ge_globalsge = Someptr_addr ≔ 65776; ptr_cap ≔ Obj65776 ∧ lookupTAtom"closeout#str.55" ge_globalsge = Somefmt ∧ lookupTAtom"closeout#str.53" ge_globalsge = Sometext ∧ ∃p : ptr, lookupTAtom"closeout#str.52" ge_globalsge = Somep
destruct Hlinked as _ & Hg & _
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
eb, eo :
Z
er :
cell :
world → ptr
rep :
mem → world → Prop
Herrno :
registryTAtom"__errno_location" = Someerrno_location_contractworld cell rep
Hlinked :
Hrep :
∀m : mem w : world h : gmappiece pval, wim w h → repm w ∧ errno_cellm cellw
Hquery_reg :
Hquery_ret :
Hquery_abi :
Hquery_pre :
Hquery_post :
∀g : term k : class d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, g = TAtom"__fpending" ∧ k = L ∨ g = TAtom"ferror" ∧ k = W → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokequery_specg CResultd k ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z, vs = WIntn ∧ 0 ≤ n < 2 ^ if class_eqbk W then 32 else 64 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
fclose_spec :
contractworld
Hfclose_reg :
registryTAtom"fclose" = Somefclose_spec
Hfclose_ret :
contract_returnsfclose_spec = RClassW
Hfclose_pre :
Hfclose_post :
∀d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokefclose_spec CResultd W ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z ys : listZ, vs = WIntn ∧ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat ∧ closed_psp ++ byte_pseb eo ys.*1 = stream_psp ++ byte_pseb eo xs.*1 ∧ agreesm′ overwriteclosed_psp ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwriteclosed_psp ++ byte_pseb eo ys h
Kerrno :
Heo :
0 ≤ eo
Herange :
0 ≤ eb + eo < 2 ^ 64
Heend :
eb + eo + 4 ≤ r_ender
He48 :
r_ender ≤ 2 ^ 48
error_spec :
contractworld
Herror_reg :
registryTAtom"error" = Someerror_spec
Herror_ret :
contract_returnserror_spec = RVoid
Herror_abi :
Herror_pre :
Herror_post :
∀v fmtv txtv : value n : Z xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, lengthxs = 4%nat → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ diag_ps ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokeerror_spec CVoid ArgW Const0; ArgW v; ArgP fmtv; ArgP txtv WInt0; WIntn; WPtrfmt; WPtrtext s m w tr CallReturnvs s′ m′ w′ → ∃ys : listZ, vs = [ ] ∧ lengthys = 4%nat ∧ diag_ps ++ byte_pseb eo ys.*1 = diag_ps ++ byte_pseb eo xs.*1 ∧ agreesm′ overwritediag_ps ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritediag_ps ++ byte_pseb eo ys h
exit_spec :
contractworld
Hexit_reg :
registryTAtom"_exit" = Someexit_spec
Hexit_ret :
contract_returnsexit_spec = RVoid
Hexit_abi :
∀v : value, contract_abiexit_spec CVoid ArgW v
Hexit_pre :
∀n : Z m : mem w : world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → wim w h → contract_preexit_spec WIntn m w
Hexit_post :
∀args : listarg n : Z s : R.state m : mem w : world tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, M.E.invokeexit_spec CVoid args WIntn s m w tr CallReturnvs s′ m′ w′ → False
ob, sb :
Z
oreg, sreg, freg, ireg, xreg :
outp, errp :
Hout_live :
Herr_live :
Hob :
0 ≤ ob < 2 ^ 64
Hob8 :
ob mod 8 = 0
Hoend :
ob + 8 ≤ r_endoreg
Hsb :
0 ≤ sb < 2 ^ 64
Hsb8 :
sb mod 8 = 0
Hsend :
sb + 8 ≤ r_endsreg
Hout :
0 ≤ ptr_addroutp < 2 ^ 64
Herrp :
0 ≤ ptr_addrerrp < 2 ^ 64
Hfend :
65584 + 8 ≤ r_endfreg
Hiend :
65616 + 1 ≤ r_endireg
Hxend :
65776 + 4 ≤ r_endxreg
Hg :
∀n : name p : ptr, lookupn hello_globals = Somep → lookupn ge_globalsge = Somep
⊢
lookupTAtom"closeout#file_name" ge_globalsge = Someptr_addr ≔ 65584; ptr_cap ≔ Obj65584 ∧ lookupTAtom"closeout#ignore_EPIPE" ge_globalsge = Someptr_addr ≔ 65616; ptr_cap ≔ Obj65616 ∧ lookupTAtom"exit_failure" ge_globalsge = Someptr_addr ≔ 65776; ptr_cap ≔ Obj65776 ∧ lookupTAtom"closeout#str.55" ge_globalsge = Somefmt ∧ lookupTAtom"closeout#str.53" ge_globalsge = Sometext ∧ ∃p : ptr, lookupTAtom"closeout#str.52" ge_globalsge = Somep
repeat split ; try apply Hg ; vm_compute ; reflexivity
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
eb, eo :
Z
er :
cell :
world → ptr
rep :
mem → world → Prop
Herrno :
registryTAtom"__errno_location" = Someerrno_location_contractworld cell rep
Hlinked :
Hrep :
∀m : mem w : world h : gmappiece pval, wim w h → repm w ∧ errno_cellm cellw
Hquery_reg :
Hquery_ret :
Hquery_abi :
Hquery_pre :
Hquery_post :
∀g : term k : class d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, g = TAtom"__fpending" ∧ k = L ∨ g = TAtom"ferror" ∧ k = W → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokequery_specg CResultd k ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z, vs = WIntn ∧ 0 ≤ n < 2 ^ if class_eqbk W then 32 else 64 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
fclose_spec :
contractworld
Hfclose_reg :
registryTAtom"fclose" = Somefclose_spec
Hfclose_ret :
contract_returnsfclose_spec = RClassW
Hfclose_pre :
Hfclose_post :
∀d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokefclose_spec CResultd W ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z ys : listZ, vs = WIntn ∧ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat ∧ closed_psp ++ byte_pseb eo ys.*1 = stream_psp ++ byte_pseb eo xs.*1 ∧ agreesm′ overwriteclosed_psp ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwriteclosed_psp ++ byte_pseb eo ys h
Kerrno :
Heo :
0 ≤ eo
Herange :
0 ≤ eb + eo < 2 ^ 64
Heend :
eb + eo + 4 ≤ r_ender
He48 :
r_ender ≤ 2 ^ 48
error_spec :
contractworld
Herror_reg :
registryTAtom"error" = Someerror_spec
Herror_ret :
contract_returnserror_spec = RVoid
Herror_abi :
Herror_pre :
Herror_post :
∀v fmtv txtv : value n : Z xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, lengthxs = 4%nat → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ diag_ps ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokeerror_spec CVoid ArgW Const0; ArgW v; ArgP fmtv; ArgP txtv WInt0; WIntn; WPtrfmt; WPtrtext s m w tr CallReturnvs s′ m′ w′ → ∃ys : listZ, vs = [ ] ∧ lengthys = 4%nat ∧ diag_ps ++ byte_pseb eo ys.*1 = diag_ps ++ byte_pseb eo xs.*1 ∧ agreesm′ overwritediag_ps ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritediag_ps ++ byte_pseb eo ys h
exit_spec :
contractworld
Hexit_reg :
registryTAtom"_exit" = Someexit_spec
Hexit_ret :
contract_returnsexit_spec = RVoid
Hexit_abi :
∀v : value, contract_abiexit_spec CVoid ArgW v
Hexit_pre :
∀n : Z m : mem w : world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → wim w h → contract_preexit_spec WIntn m w
Hexit_post :
∀args : listarg n : Z s : R.state m : mem w : world tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, M.E.invokeexit_spec CVoid args WIntn s m w tr CallReturnvs s′ m′ w′ → False
ob, sb :
Z
oreg, sreg, freg, ireg, xreg :
outp, errp :
Hout_live :
Herr_live :
Hob :
0 ≤ ob < 2 ^ 64
Hob8 :
ob mod 8 = 0
Hoend :
ob + 8 ≤ r_endoreg
Hsb :
0 ≤ sb < 2 ^ 64
Hsb8 :
sb mod 8 = 0
Hsend :
sb + 8 ≤ r_endsreg
Hout :
0 ≤ ptr_addroutp < 2 ^ 64
Herrp :
0 ≤ ptr_addrerrp < 2 ^ 64
Hfend :
65584 + 8 ≤ r_endfreg
Hiend :
65616 + 1 ≤ r_endireg
Hxend :
65776 + 4 ≤ r_endxreg
Hg :
∀n : name p : ptr, lookupn hello_globals = Somep → lookupn ge_globalsge = Somep
⊢
∃p : ptr, lookupTAtom"closeout#str.52" ge_globalsge = Somep
exists mkPtr65648 Ro65648
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
eb, eo :
Z
er :
cell :
world → ptr
rep :
mem → world → Prop
Herrno :
registryTAtom"__errno_location" = Someerrno_location_contractworld cell rep
Hlinked :
Hrep :
∀m : mem w : world h : gmappiece pval, wim w h → repm w ∧ errno_cellm cellw
Hquery_reg :
Hquery_ret :
Hquery_abi :
Hquery_pre :
Hquery_post :
∀g : term k : class d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, g = TAtom"__fpending" ∧ k = L ∨ g = TAtom"ferror" ∧ k = W → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokequery_specg CResultd k ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z, vs = WIntn ∧ 0 ≤ n < 2 ^ if class_eqbk W then 32 else 64 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
fclose_spec :
contractworld
Hfclose_reg :
registryTAtom"fclose" = Somefclose_spec
Hfclose_ret :
contract_returnsfclose_spec = RClassW
Hfclose_pre :
Hfclose_post :
∀d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokefclose_spec CResultd W ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z ys : listZ, vs = WIntn ∧ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat ∧ closed_psp ++ byte_pseb eo ys.*1 = stream_psp ++ byte_pseb eo xs.*1 ∧ agreesm′ overwriteclosed_psp ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwriteclosed_psp ++ byte_pseb eo ys h
Kerrno :
Heo :
0 ≤ eo
Herange :
0 ≤ eb + eo < 2 ^ 64
Heend :
eb + eo + 4 ≤ r_ender
He48 :
r_ender ≤ 2 ^ 48
error_spec :
contractworld
Herror_reg :
registryTAtom"error" = Someerror_spec
Herror_ret :
contract_returnserror_spec = RVoid
Herror_abi :
Herror_pre :
Herror_post :
∀v fmtv txtv : value n : Z xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, lengthxs = 4%nat → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ diag_ps ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokeerror_spec CVoid ArgW Const0; ArgW v; ArgP fmtv; ArgP txtv WInt0; WIntn; WPtrfmt; WPtrtext s m w tr CallReturnvs s′ m′ w′ → ∃ys : listZ, vs = [ ] ∧ lengthys = 4%nat ∧ diag_ps ++ byte_pseb eo ys.*1 = diag_ps ++ byte_pseb eo xs.*1 ∧ agreesm′ overwritediag_ps ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritediag_ps ++ byte_pseb eo ys h
exit_spec :
contractworld
Hexit_reg :
registryTAtom"_exit" = Someexit_spec
Hexit_ret :
contract_returnsexit_spec = RVoid
Hexit_abi :
∀v : value, contract_abiexit_spec CVoid ArgW v
Hexit_pre :
∀n : Z m : mem w : world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → wim w h → contract_preexit_spec WIntn m w
Hexit_post :
∀args : listarg n : Z s : R.state m : mem w : world tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, M.E.invokeexit_spec CVoid args WIntn s m w tr CallReturnvs s′ m′ w′ → False
ob, sb :
Z
oreg, sreg, freg, ireg, xreg :
outp, errp :
Hout_live :
Herr_live :
Hob :
0 ≤ ob < 2 ^ 64
Hob8 :
ob mod 8 = 0
Hoend :
ob + 8 ≤ r_endoreg
Hsb :
0 ≤ sb < 2 ^ 64
Hsb8 :
sb mod 8 = 0
Hsend :
sb + 8 ≤ r_endsreg
Hout :
0 ≤ ptr_addroutp < 2 ^ 64
Herrp :
0 ≤ ptr_addrerrp < 2 ^ 64
Hfend :
65584 + 8 ≤ r_endfreg
Hiend :
65616 + 1 ≤ r_endireg
Hxend :
65776 + 4 ≤ r_endxreg
Hg :
∀n : name p : ptr, lookupn hello_globals = Somep → lookupn ge_globalsge = Somep
apply Hg
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
eb, eo :
Z
er :
cell :
world → ptr
rep :
mem → world → Prop
Herrno :
registryTAtom"__errno_location" = Someerrno_location_contractworld cell rep
Hlinked :
Hrep :
∀m : mem w : world h : gmappiece pval, wim w h → repm w ∧ errno_cellm cellw
Hquery_reg :
Hquery_ret :
Hquery_abi :
Hquery_pre :
Hquery_post :
∀g : term k : class d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, g = TAtom"__fpending" ∧ k = L ∨ g = TAtom"ferror" ∧ k = W → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokequery_specg CResultd k ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z, vs = WIntn ∧ 0 ≤ n < 2 ^ if class_eqbk W then 32 else 64 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
fclose_spec :
contractworld
Hfclose_reg :
registryTAtom"fclose" = Somefclose_spec
Hfclose_ret :
contract_returnsfclose_spec = RClassW
Hfclose_pre :
Hfclose_post :
∀d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokefclose_spec CResultd W ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z ys : listZ, vs = WIntn ∧ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat ∧ closed_psp ++ byte_pseb eo ys.*1 = stream_psp ++ byte_pseb eo xs.*1 ∧ agreesm′ overwriteclosed_psp ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwriteclosed_psp ++ byte_pseb eo ys h
Kerrno :
Heo :
0 ≤ eo
Herange :
0 ≤ eb + eo < 2 ^ 64
Heend :
eb + eo + 4 ≤ r_ender
He48 :
r_ender ≤ 2 ^ 48
error_spec :
contractworld
Herror_reg :
registryTAtom"error" = Someerror_spec
Herror_ret :
contract_returnserror_spec = RVoid
Herror_abi :
Herror_pre :
Herror_post :
∀v fmtv txtv : value n : Z xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, lengthxs = 4%nat → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ diag_ps ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokeerror_spec CVoid ArgW Const0; ArgW v; ArgP fmtv; ArgP txtv WInt0; WIntn; WPtrfmt; WPtrtext s m w tr CallReturnvs s′ m′ w′ → ∃ys : listZ, vs = [ ] ∧ lengthys = 4%nat ∧ diag_ps ++ byte_pseb eo ys.*1 = diag_ps ++ byte_pseb eo xs.*1 ∧ agreesm′ overwritediag_ps ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritediag_ps ++ byte_pseb eo ys h
exit_spec :
contractworld
Hexit_reg :
registryTAtom"_exit" = Someexit_spec
Hexit_ret :
contract_returnsexit_spec = RVoid
Hexit_abi :
∀v : value, contract_abiexit_spec CVoid ArgW v
Hexit_pre :
∀n : Z m : mem w : world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → wim w h → contract_preexit_spec WIntn m w
Hexit_post :
∀args : listarg n : Z s : R.state m : mem w : world tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, M.E.invokeexit_spec CVoid args WIntn s m w tr CallReturnvs s′ m′ w′ → False
ob, sb :
Z
oreg, sreg, freg, ireg, xreg :
outp, errp :
Hout_live :
Herr_live :
Hob :
0 ≤ ob < 2 ^ 64
Hob8 :
ob mod 8 = 0
Hoend :
ob + 8 ≤ r_endoreg
Hsb :
0 ≤ sb < 2 ^ 64
Hsb8 :
sb mod 8 = 0
Hsend :
sb + 8 ≤ r_endsreg
Hout :
0 ≤ ptr_addroutp < 2 ^ 64
Herrp :
0 ≤ ptr_addrerrp < 2 ^ 64
Hfend :
65584 + 8 ≤ r_endfreg
Hiend :
65616 + 1 ≤ r_endireg
Hxend :
65776 + 4 ≤ r_endxreg
Hg :
∀n : name p : ptr, lookupn hello_globals = Somep → lookupn ge_globalsge = Somep
vm_compute
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
eb, eo :
Z
er :
cell :
world → ptr
rep :
mem → world → Prop
Herrno :
registryTAtom"__errno_location" = Someerrno_location_contractworld cell rep
Hlinked :
Hrep :
∀m : mem w : world h : gmappiece pval, wim w h → repm w ∧ errno_cellm cellw
Hquery_reg :
Hquery_ret :
Hquery_abi :
Hquery_pre :
Hquery_post :
∀g : term k : class d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, g = TAtom"__fpending" ∧ k = L ∨ g = TAtom"ferror" ∧ k = W → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokequery_specg CResultd k ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z, vs = WIntn ∧ 0 ≤ n < 2 ^ if class_eqbk W then 32 else 64 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
fclose_spec :
contractworld
Hfclose_reg :
registryTAtom"fclose" = Somefclose_spec
Hfclose_ret :
contract_returnsfclose_spec = RClassW
Hfclose_pre :
Hfclose_post :
∀d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokefclose_spec CResultd W ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z ys : listZ, vs = WIntn ∧ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat ∧ closed_psp ++ byte_pseb eo ys.*1 = stream_psp ++ byte_pseb eo xs.*1 ∧ agreesm′ overwriteclosed_psp ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwriteclosed_psp ++ byte_pseb eo ys h
Kerrno :
Heo :
0 ≤ eo
Herange :
0 ≤ eb + eo < 2 ^ 64
Heend :
eb + eo + 4 ≤ r_ender
He48 :
r_ender ≤ 2 ^ 48
error_spec :
contractworld
Herror_reg :
registryTAtom"error" = Someerror_spec
Herror_ret :
contract_returnserror_spec = RVoid
Herror_abi :
Herror_pre :
Herror_post :
∀v fmtv txtv : value n : Z xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, lengthxs = 4%nat → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ diag_ps ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokeerror_spec CVoid ArgW Const0; ArgW v; ArgP fmtv; ArgP txtv WInt0; WIntn; WPtrfmt; WPtrtext s m w tr CallReturnvs s′ m′ w′ → ∃ys : listZ, vs = [ ] ∧ lengthys = 4%nat ∧ diag_ps ++ byte_pseb eo ys.*1 = diag_ps ++ byte_pseb eo xs.*1 ∧ agreesm′ overwritediag_ps ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritediag_ps ++ byte_pseb eo ys h
exit_spec :
contractworld
Hexit_reg :
registryTAtom"_exit" = Someexit_spec
Hexit_ret :
contract_returnsexit_spec = RVoid
Hexit_abi :
∀v : value, contract_abiexit_spec CVoid ArgW v
Hexit_pre :
∀n : Z m : mem w : world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → wim w h → contract_preexit_spec WIntn m w
Hexit_post :
∀args : listarg n : Z s : R.state m : mem w : world tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, M.E.invokeexit_spec CVoid args WIntn s m w tr CallReturnvs s′ m′ w′ → False
ob, sb :
Z
oreg, sreg, freg, ireg, xreg :
outp, errp :
Hout_live :
Herr_live :
Hob :
0 ≤ ob < 2 ^ 64
Hob8 :
ob mod 8 = 0
Hoend :
ob + 8 ≤ r_endoreg
Hsb :
0 ≤ sb < 2 ^ 64
Hsb8 :
sb mod 8 = 0
Hsend :
sb + 8 ≤ r_endsreg
Hout :
0 ≤ ptr_addroutp < 2 ^ 64
Herrp :
0 ≤ ptr_addrerrp < 2 ^ 64
Hfend :
65584 + 8 ≤ r_endfreg
Hiend :
65616 + 1 ≤ r_endireg
Hxend :
65776 + 4 ≤ r_endxreg
Hg :
∀n : name p : ptr, lookupn hello_globals = Somep → lookupn ge_globalsge = Somep
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Enter one of close_stdout's blocks.
The linked module dispatches close_stream to its proved body.
Explore proof 4 tactics
Initial goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
eb, eo :
Z
er :
cell :
world → ptr
rep :
mem → world → Prop
Herrno :
registryTAtom"__errno_location" = Someerrno_location_contractworld cell rep
Hlinked :
Hrep :
∀m : mem w : world h : gmappiece pval, wim w h → repm w ∧ errno_cellm cellw
Hquery_reg :
Hquery_ret :
Hquery_abi :
Hquery_pre :
Hquery_post :
∀g : term k : class d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, g = TAtom"__fpending" ∧ k = L ∨ g = TAtom"ferror" ∧ k = W → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokequery_specg CResultd k ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z, vs = WIntn ∧ 0 ≤ n < 2 ^ if class_eqbk W then 32 else 64 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
fclose_spec :
contractworld
Hfclose_reg :
registryTAtom"fclose" = Somefclose_spec
Hfclose_ret :
contract_returnsfclose_spec = RClassW
Hfclose_pre :
Hfclose_post :
∀d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokefclose_spec CResultd W ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z ys : listZ, vs = WIntn ∧ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat ∧ closed_psp ++ byte_pseb eo ys.*1 = stream_psp ++ byte_pseb eo xs.*1 ∧ agreesm′ overwriteclosed_psp ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwriteclosed_psp ++ byte_pseb eo ys h
Kerrno :
Heo :
0 ≤ eo
Herange :
0 ≤ eb + eo < 2 ^ 64
Heend :
eb + eo + 4 ≤ r_ender
He48 :
r_ender ≤ 2 ^ 48
error_spec :
contractworld
Herror_reg :
registryTAtom"error" = Someerror_spec
Herror_ret :
contract_returnserror_spec = RVoid
Herror_abi :
Herror_pre :
Herror_post :
∀v fmtv txtv : value n : Z xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, lengthxs = 4%nat → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ diag_ps ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokeerror_spec CVoid ArgW Const0; ArgW v; ArgP fmtv; ArgP txtv WInt0; WIntn; WPtrfmt; WPtrtext s m w tr CallReturnvs s′ m′ w′ → ∃ys : listZ, vs = [ ] ∧ lengthys = 4%nat ∧ diag_ps ++ byte_pseb eo ys.*1 = diag_ps ++ byte_pseb eo xs.*1 ∧ agreesm′ overwritediag_ps ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritediag_ps ++ byte_pseb eo ys h
exit_spec :
contractworld
Hexit_reg :
registryTAtom"_exit" = Someexit_spec
Hexit_ret :
contract_returnsexit_spec = RVoid
Hexit_abi :
∀v : value, contract_abiexit_spec CVoid ArgW v
Hexit_pre :
∀n : Z m : mem w : world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → wim w h → contract_preexit_spec WIntn m w
Hexit_post :
∀args : listarg n : Z s : R.state m : mem w : world tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, M.E.invokeexit_spec CVoid args WIntn s m w tr CallReturnvs s′ m′ w′ → False
ob, sb :
Z
oreg, sreg, freg, ireg, xreg :
outp, errp :
Hout_live :
Herr_live :
Hob :
0 ≤ ob < 2 ^ 64
Hob8 :
ob mod 8 = 0
Hoend :
ob + 8 ≤ r_endoreg
Hsb :
0 ≤ sb < 2 ^ 64
Hsb8 :
sb mod 8 = 0
Hsend :
sb + 8 ≤ r_endsreg
Hout :
0 ≤ ptr_addroutp < 2 ^ 64
Herrp :
0 ≤ ptr_addrerrp < 2 ^ 64
Hfend :
65584 + 8 ≤ r_endfreg
Hiend :
65616 + 1 ≤ r_endireg
Hxend :
65776 + 4 ≤ r_endxreg
⊢
find_fnge TAtom"close_stream" = SomeDefinedclose_stream_fn
unfold find_fn
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
eb, eo :
Z
er :
cell :
world → ptr
rep :
mem → world → Prop
Herrno :
registryTAtom"__errno_location" = Someerrno_location_contractworld cell rep
Hlinked :
Hrep :
∀m : mem w : world h : gmappiece pval, wim w h → repm w ∧ errno_cellm cellw
Hquery_reg :
Hquery_ret :
Hquery_abi :
Hquery_pre :
Hquery_post :
∀g : term k : class d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, g = TAtom"__fpending" ∧ k = L ∨ g = TAtom"ferror" ∧ k = W → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokequery_specg CResultd k ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z, vs = WIntn ∧ 0 ≤ n < 2 ^ if class_eqbk W then 32 else 64 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
fclose_spec :
contractworld
Hfclose_reg :
registryTAtom"fclose" = Somefclose_spec
Hfclose_ret :
contract_returnsfclose_spec = RClassW
Hfclose_pre :
Hfclose_post :
∀d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokefclose_spec CResultd W ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z ys : listZ, vs = WIntn ∧ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat ∧ closed_psp ++ byte_pseb eo ys.*1 = stream_psp ++ byte_pseb eo xs.*1 ∧ agreesm′ overwriteclosed_psp ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwriteclosed_psp ++ byte_pseb eo ys h
Kerrno :
Heo :
0 ≤ eo
Herange :
0 ≤ eb + eo < 2 ^ 64
Heend :
eb + eo + 4 ≤ r_ender
He48 :
r_ender ≤ 2 ^ 48
error_spec :
contractworld
Herror_reg :
registryTAtom"error" = Someerror_spec
Herror_ret :
contract_returnserror_spec = RVoid
Herror_abi :
Herror_pre :
Herror_post :
∀v fmtv txtv : value n : Z xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, lengthxs = 4%nat → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ diag_ps ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokeerror_spec CVoid ArgW Const0; ArgW v; ArgP fmtv; ArgP txtv WInt0; WIntn; WPtrfmt; WPtrtext s m w tr CallReturnvs s′ m′ w′ → ∃ys : listZ, vs = [ ] ∧ lengthys = 4%nat ∧ diag_ps ++ byte_pseb eo ys.*1 = diag_ps ++ byte_pseb eo xs.*1 ∧ agreesm′ overwritediag_ps ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritediag_ps ++ byte_pseb eo ys h
exit_spec :
contractworld
Hexit_reg :
registryTAtom"_exit" = Someexit_spec
Hexit_ret :
contract_returnsexit_spec = RVoid
Hexit_abi :
∀v : value, contract_abiexit_spec CVoid ArgW v
Hexit_pre :
∀n : Z m : mem w : world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → wim w h → contract_preexit_spec WIntn m w
Hexit_post :
∀args : listarg n : Z s : R.state m : mem w : world tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, M.E.invokeexit_spec CVoid args WIntn s m w tr CallReturnvs s′ m′ w′ → False
ob, sb :
Z
oreg, sreg, freg, ireg, xreg :
outp, errp :
Hout_live :
Herr_live :
Hob :
0 ≤ ob < 2 ^ 64
Hob8 :
ob mod 8 = 0
Hoend :
ob + 8 ≤ r_endoreg
Hsb :
0 ≤ sb < 2 ^ 64
Hsb8 :
sb mod 8 = 0
Hsend :
sb + 8 ≤ r_endsreg
Hout :
0 ≤ ptr_addroutp < 2 ^ 64
Herrp :
0 ≤ ptr_addrerrp < 2 ^ 64
Hfend :
65584 + 8 ≤ r_endfreg
Hiend :
65616 + 1 ≤ r_endireg
Hxend :
65776 + 4 ≤ r_endxreg
⊢
Somed
⇒
Somed
=
rewrite proj1Hlinked
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
eb, eo :
Z
er :
cell :
world → ptr
rep :
mem → world → Prop
Herrno :
registryTAtom"__errno_location" = Someerrno_location_contractworld cell rep
Hlinked :
Hrep :
∀m : mem w : world h : gmappiece pval, wim w h → repm w ∧ errno_cellm cellw
Hquery_reg :
Hquery_ret :
Hquery_abi :
Hquery_pre :
Hquery_post :
∀g : term k : class d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, g = TAtom"__fpending" ∧ k = L ∨ g = TAtom"ferror" ∧ k = W → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokequery_specg CResultd k ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z, vs = WIntn ∧ 0 ≤ n < 2 ^ if class_eqbk W then 32 else 64 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
fclose_spec :
contractworld
Hfclose_reg :
registryTAtom"fclose" = Somefclose_spec
Hfclose_ret :
contract_returnsfclose_spec = RClassW
Hfclose_pre :
Hfclose_post :
∀d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokefclose_spec CResultd W ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z ys : listZ, vs = WIntn ∧ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat ∧ closed_psp ++ byte_pseb eo ys.*1 = stream_psp ++ byte_pseb eo xs.*1 ∧ agreesm′ overwriteclosed_psp ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwriteclosed_psp ++ byte_pseb eo ys h
Kerrno :
Heo :
0 ≤ eo
Herange :
0 ≤ eb + eo < 2 ^ 64
Heend :
eb + eo + 4 ≤ r_ender
He48 :
r_ender ≤ 2 ^ 48
error_spec :
contractworld
Herror_reg :
registryTAtom"error" = Someerror_spec
Herror_ret :
contract_returnserror_spec = RVoid
Herror_abi :
Herror_pre :
Herror_post :
∀v fmtv txtv : value n : Z xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, lengthxs = 4%nat → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ diag_ps ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokeerror_spec CVoid ArgW Const0; ArgW v; ArgP fmtv; ArgP txtv WInt0; WIntn; WPtrfmt; WPtrtext s m w tr CallReturnvs s′ m′ w′ → ∃ys : listZ, vs = [ ] ∧ lengthys = 4%nat ∧ diag_ps ++ byte_pseb eo ys.*1 = diag_ps ++ byte_pseb eo xs.*1 ∧ agreesm′ overwritediag_ps ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritediag_ps ++ byte_pseb eo ys h
exit_spec :
contractworld
Hexit_reg :
registryTAtom"_exit" = Someexit_spec
Hexit_ret :
contract_returnsexit_spec = RVoid
Hexit_abi :
∀v : value, contract_abiexit_spec CVoid ArgW v
Hexit_pre :
∀n : Z m : mem w : world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → wim w h → contract_preexit_spec WIntn m w
Hexit_post :
∀args : listarg n : Z s : R.state m : mem w : world tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, M.E.invokeexit_spec CVoid args WIntn s m w tr CallReturnvs s′ m′ w′ → False
ob, sb :
Z
oreg, sreg, freg, ireg, xreg :
outp, errp :
Hout_live :
Herr_live :
Hob :
0 ≤ ob < 2 ^ 64
Hob8 :
ob mod 8 = 0
Hoend :
ob + 8 ≤ r_endoreg
Hsb :
0 ≤ sb < 2 ^ 64
Hsb8 :
sb mod 8 = 0
Hsend :
sb + 8 ≤ r_endsreg
Hout :
0 ≤ ptr_addroutp < 2 ^ 64
Herrp :
0 ≤ ptr_addrerrp < 2 ^ 64
Hfend :
65584 + 8 ≤ r_endfreg
Hiend :
65616 + 1 ≤ r_endireg
Hxend :
65776 + 4 ≤ r_endxreg
⊢
Somed
⇒
Somed
=
vm_compute
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
eb, eo :
Z
er :
cell :
world → ptr
rep :
mem → world → Prop
Herrno :
registryTAtom"__errno_location" = Someerrno_location_contractworld cell rep
Hlinked :
Hrep :
∀m : mem w : world h : gmappiece pval, wim w h → repm w ∧ errno_cellm cellw
Hquery_reg :
Hquery_ret :
Hquery_abi :
Hquery_pre :
Hquery_post :
∀g : term k : class d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, g = TAtom"__fpending" ∧ k = L ∨ g = TAtom"ferror" ∧ k = W → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokequery_specg CResultd k ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z, vs = WIntn ∧ 0 ≤ n < 2 ^ if class_eqbk W then 32 else 64 ∧ agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ h
fclose_spec :
contractworld
Hfclose_reg :
registryTAtom"fclose" = Somefclose_spec
Hfclose_ret :
contract_returnsfclose_spec = RClassW
Hfclose_pre :
Hfclose_post :
∀d : name v : value p : ptr xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ stream_psp ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokefclose_spec CResultd W ArgP v WPtrp s m w tr CallReturnvs s′ m′ w′ → ∃n : Z ys : listZ, vs = WIntn ∧ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat ∧ closed_psp ++ byte_pseb eo ys.*1 = stream_psp ++ byte_pseb eo xs.*1 ∧ agreesm′ overwriteclosed_psp ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwriteclosed_psp ++ byte_pseb eo ys h
Kerrno :
Heo :
0 ≤ eo
Herange :
0 ≤ eb + eo < 2 ^ 64
Heend :
eb + eo + 4 ≤ r_ender
He48 :
r_ender ≤ 2 ^ 48
error_spec :
contractworld
Herror_reg :
registryTAtom"error" = Someerror_spec
Herror_ret :
contract_returnserror_spec = RVoid
Herror_abi :
Herror_pre :
Herror_post :
∀v fmtv txtv : value n : Z xs : listZ s : R.state m : mem w : world h : gmappiece pval tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, lengthxs = 4%nat → agreesm h → live_disjointm → R.readys m → wim w h → ∀l : piece v0 : pval, l, v0 ∈ diag_ps ++ byte_pseb eo xs → h !! l = Somev0 → M.E.invokeerror_spec CVoid ArgW Const0; ArgW v; ArgP fmtv; ArgP txtv WInt0; WIntn; WPtrfmt; WPtrtext s m w tr CallReturnvs s′ m′ w′ → ∃ys : listZ, vs = [ ] ∧ lengthys = 4%nat ∧ diag_ps ++ byte_pseb eo ys.*1 = diag_ps ++ byte_pseb eo xs.*1 ∧ agreesm′ overwritediag_ps ++ byte_pseb eo ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ wim′ w′ overwritediag_ps ++ byte_pseb eo ys h
exit_spec :
contractworld
Hexit_reg :
registryTAtom"_exit" = Someexit_spec
Hexit_ret :
contract_returnsexit_spec = RVoid
Hexit_abi :
∀v : value, contract_abiexit_spec CVoid ArgW v
Hexit_pre :
∀n : Z m : mem w : world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → wim w h → contract_preexit_spec WIntn m w
Hexit_post :
∀args : listarg n : Z s : R.state m : mem w : world tr : listevent vs : listword s′ : R.state m′ : mem w′ : world, M.E.invokeexit_spec CVoid args WIntn s m w tr CallReturnvs s′ m′ w′ → False
ob, sb :
Z
oreg, sreg, freg, ireg, xreg :
outp, errp :
Hout_live :
Herr_live :
Hob :
0 ≤ ob < 2 ^ 64
Hob8 :
ob mod 8 = 0
Hoend :
ob + 8 ≤ r_endoreg
Hsb :
0 ≤ sb < 2 ^ 64
Hsb8 :
sb mod 8 = 0
Hsend :
sb + 8 ≤ r_endsreg
Hout :
0 ≤ ptr_addroutp < 2 ^ 64
Herrp :
0 ≤ ptr_addrerrp < 2 ^ 64
Hfend :
65584 + 8 ≤ r_endfreg
Hiend :
65616 + 1 ≤ r_endireg
Hxend :
65776 + 4 ≤ r_endxreg
⊢
SomeDefinedfn_name ≔ TAtom"close_stream"; fn_linkage ≔ TAtom"export"; fn_ret ≔ RClassW; fn_params ≔ P, TAtom"v0"; fn_blocks ≔ b_label ≔ TAtom"start"; b_phis ≔ [ ]; b_insts ≔ CallCResultTAtom"v4" L GlobalTAtom"__fpending" ArgP TmpTAtom"v0"; LetTAtom"v5" W CmpNe L TmpTAtom"v4"; Const0; CallCResultTAtom"v9" W GlobalTAtom"ferror" ArgP TmpTAtom"v0"; LetTAtom"v10" W CmpNe W TmpTAtom"v9"; Const0; CallCResultTAtom"v14" W GlobalTAtom"fclose" ArgP TmpTAtom"v0"; LetTAtom"v15" W CmpNe W TmpTAtom"v14"; Const0; b_jump ≔ JBranchTmpTAtom"v10" ToTAtom"L22" ToTAtom"L21"; b_label ≔ TAtom"L21"; b_phis ≔ [ ]; b_insts ≔ [ ]; b_jump ≔ JBranchTmpTAtom"v15" ToTAtom"L24" ToTAtom"L22"; b_label ≔ TAtom"L24"; b_phis ≔ [ ]; b_insts ≔ [ ]; b_jump ≔ JBranchTmpTAtom"v5" ToTAtom"L22" ToTAtom"L27"; b_label ≔ TAtom"L27"; b_phis ≔ [ ]; b_insts ≔ CallCResultTAtom"v29" P GlobalTAtom"__errno_location" [ ]; LetTAtom"chk0" A Check0 4 Read 1 TmpTAtom"v29"; LetTAtom"v30" W RawLoadLdNarrowSw 0 TmpTAtom"chk0"; LetTAtom"v31" W CmpNe W TmpTAtom"v30"; Const9; b_jump ≔ JGotoToTAtom"L22"; b_label ≔ TAtom"L22"; b_phis ≔ PhiTAtom"v37" W TAtom"start", Const1; TAtom"L21", Const0; TAtom"L24", Const1; TAtom"L27", TmpTAtom"v31"; b_insts ≔ [ ]; b_jump ≔ JBranchTmpTAtom"v37" ToTAtom"L17" ToTAtom"L19"; b_label ≔ TAtom"L17"; b_phis ≔ [ ]; b_insts ≔ LetTAtom"v42" W CmpEq W TmpTAtom"v14"; Const0; b_jump ≔ JBranchTmpTAtom"v42" ToTAtom"L38" ToTAtom"L40"; b_label ≔ TAtom"L38"; b_phis ≔ [ ]; b_insts ≔ CallCResultTAtom"v43" P GlobalTAtom"__errno_location" [ ]; LetTAtom"chk1" A Check0 4 Write 1 TmpTAtom"v43"; RawStoreWw 0 Const0 TmpTAtom"chk1"; b_jump ≔ JGotoToTAtom"L40"; b_label ≔ TAtom"L40"; b_phis ≔ [ ]; b_insts ≔ [ ]; b_jump ≔ JRetConst4294967295; b_label ≔ TAtom"L19"; b_phis ≔ [ ]; b_insts ≔ [ ]; b_jump ≔ JRetConst0 = SomeDefinedfn_name ≔ TAtom"close_stream"; fn_linkage ≔ TAtom"export"; fn_ret ≔ RClassW; fn_params ≔ P, TAtom"v0"; fn_blocks ≔ b_label ≔ TAtom"start"; b_phis ≔ [ ]; b_insts ≔ CallCResultTAtom"v4" L GlobalTAtom"__fpending" ArgP TmpTAtom"v0"; LetTAtom"v5" W CmpNe L TmpTAtom"v4"; Const0; CallCResultTAtom"v9" W GlobalTAtom"ferror" ArgP TmpTAtom"v0"; LetTAtom"v10" W CmpNe W TmpTAtom"v9"; Const0; CallCResultTAtom"v14" W GlobalTAtom"fclose" ArgP TmpTAtom"v0"; LetTAtom"v15" W CmpNe W TmpTAtom"v14"; Const0; b_jump ≔ JBranchTmpTAtom"v10" ToTAtom"L22" ToTAtom"L21"; b_label ≔ TAtom"L21"; b_phis ≔ [ ]; b_insts ≔ [ ]; b_jump ≔ JBranchTmpTAtom"v15" ToTAtom"L24" ToTAtom"L22"; b_label ≔ TAtom"L24"; b_phis ≔ [ ]; b_insts ≔ [ ]; b_jump ≔ JBranchTmpTAtom"v5" ToTAtom"L22" ToTAtom"L27"; b_label ≔ TAtom"L27"; b_phis ≔ [ ]; b_insts ≔ CallCResultTAtom"v29" P GlobalTAtom"__errno_location" [ ]; LetTAtom"chk0" A Check0 4 Read 1 TmpTAtom"v29"; LetTAtom"v30" W RawLoadLdNarrowSw 0 TmpTAtom"chk0"; LetTAtom"v31" W CmpNe W TmpTAtom"v30"; Const9; b_jump ≔ JGotoToTAtom"L22"; b_label ≔ TAtom"L22"; b_phis ≔ PhiTAtom"v37" W TAtom"start", Const1; TAtom"L21", Const0; TAtom"L24", Const1; TAtom"L27", TmpTAtom"v31"; b_insts ≔ [ ]; b_jump ≔ JBranchTmpTAtom"v37" ToTAtom"L17" ToTAtom"L19"; b_label ≔ TAtom"L17"; b_phis ≔ [ ]; b_insts ≔ LetTAtom"v42" W CmpEq W TmpTAtom"v14"; Const0; b_jump ≔ JBranchTmpTAtom"v42" ToTAtom"L38" ToTAtom"L40"; b_label ≔ TAtom"L38"; b_phis ≔ [ ]; b_insts ≔ CallCResultTAtom"v43" P GlobalTAtom"__errno_location" [ ]; LetTAtom"chk1" A Check0 4 Write 1 TmpTAtom"v43"; RawStoreWw 0 Const0 TmpTAtom"chk1"; b_jump ≔ JGotoToTAtom"L40"; b_label ≔ TAtom"L40"; b_phis ≔ [ ]; b_insts ≔ [ ]; b_jump ≔ JRetConst4294967295; b_label ≔ TAtom"L19"; b_phis ≔ [ ]; b_insts ≔ [ ]; b_jump ≔ JRetConst0
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A null file name takes the unnamed-file diagnostic, then _exit. quotearg_colon is not called and needs no premise triple.
Proof 62 steps Qed
intros Hxs Hfs
iIntros Hfl Hfb Hfa Hxl Hxb Hl Hx Hd
destruct close_lookups as Hfile & Hignore & Hfailure & Hfmt & Htext & p & Hdomain
{iApply close_file_name
iFrame
co_enter "L0"
iApply wp_check with Hfl
–reflexivity
–reflexivity
–change 65584 ≤ 65584
lia
–reflexivity
–iNext
iIntros Hfl
iApply wp_raw_load_pointer_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ freg with Hfl Hfc [] ; reflexivity | word_premise | reflexivity | addr_premise | reflexivity | cbn ; lia | done |
iNext
iIntros Hfl Hfc _
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
co_enter "L61"
iApply wp_close_errno
iNext
iApply wp_check with Hl ; reflexivity | word_premise | reflexivity | unfold ep ; addr_premise | unfold ep ; addr_premise | unfold ep ; addr_premise |
iNext
iIntros Hl
iApply wp_close_load_w with Hl Hx ; word_premise | exact Herange | exact Hxs |
iNext
iIntros Hl Hx
pose proof close_w_rangexs as Hwr
iApply wp_close_error with Hd Hx ; word_premise | unfold fmt ; word_premise | unfold text ; word_premise | apply close_w_range | exact Hxs |
iNext
iIntros ys Hys Hd Hx
iApply wp_goto
iNext
co_enter "L26"
iApply wp_check with Hxl ; reflexivity | word_premise | reflexivity | addr_premise | addr_premise | addr_premise |
iNext
iIntros Hxl
iApply wp_close_load_w with Hxl Hxb ; word_premise | cbn ; lia | exact Hfs |
iNext
iIntros Hxl Hxb
pose proof close_w_rangefs as Hfr
iApply wp_close_exit ; word_premise | apply close_w_range
Close stderr after stdout was settled. Its failure exits directly; a successful return preserves all module cells and errno ownership.
∀ e xs fs Φ
lengthxs = 4%nat
lengthfs = 4%nat
Proof 49 steps Qed
intros Hxs Hfs
iIntros Hs Hcells Hl Hx Hd HΦ
iDestruct Hcells as (Hol & Hoc & Hsl & Hsc & Hfl & Hfb & Hfa & Hil & Hib & Hxl & Hxb)
destruct close_lookups as _ & _ & Hfailure & _
co_enter "L91"
assert Esb : raw_addresssb 0 = sb by unfold raw_address ; rewrite Z.add_0_r ; apply Z.mod_small ; exact Hsb
iApply wp_check with Hsl ; reflexivity | word_premise | reflexivity | change sb ≤ raw_addresssb 0 ; rewrite Esb ; lia | change raw_addresssb 0 + 8 ≤ r_endsreg ; rewrite Esb ; exact Hsend | change raw_addresssb 0 mod 8 = 0 ; rewrite Esb ; exact Hsb8 |
iNext
iIntros Hsl
iApply wp_close_stream_pointer with Hsl Hsc Hs ; exact Herr_live | word_premise | exact Hsb | exact Hsb8 | exact Herrp |
iNext
iIntros Hsl Hsc Hs
iApply wp_call_bind_ _ _ _ _ _ _ _ _ _ _ _ _ close_stream_fn invocationclose_stream_fn WPtrerrp ; word_premise | exact close_stream_linked | reflexivity |
iNext
iApply close_stream_spec with Hs Hl Hx ; exact Hxs |
iNext
iIntros r ys Hr Hys Hl Hx
iExists _
iSplit ; iPureIntro ; reflexivity |
iNext
destruct Hr as → | →
–iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
co_enter "L89"
iApply wp_ret_void
iNext
iApply HΦ $! ys with [%] [Hol Hoc Hsl Hsc Hfl Hfb Hfa Hil Hib Hxl Hxb] Hl Hx Hd ; exact Hys | rewrite / close_cells ; iFrame
–iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
co_enter "L87"
iApply wp_check with Hxl ; reflexivity | word_premise | reflexivity | addr_premise | addr_premise | addr_premise |
iNext
iIntros Hxl
iApply wp_close_load_w with Hxl Hxb ; word_premise | cbn ; lia | exact Hfs |
iNext
iIntros Hxl Hxb
pose proof close_w_rangefs as Hfr
iApply wp_close_exit ; word_premise | apply close_w_range
The exit callback closes stdout then stderr. It returns all module statics and pointer cells on normal return; errors either report the unnamed write failure and exit or, for stderr, exit directly.
Proof 61 steps Qed
intros Hxs Hfs
iIntros Hout Herr Hcells Hl Hx Hd HΦ
iDestruct Hcells as (Hol & Hoc & Hsl & Hsc & Hfl & Hfb & Hfa & Hil & Hib & Hxl & Hxb)
destruct close_lookups as _ & Hignore & _
change invocationclose_stdout_fn [ ] with mkFrameclose_stdout_fn [ ] [ ] None EnterTAtom"start" None
co_enter "start"
assert Eob : raw_addressob 0 = ob by unfold raw_address ; rewrite Z.add_0_r ; apply Z.mod_small ; exact Hob
iApply wp_check with Hol ; reflexivity | word_premise | reflexivity | change ob ≤ raw_addressob 0 ; rewrite Eob ; lia | change raw_addressob 0 + 8 ≤ r_endoreg ; rewrite Eob ; exact Hoend | change raw_addressob 0 mod 8 = 0 ; rewrite Eob ; exact Hob8 |
iNext
iIntros Hol
iApply wp_close_stream_pointer with Hol Hoc Hout ; exact Hout_live | word_premise | exact Hob | exact Hob8 | exact Hout |
iNext
iIntros Hol Hoc Hout
iApply wp_call_bind_ _ _ _ _ _ _ _ _ _ _ _ _ close_stream_fn invocationclose_stream_fn WPtroutp ; word_premise | exact close_stream_linked | reflexivity |
iNext
iApply close_stream_spec with Hout Hl Hx ; exact Hxs |
iNext
iIntros r ys Hr Hys Hl Hx
iExists _
iSplit ; iPureIntro ; reflexivity |
iNext
destruct Hr as → | →
–iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
co_enter "L8"
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
iApply close_stdout_L91 with Herr [Hol Hoc Hsl Hsc Hfl Hfb Hfa Hil Hib Hxl Hxb] Hl Hx Hd HΦ ; exact Hys | exact Hfs | rewrite / close_cells ; iFrame
–iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
co_enter "L7"
iApply wp_check with Hil ; reflexivity | word_premise | reflexivity | addr_premise | addr_premise | addr_premise |
iNext
iIntros Hil
iApply wp_raw_load_byte with Hil Hib ; reflexivity | word_premise | reflexivity | reflexivity | left ; reflexivity | addr_premise |
iNext
iIntros Hil Hib
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
co_enter "L12"
iApply wp_goto
iNext
co_enter "L8"
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
iApply close_stdout_error with Hfl Hfb Hfa Hxl Hxb Hl Hx Hd ; exact Hys | exact Hfs
HelloCloseOn over a Logic instance of its own.