Extra Stateful Relations definitions.

Main Results

• Transitive closure (plus-relation, no skip) TransPlus

• End of step relation NoStep

• Big Step relation as depleted small step actions CompletedStep. A conjuntion of the above.

def Definition.StepRel {P I S : Type} : Type

Equations

• Definition.StepRel = (P → I → S → S → Prop)

def Definition.StrongStep {P I S : Type} [DecidableEq S] (Step : P → I → S → S → Prop) : Prop

Equations

• Definition.StrongStep Step = ∀ (p : P) (i : I) (s s' : S), Step p i s s' → (s != s') = true

def Definition.Disabled {P I S : Type} (RStep : P → I → S → S → Prop) (p : P) (s : S) : Prop

Equations

• Definition.Disabled RStep p s = ∀ (i : I) (s' : S), ¬RStep p i s s'

Enabled Predicate

Enabled Predicate indicates there is a way how making the relatin progress.

In our case, we want to say that in a case where we are in a fraudulent situation (state), the action of going to a less fraudulent_ state is possible.

def Definition.Enabled {P I S : Type} (RStep : P → I → S → S → Prop) (p : P) (s : S) : Prop

Equations

• Definition.Enabled RStep p s = ∃ (i : I), ∃ (s' : S), RStep p i s s'

Invariants

def Relations.Invariant {P I S : Type} (STS : P → I → S → S → Prop) (Pred : S → Prop) : Prop

Equations

• Relations.Invariant STS Pred = ∀ (p : P) (i : I) (s s' : S), Pred s → STS p i s s' → Pred s'

inductive Relations.ReachableSTPlus {P I S : Type} (p : P) (STS : P → I → S → S → Prop) : S → S → Prop

• One {P I S : Type} {p : P} {STS : P → I → S → S → Prop} (s s' : S) (i : I) : STS p i s s' → ReachableSTPlus p STS s s'
• StepBkw {P I S : Type} {p : P} {STS : P → I → S → S → Prop} (s s' s'' : S) (i : I) : STS p i s'' s' → ReachableSTPlus p STS s s'' → ReachableSTPlus p STS s s'

def Relations.Reaches {P I S : Type} (p : P) (STS : P → I → S → S → Prop) (i e : S) (ls : List (I × S)) : Prop

Equations

• Relations.Reaches p STS i e [] = (i = e)
• Relations.Reaches p STS i e (a :: as) = (STS p a.fst i a.snd ∧ Relations.Reaches p STS a.snd e as)

structure StepMachines.StepMachine (P I S : Type) : Type

• init : S
• STS : P → I → S → S → Prop

def StepMachines.StepProduct {P I S_1 S_2 : Type} (m1 : StepMachine P I S_1) (m2 : StepMachine P I S_2) : StepMachine P I (S_1 × S_2)

Equations

• StepMachines.StepProduct m1 m2 = { init := (m1.init, m2.init), STS := fun (p : P) (i : I) (s s' : S_1 × S_2) => m1.STS p i s.fst s'.fst ∧ m2.STS p i s.snd s'.snd }

def StepMachines.MonitorProduct {P I S_1 S_2 : Type} (m1 : StepMachine P I S_1) (m2 : StepMachine (P × S_1) I S_2) : StepMachine P I (S_1 × S_2)

Equations

• StepMachines.MonitorProduct m1 m2 = { init := (m1.init, m2.init), STS := fun (p : P) (i : I) (s s' : S_1 × S_2) => m1.STS p i s.fst s'.fst ∧ m2.STS (p, s.fst) i s.snd s'.snd }

def StepMachines.StepMachine.FromInit {P I S : Type} (SM : StepMachine P I S) (p : P) (s : S) : Prop

Equations

• SM.FromInit p s = (SM.init = s ∨ Relations.ReachableSTPlus p SM.STS SM.init s)

inductive StepMachines.StepMachine.IFromInit {P I S : Type} (SM : StepMachine P I S) (p : P) (s : S) : Type

• Init {P I S : Type} {SM : StepMachine P I S} {p : P} {s : S} : SM.init = s → SM.IFromInit p s
• Reachable {P I S : Type} {SM : StepMachine P I S} {p : P} {s : S} : Relations.ReachableSTPlus p SM.STS SM.init s → SM.IFromInit p s

structure StepMachines.ReachInductionStepMachine {P I S : Type} (p : P) (SM : StepMachine P I S) (Pred : S → Prop) : Prop

• base_case : Pred SM.init
• ind_case (s s' : S) (i : I) : Pred s → SM.FromInit p s → SM.STS p i s s' → Pred s'

structure StepMachines.InductionStepMachine {P I S : Type} (p : P) (SM : StepMachine P I S) (Pred : S → Prop) : Prop

• base_case : Pred SM.init
• ind_case (s s' : S) (i : I) : Pred s → SM.STS p i s s' → Pred s'

def StepMachines.reachable_is_inductive {P I S : Type} {p : P} {sm : StepMachine P I S} : InductionStepMachine p sm (sm.FromInit p)

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev StepMachines.StepMachine.AfterInit {P I S : Type} (SM : StepMachine P I S) (p : P) (s : S) : Prop

Equations

• SM.AfterInit p s = Relations.ReachableSTPlus p SM.STS SM.init s

theorem StepMachines.ApplyInd {P I S : Type} {Pred : S → Prop} {SM : StepMachine P I S} (p : P) (ind : InductionStepMachine p SM Pred) (s : S) (reachable : Relations.ReachableSTPlus p SM.STS SM.init s) : Pred s

theorem StepMachines.ApplyFromInit {P I S : Type} {Pred : S → Prop} {SM : StepMachine P I S} (p : P) (ind : InductionStepMachine p SM Pred) (s : S) (reachable : SM.FromInit p s) : Pred s

theorem StepMachines.ApplyFromInitReach {P I S : Type} {Pred : S → Prop} {SM : StepMachine P I S} (p : P) (ind : ReachInductionStepMachine p SM Pred) (s : S) (reachable : SM.FromInit p s) : Pred s

def Products.Conditional_Joint {GP : Sort u_1} {P₁ : Type u_2} {P₂ : Type u_3} {S₁ : Type u_4} {S₂ : Type u_5} {A₁ : Type u_6} {A₂ : Type u_7} {O₁ : Type u_8} {O₂ : Type u_9} (R₁ : GP → P₁ → S₁ → A₁ → O₁ → Prop) (R₂ : GP → P₂ → S₂ → A₂ → O₂ → Prop) (Cond : S₁ → A₁ → S₂ → A₂ → Prop) : GP → P₁ × P₂ → S₁ × S₂ → A₁ × A₂ → O₁ × O₂ → Prop

Equations

• Products.Conditional_Joint R₁ R₂ Cond gp pp ss aa oo = (R₁ gp pp.fst ss.fst aa.fst oo.fst ∧ R₂ gp pp.snd ss.snd aa.snd oo.snd ∧ Cond ss.fst aa.fst ss.snd aa.snd)

def Products.Joint {GP : Sort u_1} {P₁ : Type u_2} {P₂ : Type u_3} {S₁ : Type u_4} {S₂ : Type u_5} {A₁ : Type u_6} {A₂ : Type u_7} {O₁ : Type u_8} {O₂ : Type u_9} (R₁ : GP → P₁ → S₁ → A₁ → O₁ → Prop) (R₂ : GP → P₂ → S₂ → A₂ → O₂ → Prop) : GP → P₁ × P₂ → S₁ × S₂ → A₁ × A₂ → O₁ × O₂ → Prop

Equations

• Products.Joint R₁ R₂ gp pp ss aa oo = (R₁ gp pp.fst ss.fst aa.fst oo.fst ∧ R₂ gp pp.snd ss.snd aa.snd oo.snd)

def InterfaceRestrictions.SubRel {GP : Sort u_1} {P : Sort u_2} {S : Sort u_3} {Ab : Sort u_4} {At : Sort u_5} {O : Sort u_6} (sup : GP → P → S → At → O → Prop) (lift : Ab → At) (gp : GP) (p : P) (s : S) : Ab → O → Prop

Equations

• InterfaceRestrictions.SubRel sup lift gp p s a o = sup gp p s (lift a) o

inductive InterfaceRestrictions.ConditionalSub {GP : Sort u_1} {P : Sort u_2} {S : Sort u_3} {Ab : Sort u_4} {At : Type u_5} {O : Sort u_6} (sup : GP → P → S → At → O → Prop) (lift : S → Ab → Option At) : GP → P → S → Ab → O → Prop

• condLift {GP : Sort u_1} {P : Sort u_2} {S : Sort u_3} {Ab : Sort u_4} {At : Type u_5} {O : Sort u_6} {sup : GP → P → S → At → O → Prop} {lift : S → Ab → Option At} {gp : GP} {p : P} {s : S} {ab : Ab} {t : At} {o : O} (cond : lift s ab = some t) (step : sup gp p s t o) : ConditionalSub sup lift gp p s ab o