FV add warnings to symbolic eval

[rsoeldner]

This PR aims to enable warning emission during model building (and later shimming), which was previously only possible through translation to the FV AST.

One benefit of this is the ability to remove the static knowledge requirement for the parameter in hash, which has limited the use of the FV system in real-world contract verification, as pointed out by @EnoF

Specifically, the use of hash requires statically known content. Prior to this PR, we failed verification for dynamic content (i.e. table reads). Now we check, if the data is statically known, we compute the hash, otherwise we pick (depending on the type) shimmed values and emit a warning that we did so.

This is not optimal, but usually you are not interested in verifying a specific hash value.

[jwiegley]

What is the test coverage to ensure that none of this interferes with how the code worked before?

[rsoeldner]

What is the test coverage to ensure that none of this interferes with how the code worked before?

These modifications still passes the test-suite. Additionally, I added:

• Tests about the new shimmed values
• Repl output test indicating a warning to the user (for strings)

[imalsogreg]

Would you mind adding some examples into the PR description?

• The previous behavior/outputs being preserved in happy path (no FV error)
• The previous behavior/outputs being preserved under FV error
• The new behavior with warnings emmitted

Other than wanting to see these, the PR looks good to me. I couple nits and a couple suggestions.

[imalsogreg]

The following REPL session looks good to me:

pact> (module m g (defcap g () true) (defun test: string (x: integer)
....>                @model [(property (not (= result "")))]
....>                (hash x)))
"Loaded module m, hash S3g2Lou829zTfcRLArFv_dhnPj9xhFlI4e7Ij1J_oP0"
pact> (verify 'm)
"Verification of m succeeded"
:OutputWarning: Shimmed native 'hash' (of type 'integer', substitute 'A_fIcwIweiXXYXnKU59CNCAUoIXHXwQtB_D8xhEflLY'))