From a2868d279052d6ec950822ddc580b5da203212e0 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 7 Aug 2026 18:22:05 +0200 Subject: [PATCH] =?UTF-8?q?verify(v1.133):=20close=20the=20V=20=E2=80=94?= =?UTF-8?q?=20REL-P01,=20OCI-P02=20and=20OCI-P04=20had=20zero=20verifiers?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit All three v1.133 requirements sat at `implemented` with NO verification artifact pointing at them. The release-execution traceability gate blocks a tag in that state, and it should: `implemented` with no verifier is a claim with no evidence. This was my own gap. I bumped the three to `implemented` citing OCI-P01 as precedent — but OCI-P01 landed at `implemented` WITH a verifier (FV-FALCON-OCI-001) attached. I replicated the status and not the evidence. Adds one verifier each, with CI-runnable assertions rather than prose: FV-FALCON-REL-001 -> SWREQ-FALCON-REL-P01 both `gh release create` paths pass --draft; one terminal publish step; the malformed-tag guard exists. FV-FALCON-OCI-002 -> SWREQ-FALCON-OCI-P02 8/8 components are no_std AND export the shared bounded-arena runtime. Asserted as EIGHT, not "at least one": v1.129 shipped a partially converted cascade, and one std stage re-introduces WASI and memory.grow into the fused image. FV-FALCON-OCI-003 -> SWREQ-FALCON-OCI-P04 the package declares pulseengine:falcon-cascade AND there are ZERO remaining `falcon:cascade` references. The negative assertion carries the weight — a PARTIAL rename is worse than none. These are real verifiers, not decoration — each was observed to FAIL before its implementation merged and PASS after: OCI-003 PASS once #337 landed OCI-002 1/8 -> 8/8 the moment #339 landed REL-001 0/2 -> 2/2 the moment #340 landed A step that cannot fail is not evidence; these can, and did. Also caught by running the gate rather than trusting the draft: an `gh release view falcon-v1.133.0 ... # bench-only` step really EXECUTED and failed rc=1. The gate detects bench-only by COMMAND SHAPE (BENCH_PATTERNS) — rivet strips shell comments at the YAML->JSON boundary, so the marker is inert. Removed, with the reasoning recorded in the artifact: a step whose result depends on WHEN it runs is not evidence. All three stay `implemented`, not `verified`. The binding evidence — published blobs, and an actual draft->published transition — only exists once falcon-v1.133.0 has run. Promotion is the post-tag verify PR, per the two-commit rule. Verified locally: gate scoped to these artifacts: 7/7 steps PASS, exit 0, 5 bench-only skipped rivet validate (v0.19.0 — the version the GATE pins, not local 0.28): PASS Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- artifacts/verification/FV-FALCON-OCI-002.yaml | 58 ++++++++++++++++ artifacts/verification/FV-FALCON-OCI-003.yaml | 46 +++++++++++++ artifacts/verification/FV-FALCON-REL-001.yaml | 68 +++++++++++++++++++ 3 files changed, 172 insertions(+) create mode 100644 artifacts/verification/FV-FALCON-OCI-002.yaml create mode 100644 artifacts/verification/FV-FALCON-OCI-003.yaml create mode 100644 artifacts/verification/FV-FALCON-REL-001.yaml diff --git a/artifacts/verification/FV-FALCON-OCI-002.yaml b/artifacts/verification/FV-FALCON-OCI-002.yaml new file mode 100644 index 0000000..be01014 --- /dev/null +++ b/artifacts/verification/FV-FALCON-OCI-002.yaml @@ -0,0 +1,58 @@ +artifacts: + - id: FV-FALCON-OCI-002 + type: sw-verification + title: "OCI-P02 — the whole cascade is no_std and no-grow: 8/8 components, WASI-free (v1.133)" + status: implemented + release: falcon-v1.133.0 + description: > + Verification of SWREQ-FALCON-OCI-P02. The requirement is that EVERY + published cascade stage lowers to bare metal, not just the one that was + converted first. + + WHY IT EXISTS: v1.129 shipped `falcon-rate` converted to no_std while the + other stages still linked std and carried WASI imports. A partially + converted cascade is not lowerable — jess fuses the stages together, so + one std stage re-introduces WASI and `memory.grow` into the fused image + and blocks `meld fuse --memory shared --address-rebase` (gale#89, + meld#299). "Most of the cascade lowers" is not a useful property. + + EVIDENCE, IN TWO TIERS. + + (a) SOURCE-LEVEL, ALL STAGES (CI-runnable, the steps below). All 8 + components under wasm/cm/ declare `#![cfg_attr(not(feature = "std"), + no_std)]` and export the shared Component-Model runtime via + `falcon_cm_rt::export_cm_rt!()`. The count is asserted as EIGHT rather + than "at least one", so adding a 9th stage that forgets the conversion + fails this step instead of passing unnoticed — that is the regression + this artifact exists to catch, given the v1.129 history above. + + The shared runtime matters on its own: it supplies `cabi_realloc` backed + by a BOUNDED arena. wit-bindgen-rt supplies that symbol only when std is + linked (`#[cfg(not(target_env = "p2"))]`), which is precisely why the + first no_std conversion silently produced a raw core module instead of a + component. Centralising it means the fix cannot be forgotten per-stage. + + (b) ARTIFACT-LEVEL (bench-only — needs cargo-component + wasm-tools, + which the gate runner does not provide). The binding evidence is the + built wasm: zero `wasi:*` imports and zero `memory.grow` in every + published component. That is checked per release against the actual + published blobs, and is recorded in FV-FALCON-OCI-001. + + SCOPE (honest): (a) proves the SOURCE is uniformly converted; it does not + prove the emitted binary is WASI-free — a dependency could reintroduce + std transitively. Only (b) proves that, and (b) is bench-only here. The + per-release blob inspection is what closes it. + tags: [verification, falcon, oci, wasm, no-std, embedded, component-model, v1.133] + fields: + method: test + steps: + # (a) ALL EIGHT stages are no_std — not "at least one" + - run: "test \"$(grep -l 'no_std)' wasm/cm/*/src/lib.rs | wc -l)\" -eq 8" + # ...and all eight export the shared bounded-arena CM runtime + - run: "test \"$(grep -l 'export_cm_rt' wasm/cm/*/src/lib.rs | wc -l)\" -eq 8" + # (b) the binding evidence, per published blob + - run: "wasm-tools component wit falcon_rate_cm.wasm # bench-only: expect 0 wasi:* imports" + - run: "wasm-tools print falcon_rate_cm.wasm | grep -c 'memory.grow' # bench-only: expect 0" + links: + - type: verifies + target: SWREQ-FALCON-OCI-P02 diff --git a/artifacts/verification/FV-FALCON-OCI-003.yaml b/artifacts/verification/FV-FALCON-OCI-003.yaml new file mode 100644 index 0000000..ddd44a9 --- /dev/null +++ b/artifacts/verification/FV-FALCON-OCI-003.yaml @@ -0,0 +1,46 @@ +artifacts: + - id: FV-FALCON-OCI-003 + type: sw-verification + title: "OCI-P04 — the WIT package namespace is pulseengine:falcon-*, with no falcon:* remnants (v1.133)" + status: implemented + release: falcon-v1.133.0 + description: > + Verification of SWREQ-FALCON-OCI-P04. The requirement is that the WIT + package namespace matches the registry namespace we actually publish + under, so that a consumer browsing the ecosystem finds our components and + the interfaces they export in the SAME place. + + WHY IT EXISTS: wasm.directory indexes COMPONENTS by their registry + namespace but INTERFACES by their WIT package namespace. Publishing + components under `pulseengine` while their interfaces declared + `falcon:cascade` split our own surface across two namespaces — the + exports and imports were not discoverable from the component's own page. + + EVIDENCE: the rename is only correct if it is COMPLETE. A partial rename + is worse than none — it leaves a package that resolves in one tool and + not another. So the evidence is two-sided: + + (a) POSITIVE — the cascade package declares the new namespace. + (b) NEGATIVE — there is not a single remaining `falcon:cascade` reference + anywhere under wit/. This is the step that actually carries the weight: + it is the one that fails if the rename is partial, and it is cheap enough + to run on every PR, so the property cannot silently regress. + + Measured at the time this landed: 0 remaining references across the whole + wit/ tree. + + SCOPE (honest): this verifies the WIT SOURCE. That the published OCI + manifests and the wasm.directory listing agree with it is covered by the + OCI distribution evidence (FV-FALCON-OCI-001) and re-checked per release; + this artifact does not claim it. + tags: [verification, falcon, oci, wit, namespace, wasm-directory, v1.133] + fields: + method: test + steps: + # (a) the package declares the unified namespace + - run: "grep -q 'package pulseengine:falcon-cascade' wit/falcon-cascade/cascade.wit" + # (b) THE LOAD-BEARING STEP — a partial rename must fail this + - run: "test \"$(grep -rl 'falcon:cascade' wit/ | wc -l)\" -eq 0" + links: + - type: verifies + target: SWREQ-FALCON-OCI-P04 diff --git a/artifacts/verification/FV-FALCON-REL-001.yaml b/artifacts/verification/FV-FALCON-REL-001.yaml new file mode 100644 index 0000000..1748e8e --- /dev/null +++ b/artifacts/verification/FV-FALCON-REL-001.yaml @@ -0,0 +1,68 @@ +artifacts: + - id: FV-FALCON-REL-001 + type: sw-verification + title: "REL-P01 — the release is created as a DRAFT and published only after every artifact is present (v1.133)" + status: implemented + release: falcon-v1.133.0 + description: > + Verification of SWREQ-FALCON-REL-P01. The requirement is an ORDERING + property of .github/workflows/release.yml: a tagged release must not be + visible to consumers until every asset it claims is actually attached. + + WHY IT EXISTS: falcon-v1.131.0 shipped a published GitHub Release whose + component assets were missing — the release job had switched the component + build to wasm32-unknown-unknown but did not install that target, so the + build produced nothing and the release published anyway. A consumer + pulling v1.131.0 got "half a release". Draft-then-finalize makes that + state unreachable: the release is invisible until the guard passes. + + EVIDENCE, IN TWO TIERS. + + (a) CONFIGURATION (CI-runnable, the steps below). Both `gh release create` + paths — the notes-file path and the autogenerated-notes path — pass + `--draft`, and a single terminal step ("Publish the release (flip the + draft)") is what makes it visible. This is static evidence about the + workflow's shape, which is exactly what an ordering requirement is: the + property lives in the workflow definition, not in a runtime value. + + (b) EXECUTION (bench-only until a tagged release exercises it). The + strong evidence is a real release: the draft exists during the run, the + guard rejects a malformed tag and a missing-asset set, and the release + flips to published only at the end. falcon-v1.133.0 is the first release + that exercises this path, and is the happy-path proof. The FAILURE + injection — forcing an upload to fail and confirming the release STAYS a + draft — is deliberately deferred to a scratch tag after v1.133, so the + happy path is proven before the failure path is provoked on the real + release train. + + SCOPE (honest): (a) is verified mechanically on every PR. (b) is NOT + verified at the time this artifact lands — it cannot be, since it requires + a tagged release. This artifact stays `implemented` until falcon-v1.133.0 + has run and its draft->published transition is recorded; only then does it + become `verified`. This is the same two-tier split as FV-FALCON-OCI-001. + tags: [verification, falcon, release, oci, ordering, v1.133] + fields: + method: test + steps: + # (a) CONFIGURATION — both create paths are drafts. + - run: "test \"$(grep -cE '^[[:space:]]+--draft' .github/workflows/release.yml)\" -eq 2" + # A single terminal step is what publishes it. + - run: "grep -q 'Publish the release (flip the draft)' .github/workflows/release.yml" + # The guard refuses a malformed tag rather than publishing it. + - run: "grep -q 'refusing to publish a malformed tag' .github/workflows/release.yml" + # (b) EXECUTION is deliberately NOT a step here. The obvious candidate, + # `gh release view falcon-v1.133.0 --json isDraft`, cannot be one: the + # gate identifies bench-only steps by COMMAND SHAPE (BENCH_PATTERNS), + # not by a trailing `# bench-only` comment — rivet strips shell comments + # at the YAML->JSON boundary — so such a step would really execute and + # fail with rc=1 on every PR until the release exists, and then pass for + # the rest of time. That is a step whose result depends on WHEN it runs, + # which is not evidence. (Confirmed empirically: it failed exactly that + # way when this artifact was first drafted.) + # + # The draft->published transition is instead recorded against the real + # release in the post-tag verify PR, which is what promotes this + # artifact from `implemented` to `verified`. + links: + - type: verifies + target: SWREQ-FALCON-REL-P01