rocq/theories/HelloStdio.v
Admission of Hello's actual version/footer literals. The bytes and object bounds come from the linked fixture, but current memory is read from program-owned pieces, not assumed to equal startup memory.
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 String ZArith List Lia
From Nanofil Require Import Term Syntax Values Memory Runtime Semantics Run ExternalCalls ExternalMachine Stdio Shutdown Streams Formatting Libc LibcStreams LibcExit Pieces Heap ContractFrame Logic StringLogic LentLogic LibcStreamLogic LibcErrnoLogic LibcStreamTokens LibcStreamAdapter HelloModule HelloLeaf HelloVersion HelloClose
Import ListNotations
Open Scope Z_scope
Open Scope list_scope
mapλi ⇒ m_byteshello_literal_memory ptr_addrversion_literals + Z.of_nati seq0 Z.to_natstring_lengthhello_literal_memory version_literals
Somereg
⇒
reg
Includes the author life tokens used by the variadic wrapper.
"version-etc#str.41"; "version_etc_copyright"; "version-etc#str.43"; "version-etc#str.44"; "version-etc#str.45"; "version-etc#str.46"; "version-etc#str.47"; "version-etc#str.51"; "version-etc#str.58"; "version-etc#str.59"; "version-etc#str.60"; "version-etc#str.61"; "version-etc#str.62"; "version-etc#str.63"; "version-etc#str.64"; "hello#str.70"; "hello#str.63"; "hello#str.71"; "hello#str.72"; "hello#str.73"; "hello#str.74"; "hello#str.75"
Compute the closed fixture strings once, then rewrite by a checked equality instead of repeatedly reducing the linked initializer.
List.Forallλsb ⇒ hello_literal_bytesfstsb = sndsb hello_literal_cache
Explore proof 2 tactics
Initial goal
⊢
Forallλsb : string × listZ ⇒ hello_literal_bytessb.1 = sb.2 hello_literal_cache
repeat apply List.Forall_cons ; vm_compute ; reflexivity |
⊢
Forallλsb : string × listZ ⇒ hello_literal_bytessb.1 = sb.2 [ ]
constructor
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
repeat apply List.Forall_cons ; vm_compute ; reflexivity |
constructor
Explore proof 4 tactics
Initial goal
⊢
∀s : string bytes : listZ, Ins, bytes hello_literal_cache → hello_literal_bytess = bytes
intros s bytes Hin
⊢
hello_literal_bytess = bytes
pose proof hello_literal_cache_valid as Hcache
s :
bytes :
listZ
Hin :
Ins, bytes hello_literal_cache
Hcache :
Forallλsb : string × listZ ⇒ hello_literal_bytessb.1 = sb.2 hello_literal_cache
⊢
hello_literal_bytess = bytes
rewrite List.Forall_forall in Hcache
s :
bytes :
listZ
Hin :
Ins, bytes hello_literal_cache
Hcache :
∀x : string × listZ, Inx hello_literal_cache → hello_literal_bytesx.1 = x.2
⊢
hello_literal_bytess = bytes
exact Hcaches, bytes Hin
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros s bytes Hin
pose proof hello_literal_cache_valid as Hcache
rewrite List.Forall_forall in Hcache
exact Hcaches, bytes Hin
erewrite hello_literal_cached ; | vm_compute ; eauto 30
Explore proof 2 tactics
Initial goal
intros s Hin
repeat destruct Hin as [ <-| Hin ] ; try contradiction ; vm_compute ; repeat split ; try right ; reflexivity ; repeat constructor ; congruence
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros s Hin
repeat destruct Hin as [ <-| Hin ] ; try contradiction ; vm_compute ; repeat split ; try right ; reflexivity ; repeat constructor ; congruence
This is the exact lookup/agreement interface used by HelloVersion; no condition on the current world or output result supplies bytes.
∀ s m h
Explore proof 14 tactics
Initial goal
⊢
∀s : string m : mem h : gmappiece pval, Ins hello_output_literals → ∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev → agreesm h → c_stringm version_literals hello_literal_bytess
intros s m h Hin Howned Ha
apply string_c_string with b := ptr_addrversion_literals reg := hello_literal_regions
2 openfocused goal
–apply hello_literal_shape
2 opendeferred goal
exact Hin
deferred goal
–apply all_agree_intro
⊢
∀l : piece v : pval, l, v ∈ string_psversion_literals ptr_addrversion_literals hello_literal_regions hello_literal_bytess → agree_piecem l v
intros l v Hlv
s :
m :
Hin :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
l :
v :
⊢
agree_piecem l v
apply Ha , Howned
s :
m :
Hin :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
l :
v :
⊢
l, v ∈ hello_output_pieces
apply list_elem_of_In
s :
m :
Hin :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
l :
v :
⊢
Inl, v hello_output_pieces
unfold hello_output_pieces
s :
m :
Hin :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
l :
v :
⊢
Inl, v flat_maphello_literal_pieces hello_output_literals
apply in_flat_map
s :
m :
Hin :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
l :
v :
⊢
∃x : string, Inx hello_output_literals ∧ Inl, v hello_literal_piecesx
exists s
s :
m :
Hin :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
l :
v :
⊢
Ins hello_output_literals ∧ Inl, v hello_literal_piecess
split ; exact Hin |
s :
m :
Hin :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
l :
v :
⊢
Inl, v hello_literal_piecess
apply list_elem_of_In
s :
m :
Hin :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
l :
v :
⊢
l, v ∈ hello_literal_piecess
exact Hlv
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros s m h Hin Howned Ha
apply string_c_string with b := ptr_addrversion_literals reg := hello_literal_regions
–apply hello_literal_shape
exact Hin
–apply all_agree_intro
intros l v Hlv
apply Ha , Howned
apply list_elem_of_In
unfold hello_output_pieces
apply in_flat_map
exists s
split ; exact Hin |
apply list_elem_of_In
exact Hlv
The default branch is used only for printf sites; registry facts below are restricted to actual footer/version call lists.
output_contracthello_output_apig libc_stream_modelrep requests wide libc_stdout
Hard aliases and the six stream entries compose without replacing the remaining libc contracts supplied by the caller.
libc_hard_exit_registryrep host libc_stream_registryrep requests wide fallback
Tactics mirror the selected format constructors, not a second executable parser. Every %s must prove its owned C string.
first apply format_end | eapply format_string ; apply Hstring ; simpl ; tauto | hello_format Hstring | eapply format_signed with text := 50; 48; 50; 54 ; vm_compute ; repeat split ; repeat constructor ; congruence | hello_format Hstring | apply format_percent ; hello_format Hstring | apply format_literal ; lia | discriminate | hello_format Hstring
∀ stream g xs m h
∃bytes, output_texthello_output_apig m xs bytes
Explore proof 4 tactics
Initial goal
⊢
∀stream : ptr g : name xs : listword m : mem h : gmappiece pval, Ing, xs version_output_argsstream → ∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev → agreesm h → ∃bytes : listZ, output_texthello_output_apig m xs bytes
intros stream g xs m h Hin Howned Ha
stream :
g :
xs :
listword
m :
Hin :
Ing, xs version_output_argsstream
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
⊢
∃bytes : listZ, output_texthello_output_apig m xs bytes
assert Hstring := λs Hin ⇒ hello_owned_literals m h Hin Howned Ha
stream :
g :
xs :
listword
m :
Hin :
Ing, xs version_output_argsstream
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hstring :
∀s : string, Ins hello_output_literals → c_stringm version_literals hello_literal_bytess
⊢
∃bytes : listZ, output_texthello_output_apig m xs bytes
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ←
6 openstream :
m :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hstring :
∀s : string, Ins hello_output_literals → c_stringm version_literals hello_literal_bytess
⊢
∃bytes : listZ, output_texthello_output_apiTAtom"fprintf" m WPtrstream; WPtrversion_literal"version-etc#str.41"; WPtrversion_literal"hello#str.70"; WPtrversion_literal"hello#str.63"; WPtrversion_literal"hello#str.71" bytes
focused goal
stream :
m :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hstring :
∀s : string, Ins hello_output_literals → c_stringm version_literals hello_literal_bytess
⊢
∃bytes : listZ, output_texthello_output_apiTAtom"fprintf" m WPtrstream; WPtrversion_literal"version_etc_copyright"; WPtrversion_literal"version-etc#str.44"; WInt2026 bytes
focused goal
stream :
m :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hstring :
∀s : string, Ins hello_output_literals → c_stringm version_literals hello_literal_bytess
⊢
∃bytes : listZ, output_texthello_output_apiTAtom"fputs" m WPtrversion_literal"version-etc#str.45"; WPtrstream bytes
focused goal
stream :
m :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hstring :
∀s : string, Ins hello_output_literals → c_stringm version_literals hello_literal_bytess
⊢
∃bytes : listZ, output_texthello_output_apiTAtom"fprintf" m WPtrstream; WPtrversion_literal"version-etc#str.46"; WPtrversion_literal"version-etc#str.47" bytes
focused goal
stream :
m :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hstring :
∀s : string, Ins hello_output_literals → c_stringm version_literals hello_literal_bytess
⊢
∃bytes : listZ, output_texthello_output_apiTAtom"fputs" m WPtrversion_literal"version-etc#str.45"; WPtrstream bytes
focused goal
stream :
m :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hstring :
∀s : string, Ins hello_output_literals → c_stringm version_literals hello_literal_bytess
⊢
∃bytes : listZ, output_texthello_output_apiTAtom"fprintf" m WPtrstream; WPtrversion_literal"version-etc#str.51"; WPtrversion_literal"hello#str.72"; WPtrversion_literal"hello#str.73"; WPtrversion_literal"hello#str.74"; WPtrversion_literal"hello#str.75" bytes
all: (match goal with|- ∃bytes, output_text bytes⇒let actual ≔ eval vm_compute in api in change ∃bytes, output_textactual m xs bytesend;eexists;unfold output_text;eexists;eexists;eexists;split;;split;;cbv beta iota zeta;try reflexivity;hello_cached_format;hello_format Hstring)
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros stream g xs m h Hin Howned Ha
assert Hstring := λs Hin ⇒ hello_owned_literals m h Hin Howned Ha
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ←
all: (match goal with|- ∃bytes, output_text bytes⇒let actual ≔ eval vm_compute in api in change ∃bytes, output_textactual m xs bytesend;eexists;unfold output_text;eexists;eexists;eexists;split;;split;;cbv beta iota zeta;try reflexivity;hello_cached_format;hello_format Hstring)
Explore proof 4 tactics
Initial goal
⊢
∀stream : ptr g : name xs : listword m : mem h : gmappiece pval, Ing, xs emit_output_argsstream → ∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev → agreesm h → ∃bytes : listZ, output_texthello_output_apig m xs bytes
intros stream g xs m h Hin Howned Ha
stream :
g :
xs :
listword
m :
Hin :
Ing, xs emit_output_argsstream
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
⊢
∃bytes : listZ, output_texthello_output_apig m xs bytes
assert Hstring := λs Hin ⇒ hello_owned_literals m h Hin Howned Ha
stream :
g :
xs :
listword
m :
Hin :
Ing, xs emit_output_argsstream
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hstring :
∀s : string, Ins hello_output_literals → c_stringm version_literals hello_literal_bytess
⊢
∃bytes : listZ, output_texthello_output_apig m xs bytes
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ←
4 openstream :
m :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hstring :
∀s : string, Ins hello_output_literals → c_stringm version_literals hello_literal_bytess
⊢
∃bytes : listZ, output_texthello_output_apiTAtom"fputs" m WPtrversion_literal"version-etc#str.45"; WPtrstream bytes
focused goal
stream :
m :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hstring :
∀s : string, Ins hello_output_literals → c_stringm version_literals hello_literal_bytess
⊢
∃bytes : listZ, output_texthello_output_apiTAtom"printf" m WPtrversion_literal"version-etc#str.58"; WPtrversion_literal"version-etc#str.59" bytes
focused goal
stream :
m :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hstring :
∀s : string, Ins hello_output_literals → c_stringm version_literals hello_literal_bytess
⊢
∃bytes : listZ, output_texthello_output_apiTAtom"printf" m WPtrversion_literal"version-etc#str.60"; WPtrversion_literal"version-etc#str.61"; WPtrversion_literal"version-etc#str.62" bytes
focused goal
stream :
m :
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hstring :
∀s : string, Ins hello_output_literals → c_stringm version_literals hello_literal_bytess
⊢
∃bytes : listZ, output_texthello_output_apiTAtom"printf" m WPtrversion_literal"version-etc#str.63"; WPtrversion_literal"version-etc#str.64" bytes
all: (match goal with|- ∃bytes, output_text bytes⇒let actual ≔ eval vm_compute in api in change ∃bytes, output_textactual m xs bytesend;eexists;unfold output_text;eexists;eexists;eexists;split;;split;;cbv beta iota zeta;try reflexivity;hello_cached_format;hello_format Hstring)
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros stream g xs m h Hin Howned Ha
assert Hstring := λs Hin ⇒ hello_owned_literals m h Hin Howned Ha
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ←
all: (match goal with|- ∃bytes, output_text bytes⇒let actual ≔ eval vm_compute in api in change ∃bytes, output_textactual m xs bytesend;eexists;unfold output_text;eexists;eexists;eexists;split;;split;;cbv beta iota zeta;try reflexivity;hello_cached_format;hello_format Hstring)
Class-only admission of the selected promoted ABI, independent of argument expressions and their evaluated values.
Explore proof 4 tactics
Initial goal
intros args H
induction args as | k v args IH ; constructor |
inversion H as [ |? ? Hk Hrest ] ; subst
⊢
Forallpromoted_argument Argk v :: args
constructor ; exists v ; destruct Hk ; subst ; auto | auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros args H
induction args as | k v args IH ; constructor |
inversion H as [ |? ? Hk Hrest ] ; subst
constructor ; exists v ; destruct Hk ; subst ; auto | auto
Explore proof 23 tactics
Initial goal
⊢
intros api d args H
⊢
output_abiapi CResultd W args
split ; right ; exists d ; reflexivity |
⊢
match api with
⇒
destruct api
3 opend :
args :
listarg
⊢
∃fmt : value rest : listarg, args = ArgP fmt :: rest ∧ Forallpromoted_argument rest
focused goal
–destruct H as rest & Hargs & Hrest
3 open⊢
∃fmt : value rest0 : listarg, args = ArgP fmt :: rest0 ∧ Forallpromoted_argument rest0
deferred goal
destruct args as | k fmt args ; discriminate |
3 opendeferred goal
injection Hargs as → Hargs
3 opendeferred goal
exists fmt, args
3 open⊢
ArgP fmt :: args = ArgP fmt :: args ∧ Forallpromoted_argument args
deferred goal
split ; reflexivity |
3 open⊢
Forallpromoted_argument args
deferred goal
apply promoted_classes
3 opendeferred goal
rewrite Hargs
3 opendeferred goal
exact Hrest
2 opendeferred goal
–destruct H as rest & Hargs & Hrest
2 opendestruct args as | k file | k′ fmt args ; try discriminate
2 openinjection Hargs as → → Hargs
2 openexists file, fmt, args
2 opensplit ; reflexivity |
2 open⊢
Forallpromoted_argument args
apply promoted_classes
2 openrewrite Hargs
2 openexact Hrest
–destruct args as | k text | k′ file | extra args ; try discriminate
injection H as → →
exists text, file
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros api d args H
split ; right ; exists d ; reflexivity |
destruct api
–destruct H as rest & Hargs & Hrest
destruct args as | k fmt args ; discriminate |
injection Hargs as → Hargs
exists fmt, args
split ; reflexivity |
apply promoted_classes
rewrite Hargs
exact Hrest
–destruct H as rest & Hargs & Hrest
destruct args as | k file | k′ fmt args ; try discriminate
injection Hargs as → → Hargs
exists file, fmt, args
split ; reflexivity |
apply promoted_classes
rewrite Hargs
exact Hrest
–destruct args as | k text | k′ file | extra args ; try discriminate
injection H as → →
exists text, file
reflexivity
∀ rep requests wide fallback stream g xs
Ing, xs version_output_argsstream
libc_stream_registryrep requests wide fallback g = Somehello_output_specrep requests wide g
Explore proof 2 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop fallback : name → optioncontractlibc_world stream : ptr g : name xs : listword, Ing, xs version_output_argsstream → libc_stream_registryrep requests wide fallback g = Somehello_output_specrep requests wide g
intros rep requests wide fallback stream g xs Hin
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
fallback :
name → optioncontractlibc_world
stream :
g :
xs :
listword
Hin :
Ing, xs version_output_argsstream
⊢
libc_stream_registryrep requests wide fallback g = Somehello_output_specrep requests wide g
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide fallback stream g xs Hin
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; reflexivity
Explore proof 2 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop fallback : name → optioncontractlibc_world stream : ptr g : name xs : listword, Ing, xs emit_output_argsstream → libc_stream_registryrep requests wide fallback g = Somehello_output_specrep requests wide g
intros rep requests wide fallback stream g xs Hin
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
fallback :
name → optioncontractlibc_world
stream :
g :
xs :
listword
Hin :
Ing, xs emit_output_argsstream
⊢
libc_stream_registryrep requests wide fallback g = Somehello_output_specrep requests wide g
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide fallback stream g xs Hin
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; reflexivity
∀ rep requests wide g
contract_returnshello_output_specrep requests wide g = RClassW
Explore proof 1 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop g : name, contract_returnshello_output_specrep requests wide g = RClassW
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
reflexivity
Explore proof 4 tactics
Initial goal
⊢
intros stream g xs d args Hin Hclasses
⊢
output_abihello_output_apig CResultd W args
apply output_abi_classes
⊢
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; cbn [ hello_output_api name_eqb ] ; try exact Hclasses
4 openstream :
d :
args :
listarg
Hclasses :
=
version_output_classesWPtrstream; WPtrversion_literal"version-etc#str.41"; WPtrversion_literal"hello#str.70"; WPtrversion_literal"hello#str.63"; WPtrversion_literal"hello#str.71"
⊢
focused goal
stream :
d :
args :
listarg
Hclasses :
=
version_output_classesWPtrstream; WPtrversion_literal"version_etc_copyright"; WPtrversion_literal"version-etc#str.44"; WInt2026
⊢
focused goal
stream :
d :
args :
listarg
Hclasses :
=
version_output_classesWPtrstream; WPtrversion_literal"version-etc#str.46"; WPtrversion_literal"version-etc#str.47"
⊢
focused goal
stream :
d :
args :
listarg
Hclasses :
=
version_output_classesWPtrstream; WPtrversion_literal"version-etc#str.51"; WPtrversion_literal"hello#str.72"; WPtrversion_literal"hello#str.73"; WPtrversion_literal"hello#str.74"; WPtrversion_literal"hello#str.75"
⊢
all: eexists ; split ; exact Hclasses | repeat apply Forall_cons ; auto | ; constructor
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros stream g xs d args Hin Hclasses
apply output_abi_classes
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; cbn [ hello_output_api name_eqb ] ; try exact Hclasses
all: eexists ; split ; exact Hclasses | repeat apply Forall_cons ; auto | ; constructor
Explore proof 4 tactics
Initial goal
⊢
intros stream g xs d args Hin Hclasses
⊢
output_abihello_output_apig CResultd W args
apply output_abi_classes
⊢
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; cbn [ hello_output_api name_eqb ] ; try exact Hclasses
3 openstream :
d :
args :
listarg
Hclasses :
=
replicateDatatypes.lengthWPtrversion_literal"version-etc#str.58"; WPtrversion_literal"version-etc#str.59" P
⊢
focused goal
stream :
d :
args :
listarg
Hclasses :
=
replicateDatatypes.lengthWPtrversion_literal"version-etc#str.60"; WPtrversion_literal"version-etc#str.61"; WPtrversion_literal"version-etc#str.62" P
⊢
focused goal
stream :
d :
args :
listarg
Hclasses :
=
replicateDatatypes.lengthWPtrversion_literal"version-etc#str.63"; WPtrversion_literal"version-etc#str.64" P
⊢
all: eexists ; split ; exact Hclasses | repeat apply Forall_cons ; auto | ; constructor
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros stream g xs d args Hin Hclasses
apply output_abi_classes
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; cbn [ hello_output_api name_eqb ] ; try exact Hclasses
all: eexists ; split ; exact Hclasses | repeat apply Forall_cons ; auto | ; constructor
Actual stdout-facing version/footer calls keep their stream open and non-wide. The fixed handle is a world fact, not a second token.
libc_stream_wirep stream m w h ∧ libc_stdoutw = stream ∧ ∃file, libc_file_atw stream = Somefile ∧ orientationlibc_stream_statew stream ≠ WideOriented
∀ stream g xs w
Ing, xs version_output_argsstream
output_targethello_output_apig libc_stdout w xs = stream
Explore proof 2 tactics
Initial goal
⊢
∀stream : ptr g : name xs : listword w : libc_world, Ing, xs version_output_argsstream → output_targethello_output_apig libc_stdout w xs = stream
intros stream g xs w Hin
⊢
output_targethello_output_apig libc_stdout w xs = stream
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros stream g xs w Hin
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; reflexivity
Explore proof 2 tactics
Initial goal
⊢
∀stream : ptr g : name xs : listword w : libc_world, Ing, xs emit_output_argsstream → libc_stdoutw = stream → output_targethello_output_apig libc_stdout w xs = stream
intros stream g xs w Hin Hstdout
⊢
output_targethello_output_apig libc_stdout w xs = stream
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros stream g xs w Hin Hstdout
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; auto
∀ rep requests wide stream g xs m w h
Ing, xs version_output_argsstream
∀l v, l, v ∈ hello_output_pieces → h !! l = Somev
agreesm h
hello_stdio_wirep stream m w h
contract_prehello_output_specrep requests wide g xs m w
Explore proof 5 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop stream : ptr g : name xs : listword m : mem w : libc_world h : gmappiece pval, Ing, xs version_output_argsstream → ∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev → agreesm h → hello_stdio_wirep stream m w h → contract_prehello_output_specrep requests wide g xs m w
intros rep requests wide stream g xs m w h Hin Howned Ha Hr & _ & Hstdout & Hfile & Hn
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
xs :
listword
m :
w :
Hin :
Ing, xs version_output_argsstream
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hr :
libc_stream_readyrep m w
Hstdout :
libc_stdoutw = stream
Hfile :
∃file : libc_file, libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
⊢
contract_prehello_output_specrep requests wide g xs m w
destruct hello_version_textstream g xs m h Hin Howned Ha as bytes Htext
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
xs :
listword
m :
w :
Hin :
Ing, xs version_output_argsstream
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hr :
libc_stream_readyrep m w
Hstdout :
libc_stdoutw = stream
Hfile :
∃file : libc_file, libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
bytes :
listZ
Htext :
output_texthello_output_apig m xs bytes
⊢
contract_prehello_output_specrep requests wide g xs m w
unfold hello_output_spec
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
xs :
listword
m :
w :
Hin :
Ing, xs version_output_argsstream
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hr :
libc_stream_readyrep m w
Hstdout :
libc_stdoutw = stream
Hfile :
∃file : libc_file, libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
bytes :
listZ
Htext :
output_texthello_output_apig m xs bytes
⊢
contract_preoutput_contracthello_output_apig libc_stream_modelrep requests wide libc_stdout xs m w
destruct Hfile as file Hfile
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
xs :
listword
m :
w :
Hin :
Ing, xs version_output_argsstream
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hr :
libc_stream_readyrep m w
Hstdout :
libc_stdoutw = stream
file :
Hfile :
libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
bytes :
listZ
Htext :
output_texthello_output_apig m xs bytes
⊢
contract_preoutput_contracthello_output_apig libc_stream_modelrep requests wide libc_stdout xs m w
apply libc_output_admitted with file := file bytes := bytes ; exact Hr | | | exact Htext ; rewrite hello_version_target_ _ _ _ Hin ; assumption
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide stream g xs m w h Hin Howned Ha Hr & _ & Hstdout & Hfile & Hn
destruct hello_version_textstream g xs m h Hin Howned Ha as bytes Htext
unfold hello_output_spec
destruct Hfile as file Hfile
apply libc_output_admitted with file := file bytes := bytes ; exact Hr | | | exact Htext ; rewrite hello_version_target_ _ _ _ Hin ; assumption
Explore proof 5 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop stream : ptr g : name xs : listword m : mem w : libc_world h : gmappiece pval, Ing, xs emit_output_argsstream → ∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev → agreesm h → hello_stdio_wirep stream m w h → contract_prehello_output_specrep requests wide g xs m w
intros rep requests wide stream g xs m w h Hin Howned Ha Hr & _ & Hstdout & Hfile & Hn
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
xs :
listword
m :
w :
Hin :
Ing, xs emit_output_argsstream
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hr :
libc_stream_readyrep m w
Hstdout :
libc_stdoutw = stream
Hfile :
∃file : libc_file, libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
⊢
contract_prehello_output_specrep requests wide g xs m w
destruct hello_footer_textstream g xs m h Hin Howned Ha as bytes Htext
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
xs :
listword
m :
w :
Hin :
Ing, xs emit_output_argsstream
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hr :
libc_stream_readyrep m w
Hstdout :
libc_stdoutw = stream
Hfile :
∃file : libc_file, libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
bytes :
listZ
Htext :
output_texthello_output_apig m xs bytes
⊢
contract_prehello_output_specrep requests wide g xs m w
unfold hello_output_spec
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
xs :
listword
m :
w :
Hin :
Ing, xs emit_output_argsstream
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hr :
libc_stream_readyrep m w
Hstdout :
libc_stdoutw = stream
Hfile :
∃file : libc_file, libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
bytes :
listZ
Htext :
output_texthello_output_apig m xs bytes
⊢
contract_preoutput_contracthello_output_apig libc_stream_modelrep requests wide libc_stdout xs m w
destruct Hfile as file Hfile
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
xs :
listword
m :
w :
Hin :
Ing, xs emit_output_argsstream
Howned :
∀l : piece v : pval, l, v ∈ hello_output_pieces → h !! l = Somev
Ha :
agreesm h
Hr :
libc_stream_readyrep m w
Hstdout :
libc_stdoutw = stream
file :
Hfile :
libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
bytes :
listZ
Htext :
output_texthello_output_apig m xs bytes
⊢
contract_preoutput_contracthello_output_apig libc_stream_modelrep requests wide libc_stdout xs m w
apply libc_output_admitted with file := file bytes := bytes ; exact Hr | | | exact Htext ; rewrite hello_footer_target_ _ _ _ Hin Hstdout ; assumption
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide stream g xs m w h Hin Howned Ha Hr & _ & Hstdout & Hfile & Hn
destruct hello_footer_textstream g xs m h Hin Howned Ha as bytes Htext
unfold hello_output_spec
destruct Hfile as file Hfile
apply libc_output_admitted with file := file bytes := bytes ; exact Hr | | | exact Htext ; rewrite hello_footer_target_ _ _ _ Hin Hstdout ; assumption
The actual author life-token premise, with fixture-derived regions.
∀ s
Ins "hello#str.72"; "hello#str.73"; "hello#str.74"; "hello#str.75"
Explore proof 8 tactics
Initial goal
⊢
∀s : string, Ins "hello#str.72"; "hello#str.73"; "hello#str.74"; "hello#str.75" → PLiveptr_addrversion_literals, VLivehello_literal_regions ∈ hello_output_pieces
intros s Hin
s :
Hin :
Ins "hello#str.72"; "hello#str.73"; "hello#str.74"; "hello#str.75"
apply list_elem_of_In
s :
Hin :
Ins "hello#str.72"; "hello#str.73"; "hello#str.74"; "hello#str.75"
unfold hello_output_pieces
s :
Hin :
Ins "hello#str.72"; "hello#str.73"; "hello#str.74"; "hello#str.75"
apply in_flat_map
s :
Hin :
Ins "hello#str.72"; "hello#str.73"; "hello#str.74"; "hello#str.75"
exists s
s :
Hin :
Ins "hello#str.72"; "hello#str.73"; "hello#str.74"; "hello#str.75"
split ; simpl in * ; tauto |
s :
Hin :
Ins "hello#str.72"; "hello#str.73"; "hello#str.74"; "hello#str.75"
left
s :
Hin :
Ins "hello#str.72"; "hello#str.73"; "hello#str.74"; "hello#str.75"
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros s Hin
apply list_elem_of_In
unfold hello_output_pieces
apply in_flat_map
exists s
split ; simpl in * ; tauto |
left
reflexivity
Bind the very machine used by HelloVersion's triples. The proofs below type-check invocation transport across the helper aliases.
The ordinary endpoint has exactly the overwrite shape consumed by HelloClose. The life insertion is redundant only because it is OWNED at entry; the name and errno updates still need their Iris fragments.
∀ rep requests wide out err b o dt pending fifo xs r args s m w trace values s′ m′ w′ h
dt = out ∨ dt = err
lengthxs = 4%nat
agreesm h
R.readys m
stream_tokens_wirep out err b o m w h
M.E.invokefclose_contractlibc_stream_modelrep requests wide r args WPtrtoken_handledt s m w trace CallReturnvalues s′ m′ w′
∃n ys, values = WIntn ∧ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat ∧ closed_psdt ++ byte_psb o ys.*1 = stream_psdt pending fifo ++ byte_psb o xs.*1 ∧ agreesm′ overwriteclosed_psdt ++ byte_psb o ys h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ stream_tokens_wirep out err b o m′ w′ overwriteclosed_psdt ++ byte_psb o ys h
Proof 35 steps Qed
intros rep requests wide out err b o dt pending fifo xs r args s m w trace values s′ m′ w′ h Hdt Hxs Ha Hd Hr Hw Howned Hcall
destruct A.close_framerep requests wide out err b o dt r args s m w trace values s' m' w' h xs Hdt Hcall Ha Hd Hr Hw Hxs as ys & Hys & Hkeys & Ha′ & Hd′ & Hr′ & Hw′
assert Heq : overwriteclosed_psdt ++ byte_psb o ys h = <[PNametoken_keydt ≔ VStreamtoken_handledt None]>overwritebyte_psb o ys h
{rewrite overwrite_app
apply fin_maps.insert_id
rewrite lookup_insert_ne ; | discriminate
rewrite overwrite_out
destruct A.T.EL.S.fclose_invocation_ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & p & info & final & n & _ & _ & _ & _ & Hn & _ & _ & _ & _ & _ & Hend | why & Hbad & _ ; | discriminate Hbad
injection Hend as Hvalues
subst values
exists n, ys
split ; reflexivity |
split
{destruct Hn as → | → ; unfold stream_eof ; lia
split ; exact Hys |
split
{rewrite ! fmap_app stream_closed_keysdt pending fifo Hkeys
reflexivity
rewrite Heq
auto
Import LG LG.L
338Context registry : name → optioncontractlibc_world wi : mem → libc_world → gmappiece pval → Prop `{!SafepointStablewi} ge : genv
Expose the CURRENT authoritative heap at this boundary, not a saved main-entry heap. Freshness belongs only to this one allocation: it is not an invariant the post-state must re-establish. Unneeded main resources frame through. Kentry supplies compatibility with the consumer's other private pools without switching its interpretation.
∀ rep out err b o σ h op oq ep eq Kentry : wils_memσ ls_worldσ h → stream_tokens_wirep out err b o ls_memσ ls_worldσ overwritestream_psout op oq ++ stream_pserr ep eq h → wils_memσ ls_worldσ overwritestream_psout op oq ++ stream_pserr ep eq h
stream_tokens_wirep out err b o ls_memσ ls_worldσ h
live_atls_memσ token_baseout token_regionout
live_atls_memσ token_baseerr token_regionerr
stream_observationls_worldσ token_handleout Someop, oq
stream_observationls_worldσ token_handleerr Someep, eq
Explore proof 11 tactics
Initial goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
⊢
agreesls_memσ h → live_disjointls_memσ → R.readyls_rtσ ls_memσ → wils_memσ ls_worldσ h → stream_tokens_wirep out err b o ls_memσ ls_worldσ h → live_atls_memσ token_baseout token_regionout → live_atls_memσ token_baseerr token_regionerr → stream_observationls_worldσ token_handleout Someop, oq → stream_observationls_worldσ token_handleerr Someep, eq → ∀l : piece v : pval, l, v ∈ stream_psout op oq ++ stream_pserr ep eq → h !! l = None → gen_heap_interph ⇛ heap_interpwi σ ∗ ptsstream_psout op oq ∗ ptsstream_pserr ep eq
intros Ha Hd Hr Hw Htokens Hol Hel Hoo Heo Hfresh
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Kentry :
Hd :
Htokens :
stream_tokens_wirep out err b o ls_memσ ls_worldσ h
Hol :
live_atls_memσ token_baseout token_regionout
Hel :
live_atls_memσ token_baseerr token_regionerr
Hoo :
stream_observationls_worldσ token_handleout Someop, oq
Heo :
stream_observationls_worldσ token_handleerr Someep, eq
iIntros Hh
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Kentry :
Hd :
Htokens :
stream_tokens_wirep out err b o ls_memσ ls_worldσ h
Hol :
live_atls_memσ token_baseout token_regionout
Hel :
live_atls_memσ token_baseerr token_regionerr
Hoo :
stream_observationls_worldσ token_handleout Someop, oq
Heo :
stream_observationls_worldσ token_handleerr Someep, eq
Hh :
gen_heap_interph
∗
iMod stream_entry_allocrep out err b o _ _ h op oq ep eq Ha Htokens Hol Hel Hoo Heo Hfresh with Hh as (Hh & Ho & He & %Hnew)
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Kentry :
Hd :
Htokens :
stream_tokens_wirep out err b o ls_memσ ls_worldσ h
Hol :
live_atls_memσ token_baseout token_regionout
Hel :
live_atls_memσ token_baseerr token_regionerr
Hoo :
stream_observationls_worldσ token_handleout Someop, oq
Heo :
stream_observationls_worldσ token_handleerr Someep, eq
∗
iModIntro
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Kentry :
Hd :
Htokens :
stream_tokens_wirep out err b o ls_memσ ls_worldσ h
Hol :
live_atls_memσ token_baseout token_regionout
Hel :
live_atls_memσ token_baseerr token_regionerr
Hoo :
stream_observationls_worldσ token_handleout Someop, oq
Heo :
stream_observationls_worldσ token_handleerr Someep, eq
∗
iFrame Ho He
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Kentry :
Hd :
Htokens :
stream_tokens_wirep out err b o ls_memσ ls_worldσ h
Hol :
live_atls_memσ token_baseout token_regionout
Hel :
live_atls_memσ token_baseerr token_regionerr
Hoo :
stream_observationls_worldσ token_handleout Someop, oq
Heo :
stream_observationls_worldσ token_handleerr Someep, eq
∗
heap_interpwi σ
iExists _
2 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Kentry :
Hd :
Htokens :
stream_tokens_wirep out err b o ls_memσ ls_worldσ h
Hol :
live_atls_memσ token_baseout token_regionout
Hel :
live_atls_memσ token_baseerr token_regionerr
Hoo :
stream_observationls_worldσ token_handleout Someop, oq
Heo :
stream_observationls_worldσ token_handleerr Someep, eq
∗
shelved goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Kentry :
Hd :
Htokens :
stream_tokens_wirep out err b o ls_memσ ls_worldσ h
Hol :
live_atls_memσ token_baseout token_regionout
Hel :
live_atls_memσ token_baseerr token_regionerr
Hoo :
stream_observationls_worldσ token_handleout Someop, oq
Heo :
stream_observationls_worldσ token_handleerr Someep, eq
iFrame Hh
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Kentry :
Hd :
Htokens :
stream_tokens_wirep out err b o ls_memσ ls_worldσ h
Hol :
live_atls_memσ token_baseout token_regionout
Hel :
live_atls_memσ token_baseerr token_regionerr
Hoo :
stream_observationls_worldσ token_handleout Someop, oq
Heo :
stream_observationls_worldσ token_handleerr Someep, eq
∗
iPureIntro
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Kentry :
Hd :
Htokens :
stream_tokens_wirep out err b o ls_memσ ls_worldσ h
Hol :
live_atls_memσ token_baseout token_regionout
Hel :
live_atls_memσ token_baseerr token_regionerr
Hoo :
stream_observationls_worldσ token_handleout Someop, oq
Heo :
stream_observationls_worldσ token_handleerr Someep, eq
destruct Hnew as Ha′ Hw′
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Kentry :
Hd :
Htokens :
stream_tokens_wirep out err b o ls_memσ ls_worldσ h
Hol :
live_atls_memσ token_baseout token_regionout
Hel :
live_atls_memσ token_baseerr token_regionerr
Hoo :
stream_observationls_worldσ token_handleout Someop, oq
Heo :
stream_observationls_worldσ token_handleerr Someep, eq
repeat split ; try assumption
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
rep :
mem → libc_world → Prop
out, err :
b, o :
Z
op :
Z
oq :
listZ
ep :
Z
eq :
listZ
Kentry :
Hd :
Htokens :
stream_tokens_wirep out err b o ls_memσ ls_worldσ h
Hol :
live_atls_memσ token_baseout token_regionout
Hel :
live_atls_memσ token_baseerr token_regionerr
Hoo :
stream_observationls_worldσ token_handleout Someop, oq
Heo :
stream_observationls_worldσ token_handleerr Someep, eq
exact KentryHw Hw′
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Ha Hd Hr Hw Htokens Hol Hel Hoo Heo Hfresh
iIntros Hh
iMod stream_entry_allocrep out err b o _ _ h op oq ep eq Ha Htokens Hol Hel Hoo Heo Hfresh with Hh as (Hh & Ho & He & %Hnew)
iModIntro
iFrame Ho He
iExists _
iFrame Hh
iPureIntro
destruct Hnew as Ha′ Hw′
repeat split ; try assumption
exact KentryHw Hw′
A designated-handle fclose rule, not a dispatcher for arbitrary pointers. The consumer keeps its abstract wi and supplies its local K premise for the rest of that interpretation, as for conversion.
∀ rep requests wide out err b o dt pending fifo xs f e ls lab result v rest j Φ Htokens : ∀m w h, wim w h → stream_tokens_wirep out err b o m w h Kclose : ∀s m w h trace values s′ m′ w′ ys, M.E.invokefclose_contractlibc_stream_modelrep requests wide CResultresult W ArgP v WPtrtoken_handledt s m w trace CallReturnvalues s′ m′ w′ → ∀l u, l, u ∈ stream_psdt pending fifo ++ byte_psb o xs → h !! l = Someu → wim w h → lengthys = 4%nat → stream_tokens_wirep out err b o m′ w′ overwriteclosed_psdt ++ byte_psb o ys h → wim′ w′ overwriteclosed_psdt ++ byte_psb o ys h
dt = out ∨ dt = err
lengthxs = 4%nat
lookupTAtom"fclose" ge_globalsge = None
registryTAtom"fclose" = Somefclose_contractlibc_stream_modelrep requests wide
ptsstream_psdt pending fifo −∗ ptsbyte_psb o xs −∗ ▷∀n ys, ⌜0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat⌝ −∗ ptsclosed_psdt −∗ ptsbyte_psb o ys −∗ WPERunmkFramef putresult WIntn e ls None Execlab rest j : cexpr {Φ} −∗ WPERunmkFramef e ls None Execlab CallCResultresult W GlobalTAtom"fclose" ArgP v :: rest j : cexpr {Φ}
Proof 39 steps Qed
intros Hdt Hxs Hfn Hg Hreg Hv
iIntros Hs Hx HK
iApply C.wp_close_contractregistry wi ge f e ls lab result W TAtom"fclose" _ _ _ fclose_contractlibc_stream_modelrep requests wide WPtrtoken_handledt stream_psdt pending fifo ++ byte_psb o xs λys ⇒ closed_psdt ++ byte_psb o ys λn ys ⇒ 0 ≤ n < 2 ^ 32 ∧ lengthys = 4%nat with [Hs Hx] [HK]
–exact Hfn
–exact Hg
–reflexivity
–exact Hreg
–reflexivity
–left
reflexivity
–split ; right ; eexists ; reflexivity | eexists ; reflexivity
–intros m w h Hw Hl
eapply A.open_admitted ; exact Hdt | apply Htokens ; exact Hw |
intros l u Hin
apply Hl , elem_of_app
left
exact Hin
–intros s m w h tr vs s′ m′ w′ Ha Hd Hr Hw Hl Hi
destruct hello_fclose_framerep requests wide out err b o dt pending fifo xs _ _ s m w tr vs s' m' w' h Hdt Hxs Ha Hd Hr Htokens_ _ _ Hw Hl Hi as n & ys & → & Hn & Hys & Hkeys & Ha′ & Hd′ & Hr′ & Htokens′
exists n, ys
split ; reflexivity |
split ; exact Hn |
split ; auto |
split ; exact Hkeys |
split ; exact Ha' |
split ; exact Hd' |
split ; exact Hr' |
eapply Kclose ; eauto
–rewrite pts_app
iFrame
–iNext
iIntros n ys %Hgood Hps
rewrite pts_app
iDestruct Hps as [Hs Hx]
iApply HK with [%] Hs Hx
exact Hgood
∀ rep requests wide stream g r args xs s m w trace values s′ m′ w′ h
output_targethello_output_apig libc_stdout w xs = stream
agreesm h
R.readys m
hello_stdio_wirep stream m w h
M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ hello_stdio_wirep stream m′ w′ h ∧ ∃n, values = WIntn ∧ 0 ≤ n < 2 ^ 32
Explore proof 10 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop stream : ptr g : name r : call_result args : listarg xs : listword s : R.state m : mem w : libc_world trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world h : gmappiece pval, output_targethello_output_apig libc_stdout w xs = stream → agreesm h → live_disjointm → R.readys m → hello_stdio_wirep stream m w h → M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′ → agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ hello_stdio_wirep stream m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
intros rep requests wide stream g r args xs s m w trace values s′ m′ w′ h Htarget Ha Hd Hr Hw & Hstdout & Hfile & Hn Hcall
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Htarget :
output_targethello_output_apig libc_stdout w xs = stream
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hw :
libc_stream_wirep stream m w h
Hstdout :
libc_stdoutw = stream
Hfile :
∃file : libc_file, libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
Hcall :
M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ hello_stdio_wirep stream m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
destruct SL.output_return_framerep requests wide hello_output_apig r args xs stream s m w trace values s′ m′ w′ h eq_symHtarget Hcall Ha Hd Hr Hw as Ha′ & Hd′ & Hr′ & Hw′ & Hresult
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Htarget :
output_targethello_output_apig libc_stdout w xs = stream
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hw :
libc_stream_wirep stream m w h
Hstdout :
libc_stdoutw = stream
Hfile :
∃file : libc_file, libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
Hcall :
M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′
Ha′ :
agreesm′ h
Hd′ :
Hr′ :
R.readys′ m′
Hw′ :
libc_stream_wirep stream m′ w′ h
Hresult :
∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ hello_stdio_wirep stream m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
destruct SL.output_open_narrowrep requests wide hello_output_apig r args xs stream s m w trace CallReturnvalues s′ m′ w′ eq_symHtarget Hn Hcall as Hfile′ & Hn′ & Hstdout′
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Htarget :
output_targethello_output_apig libc_stdout w xs = stream
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hw :
libc_stream_wirep stream m w h
Hstdout :
libc_stdoutw = stream
Hfile :
∃file : libc_file, libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
Hcall :
M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′
Ha′ :
agreesm′ h
Hd′ :
Hr′ :
R.readys′ m′
Hw′ :
libc_stream_wirep stream m′ w′ h
Hresult :
∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
Hfile′ :
∃file : libc_file, libc_file_atw′ stream = Somefile
Hn′ :
orientationlibc_stream_statew′ stream ≠ WideOriented
Hstdout′ :
libc_stdoutw′ = libc_stdoutw
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ hello_stdio_wirep stream m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
split ; exact Ha′ |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Htarget :
output_targethello_output_apig libc_stdout w xs = stream
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hw :
libc_stream_wirep stream m w h
Hstdout :
libc_stdoutw = stream
Hfile :
∃file : libc_file, libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
Hcall :
M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′
Ha′ :
agreesm′ h
Hd′ :
Hr′ :
R.readys′ m′
Hw′ :
libc_stream_wirep stream m′ w′ h
Hresult :
∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
Hfile′ :
∃file : libc_file, libc_file_atw′ stream = Somefile
Hn′ :
orientationlibc_stream_statew′ stream ≠ WideOriented
Hstdout′ :
libc_stdoutw′ = libc_stdoutw
⊢
live_disjointm′ ∧ R.readys′ m′ ∧ hello_stdio_wirep stream m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
split ; exact Hd′ |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Htarget :
output_targethello_output_apig libc_stdout w xs = stream
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hw :
libc_stream_wirep stream m w h
Hstdout :
libc_stdoutw = stream
Hfile :
∃file : libc_file, libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
Hcall :
M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′
Ha′ :
agreesm′ h
Hd′ :
Hr′ :
R.readys′ m′
Hw′ :
libc_stream_wirep stream m′ w′ h
Hresult :
∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
Hfile′ :
∃file : libc_file, libc_file_atw′ stream = Somefile
Hn′ :
orientationlibc_stream_statew′ stream ≠ WideOriented
Hstdout′ :
libc_stdoutw′ = libc_stdoutw
⊢
R.readys′ m′ ∧ hello_stdio_wirep stream m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
split ; exact Hr′ |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Htarget :
output_targethello_output_apig libc_stdout w xs = stream
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hw :
libc_stream_wirep stream m w h
Hstdout :
libc_stdoutw = stream
Hfile :
∃file : libc_file, libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
Hcall :
M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′
Ha′ :
agreesm′ h
Hd′ :
Hr′ :
R.readys′ m′
Hw′ :
libc_stream_wirep stream m′ w′ h
Hresult :
∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
Hfile′ :
∃file : libc_file, libc_file_atw′ stream = Somefile
Hn′ :
orientationlibc_stream_statew′ stream ≠ WideOriented
Hstdout′ :
libc_stdoutw′ = libc_stdoutw
⊢
hello_stdio_wirep stream m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
split ; | exact Hresult
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Htarget :
output_targethello_output_apig libc_stdout w xs = stream
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hw :
libc_stream_wirep stream m w h
Hstdout :
libc_stdoutw = stream
Hfile :
∃file : libc_file, libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
Hcall :
M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′
Ha′ :
agreesm′ h
Hd′ :
Hr′ :
R.readys′ m′
Hw′ :
libc_stream_wirep stream m′ w′ h
Hresult :
∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
Hfile′ :
∃file : libc_file, libc_file_atw′ stream = Somefile
Hn′ :
orientationlibc_stream_statew′ stream ≠ WideOriented
Hstdout′ :
libc_stdoutw′ = libc_stdoutw
⊢
hello_stdio_wirep stream m′ w′ h
split ; exact Hw′ |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Htarget :
output_targethello_output_apig libc_stdout w xs = stream
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hw :
libc_stream_wirep stream m w h
Hstdout :
libc_stdoutw = stream
Hfile :
∃file : libc_file, libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
Hcall :
M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′
Ha′ :
agreesm′ h
Hd′ :
Hr′ :
R.readys′ m′
Hw′ :
libc_stream_wirep stream m′ w′ h
Hresult :
∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
Hfile′ :
∃file : libc_file, libc_file_atw′ stream = Somefile
Hn′ :
orientationlibc_stream_statew′ stream ≠ WideOriented
Hstdout′ :
libc_stdoutw′ = libc_stdoutw
⊢
libc_stdoutw′ = stream ∧ ∃file : libc_file, libc_file_atw′ stream = Somefile ∧ orientationlibc_stream_statew′ stream ≠ WideOriented
split ; congruence |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Htarget :
output_targethello_output_apig libc_stdout w xs = stream
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hw :
libc_stream_wirep stream m w h
Hstdout :
libc_stdoutw = stream
Hfile :
∃file : libc_file, libc_file_atw stream = Somefile
Hn :
orientationlibc_stream_statew stream ≠ WideOriented
Hcall :
M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′
Ha′ :
agreesm′ h
Hd′ :
Hr′ :
R.readys′ m′
Hw′ :
libc_stream_wirep stream m′ w′ h
Hresult :
∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
Hfile′ :
∃file : libc_file, libc_file_atw′ stream = Somefile
Hn′ :
orientationlibc_stream_statew′ stream ≠ WideOriented
Hstdout′ :
libc_stdoutw′ = libc_stdoutw
⊢
∃file : libc_file, libc_file_atw′ stream = Somefile ∧ orientationlibc_stream_statew′ stream ≠ WideOriented
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide stream g r args xs s m w trace values s′ m′ w′ h Htarget Ha Hd Hr Hw & Hstdout & Hfile & Hn Hcall
destruct SL.output_return_framerep requests wide hello_output_apig r args xs stream s m w trace values s′ m′ w′ h eq_symHtarget Hcall Ha Hd Hr Hw as Ha′ & Hd′ & Hr′ & Hw′ & Hresult
destruct SL.output_open_narrowrep requests wide hello_output_apig r args xs stream s m w trace CallReturnvalues s′ m′ w′ eq_symHtarget Hn Hcall as Hfile′ & Hn′ & Hstdout′
split ; exact Ha′ |
split ; exact Hd′ |
split ; exact Hr′ |
split ; | exact Hresult
split ; exact Hw′ |
split ; congruence |
auto
These statements are HelloVersion's two output-frame premises, specialized to the concrete registry/spec and represented world.
∀ rep requests wide stream g xs r args s m w h trace values s′ m′ w′
Ing, xs version_output_argsstream
agreesm h
R.readys m
hello_stdio_wirep stream m w h
M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ hello_stdio_wirep stream m′ w′ h ∧ ∃n, values = WIntn ∧ 0 ≤ n < 2 ^ 32
Explore proof 3 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop stream : ptr g : name xs : listword r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, Ing, xs version_output_argsstream → agreesm h → live_disjointm → R.readys m → hello_stdio_wirep stream m w h → M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′ → agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ hello_stdio_wirep stream m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
intros
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
xs :
listword
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
Ing, xs version_output_argsstream
H0 :
agreesm h
H1 :
H2 :
R.readys m
H3 :
hello_stdio_wirep stream m w h
H4 :
M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ hello_stdio_wirep stream m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
eapply hello_output_frame ; eauto
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
xs :
listword
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
Ing, xs version_output_argsstream
H0 :
agreesm h
H1 :
H2 :
R.readys m
H3 :
hello_stdio_wirep stream m w h
H4 :
M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′
⊢
output_targethello_output_apig libc_stdout w xs = stream
eapply hello_version_target ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 3 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop stream : ptr g : name xs : listword r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, Ing, xs emit_output_argsstream → agreesm h → live_disjointm → R.readys m → hello_stdio_wirep stream m w h → M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′ → agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ hello_stdio_wirep stream m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
intros rep requests wide stream g xs r args s m w h trace values s′ m′ w′ Hin Ha Hd Hr Hw Hcall
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
xs :
listword
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hin :
Ing, xs emit_output_argsstream
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hw :
hello_stdio_wirep stream m w h
Hcall :
M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ hello_stdio_wirep stream m′ w′ h ∧ ∃n : Z, values = WIntn ∧ 0 ≤ n < 2 ^ 32
eapply hello_output_frame ; eauto
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
stream :
g :
xs :
listword
r :
args :
listarg
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hin :
Ing, xs emit_output_argsstream
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hw :
hello_stdio_wirep stream m w h
Hcall :
M.E.invokehello_output_specrep requests wide g r args xs s m w trace CallReturnvalues s′ m′ w′
⊢
output_targethello_output_apig libc_stdout w xs = stream
eapply hello_footer_target ; exact Hin | exact proj1proj2Hw
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide stream g xs r args s m w h trace values s′ m′ w′ Hin Ha Hd Hr Hw Hcall
eapply hello_output_frame ; eauto
eapply hello_footer_target ; exact Hin | exact proj1proj2Hw
HelloClose's complete ordinary _exit interface over its actual invocation relation. It requires no successful host completion to establish admission or absence of ordinary returns.
∀ rep requests wide host fallback p
hello_stdio_registryrep requests wide host fallback TAtom"_exit" = Somelibc_hard_exit_contractrep host ∧ contract_returnslibc_hard_exit_contractrep host = RVoid ∧ ∀v, contract_abilibc_hard_exit_contractrep host CVoid ArgW v ∧ ∀n m w h, 0 ≤ n < 2 ^ 32 → libc_closing_wirep p m w h → contract_prelibc_hard_exit_contractrep host WIntn m w ∧ ∀args n s m w trace values s′ m′ w′, C.L.M.E.invokelibc_hard_exit_contractrep host CVoid args WIntn s m w trace CallReturnvalues s′ m′ w′ → False
Explore proof 13 tactics
Initial goal
⊢
∀rep : mem → libc_world → Prop requests : libc_world → ptr → Z → Z → Prop wide : libc_world → ptr → stream_state → stream_state → bool → Prop host : mem → libc_world → Prop fallback : name → optioncontractlibc_world p : ptr, hello_stdio_registryrep requests wide host fallback TAtom"_exit" = Somelibc_hard_exit_contractrep host ∧ contract_returnslibc_hard_exit_contractrep host = RVoid ∧ ∀v : value, contract_abilibc_hard_exit_contractrep host CVoid ArgW v ∧ ∀n : Z m : mem w : libc_world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → libc_closing_wirep p m w h → contract_prelibc_hard_exit_contractrep host WIntn m w ∧ ∀args : listarg n : Z s : R.state m : mem w : libc_world trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, C.L.M.E.invokelibc_hard_exit_contractrep host CVoid args WIntn s m w trace CallReturnvalues s′ m′ w′ → False
intros rep requests wide host fallback p
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
⊢
hello_stdio_registryrep requests wide host fallback TAtom"_exit" = Somelibc_hard_exit_contractrep host ∧ contract_returnslibc_hard_exit_contractrep host = RVoid ∧ ∀v : value, contract_abilibc_hard_exit_contractrep host CVoid ArgW v ∧ ∀n : Z m : mem w : libc_world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → libc_closing_wirep p m w h → contract_prelibc_hard_exit_contractrep host WIntn m w ∧ ∀args : listarg n : Z s : R.state m : mem w : libc_world trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, C.L.M.E.invokelibc_hard_exit_contractrep host CVoid args WIntn s m w trace CallReturnvalues s′ m′ w′ → False
split ; reflexivity |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
⊢
contract_returnslibc_hard_exit_contractrep host = RVoid ∧ ∀v : value, contract_abilibc_hard_exit_contractrep host CVoid ArgW v ∧ ∀n : Z m : mem w : libc_world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → libc_closing_wirep p m w h → contract_prelibc_hard_exit_contractrep host WIntn m w ∧ ∀args : listarg n : Z s : R.state m : mem w : libc_world trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, C.L.M.E.invokelibc_hard_exit_contractrep host CVoid args WIntn s m w trace CallReturnvalues s′ m′ w′ → False
split ; reflexivity |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
⊢
∀v : value, contract_abilibc_hard_exit_contractrep host CVoid ArgW v ∧ ∀n : Z m : mem w : libc_world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → libc_closing_wirep p m w h → contract_prelibc_hard_exit_contractrep host WIntn m w ∧ ∀args : listarg n : Z s : R.state m : mem w : libc_world trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, C.L.M.E.invokelibc_hard_exit_contractrep host CVoid args WIntn s m w trace CallReturnvalues s′ m′ w′ → False
split ; intros ; split ; reflexivity | eexists ; reflexivity |
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
⊢
∀n : Z m : mem w : libc_world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → libc_closing_wirep p m w h → contract_prelibc_hard_exit_contractrep host WIntn m w ∧ ∀args : listarg n : Z s : R.state m : mem w : libc_world trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, C.L.M.E.invokelibc_hard_exit_contractrep host CVoid args WIntn s m w trace CallReturnvalues s′ m′ w′ → False
split
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
⊢
∀n : Z m : mem w : libc_world h : gmappiece pval, 0 ≤ n < 2 ^ 32 → libc_closing_wirep p m w h → contract_prelibc_hard_exit_contractrep host WIntn m w
focused goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
⊢
∀args : listarg n : Z s : R.state m : mem w : libc_world trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, C.L.M.E.invokelibc_hard_exit_contractrep host CVoid args WIntn s m w trace CallReturnvalues s′ m′ w′ → False
–intros n m w h Hn Hready & _ & Hphase
2 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
n :
Z
m :
w :
Hn :
0 ≤ n < 2 ^ 32
Hready :
libc_stream_readyrep m w
Hphase :
∀kind : handoff_kind, shutdown_atw.2 ≠ HandedOffkind
⊢
contract_prelibc_hard_exit_contractrep host WIntn m w
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
⊢
∀args : listarg n : Z s : R.state m : mem w : libc_world trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, C.L.M.E.invokelibc_hard_exit_contractrep host CVoid args WIntn s m w trace CallReturnvalues s′ m′ w′ → False
apply hard_exit_admitted with bits := n
4 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
n :
Z
m :
w :
Hn :
0 ≤ n < 2 ^ 32
Hready :
libc_stream_readyrep m w
Hphase :
∀kind : handoff_kind, shutdown_atw.2 ≠ HandedOffkind
⊢
libc_readyrep m w
focused goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
n :
Z
m :
w :
Hn :
0 ≤ n < 2 ^ 32
Hready :
libc_stream_readyrep m w
Hphase :
∀kind : handoff_kind, shutdown_atw.2 ≠ HandedOffkind
focused goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
n :
Z
m :
w :
Hn :
0 ≤ n < 2 ^ 32
Hready :
libc_stream_readyrep m w
Hphase :
∀kind : handoff_kind, shutdown_atw.2 ≠ HandedOffkind
⊢
∀kind : handoff_kind, shutdown_atw.2 ≠ HandedOffkind
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
⊢
∀args : listarg n : Z s : R.state m : mem w : libc_world trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, C.L.M.E.invokelibc_hard_exit_contractrep host CVoid args WIntn s m w trace CallReturnvalues s′ m′ w′ → False
+apply libc_stream_ready_libc
4 openrep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
n :
Z
m :
w :
Hn :
0 ≤ n < 2 ^ 32
Hready :
libc_stream_readyrep m w
Hphase :
∀kind : handoff_kind, shutdown_atw.2 ≠ HandedOffkind
⊢
libc_stream_readyrep m w
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
n :
Z
m :
w :
Hn :
0 ≤ n < 2 ^ 32
Hready :
libc_stream_readyrep m w
Hphase :
∀kind : handoff_kind, shutdown_atw.2 ≠ HandedOffkind
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
n :
Z
m :
w :
Hn :
0 ≤ n < 2 ^ 32
Hready :
libc_stream_readyrep m w
Hphase :
∀kind : handoff_kind, shutdown_atw.2 ≠ HandedOffkind
⊢
∀kind : handoff_kind, shutdown_atw.2 ≠ HandedOffkind
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
⊢
∀args : listarg n : Z s : R.state m : mem w : libc_world trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, C.L.M.E.invokelibc_hard_exit_contractrep host CVoid args WIntn s m w trace CallReturnvalues s′ m′ w′ → False
exact Hready
3 opendeferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
n :
Z
m :
w :
Hn :
0 ≤ n < 2 ^ 32
Hready :
libc_stream_readyrep m w
Hphase :
∀kind : handoff_kind, shutdown_atw.2 ≠ HandedOffkind
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
n :
Z
m :
w :
Hn :
0 ≤ n < 2 ^ 32
Hready :
libc_stream_readyrep m w
Hphase :
∀kind : handoff_kind, shutdown_atw.2 ≠ HandedOffkind
⊢
∀kind : handoff_kind, shutdown_atw.2 ≠ HandedOffkind
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
⊢
∀args : listarg n : Z s : R.state m : mem w : libc_world trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, C.L.M.E.invokelibc_hard_exit_contractrep host CVoid args WIntn s m w trace CallReturnvalues s′ m′ w′ → False
+split ; reflexivity | exact Hn
2 opendeferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
n :
Z
m :
w :
Hn :
0 ≤ n < 2 ^ 32
Hready :
libc_stream_readyrep m w
Hphase :
∀kind : handoff_kind, shutdown_atw.2 ≠ HandedOffkind
⊢
∀kind : handoff_kind, shutdown_atw.2 ≠ HandedOffkind
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
⊢
∀args : listarg n : Z s : R.state m : mem w : libc_world trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, C.L.M.E.invokelibc_hard_exit_contractrep host CVoid args WIntn s m w trace CallReturnvalues s′ m′ w′ → False
+exact Hphase
deferred goal
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
⊢
∀args : listarg n : Z s : R.state m : mem w : libc_world trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world, C.L.M.E.invokelibc_hard_exit_contractrep host CVoid args WIntn s m w trace CallReturnvalues s′ m′ w′ → False
–intros
rep :
mem → libc_world → Prop
requests :
libc_world → ptr → Z → Z → Prop
wide :
libc_world → ptr → stream_state → stream_state → bool → Prop
host :
mem → libc_world → Prop
fallback :
name → optioncontractlibc_world
p :
args :
listarg
n :
Z
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
H :
C.L.M.E.invokelibc_hard_exit_contractrep host CVoid args WIntn s m w trace CallReturnvalues s′ m′ w′
⊢
False
eapply X.hard_exit_no_return ; eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros rep requests wide host fallback p
split ; reflexivity |
split ; reflexivity |
split ; intros ; split ; reflexivity | eexists ; reflexivity |
split
–intros n m w h Hn Hready & _ & Hphase
apply hard_exit_admitted with bits := n
+apply libc_stream_ready_libc
exact Hready
+split ; reflexivity | exact Hn
+exact Hphase
–intros
eapply X.hard_exit_no_return ; eauto
Standalone users retain the original functor and theorem paths.
Main supplies one instance beneath output and callback triples.
Exercise the Iris rule, not just its pure replacement map: an actual fclose call instruction returns closed-token and sampled-byte resources through the following return instruction, on the fixture's exact LG.
Import LG LG.L
stream_tokens_wiλ_ _ ⇒ True T.out T.err 5120 0
λ_ ⇒ Somefclose_contractF.model
Explore proof 3 tactics
Initial goal
apply H.A.tokens_safepoint
⊢
∀s : InterpRuntime.state m : mem s′ : InterpRuntime.state m′ : mem w : libc_world, InterpRuntime.safepoints m s′ m′ → libc_stream_readyλ_ : mem _ : libc_world ⇒ True m w → libc_stream_readyλ_ : mem _ : libc_world ⇒ True m′ w
intros s m s′ m′ w → → Hw
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True m w
exact Hw
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 1 tactics
Initial goal
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
reflexivity
Instantiate the entry wrapper itself, retaining separately owned errno. Freshness is true before allocation, not after it.
Explore proof 18 tactics
Initial goal
⊢
gen_heap_interpHelloErrnoChecks.heap ∗ ptsbyte_ps5120 0 0; 0; 0; 0 ⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
iIntros [Hh Herrno]
Hh :
gen_heap_interpHelloErrnoChecks.heap
∗
|⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
iMod H.hello_callback_entryclose_wi λ_ _ ⇒ True T.out T.err 5120 0 mkLstateconversion_mem InterpRuntime.start 64 F.worldtrue HelloErrnoChecks.heap 7 65; 66 3 [ ] with Hh as (Hσ & Ho & He)
12 open⊢
close_wiH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap → stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 H.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue overwritestream_psT.out 7 65; 66 ++ stream_psT.err 3 [ ] HelloErrnoChecks.heap → close_wiH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue overwritestream_psT.out 7 65; 66 ++ stream_psT.err 3 [ ] HelloErrnoChecks.heap
focused goal
⊢
agreesH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap
focused goal
⊢
live_disjointH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
focused goal
⊢
InterpRuntime.readyH.LG.L.ls_rtH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
focused goal
⊢
close_wiH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap
focused goal
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 H.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap
focused goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.out token_regionT.out
focused goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.err token_regionT.err
focused goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.out Some7, 65; 66
focused goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.err Some3, [ ]
focused goal
focused goal
Hσ :
H.LG.heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
∗
|⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
–intros _ Hnew
12 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
Hnew :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 H.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue overwritestream_psT.out 7 65; 66 ++ stream_psT.err 3 [ ] HelloErrnoChecks.heap
⊢
close_wiH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue overwritestream_psT.out 7 65; 66 ++ stream_psT.err 3 [ ] HelloErrnoChecks.heap
deferred goal
⊢
agreesH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap
deferred goal
⊢
live_disjointH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
deferred goal
⊢
InterpRuntime.readyH.LG.L.ls_rtH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
deferred goal
⊢
close_wiH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap
deferred goal
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 H.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap
deferred goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.out token_regionT.out
deferred goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.err token_regionT.err
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.out Some7, 65; 66
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.err Some3, [ ]
deferred goal
deferred goal
Hσ :
H.LG.heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
∗
|⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
exact Hnew
11 opendeferred goal
⊢
agreesH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap
deferred goal
⊢
live_disjointH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
deferred goal
⊢
InterpRuntime.readyH.LG.L.ls_rtH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
deferred goal
⊢
close_wiH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap
deferred goal
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 H.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap
deferred goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.out token_regionT.out
deferred goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.err token_regionT.err
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.out Some7, 65; 66
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.err Some3, [ ]
deferred goal
deferred goal
Hσ :
H.LG.heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
∗
|⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
–exact HelloErrnoChecks.heap_agrees
10 opendeferred goal
⊢
live_disjointH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
deferred goal
⊢
InterpRuntime.readyH.LG.L.ls_rtH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
deferred goal
⊢
close_wiH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap
deferred goal
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 H.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap
deferred goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.out token_regionT.out
deferred goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.err token_regionT.err
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.out Some7, 65; 66
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.err Some3, [ ]
deferred goal
deferred goal
Hσ :
H.LG.heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
∗
|⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
–exact HelloErrnoChecks.disjoint
9 opendeferred goal
⊢
InterpRuntime.readyH.LG.L.ls_rtH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
deferred goal
⊢
close_wiH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap
deferred goal
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 H.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap
deferred goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.out token_regionT.out
deferred goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.err token_regionT.err
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.out Some7, 65; 66
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.err Some3, [ ]
deferred goal
deferred goal
Hσ :
H.LG.heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
∗
|⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
–exact HelloErrnoChecks.ready
8 opendeferred goal
⊢
close_wiH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap
deferred goal
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 H.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap
deferred goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.out token_regionT.out
deferred goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.err token_regionT.err
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.out Some7, 65; 66
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.err Some3, [ ]
deferred goal
deferred goal
Hσ :
H.LG.heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
∗
|⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
–exact T.entry_wi
7 opendeferred goal
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 H.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue H.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue HelloErrnoChecks.heap
deferred goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.out token_regionT.out
deferred goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.err token_regionT.err
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.out Some7, 65; 66
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.err Some3, [ ]
deferred goal
deferred goal
Hσ :
H.LG.heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
∗
|⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
–exact T.entry_wi
6 opendeferred goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.out token_regionT.out
deferred goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.err token_regionT.err
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.out Some7, 65; 66
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.err Some3, [ ]
deferred goal
deferred goal
Hσ :
H.LG.heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
∗
|⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
–split ; reflexivity
5 opendeferred goal
⊢
live_atH.LG.L.ls_memH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_baseT.err token_regionT.err
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.out Some7, 65; 66
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.err Some3, [ ]
deferred goal
deferred goal
Hσ :
H.LG.heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
∗
|⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
–split ; reflexivity
4 opendeferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.out Some7, 65; 66
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.err Some3, [ ]
deferred goal
deferred goal
Hσ :
H.LG.heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
∗
|⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
–exists mkStreamInfo1 mkStreamByteOriented 65; 66 true 7
4 open⊢
libc_stream_atH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.out = Somestream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 ∧ stream_pendingstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 = 7 ∧ outstandingstream_protocolstream_identifier ≔ 1; stream_protocol ≔ orientation ≔ ByteOriented; outstanding ≔ 65; 66; stream_error ≔ true; stream_pending ≔ 7 = 65; 66
deferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.err Some3, [ ]
deferred goal
deferred goal
Hσ :
H.LG.heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
∗
|⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
repeat split ; reflexivity
3 opendeferred goal
⊢
stream_observationH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.err Some3, [ ]
deferred goal
deferred goal
Hσ :
H.LG.heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
∗
|⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
–exists mkStreamInfo2 stdout_initial 3
3 open⊢
libc_stream_atH.LG.L.ls_worldH.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue token_handleT.err = Somestream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 ∧ stream_pendingstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 = 3 ∧ outstandingstream_protocolstream_identifier ≔ 2; stream_protocol ≔ stdout_initial; stream_pending ≔ 3 = [ ]
deferred goal
deferred goal
Hσ :
H.LG.heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
∗
|⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
repeat split ; reflexivity
2 opendeferred goal
deferred goal
Hσ :
H.LG.heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
∗
|⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
–exact T.entry_fresh
deferred goal
Hσ :
H.LG.heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
∗
|⇛ heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
–iModIntro
Hσ :
H.LG.heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue
∗
heap_interpclose_wi H.C.L.ls_mem ≔ conversion_mem; H.C.L.ls_rt ≔ InterpRuntime.start; H.C.L.ls_fuel ≔ 64; H.C.L.ls_world ≔ F.worldtrue ∗ ptsstream_psT.out 7 65; 66 ∗ ptsstream_psT.err 3 [ ] ∗ ptsbyte_ps5120 0 0; 0; 0; 0
iFrame
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
iIntros [Hh Herrno]
iMod H.hello_callback_entryclose_wi λ_ _ ⇒ True T.out T.err 5120 0 mkLstateconversion_mem InterpRuntime.start 64 F.worldtrue HelloErrnoChecks.heap 7 65; 66 3 [ ] with Hh as (Hσ & Ho & He)
–intros _ Hnew
exact Hnew
–exact HelloErrnoChecks.heap_agrees
–exact HelloErrnoChecks.disjoint
–exact HelloErrnoChecks.ready
–exact T.entry_wi
–exact T.entry_wi
–split ; reflexivity
–split ; reflexivity
–exists mkStreamInfo1 mkStreamByteOriented 65; 66 true 7
repeat split ; reflexivity
–exists mkStreamInfo2 stdout_initial 3
repeat split ; reflexivity
–exact T.entry_fresh
–iModIntro
iFrame
575Example close_then_return_resources: ptsstream_psT.out 7 65; 66 −∗ ptsbyte_ps5120 0 0; 0; 0; 0 −∗ WPERunmkFramestub entry_env [ ] None ExecTAtom"body" CallCResultTAtom"r" W GlobalTAtom"fclose" ArgP TmpTAtom"p" JRetTmpTAtom"r" : language.exprnanofil_langregistry ge {result. ∃n ys, ⌜result = RetWIntn ∧ lengthys = 4%nat⌝ ∗ ptsclosed_psT.out ∗ ptsbyte_ps5120 0 ys}
Explore proof 23 tactics
Initial goal
⊢
ptsstream_psT.out 7 65; 66 −∗ ptsbyte_ps5120 0 0; 0; 0; 0 −∗ WPERunfr_fn ≔ stub; fr_env ≔ entry_env; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"body" CallCResultTAtom"r" W GlobalTAtom"fclose" ArgP TmpTAtom"p" JRetTmpTAtom"r" : language.exprnanofil_langregistry ge {result. ∃n : Z ys : listZ, ⌜result = RetWIntn ∧ Datatypes.lengthys = 4%nat⌝ ∗ ptsclosed_psT.out ∗ ptsbyte_ps5120 0 ys}
iIntros Ho Herrno
∗
iApply H.wp_hello_fcloseregistry close_wi ge λ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False T.out T.err 5120 0 T.out 7 65; 66 0; 0; 0; 0 stub entry_env [ ] TAtom"body" TAtom"r" TmpTAtom"p" [ ] JRetTmpTAtom"r" _ with Ho Herrno []
9 open⊢
∀m : mem w : libc_world h : gmappiece pval, close_wim w h → stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 m w h
focused goal
⊢
∀s : InterpRuntime.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : InterpRuntime.state m′ : mem w′ : libc_world ys : listZ, H.LG.L.M.E.invokefclose_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False CResultTAtom"r" W ArgP TmpTAtom"p" WPtrtoken_handleT.out s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece u : pval, l, u ∈ stream_psT.out 7 65; 66 ++ byte_ps5120 0 0; 0; 0; 0 → h !! l = Someu → close_wim w h → Datatypes.lengthys = 4%nat → stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 m′ w′ overwriteclosed_psT.out ++ byte_ps5120 0 ys h → close_wim′ w′ overwriteclosed_psT.out ++ byte_ps5120 0 ys h
focused goal
focused goal
focused goal
focused goal
focused goal
⊢
registryTAtom"fclose" = Somefclose_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False
focused goal
focused goal
∗
▷∀n : Z ys : listZ, ⌜0 ≤ n < 2 ^ 32 ∧ Datatypes.lengthys = 4%nat⌝ −∗ ptsclosed_psT.out −∗ ptsbyte_ps5120 0 ys −∗ WPH.LG.L.ERunfr_fn ≔ stub; fr_env ≔ putTAtom"r" WIntn entry_env; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"body" [ ] JRetTmpTAtom"r" {result. ∃n0 : Z ys0 : listZ, ⌜result = RetWIntn0 ∧ Datatypes.lengthys0 = 4%nat⌝ ∗ ptsclosed_psT.out ∗ ptsbyte_ps5120 0 ys0}
–intros m w h Hw
9 open⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 m w h
deferred goal
⊢
∀s : InterpRuntime.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : InterpRuntime.state m′ : mem w′ : libc_world ys : listZ, H.LG.L.M.E.invokefclose_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False CResultTAtom"r" W ArgP TmpTAtom"p" WPtrtoken_handleT.out s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece u : pval, l, u ∈ stream_psT.out 7 65; 66 ++ byte_ps5120 0 0; 0; 0; 0 → h !! l = Someu → close_wim w h → Datatypes.lengthys = 4%nat → stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 m′ w′ overwriteclosed_psT.out ++ byte_ps5120 0 ys h → close_wim′ w′ overwriteclosed_psT.out ++ byte_ps5120 0 ys h
deferred goal
deferred goal
deferred goal
deferred goal
deferred goal
⊢
registryTAtom"fclose" = Somefclose_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False
deferred goal
deferred goal
∗
▷∀n : Z ys : listZ, ⌜0 ≤ n < 2 ^ 32 ∧ Datatypes.lengthys = 4%nat⌝ −∗ ptsclosed_psT.out −∗ ptsbyte_ps5120 0 ys −∗ WPH.LG.L.ERunfr_fn ≔ stub; fr_env ≔ putTAtom"r" WIntn entry_env; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"body" [ ] JRetTmpTAtom"r" {result. ∃n0 : Z ys0 : listZ, ⌜result = RetWIntn0 ∧ Datatypes.lengthys0 = 4%nat⌝ ∗ ptsclosed_psT.out ∗ ptsbyte_ps5120 0 ys0}
exact Hw
8 opendeferred goal
⊢
∀s : InterpRuntime.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : InterpRuntime.state m′ : mem w′ : libc_world ys : listZ, H.LG.L.M.E.invokefclose_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False CResultTAtom"r" W ArgP TmpTAtom"p" WPtrtoken_handleT.out s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece u : pval, l, u ∈ stream_psT.out 7 65; 66 ++ byte_ps5120 0 0; 0; 0; 0 → h !! l = Someu → close_wim w h → Datatypes.lengthys = 4%nat → stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 m′ w′ overwriteclosed_psT.out ++ byte_ps5120 0 ys h → close_wim′ w′ overwriteclosed_psT.out ++ byte_ps5120 0 ys h
deferred goal
deferred goal
deferred goal
deferred goal
deferred goal
⊢
registryTAtom"fclose" = Somefclose_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False
deferred goal
deferred goal
∗
▷∀n : Z ys : listZ, ⌜0 ≤ n < 2 ^ 32 ∧ Datatypes.lengthys = 4%nat⌝ −∗ ptsclosed_psT.out −∗ ptsbyte_ps5120 0 ys −∗ WPH.LG.L.ERunfr_fn ≔ stub; fr_env ≔ putTAtom"r" WIntn entry_env; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"body" [ ] JRetTmpTAtom"r" {result. ∃n0 : Z ys0 : listZ, ⌜result = RetWIntn0 ∧ Datatypes.lengthys0 = 4%nat⌝ ∗ ptsclosed_psT.out ∗ ptsbyte_ps5120 0 ys0}
–intros s m w h tr vs s′ m′ w′ ys Hi Hl Hw Hlen Hnew
8 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
w :
tr :
listevent
vs :
listword
m′ :
w′ :
ys :
listZ
Hi :
H.LG.L.M.E.invokefclose_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False CResultTAtom"r" W ArgP TmpTAtom"p" WPtrtoken_handleT.out s m w tr CallReturnvs s′ m′ w′
Hl :
Hw :
close_wim w h
Hlen :
Datatypes.lengthys = 4%nat
Hnew :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 m′ w′ overwriteclosed_psT.out ++ byte_ps5120 0 ys h
deferred goal
deferred goal
deferred goal
deferred goal
deferred goal
⊢
registryTAtom"fclose" = Somefclose_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False
deferred goal
deferred goal
∗
▷∀n : Z ys : listZ, ⌜0 ≤ n < 2 ^ 32 ∧ Datatypes.lengthys = 4%nat⌝ −∗ ptsclosed_psT.out −∗ ptsbyte_ps5120 0 ys −∗ WPH.LG.L.ERunfr_fn ≔ stub; fr_env ≔ putTAtom"r" WIntn entry_env; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"body" [ ] JRetTmpTAtom"r" {result. ∃n0 : Z ys0 : listZ, ⌜result = RetWIntn0 ∧ Datatypes.lengthys0 = 4%nat⌝ ∗ ptsclosed_psT.out ∗ ptsbyte_ps5120 0 ys0}
exact Hnew
7 opendeferred goal
deferred goal
deferred goal
deferred goal
deferred goal
⊢
registryTAtom"fclose" = Somefclose_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False
deferred goal
deferred goal
∗
▷∀n : Z ys : listZ, ⌜0 ≤ n < 2 ^ 32 ∧ Datatypes.lengthys = 4%nat⌝ −∗ ptsclosed_psT.out −∗ ptsbyte_ps5120 0 ys −∗ WPH.LG.L.ERunfr_fn ≔ stub; fr_env ≔ putTAtom"r" WIntn entry_env; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"body" [ ] JRetTmpTAtom"r" {result. ∃n0 : Z ys0 : listZ, ⌜result = RetWIntn0 ∧ Datatypes.lengthys0 = 4%nat⌝ ∗ ptsclosed_psT.out ∗ ptsbyte_ps5120 0 ys0}
–left
7 opendeferred goal
deferred goal
deferred goal
deferred goal
⊢
registryTAtom"fclose" = Somefclose_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False
deferred goal
deferred goal
∗
▷∀n : Z ys : listZ, ⌜0 ≤ n < 2 ^ 32 ∧ Datatypes.lengthys = 4%nat⌝ −∗ ptsclosed_psT.out −∗ ptsbyte_ps5120 0 ys −∗ WPH.LG.L.ERunfr_fn ≔ stub; fr_env ≔ putTAtom"r" WIntn entry_env; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"body" [ ] JRetTmpTAtom"r" {result. ∃n0 : Z ys0 : listZ, ⌜result = RetWIntn0 ∧ Datatypes.lengthys0 = 4%nat⌝ ∗ ptsclosed_psT.out ∗ ptsbyte_ps5120 0 ys0}
reflexivity
6 opendeferred goal
deferred goal
deferred goal
deferred goal
⊢
registryTAtom"fclose" = Somefclose_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False
deferred goal
deferred goal
∗
▷∀n : Z ys : listZ, ⌜0 ≤ n < 2 ^ 32 ∧ Datatypes.lengthys = 4%nat⌝ −∗ ptsclosed_psT.out −∗ ptsbyte_ps5120 0 ys −∗ WPH.LG.L.ERunfr_fn ≔ stub; fr_env ≔ putTAtom"r" WIntn entry_env; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"body" [ ] JRetTmpTAtom"r" {result. ∃n0 : Z ys0 : listZ, ⌜result = RetWIntn0 ∧ Datatypes.lengthys0 = 4%nat⌝ ∗ ptsclosed_psT.out ∗ ptsbyte_ps5120 0 ys0}
–reflexivity
5 opendeferred goal
deferred goal
deferred goal
⊢
registryTAtom"fclose" = Somefclose_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False
deferred goal
deferred goal
∗
▷∀n : Z ys : listZ, ⌜0 ≤ n < 2 ^ 32 ∧ Datatypes.lengthys = 4%nat⌝ −∗ ptsclosed_psT.out −∗ ptsbyte_ps5120 0 ys −∗ WPH.LG.L.ERunfr_fn ≔ stub; fr_env ≔ putTAtom"r" WIntn entry_env; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"body" [ ] JRetTmpTAtom"r" {result. ∃n0 : Z ys0 : listZ, ⌜result = RetWIntn0 ∧ Datatypes.lengthys0 = 4%nat⌝ ∗ ptsclosed_psT.out ∗ ptsbyte_ps5120 0 ys0}
–reflexivity
4 opendeferred goal
deferred goal
⊢
registryTAtom"fclose" = Somefclose_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False
deferred goal
deferred goal
∗
▷∀n : Z ys : listZ, ⌜0 ≤ n < 2 ^ 32 ∧ Datatypes.lengthys = 4%nat⌝ −∗ ptsclosed_psT.out −∗ ptsbyte_ps5120 0 ys −∗ WPH.LG.L.ERunfr_fn ≔ stub; fr_env ≔ putTAtom"r" WIntn entry_env; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"body" [ ] JRetTmpTAtom"r" {result. ∃n0 : Z ys0 : listZ, ⌜result = RetWIntn0 ∧ Datatypes.lengthys0 = 4%nat⌝ ∗ ptsclosed_psT.out ∗ ptsbyte_ps5120 0 ys0}
–reflexivity
3 opendeferred goal
⊢
registryTAtom"fclose" = Somefclose_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False
deferred goal
deferred goal
∗
▷∀n : Z ys : listZ, ⌜0 ≤ n < 2 ^ 32 ∧ Datatypes.lengthys = 4%nat⌝ −∗ ptsclosed_psT.out −∗ ptsbyte_ps5120 0 ys −∗ WPH.LG.L.ERunfr_fn ≔ stub; fr_env ≔ putTAtom"r" WIntn entry_env; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"body" [ ] JRetTmpTAtom"r" {result. ∃n0 : Z ys0 : listZ, ⌜result = RetWIntn0 ∧ Datatypes.lengthys0 = 4%nat⌝ ∗ ptsclosed_psT.out ∗ ptsbyte_ps5120 0 ys0}
–reflexivity
2 opendeferred goal
deferred goal
∗
▷∀n : Z ys : listZ, ⌜0 ≤ n < 2 ^ 32 ∧ Datatypes.lengthys = 4%nat⌝ −∗ ptsclosed_psT.out −∗ ptsbyte_ps5120 0 ys −∗ WPH.LG.L.ERunfr_fn ≔ stub; fr_env ≔ putTAtom"r" WIntn entry_env; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"body" [ ] JRetTmpTAtom"r" {result. ∃n0 : Z ys0 : listZ, ⌜result = RetWIntn0 ∧ Datatypes.lengthys0 = 4%nat⌝ ∗ ptsclosed_psT.out ∗ ptsbyte_ps5120 0 ys0}
–reflexivity
deferred goal
∗
▷∀n : Z ys : listZ, ⌜0 ≤ n < 2 ^ 32 ∧ Datatypes.lengthys = 4%nat⌝ −∗ ptsclosed_psT.out −∗ ptsbyte_ps5120 0 ys −∗ WPH.LG.L.ERunfr_fn ≔ stub; fr_env ≔ putTAtom"r" WIntn entry_env; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"body" [ ] JRetTmpTAtom"r" {result. ∃n0 : Z ys0 : listZ, ⌜result = RetWIntn0 ∧ Datatypes.lengthys0 = 4%nat⌝ ∗ ptsclosed_psT.out ∗ ptsbyte_ps5120 0 ys0}
–iNext
∗
∀n : Z ys : listZ, ⌜0 ≤ n < 2 ^ 32 ∧ Datatypes.lengthys = 4%nat⌝ −∗ ptsclosed_psT.out −∗ ptsbyte_ps5120 0 ys −∗ WPH.LG.L.ERunfr_fn ≔ stub; fr_env ≔ putTAtom"r" WIntn entry_env; fr_locals ≔ [ ]; fr_doomed ≔ None; fr_at ≔ ExecTAtom"body" [ ] JRetTmpTAtom"r" {result. ∃n0 : Z ys0 : listZ, ⌜result = RetWIntn0 ∧ Datatypes.lengthys0 = 4%nat⌝ ∗ ptsclosed_psT.out ∗ ptsbyte_ps5120 0 ys0}
iIntros n ys %Hgood Ho Herrno
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
n :
Z
ys :
listZ
Hgood :
0 ≤ n < 2 ^ 32 ∧ Datatypes.lengthys = 4%nat
∗
destruct Hgood as Hn Hys
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
n :
Z
ys :
listZ
Hn :
0 ≤ n < 2 ^ 32
Hys :
Datatypes.lengthys = 4%nat
∗
iApply wp_retregistry close_wi ge stub _ TAtom"body" TmpTAtom"r" W WIntn ; reflexivity | |
2 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
n :
Z
ys :
listZ
Hn :
0 ≤ n < 2 ^ 32
Hys :
Datatypes.lengthys = 4%nat
focused goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
n :
Z
ys :
listZ
Hn :
0 ≤ n < 2 ^ 32
Hys :
Datatypes.lengthys = 4%nat
∗
+change SomeWIntn mod 2 ^ 32 = SomeWIntn
2 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
n :
Z
ys :
listZ
Hn :
0 ≤ n < 2 ^ 32
Hys :
Datatypes.lengthys = 4%nat
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
n :
Z
ys :
listZ
Hn :
0 ≤ n < 2 ^ 32
Hys :
Datatypes.lengthys = 4%nat
∗
rewrite Z.mod_small ; reflexivity | exact Hn
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
n :
Z
ys :
listZ
Hn :
0 ≤ n < 2 ^ 32
Hys :
Datatypes.lengthys = 4%nat
∗
+iNext
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
n :
Z
ys :
listZ
Hn :
0 ≤ n < 2 ^ 32
Hys :
Datatypes.lengthys = 4%nat
∗
iExists n, ys
iFrame
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
iIntros Ho Herrno
iApply H.wp_hello_fcloseregistry close_wi ge λ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False T.out T.err 5120 0 T.out 7 65; 66 0; 0; 0; 0 stub entry_env [ ] TAtom"body" TAtom"r" TmpTAtom"p" [ ] JRetTmpTAtom"r" _ with Ho Herrno []
–intros m w h Hw
exact Hw
–intros s m w h tr vs s′ m′ w′ ys Hi Hl Hw Hlen Hnew
exact Hnew
–left
reflexivity
–reflexivity
–reflexivity
–reflexivity
–reflexivity
–reflexivity