Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor (Full Report)