rivet/MODULE.bazel at main · pulseengine/rivet · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
# 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",
    # e4660cc: build: migrate rocq-of-rust to a hermetic rules_rust toolchain (#34).
    commit = "e4660cc1b06fc4c0aefb49401fa2e2184cf804e3",
)

# 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")

# ── rules_wasm_component (REQ-086 Wasm component + witness MC/DC) ──────
#
# Org-standard Bazel rules for WebAssembly Component Model builds.
# Bundles the `witness` toolchain (toolchains/witness_toolchain.bzl) and
# the `wasm_module_coverage` rule, which is how we produce MC/DC coverage
# evidence on the feature-model composition core (REQ-086).
#
# Not in the Bazel Central Registry — pinned via git_override to a
# specific commit on pulseengine/rules_wasm_component, mirroring the
# rules_rocq_rust pattern above.
bazel_dep(name = "rules_wasm_component", version = "1.0.0")

git_override(
    module_name = "rules_wasm_component",
    remote = "https://github.com/pulseengine/rules_wasm_component.git",
    # d2347fb: chore(deps): bump PulseEngine toolchains (#471) — current
    # main HEAD on rules_wasm_component. The earlier fbe2057 pin no
    # longer resolves under Bazel's shallow git fetch on self-hosted
    # runners (it's still in upstream history; the issue is shallow
    # depth), so track HEAD instead.
    commit = "d2347fbf79ee5d4e20de0df7e8c1bb3adadf5cfe",
)