%
% implementaion of a fully associative cache
% for a 2^a x 8*B memory using LRU replacement
% with K entries comprising 2^s sectors (in a RAM each)
%

fans_cache_correct[K:upfrom(2),
                   logK:posnat,
                   a:posnat,
                   B:posnat]: THEORY
BEGIN
  ASSUMING
    logK_is_logK: ASSUMPTION 
      2^(logK-1) < K AND K = 2^logK;
  ENDASSUMING
  
  IMPORTING
    fans_cache[K,logK,a,B],
    fas_cache_correct[K,logK,a,a,0,B]

% and now for the proof...
  fans_cache_is_fas_cache : LEMMA
    FORALL (initial_fa_cache : fa_cache_configt,
            input            : cache_input_funct,
            i                : nat):
      fans_cache_config(initial_fa_cache,i,input)=
      fa_cache_config(initial_fa_cache,i,input);
  
  fas_cache_out_is_fans_cache_out : LEMMA
    FORALL (initial_fa_cache : fa_cache_configt,
            input            : cache_input_funct):
    fans_cache_out(initial_fa_cache,input)=
      fa_cache_out(initial_fa_cache,input);
  
  fans_cache_io_consistency : LEMMA
    FORALL (initial_fa_cache : fa_cache_configt,
            input            : (LAMBDA (x:(good_input?)):
                                 good_linefill_input?(fans_cache_out(initial_fa_cache,x))(x))):
        cache_io_consistency?(fans_cache_out(initial_fa_cache,input),input);

END fans_cache_correct