val va_qcode_Fast_multiply_a0b (va_mods: va_mods_t) (offset: nat) (dst_b inA_b inB_b: buffer64)
    : (va_quickCode unit (va_code_Fast_multiply_a0b offset))
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_qcode_Fast_multiply_a0b (va_mods: va_mods_t) (offset: nat) (dst_b inA_b inB_b: buffer64)
    : (va_quickCode unit (va_code_Fast_multiply_a0b offset))
let va_qcode_Fast_multiply_a0b (va_mods: va_mods_t) (offset: nat) (dst_b inA_b 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
                                                                                                                                                                                      (
                                                                                                                                                                                        ()
                                                                                                                                                                                      )

                                                                                                                                                                                  )

                                                                                                                                                                              )

                                                                                                                                                                          )

                                                                                                                                                                      )

                                                                                                                                                                )

                                                                                                                                                            )

                                                                                                                                                      )

                                                                                                                                                  )

                                                                                                                                              )

                                                                                                                                          )

                                                                                                                                    )

                                                                                                                                )

                                                                                                                            )

                                                                                                                      )

                                                                                                                  )

                                                                                                            )

                                                                                                        )

                                                                                                    )
                                                                                                  ))
                                                                                      ))))))))))))))
                          )))))))
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
Vale.X64.QuickCode.va_mods_t Prims.nat Vale.X64.Memory.buffer64 Vale.X64.QuickCodes.qblock Prims.unit Prims.Cons Vale.X64.Decls.va_code Vale.X64.InsBasic.va_code_Comment Vale.X64.InsMem.va_code_Load64_buffer Vale.X64.Decls.va_op_heaplet_mem_heaplet Vale.X64.Decls.va_op_dst_opr64_reg64 Vale.X64.Machine_s.rRdx Vale.X64.Decls.va_op_reg_opr64_reg64 Vale.X64.Machine_s.rRsi Prims.op_Addition Prims.op_Multiply Vale.Arch.HeapTypes_s.Secret Vale.X64.InsBasic.va_code_NoNewline Vale.X64.InsMem.va_code_Mem64_lemma Vale.X64.InsBasic.va_code_Mulx64 Vale.X64.Machine_s.rR9 Vale.X64.Machine_s.rR8 Vale.X64.Decls.va_opr_code_Mem64 Vale.X64.Decls.va_op_reg64_reg64 Vale.X64.Machine_s.rRcx Vale.X64.InsBasic.va_code_Space Vale.X64.InsBasic.va_code_Xor64 Vale.X64.Machine_s.rR10 Vale.X64.Decls.va_op_opr64_reg64 Vale.X64.InsMem.va_code_Store64_buffer Vale.X64.Machine_s.rRdi Vale.X64.InsBasic.va_code_Newline Vale.X64.Machine_s.rR11 Vale.X64.InsBasic.va_code_Adox64Wrap Vale.X64.Machine_s.rR13 Vale.X64.Machine_s.rRbx Vale.X64.Machine_s.rR14 Vale.X64.InsBasic.va_code_Mov64 Vale.X64.Machine_s.rRax Vale.X64.Decls.va_const_opr64 Prims.Nil Vale.X64.Machine_s.precode Vale.X64.Decls.ins Vale.X64.Decls.ocmp Vale.X64.Decls.va_state Vale.X64.QuickCodes.va_qPURE Prims.pure_post Prims.l_and Prims.l_True Prims.l_Forall Prims.l_imp Vale.Def.Words_s.nat32 Prims.eq2 Vale.Def.Types_s.ixor Prims.int Vale.Def.Words_s.nat64 Vale.X64.QuickCodes.va_range1 Vale.Arch.Types.xor_lemmas Vale.X64.QuickCodes.va_QSeq Vale.X64.InsBasic.va_quick_Comment Vale.X64.InsMem.va_quick_Load64_buffer Vale.X64.InsBasic.va_quick_NoNewline Vale.X64.InsMem.va_quick_Mem64_lemma Vale.X64.InsBasic.va_quick_Mulx64 Vale.X64.InsBasic.va_quick_Space Vale.X64.QuickCodes.va_QBind Vale.X64.InsBasic.va_quick_Xor64 Prims.b2t Prims.op_LessThan Prims.op_Subtraction Prims.l_or Prims.op_LessThanOrEqual Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds Vale.X64.InsMem.va_quick_Store64_buffer Vale.X64.InsBasic.va_quick_Newline Vale.X64.InsBasic.va_quick_Adox64Wrap Vale.X64.InsBasic.va_quick_Mov64 FStar.Tactics.Effect.with_tactic Vale.Curve25519.FastMul_helpers.int_canon Prims.squash FStar.Tactics.Effect.assert_by_tactic Vale.X64.QuickCodes.va_qAssert Prims.op_GreaterThanOrEqual Vale.X64.Decls.va_mul_nat Vale.X64.Decls.va_get_reg64 Vale.X64.Machine_s.pow2_64 Vale.X64.QuickCodes.va_QEmpty Prims.prop Vale.X64.Machine_s.pow2_128 Vale.Curve25519.Fast_defs.pow2_192 Vale.X64.Decls.va_int_range Vale.Curve25519.Fast_defs.pow2_256 Vale.Curve25519.Fast_defs.pow2_320 Vale.X64.Decls.va_if Vale.X64.Decls.overflow Vale.X64.Decls.va_get_flags Prims.l_not Vale.X64.QuickCodes.quickCodes Prims.bool Vale.X64.Decls.buffer64_read Vale.X64.Decls.va_get_mem_heaplet Vale.X64.State.vale_state Vale.X64.QuickCode.va_quickCode Vale.Curve25519.X64.FastMul.va_code_Fast_multiply_a0b
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)
val va_qcode_Fast_multiply_a0b (va_mods: va_mods_t) (offset: nat) (dst_b inA_b inB_b: buffer64)
    : (va_quickCode unit (va_code_Fast_multiply_a0b offset))

    va_mods: Vale.X64.QuickCode.va_mods_t ->
    offset: Prims.nat ->
    dst_b: Vale.X64.Memory.buffer64 ->
    inA_b: Vale.X64.Memory.buffer64 ->
    inB_b: Vale.X64.Memory.buffer64
  -> Vale.X64.QuickCode.va_quickCode Prims.unit
      (Vale.Curve25519.X64.FastMul.va_code_Fast_multiply_a0b offset)