Implement arbitrary pre-conditions for Crucible-based LLVM verification

[atomb]

The llvm_assert command from the LSS-based verification interface is missing for the Crucible-based interface. For a number of the examples we have (ZUC, SHA-384), this functionality is necessary to avoid out-of-bounds array accesses.

[brianhuffman]

As a workaround, you can use crucible_equal to encode arbitrary preconditions:

let crucible_assert (t : Term) =
  crucible_equal (crucible_term {{ if t then 0x01 else 0x00 }}) (crucible_term {{ 0x01 }});

But we should definitely add a native crucible_assert; it should be easy to implement.

[atomb]

There is now a crucible_precond command for this purpose. A crucible_postcond command also exists.