why3/examples/bitvector_examples.mlw

module Test_proofinuse

  use int.Int
  use int.Power
  use int.EuclideanDivision
  use bv.BV32

  (* Shift is div example -------------------  *)

  let shift_is_div ( x : t ) ( y : t ) : t
    requires { 0 <= t'int y < 32 }
  =
    let res = lsr_bv x 0x1 in
    assert { res = udiv x (2:t) };
    assert { t'int res = div (t'int x) 2 };
    let res : t = lsr_bv res (2:t) in
(*
    assert { res = udiv x (8:t) };
    assert { t'int res = div (t'int x) 8 };
*)
    res

 (* Mask example --------------------- *)

  use bv.BV8 as BV8
  use bv.BV64 as BV64

  use bv.BVConverter_32_64 as C32_46
  use bv.BVConverter_8_32 as C8_32

  type bitvec8 = BV8.t
  type bitvec64 = BV64.t

  let mask ( x : t ) =
    ensures { result = BV8.one }
    (* ensures{ not ( BV8.eq result (BV8.of_int 1) ) } *)
    let res = C8_32.toSmall(
                bw_and
                  (bw_or
                    (bw_and x (0xFFFF_FF00:t))
                    0x1)
                  (0x0000_00FF:t))
    in res

  (* test invariant from frama-c ---------------- *)

  use ref.Ref

  let testVariant( n : t ) =
    let i = ref n in
    let two = 2:t in

    while uge !i two do
    variant{ t'int !i }
      i := lsr_bv !i two
    done

  (* testssss *)

  predicate in_range (n : t) = (ule (0:t) n) /\ (ule n (0x0000_00FF:t))

  predicate add_over (x y : t) = (uge (add x y) x) /\ (uge (add x y) y)

  lemma ttt: forall x y.  (add_over x y) -> (forall i. ult i x -> add_over i y)
end

(** {1 Examples from Hackers Delight} *)

theory Hackers_delight
  use int.Int
  use bv.BV32

  (** de morgan's laws *)

  goal DM1: forall x y.
    bw_not( bw_and x y ) = bw_or (bw_not x) (bw_not y)

  goal DM2: forall x y.
    bw_not( bw_or x y ) = bw_and (bw_not x) (bw_not y)

  goal DM3: forall x.
    bw_not (add x one) = sub (bw_not x) one

  goal DM4: forall x.
    bw_not (sub x one) = add (bw_not x) one

  goal DM5: forall x.
    bw_not (neg x) = sub x one

  goal DM6: forall x y.
    bw_not( bw_xor x y ) = bw_xor (bw_not x) y (* = eq x y *)

  goal DM7: forall x y.
    bw_not( add x y ) = sub (bw_not x) y

  goal DM8: forall x y.
    bw_not( sub x y ) = add (bw_not x) y

  goal DMtest: forall x.
    zeros = bw_not( bw_or x (neg( add x one)))

  (* inequality  *)

  goal IE1: forall x y.
    ule (bw_xor x y) (bw_or x y)

  goal IE2: forall x y.
    ule (bw_and x y) (bw_not( bw_xor x y ))

  goal IE3: forall x y.
    ( ule x (add x y) /\ ule y (add x y) ) -> ule (bw_or x y) (add x y)

  goal IE4: forall x y.
    not ( ule x (add x y) /\ ule y (add x y) ) -> ugt (bw_or x y) (add x y)

  (* shift right and arithmetic shift right *)

  goal SR1: forall x n. ( ule zeros n /\ ule n (31:t)) ->
    bw_or (lsr_bv x n) (lsl_bv (neg( lsr_bv x (31:t) )) (sub (31:t) n))
  = asr_bv x n

  (* rotate en shift *)

  goal RS_left: forall x.
    bw_or (lsl_bv x one) (lsr_bv x (31:t)) = rotate_left_bv x one

  goal RS_right: forall x.
    bw_or (lsr_bv x one) (lsl_bv x (31:t)) = rotate_right_bv x one

  (* bound propagation *)

  goal BP1: forall a b c d x y.
    ( ule a x /\ ule x b /\ ule c y /\ ule y d ) ->
    ( ule b (add b d) /\ ule d (add b d) ) -> (* no overflow in addition *)
      ule (bw_or x y) (add b d) /\ ule zeros (bw_and x y)

  goal BP2: forall a b c d x y.
    ( ule a x /\ ule x b /\ ule c y /\ ule y d ) ->
    ( ule b (add b d) /\ ule d (add b d) ) -> (* no overflow in addition *)
      ule zeros (bw_xor x y) /\ ule (bw_xor x y) (add b d)

  goal BP3: forall a b c d x y.
    ( ule a x /\ ule x b /\ ule c y /\ ule y d ) ->
      ule (bw_not b) (bw_not x) /\ ule (bw_not x) (bw_not a)

end

module Hackers_delight_mod
  use int.Int
  use bv.BV32

  (* de morgan's laws *)

  let dm1 (x : t) (y : t) =
    ensures{ result = bw_or (bw_not x) (bw_not y) }
    bw_not( bw_and x y )

  let dm2 (x : t) (y : t) =
    ensures{ result = bw_and (bw_not x) (bw_not y) }
    bw_not( bw_or x y )

  let dm3 (x : t) =
    ensures{ result = sub (bw_not x) one }
    bw_not( add x 0x1 )

  let dm4 (x : t) =
    ensures{ result = add (bw_not x) one }
    bw_not( sub x 0x1 )

  let dm5 (x : t) =
    ensures{ result = sub x one }
    bw_not( neg x )

  let dm6 (x : t) (y : t) =
    ensures{ result = bw_xor (bw_not x) y }
    bw_not( bw_xor x y )

  let dm7 (x : t) (y : t) =
    ensures{ result = sub (bw_not x) y }
    bw_not( add x y )

  let dm8 (x : t) (y : t) =
    ensures{ result = add (bw_not x) y }
    bw_not( sub x y )

  let dmtest (x : t) =
    ensures{ result = zeros }
    bw_not( bw_or x (neg( add x 0x1)))

  (* inequality  *)

  let ie1 (x : t) (y : t) =
    ensures{ ule result (bw_or x y) }
    bw_xor x y

  let ie2 (x : t) (y : t) =
    ensures{ ule result (bw_not( bw_xor x y ))}
    bw_and x y

  let ie3 (x : t) (y : t) =
    requires{ ule x (add x y) /\ ule y (add x y) }
    ensures{ ule result (add x y) }
    bw_or x y

  let ie4 (x : t) (y : t) =
    requires{ not ( ule x (add x y) /\ ule y (add x y) ) }
    ensures{ ugt result (add x y) }
    bw_or x y

  (* shift right and arithmetic shift right *)

  let sr1 (x : t) (n : t) =
    requires{ ule zeros n /\ ule n (31:t) }
    ensures{ result = asr_bv x n }
    bw_or (lsr_bv x n) (lsl_bv (neg( lsr_bv x (31:t) )) (sub (31:t) n))

  (* rotate en shift *)

  let rs_left (x : t) =
  ensures{ result = rotate_left_bv x one }
    bw_or (lsl_bv x 0x1) (lsr_bv x (31:t))

  let rs_right (x : t) =
  ensures{ result = rotate_right_bv x one }
    bw_or (lsr_bv x 0x1) (lsl_bv x (31:t))

  (* bound propagation *)

  let bp1 (a b c d x y : t) =
  requires{ ule a x /\ ule x b }
  requires{ ule c y /\ ule y d }
  requires{ ule b (add b d) /\ ule d (add b d) } (* no overflow in addition *)
  ensures{ ule result (add b d) }
    bw_or x y

  let bp1' (a b c d x y : t) =
  requires{ ule a x /\ ule x b }
  requires{ ule c y /\ ule y d }
  requires{ ule b (add b d) /\ ule d (add b d) } (* no overflow in addition *)
  ensures{ ule zeros result }
    bw_and x y

  let bp2 (a b c d x y : t) =
  requires{ ule a x /\ ule x b }
  requires{ ule c y /\ ule y d }
  requires{ ule b (add b d) /\ ule d (add b d) } (* no overflow in addition *)
  ensures{ ule zeros result }
  ensures{ ule result (add b d) }
    bw_xor x y

  let bp3 (a b c d x y : t) =
  requires{ ule a x /\ ule x b }
  requires{ ule c y /\ ule y d }
  ensures{ ule (bw_not b) result }
  ensures{ ule result (bw_not a) }
    bw_not x

end

module Test_imperial_violet

  use int.Int
  use int.EuclideanDivision
  use bv.BV32
  use array.Array

  (* to_int and bounds *)

  lemma bv32_bounds_bv:
    forall b. ule zeros b /\ ule b ones

  lemma to_int_ule:
    forall b c. ule b c -> t'int b <= t'int c

  lemma to_int_ult:
    forall b c. ult b c -> t'int b < t'int c

  lemma bv32_bounds_0:
    forall b. 0 <= t'int b

  lemma bv32_bounds:
    forall b. 0 <= t'int b < 0x1_0000_0000

  (* bounded add of array of t *)

  let add (a : array t ) (b : array t) =
    requires{ length a = length b }
    requires{ forall i. 0 <= i < length a ->
                ult a[i] (0x8000_0000:t) }
    requires{ forall i. 0 <= i < length b ->
                ult b[i] (0x8000_0000:t) }
    ensures{ forall i. 0 <= i < length result ->
               t'int result[i] = t'int a[i] + t'int b[i] }
    let sum = make (length a) 0x0 in
    for i = 0 to length a - 1 do
      invariant{ forall j. 0 <= j < i -> sum[j] = add a[j] b[j] }
      invariant{ forall j. 0 <= j < i -> t'int sum[j] = t'int a[j] + t'int b[j] }
      sum[i] <- add a[i] b[i]
    done;
    sum

end

module Test_from_bitvector_example

  use int.Int
  use bv.BV32

  goal Test1:
    let b = bw_and zeros ones in nth_bv b one = False

  goal Test2:
    let b = lsr_bv ones (16:t) in nth_bv b (15:t) = True

  goal Test3:
    let b = lsr_bv ones (16:t) in nth_bv b (16:t) = False

  goal Test4:
    let b = asr_bv ones (16:t) in nth_bv b (15:t) = True

  goal Test5:
    let b = asr_bv ones (16:t) in nth_bv b (16:t) = True

  goal Test6:
    let b = asr_bv (lsr_bv ones one) (16:t) in nth_bv b (16:t) = False

  let lsr31 () =
    ensures{ result = one }
    lsr_bv 0xFFFF_FFFF (31:t)

  let lsr30 () =
    ensures{ result = (3:t) }
    lsr_bv 0xFFFF_FFFF (30:t)

  let lsr29 () =
    ensures{ t'int result = 7 }
    lsr_bv 0xFFFF_FFFF (29:t)

  let lsr28 () =
    ensures{ t'int result = 15 }
    lsr_bv 0xFFFF_FFFF (28:t)

  let lsr27 () =
    ensures{ t'int result = 31 }
    lsr_bv 0xFFFF_FFFF (27:t)

  let lsr26 () =
    ensures{ t'int result = 63 }
    lsr_bv 0xFFFF_FFFF (26:t)

  let lsr20 () =
    ensures{ t'int result = 4095 }
    lsr_bv 0xFFFF_FFFF (20:t)

  let lsr13 () =
    ensures{ t'int result = 524287 }
    lsr_bv 0xFFFF_FFFF (13:t)

  let lsr8 () =
    ensures{ t'int result = 16777215 }
    lsr_bv 0xFFFF_FFFF (8:t)

  goal to_int_0x00000001:
    t'int (lsr_bv ones (31:t)) = 1

  goal to_int_0x00000003:
    t'int (lsr_bv ones (30:t)) = 3

  goal to_int_0x00000007:
    t'int (lsr_bv ones (29:t)) = 7

  goal to_int_0x0000000F:
    t'int (lsr_bv ones (28:t)) = 15

  goal to_int_0x0000001F:
    t'int (lsr_bv ones (27:t)) = 31

  goal to_int_0x0000003F:
    t'int (lsr_bv ones (26:t)) = 63

  goal to_int_0x0000007F:
    t'int (lsr_bv ones (25:t)) = 127

  goal to_int_0x000000FF:
    t'int (lsr_bv ones (24:t)) = 255

  goal to_int_0x000001FF:
    t'int (lsr_bv ones (23:t)) = 511

  goal to_int_0x000003FF:
    t'int (lsr_bv ones (22:t)) = 1023

  goal to_int_0x000007FF:
    t'int (lsr_bv ones (21:t)) = 2047

  goal to_int_0x00000FFF:
    t'int (lsr_bv ones (20:t)) = 4095

  goal to_int_0x00001FFF:
    t'int (lsr_bv ones (19:t)) = 8191

  goal to_int_0x00003FFF:
    t'int (lsr_bv ones (18:t)) = 16383

  goal to_int_0x00007FFF:
    t'int (lsr_bv ones (17:t)) = 32767

  goal to_int_0x0000FFFF:
    t'int (lsr_bv ones (16:t)) = 65535

  goal to_int_0x0001FFFF:
    t'int (lsr_bv ones (15:t)) = 131071

  goal to_int_0x0003FFFF:
    t'int (lsr_bv ones (14:t)) = 262143

  goal to_int_0x0007FFFF:
    t'int (lsr_bv ones (13:t)) = 524287

  goal to_int_0x000FFFFF:
    t'int (lsr_bv ones (12:t)) = 1048575

  goal to_int_0x00FFFFFF:
    t'int (lsr_bv ones (8:t)) = 16777215

  goal to_int_0xFFFFFFFF:
    t'int ones = 4294967295

end