%
% proof that the hit vector in a set associative cache
% stays unary given "good" input
%

sa_cache_correct[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

  cache    : LIBRARY = "../cache";
  history  : LIBRARY = "../history";

  IMPORTING 
    sa_cache[K,logK,a,t,l,s,B],
    cache@dm_cache_liveness[a,t,l,s,B],
    history@meets_spec[K,logK,LAMBDA (a:hit_vectort[K,logK]):
                              (# hit := encoderf_impl[logK,K](a)`or_tree,
                                 enc := encoderf_impl[logK,K](a)`encf_out #)];

  no_change_without_cache_rd : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : cache_input_funct, 
            i                : posnat):
    LET last      = last_pred_before(input)(i),
        old_cache = sa_cache_config(initial_sa_cache,last+1,input),
        cache     = sa_cache_config(initial_sa_cache,i     ,input) IN
      cache`history =old_cache`history AND
      cache`way_reg =old_cache`way_reg AND
      cache`hist_reg=old_cache`hist_reg;

  dm_cache_input_is_valid : PROPOSITION
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : cache_input_funct,
            way              : wayt):
      valid_function?(LAMBDA (n:nat):
      dm_cache_input(sa_cache_config(initial_sa_cache,n,input)`way_reg,input(n),way));

  dm_cache_input_funct(initial_sa_cache : sa_cache_configt, 
                       input:cache_input_funct,way:wayt):cache_input_funct =
    LAMBDA (n:nat):
      dm_cache_input(sa_cache_config(initial_sa_cache,n,input)`way_reg,input(n),way);

  sa_cache_output_funct(initial_sa_cache : sa_cache_configt, 
                        input:cache_input_funct):cache_output_funct =
    LAMBDA (n:nat,address:addresst):
      LET sa_cache=sa_cache_config(initial_sa_cache,n,input) IN
        (# 
           hit          := sa_cache_hit(sa_cache,address),
           dout         := sa_cache_dout(sa_cache,address),
           dirty        := sa_cache_dirty(sa_cache,address),
           ev_address   := sa_cache_ev_address(sa_cache,address)
         #);

  sa_cache_out_is_output : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt,
            input            : cache_input_funct):
    sa_cache_out(initial_sa_cache,input)=
    LAMBDA (n:nat):
      sa_cache_output_funct(initial_sa_cache,input)(n,input(n)`address);

  dm_cache_output_funct(initial_sa_cache : sa_cache_configt, 
                        input:cache_input_funct,way:wayt):cache_output_funct =
    LAMBDA (n:nat,address:addresst):
      LET dm_cache=sa_cache_config(initial_sa_cache,n,input)`way(way) IN
        (# 
           hit          := dm_cache_hit(dm_cache,address),
           dout         := dm_cache_dout(dm_cache,address),
           dirty        := dm_cache_dirty(dm_cache,address),
           ev_address   := dm_cache_ev_address(dm_cache,address)
         #);

  dm_cache_from_sa_cache : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input  : cache_input_funct,
            i      : nat,
            way    : wayt):
      sa_cache_config(initial_sa_cache,i,input)`way(way)=
        dm_cache_config(initial_sa_cache`way(way),i,dm_cache_input_funct(initial_sa_cache,input,way));

  dm_cache_output_funct_is_dm_cache_output : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input  : cache_input_funct,
            i      : nat,
            way    : wayt):
      dm_cache_output_funct(initial_sa_cache,input,way)=
        dm_cache_output(initial_sa_cache`way(way),dm_cache_input_funct(initial_sa_cache,input,way));

  sa_cache_hit_correct : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : cache_input_funct,
            address : addresst,
            i       : nat):
      sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit IFF
        EXISTS (way:wayt): 
          dm_cache_output_funct(initial_sa_cache,input,way)(i,address)`hit;

  sa_cache_miss_is_unary : PROPOSITION
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : cache_input_funct,
            address : addresst,
            i       : nat):
      NOT sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit IMPLIES
        unary?(sa_cache_hit_vector(sa_cache_config(initial_sa_cache,i,input),address));

  dm_cache_last_cache_rd_is_last_cache_rd : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : cache_input_funct,
            way     : wayt):
      LET dm_cache_input = dm_cache_input_funct(initial_sa_cache,input,way) IN
        last_pred_before[cache_inputt, is_cache_rd?](input)=
        last_pred_before[cache_inputt, is_cache_rd?](dm_cache_input);

  dm_cache_good_input : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input :(good_input?),
            way   : wayt):
      good_input?(dm_cache_input_funct(initial_sa_cache,input,way));

  sa_cache_sectoring : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input            : cache_input_funct, 
            address          : addresst,
            address2         : addresst,
            i                : nat):
      LET cache      = sa_cache_config(initial_sa_cache,i  ,input) IN
        same_sect?(address,address2) IMPLIES
          sa_cache_hit_vector(cache,address)=sa_cache_hit_vector(cache,address2) AND
          sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit=
            sa_cache_output_funct(initial_sa_cache,input)(i,address2)`hit;

  sa_cache_no_way_change_on_cache_rd : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            i       : nat):
      LET cache      = sa_cache_config(initial_sa_cache,i  ,input),
          next_cache = sa_cache_config(initial_sa_cache,i+1,input) IN
      input(i)`cache_rd AND NOT input(i)`clear IMPLIES
        cache`way=next_cache`way;

  sa_cache_no_way_change_after_last_clear : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            i       : posnat,
            j       : subrange(last_pred_before(input)(i)+1,i-1)):
      LET last      = last_pred_before(input)(i),
          cache     = sa_cache_config(initial_sa_cache,i,input),
          old_cache = sa_cache_config(initial_sa_cache,j,input) IN
      input(last)`clear IMPLIES
        cache`way=old_cache`way;

  sa_cache_no_hit_after_last_clear : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
    input(last_pred_before(input)(i))`clear IMPLIES
      NOT sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit;

  sa_cache_way_reg_half_correct : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   :(good_input?),
            i       :posnat):
      LET cache     = sa_cache_config(initial_sa_cache,i,input),
          last      = last_pred_before(input)(i),
          old_cache = sa_cache_config(initial_sa_cache,last, input) IN
        NOT input(last)`clear IMPLIES 
          IF sa_cache_output_funct(initial_sa_cache,input)
                                  (last,input(last)`address)`hit THEN
            cache`way_reg=
              sa_cache_hit_vector(old_cache,input(last)`address)
          ELSE
            EXISTS (ev:below(2^logK)) :
              cache`way_reg = LAMBDA (l:wayt): (l=ev)
          ENDIF;

  dm_cache_last_hit_is_last_hit : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            i       : posnat,
            way     : wayt):
      LET last      = last_pred_before(input)(i),
          cache     = sa_cache_config(initial_sa_cache,i   ,input),
          old_cache = sa_cache_config(initial_sa_cache,last,input) IN
        NOT input(last)`clear AND
          cache`way_reg(way) IMPLIES
          sa_cache_output_funct(initial_sa_cache,input)
                               (last,input(last)`address)`hit=
            dm_cache_output_funct(initial_sa_cache,input,way)(last,input(last)`address)`hit;

  sa_cache_way_reg_unary_after_unary_hit : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            i       : posnat):
      LET last      = last_pred_before(input)(i),
          cache     = sa_cache_config(initial_sa_cache,i   ,input),
          old_cache = sa_cache_config(initial_sa_cache,last,input),
          hit_vector= sa_cache_hit_vector(old_cache,input(last)`address) IN
        NOT input(last)`clear AND unary?(hit_vector) IMPLIES
          unary?(cache`way_reg);

  sa_cache_no_change_without_wayreg : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            way     : wayt,
            i       : posnat):
      LET cache     = sa_cache_config(initial_sa_cache,i  ,input),
          next_cache= sa_cache_config(initial_sa_cache,i+1,input) IN
      NOT cache`way_reg(way) AND NOT input(i)`clear IMPLIES
        cache`way(way)=next_cache`way(way);

  sa_cache_no_change_without_wayreg_ind : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            way     : wayt,
            i       : posnat):
      LET last      = last_pred_before(input)(i),
          cache     = sa_cache_config(initial_sa_cache,i   ,input),
          old_cache = sa_cache_config(initial_sa_cache,last,input) IN
        NOT input(last)`clear AND NOT cache`way_reg(way) IMPLIES
          cache`way(way)=old_cache`way(way);

  sa_cache_unary_hit_is_singleton0 : LEMMA
    FORALL (sa_cache : sa_cache_configt, 
            address  : addresst):
      LET hit_vector= sa_cache_hit_vector(sa_cache,address) IN
      unary?(hit_vector) AND
        sa_cache_hit(sa_cache,address) IMPLIES
        singleton?(hit_vector);

  sa_cache_unary_hit_is_singleton : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : nat):
      LET cache     = sa_cache_config(initial_sa_cache,i,input),
          hit_vector= sa_cache_hit_vector(cache,address) IN
      unary?(hit_vector) AND
        sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit IMPLIES
        singleton?(hit_vector);

  sa_cache_dout_correct_on_unary_hit0 : LEMMA
    FORALL (sa_cache : sa_cache_configt, 
            address  : addresst):
      LET hit_vector= sa_cache_hit_vector(sa_cache,address) IN
      unary?(hit_vector) AND
        sa_cache_hit(sa_cache,address) IMPLIES
        sa_cache_dout(sa_cache,address)=
          dm_cache_dout(sa_cache`way(the(hit_vector)),address);

  sa_cache_dout_correct_on_unary_hit : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
      LET cache     = sa_cache_config(initial_sa_cache,i,input),
          hit_vector= sa_cache_hit_vector(cache,address) IN
      unary?(hit_vector) AND
        sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit IMPLIES
        sa_cache_output_funct(initial_sa_cache,input)(i,address)`dout=
          dm_cache_output_funct(initial_sa_cache,input,the(hit_vector))(i,address)`dout;

  sa_cache_no_hit_vector_change_without_vw_or_tw : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
      LET cache     = sa_cache_config(initial_sa_cache,i,input),
          next_cache = sa_cache_config(initial_sa_cache,i+1,input) IN
      NOT input(i)`clear AND 
        NOT (input(i)`tw OR input(i)`vw) IMPLIES
          sa_cache_hit_vector(cache,address)=sa_cache_hit_vector(next_cache,address);

  sa_cache_no_way_change_without_vw_or_tw_or_dw_or_cdwb : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
      LET cache      = sa_cache_config(initial_sa_cache,i  ,input),
          next_cache = sa_cache_config(initial_sa_cache,i+1,input) IN
      NOT input(i)`clear AND 
        NOT (input(i)`vw OR input(i)`tw OR input(i)`dw OR EXISTS (l:below(B)):input(i)`cdwb(l)) IMPLIES
          cache`way=next_cache`way;

  sa_cache_no_way_change_without_vw_or_tw_or_dw_or_cdwb2 : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
      LET cache      = sa_cache_config(initial_sa_cache,i  ,input),
          next_cache = sa_cache_config(initial_sa_cache,i+1,input) IN
      NOT input(i)`clear AND 
        NOT (input(i)`vw OR input(i)`tw OR input(i)`dw OR EXISTS (l:below(B)):input(i)`cdwb(l)) IMPLIES
         sa_cache_hit_vector(cache,address)=sa_cache_hit_vector(next_cache,address) AND
         sa_cache_output_funct(initial_sa_cache,input)(i,address)`dout=
           sa_cache_output_funct(initial_sa_cache,input)(i+1,address)`dout;

  sa_cache_no_way_change_on_different_line : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
      LET cache      = sa_cache_config(initial_sa_cache,i  ,input),
          next_cache = sa_cache_config(initial_sa_cache,i+1,input) IN
       NOT input(i)`clear AND 
         address_line(address)/=address_line(input(i)`address) IMPLIES
         sa_cache_hit_vector(cache,address)=sa_cache_hit_vector(next_cache,address) AND
         sa_cache_output_funct(initial_sa_cache,input)(i,address)`dout=
           sa_cache_output_funct(initial_sa_cache,input)(i+1,address)`dout;

  sa_cache_no_way_change_on_different_line_ind : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
      LET last      = last_pred_before(input)(i),
          cache     = sa_cache_config(initial_sa_cache,i   ,input),
          old_cache = sa_cache_config(initial_sa_cache,last,input) IN
       NOT input(last)`clear AND 
         address_line(address)/=address_line(input(last)`address) IMPLIES
         sa_cache_hit_vector(cache,address)=sa_cache_hit_vector(old_cache,address) AND
         sa_cache_output_funct(initial_sa_cache,input)(i,address)`dout=
           sa_cache_output_funct(initial_sa_cache,input)(last,address)`dout;

  sa_cache_hit_change_on_different_tag_is_miss : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
      LET last      = last_pred_before(input)(i),
          cache     = sa_cache_config(initial_sa_cache,i   ,input),
          old_cache = sa_cache_config(initial_sa_cache,last,input) IN
       NOT input(last)`clear AND 
         address_tag(address)/=address_tag(input(last)`address) IMPLIES
         FORALL (way:wayt): 
           sa_cache_hit_vector(cache,address)(way) IMPLIES sa_cache_hit_vector(old_cache,address)(way);

  sa_cache_hit_vector_smaller_than_last_way_reg : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
      LET last      = last_pred_before(input)(i),
          cache     = sa_cache_config(initial_sa_cache,i     ,input),
          old_cache = sa_cache_config(initial_sa_cache,last+1,input) IN
       NOT input(last)`clear AND 
         same_sect?(address,input(last)`address) IMPLIES
         FORALL (way:wayt): 
           sa_cache_hit_vector(cache,address)(way) IMPLIES old_cache`way_reg(way);

  unary_preserve : LEMMA
    FORALL (hit_vector1 : hit_vectort,
            hit_vector2 : hit_vectort):
      (unary?(hit_vector1) AND  
        FORALL (way:wayt): 
           hit_vector2(way) IMPLIES hit_vector1(way)) IMPLIES
        unary?(hit_vector2);

% and now the different parts of the hit_stays_unary-proof 

% a predicate for better proofreading
  all_hit_vectors_unary?(cache:sa_cache_configt) : bool =
    FORALL (address:addresst) : 
      unary?(sa_cache_hit_vector(cache,address));

% a trivial conclosion from the fact that there is no hit after clear...
  sa_cache_hit_unary_after_clear: LEMMA
    FORALL (i:posnat, initial_sa_cache : sa_cache_configt, 
            input:(good_input?)):
      LET cache = sa_cache_config(initial_sa_cache,i,input) IN
      input(last_pred_before(input)(i))`clear IMPLIES 
        all_hit_vectors_unary?(cache);

% using the above lemmas about change on different line/tag,
% we easily get the induction step for different sect
  sa_cache_hit_stays_unary_on_different_sect : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
      LET last      = last_pred_before(input)(i),
          cache     = sa_cache_config(initial_sa_cache,i   ,input),
          old_cache = sa_cache_config(initial_sa_cache,last,input) IN
         NOT input(last)`clear AND
         NOT same_sect?(address,input(last)`address) AND
         unary?(sa_cache_hit_vector(old_cache,address)) IMPLIES
           unary?(sa_cache_hit_vector(cache,address));

% and now for the same tag/line:
% the hit vector stays smaller than the way reg which is already unary...
  sa_cache_hit_stays_unary_on_same_sect : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
      LET last      = last_pred_before(input)(i),
          cache     = sa_cache_config(initial_sa_cache,i   ,input),
          old_cache = sa_cache_config(initial_sa_cache,last,input) IN
         NOT input(last)`clear AND
         same_sect?(address,input(last)`address) AND
           unary?(sa_cache_hit_vector(old_cache,address)) IMPLIES
             unary?(sa_cache_hit_vector(cache,address));

% put it all together and you get...
  sa_cache_hit_stays_unary : COROLLARY 
    FORALL (initial_sa_cache : sa_cache_configt, 
            input:(good_input?), i:posnat):
      LET cache = sa_cache_config(initial_sa_cache,i,input) IN
        all_hit_vectors_unary?(cache);

% a few trivial corollaries
  sa_cache_hit_is_singleton : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
      LET cache     = sa_cache_config(initial_sa_cache,i,input),
          hit_vector= sa_cache_hit_vector(cache,address) IN
        sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit IMPLIES
        singleton?(hit_vector);

  sa_cache_hit_correct2 : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
      LET cache     = sa_cache_config(initial_sa_cache,i,input),
          hit_vector= sa_cache_hit_vector(cache,address) IN
      sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit IMPLIES
        FORALL (way:wayt): 
          dm_cache_output_funct(initial_sa_cache,input,way)(i,address)`hit IFF
            way=the(hit_vector);

  sa_cache_dout_correct : COROLLARY
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
      LET cache     = sa_cache_config(initial_sa_cache,i,input),
          hit_vector= sa_cache_hit_vector(cache,address) IN
        sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit IMPLIES
        sa_cache_output_funct(initial_sa_cache,input)(i,address)`dout=
          dm_cache_output_funct(initial_sa_cache,input,the(hit_vector))(i,address)`dout;

END sa_cache_correct