From 37dd46b12b466c2ca9f737b9d907855eed053f59 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 28 Mar 2026 18:25:43 +0100 Subject: [PATCH] =?UTF-8?q?feat:=20full=20Verus=20pipeline=20=E2=80=94=20v?= =?UTF-8?q?erify=20+=20strip=20with=20hermetic=20sysroot?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit rules_verus 8a2bbf6: hermetic Rust sysroot, no rustup needed. Both targets pass: - verus_library: SMT verification (6 proofs verified) - verus_strip: strips annotations → plain Rust for coq-of-rust Pipeline: Verus specs → Z3 verify → strip → plain Rust → coq-of-rust → Rocq Co-Authored-By: Claude Opus 4.6 (1M context) --- MODULE.bazel | 2 +- src/lib/src/verus_proofs/BUILD.bazel | 18 ++++++++++++++++-- 2 files changed, 17 insertions(+), 3 deletions(-) diff --git a/MODULE.bazel b/MODULE.bazel index 94ca14d..2a4ee8f 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -112,7 +112,7 @@ bazel_dep(name = "rules_verus", version = "0.1.0") git_override( module_name = "rules_verus", - commit = "e2c1600", + commit = "8a2bbf6", remote = "https://github.com/pulseengine/rules_verus.git", ) diff --git a/src/lib/src/verus_proofs/BUILD.bazel b/src/lib/src/verus_proofs/BUILD.bazel index b9c3d04..e07be31 100644 --- a/src/lib/src/verus_proofs/BUILD.bazel +++ b/src/lib/src/verus_proofs/BUILD.bazel @@ -1,6 +1,8 @@ -load("@rules_verus//verus:defs.bzl", "verus_library", "verus_test") +load("@rules_verus//verus:defs.bzl", "verus_library", "verus_strip", "verus_test") + +# ── Track 1: Verus SMT verification (CV-20, CV-21, CV-22) ────────── +# Fully hermetic — bundled Rust sysroot, no rustup needed. -# Merkle tree inclusion proof soundness (CV-20) and anti-rollback (CV-21) verus_library( name = "wsc_merkle_proofs", srcs = [ @@ -23,3 +25,15 @@ verus_test( crate_root = "mod.rs", crate_name = "wsc_verus_proofs", ) + +# ── Track 2: Strip Verus → plain Rust for coq-of-rust pipeline ───── + +verus_strip( + name = "wsc_proofs_stripped", + srcs = [ + "mod.rs", + "merkle_proofs.rs", + "dsse_proofs.rs", + ], + visibility = ["//visibility:public"], +)