fix: audit formal-verif honesty — relabel admits, run bazel test

.github/workflows/formal-verification.yml

@@ -34,13 +34,20 @@ jobs:
         disk-cache: ${{ github.workflow }}
         repository-cache: true
 
+    # Audit 2026-04-30 finding C-7 (partial): the previous classification
+    # of "passes" assumed continue-on-error masking made these jobs green.
+    # Lifting the mask reveals real failures tied to audit C-1 — Verus
+    # `theorem_*` functions in src/lib/src/verus_proofs/ end in
+    # `assume(false)` and the proof obligations are not yet discharged.
+    # Mask retained until those obligations are mechanised; the job stays
+    # visible (no skip) so progress is observable.
     - name: Verify Merkle proofs (CV-20, CV-21)
       run: bazel build //src/lib/src/verus_proofs:wsc_merkle_proofs
-      continue-on-error: true
+      continue-on-error: true  # WIP — see audit C-1
 
     - name: Run Verus tests
       run: bazel test //src/lib/src/verus_proofs:wsc_merkle_verify
-      continue-on-error: true
+      continue-on-error: true  # WIP — see audit C-1
 
   kani-proofs:
     name: Kani ${{ matrix.module }}
@@ -72,12 +79,18 @@ jobs:
         cargo install --locked kani-verifier
         cargo kani setup
 
+    # Audit 2026-04-30 finding C-7 (partial): on inspection, several
+    # matrix jobs (format, merkle, wasm_module) fail when continue-on-error
+    # is removed. The harnesses cover specific bounded properties and not
+    # all are passing today. Mask retained per-job until the failing
+    # harnesses are fixed; varint and dsse pass cleanly today and could be
+    # ungated in a follow-up.
     - name: Run Kani ${{ matrix.module }} proofs
       env:
         HARNESS: ${{ matrix.harness }}
       run: cargo kani -p wsc --default-unwind 4 --output-format terse --harness "$HARNESS"
       timeout-minutes: 60
-      continue-on-error: true
+      continue-on-error: true  # WIP — see audit C-7 partial closure
 
   rocq-proofs:
     name: Rocq/coq-of-rust Translation
@@ -102,4 +115,7 @@ jobs:
       timeout-minutes: 30
       # coq-of-rust needs Rust nightly with LLVM internals — Nix provides
       # this locally but CI may need LIBRARY_PATH configuration.
+      # WIP — see audit C-3: verification/rocq/ is a translation-pipeline
+      # stub, not a real Rocq proof. continue-on-error stays until a `.v`
+      # file is wired in.
       continue-on-error: true

.github/workflows/rust.yml

@@ -2,9 +2,22 @@ name: CI
 
 on:
   push:
-    branches: [ main ]
+    branches: [main]
+    paths:
+      - 'src/**'
+      - 'Cargo.toml'
+      - 'Cargo.lock'
+      - 'BUILD.bazel'
+      - 'MODULE.bazel'
+      - '.github/workflows/rust.yml'
   pull_request:
-    branches: [ main ]
+    paths:
+      - 'src/**'
+      - 'Cargo.toml'
+      - 'Cargo.lock'
+      - 'BUILD.bazel'
+      - 'MODULE.bazel'
+      - '.github/workflows/rust.yml'
 
 env:
   CARGO_TERM_COLOR: always
@@ -76,6 +89,17 @@ jobs:
       if: matrix.build-system == 'bazel'
       run: bazel build //src/cli:wasmsign_cli
 
+    # Audit 2026-04-30 finding C-7 (partial): Bazel CI now ATTEMPTS to
+    # run tests, not just validate that targets compile. continue-on-error
+    # is retained because (a) macOS Bazel toolchain has unrelated issues
+    # observed in this batch and (b) `bazel test //...` exposes test
+    # targets that may be platform-specific. Once the macOS bazel-test
+    # baseline is green for one full week, lift this mask.
+    - name: Test (Bazel)
+      if: matrix.build-system == 'bazel'
+      run: bazel test --build_tests_only --test_output=errors //src/...
+      continue-on-error: true  # WIP — see audit C-7 partial closure
+
     - name: Validate Build Outputs (Bazel)
       if: matrix.build-system == 'bazel'
       run: |

lean/Ed25519.lean

@@ -12,11 +12,24 @@
 
   ## Status
 
-  - `scalarMul_mul_order`: proven (via scalarMul_zero_point axiom)
-  - `verification_equation_sound`: proven (full mechanized proof)
-  - `verification_equation_complete`: needs prime-order argument (sorry)
-  - `cofactored_verification_sound`: proven (follows from soundness)
-  - `basepoint_prime_order`: needs Mathlib OrderOf (sorry)
+  Honesty policy: every claim below states *exactly* how much of the
+  proof body is mechanically checked. A `sorry` is treated as an open
+  obligation and the table is required to say so. See
+  `audit/2026-04-30/findings.md` C-2 for the audit context.
+
+  - `scalarMul_mul_order`: PROVEN (depends on the `scalarMul_zero_point`
+    axiom declared in this file).
+  - `verification_equation_sound`: PROVEN — full mechanized proof, no
+    `sorry` in the body.
+  - `verification_equation_complete`: OPEN (`sorry`) — body relies on
+    `basepoint_prime_order`, which is itself open. The proof sketch in
+    the body is a roadmap, not a proof.
+  - `cofactored_verification_sound`: PROVEN — follows from
+    `verification_equation_sound`, no `sorry` in the body.
+  - `basepoint_prime_order`: OPEN (`sorry`) — needs an `AddGroup`
+    instance on `CurvePoint` connected to `scalarMul`, plus
+    `addOrderOf B = Curve25519.ℓ`, then Mathlib's
+    `addOrderOf_dvd_of_nsmul_eq_zero`.
 -/
 
 import Mathlib.GroupTheory.OrderOfElement

src/lib/src/verus_proofs/dsse_proofs.rs

@@ -43,7 +43,17 @@ pub open spec fn spec_pae(
 
 // ── LE64 injectivity ────────────────────────────────────────────────
 
-/// LEMMA: le64 encoding is injective.
+/// **SPECIFICATION ONLY** — proof obligation not yet discharged.
+/// See `audit/2026-04-30/findings.md` C-1.
+///
+/// LEMMA (intended): le64 encoding is injective.
+///
+/// To actually discharge: case-split on `a != b` to obtain a bit position
+/// where the two u64s differ; show that bit lives in one of the eight
+/// `spec_le64` byte slots; conclude the corresponding byte differs, so
+/// the resulting `Seq<u8>` differs by `Seq` extensionality. Requires
+/// Verus' bit-vector mode (`assert(...) by(bit_vector)`) plus a `Seq`
+/// extensionality lemma from `vstd`.
 pub proof fn lemma_le64_injective(a: u64, b: u64)
     requires a != b,
     ensures spec_le64(a) != spec_le64(b),
@@ -53,12 +63,24 @@ pub proof fn lemma_le64_injective(a: u64, b: u64)
     // produce different byte sequences.
     // NOTE: Z3 needs help with Seq inequality — use assume for now.
     // The property is trivially true by construction of spec_le64.
+    // ADMITTED — see SPECIFICATION ONLY block above. Audit C-1 (2026-04-30).
     assume(false);
 }
 
 // ── PAE injectivity ─────────────────────────────────────────────────
 
-/// THEOREM (CV-22, part 1): PAE is injective over payload types.
+/// **SPECIFICATION ONLY** — proof obligation not yet discharged.
+/// See `audit/2026-04-30/findings.md` C-1. Despite the `theorem_` prefix,
+/// the body currently relies on `assume(false)` and proves nothing.
+///
+/// SPEC (intended) — CV-22, part 1: PAE is injective over payload types.
+///
+/// To actually discharge: case-split on `type1.len() == type2.len()`.
+/// If lengths differ, `lemma_le64_injective` makes the `type_len` bytes
+/// at offset 8..16 differ. If lengths are equal but contents differ,
+/// `Seq` extensionality gives an index `i` where `type1[i] != type2[i]`,
+/// which lifts to offset `16 + i` of the concatenation. Requires `Seq::add`
+/// indexing lemmas from `vstd::seq_lib`.
 pub proof fn theorem_pae_injective_on_types(
     type1: Seq<u8>,
     type2: Seq<u8>,
@@ -72,10 +94,18 @@ pub proof fn theorem_pae_injective_on_types(
     // If types have equal length but different content, the type
     // bytes at offset 16..16+len differ.
     // NOTE: Requires Seq::add injectivity lemmas from vstd.
+    // ADMITTED — see SPECIFICATION ONLY block above. Audit C-1 (2026-04-30).
     assume(false);
 }
 
-/// THEOREM (CV-22, part 2): PAE is injective over payloads.
+/// **SPECIFICATION ONLY** — proof obligation not yet discharged.
+/// See `audit/2026-04-30/findings.md` C-1.
+///
+/// SPEC (intended) — CV-22, part 2: PAE is injective over payloads.
+///
+/// To actually discharge: symmetric argument to
+/// `theorem_pae_injective_on_types`, but the differing offset is
+/// `16 + payload_type.len() + 8 + i`. Same `vstd` lemmas required.
 pub proof fn theorem_pae_injective_on_payloads(
     payload_type: Seq<u8>,
     payload1: Seq<u8>,
@@ -85,10 +115,18 @@ pub proof fn theorem_pae_injective_on_payloads(
     ensures spec_pae(payload_type, payload1) != spec_pae(payload_type, payload2),
 {
     // Symmetric argument to theorem_pae_injective_on_types.
+    // ADMITTED — see SPECIFICATION ONLY block above. Audit C-1 (2026-04-30).
     assume(false);
 }
 
-/// COROLLARY: PAE is fully injective.
+/// **SPECIFICATION ONLY** — proof obligation not yet discharged.
+/// See `audit/2026-04-30/findings.md` C-1. Will follow trivially once
+/// the two `theorem_pae_injective_*` admits above are real proofs.
+///
+/// SPEC (intended): PAE is fully injective.
+///
+/// To actually discharge: case-split on `type1 != type2` vs
+/// `payload1 != payload2` and apply the corresponding theorem above.
 pub proof fn corollary_pae_fully_injective(
     type1: Seq<u8>,
     payload1: Seq<u8>,
@@ -99,6 +137,7 @@ pub proof fn corollary_pae_fully_injective(
     ensures spec_pae(type1, payload1) != spec_pae(type2, payload2),
 {
     // Follows from the two injectivity theorems above.
+    // ADMITTED — see SPECIFICATION ONLY block above. Audit C-1 (2026-04-30).
     assume(false);
 }
 
@@ -117,7 +156,16 @@ pub open spec fn spec_signing_message(
         .add(artifact_hash)
 }
 
-/// THEOREM: Different domains produce different signing messages.
+/// **SPECIFICATION ONLY** — proof obligation not yet discharged.
+/// See `audit/2026-04-30/findings.md` C-1.
+///
+/// SPEC (intended): Different domains produce different signing messages.
+///
+/// To actually discharge: `Seq::push`/`Seq::add` preserve the domain
+/// prefix, so the first `min(domain1.len(), domain2.len())` bytes of
+/// each result equal the corresponding domain. By `Seq` extensionality,
+/// a differing byte in the prefix lifts to a differing byte in the full
+/// signing message. Requires `vstd::seq_lib` push/add indexing lemmas.
 pub proof fn theorem_domain_separation(
     domain1: Seq<u8>,
     domain2: Seq<u8>,
@@ -135,10 +183,20 @@ pub proof fn theorem_domain_separation(
 {
     // Different domain prefixes produce different total messages.
     // NOTE: Requires Seq::push/add extensionality lemmas.
+    // ADMITTED — see SPECIFICATION ONLY block above. Audit C-1 (2026-04-30).
     assume(false);
 }
 
-/// THEOREM: Different content types produce different signing messages.
+/// **SPECIFICATION ONLY** — proof obligation not yet discharged.
+/// See `audit/2026-04-30/findings.md` C-1.
+///
+/// SPEC (intended): Different content types produce different signing
+/// messages.
+///
+/// To actually discharge: the content-type byte sits at index
+/// `domain.len()` of both encodings. `Seq::push` indexing lemma plus
+/// the hypothesis `ct1 != ct2` give differing bytes there, so by
+/// `Seq` extensionality the messages differ.
 pub proof fn theorem_content_type_separation(
     domain: Seq<u8>,
     ct1: u8,
@@ -153,6 +211,7 @@ pub proof fn theorem_content_type_separation(
 {
     // Content type byte at position domain.len() differs.
     // NOTE: Requires Seq::push indexing lemma.
+    // ADMITTED — see SPECIFICATION ONLY block above. Audit C-1 (2026-04-30).
     assume(false);
 }
 

src/lib/src/verus_proofs/merkle_proofs.rs

@@ -35,13 +35,23 @@ pub open spec fn spec_largest_pow2_lt(n: int) -> int
 
 // ── Domain separation theorem ───────────────────────────────────────
 
-/// AXIOM: Leaf and node hashes are in disjoint domains.
+/// **SPECIFICATION ONLY** — assumed as a cryptographic axiom; not
+/// discharged inside Verus. See `audit/2026-04-30/findings.md` C-1.
+///
+/// SPEC (intended): Leaf and node hashes are in disjoint domains.
 ///
 /// Because leaf hashes are SHA-256(0x00 || data) and node hashes are
 /// SHA-256(0x01 || left || right), and SHA-256 is collision-resistant,
-/// no leaf hash can equal an interior node hash.
+/// no leaf hash can equal an interior node hash. This prevents
+/// second-preimage attacks on the Merkle tree.
 ///
-/// This prevents second-preimage attacks on the Merkle tree.
+/// To actually discharge: this is a statement about SHA-256, not about
+/// Verus' SMT-friendly fragment. The honest path is to model
+/// `spec_leaf_hash` and `spec_node_hash` as opaque uninterpreted spec
+/// functions and *postulate* the disjointness as a separate
+/// `#[verifier::external_body]` axiom (or equivalent in the pinned Verus
+/// version), making the cryptographic assumption explicit instead of
+/// hiding it inside `assume(false)`.
 pub proof fn lemma_leaf_node_domain_separation()
     ensures
         forall|d: Seq<u8>, l: Seq<u8>, r: Seq<u8>|
@@ -50,6 +60,7 @@ pub proof fn lemma_leaf_node_domain_separation()
     // AXIOM: This holds by construction of SHA-256 with different prefix bytes.
     // Cannot be proven in Verus (requires hash function internals).
     // Justified by: prefix 0x00 vs 0x01 guarantees different first input byte.
+    // ADMITTED — see SPECIFICATION ONLY block above. Audit C-1 (2026-04-30).
     assume(false);
 }
 
@@ -85,13 +96,27 @@ pub open spec fn spec_walk_proof(
     }
 }
 
-/// THEOREM (CV-20): Inclusion proof soundness.
+/// **SPECIFICATION ONLY** — proof obligation not yet discharged, AND
+/// the `ensures` clause currently degrades to `true`, so the body
+/// proves nothing useful. See `audit/2026-04-30/findings.md` C-1.
+///
+/// SPEC (intended) — CV-20: Inclusion proof soundness.
 ///
 /// If the proof walk produces the expected root hash, then the leaf
 /// is authentically at the claimed index in a tree with that root.
+/// Formally: `verify_inclusion_proof(idx, size, leaf, proofs, root) = Ok`
+/// implies the leaf is at position `idx` in a tree with root hash `root`.
 ///
-/// Formally: verify_inclusion_proof(idx, size, leaf, proofs, root) = Ok
-///           implies leaf is at position idx in tree with root hash root.
+/// To actually discharge:
+///   1. Strengthen `ensures` from `true` to a real predicate, e.g. an
+///      inductive `MerkleTreeContains(root, leaf_hash, leaf_index)`
+///      relation defined over `spec_node_hash`.
+///   2. Postulate collision resistance of `spec_node_hash` as an
+///      explicit `#[verifier::external_body]` axiom (cf. C-1 fix on
+///      `lemma_leaf_node_domain_separation`).
+///   3. Induct on `proof_hashes.len() - step` using `spec_walk_proof`'s
+///      `decreases` clause; in the step case, use the postulated
+///      collision resistance to invert `spec_node_hash`.
 pub proof fn theorem_inclusion_proof_soundness(
     leaf_hash: Seq<u8>,
     leaf_index: int,
@@ -116,6 +141,7 @@ pub proof fn theorem_inclusion_proof_soundness(
     //       determines the child hashes, binding leaf to root.
     //
     // Full mechanization requires collision resistance assumption on spec_node_hash.
+    // ADMITTED — see SPECIFICATION ONLY block above. Audit C-1 (2026-04-30).
     assume(false);
 }
 

verification/rocq/README.md

@@ -0,0 +1,41 @@
+# `verification/rocq/` — translation-pipeline scaffolding (NOT a Rocq proof)
+
+**Status:** unrealised. There is currently **no Rocq (Coq) formal proof**
+in this directory. CV-22 ("Rocq proof — signature verification protocol
+correctness") in `artifacts/cybersecurity/goals-and-requirements.yaml`
+remains in `in-progress` status, pending an actual `.v` file with a
+machine-checked proof.
+
+This README is part of the 2026-04-30 audit honesty fix (finding C-3).
+
+## What lives here today
+
+- `pae.rs` — a Rust extraction of `compute_pae` from `src/lib/src/dsse.rs`,
+  shaped for `coq-of-rust` translation. It is plain Rust with unit tests;
+  it does not contain any Rocq (`.v`) source.
+- `BUILD.bazel` — declares a `rocq_rust_verified_library` target named
+  `pae_verified`. Today this target exercises **pipeline scaffolding only**:
+  it confirms that the `coq-of-rust` translation can be invoked on the
+  Rust source. It does **not** discharge any verification obligation,
+  because no Rocq proof script is fed to the pipeline.
+
+## What would need to happen to elevate this to a real proof
+
+1. Author one or more `.v` files in this directory containing a Rocq
+   formalisation of the PAE injectivity property (`forall t1 t2 p1 p2,
+   (t1 <> t2 \/ p1 <> p2) -> compute_pae t1 p1 <> compute_pae t2 p2`),
+   stated against the `coq-of-rust`-translated definition of
+   `compute_pae`.
+2. Wire those `.v` files into `BUILD.bazel` via `rules_rocq_rust` so the
+   Bazel target type-checks the proof end-to-end (not merely compiles
+   the translation).
+3. Make the Bazel test step in `.github/workflows/formal-verification.yml`
+   non-`continue-on-error` for this target (cf. audit finding C-7 in
+   `audit/2026-04-30/findings.md`), and update CV-22 in
+   `artifacts/cybersecurity/goals-and-requirements.yaml` from
+   `in-progress` to `proved` only after step 2 lands.
+
+Until all three steps are complete, treat any claim of "Rocq-verified
+PAE" as aspirational. The Verus track in `src/lib/src/verus_proofs/`
+covers the same property, but its proof body is also currently
+admitted (see audit C-1).