Compare-and-exchange, the one atomic read-modify-write term in the IR: casT reads the T at an address and, if it equals Expected, writes New there, as one sequentially consistent step. Every other atomic operation is a loop of it (c_lower:rmw//7c_lower.plrmw+U, +Addr, +Op, +V, +Ctx, -Old, -New//the atomic read-modify-write of the U at Addr, New being Old combined with the value V by Op (a binary operator, or xchg, nand, max or min): read the U, then repeat a cas of the read value for its combination until the cas finds it unchanged (ir.pl). The first read of a pointer is atomic, so the pair it combines is one; a float or double goes through its bit…).

Its checked form raw_casT, Off always keeps its own checkcheck Fil-CAn access check: check(Lo, Hi, Rights, Align) of a pointer P traps unless P's capability permits Rights on [P+Lo, P+Hi) with P+Lo Align-aligned, and otherwise yields P as a proof of class a. check_local does the same for a named local, and check_function yields a function proof of class f (ir:op_kind/2, pizlonate:checked_access/4)., and every cas ends every live factlive fact nanofilA live fact live(Q, P, Lo, Hi, Rights, Align) is the validator's record that the proof Q came from a check of P over [Lo, Hi) that still holds: no safepoint since, and neither Q nor P redefined. A later raw access through Q that the fact covers needs no check of its own.. For p it compares addresses only, so a New may replace a pointer of another 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., as Fil-C's filc_strong_cas_ptr does. Atomics are 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.: the Rocq model has no cas.