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
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 ()))))
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
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 ()))))
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
Prims.nat Prims.int Vale.X64.Decls.va_operand_xmm Vale.X64.Decls.va_Block Vale.X64.Decls.va_CCons Prims.op_Equality Vale.AES.X64.PolyOps.va_code_VPolyMul Vale.AES.X64.PolyOps.va_code_VPolyAdd Vale.X64.Decls.va_op_xmm_xmm Vale.X64.Decls.va_coerce_xmm_to_opr128 Vale.X64.Decls.va_op_opr128_xmm Vale.X64.InsVector.va_code_Mem128_lemma Vale.X64.Decls.va_opr_code_Mem128 Vale.X64.Decls.va_op_heaplet_mem_heaplet Vale.X64.Decls.va_op_reg64_reg64 Vale.X64.Machine_s.rRbp Vale.Arch.HeapTypes_s.Secret Vale.X64.Decls.va_CNil Prims.bool Vale.X64.InsVector.va_code_Load128_buffer Vale.X64.Decls.va_op_reg_opr64_reg64 Vale.X64.Machine_s.rR9 Prims.op_Subtraction Prims.op_Multiply Vale.X64.Decls.va_code Prims.op_LessThan Prims.op_Addition
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"]
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

    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
  -> Vale.X64.Decls.va_code