wsc 0.8.0

WebAssembly Signature Component - WASM signing and verification toolkit
Documentation 
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

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.

verus_library(
    name = "wsc_merkle_proofs",
    srcs = [
        "mod.rs",
        "merkle_proofs.rs",
        "dsse_proofs.rs",
    ],
    crate_root = "mod.rs",
    crate_name = "wsc_verus_proofs",
    visibility = ["//visibility:public"],
)

verus_test(
    name = "wsc_merkle_verify",
    srcs = [
        "mod.rs",
        "merkle_proofs.rs",
        "dsse_proofs.rs",
    ],
    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"],
)