val lemma_shift_2_left_1 (lo hi:poly) : Lemma
  (requires degree hi < 127 /\ degree lo < 128)
  (ensures (
    let n = monomial 128 in
    let a = hi *. n +. lo in
    let a' = shift a 1 in
    let (lo', hi') = quad32_shift_2_left_1 (to_quad32 lo) (to_quad32 hi) in
    lo' == to_quad32 (a' %. n) /\
    hi' == to_quad32 (a' /. n)
  ))
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 ();
  ()
val lemma_shift_2_left_1 (lo hi:poly) : Lemma
  (requires degree hi < 127 /\ degree lo < 128)
  (ensures (
    let n = monomial 128 in
    let a = hi *. n +. lo in
    let a' = shift a 1 in
    let (lo', hi') = quad32_shift_2_left_1 (to_quad32 lo) (to_quad32 hi) in
    lo' == to_quad32 (a' %. n) /\
    hi' == to_quad32 (a' /. n)
  ))
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 ();
()
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.Def.Types_s.quad32 Prims.unit Prims.l_True Prims.squash Prims.eq2 Vale.Math.Poly2.Bits_s.to_quad32 Vale.Math.Poly2_s.div Prims.Nil FStar.Pervasives.pattern Vale.Arch.TypesNative.lemma_quad32_vec_equal Vale.Math.Poly2.op_Slash_Dot Vale.Def.Types_s.reverse_bytes_nat32_reveal Vale.Def.Types_s.quad32_xor_reveal Vale.Math.Poly2.Lemmas.lemma_shift_define_forward Vale.Math.Poly2_s.mod Vale.Math.Poly2.op_Percent_Dot Vale.Math.Poly2.Lemmas.lemma_shift_define Vale.Math.Poly2.lemma_shift_is_mul Vale.Math.Poly2.lemma_div_mod Vale.Math.Poly2.Lemmas.lemma_reverse_define_all Vale.Math.Poly2.Lemmas.lemma_add_define_all 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 FStar.Pervasives.Native.tuple2 Vale.AES.GF128.quad32_shift_2_left_1 Vale.Math.Poly2_s.shift Vale.Math.Poly2.op_Plus_Dot Vale.Math.Poly2.op_Star_Dot Vale.Math.Poly2_s.monomial
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));
  ()
val lemma_shift_2_left_1 (lo hi:poly) : Lemma
  (requires degree hi < 127 /\ degree lo < 128)
  (ensures (
    let n = monomial 128 in
    let a = hi *. n +. lo in
    let a' = shift a 1 in
    let (lo', hi') = quad32_shift_2_left_1 (to_quad32 lo) (to_quad32 hi) in
    lo' == to_quad32 (a' %. n) /\
    hi' == to_quad32 (a' /. n)
  ))
lo: Vale.Math.Poly2_s.poly -> hi: Vale.Math.Poly2_s.poly
  -> FStar.Pervasives.Lemma
      (requires Vale.Math.Poly2_s.degree hi < 127 /\ Vale.Math.Poly2_s.degree lo < 128)
      (ensures
        (let n = Vale.Math.Poly2_s.monomial 128 in
          let a = hi *. n +. lo in
          let a' = Vale.Math.Poly2_s.shift a 1 in
          let _ =
            Vale.AES.GF128.quad32_shift_2_left_1 (Vale.Math.Poly2.Bits_s.to_quad32 lo)
              (Vale.Math.Poly2.Bits_s.to_quad32 hi)
          in
          (let FStar.Pervasives.Native.Mktuple2 #_ #_ lo' hi' = _ in
            lo' == Vale.Math.Poly2.Bits_s.to_quad32 (a' %. n) /\
            hi' == Vale.Math.Poly2.Bits_s.to_quad32 (a' /. n))
          <:
          Type0))