Sprint 1.1.D.2.c — Creusot contracts on HMAC + HKDF + Argon2id - #414
Open
LennyObez wants to merge 1 commit into
Open
Sprint 1.1.D.2.c — Creusot contracts on HMAC + HKDF + Argon2id#414LennyObez wants to merge 1 commit into
LennyObez wants to merge 1 commit into
Conversation
Third micro-slice of Phase 1.1.D.2. Extends the View + spec-ghost-
function pattern from 1.1.D.2.b across the remaining keyed-hashing
and KDF surfaces. Trust posture concentrated at the FFI and
audited-substrate boundaries; pure-logic paths (parameter validation)
carry proven postconditions.
hmac.rs — full Pearlite contract surface
=========================================
- spec_tag_len(algo) -> Int ghost #[logic(open)] mirroring
spec_digest_len from D.2.b (kept separate because the algorithm
enums are disjoint).
- HmacAlgorithm::tag_len: #[ensures(result@ == spec_tag_len(self))]
- impl View for HmacKey (ViewTy = HmacAlgorithm,
#[trusted] #[logic(opaque)]) — encapsulates private algo field.
- HmacKey::new: #[trusted] +
#[ensures(forall<h> result == Ok(h) ==> h@ == algo)]
- HmacKey::algorithm: #[ensures(result == self@)] bridge
- HmacKey::compute: #[trusted] +
#[ensures(forall<v> result == Ok(v) ==> v@.len() == spec_tag_len(self@))]
- HmacKey::compute_into + verify: #[trusted]
(FFI / subtle::ConstantTimeEq external).
hkdf.rs — #[trusted] at the FFI boundary
=========================================
- extract / expand / hkdf: all #[trusted] with HACL* F* rationale
(ADR-0009). Return type SecretBox<[u8]> is logic-opaque to
Creusot v0.11 — no View / DeepModel impl on secrecy::SecretBox,
so non-trivial postconditions on PRK/OKM byte content require
modelling SecretBox in Pearlite (deferred).
- max_output_len internal helper: no postcondition (cross-module
#[logic(open)] references don't compose on stable rustc; KAT
tests cover the program-side correctness).
argon2.rs — mixed trust posture (audit tier, not F* tier)
==========================================================
Per Decision 2.60 + ADR-0009 ("Argon2id is the only audited-but-
not-formally-verified primitive in the kernel"). State-of-art
empirical assessment (2026Q2): no production-ready F*-verified
Argon2id implementation exists. HACL* doesn't ship Argon2; libcrux
doesn't ship Argon2; Cryspen ecosystem doesn't ship Argon2. State-of-
art for this primitive = best-audited Rust implementation =
RustCrypto argon2.
- Argon2idParams::new: #[ensures] propagating field assignments.
- Argon2idParams::validate: **proven** (NOT #[trusted]) forward-
implication postcondition tying result.is_ok() to all six RFC
9106 § 3.1 admissibility bounds (uses @ to promote u32/usize
fields to Int so `8 * p_cost` is in unbounded arithmetic).
- argon2id_with / derive_key / hash_password /
hash_password_with_random_salt / verify_password /
verify_password_with_limits: #[trusted] with explicit citation of
the *audit-tier* RustCrypto v0.5+ + RFC 9106 + ADR-0009 rationale
(distinct from the F* tier used for HACL*-backed primitives).
Quality gates verified locally
==============================
- cargo fmt --all -- --check ✓
- cargo check -p pulsar-kernel ✓
- cargo clippy -p pulsar-kernel --all-targets -- -D warnings ✓
- cargo nextest run -p pulsar-kernel — 196/196 PASS ✓
- cargo test -p pulsar-kernel --doc ✓
The proof-discharge CI job remains workflow_dispatch-only per Phase
1.1.D.2.b-bis (kernel-wide Creusot v0.11 compatibility constraints
documented inline at the job level). Contracts are aspirational
specifications + future-proofing; macro expansion is no-op on stable
rustc.
Refs: docs/plan.md Section II Decision 2.20 (Creusot + TLA+);
ADR-0015 (Creusot for kernel function contracts); ADR-0009 (HACL* +
Argon2 audit-vs-verification distinction); RFC 2104 (HMAC), RFC 5869
(HKDF), RFC 9106 (Argon2).
There was a problem hiding this comment.
Pull request overview
Adds Phase 1.1.D.2.c Creusot/Pearlite contract surface and trust-boundary annotations across the remaining keyed-hashing and KDF primitives in pulsar-kernel::crypto, extending the existing View + ghost-spec pattern from the hash-family work.
Changes:
- Added
spec_tag_lenghost function and tiedHmacAlgorithm/HmacKeybehavior to it viaViewand#[ensures]postconditions (with#[trusted]at FFI/external boundaries). - Marked HKDF FFI-crossing functions (
extract,expand,hkdf) as#[trusted]with explicit rationale givenSecretBox<[u8]>is logic-opaque. - Added proven postconditions for
Argon2idParams::{new, validate}and marked RustCrypto-backed Argon2id operations as#[trusted], plus updated changelog entry for the sprint.
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
| crates/pulsar-kernel/src/crypto/hmac.rs | Introduces HMAC ghost spec + View model and postconditions; applies #[trusted] at boundary-touching functions. |
| crates/pulsar-kernel/src/crypto/hkdf.rs | Adds #[trusted] at HKDF FFI boundary and documents rationale/limitations due to SecretBox opacity. |
| crates/pulsar-kernel/src/crypto/argon2.rs | Adds postconditions for parameter construction/validation and #[trusted] annotations for RustCrypto Argon2 operations. |
| CHANGELOG.md | Documents Sprint 1.1.D.2.c scope and quality gates. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| /// earlier `p_cost <= 0x00FF_FFFF` guard caps the product at | ||
| /// `0x07FF_FFF8`, but the contract speaks at the semantic level. | ||
| #[ensures( | ||
| result.is_ok() ==> ( |
Comment on lines
+35
to
+37
| The `proof-discharge` CI job remains `workflow_dispatch`-only per Phase 1.1.D.2.b-bis (kernel-wide Creusot v0.11 compatibility constraints documented inline at the job level). Contracts are aspirational specifications + future-proofing; macro expansion is no-op on stable rustc. Section 1.1.D.3 (AEAD + signatures) and 1.1.D.4 (KEM + ML-DSA + hybrids) follow the same pattern. | ||
|
|
||
| Refs: `docs/plan.md` Section II Decision 2.20 (Creusot + TLA+); ADR-0015 (Creusot for kernel function contracts); ADR-0009 (HACL\* + Argon2 audit-vs-verification distinction); RFC 2104 (HMAC), RFC 5869 (HKDF), RFC 9106 (Argon2). |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Third micro-slice of Phase 1.1.D.2. Extends the View + spec-ghost-function pattern from 1.1.D.2.b across the remaining keyed-hashing and KDF surfaces.
What's in
Test plan
Refs