You would want to specify a version of GHC and optimization flags, then it would just involve code analysis of your output. Likely this work would be necessary

You would want to specify a version of GHC and optimization flags, then it would just involve code analysis of your output. Likely this work would be necessary to "prove" (not in the strict form) your assumptions about constant-time anyway.