Merge branch 'dev' into feat/prooftra

Author: ypatil12

.github/workflows/certora-prover.yml

@@ -1,29 +1,64 @@
-name: Certora Prover Workflow
+name: Certora
 
 on:
-  push:
-    branches:
-      - dev
+  # Run when PRs from feat/* branches are merged into dev
   pull_request:
+    types: [closed]
     branches:
       - dev
+  
+  # Run on any pushes to certora/* branches
+  push:
+    branches:
+      - 'certora/**'
+  
+  # Biweekly schedule (1st and 15th of each month at midnight UTC)
+  schedule:
+    - cron: '0 0 1,15 * *'
+  
+  # Manual trigger
   workflow_dispatch:
 
 jobs:
+  # First job: Compile the contracts for Certora verification
   compile:
-    runs-on: ubuntu-latest
+    name: Compile
+    # Run if it meets one of these conditions:
+    # 1. It's a merged PR from a feat/* branch to dev
+    # 2. It's a push to a certora/* branch
+    # 3. It's a scheduled run
+    # 4. It's a manually triggered run
+    if: >
+      (github.event_name == 'pull_request' && 
+       github.event.pull_request.merged == true && 
+       startsWith(github.head_ref, 'feat/')) || 
+      (github.event_name == 'push' && 
+       startsWith(github.ref, 'refs/heads/certora/')) ||
+      github.event_name == 'schedule' || 
+      github.event_name == 'workflow_dispatch'
+    runs-on: protocol-x64-16core
     steps:
+      # Checkout the repository with submodules
       - uses: actions/checkout@v4
         with:
           submodules: recursive
+          # Use dev branch for scheduled runs, otherwise use the branch that triggered the workflow
+          ref: ${{ github.event_name == 'schedule' && 'dev' || github.ref }}
+
+      # Install the Foundry toolchain
       - name: Install Foundry
         uses: foundry-rs/foundry-toolchain@v1
         with:
           version: stable
+
+      # Install dependencies using Forge
       - name: Install forge dependencies
         run: forge install
+
+      # Run Certora compilation step only
       - uses: Certora/certora-run-action@v1
         with:
+          # List of configuration files for different contracts to verify
           configurations: |-
             certora/confs/core/AllocationManager.conf
             certora/confs/core/AllocationManagerSanity.conf
@@ -38,25 +73,48 @@ jobs:
           solc-remove-version-prefix: "0."
           job-name: "Eigenlayer Contracts"
           certora-key: ${{ secrets.CERTORAKEY }}
+          # Only compile, don't run verification yet
           compilation-steps-only: true
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
 
+  # Second job: Run the actual verification after compilation succeeds
   verify:
-    runs-on: ubuntu-latest
+    name: Verify
+    runs-on: protocol-x64-16core
+    # This job depends on the compile job
     needs: compile
+    # Same conditions as the compile job
+    if: >
+      (github.event_name == 'pull_request' && 
+       github.event.pull_request.merged == true && 
+       startsWith(github.head_ref, 'feat/')) || 
+      (github.event_name == 'push' && 
+       startsWith(github.ref, 'refs/heads/certora/')) ||
+      github.event_name == 'schedule' || 
+      github.event_name == 'workflow_dispatch'
     steps:
+      # Checkout the repository with submodules
       - uses: actions/checkout@v4
         with:
           submodules: recursive
+          # Use dev branch for scheduled runs, otherwise use the branch that triggered the workflow
+          ref: ${{ github.event_name == 'schedule' && 'dev' || github.ref }}
+          
+      # Install the Foundry toolchain.
       - name: Install Foundry
         uses: foundry-rs/foundry-toolchain@v1
         with:
-          version: nightly
+          version: stable
+
+      # Install dependencies using Forge
       - name: Install forge dependencies
         run: forge install
+
+      # Run Certora verification with the same configurations
       - uses: Certora/certora-run-action@v1
         with:
+          # List of configuration files for different contracts to verify
           configurations: |-
             certora/confs/core/AllocationManager.conf
             certora/confs/core/AllocationManagerSanity.conf

docs/core/AllocationManager.md

@@ -529,6 +529,13 @@ Given an `operator` and an `Allocation` from a `strategy` to an AVS's `OperatorS
 
 If ALL of these are true, the `AllocationManager` will allow the AVS to slash the `operator's` `Allocation`.
 
+#### Evaluating How Much of the Allocation is "Slashable"
+
+The `getMinimumSlashableStake` calculates the minimum amount of stake that will be slashable at a specified future block. This computation accounts for each operator’s allocated stake from different strategies within an operator set. The function considers pending allocation changes that could reduce the slashable stake over time, ensuring a minimum guaranteed value. Because this is a forecast, the slashable stake at any given moment is a discrete value, but when looking ahead to a future block, the function provides the lowest possible amount, factoring in any planned allocation adjustments that will take effect within the specified timeframe.
+
+Please see [IAllocationManager.sol:getMinimumSlashableStake](https://github.com/Layr-Labs/eigenlayer-contracts/blob/dev/src/contracts/interfaces/IAllocationManager.sol#L577) for more detail.
+
+
 #### `modifyAllocations`
 
 ```solidity

docs/core/RewardsCoordinator.md

@@ -26,6 +26,8 @@ The typical user flow is as follows:
 
 This entire flow will repeat periodically as AVSs submit rewards submissions, `DistributionRoots` are submitted, and Stakers/Operators claim their accumulated earnings. Note that `DistributionRoots` contain *cumulative earnings*, meaning Stakers/Operators aren't required to claim against every root - simply claiming against the most recent root will claim anything not yet claimed.
 
+**NOTE: Use caution when using reward tokens that do not strictly conform to ERC20 standards. Please DYOR if your token falls outside of ERC20 norms.** Specific things to look out for include (but are not limited to): exotic rebasing tokens, fee-on-transfer tokens, tokens that support reentrant behavior (like ERC-777), and other nonstandard ERC20 derivatives.
+
 #### High-level Concepts
 
 This document is organized according to the following themes (click each to be taken to the relevant section):
@@ -612,4 +614,4 @@ The rewards merkle tree is structured in the diagram below:
 
 Rewards are calculated via an off-chain data pipeline. The pipeline takes snapshots of core contract state at the `SNAPSHOT_CADENCE`, currently set to once per day. It then combines these snapshots with any active rewards to calculate what the single daily reward of an earner is. Every `CALCULATION_INTERVAL_SECONDS` rewards are accumulated up to `lastRewardsTimestamp + CALCULATION_INTERVAL_SECONDS` and posted on-chain by the entity with the `rewardsUpdater` role.
 
-`MAX_REWARDS_AMOUNT` is set to `1e38-1` given the precision bounds of the off-chain pipeline. An in-depth overview of the off-chain calculation can be found [here](https://hackmd.io/Fmjcckn1RoivWpPLRAPwBw)
+`MAX_REWARDS_AMOUNT` is set to `1e38-1` given the precision bounds of the off-chain pipeline. An in-depth overview of the off-chain calculation can be found [here](https://github.com/Layr-Labs/sidecar/blob/master/docs/docs/sidecar/rewards/calculation.md)