Formally verified OSM (#6)

* remove DSStop (and transitively, DSAuth) inheritance

* change bool to uint128 or uint256 in contract storage

* osm.sol: uint64 safe math

* add hop nonzero requirement

* add minimal ValueLike implementation for verification

* use actual ds-value in osm.sol

src/osm.sol

@@ -1,45 +1,57 @@
 pragma solidity >=0.5.2;
 
-import "ds-stop/stop.sol";
+import "ds-value/value.sol";
 
-interface ValueLike {
-    function peek() external returns (bytes32,bool);
-    function read() external returns (bytes32);
-}
-
-contract OSM is DSStop {
+contract OSM {
 
     // --- Auth ---
     mapping (address => uint) public wards;
     function rely(address guy) public auth { wards[guy] = 1; }
     function deny(address guy) public auth { wards[guy] = 0; }
     modifier auth { require(wards[msg.sender] == 1); _; }
 
+    // --- Stop ---
+    uint256 public stopped;
+    modifier stoppable { require(stopped == 0, "OSM-is-stopped"); _; }
+
+    // --- Math ---
+    function add(uint64 x, uint64 y) internal pure returns (uint64 z) {
+        z = x + y;
+        require(z >= x);
+    }
+
     address public src;
-    uint16 constant ONE_HOUR = uint16(3600);
-    uint16 public hop = ONE_HOUR;
-    uint64 public zzz;
+    uint16  constant ONE_HOUR = uint16(3600);
+    uint16  public hop = ONE_HOUR;
+    uint64  public zzz;
 
     struct Feed {
         uint128 val;
-        bool    has;
+        uint128 has;
     }
 
     Feed cur;
     Feed nxt;
 
     // Whitelisted contracts, set by an auth
-    mapping (address => bool) public bud;
+    mapping (address => uint256) public bud;
 
-    modifier toll { require(bud[msg.sender], "contract-is-not-whitelisted"); _; }
+    modifier toll { require(bud[msg.sender] == 1, "contract-is-not-whitelisted"); _; }
 
     event LogValue(bytes32 val);
 
     constructor (address src_) public {
         wards[msg.sender] = 1;
         src = src_;
     }
-
+
+    function stop() public auth {
+        stopped = 1;
+    }
+    function start() public auth {
+        stopped = 0;
+    }
+
     function change(address src_) external auth {
         src = src_;
     }
@@ -49,6 +61,7 @@ contract OSM is DSStop {
     }
 
     function prev(uint ts) internal view returns (uint64) {
+        require(hop != 0);
         return uint64(ts - (ts % hop));
     }
 
@@ -58,44 +71,44 @@ contract OSM is DSStop {
     }
 
     function void() external auth {
-        cur = nxt = Feed(0, false);
-        stopped = true;
+        cur = nxt = Feed(0, 0);
+        stopped = 1;
     }
 
     function pass() public view returns (bool ok) {
-        return era() >= zzz + hop;
+        return era() >= add(zzz, hop);
     }
 
     function poke() external stoppable {
         require(pass(), "not-passed");
-        (bytes32 wut, bool ok) = ValueLike(src).peek();
+        (bytes32 wut, bool ok) = DSValue(src).peek();
         if (ok) {
             cur = nxt;
-            nxt = Feed(uint128(uint(wut)), ok);
+            nxt = Feed(uint128(uint(wut)), 1);
             zzz = prev(era());
             emit LogValue(bytes32(uint(cur.val)));
         }
     }
 
     function peek() external view toll returns (bytes32,bool) {
-        return (bytes32(uint(cur.val)), cur.has);
+        return (bytes32(uint(cur.val)), cur.has == 1);
     }
 
     function peep() external view toll returns (bytes32,bool) {
-        return (bytes32(uint(nxt.val)), nxt.has);
+        return (bytes32(uint(nxt.val)), nxt.has == 1);
     }
 
     function read() external view toll returns (bytes32) {
-        require(cur.has, "no-current-value");
+        require(cur.has == 1, "no-current-value");
         return (bytes32(uint(cur.val)));
     }
 
     function kiss(address a) external auth {
         require (a != address(0), "no-contract-0");
-        bud[a] = true;
+        bud[a] = 1;
     }
 
     function diss(address a) external auth {
-        bud[a] = false;
+        bud[a] = 0;
     }
 }

src/osm.t.sol

@@ -41,7 +41,7 @@ contract OSMTest is DSTest {
     }
 
     function testVoid() public {
-        assertTrue(!osm.stopped());                             //verify osm is active
+        assertTrue(osm.stopped() == 0);                         //verify osm is active
         osm.kiss(address(this));                                //whitelist caller
         hevm.warp(uint(osm.hop() * 2));                         //warp 2 hops
         osm.poke();                                             //set new curent and next osm value
@@ -52,7 +52,7 @@ contract OSMTest is DSTest {
         assertEq(uint(val), 100 ether);                         //verify next osm value is 100
         assertTrue(has);                                        //verify next osm value is valid
         osm.void();                                             //void all osm values
-        assertTrue(osm.stopped());                              //verify osm is inactive
+        assertTrue(osm.stopped() == 1);                         //verify osm is inactive
         (val, has) = osm.peek();                                //pull current osm value
         assertEq(uint(val), 0);                                 //verify current osm value is 0
         assertTrue(!has);                                       //verify current osm value is invalid
@@ -107,15 +107,15 @@ contract OSMTest is DSTest {
     }
 
     function testKiss() public {
-        assertTrue(!osm.bud(address(this)));                    //verify caller is not whitelisted
+        assertTrue(osm.bud(address(this)) == 0);                //verify caller is not whitelisted
         osm.kiss(address(this));                                //whitelist caller
-        assertTrue(osm.bud(address(this)));                     //verify caller is whitelisted
+        assertTrue(osm.bud(address(this)) == 1);                //verify caller is whitelisted
     }
 
     function testDiss() public {
         osm.kiss(address(this));                                //whitelist caller
-        assertTrue(osm.bud(address(this)));                     //verify caller is whitelisted
+        assertTrue(osm.bud(address(this)) == 1);                //verify caller is whitelisted
         osm.diss(address(this));                                //remove caller from whitelist
-        assertTrue(!osm.bud(address(this)));                    //verify caller is not whitelisted
+        assertTrue(osm.bud(address(this)) == 0);                //verify caller is not whitelisted
     }
 }

src/value.sol

@@ -0,0 +1,25 @@
+/// value.sol - minimal ValueLike implementation for verification
+
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU General Public License for more details.
+
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+pragma solidity >=0.5.6;
+
+contract Value {
+    bool    has;
+    bytes32 val;
+
+    function peek() public view returns (bytes32, bool) {
+        return (val,has);
+    }
+}