val va_wpProof_Fast_multiply_a2b : offset:nat -> dst_b:buffer64 -> inA_b:buffer64 -> inB_b:buffer64
  -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Fast_multiply_a2b offset dst_b inA_b inB_b va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Fast_multiply_a2b offset)
    ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64 rR13; va_Mod_reg64 rRbx;
    va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx;
    va_Mod_reg64 rRax; va_Mod_mem]) va_s0 va_k ((va_sM, va_f0, va_g))))
let va_wpProof_Fast_multiply_a2b offset dst_b inA_b inB_b va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Fast_multiply_a2b (va_code_Fast_multiply_a2b offset) va_s0 offset
    dst_b inA_b inB_b in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_mem_heaplet 0 va_sM (va_update_reg64
    rR14 va_sM (va_update_reg64 rR13 va_sM (va_update_reg64 rRbx va_sM (va_update_reg64 rR11 va_sM
    (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM (va_update_reg64 rR8 va_sM
    (va_update_reg64 rRdx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem
    va_sM va_s0))))))))))))));
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64 rR13;
    va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8;
    va_Mod_reg64 rRdx; va_Mod_reg64 rRax; va_Mod_mem]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)
val va_wpProof_Fast_multiply_a2b : offset:nat -> dst_b:buffer64 -> inA_b:buffer64 -> inB_b:buffer64
  -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Fast_multiply_a2b offset dst_b inA_b inB_b va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Fast_multiply_a2b offset)
    ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64 rR13; va_Mod_reg64 rRbx;
    va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx;
    va_Mod_reg64 rRax; va_Mod_mem]) va_s0 va_k ((va_sM, va_f0, va_g))))
let va_wpProof_Fast_multiply_a2b offset dst_b inA_b inB_b va_s0 va_k =
let va_sM, va_f0 =
  va_lemma_Fast_multiply_a2b (va_code_Fast_multiply_a2b offset) va_s0 offset dst_b inA_b inB_b
in
va_lemma_upd_update va_sM;
assert (va_state_eq va_sM
      (va_update_flags va_sM
          (va_update_mem_heaplet 0
              va_sM
              (va_update_reg64 rR14
                  va_sM
                  (va_update_reg64 rR13
                      va_sM
                      (va_update_reg64 rRbx
                          va_sM
                          (va_update_reg64 rR11
                              va_sM
                              (va_update_reg64 rR10
                                  va_sM
                                  (va_update_reg64 rR9
                                      va_sM
                                      (va_update_reg64 rR8
                                          va_sM
                                          (va_update_reg64 rRdx
                                              va_sM
                                              (va_update_reg64 rRax
                                                  va_sM
                                                  (va_update_ok va_sM (va_update_mem va_sM va_s0))))
                                      ))))))))));
va_lemma_norm_mods ([
      va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64 rR13; va_Mod_reg64 rRbx;
      va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx;
      va_Mod_reg64 rRax; va_Mod_mem
    ])
  va_sM
  va_s0;
let va_g = () in
(va_sM, va_f0, va_g)
Vale.Curve25519.X64.FastMul.fst.checked
Vale.X64.State.fsti.checked Vale.X64.Stack_i.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.InsStack.fsti.checked Vale.X64.InsMem.fsti.checked Vale.X64.InsBasic.fsti.checked Vale.X64.Flags.fsti.checked Vale.X64.Decls.fsti.checked Vale.X64.CPU_Features_s.fst.checked Vale.Def.Types_s.fst.checked Vale.Curve25519.FastMul_helpers.fsti.checked Vale.Curve25519.Fast_lemmas_external.fsti.checked Vale.Curve25519.Fast_defs.fst.checked Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.Curve25519.X64.FastMul.fst
Prims.nat Vale.X64.Memory.buffer64 Vale.X64.Decls.va_state Prims.unit Vale.X64.Decls.va_fuel FStar.Pervasives.Native.Mktuple3 Vale.X64.QuickCode.va_lemma_norm_mods Prims.Cons Vale.X64.QuickCode.mod_t Vale.X64.QuickCode.va_Mod_flags Vale.X64.QuickCode.va_Mod_mem_heaplet Vale.X64.QuickCode.va_Mod_reg64 Vale.X64.Machine_s.rR14 Vale.X64.Machine_s.rR13 Vale.X64.Machine_s.rRbx Vale.X64.Machine_s.rR11 Vale.X64.Machine_s.rR10 Vale.X64.Machine_s.rR9 Vale.X64.Machine_s.rR8 Vale.X64.Machine_s.rRdx Vale.X64.Machine_s.rRax Vale.X64.QuickCode.va_Mod_mem Prims.Nil Prims._assert Vale.X64.Decls.va_state_eq Vale.X64.Decls.va_update_flags Vale.X64.Decls.va_update_mem_heaplet Vale.X64.Decls.va_update_reg64 Vale.X64.Decls.va_update_ok Vale.X64.Decls.va_update_mem Vale.X64.Decls.va_lemma_upd_update FStar.Pervasives.Native.tuple3 FStar.Pervasives.Native.tuple2 Vale.X64.State.vale_state Vale.Curve25519.X64.FastMul.va_lemma_Fast_multiply_a2b Vale.Curve25519.X64.FastMul.va_code_Fast_multiply_a2b
module Vale.Curve25519.X64.FastMul
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.Stack_i
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsMem
open Vale.X64.InsStack
open Vale.X64.QuickCode
open Vale.X64.QuickCodes
open FStar.Tactics
open Vale.Curve25519.Fast_defs
open Vale.Curve25519.Fast_lemmas_external
open Vale.Curve25519.FastMul_helpers
open Vale.X64.CPU_Features_s
#reset-options "--z3rlimit 60"
//-- Fast_multiply_a0b
#push-options "--z3rlimit 200"

val va_code_Fast_multiply_a0b : offset:nat -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Fast_multiply_a0b offset =
  (va_Block (va_CCons (va_code_Comment
    "Compute src1[0] * src2"
    ) (va_CCons (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (0 + 8 `op_Multiply` offset) Secret) (va_CCons (va_code_NoNewline
    ()) (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx64 (va_op_dst_opr64_reg64 rR9)
    (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64
    rRcx) (0 + offset `op_Multiply` 8) Secret)) (va_CCons (va_code_Space 3) (va_CCons
    (va_code_Xor64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR10)) (va_CCons (va_code_Space
    1) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR8) (0 + offset `op_Multiply` 16) Secret) (va_CCons (va_code_Newline
    ()) (va_CCons (va_code_NoNewline ()) (va_CCons (va_code_Mem64_lemma ()) (va_CCons
    (va_code_Mulx64 (va_op_dst_opr64_reg64 rR11) (va_op_dst_opr64_reg64 rR10) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (8 + offset `op_Multiply` 8) Secret))
    (va_CCons (va_code_Space 1) (va_CCons (va_code_Adox64Wrap (va_op_dst_opr64_reg64 rR10)
    (va_op_opr64_reg64 rR9)) (va_CCons (va_code_Space 1) (va_CCons (va_code_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR10) (8 +
    offset `op_Multiply` 16) Secret) (va_CCons (va_code_Newline ()) (va_CCons (va_code_NoNewline
    ()) (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx64 (va_op_dst_opr64_reg64 rR13)
    (va_op_dst_opr64_reg64 rRbx) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (16 + offset `op_Multiply` 8) Secret)) (va_CCons (va_code_Adox64Wrap
    (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR11)) (va_CCons (va_code_NoNewline ())
    (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx64 (va_op_dst_opr64_reg64 rRdx)
    (va_op_dst_opr64_reg64 rR14) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (24 + offset `op_Multiply` 8) Secret)) (va_CCons (va_code_NoNewline
    ()) (va_CCons (va_code_Adox64Wrap (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rR13))
    (va_CCons (va_code_Mov64 (va_op_dst_opr64_reg64 rRax) (va_const_opr64 0)) (va_CCons
    (va_code_Space 35) (va_CCons (va_code_Adox64Wrap (va_op_dst_opr64_reg64 rRax)
    (va_op_opr64_reg64 rRdx)) (va_CNil ()))))))))))))))))))))))))))))))))

val va_codegen_success_Fast_multiply_a0b : offset:nat -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Fast_multiply_a0b offset =
  (va_pbool_and (va_codegen_success_Comment
    "Compute src1[0] * src2"
    ) (va_pbool_and (va_codegen_success_Load64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_dst_opr64_reg64 rRdx) (va_op_reg_opr64_reg64 rRsi) (0 + 8 `op_Multiply` offset) Secret)
    (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Mem64_lemma
    ()) (va_pbool_and (va_codegen_success_Mulx64 (va_op_dst_opr64_reg64 rR9) (va_op_dst_opr64_reg64
    rR8) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (0 + offset
    `op_Multiply` 8) Secret)) (va_pbool_and (va_codegen_success_Space 3) (va_pbool_and
    (va_codegen_success_Xor64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR10)) (va_pbool_and
    (va_codegen_success_Space 1) (va_pbool_and (va_codegen_success_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR8) (0 +
    offset `op_Multiply` 16) Secret) (va_pbool_and (va_codegen_success_Newline ()) (va_pbool_and
    (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Mem64_lemma ())
    (va_pbool_and (va_codegen_success_Mulx64 (va_op_dst_opr64_reg64 rR11) (va_op_dst_opr64_reg64
    rR10) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (8 + offset
    `op_Multiply` 8) Secret)) (va_pbool_and (va_codegen_success_Space 1) (va_pbool_and
    (va_codegen_success_Adox64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR9))
    (va_pbool_and (va_codegen_success_Space 1) (va_pbool_and (va_codegen_success_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR10) (8 +
    offset `op_Multiply` 16) Secret) (va_pbool_and (va_codegen_success_Newline ()) (va_pbool_and
    (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Mem64_lemma ())
    (va_pbool_and (va_codegen_success_Mulx64 (va_op_dst_opr64_reg64 rR13) (va_op_dst_opr64_reg64
    rRbx) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (16 + offset
    `op_Multiply` 8) Secret)) (va_pbool_and (va_codegen_success_Adox64Wrap (va_op_dst_opr64_reg64
    rRbx) (va_op_opr64_reg64 rR11)) (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and
    (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx64
    (va_op_dst_opr64_reg64 rRdx) (va_op_dst_opr64_reg64 rR14) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (24 + offset `op_Multiply` 8) Secret))
    (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Adox64Wrap
    (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rR13)) (va_pbool_and (va_codegen_success_Mov64
    (va_op_dst_opr64_reg64 rRax) (va_const_opr64 0)) (va_pbool_and (va_codegen_success_Space 35)
    (va_pbool_and (va_codegen_success_Adox64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64
    rRdx)) (va_ttrue ())))))))))))))))))))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Fast_multiply_a0b (va_mods:va_mods_t) (offset:nat) (dst_b:buffer64) (inA_b:buffer64)
  (inB_b:buffer64) : (va_quickCode unit (va_code_Fast_multiply_a0b offset)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s) in let (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (0 + offset) (va_get_mem_heaplet 0 va_s) in let (b1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (1 + offset) (va_get_mem_heaplet 0 va_s) in let
    (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (2 + offset)
    (va_get_mem_heaplet 0 va_s) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (3 + offset) (va_get_mem_heaplet 0 va_s) in let (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 106 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Arch.Types.xor_lemmas ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 115 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Comment
    "Compute src1[0] * src2"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 116 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (0 + 8 `op_Multiply` offset) Secret inA_b (0 + offset)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 118 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 119 column 26 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (0 + offset
    `op_Multiply` 8) inB_b (0 + offset) Secret) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 119 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rR9) (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (0 + offset `op_Multiply` 8) Secret))
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 120 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Space 3) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 121 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Xor64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR10)) (fun (va_s:va_state) _
    -> let (va_arg75:Vale.Def.Types_s.nat64) = va_get_reg64 rR8 va_s in let
    (va_arg74:Vale.Def.Types_s.nat64) = va_get_reg64 rR9 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 122 column 22 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg74 va_arg75 a0
    b0) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 123 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 124 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR8) (0 + offset `op_Multiply` 16) Secret dst_b (0 + offset
    `op_Multiply` 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 126 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 127 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 128 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (8 + offset
    `op_Multiply` 8) inB_b (1 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 128 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rR11) (va_op_dst_opr64_reg64 rR10) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (8 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (a0b1_lo:nat64) = va_get_reg64 rR10 va_s in let
    (va_arg73:Vale.Def.Types_s.nat64) = va_get_reg64 rR10 va_s in let
    (va_arg72:Vale.Def.Types_s.nat64) = va_get_reg64 rR11 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 129 column 42 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg72 va_arg73 a0
    b1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 130 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 131 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adox64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR9)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 132 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Space 1) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 133 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR10) (8 + offset `op_Multiply` 16) Secret dst_b (1 + offset
    `op_Multiply` 2)) (fun (va_s:va_state) _ -> let (d0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in
    let (d1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read dst_b (1 + offset `op_Multiply`
    2) (va_get_mem_heaplet 0 va_s) in let (overflow0:bool) = Vale.X64.Decls.overflow (va_get_flags
    va_s) in let (carry:(va_int_range 0 1)) = va_if (Vale.X64.Decls.overflow (va_get_flags va_s))
    (fun _ -> 1) (fun _ -> 0) in let (a0b0b1:(va_int_range 0
    6277101735386680764176071790128604879565730051895802724351)) = d0 + va_mul_nat pow2_64 d1 +
    va_mul_nat pow2_128 (va_get_reg64 rR11 va_s + carry) in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 148 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 149 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 150 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (16 + offset
    `op_Multiply` 8) inB_b (2 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 150 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rR13) (va_op_dst_opr64_reg64 rRbx) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (16 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (a0b2_lo:nat64) = va_get_reg64 rRbx va_s in let
    (va_arg71:Vale.Def.Types_s.nat64) = va_get_reg64 rRbx va_s in let
    (va_arg70:Vale.Def.Types_s.nat64) = va_get_reg64 rR13 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 151 column 42 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg70 va_arg71 a0
    b2) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 152 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adox64Wrap (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR11)) (fun
    (va_s:va_state) _ -> let (overflow1:bool) = Vale.X64.Decls.overflow (va_get_flags va_s) in
    va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 155 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 156 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (24 + offset
    `op_Multiply` 8) inB_b (3 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 156 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rRdx) (va_op_dst_opr64_reg64 rR14) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (24 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (a0b3_lo:nat64) = va_get_reg64 rR14 va_s in let
    (va_arg69:Vale.Def.Types_s.nat64) = va_get_reg64 rR14 va_s in let
    (va_arg68:Vale.Def.Types_s.nat64) = va_get_reg64 rRdx va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 157 column 42 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg68 va_arg69 a0
    b3) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 158 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 159 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adox64Wrap (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rR13)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 160 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mov64 (va_op_dst_opr64_reg64 rRax) (va_const_opr64 0)) (fun (va_s:va_state) _ -> let
    (overflow2:bool) = Vale.X64.Decls.overflow (va_get_flags va_s) in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 164 column 57 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Space 35) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 164 column 74 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adox64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRdx)) (fun
    (va_s:va_state) _ -> let carry = va_if overflow2 (fun _ -> 1) (fun _ -> 0) in let
    (carry_new:(va_int_range 0 1)) = va_if (Vale.X64.Decls.overflow (va_get_flags va_s)) (fun _ ->
    1) (fun _ -> 0) in let (a0b:(va_int_range 0
    4271974071841820164790043412339104229205409044713305539894083215644439451561281100045924173873151))
    = d0 + va_mul_nat pow2_64 d1 + va_mul_nat pow2_128 (va_get_reg64 rRbx va_s) + va_mul_nat
    pow2_192 (va_get_reg64 rR14 va_s) + va_mul_nat pow2_256 (va_get_reg64 rRax va_s) + va_mul_nat
    pow2_320 carry_new in let (va_arg67:prop) = va_mul_nat a0 b == va_mul_nat a0 b0 + va_mul_nat
    pow2_64 (va_mul_nat a0 b1) + va_mul_nat pow2_128 (va_mul_nat a0 b2) + va_mul_nat pow2_192
    (va_mul_nat a0 b3) in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 180 column 21 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> assert_by_tactic va_arg67 int_canon) (va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 181 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (a0b == va_mul_nat a0 b) (va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 184 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (carry_new == 0) (va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 185 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_get_reg64 rRax va_s < pow2_64 - 1) (va_QEmpty (()))))))))))))))))))))))))))))))))))))))))))


val va_lemma_Fast_multiply_a0b : va_b0:va_code -> va_s0:va_state -> offset:nat -> dst_b:buffer64 ->
  inA_b:buffer64 -> inB_b:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Fast_multiply_a0b offset) va_s0 /\ va_get_ok va_s0 /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let (b1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in adx_enabled /\
    bmi2_enabled /\ (offset == 0 \/ offset == 4) /\ Vale.X64.Decls.buffers_disjoint dst_b inA_b /\
    Vale.X64.Decls.buffers_disjoint dst_b inB_b /\ Vale.X64.Decls.validDstAddrs64
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) dst_b (8 + offset `op_Multiply` 2)
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) inA_b (4 + offset) (va_get_mem_layout va_s0) Secret /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRcx va_s0) inB_b (4
    + offset) (va_get_mem_layout va_s0) Secret)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let (b1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in let d0 =
    Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in
    let d1 = Vale.X64.Decls.buffer64_read dst_b (1 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in let a0b = d0 + va_mul_nat pow2_64 d1 + va_mul_nat pow2_128 (va_get_reg64 rRbx va_sM)
    + va_mul_nat pow2_192 (va_get_reg64 rR14 va_sM) + va_mul_nat pow2_256 (va_get_reg64 rRax va_sM)
    in a0b == va_mul_nat a0 b /\ va_get_reg64 rRax va_sM < pow2_64 - 1 /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b (8
    + offset `op_Multiply` 2) (va_get_mem_layout va_sM) Secret /\
    Vale.X64.Decls.modifies_buffer_specific dst_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet
    0 va_sM) (0 + offset `op_Multiply` 2) (8 + offset `op_Multiply` 2 - 1)) /\ va_state_eq va_sM
    (va_update_flags va_sM (va_update_mem_heaplet 0 va_sM (va_update_reg64 rR14 va_sM
    (va_update_reg64 rR13 va_sM (va_update_reg64 rRbx va_sM (va_update_reg64 rR11 va_sM
    (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM (va_update_reg64 rR8 va_sM
    (va_update_reg64 rRdx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem
    va_sM va_s0)))))))))))))))
[@"opaque_to_smt"]
let va_lemma_Fast_multiply_a0b va_b0 va_s0 offset dst_b inA_b inB_b =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64
    rR13; va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64
    rR8; va_Mod_reg64 rRdx; va_Mod_reg64 rRax; va_Mod_ok; va_Mod_mem] in
  let va_qc = va_qcode_Fast_multiply_a0b va_mods offset dst_b inA_b inB_b in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Fast_multiply_a0b offset) va_qc va_s0
    (fun va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 53 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_get_ok va_sM) /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 +
    offset) (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (b0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (1 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in label va_range1
    "***** POSTCONDITION NOT MET AT line 95 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (let d0 = Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 96 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (let d1 = Vale.X64.Decls.buffer64_read dst_b (1 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 97 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (let a0b = d0 + va_mul_nat pow2_64 d1 + va_mul_nat pow2_128 (va_get_reg64 rRbx va_sM) +
    va_mul_nat pow2_192 (va_get_reg64 rR14 va_sM) + va_mul_nat pow2_256 (va_get_reg64 rRax va_sM)
    in label va_range1
    "***** POSTCONDITION NOT MET AT line 98 column 22 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (a0b == va_mul_nat a0 b) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 100 column 26 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_get_reg64 rRax va_sM < pow2_64 - 1) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 102 column 80 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b (8
    + offset `op_Multiply` 2) (va_get_mem_layout va_sM) Secret) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 104 column 91 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (Vale.X64.Decls.modifies_buffer_specific dst_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet
    0 va_sM) (0 + offset `op_Multiply` 2) (8 + offset `op_Multiply` 2 - 1))))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64 rR13;
    va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8;
    va_Mod_reg64 rRdx; va_Mod_reg64 rRax; va_Mod_ok; va_Mod_mem]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Fast_multiply_a0b (offset:nat) (dst_b:buffer64) (inA_b:buffer64) (inB_b:buffer64)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 +
    offset) (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (b0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (1 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in adx_enabled /\
    bmi2_enabled /\ (offset == 0 \/ offset == 4) /\ Vale.X64.Decls.buffers_disjoint dst_b inA_b /\
    Vale.X64.Decls.buffers_disjoint dst_b inB_b /\ Vale.X64.Decls.validDstAddrs64
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) dst_b (8 + offset `op_Multiply` 2)
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) inA_b (4 + offset) (va_get_mem_layout va_s0) Secret /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRcx va_s0) inB_b (4
    + offset) (va_get_mem_layout va_s0) Secret) /\ (forall (va_x_mem:vale_heap) (va_x_rax:nat64)
    (va_x_rdx:nat64) (va_x_r8:nat64) (va_x_r9:nat64) (va_x_r10:nat64) (va_x_r11:nat64)
    (va_x_rbx:nat64) (va_x_r13:nat64) (va_x_r14:nat64) (va_x_heap0:vale_heap)
    (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_mem_heaplet 0
    va_x_heap0 (va_upd_reg64 rR14 va_x_r14 (va_upd_reg64 rR13 va_x_r13 (va_upd_reg64 rRbx va_x_rbx
    (va_upd_reg64 rR11 va_x_r11 (va_upd_reg64 rR10 va_x_r10 (va_upd_reg64 rR9 va_x_r9 (va_upd_reg64
    rR8 va_x_r8 (va_upd_reg64 rRdx va_x_rdx (va_upd_reg64 rRax va_x_rax (va_upd_mem va_x_mem
    va_s0))))))))))) in va_get_ok va_sM /\ (let (a0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (1 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (b2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in let d0 =
    Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in
    let d1 = Vale.X64.Decls.buffer64_read dst_b (1 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in let a0b = d0 + va_mul_nat pow2_64 d1 + va_mul_nat pow2_128 (va_get_reg64 rRbx va_sM)
    + va_mul_nat pow2_192 (va_get_reg64 rR14 va_sM) + va_mul_nat pow2_256 (va_get_reg64 rRax va_sM)
    in a0b == va_mul_nat a0 b /\ va_get_reg64 rRax va_sM < pow2_64 - 1 /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b (8
    + offset `op_Multiply` 2) (va_get_mem_layout va_sM) Secret /\
    Vale.X64.Decls.modifies_buffer_specific dst_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet
    0 va_sM) (0 + offset `op_Multiply` 2) (8 + offset `op_Multiply` 2 - 1)) ==> va_k va_sM (())))


val va_wpProof_Fast_multiply_a0b : offset:nat -> dst_b:buffer64 -> inA_b:buffer64 -> inB_b:buffer64
  -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Fast_multiply_a0b offset dst_b inA_b inB_b va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Fast_multiply_a0b offset)
    ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64 rR13; va_Mod_reg64 rRbx;
    va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx;
    va_Mod_reg64 rRax; va_Mod_mem]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Fast_multiply_a0b offset dst_b inA_b inB_b va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Fast_multiply_a0b (va_code_Fast_multiply_a0b offset) va_s0 offset
    dst_b inA_b inB_b in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_mem_heaplet 0 va_sM (va_update_reg64
    rR14 va_sM (va_update_reg64 rR13 va_sM (va_update_reg64 rRbx va_sM (va_update_reg64 rR11 va_sM
    (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM (va_update_reg64 rR8 va_sM
    (va_update_reg64 rRdx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem
    va_sM va_s0))))))))))))));
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64 rR13;
    va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8;
    va_Mod_reg64 rRdx; va_Mod_reg64 rRax; va_Mod_mem]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Fast_multiply_a0b (offset:nat) (dst_b:buffer64) (inA_b:buffer64) (inB_b:buffer64) :
  (va_quickCode unit (va_code_Fast_multiply_a0b offset)) =
  (va_QProc (va_code_Fast_multiply_a0b offset) ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64
    rR14; va_Mod_reg64 rR13; va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64
    rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx; va_Mod_reg64 rRax; va_Mod_mem])
    (va_wp_Fast_multiply_a0b offset dst_b inA_b inB_b) (va_wpProof_Fast_multiply_a0b offset dst_b
    inA_b inB_b))
#pop-options
//--
//-- Fast_multiply_a1b
#push-options "--z3rlimit 2000"

val va_code_Fast_multiply_a1b : offset:nat -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Fast_multiply_a1b offset =
  (va_Block (va_CCons (va_code_Comment
    "Compute src1[1] * src2"
    ) (va_CCons (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (8 + offset `op_Multiply` 8) Secret) (va_CCons (va_code_NoNewline
    ()) (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx64 (va_op_dst_opr64_reg64 rR9)
    (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64
    rRcx) (0 + offset `op_Multiply` 8) Secret)) (va_CCons (va_code_Space 3) (va_CCons
    (va_code_Xor64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR10)) (va_CCons (va_code_Space
    1) (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rR8)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRdi) (8 + offset
    `op_Multiply` 16) Secret)) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR8) (8 + offset `op_Multiply` 16) Secret)
    (va_CCons (va_code_NoNewline ()) (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx64
    (va_op_dst_opr64_reg64 rR11) (va_op_dst_opr64_reg64 rR10) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (8 + offset `op_Multiply` 8) Secret))
    (va_CCons (va_code_Space 1) (va_CCons (va_code_Adox64Wrap (va_op_dst_opr64_reg64 rR10)
    (va_op_opr64_reg64 rR9)) (va_CCons (va_code_Space 1) (va_CCons (va_code_Adcx64Wrap
    (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rRbx)) (va_CCons (va_code_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR10) (16 +
    offset `op_Multiply` 16) Secret) (va_CCons (va_code_NoNewline ()) (va_CCons
    (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx64 (va_op_dst_opr64_reg64 rR13)
    (va_op_dst_opr64_reg64 rRbx) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (16 + offset `op_Multiply` 8) Secret)) (va_CCons (va_code_NoNewline
    ()) (va_CCons (va_code_Adox64Wrap (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR11))
    (va_CCons (va_code_NoNewline ()) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rRbx)
    (va_op_opr64_reg64 rR14)) (va_CCons (va_code_Mov64 (va_op_dst_opr64_reg64 rR8) (va_const_opr64
    0)) (va_CCons (va_code_NoNewline ()) (va_CCons (va_code_Mem64_lemma ()) (va_CCons
    (va_code_Mulx64 (va_op_dst_opr64_reg64 rRdx) (va_op_dst_opr64_reg64 rR14) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (24 + offset `op_Multiply` 8) Secret))
    (va_CCons (va_code_NoNewline ()) (va_CCons (va_code_Adox64Wrap (va_op_dst_opr64_reg64 rR14)
    (va_op_opr64_reg64 rR13)) (va_CCons (va_code_NoNewline ()) (va_CCons (va_code_Adcx64Wrap
    (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rRax)) (va_CCons (va_code_Mov64
    (va_op_dst_opr64_reg64 rRax) (va_const_opr64 0)) (va_CCons (va_code_Space 35) (va_CCons
    (va_code_Adox64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRdx)) (va_CCons
    (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rR8)) (va_CNil
    ()))))))))))))))))))))))))))))))))))))))))

val va_codegen_success_Fast_multiply_a1b : offset:nat -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Fast_multiply_a1b offset =
  (va_pbool_and (va_codegen_success_Comment
    "Compute src1[1] * src2"
    ) (va_pbool_and (va_codegen_success_Load64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_dst_opr64_reg64 rRdx) (va_op_reg_opr64_reg64 rRsi) (8 + offset `op_Multiply` 8) Secret)
    (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Mem64_lemma
    ()) (va_pbool_and (va_codegen_success_Mulx64 (va_op_dst_opr64_reg64 rR9) (va_op_dst_opr64_reg64
    rR8) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (0 + offset
    `op_Multiply` 8) Secret)) (va_pbool_and (va_codegen_success_Space 3) (va_pbool_and
    (va_codegen_success_Xor64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR10)) (va_pbool_and
    (va_codegen_success_Space 1) (va_pbool_and (va_codegen_success_Mem64_lemma ()) (va_pbool_and
    (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRdi) (8 + offset `op_Multiply` 16) Secret))
    (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR8) (8 + offset `op_Multiply` 16) Secret)
    (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Mem64_lemma
    ()) (va_pbool_and (va_codegen_success_Mulx64 (va_op_dst_opr64_reg64 rR11)
    (va_op_dst_opr64_reg64 rR10) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (8 + offset `op_Multiply` 8) Secret)) (va_pbool_and
    (va_codegen_success_Space 1) (va_pbool_and (va_codegen_success_Adox64Wrap
    (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR9)) (va_pbool_and (va_codegen_success_Space
    1) (va_pbool_and (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64
    rRbx)) (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR10) (16 + offset `op_Multiply` 16)
    Secret) (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and
    (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx64
    (va_op_dst_opr64_reg64 rR13) (va_op_dst_opr64_reg64 rRbx) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (16 + offset `op_Multiply` 8) Secret))
    (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Adox64Wrap
    (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR11)) (va_pbool_and
    (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Adcx64Wrap
    (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR14)) (va_pbool_and (va_codegen_success_Mov64
    (va_op_dst_opr64_reg64 rR8) (va_const_opr64 0)) (va_pbool_and (va_codegen_success_NoNewline ())
    (va_pbool_and (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx64
    (va_op_dst_opr64_reg64 rRdx) (va_op_dst_opr64_reg64 rR14) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (24 + offset `op_Multiply` 8) Secret))
    (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Adox64Wrap
    (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rR13)) (va_pbool_and
    (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Adcx64Wrap
    (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_Mov64
    (va_op_dst_opr64_reg64 rRax) (va_const_opr64 0)) (va_pbool_and (va_codegen_success_Space 35)
    (va_pbool_and (va_codegen_success_Adox64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64
    rRdx)) (va_pbool_and (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rRax)
    (va_op_opr64_reg64 rR8)) (va_ttrue ())))))))))))))))))))))))))))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Fast_multiply_a1b (va_mods:va_mods_t) (offset:nat) (dst_b:buffer64) (inA_b:buffer64)
  (inB_b:buffer64) : (va_quickCode unit (va_code_Fast_multiply_a1b offset)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s) in let (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (0 + offset) (va_get_mem_heaplet 0 va_s) in let (b1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (1 + offset) (va_get_mem_heaplet 0 va_s) in let
    (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (2 + offset)
    (va_get_mem_heaplet 0 va_s) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (3 + offset) (va_get_mem_heaplet 0 va_s) in let (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 245 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Comment
    "Compute src1[1] * src2"
    ) (fun (va_s:va_state) _ -> va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 246 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Arch.Types.xor_lemmas ()) (let (a0b_0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in
    let (a0b_1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read dst_b (1 + offset
    `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in let (a0b_2:nat64) = va_get_reg64 rRbx va_s in
    let (a0b_3:nat64) = va_get_reg64 rR14 va_s in let (a0b_4:nat64) = va_get_reg64 rRax va_s in let
    (a0b:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_five a0b_0 a0b_1 a0b_2 a0b_3 a0b_4 in va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 262 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (8 + offset `op_Multiply` 8) Secret inA_b (1 + offset)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 264 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 265 column 26 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (0 + offset
    `op_Multiply` 8) inB_b (0 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 265 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rR9) (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (0 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg121:Vale.Def.Types_s.nat64) = va_get_reg64 rR8 va_s in let
    (va_arg120:Vale.Def.Types_s.nat64) = va_get_reg64 rR9 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 265 column 121 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg120 va_arg121 a1
    b0) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 266 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Space 3) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 267 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Xor64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR10)) (fun (va_s:va_state) _
    -> let (a1b_0:nat64) = va_get_reg64 rR8 va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 268 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 269 column 26 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRdi) (8 + offset
    `op_Multiply` 16) dst_b (1 + offset `op_Multiply` 2) Secret) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 269 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet
    0) (va_op_reg64_reg64 rRdi) (8 + offset `op_Multiply` 16) Secret)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 270 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR8) (8 + offset `op_Multiply` 16) Secret dst_b (1 + offset
    `op_Multiply` 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 272 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 273 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (8 + offset
    `op_Multiply` 8) inB_b (1 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 273 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rR11) (va_op_dst_opr64_reg64 rR10) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (8 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg119:Vale.Def.Types_s.nat64) = va_get_reg64 rR10 va_s in
    let (va_arg118:Vale.Def.Types_s.nat64) = va_get_reg64 rR11 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 273 column 123 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg118 va_arg119 a1
    b1) (let (va_arg117:Vale.Curve25519.Fast_defs.bit) = Vale.Curve25519.Fast_defs.bool_bit
    (Vale.X64.Decls.overflow (va_get_flags va_s)) in let (va_arg116:Vale.Def.Types_s.nat64) =
    va_get_reg64 rR9 va_s in let (va_arg115:Vale.Def.Types_s.nat64) = va_get_reg64 rR10 va_s in let
    (va_arg114:Vale.Def.Types_s.nat64) = va_get_reg64 rR11 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 273 column 158 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_overflow va_arg114 va_arg115
    va_arg116 va_arg117) (va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 274 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (Vale.X64.Decls.valid_of (va_get_flags va_s)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 275 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Space 1) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 276 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adox64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR9)) (fun (va_s:va_state)
    _ -> let (a1b_1:nat64) = va_get_reg64 rR10 va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 277 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 278 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rRbx)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 279 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR10) (16 + offset `op_Multiply` 16) Secret dst_b (2 + offset
    `op_Multiply` 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 281 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 282 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (16 + offset
    `op_Multiply` 8) inB_b (2 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 282 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rR13) (va_op_dst_opr64_reg64 rRbx) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (16 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg113:Vale.Def.Types_s.nat64) = va_get_reg64 rRbx va_s in
    let (va_arg112:Vale.Def.Types_s.nat64) = va_get_reg64 rR13 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 282 column 124 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg112 va_arg113 a1
    b2) (let (va_arg111:Vale.Curve25519.Fast_defs.bit) = Vale.Curve25519.Fast_defs.bool_bit
    (Vale.X64.Decls.overflow (va_get_flags va_s)) in let (va_arg110:Vale.Def.Types_s.nat64) =
    va_get_reg64 rR11 va_s in let (va_arg109:Vale.Def.Types_s.nat64) = va_get_reg64 rRbx va_s in
    let (va_arg108:Vale.Def.Types_s.nat64) = va_get_reg64 rR13 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 282 column 159 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_overflow va_arg108 va_arg109
    va_arg110 va_arg111) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 283 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 284 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adox64Wrap (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR11)) (fun
    (va_s:va_state) _ -> let (a1b_2:nat64) = va_get_reg64 rRbx va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 285 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 286 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR14)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 287 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mov64 (va_op_dst_opr64_reg64 rR8) (va_const_opr64 0)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 289 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 290 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (24 + offset
    `op_Multiply` 8) inB_b (3 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 290 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rRdx) (va_op_dst_opr64_reg64 rR14) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (24 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg107:Vale.Def.Types_s.nat64) = va_get_reg64 rR14 va_s in
    let (va_arg106:Vale.Def.Types_s.nat64) = va_get_reg64 rRdx va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 290 column 124 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg106 va_arg107 a1
    b3) (let (va_arg105:Vale.Curve25519.Fast_defs.bit) = Vale.Curve25519.Fast_defs.bool_bit
    (Vale.X64.Decls.overflow (va_get_flags va_s)) in let (va_arg104:Vale.Def.Types_s.nat64) =
    va_get_reg64 rR13 va_s in let (va_arg103:Vale.Def.Types_s.nat64) = va_get_reg64 rR14 va_s in
    let (va_arg102:Vale.Def.Types_s.nat64) = va_get_reg64 rRdx va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 290 column 159 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_overflow va_arg102 va_arg103
    va_arg104 va_arg105) (let (old_carry:Vale.Curve25519.Fast_defs.bit) =
    Vale.Curve25519.Fast_defs.bool_bit (Vale.X64.Decls.cf (va_get_flags va_s)) in let
    (old_overflow:Vale.Curve25519.Fast_defs.bit) = Vale.Curve25519.Fast_defs.bool_bit
    (Vale.X64.Decls.overflow (va_get_flags va_s)) in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 293 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 294 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adox64Wrap (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rR13)) (fun
    (va_s:va_state) _ -> let (a1b_3:nat64) = va_get_reg64 rR14 va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 295 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 296 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 297 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mov64 (va_op_dst_opr64_reg64 rRax) (va_const_opr64 0)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 299 column 57 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Space 35) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 299 column 73 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adox64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRdx)) (fun
    (va_s:va_state) _ -> let (a1b_4:nat64) = va_get_reg64 rRax va_s in let
    (overflow_bit:Vale.Curve25519.Fast_defs.bit) = Vale.Curve25519.Fast_defs.bool_bit
    (Vale.X64.Decls.overflow (va_get_flags va_s)) in va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 299 column 161 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rR8)) (fun (va_s:va_state)
    _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 301 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (overflow_bit == 0) (let (carry_bit:Vale.Curve25519.Fast_defs.bit) =
    Vale.Curve25519.Fast_defs.bool_bit (Vale.X64.Decls.cf (va_get_flags va_s)) in va_qAssert
    va_range1
    "***** PRECONDITION NOT MET AT line 304 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (carry_bit == 0) (let (d0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read dst_b (0 +
    offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in let (d1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read dst_b (1 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in
    let (d2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read dst_b (2 + offset `op_Multiply`
    2) (va_get_mem_heaplet 0 va_s) in let (a1b:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_five
    a1b_0 a1b_1 a1b_2 a1b_3 a1b_4 in let (a0a1b:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_seven
    d0 d1 d2 (va_get_reg64 rRbx va_s) (va_get_reg64 rR14 va_s) (va_get_reg64 rRax va_s) carry_bit
    in let (va_arg101:prop) = va_mul_nat a1 b == 0 + Vale.Curve25519.Fast_defs.pow2_four
    (va_mul_nat a1 b0) (va_mul_nat a1 b1) (va_mul_nat a1 b2) (va_mul_nat a1 b3) in va_qPURE
    va_range1
    "***** PRECONDITION NOT MET AT line 313 column 21 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> assert_by_tactic va_arg101 int_canon) (va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 314 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (a1b == va_mul_nat a1 b) (let (va_arg100:Vale.Def.Types_s.nat64) = carry_bit in let
    (va_arg99:Vale.Def.Types_s.nat64) = va_get_reg64 rRax va_s in let
    (va_arg98:Vale.Def.Types_s.nat64) = va_get_reg64 rR14 va_s in let
    (va_arg97:Vale.Def.Types_s.nat64) = va_get_reg64 rRbx va_s in let (va_arg96:Prims.nat) = b in
    let (va_arg95:Vale.Def.Types_s.nat64) = a1b_4 in let (va_arg94:Vale.Def.Types_s.nat64) = a1b_3
    in let (va_arg93:Vale.Def.Types_s.nat64) = a1b_2 in let (va_arg92:Vale.Def.Types_s.nat64) =
    a1b_1 in let (va_arg91:Vale.Def.Types_s.nat64) = a1b_0 in let (va_arg90:Vale.Def.Types_s.nat64)
    = a0b_4 in let (va_arg89:Vale.Def.Types_s.nat64) = a0b_3 in let
    (va_arg88:Vale.Def.Types_s.nat64) = a0b_2 in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 316 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.FastMul_helpers.lemma_sum_a1b a0 a1 a0b a0b_0 a0b_1 va_arg88
    va_arg89 va_arg90 a1b va_arg91 va_arg92 va_arg93 va_arg94 va_arg95 va_arg96 b0 b1 b2 b3 d1 d2
    va_arg97 va_arg98 va_arg99 va_arg100) (va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 323 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_mul_nat (Vale.Curve25519.Fast_defs.pow2_two a0 a1) b == a0a1b) (va_QEmpty
    (()))))))))))))))))))))))))))))))))))))))))))))))))))))))))


val va_lemma_Fast_multiply_a1b : va_b0:va_code -> va_s0:va_state -> offset:nat -> dst_b:buffer64 ->
  inA_b:buffer64 -> inB_b:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Fast_multiply_a1b offset) va_s0 /\ va_get_ok va_s0 /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let (b1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in adx_enabled /\
    bmi2_enabled /\ (offset == 0 \/ offset == 4) /\ Vale.X64.Decls.buffers_disjoint dst_b inA_b /\
    Vale.X64.Decls.buffers_disjoint dst_b inB_b /\ Vale.X64.Decls.validDstAddrs64
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) dst_b (8 + offset `op_Multiply` 2)
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) inA_b (4 + offset) (va_get_mem_layout va_s0) Secret /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRcx va_s0) inB_b (4
    + offset) (va_get_mem_layout va_s0) Secret /\ va_get_reg64 rRax va_s0 < pow2_64 - 1 /\ (let d0
    = Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s0)
    in let d1 = Vale.X64.Decls.buffer64_read dst_b (1 + offset `op_Multiply` 2) (va_get_mem_heaplet
    0 va_s0) in let a0b = d0 + va_mul_nat pow2_64 d1 + va_mul_nat pow2_128 (va_get_reg64 rRbx
    va_s0) + va_mul_nat pow2_192 (va_get_reg64 rR14 va_s0) + va_mul_nat pow2_256 (va_get_reg64 rRax
    va_s0) in a0b == va_mul_nat a0 b))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let (b1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in let d0 =
    Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in
    let d1 = Vale.X64.Decls.buffer64_read dst_b (1 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in let d2 = Vale.X64.Decls.buffer64_read dst_b (2 + offset `op_Multiply` 2)
    (va_get_mem_heaplet 0 va_sM) in va_mul_nat (Vale.Curve25519.Fast_defs.pow2_two a0 a1) b ==
    Vale.Curve25519.Fast_defs.pow2_six d0 d1 d2 (va_get_reg64 rRbx va_sM) (va_get_reg64 rR14 va_sM)
    (va_get_reg64 rRax va_sM) /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM)
    (va_get_reg64 rRdi va_sM) dst_b (8 + offset `op_Multiply` 2) (va_get_mem_layout va_sM) Secret
    /\ Vale.X64.Decls.modifies_buffer_specific dst_b (va_get_mem_heaplet 0 va_s0)
    (va_get_mem_heaplet 0 va_sM) (0 + offset `op_Multiply` 2) (8 + offset `op_Multiply` 2 - 1)) /\
    va_state_eq va_sM (va_update_flags va_sM (va_update_mem_heaplet 0 va_sM (va_update_reg64 rR14
    va_sM (va_update_reg64 rR13 va_sM (va_update_reg64 rRbx va_sM (va_update_reg64 rR11 va_sM
    (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM (va_update_reg64 rR8 va_sM
    (va_update_reg64 rRdx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem
    va_sM va_s0)))))))))))))))
[@"opaque_to_smt"]
let va_lemma_Fast_multiply_a1b va_b0 va_s0 offset dst_b inA_b inB_b =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64
    rR13; va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64
    rR8; va_Mod_reg64 rRdx; va_Mod_reg64 rRax; va_Mod_ok; va_Mod_mem] in
  let va_qc = va_qcode_Fast_multiply_a1b va_mods offset dst_b inA_b inB_b in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Fast_multiply_a1b offset) va_qc va_s0
    (fun va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 188 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_get_ok va_sM) /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 +
    offset) (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (b0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (1 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in label va_range1
    "***** POSTCONDITION NOT MET AT line 237 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (let d0 = Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 238 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (let d1 = Vale.X64.Decls.buffer64_read dst_b (1 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 239 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (let d2 = Vale.X64.Decls.buffer64_read dst_b (2 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 240 column 68 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_mul_nat (Vale.Curve25519.Fast_defs.pow2_two a0 a1) b == Vale.Curve25519.Fast_defs.pow2_six
    d0 d1 d2 (va_get_reg64 rRbx va_sM) (va_get_reg64 rR14 va_sM) (va_get_reg64 rRax va_sM)) /\
    label va_range1
    "***** POSTCONDITION NOT MET AT line 242 column 80 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b (8
    + offset `op_Multiply` 2) (va_get_mem_layout va_sM) Secret) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 243 column 91 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (Vale.X64.Decls.modifies_buffer_specific dst_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet
    0 va_sM) (0 + offset `op_Multiply` 2) (8 + offset `op_Multiply` 2 - 1))))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64 rR13;
    va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8;
    va_Mod_reg64 rRdx; va_Mod_reg64 rRax; va_Mod_ok; va_Mod_mem]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Fast_multiply_a1b (offset:nat) (dst_b:buffer64) (inA_b:buffer64) (inB_b:buffer64)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 +
    offset) (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (b0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (1 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in adx_enabled /\
    bmi2_enabled /\ (offset == 0 \/ offset == 4) /\ Vale.X64.Decls.buffers_disjoint dst_b inA_b /\
    Vale.X64.Decls.buffers_disjoint dst_b inB_b /\ Vale.X64.Decls.validDstAddrs64
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) dst_b (8 + offset `op_Multiply` 2)
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) inA_b (4 + offset) (va_get_mem_layout va_s0) Secret /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRcx va_s0) inB_b (4
    + offset) (va_get_mem_layout va_s0) Secret /\ va_get_reg64 rRax va_s0 < pow2_64 - 1 /\ (let d0
    = Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s0)
    in let d1 = Vale.X64.Decls.buffer64_read dst_b (1 + offset `op_Multiply` 2) (va_get_mem_heaplet
    0 va_s0) in let a0b = d0 + va_mul_nat pow2_64 d1 + va_mul_nat pow2_128 (va_get_reg64 rRbx
    va_s0) + va_mul_nat pow2_192 (va_get_reg64 rR14 va_s0) + va_mul_nat pow2_256 (va_get_reg64 rRax
    va_s0) in a0b == va_mul_nat a0 b)) /\ (forall (va_x_mem:vale_heap) (va_x_rax:nat64)
    (va_x_rdx:nat64) (va_x_r8:nat64) (va_x_r9:nat64) (va_x_r10:nat64) (va_x_r11:nat64)
    (va_x_rbx:nat64) (va_x_r13:nat64) (va_x_r14:nat64) (va_x_heap0:vale_heap)
    (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_mem_heaplet 0
    va_x_heap0 (va_upd_reg64 rR14 va_x_r14 (va_upd_reg64 rR13 va_x_r13 (va_upd_reg64 rRbx va_x_rbx
    (va_upd_reg64 rR11 va_x_r11 (va_upd_reg64 rR10 va_x_r10 (va_upd_reg64 rR9 va_x_r9 (va_upd_reg64
    rR8 va_x_r8 (va_upd_reg64 rRdx va_x_rdx (va_upd_reg64 rRax va_x_rax (va_upd_mem va_x_mem
    va_s0))))))))))) in va_get_ok va_sM /\ (let (a0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (1 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (b2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in let d0 =
    Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in
    let d1 = Vale.X64.Decls.buffer64_read dst_b (1 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in let d2 = Vale.X64.Decls.buffer64_read dst_b (2 + offset `op_Multiply` 2)
    (va_get_mem_heaplet 0 va_sM) in va_mul_nat (Vale.Curve25519.Fast_defs.pow2_two a0 a1) b ==
    Vale.Curve25519.Fast_defs.pow2_six d0 d1 d2 (va_get_reg64 rRbx va_sM) (va_get_reg64 rR14 va_sM)
    (va_get_reg64 rRax va_sM) /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM)
    (va_get_reg64 rRdi va_sM) dst_b (8 + offset `op_Multiply` 2) (va_get_mem_layout va_sM) Secret
    /\ Vale.X64.Decls.modifies_buffer_specific dst_b (va_get_mem_heaplet 0 va_s0)
    (va_get_mem_heaplet 0 va_sM) (0 + offset `op_Multiply` 2) (8 + offset `op_Multiply` 2 - 1)) ==>
    va_k va_sM (())))


val va_wpProof_Fast_multiply_a1b : offset:nat -> dst_b:buffer64 -> inA_b:buffer64 -> inB_b:buffer64
  -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Fast_multiply_a1b offset dst_b inA_b inB_b va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Fast_multiply_a1b offset)
    ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64 rR13; va_Mod_reg64 rRbx;
    va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx;
    va_Mod_reg64 rRax; va_Mod_mem]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Fast_multiply_a1b offset dst_b inA_b inB_b va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Fast_multiply_a1b (va_code_Fast_multiply_a1b offset) va_s0 offset
    dst_b inA_b inB_b in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_mem_heaplet 0 va_sM (va_update_reg64
    rR14 va_sM (va_update_reg64 rR13 va_sM (va_update_reg64 rRbx va_sM (va_update_reg64 rR11 va_sM
    (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM (va_update_reg64 rR8 va_sM
    (va_update_reg64 rRdx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem
    va_sM va_s0))))))))))))));
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64 rR13;
    va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8;
    va_Mod_reg64 rRdx; va_Mod_reg64 rRax; va_Mod_mem]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Fast_multiply_a1b (offset:nat) (dst_b:buffer64) (inA_b:buffer64) (inB_b:buffer64) :
  (va_quickCode unit (va_code_Fast_multiply_a1b offset)) =
  (va_QProc (va_code_Fast_multiply_a1b offset) ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64
    rR14; va_Mod_reg64 rR13; va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64
    rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx; va_Mod_reg64 rRax; va_Mod_mem])
    (va_wp_Fast_multiply_a1b offset dst_b inA_b inB_b) (va_wpProof_Fast_multiply_a1b offset dst_b
    inA_b inB_b))
#pop-options
//--
//-- Fast_multiply_a2b
#push-options "--z3rlimit 800"

val va_code_Fast_multiply_a2b : offset:nat -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Fast_multiply_a2b offset =
  (va_Block (va_CCons (va_code_Comment
    "Compute src1[2] * src2"
    ) (va_CCons (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (16 + offset `op_Multiply` 8) Secret) (va_CCons (va_code_NoNewline
    ()) (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx64 (va_op_dst_opr64_reg64 rR9)
    (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64
    rRcx) (0 + offset `op_Multiply` 8) Secret)) (va_CCons (va_code_Space 3) (va_CCons
    (va_code_Xor64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR10)) (va_CCons
    (va_code_NoNewline ()) (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Adcx64Wrap
    (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64
    rRdi) (16 + offset `op_Multiply` 16) Secret)) (va_CCons (va_code_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR8) (16 +
    offset `op_Multiply` 16) Secret) (va_CCons (va_code_NoNewline ()) (va_CCons
    (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx64 (va_op_dst_opr64_reg64 rR11)
    (va_op_dst_opr64_reg64 rR10) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (8 + offset `op_Multiply` 8) Secret)) (va_CCons (va_code_Space 1)
    (va_CCons (va_code_Adox64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR9)) (va_CCons
    (va_code_Space 1) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64
    rRbx)) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64
    rRdi) (va_op_reg_opr64_reg64 rR10) (24 + offset `op_Multiply` 16) Secret) (va_CCons
    (va_code_NoNewline ()) (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx64
    (va_op_dst_opr64_reg64 rR13) (va_op_dst_opr64_reg64 rRbx) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (16 + offset `op_Multiply` 8) Secret))
    (va_CCons (va_code_NoNewline ()) (va_CCons (va_code_Adox64Wrap (va_op_dst_opr64_reg64 rRbx)
    (va_op_opr64_reg64 rR11)) (va_CCons (va_code_NoNewline ()) (va_CCons (va_code_Adcx64Wrap
    (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR14)) (va_CCons (va_code_Mov64
    (va_op_dst_opr64_reg64 rR8) (va_const_opr64 0)) (va_CCons (va_code_NoNewline ()) (va_CCons
    (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx64 (va_op_dst_opr64_reg64 rRdx)
    (va_op_dst_opr64_reg64 rR14) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (24 + offset `op_Multiply` 8) Secret)) (va_CCons (va_code_NoNewline
    ()) (va_CCons (va_code_Adox64Wrap (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rR13))
    (va_CCons (va_code_NoNewline ()) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rR14)
    (va_op_opr64_reg64 rRax)) (va_CCons (va_code_Mov64 (va_op_dst_opr64_reg64 rRax) (va_const_opr64
    0)) (va_CCons (va_code_Space 35) (va_CCons (va_code_Adox64Wrap (va_op_dst_opr64_reg64 rRax)
    (va_op_opr64_reg64 rRdx)) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rRax)
    (va_op_opr64_reg64 rR8)) (va_CNil ()))))))))))))))))))))))))))))))))))))))))

val va_codegen_success_Fast_multiply_a2b : offset:nat -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Fast_multiply_a2b offset =
  (va_pbool_and (va_codegen_success_Comment
    "Compute src1[2] * src2"
    ) (va_pbool_and (va_codegen_success_Load64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_dst_opr64_reg64 rRdx) (va_op_reg_opr64_reg64 rRsi) (16 + offset `op_Multiply` 8) Secret)
    (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Mem64_lemma
    ()) (va_pbool_and (va_codegen_success_Mulx64 (va_op_dst_opr64_reg64 rR9) (va_op_dst_opr64_reg64
    rR8) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (0 + offset
    `op_Multiply` 8) Secret)) (va_pbool_and (va_codegen_success_Space 3) (va_pbool_and
    (va_codegen_success_Xor64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR10)) (va_pbool_and
    (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Mem64_lemma ())
    (va_pbool_and (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRdi) (16 + offset `op_Multiply` 16) Secret))
    (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR8) (16 + offset `op_Multiply` 16) Secret)
    (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Mem64_lemma
    ()) (va_pbool_and (va_codegen_success_Mulx64 (va_op_dst_opr64_reg64 rR11)
    (va_op_dst_opr64_reg64 rR10) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (8 + offset `op_Multiply` 8) Secret)) (va_pbool_and
    (va_codegen_success_Space 1) (va_pbool_and (va_codegen_success_Adox64Wrap
    (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR9)) (va_pbool_and (va_codegen_success_Space
    1) (va_pbool_and (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64
    rRbx)) (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR10) (24 + offset `op_Multiply` 16)
    Secret) (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and
    (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx64
    (va_op_dst_opr64_reg64 rR13) (va_op_dst_opr64_reg64 rRbx) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (16 + offset `op_Multiply` 8) Secret))
    (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Adox64Wrap
    (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR11)) (va_pbool_and
    (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Adcx64Wrap
    (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR14)) (va_pbool_and (va_codegen_success_Mov64
    (va_op_dst_opr64_reg64 rR8) (va_const_opr64 0)) (va_pbool_and (va_codegen_success_NoNewline ())
    (va_pbool_and (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx64
    (va_op_dst_opr64_reg64 rRdx) (va_op_dst_opr64_reg64 rR14) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (24 + offset `op_Multiply` 8) Secret))
    (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Adox64Wrap
    (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rR13)) (va_pbool_and
    (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Adcx64Wrap
    (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_Mov64
    (va_op_dst_opr64_reg64 rRax) (va_const_opr64 0)) (va_pbool_and (va_codegen_success_Space 35)
    (va_pbool_and (va_codegen_success_Adox64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64
    rRdx)) (va_pbool_and (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rRax)
    (va_op_opr64_reg64 rR8)) (va_ttrue ())))))))))))))))))))))))))))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Fast_multiply_a2b (va_mods:va_mods_t) (offset:nat) (dst_b:buffer64) (inA_b:buffer64)
  (inB_b:buffer64) : (va_quickCode unit (va_code_Fast_multiply_a2b offset)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s) in let (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (0 + offset) (va_get_mem_heaplet 0 va_s) in let (b1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (1 + offset) (va_get_mem_heaplet 0 va_s) in let
    (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (2 + offset)
    (va_get_mem_heaplet 0 va_s) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (3 + offset) (va_get_mem_heaplet 0 va_s) in let (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 381 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Comment
    "Compute src1[2] * src2"
    ) (fun (va_s:va_state) _ -> va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 382 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Arch.Types.xor_lemmas ()) (let (a0a1b_0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in
    let (a0a1b_1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read dst_b (1 + offset
    `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in let (a0a1b_2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read dst_b (2 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in
    let (a0a1b_3:nat64) = va_get_reg64 rRbx va_s in let (a0a1b_4:nat64) = va_get_reg64 rR14 va_s in
    let (a0a1b_5:nat64) = va_get_reg64 rRax va_s in let (a0a1b:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_six a0a1b_0 a0a1b_1 a0a1b_2 a0a1b_3 a0a1b_4 a0a1b_5 in va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 400 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (16 + offset `op_Multiply` 8) Secret inA_b (2 + offset)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 402 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 403 column 26 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (0 + offset
    `op_Multiply` 8) inB_b (0 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 403 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rR9) (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (0 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg119:Vale.Def.Types_s.nat64) = va_get_reg64 rR8 va_s in let
    (va_arg118:Vale.Def.Types_s.nat64) = va_get_reg64 rR9 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 403 column 121 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg118 va_arg119 a2
    b0) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 404 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Space 3) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 405 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Xor64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR10)) (fun (va_s:va_state) _
    -> let (a2b_0:nat64) = va_get_reg64 rR8 va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 406 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 407 column 26 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRdi) (16 + offset
    `op_Multiply` 16) dst_b (2 + offset `op_Multiply` 2) Secret) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 407 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet
    0) (va_op_reg64_reg64 rRdi) (16 + offset `op_Multiply` 16) Secret)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 408 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR8) (16 + offset `op_Multiply` 16) Secret dst_b (2 + offset
    `op_Multiply` 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 410 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 411 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (8 + offset
    `op_Multiply` 8) inB_b (1 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 411 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rR11) (va_op_dst_opr64_reg64 rR10) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (8 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg117:Vale.Def.Types_s.nat64) = va_get_reg64 rR10 va_s in
    let (va_arg116:Vale.Def.Types_s.nat64) = va_get_reg64 rR11 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 411 column 123 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg116 va_arg117 a2
    b1) (let (va_arg115:Vale.Curve25519.Fast_defs.bit) = Vale.Curve25519.Fast_defs.bool_bit
    (Vale.X64.Decls.overflow (va_get_flags va_s)) in let (va_arg114:Vale.Def.Types_s.nat64) =
    va_get_reg64 rR9 va_s in let (va_arg113:Vale.Def.Types_s.nat64) = va_get_reg64 rR10 va_s in let
    (va_arg112:Vale.Def.Types_s.nat64) = va_get_reg64 rR11 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 411 column 158 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_overflow va_arg112 va_arg113
    va_arg114 va_arg115) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 412 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Space 1) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 413 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adox64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR9)) (fun (va_s:va_state)
    _ -> let (a2b_1:nat64) = va_get_reg64 rR10 va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 414 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 415 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rRbx)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 416 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR10) (24 + offset `op_Multiply` 16) Secret dst_b (3 + offset
    `op_Multiply` 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 418 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 419 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (16 + offset
    `op_Multiply` 8) inB_b (2 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 419 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rR13) (va_op_dst_opr64_reg64 rRbx) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (16 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg111:Vale.Def.Types_s.nat64) = va_get_reg64 rRbx va_s in
    let (va_arg110:Vale.Def.Types_s.nat64) = va_get_reg64 rR13 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 419 column 124 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg110 va_arg111 a2
    b2) (let (va_arg109:Vale.Curve25519.Fast_defs.bit) = Vale.Curve25519.Fast_defs.bool_bit
    (Vale.X64.Decls.overflow (va_get_flags va_s)) in let (va_arg108:Vale.Def.Types_s.nat64) =
    va_get_reg64 rR11 va_s in let (va_arg107:Vale.Def.Types_s.nat64) = va_get_reg64 rRbx va_s in
    let (va_arg106:Vale.Def.Types_s.nat64) = va_get_reg64 rR13 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 419 column 159 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_overflow va_arg106 va_arg107
    va_arg108 va_arg109) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 420 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 421 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adox64Wrap (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR11)) (fun
    (va_s:va_state) _ -> let (a2b_2:nat64) = va_get_reg64 rRbx va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 422 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 423 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR14)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 424 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mov64 (va_op_dst_opr64_reg64 rR8) (va_const_opr64 0)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 426 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 427 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (24 + offset
    `op_Multiply` 8) inB_b (3 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 427 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rRdx) (va_op_dst_opr64_reg64 rR14) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (24 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg105:Vale.Def.Types_s.nat64) = va_get_reg64 rR14 va_s in
    let (va_arg104:Vale.Def.Types_s.nat64) = va_get_reg64 rRdx va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 427 column 124 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg104 va_arg105 a2
    b3) (let (va_arg103:Vale.Curve25519.Fast_defs.bit) = Vale.Curve25519.Fast_defs.bool_bit
    (Vale.X64.Decls.overflow (va_get_flags va_s)) in let (va_arg102:Vale.Def.Types_s.nat64) =
    va_get_reg64 rR13 va_s in let (va_arg101:Vale.Def.Types_s.nat64) = va_get_reg64 rR14 va_s in
    let (va_arg100:Vale.Def.Types_s.nat64) = va_get_reg64 rRdx va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 427 column 159 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_overflow va_arg100 va_arg101
    va_arg102 va_arg103) (let (old_carry:Vale.Curve25519.Fast_defs.bit) =
    Vale.Curve25519.Fast_defs.bool_bit (Vale.X64.Decls.cf (va_get_flags va_s)) in let
    (old_overflow:Vale.Curve25519.Fast_defs.bit) = Vale.Curve25519.Fast_defs.bool_bit
    (Vale.X64.Decls.overflow (va_get_flags va_s)) in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 430 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 431 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adox64Wrap (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rR13)) (fun
    (va_s:va_state) _ -> let (a2b_3:nat64) = va_get_reg64 rR14 va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 432 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 433 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 434 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Mov64 (va_op_dst_opr64_reg64 rRax) (va_const_opr64 0)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 436 column 56 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Space 35) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 436 column 73 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adox64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRdx)) (fun
    (va_s:va_state) _ -> let (a2b_4:nat64) = va_get_reg64 rRax va_s in va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 437 column 36 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rR8)) (fun (va_s:va_state)
    _ -> let (carry_bit:Vale.Curve25519.Fast_defs.bit) = Vale.Curve25519.Fast_defs.bool_bit
    (Vale.X64.Decls.cf (va_get_flags va_s)) in let (overflow_bit:Vale.Curve25519.Fast_defs.bit) =
    Vale.Curve25519.Fast_defs.bool_bit (Vale.X64.Decls.overflow (va_get_flags va_s)) in va_qAssert
    va_range1
    "***** PRECONDITION NOT MET AT line 442 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (overflow_bit == 0) (va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 443 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (carry_bit == 0) (let (d0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read dst_b (0 +
    offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in let (d1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read dst_b (1 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in
    let (d2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read dst_b (2 + offset `op_Multiply`
    2) (va_get_mem_heaplet 0 va_s) in let (d3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read dst_b (3 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in
    let (a2b:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_five a2b_0 a2b_1 a2b_2 a2b_3 a2b_4 in let
    (a0a1a2b:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_seven d0 d1 d2 d3 (va_get_reg64 rRbx va_s)
    (va_get_reg64 rR14 va_s) (va_get_reg64 rRax va_s) in let (va_arg99:prop) = va_mul_nat a2 b == 0
    + Vale.Curve25519.Fast_defs.pow2_four (va_mul_nat a2 b0) (va_mul_nat a2 b1) (va_mul_nat a2 b2)
    (va_mul_nat a2 b3) in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 453 column 21 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> assert_by_tactic va_arg99 int_canon) (let (va_arg98:Vale.Def.Types_s.nat64) =
    va_get_reg64 rRax va_s in let (va_arg97:Vale.Def.Types_s.nat64) = va_get_reg64 rR14 va_s in let
    (va_arg96:Vale.Def.Types_s.nat64) = va_get_reg64 rRbx va_s in let (va_arg95:Prims.nat) = b in
    let (va_arg94:Vale.Def.Types_s.nat64) = a2b_4 in let (va_arg93:Vale.Def.Types_s.nat64) = a2b_3
    in let (va_arg92:Vale.Def.Types_s.nat64) = a2b_2 in let (va_arg91:Vale.Def.Types_s.nat64) =
    a2b_1 in let (va_arg90:Vale.Def.Types_s.nat64) = a2b_0 in let (va_arg89:Vale.Def.Types_s.nat64)
    = a0a1b_5 in let (va_arg88:Vale.Def.Types_s.nat64) = a0a1b_4 in let
    (va_arg87:Vale.Def.Types_s.nat64) = a0a1b_3 in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 456 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.FastMul_helpers.lemma_sum_a2b a0 a1 a2 a0a1b a0a1b_0 a0a1b_1
    a0a1b_2 va_arg87 va_arg88 va_arg89 a2b va_arg90 va_arg91 va_arg92 va_arg93 va_arg94 va_arg95 b0
    b1 b2 b3 d2 d3 va_arg96 va_arg97 va_arg98) (va_QEmpty
    (())))))))))))))))))))))))))))))))))))))))))))))))))))))


val va_lemma_Fast_multiply_a2b : va_b0:va_code -> va_s0:va_state -> offset:nat -> dst_b:buffer64 ->
  inA_b:buffer64 -> inB_b:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Fast_multiply_a2b offset) va_s0 /\ va_get_ok va_s0 /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let (b1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in adx_enabled /\
    bmi2_enabled /\ (offset == 0 \/ offset == 4) /\ Vale.X64.Decls.buffers_disjoint dst_b inA_b /\
    Vale.X64.Decls.buffers_disjoint dst_b inB_b /\ Vale.X64.Decls.validDstAddrs64
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) dst_b (8 + offset `op_Multiply` 2)
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) inA_b (4 + offset) (va_get_mem_layout va_s0) Secret /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRcx va_s0) inB_b (4
    + offset) (va_get_mem_layout va_s0) Secret /\ (let d0 = Vale.X64.Decls.buffer64_read dst_b (0 +
    offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s0) in let d1 = Vale.X64.Decls.buffer64_read
    dst_b (1 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s0) in let d2 =
    Vale.X64.Decls.buffer64_read dst_b (2 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s0) in
    Vale.Curve25519.Fast_defs.mul_nats (Vale.Curve25519.Fast_defs.pow2_two a0 a1) b ==
    Vale.Curve25519.Fast_defs.pow2_six d0 d1 d2 (va_get_reg64 rRbx va_s0) (va_get_reg64 rR14 va_s0)
    (va_get_reg64 rRax va_s0)))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let (b1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in let d0 =
    Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in
    let d1 = Vale.X64.Decls.buffer64_read dst_b (1 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in let d2 = Vale.X64.Decls.buffer64_read dst_b (2 + offset `op_Multiply` 2)
    (va_get_mem_heaplet 0 va_sM) in let d3 = Vale.X64.Decls.buffer64_read dst_b (3 + offset
    `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in va_mul_nat
    (Vale.Curve25519.Fast_defs.pow2_three a0 a1 a2) b == Vale.Curve25519.Fast_defs.pow2_seven d0 d1
    d2 d3 (va_get_reg64 rRbx va_sM) (va_get_reg64 rR14 va_sM) (va_get_reg64 rRax va_sM) /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b (8
    + offset `op_Multiply` 2) (va_get_mem_layout va_sM) Secret /\
    Vale.X64.Decls.modifies_buffer_specific dst_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet
    0 va_sM) (0 + offset `op_Multiply` 2) (8 + offset `op_Multiply` 2 - 1)) /\ va_state_eq va_sM
    (va_update_flags va_sM (va_update_mem_heaplet 0 va_sM (va_update_reg64 rR14 va_sM
    (va_update_reg64 rR13 va_sM (va_update_reg64 rRbx va_sM (va_update_reg64 rR11 va_sM
    (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM (va_update_reg64 rR8 va_sM
    (va_update_reg64 rRdx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem
    va_sM va_s0)))))))))))))))
[@"opaque_to_smt"]
let va_lemma_Fast_multiply_a2b va_b0 va_s0 offset dst_b inA_b inB_b =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64
    rR13; va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64
    rR8; va_Mod_reg64 rRdx; va_Mod_reg64 rRax; va_Mod_ok; va_Mod_mem] in
  let va_qc = va_qcode_Fast_multiply_a2b va_mods offset dst_b inA_b inB_b in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Fast_multiply_a2b offset) va_qc va_s0
    (fun va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 326 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_get_ok va_sM) /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 +
    offset) (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (b0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (1 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in label va_range1
    "***** POSTCONDITION NOT MET AT line 372 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (let d0 = Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 373 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (let d1 = Vale.X64.Decls.buffer64_read dst_b (1 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 374 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (let d2 = Vale.X64.Decls.buffer64_read dst_b (2 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 375 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (let d3 = Vale.X64.Decls.buffer64_read dst_b (3 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 376 column 80 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (va_mul_nat (Vale.Curve25519.Fast_defs.pow2_three a0 a1 a2) b ==
    Vale.Curve25519.Fast_defs.pow2_seven d0 d1 d2 d3 (va_get_reg64 rRbx va_sM) (va_get_reg64 rR14
    va_sM) (va_get_reg64 rRax va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 378 column 80 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b (8
    + offset `op_Multiply` 2) (va_get_mem_layout va_sM) Secret) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 379 column 91 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastMul.vaf *****"
    (Vale.X64.Decls.modifies_buffer_specific dst_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet
    0 va_sM) (0 + offset `op_Multiply` 2) (8 + offset `op_Multiply` 2 - 1)))))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64 rR13;
    va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8;
    va_Mod_reg64 rRdx; va_Mod_reg64 rRax; va_Mod_ok; va_Mod_mem]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Fast_multiply_a2b (offset:nat) (dst_b:buffer64) (inA_b:buffer64) (inB_b:buffer64)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 +
    offset) (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (b0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (1 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in adx_enabled /\
    bmi2_enabled /\ (offset == 0 \/ offset == 4) /\ Vale.X64.Decls.buffers_disjoint dst_b inA_b /\
    Vale.X64.Decls.buffers_disjoint dst_b inB_b /\ Vale.X64.Decls.validDstAddrs64
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) dst_b (8 + offset `op_Multiply` 2)
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) inA_b (4 + offset) (va_get_mem_layout va_s0) Secret /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRcx va_s0) inB_b (4
    + offset) (va_get_mem_layout va_s0) Secret /\ (let d0 = Vale.X64.Decls.buffer64_read dst_b (0 +
    offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s0) in let d1 = Vale.X64.Decls.buffer64_read
    dst_b (1 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s0) in let d2 =
    Vale.X64.Decls.buffer64_read dst_b (2 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s0) in
    Vale.Curve25519.Fast_defs.mul_nats (Vale.Curve25519.Fast_defs.pow2_two a0 a1) b ==
    Vale.Curve25519.Fast_defs.pow2_six d0 d1 d2 (va_get_reg64 rRbx va_s0) (va_get_reg64 rR14 va_s0)
    (va_get_reg64 rRax va_s0))) /\ (forall (va_x_mem:vale_heap) (va_x_rax:nat64) (va_x_rdx:nat64)
    (va_x_r8:nat64) (va_x_r9:nat64) (va_x_r10:nat64) (va_x_r11:nat64) (va_x_rbx:nat64)
    (va_x_r13:nat64) (va_x_r14:nat64) (va_x_heap0:vale_heap) (va_x_efl:Vale.X64.Flags.t) . let
    va_sM = va_upd_flags va_x_efl (va_upd_mem_heaplet 0 va_x_heap0 (va_upd_reg64 rR14 va_x_r14
    (va_upd_reg64 rR13 va_x_r13 (va_upd_reg64 rRbx va_x_rbx (va_upd_reg64 rR11 va_x_r11
    (va_upd_reg64 rR10 va_x_r10 (va_upd_reg64 rR9 va_x_r9 (va_upd_reg64 rR8 va_x_r8 (va_upd_reg64
    rRdx va_x_rdx (va_upd_reg64 rRax va_x_rax (va_upd_mem va_x_mem va_s0))))))))))) in va_get_ok
    va_sM /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let (b1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (a:(va_int_range 0
    115792089237316195423570985008687907853269984665640564039457584007913129639935)) = a0 +
    va_mul_nat pow2_64 a1 + va_mul_nat pow2_128 a2 + va_mul_nat pow2_192 a3 in let (b:(va_int_range
    0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) = b0 +
    va_mul_nat pow2_64 b1 + va_mul_nat pow2_128 b2 + va_mul_nat pow2_192 b3 in let d0 =
    Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in
    let d1 = Vale.X64.Decls.buffer64_read dst_b (1 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in let d2 = Vale.X64.Decls.buffer64_read dst_b (2 + offset `op_Multiply` 2)
    (va_get_mem_heaplet 0 va_sM) in let d3 = Vale.X64.Decls.buffer64_read dst_b (3 + offset
    `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in va_mul_nat
    (Vale.Curve25519.Fast_defs.pow2_three a0 a1 a2) b == Vale.Curve25519.Fast_defs.pow2_seven d0 d1
    d2 d3 (va_get_reg64 rRbx va_sM) (va_get_reg64 rR14 va_sM) (va_get_reg64 rRax va_sM) /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b (8
    + offset `op_Multiply` 2) (va_get_mem_layout va_sM) Secret /\
    Vale.X64.Decls.modifies_buffer_specific dst_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet
    0 va_sM) (0 + offset `op_Multiply` 2) (8 + offset `op_Multiply` 2 - 1)) ==> va_k va_sM (())))


val va_wpProof_Fast_multiply_a2b : offset:nat -> dst_b:buffer64 -> inA_b:buffer64 -> inB_b:buffer64
  -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Fast_multiply_a2b offset dst_b inA_b inB_b va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Fast_multiply_a2b offset)
    ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64 rR13; va_Mod_reg64 rRbx;
    va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx;
    va_Mod_reg64 rRax; va_Mod_mem]) va_s0 va_k ((va_sM, va_f0, va_g))))
val va_wpProof_Fast_multiply_a2b : offset:nat -> dst_b:buffer64 -> inA_b:buffer64 -> inB_b:buffer64
  -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Fast_multiply_a2b offset dst_b inA_b inB_b va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Fast_multiply_a2b offset)
    ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64 rR13; va_Mod_reg64 rRbx;
    va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx;
    va_Mod_reg64 rRax; va_Mod_mem]) va_s0 va_k ((va_sM, va_f0, va_g))))

    offset: Prims.nat ->
    dst_b: Vale.X64.Memory.buffer64 ->
    inA_b: Vale.X64.Memory.buffer64 ->
    inB_b: Vale.X64.Memory.buffer64 ->
    va_s0: Vale.X64.Decls.va_state ->
    va_k: (_: Vale.X64.Decls.va_state -> _: Prims.unit -> Type0)
  -> Prims.Ghost ((Vale.X64.Decls.va_state * Vale.X64.Decls.va_fuel) * Prims.unit)