FV (WIP do not merge)

config.json

@@ -0,0 +1,16 @@
+{
+  "name": "ds-pause",
+  "src": {
+    "specification": "spec/spec.act.md",
+    "smt_prelude": "spec/prelude.smt2.md",
+    "rules": [
+      "spec/lemmas.k.md"
+    ]
+  },
+  "implementations": {
+    "DSPause": {
+      "src": "src/pause.sol"
+    }
+  },
+  "dapp_root": "."
+}

readme.md

@@ -14,6 +14,20 @@ time.
 time to respond to decisions. If those affected by governance decisions have e.g. exit or veto
 rights, then the pause can serve as an effective check on governance power.
 
+## Specification
+
+An executable formal specification of `DSPause` written in the klab
+[`act`](https://github.com/dapphub/klab/blob/master/acts.md) format is provided in the `spec`
+folder.
+
+To verify the generated bytecode against this spec, run the following from the repo root:
+
+```sh
+dapp build
+klab build
+klab prove-all
+```
+
 ## Plans
 
 A `plan` describes a single `delegatecall` operation and a unix timestamp `eta` before which it
@@ -101,8 +115,3 @@ pause.plot(usr, tag, fax, eta);
 bytes memory out = pause.exec(usr, tag, fax, eta);
 ```
 
-## Tests
-
-- [`pause.t.sol`](./pause.t.sol): unit tests
-- [`integration.t.sol`](./integration.t.sol): usage examples / integation tests
-

spec/lemmas.k.md

@@ -0,0 +1,65 @@
+# Storage
+
+Syntax for storage access.
+
+```k
+syntax Int ::= "#DSPause.wards" "[" Int "]" [function]
+rule #DSPause.wards[A] => #hashedLocation("Solidity", 0, A)
+
+syntax Int ::= "#DSPause.plans" "[" Int "]" [function]
+rule #DSPause.plans[A] => #hashedLocation("Solidity", 1, A)
+
+syntax Int ::= "#DSPause.proxy" [function]
+rule #DSPause.proxy => 2
+
+syntax Int ::= "#DSPause.delay" [function]
+rule #DSPause.delay => 3
+```
+
+Assume that keccack will never output an `Int` between 0 and 10.
+
+```k
+rule keccak(A) ==K B => false
+     requires B <=Int 10
+```
+
+# Plans
+
+Syntax for computing `plan` ids.
+
+```k
+syntax Int ::= #hash(Int, Int, WordStack, Int) [function]
+rule #hash(Usr, Tag, Fax, Eta) => keccak(#encodeArgs(#address(Usr), #bytes32(Tag), #bytes(Fax), #uint256(Eta)))
+```
+
+# Calldata
+
+## Layout
+
+calldata for `plot` / `drop` / `exec` is layed out as follows:
+
+1. `04 bytes` : `function selector`
+1. `32 bytes` : `usr`
+1. `32 bytes` : `tag`
+1. `32 bytes` : `pointer to fax`
+1. `32 bytes` : `eta`
+1. `32 bytes` : `size of fax`
+1. `symbolic` : `fax`
+1. `symbolic` : `padding for fax (to word boundry, max 31 bytes)`
+1. `symbolic` : `excess calldata (CD)`
+
+## Size Calculations
+
+These lemmas help `K` simplify terms that make calculations about calldata size. They are required as
+both `chop` and `#ceil32` are `[concrete]` and so cannot be rewritten if they have symbolic values
+as their arguments.
+
+```k
+rule ((164 <=Int chop((4 +Int (sizeWordStackAux((F ++ (#padToWidth((#ceil32(sizeWordStackAux(F, 0)) -Int sizeWordStackAux(F, 0)), .WordStack) ++ C)), 0) +Int 160))))) => true
+  requires #sizeWordStack(F) <=Int 64
+   andBool #sizeWordStack(C) <=Int 64
+
+rule (((164 +Int sizeWordStackAux(F, 0)) <=Int chop((4 +Int (sizeWordStackAux((F ++ (#padToWidth((#ceil32(sizeWordStackAux(F, 0)) -Int sizeWordStackAux(F, 0)), .WordStack) ++ C)), 0) +Int 160))))) => true
+  requires #sizeWordStack(F) <=Int 64
+   andBool #sizeWordStack(C) <=Int 64
+```

spec/prelude.smt2.md

@@ -0,0 +1,79 @@
+```smt2
+
+
+(set-option :auto-config false)
+(set-option :smt.mbqi false)
+;(set-option :smt.mbqi.max_iterations 15)
+
+; (set-option :auto-config false)
+; (set-option :smt.mbqi false)
+; (set-option :smt.array.extensional false)
+
+; int extra
+(define-fun int_max ((x Int) (y Int)) Int (ite (< x y) y x))
+(define-fun int_min ((x Int) (y Int)) Int (ite (< x y) x y))
+(define-fun int_abs ((x Int)) Int (ite (< x 0) (- 0 x) x))
+
+; bool to int
+(define-fun smt_bool2int ((b Bool)) Int (ite b 1 0))
+
+; ceil32
+(define-fun ceil32 ((x Int)) Int ( * ( div ( + x 31 ) 32 ) 32 ) )
+
+;; pow256 and pow255
+(define-fun pow256 () Int
+  115792089237316195423570985008687907853269984665640564039457584007913129639936)
+(define-fun pow255 () Int
+  57896044618658097711785492504343953926634992332820282019728792003956564819968)
+;; weird declaration trick (doesn't seem to be needed currently)
+;; (declare-fun pow256 () Int)
+;; (assert (>= pow256 115792089237316195423570985008687907853269984665640564039457584007913129639936))
+;; (assert (<= pow256 115792089237316195423570985008687907853269984665640564039457584007913129639936))
+
+;; signed word arithmetic definitions:
+;; integer to word:
+(define-fun unsigned ((x Int)) Int
+  (if (>= x 0)
+      x
+    (+ x pow256)))
+
+;; word to integer
+(define-fun signed ((x Int)) Int
+  (if (< x pow255)
+      x
+    (- x pow256)))
+
+;; signed_abs
+(define-fun signed_abs ((x Int)) Int
+  (if (< x pow255)
+      x
+    (- pow256 x)))
+
+;; signed_sgn
+(define-fun signed_sgn ((x Int)) Int
+  (if (< x pow255)
+      1
+    -1))
+
+;; smt_rpow
+(declare-fun smt_rpow (Int Int Int Int) Int)
+(assert (forall ((z Int) (x Int) (y Int) (b Int)) (! (=> (= y 1) (= (smt_rpow z x y b) (div (+ (* z x) (div b 2)) b))) :pattern ((smt_rpow z x y b)))))
+
+(assert (forall ((z1 Int) (z2 Int) (x1 Int) (y1 Int) (x2 Int) (y2 Int) (b1 Int) (b2 Int))
+  (!
+    (=> (and (<= z1 z2) (<= x1 x2) (<= y1 y2) (<= b1 b2))
+      (<= (smt_rpow z1 x1 y1 b1) (smt_rpow z2 x2 y2 b2))
+    )
+    :pattern ((smt_rpow z1 x1 y1 b1) (smt_rpow z2 x2 y2 b2))
+  )
+))
+
+(assert (forall ((z Int) (x Int) (y Int) (b Int)) (! (=> (>= y 1) (>= (* (smt_rpow z x y b) b) (* z x))) :pattern ((smt_rpow z x y b)))))
+(assert (forall ((z Int) (x Int) (y Int) (b Int)) (! (=> (>= y 2) (>= (* (smt_rpow z x y b) b) (* x x))) :pattern ((smt_rpow z x y b)))))
+
+(assert (forall ((z Int) (x Int) (y Int) (b Int)) (! (=> (>= y 1) (>= (* (smt_rpow z x y b) b) (+ (* z x) (div b 2)))) :pattern ((smt_rpow z x y b)))))
+(assert (forall ((z Int) (x Int) (y Int) (b Int)) (! (=> (>= y 2) (>= (* (smt_rpow z x y b) b) (+ (* x x) (div b 2)))) :pattern ((smt_rpow z x y b)))))
+;
+; end of prelude
+;
+```

spec/spec.act.md

@@ -0,0 +1,195 @@
+# Specification
+
+## Getters
+
+### `wards`
+
+```act
+behaviour wards of DSPause
+interface wards(address usr)
+
+types
+
+  Can: uint256
+
+storage
+
+  wards[usr] |-> Can
+
+iff
+
+  VCallValue == 0
+
+returns Can
+```
+
+### `plans`
+
+```act
+behaviour plans of DSPause
+interface plans(bytes32 id)
+
+types
+
+  Plan: uint256
+
+storage
+
+  plans[id] |-> Plan
+
+iff
+
+  VCallValue == 0
+
+returns Plan
+```
+
+### `proxy`
+
+```act
+behaviour proxy of DSPause
+interface proxy()
+
+types
+
+  Proxy: address
+
+storage
+
+  proxy |-> Proxy
+
+iff
+
+  VCallValue == 0
+
+returns Proxy
+```
+
+### `delay`
+
+```act
+behaviour delay of DSPause
+interface delay()
+
+types
+
+  Delay: uint256
+
+storage
+
+  delay |-> Delay
+
+iff
+
+  VCallValue == 0
+
+returns Delay
+```
+
+## Admin
+
+### `rely`
+
+```act
+behaviour rely of DSPause
+interface rely(address usr)
+
+types
+
+  Can: uint256
+  Proxy: address
+
+storage
+
+  wards[usr] |-> Can => 1
+  proxy |-> Proxy
+
+iff
+
+  VCallValue == 0
+  CALLER_ID == Proxy
+```
+
+### `deny`
+
+```act
+behaviour deny of DSPause
+interface deny(address usr)
+
+types
+
+  Can: uint256
+  Proxy: address
+
+storage
+
+  wards[usr] |-> Can => 0
+  proxy |-> Proxy
+
+iff
+
+  VCallValue == 0
+  CALLER_ID == Proxy
+```
+
+### `file`
+
+```act
+behaviour file of DSPause
+interface file(uint data)
+
+types
+
+  Delay: uint256
+  Proxy: address
+
+storage
+
+  delay |-> Delay => data
+  proxy |-> Proxy
+
+iff
+
+  VCallValue == 0
+  CALLER_ID == Proxy
+```
+
+## Operations
+
+### `plot`
+
+```act
+behaviour plot of DSPause
+interface plot(address usr, bytes32 tag, bytes fax, uint eta)
+
+types
+
+  Can: uint256
+  Delay: uint256
+  Plotted: uint256
+
+storage
+
+  delay |-> Delay
+  wards[CALLER_ID] |-> Can
+  plans[#hash(usr, tag, fax, eta)] |-> Plotted => 1
+
+iff in range uint256
+
+  TIME + Delay
+
+iff
+
+  Can == 1
+  VCallValue == 0
+  eta >= TIME + Delay
+
+if
+
+  sizeWordStackAux(fax, 0) == 64
+  sizeWordStackAux(CD, 0) == 64
+```
+
+### `drop`
+
+### `exec`