Skip to content

Commit 23ea2f3

Browse files
yveshauseryveshauser
committed
Code formatting
1 parent 5f0d66f commit 23ea2f3

File tree

1 file changed

+68
-72
lines changed

1 file changed

+68
-72
lines changed

‎formal-spec/Leios/Defaults.agda‎

Lines changed: 68 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -17,10 +17,6 @@ open Equivalence
1717

1818
-- The module contains very simple implementations for the functionalities
1919
-- that allow to build examples for traces for the different Leios variants
20-
--
21-
-- As parameters the module expects
22-
-- * numberOfParties: the total number of participants
23-
-- * SUT-id: the number of the SUT (system under test)
2420
module Leios.Defaults (params : Params) (let open Params params) where
2521

2622
instance
@@ -30,17 +26,17 @@ instance
3026
d-Abstract : LeiosAbstract
3127
d-Abstract =
3228
record
33-
{ Tx = ℕ
34-
; PoolID = Fin numberOfParties
29+
{ Tx = ℕ
30+
; PoolID = Fin numberOfParties
3531
; BodyHash = List ℕ
36-
; VrfPf = ⊤
37-
; PrivKey = ⊤
38-
; Sig = ⊤
39-
; Hash = List ℕ
40-
; Vote = ⊤
41-
; vote = λ _ _ → tt
42-
; sign = λ _ _ → tt
43-
; L = stageLength
32+
; VrfPf = ⊤
33+
; PrivKey = ⊤
34+
; Sig = ⊤
35+
; Hash = List ℕ
36+
; Vote = ⊤
37+
; vote = λ _ _ → tt
38+
; sign = λ _ _ → tt
39+
; L = stageLength
4440
}
4541

4642
open LeiosAbstract d-Abstract public
@@ -73,7 +69,7 @@ d-KeyRegistration = _
7369
d-KeyRegistrationFunctionality : KeyRegistrationAbstract.Functionality d-KeyRegistration
7470
d-KeyRegistrationFunctionality =
7571
record
76-
{ State = ⊤
72+
{ State = ⊤
7773
; _-⟦_/_⟧⇀_ = λ _ _ _ _ → ⊤
7874
}
7975

@@ -82,19 +78,19 @@ open import Leios.Base d-Abstract d-VRF public
8278
d-Base : BaseAbstract
8379
d-Base =
8480
record
85-
{ Cert = ⊤
86-
; VTy = ⊤
87-
; initSlot = λ _ → 0
81+
{ Cert = ⊤
82+
; VTy = ⊤
83+
; initSlot = λ _ → 0
8884
; V-chkCerts = λ _ _ → true
8985
}
9086

9187
d-BaseFunctionality : BaseAbstract.Functionality d-Base
9288
d-BaseFunctionality =
9389
record
94-
{ State = ⊤
95-
; _-⟦_/_⟧⇀_ = λ _ _ _ _ → ⊤
90+
{ State = ⊤
91+
; _-⟦_/_⟧⇀_ = λ _ _ _ _ → ⊤
9692
; Dec-_-⟦_/_⟧⇀_ = ⁇ (yes tt)
97-
; SUBMIT-total = tt , tt
93+
; SUBMIT-total = tt , tt
9894
}
9995

10096
open import Leios.FFD public
@@ -105,7 +101,7 @@ instance
105101
record
106102
{ slotNumber = λ _ → 0
107103
; producerID = λ _ → sutId
108-
; lotteryPf = λ _ → tt
104+
; lotteryPf = λ _ → tt
109105
}
110106

111107
hhs : Hashable PreIBHeader (List ℕ)
@@ -138,20 +134,20 @@ flushIns record { inIBs = ibs ; inEBs = ebs ; inVTs = vts } =
138134
flushIBs (record {header = h; body = b} ∷ ibs) = inj₁ (ibHeader h) ∷ inj₂ (ibBody b) ∷ flushIBs ibs
139135

140136
data SimpleFFD : FFDState → FFDAbstract.Input ffdAbstract → FFDAbstract.Output ffdAbstract → FFDState → Type where
141-
SendIB : ∀ {s h b} → SimpleFFD s (FFDAbstract.Send (ibHeader h) (just (ibBody b))) FFDAbstract.SendRes (record s { outIBs = record {header = h; body = b} ∷ outIBs s})
142-
SendEB : ∀ {s eb} → SimpleFFD s (FFDAbstract.Send (ebHeader eb) nothing) FFDAbstract.SendRes (record s { outEBs = eb ∷ outEBs s})
143-
SendVS : ∀ {s vs} → SimpleFFD s (FFDAbstract.Send (vtHeader vs) nothing) FFDAbstract.SendRes (record s { outVTs = vs ∷ outVTs s})
137+
SendIB : ∀ {s h b} → SimpleFFD s (FFDAbstract.Send (ibHeader h) (just (ibBody b))) FFDAbstract.SendRes (record s { outIBs = record {header = h; body = b} ∷ outIBs s})
138+
SendEB : ∀ {s eb} → SimpleFFD s (FFDAbstract.Send (ebHeader eb) nothing) FFDAbstract.SendRes (record s { outEBs = eb ∷ outEBs s})
139+
SendVS : ∀ {s vs} → SimpleFFD s (FFDAbstract.Send (vtHeader vs) nothing) FFDAbstract.SendRes (record s { outVTs = vs ∷ outVTs s})
144140

145-
BadSendIB : ∀ {s h} → SimpleFFD s (FFDAbstract.Send (ibHeader h) nothing) FFDAbstract.SendRes s
141+
BadSendIB : ∀ {s h} → SimpleFFD s (FFDAbstract.Send (ibHeader h) nothing) FFDAbstract.SendRes s
146142
BadSendEB : ∀ {s h b} → SimpleFFD s (FFDAbstract.Send (ebHeader h) (just b)) FFDAbstract.SendRes s
147143
BadSendVS : ∀ {s h b} → SimpleFFD s (FFDAbstract.Send (vtHeader h) (just b)) FFDAbstract.SendRes s
148144

149-
Fetch : ∀ {s} → SimpleFFD s FFDAbstract.Fetch (FFDAbstract.FetchRes (flushIns s)) (record s { inIBs = [] ; inEBs = [] ; inVTs = [] })
145+
Fetch : ∀ {s} → SimpleFFD s FFDAbstract.Fetch (FFDAbstract.FetchRes (flushIns s)) (record s { inIBs = [] ; inEBs = [] ; inVTs = [] })
150146

151147
send-total : ∀ {s h b} → ∃[ s' ] (SimpleFFD s (FFDAbstract.Send h b) FFDAbstract.SendRes s')
152148
send-total {s} {ibHeader h} {just (ibBody b)} = record s { outIBs = record {header = h; body = b} ∷ outIBs s} , SendIB
153-
send-total {s} {ebHeader eb} {nothing} = record s { outEBs = eb ∷ outEBs s} , SendEB
154-
send-total {s} {vtHeader vs} {nothing} = record s { outVTs = vs ∷ outVTs s} , SendVS
149+
send-total {s} {ebHeader eb} {nothing} = record s { outEBs = eb ∷ outEBs s} , SendEB
150+
send-total {s} {vtHeader vs} {nothing} = record s { outVTs = vs ∷ outVTs s} , SendVS
155151

156152
send-total {s} {ibHeader h} {nothing} = s , BadSendIB
157153
send-total {s} {ebHeader eb} {just _} = s , BadSendEB
@@ -161,9 +157,9 @@ fetch-total : ∀ {s} → ∃[ x ] (∃[ s' ] (SimpleFFD s FFDAbstract.Fetch (FF
161157
fetch-total {s} = flushIns s , (record s { inIBs = [] ; inEBs = [] ; inVTs = [] } , Fetch)
162158

163159
send-complete : ∀ {s h b s'} → SimpleFFD s (FFDAbstract.Send h b) FFDAbstract.SendRes s' → s' ≡ proj₁ (send-total {s} {h} {b})
164-
send-complete SendIB = refl
165-
send-complete SendEB = refl
166-
send-complete SendVS = refl
160+
send-complete SendIB = refl
161+
send-complete SendEB = refl
162+
send-complete SendVS = refl
167163
send-complete BadSendIB = refl
168164
send-complete BadSendEB = refl
169165
send-complete BadSendVS = refl
@@ -191,10 +187,10 @@ instance
191187
d-FFDFunctionality : FFDAbstract.Functionality ffdAbstract
192188
d-FFDFunctionality =
193189
record
194-
{ State = FFDState
195-
; initFFDState = record { inIBs = []; inEBs = []; inVTs = []; outIBs = []; outEBs = []; outVTs = [] }
196-
; _-⟦_/_⟧⇀_ = SimpleFFD
197-
; Dec-_-⟦_/_⟧⇀_ = Dec-SimpleFFD
190+
{ State = FFDState
191+
; initFFDState = record { inIBs = []; inEBs = []; inVTs = []; outIBs = []; outEBs = []; outVTs = [] }
192+
; _-⟦_/_⟧⇀_ = SimpleFFD
193+
; Dec-_-⟦_/_⟧⇀_ = Dec-SimpleFFD
198194
; FFD-Send-total = send-total
199195
}
200196

@@ -203,61 +199,61 @@ open import Leios.Voting public
203199
d-VotingAbstract : VotingAbstract (Fin 1 × EndorserBlock)
204200
d-VotingAbstract =
205201
record
206-
{ VotingState = ⊤
202+
{ VotingState = ⊤
207203
; initVotingState = tt
208204
; isVoteCertified = λ _ _ → ⊤
209205
}
210206

211207
d-VotingAbstract-2 : VotingAbstract (Fin 2 × EndorserBlock)
212208
d-VotingAbstract-2 =
213209
record
214-
{ VotingState = ⊤
210+
{ VotingState = ⊤
215211
; initVotingState = tt
216212
; isVoteCertified = λ _ _ → ⊤
217213
}
218214

219215
d-SpecStructure : SpecStructure 1
220216
d-SpecStructure = record
221-
{ a = d-Abstract
222-
; Hashable-PreIBHeader = hhs
217+
{ a = d-Abstract
218+
; Hashable-PreIBHeader = hhs
223219
; Hashable-PreEndorserBlock = hpe
224-
; id = sutId
225-
; FFD' = d-FFDFunctionality
226-
; vrf' = d-VRF
227-
; sk-IB = tt
228-
; sk-EB = tt
229-
; sk-V = tt
230-
; pk-IB = tt
231-
; pk-EB = tt
232-
; pk-V = tt
233-
; B' = d-Base
234-
; BF = d-BaseFunctionality
235-
; initBaseState = tt
236-
; K' = d-KeyRegistration
237-
; KF = d-KeyRegistrationFunctionality
238-
; va = d-VotingAbstract
220+
; id = sutId
221+
; FFD' = d-FFDFunctionality
222+
; vrf' = d-VRF
223+
; sk-IB = tt
224+
; sk-EB = tt
225+
; sk-V = tt
226+
; pk-IB = tt
227+
; pk-EB = tt
228+
; pk-V = tt
229+
; B' = d-Base
230+
; BF = d-BaseFunctionality
231+
; initBaseState = tt
232+
; K' = d-KeyRegistration
233+
; KF = d-KeyRegistrationFunctionality
234+
; va = d-VotingAbstract
239235
}
240236

241237
d-SpecStructure-2 : SpecStructure 2
242238
d-SpecStructure-2 = record
243-
{ a = d-Abstract
244-
; Hashable-PreIBHeader = hhs
239+
{ a = d-Abstract
240+
; Hashable-PreIBHeader = hhs
245241
; Hashable-PreEndorserBlock = hpe
246-
; id = sutId
247-
; FFD' = d-FFDFunctionality
248-
; vrf' = d-VRF
249-
; sk-IB = tt
250-
; sk-EB = tt
251-
; sk-V = tt
252-
; pk-IB = tt
253-
; pk-EB = tt
254-
; pk-V = tt
255-
; B' = d-Base
256-
; BF = d-BaseFunctionality
257-
; initBaseState = tt
258-
; K' = d-KeyRegistration
259-
; KF = d-KeyRegistrationFunctionality
260-
; va = d-VotingAbstract-2
242+
; id = sutId
243+
; FFD' = d-FFDFunctionality
244+
; vrf' = d-VRF
245+
; sk-IB = tt
246+
; sk-EB = tt
247+
; sk-V = tt
248+
; pk-IB = tt
249+
; pk-EB = tt
250+
; pk-V = tt
251+
; B' = d-Base
252+
; BF = d-BaseFunctionality
253+
; initBaseState = tt
254+
; K' = d-KeyRegistration
255+
; KF = d-KeyRegistrationFunctionality
256+
; va = d-VotingAbstract-2
261257
}
262258

263259
open import Leios.Short d-SpecStructure public

0 commit comments

Comments
 (0)