typed/crypto: AES-256-GCM AEAD kernels (encrypt/decrypt)

ober

3933ecbc6ac30098b71898ac45552ff112123f9c

diff --git a/tests/crypto_vectors.rs b/tests/crypto_vectors.rs
index 26000e5..260f544 100644
--- a/tests/crypto_vectors.rs
+++ b/tests/crypto_vectors.rs
@@ -11,8 +11,8 @@
 //! reproduces HKDF's "salt not provided" path that secmon's PSK relies on.
 
 use jerboa_typed_generated::jsecmon_typed_crypto::{
-    derive_ecies_key, hkdf_sha256_derive, hmac_sha256_tag, sha256_digest, x25519_dh_shared,
-    x25519_public_key,
+    aes_256_gcm_decrypt, aes_256_gcm_encrypt, derive_ecies_key, hkdf_sha256_derive,
+    hmac_sha256_tag, sha256_digest, x25519_dh_shared, x25519_public_key,
 };
 
 fn hex(s: &str) -> Vec<u8> {
@@ -107,3 +107,71 @@ fn derive_ecies_key_matches_reference() {
         hex("20603cc4d87eda03c246e38a9250eb66611272bf80a7d5b2d5b8a39ea5b4fcb7")
     );
 }
+
+// AES-256-GCM (NIST SP 800-38D / McGrew–Viega GCM test cases 13–16). seal
+// returns ciphertext‖tag (the RustCrypto convention); these expected values
+// were cross-checked against an independent implementation (Python
+// `cryptography`/OpenSSL), not against the kernel itself.
+const GCM_KEY: &str = "feffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308";
+const GCM_IV: &str = "cafebabefacedbaddecaf888";
+const GCM_P64: &str = "d9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255";
+
+#[test]
+fn aes256gcm_seal_nist_vectors() {
+    let zk = vec![0u8; 32];
+    let zi = vec![0u8; 12];
+    // TC13: empty plaintext + empty aad → tag only.
+    assert_eq!(
+        aes_256_gcm_encrypt(zk.clone(), zi.clone(), Vec::new(), Vec::new()),
+        hex("530f8afbc74536b9a963b4f1c4cb738b")
+    );
+    // TC14: 16 zero bytes, empty aad.
+    assert_eq!(
+        aes_256_gcm_encrypt(zk, zi, vec![0u8; 16], Vec::new()),
+        hex("cea7403d4d606b6e074ec5d3baf39d18d0d1c8a799996bf0265b98b5d48ab919")
+    );
+    // TC15: real key, 64-byte plaintext, empty aad.
+    assert_eq!(
+        aes_256_gcm_encrypt(hex(GCM_KEY), hex(GCM_IV), hex(GCM_P64), Vec::new()),
+        hex("522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662898015adb094dac5d93471bdec1a502270e3cc6c")
+    );
+}
+
+#[test]
+fn aes256gcm_seal_with_aad_nist_tc16() {
+    // TC16: 60-byte plaintext authenticated under a 20-byte aad — proves the
+    // aad operand is wired through (different tag from TC15's empty aad).
+    let p60 = &hex(GCM_P64)[..60];
+    let aad = hex("feedfacedeadbeeffeedfacedeadbeefabaddad2");
+    assert_eq!(
+        aes_256_gcm_encrypt(hex(GCM_KEY), hex(GCM_IV), p60.to_vec(), aad),
+        hex("522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f66276fc6ece0f4e1768cddf8853bb2d551b")
+    );
+}
+
+#[test]
+fn aes256gcm_open_round_trips_and_rejects_tampering() {
+    let key = hex(GCM_KEY);
+    let iv = hex(GCM_IV);
+    let aad = hex("feedfacedeadbeeffeedfacedeadbeefabaddad2");
+    let pt = hex(GCM_P64);
+    let ct = aes_256_gcm_encrypt(key.clone(), iv.clone(), pt.clone(), aad.clone());
+
+    // a faithful seal/open round-trip recovers the plaintext.
+    assert_eq!(
+        aes_256_gcm_decrypt(key.clone(), iv.clone(), ct.clone(), aad.clone()),
+        Some(pt)
+    );
+    // flipping any ciphertext byte fails the tag → None (not a panic, not garbage).
+    let mut tampered = ct.clone();
+    tampered[0] ^= 0x01;
+    assert_eq!(aes_256_gcm_decrypt(key.clone(), iv.clone(), tampered, aad.clone()), None);
+    // altering the aad fails authentication → None.
+    let mut bad_aad = aad.clone();
+    bad_aad[0] ^= 0x01;
+    assert_eq!(aes_256_gcm_decrypt(key.clone(), iv.clone(), ct.clone(), bad_aad), None);
+    // a wrong key fails authentication → None.
+    let mut wrong_key = key;
+    wrong_key[0] ^= 0x01;
+    assert_eq!(aes_256_gcm_decrypt(wrong_key, iv, ct, aad), None);
+}
diff --git a/typed/crypto.ss b/typed/crypto.ss
index 33b2d04..6501dfe 100644
--- a/typed/crypto.ss
+++ b/typed/crypto.ss
@@ -19,7 +19,8 @@
 
 (typed-library (jsecmon typed crypto)
   (export sha256-digest hmac-sha256-tag hkdf-sha256-derive
-          x25519-dh-shared x25519-public-key derive-ecies-key)
+          x25519-dh-shared x25519-public-key derive-ecies-key
+          aes-256-gcm-encrypt aes-256-gcm-decrypt)
 
   ;; SHA-256 of an arbitrary byte string → 32-byte digest.
   (def (sha256-digest (data : Bytes)) : Bytes
@@ -48,4 +49,17 @@
   ;; secmon derive_aes_key: HKDF-SHA256 with the ephemeral public key as salt,
   ;; the ECDH shared secret as IKM, info "secmon-ecies-v1" → a 32-byte AES key.
   (def (derive-ecies-key (shared-secret : Bytes) (ephemeral-public : Bytes)) : Bytes
-    (hkdf-sha256 ephemeral-public shared-secret (string->utf8 "secmon-ecies-v1") 32)))
+    (hkdf-sha256 ephemeral-public shared-secret (string->utf8 "secmon-ecies-v1") 32))
+
+  ;; --- AES-256-GCM AEAD (secmon transport + ECIES payload sealing) ---
+
+  ;; Seal `plaintext` under a 32-byte `key` and 12-byte `nonce` with additional
+  ;; authenticated data `aad` (empty in secmon). Returns ciphertext with the
+  ;; 16-byte GCM tag appended — the exact buffer Aes256Gcm::encrypt produces.
+  (def (aes-256-gcm-encrypt (key : Bytes) (nonce : Bytes) (plaintext : Bytes) (aad : Bytes)) : Bytes
+    (aes-256-gcm-seal key nonce plaintext aad))
+
+  ;; Open a ct‖tag buffer; (Some plaintext) on success, None when the tag fails
+  ;; to verify (wrong key, tampered ciphertext or aad) — secmon's decrypt error.
+  (def (aes-256-gcm-decrypt (key : Bytes) (nonce : Bytes) (ciphertext : Bytes) (aad : Bytes)) : (Option Bytes)
+    (aes-256-gcm-open key nonce ciphertext aad)))