val test_pk_compressed (a: hash_alg_ecdsa) (inp: vec_SigVer) : FStar.All.ML bool
let test_pk_compressed (a:hash_alg_ecdsa) (inp:vec_SigVer) : FStar.All.ML bool =
  let { msg; qx; qy; r; s; result } = inp in
  let msg_len   = String.strlen msg / 2 in
  let pk_x_len  = String.strlen qx / 2 in
  let pk_y_len  = String.strlen qy / 2 in
  let sig_r_len = String.strlen r / 2 in
  let sig_s_len = String.strlen s / 2 in
  let is_valid  = result in

  if not (msg_len <= max_size_t &&
         min_input_length a <= msg_len &&
         pk_x_len = 32 && pk_y_len = 32 &&
         sig_r_len = 32 && sig_s_len = 32)
  then false
  else
    let pk_x = from_hex qx in
    let pk_y = from_hex qy in
    let pk_raw = concat #_ #32 #32 pk_x pk_y in
    let pk_c = pk_compressed_from_raw pk_raw in
    let pk_raw_c = pk_compressed_to_raw pk_c in

    match pk_raw_c with
    | Some pk_raw_c -> PS.print_compare true 64 pk_raw pk_raw_c
    | None -> false
val test_pk_compressed (a: hash_alg_ecdsa) (inp: vec_SigVer) : FStar.All.ML bool
let test_pk_compressed (a: hash_alg_ecdsa) (inp: vec_SigVer) : FStar.All.ML bool =
let { msg = msg ; qx = qx ; qy = qy ; r = r ; s = s ; result = result } = inp in
let msg_len = String.strlen msg / 2 in
let pk_x_len = String.strlen qx / 2 in
let pk_y_len = String.strlen qy / 2 in
let sig_r_len = String.strlen r / 2 in
let sig_s_len = String.strlen s / 2 in
let is_valid = result in
if
  not (msg_len <= max_size_t && min_input_length a <= msg_len && pk_x_len = 32 && pk_y_len = 32 &&
      sig_r_len = 32 &&
      sig_s_len = 32)
then false
else
  let pk_x = from_hex qx in
  let pk_y = from_hex qy in
  let pk_raw = concat #_ #32 #32 pk_x pk_y in
  let pk_c = pk_compressed_from_raw pk_raw in
  let pk_raw_c = pk_compressed_to_raw pk_c in
  match pk_raw_c with
  | Some pk_raw_c -> PS.print_compare true 64 pk_raw pk_raw_c
  | None -> false
Spec.P256.Test.fst.checked
Spec.P256.fst.checked Spec.Hash.Definitions.fst.checked Spec.ECDSA.Test.Vectors.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.PrintSequence.fsti.checked Lib.Meta.fst.checked Lib.IntTypes.fsti.checked FStar.String.fsti.checked FStar.Pervasives.fsti.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.All.fst.checked
Spec.P256.Test.fst
Spec.P256.hash_alg_ecdsa Spec.ECDSA.Test.Vectors.vec_SigVer Lib.Meta.hex_string Prims.bool Prims.op_Negation Prims.op_AmpAmp Prims.op_LessThanOrEqual Lib.IntTypes.max_size_t Spec.P256.min_input_length Prims.op_Equality Prims.int Lib.ByteSequence.lbytes Lib.PrintSequence.print_compare FStar.Pervasives.Native.option Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.P256.pk_compressed_to_raw Spec.P256.pk_compressed_from_raw Prims.op_Addition Prims.eq2 FStar.Seq.Base.seq Lib.Sequence.to_seq FStar.Seq.Base.append Lib.Sequence.concat Lib.IntTypes.uint8 FStar.Seq.Properties.lseq Prims.op_Division FStar.String.strlen Lib.Meta.from_hex
module Spec.P256.Test

open Lib.IntTypes
open Lib.Sequence
open Lib.Meta

open Spec.P256
open Spec.ECDSA.Test.Vectors
open Spec.Hash.Definitions

module PS = Lib.PrintSequence

#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
val test_pk_compressed (a: hash_alg_ecdsa) (inp: vec_SigVer) : FStar.All.ML bool
a: Spec.P256.hash_alg_ecdsa -> inp: Spec.ECDSA.Test.Vectors.vec_SigVer -> FStar.All.ML Prims.bool