From d2160f8b5da1d8cae902fe6171af0bd43014163c Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Tue, 30 Jul 2024 19:18:54 +0200
Subject: [PATCH] simplification correction

---
 test/kontrol/ActivateNextState.t.sol |  2 --
 test/kontrol/lido-lemmas.k           | 12 +++++++++++-
 2 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/test/kontrol/ActivateNextState.t.sol b/test/kontrol/ActivateNextState.t.sol
index 26b450f4..2f56d09c 100644
--- a/test/kontrol/ActivateNextState.t.sol
+++ b/test/kontrol/ActivateNextState.t.sol
@@ -39,12 +39,10 @@ contract ActivateNextStateTest is DualGovernanceSetUp {
 
     function testActivateNextStateCorrectEscrows() external {
         State preState = dualGovernance.getCurrentState();
-        vm.assume(preState != State.RageQuit);
 
         dualGovernance.activateNextState();
 
         State postState = dualGovernance.getCurrentState();
-        vm.assume(postState == State.RageQuit);
 
         Escrow newSignallingEscrow = Escrow(payable(dualGovernance.getVetoSignallingEscrow()));
         Escrow newRageQuitEscrow = Escrow(payable(dualGovernance.getRageQuitEscrow()));
diff --git a/test/kontrol/lido-lemmas.k b/test/kontrol/lido-lemmas.k
index 06290efa..a52e9066 100644
--- a/test/kontrol/lido-lemmas.k
+++ b/test/kontrol/lido-lemmas.k
@@ -352,7 +352,7 @@ module LIDO-LEMMAS
        [simplification, concrete(W, SHIFT), preserves-definedness]
 
     rule [buf-bor-split]:
-      #buf ( N, X |Int Y ) => #buf ( N -Int #getFirstOneBit(X) /Int 8, X /Int ( 2 ^Int ( #getFirstOneBit(X) /Int 8 ) ) ) +Bytes
+      #buf ( N, X |Int Y ) => #buf ( N -Int #getFirstOneBit(X) /Int 8, X /Int ( 2 ^Int ( 8 *Int ( #getFirstOneBit(X) /Int 8 ) ) ) ) +Bytes
                               #buf ( #getFirstOneBit(X) /Int 8, Y )
       requires 0 <=Int N andBool N <=Int 32 andBool 0 <=Int #getFirstOneBit(X)
        andBool 0 <=Int Y andBool Y <Int 2 ^Int ( 8 *Int ( #getFirstOneBit(X) /Int 8 ) )
@@ -536,4 +536,14 @@ module LIDO-LEMMAS-SPEC
           ) ... </k>
           requires 0 <=Int WORD7 andBool WORD7 <Int 256
 
+    claim [slot-update-09]:
+      <k> runLemma (
+            ( 481644099385675654177479669474857658256926169505224677670350078624137216 |Int ( 115790322390251417039241401711187164934754157181743689629425282016341011726335 &Int #asWord ( #buf ( 2 , WORD7:Int ) +Bytes b"\xa4\xadOh\xd0\xb9\x1c\xfd\x19h|\x88\x1eP\xf3\xa0\x02B\x82\x8c" +Bytes #buf ( 5 , WORD6:Int ) +Bytes #buf ( 5 , WORD5:Int ) ) ) )
+          ) => doneLemma (
+            #asWord ( #buf ( 2 , WORD7:Int ) +Bytes b"E\xc9,,\xd0\xdf{-p^\xf1,\xffw\xcb\x0b\xc5W\xed\"" +Bytes #buf ( 5 , WORD6:Int ) +Bytes #buf ( 5 , WORD5:Int ) )
+          ) ... </k>
+          requires 0 <=Int WORD5 andBool WORD5 <Int 2 ^Int 35
+           andBool 0 <=Int WORD6 andBool WORD6 <Int 2 ^Int 35
+           andBool 0 <=Int WORD7 andBool WORD7 <Int 256
+
 endmodule
\ No newline at end of file