We develop a compositional semantics for abstract machines. Starting from the idea that abstract machines should serve as the sole operational semantics, we introduce bimodels, a mathematical structure that abstracts the components of a CK machine by giving denotations to both programs and stacks, and environment bimodels, which extend this to CEK machines with closures and environments. Each admits a syntactic instance, built from the machine itself, and a set-theoretic instance that serves as a denotational semantics. Using biorthogonality we define logical relations over (environment) bimodels and prove a fundamental lemma by a single induction on typing, parametric in the choice of model and observation. Different instantiations yield canonicity, adequacy, a relation equivalent to CIU approximation, denotational extensionality, and a simulation theorem relating the CK and CEK machines, all as corollaries. All results are mechanized in Agda.