Commit 6f012f7d authored by Clément Fumex's avatar Clément Fumex

- Update of logic/bitvectors.why test after the addition of converter in smt-libv2 driver

- Switch from AUFNIRA to AUFBVNIRA logic in cvc4_bare
parent 7487f2a1
prelude "(set-logic AUFNIRA)" (* how come bv is supported by cvc4 in this logic ?!? *)
prelude "(set-logic AUFBVNIRA)"
(** A : Array
UF : Uninterpreted Function
DT : Datatypes (not needed at the end ...)
......
(* Why driver for SMT v2 syntax for bit-vectors *)
(* Why driver for SMT-lib v2 syntax *)
prelude ";;; this is a prelude for smt-lib v2"
(*prelude "(set-logic AUFNIRA)"*)
......@@ -190,15 +190,7 @@ theory bv.BV32
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
(* syntax function to_uint "(bv2nat %1)" *)
(* syntax function to_int "(bv2int %1)" (* Z3 vb2nat *)*)
(* syntax function to_int "(ite (= ((_ extract 31 31) %1) #b0) *)
(* (bv2nat %1) *)
(* (- (bv2nat %1) 4294967296))" *)
(* syntax function of_int "((_ int2bv 32) %1)" *)
syntax converter of_int_const "((_ int2bv 32) %1)"
(* syntax function nth "(= ((_ extract 0 0) (bvlshr %1 ((_ int2bv 32) %2))) #b1)" *)
(* syntax function nth_bv "(= ((_ extract 0 0) (bvlshr %1 %2)) #b1)" *)
syntax predicate eq "(= %1 %2)"
remove prop Extensionality
......@@ -210,26 +202,6 @@ theory bv.BV32
syntax predicate ule "(bvule %1 %2)"
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
(* remove prop Nth_zero *)
(* remove prop Nth_ones *)
(* remove prop Nth_bw_and *)
(* remove prop Nth_bw_or *)
(* remove prop Nth_bw_xor *)
(* remove prop Nth_bw_not *)
(* remove prop Add_is_add *)
(* remove prop Min_is_min *)
(* remove prop Neg_is_neg *)
(* remove prop Mul_is_mul *)
(* remove prop Udiv_is_udiv *)
(* remove prop Lsr_nth_low *)
(* remove prop Lsr_nth_high *)
(* remove prop Lsl_nth_low *)
(* remove prop Lsl_nth_high *)
(* remove prop Asr_nth_low *)
(* remove prop Asr_nth_high *)
end
theory bv.BV32Ax
......@@ -261,14 +233,7 @@ theory bv.BV32Ax
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
(* syntax function to_uint "(bv2nat %1)" *)
(* syntax function to_int "(ite (= ((_ extract 31 31) %1) #b0) *)
(* (bv2nat %1) *)
(* (- (bv2nat %1) 4294967296))" *)
(* syntax function of_int "((_ int2bv 32) %1)" *)
syntax converter of_int_const "((_ int2bv 32) %1)"
(* syntax function nth "(= ((_ extract 0 0) (bvlshr %1 ((_ int2bv 32) %2))) #b1)" *)
(* syntax function nth_bv "(= ((_ extract 0 0) (bvlshr %1 %2)) #b1)" *)
syntax predicate eq "(= %1 %2)"
syntax predicate slt "(bvslt %1 %2)"
......@@ -280,25 +245,11 @@ theory bv.BV32Ax
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
(* remove prop Nth_zero *)
(* remove prop Nth_ones *)
(* remove prop Nth_bw_and *)
(* remove prop Nth_bw_or *)
(* remove prop Nth_bw_xor *)
(* remove prop Nth_bw_not *)
remove prop Add_is_add
remove prop Min_is_min
remove prop Neg_is_neg
remove prop Mul_is_mul
remove prop Udiv_is_udiv
(* remove prop Lsr_nth_low *)
(* remove prop Lsr_nth_high *)
(* remove prop Lsl_nth_low *)
(* remove prop Lsl_nth_high *)
(* remove prop Asr_nth_low *)
(* remove prop Asr_nth_high *)
end
theory bv.BV64
......
theory TestBV
use import int.Int
use import bv.BV32
constant b0000 : t = of_int 0b0000
constant b0001 : t = of_int 0b0001
constant b0010 : t = of_int 0b0010
constant b0011 : t = of_int 0b0011
constant b0110 : t = of_int 0b0110
constant b0101 : t = of_int 0b0101
constant b0111 : t = of_int 0b0111
constant b1100 : t = of_int 0b1100
constant b11100 : t = of_int 0b11100
constant b0000 : t = of_int_const 0b0000
constant b0001 : t = of_int_const 0b0001
constant b0010 : t = of_int_const 0b0010
constant b0011 : t = of_int_const 0b0011
constant b0110 : t = of_int_const 0b0110
constant b0101 : t = of_int_const 0b0101
constant b0111 : t = of_int_const 0b0111
constant b1100 : t = of_int_const 0b1100
constant b11100 : t = of_int_const 0b11100
goal g1 : bw_and b0011 b0110 = b0010
goal f1 : bw_and b0011 b0110 = b0011
......@@ -21,14 +20,14 @@ theory TestBV
goal f2 : bw_or b0011 b0110 = b0110
goal g3 : bw_xor b0011 b0110 = b0101
goal g4 : bw_not b0011 = (of_int 0xFFFFFFFC)
goal g4 : bw_not b0011 = (of_int_const 0xFFFFFFFC)
goal g3a : lsr b0111 2 = b0001
goal g3b : lsr ones 31 = b0001
goal g3c : lsr ones 0x100000001 = (of_int 0x7FFFFFFF)
goal g3c : lsr ones 0x100000001 = (of_int_const 0x7FFFFFFF)
goal g4a : lsl b0111 2 = b11100
goal g4b : lsl b0001 31 = (of_int 0x80000000)
goal g4b : lsl b0001 31 = (of_int_const 0x80000000)
goal g5a : asr b0111 2 = b0001
goal g5b : asr ones 31 = ones
......@@ -59,18 +58,17 @@ theory TestBV
forall v:t, n:int. 0 <= n < size ->
nth (bw_not v) n = notb (nth v n)
goal not_not : forall v:t. bw_not (bw_not v) = v
goal not_and : forall v1 v2:t.
bw_not (bw_and v1 v2) = bw_or (bw_not v1) (bw_not v2)
goal Lsr_nth_low:
forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s < size ->
forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s < size ->
nth (lsr b s) n = nth b (n+s)
goal Lsr_nth_high:
forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s >= size ->
forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s >= size ->
nth (lsr b s) n = False
goal Asr_nth_low:
......@@ -85,5 +83,4 @@ theory TestBV
goal Lsl_nth_low:
forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n-s < 0 -> nth (lsl b s) n = False
end
......@@ -2,95 +2,167 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="23" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="3" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="23" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../bitvectors.why" expanded="true">
<theory name="TestBV" sum="9c3a1e0f691b7f969589746c99343436" expanded="true">
<theory name="TestBV" sum="d318f02c83a7261b5dc501a4a7f36ac8" expanded="true">
<goal name="g1">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="timeout" time="4.81"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="f1" expanded="true">
<proof prover="0"><result status="timeout" time="4.98"/></proof>
<proof prover="2"><result status="timeout" time="4.91"/></proof>
<proof prover="3"><result status="timeout" time="4.97"/></proof>
</goal>
<goal name="g2">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="timeout" time="4.97"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="f2" expanded="true">
<proof prover="0"><result status="timeout" time="4.94"/></proof>
<proof prover="2"><result status="timeout" time="5.99"/></proof>
<proof prover="3"><result status="timeout" time="5.01"/></proof>
</goal>
<goal name="g3">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="timeout" time="4.98"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="g4">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="timeout" time="4.91"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="g3a">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="timeout" time="4.89"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="g3b">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="timeout" time="4.98"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="g3c">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="timeout" time="4.97"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="g4a">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="timeout" time="4.94"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="g4b">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="timeout" time="4.90"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="g5a">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="timeout" time="4.96"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="g5b">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="g6a">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="15"/></proof>
<proof prover="2"><result status="timeout" time="6.01"/></proof>
<proof prover="3"><result status="timeout" time="5.01"/></proof>
</goal>
<goal name="g6b">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="3"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="g7a">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="13"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="g7b" expanded="true">
<proof prover="1"><result status="timeout" time="4.00"/></proof>
<proof prover="0"><result status="timeout" time="4.76"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="g8a" expanded="true">
<proof prover="1"><result status="timeout" time="4.00"/></proof>
<proof prover="0"><result status="timeout" time="4.96"/></proof>
<proof prover="2"><result status="timeout" time="5.98"/></proof>
<proof prover="3"><result status="timeout" time="5.01"/></proof>
</goal>
<goal name="g8b" expanded="true">
<proof prover="1"><result status="timeout" time="4.00"/></proof>
<proof prover="0"><result status="timeout" time="4.98"/></proof>
<proof prover="2"><result status="timeout" time="5.98"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="Nth_bw_and">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="10"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Nth_bw_or">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="10"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Nth_bw_xor">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="10"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Nth_bw_not">
<proof prover="1" timelimit="5"><result status="valid" time="0.04"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="10"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="not_not">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="timeout" time="4.91"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="not_and">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="timeout" time="4.93"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Lsr_nth_low" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
<proof prover="2"><result status="timeout" time="5.98"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Lsr_nth_high" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="9"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="timeout" time="5.98"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Asr_nth_low" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Asr_nth_high" expanded="true">
<proof prover="0"><result status="valid" time="0.04" steps="13"/></proof>
<proof prover="2"><result status="timeout" time="5.99"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Lsl_nth_high" expanded="true">
<proof prover="0"><result status="valid" time="0.04" steps="13"/></proof>
<proof prover="2"><result status="timeout" time="5.99"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Lsl_nth_low" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="9"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
</file>
......
......@@ -38,7 +38,7 @@ theory BitVector
forall n:int. 0 <= n < size -> nth zero n = False
constant ones : t
axiom Nth_ones:
axiom Nth_ones:
forall n:int. 0 <= n < size -> nth ones n = True
function bw_and (v1 v2 : t) : t
......@@ -65,7 +65,7 @@ theory BitVector
(** rotate left *)
axiom Nth_rotate_left_high:
forall v:t, n:int.
forall v:t, n:int.
0 < n < size -> nth (rotate_left v) n = nth v (n - 1)
axiom Nth_rotate_left_low:
......@@ -87,11 +87,11 @@ theory BitVector
function lsr t int : t
axiom Lsr_nth_low:
forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s < size ->
forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s < size ->
nth (lsr b s) n = nth b (n+s)
axiom Lsr_nth_high:
forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s >= size ->
forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s >= size ->
nth (lsr b s) n = False
function lsr_bv t t : t
......@@ -147,10 +147,10 @@ theory BitVector
axiom of_int_is_mod:
forall i:int. to_uint( of_int i ) = mod i two_power_size
axiom of_int_extmod:
forall i,j:int. of_int i = of_int j ->
axiom of_int_extmod:
forall i,j:int. of_int i = of_int j ->
mod i two_power_size = mod j two_power_size
function of_int_const int : t
axiom of_int_const_to_int:
......@@ -161,19 +161,19 @@ theory BitVector
(* TODO? axioms related to_int/to_unit and of_int *)
(** addition modulo 2^m *)
(** addition modulo 2^m *)
function add (v1 v2 : t) : t
(** 2's complement subtraction modulo 2^m *)
function sub (v1 v2 : t) : t
(** 2's complement unary minus *)
function neg (v1 : t) : t
(** multiplication modulo 2^m *)
(** multiplication modulo 2^m *)
function mul (v1 v2 : t) : t
(** unsigned division, truncating towards 0 (undefined if divisor is 0) *)
(** unsigned division, truncating towards 0 (undefined if divisor is 0) *)
function udiv (v1 v2 : t) : t
(** unsigned remainder from truncating division (undefined if divisor is 0) *)
......@@ -258,7 +258,7 @@ theory BitVectorWithAxiom
forall n:int. 0 <= n < size -> nth zero n = False
constant ones : t
axiom Nth_ones:
axiom Nth_ones:
forall n:int. 0 <= n < size -> nth ones n = True
function bw_and (v1 v2 : t) : t
......@@ -285,7 +285,7 @@ theory BitVectorWithAxiom
(** rotate left *)
axiom Nth_rotate_left_high:
forall v:t, n:int.
forall v:t, n:int.
0 < n < size -> nth (rotate_left v) n = nth v (n - 1)
axiom Nth_rotate_left_low:
......@@ -307,11 +307,11 @@ theory BitVectorWithAxiom
function lsr t int : t
axiom Lsr_nth_low:
forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s < size ->
forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s < size ->
nth (lsr b s) n = nth b (n+s)
axiom Lsr_nth_high:
forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s >= size ->
forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s >= size ->
nth (lsr b s) n = False
function lsr_bv t t : t
......@@ -370,10 +370,10 @@ theory BitVectorWithAxiom
axiom of_int_is_mod:
forall i:int. to_uint( of_int i ) = mod i two_power_size
axiom of_int_extmod:
forall i,j:int. of_int i = of_int j ->
axiom of_int_extmod:
forall i,j:int. of_int i = of_int j ->
mod i two_power_size = mod j two_power_size
function of_int_const int : t
axiom of_int_const_to_int:
......@@ -387,27 +387,27 @@ theory BitVectorWithAxiom
(* TODO? axioms related to_int/to_unit and of_int *)
(** addition modulo 2^m *)
(** addition modulo 2^m *)
function add (v1 v2 : t) : t
axiom Add_is_add:
forall v1 v2:t. to_uint( add v1 v2 ) = mod( to_uint (v1) + to_uint (v2) ) two_power_size
(** 2's complement subtraction modulo 2^m *)
function sub (v1 v2 : t) : t
axiom Min_is_min:
forall v1 v2:t. to_uint( sub v1 v2 ) = mod( to_uint (v1) - to_uint (v2) ) two_power_size
(** 2's complement unary minus *)
function neg (v1 : t) : t
axiom Neg_is_neg:
forall v:t. to_uint( neg v ) = mod( -to_uint (v) ) two_power_size
(** multiplication modulo 2^m *)
(** multiplication modulo 2^m *)
function mul (v1 v2 : t) : t
axiom Mul_is_mul:
forall v1 v2:t. to_uint( mul v1 v2 ) = mod (to_uint (v1) * to_uint (v2) ) two_power_size
(** unsigned division, truncating towards 0 (undefined if divisor is 0) *)
(** unsigned division, truncating towards 0 (undefined if divisor is 0) *)
function udiv (v1 v2 : t) : t
axiom Udiv_is_udiv:
forall v1 v2:t. to_uint( udiv v1 v2 ) = div ( to_uint v1 ) ( to_uint v2 )
......@@ -464,10 +464,10 @@ end
theory BV32Ax
constant size: int = 32
constant two_power_size : int = 0x1_0000_0000
clone export BitVectorWithAxiom with
constant size = size,
constant two_power_size = two_power_size,
goal size_pos,
clone export BitVectorWithAxiom with
constant size = size,
constant two_power_size = two_power_size,
goal size_pos,
lemma val_two_power_size
end
......@@ -476,9 +476,9 @@ end
theory BV31
constant size: int = 31
constant two_power_size : int = 0x8000_0000
clone export BitVector with
constant size = size,
constant two_power_size = two_power_size,
clone export BitVector with
constant size = size,
constant two_power_size = two_power_size,
goal size_pos,
lemma val_two_power_size
end
......@@ -488,10 +488,10 @@ end
theory BV32
constant size: int = 32
constant two_power_size : int = 0x1_0000_0000
clone export BitVector with
constant size = size,
constant two_power_size = two_power_size,
goal size_pos,
clone export BitVector with
constant size = size,
constant two_power_size = two_power_size,
goal size_pos,
lemma val_two_power_size
end
......@@ -500,10 +500,10 @@ end
theory BV63
constant size: int = 63
constant two_power_size : int = 0x8000_0000_0000_0000
clone export BitVector with
constant size = size,
constant two_power_size = two_power_size,
goal size_pos,
clone export BitVector with
constant size = size,
constant two_power_size = two_power_size,
goal size_pos,
lemma val_two_power_size
end
......@@ -512,8 +512,8 @@ end
theory BV64
constant size: int = 64
constant two_power_size : int = 0x1_0000_0000_0000_0000
clone export BitVector with
constant size = size,
clone export BitVector with
constant size = size,
constant two_power_size = two_power_size,
goal size_pos,
lemma val_two_power_size
......@@ -524,10 +524,10 @@ end
theory BV8
constant size: int = 8
constant two_power_size : int = 0x100
clone export BitVector with
constant size = size,
constant two_power_size = two_power_size,
goal size_pos,
clone export BitVector with
constant size = size,
constant two_power_size = two_power_size,
goal size_pos,
lemma val_two_power_size
end
......@@ -536,10 +536,10 @@ end
theory BV16
constant size: int = 16
constant two_power_size : int = 0x1_0000
clone export BitVector with
constant size = size,
constant two_power_size = two_power_size,
goal size_pos,
clone export BitVector with
constant size = size,
constant two_power_size = two_power_size,
goal size_pos,
lemma val_two_power_size
end
......@@ -563,8 +563,8 @@ end
theory BVConverter_32_64
use BV32
use BV64
clone export BVConverter with
clone export BVConverter with
type bigBV = BV64.t,
type smallBV = BV32.t
end
......@@ -573,7 +573,7 @@ theory BVConverter_16_64
use BV16
use BV64
clone export BVConverter with
clone export BVConverter with
type bigBV = BV64.t,
type smallBV = BV16.t
end
......@@ -582,7 +582,7 @@ theory BVConverter_8_64
use BV8
use BV64
clone export BVConverter with
clone export BVConverter with
type bigBV = BV64.t,
type smallBV = BV8.t
end
......@@ -591,7 +591,7 @@ theory BVConverter_16_32
use BV16
use BV32
clone export BVConverter with
clone export BVConverter with
type bigBV = BV32.t,
type smallBV = BV16.t
end
......@@ -601,7 +601,7 @@ theory BVConverter_8_32
use BV8
use BV32
clone export BVConverter with
clone export BVConverter with
type bigBV = BV32.t,
type smallBV = BV8.t
end
......@@ -610,7 +610,7 @@ theory BVConverter_8_16
use BV8
use BV16
clone export BVConverter with
clone export BVConverter with
type bigBV = BV16.t,
type smallBV = BV8.t
end
\ No newline at end of file
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