60 lines
1.5 KiB
Plaintext
60 lines
1.5 KiB
Plaintext
m <- llvm_load_module "hash.bc";
|
|
|
|
include "common.saw";
|
|
|
|
thm_P12 <- mk_P12;
|
|
|
|
let ss0 = cryptol_ss ();
|
|
|
|
thm_unfold_iv <- prove_print rme
|
|
(rewrite ss0
|
|
{{ Ascon_p`{12} [Hash256_IV, 0, 0, 0, 0]
|
|
==
|
|
[0x9b1e5494e934d681,
|
|
0x4bc3a01e333751d2,
|
|
0xae65396c6b34b81a,
|
|
0x3c7fd4a4d56a4db3,
|
|
0x1a5c464906c5976d]
|
|
}});
|
|
|
|
let verify_hash256 IN_len =
|
|
llvm_verify
|
|
m "crypto_hash"
|
|
[thm_P12]
|
|
true
|
|
do {
|
|
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] }});
|
|
};
|
|
|
|
// What4 will have completely evaluated the term from symbolic evaluation
|
|
// so don't try to keep Ascon_p uninterpreted at all.
|
|
verify_hash256 0 rme;
|
|
|
|
for [ 1, 2, 3, 4, 5, 6, 7,
|
|
8, 9, 10, 11, 12, 13, 14, 15,
|
|
16, 17, 18, 19, 20, 21, 22, 23,
|
|
24, 25, 26, 27, 28, 29, 30, 31,
|
|
32, 33] (\IN_len -> do {
|
|
|
|
print ("Verifying for size", IN_len);
|
|
verify_hash256 IN_len
|
|
do {
|
|
// What4 will have simplified away the application of
|
|
// Ascon_p to the IV, so simplify that away before
|
|
// holding all other Ascon_p occurences uninterpreted.
|
|
|
|
unfolding ["Hash256_bytes", "Hash256", "hashBlocks"];
|
|
simplify (addsimp thm_unfold_iv ss0);
|
|
w4_unint_rme ["Ascon_p"];
|
|
};
|
|
});
|