Merge remote-tracking branch 'origin/main' into javierdiaz72/make-stss-computable

Author: javierdiaz72

.github/workflows/ci.yml

@@ -142,18 +142,80 @@ jobs:
       if: matrix.test-set == 'all'
       run: cabal test all -j --test-show-details=streaming
 
-    - name: Test (NoThunks-safe tests only, part 1)
+    - name: Test (NoThunks-safe tests only)
       if: matrix.test-set == 'no-thunks-safe'
-      run: cabal test ouroboros-consensus:consensus-test ouroboros-consensus:doctest ouroboros-consensus:infra-test ouroboros-consensus:storage-test ouroboros-consensus-cardano:byron-test -j --test-show-details=streaming
+      run: cabal test ouroboros-consensus:consensus-test ouroboros-consensus:doctest ouroboros-consensus:infra-test ouroboros-consensus:storage-test ouroboros-consensus-cardano:byron-test ouroboros-consensus-cardano:shelley-test ouroboros-consensus-diffusion:infra-test ouroboros-consensus-protocol:protocol-test -j --test-show-details=streaming
 
-    - name: Test (NoThunks-safe tests only, part 2)
-      if: matrix.test-set == 'no-thunks-safe'
-      run: cabal test ouroboros-consensus-cardano:shelley-test ouroboros-consensus-diffusion:infra-test ouroboros-consensus-diffusion:mock-test ouroboros-consensus-protocol:protocol-test -j --test-show-details=streaming
+    - name: Identify benchmark executables
+      run: |
+        cp $(cabal list-bin mempool-bench) mempool-bench
+
+    - name: Upload benchmark executables
+      uses: actions/upload-artifact@v4
+      with:
+        name: benchmark-exes-${{ runner.os }}-${{ matrix.ghc }}
+        path: mempool-bench
+        retention-days: 10
+
+    # NB: build the haddocks at the end to avoid unecessary recompilations.
+    # We build the haddocks only for one GHC version.
+    - name: Build Haddock documentation
+      if: |
+        github.event_name == 'push'
+        && github.ref == 'refs/heads/main'
+        && matrix.ghc=='9.6.6'
+      run: |
+        # need for latex, dvisvgm and standalone
+        sudo apt install texlive-latex-extra texlive-latex-base
+        # cabal-docspec doesn't work with XDG https://github.com/phadej/cabal-extras/issues/136
+        sed -i 's_-- store-dir:_store-dir: /home/runner/.local/state/cabal/store_g' ~/.config/cabal/config
+        export CABAL_CONFIG=~/.config/cabal/config
+
+        ./scripts/docs/haddocks.sh
+        tar vzcf haddocks.tgz ./docs/website/static/haddocks
+
+    - name: Upload haddocks as an artifact
+      if: |
+        github.event_name == 'push'
+        && github.ref == 'refs/heads/main'
+        && matrix.ghc=='9.6.6'
+      uses: actions/upload-artifact@v4
+      with:
+        name: haddocks
+        path: haddocks.tgz
+        retention-days: 1
+
+  benchmarks:
+    name: Run benchmarks
+    needs: build-test-bench-haddocks
+
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        ghc: ["8.10.7", "9.6.6", "9.10.1"]
+
+    steps:
+    - uses: actions/checkout@v4
+
+    - name: Install base libraries
+      uses: input-output-hk/actions/base@latest
+      with:
+        use-sodium-vrf: false
+
+    - name: Download benchmark executables
+      uses: actions/download-artifact@v4
+      with:
+        name: benchmark-exes-${{ runner.os }}-${{ matrix.ghc }}
+
+    - name: Set permissions for benchmark executables
+      run: |
+        chmod u+x mempool-bench
 
     - name: Create baseline-benchmark
       if: github.event_name == 'push' && github.ref == 'refs/heads/main'
       run: |
-        cabal new-run ouroboros-consensus:mempool-bench -- \
+        ./mempool-bench \
         --timeout=60 --csv mempool-benchmarks.csv \
         +RTS -T
 
@@ -167,7 +229,6 @@ jobs:
     # then we will save the same results we just restored.
     - name: Cache benchmark baseline results
       uses: actions/cache@v4
-      if: matrix.variant == 'default'
       with:
         path: baseline-mempool-benchmarks.csv
         key:  baseline-mempool-benchmarks-${{ runner.os }}-${{ matrix.ghc }}-${{ github.run_id }}
@@ -192,7 +253,7 @@ jobs:
       if: ${{ github.event_name == 'pull_request' }}
       run: |
         if [ -f baseline-mempool-benchmarks.csv ]; then
-          cabal new-run ouroboros-consensus:mempool-bench -- \
+          ./mempool-bench \
           --timeout=60 --baseline baseline-mempool-benchmarks.csv \
           --fail-if-slower 100 \
           +RTS -T
@@ -201,34 +262,6 @@ jobs:
           echo "Benchmarks comparison skipped."
         fi
 
-    # NB: build the haddocks at the end to avoid unecessary recompilations.
-    # We build the haddocks only for one GHC version.
-    - name: Build Haddock documentation
-      if: |
-        github.event_name == 'push'
-        && github.ref == 'refs/heads/main'
-        && matrix.ghc=='9.6.6'
-      run: |
-        # need for latex, dvisvgm and standalone
-        sudo apt install texlive-latex-extra texlive-latex-base
-        # cabal-docspec doesn't work with XDG https://github.com/phadej/cabal-extras/issues/136
-        sed -i 's_-- store-dir:_store-dir: /home/runner/.local/state/cabal/store_g' ~/.config/cabal/config
-        export CABAL_CONFIG=~/.config/cabal/config
-
-        ./scripts/docs/haddocks.sh
-        tar vzcf haddocks.tgz ./docs/website/static/haddocks
-
-    - name: Upload haddocks as an artifact
-      if: |
-        github.event_name == 'push'
-        && github.ref == 'refs/heads/main'
-        && matrix.ghc=='9.6.6'
-      uses: actions/upload-artifact@v4
-      with:
-        name: haddocks
-        path: haddocks.tgz
-        retention-days: 1
-
   deploy-documentation:
     name: Deploy documentation to GitHub Pages
     if: github.event_name == 'push' && github.ref == 'refs/heads/main'
@@ -248,7 +281,7 @@ jobs:
           cache: yarn
           cache-dependency-path: './docs/website/yarn.lock'
 
-      - uses: cachix/install-nix-action@V27
+      - uses: cachix/install-nix-action@v29
         with:
           extra_nix_config: |
             accept-flake-config = true

.github/workflows/documentation.yml

@@ -33,7 +33,7 @@ jobs:
           cache: yarn
           cache-dependency-path: './docs/website/yarn.lock'
 
-      - uses: cachix/install-nix-action@V27
+      - uses: cachix/install-nix-action@v29
         with:
           extra_nix_config: |
             accept-flake-config = true

.stylish-haskell.yaml

@@ -424,7 +424,7 @@ steps:
       #   between actual import and closing bracket.
       #
       # Default: true
-      align: true
+      align: false
 
       # stylish-haskell can detect redundancy of some language pragmas. If this
       # is set to true, it will remove those redundant pragmas. Default: true.

CODEOWNERS

@@ -1,4 +1,4 @@
 # Ouroboros-Consensus
 
 # These owners will be the default owners for everything in the repository.
-* @nfrisby @jasagredo @amesgen @fraser-iohk @dnadales @RenateEilers
+* @nfrisby @jasagredo @amesgen @fraser-iohk @dnadales

CONTRIBUTING.md

@@ -370,8 +370,6 @@ The core contributors to consensus codebase are:
 
 -   [Damian Nadales](https://github.com/dnadales)
 
--   [Renate Eilers](https://github.com/RenateEilers)
-
 # Code of conduct
 
 See [Cardano engineering

SECURITY.md

@@ -1 +1,19 @@
+# Security Policy
+
+## Reporting a Vulnerability
+
+Please report (suspected) security vulnerabilities to [email protected]. You will receive a
+response from us within 48 hours. If the issue is confirmed, we will release a patch as soon
+as possible.
+
+Please provide a clear and concise description of the vulnerability, including:
+
+* the affected version(s) of OSC-documentation,
+* steps that can be followed to exercise the vulnerability,
+* any workarounds or mitigations
+
+If you have developed any code or utilities that can help demonstrate the suspected
+vulnerability, please mention them in your email but ***DO NOT*** attempt to include them as
+attachments as this may cause your Email to be blocked by spam filters.
+
 See the security file in the [Cardano engineering handbook](https://github.com/input-output-hk/cardano-engineering-handbook/blob/main/SECURITY.md).

cabal.project

@@ -14,9 +14,9 @@ repository cardano-haskell-packages
 -- update either of these.
 index-state:
   -- Bump this if you need newer packages from Hackage
-  , hackage.haskell.org 2024-07-23T00:03:37Z
+  , hackage.haskell.org 2024-08-26T10:41:44Z
   -- Bump this if you need newer packages from CHaP
-  , cardano-haskell-packages 2024-08-27T16:28:01Z
+  , cardano-haskell-packages 2024-09-03T00:18:11Z
 
 packages:
   ouroboros-consensus

docs/agda-spec/src/Data/Rational/Ext.agda

@@ -1,66 +1,66 @@
-{-# OPTIONS --safe #-}
-
-open import Agda.Primitive renaming (Set to Type)
-
-module Data.Rational.Ext where
-
-open import Function using (_∘_; _$_)
-open import Data.Rational
-open import Data.Rational.Properties
-open import Data.Product using (_×_; ∃-syntax)
-open import Data.Nat as ℕ using (ℕ)
-open import Data.Integer as ℤ using (ℤ; +_)
-open import Data.Integer.GCD using (gcd)
-import Data.Integer.Properties as ℤ
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl)
-open import Relation.Binary.PropositionalEquality using (cong; sym; module ≡-Reasoning)
-open import Relation.Nullary.Negation using (contradiction)
-
--- The interval (0, 1]
-PosUnitInterval : Type
-PosUnitInterval = ∃[ p ] Positive p × p ≤ 1ℚ
-
-record RationalExtStructure : Type where
-  field
-    exp : ℚ → ℚ
-    ln  : (p : ℚ) → ⦃ Positive p ⦄ → ℚ
-
-p≢1⇒1-p≢0 : ∀ {p : ℚ} → p ≢ 1ℚ → 1ℚ - p ≢ 0ℚ
-p≢1⇒1-p≢0 {p} p≢1 1-p≡0 = contradiction p≡1 p≢1
-  where
-    open ≡-Reasoning
-    p≡1 = sym $ begin
-      1ℚ             ≡⟨ sym $ +-identityʳ 1ℚ ⟩
-      1ℚ + 0ℚ        ≡⟨ cong (λ i → 1ℚ + i) (sym $ +-inverseˡ p) ⟩
-      1ℚ + (- p + p) ≡⟨ sym $ +-assoc 1ℚ (- p) p ⟩
-      (1ℚ - p) + p   ≡⟨ cong (_+ p) 1-p≡0 ⟩
-      0ℚ + p         ≡⟨ +-identityˡ p ⟩
-      p              ∎
-
-p≤1⇒1-p≥0 : ∀ {p : ℚ} → p ≤ 1ℚ → 1ℚ - p ≥ 0ℚ
-p≤1⇒1-p≥0 {p} p≤1 = +-monoʳ-≤ 1ℚ -p≥-1
-  where
-    -p≥-1 = neg-antimono-≤ p≤1
-
-drop-≢ : ∀ {p q : ℚ} → p ≢ q → ↥ p ℤ.* ↧ q ≢ ↥ q ℤ.* ↧ p
-drop-≢ p≢q = p≢q ∘ ≃⇒≡ ∘ *≡*
-
-≤∧≢⇒< : ∀ {p q : ℚ} → p ≤ q → p ≢ q → p < q
-≤∧≢⇒< p≤q p≢q = *<* $ ℤ.≤∧≢⇒< (drop-*≤* p≤q) (drop-≢ p≢q)
-
-p≡1⇒↥p≡↧p : ∀ {p : ℚ} → p ≡ 1ℚ → ↥ p ≡ ↧ p
-p≡1⇒↥p≡↧p {p} p≡1
-  rewrite sym (ℤ.*-identityʳ (↥ p))
-        | drop-*≡* (≡⇒≃ p≡1)
-        | ℤ.*-identityˡ (↧ p)
-        = refl 
-
-↥p<↧p⇒p≢1 : ∀ {p : ℚ} → ↥ p ℤ.< ↧ p → p ≢ 1ℚ
-↥p<↧p⇒p≢1 n<m n/m≡1 = (ℤ.<⇒≢ n<m) (p≡1⇒↥p≡↧p n/m≡1)
-
-n<m⇒↥[n/m]<↧[n/m] : ∀ {n m : ℕ} → ⦃ _ : ℕ.NonZero m ⦄ → n ℕ.< m → ↥ (+ n / m) ℤ.< ↧ (+ n / m)
-n<m⇒↥[n/m]<↧[n/m] {n} {m} n<m = ℤ.*-cancelʳ-<-nonNeg g $ begin-strict
-  (↥ (+ n / m)) ℤ.* g ≡⟨ ↥-/ (+ n) m ⟩
-  + n                 <⟨ ℤ.+<+ n<m ⟩
-  + m                 ≡⟨ sym (↧-/ (+ n) m) ⟩
-  ↧ (+ n / m) ℤ.* g   ∎ where open ℤ.≤-Reasoning; g = gcd (+ n) (+ m)
+{-# OPTIONS --safe #-}
+
+open import Agda.Primitive renaming (Set to Type)
+
+module Data.Rational.Ext where
+
+open import Function using (_∘_; _$_)
+open import Data.Rational
+open import Data.Rational.Properties
+open import Data.Product using (_×_; ∃-syntax)
+open import Data.Nat as ℕ using (ℕ)
+open import Data.Integer as ℤ using (ℤ; +_)
+open import Data.Integer.GCD using (gcd)
+import Data.Integer.Properties as ℤ
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl)
+open import Relation.Binary.PropositionalEquality using (cong; sym; module ≡-Reasoning)
+open import Relation.Nullary.Negation using (contradiction)
+
+-- The interval (0, 1]
+PosUnitInterval : Type
+PosUnitInterval = ∃[ p ] Positive p × p ≤ 1ℚ
+
+record RationalExtStructure : Type where
+  field
+    exp : ℚ → ℚ
+    ln  : (p : ℚ) → ⦃ Positive p ⦄ → ℚ
+
+p≢1⇒1-p≢0 : ∀ {p : ℚ} → p ≢ 1ℚ → 1ℚ - p ≢ 0ℚ
+p≢1⇒1-p≢0 {p} p≢1 1-p≡0 = contradiction p≡1 p≢1
+  where
+    open ≡-Reasoning
+    p≡1 = sym $ begin
+      1ℚ             ≡⟨ sym $ +-identityʳ 1ℚ ⟩
+      1ℚ + 0ℚ        ≡⟨ cong (λ i → 1ℚ + i) (sym $ +-inverseˡ p) ⟩
+      1ℚ + (- p + p) ≡⟨ sym $ +-assoc 1ℚ (- p) p ⟩
+      (1ℚ - p) + p   ≡⟨ cong (_+ p) 1-p≡0 ⟩
+      0ℚ + p         ≡⟨ +-identityˡ p ⟩
+      p              ∎
+
+p≤1⇒1-p≥0 : ∀ {p : ℚ} → p ≤ 1ℚ → 1ℚ - p ≥ 0ℚ
+p≤1⇒1-p≥0 {p} p≤1 = +-monoʳ-≤ 1ℚ -p≥-1
+  where
+    -p≥-1 = neg-antimono-≤ p≤1
+
+drop-≢ : ∀ {p q : ℚ} → p ≢ q → ↥ p ℤ.* ↧ q ≢ ↥ q ℤ.* ↧ p
+drop-≢ p≢q = p≢q ∘ ≃⇒≡ ∘ *≡*
+
+≤∧≢⇒< : ∀ {p q : ℚ} → p ≤ q → p ≢ q → p < q
+≤∧≢⇒< p≤q p≢q = *<* $ ℤ.≤∧≢⇒< (drop-*≤* p≤q) (drop-≢ p≢q)
+
+p≡1⇒↥p≡↧p : ∀ {p : ℚ} → p ≡ 1ℚ → ↥ p ≡ ↧ p
+p≡1⇒↥p≡↧p {p} p≡1
+  rewrite sym (ℤ.*-identityʳ (↥ p))
+        | drop-*≡* (≡⇒≃ p≡1)
+        | ℤ.*-identityˡ (↧ p)
+        = refl 
+
+↥p<↧p⇒p≢1 : ∀ {p : ℚ} → ↥ p ℤ.< ↧ p → p ≢ 1ℚ
+↥p<↧p⇒p≢1 n<m n/m≡1 = (ℤ.<⇒≢ n<m) (p≡1⇒↥p≡↧p n/m≡1)
+
+n<m⇒↥[n/m]<↧[n/m] : ∀ {n m : ℕ} → ⦃ _ : ℕ.NonZero m ⦄ → n ℕ.< m → ↥ (+ n / m) ℤ.< ↧ (+ n / m)
+n<m⇒↥[n/m]<↧[n/m] {n} {m} n<m = ℤ.*-cancelʳ-<-nonNeg g $ begin-strict
+  (↥ (+ n / m)) ℤ.* g ≡⟨ ↥-/ (+ n) m ⟩
+  + n                 <⟨ ℤ.+<+ n<m ⟩
+  + m                 ≡⟨ sym (↧-/ (+ n) m) ⟩
+  ↧ (+ n / m) ℤ.* g   ∎ where open ℤ.≤-Reasoning; g = gcd (+ n) (+ m)

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

@@ -26,10 +26,6 @@ instance
 
   open import Data.Rational using (ℚ)
   import Data.Rational.Properties as Rat hiding (_≟_)
-
-  ℚ-Dec-≤ = ⁇² Rat._≤?_
-  ℚ-Dec-< = ⁇² Rat._<?_
-
   ℚ-hasPreorder = hasPreorderFromNonStrict Rat.≤-isPreorder _≟_
   ℚ-hasPartialOrder = HasPartialOrder ∋ record { ≤-antisym = Rat.≤-antisym }
   ℚ-hasDecPartialOrder = HasDecPartialOrder {A = ℚ} ∋ record {}