formal-ledger-specifications
formal-ledger-specifications copied to clipboard
IntersectMBO
Formal specifications of the cardano ledger
We do have a `Language` type, but it's abstract and don't have access to inhabitants like `PlutusV1`. There are at least two options to resolve this: - Change `Language` to...
For all proposal deposits `d` currently in a block, there exists an epoch `e` where if it contains a block, the deposit for `d` is not in the deposit pot...
There are at least these interesting properties: - At the epoch boundary, `dom DState.rewards` is constant - `dom DState.rewards = DepositPurpose.CredentialDeposit^{-1} (dom UTxOState.deposits)` is an invariant The first property is...
This is the companion to https://github.com/input-output-hk/cardano-ledger/issues/3149. - [ ] #413 - [ ] #414 - [ ] #415 - [ ] #412 - [ ] #417
document the details regarding the support of ref scripts for plutus v1 in the ledger specification
Please document if any changes coming to Conway era regarding fee calculation w.r.t ref scripts
Please document the changes coming regarding the pointer addresses in Conway era. Missing in the ledger specification
This should be a property of `CHAIN`. There are multiple options to state this: - If `EnactState` changes, we run `EPOCH` - If `EnactState` changes, there is a governance action...
For a stake credential `a` and a transaction that spends an input with stake credential `a` to propose something and returning the remainder back to addresses with stake credential `a`,...
This is related to #359. In fact, this is just the first few steps of `gmsc` in `Ledger.Utxo.Properties` factored out into a new lemma.