minor cosmetic fix base64 example

parent 1349b793
......@@ -83,7 +83,7 @@ module Base64
else absurd
(** character '=' *)
let function char_eq : char = chr 61
let function eq_symbol : char = chr 61
(** `valid_b64_char c` is true, if and only if, `c` is in the table
above *)
......@@ -100,18 +100,18 @@ module Base64
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 = char_eq then 0 else (* 0 *)
if c = eq_symbol then 0 else (* 0 *)
64 (* 64 *)
let b642int (c: char) : int63
requires { valid_b64_char c || c = char_eq }
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 char_eq then 0 else
if eq_char c eq_symbol then 0 else
absurd
lemma b642int_int2b64: forall i. 0 <= i < 64 -> b642int (int2b64 i) = i
......@@ -119,14 +119,14 @@ module Base64
(** `get_pad s` calculates the number of padding characters in the
string `s` (between 0 and 2) *)
function get_pad (s: string): int =
if length s >= 1 && s[length s - 1] = char_eq then
(if length s >= 2 && s[length s - 2] = char_eq then 2 else 1)
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
let get_pad (s: string): int63
ensures { result = get_pad s }
= if length s >= 1 && eq_char s[length s - 1] char_eq then
(if length s >= 2 && eq_char s[length s - 2] char_eq then 2 else 1)
= 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
(** `calc_pad s` returns the number of padding characters that will
......@@ -155,9 +155,9 @@ module Base64
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] = char_eq ) &&
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] = char_eq ) &&
s2[length s2 - 2] = s2[length s2 - 1] = eq_symbol ) &&
calc_pad s1 = get_pad s2
(** `valid_b64 s` is true, if and only if, `s` is a valid Base64
......@@ -169,10 +169,10 @@ module Base64
(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] = char_eq) &&
s[length s - 1] = eq_symbol) &&
(get_pad s = 2 -> mod (b642int s[length s - 3]) 16 = 0 &&
s[length s - 2] = char_eq &&
s[length s - 1] = char_eq)
s[length s - 2] = eq_symbol &&
s[length s - 1] = eq_symbol)
let lemma encoding_valid_b64 (s1 s2: string)
requires { encoding s1 s2 }
......@@ -187,12 +187,12 @@ module Base64
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] = char_eq && s2[last*4+3] = char_eq
else valid_b64_char s2[last*4+2] && s2[last*4+3] = char_eq
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] = char_eq) }
(length s2 - get_pad s2 <= i < length s2 -> s2[i] = eq_symbol) }
(** the decode of a string is unique *)
......@@ -218,12 +218,12 @@ module Base64
( 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] = char_eq)
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] = char_eq
&& s2[i*4+3] = char_eq)
&& 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
......@@ -233,12 +233,12 @@ module Base64
( 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] = char_eq)
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] = char_eq
&& s3[i*4+3] = char_eq)
&& 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]
......@@ -287,7 +287,7 @@ module Base64
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 char_eq);
StringBuffer.add_string r (make padding eq_symbol);
StringBuffer.contents r
let decode (s: string) : string
......
......@@ -3,7 +3,9 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="Z3" version="4.8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.3.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.7" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file format="whyml" proved="true">
<path name=".."/><path name="string_base64_encoding.mlw"/>
......@@ -11,7 +13,7 @@
<goal name="int2b64&#39;vc" expl="VC for int2b64" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.05" steps="316"/></proof>
</goal>
<goal name="char_eq&#39;vc" expl="VC for char_eq" proved="true">
<goal name="eq_symbol&#39;vc" expl="VC for eq_symbol" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="int2b64_valid_4_char" proved="true">
......@@ -744,26 +746,18 @@
<goal name="encode&#39;vc.44.0.5" expl="VC for encode" proved="true">
<transf name="assert" proved="true" arg1="(get_pad r = padding)">
<goal name="encode&#39;vc.44.0.5.0" expl="asserted formula" proved="true">
<transf name="assert" proved="true" arg1="(forall i. 0 &lt;= i &lt; length r1 -&gt; r1[i] &lt;&gt; char_eq)">
<transf name="assert" proved="true" arg1="(forall i. 0 &lt;= i &lt; length r1 -&gt; r1[i] &lt;&gt; eq_symbol)">
<goal name="encode&#39;vc.44.0.5.0.0" expl="asserted formula" proved="true">
<transf name="assert" proved="true" arg1="(forall i. 0 &lt;= i &lt; 64 -&gt; int2b64 i &lt;&gt; char_eq)">
<transf name="assert" proved="true" arg1="(forall i. 0 &lt;= i &lt; 64 -&gt; int2b64 i &lt;&gt; eq_symbol)">
<goal name="encode&#39;vc.44.0.5.0.0.0" expl="asserted formula" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="encode&#39;vc.44.0.5.0.0.0.0" expl="asserted formula" proved="true">
<transf name="instantiate" proved="true" arg1="LoopInvariant" arg2="(div i 4)">
<goal name="encode&#39;vc.44.0.5.0.0.0.0.0" expl="asserted formula" proved="true">
<proof prover="2"><result status="valid" time="0.17" steps="201"/></proof>
</goal>
</transf>
</goal>
</transf>
<proof prover="3"><result status="valid" time="0.26" steps="36339"/></proof>
</goal>
<goal name="encode&#39;vc.44.0.5.0.0.1" expl="asserted formula" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="encode&#39;vc.44.0.5.0.0.1.0" expl="asserted formula" proved="true">
<transf name="instantiate" proved="true" arg1="LoopInvariant" arg2="(div i 4)">
<goal name="encode&#39;vc.44.0.5.0.0.1.0.0" expl="asserted formula" proved="true">
<proof prover="2"><result status="valid" time="0.86" steps="1661"/></proof>
<proof prover="1"><result status="valid" time="1.16" steps="1604"/></proof>
</goal>
</transf>
</goal>
......@@ -772,7 +766,7 @@
</transf>
</goal>
<goal name="encode&#39;vc.44.0.5.0.1" expl="asserted formula" proved="true">
<proof prover="2" timelimit="30"><result status="valid" time="0.88" steps="1919"/></proof>
<proof prover="3"><result status="valid" time="0.64" steps="63900"/></proof>
</goal>
</transf>
</goal>
......@@ -787,26 +781,18 @@
<goal name="encode&#39;vc.44.0.7" expl="VC for encode" proved="true">
<transf name="assert" proved="true" arg1="(get_pad r = padding)">
<goal name="encode&#39;vc.44.0.7.0" expl="asserted formula" proved="true">
<transf name="assert" proved="true" arg1="(forall i. 0 &lt;= i &lt; length r1 -&gt; r1[i] &lt;&gt; char_eq)">
<transf name="assert" proved="true" arg1="(forall i. 0 &lt;= i &lt; length r1 -&gt; r1[i] &lt;&gt; eq_symbol)">
<goal name="encode&#39;vc.44.0.7.0.0" expl="asserted formula" proved="true">
<transf name="assert" proved="true" arg1="(forall i. 0 &lt;= i &lt; 64 -&gt; int2b64 i &lt;&gt; char_eq)">
<transf name="assert" proved="true" arg1="(forall i. 0 &lt;= i &lt; 64 -&gt; int2b64 i &lt;&gt; eq_symbol)">
<goal name="encode&#39;vc.44.0.7.0.0.0" expl="asserted formula" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="encode&#39;vc.44.0.7.0.0.0.0" expl="asserted formula" proved="true">
<transf name="instantiate" proved="true" arg1="LoopInvariant" arg2="(div i 4)">
<goal name="encode&#39;vc.44.0.7.0.0.0.0.0" expl="asserted formula" proved="true">
<proof prover="2"><result status="valid" time="0.19" steps="309"/></proof>
</goal>
</transf>
</goal>
</transf>
<proof prover="3"><result status="valid" time="0.33" steps="35840"/></proof>
</goal>
<goal name="encode&#39;vc.44.0.7.0.0.1" expl="asserted formula" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="encode&#39;vc.44.0.7.0.0.1.0" expl="asserted formula" proved="true">
<transf name="instantiate" proved="true" arg1="LoopInvariant" arg2="(div i 4)">
<goal name="encode&#39;vc.44.0.7.0.0.1.0.0" expl="asserted formula" proved="true">
<proof prover="2"><result status="valid" time="0.89" steps="1777"/></proof>
<proof prover="1"><result status="valid" time="1.21" steps="1777"/></proof>
</goal>
</transf>
</goal>
......@@ -815,7 +801,7 @@
</transf>
</goal>
<goal name="encode&#39;vc.44.0.7.0.1" expl="asserted formula" proved="true">
<proof prover="2" timelimit="30"><result status="valid" time="0.55" steps="675"/></proof>
<proof prover="3"><result status="valid" time="0.65" steps="61336"/></proof>
</goal>
</transf>
</goal>
......@@ -833,26 +819,18 @@
<goal name="encode&#39;vc.44.0.10" expl="VC for encode" proved="true">
<transf name="assert" proved="true" arg1="(get_pad r = padding)">
<goal name="encode&#39;vc.44.0.10.0" expl="asserted formula" proved="true">
<transf name="assert" proved="true" arg1="(forall i. 0 &lt;= i &lt; length r1 -&gt; r1[i] &lt;&gt; char_eq)">
<transf name="assert" proved="true" arg1="(forall i. 0 &lt;= i &lt; length r1 -&gt; r1[i] &lt;&gt; eq_symbol)">
<goal name="encode&#39;vc.44.0.10.0.0" expl="asserted formula" proved="true">
<transf name="assert" proved="true" arg1="(forall i. 0 &lt;= i &lt; 64 -&gt; int2b64 i &lt;&gt; char_eq)">
<transf name="assert" proved="true" arg1="(forall i. 0 &lt;= i &lt; 64 -&gt; int2b64 i &lt;&gt; eq_symbol)">
<goal name="encode&#39;vc.44.0.10.0.0.0" expl="asserted formula" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="encode&#39;vc.44.0.10.0.0.0.0" expl="asserted formula" proved="true">
<transf name="instantiate" proved="true" arg1="LoopInvariant" arg2="(div i 4)">
<goal name="encode&#39;vc.44.0.10.0.0.0.0.0" expl="asserted formula" proved="true">
<proof prover="2"><result status="valid" time="0.23" steps="251"/></proof>
</goal>
</transf>
</goal>
</transf>
<proof prover="3"><result status="valid" time="0.31" steps="39444"/></proof>
</goal>
<goal name="encode&#39;vc.44.0.10.0.0.1" expl="asserted formula" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="encode&#39;vc.44.0.10.0.0.1.0" expl="asserted formula" proved="true">
<transf name="instantiate" proved="true" arg1="LoopInvariant" arg2="(div i 4)">
<goal name="encode&#39;vc.44.0.10.0.0.1.0.0" expl="asserted formula" proved="true">
<proof prover="2"><result status="valid" time="0.76" steps="1425"/></proof>
<proof prover="1"><result status="valid" time="1.06" steps="1425"/></proof>
</goal>
</transf>
</goal>
......@@ -861,7 +839,7 @@
</transf>
</goal>
<goal name="encode&#39;vc.44.0.10.0.1" expl="asserted formula" proved="true">
<proof prover="2" timelimit="30"><result status="valid" time="2.07" steps="4576"/></proof>
<proof prover="3"><result status="valid" time="0.24" steps="34455"/></proof>
</goal>
</transf>
</goal>
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment