The CCR framework unifies refinement and separation logic to provide
ownership-based modular reasoning and transitive incremental reasoning
in open settings that involve unverified code. However, when reasoning
about function invocations, the reasoning principles available to
clients remain confined to pre- and postconditions, which struggle to
capture effectful behaviors such as I/O actions or interactions with
arbitrary unverified code. This limitation becomes particularly acute
in \emph{hybrid verification}, where a mixture of different verification
techniques is applied and some code is never formally verified but
instead tested or model-checked.

To overcome this limitation, we introduce \emph{imaginary
specifications}—a novel notion that freely mixes executable code
with ownership assertions—and reasoning principles for their
use. Through key technical developments, we present CRIS (Contextual
Refinement with Imaginary Specifications), a framework that
generalizes CCR with support for imaginary specifications. We
demonstrate CRIS's expressiveness and reasoning power through examples
involving hybrid verification with unverified code exhibiting arbitrary
side effects such as I/O or divergence, with complete
mechanization in Rocq.