Implement liveness property in dynamic logic #498

ghost · 2022-09-19T16:12:32Z

This PR does a couple things to "solve" the issue:

Update the q-d library to a newer version
Adapt the Model to the new version which decouples the model from the perform and thus alleviates the need for complex constraints in the ModelState instance for Hydra
Express the conflict-free liveness property from the paper using Dynamic Logic formalism, hopefully leading to more understandable properties
Introduce a couple more actions needed to express that property
Make the property pass (this required a couple fixes in the Model as the assumptions for some functions have changed)

Before investing a lot more time into this, I think it would be worthwhile to "stop & think" from this simple example.

github-actions · 2022-09-19T17:17:35Z

Transactions Costs

Sizes and execution budgets for Hydra protocol transactions. Note that unlisted parameters are currently using arbitrary values and results are not fully deterministic and comparable to previous runs.

Metadata
Generated at	2022-09-28 16:57:51.276793216 UTC
Max. memory units	14000000
Max. CPU units	10000000000
Max. tx size (kB)	16384

Cost of Init Transaction

Parties	Tx size	% max Mem	% max CPU	Min fee ₳
1	4833	9.69	3.83	0.47
2	5041	13.44	5.32	0.52
3	5243	13.30	5.21	0.53
5	5653	19.12	7.50	0.61
10	6677	30.19	11.80	0.77
46	14060	99.77	38.56	1.85

Cost of Commit Transaction

Currently only one UTxO per commit allowed (this is about to change soon)

UTxO	Tx size	% max Mem	% max CPU	Min fee ₳
1	5771	19.85	8.02	0.62

Cost of CollectCom Transaction

Parties	Tx size	% max Mem	% max CPU	Min fee ₳
1	13058	20.68	8.29	0.95
2	13380	36.46	14.76	1.14
3	13772	56.24	22.95	1.38
4	14164	78.97	32.40	1.65

Cost of Close Transaction

Parties	Tx size	% max Mem	% max CPU	Min fee ₳
1	9327	8.19	3.36	0.65
2	9528	9.55	4.04	0.68
3	9657	9.75	4.27	0.68
5	10051	12.19	5.51	0.73
10	10224	12.93	5.00	0.74
30	14212	32.26	17.02	1.16
60	15213	36.71	13.91	1.22

Cost of Contest Transaction

Parties	Tx size	% max Mem	% max CPU	Min fee ₳
1	9331	8.16	3.34	0.65
2	9528	9.38	3.96	0.67
3	9691	10.16	4.42	0.69
5	10024	11.72	5.32	0.72
10	10886	16.20	7.80	0.82
30	14218	32.23	17.00	1.16
43	16367	42.55	22.94	1.38

Cost of Abort Transaction

Some variation because of random mixture of still initial and already committed outputs.

Parties	Tx size	% max Mem	% max CPU	Min fee ₳
1	13499	22.50	9.35	0.99
2	13817	38.24	16.27	1.18
3	13928	52.72	22.50	1.35
4	13824	63.38	26.98	1.47
5	14434	97.45	42.55	1.88

Cost of FanOut Transaction

Involves spending head output and burning head tokens. Uses ada-only UTxO for better comparability.

UTxO	Tx size	% max Mem	% max CPU	Min fee ₳
1	13484	10.26	4.46	0.86
2	13585	12.16	5.49	0.89
3	13487	12.92	6.07	0.89
5	13629	16.34	7.98	0.94
10	13807	24.25	12.50	1.04
50	15248	85.18	47.72	1.85
59	15570	98.90	55.65	2.04

Also update iohkNix to not get a deprecation warning from the crypto overlay.

…dency Getting the package from hackage is not a problem, but our upstream dependencies are not fit for latest hackage versions and we did not want to bother chasing constraints at this point.

This is due to the new 1.0.0 interface of quickcheck-dynamic

This kind of duplicates ClientInput

Unfortunately, this was requiring to ditch record syntax as GADTs seem not to allow duplicate record fields with differing return types.

…ion tests

This keeps the conversion back to simple utxos out of the model.

Instead of requiring a Show instance on monitoring function we can pattern match as suggested by Max.

This gives us a Show instance for monitoring failures

…ition in the model

This requires introduction of 2 new actions in the model: * Wait to give the underlying runner time to process messages * ObserveConfirmedTx to check what's been observed by each node

We should probably remove it...

It's used in 2 different situations, one when observing some tx to appear, another one waiting for a spendable UTxO before submitting the tx

Our ObserveConfirmedTx action is not (yet) powerful enough to check the UTxO produced is there or has been consumed by another tx

This simplifies troubleshooting errors/failures

It was just a stopgap solution in order to limit the length of NewTx sequences we generate but it's not useful

github-actions · 2022-09-28T12:59:17Z

Unit Test Results

255 tests +1 249 ✔️ +1 14m 57s ⏱️ - 3m 41s
  91 suites ±0     6 💤 ±0
    5 files ±0     0 ❌ ±0

Results for commit cc45906. ± Comparison against base commit f3b881a.

♻️ This comment has been updated with latest results.

v0d1ch

This PR goes a bit over my head as I never used DynamicLogic but I think it looks good at least to my noob eyes.

hydra-node/test/Hydra/Model.hs

hydra-node/test/Hydra/ModelSpec.hs

ffakenz

🧙‍♂️

ghost force-pushed the ensemble/implement-liveness-in-DL branch from 54f1ca3 to 126a5da Compare September 28, 2022 09:39

ffakenz and others added 28 commits September 28, 2022 10:20

update index-state and remove source repository for quickcheck-dynamic

f3f880d

Update haskell.nix for recent hackage

d213757

Use nixpkgs as built & cached by haskell.nix

0d51399

Also update iohkNix to not get a deprecation warning from the crypto overlay.

Use websocat instead ws as the latter has been dropped from nix

85d2ca0

Revert this approach to instead just bump the source-repository-depen…

defd9f6

…dency Getting the package from hackage is not a problem, but our upstream dependencies are not fit for latest hackage versions and we did not want to bother chasing constraints at this point.

Try update the source-repository-package directly

970c4f8

Add subdir to q-d source dependency

109fb97

Move out ActionMonad and perform from our StateModel

e37dc2b

This is due to the new 1.0.0 interface of quickcheck-dynamic

Make Worldstate non-parameterized and remove code ❤️

950dfed

Replace generic Command action with specific actions

01e3d02

This kind of duplicates ClientInput

Make commit action return ActualCommitted

81e8ae8

Unfortunately, this was requiring to ditch record syntax as GADTs seem not to allow duplicate record fields with differing return types.

Define a waitMatch function on behavior level similar to our integrat…

2f39fc8

…ion tests

Fix perform commit usage of waitMatch

c9a6443

[wip] Add postcondition on commit action to check result

0141955

Provide a counter example of the action when postcondition failed

4f60d37

Refine postcondition monitor

17590a0

Make Commit action return a UTxOType Payment

d1f9360

This keeps the conversion back to simple utxos out of the model.

Show result of action in monitoring

5659abc

Instead of requiring a Show instance on monitoring function we can pattern match as suggested by Max.

Upgrade to q-d 1.1.0

b32c4e0

This gives us a Show instance for monitoring failures

Make performCommit compile

6a91334

Lookup signing key from UTxO's address

f32eda6

Minor formatting improvements over performCommit

674a978

Remove redundant assertion as it is already being checked by postcond…

9f7cefb

…ition in the model

[wip] introduce DL

6cd257e

Refactor runIOSimProp to use with DL formulas

887d312

Express conflict-free liveness property

7765177

This requires introduction of 2 new actions in the model: * Wait to give the underlying runner time to process messages * ObserveConfirmedTx to check what's been observed by each node

Update sha256 following bump in version:

9ff545a

Add missing instances and patterns

15a75cd

abailly added 9 commits September 28, 2022 10:21

Fix failing ModelSpec compilation

2a1eab6

[wip] start implementing missing actions

d1f5eb4

DL property compiles but fails to run

f2860bd

Make Stop no-op

e6af82e

We should probably remove it...

Refine check for UTxO to be visible

80ae565

It's used in 2 different situations, one when observing some tx to appear, another one waiting for a spendable UTxO before submitting the tx

Do not interleave more actinos before observing tx

ee17d0d

Our ObserveConfirmedTx action is not (yet) powerful enough to check the UTxO produced is there or has been consumed by another tx

Use same String representation for Payment and its UTxOType

362f44d

This simplifies troubleshooting errors/failures

Handle the case of multiple UTxO for same key

5500615

Fix imports following rebase

a2d952d

ghost force-pushed the ensemble/implement-liveness-in-DL branch from 126a5da to a2d952d Compare September 28, 2022 10:33

ghost marked this pull request as ready for review September 28, 2022 10:38

ghost requested review from ch1bo, KtorZ, ffakenz, pgrange and v0d1ch September 28, 2022 10:38

abailly added 2 commits September 28, 2022 12:13

Increase timeout for property

b540308

Remove useless Stop action

653a3fd

It was just a stopgap solution in order to limit the length of NewTx sequences we generate but it's not useful

v0d1ch approved these changes Sep 28, 2022

View reviewed changes

hydra-node/test/Hydra/Model.hs Outdated Show resolved Hide resolved

hydra-node/test/Hydra/ModelSpec.hs Outdated Show resolved Hide resolved

pgrange approved these changes Sep 28, 2022

View reviewed changes

Address reviewer's comments

cc45906

ffakenz approved these changes Sep 28, 2022

View reviewed changes

ghost merged commit 2505515 into master Sep 28, 2022

ghost deleted the ensemble/implement-liveness-in-DL branch September 28, 2022 18:04

This pull request was closed.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implement liveness property in dynamic logic #498

Implement liveness property in dynamic logic #498

ghost commented Sep 19, 2022 •

edited by ghost

Loading

github-actions bot commented Sep 19, 2022 •

edited

Loading

github-actions bot commented Sep 28, 2022 •

edited

Loading

v0d1ch left a comment

ffakenz left a comment

Implement liveness property in dynamic logic #498

Implement liveness property in dynamic logic #498

Conversation

ghost commented Sep 19, 2022 • edited by ghost Loading

github-actions bot commented Sep 19, 2022 • edited Loading

Transactions Costs

Cost of Init Transaction

Cost of Commit Transaction

Cost of CollectCom Transaction

Cost of Close Transaction

Cost of Contest Transaction

Cost of Abort Transaction

Cost of FanOut Transaction

github-actions bot commented Sep 28, 2022 • edited Loading

Unit Test Results

v0d1ch left a comment

Choose a reason for hiding this comment

ffakenz left a comment

Choose a reason for hiding this comment

ghost commented Sep 19, 2022 •

edited by ghost

Loading

github-actions bot commented Sep 19, 2022 •

edited

Loading

github-actions bot commented Sep 28, 2022 •

edited

Loading