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))))
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))))
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)
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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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/fstar_dataset/projects/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))))
/
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

    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)
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_a0b Vale.Curve25519.X64.FastMul.va_code_Fast_multiply_a0b
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)