An inline asm statement of one fixed-register instruction: asm_fixedM, Ins, Outs runs M (cpuid, xgetbv, rdtsc, rdtscp, or the operand-free lfence, sfence and pause) on w inputs in the registers M reads, defining w temporaries from the registers it writes (ir:asm_fixed_regs/3ir.plasm_fixed_regs?M, ?Reads, ?WritesnondetThe fixed-register instructions asm_fixed may name (docs/asm-fixed.md), with the registers each reads and writes (a, b, c, d: rax to rdx, of which only the low 32 bits are read; every write is 32 bits and zero-extends). mfence is the fence instruction., asm-fixed.md).

Other inline asm is a blank-template barrier (its operands are evaluated, nothing else), a call to zsafety_error where filcc would refuse it at run time, or refused. The interpreterinterpreter nanofilThe interpreter is interp.pl, nanofil's executable meaning of the IR: a relation from a module, a function, arguments and fuel to an outcome, with CLP(Z) integers so that it runs in every direction. The Rocq model transcribes it, and the outcome gate checks that the two agree on every run line of the corpus. stops at unknownasmM, Xs, since only the machine knows the results; it 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..