val uncompressedPointRepresentation_parser_kind (coordinate_length:coordinate_length_type): LP.parser_kind
val uncompressedPointRepresentation_parser_kind (coordinate_length:coordinate_length_type): LP.parser_kind
let uncompressedPointRepresentation_parser_kind (coordinate_length:coordinate_length_type) 
  = LP.and_then_kind
      constantByte_parser_kind
      (lbytes_pair_parser_kind coordinate_length)
module MiTLS.Format.UncompressedPointRepresentation
open MiTLS

open MiTLS.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
/
prims.fst.checked MiTLS.Format.Constants.fsti.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
MiTLS.Format.UncompressedPointRepresentation.fst
coordinate_length: MiTLS.Format.UncompressedPointRepresentation.coordinate_length_type
  -> LowParse.Spec.Base.parser_kind
MiTLS.Format.UncompressedPointRepresentation.coordinate_length_type LowParse.Spec.Combinators.and_then_kind MiTLS.Format.Constants.constantByte_parser_kind MiTLS.Format.UncompressedPointRepresentation.lbytes_pair_parser_kind LowParse.Spec.Base.parser_kind
let uncompressedPointRepresentation_parser_kind (coordinate_length: coordinate_length_type) =
  
LP.and_then_kind constantByte_parser_kind (lbytes_pair_parser_kind coordinate_length)