The global environment is what every stepstep nanofilA step moves a configuration on by one thing: entering a block (its phis, one unit of fuel), one instruction, or one jump. step answers Next with the next configuration, Done with an outcome, Fresh for an allocation that waits for a base, or Stuck. of a run reads but never changes: the module, each global's pointer, and the free that a call of libc's free runs.
Semantics.v's genv: ge_module, ge_globals (each symbol's name with its address and capabilitycapability Fil-CA capability is the authority half of a Fil-C pointer: which object, if any, its address may be used to access. In the model a capability is an identity, never bounds; the object's current bounds live in its region, so freeing through one alias empties what every alias sees.), ge_free. Run.v's Driver builds it with ge_free the runtimeruntime Fil-CThe runtime is what Fil-C does around one thread's program, natively libpizlo.so with FUGC: where a new object goes, what free does, and what the collector may change while the program waits at a safepoint. The model does not define it; it states it as one page of axioms, Module Type Runtime (Runtime), each with a native test in tests/c/prog/axiom-*.c.'s free; the interpreter's is Memory.v's free_res.
interp.pl's counterpart is the prepared module of interp:module_prepared/2interp.plmodule_prepared+M, -PrepareddetPrepared is M ready to run: its mode, the address of each global, its initial memory, and its functions and their blocks indexed by name and label. The initial memory holds integers only, so runs can share it., its function and global indexes; its free is interp:free_res/4interp.plfree_res+P, +Mem0, -Res, -Memthe pinned runtime's free_with_checks, object_for_deallocate and free_impl, for objects this interpreter owns. ext(_) has a placeholder address, not a known zero; it stays unsupported. Public run/5 also accepts integer p arguments: these have no capability..
find_fn looks a callee up in it, through aliases.
The subtlety: the theorems ask ge_free ge = R.free and ge_module ge = md explicitly, because a genv could pair a module with any free; valid_no_unchecked is stated for the genv a run of R would build.
Defined in Semantics.v.