formal-ledger-specifications
formal-ledger-specifications copied to clipboard
IntersectMBO
Formal specifications of the cardano ledger
# Description When finished, this PR will address issue #7 by providing a Python script `agda2vec.py` which will become part of the make command for docs in `Makefile` so that,...
This might be difficult because we may have to actually interface with Plutus.
# Description Since the same code sometimes works on my machine and sometimes doesn't, I'm using CI as a reproducible machine. To reproduce locally, use `nix-shell --command 'make ledger.docs'`. The...
Vertical vectors make the PDF way more readable. The issue here is that the LaTeX environment for rendering Agda isn't compatible with that, at least what I tried didn't work....
During bootstrap, DReps don't vote & the CC has some special emergency powers. Bootstrap will end when the term of the bootstrap CC runs out.
There are many properties that are currently part of the rules, which don't really fit into any particular rule thematically, and don't depend on anything but the signal. We could...
This is a bit non-trivial because of level issues. `Functor` is by definition level-polymorphic, but the current set-theory isn't quite level-polymorphic enough to support this yet. So we can either...
For convenience or other reasons, some properties/predicates produce booleans. Our properties should always go to `Set`, so we can use them without writing something like `≡ true`. Here are some...
These are Alonzo-era things which are currently undocumented here, but are documented in the Alonzo spec. These need to be documented when we want to produce a spec that includes...
We should prove that the following property is an invariant, i.e. that if it holds for some state it also holds when we successfully apply a block to that state....