*** Matt Webster, January 2008.

*** Proof script for virus Win9x.Zmorph.A code fragments.
*** Read in file sta.obj first.

fmod IA-32-PROOF is
	pr IA-32-SEMANTICS .
	ops g h psi : Store -> Store .
	var S : Store . 

	*** Allomorph 1 -vs- Allomorph 2
	eq g(S) = 	S ; mov edi, 2580774443 ;
										mov ebx, 467750807 ;
										sub ebx, 1745609157 ;
										sub edi, 150468176 ;
										xor ebx, 875205167 ;
										push edi ;
										xor edi, 3761393434 ;
										push ebx ;       
										push edi .
	eq h(S)	=	S ;	mov ebx, 535699961 ;
										mov edx, 1490897411 ;
										xor ebx, 2402657826 ;
										mov ecx, 3802877865 ;
										xor edx, 3743593982 ;
										add ecx, 2386458904 ;
										push ebx ;
										push edx ;       
										push ecx .

	eq psi(S)	=	S ;	mov edi, 0 ;
										mov ebx, 0 ;
										mov ecx, 0 ;
										mov edx, 0 .									
endfm									


*** Proof: equivalence modulo the stack 

*** These should be true
red g(s)[[stack]] is h(s)[[stack]] .
red g(s)[[ip]] is h(s)[[ip]] .

*** QED

red g(s)[[stack]] .

red psi(g(s))[[stack]] is psi(h(s))[[stack]] .
red psi(g(s))[[ip]] is psi(h(s))[[ip]] .
red psi(g(s))[[edi]] is psi(h(s))[[edi]] .
red psi(g(s))[[ebx]] is psi(h(s))[[ebx]] .
red psi(g(s))[[ecx]] is psi(h(s))[[ecx]] .
red psi(g(s))[[edx]] is psi(h(s))[[edx]] .