add diagnostics for evaluated contracts that succeed

Evaluated contract are contracts that are in scope (with imports), and that have at least one instantiation of their parameters.

Returning “ok” diagnostics allows differentiating between contracts that succeeded because they are true on some configuration of their parameters, from contracts that cannot apply to the current system because they cannot be instantiated.