Skip to content

Instantly share code, notes, and snippets.

@mhhf

mhhf/gist:12899a225ed57fd332318af1f3314459

Created July 20, 2019 13:30
Show Gist options
  • Save mhhf/12899a225ed57fd332318af1f3314459 to your computer and use it in GitHub Desktop.
Save mhhf/12899a225ed57fd332318af1f3314459 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
├ 0 ╭ ((((May ==K 1) AND ((Live ==K 1) AND ((VCallDepth < 1024) AND (((0 <= (Base + Duty)) AND ((Base +
│ │ │ Duty) <= maxUInt256)) AND (((0 <= (TIME - Rho)) AND ((TIME - Rho) <= maxUInt256)) AND (((0 <= (#rpo
│ │ │ w(_,_,_,_)_RULES(#Ray, (Base + Duty), (TIME - Rho), #Ray) * Rate)) AND ((#rpow(_,_,_,_)_RULES(#Ray,
│ │ │ (Base + Duty), (TIME - Rho), #Ray) * Rate) <= maxUInt256)) AND (((0 <= ((#rpow(_,_,_,_)_RULES(#Ray,
│ │ │ (Base + Duty), (TIME - Rho), #Ray) * Rate) / #Ray)) AND (((#rpow(_,_,_,_)_RULES(#Ray, (Base + Duty),
│ │ │ (TIME - Rho), #Ray) * Rate) / #Ray) <= maxUInt256)) AND (((0 <= (((#rpow(_,_,_,_)_RULES(#Ray, (Base
│ │ │ + Duty), (TIME - Rho), #Ray) * Rate) / #Ray) - Rate)) AND ((((#rpow(_,_,_,_)_RULES(#Ray, (Base + Du
│ │ │ ty), (TIME - Rho), #Ray) * Rate) / #Ray) - Rate) <= maxUInt256)) AND (((0 <= (Rate + (((#rpow(_,_,_,
│ │ │ _)_RULES(#Ray, (Base + Duty), (TIME - Rho), #Ray) * Rate) / #Ray) - Rate))) AND ((Rate + (((#rpow(_,
│ │ │ _,_,_)_RULES(#Ray, (Base + Duty), (TIME - Rho), #Ray) * Rate) / #Ray) - Rate)) <= maxUInt256)) AND (
│ │ │ ((0 <= (Dai + (Art_i * (((#rpow(_,_,_,_)_RULES(#Ray, (Base + Duty), (TIME - Rho), #Ray) * Rate) / #R
│ │ │ ay) - Rate)))) AND ((Dai + (Art_i * (((#rpow(_,_,_,_)_RULES(#Ray, (Base + Duty), (TIME - Rho), #Ray)
│ │ │ * Rate) / #Ray) - Rate))) <= maxUInt256)) AND (((0 <= (Debt + (Art_i * (((#rpow(_,_,_,_)_RULES(#Ray
│ │ │ , (Base + Duty), (TIME - Rho), #Ray) * Rate) / #Ray) - Rate)))) AND ((Debt + (Art_i * (((#rpow(_,_,_
│ │ │ ,_)_RULES(#Ray, (Base + Duty), (TIME - Rho), #Ray) * Rate) / #Ray) - Rate))) <= maxUInt256)) AND (((
│ │ │ minSInt256 <= Rate) AND (Rate <= maxSInt256)) AND (((minSInt256 <= Art_i) AND (Art_i <= maxSInt256))
│ │ │ AND (((minSInt256 <= (((#rpow(_,_,_,_)_RULES(#Ray, (Base + Duty), (TIME - Rho), #Ray) * Rate) / #Ra
│ │ │ y) - Rate)) AND ((((#rpow(_,_,_,_)_RULES(#Ray, (Base + Duty), (TIME - Rho), #Ray) * Rate) / #Ray) -
│ │ │ Rate) <= maxSInt256)) AND ((minSInt256 <= (Art_i * (((#rpow(_,_,_,_)_RULES(#Ray, (Base + Duty), (TIM
│ │ │ E - Rho), #Ray) * Rate) / #Ray) - Rate))) AND ((Art_i * (((#rpow(_,_,_,_)_RULES(#Ray, (Base + Duty),
│ │ │ (TIME - Rho), #Ray) * Rate) / #Ray) - Rate)) <= maxSInt256)))))))))))))))) ==K false) AND (VCallVal
│ │ ╰ ue ==K 0))
│ ├ 0 ((Rho <= TIME))
│ │ ├ 0 ❌ (_orBool_((0 > ACCT_ID_balance), (VCallDepth >= 1024)))
│ │ └ 1 (((VCallDepth >= 1024) ==K false) AND ((0 > ACCT_ID_balance) ==K false))
│ │ ├ 0 (((Base + Duty) <= maxUInt256))
│ │ │ ├ 0 ╭ ((((May ==K 1) AND ((Live ==K 1) AND ((VCallDepth < 1024) AND (((0 <= (Base + Duty)) AND ((Base +
│ │ │ │ │ Duty) <= maxUInt256)) AND (((0 <= (TIME - Rho)) AND ((TIME - Rho) <= maxUInt256)) AND (((0 <= Dai)
│ │ │ │ │ AND (Dai <= maxUInt256)) AND (((0 <= Debt) AND (Debt <= maxUInt256)) AND ((minSInt256 <= Art_i) AND
│ │ │ │ ╰ (Art_i <= maxSInt256))))))))) ==K false) AND (Rate ==K 0))
│ │ │ └ 1 ((Rate ==K 0) ==K false)
│ │ │ ├ 0 ╭ ((((#rpow(_,_,_,_)_RULES(#Ray, (Base + Duty), (TIME - Rho), #Ray) * Rate) <= maxUInt256)) AND ((0
│ │ │ │ │ ╰ <= (#rpow(_,_,_,_)_RULES(#Ray, (Base + Duty), (TIME - Rho), #Ray) * Rate))))
│ │ │ │ ├ 0 (((Rate <= maxSInt256)) AND ((minSInt256 <= Rate)))
│ │ │ │ │ ├ 0 ╭ ((#asWord(#take(4, #take(32, #rangeAux(_[_:=_]_EVM-DATA(((0 |-> nthbyteof(ABI_ilk, 0, 32))
│ │ │ │ │ │ │ │ (1 |-> nthbyteof(ABI_ilk, 1, 32))
│ │ │ │ │ │ │ │ (2 |-> nthbyteof(ABI_ilk, 2, 32))
│ │ │ │ │ │ │ │ (3 |-> nthbyteof(ABI_ilk, 3, 32))
│ │ │ │ │ │ │ │ (4 |-> nthbyteof(ABI_ilk, 4, 32))
│ │ │ │ │ │ │ │ (5 |-> nthbyteof(ABI_ilk, 5, 32))
│ │ │ │ │ │ │ │ (6 |-> nthbyteof(ABI_ilk, 6, 32))
│ │ │ │ │ │ │ │ (7 |-> nthbyteof(ABI_ilk, 7, 32))
│ │ │ │ │ │ │ │ (8 |-> nthbyteof(ABI_ilk, 8, 32))
@mhhf
Copy link
Author

mhhf commented Jul 20, 2019 

  │ │   │   │ │ │ │                 │ (479 |-> nthbyteof(Vow, 27, 32))                                                                    
  │ │   │   │ │ │ │                 │ (480 |-> nthbyteof(Vow, 28, 32))                                                                    
  │ │   │   │ │ │ │                 │ (481 |-> nthbyteof(Vow, 29, 32))                                                                    
  │ │   │   │ │ │ │                 │ (482 |-> nthbyteof(Vow, 30, 32))                                                                    
  │ │   │   │ │ │ │                 │ (483 |-> nthbyteof(Vow, 31, 32))), 484, #padToWidth(32, #asByteStack((((#rpow(_,_,_,_)_RULES(#Ray   
  │ │   │   │ │ │ │                 ╰ , (Base + Duty), (TIME - Rho), #Ray) * Rate) / #Ray) -W Rate)))), 515, 100)))) < 2094874590))

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment