Skip to content

Commit 6f41ea9

Browse files
javierdiaz72javierdiaz72
committed
Make all STSs in the Agda spec executable
1 parent f65e92a commit 6f41ea9

File tree

16 files changed

+430
-9
lines changed

16 files changed

+430
-9
lines changed

‎docs/agda-spec/src/Interface/HasOrder.agda‎

Lines changed: 32 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@ module _ {a} {A : Set a} where
6464
<-asymmetric : Asymmetric _<_
6565
<-asymmetric = ≤-antisym⇒<-asym ≤-antisym
6666

67-
open IsEquivalence ≈-isEquivalence renaming (sym to ≈-sym)
67+
open IsEquivalence ≈-isEquivalence using () renaming (sym to ≈-sym) public
6868

6969
<-trans : Transitive _<_
7070
<-trans i<j j<k =
@@ -78,20 +78,51 @@ module _ {a} {A : Set a} where
7878
<⇒¬>⊎≈ x<y (inj₁ y<x) = <-asymmetric x<y y<x
7979
<⇒¬>⊎≈ x<y (inj₂ x≈y) = <-irrefl (≈-sym x≈y) x<y
8080

81+
≥⇒≮ : ∀ {x y} → y ≤ x → ¬ (x < y)
82+
≥⇒≮ y≤x x<y = contradiction (to ≤⇔<∨≈ y≤x) (<⇒¬>⊎≈ x<y)
83+
84+
open HasPartialOrder ⦃...⦄
85+
8186
record HasDecPartialOrder : Set (sucˡ a) where
8287
field
8388
⦃ hasPartialOrder ⦄ : HasPartialOrder
8489
⦃ dec-≤ ⦄ : _≤_ ⁇²
8590
⦃ dec-< ⦄ : _<_ ⁇²
8691

92+
record HasTotalOrder : Set (sucˡ a) where
93+
field
94+
⦃ hasPartialOrder ⦄ : HasPartialOrder
95+
≤-total : Total _≤_
96+
97+
≤-isTotalOrder : IsTotalOrder _≈_ _≤_
98+
≤-isTotalOrder = record { isPartialOrder = ≤-isPartialOrder ; total = ≤-total }
99+
100+
≮⇒≥ : Decidable _≈_ → ∀ {x y} → ¬ (x < y) → y ≤ x
101+
≮⇒≥ _≈?_ {x} {y} x≮y with x ≈? y | ≤-total y x
102+
... | yes x≈y | _ = IsPreorder.reflexive ≤-isPreorder (≈-sym x≈y)
103+
... | _ | inj₁ y≤x = y≤x
104+
... | no x≉y | inj₂ x≤y = contradiction (≤∧≉⇒< (x≤y , x≉y)) x≮y
105+
106+
open HasTotalOrder ⦃...⦄
107+
108+
record HasDecTotalOrder : Set (sucˡ a) where
109+
field
110+
⦃ hasTotalOrder ⦄ : HasTotalOrder
111+
⦃ dec-≤ ⦄ : _≤_ ⁇²
112+
⦃ dec-< ⦄ : _<_ ⁇²
113+
87114
HasPreorder≡ = HasPreorder {_≈_ = _≡_}
88115
HasDecPreorder≡ = HasDecPreorder {_≈_ = _≡_}
89116
HasPartialOrder≡ = HasPartialOrder {_≈_ = _≡_}
90117
HasDecPartialOrder≡ = HasDecPartialOrder {_≈_ = _≡_}
118+
HasTotalOrder≡ = HasTotalOrder {_≈_ = _≡_}
119+
HasDecTotalOrder≡ = HasDecTotalOrder {_≈_ = _≡_}
91120

92121
open HasPreorder ⦃...⦄ public
93122
open HasPartialOrder ⦃...⦄ public hiding (hasPreorder)
94123
open HasDecPartialOrder ⦃...⦄ public hiding (hasPartialOrder)
124+
open HasTotalOrder ⦃...⦄ public hiding (hasPartialOrder)
125+
open HasDecTotalOrder ⦃...⦄ public hiding (hasTotalOrder)
95126

96127
module _ {a} {A : Set a} {_≈_ : Rel A a} where
97128

‎docs/agda-spec/src/Interface/HasOrder/Instance.agda‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,9 @@ instance
1616
ℕ-hasPartialOrder = HasPartialOrder ∋ record
1717
{ ≤-antisym = Nat.≤-antisym }
1818
ℕ-hasDecPartialOrder = HasDecPartialOrder {A = ℕ} ∋ record {}
19+
ℕ-hasTotalOrder = HasTotalOrder ∋ record
20+
{ ≤-total = Nat.≤-total }
21+
ℕ-hasDecTotalOrder = HasDecTotalOrder {A = ℕ} ∋ record {}
1922

2023
import Data.Integer.Properties as Int hiding (_≟_)
2124
ℤ-hasPreorder = HasPreorder ∋ record {Int; ≤⇔<∨≈ = let open Int in mk⇔
@@ -29,3 +32,6 @@ instance
2932
ℚ-hasPreorder = hasPreorderFromNonStrict Rat.≤-isPreorder _≟_
3033
ℚ-hasPartialOrder = HasPartialOrder ∋ record { ≤-antisym = Rat.≤-antisym }
3134
ℚ-hasDecPartialOrder = HasDecPartialOrder {A = ℚ} ∋ record {}
35+
ℚ-hasTotalOrder = HasTotalOrder ∋ record
36+
{ ≤-total = Rat.≤-total }
37+
ℚ-hasDecTotalOrder = HasDecTotalOrder {A = ℚ} ∋ record {}

‎docs/agda-spec/src/InterfaceLibrary/Ledger.lagda‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,10 +27,13 @@ record LedgerInterface : Type₁ where
2727
NewEpochState : Type
2828
getPParams : NewEpochState → PParams
2929
getEpoch : NewEpochState → Epoch
30-
getPoolDistr : NewEpochState → PoolDistr
30+
getPoolDistr : NewEpochState → PoolDistr
3131
adoptGenesisDelegs : NewEpochState → Slot → NewEpochState
3232
_⊢_⇀⦇_,NEWEPOCH⦈_ : ⊤ → NewEpochState → Epoch → NewEpochState → Type
3333
\end{code}
34+
\begin{code}[hide]
35+
⦃ Computational-NEWEPOCH ⦄ : Computational _⊢_⇀⦇_,NEWEPOCH⦈_ String
36+
\end{code}
3437
\caption{Ledger interface}
3538
\label{fig:interface:ledger}
3639
\end{figure*}

‎docs/agda-spec/src/Ledger/Crypto.lagda‎

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,12 @@ module Ledger.Crypto where
55

66
open import Ledger.Prelude hiding (T)
77

8+
module _ (M : Type↑) where
9+
_⁴ : ∀ {ℓ} {A B C D : Type ℓ} → (A → B → C → D → Type ℓ) → Type _
10+
_⁴ _~_~_~_ = ∀ {x y z w} → M (x ~ y ~ z ~ w)
11+
12+
_⁇⁴ = _⁇ ⁴
13+
814
\end{code}
915

1016
\subsection{Serialization}
@@ -20,7 +26,7 @@ record Serializer : Type₁ where
2026
\begin{code}
2127
Ser : Type
2228
encode : {T : Type} → T → Ser
23-
decode : {T : Type} → Ser → T
29+
decode : {T : Type} → Ser → Maybe T
2430
_∥_ : Ser → Ser → Ser
2531
\end{code}
2632
\emph{Properties}
@@ -29,7 +35,7 @@ record Serializer : Type₁ where
2935
enc-dec-correct :
3036
\end{code}
3137
\begin{code}
32-
∀ {T : Type} (x : T) → decode (encode x) ≡ x
38+
∀ {T : Type} (x : T) → decode (encode x) ≡ just x
3339
\end{code}
3440
\caption{Definitions for serialization}
3541
\label{fig:defs:serialization}
@@ -136,7 +142,7 @@ record KESScheme (srl : Serializer) : Type₁ where
136142
\end{code}
137143
\emph{Properties}
138144
\begin{code}[hide]
139-
field -- ⦃ Dec-isSigned ⦄ : isSigned ⁇⁴ -- TODO: Define ⁇⁴ if needed
145+
field ⦃ Dec-isSigned ⦄ : isSigned ⁇⁴
140146
isSigned-correct :
141147
\end{code}
142148
\begin{code}

‎docs/agda-spec/src/Ledger/Types/Epoch.agda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,12 +17,12 @@ additionVia sucFun (suc l) r = sucFun (additionVia sucFun l r)
1717

1818
record EpochStructure : Type₁ where
1919
field Slotʳ : Semiring 0ℓ 0ℓ
20-
KESPeriod : Type; ⦃ DecEq-KESPeriod ⦄ : DecEq KESPeriod; ⦃ HasPreorder-KESPeriod ⦄ : HasPreorder≡ {A = KESPeriod}
2120
Epoch : Type; ⦃ DecEq-Epoch ⦄ : DecEq Epoch; ⦃ Show-Epoch ⦄ : Show Epoch
21+
KESPeriod : Type; ⦃ DecEq-KESPeriod ⦄ : DecEq KESPeriod; ⦃ DecTo-KESPeriod ⦄ : HasDecTotalOrder≡ {A = KESPeriod}
2222

2323
Slot = Semiring.Carrier Slotʳ
2424

25-
field ⦃ DecPo-Slot ⦄ : HasDecPartialOrder≡ {A = Slot}
25+
field ⦃ DecTo-Slot ⦄ : HasDecTotalOrder≡ {A = Slot}
2626
⦃ DecEq-Slot ⦄ : DecEq Slot
2727

2828
epoch : Slot → Epoch

‎docs/agda-spec/src/Makefile‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,3 +39,7 @@ clean:
3939
$(LATEX_DIR)/$(PDF_NAME).*\
4040
$(LATEX_DIR)/*.aux\
4141
$(OUT_DIR)/
42+
43+
wipe: clean
44+
rm -rf $(LATEX_DIR)/Spec\
45+
$(OUT_DIR)/

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,9 @@ record BlockStructure : Type₁ where
3131
HashBBody : Type -- hash of a block body
3232
VRFRes : Type -- VRF result value
3333
\end{code}
34+
\begin{code}[hide]
35+
⦃ DecEq-HashHeader ⦄ : DecEq HashHeader
36+
\end{code}
3437
\emph{Concrete types}
3538
\begin{code}
3639
BlockNo = ℕ -- block number

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

Lines changed: 110 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,110 @@
1+
{-# OPTIONS --safe #-}
2+
3+
open import InterfaceLibrary.Ledger
4+
open import Spec.BaseTypes using (Nonces)
5+
open import Spec.BlockDefinitions
6+
open import Ledger.Crypto
7+
open import Ledger.Script
8+
open import Ledger.Types.Epoch
9+
open import Data.Rational.Ext
10+
11+
module Spec.ChainHead.Properties
12+
(crypto : _) (open Crypto crypto)
13+
(nonces : Nonces crypto) (open Nonces nonces)
14+
(es : _) (open EpochStructure es)
15+
(ss : ScriptStructure crypto es) (open ScriptStructure ss)
16+
(bs : BlockStructure crypto nonces es ss) (open BlockStructure bs)
17+
(af : _) (open AbstractFunctions af)
18+
(li : LedgerInterface crypto es ss) (let open LedgerInterface li)
19+
(rs : _) (open RationalExtStructure rs)
20+
where
21+
22+
open import Ledger.Prelude
23+
open import Ledger.PParams crypto es ss using (PParams; ProtVer)
24+
open import Spec.TickForecast crypto es ss li
25+
open import Spec.TickForecast.Properties crypto es ss li
26+
open import Spec.TickNonce crypto es nonces
27+
open import Spec.TickNonce.Properties crypto es nonces
28+
open import Spec.Protocol crypto nonces es ss bs af rs
29+
open import Spec.Protocol.Properties crypto nonces es ss bs af rs
30+
open import Spec.ChainHead crypto nonces es ss bs af li rs
31+
32+
instance
33+
34+
prtlSeqChecks⁇ : prtlSeqChecks ⁇²
35+
prtlSeqChecks⁇ {nothing} {_} .dec = yes tt
36+
prtlSeqChecks⁇ {lab@(just ⟦ bℓ , sℓ , _ ⟧ℓ)} {bh} .dec =
37+
sℓ <? slot ×-dec
38+
bℓ + 1 ≟ blockNo ×-dec
39+
ph ≟ prevHeader
40+
where
41+
open BHBody (proj₁ bh)
42+
ph = lastAppliedHash lab
43+
44+
chainChecks? : ∀ maxpv ps bh → Dec (chainChecks maxpv ps bh)
45+
chainChecks? maxpv (maxBHSize , maxBBSize , protocolVersion) bh =
46+
m ≤? maxpv ×-dec
47+
headerSize bh ≤? maxBHSize ×-dec
48+
bodySize ≤? maxBBSize
49+
where
50+
m = proj₁ protocolVersion
51+
open BHBody (proj₁ bh)
52+
53+
instance
54+
55+
_ = Monad-ComputationResult
56+
57+
Computational-CHAINHEAD : Computational _⊢_⇀⦇_,CHAINHEAD⦈_ String
58+
Computational-CHAINHEAD = record {Go} where
59+
open Computational ⦃...⦄ renaming (computeProof to comp; completeness to complete)
60+
computeTICKF = comp {STS = _⊢_⇀⦇_,TICKF⦈_}
61+
computeTICKN = comp {STS = _⊢_⇀⦇_,TICKN⦈_}
62+
computePRTCL = comp {STS = _⊢_⇀⦇_,PRTCL⦈_}
63+
module Go
64+
(nes : NewEpochState)
65+
(s : ChainHeadState) (let ⟦ cs , η₀ , ηv , ηc , ηh , lab ⟧ᶜˢ = s)
66+
(bh : BHeader) (let (bhb , σ) = bh; open BHBody bhb)
67+
where
68+
69+
e₁ = getEpoch nes
70+
nₚₕ = prevHashToNonce (lastAppliedHash lab)
71+
lab′ = just ⟦ blockNo , slot , headerHash bh ⟧ℓ
72+
ticknΓ = ⟦ ηc , nₚₕ ⟧ᵗᵉ
73+
ticknSt = ⟦ η₀ , ηh ⟧ᵗˢ
74+
prtclSt = ⟦ cs , ηv , ηc ⟧ᵖˢ
75+
76+
computeProof : ComputationResult String (∃[ s′ ] nes ⊢ s ⇀⦇ bh ,CHAINHEAD⦈ s′)
77+
computeProof = case ¿ prtlSeqChecks ¿² lab bh of λ where
78+
(no _) → failure "Failed in CHAINHEAD"
79+
(yes psc) → do
80+
(forecast , tickfStep) ← computeTICKF _ nes slot
81+
let
82+
e₂ = getEpoch forecast
83+
ne = (e₁ ≠ e₂)
84+
pp = getPParams forecast; open PParams
85+
pd = getPoolDistr forecast
86+
case chainChecks? MaxMajorPV (pp .maxHeaderSize , pp .maxBlockSize , pp .pv) bh of λ where
87+
(no _) → failure "Failed in CHAINHEAD"
88+
(yes cc) → do
89+
(⟦ η₀′ , _ ⟧ᵗˢ , ticknStep) ← computeTICKN ticknΓ ticknSt ne
90+
(_ , prtclStep) ← computePRTCL ⟦ pd , η₀′ ⟧ᵖᵉ prtclSt bh
91+
success (-, Chain-Head (psc , tickfStep , cc , ticknStep , prtclStep))
92+
93+
completeness : ∀ s′ → nes ⊢ s ⇀⦇ bh ,CHAINHEAD⦈ s′ → (proj₁ <$> computeProof) ≡ success s′
94+
completeness ⟦ cs′ , η₀′ , ηv′ , ηc′ , ηh′ , lab′ ⟧ᶜˢ (Chain-Head (psc , tickfStep , cc , ticknStep , prtclStep))
95+
with ¿ prtlSeqChecks ¿² lab bh
96+
... | no ¬psc = contradiction psc ¬psc
97+
... | yes _
98+
with computeTICKF _ nes slot | complete _ nes _ _ tickfStep
99+
... | success (forecast , _) | refl
100+
with
101+
(let pp = getPParams forecast; open PParams
102+
in chainChecks? MaxMajorPV (pp .maxHeaderSize , pp .maxBlockSize , pp .pv) bh)
103+
... | no ¬cc = contradiction cc ¬cc
104+
... | yes _
105+
with
106+
(let e₂ = getEpoch forecast; ne = (e₁ ≠ e₂)
107+
in computeTICKN ticknΓ ticknSt ne) | complete ticknΓ ticknSt _ _ ticknStep
108+
... | success (⟦ η₀′ , _ ⟧ᵗˢ , _) | refl
109+
with computePRTCL ⟦ getPoolDistr forecast , η₀′ ⟧ᵖᵉ prtclSt bh | complete ⟦ getPoolDistr forecast , η₀′ ⟧ᵖᵉ prtclSt _ _ prtclStep
110+
... | success _ | refl = refl

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,7 @@ data _⊢_⇀⦇_,OCERT⦈_ where
112112
in
113113
∙ c₀ ≤ kp
114114
∙ kp < c₀ +ᵏ MaxKESEvo
115-
∙ ∃[ m ] just m ≡ currentIssueNo stpools cs hk × (n ≡ m ⊎ n ≡ suc m)
115+
∙ ∃[ m ] (just m ≡ currentIssueNo stpools cs hk × (n ≡ m ⊎ n ≡ suc m))
116116
∙ isSignedˢ issuerVk (encode (vkₕ , n , c₀)) τ
117117
∙ isSignedᵏ vkₕ t (encode bhb) σ
118118
────────────────────────────────

‎docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
{-# OPTIONS --safe #-}
2+
3+
open import Ledger.Crypto
4+
open import Ledger.Script
5+
open import Ledger.Types.Epoch
6+
open import Spec.BaseTypes using (Nonces)
7+
open import Spec.BlockDefinitions
8+
9+
module Spec.OperationalCertificate.Properties
10+
(crypto : _) (open Crypto crypto)
11+
(nonces : Nonces crypto) (open Nonces nonces)
12+
(es : _) (open EpochStructure es)
13+
(ss : ScriptStructure crypto es) (open ScriptStructure ss)
14+
(bs : BlockStructure crypto nonces es ss) (open BlockStructure bs)
15+
(af : _) (open AbstractFunctions af)
16+
where
17+
18+
open import Ledger.Prelude
19+
open import Data.Maybe.Relation.Unary.Any as M
20+
open import Spec.OperationalCertificate crypto nonces es ss bs af
21+
22+
instance
23+
24+
Computational-OCERT : Computational _⊢_⇀⦇_,OCERT⦈_ String
25+
Computational-OCERT = record {Go} where
26+
module Go (stpools : OCertEnv) (cs : OCertState) (bh : BHeader) where
27+
bhb = bh .proj₁; open BHBody bhb
28+
σ = bh .proj₂
29+
open OCert oc renaming (σ to τ)
30+
hk = hash issuerVk
31+
kp = kesPeriod slot
32+
t = kp -ᵏ c₀
33+
34+
hyps = ¿ c₀ ≤ kp
35+
× kp < c₀ +ᵏ MaxKESEvo
36+
× M.Any (λ m → n ≡ m ⊎ n ≡ suc m) (currentIssueNo stpools cs hk)
37+
× isSignedˢ issuerVk (encode (vkₕ , n , c₀)) τ
38+
× isSignedᵏ vkₕ t (encode bhb) σ ¿
39+
40+
computeProof : ComputationResult String (∃[ cs′ ] stpools ⊢ cs ⇀⦇ bh ,OCERT⦈ cs′)
41+
computeProof with hyps
42+
... | no ¬p = failure "Failed in OCERT"
43+
... | yes (p₁ , p₂ , p₃ , p₄ , p₅) = success (-, Update-OCert (p₁ , p₂ , satisfied× p₃ , p₄ , p₅))
44+
where
45+
satisfied× : ∀ {a p} {A : Set a} {y : Maybe A} {P : Pred A p} → M.Any P y → ∃[ x ] just x ≡ y × P x
46+
satisfied× (just Px) = (-, refl , Px)
47+
48+
completeness : ∀ cs′ → stpools ⊢ cs ⇀⦇ bh ,OCERT⦈ cs′ → (proj₁ <$> computeProof) ≡ success cs′
49+
completeness _ (Update-OCert (p₁ , p₂ , (_ , p , q) , p₄ , p₅))
50+
with hyps
51+
... | yes prf rewrite dec-yes hyps prf .proj₂ = refl
52+
... | no ¬prf = contradiction (p₁ , p₂ , AnyP×≡→AnyP (Equivalence.to M.just-equivalence q) p , p₄ , p₅) ¬prf
53+
where
54+
AnyP×≡→AnyP : ∀ {a p} {A : Set a} {x : A} {y : Maybe A} {P : Pred A p} → M.Any P (just x) → just x ≡ y → M.Any P y
55+
AnyP×≡→AnyP {P = P} prf eq = subst (M.Any P) eq prf

0 commit comments

Comments
 (0)