fp: exploit the declared fast relaxation with one horizontal schedule

Every f32 call site that writes contract=fast has, until now, been
declaring a relaxation nothing exploited: the lowering kept the same
ordered fused chain the fma contract pins. The new
vectorize-ondsp-fp-fast-memref-reduce pass is that relaxation's one
consumer. It splits a rank-1 fast reduction into eight-lane fused
partial sums, one cross-lane vector reduction, and a scalar tail,
with every floating-point operation carrying exactly the declared
fastmath<reassoc,contract> profile. off and fma are refused - the
exact inverse of the order-preserving batching pass, whose lanes may
never regroup one output's chain. The rewrite reorders reads only
and produces one scalar, so unlike both batching passes it carries
no aliasing obligation. It runs inside the canonical schedule stage:
the per-call-site contract is the opt-in, and the standalone flag
remains the ablation interface. One MLIR 17 fact is recorded at the
emission site: vector.reduction has no fastmath attribute at this
version, so the cross-lane fold is the ordered reduce.fadd intrinsic
- a fixed deterministic regrouping the relaxation authorizes.

A relaxed result is never bit-pinned, so the object gate carries a
different evidence shape than every exact-contract gate before it:
an error envelope against an f64 reference (4*N*2^-24 * sum of
absolute products), repeated-call determinism, a structural pin that
the vector form was emitted before any object is built, and two
mechanism-directed executed divergences from the ordered fused chain
- an unfused-product rounding tie the vector body resolves down and
the ordered chain rounds up, and a cross-lane cancellation the
ordered chain absorbs - each with its observed bit patterns recorded
and each verified live by mutation. A naive period-aligned
cancellation corpus does NOT diverge under the ordered cross-lane
fold; a divergence corpus counts as a witness only once it is
executed and observed to diverge.

Author: Chennesxu

docs/status.md

@@ -12,7 +12,7 @@ the numeric model is stabilized.
 | `ondrix`, `ondsp`, and `ortumcore` dialects | Implemented; contracts remain experimental |
 | Typed conversion patterns and accumulator type conversion | Implemented |
 | Generic scalar lowering | Signed-Q15 full product with signed frac30 accumulator widths of at least 32 bits and signed-Q31 full/raw-high accumulator operations implemented; ordered rank-1 Q15/Q31 memref reductions implemented; from a supported signed frac30 accumulator the export boundary lowers a signed Q15 destination, any signed i32 destination fraction the verifier admits, and the identity signed i64/frac30 reading, while the i64/frac62 profile remains restricted to signed Q31 export; every export is a value-preserving format conversion, and value-changing scalings belong to the declared arithmetic `round_shift`; rank-1 f32 reduction is partial |
-| Floating-point contract policy | Every f32 call site names one of three declared evaluation policies, and the policy indexes the correctness relation its evidence must establish: `off` keeps separate ordered IEEE multiplies and adds (no fast-math flags, not even contraction) and `fma` pins explicit single-rounding fused multiply-add events (`math.fma`/`llvm.fma`) — both are exact contracts gated bit-for-bit against independent references; `fast` is a named relaxation profile declaring exactly reassociation plus multiply-add contraction (`fastmath<reassoc,contract>`, never LLVM's blanket `fast`, which would additionally assert NaN/Inf absence, abandon signed-zero observability, and license reciprocal division and approximate functions the language never declared), so `fast` results are characterized under an explicit error envelope and never bit-pinned; all three modes share the same environment contract (round-to-nearest-even, unobservable exception state, subnormals preserved) and the relaxation replaces only the bit-equivalence obligation — memory, bounds, and every structural legality obligation remain discharged by analysis |
+| Floating-point contract policy | Every f32 call site names one of three declared evaluation policies, and the policy indexes the correctness relation its evidence must establish: `off` keeps separate ordered IEEE multiplies and adds (no fast-math flags, not even contraction) and `fma` pins explicit single-rounding fused multiply-add events (`math.fma`/`llvm.fma`) — both are exact contracts gated bit-for-bit against independent references; `fast` is a named relaxation profile declaring exactly reassociation plus multiply-add contraction (`fastmath<reassoc,contract>`, never LLVM's blanket `fast`, which would additionally assert NaN/Inf absence, abandon signed-zero observability, and license reciprocal division and approximate functions the language never declared), so `fast` results are characterized under an explicit error envelope and never bit-pinned; all three modes share the same environment contract (round-to-nearest-even, unobservable exception state, subnormals preserved) and the relaxation replaces only the bit-equivalence obligation — memory, bounds, and every structural legality obligation remain discharged by analysis; the declared relaxation has its one exploiting schedule, `vectorize-ondsp-fp-fast-memref-reduce` (run inside the canonical schedule stage): fused partial-sum lanes plus one cross-lane reduction over a rank-1 fast reduction, refused for off/fma, no aliasing obligation (reads only), and gated by an error envelope against a double reference, a repeated-call determinism check, an executed bitwise divergence from the ordered fused chain on a directed cancellation input, and structural pins — never a bit-exact gate |
 | Canonical pipeline and automatic scheduling | `-ondrix-default-pipeline` (and `ondrix-compile --emit=llvm` from `.ox` source) runs the whole flow with one flag: compile-time design evaluation (the fail-closed quantization tie guard aborts the compile rather than ship a misquantized table), contract conversion (operations whose reductions bufferize directly stay in contract form), proof-gated constant-index forwarding before bufferization (`forward-ondrix-insert-extract`, described under Spectral magnitude), boundary bufferization, an automatic schedule stage, and lowering to the LLVM dialect; inside the schedule stage every candidate transform is filtered by its own legality analysis and applied in a documented priority order (order-preserving vertical batchings first, then saturating-certified and wrap horizontal reductions on the sites batching cannot serve), so an unauthorized site keeps its ordered scalar schedule and the user's only inputs are the numeric contracts in the source; the target vector width is a pipeline parameter in register bits from which each transform's lane count is derived (the same module compiles at any width; zero yields the all-ordered program); the individual pass flags remain available for ablation, testing, and oracle runs; cost selection is the fixed priority order plus each pass's own profitability guards — a measured regret evaluation against the best legal candidate is planned for the frozen-revision evaluation; the composed four-stage `.ox` program (windowed-sinc design, valid FIR, RFFT64, magnitude) compiles through this pipeline with no hand-picked passes — the evaluated design constants feed the certified saturating horizontal reduction — and its default-width and ordered width-zero objects are both gated bit-exactly against one independent C reference, so schedule invariance of the exact contracts is a checked fact |
 | Generic Vector CPU lowering | Automatic unit-stride Q15/Q31 chunking, ordered saturating updates, and exact-modulo wrapping reduction implemented; the horizontal wrapping path admits signed frac30 Q15 accumulators wider than i40 up to i64, since exact-modulo reassociation legality is width-independent up to the i64 lane carrier; a genuinely wrapping i48 reduction object gate pins horizontal, ordered, and an exact mod-2^48 reference bit-identical on cases whose ordered prefixes leave the accumulator range, including an exact full-turn return to zero |
 | Algorithm transforms | Opt-in specialization for static rank-1 FIR samples using immutable constant memref globals or proven complete unit-stride views: zero-tap elimination, exact-modulo symmetric full-product pairing, and symmetric saturating pairing when complete prefix-range analysis proves both schedules safe |

include/ondrix/Conversion/Passes.h

@@ -31,6 +31,9 @@ std::unique_ptr<mlir::Pass> createVectorizeOndspFixedDecimateOutputsPass(
 std::unique_ptr<mlir::Pass> createVectorizeOndspFpFilterOutputsPass();
 std::unique_ptr<mlir::Pass>
 createVectorizeOndspFpFilterOutputsPass(const VectorizeOndspFpFilterOutputsOptions &options);
+std::unique_ptr<mlir::Pass> createVectorizeOndspFpFastMemRefReducePass();
+std::unique_ptr<mlir::Pass>
+createVectorizeOndspFpFastMemRefReducePass(const VectorizeOndspFpFastMemRefReduceOptions &options);
 
 #define GEN_PASS_REGISTRATION
 #include "ondrix/Conversion/Passes.h.inc"

include/ondrix/Conversion/Passes.td

@@ -397,6 +397,47 @@ def VectorizeOndspFixedDecimateOutputs
   ];
 }
 
+def VectorizeOndspFpFastMemRefReduce
+    : Pass<"vectorize-ondsp-fp-fast-memref-reduce", "mlir::ModuleOp"> {
+  let summary = "Vectorize f32 reductions whose call sites declared the fast "
+                "relaxation";
+  let description = [{
+    Splits a rank-1 f32 `ondsp.reduce_mac` under `contract = fast` into
+    W-lane fused partial sums, one cross-lane `vector.reduction <add>`, and a
+    scalar tail, every floating-point operation carrying exactly the declared
+    `fastmath<reassoc, contract>` profile. This is the one transform that
+    exploits the relaxation the fast contract declares: regrouping one
+    output's accumulation chain across lanes is precisely the reassociation a
+    call site authorizes by writing `contract = fast`, and precisely the
+    value change the off and fma contracts forbid, so those two are refused
+    here — the exact inverse of the order-preserving batching pass's refusal
+    of fast. The rewrite reorders reads only and produces one scalar, so
+    unlike the batching passes it carries no aliasing obligation.
+
+    Because the result is declaratively relaxed, its evidence is an error
+    envelope against a higher-precision reference, a determinism check, and a
+    structural pin of the emitted vector form — never a bit-exact gate. The
+    canonical pipeline runs this pass inside its schedule stage; the
+    standalone flag remains an ablation and oracle interface. Only the
+    default LLVM memory space and statically unit-strided minor dimensions
+    are supported; other reductions remain unchanged for scalar lowering.
+  }];
+  let constructor = "ondrix::createVectorizeOndspFpFastMemRefReducePass()";
+  let dependentDialects = [
+    "ondrix::ondsp::OndspDialect",
+    "mlir::arith::ArithDialect",
+    "mlir::cf::ControlFlowDialect",
+    "mlir::math::MathDialect",
+    "mlir::memref::MemRefDialect",
+    "mlir::scf::SCFDialect",
+    "mlir::vector::VectorDialect",
+  ];
+  let options = [
+    Option<"vectorWidth", "vector-width", "int64_t", /*default=*/"8",
+           "Number of f32 lanes per partial-sum vector">,
+  ];
+}
+
 def VectorizeOndspFpFilterOutputs
     : Pass<"vectorize-ondsp-fp-filter-outputs", "mlir::ModuleOp"> {
   let summary = "Batch independent f32 filter outputs into vector lanes under "

lib/Conversion/OndspVectorization/CMakeLists.txt

@@ -1,5 +1,6 @@
 add_ondrix_library(OndspVectorization
   OndspDecimateOutputBatching.cpp
+  OndspFpFastMemRefReduce.cpp
   OndspFpFilterOutputBatching.cpp
   OndspVectorization.cpp
 

lib/Conversion/OndspVectorization/OndspFpFastMemRefReduce.cpp

@@ -0,0 +1,151 @@
+#include "ondrix/Conversion/OndspVectorization/OndspVectorization.h"
+#include "ondrix/Conversion/Utils/MemRefLayoutUtils.h"
+#include "ondrix/Conversion/Utils/ReductionUtils.h"
+
+#include "ondrix/Dialect/ondsp/IR/OndspDialect.h"
+#include "ondrix/Dialect/ondsp/IR/OndspOps.h"
+#include "ondrix/Dialect/ondsp/IR/OndspSemantics.h"
+
+#include "mlir/Dialect/Arith/IR/Arith.h"
+#include "mlir/Dialect/ControlFlow/IR/ControlFlowOps.h"
+#include "mlir/Dialect/Math/IR/Math.h"
+#include "mlir/Dialect/MemRef/IR/MemRef.h"
+#include "mlir/Dialect/SCF/IR/SCF.h"
+#include "mlir/Dialect/Vector/IR/VectorOps.h"
+#include "mlir/IR/BuiltinOps.h"
+#include "mlir/Pass/Pass.h"
+#include "mlir/Transforms/DialectConversion.h"
+
+namespace ondrix {
+#define GEN_PASS_DEF_VECTORIZEONDSPFPFASTMEMREFREDUCE
+#include "ondrix/Conversion/Passes.h.inc"
+} // namespace ondrix
+
+using namespace mlir;
+
+namespace {
+
+/// Largest accepted lane count, bounding every index the rewrite derives.
+constexpr int64_t kMaxVectorWidth = 4096;
+
+bool isSupportedFastMemRefReduction(ondrix::ondsp::ReduceMacOp op) {
+  auto numeric = dyn_cast<ondrix::ondsp::FpAttr>(op.getNumeric());
+  if (!numeric || !numeric.getFormat().isF32() ||
+      numeric.getContract() != ondrix::ondsp::FpContractMode::Fast || op.getProduct() ||
+      !op.getInitial().getType().isF32())
+    return false;
+  auto lhsType = dyn_cast<MemRefType>(op.getLhs().getType());
+  auto rhsType = dyn_cast<MemRefType>(op.getRhs().getType());
+  return lhsType && rhsType && lhsType.getRank() == 1 && rhsType.getRank() == 1 &&
+         lhsType.getElementType().isF32() && rhsType.getElementType().isF32() &&
+         ondrix::conversion::hasDefaultLLVMVectorMemorySpace(lhsType) &&
+         ondrix::conversion::hasDefaultLLVMVectorMemorySpace(rhsType) &&
+         isLastMemrefDimUnitStride(lhsType) && isLastMemrefDimUnitStride(rhsType);
+}
+
+class FastReduceMacOpVectorization final : public OpConversionPattern<ondrix::ondsp::ReduceMacOp> {
+public:
+  FastReduceMacOpVectorization(MLIRContext *context, int64_t vectorWidth)
+      : OpConversionPattern(context), vectorWidth(vectorWidth) {}
+
+  LogicalResult matchAndRewrite(ondrix::ondsp::ReduceMacOp op, OpAdaptor adaptor,
+                                ConversionPatternRewriter &rewriter) const override {
+    if (!isSupportedFastMemRefReduction(op))
+      return failure();
+
+    Type elementType = rewriter.getF32Type();
+    FailureOr<ondrix::conversion::RankOneReductionBounds> bounds =
+        ondrix::conversion::createRankOneMemRefReductionBounds(
+            op, adaptor.getLhs(), adaptor.getRhs(), elementType, "fast f32 memref vectorization",
+            rewriter);
+    if (failed(bounds))
+      return failure();
+
+    Location loc = op.getLoc();
+    auto fastFlags =
+        arith::FastMathFlagsAttr::get(getContext(), ondrix::ondsp::getFastContractFlags());
+    Value vectorStep = rewriter.create<arith::ConstantIndexOp>(loc, vectorWidth);
+    Value remainder = rewriter.create<arith::RemUIOp>(loc, bounds->upperBound, vectorStep);
+    Value vectorEnd = rewriter.create<arith::SubIOp>(loc, bounds->upperBound, remainder);
+    auto vectorType = VectorType::get({vectorWidth}, elementType);
+    Value zeroLanes = rewriter.create<arith::ConstantOp>(
+        loc, vectorType, DenseElementsAttr::get(vectorType, rewriter.getF32FloatAttr(0.0f)));
+
+    auto vectorLoop = rewriter.create<scf::ForOp>(
+        loc, bounds->lowerBound, vectorEnd, vectorStep, ValueRange{zeroLanes},
+        [&](OpBuilder &builder, Location bodyLoc, Value base, ValueRange iterArgs) {
+          Value lhs = builder.create<vector::LoadOp>(bodyLoc, vectorType, adaptor.getLhs(), base);
+          Value rhs = builder.create<vector::LoadOp>(bodyLoc, vectorType, adaptor.getRhs(), base);
+          Value next = builder.create<math::FmaOp>(bodyLoc, lhs, rhs, iterArgs.front(), fastFlags);
+          builder.create<scf::YieldOp>(bodyLoc, next);
+        });
+
+    // MLIR 17's vector.reduction carries no fastmath attribute; it lowers to
+    // the ordered llvm.intr.vector.reduce.fadd, a fixed deterministic
+    // regrouping the declared relaxation authorizes.
+    Value reduced = rewriter.create<vector::ReductionOp>(loc, vector::CombiningKind::ADD,
+                                                         vectorLoop.getResult(0));
+
+    Value scalarStep = rewriter.create<arith::ConstantIndexOp>(loc, 1);
+    auto tailLoop = rewriter.create<scf::ForOp>(
+        loc, vectorEnd, bounds->upperBound, scalarStep, ValueRange{reduced},
+        [&](OpBuilder &builder, Location bodyLoc, Value index, ValueRange iterArgs) {
+          Value lhs = builder.create<memref::LoadOp>(bodyLoc, adaptor.getLhs(), index);
+          Value rhs = builder.create<memref::LoadOp>(bodyLoc, adaptor.getRhs(), index);
+          Value next = builder.create<math::FmaOp>(bodyLoc, lhs, rhs, iterArgs.front(), fastFlags);
+          builder.create<scf::YieldOp>(bodyLoc, next);
+        });
+
+    rewriter.replaceOpWithNewOp<arith::AddFOp>(op, tailLoop.getResult(0), adaptor.getInitial(),
+                                               fastFlags);
+    return success();
+  }
+
+private:
+  int64_t vectorWidth;
+};
+
+class VectorizeOndspFpFastMemRefReducePass final
+    : public ondrix::impl::VectorizeOndspFpFastMemRefReduceBase<
+          VectorizeOndspFpFastMemRefReducePass> {
+public:
+  using ondrix::impl::VectorizeOndspFpFastMemRefReduceBase<
+      VectorizeOndspFpFastMemRefReducePass>::VectorizeOndspFpFastMemRefReduceBase;
+
+  void runOnOperation() override {
+    if (vectorWidth <= 1) {
+      getOperation().emitError("vector-width must be greater than one");
+      signalPassFailure();
+      return;
+    }
+    if (vectorWidth > kMaxVectorWidth) {
+      getOperation().emitError("vector-width must not exceed ") << kMaxVectorWidth;
+      signalPassFailure();
+      return;
+    }
+
+    RewritePatternSet patterns(&getContext());
+    patterns.add<FastReduceMacOpVectorization>(&getContext(), vectorWidth);
+
+    ConversionTarget target(getContext());
+    target.addLegalDialect<arith::ArithDialect, cf::ControlFlowDialect, math::MathDialect,
+                           memref::MemRefDialect, ondrix::ondsp::OndspDialect, scf::SCFDialect,
+                           vector::VectorDialect>();
+    target.addDynamicallyLegalOp<ondrix::ondsp::ReduceMacOp>(
+        [](ondrix::ondsp::ReduceMacOp op) { return !isSupportedFastMemRefReduction(op); });
+
+    if (failed(applyPartialConversion(getOperation(), target, std::move(patterns))))
+      signalPassFailure();
+  }
+};
+
+} // namespace
+
+std::unique_ptr<Pass> ondrix::createVectorizeOndspFpFastMemRefReducePass() {
+  return std::make_unique<VectorizeOndspFpFastMemRefReducePass>();
+}
+
+std::unique_ptr<Pass> ondrix::createVectorizeOndspFpFastMemRefReducePass(
+    const ondrix::VectorizeOndspFpFastMemRefReduceOptions &options) {
+  return std::make_unique<VectorizeOndspFpFastMemRefReducePass>(options);
+}

lib/Pipelines/OndrixPipelines.cpp

@@ -47,6 +47,7 @@ std::string defaultPipelineText(const ondrix::OndrixDefaultPipelineOptions &opti
   if (options.vectorBits >= 64) {
     int64_t lanes = options.vectorBits / 32;
     os << llvm::formatv("vectorize-ondsp-fp-filter-outputs{{vector-width={0}},", lanes);
+    os << llvm::formatv("vectorize-ondsp-fp-fast-memref-reduce{{vector-width={0}},", lanes);
     os << llvm::formatv("vectorize-ondsp-fixed-decimate-outputs{{vector-width={0}},", lanes);
     os << llvm::formatv(
         "vectorize-ondsp-constant-saturating-memref-reduce{{vector-width={0} max-elements=64},",