Add Lean (Aeneas) extraction of the crypto core

securedrop-protocol/Cargo.toml

@@ -22,4 +22,4 @@ license = "GPL-3.0"
 # `cfg(hax_backend_proverif)` is set only by hax during `cargo hax into proverif`
 # (it gates the ProVerif-specific annotations). Normal builds, `cargo test`, and
 # `into fstar` never set it, so those lanes strip the gated annotations entirely.
-unexpected_cfgs = { level = "warn", check-cfg = ["cfg(hax)", "cfg(hax_backend_proverif)"] }
+unexpected_cfgs = { level = "warn", check-cfg = ["cfg(hax)", "cfg(hax_backend_proverif)", "cfg(hax_backend_lean)"] }

securedrop-protocol/protocol-minimal/proofs/aeneas-lean/.gitignore

@@ -0,0 +1,3 @@
+# Generated diagnostics — not part of the committed Lean snapshot.
+llbc/
+aeneas-error.log

securedrop-protocol/protocol-minimal/proofs/aeneas-lean/README.md

@@ -0,0 +1,53 @@
+# Lean (Aeneas) extraction of the crypto core
+
+A functional-model extraction of `securedrop-protocol-minimal`'s cryptographic core
+to **Lean 4**, via the hax **aeneas-lean** backend (`rustc → charon → aeneas`). This
+complements the F\* extraction (`proofs/fstar/`) and the ProVerif symbolic model
+(`proofs/proverif/`) with a third, independent lifting of the same Rust.
+
+## What is extracted
+
+The driver mirrors the ProVerif target set — the loop-free SD-APKE / SD-PKE / Ed25519
+core and the envelope operations:
+
+| Module | Functions (translated to Lean `def`) |
+|---|---|
+| `message`  | `auth_enc`, `auth_dec` (SD-APKE), keygen, ciphertext/key types |
+| `metadata` | `encrypt`, `decrypt` (SD-PKE), keygen, ciphertext types |
+| `sign`     | Ed25519 `sign` / `verify` |
+| `encrypt_decrypt` | `encrypt`, `decrypt` (envelope build / open) |
+
+Aeneas cannot yet translate a few constructs; these are made opaque **for the Lean
+backend only** via `#[cfg_attr(hax_backend_lean, hax_lib::opaque)]` (F\* and normal
+builds are unaffected), and appear as `axiom`s in `Extraction/FunsExternal_Template.lean`:
+
+| Item | Why opaque | Upstream |
+|---|---|---|
+| `sign::DomainTag::tag` | returns `&'static [u8]` (promoted literal) → "no bottoms in the value" | [AeneasVerif/aeneas#392](https://github.com/AeneasVerif/aeneas/issues/392) |
+| `sign::tagged_preimage` | builds the preimage from the opaque tag with `Vec` ops | (same) |
+| `encrypt_decrypt::decrypt_with_sender` | trial-decrypt loop over `Vec<&MessageKeyBundle>` (iterator + nested borrows) | [AeneasVerif/aeneas#464](https://github.com/AeneasVerif/aeneas/issues/464) |
+
+## Running
+
+```sh
+python3 proofs/proverif/hax.py extract-lean
+```
+
+Output lands in `SecuredropProtocolMinimal/Extraction/*.lean` (committed as a snapshot);
+`llbc/` and `aeneas-error.log` are diagnostics and git-ignored.
+
+## Toolchain (pending upstream)
+
+The lane depends on two hax changes, injected at extraction time so the committed
+manifest stays on crates.io `hax-lib 0.3.7`:
+
+- **[cryspen/hax#2069](https://github.com/cryspen/hax/pull/2069)** — `into aeneas-lean`
+  sets target-side `--cfg hax` so `cfg(hax)`-gated dependencies (libcrux) compile.
+- **[cryspen/hax#2071](https://github.com/cryspen/hax/pull/2071)** — `hax_lib::opaque` /
+  `hax_lib::exclude` emit charon's native `charon::opaque` / `charon::exclude`, so the
+  `#[cfg_attr(hax_backend_lean, …)]` markers above take effect.
+
+Point `HAX_LEAN_DIR` (default `~/hax`) at a hax checkout carrying both; `hax.py
+extract-lean` uses its `cargo-hax` and injects its `hax-lib` via a temporary
+`[patch.crates-io]`. Pinned tool versions (charon `0.1.218`, aeneas
+`nightly-2026.07.01`, Lean `v4.30.0-rc2`) come from hax's `pins.toml`.

securedrop-protocol/protocol-minimal/proofs/aeneas-lean/SecuredropProtocolMinimal.lean

@@ -0,0 +1 @@
+import SecuredropProtocolMinimal.Extraction.Funs

securedrop-protocol/protocol-minimal/proofs/aeneas-lean/SecuredropProtocolMinimal/Extraction/TypesExternal_Template.lean

@@ -0,0 +1,67 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [securedrop_protocol_minimal]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
+import Aeneas
+open Aeneas Aeneas.Std Result ControlFlow Error
+open Std.Do
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
+set_option maxHeartbeats 1000000
+
+/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
+set_option maxRecDepth 2048
+
+/-- [anyhow::Error]
+    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.103/src/lib.rs', lines 390:0-390:16
+    Name pattern: [anyhow::Error]
+    Visibility: public -/
+@[rust_type "anyhow::Error"]
+axiom anyhow.Error : Type
+
+/-- [hpke_rs::HpkePublicKey]
+    Source: '/cargo/git/checkouts/hpke-rs-96cbacf2e1039d85/634caf8/src/lib.rs', lines 214:0-214:24
+    Name pattern: [hpke_rs::HpkePublicKey]
+    Visibility: public -/
+@[rust_type "hpke_rs::HpkePublicKey"]
+axiom hpke_rs.HpkePublicKey : Type
+
+/-- [hpke_rs::HpkePrivateKey]
+    Source: '/cargo/git/checkouts/hpke-rs-96cbacf2e1039d85/634caf8/src/lib.rs', lines 231:0-231:25
+    Name pattern: [hpke_rs::HpkePrivateKey]
+    Visibility: public -/
+@[rust_type "hpke_rs::HpkePrivateKey"]
+axiom hpke_rs.HpkePrivateKey : Type
+
+/-- [hpke_rs::Hpke]
+    Source: '/cargo/git/checkouts/hpke-rs-96cbacf2e1039d85/634caf8/src/lib.rs', lines 460:0-460:45
+    Name pattern: [hpke_rs::Hpke]
+    Visibility: public -/
+@[rust_type "hpke_rs::Hpke"]
+axiom hpke_rs.Hpke (Crypto : Type) (Clause0_HpkePrng : Type)
+  (Clause0_Clause3_Clause1_Clause0_Error : Type) (Clause0_Clause4_Error : Type)
+  : Type
+
+/-- [hpke_rs_libcrux::HpkeLibcruxPrng]
+    Source: '/cargo/git/checkouts/hpke-rs-96cbacf2e1039d85/634caf8/libcrux_provider/src/lib.rs', lines 34:0-34:26
+    Name pattern: [hpke_rs_libcrux::HpkeLibcruxPrng]
+    Visibility: public -/
+@[rust_type "hpke_rs_libcrux::HpkeLibcruxPrng"]
+axiom hpke_rs_libcrux.HpkeLibcruxPrng : Type
+
+/-- [libcrux_ml_kem::types::MlKemPrivateKey]
+    Source: '/cargo/git/checkouts/libcrux-b8e0ded9ad9366a7/3cd1843/libcrux-ml-kem/src/types.rs', lines 5:8-7:9
+    Name pattern: [libcrux_ml_kem::types::MlKemPrivateKey]
+    Visibility: public -/
+@[rust_type "libcrux_ml_kem::types::MlKemPrivateKey"]
+axiom libcrux_ml_kem.types.MlKemPrivateKey (SIZE : Std.Usize) : Type
+
+/-- [libcrux_ml_kem::types::MlKemPublicKey]
+    Source: '/cargo/git/checkouts/libcrux-b8e0ded9ad9366a7/3cd1843/libcrux-ml-kem/src/types.rs', lines 5:8-7:9
+    Name pattern: [libcrux_ml_kem::types::MlKemPublicKey]
+    Visibility: public -/
+@[rust_type "libcrux_ml_kem::types::MlKemPublicKey"]
+axiom libcrux_ml_kem.types.MlKemPublicKey (SIZE : Std.Usize) : Type
+

securedrop-protocol/protocol-minimal/proofs/aeneas-lean/lakefile.toml

@@ -0,0 +1,17 @@
+name = "SecuredropProtocolMinimal"
+version = "0.1.0"
+defaultTargets = ["SecuredropProtocolMinimal"]
+
+[[lean_lib]]
+name = "SecuredropProtocolMinimal"
+
+[[require]]
+name = "aeneas"
+git = "https://github.com/cryspen/aeneas"
+rev = "e0a1596"
+subDir = "backends/lean"
+
+[[require]]
+name = "Hax"
+git = { url = "https://github.com/cryspen/hax-lean" }
+rev = "v0.1.0"

securedrop-protocol/protocol-minimal/proofs/aeneas-lean/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.30.0-rc2

securedrop-protocol/protocol-minimal/proofs/proverif/hax.py

@@ -5,6 +5,11 @@
 
   extract-proverif   `cargo hax into -i '<targets>' proverif` -> extraction/lib.pvl
                      (injects the dev hax-lib via `cargo --config`; restores Cargo.lock)
+  extract-lean       `cargo hax into aeneas-lean` (charon + aeneas) -> a Lean
+                     project under ../aeneas-lean/ for the crypto core. Needs a hax
+                     checkout w/ cryspen/hax#2069 + #2071 (HAX_LEAN_DIR, default ~/hax):
+                     uses its cargo-hax and injects its hax-lib via a temporary
+                     [patch.crates-io] (Cargo.toml/lock restored afterwards).
   verify-proverif    run ProVerif on queries/*.pv, print RESULT lines
   check-proverif     run ProVerif and assert each query's (* EXPECTPV ... END *) block
                      `check-proverif update` regenerates those blocks
@@ -31,6 +36,35 @@
 QUERIES = os.path.join(HERE, "queries")
 LIB_SHA = os.path.join(GEN, "lib.pvl.sha256")
 
+# Aeneas/Lean lane. hax's aeneas-lean backend (charon + aeneas) writes a whole Lean
+# project under <crate>/proofs/aeneas-lean/. Two hax changes are needed and injected at
+# extraction time (pending upstream), so the committed manifest stays on crates.io
+# hax-lib 0.3.7:
+#   * cryspen/hax#2069 (cargo-hax): target-side `--cfg hax` so cfg(hax)-gated deps
+#     (libcrux et al.) compile under charon.
+#   * cryspen/hax#2071 (hax-lib + cargo-hax): `hax_lib::opaque`/`exclude` emit charon's
+#     native attributes, so `#[cfg_attr(hax_backend_lean, hax_lib::opaque)]` markers work.
+# HAX_LEAN_DIR (default ~/hax) is a hax checkout carrying both: its `target/{release,
+# debug}/cargo-hax` is used, and its hax-lib is injected via a temporary
+# [patch.crates-io] (charon does not honor hax's `-C` config, so we patch the manifest).
+LEAN_DIR = os.path.normpath(os.path.join(CRATE, "proofs", "aeneas-lean"))
+WS = os.path.normpath(os.path.join(CRATE, ".."))   # workspace root (holds Cargo.toml/lock)
+HAX_LEAN_DIR = os.environ.get("HAX_LEAN_DIR", os.path.expanduser("~/hax"))
+
+# Crypto core to extract, mirroring the ProVerif targets: SD-APKE (message), SD-PKE
+# (metadata), Ed25519 domain-separated signing (sign), and envelope encrypt/decrypt.
+# charon translates each item's transitive closure; aeneas-hostile helpers inside it
+# (the `&'static` domain tags, the trial-decryption loop) carry
+# `#[cfg_attr(hax_backend_lean, hax_lib::opaque)]`. `--charon-args` overrides this.
+LEAN_START_FROM = [
+    "securedrop_protocol_minimal::message",
+    "securedrop_protocol_minimal::metadata",
+    "securedrop_protocol_minimal::sign",
+    "securedrop_protocol_minimal::encrypt_decrypt::encrypt",
+    "securedrop_protocol_minimal::encrypt_decrypt::decrypt",
+    "securedrop_protocol_minimal::encrypt_decrypt::decrypt_with_sender",
+]
+
 HAX_PROVERIF_DIR = os.environ.get(
     "HAX_PROVERIF_DIR", os.path.expanduser("~/hax-proverif-backend")
 )
@@ -149,6 +183,79 @@ def cmd_extract(args):
     return rc
 
 
+def _inject_hax_lib_patch():
+    """Add a temporary [patch.crates-io] to the workspace manifest pointing hax-lib at
+    HAX_LEAN_DIR, so charon compiles against the dev hax-lib (charon ignores hax's `-C`
+    config, so unlike the ProVerif lane we patch the manifest). Returns {path: original}
+    backups (Cargo.toml + Cargo.lock) for the caller to restore; empty if already patched."""
+    lib = os.path.join(HAX_LEAN_DIR, "hax-lib")
+    entries = (
+        'hax-lib = {{ path = "{0}" }}\n'
+        'hax-lib-macros = {{ path = "{0}/macros" }}\n'
+        'hax-lib-macros-types = {{ path = "{0}/macros/types" }}\n'
+    ).format(lib)
+    ws_toml = os.path.join(WS, "Cargo.toml")
+    ws_lock = os.path.join(WS, "Cargo.lock")
+    backups = {p: open(p).read() for p in (ws_toml, ws_lock) if os.path.exists(p)}
+    text = backups.get(ws_toml, "")
+    if "hax-lib = { path" in text:
+        return {}  # already patched (e.g. re-entrant); leave as-is
+    marker = "[patch.crates-io]\n"
+    text = text.replace(marker, marker + entries, 1) if marker in text \
+        else text + "\n" + marker + entries
+    with open(ws_toml, "w") as f:
+        f.write(text)
+    return backups
+
+
+def cmd_extract_lean(args):
+    """Aeneas/Lean lane: `cargo hax into aeneas-lean` runs charon then aeneas to lift the
+    Rust into a Lean project under ../aeneas-lean/. Extracts the crypto-core closure
+    (LEAN_START_FROM); aeneas-hostile helpers are gated opaque via
+    `#[cfg_attr(hax_backend_lean, hax_lib::opaque)]`. Needs a hax checkout with
+    cryspen/hax#2069 + #2071 (HAX_LEAN_DIR): its cargo-hax is put on PATH and its hax-lib
+    injected as a temporary [patch.crates-io] (Cargo.toml/lock restored afterwards)."""
+    env = dict(os.environ)
+    # Put HAX_LEAN_DIR's cargo-hax on PATH — the most recently built of release/debug,
+    # so a stale build in the other profile can't shadow a fresh one.
+    cands = [os.path.join(HAX_LEAN_DIR, "target", s, "cargo-hax") for s in ("release", "debug")]
+    cands = [c for c in cands if os.path.exists(c)]
+    if cands:
+        newest = max(cands, key=os.path.getmtime)
+        env["PATH"] = os.path.dirname(newest) + os.pathsep + env.get("PATH", "")
+    charon = args.charon_args or " ".join("--start-from " + t for t in LEAN_START_FROM)
+    cmd = ["cargo", "hax", "into", "aeneas-lean"]
+    if not args.no_lakefile:
+        # Idempotent: scaffolds lakefile.toml + lean-toolchain, never overwriting edits.
+        cmd += ["--lakefile"]
+    # `--flag=value` form: values start with `--` (`--start-from ...`), which the
+    # space-separated form would mis-parse as new flags.
+    cmd += ["--charon-args=" + charon]
+    if args.aeneas_args:
+        cmd += ["--aeneas-args=" + args.aeneas_args]
+    backups = _inject_hax_lib_patch()
+    try:
+        rc = subprocess.run(cmd, cwd=CRATE, env=env).returncode
+    finally:
+        for p, data in backups.items():
+            with open(p, "w") as f:
+                f.write(data)
+    # Report the .lean files aeneas produced (nested under a Lean-package dir).
+    leans = sorted(
+        os.path.relpath(os.path.join(root, f), LEAN_DIR)
+        for root, _dirs, files in os.walk(LEAN_DIR)
+        for f in files if f.endswith(".lean")
+    )
+    where = os.path.relpath(LEAN_DIR, HERE)
+    if leans:
+        print("\n== aeneas-lean: {} .lean file(s) under {} ==".format(len(leans), where))
+        for f in leans:
+            print("  " + f)
+    else:
+        print("\n== aeneas-lean: no .lean produced under {} (see errors above) ==".format(where))
+    return rc
+
+
 # Names of symbols the extracted model references but that are DEFINED by our
 # hand-written libs (sd_crypto.pvl, sd_model.pvl). hax can't see those definitions,
 # so it lists them in missingdecl.pvl; leaving them there would double-declare the
@@ -332,6 +439,15 @@ def main():
     e.add_argument("--include", help="override the -i target filter")
     e.set_defaults(func=cmd_extract)
 
+    ln = sub.add_parser("extract-lean",
+                        help="cargo hax into aeneas-lean -> Lean project under ../aeneas-lean/")
+    ln.add_argument("--no-lakefile", action="store_true",
+                    help="don't scaffold lakefile.toml / lean-toolchain in ../aeneas-lean/")
+    ln.add_argument("--charon-args",
+                    help="override the default crypto-core --start-from set (shell-quoted)")
+    ln.add_argument("--aeneas-args", help="extra args forwarded to aeneas (shell-quoted)")
+    ln.set_defaults(func=cmd_extract_lean)
+
     r = sub.add_parser("reconstruct-proverif",
                        help="engine-free: verify the committed lib.pvl snapshot digest")
     r.set_defaults(func=cmd_reconstruct)

securedrop-protocol/protocol-minimal/src/encrypt_decrypt.rs

@@ -78,6 +78,11 @@ pub fn decrypt<U: UserSecret + ?Sized>(receiver: &U, envelope: &Envelope) -> Pla
 /// Decrypt like [`decrypt`], additionally returning the sender's long-term
 /// SD-APKE public key `pk_S^APKE` recovered from `ct^PKE`.
 #[cfg_attr(hax, hax_lib::fstar::verification_status(lax))]
+// The trial-decryption loop iterates a `Vec<&MessageKeyBundle>`, which aeneas/charon
+// can't translate (iterator + nested borrows, AeneasVerif/aeneas#464). This is
+// protocol dispatch rather than a crypto primitive, so make it opaque for the Lean
+// backend only; F* and normal builds are unaffected.
+#[cfg_attr(hax_backend_lean, hax_lib::opaque)]
 pub fn decrypt_with_sender<U: UserSecret + ?Sized>(
     receiver: &U,
     envelope: &Envelope,

securedrop-protocol/protocol-minimal/src/sign.rs

@@ -58,21 +58,28 @@ mod sealed_impls {
 }
 
 impl DomainTag for JournalistLongTermKey {
+    // aeneas/charon can't represent the `&'static [u8]` promoted literal ("no bottoms
+    // in the value"); the tag is a constant, so make it opaque for the Lean backend
+    // only. F* and normal builds are unaffected. See AeneasVerif/aeneas#392.
+    #[cfg_attr(hax_backend_lean, hax_lib::opaque)]
     fn tag() -> &'static [u8] {
         b"j-sig-ltk"
     }
 }
 impl DomainTag for JournalistEphemeralKey {
+    #[cfg_attr(hax_backend_lean, hax_lib::opaque)]
     fn tag() -> &'static [u8] {
         b"j-sig-eph"
     }
 }
 impl DomainTag for NewsroomOnJournalist {
+    #[cfg_attr(hax_backend_lean, hax_lib::opaque)]
     fn tag() -> &'static [u8] {
         b"nr-sig"
     }
 }
 impl DomainTag for FpfOnNewsroom {
+    #[cfg_attr(hax_backend_lean, hax_lib::opaque)]
     fn tag() -> &'static [u8] {
         b"fpf-sig-nr"
     }
@@ -154,6 +161,9 @@ impl<'de, D: DomainTag> serde::Deserialize<'de> for Signature<D> {
 
 /// Construct the tagged signing preimage: `len(tag) || tag || msg`.
 #[cfg_attr(hax, hax_lib::fstar::verification_status(lax))]
+// Builds the preimage from the opaque `&'static` domain tag with `Vec` ops aeneas
+// can't translate; it's domain-separation plumbing, so make it opaque for Lean only.
+#[cfg_attr(hax_backend_lean, hax_lib::opaque)]
 fn tagged_preimage<D: DomainTag>(msg: &[u8]) -> Vec<u8> {
     let tag = D::tag();
     #[cfg(not(hax))]