m <- llvm_load_module "hash.bc";

include "common.saw";

thm_P12 <- mk_P12;

let ss0 = cryptol_ss ();

thm_null_input <- prove_print rme
  (rewrite ss0
    {{ \(x : [0][8]) -> Hash256_bytes x ==
       [0x0b, 0x3b, 0xe5, 0x85, 0x0f, 0x2f, 0x6b, 0x98,
        0xca, 0xf2, 0x9f, 0x8f, 0xde, 0xa8, 0x9b, 0x64,
        0xa1, 0xfa, 0x70, 0xaa, 0x24, 0x9b, 0x8f, 0x83,
        0x9b, 0xd5, 0x3b, 0xaa, 0x30, 0x4d, 0x92, 0xb2] }});

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 [  0,  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 {
      // Handle zero case that completely evaluated away
      simplify (addsimp thm_null_input ss0);

      // Expose (Ascon_p [IV,0,0,0,0])
      unfolding ["Hash256_bytes", "Hash256", "hashBlocks"];

      // Handle non-zero case where W4 simplified the IV permutation
      simplify (addsimp thm_unfold_iv ss0);

      w4_unint_rme ["Ascon_p"];
    };
});