diff --git a/docs/assurance.md b/docs/assurance.md index 20473a5..88e3fd7 100644 --- a/docs/assurance.md +++ b/docs/assurance.md @@ -8,13 +8,13 @@ A claim is *evidenced* when its layer runs in CI, *planned* when a plan phase sc ## Summary -The register holds 209 claims: 196 evidenced, 0 planned, and 13 not verified. It maps 87 guidelines from 5 guides; 64 list claims and 23 are exempt. +The register holds 210 claims: 197 evidenced, 0 planned, and 13 not verified. It maps 87 guidelines from 5 guides; 64 list claims and 23 are exempt. | Layer | Evidenced | Planned | Not verified | | --- | ---: | ---: | ---: | | example test | 124 | 0 | 0 | | property test | 22 | 0 | 0 | -| stateful model | 24 | 0 | 0 | +| stateful model | 25 | 0 | 0 | | Quint model with production trace replay | 14 | 0 | 0 | | Lean proof with differential test | 8 | 0 | 0 | | differential oracle | 4 | 0 | 0 | @@ -117,8 +117,8 @@ Each claim holds only while its listed assumptions hold. | `media-tools` | yt-dlp, ffmpeg, and whisper.cpp report metadata faithfully and honor the arguments they are given. | 11 | | `provider-behaviour` | Third-party providers behave as their observed contracts describe. | 31 | | `plugin-trusted` | Source plugins are trusted in-process code; portable execution contains ordinary failures, not hostile code. | 13 | -| `github-api` | GitHub's REST, GraphQL, and Actions APIs report repository, run, and Release state truthfully. | 48 | -| `github-enforcement` | GitHub enforces rulesets, environments, concurrency groups, immutable Releases, and token permissions as configured. | 42 | +| `github-api` | GitHub's REST, GraphQL, and Actions APIs report repository, run, and Release state truthfully. | 49 | +| `github-enforcement` | GitHub enforces rulesets, environments, concurrency groups, immutable Releases, and token permissions as configured. | 43 | | `sigstore` | Sigstore and `gh attestation verify` verify attestation bundles correctly. | 2 | | `npm-registry` | The npm registry enforces version immutability, trusted publishing, and provenance as documented. | 16 | | `vercel` | Vercel builds and serves deployments as its project settings and APIs report. | 7 | @@ -1623,7 +1623,7 @@ No semantic provider operation or gateway call accepts caller-selected provider - Assumptions: `provider-behaviour` - Not verified: No property test covers this law yet; only the enumerated example cases are checked. -### `release` (32 claims) +### `release` (33 claims) #### `release-trigger-exact-tag-push-only` @@ -1917,7 +1917,7 @@ A completed Release is accepted only with its original signed identity and exact #### `release-latest-convergence-bounded` -When creating a missing Release, the workflow pins one older immutable Latest predecessor; Latest may only remain that predecessor or advance to the exact target within at most twelve 5-second absolute slots in a 60-second monotonic deadline; any third identity, regression, drift, clock regression or exhaustion fails closed. +When creating a missing Release with an existing published predecessor, the workflow pins one older immutable Latest predecessor; Latest may only remain that predecessor or advance to the exact target within at most twelve 5-second absolute slots in a 60-second monotonic deadline; any third identity, regression, drift, clock regression or exhaustion fails closed. - Evidenced by property test. - Source: `docs/publishing.md`: “GitHub's Latest projection may remain only that exact predecessor or advance to the exact created target while the workflow makes at most twelve observations at absolute five-second slots inside one 60-second monotonic deadline.” @@ -1930,6 +1930,21 @@ When creating a missing Release, the workflow pins one older immutable Latest pr - The publisher model checks that no draft is created while Latest is a completed Release under a non-stable tag, which the completed-Release census skips; the other refusals of `exactLatestPredecessor` (a mutable, malformed, or not strictly older Latest) rest on its example tests in the same file. - How quickly GitHub's Latest projection converges is not verified; the window is a fail-closed ceiling. +#### `release-first-publication-empty-history` + +The first stable Release requires an authenticated exact Latest 404 agreeing with a complete bounded inventory containing no published non-prerelease Release, repeats the absence census before publication, and requires the exact immutable target as Latest after publication. Malformed, denied, ambiguous, or contradictory prepublication Latest responses permit no mutation. + +- Evidenced by stateful model. +- Source: `docs/publishing.md`: “For the first stable Release, an authenticated exact 404 for Latest must agree with a complete bounded inventory containing no published non-prerelease Release.” +- Evidence: `scripts/github-release-publish-model.test.ts`, `scripts/release-provider-outcome.test.ts` +- Property tests: `scripts/github-release-publish-model.test.ts`: “stateful model: every schedule of attempts, faults, and foreign releases keeps the publisher's write laws” +- Assumptions: `github-api`, `github-enforcement` +- Not verified: + - The publisher model drives production against an in-memory GitHub fake; actual provider response formats and immutability remain the github-api and github-enforcement assumptions. + - CI samples up to 1,000 schedules of at most 12 commands from both empty and predecessor-present initial histories; it does not enumerate every interleaving. + - First publication requires immediate exact Latest readback. A lagging or absent projection fails closed after immutable publication and must recover through the original attested attempt. + - GitHub has no conditional publish; terminal readback detects covered drift after publication but cannot undo an immutable Release. + #### `release-never-delete-published` A published immutable Release is never deleted or rewritten, even if terminal readback fails after publication; historical versions, tags and assetless Releases are preserved. @@ -1942,7 +1957,7 @@ A published immutable Release is never deleted or rewritten, even if terminal re - Not verified: - The publisher model drives the production `publishCanonicalRelease` and its bounded asset downloader against an in-memory fake of GitHub; that GitHub behaves like the fake (drafts invisible to the by-tag endpoint, one published Release per tag, `gh release upload` resolving a tag to its published Release or else the newest draft) is the `github-api` assumption. - CI samples up to 1,000 schedules of at most 12 commands; it does not enumerate every interleaving. - - The model's history is one assetless predecessor Release; larger histories and tag deletion outside the publisher are not modelled, and the tag rulesets that forbid tag deletion are `github-enforcement` configuration. + - The model starts with either empty release history or one assetless predecessor Release; larger histories and tag deletion outside the publisher are not modelled, and the tag rulesets that forbid tag deletion are `github-enforcement` configuration. #### `stable-release-concurrency-no-cancel-pending` diff --git a/docs/publishing.md b/docs/publishing.md index d5281ea..e6cae3b 100644 --- a/docs/publishing.md +++ b/docs/publishing.md @@ -1,14 +1,13 @@ # Publish Ghostget -Ghostget starts at `@hraness/ghostget@0.17.5`, with command `ghostget` and the -existing seven SDK subpaths. GitHub Releases became canonical under the former -`@hraness/wrench` name at v0.16.13. Historical manifests, archive filenames, and -signed provenance keep that original identity. npm carries the identical -canonical archive: the same tag Release workflow publishes it through OIDC -trusted publishing immediately after the immutable GitHub Release, with no -dispatch, staged approval, or two-factor prompt. An npm failure never unpublishes -or blocks the GitHub Release, and it is rerun from the same run. Historical versions and assetless Releases through v0.16.12 remain -unchanged. +The fresh public repository starts with `@hraness/ghostget@0.19.0`, command +`ghostget`, and eleven SDK entry points. The preceding repository and its complete +history are preserved in the owner's private archive. + +Verified immutable GitHub Releases are the canonical distribution. The same tag +Release workflow publishes the identical archive to npm through OIDC trusted +publishing after the GitHub Release. An npm failure never unpublishes or blocks +the canonical Release; recover it from the same run. ## Admit the canonical GitHub artifact @@ -73,7 +72,7 @@ selected as a substitute for the unique-run gate. After admission, Release still performs a fresh frozen install and deterministic build, checks generated `dist` and `bun.lock` cleanliness, dry packing and all -twelve Node imports. Its new exact npm archive passes the strict artifact parser +eleven Node imports. Its new exact npm archive passes the strict artifact parser and isolated consumer smoke before attestation or publication capability is available. CI also packs with the same Node/npm versions and canonical npm command, then checks the archive parser and calls the actual canonical @@ -245,7 +244,7 @@ delivery proceeds through a new source-qualified version. Checked-in `CODEOWNERS` assigns source ownership and notification for the workflow, Release helper, and publishing policy paths. It does not claim live or -independent review enforcement. Live Protect-main ruleset `20921911` has no +independent review enforcement. Live Protect-main ruleset `25394567` has no bypass actors, retains the pull-request path and exact Required integration check, requires no approving review, and does not require code-owner review. Ghostget currently has one eligible maintainer, so @@ -310,8 +309,9 @@ record as the whole body. The notes are presentation, not release authority, and so are the Release display title and bot login. An owner rerun of the same workflow run can therefore recover an already-created exact immutable Release. -Only when creating a missing immutable Release, the Release workflow first -pins one exact older immutable Latest Release by tag, ID, and publication time. +When creating a missing immutable Release in a repository with prior releases, +the Release workflow first pins one exact older immutable Latest Release by tag, +ID, and publication time. After the POST, GitHub's Latest projection may remain only that exact predecessor or advance to the exact created target while the workflow makes at most twelve observations at absolute five-second slots inside one 60-second monotonic @@ -327,6 +327,15 @@ observation and must bind the same tag, ID, and publication time. This is a bounded authority sandwich, not an atomic provider snapshot, and it never changes the immutable Release or its tag. +For the first stable Release, an authenticated exact 404 for Latest must agree +with a complete bounded inventory containing no published non-prerelease Release. +The workflow repeats that absence check before publication. It still requires +all five verified files, immutable publication, and the exact target as Latest. +With no pinned predecessor, an absent or lagging Latest response after publication +fails closed; the original attempt may resume without rebuilding or rewriting +that immutable Release. Existing-release recovery and terminal authority, +ordering, and exact Latest readbacks remain the same. + ## Install the canonical release These commands require the matching published immutable v0.19.0 release. diff --git a/kb/launch/social-kit.md b/kb/launch/social-kit.md index a05eeab..177cde6 100644 --- a/kb/launch/social-kit.md +++ b/kb/launch/social-kit.md @@ -248,7 +248,7 @@ Topics: Developer Tools, Artificial Intelligence, Open Source - measuredOn: September 22, 2026. website/source/index.html, Measured table summary - serviceCount: 19. website/provider-presentation.ts createProviderDirectory().providerCount - claimsNotVerified: 13. verification/claims.json, status not-verified -- claimsTotal: 209. verification/claims.json, every claim -- claimsEvidenced: 196. verification/claims.json, status evidenced +- claimsTotal: 210. verification/claims.json, every claim +- claimsEvidenced: 197. verification/claims.json, status evidenced - claimsConfigReadback: 9. verification/claims.json, layer configuration-readback - status: Latest release: v0.19.0. package.json version diff --git a/kb/plans/beeper-provider-marketing.md b/kb/plans/beeper-provider-marketing.md index a9d4f2b..0334d96 100644 --- a/kb/plans/beeper-provider-marketing.md +++ b/kb/plans/beeper-provider-marketing.md @@ -121,7 +121,7 @@ Reject any change that: - calls Message Like Me a clone, twin, autonomous representative, direct Beeper client, or sender; - says Message Like Me analyzes every message or that style evidence preserves meaning, facts, consent, or authorship; - calls PeopleBlade a generic “people intelligence” system, says Gmail instead of Google Contacts, or implies it reads or sends Beeper message bodies; -- presents blocked Telegram or live X routes as ready; +- presents blocked Telegram routes as ready; - says data never leaves a device despite requested provider work, an external agent, optional enrichment, or optional cloud projection; - substitutes “safe,” “secure,” “seamless,” “powerful,” or “production-ready” for an observable control; - invents social proof, completion percentages, partner status, or breadth comparisons that cannot be reproduced. @@ -151,7 +151,7 @@ Reject any change that: - 2026-08-27 — Shipped PeopleBlade's canonical source catalog, homepage and About parity, exact read-only Beeper route, explicit `beeper rebind` transition, local-CLI receipt/search provenance, source-incarnation history, and responsive/source metadata through [PR 36](https://github.com/hraness/peopleblade/pull/36). The current-main gate passed lint, typecheck, 495 tests, production build, and the StyleX browser/CSP matrix. Vercel production deployment `6130951969` bound exact merge commit `9a5d859e7d37d8373bb23212256805dd2fccc67b`; all public HTML, Markdown, `llms.txt`, sitemap, and robots routes were verified on `peopleblade.com`. - 2026-08-27 — Re-audited the three production sites as one journey. Wrench advertises 32 observed read/manage/send operations at Wrench 0.15.0, adapter 2.0.0, and official CLI 0.6.2. Message Like Me accepts only bundle schema 1, source `beeper-local`, and transform 1.1.0 and explicitly never calls Beeper/Wrench or sends. PeopleBlade exposes contacts and candidate search at the generic coordinate, keeps exporter 1.1.0/macOS arm64 interaction counts separate, and explicitly exposes none of Wrench's Beeper mutations. No naming, version, or authority contradiction remained. - 2026-08-27 — User review rejected Wrench's giant grotesk title, decorative circuit/orbit field, bulky controls, neutral provider icons, and contract-state-led directory as visually heavy and hard to understand. Chose Atet's editorial system as the concrete reference: Nebula Sans body copy, system serif display headings, thin rules, low-radius panels, restrained amber labels, and a two-column install-first hero. -- 2026-08-27 — Re-audited all 317 current release-bound operation rows and all 335 starting registry entries, then challenged every unavailable R1 row against existing exact reads and mutation readbacks. The trust gate accepted two standalone promotions: one current-viewer-owned private X Article draft read and one metadata-only Reddit hosted-video read. That moves the release snapshot from 128 to 130 executable contracts while 187 reservations remain inert. Retained predecessor identities bring the active registry to 337 entries: 137 observed and 200 capture-required. +- 2026-08-27 — Re-audited the release-bound operations and challenged unavailable R1 rows against existing exact reads and mutation readbacks. The trust gate accepted a metadata-only Reddit hosted-video read. - 2026-08-27 — Implemented the revised Wrench presentation for v0.16.0. The homepage now leads with a compact two-column install surface, the provider directory renders all and only the 18 services with executable actions, and the public copy contains neither `observed` nor `capture-required`. Reviewed the generated homepage and directory at desktop and 390-pixel widths, confirmed no horizontal overflow, and replaced the social preview with a matching 1200-by-630 editorial image. - 2026-08-27 — Exercised the new website, provider contracts, registry parity, version surfaces, generated package, and clean-consumer install. A long repository run exposed one unrelated macOS child-process denial while reading `kern.boottime`; the unchanged complete derivation file then passed 173 of 173 tests and the exact reused-PID case passed 10 of 10 with the required process access. No lifecycle code change was warranted. @@ -172,7 +172,7 @@ Reject any change that: - PeopleBlade implementation review finding: a straightforward identity-row update was not enough for Wrench 0.15.0's strengthened Beeper target. Disposition: add append-only source-binding incarnations and one explicit compare-and-swap rebind that proves the prior receipt, exact complete inventory, current identity/state, and new local-CLI contract before transition. - PeopleBlade database review finding: repeated raw-SQL probes found stale guard snapshots, mutable or replaceable guards, conflict-replacement deletion with recursive triggers disabled, row-ID aliases, and delete/reinsert substitution. Disposition: snapshot and recheck predecessor metadata and inventory, make admitted guards immutable through exact consumption, fence insert/replace collisions, compare every incarnation identity value including the row ID on all updates, and regress `id`, `rowid`, `UPDATE OR REPLACE`, stale-state, authority, chronology, and rollback paths. Two independent final reviews found no remaining commit-time invariant violation. - Post-release user review: the complete 317-row ledger was technically exact but made provider discovery read like an implementation audit. Disposition: keep the ledger as checked source and CLI truth; render only executable actions, access methods, and provider names on the public support page, omit zero-action Facebook Pages, and leave exact state terminology to technical security and authoring contexts. -- Coverage review: relabeling or filtering unsupported rows would create false support. An initial sibling-readback audit surfaced six possible R1 conversions, but the repository trust gate accepted only X `articles.read@2` and Reddit `media.read@2`. It rejected LinkedIn Article reads, Threads post/media reads, and Marketplace media reads because retained implementation seams or stale evidence do not independently authorize new standalone public operations. LinkedIn `posts.read` also remains unavailable because its observed publish readback is only a mutation-parameterized equality oracle with no checked raw response fixture or standalone response projection. Disposition: ship the two evidence-approved closed projections and keep all other reservations inert until exact current captures and authorization exist. +- Coverage review: relabeling or filtering unsupported rows would create false support. An initial sibling-readback audit surfaced six possible R1 conversions, but the repository trust gate accepted Reddit `media.read@2`. It rejected LinkedIn Article reads, Threads post/media reads, and Marketplace media reads because retained implementation seams or stale evidence do not independently authorize new standalone public operations. LinkedIn `posts.read` also remains unavailable because its observed publish readback is only a mutation-parameterized equality oracle with no checked raw response fixture or standalone response projection. Disposition: ship the evidence-approved closed projection and keep all other reservations inert until exact current captures and authorization exist. ## Result diff --git a/kb/plans/effect-read-lifecycle.md b/kb/plans/effect-read-lifecycle.md index 491247a..8ade65f 100644 --- a/kb/plans/effect-read-lifecycle.md +++ b/kb/plans/effect-read-lifecycle.md @@ -75,8 +75,7 @@ PR179 advanced main to `154e33e` and changed GitHub cancellation handling. Independent review reproduced an undefined-cause edge in that change. The combined, still-unpublished 0.16.9 candidate fixes that edge and adds the independently reviewed LinkedIn company program. It retains upstream strict -natural-exit browser cleanup, the X UserTweets descriptor refresh and both -subsequent response-identity fixes. +natural-exit browser cleanup. The combined source at `112b573` includes all three new production modules in the explicit package inventory. Two npm 11.19.0 packs after a normal Bun 1.3.14 @@ -110,8 +109,7 @@ derives both identities and preserves mutation sensitivity; no production identity constant changed. That stopped run is not a successful full gate. The aggregate on `291643a` passed its static, release-fixture and installed- -package stages before being stopped to integrate the newer X changes. It is -partial evidence, not a full pass. The joined payload receives fresh package +package stages before it was stopped. It is partial evidence, not a full pass. The joined payload receives fresh package measurements and a complete repository gate; earlier limits are not carried forward as measurements of changed source. diff --git a/kb/plans/effect-transcript-persistence.md b/kb/plans/effect-transcript-persistence.md index 8579d5b..57fe258 100644 --- a/kb/plans/effect-transcript-persistence.md +++ b/kb/plans/effect-transcript-persistence.md @@ -59,11 +59,11 @@ The first PR candidate passed eight CI jobs, including the native browser shard A separate recurring native browser-startup failure has not been causally diagnosed. The existing command boundary now retains bounded, content-free wrapper and stream observations before forced stop and after settlement. The test fixture labels its initial CDP read and cleanup commands explicitly, since one retained stack did not map to the checked source line. These observations preserve the selected error and cleanup authority. The later join with main `4045057` retains PR195’s explicit fixture policy: a one-use 40-second owned cold launch, unchanged 10-second action and pin deadlines, and one non-sliding 30-second cleanup window. The diagnostics add no further deadline change. Two existing native controls and three fixture cleanup controls pass, including proof that a settled original process group does not establish escaped-descendant cleanup. The existing escaped-child teardown remains unchanged; no new post-kill exit proof or Linux root-cause claim is made. -The final package comparison joins main `4045057`, including its X Viewer/Bookmarks evidence, with the transcript owner and diagnostics. Two npm 11.19.0 archives per source are byte-identical: the candidate has 501 files, 2,252,267 compressed bytes and 12,416,444 payload bytes; the current-main baseline has 497 files, 2,249,250 compressed bytes and 12,407,079 payload bytes. All eleven generated SDK files remain unchanged. Limits retain zero compressed headroom and current main’s 315 payload bytes. Earlier source measurements are historical. The joined fixture passes 12 native tests and 313 assertions, covering all eight collection controls, both actual launch/confirmation cases and the two browser lifecycle controls. Its 772 source/config inputs and four binaries stayed fixed. Current-candidate CI and the coordinated canonical-release source join remain pending. +The final package comparison joins main `4045057` with the transcript owner and diagnostics. Two npm 11.19.0 archives per source are byte-identical: the candidate has 501 files, 2,252,267 compressed bytes and 12,416,444 payload bytes; the current-main baseline has 497 files, 2,249,250 compressed bytes and 12,407,079 payload bytes. All eleven generated SDK files remain unchanged. Limits retain zero compressed headroom and current main’s 315 payload bytes. Earlier source measurements are historical. The joined fixture passes 12 native tests and 313 assertions, covering all eight collection controls, both actual launch/confirmation cases and the two browser lifecycle controls. Its 772 source/config inputs and four binaries stayed fixed. Current-candidate CI and the coordinated canonical-release source join remain pending. ## Canonical release handoff -PR196 merged into protected main as `6e8f757a6aa70cd56a3a69805e80223beb10c183`, with its complete ten-job PR CI attempt passing. The native and transcript evidence above remains attributed to that reviewed source. PR193 now joins this implementation into the canonical GitHub `0.16.13` candidate while retaining its exact owner, diagnostics and current X evidence. The combined package is now measured below; current-candidate validation and independent final review remain pending. The transcript change is not yet released; this plan stays in progress until the canonical artifact and applicable release evidence exist. +PR196 merged into protected main as `6e8f757a6aa70cd56a3a69805e80223beb10c183`, with its complete ten-job PR CI attempt passing. The native and transcript evidence above remains attributed to that reviewed source. PR193 now joins this implementation into the canonical GitHub `0.16.13` candidate while retaining its exact owner and diagnostics. The combined package is now measured below; current-candidate validation and independent final review remain pending. The transcript change is not yet released; this plan stays in progress until the canonical artifact and applicable release evidence exist. The joined `0.16.13` candidate was built with Bun 1.3.14. After correcting the changelog’s canonical starting version to `0.16.13`, it was packed twice with npm 11.19.0 / Node 24.20.0; build inputs stayed unchanged. Both archives have SHA-256 `24af5d712ac7633931ecab576860819a5266eb2b1bc9b262bfa61069a77fd420`, 501 files, 2,252,656 packed bytes and 12,417,812 payload bytes. Every archive file and mode matches the combined Git source. Against the exact merged-main package, 492 files are unchanged; canonical documentation and version projections account for 389 packed and 1,368 payload bytes. The current main's 315 payload bytes of headroom and zero packed headroom are retained. Package admission, fresh complete current-candidate CI and actual canonical publication remain pending; these measurements alone do not complete the release. diff --git a/kb/plans/lightpanda-semantic-capture.md b/kb/plans/lightpanda-semantic-capture.md index f080397..18b8392 100644 --- a/kb/plans/lightpanda-semantic-capture.md +++ b/kb/plans/lightpanda-semantic-capture.md @@ -231,7 +231,7 @@ Lightpanda reads is not supported by the evidence. ## The "auto" default (v0.18.84) -After the live X and LinkedIn proofs, the contained-session engine +After the live LinkedIn proofs, the contained-session engine default became `"auto"`: every headless session whose realm yields explicit cookies resolves to a provisioned Lightpanda, and Chromium remains the resolution for everything else. Eligibility adds the @@ -248,7 +248,7 @@ the same unpublished-preflight protection as an explicit `"auto"`. requests` commands (live revision discovery) on a `headed: false` session, the only headed:false transport with an unqualified command stream. -- Headed transports — X transaction bootstrap, Instagram profile, +- Headed transports — Instagram profile, LinkedIn article/comment/post/feed/search — resolve to Chromium through the headed gate alone, keeping the anti-bot property they declared `headed: true` for. @@ -297,9 +297,7 @@ the same unpublished-preflight protection as an explicit `"auto"`. LinkedIn transports (article, comment, post, feed, search), the headed mutation/anti-bot lanes, and every headed request — the headless-only eligibility gate keeps those on Chromium without - per-call-site pins. X's edge currently rejects the contained - headless Chrome entirely, so no Chrome-vs-Lightpanda X benchmark - exists; Lightpanda is the only contained engine that reaches it. + per-call-site pins. ## Durable memory diff --git a/scripts/github-release-artifact.test.ts b/scripts/github-release-artifact.test.ts index b3f3315..b99f1e2 100644 --- a/scripts/github-release-artifact.test.ts +++ b/scripts/github-release-artifact.test.ts @@ -177,7 +177,7 @@ function sourceCiFixture(attempt = 1, prNumber = 50) { const ciNames = ["static", "package", "test 1/8", "test 2/8", "test 3/8", "test 4/8", "test 5/8", "test 6/8", "test 7/8", "test 8/8", "test-omni", "standalone", "macOS", "verification", "quint 1/4", "quint 2/4", "quint 3/4", "quint 4/4", "Required"]; for (const [workflowId, path, event, runId, names] of [ [389265578, ".github/workflows/ci.yml", "push", 100, ciNames], - [351099999, "dynamic/github-code-scanning/codeql", "dynamic", 200, ["Analyze (javascript-typescript)", "Analyze (actions)", "Analyze (python)", "Analyze (rust)"]], + [389334774, "dynamic/github-code-scanning/codeql", "dynamic", 200, ["Analyze (javascript-typescript)", "Analyze (actions)", "Analyze (python)", "Analyze (rust)"]], ] as const) { responses[`${prefix}/actions/workflows/${workflowId}`] = { id: workflowId, path, state: "active" }; const run = { id: runId, workflow_id: workflowId, path, event, head_sha: input.source, head_branch: "main", run_attempt: attempt, @@ -389,7 +389,7 @@ describe("exact source CI admission", () => { }); test("refuses two exact-source CodeQL runs even when the later run has both source languages", () => { const fixture = sourceCiFixture(); - const path = `${fixture.prefix}/actions/workflows/351099999/runs?head_sha=${fixture.input.source}&branch=main&event=dynamic&per_page=100`; + const path = `${fixture.prefix}/actions/workflows/389334774/runs?head_sha=${fixture.input.source}&branch=main&event=dynamic&per_page=100`; const inventory = fixture.responses[path]; const earlier = { ...inventory.workflow_runs[0], id: 199 }; inventory.workflow_runs.push(earlier); inventory.total_count = 2; @@ -890,6 +890,9 @@ describe("canonical release publication and safe local input", () => { } if (args[1] !== "api") throw new Error(`Unexpected command ${args.join(" ")}`); if (args[2] === "--include") { + if (args[3] === "/repos/hraness/ghostget/releases/latest") { + return { status: 0, stdout: `HTTP/2 200\n\n${JSON.stringify(release?.draft === false ? release : predecessor)}` }; + } const visible = release?.draft === false; return { status: visible ? 0 : 1, stdout: `HTTP/2 ${visible ? 200 : 404}\n\n${JSON.stringify(visible ? release : { message: "Not Found" })}` }; diff --git a/scripts/github-release-publish-model.test.ts b/scripts/github-release-publish-model.test.ts index a139e9f..724b21d 100644 --- a/scripts/github-release-publish-model.test.ts +++ b/scripts/github-release-publish-model.test.ts @@ -61,9 +61,11 @@ type World = { type LookupFault = "lookup-500" | "lookup-403" | "lookup-status-mismatch" | "lookup-malformed" | "lookup-wrong-404-body" | "inventory-error"; +type LatestFault = "latest-404" | "latest-500" | "latest-status-mismatch" | "latest-wrong-404-body"; type Fault = | { kind: "none" } | { kind: LookupFault } + | { kind: LatestFault } | { kind: "crash-before" | "lost-after" | "starter"; at: number } | { kind: "authority-drift" | "main-advances" | "concurrent-higher"; at: number }; @@ -95,11 +97,12 @@ function releaseJson(release: StoredRelease): Record { const snapshot = (release: StoredRelease): string => JSON.stringify({ ...releaseJson(release), stored: release.assets.map(asset => [asset.id, sha256(asset.bytes), asset.corrupt, asset.state]) }); -function initialWorld(): World { +function initialWorld(firstRelease = false): World { const predecessor: StoredRelease = { id: PREDECESSOR_ID, tag: "v0.16.11", draft: false, immutable: true, body: "historical", target: "c".repeat(40), name: "Ghostget v0.16.11", author: BOT, assets: [], publishedAt: "2026-09-08T01:00:00Z", untagged: "0".repeat(20) }; - return { releases: [predecessor], latestId: PREDECESSOR_ID, mainSha: workflowSha, nextId: 100, nextAssetId: 1000, clock: 0, latestLag: 0 }; + return { releases: firstRelease ? [] : [predecessor], latestId: firstRelease ? 0 : PREDECESSOR_ID, + mainSha: workflowSha, nextId: 100, nextAssetId: 1000, clock: 0, latestLag: 0 }; } type Write = { kind: "create" | "upload" | "publish"; releaseId: number }; @@ -195,6 +198,17 @@ async function invoke(world: World, attempt: Attempt, fault: Fault): Promise release.id === world.latestId); + events.push({ kind: "latest", id: world.latestId }); + if (fault.kind === "latest-500") return { status: 1, stdout: 'HTTP/2 500\n\n{"message":"Server Error"}' }; + if (fault.kind === "latest-wrong-404-body") return { status: 1, stdout: 'HTTP/2 404\n\n{"message":"Forbidden"}' }; + const missing = latest === undefined || fault.kind === "latest-404"; + return { + status: fault.kind === "latest-status-mismatch" ? (missing ? 0 : 1) : (missing ? 1 : 0), + stdout: `HTTP/2 ${missing ? "404" : "200"}\n\n${JSON.stringify(missing ? { message: "Not Found" } : releaseJson(latest!))}`, + }; + } if (args.length !== 4 || args[3] !== `${prefix}/releases/tags/${tag}`) { violations.push(`unexpected included read ${args.join(" ")}`); return { status: 1, stdout: "" }; @@ -236,7 +250,8 @@ async function invoke(world: World, attempt: Attempt, fault: Fault): Promise release.id === world.latestId)!)); + const latest = world.releases.find(release => release.id === world.latestId); + return latest === undefined ? notFound : ok(releaseJson(latest)); } if (endpoint === `${prefix}/releases/tags/${tag}`) { const found = byTagPublished(); return found === undefined ? notFound : ok(releaseJson(found)); } const byId = /^\/repos\/hraness\/ghostget\/releases\/([1-9][0-9]*)$/u.exec(endpoint); @@ -366,7 +381,7 @@ class Publish implements fc.AsyncCommand { names: release.assets.map(asset => asset.name) })); const live = this.fault.kind === "none" && resumable(world, attempt); const publishedBefore = world.releases.some(release => release.tag === tag && !release.draft); - const latestBefore = world.releases.find(release => release.id === world.latestId)!; + const latestBefore = world.releases.find(release => release.id === world.latestId); const outcome = await invoke(world, attempt, this.fault); expect(outcome.violations).toEqual([]); // Nothing is ever deleted, and a published release, a foreign release, or a @@ -391,8 +406,8 @@ class Publish implements fc.AsyncCommand { expect(outcome.error).toBeDefined(); expect(outcome.writes).toEqual([]); } - // A missing Release is created only after pinning one older stable Latest predecessor. - if (!publishedBefore && latestBefore.tag === NON_STABLE_TAG) { + // An existing non-stable Latest cannot be treated as an absent predecessor. + if (!publishedBefore && latestBefore?.tag === NON_STABLE_TAG) { expect(outcome.error).toBeDefined(); expect(outcome.writes).toEqual([]); } @@ -552,9 +567,40 @@ afterAll(async () => { if (root !== "") await rm(root, { recursive: true, force: const PUBLISHER_MODEL_PROPERTY = Object.freeze({ numRuns: 1000, interruptAfterTimeLimit: 30_000 }); describe("canonical GitHub publisher stateful model", () => { + test("publishes the first immutable release only after proving no published predecessor exists", async () => { + const world = initialWorld(true); + const outcome = await invoke(world, attempts.get("R1")!, { kind: "none" }); + expect(outcome.violations).toEqual([]); + expect(outcome.error).toBeUndefined(); + expect(outcome.writes.map(write => write.kind)).toEqual([ + "create", "upload", "upload", "upload", "upload", "upload", "publish", + ]); + expect(world.releases).toHaveLength(1); + const target = world.releases[0]!; + expect(target.tag).toBe(tag); + expect(target.immutable).toBe(true); + expect(target.assets.map(asset => asset.name).sort()).toEqual([...names].sort()); + expectTerminalLatestAndAuthority(outcome, target.id); + const rerun = await invoke(world, attempts.get("R1")!, { kind: "none" }); + expect(rerun.error).toBeUndefined(); + expect(rerun.writes).toEqual([]); + expect(rerun.violations).toEqual([]); + }); + + test("refuses a missing Latest projection over published history and unproven missing responses", async () => { + for (const fault of ["latest-404", "latest-500", "latest-status-mismatch", "latest-wrong-404-body"] as const) { + const world = initialWorld(); + const outcome = await invoke(world, attempts.get("R1")!, { kind: fault }); + expect(outcome.error).toBeDefined(); + expect(outcome.writes).toEqual([]); + expect(outcome.violations).toEqual([]); + expect(world.releases).toHaveLength(1); + } + }); + test("stateful model: every schedule of attempts, faults, and foreign releases keeps the publisher's write laws", async () => { - await assertAsyncProperty(fc.asyncProperty(commandArbitrary, async (commands) => { - await fc.asyncModelRun(() => ({ model: {}, real: { world: initialWorld(), attempts } }), commands); + await assertAsyncProperty(fc.asyncProperty(commandArbitrary, fc.boolean(), async (commands, firstRelease) => { + await fc.asyncModelRun(() => ({ model: {}, real: { world: initialWorld(firstRelease), attempts } }), commands); }), PUBLISHER_MODEL_PROPERTY); }); diff --git a/scripts/github-release-publish.ts b/scripts/github-release-publish.ts index 2dbc553..7e0b005 100644 --- a/scripts/github-release-publish.ts +++ b/scripts/github-release-publish.ts @@ -165,8 +165,14 @@ export async function publishCanonicalRelease(directory: string, manifest: Relea return; } await assertReleaseTagNewerThanPublished({ api, repository, verifiedTag: manifest.tag }); - const predecessor = await get(`${prefix}/releases/latest`); - exactLatestPredecessor(predecessor, manifest.tag); + const latestLookup = run(["gh", "api", "--include", `${prefix}/releases/latest`]); + const latestResponse = parseOptionalIncludedGitHubResponse(latestLookup.stdout, "pre-publication Latest Release lookup"); + if (latestLookup.status !== (latestResponse.found ? 0 : 1)) throw new Error("Latest Release lookup status is not exact"); + const predecessor = latestResponse.found ? latestResponse.value : undefined; + if (latestResponse.found) exactLatestPredecessor(predecessor, manifest.tag); + else await assertReleaseTagNewerThanPublished({ + api, repository, verifiedTag: manifest.tag, requireNoPublishedRelease: true, + }); const mutate = (method: "POST" | "PATCH", path: string, value: unknown): Record => object(JSON.parse(successful(run, ["gh", "api", "--method", method, path, "--input", "-"], JSON.stringify(value)))); const validateDraft = (value: Record): void => { @@ -199,7 +205,9 @@ export async function publishCanonicalRelease(directory: string, manifest: Relea release = await readDraft(); if (validateReleaseAssets(release, manifest, directory).missing.length !== 0) throw new Error("Draft is incomplete"); verifyRemoteBytes(release); - await assertReleaseTagNewerThanPublished({ api, repository, verifiedTag: manifest.tag }); + await assertReleaseTagNewerThanPublished({ + api, repository, verifiedTag: manifest.tag, requireNoPublishedRelease: !latestResponse.found, + }); await authority("prewrite"); const published = mutate("PATCH", `${prefix}/releases/${draftId}`, { draft: false, make_latest: "true" }); exactWorkflowPublishedRelease({ ...coordinates, value: published }); @@ -209,7 +217,13 @@ export async function publishCanonicalRelease(directory: string, manifest: Relea if (readback.id !== draftId || readback.body !== body || readback.published_at !== published.published_at || validateReleaseAssets(readback, manifest, directory).missing.length !== 0) throw new Error("Immutable publication readback differs"); verifyRemoteBytes(readback); - await waitForLatestRelease({ api, predecessorRelease: predecessor, repository, targetRelease: readback, verifiedTag: manifest.tag }); + if (latestResponse.found) { + await waitForLatestRelease({ api, predecessorRelease: predecessor, repository, targetRelease: readback, verifiedTag: manifest.tag }); + } else { + // With no pinned predecessor, only the exact target may be observed. A + // lagging/missing projection fails closed and the same attempt can resume. + await requireLatestRelease({ api, repository, targetRelease: readback, verifiedTag: manifest.tag }); + } await authority("postwrite"); // GitHub has no conditional publish: a stable Release completed out of band // after the pre-publication census would otherwise leave this older target Latest. diff --git a/scripts/release-provider-outcome.mjs b/scripts/release-provider-outcome.mjs index 092d43e..bc393e0 100644 --- a/scripts/release-provider-outcome.mjs +++ b/scripts/release-provider-outcome.mjs @@ -226,6 +226,7 @@ function compareStableVersions(left, right) { export async function assertReleaseTagNewerThanPublished({ allowExistingTarget = false, api, + requireNoPublishedRelease = false, repository, verifiedTag, }) { @@ -275,6 +276,9 @@ export async function assertReleaseTagNewerThanPublished({ release.tag_name, `published releases page ${String(page)} item ${String(index)} tag_name`, ); + if (requireNoPublishedRelease && !draft && !prerelease) { + fail("Missing Latest Release conflicts with published release history"); + } const current = stableVersion(currentTag, "published release tag"); if (!draft && !prerelease && current !== undefined) { const immutable = expectBoolean( @@ -942,4 +946,4 @@ export async function revalidateLatestReleaseProjection({ }); } -const invokedPath = process.argv[1]; \ No newline at end of file +const invokedPath = process.argv[1]; diff --git a/scripts/release-source-ci.ts b/scripts/release-source-ci.ts index 23bb591..be82f2e 100644 --- a/scripts/release-source-ci.ts +++ b/scripts/release-source-ci.ts @@ -13,7 +13,7 @@ const PREFIX = `repos/${REPOSITORY}`; const MAIN_REF = "refs/heads/main"; const CI_WORKFLOW = 389265578; const CI_PATH = ".github/workflows/ci.yml"; -const CODEQL_WORKFLOW = 351099999; +const CODEQL_WORKFLOW = 389334774; const CODEQL_PATH = "dynamic/github-code-scanning/codeql"; const MARKER = "WRENCH_SOURCE_CI_IDENTITY="; const SHA = /^[a-f0-9]{40}$/u; diff --git a/verification/claims.json b/verification/claims.json index da69dd8..2270b0a 100644 --- a/verification/claims.json +++ b/verification/claims.json @@ -5109,7 +5109,7 @@ }, { "id": "release-latest-convergence-bounded", - "statement": "When creating a missing Release, the workflow pins one older immutable Latest predecessor; Latest may only remain that predecessor or advance to the exact target within at most twelve 5-second absolute slots in a 60-second monotonic deadline; any third identity, regression, drift, clock regression or exhaustion fails closed.", + "statement": "When creating a missing Release with an existing published predecessor, the workflow pins one older immutable Latest predecessor; Latest may only remain that predecessor or advance to the exact target within at most twelve 5-second absolute slots in a 60-second monotonic deadline; any third identity, regression, drift, clock regression or exhaustion fails closed.", "area": "release", "source": { "path": "docs/publishing.md", @@ -5139,6 +5139,37 @@ } ] }, + { + "id": "release-first-publication-empty-history", + "statement": "The first stable Release requires an authenticated exact Latest 404 agreeing with a complete bounded inventory containing no published non-prerelease Release, repeats the absence census before publication, and requires the exact immutable target as Latest after publication. Malformed, denied, ambiguous, or contradictory prepublication Latest responses permit no mutation.", + "area": "release", + "source": { + "path": "docs/publishing.md", + "quote": "For the first stable Release, an authenticated exact 404 for Latest must agree with a complete bounded inventory containing no published non-prerelease Release." + }, + "layer": "stateful-model", + "status": "evidenced", + "evidence": [ + "scripts/github-release-publish-model.test.ts", + "scripts/release-provider-outcome.test.ts" + ], + "assumptions": [ + "github-api", + "github-enforcement" + ], + "notVerified": [ + "The publisher model drives production against an in-memory GitHub fake; actual provider response formats and immutability remain the github-api and github-enforcement assumptions.", + "CI samples up to 1,000 schedules of at most 12 commands from both empty and predecessor-present initial histories; it does not enumerate every interleaving.", + "First publication requires immediate exact Latest readback. A lagging or absent projection fails closed after immutable publication and must recover through the original attested attempt.", + "GitHub has no conditional publish; terminal readback detects covered drift after publication but cannot undo an immutable Release." + ], + "properties": [ + { + "path": "scripts/github-release-publish-model.test.ts", + "test": "stateful model: every schedule of attempts, faults, and foreign releases keeps the publisher's write laws" + } + ] + }, { "id": "release-never-delete-published", "statement": "A published immutable Release is never deleted or rewritten, even if terminal readback fails after publication; historical versions, tags and assetless Releases are preserved.", @@ -5160,7 +5191,7 @@ "notVerified": [ "The publisher model drives the production `publishCanonicalRelease` and its bounded asset downloader against an in-memory fake of GitHub; that GitHub behaves like the fake (drafts invisible to the by-tag endpoint, one published Release per tag, `gh release upload` resolving a tag to its published Release or else the newest draft) is the `github-api` assumption.", "CI samples up to 1,000 schedules of at most 12 commands; it does not enumerate every interleaving.", - "The model's history is one assetless predecessor Release; larger histories and tag deletion outside the publisher are not modelled, and the tag rulesets that forbid tag deletion are `github-enforcement` configuration." + "The model starts with either empty release history or one assetless predecessor Release; larger histories and tag deletion outside the publisher are not modelled, and the tag rulesets that forbid tag deletion are `github-enforcement` configuration." ], "properties": [ { diff --git a/website/launch/facts.ts b/website/launch/facts.ts index bb5cd82..e6e2ee9 100644 --- a/website/launch/facts.ts +++ b/website/launch/facts.ts @@ -29,10 +29,10 @@ export const LAUNCH_SERVICE_COUNT = 19 as const; export const LAUNCH_CLAIMS_NOT_VERIFIED = 13 as const; /** Every claim in verification/claims.json. */ -export const LAUNCH_CLAIMS_TOTAL = 209 as const; +export const LAUNCH_CLAIMS_TOTAL = 210 as const; /** Claims in verification/claims.json with status evidenced. */ -export const LAUNCH_CLAIMS_EVIDENCED = 196 as const; +export const LAUNCH_CLAIMS_EVIDENCED = 197 as const; /** Claims in verification/claims.json whose layer is configuration-readback: repository and hosting settings an administrator reads back. */ export const LAUNCH_CLAIMS_CONFIG_READBACK = 9 as const;