proposition: Theorem SharpenNoIncomingFilter: FullySharpened NoIncomingConnectionsFilter.
proof: Proof. start sharpening ADT. Transparent QSInsert. pose (h _ DroppedFilterMethod) as h. compute in h. pose (topkt _ DroppedFilterMethod) as topkt. cbn -[GetAttribute] in topkt. pose (totup _ DroppedFilterMethod) as totup. simpl in totup. pose (thm _ DroppedFilterMethod) as Hdrop. simpl in Hdrop. drop_constraints_under_bind Complete_PacketHistorySchema ltac:( intro v; intros Htemp; match goal with [H: DropQSConstraints_AbsR _ _ |- _] => apply (UnConstrPreservesFilterMethod _ Complete_topkt Complete_totup _ _ _ _ H) end; apply Htemp). hone representation using (Complete_Dropped_qs_equiv totup). - simplify with monad laws. refine pick val (DropQSConstraints (QSEmptySpec _)). subst H; reflexivity. red. intros. split; intros Htmp; cbv in Htmp; inversion Htmp. - etransitivity. simplify with monad laws. apply refine_bind. apply Hdrop. apply H0. intro. cbn. eapply refine_bind. apply (freshidxtemp _ _ _ totup H0). intro idx. Definition tmpinsert h (totup: input -> @Tuple h) (r_n: UnConstrQueryStructure (PacketHistorySchema h)) d (a: option result) idx := ret (UpdateUnConstrRelation r_n Fin.F1 (BuildADT.EnsembleInsert {| elementIndex := idx; indexedElement := totup d |} (GetUnConstrRelation r_n Fin.F1)), a). Lemma refine_pair: forall (T U: Type) (x: T) (y: U) (c: Comp T), refine c (ret x) -> refine (x' <- c; ret (x', y)) (ret (x, y)). Proof. intros. intro; intros. comp_inv. computes_to_econstructor. red in H. apply H. auto. auto. 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