val uncompressedPointRepresentation_serializer (coordinate_length:coordinate_length_type) 
  : LP.serializer (uncompressedPointRepresentation_parser coordinate_length)
val uncompressedPointRepresentation_serializer (coordinate_length:coordinate_length_type) 
  : LP.serializer (uncompressedPointRepresentation_parser coordinate_length)
let uncompressedPointRepresentation_serializer (coordinate_length:coordinate_length_type) 
  : LP.serializer (uncompressedPointRepresentation_parser coordinate_length)
  = let l = coordinate_length in
    lemma_ucp_of_cuv_is_injective #l;
    lemma_ucp_of_cuv_of_ucp #l;
    LP.serialize_synth
      (LP.nondep_then (constantByte_parser 4uy) (lbytes_pair_parser l))
      ucp_of_cuv
      (LP.serialize_nondep_then 
        (constantByte_serializer 4uy) 
        (lbytes_pair_serializer l))
      cuv_of_ucp
      ()
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

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)
  : Tot (B.lbytes32 n * B.lbytes32  n)
  = (x.x, x.y)

#reset-options "--using_facts_from '* -LowParse -FStar.Reflection -FStar.Tactics' --max_fuel 16 --initial_fuel 16 --max_ifuel 16 --initial_ifuel 16"
let lemma_ucp_of_uv_is_injective #l
  : Lemma (is_injective (ucp_of_uv #l))
  = ()

let lemma_ucp_of_uv_of_ucp #l 
  : Lemma (forall x . ucp_of_uv #l (uv_of_ucp #l x) == x)
  = lemma_ucp_of_uv_is_injective #l
#reset-options

let ucp_of_cuv #l (cuv:constantByte 4uy * lbytes_pair l): Tot (ucp:uncompressedPointRepresentation l) = let c, uv = cuv in ucp_of_uv uv
let cuv_of_ucp #l (ucp:uncompressedPointRepresentation l): Tot (cuv:constantByte 4uy * lbytes_pair l) = 4uy, (ucp.x, ucp.y)

#reset-options "--using_facts_from '* -LowParse -FStar.Reflection -FStar.Tactics' --max_fuel 16 --initial_fuel 16 --max_ifuel 16 --initial_ifuel 16"
let lemma_ucp_of_cuv_is_injective #l
  : Lemma (is_injective (ucp_of_cuv #l))
  = ()

let lemma_ucp_of_cuv_of_ucp #l 
  : Lemma (forall x . ucp_of_cuv #l (cuv_of_ucp #l x) == x)
  = lemma_ucp_of_cuv_is_injective #l
#reset-options


let uncompressedPointRepresentation_parser (coordinate_length:coordinate_length_type)
  : LP.parser (uncompressedPointRepresentation_parser_kind coordinate_length) (uncompressedPointRepresentation coordinate_length) 
  = LP.parse_synth
      (LP.nondep_then (constantByte_parser 4uy) (lbytes_pair_parser coordinate_length))
      ucp_of_cuv

inline_for_extraction
let uncompressedPointRepresentation_parser32 (coordinate_length:coordinate_length_type)
  : LP.parser32 (uncompressedPointRepresentation_parser coordinate_length)
  = LP.parse32_synth
      (LP.nondep_then (constantByte_parser 4uy) (lbytes_pair_parser coordinate_length))
      ucp_of_cuv
      (fun x -> ucp_of_cuv x)
      (LP.parse32_nondep_then (constantByte_parser32 4uy) (lbytes_pair_parser32 coordinate_length))
      ()


(* Serializers *)

#reset-options "--using_facts_from '* -FStar.Reflection -FStar.Tactics' --max_fuel 16 --initial_fuel 16 --max_ifuel 16 --initial_ifuel 16 --z3rlimit 10"
private
let lbytes_pair_serializer (coordinate_length:coordinate_length_type)
  : LP.serializer (lbytes_pair_parser coordinate_length) 
  = let l = U32.v coordinate_length in
    let p = LP.parse_flbytes l in
    let s = LP.serialize_flbytes l in
    LP.serialize_nondep_then s s

#reset-options "--using_facts_from '* -FStar.Reflection -FStar.Tactics' --max_fuel 16 --initial_fuel 16 --max_ifuel 16 --initial_ifuel 16 --z3rlimit 10"
private
inline_for_extraction
let lbytes_pair_serializer32 (coordinate_length:coordinate_length_type)
  : LP.serializer32 (lbytes_pair_serializer coordinate_length) 
  = [@inline_let]
    let l = U32.v coordinate_length in
    LP.serialize32_nondep_then
      (LP.serialize32_flbytes l)
      (LP.serialize32_flbytes l)
#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.serializer (MiTLS.Format.UncompressedPointRepresentation.uncompressedPointRepresentation_parser
          coordinate_length)
MiTLS.Format.UncompressedPointRepresentation.coordinate_length_type LowParse.Spec.Combinators.serialize_synth LowParse.Spec.Combinators.and_then_kind MiTLS.Format.Constants.constantByte_parser_kind MiTLS.Format.UncompressedPointRepresentation.lbytes_pair_parser_kind FStar.Pervasives.Native.tuple2 MiTLS.Format.Constants.constantByte FStar.UInt8.__uint_to_t MiTLS.Format.UncompressedPointRepresentation.lbytes_pair MiTLS.Format.UncompressedPointRepresentation.uncompressedPointRepresentation LowParse.Spec.Combinators.nondep_then MiTLS.Format.Constants.constantByte_parser MiTLS.Format.UncompressedPointRepresentation.lbytes_pair_parser MiTLS.Format.UncompressedPointRepresentation.ucp_of_cuv LowParse.Spec.Combinators.serialize_nondep_then MiTLS.Format.Constants.constantByte_serializer MiTLS.Format.UncompressedPointRepresentation.lbytes_pair_serializer MiTLS.Format.UncompressedPointRepresentation.cuv_of_ucp Prims.unit MiTLS.Format.UncompressedPointRepresentation.lemma_ucp_of_cuv_of_ucp MiTLS.Format.UncompressedPointRepresentation.lemma_ucp_of_cuv_is_injective LowParse.Spec.Base.serializer MiTLS.Format.UncompressedPointRepresentation.uncompressedPointRepresentation_parser_kind MiTLS.Format.UncompressedPointRepresentation.uncompressedPointRepresentation_parser
let uncompressedPointRepresentation_serializer (coordinate_length: coordinate_length_type)
    : LP.serializer (uncompressedPointRepresentation_parser coordinate_length) =
  
let l = coordinate_length in
lemma_ucp_of_cuv_is_injective #l;
lemma_ucp_of_cuv_of_ucp #l;
LP.serialize_synth (LP.nondep_then (constantByte_parser 4uy) (lbytes_pair_parser l))
  ucp_of_cuv
  (LP.serialize_nondep_then (constantByte_serializer 4uy) (lbytes_pair_serializer l))
  cuv_of_ucp
  ()