val parse_fwid_payload
: parser parse_fwid_payload_kind fwid_payload_t
val parse_fwid_payload
: parser parse_fwid_payload_kind fwid_payload_t
let parse_fwid_payload
=
  ((OID_DIGEST_SHA256) `parse_envelop_OID_with`
   (serialize_asn1_TLV_of_type OCTET_STRING
   `serialize_filter`
   filter_fwid_payload_string))
  `parse_synth`
  synth_fwid_payload_t
module L0.X509.FWID

open LowParse.Low.Base
// open LowParse.Low.Combinators

open ASN1.Spec
open ASN1.Low

// open X509.Crypto
// open X509.BasicFields
// open X509.ExtFields

open FStar.Integers

#set-options "--z3rlimit 32 --fuel 0 --ifuel 0 --using_facts_from '* -FStar.Tactics -FStar.Reflection'"

let decl = ()

(* FWID
  ======
*)

let filter_fwid_payload_string
  (s: datatype_of_asn1_type OCTET_STRING)
: GTot bool
= //fst x' = OID_DIGEST_SHA256 &&
  v (s.ASN1.Base.len) = 32

let fwid_payload_t'
= (OID_DIGEST_SHA256) `envelop_OID_with_t`
  (parse_filter_refine filter_fwid_payload_string)

(* Serialier spec *)
let synth_fwid_payload_t
  (x': fwid_payload_t')
: GTot (fwid_payload_t)
= { fwid_hashAlg = fst x';
    fwid_value   = snd x' }

inline_for_extraction noextract
let synth_fwid_payload_t'
  (x: fwid_payload_t)
: Tot (x': fwid_payload_t' { x == synth_fwid_payload_t x' } )
= (x.fwid_hashAlg, x.fwid_value)
/
prims.fst.checked LowParse.Low.Base.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked ASN1.Base.fst.checked
L0.X509.FWID.fst
LowParse.Spec.Base.parser L0.X509.FWID.parse_fwid_payload_kind L0.X509.FWID.fwid_payload_t
LowParse.Spec.Combinators.parse_synth LowParse.Spec.Combinators.and_then_kind LowParse.Spec.Combinators.parse_filter_kind ASN1.Spec.Value.OID.parse_asn1_oid_TLV_kind ASN1.Spec.TLV.parse_asn1_TLV_kind_of_type ASN1.Base.OCTET_STRING ASN1.Spec.Value.OID.envelop_OID_with_t ASN1.Base.OID_DIGEST_SHA256 LowParse.Spec.Combinators.parse_filter_refine ASN1.Base.datatype_of_asn1_type L0.X509.FWID.filter_fwid_payload_string L0.X509.FWID.fwid_payload_t ASN1.Spec.Value.OID.parse_envelop_OID_with LowParse.Spec.Combinators.parse_filter ASN1.Spec.TLV.parse_asn1_TLV_of_type LowParse.Spec.Combinators.serialize_filter ASN1.Spec.TLV.serialize_asn1_TLV_of_type L0.X509.FWID.synth_fwid_payload_t
let parse_fwid_payload =
  
((OID_DIGEST_SHA256)
  `parse_envelop_OID_with`
  ((serialize_asn1_TLV_of_type OCTET_STRING) `serialize_filter` filter_fwid_payload_string))
`parse_synth`
synth_fwid_payload_t