Add reference implementation verification scripts

ref-verification/README.md

@@ -0,0 +1,4 @@
+# Reference Implementation verification
+
+Verification scripts for reference implementations in
+https://github.com/ascon/ascon-c/tree/main

ref-verification/aead.saw

@@ -0,0 +1,57 @@
+m <- llvm_load_module "aead.bc";
+
+include "common.saw";
+
+thm_P8 <- mk_P8;
+thm_P12 <- mk_P12;
+
+let verify_aead P_len A_len = do {
+  llvm_verify
+  m "crypto_aead_encrypt"
+  [thm_P12, thm_P8]
+  false
+  do {
+    // Inputs
+
+    let P_type = llvm_array P_len i8;
+    (P, P_ptr) <- fresh_alloc_readonly "P" P_type;
+
+    let A_type = llvm_array A_len i8;
+    (A, A_ptr) <- fresh_alloc_readonly "A" A_type;
+
+    let N_type = llvm_array 16 i8;
+    (N, N_ptr) <- fresh_alloc_readonly "N" N_type;
+
+    let K_type = llvm_array 16 i8;
+    (K, K_ptr) <- fresh_alloc_readonly "K" K_type;
+
+    // Outputs
+
+    let C_len = eval_size {| P_len + 16 |};
+    let C_type = llvm_array C_len i8;
+    C_ptr <- llvm_alloc C_type;
+
+    CLEN_ptr <- llvm_alloc i64;
+
+    llvm_execute_func
+      [ C_ptr, CLEN_ptr
+      , P_ptr, llvm_term {{ `P_len:[64] }}
+      , A_ptr, llvm_term {{ `A_len:[64] }}
+      , llvm_null
+      , N_ptr
+      , K_ptr
+      ];
+
+    llvm_points_to CLEN_ptr (llvm_term {{ `C_len : [64] }});
+    llvm_points_to C_ptr (llvm_term {{ C # T where (C,T) = AEAD128_encrypt_bytes K N A P }});
+    llvm_return (llvm_term {{ 0 : [32] }});
+  }
+  (unint_yices ["Ascon::Ascon_p"]);
+};
+
+verify_aead 0 0;
+verify_aead 0 1;
+verify_aead 1 0;
+verify_aead 10 10;
+verify_aead 20 20;
+verify_aead 33 100;

ref-verification/common.saw

@@ -0,0 +1,53 @@
+import "/Users/emertens/Source/ascon/Ascon.cry";
+
+let i8 = llvm_int 8;
+let i64 = llvm_int 64;
+let S_type = llvm_array 5 i64;
+
+let fresh_alloc n t = do {
+    X <- llvm_fresh_var n t;
+    X_ptr <- llvm_alloc t;
+    llvm_points_to X_ptr (llvm_term X);
+    return (X, X_ptr);
+};
+
+let fresh_alloc_readonly n t = do {
+    X <- llvm_fresh_var n t;
+    X_ptr <- llvm_alloc_readonly t;
+    llvm_points_to X_ptr (llvm_term X);
+    return (X, X_ptr);
+};
+
+thm_ROUND <- llvm_verify
+  m "ROUND"
+  []
+  false
+  do {
+    (S, S_ptr) <- fresh_alloc "S" S_type;
+    C <- llvm_fresh_var "C" i8;
+    llvm_execute_func [S_ptr, llvm_term C];
+    llvm_points_to S_ptr (llvm_term {{ round S (zext C) }});
+  }
+  rme;
+
+let mk_P12 = llvm_verify
+  m "P12"
+  [thm_ROUND]
+  false
+  do {
+    (S, S_ptr) <- fresh_alloc "S" S_type;
+    llvm_execute_func [S_ptr];
+    llvm_points_to S_ptr (llvm_term {{ Ascon_p`{12} S }});
+  }
+  (w4_unint_rme ["Ascon::round"]);
+
+let mk_P8 = llvm_verify
+  m "P8"
+  [thm_ROUND]
+  false
+  do {
+    (S, S_ptr) <- fresh_alloc "S" S_type;
+    llvm_execute_func [S_ptr];
+    llvm_points_to S_ptr (llvm_term {{ Ascon_p`{8} S }});
+  }
+  (w4_unint_rme ["Ascon::round"]);

ref-verification/hash.saw

@@ -0,0 +1,24 @@
+m <- llvm_load_module "hash.bc";
+
+include "common.saw";
+
+thm_P12 <- mk_P12;
+
+thm_hash <- llvm_verify
+  m "crypto_hash"
+  [thm_P12]
+  true
+  do {
+    let IN_len = 17;
+    let IN_type = llvm_array IN_len (llvm_int 8);
+    (IN, IN_ptr) <- fresh_alloc_readonly "IN" IN_type;
+
+    let OUT_type = llvm_array 32 (llvm_int 8);
+    OUT_ptr <- llvm_alloc OUT_type;
+
+    llvm_execute_func [OUT_ptr, IN_ptr, llvm_term {{ `IN_len:[64] }}];
+
+    llvm_points_to OUT_ptr (llvm_term {{ Hash256_bytes IN }});
+    llvm_return (llvm_term {{ 0 : [32] }});
+  }
+  abc;