Skip to content

Independently reproduce participant-crossing bisimulation #975

Closed
Closed
Independently reproduce participant-crossing bisimulation#975
Labels
area:runtimeRuntime and control-plane codeenhancementNew feature or request
Milestone
Participant Information-Flow & Behavioral Equivalence

Description

@Brad-Edwards
Brad-Edwards
opened on Jul 29, 2026

Parent: #811

Bounded outcome

Independently reproduce the participant-crossing-dpbb-finite-v1 equivalence decision from clean pinned inputs and verify every published digest, domain count, mutation outcome, command, and claim boundary. The reproducer must not reuse an unreviewed result directory or accept a producer-authored summary as evidence.

Negative cases

  • Clean-room command or platform produces different model/result digests.
  • Tool identity or archive/container digest cannot be verified.
  • State/transition/domain counts differ.
  • Mutation outcomes or tau partition differ.
  • Network, environment, host path, or cached workspace affects the result.
  • Published artifact omits a limitation or separate-claim boundary.

Evidence required

  • Independent reviewer identity and environment record.
  • Clean fixed command, expected result, and actual result.
  • Recomputed model/profile/source/tool/artifact digests.
  • Recomputed state/transition/domain counts and mutation outcomes.
  • Reproduction decision linked to the exact model-check claim.

Explicit nonclaims

  • Reproduction does not widen the theorem profile.
  • No live-runtime realization, backend conformance, noninterference, or opacity result.

Dependencies

Requirements

  • SEM-232
  • ASR-535

Activity

  1. Brad-Edwards
    added
    enhancementNew feature or request
    area:runtimeRuntime and control-plane code
    on Jul 29, 2026
  2. Brad-Edwards
    added
    deferred
    on Sep 20, 2026
  3. Brad-Edwards
    changed the title [-]Independently reproduce participant-crossing bisimulation[/-] [+]Deferred: Independently reproduce participant-crossing bisimulation[/+] on Sep 20, 2026
  4. Brad-Edwards
    removed
    deferred
    on Sep 20, 2026
  5. Brad-Edwards
    changed the title [-]Deferred: Independently reproduce participant-crossing bisimulation[/-] [+]Independently reproduce participant-crossing bisimulation[/+] on Sep 20, 2026
  6. Brad-Edwards
    marked this as blocked on Sep 22, 2026
  7. Brad-Edwards
    marked this as blocking on Sep 22, 2026
  8. Brad-Edwards
    added this to the Participant Information-Flow & Behavioral Equivalence milestone on Sep 22, 2026
  9. Brad-Edwards
    marked this as blocking on Oct 11, 2026
  10. Brad-Edwards
    added
    in-progressAn agent is actively working this issue via /implement
    on Oct 31, 2026

  11. Brad-Edwards commented on Oct 31, 2026

    @Brad-Edwards
    Brad-Edwards
    on Oct 31, 2026
    CollaboratorAuthor

    🛠️ Picked up by /implement - driver codex, branch 975-reproduce-participant-bisimulation, 2026-10-31T05:44:20.192Z.

  12. Brad-Edwards commented on Oct 31, 2026

    @Brad-Edwards
    Brad-Edwards
    on Oct 31, 2026
    CollaboratorAuthor

    gc workflow phase recorded: preflight (issue #975). Posted by the MCP server to enforce ordering between workflow steps (issue #794 MVP-2). Do not edit or delete — used by downstream tools to gate phase prerequisites.

  13. Brad-Edwards commented on Oct 31, 2026

    @Brad-Edwards
    Brad-Edwards
    on Oct 31, 2026
    CollaboratorAuthor

    gc workflow phase recorded: preflight (issue #975). Posted by the MCP server to enforce ordering between workflow steps (issue #794 MVP-2). Do not edit or delete — used by downstream tools to gate phase prerequisites.

  14. Brad-Edwards commented on Oct 31, 2026

    @Brad-Edwards
    Brad-Edwards
    on Oct 31, 2026
    CollaboratorAuthor

    Design complete

    Issue #975; branch 975-reproduce-participant-bisimulation; pickup 6539701555.

    Design digest: 476512dd233e8596bbb314c7127499ede4c6ba3c7a1cf2327324d6cb7318d8c5.

    • specs/formal/participant-semantics/participant-crossing-reproduction.md (ebee2273c99e3d3d5bc40116cc605e1241a4b92491180263b0a0275d97251ccc)
    • docs/decisions/issue-975-independent-crossing-reproduction-preflight.md (dec4f11ce8de8c0d02a4737496dd6144eb7b89a703de3e53bbcd9362755f1fa0)

    Research and coverage

    • implementations/formal/participant_crossing/machine_check.py: Use existing public producer, expected-bundle admission, exact inventory and immutable publication.
    • implementations/formal/participant_crossing/machine_check_publication.py: Reuse qualified allowlisted hosted execution provenance; keep local observations distinct.
    • tools/mcrl2_tool.py: Retain admitted tool, fixed comparison command, native network isolation and safe bounded outputs.
    • implementations/formal/participant_crossing/ingress.py: Use bounded no-follow file reads and safe relative paths.
    • https://www.mcrl2.org/web/user_manual/tools/release/ltscompare.html (202607.0, Equivalences, tau hiding and counterexamples): Reproduce exact DPBB mode and ordered AUT inputs; retain supported witness limits.
    • https://github.com/containers/bubblewrap/blob/main/README.md (Reference read 2026-10-31; local bubblewrap version recorded separately, Sandbox security and configuration): Explicit read-only source/tool mounts, cleared environment, fresh output and entire-worker network boundary.
    • https://www.asd-ste100.org/assets/files/ASD-STE100_ISSUE9.pdf (Issue 9 (2025-01-15), read local cached official PDF, Writing rules sections 1, 4, 5 and 6): Consistent technical nouns, short sentences, one fact per sentence and document purpose.
    • architecture: participant-crossing-reproduction.md: compose the existing complete finite producer and admission; a fresh offline worker supplies actual bytes and a separate immutable measurement.
    • systems_security: participant-crossing-reproduction.md: reviewed subject digest, read-only source/tool mounts, whole-worker network isolation, cleared environment, fixed inventories, safe errors and separate external review authority.
    • data_flows: participant-crossing-reproduction.md DFD names source/pin/tool stores, fresh Python/native processes, expected versus actual comparison, measurement store and separate reviewer trust boundary.
    • diagrams: participant-crossing-reproduction.md DFD also describes component and dependency relationships; no runtime or deployment interface changes require another diagram.
    • policy_as_code: Reuse existing profile, claim, source, tool and path validators; new measurement admission composes them. No public schema or tooling policy change is needed.
    • architecture_as_code: Exact worker inventory, explicit imports/mounts and byte comparison enforce the declared source/result boundary; existing native limits and total worker deadline remain.
    • adr_changes: ADR-100, ADR-071 and ADR-117 cover the design; no new architecture decision, runtime surface or accepted-ADR edit is needed.
    • document_review: Reviewed the design against the cached official STE Issue 9 writing rules sections 1,4,5,6 for consistent technical names, sentence limits, single facts and document purpose. Preflight remains guardrail evidence, not a claimed new STE artifact.

  15. 18 remaining items

  16. Brad-Edwards commented on Oct 31, 2026

    @Brad-Edwards
    Brad-Edwards
    on Oct 31, 2026
    CollaboratorAuthor

    Design complete

    Issue #975; branch 975-reproduce-participant-bisimulation; pickup 6539701555.

    Design digest: be6204b87114f3fd86cbac26f30e89935d513350610d843b107346e34edbddaf.

    • specs/formal/participant-semantics/participant-crossing-reproduction.md (d08e3bfaa032171e64d4ef5058ea1790af9d4fbf17869e588cc7f3c50204f289)
    • docs/decisions/issue-975-independent-crossing-reproduction-preflight.md (b693376fde919c7a246d1aa012da2d009d704047ceee9cbbeecce42950984351)

    Research and coverage

    • implementations/formal/participant_crossing/machine_check.py: Use existing public producer, expected-bundle admission, exact inventory and immutable publication.
    • implementations/formal/participant_crossing/machine_check_publication.py: Reuse qualified allowlisted hosted execution provenance; keep local observations distinct.
    • tools/mcrl2_tool.py: Retain admitted tool, fixed comparison command, native network isolation and safe bounded outputs.
    • implementations/formal/participant_crossing/ingress.py: Use bounded no-follow file reads and safe relative paths.
    • implementations/formal/participant_crossing/counterexample_mutations.py: Reuse the reviewed mutation constructors and public corpus/witness interfaces; a separate fixed comparison driver avoids unsupported nested namespaces without changing producer sources or algorithms.
    • https://www.mcrl2.org/web/user_manual/tools/release/ltscompare.html (202607.0, Equivalences, tau hiding and counterexamples): Reproduce exact DPBB mode and ordered AUT inputs; retain supported witness limits.
    • https://github.com/containers/bubblewrap/blob/main/README.md (Reference read 2026-10-31; local bubblewrap version recorded separately, Sandbox security and configuration): Explicit read-only source/tool mounts, cleared environment, fresh output and entire-worker network boundary.
    • https://www.asd-ste100.org/assets/files/ASD-STE100_ISSUE9.pdf (Issue 9 (2025-01-15), read local cached official PDF, Writing rules sections 1, 4, 5 and 6): Consistent technical nouns, short sentences, one fact per sentence and document purpose.
    • architecture: participant-crossing-reproduction.md: compose existing complete model, corpus/witness, result and admission interfaces. A new bounded fixed driver runs the admitted native executable inside one rootless offline worker; original producer source and expected artifacts remain unchanged.
    • systems_security: participant-crossing-reproduction.md: one namespace boundary encloses trusted Python and the admitted native checker. Original workspace, home, credentials, host processes and network remain absent; source, tool and prepared input pairs are read-only. Each native call retains process limits, safe output admission and cleanup. No privileged execution or host-control weakening is introduced. The worker reconstructs every input pair before using its mounted bytes.
    • data_flows: participant-crossing-reproduction.md DFD names source/pin/tool stores, fresh Python/native processes, expected versus actual comparison, measurement store and separate reviewer trust boundary.
    • diagrams: participant-crossing-reproduction.md DFD also describes component and dependency relationships; no runtime or deployment interface changes require another diagram.
    • policy_as_code: Reuse existing profile, claim, source, tool and path validators; new measurement admission composes them. No public schema or tooling policy change is needed.
    • architecture_as_code: Fixed complete comparison inventory, independent fresh model reconstruction, exact mounted-input joins, strict native decision/witness checks, acyclic source/result bindings and whole-worker limits enforce the architecture. The retained manifest binds exact qualified measurement, execution and separate agent acceptance; the archive regression joins all identities without self-approving the measurement.
    • adr_changes: ADR-100, ADR-071 and ADR-117 cover the design; no new architecture decision, runtime surface or accepted-ADR edit is needed.
    • document_review: Reviewed the design against the cached official STE Issue 9 writing rules sections 1,4,5,6 for consistent technical names, sentence limits, single facts and document purpose. Preflight remains guardrail evidence, not a claimed new STE artifact. The retained-evidence description also follows these rules.

  17. Brad-Edwards commented on Oct 31, 2026

    @Brad-Edwards
    Brad-Edwards
    on Oct 31, 2026
    CollaboratorAuthor

    gc workflow phase recorded: plan (issue #975). Posted by the MCP server to enforce ordering between workflow steps (issue #794 MVP-2). Do not edit or delete — used by downstream tools to gate phase prerequisites.

    Design evidence: #975 (comment); architecture: specs/formal/participant-semantics/participant-crossing-reproduction.md. The finite profile, original producer and 46-comparison single-worker architecture remain unchanged.

    Path A: retain the actual qualified CI measurement and execution bytes, plus separate current implementation-agent acceptance linked to the exact claim/mutation subject, under a manifest-addressed capture. The archive regression first failed on the missing pin and now passes. No human identity or cryptographic signature is invented. The user identified the prior producer as an implementation agent; the current issue-975 run performs the fresh reproduction and attributable acceptance.

    Path B: repair CI's missing current runtime-mapping capture by executing all 25 public synthetic cases through collect_cases after final test/policy edits. Publish immutable current-source artifacts; preserve every historical capture, incompatible outcome and observation gap. Do not copy old observations or adjust an old source hash. Verify the targeted mapping module and source/artifact joins.

    Path D: update exact scope/requirement links and retained-evidence documentation. SEM-232 remains DRAFT for its unfulfilled public-claim obligations; ASR-535 remains ACTIVE. No new ADR, schema, runtime authority, backend claim, service, global research capture or release fragment is introduced.

    Security/maintenance: reuse existing ingress, admission, publication and source-bound mapping exporters. Retain offline bounded execution, read-only tool/source/inputs, strict output inventory, no secrets or ambient host cache, and no authenticity claim. Test/policy paths enter the existing source inventory; retained reproduction records and issue-975 scope do not. Run only the affected local cases, existing file-local policy and requirement governance, then republish and require current-head CI/Sonar before readiness.

  18. Brad-Edwards commented on Oct 31, 2026

    @Brad-Edwards
    Brad-Edwards
    on Oct 31, 2026
    CollaboratorAuthor

    Document consistency before push

    Issue #975; branch 975-reproduce-participant-bisimulation; pickup 6539701555.

    Design digest: be6204b87114f3fd86cbac26f30e89935d513350610d843b107346e34edbddaf.

    • specs/formal/participant-semantics/participant-crossing-reproduction.md (d08e3bfaa032171e64d4ef5058ea1790af9d4fbf17869e588cc7f3c50204f289)
    • docs/decisions/issue-975-independent-crossing-reproduction-preflight.md (b693376fde919c7a246d1aa012da2d009d704047ceee9cbbeecce42950984351)

    The candidate retains the exact admitted qualified measurement and execution bytes from run 41178898313 without altering the original machine-check or reproducer computational sources. A separate manifest and agent acceptance bind the exact claim, mutation subject, execution and artifact provenance; the measurement itself still requires review. The archive regression observed missing retained evidence before the pin was added and now passes. Fresh runtime-mapping capture 2f209ab5bb8b7c499881d22f9acf52b55118835de77ec77e16e04ab8ff84fed9 was generated from 25 actual public synthetic executions after the final test/policy source edits, preserving 15 incompatible cases and two observation gaps. Exact requirement ownership/scope and links cover all new artifacts; SEM-232 stays DRAFT and ASR-535 ACTIVE. The design describes this durable evidence and single offline worker accurately, with no new ADR, authority, service, schema, runtime/backend claim or authenticity assertion. Targeted requirement governance, file-local repository policy, Ruff and native Vale passed; no broad local suites ran.

    Candidate tree: 38baea02c320bd2098d35f542b14c70a7fbe8e68.
    Document check: vale: server-owned baseline (Vale.Repetition)
    Checker identity: a9749df8f46a9b49cf48ed4d14b737dd480f2c3a1a933959433a535c894408b7.

  19. Brad-Edwards commented on Oct 31, 2026

    @Brad-Edwards
    Brad-Edwards
    on Oct 31, 2026
    CollaboratorAuthor

    Execution obligation ISSUE-975-CURRENT-MAPPING-CAPTURE — Resolved

    Category: failing_check
    Observed state: A new immutable mapping capture exists for the final computational/test/policy source identity, generated from real public synthetic executions.
    Impact: Current runtime-mapping evidence now represents the changed source inventory while preserving all negative and missing-observation outcomes.
    Current obligation: Collect fresh reports and verify the exact current-source mapping artifacts.

    Evidence

    • Original failure: https://github.com/OpenRAE/rae/actions/runs/41178898313, canonical shard 1, test_issue_972_mapping_export.py::test_published_cases_match_fresh_public_execution.
    • New capture specs/formal/participant-semantics/runtime-mapping/capture-2f209ab5bb8b7c499881d22f9acf52b55118835de77ec77e16e04ab8ff84fed9.
    • Fresh crossing_runtime_cases.collect_cases() executed 25 public synthetic cases after final source/test/policy edits.

    Disposition: fix
    Corrective action: Published a new capture with the existing runtime_mapping_export.publish interface; preserved all historical captures and original model evidence. Added exact issue-975 scope bindings without modifying source-bound policy after collection.

    Verification

    • All nine tests in implementations/python/tests/test_issue_972_mapping_export.py pass, including exact fresh-public-execution replay, deterministic bundle, tamper refusal and historical-tombstone separation.
    • Observed classifications: 8 match, 15 incompatible, 2 observation-gap. Equivalence, runtime realization and backend conformance remain not-established.
    • Archive regression passes; targeted requirement governance and file-local repository policy pass for every changed file.

  20. Brad-Edwards commented on Oct 31, 2026

    @Brad-Edwards
    Brad-Edwards
    on Oct 31, 2026
    CollaboratorAuthor

    Pre-PR base synchronization

    • Source: refs/remotes/origin/dev at a601b696ce6d5d5a84f74305ee77d1983fca8ce8
    • Outcome: already_current
    • Published feature head: a4a8fbecb4c38a51ab9f4ab4ff434e750f15e8a0
    • Synchronized tree: 38baea02c320bd2098d35f542b14c70a7fbe8e68

  21. Brad-Edwards commented on Oct 31, 2026

    @Brad-Edwards
    Brad-Edwards
    on Oct 31, 2026
    CollaboratorAuthor

    Execution obligation ISSUE-975-SONAR-TEST-CLARITY — Opened

    Category: quality
    Observed state: Sonar reports two MAJOR code-smell findings in new reproduction tests; no open security hotspots.
    Impact: The Sonar gate requires clear single-purpose assertions and an unambiguous exception source before readiness.
    Current obligation: Split the composite assertion, encode the candidate before the raises block, run the exact affected tests and regenerate the mapping capture for the changed test sources.

    Evidence

    • Current head a4a8fbe; CI run https://github.com/OpenRAE/rae/actions/runs/41180565568.
    • AaGQ5Ob5wmll2o7CuRcL: implementations/python/tests/test_issue_975_reproduction_checks.py:24 composite assertion.
    • AaGQ5Ofxwmll2o7CuRcM: implementations/python/tests/test_issue_975_reproduction.py:109 exception context contains nested encoder and admission calls.

  22. Brad-Edwards commented on Oct 31, 2026

    @Brad-Edwards
    Brad-Edwards
    on Oct 31, 2026
    CollaboratorAuthor

    gc workflow phase recorded: plan (issue #975). Posted by the MCP server to enforce ordering between workflow steps (issue #794 MVP-2). Do not edit or delete — used by downstream tools to gate phase prerequisites.

    Sonar repair cycle 1 (Path C): split the baseline input assertion into two checks and encode the tampered measurement before entering pytest.raises, so admission is the sole possibly failing operation. These are test-only clarity changes; the original producer, reproducer computation, exact retained qualified measurement, execution record and accepted finite claim remain unchanged.

    Regenerate source-bound runtime mapping with 25 fresh public synthetic executions after those test edits. The new capture is 567e37e4f965c77873838507245df83fc828b50d69f892943cf354113e67eb50; preserve all previous immutable captures and the same 8 matches, 15 incompatible cases and two observation gaps. Add exact SEM-232 scope bindings. Run the seven affected reproduction cases and exact fresh-mapping replay, plus targeted file-local policy and governance. Publish via the existing gate and require a clean current-head Sonar/CI result before resolving ISSUE-975-SONAR-TEST-CLARITY and readiness.

    Architecture and security remain as recorded in #975 (comment) and specs/formal/participant-semantics/participant-crossing-reproduction.md. SEM-232 remains DRAFT; ASR-535 remains ACTIVE. No new authority, dependency, service, runtime/backend claim or broader relation result is introduced.

  23. Brad-Edwards commented on Oct 31, 2026

    @Brad-Edwards
    Brad-Edwards
    on Oct 31, 2026
    CollaboratorAuthor

    Document consistency before push

    Issue #975; branch 975-reproduce-participant-bisimulation; pickup 6539701555.

    Design digest: be6204b87114f3fd86cbac26f30e89935d513350610d843b107346e34edbddaf.

    • specs/formal/participant-semantics/participant-crossing-reproduction.md (d08e3bfaa032171e64d4ef5058ea1790af9d4fbf17869e588cc7f3c50204f289)
    • docs/decisions/issue-975-independent-crossing-reproduction-preflight.md (b693376fde919c7a246d1aa012da2d009d704047ceee9cbbeecce42950984351)

    Sonar cycle 1 changes only test clarity: two independent baseline assertions and one admission call inside the exception context, with encoding performed first. The original producer and all reproducer computational sources, retained qualified evidence and accepted finite claim stay byte-identical. The seven modified reproduction cases pass. Runtime mapping was freshly recollected through all 25 public synthetic cases under current test-source identity 567e37e4f965c77873838507245df83fc828b50d69f892943cf354113e67eb50, preserving 8 matches, 15 incompatible cases and two observation gaps. Exact new scope bindings preserve requirement ownership; SEM-232 remains DRAFT and ASR-535 ACTIVE. Existing source-bound exporter, ingress, fixed sandbox, strict inventory and qualified observer remain the canonical implementations. Documentation accurately describes this unchanged architecture; no design-file edit, new ADR/schema/service/dependency or wider claim is needed. Current-head CI/Sonar must verify the repair before readiness.

    Candidate tree: decb13358e0ac86add8754b26e64106520748920.
    Document check: vale: server-owned baseline (Vale.Repetition)
    Checker identity: a9749df8f46a9b49cf48ed4d14b737dd480f2c3a1a933959433a535c894408b7.

  24. Brad-Edwards commented on Oct 31, 2026

    @Brad-Edwards
    Brad-Edwards
    on Oct 31, 2026
    CollaboratorAuthor

    Pre-PR base synchronization

    • Source: refs/remotes/origin/dev at a601b696ce6d5d5a84f74305ee77d1983fca8ce8
    • Outcome: already_current
    • Published feature head: 4a4278342a8a3b640f1f7412ab63ea974ebfc9a8
    • Synchronized tree: decb13358e0ac86add8754b26e64106520748920

  25. Brad-Edwards commented on Oct 31, 2026

    @Brad-Edwards
    Brad-Edwards
    on Oct 31, 2026
    CollaboratorAuthor

    Execution obligation ISSUE-975-SONAR-TEST-CLARITY — Resolved

    Category: quality
    Observed state: Current-head Sonar analysis has quality gate OK, zero open issues and zero open security hotspots.
    Impact: Both test-quality findings are fixed and verified by the new Sonar analysis.
    Current obligation: Fix both Sonar test-clarity findings and verify current-source mapping evidence.

    Evidence

    • Repair head 4a42783; https://github.com/OpenRAE/rae/actions/runs/41181538154.
    • gc_watch_sonar_analysis returned quality_gate OK, issues_summary.open_count 0 and hotspots_summary.open_count 0; export .gc/sonar/1760-1793433547556.json.
    • All eight current-head test shards, native model/proof jobs, policy checks, integration, coverage and canonical verification passed.

    Disposition: fix
    Corrective action: Split the two baseline input assertions and encode the tampered measurement before pytest.raises, leaving admission as the only operation in the exception context. Recollected all 25 public synthetic mapping cases and published source capture 567e37e4f965c77873838507245df83fc828b50d69f892943cf354113e67eb50; producer/reproducer computation and retained qualified evidence are unchanged.

    Verification

    • Seven exact affected reproduction test cases pass; current-source fresh mapping replay passes.
    • Targeted requirement governance, file-local repository policy and Ruff pass.
    • Current Sonar quality gate is OK with zero open issues and zero hotspots; no suppressions or test weakening were introduced.

  26. Brad-Edwards commented on Oct 31, 2026

    @Brad-Edwards
    Brad-Edwards
    on Oct 31, 2026
    CollaboratorAuthor

    Ready for review — issue #975

    PR: #1760
    Plan: #975 (comment)

    Outcome

    Maintainers can freshly reproduce the pinned finite participant-crossing result inside an offline worker and reject any differing evidence byte. The repository retains the qualified measurement, execution provenance and separate agent acceptance, while preserving all finite-profile limits and runtime-mapping gaps.

    Qualified fresh reproduction matches the original nine-file finite evidence bundle, including 88/107 abstract states/transitions, 178/197 concrete states/transitions, five mutations, four formula checks and 46 comparisons. Current-head CI run 41181538154 and bootstrap qualification 41181538283 passed; Sonar quality gate OK with zero open issues and zero hotspots.

    In-scope requirements

    Proposed state in this PR — authoritative only after merge.

    • SEM-232 (Proof-Bearing Participant-Crossing Bisimulation) — DRAFT (proposed) — Issue 975 delivers the bounded fresh reproduction and attributable agent acceptance. Public/scientific claim publication remains owned by issue 976; no wider requirement completion is asserted.
    • ASR-535 (Participant Information-Flow And Relation Assurance) — ACTIVE (proposed) — Existing active assurance requirement gains exact finite reproduction, negative-case checks and retained qualified evidence. Other assurance axes remain separate.

    Files changed

    Added:

    • docs/decisions/issue-975-independent-crossing-reproduction-preflight.md
    • docs/governance/requirement-scopes/975.json
    • implementations/formal/participant_crossing/reproduction.py
    • implementations/formal/participant_crossing/reproduction_checks.py
    • implementations/formal/participant_crossing/reproduction_sandbox.py
    • implementations/python/tests/test_issue_975_reproduction.py
    • implementations/python/tests/test_issue_975_reproduction_checks.py
    • implementations/python/tests/test_issue_975_reproduction_record.py
    • implementations/python/tests/test_issue_975_reproduction_sandbox.py
    • implementations/python/tests/test_issue_975_reproduction_workflow.py
    • specs/formal/participant-semantics/participant-crossing-reproduction.md
    • specs/formal/participant-semantics/reproduction/capture-3d989819b2b45ea717d1c24e337f53f7bcf7c22c24c030a985e300909b509e46/execution.json
    • specs/formal/participant-semantics/reproduction/capture-3d989819b2b45ea717d1c24e337f53f7bcf7c22c24c030a985e300909b509e46/manifest.json
    • specs/formal/participant-semantics/reproduction/capture-3d989819b2b45ea717d1c24e337f53f7bcf7c22c24c030a985e300909b509e46/measurement.json
    • specs/formal/participant-semantics/reproduction/capture-3d989819b2b45ea717d1c24e337f53f7bcf7c22c24c030a985e300909b509e46/review.json
    • specs/formal/participant-semantics/reproduction/pin.json
    • specs/formal/participant-semantics/runtime-mapping/capture-2f209ab5bb8b7c499881d22f9acf52b55118835de77ec77e16e04ab8ff84fed9/cases.json
    • specs/formal/participant-semantics/runtime-mapping/capture-2f209ab5bb8b7c499881d22f9acf52b55118835de77ec77e16e04ab8ff84fed9/manifest.json
    • specs/formal/participant-semantics/runtime-mapping/capture-567e37e4f965c77873838507245df83fc828b50d69f892943cf354113e67eb50/cases.json
    • specs/formal/participant-semantics/runtime-mapping/capture-567e37e4f965c77873838507245df83fc828b50d69f892943cf354113e67eb50/manifest.json

    Modified:

    • .github/workflows/canonical-verification.yml
    • docs/requirements/ASR-535/requirement.md
    • docs/requirements/SEM-232/requirement.md
    • implementations/formal/participant_crossing/README.md
    • specs/formal/participant-semantics/semantic-coverage.md
    • specs/formal/participant-semantics/semantic-coverage/family-rows.md
    • tools/policy/requirement_order.yaml

    Reviews

    Traceability reconciliation

    Proposed in this PR — verified against the merged tree in Phase E.

    • IMPLEMENTS / TESTS / DOCUMENTS added: 2
    • Links updated: 2
    • Stale links removed: 0

    Status

    • CI: ✅ green
    • SonarCloud: ✅ passed
    • PR ready for user review and merge. Phase E validates the merged requirement state, posts the final report, and closes the issue automatically once this PR merges.

  27. Brad-Edwards commented on Oct 31, 2026

    @Brad-Edwards
    Brad-Edwards
    on Oct 31, 2026
    CollaboratorAuthor

    Delivery readiness recorded — Phase E finalizes issue #975 automatically when PR #1760 merges.

  28. github-actions commented on Oct 31, 2026

    @github-actions
    github-actionsBot
    on Oct 31, 2026 – with GitHub Actions
    Contributor

    Final report — issue #975 complete

    PR: #1760
    Plan: #975 (comment)

    Outcome

    Maintainers can freshly reproduce the pinned finite participant-crossing result inside an offline worker and reject any differing evidence byte. The repository retains the qualified measurement, execution provenance and separate agent acceptance, while preserving all finite-profile limits and runtime-mapping gaps.

    Qualified fresh reproduction matches the original nine-file finite evidence bundle, including 88/107 abstract states/transitions, 178/197 concrete states/transitions, five mutations, four formula checks and 46 comparisons. Current-head CI run 41181538154 and bootstrap qualification 41181538283 passed; Sonar quality gate OK with zero open issues and zero hotspots.

    In-scope requirements

    Verified at merge revision 9bb852c406d6.

    • SEM-232 (Proof-Bearing Participant-Crossing Bisimulation) — DRAFT — Issue 975 delivers the bounded fresh reproduction and attributable agent acceptance. Public/scientific claim publication remains owned by issue 976; no wider requirement completion is asserted.
    • ASR-535 (Participant Information-Flow And Relation Assurance) — ACTIVE — Existing active assurance requirement gains exact finite reproduction, negative-case checks and retained qualified evidence. Other assurance axes remain separate.

    Files changed

    Added:

    • docs/decisions/issue-975-independent-crossing-reproduction-preflight.md
    • docs/governance/requirement-scopes/975.json
    • implementations/formal/participant_crossing/reproduction.py
    • implementations/formal/participant_crossing/reproduction_checks.py
    • implementations/formal/participant_crossing/reproduction_sandbox.py
    • implementations/python/tests/test_issue_975_reproduction.py
    • implementations/python/tests/test_issue_975_reproduction_checks.py
    • implementations/python/tests/test_issue_975_reproduction_record.py
    • implementations/python/tests/test_issue_975_reproduction_sandbox.py
    • implementations/python/tests/test_issue_975_reproduction_workflow.py
    • specs/formal/participant-semantics/participant-crossing-reproduction.md
    • specs/formal/participant-semantics/reproduction/capture-3d989819b2b45ea717d1c24e337f53f7bcf7c22c24c030a985e300909b509e46/execution.json
    • specs/formal/participant-semantics/reproduction/capture-3d989819b2b45ea717d1c24e337f53f7bcf7c22c24c030a985e300909b509e46/manifest.json
    • specs/formal/participant-semantics/reproduction/capture-3d989819b2b45ea717d1c24e337f53f7bcf7c22c24c030a985e300909b509e46/measurement.json
    • specs/formal/participant-semantics/reproduction/capture-3d989819b2b45ea717d1c24e337f53f7bcf7c22c24c030a985e300909b509e46/review.json
    • specs/formal/participant-semantics/reproduction/pin.json
    • specs/formal/participant-semantics/runtime-mapping/capture-2f209ab5bb8b7c499881d22f9acf52b55118835de77ec77e16e04ab8ff84fed9/cases.json
    • specs/formal/participant-semantics/runtime-mapping/capture-2f209ab5bb8b7c499881d22f9acf52b55118835de77ec77e16e04ab8ff84fed9/manifest.json
    • specs/formal/participant-semantics/runtime-mapping/capture-567e37e4f965c77873838507245df83fc828b50d69f892943cf354113e67eb50/cases.json
    • specs/formal/participant-semantics/runtime-mapping/capture-567e37e4f965c77873838507245df83fc828b50d69f892943cf354113e67eb50/manifest.json

    Modified:

    • .github/workflows/canonical-verification.yml
    • docs/requirements/ASR-535/requirement.md
    • docs/requirements/SEM-232/requirement.md
    • implementations/formal/participant_crossing/README.md
    • specs/formal/participant-semantics/semantic-coverage.md
    • specs/formal/participant-semantics/semantic-coverage/family-rows.md
    • tools/policy/requirement_order.yaml

    Reviews

    Traceability reconciliation

    • IMPLEMENTS / TESTS / DOCUMENTS added: 2
    • Links updated: 2
    • Stale links removed: 0

    No authority for runtime realization, backend conformance, noninterference, opacity, unbounded proof or wider profile is asserted. Fresh 25-case runtime mapping retains 15 incompatible cases and two observation gaps.

    Status

    • CI: ✅ green
    • SonarCloud: ✅ passed
    • PR ready for user review and merge.
  29. github-actions
    closed this as completedon Oct 31, 2026
  30. github-actions
    removed
    in-progressAn agent is actively working this issue via /implement
    on Oct 31, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    area:runtimeRuntime and control-plane codeenhancementNew feature or request

    Type

    No type

    Projects

    No projects

      Milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions