Commit 017be571 authored by MARCHE Claude's avatar MARCHE Claude

In progress: bit reversal

parent 228a5cbf
module BitReversal
use import int.Int
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 }
writes { a }
ensures { a[to_uint i] = old a[to_uint j] }
ensures { a[to_uint j] = old a[to_uint i] }
ensures { forall k. 0 <= k < a.length ->
k <> to_uint i /\ k <> to_uint j -> a[k] = (old a)[k] }
=
let tmp = a[to_uint i] in
a[to_uint i] <- a[to_uint j];
a[to_uint j] <- tmp
(* a's size must be a power of two. *)
let rec aux (a:array t) (i di h hi:t)
(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 { 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 { di <> of_int 0 }
writes { a }
variant { to_uint 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 { 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) };
assert { bw_and i masklen = zeros };
assert { ult h (lsl_bv (of_int 1) loglen) };
assert { bw_and h masklen = zeros };
aux a i dj h hj loglen masklen
(BV32.sub logdi (of_int 1)) (BV32.add loghi (of_int 1));
aux a (bw_or i dj) dj (bw_or h hi) hj loglen masklen
(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) }
=
aux a (of_int 0) (of_int a.length) (of_int 0) (of_int 1)
loglen (lsl_bv ones loglen) loglen (of_int 0)
let main () =
let n = lsl_bv (of_int 1) (of_int 25) in
let a = init (to_uint n) (fun i -> of_int i) in
bit_rev a (of_int 25)
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bit_reversal.mlw" expanded="true">
<theory name="BitReversal" sum="78d22d91d33712ef59182f9944644b98" expanded="true">
<goal name="VC swap" expl="VC for swap">
<proof prover="0"><result status="valid" time="0.03" steps="91"/></proof>
</goal>
<goal name="VC aux" expl="VC for aux">
<transf name="split_goal_wp">
<goal name="VC aux.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
</goal>
<goal name="VC aux.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
</goal>
<goal name="VC aux.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.03" steps="126"/></proof>
</goal>
<goal name="VC aux.4" expl="4. assertion">
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC aux.5" expl="5. assertion">
<proof prover="1"><result status="valid" time="0.49"/></proof>
</goal>
<goal name="VC aux.6" expl="6. assertion">
<proof prover="0" timelimit="30"><result status="valid" time="0.01" steps="84"/></proof>
</goal>
<goal name="VC aux.7" expl="7. assertion">
<proof prover="1" timelimit="30"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC aux.8" expl="8. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
</goal>
<goal name="VC aux.9" expl="9. assertion">
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC aux.10" expl="10. variant decrease">
<transf name="split_goal_wp">
<goal name="VC aux.10.1" expl="1. VC for aux">
<proof prover="0"><result status="valid" time="0.03" steps="92"/></proof>
</goal>
<goal name="VC aux.10.2" expl="2. VC for aux">
<proof prover="1"><result status="valid" time="0.35"/></proof>
</goal>
</transf>
</goal>
<goal name="VC aux.11" expl="11. precondition">
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC aux.12" expl="12. precondition">
<transf name="split_goal_wp">
<goal name="VC aux.12.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
</goal>
</transf>
</goal>
<goal name="VC aux.13" expl="13. precondition">
<proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
</goal>
<goal name="VC aux.14" expl="14. precondition">
<proof prover="1"><result status="valid" time="0.37"/></proof>
</goal>
<goal name="VC aux.15" expl="15. precondition">
<proof prover="1"><result status="valid" time="2.12"/></proof>
</goal>
<goal name="VC aux.16" expl="16. precondition">
<proof prover="0"><result status="valid" time="0.27" steps="218"/></proof>
</goal>
<goal name="VC aux.17" expl="17. precondition">
<proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC aux.18" expl="18. precondition">
<proof prover="1"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="VC aux.19" expl="19. precondition">
<proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC aux.20" expl="20. precondition">
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC aux.21" expl="21. variant decrease">
<transf name="split_goal_wp">
<goal name="VC aux.21.1" expl="1. VC for aux">
<proof prover="0"><result status="valid" time="0.02" steps="93"/></proof>
<proof prover="1"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC aux.21.2" expl="2. VC for aux">
<proof prover="1"><result status="valid" time="0.37"/></proof>
</goal>
</transf>
</goal>
<goal name="VC aux.22" expl="22. precondition">
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC aux.23" expl="23. precondition">
<proof prover="1"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC aux.24" expl="24. precondition">
<proof prover="0"><result status="valid" time="0.03" steps="88"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC aux.25" expl="25. precondition">
<proof prover="1"><result status="valid" time="0.38"/></proof>
</goal>
<goal name="VC aux.26" expl="26. precondition">
<proof prover="1"><result status="valid" time="1.84"/></proof>
</goal>
<goal name="VC aux.27" expl="27. precondition">
<proof prover="0"><result status="valid" time="0.26" steps="220"/></proof>
</goal>
<goal name="VC aux.28" expl="28. precondition">
<proof prover="1"><result status="valid" time="1.94"/></proof>
</goal>
<goal name="VC aux.29" expl="29. precondition">
<proof prover="1"><result status="valid" time="0.50"/></proof>
</goal>
<goal name="VC aux.30" expl="30. precondition">
<proof prover="1"><result status="valid" time="3.92"/></proof>
</goal>
<goal name="VC aux.31" expl="31. precondition">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
<goal name="VC bit_rev" expl="VC for bit_rev">
<transf name="split_goal_wp">
<goal name="VC bit_rev.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC bit_rev.2" expl="2. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC bit_rev.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="69"/></proof>
</goal>
<goal name="VC bit_rev.4" expl="4. precondition">
<proof prover="0"><result status="valid" time="0.10" steps="88"/></proof>
</goal>
<goal name="VC bit_rev.5" expl="5. precondition">
<proof prover="0"><result status="valid" time="0.04" steps="119"/></proof>
</goal>
<goal name="VC bit_rev.6" expl="6. precondition">
<proof prover="0"><result status="valid" time="0.03" steps="76"/></proof>
</goal>
<goal name="VC bit_rev.7" expl="7. precondition">
<proof prover="0"><result status="valid" time="0.09" steps="121"/></proof>
</goal>
<goal name="VC bit_rev.8" expl="8. precondition">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC bit_rev.9" expl="9. precondition">
<proof prover="0"><result status="valid" time="0.13" steps="121"/></proof>
</goal>
<goal name="VC bit_rev.10" expl="10. precondition">
<proof prover="0"><result status="valid" time="0.07" steps="111"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main" expl="VC for main">
<transf name="split_goal_wp">
<goal name="VC main.1" expl="1. array creation size">
<proof prover="0"><result status="valid" time="0.02" steps="68"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC main.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="77"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -104,6 +104,20 @@ module Array
end
module Init
use import int.Int
use export Array
use HighOrd
val init (n: int) (f: int -> 'a) : array 'a
requires { "expl:array creation size" n >= 0 }
ensures { forall i:int. 0 <= i < n -> result[i] = f i }
ensures { result.length = n }
end
(** {2 Sorted Arrays} *)
module IntArraySorted
......
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