%
% specification for the next history vector
%
% $Id: spec.pvs,v 1.5 2001/05/29 12:30:50 sbeyer Exp $
%
% $Log: spec.pvs,v $
% Revision 1.5  2001/05/29 12:30:50  sbeyer
% * removed EXPORTING declaration
%
% Revision 1.4  2001/05/22 12:10:38  sbeyer
% added 2 lemmas about history movement
%
% Revision 1.3  2001/05/21 12:56:33  sbeyer
% added lemma way_moves_lte_1_positions_backward and fixed some unexplainable (non-existent?) errors
%
% Revision 1.2  2001/05/03 13:41:32  sbeyer
% finally removed ^ in definition of unary...
%
% Revision 1.1  2001/03/09 13:31:34  sbeyer
% *** empty log message ***
%

spec[K:upfrom(2),
     logK:posnat]: THEORY
BEGIN
  ASSUMING
    logK_is_logK: ASSUMPTION 
      2^(logK-1) < K AND K <= 2^logK;
  ENDASSUMING

  IMPORTING 
    finite_sets@func_composition,
    history_types[K,logK]

  unary?(a:hit_vectort):bool =
    FORALL (j,k:history_indext): 
      a(k) AND a(j) IMPLIES k=j;

  single_unary: JUDGEMENT 
    (singleton?[history_indext]) SUBTYPE_OF (unary?);
  empty_unary:  JUDGEMENT 
    (empty?[history_indext])     SUBTYPE_OF (unary?);
  unary_single_or_empty : JUDGEMENT
    (unary?)                     SUBTYPE_OF (empty?[history_indext] OR singleton?[history_indext]);
  unary_hit : JUDGEMENT 
    (unary? AND 
     NOT empty?[history_indext]) SUBTYPE_OF (singleton?[history_indext]);

  history_spect : TYPE = [history_indext -> history_indext];

  permutation?(history_spec:history_spect) : bool =
    bijective?[history_indext, history_indext](history_spec);

% specification of history permutation
  next_history_permutation(history_vector : (permutation?), 
                           hit_vector     : (unary?),  
                           linv           : bool) : history_spect =

    LAMBDA (i:history_indext) : 
      IF linv THEN
        IF NOT empty?(hit_vector) THEN
          IF i<K-1 THEN
            IF i+1>inverse(history_vector)(the(hit_vector)) THEN
              history_vector(i+1)
            ELSE
              history_vector(i)
            ENDIF
          ELSE
            the(hit_vector)
          ENDIF
        ELSE
          history_vector(i)
        ENDIF
      ELSE
        IF NOT empty?(hit_vector) THEN
          IF i>0 THEN
            IF i>inverse(history_vector)(the(hit_vector)) THEN
              history_vector(i)
            ELSE
              history_vector(i-1)
            ENDIF
          ELSE
            the(hit_vector)
          ENDIF
        ELSE
          IF i=0 THEN
            history_vector(K-1)
          ELSE
            history_vector(i-1)
          ENDIF
        ENDIF
      ENDIF;

% little helper: unary = no bits active or
% exacly one bit active
  unary_is_one_or_none1 : LEMMA
    FORALL (a:hit_vectort):
      unary?(a) IFF 
      ((FORALL (j:history_indext) : NOT a^j) OR
        EXISTS (i:history_indext):
          FORALL (j:history_indext) : a^j = (i=j));

  unary_is_one_or_none : COROLLARY
    FORALL (a:hit_vectort):
      unary?(a) IFF 
      (a=fill[K](FALSE) OR
        EXISTS (i:history_indext):
          a = LAMBDA (j:history_indext) : j=i);

  inverse_next_history_permutation(inverse_history: (permutation?),
                                   hit_vector     : (unary?),
                                   linv           : bool) : 
    history_spect =
    LAMBDA (i:history_indext) : 
      IF linv THEN
        IF NOT empty?(hit_vector) THEN
          IF inverse_history(i)=inverse_history(the(hit_vector)) THEN
            K-1
          ELSE
            IF inverse_history(i)>inverse_history(the(hit_vector)) THEN
              inverse_history(i)-1
            ELSE
              inverse_history(i)
            ENDIF
          ENDIF
        ELSE
          inverse_history(i)
        ENDIF
      ELSE
        IF NOT empty?(hit_vector) then
          IF inverse_history(i)=inverse_history(the(hit_vector)) THEN
            0
          ELSE
            IF inverse_history(i)>inverse_history(the(hit_vector)) THEN
              inverse_history(i)
            ELSE
              inverse_history(i)+1
            ENDIF
          ENDIF
        ELSE
          IF inverse_history(i)=K-1 THEN
            0
          ELSE
            inverse_history(i)+1
          ENDIF
        ENDIF
      ENDIF;

  next_history_permutation_bijective : THEOREM
    FORALL (history_vector : (permutation?),
            hit_vector     : (unary?),
            linv           : bool):
    permutation?(next_history_permutation(history_vector,
                                          hit_vector,
                                          linv));

  inverse_permutation : LEMMA
    FORALL (history_vector : (permutation?)):
    permutation?(inverse(history_vector));

  inverse_next_history_permutation_correct1 : LEMMA
    FORALL (history_vector : (permutation?),
            hit_vector     : (unary?),
            linv           : bool,
            history_index  : history_indext):
    (inverse_next_history_permutation(inverse(history_vector), hit_vector, linv) o 
      next_history_permutation(history_vector,hit_vector, linv))
       (history_index) = history_index;

  inverse_next_history_permutation_correct : LEMMA
    FORALL (history_vector : (permutation?),
            hit_vector     : (unary?), 
            linv           : bool):
    inverse_next_history_permutation(inverse(history_vector), hit_vector, linv) o
      next_history_permutation(history_vector, hit_vector, linv) = identity;

  inverse_next_history_permutation_is_inverse : LEMMA
    FORALL (history_vector : (permutation?),
            hit_vector     : (unary?), 
            linv           : bool):
    inverse_next_history_permutation(inverse(history_vector), hit_vector, linv) =
    inverse(next_history_permutation(history_vector, hit_vector, linv));

  next_way_reg_spec(history_vector:history_spect, 
                    hit_vector    :(unary?)) : history_indext =
    IF NOT empty?(hit_vector) THEN
      the(hit_vector)
    ELSE
      history_vector(K-1)
    ENDIF;

% a read/write hit makes a way most recently used
  hit_makes_most_recently_used : THEOREM
    FORALL (history_vector : (permutation?),
            hit_vector     : (unary?)):
      NOT empty?(hit_vector) IMPLIES
        inverse_next_history_permutation(inverse(history_vector),
                                         hit_vector,
                                         FALSE)
        (the(hit_vector))=0;

  linv_hit_makes_least_recently_used : LEMMA
    FORALL (history_vector : (permutation?),
            hit_vector     : (unary?)):
      NOT empty?(hit_vector) IMPLIES
        inverse_next_history_permutation(inverse(history_vector),
                                         hit_vector,
                                         TRUE)
        (the(hit_vector))=K-1;

  linv_miss_is_identity : LEMMA
    FORALL (history_vector : (permutation?),
            hit_vector     : (unary?)):
      empty?(hit_vector) IMPLIES
        inverse_next_history_permutation(inverse(history_vector),
                                         hit_vector,
                                         TRUE)
        =inverse(history_vector);

  no_change_behind_hit_way : LEMMA
    FORALL (history_vector : (permutation?),
            hit_vector     : (unary?)):
      NOT empty?(hit_vector) IMPLIES
        FORALL (j:history_indext):
          inverse(history_vector)(j)>inverse(history_vector)(the(hit_vector)) IMPLIES
          inverse_next_history_permutation(inverse(history_vector),
                                           hit_vector,
                                           FALSE)(j)
            =inverse(history_vector)(j);

  no_change_before_linv_hit_way : LEMMA
    FORALL (history_vector : (permutation?),
            hit_vector     : (unary?)):
      NOT empty?(hit_vector) IMPLIES
        FORALL (j:history_indext):
          inverse(history_vector)(j)<inverse(history_vector)(the(hit_vector)) IMPLIES
          inverse_next_history_permutation(inverse(history_vector),
                                           hit_vector,
                                           TRUE)(j)
            =inverse(history_vector)(j);

  only_hit_way_moves_backward : THEOREM
    FORALL (history_vector : (permutation?),
            way            : history_indext,
            hit_vector     : (unary?)):
        NOT empty?(hit_vector) AND
        inverse_next_history_permutation(inverse(history_vector),
                                    hit_vector,
                                    FALSE)(way)<
        inverse(history_vector)(way) IMPLIES
        way=the(hit_vector);

  only_linv_hit_way_moves_forward : THEOREM
    FORALL (history_vector : (permutation?),
            way            : history_indext,
            hit_vector     : (unary?)):
        inverse_next_history_permutation(inverse(history_vector),
                                    hit_vector,
                                    TRUE)(way)>
        inverse(history_vector)(way) IMPLIES
        NOT empty?(hit_vector) AND way=the(hit_vector);

% a way in the hit vector moves at most one position forward
% if there is no linv
  way_moves_lte_1_positions_forward : THEOREM
    FORALL (history_vector : (permutation?),
            way            : history_indext,
            hit_vector     : (unary?)):
        inverse_next_history_permutation(inverse(history_vector),
                                    hit_vector,
                                    FALSE)(way)<=
        inverse(history_vector)(way)+1;

% a way in the hit vector moves at most one position forward
% if there is a linv
  way_moves_lte_1_positions_backward : THEOREM
    FORALL (history_vector : (permutation?),
            way            : history_indext,
            hit_vector     : (unary?)):
        inverse_next_history_permutation(inverse(history_vector),
                                    hit_vector,
                                    TRUE)(way)>=
        inverse(history_vector)(way)-1;

END spec