Skip to main content

axon_frontend/
refinement.rs

1//! Refinement types — `Trusted<T>` / `Untrusted<T>` + closed Trust Catalog.
2//!
3//! §λ-L-E Fase 11.a — Temporal Algebraic Effects + Trust Types.
4//!
5//! Axon's type system tracks a payload's *refinement status* at the
6//! type level. An `Untrusted<T>` value — e.g. an HTTP body, a
7//! WebSocket frame, an OAuth2 redirect code — cannot reach any effect
8//! that consumes `Trusted<T>` unless it first passes through a
9//! verifier registered in [`TRUST_CATALOG`]. Forgetting to verify =
10//! compile-time error emitted by [`crate::type_checker`].
11//!
12//! The catalogue is **closed**: adding a new proof kind requires a
13//! compiler patch + security review, because new verifiers are a
14//! load-bearing security boundary. An adopter who wants to refine
15//! payloads by some custom predicate must contribute the verifier
16//! upstream — not wire their own `verify_hmac` with a non-constant-
17//! time comparison.
18//!
19//! Naming is generic: Axon is adopter-agnostic. These primitives exist
20//! at the language layer and are consumed by any adopter that needs
21//! to validate HMAC-signed webhooks, JWT-bearing requests, OAuth2
22//! code exchanges, or Ed25519-signed detached payloads.
23
24use std::fmt;
25
26// ── Closed catalogue ─────────────────────────────────────────────────
27
28/// Canonical identifiers of the verifiers that can produce a
29/// `Trusted<T>` from an `Untrusted<T>`. Each identifier maps to a
30/// runtime impl in [`crate::trust_verifiers`].
31#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
32pub enum TrustProof {
33    /// HMAC-SHA256 over the raw payload with a shared secret; used for
34    /// webhook signature verification (Stripe, GitHub, generic HMAC).
35    Hmac,
36    /// JWT signature verification (RS256/RS384/RS512) via a JWKS
37    /// endpoint. Shared with Fase 10.e's [`crate::jwt_verifier`].
38    JwtSig,
39    /// OAuth2 authorization-code exchange using PKCE S256. Returns an
40    /// access token proof that the bearer controls the code verifier.
41    OAuthCodeExchange,
42    /// Ed25519 detached signature verification (Sigstore-style).
43    Ed25519,
44}
45
46impl TrustProof {
47    /// Every variant. Keeping this as an explicit slice ensures the
48    /// compiler errors if we add a variant without updating the
49    /// catalogue consumers.
50    pub const ALL: &'static [TrustProof] = &[
51        TrustProof::Hmac,
52        TrustProof::JwtSig,
53        TrustProof::OAuthCodeExchange,
54        TrustProof::Ed25519,
55    ];
56
57    /// Slug used in source text — appears in `#[refines(...)]`
58    /// annotations and in [`crate::type_checker`] diagnostics.
59    pub fn slug(self) -> &'static str {
60        match self {
61            TrustProof::Hmac => "hmac",
62            TrustProof::JwtSig => "jwt_sig",
63            TrustProof::OAuthCodeExchange => "oauth_code_exchange",
64            TrustProof::Ed25519 => "ed25519",
65        }
66    }
67
68    /// Resolve a slug to a proof, returning `None` for unknown
69    /// identifiers. The checker uses this to reject annotations that
70    /// don't map to the closed catalogue.
71    pub fn from_slug(slug: &str) -> Option<TrustProof> {
72        Self::ALL.iter().copied().find(|p| p.slug() == slug)
73    }
74}
75
76impl fmt::Display for TrustProof {
77    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
78        f.write_str(self.slug())
79    }
80}
81
82/// Catalogue lookup for the checker's diagnostic messages.
83///
84/// ```text
85/// error: unknown trust proof 'crc32'. Valid: hmac, jwt_sig, oauth_code_exchange, ed25519
86/// ```
87pub const TRUST_CATALOG: &[&str] = &["hmac", "jwt_sig", "oauth_code_exchange", "ed25519"];
88
89// ── Refinement type names ────────────────────────────────────────────
90
91/// Type constructor names the checker recognises at the AST level.
92/// Both take a single generic parameter (`Trusted<HttpBody>`,
93/// `Untrusted<WsFrame>`). The parameter itself is an arbitrary type;
94/// the refinement is carried by the constructor.
95pub const TRUSTED_TYPE_CTOR: &str = "Trusted";
96pub const UNTRUSTED_TYPE_CTOR: &str = "Untrusted";
97
98/// True when `name` is one of the refinement constructors.
99pub fn is_refinement_type(name: &str) -> bool {
100    name == TRUSTED_TYPE_CTOR || name == UNTRUSTED_TYPE_CTOR
101}
102
103/// True when `name` is specifically the safe-to-consume side.
104pub fn is_trusted_type(name: &str) -> bool {
105    name == TRUSTED_TYPE_CTOR
106}
107
108/// True when `name` is specifically the unsafe side.
109pub fn is_untrusted_type(name: &str) -> bool {
110    name == UNTRUSTED_TYPE_CTOR
111}
112
113// ── Refinement annotation parsing ────────────────────────────────────
114
115/// A `#[refines(proof, ...options...)]` annotation attached to a
116/// function body or to a specific `let` binding, declaring that the
117/// body produces a `Trusted<T>` iff the named proof succeeds.
118#[derive(Debug, Clone, PartialEq, Eq)]
119pub struct RefinementAnnotation {
120    pub proof: TrustProof,
121    /// Raw `key=value` pairs accepted by the verifier (e.g.
122    /// `key=env.HMAC_KEY`, `algorithm=SHA256`). The checker does not
123    /// interpret these; the runtime verifier does.
124    pub options: Vec<(String, String)>,
125}
126
127/// Parse a refinement annotation body of the form `hmac` or
128/// `hmac, key=env.HMAC_KEY`. Returns `None` when the proof slug is not
129/// in [`TRUST_CATALOG`] so the checker can emit a targeted error.
130pub fn parse_refinement_annotation(body: &str) -> Option<RefinementAnnotation> {
131    let mut parts = body.split(',').map(|p| p.trim());
132    let proof_slug = parts.next()?.trim();
133    let proof = TrustProof::from_slug(proof_slug)?;
134
135    let mut options = Vec::new();
136    for raw in parts {
137        if raw.is_empty() {
138            continue;
139        }
140        if let Some((k, v)) = raw.split_once('=') {
141            options.push((k.trim().to_string(), v.trim().to_string()));
142        } else {
143            // Malformed option — signal by returning None so the
144            // checker can emit `expected key=value, got '<raw>'`.
145            return None;
146        }
147    }
148    Some(RefinementAnnotation { proof, options })
149}
150
151#[cfg(test)]
152mod tests {
153    use super::*;
154
155    #[test]
156    fn slug_roundtrip_covers_closed_catalog() {
157        for proof in TrustProof::ALL {
158            let slug = proof.slug();
159            assert_eq!(Some(*proof), TrustProof::from_slug(slug));
160            assert!(TRUST_CATALOG.contains(&slug));
161        }
162        assert_eq!(TrustProof::ALL.len(), TRUST_CATALOG.len());
163    }
164
165    #[test]
166    fn unknown_slug_is_rejected() {
167        assert!(TrustProof::from_slug("crc32").is_none());
168        assert!(TrustProof::from_slug("").is_none());
169        assert!(TrustProof::from_slug("HMAC").is_none()); // case-sensitive
170    }
171
172    #[test]
173    fn refinement_constructors_recognised() {
174        assert!(is_refinement_type("Trusted"));
175        assert!(is_refinement_type("Untrusted"));
176        assert!(!is_refinement_type("Option"));
177        assert!(!is_refinement_type("trusted")); // case-sensitive
178    }
179
180    #[test]
181    fn parse_annotation_minimal() {
182        let ann = parse_refinement_annotation("hmac").unwrap();
183        assert_eq!(ann.proof, TrustProof::Hmac);
184        assert!(ann.options.is_empty());
185    }
186
187    #[test]
188    fn parse_annotation_with_options() {
189        let ann = parse_refinement_annotation("hmac, key=env.HMAC_KEY, algorithm=SHA256").unwrap();
190        assert_eq!(ann.proof, TrustProof::Hmac);
191        assert_eq!(
192            ann.options,
193            vec![
194                ("key".to_string(), "env.HMAC_KEY".to_string()),
195                ("algorithm".to_string(), "SHA256".to_string()),
196            ]
197        );
198    }
199
200    #[test]
201    fn parse_annotation_rejects_unknown_proof() {
202        assert!(parse_refinement_annotation("crc32, key=foo").is_none());
203    }
204
205    #[test]
206    fn parse_annotation_rejects_malformed_option() {
207        // 'key_without_value' has no '=' sign.
208        assert!(parse_refinement_annotation("hmac, key_without_value").is_none());
209    }
210}