%
% correctness of the history
%

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

% predicates for better proofreading
  all_history_vectors_restricted?(cache:sa_cache_configt) : bool =
    FORALL (address:addresst):
      restricted_history_vectorp?(sa_cache_forward_mux(cache, address));

  all_history_vectors_bijective?(cache:sa_cache_configt) : bool =
    all_history_vectors_restricted?(cache) AND
    FORALL (address:addresst):
      permutation?(sa_cache_forward_mux(cache, address));

% specification of the history
  sa_cache_history_spect : TYPE = [linet -> (spec.permutation?)];

% one input of the history is the hit_vector
  hit_inputt : TYPE = [ nat -> hit_vectort ];

% and for the history implementation to meet its spec, 
% it should always be unary (safe for the 1st cycle)
  unary_hit_input?(hit_input:hit_inputt) : bool =
    FORALL (n:posnat) : unary?(hit_input(n));

% the sa_cache's hit_input is unary...
  sa_cache_hit_input_unary : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input:(good_input?)):
      LET hit_input=LAMBDA (n:nat):
            sa_cache_hit_vector(sa_cache_config(initial_sa_cache,n,input),input(n)`address) IN
      unary_hit_input?(hit_input);
    
  hist_spec(n:posnat, input:(good_input?), hit_input:(unary_hit_input?)) : 
    RECURSIVE sa_cache_history_spect =
    IF input(n-1)`clear THEN
      LAMBDA (i:linet) : 
        id[history_indext]
    ELSE
      LET address       =input(n-1)`address,
          history_vector=hist_spec(n-1,input, hit_input)(address_line(address)),
          hit_vector    =hit_input(n-1) IN
      IF input(n-1)`cache_rd THEN
        hist_spec(n-1,input,hit_input) WITH
        [ (address_line(address)):=
          next_history_permutation(history_vector,
                                   hit_vector,
                                   input(n-1)`linv)]
      ELSE
        hist_spec(n-1,input,hit_input)
      ENDIF
    ENDIF
  MEASURE n;

  ev(n:posnat, input:(good_input?), hit_input:(unary_hit_input?)) : history_indext =
    hist_spec(n,input,hit_input)(address_line(input(n)`address))(K-1);

  inv_id_is_id : LEMMA
    inverse(id[history_indext])=id[history_indext];

% specification of the inverse history
  sa_cache_inverse_history_spect : TYPE = [linet -> (spec.permutation?)];

  inv_hist_spec(n:posnat, input:(good_input?), hit_input:(unary_hit_input?)) :
    RECURSIVE sa_cache_inverse_history_spect =
    IF input(n-1)`clear THEN
      LAMBDA (i:linet) : 
        inverse(id[history_indext])
    ELSE
      LET address       =input(n-1)`address,
          history_vector=inv_hist_spec(n-1,input,hit_input)(address_line(address)),
          hit_vector    =hit_input(n-1) IN
      IF input(n-1)`cache_rd THEN
        inv_hist_spec(n-1,input,hit_input) WITH
        [ (address_line(address)):=
          inverse_next_history_permutation(history_vector,
                                           hit_vector,
                                           input(n-1)`linv)]
      ELSE
        inv_hist_spec(n-1,input,hit_input)
      ENDIF
    ENDIF
  MEASURE n;

  next_way_spec(n:posnat, input:(good_input?), 
                hit_input:(unary_hit_input?)) : wayt =
    IF NOT empty?(hit_input(n)) THEN
      the(hit_input(n))
    ELSE
      ev(n,input,hit_input)
    ENDIF;

  hist_spec_bijective : LEMMA
    FORALL (input:(good_input?), 
            hit_input:(unary_hit_input?), 
            i:posnat, 
            line:linet):
      permutation?(hist_spec(i,input,hit_input)(line));

  no_hist_spec_change_without_cache_rd_or_same_line :LEMMA
    FORALL (input     : (good_input?), 
            hit_input : (unary_hit_input?), 
            address   : addresst,
            i         : posnat):
      NOT input(i)`clear AND 
        (NOT input(i)`cache_rd OR 
          address_line(address)/=address_line(input(i)`address)) IMPLIES
      hist_spec(i,input,hit_input)(address_line(address))=
      hist_spec(i+1,input,hit_input)(address_line(address));

% inverse history
  sa_cache_inverse_history_correct : LEMMA
    FORALL (i         : posnat, 
            hit_input : (unary_hit_input?), 
            input     : (good_input?), address:addresst): 
      inv_hist_spec(i,input,hit_input)(address_line(address)) =
      inverse(hist_spec(i,input,hit_input)(address_line(address)));

  inv_hist_spec_bijective : LEMMA
    FORALL (input:(good_input?), 
            hit_input:(unary_hit_input?), 
            i:posnat, 
            line:linet):
      permutation?(inv_hist_spec(i,input,hit_input)(line));

% trivial corollary from the above 2 lemmas
  no_inv_hist_spec_change_without_cache_rd_or_same_line : COROLLARY
    FORALL (input     :(good_input?), 
            hit_input :(unary_hit_input?), 
            address   :addresst,
            i         :posnat):
      NOT input(i)`clear AND 
        (NOT input(i)`cache_rd OR 
          address_line(address)/=address_line(input(i)`address)) IMPLIES
      inv_hist_spec(i,input,hit_input)(address_line(address))=
      inv_hist_spec(i+1,input,hit_input)(address_line(address));

% and another one using "way_moves_lte_1_positions_forward"
  way_becomes_only_one_less_recently_used : COROLLARY
    FORALL (input     :(good_input?), 
            hit_input :(unary_hit_input?), 
            address   :addresst,
            way       :wayt,
            i         :posnat):
      NOT input(i)`clear AND 
        NOT input(i)`linv IMPLIES
      inv_hist_spec(i,input,hit_input)(address_line(address))(way)+1>=
      inv_hist_spec(i+1,input,hit_input)(address_line(address))(way);

% and another one using "way_moves_lte_1_positions_backward"
  way_becomes_only_one_more_recently_used : COROLLARY
    FORALL (input     :(good_input?), 
            hit_input :(unary_hit_input?), 
            address   :addresst,
            way       :wayt,
            i         :posnat):
      NOT input(i)`clear AND 
        input(i)`linv IMPLIES
      inv_hist_spec(i,input,hit_input)(address_line(address))(way)-1<=
      inv_hist_spec(i+1,input,hit_input)(address_line(address))(way);

% and another one using "hit_makes_most_recently_used"
  hit_makes_mru : COROLLARY
    FORALL (input     :(good_input?), 
            hit_input :(unary_hit_input?), 
            i         :posnat):
      input(i)`cache_rd AND
        NOT input(i)`clear AND 
          NOT input(i)`linv AND
            NOT empty?(hit_input(i)) IMPLIES
      inv_hist_spec(i+1,input,hit_input)(address_line(input(i)`address))(the(hit_input(i)))=0;

% and another one using "linv_hit_makes_least_recently_used"
  linv_hit_makes_lru : COROLLARY
    FORALL (input     :(good_input?), 
            hit_input :(unary_hit_input?), 
            i         :posnat):
      input(i)`cache_rd AND
        NOT input(i)`clear AND 
          input(i)`linv AND
            NOT empty?(hit_input(i)) IMPLIES
      inv_hist_spec(i+1,input,hit_input)(address_line(input(i)`address))(the(hit_input(i)))=K-1;

% and another one using "linv_miss_is_identity"
  linv_miss_is_id : COROLLARY
    FORALL (input     :(good_input?), 
            hit_input :(unary_hit_input?), 
            i         :posnat):
      input(i)`cache_rd AND
        NOT input(i)`clear AND 
          input(i)`linv AND
            empty?(hit_input(i)) IMPLIES
      inv_hist_spec(i+1,input,hit_input)(address_line(input(i)`address))=
      inv_hist_spec(i  ,input,hit_input)(address_line(input(i)`address));

% and another one using "only_hit_way_moves_backward"
  only_hit_way_moves_backward_in_history : COROLLARY
    FORALL (input     :(good_input?), 
            hit_input :(unary_hit_input?), 
            i         :posnat,
            way       : wayt):
      input(i)`cache_rd AND
        NOT input(i)`clear AND 
          NOT input(i)`linv AND
            NOT empty?(hit_input(i)) AND
      inv_hist_spec(i+1,input,hit_input)(address_line(input(i)`address))(way)<
      inv_hist_spec(i ,input,hit_input)(address_line(input(i)`address))(way) IMPLIES
        way=the(hit_input(i));

% and another one using "only_linv_hit_way_moves_forward"
  only_linv_hit_way_moves_forward_in_history : COROLLARY
    FORALL (input     :(good_input?), 
            hit_input :(unary_hit_input?), 
            i         :posnat,
            way       : wayt):
      input(i)`cache_rd AND
        NOT input(i)`clear AND 
          input(i)`linv AND
      inv_hist_spec(i+1,input,hit_input)(address_line(input(i)`address))(way)>
      inv_hist_spec(i ,input,hit_input)(address_line(input(i)`address))(way) IMPLIES
        NOT empty?(hit_input(i)) AND way=the(hit_input(i));

% ... using "no_change_behind_hit_way"
  no_hist_change_behind_hit_way : COROLLARY
    FORALL (input     :(good_input?), 
            hit_input :(unary_hit_input?), 
            i         :posnat):
      input(i)`cache_rd AND
        NOT input(i)`clear AND 
        NOT input(i)`linv AND
        NOT empty?(hit_input(i)) IMPLIES
          FORALL (j:history_indext):
            inv_hist_spec(i,input,hit_input)(address_line(input(i)`address))(j)>
            inv_hist_spec(i,input,hit_input)(address_line(input(i)`address))(the(hit_input(i))) IMPLIES
              inv_hist_spec(i+1,input,hit_input)(address_line(input(i)`address))(j)=
              inv_hist_spec(i  ,input,hit_input)(address_line(input(i)`address))(j);

% ... using "no_change_before_linv_hit_way"
  no_hist_change_before_linv_hit_way : COROLLARY
    FORALL (input     :(good_input?), 
            hit_input :(unary_hit_input?), 
            i         :posnat):
      input(i)`cache_rd AND
        NOT input(i)`clear AND 
        input(i)`linv AND
        NOT empty?(hit_input(i)) IMPLIES
          FORALL (j:history_indext):
            inv_hist_spec(i,input,hit_input)(address_line(input(i)`address))(j)<
            inv_hist_spec(i,input,hit_input)(address_line(input(i)`address))(the(hit_input(i))) IMPLIES
              inv_hist_spec(i+1,input,hit_input)(address_line(input(i)`address))(j)=
              inv_hist_spec(i  ,input,hit_input)(address_line(input(i)`address))(j);

%  hit_makes_mru : LEMMA
%    FORALL (initial_sa_cache : sa_cache_configt, 
%            input: (good_input?),
%            i    : posnat):
%    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 AND NOT input(i)`linv AND
%        sa_cache_output_funct(initial_sa_cache,input)(i,input(i)`address)`hit IMPLIES
%          inv_hist_spec(i+1,input,LAMBDA (n: nat):
%                       sa_cache_hit_vector(sa_cache_config(initial_sa_cache, n, input),
%                                           input(n)`address))
%           (address_line(input(i)`address))(the(sa_cache_hit_vector(cache,input(i)`address)))=0;

  history_vector_to_word_to_vector : LEMMA
    FORALL (vector: history_vectort):
      history_word_to_vector(history_vector_to_word(vector))=vector;

% history forwarding works correct
% i.e. if the history ram with adr_reg:=hist_reg
% corresponds to the history specification in every cycle
  history_forwarding_correct : THEOREM
    FORALL (initial_sa_cache : sa_cache_configt, 
            input:(good_input?), i:posnat):
      LET hit_input=LAMBDA (n:nat):
              sa_cache_hit_vector(sa_cache_config(initial_sa_cache,n,input),input(n)`address),
          cache    = sa_cache_config(initial_sa_cache,i,input) IN
    all_history_vectors_bijective?(cache) AND
    FORALL (address:addresst):
      hist_spec(i,input,hit_input)(address_line(address))=
        bv2nat[logK](sa_cache_forward_mux(cache, address));

% all history vectors remain permutations
% (a trivial corollary from the above
% lemma and theorem
%  sa_cache_history_permutation: COROLLARY
%    FORALL (i:posnat, input:(good_input?)): 
%    LET cache      = sa_cache_config(initial_sa_cache,i,  input) IN
%      all_history_vectors_bijective?(cache)

  sa_cache_hit_is_one_bit : LEMMA
    FORALL (i:posnat, initial_sa_cache : sa_cache_configt, 
            input:(good_input?), address:addresst): 
    LET cache      = sa_cache_config(initial_sa_cache,i,  input) IN
      sa_cache_output_funct(initial_sa_cache,input)(i, address)`hit
    IMPLIES
      EXISTS (l:wayt): 
        FORALL (j:wayt): sa_cache_hit_vector(cache, address)(j)=(l=j);

% the next way reg fuction is correct, i.e
% returns the unary representation of the way to be
% evicted in case of a miss or
% the unary representation of the hit way
% in case of a hit
%
  sa_cache_next_way_reg_correct: THEOREM
    FORALL (i:posnat, initial_sa_cache : sa_cache_configt, 
            input:(good_input?)): 
      LET cache      =sa_cache_config(initial_sa_cache,i,  input),
          hit_signal =sa_cache_hit(cache,input(i)`address),
          hit_input  =LAMBDA (n:nat):
            sa_cache_hit_vector(sa_cache_config(initial_sa_cache,n,input),input(n)`address) IN
      singleton?(next_way_reg(sa_cache_forward_mux(cache,input(i)`address),
                 sa_cache_hit_vector(cache, input(i)`address),hit_signal)) AND
      FORALL (l:history_indext):
        next_way_reg(sa_cache_forward_mux(cache,input(i)`address),
                     sa_cache_hit_vector(cache, input(i)`address),
                     hit_signal)(l)=
        IF sa_cache_output_funct(initial_sa_cache,input)(i,input(i)`address)`hit THEN
          sa_cache_hit_vector(cache,input(i)`address)(l)
        ELSE
          l=ev(i,input,hit_input)
        ENDIF;

% a trivial corollary from the above theorem:
% the way_reg contains the specified data
% clocked into it in the last cache_rd cycle
%
  sa_cache_way_reg_correct : COROLLARY
    FORALL (i:posnat, initial_sa_cache : sa_cache_configt, 
            input:(good_input?)): 
      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) IN
      NOT input(last)`clear
    IMPLIES
    LET cache     = sa_cache_config(initial_sa_cache,i   ,input),
        old_cache = sa_cache_config(initial_sa_cache,last,input) IN
      cache`way_reg =
        IF sa_cache_output_funct(initial_sa_cache,input)(last,input(last)`address)`hit THEN
          sa_cache_hit_vector(old_cache,input(last)`address)
        ELSE
          LAMBDA (l:history_indext):l=ev(last,input,hit_input)
        ENDIF;

  sa_cache_way_reg_is_singleton : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input: (good_input?),
            address:addresst,
            i    : posnat):
      sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit OR 
      NOT input(last_pred_before(input)(i))`clear OR
      (input(i)`vw OR input(i)`tw OR input(i)`dw OR EXISTS (l:below(B)):input(i)`cdwb(l)) IMPLIES
      singleton?(sa_cache_config(initial_sa_cache,i,input)`way_reg);
  
  sa_cache_vw_and_valid_create_hit : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
    input(i)`vw AND input(i)`valid AND NOT input(i)`clear AND
      same_sect?(address,input(i)`address) IMPLIES
      sa_cache_output_funct(initial_sa_cache,input)(i+1,address)`hit;
  
  sa_cache_miss_after_vw_not_valid : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
      input(i)`vw AND NOT input(i)`valid AND 
        same_sect?(address,input(i)`address) IMPLIES
        NOT sa_cache_output_funct(initial_sa_cache,input)(1+i,address)`hit;

  sa_cache_hit_is_last_wayreg : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt, 
            input   : (good_input?),
            address : addresst,
            i       : posnat):
      LET last=last_pred_before(input)(i),
          sa_cache=sa_cache_config(initial_sa_cache,i,input),
          last_sa_cache=sa_cache_config(initial_sa_cache,last+1,input) IN
      same_sect?(address,input(last)`address) AND
      sa_cache_output_funct(initial_sa_cache,input)(i,address)`hit IMPLIES
        last_sa_cache`way_reg=sa_cache_hit_vector(sa_cache,address);

  sa_cache_ev_address_correct : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt,
            input          : (good_input?),
            i              : posnat): 
      LET hit_input=LAMBDA (n:nat):
            sa_cache_hit_vector(sa_cache_config(initial_sa_cache,n,input),input(n)`address) IN
    sa_cache_output_funct(initial_sa_cache,input)(i,input(i)`address)`ev_address =
      IF sa_cache_output_funct(initial_sa_cache,input)(i,input(i)`address)`hit THEN
        dm_cache_output_funct(initial_sa_cache,input,the(hit_input(i)))(i,input(i)`address)`ev_address
      ELSE
        dm_cache_output_funct(initial_sa_cache,input,ev(i,input,hit_input))(i,input(i)`address)`ev_address
      ENDIF;

  sa_cache_dirty_correct : LEMMA
    FORALL (initial_sa_cache : sa_cache_configt,
            input          : (good_input?),
            i              : posnat): 
      LET hit_input=LAMBDA (n:nat):
            sa_cache_hit_vector(sa_cache_config(initial_sa_cache,n,input),input(n)`address) IN
    sa_cache_output_funct(initial_sa_cache,input)(i,input(i)`address)`dirty =
      IF sa_cache_output_funct(initial_sa_cache,input)(i,input(i)`address)`hit THEN
        dm_cache_output_funct(initial_sa_cache,input,the(hit_input(i)))(i,input(i)`address)`dirty
      ELSE
        dm_cache_output_funct(initial_sa_cache,input,ev(i,input,hit_input))(i,input(i)`address)`dirty
      ENDIF;

%  sa_cache_vw_and_valid_create_mru_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),
%        next_cache = sa_cache_config(initial_sa_cache,i+1,input) IN
%      input(i)`cache_rd AND NOT input(i)`clear AND NOT input(i)`linv AND
%        sa_cache_output_funct(initial_sa_cache,input)(i,input(i)`address)`hit IMPLIES
%          bv2nat(word2vector(sa_cache_forward_mux(next_cache,input(i)`address)))(0)=
%            the(sa_cache_hit_vector(cache,input(i)`address));

END sa_cache_history