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

This HOL Script will prove the program specified in the file
fillArray.spec. It is just a simple program to fill a locally created
array with a requested value. It is mainly used to test litemech's
feature to compute the initial assumption about the sizes of locally
created arrays.

Array overflow safety is also proven. 

*)

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

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

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

val std_tac =
	REMOVE_MARKER_TAC
	THEN REMOVE_PSEUDO_CONST_TAC
	THEN REPEAT CONJ_TAC
	THEN RW_TAC std_ss []
	THEN TRY ( mesonLib.GEN_MESON_TAC 2 2 8 [])
	THEN TRY COOPER_TAC
        THEN RW_TAC std_ss array_thms
	THEN TRY COOPER_TAC
	THENL
	[ PROVE_TAC [COOPER_CONV (--`~((0<=j) /\ (j<0))`--)],
	  PROVE_TAC [COOPER_CONV (--`j<i+1 ==> (j<i /\ ~(j=i)) \/ (j=i)`--)]
	]
	;

read_mechout "fillArray.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: 3.776s,    gctime: 0.190s,     systime: 3.776s.
Axioms asserted: 0.
Definitions made: 0.
Oracle invocations: 0.
Theorems loaded from disk: 0.
HOL primitive inference steps: 28867.
Total: 28867.
------------------------------------------------------------- *)

(* ==[2] proof of array overflow check *)

read_mechout "fillArray.ls.hout.aoc" ;
val aoc_vc = snd from_mech ; 

print "\n\n==>[2] Verification of array overflow check....\n\n" ;

val justification_of_aoc_bls_spec = (Count.apply prove) 
	(aoc_vc, 
	 REMOVE_MARKER_TAC
	 THEN REMOVE_PSEUDO_CONST_TAC
	 THEN RW_TAC std_ss [] ) ;

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

(* ==[3] proof of division by zero is skipped; goal is trivial 
   (program does not contain any division operation) *)

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

print "\n\n==> DONE. \n\n" ;

(* END *)