theorem EqCheckingAbstractInterpretation.Trace.FiniteLTS.successors_closed {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (hNextClosed : ∀ (state : State) (action : Action) (target : State), state ∈ lts.states → target ∈ lts.next state action → target ∈ lts.states) (config successor : Config State) (hConfig : config ∈ FiniteEvaluator.configUniverse lts) (hSuccessor : successor ∈ successors lts config) : successor ∈ FiniteEvaluator.configUniverse lts

theorem EqCheckingAbstractInterpretation.Trace.FiniteLTS.decodeSet_shift_iff {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (competitors : StateSet State) (action : Action) (process : CCS.CCS Action Name) (hCompetitors : ∀ competitor ∈ competitors, competitor ∈ lts.states) : CCS.FiniteLTS.decodeSet decode (FiniteEvaluator.shift lts competitors action) process ↔ CCS.DerivSetOf env (CCS.FiniteLTS.decodeSet decode competitors) action process

Decoding an executable shift agrees with the semantic lifted derivative.

theorem EqCheckingAbstractInterpretation.Trace.FiniteLTS.marks_sound {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (marked : MarkerTable State) (state : State) (competitors : StateSet State) (hConfig : (state, competitors) ∈ FiniteEvaluator.configUniverse lts) (hMarked : marks lts marked state competitors = true) (hSound : ∀ (successor : State) (shifted : FiniteEvaluator.FSet State), FiniteEvaluator.configMem (successor, shifted) marked = true → AbstractDiff env (decode successor) (CCS.FiniteLTS.decodeSet decode shifted)) : AbstractDiff env (decode state) (CCS.FiniteLTS.decodeSet decode competitors)

One Boolean Trace marker step is sound for the semantic abstract transformer.

theorem EqCheckingAbstractInterpretation.Trace.FiniteLTS.saturateN_sound {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (count : ℕ) (state : State) (competitors : StateSet State) (hMember : (state, competitors) ∈ FiniteEvaluator.saturateN (FiniteEvaluator.configUniverse lts) FiniteEvaluator.configMem (fun (marked : List (FiniteEvaluator.StateConfig State)) (config : FiniteEvaluator.StateConfig State) => marks lts marked config.1 config.2) count) : AbstractDiff env (decode state) (CCS.FiniteLTS.decodeSet decode competitors)

Each finite saturation approximation is semantically sound.

theorem EqCheckingAbstractInterpretation.Trace.FiniteLTS.abstractDiff_sound {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (state : State) (competitors : StateSet State) (hAbstractDiff : abstractDiff lts state competitors = true) : AbstractDiff env (decode state) (CCS.FiniteLTS.decodeSet decode competitors)

The executable Trace result implies the semantic abstract difference.

def EqCheckingAbstractInterpretation.Trace.FiniteLTS.marksSet {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (marked : Set (Config State)) (config : Config State) : Prop

Proof-facing form of one Trace marker rule.

Equations

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

theorem EqCheckingAbstractInterpretation.Trace.FiniteLTS.marks_iff_marksSet {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (marked : MarkerTable State) (state : State) (competitors : StateSet State) : marks lts marked state competitors = true ↔ marksSet lts ↑(List.toFinset marked) (state, competitors)

The Boolean Trace marker rule reflects its proof-facing form.

theorem EqCheckingAbstractInterpretation.Trace.FiniteLTS.marksSet_mono {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) {left right : Set (Config State)} (hSubset : left ⊆ right) (config : Config State) : marksSet lts left config → marksSet lts right config

The proof-facing Trace marker relation is monotone in its table argument.

theorem EqCheckingAbstractInterpretation.Trace.FiniteLTS.markerTable_toFinset_eq_tableLfp {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) : ↑(List.toFinset (markerTable lts)) = FiniteEvaluator.tableLfp (↑(FiniteEvaluator.configUniverse lts).toFinset) (marksSet lts) ⋯

The executable Trace marker table denotes the generic least marker table.

theorem EqCheckingAbstractInterpretation.Trace.FiniteLTS.abstractDiffReachable_eq_abstractDiff {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (hNextClosed : ∀ (source : State) (action : Action) (target : State), source ∈ lts.states → target ∈ lts.next source action → target ∈ lts.states) (state : State) (competitors : StateSet State) (hState : state ∈ lts.states) (hCompetitors : competitors ⊆ lts.states.toFinset) : abstractDiffReachable lts state competitors = abstractDiff lts state competitors

Query-local evaluation agrees with the full marker table on closed finite models.

theorem EqCheckingAbstractInterpretation.Trace.FiniteLTS.markerTable_closed {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) (competitors : StateSet State) (hConfig : (state, competitors) ∈ FiniteEvaluator.configUniverse lts) (hMarked : marks lts (markerTable lts) state competitors = true) : FiniteEvaluator.configMem (state, competitors) (markerTable lts) = true

A configuration satisfying the Trace marker rule belongs to the final marker table.

def EqCheckingAbstractInterpretation.Trace.FiniteLTS.markerPredicate {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (decode : State → CCS.CCS Action Name) : AbsDiffSys Action Name

Semantic pairs represented by the finite model inherit the final marker-table result.

Equations

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

theorem EqCheckingAbstractInterpretation.Trace.FiniteLTS.markerPredicate_prefixpoint {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (process : CCS.CCS Action Name) (processes : CCS.ProcSet Action Name) : DTrSharp env (markerPredicate lts decode) process processes → markerPredicate lts decode process processes

markerPredicate is a semantic pre-fixpoint of the Trace abstract transformer.

theorem EqCheckingAbstractInterpretation.Trace.FiniteLTS.abstractDiff_complete {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (state : State) (competitors : StateSet State) (hState : state ∈ lts.states) (hCompetitors : competitors ⊆ lts.states.toFinset) (hAbstractDiff : AbstractDiff env (decode state) (CCS.FiniteLTS.decodeSet decode competitors)) : abstractDiff lts state competitors = true

The semantic Trace abstract difference is computed by the final marker table on represented inputs.

theorem EqCheckingAbstractInterpretation.Trace.FiniteLTS.abstractDiff_iff {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (state : State) (competitors : StateSet State) (hState : state ∈ lts.states) (hCompetitors : competitors ⊆ lts.states.toFinset) : abstractDiff lts state competitors = true ↔ AbstractDiff env (decode state) (CCS.FiniteLTS.decodeSet decode competitors)

The executable and semantic Trace abstract differences agree on represented inputs.

structure EqCheckingAbstractInterpretation.Trace.FiniteLTS.AbstractDiffCorrect {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) : Prop

Certificate that a finite transition system realizes its decoded CCS model. The executable/semantic correspondence is derived by abstractDiff_correct.

• realizes : lts.Realizes env decode

theorem EqCheckingAbstractInterpretation.Trace.FiniteLTS.abstractDiff_correct {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (certificate : AbstractDiffCorrect lts env decode) (state : State) (competitors : StateSet State) (hState : state ∈ lts.states) (hCompetitors : competitors ⊆ lts.states.toFinset) : abstractDiff lts state competitors = true ↔ AbstractDiff env (decode state) (CCS.FiniteLTS.decodeSet decode competitors)

Generic connection from a realized executable finite model to AbstractDiff.

theorem EqCheckingAbstractInterpretation.Trace.FiniteLTS.abstractDiffReachable_correct {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (certificate : AbstractDiffCorrect lts env decode) (state : State) (competitors : StateSet State) (hState : state ∈ lts.states) (hCompetitors : competitors ⊆ lts.states.toFinset) : abstractDiffReachable lts state competitors = true ↔ AbstractDiff env (decode state) (CCS.FiniteLTS.decodeSet decode competitors)

The executable query-local marker agrees with CCS trace semantics.

theorem EqCheckingAbstractInterpretation.Trace.FiniteLTS.tracePreordered_correct {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (certificate : AbstractDiffCorrect lts env decode) (left right : State) (hLeft : left ∈ lts.states) (hRight : right ∈ lts.states) : tracePreordered lts left right = true ↔ TracePreorder env (decode left) (decode right)

The executable Boolean preorder agrees with semantic trace inclusion.