I haven't used Why3, but I have used other SMT solver-based frameworks such as Dafny and TLAPS for TLA+ and they all seem focused on proving function behavior,

I haven't used Why3, but I have used other SMT solver-based frameworks such as Dafny and TLAPS for TLA+ and they all seem focused on proving function behavior, rather than function runtime or memory usage. I suspect there's a way to encode runtime and memory usage theorems, but I don't have a clear conception of the best way of doing so without polluting function definitions.