proposition: Lemma CompPreservesFilterMethod: forall topkt totup r inp, topkt = (DropFields.topkt _ DroppedFilterMethod) -> totup = (DropFields.totup _ DroppedFilterMethod) -> refine (FilterMethod_UnConstr topkt totup r inp) (FilterMethod_UnConstr_Comp topkt totup r inp).
proof: Proof. unfold FilterMethod_UnConstr, FilterMethod_UnConstr_Comp. red; intros topkt totup r inp Hp Ht v H; cbn in Hp, Ht; rewrite Hp, Ht in *. destruct (cf_cond OutgoingRule inp) eqn:outrule. assumption. destruct (negb (cf_cond IncomingRule inp)) eqn:inrule. assumption. inversion H as [c Hc]. destruct Hc as [Hcount Hres]. unfold In in *. epose proof (count_zero_iff _ _ _ _ _ c _ _ Hcount) as Hcziff. computes_to_econstructor. computes_to_econstructor. instantiate (1:=(0 <? c)). red. destruct (0 <? c) eqn:Hzero; simpl. - rewrite <- Hzero in Hcziff. apply Hcziff in Hzero. destruct Hzero as [pre [Hin Hcond]]. exists pre. split; [ apply Hin | apply Hcond ]. - intro. rewrite <- Hzero in Hcziff. apply Hcziff in H0. congruence. - apply Hres. Unshelve. * intros. repeat (let i := fresh in destruct t as [i t]). reflexivity. * reflexivity. Qed.
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