feat: invariants compile and have a few TS tests

test/recon/Properties.sol

@@ -8,5 +8,6 @@ import {OptimizationProperties} from "./properties/OptimizationProperties.sol";
 import {BribeInitiativeProperties} from "./properties/BribeInitiativeProperties.sol";
 import {SynchProperties} from "./properties/SynchProperties.sol";
 import {RevertProperties} from "./properties/RevertProperties.sol";
+import {TsProperties} from "./properties/TsProperties.sol";
 
-abstract contract Properties is OptimizationProperties, BribeInitiativeProperties, SynchProperties, RevertProperties {}
+abstract contract Properties is OptimizationProperties, BribeInitiativeProperties, SynchProperties, RevertProperties, TsProperties {}

test/recon/Setup.sol

@@ -43,6 +43,8 @@ abstract contract Setup is BaseSetup {
     uint32 internal constant EPOCH_DURATION = 604800;
     uint32 internal constant EPOCH_VOTING_CUTOFF = 518400;
 
+    uint120 magnifiedStartTS;
+
     function setup() internal virtual override {
         vm.warp(block.timestamp + EPOCH_DURATION * 4); // Somehow Medusa goes back after the constructor
         // Random TS that is realistic
@@ -91,6 +93,8 @@ abstract contract Setup is BaseSetup {
         deployedInitiatives.push(address(initiative1));
 
         governance.registerInitiative(address(initiative1));
+
+        magnifiedStartTS = uint120(block.timestamp) * uint120(1e18);
     }
 
     function _getDeployedInitiative(uint8 index) internal view returns (address initiative) {

test/recon/properties/BribeInitiativeProperties.sol

@@ -66,7 +66,7 @@ abstract contract BribeInitiativeProperties is BeforeAfter {
 
             (uint88 voteLQTY,, uint16 epoch) = governance.lqtyAllocatedByUserToInitiative(user, deployedInitiatives[i]);
 
-            try initiative.lqtyAllocatedByUserAtEpoch(user, epoch) returns (uint88 amt, uint32) {
+            try initiative.lqtyAllocatedByUserAtEpoch(user, epoch) returns (uint88 amt, uint120) {
                 eq(voteLQTY, amt, "Allocation must match");
             } catch {
                 t(false, "Allocation doesn't match governance");
@@ -202,10 +202,10 @@ abstract contract BribeInitiativeProperties is BeforeAfter {
             IBribeInitiative initiative = IBribeInitiative(deployedInitiatives[i]);
             uint256 sumOfPower;
             for (uint8 j; j < users.length; j++) {
-                (uint88 lqtyAllocated, uint32 userTS) = initiative.lqtyAllocatedByUserAtEpoch(users[j], currentEpoch);
+                (uint88 lqtyAllocated, uint120 userTS) = initiative.lqtyAllocatedByUserAtEpoch(users[j], currentEpoch);
                 sumOfPower += governance.lqtyToVotes(lqtyAllocated, userTS, uint32(block.timestamp));
             }
-            (uint88 totalLQTYAllocated, uint32 totalTS) = initiative.totalLQTYAllocatedByEpoch(currentEpoch);
+            (uint88 totalLQTYAllocated, uint120 totalTS) = initiative.totalLQTYAllocatedByEpoch(currentEpoch);
 
             uint256 totalRecordedPower = governance.lqtyToVotes(totalLQTYAllocated, totalTS, uint32(block.timestamp));
 

test/recon/properties/GovernanceProperties.sol

@@ -217,16 +217,16 @@ abstract contract GovernanceProperties is BeforeAfter {
             for (uint256 j; j < users.length; j++) {
                 (uint88 userVoteLQTY,,) = governance.lqtyAllocatedByUserToInitiative(users[j], deployedInitiatives[i]);
                 // TODO: double check that okay to use this average timestamp
-                (, uint32 averageStakingTimestamp) = governance.userStates(users[j]);
+                (, uint120 averageStakingTimestamp) = governance.userStates(users[j]);
                 // add the weight calculated for each user's allocation to the accumulator
                 userWeightAccumulatorForInitiative +=
-                    governance.lqtyToVotes(userVoteLQTY, block.timestamp, averageStakingTimestamp);
+                    governance.lqtyToVotes(userVoteLQTY, uint120(block.timestamp) * uint120(1e18), averageStakingTimestamp);
             }
 
-            (uint88 initiativeVoteLQTY,, uint32 initiativeAverageStakingTimestampVoteLQTY,,) =
+            (uint88 initiativeVoteLQTY,, uint120 initiativeAverageStakingTimestampVoteLQTY,,) =
                 governance.initiativeStates(deployedInitiatives[i]);
             uint240 initiativeWeight =
-                governance.lqtyToVotes(initiativeVoteLQTY, block.timestamp, initiativeAverageStakingTimestampVoteLQTY);
+                governance.lqtyToVotes(initiativeVoteLQTY, uint120(block.timestamp) * uint120(1e18), initiativeAverageStakingTimestampVoteLQTY);
 
             acc[i].userSum = userWeightAccumulatorForInitiative;
             acc[i].initiativeWeight = initiativeWeight;
@@ -400,13 +400,13 @@ abstract contract GovernanceProperties is BeforeAfter {
         // GET state and initiative data before allocation
         (   
             uint88 totalCountedLQTY,
-            uint32 user_countedVoteLQTYAverageTimestamp 
+            uint120 user_countedVoteLQTYAverageTimestamp 
         ) = governance.globalState();
         (
             uint88 voteLQTY,
             uint88 vetoLQTY,
-            uint32 averageStakingTimestampVoteLQTY,
-            uint32 averageStakingTimestampVetoLQTY,
+            uint120 averageStakingTimestampVoteLQTY,
+            uint120 averageStakingTimestampVetoLQTY,
 
         ) = governance.initiativeStates(targetInitiative);
 
@@ -427,11 +427,11 @@ abstract contract GovernanceProperties is BeforeAfter {
 
         // Deposit (Changes total LQTY an hopefully also changes ts)
         {
-            (, uint32 averageStakingTimestamp1) = governance.userStates(user);
+            (, uint120 averageStakingTimestamp1) = governance.userStates(user);
 
             lqtyAmount = uint88(lqtyAmount % lqty.balanceOf(user));
             governance.depositLQTY(lqtyAmount);
-            (, uint32 averageStakingTimestamp2) = governance.userStates(user);
+            (, uint120 averageStakingTimestamp2) = governance.userStates(user);
 
             require(averageStakingTimestamp2 > averageStakingTimestamp1, "Must have changed");
         }
@@ -446,13 +446,13 @@ abstract contract GovernanceProperties is BeforeAfter {
         {
             (   
                 uint88 after_totalCountedLQTY,
-                uint32 after_user_countedVoteLQTYAverageTimestamp 
+                uint120 after_user_countedVoteLQTYAverageTimestamp 
             ) = governance.globalState();
             (
                 uint88 after_voteLQTY,
                 uint88 after_vetoLQTY,
-                uint32 after_averageStakingTimestampVoteLQTY,
-                uint32 after_averageStakingTimestampVetoLQTY,
+                uint120 after_averageStakingTimestampVoteLQTY,
+                uint120 after_averageStakingTimestampVetoLQTY,
 
             ) = governance.initiativeStates(targetInitiative);
 

test/recon/properties/SynchProperties.sol

@@ -20,7 +20,7 @@ abstract contract SynchProperties is BeforeAfter {
                 (uint88 votes, , uint16 epoch) = governance.lqtyAllocatedByUserToInitiative(users[j], deployedInitiatives[i]);
 
                 // Grab epoch from initiative
-                (uint88 lqtyAllocatedByUserAtEpoch, uint32 ts) =
+                (uint88 lqtyAllocatedByUserAtEpoch, uint120 ts) =
                     IBribeInitiative(deployedInitiatives[i]).lqtyAllocatedByUserAtEpoch(users[j], epoch);
 
                 // Check that TS matches (only for votes)
@@ -29,7 +29,7 @@ abstract contract SynchProperties is BeforeAfter {
                 if(votes != 0) {
                     // if we're voting and the votes are different from 0
                     // then we check user TS
-                    (, uint32 averageStakingTimestamp) = governance.userStates(users[j]);
+                    (, uint120 averageStakingTimestamp) = governance.userStates(users[j]);
 
                     eq(averageStakingTimestamp, ts, "Timestamp must be most recent when it's non zero");
                 } else {

test/recon/properties/TsProperties.sol

@@ -0,0 +1,34 @@
+// SPDX-License-Identifier: GPL-2.0
+pragma solidity ^0.8.0;
+
+import {BeforeAfter} from "../BeforeAfter.sol";
+import {Governance} from "src/Governance.sol";
+import {IGovernance} from "src/interfaces/IGovernance.sol";
+import {IBribeInitiative} from "src/interfaces/IBribeInitiative.sol";
+
+abstract contract TsProperties is BeforeAfter {
+    // Properties that ensure that a user TS is somewhat sound
+
+    function property_user_ts_is_always_greater_than_start() public {
+        for(uint256 i; i < users.length; i++) {
+            (uint88 user_allocatedLQTY, uint120 userTs) = governance.userStates(users[i]);
+            if(user_allocatedLQTY > 0) {
+                gte(userTs, magnifiedStartTS, "User ts must always be GTE than start");
+            } 
+        }
+    }
+
+    function property_global_ts_is_always_greater_than_start() public {
+        (
+            uint88 totalCountedLQTY,
+            uint120 globalTs
+        ) = governance.globalState();
+
+        if(totalCountedLQTY > 0) {
+            gte(globalTs, magnifiedStartTS, "Global ts must always be GTE than start");
+        } 
+    }
+
+
+
+}

test/recon/targets/GovernanceTargets.sol

@@ -106,6 +106,19 @@ abstract contract GovernanceTargets is BaseTargetFunctions, Properties {
         eq(user_allocatedLQTY, 0, "User has 0 allocated on a reset");
     }
 
+    function depositTsIsRational(uint88 lqtyAmount) public withChecks {
+        (uint88 user_allocatedLQTY,) = governance.userStates(user);
+
+        // Deposit on zero
+        if(user_allocatedLQTY == 0) {
+            lqtyAmount = uint88(lqtyAmount % lqty.balanceOf(user));
+            governance.depositLQTY(lqtyAmount);
+
+            // assert that user TS is now * WAD
+            (, uint120 ts) = governance.userStates(user);
+            eq(ts, block.timestamp * 1e18, "User TS is scaled by WAD");
+        }
+    }
     function depositMustFailOnNonZeroAlloc(uint88 lqtyAmount) public withChecks {
         (uint88 user_allocatedLQTY,) = governance.userStates(user);