synth/MODULE.bazel at main · pulseengine/synth · 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
"""
Synth - WebAssembly Component Synthesizer for Embedded Systems
Bazel module definition
"""

module(
    name = "synth",
    # Kept in lockstep with [workspace.package] version in Cargo.toml.
    # Both are bumped pre-tag — see docs/release-process.md.
    version = "0.18.0",
)

# Bazel dependencies
bazel_dep(name = "platforms", version = "0.0.10")
bazel_dep(name = "bazel_skylib", version = "1.7.1")
bazel_dep(name = "rules_rust", version = "0.68.1")
bazel_dep(name = "rules_cc", version = "0.2.17")


# CC toolchain (required by Bazel 8 for linking Rust binaries)
cc_configure = use_extension("@rules_cc//cc:extensions.bzl", "cc_configure_extension")
use_repo(cc_configure, "local_config_cc", "local_config_cc_toolchains")
register_toolchains("@local_config_cc_toolchains//:all")

# Rust toolchains
rust = use_extension("@rules_rust//rust:extensions.bzl", "rust")
rust.toolchain(
    edition = "2024",
    versions = ["1.88.0"],
)
use_repo(rust, "rust_toolchains")
register_toolchains("@rust_toolchains//:all")

# Rust crates repository — resolved from Cargo.lock via from_cargo rather than
# hand-maintained crate.spec pins, so the Bazel crate set always matches the
# cargo workspace and a new dep (e.g. scry-sai-core for VCR-MEM-001 layer-2,
# #242) needs no manual MODULE.bazel entry. Replaces the prior 21 crate.spec
# block (which had drifted: z3 pinned 0.12 here vs 0.19 in synth-verify).
crate = use_extension("@rules_rust//crate_universe:extension.bzl", "crate")
crate.from_cargo(
    cargo_lockfile = "//:Cargo.lock",
    manifests = ["//:Cargo.toml"],
)
use_repo(crate, "crates")

# Verus formal verification (SMT/Z3 track)
# Provides verus_library, verus_test, verus_strip, verus_strip_test
bazel_dep(name = "rules_verus", version = "0.0.0")
git_override(
    module_name = "rules_verus",
    remote = "https://github.com/pulseengine/rules_verus.git",
    commit = "a49f72ef",  # fix: bundle Rust nightly sysroot with Verus toolchain
)

verus = use_extension("@rules_verus//verus:extensions.bzl", "verus")
use_repo(verus, "verus_toolchains")
register_toolchains("@verus_toolchains//:all")

# PulseEngine WebAssembly Component Model rules
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",
    commit = "43468cd52f6a09523fc4df08d17e88f67f1cfd82",  # v1.0.0
)

# Renode simulation rules for embedded testing
# Provides hermetic Renode + Python - no local install required
# Using PulseEngine fork with macOS support
bazel_dep(name = "rules_renode", version = "0.0.0")
git_override(
    module_name = "rules_renode",
    remote = "https://github.com/pulseengine/renode-bazel-rules.git",
    commit = "cf0dcfa9338e235a076542154e9f95ece5092b11",  # feat/macos-support
)

# Renode toolchain - auto-downloads appropriate platform build
renode = use_extension("@rules_renode//renode:extensions.bzl", "renode")
use_repo(renode, "renode_toolchains")
register_toolchains("@renode_toolchains//:all")

# Rocq/Coq theorem proving rules with coq-of-rust integration
# Provides hermetic Rocq 9.0 toolchain via Nix for formal verification
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",
    commit = "090b875c6e83e32e25918f31b8c58919ff16467e",  # 2026-02-04
    patches = ["//patches:rules_rocq_rust_nix_name.patch"],
    patch_strip = 1,
)
rocq = use_extension("@rules_rocq_rust//rocq:extensions.bzl", "rocq")
rocq.toolchain(version = "9.0", strategy = "nix", with_rocq_of_rust_deps = True)
use_repo(rocq, "rocq_toolchains")
register_toolchains("@rocq_toolchains//:all")