////////////////////////////////////////////////////////////////
// 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/spec/HMAC_iterative.cry";
import "HMAC/spec/HMAC_properties.cry";

let check n = do {
    print (str_concat "Checking 'hmac_c_state_correct' for byte count " (show n));
    x <- time (prove_print abc {{ hmac_c_state_correct : HMAC_c_state -> [n][8] -> [n][8] -> Bit }});
    print("***BEGIN JSON FOR METRICS");
    print("{");
    print(str_concat (str_concat "\"Name\": \"hmac_c_state_correct size " (show n)) "\",");
    print(str_concat (str_concat "\"Size\" : " (show n)) "}");
    print("***END JSON FOR METRICS");
};

for [0, 1, 128 /*,  2, 63, 64, 65, 127, 128, 129 , 1000 */] check;