docs: def ensures(condition):
      """A function decorator to specify exit conditions for the function.
  
      Exit conditions should be a string, which will be evaluated as
      Python code.  Arguments of the function may be accessed by their
      name.  The return value of the function may be accessed using the
      special variable name "return".
  
      The special syntax "-->" and "<-->" may be used to mean "if" and
      "if and only if", respectively.  They may not be contained within
      sub-expressions.
  
      Values may be compared to previous executions of the function by
      including a "`" or "``" after them to check for higher order
      properties of the function.
  
      Note that globals will not be included by default, and must be
      manually included using the "namespace" setting, set via
      settings.Settings.
  
      Example usage:
  
        | @ensures("lower_bound <= return <= upper_bound")
        | def search(lower_bound, upper_bound):
        |     ...
  
        | @ensures("x <= x` --> return <= return`")
        | def monotonic(x):
        |     ...
      """
      def _decorator(func, condition=condition):
      # @ensures decorator
          if U.has_fun_prop(func, "ensures"):
              if not isinstance(U.get_fun_prop(func, "ensures"), list):
                  raise E.InternalError("Invalid ensures strucutre")
              ensures_statements = U.get_fun_prop(func, "ensures")
          else:
              ensures_statements = []
          e = condition.replace("return", "__RETURN__")
          if "<-->" in e:
              e_parts = e.split("<-->")
              assert len(e_parts) == 2, "Only one implies per statement in %s condition %s" % (ensurement, func.__qualname__)
              e = "((%s) if (%s) else True) and ((%s) if (%s) else True)" % (e_parts[1], e_parts[0], e_parts[0], e_parts[1])
              assert "-->" not in e, "Only one implies per statement in %s condition %s"  % (ensurement, func.__qualname__)
          if "-->" in e:
              e_parts = e.split("-->")
              assert len(e_parts) == 2, "Only one implies per statement in %s condition %s" % (ensurement, func.__qualname__)
              e = "(%s) if (%s) else True" % (e_parts[1], e_parts[0])
          _bt = "__BACKTICK__"
          _dbt = "__DOUBLEBACKTICK__"
          if "``" in e:
              e = e.replace("``", _dbt)
              e = e.replace("`", _bt)
              compiled = compile(e, '', 'eval')
              U.set_fun_prop(func, "ensures", [(2, compiled, condition)]+ensures_statements)
          elif "`" in e:
              e = e.replace("`", _bt)
              compiled = compile(e, '', 'eval')
              U.set_fun_prop(func, "ensures", [(1, compiled, condition)]+ensures_statements)
          else:
              compiled = compile(e, '', 'eval')
              U.set_fun_prop(func, "ensures", [(0, compiled, condition)]+ensures_statements)
          return _wrap(func)
      return _decorator