Support for invariant testing

[moodmosaic]

An example of how invariant testing works (using just the clarity console) can be found here. You may automate this with a syntax similar to wake's, and using hypothesis for the actual model-based testing (stateful testing) infrastructure.

Essentially, the user defines commands for each one of the public functions of the contract. Each command has essentially 3 methods:

• check given a read-only view of the current, tracked, state, decide whether the action should run
• execute given the current state, and access to the actual system under test (e.g. simnet) run the action and update the model.
• print given a failure, hypothesis's shrinking will kick-in, in this case the user can see something pretty(er) on the screen.

---

Simplest possible example can be found here, and you can run the whole test-suite via npm install && npm test. All tests should pass. — Then, you should modify counter.clar:

diff --git a/contracts/counter.clar b/contracts/counter.clar
index b4a4074..d3428c7 100644
--- a/contracts/counter.clar
+++ b/contracts/counter.clar
@@ -8,7 +8,12 @@
 )
 
 (define-public (increment)
-  (ok (var-set counter (+ (var-get counter) u1)))
+  (let ((current-counter (var-get counter)))
+    (if (> current-counter u1000) ;; Introduce a bug for large values.
+      (ok (var-set counter u0)) ;; Reset counter to zero if it exceeds 1000.
+      (ok (var-set counter (+ current-counter u1)))
+    )
+  )
 )
 
 (define-public (decrement)

and re-run npm test to see the bug being uncovered:

Failed after 2 tests
{ seed: 1037841433, path: "1:1:0", endOnFailure: true }
Counterexample: [get-counter /*replayPath="ABB/HB:l"*/]
Shrunk 2 time(s)
Got error: expected u0 to be u3464859298

Execution summary:
√ [add 1,add 0,add 648371269,get-counter,add 678641022,decrement,add 2061277405 /*replayPath="ABB/HB:l"*/]
× [add 76569602,increment,get-counter /*replayPath="ABB/HB:l"*/]
. √ [ /*replayPath="ABB/HB:l"*/]
. × [get-counter /*replayPath="ABB/HB:l"*/]
. . × [get-counter /*replayPath="ABB/HB:l"*/]