← all exploratory attempts · paired baseline · show in source

breadth-18: Shared operation admission

Agent report: partial Review pending

Session: completed

docs/spec-fabric-hw-share-group.md, lines 102–105

Graph admission, simulator dispatch, and Fabric matching must all resolve the same registered `OperationSchemaId`. An HSG descriptor may narrow where a schema can be physically shared, but it cannot make an unregistered actor canonical or reinterpret the schema's semantic projection.

Independent review

No independent interface audit has been supplied for this attempt.

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

Untested obligations

Format

standalone Python generator + Python output assertions (no ProGRMR grammar / .spct checker)

Reproduction

not measured

Measured subject code coverage

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

Coverage-preserving minimized cases: not measured

Full structured agent result
artifacts
cases
cases/ (100 seeded cases + case_cv.mlir), cases/manifest.json
checker
check.py
generator
generate.py
intent note
INTENT.md
raw subject output
evidence/raw_runs.txt
runner
reproduce.sh (single command) / payload.sh (generated remote script)
verdicts
evidence/verdicts.json
controlled violation
case
cases/case_cv.mlir
construction
a documented-admitted positive (@llvm.intr.ssub.sat under ScalarIntegerSaturatingAddSub) labelled with expect=reject
nature
synthetic checker test, not a subject defect
observed
subject rc=0 (admitted), harness verdict = fail
shows
the assertions can report a violation when subject behaviour and the documented obligation disagree
coverage
omitted - no coverage instrumentation was accessible for the remote pinned binary within the 20-minute budget; the budget was spent making the PBT exercise the real subject
format
standalone Python generator + Python output assertions (no ProGRMR grammar / .spct checker)
format reason
The property is a whole-op admission relation between the implementation_family attribute and every op_list symbol of the same fabric.op, evaluated against a documented family/member table and observed through the subject's verifier exit code and diagnostic. The .spct postcondition checker consumes input/output generic MLIR pairs and has no projection for a rejected run's diagnostic, so a standalone generator plus assertions on the real subject's return code and diagnostic was used.
notes
  • All remote execution pinned with taskset -c 79; scratch on bibim at /tmp/spectriad-autonomous-breadth-18.
  • Because O3 and the simulator-dispatch/graph-admission consumers are untested, this is a partial PBT for the passage, not whole-passage success.
passage
docs/spec-fabric-hw-share-group.md:102-105
pinned revision
48615bc5925ef4b9db8b4550b5d4322933cf4b7b
potential subject bug
not measured
sampling
bounds are conventions
bit widths {8,16,32,64}, hw_params={integer_widths=[W:i32]}, op_list size 1..|family|, unregistered-name pool - harness conventions, not source requirements
families sampled
ScalarIntegerAddSub
18
ScalarIntegerCountZeros
9
ScalarIntegerLogic
21
ScalarIntegerMultiply
21
ScalarIntegerSaturatingAddSub
23
ScalarIntegerShift
9
seed range
0..99 (python random.Random(seed)), plus one controlled-violation case
seeds
100
slot
breadth-18
source references
family member table
docs/spec-fabric-hw-share-group.md:132-147
member qualifications
docs/spec-fabric-hw-share-group.md:~112-170 (optional llvm.getelementptr; disjoint llvm.or; poison-flagged ctlz/cttz)
obligation
docs/spec-fabric-hw-share-group.md:102-105
status
partial
subject
binary
/home/blimpan/blimpan/spectriad-loom-head/loom/build/tools/loom/loom (bibim)
command
taskset -c 79 loom <case>.mlir
interface evidence
  • include/Fabric/IR/FabricOps.td: Fabric_OpOp (op_list, implementation_family, hw_params)
  • lib/Fabric/IR/FabricPrimitiveOps.cpp: OpOp::verify
  • test/fabric/unit/op/valid.mlir (attribute syntax only)
semantics
exit 0 = parsed and verified (admitted); exit 1 = verifier rejection with diagnostic
tested obligations
  • O1: an op_list naming an actor that is not a registered canonical operation schema is rejected (HSG occurrence cannot make an unregistered actor canonical) - 22 cases
  • O2a: a documented-admitted op_list subset (legitimate narrowing) is admitted - 53 cases
  • O2b: a registered schema not admitted by the declared ImplementationFamilyId is rejected (no widening/reinterpretation of admission) - 25 cases
untested obligations
  • O3: 'reinterpret the schema's semantic projection' (operand/result types, arity, flags) is not exercised
  • O4: cross-consumer agreement for simulator dispatch and graph admission - only the Fabric-side fabric.op admission verifier was exercised; no simulator dispatch API was run, and parsing would not be valid evidence for it
  • Qualified members: optional llvm.getelementptr, disjoint llvm.or, poison-flagged llvm.intr.ctlz/cttz
  • Float, cast, select, bitcast, conversion, multiply-float, FMA, loop/dataflow and fixed-vector families
verdict counts
P1 positive pass
53
P2 unregistered reject pass
22
P3 not admitted reject pass
25
controlled violation fail
1
fail
0
invalid
0

Published evidence

evidence/breadth-18 (7)
  • INTENT.md
    evidence/breadth-18/INTENT.md (3359 bytes)
  • README.md
    evidence/breadth-18/README.md (2623 bytes)
  • RESULT.json
    evidence/breadth-18/RESULT.json (4756 bytes)
  • check.py
    evidence/breadth-18/check.py (3300 bytes)
  • generate.py
    evidence/breadth-18/generate.py (6433 bytes)
  • payload.sh
    evidence/breadth-18/payload.sh (8698 bytes)
  • reproduce.sh
    evidence/breadth-18/reproduce.sh (721 bytes)
evidence/breadth-18/cases (102)
evidence/breadth-18/coverage (2)
evidence/breadth-18/evidence (3)
  • raw_runs.err
    evidence/breadth-18/evidence/raw_runs.err (82 bytes)
  • raw_runs.txt
    evidence/breadth-18/evidence/raw_runs.txt (63668 bytes)
  • verdicts.json
    evidence/breadth-18/evidence/verdicts.json (94073 bytes)