Adding better support for missed heartbeat messages - #144
johnpolymath wants to merge 5 commits into
Conversation
A missed heartbeat message is determined by the following example: last_sent_timestamp = 100, last_received_timestamp = 100 last_sent_timestamp = 200, last_received_timestamp = 200 now = 300, current message timestamp = 600 This shows that the remote has missed some heartbeats, since the timestamps should increment by a similar amount. - Added new requirement test to validate - Updated several unit tests that didn't properly set the clock correctly
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
| check_timestamp(const pstop_application_t *app, const protocol_data_t *client, const pstop_msg_t *req) | ||
| { | ||
| if(req->stamp <= client->last_received_stamp) { | ||
| return PSTOP_MSG_OUT_OF_ORDER; | ||
| } | ||
|
|
||
| if(req->received_stamp == client->last_timestamp) { | ||
| return PSTOP_OK; | ||
| } | ||
|
|
||
| // did the other end miss a message? | ||
| if(req->received_stamp < client->last_timestamp) { | ||
| uint64_t diff = client->last_timestamp - req->received_stamp; | ||
| // example of missed messages | ||
| // last sent stamp = 500, last received stamp = 500 | ||
| // now = 600, current request stamp = 900 | ||
| // diff = 100, remote diff = 400 | ||
| // diff should be close to the same if no messages have been lost | ||
|
|
||
| uint16_t missed = (uint16_t)(diff / client->heartbeat_ms); | ||
| uint64_t diff_received_stamp = get_diff(req->stamp, client->last_received_stamp); | ||
|
|
||
| if(missed >= (app_config->max_missed_heartbeats + 1U)) { | ||
| return PSTOP_MSG_LOST; | ||
| } | ||
| } | ||
| else { | ||
| uint64_t now = app->env.get_time_cb(); | ||
| if(now < client->last_timestamp) { | ||
| return PSTOP_MSG_OUT_OF_ORDER; | ||
| } | ||
|
|
||
| uint64_t diff_sent_stamp = now - client->last_timestamp; | ||
|
|
||
| uint64_t diff_remote_vs_local = get_diff(diff_sent_stamp, diff_received_stamp); | ||
|
|
||
| uint64_t missed = diff_remote_vs_local / diff_sent_stamp; | ||
| if(missed > (uint64_t)(app->app_config.max_missed_heartbeats + 1U)) { | ||
| return PSTOP_MSG_LOST; |
There was a problem hiding this comment.
🔴 This PR edits pstop_c protocol/timestamp logic directly in this repo, which CLAUDE.md designates off-limits: pstop_c is pre-qualified, "never edited here, never re-verified"; protocol and machine-safety changes must go upstream and return as a version bump. check_timestamp's signature and missed-heartbeat arithmetic (protocol.c:49-75) and pstop_application_init's default limits (pstop_application.c:47) are exactly the counter/stamp/heartbeat-timeout logic the manual reserves for the upstream track, and per CLAUDE.md this is also automatic Class C (touches timing/heartbeat-timeout on the stop path) requiring two-person sign-off before implementation, not present here. …
Extended reasoning...
…Fix: revert this change from pstop_c/ in this repo and land it upstream as a version bump with Class C review, per CLAUDE.md.
CLAUDE.md states 'pstop_c/ is off-limits. Pre-qualified, separate upstream track. Referenced at the interface, never edited here, never re-verified. Protocol and machine-safety changes go upstream and return as a version bump.' This diff modifies pstop_c/pstop/src/pstop/protocol.c (check_timestamp signature and body) and pstop_c/pstop/src/pstop/pstop_application.c (default protocol limits), both inside pstop_c/. Any change touching counter/stamp/heartbeat-timeout logic is automatic Class C requiring two-person authorization before implementation; nothing in the diff or PR description shows that sign-off. Landing this as-is bypasses the pre-qualification boundary that keeps the safety case for the missed-heartbeat diagnostic valid; any downstream user pulling this repo now gets an unvetted, locally-modified version of pre-qualified safety code instead of the upstream-verified one.
Verification: normal — the diff directly edits pstop_c/, which CLAUDE.md §1.2 declares off-limits ("Pre-qualified, separate upstream track. Referenced at the interface, never edited here, never re-verified. Protocol and machine-safety changes go upstream and return as a version bump"). The violation is not hypothetical; it is the changeset itself. Confirmed in the diff: pstop_c/pstop/src/pstop/protocol.c…
![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 3 advisory finding(s) below merit a look before merge.
Formal verification. 1 change(s) alter behavior, breaking input(s) attached.
Behavior changes: flash\_one changes behavior, here is the input that shows it.
The verifier found a concrete input on which flash\_one behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This is a sound refutation from differential testing (both versions run on many generated inputs): a concrete input on which the two versions provably differ.
Evidence: On input \{"cmd":"\-2","v5":"9223372036854775807","port":"12","erase":"0\.03","ip\_timeout":"\-10","app\_ver":"'h\\u00e9llo w\\u00f6rld'"\}, the old code produced \(False, \{'port': 9223372036854775807, 'stage': 'read\-mac'\}\) but the new code produces \(False, \{'port': 12, 'stage': 'read\-mac'\}\). Paste that input straight into a regression test.
Graphify review — findings
Reworks missed-message detection in check_timestamp to compare the elapsed request-stamp delta against the local elapsed time (via get_time_cb) rather than the previous received_stamp/last_timestamp comparison, computing missed heartbeats from the ratio of the two deltas and flagging PSTOP_MSG_LOST when it exceeds max_missed_heartbeats + 1. Changes the default protocol limits in pstop_application_init from 0/0 to 1/1 heartbeats, sets the machine example's limits to 1/2/1000, and updates existing protocol/requirement tests to drive current_time alongside message stamps to match the new time-based logic. Adds a req_2_04 requirements test covering de-bonding behaviour and wires it into the suite runner and CMake build.
Worth a look
- Timestamp echo validation removed from protocol handling —
pstop_c/pstop/src/pstop/protocol.c:49· Escalate · high- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- check_timestamp missed-message math uses wall-clock delta instead of heartbeat interval —
pstop_c/pstop/src/pstop/protocol.c: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
- Application init default protocol limits changed —
pstop_c/pstop/src/pstop/pstop_application.c:47· 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 — 128 functions depend on the 60 functions this change touches.
Health — this change adds coupling hotspots:
- new:
configure_app_defaults()— 33 callers, 7 callees - new:
send_bond()— 23 callers, 4 callees - new:
send_stop()— 18 callers, 4 callees - new:
send_ok()— 16 callers, 4 callees - new:
pstop_application_init()— 5 callers, 5 callees - new:
send_unbond()— 4 callers, 4 callees - new:
protocol_handle_message()— 1 callers, 7 callees - new:
main()— 0 callers, 34 callees - …and 37 more — each is listed as a finding
Verification — 128 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: 128 function(s) in the blast radius were not formally verified this run
Formal verification
Behavior changes: flash\_one changes behavior, here is the input that shows it.
The verifier found a concrete input on which flash\_one behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This is a sound refutation from differential testing (both versions run on many generated inputs): a concrete input on which the two versions provably differ.
Evidence: On input \{"cmd":"\-2","v5":"9223372036854775807","port":"12","erase":"0\.03","ip\_timeout":"\-10","app\_ver":"'h\\u00e9llo w\\u00f6rld'"\}, the old code produced \(False, \{'port': 9223372036854775807, 'stage': 'read\-mac'\}\) but the new code produces \(False, \{'port': 12, 'stage': 'read\-mac'\}\). Paste that input straight into a regression test.
Could not verify: Could not verify esptool\_cmd.
The verifier did not have enough to check esptool\_cmd, 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 SystemExit — names the real obstacle, not a sampling gap)
Could not verify: Could not verify flash.
The verifier did not have enough to check flash, 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: signature changed: no shared positional arity
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 SystemExit — names the real obstacle, not a sampling gap)
Verification did not run: Verification did not run for read\_mac.
The verification could not execute (an environment/toolchain issue, not a statement about the code).
Guarantee: No guarantee, the check itself did not complete.
Note: Detail: harness produced no verdict (rc=124): timeout after 30s
Could not verify: Could not verify selftest.
The verifier did not have enough to check selftest, 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: signature changed: no shared positional arity
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 25 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly NameError — names the real obstacle, not a sampling gap)
Could not verify: Could not verify test\_stale\_check\_names\_exact\_write\_remedy.
The verifier did not have enough to check test\_stale\_check\_names\_exact\_write\_remedy, 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: method — first parameter is `self`, which needs a constructed instance (not synthesizable)
Could not verify: Could not verify run.
The verifier did not have enough to check run, 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 35 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly AttributeError — names the real obstacle, not a sampling gap)
· 1 grounded finding(s) anchored inline below; 44 more finding(s) on lines outside this diff (see the check run).
| // current clock is 300. This will indicate we missed too many | ||
| // messages and will return PSTOP_MSG_LOST. | ||
|
|
||
| static |
There was a problem hiding this comment.
req_2_04_1_test()
fans out to 7 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
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. 1 change(s) alter behavior, breaking input(s) attached.
Behavior changes: flash\_one changes behavior, here is the input that shows it.
The verifier found a concrete input on which flash\_one behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This is a sound refutation from differential testing (both versions run on many generated inputs): a concrete input on which the two versions provably differ.
Evidence: On input \{"cmd":"\-2","v5":"9223372036854775807","port":"12","erase":"0\.03","ip\_timeout":"\-10","app\_ver":"'h\\u00e9llo w\\u00f6rld'"\}, the old code produced \(False, \{'port': 9223372036854775807, 'stage': 'read\-mac'\}\) but the new code produces \(False, \{'port': 12, 'stage': 'read\-mac'\}\). Paste that input straight into a regression test.
Graphify review — findings
Rewrites missed-heartbeat detection in check_timestamp to compare the elapsed time since the last sent message against the remote's reported received-timestamp gap, flagging PSTOP_MSG_LOST when the divergence exceeds max_missed_heartbeats + 1; the function now takes the full pstop_application_t so it can read the current time via get_time_cb, and a get_diff helper handles unsigned subtraction in either direction. Changes the default protocol limits in pstop_application_init from 0/0 to 1/1 and sets explicit limits in the machine example. Adds req_2_04_test to the requirements suite and updates existing protocol tests to advance current_time and populate received_stamp so the timestamp-based loss check has the values it now needs.
Worth a look
- Existing clients now require a non-null time callback —
pstop_c/pstop/src/pstop/protocol.c:67· Escalate · high- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Echoed timestamp no longer validated —
pstop_c/pstop/src/pstop/protocol.c:49· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- check_timestamp missed-heartbeat logic uses full remote-vs-local diff instead of per-heartbeat gap, misclassifying normal traffic —
pstop_c/pstop/src/pstop/protocol.c:82· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Missed heartbeat threshold is off by one —
pstop_c/pstop/src/pstop/protocol.c:79· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Application initializer changed protocol-limit defaults —
pstop_c/pstop/src/pstop/pstop_application.c:47· 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 — 128 functions depend on the 60 functions this change touches.
Health — this change adds coupling hotspots:
- new:
configure_app_defaults()— 33 callers, 7 callees - new:
send_bond()— 23 callers, 4 callees - new:
send_stop()— 18 callers, 4 callees - new:
send_ok()— 16 callers, 4 callees - new:
pstop_application_init()— 5 callers, 5 callees - new:
send_unbond()— 4 callers, 4 callees - new:
protocol_handle_message()— 1 callers, 7 callees - new:
main()— 0 callers, 34 callees - …and 37 more — each is listed as a finding
Verification — 128 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: 128 function(s) in the blast radius were not formally verified this run
Formal verification
Behavior changes: flash\_one changes behavior, here is the input that shows it.
The verifier found a concrete input on which flash\_one behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This is a sound refutation from differential testing (both versions run on many generated inputs): a concrete input on which the two versions provably differ.
Evidence: On input \{"cmd":"\-2","v5":"9223372036854775807","port":"12","erase":"0\.03","ip\_timeout":"\-10","app\_ver":"'h\\u00e9llo w\\u00f6rld'"\}, the old code produced \(False, \{'port': 9223372036854775807, 'stage': 'read\-mac'\}\) but the new code produces \(False, \{'port': 12, 'stage': 'read\-mac'\}\). Paste that input straight into a regression test.
Could not verify: Could not verify esptool\_cmd.
The verifier did not have enough to check esptool\_cmd, 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 SystemExit — names the real obstacle, not a sampling gap)
Could not verify: Could not verify flash.
The verifier did not have enough to check flash, 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: signature changed: no shared positional arity
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 SystemExit — names the real obstacle, not a sampling gap)
Verification did not run: Verification did not run for read\_mac.
The verification could not execute (an environment/toolchain issue, not a statement about the code).
Guarantee: No guarantee, the check itself did not complete.
Note: Detail: harness produced no verdict (rc=124): timeout after 30s
Could not verify: Could not verify selftest.
The verifier did not have enough to check selftest, 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: signature changed: no shared positional arity
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 25 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly NameError — names the real obstacle, not a sampling gap)
Could not verify: Could not verify test\_stale\_check\_names\_exact\_write\_remedy.
The verifier did not have enough to check test\_stale\_check\_names\_exact\_write\_remedy, 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: method — first parameter is `self`, which needs a constructed instance (not synthesizable)
Could not verify: Could not verify run.
The verifier did not have enough to check run, 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 35 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly AttributeError — names the real obstacle, not a sampling gap)
· 1 grounded finding(s) anchored inline below; 44 more finding(s) on lines outside this diff (see the check run).
| // current clock is 300. This will indicate we missed too many | ||
| // messages and will return PSTOP_MSG_LOST. | ||
|
|
||
| static |
There was a problem hiding this comment.
req_2_04_1_test()
fans out to 7 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| uint64_t diff_received_stamp = get_diff(req->stamp, client->last_received_stamp); | ||
|
|
||
| if(missed >= (app_config->max_missed_heartbeats + 1U)) { | ||
| return PSTOP_MSG_LOST; | ||
| } | ||
| uint64_t now = app->env.get_time_cb(); | ||
|
|
||
| uint64_t diff_sent_stamp = get_diff(now, client->last_timestamp); | ||
|
|
||
| uint64_t diff_remote_vs_local = get_diff(diff_sent_stamp, diff_received_stamp); | ||
|
|
||
| if(diff_sent_stamp == 0U) { | ||
| // the chances of this happening are extremely unlikely. | ||
| // It would mean that the amount of time to run through processing | ||
| // a single message takes 0ms. | ||
|
|
||
| // If this does happen then the received timestamps should also be | ||
| // close to 0ms. Setting diff_sent_stamp = 1 will mean that the | ||
| // diff_remote_vs_local is the max number of missed hearbeats. | ||
| diff_sent_stamp = 1U; | ||
| } | ||
| else { | ||
| return PSTOP_MSG_OUT_OF_ORDER; | ||
| uint64_t missed = diff_remote_vs_local / diff_sent_stamp; |
There was a problem hiding this comment.
🔴 This regresses the missed-heartbeat detector: missed is diff_remote_vs_local/diff_sent_stamp, where diff_sent_stamp is the machine's own arrival-time gap (protocol.c:66,80), not the base's heartbeat_ms/round-trip-echo count. A late-arriving prior message shrinks diff_sent_stamp, so missed balloons and PSTOP_MSG_LOST fires though nothing was lost. If delay stays constant while a real heartbeat is skipped, both deltas grow together and missed stays near 0, masking real loss. Fix: derive missed from a value immune to arrival jitter, e.g. heartbeat_ms or the round-trip echo the base used. [also at: pstop_c/pstop/src/pstop/protocol.c:81 - Machine operators now get spurious PSTOP_MSG_LOST stops after ordinary network jitter/delay recovery, even though no message was actually lost. diff_sent_stamp (line 66) is the real wall-clock gap between successive message PROCESSING times, not a fixed interval; a burst of quick arrivals right…]
Extended reasoning...
protocol_handle_message updates client->remote_data.last_timestamp=now (machine clock) and last_received_stamp=req->stamp (remote clock) on every processed message. check_timestamp (protocol.c:62-81) compares diff_received_stamp=|req->stamp-last_received_stamp| (remote clock delta) to diff_sent_stamp=|now-last_timestamp| (machine clock delta) and flags LOST when their difference/diff_sent_stamp exceeds max_missed_heartbeats+1. Example, heartbeat_ms=100: message N-1 is network-delayed 90ms so it's processed late; message N arrives on schedule 10ms after that. diff_sent_stamp=10, diff_received_stamp=100 (unaffected by transport delay, it's remote send-time gap). missed=90/10=9>threshold, LOST fires though nothing was lost. Reverse: remote genuinely skips one send but transport delay stays constant, so both deltas grow by the same skipped interval and missed stays ~0 — real loss goes undetected. Base algorithm compared only machine-clock-domain values…
Verification: normal. The new detector (protocol.c:62-82) computes missed = get_diff(diff_sent_stamp, diff_received_stamp) / diff_sent_stamp, with diff_sent_stamp = |now - last_timestamp| (line 64-66) being the machine's own inter-arrival gap (last_timestamp is set to now per processed message, line 159) and diff_received_stamp = |req->stamp - last_received_stamp| (line 62) the remote-clock gap. The…
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 2 advisory finding(s) below merit a look before merge.
Graphify review — findings
Rewrites lost-message detection in check_timestamp to compare the elapsed remote timestamp delta against locally elapsed time (via get_time_cb and a new get_diff helper) rather than dividing a raw timestamp gap by the heartbeat interval, flagging PSTOP_MSG_LOST when the two diverge by more than max_missed_heartbeats + 1. Changes the default protocol limits set by pstop_application_init from 0/0 to 1/1 heartbeats and adds an explicit set_protocol_limits call in the machine example. Adds a req_2_04_test suite to the requirements runner and updates existing protocol/requirement tests to advance current_time and set received_stamp so the new time-based check has consistent inputs.
Worth a look
- check_timestamp no longer rejects received_stamp ahead of last sent timestamp —
pstop_c/pstop/src/pstop/protocol.c:49· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Default protocol limits changed from 0/0 to 1/1 in pstop_application_init —
pstop_c/pstop/src/pstop/pstop_application.c:47· Escalate · medium · 2 independent checks- 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 — 128 functions depend on the 60 functions this change touches.
Health — this change adds coupling hotspots:
- new:
configure_app_defaults()— 33 callers, 7 callees - new:
send_bond()— 23 callers, 4 callees - new:
send_stop()— 18 callers, 4 callees - new:
send_ok()— 16 callers, 4 callees - new:
pstop_application_init()— 5 callers, 5 callees - new:
send_unbond()— 4 callers, 4 callees - new:
protocol_handle_message()— 1 callers, 7 callees - new:
main()— 0 callers, 34 callees - …and 37 more — each is listed as a finding
Verification — 128 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: 128 function(s) in the blast radius were not formally verified this run
· 1 grounded finding(s) anchored inline below; 44 more finding(s) on lines outside this diff (see the check run).
| // current clock is 300. This will indicate we missed too many | ||
| // messages and will return PSTOP_MSG_LOST. | ||
|
|
||
| static |
There was a problem hiding this comment.
req_2_04_1_test()
fans out to 7 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
There was a problem hiding this comment.
This pull request has been reviewed before and this review found new issues. Where they share a root cause, one fix may close them together.
Findings marked 🟡 are optional suggestions and need no follow-up push.
Still open from earlier reviews (2):
- 🔴
pstop_c/pstop/src/pstop/protocol.c:80—This regresses the missed-heartbeat detector: missed is diff_remote_vs_local/diff_sent_stamp, where diff_sent_stamp is… - 🔴
pstop_c/pstop/src/pstop/protocol.c:82—This PR edits pstop_c protocol/timestamp logic directly in this repo, which CLAUDE.md designates off-limits: pstop_c is…
If you have decided not to act on one of these findings, resolve its thread (a reply alone leaves it open) and the next review stops counting it. To review this commit again now, use Re-run on its "Claude Code Review" check.
| check_timestamp(const pstop_application_t *app, const protocol_data_t *client, const pstop_msg_t *req) | ||
| { | ||
| if(req->stamp <= client->last_received_stamp) { | ||
| return PSTOP_MSG_OUT_OF_ORDER; | ||
| } | ||
|
|
||
| if(req->received_stamp == client->last_timestamp) { | ||
| return PSTOP_OK; | ||
| } | ||
|
|
||
| // did the other end miss a message? | ||
| if(req->received_stamp < client->last_timestamp) { | ||
| uint64_t diff = client->last_timestamp - req->received_stamp; | ||
| // example of missed messages | ||
| // last sent stamp = 500, last received stamp = 500 | ||
| // now = 600, current request stamp = 900 | ||
| // diff = 100, remote diff = 400 | ||
| // diff should be close to the same if no messages have been lost | ||
|
|
||
| uint16_t missed = (uint16_t)(diff / client->heartbeat_ms); | ||
| uint64_t diff_received_stamp = get_diff(req->stamp, client->last_received_stamp); | ||
|
|
||
| if(missed >= (app_config->max_missed_heartbeats + 1U)) { | ||
| return PSTOP_MSG_LOST; | ||
| } | ||
| uint64_t now = app->env.get_time_cb(); | ||
|
|
||
| uint64_t diff_sent_stamp = get_diff(now, client->last_timestamp); | ||
|
|
||
| uint64_t diff_remote_vs_local = get_diff(diff_sent_stamp, diff_received_stamp); | ||
|
|
||
| if(diff_sent_stamp == 0U) { | ||
| // the chances of this happening are extremely unlikely. | ||
| // It would mean that the amount of time to run through processing | ||
| // a single message takes 0ms. | ||
|
|
||
| // If this does happen then the received timestamps should also be | ||
| // close to 0ms. Setting diff_sent_stamp = 1 will mean that the | ||
| // diff_remote_vs_local is the max number of missed hearbeats. | ||
| diff_sent_stamp = 1U; | ||
| } | ||
| else { | ||
| return PSTOP_MSG_OUT_OF_ORDER; | ||
| uint64_t missed = diff_remote_vs_local / diff_sent_stamp; | ||
| if(missed > (uint64_t)(app->app_config.max_missed_heartbeats + 1U)) { | ||
| return PSTOP_MSG_LOST; | ||
| } | ||
|
|
||
| return PSTOP_OK; |
There was a problem hiding this comment.
🔴 check_timestamp() no longer validates req->received_stamp (the remote's echo of our last sent stamp) after bonding, unlike check_counter() which still checks req->received_counter against msg_counter. A corrupted or forged received_stamp on the untrusted black channel is no longer rejected as PSTOP_MSG_OUT_OF_ORDER as long as req->stamp keeps advancing and the new heartbeat ratio stays under threshold. Fix: keep validating that req->received_stamp bounds/echoes client->last_timestamp (mirroring the received_counter check in check_counter), in addition to the new missed-heartbeat ratio math, so black-channel corruption of the echoed stamp is still caught for every message, not only at bond time (line 125).
Extended reasoning...
Base check_timestamp used req->received_stamp: if(req->received_stamp == client->last_timestamp) return OK; and rejected received_stamp > last_timestamp as OUT_OF_ORDER, catching an echo that could not legitimately have been sent yet. New check_timestamp (protocol.c:49-86) never reads req->received_stamp; it only compares req->stamp to last_received_stamp (line 51) and computes diff_received_stamp from req->stamp, not req->received_stamp (line 62). protocol_handle_message (line 118) is the only caller for bonded clients and does no other received_stamp check. So an attacker/corruption on the black channel can send any req->received_stamp (e.g. stale/garbage) every message; as long as req->stamp increases and roughly tracks time, the message passes check_counter and check_timestamp. check_counter (lines 37-39) still validates req->received_counter > msg_counter as OUT_OF_ORDER, so the asymmetry is new. No test in protocol_test.c or req_2_04_test.c sets an invalid received_stamp; all set it to the prior resp.stamp, so the regression is untested.
Verification: nit. The candidate reads the code correctly and the scenario is reachable. Base check_timestamp (git show 9d3b0e4:protocol.c) rejected req->received_stamp > client->last_timestamp as PSTOP_MSG_OUT_OF_ORDER (the else branch after the == and < cases). New check_timestamp (protocol.c:49-86) never references req->received_stamp at all — it reads only req->stamp (lines 51, 62) and the machine…
| pstop_application_set_hardware_status_cb(app, NULL); | ||
| pstop_application_set_log_cb(app, NULL); | ||
| pstop_application_set_protocol_limits(app, 0U, 0U, 1000U); | ||
| pstop_application_set_protocol_limits(app, 1U, 1U, 1000U); |
There was a problem hiding this comment.
🟡 (optional) Any downstream app that skips pstop_application_set_protocol_limits() now silently tolerates one lost STOP/OK message on the counter path, not just heartbeats, weakening default loss detection versus the base branch. pstop_application_init() changed the default max_lost_messages from 0 to 1; check_counter() in protocol.c:34 flags PSTOP_MSG_LOST only when counter gap exceeds max_lost_messages+1, so a gap of 2 (one message actually lost) now passes silently where it used to trip immediately. This bump is unrelated to the timestamp/heartbeat rework the PR is about and has no accompanying test coverage or migration note for the counter axis. …
Extended reasoning...
…Fix: keep max_lost_messages at 0 by default (or otherwise preserve zero-tolerance counter-loss detection) and bump only max_missed_heartbeats, since the PR's stated purpose is heartbeat timing, not counter-gap tolerance.
protocol.c check_counter(): line34 if((req->counter - client->remote_data.last_received_counter) > (app_config->max_lost_messages + 1U)) return PSTOP_MSG_LOST;. Base default was max_lost_messages=0, so threshold is >1: a counter jump of 2 (i.e. exactly one message dropped on the wire) triggers LOST right away. pstop_application.c:47 now calls pstop_application_set_protocol_limits(app,1U,1U,1000U) for every app using the default init path, so threshold becomes >2: a jump of 2 (one lost message) no longer triggers LOST; only losing 2+ messages does. Same widened tolerance applies to the received_counter path (protocol.c:40, >= max_lost_messages+1U). No test in this diff exercises the default-init path for the counter axis; machine_test.c and the requirements tests all call pstop_application_set_protocol_limits explicitly with their own values, so this…
Verification: nit. The mechanism is real and reachable. pstop_application.c:47 changes the default from pstop_application_set_protocol_limits(app, 0U, 0U, 1000U) to (app, 1U, 1U, 1000U). protocol.c:34 (check_counter, untouched by the diff) trips PSTOP_MSG_LOST only when (req->counter - client->remote_data.last_received_counter) > (app_config->max_lost_messages + 1U). Base default max_lost_messages=0…
|
thanks for the test fixes, but I can't approve the timestamp check as is, it will cause false stops. This divides by the local gap since our last reply, so two heartbeats arriving close together blow the ratio up. I've see 400-550 ms of jitter on every soak test I've run, and the DERP mirror bunches packets on purpose. Suggestions:
|
There was a problem hiding this comment.
Graphify reviewed this change.
Looks safe to merge — no coupling regressions and no blocking issues, checked against the code graph (not a self-assessment).
Formal verification. No changes could be formally verified in this run.
Graphify review — findings
No blocking issues surfaced.
Analysis details — impact, health, verification
Impact & health
Graphify review
Impact — 128 functions depend on the 60 functions this change touches.
Health — this change adds coupling hotspots:
- new:
configure_app_defaults()— 33 callers, 7 callees - new:
send_bond()— 23 callers, 4 callees - new:
send_stop()— 18 callers, 4 callees - new:
send_ok()— 16 callers, 4 callees - new:
pstop_application_init()— 5 callers, 5 callees - new:
send_unbond()— 4 callers, 4 callees - new:
protocol_handle_message()— 1 callers, 7 callees - new:
main()— 0 callers, 34 callees - …and 37 more — each is listed as a finding
Verification — 128 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: 128 function(s) in the blast radius were not formally verified this run
Formal verification
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: unsupported parameter type(s)
Could not verify: Could not verify check\_timestamp.
The verifier did not have enough to check check\_timestamp, 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: unsupported return type: pstop_error_t
Could not verify: Could not verify protocol\_handle\_message.
The verifier did not have enough to check protocol\_handle\_message, 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: unsupported return type: pstop_error_t
Could not verify: Could not verify pstop\_application\_init.
The verifier did not have enough to check pstop\_application\_init, 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: unsupported return type: void
Could not verify: Could not verify test\_protocol\_bond\_correct\_timestamp.
The verifier did not have enough to check test\_protocol\_bond\_correct\_timestamp, 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: unsupported return type: void
Could not verify: Could not verify test\_protocol\_bond\_invalid\_echo\_counter.
The verifier did not have enough to check test\_protocol\_bond\_invalid\_echo\_counter, 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: unsupported return type: void
Could not verify: Could not verify test\_protocol\_bond\_missing\_sent\_messages.
The verifier did not have enough to check test\_protocol\_bond\_missing\_sent\_messages, 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: unsupported return type: void
Could not verify: Could not verify test\_protocol\_bond\_then\_unbond.
The verifier did not have enough to check test\_protocol\_bond\_then\_unbond, 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: unsupported return type: void
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: unsupported parameter type(s)
Could not verify: Could not verify req\_2\_03\_1\_test.
The verifier did not have enough to check req\_2\_03\_1\_test, 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: unsupported return type: void
Could not verify: Could not verify req\_2\_03\_2\_test.
The verifier did not have enough to check req\_2\_03\_2\_test, 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: unsupported return type: void
· 1 grounded finding(s) anchored inline below; 44 more finding(s) on lines outside this diff (see the check run).
| // current clock is 300. This will indicate we missed too many | ||
| // messages and will return PSTOP_MSG_LOST. | ||
|
|
||
| static |
There was a problem hiding this comment.
req_2_04_1_test()
fans out to 7 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
There was a problem hiding this comment.
Code review found no new issues
No new issues were found in this update; 4 findings from earlier reviews are still open above.
Still open from earlier reviews (4):
- 🔴
pstop_c/pstop/src/pstop/protocol.c:80—This regresses the missed-heartbeat detector: missed is diff_remote_vs_local/diff_sent_stamp, where diff_sent_stamp is… - 🔴
pstop_c/pstop/src/pstop/protocol.c:82—This PR edits pstop_c protocol/timestamp logic directly in this repo, which CLAUDE.md designates off-limits: pstop_c is… - 🔴
pstop_c/pstop/src/pstop/protocol.c:85—check_timestamp() no longer validates req->received_stamp (the remote's echo of our last sent stamp) after bonding, unl… - Also unresolved: 1 minor or pre-existing.
If you have decided not to act on one of these findings, resolve its thread (a reply alone leaves it open) and the next review stops counting it. To review this commit again now, use Re-run on its "Claude Code Review" check.
2 participants
Heartbeat messages (OK, STOP) should be sent from the remote at a semi-consistent interval.
For example, if we are sending and receiving messages with timestamps like this:
last_sent_timestamp (current time) = 100, last_received_timestamp = 110
last_sent_timestamp (current time) = 200, last_received_timestamp = 210
last_sent_timestamp (current time) = 300, current message timestamp = 610
This shows that the remote has missed some heartbeats, since the timestamps should increment by a similar amount.
Migration Guide
Pstop application code might need to adjust the number of missed messages allowed.
This can be done with the following function.
void pstop_application_set_protocol_limits(pstop_application_t *app,
uint16_t max_lost_messages, uint16_t max_missed_heartbeats, uint32_t stop_ok_delay_ms);