val lemma_reverse_reverse (a:poly) (n:nat) : Lemma
  (requires degree a <= n)
  (ensures reverse (reverse a n) n == a)
  [SMTPat (reverse (reverse a n) n)]
let lemma_reverse_reverse a n =
  lemma_reverse_define_all ();
  lemma_index_all ();
  lemma_equal a (reverse (reverse a n) n)
val lemma_reverse_reverse (a:poly) (n:nat) : Lemma
  (requires degree a <= n)
  (ensures reverse (reverse a n) n == a)
  [SMTPat (reverse (reverse a n) n)]
let lemma_reverse_reverse a n =
lemma_reverse_define_all ();
lemma_index_all ();
lemma_equal a (reverse (reverse a n) n)
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 Prims.nat Vale.Math.Poly2.lemma_equal Vale.Math.Poly2_s.reverse Prims.unit Vale.Math.Poly2.Lemmas.lemma_index_all Vale.Math.Poly2.Lemmas.lemma_reverse_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
val lemma_reverse_reverse (a:poly) (n:nat) : Lemma
  (requires degree a <= n)
  (ensures reverse (reverse a n) n == a)
  [SMTPat (reverse (reverse a n) n)]
a: Vale.Math.Poly2_s.poly -> n: Prims.nat
  -> FStar.Pervasives.Lemma (requires Vale.Math.Poly2_s.degree a <= n)
      (ensures Vale.Math.Poly2_s.reverse (Vale.Math.Poly2_s.reverse a n) n == a)
      [SMTPat (Vale.Math.Poly2_s.reverse (Vale.Math.Poly2_s.reverse a n) n)]