MLIR passage 5: FMulAdd child type and fast-math preservation

postcondition fmuladd_children_preserve_source_type_and_contract {
  language v0;
  vocabulary mlir = mlir.generic@1;

  metadata {
    project = "PolyArch/loom";
    revision = "48615bc5925ef4b9db8b4550b5d4322933cf4b7b";
    source = "docs/spec-compiler-part-2-scf.md:L1036-L1039";
  }

  // Two dialect spellings of one fast-math contract: the imported
  // `#llvm.fastmath<...>` value of the source intrinsic and the
  // `#arith.fastmath<...>` value a standard floating operation states.
  // This is a spelling correspondence only; it neither adds nor removes a
  // flag.
  definition fastmath_spelling(): Relation<String, String> =
    set {
      ("#llvm.fastmath<none>", "#arith.fastmath<none>"),
      ("#llvm.fastmath<nnan>", "#arith.fastmath<nnan>"),
      ("#llvm.fastmath<fast>", "#arith.fastmath<fast>"),
      ("#llvm.fastmath<nnan, contract>", "#arith.fastmath<nnan,contract>"),
      ("#llvm.fastmath<nnan,contract>", "#arith.fastmath<nnan,contract>"),
      ("#llvm.fastmath<nnan, contract>", "#arith.fastmath<nnan, contract>"),
      ("#llvm.fastmath<nnan,contract>", "#arith.fastmath<nnan, contract>")
    };

  // The callables of an S0 program: an imported `llvm.func` and a native
  // `func.func`.
  definition callables(p: mlir::Program): Seq<mlir::Operation> =
    seq { op | op in p.operations
          where op.name == "llvm.func" or op.name == "func.func" };

  // The execution-shape slots the callable `f` owns, in program order: an
  // unresolved `llvm.intr.fmuladd` or the `math.fma` child materialized in its
  // place. Operations owned by a nested callable belong to that callable.
  definition owned_shape_slots(p: mlir::Program,
                               f: mlir::Operation): Seq<mlir::Operation> =
    seq { op | op in p.operations
          where (op.name == "llvm.intr.fmuladd" or op.name == "math.fma")
            and mlir::contains(f, op)
            and (none g in callables(p)
                 where g != f and mlir::contains(f, g) and mlir::contains(g, op)) };

  constraints {
    forall f in callables(output) {
      // Ownership lineage: each child stands in the same callable, at the same
      // slot, as the `llvm.intr.fmuladd` it materializes.
      assert child_preserves_exact_result_type:
        exists s in callables(input)
        where s.attributes["sym_name"].string == f.attributes["sym_name"].string
          and (forall slot in zip_exact(owned_shape_slots(output, f),
                                        owned_shape_slots(input, s))
               where slot.left.name != "math.fma"
                  or slot.left.results[0].type == slot.right.results[0].type);

      assert child_preserves_exact_operand_types:
        exists s in callables(input)
        where s.attributes["sym_name"].string == f.attributes["sym_name"].string
          and (forall slot in zip_exact(owned_shape_slots(output, f),
                                        owned_shape_slots(input, s))
               where slot.left.name != "math.fma"
                  or (forall pair in zip_exact(slot.left.operands, slot.right.operands)
                      where pair.left.type == pair.right.type));

      assert child_preserves_fastmath_contract:
        exists s in callables(input)
        where s.attributes["sym_name"].string == f.attributes["sym_name"].string
          and (forall slot in zip_exact(owned_shape_slots(output, f),
                                        owned_shape_slots(input, s))
               where slot.left.name != "math.fma"
                  or (slot.right.name == "llvm.intr.fmuladd"
                      and (slot.right.attributes["fastmathFlags"].canonical_text,
                           slot.left.attributes["fastmath"].canonical_text)
                          in fastmath_spelling())
                  or (slot.right.name == "math.fma"
                      and slot.left.attributes["fastmath"].canonical_text
                          == slot.right.attributes["fastmath"].canonical_text));
    }
  }
}