Skip to content

docs: align README with PulseEngine visual identity #20

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
avrabe merged 1 commit into from
Feb 20, 2026
Merged

docs: align README with PulseEngine visual identity #20

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
176 changes: 42 additions & 134 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,46 +1,52 @@
<div align="center">

# rules_rocq_rust

<sup>Bazel rules for Rocq theorem proving and Rust formal verification</sup>

&nbsp;

![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)

</div>

&nbsp;

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)

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"
```

Expand Down Expand Up @@ -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"],
Expand All @@ -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`) |
Expand All @@ -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 |
Expand All @@ -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 &mdash; see [LICENSE](LICENSE).

## License
---

Apache License 2.0 - See [LICENSE](LICENSE)
<div align="center">

## Related Projects
<sub>Part of <a href="https://github.com/pulseengine">PulseEngine</a> &mdash; formally verified WebAssembly toolchain for safety-critical systems</sub>

- [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
</div>
Loading