fact: Definition linkAuthorityToAdditional (curTime : timeT) (this : QueryStructure RecResolverSchema) (authority : list resourceRecord) (additional : list resourceRecord) : Comp (QueryStructure RecResolverSchema) := authorityAndAdditional <- {aal | NoDup aal /\ forall (ns : NS_Record) (ans : A_Record), List.In < sDOMAIN :: (ns!sRDATA : DomainName), sIP :: (ans!sRDATA : W) > aal <-> (List.In (NS_Record2RRecord ns) authority /\ List.In (A_Record2RRecord ans) additional /\ ns!sRDATA = ans!sNAME) }; `(this, _) <- @StatefulInsertAll RecResolverSchema _ _ _ this ``sSLIST () authorityAndAdditional (@QSInsert _) (fun aal _ => ret (< sQUERYCOUNT :: (natToWord _ 0 : W), sTTL :: (curTime ^+ serverTTL : timeT ) > ++ aal, tt)) (fun a s => ret s); ret this .
imports: Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Bedrock.Word Bedrock.Memory Fiat.Computation.ListComputations Fiat.Computation.IfDec Fiat.QueryStructure.Specification.Operations.InsertAll Fiat.QueryStructure.Automation.AutoDB Fiat.Narcissus.Examples.DNS.DNSPacket Fiat.Narcissus.Formats.DomainNameOpt Fiat.Examples.DnsServer.RecursiveDNSSchema