Library Oracle

• Introduction
• Imports
• Datatypes, Parameters (Section 3)
  • Numbers
  • Users
  • Time
  • Weights, Balances and Values
  • Maps
  • Parameters (Eq. 1)
  • State (Eq. 2)
    • Governance State
    • Oracle State
    • State
• Auxiliary Definitions (3.1)
  • Exponential Decay Factor (Def. 1)
  • Exponential decay factor lemmas
  • Time-dependent functions (Def. 2)
• Auxiliary state update operations (3.2)
• Operations (3.3)
  • Token Deposit (3.3.1)
  • Token Withdrawal (3.3.2)
  • Value Submission (3.3.3)
    • Predefinition local variables
    • Updated aggregate weight and value, and reward payout (Eq. 10-12)
  • Value reading (3.3.4)
  • Vote to blacklist (3.3.5)
  • Vote to whitelist (3.3.6)
  • Weight synchronization (3.3.7)
  • Reward Token Funding (3.3.8)
• Traces
  • Initial state
  • Execution of an operation/trace
  • Run (infinite traces)
  • Internal lemmas about reals and summations
• Theorems about the oracle protocol (Section 4)
  • Theorem 1: Equivalence of the ideal decayed weight mean function and the constant time update rule
    • Proof sketch
    • Operations preserve relevant fields
    • Submission subcase
    • Invariants and theorem statement
    • mean_raw_eq_preserved_step and subcases
    • Raw invariant along runs
    • Theorem 1 main statement
  • Theorem 2: Inactive oracle operator delay
    • Proof sketch
    • Delay definition (Defs. 4, 5)
    • Inactivity definition
    • Convergence / limit to zero formalization definition
    • Exponential dominates linear
    • Rewriting to form in line 38 in paper
    • Theorem 2 main statement
  • Theorem 3: Optimally small oracle delay
    • Proof sketch
    • Theorem 3 main statement
  • Theorem 4: Sustainable rewards
    • Proof sketch
    • Theorem 4 main statement