Created
August 1, 2019 09:26
-
-
Save mhhf/ab7413af25cf840b2b7dcea07de10c3b to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
HEAD DELTAC | |
├ 0 ╭ ((((VCallDepth < 1024) AND ((Ward ==K 1) AND (notBool_((Tag ==K 0)) AND ((Art_iu <= pow255) AND ( | |
│ │ │ ((Rate_i * Art_iu) <= pow255) AND (((minSInt256 <= Rate_i) AND (Rate_i <= maxSInt256)) AND (((0 <= ( | |
│ │ │ ((Rate_i * Art_iu) / #Ray) * Tag)) AND ((((Rate_i * Art_iu) / #Ray) * Tag) <= maxUInt256)) AND (((0 | |
│ │ │ <= (Art_i - Art_iu)) AND ((Art_i - Art_iu) <= maxUInt256)) AND (((0 <= (Gem_a + ((((Art_iu * Rate_i) | |
│ │ │ / #Ray) * Tag) / #Ray))) AND ((Gem_a + ((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray)) <= maxUInt256)) | |
│ │ │ AND (((0 <= (Awe + (Art_iu * Rate_i))) AND ((Awe + (Art_iu * Rate_i)) <= maxUInt256)) AND ((0 <= (V | |
│ │ │ ice + (Art_iu * Rate_i))) AND ((Vice + (Art_iu * Rate_i)) <= maxUInt256)))))))))))) ==K false) AND ( | |
│ │ ╰ VCallValue ==K 0)) | |
│ ├ 0 ((Tag ==K 0) ==K false) | |
│ │ ├ 0 ❌ (_orBool_((0 > ACCT_ID_balance), (VCallDepth >= 1024))) | |
│ │ └ 1 (((VCallDepth >= 1024) ==K false) AND ((0 > ACCT_ID_balance) ==K false)) | |
│ │ ├ 0 ╭ ((((VCallDepth < 1024) AND ((Ward ==K 1) AND (notBool_((Tag ==K 0)) AND ((Art_iu <= pow255) AND ( | |
│ │ │ │ │ ((0 <= (Art_i - Art_iu)) AND ((Art_i - Art_iu) <= maxUInt256)) AND (((0 <= Gem_a) AND (Gem_a <= maxU | |
│ │ │ │ │ Int256)) AND (((0 <= Awe) AND (Awe <= maxUInt256)) AND ((0 <= Vice) AND (Vice <= maxUInt256))))))))) | |
│ │ │ │ ╰ ==K false) AND (((Ink_iu > 0)) AND (Rate_i ==K 0))) | |
│ │ │ ├ 0 ((Art_iu <= pow255)) | |
│ │ │ │ ├ 0 ❌ ╭ ((((VCallDepth < 1024) AND (notBool_((Tag ==K 0)) AND ((Art_iu <= pow255) AND (((0 <= (Art_i - Ar | |
│ │ │ │ │ │ t_iu)) AND ((Art_i - Art_iu) <= maxUInt256)) AND (((0 <= Gem_a) AND (Gem_a <= maxUInt256)) AND (((0 | |
│ │ │ │ │ │ <= Awe) AND (Awe <= maxUInt256)) AND ((0 <= Vice) AND (Vice <= maxUInt256)))))))) ==K false) AND (Wa | |
│ │ │ │ │ ╰ rd ==K 1)) | |
│ │ │ │ └ 1 ❌ ((Ward ==K 1) ==K false) | |
│ │ │ └ 1 ❌ ((pow255 < Art_iu)) | |
│ │ └ 1 ((Rate_i ==K 0) ==K false) | |
│ │ ├ 0 ((((Art_iu * Rate_i) <= maxUInt256)) AND ((0 <= (Art_iu * Rate_i)))) | |
│ │ │ ├ 0 ╭ ((((((Art_iu * Rate_i) / #Ray) * Tag) <= maxUInt256)) AND ((0 <= (((Art_iu * Rate_i) / #Ray) * Ta | |
│ │ │ │ │ ╰ g)))) | |
│ │ │ │ ├ 0 ((Art_iu <= pow255)) | |
│ │ │ │ │ ├ 0 ╭ ((((VCallDepth < 1024) AND (notBool_((Tag ==K 0)) AND ((Art_iu <= pow255) AND (((Rate_i * Art_iu) | |
│ │ │ │ │ │ │ │ <= pow255) AND (((minSInt256 <= Rate_i) AND (Rate_i <= maxSInt256)) AND (((0 <= (((Rate_i * Art_iu) | |
│ │ │ │ │ │ │ │ / #Ray) * Tag)) AND ((((Rate_i * Art_iu) / #Ray) * Tag) <= maxUInt256)) AND (((0 <= (Art_i - Art_iu | |
│ │ │ │ │ │ │ │ )) AND ((Art_i - Art_iu) <= maxUInt256)) AND (((0 <= (Gem_a + ((((Art_iu * Rate_i) / #Ray) * Tag) / | |
│ │ │ │ │ │ │ │ #Ray))) AND ((Gem_a + ((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray)) <= maxUInt256)) AND (((0 <= (Awe | |
│ │ │ │ │ │ │ │ + (Art_iu * Rate_i))) AND ((Awe + (Art_iu * Rate_i)) <= maxUInt256)) AND ((0 <= (Vice + (Art_iu * Ra | |
│ │ │ │ │ │ │ ╰ te_i))) AND ((Vice + (Art_iu * Rate_i)) <= maxUInt256))))))))))) ==K false) AND (Ward ==K 1)) | |
│ │ │ │ │ │ ├ 0 ((((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray) <= 0)) | |
│ │ │ │ │ │ │ ├ 0 ❌ ((Art_iu <= 0)) | |
│ │ │ │ │ │ │ └ 1 ((0 < Art_iu)) | |
│ │ │ │ │ │ │ ├ 0 ((0 <= (Art_i - Art_iu))) | |
│ │ │ │ │ │ │ │ ├ 0 ❌ (((Awe + (Rate_i * Art_iu)) <= maxUInt256)) | |
│ │ │ │ │ │ │ │ └ 1 ❌ ((maxUInt256 < (Awe + (Rate_i * Art_iu)))) | |
│ │ │ │ │ │ │ └ 1 ❌ (((Art_i - Art_iu) < 0)) | |
│ │ │ │ │ │ └ 1 ((0 < ((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray))) | |
│ │ │ │ │ │ ├ 0 ((0 <= (Art_i - Art_iu))) | |
│ │ │ │ │ │ │ ├ 0 (((Rate_i <= maxSInt256)) AND ((minSInt256 <= Rate_i))) | |
│ │ │ │ │ │ │ │ ├ 0 ╭ (#sgnInterp((sgn(chop((Rate_i * #unsigned((0 - Art_iu))))) * -1), (abs(chop((Rate_i * #unsigned(( | |
│ │ │ │ │ │ │ │ │ │ ╰ 0 - Art_iu))))) / Art_iu)) ==K Rate_i) | |
│ │ │ │ │ │ │ │ │ ├ 0 (((Gem_a + ((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray)) <= maxUInt256)) | |
│ │ │ │ │ │ │ │ │ │ ├ 0 ((#signed(chop((Rate_i * #unsigned((0 - Art_iu))))) <= 0)) | |
│ │ │ │ │ │ │ │ │ │ │ ├ 0 ╭ (((chop((Rate_i * #unsigned((0 - Art_iu)))) <= maxSInt256)) AND ((minSInt256 <= chop((Rate_i * #u | |
│ │ │ │ │ │ │ │ │ │ │ │ ╰ nsigned((0 - Art_iu))))))) | |
│ │ │ │ │ │ │ │ │ │ │ └ 1 ╭ (((minSInt256 <= chop((Rate_i * #unsigned((0 - Art_iu))))) AND (chop((Rate_i * #unsigned((0 - Art | |
│ │ │ │ │ │ │ │ │ │ │ │ ╰ _iu)))) <= maxSInt256)) ==K false) | |
│ │ │ │ │ │ │ │ │ │ │ ├ 0 ((Awe <= (Awe -W chop((Rate_i * #unsigned((0 - Art_iu))))))) | |
│ │ │ │ │ │ │ │ │ │ │ │ ├ 0 ((Vice <= (Vice -W chop((Rate_i * #unsigned((0 - Art_iu))))))) | |
│ │ │ │ │ │ │ │ │ │ │ │ └ 1 ❌ (((Vice -W chop((Rate_i * #unsigned((0 - Art_iu))))) < Vice)) | |
│ │ │ │ │ │ │ │ │ │ │ └ 1 ❌ (((Awe -W chop((Rate_i * #unsigned((0 - Art_iu))))) < Awe)) | |
│ │ │ │ │ │ │ │ │ │ └ 1 ((0 < #signed(chop((Rate_i * #unsigned((0 - Art_iu))))))) | |
│ │ │ │ │ │ │ │ │ └ 1 ❌ ((maxUInt256 < (Gem_a + ((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray)))) | |
│ │ │ │ │ │ │ │ └ 1 ❌ ╭ ((#sgnInterp((sgn(chop((Rate_i * #unsigned((0 - Art_iu))))) * -1), (abs(chop((Rate_i * #unsigned( | |
│ │ │ │ │ │ │ │ ╰ (0 - Art_iu))))) / Art_iu)) ==K Rate_i) ==K false) | |
│ │ │ │ │ │ │ └ 1 ❌ (((minSInt256 <= Rate_i) AND (Rate_i <= maxSInt256)) ==K false) | |
│ │ │ │ │ │ └ 1 ❌ (((Art_i - Art_iu) < 0)) | |
│ │ │ │ │ └ 1 ❌ ((Ward ==K 1) ==K false) | |
│ │ │ │ └ 1 ❌ ((pow255 < Art_iu)) | |
│ │ │ └ 1 ❌ ╭ (((0 <= (((Art_iu * Rate_i) / #Ray) * Tag)) AND ((((Art_iu * Rate_i) / #Ray) * Tag) <= maxUInt256 | |
│ │ │ ╰ )) ==K false) | |
│ │ └ 1 ❌ (((0 <= (Art_iu * Rate_i)) AND ((Art_iu * Rate_i) <= maxUInt256)) ==K false) | |
│ └ 1 ❌ (((Ink_iu > 0)) AND (Tag ==K 0)) | |
└ 1 ❌ ((VCallValue ==K 0) ==K false) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment