// **************************************************************************
//
//    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 UnsignedBitArithmetic(nat{range} ?x,?y,?z)  {
    nothing;
} satisfies {
    // --- "<=" is a total order
    ord00 : assert (0 <= 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)) % range == 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: 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 [DisProveA]: 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);

    // --- modulo  ------------------------
    mod1: assert !(y == 0) -> (0 <= x % y);
    mod2: assert (0 < y) -> (x % y < y);
    mod3: assert (y < 0) -> (y < x % y);
    mod4: assert (x == (x / y) * y + (x % y));

}