README.md

evidence/breadth-13/README.md
# PBT: `fabric.module` body whitelist (docs/spec-fabric-module.md:147-169)

## Single reproduction command

```bash
cd /home/blimpan/projects/spectriad/rework-fresh/project-data/loom/48615bc5925ef4b9db8b4550b5d4322933cf4b7b/experiments/breadth-autonomous-v1/slots/breadth-13 && ./run.sh 100
```

`run.sh` regenerates the 100 seeded cases, runs each through the pinned subject on
bibim (`ssh bibim 'taskset -c 79 .../loom --mlir-print-op-generic'`), stores
stdout/stderr/returncode per seed under `runs/`, and prints the verdict tally.
The `ssh` step needs the Bash-tool sandbox escape for `ssh bibim ...` (the sandbox
hides `~/.ssh/config`).

## Intent note (source-grounded)

Pinned source: `docs/spec-fabric-module.md:147-169` (revision
48615bc5925ef4b9db8b4550b5d4322933cf4b7b).

Obligation as read: a `fabric.module` body **may contain only** `fabric.pe`,
`fabric.switch`, `fabric.mem`, `fabric.fifo`, nested named `fabric.module`
declarations, `fabric.instantiate`, `fabric.boundary`, and the `fabric.yield`
terminator. Any other operation -- explicitly including
`builtin.unrealized_conversion_cast` -- is outside the whitelist and must not be
accepted inside the body.

Property tested (two directions):

1. **Positive:** a body built only from whitelisted ops that is otherwise
   well-formed must be accepted (`returncode == 0`).
2. **Negative:** the same body plus one non-whitelisted op must be rejected
   (`returncode != 0`) with a diagnostic saying that op `is not allowed inside
   fabric.module`.

Interpretation changes during the session: none to the obligation. Two *test
scaffolding* changes were needed, both to keep failures on-property:
`fabric.fu` and `fabric.link` were dropped from the non-whitelisted pool
(`fabric.fu` needs a region in its custom syntax and `fabric.link` is not a
registered op in this build, so both produced *parse* errors rather than the
whitelist verdict -- an invalid test, not a property signal); and generated
bodies were changed to consume each entry-block argument at most once, because
an unrelated `fabric.module` rule ("transport source is used by more than one
consumer") otherwise rejected valid positive cases.

Sampling bounds/conventions (NOT source requirements): 100 seeds, 1-4
entry-block arguments, bit widths from {1,4,8,16,32,64}, 0-3 whitelisted body
ops, FIFO `max_depth` from {1,2,4,8,16}, `bypassable` in {true,false},
`fabric.switch [spatial]` with uniform port type and 1-2 results,
`fabric.boundary [s2t]` only, `~50%` negative cases.

## Chosen format

Standalone Python generator + exit-code/diagnostic oracle (not ProGRMR +
`.spct`). Reason: the property's negative half is *expected rejection* -- the
subject emits a diagnostic and no output IR, so there is no
`OUTPUT.generic.mlir` for `spectriad-check` to inspect. The verdict lives in the
returncode and diagnostic text, which the postcondition checker cannot observe.
The positive half is exercised through the real subject as well (accepted IR is
printed in generic form under `runs/*.stdout`).

## Files

- `gen.py` -- seeded generator (`gen.py N DIR`), writes `cases/seed_NNNN.mlir` + `cases/manifest.json`.
- `judge.py` -- oracle (`judge.py cases runs`), writes `verdicts.json`.
- `run.sh` -- generate + execute subject + judge.
- `cases/`, `runs/` -- generated inputs and captured subject stdout/stderr/returncode per seed.
- `verdicts.json`, `summary.json` -- per-seed verdicts and tallies.
- `controlled-violation/` -- synthetic mutated expectations plus their verdicts.
- `work/probe/` -- syntax probes used to confirm which whitelisted body ops verify standalone.
- `RESULT.json` -- machine-readable summary.

## Evidence

100/100 seeds `pass`, 0 violations, 0 invalid runs. 41 positive, 59 negative
cases across 7 distinct non-whitelisted ops
(`builtin.unrealized_conversion_cast`, `arith.constant`, `arith.addi`,
`arith.muli`, `memref.alloc`, `func.call`, `func.func`, `fabric.system`).
Representative subject diagnostic (seed with the cast):

```
<stdin>:3:5: error: 'builtin.unrealized_conversion_cast' op is not allowed inside fabric.module; only fabric.pe, fabric.switch, fabric.mem, fabric.fifo, fabric.module, fabric.instantiate, and fabric.boundary are permitted (plus the implicit terminator fabric.yield)
```

Controlled violation (synthetic, checker-side only -- **not** a subject defect):
`controlled-violation/` re-judges two already-executed real runs with inverted
expectations (one all-whitelisted body declared "must reject", one
cast-bearing body declared "must accept"); the oracle reports
`{"pass": 0, "violation": 2}`, showing the property can fail.

## Untested clauses of the passage

- `fabric.pe` `[spatial]`/`[temporal]` as a body member: a `fabric.pe` requires
  at least one inner `fabric.fu` or `fabric.instantiate`, which was out of
  budget to generate correctly.
- `fabric.mem` (`[spatial]`/`[temporal]` engine, Local Memory Service, both).
- `fabric.instantiate`: the zero-argument form is rejected for an unrelated
  reason ("targeting a Module requires non-empty domain-slot bindings"), so a
  valid instance edge was not built in budget.
- `fabric.switch [temporal]`, `fabric.boundary [t2t]`/`[t2s]`.
- The sibling-symbol-table clause ("sibling top-level declarations remain in
  their enclosing symbol table rather than the body").
- The value-provenance sentence ("all fabric module values must come from a real
  fabric producer ... or entry-block arguments") beyond the cast prohibition.

Coverage / minimization: omitted deliberately; no coverage instrumentation was
readily available for the remote binary and the budget went to making the PBT
exercise the real subject.