feat: enforce modification procedure records - #120
rajasimman-madhivanan wants to merge 15 commits into
Conversation
Co-authored-by: OpenCode <noreply@opencode.ai>
Co-authored-by: OpenCode <noreply@opencode.ai>
Co-authored-by: OpenCode <noreply@opencode.ai>
|
Coverage before: unavailable. The base predates the stacked dependency on change-0001 ( |
|
mode: warn
These checks verify artifact existence and ordering only, not truth, adequacy, or safety sufficiency. |
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
There was a problem hiding this comment.
Nothing blocking. The comments below are optional suggestions. There is no need to push a fix for them before merging.
Beyond the inline findings, I checked whether the new change-control.yml workflow executing PR-controlled Python (tools/change_control, wire_format.py, coverage_delta.py) is exploitable via pull_request_target-style privilege escalation — it isn't: the workflow uses the standard pull_request trigger, so forked PRs run with GitHub's automatically-restricted, read-only token regardless of the permissions: block, and comment-posting is additionally gated behind a same-repo check (CAN_COMMENT).
Extended reasoning...
This run's confirmed findings (checks.py dedup bug, issue_form.py YAML folding bug, parse_srs.py regex chain-length limit) are being posted as inline comments, so the review body should not restate them. I independently verified one of the candidate issues that was flagged and ruled out — the concern that new pull_request workflows might execute PR-controlled code in a privileged security context — by reading .github/workflows/change-control.yml. It uses the pull_request trigger (not pull_request_target), which means forked-repo PRs automatically receive a read-only GITHUB_TOKEN from GitHub regardless of the workflow's declared permissions: block, and the workflow additionally gates any comment-posting behind a head.repo.full_name == github.repository check. This rules out the token-exfiltration/write-access escalation pattern that would otherwise be concerning for a workflow that runs untrusted PR code. Given three confirmed correctness findings already exist as inline comments and this is a process/CI-tooling PR (no runtime safety-path or protocol changes per the PR's own classification), a brief informational note about this additional security check is worth surfacing, but no new top-level concern beyond what's already flagged warrants a fuller review body.
![graphify-labs[bot]](https://avatars.githubusercontent.com/in/4356270?s=60&v=4){kind=small}
There was a problem hiding this comment.
Graphify reviewed this change.
Worth a look — the grounded gate found no coupling regressions or blocking issues, but 5 advisory finding(s) below merit a look before merge.
Formal verification. 2 change(s) alter behavior, breaking input(s) attached.
Behavior changes: decode changes behavior, here is the input that shows it.
The verifier found a concrete input on which decode behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"data":"'\-\-host'"\}, the old code produced \{'message': None, 'stamp': 0, 'counter': 0, 'received\_counter': 0, 'crc\_ok': False\} but the new code produces raises TypeError. Paste that input straight into a regression test.
Behavior changes: encode changes behavior, here is the input that shows it.
The verifier found a concrete input on which encode behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"message":"1","stamp":"2","received\_stamp":"3","counter":"10","received\_counter":"1000000"\}, the old code produced b'\\x02\\x01\\x02\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x03\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x81\\x03\\x02\\x01\\x04\\x03\\x02\\x01\\xe8\\x03\\x00\\x00\\n\\x00\\x00\\x00@B\\x0f\\x00\\x01\\x02\\x00\… but the new code produces b'\\x00\\x01\\x02\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x03\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x81\\x03\\x02\\x01\\x04\\x03\\x02\\x01\\xe8\\x03\\x00\\x00\\n\\x00\\x00\\x00@B\\x0f\\x00;\\xca'. Paste that input straight into a regression test.
Graphify review — findings
Adds a full change-control and safety-traceability CI toolchain: a GitHub Actions suite that runs the change-control checker, coverage-delta comparison, safety-traceability lint, and a wire-break detector, plus issue/PR templates, CODEOWNERS, and contributor guidance for maintainer-owned change records. Enforces the modification procedure by parsing Change Request issue forms, validating class-based approvals (Class C requires two distinct authorizers, emergencies require two approvals and short-form IA), and posting/upserting evidence comments, with a --no-comment fallback when a PR comes from a fork that can't be commented on. Tightens the safety linter's SRS parsing — pipe-aware table splitting that ignores pipes inside code spans, rejection of duplicate and stale baseline entries, and enforcement that HIL reports name their safety requirements — and emits coverage deltas of cited SR tokens between base and head.
Worth a look
- Workflows reference nonexistent actions/checkout@v7 —
.github/workflows/change-control.yml:18· Escalate · high- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Pull-request workflow runs PR-controlled Python with a write-scoped token —
.github/workflows/change-control.yml:32· Escalate · high- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Workflows reference nonexistent actions/checkout@v7 —
.github/workflows/coverage-delta.yml:17· Escalate · high- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Coverage delta workflow runs PR-controlled module with write permissions —
.github/workflows/coverage-delta.yml:26· Escalate · high- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Workflows reference nonexistent actions/checkout@v7 —
.github/workflows/safety-lint.yml:14· Escalate · high- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
Analysis details — impact, health, verification
Impact & health
Graphify review
Impact — 579 functions depend on the 579 functions this change touches.
Health — this change adds coupling hotspots:
- new:
evaluate()— 27 callers, 15 callees - new:
parse_traceability()— 20 callers, 10 callees - new:
analyze()— 11 callers, 6 callees - new:
parse_srs()— 8 callers, 6 callees - new:
compute_signature()— 8 callers, 3 callees - new:
parse_system_definition()— 4 callers, 3 callees - new:
main()— 1 callers, 8 callees - new:
main()— 1 callers, 6 callees
Verification — 579 functions in the blast radius were not formally verified this run (proofs are advisory here).
Gate & verification
graphify gate
PASS — objectively clean (no health regressions, tests not run — proofs not run this pass (advisory)). Grounded, not self-assessed.
Advisory (not blocking):
- verification_scope: 579 function(s) in the blast radius were not formally verified this run
Formal verification
Behavior changes: decode changes behavior, here is the input that shows it.
The verifier found a concrete input on which decode behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"data":"'\-\-host'"\}, the old code produced \{'message': None, 'stamp': 0, 'counter': 0, 'received\_counter': 0, 'crc\_ok': False\} but the new code produces raises TypeError. Paste that input straight into a regression test.
Behavior changes: encode changes behavior, here is the input that shows it.
The verifier found a concrete input on which encode behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"message":"1","stamp":"2","received\_stamp":"3","counter":"10","received\_counter":"1000000"\}, the old code produced b'\\x02\\x01\\x02\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x03\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x81\\x03\\x02\\x01\\x04\\x03\\x02\\x01\\xe8\\x03\\x00\\x00\\n\\x00\\x00\\x00@B\\x0f\\x00\\x01\\x02\\x00\… but the new code produces b'\\x00\\x01\\x02\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x03\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x81\\x03\\x02\\x01\\x04\\x03\\x02\\x01\\xe8\\x03\\x00\\x00\\n\\x00\\x00\\x00@B\\x0f\\x00;\\xca'. Paste that input straight into a regression test.
Could not verify: Could not verify main.
The verifier did not have enough to check main, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 1 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly ConnectionRefusedError — names the real obstacle, not a sampling gap)
· 8 grounded finding(s) anchored inline below.
| } | ||
|
|
||
|
|
||
| def main(argv=None): |
There was a problem hiding this comment.
main()
fans out to 6 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| } | ||
|
|
||
|
|
||
| def evaluate(root, data): |
There was a problem hiding this comment.
evaluate()
fans out to 15 callees (efferent coupling); 27 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return match.group(1) | ||
|
|
||
|
|
||
| def compute_signature(root): |
There was a problem hiding this comment.
compute_signature()
8 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| } | ||
|
|
||
|
|
||
| def main(argv=None): |
There was a problem hiding this comment.
main()
fans out to 8 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return tuple(dict.fromkeys(result)) | ||
|
|
||
|
|
||
| def parse_srs(path): |
There was a problem hiding this comment.
parse_srs()
fans out to 6 callees (efferent coupling); 8 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| from .parse_srs import split_row | ||
|
|
||
|
|
||
| def parse_system_definition(path): |
There was a problem hiding this comment.
parse_system_definition()
high coupling complexity (Ca·Ce = 12).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return tuple(dict.fromkeys(refs)), tuple(issues) | ||
|
|
||
|
|
||
| def parse_traceability(root): |
There was a problem hiding this comment.
parse_traceability()
fans out to 10 callees (efferent coupling); 20 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return frozenset(re.findall(pattern, path.read_text(encoding='utf-8'))) | ||
|
|
||
|
|
||
| def analyze(root): |
There was a problem hiding this comment.
analyze()
fans out to 6 callees (efferent coupling); 11 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
The traceability summary currently contains coverage figures outside the generated regions. Those figures can drift independently and can claim that tests pass when the tooling has only resolved their citations. This adds a check that fails on competing figures and records the existing conflict until its separately authorized document correction lands. ## What changed - Added an error check for numeric requirements and function coverage claims outside generated section 3 markers. - Added an exact baseline entry owned by Raj for the current duplicate headline and footnote claims. - Made removed legacy claims valid while retaining mismatch detection for claims that remain. - Made stale --check output name python3 -m tools.safety_lint --write. - Documented manual regeneration and its citation-only limitation in CONTRIBUTING.md. - Added adversarial and drift tests for marker ownership, identifiers, later sections, and structural coverage exclusions. ## Safety lifecycle Verification and traceability. Bears on IEC 61508-3:2010 Annex A.8.7 and A.8.8, and IEC 61508-1:2010 section 7.18.2. Co-Authored-By: OpenCode <noreply@opencode.ai>
The coverage table generator replaced the document's greater-than-or-equal symbol with two plain characters. Regenerating the table then created an avoidable formatting drift inside the generated region. This keeps the symbol consistent and pins that behavior with a regression test. ## What changed - Updated tools/safety_lint/render.py to emit ≥1 cited test %. - Ran python3 -m tools.safety_lint --write. - Regenerated only the marker-owned table header in docs/safety/TRACEABILITY.md. - Added a test that rejects the ASCII >= spelling in rendered output. - Confirmed the exact C10 baseline discriminator remains unchanged. ## Safety lifecycle Verification record generation and traceability presentation. Bears on IEC 61508-3:2010 Annex A.8.7 and A.8.8, and IEC 61508-1:2010 section 7.18.2. Co-Authored-By: OpenCode <noreply@opencode.ai>
The traceability summary repeated coverage figures outside the generated regions and described resolvable citations as passing tests. Those statements could diverge while each still looked authoritative. This removes the competing figures, keeps the historical reconciliation note, and points readers to the generated source. ## What changed - Reduced section 3 bullets to pointers and retained the 2026-08-07 reconciliation and closure notes verbatim. - Reconciled the SR-M footnote with the generated ≥1 cited test % column. - Removed the now-stale C10 baseline entry. - Added Partially satisfied to the requirements conventions status list. - Updated tests to assert the reconciled real section is clean and injected outside-marker claims still fail. - Confirmed --write leaves both generated regions byte-identical. ## Safety lifecycle Safety requirements documentation, verification records, and forward and backward traceability. Bears on IEC 61508-3:2010 sections 7.2.2 and 7.9, Annex A.8.7 and A.8.8, and IEC 61508-1:2010 section 7.18.2. Co-Authored-By: OpenCode <noreply@opencode.ai>
The numeric cleanup also removed an explanation of what incomplete verification means in practice. This restores that qualitative guidance without reintroducing counts or percentages, so the generated regions remain the sole owner of quantities. ## What changed - Restored the named untested legs beneath the requirements-coverage reconciliation note. - Clarified that the residual requirement is inspection-only and unverified gaps have no test. - Added no numeric coverage claim; C10 remains clean. ## Safety lifecycle Verification records and requirements traceability. Bears on IEC 61508-3:2010 sections 7.9 and 7.10, Annex A.8.7 and A.8.8, and IEC 61508-1:2010 section 7.18.2. Co-Authored-By: OpenCode <noreply@opencode.ai>
Several malformed document shapes could be silently truncated, overwritten, or mistaken for evidence. That could make the reported coverage look complete while parts of the source data had disappeared. This makes those cases fail visibly and moves every published coverage figure into generated regions. ## What changed - Expanded arbitrary allocation slash chains and rejected malformed or descending forms. - Rejected duplicate system-function and reverse-map identifiers with both source lines. - Gave requirement-side and trace-side C6 findings distinct baseline subjects. - Restricted evidence to test artifacts, requirement-naming reports, and scripts/check_*.sh guards; rejected paths now produce C4 findings. - Validated every baseline container, entry, field type, and nonblank value before use. - Generated both function-coverage denominators and removed the obsolete hand-prose checker. - Added contents: read as the sole safety-lint workflow permission. - Added exact baselines for two rejected supplemental citations while preserving 32/40 citation coverage. - Added adversarial tests for every fail-closed path. ## Safety lifecycle Verification evidence integrity and forward and backward traceability. Bears on IEC 61508-3:2010 sections 7.9 and 7.10, Annex A.8.7 and A.8.8, and IEC 61508-1:2010 section 7.18.2. Co-Authored-By: OpenCode <noreply@opencode.ai>
The change-control branch depends on the traceability linter and had fallen behind its reviewed parser and reporting fixes. This merge carries those fixes forward without rewriting either public branch or duplicating their implementation. ## What changed - Merged change-0001-safety-traceability-linter at d399b0d. - Preserved change-0002 warn mode and wire-break enforcement. - Introduced no independent safety-document edits in this merge. ## Safety lifecycle Configuration management, verification evidence integrity, and traceability. Bears on IEC 61508-3:2010 sections 7.9 and 7.10, Annex A.8.7 and A.8.8, and IEC 61508-1:2010 section 7.18.2. Co-Authored-By: OpenCode <noreply@opencode.ai>
The wire guard watched declarations but not the source files that choose field order, checksum behavior, and byte order. Those files could therefore change compatibility without moving the expected signature. This expands the signature boundary and also stops the issue-form reader from silently truncating wrapped text. ## What changed - Added pstop_msg.c, checksum.c, and endian.c to the normalized signature and workflow watch set. - Stored repository-relative per-file hashes and updated the expected aggregate to d0819037896320c1f40b88573770809b42e4a11b7055d65c4991c598116eee4e. - Added one semantic mutation test per implementation file plus source-path diagnostics and comment-only stability tests. - Preserved initial signature bootstrap while preventing it from hiding a simultaneous source change. - Folded continued issue-form label, description, and placeholder text with one space. - Rejected orphan, option, and validation continuations instead of silently discarding them. - Updated the change record to describe the complete wire-behavior boundary. - Kept enforcement-mode at warn and wire-break enforcement independent. ## Safety lifecycle Configuration management, interface compatibility, and verification tooling. Bears on IEC 61508-3:2010 sections 7.4.4, 7.9, and 7.10, and IEC 61508-1:2010 sections 7.16 and 7.18.2. Co-Authored-By: OpenCode <noreply@opencode.ai>
|
Review triage evidence:
Inherited linter defects were fixed in PR #119 and merged via |
There was a problem hiding this comment.
Graphify reviewed this change.
Worth a look — the grounded gate found no coupling regressions or blocking issues, but 5 advisory finding(s) below merit a look before merge.
Formal verification. 2 change(s) alter behavior, breaking input(s) attached.
Behavior changes: decode changes behavior, here is the input that shows it.
The verifier found a concrete input on which decode behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"data":"'\-\-host'"\}, the old code produced \{'message': None, 'stamp': 0, 'counter': 0, 'received\_counter': 0, 'crc\_ok': False\} but the new code produces raises TypeError. Paste that input straight into a regression test.
Behavior changes: encode changes behavior, here is the input that shows it.
The verifier found a concrete input on which encode behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"message":"1","stamp":"2","received\_stamp":"3","counter":"10","received\_counter":"1000000"\}, the old code produced b'\\x02\\x01\\x02\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x03\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x81\\x03\\x02\\x01\\x04\\x03\\x02\\x01\\xe8\\x03\\x00\\x00\\n\\x00\\x00\\x00@B\\x0f\\x00\\x01\\x02\\x00\… but the new code produces b'\\x00\\x01\\x02\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x03\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x81\\x03\\x02\\x01\\x04\\x03\\x02\\x01\\xe8\\x03\\x00\\x00\\n\\x00\\x00\\x00@B\\x0f\\x00;\\xca'. Paste that input straight into a regression test.
Graphify review — findings
Adds a GitHub-native change-control pipeline: a Change Request issue form and PR template feed workflows that run tools.change_control to classify each PR (A/B/C), enforce that authorization precedes implementation and that reviews come from someone other than the implementer, and post findings as PR comments — degrading to --no-comment on forks that lack write access. Adds a wire-break workflow that labels PRs touching watched pstop_c protocol headers/sources or the wire_format.sha256 signature, plus a coverage-delta workflow comparing safety-linter citations across base and head. Documents the process in SECURITY.md, the modification procedure, and safety-traceability/requirements docs, and states in CONTRIBUTING.md that contributors need not author Change Records themselves — a maintainer fills them in when a PR arrives without one.
Worth a look
- PR-controlled revision code is executed while computing coverage delta —
tools/change_control/coverage_delta.py:65· Escalate · high- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Pull-request code runs with a write-scoped GitHub token —
.github/workflows/change-control.yml:32· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Unvalidated PSTOP_BASE_SHA allows git option injection —
scripts/check_wire_format.sh:17· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Foreign issue URLs are treated as current-repo CRs —
tools/change_control/__main__.py:71· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- E6 evidence match falls back to matching any check-run by using head_sha default —
tools/change_control/checks.py· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
Analysis details — impact, health, verification
Impact & health
Graphify review
Impact — 689 functions depend on the 689 functions this change touches.
Health — this change adds coupling hotspots:
- new:
evaluate()— 27 callers, 15 callees - new:
parse_traceability()— 27 callers, 10 callees - new:
analyze()— 12 callers, 6 callees - new:
parse_srs()— 8 callers, 6 callees - new:
compute_signature()— 12 callers, 3 callees - new:
parse_system_definition()— 5 callers, 3 callees - new:
main()— 1 callers, 8 callees - new:
main()— 1 callers, 6 callees
Verification — 689 functions in the blast radius were not formally verified this run (proofs are advisory here).
Gate & verification
graphify gate
PASS — objectively clean (no health regressions, tests not run — proofs not run this pass (advisory)). Grounded, not self-assessed.
Advisory (not blocking):
- verification_scope: 689 function(s) in the blast radius were not formally verified this run
Formal verification
Behavior changes: decode changes behavior, here is the input that shows it.
The verifier found a concrete input on which decode behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"data":"'\-\-host'"\}, the old code produced \{'message': None, 'stamp': 0, 'counter': 0, 'received\_counter': 0, 'crc\_ok': False\} but the new code produces raises TypeError. Paste that input straight into a regression test.
Behavior changes: encode changes behavior, here is the input that shows it.
The verifier found a concrete input on which encode behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"message":"1","stamp":"2","received\_stamp":"3","counter":"10","received\_counter":"1000000"\}, the old code produced b'\\x02\\x01\\x02\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x03\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x81\\x03\\x02\\x01\\x04\\x03\\x02\\x01\\xe8\\x03\\x00\\x00\\n\\x00\\x00\\x00@B\\x0f\\x00\\x01\\x02\\x00\… but the new code produces b'\\x00\\x01\\x02\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x03\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x81\\x03\\x02\\x01\\x04\\x03\\x02\\x01\\xe8\\x03\\x00\\x00\\n\\x00\\x00\\x00@B\\x0f\\x00;\\xca'. Paste that input straight into a regression test.
Could not verify: Could not verify main.
The verifier did not have enough to check main, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 1 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly ConnectionRefusedError — names the real obstacle, not a sampling gap)
· 8 grounded finding(s) anchored inline below.
| } | ||
|
|
||
|
|
||
| def main(argv=None): |
There was a problem hiding this comment.
main()
fans out to 6 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| } | ||
|
|
||
|
|
||
| def evaluate(root, data): |
There was a problem hiding this comment.
evaluate()
fans out to 15 callees (efferent coupling); 27 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return match.group(1) | ||
|
|
||
|
|
||
| def compute_signature(root): |
There was a problem hiding this comment.
compute_signature()
12 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| } | ||
|
|
||
|
|
||
| def main(argv=None): |
There was a problem hiding this comment.
main()
fans out to 8 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return tuple(dict.fromkeys(result)) | ||
|
|
||
|
|
||
| def parse_srs(path): |
There was a problem hiding this comment.
parse_srs()
fans out to 6 callees (efferent coupling); 8 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| from .parse_srs import split_row | ||
|
|
||
|
|
||
| def parse_system_definition(path): |
There was a problem hiding this comment.
parse_system_definition()
high coupling complexity (Ca·Ce = 15).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return tuple(dict.fromkeys(refs)), tuple(issues) | ||
|
|
||
|
|
||
| def parse_traceability(root): |
There was a problem hiding this comment.
parse_traceability()
fans out to 10 callees (efferent coupling); 27 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return frozenset(re.findall(pattern, path.read_text(encoding='utf-8'))) | ||
|
|
||
|
|
||
| def analyze(root): |
There was a problem hiding this comment.
analyze()
fans out to 6 callees (efferent coupling); 12 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
The previous parser hardening rejected ordinary punctuation and allowed some Markdown paths to bypass report validation. It also reused the all-function numerator for the safety-only fraction. This closes those interactions while preserving the current 32/40 citation result. ## What changed - Accepted normal punctuation after complete allocations while rejecting malformed continuations. - Required every Markdown report to live under docs and name the complete requirement token. - Allowed one lowercase decomposition suffix, such as SR-H-04b, to evidence its canonical parent. - Added a safety-only traced-function numerator to text, JSON, and generated rendering. - Added adversarial tests for rule ordering, identifier prefixes, punctuation, traversal, malformed IDs, duplicate baseline keys, and excluded-function arithmetic. - Confirmed disputed traversal, malformed-coverage, and duplicate-baseline findings are unreachable through public analysis paths. - Kept generated output byte-identical and citation coverage at 32/40. ## Safety lifecycle Verification evidence integrity and requirements traceability. Bears on IEC 61508-3:2010 sections 7.9 and 7.10, Annex A.8.7 and A.8.8, and IEC 61508-1:2010 section 7.18.2. Co-Authored-By: OpenCode <noreply@opencode.ai>
The change-control branch includes the traceability linter and must use the same reviewed parser and coverage behavior. This merge carries the final evidence, punctuation, and safety-only arithmetic corrections forward without duplicating them or rewriting public history. ## What changed - Merged change-0001-safety-traceability-linter at 74f1e7e. - Preserved change-control warn mode and independent wire-break enforcement. - Added no PR #120-specific behavior in this merge. ## Safety lifecycle Configuration management and verification evidence integrity. Bears on IEC 61508-3:2010 sections 7.9 and 7.10, Annex A.8.7 and A.8.8, and IEC 61508-1:2010 sections 7.16 and 7.18.2. Co-Authored-By: OpenCode <noreply@opencode.ai>
The change-control workflows trusted several values that came from pull requests or automation metadata. Foreign issue links, missing commit identities, unchecked revisions, inherited credentials, and concurrent comment writers could produce misleading results or duplicate reports. This makes those boundaries explicit while keeping advisory comments and warn mode unchanged. ## What changed - Validated wire comparison revisions as full hexadecimal commit identifiers before invoking Git. - Rejected foreign and mixed-repository change-request links through one shared parser. - Required successful test evidence to name the exact pull-request head commit. - Removed GitHub and Actions credentials from revision-controlled coverage subprocesses while retaining the trusted parent token for comments. - Paginated coverage marker lookup so old comments are updated rather than duplicated. - Added per-PR cancellation groups to both marker-comment workflows. - Added adversarial tests for malformed revisions, foreign identity, absent commit identity, credential inheritance, pagination, and concurrency. - Kept enforcement-mode at warn and the wire signature at d0819037896320c1f40b88573770809b42e4a11b7055d65c4991c598116eee4e. ## Safety lifecycle Modification records, configuration management, and verification evidence integrity. Bears on IEC 61508-1:2010 sections 7.16 and 7.18.2, and IEC 61508-3:2010 sections 7.9 and 7.10. Co-Authored-By: OpenCode <noreply@opencode.ai>
|
Final review evidence for
Change-control tests: 105 passed; safety-lint tests: 98 passed; wire signature remains |
There was a problem hiding this comment.
Graphify reviewed this change.
Worth a look — the grounded gate found no coupling regressions or blocking issues, but 5 advisory finding(s) below merit a look before merge.
Formal verification. 2 change(s) alter behavior, breaking input(s) attached.
Behavior changes: decode changes behavior, here is the input that shows it.
The verifier found a concrete input on which decode behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"data":"'\-\-host'"\}, the old code produced \{'message': None, 'stamp': 0, 'counter': 0, 'received\_counter': 0, 'crc\_ok': False\} but the new code produces raises TypeError. Paste that input straight into a regression test.
Behavior changes: encode changes behavior, here is the input that shows it.
The verifier found a concrete input on which encode behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"message":"1","stamp":"2","received\_stamp":"3","counter":"10","received\_counter":"1000000"\}, the old code produced b'\\x02\\x01\\x02\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x03\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x81\\x03\\x02\\x01\\x04\\x03\\x02\\x01\\xe8\\x03\\x00\\x00\\n\\x00\\x00\\x00@B\\x0f\\x00\\x01\\x02\\x00\… but the new code produces b'\\x00\\x01\\x02\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x03\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x81\\x03\\x02\\x01\\x04\\x03\\x02\\x01\\xe8\\x03\\x00\\x00\\n\\x00\\x00\\x00@B\\x0f\\x00;\\xca'. Paste that input straight into a regression test.
Graphify review — findings
Adds a change-control automation harness for the Protective Stop repo: GitHub issue/PR templates, CODEOWNERS, and workflows that run the change-control checker, safety-traceability linter, coverage-delta comparison, and a wire-break detector, each falling back to --no-comment/no-label when the PR comes from a fork. Wires in tools.change_control and tools.safety_lint (with accompanying self-test suites) to enforce that authorization precedes implementation, named tests and affected interfaces are exercised, expected-update labels carry both required labels, and safety citations don't silently regress. The wire-break job labels PRs wire-break when watched pstop_c headers/sources or the recorded wire_format.sha256 change, then enforces the declaration via check_wire_format.sh.
Worth a look
- Checked-out untrusted revision code is executed via subprocess —
tools/change_control/coverage_delta.py· Escalate · high- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- PR code runs with issue-write token in wire-break workflow —
.github/workflows/wire-break.yml:48· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Required pending E1 state is not part of the specified output states —
changes/change-0002-modification-procedure-enforcement.md· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Required status checks omit change-control despite relying on it for approval enforcement —
docs/process/BRANCH_PROTECTION.md:11· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Nullable PR body is passed directly to change-record parser —
tools/change_control/__main__.py:69· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
Analysis details — impact, health, verification
Impact & health
Graphify review
Impact — 757 functions depend on the 757 functions this change touches.
Health — this change adds coupling hotspots:
- new:
evaluate()— 37 callers, 15 callees - new:
parse_traceability()— 34 callers, 10 callees - new:
analyze()— 14 callers, 6 callees - new:
parse_srs()— 10 callers, 6 callees - new:
compute_signature()— 12 callers, 3 callees - new:
main()— 3 callers, 8 callees - new:
parse_system_definition()— 5 callers, 3 callees - new:
main()— 1 callers, 6 callees
Verification — 757 functions in the blast radius were not formally verified this run (proofs are advisory here).
Gate & verification
graphify gate
PASS — objectively clean (no health regressions, tests not run — proofs not run this pass (advisory)). Grounded, not self-assessed.
Advisory (not blocking):
- verification_scope: 757 function(s) in the blast radius were not formally verified this run
Formal verification
Behavior changes: decode changes behavior, here is the input that shows it.
The verifier found a concrete input on which decode behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"data":"'\-\-host'"\}, the old code produced \{'message': None, 'stamp': 0, 'counter': 0, 'received\_counter': 0, 'crc\_ok': False\} but the new code produces raises TypeError. Paste that input straight into a regression test.
Behavior changes: encode changes behavior, here is the input that shows it.
The verifier found a concrete input on which encode behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"message":"1","stamp":"2","received\_stamp":"3","counter":"10","received\_counter":"1000000"\}, the old code produced b'\\x02\\x01\\x02\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x03\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x81\\x03\\x02\\x01\\x04\\x03\\x02\\x01\\xe8\\x03\\x00\\x00\\n\\x00\\x00\\x00@B\\x0f\\x00\\x01\\x02\\x00\… but the new code produces b'\\x00\\x01\\x02\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x03\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x81\\x03\\x02\\x01\\x04\\x03\\x02\\x01\\xe8\\x03\\x00\\x00\\n\\x00\\x00\\x00@B\\x0f\\x00;\\xca'. Paste that input straight into a regression test.
Could not verify: Could not verify main.
The verifier did not have enough to check main, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 1 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly ConnectionRefusedError — names the real obstacle, not a sampling gap)
· 8 grounded finding(s) anchored inline below.
| } | ||
|
|
||
|
|
||
| def main(argv=None): |
There was a problem hiding this comment.
main()
fans out to 6 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| } | ||
|
|
||
|
|
||
| def evaluate(root, data): |
There was a problem hiding this comment.
evaluate()
fans out to 15 callees (efferent coupling); 37 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return match.group(1) | ||
|
|
||
|
|
||
| def compute_signature(root): |
There was a problem hiding this comment.
compute_signature()
12 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| } | ||
|
|
||
|
|
||
| def main(argv=None): |
There was a problem hiding this comment.
main()
fans out to 8 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return tuple(dict.fromkeys(result)) | ||
|
|
||
|
|
||
| def parse_srs(path): |
There was a problem hiding this comment.
parse_srs()
fans out to 6 callees (efferent coupling); 10 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| from .parse_srs import split_row | ||
|
|
||
|
|
||
| def parse_system_definition(path): |
There was a problem hiding this comment.
parse_system_definition()
high coupling complexity (Ca·Ce = 15).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return tuple(dict.fromkeys(refs)), tuple(issues) | ||
|
|
||
|
|
||
| def parse_traceability(root): |
There was a problem hiding this comment.
parse_traceability()
fans out to 10 callees (efferent coupling); 34 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return frozenset(re.findall(pattern, path.read_text(encoding='utf-8'))) | ||
|
|
||
|
|
||
| def analyze(root): |
There was a problem hiding this comment.
analyze()
fans out to 6 callees (efferent coupling); 14 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
There was a problem hiding this comment.
Nothing blocking. The comments below are optional suggestions. There is no need to push a fix for them before merging.
Beyond the inline finding on parse_srs.py, this run also looked at checks.py's cr_number CR-detection (the optional closes|refs keyword on the foreign/local issue-URL regexes) and coverage_delta.py's run_linter_at_tree subprocess env sanitization (only GH_TOKEN/GITHUB_TOKEN are stripped before running the PR's own linter code) — both were examined and ruled out as not rising to a blocking issue here.
Extended reasoning...
This is the findings-present ruled-out case: one confirmed bug (parse_srs.py:78, malformed-allocation typo detection missing the single-dot case) is being posted as an inline comment on this run. Beyond that, two additional candidate issues in tools/change_control (cr_number's optional closes/refs keyword on issue-URL matching, twice) and one in coverage_delta.py (incomplete env-var stripping before invoking the PR's own safety_lint code as a subprocess) were investigated this run and ruled out as not blocking. These are new items not raised in the three prior reviews on this PR, so per the ruled-out-note policy they are reported once, briefly, without restating the inline finding itself.
Allocation parsing still accepted several typo forms by keeping the valid prefix and dropping the malformed remainder. That could silently remove functions from traceability. This rejects those adjacent typo forms while preserving normal sentence punctuation and properly separated allocations. ## What changed - Rejected single dot, comma, and hyphen separators followed directly by digits. - Rejected malformed fully-prefixed slash members such as F-H-01/F-M02. - Added regression cases for every reproduced malformed form. - Disabled persisted checkout credentials for safety-lint CI. - Removed unused recursive submodule checkout from a repository with no submodules. - Confirmed citation coverage remains 32/40. ## Safety lifecycle Verification evidence integrity and requirements traceability. Bears on IEC 61508-3:2010 sections 7.9 and 7.10, Annex A.8.7 and A.8.8, and IEC 61508-1:2010 section 7.18.2. Co-Authored-By: OpenCode <noreply@opencode.ai>
The change-control branch includes the traceability parser and must reject the same malformed allocation forms as PR #119. This merge carries the completed parser and checkout hardening forward without duplicating code or rewriting public history. ## What changed - Merged change-0001-safety-traceability-linter at 8189602. - Preserved change-control warn mode and independent wire-break enforcement. - Added no PR #120-specific behavior. ## Safety lifecycle Configuration management and verification evidence integrity. Bears on IEC 61508-3:2010 sections 7.9 and 7.10, Annex A.8.7 and A.8.8, and IEC 61508-1:2010 sections 7.16 and 7.18.2. Co-Authored-By: OpenCode <noreply@opencode.ai>
| trailing = cell[match.end() :] | ||
| malformed = ( | ||
| (trailing.startswith('/') and not trailing.startswith('/F-')) | ||
| or (trailing.startswith('/F-') and re.match(r'^/F-[A-Z]-[0-9]{2}(?=$|[\s,.;)])', trailing) is None) |
There was a problem hiding this comment.
🟡 (optional) The new cross-area allocation validator rejects legitimate 3+-hop chains like 'F-H-01/F-M-02/F-I-03', which follow the exact same convention already used in docs (SR-I-02 uses the 2-hop 'F-H-01/F-M-02'). The lookahead (?=$|[\s,.;)]) after /F-[A-Z]-[0-9]{2} forbids a following '/', so any 3rd link in the chain makes the whole cell 'malformed', raising a LintError and breaking the safety-lint CI check for correctly-written SRS/traceability rows. Fix: allow the follow-set after a /F-X-NN token to also include another /F- (recurse/loop the validation across the whole chain), not just end-of-string or single-token punctuation.
Extended reasoning...
expand_allocations('F-H-01/F-M-02/F-I-03'): pattern.finditer first matches 'F-H-01' (alternates group only matches bare /[0-9]{2}, not /F-..., so it stops immediately). trailing = '/F-M-02/F-I-03'. The new check at line 73 tests trailing.startswith('/F-') (True) and re.match(r'^/F-[A-Z]-[0-9]{2}(?=$|[\s,.;)])', trailing); this matches '/F-M-02' but then requires end-of-string or one of \s,.;) immediately after -- the actual next char is '/', which is not in that set, so re.match returns None, making malformed True and raising LintError('malformed allocation ...') even though 'F-I-03' is a perfectly well-formed continuation. Before this commit (74f1e7e), the check only verified trailing started with '/F-' with no further validation, so this exact chain parsed fine. Any future SR row that follows the existing 2-hop convention but allocates to 3+ functions across areas will fail CI with a false 'malformed allocation' error, and self_test.py has no test covering a 3-item cross-area chain to catch this.
Verification: nit. The defect is real and demonstrable by tracing tools/safety_lint/parse_srs.py:67-80. The lookahead at line 73, re.match(r'^/F-[A-Z]-[0-9]{2}(?=$|[\s,.;)])', trailing) is None, only validates a SINGLE following /F-X-NN token: its follow-set [\s,.;)] / $ excludes /. For a 3-hop cross-area chain F-H-01/F-M-02/F-I-03, finditer's first match is bare F-H-01 (the pattern's… | nit.…
There was a problem hiding this comment.
Graphify reviewed this change.
Worth a look — the grounded gate found no coupling regressions or blocking issues, but 5 advisory finding(s) below merit a look before merge.
Formal verification. 2 change(s) alter behavior, breaking input(s) attached.
Behavior changes: decode changes behavior, here is the input that shows it.
The verifier found a concrete input on which decode behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"data":"'\-\-host'"\}, the old code produced \{'message': None, 'stamp': 0, 'counter': 0, 'received\_counter': 0, 'crc\_ok': False\} but the new code produces raises TypeError. Paste that input straight into a regression test.
Behavior changes: encode changes behavior, here is the input that shows it.
The verifier found a concrete input on which encode behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"message":"1","stamp":"2","received\_stamp":"3","counter":"10","received\_counter":"1000000"\}, the old code produced b'\\x02\\x01\\x02\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x03\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x81\\x03\\x02\\x01\\x04\\x03\\x02\\x01\\xe8\\x03\\x00\\x00\\n\\x00\\x00\\x00@B\\x0f\\x00\\x01\\x02\\x00\… but the new code produces b'\\x00\\x01\\x02\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x03\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x81\\x03\\x02\\x01\\x04\\x03\\x02\\x01\\xe8\\x03\\x00\\x00\\n\\x00\\x00\\x00@B\\x0f\\x00;\\xca'. Paste that input straight into a regression test.
Graphify review — findings
Adds a change-control and safety-traceability enforcement layer wired into GitHub PRs. Introduces the tools/change_control toolkit that parses the new Change Request issue form, checks that authorization precedes implementation, requires impact-analysis/class fields, flags stale or ordering-violating approvals, and posts findings on PRs (exiting non-zero in enforce mode); a companion coverage_delta compares safety-linter citations between base and head, and wire_format drives a wire-break label when protocol headers or the declared signature change. Adds the tools/safety_lint linter that parses SG/SR traceability, code references and test citations to build the gap map and reject missing evidence, plus workflows, CODEOWNERS, and issue/PR templates that run these on every PR — with a --no-comment fallback so fork PRs still run the checks without needing write access.
Worth a look
- Running attacker-controlled revision's linter executes untrusted code in CI —
tools/change_control/coverage_delta.py· Escalate · high- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- upsert_coverage_comment builds path with literal '{repo}' vs formatted repository —
tools/change_control/coverage_delta.py· Escalate · high- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- PR revision linter runs as Python with inherited CI environment —
tools/change_control/coverage_delta.py:71· Escalate · high- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- PR-controlled coverage-delta code runs with a writable GitHub token —
.github/workflows/coverage-delta.yml:23· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- PR-controlled wire-format module runs with the labeling token exposed —
.github/workflows/wire-break.yml:19· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
Analysis details — impact, health, verification
Impact & health
Graphify review
Impact — 759 functions depend on the 759 functions this change touches.
Health — this change adds coupling hotspots:
- new:
evaluate()— 37 callers, 15 callees - new:
parse_traceability()— 34 callers, 10 callees - new:
analyze()— 14 callers, 6 callees - new:
parse_srs()— 10 callers, 6 callees - new:
compute_signature()— 12 callers, 3 callees - new:
main()— 3 callers, 8 callees - new:
parse_system_definition()— 5 callers, 3 callees - new:
main()— 1 callers, 6 callees
Verification — 759 functions in the blast radius were not formally verified this run (proofs are advisory here).
Gate & verification
graphify gate
PASS — objectively clean (no health regressions, tests not run — proofs not run this pass (advisory)). Grounded, not self-assessed.
Advisory (not blocking):
- verification_scope: 759 function(s) in the blast radius were not formally verified this run
Formal verification
Behavior changes: decode changes behavior, here is the input that shows it.
The verifier found a concrete input on which decode behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"data":"'\-\-host'"\}, the old code produced \{'message': None, 'stamp': 0, 'counter': 0, 'received\_counter': 0, 'crc\_ok': False\} but the new code produces raises TypeError. Paste that input straight into a regression test.
Behavior changes: encode changes behavior, here is the input that shows it.
The verifier found a concrete input on which encode behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"message":"1","stamp":"2","received\_stamp":"3","counter":"10","received\_counter":"1000000"\}, the old code produced b'\\x02\\x01\\x02\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x03\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x81\\x03\\x02\\x01\\x04\\x03\\x02\\x01\\xe8\\x03\\x00\\x00\\n\\x00\\x00\\x00@B\\x0f\\x00\\x01\\x02\\x00\… but the new code produces b'\\x00\\x01\\x02\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x03\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x81\\x03\\x02\\x01\\x04\\x03\\x02\\x01\\xe8\\x03\\x00\\x00\\n\\x00\\x00\\x00@B\\x0f\\x00;\\xca'. Paste that input straight into a regression test.
Could not verify: Could not verify main.
The verifier did not have enough to check main, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 1 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly ConnectionRefusedError — names the real obstacle, not a sampling gap)
· 8 grounded finding(s) anchored inline below.
| } | ||
|
|
||
|
|
||
| def main(argv=None): |
There was a problem hiding this comment.
main()
fans out to 6 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| } | ||
|
|
||
|
|
||
| def evaluate(root, data): |
There was a problem hiding this comment.
evaluate()
fans out to 15 callees (efferent coupling); 37 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return match.group(1) | ||
|
|
||
|
|
||
| def compute_signature(root): |
There was a problem hiding this comment.
compute_signature()
12 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| } | ||
|
|
||
|
|
||
| def main(argv=None): |
There was a problem hiding this comment.
main()
fans out to 8 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return tuple(dict.fromkeys(result)) | ||
|
|
||
|
|
||
| def parse_srs(path): |
There was a problem hiding this comment.
parse_srs()
fans out to 6 callees (efferent coupling); 10 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| from .parse_srs import split_row | ||
|
|
||
|
|
||
| def parse_system_definition(path): |
There was a problem hiding this comment.
parse_system_definition()
high coupling complexity (Ca·Ce = 15).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return tuple(dict.fromkeys(refs)), tuple(issues) | ||
|
|
||
|
|
||
| def parse_traceability(root): |
There was a problem hiding this comment.
parse_traceability()
fans out to 10 callees (efferent coupling); 34 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return frozenset(re.findall(pattern, path.read_text(encoding='utf-8'))) | ||
|
|
||
|
|
||
| def analyze(root): |
There was a problem hiding this comment.
analyze()
fans out to 6 callees (efferent coupling); 14 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
|
This monolithic PR is being replaced by sequential, non-stacked PRs so each piece is reviewed once against its final base. It remains open as recovery and review history until every replacement exists. Replacement 1: #136 — process foundation and repository intake only. The wire-break, warn-mode checker, and coverage-delta replacement PRs will be created one at a time from updated |
The replacement plan originally created later branches only after each merge. That made unfinished pieces easy to lose over time. This records every branch and dependency now while retaining the rule that each PR is refreshed and reviewed against its final base before merge. ## What changed - Replaced the sequential-after-merge map with four explicit stacked branches. - Recorded each child branch and its parent. - Updated the process-foundation base to merged traceability commit c2dc4cd. - Kept original PR #120 as recovery history until all replacements exist. ## Safety lifecycle Modification planning and configuration management. Bears on IEC 61508-1:2010 sections 6.2 and 7.16, and IEC 61508-3:2010 sections 6.2 and 7.8. Co-Authored-By: OpenCode <noreply@opencode.ai>
|
Superseded by the verified replacement stack:
Each PR targets its immediate predecessor, owns a disjoint file slice, and preserves the reviewed behavior without rewriting published history. First-party CI is green on all four heads. This draft is closed as recovery and review history; its branch and discussion remain intact. |
The existing change-control proposal combined procedure text, repository intake, and several automation systems in one large review. This first replacement adds only the human process and declarative intake surface, so reviewers can assess the rules before any checker or enforcement workflow lands. ## What changed - Migrated the modification procedure, impact-analysis template, release template, and Notion forwarding map. - Added the Change Request issue form, pull-request template, CODEOWNERS, and intended branch-protection settings. - Added external-contribution guidance without requiring contributors to write safety records. - Added the reproducible 16-label definition and synchronization script. - Confirmed security@polymathrobotics.com as the private reporting contact. - Recorded the four-step sequential replacement plan for original PR #120. - Added no workflow, enforcement mode, checker code, wire guard, or coverage automation. ## Safety lifecycle Modification planning, authorization records, configuration management, and release records. Bears on IEC 61508-1:2010 sections 6.2, 7.16, and 7.18, and IEC 61508-3:2010 sections 6.2, 7.8, 7.9, and 7.10. Co-Authored-By: OpenCode <noreply@opencode.ai>
The replacement plan originally created later branches only after each merge. That made unfinished pieces easy to lose over time. This records every branch and dependency now while retaining the rule that each PR is refreshed and reviewed against its final base before merge. ## What changed - Replaced the sequential-after-merge map with four explicit stacked branches. - Recorded each child branch and its parent. - Updated the process-foundation base to merged traceability commit c2dc4cd. - Kept original PR #120 as recovery history until all replacements exist. ## Safety lifecycle Modification planning and configuration management. Bears on IEC 61508-1:2010 sections 6.2 and 7.16, and IEC 61508-3:2010 sections 6.2 and 7.8. Co-Authored-By: OpenCode <noreply@opencode.ai>
1 participant
What this delivers
Dependency
Stacked on change-0001 commit
326a6d0from PR #119. This PR targetsmain; its visible diff will narrow after #119 lands and must not merge first.Classification
Class B: process governance, assurance tooling, and CI guards only. No runtime safety path, protocol, wire layout, requirement text, or verification status changed. Enforcement mode lands as
warn; only the deterministic wire-break guard enforces immediately.Notion migration comparison
All four source pages were fetched read-only through Notion MCP and normalized against their destinations. The Modification Procedure, Impact Analysis, Change Request, and Release Record have no source-only omissions after the authorized repository-link, three-authorizer, Markdown/YAML-form, default-C, and role-annotation transformations. The comparison specifically verified section order, the three-gate model, clause index, declared gaps, warning callout, and every Change Request field. Source details for upstream
pstop_cYes/No-with-link, Gate 1 Run-by, and explicit forward/backward traceability are preserved. No Notion content was modified.Verified locally
python3 tools/change_control/self_test.py: 71 tests passed; one visible unauthenticated CODEOWNERS skipscripts/check_wire_format.sh: pass atPSTOP_VERSION 0x02U,PSTOP_MESSAGE_SIZE 48U, signaturea652abc231b4acb2d9014d73f459123e914fb4b1fcfe8c630f3f8d3853f012afpython3 -m tools.safety_lint --check: pass, unchanged 32/40 cited and 17/40 Verifiedpre-commit run --all-files: all hooks passedgit diff -- docs/safety tools/safety_lint pstop_c firmware machn host ros2 common components: emptyScope boundaries
No branch protection was applied. No bot configuration was guessed. No Gate 2 workflow was added. No runtime or safety-argument file changed.
security@polymathrobotics.comwas human-confirmed before removing its placeholder warning and linking the issue chooser to the private reporting policy.