Documentation

EqCheckingAbstractInterpretation.Ready.RunningExample

Running Example: Abstract RS Differences #

We use the following processes from the trace running example:

PA = a.PA + a.b.0 PB = a.(PB + b.0) b0 = b.0 (only enables b) PBb0 = PB + b.0 (enables both a and b)

Key RS results:

  1. abstractRSDiffExact_PA_PB_at_F: F-capability witnesses PA ≰_F PB via the concrete observation ⟨a⟩¬b: after one a-step, choose the looping PA branch, which refuses b, while PB moves to PBb0, which enables b.

  2. abstractRSDiffExact_PB_PA_at_S: S-capability witnesses PB ≰_S PA via the simulation observation ⟨a⟩(⟨a⟩⊤ ∧ ⟨b⟩⊤): after one a-step, PB reaches PBb0, which can do both a and b, while the two right-hand successors of PA split the failure: b0 cannot do a, and PA cannot do b.

source
theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PBb0_a_PBb0 :
CCS.Deriv CCS.RunningExample.runEnv CCS.RunningExample.PBb0 CCS.RunningExample.RunAct.a CCS.RunningExample.PBb0

PBb0 can do action a, looping back to itself.

source
theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PA_a_PA :
CCS.Deriv CCS.RunningExample.runEnv CCS.RunningExample.PA CCS.RunningExample.RunAct.a CCS.RunningExample.PA

PA can do action a, looping back to itself.

source
theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PA_a_b0 :
CCS.Deriv CCS.RunningExample.runEnv CCS.RunningExample.PA CCS.RunningExample.RunAct.a CCS.RunningExample.b0

PA can do action a, reaching b0.

source
theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PB_a_PBb0 :
CCS.Deriv CCS.RunningExample.runEnv CCS.RunningExample.PB CCS.RunningExample.RunAct.a CCS.RunningExample.PBb0

PB can do action a, reaching PBb0.

source
theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PBb0_b_zero :
CCS.Deriv CCS.RunningExample.runEnv CCS.RunningExample.PBb0 CCS.RunningExample.RunAct.b CCS.CCS.zero

PBb0 can do action b, reaching zero.

source
theorem EqCheckingAbstractInterpretation.Ready.RunningExample.b0_a_not_enabled :
¬CCS.Enabled CCS.RunningExample.runEnv CCS.RunningExample.b0 CCS.RunningExample.RunAct.a

b0 = b.0 cannot do action a.

source
theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PBb0_a_enabled :
CCS.Enabled CCS.RunningExample.runEnv CCS.RunningExample.PBb0 CCS.RunningExample.RunAct.a
source
theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PBb0_b_enabled :
CCS.Enabled CCS.RunningExample.runEnv CCS.RunningExample.PBb0 CCS.RunningExample.RunAct.b
source
theorem EqCheckingAbstractInterpretation.Ready.RunningExample.zero_no_deriv (a : CCS.RunningExample.RunAct) (p : CCS.RunningExample.RunProc) :
¬CCS.Deriv CCS.RunningExample.runEnv CCS.CCS.zero a p
source
theorem EqCheckingAbstractInterpretation.Ready.RunningExample.b0_deriv_cases {a : CCS.RunningExample.RunAct} {p : CCS.RunningExample.RunProc} (h : CCS.Deriv CCS.RunningExample.runEnv CCS.RunningExample.b0 a p) :
a = CCS.RunningExample.RunAct.b ∧ p = CCS.CCS.zero
source
theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PA_deriv_cases {a : CCS.RunningExample.RunAct} {p : CCS.RunningExample.RunProc} (h : CCS.Deriv CCS.RunningExample.runEnv CCS.RunningExample.PA a p) :
a = CCS.RunningExample.RunAct.a ∧ (p = CCS.RunningExample.PA ∨ p = CCS.RunningExample.b0)
source
theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PB_deriv_cases {a : CCS.RunningExample.RunAct} {p : CCS.RunningExample.RunProc} (h : CCS.Deriv CCS.RunningExample.runEnv CCS.RunningExample.PB a p) :
a = CCS.RunningExample.RunAct.a ∧ p = CCS.RunningExample.PBb0
source
theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PBb0_deriv_cases {a : CCS.RunningExample.RunAct} {p : CCS.RunningExample.RunProc} (h : CCS.Deriv CCS.RunningExample.runEnv CCS.RunningExample.PBb0 a p) :
a = CCS.RunningExample.RunAct.a ∧ p = CCS.RunningExample.PBb0 ∨ a = CCS.RunningExample.RunAct.b ∧ p = CCS.CCS.zero
source
theorem EqCheckingAbstractInterpretation.Ready.RunningExample.single_branch_tail_nil {α : Type} {x : α} {xs : List α} (h : ¬1 < (x :: xs).length) :
xs = []
source
theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PA_b_not_enabled :
¬CCS.Enabled CCS.RunningExample.runEnv CCS.RunningExample.PA CCS.RunningExample.RunAct.b

PA cannot do action b.

source
def EqCheckingAbstractInterpretation.Ready.RunningExample.obs_neg_a :
RSObs CCS.RunningExample.RunAct

The RS observation ¬a (refuse a, no positives). Capability: F.

Equations
Instances For
    source
    def EqCheckingAbstractInterpretation.Ready.RunningExample.obs_neg_b :
    RSObs CCS.RunningExample.RunAct

    The RS observation ¬b (refuse b, no positives). Capability: F.

    Equations
    Instances For
      source
      def EqCheckingAbstractInterpretation.Ready.RunningExample.obs_a_neg_b :
      RSObs CCS.RunningExample.RunAct

      The failure witness ⟨a⟩¬b. Capability: F.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def EqCheckingAbstractInterpretation.Ready.RunningExample.obs_split_ab :
        RSObs CCS.RunningExample.RunAct

        The simulation branching witness ⟨a⟩⊤ ∧ ⟨b⟩⊤. Capability: S.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def EqCheckingAbstractInterpretation.Ready.RunningExample.obs_a_split_ab :
          RSObs CCS.RunningExample.RunAct

          The simulation witness ⟨a⟩(⟨a⟩⊤ ∧ ⟨b⟩⊤). Capability: S.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem EqCheckingAbstractInterpretation.Ready.RunningExample.runLTS_realizes :
            CCS.RunningExample.runLTS.Realizes CCS.RunningExample.runEnv id

            The executable table enumerates precisely the derivatives of its listed CCS states.

            source
            def EqCheckingAbstractInterpretation.Ready.RunningExample.runReadyCapabilities (state : CCS.RunningExample.RunProc) (competitors : FiniteLTS.StateSet CCS.RunningExample.RunProc) :
            List Capability

            Compute the minimal capabilities derived by the finite Ready fixed point.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def EqCheckingAbstractInterpretation.Ready.RunningExample.runReadyFailsAt (threshold : Capability) (state : CCS.RunningExample.RunProc) (competitors : FiniteLTS.StateSet CCS.RunningExample.RunProc) :
              Bool

              Query whether the finite Ready fixed point refutes a capability preorder.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem EqCheckingAbstractInterpretation.Ready.RunningExample.runReadyCapabilities_PA_PB :
                runReadyCapabilities CCS.RunningExample.PA {CCS.RunningExample.PB} = [Capability.F]

                #eval runReadyCapabilities PA {PB} #eval runReadyCapabilities PB {PA} #eval runReadyFailsAt .F PA {PB} #eval runReadyFailsAt .S PB {PA}

                source
                theorem EqCheckingAbstractInterpretation.Ready.RunningExample.runReadyCapabilities_PB_PA :
                runReadyCapabilities CCS.RunningExample.PB {CCS.RunningExample.PA} = [Capability.S]
                source
                theorem EqCheckingAbstractInterpretation.Ready.RunningExample.runReadyCapabilities_PA_empty :
                runReadyCapabilities CCS.RunningExample.PA ∅ = [Capability.T]
                source
                theorem EqCheckingAbstractInterpretation.Ready.RunningExample.runReadyFailsAt_PA_PB_F :
                runReadyFailsAt Capability.F CCS.RunningExample.PA {CCS.RunningExample.PB} = true
                source
                theorem EqCheckingAbstractInterpretation.Ready.RunningExample.runReadyFailsAt_PB_PA_S :
                runReadyFailsAt Capability.S CCS.RunningExample.PB {CCS.RunningExample.PA} = true
                source
                theorem EqCheckingAbstractInterpretation.Ready.RunningExample.runQueryConfigs_diagonal :
                FiniteLTS.queryConfigs CCS.RunningExample.runLTS CCS.RunningExample.PA {CCS.RunningExample.PA, CCS.RunningExample.PB} = [(CCS.RunningExample.PA, {CCS.RunningExample.PA, CCS.RunningExample.PB})]
                source
                theorem EqCheckingAbstractInterpretation.Ready.RunningExample.runCapabilityTable_diagonal :
                FiniteLTS.capabilityTable CCS.RunningExample.runLTS CCS.RunningExample.PA {CCS.RunningExample.PA, CCS.RunningExample.PB} = []
                source
                theorem EqCheckingAbstractInterpretation.Ready.RunningExample.rsObsCap_F_obs_neg_a :
                rsObsCap Capability.F obs_neg_a
                source
                theorem EqCheckingAbstractInterpretation.Ready.RunningExample.rsObsCap_F_obs_a_neg_b :
                rsObsCap Capability.F obs_a_neg_b
                source
                theorem EqCheckingAbstractInterpretation.Ready.RunningExample.rsObsCap_S_obs_a_split_ab :
                rsObsCap Capability.S obs_a_split_ab
                source
                def EqCheckingAbstractInterpretation.Ready.RunningExample.noSRegion (p : CCS.RunningExample.RunProc) (Q : ProcSet CCS.RunningExample.RunAct CCS.RunningExample.RunName) :
                Prop
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def EqCheckingAbstractInterpretation.Ready.RunningExample.rhoNoS :
                  DiffSysRS CCS.RunningExample.RunAct CCS.RunningExample.RunName (RSObs CCS.RunningExample.RunAct)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def EqCheckingAbstractInterpretation.Ready.RunningExample.noFRegion (p : CCS.RunningExample.RunProc) (Q : ProcSet CCS.RunningExample.RunAct CCS.RunningExample.RunName) :
                    Prop
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def EqCheckingAbstractInterpretation.Ready.RunningExample.rhoNoF :
                      DiffSysRS CCS.RunningExample.RunAct CCS.RunningExample.RunName (RSObs CCS.RunningExample.RunAct)
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.rhoNoS_prefixpoint (p : CCS.CCS CCS.RunningExample.RunAct CCS.RunningExample.RunName) (Q : ProcSet CCS.RunningExample.RunAct CCS.RunningExample.RunName) (o : RSObs CCS.RunningExample.RunAct) :
                        DRS CCS.RunningExample.runEnv rhoNoS p Q o → rhoNoS p Q o
                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRS_noS_of_noSRegion {p : CCS.RunningExample.RunProc} {Q : ProcSet CCS.RunningExample.RunAct CCS.RunningExample.RunName} (hRegion : noSRegion p Q) (o : RSObs CCS.RunningExample.RunAct) :
                        lfpDRS CCS.RunningExample.runEnv p Q o → ¬rsObsCap Capability.S o
                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.rhoNoF_prefixpoint (p : CCS.CCS CCS.RunningExample.RunAct CCS.RunningExample.RunName) (Q : ProcSet CCS.RunningExample.RunAct CCS.RunningExample.RunName) (o : RSObs CCS.RunningExample.RunAct) :
                        DRS CCS.RunningExample.runEnv rhoNoF p Q o → rhoNoF p Q o
                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRS_noF_of_noFRegion {p : CCS.RunningExample.RunProc} {Q : ProcSet CCS.RunningExample.RunAct CCS.RunningExample.RunName} (hRegion : noFRegion p Q) (o : RSObs CCS.RunningExample.RunAct) :
                        lfpDRS CCS.RunningExample.runEnv p Q o → ¬rsObsCap Capability.F o
                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRS_b0_PBb0_obs_neg_a :
                        lfpDRS CCS.RunningExample.runEnv CCS.RunningExample.b0 {CCS.RunningExample.PBb0} obs_neg_a

                        b0 refuses a, while PBb0 enables it.

                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRSAbsExactCanon_b0_PBb0_eq_singleton_F (c : Capability) :
                        lfpDRSAbsExactCanon CCS.RunningExample.runEnv CCS.RunningExample.b0 {CCS.RunningExample.PBb0} c ↔ c = Capability.F
                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRS_PA_PB_obs_a_neg_b :
                        lfpDRS CCS.RunningExample.runEnv CCS.RunningExample.PA {CCS.RunningExample.PB} obs_a_neg_b

                        ⟨a⟩¬b distinguishes PA from PB.

                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.abstractRSDiffExact_PA_PB_at_F :
                        abstractFailsAt (lfpDRSAbsExactCanon CCS.RunningExample.runEnv) Capability.F CCS.RunningExample.PA {CCS.RunningExample.PB}

                        The exact-pruned canonical abstraction still witnesses PA ≰_F PB.

                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRS_PBb0_DerivPAa_obs_split_ab :
                        lfpDRS CCS.RunningExample.runEnv CCS.RunningExample.PBb0 (CCS.DerivSetOf CCS.RunningExample.runEnv {CCS.RunningExample.PA} CCS.RunningExample.RunAct.a) obs_split_ab

                        The branching node ⟨a⟩⊤ ∧ ⟨b⟩⊤ distinguishes PBb0 from the a-successors of PA.

                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRS_PB_PA_obs_a_split_ab :
                        lfpDRS CCS.RunningExample.runEnv CCS.RunningExample.PB {CCS.RunningExample.PA} obs_a_split_ab

                        ⟨a⟩(⟨a⟩⊤ ∧ ⟨b⟩⊤) distinguishes PB from PA.

                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.abstractRSDiffExact_PB_PA_at_S :
                        abstractFailsAt (lfpDRSAbsExactCanon CCS.RunningExample.runEnv) Capability.S CCS.RunningExample.PB {CCS.RunningExample.PA}

                        The exact-pruned canonical abstraction still witnesses PB ≰_S PA.

                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRSAbsExactCanon_PBb0_DerivPAa_eq_singleton_S (c : Capability) :
                        lfpDRSAbsExactCanon CCS.RunningExample.runEnv CCS.RunningExample.PBb0 (CCS.DerivSetOf CCS.RunningExample.runEnv {CCS.RunningExample.PA} CCS.RunningExample.RunAct.a) c ↔ c = Capability.S
                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRSAbsExactCanon_PA_PB_eq_singleton_F (c : Capability) :
                        lfpDRSAbsExactCanon CCS.RunningExample.runEnv CCS.RunningExample.PA {CCS.RunningExample.PB} c ↔ c = Capability.F
                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRSAbsExactCanon_PB_PA_eq_singleton_S (c : Capability) :
                        lfpDRSAbsExactCanon CCS.RunningExample.runEnv CCS.RunningExample.PB {CCS.RunningExample.PA} c ↔ c = Capability.S
                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.runReadyCapabilities_PA_PB_correct (capability : Capability) :
                        capability ∈ runReadyCapabilities CCS.RunningExample.PA {CCS.RunningExample.PB} ↔ lfpDRSAbsExactCanon CCS.RunningExample.runEnv CCS.RunningExample.PA {CCS.RunningExample.PB} capability

                        The computed PA result exactly matches the semantic minimal capability set.

                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.runReadyCapabilities_PB_PA_correct (capability : Capability) :
                        capability ∈ runReadyCapabilities CCS.RunningExample.PB {CCS.RunningExample.PA} ↔ lfpDRSAbsExactCanon CCS.RunningExample.runEnv CCS.RunningExample.PB {CCS.RunningExample.PA} capability

                        The computed PB result exactly matches the semantic minimal capability set.

                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.runReadyFailsAt_PA_PB_F_correct :
                        runReadyFailsAt Capability.F CCS.RunningExample.PA {CCS.RunningExample.PB} = true ↔ abstractFailsAt (lfpDRSAbsExactCanon CCS.RunningExample.runEnv) Capability.F CCS.RunningExample.PA {CCS.RunningExample.PB}

                        The computed F witness result agrees with the semantic Ready abstraction.

                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.runReadyFailsAt_PB_PA_S_correct :
                        runReadyFailsAt Capability.S CCS.RunningExample.PB {CCS.RunningExample.PA} = true ↔ abstractFailsAt (lfpDRSAbsExactCanon CCS.RunningExample.runEnv) Capability.S CCS.RunningExample.PB {CCS.RunningExample.PA}

                        The computed S witness result agrees with the semantic Ready abstraction.

                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.not_rsWitnessPreorder_PA_PB :
                        ¬RSWitnessPreorder CCS.RunningExample.runEnv CCS.RunningExample.PA CCS.RunningExample.PB

                        PA is not below PB in the failure-ready witness preorder.

                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.not_rsWitnessPreorder_PB_PA :
                        ¬RSWitnessPreorder CCS.RunningExample.runEnv CCS.RunningExample.PB CCS.RunningExample.PA

                        PB is not below PA in the simulation-ready witness preorder.

                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.not_rsWitnessPreorderAt_F_PA_PB :
                        ¬RSWitnessPreorderAt CCS.RunningExample.runEnv Capability.F CCS.RunningExample.PA CCS.RunningExample.PB

                        The executable F witness refutes PA ≤_F PB.

                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.rsWitnessPreorderAt_S_PA_PB :
                        RSWitnessPreorderAt CCS.RunningExample.runEnv Capability.S CCS.RunningExample.PA CCS.RunningExample.PB

                        PA ≤_S PB: the exact result has only the incomparable F capability.

                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.rsWitnessPreorderAt_F_PB_PA :
                        RSWitnessPreorderAt CCS.RunningExample.runEnv Capability.F CCS.RunningExample.PB CCS.RunningExample.PA

                        PB ≤_F PA: the exact result has only the incomparable S capability.

                        source
                        theorem EqCheckingAbstractInterpretation.Ready.RunningExample.not_rsWitnessPreorderAt_S_PB_PA :
                        ¬RSWitnessPreorderAt CCS.RunningExample.runEnv Capability.S CCS.RunningExample.PB CCS.RunningExample.PA

                        The executable S witness refutes PB ≤_S PA.