mirror of
https://github.com/openglow-org/forgefirm.git
synced 2026-10-19 02:51:42 -07:00
Rule 3 of the header says a sender change closes the window and a
reconnected client must re-arm. The harness does not walk the sequence
on from there, a new sender's soft reset of the held job, as a session
of its own (commit 09cf924 removed test_sender_change_then_reset), and
the header did not say where each assertion of that sequence lives.
The disarm and the latch relock at the change are laser_arm_test.c
case H (glowforge_laser.c: the client generation changing mid-cycle
enqueues the feed hold and disarms). The soft reset of the held job is
the core's reset from a completed hold, which session
hold-reset-restart walks under rule 10 with more asserted than the
removed case had: the reset banner, Idle with no alarm, and the
position kept. The hold's origin does not reach the reset path
(driver.c driverReset disarms and resets the stream whatever held the
job, and gflaser_disarm is idempotent), so the sender-change variant
is a permutation of that one branch, and this repository keeps one
proof per rule. Rule 3 now names both holders.
Proof: header text only, no behavior change. python3 -B -m py_compile
and pyflakes are clean on scripts/bench/laser_lifecycle_test.py, and
the harness passes whole against the native null-sink build of the
driver at badc832 (-DGFMCODE_WAIT_S=5.0), hold-reset-restart among
its sessions. The harness runs in grblHAL-glowforge CI (python3
forgefirm/scripts/bench/laser_lifecycle_test.py build/grblHAL_glowforge).
Acceptance: none; the header docstring of a harness outside every
covers map.