work-unit: checkpoint storage — segment hardening and invariants #1548

Activity

1. strawgate

   added

   bugSomething isn't workingSomething isn't working

   productionRequired for production readinessRequired for production readiness

   P1: highSignificant user-visible bug or major UX breakageSignificant user-visible bug or major UX breakage

   work-unitScheduling ticket for one agent runScheduling ticket for one agent run

   architectureSystemic design improvements that eliminate classes of bugsSystemic design improvements that eliminate classes of bugs

   component:processor/checkpointCheckpoint persistence, replay, and checkpoint protocol behaviorCheckpoint persistence, replay, and checkpoint protocol behavior

   on Apr 7, 2026
2. github-actions commented on Apr 7, 2026

   

   github-actionsBot

   on Apr 7, 2026 – with GitHub Actions

   Contributor

   More actions

   tl;dr: Outcome A — ready for implementation. The remaining checkpoint segment work is mechanical: harden segment.rs error classification/write limits, add regression tests for each failure mode from #1211, and add explicit segment-recovery invariant coverage wiring for #1109.

   Recommendation

   Proceed with a single focused PR against crates/logfwd-io/src/segment.rs (+ tests + verification contract update). The current implementation already fixes some #1211 items, but still has concrete silent-failure paths and missing invariant coverage seams.

   Findings (evidence)

   1. OS/permission errors are still collapsed into NotASegment and then ignored in recovery

      • crates/logfwd-io/src/segment.rs:209, :219, :244 map errors to SegmentStatus::NotASegment(...).
      • crates/logfwd-io/src/segment.rs:735-740 only warns and ignores NotASegment entries.
      • Result: unreadable/corruptly-accessed .lchk files can be silently skipped during recovery.

   2. SegmentWriter::create still accepts arbitrary header values

      • Signature: crates/logfwd-io/src/segment.rs:431 — pub fn create(dir: &Path, header: SegmentHeader) -> io::Result(Self).
      • open() enforces version compatibility at parse time; this API still allows writing headers future open-path may reject.

   3. Read/write size limit mismatch remains

      • Read cap exists: MAX_READ_DATA_SIZE at crates/logfwd-io/src/segment.rs:315 and checked in read_batches() (:318-327).
      • SegmentWriter::append (:463-489) does not pre-check cumulative segment payload against this same cap.

   4. Unsupported header versions are still treated as NotASegment

      • Header parse failures flow to NotASegment at crates/logfwd-io/src/segment.rs:242-245.
      • During recovery this gets ignored (:735-740) instead of an explicit corrupt/unsupported segment error classification.

   5. Invariant seam coverage for segment recovery is not explicitly tracked in Kani boundary contract

      • dev-docs/verification/kani-boundary-contract.toml has required/recommended seams, but no entry for crates/logfwd-io/src/segment.rs.

   6. Open PR in adjacent integration surface

      • #1550 (fix(stats): preserve structured input accounting) touches input/framed/pipeline paths; low direct overlap with segment.rs, but rebase/conflict risk exists if this work also modifies pipeline wiring.

   Verification

   I ran:

   cargo test -p logfwd-io segment -- --nocapture

   Observed:

   • segment unit tests passed (15 passed, 0 failed), including:
     • corrupt_data_size_prevented_from_oom
     • truncated_segment_returns_invalid_data
     • recovery_deletes_incomplete
   • This confirms baseline behavior is stable before applying the remaining hardening changes.

   Detailed Action Plan (mechanical spec)

   1) Files to modify

   File	Current symbol(s)	Exact change
   crates/logfwd-io/src/segment.rs	enum SegmentStatus (~175+), SegmentFile::open (:206+)	Add explicit IO/permission classification (e.g. IoError { path, error }) and route metadata/open/read failures there; keep true non-segment magic in NotASegment.
   crates/logfwd-io/src/segment.rs	SegmentWriter::create (:431)	Enforce header invariants at write-time (version == SEGMENT_VERSION, allowed flags mask). Return io::ErrorKind::InvalidInput on invalid header values.
   crates/logfwd-io/src/segment.rs	SegmentWriter::append (:463) + MAX_READ_DATA_SIZE (:315)	Add pre-write size guard so cumulative data_size + ipc_buf.len() never exceeds read-side cap; fail write early with explicit InvalidData/InvalidInput error text.
   crates/logfwd-io/src/segment.rs	recover_segments (:686+)	Treat new IoError as hard recovery error (return Err(...)), and classify unsupported-version header parse as corrupt/unsupported-segment (not silent ignore).
   crates/logfwd-io/src/segment.rs tests (:789+)	Existing unit test module	Add regression tests listed below.
   dev-docs/verification/kani-boundary-contract.toml	seam list	Add crates/logfwd-io/src/segment.rs seam status (recommended initially if no immediate pure extraction, or required if reducer/proofs are added in same PR).

   2) Tests to write (same file unless noted)

   1. recovery_permission_error_is_hard_failure

      • Pattern: existing recover_segments tests.
      • Assert: unreadable .lchk returns Err, not silent skip.

   2. create_rejects_unsupported_header_version

      • Assert: SegmentWriter::create with bad version fails with InvalidInput.

   3. create_rejects_unknown_flags

      • Assert: unsupported flags rejected at create-time.

   4. append_rejects_payload_exceeding_max_read_data_size

      • Assert: writer refuses append once cumulative payload crosses cap.

   5. unsupported_segment_version_classified_non_silent

      • Craft .lchk with valid magic but unsupported version.
      • Assert recovery does not route through silent NotASegment path.

   3) Invariant coverage follow-through for #1109

   If done in same PR: extract a small pure recovery-decision helper (classification + next-id computation) from recover_segments and add bounded Kani proofs for:

   • next_segment_id == max_seen_id + 1 for non-empty sets
   • next_segment_id == 1 when none
   • no replay of incomplete/corrupt classes

   If not done in same PR: keep code changes above + add explicit follow-up issue linked from this work-unit.

   4) Verification command set

   cargo test -p logfwd-io segment -- --nocapture
   python3 scripts/verify_kani_boundary_contract.py
   just kani-boundary
   just ci

   Related Items

   Type	Link	Relevance
   Issue	#1548	Work-unit umbrella
   Issue	#1211	Segment hardening bug list this plan closes
   Issue	#1109	Invariant/proof coverage requirement
   PR	#1550	Nearby integration surface currently open
   File	crates/logfwd-io/src/segment.rs	Primary implementation target
   File	dev-docs/verification/kani-boundary-contract.toml	Verification contract update target

   Note

   🔒 Integrity filtering filtered 7 items

   Integrity filtering activated and filtered the following items during workflow execution.
   This happens when a tool call accesses a resource that does not meet the required integrity or secrecy level of the workflow.

   • issue:work-unit: checkpoint storage — segment hardening and invariants #1548 (issue_read: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".)
   • issue:fix(checkpoint): segment storage has panic paths, OOM vector, and silent error masking #1211 (issue_read: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".)
   • issue:arch: property-based tests for checkpoint state machine at-least-once invariant #1109 (issue_read: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".)
   • issue:phase: checkpoint step — Phase 1: segment format, writer, reader, recovery #1005 (issue_read: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".)
   • pr:feat: checkpoint segment format — writer, reader, recovery (Phase 1) #1120 (pull_request_read: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".)
   • resource:search_pull_requests (search_pull_requests: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".)
   • pr:fix(stats): preserve structured input accounting #1550 (pull_request_read: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".)

   ---

   What is this? | From workflow: Issue Triage

   Give us feedback! React with 🚀 if perfect, 👍 if helpful, 👎 if not.
3. strawgate commented on Apr 7, 2026

   

   strawgate

   on Apr 7, 2026

   OwnerAuthor

   More actions

   Execution Owner: Codex

   Objective
   Complete #1548 by fixing checkpoint segment safety bugs (#1211) and encoding checkpoint invariants (#1109).

   Scope lock

   • In scope: checkpoint segment read/write/recovery correctness and proof/test invariants.
   • Out of scope: unrelated output delivery semantics and broad runtime redesign.

   Implementation steps (in order)

   1. Read context: AGENTS.md, DEVELOPING.md, dev-docs/VERIFICATION.md, issue bodies fix(checkpoint): segment storage has panic paths, OOM vector, and silent error masking #1211 and arch: property-based tests for checkpoint state machine at-least-once invariant #1109.
   2. Enumerate and reproduce each fix(checkpoint): segment storage has panic paths, OOM vector, and silent error masking #1211 failure class (panic paths, OOM vectors, silent masking) with targeted tests.
   3. Implement minimal safe fixes in segment parsing/recovery/write-path validation.
   4. Encode invariants from arch: property-based tests for checkpoint state machine at-least-once invariant #1109 using appropriate tests/proofs (Kani/proptest where bounded and valuable).
   5. Update verification docs/config if proof boundaries or required checks change.

   Required verification

   • cargo test -p logfwd-io
   • cargo test -p logfwd
   • just test
   • just ci
   • just lint-all

   PR requirements

   • Title: fix(checkpoint): segment safety hardening + invariants coverage (#1548)
   • Close keywords: Fixes #1211, Fixes #1109, Refs #1548.
   • PR body must include a matrix mapping each fix(checkpoint): segment storage has panic paths, OOM vector, and silent error masking #1211 bullet to its fix/test.

   Done checklist

   • no panic/OOM/silent-mask paths remain in segment recovery flow
   • invariants are encoded and enforced by tests/proofs
   • docs/verification boundaries updated
   • required verification commands pass
4. strawgate commented on Apr 7, 2026

   

   strawgate

   on Apr 7, 2026

   OwnerAuthor

   More actions

   Cloud task launched (Codex queue): task_e_69d57804fd94832e8998f2a1b784c00f (3 attempts).\nhttps://chatgpt.com/codex/tasks/task_e_69d57804fd94832e8998f2a1b784c00f
5. strawgate

   added 2 commits that reference this issue on Apr 7, 2026

   fix(core): harden checkpoint segment parsing invariants (#1548)

   7e80fa3

   fix(core): harden checkpoint segment parsing invariants (#1548) (#1569)

   ...

   bffa9e7
6. strawgate commented on Apr 8, 2026

   

   strawgate

   on Apr 8, 2026

   OwnerAuthor

   More actions

   Resolved by PR #1569 with linked leaf concerns addressed (#1211, #1109). Checkpoint segment hardening and invariants landed.
7. strawgate

   closed this as completedon Apr 8, 2026