intersectmbo / cardano-ledger Goto Github PK

There is a makefile inside fm-ledger-rules/latex which builds a pdf using Nix. It would be nice to check this build as a part of CI. It would also be great if there was a way to publish the pdf as an artifact.

Add certificate deposits and refunds to the Haskell executable model. This requires adding the protocol constants to the ledger state as well. It may make sense to not model refunding pool certificates until some kind of epoch boundary rules are in place.

Currently, the spec refunds both stake key registration and pool registration deposits at any slot in the UTxO rule. The pool registration, however, should not be done this way since we allow retirement certificates to override each other. These refunds can only be returned when the pool is reaped.

The section "Display of Stake Pools in the Wallet" (currently 5.2) was written before the incentives part of the document was finished. We should review this section, to make sure everything covered therein is covered in the section on incentives, and then just reference that section instead of duplicating information.

After finishing this issue it

• MUST be possible to mutate Signatures
• MUST be possible to mutate hashes

To ensure replay protection, each transaction must consume at least one input. This is in particular important for delegation transactions, but currently not implemented in the executable spec.

After resolving this issue it

• MUST be ensured that a validated transaction consumes at least one input
• MUST be ensured that 'DelegationData' transactions spend at least one input
• SHOULD be one combined LedgerEntry data type
• there SHOULD be at least one test for checking that a transaction with empty input set is not validated

Try combining our latex spec and haskell model with literate haskell. Decide if this is the approach that we should take. See this report for an example of multiple .lhs modules.

Write a property test that checks that for any valid ledger state:

45B ADA == balance utxo + balance rewards + deposits + treasury + reserves + rewardPool + fees

The executable model currently uses implicit fees. Make them explicit and validate a minimum fee.

We should change this section, to state that the refundable part of the fee is tracked separately from the rewards pool.

Implement the mechanism for reward account withdrawals in the Haskell executable model.

In the latex spec, we need to model transaction fees.

We can then state the preservation of value property as an equality instead of an inequality. For example, with implicit fees, we state this validation rule as balance (txouts tx) \leq balance (txins tx domRestr utxo). When fees and minted coins are explicit, we get an equality: fees + balance (txouts tx) = minted + balance (txins tx domRestr utxo).

We will be writing property tests for our executable haskell model of the ledger with delegation. The first step is to think of all the properties that we can test. Add these to the LaTeX (or lhs) document.

The LaTeX delegation spec has very minimal explanations right now, it is mostly tables and rules. Fill out this document with more explanations and context.

there needs to be a main/top-level ledger rule which combines the delegation with witnesses rule with the UTxO with witnesses rule.

In addition to test basic functionality of transaction validation, the hspec
tests should also cover stake delegation functionality.

Accounting model in progress, more discussion to come with model updates

we need to write rules that ensure that the total amount of ada is preserved when deposits values are changed by voting.

Combine the cardano-chain ledger rules with the delegation rules in this repo. We can probably use iohk.sty and ledger-spec.tex without modification. We can consider making a git submodule or nix package.

This property uses rewards and deposits and therefore can only be modelled / tested once this is included in the executable spec.

In the LaTeX spec, instead of keeping the minfee calculation abstract, define it as ax+b, where a and b are in the protocol constants and x is the number of bytes in an encoding of the transaction.

After finishing this issue it

• MUST be possible to instantiate the Goblins framework with the mutators as toys

• MUST be possible to instantiate the ledger value transactions using the STS framework

• SHOULD be possible to run the Goblins to create invalid data using the GA approach

• SHOULD be possible to see labeled test results from the GA run

part of #20

Write the generators for property testing the Haskell model. We may want to break this ticket into several tickets.

and write the tests in such a way that they can be individually loaded into ghci

In the latex spec, we need to model the deposit mechanisms as described in the delegation design document.

The current rule DELEGW has two rules in its antecedent. It is intended that this rule succeeds if either DELEG or POOL succeeds. As all the conditions in the antecedent are conjoined, however, as currently written, this rule can never succeed.

We need to either split this rule into multiple rules, or find a way to express the disjunction.

After finishing this issue it

• MUST be possible to generate delegation transactions from a valid ledger state
• MUST be possible to mutate valid delegation transactions

add stale stake mechanism, as described in the delegation design doc, to the ledger rules.

Liquid Haskell provides means for automatic checking of certain properties

• refinement types
• theorem proving for equational reasoning
• termination checks (automatic for subset, manual in more complex cases)

There may be some properties that could be proven directly in Haskell using Liquid Haskell. Nevertheless, there are challenges, for example:

• expressiveness
• integration into Project, CI ...
• Results depend on choice of SMT solver (Z3, CVC4, MathSAT)

after completing this issue:

• a property MUST exist in the latex spec which formalizes that double-spend is not possible using the defined transition rules
• this property MUST be implemented as a hedgehog property in the executable spec and validate the property for valid generated transactions

part of #20

Turn the properties from #18 and the generators from #19 into property tests.

In the Haskell executable model, add tracking to the ledger state for: treasury, reward pool, fee pool, reserves. This will involve adding some epoch boundary transitions.

In the latex spec, we need to model pointer addresses.

Implement the epoch boundary mechanism for paying out rewards in the Haskell executable model.

in particular http://hackage.haskell.org/package/tasty-hedgehog-coverage-0.1.0.0/docs/Test-Tasty-Hedgehog-Coverage.html

The current generators can supply valid data to the state transition function. It should also be possible to generate invalid data, to test the correct behaviour of the state transition functions in those case.

This should then collect all reasons of why a transaction is rejected.
It is necessary to choose an efficient approach to generate invalid data, likely doesn't generate "interesting" cases that test the important edge cases.

Non UTxO actions that a transaction may take do not always afford the same replay protection as the UTxO. so, for this reason, we can piggyback replay prevention by signing the transaction body, assuming the transaction spends at least one input. We should make this a conditional requirement in the appropriate rules.

In the latex spec, we need to model the rewards mechanism from the leader election.

LaTeX and executable specification of new ledger rules including delegation.