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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
"""
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.55.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",
        # VCR-WASM-001 phase 3 (#242): generic extra-coq-package hook. Lets a
        # module pull an arbitrary coqPackages.<attr> from the pinned nixpkgs
        # into the hermetic toolchain via a `rocq.extra_coq_package(...)` tag,
        # without forking this ruleset. Inert unless such a tag is declared —
        # closes named blocker (1) for wiring the REAL WasmCert-Coq dependency.
        # The dep itself stays PENDING on blockers (2)+(3): nixpkgs pin
        # 88d3861a ships coqPackages.wasmcert 2.2.0, which propagates
        # coqPackages.compcert 3.16 (license inria-compcert, unfree) — refused
        # by CI's no-unfree-dep policy. Upstream wasmcert 2.2.1 drops CompCert;
        # the next nixpkgs bump carrying >=2.2.1 removes (2)+(3), at which
        # point a single `rocq.extra_coq_package(name=..., attribute_path=
        # "coqPackages.wasmcert")` tag + a Require swap retires the
        # transcription. See coq/Synth/WASM/WasmCertReference.v header and the
        # VCR-WASM-001 entry in artifacts/verified-codegen-roadmap.yaml.
        "//patches:rules_rocq_rust_extra_coq_pkg.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)

# The generic extra-coq-package hook (VCR-WASM-001 phase 3) is LANDED and inert:
# no `rocq.extra_coq_package(...)` tag is declared here because the only intended
# consumer — the real WasmCert-Coq dependency — stays PENDING on the unfree
# CompCert 3.16 that wasmcert 2.2.0 propagates in the current nixpkgs pin. When a
# pin carrying wasmcert >= 2.2.1 lands, uncomment:
#   rocq.extra_coq_package(name = "rocq_wasmcert", attribute_path = "coqPackages.wasmcert")
# and add `use_repo(rocq, "rocq_wasmcert")`.
use_repo(rocq, "rocq_toolchains")
register_toolchains("@rocq_toolchains//:all")