// SPDX-License-Identifier: UNLICENSED
pragma solidity =0.7.6;
pragma abicoder v2;

import "./OracleTest.sol";

contract OracleEchidnaTest {
    OracleTest private oracle;

    bool private initialized;
    uint32 private timePassed;

    constructor() {
        oracle = new OracleTest();
    }

    function initialize(uint32 time, int24 tick, uint128 liquidity) external {
        oracle.initialize(
            OracleTest.InitializeParams({
                time: time,
                tick: tick,
                liquidity: liquidity
            })
        );
        initialized = true;
    }

    function limitTimePassed(uint32 by) private {
        require(timePassed + by >= timePassed);
        timePassed += by;
    }

    function advanceTime(uint32 by) public {
        limitTimePassed(by);
        oracle.advanceTime(by);
    }

    // write an observation, then change tick and liquidity
    function update(
        uint32 advanceTimeBy,
        int24 tick,
        uint128 liquidity
    ) external {
        limitTimePassed(advanceTimeBy);
        oracle.update(
            OracleTest.UpdateParams({
                advanceTimeBy: advanceTimeBy,
                tick: tick,
                liquidity: liquidity
            })
        );
    }

    function grow(uint16 cardinality) external {
        oracle.grow(cardinality);
    }

    function checkTimeWeightedResultAssertions(
        uint32 secondsAgo0,
        uint32 secondsAgo1
    ) private view {
        require(secondsAgo0 != secondsAgo1);
        require(initialized);
        // secondsAgo0 should be the larger one
        if (secondsAgo0 < secondsAgo1)
            (secondsAgo0, secondsAgo1) = (secondsAgo1, secondsAgo0);

        uint32 timeElapsed = secondsAgo0 - secondsAgo1;

        uint32[] memory secondsAgos = new uint32[](2);
        secondsAgos[0] = secondsAgo0;
        secondsAgos[1] = secondsAgo1;

        (
            int56[] memory tickCumulatives,
            uint160[] memory secondsPerLiquidityCumulativeX128s,
            uint192[] memory rewardPerLiquidityCumulativeX64s
        ) = oracle.observe(secondsAgos);
        int56 timeWeightedTick = (tickCumulatives[1] - tickCumulatives[0]) /
            timeElapsed;
        uint256 timeWeightedHarmonicMeanLiquidity = (uint256(timeElapsed) *
            type(uint160).max) /
            (uint256(
                secondsPerLiquidityCumulativeX128s[1] -
                    secondsPerLiquidityCumulativeX128s[0]
            ) << 32);
        assert(timeWeightedHarmonicMeanLiquidity <= type(uint128).max);
        assert(timeWeightedTick <= type(int24).max);
        assert(timeWeightedTick >= type(int24).min);
    }

    function echidna_indexAlwaysLtCardinality() external view returns (bool) {
        return oracle.index() < oracle.cardinality() || !initialized;
    }

    function echidna_AlwaysInitialized() external view returns (bool) {
        (, , , bool isInitialized, ) = oracle.observations(0);
        return oracle.cardinality() == 0 || isInitialized;
    }

    function echidna_cardinalityAlwaysLteNext() external view returns (bool) {
        return oracle.cardinality() <= oracle.cardinalityNext();
    }

    function echidna_canAlwaysObserve0IfInitialized()
        external
        view
        returns (bool)
    {
        if (!initialized) {
            return true;
        }
        uint32[] memory arr = new uint32[](1);
        arr[0] = 0;
        (bool success, ) = address(oracle).staticcall(
            abi.encodeWithSelector(OracleTest.observe.selector, arr)
        );
        return success;
    }

    function checkTwoAdjacentObservationsTickCumulativeModTimeElapsedAlways0(
        uint16 index
    ) external view {
        uint16 cardinality = oracle.cardinality();
        // check that the observations are initialized, and that the index is not the oldest observation
        require(
            index < cardinality && index != (oracle.index() + 1) % cardinality
        );

        (
            uint32 blockTimestamp0,
            int56 tickCumulative0,
            ,
            bool initialized0,

        ) = oracle.observations(index == 0 ? cardinality - 1 : index - 1);
        (
            uint32 blockTimestamp1,
            int56 tickCumulative1,
            ,
            bool initialized1,

        ) = oracle.observations(index);

        require(initialized0);
        require(initialized1);

        uint32 timeElapsed = blockTimestamp1 - blockTimestamp0;
        assert(timeElapsed > 0);
        assert((tickCumulative1 - tickCumulative0) % timeElapsed == 0);
    }

    function checkTimeWeightedAveragesAlwaysFitsType(
        uint32 secondsAgo
    ) external view {
        require(initialized);
        require(secondsAgo > 0);
        uint32[] memory secondsAgos = new uint32[](2);
        secondsAgos[0] = secondsAgo;
        secondsAgos[1] = 0;
        (
            int56[] memory tickCumulatives,
            uint160[] memory secondsPerLiquidityCumulativeX128s,
            uint192[] memory rewardPerLiquidityCumulativeX64s
        ) = oracle.observe(secondsAgos);

        // compute the time weighted tick, rounded towards negative infinity
        int56 numerator = tickCumulatives[1] - tickCumulatives[0];
        int56 timeWeightedTick = numerator / int56(secondsAgo);
        if (numerator < 0 && numerator % int56(secondsAgo) != 0) {
            timeWeightedTick--;
        }

        // the time weighted averages fit in their respective accumulated types
        assert(
            timeWeightedTick <= type(int24).max &&
                timeWeightedTick >= type(int24).min
        );

        uint256 timeWeightedHarmonicMeanLiquidity = (uint256(secondsAgo) *
            type(uint160).max) /
            (uint256(
                secondsPerLiquidityCumulativeX128s[1] -
                    secondsPerLiquidityCumulativeX128s[0]
            ) << 32);
        assert(timeWeightedHarmonicMeanLiquidity <= type(uint128).max);
    }
}