proposition: Theorem SharpenNoIncomingFilter: FullySharpened NoIncomingConnectionsFilter.
proof: Proof. start sharpening ADT. Transparent QSInsert. drop_constraints_under_bind Complete_PacketHistorySchema ltac:( instantiate (1:=(FilterMethodGen In_History Complete_topkt Complete_totup r_n d)); unfold FilterMethodGen; red; intros v Hv; red in Hv; red; repeat match goal with | [H: (If _ Then _ Else _) v |- (If ?cond Then _ Else _) v] => destruct cond; [ apply H | cbn; cbn in H ] | [Hv: _ v |- _ v] => repeat comp_inv; apply Pick_inv in H1; repeat computes_to_econstructor; [ | eassumption ] | [H: decides ?b _ |- _] => destruct b; cbn in * | [H: exists pre, ?A /\ ?B |- exists _, _ /\ _] => destruct H as [pre [Ha Hb]]; exists pre; split; [ | assumption ] | [Hrel: DropQSConstraints_AbsR ?r_o ?r_n, Hhist: In_History _ _ _ |- _] => unfold In_History, In_History_Constr, GetRelationBnd, GetUnConstrRelationBnd in *; rewrite <- (GetRelDropConstraints r_o); rewrite <- Hrel in Hhist; apply Hhist | [H: ~ _ |- ~ _] => intro; apply H | [Hrel: DropQSConstraints_AbsR ?r_o ?r_n, Hhist: In_History_Constr _ _ _ |- _] => unfold In_History; rewrite <- Hrel; red in Hhist; unfold GetRelationBnd in Hhist; rewrite <- (GetRelDropConstraints r_o) in Hhist; apply Hhist end). hone representation using (Complete_Dropped_qs_equiv mytotup); try simplify with monad laws; [ refine pick val (DropQSConstraints (QSEmptySpec _)); [ subst H; reflexivity | red; intros; split; intros Htmp; cbv in Htmp; inversion Htmp] | eapply refine_bind; [ apply mythm; apply H0 | intro res; cbn ]; eapply refine_bind; [ apply (DropPreservesFreshIdx _ _ _ mytotup H0) | intro idx; cbn ]; apply refine_pair; apply refine_pick; intros qs Hins; comp_inv; subst qs; instantiate (1 := (UpdateUnConstrRelation r_n Fin.F1 (BuildADT.EnsembleInsert {| elementIndex := idx; indexedElement := mytotup d |} (GetUnConstrRelation r_n Fin.F1)))); red; intros oinp oidx; split; intros Hoinp; destruct Hoinp as [Hoinp | Hoinp]; [ apply in_ensemble_insert_iff; left; inversion Hoinp; reflexivity | right; apply H0 in Hoinp; apply Hoinp | exists d; split; [ apply in_ensemble_insert_iff; left | ]; inversion Hoinp; reflexivity | pose proof (H0 oinp oidx) as H0spec; destruct H0spec as [_ Hspec]; specialize (Hspec Hoinp); destruct Hspec as [inp' [H1 H2]]; exists inp'; split; [ apply in_ensemble_insert_iff; right; apply H1 | apply H2 ] ] | ]. - hone method "Filter". subst r_o; refine pick eq; simplify with monad laws; apply refine_bind; [ apply CompPreservesFilterMethod; reflexivity | intro ]; apply refine_bind; [ reflexivity | intro; simpl; higher_order_reflexivity ]. PickIndex ltac:(fun attrlist => make_simple_indexes attrlist BuildEarlyIndex BuildLastIndex). + plan CreateTerm EarlyIndex LastIndex makeClause_dep EarlyIndex_dep LastIndex_dep. + etransitivity. simplify with monad laws. eapply refine_bind; [ | intro ]. { unfold FilterMethod_Count. repeat lazymatch goal with | [ |- refine (if _ then _ else _) _ ] => eapply refine_If_Then_Else | [ |- context[UnConstrQuery_In] ] => idtac | _ => higher_order_reflexivity end. Transparent OutgoingToRule OutgoingToRule' OutgoingRule. Hint Unfold OutgoingToRule OutgoingToRule' OutgoingRule : iptables. repeat (autounfold with iptables; cbn). etransitivity; [ setoid_rewrite refine_UnConstrQuery_In | ]. { reflexivity. } { intro. etransitivity; [apply refine_Query_Where_Cond | ]. { autorewrite with iptables. repeat match goal with | _ => rewrite and_assoc | [ |- context[chain_beq ?x ?y = true /\ ?z] ] => rewrite (and_comm (chain_beq x y = true) z) end. rewrite <- !and_assoc. reflexivity. } { higher_order_reflexivity. } } implement_Query IndexUse createEarlyTerm createLastTerm IndexUse_dep createEarlyTerm_dep createLastTerm_dep. simplify with monad laws. simpl; repeat first [ setoid_rewrite refine_bind_unit | setoid_rewrite refine_bind_bind ]. apply refine_bind; [ reflexivity | intro; simpl ]. repeat rewrite ?map_length, ?app_nil_r. higher_order_reflexivity. } { unfold mytotup; simpl. etransitivity. insertion IndexUse createEarlyTerm createLastTerm IndexUse_dep createEarlyTerm_dep createLastTerm_dep. simplify with monad laws. higher_order_reflexivity. } simpl. subst H. higher_order_reflexivity. + Implement_Bags BuildEarlyBag BuildLastBag. Defined.
imports: Fiat.Narcissus.Examples.NetworkStack.IPv4Header Fiat.Narcissus.Examples.NetworkStack.TCP_Packet Bedrock.Word Coq.Arith.Arith Coq.Lists.List Fiat.QueryStructure.Automation.MasterPlan Fiat.Common.Ensembles.IndexedEnsembles Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.IPTables Fiat.Narcissus.Examples.Guard.PacketFiltersLemmas Fiat.Narcissus.Examples.Guard.DropFields