typed/psk: transport seal/open (AES-256-GCM, nonce-prepended frame)

ober

3baf2fa72bd5706f802a3ebdc93103ff0c1884ee

diff --git a/tests/psk_vectors.rs b/tests/psk_vectors.rs
index c6c31f0..72261d4 100644
--- a/tests/psk_vectors.rs
+++ b/tests/psk_vectors.rs
@@ -9,7 +9,7 @@
 
 use jerboa_typed_generated::jsecmon_typed_psk::{
     compute_proof, constant_time_eq_p, derive_auth_key, derive_transport_key, hex_decode,
-    hex_encode, hex_string_p, psk_hex_32_p, verify_proof,
+    hex_encode, hex_string_p, psk_hex_32_p, psk_transport_open, psk_transport_seal, verify_proof,
 };
 
 fn hex(data: &[u8]) -> String {
@@ -155,3 +155,27 @@ fn verify_proof_round_trips_and_rejects_tampering() {
     let other = derive_auth_key([0x43u8; 32].to_vec());
     assert!(!verify_proof(other, nonce, ts, good));
 }
+
+#[test]
+fn psk_transport_seal_open_round_trips() {
+    // secmon encrypt_transport: AES-256-GCM under the transport key with the
+    // 12-byte nonce prepended to the output. The sealed frame is cross-checked
+    // against an independent Python AESGCM reference.
+    let tk = derive_transport_key(PSK_42.to_vec());
+    let nonce = unhex("000102030405060708090a0b");
+    let pt = b"transport probe".to_vec();
+    let sealed = psk_transport_seal(tk.clone(), nonce.clone(), pt.clone());
+    assert_eq!(
+        sealed,
+        unhex("000102030405060708090a0b0b33004bb4619b21e2af73b189248ac3425e264c42b841f1f2f99f574647da")
+    );
+    // the 12-byte nonce is carried verbatim at the front of the frame.
+    assert_eq!(&sealed[..12], &nonce[..]);
+    // decrypt_transport splits the nonce back off and recovers the plaintext.
+    assert_eq!(psk_transport_open(tk.clone(), sealed.clone()), Some(pt));
+    // a flipped byte anywhere in the frame body fails the tag → None.
+    let mut bad = sealed;
+    let last = bad.len() - 1;
+    bad[last] ^= 0x01;
+    assert_eq!(psk_transport_open(tk, bad), None);
+}
diff --git a/typed/psk.ss b/typed/psk.ss
index 65329d3..91a4b09 100644
--- a/typed/psk.ss
+++ b/typed/psk.ss
@@ -12,7 +12,8 @@
 
 (typed-library (jsecmon typed psk)
   (export constant-time-eq? hex-encode hex-decode hex-string? psk-hex-32?
-          derive-auth-key derive-transport-key compute-proof verify-proof)
+          derive-auth-key derive-transport-key compute-proof verify-proof
+          psk-transport-seal psk-transport-open)
 
   ;; --- constant-time comparison (psk.rs::constant_time_eq) ---
 
@@ -115,4 +116,21 @@
   ;; compare it to the candidate in constant time. Timestamp-freshness (a clock
   ;; read + magnitude check, no secret) stays with the untyped caller.
   (def (verify-proof (auth-key : Bytes) (nonce : Bytes) (timestamp : Int) (candidate : Bytes)) : Bool
-    (constant-time-eq? (compute-proof auth-key nonce timestamp) candidate)))
+    (constant-time-eq? (compute-proof auth-key nonce timestamp) candidate))
+
+  ;; --- transport encryption (psk.rs encrypt_transport/decrypt_transport) ---
+
+  ;; secmon prepends the random 12-byte GCM nonce to the AEAD output, so the
+  ;; sealed frame is nonce ‖ ciphertext‖tag. The nonce is supplied here (the
+  ;; untyped caller draws it from the RNG) to keep the kernel deterministic.
+  (def (psk-transport-seal (transport-key : Bytes) (nonce : Bytes) (plaintext : Bytes)) : Bytes
+    (bytevector-append nonce
+      (aes-256-gcm-seal transport-key nonce plaintext (string->utf8 ""))))
+
+  ;; decrypt_transport: split the leading 12-byte nonce back off the frame and
+  ;; AEAD-open the remainder. (Some plaintext) on success, None on a bad tag.
+  (def (psk-transport-open (transport-key : Bytes) (sealed : Bytes)) : (Option Bytes)
+    (aes-256-gcm-open transport-key
+      (bytevector-copy sealed 0 12)
+      (bytevector-copy sealed 12 (bytevector-length sealed))
+      (string->utf8 ""))))