Skip to content

Latest commit

 

History

History
421 lines (304 loc) · 34.2 KB

lemmas.k.md

File metadata and controls

421 lines (304 loc) · 34.2 KB
Raw

Constants & Ranges

The evm-semantics only defines ranges and constants for a few solidity types. A couple of extra ones are required for these specs.

Powers

syntax Int ::= "pow32"
rule pow32 => 4294967296 [macro]

syntax Int ::= "pow112"
rule pow112 => 5192296858534827628530496329220096 [macro]

syntax Int ::= "pow224"
rule pow224 => 26959946667150639794667015087019630673637144422540572481103610249216 [macro]

Limits

syntax Int ::= "maxUInt32"
rule maxUInt32 => 4294967295 [macro]

syntax Int ::= "maxUInt112"
rule maxUInt112 => 5192296858534827628530496329220095 [macro]

syntax Int ::= "maxUInt224"
rule maxUInt224 => 26959946667150639794667015087019630673637144422540572481103610249215 [macro]

Inverses

syntax Int ::= "notMaxUInt112"
rule notMaxUInt112 => 115792089237316195423570985008687907853269979473343705504629955477416800419840 [macro]

syntax Int ::= "notMaxUInt160"
rule notMaxUInt160 => 115792089237316195423570985007226406215939081747436879206741300988257197096960 [macro]

syntax Int ::= "notMaxUInt224"
rule notMaxUInt224 => 115792089210356248756420345214020892766250353992003419616917011526809519390720 [macro]

Ranges

rule #rangeUInt(32, X) => #range(0 <= X <= maxUInt32)   [macro]
rule #rangeUInt(112, X) => #range(0 <= X <= maxUInt112) [macro]

Arithmetic

0 divided by anything is 0.

rule 0 /Int X => 0
requires notBool (X ==Int 0)

Helper for cleaner storage conditions.

syntax Int ::= "#min" "(" Int "," Int ")" [function]
rule #min(X, Y) => #if (X <Int Y) #then X #else Y #fi

Over/underflow Checks

These lemmas allow K to translate the under/overflow checking as implemented in the SafeMath.sol library to the logical #rangeUInt conditions expressed within the specs.

// sub
rule A -Word B <=Int A => #rangeUInt(256, A -Int B)
  requires #rangeUInt(256, A)
  andBool #rangeUInt(256, B)

// add
rule (chop(X +Int Y) >=Int X) => #rangeUInt(256, X +Int Y)
  requires #rangeUInt(256, X)
  andBool #rangeUInt(256, Y)

rule (X <=Int chop(X +Int Y)) => #rangeUInt(256, X +Int Y)
  requires #rangeUInt(256, X)
  andBool #rangeUInt(256, Y)

// mul
rule (chop(X *Int Y) /Int Y ==K X) => #rangeUInt(256, X *Int Y)
  requires #rangeUInt(256, X)
  andBool #rangeUInt(256, Y)

Bitwise Modulo

The solidity optimizer compiles block.time % 2**32 into TIME AND maxUInt32 instead of TIME MOD pow32. K is then unable to reason about the size of the result and so cannot apply further simplifications. We therefore rewrite it back to modInt pow32.

rule (maxUInt32 &Int X) => (X modInt pow32)

Repeated application of modInt pow32 can be simplified as follows. This lets us clean the storage conditions in a few specs.

rule ((X modInt pow32) modInt pow32) => (X modInt pow32)

Simplify idempotent applications of the modulo operation:

rule X modInt Y => X
  requires X <Int Y

Commutativity For Bitwise AND

K doesn't know that bitwise AND is commutative, so we give it a little helping hand.

rule (X &Int maxUInt32) => (maxUInt32 &Int X)
rule (X &Int maxUInt112) => (maxUInt112 &Int X)
rule (X &Int maxUInt160) => (maxUInt160 &Int X)
rule (X &Int notMaxUInt160) => (notMaxUInt160 &Int X)
rule (X &Int notMaxUInt224) => (notMaxUInt224 &Int X)

Factory pairs array

allPairs is an array which stores the address of every exchange pair created using the Factory.

pair0 represents the storage key of the first array element, the keccak hash of slot 3: keccak(uint256(3)).

syntax Int ::= "pair0"
rule pair0 => 87903029871075914254377627908054574944891091886930582284385770809450030037083 [macro]

Subsequent array elements are stored at a uint256 offset from this key: pair0 + index. The maximum allowable index before integer overflow is therefore maxUInt256 - pair0 and the valid index range is zero to max. index:

Valid index range: allPairs[0]...allPairs[maxUInt256 - pair0]

The maximum number of addresses that can be stored by the allPairs array is max. index plus one.

syntax Int ::= "maxPairs"
rule maxPairs => (maxUInt256 -Int pair0) +Int 1 [macro]

Important to note is that that there is no guarentee that the storage keys of allPairs will not collide with storage keys of getPair. We make the low probablity assumption that there will be no such collision in the factory.

rule N +Int pair0 => pair0 +Int N

rule keccakIntList(X) ==K pair0 +Int N => false
rule pair0 +Int N ==K keccakIntList(X) => false

rule keccak(X) ==K pair0 +Int N => false
rule pair0 +Int N ==K keccak(X) => false

We make the probabalistic assumption that the array will not overflow. This is not enforced by Solidity.

rule chop(pair0 +Int N) => pair0 +Int N
rule chop(N +Int pair0) => pair0 +Int N

Encode packed

The packing routine for abi.encodePacked(address, address) in the factory contract, formats both addresses with a left shift and then writes them as overlapping words to memory. The first 40 bytes is then read back from memory to provide the packed result. These rules handle the writing of the shifted addresses to memory and the reduction of the resulting byte array.

rule chop(A <<Int 96) => A <<Int 96
  requires #rangeAddress(A)

rule #padToWidth(32, #asByteStack(A <<Int 96))
  => #asByteStackInWidth(A <<Int 96, 32)

rule takeWordStack(20, #asByteStack(X)) =>
   ( nthbyteof(X, 0, 32)
   : nthbyteof(X, 1, 32)
   : nthbyteof(X, 2, 32)
   : nthbyteof(X, 3, 32)
   : nthbyteof(X, 4, 32)
   : nthbyteof(X, 5, 32)
   : nthbyteof(X, 6, 32)
   : nthbyteof(X, 7, 32)
   : nthbyteof(X, 8, 32)
   : nthbyteof(X, 9, 32)
   : nthbyteof(X, 10, 32)
   : nthbyteof(X, 11, 32)
   : nthbyteof(X, 12, 32)
   : nthbyteof(X, 13, 32)
   : nthbyteof(X, 14, 32)
   : nthbyteof(X, 15, 32)
   : nthbyteof(X, 16, 32)
   : nthbyteof(X, 17, 32)
   : nthbyteof(X, 18, 32)
   : nthbyteof(X, 19, 32)
   : .WordStack
   )

Packed Storage { uint32 uint112 uint112 }

Define the symbolic term representing packed storage:

syntax Int ::= "#WordPackUInt112UInt112UInt32" "(" Int "," Int "," Int ")" [function]

Reads

Solidity reads from packed storage locations with the following sequence:

  1. SLOAD to get the packed word
  2. Bitshift the word (e.g. /Int pow112)to bring the target of the read to the lower order (rightmost) side
  3. Bitwise AND with maxUInt for the target type to zero out the rest of the word (e.g. AND maxUInt32 for a uint32)

Example: read Reserve1

write balance0 to reserve0

These lemmas define the read operations specific to each packed storage location.

// Reserve0
rule maxUInt112 &Int #WordPackUInt112UInt112UInt32(A, B, C) => A

// Reserve1
rule maxUInt112 &Int (#WordPackUInt112UInt112UInt32(A, B, C) /Int pow112 ) => B

// BlockTimestampLast
rule #WordPackUInt112UInt112UInt32(A, B, C) /Int pow224 => C

Writes

Solidity writes to packed storage locations with the following sequence:

  1. SLOAD to get the current value of the word to be written
  2. Produce a bit mask by bitshifting maxUInt for the target type and taking the one's complement (e.g. NOT (maxUInt32 * pow224))
  3. AND the mask and the current value of storage to zero out the target region of the word
  4. Bitshift the new value into place and OR with the word produced by the previous step to write the new value to the target region
  5. SSTORE the new value of the word

Example: write Balance0 to Reserve0

write balance0 to reserve0

This produces some pretty gnarly expressions, and K needs help simplifying them. Note that multiple lemmas are needed below to match the cases where individual regions within the word are known to be zero. In this case K will simplify the 0 out of the expression, meaning we have to match on a few different expressions for each write operation.

The ordering of arguments differs between the various cases to match the bytecode produced by solidity.

Write reserve0

Mask target range to zero:

rule notMaxUInt112 &Int #WordPackUInt112UInt112UInt32(A, B, C) => #WordPackUInt112UInt112UInt32(0, B, C)

Write new value:

rule X |Int #WordPackUInt112UInt112UInt32(0, B, C) => #WordPackUInt112UInt112UInt32(X, B, C)
  requires #rangeUInt(112, X)
Write reserve1

The below constant represents not(maxUInt112 * pow112), in hex 0xffffffff0000000000000000000000000000ffffffffffffffffffffffffffff:

syntax Int ::= "notMaxUInt112xPow112"
rule notMaxUInt112xPow112 => 115792089210356248756420345214020892766250359184300278151744640057305848610815 [macro]

Mask target range to zero:

rule notMaxUInt112xPow112 &Int #WordPackUInt112UInt112UInt32(A, B, C) => #WordPackUInt112UInt112UInt32(A, 0, C)

Write new value:

rule (pow112 *Int X) |Int #WordPackUInt112UInt112UInt32(A, 0, C) => #WordPackUInt112UInt112UInt32(A, X, C)
  requires #rangeUInt(112, X)
Write blockTimestampLast

Mask target range to zero. Note that solidity uses a slightly different approach here than with the other words, and directly applies a mask of &Int pow224, instead of bitshifting and inverting as for reserve0 and reserve1. This only happens when the optimizer is enabled.

rule maxUInt224 &Int #WordPackUInt112UInt112UInt32(A, B, C) => #WordPackUInt112UInt112UInt32(A, B, 0)

write new value:

rule (X *Int pow224) |Int #WordPackUInt112UInt112UInt32(A, B, 0) => #WordPackUInt112UInt112UInt32(A, B, X)
  requires #rangeUInt(32, X)

Masking For Address Types (uint160)

Address type storage routine.

When writing addresses to storage, solidity masks the existing value to zero using the address type one's compliment and inserts the new value with a bitwise OR.

The inclusion of a rangeUInt constraint on existing address A allows for the _ (Junk bytes) expectation in storage specs.

// Overwrite A with B
rule ((notMaxUInt160 &Int A)) |Int B => B
  requires #rangeAddress(B)
  andBool (#rangeAddress(A) orBool #rangeUInt(256, A))

rule (B |Int (notMaxUInt160 &Int A)) => B
  requires #rangeAddress(B)
  andBool (#rangeAddress(A) orBool #rangeUInt(256, A))

Packed Words In Memory

Sometimes solidity will try and read a Word from memory containing unaligned data. In that case K needs help simplifying the resulting expressions:

masking:

// mask first four bytes to zero
rule maxUInt224 &Int #asWord(WS) => #asWord(#padToWidth(32, #drop(4, WS)))
  requires #sizeWordStack(WS) ==Int 32

// mask everything except first four bytes to zero
rule notMaxUInt224 &Int #asWord(WS) => #asWord(#padRightToWidth(32, #take(4, WS)))
  requires #sizeWordStack(WS) ==Int 32

writes:

// write first four bytes
rule X |Int #asWord(#padToWidth(32, WS)) => #asWord(#take(4, #asByteStack(X)) ++ WS)
  requires X &Int notMaxUInt224 ==Int X
  andBool #rangeUInt(256, X)
  andBool #sizeWordStack(WS) ==Int 28

Writes To Memory

We teach K how to write some expressions involving division to memory. This is used when writing the expression for fee liquidity into memory.

rule #padToWidth(32, #asByteStack(X /Int Y)) => #asByteStackInWidth(X /Int Y, 32)
  requires #rangeUInt(256, X)
  andBool #rangeUInt(256, Y)

#sqrt

Placeholder rewrite rule for Math.sqrt. This leaves the result of the call to Math.sqrt as symbolic for now, meaning that the specs are all assuming that Math.sqrt is correctly implemented and does what it is supposed to.

syntax Int ::= "#sqrt" "(" Int ")" [smtlib(smt_sqrt), smt-prelude, function]

rule <k> #execute ~> CONTINUATION => #execute ~> CONTINUATION </k>
     <program> UniswapV2Pair_bytecode </program>
     <jumpDests> #computeValidJumpDests(UniswapV2Pair_bytecode) </jumpDests>
     <wordStack> X : JumpTo : WS  =>  JumpTo : #sqrt(X) : WS </wordStack>
     <pc> 10360 => 10441 </pc>
  requires #rangeUInt(256, X)
  [trusted]

A concrete evaluation of sqrt(0) is provided to help simplification of a few terms.

rule #sqrt(0) => 0

UniswpV2Pair Bytecode

The full bytecode of the Pair is unfortunately required here to ensure for the place holder #sqrt rewrite rule to be applied only in UniswapV2Pair.

syntax WordStack ::= "UniswapV2Pair_bytecode"
rule UniswapV2Pair_bytecode => #parseByteStack("0x608060405234801561001057600080fd5b50600436106101b95760003560e01c80636a627842116100f9578063ba9a7a5611610097578063d21220a711610071578063d21220a7146105da578063d505accf146105e2578063dd62ed3e14610640578063fff6cae91461067b576101b9565b8063ba9a7a5614610597578063bc25cf771461059f578063c45a0155146105d2576101b9565b80637ecebe00116100d35780637ecebe00146104d757806389afcb441461050a57806395d89b4114610556578063a9059cbb1461055e576101b9565b80636a6278421461046957806370a082311461049c5780637464fc3d146104cf576101b9565b806323b872dd116101665780633644e515116101405780633644e51514610416578063485cc9551461041e5780635909c0d5146104595780635a3d549314610461576101b9565b806323b872dd146103ad57806330adf81f146103f0578063313ce567146103f8576101b9565b8063095ea7b311610197578063095ea7b3146103155780630dfe16811461036257806318160ddd14610393576101b9565b8063022c0d9f146101be57806306fdde03146102595780630902f1ac146102d6575b600080fd5b610257600480360360808110156101d457600080fd5b81359160208101359173ffffffffffffffffffffffffffffffffffffffff604083013516919081019060808101606082013564010000000081111561021857600080fd5b82018360208201111561022a57600080fd5b8035906020019184600183028401116401000000008311171561024c57600080fd5b509092509050610683565b005b610261610d57565b6040805160208082528351818301528351919283929083019185019080838360005b8381101561029b578181015183820152602001610283565b50505050905090810190601f1680156102c85780820380516001836020036101000a031916815260200191505b509250505060405180910390f35b6102de610d90565b604080516dffffffffffffffffffffffffffff948516815292909316602083015263ffffffff168183015290519081900360600190f35b61034e6004803603604081101561032b57600080fd5b5073ffffffffffffffffffffffffffffffffffffffff8135169060200135610de5565b604080519115158252519081900360200190f35b61036a610dfc565b6040805173ffffffffffffffffffffffffffffffffffffffff9092168252519081900360200190f35b61039b610e18565b60408051918252519081900360200190f35b61034e600480360360608110156103c357600080fd5b5073ffffffffffffffffffffffffffffffffffffffff813581169160208101359091169060400135610e1e565b61039b610efd565b610400610f21565b6040805160ff9092168252519081900360200190f35b61039b610f26565b6102576004803603604081101561043457600080fd5b5073ffffffffffffffffffffffffffffffffffffffff81358116916020013516610f2c565b61039b611005565b61039b61100b565b61039b6004803603602081101561047f57600080fd5b503573ffffffffffffffffffffffffffffffffffffffff16611011565b61039b600480360360208110156104b257600080fd5b503573ffffffffffffffffffffffffffffffffffffffff166113cb565b61039b6113dd565b61039b600480360360208110156104ed57600080fd5b503573ffffffffffffffffffffffffffffffffffffffff166113e3565b61053d6004803603602081101561052057600080fd5b503573ffffffffffffffffffffffffffffffffffffffff166113f5565b6040805192835260208301919091528051918290030190f35b610261611892565b61034e6004803603604081101561057457600080fd5b5073ffffffffffffffffffffffffffffffffffffffff81351690602001356118cb565b61039b6118d8565b610257600480360360208110156105b557600080fd5b503573ffffffffffffffffffffffffffffffffffffffff166118de565b61036a611ad4565b61036a611af0565b610257600480360360e08110156105f857600080fd5b5073ffffffffffffffffffffffffffffffffffffffff813581169160208101359091169060408101359060608101359060ff6080820135169060a08101359060c00135611b0c565b61039b6004803603604081101561065657600080fd5b5073ffffffffffffffffffffffffffffffffffffffff81358116916020013516611dd8565b610257611df5565b600c546001146106f457604080517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152601160248201527f556e697377617056323a204c4f434b4544000000000000000000000000000000604482015290519081900360640190fd5b6000600c55841515806107075750600084115b61075c576040517f08c379a0000000000000000000000000000000000000000000000000000000008152600401808060200182810382526025815260200180612b2f6025913960400191505060405180910390fd5b600080610767610d90565b5091509150816dffffffffffffffffffffffffffff168710801561079a5750806dffffffffffffffffffffffffffff1686105b6107ef576040517f08c379a0000000000000000000000000000000000000000000000000000000008152600401808060200182810382526021815260200180612b786021913960400191505060405180910390fd5b600654600754600091829173ffffffffffffffffffffffffffffffffffffffff91821691908116908916821480159061085457508073ffffffffffffffffffffffffffffffffffffffff168973ffffffffffffffffffffffffffffffffffffffff1614155b6108bf57604080517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152601560248201527f556e697377617056323a20494e56414c49445f544f0000000000000000000000604482015290519081900360640190fd5b8a156108d0576108d0828a8d611fdb565b89156108e1576108e1818a8c611fdb565b86156109c3578873ffffffffffffffffffffffffffffffffffffffff166310d1e85c338d8d8c8c6040518663ffffffff1660e01b8152600401808673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001858152602001848152602001806020018281038252848482818152602001925080828437600081840152601f19601f8201169050808301925050509650505050505050600060405180830381600087803b1580156109aa57600080fd5b505af11580156109be573d6000803e3d6000fd5b505050505b604080517f70a08231000000000000000000000000000000000000000000000000000000008152306004820152905173ffffffffffffffffffffffffffffffffffffffff8416916370a08231916024808301926020929190829003018186803b158015610a2f57600080fd5b505afa158015610a43573d6000803e3d6000fd5b505050506040513d6020811015610a5957600080fd5b5051604080517f70a08231000000000000000000000000000000000000000000000000000000008152306004820152905191955073ffffffffffffffffffffffffffffffffffffffff8316916370a0823191602480820192602092909190829003018186803b158015610acb57600080fd5b505afa158015610adf573d6000803e3d6000fd5b505050506040513d6020811015610af557600080fd5b5051925060009150506dffffffffffffffffffffffffffff85168a90038311610b1f576000610b35565b89856dffffffffffffffffffffffffffff160383035b9050600089856dffffffffffffffffffffffffffff16038311610b59576000610b6f565b89856dffffffffffffffffffffffffffff160383035b90506000821180610b805750600081115b610bd5576040517f08c379a0000000000000000000000000000000000000000000000000000000008152600401808060200182810382526024815260200180612b546024913960400191505060405180910390fd5b6000610c09610beb84600363ffffffff6121e816565b610bfd876103e863ffffffff6121e816565b9063ffffffff61226e16565b90506000610c21610beb84600363ffffffff6121e816565b9050610c59620f4240610c4d6dffffffffffffffffffffffffffff8b8116908b1663ffffffff6121e816565b9063ffffffff6121e816565b610c69838363ffffffff6121e816565b1015610cd657604080517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152600c60248201527f556e697377617056323a204b0000000000000000000000000000000000000000604482015290519081900360640190fd5b5050610ce4848488886122e0565b60408051838152602081018390528082018d9052606081018c9052905173ffffffffffffffffffffffffffffffffffffffff8b169133917fd78ad95fa46c994b6551d0da85fc275fe613ce37657fb8d5e3d130840159d8229181900360800190a350506001600c55505050505050505050565b6040518060400160405280600a81526020017f556e69737761702056320000000000000000000000000000000000000000000081525081565b6008546dffffffffffffffffffffffffffff808216926e0100000000000000000000000000008304909116917c0100000000000000000000000000000000000000000000000000000000900463ffffffff1690565b6000610df233848461259c565b5060015b92915050565b60065473ffffffffffffffffffffffffffffffffffffffff1681565b60005481565b73ffffffffffffffffffffffffffffffffffffffff831660009081526002602090815260408083203384529091528120547fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff14610ee85773ffffffffffffffffffffffffffffffffffffffff84166000908152600260209081526040808320338452909152902054610eb6908363ffffffff61226e16565b73ffffffffffffffffffffffffffffffffffffffff851660009081526002602090815260408083203384529091529020555b610ef384848461260b565b5060019392505050565b7f6e71edae12b1b97f4d1f60370fef10105fa2faae0126114a169c64845d6126c981565b601281565b60035481565b60055473ffffffffffffffffffffffffffffffffffffffff163314610fb257604080517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152601460248201527f556e697377617056323a20464f5242494444454e000000000000000000000000604482015290519081900360640190fd5b6006805473ffffffffffffffffffffffffffffffffffffffff9384167fffffffffffffffffffffffff00000000000000000000000000000000000000009182161790915560078054929093169116179055565b60095481565b600a5481565b6000600c5460011461108457604080517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152601160248201527f556e697377617056323a204c4f434b4544000000000000000000000000000000604482015290519081900360640190fd5b6000600c81905580611094610d90565b50600654604080517f70a08231000000000000000000000000000000000000000000000000000000008152306004820152905193955091935060009273ffffffffffffffffffffffffffffffffffffffff909116916370a08231916024808301926020929190829003018186803b15801561110e57600080fd5b505afa158015611122573d6000803e3d6000fd5b505050506040513d602081101561113857600080fd5b5051600754604080517f70a08231000000000000000000000000000000000000000000000000000000008152306004820152905192935060009273ffffffffffffffffffffffffffffffffffffffff909216916370a0823191602480820192602092909190829003018186803b1580156111b157600080fd5b505afa1580156111c5573d6000803e3d6000fd5b505050506040513d60208110156111db57600080fd5b505190506000611201836dffffffffffffffffffffffffffff871663ffffffff61226e16565b90506000611225836dffffffffffffffffffffffffffff871663ffffffff61226e16565b9050600061123387876126ec565b600054909150806112705761125c6103e8610bfd611257878763ffffffff6121e816565b612878565b985061126b60006103e86128ca565b6112cd565b6112ca6dffffffffffffffffffffffffffff8916611294868463ffffffff6121e816565b8161129b57fe5b046dffffffffffffffffffffffffffff89166112bd868563ffffffff6121e816565b816112c457fe5b0461297a565b98505b60008911611326576040517f08c379a0000000000000000000000000000000000000000000000000000000008152600401808060200182810382526028815260200180612bc16028913960400191505060405180910390fd5b6113308a8a6128ca565b61133c86868a8a6122e0565b811561137e5760085461137a906dffffffffffffffffffffffffffff808216916e01000000000000000000000000000090041663ffffffff6121e816565b600b555b6040805185815260208101859052815133927f4c209b5fc8ad50758f13e2e1088ba56a560dff690a1c6fef26394f4c03821c4f928290030190a250506001600c5550949695505050505050565b60016020526000908152604090205481565b600b5481565b60046020526000908152604090205481565b600080600c5460011461146957604080517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152601160248201527f556e697377617056323a204c4f434b4544000000000000000000000000000000604482015290519081900360640190fd5b6000600c81905580611479610d90565b50600654600754604080517f70a08231000000000000000000000000000000000000000000000000000000008152306004820152905194965092945073ffffffffffffffffffffffffffffffffffffffff9182169391169160009184916370a08231916024808301926020929190829003018186803b1580156114fb57600080fd5b505afa15801561150f573d6000803e3d6000fd5b505050506040513d602081101561152557600080fd5b5051604080517f70a08231000000000000000000000000000000000000000000000000000000008152306004820152905191925060009173ffffffffffffffffffffffffffffffffffffffff8516916370a08231916024808301926020929190829003018186803b15801561159957600080fd5b505afa1580156115ad573d6000803e3d6000fd5b505050506040513d60208110156115c357600080fd5b5051306000908152600160205260408120549192506115e288886126ec565b600054909150806115f9848763ffffffff6121e816565b8161160057fe5b049a5080611614848663ffffffff6121e816565b8161161b57fe5b04995060008b11801561162e575060008a115b611683576040517f08c379a0000000000000000000000000000000000000000000000000000000008152600401808060200182810382526028815260200180612b996028913960400191505060405180910390fd5b61168d3084612992565b611698878d8d611fdb565b6116a3868d8c611fdb565b604080517f70a08231000000000000000000000000000000000000000000000000000000008152306004820152905173ffffffffffffffffffffffffffffffffffffffff8916916370a08231916024808301926020929190829003018186803b15801561170f57600080fd5b505afa158015611723573d6000803e3d6000fd5b505050506040513d602081101561173957600080fd5b5051604080517f70a08231000000000000000000000000000000000000000000000000000000008152306004820152905191965073ffffffffffffffffffffffffffffffffffffffff8816916370a0823191602480820192602092909190829003018186803b1580156117ab57600080fd5b505afa1580156117bf573d6000803e3d6000fd5b505050506040513d60208110156117d557600080fd5b505193506117e585858b8b6122e0565b811561182757600854611823906dffffffffffffffffffffffffffff808216916e01000000000000000000000000000090041663ffffffff6121e816565b600b555b604080518c8152602081018c9052815173ffffffffffffffffffffffffffffffffffffffff8f169233927fdccd412f0b1252819cb1fd330b93224ca42612892bb3f4f789976e6d81936496929081900390910190a35050505050505050506001600c81905550915091565b6040518060400160405280600681526020017f554e492d5632000000000000000000000000000000000000000000000000000081525081565b6000610df233848461260b565b6103e881565b600c5460011461194f57604080517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152601160248201527f556e697377617056323a204c4f434b4544000000000000000000000000000000604482015290519081900360640190fd5b6000600c55600654600754600854604080517f70a08231000000000000000000000000000000000000000000000000000000008152306004820152905173ffffffffffffffffffffffffffffffffffffffff9485169490931692611a2b9285928792611a26926dffffffffffffffffffffffffffff169185916370a0823191602480820192602092909190829003018186803b1580156119ee57600080fd5b505afa158015611a02573d6000803e3d6000fd5b505050506040513d6020811015611a1857600080fd5b50519063ffffffff61226e16565b611fdb565b600854604080517f70a082310000000000000000000000000000000000000000000000000000000081523060048201529051611aca9284928792611a26926e01000000000000000000000000000090046dffffffffffffffffffffffffffff169173ffffffffffffffffffffffffffffffffffffffff8616916370a0823191602480820192602092909190829003018186803b1580156119ee57600080fd5b50506001600c5550565b60055473ffffffffffffffffffffffffffffffffffffffff1681565b60075473ffffffffffffffffffffffffffffffffffffffff1681565b42841015611b7b57604080517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152601260248201527f556e697377617056323a20455850495245440000000000000000000000000000604482015290519081900360640190fd5b60035473ffffffffffffffffffffffffffffffffffffffff80891660008181526004602090815260408083208054600180820190925582517f6e71edae12b1b97f4d1f60370fef10105fa2faae0126114a169c64845d6126c98186015280840196909652958d166060860152608085018c905260a085019590955260c08085018b90528151808603909101815260e0850182528051908301207f19010000000000000000000000000000000000000000000000000000000000006101008601526101028501969096526101228085019690965280518085039096018652610142840180825286519683019690962095839052610162840180825286905260ff89166101828501526101a284018890526101c28401879052519193926101e2808201937fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe081019281900390910190855afa158015611cdc573d6000803e3d6000fd5b50506040517fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0015191505073ffffffffffffffffffffffffffffffffffffffff811615801590611d5757508873ffffffffffffffffffffffffffffffffffffffff168173ffffffffffffffffffffffffffffffffffffffff16145b611dc257604080517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152601c60248201527f556e697377617056323a20494e56414c49445f5349474e415455524500000000604482015290519081900360640190fd5b611dcd89898961259c565b505050505050505050565b600260209081526000928352604080842090915290825290205481565b600c54600114611e6657604080517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152601160248201527f556e697377617056323a204c4f434b4544000000000000000000000000000000604482015290519081900360640190fd5b6000600c55600654604080517f70a082310000000000000000000000000000000000000000000000000000000081523060048201529051611fd49273ffffffffffffffffffffffffffffffffffffffff16916370a08231916024808301926020929190829003018186803b158015611edd57600080fd5b505afa158015611ef1573d6000803e3d6000fd5b505050506040513d6020811015611f0757600080fd5b5051600754604080517f70a08231000000000000000000000000000000000000000000000000000000008152306004820152905173ffffffffffffffffffffffffffffffffffffffff909216916370a0823191602480820192602092909190829003018186803b158015611f7a57600080fd5b505afa158015611f8e573d6000803e3d6000fd5b505050506040513d6020811015611fa457600080fd5b50516008546dffffffffffffffffffffffffffff808216916e0100000000000000000000000000009004166122e0565b6001600c55565b604080518082018252601981527f7472616e7366657228616464726573732c75696e743235362900000000000000602091820152815173ffffffffffffffffffffffffffffffffffffffff85811660248301526044808301869052845180840390910181526064909201845291810180517bffffffffffffffffffffffffffffffffffffffffffffffffffffffff167fa9059cbb000000000000000000000000000000000000000000000000000000001781529251815160009460609489169392918291908083835b602083106120e157805182527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe090920191602091820191016120a4565b6001836020036101000a0380198251168184511680821785525050505050509050019150506000604051808303816000865af19150503d8060008114612143576040519150601f19603f3d011682016040523d82523d6000602084013e612148565b606091505b5091509150818015612176575080511580612176575080806020019051602081101561217357600080fd5b50515b6121e157604080517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152601a60248201527f556e697377617056323a205452414e534645525f4641494c4544000000000000604482015290519081900360640190fd5b5050505050565b60008115806122035750508082028282828161220057fe5b04145b610df657604080517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152601460248201527f64732d6d6174682d6d756c2d6f766572666c6f77000000000000000000000000604482015290519081900360640190fd5b80820382811115610df657604080517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152601560248201527f64732d6d6174682d7375622d756e646572666c6f770000000000000000000000604482015290519081900360640190fd5b6dffffffffffffffffffffffffffff841180159061230c57506dffffffffffffffffffffffffffff8311155b61237757604080517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152601360248201527f556e697377617056323a204f564552464c4f5700000000000000000000000000604482015290519081900360640190fd5b60085463ffffffff428116917c0100000000000000000000000000000000000000000000000000000000900481168203908116158015906123c757506dffffffffffffffffffffffffffff841615155b80156123e257506dffffffffffffffffffffffffffff831615155b15612492578063ffffffff16612425856123fb86612a57565b7bffffffffffffffffffffffffffffffffffffffffffffffffffffffff169063ffffffff612a7b16565b600980547bffffffffffffffffffffffffffffffffffffffffffffffffffffffff929092169290920201905563ffffffff8116612465846123fb87612a57565b600a80547bffffffffffffffffffffffffffffffffffffffffffffffffffffffff92909216929092020190555b600880547fffffffffffffffffffffffffffffffffffff0000000000000000000000000000166dffffffffffffffffffffffffffff888116919091177fffffffff0000000000000000000000000000ffffffffffffffffffffffffffff166e0100000000000000000000000000008883168102919091177bffffffffffffffffffffffffffffffffffffffffffffffffffffffff167c010000000000000000000000000000000000000000000000000000000063ffffffff871602179283905560408051848416815291909304909116602082015281517f1c411e9a96e071241c2f21f7726b17ae89e3cab4c78be50e062b03a9fffbbad1929181900390910190a1505050505050565b73ffffffffffffffffffffffffffffffffffffffff808416600081815260026020908152604080832094871680845294825291829020859055815185815291517f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b9259281900390910190a3505050565b73ffffffffffffffffffffffffffffffffffffffff8316600090815260016020526040902054612641908263ffffffff61226e16565b73ffffffffffffffffffffffffffffffffffffffff8085166000908152600160205260408082209390935590841681522054612683908263ffffffff612abc16565b73ffffffffffffffffffffffffffffffffffffffff80841660008181526001602090815260409182902094909455805185815290519193928716927fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef92918290030190a3505050565b600080600560009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663017e7e586040518163ffffffff1660e01b815260040160206040518083038186803b15801561275757600080fd5b505afa15801561276b573d6000803e3d6000fd5b505050506040513d602081101561278157600080fd5b5051600b5473ffffffffffffffffffffffffffffffffffffffff821615801594509192509061286457801561285f5760006127d86112576dffffffffffffffffffffffffffff88811690881663ffffffff6121e816565b905060006127e583612878565b90508082111561285c576000612813612804848463ffffffff61226e16565b6000549063ffffffff6121e816565b905060006128388361282c86600563ffffffff6121e816565b9063ffffffff612abc16565b9050600081838161284557fe5b04905080156128585761285887826128ca565b5050505b50505b612870565b8015612870576000600b555b505092915050565b600060038211156128bb575080600160028204015b818110156128b5578091506002818285816128a457fe5b0401816128ad57fe5b04905061288d565b506128c5565b81156128c5575060015b919050565b6000546128dd908263ffffffff612abc16565b600090815573ffffffffffffffffffffffffffffffffffffffff8316815260016020526040902054612915908263ffffffff612abc16565b73ffffffffffffffffffffffffffffffffffffffff831660008181526001602090815260408083209490945583518581529351929391927fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef9281900390910190a35050565b6000818310612989578161298b565b825b9392505050565b73ffffffffffffffffffffffffffffffffffffffff82166000908152600160205260409020546129c8908263ffffffff61226e16565b73ffffffffffffffffffffffffffffffffffffffff831660009081526001602052604081209190915554612a02908263ffffffff61226e16565b600090815560408051838152905173ffffffffffffffffffffffffffffffffffffffff8516917fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef919081900360200190a35050565b6dffffffffffffffffffffffffffff166e0100000000000000000000000000000290565b60006dffffffffffffffffffffffffffff82167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff841681612ab457fe5b049392505050565b80820182811015610df657604080517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152601460248201527f64732d6d6174682d6164642d6f766572666c6f77000000000000000000000000604482015290519081900360640190fdfe556e697377617056323a20494e53554646494349454e545f4f55545055545f414d4f554e54556e697377617056323a20494e53554646494349454e545f494e5055545f414d4f554e54556e697377617056323a20494e53554646494349454e545f4c4951554944495459556e697377617056323a20494e53554646494349454e545f4c49515549444954595f4255524e4544556e697377617056323a20494e53554646494349454e545f4c49515549444954595f4d494e544544a265627a7a723158207dca18479e58487606bf70c79e44d8dee62353c9ee6d01f9a9d70885b8765f2264736f6c63430005100032") [macro]