fact: Definition ASN1_Format_Definite_Length (length : nat) : CacheFormat -> Comp (B * CacheFormat) := If (NPeano.ltb length 127) Then format_nat 8 length Else (format_word WO~1 ThenC format_nat (S (NPeano.div (NPeano.log2 length) 8)) 7 ThenC format_nat length (S (NPeano.div (NPeano.log2 length) 8) * 8)) DoneC.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Strings.Ascii Coq.Strings.String Coq.Numbers.BinNums Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Bedrock.Word Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.Bool Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Common.ComposeOpt