feat(rocq): add Flocq/Gappa/Coq-Interval for machine-checked FP error bounds

MODULE.bazel

@@ -38,25 +38,29 @@ nix_repo = use_extension(
 )
 nix_repo.github(
     name = "nixpkgs",
-    org = "NixOS",
-    repo = "nixpkgs",
     # nixos-unstable with Rocq 9.0.1, coq-hammer, coqutil (2026-04-01)
     commit = "6201e203d09599479a3b3450ed24fa81537ebc4e",
+    org = "NixOS",
+    repo = "nixpkgs",
     sha256 = "",  # Will be computed on first fetch
 )
 use_repo(nix_repo, "nixpkgs")
 
 # Rocq toolchain extension - uses nixpkgs for hermetic Rocq/Coq
 rocq = use_extension("//rocq:extensions.bzl", "rocq")
 rocq.toolchain(
+    strategy = "nix",  # Hermetic nix-based installation
     version = "9.0",  # Rocq 9.0.1 (required for real RocqOfRust library)
-    strategy = "nix",   # Hermetic nix-based installation
     with_rocq_of_rust_deps = True,  # Include coqutil, hammer, smpl
 )
+
 # smpl is built from source (rocq-9.0 branch) since nixpkgs only has up to Coq 8.15
 # rocq_stdlib is the separate stdlib package for Rocq 9.0
 # hammer_tactics is a separate package from hammer (plugin vs library)
-use_repo(rocq, "rocq_toolchains", "rocq_stdlib", "rocq_coqutil", "rocq_hammer", "rocq_hammer_tactics", "rocq_smpl")
+# flocq/interval/coquelicot/gappa_bin/gappalib enable machine-checked
+# floating-point error-bound proofs (#37); gappalib is built from source
+# against Flocq, same as smpl is built from source against Rocq 9.0
+use_repo(rocq, "rocq_coquelicot", "rocq_coqutil", "rocq_flocq", "rocq_gappa_bin", "rocq_gappalib", "rocq_hammer", "rocq_hammer_tactics", "rocq_interval", "rocq_smpl", "rocq_stdlib", "rocq_toolchains")
 
 # Register Rocq toolchain
 register_toolchains("@rocq_toolchains//:all")
@@ -101,7 +105,7 @@ rocq_of_rust.toolchain(
     # Uses pinned default: 877dd65142b3c5217ce6ae043ff49c8f540eb8a5
     use_real_library = True,  # Full library with coqutil + hammer + smpl
 )
-use_repo(rocq_of_rust, "rocq_of_rust_toolchains", "rocq_of_rust_build")
+use_repo(rocq_of_rust, "rocq_of_rust_build", "rocq_of_rust_toolchains")
 
 # Register rocq-of-rust toolchain
 register_toolchains("@rocq_of_rust_toolchains//:toolchain")

artifacts/requirements.yaml

@@ -19,14 +19,16 @@ artifacts:
   - id: REQ-002
     type: requirement
     title: The toolchain shall support machine-checked floating-point error-bound proofs, kernel-replaying every Gappa certificate
-    status: draft
+    status: implemented
     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.
+      Add Flocq (fp model), the `gappa` binary (rounding-error layer),
+      gappalib-coq (Gappa's Rocq support library, built from source against
+      Flocq — nixpkgs has no `coq-gappa` package at this pin), and Coq-Interval
+      + Coquelicot (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"
@@ -76,16 +78,27 @@ artifacts:
       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).
+        Add coq-flocq, coq-interval, and coq-coquelicot to the Nix-pinned
+        toolchain flake via nixpkgs (coqPackages.flocq/interval/coquelicot,
+        already built against the exact same Rocq 9.0.1 as the rest of the
+        toolchain), plus the standalone `gappa` binary (nixpkgs `gappa`, an
+        external CLI, not a Coq plugin). nixpkgs has no `coq-gappa`/
+        gappalib-coq package at this pin, so gappalib-coq (Gappa's Rocq
+        support library — the `Gappa.Gappa_library` that Gappa's `-Bcoq`
+        output `Require Import`s) is built from source against Flocq, the
+        same way `smpl` is already built from source for this Rocq version
+        (see gappalib_repository.bzl). A `gappa_proof` Bazel macro
+        (rocq:defs.bzl) wraps the gappa-to-Rocq flow: it runs `gappa -Bcoq`
+        in a genrule, then always compiles the emitted `.v` with
+        `rocq_library` — there is no separate "gappa succeeded" status,
+        only a normal coqc build that fails if the kernel rejects the proof.
+        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
@@ -108,16 +121,20 @@ artifacts:
   - id: FEAT-001
     type: feature
     title: Machine-checked FP error-bound proofs (Flocq + Gappa + Coq-Interval)
-    status: draft
+    status: implemented
     description: >
       Toolchain capability requested in #37, enabling a raise-assurance proof
       on top of relay's existing exhaustive-enumeration empirical bound.
+      Verified via `bazel test //examples/gappa_proof:rounding_bound_test`,
+      which exercises the full chain: a `.gappa` rounding-bound statement,
+      Gappa's `-Bcoq` codegen, and a real Rocq kernel check of the emitted
+      proof term against gappalib-coq/Flocq — PASSED.
     fields:
-      phase: future
+      phase: phase-1
       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"
+        - "Toolchain flake provides flocq, gappa (binary), gappalib-coq, interval, coquelicot, pinned against the bundled Rocq version -- DONE (rocq/extensions.bzl, rocq/private/gappalib_repository.bzl)"
+        - "rocq_library (or a new gappa_proof rule) can depend on the new packages' .vo/include paths -- DONE (gappa_proof macro, rocq/defs.bzl)"
+        - "A minimal example proves one f32 rounding bound end-to-end, kernel-checked by Rocq, as the template for relay's kernels -- DONE (examples/gappa_proof, bazel test PASSED)"
     links:
       - type: satisfies
         target: REQ-002

examples/gappa_proof/BUILD.bazel

@@ -0,0 +1,19 @@
+# Minimal machine-checked floating-point error-bound proof (#37 / FEAT-001).
+#
+# Template for relay's flight-math kernels: a `.gappa` rounding-bound
+# statement, compiled through Gappa's `-Bcoq` backend and kernel-checked by
+# Rocq via gappa_proof (rocq:defs.bzl) -- never trusting Gappa's certificate
+# on its own (rivet CC-002).
+
+load("@rules_rocq_rust//rocq:defs.bzl", "gappa_proof", "rocq_proof_test")
+
+gappa_proof(
+    name = "rounding_bound",
+    src = "rounding_bound.gappa",
+)
+
+rocq_proof_test(
+    name = "rounding_bound_test",
+    srcs = [],
+    deps = [":rounding_bound"],
+)

examples/gappa_proof/rounding_bound.gappa

@@ -0,0 +1,13 @@
+# Minimal machine-checked floating-point error-bound proof (#37 / FEAT-001).
+#
+# Claim: rounding any x in [1, 2] to the nearest ieee_32 float introduces an
+# absolute error of at most 2^-24 (one ULP at that exponent).
+#
+# `gappa -Bcoq` turns this statement into a Rocq proof script built on top of
+# Flocq (via gappalib-coq's Gappa_library); see rocq/defs.bzl's gappa_proof
+# macro, which always kernel-checks the emitted script with coqc rather than
+# trusting Gappa's own certificate-generation success (rivet CC-002).
+
+@rnd = float<ieee_32,ne>;
+
+{ x in [1,2] -> |rnd(x) - x| <= 1b-24 }

rocq/defs.bzl

@@ -4,3 +4,37 @@ load("//rocq/private:rocq.bzl", _rocq_library = "rocq_library", _rocq_proof_test
 
 rocq_library = _rocq_library
 rocq_proof_test = _rocq_proof_test
+
+def gappa_proof(name, src, deps = [], extra_flags = [], visibility = None):
+    """Runs `gappa -Bcoq` on a `.gappa` source and kernel-checks the result.
+
+    Gappa establishes a floating-point rounding-error bound outside Rocq and
+    emits a Flocq/Rocq proof term as its certificate. Per rivet CC-002, that
+    certificate is never trusted on its own: this macro always compiles the
+    emitted proof term with `rocq_library`, so the target fails exactly like
+    any other Rocq proof if the kernel rejects what Gappa produced.
+
+    Args:
+        name: name of the resulting rocq_library target.
+        src: the `.gappa` input file.
+        deps: rocq_library deps for the generated proof (e.g. other rocq_library
+            targets); Flocq and Gappa's own support library are already
+            available toolchain-wide and don't need to be listed here.
+        extra_flags: extra flags forwarded to coqc, as in rocq_library.
+        visibility: visibility for the resulting rocq_library target.
+    """
+    generated = name + "_generated.v"
+    native.genrule(
+        name = name + "_gen",
+        srcs = [src],
+        outs = [generated],
+        cmd = "$(location @rocq_gappa_bin//:gappa) -Bcoq $(location %s) > $@" % src,
+        tools = ["@rocq_gappa_bin//:gappa"],
+    )
+    rocq_library(
+        name = name,
+        srcs = [generated],
+        deps = deps,
+        extra_flags = extra_flags,
+        visibility = visibility,
+    )

rocq/extensions.bzl

@@ -6,7 +6,8 @@ Supports Rocq 9.0.1+ and includes required external packages for rocq-of-rust.
 This extension creates its own nixpkgs repository internally for bzlmod compatibility.
 """
 
-load("@rules_nixpkgs_core//:nixpkgs.bzl", "nixpkgs_package", "nixpkgs_local_repository")
+load("@rules_nixpkgs_core//:nixpkgs.bzl", "nixpkgs_local_repository", "nixpkgs_package")
+load("//rocq/private:gappalib_repository.bzl", "gappalib_source")
 load("//rocq/private:smpl_repository.bzl", "smpl_source")
 
 # Default nixpkgs commit (nixos-unstable with Rocq 9.0.1)
@@ -102,6 +103,10 @@ rocq_toolchain_info(
     hammer_tactics_ocaml_plugins = "@rocq_hammer_tactics//:ocaml_plugins",
     smpl = "@rocq_smpl//:smpl",
     smpl_ocaml_plugins = "@rocq_smpl//:ocaml_plugins",
+    flocq = "@rocq_flocq//:flocq",
+    interval = "@rocq_interval//:interval",
+    coquelicot = "@rocq_coquelicot//:coquelicot",
+    gappalib = "@rocq_gappalib//:gappalib",
 )
 
 # Register as toolchain
@@ -205,6 +210,59 @@ filegroup(
 )
 '''
 
+# BUILD file for Flocq (floating-point formalization library)
+_FLOCQ_BUILD_FILE = '''
+package(default_visibility = ["//visibility:public"])
+
+filegroup(
+    name = "flocq",
+    srcs = glob([
+        "lib/coq/**/*.vo",
+        "lib/coq/**/*.glob",
+    ], allow_empty = True),
+)
+'''
+
+# BUILD file for Coq-Interval (interval arithmetic / approximation-error bounds)
+_INTERVAL_BUILD_FILE = '''
+package(default_visibility = ["//visibility:public"])
+
+filegroup(
+    name = "interval",
+    srcs = glob([
+        "lib/coq/**/*.vo",
+        "lib/coq/**/*.glob",
+    ], allow_empty = True),
+)
+'''
+
+# BUILD file for Coquelicot (real analysis library, Coq-Interval's dependency)
+_COQUELICOT_BUILD_FILE = '''
+package(default_visibility = ["//visibility:public"])
+
+filegroup(
+    name = "coquelicot",
+    srcs = glob([
+        "lib/coq/**/*.vo",
+        "lib/coq/**/*.glob",
+    ], allow_empty = True),
+)
+'''
+
+# BUILD file for the standalone gappa binary (external rounding/approximation prover)
+# Gappa is not a Coq plugin -- it's an external CLI whose `-Bcoq` mode emits a
+# Rocq proof script (see gappa_proof in coq_of_rust:defs.bzl / rocq:defs.bzl,
+# and rivet CC-002: the emitted script is always kernel-checked, never trusted
+# as-is).
+_GAPPA_BIN_BUILD_FILE = '''
+package(default_visibility = ["//visibility:public"])
+
+filegroup(
+    name = "gappa",
+    srcs = ["bin/gappa"],
+)
+'''
+
 # BUILD file for Rocq stdlib (separate from rocq-core in 9.0)
 # Stdlib is at lib/coq/9.0/user-contrib/Stdlib
 _STDLIB_BUILD_FILE = '''
@@ -233,6 +291,7 @@ def _rocq_impl(module_ctx):
     Includes optional dependencies for rocq-of-rust (coqutil, hammer, smpl).
     Creates its own nixpkgs repository for bzlmod compatibility.
     """
+
     # Collect toolchain configurations from all modules
     toolchains = []
     for mod in module_ctx.modules:
@@ -316,6 +375,50 @@ import (builtins.fetchTarball {{
             branch = "rocq-9.0",
         )
 
+        # Flocq - floating-point formalization library (#37)
+        nixpkgs_package(
+            name = "rocq_flocq",
+            repository = nixpkgs_repo,
+            attribute_path = "coqPackages.flocq",
+            build_file_content = _FLOCQ_BUILD_FILE,
+        )
+
+        # Coq-Interval - approximation-error (minimax remainder) bounds (#37)
+        nixpkgs_package(
+            name = "rocq_interval",
+            repository = nixpkgs_repo,
+            attribute_path = "coqPackages.interval",
+            build_file_content = _INTERVAL_BUILD_FILE,
+        )
+
+        # Coquelicot - real analysis library, Coq-Interval's dependency (#37)
+        nixpkgs_package(
+            name = "rocq_coquelicot",
+            repository = nixpkgs_repo,
+            attribute_path = "coqPackages.coquelicot",
+            build_file_content = _COQUELICOT_BUILD_FILE,
+        )
+
+        # gappa - standalone rounding-error prover binary (#37). nixpkgs has no
+        # coq-gappa/gappalib-coq package for this Rocq version, only the CLI;
+        # the matching Rocq support library is built from source below.
+        nixpkgs_package(
+            name = "rocq_gappa_bin",
+            repository = nixpkgs_repo,
+            attribute_path = "gappa",
+            build_file_content = _GAPPA_BIN_BUILD_FILE,
+        )
+
+        # gappalib-coq - Gappa's Rocq support library, built from source
+        # against this toolchain's Flocq (see gappalib_repository.bzl for why
+        # nixpkgs can't provide this directly, and CC-002 for why the emitted
+        # proof term must always be kernel-checked rather than trusted as-is)
+        gappalib_source(
+            name = "rocq_gappalib",
+            version = "1.10.0",
+            nixpkgs_commit = _DEFAULT_NIXPKGS_COMMIT,
+        )
+
     # Return extension metadata (reproducible for caching)
     return module_ctx.extension_metadata(reproducible = True)