%
% further types for a direct mapped cache
%

cache_types[a:posnat, 
            t:subrange(1,a), 
            l:upto(a-t), 
            s:upto(a-l-t), 
            B:posnat]: THEORY
BEGIN
  ASSUMING
    t_plus_l_plus_s_is_a : ASSUMPTION
      t+l+s=a;
  ENDASSUMING

  IMPORTING 
    cache_io_types[a,s,B];

% subtypes of address and extraction functions
  cache_tagt     : TYPE+ = bvec[t];
  linet    : TYPE+ = bvec[l];
  linesectt: TYPE+ = bvec[l+s];
  address_tag (address:addresst[a,B]): bvec[t]  = address^(a-1  ,a-t);
  address_line(address:addresst[a,B]): bvec[l] = 
    IF l=0 THEN
      fill[l](FALSE)
    ELSE
      address^(l+s-1,s)
    ENDIF;

  address_linesect(address:addresst[a,B]) : bvec[l+s] = 
    IF l+s=0 THEN
      fill[l+s](FALSE)
    ELSE
      address^(l+s-1,0)
    ENDIF;

% a simple lemma about addresses in the same sector
  same_sect_def : LEMMA
    FORALL (a,b:addresst):
      same_sect?(a,b) IFF 
      address_tag (a)=address_tag (b) AND
      address_line(a)=address_line(b);

  linesect_is_line_and_sect : LEMMA
    FORALL (a,b:addresst):
    address_linesect(a)=address_linesect(b) IFF
    address_line(a)=address_line(b) AND
    address_sect(a)=address_sect(b);

  address_is_line_and_sect_and_tag : LEMMA
    FORALL (a,b:addresst):
    a=b IFF
    address_line(a)=address_line(b) AND
    address_sect(a)=address_sect(b) AND
    address_tag (a)=address_tag (b);

END cache_types