val va_qcode_Fast_sqr_part1 (va_mods: va_mods_t) (offset: nat) (inA_b: buffer64)
    : (va_quickCode unit (va_code_Fast_sqr_part1 offset))
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_qcode_Fast_sqr_part1 (va_mods: va_mods_t) (offset: nat) (inA_b: buffer64)
    : (va_quickCode unit (va_code_Fast_sqr_part1 offset))
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
                                                                                                                                                                                                                                                                  (
                                                                                                                                                                                                                                                                    ()
                                                                                                                                                                                                                                                                  )

                                                                                                                                                                                                                                                              )

                                                                                                                                                                                                                                                          )

                                                                                                                                                                                                                                                      )

                                                                                                                                                                                                                                                  )

                                                                                                                                                                                                                                              )

                                                                                                                                                                                                                                        )

                                                                                                                                                                                                                                    )

                                                                                                                                                                                                                                )

                                                                                                                                                                                                                            )

                                                                                                                                                                                                                        )

                                                                                                                                                                                                                    )

                                                                                                                                                                                                                )

                                                                                                                                                                                                            )

                                                                                                                                                                                                        )

                                                                                                                                                                                                    )

                                                                                                                                                                                                )

                                                                                                                                                                                            )

                                                                                                                                                                                      )

                                                                                                                                                                                  )

                                                                                                                                                                              )

                                                                                                                                                                          )

                                                                                                                                                                      )

                                                                                                                                                                  )

                                                                                                                                                              )

                                                                                                                                                        )

                                                                                                                                                    )

                                                                                                                                                )

                                                                                                                                            )

                                                                                                                                        )

                                                                                                                                    )

                                                                                                                                )

                                                                                                                            )

                                                                                                                        )

                                                                                                                    )

                                                                                                                )

                                                                                                          )

                                                                                                      )

                                                                                                  ))
                                                                                          ))))))))))
                                                ))))))))))))
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
Vale.X64.QuickCode.va_mods_t Prims.nat Vale.X64.Memory.buffer64 Vale.X64.QuickCodes.qblock Prims.unit Prims.Cons Vale.X64.Decls.va_code Vale.X64.InsBasic.va_code_NoNewline Vale.X64.InsMem.va_code_Load64_buffer Vale.X64.Decls.va_op_heaplet_mem_heaplet Vale.X64.Decls.va_op_dst_opr64_reg64 Vale.X64.Machine_s.rRdx Vale.X64.Decls.va_op_reg_opr64_reg64 Vale.X64.Machine_s.rRsi Prims.op_Addition Prims.op_Multiply Vale.Arch.HeapTypes_s.Secret Vale.X64.InsBasic.va_code_Space Vale.X64.InsBasic.va_code_Comment Vale.X64.InsMem.va_code_Mem64_lemma Vale.X64.InsBasic.va_code_Mulx64 Vale.X64.Machine_s.rR14 Vale.X64.Machine_s.rR8 Vale.X64.Decls.va_opr_code_Mem64 Vale.X64.Decls.va_op_reg64_reg64 Vale.X64.InsBasic.va_code_Xor64 Vale.X64.Machine_s.rR15 Vale.X64.Decls.va_op_opr64_reg64 Vale.X64.Machine_s.rR10 Vale.X64.Machine_s.rR9 Vale.X64.InsBasic.va_code_Adcx64Wrap Vale.X64.Machine_s.rRcx Vale.X64.Machine_s.rRax Vale.X64.Machine_s.rRbx Vale.X64.Machine_s.rR11 Vale.X64.Machine_s.rR13 Vale.X64.InsBasic.va_code_Mov64 Vale.X64.Decls.va_const_opr64 Prims.Nil Vale.X64.Machine_s.precode Vale.X64.Decls.ins Vale.X64.Decls.ocmp Vale.X64.Decls.va_state Vale.X64.QuickCodes.va_qPURE Prims.pure_post Prims.l_and Prims.l_True Prims.l_Forall Prims.l_imp Vale.Def.Words_s.nat32 Prims.eq2 Vale.Def.Types_s.ixor Prims.int Vale.Def.Words_s.nat64 Vale.X64.QuickCodes.va_range1 Vale.Arch.Types.xor_lemmas Vale.X64.QuickCodes.va_QSeq Vale.X64.InsBasic.va_quick_NoNewline Vale.X64.InsMem.va_quick_Load64_buffer Vale.X64.InsBasic.va_quick_Space Vale.X64.InsBasic.va_quick_Comment Vale.X64.InsMem.va_quick_Mem64_lemma Vale.X64.QuickCodes.va_QBind Vale.X64.InsBasic.va_quick_Mulx64 Prims.b2t Prims.op_LessThan Prims.op_Subtraction Prims.l_or Prims.op_LessThanOrEqual Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds Vale.X64.InsBasic.va_quick_Xor64 Vale.X64.InsBasic.va_quick_Adcx64Wrap Vale.X64.InsBasic.va_quick_Mov64 Vale.X64.QuickCodes.va_QEmpty Vale.X64.Decls.va_get_reg64 Vale.X64.QuickCodes.quickCodes Vale.Curve25519.Fast_defs.pow2_four Vale.X64.Decls.buffer64_read Vale.X64.Decls.va_get_mem_heaplet Vale.X64.State.vale_state Vale.X64.QuickCode.va_quickCode Vale.Curve25519.X64.FastSqr.va_code_Fast_sqr_part1
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
val va_qcode_Fast_sqr_part1 (va_mods: va_mods_t) (offset: nat) (inA_b: buffer64)
    : (va_quickCode unit (va_code_Fast_sqr_part1 offset))
va_mods: Vale.X64.QuickCode.va_mods_t -> offset: Prims.nat -> inA_b: Vale.X64.Memory.buffer64
  -> Vale.X64.QuickCode.va_quickCode Prims.unit
      (Vale.Curve25519.X64.FastSqr.va_code_Fast_sqr_part1 offset)