////////////////////////////////////////////////////////////////
// Copyright 2020 Galois, Inc. All Rights Reserved
//
// Authors:
//      Aaron Tomb : atomb@galois.com
//	Nathan Collins : conathan@galois.com
//      Joey Dodds : jdodds@galois.com
//
// Licensed under the Apache License, Version 2.0 (the "License").
// You may not use this file except in compliance with the License.
// A copy of the License is located at
//
//  http://aws.amazon.com/apache2.0
//
// or in the "license" file accompanying this file. This file is distributed
// on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
// express or implied. See the License for the specific language governing
// permissions and limitations under the License.
//
////////////////////////////////////////////////////////////////

enable_experimental;

include "HMAC/spec/HMAC.saw";

m <- llvm_load_module "bitcode/all_llvm.bc";

// Verifies s2n_hmac_init at 3 key sizes in the given config
let verify_s2n_hmac_init
  (cfg : { name            : String
             , hmac_alg        : Term
             , digest_size     : Int
             , block_size      : Int
             , hash_block_size : Int
             }) = do {
  set_base 16;
  
  print "";
  print (str_concat "Verifying HMAC init: alg = " cfg.name);
  
  print "Creating hash overrides...";
  (t, hash_init_ov)  <- with_time (crucible_llvm_unsafe_assume_spec m "s2n_hash_init" hash_init_spec);
  (t, hmac_digest_size_ov) <- with_time (crucible_llvm_unsafe_assume_spec m "s2n_hmac_digest_size" (hmac_digest_size_spec cfg));
  (t, hash_copy_ov) <- with_time (crucible_llvm_unsafe_assume_spec m "s2n_hash_copy" hash_copy_spec);
  (t, hash_reset_ov) <- with_time (crucible_llvm_unsafe_assume_spec m "s2n_hash_reset" hash_reset_spec);
  (t, hash_get_currently_in_hash_total_ov) <- with_time (crucible_llvm_unsafe_assume_spec m "s2n_hash_get_currently_in_hash_total" (hash_get_currently_in_hash_total_spec));
  (t, hash_update_block_size_ov)  <- with_time (crucible_llvm_unsafe_assume_spec m "s2n_hash_update" (hash_update_spec cfg.block_size));
  (t, hash_update_key_size_ov) <- with_time (crucible_llvm_unsafe_assume_spec m "s2n_hash_update" hash_update_unbounded_spec);
  (t, hash_digest_ov) <- with_time (crucible_llvm_unsafe_assume_spec m "s2n_hash_digest" (hash_digest_spec (cfg.digest_size)));
  print "Done";
  
  let ovs =
    [ hash_init_ov
    , hmac_digest_size_ov
    , hash_copy_ov
    , hash_reset_ov
    , hash_get_currently_in_hash_total_ov
    , hash_update_block_size_ov
    , hash_update_key_size_ov
    , hash_digest_ov
    ];
  let block_size = cfg.block_size;
  
  with_time (crucible_llvm_verify m "s2n_hmac_init" ovs false (hmac_init_spec cfg) z3_hash_unint);
        
  print "Finished proving s2n_hmac_init";
};

// Verifies s2n_hmac_update at the given message sizes and config
let verify_s2n_hmac_update
  (cfg : { name            : String
             , hmac_alg        : Term
             , digest_size     : Int
             , block_size      : Int
             , hash_block_size : Int
             }) = do {
  set_base 16;
  
  print "";
  print (str_concat "Verifying HMAC update: alg = " cfg.name);
  
  (t, hash_update_msg_size_ov) <- with_time (crucible_llvm_unsafe_assume_spec m "s2n_hash_update" hash_update_unbounded_spec);
  with_time (crucible_llvm_verify m "s2n_hmac_update" [hash_update_msg_size_ov] false (hmac_update_spec cfg) z3_hash_unint);
        
  print "Finished proving s2n_hmac_update";
};

// Verifies s2n_hmac_digest
let verify_s2n_hmac_digest
  (cfg : { name            : String
             , hmac_alg        : Term
             , digest_size     : Int
             , block_size      : Int
             , hash_block_size : Int
             }) = do {
  set_base 16;
  
  print "";
  print (str_concat "Verifying HMAC digest: alg = " cfg.name);
  
  print "Creating hash overrides...";
  (t, hash_copy_ov) <- with_time (crucible_llvm_unsafe_assume_spec m "s2n_hash_copy" hash_copy_spec);
  (t, hash_update_block_size_ov)  <- with_time (crucible_llvm_unsafe_assume_spec m "s2n_hash_update" (hash_update_spec cfg.digest_size));
  (t, hash_digest_ov) <- with_time (crucible_llvm_unsafe_assume_spec m "s2n_hash_digest" (hash_digest_spec (cfg.digest_size)));
  print "Done";
  
  let ovs =
    [ hash_copy_ov
    , hash_update_block_size_ov
    , hash_digest_ov
    ];
  
  (t, hmac_digest_ov) <-
    with_time (crucible_llvm_verify m "s2n_hmac_digest" ovs false (hmac_digest_spec cfg) z3_hash_unint);
        
  print "Finished proving s2n_hmac_digest";
};

let none_cfg =
  { name            = "NONE"
  , hmac_alg        = {{ S2N_HMAC_NONE }}
  , digest_size     = 0
  , block_size      = 64
  , hash_block_size = 64
  };

// let sslv3_md5_cfg = <not supported>

let md5_cfg =
  { name            = "MD5"
  , hmac_alg        = {{ S2N_HMAC_MD5 }}
  , digest_size     = 16
  , block_size      = 64
  , hash_block_size = 64
  };

// let sslv3_sha1_cfg = <not supported>

let sha1_cfg =
  { name            = "SHA1"
  , hmac_alg        = {{ S2N_HMAC_SHA1 }}
  , digest_size     = 20
  , block_size      = 64
  , hash_block_size = 64
  };

let sha224_cfg =
  { name            = "SHA224"
  , hmac_alg        = {{ S2N_HMAC_SHA224 }}
  , digest_size     = 28
  , block_size      = 64
  , hash_block_size = 64
  };

let sha256_cfg =
  { name            = "SHA256"
  , hmac_alg        = {{ S2N_HMAC_SHA256 }}
  , digest_size     = 32
  , block_size      = 64
  , hash_block_size = 64
  };

let sha384_cfg =
  { name            = "SHA384"
  , hmac_alg        = {{ S2N_HMAC_SHA384 }}
  , digest_size     = 48
  , block_size      = 128
  , hash_block_size = 128
  };

let sha512_cfg =
  { name            = "SHA512"
  , hmac_alg        = {{ S2N_HMAC_SHA512 }}
  , digest_size     = 64
  , block_size      = 128
  , hash_block_size = 128
  };

let verify_s2n_hmac_at_config
      (cfg : { name            : String
             , hmac_alg        : Term
             , digest_size     : Int
             , block_size      : Int
             , hash_block_size : Int
             }) = do {
  verify_s2n_hmac_init cfg;
  verify_s2n_hmac_update cfg;
  verify_s2n_hmac_digest cfg;
};

let verify_s2n_hmac = do {
  let configs = [md5_cfg, sha1_cfg, sha224_cfg, sha256_cfg, sha384_cfg, sha512_cfg];
  
  for configs (\config -> verify_s2n_hmac_at_config config);
};

verify_s2n_hmac;