module String_lemmas

  use array.Array
  use map.Map
  use map.MapEq
  use map.Const
  use int.Int
  use int.Power
  use lemmas.Lemmas
  use mach.c.C
  use mach.c.UChar

  predicate in_base (b:int) (x:map int uchar) (n:int) (m:int) =
    forall i. n <= i < m -> 0 <= x[i] < b

  let lemma in_base_concat (b:int) (x:map int uchar) (n m l:int)
    requires { in_base b x n m }
    requires { in_base b x m l }
    ensures  { in_base b x n l }
  = ()

  let rec ghost function
      svalue_le_sub (b:int) (x:map int uchar) (n:int) (m:int) : int
    variant  { m - n }
  =
    if n < m
    then uchar'int x[n] + b * svalue_le_sub b x (n+1) m
    else 0

  predicate string_in_base (b:int) (p:ptr uchar) =
    in_base b (pelts p) (min p) (max p)

  let rec lemma svalue_le_sub_tail (b:int) (x:map int uchar) (n m:int)
    requires { n <= m }
    requires { in_base b x n (m+1) }
    requires { 2 <= b <= 256 }
    variant  { m - n }
    ensures  {
      svalue_le_sub b x n (m+1) =
        svalue_le_sub b x n m + (Map.get x m) * power b (m-n) }
  = [@vc:sp] if n < m then svalue_le_sub_tail b x (n+1) m else ()

  let rec lemma svalue_le_sub_concat (b:int) (x:map int uchar) (n m l:int)
    requires { n <= m <= l}
    requires { in_base b x n l }
    requires { 2 <= b <= 256 }
    variant  { m - n }
    ensures  {
      svalue_le_sub b x n l =
        svalue_le_sub b x n m + svalue_le_sub b x m l * power b (m-n) }
  =
  if n < m then
     begin
     assert {n<m};
     svalue_le_sub_concat b x (n+1) m l
     end
  else ()

  let lemma svalue_le_sub_head (b:int) (x:map int uchar) (n m:int)
    requires { n < m }
    requires { in_base b x n m }
    requires { 2 <= b <= 256 }
    ensures { svalue_le_sub b x n m = x[n] + b * svalue_le_sub b x (n+1) m }
  = ()

  let rec lemma svalue_le_sub_frame (b:int) (x y:map int uchar) (n m:int)
    requires { MapEq.map_eq_sub x y n m }
    variant  { m - n }
    ensures  { svalue_le_sub b x n m = svalue_le_sub b y n m }
  =
    if n < m then svalue_le_sub_frame b x y (n+1) m else ()

  use mach.int.Int32

  function svalue_le (b:int) (x:ptr uchar) (sz:int) : int
  =
    svalue_le_sub b (pelts x) x.offset (x.offset + sz)

   let lemma svalue_le_tail (b:int) (x:ptr uchar) (sz:int32)
    requires { 0 <= sz }
    requires { in_base b (pelts x) x.offset (x.offset + sz + 1)  }
    requires { 2 <= b <= 256 }
    ensures  { svalue_le b x (sz + 1)
               = svalue_le b x sz + (pelts x)[x.offset + sz] * power b sz }
  = svalue_le_sub_tail b (pelts x) x.offset (x.offset + p2i sz)

  meta remove_prop axiom svalue_le_tail

  let lemma svalue_le_concat (b:int) (x:ptr uchar) (n m:int32)
    requires { 0 <= n <= m }
    requires { in_base b (pelts x) x.offset (x.offset + p2i m)  }
    requires { 2 <= b <= 256 }
    ensures  { svalue_le b x m
               = svalue_le b x n
                 + power b n
                   * svalue_le_sub b (pelts x) (x.offset + n) (x.offset + m) }
  = svalue_le_sub_concat b (pelts x) x.offset
                         (x.offset + p2i n) (x.offset + p2i m)

Big-endian values for strings

  let rec ghost function
                svalue_sub (b:int) (x: map int uchar) (n:int) (m:int) : int
    variant { m - n }
  = if n < m
    then uchar'int x[m-1] + b * svalue_sub b x n (m-1)
    else 0

  let rec lemma svalue_sub_tail (b:int) (x:map int uchar) (n m:int)
    requires { n <= m }
    requires { in_base b x (n-1) m }
    requires { 2 <= b <= 256 }
    variant  { m - n }
    ensures  { svalue_sub b x (n-1) m =
                 svalue_sub b x n m + (Map.get x (n-1)) * power b (m - n) }
  = if n < m
    then begin
      svalue_sub_tail b x n (m-1);
    end else ()

  let rec lemma svalue_sub_concat (b:int) (x:map int uchar) (n m l:int)
    requires { n <= m <= l}
    requires { in_base b x n l }
    requires { 2 <= b <= 256 }
    variant  { l - m }
    ensures  { svalue_sub b x n l
               = svalue_sub b x m l + power b (l - m) * svalue_sub b x n m }
  =
    if m < l then svalue_sub_concat b x n m (l-1) else ()

  let lemma svalue_sub_head (b:int) (x:map int uchar) (n m:int)
    requires { n < m }
    requires { in_base b x n m }
    requires { 2 <= b <= 256 }
    ensures { svalue_sub b x n m = x[m-1] + b * svalue_sub b x n (m-1) }
  = ()

  let rec lemma svalue_sub_frame (b:int) (x y:map int uchar) (n m:int)
    requires { MapEq.map_eq_sub x y n m }
    variant  { m - n }
    ensures  { svalue_sub b x n m = svalue_sub b y n m }
  =
    if n < m then svalue_sub_frame b x y n (m-1) else ()

  function svalue (b:int) (x:ptr uchar) (sz:int) : int
  = svalue_sub b (pelts x) x.offset (x.offset + sz)

  let rec lemma svalue_le_sub_lower_bound (b:int) (x:map int uchar) (n m:int)
    variant { m - n }
    requires { 2 <= b <= 256 }
    ensures { 0 <= svalue_le_sub b x n m }
  = if m <= n then ()
    else svalue_le_sub_lower_bound b x (n+1) m

  let rec lemma svalue_sub_lower_bound (b:int) (x:map int uchar) (n m:int)
    variant { m - n }
    requires { 2 <= b <= 256 }
    ensures { 0 <= svalue_sub b x n m }
  = if m <= n then ()
    else svalue_sub_lower_bound b x n (m-1)

  let rec lemma svalue_le_sub_upper_bound (b:int) (x:map int uchar) (n m:int)
    variant { m - n }
    requires { 2 <= b <= 256 }
    requires { n <= m }
    requires { in_base b x n m }
    ensures  { svalue_le_sub b x n m < power b (m - n) }
    = if n = m then ()
      else begin
        svalue_le_sub_tail b x n (m-1);
        svalue_le_sub_upper_bound b x n (m-1);
        assert { svalue_le_sub b x n m
                 <= svalue_le_sub b x n (m-1) + power b (m - n - 1) * (b-1) };
      end

  let rec lemma svalue_sub_upper_bound (b:int) (x:map int uchar) (n m:int)
    variant { m - n }
    requires { 2 <= b <= 256 }
    requires { n <= m }
    requires { in_base b x n m }
    ensures  { svalue_sub b x n m < power b (m - n) }
    = if n = m then ()
      else begin
        svalue_sub_tail b x (n+1) m;
        svalue_sub_upper_bound b x (n+1) m;
        assert { svalue_sub b x n m
                 <= svalue_sub b x (n+1) m + power b (m - n - 1) * (b-1) };
      end
end

module Conversions [@W:non_conservative_extension:N]

  use array.Array
  use map.Map
  use map.MapEq
  use map.Const
  use int.Int
  use int.Power
  use lemmas.Lemmas
  use string.String
  use mach.c.String
  use string.Char
  use mach.int.Int32
  use mach.c.UChar

  constant numlowstring : string = "0123456789abcdefghijklmnopqrstuvwxyz"

  function num_to_lowercase_text (d:uchar) : char
  = if 0 <= d < 36
    then get numlowstring d
    else chr (-1)

  predicate to_lowercase_text (d:map int uchar) (t:map int char) (m n:int)
  = forall i. n <= i < m -> Map.get t i = num_to_lowercase_text (Map.get d i)

  constant numupstring : string = "0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZ"

  function num_to_uppercase_text (d:uchar) : char
  = if 0 <= d < 36
    then get numupstring d
    else chr (-1)

  predicate to_uppercase_text (d:map int uchar) (t:map int char) (m n:int)
  = forall i. n <= i < m -> Map.get t i = num_to_uppercase_text (Map.get d i)

  constant numuplowstring : string
           = "0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz"

  function num_to_bothcase_text (d:uchar): char
  = if 0 <= d < 62
    then get numuplowstring d
    else chr (-1)

  predicate to_bothcase_text (d:map int uchar) (t:map int char) (m n:int)
  = forall i. n <= i < m -> Map.get t i = num_to_bothcase_text (Map.get d i)

  lemma lowconcat: numlowstring = concat digitstring lowstring
  lemma upconcat: numupstring = concat digitstring upstring
  lemma digitsublow: digitstring = substring numlowstring 0 10
  lemma digitsubup: digitstring = substring numupstring 0 10
  lemma lowsub: lowstring = substring numlowstring 10 26
  lemma upsub: upstring = substring numupstring 10 26
  lemma lowupconcat: numuplowstring = concat numupstring lowstring
  lemma digitsublowup: digitstring = substring numuplowstring 0 10
  lemma upsublowup: upstring = substring numuplowstring 10 26
  lemma lowsublowup: lowstring = substring numuplowstring 36 26

  function text_to_num_onecase (c:char) : int
  = if (get "0" 0) <= c <= (get "9" 0)
    then c - (get "0" 0)
    else if (get "a" 0) <= c <= (get "z" 0)
    then c - (get "a" 0) + 10
    else if (get "A" 0) <= c <= (get "Z" 0)
    then c - (get "A" 0) + 10
    else -1

  function text_to_num_bothcase (c:char) : int
  = if (get "0" 0) <= c <= (get "9" 0)
    then c - (get "0" 0)
    else if (get "a" 0) <= c <= (get "z" 0)
    then c - (get "a" 0) + 36
    else if (get "A" 0) <= c <= (get "Z" 0)
    then c - (get "A" 0) + 10
    else -1

  function text_to_num (base:int) (c:char) : int
  = if - 36 <= base <= 36
    then text_to_num_onecase c
    else text_to_num_bothcase c

  function num_to_text (base:int) (d:uchar) : char
  = if 0 <= base <= 36
    then num_to_lowercase_text d
    else if 36 < base <= 62
    then num_to_bothcase_text d
    else if -36 <= base
    then num_to_uppercase_text d
    else chr (-1)

  predicate to_num (base:int) (t: map int char) (d: map int uchar) (n m:int)
    = forall i. n <= i < m -> Map.get d i = text_to_num base (Map.get t i)

  let lemma digits ()
    ensures { code (get "9" 0) = code (get "0" 0) + 9 }
  =
    assert { "9" = substring digitstring 9 1 };
    assert { get "9" 0 = get digitstring 9 }

  let lemma lower ()
    ensures { code (get "z" 0) = code (get "a" 0) + 25 }
  =
    assert { "z" = substring lowstring 25 1 };
    assert { get "z" 0 = get lowstring 25 }

  let lemma upper ()
    ensures { code (get "Z" 0) = code (get "A" 0) + 25 }
  =
    assert { "Z" = substring upstring 25 1 };
    assert { get "Z" 0 = get upstring (25+0) = get upstring 25 }

  lemma diglow: code (get "9" 0) < code (get "a" 0)
  lemma digup: code (get "9" 0) < code (get "A" 0)
  lemma lowup: code (get "Z" 0) < code (get "a" 0)

  let lemma tnt_low (d:uchar)
    requires { 0 <= d < 36 }
    ensures { text_to_num_onecase (num_to_lowercase_text d) = d }
  =
    let t = num_to_lowercase_text d in
    if 0 <= d < 10
    then assert { t = get digitstring d }
    else begin
      assert { get lowstring (d - 10) = t
               by get lowstring (d-10)
                  = get (substring numlowstring 10 26) (d - 10)
                  = get numlowstring d };
      assert { text_to_num_onecase t = d
               by code t = code (get lowstring (d-10))
                    = code (get "a" 0) + (d-10)
                    <= code (get "z" 0)
               so code t > code (get "9" 0)
               so text_to_num_onecase t = code t - code (get "a" 0) + 10 = d }
    end

  let lemma tnt_up (d:uchar)
    requires { 0 <= d < 36 }
    ensures { text_to_num_onecase (num_to_uppercase_text d) = d }
  =
    let t = num_to_uppercase_text d in
    if 0 <= d < 10
    then assert { t = get digitstring d }
    else begin
      assert { get upstring (d - 10) = t
               by get upstring (d-10)
                  = get (substring numupstring 10 26) (d - 10)
                  = get numupstring d };
      assert { text_to_num_onecase t = d
               by code t = code (get upstring (d-10))
                    = code (get "A" 0) + (d-10)
                    <= code (get "Z" 0)
               so code t > code (get "9" 0)
               so code t < code (get "a" 0)
               so text_to_num_onecase t = code t - code (get "A" 0) + 10 = d }
    end

  let lemma tnt_both (d:uchar)
    requires { 0 <= d < 62 }
    ensures { text_to_num_bothcase (num_to_bothcase_text d) = d }
  =
    let t = num_to_bothcase_text d in
    if 0 <= d < 10
    then assert { t = get digitstring d }
    else begin
      if 10 <= d < 36
      then begin
        assert { get upstring (d-10) = t
                 by get upstring (d-10)
                  = get (substring numuplowstring 10 26) (d - 10)
                  = get numuplowstring d };
        assert { text_to_num_bothcase t = d
                 by code t = code (get upstring (d-10))
                     = code (get "A" 0) + (d-10)
                     <= code (get "Z" 0)
                 so code t > code (get "9" 0)
                 so code t < code (get "a" 0)
                 so text_to_num_bothcase t
                    = code t - code (get "A" 0) + 10 = d }
      end
      else begin
        assert { get lowstring (d - 36) = t
                 by get lowstring (d-36)
                    = get (substring numuplowstring 36 26) (d - 36)
                    = get numuplowstring d };
        assert { text_to_num_bothcase t = d
                 by code t = code (get lowstring (d-36))
                      = code (get "a" 0) + (d-36)
                      <= code (get "z" 0)
                 so code t > code (get "9" 0)
                 so text_to_num_bothcase t
                    = code t - code (get "a" 0) + 10 = d }
      end
    end

  use int.Abs

  let lemma tnt (base:int) (d:uchar)
    requires { -36 <= base <= 62 }
    requires { 0 <= d < abs base }
    ensures  { text_to_num base (num_to_text base d) = d }
  = if 0 <= base <= 36 then tnt_low d
    else if 36 < base <= 62
    then begin
      tnt_both d
    end else tnt_up d

end
module String_value

  use mach.c.C
  use mach.c.String
  use string.Char
  use map.Map
  use int.Int
  use String_lemmas
  use Conversions
  use mach.c.UChar

  let rec ghost function
                abs_value_sub_text (b:int) (s:map int char) (n m: int) : int
    variant { m - n }
  = if n < m
    then text_to_num b s[m-1] + b * abs_value_sub_text b s n (m-1)
    else 0

  let rec lemma text_conversion (b:int) (t: map int char)
                                (d: map int uchar) (n m:int)
    requires { to_num b t d n m }
    variant  { m - n }
    ensures  { abs_value_sub_text b t n m = svalue_sub b d n m }
  =
    if n < m then text_conversion b t d n (m-1)

  function abs_value_text (b:int) (s:map int char) (ofs:int) : int
    = abs_value_sub_text b s ofs (ofs + strlen s ofs)

  function value_text (b:int) (s:map int char) (ofs:int) : int
    = if Char.(=) s[ofs] minus_char
      then - abs_value_text b s (ofs + 1)
      else abs_value_text b s ofs

  predicate text_in_base (b:int) (t: map int char) (n m:int)
    = forall i. n <= i < m -> 0 <= text_to_num b t[i] < b

  predicate string_in_base (b:int) (s:map int char) (ofs: int)
    = (text_in_base b s ofs (ofs + strlen s ofs) /\ strlen s ofs > 0)
      \/ (s[ofs] = minus_char
         /\ text_in_base b s (ofs + 1) (ofs + strlen s ofs)
         /\ strlen s ofs > 1)

  let rec lemma abs_value_sub_text_frame (b:int) (x y: map int char) (n m: int)
    requires { forall i. n <= i < m -> x[i] = y[i] }
    ensures  { abs_value_sub_text b x n m = abs_value_sub_text b y n m }
    variant  { m - n }
  = if n < m then abs_value_sub_text_frame b x y n (m-1) else ()

end