tom_correct[(IMPORTING fpu_impl_ui_types,cache_mem_impl_types)
	    fpu_spec_op : fpu_spec_op_t,
	    TOMadd : add_circuit_t,
	    TOMmd  : md_circuit_t,
	    TOMfpm : fpm_circuit_t,
	    mif_next:mif_next_t,
	    (IMPORTING tom_impl_spec[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op])
	    init_conf:dlx_conft]: THEORY
BEGIN

  tomasulo: LIBRARY = "../tomasulo";

  IMPORTING tomasulo@tomspecconf[no_reg];

%% proof step 1:
%% show the equality of VAMP specification (dlx_conf) WITHOUT INTERRUPTS 
%% and Tomasulo specification (cS) by Daniel

% and now for the grand proof...
% we want to apply Daniel's Tomasulo proof to the VAMP and its specification in dlxifspex
% however, Daniel verifies his Tomasulo implementation against a local in-order specification called cS
% this cS only contains one large register file and writes to r0 are ignored!
% so the first step is to define cS in such a way that in reflects VAMP behaviour 
% and then show that this cS equals dlxifspec in some way...

% the mapping function between cS-configurations and dlx-configuration
  map_cSR(dlx_conf: dlx_conft):cSt=
  (# R :=
    LAMBDA (r:regnot):
    COND
    r<32           -> LET x=nat2bv[5](r)    IN dlx_conf`GPR(x),
    r>=32 AND r<48 -> LET x=nat2bv[4](r-32) IN dlx_conf`FPRl(x),
    r>=48 AND r<64 -> LET x=nat2bv[4](r-48) IN dlx_conf`FPRh(x),
    ELSE           -> LET x=nat2bv[5](r-64) IN dlx_conf`SPR(x)
    ENDCOND #);

% we derive the initial cS-configuration from the initial dlx-configuration
  cSinitial: cSt = map_cSR(init_conf);

% cs is generated in the Tomasulo proof locally by some inputs:
% functions specifying an
% instructions source- and  destination registers and its result
% cS expects these as functions on nats
% we define these functions first as functions on the instruction word
% (or on the whole dlx configuration in case of the result function)
% the nat-version of these functions is easily derived by generating 
% the n-th instruction word using the n-th dlx configuration...

% the source register function is directly derived from tomIA which is
% actually implemented in the VAMP
  cSS: [registert, st->regnot] =
    LAMBDA (Iw: registert, s:st): 
    LET IA=tomIA(tomID(Iw)) IN
    IF IA`sop(s)`gpr THEN
      bv2nat(IA`sop(s)`A)
    ELSIF IA`sop(s)`fprl THEN
      bv2nat(IA`sop(s)`A^(4,1))+32
    ELSIF IA`sop(s)`fprh THEN
      bv2nat(IA`sop(s)`A^(4,1))+48
    ELSIF IA`sop(s)`spr THEN
      bv2nat(IA`sop(s)`A)+64
    ELSE
      0
    ENDIF;

% the timed version as input to Daniel's cS
  cSS_t: [mathmtimet, st->regnot] =
    LAMBDA (i: mathmtimet, s:st): 
    cSS(Iw(dlx_conf_without_interrupt_IEEEf(init_conf,i)),s);

% the same for the destination registers
% we support 4 destination registers: 2 for fp-double-precision,
% and 2 further registers for CA and EData (that are simply written to
% register 0, that is not at all)
  cSD: [registert, dt->regnot] =
    LAMBDA (Iw: registert, d: dt): 
    LET IA=tomIA(tomID(Iw)) IN
    COND 
      d=0 -> IF IA`dest`gpr THEN
        	bv2nat(IA`dest`A)
       	     ELSIF IA`dest`fprl THEN
      		bv2nat(IA`dest`A^(4,1))+32
      	     ELSIF IA`dest`spr THEN
      		bv2nat(IA`dest`A)+64
      	     ELSE
      		0
      	     ENDIF,
      d=1 -> IF IA`dest`fprh THEN
      		bv2nat(IA`dest`A^(4,1))+48
       	     ELSE
		0
	     ENDIF,
      ELSE-> 0	% exception results written to register 0 - that is not at all!
    ENDCOND;

  cSD_t: [mathmtimet, dt->regnot] =
    LAMBDA (i: mathmtimet, d: dt): 
    cSD(Iw(dlx_conf_without_interrupt_IEEEf(init_conf,i)),d);

% and the result... also computes correct causes and EData!
  cSresult: [dlx_conft->resultt] =
    LAMBDA (dlx_conf: dlx_conft): 
      LET Iw =Iw(dlx_conf),
	  src_op=LAMBDA (s:st): source(map_cSR(dlx_conf),cSS(Iw,s)) IN
    	LAMBDA (d: dt): 
	  COND d<2 -> IF I_is_alu(Iw) THEN
			LET op2=IF I_ALU(Iw) OR I_shift(Iw) THEN
                	    	  src_op(2)
              			ELSE
                		  I_immediate(Iw)
              			ENDIF IN
			  ALUf_spec(src_op(0),op2,ALUfunction(Iw))`result
		      ELSIF ((I_j(Iw) OR I_jr(Iw)) AND I_link(Iw)) AND d=0 THEN
			dlx_conf`PCp+r4
		% branch and jump dont need a result, but the proof is
		% simplified by it
		      ELSIF (I_branch(Iw) OR I_j(Iw) OR I_jr(Iw) OR 
			     I_movs2i(Iw) OR I_movi2s(Iw) OR I_rfe(Iw)) AND d=0 THEN
			src_op(0)
		% in case of an interrupt, the memory return value is in fact dont care,
		% therefore r0 is specified (in the ELSE case a few lines down)
		      ELSIF I_mem(Iw) AND (I_load(Iw) OR I_fload(Iw)) THEN			  
			dmem_spec_load(dlx_conf`mem,op1(dlx_conf),Iw)^(31+32*d,32*d)
		      ELSIF I_mf2i(Iw) OR I_mi2f(Iw) OR I_fpu(Iw) OR
			    I_fcond(Iw) THEN
			LET fpu_ret = fpu_spec(src_op(1) o src_op(0),
				   	src_op(3) o src_op(2),
				   	src_op(4)^(1,0),
				   	src_op(5)^(12,7),
				   	Iw) IN
			  IF fpu_ret`double THEN
			    fpu_ret`result^(31+32*d,32*d)
			  ELSE
			    fpu_ret`result^(63,32)
			  ENDIF
		      ELSE
			r0
		      ENDIF,
	       d=2 -> CA(dlx_conf),
	       d=3 -> EData(dlx_conf)
	  ENDCOND;

  cSresult_t: [mathmtimet->resultt] =
    LAMBDA (i: mathmtimet): 
      cSresult(dlx_conf_without_interrupt_IEEEf(init_conf,i));

% and the mysterious embedding function that is later really reflected in hadware...
  cSe: [regnot->dt] =
    LAMBDA (r:regnot):
      IF r>=48 AND r<64 THEN 1 ELSE 0 ENDIF;

  cSspec: cSspect =
    (#
      initial:=cSinitial,
      S:=cSS_t,                               % source registers
      D:=cSD_t,                               % destination registers
      result:=cSresult_t,
      e:=cSe                                  % result embedding 
    #);

% register number of the ieeef register
  idx_ieeef : regnot = 64+nspr_IEEEf;

% computation function for ieeef register,
% takes old value and result of the instruction (containing cause) as inputs
  f_ieeef(old:regt,res:resultt):regt=
    old^(31,5) o (old^(4,0) OR res(2)^(11,7));

% define the cS
  IMPORTING tomasulo@tomieeefspec[no_reg,cSspec,idx_ieeef,f_ieeef];

% and now for the tedious OBVIOUS proofs...

% source FPU registers equal in cS and dlx
  cSS_fpu_correct : LEMMA
  FORALL (dlx_conf : dlx_conft,
	  cS       : cSt):
    LET Iw=Iw(dlx_conf) IN
      map_cSR(dlx_conf)=cS IMPLIES
      ((I_fpu(Iw) OR I_fcond(Iw) OR I_mf2i(Iw)) IMPLIES
        fop1(dlx_conf)=source(cS,cSS(Iw,1)) o source(cS,cSS(Iw,0))) AND
      ((I_faddsub(Iw) OR I_fmuldiv(Iw) OR I_fcond(Iw) OR I_fstore(Iw)) IMPLIES
        fop2(dlx_conf)=source(cS,cSS(Iw,3)) o source(cS,cSS(Iw,2))) AND
      (I_fpu(Iw) IMPLIES
        dlx_conf`SPR(SPR_RM)=source(cS,cSS(Iw,4))) AND
      ((I_fpu(Iw) OR I_fcond(Iw)) IMPLIES
        dlx_conf`SPR(SPR_SR)=source(cS,cSS(Iw,5)));

% same for spr
  cSS_spr_correct : LEMMA
  FORALL (dlx_conf : dlx_conft,
	  cS       : cSt):
    LET Iw=Iw(dlx_conf) IN
      map_cSR(dlx_conf)=cS IMPLIES
      (I_rfe(Iw)  IMPLIES
        dlx_conf`SPR(SPR_ESR)=source(cS,cSS(Iw,0)) AND
	r0		     =source(cS,cSS(Iw,1))) AND
      (I_branch(Iw) AND I_branch_fcc(Iw) IMPLIES
        dlx_conf`SPR(SPR_FCC)=source(cS,cSS(Iw,0)) AND
	r0		     =source(cS,cSS(Iw,1))) AND
      (I_movs2i(Iw) IMPLIES
        IF bv2nat(I_immediate(Iw)^(4,0))<=nspr_LAST THEN
	  dlx_conf`SPR(I_immediate(Iw)^(4,0))
	ELSE
	  r0
	ENDIF=source(cS,cSS(Iw,0)) AND
	r0   =source(cS,cSS(Iw,1)));

  no_illegal : LEMMA
  FORALL (dlx_conf : dlx_conft):
    NOT JISR(dlx_conf) IMPLIES
      NOT I_illegal(Iw(dlx_conf)) AND NOT imal(dlx_conf) AND NOT ipf(dlx_conf);

  imal_and_ipf_helper : LEMMA
  FORALL (dlx_conf : dlx_conft):
    imal(dlx_conf) OR ipf(dlx_conf) IMPLIES
	I_is_alu(Iw(dlx_conf));

% and the rest...
  cSS_else_correct : LEMMA
  FORALL (dlx_conf : dlx_conft,
	  cS       : cSt):
    LET Iw=Iw(dlx_conf) IN
      map_cSR(dlx_conf)=cS IMPLIES
      ((I_is_alu(Iw) OR I_mem(Iw) OR I_branch(Iw) AND NOT I_branch_fcc(Iw) OR 
	I_jr(Iw) OR I_movi2s(Iw)) IMPLIES
        (op1(dlx_conf)=source(cS,cSS(Iw,0))) AND
	 op1(dlx_conf)=source(cS,cSS(Iw,1))) AND
      (I_mi2f(Iw) IMPLIES
        op2(dlx_conf)=source(cS,cSS(Iw,0)) AND
        op2(dlx_conf)=source(cS,cSS(Iw,1))) AND
      ((I_ALU(Iw) OR I_shift(Iw) OR I_store(Iw)) IMPLIES
        op2(dlx_conf)=source(cS,cSS(Iw,2)));

  reg0_helper : LEMMA
  FORALL (a:bvec[5]):
    (a(0) OR a(1) OR a(2) OR a(3) OR a(4)) = (bv2nat(a)/=0);

% destination registers equal in dlx and cS
  cSD_fpu_correct : LEMMA
  FORALL (dlx_conf : dlx_conft,
	  cS       : cSt):
    LET Iw=Iw(dlx_conf) IN
      ((I_fpu(Iw) OR I_mem(Iw) AND I_fload(Iw) OR I_mi2f(Iw)) AND 
	(fdouble_dest(Iw) OR NOT I_RD(Iw)(0)) IMPLIES
        bv2nat(I_RD(Iw)^(4,1))+32=cSD(Iw,0)) AND
      ((I_fpu(Iw) OR I_mem(Iw) AND I_fload(Iw) OR I_mi2f(Iw)) AND 
	NOT fdouble_dest(Iw) AND I_RD(Iw)(0) IMPLIES
        0=cSD(Iw,0)) AND
      ((I_fpu(Iw) OR I_mem(Iw) AND I_fload(Iw) OR I_mi2f(Iw)) AND 
	(fdouble_dest(Iw) OR I_RD(Iw)(0)) IMPLIES
        bv2nat(I_RD(Iw)^(4,1))+48=cSD(Iw,1)) AND
      ((I_fpu(Iw) OR I_mem(Iw) AND I_fload(Iw) OR I_mi2f(Iw)) AND 
	NOT fdouble_dest(Iw) AND NOT I_RD(Iw)(0) IMPLIES
        0=cSD(Iw,1));

  cSD_high_helper : LEMMA
  FORALL (dlx_conf : dlx_conft,
	  cS       : cSt):
    LET Iw=Iw(dlx_conf) IN
      cSD(Iw,1)/=0 IMPLIES
      cSD(Iw,1)>=48 AND cSD(Iw,1)<64 AND
      (cSD(Iw,0)>=32 AND cSD(Iw,0)<48 OR cSD(Iw,0)=0) AND 
      (I_fpu(Iw) OR I_fload(Iw) OR I_mi2f(Iw));

  cSD_correct: LEMMA
    FORALL (dlx_conf: dlx_conft, cS: cSt):
      LET Iw = Iw(dlx_conf) IN
        ((I_is_alu(Iw) OR I_mem(Iw) AND I_load(Iw) OR I_movs2i(Iw) OR I_mf2i(Iw)) IMPLIES
          (bv2nat(I_RD(Iw)) = cSD(Iw, 0) AND 0 = cSD(Iw, 1))) AND
         ((I_j(Iw) OR I_jr(Iw)) AND I_link(Iw) IMPLIES
           (bv2nat(index31) = cSD(Iw, 0) AND 0 = cSD(Iw, 1))) AND
          (I_rfe(Iw) IMPLIES 
	   nspr_SR  = cSD(Iw, 0) - 64 AND 0 = cSD(Iw, 1)) AND
          (I_fcond(Iw) IMPLIES 
	   nspr_FCC = cSD(Iw, 0) - 64 AND 0 = cSD(Iw, 1)) AND
          (I_movi2s(Iw) IMPLIES
             IF bv2nat(I_immediate(Iw) ^ (4, 0)) <= nspr_LAST
               THEN bv2nat(I_immediate(Iw) ^ (4, 0)) + 64
             ELSE 0
             ENDIF
              = cSD(Iw, 0)
              AND 0 = cSD(Iw, 1)) AND
         ((I_mem(Iw) AND (I_store(Iw) OR I_fstore(Iw)) OR
           I_trap(Iw) OR I_branch(Iw) OR (I_j(Iw) OR I_jr(Iw)) AND NOT I_link(Iw)) IMPLIES 
	   0 = cSD(Iw, 0) AND 0 = cSD(Iw, 1));
  
  no_dest_for_CA_and_EData : LEMMA
  FORALL (Iw:registert):
    cSD(Iw,2)=0 AND
    cSD(Iw,3)=0;

  no_dest_for_illegal : LEMMA
  FORALL (Iw:registert):
    I_illegal(Iw) IMPLIES 
	cSD(Iw,0)=0 AND
        cSD(Iw,1)=0;

% and finally the equality of the next-step-functions
% since the Tomasulo proof does not feature interrupts,
% we use a dlx without interrupt as specification
  cSstep_correct_gpr : LEMMA
  FORALL (cS       : cSt,
	  dlx_conf : dlx_conft):
     map_cSR(dlx_conf)=cS IMPLIES
     FORALL (r:below(32)):
       map_cSR(dlx_step_without_interrupt(dlx_conf))`R(r)=
	  IF r/=0 AND EXISTS (q: dt): cSD(Iw(dlx_conf), q)=r THEN
	    cSresult(dlx_conf)(cSspec`e(r))
	  ELSE
	    cS`R(r)
	  ENDIF;

  cSstep_correct_fpr : LEMMA
  FORALL (cS       : cSt,
	  dlx_conf : dlx_conft):
     map_cSR(dlx_conf)=cS IMPLIES
     FORALL (r:subrange(32,63)):
       map_cSR(dlx_step_without_interrupt(dlx_conf))`R(r)=
	  IF r/=0 AND EXISTS (q: dt): cSD(Iw(dlx_conf), q)=r THEN
	    cSresult(dlx_conf)(cSspec`e(r))
	  ELSE
	    cS`R(r)
	  ENDIF;

  fpu_exception_helper : LEMMA
  FORALL (dlx_conf : dlx_conft):
    NOT (I_fpu(Iw(dlx_conf)) OR I_fcond(Iw(dlx_conf)) OR I_mf2i(Iw(dlx_conf)) OR I_mi2f(Iw(dlx_conf))) IMPLIES
      CA(dlx_conf)^(12,7)=fill[6](FALSE);
  
  cSstep_correct_spr : LEMMA
  FORALL (cS       : cSt,
	  dlx_conf : dlx_conft):
     map_cSR(dlx_conf)=cS IMPLIES
     FORALL (r:subrange(64,no_reg-1)):
       map_cSR(dlx_step_without_interrupt(dlx_conf))`R(r)=
	  IF r/=0 AND EXISTS (q: dt): cSD(Iw(dlx_conf), q)=r THEN
	    cSresult(dlx_conf)(cSspec`e(r))
	  ELSE  
	    cS`R(r)
	  ENDIF;

% the IEEEf-Register is treated specially
  cSstep_correct_spr_IEEEf : LEMMA
  FORALL (cS       : cSt,
	  dlx_conf : dlx_conft):
     map_cSR(dlx_conf)=cS IMPLIES
     FORALL (r:subrange(64,no_reg-1)):
       map_cSR(dlx_step_without_interrupt_IEEEf(dlx_conf))`R(r)=
	  IF r/=0 AND EXISTS (q: dt): cSD(Iw(dlx_conf), q)=r THEN
	    cSresult(dlx_conf)(cSspec`e(r))
	  ELSIF r=idx_ieeef THEN % IEEEf
	    f_ieeef(cS`R(r),cSresult(dlx_conf))
	  ELSE  
	    cS`R(r)
	  ENDIF;

% and finally the correctness: cS_ieeef=dlx_conf_without_interrupt_IEEEf
  cS_ieeef_correct : LEMMA
  FORALL (t:nat):
    map_cSR(dlx_conf_without_interrupt_IEEEf(init_conf,t))=cS_ieeef(t);

END tom_correct