Operators Directory Properties.

The properties listed in this file are not optimistic. The invariants listed here are invariant/properties of the Operator Directory module.

List Invariants.

After detecting possible violations on one of the basic building blocks: key-unordered singly linked lists. Here we proposed a new property checking that the list is kept connected

Connected means that there is a path from root to last involving all tokens in existence. In particular, this property prevents operators to be left as dangling nodes. Dangling nodes cannot recover their bonds.

def OperatorDirectory.Properties.ListConsistency.ConnectedList (opdir : State.OperatorDirectory) : Prop

The following definition states the desired property.

Equations

• OperatorDirectory.Properties.ListConsistency.ConnectedList opdir = ∃ (ls : List Tokens.Elem.TId), Paths.Traversals.CompleteTraversal ls opdir.registered = true

To prove it, we used a trace generation to find counter-examples. See FMMidgard.DataStructures.List.SimProp+160.

In this case, it means that a reachable OperatorsDirectory state, contains reachable states on each of its lists.

theorem OperatorDirectory.Properties.ListConsistency.registered_reachable {ops : State.OperatorDirectory} {p : MidgardParameters} (reach_state : Computational.Relation.StepMachine.FromInit p ops) : (MUList.Computational.StepList 0).FromInit () ops.registered

theorem OperatorDirectory.Properties.ListConsistency.active_reachable {ops : State.OperatorDirectory} {p : MidgardParameters} (reach_state : Computational.Relation.StepMachine.FromInit p ops) : (MOList.Relation.StepListOrdered none).FromInit () ops.active

theorem OperatorDirectory.Properties.ListConsistency.retired_reachable {ops : State.OperatorDirectory} {p : MidgardParameters} (reach_state : Computational.Relation.StepMachine.FromInit p ops) : (MOList.Relation.StepListOrdered none).FromInit () ops.retired

Actions Pre/Post condictions and Properties.

Activate Properties.

Activate opDir ! .Activate tkn anch ↝ opsDir' conditions are:

• Tokens exists. In Cardano is proved by showing them, in our representation, it is enough by /presenting/ their ids.

• Token anch is anchor for tkn proven by opDir.registered.is_anchor tkn anch. For this to be a valid proof, tkn and anch must exists (first bullet.)

• Because we use the Activated queue, and activated is sorted, we known that the key of tkn was not activate and now is. In symbols, we have

  1. opDir.registered.get_key tkn ∉ opsDir.active and
  2. ⟨opDir.registered.get_key tkn , .none ⟩ ∈ opDir'.active.

def OperatorDirectory.Properties.Actions.activate_prop_def (tkn anch act_anch ret_non : Tokens.Elem.TId) (opDir opDir' : State.OperatorDirectory) : Prop

Equations

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

theorem OperatorDirectory.Properties.Actions.activate_props {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anch ret_non act_tkn : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.Activate tkn anch ret_non act_tkn, info := i } opDir opDir') : activate_prop_def tkn anch act_tkn ret_non opDir opDir'

theorem OperatorDirectory.Properties.Actions.next_activate_props {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anch ret_non act_anchor : Tokens.Elem.TId} (Step : StateMachine.next p { act := State.OperActions.Activate tkn anch ret_non act_anchor, info := i } opDir = ComputationResult.Success opDir') : activate_prop_def tkn anch act_anchor ret_non opDir opDir'

theorem OperatorDirectory.Properties.Actions.activate_insert_activates {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anch ret_non act_anchor : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.Activate tkn anch ret_non act_anchor, info := i } opDir opDir') : ∃ (k : MUList.State.Key), MOList.Relation.Rel opDir.active (MOList.State.Actions.Insert k none act_anchor) opDir'.active ∧ MUList.State.ListST.get_key tkn opDir.registered = some k

After activation we insert a node in the active list with the same key

theorem OperatorDirectory.Properties.Actions.activate_register_removes {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anch ret_non act_anchor : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.Activate tkn anch ret_non act_anchor, info := i } opDir opDir') : MUList.Relation.Rel opDir.registered (MUList.State.Actions.Remove tkn anch) opDir'.registered

Activating a node removes it from the registered list

theorem OperatorDirectory.Properties.Actions.activate_register_not_self {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anch ret_non act_anchor : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.Activate tkn anch ret_non act_anchor, info := i } opDir opDir') : ¬tkn = anch

We cannot activate operators using themselves as anchors.

theorem OperatorDirectory.Properties.Actions.activate_register_non_retired {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anch ret_non act_anchor : Tokens.Elem.TId} {key : MUList.State.Key} (Step : Relation p { act := State.OperActions.Activate tkn anch ret_non act_anchor, info := i } opDir opDir') (Key : MUList.State.ListST.get_key tkn opDir.registered = some key) : MOList.Operations.is_non_member (some key) ret_non opDir.retired = true

Activation of no-retired operators.

theorem OperatorDirectory.Properties.Actions.activate_same_retired {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {toact anchor_reg ret_non act_anch : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.Activate toact anchor_reg ret_non act_anch, info := i } opDir opDir') : opDir'.retired = opDir.retired

Activation does not modify retired operators.

theorem OperatorDirectory.Properties.Actions.activate_register_membership {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anch ret_non act_anchor : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.Activate tkn anch ret_non act_anchor, info := i } opDir opDir') : (∀ (t : Tokens.Elem.TId), ¬t = tkn ∧ ¬t = anch → Tokens.State.Tokens.get t opDir'.registered = Tokens.State.Tokens.get t opDir.registered) ∧ Tokens.State.Tokens.get tkn opDir'.registered = none ∧ ∀ (e : Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key PosixTime)), Tokens.State.Tokens.get anch opDir.registered = some e → Tokens.State.Tokens.get anch opDir'.registered = some { name := e.name, data := have __src := e.data; { key := __src.key, link := joinM ((fun (x : Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key PosixTime)) => x.data.link) <$> Tokens.State.Tokens.get tkn opDir.registered), data := __src.data }, id := e.id }

Activation removes a registered operator, modifies it's anchor properly, and all other registered operators remain the same.

Retiring Properties.

theorem OperatorDirectory.Properties.Actions.retired_active_substep {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anchor ret_anchor : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.Retire tkn anchor ret_anchor, info := i } opDir opDir') : MOList.Relation.Rel opDir.active (MOList.State.Actions.Remove tkn anchor) opDir'.active

Retiring removes an operator from the active list.

theorem OperatorDirectory.Properties.Actions.retired_retired_step {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anchor ret_anchor : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.Retire tkn anchor ret_anchor, info := i } opDir opDir') : MUList.State.ListST.get_data tkn id opDir.active = MUList.State.ListST.get_data (Tokens.State.Tokens.last_id opDir'.retired) id opDir'.retired ∧ MUList.State.ListST.get_key tkn opDir.active = MUList.State.ListST.get_key (Tokens.State.Tokens.last_id opDir'.retired) opDir'.retired ∧ ∃ (key : MUList.State.Key) (md : Option PosixTime), MOList.Relation.Rel opDir.retired (MOList.State.Actions.Insert key md ret_anchor) opDir'.retired

Retiring operators adds the retiring operator to the retired ops list.

theorem OperatorDirectory.Properties.Actions.retired_registered {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anchor ret_anchor : Tokens.Elem.TId} (Step : StateMachine.next p { act := State.OperActions.Retire tkn anchor ret_anchor, info := i } opDir = ComputationResult.Success opDir') : opDir.registered = opDir'.registered

Retiring operators do not modify the registered list.

Register Operators

theorem OperatorDirectory.Properties.Actions.register_same_active {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.Register tkn, info := i } opDir opDir') : opDir'.active = opDir.active

Registering operators do not modify the active list.

theorem OperatorDirectory.Properties.Actions.register_same_retired {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.Register tkn, info := i } opDir opDir') : opDir'.retired = opDir.retired

Registering operators do not modify the retired list.

theorem OperatorDirectory.Properties.Actions.register_register {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.Register tkn, info := i } opDir opDir') : (∀ (t : Tokens.Elem.TId), ¬t = tkn → ¬t = Tokens.State.Tokens.last_id opDir'.registered → Tokens.State.Tokens.get t opDir'.registered = Tokens.State.Tokens.get t opDir.registered) ∧ MUList.State.ListST.is_anchor i.validator tkn opDir'.registered = true ∧ Tokens.State.Tokens.last_id opDir'.registered ∉ opDir.registered ∧ MUList.State.ListST.is_member i.validator (Tokens.State.Tokens.last_id opDir'.registered) opDir'.registered = true

Registering operators add an operator to the end of the list, all other registered operators remain the same but the last, now leading to the just added operator.

theorem OperatorDirectory.Properties.Actions.register_prepend {root : Tokens.Elem.TId} {p : MidgardParameters} {info : InputInfo} {opdir opdir' : State.OperatorDirectory} (step : Relation p { act := State.OperActions.Register root, info := info } opdir opdir') : ∃ (time : PosixTime), info.validityInternal.upper = some time ∧ MUList.Relation.Rel opdir.registered (MUList.State.Actions.UnsafePrepend info.validator (time + p.registration_duration) root) opdir'.registered

Registering operators prepend operators into the registered operators list.

Deregister Operators

theorem OperatorDirectory.Properties.Actions.deregister_same_active {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anch : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.Deregister tkn anch, info := i } opDir opDir') : opDir'.active = opDir.active

Deregistering operators do not modify the active list.

theorem OperatorDirectory.Properties.Actions.deregister_same_retired {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anch : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.Deregister tkn anch, info := i } opDir opDir') : opDir'.retired = opDir.retired

Deregistering operators do not modify the retired list.

theorem OperatorDirectory.Properties.Actions.deregister_registered {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anch : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.Deregister tkn anch, info := i } opDir opDir') : (∀ (t : Tokens.Elem.TId), ¬t = tkn → ¬t = anch → Tokens.State.Tokens.get t opDir'.registered = Tokens.State.Tokens.get t opDir.registered) ∧ Tokens.State.Tokens.get tkn opDir'.registered = none ∧ ∃ (a : Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key PosixTime)), Tokens.State.Tokens.get anch opDir'.registered = some a ∧ ∀ (rem_nd : Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key PosixTime)), Tokens.State.Tokens.get tkn opDir.registered = some rem_nd → a.data.link = rem_nd.data.link

Deregistering removes an operator from the registered list, all but the anchor remains the same, the anchor node is updated properly.

Remove Duplicate Propes

theorem OperatorDirectory.Properties.Actions.removeduplicatereg_same_active {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anch : Tokens.Elem.TId} {wit : State.WitnessStatus} (Step : Relation p { act := State.OperActions.RemoveDuplicateSlashBond tkn anch wit, info := i } opDir opDir') : opDir'.active = opDir.active

Removes Duplicate operations do not modify the active list.

theorem OperatorDirectory.Properties.Actions.removeduplicatereg_retired {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anch : Tokens.Elem.TId} {wit : State.WitnessStatus} (Step : Relation p { act := State.OperActions.RemoveDuplicateSlashBond tkn anch wit, info := i } opDir opDir') : opDir'.retired = opDir.retired

Removes Duplicate operations do not modify the retired list.

theorem OperatorDirectory.Properties.Actions.removeduplicatereg_removes_dup_registered {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anch : Tokens.Elem.TId} {wit : State.WitnessStatus} (Step : Relation p { act := State.OperActions.RemoveDuplicateSlashBond tkn anch wit, info := i } opDir opDir') : MUList.Relation.Rel opDir.registered (MUList.State.Actions.Remove tkn anch) opDir'.registered

Removes Duplicate operations remove a regiseterd operator.

Active Remove Bad Operator

theorem OperatorDirectory.Properties.Actions.active_remove_bad_active_keys {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anchor : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.ActRemoveOperatorBad tkn anchor, info := i } opDir opDir') : MOList.Relation.Rel opDir.active (MOList.State.Actions.Remove tkn anchor) opDir'.active

An active operator is removed.

theorem OperatorDirectory.Properties.Actions.active_remove_bad_registered {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anchor : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.ActRemoveOperatorBad tkn anchor, info := i } opDir opDir') : opDir'.registered = opDir.registered

Registered list is not modified.

theorem OperatorDirectory.Properties.Actions.retired_remove_bad_registered {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anchor : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.ActRemoveOperatorBad tkn anchor, info := i } opDir opDir') : opDir'.retired = opDir.retired

Retired list is not modified.

Update Bond

theorem OperatorDirectory.Properties.Actions.update_bond_hold_active_keys {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.UpdateBondHold tkn, info := i } opDir opDir') : (∀ (k : Tokens.Elem.TId), ¬k = tkn → Tokens.State.Tokens.get k opDir.active = Tokens.State.Tokens.get k opDir'.active) ∧ i.validityInternal.upper.isSome = true ∧ (Tokens.State.Tokens.get tkn opDir.active).isSome = true ∧ (Tokens.State.Tokens.get tkn opDir'.active).isSome = true ∧ ∀ (tl tr : Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key (Option PosixTime))), Tokens.State.Tokens.get tkn opDir.active = some tl → Tokens.State.Tokens.get tkn opDir'.active = some tr → MUList.Properties.same_but_data_this tl tr ((fun (x : PosixTime) => p.maturity_duration + x) <$> i.validityInternal.upper)

If we updated the bond of an operator, then transaction infomation i has it's transaction interval upper bound defined and we updated the bond hold variable properly: upper_bond + maturity_duration.

theorem OperatorDirectory.Properties.Actions.update_bond_hold_same_act_members {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.UpdateBondHold tkn, info := i } opDir opDir') (k : Tokens.Elem.TId) (tid : MUList.State.Key) : MUList.State.ListST.is_member tid k opDir.active = MUList.State.ListST.is_member tid k opDir'.active

Update pond does not modify the active members. It does not add nor remove members, just modify the data of one of them.

theorem OperatorDirectory.Properties.Actions.update_bond_hold_same_registered {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.UpdateBondHold tkn, info := i } opDir opDir') : opDir'.registered = opDir.registered

Update pond does not modify the registered operators list.

theorem OperatorDirectory.Properties.Actions.update_bond_hold_same_retired {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.UpdateBondHold tkn, info := i } opDir opDir') : opDir'.retired = opDir.retired

Update pond does not modify the retired operators list.

Recover Bond

theorem OperatorDirectory.Properties.Actions.recover_bond_same_active {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anchor : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.RecoverBond tkn anchor, info := i } opDir opDir') : opDir'.active = opDir.active

Active operators list remains the same.

theorem OperatorDirectory.Properties.Actions.recover_bond_same_registered {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anchor : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.RecoverBond tkn anchor, info := i } opDir opDir') : opDir'.registered = opDir.registered

Registered operators list remains the same.

theorem OperatorDirectory.Properties.Actions.recover_bond_retired {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anchor : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.RecoverBond tkn anchor, info := i } opDir opDir') : MOList.Relation.Rel opDir.retired (MOList.State.Actions.Remove tkn anchor) opDir'.retired

The operator recovering it's bond is removed from the retired operators list.

Remove Bad Retired Operator Props

theorem OperatorDirectory.Properties.Actions.retired_remove_same_active {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anchor : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.RetRemoveOperatorBad tkn anchor, info := i } opDir opDir') : opDir'.active = opDir.active

The active operators list remains the same.

theorem OperatorDirectory.Properties.Actions.retired_remove_same_registered {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anchor : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.RetRemoveOperatorBad tkn anchor, info := i } opDir opDir') : opDir'.registered = opDir.registered

The registered operators list remains the same.

theorem OperatorDirectory.Properties.Actions.retired_remove_retired {opDir opDir' : State.OperatorDirectory} {p : MidgardParameters} {i : InputInfo} {tkn anchor : Tokens.Elem.TId} (Step : Relation p { act := State.OperActions.RetRemoveOperatorBad tkn anchor, info := i } opDir opDir') : MOList.Relation.Rel opDir.retired (MOList.State.Actions.Remove tkn anchor) opDir'.retired

The bad retired operator is removed from the retired operators list.

Registered Operators Queue

Inv Registered Operators time is GT

From the spec document, it seems the Midgard designers assume time increases when operators are registered. This is false, since within a certain range, users can set the transaction validity interval bounds of each transaction.

In particular, this affects the activation criteria. See issue Registered Operators Eligible for Activation Criteria and Scheduler Rewind

The scheduler only checks the time of the oldest operator registered (by it's position in the registered list.), but there may be operators eligible for activation.

Operators can register themselves.

Provided: operator sends bond and sets a valid transaction validity upper bound. Inv: [](Enabled(∀ op, <op>.Register))

This is part of Register and Activer Operators invariant in the spec.

theorem OperatorDirectory.Properties.Registered.AnyoneCanRegister (p : MidgardParameters) (opsDir : State.OperatorDirectory) (root : Tokens.Elem.TId) (HRoot : MUList.State.ListST.is_root_node root opsDir.registered = true) (tx : InputInfo) (uu : PosixTime) (HUpper : tx.validityInternal.upper = some uu) (HSentBond : tx.value = p.required_bond) : ∃ (s : State.OperatorDirectory), StateMachine.next p { act := State.OperActions.Register root, info := tx } opsDir = ComputationResult.Success s ∧ MUList.State.ListST.is_member tx.validator (Tokens.State.Tokens.last_id s.registered) s.registered = true ∧ MUList.State.ListST.is_anchor tx.validator root s.registered = true

Registered node can be activated if its waiting activation time has passed.

Requires: Operator is not already activated nor retired. Inv [](ActivationTimePassed(t) -> Enabled(.Activation t))

theorem OperatorDirectory.Properties.Registered.RegisteredBecomeActive (p : MidgardParameters) (opsDir : State.OperatorDirectory) {opId : OperatorId} {nd anchor : Tokens.Elem.TId} {node anchor_node : MUList.State.ListToken PosixTime} (HNode : Tokens.State.Tokens.get nd opsDir.registered = some node) (HAnch : Tokens.State.Tokens.get anchor opsDir.registered = some anchor_node) (HPth : anchor_node.data.link = some opId) (HNoSelf : ¬nd = anchor) (last_in_reg : MUList.State.midgard_is_member opId node = true) (ret_non : Tokens.Elem.TId) (HNoRet : MOList.Operations.is_non_member (some opId) ret_non opsDir.retired = true) (act_non : Tokens.Elem.TId) (HNoAct : MOList.Operations.is_non_member (some opId) act_non opsDir.active = true) (tx : InputInfo) (ll : PosixTime) (HSome : tx.validityInternal.lower = some ll) (HAfter : node.data.data ≤ ll) : ∃ (s : State.OperatorDirectory), StateMachine.next p { act := State.OperActions.Activate nd anchor ret_non act_non, info := tx } opsDir = ComputationResult.Success s ∧ MUList.State.ListST.is_member opId (Tokens.State.Tokens.last_id s.active) s.active = true

theorem OperatorDirectory.Properties.Registered.RegisterDeregister (p : MidgardParameters) (opsDir : State.OperatorDirectory) (tx : InputInfo) {rem anchor : Tokens.Elem.TId} (HNeq : ¬rem = anchor) (RemIn : MUList.State.ListST.is_member tx.validator rem opsDir.registered = true) (Anchor : MUList.State.ListST.is_anchor tx.validator anchor opsDir.registered = true) : ∃ (s : State.OperatorDirectory), StateMachine.next p { act := State.OperActions.Deregister rem anchor, info := tx } opsDir = ComputationResult.Success s

Registered operators can de-registerd whenever they want.

Inv: []( p ∈ Registered -> Enabled(Deregister(p)))

Activated operators list is decr-sorted.

theorem OperatorDirectory.Properties.ActiveOpDir.ActiveNodesRetire {p : MidgardParameters} {o : State.OperatorDirectory} {act anc ret : Tokens.Elem.TId} {act_tkn anc_tkn : Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key (Option PosixTime))} {key : MUList.State.Key} (Reachable : Computational.Relation.StepMachine.FromInit p o) (isActive : Tokens.State.Tokens.get act o.active = some act_tkn) (act_key : act_tkn.data.key = some key) (isAnchor : Tokens.State.Tokens.get anc o.active = some anc_tkn) (anchor : anc_tkn.data.link = some key) (is_not_retired : MOList.Operations.is_non_member (some key) ret o.retired = true) (tx : InputInfo) : ∃ (o' : State.OperatorDirectory), StateMachine.next p { act := State.OperActions.Retire act anc ret, info := tx } o = ComputationResult.Success o'

Active operators can retire whenever they want.

[](p ∈ active ∧ p ∉ retired -> Enabled(Retire(p)))

We proved that if we are in a reachable state Active and Retired lists are disjoint lists.

We detected that there are no restrictions when it comes to retire operators. See issue Anyone can retire active operators.

def OperatorDirectory.Properties.NoRetiredAndActive (o : State.OperatorDirectory) : Prop

Active and Retired ops lists are disjoint.

Equations

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

theorem OperatorDirectory.Properties.NonRetiredActive {p : MidgardParameters} {i : InfoActions State.OperActions} {s s' : State.OperatorDirectory} (reach_state : Computational.Relation.StepMachine.FromInit p s) (pre : NoRetiredAndActive s) (step : Relation p i s s') : NoRetiredAndActive s'

There are not active and retired nodes