diff --git a/.circleci/config.yml b/.circleci/config.yml index f0018493..30ecfb39 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -10,7 +10,7 @@ jobs: working_directory: ~/repo steps: - run: - | + | sudo wget https://github.com/ethereum/solidity/releases/download/v0.6.10/solc-static-linux -O /usr/local/bin/solc sudo chmod +x /usr/local/bin/solc - checkout @@ -54,7 +54,7 @@ jobs: working_directory: ~/repo steps: - run: - | + | sudo wget https://github.com/ethereum/solidity/releases/download/v0.6.10/solc-static-linux -O /usr/local/bin/solc sudo chmod +x /usr/local/bin/solc - checkout @@ -126,7 +126,7 @@ jobs: path: ~/junit-poster - store_artifacts: path: ~/junit-poster - + test_reporter_javascript: docker: - image: circleci/node:12 @@ -149,7 +149,28 @@ jobs: path: ~/junit-sdk-javascript - store_artifacts: path: ~/junit-sdk-javascript - + + certora-test: + working_directory: ~/repo + docker: + - image: circleci/openjdk:11-jdk-node + steps: + - checkout + - run: + name: Certora dependencies + command: | + echo "export PATH=$PATH:~/.local/bin" >> $BASH_ENV + sudo apt-get update || sudo apt-get update + sudo apt-get install -y software-properties-common + sudo apt-get install python3-pip + pip3 install certora-cli==0.2.1 + wget https://github.com/ethereum/solidity/releases/download/v0.6.10/solc-static-linux + chmod +x solc-static-linux + sudo mv solc-static-linux /usr/bin/solc + - run: + name: Build and run - Open Oracle With Uniswap Anchor + command: | + certoraRun specs/harnesses/OpenOraclePriceDataHarness.sol specs/harnesses/UniswapAnchoredViewHarness.sol --verify UniswapAnchoredViewHarness:specs/harness.spec.spec --link UniswapAnchoredViewHarness:priceData=OpenOraclePriceDataHarness --settings -b=2,-assumeUnwindCond,-ruleSanityChecks --cache compoundUniswapAnchor workflows: version: 2 test: @@ -158,3 +179,4 @@ workflows: - test_coverage - test_poster - test_reporter_javascript + - certora-test \ No newline at end of file diff --git a/contracts/Uniswap/UniswapAnchoredView.sol b/contracts/Uniswap/UniswapAnchoredView.sol index 81695a84..9bb4eca6 100644 --- a/contracts/Uniswap/UniswapAnchoredView.sol +++ b/contracts/Uniswap/UniswapAnchoredView.sol @@ -146,7 +146,7 @@ contract UniswapAnchoredView is UniswapConfig { * @param signatures The signatures for the corresponding messages * @param symbols The symbols to compare to anchor for authoritative reading */ - function postPrices(bytes[] calldata messages, bytes[] calldata signatures, string[] calldata symbols) external { + function postPrices(bytes[] calldata messages, bytes[] calldata signatures, string[] calldata symbols) virtual external { //CERTORA: added virtual modifier for harness require(messages.length == signatures.length, "messages and signatures must be 1:1"); // Save the prices @@ -197,7 +197,7 @@ contract UniswapAnchoredView is UniswapConfig { /** * @dev Fetches the current token/eth price accumulator from uniswap. */ - function currentCumulativePrice(TokenConfig memory config) internal view returns (uint) { + function currentCumulativePrice(TokenConfig memory config) internal virtual view returns (uint) { //CERTORA: added virtual modifier for harness (uint cumulativePrice0, uint cumulativePrice1,) = UniswapV2OracleLibrary.currentCumulativePrices(config.uniswapMarket); if (config.isUniswapReversed) { return cumulativePrice1; @@ -210,7 +210,7 @@ contract UniswapAnchoredView is UniswapConfig { * @dev Fetches the current eth/usd price from uniswap, with 6 decimals of precision. * Conversion factor is 1e18 for eth/usdc market, since we decode uniswap price statically with 18 decimals. */ - function fetchEthPrice() internal returns (uint) { + function fetchEthPrice() internal virtual returns (uint) { //CERTORA: added virtual modifier for harness return fetchAnchorPrice("ETH", getTokenConfigBySymbolHash(ethHash), ethBaseUnit); } diff --git a/contracts/Uniswap/UniswapConfig.sol b/contracts/Uniswap/UniswapConfig.sol index cc05feec..c4bc4c6f 100644 --- a/contracts/Uniswap/UniswapConfig.sol +++ b/contracts/Uniswap/UniswapConfig.sol @@ -555,7 +555,7 @@ contract UniswapConfig { }); } - function getCTokenIndex(address cToken) internal view returns (uint) { + function getCTokenIndex(address cToken) internal virtual view returns (uint) { //CERTORA: added virtual for harness if (cToken == cToken00) return 0; if (cToken == cToken01) return 1; if (cToken == cToken02) return 2; @@ -590,7 +590,7 @@ contract UniswapConfig { return uint(-1); } - function getUnderlyingIndex(address underlying) internal view returns (uint) { + function getUnderlyingIndex(address underlying) internal virtual view returns (uint) { //CERTORA: Added virtual for harness if (underlying == underlying00) return 0; if (underlying == underlying01) return 1; if (underlying == underlying02) return 2; @@ -625,7 +625,7 @@ contract UniswapConfig { return uint(-1); } - function getSymbolHashIndex(bytes32 symbolHash) internal view returns (uint) { + function getSymbolHashIndex(bytes32 symbolHash) internal virtual view returns (uint) { //CERTORA: Added virtual for harness if (symbolHash == symbolHash00) return 0; if (symbolHash == symbolHash01) return 1; if (symbolHash == symbolHash02) return 2; @@ -665,7 +665,7 @@ contract UniswapConfig { * @param i The index of the config to get * @return The config object */ - function getTokenConfig(uint i) public view returns (TokenConfig memory) { + function getTokenConfig(uint i) public virtual view returns (TokenConfig memory) { //CERTORA: Added virtual for harness require(i < numTokens, "token config not found"); if (i == 0) return TokenConfig({cToken: cToken00, underlying: underlying00, symbolHash: symbolHash00, baseUnit: baseUnit00, priceSource: priceSource00, fixedPrice: fixedPrice00, uniswapMarket: uniswapMarket00, isUniswapReversed: isUniswapReversed00}); diff --git a/specs/harness.spec.spec b/specs/harness.spec.spec new file mode 100644 index 00000000..c4d0672e --- /dev/null +++ b/specs/harness.spec.spec @@ -0,0 +1,214 @@ +methods { +getUpperThreshold() returns uint256 envfree +getLowerThreshold() returns uint256 envfree +getPriceData(address,uint256) returns uint64 envfree +priceHarness(uint256) returns uint256 envfree +newObservationTimestamp(bytes32) returns uint256 envfree +oldObservationTimestamp(bytes32) returns uint256 envfree +anchorPeriod() returns uint256 envfree +getSymbolHash(uint256) returns bytes32 envfree +getSymbolKeccakHash(uint256) returns bytes32 envfree +reporter() returns address envfree +getEthHash() returns bytes32 envfree +reporterInvalidated() returns bool envfree +getSymbolBaseUnit(uint256) returns uint256 envfree +getSymbolPriceSource(uint256) returns uint256 envfree +getSymbolHashIndexHarness(bytes32) returns uint256 envfree +} + +/* +The percentage tolerance that the reporter price may deviate from the uniswap anchor price should +be bounded. Specifically, anchorPrice*10^18/reporterPrice >= sinvoke getLowerThreshold() && anchorPrice*10^18/reporterPrice <= sinvoke getUpperThreshold(). +NOTE: 2000000000000000000 == 2*10^18; 1000000000000000000 == 10^18 + */ +invariant anchorThresholds() sinvoke getUpperThreshold() >= sinvoke getLowerThreshold() && sinvoke getLowerThreshold() > 0 + && ((sinvoke getUpperThreshold() >= 2000000000000000000 && sinvoke getLowerThreshold() == 1) || + (sinvoke getUpperThreshold() < 2000000000000000000 && sinvoke getLowerThreshold() <= 1000000000000000000)) +/* +The new and old Uniswap cumulative anchor prices stored ("observed") by the system are at least anchorPeriod apart. This invariant is maintained in all system's states except the initialization state. The system is in an initialization state during the first anchorPeriod. In this state, the new and old cumulative anchor prices are equal. This invariant entails that once the sysem is no longer in initialization state, the TWAP is computed over a time interval at least anchorPrice. +*/ +invariant consistentObservationsTimeStamps(bytes32 symbolHash) sinvoke oldObservationTimestamp(symbolHash) == sinvoke newObservationTimestamp(symbolHash) || + sinvoke newObservationTimestamp(symbolHash) >= sinvoke oldObservationTimestamp(symbolHash) + sinvoke anchorPeriod() { + preserved pokeWindowValuesHarness(env e, uint256 symbolIndex) { + require symbolHash == sinvoke getSymbolHash(symbolIndex) && (sinvoke newObservationTimestamp(symbolHash) >= sinvoke oldObservationTimestamp(symbolHash) + sinvoke anchorPeriod() || sinvoke oldObservationTimestamp(symbolHash) == sinvoke newObservationTimestamp(symbolHash)) && e.block.timestamp >= sinvoke newObservationTimestamp(symbolHash); + //In addition to the original invariant, assume that now does not come before the new //observation; + //otherwise, we may get an underflow in pokeWindowValues, and as a result, oldTimeStamp > newTimeStamp (violating the invariant). + } + } + +/* +Assuming the system is in initialization state, after anchorPeriod the system reaches a state where the new and old Uniswap cumulative anchor prices stored ("observed") by the system are at least anchorPeriod apart. +*/ +rule observationTimeStampsInitizializedEndPeriod(uint256 symbolIndex, uint256 oldTimestamp, uint256 newTimestamp, uint256 currtimestamp, uint256 anchorPeriodTime) { + env e; + + bytes32 symbolHash = sinvoke getSymbolHash(symbolIndex); + + require currtimestamp == e.block.timestamp ; + require oldTimestamp == sinvoke oldObservationTimestamp(symbolHash); + require newTimestamp == sinvoke newObservationTimestamp(symbolHash); + require anchorPeriodTime == sinvoke anchorPeriod(); + + //Assume initialization state + require oldTimestamp == newTimestamp; + + //Require that the first anchor period has elapsed. + require currtimestamp >= newTimestamp + anchorPeriodTime; + + //Require that anchorPeriod is properly initialized to a non-zero value. + require anchorPeriodTime > 0; + + //Invoke UniswapAnchoredView.pokeWindowValues + invoke pokeWindowValuesHarness(e,symbolIndex); + assert !lastReverted => sinvoke newObservationTimestamp(symbolHash) >= sinvoke oldObservationTimestamp(symbolHash) + sinvoke anchorPeriod(); +} + +/* +Assuming the system is in a state after initialization, the new and old Uniswap cumulative anchor prices stored ("observed") by the system are at least anchorPeriod apart. +*/ +rule observationTimeStampsOnPokeAfterInit(uint256 symbolIndex, uint256 oldTimestamp, uint256 newTimestamp, uint256 currtimestamp, uint anchorPeriodTime) { + env e; + bytes32 symbolHash = sinvoke getSymbolHash(symbolIndex); + + require currtimestamp == e.block.timestamp ; + require oldTimestamp == sinvoke oldObservationTimestamp(symbolHash); + require newTimestamp == sinvoke newObservationTimestamp(symbolHash); + require anchorPeriodTime == sinvoke anchorPeriod(); + + //Require that the block numbers are realistic (namely, now does not come before the new observation); + //otherwise, this rule is violated due to a possible subtraction underflow in pokeWindowValues + //(see line 255 in UniswapAnchoredView: uint timeElapsed = block.timestamp - newObservation.timestamp;) + require currtimestamp >= newTimestamp; + + // require that we start with a valid state + require anchorPeriodTime > 0; + + //require that the state is after the initialization state + require newTimestamp >= oldTimestamp + anchorPeriodTime; + + // perform a pokeWindowValues + invoke pokeWindowValuesHarness(e,symbolIndex); + assert !lastReverted => currtimestamp >= sinvoke oldObservationTimestamp(symbolHash) + anchorPeriodTime; +} + +/* +With the same Open Oracle Price Data, and once a symbol’s price is posted, its price should remain unchanged. +This property does not hold when the reporter is invalidated, as the price changes to the anchor price on every post. +Currently, this rule is disabled due to performance issues of the tool. +*/ +//@Disable "performance issues" +// rule priceIdempotent(uint256 symbolIndex, bytes32 symbolKeccakHash, uint256 beforePrice, uint256 price1, uint256 price2, uint256 ethPrice) { + // env e1; + // env e2; + + // //Require that the reporter is not invalidated. + // require !sinvoke reporterInvalidated(); + + // //Require that symbolIndex has a valid priceSource enum value (either 0,1, or 2). + // require sinvoke getSymbolPriceSource(symbolIndex) < 3; + + // //Require that symbolKeccakHash uniquely maps to symbolIndex. + // /*NOTE: + // 1. This assumption also entails that both getTokenConfig(symbolIndex) and getTokenConfigBySymbolHash(symbolKeccakHash) do not revert. + // 2. This assumption ensures that getTokenConfig(symbolIndex) == getTokenConfigBySymbolHash(symbolKeccakHash), hence + // priceHarness(symbolIndex) and postPrice(*,symbolIndex,*) respectively return and change the price of the same symbol. + // */ + // require symbolKeccakHash == sinvoke getSymbolKeccakHash(symbolIndex) && symbolKeccakHash == sinvoke getSymbolHash(symbolIndex); + // require symbolIndex == sinvoke getSymbolHashIndexHarness(symbolKeccakHash); + + // //The symbol's price before posting its price. + // require beforePrice == sinvoke priceHarness(symbolIndex); + + // //Post the symbol's price. + // sinvoke postPrice(e1,symbolIndex,ethPrice); + // require price1 == sinvoke priceHarness(symbolIndex); + // require beforePrice != price1; + + // //Repost the symbol's price, without preceding calls to priceData.put. + // sinvoke postPrice(e2,symbolIndex,ethPrice); + // require price2 == sinvoke priceHarness(symbolIndex); + + // //Expect that the post operation is idempotent. + // assert price1 == price2; +// } + +/* +When posting a price for a symbol, the prices of other symbols do not change. The only +exception is the Ether (eth) price, which influences Ether denominated symbols’ prices. +Currently, this rule is disabled due to performance issues of the tool. +*/ +//@Disable "performance issues" +/* rule noChangeToOtherSymbols(uint256 symbolIndex,bytes32 symbolKeccakHash, uint256 ethSymbolIndex, bytes32 ethHash, address source, uint64 timestamp, uint64 value, + uint256 otherSymbolIndex, bytes32 otherSymbolKeccakHash, uint256 ethPrice) { + env e; + require sinvoke getEthHash() == ethHash; + require ethSymbolIndex == sinvoke getSymbolHashIndexHarness(ethHash) && ethSymbolIndex < 3; + require ethHash == sinvoke getSymbolHash(ethSymbolIndex) && ethHash == sinvoke getSymbolKeccakHash(ethSymbolIndex); + + //Require that symbol!=ETH. + //NOTE: otherwise, if otherSymbol is FIXED_ETH (thus eth denominated), its price may change + require symbolIndex != otherSymbolIndex && symbolIndex != ethSymbolIndex && symbolIndex < 3 && otherSymbolIndex < 3; + require symbolKeccakHash == sinvoke getSymbolKeccakHash(symbolIndex) && symbolKeccakHash == sinvoke getSymbolHash(symbolIndex); + require otherSymbolKeccakHash == sinvoke getSymbolKeccakHash(otherSymbolIndex) && otherSymbolKeccakHash == sinvoke getSymbolHash(otherSymbolIndex); + require symbolKeccakHash != otherSymbolKeccakHash && symbolKeccakHash != ethHash; + + require symbolIndex == sinvoke getSymbolHashIndexHarness(symbolKeccakHash); + require otherSymbolIndex == sinvoke getSymbolHashIndexHarness(otherSymbolKeccakHash); + + uint256 otherSymbolPriceBefore = sinvoke priceHarness(otherSymbolIndex); + + sinvoke harnessPut(e, source, timestamp, symbolIndex, value); + sinvoke postPrice(e,symbolIndex,ethPrice); + + uint256 otherSymbolPriceAfter = sinvoke priceHarness(otherSymbolIndex); + assert otherSymbolPriceBefore == otherSymbolPriceAfter, "otherSymbol price changed"; +} */ + +/* +This rule specifies sufficient assumptions under which the function UniswapAnchoredView.postPriceInternal does not revert. +Currently, this rule is disabled due to performance issues of the tool. +*/ +//@Disable "performance issues" +/* rule postPriceRevertCharacterisrtics(uint256 symbolIndex, uint256 ethPrice, uint256 newTimeStamp, uint256 oldTimeStamp) { + env e; + address reporter_ = sinvoke reporter(); + + //Avoid reverts due to functions being non-payable + require e.msg.value==0; + + bytes32 symbolHash = sinvoke getSymbolKeccakHash(symbolIndex); + + //Require that symbolIndex has valid config struct (in particular, getTokenConfig(symbolIndex) does not revert): + //Require that the symbol's config struct is initialized with a valid symbolHash + require symbolHash == sinvoke getSymbolHash(symbolIndex); + //Require that the symbol's config struct is initialized with a valid priceSource enum value (either 0,1, or 2) + require sinvoke getSymbolPriceSource(symbolIndex) < 3; + + require symbolIndex == sinvoke getSymbolHashIndexHarness(symbolHash); + //NOTE: this entails that getSymbolHashIndex(symbolHash) != -1 + + //Require that priceData has a getPrice method + sinvoke getPriceData(reporter_, symbolIndex); + + //Require config.baseUnit > 0 to avoid division by zero + require sinvoke getSymbolBaseUnit(symbolIndex) > 0; + + require newTimeStamp == sinvoke newObservationTimestamp(symbolHash); + require oldTimeStamp == sinvoke oldObservationTimestamp(symbolHash); + + //Assume invariant of consistent observation timestamps + requireInvariant consistentObservationsTimeStamps(symbolHash); + + //Assume that now does not come before the new observation + //otherwise, we may get an underflow, and as a result, oldTimeStamp > newTimeStamp + require e.block.timestamp >= newTimeStamp; + + //Assume that if in initialization state, now must come after either observations + //to avoid a revert due to the require statement in fetchAnchorPrice + require (oldTimeStamp == newTimeStamp) => (e.block.timestamp > oldTimeStamp); + //Assume that anchorPeriod > 0 to avoid timeElaped of zero (i.e., division by zero in fetchAnchorPrice) + require sinvoke anchorPeriod() > 0; + //require sinvoke getTokenConfigHash(s) != sinvoke getEthHash(); //just to take the path we want + invoke postPrice(e,symbolIndex,ethPrice); + assert !lastReverted; //we are expect to fail on mul overflow in fetchAnchorPrice +} */ diff --git a/specs/harnesses/OpenOraclePriceDataHarness.sol b/specs/harnesses/OpenOraclePriceDataHarness.sol new file mode 100644 index 00000000..3f10056a --- /dev/null +++ b/specs/harnesses/OpenOraclePriceDataHarness.sol @@ -0,0 +1,10 @@ +pragma solidity ^0.6.10; + +import "../../contracts/OpenOraclePriceData.sol"; + +contract OpenOraclePriceDataHarness is OpenOraclePriceData { + + function invokePutInternal(address source, uint64 timestamp, string memory key, uint64 value) external returns (string memory) { + return putInternal(source, timestamp, key, value); + } +} \ No newline at end of file diff --git a/specs/harnesses/UniswapAnchoredViewHarness.sol b/specs/harnesses/UniswapAnchoredViewHarness.sol new file mode 100644 index 00000000..6aa8f811 --- /dev/null +++ b/specs/harnesses/UniswapAnchoredViewHarness.sol @@ -0,0 +1,191 @@ +pragma solidity ^0.6.6; +pragma experimental ABIEncoderV2; + +import "../../contracts/Uniswap/UniswapAnchoredView.sol"; +import "./OpenOraclePriceDataHarness.sol"; + +contract UniswapAnchoredViewHarness is UniswapAnchoredView { + + constructor(OpenOraclePriceData priceData_, + address reporter_, + uint anchorToleranceMantissa_, + uint anchorPeriod_, + TokenConfig[] memory configs) public + UniswapAnchoredView(priceData_, reporter_, anchorToleranceMantissa_, anchorPeriod_, configs){ + } + + /* + CERTORA: + Overrding postPrices due to performance issues of the tool when checking the invariant consistentObservationsTimeStamps. + As a result, we have to make postPrices virtual. + NOTE: we do check the invariant for postPriceInternal, using the harness function postPrice. + */ + function postPrices(bytes[] calldata messages, bytes[] calldata signatures, string[] calldata symbols) override external {} + + /* + CERTORA: + This function replaces the constructor of UniswapAnchoredView and it is used to verify the invariants written in the specification. + NOTE: Any change to the constructor code should be reflected in this function as well in order to keep the verification results correct. + */ + function init_state(uint anchorToleranceMantissa_, address cToken_, address underlying_, bytes32 symbolHash_, uint256 baseUnit_, PriceSource priceSource_, + uint256 fixedPrice_, address uniswapMarket_, bool isUniswapReversed_) public { + require(upperBoundAnchorRatio == (anchorToleranceMantissa_ > uint(-1) - 100e16 ? uint(-1) : 100e16 + anchorToleranceMantissa_)); + require(lowerBoundAnchorRatio == (anchorToleranceMantissa_ < 100e16 ? 100e16 - anchorToleranceMantissa_ : 1)); + /* + CERTORA: + The code below should "mimic" the iteration performed in the constructor over the TokenConfigs array. + Each symbolHash may belong to a config (in the configs array) whose price source is either the reporter or some other source. + In the former case, both oldObservations[symbolHash] and newObservations[symbolHash] are initialized in the constructor + in the same way as in the code below. In the latter case, oldObservations[symbolHash] and newObservations[symbolHash] + are initialized to the default value (0x0). This also holds for every symbolHash that does not belong to any config. + */ + TokenConfig memory config = TokenConfig({ + cToken: cToken_, + underlying: underlying_, + symbolHash: symbolHash_, + baseUnit: baseUnit_, + priceSource: priceSource_, + fixedPrice: fixedPrice_, + uniswapMarket: uniswapMarket_, + isUniswapReversed: isUniswapReversed_ + }); + address uniswapMarket = config.uniswapMarket; + if (config.priceSource == PriceSource.REPORTER) { + require(uniswapMarket != address(0), "reported prices must have an anchor"); + bytes32 symbolHash = config.symbolHash; + uint cumulativePrice = currentCumulativePrice(config); + oldObservations[symbolHash].timestamp = block.timestamp; + newObservations[symbolHash].timestamp = block.timestamp; + oldObservations[symbolHash].acc = cumulativePrice; + newObservations[symbolHash].acc = cumulativePrice; + } else { + require(uniswapMarket == address(0), "only reported prices utilize an anchor"); + } + } + + function getUpperThreshold() public returns (uint) { return upperBoundAnchorRatio; } + function getLowerThreshold() public returns (uint) { return lowerBoundAnchorRatio; } + function newObservationTimestamp(bytes32 sym) public returns (uint) { return newObservations[sym].timestamp; } + function oldObservationTimestamp(bytes32 sym) public returns (uint) { return oldObservations[sym].timestamp; } + + string symStr; + function getEthHash() public returns (bytes32) { + /* + CERTORA: + Added the first line below to bypass (disable) the eager evaluation of keccak256(abi.encodePacked("ETH")), performed + as part of the verification condition generation. As this eager evaluation was not performed in case of other references to ethHash, + the equality of getEthHash() and ethHash was not asserted by the verification condition. That led to spurious counter-examples. + */ + keccak256(abi.encodePacked(symStr)); + + return ethHash; + } + + function priceHarness(uint symbolIndex) public view returns (uint) { + TokenConfig memory config = getTokenConfig(symbolIndex); + return priceInternal(config); + } + + function pokeWindowValuesHarness(uint symbolIndex) public returns (uint, uint, uint) { + TokenConfig memory config = getTokenConfig(symbolIndex); + return pokeWindowValues(config); + } + + mapping (uint => string) public indexToSymbol; + function symbolOfIndex(uint index) public returns (string memory) { + /* CERTORA: + To enable the verification condition to model that two strings are equal iff their (keccak) hashes are equal, + we require that all symbol strings are of length at most 32 bytes (one word). + */ + require(bytes(indexToSymbol[index]).length <= 32); + return indexToSymbol[index]; + } + + function postPrice(uint symbolIndex, uint ethPrice) external { //corresponds to postPriceInternal(string, uint) + postPriceInternal(symbolOfIndex(symbolIndex), ethPrice); + } + + function getSymbolHash(uint symbolIndex) public returns (bytes32) { + TokenConfig memory config = getTokenConfig(symbolIndex); + return config.symbolHash; + } + + function getSymbolKeccakHash(uint symbolIndex) public returns (bytes32) { + return keccak256(abi.encodePacked(symbolOfIndex(symbolIndex))); + } + + /* + CERTORA: + Added this function here rather than in OpenOraclePriceDataHarness because OpenOraclePriceData.getPrice is external; + otherwise, we would have to change it to be public. + */ + function getPriceData(address source, uint symbolIndex) public returns (uint64) { + return priceData.getPrice(source, symbolOfIndex(symbolIndex)); + } + + function harnessPut(address source, uint64 timestamp, uint symbolIndex, uint64 value) external { + OpenOraclePriceDataHarness(address(priceData)).invokePutInternal(source, timestamp, symbolOfIndex(symbolIndex), value); + } + + mapping (address => mapping (uint => mapping (bool => uint))) public uniswapHarness; + function currentCumulativePrice(TokenConfig memory config) internal view override returns (uint) { + return uniswapHarness[config.uniswapMarket][block.timestamp][config.isUniswapReversed]; + } + + function getCTokenIndex(address cToken) internal override view returns (uint) { + if (cToken == cToken00) return 0; + if (cToken == cToken01) return 1; + if (cToken == cToken02) return 2; + + return uint(-1); + } + + function getUnderlyingIndex(address underlying) internal override view returns (uint) { + if (underlying == underlying00) return 0; + if (underlying == underlying01) return 1; + if (underlying == underlying02) return 2; + + return uint(-1); + } + + function getSymbolHashIndex(bytes32 symbolHash) internal override view returns (uint) { + if (symbolHash == symbolHash00) return 0; + if (symbolHash == symbolHash01) return 1; + if (symbolHash == symbolHash02) return 2; + + return uint(-1); + } + + /* + CERTORA: + Added this fuction to keep getSymbolHashIndex (bytes32) internal. + */ + function getSymbolHashIndexHarness(bytes32 symbolHash) external view returns (uint) { + return getSymbolHashIndex(symbolHash); + } + + function getTokenConfig(uint i) public override view returns (TokenConfig memory) { + require(i < 3, "token config not found"); + + if (i == 0) return TokenConfig({cToken: cToken00, underlying: underlying00, symbolHash: symbolHash00, baseUnit: baseUnit00, priceSource: priceSource00, fixedPrice: fixedPrice00, uniswapMarket: uniswapMarket00, isUniswapReversed: isUniswapReversed00}); + if (i == 1) return TokenConfig({cToken: cToken01, underlying: underlying01, symbolHash: symbolHash01, baseUnit: baseUnit01, priceSource: priceSource01, fixedPrice: fixedPrice01, uniswapMarket: uniswapMarket01, isUniswapReversed: isUniswapReversed01}); + if (i == 2) return TokenConfig({cToken: cToken02, underlying: underlying02, symbolHash: symbolHash02, baseUnit: baseUnit02, priceSource: priceSource02, fixedPrice: fixedPrice02, uniswapMarket: uniswapMarket02, isUniswapReversed: isUniswapReversed02}); + } + + function getSymbolPriceSource(uint symbolIndex) public view returns (uint) { + require(symbolIndex < 3); + if(symbolIndex==0) return uint256(priceSource00); + if(symbolIndex==1) return uint256(priceSource01); + if(symbolIndex==2) return uint256(priceSource01); + } + + function getSymbolBaseUnit(uint symbolIndex) public view returns (uint) { + TokenConfig memory config = getTokenConfig(symbolIndex); + return config.baseUnit; + } + + mapping (uint => uint) public ethPrice; + function fetchEthPrice() internal override returns (uint) { + return ethPrice[block.timestamp]; + } +} \ No newline at end of file