Skip to content

Plan: Implement shared download primitives (10.1.2) - #199

Draft
leynos wants to merge 2 commits into
mainfrom
10-1-2-shared-download-primitives
Draft

Plan: Implement shared download primitives (10.1.2)#199
leynos wants to merge 2 commits into
mainfrom
10-1-2-shared-download-primitives

Conversation

@leynos

@leynos leynos commented Aug 16, 2026

Copy link
Copy Markdown
Owner

Summary

Draft ExecPlan for roadmap item 10.1.2 — pinned source URLs, checksum verification, resumable transfers, and archive extraction (.gz, .bz2, .xz, .tar) in chutoro-bench-datasets.

This is a plan only. No implementation has begun, and none will until the plan is approved.

How the plan was produced

A six-lens design review stress-tested the design before any code was written, and every load-bearing claim was checked against the working tree or live upstreams rather than assumed. Eight checks changed the design:

Check Result Consequence for the plan
Do real upstreams honour Range? SIFT1M, GloVe-200 and the in-repo MNIST mirror all return 206, correct Content-Range, Accept-Ranges: bytes, strong ETags, no Content-Encoding Resume has a working primary path, not just a fallback
Can sha2 0.10 persist hasher state? NoSerializableState arrived in digest 0.11 Digests are chunked; otherwise every cross-process resume re-reads the whole prefix
Does cap-std offer file locking? No — only into_std(), which returns the std::fs::File Whitaker bans here Locking via rustix::fs::flock on the borrowed descriptor
Is Checksum inhabited? No — its sole variant is behind #[cfg(any())] SourceSpec.checksum provably can never hold a value; migration is in-crate only
How much room is in RecipeError? Exactly 32 bytes, payload budget already fully spent Every rich failure payload must be boxed
Do the datasets need .bz2/.xz? No — but canonical GloVe ships .zip, which is out of scope Both gated off by default; .zip raised as a note against 10.3.10
Is there a supply-chain gate? None — no deny.toml, no advisory check in any of eight workflows A prerequisite stage adds one
Is make verus blocking? Yes on every PR; Kani is nightly only Raises the bar for adding a proof

Design decisions worth reviewer attention

  1. HTTP protocol types stay out of the domain layer. The adapter classifies a ranged read into a transport-neutral RangeOutcome; the domain parses header values but never branches on a status code. Without this, roadmap 10.1.4's object_store adapter would have to fabricate HTTP status codes for the domain to inspect.
  2. RecipeContext gains a builder accessor. As originally designed the streaming ports would have shipped complete, verified, and unreachable from DatasetRecipe::fetch. RecipeContext::new keeps its exact three-argument signature, so all eight existing call sites are untouched.
  3. Option<Checksum> becomes a mandatory Integrity field with a greppable Unpinned { justification } escape hatch, and size_bytes lives in the same variant as checksum so the length-before-digest retry rule is true by construction.
  4. The signature adapter defers to 10.1.6. ANN-Benchmarks publishes neither checksums nor signatures, and no dataset in §10.3 ships one, so an adapter would have zero producers and zero consumers. The port and Integrity::Signed still ship, so verification stays expressible.
  5. One Verus proof, not two — and on a different target. The originally proposed entry-path and resume-sequence lemmas were cut as restatements of assumed properties. The replacement proves the jitter bound (sample * span) >> 64 <= span: nonlinear, unbounded in both operands, unsamplable by proptest and infeasible for Kani. A proptest state machine over attempt sequences covers the resume property against the real code.
  6. Delivered as three sequential PRs under one roadmap checkbox, calibrated against 10.1.1 — a third of this scope, which took nine milestones and eleven review rounds.

Validation

make markdownlint (0 errors, including the spelling gate) and make nixie both pass. No source code is touched.

References

  • Roadmap item 10.1.2 in docs/roadmap.md §10.1
  • Design source of truth: docs/benchmark-dataset-retrieval.md §3.2
  • Prior milestone: docs/execplans/10-1-1-chutoro-bench-datasets-and-dataset-recipe-trait.md
  • Existing decisions amended by this plan: docs/adr-004-bench-dataset-recipe-trait.md
  • Lody session: https://lody.ai/leynos/sessions/88ad3710-0b7c-4449-aa94-d9cfa7359ca1

🤖 Generated with Claude Code

Summary by Sourcery

Document the proposed implementation plan for trusted, resumable benchmark dataset downloads and bounded archive extraction without adding implementation code.

Enhancements:

  • Add a draft execution plan for shared benchmark-dataset download primitives covering integrity pinning, resumable transfers, and archive extraction.
  • Document staged delivery, architectural boundaries, validation strategy, dependency choices, and security and reliability constraints for roadmap item 10.1.2.

Documentation:

  • Index the new shared download primitives execution plan in the documentation contents.

@coderabbitai

coderabbitai Bot commented Aug 16, 2026

Copy link
Copy Markdown
Contributor

Important

Review skipped

Draft detected.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: d531f8c0-dbb9-4786-a3b3-b1940d33cca2

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

  • 🔍 Trigger review

Warning

Your free Security trial is over. An organization admin can activate billing to continue.


Comment @coderabbitai help to get the list of available commands.

@sourcery-ai

sourcery-ai Bot commented Aug 16, 2026

Copy link
Copy Markdown

Reviewer's Guide

Adds a new ExecPlan document for roadmap item 10.1.2 describing shared download primitives for benchmark datasets and wires it into the documentation contents index; no code changes, only documentation for a multi-stage implementation plan.

Sequence diagram for resumable verified download via RangeFetcher and PartialStore

sequenceDiagram
    actor DatasetRecipe
    participant RecipeContext
    participant TransferPorts
    participant DownloadDomain
    participant RangeFetcher
    participant PartialStore
    participant PartialSlot

    DatasetRecipe->>RecipeContext: transfer()
    RecipeContext-->>DatasetRecipe: TransferPorts

    DatasetRecipe->>DownloadDomain: download_verified(TransferPorts, DownloadRequest)

    DownloadDomain->>PartialStore: acquire(CacheKey)
    PartialStore-->>DownloadDomain: PartialSlot

    DownloadDomain->>PartialSlot: staged_len()
    DownloadDomain->>PartialSlot: expectation()
    DownloadDomain->>DownloadDomain: decide_resume(ResumeContext)

    alt ResumeFrom
      DownloadDomain->>RangeFetcher: open_range(RangeRequest)
      RangeFetcher-->>DownloadDomain: RangeResponse
      DownloadDomain->>PartialSlot: append(&[u8])
    else DiscardAndRestart
      DownloadDomain->>PartialSlot: reset(0, StagedExpectation)
      DownloadDomain->>RangeFetcher: open_range(RangeRequest)
      RangeFetcher-->>DownloadDomain: RangeResponse
      DownloadDomain->>PartialSlot: append(&[u8])
    end

    DownloadDomain->>PartialSlot: commit(ObjectKey)
    DownloadDomain-->>DatasetRecipe: DownloadOutcome
Loading

File-Level Changes

Change Details Files
Register the new 10.1.2 execution plan in the documentation table of contents so it is discoverable alongside existing ExecPlans.
  • Insert a bullet entry referencing the new shared download primitives ExecPlan under the ExecPlans section.
  • Describe briefly that the plan covers pinned sources, checksum verification, resumable transfers, and archive extraction.
docs/contents.md
Introduce a comprehensive ExecPlan document for roadmap item 10.1.2 detailing constraints, risks, staged work plan, design decisions, interfaces, and validation strategy for shared download primitives in chutoro-bench-datasets.
  • Create a new markdown file that explains purpose and big-picture outcomes for shared download primitives, including pinning, resumable downloads, and archive extraction.
  • Document hard constraints, tolerances, risks, progress milestones, and surprises/discoveries affecting the design.
  • Record a detailed decision log about domain vs adapter boundaries, integrity modeling, error budget, digest strategy, resume behavior, archive policy, and proof strategy.
  • Lay out staged implementation work (supply chain, integrity domain, transfer logic and adapters, archive handling, documentation) and associated validation and acceptance criteria.
  • Specify planned Rust interfaces, feature flags, and dependencies for future implementation of integrity, transfer, and archive primitives.
  • Affirm that this PR is plan-only with no source code modifications and validated via markdownlint and nixie.
docs/execplans/10-1-2-shared-download-primitives.md

Tips and commands

Interacting with Sourcery

  • Trigger a new review: Comment @sourcery-ai review on the pull request.
  • Continue discussions: Reply directly to Sourcery's review comments.
  • Generate a GitHub issue from a review comment: Ask Sourcery to create an
    issue from a review comment by replying to it. You can also reply to a
    review comment with @sourcery-ai issue to create an issue from it.
  • Generate a pull request title: Write @sourcery-ai anywhere in the pull
    request title to generate a title at any time. You can also comment
    @sourcery-ai title on the pull request to (re-)generate the title at any time.
  • Generate a pull request summary: Write @sourcery-ai summary anywhere in
    the pull request body to generate a PR summary at any time exactly where you
    want it. You can also comment @sourcery-ai summary on the pull request to
    (re-)generate the summary at any time.
  • Generate reviewer's guide: Comment @sourcery-ai guide on the pull
    request to (re-)generate the reviewer's guide at any time.
  • Resolve all Sourcery comments: Comment @sourcery-ai resolve on the
    pull request to resolve all Sourcery comments. Useful if you've already
    addressed all the comments and don't want to see them anymore.
  • Dismiss all Sourcery reviews: Comment @sourcery-ai dismiss on the pull
    request to dismiss all existing Sourcery reviews. Especially useful if you
    want to start fresh with a new review - don't forget to comment
    @sourcery-ai review to trigger a new review!

Customizing Your Experience

Access your dashboard to:

  • Enable or disable review features such as the Sourcery-generated pull request
    summary, the reviewer's guide, and others.
  • Change the review language.
  • Add, remove or edit custom review instructions.
  • Adjust other review settings.

Getting Help

codescene-access[bot]

This comment was marked as outdated.

Draft the execution plan for roadmap item 10.1.2: pinned source URLs,
checksum verification, resumable transfers, and archive extraction in
`chutoro-bench-datasets`.

The plan was produced with a six-lens design review and validated against
the working tree and live upstreams rather than assumption. Eight empirical
checks shaped it:

- Every upstream the project actually uses honours HTTP range requests with
  strong validators and no content coding, so resume has a working primary
  path rather than only a fallback.
- `sha2 0.10` cannot persist hasher midstate, so a flat digest would force a
  full prefix re-read on every cross-process resume. Digests are chunked.
- `cap-std` exposes no file locking, and `into_std()` returns the
  `std::fs::File` that Whitaker bans in this crate, so locking goes through
  `rustix::fs::flock` on the borrowed descriptor.
- `Checksum` is currently uninhabited, so `SourceSpec.checksum` is a field
  that can provably never hold a value.
- `RecipeError` is exactly 32 bytes with its payload budget already spent, so
  every rich failure payload must be boxed.
- No roadmap dataset ships `.bz2` or `.xz`, while canonical GloVe ships
  `.zip`, which is outside the item's declared format list.
- The repository has no advisory or licence gate, while this item roughly
  doubles the crate's dependency count.
- `make verus` is a blocking pull-request gate whereas Kani is nightly only.

Notable design decisions recorded in the plan: HTTP protocol types stay out
of the domain layer so roadmap 10.1.4's object-store adapter need not
fabricate status codes; `RecipeContext` gains a builder accessor so the
streaming ports are reachable from a recipe at all; `Option<Checksum>`
becomes a mandatory `Integrity` field with a greppable unpinned escape
hatch; the signature adapter defers to 10.1.6 since no dataset in the
backlog ships a signature; and the two originally proposed Verus proofs are
replaced by one proof on the jitter arithmetic plus a proptest state machine
over attempt sequences.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@leynos
leynos force-pushed the 10-1-2-shared-download-primitives branch from c2911b1 to b77564e Compare August 16, 2026 01:28
codescene-access[bot]

This comment was marked as outdated.

codescene-access[bot]

This comment was marked as outdated.

The first draft said "Kani is nightly only". Issue #202 establishes the
sharper position: `make kani` is invoked by no workflow at all, and
`make kani-full` runs only post-merge on `main` and currently does not
complete owing to CBMC budget exhaustion.

The verification story is unchanged — two Kani harnesses and one Verus
proof — but the plan now states plainly that the harnesses are developer
tooling rather than a merge gate, must be run by hand at each stage
boundary, and that a green pull request is not evidence they passed.

Also records that the plan's findings were filed as issues #208 to #217.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
codescene-access[bot]

This comment was marked as outdated.

@codescene-access codescene-access Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No quality gates enabled for this code.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant