%
% Proof of the Shifter for the DLX ALU
%
% (C) 2000-2001 Daniel Kroening
%

alu_shifter_proof[N: above(1), logN: posnat]: THEORY
  BEGIN
    ASSUMING

      logN_is_logN: ASSUMPTION N=2^logN;

    ENDASSUMING

    IMPORTING alu_shifter_impl[N, logN],
              alu_shifter_spec[N, logN];

    op: VAR bvec[N];
    distance: VAR bvec[logN];
    right, arithmetic: VAR bit;

    shifter_distance_correct: LEMMA
      bv2nat(shifter_distance(distance, right))=
      IF right AND bv2nat(distance)/=0 THEN
        N-bv2nat(distance)
      ELSE
        bv2nat(distance)
      ENDIF;

    alu_leftshift_correct: LEMMA
      NOT right =>
      alu_shifter_spec(op, distance, right, arithmetic)=
      alu_shifter_impl(op, distance, right, arithmetic);      

    alu_rightshift_correct: LEMMA
      right =>
      alu_shifter_spec(op, distance, right, arithmetic)=
      alu_shifter_impl(op, distance, right, arithmetic);

    alu_shifter_correct: LEMMA
      alu_shifter_spec(op, distance, right, arithmetic)=
      alu_shifter_impl(op, distance, right, arithmetic);

  END alu_shifter_proof