Code proved correct,
compiled to native speed.

package Counters {
    pub fn clamp(value, low, high: Integer) -> Integer
        requires low <= high
        ensures result in low..=high
    {
        if value < low {
            return low;
        } else if value > high {
            return high;
        }
        return value;
    }

    pub fn increment(count: inout Natural)
        requires count < Natural::Last
        ensures count == old(count) + 1
    {
        count += 1;
    }
}

from byron import Natural, ensures, requires, result


def clamp(value: int, low: int, high: int) -> int:
    requires(low <= high)
    ensures(low <= result <= high)
    if value < low:
        return low
    elif value > high:
        return high
    return value


def increment(count: Natural) -> Natural:
    requires(count < Natural.last)
    ensures(result == count + 1)
    return count + 1

package Counters is

   function Clamp (Value, Low, High : Integer) return Integer
     with Pre  => Low <= High,
          Post => Clamp'Result in Low .. High;

   procedure Increment (Count : in out Natural)
     with Pre  => Count < Natural'Last,
          Post => Count = Count'Old + 1;

end Counters;

package body Counters is

   function Clamp (Value, Low, High : Integer) return Integer is
   begin
      if Value < Low then
         return Low;
      elsif Value > High then
         return High;
      else
         return Value;
      end if;
   end Clamp;

   procedure Increment (Count : in out Natural) is
   begin
      Count := Count + 1;
   end Increment;

end Counters;