Add runtime operations between lib types and verified types

[mborland]

A verified_u32 is fundamentally a u32. At run time u32 should be able to perform arithmetic operations, and comparisons using what is effectively a same type constant.