An explanatory item of a module: contextFn, Records holds binding, typed-origin, value, alias and site records that say where Fn's IR came from (provenance.pl). Nothing runs it; only provenance's own check reads it (provenance:valid_contexts/1provenance.plvalid_contexts+ItemssemidetEvery context(Name, Records) of Items is for a function of Items, no two for the same one, and each record is well formed: its identity unique among records of its kind, every origin it cites defined, every hint's binding declared, and every site an instruction, phi or jump the function has. ir:valid_module/1 calls this last.).

The Rocq model does not transcribe context items: interp:run/5interp.plrun+M, +Fn, ?Args, +Fuel, ?OutcomenondetOutcome is the result of calling the function Fn of module M on Args and executing at most Fuel blocks. With unknown Args each solution constrains them to the inputs that take one path; see run_prepared/5. never reads them, and the module the gates compare has none. See also originorigin Fil-CAn origin is a static record the runtime reads to name a function and source location in a trap or backtrace (filc_amd64:function_origins//3). In context records the word means something else: a typed source node (provenance.pl)..