Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

PDF cleanup 282: rename sucᵉ to 1 +ᵉ_ #363

Closed
wants to merge 1 commit into from
Closed

PDF cleanup 282: rename sucᵉ to 1 +ᵉ_ #363

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions src/Ledger/Epoch.lagda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ its results, i.e:
certState' =
⟦ record dState { rewards = rewards ∪⁺ refunds }
, ⟦ pools ∣ retired ᶜ , retiring ∣ retired ᶜ ⟧ᵖ
, ⟦ if null govSt' then mapValues sucᵉ dreps else dreps
, ⟦ if null govSt' then mapValues (1 +ᵉ_) dreps else dreps
, ccHotKeys ∣ ccCreds (es .EnactState.cc) ⟧ᵛ ⟧ᶜˢ

utxoSt' = ⟦ utxo , 0 , deposits ∣ mapˢ (proj₁ ∘ proj₂) removedGovActions ᶜ , 0 ⟧ᵘ
Expand Down Expand Up @@ -131,13 +131,13 @@ data
\end{code}
\begin{code}
NEWEPOCH-New :
e ≡ sucᵉ lastEpoch
e ≡ 1 +ᵉ lastEpoch
→ Γ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
────────────────────────────────
Γ ⊢ ⟦ lastEpoch , eps ⟧ⁿᵉ ⇀⦇ e ,NEWEPOCH⦈ ⟦ e , eps' ⟧ⁿᵉ

NEWEPOCH-Not-New :
e ≢ sucᵉ lastEpoch
e ≢ 1 +ᵉ lastEpoch
────────────────────────────────
Γ ⊢ ⟦ lastEpoch , eps ⟧ⁿᵉ ⇀⦇ e ,NEWEPOCH⦈ ⟦ lastEpoch , eps ⟧ⁿᵉ
\end{code}
Expand Down
4 changes: 2 additions & 2 deletions src/Ledger/Epoch/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,12 +50,12 @@ module _ {Γ : NewEpochEnv} {nes : NewEpochState} {e : Epoch} where
open NewEpochState nes

NEWEPOCH-total : ∃[ nes' ] Γ ⊢ nes ⇀⦇ e ,NEWEPOCH⦈ nes'
NEWEPOCH-total with e ≟ sucᵉ lastEpoch
NEWEPOCH-total with e ≟ 1 +ᵉ lastEpoch
... | yes p = ⟦ e , proj₁ EPOCH-total' ⟧ⁿᵉ , NEWEPOCH-New p (EPOCH-total' .proj₂)
... | no ¬p = -, NEWEPOCH-Not-New ¬p

NEWEPOCH-complete : ∀ nes' → Γ ⊢ nes ⇀⦇ e ,NEWEPOCH⦈ nes' → proj₁ NEWEPOCH-total ≡ nes'
NEWEPOCH-complete nes' h with e ≟ sucᵉ lastEpoch | h
NEWEPOCH-complete nes' h with e ≟ 1 +ᵉ lastEpoch | h
... | yes p | NEWEPOCH-New x x₁ rewrite EPOCH-complete' _ x₁ = refl
... | yes p | NEWEPOCH-Not-New x = ⊥-elim $ x p
... | no ¬p | NEWEPOCH-New x x₁ = ⊥-elim $ ¬p x
Expand Down
6 changes: 3 additions & 3 deletions src/Ledger/PPUp.lagda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ data _⊢_⇀⦇_,PPUP⦈_ : PPUpdateEnv → PPUpdateState → Maybe Update →
PPUpdateCurrent : let open PPUpdateEnv Γ in
dom pup ⊆ dom genDelegs
→ All (isViableUpdate pparams) (range pup)
→ slot + (2 * StabilityWindow) < firstSlot (sucᵉ (epoch slot))
→ slot + (2 * StabilityWindow) < firstSlot (1 +ᵉ (epoch slot))
→ epoch slot ≡ e
────────────────────────────────
Γ ⊢ record { pup = pupˢ ; fpup = fpupˢ } ⇀⦇ just (pup , e) ,PPUP⦈
Expand All @@ -80,8 +80,8 @@ data _⊢_⇀⦇_,PPUP⦈_ : PPUpdateEnv → PPUpdateState → Maybe Update →
PPUpdateFuture : let open PPUpdateEnv Γ in
dom pup ⊆ dom genDelegs
→ All (isViableUpdate pparams) (range pup)
→ firstSlot (sucᵉ (epoch slot)) ≤ slot + (2 * StabilityWindow)
→ sucᵉ (epoch slot) ≡ e
→ firstSlot (1 +ᵉ (epoch slot)) ≤ slot + (2 * StabilityWindow)
→ 1 +ᵉ (epoch slot) ≡ e
────────────────────────────────
Γ ⊢ record { pup = pupˢ ; fpup = fpupˢ } ⇀⦇ just (pup , e) ,PPUP⦈
record { pup = pupˢ ; fpup = pup ∪ˡ fpupˢ }
Expand Down
8 changes: 5 additions & 3 deletions src/Ledger/PPUp/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,20 +13,22 @@ private
open import Agda.Builtin.FromNat
open import Algebra; open Semiring Slotʳ hiding (refl)
open import Algebra.Literals; open Semiring-Lit Slotʳ
import Data.Nat.Literals as ℕ
instance _ = ℕ.number

Current-Property : PPUpdateEnv → Update → Set
Current-Property Γ (pup , e) = let open PPUpdateEnv Γ in
dom pup ⊆ dom genDelegs
× All (isViableUpdate pparams) (range pup)
× (slot + (2 * StabilityWindow)) < firstSlot (sucᵉ (epoch slot))
× (slot + (2 * StabilityWindow)) < firstSlot (1 +ᵉ (epoch slot))
× epoch slot ≡ e

Future-Property : PPUpdateEnv → Update → Set
Future-Property Γ (pup , e) = let open PPUpdateEnv Γ in
dom pup ⊆ dom genDelegs
× All (isViableUpdate pparams) (range pup)
× firstSlot (sucᵉ (epoch slot)) ≤ (slot + (2 * StabilityWindow))
× sucᵉ (epoch slot) ≡ e
× firstSlot (1 +ᵉ (epoch slot)) ≤ (slot + (2 * StabilityWindow))
× 1 +ᵉ (epoch slot) ≡ e

instance
Computational-PPUP : Computational _⊢_⇀⦇_,PPUP⦈_ String
Expand Down
Loading