SHARE
TWEET

Untitled

a guest Jan 23rd, 2019 64 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. (set-option :auto-config false)
  2. (set-option :smt.mbqi false)
  3. ;(set-option :smt.mbqi.max_iterations 15)
  4.  
  5. ;; pow256 and pow255
  6. (define-fun pow256 () Int
  7.   115792089237316195423570985008687907853269984665640564039457584007913129639936)
  8. (define-fun pow255 () Int
  9.   57896044618658097711785492504343953926634992332820282019728792003956564819968)
  10. ;; weird declaration trick (doesn't seem to be needed currently)
  11. ;; (declare-fun pow256 () Int)
  12. ;; (assert (>= pow256 115792089237316195423570985008687907853269984665640564039457584007913129639936))
  13. ;; (assert (<= pow256 115792089237316195423570985008687907853269984665640564039457584007913129639936))
  14.  
  15. ;; signed word arithmetic definitions:
  16. ;; integer to word:
  17. (define-fun unsigned ((x Int)) Int
  18.   (if (>= x 0)
  19.       x
  20.     (+ x pow256)))
  21.  
  22. ;; word to integer
  23. (define-fun signed ((x Int)) Int
  24.   (if (< x pow255)
  25.       x
  26.     (- x pow256)))
  27.  
  28. ;; signed_abs
  29. (define-fun signed_abs ((x Int)) Int
  30.   (if (< x pow255)
  31.       x
  32.     (- pow256 x)))
  33.  
  34. ;; signed_sgn
  35. (define-fun signed_sgn ((x Int)) Int
  36.   (if (< x pow255)
  37.       1
  38.     -1))
  39.  
  40. ;; smt_rpow
  41. (declare-fun smt_rpow (Int Int Int Int) Int)
  42. (assert (forall ((z Int) (x Int) (y Int) (b Int)) (! (=> (= y 1) (= (smt_rpow z x y b) (div (+ (* z x) (div b 2)) b))) :pattern ((smt_rpow z x y b)))))
  43.  
  44. (assert (forall ((z1 Int) (z2 Int) (x1 Int) (y1 Int) (x2 Int) (y2 Int) (b1 Int) (b2 Int))
  45.   (!
  46.     (=> (and (<= z1 z2) (<= x1 x2) (<= y1 y2) (<= b1 b2))
  47.       (<= (smt_rpow z1 x1 y1 b1) (smt_rpow z2 x2 y2 b2))
  48.     )
  49.     :pattern ((smt_rpow z1 x1 y1 b1) (smt_rpow z2 x2 y2 b2))
  50.   )
  51. ))
  52.  
  53. (assert (forall ((z Int) (x Int) (y Int) (b Int)) (! (=> (>= y 1) (>= (* (smt_rpow z x y b) b) (* z x))) :pattern ((smt_rpow z x y b)))))
  54. (assert (forall ((z Int) (x Int) (y Int) (b Int)) (! (=> (>= y 2) (>= (* (smt_rpow z x y b) b) (* x x))) :pattern ((smt_rpow z x y b)))))
  55.  
  56. (assert (forall ((z Int) (x Int) (y Int) (b Int)) (! (=> (>= y 1) (>= (* (smt_rpow z x y b) b) (+ (* z x) (div b 2)))) :pattern ((smt_rpow z x y b)))))
  57. (assert (forall ((z Int) (x Int) (y Int) (b Int)) (! (=> (>= y 2) (>= (* (smt_rpow z x y b) b) (+ (* x x) (div b 2)))) :pattern ((smt_rpow z x y b)))))
  58. ;
  59. ; end of prelude
  60. ;
  61. (declare-sort IntList)
  62. (declare-sort Bytes)
  63. (declare-sort WordStack)
  64. (declare-fun sizeWordStackAux (WordStack Int) Int)
  65. (declare-fun word_mod (Int Int) Int)
  66. (declare-fun word_plus (Int Int) Int)
  67. (declare-fun word_sub (Int Int) Int)
  68. (declare-fun smt_keccakIntList (IntList) Int)
  69. (declare-fun lengthBytesAux (Bytes Int) Int)
  70. (declare-fun sizeWordStack (WordStack) Int)
  71. (declare-fun smt_keccak (WordStack) Int)
  72. (declare-fun asByteStack (Int WordStack) WordStack)
  73. (declare-fun word_div (Int Int) Int)
  74. (declare-fun chop (Int) Int)
  75. (declare-fun lengthBytes (Bytes) Int)
  76. (declare-fun smt_nthbyteof (Int Int Int) Int)
  77. (declare-fun word_times (Int Int) Int)
  78. (declare-fun asWord (WordStack) Int)
  79. (declare-fun expFunc (Int Int) Int)
  80. (assert (forall ((|_125_R_I| Int)) (= (chop |_125_R_I|) (mod |_125_R_I| pow256))))
  81. (assert (forall ((|_393_R__533| Int)(|_392_R__532| WordStack)) (= (>= (sizeWordStackAux |_392_R__532| |_393_R__533|) 0) true)))
  82. (declare-fun |_1961_ABI_wad| () Int)
  83. (declare-fun |_2007_Vat_balance| () Int)
  84. (declare-fun |_1952_ORIGIN_ID| () Int)
  85. (declare-fun |_1962_ACCT_ID| () Int)
  86. (declare-fun |_1954_Dai_dst| () Int)
  87. (declare-fun |_1965_Vat| () Int)
  88. (declare-fun |_1964_Can| () Int)
  89. (declare-fun |_1953_ACCT_ID_balance| () Int)
  90. (declare-fun |_2008_VCallDepth| () Int)
  91. (declare-fun |_1967_VGas| () Int)
  92. (declare-fun |_1966_TIME| () Int)
  93. (declare-fun |_1955_Dai_src| () Int)
  94. (declare-fun |_1959_ABI_dst| () Int)
  95. (declare-fun |_2012_CALLER_ID| () Int)
  96. (declare-fun |_279753_| () Bool)
  97. (declare-fun |_279755_| () Bool)
  98. (declare-fun |_279752_| () Bool)
  99. (declare-fun |_279756_| () Bool)
  100. (declare-fun |_279754_| () Bool)
  101. (declare-fun |_1869_Dai_src| () Int)
  102. (assert (and (and
  103.  (= (<= 0 |_1961_ABI_wad|) true)
  104.  (= _279752_ false)
  105.  (= (<= |_2012_CALLER_ID| 1461501637330902918203684832716283019655932542975) true)
  106.  (= (<= (+ |_1954_Dai_dst| (* 1000000000000000000000000000 |_1961_ABI_wad|)) 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
  107.  (= (<= 0 |_1965_Vat|) true)
  108.  (= (<= 0 |_1952_ORIGIN_ID|) true)
  109.  (= (<= 9 |_1962_ACCT_ID|) true)
  110.  (= (<= |_1966_TIME| 281474976710655) true)
  111.  (= (= |_1961_ABI_wad| 0) false)
  112.  (= (<= 0 |_2012_CALLER_ID|) true)
  113.  (= (<= (- |_1955_Dai_src| (* 1000000000000000000000000000 |_1961_ABI_wad|)) 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
  114.  (= (<= |_2008_VCallDepth| 1024) true)
  115.  (= (<= |_1954_Dai_dst| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
  116.  (= (<= 0 |_2007_Vat_balance|) true)
  117.  (= (<= |_1961_ABI_wad| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
  118.  (= (<= |_1959_ABI_dst| 1461501637330902918203684832716283019655932542975) true)
  119.  (= (<= 0 |_1955_Dai_src|) true)
  120.  (= (<= 0 |_1964_Can|) true)
  121.  (= _279753_ false)
  122.  (= (= |_1962_ACCT_ID| |_1965_Vat|) false)
  123.  (= (<= -57896044618658097711785492504343953926634992332820282019728792003956564819968 (* 1000000000000000000000000000 |_1961_ABI_wad|)) true)
  124.  (= (<= 0 |_1959_ABI_dst|) true)
  125.  (= (<= 0 (+ |_1954_Dai_dst| (* 1000000000000000000000000000 |_1961_ABI_wad|))) true)
  126.  (= _279754_ false)
  127.  (= (<= |_1953_ACCT_ID_balance| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
  128.  (= (<= 9 |_1965_Vat|) true)
  129.  (= (>= |_1967_VGas| 3000000) true)
  130.  (= _279755_ false)
  131.  (= (<= 0 |_1954_Dai_dst|) true)
  132.  (= (< |_2008_VCallDepth| 1024) true)
  133.  (= (<= (* 1000000000000000000000000000 |_1961_ABI_wad|) 57896044618658097711785492504343953926634992332820282019728792003956564819967) true)
  134.  (= (<= 0 (- |_1955_Dai_src| (* 1000000000000000000000000000 |_1961_ABI_wad|))) true)
  135.  (= (<= |_1952_ORIGIN_ID| 1461501637330902918203684832716283019655932542975) true)
  136.  (= (<= |_1965_Vat| 1461501637330902918203684832716283019655932542975) true)
  137.  (= (<= 0 |_1962_ACCT_ID|) true)
  138.  (= (<= 0 |_1966_TIME|) true)
  139.  (= _279756_ false)
  140.  (= (<= 0 |_1953_ACCT_ID_balance|) true)
  141.  (= (<= |_1964_Can| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
  142.  (= (<= |_1962_ACCT_ID| 1461501637330902918203684832716283019655932542975) true)
  143.  (= (<= |_1955_Dai_src| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
  144.  (= (<= |_2007_Vat_b1111728884 alance| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
  145.  (= (= |_2012_CALLER_ID| |_1959_ABI_dst|) false))
  146. (not (and
  147.  (= (and (not (= (- |_1869_Dai_src| (* 1000000000000000000000000000 |_1961_ABI_wad|)) 0)) (= |_1869_Dai_src| 0)) false)))))(check-sat-using (or-else (using-params smt :random-seed 3 :timeout 1000) (using-params smt :random-seed 2 :timeout 2000) (using-params smt :random-seed 1)))
RAW Paste Data
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
 
Top