% % correctness of the history computation % % $Id: meets_spec.pvs,v 1.9 2001/07/09 09:09:49 sbeyer Exp $ % % $Log: meets_spec.pvs,v $ % Revision 1.9 2001/07/09 09:09:49 sbeyer % * now using arrays for history_vector (since it is supported by pvs2hdl) % % Revision 1.8 2001/05/21 13:31:39 sbeyer % added f***uing actuals for initial_history % % Revision 1.7 2001/05/21 12:56:33 sbeyer % added lemma way_moves_lte_1_positions_backward and fixed some unexplainable (non-existent?) errors % % Revision 1.6 2001/05/03 13:43:23 sbeyer % lifted the way-reg prrofs from bitwise equality to function equality % for next_way_reg_correct, the hit vector need no longer be unary % % Revision 1.5 2001/04/03 12:56:20 sbeyer % fixed f***ing typo in lemma name % % Revision 1.4 2001/04/03 09:41:02 sbeyer % % added pseudo-trivial lemmas about initial and next history % % Revision 1.3 2001/03/23 13:47:59 sbeyer % added 2 predicates for better proof reading (using subtyping now) % % Revision 1.2 2001/03/22 10:52:30 sbeyer % finally, all proof goals are 'proved complete' % % Revision 1.1 2001/03/09 13:31:33 sbeyer % *** empty log message *** % meets_spec[K : upfrom(2), logK : posnat, (IMPORTING implementation[K,logK]) hit_and_enc : [bvec[K]->[# hit : bit, enc : bvec[logK] #]]]: THEORY BEGIN ASSUMING logK_is_logK: ASSUMPTION 2^(logK-1) < K AND K <= 2^logK; hit_correct : ASSUMPTION FORALL (hit_vector:bvec[K]): hit_and_enc(hit_vector)`hit = EXISTS(i:below(K)):hit_vector(i); enc_correct : ASSUMPTION FORALL (hit_vector:(singleton?[below(K)])): bv2nat(hit_and_enc(hit_vector)`enc) = the(hit_vector); ENDASSUMING IMPORTING spec[K,logK] restricted_history_datap?(a:history_datat) : bool = bv2nat[logK](a)restricted_history_datat]= % LAMBDA (i:history_indext):history_vector^((i+1)*logK-1,i*logK); % permutation?(history_vector:restricted_history_vectort) : bool = bijective?[history_indext, restricted_history_datat](history_vector); permutation_heler : JUDGEMENT (permutation?) SUBTYPE_OF [history_indext -> restricted_history_datat]; restricted_bv2nat(history_data:restricted_history_datat) : history_indext= bv2nat[logK](history_data); restricted_nat2bv(history_index:history_indext) : restricted_history_datat= nat2bv[logK](history_index); restricted_bv2nat_bij : LEMMA bijective?[restricted_history_datat,history_indext](restricted_bv2nat); restricted_nat2bv_bij : LEMMA bijective?[history_indext,restricted_history_datat](restricted_nat2bv); restricted_bv2nat_helper : LEMMA restricted_bv2nat=restrict[history_datat,restricted_history_datat,below(2^logK)](bv2nat[logK]); restricted_nat2bv_helper : LEMMA restricted_nat2bv=restrict[below(2^logK),history_indext,history_datat](nat2bv[logK]); hit_not_empty : JUDGEMENT (LAMBDA (x:hit_vectort):hit_and_enc(x)`hit) SUBTYPE_OF (NOT empty?[history_indext]); not_empty_hit : JUDGEMENT (NOT empty?[history_indext]) SUBTYPE_OF (LAMBDA (x:hit_vectort):hit_and_enc(x)`hit); not_hit_empty : JUDGEMENT (LAMBDA (x:hit_vectort): NOT hit_and_enc(x)`hit) SUBTYPE_OF (empty?[history_indext]); empty_not_hit : JUDGEMENT (empty?[history_indext]) SUBTYPE_OF (LAMBDA (x:hit_vectort):NOT hit_and_enc(x)`hit); unary_encode : LEMMA FORALL (hit_vector:(singleton?[below(K)])): restricted_history_datap?(hit_and_enc(hit_vector)`enc); restricted_bv2nat_helper2 : LEMMA FORALL (hit_vector:(singleton?[below(K)])): LET hit_vector_binary=hit_and_enc(hit_vector)`enc IN restricted_bv2nat(hit_vector_binary)=bv2nat(hit_vector_binary); perm_impl_is_perm_spec : LEMMA FORALL (history_vector:(permutation?)): spec.permutation?(bv2nat[logK] o history_vector); perm_spec_is_perm_impl : LEMMA FORALL (history_vector:(LAMBDA (x:restricted_history_vectort) : spec.permutation?(bv2nat[logK] o x))): permutation?(history_vector); compute_hit : LEMMA FORALL (hit_vector:(singleton?[history_indext])): the(hit_vector) = bv2nat[logK](hit_and_enc(hit_vector)`enc); inv_hist_helper : LEMMA FORALL (history_vector : (permutation?), x : restricted_history_datat): history_vector(inverse(history_vector)(x))=x; inv_helper1 : LEMMA FORALL (history_vector : (permutation?)): o[history_indext,restricted_history_datat,history_indext](restricted_bv2nat, history_vector) o inverse[history_indext,restricted_history_datat](history_vector) o inverse[restricted_history_datat,history_indext](restricted_bv2nat)=identity[history_indext]; inv_helper : LEMMA FORALL (history_vector : (permutation?)): inverse[history_indext,history_indext](o[history_indext,restricted_history_datat,history_indext](restricted_bv2nat,history_vector))= (inverse[history_indext,restricted_history_datat](history_vector) o inverse[restricted_history_datat,history_indext](restricted_bv2nat)); % pp-input-correct pp_input_correct : LEMMA FORALL (history_vector : (permutation?), hit_vector : (unary?), i : history_indext): LET hit_signal =hit_and_enc(hit_vector)`hit, hit_vector_binary=hit_and_enc(hit_vector)`enc, hit_index =inverse(history_vector)(hit_vector_binary), eq =equal_impl[logK](history_vector(i), hit_vector_binary) IN (eq AND hit_signal) = IF NOT hit_signal THEN FALSE ELSE i=hit_index ENDIF; % hsel-input-correct hsel_input_correct : LEMMA FORALL (history_vector : (permutation?), hit_vector : (unary?), i : history_indext): LET hit_signal = hit_and_enc(hit_vector)`hit, hit_vector_binary = hit_and_enc(hit_vector)`enc, hit_index = inverse(history_vector)(hit_vector_binary) IN hsel_input[K,logK](history_vector,hit_vector_binary,hit_signal)(i)= IF NOT hit_signal THEN FALSE ELSE i>=hit_index ENDIF; % a-mux-correct hsel_a_mux_correct: LEMMA FORALL (history_vector : (permutation?), hit_vector : (unary?)): LET hit_signal = hit_and_enc(hit_vector)`hit, hit_vector_binary = hit_and_enc(hit_vector)`enc, hit_index = inverse(history_vector)(hit_vector_binary) IN hsel_a_mux[K,logK](ev(history_vector),hit_vector_binary,hit_signal)= IF NOT hit_signal THEN ev(history_vector) ELSE history_vector(hit_index) ENDIF; % b-mux-correct hsel_b_mux_correct: LEMMA FORALL (history_vector : (permutation?), hit_vector : (unary?)): LET hit_signal = hit_and_enc(hit_vector)`hit, hit_vector_binary = hit_and_enc(hit_vector)`enc, hit_index = inverse(history_vector)(hit_vector_binary), pp_output = hsel_input[K,logK](history_vector,hit_vector_binary,hit_signal) IN hsel_b_mux[K,logK](pp_output,history_vector)= LAMBDA (i:below(K-1)): history_vector(IF i>=hit_index AND hit_signal THEN i+1 ELSE i ENDIF); initial_history_restricted : JUDGEMENT initial_history_vector[K,logK] HAS_TYPE restricted_history_vectort; next_history_restricted : LEMMA FORALL (history_vector:restricted_history_vectort, hit_vector:(unary?), linv : bit): restricted_history_vectorp?(next_history_vector(history_vector, hit_vector, hit_and_enc(hit_vector)`enc, hit_and_enc(hit_vector)`hit, linv)); initial_history_meets_spec : LEMMA id[history_indext]= bv2nat[logK](initial_history_vector[K,logK]); next_history_meets_spec0 : THEOREM FORALL (history_vector : (permutation?), hit_vector : (unary?), linv : bit, history_index : history_indext): LET hit_signal = hit_and_enc(hit_vector)`hit, hit_vector_binary = hit_and_enc(hit_vector)`enc IN next_history_permutation(o[history_indext,restricted_history_datat,history_indext](restricted_bv2nat,history_vector), hit_vector, linv)(history_index)= bv2nat[logK](next_history_vector[K,logK](history_vector, hit_vector, hit_vector_binary, hit_signal, linv)(history_index)); next_history_meets_spec : COROLLARY FORALL (history_vector : (permutation?), hit_vector : (unary?), linv : bool): LET hit_signal = hit_and_enc(hit_vector)`hit, hit_vector_binary = hit_and_enc(hit_vector)`enc IN next_history_permutation(o[history_indext,restricted_history_datat,history_indext](restricted_bv2nat,history_vector), hit_vector, linv)= bv2nat[logK](next_history_vector[K,logK](history_vector, hit_vector, hit_vector_binary, hit_signal, linv)); initial_history_bijective : LEMMA restricted_history_vectorp?(initial_history_vector[K,logK]) AND permutation?(initial_history_vector[K,logK]); next_history_bijective : COROLLARY FORALL (history_vector : (permutation?), hit_vector : (unary?), linv : bool): LET hit_signal = hit_and_enc(hit_vector)`hit, hit_vector_binary = hit_and_enc(hit_vector)`enc, next_history = next_history_vector[K,logK](history_vector, hit_vector, hit_vector_binary, hit_signal, linv) IN restricted_history_vectorp?(next_history) AND permutation?(next_history); % next_way_reg returns a bitvector with exactly one bit active: % it's the active bit of the hit vector in case of a hit, % else it's the number of the way to be evicted next_way_reg_meets_spec : THEOREM FORALL (history_vector : (permutation?), hit_vector : (unary?)): next_way_reg[K,logK](history_vector, hit_vector, hit_and_enc(hit_vector)`hit)= LAMBDA (i:history_indext): i=next_way_reg_spec(bv2nat[logK] o history_vector,hit_vector); % for the following lemma, neither the history vector % needs to be bijective nor the hit vector unary next_way_reg_correct : THEOREM FORALL (history_vector : history_vectort, hit_vector : hit_vectort): LET hit_signal = hit_and_enc(hit_vector)`hit IN next_way_reg[K,logK](history_vector,hit_vector,hit_signal)= IF hit_signal THEN hit_vector ELSE LAMBDA (i:history_indext) : i=bv2nat[logK](ev(history_vector)) ENDIF; % simple corollary next_way_reg_unary : COROLLARY FORALL (history_vector : history_vectort, hit_vector : (unary?)): unary?(next_way_reg[K,logK](history_vector, hit_vector, hit_and_enc(hit_vector)`hit)); END meets_spec