Skip to content

Instantly share code, notes, and snippets.

@livnev

livnev/tune-fail-tree

Created August 25, 2018 09:21
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save livnev/7d9a217b66474b3b090b06f6929a7fdb to your computer and use it in GitHub Desktop.
Save livnev/7d9a217b66474b3b090b06f6929a7fdb to your computer and use it in GitHub Desktop.
Download ZIP
wow such proof
Raw
tune-fail-tree
behaviour
HEAD DELTAC
├ 0 ¬( 0 < ABI_dink )
│ ├ 0 ¬( ABI_dink < 0 )
│ │ ├ 0 ¬( 0 < ABI_dart )
│ │ │ ├ 0 ✓ ¬( ABI_dart < 0 )
│ │ │ └ 1 ABI_dart < 0
│ │ │ ├ 0 Art_u + ABI_dart >= 0
│ │ │ │ ├ 0 Art_i + ABI_dart >= 0
│ │ │ │ │ ├ 0 ¬( #signed ( Rate ) < 0 )
│ │ │ │ │ │ ├ 0 Rate * ABI_dart >= minSInt256
│ │ │ │ │ │ │ ├ 0 ✓ Dai + Rate * ABI_dart >= 0
│ │ │ │ │ │ │ └ 1 ✓ ¬( Dai + Rate * ABI_dart >= 0 )
│ │ │ │ │ │ └ 1 ✓ ¬( Rate * ABI_dart >= minSInt256 )
│ │ │ │ │ └ 1 ✓ #signed ( Rate ) < 0
│ │ │ │ └ 1 ✓ ¬( Art_i + ABI_dart >= 0 )
│ │ │ └ 1 ✓ ¬( Art_u + ABI_dart >= 0 )
│ │ └ 1 0 < ABI_dart
│ │ ├ 0 ╭ Art_u + ABI_dart <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ │ │ ╰ 5
│ │ │ ├ 0 ╭ Art_i + ABI_dart <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ │ │ │ ╰ 5
│ │ │ │ ├ 0 ¬( #signed ( Rate ) < 0 )
│ │ │ │ │ ├ 0 Rate * ABI_dart <= maxSInt256
│ │ │ │ │ │ ├ 0 ✓ ╭ Dai + Rate * ABI_dart <= 115792089237316195423570985008687907853269984665640564039457584007913129
│ │ │ │ │ │ │ ╰ 639935
│ │ │ │ │ │ └ 1 ✓ ╭ ¬( Dai + Rate * ABI_dart <= 115792089237316195423570985008687907853269984665640564039457584007913129
│ │ │ │ │ │ ╰ 639935 )
│ │ │ │ │ └ 1 ✓ ¬( Rate * ABI_dart <= maxSInt256 )
│ │ │ │ └ 1 ✓ #signed ( Rate ) < 0
│ │ │ └ 1 ✓ ╭ ¬( Art_i + ABI_dart <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ │ ╰ 5 )
│ │ └ 1 ✓ ╭ ¬( Art_u + ABI_dart <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ ╰ 5 )
│ └ 1 ABI_dink < 0
│ ├ 0 Ink_u + ABI_dink >= 0
│ │ ├ 0 ¬( 0 < ABI_dart )
│ │ │ ├ 0 ¬( ABI_dart < 0 )
│ │ │ │ ├ 0 ✓ ╭ Gem_v - ABI_dink <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ │ │ │ ╰ 5
│ │ │ │ └ 1 ✓ ╭ ¬( Gem_v - ABI_dink <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ │ │ ╰ 5 )
│ │ │ └ 1 ABI_dart < 0
│ │ │ ├ 0 Art_u + ABI_dart >= 0
│ │ │ │ ├ 0 Art_i + ABI_dart >= 0
│ │ │ │ │ ├ 0 ╭ Gem_v - ABI_dink <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ │ │ │ │ │ ╰ 5
│ │ │ │ │ │ ├ 0 ¬( #signed ( Rate ) < 0 )
│ │ │ │ │ │ │ ├ 0 Rate * ABI_dart >= minSInt256
│ │ │ │ │ │ │ │ ├ 0 ✓ Dai + Rate * ABI_dart >= 0
│ │ │ │ │ │ │ │ └ 1 ✓ ¬( Dai + Rate * ABI_dart >= 0 )
│ │ │ │ │ │ │ └ 1 ✓ ¬( Rate * ABI_dart >= minSInt256 )
│ │ │ │ │ │ └ 1 ✓ #signed ( Rate ) < 0
│ │ │ │ │ └ 1 ✓ ╭ ¬( Gem_v - ABI_dink <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ │ │ │ ╰ 5 )
│ │ │ │ └ 1 ✓ ¬( Art_i + ABI_dart >= 0 )
│ │ │ └ 1 ✓ ¬( Art_u + ABI_dart >= 0 )
│ │ └ 1 0 < ABI_dart
│ │ ├ 0 ╭ Art_u + ABI_dart <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ │ │ ╰ 5
│ │ │ ├ 0 ╭ Art_i + ABI_dart <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ │ │ │ ╰ 5
│ │ │ │ ├ 0 ╭ Gem_v - ABI_dink <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ │ │ │ │ ╰ 5
│ │ │ │ │ ├ 0 ¬( #signed ( Rate ) < 0 )
│ │ │ │ │ │ ├ 0 Rate * ABI_dart <= maxSInt256
│ │ │ │ │ │ │ ├ 0 ✓ ╭ Dai + Rate * ABI_dart <= 115792089237316195423570985008687907853269984665640564039457584007913129
│ │ │ │ │ │ │ │ ╰ 639935
│ │ │ │ │ │ │ └ 1 ✓ ╭ ¬( Dai + Rate * ABI_dart <= 115792089237316195423570985008687907853269984665640564039457584007913129
│ │ │ │ │ │ │ ╰ 639935 )
│ │ │ │ │ │ └ 1 ✓ ¬( Rate * ABI_dart <= maxSInt256 )
│ │ │ │ │ └ 1 ✓ #signed ( Rate ) < 0
│ │ │ │ └ 1 ✓ ╭ ¬( Gem_v - ABI_dink <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ │ │ ╰ 5 )
│ │ │ └ 1 ✓ ╭ ¬( Art_i + ABI_dart <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ │ ╰ 5 )
│ │ └ 1 ✓ ╭ ¬( Art_u + ABI_dart <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ ╰ 5 )
│ └ 1 ✓ ¬( Ink_u + ABI_dink >= 0 )
└ 1 0 < ABI_dink
├ 0 ╭ Ink_u + ABI_dink <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ ╰ 5
│ ├ 0 ¬( 0 < ABI_dart )
│ │ ├ 0 ¬( ABI_dart < 0 )
│ │ │ ├ 0 ✓ Gem_v - ABI_dink >= 0
│ │ │ └ 1 ✓ ¬( Gem_v - ABI_dink >= 0 )
│ │ └ 1 ABI_dart < 0
│ │ ├ 0 Art_u + ABI_dart >= 0
│ │ │ ├ 0 Art_i + ABI_dart >= 0
│ │ │ │ ├ 0 Gem_v - ABI_dink >= 0
│ │ │ │ │ ├ 0 ¬( #signed ( Rate ) < 0 )
│ │ │ │ │ │ ├ 0 Rate * ABI_dart >= minSInt256
│ │ │ │ │ │ │ ├ 0 ✓ Dai + Rate * ABI_dart >= 0
│ │ │ │ │ │ │ └ 1 ✓ ¬( Dai + Rate * ABI_dart >= 0 )
│ │ │ │ │ │ └ 1 ✓ ¬( Rate * ABI_dart >= minSInt256 )
│ │ │ │ │ └ 1 ✓ #signed ( Rate ) < 0
│ │ │ │ └ 1 ✓ ¬( Gem_v - ABI_dink >= 0 )
│ │ │ └ 1 ✓ ¬( Art_i + ABI_dart >= 0 )
│ │ └ 1 ✓ ¬( Art_u + ABI_dart >= 0 )
│ └ 1 0 < ABI_dart
│ ├ 0 ╭ Art_u + ABI_dart <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ │ ╰ 5
│ │ ├ 0 ╭ Art_i + ABI_dart <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ │ │ ╰ 5
│ │ │ ├ 0 Gem_v - ABI_dink >= 0
│ │ │ │ ├ 0 ¬( #signed ( Rate ) < 0 )
│ │ │ │ │ ├ 0 Rate * ABI_dart <= maxSInt256
│ │ │ │ │ │ ├ 0 ✓ ╭ Dai + Rate * ABI_dart <= 115792089237316195423570985008687907853269984665640564039457584007913129
│ │ │ │ │ │ │ ╰ 639935
│ │ │ │ │ │ └ 1 ✓ ╭ ¬( Dai + Rate * ABI_dart <= 115792089237316195423570985008687907853269984665640564039457584007913129
│ │ │ │ │ │ ╰ 639935 )
│ │ │ │ │ └ 1 ✓ ¬( Rate * ABI_dart <= maxSInt256 )
│ │ │ │ └ 1 ✓ #signed ( Rate ) < 0
│ │ │ └ 1 ✓ ¬( Gem_v - ABI_dink >= 0 )
│ │ └ 1 ✓ ╭ ¬( Art_i + ABI_dart <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ │ ╰ 5 )
│ └ 1 ✓ ╭ ¬( Art_u + ABI_dart <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
│ ╰ 5 )
└ 1 ✓ ╭ ¬( Ink_u + ABI_dink <= 11579208923731619542357098500868790785326998466564056403945758400791312963993
╰ 5 )
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment