val lemma_gf128_degree (_:unit) : Lemma
  (ensures
    degree gf128_modulus_low_terms == 7 /\
    degree (monomial 128) == 128 /\
    degree gf128_modulus == 128
  )
let lemma_gf128_degree () =
  lemma_add_define_all ();
  lemma_monomial_define 128;
  lemma_degree_is gf128_modulus_low_terms 7;
  lemma_degree_is (monomial 128) 128;
  lemma_degree_is gf128_modulus 128;
  ()
val lemma_gf128_degree (_:unit) : Lemma
  (ensures
    degree gf128_modulus_low_terms == 7 /\
    degree (monomial 128) == 128 /\
    degree gf128_modulus == 128
  )
let lemma_gf128_degree () =
lemma_add_define_all ();
lemma_monomial_define 128;
lemma_degree_is gf128_modulus_low_terms 7;
lemma_degree_is (monomial 128) 128;
lemma_degree_is gf128_modulus 128;
()
Vale.AES.GF128.fst.checked
Vale.Math.Poly2.Bits.fsti.checked Vale.Arch.TypesNative.fsti.checked Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Calc.fsti.checked
Vale.AES.GF128.fst
Prims.unit Vale.Math.Poly2.Lemmas.lemma_degree_is Vale.AES.GF128_s.gf128_modulus Vale.Math.Poly2_s.monomial Vale.AES.GF128_s.gf128_modulus_low_terms Vale.Math.Poly2.Lemmas.lemma_monomial_define Vale.Math.Poly2.Lemmas.lemma_add_define_all
module Vale.AES.GF128
open FStar.Mul
open Vale.Arch.TypesNative
open Vale.Math.Poly2.Bits

#reset-options "--z3rlimit 20"
let lemma_shift_left_1 a =
  reveal_to_quad32 a;
  reveal_to_quad32 (shift a 1);
  lemma_zero_nth 32;
  lemma_ishl_nth_all 32;
  lemma_ishr_nth_all 32;
  lemma_ixor_nth_all 32;
  lemma_index_all ();
  lemma_shift_define a 1;
  lemma_reverse_define_all ();
  quad32_xor_reveal ();
  reverse_bytes_nat32_reveal ();
  lemma_quad32_vec_equal (to_quad32 (shift a 1)) (quad32_shift_left_1 (to_quad32 a));
  ()

let lemma_shift_2_left_1 lo hi =
  let n = monomial 128 in
  let a = hi *. n +. lo in
  let a' = shift a 1 in
  let (qlo', qhi') = quad32_shift_2_left_1 (to_quad32 lo) (to_quad32 hi) in
  reveal_to_quad32 lo;
  reveal_to_quad32 hi;
  reveal_to_quad32 (a' %. n);
  reveal_to_quad32 (a' /. n);
  lemma_zero_nth 32;
  lemma_ishl_nth_all 32;
  lemma_ishr_nth_all 32;
  lemma_ixor_nth_all 32;
  lemma_index_all ();
  lemma_shift_define a 1;
  lemma_add_define_all ();
  lemma_reverse_define_all ();
  lemma_div_mod a' n;
  lemma_shift_is_mul hi 128;
  lemma_shift_define hi 128;
  lemma_shift_is_mul (a' /. n) 128;
  let lemma_lo () : Lemma (qlo' == to_quad32 (a' %. n)) =
    lemma_shift_define (a' /. n) 128;
    quad32_xor_reveal ();
    reverse_bytes_nat32_reveal ();
    lemma_quad32_vec_equal qlo' (to_quad32 (a' %. n))
    in
  let lemma_hi () : Lemma (qhi' == to_quad32 (a' /. n)) =
    lemma_shift_define_forward (a' /. n) 128;
    quad32_xor_reveal ();
    reverse_bytes_nat32_reveal ();
    lemma_quad32_vec_equal qhi' (to_quad32 (a' /. n))
    in
  lemma_lo ();
  lemma_hi ();
  ()
#reset-options

let lemma_reverse_reverse a n =
  lemma_reverse_define_all ();
  lemma_index_all ();
  lemma_equal a (reverse (reverse a n) n)
val lemma_gf128_degree (_:unit) : Lemma
  (ensures
    degree gf128_modulus_low_terms == 7 /\
    degree (monomial 128) == 128 /\
    degree gf128_modulus == 128
  )
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      Vale.Math.Poly2_s.degree Vale.AES.GF128_s.gf128_modulus_low_terms == 7 /\
      Vale.Math.Poly2_s.degree (Vale.Math.Poly2_s.monomial 128) == 128 /\
      Vale.Math.Poly2_s.degree Vale.AES.GF128_s.gf128_modulus == 128)