proof: extract a single pattern to start

[cfm]

#131 demonstrated how to integrate hax into our CI for extraction (by hax) and proof (in F*).

Closes #154 by demonstrating how to use hax and F* to prove some property about some function implemented in #164. Per #164 (comment), securedrop_protocol_minimal::primitives::*::typed() seemed to be the lowest-hanging fruit.

At a high level:

securedrop-protocol/securedrop-protocol/protocol-minimal
├── Cargo.toml                                                # hax and libcrux crates updated and pinned
├── Makefile                                                  # "make hax" extracts, type-checks, and checks proofs
├── proofs
│   └── fstar
│       ├── extraction
│       │   ├── hax.fst.config.json
│       │   ├── Makefile
│       │   └── Securedrop_protocol_minimal.Primitives.*.fst  # extracted from securedrop_protocol_minimal::primitives::*::typed() [1]
│       └── libcrux-models                                    # axiom stubs for unverified crates (generated by Claude)
│           ├── Anyhow.Error.fsti
│           ├── Anyhow.fsti
│           └── Libcrux_kem.fsti
├── src
│   ├── api.rs
│   ├── encrypt_decrypt.rs
│   ├── keys
│   │   └── newsroom.rs
│   ├── keys.rs
│   ├── lib.rs
│   ├── messages
│   │   ├── core.rs
│   │   └── setup.rs
│   ├── messages.rs
│   ├── primitives                                             # see preconditions on *::typed()
│   │   ├── dh_akem.rs
│   │   ├── mlkem.rs
│   │   ├── pad.rs
│   │   ├── x25519.rs
│   │   └── xwing.rs
│   ├── primitives.rs
│   ├── server.rs
│   ├── setup.rs
│   ├── sign.rs
│   ├── storage.rs
│   └── types.rs
└── tests
    ├── core.rs
    └── setup.rs

Notes:

1. Committed here for demonstration. In CI these will likely be cleared and extracted fresh on every run, because they should always extract and prove successfully from the Rust source.

[cfm]

cryspen/libcrux#1312 has been merged, so we can revert to specifying a version for these crates once they're released in versions that include it.

[redshiftzero]

LGTM!

I see the wasm build is failing and didn't investigate but good to merge once that's addressed

[cfm]

Thanks, @redshiftzero. That's fixed in c7d4a41.