val va_lemma_MulAdd_step : va_b0:va_code -> va_s0:va_state -> m:nat -> power_index:int ->
  a0:va_operand_xmm -> a1:va_operand_xmm -> a2:va_operand_xmm -> a3:va_operand_xmm ->
  b:va_operand_xmm -> c:va_operand_xmm -> hkeys_b:buffer128 -> scratch_b:buffer128 -> h:poly ->
  prev:poly -> data:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_MulAdd_step m power_index a0 a1 a2 a3 b c) va_s0 /\
    va_is_dst_xmm a0 va_s0 /\ va_is_dst_xmm a1 va_s0 /\ va_is_dst_xmm a2 va_s0 /\ va_is_dst_xmm a3
    va_s0 /\ va_is_dst_xmm b va_s0 /\ va_is_dst_xmm c va_s0 /\ va_get_ok va_s0 /\ (let
    (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in pclmulqdq_enabled /\ avx_enabled /\ sse_enabled /\ m < 6 /\ FStar.Seq.Base.length #quad32
    data >= 6 /\ (m == 0 ==> a0 == 1 /\ a1 == 5 /\ a2 == 6 /\ a3 == 7 /\ b == 7 /\ c == 3) /\ (m ==
    1 ==> a0 == 5 /\ a1 == 1 /\ a2 == 2 /\ a3 == 3 /\ b == 0 /\ c == 3) /\ (m == 2 ==> a0 == 1 /\
    a1 == 2 /\ a2 == 3 /\ a3 == 5 /\ b == 0 /\ c == 5) /\ (m == 3 ==> a0 == 2 /\ a1 == 3 /\ a2 == 5
    /\ a3 == 1 /\ b == 0 /\ c == 1) /\ (m == 4 ==> a0 == 3 /\ a1 == 5 /\ a2 == 1 /\ a3 == 2 /\ b ==
    0 /\ c == 2) /\ (m == 5 ==> a0 == 2 /\ a1 == 5 /\ a2 == 1 /\ a3 == 8 /\ b == 8 /\ c == 3) /\
    Vale.X64.Decls.validSrcAddrs128 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rR9 va_s0 - 32)
    hkeys_b 8 (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs128
    (va_get_mem_heaplet 3 va_s0) (va_get_reg64 rRbp va_s0) scratch_b 8 (va_get_mem_layout va_s0)
    Secret /\ (0 <= power_index /\ power_index < 8) /\ (let z0 = (if (m = 1) then va_eval_xmm va_s0
    a1 else va_get_xmm 4 va_s0) in (m > 0 ==> add (add (Vale.Math.Poly2.Bits_s.of_quad32 z0)
    (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_s0)) 64))
    (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_s0)) 128) ==
    Vale.AES.GHash.ghash_unroll_back h prev pdata 0 6 (m - 1)) /\ (m < 5 ==> va_eval_xmm va_s0 b ==
    Vale.Def.Types_s.reverse_bytes_quad32 (va_subscript_FStar__Seq__Base__seq data (5 - m))) /\ (m
    == 5 ==> Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_xmm va_s0 b) == add prev
    (Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32
    (va_subscript_FStar__Seq__Base__seq data (5 - m))))) /\ (m == 0 ==>
    Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_xmm va_s0 c) == Vale.AES.GHash.gf128_power h (m + 1))
    /\ Vale.Math.Poly2.Bits_s.of_quad32 (Vale.X64.Decls.buffer128_read hkeys_b power_index
    (va_get_mem_heaplet 0 va_s0)) == Vale.AES.GHash.gf128_power h (m + 1)))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128
    data in (m < 4 ==> va_get_xmm 0 va_sM == Vale.X64.Decls.buffer128_read scratch_b (3 + m)
    (va_get_mem_heaplet 3 va_sM)) /\ (let z0 = (if (m = 0) then va_eval_xmm va_sM a0 else
    va_get_xmm 4 va_sM) in add (add (Vale.Math.Poly2.Bits_s.of_quad32 z0) (Vale.Math.Poly2_s.shift
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_sM)) 64)) (Vale.Math.Poly2_s.shift
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_sM)) 128) ==
    Vale.AES.GHash.ghash_unroll_back h prev pdata 0 6 m /\ (m == 0 ==>
    Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_sM) == add (add
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_s0)) (Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 4 va_s0))) (Vale.Math.Poly2.Bits_s.of_quad32 (Vale.X64.Decls.buffer128_read
    scratch_b 1 (va_get_mem_heaplet 3 va_s0)))) /\ (m == 4 ==> Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 8 va_sM) == add (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_s0))
    (Vale.Math.Poly2.Bits_s.of_quad32 (Vale.X64.Decls.buffer128_read scratch_b 7
    (va_get_mem_heaplet 3 va_s0)))) /\ (0 < m /\ m < 4 ==> va_get_xmm 8 va_sM == va_get_xmm 8
    va_s0))) /\ va_state_eq va_sM (va_update_xmm 8 va_sM (va_update_xmm 7 va_sM (va_update_xmm 6
    va_sM (va_update_xmm 4 va_sM (va_update_xmm 0 va_sM (va_update_flags va_sM (va_update_ok va_sM
    (va_update_operand_xmm c va_sM (va_update_operand_xmm b va_sM (va_update_operand_xmm a3 va_sM
    (va_update_operand_xmm a2 va_sM (va_update_operand_xmm a1 va_sM (va_update_operand_xmm a0 va_sM
    va_s0)))))))))))))))
let va_lemma_MulAdd_step va_b0 va_s0 m power_index a0 a1 a2 a3 b c hkeys_b scratch_b h prev data =
  va_reveal_opaque (`%va_code_MulAdd_step) (va_code_MulAdd_step m power_index a0 a1 a2 a3 b c);
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in
  let (data_i:poly) = pdata (5 - m) in
  let (z0:quad32) = (if (m = 1) then va_eval_xmm va_s0 a1 else va_get_xmm 4 va_s0) in
  Vale.AES.GF128.lemma_Mul128_accum (of_quad32 z0) (of_quad32 (va_get_xmm 6 va_s0)) (of_quad32
    (va_get_xmm 7 va_s0)) (if (m = 5) then add prev data_i else data_i) (Vale.AES.GHash.gf128_power
    h (m + 1));
  let va_b12 = va_tl va_b1 in
  let va_c12 = va_hd va_b1 in
  let (va_fc12, va_s12) =
  (
    if (m = 0) then
    (
      let va_b13 = va_get_block va_c12 in
      let (va_s14, va_fc14) = va_lemma_VPolyMul (va_hd va_b13) va_s0 a0 b c false false in
      let va_b14 = va_tl va_b13 in
      let (va_s15, va_fc15) = va_lemma_VPolyMul (va_hd va_b14) va_s14 a1 b c false true in
      let va_b15 = va_tl va_b14 in
      let (va_s16, va_fc16) = va_lemma_VPolyMul (va_hd va_b15) va_s15 a2 b c true false in
      let va_b16 = va_tl va_b15 in
      let (va_s17, va_fc17) = va_lemma_VPolyMul (va_hd va_b16) va_s16 b b c true true in
      let va_b17 = va_tl va_b16 in
      Vale.AES.GF128.lemma_Mul128 data_i (Vale.AES.GHash.gf128_power h 1);
      Vale.Math.Poly2.lemma_add_commute (of_quad32 (va_eval_xmm va_s17 a1)) (of_quad32 (va_eval_xmm
        va_s17 a2));
      let (va_s20, va_fc20) = va_lemma_VPolyAdd (va_hd va_b17) va_s17 (va_op_xmm_xmm 6) a2
        (va_coerce_xmm_to_opr128 a1) in
      let va_b20 = va_tl va_b17 in
      let (va_s21, va_fc21) = va_lemma_VPolyAdd (va_hd va_b20) va_s20 (va_op_xmm_xmm 8)
        (va_op_xmm_xmm 8) (va_op_opr128_xmm 4) in
      let va_b21 = va_tl va_b20 in
      let (va_s22, va_fc22) = va_lemma_Mem128_lemma (va_hd va_b21) va_s21
        (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp) 16 Secret scratch_b 1 in
      let va_b22 = va_tl va_b21 in
      let (va_s23, va_fc23) = va_lemma_VPolyAdd (va_hd va_b22) va_s22 (va_op_xmm_xmm 8)
        (va_op_xmm_xmm 8) (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64
        rRbp) 16 Secret) in
      let va_b23 = va_tl va_b22 in
      let (va_s12, va_f23) = va_lemma_empty_total va_s23 va_b23 in
      let va_f22 = va_lemma_merge_total va_b22 va_s22 va_fc23 va_s23 va_f23 va_s12 in
      let va_f21 = va_lemma_merge_total va_b21 va_s21 va_fc22 va_s22 va_f22 va_s12 in
      let va_f20 = va_lemma_merge_total va_b20 va_s20 va_fc21 va_s21 va_f21 va_s12 in
      let va_f17 = va_lemma_merge_total va_b17 va_s17 va_fc20 va_s20 va_f20 va_s12 in
      let va_f16 = va_lemma_merge_total va_b16 va_s16 va_fc17 va_s17 va_f17 va_s12 in
      let va_f15 = va_lemma_merge_total va_b15 va_s15 va_fc16 va_s16 va_f16 va_s12 in
      let va_f14 = va_lemma_merge_total va_b14 va_s14 va_fc15 va_s15 va_f15 va_s12 in
      let va_fc12 = va_lemma_merge_total va_b13 va_s0 va_fc14 va_s14 va_f14 va_s12 in
      (va_fc12, va_s12)
    )
    else
    (
      let va_b24 = va_get_block va_c12 in
      let (va_s25, va_fc25) = va_lemma_Load128_buffer (va_hd va_b24) va_s0
        (va_op_heaplet_mem_heaplet 0) c (va_op_reg_opr64_reg64 rR9) (16 `op_Multiply` power_index -
        32) Secret hkeys_b power_index in
      let va_b25 = va_tl va_b24 in
      let (va_s26, va_fc26) = va_lemma_VPolyMul (va_hd va_b25) va_s25 a0 b c false false in
      let va_b26 = va_tl va_b25 in
      let va_b27 = va_tl va_b26 in
      let va_c27 = va_hd va_b26 in
      let (va_fc27, va_s27) =
      (
        if (m = 1) then
        (
          let va_b28 = va_get_block va_c27 in
          let (va_s29, va_fc29) = va_lemma_VPolyAdd (va_hd va_b28) va_s26 (va_op_xmm_xmm 4) a1
            (va_coerce_xmm_to_opr128 a0) in
          let va_b29 = va_tl va_b28 in
          let (va_s27, va_f29) = va_lemma_empty_total va_s29 va_b29 in
          let va_fc27 = va_lemma_merge_total va_b28 va_s26 va_fc29 va_s29 va_f29 va_s27 in
          (va_fc27, va_s27)
        )
        else
        (
          let va_b30 = va_get_block va_c27 in
          let (va_s31, va_fc31) = va_lemma_VPolyAdd (va_hd va_b30) va_s26 (va_op_xmm_xmm 4)
            (va_op_xmm_xmm 4) (va_coerce_xmm_to_opr128 a0) in
          let va_b31 = va_tl va_b30 in
          let (va_s27, va_f31) = va_lemma_empty_total va_s31 va_b31 in
          let va_fc27 = va_lemma_merge_total va_b30 va_s26 va_fc31 va_s31 va_f31 va_s27 in
          (va_fc27, va_s27)
        )
      ) in
      let (va_s32, va_fc32) = va_lemma_VPolyMul (va_hd va_b27) va_s27 a1 b c false true in
      let va_b32 = va_tl va_b27 in
      let (va_s33, va_fc33) = va_lemma_VPolyMul (va_hd va_b32) va_s32 a2 b c true false in
      let va_b33 = va_tl va_b32 in
      let (va_s34, va_fc34) = va_lemma_VPolyMul (va_hd va_b33) va_s33 a3 b c true true in
      let va_b34 = va_tl va_b33 in
      let (va_s35, va_fc35) = va_lemma_VPolyAdd (va_hd va_b34) va_s34 (va_op_xmm_xmm 6)
        (va_op_xmm_xmm 6) (va_coerce_xmm_to_opr128 a1) in
      let va_b35 = va_tl va_b34 in
      let (va_s36, va_fc36) = va_lemma_VPolyAdd (va_hd va_b35) va_s35 (va_op_xmm_xmm 6)
        (va_op_xmm_xmm 6) (va_coerce_xmm_to_opr128 a2) in
      let va_b36 = va_tl va_b35 in
      let (va_s37, va_fc37) = va_lemma_VPolyAdd (va_hd va_b36) va_s36 (va_op_xmm_xmm 7)
        (va_op_xmm_xmm 7) (va_coerce_xmm_to_opr128 a3) in
      let va_b37 = va_tl va_b36 in
      let va_b38 = va_tl va_b37 in
      let va_c38 = va_hd va_b37 in
      let (va_fc38, va_s38) =
      (
        if (m = 4) then
        (
          let va_b39 = va_get_block va_c38 in
          let (va_s40, va_fc40) = va_lemma_Mem128_lemma (va_hd va_b39) va_s37
            (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp) 112 Secret scratch_b 7 in
          let va_b40 = va_tl va_b39 in
          let (va_s41, va_fc41) = va_lemma_VPolyAdd (va_hd va_b40) va_s40 (va_op_xmm_xmm 8)
            (va_op_xmm_xmm 8) (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64
            rRbp) 112 Secret) in
          let va_b41 = va_tl va_b40 in
          let (va_s38, va_f41) = va_lemma_empty_total va_s41 va_b41 in
          let va_f40 = va_lemma_merge_total va_b40 va_s40 va_fc41 va_s41 va_f41 va_s38 in
          let va_fc38 = va_lemma_merge_total va_b39 va_s37 va_fc40 va_s40 va_f40 va_s38 in
          (va_fc38, va_s38)
        )
        else
        (
          let va_b42 = va_get_block va_c38 in
          let (va_s38, va_fc38) = va_lemma_empty_total va_s37 va_b42 in
          (va_fc38, va_s38)
        )
      ) in
      let (va_s12, va_f38) = va_lemma_empty_total va_s38 va_b38 in
      let va_f37 = va_lemma_merge_total va_b37 va_s37 va_fc38 va_s38 va_f38 va_s12 in
      let va_f36 = va_lemma_merge_total va_b36 va_s36 va_fc37 va_s37 va_f37 va_s12 in
      let va_f35 = va_lemma_merge_total va_b35 va_s35 va_fc36 va_s36 va_f36 va_s12 in
      let va_f34 = va_lemma_merge_total va_b34 va_s34 va_fc35 va_s35 va_f35 va_s12 in
      let va_f33 = va_lemma_merge_total va_b33 va_s33 va_fc34 va_s34 va_f34 va_s12 in
      let va_f32 = va_lemma_merge_total va_b32 va_s32 va_fc33 va_s33 va_f33 va_s12 in
      let va_f27 = va_lemma_merge_total va_b27 va_s27 va_fc32 va_s32 va_f32 va_s12 in
      let va_f26 = va_lemma_merge_total va_b26 va_s26 va_fc27 va_s27 va_f27 va_s12 in
      let va_f25 = va_lemma_merge_total va_b25 va_s25 va_fc26 va_s26 va_f26 va_s12 in
      let va_fc12 = va_lemma_merge_total va_b24 va_s0 va_fc25 va_s25 va_f25 va_s12 in
      (va_fc12, va_s12)
    )
  ) in
  let va_b43 = va_tl va_b12 in
  let va_c43 = va_hd va_b12 in
  let (va_fc43, va_s43) =
  (
    if (m < 4) then
    (
      let va_b44 = va_get_block va_c43 in
      let (va_s45, va_fc45) = va_lemma_Load128_buffer (va_hd va_b44) va_s12
        (va_op_heaplet_mem_heaplet 3) (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64 rRbp) (48 + 16
        `op_Multiply` m) Secret scratch_b (3 + m) in
      let va_b45 = va_tl va_b44 in
      let (va_s43, va_f45) = va_lemma_empty_total va_s45 va_b45 in
      let va_fc43 = va_lemma_merge_total va_b44 va_s12 va_fc45 va_s45 va_f45 va_s43 in
      (va_fc43, va_s43)
    )
    else
    (
      let va_b46 = va_get_block va_c43 in
      let (va_s43, va_fc43) = va_lemma_empty_total va_s12 va_b46 in
      (va_fc43, va_s43)
    )
  ) in
  let (va_sM, va_f43) = va_lemma_empty_total va_s43 va_b43 in
  let va_f12 = va_lemma_merge_total va_b12 va_s12 va_fc43 va_s43 va_f43 va_sM in
  let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc12 va_s12 va_f12 va_sM in
  (va_sM, va_fM)
val va_lemma_MulAdd_step : va_b0:va_code -> va_s0:va_state -> m:nat -> power_index:int ->
  a0:va_operand_xmm -> a1:va_operand_xmm -> a2:va_operand_xmm -> a3:va_operand_xmm ->
  b:va_operand_xmm -> c:va_operand_xmm -> hkeys_b:buffer128 -> scratch_b:buffer128 -> h:poly ->
  prev:poly -> data:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_MulAdd_step m power_index a0 a1 a2 a3 b c) va_s0 /\
    va_is_dst_xmm a0 va_s0 /\ va_is_dst_xmm a1 va_s0 /\ va_is_dst_xmm a2 va_s0 /\ va_is_dst_xmm a3
    va_s0 /\ va_is_dst_xmm b va_s0 /\ va_is_dst_xmm c va_s0 /\ va_get_ok va_s0 /\ (let
    (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in pclmulqdq_enabled /\ avx_enabled /\ sse_enabled /\ m < 6 /\ FStar.Seq.Base.length #quad32
    data >= 6 /\ (m == 0 ==> a0 == 1 /\ a1 == 5 /\ a2 == 6 /\ a3 == 7 /\ b == 7 /\ c == 3) /\ (m ==
    1 ==> a0 == 5 /\ a1 == 1 /\ a2 == 2 /\ a3 == 3 /\ b == 0 /\ c == 3) /\ (m == 2 ==> a0 == 1 /\
    a1 == 2 /\ a2 == 3 /\ a3 == 5 /\ b == 0 /\ c == 5) /\ (m == 3 ==> a0 == 2 /\ a1 == 3 /\ a2 == 5
    /\ a3 == 1 /\ b == 0 /\ c == 1) /\ (m == 4 ==> a0 == 3 /\ a1 == 5 /\ a2 == 1 /\ a3 == 2 /\ b ==
    0 /\ c == 2) /\ (m == 5 ==> a0 == 2 /\ a1 == 5 /\ a2 == 1 /\ a3 == 8 /\ b == 8 /\ c == 3) /\
    Vale.X64.Decls.validSrcAddrs128 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rR9 va_s0 - 32)
    hkeys_b 8 (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs128
    (va_get_mem_heaplet 3 va_s0) (va_get_reg64 rRbp va_s0) scratch_b 8 (va_get_mem_layout va_s0)
    Secret /\ (0 <= power_index /\ power_index < 8) /\ (let z0 = (if (m = 1) then va_eval_xmm va_s0
    a1 else va_get_xmm 4 va_s0) in (m > 0 ==> add (add (Vale.Math.Poly2.Bits_s.of_quad32 z0)
    (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_s0)) 64))
    (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_s0)) 128) ==
    Vale.AES.GHash.ghash_unroll_back h prev pdata 0 6 (m - 1)) /\ (m < 5 ==> va_eval_xmm va_s0 b ==
    Vale.Def.Types_s.reverse_bytes_quad32 (va_subscript_FStar__Seq__Base__seq data (5 - m))) /\ (m
    == 5 ==> Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_xmm va_s0 b) == add prev
    (Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32
    (va_subscript_FStar__Seq__Base__seq data (5 - m))))) /\ (m == 0 ==>
    Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_xmm va_s0 c) == Vale.AES.GHash.gf128_power h (m + 1))
    /\ Vale.Math.Poly2.Bits_s.of_quad32 (Vale.X64.Decls.buffer128_read hkeys_b power_index
    (va_get_mem_heaplet 0 va_s0)) == Vale.AES.GHash.gf128_power h (m + 1)))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128
    data in (m < 4 ==> va_get_xmm 0 va_sM == Vale.X64.Decls.buffer128_read scratch_b (3 + m)
    (va_get_mem_heaplet 3 va_sM)) /\ (let z0 = (if (m = 0) then va_eval_xmm va_sM a0 else
    va_get_xmm 4 va_sM) in add (add (Vale.Math.Poly2.Bits_s.of_quad32 z0) (Vale.Math.Poly2_s.shift
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_sM)) 64)) (Vale.Math.Poly2_s.shift
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_sM)) 128) ==
    Vale.AES.GHash.ghash_unroll_back h prev pdata 0 6 m /\ (m == 0 ==>
    Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_sM) == add (add
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_s0)) (Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 4 va_s0))) (Vale.Math.Poly2.Bits_s.of_quad32 (Vale.X64.Decls.buffer128_read
    scratch_b 1 (va_get_mem_heaplet 3 va_s0)))) /\ (m == 4 ==> Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 8 va_sM) == add (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_s0))
    (Vale.Math.Poly2.Bits_s.of_quad32 (Vale.X64.Decls.buffer128_read scratch_b 7
    (va_get_mem_heaplet 3 va_s0)))) /\ (0 < m /\ m < 4 ==> va_get_xmm 8 va_sM == va_get_xmm 8
    va_s0))) /\ va_state_eq va_sM (va_update_xmm 8 va_sM (va_update_xmm 7 va_sM (va_update_xmm 6
    va_sM (va_update_xmm 4 va_sM (va_update_xmm 0 va_sM (va_update_flags va_sM (va_update_ok va_sM
    (va_update_operand_xmm c va_sM (va_update_operand_xmm b va_sM (va_update_operand_xmm a3 va_sM
    (va_update_operand_xmm a2 va_sM (va_update_operand_xmm a1 va_sM (va_update_operand_xmm a0 va_sM
    va_s0)))))))))))))))
let va_lemma_MulAdd_step va_b0 va_s0 m power_index a0 a1 a2 a3 b c hkeys_b scratch_b h prev data =
va_reveal_opaque (`%va_code_MulAdd_step) (va_code_MulAdd_step m power_index a0 a1 a2 a3 b c);
let va_old_s:va_state = va_s0 in
let va_b1:va_codes = va_get_block va_b0 in
let pdata:(Prims.int -> Vale.AES.GHash.poly128) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in
let data_i:poly = pdata (5 - m) in
let z0:quad32 = (if (m = 1) then va_eval_xmm va_s0 a1 else va_get_xmm 4 va_s0) in
Vale.AES.GF128.lemma_Mul128_accum (of_quad32 z0)
  (of_quad32 (va_get_xmm 6 va_s0))
  (of_quad32 (va_get_xmm 7 va_s0))
  (if (m = 5) then add prev data_i else data_i)
  (Vale.AES.GHash.gf128_power h (m + 1));
let va_b12 = va_tl va_b1 in
let va_c12 = va_hd va_b1 in
let va_fc12, va_s12 =
  (if (m = 0)
    then
      (let va_b13 = va_get_block va_c12 in
        let va_s14, va_fc14 = va_lemma_VPolyMul (va_hd va_b13) va_s0 a0 b c false false in
        let va_b14 = va_tl va_b13 in
        let va_s15, va_fc15 = va_lemma_VPolyMul (va_hd va_b14) va_s14 a1 b c false true in
        let va_b15 = va_tl va_b14 in
        let va_s16, va_fc16 = va_lemma_VPolyMul (va_hd va_b15) va_s15 a2 b c true false in
        let va_b16 = va_tl va_b15 in
        let va_s17, va_fc17 = va_lemma_VPolyMul (va_hd va_b16) va_s16 b b c true true in
        let va_b17 = va_tl va_b16 in
        Vale.AES.GF128.lemma_Mul128 data_i (Vale.AES.GHash.gf128_power h 1);
        Vale.Math.Poly2.lemma_add_commute (of_quad32 (va_eval_xmm va_s17 a1))
          (of_quad32 (va_eval_xmm va_s17 a2));
        let va_s20, va_fc20 =
          va_lemma_VPolyAdd (va_hd va_b17) va_s17 (va_op_xmm_xmm 6) a2 (va_coerce_xmm_to_opr128 a1)
        in
        let va_b20 = va_tl va_b17 in
        let va_s21, va_fc21 =
          va_lemma_VPolyAdd (va_hd va_b20)
            va_s20
            (va_op_xmm_xmm 8)
            (va_op_xmm_xmm 8)
            (va_op_opr128_xmm 4)
        in
        let va_b21 = va_tl va_b20 in
        let va_s22, va_fc22 =
          va_lemma_Mem128_lemma (va_hd va_b21)
            va_s21
            (va_op_heaplet_mem_heaplet 3)
            (va_op_reg64_reg64 rRbp)
            16
            Secret
            scratch_b
            1
        in
        let va_b22 = va_tl va_b21 in
        let va_s23, va_fc23 =
          va_lemma_VPolyAdd (va_hd va_b22)
            va_s22
            (va_op_xmm_xmm 8)
            (va_op_xmm_xmm 8)
            (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp) 16 Secret)
        in
        let va_b23 = va_tl va_b22 in
        let va_s12, va_f23 = va_lemma_empty_total va_s23 va_b23 in
        let va_f22 = va_lemma_merge_total va_b22 va_s22 va_fc23 va_s23 va_f23 va_s12 in
        let va_f21 = va_lemma_merge_total va_b21 va_s21 va_fc22 va_s22 va_f22 va_s12 in
        let va_f20 = va_lemma_merge_total va_b20 va_s20 va_fc21 va_s21 va_f21 va_s12 in
        let va_f17 = va_lemma_merge_total va_b17 va_s17 va_fc20 va_s20 va_f20 va_s12 in
        let va_f16 = va_lemma_merge_total va_b16 va_s16 va_fc17 va_s17 va_f17 va_s12 in
        let va_f15 = va_lemma_merge_total va_b15 va_s15 va_fc16 va_s16 va_f16 va_s12 in
        let va_f14 = va_lemma_merge_total va_b14 va_s14 va_fc15 va_s15 va_f15 va_s12 in
        let va_fc12 = va_lemma_merge_total va_b13 va_s0 va_fc14 va_s14 va_f14 va_s12 in
        (va_fc12, va_s12))
    else
      (let va_b24 = va_get_block va_c12 in
        let va_s25, va_fc25 =
          va_lemma_Load128_buffer (va_hd va_b24)
            va_s0
            (va_op_heaplet_mem_heaplet 0)
            c
            (va_op_reg_opr64_reg64 rR9)
            (16 `op_Multiply` power_index - 32)
            Secret
            hkeys_b
            power_index
        in
        let va_b25 = va_tl va_b24 in
        let va_s26, va_fc26 = va_lemma_VPolyMul (va_hd va_b25) va_s25 a0 b c false false in
        let va_b26 = va_tl va_b25 in
        let va_b27 = va_tl va_b26 in
        let va_c27 = va_hd va_b26 in
        let va_fc27, va_s27 =
          (if (m = 1)
            then
              (let va_b28 = va_get_block va_c27 in
                let va_s29, va_fc29 =
                  va_lemma_VPolyAdd (va_hd va_b28)
                    va_s26
                    (va_op_xmm_xmm 4)
                    a1
                    (va_coerce_xmm_to_opr128 a0)
                in
                let va_b29 = va_tl va_b28 in
                let va_s27, va_f29 = va_lemma_empty_total va_s29 va_b29 in
                let va_fc27 = va_lemma_merge_total va_b28 va_s26 va_fc29 va_s29 va_f29 va_s27 in
                (va_fc27, va_s27))
            else
              (let va_b30 = va_get_block va_c27 in
                let va_s31, va_fc31 =
                  va_lemma_VPolyAdd (va_hd va_b30)
                    va_s26
                    (va_op_xmm_xmm 4)
                    (va_op_xmm_xmm 4)
                    (va_coerce_xmm_to_opr128 a0)
                in
                let va_b31 = va_tl va_b30 in
                let va_s27, va_f31 = va_lemma_empty_total va_s31 va_b31 in
                let va_fc27 = va_lemma_merge_total va_b30 va_s26 va_fc31 va_s31 va_f31 va_s27 in
                (va_fc27, va_s27)))
        in
        let va_s32, va_fc32 = va_lemma_VPolyMul (va_hd va_b27) va_s27 a1 b c false true in
        let va_b32 = va_tl va_b27 in
        let va_s33, va_fc33 = va_lemma_VPolyMul (va_hd va_b32) va_s32 a2 b c true false in
        let va_b33 = va_tl va_b32 in
        let va_s34, va_fc34 = va_lemma_VPolyMul (va_hd va_b33) va_s33 a3 b c true true in
        let va_b34 = va_tl va_b33 in
        let va_s35, va_fc35 =
          va_lemma_VPolyAdd (va_hd va_b34)
            va_s34
            (va_op_xmm_xmm 6)
            (va_op_xmm_xmm 6)
            (va_coerce_xmm_to_opr128 a1)
        in
        let va_b35 = va_tl va_b34 in
        let va_s36, va_fc36 =
          va_lemma_VPolyAdd (va_hd va_b35)
            va_s35
            (va_op_xmm_xmm 6)
            (va_op_xmm_xmm 6)
            (va_coerce_xmm_to_opr128 a2)
        in
        let va_b36 = va_tl va_b35 in
        let va_s37, va_fc37 =
          va_lemma_VPolyAdd (va_hd va_b36)
            va_s36
            (va_op_xmm_xmm 7)
            (va_op_xmm_xmm 7)
            (va_coerce_xmm_to_opr128 a3)
        in
        let va_b37 = va_tl va_b36 in
        let va_b38 = va_tl va_b37 in
        let va_c38 = va_hd va_b37 in
        let va_fc38, va_s38 =
          (if (m = 4)
            then
              (let va_b39 = va_get_block va_c38 in
                let va_s40, va_fc40 =
                  va_lemma_Mem128_lemma (va_hd va_b39)
                    va_s37
                    (va_op_heaplet_mem_heaplet 3)
                    (va_op_reg64_reg64 rRbp)
                    112
                    Secret
                    scratch_b
                    7
                in
                let va_b40 = va_tl va_b39 in
                let va_s41, va_fc41 =
                  va_lemma_VPolyAdd (va_hd va_b40)
                    va_s40
                    (va_op_xmm_xmm 8)
                    (va_op_xmm_xmm 8)
                    (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3)
                        (va_op_reg64_reg64 rRbp)
                        112
                        Secret)
                in
                let va_b41 = va_tl va_b40 in
                let va_s38, va_f41 = va_lemma_empty_total va_s41 va_b41 in
                let va_f40 = va_lemma_merge_total va_b40 va_s40 va_fc41 va_s41 va_f41 va_s38 in
                let va_fc38 = va_lemma_merge_total va_b39 va_s37 va_fc40 va_s40 va_f40 va_s38 in
                (va_fc38, va_s38))
            else
              (let va_b42 = va_get_block va_c38 in
                let va_s38, va_fc38 = va_lemma_empty_total va_s37 va_b42 in
                (va_fc38, va_s38)))
        in
        let va_s12, va_f38 = va_lemma_empty_total va_s38 va_b38 in
        let va_f37 = va_lemma_merge_total va_b37 va_s37 va_fc38 va_s38 va_f38 va_s12 in
        let va_f36 = va_lemma_merge_total va_b36 va_s36 va_fc37 va_s37 va_f37 va_s12 in
        let va_f35 = va_lemma_merge_total va_b35 va_s35 va_fc36 va_s36 va_f36 va_s12 in
        let va_f34 = va_lemma_merge_total va_b34 va_s34 va_fc35 va_s35 va_f35 va_s12 in
        let va_f33 = va_lemma_merge_total va_b33 va_s33 va_fc34 va_s34 va_f34 va_s12 in
        let va_f32 = va_lemma_merge_total va_b32 va_s32 va_fc33 va_s33 va_f33 va_s12 in
        let va_f27 = va_lemma_merge_total va_b27 va_s27 va_fc32 va_s32 va_f32 va_s12 in
        let va_f26 = va_lemma_merge_total va_b26 va_s26 va_fc27 va_s27 va_f27 va_s12 in
        let va_f25 = va_lemma_merge_total va_b25 va_s25 va_fc26 va_s26 va_f26 va_s12 in
        let va_fc12 = va_lemma_merge_total va_b24 va_s0 va_fc25 va_s25 va_f25 va_s12 in
        (va_fc12, va_s12)))
in
let va_b43 = va_tl va_b12 in
let va_c43 = va_hd va_b12 in
let va_fc43, va_s43 =
  (if (m < 4)
    then
      (let va_b44 = va_get_block va_c43 in
        let va_s45, va_fc45 =
          va_lemma_Load128_buffer (va_hd va_b44)
            va_s12
            (va_op_heaplet_mem_heaplet 3)
            (va_op_xmm_xmm 0)
            (va_op_reg_opr64_reg64 rRbp)
            (48 + 16 `op_Multiply` m)
            Secret
            scratch_b
            (3 + m)
        in
        let va_b45 = va_tl va_b44 in
        let va_s43, va_f45 = va_lemma_empty_total va_s45 va_b45 in
        let va_fc43 = va_lemma_merge_total va_b44 va_s12 va_fc45 va_s45 va_f45 va_s43 in
        (va_fc43, va_s43))
    else
      (let va_b46 = va_get_block va_c43 in
        let va_s43, va_fc43 = va_lemma_empty_total va_s12 va_b46 in
        (va_fc43, va_s43)))
in
let va_sM, va_f43 = va_lemma_empty_total va_s43 va_b43 in
let va_f12 = va_lemma_merge_total va_b12 va_s12 va_fc43 va_s43 va_f43 va_sM in
let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc12 va_s12 va_f12 va_sM in
(va_sM, va_fM)
Vale.AES.X64.AESopt2.fst.checked
Vale.X64.State.fsti.checked Vale.X64.QuickCodes.fsti.checked Vale.X64.QuickCode.fst.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.InsVector.fsti.checked Vale.X64.InsMem.fsti.checked Vale.X64.InsBasic.fsti.checked Vale.X64.InsAes.fsti.checked Vale.X64.Flags.fsti.checked Vale.X64.Decls.fsti.checked Vale.X64.CPU_Features_s.fst.checked Vale.Poly1305.Math.fsti.checked Vale.Math.Poly2_s.fsti.checked Vale.Math.Poly2.Lemmas.fsti.checked Vale.Math.Poly2.Bits_s.fsti.checked Vale.Math.Poly2.Bits.fsti.checked Vale.Math.Poly2.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.TypesNative.fsti.checked Vale.Arch.Types.fsti.checked Vale.Arch.HeapImpl.fsti.checked Vale.AES.X64.PolyOps.fsti.checked Vale.AES.GHash.fsti.checked Vale.AES.GF128_s.fsti.checked Vale.AES.GF128.fsti.checked Vale.AES.GCTR_s.fst.checked Vale.AES.GCTR.fsti.checked Vale.AES.GCM_helpers.fsti.checked Vale.AES.AES_s.fst.checked Vale.AES.AES_helpers.fsti.checked prims.fst.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.AES.X64.AESopt2.fst
Vale.X64.Decls.va_code Vale.X64.Decls.va_state Prims.nat Prims.int Vale.X64.Decls.va_operand_xmm Vale.X64.Memory.buffer128 Vale.Math.Poly2_s.poly FStar.Seq.Base.seq Vale.X64.Decls.quad32 Vale.X64.Decls.va_fuel FStar.Pervasives.Native.Mktuple2 Vale.X64.Decls.va_lemma_merge_total FStar.Pervasives.Native.tuple2 Vale.X64.State.vale_state Vale.X64.Decls.va_lemma_empty_total Prims.op_LessThan Prims.list Vale.X64.Machine_s.precode Vale.X64.Decls.ins Vale.X64.Decls.ocmp Vale.X64.Decls.va_tl Vale.X64.InsVector.va_lemma_Load128_buffer Vale.X64.Decls.va_hd Vale.X64.Decls.va_op_heaplet_mem_heaplet Vale.X64.Decls.va_op_xmm_xmm Vale.X64.Decls.va_op_reg_opr64_reg64 Vale.X64.Machine_s.rRbp Prims.op_Addition Prims.op_Multiply Vale.Arch.HeapTypes_s.Secret Vale.X64.Decls.va_get_block Prims.bool Prims.op_Equality Vale.AES.X64.PolyOps.va_lemma_VPolyAdd Vale.X64.Decls.va_opr_code_Mem128 Vale.X64.Decls.va_op_reg64_reg64 Vale.X64.InsVector.va_lemma_Mem128_lemma Vale.X64.Decls.va_op_opr128_xmm Vale.X64.Decls.va_coerce_xmm_to_opr128 Prims.unit Vale.Math.Poly2.lemma_add_commute Vale.Math.Poly2.Bits_s.of_quad32 Vale.X64.Decls.va_eval_xmm Vale.AES.GF128.lemma_Mul128 Vale.AES.GHash.gf128_power Vale.AES.X64.PolyOps.va_lemma_VPolyMul Vale.X64.Machine_s.rR9 Prims.op_Subtraction Vale.AES.GF128.lemma_Mul128_accum Vale.X64.Decls.va_get_xmm Vale.Math.Poly2_s.add Vale.Def.Types_s.quad32 Vale.AES.GHash.poly128 Vale.AES.GHash.fun_seq_quad32_LE_poly128 Vale.X64.Decls.va_reveal_opaque Vale.AES.X64.AESopt2.va_code_MulAdd_step
module Vale.AES.X64.AESopt2
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Seq
open Vale.Arch.Types
open Vale.Arch.HeapImpl
open Vale.AES.AES_s
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsMem
open Vale.X64.InsVector
open Vale.X64.InsAes
open Vale.X64.QuickCode
open Vale.X64.QuickCodes
open Vale.AES.AES_helpers
open Vale.Poly1305.Math    // For lemma_poly_bits64()
open Vale.AES.GCM_helpers
open Vale.AES.GCTR_s
open Vale.AES.GCTR
open Vale.Arch.TypesNative
open Vale.X64.CPU_Features_s
open Vale.AES.X64.PolyOps

open Vale.Math.Poly2_s
open Vale.Math.Poly2
open Vale.Math.Poly2.Bits_s
open Vale.Math.Poly2.Bits
open Vale.Math.Poly2.Lemmas
open Vale.AES.GF128_s
open Vale.AES.GF128
open Vale.AES.GHash
#reset-options "--z3rlimit 50"
//-- MulAdd_step

[@ "opaque_to_smt"]
let va_code_MulAdd_step m power_index a0 a1 a2 a3 b c =
  (va_Block (va_CCons (if (m = 0) then va_Block (va_CCons (va_code_VPolyMul a0 b c false false)
    (va_CCons (va_code_VPolyMul a1 b c false true) (va_CCons (va_code_VPolyMul a2 b c true false)
    (va_CCons (va_code_VPolyMul b b c true true) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6) a2
    (va_coerce_xmm_to_opr128 a1)) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 8) (va_op_xmm_xmm 8)
    (va_op_opr128_xmm 4)) (va_CCons (va_code_Mem128_lemma ()) (va_CCons (va_code_VPolyAdd
    (va_op_xmm_xmm 8) (va_op_xmm_xmm 8) (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3)
    (va_op_reg64_reg64 rRbp) 16 Secret)) (va_CNil ()))))))))) else va_Block (va_CCons
    (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 0) c (va_op_reg_opr64_reg64 rR9) (16
    `op_Multiply` power_index - 32) Secret) (va_CCons (va_code_VPolyMul a0 b c false false)
    (va_CCons (if (m = 1) then va_Block (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 4) a1
    (va_coerce_xmm_to_opr128 a0)) (va_CNil ())) else va_Block (va_CCons (va_code_VPolyAdd
    (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_coerce_xmm_to_opr128 a0)) (va_CNil ()))) (va_CCons
    (va_code_VPolyMul a1 b c false true) (va_CCons (va_code_VPolyMul a2 b c true false) (va_CCons
    (va_code_VPolyMul a3 b c true true) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6)
    (va_op_xmm_xmm 6) (va_coerce_xmm_to_opr128 a1)) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6)
    (va_op_xmm_xmm 6) (va_coerce_xmm_to_opr128 a2)) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 7)
    (va_op_xmm_xmm 7) (va_coerce_xmm_to_opr128 a3)) (va_CCons (if (m = 4) then va_Block (va_CCons
    (va_code_Mem128_lemma ()) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 8) (va_op_xmm_xmm 8)
    (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp) 112 Secret))
    (va_CNil ()))) else va_Block (va_CNil ())) (va_CNil ())))))))))))) (va_CCons (if (m < 4) then
    va_Block (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 3) (va_op_xmm_xmm 0)
    (va_op_reg_opr64_reg64 rRbp) (48 + 16 `op_Multiply` m) Secret) (va_CNil ())) else va_Block
    (va_CNil ())) (va_CNil ()))))

[@ "opaque_to_smt"]
let va_codegen_success_MulAdd_step m power_index a0 a1 a2 a3 b c =
  (va_pbool_and (if (m = 0) then va_pbool_and (va_codegen_success_VPolyMul a0 b c false false)
    (va_pbool_and (va_codegen_success_VPolyMul a1 b c false true) (va_pbool_and
    (va_codegen_success_VPolyMul a2 b c true false) (va_pbool_and (va_codegen_success_VPolyMul b b
    c true true) (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 6) a2
    (va_coerce_xmm_to_opr128 a1)) (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 8)
    (va_op_xmm_xmm 8) (va_op_opr128_xmm 4)) (va_pbool_and (va_codegen_success_Mem128_lemma ())
    (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 8) (va_op_xmm_xmm 8)
    (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp) 16 Secret))
    (va_ttrue ())))))))) else va_pbool_and (va_codegen_success_Load128_buffer
    (va_op_heaplet_mem_heaplet 0) c (va_op_reg_opr64_reg64 rR9) (16 `op_Multiply` power_index - 32)
    Secret) (va_pbool_and (va_codegen_success_VPolyMul a0 b c false false) (va_pbool_and (if (m =
    1) then va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 4) a1 (va_coerce_xmm_to_opr128
    a0)) (va_ttrue ()) else va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 4)
    (va_op_xmm_xmm 4) (va_coerce_xmm_to_opr128 a0)) (va_ttrue ())) (va_pbool_and
    (va_codegen_success_VPolyMul a1 b c false true) (va_pbool_and (va_codegen_success_VPolyMul a2 b
    c true false) (va_pbool_and (va_codegen_success_VPolyMul a3 b c true true) (va_pbool_and
    (va_codegen_success_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_coerce_xmm_to_opr128 a1))
    (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6)
    (va_coerce_xmm_to_opr128 a2)) (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 7)
    (va_op_xmm_xmm 7) (va_coerce_xmm_to_opr128 a3)) (va_pbool_and (if (m = 4) then va_pbool_and
    (va_codegen_success_Mem128_lemma ()) (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm
    8) (va_op_xmm_xmm 8) (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp)
    112 Secret)) (va_ttrue ())) else va_ttrue ()) (va_ttrue ()))))))))))) (va_pbool_and (if (m < 4)
    then va_pbool_and (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 3)
    (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64 rRbp) (48 + 16 `op_Multiply` m) Secret) (va_ttrue ())
    else va_ttrue ()) (va_ttrue ())))

[@"opaque_to_smt"]
val va_lemma_MulAdd_step : va_b0:va_code -> va_s0:va_state -> m:nat -> power_index:int ->
  a0:va_operand_xmm -> a1:va_operand_xmm -> a2:va_operand_xmm -> a3:va_operand_xmm ->
  b:va_operand_xmm -> c:va_operand_xmm -> hkeys_b:buffer128 -> scratch_b:buffer128 -> h:poly ->
  prev:poly -> data:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_MulAdd_step m power_index a0 a1 a2 a3 b c) va_s0 /\
    va_is_dst_xmm a0 va_s0 /\ va_is_dst_xmm a1 va_s0 /\ va_is_dst_xmm a2 va_s0 /\ va_is_dst_xmm a3
    va_s0 /\ va_is_dst_xmm b va_s0 /\ va_is_dst_xmm c va_s0 /\ va_get_ok va_s0 /\ (let
    (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in pclmulqdq_enabled /\ avx_enabled /\ sse_enabled /\ m < 6 /\ FStar.Seq.Base.length #quad32
    data >= 6 /\ (m == 0 ==> a0 == 1 /\ a1 == 5 /\ a2 == 6 /\ a3 == 7 /\ b == 7 /\ c == 3) /\ (m ==
    1 ==> a0 == 5 /\ a1 == 1 /\ a2 == 2 /\ a3 == 3 /\ b == 0 /\ c == 3) /\ (m == 2 ==> a0 == 1 /\
    a1 == 2 /\ a2 == 3 /\ a3 == 5 /\ b == 0 /\ c == 5) /\ (m == 3 ==> a0 == 2 /\ a1 == 3 /\ a2 == 5
    /\ a3 == 1 /\ b == 0 /\ c == 1) /\ (m == 4 ==> a0 == 3 /\ a1 == 5 /\ a2 == 1 /\ a3 == 2 /\ b ==
    0 /\ c == 2) /\ (m == 5 ==> a0 == 2 /\ a1 == 5 /\ a2 == 1 /\ a3 == 8 /\ b == 8 /\ c == 3) /\
    Vale.X64.Decls.validSrcAddrs128 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rR9 va_s0 - 32)
    hkeys_b 8 (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs128
    (va_get_mem_heaplet 3 va_s0) (va_get_reg64 rRbp va_s0) scratch_b 8 (va_get_mem_layout va_s0)
    Secret /\ (0 <= power_index /\ power_index < 8) /\ (let z0 = (if (m = 1) then va_eval_xmm va_s0
    a1 else va_get_xmm 4 va_s0) in (m > 0 ==> add (add (Vale.Math.Poly2.Bits_s.of_quad32 z0)
    (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_s0)) 64))
    (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_s0)) 128) ==
    Vale.AES.GHash.ghash_unroll_back h prev pdata 0 6 (m - 1)) /\ (m < 5 ==> va_eval_xmm va_s0 b ==
    Vale.Def.Types_s.reverse_bytes_quad32 (va_subscript_FStar__Seq__Base__seq data (5 - m))) /\ (m
    == 5 ==> Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_xmm va_s0 b) == add prev
    (Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32
    (va_subscript_FStar__Seq__Base__seq data (5 - m))))) /\ (m == 0 ==>
    Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_xmm va_s0 c) == Vale.AES.GHash.gf128_power h (m + 1))
    /\ Vale.Math.Poly2.Bits_s.of_quad32 (Vale.X64.Decls.buffer128_read hkeys_b power_index
    (va_get_mem_heaplet 0 va_s0)) == Vale.AES.GHash.gf128_power h (m + 1)))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128
    data in (m < 4 ==> va_get_xmm 0 va_sM == Vale.X64.Decls.buffer128_read scratch_b (3 + m)
    (va_get_mem_heaplet 3 va_sM)) /\ (let z0 = (if (m = 0) then va_eval_xmm va_sM a0 else
    va_get_xmm 4 va_sM) in add (add (Vale.Math.Poly2.Bits_s.of_quad32 z0) (Vale.Math.Poly2_s.shift
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_sM)) 64)) (Vale.Math.Poly2_s.shift
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_sM)) 128) ==
    Vale.AES.GHash.ghash_unroll_back h prev pdata 0 6 m /\ (m == 0 ==>
    Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_sM) == add (add
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_s0)) (Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 4 va_s0))) (Vale.Math.Poly2.Bits_s.of_quad32 (Vale.X64.Decls.buffer128_read
    scratch_b 1 (va_get_mem_heaplet 3 va_s0)))) /\ (m == 4 ==> Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 8 va_sM) == add (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_s0))
    (Vale.Math.Poly2.Bits_s.of_quad32 (Vale.X64.Decls.buffer128_read scratch_b 7
    (va_get_mem_heaplet 3 va_s0)))) /\ (0 < m /\ m < 4 ==> va_get_xmm 8 va_sM == va_get_xmm 8
    va_s0))) /\ va_state_eq va_sM (va_update_xmm 8 va_sM (va_update_xmm 7 va_sM (va_update_xmm 6
    va_sM (va_update_xmm 4 va_sM (va_update_xmm 0 va_sM (va_update_flags va_sM (va_update_ok va_sM
    (va_update_operand_xmm c va_sM (va_update_operand_xmm b va_sM (va_update_operand_xmm a3 va_sM
    (va_update_operand_xmm a2 va_sM (va_update_operand_xmm a1 va_sM (va_update_operand_xmm a0 va_sM
    va_s0)))))))))))))))

    va_b0: Vale.X64.Decls.va_code ->
    va_s0: Vale.X64.Decls.va_state ->
    m: Prims.nat ->
    power_index: Prims.int ->
    a0: Vale.X64.Decls.va_operand_xmm ->
    a1: Vale.X64.Decls.va_operand_xmm ->
    a2: Vale.X64.Decls.va_operand_xmm ->
    a3: Vale.X64.Decls.va_operand_xmm ->
    b: Vale.X64.Decls.va_operand_xmm ->
    c: Vale.X64.Decls.va_operand_xmm ->
    hkeys_b: Vale.X64.Memory.buffer128 ->
    scratch_b: Vale.X64.Memory.buffer128 ->
    h: Vale.Math.Poly2_s.poly ->
    prev: Vale.Math.Poly2_s.poly ->
    data: FStar.Seq.Base.seq Vale.X64.Decls.quad32
  -> Prims.Ghost (Vale.X64.Decls.va_state * Vale.X64.Decls.va_fuel)