%
% consistency of the set associative cache
%

sa_cache_liveness[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_consistency[K,logK,a,t,l,s,B];

%  good_history_input?(output :cache_output_funct)
%                      (input  :(good_linefill_input?)) : bool =
%    FORALL (i:posnat):
%      input(i)`cache_rd AND input(i)`linv IMPLIES
%        EXISTS (j:above(i)):
%          last_pred_before(input)(j)=last AND
%          input(j)`clear OR
%          input(j)`vw AND NOT input(j)`valid AND ;

  sa_cache_lost_hit_is_clear_or_linv_or_lru_miss : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : sa_good_linefill_inputt(initial_sa_cache),
            address          : addresst,
            i                : posnat):
      LET hit_input=LAMBDA (n:nat):
              sa_cache_hit_vector(sa_cache_config(initial_sa_cache,n,input),input(n)`address),
          last     = last_pred_before(input)(i),
          sa_cache = sa_cache_config(initial_sa_cache,i,input) IN
      sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit AND
      NOT sa_cache_output_funct(initial_sa_cache,input)(i+1,address)`hit IMPLIES
        LET k=the(sa_cache_hit_vector(sa_cache,address)) IN
        input(i)`clear OR  %clear
        same_sect?(address,input(i)`address) AND %linv
          input(i)`vw AND NOT input(i)`valid OR
        NOT same_sect?(address,input(i)`address) AND
          address_line(address)=address_line(input(i)`address) AND %different tag
          input(i)`vw AND NOT input(i)`valid AND %linv
          ev(last, input,
              LAMBDA (n: nat):
                sa_cache_hit_vector(sa_cache_config
                                    (initial_sa_cache, n, input),
                                    input(n)`address))=k AND %lru
          NOT sa_cache_output_funct(initial_sa_cache,input)(last,input(last)`address)`hit; %miss

  sa_cache_way_becomes_less_recently_used_after_miss : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : sa_good_linefill_inputt(initial_sa_cache),
            address          : addresst,
            i                : posnat,
            k                : wayt):
      LET hit_input=LAMBDA (n:nat):
              sa_cache_hit_vector(sa_cache_config(initial_sa_cache,n,input),input(n)`address) IN
      inv_hist_spec(i+1,input,hit_input)(address_line(address))(k)>
        inv_hist_spec(i,input,hit_input)(address_line(address))(k) AND
        NOT input(i)`clear AND NOT input(i)`linv IMPLIES
        input(i)`cache_rd AND % $rd
          address_line(address)=address_line(input(i)`address) AND %same line
          inv_hist_spec(i+1,input,hit_input)(address_line(address))(k)=
          inv_hist_spec(i,input,hit_input)(address_line(address))(k)+1 AND %lte 1 position
          FORALL (j:(LAMBDA (way:wayt): 
                      inv_hist_spec(i,input,hit_input)(address_line(address))(way)<=
                      inv_hist_spec(i,input,hit_input)(address_line(address))(k))): 
              NOT dm_cache_output_funct(initial_sa_cache,input,j)(i,input(i)`address)`hit; %miss

% an extension of the above lemma
  sa_cache_history_movement_monotonous : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : sa_good_linefill_inputt(initial_sa_cache),
            address          : addresst,
            i                : (LAMBDA (j:posnat):
                                 sa_cache_output_funct(initial_sa_cache,input)(j,address)`hit),
            pos              : wayt):
      FORALL (j : upfrom(i)):
      LET hit_input=LAMBDA (n:nat):
            sa_cache_hit_vector(sa_cache_config(initial_sa_cache,n,input),input(n)`address),
          k=the(sa_cache_hit_vector(sa_cache_config(initial_sa_cache,i,input),address)) IN
      (inv_hist_spec(i,input,hit_input)(address_line(address))(k)=0 AND
      inv_hist_spec(j,input,hit_input)(address_line(address))(k)>=pos+1 AND
        FORALL (l:subrange(i,j-1)): 
          NOT input(l)`clear AND 
          NOT (input(l)`linv AND input(l)`cache_rd AND 
               address_line(address)=address_line(input(l)`address) AND
               sa_cache_output_funct(initial_sa_cache,input)(l,input(l)`address)`hit AND
               the(sa_cache_hit_vector(sa_cache_config(initial_sa_cache,l,input),input(l)`address))=k)) IMPLIES
      EXISTS (l:subrange(i,j-1)):
        inv_hist_spec(l,input,hit_input)(address_line(address))(k)=pos AND
        input(l)`cache_rd AND 
        address_line(address)=address_line(input(l)`address) AND 
        NOT input(l)`linv AND %same line
        inv_hist_spec(l+1,input,hit_input)(address_line(address))(k)=pos+1 AND
        FORALL (j:(LAMBDA (way:wayt): 
                    inv_hist_spec(l,input,hit_input)(address_line(address))(way)<=
                    inv_hist_spec(l,input,hit_input)(address_line(address))(k))): 
          NOT dm_cache_output_funct(initial_sa_cache,input,j)(l,input(l)`address)`hit; %miss

  sa_cache_mru_to_pos_needs_pos_accesses : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : sa_good_linefill_inputt(initial_sa_cache),
            address          : addresst,
            i                : (LAMBDA (j:posnat):
                                 sa_cache_output_funct(initial_sa_cache,input)(j,address)`hit)):
      FORALL (pos            : wayt,
              j              : upfrom(i)):
      LET hit_input=LAMBDA (n:nat):
            sa_cache_hit_vector(sa_cache_config(initial_sa_cache,n,input),input(n)`address),
          k=the(sa_cache_hit_vector(sa_cache_config(initial_sa_cache,i,input),address)) IN
      (inv_hist_spec(i,input,hit_input)(address_line(address))(k)=0 AND
      inv_hist_spec(j,input,hit_input)(address_line(address))(k)=pos AND
        FORALL (l:subrange(i,j-1)): 
          NOT input(l)`clear AND 
          NOT (input(l)`linv AND input(l)`cache_rd AND 
               address_line(address)=address_line(input(l)`address) AND
               sa_cache_output_funct(initial_sa_cache,input)(l,input(l)`address)`hit AND
               the(sa_cache_hit_vector(sa_cache_config(initial_sa_cache,l,input),input(l)`address))=k)) IMPLIES
          EXISTS (f:[below(pos)->subrange(i,j-1)]):
            FORALL (x:below(pos)):
              (x=0 OR f(x)>f(x-1)) AND input(f(x))`cache_rd AND 
              address_line(address)=address_line(input(f(x))`address) AND 
              NOT input(f(x))`linv AND %same line
              inv_hist_spec(f(x)+1,input,hit_input)(address_line(address))(k)=x+1 AND
              FORALL (j:(LAMBDA (way:wayt): 
                          inv_hist_spec(f(x),input,hit_input)(address_line(address))(way)<=
                          inv_hist_spec(f(x),input,hit_input)(address_line(address))(k))): 
                NOT dm_cache_output_funct(initial_sa_cache,input,j)(f(x),input(f(x))`address)`hit; %miss
       
  sa_cache_mru_eviction_needs_K_accesses : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : sa_good_linefill_inputt(initial_sa_cache),
            address          : addresst,
            i                : (LAMBDA (j:posnat):
                                 sa_cache_output_funct(initial_sa_cache,input)(j,address)`hit),
            j              : upfrom(i)):
      LET hit_input=LAMBDA (n:nat):
            sa_cache_hit_vector(sa_cache_config(initial_sa_cache,n,input),input(n)`address),
          k=the(sa_cache_hit_vector(sa_cache_config(initial_sa_cache,i,input),address)) IN
      (inv_hist_spec(i,input,hit_input)(address_line(address))(k)=0 AND
      sa_cache_output_funct(initial_sa_cache,input)(j,address)`hit AND
      NOT sa_cache_output_funct(initial_sa_cache,input)(j+1,address)`hit AND
        NOT input(j)`clear AND 
        NOT (same_sect?(address,input(j)`address) AND %linv
             input(j)`vw AND NOT input(j)`valid) AND
        FORALL (l:subrange(i,j-1)): 
          NOT input(l)`clear AND 
          NOT (input(l)`linv AND input(l)`cache_rd AND 
               address_line(address)=address_line(input(l)`address) AND
               sa_cache_output_funct(initial_sa_cache,input)(l,input(l)`address)`hit AND
               the(sa_cache_hit_vector(sa_cache_config(initial_sa_cache,l,input),input(l)`address))=k)) IMPLIES
          EXISTS (f:[below(K)->subrange(i,j)]):
            FORALL (x:below(K)):
              (x=0 OR f(x)>f(x-1)) AND input(f(x))`cache_rd AND 
              address_line(address)=address_line(input(f(x))`address) AND 
              NOT input(f(x))`linv AND %same line
%              (x=K-1 OR inv_hist_spec(f(x)+1,input,hit_input)(address_line(address))(k)=x+1) AND
              FORALL (j:(LAMBDA (way:wayt): 
                          inv_hist_spec(f(x),input,hit_input)(address_line(address))(way)<=
                          inv_hist_spec(f(x),input,hit_input)(address_line(address))(k))): 
                NOT dm_cache_output_funct(initial_sa_cache,input,j)(f(x),input(f(x))`address)`hit; %miss

%
%
%
%
%

  sa_cache_hit_change_is_vw_or_clear : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt,
            input            : (LAMBDA (x:(good_input?)): 
                                  good_linefill_input?(sa_cache_out(initial_sa_cache,x))(x)),
            i                : posnat,
            j                : subrange(last_pred_before(input)(i),i-1)):
      LET out=sa_cache_out(initial_sa_cache,input) IN
      out(i)`hit /= out(j)`hit AND
        same_sect?(input(i)`address,input(j)`address) IMPLIES
        EXISTS (k:subrange(j,i-1)):
          input(k)`vw AND 
          input(k)`valid = out(i)`hit OR 
          input(k)`clear AND out(j)`hit;

  sa_cache_tw_creates_hit : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt,
            input            : (LAMBDA (x:(good_input?)): 
                                  good_linefill_input?(sa_cache_out(initial_sa_cache,x))(x)),
            i                : posnat):
      LET out=sa_cache_out(initial_sa_cache,input) IN
      input(i)`tw AND NOT input(i)`clear AND
        same_sect?(input(i)`address,input(i+1)`address) IMPLIES
        out(i+1)`hit;

  sa_cache_dirty_change_is_dw_or_vw_or_clear : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt,
            input            : (LAMBDA (x:(good_input?)): 
                                  good_linefill_input?(sa_cache_out(initial_sa_cache,x))(x)),
            i                : posnat):
      LET out=sa_cache_out(initial_sa_cache,input),
          last=last_pred_before(input)(i) IN
      same_sect?(input(i)`address,out(last)`ev_address) AND
      NOT input(last)`clear AND out(last)`dirty AND
      (FORALL (j:subrange(last+1,i-1)): 
        NOT input(j)`dw AND NOT input(j)`vw) IMPLIES
      out(i)`hit AND out(i)`dirty;

  sa_cache_keeps_dirty_hit : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt,
            input            : (LAMBDA (x:(good_input?)): 
                                  good_linefill_input?(sa_cache_out(initial_sa_cache,x))(x)),
            i                : posnat,
            j                : above(i)):
      LET out=sa_cache_out(initial_sa_cache,input) IN     
      same_sect?(input(i)`address,input(j)`address) AND
      input(i)`dw AND input(i)`dirty AND out(i)`hit AND
      NOT input(i)`vw AND NOT input(i)`clear AND
      (NOT out(j)`dirty OR NOT out(j)`hit) IMPLIES
        EXISTS (k:subrange(i+1,j-1)):
          LET last=last_pred_before(input)(k) IN
          input(k)`clear OR
          (input(k)`dw AND NOT input(k)`dirty OR
           input(k)`vw AND NOT input(k)`valid) AND
           (last <= i OR
            out(last)`hit AND out(last)`dirty AND 
              same_sect?(input(i)`address,input(k)`address) OR
            NOT out(last)`hit AND out(last)`dirty AND 
              same_sect?(out(last)`ev_address,input(i)`address));

    sa_cache_ev_address_on_hit_is_address : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt,
            input            : (good_input?),
            i                : posnat):
      LET out=sa_cache_out(initial_sa_cache,input) IN     
        out(i)`hit IMPLIES
          out(i)`ev_address=input(i)`address;

    sa_cache_continuous_hit : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt,
            input            : (LAMBDA (x:(good_input?)): 
                                 good_linefill_input?(sa_cache_out(initial_sa_cache,x))(x)),
            byte             : below(B),
            i                : posnat):
      LET out    =sa_cache_out(initial_sa_cache,input),
          address=input(i)`address IN
        (out(i)`hit IMPLIES    
          exists_last_pred?[cache_inputt,is_byte_write?(address,byte)](input)(i) AND
          LET last_bw=last_pred_before[cache_inputt,is_byte_write?(address,byte)](input)(i) IN
            last_bw>0 AND
            EXISTS (j:subrange(last_bw,i)):
              last_pred_before[cache_inputt,is_cache_rd?](input)(j)=
              last_pred_before[cache_inputt,is_cache_rd?](input)(last_bw) AND
              FORALL (k:subrange(last_bw,i)):
                (same_sect?(input(k)`address,address) IMPLIES
                 (out(k)`hit IFF k>=j)) AND 
                 (j<=k AND k<i IMPLIES 
                  NOT (input(k)`vw AND same_sect?(input(k)`address,address))) AND
                  (k<j-1 IMPLIES NOT input(k)`tw));

    sa_cache_create_hit_is_tw : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt,
            input            : (LAMBDA (x:(good_input?)): 
                                 good_linefill_input?(sa_cache_out(initial_sa_cache,x))(x)),
            i                : posnat,
            j                : above(i)):
      LET out=sa_cache_out(initial_sa_cache,input) IN     
        (same_sect?(input(i)`address,input(j)`address) AND
        (NOT out(i)`hit OR input(i)`vw AND NOT input(i)`valid) AND
         out(j)`hit IMPLIES
         EXISTS (k:subrange(i,j-1)):
           input(k)`tw AND same_sect?(input(k)`address,input(i)`address));

END sa_cache_liveness