Second version of the cost Hoare logic. Here are the objectives of
this new version (some are still [WIP]):
- 1) removed the "flattened" semantics of cost vectors
- 2) [WIP] less boilerplate, better user interaction
- 3) [WIP] use cost information in other Hoare logics

1) No flattened semantics:
   - the previous semantics flattened the cost vectors, i.e.
     `{42, A.f: 2}` was to be understood as the integer `42 + 2 *
     intr_A.f` where `intr_A.f` is the intrinsic cost of `A.f`.
     This flattened semantics prevent from ignoring the concrete cost
     of a procedure (setting it to be at most +infinity), while still
     bounding the number of calls to some specific module parameters
     or abstract modules.

   - previous point necessary to use cost information in other Hoare
     logics (especially to remove counting wrappers), while ignoring
     the concrete cost.

   - in some settings (e.g. quantum, information theoretic arguments,
     rejection samplings), the worst-case concrete cost may be
     unbounded. It is therefore crucial to get rid of the flattened
     semantics to apply the cost logic in these settings

2) Less boilerplate (still [WIP]):
   - w.r.t. the old approach, which requires to write, for every pair of
     procedure and oracle procedure, the number of times the former
     can call the latter
     => somehow quadratic number of constants to introduce/write

   - no new boilerplate added even though we prove more.
     Indeed, if we remove the flattened semantics and kept the old
     style for stating lemmas, then we also need to anticipate and
     state that some procedure will call some abstract module (not a
     functor parameter) some number of times. Issues:
     * this is heavy;
     * if we use many times the lemma, in ≠ contexts with ≠ abstract
       modules, then we need to anticipate *each* usage in the lemma statement.

3) use cost information in Hoare logics (still [WIP]):
   - remove wrappers with little overhead.