This is the spec that ties the M87 architectural invariants to concrete,
testable enforcement points. Each invariant is enforced in three layers that
must agree: the BPMN structure, the pure decision functions, and the unit
tests that prove them. Node IDs are identical across reference/ and
executable/, so this table applies to both BPMN files.
| Invariant | BPMN structure | Pure function (Python / Java) | Proof |
|---|---|---|---|
| Proposal ≠ Execution | Proposer lane has no sequence flow into the Runner lane; the only path crosses two Governance gateways. | decide() cannot reach execute telemetry without passing evaluate_constraints then tool_in_manifest. |
test_complete_path_is_reachable_only_through_verification |
| Authority separation | Decision nodes live in the Governance lane; execution nodes in the Runner lane. | Gate functions (decision) are separate from the worker marshalling (execution). | module structure: gates.py vs workers.py |
| Fail-closed default | Each gateway's default flow routes to a refusing exit; the permissive branch needs an explicit FEEL condition. |
Every gate returns the refusing branch on missing/ambiguous input. | test_halt_*, test_reject_*, test_failed_* |
| Manifest gate | Gw_Manifest default → End_RejManifest. |
tool_in_manifest returns False for unknown tool, action-type mismatch, or a target outside the tool's declared targets_allowed. |
test_reject_when_tool_not_in_manifest, test_m1_targets_allowed_is_enforced |
| Autonomy budget | Gw_Budget default → FailReceipt → End_Failed. |
budget_exceeded_or_error; missing telemetry = exceeded. |
test_failed_on_budget_or_error_or_missing_telemetry, test_budget_boundary_* |
| Artifact-backed completion | End_Complete is reachable only through Verify → Gw_Verify (Yes). |
artifact_verified requires artifact + hash match + validation pass. |
test_reject_verify_when_artifact_unproven |
| Receipts / structured memory | route-memory terminal task records the run. |
make_receipt is deterministic; even a failure is hash-backed. |
test_receipt_is_byte_identical_*, test_even_failure_is_artifact_backed |
| Reasoning trace required | Captured at Propose. |
evaluate_constraints halts when reasoning_trace is empty. |
test_halt_* (no-trace case) |
| BPMN end event | Terminal enum |
Trigger |
|---|---|---|
End_Complete |
COMPLETE |
artifact produced and verified |
End_Halt |
HALT |
constraints unsatisfied / unclear (Gw_Constraints default) |
End_RejManifest |
REJECT_MANIFEST |
tool absent from manifest, or action_type mismatch |
End_Failed |
FAILED |
budget exceeded, runtime error, or missing telemetry |
End_RejVerify |
REJECT_VERIFY |
no artifact, hash mismatch, or validation command failed |
One success path. Four fail-closed exits.
The strongest claim — a gate is a function, a gateway is the same function — is
proven, not asserted. workers/python/tests/test_bpmn_equivalence.py parses the
actual executable/m87-governed-loop.bpmn, evaluates each exclusive gateway the
way Zeebe would (FEEL-guarded flow when its variable matches, else default),
feeds it the variables the real workers emit, and asserts the end event reached
equals decide()'s terminal — across all five terminal classes.
compute_hash / Receipts.computeHash hash structured artifacts via canonical
JSON (sorted keys, compact separators) in both languages, so a receipt produced
by a Java worker verifies against a Python recomputation and vice-versa. A parity
test in each language pins the canonical encoding (test_h2_*, h2StructuredArtifactHashIsCanonicalJson).