%
% implementaion of a direct mapped cache
% for a 2^a x 8*B memory
% with 2^l lines, 2^s sectors
%

cache_io_types[a:posnat, s:below(a), B:posnat]: THEORY
BEGIN
  memory_interface : LIBRARY = "../memory_interface";
  predicates       : LIBRARY = "../predicates";

  IMPORTING 
    memory_interface@memory_interface_lemmas[a, B]

% subtypes of address and extraction functions
  sectt    : TYPE+ = bvec[s];
  non_sectt: TYPE+ = bvec[a-s];

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

  address_non_sect(address:addresst[a,B]):bvec[a-s] = address^(a-1,s);

% a predicate for addresses in the same sector
  same_sect?(c,b:addresst) : bool = 
    address_non_sect(c)=address_non_sect(b);

% for use as a predicate, written as a function of one parameter
  same_sect_p?(c:addresst)(b:addresst) : bool =
    same_sect?(c,b);

% a tuple type supporting a cache with all its inputs
  cache_inputt : TYPE+ =
    [# address    : addresst[a,B], 
       di         : wordt[a,B], 
       valid      : bit,
       vw         : bit,
       dirty      : bit,
       dw         : bit,
       clear      : bit,
       tw         : bit,
       cdwb       : bvec[B],
       linv       : bit,
       cache_rd   : bit #];

  cache_outputt : TYPE+ =
    [# hit          : bit, 
       dirty        : bit,
       ev_address   : addresst[a,B],
       dout         : wordt[a,B]  #];

% subtypes for clear/nonclear inputs with predicates
  clear?(x:cache_inputt):bool = x`clear;

  cache_input_ct  : TYPE+ = (clear?) CONTAINING
    (# address :=fill[a](FALSE), 
       di      :=fill[8*B](FALSE),
       valid   :=FALSE, 
       vw      :=FALSE, 
       dirty   :=FALSE,
       dw      :=FALSE,
       clear   :=TRUE, 
       tw      :=FALSE, 
       cdwb    :=fill[B](FALSE),
       linv    :=FALSE, 
       cache_rd:=FALSE #);

  cache_input_nct : TYPE+ = (NOT clear?) CONTAINING
    (# address :=fill[a](FALSE), 
       di      :=fill[8*B](FALSE),
       valid   :=FALSE, 
       vw      :=FALSE, 
       dirty   :=FALSE,
       dw      :=FALSE,
       clear   :=FALSE, 
       tw      :=FALSE, 
       cdwb    :=fill[B](FALSE),
       linv    :=FALSE, 
       cache_rd:=FALSE #);


% if the cache inputs are provided by a function
% nat -> cache_inputt,
% we call this function valid iff clear is active in cycle 0
  valid_function?(f:[nat -> cache_inputt]):bool = clear?(f(0));

  cache_input_funct : TYPE+ = (valid_function?)
  CONTAINING LAMBDA (i:nat):
    (# address :=fill[a](FALSE), 
       di      :=fill[8*B](FALSE),
       valid   :=FALSE, 
       vw      :=FALSE, 
       dirty   :=FALSE,
       dw      :=FALSE,
       clear   :=i=0, 
       tw      :=FALSE, 
       cdwb    :=fill[B](FALSE),
       linv    :=FALSE, 
       cache_rd:=FALSE #);
  
% the cache output depends on the address at the cache input
  cache_output_funct : TYPE+ = [nat,addresst -> cache_outputt];

% the following induction is on cache_rd-cycles
  is_cache_rd?(input:cache_inputt) : bool = 
    input`cache_rd OR input`clear;

  IMPORTING predicates@predicates[cache_inputt,is_cache_rd?];

  exists_last_cache_rd : LEMMA
    FORALL (input: cache_input_funct,t: posnat) :
      exists_last_pred?(input)(t);

% a predicate stating that inputs are "good"
  good_input?(input:cache_input_funct) : bool =
    (FORALL (i:posnat):
    % an active valid write is alway accompanied by a tag write
      input(i)`valid AND input(i)`vw IMPLIES input(i)`tw) AND
    FORALL (i:posnat):
      input(i)`vw OR input(i)`tw OR input(i)`dw OR
          (EXISTS (l:below(B)):input(i)`cdwb(l))
        IMPLIES
    % any write is to the address (mod sector)
    % of the last cache_rd
          same_sect?(input(i)`address,
                     input(last_pred_before(input)(i))`address) AND
    % especially, there is no such access if there is no
    % last cache_rd, i.e. the last cache_rd is a clear
          NOT input(last_pred_before(input)(i))`clear AND
    % and, last but not least, a write never coincides
    % with a cache_rd
          NOT input(i)`cache_rd;

  cdwb_helper : PROPOSITION
    FORALL (input: cache_inputt,
            byte : below(B)):
      input`cdwb(byte) IMPLIES EXISTS (l:below(B)):input`cdwb(l);

  address_nonsect_helper : PROPOSITION
   FORALL (a:non_sectt,s:sectt):
     address_non_sect(a o s)=a;

END cache_io_types