tom_impl_spec_correct[(IMPORTING fpu_impl_ui_types)
	    fpu_spec_op : fpu_spec_op_t]: THEORY
BEGIN

  dlxalu : LIBRARY ="../dlxalu";
  fpu : LIBRARY = "../fpu";

%% this theory shows equality of the abstract VAMP implementation
%% where the black-boxed memory unit and fpus are replaced by their 
%% actual implementation with the concrete VAMP implementation

  IMPORTING tom_implementation,dlxalu@dlxalu_proof,
	    fpu@md_correct,fpu@add_correct,fpu@fpm_correct;

  TOMadd_clear : JUDGEMENT TOMadd HAS_TYPE add_circuit_t;
  TOMmd_clear  : JUDGEMENT TOMmd HAS_TYPE md_circuit_t;
  TOMfpm_clear : JUDGEMENT TOMfpm HAS_TYPE fpm_circuit_t;

  mif_next : mif_next_t = ext_pipe_impl_next_conf_nc;

%% use the proper parameters for the abstract VAMP implementation
%% such that we can show equality to the concrete version

  IMPORTING tom_impl_spec[TOMadd,TOMmd,TOMfpm,
			  mif_next,
			  fpu_spec_op];

%% dozens of f_spec=f lemmas stating equality of abstract and concrete
%% versions
  signals4_rewrite : LEMMA
  signals4_spec=signals4;

  arbiter_impl5_rewrite : LEMMA
    arbiter_impl_spec[no_fu]=arbiter_impl[no_fu];

  arbiter_impl4_rewrite : LEMMA
    arbiter_impl_spec[4]=arbiter_impl[4];

  signals3_rewrite : LEMMA
    signals3_spec=signals3;

  alu_step_rewrite : LEMMA
    tomalu_step_spec=tomalu_step;

  SPR_next_rewrite : LEMMA
    SPR_next_spec=SPR_next;

  rob_step_rewrite : LEMMA
    rob_step_spec=rob_step;

  prod_step5_rewrite : LEMMA
    prod_step5_spec=prod_step[5];

  prod_step4_rewrite : LEMMA
    prod_step4_spec=prod_step[4];

  arbiter_step5_rewrite : LEMMA
    arbiter_step_spec[no_fu]=arbiter_step[no_fu];

  arbiter_step4_rewrite : LEMMA
    arbiter_step_spec[4]=arbiter_step[4];

  tomrf_rewrite : LEMMA
    tomrf_spec=tomrf;

  tomsourceops_rewrite : LEMMA
    tomsourceops_spec=tomsourceops;

  rs_step_rewrite : LEMMA
    rs_step_spec=rs_step;

  fpu1_step_rewrite : LEMMA
    tomfpu1_step_ui=tomfpu1_step;

  fpu2_step_rewrite : LEMMA
    tomfpu2_step_ui=tomfpu2_step;

  fpu3_step_rewrite : LEMMA
    tomfpu3_step_ui=tomfpu3_step;

  fpu1_stallout_rewrite : LEMMA
    tomfpu1_stallout_ui=tomfpu1_stallout;

  fpu2_stallout_rewrite : LEMMA
    tomfpu2_stallout_ui=tomfpu2_stallout;

  fpu3_stallout_rewrite : LEMMA
    tomfpu3_stallout_ui=tomfpu3_stallout;

  signals2_rewrite : LEMMA
    signals2_spec=signals2;

  signals1_rewrite : LEMMA
    signals1_spec=signals1;

  tommem_step_rewrite : LEMMA
    tommem_step_ui=tommem_step;

  signals0_rewrite : LEMMA
    signals0_spec=signals0;

%% and the final lemma, i.e., the synthesized tom_step function
%% equals the abstract tom_step_spec used in the tom_correct*-theories

  tom_impl_spec_correct : THEOREM
    tom_step=tom_step_spec;

%% and the recursive version of the actual implementation state

  vamp_conf(init_conf: tom_conft, input:tom_impl_input_funct,n:nat):RECURSIVE tom_conft=
    IF n=0 THEN
      init_conf
    ELSE
      tom_step(vamp_conf(init_conf,input,n-1),
		      input(n-1)`reset,
		      input(n-1)`ext_in,
		      input(n-1)`ext_reset,
		      input(n-1)`bp_in)`conf
    ENDIF
    MEASURE n;

  vamp_out(init_conf: tom_conft, input:tom_impl_input_funct)(n:nat):tom_impl_outputt=
    LET next=tom_step(vamp_conf(init_conf,input,n),
		      input(n)`reset,
		      input(n)`ext_in,
		      input(n)`ext_reset,
		      input(n)`bp_in) IN
	(# ext_out := next`ext_out,
	   bp_out  := next`bp_out #);

%% the trivial inductive equality of concrete and abstract states

  vamp_equals_impl_spec : THEOREM
    FORALL (init_conf: tom_conft, input:tom_impl_input_funct,T:nat):
      vamp_conf(init_conf,input,T)=tom_impl_conf(init_conf,input,T);

%% and some helpers about initial configurations

  initial_vamp_conf_after_ext_reset : LEMMA
    FORALL (init_conf: tom_conft, input:tom_impl_inputt):
      LET conf=tom_step(init_conf,TRUE,input`ext_in,TRUE,input`bp_in)`conf IN
	initial_vamp_conf?(conf) AND
	NOT conf`S3`mem`inst`rollback AND
	conf`S2`PCp = SISRnext AND
	conf`S2`DPC = SISR AND
	conf`S5`SPR = LAMBDA(x:upto(nspr_LAST)):
		        IF x=nspr_ECA THEN r1 ELSE r0 ENDIF;

  initial_vamp_conf_stays_after_reset : LEMMA
    FORALL (init_conf: tom_conft, input:tom_impl_inputt):
     (initial_vamp_conf?(init_conf) AND
      NOT init_conf`S3`mem`inst`rollback AND
      init_conf`S2`PCp = SISRnext AND
      init_conf`S2`DPC = SISR AND
      init_conf`S5`SPR = LAMBDA(x:upto(nspr_LAST)):
		           IF x=nspr_ECA THEN r1 ELSE r0 ENDIF)
	IMPLIES
      LET conf=tom_step(init_conf,TRUE,input`ext_in,input`ext_reset,input`bp_in)`conf IN
	initial_vamp_conf?(conf) AND
	NOT conf`S3`mem`inst`rollback AND
	conf`S2`PCp = SISRnext AND
	conf`S2`DPC = SISR AND
	conf`S5`SPR = LAMBDA(x:upto(nspr_LAST)):
		        IF x=nspr_ECA THEN r1 ELSE r0 ENDIF;

  initial_vamp_conf_lemma : LEMMA
    FORALL (init_conf: tom_conft, 
	    input:tom_impl_input_funct,
	    last_reset : nat):
    (FORALL (T:nat):input(T)`ext_reset=(T=0)) AND
    (FORALL (T:nat):input(T)`reset=(T<=last_reset)) IMPLIES
      FORALL (T:upto(last_reset)):
	LET conf=vamp_conf(init_conf,input,T+1) IN
	  initial_vamp_conf?(conf) AND
	  NOT conf`S3`mem`inst`rollback AND
	  conf`S2`PCp = SISRnext AND
	  conf`S2`DPC = SISR AND
	  conf`S5`SPR = LAMBDA(x:upto(nspr_LAST)):
		          IF x=nspr_ECA THEN r1 ELSE r0 ENDIF;

%% derive the actual memory und memory interface input

  vamp_mem_input(conf:tom_conft,
		 input:tom_impl_inputt):tommem_inputt =
    LET s4  =signals4(conf`S4,conf`S5`SPR(nspr_SR),input`reset),
        s3  =signals3(conf`S3),
        s2  =signals2(conf`S3, conf`S2, input`reset, s3, s4`clear),
        s1  =signals1(conf`S1, conf`S2, conf`S4, conf`S5,input`reset,s3, s4),
        g_0DPC=IF s1`full_1 THEN s1`nextDPC ELSE conf`S2`DPC ENDIF IN
	(# clear    := s4`clear,
           stall_in := s3`FU_stall_in(fu_mem),
           inputs   := s2`fu_inputs(fu_mem),
           PC       := g_0DPC,
           ROBtail  := conf`S4`ROBhead,
           bp_in    := input`bp_in,
           ext_in   := input`ext_in,
           ext_reset:= input`ext_reset #);

  mif_input(mem:mem_reg,input:tommem_inputt):ext_control_with_caches_inputt=
    (# memory_output := input`bp_in,
       ext_memory_interface_output :=
	(# data := 
                 (# mr := mem`inst`valid AND NOT mem`inst`I_s AND 
		   	  NOT mem`inst`dmal AND NOT mem`inst`stalled OR
                          mem`inst`rollback AND NOT mem`inst`I_s,
                    mw := mem`inst`valid AND mem`inst`I_s AND 
			  NOT mem`inst`dmal AND NOT mem`inst`stalled AND
                          mem`inst`storing OR
                          mem`inst`rollback AND mem`inst`I_s,
                    address := mem`inst`EA ^ (31, 3),
                          dout := mem`inst`data,
                          mbw := mem`inst`mwb 
                  #),
           data2 := input`ext_in,
           inst  := 
                  (# mr := NOT (input`PC(1) OR input`PC(0)) OR
			    mem`istalled, 
                     address := IF mem`istalled THEN
				 mem`mPC
			       ELSE
				 input`PC ^ (31, 3)
			       ENDIF 
                   #),
	   clear := input`ext_reset
	#)
    #);

  mif_inputt(init_conf: tom_conft,
	     input    : tom_impl_input_funct): [nat->ext_control_with_caches_inputt]=
    LAMBDA (n:nat):
      LET conf=vamp_conf(init_conf,input,n) IN
	mif_input(conf`S3`mem,vamp_mem_input(conf,input(n)));

%% and another trivial induction showing that the memory interface in
%% the VAMP implementation is equal to a stand-alone memory interface
%% that is fed with the memory input the VAMP produces

  mif_helper : LEMMA
    FORALL (conf  : tom_conft,
	    input : tom_impl_inputt):
      tom_step(conf,input`reset,input`ext_in,input`ext_reset,input`bp_in)`conf`S3`mem`mif=
	ext_pipe_impl_next_conf_nc(conf`S3`mem`mif,mif_input(conf`S3`mem,vamp_mem_input(conf,input)))`next_conf;

  tommem_conf_is_vamp_conf_mem : LEMMA
    FORALL (init_conf:tom_conft,
	    input:tom_impl_input_funct,
	    T:nat):
      tommem_conf(init_conf`S3`mem,T,LAMBDA (n:nat):vamp_mem_input(vamp_conf(init_conf,input,n),input(n)))=
	vamp_conf(init_conf,input,T)`S3`mem;

END tom_impl_spec_correct