v0.9 atomic matrix

<!-- @generated by wync/tools/atomic-matrix.mjs from design/atomic-matrix.json; do not edit -->

Atomic storage is spelled atomic<T>, its address is @atomic<T>, and its sole constructor is atomic<T>(value). Storage is opaque, non-copyable, exactly the size and natural alignment of T, and has no hidden bytes. Construction is a direct storage-initialization event, not an atomic access effect. Static construction emits bytes and relocations without startup code; runtime construction establishes the location's initial modification-order value. That initial write is the first member of the location's modification order and happens-before every later atomic event on the location; construction itself is not an SC event.

The sole raw construction path is address<@atomic<T>>(raw), admitted only in the executable-function-body context. It accepts u64-or-representable-untyped-integer, preserves the address bits, and performs no memory event or runtime check. It is a programmer_asserted trust boundary under contract wyst.atomicRawAddress.v1, asserting that the raw address denotes exact atomic<T> storage with natural element alignment, atomic-capable Normal memory, and no mixed atomic/plain access. Provable misalignment and a known Device-memory mapping are compile-time errors. No implicit conversion, relensing into atomic storage, reverse exposure as an ordinary/raw address, or const-context assertion is permitted.

The closed element classes are Boolean (bool), integer (u8, u16, u32, u64, i8, i16, i32, i64), and one-target-word address values, including @atomic<U>. Address elements preserve their pointee intent; atomic storage itself may not be volatile- or MMIO-qualified. Every access requires atomic-capable Normal memory and the natural alignment of its exact 1-, 2-, 4-, 8-byte, or target-word width. Device/MMIO, under-aligned, and mixed atomic/plain access are rejected.

# Methods

Method	Elements	Value operands	Orders	Result	Typed IR operation	Progress
.load	boolean, integer, address	none	.relaxed, .acquire, .seq_cst	element	load	lock-free-single-access
.store	boolean, integer, address	desired:T	.relaxed, .release, .seq_cst	void	store	lock-free-single-access
.exchange	boolean, integer, address	desired:T	.relaxed, .acquire, .release, .acq_rel, .seq_cst	element	exchange	lock-free-retry-until-success
.compare_exchange	boolean, integer, address	expected:T, desired:T	.relaxed, .acquire, .release, .acq_rel, .seq_cst	(observed:T, exchanged:bool)	compare-exchange	lock-free-strong-retry-until-success-or-mismatch
.fetch_add	integer	operand:T	.relaxed, .acquire, .release, .acq_rel, .seq_cst	element	fetch-add	lock-free-retry-until-success
.fetch_sub	integer	operand:T	.relaxed, .acquire, .release, .acq_rel, .seq_cst	element	fetch-sub	lock-free-retry-until-success
.fetch_and	integer	operand:T	.relaxed, .acquire, .release, .acq_rel, .seq_cst	element	fetch-and	lock-free-retry-until-success
.fetch_or	integer	operand:T	.relaxed, .acquire, .release, .acq_rel, .seq_cst	element	fetch-or	lock-free-retry-until-success
.fetch_xor	integer	operand:T	.relaxed, .acquire, .release, .acq_rel, .seq_cst	element	fetch-xor	lock-free-retry-until-success
.test_and_set_bit	integer	bit:const-u32-in-range	.relaxed, .acquire, .release, .acq_rel, .seq_cst	bool	test-and-set-bit	lock-free-retry-until-success
.test_and_clear_bit	integer	bit:const-u32-in-range	.relaxed, .acquire, .release, .acq_rel, .seq_cst	bool	test-and-clear-bit	lock-free-retry-until-success

# Compare-exchange and ARM64 order policy

compare_exchange has strong strength and uses exact-width-value-equality. Its result is (observed: T, exchanged: bool); the failure column below is the ordering of the failed comparison/read. A successful comparison writes desired and returns observed-and-true. A mismatch writes none, returns observed-and-false, and its LL/SC path executes clrex. Store-exclusive failure writes none, produces none, and takes retry-while-comparison-remains-eligible.

Order	Successful exchange	Failed read	LL/SC load	LL/SC store	LSE suffix
.relaxed	relaxed-rmw	relaxed-load	ldxr	stxr	(none)
.acquire	acquire-rmw	acquire-load	ldaxr	stxr	a
.release	release-rmw	relaxed-load	ldxr	stlxr	l
.acq_rel	acquire-release-rmw	acquire-load	ldaxr	stlxr	al
.seq_cst	sequentially-consistent-rmw	sequentially-consistent-load	ldaxr	stlxr	al

Sequentially consistent loads use acquire loads, stores use release stores, and RMW operations use acquire-release forms; no implicit dmb is emitted. This mapping remains subject to Chapter 9's ARM64 architecture proof and normative store-buffering, load-buffering, and IRIW litmus obligations; matching mnemonics alone is not proof of the global SC order. The generated LL/SC retry policy is unbounded-retry-until-store-exclusive-success, and unsupported target capability uses hard-target-capability-error. The ARM64 implementation contract records exact-width lowering as enabled, lock-free lowering as enabled, fallback locks as forbidden, fallback helpers as forbidden, allocation as forbidden, a retry budget of none, a timeout of none, synthetic failure as forbidden, and per-agent wait-freedom as forbidden.

Bytes	Plain load	Acquire/SC load	Plain store	Release/SC store	Signed result reconstruction
1	ldrb	ldarb	strb	stlrb	sxtb
2	ldrh	ldarh	strh	stlrh	sxth
4	ldr-w	ldar-w	str-w	stlr-w	sxtw
8	ldr-x	ldar-x	str-x	stlr-x	none

The RMW LSE families and LL/SC updates are the method rows in the normative JSON source. Pair-atomic/exclusive catalog rows remain separate checked 16-byte operations and do not add a atomic<T> element, widen @atomic<u64> to 16 bytes, or authorize aggregate atomic storage.

Legacy hash-directive dispositions are owned only by the item 54 non-parser release-audit manifest. Every migrated address must explicitly have type @atomic<T>; a pair-atomic row cannot claim scalar atomic<u64> storage.