fact: Definition FilterMethod_UnConstr_Comp {h} (topkt: @Tuple h -> input) (totup: input -> @Tuple h) (r: UnConstrQueryStructure (PacketHistorySchema h)) (inp: input) := If cf_cond OutgoingRule inp Then <ACCEPT> Else If negb (cf_cond IncomingRule inp) Then ret None Else (c <- Count (For (t in r%"History") Where (cf_cond (OutgoingToRule (ipv4_source (in_ip4 inp))) (topkt t) = true) Return ()); If 0 <? c Then <ACCEPT> Else <DROP>).
imports: Fiat.Narcissus.Examples.NetworkStack.IPv4Header Fiat.Narcissus.Examples.NetworkStack.TCP_Packet Bedrock.Word Coq.Arith.Arith Coq.Lists.List Fiat.QueryStructure.Automation.MasterPlan IndexedEnsembles Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.IPTables Fiat.Narcissus.Examples.Guard.PacketFiltersLemmas Fiat.Narcissus.Examples.Guard.DropFields Coq.Sets.Ensembles