liquid-collective · iamsahu · Feb 5, 2026 · Feb 5, 2026 · Feb 5, 2026 · Feb 5, 2026
@@ -42,6 +42,12 @@ jobs:
       - name: Install certora
         run: pip3 install certora-cli
 
+      - name: Set up JDK
+        uses: actions/setup-java@v4
+        with:
+          distribution: 'temurin'
+          java-version: '21'
+
       - name: Install solc
         run: |
           pip install solc-select

diff --git a/certora/conf/RedeemManagerV1.conf b/certora/conf/RedeemManagerV1.conf
@@ -16,7 +16,7 @@
   "loop_iter": "2",
   "optimistic_loop": true,
   "packages": ["openzeppelin-contracts=lib/openzeppelin-contracts"],
-  "solc": "solc8.20",
+  "solc": "solc8.33",
   "prover_args": [
     " -contractRecursionLimit 1", // River.resolveRedeemRequests(uint32[]) calls RedeemManager.resolveRedeemRequests(uint32[]) 
     " -recursionErrorAsAssert false", //RedeemManager._claimRedeemRequest() is recursive 

diff --git a/certora/conf/RiverV1.conf b/certora/conf/RiverV1.conf
@@ -4,7 +4,7 @@
     "contracts/src/Allowlist.1.sol:AllowlistV1",
     "contracts/src/CoverageFund.1.sol:CoverageFundV1",
     "contracts/src/ELFeeRecipient.1.sol:ELFeeRecipientV1",
-    "contracts/src/OperatorsRegistry.1.sol:OperatorsRegistryV1",
+    "certora/harness/OperatorsRegistryV1Harness.sol:OperatorsRegistryV1Harness",
     "certora/harness/RedeemManagerV1Harness.sol",
     "contracts/src/Withdraw.1.sol:WithdrawV1",
     "contracts/src/mock/DepositContractMock.sol", // This is needed only when working with the Ethereum network outside.

diff --git a/certora/conf/SharesManagerV1.conf b/certora/conf/SharesManagerV1.conf
@@ -4,7 +4,7 @@
     "contracts/src/Allowlist.1.sol:AllowlistV1",
     "contracts/src/CoverageFund.1.sol:CoverageFundV1",
     "contracts/src/ELFeeRecipient.1.sol:ELFeeRecipientV1",
-    "contracts/src/OperatorsRegistry.1.sol:OperatorsRegistryV1",
+    "certora/harness/OperatorsRegistryV1Harness.sol:OperatorsRegistryV1Harness",
     "certora/harness/RedeemManagerV1Harness.sol",
     "contracts/src/Withdraw.1.sol:WithdrawV1",
     "contracts/src/mock/DepositContractMock.sol", // This is needed only when working with the Ethereum network outside.

diff --git a/certora/harness/OperatorsRegistryV1Harness.sol b/certora/harness/OperatorsRegistryV1Harness.sol
@@ -14,10 +14,6 @@ contract OperatorsRegistryV1Harness is OperatorsRegistryV1 {
         return OperatorsV2.getCount();
     }
 
-    function getMaxValidatorAttributionPerRound() external view returns (uint256) {
-        return MAX_VALIDATOR_ATTRIBUTION_PER_ROUND;
-    }
-
     function getStoppedValidatorsLength() external view returns (uint256) {
         return OperatorsV2.getStoppedValidators().length;
     }
@@ -42,7 +38,7 @@ contract OperatorsRegistryV1Harness is OperatorsRegistryV1 {
         OperatorsV2.Operator memory op = OperatorsV2.get(opIndex);
         uint256 valIndex = 0;
         bytes32 validatorDataHash = keccak256(abi.encodePacked(publicKeyAndSignature));
-        for (; valIndex < op.keys;) 
+        for (; valIndex < op.keys; ++valIndex) 
         {
             (bytes memory valData) = ValidatorKeys.getRaw(opIndex, valIndex);
             if (validatorDataHash == keccak256(abi.encodePacked(valData)))  //element found

diff --git a/certora/specs/Base.spec b/certora/specs/Base.spec
@@ -66,7 +66,7 @@ methods {
     function RiverV1Harness.getCLValidatorCount() external returns(uint256) envfree;
 
     // RiverV1 : ConsensusLayerDepositManagerV1
-    function _.depositToConsensusLayerWithDepositRoot(uint256, bytes32) external => DISPATCHER(true);
+    function _.depositToConsensusLayerWithDepositRoot(IOperatorsRegistryV1.OperatorAllocation[], bytes32) external => DISPATCHER(true);
     function RiverV1Harness.getDepositedValidatorCount() external returns(uint256) envfree;
 
     // WithdrawV1
@@ -83,7 +83,7 @@ methods {
     function OR.getStoppedAndRequestedExitCounts() external returns (uint32, uint256) envfree;
     function _.getStoppedAndRequestedExitCounts() external => DISPATCHER(true);
     function _.demandValidatorExits(uint256, uint256) external => DISPATCHER(true);
-    function _.pickNextValidatorsToDeposit(uint256) external => DISPATCHER(true); // has no effect - CERT-4615
+    function _.pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[]) external => DISPATCHER(true); // has no effect - CERT-4615
 
     //function _.deposit(bytes,bytes,bytes,bytes32) external => DISPATCHER(true); // has no effect - CERT-4615
 

@@ -129,7 +129,7 @@ invariant inactiveOperatorsRemainNotFunded_LI2(uint opIndex)
         } 
     { 
         preserved requestValidatorExits(uint256 x) with(env e) { require x <= 2; }
-        preserved pickNextValidatorsToDeposit(uint256 x) with(env e) { require x <= 1; }  
+        preserved pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[] x) with(env e) { require x.length <= 1; }  
         preserved removeValidators(uint256 _index, uint256[] _indexes) with(env e) { require _indexes.length <= 1; }  
     }
 
@@ -216,7 +216,7 @@ invariant operatorsStatesRemainValid_LI2_easyMethods(uint opIndex)
     filtered { f -> !ignoredMethod(f) && 
     !needsLoopIter4(f) &&
     f.selector != sig:requestValidatorExits(uint256).selector &&
-    f.selector != sig:pickNextValidatorsToDeposit(uint256).selector &&
+    f.selector != sig:pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[]).selector &&
     f.selector != sig:removeValidators(uint256,uint256[]).selector
     }
 
@@ -225,7 +225,7 @@ invariant operatorsStatesRemainValid_LI2_easyMethods(uint opIndex)
 invariant operatorsStatesRemainValid_LI2_pickNextValidatorsToDeposit(uint opIndex) 
     isValidState() => (operatorStateIsValid(opIndex))
     filtered { f -> !ignoredMethod(f) && 
-    !needsLoopIter4(f) && f.selector != sig:pickNextValidatorsToDeposit(uint256).selector
+    !needsLoopIter4(f) && f.selector != sig:pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[]).selector
     }
 
 // proves the invariant for reportStoppedValidatorCounts

@@ -9,7 +9,7 @@ methods {
     function OR.getStoppedAndRequestedExitCounts() external returns (uint32, uint256) envfree;
     function _.getStoppedAndRequestedExitCounts() external => DISPATCHER(true);
     function _.demandValidatorExits(uint256, uint256) external => DISPATCHER(true);
-    //function _.pickNextValidatorsToDeposit(uint256) external => DISPATCHER(true); // has no effect - CERT-4615
+    //function _.pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[]) external => DISPATCHER(true); // has no effect - CERT-4615
 
     //function _.deposit(bytes,bytes,bytes,bytes32) external => DISPATCHER(true); // has no effect - CERT-4615 
 
@@ -30,7 +30,7 @@ methods {
     function OR.getActiveOperatorsCount() external returns (uint256) envfree;
     function OR.getOperatorsSaturationDiscrepancy() external returns (uint256) envfree;
     function OR.getKeysCount(uint256) external returns (uint256) envfree;
-    function OR.pickNextValidatorsToDeposit(uint256) external returns (bytes[] memory, bytes[] memory);
+    function OR.pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[]) external returns (bytes[] memory, bytes[] memory);
     function OR.requestValidatorExits(uint256) external;
     function OR.setOperatorAddress(uint256, address) external;   
     function OR.getOperatorsSaturationDiscrepancy(uint256, uint256) external returns (uint256) envfree;
@@ -88,7 +88,7 @@ definition isMethodID(method f, uint ID) returns bool =
     (f.selector == sig:addOperator(string,address).selector && ID == 4) ||
     (f.selector == sig:demandValidatorExits(uint256,uint256).selector && ID == 5) ||
     (f.selector == sig:initOperatorsRegistryV1(address,address).selector && ID == 6) ||
-    (f.selector == sig:pickNextValidatorsToDeposit(uint256).selector && ID == 7) ||
+    (f.selector == sig:pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[]).selector && ID == 7) ||
     (f.selector == sig:proposeAdmin(address).selector && ID == 8) ||
     (f.selector == sig:removeValidators(uint256,uint256[]).selector && ID == 9) ||
     (f.selector == sig:requestValidatorExits(uint256).selector && ID == 10) ||

@@ -49,7 +49,7 @@ invariant inactiveOperatorsRemainNotFunded(uint opIndex)
         (!getOperator(opIndex).active => getOperator(opIndex).funded == 0)
     { 
         preserved requestValidatorExits(uint256 x) with(env e) { require x <= 2; }
-        preserved pickNextValidatorsToDeposit(uint256 x) with(env e) { require x <= 1; }  
+        preserved pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[] x) with(env e) { require x.length <= 1; }  
         preserved removeValidators(uint256 _index, uint256[] _indexes) with(env e) { require _indexes.length <= 1; }  
     }
 
@@ -68,7 +68,7 @@ invariant inactiveOperatorsRemainNotFunded_LI2(uint opIndex)
         } 
     { 
         preserved requestValidatorExits(uint256 x) with(env e) { require x <= 2; }
-        preserved pickNextValidatorsToDeposit(uint256 x) with(env e) { require x <= 1; }  
+        preserved pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[] x) with(env e) { require x.length <= 1; }  
         preserved removeValidators(uint256 _index, uint256[] _indexes) with(env e) { require _indexes.length <= 1; }  
     }
 
@@ -181,7 +181,7 @@ invariant operatorsStatesRemainValid_LI2_easyMethods(uint opIndex)
     filtered { f -> !ignoredMethod(f) && 
     !needsLoopIter4(f) &&
     f.selector != sig:requestValidatorExits(uint256).selector &&
-    f.selector != sig:pickNextValidatorsToDeposit(uint256).selector &&
+    f.selector != sig:pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[]).selector &&
     f.selector != sig:removeValidators(uint256,uint256[]).selector
     }
 
@@ -190,7 +190,7 @@ invariant operatorsStatesRemainValid_LI2_easyMethods(uint opIndex)
 invariant operatorsStatesRemainValid_LI2_pickNextValidatorsToDeposit(uint opIndex) 
     isValidState() => (operatorStateIsValid(opIndex))
     filtered { f -> !ignoredMethod(f) && 
-    !needsLoopIter4(f) && f.selector != sig:pickNextValidatorsToDeposit(uint256).selector
+    !needsLoopIter4(f) && f.selector != sig:pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[]).selector
     }
 
 // proves the invariant for reportStoppedValidatorCounts

@@ -38,7 +38,7 @@ invariant validatorKeysRemainUnique_LI2(
     filtered { f -> !ignoredMethod(f) && !needsLoopIter4(f) }
     { 
         preserved requestValidatorExits(uint256 x) with(env e) { require x <= 2; }
-        preserved pickNextValidatorsToDeposit(uint256 x) with(env e) { require x <= 2; }  
+        preserved pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[] x) with(env e) { require x.length <= 2; }  
         preserved removeValidators(uint256 _index, uint256[] _indexes) with(env e) { require _indexes.length <= 2; }  
     }
 
@@ -73,9 +73,9 @@ rule startingValidatorsDecreasesDiscrepancy(env e)
     require getKeysCount(index1) < 5; 
     require getKeysCount(index2) < 5;  //counterexamples when the keys count overflows
 
-    uint count;
-    require count > 0 && count <= 3;
-    pickNextValidatorsToDeposit(e, count);
+    IOperatorsRegistryV1.OperatorAllocation[] allocations;
+    require allocations.length > 0 && allocations.length <= 3;
+    pickNextValidatorsToDeposit(e, allocations);
     uint discrepancyAfter = getOperatorsSaturationDiscrepancy(index1, index2);
 
     //uint256 keysAfter1; uint256 limitAfter1; uint256 fundedAfter1; uint256 requestedExitsAfter1; uint256 stoppedCountAfter1; bool activeAfter1; address operatorAfter1;
@@ -84,7 +84,7 @@ rule startingValidatorsDecreasesDiscrepancy(env e)
     //keysAfter2, limitAfter2, fundedAfter2, requestedExitsAfter2, stoppedCountAfter2, activeAfter2, operatorAfter2 = getOperatorState(e, index2);
 
     assert discrepancyBefore > 0 => to_mathint(discrepancyBefore) >= 
-        discrepancyAfter - count + 1; //getMaxValidatorAttributionPerRound(e);
+        discrepancyAfter - allocations.length + 1;
 }
 
 rule startingValidatorsNeverUsesSameValidatorTwice(env e) 
@@ -129,9 +129,9 @@ rule witness4_3StartingValidatorsDecreasesDiscrepancy(env e)
     require operatorStateIsValid(index2);
 
     uint discrepancyBefore = getOperatorsSaturationDiscrepancy(index1, index2);
-    uint count;
-    require count <= 1;
-    pickNextValidatorsToDeposit(e, count);
+    IOperatorsRegistryV1.OperatorAllocation[] allocations;
+    require allocations.length <= 1;
+    pickNextValidatorsToDeposit(e, allocations);
     uint discrepancyAfter = getOperatorsSaturationDiscrepancy(index1, index2);
     satisfy discrepancyBefore == 4 && discrepancyAfter == 3;
 }

diff --git a/certora/specs/SharesManagerV1.spec b/certora/specs/SharesManagerV1.spec
@@ -195,7 +195,7 @@ rule sharesBalanceChangesRestrictively(method f) filtered {
 rule pricePerShareChangesRespectively(method f) filtered {
     f -> !f.isView
         && f.selector != sig:initRiverV1_1(address,uint64,uint64,uint64,uint64,uint64,uint256,uint256,uint128,uint128).selector
-        && f.selector != sig:depositToConsensusLayerWithDepositRoot(uint256, bytes32).selector
+        && f.selector != sig:depositToConsensusLayerWithDepositRoot(IOperatorsRegistryV1.OperatorAllocation[], bytes32).selector
         && f.selector != sig:claimRedeemRequests(uint32[],uint32[]).selector
         && f.selector != sig:deposit().selector
         && f.selector != sig:depositAndTransfer(address).selector

@@ -21,13 +21,13 @@ rule startingValidatorsDecreasesDiscrepancy(env e)
     require getKeysCount(index1) < 5; 
     require getKeysCount(index2) < 5;
 
-    uint count;
-    require count > 0 && count <= 3;
-    pickNextValidatorsToDeposit(e, count);
+    IOperatorsRegistryV1.OperatorAllocation[] allocations;
+    require allocations.length > 0 && allocations.length <= 3;
+    pickNextValidatorsToDeposit(e, allocations);
     uint discrepancyAfter = getOperatorsSaturationDiscrepancy(index1, index2);
 
     assert discrepancyBefore > 0 => to_mathint(discrepancyBefore) >= 
-        discrepancyAfter - count + 1; // this conditions is fine as long as count <= MAX_VALIDATOR_ATTRIBUTION_PER_ROUND
+        discrepancyAfter - allocations.length + 1;
 }
 
 rule witness4_3StartingValidatorsDecreasesDiscrepancy(env e) 
@@ -38,9 +38,9 @@ rule witness4_3StartingValidatorsDecreasesDiscrepancy(env e)
     require operatorStateIsValid(index2);
 
     uint discrepancyBefore = getOperatorsSaturationDiscrepancy(index1, index2);
-    uint count;
-    require count <= 1;
-    pickNextValidatorsToDeposit(e, count);
+    IOperatorsRegistryV1.OperatorAllocation[] allocations;
+    require allocations.length <= 1;
+    pickNextValidatorsToDeposit(e, allocations);
     uint discrepancyAfter = getOperatorsSaturationDiscrepancy(index1, index2);
     satisfy discrepancyBefore == 4 && discrepancyAfter == 3;
 }
@@ -119,7 +119,7 @@ invariant inactiveOperatorsRemainNotFunded_LI2(uint opIndex)
         } 
     { 
         preserved requestValidatorExits(uint256 x) with(env e) { require x <= 2; }
-        preserved pickNextValidatorsToDeposit(uint256 x) with(env e) { require x <= 1; }  
+        preserved pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[] x) with(env e) { require x.length <= 1; }  
         preserved removeValidators(uint256 _index, uint256[] _indexes) with(env e) { require _indexes.length <= 1; }  
     }
 
@@ -178,7 +178,7 @@ invariant operatorsStatesRemainValid_LI2_easyMethods(uint opIndex)
     filtered { f -> !ignoredMethod(f) && 
     !needsLoopIter4(f) &&
     f.selector != sig:requestValidatorExits(uint256).selector &&
-    f.selector != sig:pickNextValidatorsToDeposit(uint256).selector &&
+    f.selector != sig:pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[]).selector &&
     f.selector != sig:removeValidators(uint256,uint256[]).selector
     }
 
@@ -187,7 +187,7 @@ invariant operatorsStatesRemainValid_LI2_easyMethods(uint opIndex)
 invariant operatorsStatesRemainValid_LI2_pickNextValidatorsToDeposit(uint opIndex) 
     isValidState() => (operatorStateIsValid(opIndex))
     filtered { f -> !ignoredMethod(f) && 
-    !needsLoopIter4(f) && f.selector != sig:pickNextValidatorsToDeposit(uint256).selector
+    !needsLoopIter4(f) && f.selector != sig:pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[]).selector
     }
 
 // proves the invariant for reportStoppedValidatorCounts
@@ -392,7 +392,7 @@ invariant validatorKeysRemainUnique_LI2(
     filtered { f -> !ignoredMethod(f) && !needsLoopIter4(f) }
     { 
         preserved requestValidatorExits(uint256 x) with(env e) { require x <= 2; }
-        preserved pickNextValidatorsToDeposit(uint256 x) with(env e) { require x <= 2; }  
+        preserved pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[] x) with(env e) { require x.length <= 2; }  
         preserved removeValidators(uint256 _index, uint256[] _indexes) with(env e) { require _indexes.length <= 2; }  
     }
 
@@ -784,7 +784,7 @@ invariant inactiveOperatorsRemainNotFunded(uint opIndex)
         (!getOperator(opIndex).active => getOperator(opIndex).funded == 0)
     { 
         preserved requestValidatorExits(uint256 x) with(env e) { require x <= 2; }
-        preserved pickNextValidatorsToDeposit(uint256 x) with(env e) { require x <= 1; }  
+        preserved pickNextValidatorsToDeposit(IOperatorsRegistryV1.OperatorAllocation[] x) with(env e) { require x.length <= 1; }  
         preserved removeValidators(uint256 _index, uint256[] _indexes) with(env e) { require _indexes.length <= 1; }  
     }
 

diff --git a/certora/specs_for_CI/River_base.spec b/certora/specs_for_CI/River_base.spec
@@ -14,4 +14,4 @@ definition ignoredMethod(method f) returns bool =
     f.selector == sig:helper11_commitBalanceToDeposit(OracleManagerV1.ConsensusLayerDataReportingVariables).selector;
 
 definition excludedInCI(method f) returns bool =
-    f.selector == sig:depositToConsensusLayerWithDepositRoot(uint256, bytes32).selector;
+    f.selector == sig:depositToConsensusLayerWithDepositRoot(IOperatorsRegistryV1.OperatorAllocation[], bytes32).selector;