formal-ledger-specifications icon indicating copy to clipboard operation
formal-ledger-specifications copied to clipboard

Published 20 hours ago • verified publisher icon IntersectMBO

Property: `allEnactable` is an invariant of `CHAIN`

Open WhatisRT opened this issue 9 months ago • 0 comments

This is a little difficult, since allEnactable depends on the list of governance actions twice: once for the enactability criterion and then all elements in the list need to satisfy it. This means that this cannot be proven by a simple induction.

There are two sub-lemmas here:

  • allEnactable is an invariant of GOV
  • allEnactable is an invariant of EPOCH (this currently isn't true, need to filter things properly in EPOCH)

WhatisRT avatar May 06 '24 14:05 WhatisRT