Commit 7caecf0f authored by MARCHE Claude's avatar MARCHE Claude

update example source

parent 9669a549
......@@ -5,14 +5,15 @@ module BitReversal
use import bv.BV32
use import array.Init
let swap (a:array 'a) (i j : t)
requires { 0 <= to_uint i < a.length }
requires { 0 <= to_uint j < a.length }
requires { 0 <= t'int i < a.length }
requires { 0 <= t'int j < a.length }
writes { a }
ensures { a[to_uint i] = old a[to_uint j] }
ensures { a[to_uint j] = old a[to_uint i] }
ensures { a[t'int i] = old a[t'int j] }
ensures { a[t'int j] = old a[t'int i] }
ensures { forall k. 0 <= k < a.length ->
k <> to_uint i /\ k <> to_uint j -> a[k] = (old a)[k] }
k <> t'int i /\ k <> t'int j -> a[k] = (old a)[k] }
=
let tmp = a[to_uint i] in
a[to_uint i] <- a[to_uint j];
......@@ -24,21 +25,21 @@ module BitReversal
(ghost loglen masklen logdi loghi:t)
requires { ult loglen (of_int 32) }
requires { masklen = lsl_bv ones loglen }
requires { a.length = to_uint (lsl_bv (of_int 1) loglen) }
requires { a.length = t'int (lsl_bv (of_int 1) loglen) }
requires { ult logdi (of_int 32) && di = lsl_bv (of_int 1) logdi }
requires { ult loghi (of_int 32) && hi = lsl_bv (of_int 1) loghi }
requires { to_uint logdi + to_uint loghi = to_uint loglen }
requires { to_uint i < a.length }
requires { to_uint di <= a.length }
requires { to_uint h < a.length }
requires { t'int logdi + t'int loghi = t'int loglen }
requires { t'int i < a.length }
requires { t'int di <= a.length }
requires { t'int h < a.length }
requires { di <> of_int 0 }
writes { a }
variant { to_uint di }
variant { t'int di }
=
if eq di (of_int 1) then (if ult i h then swap a i h) else
let dj = lsr_bv di (of_int 1) in
let hj = lsl_bv hi (of_int 1) in
assert { to_uint logdi >= 1 };
assert { t'int logdi >= 1 };
assert { ule dj (lsl_bv (of_int 1) (BV32.sub logdi (of_int 1))) };
assert { bw_and dj masklen = zeros };
assert { ult i (lsl_bv (of_int 1) loglen) };
......@@ -51,7 +52,7 @@ module BitReversal
(BV32.sub logdi (of_int 1)) (BV32.add loghi (of_int 1))
let bit_rev (a:array t) (ghost loglen:t)
requires { ult loglen (of_int 32) && a.length = to_uint (lsl_bv (of_int 1) loglen) }
requires { ult loglen (of_int 32) && a.length = t'int (lsl_bv (of_int 1) loglen) }
=
aux a (of_int 0) (of_int a.length) (of_int 0) (of_int 1)
loglen (lsl_bv ones loglen) loglen (of_int 0)
......
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