(* //===========================================================================
-- //
-- // 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
Dijsktra's Duct National Flag program specified in the file
dflag1.spec. Array overflow safety is also proven.

------------------------------------------------------------ *)

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

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

load "dflagTheory" ;
load "intLib" ;
open dflagTheory intLib ;


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

(* DEPRACATED -------------------------------------------------

Construct pairs of small assumptions, then check if they
are contradictive. 

fun TRY_2_CONTRADICTION_TAC conv
	=
	let
	fun mkpairs []     = []
	  | mkpairs (x::s) = map (fn z=> (x,z)) s @ mkpairs s
	fun CONTR_TAC (t1,t2) = mesonLib.GEN_MESON_TAC 2 2 8
					[ conv (mk_imp (t1,mk_neg t2))]
				handle
				_ => NO_TAC

	fun isAtom t = mem ((fst o dest_const o rator o rator) t)
			["int_lt","int_gt","int_le","int_ge"]
			handle
			_ => false

	fun isNegAtom t = ((fst o dest_const o rator) t = "~")
			  andalso 
			  isAtom (rand t) 
			  handle
			  _ => false

	fun select t = isAtom t orelse isNegAtom t

	in 
	TRY
	(ASSUM_LIST
		(FIRST	o
		 map CONTR_TAC o
		 mkpairs o
		 filter select o
		 map concl))
	end ;

DEPRACATED --------------------------------------------------- *)

(* ------------------------------------------------------------ 

This tactic will throw away 'big' assumptions from the goal. Here
'big' means it is quantified at the outer level.

------------------------------------------------------------ *)

fun STRIP_BIG_ASM_TAC goal
	=
	(TRY (POP_ASSUM 
	       (fn thm => 
			let
			val t = concl thm
			in 
			if is_forall t orelse is_exists t
			   then STRIP_BIG_ASM_TAC
			   else STRIP_BIG_ASM_TAC THEN ASSUME_TAC thm
			end ))) 
	goal ;

val UNDISCH_ALL_TAC = REPEAT
	(FIRST_ASSUM (UNDISCH_TAC o concl)) ;

val std_tac =
	REMOVE_MARKER_TAC
	THEN REMOVE_PSEUDO_CONST_TAC
	THEN REWRITE_TAC [isRed_def, isWhite_def, isBlue_def, allRWB_def]
	THEN REPEAT CONJ_TAC

	(* -- filtering trivial goals --------------------- *)

	(* -- filter 1 *)
	THEN RW_TAC std_ss []
	THEN TRY (STRIP_BIG_ASM_TAC THEN COOPER_TAC)
	(* -- simplifying arraySize (ArrayUpdate a ...) 
	   -- kind of expressions in the assumptions 		
           -- *)
	THEN UNDISCH_ALL_TAC
	THEN REWRITE_TAC [SizeOf_ArrayUpdate_thm]
	THEN REPEAT STRIP_TAC
	(* -- filter 2 *)
	THEN RW_TAC std_ss array_thms
	THEN TRY (STRIP_BIG_ASM_TAC THEN COOPER_TAC)
	(* -- filter 3 *)	
	THEN TRY (FIRST_ASSUM MATCH_MP_TAC
		    THEN STRIP_BIG_ASM_TAC 
		    THEN COOPER_TAC)

	THENL

	(* --
           -- 4-goals remain .... including PEC
           --  *)

	let
	val TAC1 = FIRST_ASSUM 
		(fn thm =>
		 MATCH_MP_TAC 
		   (REWRITE_RULE 
			[PROVE [] (--`(p ==> a\/b\/c) = (p /\ ~b /\ ~c ==> a)`--)]
			thm)
	         THEN STRIP_BIG_ASM_TAC 
	         THEN COOPER_TAC)
	in

	[ RW_TAC std_ss [dutchSorted_def, isBlue_def, isRed_def, isWhite_def]
	  THEN SUBGOAL_THEN (--`(i:int)=r`--) ASSUME_TAC
	  THENL [STRIP_BIG_ASM_TAC THEN COOPER_TAC, ALL_TAC]
	  THEN SUBGOAL_THEN (--`(b:int)<=r`--) ASSUME_TAC
	  THENL [STRIP_BIG_ASM_TAC THEN COOPER_TAC, ALL_TAC]
	  (* still too deep for PROVE_TAC *)
	  THEN EXISTS_TAC (--`b:int`--)
	  THEN EXISTS_TAC (--`r:int`--)
	  THEN RW_TAC std_ss [],
	  ASM_CASES_TAC (--`(k:int) = i`--)
	  THENL [RW_TAC std_ss [],
		 FIRST_ASSUM MATCH_MP_TAC
		 THEN STRIP_BIG_ASM_TAC 
		 THEN COOPER_TAC ],
	  TAC1,
	  TAC1
	] 

	end ;


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

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

read_mechout "dflag1.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 REPEAT CONJ_TAC
	 THEN RW_TAC std_ss [SizeOf_ArrayUpdate_thm] 
	 THEN TRY (STRIP_BIG_ASM_TAC THEN COOPER_TAC) ) ;

(* ------------------------------------------------------------
- run data:
runtime: 24.276s,    gctime: 2.640s,     systime: 24.276s.
Axioms asserted: 0.
Definitions made: 0.
Oracle invocations: 0.
Theorems loaded from disk: 0.
HOL primitive inference steps: 198853.
Total: 198853.
------------------------------------------------------------ *)

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