Skip to content

Instantly share code, notes, and snippets.

@mhhf
Created August 1, 2019 09:26
Show Gist options
  • Save mhhf/ab7413af25cf840b2b7dcea07de10c3b to your computer and use it in GitHub Desktop.
Save mhhf/ab7413af25cf840b2b7dcea07de10c3b to your computer and use it in GitHub Desktop.
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