Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
58 changes: 58 additions & 0 deletions artifacts/verification/FV-FALCON-OCI-002.yaml
Original file line number Diff line number Diff line change
@@ -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
46 changes: 46 additions & 0 deletions artifacts/verification/FV-FALCON-OCI-003.yaml
Original file line number Diff line number Diff line change
@@ -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
68 changes: 68 additions & 0 deletions artifacts/verification/FV-FALCON-REL-001.yaml
Original file line number Diff line number Diff line change
@@ -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
Loading