val lemma_shift_left_1 (a:poly) : Lemma
  (requires degree a < 128)
  (ensures to_quad32 (shift a 1) == quad32_shift_left_1 (to_quad32 a))
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));
  ()
val lemma_shift_left_1 (a:poly) : Lemma
  (requires degree a < 128)
  (ensures to_quad32 (shift a 1) == quad32_shift_left_1 (to_quad32 a))
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));
()
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.unit Vale.Arch.TypesNative.lemma_quad32_vec_equal Vale.Math.Poly2.Bits_s.to_quad32 Vale.Math.Poly2_s.shift Vale.AES.GF128.quad32_shift_left_1 Vale.Def.Types_s.reverse_bytes_nat32_reveal Vale.Def.Types_s.quad32_xor_reveal Vale.Math.Poly2.Lemmas.lemma_reverse_define_all Vale.Math.Poly2.Lemmas.lemma_shift_define Vale.Math.Poly2.Lemmas.lemma_index_all Vale.Arch.TypesNative.lemma_ixor_nth_all Vale.Arch.TypesNative.lemma_ishr_nth_all Vale.Arch.TypesNative.lemma_ishl_nth_all Vale.Arch.TypesNative.lemma_zero_nth Vale.Math.Poly2.Bits_s.reveal_to_quad32
module Vale.AES.GF128
open FStar.Mul
open Vale.Arch.TypesNative
open Vale.Math.Poly2.Bits

#reset-options "--z3rlimit 20"
val lemma_shift_left_1 (a:poly) : Lemma
  (requires degree a < 128)
  (ensures to_quad32 (shift a 1) == quad32_shift_left_1 (to_quad32 a))
a: Vale.Math.Poly2_s.poly
  -> FStar.Pervasives.Lemma (requires Vale.Math.Poly2_s.degree a < 128)
      (ensures
        Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.shift a 1) ==
        Vale.AES.GF128.quad32_shift_left_1 (Vale.Math.Poly2.Bits_s.to_quad32 a))