Context
#50 (trainee packets, ADR 0015) verifies each packet's documents against the enrollment's pin history: the lifecycle events' version changes define which versions were ever pinned, each signoff and phase event names a pinned version with the packet's label for it, and each phase event's version is the one its named epoch reached (docs/formats/trainee-packet.md, verification check 8). Codex's review of c19460a raised two findings that these checks are set membership over the history, not position on its timeline:
- Signoffs. A rehashed packet can relabel a signoff recorded under version 1 as a version-2 task when the enrollment later moved to version 2, because version 2 appears somewhere in the pin history.
task_signoff stores no epoch; the trigger task_signoff_takes_a_pinned_task (migration 0013) binds the task to the pin current at insert, so the property to verify is temporal: the signoff's version was the pin at signed_at.
- Phase events. A phase event naming a recorded epoch verifies even when its
effective_at and recorded_at precede that version change's occurred_at. Production refuses this (lifecycle::record_phase_event: "a phase event cannot take effect before its epoch opened", effective < epoch_opened is refused); the verifier does not mirror it.
Proposed design
Extend PinHistory in packet_verify.rs with each version change's occurred_at, and check position on the timeline with second-granularity tolerance, since every instant the packet carries is a unix second and a change and an act in the same second are legitimately unordered:
pinned_during(t): the pin after all changes with occurred_at < t, plus the target of every change with occurred_at == t. A signoff's program_version must be in pinned_during(signed_at).- A phase event under epoch
E (a version change at instant o, closed by the next change at n if any) must have recorded_at >= o, effective_at >= o, and recorded_at <= n; a phase event under the original pin (null epoch) must have recorded_at <= o of the first change.
- Findings are
DocumentPinHistory; the format document's pin-history paragraph and check 8 state the timeline rules.
Tests: forge a signoff relabelled to a version pinned only later, a phase event effective before its epoch opened, and one recorded under the original pin after the first change; the genuine packet, including a same-second change and act, must still verify.
Raised by Codex on #50 (review threads r3909122078 and r3909122081) after the set-membership checks landed in c19460a; tracked here so #50 merges with the format's stated checks complete. Refs #48, #44.
Context
#50 (trainee packets, ADR 0015) verifies each packet's documents against the enrollment's pin history: the lifecycle events' version changes define which versions were ever pinned, each signoff and phase event names a pinned version with the packet's label for it, and each phase event's version is the one its named epoch reached (
docs/formats/trainee-packet.md, verification check 8). Codex's review of c19460a raised two findings that these checks are set membership over the history, not position on its timeline:task_signoffstores no epoch; the triggertask_signoff_takes_a_pinned_task(migration 0013) binds the task to the pin current at insert, so the property to verify is temporal: the signoff's version was the pin atsigned_at.effective_atandrecorded_atprecede that version change'soccurred_at. Production refuses this (lifecycle::record_phase_event: "a phase event cannot take effect before its epoch opened",effective < epoch_openedis refused); the verifier does not mirror it.Proposed design
Extend
PinHistoryinpacket_verify.rswith each version change'soccurred_at, and check position on the timeline with second-granularity tolerance, since every instant the packet carries is a unix second and a change and an act in the same second are legitimately unordered:pinned_during(t): the pin after all changes withoccurred_at < t, plus the target of every change withoccurred_at == t. A signoff'sprogram_versionmust be inpinned_during(signed_at).E(a version change at instanto, closed by the next change atnif any) must haverecorded_at >= o,effective_at >= o, andrecorded_at <= n; a phase event under the original pin (nullepoch) must haverecorded_at <= oof the first change.DocumentPinHistory; the format document's pin-history paragraph and check 8 state the timeline rules.Tests: forge a signoff relabelled to a version pinned only later, a phase event effective before its epoch opened, and one recorded under the original pin after the first change; the genuine packet, including a same-second change and act, must still verify.
Raised by Codex on #50 (review threads r3909122078 and r3909122081) after the set-membership checks landed in c19460a; tracked here so #50 merges with the format's stated checks complete. Refs #48, #44.