Disabling maxTerm check

IntersectMBO · Aug 27, 2024 · 00650b8 · 00650b8
1 parent 993b50b
commit 00650b8
Show file tree

Hide file tree

Showing 4 changed files with 53 additions and 40 deletions.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -44,6 +44,36 @@ jobs:
           nix-build -A formalLedger -j1 -o outputs/formalLedger
           rsync -r --include={'**/*.time'} outputs/formalLedger*/* docs/
 
+      - name: Configure git
+        run: |
+          git config user.name 'github-actions[bot]'
+          git config user.email 'github-actions[bot]@users.noreply.github.com'
+
+      - name: Add files
+        if: github.ref == 'refs/heads/master'
+        run: |
+            git add -f docs/
+            git commit -m "Updated for ${{ github.sha }}"
+
+      - name: Commit generated code at ${{ env.MAlonzo_branch }}
+        if: github.ref != 'refs/heads/master'
+        run: |
+            nix-build -A ledger.hsSrc -j1 -o outputs/MAlonzo
+            git stash push
+            git fetch origin ${{ env.MAlonzo_branch }} --depth 1
+            git checkout ${{ env.MAlonzo_branch }}
+            rsync -r --exclude={'**/nix-support','**/lib'} outputs/MAlonzo/haskell/Ledger/* generated/
+            git add -f generated && git commit -m "Generate code for ${{ github.sha }}" || echo "Everything is up-to-date."
+
+      - name: Push ${{ env.MAlonzo_branch }}
+        if: github.ref != 'refs/heads/master'
+        uses: ad-m/[email protected]
+        with:
+            github_token: ${{ secrets.GITHUB_TOKEN }}
+            branch: ${{ env.MAlonzo_branch }}
+            force: false
+            directory: .
+
       - name: Build ledger
         id: ledger
         run: |
@@ -78,17 +108,6 @@ jobs:
           echo "** Generated Haskell files:"; find -L docs/ -name '*.hs'
           OUT_DIR=../docs/ make staticWebsite
 
-      - name: Configure git
-        run: |
-          git config user.name 'github-actions[bot]'
-          git config user.email 'github-actions[bot]@users.noreply.github.com'
-
-      - name: Add files
-        if: github.ref == 'refs/heads/master'
-        run: |
-            git add -f docs/
-            git commit -m "Updated for ${{ github.sha }}"
-
       - name: Push to gh-pages
         if: github.ref == 'refs/heads/master'
         uses: ad-m/[email protected]
@@ -97,22 +116,3 @@ jobs:
             branch: gh-pages
             force: true
             directory: .
-
-      - name: Commit generated code at ${{ env.MAlonzo_branch }}
-        if: github.ref != 'refs/heads/master'
-        run: |
-            nix-build -A ledger.hsSrc -j1 -o outputs/MAlonzo
-            git stash push
-            git fetch origin ${{ env.MAlonzo_branch }} --depth 1
-            git checkout ${{ env.MAlonzo_branch }}
-            rsync -r --exclude={'**/nix-support','**/lib'} outputs/MAlonzo/haskell/Ledger/* generated/
-            git add -f generated && git commit -m "Generate code for ${{ github.sha }}" || echo "Everything is up-to-date."
-
-      - name: Push ${{ env.MAlonzo_branch }}
-        if: github.ref != 'refs/heads/master'
-        uses: ad-m/[email protected]
-        with:
-            github_token: ${{ secrets.GITHUB_TOKEN }}
-            branch: ${{ env.MAlonzo_branch }}
-            force: false
-            directory: .
diff --git a/src/Ledger/Enact.lagda b/src/Ledger/Enact.lagda
@@ -136,14 +136,13 @@ data _⊢_⇀⦇_,ENACT⦈_ where
     ───────────────────────────────────────
     ⟦ gid , t , e ⟧ᵉ ⊢ s ⇀⦇ NoConfidence ,ENACT⦈ record s { cc = nothing , gid }
 
-  Enact-NewComm : let -- old      = maybe proj₁ ∅ (s .cc .proj₁)
+  Enact-NewComm : let old      = maybe proj₁ ∅ (s .cc .proj₁)
                       maxTerm  = s .pparams .proj₁ .ccMaxTermLength +ᵉ e
                   in
     ∀[ term ∈ range new ] term ≤ maxTerm
     ───────────────────────────────────────
     ⟦ gid , t , e ⟧ᵉ ⊢ s ⇀⦇ UpdateCommittee new rem q ,ENACT⦈
-      s
-      -- record s { cc = just ((new ∪ˡ old) ∣ rem ᶜ , q) , gid }
+      record s { cc = just ((new ∪ˡ old) ∣ rem ᶜ , q) , gid }
 
   Enact-NewConst :
     ───────────────────────────────────────

diff --git a/src/Ledger/GovernanceActions/Properties.agda b/src/Ledger/GovernanceActions/Properties.agda
@@ -22,8 +22,9 @@ instance
     NoConfidence             → success (_ , Enact-NoConf)
     (UpdateCommittee new rem q) →
       case ¿ ∀[ term ∈ range new ]
-               term ≤ s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e ¿ of λ where
-      (yes p) → success (-, Enact-NewComm p)
+               term ≤ s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ' e ¿ of λ where
+      (yes p) → success (-, Enact-NewComm
+        (subst (λ x → ∀[ term ∈ range new ] term ≤ x) (sym +ᵉ≡+ᵉ') p))
       (no ¬p) → failure "ENACT failed at ∀[ term ∈ range new ] term ≤ (s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e)"
     (NewConstitution dh sh)  → success (-, Enact-NewConst)
     (TriggerHF v)            → success (-, Enact-HF)
@@ -39,7 +40,8 @@ instance
   ... | .UpdateCommittee new rem q | Enact-NewComm p
     rewrite dec-yes
       (¿ ∀[ term ∈ range new ] term
-           ≤ s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e ¿) p .proj₂
+           ≤ s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ' e ¿)
+      (subst (λ x → ∀[ term ∈ range new ] term ≤ x) +ᵉ≡+ᵉ' p) .proj₂
       = refl
   ... | .NewConstitution dh sh  | Enact-NewConst = refl
   ... | .TriggerHF v            | Enact-HF       = refl

diff --git a/src/Ledger/Types/Epoch.agda b/src/Ledger/Types/Epoch.agda
@@ -9,6 +9,10 @@ open import Algebra using (Semiring)
 open import Relation.Binary
 open import Data.Nat.Properties using (+-*-semiring)
 
+additionVia : ∀{A : Set} → (A → A) → ℕ → A → A
+additionVia sucFun zero r = r
+additionVia sucFun (suc l) r = sucFun (additionVia sucFun l r)
+
 record EpochStructure : Type₁ where
   field Slotʳ : Semiring 0ℓ 0ℓ
         Epoch : Type; ⦃ DecEq-Epoch ⦄ : DecEq Epoch; ⦃ Show-Epoch ⦄ : Show Epoch
@@ -23,6 +27,12 @@ record EpochStructure : Type₁ where
         StabilityWindow : Slot
         sucᵉ            : Epoch → Epoch
 
+  _+ᵉ_ = additionVia sucᵉ
+
+  field
+        _+ᵉ'_           : ℕ → Epoch → Epoch
+        +ᵉ≡+ᵉ'          : ∀ {a b} → a +ᵉ b ≡ a +ᵉ' b
+
   -- preorders and partial orders
 
   instance
@@ -48,10 +58,6 @@ record EpochStructure : Type₁ where
   ℕtoEpoch zero    = epoch 0#
   ℕtoEpoch (suc n) = sucᵉ (ℕtoEpoch n)
 
-  _+ᵉ_ : ℕ → Epoch → Epoch
-  zero  +ᵉ e = e
-  suc n +ᵉ e = sucᵉ (n +ᵉ e)
-
   instance
     addSlot : HasAdd Slot
     addSlot ._+_ = _+ˢ_
@@ -70,6 +76,10 @@ record GlobalConstants : Type₁ where
          Quorum : ℕ
          NetworkId : Network
 
+  ℕ+ᵉ≡+ᵉ' : ∀ {a b} → additionVia suc a b ≡ a + b
+  ℕ+ᵉ≡+ᵉ' {zero} {b} = refl
+  ℕ+ᵉ≡+ᵉ' {suc a} {b} = cong suc (ℕ+ᵉ≡+ᵉ' {a} {b})
+
   ℕEpochStructure : EpochStructure
   ℕEpochStructure = λ where
     .Slotʳ           → +-*-semiring
@@ -78,6 +88,8 @@ record GlobalConstants : Type₁ where
     .firstSlot e     → e * SlotsPerEpochᶜ
     .StabilityWindow → StabilityWindowᶜ
     .sucᵉ            → suc
+    ._+ᵉ'_           → _+_
+    .+ᵉ≡+ᵉ' {a} {b}  → ℕ+ᵉ≡+ᵉ' {a} {b}
 
    where open EpochStructure