gale/MODULE.bazel at main · pulseengine/gale · 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
"""Gale — formally verified Zephyr kernel primitives for ASIL-D safety-critical systems.

Zephyr's wind, hardened through formal verification.
Verus (SMT/Z3) + Rocq (theorem proving).
"""

module(
    name = "gale",
    version = "0.1.0",
    compatibility_level = 1,
)

# Verus verification rules
bazel_dep(name = "rules_verus", version = "0.1.0")
git_override(
    module_name = "rules_verus",
    remote = "https://github.com/pulseengine/rules_verus.git",
    commit = "f84a0a55593bbb1a7eb64d044eea3ee8f27fe1ea",  # PR #20: fix sysroot extraction via tar
)

# Rocq + coq-of-rust rules
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 = "2cfb99ca46eb570c5dc54ed1ee2124b8add212e2",
)

# rocq-of-rust toolchain — translates Rust to Rocq
rocq_of_rust = use_extension("@rules_rocq_rust//coq_of_rust:extensions.bzl", "rocq_of_rust")
rocq_of_rust.toolchain(
    use_real_library = True,
)
use_repo(rocq_of_rust, "rocq_of_rust_toolchains", "rocq_of_rust_source")
register_toolchains("@rocq_of_rust_toolchains//:toolchain")

# Rust rules — used for verus-strip tool and future Rust targets
bazel_dep(name = "rules_rust", version = "0.69.0")

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

# Crate dependencies for verus-strip tool
crate = use_extension("@rules_rust//crate_universe:extensions.bzl", "crate")
crate.from_cargo(
    name = "crates",
    cargo_lockfile = "//tools/verus-strip:Cargo.lock",
    manifests = ["//tools/verus-strip:Cargo.toml"],
)
use_repo(crate, "crates")

# Lean 4 rules — scheduling theory proofs
bazel_dep(name = "rules_lean", version = "0.1.0")
git_override(
    module_name = "rules_lean",
    remote = "https://github.com/pulseengine/rules_lean.git",
    commit = "2fe64f13f8df31678a27483286868a67636d7217",
    patches = ["//patches:rules_lean_mathlib_timeout.patch"],
    patch_strip = 1,
)

# Lean 4 toolchain + Mathlib (mathlib declared by rules_lean, just use_repo it)
lean = use_extension("@rules_lean//lean:extensions.bzl", "lean")
lean.toolchain(version = "4.27.0")
use_repo(lean, "lean_toolchains", "mathlib")
register_toolchains("@lean_toolchains//:all")

# Renode emulation — handled by GitHub Actions (renode-tests.yml), not Bazel.
# rules_renode removed: download_portable URL was broken, blocking all Bazel targets.
# Re-add when renode-bazel-rules has a working default URL.

# Nix integration for Rocq toolchain
bazel_dep(name = "rules_nixpkgs_core", version = "0.13.0")

# Configure nixpkgs
nix_repo = use_extension(
    "@rules_nixpkgs_core//extensions:repository.bzl",
    "nix_repo",
)
nix_repo.github(
    name = "nixpkgs",
    org = "NixOS",
    repo = "nixpkgs",
    commit = "88d3861acdd3d2f0e361767018218e51810df8a1",
    sha256 = "",
)
use_repo(nix_repo, "nixpkgs")