glguy/ascon
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Cleanups

Browse Source
This commit is contained in:
Eric Mertens
2025-09-30 20:39:30 -07:00
parent 1a52dd9b2d
commit 8732e75271
2 changed files with 15 additions and 16 deletions
Download Patch File Download Diff File Expand all files Collapse all files

11
ref-verification/aead.saw
View File

@@ -22,10 +22,10 @@ let verify_encrypt A_len P_len = do {
do {
// Inputs
let CT_len = eval_size {| P_len + T_len |};
let A_type = llvm_array A_len i8;
let P_type = llvm_array P_len i8;
let CT_len = eval_size {| P_len + T_len |};
let CT_type = llvm_array CT_len i8;
(P, P_ptr) <- fresh_alloc_readonly "P" P_type;
@@ -62,15 +62,14 @@ let verify_decrypt A_len P_len = do {
do {
let CT_len = eval_size {| P_len + T_len |};
let C_type = llvm_array P_len i8;
let CT_type = llvm_array CT_len i8;
let A_type = llvm_array A_len i8;
let P_type = llvm_array P_len i8;
let C_type = llvm_array P_len i8;
let CT_type = llvm_array CT_len i8;
// Inputs
C <- llvm_fresh_var "C" C_type;
T <- llvm_fresh_var "T" T_type;
CT_ptr <- llvm_alloc_readonly CT_type;
llvm_points_to CT_ptr (llvm_term {{ C # T }});

20
ref-verification/hash.saw
View File

@@ -22,19 +22,19 @@ thm_unfold_iv <- prove_print rme
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;
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;
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_execute_func [OUT_ptr, IN_ptr, llvm_term {{ `IN_len:[64] }}];
llvm_points_to OUT_ptr (llvm_term {{ Hash256_bytes IN }});
llvm_points_to OUT_ptr (llvm_term {{ Hash256_bytes IN }});
llvm_return (llvm_term {{ 0 : [32] }});
};