The linked module (hello_term).

The fixture decodes to hello_module.

The validatorvalidator nanofilThe validator decides whether a module is well formed and, in checked IR, whether every access is covered by evidence that still holds. Every producer of checked IR must get its output past it, and Soundness.v proves that a module it accepts never runs to unchecked. accepts the linked module: every function of the core subsetcore subset nanofilThe core subset is the part of checked filc-mode IR that the Rocq model runs and validates: the integer, pointer and proof classes, floats, check and every reuse form, the raw accesses, flight, poll edges, direct calls, check_function with raw_call, free, named locals, touch, variadics and setjmp, which is validated as ir.pl does while its step is stuck, as the interpreter refuses it. A function that uses anything else decodes to IOutside., every name unique (valid). Each object was valid alone; this is the link.

The function of the module named n, or an empty one.

The names the function f calls directly.

The names some function of md calls that md does not define, each once, in order of first call.

The 33 libc functions Hello calls: the contracts its proof needs. They are the plain entries, not the fortified ones (printf, not __printf_chk), and zmemmove is Fil-C's. The ones only quotearg calls (iswprint, mbrtoc32, __ctype_b_loc, __ctype_get_mb_cur_max, mbsinit, zmemmove, realloc) are reached only through close_stdout's diagnostic for a named file, which Hello never names.

They are exactly the calls the module leaves undefined.