(def-language filtered-network-language
    (embedded-languages routed-networks)
    (base-types directions actions)
    (sorts
      (filters "[datagrams,directions,states -> actions]")
      )
    (constants
      (inbound directions)
      (outbound directions)
      (accept actions)
      (reject actions)
      (drop actions)
      (netstate "[netstates, zz -> prop]")
      (iface%filter "[ifaces -> filters]")
      (at%router "[datagrams, hosts, zz -> prop]")
      (delivered "[datagrams, hosts, zz -> prop]")
      (failed%delivery "[datagrams, hosts, zz -> prop]")
      (inbound%at%iface "[datagrams, ifaces, zz -> prop]")
      (outbound%at%iface "[datagrams, ifaces, addresses, zz -> prop]")
      (filtered%out "[datagrams, ifaces, directions, actions, zz -> prop]")
      ))

(def-theory filtered-networks 
    (language filtered-network-language)
    (component-theories routed-networks)
    (distinct-constants 
      (inbound outbound)
      (accept reject drop))
    (axioms
      (iface_router-is-total
        "total_q{iface%filter, [ifaces -> filters]}")
      (delivery-transition
        "forall(d:datagrams, h:hosts, i:ifaces, k:zz,
              destination%address(d) in addresses%of%host(h)
                implies
              at%router(d,h,k)
                iff
              delivered(d,h,k))")
      (forwarding-transition
        "forall(d:datagrams, h:hosts, i:ifaces, a:addresses, k:zz,
              routing%fn(host%router(h),d) = make%route%component(i,a)
                implies
              at%router(d,h,k)
                iff
              outbound%at%iface(d,i,a,k))")
      (failed-delivery-transition
        "forall(d:datagrams, h:hosts, k:zz,
              not(#(routing%fn(host%router(h),d)))
                implies
              at%router(d,h,k)
                iff
              failed%delivery(d,h,k))")
      (inbound-filtering-transition
        "forall(d:datagrams, h:hosts, i:ifaces, act:actions, n:netstates, 
                        k:zz,
              h = iface%host(i)
                and 
              netstate(n,k)
                and
              i in ifaces%of%host(h)
                and 
              iface%filter(i)(d,inbound,n(h)) = act
                implies
              inbound%at%iface(d,i,k) 
                iff
              if_form(act = accept, 
                              at%router(d,h,k), 
                              filtered%out(d,i,inbound,act,k)))")
      (outbound-filtering-transition
        "forall(d:datagrams, h:hosts, i:ifaces, a:addresses, act:actions, 
                        n:netstates, k:zz, 
              h = iface%host(i)
                and
              netstate(n,k)
                and
              i in ifaces%of%host(h)
                and 
              iface%filter(i)(d,outbound,n(h)) = act
                and
              routing%fn(host%router(h),d) = make%route%component(i,a)
                and
              #(addr%to%iface(a))
                implies
              outbound%at%iface(d,i,a,k)
                iff
              if_form(act = accept, 
                              inbound%at%iface(d,addr%to%iface(a),k+1), 
                              filtered%out(d,i,outbound,act,k)))")
      (state-transition
        "forall(d:datagrams, h:hosts, n:netstates, k:zz,
              at%router(d,h,k)
                implies
              netstate(n,k)
                iff
              netstate(append%to%netstate(n,h,d),k+1))")
      
      ))

(def-constant iface%out%to%in 
    "lambda(out%i:ifaces,d:datagrams,n:netstates,
          iota(in%i:ifaces,
              iface%filter(out%i)(d,outbound,n(iface%host(out%i))) = accept
                and
              in%i = next%hop%iface(routing%fn(host%router(iface%host(out%i)),d))))"
    (theory filtered-networks))

(def-constant iface%in%to%out 
    "lambda(in%i:ifaces,d:datagrams,n:netstates,
          iota(out%i:ifaces,
              iface%filter(in%i)(d,inbound,n(iface%host(out%i))) = accept
                and
              out%i = out%iface(routing%fn(host%router(iface%host(in%i)),d))))"
    (theory filtered-networks))

(def-theorem iface_out_to_in-macete 
    "forall(i:ifaces, d:datagrams, a:addresses, n:netstates, k:zz,
          netstate(n,k) 
            and 
          routing%fn(host%router(iface%host(i)),d) = make%route%component(i,a)
            and
          #(iface%out%to%in(i,d,n))
            implies
          outbound%at%iface(d,i,a,k)
            iff
          inbound%at%iface(d,iface%out%to%in(i,d,n),k+1))"
    (theory filtered-networks)
    (proof
      (
        (unfold-single-defined-constant-globally iface%out%to%in)
        (eliminate-defined-iota-expression 0 w)
        direct-inference
        (instantiate-theorem 
          outbound-filtering-transition
          ("d" "iface%host(i)" "i" "a" "accept" "n" "k"))
        (block 
            (script-comment "`instantiate-theorem' at (0 0 2)")
            (contrapose "with(p:prop,not(p));")
            (apply-macete-with-minor-premises iface-is-an-iface-of-host))
        (block 
            (script-comment "`instantiate-theorem' at (0 0 5)")
            (contrapose "with(p:prop,not(p));")
            (instantiate-theorem 
              next_hop_iface-lemma 
              ("iface%host(i)" "d" "i" "a")))
        (move-to-ancestor 2)
        (block 
            (script-comment "`instantiate-theorem' at (0 1)")
            (instantiate-theorem 
              next_hop_iface-lemma 
              ("iface%host(i)" "d" "i" "a"))
            simplify)
        )))

(def-theorem iface_in_to_out-macete 
    "forall(i:ifaces, d:datagrams, a:addresses, n:netstates, k:zz,
          netstate(n,k) 
            and 
          (routing%fn(host%router(iface%host(i)),d) 
              = 
            make%route%component(iface%in%to%out(i,d,n),a))
            implies
          inbound%at%iface(d,i,k)
            iff
          outbound%at%iface(d,iface%in%to%out(i,d,n),a,k))"
    (theory filtered-networks)
    (proof
      (
        (unfold-single-defined-constant-globally iface%in%to%out)
        (eliminate-defined-iota-expression 0 u)
        direct-inference
        (cut-with-single-formula "iface%host(i)=iface%host(u)")
        (move-to-sibling 1)
        (block 
            (script-comment "`cut-with-single-formula' at (1)")
            (backchain "with(p:prop,p and p);")
            (apply-macete-with-minor-premises host-of-out_iface))
        (block 
            (script-comment "`cut-with-single-formula' at (0)")
            (instantiate-theorem 
              inbound-filtering-transition
			      
              ("d" "iface%host(i)" "i" "accept" "n" "k"))
            (block 
	(script-comment "`instantiate-theorem' at (0 0 2)")
	(contrapose "with(p:prop,not(p));")
	(apply-macete-with-minor-premises iface-is-an-iface-of-host))
            (block 
	(script-comment "`instantiate-theorem' at (0 0 3)")
	(contrapose "with(p:prop,not(p));")
	simplify)
            (block 
	(script-comment "`instantiate-theorem' at (0 1 0 0)")
	simplify
	(instantiate-theorem 
	  forwarding-transition
			          
	  ("d" "iface%host(i)" "u" "a" "k")))
            (block 
	(script-comment "`instantiate-theorem' at (0 1 1 0)")
	(instantiate-theorem 
	  forwarding-transition
			          
	  ("d" "iface%host(i)" "u" "a" "k"))
	simplify))
        )))

(def-translation packet-trajectory-theory-to-filtered-networks 
    (source packet-trajectory-theory)
    (target filtered-networks)
    (fixed-theories h-o-real-arithmetic)
    (sort-pairs
      (ifaces ifaces)
      (datagrams datagrams)
      (netstates netstates))
    (constant-pairs
      (iface%out%to%in iface%out%to%in)
      (iface%in%to%out iface%in%to%out))
    dont-enrich)

(def-transported-symbols trajectory
    (translation packet-trajectory-theory-to-filtered-networks))