Wiki Agenda Contact Version française

Base64

Base64 encoding and decoding of strings.


Authors: Cláudio; Lourenço

Topics: Strings

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


Base64 encoding

Implementation of the Base64 encoding algorithm.

An encode function translates an arbitrary string intro a string containing only the following 64 characters.

  Index  Binary  Char    |    Index  Binary  Char
  0      000000  'A'     |    32     100000  'g'
  1      000001  'B'     |    33     100001  'h'
  2      000010  'C'     |    34     100010  'i'
  3      000011  'D'     |    35     100011  'j'
  4      000100  'E'     |    36     100100  'k'
  5      000101  'F'     |    37     100101  'l'
  6      000110  'G'     |    38     100110  'm'
  7      000111  'H'     |    39     100111  'n'
  8      001000  'I'     |    40     101000  'o'
  9      001001  'J'     |    41     101001  'p'
  10     001010  'K'     |    42     101010  'q'
  11     001011  'L'     |    43     101011  'r'
  12     001100  'M'     |    44     101100  's'
  13     001101  'N'     |    45     101101  't'
  14     001110  'O'     |    46     101110  'u'
  15     001111  'P'     |    47     101111  'v'
  16     010000  'Q'     |    48     110000  'w'
  17     010001  'R'     |    49     110001  'x'
  18     010010  'S'     |    50     110010  'y'
  19     010011  'T'     |    51     110011  'z'
  20     010100  'U'     |    52     110100  '0'
  21     010101  'V'     |    53     110101  '1'
  22     010110  'W'     |    54     110110  '2'
  23     010111  'X'     |    55     110111  '3'
  24     011000  'Y'     |    56     111000  '4'
  25     011001  'Z'     |    57     111001  '5'
  26     011010  'a'     |    58     111010  '6'
  27     011011  'b'     |    59     111011  '7'
  28     011100  'c'     |    60     111100  '8'
  29     011101  'd'     |    61     111101  '9'
  30     011110  'e'     |    62     111110  '+'
  31     011111  'f'     |    63     111111  '/'
  

Four characters are required to encode each sequence of 3 characters of the input string. The length of the encoded string is always a multiple of four (if needed the padding character '=' is used).

A decode function does the inverse operation. It takes a previously encoded string and returns the original string.

The main property of the algorithm is that, for every string s, decode (encode s) = s.

module Base64
  use mach.int.Int
  use mach.int.Int63
  use string.String
  use string.Char
  use string.OCaml
  use string.StringBuffer

  function int2b64 (i: int) : char =
    if 0 <= i <= 25 then chr (i + 65) else
    if 26 <= i <= 51 then chr (i - 26 + 97) else
    if 52 <= i <= 61 then chr (i - 52 + 48) else
    if i = 62 then chr 43 else if i = 63 then chr 47
    else chr 0

int2b64 i calculates the character corresponding to index i (see table above)

  let int2b64 (i: int63) : char
    requires { 0 <= i < 64 }
    ensures  { result = int2b64 i }
  =
    if 0 <= i <= 25 then chr (i + 65) else
    if 26 <= i <= 51 then chr (i - 26 + 97) else
    if 52 <= i <= 61 then chr (i - 52 + 48) else
    if i = 62 then chr 43 else if i = 63 then chr 47
    else absurd

  let function eq_symbol : char = chr 61

character '='

  predicate valid_b64_char (c: char) =
    65 <= code c <= 90 || 97 <= code c <= 122 || 48 <= code c <= 57 ||
    code c = 43 || code c = 47

valid_b64_char c is true, if and only if, c is in the table above

  lemma int2b64_valid_4_char: forall i. 0 <= i < 64 -> valid_b64_char (int2b64 i)

  function b642int (c: char) : int =
    if 65 <= code c <= 90  then code c - 65      else (* 0  - 25 *)
    if 97 <= code c <= 122 then code c - 97 + 26 else (* 26 - 51 *)
    if 48 <= code c <= 57  then code c - 48 + 52 else (* 52 - 61 *)
    if code c = 43         then 62               else (* 62 *)
    if code c = 47         then 63               else (* 63 *)
    if c = eq_symbol       then 0                else (* 0 *)
    64                                                (* 64 *)

inverse of function int2b64

  let b642int (c: char) : int63
    requires { valid_b64_char c || c = eq_symbol }
    ensures  { result = b642int c }
  = if 65 <= code c <= 90  then code c - 65      else
    if 97 <= code c <= 122 then code c - 97 + 26 else
    if 48 <= code c <= 57  then code c - 48 + 52 else
    if code c = 43         then 62               else
    if code c = 47         then 63               else
    if eq_char c eq_symbol then 0                else
    absurd

  lemma b642int_int2b64: forall i. 0 <= i < 64 -> b642int (int2b64 i) = i

  function get_pad (s: string): int =
    if length s >= 1 && s[length s - 1] = eq_symbol then
        (if length s >= 2 && s[length s - 2] = eq_symbol then 2 else 1)
    else 0

get_pad s calculates the number of padding characters in the string s (between 0 and 2)

  let get_pad (s: string): int63
    ensures { result = get_pad s }
  = if length s >= 1 && eq_char s[length s - 1] eq_symbol then
        (if length s >= 2 && eq_char s[length s - 2] eq_symbol then 2 else 1)
    else 0

  function calc_pad (s: string): int =
    if mod (length s) 3 = 1 then 2 else
      if mod (length s) 3 = 2 then 1 else 0

calc_pad s returns the number of padding characters that will appear in the string that results from encoding s

  lemma calc_pad_mod3: forall s. mod (length s + calc_pad s) 3 = 0

  let calc_pad (s: string): int63
    ensures { result = calc_pad s }
  = if length s % 3 = 1 then 2 else
      if length s % 3 = 2 then 1 else 0

  predicate encoding (s1 s2: string) =
    length s2 = div (length s1 + calc_pad s1) 3 * 4 &&
    ( forall i. 0 <= i < div (length s2) 4 ->
      let b1,b2,b3,b4 = s2[4*i], s2[4*i+1],s2[4*i+2], s2[4*i+3] in
      s1[i*3] = chr (b642int b1 * 4 + div (b642int b2) 16) &&
      (i * 3 + 1 < length s1 ->
        s1[i*3+1] = chr (mod (b642int b2) 16 * 16 + div (b642int b3) 4)) &&
      (i * 3 + 2 < length s1 ->
        s1[i*3+2] = chr (mod (b642int b3) 4 * 64 + b642int b4))) &&
    ( forall i. 0 <= i < length s2 - get_pad s2 -> valid_b64_char s2[i] ) &&
    ( get_pad s2 = 1 -> mod (b642int s2[length s2 - 2]) 4  = 0 /\
                       s2[length s2 - 1] = eq_symbol ) &&
    ( get_pad s2 = 2 -> mod (b642int s2[length s2 - 3]) 16 = 0 /\
                       s2[length s2 - 2] = s2[length s2 - 1] = eq_symbol ) &&
    calc_pad s1 = get_pad s2

encoding s1 s2 is true, if and only if, s2 is a valid encoding of s1

  predicate valid_b64 (s: string) =
    (mod (length s) 4 = 0) &&
    (forall i. 0 <= i < length s - get_pad s -> valid_b64_char s[i]) &&
    (get_pad s = 1 -> mod (b642int s[length s - 2]) 4  = 0 &&
                      s[length s - 1] = eq_symbol) &&
    (get_pad s = 2 -> mod (b642int s[length s - 3]) 16 = 0 &&
                      s[length s - 2] = eq_symbol &&
                      s[length s - 1] = eq_symbol)

valid_b64 s is true, if and only if, s is a valid Base64 string: the length of s is a multiple of 4, and all its characters (with exception to the last element or the two last elements) belong to the table above. If the last characters of the string are not valid then either the string terminates with "=" or "==".

  let lemma encoding_valid_b64 (s1 s2: string)
    requires { encoding s1 s2 }
    ensures  { valid_b64 s2 }
  =
    assert { length s1 = div (length s2) 4 * 3 - get_pad s2 };
    assert { forall i. 0 <= i < div (length s1) 3 ->
      (valid_b64_char s2[i*4] && valid_b64_char s2[i*4+1] &&
      valid_b64_char s2[i*4+2] && valid_b64_char s2[i*4+3])
    };
    assert { mod (length s1) 3 <> 0 ->
      let last = div (length s1) 3 in
      valid_b64_char s2[last*4] && valid_b64_char s2[last*4+1] &&
      if last * 3 + 1 = length s1 then
        s2[last*4+2] = eq_symbol && s2[last*4+3] = eq_symbol
      else valid_b64_char s2[last*4+2] && s2[last*4+3] = eq_symbol
    };
    assert { forall i.
      (0 <= i < length s2 - get_pad s2 -> valid_b64_char s2[i]) &&
      (length s2 - get_pad s2 <= i < length s2 -> s2[i] = eq_symbol) }

  let lemma decode_unique (s1 s2 s3: string)
    requires { encoding s1 s2 /\ encoding s3 s2 }
    ensures  { s1 = s3 }
  = assert { forall i. 0 <= i < div (length s1 + calc_pad s1) 3 ->
      s1[i*3] = s3[i*3] &&
      (i * 3 + 1 < length s1 -> s1[i*3+1] = s3[i*3+1]) &&
      (i * 3 + 2 < length s1 -> s1[i*3+2] = s3[i*3+2]) };
    assert { forall i. 0 <= i < length s1 -> s1[i] = s3[i] }

the decode of a string is unique

  let lemma encode_unique (s1 s2 s3: string)
    requires { encoding s1 s2 /\ encoding s1 s3 }
    ensures  { s2 = s3 }
  = assert { length s2 = length s3 };
    assert { forall i. 0 <= i < div (length s2) 4 ->
        let a1, a2, a3 = s1[i*3], s1[i*3+1], s1[i*3+2] in
        s2[i*4] = int2b64 (div (code a1)  4) &&
        if i * 3 + 1 < length s1 then
        ( s2[i*4+1] = int2b64 (mod (code a1) 4 * 16 + div (code a2) 16) &&
          ( if i * 3 + 2 < length s1 then
              s2[i*4+2] = int2b64 (mod (code a2) 16 * 4 + div (code a3) 64) &&
              s2[i*4+3] = int2b64 (mod (code a3) 64)
            else (s2[i*4+2] = int2b64 (mod (code a2) 16 * 4) && s2[i*4+3] = eq_symbol)
          )
        )      else
        (    s2[i*4+1] = int2b64 (mod (code a1) 4 * 16)
          && s2[i*4+2] = eq_symbol
          && s2[i*4+3] = eq_symbol)
    };
    assert { forall i. 0 <= i < div (length s3) 4 ->
        let a1, a2, a3 = s1[i*3], s1[i*3+1], s1[i*3+2] in
        s3[i*4] = int2b64 (div (code a1)  4) &&
        if i * 3 + 1 < length s1 then
        ( s3[i*4+1] = int2b64 (mod (code a1) 4 * 16 + div (code a2) 16) &&
          ( if i * 3 + 2 < length s1 then
              s3[i*4+2] = int2b64 (mod (code a2) 16 * 4 + div (code a3) 64) &&
              s3[i*4+3] = int2b64 (mod (code a3) 64)
            else (s3[i*4+2] = int2b64 (mod (code a2) 16 * 4) && s3[i*4+3] = eq_symbol)
          )
        )      else
        (    s3[i*4+1] = int2b64 (mod (code a1) 4 * 16)
          && s3[i*4+2] = eq_symbol
          && s3[i*4+3] = eq_symbol)
    };
    assert { forall i. 0 <= i < div (length s2) 4 ->
                s2[i*4]   = s3[i*4]   /\ s2[i*4+1] = s3[i*4+1]
             /\ s2[i*4+2] = s3[i*4+2] /\ s2[i*4+3] = s3[i*4+3]
    };
    assert { forall i. 0 <= i < length s2 -> s2[i] = s3[i]};
    assert { eq_string s2 s3}

the encode of a string is unique

  let encode (s: string) : string
    ensures { encoding s result }
  = let padding = calc_pad s in
    let sp = concat s (make padding (chr 0)) in
    let ref i = 0 in
    let r = StringBuffer.create 42 in
    let ghost ref b = 0 : int in
    while i < length sp do
      variant {length sp - i}
      invariant { i = b * 3 }
      invariant { length r = b * 4 }
      invariant { 0 <= i <= length sp }
      invariant { forall j. 0 <= j < b ->
        let a1, a2, a3 = sp[j*3], sp[j*3+1], sp[j*3+2] in
        r[j*4]   = int2b64 (div (code a1)  4) &&
        r[j*4+1] = int2b64 (mod (code a1) 4 * 16 + div (code a2) 16) &&
        r[j*4+2] = int2b64 (mod (code a2) 16 * 4 + div (code a3) 64) &&
        r[j*4+3] = int2b64 (mod (code a3) 64)
      }
      let c1,c2,c3 = sp[i], sp[i+1], sp[i+2] in
      let b1 = code c1 / 4 in
      let b2 = (code c1 % 4) * 16 + code c2 / 16 in
      let b3 = (code c2 % 16) * 4 + code c3 / 64 in
      let b4 = code c3 % 64 in
      label L in
      StringBuffer.add_char r (int2b64 b1);
      StringBuffer.add_char r (int2b64 b2);
      StringBuffer.add_char r (int2b64 b3);
      StringBuffer.add_char r (int2b64 b4);
      i <- i + 3;
      ghost (b <- b + 1);
      assert { r[length r - 4] = int2b64 (div (code c1) 4)  &&
               r[length r - 3] = int2b64 (mod (code c1) 4 * 16 + div (code c2) 16) &&
               r[length r - 2] = int2b64 (mod (code c2) 16 * 4 + div (code c3) 64) &&
               r[length r - 1] = int2b64 (mod (code c3) 64) };
      assert { forall j. 0 <= j < length r - 4 -> r[j] = (r at L)[j] };
    done;
    assert { padding = 1 -> mod (b642int r[length r - 2]) 4  = 0 };
    assert { padding = 2 -> mod (b642int r[length r - 3]) 16 = 0 };
    StringBuffer.truncate r (length r - padding);
    StringBuffer.add_string r (make padding eq_symbol);
    StringBuffer.contents r

  let decode (s: string) : string
    requires { valid_b64 s }
    ensures  { encoding result s }
  = let ref i = 0 in
    let r = StringBuffer.create 42 in
    let ghost ref b = 0:int in
    while i < length s do
      variant { length s - i }
      invariant { 0 <= i <= length s }
      invariant { i = b * 4 }
      invariant { length r = b * 3 }
      invariant { forall j. 0 <= j < b ->
        let b1,b2,b3,b4 = s[4*j], s[4*j+1], s[4*j+2], s[4*j+3] in
        r[j*3]   = chr (b642int b1 * 4 + div (b642int b2) 16) &&
        r[j*3+1] = chr (mod (b642int b2) 16 * 16 + div (b642int b3) 4) &&
        r[j*3+2] = chr (mod (b642int b3) 4 * 64 + b642int b4)
      }
      label L in
      let b1,b2,b3,b4 = s[i], s[i+1], s[i+2], s[i+3] in
      let a1 = b642int b1 * 4 + b642int b2 / 16 in
      let a2 = b642int b2 % 16 * 16 + b642int b3 / 4 in
      let a3 = b642int b3 % 4 * 64 + b642int b4 in
      StringBuffer.add_char r (chr a1);
      StringBuffer.add_char r (chr a2);
      StringBuffer.add_char r (chr a3);
      i <- i + 4;
      ghost (b <- b + 1);
      assert { r[length r - 3] = chr (b642int b1 * 4 + div (b642int b2) 16) &&
               r[length r - 2] = chr (mod (b642int b2) 16 * 16 + div (b642int b3) 4) &&
               r[length r - 1] = chr (mod (b642int b3) 4 * 64 + b642int b4) };
      assert { forall j. 0 <= j < length r - 3 -> r[j] =  (r at L)[j]}
    done;
    StringBuffer.sub r 0 (length r - get_pad s)

  let decode_encode (s: string) : unit
  = let s1 = encode s in
    let s2 = decode s1 in
    assert { s = s2 }

end

download ZIP archive

Why3 Proof Results for Project "string_base64_encoding"

Theory "string_base64_encoding.Base64": fully verified

ObligationsAlt-Ergo 2.3.0Alt-Ergo 2.4.0CVC4 1.7Z3 4.8.10Z3 4.8.6
VC for int2b640.05------------
VC for eq_symbol0.01------------
int2b64_valid_4_char0.02------------
VC for b642int0.29------------
b642int_int2b640.05------------
VC for get_pad0.35------------
calc_pad_mod3---------------
introduce_premises
calc_pad_mod3.0---------------
case (mod (length s) 3 = 0)
true case0.02------------
false case---------------
case (mod (length s) 3 = 1)
false case (true case)0.02------------
false case---------------
assert (mod (length s) 3 = 2)
asserted formula------------0.02
false case0.03------------
VC for calc_pad0.81------------
VC for encoding_valid_b642.90------------
VC for decode_unique---------------
split_vc
assertion---------------
split_vc
assertion------------0.04
remove real,bool,tuple0,unit,buffer,zero,one,(>),empty,concat,lt,le,s_at,substring,prefixof,suffixof,contains,indexof,replace,replaceall,to_int,is_digit,from_int,code,get,eq_string,make,int63'maxInt,int63'minInt,min_int63,max_int63,to_int1,in_bounds,max_int,min_int,str,int2b64,valid_b64,Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,concat_assoc,concat_empty,length_empty,length_concat,lt_empty,lt_not_com,lt_ref,lt_trans,le_empty,le_ref,lt_le,lt_le_eq,le_trans,at_out_of_range,at_empty,at_length,concat_at,substring_out_of_range,substring_of_length_zero_or_less,substring_of_empty,substring_smaller,substring_smaller_x,substring_length,substring_at,substring_substring,concat_substring,prefixof_substring,prefixof_concat,prefixof_empty,prefixof_empty2,suffixof_substring,suffixof_concat,suffixof_empty,suffixof_empty2,contains_prefixof,contains_suffixof,contains_empty,contains_empty2,contains_substring,contains_concat,contains_at,indexof_empty,indexof_empty1,indexof_contains,contains_indexof,not_contains_indexof,substring_indexof,indexof_out_of_range,indexof_in_range,indexof_contains_substring,replace_empty,replace_not_contains,replace_empty2,replace_substring_indexof,replaceall_empty1,not_contains_replaceall,to_int_gt_minus_1,to_int_empty,from_int_negative,from_int_to_int,char'invariant,code,code_chr,chr_code,get,substring_get,concat_first,concat_second,extensionality,make_length,make_contents,to_int_in_bounds,extensionality1,max_int'def,min_int'def,int2b64_valid_4_char,b642int_int2b64,calc_pad_mod3,encoding_valid_b64
assertion---------0.020.03
assertion------------0.04
remove real,bool,tuple0,unit,buffer,zero,one,(>),abs,empty,concat,lt,le,s_at,substring,prefixof,suffixof,contains,indexof,replace,replaceall,to_int,is_digit,from_int,code,get,eq_string,make,int63'maxInt,int63'minInt,min_int63,max_int63,to_int1,in_bounds,max_int,min_int,str,int2b64,Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,concat_assoc,concat_empty,length_empty,length_concat,lt_empty,lt_not_com,lt_ref,lt_trans,le_empty,le_ref,lt_le,lt_le_eq,le_trans,at_out_of_range,at_empty,at_length,concat_at,substring_out_of_range,substring_of_length_zero_or_less,substring_of_empty,substring_smaller,substring_smaller_x,substring_length,substring_at,substring_substring,concat_substring,prefixof_substring,prefixof_concat,prefixof_empty,prefixof_empty2,suffixof_substring,suffixof_concat,suffixof_empty,suffixof_empty2,contains_prefixof,contains_suffixof,contains_empty,contains_empty2,contains_substring,contains_concat,contains_at,indexof_empty,indexof_empty1,indexof_contains,contains_indexof,not_contains_indexof,substring_indexof,indexof_out_of_range,indexof_in_range,indexof_contains_substring,replace_empty,replace_not_contains,replace_empty2,replace_substring_indexof,replaceall_empty1,not_contains_replaceall,to_int_gt_minus_1,to_int_empty,from_int_negative,from_int_to_int,char'invariant,code,code_chr,chr_code,get,substring_get,concat_first,concat_second,extensionality,make_length,make_contents,to_int_in_bounds,extensionality1,max_int'def,min_int'def,int2b64_valid_4_char,b642int_int2b64,H1,H2
assertion---------0.020.02
assertion------------0.06
remove real,bool,tuple0,unit,buffer,zero,one,(>),empty,concat,lt,le,s_at,substring,prefixof,suffixof,contains,indexof,replace,replaceall,to_int,is_digit,from_int,code,get,eq_string,make,int63'maxInt,int63'minInt,min_int63,max_int63,to_int1,in_bounds,max_int,min_int,str,int2b64,valid_b64,Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,concat_assoc,concat_empty,length_empty,length_concat,lt_empty,lt_not_com,lt_ref,lt_trans,le_empty,le_ref,lt_le,lt_le_eq,le_trans,at_out_of_range,at_empty,at_length,concat_at,substring_out_of_range,substring_of_length_zero_or_less,substring_of_empty,substring_smaller,substring_smaller_x,substring_length,substring_at,substring_substring,concat_substring,prefixof_substring,prefixof_concat,prefixof_empty,prefixof_empty2,suffixof_substring,suffixof_concat,suffixof_empty,suffixof_empty2,contains_prefixof,contains_suffixof,contains_empty,contains_empty2,contains_substring,contains_concat,contains_at,indexof_empty,indexof_empty1,indexof_contains,contains_indexof,not_contains_indexof,substring_indexof,indexof_out_of_range,indexof_in_range,indexof_contains_substring,replace_empty,replace_not_contains,replace_empty2,replace_substring_indexof,replaceall_empty1,not_contains_replaceall,to_int_gt_minus_1,to_int_empty,from_int_negative,from_int_to_int,char'invariant,code,code_chr,chr_code,get,substring_get,concat_first,concat_second,extensionality,make_length,make_contents,to_int_in_bounds,extensionality1,max_int'def,min_int'def,int2b64_valid_4_char,b642int_int2b64,encoding_valid_b64,H1,H2,H3
assertion---------0.020.03
assertion---------------
instantiate Assert (div i 3)
assertion0.08------------
postcondition---------------
apply extensionality
apply premises0.11------------
VC for encode_unique---------------
split_vc
assertion0.01------------
assertion---------------
split_vc
assertion---------------
unfold encoding in H3
assertion---------------
split_premise_full
assertion---------------
instantiate H12 i
assertion2.41------------
assertion---------------
unfold encoding in H5
assertion---------------
split_premise_full
assertion---------------
instantiate H14 i
assertion---------------
instantiate H13 i
assertion9.79------------
assertion---------------
unfold encoding in H7
assertion---------------
split_premise_full
assertion---------------
instantiate H14 i
assertion---------------
instantiate H15 i
assertion16.44------------
assertion---------------
unfold encoding in H8
assertion---------------
split_premise_full
assertion---------------
instantiate H15 i
assertion4.91------------
assertion---------------
unfold encoding in H7
assertion---------------
split_premise_full
assertion---------------
instantiate H14 i
assertion---------------
instantiate H15 i
assertion5.57------------
assertion0.28------------
assertion---------------
unfold encoding in H5
assertion---------------
split_premise_full
assertion---------------
instantiate H13 i
assertion---------------
instantiate H14 i
assertion---------------
destruct Hinst
destruct premise0.01------------
assertion---------------
destruct Hinst1
destruct premise0.01------------
assertion---------------
eliminate_let
assertion---------------
case (i*3+1 < length s1)
true case (assertion)0.01------------
false case (assertion)0.90------------
assertion0.34------------
assertion0.28------------
assertion---------------
split_vc
assertion---------------
unfold encoding in H2
assertion---------------
split_premise_full
assertion---------------
instantiate H11 i
assertion3.42------------
assertion---------------
unfold encoding in H4
assertion---------------
split_premise_full
assertion---------------
instantiate H12 i
assertion---------------
instantiate H13 i
assertion6.93------------
assertion---------------
unfold encoding in H6
assertion---------------
split_premise_full
assertion---------------
instantiate H13 i
assertion---------------
instantiate H14 i
assertion30.13------------
assertion---------------
unfold encoding in H7
assertion---------------
split_premise_full
assertion---------------
instantiate H14 i
assertion4.05------------
assertion---------------
unfold encoding in H6
assertion---------------
split_premise_full
assertion---------------
instantiate H13 i
assertion---------------
instantiate H14 i
assertion5.35------------
assertion0.30------------
assertion---------------
unfold encoding in H4
assertion---------------
split_premise_full
assertion---------------
instantiate H12 i
assertion---------------
instantiate H13 i
assertion---------------
destruct Hinst
destruct premise0.01------------
assertion---------------
destruct Hinst1
destruct premise0.01------------
assertion---------------
eliminate_let
assertion---------------
case (i*3+1 < length s1)
true case (assertion)0.02------------
false case (assertion)1.78------------
assertion0.27------------
assertion0.18------------
assertion---------------
instantiate Assert i
assertion---------------
instantiate Assert1 i
assertion---------------
split_vc
VC for encode_unique0.02------------
VC for encode_unique0.02------------
VC for encode_unique0.02------------
VC for encode_unique0.02------------
assertion---------------
instantiate Assert (div i 4)
assertion0.04------------
assertion0.02------------
postcondition0.01------------
VC for encode---------------
split_vc
precondition0.06------------
precondition0.02------------
loop invariant init---------------
split_vc
loop invariant init0.01------------
loop invariant init0.01------------
loop invariant init0.01------------
loop invariant init0.02------------
integer overflow0.01------------
precondition0.03------------
integer overflow0.02------------
precondition0.04------------
precondition0.01------------
division by zero0.01------------
integer overflow0.09------------
division by zero0.03------------
integer overflow0.15------------
division by zero0.01------------
integer overflow---------------
split_vc
integer overflow0.64------------
integer overflow0.46------------
integer overflow0.37------------
division by zero0.10------------
integer overflow0.26------------
division by zero---------------
split_vc
division by zero0.02------------
integer overflow1.25------------
integer overflow1.03------------
integer overflow2.01------------
division by zero0.01------------
integer overflow------------0.04
precondition---------------
instantiate LoopInvariant (div (length r - 3) 4)
precondition0.74------------
precondition---------------
instantiate LoopInvariant (div (length r - 2) 4)
precondition0.95------------
precondition---------------
split_vc
precondition0.28------------
precondition0.42------------
precondition0.48------------
integer overflow0.08------------
assertion---------------
split_vc
assertion5.76------------
assertion4.66------------
assertion6.54------------
assertion0.86------------
assertion3.26------------
loop variant decrease0.02------------
loop invariant preservation0.03------------
loop invariant preservation0.14------------
loop invariant preservation---------------
split_vc
loop invariant preservation0.03------------
loop invariant preservation0.89------------
loop invariant preservation---------------
split_vc
loop invariant preservation0.72------------
loop invariant preservation0.79------------
loop invariant preservation1.02------------
loop invariant preservation0.98------------
assertion---------------
instantiate LoopInvariant (div (length r - 2) 4)
assertion0.98------------
assertion---------------
instantiate LoopInvariant (div (length r - 3) 4)
assertion1.21------------
integer overflow0.12------------
precondition0.14------------
precondition0.04------------
postcondition---------------
unfold encoding
VC for encode---------------
split_vc
VC for encode0.33------------
VC for encode---------------
instantiate LoopInvariant i
VC for encode---------------
remove Assert
VC for encode---------------
remove Assert
VC for encode3.49------------
VC for encode---------------
instantiate LoopInvariant i
VC for encode---------------
remove Assert
VC for encode---------------
remove Assert
VC for encode15.17------------
VC for encode---------------
instantiate LoopInvariant i
VC for encode---------------
remove Assert
VC for encode---------------
remove Assert
VC for encode8.82------------
VC for encode---------------
assert (forall i. 0 <= i < b -> valid_b64_char r2[i*4] && valid_b64_char r2[i*4+1] && valid_b64_char r2[i*4+2] && valid_b64_char r2[i*4+3])
asserted formula---------------
instantiate LoopInvariant i
asserted formula---------------
split_vc
asserted formula------------0.07
asserted formula------------0.06
asserted formula------------0.07
asserted formula------------0.06
VC for encode---------------
assert (forall i. 0 <= i < o -> r[i] = r1[i] = r2[i])
asserted formula0.17------------
VC for encode---------------
instantiate h1 (div i 4)
VC for encode---------------
remove Assert
VC for encode---------------
remove Assert
VC for encode3.28------------
VC for encode---------------
assert (get_pad r = padding)
asserted formula---------------
assert (forall i. 0 <= i < length r1 -> r1[i] <> eq_symbol)
asserted formula---------------
assert (forall i. 0 <= i < 64 -> int2b64 i <> eq_symbol)
asserted formula------0.26------
asserted formula---------------
introduce_premises
asserted formula---------------
instantiate LoopInvariant (div i 4)
asserted formula---0.77---------
asserted formula------0.44------
VC for encode0.30------------
VC for encode0.03------------
VC for encode---------------
assert (get_pad r = padding)
asserted formula---------------
assert (forall i. 0 <= i < length r1 -> r1[i] <> eq_symbol)
asserted formula---------------
assert (forall i. 0 <= i < 64 -> int2b64 i <> eq_symbol)
asserted formula------0.18------
asserted formula---------------
introduce_premises
asserted formula---------------
instantiate LoopInvariant (div i 4)
asserted formula---0.84---------
asserted formula------0.40------
VC for encode0.63------------
VC for encode0.08------------
VC for encode0.05------------
VC for encode---------------
assert (get_pad r = padding)
asserted formula---------------
assert (forall i. 0 <= i < length r1 -> r1[i] <> eq_symbol)
asserted formula---------------
assert (forall i. 0 <= i < 64 -> int2b64 i <> eq_symbol)
asserted formula------0.31------
asserted formula---------------
introduce_premises
asserted formula---------------
instantiate LoopInvariant (div i 4)
asserted formula---0.83---------
asserted formula------0.24------
VC for encode0.02------------
VC for decode---------------
split_vc
loop invariant init------------0.03
loop invariant init0.01------------
loop invariant init0.01------------
loop invariant init0.02------------
integer overflow0.02------------
precondition0.02------------
integer overflow0.02------------
precondition0.02------------
integer overflow0.02------------
precondition0.03------------
precondition0.01------------
precondition---------------
split_vc
precondition0.08------------
division by zero0.01------------
integer overflow0.01------------
precondition0.14------------
integer overflow0.06------------
integer overflow0.23------------
precondition---------------
split_vc
precondition0.16------------
division by zero0.01------------
integer overflow0.09------------
precondition0.26------------
division by zero0.02------------
integer overflow0.23------------
integer overflow0.37------------
integer overflow0.85------------
precondition0.42------------
precondition0.41------------
division by zero0.02------------
integer overflow0.22------------
integer overflow0.43------------
integer overflow1.57------------
precondition2.08------------
precondition4.65------------
precondition8.86------------
integer overflow0.33------------
assertion---------------
split_vc
assertion3.20------------
assertion12.37------------
assertion2.53------------
assertion0.64------------
loop variant decrease---------------
split_vc
loop variant decrease0.02------------
loop variant decrease0.03------------
loop invariant preservation0.59------------
loop invariant preservation0.01------------
loop invariant preservation---------------
split_vc
loop invariant preservation0.11------------
loop invariant preservation---------------
split_vc
loop invariant preservation0.78------------
loop invariant preservation0.68------------
loop invariant preservation1.19------------
integer overflow0.05------------
precondition0.02------------
postcondition1.32------------
VC for decode_encode0.09------------