////////////////////////////////////////////////////////////////
// Copyright 2016 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.
//
////////////////////////////////////////////////////////////////

import "HMAC_iterative_old.cry";
import "Hashing.cry";

////////////////////////////////////////////////////////////////
// Generic Utilities.
//

let alloc_init ty v = do {
    p <- crucible_alloc ty;
    crucible_points_to p v;
    return p;
};

let ptr_to_fresh n ty = do {
    x <- crucible_fresh_var n ty;
    p <- alloc_init ty (crucible_term x);
    return (x, p);
};

let yices_hash_unint =
    unint_yices [ "hash_init_c_state"
                , "hash_update_c_state"
                , "hash_digest_c_state"
                ];

////////////////////////////////////////////////////////////////
// Hash.
//

let hash_state_inner pstate =
    crucible_elem (crucible_elem (crucible_elem pstate 2) 0) 0;

let setup_hash_state pstate = do {
    alg0 <- crucible_fresh_var "alg" (llvm_int 32);
    h0 <- crucible_fresh_var "h" (llvm_array 8 (llvm_int 64));
    Nl0 <- crucible_fresh_var "Nl" (llvm_int 64);
    Nh0 <- crucible_fresh_var "Nh" (llvm_int 64);
    u0 <- crucible_fresh_var "u" (llvm_array 16 (llvm_int 64));
    num0 <- crucible_fresh_var "num" (llvm_int 32);
    md_len0 <- crucible_fresh_var "md_len" (llvm_int 32);
    (_, pimpl) <- ptr_to_fresh "impl" (llvm_struct "struct.s2n_hash");
    crucible_points_to pstate
      (crucible_struct
        [ pimpl
        , crucible_term alg0
        , crucible_struct
          [ crucible_struct
            [ crucible_struct
              [ crucible_term h0
              , crucible_term Nl0
              , crucible_term Nh0
              , crucible_struct [ crucible_term u0 ]
              , crucible_term num0
              , crucible_term md_len0
              ]
            ]
          ]
        ]);
    let st = {{
      { h = h0
      , Nl = Nl0
      , Nh = Nh0
      , u = u0
      , num = num0
      , md_len = md_len0
      }
    }};
    return st;
};

let update_hash_state pstate st = do {
    crucible_points_to (crucible_elem (hash_state_inner pstate) 0) (crucible_term {{ st.h }});
    crucible_points_to (crucible_elem (hash_state_inner pstate) 1) (crucible_term {{ st.Nl }});
    crucible_points_to (crucible_elem (hash_state_inner pstate) 2) (crucible_term {{ st.Nh }});
    crucible_points_to (crucible_elem (crucible_elem (hash_state_inner pstate) 3) 0) (crucible_term {{ st.u }});
    crucible_points_to (crucible_elem (hash_state_inner pstate) 4) (crucible_term {{ st.num }});
    crucible_points_to (crucible_elem (hash_state_inner pstate) 5) (crucible_term {{ st.md_len }});
};

let hash_init_spec = do {
    pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
    st0 <- setup_hash_state pstate;
    alg <- crucible_fresh_var "alg" (llvm_int 32);
    crucible_execute_func [pstate, crucible_term alg];
    // We need to pass in the starting state since many of the bits in
    // the union are unused by many of the hash algorithms.
    let st1 = {{ hash_init_c_state st0 }};
    update_hash_state pstate st1;
    crucible_return (crucible_term {{ 0 : [32] }});
};

let hash_reset_spec = do {
    pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
    st0 <- setup_hash_state pstate;
    crucible_execute_func [pstate];
    let st1 = {{ hash_init_c_state st0 }};
    update_hash_state pstate st1;
    crucible_return (crucible_term {{ 0 : [32] }});
};

let hash_copy_spec = do {
    pstate1 <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
    pstate2 <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
    st1 <- setup_hash_state pstate1;
    st2 <- setup_hash_state pstate2;
    crucible_execute_func [pstate1, pstate2];
    update_hash_state pstate1 st2;
    crucible_return (crucible_term {{ 0 : [32] }});
};

let hash_update_spec msg_size = do {
    pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
    (msg, pmsg) <- ptr_to_fresh "msg" (llvm_array msg_size (llvm_int 8));
    st0 <- setup_hash_state pstate;
    let size = crucible_term {{ `msg_size : [32] }};
    crucible_execute_func [pstate, pmsg, size];
    let st1 = {{ hash_update_c_state`{msg_size=msg_size} st0 msg }};
    update_hash_state pstate st1;
    crucible_return (crucible_term {{ 0 : [32] }});
};

let hash_digest_spec digest_size = do {
    pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
    (dgst, pdgst) <- ptr_to_fresh "out" (llvm_array digest_size (llvm_int 8));
    st0 <- setup_hash_state pstate;
    size <- crucible_fresh_var "size" (llvm_int 32);
    crucible_execute_func [pstate, pdgst, crucible_term size];
    let out1 = {{ hash_digest_c_state`{digest_size=digest_size} st0 }};
    crucible_points_to pdgst (crucible_term out1);
    crucible_return (crucible_term {{ 0 : [32] }});
};

////////////////////////////////////////////////////////////////
// HMAC.

let setup_hmac_state alg0 hash_block_size0 block_size0 digest_size0 = do {
    pstate <- crucible_alloc (llvm_struct "struct.s2n_hmac_state");
    currently_in_hash_block0 <- crucible_fresh_var "currently_in_hash_block" (llvm_int 32);
    xor_pad0 <- crucible_fresh_var "xor_pad" (llvm_array 128 (llvm_int 8));
    let digest_size = eval_size {| SHA512_DIGEST_LENGTH |};
    digest_pad0 <- crucible_fresh_var "digest_pad" (llvm_array digest_size (llvm_int 8));

    // ...
    crucible_points_to (crucible_elem pstate 0) (crucible_term alg0);
    crucible_points_to (crucible_elem pstate 1) (crucible_term hash_block_size0);
    crucible_points_to (crucible_elem pstate 2) (crucible_term currently_in_hash_block0);
    crucible_points_to (crucible_elem pstate 3) (crucible_term block_size0);
    crucible_points_to (crucible_elem pstate 4) (crucible_term digest_size0);
    inner0 <- setup_hash_state (crucible_elem pstate 5);
    inner_just_key0 <- setup_hash_state (crucible_elem pstate 6);
    outer0 <- setup_hash_state (crucible_elem pstate 7);
    crucible_points_to (crucible_elem pstate 8) (crucible_term xor_pad0);
    crucible_points_to (crucible_elem pstate 9) (crucible_term digest_pad0);
    // ...

    // ...
    let st0 = {{
        { alg                     = alg0
        , hash_block_size         = hash_block_size0
        , currently_in_hash_block = currently_in_hash_block0
        , block_size              = block_size0
        , digest_size             = digest_size0
        , inner                   = inner0
        , inner_just_key          = inner_just_key0
        , outer                   = outer0
        , xor_pad                 = xor_pad0
        , digest_pad              = digest_pad0
        }
      }};
    // ...
    return (pstate, st0);
};

let check_hmac_state pstate st = do {
    crucible_points_to (crucible_elem pstate 0) (crucible_term {{ st.alg }});
    crucible_points_to (crucible_elem pstate 1) (crucible_term {{ st.hash_block_size }});
    crucible_points_to (crucible_elem pstate 2) (crucible_term {{ st.currently_in_hash_block }});
    crucible_points_to (crucible_elem pstate 3) (crucible_term {{ st.block_size }});
    crucible_points_to (crucible_elem pstate 4) (crucible_term {{ st.digest_size }});
    update_hash_state (crucible_elem pstate 5) {{ st.inner }};
    update_hash_state (crucible_elem pstate 6) {{ st.inner_just_key }};

    // XXX: Don't care about 'outer' because it gets overwritten by
    // 's2n_hash_reset' before use in 's2n_hmac_digest'.
    //
    //update_hash_state (crucible_elem pstate 7) {{ st.outer }};
    crucible_points_to (crucible_elem pstate 8) (crucible_term {{ st.xor_pad }});

    // Don't care about 'digest_pad', because it gets overwritten
    // using 's2n_hash_digest' before use in 's2n_hmac_digest'.
    //
    // However, if we leave it in, the proof still goes through
    // (since we model exactly what happens).
    //
    //crucible_points_to (crucible_elem pstate 9) (crucible_term {{ st.digest_pad }});
};

let hmac_invariants
      st
      (cfg : { name            : String
             , hmac_alg        : Term
             , digest_size     : Int
             , block_size      : Int
             , hash_block_size : Int
             }) = do {
    // Specify the HMAC algorithm.
    crucible_equal (crucible_term {{ st.alg }}) (crucible_term cfg.hmac_alg);

    // Specify sizes
    let hash_block_size = cfg.hash_block_size;
    let block_size = cfg.block_size;
    let digest_size = cfg.digest_size;
    crucible_equal (crucible_term {{ st.hash_block_size }}) (crucible_term {{ `hash_block_size : [16] }});
    crucible_equal (crucible_term {{ st.block_size }}) (crucible_term {{ `block_size : [16] }});
    crucible_equal (crucible_term {{ st.digest_size }}) (crucible_term {{ `digest_size : [8] }});
};

////////////////////////////////////////////////////////////////

let hmac_init_spec
      key_size
      (cfg : { name            : String
             , hmac_alg        : Term
             , digest_size     : Int
             , block_size      : Int
             , hash_block_size : Int
             }) = do {
    (key0, pkey) <- ptr_to_fresh "key" (llvm_array key_size (llvm_int 8));

    alg0 <- crucible_fresh_var "alg" (llvm_int 32);
    hash_block_size0 <- crucible_fresh_var "hash_block_size" (llvm_int 16);
    block_size0 <- crucible_fresh_var "block_size" (llvm_int 16);
    digest_size0 <- crucible_fresh_var "digest_size" (llvm_int 8);
    (pstate, st0) <- setup_hmac_state alg0 hash_block_size0 block_size0 digest_size0;

    crucible_execute_func [pstate, crucible_term (cfg.hmac_alg), pkey, crucible_term {{ `key_size : [32] }}];

    let block_size      = cfg.block_size;
    let hash_block_size = cfg.hash_block_size;
    let digest_size     = cfg.digest_size;
    let alg0            = cfg.hmac_alg;

    let st1 = {{
      hmac_init_c_state
        `{key_size=key_size
         ,block_size=block_size
         ,hash_block_size=hash_block_size
         ,digest_size=digest_size}
        st0 alg0 key0
    }};
    check_hmac_state pstate st1;
    hmac_invariants st1 cfg;
    crucible_return (crucible_term {{ 0 : [32] }});
};

let hmac_update_spec
      msg_size
      (cfg : { name            : String
             , hmac_alg        : Term
             , digest_size     : Int
             , block_size      : Int
             , hash_block_size : Int
             }) = do {
    (msg, pmsg) <- ptr_to_fresh "msg" (llvm_array msg_size (llvm_int 8));

    let digest_size = cfg.digest_size;
    let block_size = cfg.block_size;
    let hash_block_size = cfg.hash_block_size;
    (pstate, st0) <- setup_hmac_state
                       cfg.hmac_alg
                       {{ `hash_block_size : [16] }}
                       {{ `block_size : [16] }}
                       {{ `digest_size : [8] }};

    hmac_invariants st0 cfg;

    let size = {{ `msg_size : [32] }};
    crucible_execute_func [pstate, pmsg, crucible_term size];

    let st1 = {{ hmac_update_c_state st0 msg }};
    check_hmac_state pstate st1;
    hmac_invariants st1 cfg;

    crucible_return (crucible_term {{ 0 : [32] }});
};

let hmac_digest_spec
      (cfg : { name            : String
             , hmac_alg        : Term
             , digest_size     : Int
             , block_size      : Int
             , hash_block_size : Int
             }) = do {
    (out, pout) <- ptr_to_fresh "out" (llvm_array cfg.digest_size (llvm_int 8));

    let digest_size = cfg.digest_size;
    let block_size = cfg.block_size;
    let hash_block_size = cfg.hash_block_size;
    (pstate, st0) <- setup_hmac_state
                       cfg.hmac_alg
                       {{ `hash_block_size : [16] }}
                       {{ `block_size : [16] }}
                       {{ `digest_size : [8] }};

    hmac_invariants st0 cfg;

    let hash_block_size = cfg.hash_block_size;
    let block_size = cfg.block_size;
    let digest_size = cfg.digest_size;
    let size = {{ `digest_size : [32] }};
    crucible_execute_func [pstate, pout, crucible_term size];
    let st1_digest = {{
      hmac_digest_c_state`{block_size=block_size,digest_size=digest_size} st0
    }};
    let st1 = {{ st1_digest.0 }};
    let digest = {{ split (st1_digest.1) : [digest_size][8] }};

    crucible_points_to pout (crucible_term digest);
    crucible_return (crucible_term {{ 0 : [32] }});
};

let hmac_digest_size_spec
      (cfg : { name            : String
             , hmac_alg        : Term
             , digest_size     : Int
             , block_size      : Int
             , hash_block_size : Int
             }) = do {
    psize <- crucible_alloc (llvm_int 8);
    crucible_execute_func [crucible_term cfg.hmac_alg, psize];
    let digest_size = cfg.digest_size;
    crucible_points_to psize (crucible_term {{ `digest_size : [8] }});
    crucible_return (crucible_term {{ 0 : [32] }});
};