There is no specification, or really documentation, for Miniscript other than sipa's website. There is no "correct" or singular way to compile a miniscript policy into miniscript. The two existing implementations actually go about compiling in different ways, although both arrive at the same result (occasionally they differ, but the two results are semantically the same but are equally optimal). The only thing to be concerned about are whether the miniscript is optimal, and whether it is semantically the same as the policy.
Checking whether it is semantically the same is trivial. A miniscript can be "lifted" into policy by dropping tags and types so it is easy to check that a compiled miniscript is semantically the same as the policy.
Checking whether a given miniscript is optimal generally boils down to its size and expected satisfaction size. Smaller is better, so a miniscript whose end scriptWitness size is the smallest is considered to be optimal. When considering policies that include probabilities, the expected value should be taken into account.
As for compiling from policy into miniscript itself, there are different strategies. One strategy (which I believe is actually done in one of the libraries) is to construct every possible miniscript for a given policy and just select the optimal one.
