[robdockins]

Pull in some submodule updates and start incorporating floating-point support.

This PR adds a new example based on the well-clear violation code from the copilot examples directory. It doesn't currently verify because of Copilot-Language/copilot#263

Independent of that, however, we have an opportunity for improvement here, as the output of the tool currently is:

$ cabal run verify-examples -- WCV
Up to date
=====
== Running the WCV example...
=====

Generated "results/wcv/wcv.c"
Compiled wcv into results/wcv/crux~wcv.bc
Translated bitcode into Crucible
Generating proof state data
Computing initial state verification conditions
Proving initial state verification conditions
All obligations proved by concrete simplification
Computing step bisimulation verification conditions
Proving step bisimulation verification conditions
verify-examples: user error (user error (evalGroundExpr: could not evaluate expression: let uninterpreted_float_lt = ??
    uninterpreted_sbv_to_float = ??
    uninterpreted_float_to_sbv = ??
    -- results/wcv/wcv.c:21:208
    v366 = apply uninterpreted_float_to_sbv 0 crelative_velocity_x_r0@58:bv
    -- results/wcv/wcv.c:21:202
    v373 = ite (bvSlt v366 0x0:[32]) (bvSum (bvMul 0xffffffff:[32] v366)) v366
    -- results/wcv/wcv.c:21:201
    v374 = apply uninterpreted_sbv_to_float 0 v373
 in apply uninterpreted_float_lt v374 0x3f50624dd2f1a9fc:[64])
)

[RyanGlScott]

My apologies for letting this sit for a while. I've merged in the latest changes from main, since they overlap with this PR somewhat. I also pushed a separate commit which includes a workaround for Copilot-Language/copilot#263 so that the WCV example verifies.

The main thrust of the PR looks great. Are there still improvements to be made regarding the error message reporting, or should we just land this?

[robdockins]

We definitely should improve the error reporting, but I don't know it should keep us from landing this. Let's open a ticket.

[RyanGlScott]

I've opened #12 to continue the effort to improve error-message reporting.