val lemma_quad32_double_hi_rev (a:poly) : Lemma
  (requires degree a <= 127 /\ degree (reverse a 127) <= 63)
  (ensures of_double32 (quad32_double_hi (to_quad32 a)) == reverse (reverse a 127) 63)
let lemma_quad32_double_hi_rev a =
  let ra = reverse a 127 in
  lemma_split_define ra 64;
  lemma_split_define_forward a 64;
  lemma_index_all ();
  lemma_add_define_all ();
  lemma_reverse_define_all ();
  lemma_equal (a /. monomial 64) (reverse ra 63);
  lemma_quad32_double a
val lemma_quad32_double_hi_rev (a:poly) : Lemma
  (requires degree a <= 127 /\ degree (reverse a 127) <= 63)
  (ensures of_double32 (quad32_double_hi (to_quad32 a)) == reverse (reverse a 127) 63)
let lemma_quad32_double_hi_rev a =
let ra = reverse a 127 in
lemma_split_define ra 64;
lemma_split_define_forward a 64;
lemma_index_all ();
lemma_add_define_all ();
lemma_reverse_define_all ();
lemma_equal (a /. monomial 64) (reverse ra 63);
lemma_quad32_double a
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
Vale.Math.Poly2_s.poly Vale.Math.Poly2.Bits.lemma_quad32_double Prims.unit Vale.Math.Poly2.lemma_equal Vale.Math.Poly2.op_Slash_Dot Vale.Math.Poly2_s.monomial Vale.Math.Poly2_s.reverse Vale.Math.Poly2.Lemmas.lemma_reverse_define_all Vale.Math.Poly2.Lemmas.lemma_add_define_all Vale.Math.Poly2.Lemmas.lemma_index_all Vale.Math.Poly2.Lemmas.lemma_split_define_forward Vale.Math.Poly2.Lemmas.lemma_split_define
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)

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;
  ()

let lemma_gf128_constant_rev q =
  let n0:nat32 = 0 in
  let n1:nat32 = 0 in
  let n2:nat32 = 0 in
  let n3:nat32 = 0xe1000000 in
  calc (==) {
    Mkfour n0 n1 n2 n3;
    == {lemma_quad32_of_nat32s n0 n1 n2 n3}
    to_quad32 (poly128_of_nat32s n0 n1 n2 n3);
    == {
      lemma_bitwise_all ();
      lemma_to_nat 32 (reverse gf128_modulus_low_terms 31) 0xe1000000;
      lemma_equal (poly128_of_nat32s n0 n1 n2 n3) (reverse gf128_modulus_low_terms 127)
    }
    to_quad32 (reverse gf128_modulus_low_terms 127);
  };
  Vale.Arch.Types.lemma_quad32_xor ()
val lemma_quad32_double_hi_rev (a:poly) : Lemma
  (requires degree a <= 127 /\ degree (reverse a 127) <= 63)
  (ensures of_double32 (quad32_double_hi (to_quad32 a)) == reverse (reverse a 127) 63)
a: Vale.Math.Poly2_s.poly
  -> FStar.Pervasives.Lemma
      (requires
        Vale.Math.Poly2_s.degree a <= 127 /\
        Vale.Math.Poly2_s.degree (Vale.Math.Poly2_s.reverse a 127) <= 63)
      (ensures
        Vale.Math.Poly2.Bits_s.of_double32 (Vale.Arch.Types.quad32_double_hi (Vale.Math.Poly2.Bits_s.to_quad32
                  a)) ==
        Vale.Math.Poly2_s.reverse (Vale.Math.Poly2_s.reverse a 127) 63)