fact: Definition format_DomainName : FormatM DomainName B := LeastFixedPoint (fDom := [DomainName; CacheFormat]) (fun format_DomainName domain env => If (string_dec domain "") Then format_ascii terminal_char env Else (position <- { position | forall p, position = Some p -> In p (getE env domain)}; Ifopt position as position Then (`(ptr1b, env') <- format_word (proj1_sig (fst position)) env; `(ptr2b, env') <- format_word (snd position) env'; ret (mappend ptr1b ptr2b, env')) Else (`(label, domain') <- { labeldomain' | (domain = (fst labeldomain') ++ String "." (snd labeldomain') \/ labeldomain' = (domain, "")) /\ ValidLabel (fst labeldomain') /\ (forall label' post', domain = label' ++ post' -> ValidLabel label' -> String.length label' <= String.length (fst labeldomain'))}%string%nat; `(lenb, env') <- format_nat 8 (String.length label) env; `(labelb, env') <- format_string label env'; `(domainb, env') <- format_DomainName domain' env'; ret (mappend (mappend lenb labelb) domainb, Ifopt peekE env as curPtr Then addE_G env' (domain, curPtr) Else env' )))).
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Computation.Core Fiat.Computation.FixComp Fiat.Computation.Notations Fiat.Computation.Refinements.General Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.AsciiOpt