Skip to content

Commit 6770198

Browse files
javierdiaz72amesgen
javierdiaz72
authored and
amesgen
committed
Hide field and constructor ... in record's
1 parent 01448d4 commit 6770198

File tree

5 files changed

+115
-38
lines changed

5 files changed

+115
-38
lines changed

‎docs/agda-spec/src/Spec/BlockDefinitions.lagda‎

Lines changed: 32 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -21,10 +21,10 @@ open import Ledger.PParams crypto es ss using (ProtVer)
2121

2222
record BlockStructure : Type₁ where
2323
field
24-
2524
\end{code}
2625

27-
\begin{figure*}[htb]
26+
\begin{figure*}[h]
27+
\begin{AgdaAlign}
2828
\emph{Abstract types}
2929
\begin{code}
3030
HashHeader : Type -- hash of a block header
@@ -36,29 +36,43 @@ record BlockStructure : Type₁ where
3636
BlockNo = ℕ -- block number
3737
\end{code}
3838
\emph{Operational Certificate}
39+
\begin{AgdaSuppressSpace}
3940
\begin{code}
4041
record OCert : Type where
42+
\end{code}
43+
\begin{code}[hide]
4144
constructor ⟦_,_,_,_⟧ᵒᶜ
42-
field vkₕ : VKeyᵏ -- operational (hot) key
43-
n : ℕ -- certificate issue number
44-
c₀ : KESPeriod -- start KES period
45-
σ : Sigˢ -- cold key signature
45+
field
46+
\end{code}
47+
\begin{code}
48+
vkₕ : VKeyᵏ -- operational (hot) key
49+
n : ℕ -- certificate issue number
50+
c₀ : KESPeriod -- start KES period
51+
σ : Sigˢ -- cold key signature
4652
\end{code}
53+
\end{AgdaSuppressSpace}
4754
\emph{Block Header Body}
55+
\begin{AgdaSuppressSpace}
4856
\begin{code}
4957
record BHBody : Type where
50-
field prevHeader : Maybe HashHeader -- hash of previous block header
51-
issuerVk : VKeyˢ -- block issuer
52-
vrfVk : VKeyᵛ -- VRF verification key
53-
blockNo : BlockNo -- block number
54-
slot : Slot -- block slot
55-
vrfRes : VRFRes -- VRF result value
56-
vrfPrf : Proof -- VRF proof
57-
bodySize : ℕ -- size of the block body
58-
bodyHash : HashBBody -- block body hash
59-
oc : OCert -- operational certificate
60-
pv : ProtVer -- protocol version
6158
\end{code}
59+
\begin{code}[hide]
60+
field
61+
\end{code}
62+
\begin{code}
63+
prevHeader : Maybe HashHeader -- hash of previous block header
64+
issuerVk : VKeyˢ -- block issuer
65+
vrfVk : VKeyᵛ -- VRF verification key
66+
blockNo : BlockNo -- block number
67+
slot : Slot -- block slot
68+
vrfRes : VRFRes -- VRF result value
69+
vrfPrf : Proof -- VRF proof
70+
bodySize : ℕ -- size of the block body
71+
bodyHash : HashBBody -- block body hash
72+
oc : OCert -- operational certificate
73+
pv : ProtVer -- protocol version
74+
\end{code}
75+
\end{AgdaSuppressSpace}
6276
\emph{Block Types}
6377
\begin{code}
6478
BHeader = BHBody × Sigᵏ -- block header
@@ -76,6 +90,7 @@ record BlockStructure : Type₁ where
7690
serHashToℕ : SerHash → ∃[ n ] n < 2 ^ 512 -- [0, 2^512) (64-byte VRF output)
7791
serHashToNonce : SerHash → Nonce
7892
\end{code}
93+
\end{AgdaAlign}
7994
\caption{Block definitions}
8095
\label{fig:defs:blocks}
8196
\end{figure*}

‎docs/agda-spec/src/Spec/ChainHead.lagda‎

Lines changed: 23 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -52,27 +52,40 @@ open import Ledger.Prelude
5252
\end{code}
5353

5454
\begin{figure*}[h]
55+
\begin{AgdaAlign}
5556
\emph{Chain Head environments}
5657
\begin{code}
5758
ChainHeadEnv = NewEpochState
5859
\end{code}
5960
\emph{Chain Head states}
61+
\begin{AgdaSuppressSpace}
6062
\begin{code}
6163
record LastAppliedBlock : Type where
64+
\end{code}
65+
\begin{code}[hide]
6266
constructor ⟦_,_,_⟧ℓ
63-
field bℓ : BlockNo -- last block number
64-
sℓ : Slot -- last slot
65-
h : HashHeader -- latest header hash
67+
field
68+
\end{code}
69+
\begin{code}
70+
bℓ : BlockNo -- last block number
71+
sℓ : Slot -- last slot
72+
h : HashHeader -- latest header hash
6673

6774
record ChainHeadState : Type where
75+
\end{code}
76+
\begin{code}[hide]
6877
constructor ⟦_,_,_,_,_,_⟧ᶜˢ
69-
field cs : OCertCounters -- operational certificate issue numbers
70-
η₀ : Nonce -- epoch nonce
71-
ηv : Nonce -- evolving nonce
72-
ηc : Nonce -- candidate nonce
73-
ηh : Nonce -- nonce from hash of last epoch’s last header
74-
lab : Maybe LastAppliedBlock -- latest applied block
78+
field
79+
\end{code}
80+
\begin{code}
81+
cs : OCertCounters -- operational certificate issue numbers
82+
η₀ : Nonce -- epoch nonce
83+
ηv : Nonce -- evolving nonce
84+
ηc : Nonce -- candidate nonce
85+
ηh : Nonce -- nonce from hash of last epoch’s last header
86+
lab : Maybe LastAppliedBlock -- latest applied block
7587
\end{code}
88+
\end{AgdaSuppressSpace}
7689
\emph{Chain Head transitions}
7790
\begin{code}[hide]
7891
data
@@ -100,6 +113,7 @@ prtlSeqChecks lab@(just ⟦ bℓ , sℓ , _ ⟧ℓ) bh = sℓ < slot × bℓ + 1
100113
open BHBody (proj₁ bh)
101114
ph = lastAppliedHash lab
102115
\end{code}
116+
\end{AgdaAlign}
103117
\caption{Chain Head transition system types and functions}
104118
\label{fig:ts-types:chainhead}
105119
\end{figure*}

‎docs/agda-spec/src/Spec/Protocol.lagda‎

Lines changed: 21 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -48,28 +48,44 @@ open Ledger.Prelude.ℤ using (pos)
4848
\end{code}
4949

5050
\begin{figure*}[h]
51+
\begin{AgdaAlign}
5152
\emph{Protocol environments}
53+
\begin{AgdaSuppressSpace}
5254
\begin{code}
5355
record PrtclEnv : Type where
56+
\end{code}
57+
\begin{code}[hide]
5458
constructor ⟦_,_⟧ᵖᵉ
55-
field pd : PoolDistr -- pool stake distribution
56-
η₀ : Nonce -- epoch nonce
59+
field
5760
\end{code}
61+
\begin{code}
62+
pd : PoolDistr -- pool stake distribution
63+
η₀ : Nonce -- epoch nonce
64+
\end{code}
65+
\end{AgdaSuppressSpace}
5866
\emph{Protocol states}
67+
\begin{AgdaSuppressSpace}
5968
\begin{code}
6069
record PrtclState : Type where
70+
\end{code}
71+
\begin{code}[hide]
6172
constructor ⟦_,_,_⟧ᵖˢ
62-
field cs : OCertCounters -- operational certificate issues numbers
63-
ηv : Nonce -- evolving nonce
64-
ηc : Nonce -- candidate nonce
73+
field
74+
\end{code}
75+
\begin{code}
76+
cs : OCertCounters -- operational certificate issues numbers
77+
ηv : Nonce -- evolving nonce
78+
ηc : Nonce -- candidate nonce
6579
\end{code}
80+
\end{AgdaSuppressSpace}
6681
\emph{Protocol transitions}
6782
\begin{code}[hide]
6883
data
6984
\end{code}
7085
\begin{code}
7186
_⊢_⇀⦇_,PRTCL⦈_ : PrtclEnv → PrtclState → BHeader → PrtclState → Type
7287
\end{code}
88+
\end{AgdaAlign}
7389
\caption{Protocol transition system types}
7490
\label{fig:ts-types:prtcl}
7591
\end{figure*}

‎docs/agda-spec/src/Spec/TickNonce.lagda‎

Lines changed: 20 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -26,27 +26,43 @@ open import Ledger.Prelude
2626
\end{code}
2727

2828
\begin{figure*}[h]
29+
\begin{AgdaAlign}
2930
\emph{Tick Nonce environments}
31+
\begin{AgdaSuppressSpace}
3032
\begin{code}
3133
record TickNonceEnv : Type where
34+
\end{code}
35+
\begin{code}[hide]
3236
constructor ⟦_,_⟧ᵗᵉ
33-
field ηc : Nonce -- candidate nonce
34-
ηph : Nonce -- previous header hash as nonce
37+
field
38+
\end{code}
39+
\begin{code}
40+
ηc : Nonce -- candidate nonce
41+
ηph : Nonce -- previous header hash as nonce
3542
\end{code}
43+
\end{AgdaSuppressSpace}
3644
\emph{Tick Nonce states}
45+
\begin{AgdaSuppressSpace}
3746
\begin{code}
3847
record TickNonceState : Type where
48+
\end{code}
49+
\begin{code}[hide]
3950
constructor ⟦_,_⟧ᵗˢ
40-
field η₀ : Nonce -- epoch nonce
41-
ηh : Nonce -- nonce from hash of previous epoch's last block header
51+
field
52+
\end{code}
53+
\begin{code}
54+
η₀ : Nonce -- epoch nonce
55+
ηh : Nonce -- nonce from hash of previous epoch's last block header
4256
\end{code}
57+
\end{AgdaSuppressSpace}
4358
\emph{Tick Nonce transitions}
4459
\begin{code}[hide]
4560
data
4661
\end{code}
4762
\begin{code}
4863
_⊢_⇀⦇_,TICKN⦈_ : TickNonceEnv → TickNonceState → Bool → TickNonceState → Type
4964
\end{code}
65+
\end{AgdaAlign}
5066
\caption{Tick Nonce transition system types}
5167
\label{fig:ts-types:ticknonce}
5268
\end{figure*}

‎docs/agda-spec/src/Spec/UpdateNonce.lagda‎

Lines changed: 19 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -25,26 +25,42 @@ open import Ledger.Prelude
2525
\end{code}
2626

2727
\begin{figure*}[h]
28+
\begin{AgdaAlign}
2829
\emph{Update Nonce environments}
30+
\begin{AgdaSuppressSpace}
2931
\begin{code}
3032
record UpdateNonceEnv : Type where
33+
\end{code}
34+
\begin{code}[hide]
3135
constructor ⟦_⟧ᵘᵉ
32-
field η : Nonce -- new nonce
36+
field
3337
\end{code}
38+
\begin{code}
39+
η : Nonce -- new nonce
40+
\end{code}
41+
\end{AgdaSuppressSpace}
3442
\emph{Update Nonce states}
43+
\begin{AgdaSuppressSpace}
3544
\begin{code}
3645
record UpdateNonceState : Type where
46+
\end{code}
47+
\begin{code}[hide]
3748
constructor ⟦_,_⟧ᵘˢ
38-
field ηv : Nonce -- evolving nonce
39-
ηc : Nonce -- candidate nonce
49+
field
50+
\end{code}
51+
\begin{code}
52+
ηv : Nonce -- evolving nonce
53+
ηc : Nonce -- candidate nonce
4054
\end{code}
55+
\end{AgdaSuppressSpace}
4156
\emph{Update Nonce transitions}
4257
\begin{code}[hide]
4358
data
4459
\end{code}
4560
\begin{code}
4661
_⊢_⇀⦇_,UPDN⦈_ : UpdateNonceEnv → UpdateNonceState → Slot → UpdateNonceState → Type
4762
\end{code}
63+
\end{AgdaAlign}
4864
\caption{Update Nonce transition system types}
4965
\label{fig:ts-types:updnonce}
5066
\end{figure*}

0 commit comments

Comments
 (0)