Implement verified x86-64 Triple DES ECB

README.md

@@ -397,7 +397,7 @@ yours to keep:
 
 <td>✅</td>
 
-<td>❌</td>
+<td>✅</td>
 
 <td>❌</td>
 

bench/benches/primitives/main.rs

@@ -45,6 +45,7 @@ mod sha224;
 mod sha256;
 mod sha3;
 mod sha512;
+mod triple_des_ecb;
 mod x25519;
 mod x448;
 
@@ -212,6 +213,7 @@ const BENCHES: &[Bench] = &[
     (pbkdf2_sha512::USES, pbkdf2_sha512::bench),
     (poly1305::USES, poly1305::bench),
     (rc2_cbc::USES, rc2_cbc::bench),
+    (triple_des_ecb::USES, triple_des_ecb::bench),
     (scrypt::USES, scrypt::bench),
     (sha1::USES, sha1::bench),
     (sha224::USES, sha224::bench),

bench/benches/primitives/triple_des_ecb.rs

@@ -0,0 +1,63 @@
+//! Triple DES ECB, including key expansion and in-place encryption/decryption.
+
+use criterion::Criterion;
+
+/// The library modules whose code these benchmarks run.
+pub const USES: &[&str] = &["triple_des_ecb", "triple_des"];
+
+#[cfg(target_arch = "x86_64")]
+pub fn bench(c: &mut Criterion) {
+    use std::hint::black_box;
+
+    use criterion::{BenchmarkId, Throughput};
+    use openssl::nid::Nid;
+    use openssl::symm::{Cipher, Crypter, Mode};
+    use verified_garbage::triple_des_ecb::TripleDesEcb;
+
+    use crate::{OPENSSL, SIZES, VG};
+
+    let key: Vec<_> = (0..24).map(|i| (17 * i + 3) as u8).collect();
+    for (key_len, cipher) in [
+        (16, Cipher::from_nid(Nid::DES_EDE_ECB).unwrap()),
+        (24, Cipher::des_ede3_ecb()),
+    ] {
+        for (operation, encrypt, mode) in [
+            ("encrypt", true, Mode::Encrypt),
+            ("decrypt", false, Mode::Decrypt),
+        ] {
+            let mut group = c.benchmark_group(format!("3des-ecb-{operation}-{key_len}"));
+            for size in SIZES {
+                group.throughput(Throughput::Bytes(size as u64));
+                let data = vec![0x5a; size];
+                let mut buffer = vec![0; size];
+                group.bench_function(BenchmarkId::new(VG, size), |b| {
+                    b.iter(|| {
+                        let ctx = TripleDesEcb::new(black_box(&key[..key_len])).unwrap();
+                        buffer.copy_from_slice(black_box(&data));
+                        if encrypt {
+                            ctx.encrypt(black_box(&mut buffer)).unwrap();
+                        } else {
+                            ctx.decrypt(black_box(&mut buffer)).unwrap();
+                        }
+                        black_box(&buffer);
+                    })
+                });
+                let mut output = vec![0; size + 8];
+                group.bench_function(BenchmarkId::new(OPENSSL, size), |b| {
+                    b.iter(|| {
+                        let mut ctx =
+                            Crypter::new(cipher, mode, black_box(&key[..key_len]), None).unwrap();
+                        ctx.pad(false);
+                        let n = ctx.update(black_box(&data), &mut output).unwrap();
+                        let n = n + ctx.finalize(&mut output[n..]).unwrap();
+                        black_box(&output[..n]);
+                    })
+                });
+            }
+            group.finish();
+        }
+    }
+}
+
+#[cfg(not(target_arch = "x86_64"))]
+pub fn bench(_: &mut Criterion) {}

lean/VerifiedGarbage/Artifacts/TripleDes/X86_64.lean

@@ -0,0 +1,56 @@
+import VerifiedGarbage.Proof.TripleDes.X86_64.VerifiedBlock
+import VerifiedGarbage.Proof.TripleDes.X86_64.Key.Verified
+import VerifiedGarbage.Proof.TripleDes.X86_64.Ecb.Verified
+
+namespace VG.Artifacts.TripleDes.X86_64
+
+def artifacts : List Artifact := [
+  { Spec.TripleDes.expandKeyApi with
+    target := X86_64.target
+    doc := Spec.TripleDes.expandKeyApi.doc
+      (notes := ["Baseline x86-64 scalar key expansion with fixed permutations and public round-count branches."])
+    code := Impl.TripleDes.X86_64.Key.expandKey
+    contract := Spec.TripleDes.expandKeyContract X86_64.abi
+    stack := 0
+    verified := Proof.TripleDes.X86_64.Key.verified
+    spSafe := Code.all_of_allInstrs (by lit_decide) },
+  { Spec.TripleDes.encryptBlockApi with
+    target := X86_64.target
+    doc := Spec.TripleDes.encryptBlockApi.doc
+      (notes := ["Baseline x86-64 scalar Boolean S-box circuits; IP and FP shared across all three DES passes."])
+    code := Impl.TripleDes.X86_64.encryptBlock
+    contract := Spec.TripleDes.encryptBlockContract X86_64.abi
+    stack := 0
+    verified := Proof.TripleDes.X86_64.encrypt_verified
+    spSafe := Code.all_of_allInstrs (by lit_decide) },
+  { Spec.TripleDes.decryptBlockApi with
+    target := X86_64.target
+    doc := Spec.TripleDes.decryptBlockApi.doc
+      (notes := ["Baseline x86-64 scalar Boolean S-box circuits with reverse EDE key order."])
+    code := Impl.TripleDes.X86_64.decryptBlock
+    contract := Spec.TripleDes.decryptBlockContract X86_64.abi
+    stack := 0
+    verified := Proof.TripleDes.X86_64.decrypt_verified
+    spSafe := Code.all_of_allInstrs (by lit_decide) },
+  { Spec.TripleDes.ecbEncryptApi with
+    target := X86_64.target
+    doc := Spec.TripleDes.ecbEncryptApi.doc
+      (notes := ["Baseline x86-64, calling the verified Triple DES block primitive for each complete block."])
+    code := Impl.TripleDes.X86_64.Ecb.encrypt
+    contract := Spec.TripleDes.ecbEncryptContract X86_64.abi 8
+    stack := 8
+    ofSig := ⟨_, _, _, by unfold Spec.TripleDes.ecbEncryptContract Spec.TripleDes.ecbContract; rfl⟩
+    verified := Proof.TripleDes.X86_64.Ecb.encrypt_verified
+    spSafe := Code.all_of_allInstrs (by lit_decide) },
+  { Spec.TripleDes.ecbDecryptApi with
+    target := X86_64.target
+    doc := Spec.TripleDes.ecbDecryptApi.doc
+      (notes := ["Baseline x86-64, calling the verified Triple DES block primitive for each complete block."])
+    code := Impl.TripleDes.X86_64.Ecb.decrypt
+    contract := Spec.TripleDes.ecbDecryptContract X86_64.abi 8
+    stack := 8
+    ofSig := ⟨_, _, _, by unfold Spec.TripleDes.ecbDecryptContract Spec.TripleDes.ecbContract; rfl⟩
+    verified := Proof.TripleDes.X86_64.Ecb.decrypt_verified
+    spSafe := Code.all_of_allInstrs (by lit_decide) }]
+
+end VG.Artifacts.TripleDes.X86_64