Skip to content

Commit

Permalink
corrections
Browse files Browse the repository at this point in the history
  • Loading branch information
@PetarMax
PetarMax committed Aug 10, 2024
1 parent 9cbf486 commit c0dca20
Show file tree
Hide file tree
Showing 3 changed files with 35 additions and 32 deletions.
22 changes: 11 additions & 11 deletions contracts/libraries/DualGovernanceState.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -298,14 +298,14 @@ library DualGovernanceState {
DualGovernanceConfig memory config,
uint256 rageQuitSupport
) private pure returns (bool) {
return rageQuitSupport > config.firstSealRageQuitSupport;
return rageQuitSupport >= config.firstSealRageQuitSupport;
}

function _isSecondSealRageQuitSupportCrossed(
DualGovernanceConfig memory config,
uint256 rageQuitSupport
) private pure returns (bool) {
return rageQuitSupport > config.secondSealRageQuitSupport;
return rageQuitSupport >= config.secondSealRageQuitSupport;
}

function _isDynamicTimelockMaxDurationPassed(
Expand Down Expand Up @@ -388,19 +388,19 @@ library DualGovernanceState {
Duration dynamicTimelockMinDuration = config.dynamicTimelockMinDuration;
Duration dynamicTimelockMaxDuration = config.dynamicTimelockMaxDuration;

if (rageQuitSupport <= firstSealRageQuitSupport) {
if (rageQuitSupport < firstSealRageQuitSupport) {
return Durations.ZERO;
}

if (rageQuitSupport > secondSealRageQuitSupport) {
return dynamicTimelockMaxDuration;
if (rageQuitSupport < secondSealRageQuitSupport) {
duration_ = dynamicTimelockMinDuration
+ Durations.from(
(rageQuitSupport - firstSealRageQuitSupport)
* (dynamicTimelockMaxDuration - dynamicTimelockMinDuration).toSeconds()
/ (secondSealRageQuitSupport - firstSealRageQuitSupport)
);
}

duration_ = dynamicTimelockMinDuration
+ Durations.from(
(rageQuitSupport - firstSealRageQuitSupport)
* (dynamicTimelockMaxDuration - dynamicTimelockMinDuration).toSeconds()
/ (secondSealRageQuitSupport - firstSealRageQuitSupport)
);
return dynamicTimelockMaxDuration;
}
}
4 changes: 2 additions & 2 deletions test/kontrol/VetoSignalling.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,9 +75,9 @@ contract VetoSignallingTest is DualGovernanceSetUp {
}

function _calculateDynamicTimelock(Configuration _config, uint256 rageQuitSupport) public view returns (Duration) {
if (rageQuitSupport <= _config.FIRST_SEAL_RAGE_QUIT_SUPPORT()) {
if (rageQuitSupport < _config.FIRST_SEAL_RAGE_QUIT_SUPPORT()) {
return Durations.ZERO;
} else if (rageQuitSupport <= _config.SECOND_SEAL_RAGE_QUIT_SUPPORT()) {
} else if (rageQuitSupport < _config.SECOND_SEAL_RAGE_QUIT_SUPPORT()) {
return _linearInterpolation(_config, rageQuitSupport);
} else {
return _config.DYNAMIC_TIMELOCK_MAX_DURATION();
Expand Down
41 changes: 22 additions & 19 deletions test/kontrol/lido-lemmas.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,11 +43,12 @@ module LIDO-LEMMAS
// *Int
rule A *Int B ==Int 0 => A ==Int 0 orBool B ==Int 0 [simplification]

rule A *Int B => B *Int A [simplification(30), symbolic(A), concrete(B)]

// /Int
rule 0 /Int B => 0 requires B =/=Int 0 [simplification, preserves-definedness]
rule A /Int B ==Int 0 => A ==Int 0 requires B =/=Int 0 [simplification, preserves-definedness]

rule ( A *Int B ) /Int C => A *Int ( B /Int C ) requires B modInt C ==Int 0 [simplification, concrete(B, C), preserves-definedness]
rule ( A *Int B ) /Int C => ( A /Int C ) *Int B requires A modInt C ==Int 0 [simplification, concrete(A, C), preserves-definedness]

// /Word
Expand Down Expand Up @@ -77,7 +78,6 @@ module LIDO-LEMMAS

// modInt
rule (X *Int Y) modInt Z => 0 requires X modInt Z ==Int 0 [simplification, concrete(X, Z), preserves-definedness]
rule (X *Int Y) modInt Z => 0 requires Y modInt Z ==Int 0 [simplification, concrete(Y, Z), preserves-definedness]

// Further generalization of: maxUIntXXX &Int #asWord ( BA )
rule X &Int #asWord ( BA ) => #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) )
Expand Down Expand Up @@ -220,13 +220,6 @@ module LIDO-LEMMAS
andBool log2Int(X +Int 1) <=Int log2Int(Y)
[simplification, concrete(X, Y), preserves-definedness]

rule X &Int ( Y *Int Z ) => 0
requires 0 <=Int X andBool 0 <=Int Y andBool 0 <=Int Z
andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
andBool Z ==Int 2 ^Int log2Int(Z)
andBool log2Int(X +Int 1) <=Int log2Int(Z)
[simplification, concrete(X, Z), preserves-definedness]

rule chop ( X *Int Y ) => X *Int Y
requires 0 <=Int X andBool X <Int ethUpperBound
andBool 0 <=Int Y andBool Y <Int 2 ^Int ( 256 -Int ethMaxWidth )
Expand All @@ -242,17 +235,27 @@ module LIDO-LEMMAS
requires #rangeUInt(256, X) andBool 0 <Int Y
[simplification, preserves-definedness]

rule [mul-cancel-10-le]:
A *Int B <=Int C *Int D => (A /Int 10) *Int B <=Int (C /Int 10) *Int D
requires 0 <=Int A andBool 0 <=Int C andBool A modInt 10 ==Int 0 andBool C modInt 10 ==Int 0
[simplification, concrete(A, C), preserves-definedness]

rule [mul-cancel-10-lt]:
A *Int B <Int C *Int D => (A /Int 10) *Int B <Int (C /Int 10) *Int D
requires 0 <=Int A andBool 0 <=Int C andBool A modInt 10 ==Int 0 andBool C modInt 10 ==Int 0
[simplification, concrete(A, C), preserves-definedness]

//
// Overflows and ranges
//
// rule X <=Int A +Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0 <=Int B [concrete(X), simplification, preserves-definedness]
// rule X <=Int A *Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0 <=Int B [concrete(X), simplification, preserves-definedness]
// rule X <=Int A /Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0 <Int B [concrete(X), simplification, preserves-definedness]
rule X <=Int A +Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0 <=Int B [concrete(X), simplification, preserves-definedness]
rule X <=Int A *Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0 <=Int B [concrete(X), simplification, preserves-definedness]
rule X <=Int A /Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0 <Int B [concrete(X), simplification, preserves-definedness]

// rule X <Int A +Int B => true requires X <=Int 0 andBool 0 <Int A andBool 0 <=Int B [concrete(X), simplification]
// rule X <Int A +Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0 <Int B [concrete(X), simplification]
// rule X <Int A *Int B => true requires X <=Int 0 andBool 0 <Int A andBool 0 <Int B [concrete(X), simplification]
// rule X <Int A /Int B => true requires X <=Int 0 andBool 0 <Int A andBool 0 <Int B [concrete(X), simplification, preserves-definedness]
rule X <Int A +Int B => true requires X <=Int 0 andBool 0 <Int A andBool 0 <=Int B [concrete(X), simplification]
rule X <Int A +Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0 <Int B [concrete(X), simplification]
rule X <Int A *Int B => true requires X <=Int 0 andBool 0 <Int A andBool 0 <Int B [concrete(X), simplification]
rule X <Int A /Int B => true requires X <=Int 0 andBool 0 <Int A andBool 0 <Int B [concrete(X), simplification, preserves-definedness]

rule [chop-no-overflow-add-l]: X:Int <=Int chop ( X +Int Y:Int ) => X +Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y) [simplification]
rule [chop-no-overflow-add-r]: X:Int <=Int chop ( Y +Int X:Int ) => X +Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y) [simplification]
Expand Down Expand Up @@ -328,7 +331,7 @@ module LIDO-LEMMAS

// #buf and |Int
rule [buf-bor-split-l]:
#buf ( W, ( X *Int SHIFT ) |Int Y ) => #buf( W -Int ( log2Int(SHIFT) /Int 8 ), X ) +Bytes #buf( log2Int(SHIFT) /Int 8, Y)
#buf ( W, ( SHIFT *Int X ) |Int Y ) => #buf( W -Int ( log2Int(SHIFT) /Int 8 ), X ) +Bytes #buf( log2Int(SHIFT) /Int 8, Y)
requires 0 <=Int W andBool W <=Int 32 andBool rangeUInt(256, SHIFT)
andBool SHIFT ==Int 2 ^Int log2Int(SHIFT)
andBool log2Int(SHIFT) modInt 8 ==Int 0
Expand All @@ -337,7 +340,7 @@ module LIDO-LEMMAS
[simplification, concrete(W, SHIFT), preserves-definedness]

rule [buf-bor-split-r]:
#buf ( W, Y |Int ( X *Int SHIFT ) ) => #buf(W -Int ( log2Int(SHIFT) /Int 8 ), X) +Bytes #buf(log2Int(SHIFT) /Int 8, Y)
#buf ( W, Y |Int ( SHIFT *Int X ) ) => #buf(W -Int ( log2Int(SHIFT) /Int 8 ), X) +Bytes #buf(log2Int(SHIFT) /Int 8, Y)
requires 0 <=Int W andBool W <=Int 32 andBool rangeUInt(256, SHIFT)
andBool SHIFT ==Int 2 ^Int log2Int(SHIFT)
andBool log2Int(SHIFT) modInt 8 ==Int 0
Expand All @@ -347,7 +350,7 @@ module LIDO-LEMMAS

// #buf and |Int
rule [buf-split-l]:
#buf ( W, X *Int SHIFT ) => #buf( W -Int ( log2Int(SHIFT) /Int 8 ), X ) +Bytes #buf( log2Int(SHIFT) /Int 8, 0)
#buf ( W, SHIFT *Int X ) => #buf( W -Int ( log2Int(SHIFT) /Int 8 ), X ) +Bytes #buf( log2Int(SHIFT) /Int 8, 0)
requires 0 <=Int W andBool W <=Int 32 andBool rangeUInt(256, SHIFT)
andBool SHIFT ==Int 2 ^Int log2Int(SHIFT)
andBool log2Int(SHIFT) modInt 8 ==Int 0
Expand Down

0 comments on commit c0dca20

Please sign in to comment.