%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Proofs of progress and preservation.
%%
%% Author: Fernando Magno Quintao Pereira, 03-26-2007%
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% The proof that if you jump to another instructions sequence, you can type
% check that sequence as long as your environment is sound:

seqLemmaAux : tpCodeHeapAux Psi C (CodeHeapTp Psi')
	-> proj_exp C N (i_seq I)
	-> proj_exp Psi' N (CodeExp G)
	-> tpSeq Psi I (CodeTp G)
	-> type.

%mode seqLemmaAux +TCHA +PE +PG -TS.

seqLemmaAux_z : seqLemmaAux (tpCodeHeapAux_con TCHA TS) proj_exp_z proj_exp_z TS.

seqLemmaAux_s : seqLemmaAux (tpCodeHeapAux_con TCHA TS') (proj_exp_s PE) (proj_exp_s PG) TS
        <- seqLemmaAux TCHA PE PG TS.

%worlds () (seqLemmaAux _ _ _ _).
%total TCHA (seqLemmaAux TCHA _ _ _).

seqLemma : tpCodeHeap Psi C
        -> proj_exp C N (i_seq I)
        -> proj_exp Psi N (CodeExp G)
        -> tpSeq Psi I (CodeTp G)
        -> type.

%mode seqLemma +TCH +PE +PG -TS.

seqLemma_ : seqLemma (tpCodeHeap_ TCHA) PE PG TS
        <- seqLemmaAux TCHA PE PG TS.

%worlds () (seqLemma _ _ _ _).
%total {} (seqLemma _ _ _ _).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% The proof that the bank of register remains consistent after being updated.

rbLemma : tpRegBank R (CodeTp G)
	-> update_exp R (psd Np) Nr R' X
	-> update_exp G (psd Np) Nr G' Y
	-> tpRegBank R' (CodeTp G')
	-> type.

%mode rbLemma +TRB +UR +UG -TRB'.

rbLemma_c : rbLemma (tpRegBank_con TRB) update_exp_z update_exp_z (tpRegBank_con TRB).

rbLemma_d : rbLemma (tpRegBank_con TRB) (update_exp_s UR) (update_exp_s UG) (tpRegBank_con TRB')
	<- rbLemma TRB UR UG TRB'.

%worlds () (rbLemma _ _ _ _).
%total TRB (rbLemma TRB _ _ _).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Proofs of preservation:

preservation: tpState C R I -> step C R I C' R' I' -> tpState C' R' I' -> type.

%mode preservation +TE +SE -TE'.

preservation_mov: preservation
	(tpState_ SUB (tpSeq_seq TS (tpIns_mov UG NZ _)) TRB TCH)
	(step_mov UR _)
	(tpState_ SUB' TS TRB' TCH)
	<- subUpdtLemma SUB UG UG'
	<- subUpdtSubLemma SUB UG UG' NZ SUB'
	<- rbLemma TRB UR UG' TRB'.

preservation_jeq: preservation
	(tpState_ SUB (tpSeq_seq TS TPC) TRB TCH)
	(step_jeq EV)
	(tpState_ SUB TS TRB TCH).

preservation_jmp: preservation
	(tpState_ SUB (tpSeq_jmp SUB' (tplb_ PG)) TRB TCH)
	(step_jmp PE)
	(tpState_ SUBT TS TRB TCH)
	<- seqLemma TCH PE PG TS
	<- subTransLemma SUB SUB' SUBT.

preservation_jne: preservation
	(tpState_ SUB (tpSeq_seq TSOld (tpIns_cnd SUB' (tplb_ PG) TPO)) TRB TCH)
	(step_jne PE EV)
	(tpState_ SUBT TS TRB TCH)
	<- seqLemma TCH PE PG TS
	<- subTransLemma SUB SUB' SUBT.

%worlds () (preservation _ _ _).
%total TPS (preservation TPS _ _).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Lemmas for progress:

% If the bank of register type-checks, it can be updated.

updtLemma : tpRegBank R (CodeTp G)
	-> update_exp G (psd Np) Nr G' PG
	-> update_exp R (psd Np) Nr R' PR
	-> type.

%mode updtLemma +TRB +UG -UR.

updtLemma_z : updtLemma TRB update_exp_z update_exp_z.

updtLemma_s : updtLemma (tpRegBank_con TRB) (update_exp_s UG) (update_exp_s UR)
	<- updtLemma TRB UG UR.

%worlds () (updtLemma  _ _ _).
%total TRB (updtLemma  TRB _ _).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Auxiliar lemma for proving evaluation of registers:

regLemma : tpRegBank R (CodeTp G)
        -> proj_exp G Nr (psd Np)
        -> proj_exp R Nr (psd Np)
        -> type.

%mode regLemma +TRB +PG -PR.

regLemma_z : regLemma (tpRegBank_con TRB) proj_exp_z proj_exp_z.

regLemma_s : regLemma (tpRegBank_con TRB) (proj_exp_s PG) (proj_exp_s PR)
        <- regLemma TRB PG PR.

%worlds () (regLemma _ _ _).
%total TRB (regLemma TRB _ _).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% If |- C : Psi and C(L) : G, then exists I, such that C(L) = I

jmpLemmaAux : tpCodeHeapAux Psi C' (CodeHeapTp Psi')
        -> proj_exp Psi' N X
        -> proj_exp C' N (i_seq I)
        -> type.

%mode jmpLemmaAux +TCHA +TPG -PjExp.

jmpLemmaAux_z : jmpLemmaAux _ proj_exp_z proj_exp_z.

jmpLemmaAux_s : jmpLemmaAux (tpCodeHeapAux_con TCHA TS) (proj_exp_s PG) (proj_exp_s PE)
        <- jmpLemmaAux TCHA PG PE.

%worlds () (jmpLemmaAux _ _ _).
%total TCHA (jmpLemmaAux TCHA _ _).


jmpLemma : tpCodeHeap Psi C
        -> proj_exp Psi N X
        -> proj_exp C N (i_seq I)
        -> type.

%mode jmpLemma +TCH +TPG -PjExp.

jmpLemma_ : jmpLemma (tpCodeHeap_ TCHA) PG PE
        <- jmpLemmaAux TCHA PG PE.

%worlds () (jmpLemma _ _ _).
%total TCHA (jmpLemma TCHA _ _).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Proofs of progress:

progress: tpState C R I -> step C R I C' R' I' -> type.

%mode progress +T -S.

progress_mov_blt : progress
        (tpState_ SUB (tpSeq_seq TS (tpIns_mov UpExp NZ tpop_gab)) TRB TCH)
        (step_mov UP eval_blt)
	<- subUpdtLemma SUB UpExp UpExp'
        <- updtLemma TRB UpExp' UP.

progress_mov_reg : progress
        (tpState_ SUB (tpSeq_seq TS (tpIns_mov UpExp NZ (tpop_reg NZ' PG))) TRB TCH)
        (step_mov UP (eval_reg NZ' PR))
        <- subRegLemma SUB PG NZ' PG'
        <- regLemma TRB PG' PR
	<- subUpdtLemma SUB UpExp UpExp'
        <- updtLemma TRB UpExp' UP.

progress_jeq : progress
        (tpState_ SUB (tpSeq_seq TS (tpIns_cnd SUB' TPG (tpop_reg NZ PG))) TRB TCH)
        (step_jeq (eval_reg NZ PR))
        <- regLemma TRB PG PR.

progress_jmp : progress
        (tpState_ SUB (tpSeq_jmp SUB' (tplb_ PG)) TRB TCH)
        (step_jmp PjExp)
        <- jmpLemma TCH PG PjExp.

progress_jne : progress
        (tpState_ SUB (tpSeq_seq TS (tpIns_cnd SUB' (tplb_ PLb) (tpop_reg NZ PG))) TRB TCH)
        (step_jne PjExp (eval_reg NZ PR))
        <- subRegLemma SUB PG NZ PG'
        <- regLemma TRB PG' PR
        <- jmpLemma TCH PLb PjExp.

%worlds () (progress _ _).
%total TPS (progress TPS _).