← all exploratory attempts · paired baseline · show in source

breadth-13: Fabric module contents

Agent report: partial Review pending

Session: completed

docs/spec-fabric-module.md, lines 147–169

## Body whitelist `fabric.module` body may contain only: * `fabric.pe` (both `[spatial]` and `[temporal]`) * `fabric.switch` (both `[spatial]` and `[temporal]`; see `docs/spec-fabric-switch.md`) * `fabric.mem` (an optional `[spatial]` or `[temporal]` Operation Engine, an optional Local Memory Service, or both; see `docs/spec-fabric-mem.md`) * `fabric.fifo` (see `docs/spec-fabric-fifo.md`) * nested named `fabric.module` template declarations; sibling top-level declarations remain in their enclosing symbol table rather than the body * `fabric.instantiate` (binds a previously-defined fabric symbol into this scope; see `docs/spec-fabric-instantiate.md`) * `fabric.boundary` (single op covering all three boundary directions -- `[s2t]`, `[t2t]`, `[t2s]` -- between the spatial `bits` domain and the temporal `bits_tag` domain; see `docs/spec-fabric-boundary.md`) * `fabric.yield` (terminator) `builtin.unrealized_conversion_cast` is **not** in the whitelist. All fabric module values must come from a real fabric producer (a sub- module result) or from the module's entry-block arguments.

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.

No author explanation recorded.

Reported numeric verdicts

not measured

Tested obligations

• fabric.fifo permitted in body
• fabric.switch [spatial] permitted in body
• fabric.boundary [s2t] permitted in body
• nested named fabric.module declaration permitted in body
• fabric.yield terminator permitted / implicit
• builtin.unrealized_conversion_cast NOT in whitelist (explicit passage clause)
• arbitrary non-fabric ops rejected: arith.constant, arith.addi, arith.muli, memref.alloc, func.call, func.func
• non-whitelisted fabric op rejected: fabric.system

Untested obligations

• fabric.pe [spatial]/[temporal] as body member (requires inner fabric.fu or fabric.instantiate; out of budget)
• fabric.mem (operation engine, local memory service, both)
• fabric.instantiate (zero-arg form blocked by unrelated non-empty domain-slot-bindings rule)
• fabric.switch [temporal]
• fabric.boundary [t2t] and [t2s]
• sibling top-level declarations remain in enclosing symbol table clause
• value-provenance sentence beyond the cast prohibition

Format

chosen

standalone Python generator + exit-code/diagnostic oracle

progrmr spct used

false

reason

the negative half of the property is expected rejection: the subject emits a diagnostic and no output IR, so there is no OUTPUT.generic.mlir for spectriad-check to evaluate; the verdict lives in returncode/diagnostic

Reproduction

Measured subject code coverage

pending · Instrumented coverage follow-up in progress; original pilot did not collect profiles.

Coverage-preserving minimized cases: not measured

Published evidence