Directed-rounding soundness entry point.

The submodules prove that executable lower/upper rounding operations enclose the corresponding real operations, which is the boundary required by interval and LiRPA proofs.