act: add where block

allow definition of per act macro substitutions.

substitution is regex based and occurs as part of klab build.

Author: d-xo

Makefile

@@ -61,7 +61,7 @@ media/%.pdf: media/%.md
 KLAB = $(CURDIR)/bin/klab
 
 # doing them in this order should save time
-examples := $(addprefix examples/,heal multipleCalls token SafeAdd multipleInternals createContract)
+examples := $(addprefix examples/,heal multipleCalls token SafeAdd multipleInternals createContract where)
 
 # this is now redundant
 build-test:

acts.md

@@ -201,4 +201,13 @@ Lists the behaviours that this spec calls. If the listed behaviour's `_pass` pro
 calls
     DSToken.transferFrom
 ```
-    
+
+### where
+Allows for the definition of named expressions. All instances of the name on the LHS of the `where` binding will be expanded to the RHS as part of `klab build`. Helps to reduce duplication in specs for methods that have lots of intermediate variables.
+
+```
+where
+
+    Var := X + Y
+```
+

examples/where/config.json

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

examples/where/dapp/out/dapp.sol.json

@@ -0,0 +1,19 @@
+pragma solidity >=0.4.21;
+
+contract Calculate {
+    function add(uint x, uint y) internal pure returns (uint z) {
+        require((z = x + y) >= x);
+    }
+    function sub(uint x, uint y) internal pure returns (uint z) {
+        require((z = x - y) <= x);
+    }
+    function mul(uint x, uint y) internal pure returns (uint z) {
+        require(y == 0 || (z = x * y) / y == x);
+    }
+
+    function run(uint a, uint b) public pure returns (uint e) {
+        uint c = sub(a, b);
+        uint d = mul(c, b);
+        e = add(d, a);
+    }
+}

examples/where/dapp/src/Calculate.sol

@@ -0,0 +1,5 @@
+```k
+rule A -Word B <=Int A => #rangeUInt(256, A -Int B)
+  requires #rangeUInt(256, A) andBool #rangeUInt(256, B)
+```
+

examples/where/src/lemmas.k.md

@@ -0,0 +1,2 @@
+```smt2
+```

examples/where/src/prelude.smt2.md

@@ -0,0 +1,22 @@
+```act
+behaviour run of Calculate
+interface run(uint256 A, uint256 B)
+
+iff in range uint256
+
+    C
+    D
+    E
+
+iff
+
+    VCallValue == 0
+
+where
+
+    C := A - B
+    D := C * B
+    E := D + C
+
+returns E
+```

examples/where/src/specification.act.md

@@ -430,6 +430,43 @@ const parseAct = config => (act_str, silent = false) => {
         a.returns = returns
       } else if(/^returnsRaw/.test(head)) {
         a.returnsRaw = head.split(" ").slice(1).join(" ")
+      } else if(/^where/.test(head)) {
+          a.whereBindings = tail
+              .map(l => l.trim())
+              .filter(l => l != "")
+              .map(l => mapInterface(a.interface, toK(l).trim()))
+              .map(l => ({
+                /* matches the LHS of the macro if it is:
+                 * preceded by:
+                 *  - ', ' or ','
+                 *  - '('
+                 *  - the start of a line
+                 *  - a tab
+                 *  - a space
+                 * and followed by:
+                 *  - ','
+                 *  - ')'
+                 *  - the end of a line
+                 *  - a tab
+                 *  - a space
+                 *
+                 *  example here: https://regex101.com/r/ZubkN1/3
+                 */
+                "from": new RegExp(`(, ?|\\(|^|\\t| )(${l.split(":=")[0].trim()})(,|\\)|$|\\t| )`, "gm"),
+                /*
+                 * replaces with the first capture group from the expression
+                 * above ('$1'), then the RHS of the macro (surrounded by
+                 * brackets), then the third capture group from above ('$3')
+                 */
+                "to": `$1(${l.split(":=")[1].trim()})$3`
+              }))
+
+            // apply every where binding in turn to every other where binding
+            for (i = 0; i < a.whereBindings.length; i++) {
+              for (j = 0; j < a.whereBindings.length; j++) {
+                a.whereBindings[j].to = a.whereBindings[j].to.replace(a.whereBindings[i].from, a.whereBindings[i].to);
+              }
+            }
       } else if(/^calls/.test(head)) {
           a.calls = tail
               .map(l => l.trim())
@@ -943,6 +980,7 @@ const buildActs = (config, act_proofs) => {
           //     .filter(r => r.file_suffix)
           //     .map(r => r.file_suffix)
           //     .join('\n\n')
+          rule.spec = applyWhereBindings(rule.spec, extractWhereBindings(rule.act))
           const _rules = [rule.spec].concat(rule.ctx.map(r => r.spec  + "\n[trusted]\n"))
           const module = kjson.renderModule(_rules, rule.name) // TODO maybe skip this
           const hash   = config.get_proof_hash({name: rule.name, spec: module});
@@ -979,6 +1017,21 @@ const buildActs = (config, act_proofs) => {
 
 }
 
+// convenience wrapper to ensure we always have something to iterate over when
+// dealing with where bindings
+const extractWhereBindings = (act) => {
+  if (typeof act.whereBindings === "undefined") return []
+  return act.whereBindings
+}
+
+// apply where bindings to the spec
+const applyWhereBindings = (spec, bindings) => {
+  for (const b of bindings) {
+    spec = spec.replace(b.from, b.to)
+  }
+  return spec
+}
+
 module.exports = {
   proofCollection,
   makePrelude,

lib/build.js

@@ -1,7 +1,6 @@
 const path          = require("path")
 const marked        = require("marked");
 const Config        = require("../lib/config.js");
-const {parseAct}    = require("../lib/build.js");
 const {
   testPath,
   read,