M2.1: DPO concurrency theorem coverage (critical pair / rule composition litmus tests)

[flyingrobots]

Pulse context: adhesive/quasi-adhesive category foundations for DPO rewriting + concurrency theorem / rule composition.

Goal

• Strengthen Echo’s determinism + concurrency claims by grounding and testing DPO-style rule composition/independence properties:
  • commuting (parallel independent) rule applications
  • conflicting overlaps (critical pairs)
  • composite/concurrent rule reasoning as executable tests.

Scope

• Spec work:
  • Document the assumed ambient category conditions (pragmatically: typed directed graphs behave like an adhesive setting for the rewrite operations Echo uses).
  • Map Echo/WARP concepts (footprints, in/out slots, dangling-edge prevention) to DPO conditions (gluing/dangling) at the level we need.
• Tests (litmus set):
  • Add a minimal suite of rule-pair scenarios that:
    • commute (apply A then B == B then A) and match terminal digests.
    • conflict (non-commuting overlap) and demonstrate deterministic resolution (reject/serialize or conflict resolver).
  • Where possible, express expected behavior using critical-pair style classification (independent vs dependent).

Acceptance criteria

• A spec note explains which parts of the DPO concurrency story we rely on, and what Echo enforces mechanically (scheduler overlap detection, footprint independence checks).
• New tests pin at least:
  • one commuting pair
  • one conflicting pair
  • one “overlap but still composable” scenario if applicable.

Related

• Complements existing commute/independence property tests in warp-core.
• Informs issue M4: Concurrency litmus suite for scheduler determinism (overlap detection + canonical reduction) #189 (concurrency litmus suite) by giving a theory-backed taxonomy of cases.