val uv_of_ucp (#n: coordinate_length_type) (x: uncompressedPointRepresentation n)
    : Tot (B.lbytes32 n * B.lbytes32 n)
let uv_of_ucp (#n:coordinate_length_type) (x:uncompressedPointRepresentation n)
  : Tot (B.lbytes32 n * B.lbytes32  n)
  = (x.x, x.y)
val uv_of_ucp (#n: coordinate_length_type) (x: uncompressedPointRepresentation n)
    : Tot (B.lbytes32 n * B.lbytes32 n)
let uv_of_ucp (#n: coordinate_length_type) (x: uncompressedPointRepresentation n)
    : Tot (B.lbytes32 n * B.lbytes32 n) =
(x.x, x.y)
Format.UncompressedPointRepresentation.fst.checked
prims.fst.checked LowParse.SLow.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked Format.Constants.fsti.checked
Format.UncompressedPointRepresentation.fst
Format.UncompressedPointRepresentation.coordinate_length_type Format.UncompressedPointRepresentation.uncompressedPointRepresentation FStar.Pervasives.Native.Mktuple2 FStar.Bytes.lbytes32 Format.UncompressedPointRepresentation.__proj__MkuncompressedPointRepresentation__item__x Format.UncompressedPointRepresentation.__proj__MkuncompressedPointRepresentation__item__y FStar.Pervasives.Native.tuple2
module Format.UncompressedPointRepresentation

open Format.Constants

module B = FStar.Bytes
module U32 = FStar.UInt32
module LP = LowParse.SLow

unfold type is_injective (#a:Type) (#b:Type) (f:a -> b) 
  = forall x y . f x == f y ==> x == y
 
unfold type is_injective_2 (#a:Type) (#b:Type) (f:a -> b) (x:a) (y:a)
  = f x == f y ==> x == y

(* Types *)

private unfold
type lbytes_pair (coordinate_length:coordinate_length_type) 
  = B.lbytes32 coordinate_length * B.lbytes32 coordinate_length
  // = (p:(B.lbytes32 coordinate_length * B.lbytes32 coordinate_length)
  //       {U32.(coordinate_length +^ coordinate_length <^ 512ul) /\
  //       U32.v coordinate_length + U32.v coordinate_length < 512 /\
  //       B.length (fst p) + B.length (snd p) < pow2 32 /\
  //       UInt.fits (B.length (fst p) + B.length (snd p)) 32})


(* Parsers *)

private
inline_for_extraction
let lbytes_pair_parser_kind (coordinate_length:coordinate_length_type)
  : LP.parser_kind
  = let l = (UInt32.v coordinate_length) in
    LP.and_then_kind 
      (LP.total_constant_size_parser_kind l)
      (LP.total_constant_size_parser_kind l)

private
inline_for_extraction
let lbytes_pair_parser (coordinate_length:coordinate_length_type)
  : LP.parser (lbytes_pair_parser_kind coordinate_length) (lbytes_pair coordinate_length)
  = let l = U32.v coordinate_length in
    LP.nondep_then
      (LP.parse_flbytes l)
      (LP.parse_flbytes l)

#reset-options "--using_facts_from '* -FStar.Reflection -FStar.Tactics' --max_fuel 16 --initial_fuel 16 --max_ifuel 16 --initial_ifuel 16"
private
inline_for_extraction
let lbytes_pair_parser32 (coordinate_length:coordinate_length_type)
  : LP.parser32 (lbytes_pair_parser coordinate_length) 
  = [@inline_let]
    let l = UInt32.v coordinate_length in
    LP.parse32_nondep_then
      (LP.parse32_flbytes l coordinate_length)
      (LP.parse32_flbytes l coordinate_length)
#reset-options

inline_for_extraction
let uncompressedPointRepresentation_parser_kind (coordinate_length:coordinate_length_type) 
  = LP.and_then_kind
      constantByte_parser_kind
      (lbytes_pair_parser_kind coordinate_length)

private
inline_for_extraction
let ucp_of_uv (#n:coordinate_length_type) (p:(B.lbytes32 n) * (B.lbytes32 n))
  : uncompressedPointRepresentation n
  = { legacy_form = 4uy; x = (fst p); y = (snd p) }

private
inline_for_extraction
let uv_of_ucp (#n:coordinate_length_type) (x:uncompressedPointRepresentation n)
val uv_of_ucp (#n: coordinate_length_type) (x: uncompressedPointRepresentation n)
    : Tot (B.lbytes32 n * B.lbytes32 n)
x: Format.UncompressedPointRepresentation.uncompressedPointRepresentation n
  -> FStar.Bytes.lbytes32 n * FStar.Bytes.lbytes32 n