fact: Definition DnsSpec (q : _ -> packet) : ADT _ := Def ADT { rep := QueryStructure RecResolverSchema, Def Constructor "Init" : rep := empty,, Def Method3 "Process" (this : rep) (sourceIP : W) (curTime : timeT) (p : packet) : rep * packet * option W := If p!"QR" Then vs <- For (v in this!sCACHE) Where (p!"question"!"qtype" = CachedQueryTypes_inj v!sQTYPE) Where (curTime <= v!sTTL) Return (v ! sCACHEDVALUE) ; If is_empty vs Then (reqIDs <- For (req in this!sREQUESTS) Where (curTime <= req!sTTL) Return (req!sID); newID <- { newID | ~ List.In newID reqIDs}; bestServer <- MaxElement (fun r r' : @Tuple SLISTHeading => (prefix r!sDOMAIN r'!sDOMAIN) /\ r!sQUERYCOUNT <= r'!sQUERYCOUNT) (For (server in this!sSLIST) Where (prefix server!sDOMAIN p!"question"!"qname") Where (curTime <= server!sTTL) Return server); Ifopt bestServer as bestServer Then `(this, _) <- Delete req from this ! sREQUESTS where (req!sTTL <= curTime); `(this, b) <- Insert < sID :: newID, sIP :: sourceIP, sTTL :: curTime ^+ requestTTL > ++ p into this!sREQUESTS; ret (this, (q <"id" :: newID, "QR" :: false, "Opcode" :: ``"Query", "AA" :: false, "TC" :: false, "RD" :: true, "RA" :: false, "RCode" :: ``"NoError", "question" :: p!"question", "answers" :: [ ], "authority" :: [ ], "additional" :: [ ] >, Some (getSIP bestServer))) Else ret (this, (buildempty false ``"ServFail" p, Some sourceIP)) ) Else (answers <- { answers | NoDup answers /\ forall ans : resourceRecord, List.In ans answers <-> List.In (A := CachedValue) ans vs }; If is_empty answers Then failures <- { failures | NoDup failures /\ forall fail : SOA_Record, List.In (A := resourceRecord) fail failures <-> List.In (A := CachedValue) fail vs }; ret (this, (add_additionals failures (buildempty false ``"NXDomain" p), Some sourceIP)) Else ret (this, (add_answers answers (buildempty false ``"NoError" p), Some sourceIP))) Else (reqs <- For (req in this!sREQUESTS) Where (req!sID = p!"id") Where (req!"question"!"qtype" = p!"question"!"qtype") Return req; Ifopt List.hd_error reqs as req Then (IfDec p!"RCODE" = ``"NoError" Then (If isAnswer p Then `(this, reqs) <- Delete req from this!sREQUESTS where (req!sID = p!"id"); this <- addAnswersToCache curTime this p!"answers" p!"authority" p!"additional"; ret (this, (<"id" :: req!"id", "QR" :: true, "Opcode" :: req!"Opcode", "AA" :: false, "TC" :: p!"TC", "RD" :: req!"RD", "RA" :: true, "RCode" :: ``"NoError", "question" :: req!"question", "answers" :: p!"answers", "authority" :: p!"authority", "additional" :: p!"additional" >, Some req!sIP) ) Else (this <- linkAuthorityToAdditional curTime this p!"authority" p!"additional"; bestServer <- MaxElement (fun r r' : @Tuple SLISTHeading => (prefix r!sDOMAIN r'!sDOMAIN) /\ r!sQUERYCOUNT <= r'!sQUERYCOUNT) (For (server in this!sSLIST) Where (prefix server!sDOMAIN p!"question"!"qname") Where (curTime <= server!sTTL) Return server); Ifopt bestServer as bestServer Then ret (this, (<"id" :: p!"id", "QR" :: false, "Opcode" :: ``"Query", "AA" :: false, "TC" :: false, "RD" :: true, "RA" :: false, "RCode" :: ``"NoError", "question" :: p!"question", "answers" :: [ ], "authority" :: [ ], "additional" :: [ ] >, Some bestServer!sIP)) Else ret (this, (p, None ) ) ) ) Else (soas <- { soas | NoDup soas /\ forall soa : SOA_Record, List.In soa soas <-> List.In (A := resourceRecord) soa (p!"authority") }; Ifopt List.hd_error soas as soa Then reqType <- SingletonSet (fun b : CachedQueryTypes => req!"question"!"qtype" = CachedQueryTypes_inj b); Ifopt reqType as reqType Then (`(this, foo) <- Insert (< sTTL :: curTime ^+ cachedTTL, sCACHETYPE :: ``"Failure", sDOMAIN :: req!"question"!"qname", sQTYPE :: reqType, sCACHEDVALUE :: Failure2CachedValue (<"RCODE" :: (p!"RCODE" : ResponseCode) > ++ soa!sRDATA : FailureRecord ) > ) into this!sCACHE; ret (this, (p, Some req!sIP)) ) Else ret (this, (p, Some req!sIP) ) Else ret (this, (p, Some req!sIP ) ) ) ) Else ret (this, (p, None ) ) ) }.
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