Skip to content

Commit ca269d9

Browse files
williamdemeowilliamdemeo
committed
improvements
+ improve Dijkstra.Transaction + improve toc + add intro to "top-level" Spec modules
1 parent e8eac02 commit ca269d9

File tree

9 files changed

+429
-218
lines changed

9 files changed

+429
-218
lines changed

‎build-tools/static/md/mkdocs/includes/links.md‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@
3838
[GOVCERT]: Ledger.Conway.Specification.Certs.md#auxiliary-govcert-transition-system
3939
[Governance Functions]: Ledger.Conway.Specification.Gov.md#governance-functions
4040
[issues]: https://github.com/IntersectMBO/formal-ledger-specifications/issues
41+
[Introduction]: Ledger.Introduction.md
4142
[LEDGER]: Ledger.Conway.Specification.Ledger.md#ledger-transition-system
4243
[Ledger.Properties]: Ledger.Conway.Specification.Ledger.Properties.md
4344
[Ledger.Properties.GovDepsMatch]: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md
@@ -60,16 +61,19 @@
6061
[scriptsCost]: Ledger.Conway.Specification.Fees.md#scriptsCost
6162
[Shelley Ledger Spec (pdf)]: https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf
6263
[SNAP]: Ledger.Conway.Specification.Rewards.md#sec:snap-transition-system
64+
[STS Diagram]: Ledger.Introduction.md#fig:latest-sts-diagram
65+
[The GOV Transition System]: Ledger.Conway.Specification.Gov.md#the-gov-transition-system
6366
[The UTXOW Transition System]: Ledger.Conway.Specification.Utxow.md#sec:the-utxow-transition-system
6467
[thm:ChainGovDepsMatch]: Ledger.Conway.Specification.Chain.Properties.GovDepsMatch.md#thm:ChainGovDepsMatch
6568
[Time handling on Cardano]: https://docs.cardano.org/about-cardano/explore-more/time
6669
[Timing of Rewards Payout]: Ledger.Conway.Specification.Rewards.md#sec:timing-of-rewards-payout
67-
[The GOV Transition System]: Ledger.Conway.Specification.Gov.md#the-gov-transition-system
70+
[Transaction Levels]: Ledger.Dijkstra.Specification.Transaction.md#sec:transaction-levels
71+
[Transaction Structure]: Ledger.Dijkstra.Specification.Transaction.md#sec:transaction-structure
72+
[Transactions]: Ledger.Dijkstra.Specification.Transaction.md#sec:transactions
6873
[UTXO]: Ledger.Conway.Specification.Utxo.md#sec:the-utxo-transition-system
6974
[Utxo.Properties.MinSpend]: Ledger.Conway.Specification.Utxo.Properties.MinSpend.md
7075
[Utxo.Properties.PoV]: Ledger.Conway.Specification.Utxo.Properties.PoV.md
7176
[UTXOS]: Ledger.Conway.Specification.Utxo.md#sec:the-utxos-transition-rule
7277
[UTXOW]: Ledger.Conway.Specification.Utxow.md#sec:the-utxow-transition-system
7378
[Utxow module]: Ledger.Conway.Specification.Utxow.md
7479
[Validity and wellformedness predicates]: Ledger.Conway.Specification.Gov.md#validity-and-wellformedness-predicates
75-

‎build-tools/static/md/nav.yml‎

Lines changed: 178 additions & 175 deletions
Large diffs are not rendered by default.

‎src/Ledger.lagda.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ module Ledger where
88
99
import Ledger.Introduction
1010
import Ledger.PreConway
11+
import Ledger.Core
1112
import Ledger.Conway
1213
import Ledger.Dijkstra
1314

‎src/Ledger/Conway/Specification.lagda.md‎

Lines changed: 114 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,46 +3,159 @@ source_branch: master
33
source_path: src/Ledger/Conway/Specification.lagda.md
44
---
55

6+
This is the formal specification of the Cardano ledger for the Conway era.
7+
8+
The Agda source code which formalizes the ledger specification in the Conway era
9+
consists of the modules listed below. How these modules fit together to form a
10+
collection of interdependent state transition systems is illustrated by the
11+
[STS Diagram][] in the [Introduction][] section.
12+
13+
<!--
614
```agda
715
{-# OPTIONS --safe #-}
816
module Ledger.Conway.Specification where
17+
```
18+
-->
919

20+
## <span class="AgdaModule">BlockBody</span>
21+
22+
The Block Body Transition updates the block body state which comprises the
23+
ledger state and the map describing the produced blocks.
24+
25+
```agda
1026
import Ledger.Conway.Specification.BlockBody
1127
import Ledger.Conway.Specification.BlockBody.Properties
28+
```
29+
30+
31+
## Certificates
32+
33+
```agda
1234
import Ledger.Conway.Specification.Certs
1335
import Ledger.Conway.Specification.Certs.Properties
36+
```
37+
38+
39+
## <span class="AgdaModule">Chain</span>
40+
41+
```agda
1442
import Ledger.Conway.Specification.Chain
1543
import Ledger.Conway.Specification.Chain.Properties
44+
```
45+
46+
## Enactment
47+
48+
These modules concern the enactment of governance proposals and actions.
49+
50+
```agda
1651
import Ledger.Conway.Specification.Enact
1752
import Ledger.Conway.Specification.Enact.Properties
53+
```
54+
55+
## <span class="AgdaModule">Epoch</span>
56+
57+
```agda
1858
import Ledger.Conway.Specification.Epoch
1959
import Ledger.Conway.Specification.Epoch.Properties
60+
```
61+
62+
## <span class="AgdaModule">Fees</span>
63+
64+
This module defines a function that calculates the fee for reference scripts in a
65+
transaction.
66+
67+
```agda
2068
import Ledger.Conway.Specification.Fees
69+
```
70+
71+
## Governance
72+
73+
```agda
2174
import Ledger.Conway.Specification.Gov
2275
import Ledger.Conway.Specification.Gov.Actions
2376
import Ledger.Conway.Specification.Gov.Properties
2477
import Ledger.Conway.Specification.Gov.Properties.ChangePPGroup
78+
import Ledger.Conway.Specification.Types.GovStructure
79+
```
80+
81+
## <span class="AgdaModule">Ledger</span>
82+
83+
The `Ledger`{.AgdaModule} module defines the ledger transition system where valid
84+
transactions transform the ledger state.
85+
86+
```agda
2587
import Ledger.Conway.Specification.Ledger
2688
import Ledger.Conway.Specification.Ledger.Properties
89+
```
90+
91+
## Protocol Parameters
92+
93+
The defines the adjustable protocol parameters of the Cardano ledger.
94+
95+
```agda
2796
import Ledger.Conway.Specification.PParams
97+
```
98+
99+
## Properties of the Ledger Specification
100+
101+
```agda
28102
import Ledger.Conway.Specification.Properties
103+
```
104+
105+
## Ratification
106+
107+
```agda
29108
import Ledger.Conway.Specification.Ratify
30109
import Ledger.Conway.Specification.Ratify.Properties
110+
```
111+
112+
## <span class="AgdaModule">Rewards</span>
113+
114+
```agda
31115
import Ledger.Conway.Specification.Rewards
32116
import Ledger.Conway.Specification.RewardUpdate
33117
import Ledger.Conway.Specification.RewardUpdate.Properties
118+
```
119+
120+
## Scripts
121+
122+
```agda
34123
import Ledger.Conway.Specification.Script
35124
import Ledger.Conway.Specification.Script.Validation
125+
```
126+
127+
## Tests and Examples
128+
129+
```agda
36130
import Ledger.Conway.Specification.Test.Examples
37131
import Ledger.Conway.Specification.Test.StructuredContracts
132+
```
133+
134+
## Token Algebras
135+
136+
```agda
38137
import Ledger.Conway.Specification.TokenAlgebra.Base
39138
import Ledger.Conway.Specification.TokenAlgebra.Coin
40139
import Ledger.Conway.Specification.TokenAlgebra.ValueSet
41140
import Ledger.Conway.Specification.TokenAlgebra.ValueVector
141+
```
142+
143+
## Transactions
144+
145+
```agda
42146
import Ledger.Conway.Specification.Transaction
43-
import Ledger.Conway.Specification.Types.GovStructure
147+
```
148+
149+
## <span class="AgdaModule">Utxo</span>
150+
151+
```agda
44152
import Ledger.Conway.Specification.Utxo
45153
import Ledger.Conway.Specification.Utxo.Properties
154+
```
155+
156+
## <span class="AgdaModule">Utxow</span>
157+
158+
```agda
46159
import Ledger.Conway.Specification.Utxow
47160
import Ledger.Conway.Specification.Utxow.Properties
48161
```

‎src/Ledger/Conway/Specification/Utxo.lagda.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,5 @@
11
# UTxO {#sec:utxo}
22

3-
This section defines types and functions needed for the UTxO transition system.
4-
53
The UTxO transition system is built up from a number of smaller parts defined in this
64
section, culminating in the `UTXO`{.AgdaDatatype} rule given in the final
75
subsection below ([UTXO Inference Rule][UTXO]).
@@ -50,6 +48,8 @@ instance
5048

5149
## Functions supporting UTxO rules {#sec:functions-supporting-utxo-rules}
5250

51+
This section defines types and functions needed for the UTxO transition system.
52+
5353
```agda
5454
totExUnits : Tx → ExUnits
5555
totExUnits tx = ∑[ (_ , eu) ← tx .wits .txrdmrs ] eu

‎src/Ledger/Core.lagda.md‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
---
2+
source_branch: master
3+
source_path: src/Ledger/Core.lagda.md
4+
---
5+
6+
```agda
7+
module Ledger.Core where
8+
9+
import Ledger.Core.Specification
10+
```

‎src/Ledger/Core/Specification.lagda.md‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
---
2+
source_branch: master
3+
source_path: src/Ledger/Core.Specification.lagda.md
4+
---
5+
6+
```agda
7+
module Ledger.Core.Specification where
8+
9+
import Ledger.Core.Specification.Address
10+
import Ledger.Core.Specification.Crypto
11+
import Ledger.Core.Specification.Epoch
12+
```

‎src/Ledger/Dijkstra/Specification.lagda.md‎

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,65 @@
1+
---
2+
source_branch: master
3+
source_path: src/Ledger/Dijkstra/Specification.lagda.md
4+
---
5+
6+
This is the formal specification of the Cardano ledger for the Dijkstra era.
7+
The Agda source code which formalizes the ledger specification in the Conway era
8+
consists of the modules listed below.
9+
10+
<!--
111
```agda
212
{-# OPTIONS --safe #-}
313
module Ledger.Dijkstra.Specification where
14+
```
15+
-->
16+
17+
## Addresses
418

19+
```agda
520
import Ledger.Core.Specification.Address renaming (RwdAddr to RewardAddress)
21+
```
22+
23+
## <span class="AgdaModule">Epoch</span>
24+
25+
```agda
626
import Ledger.Core.Specification.Epoch
27+
```
728

29+
## Certificates
30+
31+
```agda
832
import Ledger.Dijkstra.Specification.Certs
33+
```
34+
35+
## Governance
36+
37+
```agda
938
import Ledger.Dijkstra.Specification.Gov.Base
1039
import Ledger.Dijkstra.Specification.Gov.Actions
40+
```
41+
42+
## Protocol Parameters
43+
44+
```agda
1145
import Ledger.Dijkstra.Specification.PParams
46+
```
47+
48+
## Scripts
49+
50+
```agda
1251
import Ledger.Dijkstra.Specification.Script
1352
import Ledger.Dijkstra.Specification.Script.Validation
53+
```
54+
55+
## Token Algebras
56+
57+
```agda
1458
import Ledger.Dijkstra.Specification.TokenAlgebra.Base
59+
```
60+
61+
## Transactions
62+
63+
```agda
1564
import Ledger.Dijkstra.Specification.Transaction
1665
```

0 commit comments

Comments
 (0)