Andre Knispel
Andre Knispel
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
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.
`EPOCH` is very complicated, especially considering that we use a lot of `open` and record stuff. Some of the logic that is responsible for splitting up rewards into what we...
I like this notation, but the issue is that it can be accidentally mixed up with the regular function arrow. It would have been nice to force parentheses around the...
This issue contains various items that don't really fit anywhere else. I've divided this into smaller and bigger tasks. None of this is really urgent ATM, so we can do...