feat: bootstrap rivet verification scaffolding, seed hazard analysis for #37

artifacts/requirements.yaml

@@ -0,0 +1,125 @@
+artifacts:
+  - id: REQ-001
+    type: requirement
+    title: Proof-obligation build rules shall only report success on a version-matched, zero-exit kernel check
+    status: approved
+    priority: must
+    description: >
+      Addresses CC-001 / H-001. Applies to `rocq_library`, `rocq_proof_test`,
+      and every proof-obligation rule this toolchain provides.
+    fields:
+      category: constraint
+      upstream-ref: "pulseengine/rules_rocq_rust#31"
+    links:
+      - type: constraint-satisfies
+        target: CC-001
+      - type: satisfies
+        target: H-001
+
+  - id: REQ-002
+    type: requirement
+    title: The toolchain shall support machine-checked floating-point error-bound proofs, kernel-replaying every Gappa certificate
+    status: draft
+    priority: must
+    description: >
+      Add Flocq (fp model), Coq-Gappa + the `gappa` binary (rounding-error
+      layer), and Coq-Interval (approximation-error layer) to the toolchain
+      flake, pinned against the bundled Rocq version. Any rule built on top of
+      Gappa must satisfy CC-002 — the Gappa-emitted proof term is always
+      replayed through the Rocq kernel, never trusted as-is.
+    fields:
+      category: functional
+      upstream-ref: "pulseengine/rules_rocq_rust#37"
+    links:
+      - type: constraint-satisfies
+        target: CC-002
+
+  - id: DD-002
+    type: design-decision
+    title: Rely on Bazel action-failure semantics plus explicit Rocq-version pinning to satisfy REQ-001
+    status: approved
+    description: >
+      Existing mechanism that already satisfies REQ-001 for today's
+      `rocq_library`/`rocq_proof_test` rules.
+    fields:
+      decision: >
+        `rocq_library` and `rocq_proof_test` invoke `coqc`/`rocq` as a Bazel
+        action; a non-zero exit fails the action (and the build) directly, so
+        there is no separate "report PASS" step that could mask a kernel
+        failure. Version-matching is enforced by pinning every dependency
+        (rocq-core, coqutil, hammer, smpl) to the single Rocq version declared
+        in `MODULE.bazel`'s `rocq.toolchain()` per-repo, rather than resolving
+        them independently — the smpl `.vo` version mismatch fixed in PR #30
+        (16f6ff2, "build smpl against matching Rocq version") is this
+        mechanism being repaired, not a new one being introduced.
+      rationale: >
+        Bazel's own action-failure propagation is a stronger oracle than any
+        rule-level status flag the build script could set and get wrong; the
+        gap that actually bit us (#31, PR #30) was a *dependency* pinned to
+        the wrong Rocq version producing a `.vo` the kernel silently accepted
+        as compatible, not the build masking a real failure.
+      alternatives: >
+        A rule-level "did the kernel actually check this" flag written by the
+        build script — rejected as strictly weaker than letting the action
+        itself fail, and it would be one more thing to get wrong.
+      source-ref: "pulseengine/rules_rocq_rust#31, PR #30"
+    links:
+      - type: satisfies
+        target: REQ-001
+
+  - id: DD-001
+    type: design-decision
+    title: Layer Gappa (rounding) + Coq-Interval (approximation) + Flocq (fp model), kernel-replay every Gappa certificate
+    status: approved
+    description: >
+      Toolchain architecture for issue #37's floating-point error-bound proof
+      capability.
+    fields:
+      decision: >
+        Add coq-flocq, coq-gappa (+ the gappa binary), coq-interval, and
+        coq-coquelicot to the Nix-pinned toolchain flake, exposing their
+        .vo/include paths so `rocq_library` can depend on them (or a thin
+        `gappa_proof` rule wrapping the gappa-to-Rocq flow). A complete kernel
+        bound = Gappa (rounding, semi-automatic via interval arithmetic +
+        rewriting) + Coq-Interval (approximation, Taylor-model/interval bounds
+        on the minimax remainder) + Flocq (the underlying fp model) — and
+        whatever wraps Gappa must always kernel-check its emitted Flocq proof
+        term, never accept Gappa's own certificate-generation success as
+        sufficient (see the controller-constraint on gappa-wrapping rules).
+      rationale: >
+        Gappa is semi-automatic and emits a Flocq/Rocq proof term the kernel
+        checks — dramatically less manual labor than hand-written Rocq for the
+        rounding-error layer (Cody-Waite reduction + Horner accumulation), but
+        it does not cover the approximation-error layer (the minimax remainder
+        bound), which needs Coq-Interval or an externally-checked Sollya
+        certificate. Filed by the relay maintainer against relay's exhaustively
+        enumerated f32 sin/cos kernels (worst abs error 1.19e-7, falcon
+        MATHF32-P02) as the next assurance-level investment.
+      alternatives: >
+        Base Rocq + Flocq alone, with no Gappa/Coq-Interval — maximally
+        flexible but hundreds of manual proof lines per function; rejected as
+        the primary path (the crlibm/CORE-MATH literature shows this is a
+        multi-week effort per kernel even with the tools).
+      source-ref: "pulseengine/rules_rocq_rust#37"
+    links:
+      - type: satisfies
+        target: REQ-002
+
+  - id: FEAT-001
+    type: feature
+    title: Machine-checked FP error-bound proofs (Flocq + Gappa + Coq-Interval)
+    status: draft
+    description: >
+      Toolchain capability requested in #37, enabling a raise-assurance proof
+      on top of relay's existing exhaustive-enumeration empirical bound.
+    fields:
+      phase: future
+      acceptance-criteria:
+        - "Toolchain flake provides coq-flocq, coq-gappa (+ gappa binary), coq-interval, coq-coquelicot, pinned against the bundled Rocq version"
+        - "rocq_library (or a new gappa_proof rule) can depend on the new packages' .vo/include paths"
+        - "A minimal example proves one f32 rounding bound end-to-end, kernel-checked by Rocq, as the template for relay's kernels"
+    links:
+      - type: satisfies
+        target: REQ-002
+      - type: implements
+        target: DD-001

artifacts/safety.yaml

@@ -0,0 +1,146 @@
+artifacts:
+  - id: L-001
+    type: loss
+    title: Loss of trust in a verification claim produced by this toolchain
+    status: draft
+    description: >
+      A `rocq_proof_test` (or any future proof-obligation rule built on this
+      toolchain) is reported as passing when the claimed property was not
+      actually kernel-checked by Rocq. Consumers of rules_rocq_rust — including
+      safety-critical downstream projects such as relay's flight-math kernels —
+      rely on a green build as evidence that a proof holds. A false-positive
+      "verified" signal from the tool propagates a false assurance claim into
+      whatever the consumer ships.
+    fields:
+      stakeholders: [rules_rocq_rust-consumers, relay-flight-math, downstream-safety-cases]
+
+  - id: H-001
+    type: hazard
+    title: Toolchain reports a Rocq proof as checked when the kernel did not verify it
+    status: draft
+    description: >
+      The build accepts a `.vo` (compiled proof) as evidence of a passing
+      proof obligation without the Rocq kernel actually having type-checked it
+      against the pinned toolchain version — e.g. a stale or version-mismatched
+      `.vo` is treated as valid, or a non-zero `coqc`/`rocq` exit is masked by
+      the build rule. (This is exactly the failure class fixed ad hoc for smpl
+      in PR #30 — a `.vo` version mismatch between Rocq 9.0 and 9.1 — and for
+      `rocq_library`'s `-Q` path handling in #35; H-001 exists so future
+      instances are caught by design instead of by incident.)
+    fields:
+      severity: critical
+    links:
+      - type: leads-to-loss
+        target: L-001
+
+  - id: H-002
+    type: hazard
+    title: A Gappa-emitted rounding-error certificate is trusted without Rocq kernel replay
+    status: draft
+    description: >
+      Gappa establishes a floating-point rounding-error bound outside Rocq and
+      emits a Flocq/Rocq proof term as its certificate. If a build rule accepts
+      Gappa's report of success directly — without feeding that emitted proof
+      term back through the Rocq kernel — the claimed error bound is asserted
+      by an external, un-kernel-checked tool rather than proven. This is the
+      concrete new risk introduced by issue #37 (adding Flocq + Gappa +
+      Coq-Interval to enable machine-checked FP error-bound proofs for
+      relay's flight-math kernels).
+    fields:
+      severity: critical
+    links:
+      - type: leads-to-loss
+        target: L-001
+
+  - id: CTRL-001
+    type: controller
+    title: Rocq proof-obligation build rules (rocq_library / rocq_proof_test / future gappa_proof)
+    status: draft
+    description: >
+      The Bazel rules that compile `.v` sources and report whether a proof
+      obligation is satisfied. This is the tool's own correctness-critical
+      control point — the inward-facing oracle for the whole toolchain.
+    fields:
+      controller-type: automated
+
+  - id: UCA-001
+    type: uca
+    title: Proof-obligation rule reports PASS without a successful, version-matched kernel check
+    status: draft
+    description: >
+      Providing a "proof checked" signal when the underlying `coqc`/`rocq`
+      process did not exit zero, or when the checked `.vo` was compiled
+      against a different Rocq version than the toolchain currently pins,
+      leads to H-001.
+    fields:
+      uca-type: providing
+      context: >
+        Any `rocq_library`/`rocq_proof_test` target build, across a Rocq
+        version bump (e.g. the in-flight 9.0 -> 9.1 upgrade, PR #30/#31) or a
+        misconfigured `-Q`/include-path (#35's failure mode).
+    links:
+      - type: issued-by
+        target: CTRL-001
+      - type: leads-to-hazard
+        target: H-001
+
+  - id: UCA-002
+    type: uca
+    title: FP error-bound proof obligation accepted from Gappa's own report, without kernel replay
+    status: draft
+    description: >
+      Providing a "floating-point error bound proven" signal based on Gappa's
+      certificate generation succeeding, without invoking Rocq to kernel-check
+      the Flocq proof term Gappa emitted, leads to H-002.
+    fields:
+      uca-type: providing
+      context: >
+        Any future `gappa_proof` (or equivalent) rule built for issue #37's
+        Flocq + Gappa + Coq-Interval toolchain addition.
+    links:
+      - type: issued-by
+        target: CTRL-001
+      - type: leads-to-hazard
+        target: H-002
+
+  - id: CC-001
+    type: controller-constraint
+    title: Proof-obligation rules must only report PASS on a zero-exit, version-matched kernel check
+    status: draft
+    description: >
+      Inverts UCA-001.
+    fields:
+      constraint: >
+        A `rocq_library`/`rocq_proof_test` target must report its proof
+        obligation as satisfied only when (a) `coqc`/`rocq` exits zero on the
+        `.v` source, and (b) the resulting `.vo`'s compiled-against Rocq
+        version matches the toolchain version currently registered — never
+        infer success from a cached/stale artifact or a partial build graph.
+    links:
+      - type: constrains-controller
+        target: CTRL-001
+      - type: inverts-uca
+        target: UCA-001
+      - type: prevents
+        target: H-001
+
+  - id: CC-002
+    type: controller-constraint
+    title: A gappa_proof rule must kernel-check Gappa's emitted Flocq proof term, never trust the certificate directly
+    status: draft
+    description: >
+      Inverts UCA-002.
+    fields:
+      constraint: >
+        Any rule that wraps the Gappa rounding-error prover must feed Gappa's
+        emitted Flocq/Rocq proof term back through the Rocq kernel and report
+        the proof obligation as satisfied only on a successful, version-matched
+        kernel check of that term — Gappa's own certificate-generation success
+        is never sufficient by itself.
+    links:
+      - type: constrains-controller
+        target: CTRL-001
+      - type: inverts-uca
+        target: UCA-002
+      - type: prevents
+        target: H-002

docs/getting-started.md

@@ -0,0 +1,17 @@
+# rules_rocq_rust
+
+Getting started with your rivet project.
+
+## Overview
+
+This project uses [rivet](https://github.com/pulseengine/rivet) for SDLC artifact
+traceability and validation. Artifacts are stored as YAML files in `artifacts/` and
+validated against schemas listed in `rivet.yaml`.
+
+## Quick start
+
+```bash
+rivet validate     # Validate all artifacts
+rivet list         # List all artifacts
+rivet stats        # Show summary statistics
+```

rivet.yaml

@@ -0,0 +1,11 @@
+project:
+  name: rules_rocq_rust
+  version: "0.1.0"
+  schemas:
+    - common
+    - stpa
+    - dev
+
+sources:
+  - path: artifacts
+    format: generic-yaml