Dense-overlay RAM instruction kernels

This module collects the concrete positive-tag instruction simulators and their exact Hoare/time contracts.