inductive OperatorDirectory.Relation (p : MidgardParameters) (t : State.ODirActs) (ops_in : State.OperatorDirectory) : State.OperatorDirectory → Prop

• RegisterOperator {p : MidgardParameters} {t : State.ODirActs} {ops_in : State.OperatorDirectory} (u : PosixTime) (reg_out : MUList.State.ListST PosixTime) (root : Tokens.Elem.TId) : t.act = State.OperActions.Register root → t.info.value = p.required_bond → t.info.validityInternal.upper = some u → MUList.Relation.Rel ops_in.registered (MUList.State.Actions.UnsafePrepend t.info.validator (u + p.registration_duration) root) reg_out → Relation p t ops_in { registered := reg_out, active := ops_in.active, retired := ops_in.retired }
• DeregisterOperator {p : MidgardParameters} {t : State.ODirActs} {ops_in : State.OperatorDirectory} (reg_tkn anch_tkn : Tokens.Elem.TId) (reg_out : MUList.State.ListST PosixTime) : t.act = State.OperActions.Deregister reg_tkn anch_tkn → MUList.Relation.Rel ops_in.registered (MUList.State.Actions.Remove reg_tkn anch_tkn) reg_out → MUList.State.ListST.get_key reg_tkn ops_in.registered = some t.info.validator → Relation p t ops_in { registered := reg_out, active := ops_in.active, retired := ops_in.retired }
• ActivateOperator {p : MidgardParameters} {t : State.ODirActs} {ops_in : State.OperatorDirectory} (reg_tkn ret_non act_anchor : Tokens.Elem.TId) (reg_out : MUList.State.ListST PosixTime) (anch : Tokens.Elem.TId) (opId : OperatorId) (activation_time lower : PosixTime) (active' : MUList.State.ListST (Option PosixTime)) : t.act = State.OperActions.Activate reg_tkn anch ret_non act_anchor → MUList.State.ListST.get_data reg_tkn id ops_in.registered = some activation_time → MUList.Relation.Rel ops_in.registered (MUList.State.Actions.Remove reg_tkn anch) reg_out → MUList.State.ListST.get_key reg_tkn ops_in.registered = some opId → t.info.validityInternal.lower = some lower → activation_time ≤ lower → MOList.Operations.is_non_member (some opId) ret_non ops_in.retired = true → MOList.Relation.Rel ops_in.active (MOList.State.Actions.Insert opId none act_anchor) active' → Relation p t ops_in { registered := reg_out, active := active', retired := ops_in.retired }
• RemDupSlahBondRegistered {p : MidgardParameters} {t : State.ODirActs} {ops_in : State.OperatorDirectory} (opId : MUList.State.Key) (duptkn anch tkn : Tokens.Elem.TId) (reg_out : MUList.State.ListST PosixTime) : t.act = State.OperActions.RemoveDuplicateSlashBond duptkn anch (State.WitnessStatus.Registered tkn) → MUList.Relation.Rel ops_in.registered (MUList.State.Actions.Remove duptkn anch) reg_out → MUList.State.ListST.get_key duptkn ops_in.registered = some opId → p.required_bond * ↑p.slashing_penality ≤ t.info.fee * 100 → MUList.State.ListST.is_member opId tkn reg_out = true → Relation p t ops_in { registered := reg_out, active := ops_in.active, retired := ops_in.retired }
• RemDupSlahBondActive {p : MidgardParameters} {t : State.ODirActs} {ops_in : State.OperatorDirectory} (opId : MUList.State.Key) (remTkn ancTkn : Tokens.Elem.TId) (reg_out : MUList.State.ListST PosixTime) (tkn : Tokens.Elem.TId) : t.act = State.OperActions.RemoveDuplicateSlashBond remTkn ancTkn (State.WitnessStatus.Active tkn) → p.required_bond * ↑p.slashing_penality ≤ t.info.fee * 100 → MUList.Relation.Rel ops_in.registered (MUList.State.Actions.Remove remTkn ancTkn) reg_out → MUList.State.ListST.is_member opId remTkn ops_in.registered = true → MUList.State.ListST.is_member opId tkn ops_in.active = true → Relation p t ops_in { registered := reg_out, active := ops_in.active, retired := ops_in.retired }
• RemDupSlahBondRetired {p : MidgardParameters} {t : State.ODirActs} {ops_in : State.OperatorDirectory} (opId : MUList.State.Key) (remTkn ancTkn : Tokens.Elem.TId) (reg_out : MUList.State.ListST PosixTime) (tkn : Tokens.Elem.TId) : t.act = State.OperActions.RemoveDuplicateSlashBond remTkn ancTkn (State.WitnessStatus.Retired tkn) → MUList.Relation.Rel ops_in.registered (MUList.State.Actions.Remove remTkn ancTkn) reg_out → MUList.State.ListST.get_key remTkn ops_in.registered = some opId → p.required_bond * ↑p.slashing_penality ≤ t.info.fee * 100 → MUList.State.ListST.is_member opId tkn ops_in.retired = true → Relation p t ops_in { registered := reg_out, active := ops_in.active, retired := ops_in.retired }
• ActRemoveOperatorBad {p : MidgardParameters} {t : State.ODirActs} {ops_in : State.OperatorDirectory} (tkn anchor : Tokens.Elem.TId) (active' : MUList.State.ListST (Option PosixTime)) : t.act = State.OperActions.ActRemoveOperatorBad tkn anchor → MOList.Relation.Rel ops_in.active (MOList.State.Actions.Remove tkn anchor) active' → p.required_bond * ↑p.slashing_penality ≤ t.info.fee * 100 → Relation p t ops_in { registered := ops_in.registered, active := active', retired := ops_in.retired }
• ActUpdateBondHold {p : MidgardParameters} {t : State.ODirActs} {ops_in : State.OperatorDirectory} (uu : PosixTime) (active' : MUList.State.ListST (Option PosixTime)) (tkn : Tokens.Elem.TId) : t.act = State.OperActions.UpdateBondHold tkn → t.info.validityInternal.upper = some uu → MOList.Relation.Rel ops_in.active (MOList.State.Actions.ModifyData tkn (some (p.maturity_duration + uu))) active' → Relation p t ops_in { registered := ops_in.registered, active := active', retired := ops_in.retired }
• Retire {p : MidgardParameters} {t : State.ODirActs} {ops_in : State.OperatorDirectory} (token : Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key (Option PosixTime))) (key : MUList.State.Key) (locktime : Option PosixTime) (tkn anchor ret_anchor : Tokens.Elem.TId) (active' retired' : MUList.State.ListST (Option PosixTime)) : t.act = State.OperActions.Retire tkn anchor ret_anchor → MOList.Relation.Rel ops_in.active (MOList.State.Actions.Remove tkn anchor) active' → Tokens.State.Tokens.get tkn ops_in.active = some token → token.data.key = some key → token.data.data = locktime → MOList.Relation.Rel ops_in.retired (MOList.State.Actions.Insert key locktime ret_anchor) retired' → Relation p t ops_in { registered := ops_in.registered, active := active', retired := retired' }
• RecoverBondNoUnlockTime {p : MidgardParameters} {t : State.ODirActs} {ops_in : State.OperatorDirectory} (tkn : Tokens.Elem.TId) (retired' : MUList.State.ListST (Option PosixTime)) (anchor : Tokens.Elem.TId) : t.act = State.OperActions.RecoverBond tkn anchor → MUList.State.ListST.get_data tkn id ops_in.retired = some none → MOList.Relation.Rel ops_in.retired (MOList.State.Actions.Remove tkn anchor) retired' → Relation p t ops_in { registered := ops_in.registered, active := ops_in.active, retired := retired' }
• RecoverBondUnlockTime {p : MidgardParameters} {t : State.ODirActs} {ops_in : State.OperatorDirectory} (tkn anchor : Tokens.Elem.TId) (unlockTime ll : PosixTime) (retired' : MUList.State.ListST (Option PosixTime)) : t.act = State.OperActions.RecoverBond tkn anchor → MUList.State.ListST.get_data tkn id ops_in.retired = some (some unlockTime) → t.info.validityInternal.lower = some ll → unlockTime ≤ ll → MOList.Relation.Rel ops_in.retired (MOList.State.Actions.Remove tkn anchor) retired' → Relation p t ops_in { registered := ops_in.registered, active := ops_in.active, retired := retired' }
• RetireRemove {p : MidgardParameters} {t : State.ODirActs} {ops_in : State.OperatorDirectory} (tkn anchor : Tokens.Elem.TId) (retired' : MUList.State.ListST (Option PosixTime)) : t.act = State.OperActions.RetRemoveOperatorBad tkn anchor → p.required_bond * ↑p.slashing_penality ≤ t.info.fee * 100 → MOList.Relation.Rel ops_in.retired (MOList.State.Actions.Remove tkn anchor) retired' → Relation p t ops_in { registered := ops_in.registered, active := ops_in.active, retired := retired' }

def OperatorDirectory.Notation.«term_=>OpD⟨_,_;_⟩_» : Lean.TrailingParserDescr

Equations

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

def OperatorDirectory.Rechable.operatorsSteps : StepMachines.StepMachine MidgardParameters State.ODirActs State.OperatorDirectory

Equations

• OperatorDirectory.Rechable.operatorsSteps = { init := OperatorDirectory.State.OperatorDirectory.init, STS := OperatorDirectory.Relation }