[#870] Add pStateIsInternallyConsistent property
Relates to #870.
Home /
Input Output /
cardano-ledger-specs
41 commits this week
Oct 14, 2019 -
Oct 21, 2019
[#950] Add pStateIsInternallyConsistent property
Also creates a new test group for POOL and relocates the RegPool property to it.
Closes #950.
Merge pull request #948 from input-output-hk/mhuesch/870
[#870] Generate RegPool DCerts
[#870] Address second round of PR feedback
added images
Signed-off-by: Kevin Hammond [email protected]
Check property: utxo and transaction outputs (txouts) must be disjoint.
updated version
Signed-off-by: Kevin Hammond [email protected]
[#870] Address PR feedback: factor out to Rules.TestPool
I follow the example of Test.TestDeleg and define a transformation between
SourceSignalTarget LEDGER -> SourceSignalTarget POOL.
Then I relocate the registeredPoolIsAdded property to TestPool.
I also move the transformation function for DELEG into TestDeleg, for
consistency.
Move nonce calculation to UPDN in exec spec
Move nonce calculation to UPDN in exec spec
[#870] Address PR feedback
Add additional KeyPairs, since
RegPoolrequires more of them, and thus its generator frequency drops when we exhaust the key space.- In concert with this, increase the coverage check for RegPool from 1/60 to 1/20.
- Use applicative style in
genStakePoolto reduce generator dependencies & get better shrinking.
[#870] Address bug from #867
Lower bound was set too low.
A failed attempt to build the PDF’s of isabelle proofs on CI.
Problems:
- HOT is only successfully built if isabelle is run from the GUI (
isabelle jedit). - Even after building I get an
unknown Z3 proof rule "proof-bind"error.
[skip ci]
check against design document. added additional material
Signed-off-by: Kevin Hammond [email protected]
Merge pull request #936 from input-output-hk/jdiaz/utxo-diff-proof
Add proof of UTxO difference property
First version of a derivation that contains Isabelle in its environment. [skip ci]
First version of a derivation that contains Isabelle in its environment. [skip ci]
fixup! Migrate operational certificate issue numbersThese are now purely a protocol concern, and are not updated in the legdger rules.
Migrate operational certificate issue numbersThese are now purely a protocol concern, and are not updated in the legdger rules.
Migrate operational certificate issue numbers
These are now purely a protocol concern, and are not updated in the legdger rules.
Migrate operational certificate issue numbersThese are now purely a protocol concern, and are not updated in the legdger rules.
Address the issue of the first slot in an epoch not being filled.
This sadly makes the change less nice, but is needed.
Merge pull request #945 from input-output-hk/uroboros/867/generate_pparams
[867] Generate PParams
added mainnet calcs
Signed-off-by: Kevin Hammond [email protected]
Move nonce related calculations into protocol rules
This addesses one part of #946
All nonce updates are now managed in UPDN, which has an additional case when the slot is the first slot of the epoch, updating the epoch nonce. All mention of nonces is now removed from the ledger part of the rules.
I think this is actually a nicer formulation after all anyway.
Move nonce related calculations into protocol rules
This addesses one part of #946
All nonce updates are now managed in UPDN, which has an additional case when the slot is the first slot of the epoch, updating the epoch nonce. All mention of nonces is now removed from the ledger part of the rules.
I think this is actually a nicer formulation after all anyway.
Move nonce related calculations into protocol rules
This addesses one part of #946
All nonce updates are now managed in UPDN, which has an additional case when the slot is the first slot of the epoch, updating the epoch nonce. All mention of nonces is now removed from the ledger part of the rules.
I think this is actually a nicer formulation after all anyway.
back to correct version
Signed-off-by: Kevin Hammond [email protected]
[867] Generate PParams - explicit generation of some bounds, special range for d param
added .gitattributes again
Signed-off-by: Kevin Hammond [email protected]
add gitattributes
Signed-off-by: Kevin Hammond [email protected]
using LSF
Signed-off-by: Kevin Hammond [email protected]
Merge pull request #937 from input-output-hk/topic/deps-20190114
Update dependencies
bump iohk-nix without bad haskell.nix bump