diff --git a/README.md b/README.md index 8b17f77..5ec1f67 100644 --- a/README.md +++ b/README.md @@ -1,32 +1,43 @@ +
+ # rules_rocq_rust +Bazel rules for Rocq theorem proving and Rust formal verification + +  + +![Bazel](https://img.shields.io/badge/Bazel-43A047?style=flat-square&logo=bazel&logoColor=white&labelColor=1a1b27) +![Formally Verified](https://img.shields.io/badge/Formally_Verified-00C853?style=flat-square&logoColor=white&labelColor=1a1b27) +![License: Apache-2.0](https://img.shields.io/badge/License-Apache--2.0-blue?style=flat-square&labelColor=1a1b27) + +
+ +  + Bazel rules for Rocq/Coq theorem proving and Rust formal verification with hermetic toolchain support via [Nix](https://nixos.org/). +> [!NOTE] +> Part of the PulseEngine toolchain. Powers the mechanized proofs in Meld, Loom, and PulseEngine verification infrastructure. + ## Features -- **Rust → Rocq → Proofs**: Complete pipeline from Rust code to verified proofs +- **Rust to Rocq to Proofs**: Complete pipeline from Rust code to verified proofs - **rocq-of-rust Integration**: Translate Rust to Rocq via [rocq-of-rust](https://github.com/formal-land/rocq-of-rust) - **Hermetic Toolchains**: Rocq 9.0, coqutil, Hammer, smpl via nixpkgs -- **Cross-Platform**: Linux, macOS (Intel & Apple Silicon) +- **Cross-Platform**: Linux, macOS (Intel and Apple Silicon) - **Bazel 8 bzlmod**: Modern module system support ## Prerequisites ### Nix (Required) -Nix is required for the Rocq toolchain. - -**macOS:** ```bash +# macOS sh <(curl -L https://nixos.org/nix/install) . /nix/var/nix/profiles/default/etc/profile.d/nix-daemon.sh -nix --version -``` -**Linux:** -```bash +# Linux sh <(curl -L https://nixos.org/nix/install) --daemon -nix --version ``` ### Rust Nightly (Linux only) @@ -34,13 +45,8 @@ nix --version On Linux, rocq-of-rust requires Rust nightly with rustc internals: ```bash -# Install nightly toolchain rustup toolchain install nightly-2024-12-01 - -# Add required components rustup component add rustc-dev rust-src --toolchain nightly-2024-12-01 - -# Set library path for LLVM (add to ~/.bashrc or ~/.zshrc) export LIBRARY_PATH="$(rustc +nightly-2024-12-01 --print sysroot)/lib:$LIBRARY_PATH" ``` @@ -91,14 +97,12 @@ impl Point { load("@rules_rocq_rust//coq_of_rust:defs.bzl", "rocq_rust_verified_library") load("@rules_rocq_rust//rocq:defs.bzl", "rocq_library") -# One-liner: translate and compile rocq_rust_verified_library( name = "point_verified", rust_sources = ["point.rs"], extra_flags = ["-impredicative-set"], ) -# Write proofs about the Rust code rocq_library( name = "point_proofs", srcs = ["point_proofs.v"], @@ -119,16 +123,6 @@ bazel build //:point_proofs Compiles Rocq `.v` files to `.vo`. -```starlark -rocq_library( - name = "my_proofs", - srcs = ["proof.v"], - deps = [":other_library"], - include_path = "MyProject", # Logical path prefix - extra_flags = ["-impredicative-set"], -) -``` - | Attribute | Description | |-----------|-------------| | `srcs` | Rocq source files (`.v`) | @@ -140,14 +134,6 @@ rocq_library( Translates Rust source files to Rocq. -```starlark -coq_of_rust_library( - name = "translated", - rust_sources = ["lib.rs"], - edition = "2021", -) -``` - | Attribute | Description | |-----------|-------------| | `rust_sources` | Rust source files to translate | @@ -157,139 +143,61 @@ coq_of_rust_library( Convenience macro: translates Rust to Rocq and compiles. -```starlark -rocq_rust_verified_library( - name = "verified", - rust_sources = ["lib.rs"], - edition = "2021", - deps = [], # Additional Rocq dependencies - extra_flags = ["-impredicative-set"], -) -``` - ### rocq_proof_test Test rule that verifies proofs compile successfully. -```starlark -rocq_proof_test( - name = "proofs_test", - srcs = ["proofs.v"], - deps = [":proofs"], -) -``` - -## Configuration Options +## Toolchain Contents -### rocq_of_rust.toolchain() +| Component | Description | +|-----------|-------------| +| Rocq 9.0 | Core theorem prover | +| coqutil | Utility library | +| Hammer | Automated proof tactics | +| smpl | Simplification tactics | +| rocq-of-rust | Rust-to-Rocq translator (pinned version) | -```starlark -rocq_of_rust.toolchain( - use_real_library = True, # Use full RocqOfRust library (recommended) - fail_on_error = True, # Fail if rocq-of-rust build fails (default: True) - rust_nightly = "nightly-2024-12-01", # Rust nightly version -) -``` +## Supported Platforms -| Option | Description | -|--------|-------------| -| `use_real_library` | Use full RocqOfRust library with coqutil/hammer/smpl | -| `fail_on_error` | Fail build if rocq-of-rust cannot be built | -| `rust_nightly` | Rust nightly version for building rocq-of-rust | +| Platform | Status | +|----------|--------| +| Linux x86_64 | Supported | +| Linux aarch64 | Supported | +| macOS x86_64 | Supported | +| macOS aarch64 | Supported | ## Troubleshooting ### "unable to find library -lLLVM-19-rust-*" (Linux) -The Rust nightly compiler bundles its own LLVM. Set `LIBRARY_PATH`: - ```bash export LIBRARY_PATH="$(rustc +nightly-2024-12-01 --print sysroot)/lib:$LIBRARY_PATH" ``` -### "cargo not found" - -Install Rust via rustup: - -```bash -curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -``` - ### "rustc-dev component not found" -Install the required nightly components: - ```bash rustup component add rustc-dev rust-src --toolchain nightly-2024-12-01 ``` -### Build fails silently with placeholder - -By default, builds fail loudly. If you see placeholder output, check the build logs for the actual error. To debug, run: - -```bash -bazel build @rocq_of_rust_source//:rocq_of_rust_main --verbose_failures -``` - -### Proofs fail with "reference not found" - -Ensure the translated code compiled successfully first: - -```bash -bazel build //:point_compiled -``` - -Then check that your proof imports match the generated module names. - ## Example See `examples/rust_to_rocq/` for a complete working example: -- `point.rs` - Rust source with Point and Rectangle structs -- `advanced.rs` - Generics, traits, lifetimes, enums -- `point_proofs.v` - Formal proofs about the translated code - ```bash -# Build all examples bazel build //examples/rust_to_rocq:point_proofs bazel build //examples/rust_to_rocq:advanced_verified - -# Run proof tests bazel test //examples/rust_to_rocq:point_proofs_test ``` -## How It Works - -1. **rocq-of-rust** translates Rust source to Rocq using a deeply embedded monadic DSL -2. **coqc** compiles the translated `.v` files with the RocqOfRust library -3. You write proofs in Rocq that reason about the translated Rust semantics -4. Proofs are machine-checked by the Rocq type system - -## Toolchain Contents - -| Component | Description | -|-----------|-------------| -| Rocq 9.0 | Core theorem prover | -| coqutil | Utility library | -| Hammer | Automated proof tactics | -| smpl | Simplification tactics | -| rocq-of-rust | Rust-to-Rocq translator (pinned version) | - -## Supported Platforms +## License -| Platform | Status | -|----------|--------| -| Linux x86_64 | ✅ | -| Linux aarch64 | ✅ | -| macOS x86_64 | ✅ | -| macOS aarch64 | ✅ | +Apache-2.0 — see [LICENSE](LICENSE). -## License +--- -Apache License 2.0 - See [LICENSE](LICENSE) +
-## Related Projects +Part of PulseEngine — formally verified WebAssembly toolchain for safety-critical systems -- [rocq-of-rust](https://github.com/formal-land/rocq-of-rust) - Rust to Rocq translator -- [nixpkgs](https://github.com/NixOS/nixpkgs) - Nix packages -- [Rocq Prover](https://rocq-prover.org/) - The Rocq theorem prover +