val lemma_ghash_incremental_poly_rec (h_LE y_prev: quad32) (x: seq quad32) (data: (int -> poly128))
    : Lemma
      (requires
        (forall (i: int). {:pattern data i\/index x i}
            0 <= i && i < length x ==> data i == of_quad32 (reverse_bytes_quad32 (index x i))))
      (ensures
        of_quad32 (reverse_bytes_quad32 (ghash_incremental_def h_LE y_prev x)) ==
        ghash_poly (of_quad32 (reverse_bytes_quad32 h_LE))
          (of_quad32 (reverse_bytes_quad32 y_prev))
          data
          0
          (length x))
      (decreases (length x))
let rec lemma_ghash_incremental_poly_rec (h_LE:quad32) (y_prev:quad32) (x:seq quad32) (data:int -> poly128) : Lemma
  (requires
    (forall (i:int).{:pattern data i \/ index x i} 0 <= i && i < length x ==>
      data i == of_quad32 (reverse_bytes_quad32 (index x i)))
  )
  (ensures
    of_quad32 (reverse_bytes_quad32 (ghash_incremental_def h_LE y_prev x)) ==
    ghash_poly (of_quad32 (reverse_bytes_quad32 h_LE)) (of_quad32 (reverse_bytes_quad32 y_prev)) data 0 (length x)
  )
  (decreases (length x))
  =
  ghash_incremental_reveal ();
  let (~~) = of_quad32 in
  let (!!) = reverse_bytes_quad32 in
  let (~!) x = ~~(!!x) in
  let h = ~!h_LE in
  let prev = ~!y_prev in
  let m = length x in
  if m > 0 then
    let y_i_minus_1 = ghash_incremental_def h_LE y_prev (all_but_last x) in
    let x_i = last x in
    let xor_LE = quad32_xor y_i_minus_1 x_i in
    let g = gf128_modulus in
    calc (==) {
      ~!(ghash_incremental_def h_LE y_prev x);
      == {}
      ~!(gf128_mul_LE xor_LE h_LE);
      == {lemma_of_to_quad32 (~!xor_LE *~ h)}
      ~!xor_LE *~ h;
      == {calc (==) {
        ~!(quad32_xor y_i_minus_1 x_i);
        == {lemma_reverse_bytes_quad32_xor y_i_minus_1 x_i}
        ~~(quad32_xor !!y_i_minus_1 !!x_i);
        == {lemma_add_quad32 !!y_i_minus_1 !!x_i}
        ~!y_i_minus_1 +. ~!x_i;
      }}
      (~!y_i_minus_1 +. ~!x_i) *~ h;
      == {lemma_ghash_incremental_poly_rec h_LE y_prev (all_but_last x) data}
      (ghash_poly h prev data 0 (m - 1) +. data (m - 1)) *~ h;
      == {}
      ghash_poly h prev data 0 m;
    }
val lemma_ghash_incremental_poly_rec (h_LE y_prev: quad32) (x: seq quad32) (data: (int -> poly128))
    : Lemma
      (requires
        (forall (i: int). {:pattern data i\/index x i}
            0 <= i && i < length x ==> data i == of_quad32 (reverse_bytes_quad32 (index x i))))
      (ensures
        of_quad32 (reverse_bytes_quad32 (ghash_incremental_def h_LE y_prev x)) ==
        ghash_poly (of_quad32 (reverse_bytes_quad32 h_LE))
          (of_quad32 (reverse_bytes_quad32 y_prev))
          data
          0
          (length x))
      (decreases (length x))
let rec lemma_ghash_incremental_poly_rec
      (h_LE y_prev: quad32)
      (x: seq quad32)
      (data: (int -> poly128))
    : Lemma
      (requires
        (forall (i: int). {:pattern data i\/index x i}
            0 <= i && i < length x ==> data i == of_quad32 (reverse_bytes_quad32 (index x i))))
      (ensures
        of_quad32 (reverse_bytes_quad32 (ghash_incremental_def h_LE y_prev x)) ==
        ghash_poly (of_quad32 (reverse_bytes_quad32 h_LE))
          (of_quad32 (reverse_bytes_quad32 y_prev))
          data
          0
          (length x))
      (decreases (length x)) =
ghash_incremental_reveal ();
let ( ~~ ) = of_quad32 in
let ( !! ) = reverse_bytes_quad32 in
let op_Tilde_Bang x = ~~(!!x) in
let h = ~!h_LE in
let prev = ~!y_prev in
let m = length x in
if m > 0
then
  let y_i_minus_1 = ghash_incremental_def h_LE y_prev (all_but_last x) in
  let x_i = last x in
  let xor_LE = quad32_xor y_i_minus_1 x_i in
  let g = gf128_modulus in
  calc ( == ) {
    ~!(ghash_incremental_def h_LE y_prev x);
    ( == ) { () }
    ~!(gf128_mul_LE xor_LE h_LE);
    ( == ) { lemma_of_to_quad32 (~!xor_LE *~ h) }
    ~!xor_LE *~ h;
    ( == ) { calc ( == ) {
      ~!(quad32_xor y_i_minus_1 x_i);
      ( == ) { lemma_reverse_bytes_quad32_xor y_i_minus_1 x_i }
      ~~(quad32_xor !!y_i_minus_1 !!x_i);
      ( == ) { lemma_add_quad32 !!y_i_minus_1 !!x_i }
      ~!y_i_minus_1 +. ~!x_i;
    } }
    (~!y_i_minus_1 +. ~!x_i) *~ h;
    ( == ) { lemma_ghash_incremental_poly_rec h_LE y_prev (all_but_last x) data }
    (ghash_poly h prev data 0 (m - 1) +. data (m - 1)) *~ h;
    ( == ) { () }
    ghash_poly h prev data 0 m;
  }
Vale.AES.GHash.fst.checked
Vale.Math.Poly2.Words.fsti.checked Vale.Math.Poly2.Lemmas.fsti.checked Vale.Math.Bits.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Arch.TypesNative.fsti.checked Vale.AES.OptPublic.fst.checked prims.fst.checked FStar.UInt.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked FStar.BV.fsti.checked
Vale.AES.GHash.fst
Vale.Def.Types_s.quad32 FStar.Seq.Base.seq Prims.int Vale.AES.GHash.poly128 Prims.op_GreaterThan FStar.Calc.calc_finish Vale.Math.Poly2_s.poly Prims.eq2 Vale.AES.GHash.ghash_incremental_def Vale.AES.GHash.ghash_poly Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Vale.AES.GF128.op_Star_Tilde Vale.Math.Poly2.op_Plus_Dot Prims.op_Subtraction Vale.AES.GHash_s.gf128_mul_LE FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Vale.Math.Poly2.Bits.lemma_of_to_quad32 Vale.Def.Types_s.quad32_xor Vale.AES.GHash.lemma_reverse_bytes_quad32_xor Vale.Math.Poly2.Words.lemma_add_quad32 Vale.AES.GHash.lemma_ghash_incremental_poly_rec Vale.Lib.Seqs_s.all_but_last Vale.AES.GF128_s.gf128_modulus FStar.Seq.Properties.last Prims.bool Prims.nat FStar.Seq.Base.length Vale.Def.Types_s.reverse_bytes_quad32 Vale.Math.Poly2.Bits_s.of_quad32 Vale.AES.GHash.ghash_incremental_reveal Prims.l_Forall Prims.l_imp Prims.b2t Prims.op_AmpAmp Prims.op_LessThanOrEqual Prims.op_LessThan FStar.Seq.Base.index FStar.Pervasives.pattern
module Vale.AES.GHash
open FStar.Mul
open Vale.Math.Poly2.Lemmas
open Vale.Math.Poly2.Words

friend Vale.AES.OptPublic

#reset-options

let shift_gf128_key_1 (h:poly) : poly =
  shift_key_1 128 gf128_modulus_low_terms h

let rec g_power (a:poly) (n:nat) : poly =
  if n = 0 then zero else // arbitrary value for n = 0
  if n = 1 then a else
  a *~ g_power a (n - 1)

let lemma_g_power_1 a = ()
let lemma_g_power_n a n = ()

let gf128_power h n = shift_gf128_key_1 (g_power h n)
let lemma_gf128_power h n = ()

let rec ghash_poly_unroll (h:poly) (prev:poly) (data:int -> poly128) (k:int) (m n:nat) : poly =
  let d = data (k + m) in
  let p = g_power h (n + 1) in
  if m = 0 then (prev +. d) *~ p else
  ghash_poly_unroll h prev data k (m - 1) (n + 1) +. d *~ p

let lemma_hkeys_reqs_pub_priv (hkeys:seq quad32) (h_BE:quad32) : Lemma
  (hkeys_reqs_pub hkeys h_BE <==> hkeys_reqs_priv hkeys h_BE)
  =
  ()

let rec lemma_ghash_unroll_back_forward_rec (h:poly) (prev:poly) (data:int -> poly128) (k:int) (n m:nat) : Lemma
  (requires m < n)
  (ensures ghash_unroll h prev data k n 0 ==
    ghash_unroll h prev data k (n - 1 - m) (m + 1) +. ghash_unroll_back h prev data k (n + 1) m)
  =
  lemma_add_all ();
  if m > 0 then lemma_ghash_unroll_back_forward_rec h prev data k n (m - 1)

let lemma_ghash_unroll_back_forward (h:poly) (prev:poly) (data:int -> poly128) (k:int) (n:nat) : Lemma
  (ghash_unroll h prev data k n 0 == ghash_unroll_back h prev data k (n + 1) n)
  =
  lemma_add_all ();
  if n > 0 then lemma_ghash_unroll_back_forward_rec h prev data k n (n - 1)

let lemma_gf128_mul_rev_mod_rev (a h:poly) : Lemma
  (requires degree a < 128 /\ degree h < 128)
  (ensures gf128_mul_rev a h == mod_rev 128 (a *. shift_gf128_key_1 h) gf128_modulus)
  =
  let h1 = shift_gf128_key_1 h in
  let rev x = reverse x 127 in
  let g = gf128_modulus in
  lemma_gf128_degree ();
  calc (==) {
    // gf128_mul_rev a h
    rev ((rev a *. rev h) %. g);
    == {lemma_mod_mul_mod_right (rev a) (rev h) g}
    rev ((rev a *. (rev h %. g)) %. g);
    == {lemma_shift_key_1 128 gf128_modulus_low_terms h}
    rev ((rev a *. (shift (rev h1) 1 %. g)) %. g);
    == {lemma_mod_mul_mod_right (rev a) (shift (rev h1) 1) g}
    rev ((rev a *. (shift (rev h1) 1)) %. g);
    == {lemma_shift_is_mul (rev h1) 1}
    rev ((rev a *. (rev h1 *. monomial 1)) %. g);
    == {lemma_mul_all ()}
    rev (((rev a *. rev h1) *. monomial 1) %. g);
    == {lemma_shift_is_mul (rev a *. rev h1) 1}
    rev (shift (rev a *. rev h1) 1 %. g);
    == {lemma_mul_reverse_shift_1 a h1 127}
    rev (reverse (a *. h1) 255 %. g);
  }

let rec lemma_ghash_poly_degree h init data j k =
  if k > j then lemma_ghash_poly_degree h init data j (k - 1)

let rec lemma_ghash_poly_unroll_n (h:poly) (prev:poly) (data:int -> poly128) (k:int) (m n:nat) : Lemma
  (ghash_poly_unroll h prev data k m (n + 1) == ghash_poly_unroll h prev data k m n *~ h)
  =
  let d = data (k + m) in
  let p0 = g_power h (n + 1) in
  let p1 = g_power h (n + 2) in
  if m = 0 then
    calc (==) {
      ghash_poly_unroll h prev data k m (n + 1);
      == {}
      (prev +. d) *~ p1;
      == {}
      (prev +. d) *~ (h *~ p0);
      == {lemma_gf128_mul_rev_commute p0 h}
      (prev +. d) *~ (p0 *~ h);
      == {lemma_gf128_mul_rev_associate (prev +. d) p0 h}
      ((prev +. d) *~ p0) *~ h;
      == {}
      ghash_poly_unroll h prev data k m n *~ h;
    }
  else
    let ghash0 = ghash_poly_unroll h prev data k (m - 1) (n + 1) in
    let ghash1 = ghash_poly_unroll h prev data k (m - 1) (n + 2) in
    calc (==) {
      ghash_poly_unroll h prev data k m (n + 1);
      == {}
      ghash1 +. d *~ p1;
      == {lemma_ghash_poly_unroll_n h prev data k (m - 1) (n + 1)}
      ghash0 *~ h +. d *~ p1;
      == {}
      ghash0 *~ h +. d *~ (h *~ p0);
      == {lemma_gf128_mul_rev_commute p0 h}
      ghash0 *~ h +. d *~ (p0 *~ h);
      == {lemma_gf128_mul_rev_associate d p0 h}
      ghash0 *~ h +. (d *~ p0) *~ h;
      == {lemma_gf128_mul_rev_distribute_left ghash0 (d *~ p0) h}
      (ghash0 +. d *~ p0) *~ h;
      == {}
      ghash_poly_unroll h prev data k m n *~ h;
    }

let rec lemma_ghash_poly_unroll (h0:poly) (prev:poly) (data:int -> poly128) (k:int) (m:nat) : Lemma
  (requires degree h0 < 128 /\ degree prev < 128)
  (ensures ghash_poly_unroll h0 prev data k m 0 == ghash_poly h0 prev data k (k + m + 1))
  =
  let d = data (k + m) in
  let p1 = g_power h0 1 in
  let ghash0 = ghash_poly h0 prev data k (k + m) in
  if m = 0 then
    calc (==) {
      ghash_poly_unroll h0 prev data k m 0;
      == {}
      (prev +. d) *~ p1;
      == {}
      (ghash0 +. d) *~ h0;
      == {}
      ghash_poly h0 prev data k (k + m + 1);
    }
  else
    let unroll0 = ghash_poly_unroll h0 prev data k (m - 1) 0 in
    let unroll1 = ghash_poly_unroll h0 prev data k (m - 1) 1 in
    calc (==) {
      ghash_poly_unroll h0 prev data k m 0;
      == {}
      unroll1 +. d *~ p1;
      == {
        calc (==) {
          unroll1;
          == {lemma_ghash_poly_unroll_n h0 prev data k (m - 1) 0}
          unroll0 *~ h0;
          == {lemma_ghash_poly_unroll h0 prev data k (m - 1)}
          ghash0 *~ h0;
        }
      }
      ghash0 *~ h0 +. d *~ h0;
      == {lemma_gf128_mul_rev_distribute_left ghash0 d h0}
      (ghash0 +. d) *~ h0;
      == {}
      ghash_poly h0 prev data k (k + m + 1);
    }

let rec lemma_ghash_unroll_poly_unroll (h:poly) (prev:poly) (data:int -> poly128) (k:int) (m n:nat) : Lemma
  (requires degree h < 128 /\ degree prev < 128)
  (ensures
    mod_rev 128 (ghash_unroll h prev data k m n) gf128_modulus ==
    ghash_poly_unroll h prev data k m n
  )
  =
  let g = gf128_modulus in
  let d = data (k + m) in
  let p = g_power h (n + 1) in
  let sp = shift_gf128_key_1 p in
  lemma_gf128_degree ();
  if m = 0 then
    calc (==) {
      mod_rev 128 (ghash_unroll h prev data k m n) g;
      == {}
      mod_rev 128 ((prev +. d) *. sp) g;
      == {lemma_gf128_mul_rev_mod_rev (prev +. d) p}
      (prev +. d) *~ p;
      == {}
      ghash_poly_unroll h prev data k m n;
    }
  else
    let unroll1 = ghash_unroll h prev data k (m - 1) (n + 1) in
    let ghash0 = ghash_poly_unroll h prev data k (m - 1) (n + 1) in
    calc (==) {
      mod_rev 128 (ghash_unroll h prev data k m n) g;
      == {}
      mod_rev 128 (unroll1 +. d *. sp) g;
      == {lemma_add_mod_rev 128 unroll1 (d *. sp) g}
      mod_rev 128 unroll1 g +. mod_rev 128 (d *. sp) g;
      == {lemma_ghash_unroll_poly_unroll h prev data k (m - 1) (n + 1)}
      ghash0 +. mod_rev 128 (d *. sp) g;
      == {lemma_gf128_mul_rev_mod_rev d p}
      ghash0 +. d *~ p;
      == {}
      ghash_poly_unroll h prev data k m n;
    }

let lemma_ghash_poly_of_unroll h prev data k m =
  lemma_ghash_poly_unroll h prev data k m;
  lemma_ghash_unroll_poly_unroll h prev data k m 0;
  ()

// TODO:
// The spec for ghash_LE_def should be rewritten in a more endian-consistent style.
// Right now, it performs the gf128_mul on BE (forward) values but performs the quad32_xor
// on LE (backwards) values.  Xor is endianness-neutral, so it's still correct, but
// it forces us to either insert extra byte reversals into the implementation (see the two
// Pshufb operations in ReduceMul128_LE) or to prove this otherwise-unnecessary lemma:
#reset-options "--z3rlimit 20"
let lemma_reverse_bytes_quad32_xor (a b:quad32) : Lemma
  (reverse_bytes_quad32 (quad32_xor a b) == quad32_xor (reverse_bytes_quad32 a) (reverse_bytes_quad32 b))
  =
  let open Vale.Def.Words.Four_s in
  let open FStar.UInt in
  let open FStar.BV in
  let open Vale.Math.Bits in
  let (!!) = reverse_bytes_quad32 in
  let r32 = reverse_bytes_nat32 in
  let mk4 (x0 x1 x2 x3:nat8) : nat32 = four_to_nat 8 (Mkfour x0 x1 x2 x3) in
  let mk4n (x0 x1 x2 x3:nat8) : nat32 = x0 + x1 * 0x100 + x2 * 0x10000 + x3 * 0x1000000 in
  let mk4m (x0 x1 x2 x3:nat8) : nat32 = add_hide #32 x0 (add_hide #32 (mul_hide #32 x1 0x100) (add_hide #32 (mul_hide #32 x2 0x10000) (mul_hide #32 x3 0x1000000))) in
  let mk4b (x0 x1 x2 x3:bv_t 32) : bv_t 32 = b_add x0 (b_add (b_mul x1 0x100) (b_add (b_mul x2 0x10000) (b_mul x3 0x1000000))) in
  let lemma_mk4_mk4m (a0 a1 a2 a3:nat8) : Lemma
    (mk4 a0 a1 a2 a3 == mk4m a0 a1 a2 a3)
    =
    assert_norm (mk4 a0 a1 a2 a3 == mk4n a0 a1 a2 a3);
    assert_norm (mk4m a0 a1 a2 a3 == mk4n a0 a1 a2 a3)
    in
  let lemma_small_logxor_32_8 (a b:nat8) : Lemma (logxor #32 a b < 0x100) =
    lemma_to_is_bv8 a;
    lemma_to_is_bv8 b;
    let va = b_i2b #32 a in
    let vb = b_i2b #32 b in
    assert_norm (is_bv8 va /\ is_bv8 vb ==> b_xor va vb == b_and (b_xor va vb) (b_i2b 0xff));
    lemma_i2b_equal (logxor #32 a b) (logand (logxor #32 a b) 0xff);
    logand_le (logxor #32 a b) 0xff
    in
  let lemma_small_nat32_xor_32_8 (a b:nat8) : Lemma (nat32_xor a b < 0x100) =
    Vale.Arch.TypesNative.reveal_ixor_all 32;
    lemma_small_logxor_32_8 a b
    in
  let lemma_small_logxor_32_8 : squash (forall (a b:nat8).{:pattern (logxor #32 a b)} logxor #32 a b < 0x100) =
    // FStar.Classical.forall_intro_2_with_pat didn't work; TODO: use new non-top-level SMTPat feature
    FStar.Classical.forall_intro_2 lemma_small_logxor_32_8
    in
  let lemma_small_logxor_32_8 : squash (forall (a b:nat8).{:pattern (nat32_xor a b)} nat32_xor a b < 0x100) =
    FStar.Classical.forall_intro_2 lemma_small_nat32_xor_32_8
    in
  let lemma_xor_mk4b (a0 a1 a2 a3 b0 b1 b2 b3:bv_t 32) : Lemma
    (requires
      is_bv8 a0 /\ is_bv8 a1 /\ is_bv8 a2 /\ is_bv8 a3 /\
      is_bv8 b0 /\ is_bv8 b1 /\ is_bv8 b2 /\ is_bv8 b3
    )
    (ensures
      b_xor (mk4b a0 a1 a2 a3) (mk4b b0 b1 b2 b3) ==
      mk4b (b_xor a0 b0) (b_xor a1 b1) (b_xor a2 b2) (b_xor a3 b3)
    )
    =
    let fact1 =
      is_bv8 a0 /\ is_bv8 a1 /\ is_bv8 a2 /\ is_bv8 a3 /\
      is_bv8 b0 /\ is_bv8 b1 /\ is_bv8 b2 /\ is_bv8 b3
      in
    // This turns out to be too slow:
    // assert_norm (fact1 ==> bvxor (mk4b a0 a1 a2 a3) (mk4b b0 b1 b2 b3) == mk4b (bvxor a0 b0) (bvxor a1 b1) (bvxor a2 b2) (bvxor a3 b3));
    let a = mk4b a0 a1 a2 a3 in
    let b = mk4b b0 b1 b2 b3 in
    assert_norm (fact1 ==> b_and (b_xor a b) (b_i2b 0x000000ff) ==        b_xor a0 b0);
    assert_norm (fact1 ==> b_and (b_xor a b) (b_i2b 0x0000ff00) == b_shl (b_xor a1 b1) 8);
    assert_norm (fact1 ==> b_and (b_xor a b) (b_i2b 0x00ff0000) == b_shl (b_xor a2 b2) 16);
    assert_norm (fact1 ==> b_and (b_xor a b) (b_i2b 0xff000000) == b_shl (b_xor a3 b3) 24);
    let f_pre (x x0 x1 x2 x3:bv_t 32) =
      b_and x (b_i2b 0x000000ff) ==       x0 /\
      b_and x (b_i2b 0x0000ff00) == b_shl x1 8 /\
      b_and x (b_i2b 0x00ff0000) == b_shl x2 16 /\
      b_and x (b_i2b 0xff000000) == b_shl x3 24
      in
    let f (x x0 x1 x2 x3:bv_t 32) : Lemma
      (requires f_pre x x0 x1 x2 x3)
      (ensures bveq x (mk4b x0 x1 x2 x3))
      =
      assert_norm (f_pre x x0 x1 x2 x3 ==> bveq x (mk4b x0 x1 x2 x3))
    in
    f (b_xor a b) (b_xor a0 b0) (b_xor a1 b1) (b_xor a2 b2) (b_xor a3 b3);
    lemma_bveq (b_xor a b) (mk4b (b_xor a0 b0) (b_xor a1 b1) (b_xor a2 b2) (b_xor a3 b3));
    ()
    in
  let lemma_logxor_4_nat8 (a0 a1 a2 a3 b0 b1 b2 b3:nat8) : Lemma
    (logxor #32 (mk4m a0 a1 a2 a3) (mk4m b0 b1 b2 b3) == mk4m (logxor #32 a0 b0) (logxor #32 a1 b1) (logxor #32 a2 b2) (logxor #32 a3 b3))
    =
    lemma_to_is_bv8 a0;
    lemma_to_is_bv8 a1;
    lemma_to_is_bv8 a2;
    lemma_to_is_bv8 a3;
    lemma_to_is_bv8 b0;
    lemma_to_is_bv8 b1;
    lemma_to_is_bv8 b2;
    lemma_to_is_bv8 b3;
    lemma_xor_mk4b (b_i2b a0) (b_i2b a1) (b_i2b a2) (b_i2b a3) (b_i2b b0) (b_i2b b1) (b_i2b b2) (b_i2b b3);
    lemma_i2b_equal
      (logxor #32 (mk4m a0 a1 a2 a3) (mk4m b0 b1 b2 b3))
      (mk4m (logxor #32 a0 b0) (logxor #32 a1 b1) (logxor #32 a2 b2) (logxor #32 a3 b3))
    in
  let lemma_xor_4_nat8_n (a0 a1 a2 a3 b0 b1 b2 b3:nat8) : Lemma
    (nat32_xor (mk4m a0 a1 a2 a3) (mk4m b0 b1 b2 b3) == mk4m (nat32_xor a0 b0) (nat32_xor a1 b1) (nat32_xor a2 b2) (nat32_xor a3 b3))
    =
    Vale.Arch.TypesNative.reveal_ixor_all 32;
    lemma_logxor_4_nat8 a0 a1 a2 a3 b0 b1 b2 b3
    in
  let lemma_xor_4_nat8 (a0 a1 a2 a3 b0 b1 b2 b3:nat8) : Lemma
    (nat32_xor (mk4 a0 a1 a2 a3) (mk4 b0 b1 b2 b3) == mk4 (nat32_xor a0 b0) (nat32_xor a1 b1) (nat32_xor a2 b2) (nat32_xor a3 b3))
    =
    lemma_mk4_mk4m a0 a1 a2 a3;
    lemma_mk4_mk4m b0 b1 b2 b3;
    lemma_mk4_mk4m (nat32_xor a0 b0) (nat32_xor a1 b1) (nat32_xor a2 b2) (nat32_xor a3 b3);
    lemma_xor_4_nat8_n a0 a1 a2 a3 b0 b1 b2 b3
    in
  let rev_nat32 (a b:nat32) : Lemma
    (r32 (nat32_xor a b) == nat32_xor (r32 a) (r32 b))
    =
    calc (==) {
      r32 (nat32_xor a b);
      == {reverse_bytes_nat32_reveal ()}
      be_bytes_to_nat32 (reverse_seq (nat32_to_be_bytes (nat32_xor a b)));
      == {
        let x = nat32_xor a b in
        let y = r32 x in
        let Mkfour a0 a1 a2 a3 = nat_to_four 8 a in
        let Mkfour b0 b1 b2 b3 = nat_to_four 8 b in
        let Mkfour x0 x1 x2 x3 = nat_to_four 8 x in
        let Mkfour y0 y1 y2 y3 = nat_to_four 8 y in
        lemma_xor_4_nat8 a0 a1 a2 a3 b0 b1 b2 b3;
        lemma_xor_4_nat8 a3 a2 a1 a0 b3 b2 b1 b0;
        ()
      }
      nat32_xor (be_bytes_to_nat32 (reverse_seq (nat32_to_be_bytes a))) (be_bytes_to_nat32 (reverse_seq (nat32_to_be_bytes b)));
      == {reverse_bytes_nat32_reveal ()}
      nat32_xor (r32 a) (r32 b);
    }
    // r32 n = be_bytes_to_nat32 (reverse_seq (nat32_to_be_bytes n))
    // lemma_ixor_nth_all 32;
    in
  calc (==) {
    !!(quad32_xor a b);
    == {quad32_xor_reveal ()}
    !!(four_map2 nat32_xor a b);
    == {reveal_reverse_bytes_quad32 (four_map2 nat32_xor a b)}
    four_reverse (four_map r32 (four_map2 nat32_xor a b));
    == {
      let Mkfour a0 a1 a2 a3 = a in
      let Mkfour b0 b1 b2 b3 = b in
      rev_nat32 a0 b0;
      rev_nat32 a1 b1;
      rev_nat32 a2 b2;
      rev_nat32 a3 b3;
      ()
    }
    four_reverse (four_map2 nat32_xor (four_map r32 a) (four_map r32 b));
    == {}
    four_map2 nat32_xor (four_reverse (four_map r32 a)) (four_reverse (four_map r32 b));
    == {reveal_reverse_bytes_quad32 a; reveal_reverse_bytes_quad32 b}
    four_map2 nat32_xor !!a !!b;
    == {quad32_xor_reveal ()}
    quad32_xor !!a !!b;
  }

let rec lemma_ghash_incremental_poly_rec (h_LE:quad32) (y_prev:quad32) (x:seq quad32) (data:int -> poly128) : Lemma
  (requires
    (forall (i:int).{:pattern data i \/ index x i} 0 <= i && i < length x ==>
      data i == of_quad32 (reverse_bytes_quad32 (index x i)))
  )
  (ensures
    of_quad32 (reverse_bytes_quad32 (ghash_incremental_def h_LE y_prev x)) ==
    ghash_poly (of_quad32 (reverse_bytes_quad32 h_LE)) (of_quad32 (reverse_bytes_quad32 y_prev)) data 0 (length x)
  )
  (decreases (length x))
val lemma_ghash_incremental_poly_rec (h_LE y_prev: quad32) (x: seq quad32) (data: (int -> poly128))
    : Lemma
      (requires
        (forall (i: int). {:pattern data i\/index x i}
            0 <= i && i < length x ==> data i == of_quad32 (reverse_bytes_quad32 (index x i))))
      (ensures
        of_quad32 (reverse_bytes_quad32 (ghash_incremental_def h_LE y_prev x)) ==
        ghash_poly (of_quad32 (reverse_bytes_quad32 h_LE))
          (of_quad32 (reverse_bytes_quad32 y_prev))
          data
          0
          (length x))
      (decreases (length x))

    h_LE: Vale.Def.Types_s.quad32 ->
    y_prev: Vale.Def.Types_s.quad32 ->
    x: FStar.Seq.Base.seq Vale.Def.Types_s.quad32 ->
    data: (_: Prims.int -> Vale.AES.GHash.poly128)
  -> FStar.Pervasives.Lemma
      (requires
        forall (i: Prims.int). {:pattern data i\/FStar.Seq.Base.index x i}
          0 <= i && i < FStar.Seq.Base.length x ==>
          data i ==
          Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 (FStar.Seq.Base.index
                    x
                    i)))
      (ensures
        Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 (Vale.AES.GHash.ghash_incremental_def
                  h_LE
                  y_prev
                  x)) ==
        Vale.AES.GHash.ghash_poly (Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32
                  h_LE))
          (Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 y_prev))
          data
          0
          (FStar.Seq.Base.length x))
      (decreases FStar.Seq.Base.length x)