val va_qcode_Cswap2 (va_mods: va_mods_t) (bit_in: nat64) (p0_b p1_b: buffer64)
    : (va_quickCode unit (va_code_Cswap2 ()))
let va_qcode_Cswap2 (va_mods:va_mods_t) (bit_in:nat64) (p0_b:buffer64) (p1_b:buffer64) :
  (va_quickCode unit (va_code_Cswap2 ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (old_p0_0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read p0_b 0 (va_get_mem va_s) in
    let (old_p0_1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read p0_b 1 (va_get_mem va_s)
    in let (old_p0_2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read p0_b 2 (va_get_mem
    va_s) in let (old_p0_3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read p0_b 3
    (va_get_mem va_s) in let (old_p0_4:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read p0_b
    4 (va_get_mem va_s) in let (old_p0_5:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    p0_b 5 (va_get_mem va_s) in let (old_p0_6:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read p0_b 6 (va_get_mem va_s) in let (old_p0_7:Vale.Def.Types_s.nat64)
    = Vale.X64.Decls.buffer64_read p0_b 7 (va_get_mem va_s) in let
    (old_p1_0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read p1_b 0 (va_get_mem va_s) in
    let (old_p1_1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read p1_b 1 (va_get_mem va_s)
    in let (old_p1_2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read p1_b 2 (va_get_mem
    va_s) in let (old_p1_3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read p1_b 3
    (va_get_mem va_s) in let (old_p1_4:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read p1_b
    4 (va_get_mem va_s) in let (old_p1_5:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    p1_b 5 (va_get_mem va_s) in let (old_p1_6:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read p1_b 6 (va_get_mem va_s) in let (old_p1_7:Vale.Def.Types_s.nat64)
    = Vale.X64.Decls.buffer64_read p1_b 7 (va_get_mem va_s) in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 932 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_CreateHeaplets ([declare_buffer64 p0_b 0 Secret Mutable; declare_buffer64 p1_b 0
    Secret Mutable])) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 936 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Comment
    "Transfer bit into CF flag"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 937 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 rRdi) (va_const_opr64 18446744073709551615))
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 939 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 940 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Comment
    "cswap p1[0], p2[0]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 941 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Cswap_single 0 p0_b p1_b) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 943 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 944 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Comment
    "cswap p1[1], p2[1]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 945 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Cswap_single 1 p0_b p1_b) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 947 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 948 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Comment
    "cswap p1[2], p2[2]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 949 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Cswap_single 2 p0_b p1_b) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 951 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 952 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Comment
    "cswap p1[3], p2[3]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 953 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Cswap_single 3 p0_b p1_b) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 955 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 956 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Comment
    "cswap p1[4], p2[4]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 957 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Cswap_single 4 p0_b p1_b) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 959 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 960 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Comment
    "cswap p1[5], p2[5]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 961 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Cswap_single 5 p0_b p1_b) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 963 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 964 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Comment
    "cswap p1[6], p2[6]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 965 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Cswap_single 6 p0_b p1_b) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 967 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 968 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Comment
    "cswap p1[7], p2[7]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 969 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Cswap_single 7 p0_b p1_b) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 971 column 20 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_DestroyHeaplets ()) (va_QEmpty (())))))))))))))))))))))))))))))))
val va_qcode_Cswap2 (va_mods: va_mods_t) (bit_in: nat64) (p0_b p1_b: buffer64)
    : (va_quickCode unit (va_code_Cswap2 ()))
let va_qcode_Cswap2 (va_mods: va_mods_t) (bit_in: nat64) (p0_b p1_b: buffer64)
    : (va_quickCode unit (va_code_Cswap2 ())) =
(qblock va_mods
    (fun (va_s: va_state) ->
        let va_old_s:va_state = va_s in
        let old_p0_0:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read p0_b 0 (va_get_mem va_s)
        in
        let old_p0_1:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read p0_b 1 (va_get_mem va_s)
        in
        let old_p0_2:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read p0_b 2 (va_get_mem va_s)
        in
        let old_p0_3:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read p0_b 3 (va_get_mem va_s)
        in
        let old_p0_4:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read p0_b 4 (va_get_mem va_s)
        in
        let old_p0_5:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read p0_b 5 (va_get_mem va_s)
        in
        let old_p0_6:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read p0_b 6 (va_get_mem va_s)
        in
        let old_p0_7:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read p0_b 7 (va_get_mem va_s)
        in
        let old_p1_0:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read p1_b 0 (va_get_mem va_s)
        in
        let old_p1_1:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read p1_b 1 (va_get_mem va_s)
        in
        let old_p1_2:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read p1_b 2 (va_get_mem va_s)
        in
        let old_p1_3:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read p1_b 3 (va_get_mem va_s)
        in
        let old_p1_4:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read p1_b 4 (va_get_mem va_s)
        in
        let old_p1_5:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read p1_b 5 (va_get_mem va_s)
        in
        let old_p1_6:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read p1_b 6 (va_get_mem va_s)
        in
        let old_p1_7:Vale.Def.Types_s.nat64 =
          Vale.X64.Decls.buffer64_read p1_b 7 (va_get_mem va_s)
        in
        va_QSeq va_range1
          "***** PRECONDITION NOT MET AT line 932 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
          (va_quick_CreateHeaplets ([
                  declare_buffer64 p0_b 0 Secret Mutable;
                  declare_buffer64 p1_b 0 Secret Mutable
                ]))
          (va_QSeq va_range1
              "***** PRECONDITION NOT MET AT line 936 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
              (va_quick_Comment "Transfer bit into CF flag")
              (va_QSeq va_range1
                  "***** PRECONDITION NOT MET AT line 937 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 rRdi)
                      (va_const_opr64 18446744073709551615))
                  (va_QSeq va_range1
                      "***** PRECONDITION NOT MET AT line 939 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                      (va_quick_Newline ())
                      (va_QSeq va_range1
                          "***** PRECONDITION NOT MET AT line 940 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                          (va_quick_Comment "cswap p1[0], p2[0]")
                          (va_QSeq va_range1
                              "***** PRECONDITION NOT MET AT line 941 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                              (va_quick_Cswap_single 0 p0_b p1_b)
                              (va_QSeq va_range1
                                  "***** PRECONDITION NOT MET AT line 943 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                  (va_quick_Newline ())
                                  (va_QSeq va_range1
                                      "***** PRECONDITION NOT MET AT line 944 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                      (va_quick_Comment "cswap p1[1], p2[1]")
                                      (va_QSeq va_range1
                                          "***** PRECONDITION NOT MET AT line 945 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                          (va_quick_Cswap_single 1 p0_b p1_b)
                                          (va_QSeq va_range1
                                              "***** PRECONDITION NOT MET AT line 947 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                              (va_quick_Newline ())
                                              (va_QSeq va_range1
                                                  "***** PRECONDITION NOT MET AT line 948 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                  (va_quick_Comment "cswap p1[2], p2[2]")
                                                  (va_QSeq va_range1
                                                      "***** PRECONDITION NOT MET AT line 949 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                      (va_quick_Cswap_single 2 p0_b p1_b)
                                                      (va_QSeq va_range1
                                                          "***** PRECONDITION NOT MET AT line 951 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                          (va_quick_Newline ())
                                                          (va_QSeq va_range1
                                                              "***** PRECONDITION NOT MET AT line 952 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                              (va_quick_Comment "cswap p1[3], p2[3]"
                                                              )
                                                              (va_QSeq va_range1
                                                                  "***** PRECONDITION NOT MET AT line 953 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                  (va_quick_Cswap_single 3 p0_b p1_b
                                                                  )
                                                                  (va_QSeq va_range1
                                                                      "***** PRECONDITION NOT MET AT line 955 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                      (va_quick_Newline ())
                                                                      (va_QSeq va_range1
                                                                          "***** PRECONDITION NOT MET AT line 956 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                          (va_quick_Comment "cswap p1[4], p2[4]"
                                                                            )
                                                                          (va_QSeq va_range1
                                                                              "***** PRECONDITION NOT MET AT line 957 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                              (va_quick_Cswap_single
                                                                                  4
                                                                                  p0_b
                                                                                  p1_b)
                                                                              (va_QSeq va_range1
                                                                                  "***** PRECONDITION NOT MET AT line 959 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                                  (va_quick_Newline ()
                                                                                    )
                                                                                  (va_QSeq va_range1
                                                                                      "***** PRECONDITION NOT MET AT line 960 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                                      (va_quick_Comment
                                                                                          "cswap p1[5], p2[5]"
                                                                                        )
                                                                                      (va_QSeq va_range1
                                                                                          "***** PRECONDITION NOT MET AT line 961 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                                          (va_quick_Cswap_single
                                                                                              5
                                                                                              p0_b
                                                                                              p1_b)
                                                                                          (va_QSeq va_range1
                                                                                              "***** PRECONDITION NOT MET AT line 963 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                                              (va_quick_Newline
                                                                                                  ()
                                                                                              )
                                                                                              (va_QSeq
                                                                                                  va_range1
                                                                                                  "***** PRECONDITION NOT MET AT line 964 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                                                  (va_quick_Comment
                                                                                                      "cswap p1[6], p2[6]"

                                                                                                  )
                                                                                                  (va_QSeq
                                                                                                      va_range1
                                                                                                      "***** PRECONDITION NOT MET AT line 965 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                                                      (
                                                                                                        va_quick_Cswap_single
                                                                                                          6
                                                                                                          p0_b
                                                                                                          p1_b

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

                                                                                                          )
                                                                                                          (
                                                                                                            va_QSeq
                                                                                                              va_range1
                                                                                                              "***** PRECONDITION NOT MET AT line 968 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                                                              (
                                                                                                                va_quick_Comment
                                                                                                                  "cswap p1[7], p2[7]"

                                                                                                              )
                                                                                                              (
                                                                                                                va_QSeq
                                                                                                                  va_range1
                                                                                                                  "***** PRECONDITION NOT MET AT line 969 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
                                                                                                                  (
                                                                                                                    va_quick_Cswap_single
                                                                                                                      7
                                                                                                                      p0_b
                                                                                                                      p1_b

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

                                                                                                                      )
                                                                                                                      (
                                                                                                                        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.nat64 Vale.X64.Memory.buffer64 Vale.X64.QuickCodes.qblock Prims.unit Prims.Cons Vale.X64.Decls.va_code Vale.X64.InsMem.va_code_CreateHeaplets Vale.X64.InsBasic.va_code_Comment Vale.X64.InsBasic.va_code_Add64Wrap Vale.X64.Decls.va_op_dst_opr64_reg64 Vale.X64.Machine_s.rRdi Vale.X64.Decls.va_const_opr64 Vale.X64.InsBasic.va_code_Newline Vale.Curve25519.X64.FastUtil.va_code_Cswap_single Vale.X64.InsMem.va_code_DestroyHeaplets Prims.Nil Vale.X64.Machine_s.precode Vale.X64.Decls.ins Vale.X64.Decls.ocmp Vale.X64.Decls.va_state Vale.X64.QuickCodes.va_QSeq Vale.X64.QuickCodes.va_range1 Vale.X64.InsMem.va_quick_CreateHeaplets Vale.Arch.HeapImpl.buffer_info Vale.X64.InsMem.declare_buffer64 Vale.Arch.HeapTypes_s.Secret Vale.Arch.HeapImpl.Mutable Vale.X64.InsBasic.va_quick_Comment Vale.X64.InsBasic.va_quick_Add64Wrap Vale.X64.InsBasic.va_quick_Newline Vale.Curve25519.X64.FastUtil.va_quick_Cswap_single Vale.X64.InsMem.va_quick_DestroyHeaplets Vale.X64.QuickCodes.va_QEmpty Vale.Def.Words_s.nat64 Vale.X64.Decls.buffer64_read Vale.X64.Decls.va_get_mem Vale.X64.State.vale_state Vale.X64.QuickCodes.quickCodes Vale.X64.QuickCode.va_quickCode Vale.Curve25519.X64.FastUtil.va_code_Cswap2
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
  (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_lemma_Fast_mul1 : va_b0:va_code -> va_s0:va_state -> dst_b:buffer64 -> inA_b:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Fast_mul1 ()) va_s0 /\ va_get_ok va_s0 /\ (let
    (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0 (va_get_mem_heaplet 0 va_s0)
    in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 1 (va_get_mem_heaplet 0
    va_s0) in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 2
    (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 3 (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four
    a0 a1 a2 a3 in adx_enabled /\ bmi2_enabled /\ (Vale.X64.Decls.buffers_disjoint dst_b inA_b \/
    inA_b == dst_b) /\ Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64
    rRdi va_s0) dst_b 4 (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRsi va_s0) inA_b 4 (va_get_mem_layout va_s0)
    Secret)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0 (va_get_mem_heaplet 0
    va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 1
    (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 2 (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in let d0 = Vale.X64.Decls.buffer64_read dst_b
    0 (va_get_mem_heaplet 0 va_sM) in let d1 = Vale.X64.Decls.buffer64_read dst_b 1
    (va_get_mem_heaplet 0 va_sM) in let d2 = Vale.X64.Decls.buffer64_read dst_b 2
    (va_get_mem_heaplet 0 va_sM) in let d3 = Vale.X64.Decls.buffer64_read dst_b 3
    (va_get_mem_heaplet 0 va_sM) in let d = Vale.Curve25519.Fast_defs.pow2_five d0 d1 d2 d3
    (va_get_reg64 rRax va_sM) in d == va_mul_nat a (va_get_reg64 rRdx va_s0) /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b 4
    (va_get_mem_layout va_sM) Secret /\ Vale.X64.Decls.modifies_buffer dst_b (va_get_mem_heaplet 0
    va_s0) (va_get_mem_heaplet 0 va_sM)) /\ va_state_eq va_sM (va_update_flags va_sM
    (va_update_mem_heaplet 0 va_sM (va_update_reg64 rR14 va_sM (va_update_reg64 rR13 va_sM
    (va_update_reg64 rRbx va_sM (va_update_reg64 rR11 va_sM (va_update_reg64 rR10 va_sM
    (va_update_reg64 rR9 va_sM (va_update_reg64 rR8 va_sM (va_update_reg64 rRax va_sM (va_update_ok
    va_sM (va_update_mem va_sM va_s0))))))))))))))
[@"opaque_to_smt"]
let va_lemma_Fast_mul1 va_b0 va_s0 dst_b inA_b =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64
    rR13; va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64
    rR8; va_Mod_reg64 rRax; va_Mod_ok; va_Mod_mem] in
  let va_qc = va_qcode_Fast_mul1 va_mods dst_b inA_b in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Fast_mul1 ()) va_qc va_s0 (fun va_s0
    va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 52 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_get_ok va_sM) /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 1 (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b 2 (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem_heaplet 0 va_s0)
    in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in label va_range1
    "***** POSTCONDITION NOT MET AT line 81 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d0 = Vale.X64.Decls.buffer64_read dst_b 0 (va_get_mem_heaplet 0 va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 82 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d1 = Vale.X64.Decls.buffer64_read dst_b 1 (va_get_mem_heaplet 0 va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 83 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d2 = Vale.X64.Decls.buffer64_read dst_b 2 (va_get_mem_heaplet 0 va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 84 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d3 = Vale.X64.Decls.buffer64_read dst_b 3 (va_get_mem_heaplet 0 va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 85 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d = Vale.Curve25519.Fast_defs.pow2_five d0 d1 d2 d3 (va_get_reg64 rRax va_sM) in label
    va_range1
    "***** POSTCONDITION NOT MET AT line 86 column 24 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (d == va_mul_nat a (va_get_reg64 rRdx va_s0)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 88 column 69 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b 4
    (va_get_mem_layout va_sM) Secret) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 89 column 50 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (Vale.X64.Decls.modifies_buffer dst_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet 0
    va_sM))))))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14; va_Mod_reg64 rR13;
    va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8;
    va_Mod_reg64 rRax; va_Mod_ok; va_Mod_mem]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Fast_mul1 (dst_b:buffer64) (inA_b:buffer64) (va_s0:va_state) (va_k:(va_state -> unit ->
  Type0)) : Type0 =
  (va_get_ok va_s0 /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 1 (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b 2 (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem_heaplet 0 va_s0)
    in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in adx_enabled /\
    bmi2_enabled /\ (Vale.X64.Decls.buffers_disjoint dst_b inA_b \/ inA_b == dst_b) /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) dst_b 4
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) inA_b 4 (va_get_mem_layout va_s0) Secret) /\ (forall
    (va_x_mem:vale_heap) (va_x_rax:nat64) (va_x_r8:nat64) (va_x_r9:nat64) (va_x_r10:nat64)
    (va_x_r11:nat64) (va_x_rbx:nat64) (va_x_r13:nat64) (va_x_r14:nat64) (va_x_heap0:vale_heap)
    (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_mem_heaplet 0
    va_x_heap0 (va_upd_reg64 rR14 va_x_r14 (va_upd_reg64 rR13 va_x_r13 (va_upd_reg64 rRbx va_x_rbx
    (va_upd_reg64 rR11 va_x_r11 (va_upd_reg64 rR10 va_x_r10 (va_upd_reg64 rR9 va_x_r9 (va_upd_reg64
    rR8 va_x_r8 (va_upd_reg64 rRax va_x_rax (va_upd_mem va_x_mem va_s0)))))))))) in va_get_ok va_sM
    /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0 (va_get_mem_heaplet
    0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 1
    (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 2 (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in let d0 = Vale.X64.Decls.buffer64_read dst_b
    0 (va_get_mem_heaplet 0 va_sM) in let d1 = Vale.X64.Decls.buffer64_read dst_b 1
    (va_get_mem_heaplet 0 va_sM) in let d2 = Vale.X64.Decls.buffer64_read dst_b 2
    (va_get_mem_heaplet 0 va_sM) in let d3 = Vale.X64.Decls.buffer64_read dst_b 3
    (va_get_mem_heaplet 0 va_sM) in let d = Vale.Curve25519.Fast_defs.pow2_five d0 d1 d2 d3
    (va_get_reg64 rRax va_sM) in d == va_mul_nat a (va_get_reg64 rRdx va_s0) /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b 4
    (va_get_mem_layout va_sM) Secret /\ Vale.X64.Decls.modifies_buffer dst_b (va_get_mem_heaplet 0
    va_s0) (va_get_mem_heaplet 0 va_sM)) ==> va_k va_sM (())))


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

[@ "opaque_to_smt" va_qattr]
let va_quick_Fast_mul1 (dst_b:buffer64) (inA_b:buffer64) : (va_quickCode unit (va_code_Fast_mul1
  ())) =
  (va_QProc (va_code_Fast_mul1 ()) ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR14;
    va_Mod_reg64 rR13; va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9;
    va_Mod_reg64 rR8; va_Mod_reg64 rRax; va_Mod_mem]) (va_wp_Fast_mul1 dst_b inA_b)
    (va_wpProof_Fast_mul1 dst_b inA_b))
#pop-options
//--
//-- Fast_add1
#push-options "--z3rlimit 600"

[@ "opaque_to_smt" va_qattr]
let va_code_Fast_add1 () =
  (va_Block (va_CCons (va_code_CreateHeaplets ()) (va_CCons (va_code_Comment
    "Clear registers to propagate the carry bit"
    ) (va_CCons (va_code_Xor64 (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rR8)) (va_CCons
    (va_code_Xor64 (va_op_dst_opr64_reg64 rR9) (va_op_opr64_reg64 rR9)) (va_CCons (va_code_Xor64
    (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR10)) (va_CCons (va_code_Xor64
    (va_op_dst_opr64_reg64 rR11) (va_op_opr64_reg64 rR11)) (va_CCons (va_code_Xor64
    (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRax)) (va_CCons (va_code_Newline ()) (va_CCons
    (va_code_Comment
    "Begin addition chain"
    ) (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Add64Wrap (va_op_dst_opr64_reg64 rRdx)
    (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 rRdx) 0 Secret) (va_CCons (va_code_Mem64_lemma ()) (va_CCons
    (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet
    0) (va_op_reg64_reg64 rRsi) 8 Secret)) (va_CCons (va_code_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR8) 8
    Secret) (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64
    rR9) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 16 Secret))
    (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR9) 16 Secret) (va_CCons (va_code_Mem64_lemma ()) (va_CCons
    (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rR10) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet
    0) (va_op_reg64_reg64 rRsi) 24 Secret)) (va_CCons (va_code_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR10) 24
    Secret) (va_CCons (va_code_Newline ()) (va_CCons (va_code_Comment
    "Return the carry bit in a register"
    ) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rR11))
    (va_CCons (va_code_DestroyHeaplets ()) (va_CNil ())))))))))))))))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Fast_add1 () =
  (va_pbool_and (va_codegen_success_CreateHeaplets ()) (va_pbool_and (va_codegen_success_Comment
    "Clear registers to propagate the carry bit"
    ) (va_pbool_and (va_codegen_success_Xor64 (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rR8))
    (va_pbool_and (va_codegen_success_Xor64 (va_op_dst_opr64_reg64 rR9) (va_op_opr64_reg64 rR9))
    (va_pbool_and (va_codegen_success_Xor64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR10))
    (va_pbool_and (va_codegen_success_Xor64 (va_op_dst_opr64_reg64 rR11) (va_op_opr64_reg64 rR11))
    (va_pbool_and (va_codegen_success_Xor64 (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRax))
    (va_pbool_and (va_codegen_success_Newline ()) (va_pbool_and (va_codegen_success_Comment
    "Begin addition chain"
    ) (va_pbool_and (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Add64Wrap
    (va_op_dst_opr64_reg64 rRdx) (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 rRdx) 0
    Secret) (va_pbool_and (va_codegen_success_Mem64_lemma ()) (va_pbool_and
    (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 8 Secret)) (va_pbool_and
    (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR8) 8 Secret) (va_pbool_and (va_codegen_success_Mem64_lemma ())
    (va_pbool_and (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rR9) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 16 Secret)) (va_pbool_and
    (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR9) 16 Secret) (va_pbool_and (va_codegen_success_Mem64_lemma ())
    (va_pbool_and (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rR10) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 24 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 rR10) 24 Secret) (va_pbool_and (va_codegen_success_Newline ())
    (va_pbool_and (va_codegen_success_Comment
    "Return the carry bit in a register"
    ) (va_pbool_and (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64
    rR11)) (va_pbool_and (va_codegen_success_DestroyHeaplets ()) (va_ttrue
    ()))))))))))))))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Fast_add1 (va_mods:va_mods_t) (dst_b:buffer64) (inA_b:buffer64) (inB:nat64) :
  (va_quickCode unit (va_code_Fast_add1 ())) =
  (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 va_s) in let
    (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 1 (va_get_mem va_s) in let
    (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 2 (va_get_mem va_s) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem va_s) in let
    (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 224 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_CreateHeaplets ([declare_buffer64 inA_b 0 Secret Immutable; declare_buffer64 dst_b 0
    Secret Mutable])) (fun (va_s:va_state) _ -> va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 228 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 229 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Comment
    "Clear registers to propagate the carry bit"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 230 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 231 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 rR9) (va_op_opr64_reg64 rR9)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 232 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 rR10) (va_op_opr64_reg64 rR10)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 233 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 rR11) (va_op_opr64_reg64 rR11)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 234 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 rRax) (va_op_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 236 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 237 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Comment
    "Begin addition chain"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 238 column 24 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_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 238 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 rRdx) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet
    0) (va_op_reg64_reg64 rRsi) 0 Secret)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 239 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 rRdx) 0 Secret dst_b 0) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 241 column 26 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_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 241 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 rR8) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet
    0) (va_op_reg64_reg64 rRsi) 8 Secret)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 242 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) 8 Secret dst_b 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 244 column 26 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_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 244 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 rR9) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet
    0) (va_op_reg64_reg64 rRsi) 16 Secret)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 245 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 rR9) 16 Secret dst_b 2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 247 column 27 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_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 247 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 rR10) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet
    0) (va_op_reg64_reg64 rRsi) 24 Secret)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 248 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) 24 Secret dst_b 3) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 250 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 251 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Comment
    "Return the carry bit in a register"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 252 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 rR11)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 254 column 20 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_DestroyHeaplets ()) (va_QEmpty (())))))))))))))))))))))))))))))



[@"opaque_to_smt"]
let va_lemma_Fast_add1 va_b0 va_s0 dst_b inA_b inB =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_mem_layout; va_Mod_mem_heaplet 0; va_Mod_reg64
    rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx; va_Mod_reg64
    rRax; va_Mod_ok; va_Mod_mem] in
  let va_qc = va_qcode_Fast_add1 va_mods dst_b inA_b inB in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Fast_add1 ()) va_qc va_s0 (fun va_s0
    va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 182 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_get_ok va_sM) /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0
    (va_get_mem va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 1
    (va_get_mem va_s0) in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 2
    (va_get_mem va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 3
    (va_get_mem va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in
    label va_range1
    "***** POSTCONDITION NOT MET AT line 215 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d0 = Vale.X64.Decls.buffer64_read dst_b 0 (va_get_mem va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 216 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d1 = Vale.X64.Decls.buffer64_read dst_b 1 (va_get_mem va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 217 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d2 = Vale.X64.Decls.buffer64_read dst_b 2 (va_get_mem va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 218 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d3 = Vale.X64.Decls.buffer64_read dst_b 3 (va_get_mem va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 219 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d = Vale.Curve25519.Fast_defs.pow2_five d0 d1 d2 d3 (va_get_reg64 rRax va_sM) in label
    va_range1
    "***** POSTCONDITION NOT MET AT line 220 column 24 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (d == a + va_get_reg64 rRdx va_s0) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 222 column 46 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (Vale.X64.Decls.modifies_buffer dst_b (va_get_mem va_s0) (va_get_mem va_sM))))))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_layout; va_Mod_mem_heaplet 0; va_Mod_reg64 rR11;
    va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx; va_Mod_reg64 rRax;
    va_Mod_ok; va_Mod_mem]) va_sM va_s0;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Fast_add1 dst_b inA_b inB va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Fast_add1 (va_code_Fast_add1 ()) va_s0 dst_b inA_b inB in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_mem_layout va_sM
    (va_update_mem_heaplet 0 va_sM (va_update_reg64 rR11 va_sM (va_update_reg64 rR10 va_sM
    (va_update_reg64 rR9 va_sM (va_update_reg64 rR8 va_sM (va_update_reg64 rRdx va_sM
    (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem va_sM va_s0))))))))))));
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_layout; va_Mod_mem_heaplet 0; va_Mod_reg64 rR11;
    va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx; va_Mod_reg64 rRax;
    va_Mod_mem]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

#pop-options
//--
//-- Fast_add1_stdcall
#push-options "--z3rlimit 600"

[@ "opaque_to_smt" va_qattr]
let va_code_Fast_add1_stdcall win =
  (va_Block (va_CCons (va_code_Push_Secret (va_op_reg_opr64_reg64 rRdi)) (va_CCons
    (va_code_Push_Secret (va_op_reg_opr64_reg64 rRsi)) (va_CCons (if win then va_Block (va_CCons
    (va_code_Mov64 (va_op_dst_opr64_reg64 rRdi) (va_op_opr64_reg64 rRcx)) (va_CCons (va_code_Mov64
    (va_op_dst_opr64_reg64 rRsi) (va_op_opr64_reg64 rRdx)) (va_CCons (va_code_Mov64
    (va_op_dst_opr64_reg64 rRdx) (va_op_opr64_reg64 rR8)) (va_CNil ())))) else va_Block (va_CNil
    ())) (va_CCons (va_code_Fast_add1 ()) (va_CCons (va_code_Pop_Secret (va_op_dst_opr64_reg64
    rRsi)) (va_CCons (va_code_Pop_Secret (va_op_dst_opr64_reg64 rRdi)) (va_CNil ()))))))))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Fast_add1_stdcall win =
  (va_pbool_and (va_codegen_success_Push_Secret (va_op_reg_opr64_reg64 rRdi)) (va_pbool_and
    (va_codegen_success_Push_Secret (va_op_reg_opr64_reg64 rRsi)) (va_pbool_and (if win then
    va_pbool_and (va_codegen_success_Mov64 (va_op_dst_opr64_reg64 rRdi) (va_op_opr64_reg64 rRcx))
    (va_pbool_and (va_codegen_success_Mov64 (va_op_dst_opr64_reg64 rRsi) (va_op_opr64_reg64 rRdx))
    (va_pbool_and (va_codegen_success_Mov64 (va_op_dst_opr64_reg64 rRdx) (va_op_opr64_reg64 rR8))
    (va_ttrue ()))) else va_ttrue ()) (va_pbool_and (va_codegen_success_Fast_add1 ()) (va_pbool_and
    (va_codegen_success_Pop_Secret (va_op_dst_opr64_reg64 rRsi)) (va_pbool_and
    (va_codegen_success_Pop_Secret (va_op_dst_opr64_reg64 rRdi)) (va_ttrue ())))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Fast_add1_stdcall (va_mods:va_mods_t) (win:bool) (dst_b:buffer64) (inA_b:buffer64)
  (inB_in:nat64) : (va_quickCode unit (va_code_Fast_add1_stdcall win)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (dst_in:(va_int_range 0 18446744073709551615)) = va_if win (fun _ -> va_get_reg64 rRcx va_s)
    (fun _ -> va_get_reg64 rRdi va_s) in let (inA_in:(va_int_range 0 18446744073709551615)) = va_if
    win (fun _ -> va_get_reg64 rRdx va_s) (fun _ -> va_get_reg64 rRsi va_s) in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 323 column 16 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Push_Secret (va_op_reg_opr64_reg64 rRdi)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 324 column 16 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Push_Secret (va_op_reg_opr64_reg64 rRsi)) (fun (va_s:va_state) _ -> va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 327 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_qInlineIf va_mods win (qblock va_mods (fun (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 328 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Mov64 (va_op_dst_opr64_reg64 rRdi) (va_op_opr64_reg64 rRcx)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 329 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Mov64 (va_op_dst_opr64_reg64 rRsi) (va_op_opr64_reg64 rRdx)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 330 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Mov64 (va_op_dst_opr64_reg64 rRdx) (va_op_opr64_reg64 rR8)) (va_QEmpty (()))))))
    (qblock va_mods (fun (va_s:va_state) -> va_QEmpty (())))) (fun (va_s:va_state) va_g -> va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 333 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Fast_add1 dst_b inA_b inB_in) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 335 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Pop_Secret (va_op_dst_opr64_reg64 rRsi)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 336 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Pop_Secret (va_op_dst_opr64_reg64 rRdi)) (va_QEmpty (())))))))))



[@"opaque_to_smt"]
let va_lemma_Fast_add1_stdcall va_b0 va_s0 win dst_b inA_b inB_in =
  let (va_mods:va_mods_t) = [va_Mod_stackTaint; va_Mod_stack; va_Mod_mem_layout; va_Mod_mem_heaplet
    0; va_Mod_flags; va_Mod_reg64 rR15; va_Mod_reg64 rR14; va_Mod_reg64 rR13; va_Mod_reg64 rR11;
    va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRsp; va_Mod_reg64 rRbp;
    va_Mod_reg64 rRdi; va_Mod_reg64 rRsi; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx;
    va_Mod_reg64 rRax; va_Mod_ok; va_Mod_mem] in
  let va_qc = va_qcode_Fast_add1_stdcall va_mods win dst_b inA_b inB_in in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Fast_add1_stdcall win) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 257 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_get_ok va_sM) /\ (let (dst_in:(va_int_range 0 18446744073709551615)) = va_if win (fun _ ->
    va_get_reg64 rRcx va_s0) (fun _ -> va_get_reg64 rRdi va_s0) in let (inA_in:(va_int_range 0
    18446744073709551615)) = va_if win (fun _ -> va_get_reg64 rRdx va_s0) (fun _ -> va_get_reg64
    rRsi va_s0) in label va_range1
    "***** POSTCONDITION NOT MET AT line 284 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let a0 = Vale.X64.Decls.buffer64_read inA_b 0 (va_get_mem va_s0) in label va_range1
    "***** POSTCONDITION NOT MET AT line 285 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let a1 = Vale.X64.Decls.buffer64_read inA_b 1 (va_get_mem va_s0) in label va_range1
    "***** POSTCONDITION NOT MET AT line 286 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let a2 = Vale.X64.Decls.buffer64_read inA_b 2 (va_get_mem va_s0) in label va_range1
    "***** POSTCONDITION NOT MET AT line 287 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let a3 = Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem va_s0) in label va_range1
    "***** POSTCONDITION NOT MET AT line 289 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d0 = Vale.X64.Decls.buffer64_read dst_b 0 (va_get_mem va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 290 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d1 = Vale.X64.Decls.buffer64_read dst_b 1 (va_get_mem va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 291 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d2 = Vale.X64.Decls.buffer64_read dst_b 2 (va_get_mem va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 292 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d3 = Vale.X64.Decls.buffer64_read dst_b 3 (va_get_mem va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 294 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let a = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in label va_range1
    "***** POSTCONDITION NOT MET AT line 295 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d = Vale.Curve25519.Fast_defs.pow2_five d0 d1 d2 d3 (va_get_reg64 rRax va_sM) in label
    va_range1
    "***** POSTCONDITION NOT MET AT line 297 column 29 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (d == a + inB_in) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 303 column 46 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (Vale.X64.Decls.modifies_buffer dst_b (va_get_mem va_s0) (va_get_mem va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 306 column 33 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (win ==> va_get_reg64 rRbx va_sM == va_get_reg64 rRbx va_s0) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 307 column 33 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (win ==> va_get_reg64 rRbp va_sM == va_get_reg64 rRbp va_s0) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 308 column 33 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (win ==> va_get_reg64 rRdi va_sM == va_get_reg64 rRdi va_s0) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 309 column 33 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (win ==> va_get_reg64 rRsi va_sM == va_get_reg64 rRsi va_s0) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 310 column 33 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (win ==> va_get_reg64 rRsp va_sM == va_get_reg64 rRsp va_s0) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 311 column 33 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (win ==> va_get_reg64 rR13 va_sM == va_get_reg64 rR13 va_s0) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 312 column 33 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (win ==> va_get_reg64 rR14 va_sM == va_get_reg64 rR14 va_s0) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 313 column 33 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (win ==> va_get_reg64 rR15 va_sM == va_get_reg64 rR15 va_s0) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 314 column 34 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (~win ==> va_get_reg64 rRbx va_sM == va_get_reg64 rRbx va_s0) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 315 column 34 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (~win ==> va_get_reg64 rRbp va_sM == va_get_reg64 rRbp va_s0) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 316 column 34 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (~win ==> va_get_reg64 rR13 va_sM == va_get_reg64 rR13 va_s0) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 317 column 34 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (~win ==> va_get_reg64 rR14 va_sM == va_get_reg64 rR14 va_s0) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 318 column 34 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (~win ==> va_get_reg64 rR15 va_sM == va_get_reg64 rR15 va_s0) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 320 column 24 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_get_reg64 rRsp va_sM == va_get_reg64 rRsp va_s0))))))))))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_stackTaint; va_Mod_stack; va_Mod_mem_layout; va_Mod_mem_heaplet 0;
    va_Mod_flags; va_Mod_reg64 rR15; va_Mod_reg64 rR14; va_Mod_reg64 rR13; va_Mod_reg64 rR11;
    va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRsp; va_Mod_reg64 rRbp;
    va_Mod_reg64 rRdi; va_Mod_reg64 rRsi; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx;
    va_Mod_reg64 rRax; va_Mod_ok; va_Mod_mem]) va_sM va_s0;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Fast_add1_stdcall win dst_b inA_b inB_in va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Fast_add1_stdcall (va_code_Fast_add1_stdcall win) va_s0 win dst_b
    inA_b inB_in in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_stackTaint va_sM (va_update_stack va_sM
    (va_update_mem_layout va_sM (va_update_mem_heaplet 0 va_sM (va_update_flags va_sM
    (va_update_reg64 rR15 va_sM (va_update_reg64 rR14 va_sM (va_update_reg64 rR13 va_sM
    (va_update_reg64 rR11 va_sM (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM
    (va_update_reg64 rR8 va_sM (va_update_reg64 rRsp va_sM (va_update_reg64 rRbp va_sM
    (va_update_reg64 rRdi va_sM (va_update_reg64 rRsi va_sM (va_update_reg64 rRdx va_sM
    (va_update_reg64 rRcx va_sM (va_update_reg64 rRbx va_sM (va_update_reg64 rRax va_sM
    (va_update_ok va_sM (va_update_mem va_sM va_s0)))))))))))))))))))))));
  va_lemma_norm_mods ([va_Mod_stackTaint; va_Mod_stack; va_Mod_mem_layout; va_Mod_mem_heaplet 0;
    va_Mod_flags; va_Mod_reg64 rR15; va_Mod_reg64 rR14; va_Mod_reg64 rR13; va_Mod_reg64 rR11;
    va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRsp; va_Mod_reg64 rRbp;
    va_Mod_reg64 rRdi; va_Mod_reg64 rRsi; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx;
    va_Mod_reg64 rRax; va_Mod_mem]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

#pop-options
//--
//-- Fast_sub1
#push-options "--z3rlimit 1200"

val va_code_Fast_sub1 : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Fast_sub1 () =
  (va_Block (va_CCons (va_code_Xor64 (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRax))
    (va_CCons (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR8)
    (va_op_reg_opr64_reg64 rRsi) 0 Secret) (va_CCons (va_code_Sub64Wrap (va_op_dst_opr64_reg64 rR8)
    (va_op_opr64_reg64 rRcx)) (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_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR9)
    (va_op_reg_opr64_reg64 rRsi) 8 Secret) (va_CCons (va_code_Sbb64 (va_op_dst_opr64_reg64 rR9)
    (va_const_opr64 0)) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR9) 8 Secret) (va_CCons
    (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR10)
    (va_op_reg_opr64_reg64 rRsi) 16 Secret) (va_CCons (va_code_Sbb64 (va_op_dst_opr64_reg64 rR10)
    (va_const_opr64 0)) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR10) 16 Secret) (va_CCons
    (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR11)
    (va_op_reg_opr64_reg64 rRsi) 24 Secret) (va_CCons (va_code_Sbb64 (va_op_dst_opr64_reg64 rR11)
    (va_const_opr64 0)) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR11) 24 Secret) (va_CCons
    (va_code_Adc64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRax)) (va_CNil
    ()))))))))))))))))

val va_codegen_success_Fast_sub1 : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Fast_sub1 () =
  (va_pbool_and (va_codegen_success_Xor64 (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRax))
    (va_pbool_and (va_codegen_success_Load64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_dst_opr64_reg64 rR8) (va_op_reg_opr64_reg64 rRsi) 0 Secret) (va_pbool_and
    (va_codegen_success_Sub64Wrap (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rRcx))
    (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_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR9)
    (va_op_reg_opr64_reg64 rRsi) 8 Secret) (va_pbool_and (va_codegen_success_Sbb64
    (va_op_dst_opr64_reg64 rR9) (va_const_opr64 0)) (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 rR9) 8 Secret) (va_pbool_and (va_codegen_success_Load64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR10) (va_op_reg_opr64_reg64 rRsi) 16
    Secret) (va_pbool_and (va_codegen_success_Sbb64 (va_op_dst_opr64_reg64 rR10) (va_const_opr64
    0)) (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR10) 16 Secret) (va_pbool_and
    (va_codegen_success_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR11)
    (va_op_reg_opr64_reg64 rRsi) 24 Secret) (va_pbool_and (va_codegen_success_Sbb64
    (va_op_dst_opr64_reg64 rR11) (va_const_opr64 0)) (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 rR11) 24 Secret) (va_pbool_and (va_codegen_success_Adc64Wrap
    (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRax)) (va_ttrue ())))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Fast_sub1 (va_mods:va_mods_t) (dst_b:buffer64) (inA_b:buffer64) : (va_quickCode unit
  (va_code_Fast_sub1 ())) =
  (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 378 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 379 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 rRax) (va_op_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 381 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR8)
    (va_op_reg_opr64_reg64 rRsi) 0 Secret inA_b 0) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 382 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Sub64Wrap (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rRcx)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 383 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 385 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR9)
    (va_op_reg_opr64_reg64 rRsi) 8 Secret inA_b 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 386 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Sbb64 (va_op_dst_opr64_reg64 rR9) (va_const_opr64 0)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 387 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 rR9) 8 Secret dst_b 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 389 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR10)
    (va_op_reg_opr64_reg64 rRsi) 16 Secret inA_b 2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 390 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Sbb64 (va_op_dst_opr64_reg64 rR10) (va_const_opr64 0)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 391 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) 16 Secret dst_b 2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 393 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR11)
    (va_op_reg_opr64_reg64 rRsi) 24 Secret inA_b 3) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 394 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Sbb64 (va_op_dst_opr64_reg64 rR11) (va_const_opr64 0)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 395 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 rR11) 24 Secret dst_b 3) (fun (va_s:va_state) _ -> let (c:bool) =
    Vale.X64.Decls.cf (va_get_flags va_s) in va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 398 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Adc64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRax)) (fun (va_s:va_state)
    _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 399 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_get_reg64 rRax va_s == Vale.Curve25519.Fast_defs.bool_bit c) (va_QEmpty
    (())))))))))))))))))))


val va_lemma_Fast_sub1 : va_b0:va_code -> va_s0:va_state -> dst_b:buffer64 -> inA_b:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Fast_sub1 ()) va_s0 /\ va_get_ok va_s0 /\ (let
    (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0 (va_get_mem_heaplet 0 va_s0)
    in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 1 (va_get_mem_heaplet 0
    va_s0) in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 2
    (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 3 (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four
    a0 a1 a2 a3 in (Vale.X64.Decls.buffers_disjoint dst_b inA_b \/ dst_b == inA_b) /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) dst_b 4
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) inA_b 4 (va_get_mem_layout va_s0) Secret)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0 (va_get_mem_heaplet 0
    va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 1
    (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 2 (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in let d0 = Vale.X64.Decls.buffer64_read dst_b
    0 (va_get_mem_heaplet 0 va_sM) in let d1 = Vale.X64.Decls.buffer64_read dst_b 1
    (va_get_mem_heaplet 0 va_sM) in let d2 = Vale.X64.Decls.buffer64_read dst_b 2
    (va_get_mem_heaplet 0 va_sM) in let d3 = Vale.X64.Decls.buffer64_read dst_b 3
    (va_get_mem_heaplet 0 va_sM) in let d = Vale.Curve25519.Fast_defs.pow2_four d0 d1 d2 d3 in d -
    va_mul_nat (va_get_reg64 rRax va_sM) pow2_256 == a - va_get_reg64 rRcx va_s0 /\ (va_get_reg64
    rRax va_sM == 0 \/ va_get_reg64 rRax va_sM == 1) /\ Vale.X64.Decls.validSrcAddrs64
    (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b 4 (va_get_mem_layout va_sM) Secret
    /\ Vale.X64.Decls.modifies_buffer dst_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet 0
    va_sM)) /\ va_state_eq va_sM (va_update_flags va_sM (va_update_mem_heaplet 0 va_sM
    (va_update_reg64 rR11 va_sM (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM
    (va_update_reg64 rR8 va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem va_sM
    va_s0)))))))))))
[@"opaque_to_smt"]
let va_lemma_Fast_sub1 va_b0 va_s0 dst_b inA_b =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR11; va_Mod_reg64
    rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRax; va_Mod_ok; va_Mod_mem] in
  let va_qc = va_qcode_Fast_sub1 va_mods dst_b inA_b in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Fast_sub1 ()) va_qc va_s0 (fun va_s0
    va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 339 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_get_ok va_sM) /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 1 (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b 2 (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem_heaplet 0 va_s0)
    in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in label va_range1
    "***** POSTCONDITION NOT MET AT line 367 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d0 = Vale.X64.Decls.buffer64_read dst_b 0 (va_get_mem_heaplet 0 va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 368 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d1 = Vale.X64.Decls.buffer64_read dst_b 1 (va_get_mem_heaplet 0 va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 369 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d2 = Vale.X64.Decls.buffer64_read dst_b 2 (va_get_mem_heaplet 0 va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 370 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d3 = Vale.X64.Decls.buffer64_read dst_b 3 (va_get_mem_heaplet 0 va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 371 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d = Vale.Curve25519.Fast_defs.pow2_four d0 d1 d2 d3 in label va_range1
    "***** POSTCONDITION NOT MET AT line 372 column 41 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (d - va_mul_nat (va_get_reg64 rRax va_sM) pow2_256 == a - va_get_reg64 rRcx va_s0) /\ label
    va_range1
    "***** POSTCONDITION NOT MET AT line 373 column 29 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_get_reg64 rRax va_sM == 0 \/ va_get_reg64 rRax va_sM == 1) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 375 column 69 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b 4
    (va_get_mem_layout va_sM) Secret) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 376 column 50 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (Vale.X64.Decls.modifies_buffer dst_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet 0
    va_sM))))))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR11; va_Mod_reg64 rR10;
    va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRax; va_Mod_ok; va_Mod_mem]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Fast_sub1 (dst_b:buffer64) (inA_b:buffer64) (va_s0:va_state) (va_k:(va_state -> unit ->
  Type0)) : Type0 =
  (va_get_ok va_s0 /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 1 (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b 2 (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem_heaplet 0 va_s0)
    in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in
    (Vale.X64.Decls.buffers_disjoint dst_b inA_b \/ dst_b == inA_b) /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) dst_b 4
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) inA_b 4 (va_get_mem_layout va_s0) Secret) /\ (forall
    (va_x_mem:vale_heap) (va_x_rax:nat64) (va_x_r8:nat64) (va_x_r9:nat64) (va_x_r10:nat64)
    (va_x_r11:nat64) (va_x_heap0:vale_heap) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags
    va_x_efl (va_upd_mem_heaplet 0 va_x_heap0 (va_upd_reg64 rR11 va_x_r11 (va_upd_reg64 rR10
    va_x_r10 (va_upd_reg64 rR9 va_x_r9 (va_upd_reg64 rR8 va_x_r8 (va_upd_reg64 rRax va_x_rax
    (va_upd_mem va_x_mem va_s0))))))) in va_get_ok va_sM /\ (let (a0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b 0 (va_get_mem_heaplet 0 va_s0) in let
    (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 1 (va_get_mem_heaplet 0 va_s0)
    in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 2 (va_get_mem_heaplet 0
    va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 3
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in let d0 = Vale.X64.Decls.buffer64_read dst_b 0 (va_get_mem_heaplet 0 va_sM) in let d1 =
    Vale.X64.Decls.buffer64_read dst_b 1 (va_get_mem_heaplet 0 va_sM) in let d2 =
    Vale.X64.Decls.buffer64_read dst_b 2 (va_get_mem_heaplet 0 va_sM) in let d3 =
    Vale.X64.Decls.buffer64_read dst_b 3 (va_get_mem_heaplet 0 va_sM) in let d =
    Vale.Curve25519.Fast_defs.pow2_four d0 d1 d2 d3 in d - va_mul_nat (va_get_reg64 rRax va_sM)
    pow2_256 == a - va_get_reg64 rRcx va_s0 /\ (va_get_reg64 rRax va_sM == 0 \/ va_get_reg64 rRax
    va_sM == 1) /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi
    va_sM) dst_b 4 (va_get_mem_layout va_sM) Secret /\ Vale.X64.Decls.modifies_buffer dst_b
    (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet 0 va_sM)) ==> va_k va_sM (())))


val va_wpProof_Fast_sub1 : dst_b:buffer64 -> inA_b:buffer64 -> va_s0:va_state -> va_k:(va_state ->
  unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Fast_sub1 dst_b inA_b va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Fast_sub1 ()) ([va_Mod_flags;
    va_Mod_mem_heaplet 0; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8;
    va_Mod_reg64 rRax; va_Mod_mem]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Fast_sub1 dst_b inA_b va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Fast_sub1 (va_code_Fast_sub1 ()) va_s0 dst_b inA_b in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_mem_heaplet 0 va_sM (va_update_reg64
    rR11 va_sM (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM (va_update_reg64 rR8 va_sM
    (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem va_sM va_s0))))))))));
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR11; va_Mod_reg64 rR10;
    va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRax; va_Mod_mem]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Fast_sub1 (dst_b:buffer64) (inA_b:buffer64) : (va_quickCode unit (va_code_Fast_sub1
  ())) =
  (va_QProc (va_code_Fast_sub1 ()) ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR11;
    va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRax; va_Mod_mem])
    (va_wp_Fast_sub1 dst_b inA_b) (va_wpProof_Fast_sub1 dst_b inA_b))
#pop-options
//--
//-- Fast_add
#push-options "--z3rlimit 600"

val va_code_Fast_add : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Fast_add () =
  (va_Block (va_CCons (va_code_Xor64 (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rR8)) (va_CCons
    (va_code_Xor64 (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRax)) (va_CCons
    (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR9)
    (va_op_reg_opr64_reg64 rRcx) 0 Secret) (va_CCons (va_code_Mem64_lemma ()) (va_CCons
    (va_code_Add64Wrap (va_op_dst_opr64_reg64 rR9) (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 rR9) 0
    Secret) (va_CCons (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64
    rR10) (va_op_reg_opr64_reg64 rRcx) 8 Secret) (va_CCons (va_code_Mem64_lemma ()) (va_CCons
    (va_code_Adcx64Wrap (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_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_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64
    rR11) (va_op_reg_opr64_reg64 rRcx) 16 Secret) (va_CCons (va_code_Mem64_lemma ()) (va_CCons
    (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rR11) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet
    0) (va_op_reg64_reg64 rRsi) 16 Secret)) (va_CCons (va_code_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR11) 16
    Secret) (va_CCons (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64
    rRbx) (va_op_reg_opr64_reg64 rRcx) 24 Secret) (va_CCons (va_code_Mem64_lemma ()) (va_CCons
    (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rRbx) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet
    0) (va_op_reg64_reg64 rRsi) 24 Secret)) (va_CCons (va_code_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rRbx) 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_add : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Fast_add () =
  (va_pbool_and (va_codegen_success_Xor64 (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rR8))
    (va_pbool_and (va_codegen_success_Xor64 (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRax))
    (va_pbool_and (va_codegen_success_Load64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_dst_opr64_reg64 rR9) (va_op_reg_opr64_reg64 rRcx) 0 Secret) (va_pbool_and
    (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Add64Wrap
    (va_op_dst_opr64_reg64 rR9) (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 rR9) 0 Secret) (va_pbool_and
    (va_codegen_success_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR10)
    (va_op_reg_opr64_reg64 rRcx) 8 Secret) (va_pbool_and (va_codegen_success_Mem64_lemma ())
    (va_pbool_and (va_codegen_success_Adcx64Wrap (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_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_Load64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR11) (va_op_reg_opr64_reg64 rRcx) 16
    Secret) (va_pbool_and (va_codegen_success_Mem64_lemma ()) (va_pbool_and
    (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rR11) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 16 Secret)) (va_pbool_and
    (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR11) 16 Secret) (va_pbool_and (va_codegen_success_Load64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRbx) (va_op_reg_opr64_reg64 rRcx) 24
    Secret) (va_pbool_and (va_codegen_success_Mem64_lemma ()) (va_pbool_and
    (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rRbx) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 24 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 rRbx) 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_add (va_mods:va_mods_t) (dst_b:buffer64) (inA_b:buffer64) (inB_b:buffer64) :
  (va_quickCode unit (va_code_Fast_add ())) =
  (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 (b0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b 0 (va_get_mem_heaplet 0 va_s) in let
    (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 1 (va_get_mem_heaplet 0 va_s)
    in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 2 (va_get_mem_heaplet 0
    va_s) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_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 let (b:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four b0 b1 b2 b3 in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 521 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 522 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 523 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 rRax) (va_op_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 525 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR9)
    (va_op_reg_opr64_reg64 rRcx) 0 Secret inB_b 0) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 526 column 25 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_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 526 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 rR9) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet
    0) (va_op_reg64_reg64 rRsi) 0 Secret)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 527 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 rR9) 0 Secret dst_b 0) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 529 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR10)
    (va_op_reg_opr64_reg64 rRcx) 8 Secret inB_b 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 530 column 27 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_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 530 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 rR10) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet
    0) (va_op_reg64_reg64 rRsi) 8 Secret)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 531 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 533 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR11)
    (va_op_reg_opr64_reg64 rRcx) 16 Secret inB_b 2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 534 column 27 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_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 534 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 rR11) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet
    0) (va_op_reg64_reg64 rRsi) 16 Secret)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 535 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 rR11) 16 Secret dst_b 2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 537 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRbx)
    (va_op_reg_opr64_reg64 rRcx) 24 Secret inB_b 3) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 538 column 27 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_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 538 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_opr_code_Mem64 (va_op_heaplet_mem_heaplet
    0) (va_op_reg64_reg64 rRsi) 24 Secret)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 539 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) 24 Secret dst_b 3) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 541 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)) (va_QEmpty
    (())))))))))))))))))))))))


val va_lemma_Fast_add : va_b0:va_code -> va_s0:va_state -> dst_b:buffer64 -> inA_b:buffer64 ->
  inB_b:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Fast_add ()) va_s0 /\ va_get_ok va_s0 /\ (let
    (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0 (va_get_mem_heaplet 0 va_s0)
    in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 1 (va_get_mem_heaplet 0
    va_s0) in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 2
    (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 3 (va_get_mem_heaplet 0 va_s0) in let (b0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b 0 (va_get_mem_heaplet 0 va_s0) in let
    (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 1 (va_get_mem_heaplet 0 va_s0)
    in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 2 (va_get_mem_heaplet 0
    va_s0) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 3
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in let (b:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four b0 b1 b2 b3 in adx_enabled /\
    bmi2_enabled /\ (Vale.X64.Decls.buffers_disjoint dst_b inA_b \/ dst_b == inA_b) /\
    (Vale.X64.Decls.buffers_disjoint dst_b inB_b \/ dst_b == inB_b) /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) dst_b 4
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) inA_b 4 (va_get_mem_layout va_s0) Secret /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRcx va_s0) inB_b 4
    (va_get_mem_layout va_s0) Secret)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0 (va_get_mem_heaplet 0
    va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 1
    (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 2 (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem_heaplet 0 va_s0) in let
    (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 0 (va_get_mem_heaplet 0 va_s0)
    in let (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 1 (va_get_mem_heaplet 0
    va_s0) in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 2
    (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b 3 (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four
    a0 a1 a2 a3 in let (b:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four b0 b1 b2 b3 in let d0 =
    Vale.X64.Decls.buffer64_read dst_b 0 (va_get_mem_heaplet 0 va_sM) in let d1 =
    Vale.X64.Decls.buffer64_read dst_b 1 (va_get_mem_heaplet 0 va_sM) in let d2 =
    Vale.X64.Decls.buffer64_read dst_b 2 (va_get_mem_heaplet 0 va_sM) in let d3 =
    Vale.X64.Decls.buffer64_read dst_b 3 (va_get_mem_heaplet 0 va_sM) in let d =
    Vale.Curve25519.Fast_defs.pow2_five d0 d1 d2 d3 (va_get_reg64 rRax va_sM) in d == a + b /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b 4
    (va_get_mem_layout va_sM) Secret /\ Vale.X64.Decls.modifies_buffer dst_b (va_get_mem_heaplet 0
    va_s0) (va_get_mem_heaplet 0 va_sM)) /\ va_state_eq va_sM (va_update_flags va_sM
    (va_update_mem_heaplet 0 va_sM (va_update_reg64 rRbx va_sM (va_update_reg64 rR11 va_sM
    (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM (va_update_reg64 rR8 va_sM
    (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem va_sM va_s0))))))))))))
[@"opaque_to_smt"]
let va_lemma_Fast_add va_b0 va_s0 dst_b inA_b inB_b =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rRbx; va_Mod_reg64
    rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRax; va_Mod_ok;
    va_Mod_mem] in
  let va_qc = va_qcode_Fast_add va_mods dst_b inA_b inB_b in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Fast_add ()) va_qc va_s0 (fun va_s0
    va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 474 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_get_ok va_sM) /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 1 (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b 2 (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem_heaplet 0 va_s0)
    in let (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 0 (va_get_mem_heaplet 0
    va_s0) in let (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 1
    (va_get_mem_heaplet 0 va_s0) in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b 2 (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b 3 (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in let (b:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four b0 b1 b2 b3 in label va_range1
    "***** POSTCONDITION NOT MET AT line 511 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d0 = Vale.X64.Decls.buffer64_read dst_b 0 (va_get_mem_heaplet 0 va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 512 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d1 = Vale.X64.Decls.buffer64_read dst_b 1 (va_get_mem_heaplet 0 va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 513 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d2 = Vale.X64.Decls.buffer64_read dst_b 2 (va_get_mem_heaplet 0 va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 514 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d3 = Vale.X64.Decls.buffer64_read dst_b 3 (va_get_mem_heaplet 0 va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 515 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d = Vale.Curve25519.Fast_defs.pow2_five d0 d1 d2 d3 (va_get_reg64 rRax va_sM) in label
    va_range1
    "***** POSTCONDITION NOT MET AT line 516 column 24 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (d == a + b) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 518 column 69 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b 4
    (va_get_mem_layout va_sM) Secret) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 519 column 50 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (Vale.X64.Decls.modifies_buffer dst_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet 0
    va_sM))))))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rRbx; va_Mod_reg64 rR11;
    va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRax; va_Mod_ok;
    va_Mod_mem]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Fast_add (dst_b:buffer64) (inA_b:buffer64) (inB_b:buffer64) (va_s0:va_state)
  (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 1 (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b 2 (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem_heaplet 0 va_s0)
    in let (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 0 (va_get_mem_heaplet 0
    va_s0) in let (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 1
    (va_get_mem_heaplet 0 va_s0) in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b 2 (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b 3 (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in let (b:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four b0 b1 b2 b3 in adx_enabled /\ bmi2_enabled /\
    (Vale.X64.Decls.buffers_disjoint dst_b inA_b \/ dst_b == inA_b) /\
    (Vale.X64.Decls.buffers_disjoint dst_b inB_b \/ dst_b == inB_b) /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) dst_b 4
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) inA_b 4 (va_get_mem_layout va_s0) Secret /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRcx va_s0) inB_b 4
    (va_get_mem_layout va_s0) Secret) /\ (forall (va_x_mem:vale_heap) (va_x_rax:nat64)
    (va_x_r8:nat64) (va_x_r9:nat64) (va_x_r10:nat64) (va_x_r11:nat64) (va_x_rbx:nat64)
    (va_x_heap0:vale_heap) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl
    (va_upd_mem_heaplet 0 va_x_heap0 (va_upd_reg64 rRbx va_x_rbx (va_upd_reg64 rR11 va_x_r11
    (va_upd_reg64 rR10 va_x_r10 (va_upd_reg64 rR9 va_x_r9 (va_upd_reg64 rR8 va_x_r8 (va_upd_reg64
    rRax va_x_rax (va_upd_mem va_x_mem va_s0)))))))) in va_get_ok va_sM /\ (let
    (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0 (va_get_mem_heaplet 0 va_s0)
    in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 1 (va_get_mem_heaplet 0
    va_s0) in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 2
    (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 3 (va_get_mem_heaplet 0 va_s0) in let (b0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b 0 (va_get_mem_heaplet 0 va_s0) in let
    (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 1 (va_get_mem_heaplet 0 va_s0)
    in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 2 (va_get_mem_heaplet 0
    va_s0) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 3
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in let (b:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four b0 b1 b2 b3 in let d0 =
    Vale.X64.Decls.buffer64_read dst_b 0 (va_get_mem_heaplet 0 va_sM) in let d1 =
    Vale.X64.Decls.buffer64_read dst_b 1 (va_get_mem_heaplet 0 va_sM) in let d2 =
    Vale.X64.Decls.buffer64_read dst_b 2 (va_get_mem_heaplet 0 va_sM) in let d3 =
    Vale.X64.Decls.buffer64_read dst_b 3 (va_get_mem_heaplet 0 va_sM) in let d =
    Vale.Curve25519.Fast_defs.pow2_five d0 d1 d2 d3 (va_get_reg64 rRax va_sM) in d == a + b /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b 4
    (va_get_mem_layout va_sM) Secret /\ Vale.X64.Decls.modifies_buffer dst_b (va_get_mem_heaplet 0
    va_s0) (va_get_mem_heaplet 0 va_sM)) ==> va_k va_sM (())))


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

[@ "opaque_to_smt" va_qattr]
let va_quick_Fast_add (dst_b:buffer64) (inA_b:buffer64) (inB_b:buffer64) : (va_quickCode unit
  (va_code_Fast_add ())) =
  (va_QProc (va_code_Fast_add ()) ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rRbx;
    va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRax;
    va_Mod_mem]) (va_wp_Fast_add dst_b inA_b inB_b) (va_wpProof_Fast_add dst_b inA_b inB_b))
#pop-options
//--
//-- Fast_sub
#push-options "--z3rlimit 600"

val va_code_Fast_sub : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Fast_sub () =
  (va_Block (va_CCons (va_code_Xor64 (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRax))
    (va_CCons (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR8)
    (va_op_reg_opr64_reg64 rRsi) 0 Secret) (va_CCons (va_code_Mem64_lemma ()) (va_CCons
    (va_code_Sub64Wrap (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) 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_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64
    rR9) (va_op_reg_opr64_reg64 rRsi) 8 Secret) (va_CCons (va_code_Mem64_lemma ()) (va_CCons
    (va_code_Sbb64 (va_op_dst_opr64_reg64 rR9) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) 8 Secret)) (va_CCons (va_code_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR9) 8
    Secret) (va_CCons (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64
    rR10) (va_op_reg_opr64_reg64 rRsi) 16 Secret) (va_CCons (va_code_Mem64_lemma ()) (va_CCons
    (va_code_Sbb64 (va_op_dst_opr64_reg64 rR10) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) 16 Secret)) (va_CCons (va_code_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR10) 16
    Secret) (va_CCons (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64
    rR11) (va_op_reg_opr64_reg64 rRsi) 24 Secret) (va_CCons (va_code_Mem64_lemma ()) (va_CCons
    (va_code_Sbb64 (va_op_dst_opr64_reg64 rR11) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) 24 Secret)) (va_CCons (va_code_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR11) 24
    Secret) (va_CCons (va_code_Adc64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRax))
    (va_CNil ()))))))))))))))))))))

val va_codegen_success_Fast_sub : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Fast_sub () =
  (va_pbool_and (va_codegen_success_Xor64 (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRax))
    (va_pbool_and (va_codegen_success_Load64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_dst_opr64_reg64 rR8) (va_op_reg_opr64_reg64 rRsi) 0 Secret) (va_pbool_and
    (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Sub64Wrap
    (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64
    rRcx) 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_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR9)
    (va_op_reg_opr64_reg64 rRsi) 8 Secret) (va_pbool_and (va_codegen_success_Mem64_lemma ())
    (va_pbool_and (va_codegen_success_Sbb64 (va_op_dst_opr64_reg64 rR9) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) 8 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 rR9) 8 Secret) (va_pbool_and (va_codegen_success_Load64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR10) (va_op_reg_opr64_reg64 rRsi) 16
    Secret) (va_pbool_and (va_codegen_success_Mem64_lemma ()) (va_pbool_and
    (va_codegen_success_Sbb64 (va_op_dst_opr64_reg64 rR10) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) 16 Secret)) (va_pbool_and
    (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR10) 16 Secret) (va_pbool_and (va_codegen_success_Load64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR11) (va_op_reg_opr64_reg64 rRsi) 24
    Secret) (va_pbool_and (va_codegen_success_Mem64_lemma ()) (va_pbool_and
    (va_codegen_success_Sbb64 (va_op_dst_opr64_reg64 rR11) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) 24 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 rR11) 24 Secret) (va_pbool_and (va_codegen_success_Adc64Wrap
    (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRax)) (va_ttrue ())))))))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Fast_sub (va_mods:va_mods_t) (dst_b:buffer64) (inA_b:buffer64) (inB_b:buffer64) :
  (va_quickCode unit (va_code_Fast_sub ())) =
  (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 (b0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b 0 (va_get_mem_heaplet 0 va_s) in let
    (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 1 (va_get_mem_heaplet 0 va_s)
    in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 2 (va_get_mem_heaplet 0
    va_s) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_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 let (b:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four b0 b1 b2 b3 in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 674 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 677 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 rRax) (va_op_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 679 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR8)
    (va_op_reg_opr64_reg64 rRsi) 0 Secret inA_b 0) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 680 column 25 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 rRcx) 0 inB_b 0 Secret)
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 680 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Sub64Wrap (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet
    0) (va_op_reg64_reg64 rRcx) 0 Secret)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 681 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 685 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR9)
    (va_op_reg_opr64_reg64 rRsi) 8 Secret inA_b 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 686 column 21 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 rRcx) 8 inB_b 1 Secret)
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 686 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Sbb64 (va_op_dst_opr64_reg64 rR9) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) 8 Secret)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 687 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 rR9) 8 Secret dst_b 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 691 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR10)
    (va_op_reg_opr64_reg64 rRsi) 16 Secret inA_b 2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 692 column 22 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 rRcx) 16 inB_b 2 Secret)
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 692 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Sbb64 (va_op_dst_opr64_reg64 rR10) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) 16 Secret)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 694 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) 16 Secret dst_b 2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 696 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR11)
    (va_op_reg_opr64_reg64 rRsi) 24 Secret inA_b 3) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 697 column 22 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 rRcx) 24 inB_b 3 Secret)
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 697 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Sbb64 (va_op_dst_opr64_reg64 rR11) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) 24 Secret)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 698 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 rR11) 24 Secret dst_b 3) (fun (va_s:va_state) _ -> let (c:bool) =
    Vale.X64.Decls.cf (va_get_flags va_s) in va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 701 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Adc64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRax)) (fun (va_s:va_state)
    _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 702 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_get_reg64 rRax va_s == Vale.Curve25519.Fast_defs.bool_bit c) (let
    (va_arg41:Vale.Curve25519.Fast_defs.bit) = Vale.Curve25519.Fast_defs.bool_bit c in let
    (va_arg40:Vale.Def.Types_s.nat64) = va_get_reg64 rR11 va_s in let
    (va_arg39:Vale.Def.Types_s.nat64) = va_get_reg64 rR10 va_s in let
    (va_arg38:Vale.Def.Types_s.nat64) = va_get_reg64 rR9 va_s in let
    (va_arg37:Vale.Def.Types_s.nat64) = va_get_reg64 rR8 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 704 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.FastUtil_helpers.lemma_sub a a0 a1 a2 a3 b b0 b1 b2 b3
    va_arg37 va_arg38 va_arg39 va_arg40 va_arg41) (va_QEmpty (()))))))))))))))))))))))))


val va_lemma_Fast_sub : va_b0:va_code -> va_s0:va_state -> dst_b:buffer64 -> inA_b:buffer64 ->
  inB_b:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Fast_sub ()) va_s0 /\ va_get_ok va_s0 /\ (let
    (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0 (va_get_mem_heaplet 0 va_s0)
    in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 1 (va_get_mem_heaplet 0
    va_s0) in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 2
    (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 3 (va_get_mem_heaplet 0 va_s0) in let (b0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b 0 (va_get_mem_heaplet 0 va_s0) in let
    (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 1 (va_get_mem_heaplet 0 va_s0)
    in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 2 (va_get_mem_heaplet 0
    va_s0) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 3
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in let (b:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four b0 b1 b2 b3 in
    (Vale.X64.Decls.buffers_disjoint dst_b inA_b \/ dst_b == inA_b) /\
    (Vale.X64.Decls.buffers_disjoint dst_b inB_b \/ dst_b == inB_b) /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) dst_b 4
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) inA_b 4 (va_get_mem_layout va_s0) Secret /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRcx va_s0) inB_b 4
    (va_get_mem_layout va_s0) Secret)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0 (va_get_mem_heaplet 0
    va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 1
    (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 2 (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem_heaplet 0 va_s0) in let
    (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 0 (va_get_mem_heaplet 0 va_s0)
    in let (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 1 (va_get_mem_heaplet 0
    va_s0) in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 2
    (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b 3 (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four
    a0 a1 a2 a3 in let (b:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four b0 b1 b2 b3 in let d0 =
    Vale.X64.Decls.buffer64_read dst_b 0 (va_get_mem_heaplet 0 va_sM) in let d1 =
    Vale.X64.Decls.buffer64_read dst_b 1 (va_get_mem_heaplet 0 va_sM) in let d2 =
    Vale.X64.Decls.buffer64_read dst_b 2 (va_get_mem_heaplet 0 va_sM) in let d3 =
    Vale.X64.Decls.buffer64_read dst_b 3 (va_get_mem_heaplet 0 va_sM) in let d =
    Vale.Curve25519.Fast_defs.pow2_four d0 d1 d2 d3 in d - va_mul_nat (va_get_reg64 rRax va_sM)
    pow2_256 == a - b /\ (va_get_reg64 rRax va_sM == 0 \/ va_get_reg64 rRax va_sM == 1) /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b 4
    (va_get_mem_layout va_sM) Secret /\ Vale.X64.Decls.modifies_buffer dst_b (va_get_mem_heaplet 0
    va_s0) (va_get_mem_heaplet 0 va_sM)) /\ va_state_eq va_sM (va_update_flags va_sM
    (va_update_mem_heaplet 0 va_sM (va_update_reg64 rR11 va_sM (va_update_reg64 rR10 va_sM
    (va_update_reg64 rR9 va_sM (va_update_reg64 rR8 va_sM (va_update_reg64 rRax va_sM (va_update_ok
    va_sM (va_update_mem va_sM va_s0)))))))))))
[@"opaque_to_smt"]
let va_lemma_Fast_sub va_b0 va_s0 dst_b inA_b inB_b =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR11; va_Mod_reg64
    rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRax; va_Mod_ok; va_Mod_mem] in
  let va_qc = va_qcode_Fast_sub va_mods dst_b inA_b inB_b in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Fast_sub ()) va_qc va_s0 (fun va_s0
    va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 627 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_get_ok va_sM) /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 1 (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b 2 (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem_heaplet 0 va_s0)
    in let (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 0 (va_get_mem_heaplet 0
    va_s0) in let (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 1
    (va_get_mem_heaplet 0 va_s0) in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b 2 (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b 3 (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in let (b:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four b0 b1 b2 b3 in label va_range1
    "***** POSTCONDITION NOT MET AT line 663 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d0 = Vale.X64.Decls.buffer64_read dst_b 0 (va_get_mem_heaplet 0 va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 664 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d1 = Vale.X64.Decls.buffer64_read dst_b 1 (va_get_mem_heaplet 0 va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 665 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d2 = Vale.X64.Decls.buffer64_read dst_b 2 (va_get_mem_heaplet 0 va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 666 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d3 = Vale.X64.Decls.buffer64_read dst_b 3 (va_get_mem_heaplet 0 va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 667 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let d = Vale.Curve25519.Fast_defs.pow2_four d0 d1 d2 d3 in label va_range1
    "***** POSTCONDITION NOT MET AT line 668 column 41 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (d - va_mul_nat (va_get_reg64 rRax va_sM) pow2_256 == a - b) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 669 column 29 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_get_reg64 rRax va_sM == 0 \/ va_get_reg64 rRax va_sM == 1) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 671 column 69 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b 4
    (va_get_mem_layout va_sM) Secret) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 672 column 50 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (Vale.X64.Decls.modifies_buffer dst_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet 0
    va_sM))))))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR11; va_Mod_reg64 rR10;
    va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRax; va_Mod_ok; va_Mod_mem]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Fast_sub (dst_b:buffer64) (inA_b:buffer64) (inB_b:buffer64) (va_s0:va_state)
  (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 1 (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b 2 (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem_heaplet 0 va_s0)
    in let (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 0 (va_get_mem_heaplet 0
    va_s0) in let (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 1
    (va_get_mem_heaplet 0 va_s0) in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b 2 (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b 3 (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in let (b:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four b0 b1 b2 b3 in (Vale.X64.Decls.buffers_disjoint dst_b inA_b
    \/ dst_b == inA_b) /\ (Vale.X64.Decls.buffers_disjoint dst_b inB_b \/ dst_b == inB_b) /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) dst_b 4
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) inA_b 4 (va_get_mem_layout va_s0) Secret /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRcx va_s0) inB_b 4
    (va_get_mem_layout va_s0) Secret) /\ (forall (va_x_mem:vale_heap) (va_x_rax:nat64)
    (va_x_r8:nat64) (va_x_r9:nat64) (va_x_r10:nat64) (va_x_r11:nat64) (va_x_heap0:vale_heap)
    (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_mem_heaplet 0
    va_x_heap0 (va_upd_reg64 rR11 va_x_r11 (va_upd_reg64 rR10 va_x_r10 (va_upd_reg64 rR9 va_x_r9
    (va_upd_reg64 rR8 va_x_r8 (va_upd_reg64 rRax va_x_rax (va_upd_mem va_x_mem va_s0))))))) in
    va_get_ok va_sM /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b 1 (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b 2 (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem_heaplet 0 va_s0)
    in let (b0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 0 (va_get_mem_heaplet 0
    va_s0) in let (b1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inB_b 1
    (va_get_mem_heaplet 0 va_s0) in let (b2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inB_b 2 (va_get_mem_heaplet 0 va_s0) in let (b3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inB_b 3 (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in let (b:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four b0 b1 b2 b3 in let d0 = Vale.X64.Decls.buffer64_read dst_b
    0 (va_get_mem_heaplet 0 va_sM) in let d1 = Vale.X64.Decls.buffer64_read dst_b 1
    (va_get_mem_heaplet 0 va_sM) in let d2 = Vale.X64.Decls.buffer64_read dst_b 2
    (va_get_mem_heaplet 0 va_sM) in let d3 = Vale.X64.Decls.buffer64_read dst_b 3
    (va_get_mem_heaplet 0 va_sM) in let d = Vale.Curve25519.Fast_defs.pow2_four d0 d1 d2 d3 in d -
    va_mul_nat (va_get_reg64 rRax va_sM) pow2_256 == a - b /\ (va_get_reg64 rRax va_sM == 0 \/
    va_get_reg64 rRax va_sM == 1) /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM)
    (va_get_reg64 rRdi va_sM) dst_b 4 (va_get_mem_layout va_sM) Secret /\
    Vale.X64.Decls.modifies_buffer dst_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet 0 va_sM))
    ==> va_k va_sM (())))


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

[@ "opaque_to_smt" va_qattr]
let va_quick_Fast_sub (dst_b:buffer64) (inA_b:buffer64) (inB_b:buffer64) : (va_quickCode unit
  (va_code_Fast_sub ())) =
  (va_QProc (va_code_Fast_sub ()) ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR11;
    va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRax; va_Mod_mem])
    (va_wp_Fast_sub dst_b inA_b inB_b) (va_wpProof_Fast_sub dst_b inA_b inB_b))
#pop-options
//--
//-- Cswap_single

val va_code_Cswap_single : offset:nat -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Cswap_single offset =
  (va_Block (va_CCons (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64
    rR8) (va_op_reg_opr64_reg64 rRsi) (0 + offset `op_Multiply` 8) Secret) (va_CCons
    (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR9)
    (va_op_reg_opr64_reg64 rRdx) (0 + offset `op_Multiply` 8) Secret) (va_CCons (va_code_Mov64
    (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR8)) (va_CCons (va_code_Cmovc64
    (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rR9)) (va_CCons (va_code_Cmovc64
    (va_op_dst_opr64_reg64 rR9) (va_op_opr64_reg64 rR10)) (va_CCons (va_code_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRsi) (va_op_reg_opr64_reg64 rR8) (0 +
    offset `op_Multiply` 8) Secret) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdx) (va_op_reg_opr64_reg64 rR9) (0 + offset `op_Multiply` 8) Secret)
    (va_CNil ())))))))))

val va_codegen_success_Cswap_single : offset:nat -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Cswap_single offset =
  (va_pbool_and (va_codegen_success_Load64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_dst_opr64_reg64 rR8) (va_op_reg_opr64_reg64 rRsi) (0 + offset `op_Multiply` 8) Secret)
    (va_pbool_and (va_codegen_success_Load64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_dst_opr64_reg64 rR9) (va_op_reg_opr64_reg64 rRdx) (0 + offset `op_Multiply` 8) Secret)
    (va_pbool_and (va_codegen_success_Mov64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR8))
    (va_pbool_and (va_codegen_success_Cmovc64 (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rR9))
    (va_pbool_and (va_codegen_success_Cmovc64 (va_op_dst_opr64_reg64 rR9) (va_op_opr64_reg64 rR10))
    (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRsi) (va_op_reg_opr64_reg64 rR8) (0 + offset `op_Multiply` 8) Secret)
    (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdx) (va_op_reg_opr64_reg64 rR9) (0 + offset `op_Multiply` 8) Secret)
    (va_ttrue ()))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Cswap_single (va_mods:va_mods_t) (offset:nat) (p0_b:buffer64) (p1_b:buffer64) :
  (va_quickCode unit (va_code_Cswap_single offset)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (old_p0_val:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read p0_b (0 + offset)
    (va_get_mem_heaplet 0 va_s) in let (old_p1_val:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read p1_b (0 + offset) (va_get_mem_heaplet 0 va_s) in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 839 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR8)
    (va_op_reg_opr64_reg64 rRsi) (0 + offset `op_Multiply` 8) Secret p0_b (0 + offset)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 840 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rR9)
    (va_op_reg_opr64_reg64 rRdx) (0 + offset `op_Multiply` 8) Secret p1_b (0 + offset)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 841 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Mov64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR8)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 842 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Cmovc64 (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rR9)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 843 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_quick_Cmovc64 (va_op_dst_opr64_reg64 rR9) (va_op_opr64_reg64 rR10)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 844 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 rRsi)
    (va_op_reg_opr64_reg64 rR8) (0 + offset `op_Multiply` 8) Secret p0_b (0 + offset)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 845 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 rRdx)
    (va_op_reg_opr64_reg64 rR9) (0 + offset `op_Multiply` 8) Secret p1_b (0 + offset)) (va_QEmpty
    (()))))))))))


val va_lemma_Cswap_single : va_b0:va_code -> va_s0:va_state -> offset:nat -> p0_b:buffer64 ->
  p1_b:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Cswap_single offset) va_s0 /\ va_get_ok va_s0 /\ (let
    (old_p0_val:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read p0_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (old_p1_val:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read p1_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in offset < 8 /\
    (Vale.X64.Decls.buffers_disjoint p1_b p0_b \/ p1_b == p0_b) /\ Vale.X64.Decls.validDstAddrs64
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRsi va_s0) p0_b 8 (va_get_mem_layout va_s0) Secret
    /\ Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdx va_s0) p1_b 8
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.valid_cf (va_get_flags va_s0))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (old_p0_val:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read p0_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (old_p1_val:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read p1_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRsi va_sM) p0_b 8
    (va_get_mem_layout va_sM) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM)
    (va_get_reg64 rRdx va_sM) p1_b 8 (va_get_mem_layout va_sM) Secret /\
    Vale.X64.Decls.modifies_buffer_2 p0_b p1_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet 0
    va_sM) /\ (forall (i:nat) . 0 <= i /\ i < 8 /\ i =!= offset ==> Vale.X64.Decls.buffer64_read
    p0_b i (va_get_mem_heaplet 0 va_sM) == Vale.X64.Decls.buffer64_read p0_b i (va_get_mem_heaplet
    0 va_s0) /\ Vale.X64.Decls.buffer64_read p1_b i (va_get_mem_heaplet 0 va_sM) ==
    Vale.X64.Decls.buffer64_read p1_b i (va_get_mem_heaplet 0 va_s0)) /\ (let p0_val =
    Vale.X64.Decls.buffer64_read p0_b (0 + offset) (va_get_mem_heaplet 0 va_sM) in let p1_val =
    Vale.X64.Decls.buffer64_read p1_b (0 + offset) (va_get_mem_heaplet 0 va_sM) in p0_val == (if
    Vale.X64.Decls.cf (va_get_flags va_sM) then old_p1_val else old_p0_val) /\ p1_val == (if
    Vale.X64.Decls.cf (va_get_flags va_sM) then old_p0_val else old_p1_val))) /\ va_state_eq va_sM
    (va_update_mem_heaplet 0 va_sM (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM
    (va_update_reg64 rR8 va_sM (va_update_ok va_sM (va_update_mem va_sM va_s0))))))))
[@"opaque_to_smt"]
let va_lemma_Cswap_single va_b0 va_s0 offset p0_b p1_b =
  let (va_mods:va_mods_t) = [va_Mod_mem_heaplet 0; va_Mod_reg64 rR10; va_Mod_reg64 rR9;
    va_Mod_reg64 rR8; va_Mod_ok; va_Mod_mem] in
  let va_qc = va_qcode_Cswap_single va_mods offset p0_b p1_b in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Cswap_single offset) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 792 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (va_get_ok va_sM) /\ (let (old_p0_val:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    p0_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let (old_p1_val:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read p1_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in label va_range1
    "***** POSTCONDITION NOT MET AT line 821 column 67 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRsi va_sM) p0_b 8
    (va_get_mem_layout va_sM) Secret) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 822 column 67 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdx va_sM) p1_b 8
    (va_get_mem_layout va_sM) Secret) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 824 column 57 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (Vale.X64.Decls.modifies_buffer_2 p0_b p1_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet 0
    va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 832 column 59 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (forall (i:nat) . 0 <= i /\ i < 8 /\ i =!= offset ==> Vale.X64.Decls.buffer64_read p0_b i
    (va_get_mem_heaplet 0 va_sM) == Vale.X64.Decls.buffer64_read p0_b i (va_get_mem_heaplet 0
    va_s0) /\ Vale.X64.Decls.buffer64_read p1_b i (va_get_mem_heaplet 0 va_sM) ==
    Vale.X64.Decls.buffer64_read p1_b i (va_get_mem_heaplet 0 va_s0)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 834 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let p0_val = Vale.X64.Decls.buffer64_read p0_b (0 + offset) (va_get_mem_heaplet 0 va_sM) in
    label va_range1
    "***** POSTCONDITION NOT MET AT line 835 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (let p1_val = Vale.X64.Decls.buffer64_read p1_b (0 + offset) (va_get_mem_heaplet 0 va_sM) in
    label va_range1
    "***** POSTCONDITION NOT MET AT line 836 column 63 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (p0_val == va_if (Vale.X64.Decls.cf (va_get_flags va_sM)) (fun _ -> old_p1_val) (fun _ ->
    old_p0_val)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 837 column 63 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastUtil.vaf *****"
    (p1_val == va_if (Vale.X64.Decls.cf (va_get_flags va_sM)) (fun _ -> old_p0_val) (fun _ ->
    old_p1_val)))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_mem_heaplet 0; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8;
    va_Mod_ok; va_Mod_mem]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Cswap_single (offset:nat) (p0_b:buffer64) (p1_b:buffer64) (va_s0:va_state)
  (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (let (old_p0_val:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read p0_b
    (0 + offset) (va_get_mem_heaplet 0 va_s0) in let (old_p1_val:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read p1_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in offset < 8 /\
    (Vale.X64.Decls.buffers_disjoint p1_b p0_b \/ p1_b == p0_b) /\ Vale.X64.Decls.validDstAddrs64
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRsi va_s0) p0_b 8 (va_get_mem_layout va_s0) Secret
    /\ Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdx va_s0) p1_b 8
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.valid_cf (va_get_flags va_s0)) /\ (forall
    (va_x_mem:vale_heap) (va_x_r8:nat64) (va_x_r9:nat64) (va_x_r10:nat64) (va_x_heap0:vale_heap) .
    let va_sM = va_upd_mem_heaplet 0 va_x_heap0 (va_upd_reg64 rR10 va_x_r10 (va_upd_reg64 rR9
    va_x_r9 (va_upd_reg64 rR8 va_x_r8 (va_upd_mem va_x_mem va_s0)))) in va_get_ok va_sM /\ (let
    (old_p0_val:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read p0_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (old_p1_val:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read p1_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRsi va_sM) p0_b 8
    (va_get_mem_layout va_sM) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM)
    (va_get_reg64 rRdx va_sM) p1_b 8 (va_get_mem_layout va_sM) Secret /\
    Vale.X64.Decls.modifies_buffer_2 p0_b p1_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet 0
    va_sM) /\ (forall (i:nat) . 0 <= i /\ i < 8 /\ i =!= offset ==> Vale.X64.Decls.buffer64_read
    p0_b i (va_get_mem_heaplet 0 va_sM) == Vale.X64.Decls.buffer64_read p0_b i (va_get_mem_heaplet
    0 va_s0) /\ Vale.X64.Decls.buffer64_read p1_b i (va_get_mem_heaplet 0 va_sM) ==
    Vale.X64.Decls.buffer64_read p1_b i (va_get_mem_heaplet 0 va_s0)) /\ (let p0_val =
    Vale.X64.Decls.buffer64_read p0_b (0 + offset) (va_get_mem_heaplet 0 va_sM) in let p1_val =
    Vale.X64.Decls.buffer64_read p1_b (0 + offset) (va_get_mem_heaplet 0 va_sM) in p0_val == va_if
    (Vale.X64.Decls.cf (va_get_flags va_sM)) (fun _ -> old_p1_val) (fun _ -> old_p0_val) /\ p1_val
    == va_if (Vale.X64.Decls.cf (va_get_flags va_sM)) (fun _ -> old_p0_val) (fun _ -> old_p1_val)))
    ==> va_k va_sM (())))


val va_wpProof_Cswap_single : offset:nat -> p0_b:buffer64 -> p1_b:buffer64 -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Cswap_single offset p0_b p1_b va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Cswap_single offset)
    ([va_Mod_mem_heaplet 0; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_mem])
    va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Cswap_single offset p0_b p1_b va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Cswap_single (va_code_Cswap_single offset) va_s0 offset p0_b p1_b in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_mem_heaplet 0 va_sM (va_update_reg64 rR10 va_sM
    (va_update_reg64 rR9 va_sM (va_update_reg64 rR8 va_sM (va_update_ok va_sM (va_update_mem va_sM
    va_s0)))))));
  va_lemma_norm_mods ([va_Mod_mem_heaplet 0; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8;
    va_Mod_mem]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Cswap_single (offset:nat) (p0_b:buffer64) (p1_b:buffer64) : (va_quickCode unit
  (va_code_Cswap_single offset)) =
  (va_QProc (va_code_Cswap_single offset) ([va_Mod_mem_heaplet 0; va_Mod_reg64 rR10; va_Mod_reg64
    rR9; va_Mod_reg64 rR8; va_Mod_mem]) (va_wp_Cswap_single offset p0_b p1_b)
    (va_wpProof_Cswap_single offset p0_b p1_b))
//--
//-- Cswap2

[@ "opaque_to_smt" va_qattr]
let va_code_Cswap2 () =
  (va_Block (va_CCons (va_code_CreateHeaplets ()) (va_CCons (va_code_Comment
    "Transfer bit into CF flag"
    ) (va_CCons (va_code_Add64Wrap (va_op_dst_opr64_reg64 rRdi) (va_const_opr64
    18446744073709551615)) (va_CCons (va_code_Newline ()) (va_CCons (va_code_Comment
    "cswap p1[0], p2[0]"
    ) (va_CCons (va_code_Cswap_single 0) (va_CCons (va_code_Newline ()) (va_CCons (va_code_Comment
    "cswap p1[1], p2[1]"
    ) (va_CCons (va_code_Cswap_single 1) (va_CCons (va_code_Newline ()) (va_CCons (va_code_Comment
    "cswap p1[2], p2[2]"
    ) (va_CCons (va_code_Cswap_single 2) (va_CCons (va_code_Newline ()) (va_CCons (va_code_Comment
    "cswap p1[3], p2[3]"
    ) (va_CCons (va_code_Cswap_single 3) (va_CCons (va_code_Newline ()) (va_CCons (va_code_Comment
    "cswap p1[4], p2[4]"
    ) (va_CCons (va_code_Cswap_single 4) (va_CCons (va_code_Newline ()) (va_CCons (va_code_Comment
    "cswap p1[5], p2[5]"
    ) (va_CCons (va_code_Cswap_single 5) (va_CCons (va_code_Newline ()) (va_CCons (va_code_Comment
    "cswap p1[6], p2[6]"
    ) (va_CCons (va_code_Cswap_single 6) (va_CCons (va_code_Newline ()) (va_CCons (va_code_Comment
    "cswap p1[7], p2[7]"
    ) (va_CCons (va_code_Cswap_single 7) (va_CCons (va_code_DestroyHeaplets ()) (va_CNil
    ()))))))))))))))))))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Cswap2 () =
  (va_pbool_and (va_codegen_success_CreateHeaplets ()) (va_pbool_and (va_codegen_success_Comment
    "Transfer bit into CF flag"
    ) (va_pbool_and (va_codegen_success_Add64Wrap (va_op_dst_opr64_reg64 rRdi) (va_const_opr64
    18446744073709551615)) (va_pbool_and (va_codegen_success_Newline ()) (va_pbool_and
    (va_codegen_success_Comment
    "cswap p1[0], p2[0]"
    ) (va_pbool_and (va_codegen_success_Cswap_single 0) (va_pbool_and (va_codegen_success_Newline
    ()) (va_pbool_and (va_codegen_success_Comment
    "cswap p1[1], p2[1]"
    ) (va_pbool_and (va_codegen_success_Cswap_single 1) (va_pbool_and (va_codegen_success_Newline
    ()) (va_pbool_and (va_codegen_success_Comment
    "cswap p1[2], p2[2]"
    ) (va_pbool_and (va_codegen_success_Cswap_single 2) (va_pbool_and (va_codegen_success_Newline
    ()) (va_pbool_and (va_codegen_success_Comment
    "cswap p1[3], p2[3]"
    ) (va_pbool_and (va_codegen_success_Cswap_single 3) (va_pbool_and (va_codegen_success_Newline
    ()) (va_pbool_and (va_codegen_success_Comment
    "cswap p1[4], p2[4]"
    ) (va_pbool_and (va_codegen_success_Cswap_single 4) (va_pbool_and (va_codegen_success_Newline
    ()) (va_pbool_and (va_codegen_success_Comment
    "cswap p1[5], p2[5]"
    ) (va_pbool_and (va_codegen_success_Cswap_single 5) (va_pbool_and (va_codegen_success_Newline
    ()) (va_pbool_and (va_codegen_success_Comment
    "cswap p1[6], p2[6]"
    ) (va_pbool_and (va_codegen_success_Cswap_single 6) (va_pbool_and (va_codegen_success_Newline
    ()) (va_pbool_and (va_codegen_success_Comment
    "cswap p1[7], p2[7]"
    ) (va_pbool_and (va_codegen_success_Cswap_single 7) (va_pbool_and
    (va_codegen_success_DestroyHeaplets ()) (va_ttrue ())))))))))))))))))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Cswap2 (va_mods:va_mods_t) (bit_in:nat64) (p0_b:buffer64) (p1_b:buffer64) :
val va_qcode_Cswap2 (va_mods: va_mods_t) (bit_in: nat64) (p0_b p1_b: buffer64)
    : (va_quickCode unit (va_code_Cswap2 ()))

    va_mods: Vale.X64.QuickCode.va_mods_t ->
    bit_in: Vale.X64.Memory.nat64 ->
    p0_b: Vale.X64.Memory.buffer64 ->
    p1_b: Vale.X64.Memory.buffer64
  -> Vale.X64.QuickCode.va_quickCode Prims.unit (Vale.Curve25519.X64.FastUtil.va_code_Cswap2 ())