SHARE
TWEET

Untitled




Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
- (set-option :auto-config false)
- (set-option :smt.mbqi false)
- ;(set-option :smt.mbqi.max_iterations 15)
- ;; pow256 and pow255
- (define-fun pow256 () Int
- 115792089237316195423570985008687907853269984665640564039457584007913129639936)
- (define-fun pow255 () Int
- 57896044618658097711785492504343953926634992332820282019728792003956564819968)
- ;; weird declaration trick (doesn't seem to be needed currently)
- ;; (declare-fun pow256 () Int)
- ;; (assert (>= pow256 115792089237316195423570985008687907853269984665640564039457584007913129639936))
- ;; (assert (<= pow256 115792089237316195423570985008687907853269984665640564039457584007913129639936))
- ;; signed word arithmetic definitions:
- ;; integer to word:
- (define-fun unsigned ((x Int)) Int
- (if (>= x 0)
- x
- (+ x pow256)))
- ;; word to integer
- (define-fun signed ((x Int)) Int
- (if (< x pow255)
- x
- (- x pow256)))
- ;; signed_abs
- (define-fun signed_abs ((x Int)) Int
- (if (< x pow255)
- x
- (- pow256 x)))
- ;; signed_sgn
- (define-fun signed_sgn ((x Int)) Int
- (if (< x pow255)
- 1
- -1))
- ;; smt_rpow
- (declare-fun smt_rpow (Int Int Int Int) Int)
- (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)))))
- (assert (forall ((z1 Int) (z2 Int) (x1 Int) (y1 Int) (x2 Int) (y2 Int) (b1 Int) (b2 Int))
- (!
- (=> (and (<= z1 z2) (<= x1 x2) (<= y1 y2) (<= b1 b2))
- (<= (smt_rpow z1 x1 y1 b1) (smt_rpow z2 x2 y2 b2))
- )
- :pattern ((smt_rpow z1 x1 y1 b1) (smt_rpow z2 x2 y2 b2))
- )
- ))
- (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)))))
- (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)))))
- (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)))))
- (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)))))
- ;
- ; end of prelude
- ;
- (declare-sort IntList)
- (declare-sort Bytes)
- (declare-sort WordStack)
- (declare-fun sizeWordStackAux (WordStack Int) Int)
- (declare-fun word_mod (Int Int) Int)
- (declare-fun word_plus (Int Int) Int)
- (declare-fun word_sub (Int Int) Int)
- (declare-fun smt_keccakIntList (IntList) Int)
- (declare-fun lengthBytesAux (Bytes Int) Int)
- (declare-fun sizeWordStack (WordStack) Int)
- (declare-fun smt_keccak (WordStack) Int)
- (declare-fun asByteStack (Int WordStack) WordStack)
- (declare-fun word_div (Int Int) Int)
- (declare-fun chop (Int) Int)
- (declare-fun lengthBytes (Bytes) Int)
- (declare-fun smt_nthbyteof (Int Int Int) Int)
- (declare-fun word_times (Int Int) Int)
- (declare-fun asWord (WordStack) Int)
- (declare-fun expFunc (Int Int) Int)
- (assert (forall ((|_125_R_I| Int)) (= (chop |_125_R_I|) (mod |_125_R_I| pow256))))
- (assert (forall ((|_393_R__533| Int)(|_392_R__532| WordStack)) (= (>= (sizeWordStackAux |_392_R__532| |_393_R__533|) 0) true)))
- (declare-fun |_1961_ABI_wad| () Int)
- (declare-fun |_2007_Vat_balance| () Int)
- (declare-fun |_1952_ORIGIN_ID| () Int)
- (declare-fun |_1962_ACCT_ID| () Int)
- (declare-fun |_1954_Dai_dst| () Int)
- (declare-fun |_1965_Vat| () Int)
- (declare-fun |_1964_Can| () Int)
- (declare-fun |_1953_ACCT_ID_balance| () Int)
- (declare-fun |_2008_VCallDepth| () Int)
- (declare-fun |_1967_VGas| () Int)
- (declare-fun |_1966_TIME| () Int)
- (declare-fun |_1955_Dai_src| () Int)
- (declare-fun |_1959_ABI_dst| () Int)
- (declare-fun |_2012_CALLER_ID| () Int)
- (declare-fun |_279753_| () Bool)
- (declare-fun |_279755_| () Bool)
- (declare-fun |_279752_| () Bool)
- (declare-fun |_279756_| () Bool)
- (declare-fun |_279754_| () Bool)
- (declare-fun |_1869_Dai_src| () Int)
- (assert (and (and
- (= (<= 0 |_1961_ABI_wad|) true)
- (= _279752_ false)
- (= (<= |_2012_CALLER_ID| 1461501637330902918203684832716283019655932542975) true)
- (= (<= (+ |_1954_Dai_dst| (* 1000000000000000000000000000 |_1961_ABI_wad|)) 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
- (= (<= 0 |_1965_Vat|) true)
- (= (<= 0 |_1952_ORIGIN_ID|) true)
- (= (<= 9 |_1962_ACCT_ID|) true)
- (= (<= |_1966_TIME| 281474976710655) true)
- (= (= |_1961_ABI_wad| 0) false)
- (= (<= 0 |_2012_CALLER_ID|) true)
- (= (<= (- |_1955_Dai_src| (* 1000000000000000000000000000 |_1961_ABI_wad|)) 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
- (= (<= |_2008_VCallDepth| 1024) true)
- (= (<= |_1954_Dai_dst| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
- (= (<= 0 |_2007_Vat_balance|) true)
- (= (<= |_1961_ABI_wad| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
- (= (<= |_1959_ABI_dst| 1461501637330902918203684832716283019655932542975) true)
- (= (<= 0 |_1955_Dai_src|) true)
- (= (<= 0 |_1964_Can|) true)
- (= _279753_ false)
- (= (= |_1962_ACCT_ID| |_1965_Vat|) false)
- (= (<= -57896044618658097711785492504343953926634992332820282019728792003956564819968 (* 1000000000000000000000000000 |_1961_ABI_wad|)) true)
- (= (<= 0 |_1959_ABI_dst|) true)
- (= (<= 0 (+ |_1954_Dai_dst| (* 1000000000000000000000000000 |_1961_ABI_wad|))) true)
- (= _279754_ false)
- (= (<= |_1953_ACCT_ID_balance| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
- (= (<= 9 |_1965_Vat|) true)
- (= (>= |_1967_VGas| 3000000) true)
- (= _279755_ false)
- (= (<= 0 |_1954_Dai_dst|) true)
- (= (< |_2008_VCallDepth| 1024) true)
- (= (<= (* 1000000000000000000000000000 |_1961_ABI_wad|) 57896044618658097711785492504343953926634992332820282019728792003956564819967) true)
- (= (<= 0 (- |_1955_Dai_src| (* 1000000000000000000000000000 |_1961_ABI_wad|))) true)
- (= (<= |_1952_ORIGIN_ID| 1461501637330902918203684832716283019655932542975) true)
- (= (<= |_1965_Vat| 1461501637330902918203684832716283019655932542975) true)
- (= (<= 0 |_1962_ACCT_ID|) true)
- (= (<= 0 |_1966_TIME|) true)
- (= _279756_ false)
- (= (<= 0 |_1953_ACCT_ID_balance|) true)
- (= (<= |_1964_Can| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
- (= (<= |_1962_ACCT_ID| 1461501637330902918203684832716283019655932542975) true)
- (= (<= |_1955_Dai_src| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
- (= (<= |_2007_Vat_b1111728884 alance| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
- (= (= |_2012_CALLER_ID| |_1959_ABI_dst|) false))
- (not (and
- (= (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.