val va_lemma_Fast_sqr_part1 : va_b0:va_code -> va_s0:va_state -> offset:nat -> inA_b:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Fast_sqr_part1 offset) va_s0 /\ va_get_ok va_s0 /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in adx_enabled /\ bmi2_enabled /\ (offset == 0 \/ offset == 4) /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRsi va_s0) inA_b (4
    + offset) (va_get_mem_layout va_s0) Secret)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in Vale.Curve25519.Fast_defs.pow2_six (va_get_reg64 rR8 va_sM) (va_get_reg64 rR9 va_sM)
    (va_get_reg64 rR10 va_sM) (va_get_reg64 rR11 va_sM) (va_get_reg64 rRbx va_sM) (va_get_reg64
    rR13 va_sM) == Vale.Curve25519.Fast_defs.pow2_five (Vale.Curve25519.Fast_defs.mul_nats a0 a1)
    (Vale.Curve25519.Fast_defs.mul_nats a0 a2) (Vale.Curve25519.Fast_defs.mul_nats a0 a3)
    (Vale.Curve25519.Fast_defs.mul_nats a1 a3) (Vale.Curve25519.Fast_defs.mul_nats a2 a3) /\
    va_mul_nat pow2_64 (va_get_reg64 rRcx va_sM) + va_get_reg64 rRax va_sM == va_mul_nat a1 a2 /\
    va_get_reg64 rR14 va_sM == 0) /\ va_state_eq va_sM (va_update_flags va_sM (va_update_reg64 rR15
    va_sM (va_update_reg64 rR14 va_sM (va_update_reg64 rR13 va_sM (va_update_reg64 rRbx va_sM
    (va_update_reg64 rR11 va_sM (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM
    (va_update_reg64 rR8 va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRax va_sM (va_update_ok va_sM va_s0)))))))))))))))
let va_lemma_Fast_sqr_part1 va_b0 va_s0 offset inA_b =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_reg64 rR15; va_Mod_reg64 rR14; va_Mod_reg64 rR13;
    va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8;
    va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRax; va_Mod_ok] in
  let va_qc = va_qcode_Fast_sqr_part1 va_mods offset inA_b in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Fast_sqr_part1 offset) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 55 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_get_ok va_sM) /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 +
    offset) (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (2 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (3 + offset) (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) =
    Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in label va_range1
    "***** POSTCONDITION NOT MET AT line 82 column 103 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (Vale.Curve25519.Fast_defs.pow2_six (va_get_reg64 rR8 va_sM) (va_get_reg64 rR9 va_sM)
    (va_get_reg64 rR10 va_sM) (va_get_reg64 rR11 va_sM) (va_get_reg64 rRbx va_sM) (va_get_reg64
    rR13 va_sM) == Vale.Curve25519.Fast_defs.pow2_five (Vale.Curve25519.Fast_defs.mul_nats a0 a1)
    (Vale.Curve25519.Fast_defs.mul_nats a0 a2) (Vale.Curve25519.Fast_defs.mul_nats a0 a3)
    (Vale.Curve25519.Fast_defs.mul_nats a1 a3) (Vale.Curve25519.Fast_defs.mul_nats a2 a3)) /\ label
    va_range1
    "***** POSTCONDITION NOT MET AT line 84 column 39 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_mul_nat pow2_64 (va_get_reg64 rRcx va_sM) + va_get_reg64 rRax va_sM == va_mul_nat a1 a2) /\
    label va_range1
    "***** POSTCONDITION NOT MET AT line 86 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_get_reg64 rR14 va_sM == 0))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_reg64 rR15; va_Mod_reg64 rR14; va_Mod_reg64 rR13;
    va_Mod_reg64 rRbx; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8;
    va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRax; va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)
val va_lemma_Fast_sqr_part1 : va_b0:va_code -> va_s0:va_state -> offset:nat -> inA_b:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Fast_sqr_part1 offset) va_s0 /\ va_get_ok va_s0 /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in adx_enabled /\ bmi2_enabled /\ (offset == 0 \/ offset == 4) /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRsi va_s0) inA_b (4
    + offset) (va_get_mem_layout va_s0) Secret)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in Vale.Curve25519.Fast_defs.pow2_six (va_get_reg64 rR8 va_sM) (va_get_reg64 rR9 va_sM)
    (va_get_reg64 rR10 va_sM) (va_get_reg64 rR11 va_sM) (va_get_reg64 rRbx va_sM) (va_get_reg64
    rR13 va_sM) == Vale.Curve25519.Fast_defs.pow2_five (Vale.Curve25519.Fast_defs.mul_nats a0 a1)
    (Vale.Curve25519.Fast_defs.mul_nats a0 a2) (Vale.Curve25519.Fast_defs.mul_nats a0 a3)
    (Vale.Curve25519.Fast_defs.mul_nats a1 a3) (Vale.Curve25519.Fast_defs.mul_nats a2 a3) /\
    va_mul_nat pow2_64 (va_get_reg64 rRcx va_sM) + va_get_reg64 rRax va_sM == va_mul_nat a1 a2 /\
    va_get_reg64 rR14 va_sM == 0) /\ va_state_eq va_sM (va_update_flags va_sM (va_update_reg64 rR15
    va_sM (va_update_reg64 rR14 va_sM (va_update_reg64 rR13 va_sM (va_update_reg64 rRbx va_sM
    (va_update_reg64 rR11 va_sM (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM
    (va_update_reg64 rR8 va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRax va_sM (va_update_ok va_sM va_s0)))))))))))))))
let va_lemma_Fast_sqr_part1 va_b0 va_s0 offset inA_b =
let va_mods:va_mods_t =
  [
    va_Mod_flags; va_Mod_reg64 rR15; va_Mod_reg64 rR14; va_Mod_reg64 rR13; va_Mod_reg64 rRbx;
    va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx;
    va_Mod_reg64 rRcx; va_Mod_reg64 rRax; va_Mod_ok
  ]
in
let va_qc = va_qcode_Fast_sqr_part1 va_mods offset inA_b in
let va_sM, va_fM, va_g =
  va_wp_sound_code_norm (va_code_Fast_sqr_part1 offset)
    va_qc
    va_s0
    (fun va_s0 va_sM va_g ->
        let () = va_g in
        label va_range1
          "***** POSTCONDITION NOT MET AT line 55 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
          (va_get_ok va_sM) /\
        (let a0:Vale.Def.Types_s.nat64 =
            Vale.X64.Decls.buffer64_read inA_b (0 + offset) (va_get_mem_heaplet 0 va_s0)
          in
          let a1:Vale.Def.Types_s.nat64 =
            Vale.X64.Decls.buffer64_read inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0)
          in
          let a2:Vale.Def.Types_s.nat64 =
            Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0)
          in
          let a3:Vale.Def.Types_s.nat64 =
            Vale.X64.Decls.buffer64_read inA_b (3 + offset) (va_get_mem_heaplet 0 va_s0)
          in
          let a:Prims.nat = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in
          label va_range1
            "***** POSTCONDITION NOT MET AT line 82 column 103 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
            (Vale.Curve25519.Fast_defs.pow2_six (va_get_reg64 rR8 va_sM)
                (va_get_reg64 rR9 va_sM)
                (va_get_reg64 rR10 va_sM)
                (va_get_reg64 rR11 va_sM)
                (va_get_reg64 rRbx va_sM)
                (va_get_reg64 rR13 va_sM) ==
              Vale.Curve25519.Fast_defs.pow2_five (Vale.Curve25519.Fast_defs.mul_nats a0 a1)
                (Vale.Curve25519.Fast_defs.mul_nats a0 a2)
                (Vale.Curve25519.Fast_defs.mul_nats a0 a3)
                (Vale.Curve25519.Fast_defs.mul_nats a1 a3)
                (Vale.Curve25519.Fast_defs.mul_nats a2 a3)) /\
          label va_range1
            "***** POSTCONDITION NOT MET AT line 84 column 39 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
            (va_mul_nat pow2_64 (va_get_reg64 rRcx va_sM) + va_get_reg64 rRax va_sM ==
              va_mul_nat a1 a2) /\
          label va_range1
            "***** POSTCONDITION NOT MET AT line 86 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
            (va_get_reg64 rR14 va_sM == 0)))
in
assert_norm (va_qc.mods == va_mods);
va_lemma_norm_mods ([
      va_Mod_flags; va_Mod_reg64 rR15; va_Mod_reg64 rR14; va_Mod_reg64 rR13; va_Mod_reg64 rRbx;
      va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rR8; va_Mod_reg64 rRdx;
      va_Mod_reg64 rRcx; va_Mod_reg64 rRax; va_Mod_ok
    ])
  va_sM
  va_s0;
(va_sM, va_fM)
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.Decls.va_code Vale.X64.Decls.va_state Prims.nat Vale.X64.Memory.buffer64 Vale.X64.QuickCodes.fuel Prims.unit FStar.Pervasives.Native.Mktuple2 Vale.X64.Decls.va_fuel Vale.X64.QuickCode.va_lemma_norm_mods Prims.Cons Vale.X64.QuickCode.mod_t Vale.X64.QuickCode.va_Mod_flags Vale.X64.QuickCode.va_Mod_reg64 Vale.X64.Machine_s.rR15 Vale.X64.Machine_s.rR14 Vale.X64.Machine_s.rR13 Vale.X64.Machine_s.rRbx Vale.X64.Machine_s.rR11 Vale.X64.Machine_s.rR10 Vale.X64.Machine_s.rR9 Vale.X64.Machine_s.rR8 Vale.X64.Machine_s.rRdx Vale.X64.Machine_s.rRcx Vale.X64.Machine_s.rRax Vale.X64.QuickCode.va_Mod_ok Prims.Nil FStar.Pervasives.assert_norm Prims.eq2 Prims.list Vale.X64.QuickCode.__proj__QProc__item__mods Vale.Curve25519.X64.FastSqr.va_code_Fast_sqr_part1 FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.tuple3 Vale.X64.State.vale_state Vale.X64.QuickCodes.va_wp_sound_code_norm Prims.l_and Vale.X64.QuickCodes.label Vale.X64.QuickCodes.va_range1 Prims.b2t Vale.X64.Decls.va_get_ok Vale.Curve25519.Fast_defs.pow2_six Vale.X64.Decls.va_get_reg64 Vale.Curve25519.Fast_defs.pow2_five Vale.Curve25519.Fast_defs.mul_nats Prims.int Prims.op_Addition Vale.X64.Decls.va_mul_nat Vale.X64.Machine_s.pow2_64 Vale.Curve25519.Fast_defs.pow2_four Vale.Def.Words_s.nat64 Vale.X64.Decls.buffer64_read Vale.X64.Decls.va_get_mem_heaplet Vale.X64.QuickCode.quickCode Vale.Curve25519.X64.FastSqr.va_qcode_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
  (va_code_Fast_sqr_part1 offset)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2
    a3 in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 88 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Arch.Types.xor_lemmas ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 101 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 102 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (0 + offset `op_Multiply` 8) Secret inA_b (0 + offset)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 103 column 134 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 35) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 103 column 147 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[0]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 105 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 106 column 27 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (8 + offset
    `op_Multiply` 8) inA_b (1 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 106 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rR14) (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (8 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg78:Vale.Def.Types_s.nat64) = va_get_reg64 rR8 va_s in let
    (va_arg77:Vale.Def.Types_s.nat64) = va_get_reg64 rR14 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 106 column 122 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg77 va_arg78 a0
    a1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 106 column 148 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 106 column 158 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Xor64 (va_op_dst_opr64_reg64 rR15) (va_op_opr64_reg64 rR15)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 106 column 175 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 106 column 187 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[1]*f[0]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 108 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 109 column 27 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (16 + offset
    `op_Multiply` 8) inA_b (2 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 109 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rR10) (va_op_dst_opr64_reg64 rR9) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (16 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg76:Vale.Def.Types_s.nat64) = va_get_reg64 rR9 va_s in let
    (va_arg75:Vale.Def.Types_s.nat64) = va_get_reg64 rR10 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 109 column 123 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg75 va_arg76 a0
    a2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 109 column 148 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 109 column 163 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR9) (va_op_opr64_reg64 rR14)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 109 column 180 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 109 column 192 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[2]*f[0]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 111 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 112 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (24 + offset
    `op_Multiply` 8) inA_b (3 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 112 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rRcx) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (24 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg74:Vale.Def.Types_s.nat64) = va_get_reg64 rRax va_s in let
    (va_arg73:Vale.Def.Types_s.nat64) = va_get_reg64 rRcx va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 112 column 124 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg73 va_arg74 a0
    a3) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 112 column 154 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 112 column 168 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 112 column 187 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[3]*f[0]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 114 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 115 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (24 + offset `op_Multiply` 8) Secret inA_b (3 + offset)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 116 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 34) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 116 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[3]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 118 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 119 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (8 + offset
    `op_Multiply` 8) inA_b (1 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 119 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rRbx) (va_op_dst_opr64_reg64 rR11) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (8 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg72:Vale.Def.Types_s.nat64) = va_get_reg64 rR11 va_s in let
    (va_arg71:Vale.Def.Types_s.nat64) = va_get_reg64 rRbx va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 119 column 123 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg71 va_arg72 a3
    a1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 119 column 148 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 119 column 163 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR11) (va_op_opr64_reg64 rRcx)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 119 column 182 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[1]*f[3]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 121 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 122 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (16 + offset
    `op_Multiply` 8) inA_b (2 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 122 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rR13) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (16 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg70:Vale.Def.Types_s.nat64) = va_get_reg64 rRax va_s in let
    (va_arg69:Vale.Def.Types_s.nat64) = va_get_reg64 rR13 va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 122 column 124 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg69 va_arg70 a3
    a2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 122 column 154 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 122 column 168 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 122 column 187 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[2]*f[3]"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 124 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 125 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRdx)
    (va_op_reg_opr64_reg64 rRsi) (8 + offset `op_Multiply` 8) Secret inA_b (1 + offset)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 126 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 9) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 126 column 25 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Adcx64Wrap (va_op_dst_opr64_reg64 rR13) (va_op_opr64_reg64 rR15)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 126 column 44 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f1"
    ) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 130 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 131 column 27 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mem64_lemma (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (16 + offset
    `op_Multiply` 8) inA_b (2 + offset) Secret) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 131 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mulx64 (va_op_dst_opr64_reg64 rRcx) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) (16 + offset `op_Multiply` 8) Secret))
    (fun (va_s:va_state) _ -> let (va_arg68:Vale.Def.Types_s.nat64) = va_get_reg64 rRax va_s in let
    (va_arg67:Vale.Def.Types_s.nat64) = va_get_reg64 rRcx va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 131 column 121 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (fun (_:unit) -> Vale.Curve25519.Fast_lemmas_external.lemma_prod_bounds va_arg67 va_arg68 a1
    a2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 131 column 150 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_NoNewline ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 131 column 159 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Mov64 (va_op_dst_opr64_reg64 rR14) (va_const_opr64 0)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 131 column 174 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Space 4) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 131 column 186 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/Vale.Curve25519.X64.FastSqr.vaf *****"
    (va_quick_Comment
    "f[2]*f[1]") (va_QEmpty (()))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))


val va_lemma_Fast_sqr_part1 : va_b0:va_code -> va_s0:va_state -> offset:nat -> inA_b:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Fast_sqr_part1 offset) va_s0 /\ va_get_ok va_s0 /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in adx_enabled /\ bmi2_enabled /\ (offset == 0 \/ offset == 4) /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRsi va_s0) inA_b (4
    + offset) (va_get_mem_layout va_s0) Secret)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in Vale.Curve25519.Fast_defs.pow2_six (va_get_reg64 rR8 va_sM) (va_get_reg64 rR9 va_sM)
    (va_get_reg64 rR10 va_sM) (va_get_reg64 rR11 va_sM) (va_get_reg64 rRbx va_sM) (va_get_reg64
    rR13 va_sM) == Vale.Curve25519.Fast_defs.pow2_five (Vale.Curve25519.Fast_defs.mul_nats a0 a1)
    (Vale.Curve25519.Fast_defs.mul_nats a0 a2) (Vale.Curve25519.Fast_defs.mul_nats a0 a3)
    (Vale.Curve25519.Fast_defs.mul_nats a1 a3) (Vale.Curve25519.Fast_defs.mul_nats a2 a3) /\
    va_mul_nat pow2_64 (va_get_reg64 rRcx va_sM) + va_get_reg64 rRax va_sM == va_mul_nat a1 a2 /\
    va_get_reg64 rR14 va_sM == 0) /\ va_state_eq va_sM (va_update_flags va_sM (va_update_reg64 rR15
    va_sM (va_update_reg64 rR14 va_sM (va_update_reg64 rR13 va_sM (va_update_reg64 rRbx va_sM
    (va_update_reg64 rR11 va_sM (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM
    (va_update_reg64 rR8 va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRax va_sM (va_update_ok va_sM va_s0)))))))))))))))
val va_lemma_Fast_sqr_part1 : va_b0:va_code -> va_s0:va_state -> offset:nat -> inA_b:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Fast_sqr_part1 offset) va_s0 /\ va_get_ok va_s0 /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in adx_enabled /\ bmi2_enabled /\ (offset == 0 \/ offset == 4) /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRsi va_s0) inA_b (4
    + offset) (va_get_mem_layout va_s0) Secret)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (0 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read
    inA_b (1 + offset) (va_get_mem_heaplet 0 va_s0) in let (a2:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read inA_b (2 + offset) (va_get_mem_heaplet 0 va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b (3 + offset)
    (va_get_mem_heaplet 0 va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1
    a2 a3 in Vale.Curve25519.Fast_defs.pow2_six (va_get_reg64 rR8 va_sM) (va_get_reg64 rR9 va_sM)
    (va_get_reg64 rR10 va_sM) (va_get_reg64 rR11 va_sM) (va_get_reg64 rRbx va_sM) (va_get_reg64
    rR13 va_sM) == Vale.Curve25519.Fast_defs.pow2_five (Vale.Curve25519.Fast_defs.mul_nats a0 a1)
    (Vale.Curve25519.Fast_defs.mul_nats a0 a2) (Vale.Curve25519.Fast_defs.mul_nats a0 a3)
    (Vale.Curve25519.Fast_defs.mul_nats a1 a3) (Vale.Curve25519.Fast_defs.mul_nats a2 a3) /\
    va_mul_nat pow2_64 (va_get_reg64 rRcx va_sM) + va_get_reg64 rRax va_sM == va_mul_nat a1 a2 /\
    va_get_reg64 rR14 va_sM == 0) /\ va_state_eq va_sM (va_update_flags va_sM (va_update_reg64 rR15
    va_sM (va_update_reg64 rR14 va_sM (va_update_reg64 rR13 va_sM (va_update_reg64 rRbx va_sM
    (va_update_reg64 rR11 va_sM (va_update_reg64 rR10 va_sM (va_update_reg64 rR9 va_sM
    (va_update_reg64 rR8 va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRax va_sM (va_update_ok va_sM va_s0)))))))))))))))

    va_b0: Vale.X64.Decls.va_code ->
    va_s0: Vale.X64.Decls.va_state ->
    offset: Prims.nat ->
    inA_b: Vale.X64.Memory.buffer64
  -> Prims.Ghost (Vale.X64.Decls.va_state * Vale.X64.Decls.va_fuel)