diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml new file mode 100644 index 0000000..a8c2eb2 --- /dev/null +++ b/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 diff --git a/artifacts/safety.yaml b/artifacts/safety.yaml new file mode 100644 index 0000000..ea07170 --- /dev/null +++ b/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 diff --git a/docs/getting-started.md b/docs/getting-started.md new file mode 100644 index 0000000..e9168f2 --- /dev/null +++ b/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 +``` diff --git a/rivet.yaml b/rivet.yaml new file mode 100644 index 0000000..874f168 --- /dev/null +++ b/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