Library liblayers.compcertx.LiftValueDomain

CompCert passes based on value analysis now require the definition of a mmatch "memory abstraction" predicate. A memory has to inject into itself if the abstract memory state satisfies some well-formedness properties. This requirement is formalized by the compcert.backend.ValueDomain.mmatch_inj property. Unfortunately, it is not possible to prove mmatch_inj directly using the axioms of the CompCert memory model, so in practice, a proof is directly made in compcert.backend.ValueDomainImpl on the concrete memory implementation compcert.common.Memimpl. It should be possible to generalize this property over all lenses to Memimpl.mem. In this file, we are lifting the mmatch_inj property along a lens to a bmem memory model, assuming that mmatch_inj is already specified on bmem. In fact, we have to lift the whole specification of mmatch, not just mmatch_inj (that property alone fails).