val point_double_1 (t0 t1 t2 t3 t4:felem) (p:point) : Stack unit
  (requires fun h ->
    live h t0 /\ live h t1 /\ live h t2 /\
    live h t3 /\ live h t4 /\ live h p /\
    LowStar.Monotonic.Buffer.all_disjoint
      [loc t0; loc t1; loc t2; loc t3; loc t4; loc p ] /\
    point_inv h p)
  (ensures fun h0 _ h1 -> modifies (loc t0 |+| loc t1 |+| loc t2 |+| loc t3 |+| loc t4) h0 h1 /\
    as_nat h1 t0 < S.prime /\ as_nat h1 t1 < S.prime /\
    as_nat h1 t2 < S.prime /\ as_nat h1 t3 < S.prime /\
    as_nat h1 t4 < S.prime /\
    (let x, y, z = from_mont_point (as_point_nat h0 p) in
    let t0_s = S.fmul x x in
    let t1_s = S.fmul y y in
    let t2_s = S.fmul z z in
    let t3_s = S.fmul x y in
    let t3_s = S.fadd t3_s t3_s in
    let t4_s = S.fmul y z in
    fmont_as_nat h1 t0 == t0_s /\ fmont_as_nat h1 t1 == t1_s /\
    fmont_as_nat h1 t2 == t2_s /\ fmont_as_nat h1 t3 == t3_s /\
    fmont_as_nat h1 t4 == t4_s))
let point_double_1 t0 t1 t2 t3 t4 p =
  let x, y, z = getx p, gety p, getz p in
  fsqr t0 x;
  fsqr t1 y;
  fsqr t2 z;
  fmul t3 x y;
  fdouble t3 t3;
  fmul t4 y z
val point_double_1 (t0 t1 t2 t3 t4:felem) (p:point) : Stack unit
  (requires fun h ->
    live h t0 /\ live h t1 /\ live h t2 /\
    live h t3 /\ live h t4 /\ live h p /\
    LowStar.Monotonic.Buffer.all_disjoint
      [loc t0; loc t1; loc t2; loc t3; loc t4; loc p ] /\
    point_inv h p)
  (ensures fun h0 _ h1 -> modifies (loc t0 |+| loc t1 |+| loc t2 |+| loc t3 |+| loc t4) h0 h1 /\
    as_nat h1 t0 < S.prime /\ as_nat h1 t1 < S.prime /\
    as_nat h1 t2 < S.prime /\ as_nat h1 t3 < S.prime /\
    as_nat h1 t4 < S.prime /\
    (let x, y, z = from_mont_point (as_point_nat h0 p) in
    let t0_s = S.fmul x x in
    let t1_s = S.fmul y y in
    let t2_s = S.fmul z z in
    let t3_s = S.fmul x y in
    let t3_s = S.fadd t3_s t3_s in
    let t4_s = S.fmul y z in
    fmont_as_nat h1 t0 == t0_s /\ fmont_as_nat h1 t1 == t1_s /\
    fmont_as_nat h1 t2 == t2_s /\ fmont_as_nat h1 t3 == t3_s /\
    fmont_as_nat h1 t4 == t4_s))
let point_double_1 t0 t1 t2 t3 t4 p =
let x, y, z = getx p, gety p, getz p in
fsqr t0 x;
fsqr t1 y;
fsqr t2 z;
fmul t3 x y;
fdouble t3 t3;
fmul t4 y z
Hacl.Impl.P256.PointDouble.fst.checked
Spec.P256.fst.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.P256.Field.fsti.checked Hacl.Impl.P256.Bignum.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.P256.PointDouble.fst
Hacl.Impl.P256.Bignum.felem Hacl.Impl.P256.Point.point Hacl.Impl.P256.Field.fmul Prims.unit Hacl.Impl.P256.Field.fdouble Hacl.Impl.P256.Field.fsqr FStar.Pervasives.Native.tuple3 FStar.Pervasives.Native.Mktuple3 Hacl.Impl.P256.Point.getz Hacl.Impl.P256.Point.gety Hacl.Impl.P256.Point.getx
module Hacl.Impl.P256.PointDouble

open FStar.Mul
open FStar.HyperStack.All
open FStar.HyperStack
module ST = FStar.HyperStack.ST

open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.P256.Bignum
open Hacl.Impl.P256.Field

module S = Spec.P256

#set-options "--z3rlimit 50 --ifuel 0 --fuel 0"

inline_for_extraction noextract
val point_double_1 (t0 t1 t2 t3 t4:felem) (p:point) : Stack unit
  (requires fun h ->
    live h t0 /\ live h t1 /\ live h t2 /\
    live h t3 /\ live h t4 /\ live h p /\
    LowStar.Monotonic.Buffer.all_disjoint
      [loc t0; loc t1; loc t2; loc t3; loc t4; loc p ] /\
    point_inv h p)
  (ensures fun h0 _ h1 -> modifies (loc t0 |+| loc t1 |+| loc t2 |+| loc t3 |+| loc t4) h0 h1 /\
    as_nat h1 t0 < S.prime /\ as_nat h1 t1 < S.prime /\
    as_nat h1 t2 < S.prime /\ as_nat h1 t3 < S.prime /\
    as_nat h1 t4 < S.prime /\
    (let x, y, z = from_mont_point (as_point_nat h0 p) in
    let t0_s = S.fmul x x in
    let t1_s = S.fmul y y in
    let t2_s = S.fmul z z in
    let t3_s = S.fmul x y in
    let t3_s = S.fadd t3_s t3_s in
    let t4_s = S.fmul y z in
    fmont_as_nat h1 t0 == t0_s /\ fmont_as_nat h1 t1 == t1_s /\
    fmont_as_nat h1 t2 == t2_s /\ fmont_as_nat h1 t3 == t3_s /\
    fmont_as_nat h1 t4 == t4_s))
val point_double_1 (t0 t1 t2 t3 t4:felem) (p:point) : Stack unit
  (requires fun h ->
    live h t0 /\ live h t1 /\ live h t2 /\
    live h t3 /\ live h t4 /\ live h p /\
    LowStar.Monotonic.Buffer.all_disjoint
      [loc t0; loc t1; loc t2; loc t3; loc t4; loc p ] /\
    point_inv h p)
  (ensures fun h0 _ h1 -> modifies (loc t0 |+| loc t1 |+| loc t2 |+| loc t3 |+| loc t4) h0 h1 /\
    as_nat h1 t0 < S.prime /\ as_nat h1 t1 < S.prime /\
    as_nat h1 t2 < S.prime /\ as_nat h1 t3 < S.prime /\
    as_nat h1 t4 < S.prime /\
    (let x, y, z = from_mont_point (as_point_nat h0 p) in
    let t0_s = S.fmul x x in
    let t1_s = S.fmul y y in
    let t2_s = S.fmul z z in
    let t3_s = S.fmul x y in
    let t3_s = S.fadd t3_s t3_s in
    let t4_s = S.fmul y z in
    fmont_as_nat h1 t0 == t0_s /\ fmont_as_nat h1 t1 == t1_s /\
    fmont_as_nat h1 t2 == t2_s /\ fmont_as_nat h1 t3 == t3_s /\
    fmont_as_nat h1 t4 == t4_s))

    t0: Hacl.Impl.P256.Bignum.felem ->
    t1: Hacl.Impl.P256.Bignum.felem ->
    t2: Hacl.Impl.P256.Bignum.felem ->
    t3: Hacl.Impl.P256.Bignum.felem ->
    t4: Hacl.Impl.P256.Bignum.felem ->
    p: Hacl.Impl.P256.Point.point
  -> FStar.HyperStack.ST.Stack Prims.unit