API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Feb 21st, 2019
76
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 13.75 KB | None | 0 0
raw download clone embed print report
  1. requires "domains.k"
  2. requires "edsl.k"
  3. requires "evm.k"
  4.  
  5. module RULES
  6. imports EVM
  7. imports EDSL
  8.  
  9. // VERIFICATION.k
  10.  
  11. syntax Int ::= nthbyteof ( Int , Int , Int ) [function, smtlib(smt_nthbyteof), proj]
  12. // ------------------------------------------------------------------------------
  13. rule nthbyteof(V, I, N) => nthbyteof(V /Int 256, I, N -Int 1) when N >Int (I +Int 1) [concrete]
  14. rule nthbyteof(V, I, N) => V modInt 256 when N ==Int (I +Int 1) [concrete]
  15.  
  16. syntax Map ::= Map "+Map" Map [function] //concatenates two maps if their keys are disjoint
  17.  
  18. rule M +Map (K1 |-> V1) => M (K1 |-> V1)
  19. requires notBool #inKeys(M, K1)
  20.  
  21. syntax Bool ::= #inKeys(Map, Int) [function]
  22.  
  23. rule #inKeys(.Map, KEY) => false
  24. rule #inKeys((M:Map K0 |-> V0), K1) => true
  25. requires K0 ==K K1
  26. rule #inKeys((M:Map K0 |-> V0), K1) => #inKeys(M, K1)
  27. requires K0 =/=K K1
  28.  
  29.  
  30. rule 0 <=Int nthbyteof(V, I, N) => true
  31. rule nthbyteof(V, I, N) <Int 256 => true
  32.  
  33. rule #asWord( nthbyteof(V, 0, 32)
  34. : nthbyteof(V, 1, 32)
  35. : nthbyteof(V, 2, 32)
  36. : nthbyteof(V, 3, 32)
  37. : nthbyteof(V, 4, 32)
  38. : nthbyteof(V, 5, 32)
  39. : nthbyteof(V, 6, 32)
  40. : nthbyteof(V, 7, 32)
  41. : nthbyteof(V, 8, 32)
  42. : nthbyteof(V, 9, 32)
  43. : nthbyteof(V, 10, 32)
  44. : nthbyteof(V, 11, 32)
  45. : nthbyteof(V, 12, 32)
  46. : nthbyteof(V, 13, 32)
  47. : nthbyteof(V, 14, 32)
  48. : nthbyteof(V, 15, 32)
  49. : nthbyteof(V, 16, 32)
  50. : nthbyteof(V, 17, 32)
  51. : nthbyteof(V, 18, 32)
  52. : nthbyteof(V, 19, 32)
  53. : nthbyteof(V, 20, 32)
  54. : nthbyteof(V, 21, 32)
  55. : nthbyteof(V, 22, 32)
  56. : nthbyteof(V, 23, 32)
  57. : nthbyteof(V, 24, 32)
  58. : nthbyteof(V, 25, 32)
  59. : nthbyteof(V, 26, 32)
  60. : nthbyteof(V, 27, 32)
  61. : nthbyteof(V, 28, 32)
  62. : nthbyteof(V, 29, 32)
  63. : nthbyteof(V, 30, 32)
  64. : nthbyteof(V, 31, 32)
  65. : .WordStack ) => V
  66. requires 0 <=Int V andBool V <Int pow256
  67.  
  68.  
  69. rule #asWord( nthbyteof(#unsigned(V), 0, 32)
  70. : nthbyteof(#unsigned(V), 1, 32)
  71. : nthbyteof(#unsigned(V), 2, 32)
  72. : nthbyteof(#unsigned(V), 3, 32)
  73. : nthbyteof(#unsigned(V), 4, 32)
  74. : nthbyteof(#unsigned(V), 5, 32)
  75. : nthbyteof(#unsigned(V), 6, 32)
  76. : nthbyteof(#unsigned(V), 7, 32)
  77. : nthbyteof(#unsigned(V), 8, 32)
  78. : nthbyteof(#unsigned(V), 9, 32)
  79. : nthbyteof(#unsigned(V), 10, 32)
  80. : nthbyteof(#unsigned(V), 11, 32)
  81. : nthbyteof(#unsigned(V), 12, 32)
  82. : nthbyteof(#unsigned(V), 13, 32)
  83. : nthbyteof(#unsigned(V), 14, 32)
  84. : nthbyteof(#unsigned(V), 15, 32)
  85. : nthbyteof(#unsigned(V), 16, 32)
  86. : nthbyteof(#unsigned(V), 17, 32)
  87. : nthbyteof(#unsigned(V), 18, 32)
  88. : nthbyteof(#unsigned(V), 19, 32)
  89. : nthbyteof(#unsigned(V), 20, 32)
  90. : nthbyteof(#unsigned(V), 21, 32)
  91. : nthbyteof(#unsigned(V), 22, 32)
  92. : nthbyteof(#unsigned(V), 23, 32)
  93. : nthbyteof(#unsigned(V), 24, 32)
  94. : nthbyteof(#unsigned(V), 25, 32)
  95. : nthbyteof(#unsigned(V), 26, 32)
  96. : nthbyteof(#unsigned(V), 27, 32)
  97. : nthbyteof(#unsigned(V), 28, 32)
  98. : nthbyteof(#unsigned(V), 29, 32)
  99. : nthbyteof(#unsigned(V), 30, 32)
  100. : nthbyteof(#unsigned(V), 31, 32)
  101. : .WordStack ) => #unsigned(V)
  102. requires #rangeSInt(256, V)
  103.  
  104. rule #asWord( nthbyteof(keccakIntList(V), 0, 32)
  105. : nthbyteof(keccakIntList(V), 1, 32)
  106. : nthbyteof(keccakIntList(V), 2, 32)
  107. : nthbyteof(keccakIntList(V), 3, 32)
  108. : nthbyteof(keccakIntList(V), 4, 32)
  109. : nthbyteof(keccakIntList(V), 5, 32)
  110. : nthbyteof(keccakIntList(V), 6, 32)
  111. : nthbyteof(keccakIntList(V), 7, 32)
  112. : nthbyteof(keccakIntList(V), 8, 32)
  113. : nthbyteof(keccakIntList(V), 9, 32)
  114. : nthbyteof(keccakIntList(V), 10, 32)
  115. : nthbyteof(keccakIntList(V), 11, 32)
  116. : nthbyteof(keccakIntList(V), 12, 32)
  117. : nthbyteof(keccakIntList(V), 13, 32)
  118. : nthbyteof(keccakIntList(V), 14, 32)
  119. : nthbyteof(keccakIntList(V), 15, 32)
  120. : nthbyteof(keccakIntList(V), 16, 32)
  121. : nthbyteof(keccakIntList(V), 17, 32)
  122. : nthbyteof(keccakIntList(V), 18, 32)
  123. : nthbyteof(keccakIntList(V), 19, 32)
  124. : nthbyteof(keccakIntList(V), 20, 32)
  125. : nthbyteof(keccakIntList(V), 21, 32)
  126. : nthbyteof(keccakIntList(V), 22, 32)
  127. : nthbyteof(keccakIntList(V), 23, 32)
  128. : nthbyteof(keccakIntList(V), 24, 32)
  129. : nthbyteof(keccakIntList(V), 25, 32)
  130. : nthbyteof(keccakIntList(V), 26, 32)
  131. : nthbyteof(keccakIntList(V), 27, 32)
  132. : nthbyteof(keccakIntList(V), 28, 32)
  133. : nthbyteof(keccakIntList(V), 29, 32)
  134. : nthbyteof(keccakIntList(V), 30, 32)
  135. : nthbyteof(keccakIntList(V), 31, 32)
  136. : .WordStack ) => keccakIntList(V)
  137.  
  138.  
  139. rule ACCTCODE in SetItem( 1 )
  140. SetItem ( 2 )
  141. SetItem ( 3 )
  142. SetItem ( 4 )
  143. SetItem ( 5 )
  144. SetItem ( 6 )
  145. SetItem ( 7 )
  146. SetItem ( 8 )
  147. => false
  148. requires 9 <=Int ACCTCODE
  149.  
  150.  
  151. // for terms came from bytecode not via #hashedLocation
  152. rule keccak(WS) => keccakIntList(byteStack2IntList(WS))
  153. requires ( notBool #isConcrete(WS) )
  154. // andBool ( #sizeWordStack(WS) ==Int 32 orBool #sizeWordStack(WS) ==Int 64 )
  155.  
  156. rule 0 <=Int keccakIntList(N) => true
  157. rule keccaktIntList(N) <Int pow256 => true
  158.  
  159.  
  160. rule #padToWidth(32, #asByteStack( #unsigned(V) )) => #asByteStackInWidth( #unsigned(V), 32)
  161. requires #rangeSInt(256, V)
  162.  
  163.  
  164. rule #padToWidth(32, #asByteStack(V)) => #asByteStackInWidth(V, 32)
  165. requires 0 <=Int V andBool V <Int pow256
  166.  
  167.  
  168. rule #padToWidth(32, #asByteStack( keccakIntList (V) )) => #asByteStackInWidth( keccakIntList (V), 32)
  169.  
  170.  
  171.  
  172.  
  173. // for Vyper
  174. rule #padToWidth(N, #asByteStack(#asWord(WS))) => WS
  175. requires #noOverflow(WS) andBool N ==Int #sizeWordStack(WS)
  176.  
  177. // for Solidity
  178. rule #asWord(WS) /Int D => #asWord(#take(#sizeWordStack(WS) -Int log256Int(D), WS))
  179. requires D modInt 256 ==Int 0 andBool D >=Int 0
  180. andBool #sizeWordStack(WS) >=Int log256Int(D)
  181. andBool #noOverflow(WS)
  182.  
  183. syntax Bool ::= #noOverflow ( WordStack ) [function]
  184. | #noOverflowAux ( WordStack ) [function]
  185. // -------------------------------------------------------
  186. rule #noOverflow(WS) => #sizeWordStack(WS) <=Int 32 andBool #noOverflowAux(WS)
  187.  
  188. rule #noOverflowAux(W : WS) => 0 <=Int W andBool W <Int 256 andBool #noOverflowAux(WS)
  189. rule #noOverflowAux(.WordStack) => true
  190.  
  191. syntax WordStack ::= #asByteStackInWidth ( Int, Int ) [function]
  192. | #asByteStackInWidthaux ( Int, Int, Int, WordStack ) [function]
  193. // -----------------------------------------------------------------------------------
  194. rule #asByteStackInWidth(X, N) => #asByteStackInWidthaux(X, N -Int 1, N, .WordStack)
  195.  
  196. rule #asByteStackInWidthaux(X, I, N, WS) => #asByteStackInWidthaux(X, I -Int 1, N, nthbyteof(X, I, N) : WS) when I >Int 0
  197. rule #asByteStackInWidthaux(X, 0, N, WS) => nthbyteof(X, 0, N) : WS
  198.  
  199.  
  200.  
  201.  
  202.  
  203.  
  204.  
  205.  
  206.  
  207.  
  208. rule 0 +Int N => N
  209. rule N +Int 0 => N
  210.  
  211. rule N -Int 0 => N
  212.  
  213. rule 1 *Int N => N
  214. rule N *Int 1 => N
  215. rule 0 *Int _ => 0
  216. rule _ *Int 0 => 0
  217.  
  218. rule N /Int 1 => N
  219.  
  220. rule 0 |Int N => N
  221. rule N |Int 0 => N
  222. rule N |Int N => N
  223.  
  224. rule 0 &Int N => 0
  225. rule N &Int 0 => 0
  226. rule N &Int N => N
  227.  
  228.  
  229.  
  230.  
  231.  
  232.  
  233.  
  234. rule (I1 +Int I2) +Int I3 => I1 +Int (I2 +Int I3) when #isConcrete(I2) andBool #isConcrete(I3)
  235. rule (I1 +Int I2) -Int I3 => I1 +Int (I2 -Int I3) when #isConcrete(I2) andBool #isConcrete(I3)
  236. rule (I1 -Int I2) +Int I3 => I1 -Int (I2 -Int I3) when #isConcrete(I2) andBool #isConcrete(I3)
  237. rule (I1 -Int I2) -Int I3 => I1 -Int (I2 +Int I3) when #isConcrete(I2) andBool #isConcrete(I3)
  238.  
  239. rule I1 &Int (I2 &Int I3) => (I1 &Int I2) &Int I3 when #isConcrete(I1) andBool #isConcrete(I2)
  240.  
  241. // 0xffff...f &Int N = N
  242. rule MASK &Int N => N requires MASK ==Int (2 ^Int (log2Int(MASK) +Int 1)) -Int 1 // MASK = 0xffff...f
  243. andBool 0 <=Int N andBool N <=Int MASK
  244.  
  245. // for gas calculation
  246. rule A -Int (#if C #then B1 #else B2 #fi) => #if C #then (A -Int B1) #else (A -Int B2) #fi
  247. rule (#if C #then B1 #else B2 #fi) -Int A => #if C #then (B1 -Int A) #else (B2 -Int A) #fi
  248.  
  249. rule (#if C #then B1 #else B2 #fi) >Int A => true
  250. requires B1 >Int A andBool B2 >Int A
  251.  
  252. rule (#if C #then B1 #else B2 #fi) >=Int A => true
  253. requires B1 >=Int A andBool B2 >=Int A
  254.  
  255. rule A -Int A => 0
  256.  
  257. rule bool2Word(A) |Int bool2Word(B) => bool2Word(A orBool B)
  258. rule bool2Word(A) &Int bool2Word(B) => bool2Word(A andBool B)
  259.  
  260. rule bool2Word(A) ==K 0 => notBool(A)
  261. rule bool2Word(A) ==K 1 => A
  262. rule bool2Word(A) =/=K 0 => A
  263. rule bool2Word(A) =/=K 1 => notBool(A)
  264.  
  265. rule chop(bool2Word(B)) => bool2Word(B)
  266.  
  267.  
  268.  
  269.  
  270.  
  271. rule 0 <=Int chop(V) => true
  272. rule chop(V) <Int pow256 => true
  273.  
  274. rule 0 <=Int keccak(V) => true
  275. rule keccak(V) <Int pow256 => true
  276.  
  277. rule 0 <=Int X &Int Y => true requires 0 <=Int X andBool X <Int pow256 andBool 0 <=Int Y andBool Y <Int pow256
  278. rule X &Int Y <Int pow256 => true requires 0 <=Int X andBool X <Int pow256 andBool 0 <=Int Y andBool Y <Int pow256
  279.  
  280.  
  281.  
  282.  
  283.  
  284. rule chop(I) => I requires 0 <=Int I andBool I <Int pow256
  285.  
  286.  
  287.  
  288.  
  289. rule #sizeWordStack ( _ , _ ) >=Int 0 => true [smt-lemma]
  290. rule #sizeWordStack ( WS , N:Int )
  291. => #sizeWordStack ( WS , 0 ) +Int N
  292. requires N =/=K 0
  293. [lemma]
  294.  
  295. rule chop(#unsigned(W)) => #unsigned(W)
  296. requires #rangeSInt(256, W)
  297.  
  298. rule #signed(#unsigned(W)) => W
  299. requires #rangeSInt(256, W)
  300.  
  301. rule #unsigned(#signed(W)) => W
  302. requires #rangeUInt(256, W)
  303.  
  304. rule W0 s<Word W1 => #signed(W0) <Word #signed(W1)
  305.  
  306. rule #signed(X) ==K #signed(Y) => X ==K Y requires #rangeUInt(256,X) orBool #rangeUInt(256,Y)
  307. rule #unsigned(X) ==K #unsigned(Y) => X ==K Y requires #rangeSInt(256,X) orBool #rangeSInt(256,Y)
  308.  
  309.  
  310. rule A modInt pow160 => A
  311. requires #rangeAddress(A)
  312.  
  313. syntax Bool ::= #notPrecompileAddress ( Int ) [function]
  314. // ---------------------------------------
  315. rule #notPrecompileAddress ( X ) => 9 <=Int X andBool #rangeAddress(X)
  316.  
  317. // ABSTRACT SEMANTICS.k
  318.  
  319. rule <k> LT W0 W1 => bool2Word(W0 <Int W1) ~> #push ... </k> [trusted]
  320. rule <k> GT W0 W1 => bool2Word(W0 >Int W1) ~> #push ... </k> [trusted]
  321. rule <k> EQ W0 W1 => bool2Word(W0 ==Int W1) ~> #push ... </k> [trusted]
  322. rule <k> ISZERO W => bool2Word(W ==Int 0 ) ~> #push ... </k> [trusted]
  323.  
  324.  
  325. //RULES MUST USE ==K and not ==Int
  326. //Warning: assumes injective hashing
  327. rule keccakIntList(A B .IntList) ==K keccakIntList(C D .IntList) => A ==Int C andBool B ==Int D
  328. rule keccakIntList(A B .IntList) =/=K keccakIntList(C D .IntList) => A =/=Int C orBool B =/=Int D
  329.  
  330. rule keccakIntList(A B C .IntList) ==K keccakIntList(D E F .IntList) => A ==Int D andBool B ==Int E andBool C ==Int F
  331. rule keccakIntList(A B C .IntList) =/=K keccakIntList(D E F .IntList) => A =/=Int D orBool B =/=Int E orBool C =/=Int F
  332.  
  333.  
  334. rule keccakIntList(C) ==K A => false
  335. requires 0 <=Int A andBool A <=Int 20
  336. rule keccakIntList(C) =/=K A => true
  337. requires 0 <=Int A andBool A <=Int 20
  338.  
  339. rule keccakIntList(C) +Int B ==K A => false
  340. requires 0 <=Int A andBool A <=Int 20
  341. andBool 0 <=Int B andBool B <=Int 20
  342. rule keccakIntList(C) +Int B =/=K A => true
  343. requires 0 <=Int A andBool A <=Int 20
  344. andBool 0 <=Int B andBool B <=Int 20
  345.  
  346. rule A ==K keccakIntList(C) +Int B => false
  347. requires 0 <=Int A andBool A <=Int 20
  348. andBool 0 <=Int B andBool B <=Int 20
  349. rule A =/=K keccakIntList(C) +Int B => true
  350. requires 0 <=Int A andBool A <=Int 20
  351. andBool 0 <=Int B andBool B <=Int 20
  352.  
  353. rule keccakIntList(C) +Int B ==K keccakIntList(A) => false
  354. requires 0 <=Int B andBool B <=Int 20
  355. rule keccakIntList(C) +Int B =/=K keccakIntList(A) => true
  356. requires 0 <=Int B andBool B <=Int 20
  357.  
  358. rule keccakIntList(A) +Int B ==K keccakIntList(A) +Int C => false
  359. requires B =/=Int C
  360. rule keccakIntList(A) +Int B =/=K keccakIntList(A) +Int C => true
  361. requires B =/=Int C
  362.  
  363. rule keccakIntList(A) +Int B ==K keccakIntList(C) +Int D => false
  364. requires B =/=Int C
  365. rule keccakIntList(A) +Int B =/=K keccakIntList(C) +Int D => true
  366. requires B =/=Int C
  367.  
  368.  
  369. rule keccakIntList(A) ==K keccakIntList(C) +Int B => false
  370. requires 0 <=Int B andBool B <=Int 20
  371. rule keccakIntList(A) =/=K keccakIntList(C) +Int B => true
  372. requires 0 <=Int B andBool B <=Int 20
  373.  
  374.  
  375. rule A ==K keccakIntList(C) => false
  376. requires 0 <=Int A andBool A <=Int 20
  377. rule A =/=K keccakIntList(C)=> true
  378. requires 0 <=Int A andBool A <=Int 20
  379.  
  380.  
  381. // src/lemmas.k.md
  382.  
  383. // src/storage.md
  384.  
  385. syntax Int ::= "#Token.balances" "[" Int "]" [function]
  386. // -----------------------------------------------
  387. // doc: The token balance of `$0`
  388. rule #Token.balances[A] => #hashedLocation("Solidity", 0, A)
  389.  
  390. endmodule
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!