%
% consistency of the set associative cache
%

sa_cache_consistency[K:upfrom(2),
                     logK:posnat,
                     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;
    logK_is_logK: ASSUMPTION 
      2^(logK-1) < K AND K <= 2^logK;
  ENDASSUMING

  IMPORTING 
    sa_cache_history[K,logK,a,t,l,s,B];

  sa_good_linefill_inputt(initial_sa_cache : sa_cache_configt) : TYPE =
    (LAMBDA (x:(good_input?)): 
      good_linefill_input?(LAMBDA (n:nat):sa_cache_output_funct(initial_sa_cache,x)(n,x(n)`address))(x));

  dm_cache_input_address_is_address : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : cache_input_funct,
            k                : wayt,
            n                : nat):
      dm_cache_input_funct(initial_sa_cache,input,k)(n)`address=input(n)`address;

  dm_cache_good_linefill_input : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : sa_good_linefill_inputt(initial_sa_cache),
            k                : wayt):
      good_linefill_input?(LAMBDA (n:nat):dm_cache_output_funct(initial_sa_cache,input,k)(n,input(n)`address))
                          (dm_cache_input_funct(initial_sa_cache,input,k));

  dm_cache_data_consistency : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : sa_good_linefill_inputt(initial_sa_cache),
            k                : wayt):
      cache_consistency?(dm_cache_output_funct(initial_sa_cache,input,k),
                         dm_cache_input_funct(initial_sa_cache,input,k));

  sa_cache_exists_last_write_to_hit_way : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : sa_good_linefill_inputt(initial_sa_cache),
            address          : addresst,
            b                : below(B),
            i                : posnat): 
      sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit IMPLIES
        LET sa_cache      =sa_cache_config(initial_sa_cache,i,input),
            k             =the(sa_cache_hit_vector(sa_cache,address)),
            dm_cache_input=dm_cache_input_funct(initial_sa_cache,input,k) IN
        exists_last_pred?[cache_inputt,is_byte_write?(address,b)](dm_cache_input)(i) AND
          last_pred_before[cache_inputt,is_byte_write?(address,b)](dm_cache_input)(i)>0;

  sa_cache_exists_last_write_before_hit : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : sa_good_linefill_inputt(initial_sa_cache),
            address          : addresst,
            b                : below(B),
            i                : posnat):
      sa_cache_output_funct(initial_sa_cache,input)(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;

  sa_cache_create_hit_implies_vw_and_valid : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : sa_good_linefill_inputt(initial_sa_cache),
            address          : addresst,
            j                : posnat,
            i                : below(j)):
    NOT sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit AND
      sa_cache_output_funct(initial_sa_cache,input)(j,address)`hit IMPLIES
    EXISTS (k:subrange(i,j-1)):input(k)`vw AND input(k)`valid AND same_sect?(address,input(k)`address);

  sa_cache_vw_and_valid_is_miss : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : sa_good_linefill_inputt(initial_sa_cache),
            address          : addresst,
            i                : posnat):
      input(i)`vw AND input(i)`valid AND NOT input(i)`clear AND 
        same_sect?(address,input(i)`address) IMPLIES
        NOT sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit;

  sa_cache_hit_equal_after_last_write : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : sa_good_linefill_inputt(initial_sa_cache),
            address          : addresst,
            b                : below(B),
            i                : posnat): 
      sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit IMPLIES
        LET sa_cache      =sa_cache_config(initial_sa_cache,i,input),
            k             =the(sa_cache_hit_vector(sa_cache,address)),
            dm_cache_input=dm_cache_input_funct(initial_sa_cache,input,k),
            last_bw = last_pred_before[cache_inputt,is_byte_write?(address,b)](dm_cache_input)(i),
            last    = last_pred_before(input)(last_bw) IN
          EXISTS (j:subrange(last_bw,i)):
            last_pred_before(input)(j)=last AND            
            FORALL (k:subrange(last_bw,i)):
              IF k>=j THEN
                LET old_sa_cache=sa_cache_config(initial_sa_cache,k,input) IN
                  sa_cache_hit_vector(sa_cache,address)=sa_cache_hit_vector(old_sa_cache,address)
              ELSE
                NOT sa_cache_output_funct(initial_sa_cache,input)(k,address)`hit
              ENDIF;

  sa_cache_no_byte_write_after_last_write_to_hit_way : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : sa_good_linefill_inputt(initial_sa_cache),
            address          : addresst,
            b                : below(B),
            i                : posnat): 
      sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit IMPLIES
        LET sa_cache      =sa_cache_config(initial_sa_cache,i,input),
            k             =the(sa_cache_hit_vector(sa_cache,address)),
            dm_cache_input=dm_cache_input_funct(initial_sa_cache,input,k),
            last_bw = last_pred_before[cache_inputt,is_byte_write?(address,b)](dm_cache_input)(i) IN
        FORALL (j:subrange(last_bw+1,i-1)):
          NOT is_byte_write?(address,b)(input(j));

  sa_cache_last_write_to_hit_way : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : sa_good_linefill_inputt(initial_sa_cache),
            address          : addresst,
            b                : below(B),
            i                : posnat):
    sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit IMPLIES
      LET sa_cache      =sa_cache_config(initial_sa_cache,i,input),
          k             =the(sa_cache_hit_vector(sa_cache,address)),
          dm_cache_input=dm_cache_input_funct(initial_sa_cache,input,k) IN
        last_pred_before[cache_inputt[a,s,B],is_byte_write?(address,b)](dm_cache_input)(i)=
        last_pred_before[cache_inputt[a,s,B],is_byte_write?(address,b)](input)(i);

  sa_cache_data_consistency_inherited : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : sa_good_linefill_inputt(initial_sa_cache)):
      (FORALL (k : wayt):
        cache_consistency?(dm_cache_output_funct(initial_sa_cache,input,k),
                           dm_cache_input_funct(initial_sa_cache,input,k))) IMPLIES
        cache_consistency?(sa_cache_output_funct(initial_sa_cache,input),input);

  sa_cache_data_consistency : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : sa_good_linefill_inputt(initial_sa_cache)):
        cache_consistency?(sa_cache_output_funct(initial_sa_cache,input),input);

  sa_cache_io_consistency : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : (LAMBDA (x:(good_input?)): 
                                  good_linefill_input?(sa_cache_out(initial_sa_cache,x))(x))):
        cache_io_consistency?(sa_cache_out(initial_sa_cache,input),input);

END sa_cache_consistency