## 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

Obligations | Alt-Ergo 2.3.0 | Alt-Ergo 2.4.0 | CVC4 1.7 | Z3 4.8.10 | Z3 4.8.6 | ||||||||||

VC for int2b64 | 0.05 | --- | --- | --- | --- | ||||||||||

VC for eq_symbol | 0.01 | --- | --- | --- | --- | ||||||||||

int2b64_valid_4_char | 0.02 | --- | --- | --- | --- | ||||||||||

VC for b642int | 0.29 | --- | --- | --- | --- | ||||||||||

b642int_int2b64 | 0.05 | --- | --- | --- | --- | ||||||||||

VC for get_pad | 0.35 | --- | --- | --- | --- | ||||||||||

calc_pad_mod3 | --- | --- | --- | --- | --- | ||||||||||

introduce_premises | |||||||||||||||

calc_pad_mod3.0 | --- | --- | --- | --- | --- | ||||||||||

case (mod (length s) 3 = 0) | |||||||||||||||

true case | 0.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 case | 0.03 | --- | --- | --- | --- | ||||||||||

VC for calc_pad | 0.81 | --- | --- | --- | --- | ||||||||||

VC for encoding_valid_b64 | 2.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.02 | 0.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.02 | 0.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.02 | 0.03 | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate Assert (div i 3) | |||||||||||||||

assertion | 0.08 | --- | --- | --- | --- | ||||||||||

postcondition | --- | --- | --- | --- | --- | ||||||||||

apply extensionality | |||||||||||||||

apply premises | 0.11 | --- | --- | --- | --- | ||||||||||

VC for encode_unique | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

assertion | 0.01 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

unfold encoding in H3 | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_premise_full | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H12 i | |||||||||||||||

assertion | 2.41 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

unfold encoding in H5 | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_premise_full | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H14 i | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H13 i | |||||||||||||||

assertion | 9.79 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

unfold encoding in H7 | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_premise_full | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H14 i | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H15 i | |||||||||||||||

assertion | 16.44 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

unfold encoding in H8 | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_premise_full | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H15 i | |||||||||||||||

assertion | 4.91 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

unfold encoding in H7 | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_premise_full | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H14 i | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H15 i | |||||||||||||||

assertion | 5.57 | --- | --- | --- | --- | ||||||||||

assertion | 0.28 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

unfold encoding in H5 | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_premise_full | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H13 i | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H14 i | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

destruct Hinst | |||||||||||||||

destruct premise | 0.01 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

destruct Hinst1 | |||||||||||||||

destruct premise | 0.01 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

eliminate_let | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

case (i*3+1 < length s1) | |||||||||||||||

true case (assertion) | 0.01 | --- | --- | --- | --- | ||||||||||

false case (assertion) | 0.90 | --- | --- | --- | --- | ||||||||||

assertion | 0.34 | --- | --- | --- | --- | ||||||||||

assertion | 0.28 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

unfold encoding in H2 | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_premise_full | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H11 i | |||||||||||||||

assertion | 3.42 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

unfold encoding in H4 | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_premise_full | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H12 i | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H13 i | |||||||||||||||

assertion | 6.93 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

unfold encoding in H6 | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_premise_full | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H13 i | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H14 i | |||||||||||||||

assertion | 30.13 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

unfold encoding in H7 | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_premise_full | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H14 i | |||||||||||||||

assertion | 4.05 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

unfold encoding in H6 | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_premise_full | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H13 i | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H14 i | |||||||||||||||

assertion | 5.35 | --- | --- | --- | --- | ||||||||||

assertion | 0.30 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

unfold encoding in H4 | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_premise_full | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H12 i | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate H13 i | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

destruct Hinst | |||||||||||||||

destruct premise | 0.01 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

destruct Hinst1 | |||||||||||||||

destruct premise | 0.01 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

eliminate_let | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

case (i*3+1 < length s1) | |||||||||||||||

true case (assertion) | 0.02 | --- | --- | --- | --- | ||||||||||

false case (assertion) | 1.78 | --- | --- | --- | --- | ||||||||||

assertion | 0.27 | --- | --- | --- | --- | ||||||||||

assertion | 0.18 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate Assert i | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate Assert1 i | |||||||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

VC for encode_unique | 0.02 | --- | --- | --- | --- | ||||||||||

VC for encode_unique | 0.02 | --- | --- | --- | --- | ||||||||||

VC for encode_unique | 0.02 | --- | --- | --- | --- | ||||||||||

VC for encode_unique | 0.02 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate Assert (div i 4) | |||||||||||||||

assertion | 0.04 | --- | --- | --- | --- | ||||||||||

assertion | 0.02 | --- | --- | --- | --- | ||||||||||

postcondition | 0.01 | --- | --- | --- | --- | ||||||||||

VC for encode | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

precondition | 0.06 | --- | --- | --- | --- | ||||||||||

precondition | 0.02 | --- | --- | --- | --- | ||||||||||

loop invariant init | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

loop invariant init | 0.01 | --- | --- | --- | --- | ||||||||||

loop invariant init | 0.01 | --- | --- | --- | --- | ||||||||||

loop invariant init | 0.01 | --- | --- | --- | --- | ||||||||||

loop invariant init | 0.02 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.01 | --- | --- | --- | --- | ||||||||||

precondition | 0.03 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.02 | --- | --- | --- | --- | ||||||||||

precondition | 0.04 | --- | --- | --- | --- | ||||||||||

precondition | 0.01 | --- | --- | --- | --- | ||||||||||

division by zero | 0.01 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.09 | --- | --- | --- | --- | ||||||||||

division by zero | 0.03 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.15 | --- | --- | --- | --- | ||||||||||

division by zero | 0.01 | --- | --- | --- | --- | ||||||||||

integer overflow | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

integer overflow | 0.64 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.46 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.37 | --- | --- | --- | --- | ||||||||||

division by zero | 0.10 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.26 | --- | --- | --- | --- | ||||||||||

division by zero | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

division by zero | 0.02 | --- | --- | --- | --- | ||||||||||

integer overflow | 1.25 | --- | --- | --- | --- | ||||||||||

integer overflow | 1.03 | --- | --- | --- | --- | ||||||||||

integer overflow | 2.01 | --- | --- | --- | --- | ||||||||||

division by zero | 0.01 | --- | --- | --- | --- | ||||||||||

integer overflow | --- | --- | --- | --- | 0.04 | ||||||||||

precondition | --- | --- | --- | --- | --- | ||||||||||

instantiate LoopInvariant (div (length r - 3) 4) | |||||||||||||||

precondition | 0.74 | --- | --- | --- | --- | ||||||||||

precondition | --- | --- | --- | --- | --- | ||||||||||

instantiate LoopInvariant (div (length r - 2) 4) | |||||||||||||||

precondition | 0.95 | --- | --- | --- | --- | ||||||||||

precondition | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

precondition | 0.28 | --- | --- | --- | --- | ||||||||||

precondition | 0.42 | --- | --- | --- | --- | ||||||||||

precondition | 0.48 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.08 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

assertion | 5.76 | --- | --- | --- | --- | ||||||||||

assertion | 4.66 | --- | --- | --- | --- | ||||||||||

assertion | 6.54 | --- | --- | --- | --- | ||||||||||

assertion | 0.86 | --- | --- | --- | --- | ||||||||||

assertion | 3.26 | --- | --- | --- | --- | ||||||||||

loop variant decrease | 0.02 | --- | --- | --- | --- | ||||||||||

loop invariant preservation | 0.03 | --- | --- | --- | --- | ||||||||||

loop invariant preservation | 0.14 | --- | --- | --- | --- | ||||||||||

loop invariant preservation | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

loop invariant preservation | 0.03 | --- | --- | --- | --- | ||||||||||

loop invariant preservation | 0.89 | --- | --- | --- | --- | ||||||||||

loop invariant preservation | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

loop invariant preservation | 0.72 | --- | --- | --- | --- | ||||||||||

loop invariant preservation | 0.79 | --- | --- | --- | --- | ||||||||||

loop invariant preservation | 1.02 | --- | --- | --- | --- | ||||||||||

loop invariant preservation | 0.98 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate LoopInvariant (div (length r - 2) 4) | |||||||||||||||

assertion | 0.98 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

instantiate LoopInvariant (div (length r - 3) 4) | |||||||||||||||

assertion | 1.21 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.12 | --- | --- | --- | --- | ||||||||||

precondition | 0.14 | --- | --- | --- | --- | ||||||||||

precondition | 0.04 | --- | --- | --- | --- | ||||||||||

postcondition | --- | --- | --- | --- | --- | ||||||||||

unfold encoding | |||||||||||||||

VC for encode | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

VC for encode | 0.33 | --- | --- | --- | --- | ||||||||||

VC for encode | --- | --- | --- | --- | --- | ||||||||||

instantiate LoopInvariant i | |||||||||||||||

VC for encode | --- | --- | --- | --- | --- | ||||||||||

remove Assert | |||||||||||||||

VC for encode | --- | --- | --- | --- | --- | ||||||||||

remove Assert | |||||||||||||||

VC for encode | 3.49 | --- | --- | --- | --- | ||||||||||

VC for encode | --- | --- | --- | --- | --- | ||||||||||

instantiate LoopInvariant i | |||||||||||||||

VC for encode | --- | --- | --- | --- | --- | ||||||||||

remove Assert | |||||||||||||||

VC for encode | --- | --- | --- | --- | --- | ||||||||||

remove Assert | |||||||||||||||

VC for encode | 15.17 | --- | --- | --- | --- | ||||||||||

VC for encode | --- | --- | --- | --- | --- | ||||||||||

instantiate LoopInvariant i | |||||||||||||||

VC for encode | --- | --- | --- | --- | --- | ||||||||||

remove Assert | |||||||||||||||

VC for encode | --- | --- | --- | --- | --- | ||||||||||

remove Assert | |||||||||||||||

VC for encode | 8.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 formula | 0.17 | --- | --- | --- | --- | ||||||||||

VC for encode | --- | --- | --- | --- | --- | ||||||||||

instantiate h1 (div i 4) | |||||||||||||||

VC for encode | --- | --- | --- | --- | --- | ||||||||||

remove Assert | |||||||||||||||

VC for encode | --- | --- | --- | --- | --- | ||||||||||

remove Assert | |||||||||||||||

VC for encode | 3.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 encode | 0.30 | --- | --- | --- | --- | ||||||||||

VC for encode | 0.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 encode | 0.63 | --- | --- | --- | --- | ||||||||||

VC for encode | 0.08 | --- | --- | --- | --- | ||||||||||

VC for encode | 0.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 encode | 0.02 | --- | --- | --- | --- | ||||||||||

VC for decode | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

loop invariant init | --- | --- | --- | --- | 0.03 | ||||||||||

loop invariant init | 0.01 | --- | --- | --- | --- | ||||||||||

loop invariant init | 0.01 | --- | --- | --- | --- | ||||||||||

loop invariant init | 0.02 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.02 | --- | --- | --- | --- | ||||||||||

precondition | 0.02 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.02 | --- | --- | --- | --- | ||||||||||

precondition | 0.02 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.02 | --- | --- | --- | --- | ||||||||||

precondition | 0.03 | --- | --- | --- | --- | ||||||||||

precondition | 0.01 | --- | --- | --- | --- | ||||||||||

precondition | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

precondition | 0.08 | --- | --- | --- | --- | ||||||||||

division by zero | 0.01 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.01 | --- | --- | --- | --- | ||||||||||

precondition | 0.14 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.06 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.23 | --- | --- | --- | --- | ||||||||||

precondition | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

precondition | 0.16 | --- | --- | --- | --- | ||||||||||

division by zero | 0.01 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.09 | --- | --- | --- | --- | ||||||||||

precondition | 0.26 | --- | --- | --- | --- | ||||||||||

division by zero | 0.02 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.23 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.37 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.85 | --- | --- | --- | --- | ||||||||||

precondition | 0.42 | --- | --- | --- | --- | ||||||||||

precondition | 0.41 | --- | --- | --- | --- | ||||||||||

division by zero | 0.02 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.22 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.43 | --- | --- | --- | --- | ||||||||||

integer overflow | 1.57 | --- | --- | --- | --- | ||||||||||

precondition | 2.08 | --- | --- | --- | --- | ||||||||||

precondition | 4.65 | --- | --- | --- | --- | ||||||||||

precondition | 8.86 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.33 | --- | --- | --- | --- | ||||||||||

assertion | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

assertion | 3.20 | --- | --- | --- | --- | ||||||||||

assertion | 12.37 | --- | --- | --- | --- | ||||||||||

assertion | 2.53 | --- | --- | --- | --- | ||||||||||

assertion | 0.64 | --- | --- | --- | --- | ||||||||||

loop variant decrease | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

loop variant decrease | 0.02 | --- | --- | --- | --- | ||||||||||

loop variant decrease | 0.03 | --- | --- | --- | --- | ||||||||||

loop invariant preservation | 0.59 | --- | --- | --- | --- | ||||||||||

loop invariant preservation | 0.01 | --- | --- | --- | --- | ||||||||||

loop invariant preservation | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

loop invariant preservation | 0.11 | --- | --- | --- | --- | ||||||||||

loop invariant preservation | --- | --- | --- | --- | --- | ||||||||||

split_vc | |||||||||||||||

loop invariant preservation | 0.78 | --- | --- | --- | --- | ||||||||||

loop invariant preservation | 0.68 | --- | --- | --- | --- | ||||||||||

loop invariant preservation | 1.19 | --- | --- | --- | --- | ||||||||||

integer overflow | 0.05 | --- | --- | --- | --- | ||||||||||

precondition | 0.02 | --- | --- | --- | --- | ||||||||||

postcondition | 1.32 | --- | --- | --- | --- | ||||||||||

VC for decode_encode | 0.09 | --- | --- | --- | --- |