Registered Operator Queue No duplication and No Intersection with Retired and Active.

Properties listed here are optimistic: operators can brake the invariant, but they must pay the price for it.

The methodology we use to prove these properties is:

• Agents can detect when the system reaches an undesired (but valid) state
• Agents can submit a valid witness
• The system accepts the witness and (partially) corrects the state

The system may not be fully but partially correct, i.e. there may be several ways to correct the system and there may be several duplicated nodes.

However, we would like to prove the following properties:

• If there are no detectable witnesses, then the system is completely correct.
• After submitting a witness w and the systems is (partially) corrected, then the witness w is not a witness of the new system.
• It is always possible for agents to detect when the system state is not valid.
• It is always possible for agents to submit witnesses.

The last two properties are assumptions here, but should be checked somewhere else.

Optimistic Properties.

Since we cannot directly prove liveness properties as agents actually submitting proofs, we just prove that the such actions are always enabled. For example, the action of submitting a valid witness is always enabled.

def List.filter_cons_p {α : Type} {l rs : List α} {p : α → Bool} {r : α} (h : filter p l = r :: rs) : p r = true ∧ r ∈ l

Equations

• ⋯ = ⋯

A Witness presents a registered node whose key (opId) also appears in one of the other lists:

• opId appears twice in Registered Queue.
• opId appears in Registered and Active Queue.
• opId appears in Registered and Retired Queue.

structure OpsDir.OptimisticWitness.Witness : Type

• registered_id : OperatorId
• registered_nd : Tokens.Elem.TId
• anchor : Tokens.Elem.TId
• duplicated : OperatorDirectory.State.WitnessStatus

Valid witnesses:

• Duplicated registered elements are actually different tokens. In the case we have duplicated registered nodes. When we have a registered and retired or active, it is not necesary since they belong to different lists.

def OpsDir.OptimisticWitness.valid_witness_dup (w : Witness) : Bool

Equations

• OpsDir.OptimisticWitness.valid_witness_dup w = match w.duplicated with | OperatorDirectory.State.WitnessStatus.Registered dup_tid => w.registered_nd != dup_tid | x => true

• And anchor is valid anchor (tokens cannot be anchor of themselves.) We cannot remove nodes that are anchor of themselves.

def OpsDir.OptimisticWitness.valid_witness_anch (w : Witness) : Bool

Equations

• OpsDir.OptimisticWitness.valid_witness_anch w = (w.registered_nd != w.anchor)

Fraud Detection function

The goal of this section is to define a procedure such that it returns:

• .none if no fraud was detected, or
• some Witness in the case of founding duplicates or intersection between the lists.

This procedure defines what we mentioned earlier as the possibility to detect fraud.

Duplication Detection.

structure OpsDir.OptimisticDetection.DupRegWitness : Type

Duplicated register operator witness. A valid duplicate it is different from the previous one.

• opId : OperatorId
• reg1 : Tokens.Elem.TId
• reg2 : Tokens.Elem.TId

def OpsDir.OptimisticDetection.find_duplicate_register {α : Type} (reg : MUList.State.ListST α) : Option DupRegWitness

Definition of finding duplicates by finding the first duplicated key in the registered operator directory starting from the beginning. Returns two Token ids and the key they both share.

Equations

• One or more equations did not get rendered due to their size.
• OpsDir.OptimisticDetection.find_duplicate_register [] = none
• OpsDir.OptimisticDetection.find_duplicate_register (none :: rest) = OpsDir.OptimisticDetection.find_duplicate_register rest

axiom OpsDir.OptimisticDetection.find_duplicate_mem_neq {reg : MUList.State.ListST PosixTime} {wit : DupRegWitness} (reachSt : MUList.Computational.ReachableUList reg) (H : find_duplicate_register reg = some wit) : MUList.State.ListST.get_key wit.reg1 reg = some wit.opId ∧ MUList.State.ListST.get_key wit.reg2 reg = some wit.opId ∧ ¬wit.reg1 = wit.reg2

The definition of find_duplicate_register as a property. This is valid for well-built lists, i.e. lists holding the reachable predicate RechableUList.

axiom OpsDir.OptimisticDetection.find_duplicate_none {α : Type} {reg : MUList.State.ListST α} (H : find_duplicate_register reg = none) (t1 t2 : Tokens.Elem.TId) : ¬t1 = t2 → t1 ∈ reg → t2 ∈ reg → ¬MUList.State.ListST.get_key t1 reg = MUList.State.ListST.get_key t2 reg

If we do not find anything, then all tokens have different key.

def OpsDir.OptimisticDetection.DiffId {α : Type} (l r : Option (Tokens.Elem.TokenD α)) : Prop

Equations

• OpsDir.OptimisticDetection.DiffId (some l') (some r') = ¬l'.id = r'.id
• OpsDir.OptimisticDetection.DiffId l r = True

Intersection Detection.

We use this to detect when a registered node is also in either of the other two lists.

def OpsDir.OptimisticDetection.find_witness_cross {α β : Type} (dup : MUList.State.ListST α) (removable : MUList.State.ListST β) : Option ((OperatorId × Tokens.Elem.TId) × Tokens.Elem.TId)

The following procedure finds if there is a token in the two list with the same key. We use it to find elements belonging to the intersection of to Midgard Lists.

Equations

• One or more equations did not get rendered due to their size.
• OpsDir.OptimisticDetection.find_witness_cross dup [] = none
• OpsDir.OptimisticDetection.find_witness_cross dup (none :: rest) = OpsDir.OptimisticDetection.find_witness_cross dup rest

axiom OpsDir.OptimisticDetection.some_find_witness {α β : Type} {opId : OperatorId} {tknId dupId : Tokens.Elem.TId} {dup : MUList.State.ListST α} {rem : MUList.State.ListST β} (H : find_witness_cross dup rem = some ((opId, tknId), dupId)) : MUList.State.ListST.is_member opId tknId rem = true ∧ MUList.State.ListST.is_member opId dupId dup = true

Correctness of find_witness_cross . The finding is composed of to two tokens each one showing membership of the same operator's id opId on both lists.

axiom OpsDir.OptimisticDetection.none_find_witness_dup {α β : Type} {dup : MUList.State.ListST α} {rem : MUList.State.ListST β} (H : find_witness_cross dup rem = none) : (MUList.InternalUtils.all_alive_tids dup fun (x : Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key α) × ℕ) => match x with | (tkn, snd) => match tkn.data.key with | none => true | some key => (MUList.InternalUtils.find_key rem key).isNone) = true

If we cannot find a witness, the two lists do not share any key. We write it as: all keys alive in dup, do not have a token in rem

axiom OpsDir.OptimisticDetection.none_find_witness_rem {α β : Type} {dup : MUList.State.ListST α} {rem : MUList.State.ListST β} (H : find_witness_cross dup rem = none) : (MUList.InternalUtils.all_alive_tids rem fun (x : Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key β) × ℕ) => match x with | (tkn, snd) => match tkn.data.key with | none => true | some key => (MUList.InternalUtils.find_key dup key).isNone) = true

If we cannot find a witness, the two lists do not share any key. This is the symmetric of the above.

Computation of the Optimistic Properties

We check the try in one go. We could also have split it into different procedures.

inductive OpsDir.OptimisticDetection.Error : Type

• NoAnchorReg : Error
• NoAnchorActive : Error
• NoAnchorRetired : Error
• SelfAnchor : Error

def OpsDir.OptimisticDetection.find_witness (ops : OperatorDirectory.State.OperatorDirectory) : Error ⊕ Option OptimisticWitness.Witness

The following procedure, find_witness, does the following.

1. Check for duplicated Keys in Registered Ops Dir. 1a. If True, .DupReg ...
2. If False, Checks Act ∩ Regs 2a. If True, .InterAct ...
3. If False, checks Ret ∩ Regs 3a. If True, .InterRet ...
4. If False -> .none

Equations

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

theorem OpsDir.OptimisticDetection.find_witness_valid {p : MidgardParameters} {ops : OperatorDirectory.State.OperatorDirectory} (Reachable : OperatorDirectory.Computational.Relation.StepMachine.FromInit p ops) {wit : OptimisticWitness.Witness} (HWit : find_witness ops = Sum.inr (some wit)) : OptimisticWitness.valid_witness_dup wit = true

The result of finding a witness is a valid witness.

theorem OpsDir.OptimisticDetection.find_witness_valid_anchor {p : MidgardParameters} {ops : OperatorDirectory.State.OperatorDirectory} {wit : OptimisticWitness.Witness} (Reachable : OperatorDirectory.Computational.Relation.StepMachine.FromInit p ops) (HWit : find_witness ops = Sum.inr (some wit)) : OptimisticWitness.valid_witness_anch wit = true

The witness we found has a valid anchor and thus we can eventually remove the fraudulent operator.

theorem OpsDir.OptimisticDetection.find_witness_key {ops : OperatorDirectory.State.OperatorDirectory} {p : MidgardParameters} {wit : OptimisticWitness.Witness} (Reachable : OperatorDirectory.Computational.Relation.StepMachine.FromInit p ops) (HWit : find_witness ops = Sum.inr (some wit)) : some wit.registered_id = MUList.State.ListST.get_key wit.registered_nd ops.registered

The witness we found shows membership of the duplicated key.

theorem OpsDir.OptimisticDetection.find_witness_registered (ops : OperatorDirectory.State.OperatorDirectory) {wit : OptimisticWitness.Witness} {p : MidgardParameters} (Reachable : OperatorDirectory.Computational.Relation.StepMachine.FromInit p ops) (HWit : find_witness ops = Sum.inr (some wit)) : MUList.State.ListST.is_member wit.registered_id wit.registered_nd ops.registered = true ∧ MUList.State.ListST.is_anchor wit.registered_id wit.anchor ops.registered = true

The witness is a valid token in the registered operator directory and has a valid anchor.

theorem OpsDir.OptimisticDetection.find_witness_dup_reg (ops : OperatorDirectory.State.OperatorDirectory) {wit : OptimisticWitness.Witness} {dup_id : Tokens.Elem.TId} {p : MidgardParameters} (Reachable : OperatorDirectory.Computational.Relation.StepMachine.FromInit p ops) (HWit : find_witness ops = Sum.inr (some wit)) (HReg : wit.duplicated = OperatorDirectory.State.WitnessStatus.Registered dup_id) : MUList.State.ListST.is_member wit.registered_id dup_id ops.registered = true

If we found a duplicated in the registered op list, then the duplicate also belongs to the registered list.

theorem OpsDir.OptimisticDetection.find_witness_dup_act (ops : OperatorDirectory.State.OperatorDirectory) {wit : OptimisticWitness.Witness} {act_tkn : Tokens.Elem.TId} (HWit : find_witness ops = Sum.inr (some wit)) (HReg : wit.duplicated = OperatorDirectory.State.WitnessStatus.Active act_tkn) : MUList.State.ListST.is_member wit.registered_id act_tkn ops.active = true

If we found a witness pointing to an active operator, the the operator is a member of the active list.

theorem OpsDir.OptimisticDetection.find_witness_dup_ret (ops : OperatorDirectory.State.OperatorDirectory) {wit : OptimisticWitness.Witness} {ret_tkn : Tokens.Elem.TId} (HWit : find_witness ops = Sum.inr (some wit)) (HReg : wit.duplicated = OperatorDirectory.State.WitnessStatus.Retired ret_tkn) : MUList.State.ListST.is_member wit.registered_id ret_tkn ops.retired = true

If we found a retired witness, then we can also show membership in the retired list.

theorem OpsDir.OptimisticDetection.not_finding_witness (ops : OperatorDirectory.State.OperatorDirectory) (HNoWit : find_witness ops = Sum.inr none) : (∀ (t1 t2 : Tokens.Elem.TId), ¬t1 = t2 → t1 ∈ ops.registered → t2 ∈ ops.registered → ¬MUList.State.ListST.get_key t1 ops.registered = MUList.State.ListST.get_key t2 ops.registered) ∧ (MUList.InternalUtils.all_alive_tids ops.active fun (x : Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key (Option PosixTime)) × ℕ) => match x with | (t, snd) => match t.data.key with | none => true | some k => (MUList.InternalUtils.find_key ops.registered k).isNone) = true ∧ (MUList.InternalUtils.all_alive_tids ops.retired fun (x : Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key (Option PosixTime)) × ℕ) => match x with | (t, snd) => match t.data.key with | none => true | some k => (MUList.InternalUtils.find_key ops.registered k).isNone) = true

However, if we do not find any witness, then there are no duplicated keys in the registered list, nor there is any intersection between the registered and active; and the retired and active lists.

Generate FraudProof from detected fraud.

Once we detected fraud, we found a witness, we generate the corresponding action.

def OpsDir.OptimisticProof.GenerateFraudProof (w : OptimisticWitness.Witness) : OperatorDirectory.State.OperActions

Equations

• OpsDir.OptimisticProof.GenerateFraudProof w = OperatorDirectory.State.OperActions.RemoveDuplicateSlashBond w.registered_nd w.anchor w.duplicated

Agents are enabled to submit fraudproof.

theorem OpsDir.OptimisticProof.EnabledFPSubmission {p : MidgardParameters} {obs : OperatorDirectory.State.OperatorDirectory} {wit : OptimisticWitness.Witness} (Reachable : OperatorDirectory.Computational.Relation.StepMachine.FromInit p obs) (info : InputInfo) (slashedBond : p.required_bond * ↑p.slashing_penality ≤ info.fee * 100) (FState : OptimisticDetection.find_witness obs = Sum.inr (some wit)) : ∃ (s' : OperatorDirectory.State.OperatorDirectory), OperatorDirectory.Relation p { act := GenerateFraudProof wit, info := info } obs s'

Fixed After FP.

We cannot say that we reached a valid state after submitting a FP. But we should be able to prove that we cannot generate the same FP (or witness.) In other words, the state is invalid in a different way.

theorem OpsDir.OptimisticProof.AfterFP {p : MidgardParameters} {info : InputInfo} {wit wit' : OptimisticWitness.Witness} {obs obs' : OperatorDirectory.State.OperatorDirectory} (reachable : OperatorDirectory.Computational.Relation.StepMachine.FromInit p obs) (Step : OperatorDirectory.Relation p { act := GenerateFraudProof wit, info := info } obs obs') (next : OptimisticDetection.find_witness obs' = Sum.inr (some wit')) : ¬wit'.registered_nd = wit.registered_nd

If condition is not met, then it is not possible to submit a FP.

theorem OpsDir.OptimisticProof.DisableFPSubmittion {p : MidgardParameters} {info : InputInfo} {tknId anchId : Tokens.Elem.TId} {w : OperatorDirectory.State.WitnessStatus} {s obs : OperatorDirectory.State.OperatorDirectory} (CState : OptimisticDetection.find_witness obs = Sum.inr none) : ¬OperatorDirectory.Relation p { act := OperatorDirectory.State.OperActions.RemoveDuplicateSlashBond tknId anchId w, info := info } obs s

[Alternative] Monitors.

The above approach computes the possiblity of detecting witnesses at any state. However, we can write a monitor detecting when new operators register, activate or retired.

In other words, we can write a monitor checking keeping track of the evolutino of the system, analyzing actions as they come, detecting duplicates, generating witnesses and submitting them to Midgard.

We leave this approach for future implementations, although all components required to define such monitors should be here.