val synth_fwid_payload_t (x': fwid_payload_t') : GTot (fwid_payload_t)
val synth_fwid_payload_t (x': fwid_payload_t') : GTot (fwid_payload_t)
let synth_fwid_payload_t
  (x': fwid_payload_t')
: GTot (fwid_payload_t)
= { fwid_hashAlg = fst x';
    fwid_value   = snd x' }
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)
/
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
x': L0.X509.FWID.fwid_payload_t' -> Prims.GTot L0.X509.FWID.fwid_payload_t
L0.X509.FWID.fwid_payload_t' L0.X509.FWID.Mkfwid_payload_t FStar.Pervasives.Native.fst LowParse.Spec.Combinators.parse_filter_refine ASN1.Base.datatype_of_asn1_type ASN1.Base.OID ASN1.Spec.Value.OID.filter_asn1_oid_TLV_of ASN1.Base.OID_DIGEST_SHA256 ASN1.Base.OCTET_STRING L0.X509.FWID.filter_fwid_payload_string FStar.Pervasives.Native.snd L0.X509.FWID.fwid_payload_t
let synth_fwid_payload_t (x': fwid_payload_t') : GTot (fwid_payload_t) =
  
{ fwid_hashAlg = fst x'; fwid_value = snd x' }