Add fields on statistics to benchmark JSON

[polytypic]

This PR adds some fields (namely #best, #mean, #median, #sd, #runs) to the benchmark JSON. These fields are ignored by current-bench.