proposition: Lemma refine_no_usurp_authority_check : forall (rr : resourceRecord) (R : @IndexedEnsemble resourceRecord), (forall tup tup' : IndexedElement, elementIndex tup <> elementIndex tup' -> R tup -> R tup' -> (indexedElement tup)!sNAME = (indexedElement tup')!sNAME -> RDataTypeToRRecordType (indexedElement tup)!sRDATA = NS -> RDataTypeToRRecordType (indexedElement tup')!sRDATA <> NS -> prefix (indexedElement tup)!sNAME (indexedElement tup')!sNAME -> (indexedElement tup)!sNAME = (indexedElement tup')!sNAME) -> refine {b | decides b (forall tup', R tup' -> RDataTypeToRRecordType rr!sRDATA = NS -> RDataTypeToRRecordType (indexedElement tup')!sRDATA <> NS -> prefix rr!sNAME (indexedElement tup')!sNAME -> rr!sNAME = (indexedElement tup')!sNAME)} (If (beq_RRecordType (RDataTypeToRRecordType rr!sRDATA) NS) Then count <- Count For (QueryResultComp R (fun tup => Where (rr!sNAME <> tup!sNAME /\ RDataTypeToRRecordType tup!sRDATA <> NS /\ prefix (rr!sNAME) (tup!sNAME)) Return tup )%QueryImpl); ret (beq_nat count 0) Else ret true).
proof: Proof. intros. let p := constr:(RDataTypeToRRecordType (rr!sRDATA : RDataType) = NS) in intros; setoid_rewrite refine_pick_decides with (P := p) at 1. setoid_rewrite refine_beq_RRecordType_dec; simplify with monad laws. finish honing. { intros. erewrite refine_decides_Equiv_Ensemble' with (P' := fun tup' => R tup' -> (_ (indexedElement tup') /\ _ (indexedElement tup')) -> rr!sNAME = (indexedElement tup')!sNAME). Focus 2. split; intros. apply H1. eassumption. eassumption. pattern (indexedElement idx'). apply (proj1 H3). pattern (indexedElement idx'). apply (proj2 H3). eauto. pose proof (@refine_forall_to_exists _ (fun idx => rr!sNAME = idx!sNAME) (fun tup => (fun r : resourceRecord => RDataTypeToRRecordType r!sRDATA <> NS /\ is_true (prefix rr!sNAME r!sNAME)) tup) R _); simpl in *; erewrite H1. setoid_rewrite refine_constraint_check_into_QueryResultComp. simplify with monad laws. setoid_rewrite <- negb_involutive_reverse. finish honing. apply DecideableEnsemble_And. unfold Same_set, Included, In; intuition. } intros; refine pick val _. finish honing. simpl; intros; intuition. 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