Selected stage: loom-lower-graph-memory. Test exactly output obligation mlir-obligation:b2259d118a5c5dd477532292 with its governing context; report any stage at

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

  metadata {
    project = "PolyArch/loom";
    revision = "48615bc5925ef4b9db8b4550b5d4322933cf4b7b";
    source = "docs/spec-compiler-part-3-mem.md:L228-L238";
  }

  // One explicit event edge: a producer's event-plane (`none`) result feeding
  // a consumer operand. Ordinary `dataflow.sync`, `dataflow.mux`, and
  // `dataflow.demux` relay these edges, so the transitive closure of this
  // relation is exactly the ordering materialized by the published event
  // network.
  definition event_edges(program: mlir::Program): Relation<mlir::Operation, mlir::Operation> =
    set { (op, use.owner) |
          op in program.operations,
          value in op.results,
          use in value.uses
          where value.type == mlir::none };

  constraints {
    // The generated strand tags each source memory actor and fence of the one
    // straight-line logical source strand with its selected order.
    let tagged = seq { op | op in output.operations
                       where "sb_index" in op.attributes };

    let sb = closure(event_edges(output));

    // A memory effect is an addressed memory actor; a fence has no
    // alias-partition read or write effect.
    let effects = seq { op | op in tagged
                        where op.name == "dataflow.load"
                           or op.name == "dataflow.store"
                           or op.name == "dataflow.atomic_rmw"
                           or op.name == "dataflow.cmpxchg" };

    let atomic_ops = seq { op | op in tagged
                           where "contract" in op.attributes
                             and (op.attributes["contract"].kind == "#dataflow.atomic_access"
                                  or op.attributes["contract"].kind == "#dataflow.fence_contract"
                                  or op.attributes["contract"].kind == "#dataflow.rmw_contract"
                                  or op.attributes["contract"].kind == "#dataflow.cmpxchg_contract") };

    // Volatile actors, including atomic-volatile actors, which participate in
    // both strand relations.
    let volatile_ops = seq { op | op in tagged
                             where "contract" in op.attributes
                               and (op.attributes["contract"].canonical_text
                                      == "#dataflow.plain_access<is_volatile = true>"
                                    or op.attributes["contract"].canonical_text
                                      == "#dataflow.atomic_access<ordering = seq_cst, sync_scope = <system>, source_alignment_bytes = 4, is_volatile = true>") };

    // Release side: `release`, plus `acq_rel` and `seq_cst`, which apply both
    // directions.
    let release_ops = seq { op | op in tagged
                            where "contract" in op.attributes
                              and (op.attributes["contract"].canonical_text
                                     == "#dataflow.atomic_access<ordering = release, sync_scope = <system>, source_alignment_bytes = 4>"
                                   or op.attributes["contract"].canonical_text
                                     == "#dataflow.atomic_access<ordering = seq_cst, sync_scope = <system>, source_alignment_bytes = 4, is_volatile = true>"
                                   or op.attributes["contract"].canonical_text
                                     == "#dataflow.fence_contract<ordering = release, sync_scope = <system>>"
                                   or op.attributes["contract"].canonical_text
                                     == "#dataflow.fence_contract<ordering = seq_cst, sync_scope = <system>>") };

    // Acquire side: `acquire`, plus `acq_rel` and `seq_cst`.
    let acquire_ops = seq { op | op in tagged
                            where "contract" in op.attributes
                              and (op.attributes["contract"].canonical_text
                                     == "#dataflow.atomic_access<ordering = acquire, sync_scope = <system>, source_alignment_bytes = 4>"
                                   or op.attributes["contract"].canonical_text
                                     == "#dataflow.atomic_access<ordering = seq_cst, sync_scope = <system>, source_alignment_bytes = 4, is_volatile = true>"
                                   or op.attributes["contract"].canonical_text
                                     == "#dataflow.fence_contract<ordering = acquire, sync_scope = <system>>"
                                   or op.attributes["contract"].canonical_text
                                     == "#dataflow.fence_contract<ordering = seq_cst, sync_scope = <system>>") };

    // atomic actors and fences in one logical source strand preserve their
    // selected order
    forall earlier in atomic_ops {
      forall later in atomic_ops
        where earlier.attributes["sb_index"].int < later.attributes["sb_index"].int {
        assert atomic_strand_order: (earlier, later) in sb;
      }
    }

    // volatile actors in one logical source strand preserve their relative
    // order
    forall earlier in volatile_ops {
      forall later in volatile_ops
        where earlier.attributes["sb_index"].int < later.attributes["sb_index"].int {
        assert volatile_strand_order: (earlier, later) in sb;
      }
    }

    // release actors and fences wait for prior memory-effect tails whose
    // visibility they publish
    forall publisher in release_ops {
      forall effect in effects
        where effect.attributes["sb_index"].int < publisher.attributes["sb_index"].int {
        assert release_waits_for_prior_effects: (effect, publisher) in sb;
      }
    }

    // acquire actors and fences precede later constrained memory effects
    forall importer in acquire_ops {
      forall effect in effects
        where effect.attributes["sb_index"].int > importer.attributes["sb_index"].int {
        assert acquire_precedes_later_effects: (importer, effect) in sb;
      }
    }
  }
}