Vec arrays

[yav]

This PR wraps the vectors used to implement Crucible vector values with a newtype, which should allow us to support more representations in the future (e.g., vectors backed by SMT arrays, which would be useful for uninterpreted functions returning vectors)

[RyanGlScott]

Do you always expect this class to have exactly one instance? If so, my preference would be to move the definition of RegValue' to another module to avoid recursive module dependencies, rather than complicating all of the type signatures in this module with yet another type class.

[RyanGlScott]

For symmetry with the VecSize class, it might be worth factoring out the IsExprBuilder sym constraint into a superclass, i.e.,

Suggested change

	class MonadIO m => VecMonad sym m where
	-- | We use this for partial operations (e.g., indexing a vector out of bounds).
	vecAbort :: IsSymBackend sym bak => bak -> SimErrorReason -> m a
	-- | A pre-condition on the current operation. Assertions we generate
	-- are conditional on this.
	vecPre :: IsExprBuilder sym => sym -> m (Pred sym)
	class (IsExprBuilder sym, MonadIO m) => VecMonad sym m where
	-- | We use this for partial operations (e.g., indexing a vector out of bounds).
	vecAbort :: IsSymBackend sym bak => bak -> SimErrorReason -> m a
	-- | A pre-condition on the current operation. Assertions we generate
	-- are conditional on this.
	vecPre :: sym -> m (Pred sym)

[RyanGlScott]

The name of this module is "VecValue", but this data type is named "VecVal". For consistency, it would be nice to use the same name throughout. My personal preference would be "VecValue", as it more closely aligns with the names of other types in Crucible (e.g., RegValue and AtomValue).