Verified native-word primitives

Executable native-word primitives are exported with their refinement proofs. Runtime-only clients may import FloatLib.Kernels.FixedWord.Core.Runtime directly.