← all exploratory attempts · paired baseline · show in source

breadth-01: PE input/output bounds

Agent report: partial Reviewed: partial proxy

Session: completed

docs/spec-fabric-pe.md, lines 257–264

### Implicit (derived from the FU set) `max_fu_inputs` -- the maximum, across the concrete FU occurrence set, of each FU's input-port count. If FU `f0` has 2 inputs and FU `f1` has 3 inputs, `max_fu_inputs = 3`. `max_fu_outputs` -- the maximum, across the concrete FU occurrence set, of each FU's output-port count. Same shape.

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.

Maximum-semantics of max_fu_inputs/max_fu_outputs verified through the real verifier bound; ConcreteFuOccurrenceSet membership clauses (named declarations / instantiate elaboration) untested.

Reported numeric verdicts

verdicts

documented oracle max

PASS

100

subject exit codes

0

54

nonzero

46

Tested obligations

• max over the concrete FU occurrence set of input-port counts governs acceptance against K (maximum, not first/last/sum/min)
• max over the concrete FU occurrence set of output-port counts governs acceptance against L
• on violation the diagnostic reports a real FU port count that exceeds the bound and the bound value equals the PE's operand/result count

Untested obligations

• exclusion of named FU declarations from the ConcreteFuOccurrenceSet
• instantiate -> anonymous-occurrence canonical elaboration
• direct readout of the max_fu_inputs/max_fu_outputs values (no interface exists: no max_fu/maxFu symbol in include/, lib/, tools/ at the pinned revision)
• typed configuration-field domain sentence (:266-269)

Format

checker

artifacts/check_property.py

chosen

standalone Python generator + output/diagnostic assertions

generator

artifacts/gen_pe.py (+ make_inputs.py)

reason

The derived parameters are not materialised in any IR field, so the property is an accept/reject + diagnostic property over whole modules rather than an input/output op relation; the .spct checker compares generic-form input/output pairs and cannot express verifier rejection.

reproduce

artifacts/run_all.sh

runner

artifacts/run_subject.sh

Reproduction

Measured subject code coverage

measured · Measured handwritten Loom subject code only; external LLVM/MLIR and generated code excluded. Includes main executions, including rejected inputs; deliberate controls excluded. No matching native-suite baseline for this executable has been imported, so no coverage gain is claimed. Semantic fidelity remains a separate audit.

Execution: {'subject_exit_codes': {'0': 54, '1': 46}, 'subject_invocations': 100}
Baseline: No matching baseline measured
Minimized cases: not measured

Published evidence