val va_quick_Ghash_register (hkeys_b: buffer128) (h_LE y_prev: quad32)
    : (va_quickCode unit (va_code_Ghash_register ()))
val va_quick_Ghash_register (hkeys_b: buffer128) (h_LE y_prev: quad32)
    : (va_quickCode unit (va_code_Ghash_register ()))
let va_quick_Ghash_register (hkeys_b:buffer128) (h_LE:quad32) (y_prev:quad32) : (va_quickCode unit
  (va_code_Ghash_register ())) =
  (va_QProc (va_code_Ghash_register ()) ([va_Mod_xmm 8; va_Mod_xmm 7; va_Mod_xmm 6; va_Mod_xmm 5;
    va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm 2; va_Mod_xmm 1; va_Mod_xmm 0; va_Mod_reg64 rR11;
    va_Mod_flags]) (va_wp_Ghash_register hkeys_b h_LE y_prev) (va_wpProof_Ghash_register hkeys_b
    h_LE y_prev))
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"

unfold let va_subscript_FStar__Seq__Base__seq = Seq.index

let hkeys_b_powers (hkeys_b:buffer128) (heap0:vale_heap) (layout:vale_heap_layout) (ptr:int) (h:poly) =
  validSrcAddrs128 heap0 ptr hkeys_b 8 layout Secret /\
  of_quad32 (buffer128_read hkeys_b 0 heap0) == gf128_power h 1 /\
  of_quad32 (buffer128_read hkeys_b 1 heap0) == gf128_power h 2 /\
  of_quad32 (buffer128_read hkeys_b 3 heap0) == gf128_power h 3 /\
  of_quad32 (buffer128_read hkeys_b 4 heap0) == gf128_power h 4 /\
  of_quad32 (buffer128_read hkeys_b 6 heap0) == gf128_power h 5 /\
  of_quad32 (buffer128_read hkeys_b 7 heap0) == gf128_power h 6

let quad32_opt_rev (b:bool) (q:quad32) : quad32 =
  if b then reverse_bytes_quad32 q else q

let index_opt_rev (b:bool) (len n i:int) : int =
  if b then len - 1 - i else len - n + i

let scratch_b_blocks
    (rev_bytes:bool) (rev_blocks:bool) (scratch_in_b:buffer128) (scratch_len count:int) (heap_s:vale_heap)
    (data:seq quad32)
  =
  (forall (i:nat).{:pattern (index data i)}
    i < count /\ i < length data ==>
      buffer128_read scratch_in_b (index_opt_rev rev_blocks scratch_len (length data) i) heap_s ==
      quad32_opt_rev rev_bytes (index data i))

let scratch_b_data
    (rev_bytes:bool) (rev_blocks:bool) (scratch_in_b:buffer128) (scratch_len count:int) (heap_s:vale_heap)
    (layout:vale_heap_layout) (ptr:int) (data:seq quad32)
  =
  validSrcAddrs128 heap_s ptr scratch_in_b scratch_len layout Secret /\
  scratch_b_blocks rev_bytes rev_blocks scratch_in_b scratch_len count heap_s data
//-- MulAdd_step

val va_code_MulAdd_step : 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 -> Tot va_code

val va_codegen_success_MulAdd_step : 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 -> Tot va_pbool

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_qattr]
let va_wp_MulAdd_step (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)) (va_s0:va_state) (va_k:(va_state
  -> unit -> Type0)) : Type0 =
  (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 = va_if (m = 1) (fun _ ->
    va_eval_xmm va_s0 a1) (fun _ -> 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))) /\ (forall
    (va_x_a0:va_value_xmm) (va_x_a1:va_value_xmm) (va_x_a2:va_value_xmm) (va_x_a3:va_value_xmm)
    (va_x_b:va_value_xmm) (va_x_c:va_value_xmm) (va_x_efl:Vale.X64.Flags.t) (va_x_xmm0:quad32)
    (va_x_xmm4:quad32) (va_x_xmm6:quad32) (va_x_xmm7:quad32) (va_x_xmm8:quad32) . let va_sM =
    va_upd_xmm 8 va_x_xmm8 (va_upd_xmm 7 va_x_xmm7 (va_upd_xmm 6 va_x_xmm6 (va_upd_xmm 4 va_x_xmm4
    (va_upd_xmm 0 va_x_xmm0 (va_upd_flags va_x_efl (va_upd_operand_xmm c va_x_c (va_upd_operand_xmm
    b va_x_b (va_upd_operand_xmm a3 va_x_a3 (va_upd_operand_xmm a2 va_x_a2 (va_upd_operand_xmm a1
    va_x_a1 (va_upd_operand_xmm a0 va_x_a0 va_s0))))))))))) in 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 = va_if (m = 0) (fun _ -> va_eval_xmm va_sM a0) (fun _
    -> 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_k va_sM (())))

val va_wpProof_MulAdd_step : 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) ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_MulAdd_step m power_index a0 a1 a2 a3 b c hkeys_b
    scratch_b h prev data va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_MulAdd_step m power_index a0 a1 a2 a3
    b c) ([va_Mod_xmm 8; va_Mod_xmm 7; va_Mod_xmm 6; va_Mod_xmm 4; va_Mod_xmm 0; va_Mod_flags;
    va_mod_xmm c; va_mod_xmm b; va_mod_xmm a3; va_mod_xmm a2; va_mod_xmm a1; va_mod_xmm a0]) va_s0
    va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_MulAdd_step (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)) : (va_quickCode unit
  (va_code_MulAdd_step m power_index a0 a1 a2 a3 b c)) =
  (va_QProc (va_code_MulAdd_step m power_index a0 a1 a2 a3 b c) ([va_Mod_xmm 8; va_Mod_xmm 7;
    va_Mod_xmm 6; va_Mod_xmm 4; va_Mod_xmm 0; va_Mod_flags; va_mod_xmm c; va_mod_xmm b; va_mod_xmm
    a3; va_mod_xmm a2; va_mod_xmm a1; va_mod_xmm a0]) (va_wp_MulAdd_step m power_index a0 a1 a2 a3
    b c hkeys_b scratch_b h prev data) (va_wpProof_MulAdd_step m power_index a0 a1 a2 a3 b c
    hkeys_b scratch_b h prev data))
//--
//-- ReduceLast

val va_code_ReduceLast : last_adds:bool -> Tot va_code

val va_codegen_success_ReduceLast : last_adds:bool -> Tot va_pbool

val va_lemma_ReduceLast : va_b0:va_code -> va_s0:va_state -> last_adds:bool -> h_LE:quad32 ->
  y_prev:quad32 -> data:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_ReduceLast last_adds) va_s0 /\ va_get_ok va_s0 /\ (let
    (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (prev:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let
    (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in let (n:Prims.nat) = FStar.Seq.Base.length #quad32 data in pclmulqdq_enabled /\ avx_enabled
    /\ va_get_xmm 3 va_s0 == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 0 0 0 3254779904 /\ n
    > 0 /\ add (add (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_s0))
    (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 n (n - 1))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (prev:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let
    (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in let (n:Prims.nat) = FStar.Seq.Base.length #quad32 data in let xi = (if last_adds then
    Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_sM) else add (add
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_sM)) (Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 7 va_sM))) (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_sM))) in
    Vale.Math.Poly2.Bits_s.to_quad32 xi == Vale.Def.Types_s.reverse_bytes_quad32
    (Vale.AES.GHash.ghash_incremental h_LE y_prev data) /\ xi == Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Math.Poly2.Bits_s.to_quad32 xi)) /\ 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 5 va_sM (va_update_xmm 4 va_sM
    (va_update_xmm 3 va_sM (va_update_xmm 0 va_sM (va_update_flags va_sM (va_update_ok va_sM
    va_s0)))))))))))
[@ va_qattr]
let va_wp_ReduceLast (last_adds:bool) (h_LE:quad32) (y_prev:quad32) (data:(seq quad32))
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (let (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (prev:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let
    (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in let (n:Prims.nat) = FStar.Seq.Base.length #quad32 data in pclmulqdq_enabled /\ avx_enabled
    /\ va_get_xmm 3 va_s0 == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 0 0 0 3254779904 /\ n
    > 0 /\ add (add (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_s0))
    (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 n (n - 1)) /\ (forall
    (va_x_efl:Vale.X64.Flags.t) (va_x_xmm0:quad32) (va_x_xmm3:quad32) (va_x_xmm4:quad32)
    (va_x_xmm5:quad32) (va_x_xmm6:quad32) (va_x_xmm7:quad32) (va_x_xmm8:quad32) . let va_sM =
    va_upd_xmm 8 va_x_xmm8 (va_upd_xmm 7 va_x_xmm7 (va_upd_xmm 6 va_x_xmm6 (va_upd_xmm 5 va_x_xmm5
    (va_upd_xmm 4 va_x_xmm4 (va_upd_xmm 3 va_x_xmm3 (va_upd_xmm 0 va_x_xmm0 (va_upd_flags va_x_efl
    va_s0))))))) in va_get_ok va_sM /\ (let (h:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let
    (prev:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let (pdata:(Prims.int ->
    Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in let (n:Prims.nat) =
    FStar.Seq.Base.length #quad32 data in let xi = va_if last_adds (fun _ ->
    Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_sM)) (fun _ -> add (add
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_sM)) (Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 7 va_sM))) (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_sM))) in
    Vale.Math.Poly2.Bits_s.to_quad32 xi == Vale.Def.Types_s.reverse_bytes_quad32
    (Vale.AES.GHash.ghash_incremental h_LE y_prev data) /\ xi == Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Math.Poly2.Bits_s.to_quad32 xi)) ==> va_k va_sM (())))

val va_wpProof_ReduceLast : last_adds:bool -> h_LE:quad32 -> y_prev:quad32 -> data:(seq quad32) ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_ReduceLast last_adds h_LE y_prev data va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_ReduceLast last_adds) ([va_Mod_xmm 8;
    va_Mod_xmm 7; va_Mod_xmm 6; va_Mod_xmm 5; va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm 0;
    va_Mod_flags]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_ReduceLast (last_adds:bool) (h_LE:quad32) (y_prev:quad32) (data:(seq quad32)) :
  (va_quickCode unit (va_code_ReduceLast last_adds)) =
  (va_QProc (va_code_ReduceLast last_adds) ([va_Mod_xmm 8; va_Mod_xmm 7; va_Mod_xmm 6; va_Mod_xmm
    5; va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm 0; va_Mod_flags]) (va_wp_ReduceLast last_adds h_LE
    y_prev data) (va_wpProof_ReduceLast last_adds h_LE y_prev data))
//--
//-- GhashUnroll_n

val va_code_GhashUnroll_n : rev_bytes:bool -> rev_blocks:bool -> exactly6:bool -> Tot va_code

val va_codegen_success_GhashUnroll_n : rev_bytes:bool -> rev_blocks:bool -> exactly6:bool -> Tot
  va_pbool

val va_lemma_GhashUnroll_n : va_b0:va_code -> va_s0:va_state -> rev_bytes:bool -> rev_blocks:bool
  -> exactly6:bool -> scratch_len:nat64 -> hkeys_b:buffer128 -> scratch_in_b:buffer128 ->
  h_LE:quad32 -> y_prev:quad32 -> data:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_GhashUnroll_n rev_bytes rev_blocks exactly6) va_s0 /\
    va_get_ok va_s0 /\ (let (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (prev:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let
    (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in let (n:Prims.nat) = FStar.Seq.Base.length #quad32 data in let (scratch_index:int) =
    index_opt_rev rev_blocks scratch_len n (n - 1) in pclmulqdq_enabled /\ avx_enabled /\
    sse_enabled /\ (exactly6 ==> n == 6) /\ (~exactly6 ==> 1 <= n /\ n < 6) /\ n <= scratch_len /\
    hkeys_b_powers hkeys_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_layout va_s0) (va_get_reg64 rR9
    va_s0 - 32) h /\ scratch_b_data rev_bytes rev_blocks scratch_in_b scratch_len 6
    (va_get_mem_heaplet 1 va_s0) (va_get_mem_layout va_s0) (va_get_reg64 rRdi va_s0) data /\
    va_get_reg64 rRdi va_s0 + 16 `op_Multiply` scratch_len <= pow2_64 /\
    Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_s0) == prev /\ (~exactly6 ==> va_get_reg64
    rRdx va_s0 == n) /\ va_get_reg64 rR11 va_s0 == va_get_reg64 rRdi va_s0 + 16 `op_Multiply`
    scratch_index /\ (~rev_bytes ==> va_get_xmm 9 va_s0 == Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat32 202182159 134810123 67438087 66051))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (prev:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let
    (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in let (n:Prims.nat) = FStar.Seq.Base.length #quad32 data in let (scratch_index:int) =
    index_opt_rev rev_blocks scratch_len n (n - 1) in va_get_xmm 8 va_sM ==
    Vale.Def.Types_s.reverse_bytes_quad32 (Vale.AES.GHash.ghash_incremental h_LE y_prev data) /\
    (l_and exactly6 (~rev_blocks) ==> va_get_reg64 rR11 va_sM == va_get_reg64 rR11 va_s0 - 80)) /\
    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 5 va_sM (va_update_xmm 4 va_sM (va_update_xmm 3 va_sM (va_update_xmm 2 va_sM
    (va_update_xmm 1 va_sM (va_update_xmm 0 va_sM (va_update_reg64 rR11 va_sM (va_update_reg64 rR10
    va_sM (va_update_flags va_sM (va_update_ok va_sM va_s0)))))))))))))))
[@ va_qattr]
let va_wp_GhashUnroll_n (rev_bytes:bool) (rev_blocks:bool) (exactly6:bool) (scratch_len:nat64)
  (hkeys_b:buffer128) (scratch_in_b:buffer128) (h_LE:quad32) (y_prev:quad32) (data:(seq quad32))
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (let (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (prev:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let
    (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in let (n:Prims.nat) = FStar.Seq.Base.length #quad32 data in let (scratch_index:int) =
    index_opt_rev rev_blocks scratch_len n (n - 1) in pclmulqdq_enabled /\ avx_enabled /\
    sse_enabled /\ (exactly6 ==> n == 6) /\ (~exactly6 ==> 1 <= n /\ n < 6) /\ n <= scratch_len /\
    hkeys_b_powers hkeys_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_layout va_s0) (va_get_reg64 rR9
    va_s0 - 32) h /\ scratch_b_data rev_bytes rev_blocks scratch_in_b scratch_len 6
    (va_get_mem_heaplet 1 va_s0) (va_get_mem_layout va_s0) (va_get_reg64 rRdi va_s0) data /\
    va_get_reg64 rRdi va_s0 + 16 `op_Multiply` scratch_len <= pow2_64 /\
    Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_s0) == prev /\ (~exactly6 ==> va_get_reg64
    rRdx va_s0 == n) /\ va_get_reg64 rR11 va_s0 == va_get_reg64 rRdi va_s0 + 16 `op_Multiply`
    scratch_index /\ (~rev_bytes ==> va_get_xmm 9 va_s0 == Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat32 202182159 134810123 67438087 66051)) /\ (forall
    (va_x_efl:Vale.X64.Flags.t) (va_x_r10:nat64) (va_x_r11:nat64) (va_x_xmm0:quad32)
    (va_x_xmm1:quad32) (va_x_xmm2:quad32) (va_x_xmm3:quad32) (va_x_xmm4:quad32) (va_x_xmm5:quad32)
    (va_x_xmm6:quad32) (va_x_xmm7:quad32) (va_x_xmm8:quad32) . let va_sM = va_upd_xmm 8 va_x_xmm8
    (va_upd_xmm 7 va_x_xmm7 (va_upd_xmm 6 va_x_xmm6 (va_upd_xmm 5 va_x_xmm5 (va_upd_xmm 4 va_x_xmm4
    (va_upd_xmm 3 va_x_xmm3 (va_upd_xmm 2 va_x_xmm2 (va_upd_xmm 1 va_x_xmm1 (va_upd_xmm 0 va_x_xmm0
    (va_upd_reg64 rR11 va_x_r11 (va_upd_reg64 rR10 va_x_r10 (va_upd_flags va_x_efl va_s0)))))))))))
    in va_get_ok va_sM /\ (let (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (prev:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let
    (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in let (n:Prims.nat) = FStar.Seq.Base.length #quad32 data in let (scratch_index:int) =
    index_opt_rev rev_blocks scratch_len n (n - 1) in va_get_xmm 8 va_sM ==
    Vale.Def.Types_s.reverse_bytes_quad32 (Vale.AES.GHash.ghash_incremental h_LE y_prev data) /\
    (l_and exactly6 (~rev_blocks) ==> va_get_reg64 rR11 va_sM == va_get_reg64 rR11 va_s0 - 80)) ==>
    va_k va_sM (())))

val va_wpProof_GhashUnroll_n : rev_bytes:bool -> rev_blocks:bool -> exactly6:bool ->
  scratch_len:nat64 -> hkeys_b:buffer128 -> scratch_in_b:buffer128 -> h_LE:quad32 -> y_prev:quad32
  -> data:(seq quad32) -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_GhashUnroll_n rev_bytes rev_blocks exactly6 scratch_len
    hkeys_b scratch_in_b h_LE y_prev data va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_GhashUnroll_n rev_bytes rev_blocks
    exactly6) ([va_Mod_xmm 8; va_Mod_xmm 7; va_Mod_xmm 6; va_Mod_xmm 5; va_Mod_xmm 4; va_Mod_xmm 3;
    va_Mod_xmm 2; va_Mod_xmm 1; va_Mod_xmm 0; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_flags])
    va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_GhashUnroll_n (rev_bytes:bool) (rev_blocks:bool) (exactly6:bool) (scratch_len:nat64)
  (hkeys_b:buffer128) (scratch_in_b:buffer128) (h_LE:quad32) (y_prev:quad32) (data:(seq quad32)) :
  (va_quickCode unit (va_code_GhashUnroll_n rev_bytes rev_blocks exactly6)) =
  (va_QProc (va_code_GhashUnroll_n rev_bytes rev_blocks exactly6) ([va_Mod_xmm 8; va_Mod_xmm 7;
    va_Mod_xmm 6; va_Mod_xmm 5; va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm 2; va_Mod_xmm 1; va_Mod_xmm
    0; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_flags]) (va_wp_GhashUnroll_n rev_bytes
    rev_blocks exactly6 scratch_len hkeys_b scratch_in_b h_LE y_prev data)
    (va_wpProof_GhashUnroll_n rev_bytes rev_blocks exactly6 scratch_len hkeys_b scratch_in_b h_LE
    y_prev data))
//--
//-- Ghash_register

val va_code_Ghash_register : va_dummy:unit -> Tot va_code

val va_codegen_success_Ghash_register : va_dummy:unit -> Tot va_pbool

val va_lemma_Ghash_register : va_b0:va_code -> va_s0:va_state -> hkeys_b:buffer128 -> h_LE:quad32
  -> y_prev:quad32
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Ghash_register ()) va_s0 /\ va_get_ok va_s0 /\ (let
    (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (data:(FStar.Seq.Base.seq
    Vale.Def.Types_s.quad32)) = FStar.Seq.Base.create #Vale.Def.Types_s.quad32 1
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 0 va_s0)) in let
    (prev:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let (pdata:(Prims.int ->
    Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in pclmulqdq_enabled
    /\ avx_enabled /\ sse_enabled /\ hkeys_b_powers hkeys_b (va_get_mem_heaplet 0 va_s0)
    (va_get_mem_layout va_s0) (va_get_reg64 rR9 va_s0 - 32) h /\ Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 8 va_s0) == prev)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (data:(FStar.Seq.Base.seq
    Vale.Def.Types_s.quad32)) = FStar.Seq.Base.create #Vale.Def.Types_s.quad32 1
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 0 va_s0)) in let
    (prev:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let (pdata:(Prims.int ->
    Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in va_get_xmm 8 va_sM
    == Vale.Def.Types_s.reverse_bytes_quad32 (Vale.AES.GHash.ghash_incremental h_LE y_prev data))
    /\ 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 5 va_sM (va_update_xmm 4 va_sM (va_update_xmm 3 va_sM (va_update_xmm 2 va_sM
    (va_update_xmm 1 va_sM (va_update_xmm 0 va_sM (va_update_reg64 rR11 va_sM (va_update_flags
    va_sM (va_update_ok va_sM va_s0))))))))))))))
[@ va_qattr]
let va_wp_Ghash_register (hkeys_b:buffer128) (h_LE:quad32) (y_prev:quad32) (va_s0:va_state)
  (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (let (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (data:(FStar.Seq.Base.seq
    Vale.Def.Types_s.quad32)) = FStar.Seq.Base.create #Vale.Def.Types_s.quad32 1
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 0 va_s0)) in let
    (prev:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let (pdata:(Prims.int ->
    Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in pclmulqdq_enabled
    /\ avx_enabled /\ sse_enabled /\ hkeys_b_powers hkeys_b (va_get_mem_heaplet 0 va_s0)
    (va_get_mem_layout va_s0) (va_get_reg64 rR9 va_s0 - 32) h /\ Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 8 va_s0) == prev) /\ (forall (va_x_efl:Vale.X64.Flags.t) (va_x_r11:nat64)
    (va_x_xmm0:quad32) (va_x_xmm1:quad32) (va_x_xmm2:quad32) (va_x_xmm3:quad32) (va_x_xmm4:quad32)
    (va_x_xmm5:quad32) (va_x_xmm6:quad32) (va_x_xmm7:quad32) (va_x_xmm8:quad32) . let va_sM =
    va_upd_xmm 8 va_x_xmm8 (va_upd_xmm 7 va_x_xmm7 (va_upd_xmm 6 va_x_xmm6 (va_upd_xmm 5 va_x_xmm5
    (va_upd_xmm 4 va_x_xmm4 (va_upd_xmm 3 va_x_xmm3 (va_upd_xmm 2 va_x_xmm2 (va_upd_xmm 1 va_x_xmm1
    (va_upd_xmm 0 va_x_xmm0 (va_upd_reg64 rR11 va_x_r11 (va_upd_flags va_x_efl va_s0)))))))))) in
    va_get_ok va_sM /\ (let (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (data:(FStar.Seq.Base.seq
    Vale.Def.Types_s.quad32)) = FStar.Seq.Base.create #Vale.Def.Types_s.quad32 1
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 0 va_s0)) in let
    (prev:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let (pdata:(Prims.int ->
    Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in va_get_xmm 8 va_sM
    == Vale.Def.Types_s.reverse_bytes_quad32 (Vale.AES.GHash.ghash_incremental h_LE y_prev data))
    ==> va_k va_sM (())))

val va_wpProof_Ghash_register : hkeys_b:buffer128 -> h_LE:quad32 -> y_prev:quad32 -> va_s0:va_state
  -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Ghash_register hkeys_b h_LE y_prev va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Ghash_register ()) ([va_Mod_xmm 8;
    va_Mod_xmm 7; va_Mod_xmm 6; va_Mod_xmm 5; va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm 2; va_Mod_xmm
    1; va_Mod_xmm 0; va_Mod_reg64 rR11; va_Mod_flags]) va_s0 va_k ((va_sM, va_f0, va_g))))
/
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.fsti
hkeys_b: Vale.X64.Memory.buffer128 -> h_LE: Vale.X64.Decls.quad32 -> y_prev: Vale.X64.Decls.quad32
  -> Vale.X64.QuickCode.va_quickCode Prims.unit (Vale.AES.X64.AESopt2.va_code_Ghash_register ())
Vale.X64.Memory.buffer128 Vale.X64.Decls.quad32 Vale.X64.QuickCode.va_QProc Prims.unit Vale.AES.X64.AESopt2.va_code_Ghash_register Prims.Cons Vale.X64.QuickCode.mod_t Vale.X64.QuickCode.va_Mod_xmm Vale.X64.QuickCode.va_Mod_reg64 Vale.X64.Machine_s.rR11 Vale.X64.QuickCode.va_Mod_flags Prims.Nil Vale.AES.X64.AESopt2.va_wp_Ghash_register Vale.AES.X64.AESopt2.va_wpProof_Ghash_register Vale.X64.QuickCode.va_quickCode
let va_quick_Ghash_register (hkeys_b: buffer128) (h_LE y_prev: quad32)
    : (va_quickCode unit (va_code_Ghash_register ())) =
  
(va_QProc (va_code_Ghash_register ())
    ([
        va_Mod_xmm 8; va_Mod_xmm 7; va_Mod_xmm 6; va_Mod_xmm 5; va_Mod_xmm 4; va_Mod_xmm 3;
        va_Mod_xmm 2; va_Mod_xmm 1; va_Mod_xmm 0; va_Mod_reg64 rR11; va_Mod_flags
      ])
    (va_wp_Ghash_register hkeys_b h_LE y_prev)
    (va_wpProof_Ghash_register hkeys_b h_LE y_prev))