A PBT without violations is consistent with the inputs it was sampled on. It is not evidence that the translation from the document is accurate or complete, and confidence is an estimated residual risk over the run's own partitions, not a reliability bound.
mlir-stage-pbt-v119PBTs1with violations15/19with a confidence estimate
| PBT | document | latest run | checked pairs | confidence | added code coverage |
|---|---|---|---|---|---|
mlir-stage-01-v1--loom-llvm-arith-to-arith“The poison-flagged forms retain their LLVM spelling and project that flag through the registered typed semantic case; the standar…” | spec-compiler-part-2-scf.md | passing 5000/5000 | 5000/5000checker passes | 54.9%estimated | +0lines+0branches |
mlir-stage-02-v1--loom-lower-for-to-graph“`dataflow.graph.launch` is the SpatialCore execution boundary inside a `dataflow.thread` definition's body. It references a `data…” | spec-compiler-part-3-dfg.md | passing 5000/5000 | 5000/5000checker passes | 99.5%estimated | +0lines+0branches |
mlir-stage-04-v1--loom-lower-for-to-graph“`dataflow.graph` is the SpatialCore leaf DFG **definition** (Symbol-bearing, module-scope, function-like). Its body cannot contai…” | spec-compiler-part-3-dfg.md | passing 824/1000 | 824/824checker passes | not estimated | +0lines+1branches |
mlir-stage-05-v1--loom-materialize-fmuladd=shape=fused“Each child preserves the exact floating type, fast-math contract, source location, Ownership lineage, and source-provenance proje…” | spec-compiler-part-2-scf.md | passing 1000/1000 | 1000/1000checker passes | not estimated | +3lines+3branches |
mlir-stage-06-v1--loom-lower-scf-to-dfg“Output is an initial Canonical Dataflow Program: module-level `llvm.func` symbols for imported LLVM callables, any genuinely nati…” | spec-compiler-part-3-dfg.md | passing 964/1000 | 964/964checker passes | not estimated | +56lines+49branches |
mlir-stage-07-v1--loom-lower-for-to-graph“The target Part 3 dataflow surface uses module-scope, Symbol-bearing, function-like definitions for both `dataflow.thread` and `d…” | spec-compiler-part-3-dfg.md | passing 5000/5000 | 5000/5000checker passes | 99.7%estimated | +0lines+0branches |
mlir-stage-08-v1--loom-lower-graph-memory“In addition to alias hazards, lowering materializes the sequenced-before rules from the actor contracts: * atomic actors and fenc…” | spec-compiler-part-3-mem.md | 97 violation(s) | 903/1000checker passes97violations | not estimated | +23lines+18branches |
mlir-stage-09-v1--loom-lower-scf-to-dfg“The Structured Transfer Algebra defines graph-owned parallel composition only after the Structured Program Candidate has material…” | spec-compiler-part-3-dfg.md | passing 5000/5000 | 5000/5000checker passes | 78.7%estimated | +6lines+8branches |
mlir-stage-10-v1--loom-lower-for-to-graph“The wrap is mandatory output, not an optimization, and is verified by the front-end's standard verifier rules in Section 9.” | spec-compiler-part-3-dfg.md | passing 5000/5000 | 5000/5000checker passes | 88.1%estimated | +0lines+0branches |
mlir-stage-11-v1--loom-lower-graph-memory“One vector addressed memory actor is one canonical firing. Its active lanes do not create independent frontier records or an impl…” | spec-compiler-part-3-mem.md | passing 5000/5000 | 5000/5000checker passes | 56.2%estimated | +147lines+71branches |
mlir-stage-12-v1--loom-lower-forall-to-thread“`function_type` is a `FunctionType` whose inputs are the kernel's user-data operand types `(T0, ..., TN)` and whose results are e…” | spec-compiler-part-3-dfg.md | passing 5000/5000 | 5000/5000checker passes | 63.2%estimated | +57lines+38branches |
mlir-stage-13-v1--loom-lower-graph-memory“LLVM memcpy, memmove, and memset intrinsics are expanded into their exact structured loop semantics before ownership selection. S…” | spec-compiler-part-3-mem.md | passing 5000/5000 | 5000/5000checker passes | 27.4%estimated | +68lines+46branches |
mlir-stage-14-v1--loom-lift-cf-to-scf“The whole callable is the preferred exact CFG-to-SCF projection. When a local obstacle makes that projection inadmissible, raisin…” | spec-compiler-part-2-scf.md | passing 5000/5000 | 5000/5000checker passes | 94.9%estimated | +0lines+0branches |
mlir-stage-15-v1--loom-materialize-fmuladd=shape=fused“After materialization, no `fmuladd` operation may remain in a finalizable Sn or be registered as a Canonical Dataflow actor.” | spec-compiler-part-2-scf.md | passing 5000/5000 | 5000/5000checker passes | 55.4%estimated | +1lines+7branches |
mlir-stage-16-v1--loom-lower-graph-memory“Memory exports preserve an imported root or view, or expose a fresh allocation root. Every export retains a memref result payload.” | spec-compiler-part-3-mem.md | passing 5000/5000 | 5000/5000checker passes | 99.6%estimated | +15lines+8branches |
mlir-stage-19-v1--loom-lower-forall-to-thread“The first `N` block arguments mirror `function_type.inputs` exactly (each user body operand). Putting the signature args first pr…” | spec-compiler-part-3-dfg.md | passing 5000/5000 | 5000/5000checker passes | 91.1%estimated | +42lines+25branches |
mlir-stage-21-v1--loom-lower-graph-memory“No dependence is removed because a loop appears parallelizable. Source iteration order remains authoritative until an earlier tra…” | spec-compiler-part-3-mem.md | passing 5000/5000 | 5000/5000checker passes | 91.9%estimated | +11lines+2branches |
mlir-stage-25-v1--loom-materialize-fmuladd=shape=split“No unresolved parent, mixed Fused/Split child, hidden backend default, or target-code-generation choice may cross the ExecutionSh…” | spec-compiler-part-2-scf.md | passing 5000/5000 | 5000/5000checker passes | 90.8%estimated | +1lines+1branches |
mlir-stage-29-v1--loom-lower-graph-memory“After recursively lowering before: * false-lane execution is `E_out`; * `dataflow.gate` projects before execution into after phas…” | spec-compiler-part-3-mem.md | passing 5000/5000 | 5000/5000checker passes | 100.0%estimated | +0lines+0branches |