Tai D. Nguyen duytai

## id_rsa.pub
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= duytai.cse@gmail.com

## BAT_transfer.py
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),

## preconditions.py
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),

## hello.ipynb

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                duytai
                / hello.ipynb
            
            
              Last active
              March 12, 2023 11:34
            
          
        Loading

      Sorry, something went wrong. Reload?
      Sorry, we cannot display this file.
      Sorry, this file is invalid so it cannot be displayed.
      
          Viewer requires iframe.
      
    
## verification-example.ipynb

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                duytai
                / verification-example.ipynb
            
            
              Created
              October 13, 2022 09:38
            
              
                Verification example
              
          
        Loading

      Sorry, something went wrong. Reload?
      Sorry, we cannot display this file.
      Sorry, this file is invalid so it cannot be displayed.
      
          Viewer requires iframe.
      
    
## ERC20Basic.sol
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);

## FSM.py
# 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

## Auction.rs
// 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;
  }

## index.js
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'

## fixed_transaction.csv
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
	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),
	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),
	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);
	# 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
	// 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;
	}
	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'
	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