Implement liveness property in dynamic logic

[ghost]

fix #467

[ch1bo]

Could: inline newTx

[ghost]

Thanks. This PR is still a draft, I just refreshed it following a discussion we had with @pgrange who was interested in having a look at what we are currently working on concretely.

[github-actions]

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-19 13:24:39.481447621 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	4837	9.52	3.75	0.47
2	5038	11.13	4.37	0.49
3	5243	13.29	5.20	0.53
5	5652	18.45	7.23	0.60
10	6678	27.72	10.78	0.75
46	14060	98.77	38.15	1.84

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.73	7.96	0.62

Cost of CollectCom Transaction

Parties	Tx size	% max Mem	% max CPU	Min fee ₳
1	13058	20.77	8.32	0.95
2	13380	36.55	14.80	1.14
3	13702	54.66	22.31	1.36
4	14093	78.14	32.04	1.63

Cost of Close Transaction

Parties	Tx size	% max Mem	% max CPU	Min fee ₳
1	9323	8.19	3.36	0.65
2	9488	8.97	3.81	0.67
3	9727	10.58	4.59	0.70
5	9989	11.31	5.17	0.72
10	10842	15.60	7.58	0.81
30	14182	31.82	16.85	1.15
70	16213	41.68	15.78	1.31

Cost of Contest Transaction

Parties	Tx size	% max Mem	% max CPU	Min fee ₳
1	9328	8.16	3.34	0.65
2	9495	8.94	3.79	0.67
3	9691	10.16	4.42	0.69
5	10047	12.12	5.47	0.73
10	10884	16.20	7.80	0.82
30	14206	32.00	16.91	1.16
43	16370	42.74	23.01	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	13495	22.50	9.35	0.99
2	13604	34.02	14.28	1.13
3	13927	52.63	22.47	1.35
4	14037	69.17	29.63	1.54
5	14434	97.19	42.44	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	13416	9.88	4.31	0.85
2	13521	11.78	5.34	0.88
3	13550	13.30	6.22	0.90
5	13692	16.72	8.12	0.95
10	13742	23.82	12.33	1.04
50	15313	85.26	47.74	1.86
60	15536	99.74	56.26	2.05