val from_mont_point (a: tuple3 nat nat nat) : S.proj_point
let from_mont_point (a:tuple3 nat nat nat) : S.proj_point =
  let x, y, z = a in SM.from_mont x, SM.from_mont y, SM.from_mont z
val from_mont_point (a: tuple3 nat nat nat) : S.proj_point
let from_mont_point (a: tuple3 nat nat nat) : S.proj_point =
let x, y, z = a in
SM.from_mont x, SM.from_mont y, SM.from_mont z
Hacl.Impl.P256.Point.fsti.checked
Spec.P256.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.P256.Montgomery.fsti.checked Hacl.Spec.Bignum.Definitions.fst.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.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.P256.Point.fsti
FStar.Pervasives.Native.tuple3 Prims.nat FStar.Pervasives.Native.Mktuple3 Hacl.Spec.P256.Montgomery.from_mont Spec.P256.PointOps.proj_point
module Hacl.Impl.P256.Point

open FStar.Mul
open FStar.HyperStack.All
open FStar.HyperStack

open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.P256.Bignum

module S = Spec.P256
module SM = Hacl.Spec.P256.Montgomery
module BD = Hacl.Spec.Bignum.Definitions
module LSeq = Lib.Sequence

#set-options "--z3rlimit 30 --fuel 0 --ifuel 0"
val from_mont_point (a: tuple3 nat nat nat) : S.proj_point
a: ((Prims.nat * Prims.nat) * Prims.nat) -> Spec.P256.PointOps.proj_point