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.

inductive EqCheckingAbstractInterpretation.Ready.RunningExample.RunAct : Type

• a : RunAct
• b : RunAct

@[implicit_reducible]

instance EqCheckingAbstractInterpretation.Ready.RunningExample.instDecidableEqRunAct : DecidableEq RunAct

Equations

• EqCheckingAbstractInterpretation.Ready.RunningExample.instDecidableEqRunAct x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def EqCheckingAbstractInterpretation.Ready.RunningExample.instReprRunAct.repr : RunAct → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance EqCheckingAbstractInterpretation.Ready.RunningExample.instReprRunAct : Repr RunAct

Equations

• EqCheckingAbstractInterpretation.Ready.RunningExample.instReprRunAct = { reprPrec := EqCheckingAbstractInterpretation.Ready.RunningExample.instReprRunAct.repr }

inductive EqCheckingAbstractInterpretation.Ready.RunningExample.RunName : Type

• PA : RunName
• PB : RunName

@[implicit_reducible]

instance EqCheckingAbstractInterpretation.Ready.RunningExample.instDecidableEqRunName : DecidableEq RunName

Equations

• EqCheckingAbstractInterpretation.Ready.RunningExample.instDecidableEqRunName x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def EqCheckingAbstractInterpretation.Ready.RunningExample.instReprRunName.repr : RunName → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance EqCheckingAbstractInterpretation.Ready.RunningExample.instReprRunName : Repr RunName

Equations

• EqCheckingAbstractInterpretation.Ready.RunningExample.instReprRunName = { reprPrec := EqCheckingAbstractInterpretation.Ready.RunningExample.instReprRunName.repr }

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Ready.RunningExample.RunProc : Type

Equations

• One or more equations did not get rendered due to their size.

def EqCheckingAbstractInterpretation.Ready.RunningExample.PA : RunProc

Equations

• EqCheckingAbstractInterpretation.Ready.RunningExample.PA = EqCheckingAbstractInterpretation.CCS.CCS.var EqCheckingAbstractInterpretation.Ready.RunningExample.RunName.PA

def EqCheckingAbstractInterpretation.Ready.RunningExample.PB : RunProc

Equations

• EqCheckingAbstractInterpretation.Ready.RunningExample.PB = EqCheckingAbstractInterpretation.CCS.CCS.var EqCheckingAbstractInterpretation.Ready.RunningExample.RunName.PB

def EqCheckingAbstractInterpretation.Ready.RunningExample.runEnv : CCS.Env RunAct RunName

PA ↦ a.PA + a.b.0, PB ↦ a.(PB + b.0)

Equations

• One or more equations did not get rendered due to their size.

def EqCheckingAbstractInterpretation.Ready.RunningExample.b0 : RunProc

Equations

• One or more equations did not get rendered due to their size.

def EqCheckingAbstractInterpretation.Ready.RunningExample.PBb0 : RunProc

Equations

• One or more equations did not get rendered due to their size.

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

PBb0 can do action a, looping back to itself.

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

PA can do action a, looping back to itself.

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

PA can do action a, reaching b0.

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

PB can do action a, reaching PBb0.

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

PBb0 can do action b, reaching zero.

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

b0 = b.0 cannot do action a.

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PBb0_a_enabled : CCS.Enabled runEnv PBb0 RunAct.a

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PBb0_b_enabled : CCS.Enabled runEnv PBb0 RunAct.b

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.zero_no_deriv (a : RunAct) (p : RunProc) : ¬CCS.Deriv runEnv CCS.CCS.zero a p

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.b0_deriv_cases {a : RunAct} {p : RunProc} (h : CCS.Deriv runEnv b0 a p) : a = RunAct.b ∧ p = CCS.CCS.zero

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PA_deriv_cases {a : RunAct} {p : RunProc} (h : CCS.Deriv runEnv PA a p) : a = RunAct.a ∧ (p = PA ∨ p = b0)

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PB_deriv_cases {a : RunAct} {p : RunProc} (h : CCS.Deriv runEnv PB a p) : a = RunAct.a ∧ p = PBb0

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PBb0_deriv_cases {a : RunAct} {p : RunProc} (h : CCS.Deriv runEnv PBb0 a p) : a = RunAct.a ∧ p = PBb0 ∨ a = RunAct.b ∧ p = CCS.CCS.zero

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.single_branch_tail_nil {α : Type} {x : α} {xs : List α} (h : ¬1 < (x :: xs).length) : xs = []

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.PA_b_not_enabled : ¬CCS.Enabled runEnv PA RunAct.b

PA cannot do action b.

def EqCheckingAbstractInterpretation.Ready.RunningExample.obs_neg_a : RSObs RunAct

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

Equations

• EqCheckingAbstractInterpretation.Ready.RunningExample.obs_neg_a = EqCheckingAbstractInterpretation.Ready.RSObs.node [] [EqCheckingAbstractInterpretation.Ready.RunningExample.RunAct.a]

def EqCheckingAbstractInterpretation.Ready.RunningExample.obs_neg_b : RSObs RunAct

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

Equations

• EqCheckingAbstractInterpretation.Ready.RunningExample.obs_neg_b = EqCheckingAbstractInterpretation.Ready.RSObs.node [] [EqCheckingAbstractInterpretation.Ready.RunningExample.RunAct.b]

def EqCheckingAbstractInterpretation.Ready.RunningExample.obs_a_neg_b : RSObs RunAct

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

Equations

• One or more equations did not get rendered due to their size.

def EqCheckingAbstractInterpretation.Ready.RunningExample.obs_split_ab : RSObs RunAct

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

Equations

• One or more equations did not get rendered due to their size.

def EqCheckingAbstractInterpretation.Ready.RunningExample.obs_a_split_ab : RSObs RunAct

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

Equations

• One or more equations did not get rendered due to their size.

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.rsObsCap_F_obs_neg_a : rsObsCap Capability.F obs_neg_a

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.rsObsCap_F_obs_a_neg_b : rsObsCap Capability.F obs_a_neg_b

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.rsObsCap_S_obs_a_split_ab : rsObsCap Capability.S obs_a_split_ab

def EqCheckingAbstractInterpretation.Ready.RunningExample.noSRegion (p : RunProc) (Q : ProcSet RunAct RunName) : Prop

Equations

• One or more equations did not get rendered due to their size.

def EqCheckingAbstractInterpretation.Ready.RunningExample.rhoNoS : DiffSysRS RunAct RunName (RSObs RunAct)

Equations

• One or more equations did not get rendered due to their size.

def EqCheckingAbstractInterpretation.Ready.RunningExample.noFRegion (p : RunProc) (Q : ProcSet RunAct RunName) : Prop

Equations

• One or more equations did not get rendered due to their size.

def EqCheckingAbstractInterpretation.Ready.RunningExample.rhoNoF : DiffSysRS RunAct RunName (RSObs RunAct)

Equations

• One or more equations did not get rendered due to their size.

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.rhoNoS_prefixpoint (p : CCS.CCS RunAct RunName) (Q : ProcSet RunAct RunName) (o : RSObs RunAct) : DRS runEnv rhoNoS p Q o → rhoNoS p Q o

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRS_noS_of_noSRegion {p : RunProc} {Q : ProcSet RunAct RunName} (hRegion : noSRegion p Q) (o : RSObs RunAct) : lfpDRS runEnv p Q o → ¬rsObsCap Capability.S o

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.rhoNoF_prefixpoint (p : CCS.CCS RunAct RunName) (Q : ProcSet RunAct RunName) (o : RSObs RunAct) : DRS runEnv rhoNoF p Q o → rhoNoF p Q o

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRS_noF_of_noFRegion {p : RunProc} {Q : ProcSet RunAct RunName} (hRegion : noFRegion p Q) (o : RSObs RunAct) : lfpDRS runEnv p Q o → ¬rsObsCap Capability.F o

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRS_b0_PBb0_obs_neg_a : lfpDRS runEnv b0 {PBb0} obs_neg_a

b0 refuses a, while PBb0 enables it.

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRSAbsExactCanon_b0_PBb0_eq_singleton_F (c : Capability) : lfpDRSAbsExactCanon runEnv b0 {PBb0} c ↔ c = Capability.F

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRS_PA_PB_obs_a_neg_b : lfpDRS runEnv PA {PB} obs_a_neg_b

⟨a⟩¬b distinguishes PA from PB.

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

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

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

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

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

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

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

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

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRSAbsExactCanon_PBb0_DerivPAa_eq_singleton_S (c : Capability) : lfpDRSAbsExactCanon runEnv PBb0 (CCS.DerivSetOf runEnv {PA} RunAct.a) c ↔ c = Capability.S

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRSAbsExactCanon_PA_PB_eq_singleton_F (c : Capability) : lfpDRSAbsExactCanon runEnv PA {PB} c ↔ c = Capability.F

theorem EqCheckingAbstractInterpretation.Ready.RunningExample.lfpDRSAbsExactCanon_PB_PA_eq_singleton_S (c : Capability) : lfpDRSAbsExactCanon runEnv PB {PA} c ↔ c = Capability.S