(* //===========================================================================
-- //
-- // AUTHOR(S): Wishnu Prasetya, Ade Azurat
-- // PACKAGE  : (c)xMECH, class LITE, version alpha 1.3.1
-- //
-- //======================================================================== *)
(* // *)
(* 

This HOL Script will prove the program to compute gcd of two positive
integers. The program is specified in the file gcd.spec.

*)

val litemechDir = "../../hollib" ;

loadPath := !loadPath @ [litemechDir] ;
use  (litemechDir ^ "/litemech.smx") ;

load "xgcdTheory" ;
open xgcdTheory ;

(* === [1] proof of the abstracted total correctness *)

val gcd_facts = map DISCH_ALL [gcd_ora1,gcd_ora2,gcd_ora3] ;

val std_tac =
	REMOVE_MARKER_TAC
	THEN REMOVE_PSEUDO_CONST_TAC
	THEN REPEAT CONJ_TAC
	THEN RW_TAC std_ss gcd_facts
	THEN TRY ( mesonLib.GEN_MESON_TAC 2 2 8 gcd_facts)
	THEN TRY COOPER_TAC
	THENL
	[ PROVE_TAC gcd_facts ,
	  SUBGOAL_THEN (--`y>x`--) ASSUME_TAC
	  THENL [ COOPER_TAC, ALL_TAC ]
	  THEN PROVE_TAC gcd_facts
	]
	;


read_mechout "gcd.ls.hout.std" ;
val std_vc = snd from_mech ; 
print "\n\n==>[1] Verification of abstracted standard correctness.... \n\n" ;
val justification_of_stdcor_bls_spec = (Count.apply prove) (std_vc, std_tac) ;

(* -------------------------------------------------------------
Run data:
runtime: 6.629s,    gctime: 0.791s,     systime: 6.629s.
Axioms asserted: 0.
Definitions made: 0.
Oracle invocations: 0.
Theorems loaded from disk: 0.
HOL primitive inference steps: 55008.
Total: 55008.
------------------------------------------------------------- *)

(* ==[2,3] proof of array overflow and division by zero is skipped; 
	they are trivial (program does not contain any array or
	division operation) *)

print "\n\n==>[2] Verification of array overflow check is skipped (trivial). \n\n" ;
print "\n\n==>[3] Verification of division by zero check is skipped (trivial). \n\n" ;
print "\n\n==> DONE. \n\n" ;

(* END *)