////////////////////////////////////////////////////////////////
// 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_properties.cry";
import "modthm.cry";

let hash_lemma1 =
  rewrite (cryptol_ss ()) (unfold_term ["hash_update_append"] {{ hash_update_append }});

let hash_lemma2 =
  rewrite (cryptol_ss ()) (unfold_term ["hash_update_empty"] {{ hash_update_empty }});

let mod_lemma = rewrite (cryptol_ss ()) (unfold_term ["modthm"] {{ modthm }});

let tuple_lemma = rewrite (cryptol_ss ()) (unfold_term ["modthm"] {{ modthm }});

let tuple_lemma = rewrite (cryptol_ss ()) {{
  \a1 b1 c1 d1 a2 b2 c2 d2 ->
    ((a1,b1,c1,d1) == (a2,b2,c2,d2)) == (a1 == a2 /\ b1 == b2 /\ c1 == c2 /\ d1 == d2)
}};

let eq_lemma = rewrite (cryptol_ss ()) {{
  \a -> (a == a) == True
}};

let and_true1 = rewrite (cryptol_ss ()) {{
  \a -> (a /\ True) == a
}};

let and_true2 = rewrite (cryptol_ss ()) {{
  \a -> (True /\ a) == a
}};

let {{
type_add_lemma : {a,b} (fin a, fin b, 32 >= width a, 32 >= width b, 32 >= width (a + b)) => Bit
type_add_lemma = (`(a + b) : [32]) == ((`b : [32]) + (`a : [32]))
}};

let type_add_lemma = rewrite (cryptol_ss()) (unfold_term ["type_add_lemma"] {{ type_add_lemma }});

and_true1_thm <- time (prove_print abc and_true1);
and_true2_thm <- time (prove_print abc and_true2);

time (prove_print (do {
    unfolding ["hmac_update_append"];
    unfolding ["hmac_update_c_state"];
    simplify (cryptol_ss ());
    simplify (addsimps' [hash_lemma1, mod_lemma, tuple_lemma, eq_lemma] empty_ss);
    simplify (addsimps [and_true1_thm, and_true2_thm] empty_ss); 
    simplify (addsimps' [type_add_lemma] empty_ss); 
    simplify (add_prelude_eqs ["eq_refl"] empty_ss);
    simplify (addsimps' [eq_lemma] empty_ss); 
    trivial;
}) {{ hmac_update_append }});

time (prove_print (do {
    unfolding ["hmac_update_empty"];
    unfolding ["hmac_update_c_state"];
    simplify(cryptol_ss ());
    simplify (addsimp' hash_lemma2 empty_ss);
    unint_yices ["hash_update_c_state"];
}) {{ hmac_update_empty }});