From 50f9b859a9288c3afbb81bfd9111a1d0bf23650f Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Mon, 20 Apr 2026 19:08:34 +0200 Subject: [PATCH 01/15] fix(ci): make Kani, Rocq, and Mutation Testing real hard gates MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Audit found that all four verification-pyramid CI jobs were silently failing on main. None had ever run green. This fixes three and scopes the fourth to an upstream bug. **Kani Proofs** — flipped to hard gate. Five harnesses in rivet-core/src/proofs.rs were initializing `EvalContext` with only `artifact` + `graph` fields after the struct grew a `store: Option<...>` field for quantifier support. The cfg(kani) gate meant the break was invisible to normal `cargo check`. Added `store: None` to all five. **Rocq Proofs** — flipped to hard gate. The `rocq_library` target `rivet_metamodel` had `srcs = []`, which fails Bazel analysis with "rocq_library requires at least one source file". Removed the empty aggregator target and pointed the test at the two real libraries (Schema + Validation) directly. **Mutation Testing** — split into a per-crate matrix so rivet-core and rivet-cli each get a 45-minute budget. Previously both crates shared a single 40-minute timeout, causing rivet-core to be cancelled before finishing and rivet-cli to never run. `--timeout` per-mutant reduced from 120s to 90s. Uploads are now per-crate artifacts. **Verus Proofs** — left as continue-on-error with a pointer comment. Root cause is in rules_verus (pulseengine/rules_verus, commit e2c1600): the hub repository's `:all` alias only points to the first platform's toolchain rather than registering `toolchain()` rules for each platform, so `register_toolchains("@verus_toolchains//:all")` resolves to a non-toolchain target. Fixing this requires an upstream change to rules_verus. With these fixes, CI will fail — honestly — on Kani regressions, Rocq proof breaks, and surviving mutants, instead of silently reporting green. Implements: REQ-010, REQ-029 Verifies: REQ-010 --- .github/workflows/ci.yml | 55 ++++++++++++++++++++-------------------- proofs/rocq/BUILD.bazel | 15 +++-------- rivet-core/src/proofs.rs | 5 ++++ 3 files changed, 36 insertions(+), 39 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b69d9ab..c55ee47 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -286,51 +286,46 @@ jobs: PROPTEST_CASES: "1000" # ── Mutation testing (hard gate — zero surviving mutants) ──────────── + # Split per-crate into parallel jobs so each has its own 45-min budget. mutants: - name: Mutation Testing + name: Mutation Testing (${{ matrix.crate }}) needs: [test] runs-on: ubuntu-latest - timeout-minutes: 40 + timeout-minutes: 45 + strategy: + fail-fast: false + matrix: + crate: [rivet-core, rivet-cli] steps: - uses: actions/checkout@v6 - uses: dtolnay/rust-toolchain@stable - uses: Swatinem/rust-cache@v2 + with: + key: mutants-${{ matrix.crate }} - name: Install cargo-mutants uses: taiki-e/install-action@v2 with: tool: cargo-mutants - - name: Run cargo-mutants on rivet-core - run: cargo mutants -p rivet-core --timeout 120 --jobs 4 --output mutants-out -- --lib || true - - name: Run cargo-mutants on rivet-cli - run: cargo mutants -p rivet-cli --timeout 120 --jobs 4 --output mutants-cli-out -- --lib || true + - name: Run cargo-mutants + run: cargo mutants -p ${{ matrix.crate }} --timeout 90 --jobs 4 --output mutants-out -- --lib || true - name: Check surviving mutants run: | MISSED=0 - for dir in mutants-out mutants-cli-out; do - if [ -f "$dir/missed.txt" ]; then - COUNT=$(wc -l < "$dir/missed.txt" | tr -d ' ') - MISSED=$((MISSED + COUNT)) - fi - done - echo "Surviving mutants: $MISSED" + if [ -f "mutants-out/missed.txt" ]; then + MISSED=$(wc -l < "mutants-out/missed.txt" | tr -d ' ') + fi + echo "Surviving mutants in ${{ matrix.crate }}: $MISSED" if [ "$MISSED" -gt 0 ]; then - echo "::error::$MISSED mutant(s) survived — add tests to kill them" - for dir in mutants-out mutants-cli-out; do - if [ -f "$dir/missed.txt" ]; then - echo "--- $dir ---" - head -30 "$dir/missed.txt" - fi - done + echo "::error::$MISSED mutant(s) survived in ${{ matrix.crate }} — add tests to kill them" + head -30 mutants-out/missed.txt exit 1 fi - name: Upload mutants report if: always() uses: actions/upload-artifact@v4 with: - name: mutants-report - path: | - mutants-out/ - mutants-cli-out/ + name: mutants-report-${{ matrix.crate }} + path: mutants-out/ # ── Fuzz testing (main only — too slow for PRs) ─────────────────── fuzz: @@ -384,12 +379,11 @@ jobs: - name: Check supply chain run: cargo vet --locked - # ── Kani bounded model checking ──────────────────────────────────── + # ── Kani bounded model checking (hard gate) ───────────────────────── kani: name: Kani Proofs needs: [test] runs-on: ubuntu-latest - continue-on-error: true timeout-minutes: 30 steps: - uses: actions/checkout@v6 @@ -397,6 +391,12 @@ jobs: - run: cargo kani -p rivet-core # ── Verus SMT verification ────────────────────────────────────────── + # TODO: flip to hard gate once the upstream hub-repo bug in rules_verus + # is fixed. Currently the `:all` alias points to only the first platform's + # toolchain rather than registering toolchain() rules for each platform, + # so `register_toolchains("@verus_toolchains//:all")` resolves to a + # non-toolchain target and resolution fails. + # Upstream: https://github.com/pulseengine/rules_verus verus: name: Verus Proofs needs: [test] @@ -415,12 +415,11 @@ jobs: working-directory: verus run: bazel test //:rivet_specs_verify - # ── Rocq metamodel proofs ───────────────────────────────────────── + # ── Rocq metamodel proofs (hard gate) ───────────────────────────── rocq: name: Rocq Proofs needs: [test] runs-on: ubuntu-latest - continue-on-error: true timeout-minutes: 20 steps: - uses: actions/checkout@v6 diff --git a/proofs/rocq/BUILD.bazel b/proofs/rocq/BUILD.bazel index f65bc78..4153df3 100644 --- a/proofs/rocq/BUILD.bazel +++ b/proofs/rocq/BUILD.bazel @@ -24,16 +24,6 @@ rocq_library( deps = [":rivet_schema"], ) -# Combined metamodel target -rocq_library( - name = "rivet_metamodel", - srcs = [], - deps = [ - ":rivet_schema", - ":rivet_validation", - ], -) - # Proof verification test — confirms all proofs compile and check rocq_proof_test( name = "rivet_metamodel_test", @@ -41,5 +31,8 @@ rocq_proof_test( "Schema.v", "Validation.v", ], - deps = [":rivet_metamodel"], + deps = [ + ":rivet_schema", + ":rivet_validation", + ], ) diff --git a/rivet-core/src/proofs.rs b/rivet-core/src/proofs.rs index b2575bb..889296a 100644 --- a/rivet-core/src/proofs.rs +++ b/rivet-core/src/proofs.rs @@ -669,6 +669,7 @@ mod proofs { let ctx = EvalContext { artifact: &artifact, graph: &graph, + store: None, }; let expr = arb_expr(2); @@ -688,6 +689,7 @@ mod proofs { let ctx = EvalContext { artifact: &artifact, graph: &graph, + store: None, }; let a = arb_expr(2); @@ -714,6 +716,7 @@ mod proofs { let ctx = EvalContext { artifact: &artifact, graph: &graph, + store: None, }; let a = arb_expr(2); @@ -738,6 +741,7 @@ mod proofs { let ctx = EvalContext { artifact: &artifact, graph: &graph, + store: None, }; let a = arb_expr(2); @@ -764,6 +768,7 @@ mod proofs { let ctx = EvalContext { artifact: &artifact, graph: &graph, + store: None, }; let a = arb_expr(2); From 89e14a9c20f24bb04b1926755902904352fd1145 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Mon, 20 Apr 2026 19:08:58 +0200 Subject: [PATCH 02/15] perf(serve): enforce node budget on /graph to prevent 57s render The /graph dashboard route previously ran layout + SVG over the full link graph (~1800 artifacts on the dogfood dataset), taking ~57s and producing ~1MB of HTML. The Playwright test at graph.spec.ts:17 was named "node budget prevents crash on full graph" but grepping the renderer for budget/max_nodes returned zero matches -- the budget was aspirational. This commit adds a real safety valve in render_graph_view: - DEFAULT_NODE_BUDGET = 200, MAX_NODE_BUDGET = 2000 (hard ceiling). - After the filtered subgraph is built but before the expensive pgv_layout + render_svg calls, short-circuit with a budget message when node_count > budget. - The message contains the literal string "budget" so the Playwright locator `svg, :text('budget')` matches and exposes the standard filter form (types / focus / depth / link_types / limit) so users can scope the view without editing URLs. - Per-request override via ?limit=NNN, clamped to [1, MAX_NODE_BUDGET]. - Filtered views under the budget (?types=requirement, ?focus=REQ-001&depth=2) continue to render SVG unchanged. Perf (release build, rivet dogfood dataset via serve_integration test): before after GET /graph ~57s / ~1MB ~1ms / 20KB GET /graph?types=requirement (filtered) ~1ms / 44KB (SVG) GET /graph?focus=REQ-001&depth=2 (filtered) ~44ms / 67KB (SVG) Three new integration tests in serve_integration.rs lock in the invariant: full graph stays under 5s and returns the budget message, focused view still renders SVG, and ?limit=1 forces the budget path. Implements: REQ-007 --- rivet-cli/src/render/graph.rs | 115 +++++++++++++++++++++++++++ rivet-cli/src/render/mod.rs | 2 + rivet-cli/src/serve/views.rs | 3 + rivet-cli/tests/serve_integration.rs | 106 ++++++++++++++++++++++++ 4 files changed, 226 insertions(+) diff --git a/rivet-cli/src/render/graph.rs b/rivet-cli/src/render/graph.rs index cd9cffe..a93e5eb 100644 --- a/rivet-cli/src/render/graph.rs +++ b/rivet-cli/src/render/graph.rs @@ -19,8 +19,20 @@ pub(crate) struct GraphParams { pub(crate) link_types: Option, pub(crate) depth: usize, pub(crate) focus: Option, + /// Per-request override of the node budget. Capped at `MAX_NODE_BUDGET`. + pub(crate) limit: Option, } +/// Default node budget for the full-graph render. Above this, we refuse to +/// run layout + SVG (which is O(n log n) + O(n^2) on the rivet dogfood +/// dataset of ~1800 artifacts, taking ~57s and producing ~1MB of HTML). +/// Users can override via `?limit=NNN` up to `MAX_NODE_BUDGET`. +pub(crate) const DEFAULT_NODE_BUDGET: usize = 200; + +/// Hard ceiling on the node budget, even with explicit `?limit=` override. +/// Gives power users headroom but still caps worst-case render time. +pub(crate) const MAX_NODE_BUDGET: usize = 2000; + pub(crate) struct EgoParams { pub(crate) hops: usize, } @@ -169,6 +181,94 @@ fn default_layout_opts() -> LayoutOptions { } } +/// Render a short HTML page explaining the node budget was exceeded and +/// pointing the user at the filter controls (types / focus / limit). The +/// Playwright regression locator `svg, :text('budget')` matches the word +/// "budget" in the body here. +fn render_budget_message( + store: &Store, + node_count: usize, + budget: usize, + type_filter: &Option>, + params: &GraphParams, +) -> String { + let mut html = String::from("

Traceability Graph

"); + + // Re-render the same filter form so users can scope the view without + // hand-editing the URL. Keep this in sync with the main render form. + html.push_str("
"); + html.push_str( + "
", + ); + + let mut all_types: Vec<&str> = store.types().collect(); + all_types.sort(); + html.push_str("
"); + for t in &all_types { + let checked = match type_filter { + Some(f) if f.iter().any(|x| x == *t) => " checked", + _ => "", + }; + html.push_str(&format!( + "" + )); + } + html.push_str("
"); + + let focus_val = params.focus.as_deref().unwrap_or(""); + html.push_str(&format!( + "

\ +
", + html_escape(focus_val) + )); + + html.push_str(""); + for a in store.iter() { + html.push_str(&format!(""); + + let depth_val = if params.depth > 0 { params.depth } else { 3 }; + html.push_str(&format!( + "

\ +
" + )); + + let lt_val = params.link_types.as_deref().unwrap_or(""); + html.push_str(&format!( + "

\ +
", + html_escape(lt_val) + )); + + html.push_str(&format!( + "

\ +
" + )); + + html.push_str("

"); + html.push_str("
"); + html.push_str("
"); + + html.push_str(&format!( + "
\ +

Graph above node budget

\ +

Graph has {node_count} artifacts — above the render budget of {budget} nodes. \ + Rendering the full graph is disabled here because layout and SVG generation would take tens of seconds and produce ~1MB of HTML.

\ +

Narrow the view before the graph will render:

\ +
    \ +
  • Filter by artifact type with the checkboxes above, or ?types=requirement,test in the URL.
    • \ +
  • Focus on a single artifact and its neighborhood with ?focus=REQ-001&depth=2.
    • \ +
  • Raise the budget for this request with ?limit=NNN (capped at {MAX_NODE_BUDGET}).
    • \ +
\ +

Once the filtered subgraph is under the budget, the full graph renders normally.

\ +
" + )); + + html +} + pub(crate) fn render_graph_view(ctx: &RenderContext, params: &GraphParams) -> String { let store = ctx.store; let link_graph = ctx.graph; @@ -200,6 +300,21 @@ pub(crate) fn render_graph_view(ctx: &RenderContext, params: &GraphParams) -> St build_filtered_subgraph(pg, store, node_map, &type_filter, &link_filter) }; + // ── Node budget safety valve ───────────────────────────────────────── + // Layout + SVG is ~O(n^2) on the layered layout engine. On the rivet + // dogfood dataset (~1800 artifacts) it takes ~57s and produces ~1MB + // of HTML. If the caller hasn't narrowed the view to something + // renderable, short-circuit with an explanatory message that points + // them at the filter controls. REQ-007: dashboard must stay responsive. + let effective_budget = params + .limit + .unwrap_or(DEFAULT_NODE_BUDGET) + .clamp(1, MAX_NODE_BUDGET); + let node_count = sub.node_count(); + if node_count > effective_budget { + return render_budget_message(store, node_count, effective_budget, &type_filter, params); + } + let colors = type_color_map(); let svg_opts = SvgOptions { type_colors: colors.clone(), diff --git a/rivet-cli/src/render/mod.rs b/rivet-cli/src/render/mod.rs index 670c0ca..ac45703 100644 --- a/rivet-cli/src/render/mod.rs +++ b/rivet-cli/src/render/mod.rs @@ -152,6 +152,7 @@ pub(crate) fn render_page( link_types: None, depth: 0, focus: None, + limit: None, }; RenderResult { html: graph::render_graph_view(ctx, ¶ms), @@ -166,6 +167,7 @@ pub(crate) fn render_page( link_types: None, depth: 0, focus: None, + limit: None, }; RenderResult { html: graph::render_graph_view(ctx, ¶ms), diff --git a/rivet-cli/src/serve/views.rs b/rivet-cli/src/serve/views.rs index 38dff2d..dac79f6 100644 --- a/rivet-cli/src/serve/views.rs +++ b/rivet-cli/src/serve/views.rs @@ -89,6 +89,8 @@ pub(crate) struct GraphParams { #[serde(default = "default_depth")] depth: usize, focus: Option, + /// Optional override of the node render budget. Capped in the renderer. + limit: Option, } fn default_depth() -> usize { @@ -107,6 +109,7 @@ pub(crate) async fn graph_view( link_types: params.link_types, depth: params.depth, focus: params.focus, + limit: params.limit, }; Html(crate::render::graph::render_graph_view(&ctx, &rparams)) } diff --git a/rivet-cli/tests/serve_integration.rs b/rivet-cli/tests/serve_integration.rs index 999d65f..d4db671 100644 --- a/rivet-cli/tests/serve_integration.rs +++ b/rivet-cli/tests/serve_integration.rs @@ -817,3 +817,109 @@ fn test_reload_failure_preserves_state() { child.kill().ok(); child.wait().ok(); } + +// ── /graph node budget (REQ-007) ──────────────────────────────────────── + +/// The full graph on the dogfood dataset (~1800 artifacts) must respond +/// quickly by short-circuiting into the budget message rather than running +/// layout + SVG, which previously took ~57s and produced ~1MB of HTML. +#[test] +fn graph_full_view_respects_node_budget() { + let (mut child, port) = start_server(); + + let start = std::time::Instant::now(); + let (status, body, _) = fetch(port, "/graph", true); + let elapsed = start.elapsed(); + eprintln!( + "graph_full_view_respects_node_budget: GET /graph -> {} bytes in {elapsed:?}", + body.len() + ); + + assert_eq!(status, 200, "/graph must return 200"); + assert!( + body.contains("budget"), + "full /graph must render the budget message (literal 'budget') when over the limit" + ); + assert!( + elapsed < std::time::Duration::from_secs(5), + "/graph must respond fast when above node budget, took {elapsed:?}" + ); + + child.kill().ok(); + child.wait().ok(); +} + +/// A focused view (`?focus=REQ-001&depth=2`) stays under the budget and +/// must render SVG normally. +#[test] +fn graph_focused_view_renders_svg() { + let (mut child, port) = start_server(); + + let start = std::time::Instant::now(); + let (status, body, _) = fetch(port, "/graph?focus=REQ-001&depth=2", true); + let elapsed = start.elapsed(); + eprintln!( + "graph_focused_view_renders_svg: GET /graph?focus=REQ-001&depth=2 -> {} bytes in {elapsed:?}", + body.len() + ); + + assert_eq!(status, 200, "focused /graph must return 200"); + assert!( + body.contains("() + ); + + child.kill().ok(); + child.wait().ok(); +} + +/// A very low `?limit=` forces the budget message even for a tiny focus +/// subgraph, confirming the override is wired through. +#[test] +fn graph_limit_override_triggers_budget_message() { + let (mut child, port) = start_server(); + + // Depth 3 around REQ-001 typically pulls in >1 node; limit=1 guarantees + // we exceed the effective budget. + let (status, body, _) = fetch(port, "/graph?focus=REQ-001&depth=3&limit=1", true); + + assert_eq!(status, 200, "/graph?limit=1 must return 200"); + assert!( + body.contains("budget"), + "/graph with an overly-tight limit must render the budget message" + ); + + child.kill().ok(); + child.wait().ok(); +} + +/// `?types=requirement` filters the full graph down; if the filtered +/// subgraph is under the budget it must render SVG (regression test for +/// the existing `graph with type filter renders SVG` Playwright case). +#[test] +fn graph_type_filter_renders_when_under_budget() { + let (mut child, port) = start_server(); + + let start = std::time::Instant::now(); + let (status, body, _) = fetch(port, "/graph?types=requirement", true); + let elapsed = start.elapsed(); + let has_svg = body.contains(" {} bytes in {elapsed:?}, svg={has_svg}, budget={has_budget}", + body.len() + ); + + assert_eq!(status, 200, "/graph?types=requirement must return 200"); + // Either renders SVG (under budget) or renders the budget message — + // both are acceptable. The key invariant is that the response is fast + // and contains one of the two. + assert!( + body.contains(" Date: Mon, 20 Apr 2026 19:14:27 +0200 Subject: [PATCH 03/15] feat(ple): feature model + variants for rivet itself (dogfooding #128) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Ship a feature model that describes the real variability in rivet: compile-time cargo features, CLI deployment surfaces (cli / dashboard / LSP / MCP), built-in adapters, export formats, test-import formats, and init presets. Every declared feature maps 1:1 to something grep-able in the code: a cargo feature flag, a `rivet` subcommand, a format string dispatched by `export --format` / `import-results --format`, or an init preset in `resolve_preset()`. Closes the dogfooding gap for #128 — v0.4.0 shipped `rivet variant check`, but the rivet project itself had no feature model to feed it. Files: * artifacts/feature-model.yaml — root feature tree + constraints * artifacts/variants/minimal-ci.yaml — default-features cargo build, CLI-only deployment (what CI runs) * artifacts/variants/full-desktop.yaml — every surface, every preset, wasm + oslc cargo features on Real variability identified: * yaml-backend alternative (rowan-yaml default, serde-yaml-only fallback) * deployment-surface or-group (cli-only, dashboard, lsp-server, mcp-server) * adapters or-group with cargo-feature constraints (implies oslc-client feat-oslc; implies wasm-adapter feat-wasm) * export-formats / test-import-formats / init-presets or-groups * preset ↔ adapter constraints (preset-aadl implies aadl-adapter; preset-stpa implies stpa-yaml-adapter) * dashboard implies html-export (shared HTML pipeline) * reqif-export implies reqif-adapter (shared reqif module) Verification (both variants pass): $ rivet variant check --model artifacts/feature-model.yaml \ --variant artifacts/variants/minimal-ci.yaml Variant 'minimal-ci': PASS Effective features (40): aadl-adapter, adapters, baselines, cli-only, commits, core, coverage, deployment-surface, docs-cli, export-formats, generic-yaml-adapter, generic-yaml-export, hooks-infra, html-export, impact-analysis, init-presets, junit-adapter, junit-import, matrix, mutations, needs-json-adapter, needs-json-import, optional-cargo-features, preset-aadl, preset-dev, preset-stpa, query, reqif-adapter, reqif-export, rivet, rowan-yaml, schema-system, sexpr-language, snapshots, stpa-yaml-adapter, test-import-formats, validate, variant-mgmt, yaml-backend, zola-export $ rivet variant check --model artifacts/feature-model.yaml \ --variant artifacts/variants/full-desktop.yaml Variant 'full-desktop': PASS Effective features (58): ...minimal-ci set plus dashboard, lsp-server, mcp-server, oslc-client, wasm-adapter, feat-oslc, feat-wasm, and all 14 init presets (aspice, stpa-ai, cybersecurity, eu-ai-act, safety-case, do-178c, en-50128, iec-61508, iec-62304, iso-pas-8800, sotif, plus the three in minimal-ci). Notes from reading the code: * `rowan-yaml` cargo feature: default-on, with a `cfg(not(feature = "rowan-yaml"))` fallback path in rivet-core/src/db.rs — so the alternative group has two real arms, not one. * `aadl` cargo feature: default-on. Modelled as a mandatory (always-present) adapter since no real build disables it — not as an optional-feature toggle. * `oslc` and `wasm`: off-by-default cargo features, correctly modelled as optional with implies-constraints from the adapters. * `lsp-server`, `dashboard`, `mcp-server` are *not* behind cargo features — they're always compiled in today. The variance is runtime/deployment, not compile-time. Flagged this as a surprising mismatch with the v0.4.0 narrative (where LSP/MCP are described as optional deployment surfaces): they are, but only in the sense of "whether you launch that process", not "whether the code is in the binary". * The rowan YAML parser rejects multi-line `#` comments between mapping entries at the same indent (`expected mapping key, found Some(Comment)`). Worked around by keeping single-line section comments in feature-model.yaml; flagging this as a latent parser bug worth a follow-up issue. Refs: #128 --- artifacts/feature-model.yaml | 254 +++++++++++++++++++++++++++ artifacts/variants/full-desktop.yaml | 50 ++++++ artifacts/variants/minimal-ci.yaml | 28 +++ 3 files changed, 332 insertions(+) create mode 100644 artifacts/feature-model.yaml create mode 100644 artifacts/variants/full-desktop.yaml create mode 100644 artifacts/variants/minimal-ci.yaml diff --git a/artifacts/feature-model.yaml b/artifacts/feature-model.yaml new file mode 100644 index 0000000..abe23f8 --- /dev/null +++ b/artifacts/feature-model.yaml @@ -0,0 +1,254 @@ +# Feature model for rivet itself (dogfooding the PLE system shipped in v0.4.0). +# +# This model describes the real variability in the rivet tool — both +# compile-time (cargo features) and runtime/deployment-time surface +# choices. Features that don't actually exist in the code are excluded; +# the declared features map 1:1 to either a cargo feature, a cargo +# binary subcommand, an export format, or an init preset. +# +# Verify with: +# rivet variant check --model artifacts/feature-model.yaml \ +# --variant artifacts/variants/minimal-ci.yaml +# rivet variant check --model artifacts/feature-model.yaml \ +# --variant artifacts/variants/full-desktop.yaml +# +# Closes the dogfooding gap for issue #128. + +kind: feature-model +root: rivet + +features: + rivet: + group: mandatory + children: + - core + - yaml-backend + - deployment-surface + - adapters + - export-formats + - test-import-formats + - init-presets + - optional-cargo-features + + # Mandatory core: code not behind any #[cfg(feature)], always on. + core: + group: mandatory + children: + - sexpr-language + - schema-system + - validate + - coverage + - matrix + - query + - mutations + - commits + - baselines + - snapshots + - impact-analysis + - variant-mgmt + - hooks-infra + - docs-cli + + sexpr-language: + group: leaf + schema-system: + group: leaf + validate: + group: leaf + coverage: + group: leaf + matrix: + group: leaf + query: + group: leaf + mutations: + group: leaf + commits: + group: leaf + baselines: + group: leaf + snapshots: + group: leaf + impact-analysis: + group: leaf + variant-mgmt: + group: leaf + hooks-infra: + group: leaf + docs-cli: + group: leaf + + # YAML backend: rowan-yaml cargo feature (default on) or serde_yaml fallback. + yaml-backend: + group: alternative + children: + - rowan-yaml + - serde-yaml-only + + rowan-yaml: + group: leaf + serde-yaml-only: + group: leaf + + # Deployment surface: which subcommands a deployment actually exposes. + deployment-surface: + group: or + children: + - cli-only + - dashboard + - lsp-server + - mcp-server + + cli-only: + group: leaf + dashboard: + group: leaf + lsp-server: + group: leaf + mcp-server: + group: leaf + + # Import adapters (aadl default-on; oslc, wasm off-by-default cargo features). + adapters: + group: or + children: + - stpa-yaml-adapter + - generic-yaml-adapter + - aadl-adapter + - needs-json-adapter + - junit-adapter + - reqif-adapter + - oslc-client + - wasm-adapter + + stpa-yaml-adapter: + group: leaf + generic-yaml-adapter: + group: leaf + aadl-adapter: + group: leaf + needs-json-adapter: + group: leaf + junit-adapter: + group: leaf + reqif-adapter: + group: leaf + oslc-client: + group: leaf + wasm-adapter: + group: leaf + + # Export formats dispatched by `rivet export --format `. + export-formats: + group: or + children: + - reqif-export + - generic-yaml-export + - html-export + - zola-export + + reqif-export: + group: leaf + generic-yaml-export: + group: leaf + html-export: + group: leaf + zola-export: + group: leaf + + # Test-result import: `rivet import-results --format `. + test-import-formats: + group: or + children: + - junit-import + - needs-json-import + + junit-import: + group: leaf + needs-json-import: + group: leaf + + # Init presets exposed via `rivet init --preset `. + init-presets: + group: or + children: + - preset-dev + - preset-aspice + - preset-stpa + - preset-stpa-ai + - preset-cybersecurity + - preset-aadl + - preset-eu-ai-act + - preset-safety-case + - preset-do-178c + - preset-en-50128 + - preset-iec-61508 + - preset-iec-62304 + - preset-iso-pas-8800 + - preset-sotif + + preset-dev: + group: leaf + preset-aspice: + group: leaf + preset-stpa: + group: leaf + preset-stpa-ai: + group: leaf + preset-cybersecurity: + group: leaf + preset-aadl: + group: leaf + preset-eu-ai-act: + group: leaf + preset-safety-case: + group: leaf + preset-do-178c: + group: leaf + preset-en-50128: + group: leaf + preset-iec-61508: + group: leaf + preset-iec-62304: + group: leaf + preset-iso-pas-8800: + group: leaf + preset-sotif: + group: leaf + + # Off-by-default cargo features a build may opt into. + optional-cargo-features: + group: optional + children: + - feat-oslc + - feat-wasm + + feat-oslc: + group: leaf + feat-wasm: + group: leaf + +constraints: + # Cargo feature consistency: adapter modules gated by their features. + - (implies oslc-client feat-oslc) + - (implies wasm-adapter feat-wasm) + + # ReqIF export shares the reqif module with reqif-adapter. + - (implies reqif-export reqif-adapter) + + # Preset ↔ schema-bundle: presets that seed schemas requiring a + # specific adapter imply that adapter. + - (implies preset-aadl aadl-adapter) + - (implies preset-stpa stpa-yaml-adapter) + - (implies preset-stpa-ai stpa-yaml-adapter) + + # Dashboard renders via the same HTML pipeline as html-export. + - (implies dashboard html-export) + + # LSP server's in-memory check reuses validate (which is mandatory + # anyway; assert explicitly). + - (implies lsp-server validate) + + # Test-import ↔ adapter consistency. + - (implies junit-import junit-adapter) + - (implies needs-json-import needs-json-adapter) diff --git a/artifacts/variants/full-desktop.yaml b/artifacts/variants/full-desktop.yaml new file mode 100644 index 0000000..12d9d5b --- /dev/null +++ b/artifacts/variants/full-desktop.yaml @@ -0,0 +1,50 @@ +# Full desktop developer variant of rivet. +# +# Everything a developer interactively uses: CLI + dashboard + LSP +# (for vscode-rivet) + MCP server (for Claude Code / other MCP hosts), +# every export format, every init preset, every adapter, and the +# optional wasm + oslc cargo features opted in. +# +# Build with: cargo build --release -p rivet-cli --features wasm +# (and enable rivet-core `oslc` via workspace). +# +# Verify with: +# rivet variant check --model artifacts/feature-model.yaml \ +# --variant artifacts/variants/full-desktop.yaml +name: full-desktop +selects: + - rowan-yaml + - cli-only + - dashboard + - lsp-server + - mcp-server + - stpa-yaml-adapter + - generic-yaml-adapter + - aadl-adapter + - needs-json-adapter + - junit-adapter + - reqif-adapter + - oslc-client + - wasm-adapter + - reqif-export + - generic-yaml-export + - html-export + - zola-export + - junit-import + - needs-json-import + - preset-dev + - preset-aspice + - preset-stpa + - preset-stpa-ai + - preset-cybersecurity + - preset-aadl + - preset-eu-ai-act + - preset-safety-case + - preset-do-178c + - preset-en-50128 + - preset-iec-61508 + - preset-iec-62304 + - preset-iso-pas-8800 + - preset-sotif + - feat-oslc + - feat-wasm diff --git a/artifacts/variants/minimal-ci.yaml b/artifacts/variants/minimal-ci.yaml new file mode 100644 index 0000000..ef68a76 --- /dev/null +++ b/artifacts/variants/minimal-ci.yaml @@ -0,0 +1,28 @@ +# Minimal CI variant of rivet. +# +# Matches `cargo build --release -p rivet-cli` with default features: +# rowan-yaml + aadl on, no optional cargo features, pure one-shot CLI +# use (no dashboard, LSP, or MCP server process). +# +# Verify with: +# rivet variant check --model artifacts/feature-model.yaml \ +# --variant artifacts/variants/minimal-ci.yaml +name: minimal-ci +selects: + - rowan-yaml + - cli-only + - stpa-yaml-adapter + - generic-yaml-adapter + - aadl-adapter + - needs-json-adapter + - junit-adapter + - reqif-adapter + - reqif-export + - generic-yaml-export + - html-export + - zola-export + - junit-import + - needs-json-import + - preset-dev + - preset-aadl + - preset-stpa From e0424d30d1c9c1d4ea7d568cc741bad3923092b4 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Mon, 20 Apr 2026 19:29:39 +0200 Subject: [PATCH 04/15] feat(audit): v0.4.0 artifacts, retroactive trailer map, Verus hard gate MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addresses three gaps found in the post-v0.4.0 dogfooding audit. **v0.4.0 shipped-work artifacts** — `artifacts/v040-features.yaml` was last touched 2026-04-12 and describes variant/PLE work (FEAT-106..114), not the verification pyramid that actually shipped on 2026-04-19. New file `artifacts/v040-verification.yaml` authors 4 design decisions (DD-052 four-layer verification pyramid, DD-053 suffix-based yaml-section matching, DD-054 non-blocking framing for formal CI jobs, DD-055 cfg-gate platform syscalls), 8 features (FEAT-115..122 covering Kani 27-harness expansion, differential YAML tests, operation-sequence proptest, STPA-Sec suite, suffix-based UCA extraction, nested control-action extraction, Zola export, Windows support), and 1 requirement (REQ-060 cross-platform binaries). Counts were verified against the actual codebase — 27 `#[kani::proof]` attrs in proofs.rs, 6 differential tests, 16 STPA-Sec tests. **Retroactive trailer map** — extended `AGENTS.md` with three more legacy orphans (51f2054a #126, f958a7ef, 75521b85 #44), a new v0.4.0 PR-level section for #150/#151/#152/#153, and an honest "genuinely-unmappable" section calling out `ca97dd9f` (#95) whose `SC-EMBED-*` trailers point to artifacts that were never authored. **Verus Proofs → hard gate** — rules_verus PR #21 (merged as 5bc96f39) fixes the hub-repo's ambiguous `:all` alias by emitting proper `toolchain()` wrappers per platform. Updates the git_override pin from e2c1600a (Feb 2026, broken) to 5bc96f39 and removes `continue-on-error: true` from the Verus job. Implements: REQ-030, REQ-060 Refs: DD-052, DD-053, DD-054, DD-055, FEAT-115, FEAT-116, FEAT-117, FEAT-118, FEAT-119, FEAT-120, FEAT-121, FEAT-122 Verifies: REQ-030 --- .github/workflows/ci.yml | 9 +- AGENTS.md | 25 ++ artifacts/v040-verification.yaml | 494 +++++++++++++++++++++++++++++++ verus/MODULE.bazel | 2 +- 4 files changed, 521 insertions(+), 9 deletions(-) create mode 100644 artifacts/v040-verification.yaml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c55ee47..15cc80c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -390,18 +390,11 @@ jobs: - uses: model-checking/kani-github-action@v1 - run: cargo kani -p rivet-core - # ── Verus SMT verification ────────────────────────────────────────── - # TODO: flip to hard gate once the upstream hub-repo bug in rules_verus - # is fixed. Currently the `:all` alias points to only the first platform's - # toolchain rather than registering toolchain() rules for each platform, - # so `register_toolchains("@verus_toolchains//:all")` resolves to a - # non-toolchain target and resolution fails. - # Upstream: https://github.com/pulseengine/rules_verus + # ── Verus SMT verification (hard gate) ─────────────────────────────── verus: name: Verus Proofs needs: [test] runs-on: ubuntu-latest - continue-on-error: true timeout-minutes: 20 steps: - uses: actions/checkout@v6 diff --git a/AGENTS.md b/AGENTS.md index ce78060..4c26afd 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -189,6 +189,31 @@ added as trailers without rewriting git history): | `c5ff64c8` | #96 | Embed phases 2+5 (diagnostics, matrix, snapshots) | Implements REQ-033 | | `cc4cc1c1` | #94 | oEmbed provider and Grafana JSON API | Implements FEAT-001 | | `adcf0bc1` | #28 | Phase 3 (30+ features, 402 tests, formal verification) | Implements REQ-004, REQ-012 | +| `51f2054a` | #126 | S-expression query language, MCP CRUD, variant/PLE artifacts, EU AI Act runtime evidence | Implements REQ-041, REQ-042, REQ-043, REQ-044, REQ-045, REQ-046, REQ-047, REQ-048, FEAT-106..108 | +| `f958a7ef` | — | `fix(ci):` — Miri, cargo-deny, cargo-audit CI failures | Exempt: `ci` type (rivet-commits mis-classifies `fix(ci):` as non-exempt; treat as exempt per CLAUDE.md) | +| `75521b85` | #44 | `rivet sync` — replace incompatible `git clone --config` | Fixes REQ-017 (external reference resolution) | + +### v0.4.0 Release PRs (2026-04-14 … 2026-04-19) + +PR-level merge commits for v0.4.0. The individual non-merge commits that feed +these PRs already carry trailers (or `Trace: skip` for release/test/platform +work). This table exists so auditors can trace the PR titles they see on +GitHub to the artifacts that document the work. + +| Commit | PR | Summary | Artifacts | +|--------|----|---------|-----------| +| `912530c5` | #150 | Verification pyramid + STPA bug fixes (merge) | Implements FEAT-115, FEAT-116, FEAT-117, FEAT-118, FEAT-119, FEAT-120, DD-052, DD-053, DD-054; Fixes REQ-002, REQ-004; Verifies REQ-030 | +| `913ce295` | #151 | Playwright regression fixes + rustls-webpki 0.103.12 + junit clippy (merge; `Trace: skip` on sub-commits) | Verifies FEAT-001 (dashboard E2E); Refs REQ-025 (junit adapter); deps-only otherwise | +| `9a46e86e` | #152 | `chore(release): v0.4.0` | Exempt: `chore` type | +| `aa706fc7` | #153 | Windows chmod gating (merge; `Trace: skip`) | Implements FEAT-122; Satisfies REQ-060; Refs DD-055 | + +### Commits that are genuinely unmappable + +- `ca97dd9f` (#95) — still carries broken refs to `SC-EMBED-1`/`-3`/`-4` + which do not exist in any artifacts file. Preserving for historical record; + the intended artifacts appear never to have been authored. An auditor + should treat the `satisfies SC-EMBED-*` trailers on that commit as + aspirational, not as evidence. ### Current Coverage diff --git a/artifacts/v040-verification.yaml b/artifacts/v040-verification.yaml new file mode 100644 index 0000000..52012de --- /dev/null +++ b/artifacts/v040-verification.yaml @@ -0,0 +1,494 @@ +# Artifacts for what actually shipped in v0.4.0 (2026-04-19): +# verification pyramid, STPA extraction fixes, Zola export, Windows build. +# +# Authored retroactively on 2026-04-19 to close the audit gap where +# v0.4.0 merged without artifacts covering the real release content. +# v040-features.yaml was last touched 2026-04-12 and described the +# variant/PLE work (FEAT-106..114), not the verification work. +artifacts: + + # ── Design decisions ──────────────────────────────────────────────── + + - id: DD-052 + type: design-decision + title: Four-layer verification pyramid (Rocq / Verus / Kani / dynamic) + status: approved + description: > + Core validation and extraction algorithms are verified at four + layers, each addressing a different failure mode. + Layer 1 — Rocq/coq-of-rust metamodel proofs (schemas/links consistency). + Layer 2 — Verus SMT functional correctness (validation soundness). + Layer 3 — Kani bounded model checking (panic freedom over bounded input). + Layer 4 — proptest + differential + mutation testing (coverage of + behaviour not expressible in formal contracts). + No single layer is sufficient: Rocq proves the schema model, Verus + proves the algorithm against its contract, Kani proves the actual + compiled Rust does not panic, and dynamic testing catches gaps in + the specs themselves. + tags: [verification, formal-methods, tool-qualification] + links: + - type: satisfies + target: REQ-030 + - type: satisfies + target: REQ-012 + fields: + rationale: > + Tool qualification for ISO 26262 TCL 1 requires evidence that + the tool produces correct output under all inputs it is exposed + to. Any one verification technique has known blind spots: + Kani cannot prove properties beyond a bounded depth, Verus + requires manual loop invariants that drift from the real code, + Rocq proves the model but not the implementation, and tests + cover only exercised paths. Stacking the four layers gives + coverage that compounds: a bug that slips past one is typically + caught by another. The v0.4.0 release wires all four into CI + so every PR runs them (though Kani/Verus/Rocq jobs are + non-blocking — see DD-054). + alternatives: > + (1) Tests only. Rejected: cannot claim tool qualification, no + coverage of unexercised edge cases. (2) Kani only. Rejected: + bounded depth means unbounded-input algorithms (parsers) aren't + covered past the bound. (3) Full Verus proofs of everything. + Rejected: proof-engineering cost is prohibitive, many Rust + patterns (trait objects, async) aren't yet supported. (4) One + external formal-verification consultant. Rejected: doesn't + scale to a daily-commit OSS project; proofs must live with the + code. + source-ref: > + AWS s2n-tls uses a similar pyramid: SAW proofs for crypto + primitives, Dafny for protocol state machines, libFuzzer for + wire format. The Rust compiler ships with Kani, Miri, + proptest, and compiletest in the same stack. docs/verification.md + describes the rivet instantiation. + provenance: + created-by: ai-assisted + model: claude-opus-4-7 + timestamp: 2026-04-19T12:00:00Z + + - id: DD-053 + type: design-decision + title: Suffix-based yaml-section matching for sub-artifact discovery + status: approved + description: > + Schemas may declare yaml-section-suffix in addition to the existing + yaml-section. Any top-level YAML key that ends with the declared + suffix (e.g. *-ucas) matches the artifact type. This replaces the + previous hardcoded section-name list that silently dropped + artifacts in projects using custom section names. + tags: [schema, yaml, extraction, stpa] + links: + - type: satisfies + target: REQ-002 + - type: satisfies + target: REQ-010 + fields: + rationale: > + Real STPA projects group UCAs by controller (e.g. + isle-rewriter-ucas, tower-supervisor-ucas). The pre-v0.4.0 + extractor only matched an exact "ucas" key, so these projects + reported 0 UCAs despite having dozens defined. Switching to a + suffix-based match keeps the canonical "ucas" working while + covering any per-controller grouping the project chooses, + without the schema having to enumerate every possible section + name. The same mechanism generalises to other STPA artifact + types with per-controller grouping (e.g. *-scenarios). + alternatives: > + (1) Keep the exact-match list, tell projects to rename their + sections. Rejected: breaks dogfooding for projects like loom + that predate rivet. (2) Full regex. Rejected: overkill, + anchor-escaping footguns, slower. (3) Per-project config file + listing extra section names. Rejected: duplicates information + already implicit in the suffix convention and creates a + second source of truth. + source-ref: > + See rivet-core/src/yaml_hir.rs suffix_patterns (introduced + 2026-04-14 in 9a27a53) and schemas/stpa.yaml uca type. + Closes #129. + provenance: + created-by: ai-assisted + model: claude-opus-4-7 + timestamp: 2026-04-19T12:00:00Z + + - id: DD-055 + type: design-decision + title: Gate platform-specific syscalls behind cfg attributes, not runtime detection + status: approved + description: > + Platform-specific code paths (POSIX permissions, fork/exec, + symlinks, signal handlers) are gated at compile time with + #[cfg(unix)] / #[cfg(windows)] rather than probed at runtime. + The default is "do the cross-platform thing unconditionally"; + the cfg branch only adds POSIX-specific extras when they apply. + tags: [platform, cross-platform, architecture] + links: + - type: satisfies + target: REQ-060 + - type: satisfies + target: REQ-007 + fields: + rationale: > + Compile-time gating catches platform bugs at build time on + each target, not in runtime logs on a user's machine. Runtime + probes (cfg!(unix), std::env::consts::OS) still compile the + POSIX-only type paths on Windows, producing "unresolved + import std::os::unix" errors — exactly the bug fixed in + aa706fc. The v0.4.0 Windows release binary failed precisely + because install_hook unconditionally imported PermissionsExt. + Gating with #[cfg(unix)] removes the import on non-Unix + targets and forces the author to think about the non-Unix + code path explicitly. + alternatives: > + (1) Runtime OS detection with cfg!(unix). Rejected: the + std::os::unix imports still need to compile on Windows, + defeating the purpose. (2) Wrapper crate abstracting + permissions. Rejected: overkill for one call site; introduces + a dependency to hide a three-line cfg branch. (3) Unix-only + builds. Rejected: we ship a Windows binary; dropping Windows + is not an option. + source-ref: > + rivet-cli/src/main.rs install_hook() (post-aa706fc state). + PR #153 retroactively links here. + provenance: + created-by: ai-assisted + model: claude-opus-4-7 + timestamp: 2026-04-19T12:00:00Z + + - id: DD-054 + type: design-decision + title: Non-blocking (continue-on-error) framing for formal-verification CI jobs + status: approved + description: > + The Kani, Verus, and Rocq CI jobs are wired with + continue-on-error: true. A failing formal job does not block + merges; a failing test/clippy/audit job still does. This is a + deliberate trade-off while the underlying toolchains (rules_verus, + rules_rocq_rust, kani-verifier GitHub Action) stabilise on + GitHub Actions runners. + tags: [ci, formal-methods, workflow, verification] + links: + - type: satisfies + target: REQ-012 + - type: satisfies + target: REQ-030 + fields: + rationale: > + Rivet depends on bleeding-edge formal-verification toolchains + whose Bazel+nix CI recipes have known transient failures + (cache misses, sandbox issues, occasional rules_verus + incompatibilities with nightly Rust). Blocking merges on these + would grind development to a halt for reasons unrelated to + correctness. Running them non-blocking still gives (a) regression + signal (PR author sees the red check), (b) trend data in the + Actions history, and (c) a path to flipping the gate once the + toolchains stabilise. Honest caveat: as of v0.4.0 none of the + three formal jobs have executed green end-to-end on CI; the + current state is "wired up, actively stabilising". This + decision and the caveat are documented so future auditors are + not misled by the green overall CI badge. + alternatives: > + (1) Hard gate from day one. Rejected: would have blocked the + v0.4.0 release on toolchain flakes unrelated to the artifacts + being verified. (2) Run formal jobs only on schedule (nightly). + Rejected: loses per-PR feedback, signal becomes stale. + (3) Omit from CI entirely until stable. Rejected: removes the + forcing function that drives stabilisation and removes + evidence for tool qualification that the proofs exist. + source-ref: > + .github/workflows/ci.yml jobs kani, verus, rocq (all carry + continue-on-error: true as of v0.4.0). + provenance: + created-by: ai-assisted + model: claude-opus-4-7 + timestamp: 2026-04-19T12:00:00Z + + # ── Features ──────────────────────────────────────────────────────── + + - id: FEAT-115 + type: feature + title: Kani bounded model checking expanded to 27 harnesses + status: approved + description: > + The Kani proof suite in rivet-core/src/proofs.rs grew from 15 to + 27 #[kani::proof] harnesses covering the core public API that + handles user-supplied input: commit trailer parsing + (parse_commit_type, extract_artifact_ids, expand_artifact_range, + parse_trailers), store upsert panic-freedom and retrievability + after type change, ArtifactDiff::compute over stores up to size 3, + mutation helpers (prefix_for_type, next_id, validate_link), + markdown rendering (render_markdown panic-freedom, + strip_html_tags invariant that output contains no angle brackets), + plus the previously existing 15 harnesses. Each harness proves + panic-freedom over all bounded inputs via exhaustive symbolic + execution. + tags: [verification, kani, formal-methods, phase-3] + links: + - type: satisfies + target: REQ-030 + - type: implements + target: DD-052 + - type: verifies + target: REQ-004 + fields: + baseline: v0.4.0 + acceptance-criteria: + - "Given the rivet-core crate, When cargo kani -p rivet-core runs, Then 27 harnesses are discovered" + - "Given any input in the bounded domain of each harness, When Kani enumerates it symbolically, Then no panic is reached" + - "Given strip_html_tags, When called on any bounded ASCII input, Then the output contains no '<' or '>'" + provenance: + created-by: ai-assisted + model: claude-opus-4-7 + timestamp: 2026-04-19T12:00:00Z + + - id: FEAT-116 + type: feature + title: Differential YAML parser tests (rowan vs serde_yaml) + status: approved + description: > + Six differential tests in rivet-core/tests/differential_yaml.rs + feed the same YAML input to both the new rowan-based CST parser + and serde_yaml, then assert the extracted artifact set (IDs, + types, links) is equivalent. Catches silent regressions between + the two parsers during the rowan migration tail and documents + expected divergences (comments, formatting) as explicit + test fixtures. + tags: [verification, differential-testing, yaml, parser, phase-3] + links: + - type: satisfies + target: REQ-030 + - type: verifies + target: REQ-028 + - type: verifies + target: REQ-034 + - type: implements + target: DD-052 + fields: + baseline: v0.4.0 + acceptance-criteria: + - "Given the same YAML artifact file, When parsed by rowan and by serde_yaml, Then the extracted artifact sets are equal" + - "Given a known divergence (e.g. comment preservation), When the differential runs, Then the divergence is asserted explicitly rather than surprising the reader" + provenance: + created-by: ai-assisted + model: claude-opus-4-7 + timestamp: 2026-04-19T12:00:00Z + + - id: FEAT-117 + type: feature + title: Operation-sequence property tests for the artifact store + status: approved + description: > + Three proptest properties in + rivet-core/tests/proptest_operations.rs fuzz random sequences of + insert/upsert/validate operations against store invariants. + Shrinks failing cases to minimal reproducers. Catches ordering + bugs, index-consistency violations, and state-corruption + regressions that unit tests miss because they exercise pre-chosen + call sequences. Runs 1000 cases per property in CI via + PROPTEST_CASES=1000. + tags: [verification, proptest, property-based, fuzzing, phase-3] + links: + - type: satisfies + target: REQ-030 + - type: verifies + target: REQ-004 + - type: verifies + target: REQ-014 + - type: implements + target: DD-052 + fields: + baseline: v0.4.0 + acceptance-criteria: + - "Given an arbitrary sequence of insert/upsert/validate operations, When the sequence runs against a store, Then all documented invariants hold at every step" + - "Given a failing sequence, When proptest shrinks, Then the minimal reproducer is reported" + provenance: + created-by: ai-assisted + model: claude-opus-4-7 + timestamp: 2026-04-19T12:00:00Z + + - id: FEAT-118 + type: feature + title: STPA-Sec verification test suite + status: approved + description: > + Sixteen #[test] functions in + rivet-core/tests/stpa_sec_verification.rs implement the test + cases catalogued in docs/verification.md §12. Coverage includes + XSS prevention in artifact rendering, commit-trailer traceability + round-trip, git-hook install/uninstall idempotency, document + embed resolution boundaries, and schema-level defences for the + STPA-Sec artifact types introduced in earlier releases. Provides + running evidence that the security-relevant controls described + in STPA-Sec artifacts are actually implemented. + tags: [verification, stpa-sec, security, phase-3] + links: + - type: verifies + target: REQ-004 + - type: verifies + target: REQ-002 + - type: satisfies + target: REQ-030 + - type: implements + target: DD-052 + fields: + baseline: v0.4.0 + acceptance-criteria: + - "Given the rivet-core crate, When cargo test --test stpa_sec_verification runs, Then 16 tests execute" + - "Given each STPA-Sec security control described in docs/verification.md §12, Then at least one test asserts the control is in place" + provenance: + created-by: ai-assisted + model: claude-opus-4-7 + timestamp: 2026-04-19T12:00:00Z + + - id: FEAT-119 + type: feature + title: Suffix-based STPA UCA extraction + status: approved + description: > + yaml_hir.rs builds a suffix_patterns table from schema types that + declare yaml-section-suffix and matches any top-level key whose + name ends with the declared suffix. schemas/stpa.yaml registers + yaml-section-suffix: "-ucas" for the uca type. Fixes #129: + projects that group UCAs per controller (e.g. + isle-rewriter-ucas, tower-supervisor-ucas) previously reported + 0 UCAs because the extractor only matched exact "ucas". Now all + *-ucas sections are discovered. + tags: [stpa, yaml, extraction, bugfix] + links: + - type: implements + target: DD-053 + - type: satisfies + target: REQ-002 + - type: satisfies + target: REQ-010 + fields: + baseline: v0.4.0 + acceptance-criteria: + - "Given a YAML file with an *-ucas top-level section, When rivet extracts artifacts, Then the entries are registered as uca type" + - "Given a YAML file with the canonical 'ucas' section, When rivet extracts, Then behaviour is unchanged (no regression)" + - "Given the loom project with isle-rewriter-ucas, When rivet validate runs, Then UCA artifacts are discovered (regression test for #129)" + provenance: + created-by: ai-assisted + model: claude-opus-4-7 + timestamp: 2026-04-19T12:00:00Z + + - id: FEAT-120 + type: feature + title: Nested control-action extraction from STPA controllers + status: approved + description: > + yaml_hir.rs recursively traverses controller items and extracts + embedded control-actions: [{ca: ..., ...}] entries as first-class + control-action artifacts, automatically creating an issued-by + link back to the parent controller. Recognises "ca" as an ID + field alias. Closes #130: previously, projects that nested + control-actions inside controllers (the natural YAML structure) + reported 0 control-action artifacts. + tags: [stpa, yaml, extraction, bugfix] + links: + - type: implements + target: DD-053 + - type: satisfies + target: REQ-002 + - type: satisfies + target: REQ-010 + fields: + baseline: v0.4.0 + acceptance-criteria: + - "Given a controller item with nested control-actions, When rivet extracts artifacts, Then each nested ca is a separate control-action artifact" + - "Given a nested control-action in controller X, When rivet extracts, Then the artifact has an issued-by link to X" + - "Given a real STPA project using the nested form, When rivet validate runs, Then the control-action count is non-zero (regression test for #130)" + provenance: + created-by: ai-assisted + model: claude-opus-4-7 + timestamp: 2026-04-19T12:00:00Z + + - id: FEAT-121 + type: feature + title: Zola static-site export with multi-project namespacing + status: approved + description: > + rivet export --format zola renders the artifact store as a Zola + content tree with per-artifact pages, resolved [[wiki-links]], + CommonMark rendering (including mermaid blocks), TOML + front-matter with escaped strings and date handling, and + per-project prefixing via --prefix so multiple rivet projects + can be unioned into one Zola site without ID collisions. + Validation results are written to data//validation.json + per REQ-049. The export is additive to existing HTML export + (FEAT-066) and does not replace it. + tags: [export, zola, static-site, documentation] + links: + - type: satisfies + target: REQ-036 + - type: satisfies + target: REQ-049 + - type: satisfies + target: REQ-007 + fields: + baseline: v0.4.0 + acceptance-criteria: + - "Given a rivet project, When rivet export --format zola --prefix foo runs, Then a Zola content tree is produced under content/foo/" + - "Given artifacts containing [[IDs]], When exported, Then wiki-links resolve to relative Zola paths" + - "Given a title containing TOML-special characters, When exported, Then the front-matter is still valid TOML" + - "Given validation results, When exported, Then data/foo/validation.json contains PASS/FAIL, counts, timestamp, and git commit" + provenance: + created-by: ai-assisted + model: claude-opus-4-7 + timestamp: 2026-04-19T12:00:00Z + + - id: FEAT-122 + type: feature + title: Windows cross-platform support for hook installation + status: approved + description: > + install_hook() in rivet-cli/src/main.rs gates the POSIX + set_permissions(0o755) call behind #[cfg(unix)], so the Windows + build no longer fails with E0433/E0599 on + std::os::unix::fs::PermissionsExt. On Windows, Git-Bash runs + hooks via its own shim regardless of NTFS executable bits, so + skipping the chmod is semantically correct. Unblocks the v0.4.0 + cross-platform release binary for Windows. + tags: [platform, windows, bugfix] + links: + - type: satisfies + target: REQ-060 + - type: implements + target: DD-055 + - type: satisfies + target: REQ-051 + fields: + baseline: v0.4.0 + acceptance-criteria: + - "Given a Windows build of rivet, When cargo build --release runs, Then the build succeeds" + - "Given rivet init --hooks on Windows, When run in a git repo, Then the hook files are created under .git/hooks/ without a permissions error" + - "Given rivet init --hooks on Linux/macOS, When run, Then hooks are still installed with 0o755 (no regression)" + provenance: + created-by: ai-assisted + model: claude-opus-4-7 + timestamp: 2026-04-19T12:00:00Z + + # ── Requirements ──────────────────────────────────────────────────── + + - id: REQ-060 + type: requirement + title: Cross-platform binary support + status: approved + description: > + Rivet must build and run on Linux, macOS, and Windows. Platform- + specific code must be gated behind cfg attributes rather than + assumed. The release workflow must publish binaries for all + three platforms. Integration tests that exercise platform- + specific paths (file permissions, path separators, process + spawning) must be gated behind the matching cfg so they compile + on every supported target. + tags: [platform, cross-platform, release] + links: + - type: satisfies + target: REQ-007 + fields: + priority: must + category: non-functional + baseline: v0.4.0 + provenance: + created-by: ai-assisted + model: claude-opus-4-7 + timestamp: 2026-04-19T12:00:00Z diff --git a/verus/MODULE.bazel b/verus/MODULE.bazel index e649633..fad8cf0 100644 --- a/verus/MODULE.bazel +++ b/verus/MODULE.bazel @@ -19,7 +19,7 @@ bazel_dep(name = "rules_verus", version = "0.1.0") git_override( module_name = "rules_verus", remote = "https://github.com/pulseengine/rules_verus.git", - commit = "e2c1600a8cca4c0deb78c5fcb4a33f1da2273d29", + commit = "5bc96f39cb4ccf5028a8cca94950f4bee6405423", ) # ── Verus toolchain registration ─────────────────────────────────────── From 7de792668d52f2cb971e1d1d38f2b53c40d17737 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Mon, 20 Apr 2026 20:36:38 +0200 Subject: [PATCH 05/15] fix(ci): honest feedback on first hard-gate run MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit First run of the flipped hard gates exposed real issues: - **Kani**: `eval_context(artifact: &Artifact)` had an unused param after the store-building refactor. cfg(kani) hid it from `cargo check`; CI's `-D warnings` caught it. Prefixed with `_artifact`. - **Rocq**: Schema.v / Validation.v opened `string_scope` but used `++` on `Store` (a list). Rocq 9.0.1 parses `++` in string_scope as `String.append`, so `s ++ [a]` failed with "s has type Store while expected string". Added `Open Scope list_scope.` after the string open so list concatenation takes precedence. Neither file uses string `++` so the scope swap is safe. - **Verus**: unblocked the `:all` alias bug via upstream rules_verus PR (5bc96f39), but hit a deeper upstream issue — rules_rust 0.56.0 references `CcInfo` which has been removed from current Bazel. Needs a rules_rust bump inside rules_verus before Verus can be a hard gate. Reverted to `continue-on-error: true` with a pointer comment so this is honestly signposted rather than silently advertised as shipped. Mutation Testing rivet-cli passed on the first run. rivet-core still running. /graph budget works in CI (included in the same PR). Implements: REQ-030 --- .github/workflows/ci.yml | 9 ++++++++- proofs/rocq/Schema.v | 1 + proofs/rocq/Validation.v | 1 + rivet-core/src/proofs.rs | 2 +- 4 files changed, 11 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 15cc80c..0a4be48 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -390,11 +390,18 @@ jobs: - uses: model-checking/kani-github-action@v1 - run: cargo kani -p rivet-core - # ── Verus SMT verification (hard gate) ─────────────────────────────── + # ── Verus SMT verification ────────────────────────────────────────── + # Not yet a hard gate. Upstream chain blocks us: rules_verus (pinned at + # pulseengine/rules_verus@5bc96f39, our fix for the :all alias bug) + # depends on rules_rust 0.56.0, which uses the removed `CcInfo` symbol + # and fails to load in current Bazel. Needs either a rules_rust bump + # in rules_verus or a wrapper around the removed symbol before this + # can be flipped back to a hard gate. verus: name: Verus Proofs needs: [test] runs-on: ubuntu-latest + continue-on-error: true timeout-minutes: 20 steps: - uses: actions/checkout@v6 diff --git a/proofs/rocq/Schema.v b/proofs/rocq/Schema.v index 74dda05..35fa1ae 100644 --- a/proofs/rocq/Schema.v +++ b/proofs/rocq/Schema.v @@ -25,6 +25,7 @@ Require Import Coq.Arith.Arith. Import ListNotations. Open Scope string_scope. +Open Scope list_scope. (* ========================================================================= *) (** * Section 1: Domain Types *) diff --git a/proofs/rocq/Validation.v b/proofs/rocq/Validation.v index 2e1f80d..58653e3 100644 --- a/proofs/rocq/Validation.v +++ b/proofs/rocq/Validation.v @@ -27,6 +27,7 @@ Import ListNotations. Require Import Schema. Open Scope string_scope. +Open Scope list_scope. (* ========================================================================= *) (** * Section 1: Validation as a Pure Function *) diff --git a/rivet-core/src/proofs.rs b/rivet-core/src/proofs.rs index 889296a..bfe78a6 100644 --- a/rivet-core/src/proofs.rs +++ b/rivet-core/src/proofs.rs @@ -590,7 +590,7 @@ mod proofs { } /// Build an eval context with empty link graph. - fn eval_context(artifact: &Artifact) -> (LinkGraph, Store) { + fn eval_context(_artifact: &Artifact) -> (LinkGraph, Store) { let store = Store::new(); let schema = empty_schema(); let graph = LinkGraph::build(&store, &schema); From 0cacaac371ed1a7d2191dabdc207144b24568e34 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Mon, 20 Apr 2026 20:42:22 +0200 Subject: [PATCH 06/15] fix(rocq): drop Open Scope string_scope, tag string literals MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `Open Scope string_scope.` at the top of Schema.v / Validation.v shadowed `length` (String.length vs List.length) and `++` (String.append vs List.app), breaking every Store operation once the proofs got compiled under Rocq 9.0.1. Neither file actually uses infix string operators — all string literals are either passed to `String.eqb` or constructed with explicit `%string` tags. Drop the scope open; tag the one remaining bare literal `"broken-link"` in Validation.v:120 with `%string`. Explanatory comment in both files so a future reader doesn't reopen string_scope and re-break this. --- proofs/rocq/Schema.v | 8 ++++++-- proofs/rocq/Validation.v | 7 ++++--- 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/proofs/rocq/Schema.v b/proofs/rocq/Schema.v index 35fa1ae..fa48400 100644 --- a/proofs/rocq/Schema.v +++ b/proofs/rocq/Schema.v @@ -24,8 +24,12 @@ Require Import Coq.Bool.Bool. Require Import Coq.Arith.Arith. Import ListNotations. -Open Scope string_scope. -Open Scope list_scope. +(* We deliberately do NOT `Open Scope string_scope.` here: string_scope + * shadows `length` (picks String.length over List.length) and `++` + * (picks String.append over List.app), which silently mis-type every + * Store operation in this file. All strings used here appear either + * as quoted literals or via fully-qualified `String.eqb`, so the + * default list_scope is what we want. *) (* ========================================================================= *) (** * Section 1: Domain Types *) diff --git a/proofs/rocq/Validation.v b/proofs/rocq/Validation.v index 58653e3..93b8256 100644 --- a/proofs/rocq/Validation.v +++ b/proofs/rocq/Validation.v @@ -26,8 +26,9 @@ Import ListNotations. Require Import Schema. -Open Scope string_scope. -Open Scope list_scope. +(* Mirroring Schema.v: no `Open Scope string_scope` — it shadows + * List.length / List.app. All string literals in this file carry + * an explicit `%string` scope annotation. *) (* ========================================================================= *) (** * Section 1: Validation as a Pure Function *) @@ -117,7 +118,7 @@ Proof. - simpl in Hin. destruct Hin as [Heq | Hin_rest]. + subst h. simpl. rewrite Habs. - exists (mkDiagnostic SevError (Some (art_id a)) "broken-link" (link_target l)). + exists (mkDiagnostic SevError (Some (art_id a)) "broken-link"%string (link_target l)). split. * apply in_or_app. left. left. reflexivity. * simpl. split; reflexivity. From bdc63f2f3c8ae6278d9badadfe9a56bfd043f78a Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Mon, 20 Apr 2026 20:59:22 +0200 Subject: [PATCH 07/15] fix(rocq): fully qualify List.length in proofs With `Require Import Coq.Strings.String` after `Coq.Lists.List`, the bare identifier `length` resolves to `String.length` (the latest import wins), so `length s` with `s : Store` fails to typecheck. Qualify every `length` call against a list as `List.length` so name resolution cannot drift. Five call sites across Schema.v / Validation.v. --- proofs/rocq/Schema.v | 6 +++--- proofs/rocq/Validation.v | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/proofs/rocq/Schema.v b/proofs/rocq/Schema.v index fa48400..a6f48f1 100644 --- a/proofs/rocq/Schema.v +++ b/proofs/rocq/Schema.v @@ -284,7 +284,7 @@ Qed. is bounded by |store| * |rules| * max_links. *) Definition validation_work (s : Store) (rules : list TraceRule) : nat := - length s * length rules. + List.length s * List.length rules. (** The empty store requires zero work. *) Lemma validation_empty_store : forall rules, @@ -304,7 +304,7 @@ Qed. (** Adding one artifact adds at most |rules| checks. *) Lemma validation_work_add_one : forall s a rules, validation_work (s ++ [a]) rules = - validation_work s rules + length rules. + validation_work s rules + List.length rules. Proof. intros. unfold validation_work. rewrite app_length. simpl. @@ -559,7 +559,7 @@ Qed. (** Count how many artifacts of a given kind lack the required link. *) Definition count_violations (s : Store) (r : TraceRule) : nat := - length (filter + List.length (filter (fun a => artifact_kind_eqb (art_kind a) (rule_source_kind r) && negb (existsb (fun l => link_kind_eqb (link_kind l) (rule_link_kind r) && diff --git a/proofs/rocq/Validation.v b/proofs/rocq/Validation.v index 93b8256..12a72a3 100644 --- a/proofs/rocq/Validation.v +++ b/proofs/rocq/Validation.v @@ -173,7 +173,7 @@ Qed. (** The number of diagnostics is bounded by store size * (max_links + rules). *) Lemma check_broken_links_length : forall s a, - length (check_broken_links s a) <= length (art_links a). + List.length (check_broken_links s a) <= List.length (art_links a). Proof. intros s a. unfold check_broken_links. @@ -186,7 +186,7 @@ Proof. Qed. Lemma check_artifact_rules_length : forall s a rules, - length (check_artifact_rules s a rules) <= length rules. + List.length (check_artifact_rules s a rules) <= List.length rules. Proof. intros s a rules. unfold check_artifact_rules. From 6329d34b680947957f0fdbc331e42256434be6f8 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Mon, 20 Apr 2026 21:15:48 +0200 Subject: [PATCH 08/15] fix(rocq): apply -> eapply reach_direct for constructor with implicit lk `reach_direct` has a forall-bound `lk : LinkKind` that isn't surfaced in the goal after `apply`. Rocq 9.0.1 refuses the implicit instantiation that older versions allowed, fails with "Unable to find an instance for the variable lk". Using `eapply` creates a metavariable that unifies when the inner `exact Hl1_kind` step substitutes the real link kind. --- proofs/rocq/Schema.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/rocq/Schema.v b/proofs/rocq/Schema.v index a6f48f1..f22f526 100644 --- a/proofs/rocq/Schema.v +++ b/proofs/rocq/Schema.v @@ -506,7 +506,7 @@ Proof. intros s r1 r2 a1 a2 Hr1 Hr2 Hin1 Hk1 Hchain Hin2 Hk2 Hsat1 Hsat2. unfold artifact_satisfies_rule in Hsat1. destruct Hsat1 as [l1 [Hl1_in [Hl1_kind [t1 [Ht1_in [Ht1_id Ht1_kind]]]]]]. - apply reach_direct. + eapply reach_direct. exists a1. split; [exact Hin1 |]. split; [reflexivity |]. unfold has_link_to. From 68ad2c7ff6afbc86b4006f6a6d16a972141afee4 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Mon, 20 Apr 2026 21:43:42 +0200 Subject: [PATCH 09/15] fix(rocq): admit vmodel_chain_two_steps honestly (real proof gap) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `apply reach_direct` + `eapply reach_direct` routes both fail under Rocq 9.0.1 because the proof has an actual hole: `t1` (the link target artifact introduced by destructing `artifact_satisfies_rule`) is not the same as `a2` (the caller-supplied intermediate). The goal after the link-wiring step reduces to `link_target l1 = art_id a2`, but we only have `art_id t1 = link_target l1` — nothing ties `t1` to `a2`. Rather than write around the gap with tactics that wouldn't hold, mark the theorem `Admitted.` with an explicit comment describing what the correct strengthening would look like. All other theorems in Schema.v / Validation.v remain Qed'd. This lets the Rocq hard gate actually compile and enforce the proofs we DO have, rather than hiding a stale semantic break behind a tactic that just happened to typecheck on older Rocq. --- proofs/rocq/Schema.v | 30 +++++++++++++++++++----------- 1 file changed, 19 insertions(+), 11 deletions(-) diff --git a/proofs/rocq/Schema.v b/proofs/rocq/Schema.v index f22f526..406e44d 100644 --- a/proofs/rocq/Schema.v +++ b/proofs/rocq/Schema.v @@ -487,7 +487,24 @@ Inductive reachable (s : Store) : string -> string -> Prop := reachable s src tgt. (** If two consecutive rules are satisfied and there exist matching artifacts, - then the source of the first rule can reach the target of the second. *) + then the source of the first rule can reach the target of the second. + + Honest status: this theorem is currently [Admitted]. As stated, it is + under-constrained — the proof needs to connect the anonymous link + target [t1] (the artifact satisfying [a1]'s outgoing [r1] link) to the + named [a2] (the intermediate the caller supplied). Without an + additional hypothesis [art_id t1 = art_id a2] or a lemma forcing + artifact-id uniqueness, the chain doesn't close. + + The correct strengthening is likely one of: + 1. Add [art_id t1 = art_id a2] as an explicit premise. + 2. Quantify existentially over the middle artifact rather than + taking [a2] as a parameter. + 3. Prove an "ID-uniqueness" lemma and use it to identify t1 with a2. + + Leaving Admitted with this note rather than claiming a proof we + don't have. All other theorems in Schema.v and Validation.v are + Qed'd. *) Theorem vmodel_chain_two_steps : forall s r1 r2 a1 a2, rule_satisfied s r1 -> @@ -503,16 +520,7 @@ Theorem vmodel_chain_two_steps : artifact_satisfies_rule s a2 r2 -> reachable s (art_id a1) (art_id a2). Proof. - intros s r1 r2 a1 a2 Hr1 Hr2 Hin1 Hk1 Hchain Hin2 Hk2 Hsat1 Hsat2. - unfold artifact_satisfies_rule in Hsat1. - destruct Hsat1 as [l1 [Hl1_in [Hl1_kind [t1 [Ht1_in [Ht1_id Ht1_kind]]]]]]. - eapply reach_direct. - exists a1. split; [exact Hin1 |]. - split; [reflexivity |]. - unfold has_link_to. - exists l1. split; [exact Hl1_in |]. - split; [exact Ht1_id | exact Hl1_kind]. -Qed. +Admitted. (* ========================================================================= *) (** * Section 11: Conditional Rule Support *) From 653dca8c1e714af29a4694137ceacc21f543c9d8 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 21 Apr 2026 06:14:08 +0200 Subject: [PATCH 10/15] fix(ci): honest gate status after first real run MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The first hard-gate run surfaced issues deeper than one-line fixes. This commit restores honesty rather than hiding them: **Hard gates that stay on:** - Kani compile errors (`store: None`, `_artifact`) — fixed, but see below. - Rocq `Open Scope list_scope.` + `List.length` qualification + `eapply reach_direct` — applied. - Mutation Testing (rivet-cli): 0 surviving mutants, hard gate. **Jobs moved back to continue-on-error with TODOs:** - **Kani**: 27-harness suite exceeded the 30-min CI budget and got cancelled. Bumped timeout to 45 min and left continue-on-error on until we scope the PR-sized subset vs nightly full suite. - **Rocq**: Rocq 9.0.1 is stricter than the version the proofs were written against. Fixed three classes of errors; a fourth (`No such contradiction` in a destructure) remains unfixed. Also `vmodel_chain_two_steps` has a genuine proof gap (link target t1 ≠ caller's a2 without an extra hypothesis) and is now `Admitted.` with an explicit note. Needs a systematic port pass before hard-gating. - **Mutation Testing (rivet-core)**: 3677 mutants, real surviving ones in `collect_yaml_files` / `import_with_schema` (lib.rs:80,241,268) and `bazel.rs::lex` (delete match arm `b'\r'`). Those are actual test coverage gaps. Hard-gating rivet-core means writing tests to kill every one of them first; scoping that out of this PR. rivet-cli mutation stays hard-gated per above. - **Verus**: still blocked on rules_rust 0.56 `CcInfo` removal upstream. The goal of "real hard gates" was to stop advertising verification that never ran green. Three checkpoints are now genuine (rivet-cli mutations, Kani compile-clean once unblocked, Rocq compile-clean once ported). The rest have explicit follow-up notes in ci.yml pointing at what needs to happen before they flip. --- .github/workflows/ci.yml | 29 +++++++++++++++++++++++++---- 1 file changed, 25 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0a4be48..33d568f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -285,13 +285,22 @@ jobs: env: PROPTEST_CASES: "1000" - # ── Mutation testing (hard gate — zero surviving mutants) ──────────── + # ── Mutation testing ───────────────────────────────────────────────── # Split per-crate into parallel jobs so each has its own 45-min budget. + # + # rivet-cli: hard gate (0 surviving mutants as of this commit). + # rivet-core: NOT a hard gate — 3677 mutants, known-surviving ones in + # lib.rs (collect_yaml_files, import_with_schema branches) and bazel.rs + # lex(). Need targeted tests before this can be flipped. See the + # per-crate `continue-on-error` below. mutants: name: Mutation Testing (${{ matrix.crate }}) needs: [test] runs-on: ubuntu-latest timeout-minutes: 45 + # Hard gate only for rivet-cli; rivet-core is still surfacing real + # coverage gaps that need tests written. Flip to `false` once killed. + continue-on-error: ${{ matrix.crate == 'rivet-core' }} strategy: fail-fast: false matrix: @@ -379,12 +388,17 @@ jobs: - name: Check supply chain run: cargo vet --locked - # ── Kani bounded model checking (hard gate) ───────────────────────── + # ── Kani bounded model checking ──────────────────────────────────── + # Not yet a hard gate: the 27-harness suite exceeds the 30-minute budget. + # Either needs scoping (run a subset on PRs, full suite nightly) or + # harness-by-harness unwind tuning. TODO: flip to hard gate once a + # PR-sized subset completes in <20 min. kani: name: Kani Proofs needs: [test] runs-on: ubuntu-latest - timeout-minutes: 30 + continue-on-error: true + timeout-minutes: 45 steps: - uses: actions/checkout@v6 - uses: model-checking/kani-github-action@v1 @@ -415,11 +429,18 @@ jobs: working-directory: verus run: bazel test //:rivet_specs_verify - # ── Rocq metamodel proofs (hard gate) ───────────────────────────── + # ── Rocq metamodel proofs ───────────────────────────────────────── + # Not yet a hard gate: the proofs were written against an older Rocq and + # hit multiple 9.0.1 compatibility issues (length/++ scope resolution — + # fixed; `apply` constructor inference — fixed via `eapply`; `No such + # contradiction` on some destructures — unfixed; vmodel_chain_two_steps + # has a real proof gap, currently Admitted with note). Needs systematic + # port. TODO: flip to hard gate after the Rocq 9 port PR. rocq: name: Rocq Proofs needs: [test] runs-on: ubuntu-latest + continue-on-error: true timeout-minutes: 20 steps: - uses: actions/checkout@v6 From fef63e615b322f7a45945925c07a1cc5e5728bfd Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 21 Apr 2026 06:41:19 +0200 Subject: [PATCH 11/15] ci(verus): flip to hard gate; bump rules_verus pin past CcInfo fix MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Verus job was marked continue-on-error because rules_verus's minimum rules_rust (0.56.0) used the Bazel built-in `CcInfo` symbol that current Bazel has removed, so the module failed to load. pulseengine/rules_verus@fc7b636 bumps the floor to 0.58.0 — the release where CcInfo is loaded from @rules_cc//cc/common:cc_info.bzl instead. Bumping our pin past that commit unblocks the load and lets the verus job run as a real gate. The same pin range (5e2b7c6) also picks up three correctness fixes in verus-strip: backtick-escaped `verus!` in doc comments no longer truncates output, `pub exec const` strips the `exec` keyword, and content after the `verus!{}` block is preserved. Trace: skip --- .github/workflows/ci.yml | 11 ++++------- verus/MODULE.bazel | 6 +++++- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 33d568f..f0e4cd2 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -405,17 +405,14 @@ jobs: - run: cargo kani -p rivet-core # ── Verus SMT verification ────────────────────────────────────────── - # Not yet a hard gate. Upstream chain blocks us: rules_verus (pinned at - # pulseengine/rules_verus@5bc96f39, our fix for the :all alias bug) - # depends on rules_rust 0.56.0, which uses the removed `CcInfo` symbol - # and fails to load in current Bazel. Needs either a rules_rust bump - # in rules_verus or a wrapper around the removed symbol before this - # can be flipped back to a hard gate. + # Hard gate as of pulseengine/rules_verus@fc7b636: that commit bumped + # the rules_rust minimum to 0.58.0, the floor where CcInfo is loaded + # from @rules_cc//cc/common:cc_info.bzl rather than the removed Bazel + # built-in. With that fix, rules_verus loads cleanly on current Bazel. verus: name: Verus Proofs needs: [test] runs-on: ubuntu-latest - continue-on-error: true timeout-minutes: 20 steps: - uses: actions/checkout@v6 diff --git a/verus/MODULE.bazel b/verus/MODULE.bazel index fad8cf0..48cbdd5 100644 --- a/verus/MODULE.bazel +++ b/verus/MODULE.bazel @@ -19,7 +19,11 @@ bazel_dep(name = "rules_verus", version = "0.1.0") git_override( module_name = "rules_verus", remote = "https://github.com/pulseengine/rules_verus.git", - commit = "5bc96f39cb4ccf5028a8cca94950f4bee6405423", + # fc7b636: rules_rust minimum bumped to 0.58.0 — earlier minimum + # depended on the removed Bazel built-in `CcInfo` and broke load. + # 5e2b7c6: three correctness fixes in verus-strip (backtick-in-doc, + # `pub exec const` qualifier, content-after-`verus!{}` truncation). + commit = "fc7b63692b1d2d91511f04507b814187932cd733", ) # ── Verus toolchain registration ─────────────────────────────────────── From ecab4c1fd350f3902b6c31a7302b12b76bf2adda Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 21 Apr 2026 06:53:52 +0200 Subject: [PATCH 12/15] fix(bazel): expose verus_specs.rs via rivet-core/src/BUILD.bazel MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit //verus:rivet_specs_verify references `//rivet-core/src:verus_specs.rs` as a Bazel label, but rivet-core/src was not a Bazel package, so `bazel test` failed analysis with: ERROR: no such package 'rivet-core/src': BUILD file not found Adds a minimal BUILD.bazel that marks the directory as a package and exports the verus specs file. The crate itself is still built via cargo — this file exists only so the Bazel-side Verus targets can address the spec source. Trace: skip --- rivet-core/src/BUILD.bazel | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 rivet-core/src/BUILD.bazel diff --git a/rivet-core/src/BUILD.bazel b/rivet-core/src/BUILD.bazel new file mode 100644 index 0000000..70a7de2 --- /dev/null +++ b/rivet-core/src/BUILD.bazel @@ -0,0 +1,9 @@ +# Bazel package marker for rivet-core/src. +# +# This file exists solely so that //verus:rivet_specs_verify can +# reference `//rivet-core/src:verus_specs.rs` as a Bazel label. +# The crate itself is built via cargo, not Bazel. + +package(default_visibility = ["//visibility:public"]) + +exports_files(["verus_specs.rs"]) From 080527a108b8c2c17a8de66bd9cb077d5db34dbc Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 21 Apr 2026 07:44:31 +0200 Subject: [PATCH 13/15] refactor(bazel): unify repo into a single bzlmod workspace MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit verus/ and proofs/rocq/ each had their own MODULE.bazel, which made every Bazel label relative to those subdirectories. That broke //verus:rivet_specs_verify's attempt to reference //rivet-core/src:verus_specs.rs — the label resolved against the verus/ workspace root and demanded a `verus/rivet-core/src` directory that doesn't exist, yielding: ERROR: no such package 'rivet-core/src': BUILD file not found Root cause was architectural. Consolidate into one workspace at the repo root so cross-directory Bazel references work: - New top-level `MODULE.bazel` merges the two previous module declarations (rules_verus + rules_rocq_rust + rules_nixpkgs_core, same commit pins and same toolchain registrations). - New top-level `BUILD.bazel` as a minimal package marker. - Deleted `verus/MODULE.bazel` and `proofs/rocq/MODULE.bazel`. - CI: run `bazel test //verus:rivet_specs_verify` and `bazel test //proofs/rocq:rivet_metamodel_test` from the repo root, not `working-directory: verus|proofs/rocq`. The Rust crates are still built via cargo. Bazel in this repo is scoped to the formal-verification targets only. With the unified workspace, //verus:rivet_specs_verify can now reach //rivet-core/src:verus_specs.rs which is the precondition for the Verus hard gate to do real work. Trace: skip --- .github/workflows/ci.yml | 6 +-- BUILD.bazel | 8 ++++ MODULE.bazel | 80 ++++++++++++++++++++++++++++++++++++++++ proofs/rocq/MODULE.bazel | 52 -------------------------- verus/MODULE.bazel | 35 ------------------ 5 files changed, 90 insertions(+), 91 deletions(-) create mode 100644 BUILD.bazel create mode 100644 MODULE.bazel delete mode 100644 proofs/rocq/MODULE.bazel delete mode 100644 verus/MODULE.bazel diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f0e4cd2..1a55325 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -423,8 +423,7 @@ jobs: disk-cache: ${{ github.workflow }} repository-cache: true - name: Verify Verus specs - working-directory: verus - run: bazel test //:rivet_specs_verify + run: bazel test //verus:rivet_specs_verify # ── Rocq metamodel proofs ───────────────────────────────────────── # Not yet a hard gate: the proofs were written against an older Rocq and @@ -452,8 +451,7 @@ jobs: with: nix_path: nixpkgs=channel:nixos-unstable - name: Verify Rocq proofs - working-directory: proofs/rocq - run: bazel test //:rivet_metamodel_test + run: bazel test //proofs/rocq:rivet_metamodel_test # ── MSRV check ────────────────────────────────────────────────────── msrv: diff --git a/BUILD.bazel b/BUILD.bazel new file mode 100644 index 0000000..b1f4eb1 --- /dev/null +++ b/BUILD.bazel @@ -0,0 +1,8 @@ +# Repo-root BUILD file. Exists to mark the repo root as a Bazel +# package so sibling subpackages (verus/, proofs/rocq/, rivet-core/src/) +# resolve cleanly under a unified workspace. +# +# No targets live here — Bazel in this repo is scoped to +# formal-verification surfaces under verus/ and proofs/rocq/. + +package(default_visibility = ["//visibility:public"]) diff --git a/MODULE.bazel b/MODULE.bazel new file mode 100644 index 0000000..c6b7b60 --- /dev/null +++ b/MODULE.bazel @@ -0,0 +1,80 @@ +# Rivet — root Bazel module (bzlmod). +# +# This file defines the repo as a single Bazel workspace so that +# Verus SMT verification and Rocq metamodel proofs can reference +# Rust source files that live outside their own subdirectories +# (e.g. //rivet-core/src:verus_specs.rs). +# +# Prior to consolidation each subproject (verus/, proofs/rocq/) had +# its own MODULE.bazel, which made every Bazel label relative to that +# subdirectory and broke cross-package references. Unifying the +# workspace at the repo root lets //verus:rivet_specs_verify depend +# on //rivet-core/src:verus_specs.rs directly. +# +# The Rust crates themselves are still built via cargo. Bazel is only +# used for the formal-verification targets under verus/ and +# proofs/rocq/. +# +# Usage: +# bazel test //verus:rivet_specs_verify # Verus SMT verification +# bazel test //proofs/rocq:rivet_metamodel_test # Rocq proof checking + +module( + name = "rivet", + version = "0.4.0", +) + +# ── rules_verus (Verus SMT verification) ──────────────────────────────── + +bazel_dep(name = "rules_verus", version = "0.1.0") + +git_override( + module_name = "rules_verus", + remote = "https://github.com/pulseengine/rules_verus.git", + # fc7b636: rules_rust minimum bumped to 0.58.0 — earlier minimum + # depended on the removed Bazel built-in `CcInfo` and broke load. + # 5e2b7c6: three correctness fixes in verus-strip (backtick-in-doc, + # `pub exec const` qualifier, content-after-`verus!{}` truncation). + commit = "fc7b63692b1d2d91511f04507b814187932cd733", +) + +verus = use_extension("@rules_verus//verus:extensions.bzl", "verus") +verus.toolchain(version = "0.2026.02.15") +use_repo(verus, "verus_toolchains") + +register_toolchains("@verus_toolchains//:all") + +# ── rules_rocq_rust (Rocq metamodel proofs) ──────────────────────────── + +bazel_dep(name = "rules_rocq_rust", version = "0.1.0") + +git_override( + module_name = "rules_rocq_rust", + remote = "https://github.com/pulseengine/rules_rocq_rust.git", + commit = "6a8da0bd30b5f80f811acefbf6ac5740a08d4a8c", +) + +# rules_rocq_rust needs a Nix toolchain for hermetic Rocq binaries. +bazel_dep(name = "rules_nixpkgs_core", version = "0.13.0") + +nix_repo = use_extension( + "@rules_nixpkgs_core//extensions:repository.bzl", + "nix_repo", +) +nix_repo.github( + name = "nixpkgs", + org = "NixOS", + repo = "nixpkgs", + # nixos-unstable with Rocq 9.0.1 (pinned 2026-03-06) + commit = "aca4d95fce4914b3892661bcb80b8087293536c6", + sha256 = "", +) +use_repo(nix_repo, "nixpkgs") + +rocq = use_extension("@rules_rocq_rust//rocq:extensions.bzl", "rocq") +rocq.toolchain( + version = "9.0", + strategy = "nix", +) +use_repo(rocq, "rocq_toolchains", "rocq_stdlib") +register_toolchains("@rocq_toolchains//:all") diff --git a/proofs/rocq/MODULE.bazel b/proofs/rocq/MODULE.bazel deleted file mode 100644 index 401ac9a..0000000 --- a/proofs/rocq/MODULE.bazel +++ /dev/null @@ -1,52 +0,0 @@ -# Rivet Formal Verification — Rocq/Coq Proofs -# -# This module integrates rules_rocq_rust for compiling Rocq proof files -# that formally verify properties of Rivet's validation engine. -# -# Prerequisites: -# - Nix package manager (provides hermetic Rocq 9.0 toolchain) -# - Bazel 8+ with bzlmod enabled -# -# Usage: -# bazel build //proofs/rocq:rivet_metamodel -# bazel test //proofs/rocq:rivet_metamodel_test - -module( - name = "rivet_proofs", - version = "0.1.0", -) - -# rules_rocq_rust — Bazel rules for Rocq theorem proving -bazel_dep(name = "rules_rocq_rust", version = "0.1.0") - -git_override( - module_name = "rules_rocq_rust", - remote = "https://github.com/pulseengine/rules_rocq_rust.git", - commit = "6a8da0bd30b5f80f811acefbf6ac5740a08d4a8c", -) - -# Nix integration (required by rules_rocq_rust for hermetic toolchains) -bazel_dep(name = "rules_nixpkgs_core", version = "0.13.0") - -nix_repo = use_extension( - "@rules_nixpkgs_core//extensions:repository.bzl", - "nix_repo", -) -nix_repo.github( - name = "nixpkgs", - org = "NixOS", - repo = "nixpkgs", - # nixos-unstable with Rocq 9.0.1 (pinned 2026-03-06) - commit = "aca4d95fce4914b3892661bcb80b8087293536c6", - sha256 = "", -) -use_repo(nix_repo, "nixpkgs") - -# Rocq toolchain — hermetic Rocq 9.0 via nixpkgs -rocq = use_extension("@rules_rocq_rust//rocq:extensions.bzl", "rocq") -rocq.toolchain( - version = "9.0", - strategy = "nix", -) -use_repo(rocq, "rocq_toolchains", "rocq_stdlib") -register_toolchains("@rocq_toolchains//:all") diff --git a/verus/MODULE.bazel b/verus/MODULE.bazel deleted file mode 100644 index 48cbdd5..0000000 --- a/verus/MODULE.bazel +++ /dev/null @@ -1,35 +0,0 @@ -# Verus formal verification integration for Rivet. -# -# This file shows the MODULE.bazel fragment needed to enable Verus -# verification. Merge these declarations into the project root -# MODULE.bazel when Bazel is adopted as a build system. -# -# The rules_verus module downloads pre-built Verus binaries (rust_verify -# + Z3) from GitHub releases and provides hermetic toolchain support. - -module( - name = "rivet", - version = "0.1.0", -) - -# ── rules_verus dependency ────────────────────────────────────────────── - -bazel_dep(name = "rules_verus", version = "0.1.0") - -git_override( - module_name = "rules_verus", - remote = "https://github.com/pulseengine/rules_verus.git", - # fc7b636: rules_rust minimum bumped to 0.58.0 — earlier minimum - # depended on the removed Bazel built-in `CcInfo` and broke load. - # 5e2b7c6: three correctness fixes in verus-strip (backtick-in-doc, - # `pub exec const` qualifier, content-after-`verus!{}` truncation). - commit = "fc7b63692b1d2d91511f04507b814187932cd733", -) - -# ── Verus toolchain registration ─────────────────────────────────────── - -verus = use_extension("@rules_verus//verus:extensions.bzl", "verus") -verus.toolchain(version = "0.2026.02.15") -use_repo(verus, "verus_toolchains") - -register_toolchains("@verus_toolchains//:all") From b3eaf623c8e8c6431073fd7aa556049c9290ea80 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 21 Apr 2026 08:02:50 +0200 Subject: [PATCH 14/15] fix(ci): install Nix on Verus runner too MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Workspace consolidation (6771e6e) means root MODULE.bazel registers both Verus and Rocq toolchains. Bazel resolves every registered toolchain at analysis time regardless of which target is being built, so the Verus-only job now hits the Rocq toolchain extension, which requires rules_nixpkgs_core, which requires nix-build on PATH: ERROR: An error occurred during the fetch of repository 'rules_rocq_rust++rocq+rocq_toolchains': Platform is not supported: nix-build not found in PATH. Install Nix on the Verus runner too. Small cost (~30s) on a job that already takes 20 min, and it's the minimal fix — alternatives (split MODULE.bazel, or rules_nixpkgs_core fail_not_supported) either undo the consolidation or require upstream changes. Trace: skip --- .github/workflows/ci.yml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1a55325..24dd488 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -422,6 +422,15 @@ jobs: bazelisk-cache: true disk-cache: ${{ github.workflow }} repository-cache: true + # Nix is required because the unified root MODULE.bazel registers + # the Rocq toolchain, which depends on rules_nixpkgs_core. Bazel + # resolves all registered toolchains at analysis time regardless + # of which target is being built, so Nix must be on PATH even for + # Verus-only invocations. + - name: Install Nix + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixos-unstable - name: Verify Verus specs run: bazel test //verus:rivet_specs_verify From 1efc2e6050fab47fb714bb08039818201d6ae909 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 21 Apr 2026 18:31:02 +0200 Subject: [PATCH 15/15] =?UTF-8?q?ci(verus):=20soft-gate=20again=20?= =?UTF-8?q?=E2=80=94=20toolchain=20works,=20specs=20fail?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Workspace hoist + Nix install fixed the plumbing: Verus now analyses //verus:rivet_specs_verify against //rivet-core/src:verus_specs.rs and invokes rust_verify. But the specs themselves fail verification in 0.1s — a real SMT proof obligation can't be discharged. That's spec-level work (audit which `requires`/`ensures` clauses are wrong) and doesn't belong in this CI-hard-gate PR. Soft-gate until the spec fixes land. Trace: skip --- .github/workflows/ci.yml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 24dd488..5e9cd25 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -405,14 +405,18 @@ jobs: - run: cargo kani -p rivet-core # ── Verus SMT verification ────────────────────────────────────────── - # Hard gate as of pulseengine/rules_verus@fc7b636: that commit bumped - # the rules_rust minimum to 0.58.0, the floor where CcInfo is loaded - # from @rules_cc//cc/common:cc_info.bzl rather than the removed Bazel - # built-in. With that fix, rules_verus loads cleanly on current Bazel. + # Toolchain + workspace are now correct (rules_verus@fc7b636 past the + # CcInfo bump; root MODULE.bazel lets //verus see //rivet-core/src). + # But the specs themselves fail verification ("FAIL in 0.1s" — Verus + # rejects at least one proof obligation). That's a genuine SMT result, + # not a plumbing issue, and it needs spec-level work separate from + # the CI hard-gate PR. Soft-gate with a clear TODO until the specs + # are green under the unified workspace. verus: name: Verus Proofs needs: [test] runs-on: ubuntu-latest + continue-on-error: true timeout-minutes: 20 steps: - uses: actions/checkout@v6