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

This HOL Script will prove the abstracted standard correctness of
bounded linear search program specified in the file bls.spec. 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
	THENL
	[ PROVE_TAC [COOPER_CONV (--`~(0<=j) \/ ~(j<0)`--)],
	  EQ_TAC THEN RW_TAC std_ss []
	  THENL
	  [ PROVE_TAC [COOPER_CONV (--`j<i /\ i<k+1 ==> j<k`--)],
	    PROVE_TAC [] 
	  ],
	  EQ_TAC THEN RW_TAC std_ss []
	  THENL
	  [ PROVE_TAC [COOPER_CONV (--`j<i /\ i<k+1 ==> j<k`--)],
	    PROVE_TAC [COOPER_CONV (--`i'<k /\ i<k+1 /\ ~(i<k) ==> i'<i`--)]
	  ],
          PROVE_TAC [COOPER_CONV (--`i<i+1`--)],
	  EQ_TAC THEN RW_TAC std_ss []
	  THENL
	  [ PROVE_TAC [COOPER_CONV (--`j<i ==> j<i+1`--)],
	    SUBGOAL_THEN (--`~((j:int)=i)`--) ASSUME_TAC
	    THENL [PROVE_TAC [], ALL_TAC ]
	    THEN PROVE_TAC [COOPER_CONV (--`j<i+1 /\ ~(j=i) ==> j<i`--)]
	  ]
	] ;

read_mechout "bls.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.159s,    gctime: 0.600s,     systime: 6.159s.
Axioms asserted: 0.
Definitions made: 0.
Oracle invocations: 0.
Theorems loaded from disk: 0.
HOL primitive inference steps: 35822.
Total: 35822.
------------------------------------------------------------- *)

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

(* read_mechout "bls.ls.hout.aoc" ;
   val aoc_vc = snd from_mech ; 
*)
print "\n\n==>[2] Verification of array overflow check.... [currently disengaged]\n\n" ;

(* AOC is temporarily disengaged!!
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.000s,     systime: 0.070s.
Axioms asserted: 0.
Definitions made: 0.
Oracle invocations: 0.
Theorems loaded from disk: 0.
HOL primitive inference steps: 102.
Total: 102.
------------------------------------------------------------- *)

(* ==[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 *)