val va_quick_Fast_sqr_part3 (offset: nat) (dst_b inA_b: buffer64)
    : (va_quickCode unit (va_code_Fast_sqr_part3 offset))
let va_quick_Fast_sqr_part3 (offset:nat) (dst_b:buffer64) (inA_b:buffer64) : (va_quickCode unit
  (va_code_Fast_sqr_part3 offset)) =
  (va_QProc (va_code_Fast_sqr_part3 offset) ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64
    rR15; va_Mod_reg64 rR14; va_Mod_reg64 rR13; va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64
    rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64
    rRax; va_Mod_mem]) (va_wp_Fast_sqr_part3 offset dst_b inA_b) (va_wpProof_Fast_sqr_part3 offset
    dst_b inA_b))
val va_quick_Fast_sqr_part3 (offset: nat) (dst_b inA_b: buffer64)
    : (va_quickCode unit (va_code_Fast_sqr_part3 offset))
let va_quick_Fast_sqr_part3 (offset: nat) (dst_b inA_b: buffer64)
    : (va_quickCode unit (va_code_Fast_sqr_part3 offset)) =
(va_QProc (va_code_Fast_sqr_part3 offset)
    ([
        va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR15; va_Mod_reg64 rR14; va_Mod_reg64 rR13;
        va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8;
        va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRax; va_Mod_mem
      ])
    (va_wp_Fast_sqr_part3 offset dst_b inA_b)
    (va_wpProof_Fast_sqr_part3 offset dst_b inA_b))
Vale.Curve25519.X64.FastSqr.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.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Curve25519.FastSqr_helpers.fsti.checked Vale.Curve25519.Fast_lemmas_external.fsti.checked Vale.Curve25519.Fast_defs.fst.checked Vale.Bignum.X64.fsti.checked Vale.Bignum.Defs.fsti.checked Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Curve25519.X64.FastSqr.fst
Prims.nat Vale.X64.Memory.buffer64 Vale.X64.QuickCode.va_QProc Prims.unit Vale.Curve25519.X64.FastSqr.va_code_Fast_sqr_part3 Prims.Cons Vale.X64.QuickCode.mod_t Vale.X64.QuickCode.va_Mod_flags Vale.X64.QuickCode.va_Mod_mem_heaplet Vale.X64.QuickCode.va_Mod_reg64 Vale.X64.Machine_s.rR15 Vale.X64.Machine_s.rR14 Vale.X64.Machine_s.rR13 Vale.X64.Machine_s.rRbx Vale.X64.Machine_s.rR11 Vale.X64.Machine_s.rR10 Vale.X64.Machine_s.rR9 Vale.X64.Machine_s.rR8 Vale.X64.Machine_s.rRdx Vale.X64.Machine_s.rRcx Vale.X64.Machine_s.rRax Vale.X64.QuickCode.va_Mod_mem Prims.Nil Vale.Curve25519.X64.FastSqr.va_wp_Fast_sqr_part3 Vale.Curve25519.X64.FastSqr.va_wpProof_Fast_sqr_part3 Vale.X64.QuickCode.va_quickCode
module Vale.Curve25519.X64.FastSqr
open Vale.Def.Words_s
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.FastSqr_helpers
open Vale.X64.CPU_Features_s
open Vale.Bignum.Defs
open Vale.Bignum.X64
#reset-options "--z3rlimit 60"
//-- Fast_sqr_part1
#push-options "--z3rlimit 600"

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

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

[@ "opaque_to_smt" va_qattr]
let va_qcode_Fast_sqr_part1 (va_mods:va_mods_t) (offset:nat) (inA_b:buffer64) : (va_quickCode unit
  (va_code_Fast_sqr_part1 offset)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2
    a3 in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 88 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Arch.Types.xor_lemmas ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 101 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 102 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (0 + offset `op_Multiply` 8) Secret inA_b (0 + offset)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 103 column 134 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 35) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 103 column 147 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[0]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 105 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 106 column 27 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (8 + offset
    `op_Multiply` 8) inA_b (1 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 106 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rR14) (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (8 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg78:Vale.Def.Types_s.nat64) = va_get_reg64 rR8 va_s in let
    (va_arg77:Vale.Def.Types_s.nat64) = va_get_reg64 rR14 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 106 column 122 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg77 va_arg78 a0
    a1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 106 column 148 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 106 column 158 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Xor64 (va_op_dst_opr64_reg64 rR15) (va_op_opr64_reg64 rR15)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 106 column 175 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 106 column 187 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[1]*f[0]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 108 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 109 column 27 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (16 + offset
    `op_Multiply` 8) inA_b (2 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 109 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rR10) (va_op_dst_opr64_reg64 rR9) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (16 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg76:Vale.Def.Types_s.nat64) = va_get_reg64 rR9 va_s in let
    (va_arg75:Vale.Def.Types_s.nat64) = va_get_reg64 rR10 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 109 column 123 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg75 va_arg76 a0
    a2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 109 column 148 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 109 column 163 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR9) (va_op_opr64_reg64 rR14)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 109 column 180 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 109 column 192 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[2]*f[0]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 111 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 112 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (24 + offset
    `op_Multiply` 8) inA_b (3 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 112 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rRcx) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (24 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg74:Vale.Def.Types_s.nat64) = va_get_reg64 rRax va_s in let
    (va_arg73:Vale.Def.Types_s.nat64) = va_get_reg64 rRcx va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 112 column 124 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg73 va_arg74 a0
    a3) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 112 column 154 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 112 column 168 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 112 column 187 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[3]*f[0]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 114 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 115 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (24 + offset `op_Multiply` 8) Secret inA_b (3 + offset)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 116 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 34) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 116 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[3]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 118 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 119 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (8 + offset
    `op_Multiply` 8) inA_b (1 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 119 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rRbx) (va_op_dst_opr64_reg64 rR11) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (8 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg72:Vale.Def.Types_s.nat64) = va_get_reg64 rR11 va_s in let
    (va_arg71:Vale.Def.Types_s.nat64) = va_get_reg64 rRbx va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 119 column 123 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg71 va_arg72 a3
    a1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 119 column 148 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 119 column 163 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR11) (va_op_opr64_reg64 rRcx)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 119 column 182 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[1]*f[3]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 121 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 122 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (16 + offset
    `op_Multiply` 8) inA_b (2 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 122 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rR13) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (16 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg70:Vale.Def.Types_s.nat64) = va_get_reg64 rRax va_s in let
    (va_arg69:Vale.Def.Types_s.nat64) = va_get_reg64 rR13 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 122 column 124 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg69 va_arg70 a3
    a2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 122 column 154 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 122 column 168 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 122 column 187 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[2]*f[3]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 124 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 125 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (8 + offset `op_Multiply` 8) Secret inA_b (1 + offset)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 126 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 9) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 126 column 25 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR13) (va_op_opr64_reg64 rR15)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 126 column 44 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f1"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 130 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 131 column 27 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (16 + offset
    `op_Multiply` 8) inA_b (2 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 131 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rRcx) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (16 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg68:Vale.Def.Types_s.nat64) = va_get_reg64 rRax va_s in let
    (va_arg67:Vale.Def.Types_s.nat64) = va_get_reg64 rRcx va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 131 column 121 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg67 va_arg68 a1
    a2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 131 column 150 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 131 column 159 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mov64 (va_op_dst_opr64_reg64 rR14) (va_const_opr64 0)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 131 column 174 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 4) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 131 column 186 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[2]*f[1]") (va_QEmpty (()))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))


val va_lemma_Fast_sqr_part1 : va_b0:va_code -> va_s0:va_state -> offset:nat -> inA_b:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Fast_sqr_part1 offset) va_s0 /\ va_get_ok va_s0 /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in adx_enabled /\ bmi2_enabled /\ (offset == 0 \/ offset == 4) /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRsi va_s0) inA_b (4
    + offset) (va_get_mem_layout va_s0) Secret)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in Vale.Curve25519.Fast_defs.pow2_six (va_get_reg64 rR8 va_sM) (va_get_reg64 rR9 va_sM)
    (va_get_reg64 rR10 va_sM) (va_get_reg64 rR11 va_sM) (va_get_reg64 rRbx va_sM) (va_get_reg64
    rR13 va_sM) == Vale.Curve25519.Fast_defs.pow2_five (Vale.Curve25519.Fast_defs.mul_nats a0 a1)
    (Vale.Curve25519.Fast_defs.mul_nats a0 a2) (Vale.Curve25519.Fast_defs.mul_nats a0 a3)
    (Vale.Curve25519.Fast_defs.mul_nats a1 a3) (Vale.Curve25519.Fast_defs.mul_nats a2 a3) /\
    va_mul_nat pow2_64 (va_get_reg64 rRcx va_sM) + va_get_reg64 rRax va_sM == va_mul_nat a1 a2 /\
    va_get_reg64 rR14 va_sM == 0) /\ va_state_eq 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 rRbx va_sM
    (va_update_reg64 rR11 va_sM (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM
    (va_update_reg64 rR8 va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRax va_sM (va_update_ok va_sM va_s0)))))))))))))))
[@"opaque_to_smt"]
let va_lemma_Fast_sqr_part1 va_b0 va_s0 offset inA_b =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_reg64 rR15; va_Mod_reg64 rR14; va_Mod_reg64 rR13;
    va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8;
    va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRax; va_Mod_ok] in
  let va_qc = va_qcode_Fast_sqr_part1 va_mods offset inA_b in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Fast_sqr_part1 offset) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 55 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_get_ok va_sM) /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 +
    offset) (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in label va_range1
    "***** POSTCONDITION NOT MET AT line 82 column 103 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (Vale.Curve25519.Fast_defs.pow2_six (va_get_reg64 rR8 va_sM) (va_get_reg64 rR9 va_sM)
    (va_get_reg64 rR10 va_sM) (va_get_reg64 rR11 va_sM) (va_get_reg64 rRbx va_sM) (va_get_reg64
    rR13 va_sM) == Vale.Curve25519.Fast_defs.pow2_five (Vale.Curve25519.Fast_defs.mul_nats a0 a1)
    (Vale.Curve25519.Fast_defs.mul_nats a0 a2) (Vale.Curve25519.Fast_defs.mul_nats a0 a3)
    (Vale.Curve25519.Fast_defs.mul_nats a1 a3) (Vale.Curve25519.Fast_defs.mul_nats a2 a3)) /\ label
    va_range1
    "***** POSTCONDITION NOT MET AT line 84 column 39 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_mul_nat pow2_64 (va_get_reg64 rRcx va_sM) + va_get_reg64 rRax va_sM == va_mul_nat a1 a2) /\
    label va_range1
    "***** POSTCONDITION NOT MET AT line 86 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_get_reg64 rR14 va_sM == 0))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_reg64 rR15; va_Mod_reg64 rR14; va_Mod_reg64 rR13;
    va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8;
    va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRax; va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Fast_sqr_part1 (offset:nat) (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 +
    offset) (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in adx_enabled /\ bmi2_enabled /\ (offset == 0
    \/ offset == 4) /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64
    rRsi va_s0) inA_b (4 + offset) (va_get_mem_layout va_s0) Secret) /\ (forall (va_x_rax:nat64)
    (va_x_rcx:nat64) (va_x_rdx:nat64) (va_x_r8:nat64) (va_x_r9:nat64) (va_x_r10:nat64)
    (va_x_r11:nat64) (va_x_rbx:nat64) (va_x_r13:nat64) (va_x_r14:nat64) (va_x_r15:nat64)
    (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_reg64 rR15 va_x_r15
    (va_upd_reg64 rR14 va_x_r14 (va_upd_reg64 rR13 va_x_r13 (va_upd_reg64 rRbx va_x_rbx
    (va_upd_reg64 rR11 va_x_r11 (va_upd_reg64 rR10 va_x_r10 (va_upd_reg64 rR9 va_x_r9 (va_upd_reg64
    rR8 va_x_r8 (va_upd_reg64 rRdx va_x_rdx (va_upd_reg64 rRcx va_x_rcx (va_upd_reg64 rRax va_x_rax
    va_s0))))))))))) in va_get_ok va_sM /\ (let (a0:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (0 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (1 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in
    Vale.Curve25519.Fast_defs.pow2_six (va_get_reg64 rR8 va_sM) (va_get_reg64 rR9 va_sM)
    (va_get_reg64 rR10 va_sM) (va_get_reg64 rR11 va_sM) (va_get_reg64 rRbx va_sM) (va_get_reg64
    rR13 va_sM) == Vale.Curve25519.Fast_defs.pow2_five (Vale.Curve25519.Fast_defs.mul_nats a0 a1)
    (Vale.Curve25519.Fast_defs.mul_nats a0 a2) (Vale.Curve25519.Fast_defs.mul_nats a0 a3)
    (Vale.Curve25519.Fast_defs.mul_nats a1 a3) (Vale.Curve25519.Fast_defs.mul_nats a2 a3) /\
    va_mul_nat pow2_64 (va_get_reg64 rRcx va_sM) + va_get_reg64 rRax va_sM == va_mul_nat a1 a2 /\
    va_get_reg64 rR14 va_sM == 0) ==> va_k va_sM (())))


val va_wpProof_Fast_sqr_part1 : offset:nat -> 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_sqr_part1 offset inA_b va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Fast_sqr_part1 offset) ([va_Mod_flags;
    va_Mod_reg64 rR15; va_Mod_reg64 rR14; va_Mod_reg64 rR13; va_Mod_reg64 rRbx; va_Mod_reg64 rR11;
    va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx;
    va_Mod_reg64 rRax]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Fast_sqr_part1 offset inA_b va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Fast_sqr_part1 (va_code_Fast_sqr_part1 offset) va_s0 offset inA_b in
  va_lemma_upd_update va_sM;
  assert (va_state_eq 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 rRbx va_sM (va_update_reg64 rR11 va_sM
    (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM (va_update_reg64 rR8 va_sM
    (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM (va_update_reg64 rRax va_sM
    (va_update_ok va_sM va_s0))))))))))))));
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_reg64 rR15; va_Mod_reg64 rR14; va_Mod_reg64 rR13;
    va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8;
    va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRax]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Fast_sqr_part1 (offset:nat) (inA_b:buffer64) : (va_quickCode unit
  (va_code_Fast_sqr_part1 offset)) =
  (va_QProc (va_code_Fast_sqr_part1 offset) ([va_Mod_flags; va_Mod_reg64 rR15; va_Mod_reg64 rR14;
    va_Mod_reg64 rR13; va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9;
    va_Mod_reg64 rR8; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRax])
    (va_wp_Fast_sqr_part1 offset inA_b) (va_wpProof_Fast_sqr_part1 offset inA_b))
#pop-options
//--
#restart-solver
#push-options "--z3rlimit 400 --max_fuel 0 --max_ifuel 0"
open FStar.Mul

let lemma_fast_sqr_part2 (a0 a1 a2 a3 a4 a5 b2 b3:nat64) : Lemma
  (ensures (
    let z:nat64 = 0 in
    let (x0, c) = (add_lo_hi a0 a0 0) in
    let (x1, c) = (add_lo_hi a1 a1 c) in
    let (x2, o) = (add_lo_hi a2 b2 0) in let (x2, c) = (add_lo_hi x2 x2 c) in
    let (x3, o) = (add_lo_hi a3 b3 o) in let (x3, c) = (add_lo_hi x3 x3 c) in
    let (x4, o) = (add_lo_hi a4  z o) in let (x4, c) = (add_lo_hi x4 x4 c) in
    let (x5, o) = (add_lo_hi a5  z o) in let (x5, c) = (add_lo_hi x5 x5 c) in
    let (x6, _) = (add_lo_hi  z  z o) in let (x6, _) = (add_lo_hi x6 x6 c) in
    pow2_seven x0 x1 x2 x3 x4 x5 x6 ==
      pow2_six (2 * a0) (2 * a1) (2 * (a2 + b2)) (2 * (a3 + b3)) (2 * a4) (2 * a5) /\
    x6 <= 2
  ))
  =
  lemma_add_hi_lo64 0
#pop-options
#restart-solver
//-- lemma_fast_sqr_part2
//--
//-- Fast_sqr_part2
#push-options "--z3rlimit 600"

val va_code_Fast_sqr_part2 : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Fast_sqr_part2 () =
  (va_Block (va_CCons (va_code_Xor64 (va_op_dst_opr64_reg64 rR15) (va_op_opr64_reg64 rR15))
    (va_CCons (va_code_Adox_64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rRax)) (va_CCons
    (va_code_Adcx_64 (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rR8)) (va_CCons
    (va_code_Adox_64 (va_op_dst_opr64_reg64 rR11) (va_op_opr64_reg64 rRcx)) (va_CCons
    (va_code_Adcx_64 (va_op_dst_opr64_reg64 rR9) (va_op_opr64_reg64 rR9)) (va_CCons
    (va_code_Adox_64 (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR15)) (va_CCons
    (va_code_Adcx_64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR10)) (va_CCons
    (va_code_Adox_64 (va_op_dst_opr64_reg64 rR13) (va_op_opr64_reg64 rR15)) (va_CCons
    (va_code_Adcx_64 (va_op_dst_opr64_reg64 rR11) (va_op_opr64_reg64 rR11)) (va_CCons
    (va_code_Adox_64 (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rR15)) (va_CCons
    (va_code_Adcx_64 (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rRbx)) (va_CCons
    (va_code_Adcx_64 (va_op_dst_opr64_reg64 rR13) (va_op_opr64_reg64 rR13)) (va_CCons
    (va_code_Adcx_64 (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rR14)) (va_CNil
    ())))))))))))))))

val va_codegen_success_Fast_sqr_part2 : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Fast_sqr_part2 () =
  (va_pbool_and (va_codegen_success_Xor64 (va_op_dst_opr64_reg64 rR15) (va_op_opr64_reg64 rR15))
    (va_pbool_and (va_codegen_success_Adox_64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64
    rRax)) (va_pbool_and (va_codegen_success_Adcx_64 (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64
    rR8)) (va_pbool_and (va_codegen_success_Adox_64 (va_op_dst_opr64_reg64 rR11) (va_op_opr64_reg64
    rRcx)) (va_pbool_and (va_codegen_success_Adcx_64 (va_op_dst_opr64_reg64 rR9) (va_op_opr64_reg64
    rR9)) (va_pbool_and (va_codegen_success_Adox_64 (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64
    rR15)) (va_pbool_and (va_codegen_success_Adcx_64 (va_op_dst_opr64_reg64 rR10)
    (va_op_opr64_reg64 rR10)) (va_pbool_and (va_codegen_success_Adox_64 (va_op_dst_opr64_reg64
    rR13) (va_op_opr64_reg64 rR15)) (va_pbool_and (va_codegen_success_Adcx_64
    (va_op_dst_opr64_reg64 rR11) (va_op_opr64_reg64 rR11)) (va_pbool_and
    (va_codegen_success_Adox_64 (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rR15))
    (va_pbool_and (va_codegen_success_Adcx_64 (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64
    rRbx)) (va_pbool_and (va_codegen_success_Adcx_64 (va_op_dst_opr64_reg64 rR13)
    (va_op_opr64_reg64 rR13)) (va_pbool_and (va_codegen_success_Adcx_64 (va_op_dst_opr64_reg64
    rR14) (va_op_opr64_reg64 rR14)) (va_ttrue ()))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Fast_sqr_part2 (va_mods:va_mods_t) : (va_quickCode unit (va_code_Fast_sqr_part2 ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 190 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Arch.Types.xor_lemmas ()) (let (va_arg25:nat64) = va_get_reg64 rRcx va_s
    in let (va_arg24:nat64) = va_get_reg64 rRax va_s in let (va_arg23:nat64) = va_get_reg64 rR13
    va_s in let (va_arg22:nat64) = va_get_reg64 rRbx va_s in let (va_arg21:nat64) = va_get_reg64
    rR11 va_s in let (va_arg20:nat64) = va_get_reg64 rR10 va_s in let (va_arg19:nat64) =
    va_get_reg64 rR9 va_s in let (va_arg18:nat64) = va_get_reg64 rR8 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 191 column 25 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> lemma_fast_sqr_part2 va_arg18 va_arg19 va_arg20 va_arg21 va_arg22 va_arg23
    va_arg24 va_arg25) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 193 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Xor64 (va_op_dst_opr64_reg64 rR15) (va_op_opr64_reg64 rR15)) (fun (va_s:va_state) _
    -> va_QLemma va_range1
    "***** PRECONDITION NOT MET AT line 194 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    ((fun (f:flags_t) -> true) (va_get_flags va_s)) (fun _ -> (fun (f:flags_t) -> flag_cf f = 1 ==
    cf f /\ flag_of f = 1 == overflow f) (va_get_flags va_s)) (fun (_:unit) -> reveal_flags
    (va_get_flags va_s)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 196 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adox_64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 196 column 35 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx_64 (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rR8)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 197 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adox_64 (va_op_dst_opr64_reg64 rR11) (va_op_opr64_reg64 rRcx)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 197 column 35 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx_64 (va_op_dst_opr64_reg64 rR9) (va_op_opr64_reg64 rR9)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 198 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adox_64 (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR15)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 198 column 35 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx_64 (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR10)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 199 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adox_64 (va_op_dst_opr64_reg64 rR13) (va_op_opr64_reg64 rR15)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 199 column 35 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx_64 (va_op_dst_opr64_reg64 rR11) (va_op_opr64_reg64 rR11)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 200 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adox_64 (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rR15)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 200 column 35 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx_64 (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rRbx)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 201 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx_64 (va_op_dst_opr64_reg64 rR13) (va_op_opr64_reg64 rR13)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 201 column 35 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx_64 (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rR14)) (va_QEmpty
    (())))))))))))))))))))


val va_lemma_Fast_sqr_part2 : va_b0:va_code -> va_s0:va_state
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Fast_sqr_part2 ()) va_s0 /\ va_get_ok va_s0 /\
    (adx_enabled /\ bmi2_enabled) /\ va_get_reg64 rR14 va_s0 == 0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    Vale.Curve25519.Fast_defs.pow2_seven (va_get_reg64 rR8 va_sM) (va_get_reg64 rR9 va_sM)
    (va_get_reg64 rR10 va_sM) (va_get_reg64 rR11 va_sM) (va_get_reg64 rRbx va_sM) (va_get_reg64
    rR13 va_sM) (va_get_reg64 rR14 va_sM) == Vale.Curve25519.Fast_defs.pow2_six (2 `op_Multiply`
    va_get_reg64 rR8 va_s0) (2 `op_Multiply` va_get_reg64 rR9 va_s0) (2 `op_Multiply` (va_get_reg64
    rR10 va_s0 + va_get_reg64 rRax va_s0)) (2 `op_Multiply` (va_get_reg64 rR11 va_s0 + va_get_reg64
    rRcx va_s0)) (2 `op_Multiply` va_get_reg64 rRbx va_s0) (2 `op_Multiply` va_get_reg64 rR13
    va_s0) /\ va_get_reg64 rR14 va_sM <= 2 /\ va_state_eq 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 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_ok va_sM va_s0))))))))))))
[@"opaque_to_smt"]
let va_lemma_Fast_sqr_part2 va_b0 va_s0 =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_reg64 rR15; 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_ok] in
  let va_qc = va_qcode_Fast_sqr_part2 va_mods in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Fast_sqr_part2 ()) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 170 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_get_ok va_sM) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 186 column 76 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (Vale.Curve25519.Fast_defs.pow2_seven (va_get_reg64 rR8 va_sM) (va_get_reg64 rR9 va_sM)
    (va_get_reg64 rR10 va_sM) (va_get_reg64 rR11 va_sM) (va_get_reg64 rRbx va_sM) (va_get_reg64
    rR13 va_sM) (va_get_reg64 rR14 va_sM) == Vale.Curve25519.Fast_defs.pow2_six (2 `op_Multiply`
    va_get_reg64 rR8 va_s0) (2 `op_Multiply` va_get_reg64 rR9 va_s0) (2 `op_Multiply` (va_get_reg64
    rR10 va_s0 + va_get_reg64 rRax va_s0)) (2 `op_Multiply` (va_get_reg64 rR11 va_s0 + va_get_reg64
    rRcx va_s0)) (2 `op_Multiply` va_get_reg64 rRbx va_s0) (2 `op_Multiply` va_get_reg64 rR13
    va_s0)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 188 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_get_reg64 rR14 va_sM <= 2)) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_reg64 rR15; 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_ok]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Fast_sqr_part2 (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (adx_enabled /\ bmi2_enabled) /\ va_get_reg64 rR14 va_s0 == 0 /\ (forall
    (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_r15:nat64) (va_x_efl:Vale.X64.Flags.t) . let va_sM =
    va_upd_flags va_x_efl (va_upd_reg64 rR15 va_x_r15 (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_s0)))))))) in va_get_ok va_sM
    /\ Vale.Curve25519.Fast_defs.pow2_seven (va_get_reg64 rR8 va_sM) (va_get_reg64 rR9 va_sM)
    (va_get_reg64 rR10 va_sM) (va_get_reg64 rR11 va_sM) (va_get_reg64 rRbx va_sM) (va_get_reg64
    rR13 va_sM) (va_get_reg64 rR14 va_sM) == Vale.Curve25519.Fast_defs.pow2_six (2 `op_Multiply`
    va_get_reg64 rR8 va_s0) (2 `op_Multiply` va_get_reg64 rR9 va_s0) (2 `op_Multiply` (va_get_reg64
    rR10 va_s0 + va_get_reg64 rRax va_s0)) (2 `op_Multiply` (va_get_reg64 rR11 va_s0 + va_get_reg64
    rRcx va_s0)) (2 `op_Multiply` va_get_reg64 rRbx va_s0) (2 `op_Multiply` va_get_reg64 rR13
    va_s0) /\ va_get_reg64 rR14 va_sM <= 2 ==> va_k va_sM (())))


val va_wpProof_Fast_sqr_part2 : 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_sqr_part2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Fast_sqr_part2 ()) ([va_Mod_flags;
    va_Mod_reg64 rR15; 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_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Fast_sqr_part2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Fast_sqr_part2 (va_code_Fast_sqr_part2 ()) va_s0 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq 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 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_ok
    va_sM va_s0)))))))))));
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_reg64 rR15; 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_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Fast_sqr_part2 () : (va_quickCode unit (va_code_Fast_sqr_part2 ())) =
  (va_QProc (va_code_Fast_sqr_part2 ()) ([va_Mod_flags; va_Mod_reg64 rR15; 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_wp_Fast_sqr_part2 va_wpProof_Fast_sqr_part2)
#pop-options
//--
//-- Fast_sqr_part3
#push-options "--z3rlimit 1000"
#restart-solver

val va_code_Fast_sqr_part3 : offset:nat -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Fast_sqr_part3 offset =
  (va_Block (va_CCons (va_code_NoNewline ()) (va_CCons (va_code_Load64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx) (va_op_reg_opr64_reg64 rRsi) (0 +
    offset `op_Multiply` 8) Secret) (va_CCons (va_code_Space 1) (va_CCons (va_code_Mulx64
    (va_op_dst_opr64_reg64 rRcx) (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRdx)) (va_CCons
    (va_code_Comment
    "f[0]^2"
    ) (va_CCons (va_code_Space 27) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rRax) (0 + offset `op_Multiply` 16) Secret)
    (va_CCons (va_code_Newline ()) (va_CCons (va_code_NoNewline ()) (va_CCons (va_code_Add64Wrap
    (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rRcx)) (va_CCons (va_code_Space 3) (va_CCons
    (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR8) (8 + offset `op_Multiply` 16) Secret) (va_CCons (va_code_Newline
    ()) (va_CCons (va_code_NoNewline ()) (va_CCons (va_code_Load64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx) (va_op_reg_opr64_reg64 rRsi) (8 +
    offset `op_Multiply` 8) Secret) (va_CCons (va_code_Space 1) (va_CCons (va_code_Mulx64
    (va_op_dst_opr64_reg64 rRcx) (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRdx)) (va_CCons
    (va_code_Comment
    "f[1]^2"
    ) (va_CCons (va_code_NoNewline ()) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rR9)
    (va_op_opr64_reg64 rRax)) (va_CCons (va_code_Space 2) (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 +
    offset `op_Multiply` 16) Secret) (va_CCons (va_code_Newline ()) (va_CCons (va_code_NoNewline
    ()) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rRcx))
    (va_CCons (va_code_Space 1) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR10) (24 + offset `op_Multiply` 16)
    Secret) (va_CCons (va_code_Newline ()) (va_CCons (va_code_NoNewline ()) (va_CCons
    (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (16 + offset `op_Multiply` 8) Secret) (va_CCons (va_code_NoNewline
    ()) (va_CCons (va_code_Mulx64 (va_op_dst_opr64_reg64 rRcx) (va_op_dst_opr64_reg64 rRax)
    (va_op_opr64_reg64 rRdx)) (va_CCons (va_code_Comment
    "f[2]^2"
    ) (va_CCons (va_code_NoNewline ()) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rR11)
    (va_op_opr64_reg64 rRax)) (va_CCons (va_code_Space 1) (va_CCons (va_code_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR11) (32 +
    offset `op_Multiply` 16) Secret) (va_CCons (va_code_Newline ()) (va_CCons (va_code_NoNewline
    ()) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rRcx))
    (va_CCons (va_code_Space 1) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rRbx) (40 + offset `op_Multiply` 16)
    Secret) (va_CCons (va_code_Newline ()) (va_CCons (va_code_NoNewline ()) (va_CCons
    (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (24 + offset `op_Multiply` 8) Secret) (va_CCons (va_code_NoNewline
    ()) (va_CCons (va_code_Mulx64 (va_op_dst_opr64_reg64 rRcx) (va_op_dst_opr64_reg64 rRax)
    (va_op_opr64_reg64 rRdx)) (va_CCons (va_code_Comment
    "f[3]^2"
    ) (va_CCons (va_code_NoNewline ()) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rR13)
    (va_op_opr64_reg64 rRax)) (va_CCons (va_code_Space 1) (va_CCons (va_code_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR13) (48 +
    offset `op_Multiply` 16) Secret) (va_CCons (va_code_Newline ()) (va_CCons (va_code_NoNewline
    ()) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rRcx))
    (va_CCons (va_code_Space 1) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR14) (56 + offset `op_Multiply` 16)
    Secret) (va_CCons (va_code_Newline ()) (va_CNil
    ()))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

val va_codegen_success_Fast_sqr_part3 : offset:nat -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Fast_sqr_part3 offset =
  (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Load64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx) (va_op_reg_opr64_reg64 rRsi) (0 +
    offset `op_Multiply` 8) Secret) (va_pbool_and (va_codegen_success_Space 1) (va_pbool_and
    (va_codegen_success_Mulx64 (va_op_dst_opr64_reg64 rRcx) (va_op_dst_opr64_reg64 rRax)
    (va_op_opr64_reg64 rRdx)) (va_pbool_and (va_codegen_success_Comment
    "f[0]^2"
    ) (va_pbool_and (va_codegen_success_Space 27) (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 rRax) (0 +
    offset `op_Multiply` 16) Secret) (va_pbool_and (va_codegen_success_Newline ()) (va_pbool_and
    (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Add64Wrap
    (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rRcx)) (va_pbool_and (va_codegen_success_Space
    3) (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR8) (8 + offset `op_Multiply` 16) Secret)
    (va_pbool_and (va_codegen_success_Newline ()) (va_pbool_and (va_codegen_success_NoNewline ())
    (va_pbool_and (va_codegen_success_Load64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_dst_opr64_reg64 rRdx) (va_op_reg_opr64_reg64 rRsi) (8 + offset `op_Multiply` 8) Secret)
    (va_pbool_and (va_codegen_success_Space 1) (va_pbool_and (va_codegen_success_Mulx64
    (va_op_dst_opr64_reg64 rRcx) (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRdx))
    (va_pbool_and (va_codegen_success_Comment
    "f[1]^2"
    ) (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Adcx64Wrap
    (va_op_dst_opr64_reg64 rR9) (va_op_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_Space
    2) (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 + offset `op_Multiply` 16) Secret)
    (va_pbool_and (va_codegen_success_Newline ()) (va_pbool_and (va_codegen_success_NoNewline ())
    (va_pbool_and (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64
    rRcx)) (va_pbool_and (va_codegen_success_Space 1) (va_pbool_and
    (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR10) (24 + offset `op_Multiply` 16) Secret) (va_pbool_and
    (va_codegen_success_Newline ()) (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and
    (va_codegen_success_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (16 + offset `op_Multiply` 8) Secret) (va_pbool_and
    (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Mulx64
    (va_op_dst_opr64_reg64 rRcx) (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rRdx))
    (va_pbool_and (va_codegen_success_Comment
    "f[2]^2"
    ) (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Adcx64Wrap
    (va_op_dst_opr64_reg64 rR11) (va_op_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_Space
    1) (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR11) (32 + offset `op_Multiply` 16)
    Secret) (va_pbool_and (va_codegen_success_Newline ()) (va_pbool_and
    (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Adcx64Wrap
    (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rRcx)) (va_pbool_and (va_codegen_success_Space
    1) (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rRbx) (40 + offset `op_Multiply` 16)
    Secret) (va_pbool_and (va_codegen_success_Newline ()) (va_pbool_and
    (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Load64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx) (va_op_reg_opr64_reg64 rRsi) (24 +
    offset `op_Multiply` 8) Secret) (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and
    (va_codegen_success_Mulx64 (va_op_dst_opr64_reg64 rRcx) (va_op_dst_opr64_reg64 rRax)
    (va_op_opr64_reg64 rRdx)) (va_pbool_and (va_codegen_success_Comment
    "f[3]^2"
    ) (va_pbool_and (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Adcx64Wrap
    (va_op_dst_opr64_reg64 rR13) (va_op_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_Space
    1) (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR13) (48 + offset `op_Multiply` 16)
    Secret) (va_pbool_and (va_codegen_success_Newline ()) (va_pbool_and
    (va_codegen_success_NoNewline ()) (va_pbool_and (va_codegen_success_Adcx64Wrap
    (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rRcx)) (va_pbool_and (va_codegen_success_Space
    1) (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR14) (56 + offset `op_Multiply` 16)
    Secret) (va_pbool_and (va_codegen_success_Newline ()) (va_ttrue
    ())))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Fast_sqr_part3 (va_mods:va_mods_t) (offset:nat) (dst_b:buffer64) (inA_b:buffer64) :
  (va_quickCode unit (va_code_Fast_sqr_part3 offset)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2
    a3 in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 251 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Arch.Types.xor_lemmas ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 266 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 267 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (0 + offset `op_Multiply` 8) Secret inA_b (0 + offset)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 267 column 89 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 267 column 101 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rRcx) (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64
    rRdx)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 267 column 140 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[0]^2"
    ) (fun (va_s:va_state) _ -> let (a0_sqr_hi:nat64) = va_get_reg64 rRcx va_s in let
    (a0_sqr_lo:nat64) = va_get_reg64 rRax va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 269 column 36 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 27) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 269 column 72 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rRax) (0 + offset `op_Multiply` 16) Secret dst_b (0 + offset
    `op_Multiply` 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 270 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 271 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 272 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Add64Wrap (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rRcx)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 272 column 33 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 3) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 272 column 72 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR8) (8 + offset `op_Multiply` 16) Secret dst_b (1 + offset
    `op_Multiply` 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 273 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 274 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 275 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (8 + offset `op_Multiply` 8) Secret inA_b (1 + offset)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 275 column 90 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 275 column 101 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rRcx) (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64
    rRdx)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 275 column 139 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[1]^2"
    ) (fun (va_s:va_state) _ -> let (a1_sqr_hi:nat64) = va_get_reg64 rRcx va_s in let
    (a1_sqr_lo:nat64) = va_get_reg64 rRax va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 277 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 278 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR9) (va_op_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 278 column 33 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 278 column 72 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR9) (16 + offset `op_Multiply` 16) Secret dst_b (2 + offset
    `op_Multiply` 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 279 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 280 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 281 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rRcx)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 281 column 34 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 281 column 73 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR10) (24 + offset `op_Multiply` 16) Secret dst_b (3 + offset
    `op_Multiply` 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 282 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 283 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 284 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (16 + offset `op_Multiply` 8) Secret inA_b (2 + offset)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 284 column 94 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 284 column 106 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rRcx) (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64
    rRdx)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 284 column 144 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[2]^2"
    ) (fun (va_s:va_state) _ -> let (a2_sqr_hi:nat64) = va_get_reg64 rRcx va_s in let
    (a2_sqr_lo:nat64) = va_get_reg64 rRax va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 286 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 287 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR11) (va_op_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 287 column 34 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 287 column 72 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR11) (32 + offset `op_Multiply` 16) Secret dst_b (4 + offset
    `op_Multiply` 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 288 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 289 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 290 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rRcx)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 290 column 34 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 290 column 72 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rRbx) (40 + offset `op_Multiply` 16) Secret dst_b (5 + offset
    `op_Multiply` 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 291 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 292 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 293 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (24 + offset `op_Multiply` 8) Secret inA_b (3 + offset)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 293 column 94 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 293 column 105 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rRcx) (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64
    rRdx)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 293 column 144 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[3]^2"
    ) (fun (va_s:va_state) _ -> let (va_arg105:Vale.Def.Types_s.nat64) = va_get_reg64 rRdx va_s in
    let (va_arg104:Vale.Def.Types_s.nat64) = va_get_reg64 rRdx va_s in let
    (va_arg103:Vale.Def.Types_s.nat64) = va_get_reg64 rRax va_s in let
    (va_arg102:Vale.Def.Types_s.nat64) = va_get_reg64 rRcx va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 294 column 22 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg102 va_arg103
    va_arg104 va_arg105) (let (a3_sqr_hi:nat64) = va_get_reg64 rRcx va_s in let (a3_sqr_lo:nat64) =
    va_get_reg64 rRax va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 296 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 297 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR13) (va_op_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 297 column 35 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 297 column 72 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR13) (48 + offset `op_Multiply` 16) Secret dst_b (6 + offset
    `op_Multiply` 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 298 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Newline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 299 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 300 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rRcx)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 300 column 35 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 300 column 72 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR14) (56 + offset `op_Multiply` 16) Secret dst_b (7 + offset
    `op_Multiply` 2)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 301 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Newline ()) (fun (va_s:va_state) _ -> let (va_arg101:Vale.Curve25519.Fast_defs.bit) =
    Vale.Curve25519.Fast_defs.bool_bit (Vale.X64.Decls.cf (va_get_flags va_s)) in let
    (va_arg100:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read dst_b (7 + offset
    `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in let (va_arg99:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read dst_b (6 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in
    let (va_arg98:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read dst_b (5 + offset
    `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in let (va_arg97:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read dst_b (4 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in
    let (va_arg96:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read dst_b (3 + offset
    `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in let (va_arg95:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read dst_b (2 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in
    let (va_arg94:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read dst_b (1 + offset
    `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in let (va_arg93:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_s) in
    let (va_arg92:Vale.Def.Types_s.nat64) = va_get_reg64 rR14 va_old_s in let
    (va_arg91:Vale.Def.Types_s.nat64) = va_get_reg64 rR13 va_old_s in let
    (va_arg90:Vale.Def.Types_s.nat64) = va_get_reg64 rRbx va_old_s in let
    (va_arg89:Vale.Def.Types_s.nat64) = va_get_reg64 rR11 va_old_s in let
    (va_arg88:Vale.Def.Types_s.nat64) = va_get_reg64 rR10 va_old_s in let
    (va_arg87:Vale.Def.Types_s.nat64) = va_get_reg64 rR9 va_old_s in let
    (va_arg86:Vale.Def.Types_s.nat64) = va_get_reg64 rR8 va_old_s in let
    (va_arg85:Vale.Def.Types_s.nat64) = a3_sqr_lo in let (va_arg84:Vale.Def.Types_s.nat64) =
    a3_sqr_hi in let (va_arg83:Vale.Def.Types_s.nat64) = a2_sqr_lo in let
    (va_arg82:Vale.Def.Types_s.nat64) = a2_sqr_hi in let (va_arg81:Vale.Def.Types_s.nat64) =
    a1_sqr_lo in let (va_arg80:Vale.Def.Types_s.nat64) = a1_sqr_hi in let
    (va_arg79:Vale.Def.Types_s.nat64) = a0_sqr_lo in let (va_arg78:Vale.Def.Types_s.nat64) =
    a0_sqr_hi in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 303 column 20 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.FastSqr_helpers.lemma_sqr_part3 a a0 a1 a2 a3 va_arg78
    va_arg79 va_arg80 va_arg81 va_arg82 va_arg83 va_arg84 va_arg85 va_arg86 va_arg87 va_arg88
    va_arg89 va_arg90 va_arg91 va_arg92 va_arg93 va_arg94 va_arg95 va_arg96 va_arg97 va_arg98
    va_arg99 va_arg100 va_arg101) (va_QEmpty
    (()))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))


val va_lemma_Fast_sqr_part3 : va_b0:va_code -> va_s0:va_state -> offset:nat -> dst_b:buffer64 ->
  inA_b:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Fast_sqr_part3 offset) va_s0 /\ va_get_ok va_s0 /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in adx_enabled /\ bmi2_enabled /\ (offset == 0 \/ offset == 4) /\
    Vale.X64.Decls.buffers_disjoint dst_b inA_b /\ va_get_reg64 rR14 va_s0 <= 2 /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) dst_b (8
    + offset `op_Multiply` 2) (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRsi va_s0) inA_b (4 + offset) (va_get_mem_layout
    va_s0) Secret)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in let d0 = Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2)
    (va_get_mem_heaplet 0 va_sM) in let d1 = Vale.X64.Decls.buffer64_read dst_b (1 + offset
    `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in let d2 = Vale.X64.Decls.buffer64_read dst_b (2
    + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in let d3 = Vale.X64.Decls.buffer64_read
    dst_b (3 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in let d4 =
    Vale.X64.Decls.buffer64_read dst_b (4 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in
    let d5 = Vale.X64.Decls.buffer64_read dst_b (5 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in let d6 = Vale.X64.Decls.buffer64_read dst_b (6 + offset `op_Multiply` 2)
    (va_get_mem_heaplet 0 va_sM) in let d7 = Vale.X64.Decls.buffer64_read dst_b (7 + offset
    `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in Vale.Curve25519.Fast_defs.pow2_nine d0 d1 d2
    d3 d4 d5 d6 d7 (Vale.Curve25519.Fast_defs.bool_bit (Vale.X64.Decls.cf (va_get_flags va_sM))) ==
    Vale.Curve25519.Fast_defs.pow2_eight (Vale.Curve25519.Fast_defs.mul_nats a0 a0) (va_get_reg64
    rR8 va_s0) (Vale.Curve25519.Fast_defs.mul_nats a1 a1 + va_get_reg64 rR9 va_s0) (va_get_reg64
    rR10 va_s0) (Vale.Curve25519.Fast_defs.mul_nats a2 a2 + va_get_reg64 rR11 va_s0) (va_get_reg64
    rRbx va_s0) (Vale.Curve25519.Fast_defs.mul_nats a3 a3 + va_get_reg64 rR13 va_s0) (va_get_reg64
    rR14 va_s0) /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi
    va_sM) dst_b (8 + offset `op_Multiply` 2) (va_get_mem_layout va_sM) Secret /\
    Vale.X64.Decls.modifies_buffer_specific dst_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet
    0 va_sM) (0 + offset `op_Multiply` 2) (8 + offset `op_Multiply` 2 - 1)) /\ va_state_eq va_sM
    (va_update_flags va_sM (va_update_mem_heaplet 0 va_sM (va_update_reg64 rR15 va_sM
    (va_update_reg64 rR14 va_sM (va_update_reg64 rR13 va_sM (va_update_reg64 rRbx va_sM
    (va_update_reg64 rR11 va_sM (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM
    (va_update_reg64 rR8 va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx 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_sqr_part3 va_b0 va_s0 offset dst_b inA_b =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR15; va_Mod_reg64
    rR14; va_Mod_reg64 rR13; va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64
    rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRax; va_Mod_ok;
    va_Mod_mem] in
  let va_qc = va_qcode_Fast_sqr_part3 va_mods offset dst_b inA_b in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Fast_sqr_part3 offset) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 204 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_get_ok va_sM) /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 +
    offset) (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in label va_range1
    "***** POSTCONDITION NOT MET AT line 236 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (let d0 = Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 237 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (let d1 = Vale.X64.Decls.buffer64_read dst_b (1 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 238 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (let d2 = Vale.X64.Decls.buffer64_read dst_b (2 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 239 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (let d3 = Vale.X64.Decls.buffer64_read dst_b (3 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 240 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (let d4 = Vale.X64.Decls.buffer64_read dst_b (4 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 241 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (let d5 = Vale.X64.Decls.buffer64_read dst_b (5 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 242 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (let d6 = Vale.X64.Decls.buffer64_read dst_b (6 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 243 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (let d7 = Vale.X64.Decls.buffer64_read dst_b (7 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in label va_range1
    "***** POSTCONDITION NOT MET AT line 246 column 128 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (Vale.Curve25519.Fast_defs.pow2_nine d0 d1 d2 d3 d4 d5 d6 d7
    (Vale.Curve25519.Fast_defs.bool_bit (Vale.X64.Decls.cf (va_get_flags va_sM))) ==
    Vale.Curve25519.Fast_defs.pow2_eight (Vale.Curve25519.Fast_defs.mul_nats a0 a0) (va_get_reg64
    rR8 va_s0) (Vale.Curve25519.Fast_defs.mul_nats a1 a1 + va_get_reg64 rR9 va_s0) (va_get_reg64
    rR10 va_s0) (Vale.Curve25519.Fast_defs.mul_nats a2 a2 + va_get_reg64 rR11 va_s0) (va_get_reg64
    rRbx va_s0) (Vale.Curve25519.Fast_defs.mul_nats a3 a3 + va_get_reg64 rR13 va_s0) (va_get_reg64
    rR14 va_s0)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 248 column 80 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) dst_b (8
    + offset `op_Multiply` 2) (va_get_mem_layout va_sM) Secret) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 249 column 91 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (Vale.X64.Decls.modifies_buffer_specific dst_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet
    0 va_sM) (0 + offset `op_Multiply` 2) (8 + offset `op_Multiply` 2 - 1)))))))))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_heaplet 0; va_Mod_reg64 rR15; va_Mod_reg64 rR14;
    va_Mod_reg64 rR13; va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9;
    va_Mod_reg64 rR8; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRax; va_Mod_ok;
    va_Mod_mem]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Fast_sqr_part3 (offset:nat) (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 +
    offset) (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in adx_enabled /\ bmi2_enabled /\ (offset == 0
    \/ offset == 4) /\ Vale.X64.Decls.buffers_disjoint dst_b inA_b /\ va_get_reg64 rR14 va_s0 <= 2
    /\ Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) dst_b
    (8 + offset `op_Multiply` 2) (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRsi va_s0) inA_b (4 + offset) (va_get_mem_layout
    va_s0) Secret) /\ (forall (va_x_mem:vale_heap) (va_x_rax:nat64) (va_x_rcx:nat64)
    (va_x_rdx:nat64) (va_x_r8:nat64) (va_x_r9:nat64) (va_x_r10:nat64) (va_x_r11:nat64)
    (va_x_rbx:nat64) (va_x_r13:nat64) (va_x_r14:nat64) (va_x_r15: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 rR15 va_x_r15 (va_upd_reg64 rR14 va_x_r14 (va_upd_reg64 rR13 va_x_r13
    (va_upd_reg64 rRbx va_x_rbx (va_upd_reg64 rR11 va_x_r11 (va_upd_reg64 rR10 va_x_r10
    (va_upd_reg64 rR9 va_x_r9 (va_upd_reg64 rR8 va_x_r8 (va_upd_reg64 rRdx va_x_rdx (va_upd_reg64
    rRcx va_x_rcx (va_upd_reg64 rRax va_x_rax (va_upd_mem va_x_mem va_s0))))))))))))) in va_get_ok
    va_sM /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in let d0 = Vale.X64.Decls.buffer64_read dst_b (0 + offset `op_Multiply` 2)
    (va_get_mem_heaplet 0 va_sM) in let d1 = Vale.X64.Decls.buffer64_read dst_b (1 + offset
    `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in let d2 = Vale.X64.Decls.buffer64_read dst_b (2
    + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in let d3 = Vale.X64.Decls.buffer64_read
    dst_b (3 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in let d4 =
    Vale.X64.Decls.buffer64_read dst_b (4 + offset `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in
    let d5 = Vale.X64.Decls.buffer64_read dst_b (5 + offset `op_Multiply` 2) (va_get_mem_heaplet 0
    va_sM) in let d6 = Vale.X64.Decls.buffer64_read dst_b (6 + offset `op_Multiply` 2)
    (va_get_mem_heaplet 0 va_sM) in let d7 = Vale.X64.Decls.buffer64_read dst_b (7 + offset
    `op_Multiply` 2) (va_get_mem_heaplet 0 va_sM) in Vale.Curve25519.Fast_defs.pow2_nine d0 d1 d2
    d3 d4 d5 d6 d7 (Vale.Curve25519.Fast_defs.bool_bit (Vale.X64.Decls.cf (va_get_flags va_sM))) ==
    Vale.Curve25519.Fast_defs.pow2_eight (Vale.Curve25519.Fast_defs.mul_nats a0 a0) (va_get_reg64
    rR8 va_s0) (Vale.Curve25519.Fast_defs.mul_nats a1 a1 + va_get_reg64 rR9 va_s0) (va_get_reg64
    rR10 va_s0) (Vale.Curve25519.Fast_defs.mul_nats a2 a2 + va_get_reg64 rR11 va_s0) (va_get_reg64
    rRbx va_s0) (Vale.Curve25519.Fast_defs.mul_nats a3 a3 + va_get_reg64 rR13 va_s0) (va_get_reg64
    rR14 va_s0) /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi
    va_sM) dst_b (8 + offset `op_Multiply` 2) (va_get_mem_layout va_sM) Secret /\
    Vale.X64.Decls.modifies_buffer_specific dst_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet
    0 va_sM) (0 + offset `op_Multiply` 2) (8 + offset `op_Multiply` 2 - 1)) ==> va_k va_sM (())))


val va_wpProof_Fast_sqr_part3 : offset:nat -> 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_sqr_part3 offset dst_b inA_b va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Fast_sqr_part3 offset) ([va_Mod_flags;
    va_Mod_mem_heaplet 0; va_Mod_reg64 rR15; va_Mod_reg64 rR14; va_Mod_reg64 rR13; va_Mod_reg64
    rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64
    rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRax; va_Mod_mem]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Fast_sqr_part3 offset dst_b inA_b va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Fast_sqr_part3 (va_code_Fast_sqr_part3 offset) va_s0 offset 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
    rR15 va_sM (va_update_reg64 rR14 va_sM (va_update_reg64 rR13 va_sM (va_update_reg64 rRbx va_sM
    (va_update_reg64 rR11 va_sM (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM
    (va_update_reg64 rR8 va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx 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 rR15; va_Mod_reg64 rR14;
    va_Mod_reg64 rR13; va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9;
    va_Mod_reg64 rR8; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; 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_sqr_part3 (offset:nat) (dst_b:buffer64) (inA_b:buffer64) : (va_quickCode unit
val va_quick_Fast_sqr_part3 (offset: nat) (dst_b inA_b: buffer64)
    : (va_quickCode unit (va_code_Fast_sqr_part3 offset))
offset: Prims.nat -> dst_b: Vale.X64.Memory.buffer64 -> inA_b: Vale.X64.Memory.buffer64
  -> Vale.X64.QuickCode.va_quickCode Prims.unit
      (Vale.Curve25519.X64.FastSqr.va_code_Fast_sqr_part3 offset)