duytai

ssh-rsa AAAAB3NzaC1yc2EAAAADAQABAAABgQCi3v4Hmbo0V39MNMEorTlO+OTQYfnu12l8bSiNUre32gNJXV6mA9z6ilC6tpTru/IKs+BpTsptODu/zby8mOt4UzNxr+VNCTsmIYtSGC+yJW6j9xGHPiqYN5WOAtqQ5h5UdhoVIckuIFfie0PKLiL6QZsQfwxpq8KjT/WsrJCxG5jhkQ4dbGeIcKa4531HgaLF8aLitbW5+oVVDXyFmRSk0jGNJgEbE+LPbeNlo+fYC7NVNLJ5+vvQ5uvFsrHOG4dO6TN+Po3UwvFtl5GenMyxmCddEvD0fR9qb8V/fKtgwB64pjMfyU3rOzwg4KMU5W/r83mwmwKgQbK/bEZUN/tgYWJBM6Qsc4MUyRt00njgwebH/DWw5CRUWERMQRCYN1hjeK2Fh4EgWFm/N2oJ6AubCcZzKiy0mmc3i/UYoo29vgq2G5voUwFro/ieuIWuN2ODAnS/fNs0t4zUgYtHnh0JMfztsAI8Pcub1wv+lZlAMg8A3deAGdjOk8UJB/3aXS0= [email protected]

duytai

And(_value <= 0, 0 == _value)
And(0 == _value)
And(Not(msg.sender == _to), 0 == _value)
And(Not(msg.sender == _to),
    Not(_value <= 0),
    balances[msg.sender] >= _value)
And(Not(msg.sender == _to),
    0 == _value,
    balances[msg.sender] >= _value)
And(Not(msg.sender == _to),

duytai

And(Or(Not(-1*amount + _allowances[sender][msg.sender] <= -1),
       Not(amount == 0),
       Not(_balances[sender] >= amount),
       Not(amount >= 0),
       Not(recipient <= -1),
       Not(sender <= -1),
       Not(sender + -1*recipient <= -1),
       Not(0 <= _balances[recipient])),
    Or(_balances[sender] >= amount, Not(amount == 0)),
    Or(Not(amount == 0),

duytai

duytai

duytai

contract ERC20Basic {

  string public constant name = "ERC20Basic";
  string public constant symbol = "BSC";
  uint8 public constant decimals = 18;


  event Approval(address indexed tokenOwner, address indexed spender, uint tokens);
  event Transfer(address indexed from, address indexed to, uint tokens);

duytai

# contract: ERC20
# code: https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/token/ERC20/ERC20.sol

uint x = balances[msg.sender]
uint y = balances[*]
uint m = allowance[*][msg.sender]
uint n = allowance[msg.sender][*]

init(uint k = totalSupply):
  (x = k) if k > 0

duytai

// Code: https://www.microsoft.com/en-us/research/uploads/prod/2021/02/SmartPulse-Oakland21-preprint.pdf

impl Bidding for Auction {
  uint eth_amount = address(this).balance;
  uint refund_amount = refunds[*];

  init {
    dist(eth_amount) + dist(refund_amount) == 0;
  }

duytai

import needle from 'needle'
import Q from 'q'
import cheerio from 'cheerio'
import he from 'he'
import queryString from 'query-string'
import { CronJob } from 'cron'
import { MongoClient } from 'mongodb'
import redis from 'redis'
import getFirstPhone from './getFirstPhone'
import getDistrict from './getDistrict'

duytai

0x000000000092c287eb63e8c2c30b4a74787054f8,0x2bab1d416621530a0f1ea71aebafa6dc2d0f658ea5cdf012608da21aa5d3e3ce,0,0,0
0x000f400e6818158d541c3ebe45fe3aa0d47372ff,0xe2a92b7ff253de78bb87628c0f12e0745989bbe139701f5a24797d275221e12e,71,136585,1
0x002c97933d0976dbcf51c0e8f8a3e64d8fd9d296,0xa3fe9f182eeba8e680ee58360b072e595e111caf977b72b2abba52e4c5525de0,87,1670977,1
0x004982bfa6ed67cd7f290f45aed3057e5c7463e0,0x03c9db5f7329800bee55328ad212250a892435d3d6f9a5013105ddcb65f0674b,87,1436590,1
0x00534caeb1c9a7fbe59449653914eccd4bcfbdb6,0x2b6daa36dfde8358d338e4d69f358646a4146830b16a15ed45fe3d34d6c00e08,0,0,0
0x007ff3b4639baf3aed4056b11c5abb03b243835b,0x98e5d986d23e1c3decce3490db87ab20788ab5021f504164b5c9523c38d6b96f,0,0,0
0x009631f3cb11a9af2e2f0186e698a2bc976d86eb,0x9e30d62911d566ade2dd34fa80bf58407b68c0358c7de650cdd09803c1fa313f,111,1052778,1
0x009631f3cb11a9af2e2f0186e698a2bc976d86eb,0x1a5f6b19d1c31c4373b7460a95cce0958738ac0407021e3dfff020fd3ac844e6,41,44262,1
0x009631f3cb11a9af2e2f0186e698a2bc976d86eb,0x43142dfd2d91972a73