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
34
35
|
////////////////////////////////////////////////////////////////
// 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;
|
