Skip to content

Commit

Permalink
Add log2 verification (#21)
Browse files Browse the repository at this point in the history 
* Make mulWad specs exhaustive

* Update run script and add `smt-timeout` flag

* Add lemmas for mulWad proofs

* Update run script comptibility with `kontrol` tool

* Update verification summary for `wadMul` and `wadMulUp`

* Re-push to rebuild with CI changes

* Update action.yml

* login to pull private image form docker

* Define the ubuntu user

* WRong path

* Run direct

* Check copy directory

* call just the script

* Remove interactive shell

* List directory

* Fix user chown

* Change permissions

* Wrong workspace

* First try to debug the proof

* entire log2 proof

* lemmas and simplifications

* getting there

* passing probably

* adjustment to test

* this hopefully passes

* run-kevm.sh: update `log2` test name

* Try fix CI merge mess

* Fix merge mess for `mulWad` proofs

* Remove selector error comments

* Set `testLog2` mutability to `pure`

* action.yml: revert `ubuntu` user name to `user`

* Revert "Try fix CI merge mess"

This reverts commit 7839dd6.

* run-kevm.sh: add branch parallelization and increase eqn recursion

---------

Co-authored-by: Freeman <[email protected]>
Co-authored-by: F-WRunTime <[email protected]>
Co-authored-by: Lisandra Silva <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
Co-authored-by: Palina Tolmach <[email protected]>
  • Loading branch information
@JuanCoRo @F-WRunTime
@PetarMax @palinatolmach
6 people authored Aug 23, 2024
1 parent d83ef9c commit 7ffbf14
Show file tree
Hide file tree
Showing 3 changed files with 225 additions and 19 deletions.
58 changes: 55 additions & 3 deletions test/FixedPointMathLib.k.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ contract FixedPointMathLibVerification is Test, KontrolCheats {
// Constants
uint256 constant WAD = 1e18;

// Public wrapper for mulWad since Kontrol doesn't support vm.expectRevert
// Public wrapper for mulWad since Kontrol doesn't support vm.expectRevert
// for internal calls, and FixedPointMathLib.mulWad is internal
function mulWad(uint x, uint y) public pure returns (uint256) {
return FixedPointMathLib.mulWad(x, y);
Expand All @@ -30,7 +30,7 @@ contract FixedPointMathLibVerification is Test, KontrolCheats {

assert(zImpl == zSpec);
} else {
vm.expectRevert(FixedPointMathLib.MulWadFailed.selector); // FixedPointMathLib.MulWadFailed.selector
vm.expectRevert(FixedPointMathLib.MulWadFailed.selector);
this.mulWad(x, y);
}

Expand All @@ -44,8 +44,60 @@ contract FixedPointMathLibVerification is Test, KontrolCheats {

assert(zImpl == zSpec);
} else {
vm.expectRevert(FixedPointMathLib.MulWadFailed.selector); // FixedPointMathLib.MulWadFailed.selector
vm.expectRevert(FixedPointMathLib.MulWadFailed.selector);
this.mulWadUp(x, y);
}
}

//function log2(uint256 x) internal pure returns (uint256 r) {
// /// @solidity memory-safe-assembly
// assembly {
// r := shl(7, lt(0xffffffffffffffffffffffffffffffff, x))
// r := or(r, shl(6, lt(0xffffffffffffffff, shr(r, x))))
// r := or(r, shl(5, lt(0xffffffff, shr(r, x))))
// r := or(r, shl(4, lt(0xffff, shr(r, x))))
// r := or(r, shl(3, lt(0xff, shr(r, x))))
// r := or(r, shl(2, lt(0xf, shr(r, x))))
// r := or(r, byte(shr(r, x), hex"00000101020202020303030303030303"))
// }
//}

//function testMyLog2(uint256 x) public {
// uint256 r = log2(x);
// if(x > 0)
// assertLe(2**r, x);
// else
// assertEq(r,0);
//}

function testLog2(uint256 x) public pure {

unchecked {
uint256 y = x; uint256 z = 0;
if (2 ** 128 - 1 < y) { y = y >> 128; } else { }
if (2 ** 64 - 1 < y) { y = y >> 64; } else { }
if (2 ** 32 - 1 < y) { y = y >> 32; } else { }
if (2 ** 16 - 1 < y) { y = y >> 16; } else { }
if (2 ** 8 - 1 < y) { y = y >> 8; } else { }
if (2 ** 4 - 1 < y) { y = y >> 4; } else { }

if (2 ** 3 - 1 < y) z = 4; else
if (2 ** 2 - 1 < y) z = 3; else
if (2 ** 1 - 1 < y) z = 2; else
if (2 ** 0 - 1 < y) z = 1;
}

uint256 r = FixedPointMathLib.log2(x);

if(x > 0){
assertLe(2**r, x);
if (r < 255) {
assertLt(x, 2**(r+1));
} else {
assertEq(r, 255);
}
}
else
assertEq(r,0);
}
}
17 changes: 10 additions & 7 deletions test/run-kevm.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,14 +7,15 @@ forge_build() {
}

kontrol_kompile() {
kontrol build \
--verbose \
--require ${lemmas} \
--module-import ${module} \
GHCRTS='' kontrol build \
--verbose \
--require ${lemmas} \
--module-import ${module} \
${rekompile}
}

kontrol_prove() {
export GHCRTS='-N6'
kontrol prove \
--max-depth ${max_depth} \
--max-iterations ${max_iterations} \
Expand All @@ -29,7 +30,8 @@ kontrol_prove() {
${break_every_step} \
${break_on_calls} \
${tests} \
${use_booster}
--max-frontier-parallel 6 \
--kore-rpc-command 'kore-rpc-booster --equation-max-recursion 10'
}

kontrol_claim() {
Expand All @@ -51,7 +53,7 @@ smt_timeout=100000

# Number of processes run by the prover in parallel
# Should be at most (M - 8) / 8 in a machine with M GB of RAM
workers=12
workers=3

# Switch the options below to turn them on or off
rekompile=--rekompile
Expand Down Expand Up @@ -89,9 +91,10 @@ use_booster=--use-booster
tests=""
tests+="--match-test FixedPointMathLibVerification.testMulWad(uint256,uint256) "
tests+="--match-test FixedPointMathLibVerification.testMulWadUp "
tests+="--match-test FixedPointMathLibVerification.testLog2 "

# Name of the claim to execute
claim=mulWadUp-first-roadblock
claim=log2-06

# Comment these lines as needed
pkill kore-rpc || true
Expand Down
169 changes: 160 additions & 9 deletions test/solady-lemmas.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,36 +20,187 @@ module SOLADY-LEMMAS

rule <k> runLemma(T) => doneLemma(T) ... </k>


//
// Bool
//

rule bool2Word ( X ) => 1 requires X [simplification]
rule bool2Word ( X ) => 0 requires notBool X [simplification]

rule chop ( bool2Word ( X ) <<Int Y ) => bool2Word ( X ) <<Int Y requires Y <Int 256 [simplification]

rule chop ( 1 <<Int Y ) => 1 <<Int Y requires Y <Int 256 [simplification]

rule ( A:Int >>Int B:Int ) >>Int C:Int => A >>Int ( B +Int C ) [simplification]

rule A =/=Int B => notBool ( A ==Int B )
[simplification, comm]

rule #Ceil ( byte (X:Int, Y:Int) ) => #Top
requires 0 <=Int X andBool X <Int 32
andBool 0 <=Int Y andBool Y <Int pow256
[simplification]

//
// ML
// Bitwise
//

rule #Not ( { false #Equals X:Bool andBool Y:Bool } ) => {true #Equals X } #And { true #Equals Y } [simplification]
rule A >>Int B ==Int 0 => log2Int ( A ) <=Int B
[simplification, comm, concrete(A)]

//
// Arithmetic
//
rule 0 <=Int A >>Int B => true
requires 0 <=Int A andBool 0 <=Int B
[simplification]

rule A >>Int B <=Int C => A <=Int ( C <<Int B ) +Int ( 2 ^Int B ) -Int 1
requires C +Int 1 ==Int 2 ^Int ( log2Int ( C +Int 1 ) )
[simplification, concrete(B, C)]

rule C <Int A >>Int B => ( C <<Int B ) +Int ( 2 ^Int B ) -Int 1 <Int A
requires C +Int 1 ==Int 2 ^Int ( log2Int ( C +Int 1 ) )
[simplification, concrete(B, C)]

rule X xorInt maxUInt256 => maxUInt256 -Int X
requires #rangeUInt ( 256 , X )
[simplification]

//
// Comparisons
//

// Concrete to the left of comparisons, prioritising <=Int and <Int
rule X >=Int Y => Y <=Int X [simplification, concrete(Y)]
rule X >Int Y => Y <Int X [simplification, concrete(Y)]

// Negations at K-level
rule notBool X <=Int Y => Y <Int X [simplification]
rule notBool X <Int Y => Y <=Int X [simplification]
rule notBool X >Int Y => X <=Int Y [simplification]
rule notBool X >=Int Y => X <Int Y [simplification]

// Negations ad ML-level
rule { true #Equals ( notBool X <=Int Y ) } => { true #Equals Y <Int X } [simplification]
rule { true #Equals ( notBool X <Int Y ) } => { true #Equals Y <=Int X } [simplification]
rule { true #Equals ( notBool X >Int Y ) } => { true #Equals X <=Int Y } [simplification]
rule { true #Equals ( notBool X >=Int Y ) } => { true #Equals X <Int Y } [simplification]
rule { ( notBool X <=Int Y ) #Equals true } => { true #Equals Y <Int X } [simplification]
rule { ( notBool X <Int Y ) #Equals true } => { true #Equals Y <=Int X } [simplification]
rule { ( notBool X >Int Y ) #Equals true } => { true #Equals X <=Int Y } [simplification]
rule { ( notBool X >=Int Y ) #Equals true } => { true #Equals X <Int Y } [simplification]

//
// Arithmetic
//

rule A modInt B => A
requires 0 <=Int A andBool A <Int B
[simplification]

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

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

rule A <=Int B -Int C => C <=Int B -Int A
[simplification, concrete(A, B)]

//
// Specialised
//

syntax Int ::= "cachedBytesConstant" [alias]
rule cachedBytesConstant => 6928917744019834342450304135053993530982274426945361611473370484834304

rule ( cachedBytesConstant >>Int ( ( maxUInt5 -Int Y ) *Int 8 ) ) modInt 256 => 0
requires 0 <=Int Y andBool Y <Int 32
andBool ( Y <=Int 1 orBool Y >=Int 16 )
[simplification]

rule ( cachedBytesConstant >>Int ( ( maxUInt5 -Int Y ) *Int 8 ) ) modInt 256 => 1
requires 0 <=Int Y andBool Y <Int 32
andBool 1 <Int Y andBool Y <=Int 3
[simplification]

rule ( cachedBytesConstant >>Int ( ( maxUInt5 -Int Y ) *Int 8 ) ) modInt 256 => 2
requires 0 <=Int Y andBool Y <Int 32
andBool 3 <Int Y andBool Y <=Int 7
[simplification]

rule ( cachedBytesConstant >>Int ( ( maxUInt5 -Int Y ) *Int 8 ) ) modInt 256 => 3
requires 0 <=Int Y andBool Y <Int 32
andBool 7 <Int Y andBool Y <=Int 15
[simplification]

rule byte ( X:Int >>Int Y:Int , cachedBytesConstant ) => 3
requires 0 <=Int X andBool 0 <=Int Y
andBool X <=Int ( 2 ^Int ( Y +Int 4 ) -Int 1 )
andBool 7 <Int X >>Int Y
[simplification, concrete(Y)]

rule byte ( X:Int >>Int Y:Int , cachedBytesConstant ) => 2
requires 0 <=Int X andBool 0 <=Int Y
andBool X <=Int ( 2 ^Int ( Y +Int 4 ) -Int 1 )
andBool notBool 7 <Int X >>Int Y
andBool 3 <Int X >>Int Y
[simplification, concrete(Y)]

rule byte ( X:Int >>Int Y:Int , cachedBytesConstant ) => 1
requires 0 <=Int X andBool 0 <=Int Y
andBool X <=Int ( 2 ^Int ( Y +Int 4 ) -Int 1 )
andBool notBool 3 <Int X >>Int Y
andBool 1 <Int X >>Int Y
[simplification, concrete(Y)]

rule byte ( X:Int >>Int Y:Int , cachedBytesConstant ) => 0
requires 0 <=Int X andBool 0 <=Int Y
andBool X <=Int ( 2 ^Int ( Y +Int 4 ) -Int 1 )
andBool notBool 1 <Int X >>Int Y
andBool 0 <Int X >>Int Y
[simplification, concrete(Y)]

endmodule

module SOLADY-LEMMAS-SPEC
imports SOLADY-LEMMAS

claim [first-roadblock]: <k> runLemma(bool2Word( notBool ( notBool ( ( notBool X:Int ==Int 0 ) andBool maxUInt256 /Word X:Int <Int 0 ) ) )) => doneLemma(0) ... </k>
claim [mulWad-first-roadblock]: <k> runLemma(bool2Word( notBool ( notBool ( ( notBool X:Int ==Int 0 ) andBool maxUInt256 /Word X:Int <Int 0 ) ) )) => doneLemma(0) ... </k>
requires 0 <=Int X
//claim [log2-01]: <k> runLemma(chop (bool2Word ( X:Bool ) <<Int 7)) => doneLemma(128) ... </k>
// requires X:Bool

//claim [log2-02]: <k> runLemma(chop (bool2Word ( X:Bool ) <<Int 7)) => doneLemma(0) ... </k>
// requires notBool X:Bool

//claim [log2-03]: <k> runLemma(1 <<Word (bool2Word ( X:Bool ) <<Int 7)) => doneLemma(pow128) ... </k>
// requires X:Bool

//claim [log2-04]: <k> runLemma(bool2Word ( X:Bool ) <<Int 7) => doneLemma(128) ... </k>
// requires X:Bool

//claim [log2-05]: <k> runLemma( maxUInt8 <Int chop ( bool2Word ( _ ) <<Int 7) ) => doneLemma(false) ... </k>

//claim [log2-06]: <k> runLemma (maxUInt8 <Int ( bool2Word ( maxUInt64 <Int X:Int >>Int bool2Word ( maxUInt128 <Int X:Int ) <<Int 7 ) <<Int 6 |Int bool2Word ( maxUInt128 <Int X:Int ) <<Int 7 ) ) => doneLemma(false) ... </k>

// claim [log2-07]: <k> runLemma (1 <<Int ( bool2Word ( maxUInt64 <Int X:Int >>Int bool2Word ( maxUInt128 <Int X:Int ) <<Int 7 ) <<Int 6 |Int bool2Word ( maxUInt128 <Int X:Int ) <<Int 7 ) <=Int X:Int) => doneLemma(maxUInt128 <Int X:Int) ... </k>

claim [arith-01]:
<k>
runLemma (
notBool ( maxUInt8 <=Int ( 4 |Int ( ( cachedBytesConstant >>Int ( ( maxUInt5 -Int ( VV0_x_114b9705:Int >>Int 4 ) ) *Int 8 ) ) modInt 256 ) ) )
andBool VV0_x_114b9705 >>Int 4 <Int 32
) => doneLemma (
true
)
</k>
requires 0 <=Int VV0_x_114b9705:Int
andBool VV0_x_114b9705:Int >>Int 4 <=Int 1

claim [arith-02]:
<k>
runLemma ( maxUInt64 <Int VV0_x_114b9705:Int >>Int 128 ) => doneLemma ( false )
</k>
requires VV0_x_114b9705 <=Int maxUInt192

claim [mulWadUp-second-roadblock]: <k> runLemma( notBool ( ( notBool X:Int ==Int 0 ) andBool maxUInt256 /Word X:Int <Int Y:Int ) ) => doneLemma(false) ... </k>
requires ( notBool ( notBool ( ( notBool X:Int ==Int 0 ) andBool maxUInt256 /Word X:Int <Int Y:Int ) ) )
Expand Down

0 comments on commit 7ffbf14

Please sign in to comment.