Fil-C on Nix

Filnix wiki

the formal campaign

rocq/theories/HelloReach.v

Reference closure of the linked GNU Hello image, including function addresses passed as callbacks and symbols stored in data. This checks the image we run, not preservation of the original object collection: pruning is trusted, checked by link.pl's own reachability traversal.

From Stdlib Require Import String ZArith List Bool
From Nanofil Require Import Term Maps Syntax Values Memory Runtime Semantics Run HelloCode HelloModule HelloLeaf
Import ListNotations
Open Scope string_scope
Open Scope list_scope

Every global or initializer symbol below a term, following the same reference forms as link.pl; a callback address is not just a call.

15Fixpoint image_refst : term : listname ≔
let fix refs_list ts : listterm : listname ≔
match ts with
[ ]
⇒
[ ]
x :: xs
⇒
image_refsx ++ refs_listxs
in
match t with
TApp"global" n
⇒
n
TApp"sym" n; off
⇒
n
TApp_ ts
⇒
refs_listts
TListts
⇒
refs_listts
_
⇒
[ ]

The linked image's named items and all their outgoing references, computed once rather than unfolding its large bodies in proofs.

31Definition hello_edges: listname × listname ≔
Eval vm_compute in match hello_term with TApp"module" TListitems ⇒ flat_mapλt ⇒ match t with TApp"func" n; linkage; result; ps; bs ⇒ n, image_refst | TApp"data" n; linkage; alignment; contents ⇒ n, image_refst | _ ⇒ [ ] end items | _ ⇒ [ ] end

Static reachability from main follows all references, not just direct calls, so registration and data initialization cannot hide an edge.

44Inductive hello_reachable: name → Prop ≔
hello_reachableTAtom"main"
hello_reach_main
∀ source refs target
hello_reachablesource
Insource, refs hello_edges
Intarget refs
hello_reach_ref
hello_reachabletarget

External data imports may be supplied by startup, unlike function imports, which hello_linked requires to stay outside the globals.

52Definition hello_data_imports: liststring ≔
"stdout"; "stderr"; "program_invocation_name"; "program_invocation_short_name"; "optarg"; "optind"

Classification uses actual decoded functions and allocated globals; no missing definition is silently treated as an arbitrary import.

58Definition hello_reference_okn : name : bool ≔
match find_directn hello_module with
SomeDefined_
⇒
true
_
⇒
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false

Every edge in the image ends at a definition or an enumerated libc import, including edges originating in data rather than code.

73Lemma hello_edges_closed
forallbλedge ⇒ forallbhello_reference_ok sndedge hello_edges = true
Explore proof 2 tactics

Initial goal

⊢
forallbλedge : name × listname ⇒ forallbhello_reference_ok sndedge hello_edges = true

vm_compute

⊢
true = true

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
vm_compute
reflexivity

Every statically reachable symbol is a decoded function, allocated module symbol, external function import, or external data import.

79Theorem hello_reachable_closed
∀ n
hello_reachablen
∃f, find_directn hello_module = SomeDefinedf ∨ ∃p, lookupn hello_globals = Somep ∨ ∃s, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
Explore proof 35 tactics

Initial goal

n :
name
⊢
hello_reachablen → ∃f : func, find_directn hello_module = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

intro Hreach

n :
name
Hreach :
hello_reachablen
⊢
∃f : func, find_directn hello_module = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

assert Hok : hello_reference_okn = true

2 open

n :
name
Hreach :
hello_reachablen
⊢
hello_reference_okn = true
focused goal
n :
name
Hreach :
hello_reachablen
Hok :
hello_reference_okn = true
⊢
∃f : func, find_directn hello_module = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

{destruct Hreach as | source refs target Hsource Hedge Hin

3 open

⊢
hello_reference_okTAtom"main" = true
focused goal
source :
name
refs :
listname
target :
name
Hsource :
hello_reachablesource
Hedge :
Insource, refs hello_edges
Hin :
Intarget refs
⊢
hello_reference_oktarget = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hok :
hello_reference_okn = true
⊢
∃f : func, find_directn hello_module = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

–vm_compute

3 open

⊢
true = true
deferred goal
source :
name
refs :
listname
target :
name
Hsource :
hello_reachablesource
Hedge :
Insource, refs hello_edges
Hin :
Intarget refs
⊢
hello_reference_oktarget = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hok :
hello_reference_okn = true
⊢
∃f : func, find_directn hello_module = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

reflexivity

2 open

deferred goal
source :
name
refs :
listname
target :
name
Hsource :
hello_reachablesource
Hedge :
Insource, refs hello_edges
Hin :
Intarget refs
⊢
hello_reference_oktarget = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hok :
hello_reference_okn = true
⊢
∃f : func, find_directn hello_module = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

–pose proof hello_edges_closed as Hclosed

2 open

source :
name
refs :
listname
target :
name
Hsource :
hello_reachablesource
Hedge :
Insource, refs hello_edges
Hin :
Intarget refs
Hclosed :
forallbλedge : name × listname ⇒ forallbhello_reference_ok sndedge hello_edges = true
⊢
hello_reference_oktarget = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hok :
hello_reference_okn = true
⊢
∃f : func, find_directn hello_module = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

apply forallb_forall with x := source, refs in Hclosed ; | exact Hedge

2 open

source :
name
refs :
listname
target :
name
Hsource :
hello_reachablesource
Hedge :
Insource, refs hello_edges
Hin :
Intarget refs
Hclosed :
forallbhello_reference_ok sndsource, refs = true
⊢
hello_reference_oktarget = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hok :
hello_reference_okn = true
⊢
∃f : func, find_directn hello_module = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

apply forallb_forall with x := target in Hclosed ; exact Hclosed | exact Hin

deferred goal
n :
name
Hreach :
hello_reachablen
Hok :
hello_reference_okn = true
⊢
∃f : func, find_directn hello_module = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

unfold hello_reference_ok in Hok

n :
name
Hreach :
hello_reachablen
Hok :
match find_directn hello_module with
SomeDefined_
⇒
true
_
⇒
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, find_directn hello_module = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

destruct find_directn hello_module as f | outside_name | eqn: Hfn

3 open

n :
name
Hreach :
hello_reachablen
f :
func
Hfn :
find_directn hello_module = SomeDefinedf
Hok :
true = true
⊢
∃f0 : func, SomeDefinedf = SomeDefinedf0 ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
focused goal
n :
name
Hreach :
hello_reachablen
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, SomeOutsideoutside_name = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
focused goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, None = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

–left

3 open

n :
name
Hreach :
hello_reachablen
f :
func
Hfn :
find_directn hello_module = SomeDefinedf
Hok :
true = true
⊢
∃f0 : func, SomeDefinedf = SomeDefinedf0
deferred goal
n :
name
Hreach :
hello_reachablen
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, SomeOutsideoutside_name = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, None = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

exists f

3 open

n :
name
Hreach :
hello_reachablen
f :
func
Hfn :
find_directn hello_module = SomeDefinedf
Hok :
true = true
⊢
SomeDefinedf = SomeDefinedf
deferred goal
n :
name
Hreach :
hello_reachablen
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, SomeOutsideoutside_name = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, None = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

reflexivity

2 open

deferred goal
n :
name
Hreach :
hello_reachablen
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, SomeOutsideoutside_name = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, None = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

–right

2 open

n :
name
Hreach :
hello_reachablen
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, None = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

destruct lookupn hello_globals as p | eqn: Hp

3 open

n :
name
Hreach :
hello_reachablen
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
p :
ptr
Hp :
lookupn hello_globals = Somep
Hok :
true = true
⊢
∃p0 : ptr, Somep = Somep0 ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
focused goal
n :
name
Hreach :
hello_reachablen
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
Hp :
lookupn hello_globals = None
Hok :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃p : ptr, None = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, None = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

+left

3 open

n :
name
Hreach :
hello_reachablen
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
p :
ptr
Hp :
lookupn hello_globals = Somep
Hok :
true = true
⊢
∃p0 : ptr, Somep = Somep0
deferred goal
n :
name
Hreach :
hello_reachablen
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
Hp :
lookupn hello_globals = None
Hok :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃p : ptr, None = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, None = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

exists p

3 open

n :
name
Hreach :
hello_reachablen
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
p :
ptr
Hp :
lookupn hello_globals = Somep
Hok :
true = true
⊢
Somep = Somep
deferred goal
n :
name
Hreach :
hello_reachablen
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
Hp :
lookupn hello_globals = None
Hok :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃p : ptr, None = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, None = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

reflexivity

2 open

deferred goal
n :
name
Hreach :
hello_reachablen
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
Hp :
lookupn hello_globals = None
Hok :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃p : ptr, None = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, None = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

+right

2 open

n :
name
Hreach :
hello_reachablen
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
Hp :
lookupn hello_globals = None
Hok :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, None = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

destruct n as z | s | tag args | items ; try discriminate Hok

2 open

s :
string
Hreach :
hello_reachableTAtoms
outside_name :
name
Hfn :
find_directTAtoms hello_module = SomeOutsideoutside_name
Hp :
lookupTAtoms hello_globals = None
Hok :
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports = true
⊢
∃s0 : string, TAtoms = TAtoms0 ∧ existsbString.eqbs0 hello_externals = true ∨ existsbString.eqbs0 hello_data_imports = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, None = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

exists s

2 open

s :
string
Hreach :
hello_reachableTAtoms
outside_name :
name
Hfn :
find_directTAtoms hello_module = SomeOutsideoutside_name
Hp :
lookupTAtoms hello_globals = None
Hok :
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports = true
⊢
TAtoms = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, None = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

split ; reflexivity |

2 open

s :
string
Hreach :
hello_reachableTAtoms
outside_name :
name
Hfn :
find_directTAtoms hello_module = SomeOutsideoutside_name
Hp :
lookupTAtoms hello_globals = None
Hok :
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports = true
⊢
existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, None = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

apply orb_true_iff

2 open

s :
string
Hreach :
hello_reachableTAtoms
outside_name :
name
Hfn :
find_directTAtoms hello_module = SomeOutsideoutside_name
Hp :
lookupTAtoms hello_globals = None
Hok :
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports = true
⊢
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, None = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

exact Hok

deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃f : func, None = SomeDefinedf ∨ ∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

–right

n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hok :
match lookupn hello_globals with
Some_
⇒
true
None
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃p : ptr, lookupn hello_globals = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

destruct lookupn hello_globals as p | eqn: Hp

2 open

n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
p :
ptr
Hp :
lookupn hello_globals = Somep
Hok :
true = true
⊢
∃p0 : ptr, Somep = Somep0 ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
focused goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Hok :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃p : ptr, None = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

+left

2 open

n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
p :
ptr
Hp :
lookupn hello_globals = Somep
Hok :
true = true
⊢
∃p0 : ptr, Somep = Somep0
deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Hok :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃p : ptr, None = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

exists p

2 open

n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
p :
ptr
Hp :
lookupn hello_globals = Somep
Hok :
true = true
⊢
Somep = Somep
deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Hok :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃p : ptr, None = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

reflexivity

deferred goal
n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Hok :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃p : ptr, None = Somep ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

+right

n :
name
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Hok :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports
_
⇒
false
=
true
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

destruct n as z | s | tag args | items ; try discriminate Hok

s :
string
Hreach :
hello_reachableTAtoms
Hfn :
find_directTAtoms hello_module = None
Hp :
lookupTAtoms hello_globals = None
Hok :
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports = true
⊢
∃s0 : string, TAtoms = TAtoms0 ∧ existsbString.eqbs0 hello_externals = true ∨ existsbString.eqbs0 hello_data_imports = true

exists s

s :
string
Hreach :
hello_reachableTAtoms
Hfn :
find_directTAtoms hello_module = None
Hp :
lookupTAtoms hello_globals = None
Hok :
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports = true
⊢
TAtoms = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

split ; reflexivity |

s :
string
Hreach :
hello_reachableTAtoms
Hfn :
find_directTAtoms hello_module = None
Hp :
lookupTAtoms hello_globals = None
Hok :
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports = true
⊢
existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

apply orb_true_iff

s :
string
Hreach :
hello_reachableTAtoms
Hfn :
find_directTAtoms hello_module = None
Hp :
lookupTAtoms hello_globals = None
Hok :
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports = true
⊢
existsbString.eqbs hello_externals || existsbString.eqbs hello_data_imports = true

exact Hok

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intro Hreach
assert Hok : hello_reference_okn = true
{destruct Hreach as | source refs target Hsource Hedge Hin
–vm_compute
reflexivity
–pose proof hello_edges_closed as Hclosed
apply forallb_forall with x := source, refs in Hclosed ; | exact Hedge
apply forallb_forall with x := target in Hclosed ; exact Hclosed | exact Hin
unfold hello_reference_ok in Hok
destruct find_directn hello_module as f | outside_name | eqn: Hfn
–left
exists f
reflexivity
–right
destruct lookupn hello_globals as p | eqn: Hp
+left
exists p
reflexivity
+right
destruct n as z | s | tag args | items ; try discriminate Hok
exists s
split ; reflexivity |
apply orb_true_iff
exact Hok
–right
destruct lookupn hello_globals as p | eqn: Hp
+left
exists p
reflexivity
+right
destruct n as z | s | tag args | items ; try discriminate Hok
exists s
split ; reflexivity |
apply orb_true_iff
exact Hok

A direct call has a decoded body or names one of the enumerated external functions; a data import can never discharge this check.

108Definition hello_call_okn : name : bool ≔
match find_directn hello_module with
SomeDefined_
⇒
true
_
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals
_
⇒
false

All calls in the decoded image meet the function-only classification, independently of whether a particular control-flow path is taken.

119Lemma hello_calls_closed
forallb
λ it  ⇒
match it with
IFuncf
⇒
forallbhello_call_ok calledf
_
⇒
true
hello_module
=
true
Explore proof 2 tactics

Initial goal

⊢
forallb
λ it : item  ⇒
match it with
IFuncf
⇒
forallbhello_call_ok calledf
_
⇒
true
hello_module
=
true

vm_compute

⊢
true = true

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
vm_compute
reflexivity

Every call target of a module function is defined in the module or is a libc function import. This also covers code reached by callback.

128Theorem hello_function_target
∀ f n
InIFuncf hello_module
Inn calledf
∃body, find_directn hello_module = SomeDefinedbody ∨ ∃s, n = TAtoms ∧ existsbString.eqbs hello_externals = true
Explore proof 17 tactics

Initial goal

f :
func
n :
name
⊢
InIFuncf hello_module → Inn calledf → ∃body : func, find_directn hello_module = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true

intros Hf Hn

f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
⊢
∃body : func, find_directn hello_module = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true

pose proof hello_calls_closed as Hall

f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
Hall :
forallb
λ it : item  ⇒
match it with
IFuncf
⇒
forallbhello_call_ok calledf
_
⇒
true
hello_module
=
true
⊢
∃body : func, find_directn hello_module = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true

apply forallb_forall with x := IFuncf in Hall ; | exact Hf

f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
Hall :
forallbhello_call_ok calledf = true
⊢
∃body : func, find_directn hello_module = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true

apply forallb_forall with x := n in Hall ; | exact Hn

f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
Hall :
hello_call_okn = true
⊢
∃body : func, find_directn hello_module = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true

unfold hello_call_ok in Hall

f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
Hall :
match find_directn hello_module with
SomeDefined_
⇒
true
_
⇒
match n with
TAtoms
⇒
existsbString.eqbs hello_externals
_
⇒
false
=
true
⊢
∃body : func, find_directn hello_module = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true

destruct find_directn hello_module as body | outside_name | eqn: Hfn

3 open

f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
body :
func
Hfn :
find_directn hello_module = SomeDefinedbody
Hall :
true = true
⊢
∃body0 : func, SomeDefinedbody = SomeDefinedbody0 ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true
focused goal
f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
Hall :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals
_
⇒
false
=
true
⊢
∃body : func, SomeOutsideoutside_name = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true
focused goal
f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
Hfn :
find_directn hello_module = None
Hall :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals
_
⇒
false
=
true
⊢
∃body : func, None = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true

–left

3 open

f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
body :
func
Hfn :
find_directn hello_module = SomeDefinedbody
Hall :
true = true
⊢
∃body0 : func, SomeDefinedbody = SomeDefinedbody0
deferred goal
f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
Hall :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals
_
⇒
false
=
true
⊢
∃body : func, SomeOutsideoutside_name = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true
deferred goal
f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
Hfn :
find_directn hello_module = None
Hall :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals
_
⇒
false
=
true
⊢
∃body : func, None = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true

exists body

3 open

f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
body :
func
Hfn :
find_directn hello_module = SomeDefinedbody
Hall :
true = true
⊢
SomeDefinedbody = SomeDefinedbody
deferred goal
f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
Hall :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals
_
⇒
false
=
true
⊢
∃body : func, SomeOutsideoutside_name = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true
deferred goal
f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
Hfn :
find_directn hello_module = None
Hall :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals
_
⇒
false
=
true
⊢
∃body : func, None = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true

reflexivity

2 open

deferred goal
f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
Hall :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals
_
⇒
false
=
true
⊢
∃body : func, SomeOutsideoutside_name = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true
deferred goal
f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
Hfn :
find_directn hello_module = None
Hall :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals
_
⇒
false
=
true
⊢
∃body : func, None = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true

–right

2 open

f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
outside_name :
name
Hfn :
find_directn hello_module = SomeOutsideoutside_name
Hall :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals
_
⇒
false
=
true
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true
deferred goal
f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
Hfn :
find_directn hello_module = None
Hall :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals
_
⇒
false
=
true
⊢
∃body : func, None = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true

destruct n as z | s | tag args | items ; try discriminate Hall

2 open

f :
func
s :
string
Hf :
InIFuncf hello_module
Hn :
InTAtoms calledf
outside_name :
name
Hfn :
find_directTAtoms hello_module = SomeOutsideoutside_name
Hall :
existsbString.eqbs hello_externals = true
⊢
∃s0 : string, TAtoms = TAtoms0 ∧ existsbString.eqbs0 hello_externals = true
deferred goal
f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
Hfn :
find_directn hello_module = None
Hall :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals
_
⇒
false
=
true
⊢
∃body : func, None = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true

exists s

2 open

f :
func
s :
string
Hf :
InIFuncf hello_module
Hn :
InTAtoms calledf
outside_name :
name
Hfn :
find_directTAtoms hello_module = SomeOutsideoutside_name
Hall :
existsbString.eqbs hello_externals = true
⊢
TAtoms = TAtoms ∧ existsbString.eqbs hello_externals = true
deferred goal
f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
Hfn :
find_directn hello_module = None
Hall :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals
_
⇒
false
=
true
⊢
∃body : func, None = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true

split ; reflexivity | exact Hall

deferred goal
f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
Hfn :
find_directn hello_module = None
Hall :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals
_
⇒
false
=
true
⊢
∃body : func, None = SomeDefinedbody ∨ ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true

–right

f :
func
n :
name
Hf :
InIFuncf hello_module
Hn :
Inn calledf
Hfn :
find_directn hello_module = None
Hall :
match n with
TAtoms
⇒
existsbString.eqbs hello_externals
_
⇒
false
=
true
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true

destruct n as z | s | tag args | items ; try discriminate Hall

f :
func
s :
string
Hf :
InIFuncf hello_module
Hn :
InTAtoms calledf
Hfn :
find_directTAtoms hello_module = None
Hall :
existsbString.eqbs hello_externals = true
⊢
∃s0 : string, TAtoms = TAtoms0 ∧ existsbString.eqbs0 hello_externals = true

exists s

f :
func
s :
string
Hf :
InIFuncf hello_module
Hn :
InTAtoms calledf
Hfn :
find_directTAtoms hello_module = None
Hall :
existsbString.eqbs hello_externals = true
⊢
TAtoms = TAtoms ∧ existsbString.eqbs hello_externals = true

split ; reflexivity | exact Hall

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros Hf Hn
pose proof hello_calls_closed as Hall
apply forallb_forall with x := IFuncf in Hall ; | exact Hf
apply forallb_forall with x := n in Hall ; | exact Hn
unfold hello_call_ok in Hall
destruct find_directn hello_module as body | outside_name | eqn: Hfn
–left
exists body
reflexivity
–right
destruct n as z | s | tag args | items ; try discriminate Hall
exists s
split ; reflexivity | exact Hall
–right
destruct n as z | s | tag args | items ; try discriminate Hall
exists s
split ; reflexivity | exact Hall

A reference with neither a function definition nor a module symbol is explicitly imported; the image cannot refer to an unlisted name.

147Theorem hello_reachable_import
∀ n
hello_reachablen
find_directn hello_module = None
lookupn hello_globals = None
∃s, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
Explore proof 9 tactics

Initial goal

n :
name
⊢
hello_reachablen → find_directn hello_module = None → lookupn hello_globals = None → ∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

intros Hr Hfn Hp

n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

destruct hello_reachable_closedn Hr as Hbody | Hglobal | Himport

3 open

n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Hbody :
∃f : func, find_directn hello_module = SomeDefinedf
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
focused goal
n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Hglobal :
∃p : ptr, lookupn hello_globals = Somep
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
focused goal
n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Himport :
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

–destruct Hbody as f Hf

3 open

n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
f :
func
Hf :
find_directn hello_module = SomeDefinedf
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Hglobal :
∃p : ptr, lookupn hello_globals = Somep
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Himport :
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

rewrite Hfn in Hf

3 open

n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
f :
func
Hf :
None = SomeDefinedf
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Hglobal :
∃p : ptr, lookupn hello_globals = Somep
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Himport :
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

discriminate Hf

2 open

deferred goal
n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Hglobal :
∃p : ptr, lookupn hello_globals = Somep
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Himport :
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

–destruct Hglobal as p Hglobal

2 open

n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
p :
ptr
Hglobal :
lookupn hello_globals = Somep
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Himport :
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

rewrite Hp in Hglobal

2 open

n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
p :
ptr
Hglobal :
None = Somep
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
deferred goal
n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Himport :
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

discriminate Hglobal

deferred goal
n :
name
Hr :
hello_reachablen
Hfn :
find_directn hello_module = None
Hp :
lookupn hello_globals = None
Himport :
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true
⊢
∃s : string, n = TAtoms ∧ existsbString.eqbs hello_externals = true ∨ existsbString.eqbs hello_data_imports = true

–exact Himport

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros Hr Hfn Hp
destruct hello_reachable_closedn Hr as Hbody | Hglobal | Himport
–destruct Hbody as f Hf
rewrite Hfn in Hf
discriminate Hf
–destruct Hglobal as p Hglobal
rewrite Hp in Hglobal
discriminate Hglobal
–exact Himport

Runtime-specific linking keeps the image and its own symbol prefix fixed, leaving only actual libc data cells to the entry proof.

161Module HelloReach R : Runtime

Module definitions take precedence over any startup data extension.

164Definition hello_genvlibc_globals : listname × ptr : genv ≔
mkGenvhello_module hello_globals ++ libc_globals R.free

A data-only extension does not bind any external function import. Cell layout and initialized representation remain entry obligations.

169Definition hello_data_extensionlibc_globals : listname × ptr : Prop ≔
∀s, existsbString.eqbs hello_externals = true → lookupTAtoms libc_globals = None

Prefix lookup needs no uniqueness or disjointness premise: the actual association-list lookup deliberately chooses the module's binding.

175Theorem hello_global_agreement
∀ libc_globals n p
lookupn hello_globals = Somep
lookupn ge_globalshello_genvlibc_globals = Somep
Explore proof 4 tactics

Initial goal

libc_globals :
listname × ptr
n :
name
p :
ptr
⊢
lookupn hello_globals = Somep → lookupn ge_globalshello_genvlibc_globals = Somep

intro Hp

libc_globals :
listname × ptr
n :
name
p :
ptr
Hp :
lookupn hello_globals = Somep
⊢
lookupn ge_globalshello_genvlibc_globals = Somep

change lookupn hello_globals ++ libc_globals = Somep

libc_globals :
listname × ptr
n :
name
p :
ptr
Hp :
lookupn hello_globals = Somep
⊢
lookupn hello_globals ++ libc_globals = Somep

rewrite lookup_app , Hp

libc_globals :
listname × ptr
n :
name
p :
ptr
Hp :
lookupn hello_globals = Somep
⊢
Somep = Somep

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intro Hp
change lookupn hello_globals ++ libc_globals = Somep
rewrite lookup_app , Hp
reflexivity

The module itself never binds one of its external function imports.

184Lemma hello_function_imports_unbound
∀ s
existsbString.eqbs hello_externals = true
lookupTAtoms hello_globals = None
Explore proof 7 tactics

Initial goal

s :
string
⊢
existsbString.eqbs hello_externals = true → lookupTAtoms hello_globals = None

intro Hs

s :
string
Hs :
existsbString.eqbs hello_externals = true
⊢
lookupTAtoms hello_globals = None

assert Hall : forallbλs ⇒ match lookupTAtoms hello_globals with None ⇒ true | _ ⇒ false end hello_externals = true by vm_compute ; reflexivity

s :
string
Hs :
existsbString.eqbs hello_externals = true
Hall :
forallb
λ s : string  ⇒
match lookupTAtoms hello_globals with
Some_
⇒
false
None
⇒
true
hello_externals
=
true
⊢
lookupTAtoms hello_globals = None

apply existsb_exists in Hs as s′ & Hin & Heq

s, s′ :
string
Hin :
Ins′ hello_externals
Heq :
s =? s′ = true
Hall :
forallb
λ s : string  ⇒
match lookupTAtoms hello_globals with
Some_
⇒
false
None
⇒
true
hello_externals
=
true
⊢
lookupTAtoms hello_globals = None

apply String.eqb_eq in Heq

s, s′ :
string
Hin :
Ins′ hello_externals
Heq :
s = s′
Hall :
forallb
λ s : string  ⇒
match lookupTAtoms hello_globals with
Some_
⇒
false
None
⇒
true
hello_externals
=
true
⊢
lookupTAtoms hello_globals = None

subst s′

s :
string
Hin :
Ins hello_externals
Hall :
forallb
λ s : string  ⇒
match lookupTAtoms hello_globals with
Some_
⇒
false
None
⇒
true
hello_externals
=
true
⊢
lookupTAtoms hello_globals = None

apply forallb_forall with x := s in Hall ; | exact Hin

s :
string
Hin :
Ins hello_externals
Hall :
match lookupTAtoms hello_globals with
Some_
⇒
false
None
⇒
true
=
true
⊢
lookupTAtoms hello_globals = None

destruct lookupTAtoms hello_globals ; discriminate Hall | reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intro Hs
assert Hall : forallbλs ⇒ match lookupTAtoms hello_globals with None ⇒ true | _ ⇒ false end hello_externals = true by vm_compute ; reflexivity
apply existsb_exists in Hs as s′ & Hin & Heq
apply String.eqb_eq in Heq
subst s′
apply forallb_forall with x := s in Hall ; | exact Hin
destruct lookupTAtoms hello_globals ; discriminate Hall | reflexivity

The constructed environment discharges the leaf proofs' full linking contract when startup supplies no external function binding.

200Theorem hello_genv_linked
∀ libc_globals
hello_data_extensionlibc_globals
hello_linkedhello_genvlibc_globals
Explore proof 11 tactics

Initial goal

libc_globals :
listname × ptr
⊢
hello_data_extensionlibc_globals → hello_linkedhello_genvlibc_globals

intro Hdata

libc_globals :
listname × ptr
Hdata :
hello_data_extensionlibc_globals
⊢
hello_linkedhello_genvlibc_globals

split ; reflexivity |

libc_globals :
listname × ptr
Hdata :
hello_data_extensionlibc_globals
⊢
∀n : name p : ptr, lookupn hello_globals = Somep → lookupn ge_globalshello_genvlibc_globals = Somep ∧ ∀s : string, existsbString.eqbs hello_externals = true → lookupTAtoms ge_globalshello_genvlibc_globals = None

split

2 open

libc_globals :
listname × ptr
Hdata :
hello_data_extensionlibc_globals
⊢
∀n : name p : ptr, lookupn hello_globals = Somep → lookupn ge_globalshello_genvlibc_globals = Somep
focused goal
libc_globals :
listname × ptr
Hdata :
hello_data_extensionlibc_globals
⊢
∀s : string, existsbString.eqbs hello_externals = true → lookupTAtoms ge_globalshello_genvlibc_globals = None

–intros n p Hp

2 open

libc_globals :
listname × ptr
Hdata :
hello_data_extensionlibc_globals
n :
name
p :
ptr
Hp :
lookupn hello_globals = Somep
⊢
lookupn ge_globalshello_genvlibc_globals = Somep
deferred goal
libc_globals :
listname × ptr
Hdata :
hello_data_extensionlibc_globals
⊢
∀s : string, existsbString.eqbs hello_externals = true → lookupTAtoms ge_globalshello_genvlibc_globals = None

apply hello_global_agreement

2 open

libc_globals :
listname × ptr
Hdata :
hello_data_extensionlibc_globals
n :
name
p :
ptr
Hp :
lookupn hello_globals = Somep
⊢
lookupn hello_globals = Somep
deferred goal
libc_globals :
listname × ptr
Hdata :
hello_data_extensionlibc_globals
⊢
∀s : string, existsbString.eqbs hello_externals = true → lookupTAtoms ge_globalshello_genvlibc_globals = None

exact Hp

deferred goal
libc_globals :
listname × ptr
Hdata :
hello_data_extensionlibc_globals
⊢
∀s : string, existsbString.eqbs hello_externals = true → lookupTAtoms ge_globalshello_genvlibc_globals = None

–intros s Hs

libc_globals :
listname × ptr
Hdata :
hello_data_extensionlibc_globals
s :
string
Hs :
existsbString.eqbs hello_externals = true
⊢
lookupTAtoms ge_globalshello_genvlibc_globals = None

change lookupTAtoms hello_globals ++ libc_globals = None

libc_globals :
listname × ptr
Hdata :
hello_data_extensionlibc_globals
s :
string
Hs :
existsbString.eqbs hello_externals = true
⊢
lookupTAtoms hello_globals ++ libc_globals = None

rewrite lookup_app , hello_function_imports_unbounds Hs

libc_globals :
listname × ptr
Hdata :
hello_data_extensionlibc_globals
s :
string
Hs :
existsbString.eqbs hello_externals = true
⊢
lookupTAtoms libc_globals = None

apply Hdata

libc_globals :
listname × ptr
Hdata :
hello_data_extensionlibc_globals
s :
string
Hs :
existsbString.eqbs hello_externals = true
⊢
existsbString.eqbs hello_externals = true

exact Hs

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intro Hdata
split ; reflexivity |
split
–intros n p Hp
apply hello_global_agreement
exact Hp
–intros s Hs
change lookupTAtoms hello_globals ++ libc_globals = None
rewrite lookup_app , hello_function_imports_unbounds Hs
apply Hdata
exact Hs

No wrapper changes the runtime's free operation.

211Theorem hello_free_agreement
∀ libc_globals
ge_freehello_genvlibc_globals = R.free
Explore proof 1 tactics

Initial goal

libc_globals :
listname × ptr
⊢
ge_freehello_genvlibc_globals = R.free

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
reflexivity

Function lookup reads only the module. This stronger agreement holds for every name, whether reachable, missing, or an external import.

217Theorem hello_find_fn_agreement
∀ ge n
ge_modulege = hello_module
find_fnge n = find_fnhello_genv[ ] n
Explore proof 4 tactics

Initial goal

ge :
genv
n :
name
⊢
ge_modulege = hello_module → find_fnge n = find_fnhello_genv[ ] n

intro Hmodule

ge :
genv
n :
name
Hmodule :
ge_modulege = hello_module
⊢
find_fnge n = find_fnhello_genv[ ] n

unfold find_fn

ge :
genv
n :
name
Hmodule :
ge_modulege = hello_module
⊢
match find_directn ge_modulege with
Somed
⇒
Somed
None
⇒
match find_aliasn ge_modulege with
Somet
⇒
find_directt ge_modulege
None
⇒
None
=
match find_directn ge_modulehello_genv[ ] with
Somed
⇒
Somed
None
⇒
match find_aliasn ge_modulehello_genv[ ] with
Somet
⇒
find_directt ge_modulehello_genv[ ]
None
⇒
None

rewrite Hmodule

ge :
genv
n :
name
Hmodule :
ge_modulege = hello_module
⊢
match find_directn hello_module with
Somed
⇒
Somed
None
⇒
match find_aliasn hello_module with
Somet
⇒
find_directt hello_module
None
⇒
None
=
match find_directn ge_modulehello_genv[ ] with
Somed
⇒
Somed
None
⇒
match find_aliasn ge_modulehello_genv[ ] with
Somet
⇒
find_directt ge_modulehello_genv[ ]
None
⇒
None

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intro Hmodule
unfold find_fn
rewrite Hmodule
reflexivity

In particular every reachable function definition is the exact body the linked environment dispatches, not a replacement with its name.

223Theorem hello_reachable_function
∀ ge n f
ge_modulege = hello_module
hello_reachablen
find_directn hello_module = SomeDefinedf
find_fnge n = SomeDefinedf
Explore proof 4 tactics

Initial goal

ge :
genv
n :
name
f :
func
⊢
ge_modulege = hello_module → hello_reachablen → find_directn hello_module = SomeDefinedf → find_fnge n = SomeDefinedf

intros Hmodule Hreach Hfn

ge :
genv
n :
name
f :
func
Hmodule :
ge_modulege = hello_module
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = SomeDefinedf
⊢
find_fnge n = SomeDefinedf

unfold find_fn

ge :
genv
n :
name
f :
func
Hmodule :
ge_modulege = hello_module
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = SomeDefinedf
⊢
match find_directn ge_modulege with
Somed
⇒
Somed
None
⇒
match find_aliasn ge_modulege with
Somet
⇒
find_directt ge_modulege
None
⇒
None
=
SomeDefinedf

rewrite Hmodule , Hfn

ge :
genv
n :
name
f :
func
Hmodule :
ge_modulege = hello_module
Hreach :
hello_reachablen
Hfn :
find_directn hello_module = SomeDefinedf
⊢
SomeDefinedf = SomeDefinedf

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros Hmodule Hreach Hfn
unfold find_fn
rewrite Hmodule , Hfn
reflexivity

External function imports cannot become internal pointer targets in any environment satisfying the leaf proofs' linking contract.

233Theorem hello_external_unbound
∀ ge s
hello_linkedge
existsbString.eqbs hello_externals = true
lookupTAtoms ge_globalsge = None ∧ find_fnge TAtoms = None
Explore proof 5 tactics

Initial goal

ge :
genv
s :
string
⊢
hello_linkedge → existsbString.eqbs hello_externals = true → lookupTAtoms ge_globalsge = None ∧ find_fnge TAtoms = None

intros Hmodule Hglobals Himports Hs

ge :
genv
s :
string
Hmodule :
ge_modulege = hello_module
Hglobals :
∀n : name p : ptr, lookupn hello_globals = Somep → lookupn ge_globalsge = Somep
Himports :
∀s : string, existsbString.eqbs hello_externals = true → lookupTAtoms ge_globalsge = None
Hs :
existsbString.eqbs hello_externals = true
⊢
lookupTAtoms ge_globalsge = None ∧ find_fnge TAtoms = None

split

2 open

ge :
genv
s :
string
Hmodule :
ge_modulege = hello_module
Hglobals :
∀n : name p : ptr, lookupn hello_globals = Somep → lookupn ge_globalsge = Somep
Himports :
∀s : string, existsbString.eqbs hello_externals = true → lookupTAtoms ge_globalsge = None
Hs :
existsbString.eqbs hello_externals = true
⊢
lookupTAtoms ge_globalsge = None
focused goal
ge :
genv
s :
string
Hmodule :
ge_modulege = hello_module
Hglobals :
∀n : name p : ptr, lookupn hello_globals = Somep → lookupn ge_globalsge = Somep
Himports :
∀s : string, existsbString.eqbs hello_externals = true → lookupTAtoms ge_globalsge = None
Hs :
existsbString.eqbs hello_externals = true
⊢
find_fnge TAtoms = None

–apply Himports

2 open

ge :
genv
s :
string
Hmodule :
ge_modulege = hello_module
Hglobals :
∀n : name p : ptr, lookupn hello_globals = Somep → lookupn ge_globalsge = Somep
Himports :
∀s : string, existsbString.eqbs hello_externals = true → lookupTAtoms ge_globalsge = None
Hs :
existsbString.eqbs hello_externals = true
⊢
existsbString.eqbs hello_externals = true
deferred goal
ge :
genv
s :
string
Hmodule :
ge_modulege = hello_module
Hglobals :
∀n : name p : ptr, lookupn hello_globals = Somep → lookupn ge_globalsge = Somep
Himports :
∀s : string, existsbString.eqbs hello_externals = true → lookupTAtoms ge_globalsge = None
Hs :
existsbString.eqbs hello_externals = true
⊢
find_fnge TAtoms = None

exact Hs

deferred goal
ge :
genv
s :
string
Hmodule :
ge_modulege = hello_module
Hglobals :
∀n : name p : ptr, lookupn hello_globals = Somep → lookupn ge_globalsge = Somep
Himports :
∀s : string, existsbString.eqbs hello_externals = true → lookupTAtoms ge_globalsge = None
Hs :
existsbString.eqbs hello_externals = true
⊢
find_fnge TAtoms = None

–apply hello_outside ; assumption

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros Hmodule Hglobals Himports Hs
split
–apply Himports
exact Hs
–apply hello_outside ; assumption