ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
why3/stdlib/bv.mlw

1062 lines
35 KiB
Plaintext
Raw Permalink Blame History

(** {1 Bit Vectors} *)
(** {2 Powers of two} *)
module Pow2int
use int.Int
function pow2 (i:int) : int
axiom Power_0 : pow2 0 = 1
meta "remove_unused:dependency" axiom Power_0, function pow2
axiom Power_s : forall n: int. n >= 0 -> pow2 (n+1) = 2 * pow2 n
meta "remove_unused:dependency" axiom Power_s, function pow2
lemma Power_1 : pow2 1 = 2
meta "remove_unused:dependency" lemma Power_1, function pow2
lemma Power_sum :
forall n m: int. n >= 0 /\ m >= 0 -> pow2 (n+m) = pow2 n * pow2 m
meta "remove_unused:dependency" lemma Power_sum, function pow2
lemma pow2pos: forall i:int. i >= 0 -> pow2 i > 0
meta "remove_unused:dependency" lemma pow2pos, function pow2
lemma pow2_0: pow2 0 = 0x1
lemma pow2_1: pow2 1 = 0x2
lemma pow2_2: pow2 2 = 0x4
lemma pow2_3: pow2 3 = 0x8
lemma pow2_4: pow2 4 = 0x10
lemma pow2_5: pow2 5 = 0x20
lemma pow2_6: pow2 6 = 0x40
lemma pow2_7: pow2 7 = 0x80
lemma pow2_8: pow2 8 = 0x100
lemma pow2_9: pow2 9 = 0x200
lemma pow2_10: pow2 10 = 0x400
lemma pow2_11: pow2 11 = 0x800
lemma pow2_12: pow2 12 = 0x1000
lemma pow2_13: pow2 13 = 0x2000
lemma pow2_14: pow2 14 = 0x4000
lemma pow2_15: pow2 15 = 0x8000
lemma pow2_16: pow2 16 = 0x10000
lemma pow2_17: pow2 17 = 0x20000
lemma pow2_18: pow2 18 = 0x40000
lemma pow2_19: pow2 19 = 0x80000
lemma pow2_20: pow2 20 = 0x100000
lemma pow2_21: pow2 21 = 0x200000
lemma pow2_22: pow2 22 = 0x400000
lemma pow2_23: pow2 23 = 0x800000
lemma pow2_24: pow2 24 = 0x1000000
lemma pow2_25: pow2 25 = 0x2000000
lemma pow2_26: pow2 26 = 0x4000000
lemma pow2_27: pow2 27 = 0x8000000
lemma pow2_28: pow2 28 = 0x10000000
lemma pow2_29: pow2 29 = 0x20000000
lemma pow2_30: pow2 30 = 0x40000000
lemma pow2_31: pow2 31 = 0x80000000
lemma pow2_32: pow2 32 = 0x100000000
lemma pow2_33: pow2 33 = 0x200000000
lemma pow2_34: pow2 34 = 0x400000000
lemma pow2_35: pow2 35 = 0x800000000
lemma pow2_36: pow2 36 = 0x1000000000
lemma pow2_37: pow2 37 = 0x2000000000
lemma pow2_38: pow2 38 = 0x4000000000
lemma pow2_39: pow2 39 = 0x8000000000
lemma pow2_40: pow2 40 = 0x10000000000
lemma pow2_41: pow2 41 = 0x20000000000
lemma pow2_42: pow2 42 = 0x40000000000
lemma pow2_43: pow2 43 = 0x80000000000
lemma pow2_44: pow2 44 = 0x100000000000
lemma pow2_45: pow2 45 = 0x200000000000
lemma pow2_46: pow2 46 = 0x400000000000
lemma pow2_47: pow2 47 = 0x800000000000
lemma pow2_48: pow2 48 = 0x1000000000000
lemma pow2_49: pow2 49 = 0x2000000000000
lemma pow2_50: pow2 50 = 0x4000000000000
lemma pow2_51: pow2 51 = 0x8000000000000
lemma pow2_52: pow2 52 = 0x10000000000000
lemma pow2_53: pow2 53 = 0x20000000000000
lemma pow2_54: pow2 54 = 0x40000000000000
lemma pow2_55: pow2 55 = 0x80000000000000
lemma pow2_56: pow2 56 = 0x100000000000000
lemma pow2_57: pow2 57 = 0x200000000000000
lemma pow2_58: pow2 58 = 0x400000000000000
lemma pow2_59: pow2 59 = 0x800000000000000
lemma pow2_60: pow2 60 = 0x1000000000000000
lemma pow2_61: pow2 61 = 0x2000000000000000
lemma pow2_62: pow2 62 = 0x4000000000000000
lemma pow2_63: pow2 63 = 0x8000000000000000
lemma pow2_64: pow2 64 = 0x10000000000000000
meta "remove_unused:dependency" lemma pow2_0, function pow2
meta "remove_unused:dependency" lemma pow2_1, function pow2
meta "remove_unused:dependency" lemma pow2_2, function pow2
meta "remove_unused:dependency" lemma pow2_3, function pow2
meta "remove_unused:dependency" lemma pow2_4, function pow2
meta "remove_unused:dependency" lemma pow2_5, function pow2
meta "remove_unused:dependency" lemma pow2_6, function pow2
meta "remove_unused:dependency" lemma pow2_7, function pow2
meta "remove_unused:dependency" lemma pow2_8, function pow2
meta "remove_unused:dependency" lemma pow2_9, function pow2
meta "remove_unused:dependency" lemma pow2_10, function pow2
meta "remove_unused:dependency" lemma pow2_11, function pow2
meta "remove_unused:dependency" lemma pow2_12, function pow2
meta "remove_unused:dependency" lemma pow2_13, function pow2
meta "remove_unused:dependency" lemma pow2_14, function pow2
meta "remove_unused:dependency" lemma pow2_15, function pow2
meta "remove_unused:dependency" lemma pow2_16, function pow2
meta "remove_unused:dependency" lemma pow2_17, function pow2
meta "remove_unused:dependency" lemma pow2_18, function pow2
meta "remove_unused:dependency" lemma pow2_19, function pow2
meta "remove_unused:dependency" lemma pow2_20, function pow2
meta "remove_unused:dependency" lemma pow2_21, function pow2
meta "remove_unused:dependency" lemma pow2_22, function pow2
meta "remove_unused:dependency" lemma pow2_23, function pow2
meta "remove_unused:dependency" lemma pow2_24, function pow2
meta "remove_unused:dependency" lemma pow2_25, function pow2
meta "remove_unused:dependency" lemma pow2_26, function pow2
meta "remove_unused:dependency" lemma pow2_27, function pow2
meta "remove_unused:dependency" lemma pow2_28, function pow2
meta "remove_unused:dependency" lemma pow2_29, function pow2
meta "remove_unused:dependency" lemma pow2_30, function pow2
meta "remove_unused:dependency" lemma pow2_31, function pow2
meta "remove_unused:dependency" lemma pow2_32, function pow2
meta "remove_unused:dependency" lemma pow2_33, function pow2
meta "remove_unused:dependency" lemma pow2_34, function pow2
meta "remove_unused:dependency" lemma pow2_35, function pow2
meta "remove_unused:dependency" lemma pow2_36, function pow2
meta "remove_unused:dependency" lemma pow2_37, function pow2
meta "remove_unused:dependency" lemma pow2_38, function pow2
meta "remove_unused:dependency" lemma pow2_39, function pow2
meta "remove_unused:dependency" lemma pow2_40, function pow2
meta "remove_unused:dependency" lemma pow2_41, function pow2
meta "remove_unused:dependency" lemma pow2_42, function pow2
meta "remove_unused:dependency" lemma pow2_43, function pow2
meta "remove_unused:dependency" lemma pow2_44, function pow2
meta "remove_unused:dependency" lemma pow2_45, function pow2
meta "remove_unused:dependency" lemma pow2_46, function pow2
meta "remove_unused:dependency" lemma pow2_47, function pow2
meta "remove_unused:dependency" lemma pow2_48, function pow2
meta "remove_unused:dependency" lemma pow2_49, function pow2
meta "remove_unused:dependency" lemma pow2_50, function pow2
meta "remove_unused:dependency" lemma pow2_51, function pow2
meta "remove_unused:dependency" lemma pow2_52, function pow2
meta "remove_unused:dependency" lemma pow2_53, function pow2
meta "remove_unused:dependency" lemma pow2_54, function pow2
meta "remove_unused:dependency" lemma pow2_55, function pow2
meta "remove_unused:dependency" lemma pow2_56, function pow2
meta "remove_unused:dependency" lemma pow2_57, function pow2
meta "remove_unused:dependency" lemma pow2_58, function pow2
meta "remove_unused:dependency" lemma pow2_59, function pow2
meta "remove_unused:dependency" lemma pow2_60, function pow2
meta "remove_unused:dependency" lemma pow2_61, function pow2
meta "remove_unused:dependency" lemma pow2_62, function pow2
meta "remove_unused:dependency" lemma pow2_63, function pow2
meta "remove_unused:dependency" lemma pow2_64, function pow2
(*** use int.EuclideanDivision
lemma Div_pow: forall x i:int.
i > 0 -> pow2 (i-1) <= x < pow2 i -> div x (pow2 (i-1)) = 1
lemma Div_div_pow: forall x i j:int.
i > 0 /\ j > 0 -> div (div x (pow2 i)) (pow2 j) = div x (pow2 (i+j))
lemma Mod_pow2_gen: forall x i k :int.
0 <= k < i -> mod (div (x + pow2 i) (pow2 k)) 2 = mod (div x (pow2 k)) 2
*)
end
(** {2 Generic theory of Bit Vectors (arbitrary length)} *)
module BV_Gen
use export bool.Bool
use int.Int
constant size : int
axiom size_pos : size > 0
type t
(** `nth b n` is the `n`-th bit of `b`. Bit 0 is
the least significant bit *)
val function nth t int : bool
axiom nth_out_of_bound: forall x n. n < 0 \/ n >= size -> nth x n = False
meta "remove_unused:dependency" axiom nth_out_of_bound, function nth
constant zeros : t
axiom Nth_zeros:
forall n:int. nth zeros n = False
meta "remove_unused:dependency" axiom Nth_zeros, function zeros
constant one : t
constant ones : t
axiom Nth_ones:
forall n. 0 <= n < size -> nth ones n = True
meta "remove_unused:dependency" axiom Nth_ones, function ones
(** Bitwise operators *)
(* /!\ NOTE : both bw_and and bw_or don't need guard on n because of
nth out of bound axiom *)
val function bw_and (v1 v2 : t) : t
axiom Nth_bw_and:
forall v1 v2:t, n:int. 0 <= n < size ->
nth (bw_and v1 v2) n = andb (nth v1 n) (nth v2 n)
meta "remove_unused:dependency" axiom Nth_bw_and, function bw_and
val function bw_or (v1 v2 : t) : t
axiom Nth_bw_or:
forall v1 v2:t, n:int. 0 <= n < size ->
nth (bw_or v1 v2) n = orb (nth v1 n) (nth v2 n)
meta "remove_unused:dependency" axiom Nth_bw_or, function bw_or
val function bw_xor (v1 v2 : t) : t
axiom Nth_bw_xor:
forall v1 v2:t, n:int. 0 <= n < size ->
nth (bw_xor v1 v2) n = xorb (nth v1 n) (nth v2 n)
meta "remove_unused:dependency" axiom Nth_bw_xor, function bw_xor
val function bw_not (v : t) : t
axiom Nth_bw_not:
forall v:t, n:int. 0 <= n < size ->
nth (bw_not v) n = notb (nth v n)
meta "remove_unused:dependency" axiom Nth_bw_not, function bw_not
(** 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.
*)
val function lsr t int : t
axiom Lsr_nth_low:
forall b:t,n s:int. 0 <= s -> 0 <= n -> n+s < size ->
nth (lsr b s) n = nth b (n+s)
meta "remove_unused:dependency" axiom Lsr_nth_low, function lsr
axiom Lsr_nth_high:
forall b:t,n s:int. 0 <= s -> 0 <= n -> n+s >= size ->
nth (lsr b s) n = False
meta "remove_unused:dependency" axiom Lsr_nth_high, function lsr
lemma lsr_zeros: forall x. lsr x 0 = x
meta "remove_unused:dependency" lemma lsr_zeros, function lsr
val function asr t int : t
axiom Asr_nth_low:
forall b:t,n s:int. 0 <= s -> 0 <= n < size -> n+s < size ->
nth (asr b s) n = nth b (n+s)
meta "remove_unused:dependency" axiom Asr_nth_low, function asr
axiom Asr_nth_high:
forall b:t,n s:int. 0 <= s -> 0 <= n < size -> n+s >= size ->
nth (asr b s) n = nth b (size-1)
meta "remove_unused:dependency" axiom Asr_nth_high, function asr
lemma asr_zeros: forall x. asr x 0 = x
meta "remove_unused:dependency" lemma asr_zeros, function asr
val function lsl t int : t
axiom Lsl_nth_high:
forall b:t,n s:int. 0 <= s <= n < size ->
nth (lsl b s) n = nth b (n-s)
meta "remove_unused:dependency" axiom Lsl_nth_high, function lsl
axiom Lsl_nth_low:
forall b:t,n s:int. 0 <= n < s ->
nth (lsl b s) n = False
meta "remove_unused:dependency" axiom Lsl_nth_low, function lsl
lemma lsl_zeros: forall x. lsl x 0 = x
meta "remove_unused:dependency" lemma lsl_zeros, function lsl
use int.EuclideanDivision
use int.ComputerDivision as CD
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)
meta "remove_unused:dependency" axiom Nth_rotate_right, function rotate_right
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)
meta "remove_unused:dependency" axiom Nth_rotate_left, function rotate_left
(** Conversions from/to integers *)
use Pow2int
constant two_power_size : int
constant two_power_size_minus_one : int
constant max_int : int
axiom two_power_size_val : two_power_size = pow2 size
axiom two_power_size_minus_one_val : two_power_size_minus_one = pow2 (size-1)
axiom max_int_val : max_int = two_power_size - 1
predicate is_signed_positive t
function to_uint t : int
val to_uint (x:t) : int ensures { result = to_uint x }
val function of_int [@rewrite:of_int] int : t
function to_int (x:t) : int =
if (is_signed_positive x) then (to_uint x) else (- (two_power_size - (to_uint x)))
val to_int (x:t) : int ensures { result = to_int x }
axiom to_uint_extensionality :
forall v,v':t. to_uint v = to_uint v' -> v = v'
meta "remove_unused:dependency" axiom to_uint_extensionality, function to_uint
axiom to_int_extensionality:
forall v,v':t. to_int v = to_int v' -> v = v'
meta "remove_unused:dependency" axiom to_int_extensionality, function to_int
(* *)
predicate uint_in_range (i : int) = (Int.(<=) 0 i) /\ (Int.(<=) i max_int)
(* *)
axiom to_uint_bounds :
(*
forall v:t. uint_in_range (to_uint v)
*)
forall v:t. 0 <= to_uint v < two_power_size
meta "remove_unused:dependency" axiom to_uint_bounds, function to_uint
axiom to_uint_of_int :
forall i. 0 <= i < two_power_size -> to_uint (of_int i) = i
meta "remove_unused:dependency" axiom to_uint_of_int, function to_uint
meta "remove_unused:dependency" axiom to_uint_of_int, function of_int
axiom to_int_bounds :
forall v:t. - two_power_size_minus_one <= to_int v < two_power_size_minus_one
meta "remove_unused:dependency" axiom to_int_bounds, function to_int
axiom to_int_of_int :
forall i. - two_power_size_minus_one <= i < two_power_size_minus_one -> to_int (of_int i) = i
meta "remove_unused:dependency" axiom to_int_of_int, function of_int
constant size_bv : t
axiom to_uint_size_bv : to_uint size_bv = size
axiom to_uint_zeros : to_uint zeros = 0
axiom to_uint_one : to_uint one = 1
axiom to_uint_ones : to_uint ones = max_int
(** comparison operators *)
use export why3.WellFounded.WellFounded
let predicate ult (x y : t) =
Int.(<) (to_uint x) (to_uint y)
(* note : the following must be a lemma so that it is cloned in the instances *)
lemma ult_wf : well_founded ult
meta "vc:proved_wf" predicate ult, lemma ult_wf
meta "remove_unused:dependency" lemma ult_wf, predicate ult
let predicate ule (x y : t) =
Int.(<=) (to_uint x) (to_uint y)
let predicate ugt (x y : t) =
Int.(>) (to_uint x) (to_uint y)
lemma ugt_wf : well_founded ugt
meta "vc:proved_wf" predicate ugt, lemma ugt_wf
meta "remove_unused:dependency" lemma ugt_wf, predicate ugt
let predicate uge (x y : t) =
Int.(>=) (to_uint x) (to_uint y)
let predicate slt (v1 v2 : t) =
Int.(<) (to_int v1) (to_int v2)
lemma slt_wf : well_founded slt
meta "vc:proved_wf" predicate slt, lemma slt_wf
meta "remove_unused:dependency" lemma slt_wf, predicate slt
let predicate sle (v1 v2 : t) =
Int.(<=) (to_int v1) (to_int v2)
let predicate sgt (v1 v2 : t) =
Int.(>) (to_int v1) (to_int v2)
lemma sgt_wf : well_founded sgt
meta "vc:proved_wf" predicate sgt, lemma sgt_wf
meta "remove_unused:dependency" lemma sgt_wf, predicate sgt
let predicate sge (v1 v2 : t) =
Int.(>=) (to_int v1) (to_int v2)
axiom positive_is_ge_zeros:
forall x. is_signed_positive x <-> sge x zeros
meta "remove_unused:dependency" axiom positive_is_ge_zeros, predicate sge
meta "remove_unused:dependency" axiom positive_is_ge_zeros, predicate is_signed_positive
(** Arithmetic operators *)
val function add (v1 v2 : t) : t
axiom to_uint_add:
forall v1 v2. to_uint (add v1 v2) = mod (Int.(+) (to_uint v1) (to_uint v2)) two_power_size
meta "remove_unused:dependency" axiom to_uint_add, function add
lemma to_uint_add_bounded:
forall v1 v2.
to_uint v1 + to_uint v2 < two_power_size ->
to_uint (add v1 v2) = to_uint v1 + to_uint v2
meta "remove_unused:dependency" lemma to_uint_add_bounded, function add
lemma to_uint_add_overflow:
forall v1 v2.
to_uint v1 + to_uint v2 >= two_power_size ->
to_uint (add v1 v2) = to_uint v1 + to_uint v2 - two_power_size
meta "remove_unused:dependency" lemma to_uint_add_overflow, function add
val function sub (v1 v2 : t) : t
axiom to_uint_sub:
forall v1 v2. to_uint (sub v1 v2) = mod (Int.(-) (to_uint v1) (to_uint v2)) two_power_size
meta "remove_unused:dependency" axiom to_uint_sub , function sub
lemma to_uint_sub_bounded:
forall v1 v2.
0 <= to_uint v1 - to_uint v2 ->
to_uint (sub v1 v2) = to_uint v1 - to_uint v2
meta "remove_unused:dependency" lemma to_uint_sub_bounded, function sub
lemma to_uint_sub_overflow:
forall v1 v2.
0 > to_uint v1 - to_uint v2 ->
to_uint (sub v1 v2) = to_uint v1 - to_uint v2 + two_power_size
meta "remove_unused:dependency" lemma to_uint_sub_overflow, function sub
val function neg (v1 : t) : t
axiom to_uint_neg:
forall v. to_uint (neg v) = mod (Int.(-_) (to_uint v)) two_power_size
meta "remove_unused:dependency" axiom to_uint_neg, function neg
lemma to_uint_neg_no_mod:
forall v. to_uint (neg v) =
if v = zeros then 0 else two_power_size - to_uint v
meta "remove_unused:dependency" lemma to_uint_neg_no_mod, function neg
val function mul (v1 v2 : t) : t
axiom to_uint_mul:
forall v1 v2. to_uint (mul v1 v2) = mod (Int.( * ) (to_uint v1) (to_uint v2)) two_power_size
meta "remove_unused:dependency" axiom to_uint_mul, function mul
lemma to_uint_mul_bounded:
forall v1 v2.
to_uint v1 * to_uint v2 < two_power_size ->
to_uint (mul v1 v2) = to_uint v1 * to_uint v2
meta "remove_unused:dependency" lemma to_uint_mul_bounded, function mul
val function udiv (v1 v2 : t) : t
axiom to_uint_udiv:
forall v1 v2. to_uint (udiv v1 v2) = div (to_uint v1) (to_uint v2)
meta "remove_unused:dependency" axiom to_uint_udiv, function udiv
val function urem (v1 v2 : t) : t
axiom to_uint_urem:
forall v1 v2. to_uint (urem v1 v2) = mod (to_uint v1) (to_uint v2)
meta "remove_unused:dependency" axiom to_uint_urem, function urem
val function sdiv (v1 v2 : t) : t
axiom to_int_sdiv:
forall v1 v2. to_int (sdiv v1 v2) = CD.mod (CD.div (to_int v1) (to_int v2)) two_power_size
meta "remove_unused:dependency" axiom to_int_sdiv, function sdiv
axiom to_int_sdiv_bounded:
forall v1 v2.
v1 <> (lsl one (size-1)) \/ v2 <> ones ->
to_int (sdiv v1 v2) = CD.div (to_int v1) (to_int v2)
meta "remove_unused:dependency" axiom to_int_sdiv_bounded, function sdiv
val function srem (v1 v2 : t) : t
axiom to_int_srem:
forall v1 v2. to_int (srem v1 v2) = CD.mod (to_int v1) (to_int v2)
meta "remove_unused:dependency" axiom to_int_srem, function srem
(** Bitvector alternatives for shifts, rotations and nth *)
(** logical shift right *)
val function lsr_bv t t : t
axiom lsr_bv_is_lsr:
forall x n.
lsr_bv x n = lsr x (to_uint n)
meta "remove_unused:dependency" axiom lsr_bv_is_lsr, function lsr_bv
axiom to_uint_lsr:
forall v n : t.
to_uint (lsr_bv v n) = div (to_uint v) (pow2 ( to_uint n ))
meta "remove_unused:dependency" axiom to_uint_lsr, function lsr_bv
(** arithmetic shift right *)
val function asr_bv t t : t
axiom asr_bv_is_asr:
forall x n.
asr_bv x n = asr x (to_uint n)
meta "remove_unused:dependency" axiom asr_bv_is_asr, function asr_bv
(** logical shift left *)
val function lsl_bv t t : t
axiom lsl_bv_is_lsl:
forall x n.
lsl_bv x n = lsl x (to_uint n)
meta "remove_unused:dependency" axiom lsl_bv_is_lsl, function lsl_bv
axiom to_uint_lsl:
forall v n : t.
to_uint (lsl_bv v n) = mod (Int.( * ) (to_uint v) (pow2 (to_uint n))) two_power_size
meta "remove_unused:dependency" axiom to_uint_lsl, function lsl_bv
(** rotations *)
val function rotate_right_bv (v n : t) : t
val function rotate_left_bv (v n : t) : t
axiom rotate_left_bv_is_rotate_left :
forall v n. rotate_left_bv v n = rotate_left v (to_uint n)
meta "remove_unused:dependency" axiom rotate_left_bv_is_rotate_left, function rotate_left_bv
meta "remove_unused:dependency" axiom rotate_left_bv_is_rotate_left, function rotate_left
axiom rotate_right_bv_is_rotate_right :
forall v n. rotate_right_bv v n = rotate_right v (to_uint n)
meta "remove_unused:dependency" axiom rotate_right_bv_is_rotate_right, function rotate_right_bv
meta "remove_unused:dependency" axiom rotate_right_bv_is_rotate_right, function rotate_right
val function nth_bv t t: bool
axiom nth_bv_def:
forall x i.
nth_bv x i = not (bw_and (lsr_bv x i) one = zeros)
meta "remove_unused:dependency" axiom nth_bv_def, function nth_bv
axiom Nth_bv_is_nth:
forall x i.
nth x (to_uint i) = nth_bv x i
meta "remove_unused:dependency" axiom Nth_bv_is_nth, function nth_bv
meta "remove_unused:dependency" axiom Nth_bv_is_nth, function nth
axiom Nth_bv_is_nth2:
forall x i. 0 <= i < two_power_size ->
nth_bv x (of_int i) = nth x i
meta "remove_unused:dependency" axiom Nth_bv_is_nth2, function nth_bv
meta "remove_unused:dependency" axiom Nth_bv_is_nth2, function nth
(** equality axioms *)
predicate eq_sub_bv t t t t
axiom eq_sub_bv_def: forall a b i n.
let mask = lsl_bv (sub (lsl_bv one n) one) i in
eq_sub_bv a b i n = (bw_and b mask = bw_and a mask)
meta "remove_unused:dependency" axiom eq_sub_bv_def, predicate eq_sub_bv
predicate eq_sub (a b:t) (i n:int) =
forall j. i <= j < i + n -> nth a j = nth b j
axiom eq_sub_equiv: forall a b i n:t.
eq_sub a b (to_uint i) (to_uint n)
<-> eq_sub_bv a b i n
meta "remove_unused:dependency" axiom eq_sub_equiv, predicate eq_sub_bv
meta "remove_unused:dependency" axiom eq_sub_equiv, predicate eq_sub
predicate (==) (v1 v2 : t) =
eq_sub v1 v2 0 size
axiom Extensionality [@W:non_conservative_extension:N] :
forall x y : t [x == y]. x == y -> x = y
meta "remove_unused:dependency" axiom Extensionality, predicate (==)
(* not a good idea to apply extensionality systematically here, since provers with built-in bitvectors will prefer using `=` directly
this meta could be added in drivers though.
meta extensionality predicate (==)
*)
val eq (v1 v2 : t) : bool
ensures { result <-> v1 = v2 }
end
(** {2 Bit Vectors of common sizes, 8/16/32/64/128/256} *)
module BV256
constant size : int = 256
constant two_power_size : int =
0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000
constant two_power_size_minus_one : int =
0x8000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000
use int.Int as Int (* needed to use range types *)
type t = < range 0 0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF >
constant zeros : t = 0x0
constant one : t = 0x1
constant ones : t = 0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF
clone export BV_Gen with
type t = t,
function to_uint = t'int,
constant size = size,
constant two_power_size = two_power_size,
constant two_power_size_minus_one = two_power_size_minus_one,
constant max_int = t'maxInt,
constant zeros = zeros,
constant one,
constant ones,
goal size_pos,
goal two_power_size_val,
goal two_power_size_minus_one_val,
goal max_int_val,
axiom . (* should this be "lemma"? "goal"? *)
end
module BV128
constant size : int = 128
constant two_power_size : int =
0x1_0000_0000_0000_0000_0000_0000_0000_0000
constant two_power_size_minus_one : int =
0x8000_0000_0000_0000_0000_0000_0000_0000
use int.Int as Int (* needed to use range types *)
type t = < range 0 0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF >
constant zeros : t = 0x0
constant one : t = 0x1
constant ones : t = 0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF
clone export BV_Gen with
type t = t,
function to_uint = t'int,
constant size = size,
constant two_power_size = two_power_size,
constant two_power_size_minus_one = two_power_size_minus_one,
constant max_int = t'maxInt,
constant zeros,
constant one,
constant ones,
goal size_pos,
goal two_power_size_val,
goal two_power_size_minus_one_val,
goal max_int_val,
axiom . (* should this be "lemma"? "goal"? *)
end
module BV64
constant size : int = 64
constant two_power_size : int = 0x1_0000_0000_0000_0000
constant two_power_size_minus_one : int = 0x8000_0000_0000_0000
use int.Int as Int (* needed to use range types *)
type t = < range 0 0xFFFF_FFFF_FFFF_FFFF >
constant zeros : t = 0x0
constant one : t = 0x1
constant ones : t = 0xFFFF_FFFF_FFFF_FFFF
clone export BV_Gen with
type t = t,
function to_uint = t'int,
constant size = size,
constant two_power_size = two_power_size,
constant two_power_size_minus_one = two_power_size_minus_one,
constant max_int = t'maxInt,
constant zeros,
constant one,
constant ones,
goal size_pos,
goal two_power_size_val,
goal two_power_size_minus_one_val,
goal max_int_val,
axiom . (* should this be "lemma"? "goal"? *)
end
module BV32
constant size : int = 32
constant two_power_size : int = 0x1_0000_0000
constant two_power_size_minus_one : int = 0x8000_0000
use int.Int as Int (* needed to use range types *)
type t = < range 0 0xFFFF_FFFF >
constant zeros : t = 0x0
constant one : t = 0x1
constant ones : t = 0xFFFF_FFFF
clone export BV_Gen with
type t = t,
function to_uint = t'int,
constant size = size,
constant two_power_size = two_power_size,
constant two_power_size_minus_one = two_power_size_minus_one,
constant max_int = t'maxInt,
constant zeros,
constant one,
constant ones,
goal size_pos,
goal two_power_size_val,
goal two_power_size_minus_one_val,
goal max_int_val,
axiom . (* should this be "lemma"? "goal"? *)
end
module BV16
constant size : int = 16
constant two_power_size : int = 0x1_0000
constant two_power_size_minus_one : int = 0x8000
use int.Int as Int (* needed to use range types *)
type t = < range 0 0xFFFF >
constant zeros : t = 0x0
constant one : t = 0x1
constant ones : t = 0xFFFF
clone export BV_Gen with
type t = t,
function to_uint = t'int,
constant size = size,
constant two_power_size = two_power_size,
constant two_power_size_minus_one = two_power_size_minus_one,
constant max_int = t'maxInt,
constant zeros,
constant one,
constant ones,
goal size_pos,
goal two_power_size_val,
goal two_power_size_minus_one_val,
goal max_int_val,
axiom . (* should this be "lemma"? "goal"? *)
end
module BV8
constant size : int = 8
constant two_power_size : int = 0x1_00
constant two_power_size_minus_one : int = 0x80
use int.Int as Int (* needed to use range types *)
type t = < range 0 0xFF >
constant zeros : t = 0x0
constant one : t = 0x1
constant ones : t = 0xFF
clone export BV_Gen with
type t = t,
function to_uint = t'int,
constant size = size,
constant two_power_size = two_power_size,
constant two_power_size_minus_one = two_power_size_minus_one,
constant max_int = t'maxInt,
constant zeros,
constant one,
constant ones,
goal size_pos,
goal two_power_size_val,
goal two_power_size_minus_one_val,
goal max_int_val,
axiom . (* should this be "lemma"? "goal"? *)
end
(** {2 Generic Converter} *)
module BVConverter_Gen
type bigBV
type smallBV
predicate in_small_range bigBV
function to_uint_small smallBV : int
function to_uint_big bigBV : int
val function toBig smallBV : bigBV (* unsigned, that is "zero extend" *)
val function stoBig smallBV : bigBV (* signed, that is "sign extend" *)
val function toSmall bigBV : smallBV
axiom toSmall_to_uint :
forall x:bigBV. in_small_range x ->
to_uint_big x = to_uint_small (toSmall x)
axiom toBig_to_uint :
forall x:smallBV.
to_uint_small x = to_uint_big (toBig x)
(* TODO: specify stoBig by axioms too *)
end
(** {3 Converters of common size_bvs} *)
module BVConverter_128_256
use BV128 as BV128
use BV256 as BV256
predicate in_range (b : BV256.t) = BV256.ule b (0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF:BV256.t)
clone export BVConverter_Gen with
type bigBV = BV256.t,
type smallBV = BV128.t,
predicate in_small_range = in_range,
function to_uint_small = BV128.t'int,
function to_uint_big = BV256.t'int,
axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
axiom toBig_to_uint (* TODO: "lemma"? "goal"? *)
end
module BVConverter_64_256
use BV64 as BV64
use BV256 as BV256
predicate in_range (b : BV256.t) = BV256.ule b (0xFFFF_FFFF_FFFF_FFFF:BV256.t)
clone export BVConverter_Gen with
type bigBV = BV256.t,
type smallBV = BV64.t,
predicate in_small_range = in_range,
function to_uint_small = BV64.t'int,
function to_uint_big = BV256.t'int,
axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
axiom toBig_to_uint (* TODO: "lemma"? "goal"? *)
end
module BVConverter_32_256
use BV32 as BV32
use BV256 as BV256
predicate in_range (b : BV256.t) = BV256.ule b (0xFFFF_FFFF:BV256.t)
clone export BVConverter_Gen with
type bigBV = BV256.t,
type smallBV = BV32.t,
predicate in_small_range = in_range,
function to_uint_small = BV32.t'int,
function to_uint_big = BV256.t'int,
axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
axiom toBig_to_uint (* TODO: "lemma"? "goal"? *)
end
module BVConverter_16_256
use BV16 as BV16
use BV256 as BV256
predicate in_range (b : BV256.t) = BV256.ule b (0xFFFF:BV256.t)
clone export BVConverter_Gen with
type bigBV = BV256.t,
type smallBV = BV16.t,
predicate in_small_range = in_range,
function to_uint_small = BV16.t'int,
function to_uint_big = BV256.t'int,
axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
axiom toBig_to_uint (* TODO: "lemma"? "goal"? *)
end
module BVConverter_8_256
use BV8 as BV8
use BV256 as BV256
predicate in_range (b : BV256.t) = BV256.ule b (0xFF:BV256.t)
clone export BVConverter_Gen with
type bigBV = BV256.t,
type smallBV = BV8.t,
predicate in_small_range = in_range,
function to_uint_small = BV8.t'int,
function to_uint_big = BV256.t'int,
axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
axiom toBig_to_uint (* TODO: "lemma"? "goal"? *)
end
module BVConverter_64_128
use BV64 as BV64
use BV128 as BV128
predicate in_range (b : BV128.t) = BV128.ule b (0xFFFF_FFFF_FFFF_FFFF:BV128.t)
clone export BVConverter_Gen with
type bigBV = BV128.t,
type smallBV = BV64.t,
predicate in_small_range = in_range,
function to_uint_small = BV64.t'int,
function to_uint_big = BV128.t'int,
axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
axiom toBig_to_uint (* TODO: "lemma"? "goal"? *)
end
module BVConverter_32_128
use BV32 as BV32
use BV128 as BV128
predicate in_range (b : BV128.t) = BV128.ule b (0xFFFF_FFFF:BV128.t)
clone export BVConverter_Gen with
type bigBV = BV128.t,
type smallBV = BV32.t,
predicate in_small_range = in_range,
function to_uint_small = BV32.t'int,
function to_uint_big = BV128.t'int,
axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
axiom toBig_to_uint (* TODO: "lemma"? "goal"? *)
end
module BVConverter_16_128
use BV16 as BV16
use BV128 as BV128
predicate in_range (b : BV128.t) = BV128.ule b (0xFFFF:BV128.t)
clone export BVConverter_Gen with
type bigBV = BV128.t,
type smallBV = BV16.t,
predicate in_small_range = in_range,
function to_uint_small = BV16.t'int,
function to_uint_big = BV128.t'int,
axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
axiom toBig_to_uint (* TODO: "lemma"? "goal"? *)
end
module BVConverter_8_128
use BV8 as BV8
use BV128 as BV128
predicate in_range (b : BV128.t) = BV128.ule b (0xFF:BV128.t)
clone export BVConverter_Gen with
type bigBV = BV128.t,
type smallBV = BV8.t,
predicate in_small_range = in_range,
function to_uint_small = BV8.t'int,
function to_uint_big = BV128.t'int,
axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
axiom toBig_to_uint (* TODO: "lemma"? "goal"? *)
end
module BVConverter_32_64
use BV32 as BV32
use BV64 as BV64
predicate in_range (b : BV64.t) = BV64.ule b (0xFFFF_FFFF:BV64.t)
clone export BVConverter_Gen with
type bigBV = BV64.t,
type smallBV = BV32.t,
predicate in_small_range = in_range,
function to_uint_small = BV32.t'int,
function to_uint_big = BV64.t'int,
axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
axiom toBig_to_uint (* TODO: "lemma"? "goal"? *)
end
module BVConverter_16_64
use BV16 as BV16
use BV64 as BV64
predicate in_range (b : BV64.t) = BV64.ule b (0xFFFF:BV64.t)
clone export BVConverter_Gen with
type bigBV = BV64.t,
type smallBV = BV16.t,
predicate in_small_range = in_range,
function to_uint_small = BV16.t'int,
function to_uint_big = BV64.t'int,
axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
axiom toBig_to_uint (* TODO: "lemma"? "goal"? *)
end
module BVConverter_8_64
use BV8 as BV8
use BV64 as BV64
predicate in_range (b : BV64.t) = BV64.ule b (0xFF:BV64.t)
clone export BVConverter_Gen with
type bigBV = BV64.t,
type smallBV = BV8.t,
predicate in_small_range = in_range,
function to_uint_small = BV8.t'int,
function to_uint_big = BV64.t'int,
axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
axiom toBig_to_uint (* TODO: "lemma"? "goal"? *)
end
module BVConverter_16_32
use BV16 as BV16
use BV32 as BV32
predicate in_range (b : BV32.t) = BV32.ule b (0xFFFF:BV32.t)
clone export BVConverter_Gen with
type bigBV = BV32.t,
type smallBV = BV16.t,
predicate in_small_range = in_range,
function to_uint_small = BV16.t'int,
function to_uint_big = BV32.t'int,
axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
axiom toBig_to_uint (* TODO: "lemma"? "goal"? *)
end
module BVConverter_8_32
use BV8 as BV8
use BV32 as BV32
predicate in_range (b : BV32.t) = BV32.ule b (0xFF:BV32.t)
clone export BVConverter_Gen with
type bigBV = BV32.t,
type smallBV = BV8.t,
predicate in_small_range = in_range,
function to_uint_small = BV8.t'int,
function to_uint_big = BV32.t'int,
axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
axiom toBig_to_uint (* TODO: "lemma"? "goal"? *)
end
module BVConverter_8_16
use BV8 as BV8
use BV16 as BV16
predicate in_range (b : BV16.t) = BV16.ule b (0xFF:BV16.t)
clone export BVConverter_Gen with
type bigBV = BV16.t,
type smallBV = BV8.t,
predicate in_small_range = in_range,
function to_uint_small = BV8.t'int,
function to_uint_big = BV16.t'int,
axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
axiom toBig_to_uint (* TODO: "lemma"? "goal"? *)
end
Reference in New Issue View Git Blame Copy Permalink