fp_compare_impl: THEORY
BEGIN

	IMPORTING fp_misc_import


	%%%%%%%%%%%% First we compute the four possible relations (lt,eq,gt,unordered)	

	fp_compare_impl(sa,sb: bit, ea,eb: bvec[11], fa,fb: bvec[53],
					NANa,NANb,ZEROa,ZEROb,pINFa,pINFb,nINFa, nINFb: bit): 
				[# unord, lt, gr, eq: bit #] =
		LET IEEEa = NOT (NANa OR pINFa OR nINFa),
			IEEEb = NOT (NANb OR pINFb OR nINFb),
			LTe = sub_impl[11](ea,eb)`neg,
			LTf = sub_impl[54](fill[1](FALSE) o fa, fill[1](FALSE) o fb)`neg,
			EQe = equal_impl[11](ea,eb),
			EQf = equal_impl[53](fa,fb),
			GTe = NOT (LTe OR EQe),
			GTf = NOT (LTf OR EQf),
			LT  = NOT (NANa OR NANb) AND
					((NOT pINFa AND pINFb) OR
					 (nINFa AND NOT nINFb) OR
					 (IEEEa AND IEEEb AND (
						NOT (ZEROa AND ZEROb) AND
						((sa AND NOT sb) OR
						 (NOT sa AND NOT sb AND (LTe OR (EQe AND LTf))) OR
							 (sa and sb AND (GTe OR (EQe AND GTf))))))),
			EQ  = NOT (NANa OR NANb) AND
					((nINFa AND nINFb) OR 
					 (pINFa AND pINFb) OR
					 (ZEROa AND ZEROb) OR 
					 (IEEEa AND IEEEb AND (NOT sa XOR sb) AND EQe AND EQf))
		IN
		(# unord := NANa OR NANb,
		   lt    := LT,
		   eq	 := EQ,
		   gr	 := NOT (EQ OR LT OR NANa OR NANb) #);

	 fp_compare_correct_sgl: LEMMA FORALL(a,b: bvec[64]):
								   FORALL(sa,sb: bit, ea,eb: bvec[11], fa,fb: bvec[53],
										  NANa,NANb,ZEROa,ZEROb,pINFa,pINFb,nINFa, nINFb: bit):
					 LET A=Sbv2ieee_bv(a), B=Sbv2ieee_bv(b) IN
					 NANa=Snan?(A) AND NANb=Snan?(B) AND 
					 ZEROa=Szero?(A) AND ZEROb=Szero?(B) AND
					 pINFa=Sp_inf?(A) AND pINFb=Sp_inf?(B) AND
					 nINFa=Sn_inf?(A) AND nINFb=Sn_inf?(B) AND
					 (Sieee_number?(A) IMPLIES Sieeebv2fact(A) = (# s:=b2n(sa),
																	e:=bv2int(ea),
																	f:=bv2nat(fa)*2^-52 #)) AND
					 (Sieee_number?(B) IMPLIES Sieeebv2fact(B) = (# s:=b2n(sb),
																	e:=bv2int(eb),
																	f:=bv2nat(fb)*2^-52 #))
				 IMPLIES
					 LET C=fp_compare_impl(sa,sb,ea,eb,fa,fb,
										   NANa,NANb,ZEROa,ZEROb,pINFa,pINFb,nINFa, nINFb) IN
					 C`unord = unordered?[8,8,24,24](A,B) AND
					 C`lt = less?[8,8,24,24](A,B) AND
					 C`eq = equal?[8,8,24,24](A,B) AND
					 C`gr = greater?[8,8,24,24](A,B);


	 fp_compare_correct_dbl: LEMMA FORALL(a,b: bvec[64]):
								   FORALL(sa,sb: bit, ea,eb: bvec[11], fa,fb: bvec[53],
										  NANa,NANb,ZEROa,ZEROb,pINFa,pINFb,nINFa, nINFb: bit):
					 LET A=Dbv2ieee_bv(a), B=Dbv2ieee_bv(b) IN
					 NANa=Dnan?(A) AND NANb=Dnan?(B) AND 
					 ZEROa=Dzero?(A) AND ZEROb=Dzero?(B) AND
					 pINFa=Dp_inf?(A) AND pINFb=Dp_inf?(B) AND
					 nINFa=Dn_inf?(A) AND nINFb=Dn_inf?(B) AND
					 (Dieee_number?(A) IMPLIES Dieeebv2fact(A) = (# s:=b2n(sa),
																	e:=bv2int(ea),
																	f:=bv2nat(fa)*2^-52 #)) AND
					 (Dieee_number?(B) IMPLIES Dieeebv2fact(B) = (# s:=b2n(sb),
																	e:=bv2int(eb),
																	f:=bv2nat(fb)*2^-52 #))
				 IMPLIES
					 LET C=fp_compare_impl(sa,sb,ea,eb,fa,fb,
										   NANa,NANb,ZEROa,ZEROb,pINFa,pINFb,nINFa, nINFb) IN
					 C`unord = unordered?[11,11,53,53](A,B) AND
					 C`lt = less?[11,11,53,53](A,B) AND
					 C`eq = equal?[11,11,53,53](A,B) AND
					 C`gr = greater?[11,11,53,53](A,B);


	 %%%%%%%%%%% Next we compute the FCC according to the desired predicate,
	 %%%%%%%%%%% which is encoded in the opcode op
	 fp_compute_fcc(sa,sb: bit, ea,eb: bvec[11], fa,fb: bvec[53],
					QNANa,QNANb,SNANa,SNANb,ZEROa,ZEROb,pINFa,pINFb,nINFa, nINFb: bit,
					op: bvec[9]): fpu_out_t =
			 LET NANa=QNANa OR SNANa, NANb=QNANb OR SNANb,
				 C=fp_compare_impl(sa,sb,ea,eb,fa,fb,
								   NANa,NANb,ZEROa,ZEROb,pINFa,pINFb,nINFa, nINFb),
				 R=(C`unord AND FCON_un(op)) OR (C`lt AND FCON_lt(op)) OR
				   (C`eq AND FCON_eq(op)) OR (C`gr AND FCON_gt(op)) 
			 IN
			 (# result :=  fill[31](FALSE) o fill[1](R) o fill[32](FALSE),
				exceptions := (# OVF:=FALSE, UNF:=FALSE, INX:=FALSE, DIVZ:=FALSE,
								 INV:=C`unord AND FCON_sig_unordered(op) OR SNANa OR SNANb,
								 UNIMPL:=FALSE #),
				double := FALSE #);

	%% the corresponding lemmas are to trivial. use the above lemmas and expand
	%% the definition of fp_compute_fcc.
	%% (we are lazy)				
END fp_compare_impl