Skip to content

Instantly share code, notes, and snippets.

@MrChico

MrChico/rules.k

Created February 18, 2019 22:31
Show Gist options
  • Save MrChico/4f5e3eac848ec692479e958293484d9a to your computer and use it in GitHub Desktop.
Save MrChico/4f5e3eac848ec692479e958293484d9a to your computer and use it in GitHub Desktop.
Download ZIP
Raw
rules.k
requires "domains.k"
requires "edsl.k"
requires "evm.k"
module RULES
imports EVM
imports EDSL
// VERIFICATION.k
syntax Int ::= nthbyteof ( Int , Int , Int ) [function, smtlib(smt_nthbyteof), proj]
// ------------------------------------------------------------------------------
rule nthbyteof(V, I, N) => nthbyteof(V /Int 256, I, N -Int 1) when N >Int (I +Int 1) [concrete]
rule nthbyteof(V, I, N) => V modInt 256 when N ==Int (I +Int 1) [concrete]
syntax Map ::= Map "+Map" Map [function] //concatenates two maps if their keys are disjoint
rule M +Map (K1 |-> V1) => M (K1 |-> V1)
requires notBool #inKeys(M, K1)
syntax Bool ::= #inKeys(Map, Int) [function]
rule #inKeys(.Map, KEY) => false
rule #inKeys((M:Map K0 |-> V0), K1) => true
requires K0 ==K K1
rule #inKeys((M:Map K0 |-> V0), K1) => #inKeys(M, K1)
requires K0 =/=K K1
rule 0 <=Int nthbyteof(V, I, N) => true
rule nthbyteof(V, I, N) <Int 256 => true
rule #asWord( nthbyteof(V, 0, 32)
: nthbyteof(V, 1, 32)
: nthbyteof(V, 2, 32)
: nthbyteof(V, 3, 32)
: nthbyteof(V, 4, 32)
: nthbyteof(V, 5, 32)
: nthbyteof(V, 6, 32)
: nthbyteof(V, 7, 32)
: nthbyteof(V, 8, 32)
: nthbyteof(V, 9, 32)
: nthbyteof(V, 10, 32)
: nthbyteof(V, 11, 32)
: nthbyteof(V, 12, 32)
: nthbyteof(V, 13, 32)
: nthbyteof(V, 14, 32)
: nthbyteof(V, 15, 32)
: nthbyteof(V, 16, 32)
: nthbyteof(V, 17, 32)
: nthbyteof(V, 18, 32)
: nthbyteof(V, 19, 32)
: nthbyteof(V, 20, 32)
: nthbyteof(V, 21, 32)
: nthbyteof(V, 22, 32)
: nthbyteof(V, 23, 32)
: nthbyteof(V, 24, 32)
: nthbyteof(V, 25, 32)
: nthbyteof(V, 26, 32)
: nthbyteof(V, 27, 32)
: nthbyteof(V, 28, 32)
: nthbyteof(V, 29, 32)
: nthbyteof(V, 30, 32)
: nthbyteof(V, 31, 32)
: .WordStack ) => V
requires 0 <=Int V andBool V <Int pow256
rule #asWord( nthbyteof(#unsigned(V), 0, 32)
: nthbyteof(#unsigned(V), 1, 32)
: nthbyteof(#unsigned(V), 2, 32)
: nthbyteof(#unsigned(V), 3, 32)
: nthbyteof(#unsigned(V), 4, 32)
: nthbyteof(#unsigned(V), 5, 32)
: nthbyteof(#unsigned(V), 6, 32)
: nthbyteof(#unsigned(V), 7, 32)
: nthbyteof(#unsigned(V), 8, 32)
: nthbyteof(#unsigned(V), 9, 32)
: nthbyteof(#unsigned(V), 10, 32)
: nthbyteof(#unsigned(V), 11, 32)
: nthbyteof(#unsigned(V), 12, 32)
: nthbyteof(#unsigned(V), 13, 32)
: nthbyteof(#unsigned(V), 14, 32)
: nthbyteof(#unsigned(V), 15, 32)
: nthbyteof(#unsigned(V), 16, 32)
: nthbyteof(#unsigned(V), 17, 32)
: nthbyteof(#unsigned(V), 18, 32)
: nthbyteof(#unsigned(V), 19, 32)
: nthbyteof(#unsigned(V), 20, 32)
: nthbyteof(#unsigned(V), 21, 32)
: nthbyteof(#unsigned(V), 22, 32)
: nthbyteof(#unsigned(V), 23, 32)
: nthbyteof(#unsigned(V), 24, 32)
: nthbyteof(#unsigned(V), 25, 32)
: nthbyteof(#unsigned(V), 26, 32)
: nthbyteof(#unsigned(V), 27, 32)
: nthbyteof(#unsigned(V), 28, 32)
: nthbyteof(#unsigned(V), 29, 32)
: nthbyteof(#unsigned(V), 30, 32)
: nthbyteof(#unsigned(V), 31, 32)
: .WordStack ) => #unsigned(V)
requires #rangeSInt(256, V)
rule #asWord( nthbyteof(keccakIntList(V), 0, 32)
: nthbyteof(keccakIntList(V), 1, 32)
: nthbyteof(keccakIntList(V), 2, 32)
: nthbyteof(keccakIntList(V), 3, 32)
: nthbyteof(keccakIntList(V), 4, 32)
: nthbyteof(keccakIntList(V), 5, 32)
: nthbyteof(keccakIntList(V), 6, 32)
: nthbyteof(keccakIntList(V), 7, 32)
: nthbyteof(keccakIntList(V), 8, 32)
: nthbyteof(keccakIntList(V), 9, 32)
: nthbyteof(keccakIntList(V), 10, 32)
: nthbyteof(keccakIntList(V), 11, 32)
: nthbyteof(keccakIntList(V), 12, 32)
: nthbyteof(keccakIntList(V), 13, 32)
: nthbyteof(keccakIntList(V), 14, 32)
: nthbyteof(keccakIntList(V), 15, 32)
: nthbyteof(keccakIntList(V), 16, 32)
: nthbyteof(keccakIntList(V), 17, 32)
: nthbyteof(keccakIntList(V), 18, 32)
: nthbyteof(keccakIntList(V), 19, 32)
: nthbyteof(keccakIntList(V), 20, 32)
: nthbyteof(keccakIntList(V), 21, 32)
: nthbyteof(keccakIntList(V), 22, 32)
: nthbyteof(keccakIntList(V), 23, 32)
: nthbyteof(keccakIntList(V), 24, 32)
: nthbyteof(keccakIntList(V), 25, 32)
: nthbyteof(keccakIntList(V), 26, 32)
: nthbyteof(keccakIntList(V), 27, 32)
: nthbyteof(keccakIntList(V), 28, 32)
: nthbyteof(keccakIntList(V), 29, 32)
: nthbyteof(keccakIntList(V), 30, 32)
: nthbyteof(keccakIntList(V), 31, 32)
: .WordStack ) => keccakIntList(V)
rule ACCTCODE in SetItem( 1 )
SetItem ( 2 )
SetItem ( 3 )
SetItem ( 4 )
SetItem ( 5 )
SetItem ( 6 )
SetItem ( 7 )
SetItem ( 8 )
=> false
requires 9 <=Int ACCTCODE
// for terms came from bytecode not via #hashedLocation
rule keccak(WS) => keccakIntList(byteStack2IntList(WS))
requires ( notBool #isConcrete(WS) )
// andBool ( #sizeWordStack(WS) ==Int 32 orBool #sizeWordStack(WS) ==Int 64 )
rule 0 <=Int keccakIntList(N) => true
rule keccaktIntList(N) <Int pow256 => true
rule #padToWidth(32, #asByteStack( #unsigned(V) )) => #asByteStackInWidth( #unsigned(V), 32)
requires #rangeSInt(256, V)
rule #padToWidth(32, #asByteStack(V)) => #asByteStackInWidth(V, 32)
requires 0 <=Int V andBool V <Int pow256
rule #padToWidth(32, #asByteStack( keccakIntList (V) )) => #asByteStackInWidth( keccakIntList (V), 32)
// for Vyper
rule #padToWidth(N, #asByteStack(#asWord(WS))) => WS
requires #noOverflow(WS) andBool N ==Int #sizeWordStack(WS)
// for Solidity
rule #asWord(WS) /Int D => #asWord(#take(#sizeWordStack(WS) -Int log256Int(D), WS))
requires D modInt 256 ==Int 0 andBool D >=Int 0
andBool #sizeWordStack(WS) >=Int log256Int(D)
andBool #noOverflow(WS)
syntax Bool ::= #noOverflow ( WordStack ) [function]
| #noOverflowAux ( WordStack ) [function]
// -------------------------------------------------------
rule #noOverflow(WS) => #sizeWordStack(WS) <=Int 32 andBool #noOverflowAux(WS)
rule #noOverflowAux(W : WS) => 0 <=Int W andBool W <Int 256 andBool #noOverflowAux(WS)
rule #noOverflowAux(.WordStack) => true
syntax WordStack ::= #asByteStackInWidth ( Int, Int ) [function]
| #asByteStackInWidthaux ( Int, Int, Int, WordStack ) [function]
// -----------------------------------------------------------------------------------
rule #asByteStackInWidth(X, N) => #asByteStackInWidthaux(X, N -Int 1, N, .WordStack)
rule #asByteStackInWidthaux(X, I, N, WS) => #asByteStackInWidthaux(X, I -Int 1, N, nthbyteof(X, I, N) : WS) when I >Int 0
rule #asByteStackInWidthaux(X, 0, N, WS) => nthbyteof(X, 0, N) : WS
rule 0 +Int N => N
rule N +Int 0 => N
rule N -Int 0 => N
rule 1 *Int N => N
rule N *Int 1 => N
rule 0 *Int _ => 0
rule _ *Int 0 => 0
rule N /Int 1 => N
rule 0 |Int N => N
rule N |Int 0 => N
rule N |Int N => N
rule 0 &Int N => 0
rule N &Int 0 => 0
rule N &Int N => N
rule (I1 +Int I2) +Int I3 => I1 +Int (I2 +Int I3) when #isConcrete(I2) andBool #isConcrete(I3)
rule (I1 +Int I2) -Int I3 => I1 +Int (I2 -Int I3) when #isConcrete(I2) andBool #isConcrete(I3)
rule (I1 -Int I2) +Int I3 => I1 -Int (I2 -Int I3) when #isConcrete(I2) andBool #isConcrete(I3)
rule (I1 -Int I2) -Int I3 => I1 -Int (I2 +Int I3) when #isConcrete(I2) andBool #isConcrete(I3)
rule I1 &Int (I2 &Int I3) => (I1 &Int I2) &Int I3 when #isConcrete(I1) andBool #isConcrete(I2)
// 0xffff...f &Int N = N
rule MASK &Int N => N requires MASK ==Int (2 ^Int (log2Int(MASK) +Int 1)) -Int 1 // MASK = 0xffff...f
andBool 0 <=Int N andBool N <=Int MASK
// for gas calculation
rule A -Int (#if C #then B1 #else B2 #fi) => #if C #then (A -Int B1) #else (A -Int B2) #fi
rule (#if C #then B1 #else B2 #fi) -Int A => #if C #then (B1 -Int A) #else (B2 -Int A) #fi
rule (#if C #then B1 #else B2 #fi) >Int A => true
requires B1 >Int A andBool B2 >Int A
rule (#if C #then B1 #else B2 #fi) >=Int A => true
requires B1 >=Int A andBool B2 >=Int A
rule A -Int A => 0
rule bool2Word(A) |Int bool2Word(B) => bool2Word(A orBool B)
rule bool2Word(A) &Int bool2Word(B) => bool2Word(A andBool B)
rule bool2Word(A) ==K 0 => notBool(A)
rule bool2Word(A) ==K 1 => A
rule bool2Word(A) =/=K 0 => A
rule bool2Word(A) =/=K 1 => notBool(A)
rule chop(bool2Word(B)) => bool2Word(B)
rule 0 <=Int chop(V) => true
rule chop(V) <Int pow256 => true
rule 0 <=Int keccak(V) => true
rule keccak(V) <Int pow256 => true
rule 0 <=Int X &Int Y => true requires 0 <=Int X andBool X <Int pow256 andBool 0 <=Int Y andBool Y <Int pow256
rule X &Int Y <Int pow256 => true requires 0 <=Int X andBool X <Int pow256 andBool 0 <=Int Y andBool Y <Int pow256
rule chop(I) => I requires 0 <=Int I andBool I <Int pow256
rule #sizeWordStack ( _ , _ ) >=Int 0 => true [smt-lemma]
rule #sizeWordStack ( WS , N:Int )
=> #sizeWordStack ( WS , 0 ) +Int N
requires N =/=K 0
[lemma]
rule chop(#unsigned(W)) => #unsigned(W)
requires #rangeSInt(256, W)
rule #signed(#unsigned(W)) => W
requires #rangeSInt(256, W)
rule #unsigned(#signed(W)) => W
requires #rangeUInt(256, W)
rule W0 s<Word W1 => #signed(W0) <Word #signed(W1)
rule #signed(X) ==K #signed(Y) => X ==K Y requires #rangeUInt(256,X) orBool #rangeUInt(256,Y)
rule #unsigned(X) ==K #unsigned(Y) => X ==K Y requires #rangeSInt(256,X) orBool #rangeSInt(256,Y)
rule A modInt pow160 => A
requires #rangeAddress(A)
syntax Bool ::= #notPrecompileAddress ( Int ) [function]
// ---------------------------------------
rule #notPrecompileAddress ( X ) => 9 <=Int X andBool #rangeAddress(X)
// ABSTRACT SEMANTICS.k
rule <k> LT W0 W1 => bool2Word(W0 <Int W1) ~> #push ... </k> [trusted]
rule <k> GT W0 W1 => bool2Word(W0 >Int W1) ~> #push ... </k> [trusted]
rule <k> EQ W0 W1 => bool2Word(W0 ==Int W1) ~> #push ... </k> [trusted]
rule <k> ISZERO W => bool2Word(W ==Int 0 ) ~> #push ... </k> [trusted]
//RULES MUST USE ==K and not ==Int
//Warning: assumes injective hashing
rule keccakIntList(A B .IntList) ==K keccakIntList(C D .IntList) => A ==Int C andBool B ==Int D
rule keccakIntList(A B .IntList) =/=K keccakIntList(C D .IntList) => A =/=Int C orBool B =/=Int D
rule keccakIntList(A B C .IntList) ==K keccakIntList(D E F .IntList) => A ==Int D andBool B ==Int E andBool C ==Int F
rule keccakIntList(A B C .IntList) =/=K keccakIntList(D E F .IntList) => A =/=Int D orBool B =/=Int E orBool C =/=Int F
rule keccakIntList(C) ==K A => false
requires 0 <=Int A andBool A <=Int 20
rule keccakIntList(C) =/=K A => true
requires 0 <=Int A andBool A <=Int 20
rule keccakIntList(C) +Int B ==K A => false
requires 0 <=Int A andBool A <=Int 20
andBool 0 <=Int B andBool B <=Int 20
rule keccakIntList(C) +Int B =/=K A => true
requires 0 <=Int A andBool A <=Int 20
andBool 0 <=Int B andBool B <=Int 20
rule A ==K keccakIntList(C) +Int B => false
requires 0 <=Int A andBool A <=Int 20
andBool 0 <=Int B andBool B <=Int 20
rule A =/=K keccakIntList(C) +Int B => true
requires 0 <=Int A andBool A <=Int 20
andBool 0 <=Int B andBool B <=Int 20
rule keccakIntList(C) +Int B ==K keccakIntList(A) => false
requires 0 <=Int B andBool B <=Int 20
rule keccakIntList(C) +Int B =/=K keccakIntList(A) => true
requires 0 <=Int B andBool B <=Int 20
rule keccakIntList(A) +Int B ==K keccakIntList(A) +Int C => false
requires B =/=Int C
rule keccakIntList(A) +Int B =/=K keccakIntList(A) +Int C => true
requires B =/=Int C
rule keccakIntList(A) +Int B ==K keccakIntList(C) +Int D => false
requires B =/=Int C
rule keccakIntList(A) +Int B =/=K keccakIntList(C) +Int D => true
requires B =/=Int C
rule keccakIntList(A) ==K keccakIntList(C) +Int B => false
requires 0 <=Int B andBool B <=Int 20
rule keccakIntList(A) =/=K keccakIntList(C) +Int B => true
requires 0 <=Int B andBool B <=Int 20
rule A ==K keccakIntList(C) => false
requires 0 <=Int A andBool A <=Int 20
rule A =/=K keccakIntList(C)=> true
requires 0 <=Int A andBool A <=Int 20
// src/lemmas.k.md
// src/storage.md
syntax Int ::= "#Token.balances" "[" Int "]" [function]
// -----------------------------------------------
// doc: The token balance of `$0`
rule #Token.balances[A] => #hashedLocation("Solidity", 0, A)
endmodule
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment