val va_qcode_Fast_mul1 (va_mods: va_mods_t) (dst_b inA_b: buffer64)
    : (va_quickCode unit (va_code_Fast_mul1 ()))
let va_qcode_Fast_mul1 (va_mods:va_mods_t) (dst_b:buffer64) (inA_b:buffer64) : (va_quickCode unit
  (va_code_Fast_mul1 ())) =
  (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 (va_get_mem_heaplet 0 va_s)
    in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 1 (va_get_mem_heaplet 0
    va_s) in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 2
    (va_get_mem_heaplet 0 va_s) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 3 (va_get_mem_heaplet 0 va_s) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four
    a0 a1 a2 a3 in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 91 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (fun (_:unit) -> Vale.Arch.Types.xor_lemmas ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 93 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 0 inA_b 0 Secret)
    (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 93 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.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 rRsi) 0 Secret)) (fun (va_s:va_state) _ -> let
    (va_arg48:Vale.Def.Types_s.nat64) = va_get_reg64 rRdx va_s in let
    (va_arg47:Vale.Def.Types_s.nat64) = va_get_reg64 rR8 va_s in let
    (va_arg46:Vale.Def.Types_s.nat64) = va_get_reg64 rR9 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 93 column 99 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg46 va_arg47
    va_arg48 a0) (let (old_r8:nat64) = va_get_reg64 rR8 va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 94 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR8) 0 Secret dst_b 0) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 95 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Xor64 (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rR8)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 96 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 8 inA_b 1 Secret)
    (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 96 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.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 rRsi) 8 Secret)) (fun (va_s:va_state) _ -> let
    (va_arg45:Vale.Def.Types_s.nat64) = va_get_reg64 rRdx va_s in let
    (va_arg44:Vale.Def.Types_s.nat64) = va_get_reg64 rR10 va_s in let
    (va_arg43:Vale.Def.Types_s.nat64) = va_get_reg64 rR11 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 96 column 99 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg43 va_arg44
    va_arg45 a1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 97 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Add64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR9)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 98 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR10) 8 Secret dst_b 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 99 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 16 inA_b 2 Secret)
    (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 99 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.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 rRsi) 16 Secret)) (fun (va_s:va_state) _ ->
    let (va_arg42:Vale.Def.Types_s.nat64) = va_get_reg64 rRdx va_s in let
    (va_arg41:Vale.Def.Types_s.nat64) = va_get_reg64 rRbx va_s in let
    (va_arg40:Vale.Def.Types_s.nat64) = va_get_reg64 rR13 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 99 column 99 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg40 va_arg41
    va_arg42 a2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 100 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR11)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 101 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rRbx) 16 Secret dst_b 2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 102 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 24 inA_b 3 Secret)
    (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 102 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rRax) (va_op_dst_opr64_reg64 rR14) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 24 Secret)) (fun (va_s:va_state) _ ->
    let (va_arg39:Vale.Def.Types_s.nat64) = va_get_reg64 rRdx va_s in let
    (va_arg38:Vale.Def.Types_s.nat64) = va_get_reg64 rR14 va_s in let
    (va_arg37:Vale.Def.Types_s.nat64) = va_get_reg64 rRax va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 102 column 99 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg37 va_arg38
    va_arg39 a3) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 103 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rR13)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 104 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR14) 24 Secret dst_b 3) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 105 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rR8)) (fun (va_s:va_state)
    _ -> let (carry_bit:Vale.Curve25519.Fast_defs.bit) = Vale.Curve25519.Fast_defs.bool_bit
    (Vale.X64.Decls.cf (va_get_flags va_s)) in va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 108 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (carry_bit == 0) (let (va_arg36:prop) = va_mul_nat a (va_get_reg64 rRdx va_s) == 0 +
    Vale.Curve25519.Fast_defs.pow2_four (va_mul_nat (va_get_reg64 rRdx va_s) a0) (va_mul_nat
    (va_get_reg64 rRdx va_s) a1) (va_mul_nat (va_get_reg64 rRdx va_s) a2) (va_mul_nat (va_get_reg64
    rRdx va_s) a3) in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 109 column 21 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (fun (_:unit) -> assert_by_tactic va_arg36 int_canon) (va_QEmpty (())))))))))))))))))))))))))))
val va_qcode_Fast_mul1 (va_mods: va_mods_t) (dst_b inA_b: buffer64)
    : (va_quickCode unit (va_code_Fast_mul1 ()))
let va_qcode_Fast_mul1 (va_mods: va_mods_t) (dst_b inA_b: buffer64)
    : (va_quickCode unit (va_code_Fast_mul1 ())) =
(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 (va_get_mem_heaplet 0 va_s)
        in
        let a1:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read inA_b 1 (va_get_mem_heaplet 0 va_s)
        in
        let a2:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read inA_b 2 (va_get_mem_heaplet 0 va_s)
        in
        let a3:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem_heaplet 0 va_s)
        in
        let a:Prims.nat = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in
        va_qPURE va_range1
          "***** PRECONDITION NOT MET AT line 91 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
          (fun (_: unit) -> Vale.Arch.Types.xor_lemmas ())
          (va_QSeq va_range1
              "***** PRECONDITION NOT MET AT line 93 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
              (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0)
                  (va_op_reg64_reg64 rRsi)
                  0
                  inA_b
                  0
                  Secret)
              (va_QBind va_range1
                  "***** PRECONDITION NOT MET AT line 93 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.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 rRsi)
                          0
                          Secret))
                  (fun (va_s: va_state) _ ->
                      let va_arg48:Vale.Def.Types_s.nat64 = va_get_reg64 rRdx va_s in
                      let va_arg47:Vale.Def.Types_s.nat64 = va_get_reg64 rR8 va_s in
                      let va_arg46:Vale.Def.Types_s.nat64 = va_get_reg64 rR9 va_s in
                      va_qPURE va_range1
                        "***** PRECONDITION NOT MET AT line 93 column 99 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                        (fun (_: unit) ->
                            Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg46
                              va_arg47
                              va_arg48
                              a0)
                        (let old_r8:nat64 = va_get_reg64 rR8 va_s in
                          va_QSeq va_range1
                            "***** PRECONDITION NOT MET AT line 94 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                            (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0)
                                (va_op_reg_opr64_reg64 rRdi)
                                (va_op_reg_opr64_reg64 rR8)
                                0
                                Secret
                                dst_b
                                0)
                            (va_QSeq va_range1
                                "***** PRECONDITION NOT MET AT line 95 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                (va_quick_Xor64 (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rR8))
                                (va_QSeq va_range1
                                    "***** PRECONDITION NOT MET AT line 96 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0)
                                        (va_op_reg64_reg64 rRsi)
                                        8
                                        inA_b
                                        1
                                        Secret)
                                    (va_QBind va_range1
                                        "***** PRECONDITION NOT MET AT line 96 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.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 rRsi)
                                                8
                                                Secret))
                                        (fun (va_s: va_state) _ ->
                                            let va_arg45:Vale.Def.Types_s.nat64 =
                                              va_get_reg64 rRdx va_s
                                            in
                                            let va_arg44:Vale.Def.Types_s.nat64 =
                                              va_get_reg64 rR10 va_s
                                            in
                                            let va_arg43:Vale.Def.Types_s.nat64 =
                                              va_get_reg64 rR11 va_s
                                            in
                                            va_qPURE va_range1
                                              "***** PRECONDITION NOT MET AT line 96 column 99 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                              (fun (_: unit) ->
                                                  Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds
                                                    va_arg43
                                                    va_arg44
                                                    va_arg45
                                                    a1)
                                              (va_QSeq va_range1
                                                  "***** PRECONDITION NOT MET AT line 97 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                  (va_quick_Add64Wrap (va_op_dst_opr64_reg64 rR10)
                                                      (va_op_opr64_reg64 rR9))
                                                  (va_QSeq va_range1
                                                      "***** PRECONDITION NOT MET AT line 98 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                      (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet
                                                              0)
                                                          (va_op_reg_opr64_reg64 rRdi)
                                                          (va_op_reg_opr64_reg64 rR10)
                                                          8
                                                          Secret
                                                          dst_b
                                                          1)
                                                      (va_QSeq va_range1
                                                          "***** PRECONDITION NOT MET AT line 99 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                          (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet
                                                                  0)
                                                              (va_op_reg64_reg64 rRsi)
                                                              16
                                                              inA_b
                                                              2
                                                              Secret)
                                                          (va_QBind va_range1
                                                              "***** PRECONDITION NOT MET AT line 99 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.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 rRsi)
                                                                      16
                                                                      Secret))
                                                              (fun (va_s: va_state) _ ->
                                                                  let va_arg42:Vale.Def.Types_s.nat64
                                                                  =
                                                                    va_get_reg64 rRdx va_s
                                                                  in
                                                                  let va_arg41:Vale.Def.Types_s.nat64
                                                                  =
                                                                    va_get_reg64 rRbx va_s
                                                                  in
                                                                  let va_arg40:Vale.Def.Types_s.nat64
                                                                  =
                                                                    va_get_reg64 rR13 va_s
                                                                  in
                                                                  va_qPURE va_range1
                                                                    "***** PRECONDITION NOT MET AT line 99 column 99 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                    (fun (_: unit) ->
                                                                        Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds
                                                                          va_arg40
                                                                          va_arg41
                                                                          va_arg42
                                                                          a2)
                                                                    (va_QSeq va_range1
                                                                        "***** PRECONDITION NOT MET AT line 100 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                        (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64
                                                                                rRbx)
                                                                            (va_op_opr64_reg64 rR11)
                                                                        )
                                                                        (va_QSeq va_range1
                                                                            "***** PRECONDITION NOT MET AT line 101 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                            (va_quick_Store64_buffer
                                                                                (va_op_heaplet_mem_heaplet
                                                                                    0)
                                                                                (va_op_reg_opr64_reg64
                                                                                    rRdi)
                                                                                (va_op_reg_opr64_reg64
                                                                                    rRbx)
                                                                                16
                                                                                Secret
                                                                                dst_b
                                                                                2)
                                                                            (va_QSeq va_range1
                                                                                "***** PRECONDITION NOT MET AT line 102 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                                (va_quick_Mem64_lemma
                                                                                    (va_op_heaplet_mem_heaplet
                                                                                        0)
                                                                                    (va_op_reg64_reg64
                                                                                        rRsi)
                                                                                    24
                                                                                    inA_b
                                                                                    3
                                                                                    Secret)
                                                                                (va_QBind va_range1
                                                                                    "***** PRECONDITION NOT MET AT line 102 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                                    (va_quick_Mulx64
                                                                                        (va_op_dst_opr64_reg64
                                                                                            rRax)
                                                                                        (va_op_dst_opr64_reg64
                                                                                            rR14)
                                                                                        (va_opr_code_Mem64
                                                                                            (va_op_heaplet_mem_heaplet
                                                                                                0)
                                                                                            (va_op_reg64_reg64
                                                                                                rRsi
                                                                                            )
                                                                                            24
                                                                                            Secret))
                                                                                    (fun
                                                                                        (va_s:
                                                                                          va_state)
                                                                                        _
                                                                                        ->
                                                                                        let va_arg39:Vale.Def.Types_s.nat64
                                                                                        =
                                                                                          va_get_reg64
                                                                                            rRdx
                                                                                            va_s
                                                                                        in
                                                                                        let va_arg38:Vale.Def.Types_s.nat64
                                                                                        =
                                                                                          va_get_reg64
                                                                                            rR14
                                                                                            va_s
                                                                                        in
                                                                                        let va_arg37:Vale.Def.Types_s.nat64
                                                                                        =
                                                                                          va_get_reg64
                                                                                            rRax
                                                                                            va_s
                                                                                        in
                                                                                        va_qPURE va_range1
                                                                                          "***** PRECONDITION NOT MET AT line 102 column 99 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                                          (fun
                                                                                              (_:
                                                                                                unit
                                                                                              )
                                                                                              ->
                                                                                              Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds
                                                                                                va_arg37
                                                                                                va_arg38
                                                                                                va_arg39
                                                                                                a3)
                                                                                          (va_QSeq va_range1
                                                                                              "***** PRECONDITION NOT MET AT line 103 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                                              (va_quick_Adcx64Wrap
                                                                                                  (va_op_dst_opr64_reg64
                                                                                                      rR14

                                                                                                  )
                                                                                                  (va_op_opr64_reg64
                                                                                                      rR13

                                                                                                  ))
                                                                                              (va_QSeq
                                                                                                  va_range1
                                                                                                  "***** PRECONDITION NOT MET AT line 104 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                                                  (va_quick_Store64_buffer
                                                                                                      (
                                                                                                        va_op_heaplet_mem_heaplet
                                                                                                          0

                                                                                                      )
                                                                                                      (
                                                                                                        va_op_reg_opr64_reg64
                                                                                                          rRdi

                                                                                                      )
                                                                                                      (
                                                                                                        va_op_reg_opr64_reg64
                                                                                                          rR14

                                                                                                      )
                                                                                                      24
                                                                                                      Secret
                                                                                                      dst_b
                                                                                                      3

                                                                                                  )
                                                                                                  (va_QBind
                                                                                                      va_range1
                                                                                                      "***** PRECONDITION NOT MET AT line 105 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                                                      (
                                                                                                        va_quick_Adcx64Wrap
                                                                                                          (
                                                                                                            va_op_dst_opr64_reg64
                                                                                                              rRax

                                                                                                          )
                                                                                                          (
                                                                                                            va_op_opr64_reg64
                                                                                                              rR8

                                                                                                          )

                                                                                                      )
                                                                                                      (
                                                                                                        fun
                                                                                                          (
                                                                                                            va_s:
                                                                                                            va_state
                                                                                                          )
                                                                                                          _
                                                                                                          ->
                                                                                                          let
                                                                                                          carry_bit:Vale.Curve25519.Fast_defs.bit
                                                                                                          =
                                                                                                            Vale.Curve25519.Fast_defs.bool_bit
                                                                                                              (
                                                                                                                Vale.X64.Decls.cf
                                                                                                                  (
                                                                                                                    va_get_flags
                                                                                                                      va_s

                                                                                                                  )

                                                                                                              )

                                                                                                          in
                                                                                                          va_qAssert
                                                                                                            va_range1
                                                                                                            "***** PRECONDITION NOT MET AT line 108 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                                                            (
                                                                                                              carry_bit ==
                                                                                                              0
                                                                                                            )
                                                                                                            (
                                                                                                              let
                                                                                                              va_arg36:prop
                                                                                                              =
                                                                                                                va_mul_nat
                                                                                                                  a
                                                                                                                  (
                                                                                                                    va_get_reg64
                                                                                                                      rRdx
                                                                                                                      va_s

                                                                                                                  )
                                                                                                                 ==
                                                                                                                0 +
                                                                                                                Vale.Curve25519.Fast_defs.pow2_four
                                                                                                                  (
                                                                                                                    va_mul_nat
                                                                                                                      (
                                                                                                                        va_get_reg64
                                                                                                                          rRdx
                                                                                                                          va_s

                                                                                                                      )
                                                                                                                      a0

                                                                                                                  )
                                                                                                                  (
                                                                                                                    va_mul_nat
                                                                                                                      (
                                                                                                                        va_get_reg64
                                                                                                                          rRdx
                                                                                                                          va_s

                                                                                                                      )
                                                                                                                      a1

                                                                                                                  )
                                                                                                                  (
                                                                                                                    va_mul_nat
                                                                                                                      (
                                                                                                                        va_get_reg64
                                                                                                                          rRdx
                                                                                                                          va_s

                                                                                                                      )
                                                                                                                      a2

                                                                                                                  )
                                                                                                                  (
                                                                                                                    va_mul_nat
                                                                                                                      (
                                                                                                                        va_get_reg64
                                                                                                                          rRdx
                                                                                                                          va_s

                                                                                                                      )
                                                                                                                      a3

                                                                                                                  )

                                                                                                              in
                                                                                                              va_qPURE
                                                                                                                va_range1
                                                                                                                "***** PRECONDITION NOT MET AT line 109 column 21 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                                                                (
                                                                                                                  fun
                                                                                                                    (
                                                                                                                      _:
                                                                                                                      unit
                                                                                                                    )
                                                                                                                    ->
                                                                                                                    assert_by_tactic
                                                                                                                      va_arg36
                                                                                                                      int_canon

                                                                                                                )
                                                                                                                (
                                                                                                                  va_QEmpty
                                                                                                                    (
                                                                                                                      ()
                                                                                                                    )

                                                                                                                )

                                                                                                            )

                                                                                                      )

                                                                                                  ))
                                                                                          ))))))))))
                                              )))))))))))
Vale.Curve25519.X64.FastUtil.fst.checked
Vale.X64.State.fsti.checked Vale.X64.QuickCodes.fsti.checked Vale.X64.QuickCode.fst.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.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.FastUtil_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.FastUtil.fst
Vale.X64.QuickCode.va_mods_t Vale.X64.Memory.buffer64 Vale.X64.QuickCodes.qblock Prims.unit Prims.Cons Vale.X64.Decls.va_code Vale.X64.InsMem.va_code_Mem64_lemma Vale.X64.InsBasic.va_code_Mulx64 Vale.X64.Decls.va_op_dst_opr64_reg64 Vale.X64.Machine_s.rR9 Vale.X64.Machine_s.rR8 Vale.X64.Decls.va_opr_code_Mem64 Vale.X64.Decls.va_op_heaplet_mem_heaplet Vale.X64.Decls.va_op_reg64_reg64 Vale.X64.Machine_s.rRsi Vale.Arch.HeapTypes_s.Secret Vale.X64.InsMem.va_code_Store64_buffer Vale.X64.Decls.va_op_reg_opr64_reg64 Vale.X64.Machine_s.rRdi Vale.X64.InsBasic.va_code_Xor64 Vale.X64.Decls.va_op_opr64_reg64 Vale.X64.Machine_s.rR11 Vale.X64.Machine_s.rR10 Vale.X64.InsBasic.va_code_Add64Wrap Vale.X64.Machine_s.rR13 Vale.X64.Machine_s.rRbx Vale.X64.InsBasic.va_code_Adcx64Wrap Vale.X64.Machine_s.rRax Vale.X64.Machine_s.rR14 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.InsMem.va_quick_Mem64_lemma Vale.X64.QuickCodes.va_QBind Vale.X64.InsBasic.va_quick_Mulx64 Prims.op_Addition Prims.op_Multiply 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_Xor64 Vale.X64.InsBasic.va_quick_Add64Wrap Vale.X64.InsBasic.va_quick_Adcx64Wrap Vale.X64.QuickCodes.va_qAssert FStar.Tactics.Effect.with_tactic Vale.Curve25519.FastUtil_helpers.int_canon Prims.squash FStar.Tactics.Effect.assert_by_tactic Vale.X64.QuickCodes.va_QEmpty Prims.prop Vale.X64.Decls.va_mul_nat Vale.X64.Decls.va_get_reg64 Vale.X64.Machine_s.rRdx Vale.Curve25519.Fast_defs.pow2_four Vale.Curve25519.Fast_defs.bit Vale.Curve25519.Fast_defs.bool_bit Vale.X64.Decls.cf Vale.X64.Decls.va_get_flags Vale.X64.QuickCodes.quickCodes Prims.nat 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.FastUtil.va_code_Fast_mul1
module Vale.Curve25519.X64.FastUtil
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsMem
open Vale.X64.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.FastUtil_helpers
open Vale.X64.CPU_Features_s
#reset-options "--z3rlimit 60"
//-- Fast_mul1
#push-options "--z3rlimit 600"

val va_code_Fast_mul1 : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Fast_mul1 () =
  (va_Block (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 rRsi) 0 Secret)) (va_CCons (va_code_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR8) 0
    Secret) (va_CCons (va_code_Xor64 (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rR8)) (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 rRsi) 8 Secret)) (va_CCons (va_code_Add64Wrap (va_op_dst_opr64_reg64 rR10)
    (va_op_opr64_reg64 rR9)) (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 Secret) (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 rRsi) 16 Secret)) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rRbx)
    (va_op_opr64_reg64 rR11)) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rRbx) 16 Secret) (va_CCons
    (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx64 (va_op_dst_opr64_reg64 rRax)
    (va_op_dst_opr64_reg64 rR14) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRsi) 24 Secret)) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rR14)
    (va_op_opr64_reg64 rR13)) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR14) 24 Secret) (va_CCons
    (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rR8)) (va_CNil
    ())))))))))))))))))))

val va_codegen_success_Fast_mul1 : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Fast_mul1 () =
  (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 rRsi) 0 Secret)) (va_pbool_and
    (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR8) 0 Secret) (va_pbool_and (va_codegen_success_Xor64
    (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rR8)) (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 rRsi) 8 Secret)) (va_pbool_and
    (va_codegen_success_Add64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR9))
    (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 Secret) (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 rRsi) 16 Secret)) (va_pbool_and
    (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR11))
    (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 rRbx) 16 Secret) (va_pbool_and
    (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx64
    (va_op_dst_opr64_reg64 rRax) (va_op_dst_opr64_reg64 rR14) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 24 Secret)) (va_pbool_and
    (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rR13))
    (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 rR14) 24 Secret) (va_pbool_and
    (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rR8)) (va_ttrue
    ()))))))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Fast_mul1 (va_mods:va_mods_t) (dst_b:buffer64) (inA_b:buffer64) : (va_quickCode unit
val va_qcode_Fast_mul1 (va_mods: va_mods_t) (dst_b inA_b: buffer64)
    : (va_quickCode unit (va_code_Fast_mul1 ()))

    va_mods: Vale.X64.QuickCode.va_mods_t ->
    dst_b: Vale.X64.Memory.buffer64 ->
    inA_b: Vale.X64.Memory.buffer64
  -> Vale.X64.QuickCode.va_quickCode Prims.unit (Vale.Curve25519.X64.FastUtil.va_code_Fast_mul1 ())