Skip to content

Commit

Permalink
removing lemmas that are now in KEVM
Browse files Browse the repository at this point in the history
  • Loading branch information
@PetarMax
PetarMax committed Aug 24, 2024
1 parent 5aeed76 commit 09e7031
Showing 1 changed file with 0 additions and 139 deletions.
139 changes: 0 additions & 139 deletions src/kontrol/kdist/kontrol_lemmas.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,8 +49,6 @@ module KONTROL-AUX-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 B requires 0 <=Int A andBool 0 <Int B [simplification, preserves-definedness]
Expand Down Expand Up @@ -95,11 +93,6 @@ module KONTROL-AUX-LEMMAS
andBool (log2Int (X +Int 1)) /Int 8 <=Int lengthBytes(BA) andBool lengthBytes(BA) <=Int 32
[simplification, concrete(X), preserves-definedness]
// #asWord
rule #asWord ( B1 +Bytes B2 ) => #asWord ( B2 )
requires #asWord ( B1 ) ==Int 0
[simplification, concrete(B1)]
rule #asWord( BA ) >>Int N => #asWord( #range ( BA, 0, lengthBytes( BA ) -Int ( N /Int 8 ) ) )
requires 0 <=Int N andBool N modInt 8 ==Int 0
[simplification, concrete(N), preserves-definedness]
Expand Down Expand Up @@ -275,138 +268,6 @@ module KONTROL-AUX-LEMMAS
rule [chop-no-overflow-mul-r]: X:Int <=Int chop ( Y *Int X:Int ) => X *Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y) [simplification]
rule [chop-no-overflow-div]: X:Int <=Int chop ( X /Int Y:Int ) => X /Int Y <Int pow256 requires #rangeUInt(256, X) andBool 0 <Int Y andBool Y <Int pow256 [simplification]
// Index of first bit that equals one
syntax Int ::= #getFirstOneBit(Int) [function, total]
rule [gfo-succ]: #getFirstOneBit(X:Int) => log2Int ( X &Int ( ( maxUInt256 xorInt X ) +Int 1 ) ) requires #rangeUInt(256, X) andBool X =/=Int 0
rule [gfo-fail]: #getFirstOneBit(X:Int) => -1 requires notBool (#rangeUInt(256, X) andBool X =/=Int 0)
// Index of first bit that equals zero
syntax Int ::= #getFirstZeroBit(Int) [function, total]
rule [gfz-succ]: #getFirstZeroBit(X:Int) => #getFirstOneBit ( maxUInt256 xorInt X ) requires #rangeUInt(256, X)
rule [gfz-fail]: #getFirstZeroBit(X:Int) => -1 requires notBool #rangeUInt(256, X)
// Slot updates are performed by the compiler with the help of masks,
// which are 256-bit integers of the form 11111111100000000000111111111111111
// |- WIDTH -||- SHIFT -|
// Shift of a mask, in bits and in bytes
syntax Int ::= #getMaskShiftBits(Int) [function, total]
syntax Int ::= #getMaskShiftBytes(Int) [function, total]
rule [gms-bits]: #getMaskShiftBits(X:Int) => #getFirstZeroBit(X) [concrete(X), simplification]
rule [gms-bits-succ]: #getMaskShiftBytes(X:Int) => #getFirstZeroBit(X) /Int 8 requires #getMaskShiftBits(X) modInt 8 ==Int 0 [concrete(X), simplification, preserves-definedness]
rule [gms-bits-fail]: #getMaskShiftBytes(X:Int) => -1 requires notBool ( #getMaskShiftBits(X) modInt 8 ==Int 0 ) [concrete(X), simplification, preserves-definedness]
// Width of a mask, in bits and in bytes
syntax Int ::= #getMaskWidthBits(Int) [function, total]
syntax Int ::= #getMaskWidthBytes(Int) [function, total]
rule [gmw-bits-succ-1]: #getMaskWidthBits(X:Int) => 256 -Int #getMaskShiftBits(X:Int) requires 0 <=Int #getMaskShiftBits(X) andBool 0 ==Int X >>Int #getMaskShiftBits(X) [concrete(X), simplification]
rule [gmw-bits-succ-2]: #getMaskWidthBits(X:Int) => #getFirstOneBit(X >>Int #getMaskShiftBits(X)) requires 0 <=Int #getMaskShiftBits(X) andBool 0 <Int X >>Int #getMaskShiftBits(X) [concrete(X), simplification]
rule [gmw-bits-fail]: #getMaskWidthBits(X:Int) => -1 requires -1 ==Int #getMaskShiftBits(X) [concrete(X), simplification]
rule [gmw-bytes-succ]: #getMaskWidthBytes(X:Int) => #getMaskWidthBits(X) /Int 8 requires #getMaskWidthBits(X) modInt 8 ==Int 0 [concrete(X), simplification, preserves-definedness]
rule [gmw-bytes-fail]: #getMaskWidthBytes(X:Int) => -1 requires notBool ( #getMaskWidthBits(X) modInt 8 ==Int 0 ) [concrete(X), simplification, preserves-definedness]
// Mask recogniser
syntax Bool ::= #isMask(Int) [function, total]
// A number is a mask if it has a valid shift, and a valid width, and all remaining bits set to one
rule [is-mask-true]:
#isMask(X:Int) => maxUInt256 ==Int X |Int ( 2 ^Int ( #getMaskShiftBits(X) +Int #getMaskWidthBits(X) ) -Int 1 )
requires 0 <=Int #getMaskShiftBytes(X) andBool 0 <=Int #getMaskWidthBytes(X)
[concrete(X), simplification, preserves-definedness]
// and is not a mask otherwise
rule [is-mask-false]:
#isMask(X:Int) => false
requires notBool ( 0 <=Int #getMaskShiftBytes(X) andBool 0 <=Int #getMaskWidthBytes(X) )
[concrete(X), simplification, preserves-definedness]
// ###########################################################################
// Masking lemmas
// ###########################################################################
// Slot updates are of the general form (SHIFT *Int VALUE) |Int (MASK &Int #asWord( SLOT:Bytes )),
// andthe masking clears the part of the slot into which VALUE will be stored,
// and for VALUE to be stored correctly it first has to be shifted appropriately.
// Note that SHIFT and MASK are always concrete.
//
// We perform this update in several stages:
// 1. First, we simplify MASK &Int #asWord( SLOT ), which results in
// ( VALUE *Int SHIFT ) |Int #asWord ( B1 +Bytes ... +Bytes BN ).
// 2. Then, we isolate the +Bytes-junct(s) that will be overwritten.
// 3. Then, we write the VALUE, possibly splitting the identified +Bytes-junct(s).
//
// Note that we require additional simplifications to account for the fact that
// VALUE and SLOT can also be concrete. In the former case, we need to extract the
// SHIFT appropriate, and in the latter case, the slot will appear on the LHS of the |Int.
// 1. Slot masking using &Int
rule [mask-b-and]:
MASK:Int &Int SLOT:Int =>
#asWord ( #buf ( 32, SLOT ) [ 32 -Int ( #getMaskShiftBytes(MASK) +Int #getMaskWidthBytes(MASK) ) := #buf ( #getMaskWidthBytes(MASK), 0 ) ] )
requires #rangeUInt(256, MASK) andBool #rangeUInt(256, SLOT)
andBool #isMask(MASK)
[simplification, concrete(MASK), preserves-definedness]
// 2a. |Int and +Bytes, update to be done in left
rule [bor-update-to-left]:
A |Int #asWord ( B1 +Bytes B2 ) =>
#asWord ( #buf ( 32 -Int lengthBytes(B2), (A /Int (2 ^Int (8 *Int lengthBytes(B2)))) |Int #asWord ( #buf (32 -Int (lengthBytes(B1) +Int lengthBytes(B2)), 0) +Bytes B1 ) ) +Bytes B2 )
requires #rangeUInt(256, A) andBool A modInt (2 ^Int (8 *Int lengthBytes(B2))) ==Int 0 andBool lengthBytes(B1 +Bytes B2) <=Int 32
[simplification, preserves-definedness]
// 2b. |Int of +Bytes, update to be done in right
rule [bor-update-to-right]:
A |Int #asWord ( B1 +Bytes B2 ) =>
#asWord ( B1 +Bytes #buf ( lengthBytes(B2), A |Int #asWord ( B2 ) ) )
requires 0 <=Int A andBool A <Int 2 ^Int (8 *Int lengthBytes(B2))
[simplification, preserves-definedness]
// 3a. Update with explicit shift and symbolic slot
rule [bor-update-with-shift]:
( SHIFT *Int X ) |Int Y => #asWord ( #buf( 32 -Int ( log2Int(SHIFT) /Int 8 ), X ) +Bytes #buf( log2Int(SHIFT) /Int 8, Y ) )
requires rangeUInt(256, SHIFT) andBool SHIFT ==Int 2 ^Int log2Int(SHIFT) andBool log2Int(SHIFT) modInt 8 ==Int 0
andBool 0 <=Int X andBool X <Int 2 ^Int (8 *Int (32 -Int ( log2Int(SHIFT) /Int 8 )))
andBool 0 <=Int Y andBool Y <Int SHIFT
[simplification, concrete(SHIFT), comm, preserves-definedness]
// 3b. Buffer cropping
rule [buf-asWord-crop]:
#buf (W1:Int, #asWord(#buf(W2, X:Int) +Bytes B)) => #buf(W1 -Int lengthBytes(B), X) +Bytes B
requires 0 <=Int W1 andBool 0 <=Int W2 andBool lengthBytes(B) <=Int W1 andBool W1 <=Int W2 +Int lengthBytes(B)
andBool 0 <=Int X andBool X <Int 2 ^Int (8 *Int (W1 -Int lengthBytes(B)))
[simplification]
// 3c. Splitting the updated buffer into the updated value and the trailing zeros, explicit shift
rule [buf-split-l]:
#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
andBool 0 <=Int X andBool X <Int 2 ^Int (8 *Int (W -Int ( log2Int(SHIFT) /Int 8)))
[simplification, concrete(W, SHIFT), preserves-definedness]
// 3d. Splitting the updated buffer into the updated value and the trailing zeros, implicit shift
rule [bor-split]:
X |Int Y => #asWord ( #buf ( 32 -Int #getFirstOneBit(X) /Int 8, X /Int ( 2 ^Int ( 8 *Int ( #getFirstOneBit(X) /Int 8 ) ) ) ) +Bytes
#buf ( #getFirstOneBit(X) /Int 8, Y ) )
requires #rangeUInt(256, X) andBool 0 <=Int #getFirstOneBit(X)
andBool 0 <=Int Y andBool Y <Int 2 ^Int ( 8 *Int ( #getFirstOneBit(X) /Int 8 ) )
[simplification, concrete(X), preserves-definedness]
// 3e. Clearing update leftovers that only have bits higher than the buffer accepts
rule [buf-bor-subsume]:
#buf ( N, X |Int Y ) => #buf ( N, X )
requires 0 <=Int N andBool N <=Int 32
andBool 0 <=Int X andBool X <Int 2 ^Int ( 8 *Int N )
andBool Y modInt 2 ^Int ( 8 *Int N ) ==Int 0
[simplification, concrete(X), preserves-definedness]
//
// #lookup
//
Expand Down

0 comments on commit 09e7031

Please sign in to comment.