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 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 LibcStreamLogic 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.
∀ 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.