A module's mode is plain or filc: filc if it uses anything Fil-C-specific (a p, a call to an external function, ...), plain otherwise, read off its contents (ir:module_mode/2ir.plmodule_mode+M, -ModedetMode is filc when anything in M has class p, uses a pointer-only op, or calls a function M does not define (which only the Fil-C ABI can reach), and plain otherwise.).

Plain mode is C without capabilities: an access outside every live allocation is ub, not a traptrap Fil-CA trap is a Fil-C check failing, which upstream calls a Fil-C panic or safety error (filc_safety_panic): the run ends trap(Reason), terminal and uncatchable. Because nothing follows it, a check is a pure assertion, which is why a check proved never to fail can be deleted without changing behaviour.. The Rocq model covers filc mode only; plain mode is outside 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..