[GH-ISSUE #403] Add partial-order and finite-trace comparison for concurrent captures #248

New issue

Closed

opened 2026-10-15 18:22:58 +00:00 by bsakaguchi · 0 comments

bsakaguchi commented

2026-10-15 18:22:58 +00:00

Owner

Originally created by @morluto on GitHub (Jul 22, 2026).
Original GitHub issue: https://github.com/morluto/rea/issues/403

Problem

Process and application comparisons currently tend toward one of two unsafe extremes:

require one byte-for-byte total order, which rejects valid concurrent executions; or
sort, drop, or broadly normalize events, which can hide real ordering regressions.

High-fidelity reconstruction needs a third option: validate every event and field exactly, then compare executions against an explicit concurrency model.

Examples include two background workers completing in either order, teardown events racing after a signal, duplicated terminal reports with bounded cardinality, and optional events established as genuinely optional only by repeated authority captures.

Proposal

Add a first-class partial-order / finite-trace comparison contract for Process Capture and reusable application-runtime evidence.

The contract should support:

named event predicates over terminal, process, filesystem, HTTP, WebSocket, shim, and lifecycle records;
happens_before edges;
unordered concurrent groups;
exact, minimum, maximum, and range cardinalities;
required and optional events;
finite allowed trace variants;
prefix/suffix settlement requirements;
negative constraints such as B must not occur before A;
field-level exact matching before any schedule canonicalization;
evidence identifying which constraint and source events justified equivalence or failure.

Illustrative shape:

{
  "events": {
    "ready": { "kind": "terminal", "contains": "Ready" },
    "shutdown": { "kind": "process", "event": "signal", "signal": "SIGINT" },
    "worker_done": { "kind": "http", "path": "/status", "body": { "status": "completed" } }
  },
  "constraints": [
    { "happens_before": ["ready", "shutdown"] },
    { "happens_before": ["shutdown", "worker_done"] },
    { "cardinality": { "event": "worker_done", "min": 1, "max": 2 } }
  ]
}

Correctness requirements

Validate complete event payloads against exact predicates before canonicalizing order.
Never infer commutativity merely because events have different timestamps or sources.
Broad sorting is not a substitute for declared concurrency.
An event may be optional only when the specification says so; repeated observations can justify a proposed spec but must not silently mutate it.
Unknown or truncated capture regions cannot prove absence, exclusivity, or a cardinality upper bound.
Clock timestamps alone must not establish causality across independent sources.
Preserve raw capture order and locations in Evidence v2 even when the comparison projection is canonicalized.
A passing result must identify the matched allowed variant or the complete satisfied constraint set.
A failure must return the minimal violated edge/cardinality/predicate plus the relevant event slice.

Integration

Process Capture v4 comparison.
Reactive scenario transition journals from #330 and #334.
Event-complete process-tree work in #332 and #333.
Static/runtime application comparison where runtime events are available.
Reconstruction verification and portable conformance exports in #336.

Acceptance criteria

A typed schema represents event predicates, happens-before edges, unordered groups, cardinality bounds, and finite allowed traces.
Invalid, cyclic, ambiguous, and unsatisfiable specifications fail validation.
Comparison exact-validates event fields before applying schedule semantics.
Two valid concurrent schedules compare equivalent without sorting unrelated records.
Reversing a required edge fails with a minimal diagnostic.
Missing, extra, duplicated, and out-of-range events fail deterministically.
Optional events and bounded duplicates are accepted only when declared.
Truncated evidence produces unknown, not an equivalence verdict.
Raw order and Evidence v2 locations remain available in the result.
CLI and MCP expose identical structured results and typed failures.
Fixtures cover terminal/process/filesystem/HTTP/WebSocket cross-source ordering.
Documentation explains total order, partial order, finite trace languages, and unsafe normalization patterns.

Non-goals

Guessing a concurrency model from one capture.
Treating timestamp proximity as commutativity.
Ignoring payload differences because event names match.
Solving general distributed-system clock synchronization.

Originally created by @morluto on GitHub (Jul 22, 2026). Original GitHub issue: https://github.com/morluto/rea/issues/403 ## Problem Process and application comparisons currently tend toward one of two unsafe extremes: 1. require one byte-for-byte total order, which rejects valid concurrent executions; or 2. sort, drop, or broadly normalize events, which can hide real ordering regressions. High-fidelity reconstruction needs a third option: validate every event and field exactly, then compare executions against an explicit concurrency model. Examples include two background workers completing in either order, teardown events racing after a signal, duplicated terminal reports with bounded cardinality, and optional events established as genuinely optional only by repeated authority captures. ## Proposal Add a first-class partial-order / finite-trace comparison contract for Process Capture and reusable application-runtime evidence. The contract should support: - named event predicates over terminal, process, filesystem, HTTP, WebSocket, shim, and lifecycle records; - `happens_before` edges; - unordered concurrent groups; - exact, minimum, maximum, and range cardinalities; - required and optional events; - finite allowed trace variants; - prefix/suffix settlement requirements; - negative constraints such as `B must not occur before A`; - field-level exact matching before any schedule canonicalization; - evidence identifying which constraint and source events justified equivalence or failure. Illustrative shape: ```json { "events": { "ready": { "kind": "terminal", "contains": "Ready" }, "shutdown": { "kind": "process", "event": "signal", "signal": "SIGINT" }, "worker_done": { "kind": "http", "path": "/status", "body": { "status": "completed" } } }, "constraints": [ { "happens_before": ["ready", "shutdown"] }, { "happens_before": ["shutdown", "worker_done"] }, { "cardinality": { "event": "worker_done", "min": 1, "max": 2 } } ] } ``` ## Correctness requirements - Validate complete event payloads against exact predicates before canonicalizing order. - Never infer commutativity merely because events have different timestamps or sources. - Broad sorting is not a substitute for declared concurrency. - An event may be optional only when the specification says so; repeated observations can justify a proposed spec but must not silently mutate it. - Unknown or truncated capture regions cannot prove absence, exclusivity, or a cardinality upper bound. - Clock timestamps alone must not establish causality across independent sources. - Preserve raw capture order and locations in Evidence v2 even when the comparison projection is canonicalized. - A passing result must identify the matched allowed variant or the complete satisfied constraint set. - A failure must return the minimal violated edge/cardinality/predicate plus the relevant event slice. ## Integration - Process Capture v4 comparison. - Reactive scenario transition journals from #330 and #334. - Event-complete process-tree work in #332 and #333. - Static/runtime application comparison where runtime events are available. - Reconstruction verification and portable conformance exports in #336. ## Acceptance criteria - [ ] A typed schema represents event predicates, happens-before edges, unordered groups, cardinality bounds, and finite allowed traces. - [ ] Invalid, cyclic, ambiguous, and unsatisfiable specifications fail validation. - [ ] Comparison exact-validates event fields before applying schedule semantics. - [ ] Two valid concurrent schedules compare equivalent without sorting unrelated records. - [ ] Reversing a required edge fails with a minimal diagnostic. - [ ] Missing, extra, duplicated, and out-of-range events fail deterministically. - [ ] Optional events and bounded duplicates are accepted only when declared. - [ ] Truncated evidence produces `unknown`, not an equivalence verdict. - [ ] Raw order and Evidence v2 locations remain available in the result. - [ ] CLI and MCP expose identical structured results and typed failures. - [ ] Fixtures cover terminal/process/filesystem/HTTP/WebSocket cross-source ordering. - [ ] Documentation explains total order, partial order, finite trace languages, and unsafe normalization patterns. ## Non-goals - Guessing a concurrency model from one capture. - Treating timestamp proximity as commutativity. - Ignoring payload differences because event names match. - Solving general distributed-system clock synchronization.

bsakaguchi

2026-10-15 18:22:58 +00:00