← all exploratory attempts · paired baseline · show in source

breadth-12: Inactive memory lanes

Agent report: partial Review pending

Session: completed

docs/spec-fabric-mem.md, lines 432–436

Dynamic-mask admission has one invariant meaning: inactive addresses are not evaluated, inactive operations are suppressed, inactive load-like result lanes are zero-filled, and an all-zero mask completes without a service request. There is no independent `all_zero_mask_completes` field: a dynamic mask class that cannot provide this invariant must not be declared.

Execution provenance

The original pilot recorded the compiler hash and checkout revision separately; its binary build revision was not verified. Coverage follow-ups use separately identified rebuilt binaries. Original simulator binary hashes were not retained.

Original standalone-test agent report

This is exploratory evidence, not an accepted production-format PBT.

Three of the four behavioral clauses plus the completion half of the fourth are exercised against the real runtime; the 'without a service request' observable and the declaration-side clause have no reachable interface at this revision.

Reported numeric verdicts

all zero mask cases

31

Tested obligations

• O1 inactive addresses are not evaluated (out-of-range/duplicated addresses on inactive lanes do not refuse or collide)
• O2 inactive operations are suppressed (masked store leaves non-active memory bytes identical)
• O3 inactive load-like result lanes are zero-filled (active lanes equal mem[addr], inactive lanes equal 0)
• O4a all-zero mask completes (status pass, all-zero result, memory unchanged)

Untested obligations

• O4b 'without a service request' - no service-beat/transaction observable in the DFG simulation report; operation_fire_counts is an op firing count, not a service request
• Declaration-side clause: 'no independent all_zero_mask_completes field; a dynamic mask class that cannot provide this invariant must not be declared' - MaskInactivePair / MemoryAccessClass::create are C++-only APIs (include/Fabric/IR/MemoryCapabilityDomains.h) with no MLIR attribute or CLI surface at this revision
• Suppress vs SuppressAndZeroFill selection per access form, atomic / compare-exchange actors, PointerAddressed address form, ranked (multi-dim) mask geometry, non-i8 element widths

Format

Reproduction

Measured subject code coverage

blocked · The pinned subject target cannot be rebuilt with the available Clang 21 or Clang 24 / libstdc++13 toolchains: CgraClosedWaitSetDiagnostic has an implicitly deleted std::variant default constructor. Both simulator and pre-mapping targets depend on this code. No subject source was changed; original uninstrumented runs remain available, with their build revision unverified.

Coverage-preserving minimized cases: not measured

Published evidence