Last active
October 11, 2021 11:10
-
-
Save duytai/d0e58ab6f4132226da8b0c3392e3fe63 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// 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; | |
} | |
init -- bid { | |
diff(eth_amount - refund_amount) == 0; | |
diff(eth_amout) > 0; | |
} | |
bid -- refund { | |
diff(eth_amount - refund_amount) == 0; | |
diff(eth_amount) < 0; | |
} | |
loop { | |
dist(eth_amount) + dist(refund_amount) == 0; | |
} | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
//Contract: https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/token/ERC20/ERC20.sol | |
impl Cashflow for ERC20 { | |
uint sending_amount = balances[*]; | |
uint receiving_amount = balances[*]; | |
uint owner_amount = balances[*]; | |
uint total_supply = totalSupply; | |
init { | |
diff(owner_amount) + diff(total_supply) == 0; | |
} | |
init -- exchange { | |
diff(sending_amount) + diff(receiving_amount) == 0; | |
} | |
loop { | |
dist(sending_amount) + dist(receiving_amount) == 0; | |
} | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// contract: https://peckshield.medium.com/origin-dollar-incident-root-cause-analysis-f27e11988c90 | |
impl DaiVault for oUSD { | |
address DAI_ADDRESS = "0x...."; | |
address PRICE_PROVIDER = "0x...."; | |
uint dai_price = IOracle(PRICE_PROVIDER).price(DAI_ADDRESS); | |
uint dai_amount = IERC20(TOKEN_ADDRESS).balanceOf(address(this)); // VAULT dai balance | |
uint usd_amount oUSD.balanceOf(msg.sender); // user usd balance | |
init { | |
dist(dai_amount) + dist(usd_amount) == 0; | |
} | |
init -- mint { | |
diff(dai_amount) * new(dai_price) == diff(usd_amount); | |
} | |
loop { | |
dist(dai_amount) + dist(usd_amount) == 0; | |
} | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// Contract: https://github.com/Uniswap/v1-contracts/blob/master/contracts/uniswap_exchange.vy | |
impl AMM for Exchange { | |
uint eth_amount = address(this).balance; | |
uint token_amount = this.balanceOf(address(this)); | |
init { | |
new(eth_amount) + new(token_amount) == 0; | |
} | |
init, exchange -- liquid { | |
diff(eth_amount) * diff(token_amount) > 0; // both assets increase/decrease | |
diff(eth_amount) * old(token_amount) == diff(token_amount) * old(eth_amount); // must maintain this ratio | |
} | |
init, liquid -- exchange { | |
diff(eth_amount) * diff(token_amount) < 0; | |
if diff(eth_amount) < 0 { | |
diff(eth_amount * token_amount) == 3 * diff(token_amount) * new(eth_amount) / 1000; // 0.3% fee | |
} else { | |
diff(eth_amount * token_amount) == 3 * diff(eth_amount) * new(token_amount) / 1000; // 0.3% fee | |
} | |
} | |
loop { | |
dist(eth_amount) + dist(token_amount) == 0; | |
} | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1. built-in functions:
old(x)
: old value of xnew(x)
: new value of xdiff(x)
: new(x) - old(x)dist(x)
: |new(x) - old(x)|min(x, y)
: if x > y return y else return xmax(x, y)
: if x > y return x else return y2. reversed states:
init
: is executed when the contract is deployedloop
: is executed before other state transitions (exceptinit
). If the condition is satisfied then state is unchanged, otherwise execute other state transitions3. syntax
use <type> <expression> as <variable_name>;
: in the state transitions, the<variable_name>
is used as an alias of<expression>
where the<expression>
is imported from the contractnew(cur_bid)
is valid, butcur_bid
is invalid