Documentation

WeightedNetKAT.Papers.PLDI2026

Definitions, lemmas and theorems listed in order #

This file contains links to all definitions, lemmas and theorems from the paper.

They are listed roughly in the order they appear in the paper. This file should serve as a jumping off point to navigate and explore the formalization, and not as a reference to how things are defined. We invite the reader to click on the names in each definition to jump to their original definition. In Visual Studio Code one can Ctrl/CMD+Click on symbols to jump to their definition.

Section 3 – wNetKAT: Syntax and Semantics #

source
def WeightedNetKAT.Paper.PLDI2026.Section3.Definition1 :
Paper.Link Countsupp
Equations
Instances For
    source
    def WeightedNetKAT.Paper.PLDI2026.Section3.Figure6 {F : Type u_1} {N : Type u_2} {𝒮 : Type u_3} [DecidableEq F] [Listed F] [DecidableEq N] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {p : Pol[F,N,𝒮]} {t : Pred[F,N]} :
    Paper.Link (Pol[F,N,𝒮], p.sem, t.test)
    Equations
    Instances For
      source
      def WeightedNetKAT.Paper.PLDI2026.Section3.Figure7 {F : Type u_1} {N : Type u_2} {𝒮 : Type u_3} [Listed F] :
      Paper.Link (RPol 𝒮)
      Equations
      Instances For

        Section 4 – Language Model #

        source
        theorem WeightedNetKAT.Paper.PLDI2026.Section4.Inline1 :
        Paper.Link GS
        source
        def WeightedNetKAT.Paper.PLDI2026.Section4.Definition2 {F : Type u_1} {N : Type u_2} {𝒮 : Type u_3} [DecidableEq F] [Listed F] [DecidableEq N] [Listed N] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {p' : RPol 𝒮} :
        Paper.Link G⟦~p'⟧
        Equations
        Instances For
          source
          theorem WeightedNetKAT.Paper.PLDI2026.Section4.Lemma1 {F : Type u_1} {N : Type u_2} {𝒮 : Type u_3} [DecidableEq F] [Listed F] [Inhabited F] [DecidableEq N] [Listed N] [Inhabited N] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {p' : RPol 𝒮} :
          Paper.LinkLem (p'.sem = fun (h : Pk[F,N] × List Pk[F,N]) => ω∑ (x : ↑G⟦~p'⟧.support), G⟦~p'⟧ ↑x * (↑x).sem h)

          Section 5 – wNetKAT Automata #

          source
          def WeightedNetKAT.Paper.PLDI2026.Section5.Definition3 {F : Type u_1} {N : Type u_2} {𝒮 : Type u_3} [Listed F] [Semiring 𝒮] {p' : RPol 𝒮} :
          Paper.Link WNKA[F,N,𝒮,S p']
          Equations
          Instances For
            source
            theorem WeightedNetKAT.Paper.PLDI2026.Section5.Inline1 {F : Type u_1} {N : Type u_2} {𝒮 : Type u_3} [DecidableEq F] [Listed F] [Inhabited F] [DecidableEq N] [Listed N] [Inhabited N] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {p' : RPol 𝒮} :
            Paper.Link RPol.𝒜⟦~p'⟧
            source
            theorem WeightedNetKAT.Paper.PLDI2026.Section5.Table1 {F : Type u_1} {N : Type u_2} {𝒮 : Type u_3} [DecidableEq F] [Listed F] [Inhabited F] [DecidableEq N] [Listed N] [Inhabited N] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {p' : RPol 𝒮} :
            Paper.Link (S p', p'.wnka.ι, p'.wnka.δ, p'.wnka.𝒪)

            We use 𝒪 in stead of λ due it it being reserved for lambda functions in lean

            source
            theorem WeightedNetKAT.Paper.PLDI2026.Section5.Lemma2 {F : Type u_1} {N : Type u_2} {𝒮 : Type u_3} [DecidableEq F] [Listed F] [Inhabited F] [DecidableEq N] [Listed N] [Inhabited N] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {p' : RPol 𝒮} :
            Paper.LinkLem (RPol.𝒜⟦~p'⟧ = G⟦~p'⟧)
            source
            theorem WeightedNetKAT.Paper.PLDI2026.Section5.Corollary1 {F : Type u_1} {N : Type u_2} {𝒮 : Type u_3} [DecidableEq F] [Listed F] [Inhabited F] [DecidableEq N] [Listed N] [Inhabited N] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {p : Pol[F,N,𝒮]} :
            Paper.LinkCol (∀ (π : Pk[F,N]) (h : Pk[F,N] × List Pk[F,N]), (p.sem (π, [])) h = RPol.𝒜⟦~p.toRPol⟧ (π, h.2.reverse, h.1))
            source
            def WeightedNetKAT.Paper.PLDI2026.Section5.Definition4 {𝒮 : Type u_3} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {n : Type u_4} [Fintype n] [DecidableEq n] :
            Paper.Link Matrix.KStar.instKStar
            Equations
            Instances For