%
% a criterion for cache consistency
%

consistency[a:posnat, s:below(a), B:posnat]: THEORY
BEGIN

  predicates       : LIBRARY = "../predicates";

  IMPORTING 
    cache_io_types[a, s, B]

% we restrict good_input still further by 2 criteria
% (this time depending on the actual cache output)
  good_linefill_input?(output :[nat->cache_outputt])
                      (input  :cache_input_funct) : bool =
% 0) tw => vw and valid
    (FORALL (i:posnat):
      input(i)`tw IMPLIES input(i)`vw AND input(i)`valid) AND
% 1) on a line fill, all bytes in the cache sector
%    are written prior to raising the valid flag
%    (still independent of cache output)
    (FORALL (i:posnat):
      LET last = last_pred_before(input)(i) IN
      input(i)`valid AND input(i)`vw IMPLIES
        EXISTS (k : subrange(last+1,i-1)):
          NOT input(k)`valid AND input(k)`vw AND
          (FORALL (j    : subrange(last+1,k-1)):
             NOT input(j)`vw) AND
          (FORALL (j    : subrange(k+1,i-1)):
             NOT input(j)`vw) AND         
          FORALL (address : (same_sect_p?(input(i)`address)),
                  byte    : below(B)):
            EXISTS (j : subrange(k+1,i)):
              input(j)`address=address AND
              input(j)`cdwb(byte)) AND
% 2) after a cache miss, there is no data write 
%    safe for a line fill 
%    (criterion 1 is not sufficient to show cache consistency)
    FORALL (i:posnat):
      LET last = last_pred_before(input)(i) IN
        (NOT output(last)`hit AND
          EXISTS (byte : below(B)) : input(i)`cdwb(byte))
        IMPLIES EXISTS (j : subrange(last+1,i-1)): 
          input(j)`vw AND NOT input(j)`valid AND
          (FORALL (k:subrange(last+1,j-1)): NOT input(k)`vw);

  same_sect_helper : SUBLEMMA
    FORALL (a,b:addresst) : 
      same_sect?(a,b) = same_sect_p?(a)(b);

% in the criterion below, we need to refer to the
% 'last write' to a byte in an address
  is_byte_write?(address:addresst, byte:below(B))
                (input:cache_inputt) : bool =
    input`address=address AND input`cdwb(byte);

  IMPORTING predicates@predicates;

% a criterion for cache consistency:
% in case of a hit, any byte in the 'hit' address
% corresponds to the value written to this byte
% on the last write to it 
% (in particular there exists such a write!)
  cache_consistency?(output :cache_output_funct,
                     input  :[nat->cache_inputt]) : bool =
    FORALL (i       : posnat,
            address : addresst,
            b       : below(B)):
      output(i,address)`hit IMPLIES
        exists_last_pred?[cache_inputt,is_byte_write?(address,b)](input)(i) AND
        last_pred_before[cache_inputt,is_byte_write?(address,b)](input)(i)>0 AND
        byte(b,output(i,address)`dout) = 
        byte(b,input(last_pred_before[cache_inputt,is_byte_write?(address,b)](input)(i))`di);

  cache_io_consistency?(output : [nat->cache_outputt],
                        input  : [nat->cache_inputt]) : bool =
    FORALL (i       : posnat,
            b       : below(B)):
      output(i)`hit IMPLIES
        exists_last_pred?[cache_inputt,is_byte_write?(input(i)`address,b)](input)(i) AND
        last_pred_before[cache_inputt,is_byte_write?(input(i)`address,b)](input)(i)>0 AND
        byte(b,output(i)`dout) = 
        byte(b,input(last_pred_before[cache_inputt,is_byte_write?(input(i)`address,b)](input)(i))`di);

  good_input_upto?(T:nat)(input:cache_input_funct) : bool =
    (FORALL (i:subrange(1,T)):
      input(i)`valid AND input(i)`vw IMPLIES input(i)`tw) AND
    FORALL (i:subrange(1,T)):
      input(i)`vw OR input(i)`tw OR input(i)`dw OR
          (EXISTS (l:below(B)):input(i)`cdwb(l))
        IMPLIES
          same_sect?(input(i)`address,
                     input(last_pred_before(input)(i))`address) AND
          NOT input(last_pred_before(input)(i))`clear AND
          NOT input(i)`cache_rd;

  good_linefill_input_upto?(T:nat,output :[nat->cache_outputt])
                           (input  :cache_input_funct) : bool =
    (FORALL (i:subrange(1,T)):
      input(i)`tw IMPLIES input(i)`vw AND input(i)`valid) AND
    (FORALL (i:subrange(1,T)):
      LET last = last_pred_before(input)(i) IN
      input(i)`valid AND input(i)`vw IMPLIES
        EXISTS (k : subrange(last+1,i-1)):
          NOT input(k)`valid AND input(k)`vw AND
          (FORALL (j    : subrange(last+1,k-1)):
             NOT input(j)`vw) AND
          (FORALL (j    : subrange(k+1,i-1)):
             NOT input(j)`vw) AND         
          FORALL (address : (same_sect_p?(input(i)`address)),
                  byte    : below(B)):
            EXISTS (j : subrange(k+1,i)):
              input(j)`address=address AND
              input(j)`cdwb(byte)) AND
    FORALL (i:subrange(1,T)):
      LET last = last_pred_before(input)(i) IN
        (NOT output(last)`hit AND
          EXISTS (byte : below(B)) : input(i)`cdwb(byte))
        IMPLIES EXISTS (j : subrange(last+1,i-1)): 
          input(j)`vw AND NOT input(j)`valid AND
          (FORALL (k:subrange(last+1,j-1)): NOT input(k)`vw);

  cache_io_consistency_upto?(T:nat,output : [nat->cache_outputt],
                             input : [nat->cache_inputt]) : bool =
    FORALL (i       : subrange(1,T),
            byte    : below(B)):
      output(i)`hit IMPLIES
        exists_last_pred?[cache_inputt,is_byte_write?(input(i)`address,byte)](input)(i) AND
        last_pred_before[cache_inputt,is_byte_write?(input(i)`address,byte)](input)(i)>0 AND
        byte(byte,output(i)`dout) = 
        byte(byte,input(last_pred_before[cache_inputt,is_byte_write?(input(i)`address,byte)](input)(i))`di);


END consistency