proposition: Lemma encode_buildempty_packet : forall (p : packet) b idx, ValidDomainName (p!"question")!"qname" -> refine (b <- format_packet (buildempty b idx p) list_CacheFormat_empty; ret (fst b)) (ret ((build_aligned_ByteString (AlignWord.split1' 8 8 p!"id" :: AlignWord.split2' 8 8 p!"id" :: WS p!"RD" (WS p!"TC" (WS b (combine Opcode_Ws[@(p : packet)!"Opcode"] WO~1))) :: combine RCODE_Ws[@ibound (indexb idx)] (WS p!"RA" WO)~0~0~0 :: AlignWord.split1' 8 8 (natToWord 16 1) :: AlignWord.split2' 8 8 (natToWord 16 1) :: AlignWord.split1' 8 8 (natToWord 16 0) :: AlignWord.split2' 8 8 (natToWord 16 0) :: AlignWord.split1' 8 8 (natToWord 16 0) :: AlignWord.split2' 8 8 (natToWord 16 0) :: AlignWord.split1' 8 8 (natToWord 16 0) :: AlignWord.split2' 8 8 (natToWord 16 0) :: projT2 (fst (aligned_format_DomainName p!"question"!"qname" (if lt_dec 96 (pow2 17) then Some (natToWord 17 96) else None, @nil _))) ++ AlignWord.split1' 8 8 QType_Ws[@p!"question"!"qtype"] :: AlignWord.split2' 8 8 QType_Ws[@p!"question"!"qtype"] :: AlignWord.split1' 8 8 QClass_Ws[@p!"question"!"qclass"] :: [AlignWord.split2' 8 8 QClass_Ws[@p!"question"!"qclass"]])))).
proof: Proof. intros. rewrite refine_format_packet_Impl_OK. simplify with monad laws. unfold encode_packet. unfold fst at 1. rewrite !GetAA_buildempty_packet. rewrite !Getid_buildempty_packet. rewrite !GetTC_buildempty_packet. rewrite !GetOpcode_buildempty_packet. rewrite !GetRD_buildempty_packet. rewrite !GetRA_buildempty_packet. rewrite !GetAuthority_buildempty_packet. rewrite !GetAnswers_buildempty_packet. rewrite !GetAdditional_buildempty_packet. rewrite !GetRCODE_buildempty_packet. Admitted. Open Scope list_scope. Definition DnsSpec : ADT DnsSig := Def ADT { rep := QueryStructure DnsSchema, Def Constructor "Init" : rep := empty,, Def Method1 "AddData" (this : rep) (t : resourceRecord) : rep * bool := Insert t into this!sRRecords, Def Method1 "Process" (this : rep) (b : Vector.t (word 8) (12 + buffSize)) : rep * (option ByteString) := p' <- Specs.Pick_Decoder_For DNS_Packet_OK format_packet (build_aligned_ByteString b) list_CacheFormat_empty; Ifopt p' as p Then p' <- Repeat recurseDepth initializing n with (p!"question"!"qname", @nil CNAME_Record) defaulting rec with (format_packet (buildempty true ``"ServFail" p) list_CacheFormat_empty) {{ results <- MaxElements (fun r r' : resourceRecord => prefix r!sNAME r'!sNAME) (For (r in this!sRRecords) Where (prefix r!sNAME (fst n)) Return r); If (is_empty results) Then format_packet (add_answers (map CNAME_Record2RRecord (snd n)) (buildempty true ``"NXDomain" p)) list_CacheFormat_empty Else (IfDec (List.Forall (fun r : resourceRecord => r!sNAME = (fst n)) results) Then b <- SingletonSet (fun b : CNAME_Record => List.In (A := resourceRecord) b results /\ p!"question"!"qtype" <> QType_inj CNAME); Ifopt b as b' Then rec (b'!sRDATA, b' :: snd n) Else (results <- ⟦ element in results | QType_match (RDataTypeToRRecordType element!sRDATA) (p!"question"!"qtype") ⟧; format_packet (add_answers (map CNAME_Record2RRecord (snd n)) (add_answers results (buildempty true ``"NoError" p))) list_CacheFormat_empty) Else (ns_results <- { ns_results | forall x : NS_Record, List.In x ns_results <-> List.In (A := resourceRecord) x results }; glue_results <- (foldComp (fun glue_records (ns_result : NS_Record) => glue_records' <- (For (rRec in this!sRRecords) Where (rRec!sNAME = ns_result!sRDATA) Return rRec); ret (glue_records' ++ glue_records)) [ ] ns_results); format_packet (add_answers (map CNAME_Record2RRecord (snd n)) (add_additionals glue_results (add_nses (map VariantResourceRecord2RRecord ns_results) (buildempty true ``"NoError" p)))) list_CacheFormat_empty)) }}; ret (this, Some (fst p')) Else ret (this, None) }. Local Opaque format_packet. Local Opaque packetDecoderImpl. Local Opaque MaxElements. Local Opaque format_packet. Local Opaque SumType.SumType_index. Local Opaque SumType.SumType_proj. Ltac implement_insert'' := implement_insert' ltac:(CombineCase5 StringPrefixIndexUse EqIndexUse) ltac:(CombineCase10 createEarlyStringPrefixTerm createEarlyEqualityTerm) ltac:(CombineCase7 createLastStringPrefixTerm createLastEqualityTerm) ltac:(CombineCase7 StringPrefixIndexUse_dep EqIndexUse_dep) ltac:(CombineCase11 createEarlyStringPrefixTerm_dep createEarlyEqualityTerm_dep) ltac:(CombineCase8 createLastStringPrefixTerm_dep createLastEqualityTerm_dep). Ltac drop_constraints ::= first [ simplify with monad laws | match goal with | H:DropQSConstraints_AbsR ?r_o ?r_n |- context [Query_In ?r_o _ _] => rewrite (DropQSConstraintsQuery_In r_o); rewrite !H end | rewrite refine_If_Then_Else_Bind | rewrite refine_If_Opt_Then_Else_Bind | rewrite refine_if_Then_Else_Duplicate | apply refine_MaxElements' | subst_refine_evar; eapply refineFueledFix; [ set_refine_evar | let refine_bid := fresh in intros ? ? ? refine_bod; set_refine_evar; repeat setoid_rewrite refine_bod ] | implement_DropQSConstraints_AbsR ]. Instance ADomainName_eq : Query_eq DomainName := Astring_eq. Instance ARRecordType_eq : Query_eq RRecordType := {| A_eq_dec := fin_eq_dec |}. Lemma refine_decode_packet {A} : forall b (k : _ -> Comp A) a', refine (p <- Specs.Pick_Decoder_For DNS_Packet_OK format_packet (build_aligned_ByteString b) list_CacheFormat_empty; Ifopt p as p' Then k p' Else a') (ByteAligned_packetDecoderImpl' (fun p => Ifopt p as p' Then k (fst (fst p')) Else a') buffSize b list_CacheDecode_empty). Proof. intros; setoid_rewrite Specs.refine_Pick_Decoder_For with (decoderImpl := packet_decoder); eauto using list_cache_empty_Equiv. simplify with monad laws. replace (` packet_decoder) with packetDecoderImpl. unfold list_CacheDecode_empty. pose proof (ByteAligned_packetDecoderImpl'_OK (fun p => Ifopt p as p' Then k (fst (fst p')) Else a') _ b). rewrite <- H. match goal with |- context [match ?z with _ => _ end ] => destruct z as [ [ [? ?] ?] | ] eqn:? ; simpl end. match goal with |- context [If_Opt_Then_Else ?z _ _ ] => replace z with (Some (p, b0, c)); try reflexivity end; rewrite <- Heqo; reflexivity. match goal with |- context [If_Opt_Then_Else (A := ?A) ?z _ _ ] => replace z with (@None A); try reflexivity end; simpl in Heqo; rewrite <- Heqo; reflexivity. reflexivity. simpl; unfold GoodCache; simpl; intuition; try congruence. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Fiat.Common.Tactics.CacheStringConstant Fiat.Computation.Decidable Fiat.Computation.IfDec Fiat.Computation.FoldComp Fiat.Computation.FueledFix Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.Common Fiat.QueryStructure.Automation.MasterPlan Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindStringPrefixSearchTerms Fiat.QueryStructure.Automation.QSImplementation Bedrock.Word Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.SimpleDnsOpt Fiat.Narcissus.Examples.DNS.SimpleDNSPacket Fiat.Narcissus.Stores.Cache Fiat.Narcissus.Stores.DomainNameStore Fiat.Narcissus.BinLib.AlignedDomainName Fiat.Narcissus.BinLib.AlignedByteString Fiat.Examples.DnsServer.DecomposeSumField Fiat.Examples.DnsServer.SimpleDnsLemmas Fiat.Examples.DnsServer.DnsAutomation Fiat.Examples.DnsServer.SimpleAuthoritativeDNSSchema