functor (M : Memory.Model) ->   sig class wp : Model.t -> Generator.computer end