Skip to content

AGENTS.md

Latest commit

 

History

History
758 lines (583 loc) · 26.5 KB

AGENTS.md

File metadata and controls

758 lines (583 loc) · 26.5 KB

AGENTS.md — Rivet Project Instructions

This file was generated by rivet init --agents. Re-run the command any time artifacts change to keep this file current.

Project Overview

This project uses Rivet for SDLC artifact traceability.

  • Config: rivet.yaml
  • Schemas: common, stpa, aspice, dev
  • Artifacts: 213 across 11 types
  • Validation: rivet validate (current status: pass)

Available Commands

Command Purpose Example
rivet validate Check link integrity, coverage, required fields rivet validate --format json
rivet list List artifacts with filters rivet list --type requirement --format json
rivet stats Show artifact counts by type rivet stats --format json
rivet add Create a new artifact rivet add -t requirement --title "..." --link "satisfies:SC-1"
rivet link Add a link between artifacts rivet link SOURCE -t satisfies --target TARGET
rivet serve Start the dashboard rivet serve --port 3000
rivet export Generate HTML reports rivet export --format html --output ./dist
rivet impact Show change impact rivet impact --since HEAD~1
rivet coverage Show traceability coverage rivet coverage --format json
rivet diff Compare artifact versions rivet diff --base path/old --head path/new

Artifact Types

Type Count Description
control-action 26 An action issued by a controller to a controlled process or another controller.
controlled-process 5 A process being controlled — the physical or data transformation acted upon by controllers.
controller 7 A system component (human or automated) responsible for issuing control actions. Each controller has a process model — its internal beliefs about the state of the controlled process.
controller-constraint 45 A constraint on a controller's behavior derived by inverting a UCA. Specifies what the controller must or must not do.
hazard 10 A system state or set of conditions that, together with worst-case environmental conditions, will lead to a loss.
loss 5 An undesired or unplanned event involving something of value to stakeholders. Losses define what the analysis aims to prevent.
loss-scenario 21 A causal pathway describing how a UCA could occur or how the control action could be improperly executed, leading to a hazard.
requirement 27 A functional or non-functional requirement
sub-hazard 10 A refinement of a hazard into a more specific unsafe condition.
system-constraint 12 A condition or behavior that must be satisfied to prevent a hazard. Each constraint is the inversion of a hazard.
uca 45 An Unsafe Control Action — a control action that, in a particular context and worst-case environment, leads to a hazard. Four types (provably complete): 1. Not providing the control action leads to a hazard 2. Providing the control action leads to a hazard 3. Providing too early, too late, or in the wrong order 4. Control action stopped too soon or applied too long
design-decision 0 An architectural or design decision with rationale
feature 0 A user-visible capability or feature
stakeholder-req 0 Stakeholder requirement (SYS.1)
sw-arch-component 0 Software architectural element (SWE.2)
sw-detail-design 0 Software detailed design or unit specification (SWE.3)
sw-integration-verification 0 Software component and integration verification measure (SWE.5 — Software Component Verification and Integration Verification)
sw-req 0 Software requirement (SWE.1)
sw-verification 0 Software verification measure against SW requirements (SWE.6 — Software Verification)
sys-integration-verification 0 System integration and integration verification measure (SYS.4 — System Integration and Integration Verification)
sys-verification 0 System verification measure against system requirements (SYS.5 — System Verification)
system-arch-component 0 System architectural element (SYS.3)
system-req 0 System requirement derived from stakeholder needs (SYS.2)
unit-verification 0 Unit verification measure (SWE.4 — Software Unit Verification)
verification-execution 0 A verification execution run against a specific version
verification-verdict 0 Pass/fail verdict for a single verification measure in an execution run

Working with Artifacts

File Structure

  • Artifacts are stored as YAML files in: safety/stpa, safety/requirements
  • Schema definitions: schemas/ directory
  • Documents: docs

Creating Artifacts

rivet add -t requirement --title "New requirement" --status draft --link "satisfies:SC-1"

Validating Changes

Always run rivet validate after modifying artifact YAML files. Use rivet validate --format json for machine-readable output.

Link Types

Link Type Description Inverse
acts-on Control action acts on a process or controller acted-on-by
allocated-to Source is allocated to the target (e.g. requirement to architecture component) allocated-from
caused-by-uca Loss scenario is caused by an unsafe control action causes-scenario
constrained-by Source is constrained by the target constrains
constrains-controller Constraint applies to a specific controller controller-constrained-by
depends-on Source depends on target being completed first depended-on-by
derives-from Source is derived from the target derived-into
implements Source implements the target implemented-by
inverts-uca Controller constraint inverts (is derived from) an UCA inverted-by
issued-by Control action or UCA is issued by a controller issues
leads-to-hazard UCA or loss scenario leads to a hazard hazard-caused-by
leads-to-loss Hazard leads to a specific loss loss-caused-by
mitigates Source mitigates or prevents the target mitigated-by
part-of-execution Verification verdict belongs to a verification execution run contains-verdict
prevents Constraint prevents a hazard prevented-by
refines Source is a refinement or decomposition of the target refined-by
result-of Verification verdict is the result of executing a verification measure has-result
satisfies Source satisfies or fulfils the target satisfied-by
traces-to General traceability link between any two artifacts traced-from
verifies Source verifies or validates the target verified-by

Conventions

  • Artifact IDs follow the pattern: PREFIX-NNN (e.g., REQ-001, FEAT-042)
  • Use rivet add to create artifacts (auto-generates next ID)
  • Always include traceability links when creating artifacts
  • Run rivet validate before committing

Commit Traceability

This project enforces commit-to-artifact traceability.

Required git trailers:

  • trace -> maps to link type Trace

To skip traceability for a commit, add: Trace: skip

Project Guidance (Manually Maintained)

The content below is NOT auto-generated by rivet. Preserve it during rivet init --agents regeneration. If the tool overwrites this section, restore it from git history.

Project Overview

Meld is a static component fusion tool for WebAssembly. It takes composed P2/P3 components and fuses them into a single core wasm module, eliminating the need for runtime linking.

Part of the pulseengine toolchain:

  • loom — WebAssembly optimizer (formally verified)
  • meld — Static component fuser (this tool)

Build Commands

Cargo (Development)

# Build all crates
cargo build

# Build release
cargo build --release

# Run tests
cargo test

# Run specific test
cargo test --package meld-core test_name

# Run CLI
cargo run --bin meld -- fuse input.wasm -o output.wasm

# Build for WASM target
cargo build --target wasm32-wasip2 --profile release-wasm

Bazel (Production/CI)

# Build all targets
bazel build //...

# Build specific target
bazel build //meld-cli:meld

# Run tests
bazel test //...

# Build with release config
bazel build --config=release //meld-cli:meld

Architecture

meld/
├── meld-core/          # Core fusion library
│   ├── src/
│   │   ├── lib.rs          # Public API
│   │   ├── parser.rs       # Component parsing (wasmparser)
│   │   ├── resolver.rs     # Dependency resolution
│   │   ├── merger.rs       # Module merging
│   │   ├── adapter/        # Adapter generation
│   │   │   ├── mod.rs      # Trait interface
│   │   │   └── fact.rs     # FACT-style implementation
│   │   ├── error.rs        # Error types (thiserror)
│   │   └── attestation.rs  # wsc-attestation integration
│   └── Cargo.toml
├── meld-cli/           # CLI binary
│   ├── src/main.rs
│   └── Cargo.toml
└── rules/              # Bazel rules (for rules_wasm_component)
    ├── meld.bzl        # meld_fuse() rule
    └── providers.bzl

Key Concepts

Component Fusion Pipeline

P2/P3 Components → Parser → Resolver → Merger → Adapter Gen → Single Module
  1. Parser: Extracts core modules and type info from components
  2. Resolver: Builds import/export graph, topological sort
  3. Merger: Combines function/memory/table/global spaces
  4. Adapter Gen: Creates Canonical ABI trampolines for cross-component calls

Memory Strategies

  • Multi-memory (default): Each component keeps its own linear memory. Cross-component calls that pass pointers use adapters that allocate in the callee's memory via cabi_realloc, copy data with memory.copy, call the target, and copy results back. Requires WebAssembly multi-memory (Core Spec 3.0, supported by wasmtime/Chrome/Firefox).
  • Shared memory (legacy): All components share a single linear memory. Simpler but broken when any component uses memory.grow, because one component's growth corrupts every other component's address space. Use --memory shared to opt in.

Development Guidelines

  1. Error Handling: Use anyhow for CLI, thiserror for library errors
  2. Testing: Property-based tests with proptest for core logic
  3. Documentation: Doc comments on all public APIs
  4. Logging: Use log crate, configure via RUST_LOG env var

Key Files

  • meld-core/src/parser.rs — Component binary parsing
  • meld-core/src/resolver.rs — Import/export resolution
  • meld-core/src/merger.rs — Module merging logic
  • meld-core/src/rewriter.rs — Instruction rewriting (index remapping)
  • meld-core/src/adapter/mod.rs — Adapter trait definition
  • meld-core/src/adapter/fact.rs — FACT-style adapter generation
  • meld-core/src/segments.rs — Data/element segment handling
  • meld-cli/src/main.rs — CLI entry point

Integration Points

wsc-attestation

Track transformation provenance through fusion. Add attestation to output module's custom section.

LOOM

Output is optimizable by LOOM. Use LOOM after meld for whole-program optimization:

meld fuse a.wasm b.wasm -o fused.wasm
loom optimize fused.wasm -o optimized.wasm

rules_wasm_component

Bazel rule integration via meld_fuse():

load("@meld//rules:meld.bzl", "meld_fuse")

meld_fuse(
    name = "fused",
    components = [":component_a", ":component_b"],
)

Testing

# All tests (unit + integration)
cargo test

# Specific integration test
cargo test --test cross_component_call
cargo test --test multi_memory
cargo test --test rebasing_end_to_end

# Specific unit test
cargo test --package meld-core test_name

Verification

# Validate output
wasm-tools validate fused.wasm

# Print structure
wasm-tools print fused.wasm | head -50

# Component info
wasm-tools component wit input.wasm

Formal Verification

Kani scope limitation

Kani/CBMC runs out of memory on code that exercises std::io (BufReader, BorrowedBuf), rich Vec manipulation, or deep generic trait dispatch. When a Kani harness OOMs, that is NOT evidence the property holds — it is evidence the tool cannot reach the property. Fall back to the nearest lower-level Kani proof on the primitives the code composes, and document the limitation in the finding report.

Rocq Formal Verification

This project uses Rocq 9.0 (formerly Coq) for formal verification of the fusion pipeline. Proofs are built via Bazel using rules_rocq_rust, which provides both the Rocq toolchain and rocq-of-rust for Rust-to-Rocq translation.

Rocq 9.0 Migration from Coq 8.x

Rocq 9.0 introduced significant naming changes. The codebase uses the new conventions:

Import Changes
(* OLD Coq 8.x style - DO NOT USE *)
From Coq Require Import List ZArith.

(* NEW Rocq 9.0 style - USE THIS *)
From Stdlib Require Import List ZArith Lia Arith.
Deprecated Lemma Names

Many lemmas were renamed to follow a consistent property_type pattern:

Old Name (8.x) New Name (9.0)
app_length length_app
map_length length_map
app_nil_r app_nil_r (same)
app_assoc app_assoc (same)
fold_left_app fold_left_app
nth_error_None nth_error_None
nth_error_Some nth_error_Some
in_map_iff in_map_iff
in_seq in_seq

Build Commands

# Build all proofs
bazel build //proofs:all_proofs

# Run a specific proof test (note: tagged 'manual')
bazel test //proofs:parser_proofs_test

# Build Rust-translated proofs
bazel build //proofs/rust_verified:merger_core_proofs

Note: Proof builds require Nix for the hermetic Rocq toolchain.

Powerful Tactics and Automation

Arithmetic Solvers

  • lia (Linear Integer Arithmetic): Solves goals involving linear arithmetic over integers/naturals. Use for bounds, inequalities, and simple arithmetic.

    Proof. intros. lia. Qed.

  • nia (Nonlinear Integer Arithmetic): Extends lia with limited nonlinear support. More powerful but slower.

  • omega: Deprecated in Rocq 9.0. Use lia instead.

Automated Proof Search

  • auto: Basic proof search using hint databases. Fast but limited.

    auto with arith.  (* Use arithmetic hints *)

  • eauto: Like auto but handles existentials. Use eauto with * for aggressive search.

  • intuition: Propositional logic solver. Combines auto with logical decomposition.

    intuition lia.  (* Decompose then solve arithmetic *)

  • tauto: Pure propositional tautology checker. Fast and complete for propositional goals.

  • firstorder: First-order logic prover. Powerful but can be slow.

    firstorder auto.  (* First-order with auto fallback *)
Extensions in This Codebase

From MODULE.bazel, the following Rocq extensions are available:

  • rocq_stdlib: Standard library (Lists, Arith, ZArith, etc.)
  • rocq_coqutil: Utility library with tactics and definitions
  • rocq_hammer: Automated theorem prover integration (for hard goals)
  • rocq_smpl: Simplification tactics

Proof Engineering Patterns

Structuring Complex Proofs

  1. Use sections for local assumptions:

    Section MergeCorrectness.
  Variable input : merge_input.
  Hypothesis Hwf : well_formed input.

  Lemma helper1 : ... .
  Lemma helper2 : ... .
  Theorem main : ... .
End MergeCorrectness.

  2. Break into helper lemmas: Each file in proofs/ contains multiple lemmas building toward main theorems.

Assertion Tactics: assert vs enough vs cut

  • assert (H: P): Prove P first, then use H in the main goal. Most common pattern.

    assert (Hbound: x < length l).
{ (* prove bound *) lia. }
(* now use Hbound *)

  • enough (H: P): Assume H, prove main goal, then prove H. Use when H makes the main goal obvious.

    enough (Heq: x = y).
{ subst. reflexivity. }
(* now prove x = y *)

  • cut P: Like assert but leaves goals in reverse order. Rarely needed; prefer assert.

Generalizing Induction Hypotheses with revert

When induction needs a stronger hypothesis, use revert to generalize:

(* BAD: IH is too weak *)
Lemma fold_monotonic : forall l base,
    base <= fold_left f l base.
Proof.
  induction l.  (* IH only works for specific base *)
  ...

(* GOOD: revert makes IH general *)
Lemma fold_monotonic : forall l base,
    base <= fold_left f l base.
Proof.
  induction l; intro base.  (* IH works for all base values *)
  - simpl. lia.
  - simpl. apply IH.  (* Can apply to any base *)
Qed.

See proofs/transformations/merge/merge_layout.v for examples of this pattern in fold_left_add_nonneg_ge and related lemmas.

Using set and remember for Abstraction

  • set (x := expr): Name a subexpression without generating equality. Good for readability.

    set (offset := compute_offset input space mod_idx).

  • remember expr as x eqn:Heq: Name subexpression AND generate equality hypothesis. Use when you need to unfold later.

    remember (j - i) as diff eqn:Hdiff.

rocq-of-rust Translation

Rust code is translated to Rocq via coq_of_rust_library rules. See proofs/rust_verified/BUILD.bazel:

coq_of_rust_library(
    name = "merger_core_translated",
    rust_sources = ["merger_core.rs"],
    edition = "2021",
)

rocq_library(
    name = "merger_core",
    srcs = [":merger_core_translated"],
    deps = [":rocq_of_rust_lib"],
    include_path = "meld",
    extra_flags = ["-impredicative-set"],
)

The translated code uses the rocq-of-rust runtime library. Proofs then bridge between the translated Rust and pure-model specifications.

Common Pitfalls and Solutions

1. lia Failing on fold_left

lia cannot reason about fold_left directly. Abstract the term first:

(* BAD: lia fails *)
Lemma bad : forall l, 0 <= fold_left (fun a x => a + x) l 0.
Proof. intros. lia. (* FAILS *) Abort.

(* GOOD: use a helper lemma *)
Lemma fold_left_nonneg : forall l base,
    base <= fold_left (fun a x => a + x) l base.
Proof.
  induction l; intro base; simpl.
  - lia.
  - specialize (IHl (base + a)). lia.
Qed.

Lemma good : forall l, 0 <= fold_left (fun a x => a + x) l 0.
Proof. intros. apply fold_left_nonneg. Qed.

See proofs/transformations/merge/merge_layout.v:fold_left_add_nonneg_ge.

2. Pattern Matching Issues (Boolean Associativity)

Boolean && is left-associative. When matching on complex conditions:

(* The expression ((A && B) && C) && D *)
apply Bool.andb_true_iff in H.
destruct H as [H123 H4].      (* Split off D *)
apply Bool.andb_true_iff in H123.
destruct H123 as [H12 H3].    (* Split off C *)
apply Bool.andb_true_iff in H12.
destruct H12 as [H1 H2].      (* Split A and B *)
3. Induction Needing Generalization

If induction gives a weak hypothesis, generalize more variables:

(* Weak: IH only for fixed values *)
induction l.

(* Strong: generalize auxiliary variables *)
generalize dependent aux_var.
induction l; intros aux_var.

(* Or use revert before induction *)
revert aux_var.
induction l.
4. nth_error vs In

Converting between In and nth_error:

(* In -> nth_error *)
apply In_nth_error in Hin.
destruct Hin as [i Hi].

(* nth_error -> In *)
apply nth_error_In in Hnth.

(* Checking bounds *)
apply nth_error_Some. rewrite H. discriminate.
apply nth_error_None in H. (* H : i >= length l *)
5. Proof Completion

All proofs across the entire proofs/ directory are fully closed (Qed). There are zero Admitted theorems, zero admit tactics, and zero Axiom declarations. If you add new proofs, aim to close them fully.

Proof Directory Layout

Proofs path Source path Focus
proofs/parser/ meld-core/src/parser.rs Parsing and decoding
proofs/resolver/ meld-core/src/resolver.rs Import/export resolution
proofs/merger/ meld-core/src/merger.rs Index-space merging
proofs/adapter/ meld-core/src/adapter/ Canonical ABI adapters
proofs/rewriter/ meld-core/src/rewriter.rs Rewrite passes
proofs/segments/ meld-core/src/segments.rs Segment layout
proofs/attestation/ meld-core/src/attestation.rs Attestation integrity
proofs/rust_verified/ (special) Rust-to-Rocq translated proofs
proofs/spec/ (specifications) Core spec definitions
proofs/transformations/ (specs for transforms) Transform correctness specs

Specification Baselines

From proofs/DECISIONS.md:

  • Core spec: WebAssembly Core Specification, Release 3.0
  • Component Model: Commit deb0b0a
  • WASI: v0.2.3 WIT definitions

Tips for Writing New Proofs

  1. Start with the spec: Define what correctness means in proofs/spec/ or proofs/transformations/ before proving.

  2. Use pure-model definitions: Mirror Rust implementation in a simpler form (see merger_core_proofs.v for examples).

  3. Build incrementally: Small lemmas compose into theorems.

  4. Leverage automation: Try auto, eauto, lia early. Use intuition for propositional goals.

  5. Document admitted proofs: Explain why and what's needed to complete.

  6. Human readability: All lemmas, theorems, and proof structures must be human readable and understandable. Proofs should be written so that a developer can follow the logical reasoning without needing to step through tactics interactively. Prefer explicit structure over tactic magic:

    • Use meaningful names for hypotheses (Hbound, Hvalid, not H1, H2)
    • Add comments for non-obvious proof steps
    • Break complex proofs into named helper lemmas
    • Avoid deeply nested bullet structures (max 3-4 levels)
    • When using admit, document what remains to be proven

Mythos Bug-Hunt Pipeline

Mythos-style agentic bug hunting is wired into this repo. Prompts, rubric, and the portable HOWTO live in scripts/mythos/:

  • rank.md — file ranking (1–5) by bug likelihood, meld-specific rubric
  • discover.md — per-file discovery prompt with oracle requirement
  • validate.md — fresh-session confirmation (rejects hallucinations)
  • emit.md — converts confirmed findings to draft LS-N entries in safety/stpa/loss-scenarios.yaml, grouped under existing UCAs (UCA IDs use controller-prefixed form: UCA-P-N for parser, UCA-M-N for merger, etc.)
  • HOWTO.md — portable pipeline documentation (same across all PulseEngine repos)

Oracle requirement (invariant)

A failing PoC test is ALWAYS required for a confirmed finding — this is the deterministic oracle. A failing Kani harness is required unless the subject code exercises a symbolic surface CBMC cannot handle (see Kani scope limitation above); in that case, cite the nearest primitive-layer Kani proof and document the limitation. Hallucinations are more expensive than silence. If neither oracle can be produced, the finding does not count — do not report it.

Pre-Release Mythos delta pass (MANDATORY)

Before creating a release tag, run a Mythos delta pass scoped by release type:

Release Scope
Patch (x.y.Z) Tier-5 files changed since last tag
Minor (x.Y.z) Tier-5 + tier-4 files changed since last tag
Major / LTS Full tier-5 sweep regardless of diff

Procedure:

# Identify changed tier-5 files (meld-core parser / fusion / types / writer)
git diff --name-only v<last>..HEAD -- \
  meld-core/src/parser.rs \
  meld-core/src/merger.rs \
  'meld-core/src/fuse/**' \
  'meld-core/src/fusion/**' \
  'meld-core/src/types/**' \
  'meld-core/src/type_check/**' \
  'meld-core/src/writer.rs' \
  'meld-core/src/emit/**'

For each file, in a fresh Claude Code session:

Read scripts/mythos/discover.md and apply it to <file>. Do not relax the
oracle requirement.

For each finding, fresh session: Read scripts/mythos/validate.md and apply it to the report above.

Block the release if any confirmed finding lacks an approved LS-N in safety/stpa/loss-scenarios.yaml with a shipped fix or an explicit risk-acceptance note.

Release Process

Pre-Release Checklist (MANDATORY)

  1. All changes via PR: Never push directly to main for any code changes
  2. CI must pass completely: Wait for ALL CI jobs to succeed before merging
  3. Watch the full CI run: Do not assume CI passes — verify it
  4. Mythos delta pass: Run per ### Pre-Release Mythos delta pass above. Zero confirmed findings, OR every confirmed finding maps to an approved LS-N in safety/stpa/loss-scenarios.yaml with a shipped fix

Release Steps

  1. Create version bump PR:

    git checkout -b release/vX.Y.Z
# Update version in Cargo.toml
# Update internal dependency versions
git commit -m "chore: bump version to X.Y.Z"
git push -u origin release/vX.Y.Z
gh pr create

  2. Wait for CI to complete: Watch ALL checks pass

    gh pr checks <PR#> --watch

  3. Merge PR: Only after all checks pass

    gh pr merge <PR#> --squash

  4. Create release: Only after merge and main CI passes

    # Pull latest main
git checkout main && git pull

# Verify main CI passed
gh run list --branch main --limit 1

# Create and push tag
git tag -a vX.Y.Z -m "Release vX.Y.Z"
git push origin vX.Y.Z

# Create GitHub release
gh release create vX.Y.Z --generate-notes

What NOT to do

  • NEVER release without CI verification
  • NEVER push tags before PR is merged and CI passes
  • NEVER assume CI will pass — always watch it complete
  • NEVER release if any fusion-correctness test fails