This commit completes the Justify testcase with some more
advanced properties.

It provides both an implementation with its specification for
verification, and a synthesis benchmark where choose is used
to try to derive the correct implementation.