proposition: Lemma MaxElements_UnConstrQuery_In_Where_Prop {qs_schema} : forall (idx : Fin.t (numRawQSschemaSchemas qs_schema)) (r_o0 : UnConstrQueryStructure qs_schema) (P : Ensemble RawTuple) (l : list RawTuple) op, DecideableEnsemble P -> MaxElements op (For (UnConstrQuery_In r_o0 idx (fun r0 : RawTuple => Where (P r0) Return r0 ))) ↝ l -> Forall P l.
proof: Proof. Admitted. Definition QType_proj : QType -> option RRecordType. Admitted. Lemma refine_Process_Query_Exact_Match : forall (r_o : UnConstrQueryStructure DnsSchema) r_n e a1 qType a0 s answers, DecomposeRawQueryStructureSchema_AbsR (qs_schema := DnsSchema) Fin.F1 (Fin.FS (Fin.FS (Fin.FS Fin.F1))) ResourceRecordTypeTypes (SumType.SumType_index ResourceRecordTypeTypes) (SumType.SumType_proj ResourceRecordTypeTypes) (SumType.inj_SumType ResourceRecordTypeTypes) r_o r_n -> refine (a3 <- For (UnConstrQuery_In r_o Fin.F1 (fun r : RawTuple => Where (RDataTypeToRRecordType (GetAttributeRaw r (Fin.FS (Fin.FS (Fin.FS Fin.F1)))) <> CNAME /\ GetAttributeRaw r Fin.F1 = a1) Return r )); a' <- ⟦element in a3 | QType_match (RDataTypeToRRecordType (GetAttributeRaw element (Fin.FS (Fin.FS (Fin.FS Fin.F1))))) qType ⟧; If negb (is_empty a3) Then format_packet (add_answers answers (add_answers a' (buildempty true s a0))) DomainNameStore.list_CacheFormat_empty Else e) (If (QType_dec qType (EnumType.BoundedIndex_inj_EnumType ``("STAR"))) Then (a3 <- For (UnConstrQuery_In r_o Fin.F1 (fun r : RawTuple => Where (RDataTypeToRRecordType (GetAttributeRaw r (Fin.FS (Fin.FS (Fin.FS Fin.F1)))) <> CNAME /\ GetAttributeRaw r Fin.F1 = a1) Return r )); If negb (is_empty a3) Then (format_packet (add_answers answers (add_answers a3 (buildempty true s a0))) DomainNameStore.list_CacheFormat_empty) Else e) Else (Ifopt QType_proj qType as rType Then (a3 <- For (UnConstrQuery_In r_o Fin.F1 (fun r : RawTuple => Where (RDataTypeToRRecordType (GetAttributeRaw r (Fin.FS (Fin.FS (Fin.FS Fin.F1)))) = rType /\ RDataTypeToRRecordType (GetAttributeRaw r (Fin.FS (Fin.FS (Fin.FS Fin.F1)))) <> CNAME /\ GetAttributeRaw r Fin.F1 = a1) Return r )); count <- Count (For (UnConstrQuery_In r_o Fin.F1 (fun r : RawTuple => Where (RDataTypeToRRecordType (GetAttributeRaw r (Fin.FS (Fin.FS (Fin.FS Fin.F1)))) <> rType /\ RDataTypeToRRecordType (GetAttributeRaw r (Fin.FS (Fin.FS (Fin.FS Fin.F1)))) <> CNAME /\ GetAttributeRaw r Fin.F1 = a1) Return () ))); If negb (is_empty a3) || (le_lt_dec count 0) Then (format_packet (add_answers answers (add_answers a3 (buildempty true s a0))) DomainNameStore.list_CacheFormat_empty) Else e) Else e)). Admitted. Lemma refine_If_Else_Bind {A B} : forall b a (k : A -> Comp B) t, refine (If b Then t Else (a' <- a; k a')) (a' <- a; If b Then t Else k a'). Proof. destruct b; simpl; intros; try reflexivity. intros ? ?. computes_to_inv; eauto. Qed.
imports: Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Bool.Bvector Coq.Lists.List Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.AutoDB Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms Fiat.QueryStructure.Automation.QSImplementation Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.SimpleDnsOpt Fiat.Narcissus.Examples.DNS.SimpleDNSPacket Fiat.Examples.DnsServer.DecomposeSumField Fiat.Computation.FoldComp Fiat.Examples.DnsServer.SimpleAuthoritativeDNSSchema