Commit 52897571 authored by MARCHE Claude's avatar MARCHE Claude

Bit-vector: changes spec of rotations + updated sessions

parent a679c796
......@@ -44,8 +44,8 @@ theory bv.BV64
"(= ((_ extract 0 0) (bvlshr %1 %2)) (_ bv1 1))"
*)
syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ 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
......@@ -57,8 +57,8 @@ theory bv.BV32
syntax function nth_bv
"(not (= (bvand (bvlshr %1 %2) (_ bv1 32)) (_ bv0 32)))"
syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv32 32))) (bvshl %1 (bvsub (_ bv32 32) (bvurem %2 (_ 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
......@@ -70,8 +70,8 @@ theory bv.BV16
syntax function nth_bv
"(not (= (bvand (bvlshr %1 %2) (_ bv1 16)) (_ bv0 16)))"
syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv16 16))) (bvshl %1 (bvsub (_ bv16 16) (bvurem %2 (_ 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
......@@ -83,8 +83,8 @@ theory bv.BV8
syntax function nth_bv
"(not (= (bvand (bvlshr %1 %2) (_ bv1 8)) (_ bv0 8)))"
syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv8 8))) (bvlshr %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ 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)))))"
end
theory bv.BVConverter_Gen
......
This diff is collapsed.
......@@ -119,10 +119,10 @@ theory Hackers_delight
(* rotate en shift *)
goal RS_left: forall x.
bw_or (lsl_bv x (of_int 1)) (lsr_bv x (of_int 31)) = rotate_left x (of_int 1)
bw_or (lsl_bv x (of_int 1)) (lsr_bv x (of_int 31)) = rotate_left_bv x (of_int 1)
goal RS_right: forall x.
bw_or (lsr_bv x (of_int 1)) (lsl_bv x (of_int 31)) = rotate_right x (of_int 1)
bw_or (lsr_bv x (of_int 1)) (lsl_bv x (of_int 31)) = rotate_right_bv x (of_int 1)
(* bound propagation *)
......@@ -214,11 +214,11 @@ module Hackers_delight_mod
(* rotate en shift *)
let rs_left (x : t) =
ensures{ result = rotate_left x (of_int 1) }
ensures{ result = rotate_left_bv x (of_int 1) }
bw_or (lsl_bv x (of_int 1)) (lsr_bv x (of_int 31))
let rs_right (x : t) =
ensures{ result = rotate_right x (of_int 1) }
ensures{ result = rotate_right_bv x (of_int 1) }
bw_or (lsr_bv x (of_int 1)) (lsl_bv x (of_int 31))
(* bound propagation *)
......
......@@ -6,14 +6,14 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="5" memlimit="1000"/>
<file name="../bitvector_examples.mlw" expanded="true">
<theory name="Test_proofinuse" sum="363859681ea54f33f3a8380b4860c8be">
<theory name="Test_proofinuse" sum="cc40a339e91f8798e286caa7bb80a0e0">
<goal name="WP_parameter shift_is_div" expl="VC for shift_is_div">
<transf name="split_goal_wp">
<goal name="WP_parameter shift_is_div.1" expl="1. assertion">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter shift_is_div.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.66" steps="145"/></proof>
<proof prover="0"><result status="valid" time="0.66" steps="137"/></proof>
</goal>
<goal name="WP_parameter shift_is_div.3" expl="3. assertion">
<proof prover="2"><result status="valid" time="0.01"/></proof>
......@@ -33,7 +33,7 @@
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" sum="374bec757fbc16e0e581584872d8aae6">
<theory name="Hackers_delight" sum="79374fa0e16f15839d139d3dc19925ac">
<goal name="DM1">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -92,7 +92,7 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
<theory name="Hackers_delight_mod" sum="57c1cfa57dd348da4aab15bb9417d91e">
<theory name="Hackers_delight_mod" sum="a95ebf9a8bf11ace664e844cc233ea3a">
<goal name="WP_parameter dm1" expl="VC for dm1">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -154,7 +154,7 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
</theory>
<theory name="Test_imperial_violet" sum="398dfc680acac60dbe43c669d84771f1">
<theory name="Test_imperial_violet" sum="c2bb087b9b1f9714b1604e01d385f9fe">
<goal name="bv32_bounds_bv">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -174,7 +174,7 @@
<proof prover="4"><result status="valid" time="0.16"/></proof>
</goal>
</theory>
<theory name="Test_from_bitvector_example" sum="50affb819c6789444948a1502385352d">
<theory name="Test_from_bitvector_example" sum="a8178d2d670a7c2eb3ce6242edd99c0e">
<goal name="Test1">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
......
......@@ -349,10 +349,10 @@ module Hackers_delight
(** rotate vs shift (p.37)*)
lemma RS_left: forall x.
bw_or (lsl_bv x (of_int 1)) (lsr_bv x (of_int 31)) = rotate_left x one
bw_or (lsl_bv x (of_int 1)) (lsr_bv x (of_int 31)) = rotate_left_bv x one
lemma RS_right: forall x.
bw_or (lsr_bv x (of_int 1)) (lsl_bv x (of_int 31)) = rotate_right x one
bw_or (lsr_bv x (of_int 1)) (lsl_bv x (of_int 31)) = rotate_right_bv x one
(** {6 bound propagation (p.73)} *)
......
......@@ -9,15 +9,15 @@
<file name="../hackers-delight.mlw" expanded="true">
<theory name="Utils" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Utils_Spec" sum="a29d5df9ccd8df5209597453ff480d53" expanded="true">
<theory name="Utils_Spec" sum="1a4656700b43facbed02dc710dee707b" expanded="true">
<goal name="countZero">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="numOfZero">
<proof prover="0"><result status="valid" time="0.47" steps="241"/></proof>
<proof prover="0"><result status="valid" time="0.70" steps="241"/></proof>
</goal>
<goal name="countStep">
<proof prover="1"><result status="valid" time="4.95"/></proof>
<proof prover="1"><result status="valid" time="6.13"/></proof>
</goal>
<goal name="WP_parameter numof_shift" expl="VC for numof_shift">
<proof prover="1"><result status="valid" time="0.24"/></proof>
......@@ -28,7 +28,7 @@
<proof prover="0"><result status="valid" time="0.03" steps="76"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.2" expl="2. variant decrease">
<proof prover="0"><result status="valid" time="0.65" steps="282"/></proof>
<proof prover="0"><result status="valid" time="1.06" steps="282"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3" expl="3. assertion">
<transf name="split_goal_wp">
......@@ -36,18 +36,18 @@
<proof prover="0"><result status="valid" time="0.22" steps="150"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="2.60" steps="535"/></proof>
<proof prover="0"><result status="valid" time="3.97" steps="535"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.51" steps="162"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.4" expl="4. assertion">
<proof prover="5"><result status="valid" time="2.23"/></proof>
<proof prover="5"><result status="valid" time="4.30"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter countSpec_Aux.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.30"/></proof>
<proof prover="1"><result status="valid" time="0.51"/></proof>
</goal>
</transf>
</goal>
......@@ -76,7 +76,7 @@
<goal name="WP_parameter triangleInequalityInt" expl="VC for triangleInequalityInt">
<transf name="split_goal_wp">
<goal name="WP_parameter triangleInequalityInt.1" expl="1. assertion">
<proof prover="4"><result status="valid" time="2.26"/></proof>
<proof prover="4"><result status="valid" time="3.36"/></proof>
</goal>
<goal name="WP_parameter triangleInequalityInt.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="78"/></proof>
......@@ -84,15 +84,15 @@
</transf>
</goal>
<goal name="triangleInequality">
<proof prover="0"><result status="valid" time="4.65" steps="726"/></proof>
<proof prover="0"><result status="valid" time="5.87" steps="726"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" sum="d473e832977fd6e285755f138e96283d" expanded="true">
<theory name="Hackers_delight" sum="26cb4b8b52fdf2b9695b4739a03ceea8" expanded="true">
<goal name="WP_parameter ascii" expl="VC for ascii">
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="asciiProp">
<proof prover="1"><result status="valid" time="0.66"/></proof>
<proof prover="1"><result status="valid" time="1.16"/></proof>
</goal>
<goal name="iso">
<proof prover="1"><result status="valid" time="0.43"/></proof>
......@@ -101,13 +101,13 @@
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="nthGray">
<proof prover="0"><result status="valid" time="1.25" steps="544"/></proof>
<proof prover="0"><result status="valid" time="1.67" steps="542"/></proof>
</goal>
<goal name="lastNthGray">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="nthBinary">
<proof prover="1"><result status="valid" time="0.22"/></proof>
<proof prover="1"><result status="valid" time="0.35"/></proof>
</goal>
<goal name="evenOdd">
<proof prover="1"><result status="valid" time="0.14"/></proof>
......@@ -143,7 +143,7 @@
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="Ac">
<proof prover="0"><result status="valid" time="0.49" steps="319"/></proof>
<proof prover="0"><result status="valid" time="0.77" steps="319"/></proof>
</goal>
<goal name="Ad">
<proof prover="1"><result status="valid" time="0.06"/></proof>
......
This diff is collapsed.
This diff is collapsed.
......@@ -8,7 +8,7 @@
<prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
<file name="../bv.why" expanded="true">
<theory name="CheckBV64" sum="64018b237ceaeb1a893ee273ebc20a15" expanded="true">
<theory name="CheckBV64" sum="3667990497edb88e067efe68d8b0bb8b" expanded="true">
<goal name="ok_zero" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="68"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -175,7 +175,7 @@
</goal>
<goal name="smoke1" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1" timelimit="15"><result status="unknown" time="0.41"/></proof>
<proof prover="1" timelimit="15"><result status="unknown" time="0.59"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
......@@ -210,7 +210,7 @@
</goal>
<goal name="smoke6" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.75"/></proof>
<proof prover="1"><result status="unknown" time="0.98"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
......@@ -246,7 +246,7 @@
</goal>
<goal name="f2" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.73"/></proof>
<proof prover="1"><result status="unknown" time="1.17"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.01"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
......@@ -309,7 +309,7 @@
</goal>
<goal name="f7" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.34"/></proof>
<proof prover="1"><result status="unknown" time="0.64"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="4.99"/></proof>
......@@ -323,19 +323,19 @@
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Nth_Bv_bw_and" expanded="true">
<proof prover="0"><result status="valid" time="0.15" steps="174"/></proof>
<proof prover="0"><result status="valid" time="0.15" steps="164"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Nth_Bv_bw_or" expanded="true">
<proof prover="0"><result status="valid" time="0.18" steps="200"/></proof>
<proof prover="0"><result status="valid" time="0.18" steps="190"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Nth_Bv_bw_xor" expanded="true">
<proof prover="0"><result status="valid" time="0.24" steps="234"/></proof>
<proof prover="0"><result status="valid" time="0.54" steps="234"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
......@@ -385,7 +385,7 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="CheckBV32" sum="c176a9c5904bae80d8733c39fe4742a3" expanded="true">
<theory name="CheckBV32" sum="32c898047541b7dddb4509df1082a714" expanded="true">
<goal name="ok_zero" expanded="true">
<proof prover="0"><result status="valid" time="0.03" steps="68"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
......@@ -574,21 +574,21 @@
</goal>
<goal name="smoke4" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.39"/></proof>
<proof prover="1"><result status="unknown" time="0.68"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="smoke5" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.50"/></proof>
<proof prover="1"><result status="unknown" time="0.67"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.03"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="smoke6" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.76"/></proof>
<proof prover="1"><result status="unknown" time="0.98"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
<proof prover="4"><result status="timeout" time="4.99"/></proof>
......@@ -608,7 +608,7 @@
<proof prover="4"><result status="timeout" time="4.99"/></proof>
</goal>
</theory>
<theory name="CheckBV16" sum="5e30a4cf13ef35d7b16dc38ffc8739ea" expanded="true">
<theory name="CheckBV16" sum="48ef2f5bab124330528a2a0693742385" expanded="true">
<goal name="ok_zero" expanded="true">
<proof prover="0"><result status="valid" time="0.04" steps="68"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
......@@ -804,7 +804,7 @@
</goal>
<goal name="smoke5" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="unknown" time="0.52"/></proof>
<proof prover="1"><result status="unknown" time="0.78"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.01"/></proof>
<proof prover="4"><result status="timeout" time="4.99"/></proof>
......@@ -831,7 +831,7 @@
<proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
</theory>
<theory name="CheckBV8" sum="9bf444d55af69fbb2f117b386d7678a0" expanded="true">
<theory name="CheckBV8" sum="a92468f6e69e618390432ba249f6522a" expanded="true">
<goal name="ok_zero" expanded="true">
<proof prover="0"><result status="valid" time="0.04" steps="68"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
......@@ -1006,7 +1006,7 @@
</goal>
<goal name="smoke2" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.48"/></proof>
<proof prover="1"><result status="unknown" time="0.65"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.97"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
......@@ -1020,7 +1020,7 @@
</goal>
<goal name="smoke4" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.39"/></proof>
<proof prover="1"><result status="unknown" time="0.54"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
......
......@@ -59,8 +59,6 @@ driver = "drivers/cvc4_14.drv"
# cvc4 1.4 does not print steps used in --stats anyway
command = "%l/why3-cpulimit %T %m -s %e --tlimit-per=%t000 --lang=smt2 %f"
# CVC4 version 1.4, not using SMTLIB bitvectors
[ATP cvc4]
name = "CVC4"
......
......@@ -148,6 +148,15 @@ theory BV_Gen
forall v:t, n:int. 0 <= n < size ->
nth (bw_not v) n = notb (nth v n)
(** Shift operators *)
(** Warning: shift operators of an amount greater than or equal to
the size are specified here, in concordance with SMTLIB. This is
not necessarily the case in hardware, where the amount of the
shift might be taken modulo the size, eg. [lsr x 64] might be
equal to [x], whereas in this theory it is 0.
*)
function lsr t int : t
axiom Lsr_nth_low:
......@@ -184,9 +193,25 @@ theory BV_Gen
lemma lsl_zero: forall x. lsr x 0 = x
use import Pow2int
use import int.EuclideanDivision
function rotate_right t int : t
axiom Nth_rotate_right :
forall v n i. 0 <= i < size -> 0 <= n ->
nth (rotate_right v n) i = nth v (mod (i + n) size)
function rotate_left t int : t
axiom Nth_rotate_left :
forall v n i. 0 <= i < size -> 0 <= n ->
nth (rotate_left v n) i = nth v (mod (i - n) size)
(* Conversions from/to integers *)
use import Pow2int
constant two_power_size : int
constant max_int : int
......@@ -328,17 +353,16 @@ theory BV_Gen
forall v n : t.
to_uint (lsl_bv v n) = mod (Int.( * ) (to_uint v) (pow2 (to_uint n))) two_power_size
function rotate_right (v n : t) : t
function rotate_right_bv (v n : t) : t
function rotate_left (v n : t) : t
function rotate_left_bv (v n : t) : t
axiom Nth_rotate_left :
forall v n i. ult i size_bv -> ult n (sub ones size_bv) ->
nth_bv v i = nth_bv (rotate_left v n) (urem (add i n) size_bv)
axiom rotate_left_bv_is_rotate_left :
forall v n. rotate_left_bv v n = rotate_left v (to_uint n)
axiom rotate_right_bv_is_rotate_right :
forall v n. rotate_right_bv v n = rotate_right v (to_uint n)
axiom Nth_rotate_right :
forall v n i. ult i size_bv -> ult n (sub ones size_bv) ->
nth_bv (rotate_right v n) i = nth_bv v (urem (add i n) size_bv)
(* equality axioms *)
......
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