// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************
//  This file demonstrates the theorem proving facilities of Averest
//  concerning bitvectors.
// **************************************************************************

macro range = 16;

module SignedBitArithmetic(int{range} x,y,z) {
    nothing;
} satisfies {

    // --- " <= " is a total order
    ord00 : assert (-range <= x) & (x < range);
    ord01 : assert x <= x;
    ord02 : assert (x <= y) & (y <= x) -> (x == y);
    ord03 : assert (x <= y) & (y <= z) -> (x <= z);
    ord04 : assert (x <= y) | (y <= x);

    // --- "<" is a strict total order
    ord05 : assert !(x < x);
    ord06: assert (x < y) -> !(y < x);
    ord07: assert (x < y) & (y < z) -> (x < z);
    ord08: assert (x < y) | (x == y) | (y < x);

    // --- defining numeric relations by "<"
    ord09: assert (x <= y) <-> (x < y) | (x == y);
    ord10: assert (x > y) <-> (y < x);
    ord11: assert (x >= y) <-> !(x < y);
    ord12: assert (x == y) <-> !(x < y) & !(y < x);

    // --- defining numeric relations by " <= "
    ord13: assert (x < y)  <-> (x <= y) & !(y <= x);
    ord14: assert (x > y)  <-> !(x <= y);
    ord15: assert (x >= y) <-> (y <= x);
    ord16: assert (x == y)  <-> (x <= y) & (y <= x);

    // --- field axioms ---------------------
    f01 : assert x + +0 == x;
    f02 : assert x + y == y + x;
    f03 : assert (x + y) + z == x + (y + z);
    f04 : assert x + (+0 - x) == +0;
    f05 : assert x * +0 == +0;
    f06 : assert x == x * +1;
    f07 : assert x * y == y * x;
    f08 : assert x * (y * z) == (x * y) * z;
    f09 : assert x * (y + z) == x * y + x * z;

    // --- monotonicity ------------------------
    mono00: assert (x == y) <-> (x + z == y + z);
    mono01[DisProveA]: assert (x <= y) <-> (x + z <= y + z);
    // counterexample for mono01: assert  x == 0000, y=1000, z=1000
    mono02[DisProveA]: assert (x < y) <-> (x + z < y + z);
    // counterexample for mono02: assert  x == 0000, y=1000, z=1000
    mono03: assert (x + y == +0) & (+0 <= x) & (+0 <= y) -> (x == +0) & (y == +0);
    mono04: assert (x + y == x) -> (y == +0);
    mono05[DisProveA]: assert (x < y) & (+0 <= z) -> (x < y+z);
    // counterexample for mono05: assert  x == 0000, y=0100, z=0100
    mono06: assert (x < y) & (y <= z) -> (x < z);

    // --- division  ------------------------
    div1 : assert !(y == +0) -> (+0 <= x % y);
    div2 : assert (+0 < y) -> (x % y < y);
    div3 : assert (y < +0) -> (y < x % y);
    div4 : assert (y!=+0) -> (x == (x / y) * y + (x % y));
}