vamp_correct[(IMPORTING tom_conft,fpu_impl_ui_types)
	      initial_vamp:tom_conft,
	      input:tom_impl_input_funct,
	      last_reset : nat,
	      initial_vamp_mem:mem_state]: THEORY
BEGIN

%% the final theory...

  ASSUMING
  dlxif : LIBRARY = "../dlxif";

  IMPORTING dlxif@fpu_spec_IEEE, 
	    fpu_impl_ui_ok_types[fpu_spec_op],
	    tom_impl_spec_correct[fpu_spec_op],
  	    pipe_control@ext_pipe_control_with_caches_nc_correct[29,sa_cache,2,1,20,7,sa_cache,4,2,20,7,2,3];
  
%% our assumptions:
%% * only initial external reset
%% * rest upto time last_reset
%% * valid external read or write accesses up to last_reset
%% * only valid external reads after last_reset

    input_is_good : ASSUMPTION
    (FORALL (T:nat):input(T)`ext_reset=(T=0)) AND
    (FORALL (T:nat):input(T)`reset=(T<=last_reset)) AND
    (FORALL (T:above(last_reset)):NOT input(T)`ext_in`mw) AND
    (FORALL (T:upto(last_reset)):NOT input(T)`ext_in`mw OR NOT input(T)`ext_in`mr) AND
    (FORALL (T:nat): (input(T)`ext_in`mr OR input(T)`ext_in`mw) AND
                        vamp_out(initial_vamp,input)(T)`ext_out`busy IMPLIES
                        input(T+1)`ext_in=input(T)`ext_in);

%% caches are initialized in the FPGA

    vamp_caches_initial : ASSUMPTION
	initial_ext_configt?(initial_vamp`S3`mem`mif);

  ENDASSUMING

  add_spec_ok : JUDGEMENT add_comb HAS_TYPE add_spec_t;
  md_spec_ok  : JUDGEMENT md_comb  HAS_TYPE md_spec_t;
  fpm_spec_ok : JUDGEMENT fpm_comb HAS_TYPE fpm_spec_t;

  IMPORTING fpu_impl_ui_ok[fpu_spec_op,add_comb,md_comb,fpm_comb];

  TOMadd_ok : JUDGEMENT TOMadd HAS_TYPE add_circuit_ok_t;
  TOMmd_ok  : JUDGEMENT TOMmd  HAS_TYPE md_circuit_ok_t;
  TOMfpm_ok : JUDGEMENT TOMfpm HAS_TYPE fpm_circuit_ok_t;

%% we now basically want to take the criterion from tom_correct5,
%% the equality from tom_impl_spec_correct, AND the memory interface
%% correctness (under the bus protocol assumption) in order to conclude
%% correctness of the concrete VAMP implementation that is 
%% actually synthesized

%% the visible memory (not part of the configuration tom_conft)

  vamp_mem_conf(T:nat):mem_state=
    LET inp=LAMBDA (n:nat): 
	      LET conf=vamp_conf(initial_vamp,input,n) IN
	  	mif_input(conf`S3`mem,vamp_mem_input(conf,input(n))) IN
       ext_memory_spec_conf(initial_vamp_mem,
                            LAMBDA (n: nat):
                              ext_pipe_impl_out_with_caches(initial_vamp`S3`mem`mif,inp)
                                                           (n)`ext_memory_interface_input,
                            LAMBDA (n:nat):inp(n)`ext_memory_interface_output,
			    T);

  start_vamp : initial_conft = vamp_conf(initial_vamp,input,last_reset+1);
  vamp_input : tom_impl_input_funct = LAMBDA (T:nat):input(T+last_reset+1);
  start_vamp_mem : mem_state = vamp_mem_conf(last_reset+1);

  start_vamp_ok : JUDGEMENT
    start_vamp HAS_TYPE (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);

%% use the correctness

  IMPORTING tom_correct5[fpu_spec_op,add_comb,md_comb,fpm_comb,TOMadd,TOMmd,TOMfpm,mif_next,
			start_vamp,vamp_input,start_vamp_mem];

%% define scheduling function for concrete implementation

  sI_vamp_inst(T:nat):RECURSIVE upto(T)=
    IF T=0 THEN
      0
    ELSE
    LET conf=vamp_conf(initial_vamp,input,last_reset+T),
	s4=signals4(conf`S4,conf`S5`SPR(nspr_SR),FALSE) IN
      IF s4`writeback OR s4`JISR THEN
        sI_vamp_inst(T-1)+1
      ELSE
        sI_vamp_inst(T-1)
      ENDIF
    ENDIF
    MEASURE T;

%% simple lemma about decomposition
      
  vamp_conf_helper : LEMMA
    FORALL (init_conf:tom_conft, T  : nat):
      FORALL (Tp : upfrom(T)):
      vamp_conf(init_conf,input,Tp)=
      	vamp_conf(vamp_conf(init_conf,input,T),LAMBDA (n:nat):input(T+n),Tp-T);

%% simple equality lemma 

  vamp_conf_lemma : LEMMA
    FORALL (T : nat):
      tom_impl_conf[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op](start_vamp,vamp_input,T)=
        vamp_conf(initial_vamp,input,T+1+last_reset);

%% scheduling function equality

  sI_vamp_inst_correct : LEMMA
    FORALL (T:nat):
      sI_vamp_inst(T)=sI_Inst(T);

%% tedious "input-from-the-future-does-not-affect-the-past"-lemma

  vamp_conf_input_helper : LEMMA
    FORALL (init_conf:tom_conft,
	    input,input2:tom_impl_input_funct,
	    T:nat):
      (FORALL (Tp:below(T)):input(Tp)=input2(Tp))IMPLIES
      vamp_conf(init_conf,input,T)=vamp_conf(init_conf,input2,T);

%% map the defined VAMP memory to the proved version (3 lemmas)

  ext_pipe_conf_is_vamp_conf_mif : LEMMA
    FORALL (init_conf:tom_conft,
	    input:tom_impl_input_funct,
	    T:nat):
      ext_pipe_impl_conf_with_caches(init_conf`S3`mem`mif,T,mif_inputt(init_conf,input))=
	vamp_conf(init_conf,input,T)`S3`mem`mif;

  ext_pipe_conf_input_is_tommem_conf_mif_input : LEMMA
    FORALL (init_conf:tom_conft,
	    input:tom_impl_input_funct):
    LET mem_in=LAMBDA (n:nat):vamp_mem_input(vamp_conf(init_conf,input,n),input(n)) IN
      mif_inputt(init_conf,input)=LAMBDA (n:nat): 
	(# ext_memory_interface_output :=
	     tommem_out[mif_next](init_conf`S3`mem,mem_in)(n)`mif_input,
	   memory_output := input(n)`bp_in #);

  ext_pipe_conf_output_is_tommem_conf_mif_output : LEMMA
    FORALL (init_conf:tom_conft,
	    input:tom_impl_input_funct):
    LET mem_in=LAMBDA (n:nat):vamp_mem_input(vamp_conf(init_conf,input,n),input(n)) IN
      ext_pipe_impl_out_with_caches(init_conf`S3`mem`mif,mif_inputt(init_conf,input))=LAMBDA (n:nat): 
	(# ext_memory_interface_input :=
	     tommem_out[mif_next](init_conf`S3`mem,mem_in)(n)`mif_output,
	   memory_input := vamp_out(init_conf,input)(n)`bp_out #);

%% our assumption about the bus protocl holding upto cycle T

  is_really_good_bus_protocol?(T:nat):bool=
    is_bus_protocol?(T,initial_vamp_mem,
		     LAMBDA (n:nat):vamp_out(initial_vamp,input)(n)`bp_out)
	 	    (LAMBDA (n:nat):input(n)`bp_in);

%% some furthrt lemmas needed in order to map VAMP memory to the
%% proved version
  mem_input_helper : LEMMA
    real_mem_input_t[start_vamp,fpu_spec_op,add_comb,md_comb,fpm_comb,TOMadd,TOMmd,TOMfpm,mif_next,vamp_input,start_vamp_mem]=LAMBDA (n:nat):vamp_mem_input(vamp_conf(initial_vamp,input,1+last_reset+n),input(1+last_reset+n));

  final_ext_helper_helper : LEMMA
    FORALL(T:nat):
      ext_pipe_impl_conf_with_caches(initial_vamp`S3`mem`mif,T,LAMBDA (n:nat):
				mif_input(vamp_conf(initial_vamp,input,n)`S3`mem,
				vamp_mem_input(vamp_conf(initial_vamp,input,n),input(n))))=
	vamp_conf(initial_vamp,input,T)`S3`mem`mif;

  ext_helper_helper : LEMMA
    FORALL(T:nat):
      vamp_mem_conf(T+1+last_reset)=mem_conf_with_Interrupts(T);

%% we can derive good_ext_memory_interface_output_upto? from our
%% input assumptions which we need in order to use the proved correctness

  good_mif_output_upto : LEMMA
    LET mem_in=LAMBDA (n:nat):vamp_mem_input(vamp_conf(initial_vamp,input,n),input(n)) IN
    FORALL (T:nat):
	good_ext_memory_interface_output_upto?(T,
	  LAMBDA (n:nat): tommem_out[mif_next](initial_vamp`S3`mem,mem_in)(n)`mif_output)
	 (LAMBDA (n:nat): tommem_out[mif_next](initial_vamp`S3`mem,mem_in)(n)`mif_input);

%% and we apply memory interface correctness in order to show this lemma

  correct_mif_upto : LEMMA
    LET mem_in=LAMBDA (n:nat):vamp_mem_input(vamp_conf(initial_vamp,input,n),input(n)) IN
    FORALL (T:posnat):
	is_really_good_bus_protocol?(T) IMPLIES
	consistent_ext_memory_interface_upto?(T, initial_vamp_mem,
	  LAMBDA (n:nat): tommem_out[mif_next](initial_vamp`S3`mem,mem_in)(n)`mif_output)
	 (LAMBDA (n:nat): tommem_out[mif_next](initial_vamp`S3`mem,mem_in)(n)`mif_input);

%% in order to conclude VAMP memory correctness, we need an additional helper

  tommem_out_helper : LEMMA
    FORALL (T:nat):
    LET mem_in=LAMBDA (n:nat):vamp_mem_input(vamp_conf(initial_vamp,input,n),input(n)) IN
      tommem_out[mif_next](initial_vamp`S3`mem,mem_in)(1+last_reset+T)=
      tommem_out[mif_next](start_vamp`S3`mem,real_mem_input_t[start_vamp,fpu_spec_op,add_comb,md_comb,fpm_comb,TOMadd,TOMmd,TOMfpm,mif_next,vamp_input,start_vamp_mem])(T);

%% and the final lemma for VAMP memory correctness:
%% from the bus protocol and our assumptions, we can conclude
%% that the visible VAMP memory is really implemented by the memory interface

  memory_interface_correct : LEMMA
    FORALL (T:nat):
      is_really_good_bus_protocol?(T+last_reset+1) IMPLIES
      good_mif_next_with_interrupts?[start_vamp,fpu_spec_op,add_comb,md_comb,fpm_comb,TOMadd,TOMmd,TOMfpm,mif_next,vamp_input,start_vamp_mem](T);

%% and putting all this together, we have the overall correctness
%% (imagine Richard Strauss' "Thus Spake Zarathustra" being played here)

  final_lemma : THEOREM
    FORALL (T:nat):
    is_really_good_bus_protocol?(T+last_reset+1) AND
    synced_code_with_interrupt?(dlx_init_conf) IMPLIES
    LET conf =vamp_conf(initial_vamp,input,T+last_reset+1),
	old  =vamp_conf(initial_vamp,input,T+last_reset),
	spec =dlx_conf_IEEEf(dlx_init_conf,sI_vamp_inst(T)) IN
    conf`S5`GPR =spec`GPR AND conf`S5`FPRh=spec`FPRh AND conf`S5`FPRl=spec`FPRl AND
    (conf`S5`SPR = LAMBDA(sp:upto(nspr_LAST)):spec`SPR(nat2bv[5](sp))) AND
    ((T=0 OR signals4(old`S4,old`S5`SPR(nspr_SR),input(T+last_reset)`reset)`JISR) IMPLIES
	conf`S2`DPC=spec`DPC AND conf`S2`PCp=spec`PCp AND 
	vamp_mem_conf(T+1+last_reset)=spec`mem);

END vamp_correct