Skip to content

GitLab

why3
why3
Commit f0547868 authored by Clément Fumex's avatar Clément Fumex
Browse files
Options

Add the ability to 

* declare range types and float types,
* use integer (resp. real) literals for those types through casting,
* specify how to print them in drivers.

Change in syntax
* use

  type t = < range 1 2 >   (* integers from 1 to 2 *)
  type t' = < float 4 12 > (* float with 4 bits in exponent and 12 in mantissa *)

  the two projections :
  t'int
  t''real

  and the predicate :
  t''isFinite

* Restrict the use of "'" in whyml:
  Users are not allowed to introduce names where a quote symbol
  is followed by a letter. Thus, the following identifiers are
  valid:

  t'
  toto'0''
  toto'_phi

  whereas toto'phi is not.

Note: we do not yet support negative numbers in range declaration
and casting of a literal.
parent 0026440d
Hide whitespace changes
Inline Side-by-side
Showing with 3322 additions and 1930 deletions
Makefile.in
View file @ f0547868
......@@ -181,8 +181,7 @@ LIB_MLW = ity expr dexpr pdecl pmodule
LIB_PARSER = ptree glob parser typing lexer
LIB_TRANSFORM = simplify_formula inlining split_goal induction \
detect_polymorphism \
reduction_engine compute \
detect_polymorphism reduction_engine compute \
eliminate_definition eliminate_algebraic \
eliminate_inductive eliminate_let eliminate_if \
libencoding discriminate encoding encoding_select \
......@@ -193,7 +192,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
eliminate_epsilon intro_projections_counterexmp \
intro_vc_vars_counterexmp prepare_for_counterexmp \
eval_match instantiate_predicate smoke_detector \
induction_pr prop_curry
induction_pr prop_curry eliminate_literal
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
simplify gappa cvc3 yices mathematica
......
drivers/alt_ergo_common.drv
View file @ f0547868
......@@ -20,13 +20,13 @@ steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\))" 2
steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\) steps)" 2
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
drivers/coq-common.gen
View file @ f0547868
......@@ -4,9 +4,9 @@ unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "eliminate_non_struct_recursion"
transformation "eliminate_if"
transformation "eliminate_literal"
transformation "eliminate_non_lambda_set_epsilon"
transformation "eliminate_projections"
......
drivers/cvc3.drv
View file @ f0547868
......@@ -14,13 +14,12 @@ outofmemory "Out of memory\\|std::bad_alloc\\|GNU MP: Cannot allocate memory"
timeout "self-timeout"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
drivers/cvc4.drv
View file @ f0547868
......@@ -16,6 +16,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
drivers/cvc4_14.drv
View file @ f0547868
......@@ -27,6 +27,7 @@ transformation "eliminate_definition"
*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
drivers/cvc4_bv.gen
View file @ f0547868
......@@ -3,20 +3,20 @@
theory bv.BV64
syntax converter of_int "(_ bv%1 64)"
syntax function to_uint "(bv2nat %1)"
syntax function t'int "(bv2nat %1)"
end
theory bv.BV32
syntax converter of_int "(_ bv%1 32)"
syntax function to_uint "(bv2nat %1)"
syntax function t'int "(bv2nat %1)"
end
theory bv.BV16
syntax converter of_int "(_ bv%1 16)"
syntax function to_uint "(bv2nat %1)"
syntax function t'int "(bv2nat %1)"
end
theory bv.BV8
syntax converter of_int "(_ bv%1 8)"
syntax function to_uint "(bv2nat %1)"
syntax function t'int "(bv2nat %1)"
end
drivers/isabelle-common.gen
View file @ f0547868
......@@ -6,6 +6,7 @@ valid "Finished Why3 theory"
fail "\\*\\*\\* \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if_fmla"
transformation "eliminate_let_fmla"
......
drivers/mathsat.drv
View file @ f0547868
......@@ -12,9 +12,7 @@ outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
......
drivers/psyche.drv
View file @ f0547868
......@@ -10,9 +10,7 @@ invalid "^NOT PROVABLE"
timeout "interrupted by timeout"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
......
drivers/smt-libv2-bv-realization.gen
View file @ f0547868
......@@ -62,8 +62,10 @@ theory bv.BV_Gen
remove prop to_uint_bounds
remove prop to_uint_of_int
remove prop Of_int_zeros
remove prop Of_int_ones
remove prop to_uint_size_bv
remove prop to_uint_zeros
remove prop to_uint_ones
remove prop to_uint_one
(** Arithmetic operators *)
......
drivers/smt-libv2-bv.gen
View file @ f0547868
......@@ -48,8 +48,10 @@ theory bv.BV_Gen
remove prop to_uint_bounds
remove prop to_int_extensionality
remove prop Of_int_zeros
remove prop Of_int_ones
remove prop to_uint_size_bv
remove prop to_uint_zeros
remove prop to_uint_ones
remove prop to_uint_one
remove prop to_uint_add
remove prop to_uint_add_bounded
......@@ -76,40 +78,60 @@ theory bv.BV_Gen
end
theory bv.BV64
meta "literal:keep" type t
syntax literal t "#x%16x"
syntax type t "(_ BitVec 64)"
syntax function zeros "#x0000000000000000"
syntax function ones "#xFFFFFFFFFFFFFFFF"
syntax function one "#x0000000000000001"
syntax function ones "#xFFFFFFFFFFFFFFFF"
syntax function size_bv "(_ bv64 64)"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
end
theory bv.BV32
meta "literal:keep" type t
syntax literal t "#x%8x"
syntax type t "(_ BitVec 32)"
syntax function zeros "#x00000000"
syntax function ones "#xFFFFFFFF"
syntax function one "#x00000001"
syntax function ones "#xFFFFFFFF"
syntax function size_bv "(_ bv32 32)"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv32 32))) (bvshl %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
end
theory bv.BV16
meta "literal:keep" type t
syntax literal t "#x%4x"
syntax type t "(_ BitVec 16)"
syntax function zeros "#x0000"
syntax function ones "#xFFFF"
syntax function one "#x0001"
syntax function ones "#xFFFF"
syntax function size_bv "(_ bv16 16)"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv16 16))) (bvshl %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
end
theory bv.BV8
meta "literal:keep" type t
syntax literal t (* "#b%8b" *) "#x%2x"
syntax type t "(_ BitVec 8)"
syntax function zeros "#x00"
syntax function ones "#xFF"
syntax function one "#x01"
syntax function ones "#xFF"
syntax function size_bv "(_ bv8 8)"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv8 8))) (bvlshr %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
......
drivers/yices.drv
View file @ f0547868
......@@ -11,9 +11,7 @@ unknown "\\bunknown\\b\\|\\bsat\\b" ""
unknown "feature not supported: non linear problem" "non linear arith"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
......
drivers/z3-realize.drv deleted 100644 → 0
View file @ 0026440d
(** Why3 driver for Z3 >= 4.3.2 *)
(* Do not set any logic, let z3 choose by itself
prelude "(set-logic AUFNIRA)"
*)
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2-bv-realization.gen"
import "discrimination.gen"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "detect_polymorphism"
transformation "eliminate_definition"
(* We could keep more definitions by using
transformation "eliminate_definition_if_poly"
instead, but some proofs are lost
(examples/logic/triangle_inequality.why)
*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
(* Prepare for counter-example query: get rid of some quantifiers (makes it
possible to query model values of the variables in premises) and introduce
counter-example projections *)
transformation "prepare_for_counterexmp"
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"
(** Error messages specific to Z3 *)
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
(** Extra theories supported by Z3 *)
(* div/mod of Z3 seems to be Euclidean Division *)
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
theory real.FromInt
syntax function from_int "(to_real %1)"
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
(* does not work: Z3 segfaults
theory real.Trigonometry
syntax function cos "(cos %1)"
syntax function sin "(sin %1)"
syntax function pi "pi"
syntax function tan "(tan %1)"
syntax function atan "(atan %1)"
end
*)
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
have the same name for the function to_uint *)
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
syntax function to_uint "(bv2int %1)"
end
drivers/z3_432.drv
View file @ f0547868
......@@ -7,7 +7,6 @@
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
import "no-bv.gen"
import "discrimination.gen"
......@@ -23,6 +22,7 @@ transformation "eliminate_definition"
*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
drivers/z3_440.drv
View file @ f0547868
......@@ -23,6 +23,7 @@ transformation "eliminate_definition"
*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......@@ -81,7 +82,7 @@ end
have the same name for the function to_uint *)
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
syntax function to_uint "(bv2int %1)"
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
......@@ -89,7 +90,7 @@ end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
syntax function to_uint "(bv2int %1)"
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
......@@ -97,7 +98,7 @@ end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
syntax function to_uint "(bv2int %1)"
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
......@@ -105,7 +106,7 @@ end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
syntax function to_uint "(bv2int %1)"
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
......
drivers/z3_smtv1.drv
View file @ f0547868
......@@ -10,9 +10,7 @@ unknown "^\\(unknown\\|sat\\|Fail\\)" ""
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
......
examples/binary_search/why3session.xml
View file @ f0547868
......@@ -21,87 +21,87 @@
<proof prover="5" timelimit="10"><result status="valid" time="0.02" steps="44"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="e1d44ffe67ec79d3738d89b5a90b5f4e" expanded="true">
<theory name="BinarySearchInt32" sum="f5215003128fd45477d65ffa703ca26d" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter binary_search.1" expl="1. integer overflow">
<proof prover="5"><result status="valid" time="0.02" steps="69"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="71"/></proof>
</goal>
<goal name="WP_parameter binary_search.2" expl="2. integer overflow">
<proof prover="5"><result status="valid" time="0.01" steps="73"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="75"/></proof>
</goal>
<goal name="WP_parameter binary_search.3" expl="3. integer overflow">
<proof prover="5"><result status="valid" time="0.12" steps="93"/></proof>
<proof prover="5"><result status="valid" time="0.12" steps="105"/></proof>
</goal>
<goal name="WP_parameter binary_search.4" expl="4. loop invariant init">
<proof prover="5"><result status="valid" time="0.01" steps="74"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="76"/></proof>
</goal>
<goal name="WP_parameter binary_search.5" expl="5. loop invariant init">
<proof prover="5"><result status="valid" time="0.01" steps="77"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="79"/></proof>
</goal>
<goal name="WP_parameter binary_search.6" expl="6. integer overflow">
<proof prover="5"><result status="valid" time="0.02" steps="85"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="87"/></proof>
</goal>
<goal name="WP_parameter binary_search.7" expl="7. integer overflow">
<proof prover="5"><result status="valid" time="0.02" steps="89"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="91"/></proof>
</goal>
<goal name="WP_parameter binary_search.8" expl="8. division by zero">
<proof prover="5"><result status="valid" time="0.01" steps="82"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="84"/></proof>
</goal>
<goal name="WP_parameter binary_search.9" expl="9. integer overflow">
<proof prover="5"><result status="valid" time="0.04" steps="97"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="99"/></proof>
</goal>
<goal name="WP_parameter binary_search.10" expl="10. integer overflow">
<proof prover="5"><result status="valid" time="0.11" steps="113"/></proof>
<proof prover="5"><result status="valid" time="0.11" steps="127"/></proof>
</goal>
<goal name="WP_parameter binary_search.11" expl="11. assertion">
<proof prover="5"><result status="valid" time="0.27" steps="132"/></proof>
<proof prover="5"><result status="valid" time="0.27" steps="158"/></proof>
</goal>
<goal name="WP_parameter binary_search.12" expl="12. index in array bounds">
<proof prover="5"><result status="valid" time="0.01" steps="89"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="91"/></proof>
</goal>
<goal name="WP_parameter binary_search.13" expl="13. integer overflow">
<proof prover="5"><result status="valid" time="0.01" steps="93"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="95"/></proof>
</goal>
<goal name="WP_parameter binary_search.14" expl="14. integer overflow">
<proof prover="5"><result status="valid" time="0.03" steps="110"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="112"/></proof>
</goal>
<goal name="WP_parameter binary_search.15" expl="15. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.02" steps="97"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="99"/></proof>
</goal>
<goal name="WP_parameter binary_search.16" expl="16. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="3.48"/></proof>
<proof prover="5"><result status="valid" time="1.34" steps="176"/></proof>
<proof prover="5"><result status="valid" time="1.34" steps="202"/></proof>
</goal>
<goal name="WP_parameter binary_search.17" expl="17. loop variant decrease">
<proof prover="5"><result status="valid" time="0.02" steps="97"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="99"/></proof>
</goal>
<goal name="WP_parameter binary_search.18" expl="18. index in array bounds">
<proof prover="5"><result status="valid" time="0.01" steps="93"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="95"/></proof>
</goal>
<goal name="WP_parameter binary_search.19" expl="19. integer overflow">
<proof prover="5"><result status="valid" time="0.01" steps="95"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="97"/></proof>
</goal>
<goal name="WP_parameter binary_search.20" expl="20. integer overflow">
<proof prover="5"><result status="valid" time="0.02" steps="111"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="113"/></proof>
</goal>
<goal name="WP_parameter binary_search.21" expl="21. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.02" steps="99"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="101"/></proof>
</goal>
<goal name="WP_parameter binary_search.22" expl="22. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="3.46"/></proof>
<proof prover="5"><result status="valid" time="1.35" steps="177"/></proof>
<proof prover="5"><result status="valid" time="1.35" steps="203"/></proof>
</goal>
<goal name="WP_parameter binary_search.23" expl="23. loop variant decrease">
<proof prover="5"><result status="valid" time="0.02" steps="99"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="101"/></proof>
</goal>
<goal name="WP_parameter binary_search.24" expl="24. postcondition">
<proof prover="5"><result status="valid" time="0.08" steps="123"/></proof>
<proof prover="5"><result status="valid" time="0.08" steps="137"/></proof>
</goal>
<goal name="WP_parameter binary_search.25" expl="25. exceptional postcondition">
<proof prover="5"><result status="valid" time="0.01" steps="88"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="90"/></proof>
</goal>
</transf>
</goal>
......
examples/bitcount.mlw
View file @ f0547868
......@@ -7,7 +7,7 @@ module BitCount8bit_fact
function nth_as_bv (a i : t) : t =
if nth_bv a i
then (of_int 1)
then (1 : t)
else zeros
function nth_as_int (a : t) (i : int) : int =
......@@ -16,81 +16,81 @@ module BitCount8bit_fact
else 0
lemma nth_as_bv_is_int : forall a i.
to_uint (nth_as_bv a i) = nth_as_int a (to_uint i)
t'int (nth_as_bv a i) = nth_as_int a (t'int i)
use import int.EuclideanDivision
let ghost step1 (n x1 : t) (i : int) : unit
requires { 0 <= i < 4 }
requires { x1 = sub n (bw_and (lsr_bv n (of_int 1)) (of_int 0x55)) }
ensures { to_uint (bw_and (lsr x1 (2*i)) (of_int 0x03))
requires { x1 = sub n (bw_and (lsr_bv n (1 : t)) (0x55 : t)) }
ensures { t'int (bw_and (lsr x1 (2*i)) (0x03 : t))
= numof (nth n) (2*i) (2*i + 2) }
ensures { ule (bw_and (lsr x1 (2*i)) (of_int 0x03)) (of_int 2) }
ensures { ule (bw_and (lsr x1 (2*i)) (0x03 : t)) (2 : t) }
=
assert { let i' = of_int i in
let twoi = mul (of_int 2) i' in
bw_and (lsr_bv x1 twoi) (of_int 0x03)
= add (nth_as_bv n twoi) (nth_as_bv n (add twoi (of_int 1)))
let twoi = mul (2 : t) i' in
bw_and (lsr_bv x1 twoi) (0x03 : t)
= add (nth_as_bv n twoi) (nth_as_bv n (add twoi (1 : t)))
&&
to_uint (bw_and (lsr_bv x1 twoi) (of_int 0x03))
= numof (nth n) (to_uint twoi) (to_uint twoi + 2) }
t'int (bw_and (lsr_bv x1 twoi) (0x03 : t))
= numof (nth n) (t'int twoi) (t'int twoi + 2) }
let ghost step2 (n x1 x2 : t) (i : int) : unit
requires { 0 <= i < 2 }
requires { x1 = sub n (bw_and (lsr_bv n (of_int 1)) (of_int 0x55)) }
requires { x1 = sub n (bw_and (lsr_bv n (1 : t)) (0x55 : t)) }
requires { x2 = add
(bw_and x1 (of_int 0x33))
(bw_and (lsr_bv x1 (of_int 2)) (of_int (0x33))) }
ensures { to_uint (bw_and (lsr x2 (4*i)) (of_int 0x0F))
(bw_and x1 (0x33 : t))
(bw_and (lsr_bv x1 (2 : t)) (0x33 : t)) }
ensures { t'int (bw_and (lsr x2 (4*i)) (0x0F : t))
= numof (nth n) (4*i) (4*i+4) }
ensures { ule (bw_and (lsr_bv x2 (of_int (4*i))) (of_int 0x0F))
(of_int 4) }
ensures { ule (bw_and (lsr_bv x2 (of_int (4*i))) (0x0F : t))
(4 : t) }
=
step1 n x1 (2*i);
step1 n x1 (2*i+1);
assert { let i' = of_int i in
ult i' (of_int 2)
ult i' (2 : t)
&&
of_int (4*i) = mul (of_int 4) i'
of_int (4*i) = mul (4 : t) i'
&&
to_uint (bw_and (lsr x2 (4*i)) (of_int 0x0F))
= to_uint (bw_and (lsr_bv x2 (mul (of_int 4) i')) (of_int 0x0F))
= to_uint (add (bw_and (lsr_bv x1 (mul (of_int 4) i')) (of_int 0x03))
(bw_and (lsr_bv x1 (add (mul (of_int 4) i') (of_int 2))) (of_int (0x03))))
= to_uint (add (bw_and (lsr x1 (4*i)) (of_int 0x03))
(bw_and (lsr x1 ((4*i)+2)) (of_int (0x03))))}
t'int (bw_and (lsr x2 (4*i)) (0x0F : t))
= t'int (bw_and (lsr_bv x2 (mul (4 : t) i')) (0x0F : t))
= t'int (add (bw_and (lsr_bv x1 (mul (4 : t) i')) (0x03 : t))
(bw_and (lsr_bv x1 (add (mul (4 : t) i') (2 : t))) (0x03 : t)))
= t'int (add (bw_and (lsr x1 (4*i)) (0x03 : t))
(bw_and (lsr x1 ((4*i)+2)) (0x03 : t)))}
let ghost prove (n x1 x2 x3 : t) : unit
requires { x1 = sub n (bw_and (lsr_bv n (of_int 1)) (of_int 0x55)) }
requires { x1 = sub n (bw_and (lsr_bv n (1 : t)) (0x55 : t)) }
requires { x2 = add
(bw_and x1 (of_int 0x33))
(bw_and (lsr_bv x1 (of_int 2)) (of_int (0x33))) }
requires { x3 = bw_and (add x2 (lsr_bv x2 (of_int 4))) (of_int 0x0F) }
ensures { to_uint x3 = numof (nth n) 0 8 }
(bw_and x1 (0x33 : t))
(bw_and (lsr_bv x1 (2 : t)) (0x33 : t)) }
requires { x3 = bw_and (add x2 (lsr_bv x2 (4 : t))) (0x0F : t) }
ensures { t'int x3 = numof (nth n) 0 8 }
=
step2 n x1 x2 0;
step2 n x1 x2 1;
assert { to_uint (bw_and x2 (of_int 0x0F)) +
to_uint (bw_and (lsr_bv x2 (of_int 4)) (of_int 0x0F))