tom_correct5[(IMPORTING tom_conft,fpu_impl_ui_ok_types)
	       fpu_spec_op : fpu_spec_op_t,
	       (IMPORTING fpu_impl_ui_ok_types[fpu_spec_op])
	       add_spec:add_spec_t,
	       md_spec :md_spec_t,
	       fpm_spec:fpm_spec_t,
	       (IMPORTING fpu_impl_ui_ok[fpu_spec_op,add_spec,md_spec,fpm_spec])
	     TOMadd : add_circuit_ok_t,
	     TOMmd  : md_circuit_ok_t,
	     TOMfpm : fpm_circuit_ok_t,
	     mif_next:mif_next_t,
	    (IMPORTING tom_impl_spec[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op])
	    initial_vamp_conf_after_reset:(LAMBDA (x:initial_conft):
			NOT x`S3`mem`inst`rollback AND 
			x`S2`PCp=SISRnext AND x`S2`DPC=SISR AND
			x`S5`SPR=LAMBDA(x:upto(nspr_LAST)):
				   IF x=nspr_ECA THEN r1 ELSE r0 ENDIF),
	    input:tom_impl_input_funct,
	    initial_vamp_mem:mem_state]: THEORY
BEGIN

  IMPORTING tom_correct4_JISR

%% the final theory of correctness of the (abstract) VAMP implementation
%% In this theory, we only "put together" the correctness with interrupts
%% from the previous theory (up to cycle after first interrupt) 
%% to arbitrary interrupt sequences

%% a predicate for arguing about interrupts
  is_JISR?(conf:tom_conft):bool=
    LET s4=signals4_spec(conf`S4,conf`S5`SPR(nspr_SR),FALSE) IN
      s4`JISR;

% wrappers to avoid zillions of actuals...
  sI_Inst(T:nat):upto(T)=sI_inst[initial_vamp_conf_after_reset,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,input,initial_vamp_mem](T);

  vamp_fulfills_Spec?(T:nat):bool=vamp_fulfills_spec?[initial_vamp_conf_after_reset,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,input,initial_vamp_mem](T);

  good_mif_next_with_Interrupts?(T:nat):bool = good_mif_next_with_interrupts?[initial_vamp_conf_after_reset,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,input,initial_vamp_mem](T);

  mem_conf_with_Interrupts(T:nat):mem_state = mem_conf_with_interrupts[initial_vamp_conf_after_reset,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,input,initial_vamp_mem](T);

  good_tom_impl_input_func_Below?(T:nat):bool=good_tom_impl_input_func_below?[initial_vamp_conf_after_reset,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,input,initial_vamp_mem](T);
% end wrappers

%% simple, but important goal: after a reset, we have an initial
%% vamp state and thus can instantiate the correctess proof again
  initial_vamp_conf_after_JISR_or_reset : LEMMA
    FORALL (T   :nat):
      LET conf=tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T) IN
      (input(T)`reset OR  signals4_spec(conf`S4,conf`S5`SPR(nspr_SR),FALSE)`JISR) AND 
      NOT (tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T+1)`S3`mem`inst`rollback AND tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T+1)`S3`mem`inst`I_s) IMPLIES
      initial_vamp_conf?(tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T+1));

%% the PCs are also initial (should be part of initial_vamp_conf?)
  initial_PCs_after_JISR_or_reset : LEMMA
    FORALL (input:tom_impl_input_funct,
	    conf:tom_conft,
	    T   :nat):
      input(T)`reset OR signals4_spec(conf`S4,conf`S5`SPR(nspr_SR),FALSE)`JISR IMPLIES
      LET conf = tom_step_spec(conf,input(T)`reset,
		  		    input(T)`ext_in,
		      		    input(T)`ext_reset,
		      		    input(T)`bp_in)`conf IN
	conf`S2`PCp=SISRnext AND
	conf`S2`DPC=SISR;

%% once again avoid writing all these actuals...
  dlx_init_conf : dlx_conft = tom_correct2a[initial_vamp_conf_after_reset,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,initial_vamp_mem].init_conf;

%% simple helper
  dlx_init_conf_spr_correct : LEMMA
    dlx_init_conf`SPR=LAMBDA(x:bvec[5]):IF bv2nat(x)=2 THEN r1 ELSE r0 ENDIF;

%  sI_JISR(T:nat):RECURSIVE upto(T)=
%    IF T=0 THEN
%      0
%    ELSE
%    LET conf=tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T-1),
%	s4=signals4_spec(conf`S4,conf`S5`SPR(nspr_SR),FALSE) IN
%      IF s4`JISR THEN
%        sI_JISR(T-1)+1
%      ELSE
%        sI_JISR(T-1)
%      ENDIF
%    ENDIF
%    MEASURE T;

%  vamp_conf_equal : LEMMA
%    FORALL (T  : nat):
%      FORALL (Tp : upfrom(T)):
%      tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,Tp)=
%      	tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](
%	  tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T),LAMBDA (n:nat):input(T+n),Tp-T);

  predicates : LIBRARY = "../predicates";
  IMPORTING predicates@predicates[tom_conft,is_JISR?];


%% important lemma about decomposition of mem_conf, tom_impl_conf, and sI_inst
  sI_inst_decomposition : LEMMA
    FORALL (T:nat):
      LET conf = tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T),
          inp  = LAMBDA (x:nat):input(x+T) IN
	initial_vamp_conf?(conf) IMPLIES
      FORALL (Tp:upfrom(T)):
	tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,Tp)=tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](conf,inp,Tp-T) AND
	mem_conf_with_Interrupts(Tp)=mem_conf_with_interrupts[conf,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,inp,mem_conf_with_Interrupts(T)](Tp-T) AND
	sI_Inst(Tp)=sI_Inst(T)+sI_inst[conf,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,inp,mem_conf_with_Interrupts(T)](Tp-T);

%% important helper lemma for correcntess:
%% correcntess in cycle Tp is equal to correctness in cycle Tp-T with
%% the configuration in cycle T as initial configuration
  vamp_fulfills_spec_decomposition : LEMMA
    FORALL (T:nat):
      LET conf = tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T),
          inp  = LAMBDA (x:nat):input(x+T) IN
	initial_vamp_conf?(conf) AND vamp_fulfills_Spec?(T) AND
	(T=0 OR is_JISR?(tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T-1))) AND
 	NOT (conf`S3`mem`inst`rollback AND conf`S3`mem`inst`I_s) IMPLIES
      	init_conf[conf,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,mem_conf_with_Interrupts(T)]=dlx_conf_IEEEf(dlx_init_conf,sI_Inst(T)) AND
      	FORALL (Tp:upfrom(T)):
	  vamp_fulfills_Spec?(Tp)=vamp_fulfills_spec?[conf,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,inp,mem_conf_with_Interrupts(T)](Tp-T);

%% further decomposition lemmas
  good_mif_next_with_interrupts_decomposition : LEMMA
    FORALL (T:nat,Tp:upfrom(T)):
      LET conf = tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T) IN
      initial_vamp_conf?(conf) AND good_mif_next_with_Interrupts?(Tp) IMPLIES
	FORALL (Tpp:upto(Tp-T)): 
	  good_mif_next_with_interrupts?[conf,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,LAMBDA(x:nat):input(x+T),mem_conf_with_Interrupts(T)](Tpp);

%  real_mem_input_t(T:nat):tommem_inputt =
%    LET conf=tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T),
%	s4  =signals4_spec[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](conf`S4,conf`S5`SPR(nspr_SR),input(T)`reset),
%        s3  =signals3_spec[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](conf`S3),
%        s2  =signals2_spec[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](conf`S3, conf`S2, input(T)`reset, s3, s4`clear),
%        s1  =signals1_spec[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](conf`S1, conf`S2, conf`S4, conf`S5,input(T)`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(T)`bp_in,
%           ext_in   := input(T)`ext_in,
%           ext_reset:= input(T)`ext_reset #);

%  mem_conf_with_interrupts(T:nat):mem_state=
%    mif_memory_conf(initial_vamp_conf_after_reset`S3`mem,initial_vamp_mem,real_mem_input_t)(T);
       
%  mem_conf_with_interupts_strongly_correct : LEMMA
%    FORALL (T:nat):
%      LET conf=tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T) IN
%      FORALL (Tp:nat):
%      tommem_conf[mif_next](conf`S3`mem,Tp,LAMBDA(n:nat):real_mem_input_t(n+T))=
%       tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](conf,LAMBDA(n:nat):input(n+T),Tp)`S3`mem;

%  mem_conf_with_interupts_correct : LEMMA
%    FORALL (T:nat):
%      tommem_conf[mif_next](initial_vamp_conf_after_reset`S3`mem,T,real_mem_input_t)=
%       tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T)`S3`mem;

%  mem_conf_with_interupts_equal : LEMMA
%    FORALL (T:nat):
%      LET conf=tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T),
%	  mem =mem_conf_with_interrupts(T) IN
%	FORALL (Tp:nat):
%	  mem_conf_with_interrupts(T+Tp)=
%    	  mif_memory_conf(conf`S3`mem,mem,LAMBDA(n:nat):real_mem_input_t(n+T))(Tp);

  mem_conf_with_inputs_equal : LEMMA
    FORALL (conf : mem_reg,
	    mem  : mem_state,
	    i1,i2: tommem_input_funct):
      i2(0)`ext_reset=i1(0)`ext_reset AND i2(0)`ext_in=i1(0)`ext_in AND 
	i2(0)`bp_in=i1(0)`bp_in AND i2(0)`PC=i1(0)`PC IMPLIES
        mif_memory_conf(conf,mem,i1)(1)=
        mif_memory_conf(conf,mem,i2)(1);

%  good_mif_next_with_interrupts?(T:nat):bool=
%    consistent_mif_next?(T,initial_vamp_conf_after_reset`S3`mem,initial_vamp_mem)
%	(real_mem_input_t);

%  consistent_mif_helper : LEMMA
%    FORALL (T  : nat,
%	    Tp : above(T)):
%      LET conf=tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T),
%	  mem =mem_conf_with_Interrupts(T) IN
%	initial_vamp_conf?(conf) AND 
%	good_mif_next_with_Interrupts?(Tp) IMPLIES
%	LET mem_in=mem_input_t[conf,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,LAMBDA(x:nat):input(x+T),mem] IN
%	consistent_mif_next?(Tp-T-1,conf`S3`mem,mem)(mem_in) AND
%	mem_in(Tp-T-1)=real_mem_input_t(Tp-1) AND 
%	tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,Tp-1)`S3`mem=
%	  tommem_conf[mif_next](conf`S3`mem,Tp-T-1,mem_in) AND
% 	mem_conf_with_Interrupts(Tp-1)=mif_memory_conf[mif_next](conf`S3`mem,mem,mem_in)(Tp-T-1)
%	IMPLIES
%	consistent_mif_next?(Tp-T,conf`S3`mem,mem)(mem_input_t[conf,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,LAMBDA(x:nat):input(x+T),mem]);

%% The following 2 lemmas are the core of the proof with interrupts
  sI_inst_helper : LEMMA
    synced_code_with_interrupt?(dlx_init_conf) IMPLIES
    FORALL (T:nat):
      LET conf=tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T),
	  mem =mem_conf_with_Interrupts(T) IN
        vamp_fulfills_Spec?(T) AND initial_vamp_conf?(conf) AND 
	NOT (conf`S3`mem`inst`rollback AND conf`S3`mem`inst`I_s) AND
	(T=0 OR is_JISR?(tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T-1))) IMPLIES
	init_conf[conf,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,mem]=dlx_conf_IEEEf(dlx_init_conf,sI_Inst(T)) AND
    	synced_code_with_interrupt?(dlx_conf_IEEEf(dlx_init_conf,sI_Inst(T))) AND
         FORALL (Tp:upfrom(T)):
	(good_mif_next_with_Interrupts?(Tp) AND
         good_tom_impl_input_func_Below?(1+Tp) AND
	(FORALL (x:upto(Tp)):NOT input(x)`reset) AND
	FORALL (x:subrange(T,Tp-1)): NOT is_JISR?(tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,x))) IMPLIES
	  vamp_correct?[conf,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,LAMBDA(x:nat):input(x+T),mem](Tp-T) AND
	  vamp_fulfills_Spec?(Tp+1) AND
	  (is_JISR?(tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,Tp)) IMPLIES
      LET inst=tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,Tp)`S3`mem`inst IN
	NOT (tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,Tp+1)`S3`mem`inst`rollback AND tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,Tp+1)`S3`mem`inst`I_s));

  sI_inst_correct : LEMMA
    synced_code_with_interrupt?(dlx_init_conf) IMPLIES
    FORALL (T:nat):
      good_mif_next_with_Interrupts?(T) AND
      good_tom_impl_input_func_Below?(T) AND
      (FORALL (Tp:below(T)):NOT input(Tp)`reset) IMPLIES
    LET inp=LAMBDA(n:nat):tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,n),
	inst=tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T)`S3`mem`inst IN
      ((NOT T-1>=0 OR is_JISR?(tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](initial_vamp_conf_after_reset,input,T-1))) IMPLIES
	  NOT (inst`rollback AND inst`I_s)) AND
      vamp_fulfills_Spec?(T);
    
%% a nice summary of the previous lemma
  vamp_is_correct : LEMMA
    synced_code_with_interrupt?(dlx_init_conf) IMPLIES
    FORALL (T:nat):
      good_mif_next_with_Interrupts?(T) AND
      good_tom_impl_input_func_Below?(T) AND
      (FORALL (Tp:below(T)): NOT input(Tp)`reset) IMPLIES
      vamp_fulfills_Spec?(T);

END tom_correct5