(* ========================================================================= *)
(* Create "cryptolTheory" setting up the shallow embedding of uCryptol       *)
(* 2006-2007, Joe Hurd.                                                      *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* Load and open relevant theories.                                          *)
(* (Comment out "load"s and "quietdec"s for compilation.)                    *)
(* ------------------------------------------------------------------------- *)
(*
val () = loadPath := [] @ !loadPath;
val () = app load
  ["bossLib", "metisLib", "res_quanTools",
   "optionTheory", "listTheory",
   "arithmeticTheory", "dividesTheory", "gcdTheory",
   "pred_setTheory", "pred_setSyntax", "wordsTheory", "fcpLib"];
val () = quietdec := true;

open HolKernel Parse boolLib bossLib metisLib res_quanTools;
open optionTheory listTheory arithmeticTheory dividesTheory gcdTheory;
open pred_setTheory fcpTheory wordsTheory;
*)

(*
val () = quietdec := false;
*)

(* ------------------------------------------------------------------------- *)
(* Start a new theory called "cryptol".                                     *)
(* ------------------------------------------------------------------------- *)

val _ = new_theory "cryptol";

val ERR = mk_HOL_ERR "cryptol";
val Bug = mlibUseful.Bug;

(* ------------------------------------------------------------------------- *)
(* Sort out the parser.                                                      *)
(* ------------------------------------------------------------------------- *)

val () = Parse.add_infix ("/", 600, HOLgrammars.LEFT);

(* ------------------------------------------------------------------------- *)
(* Helper functions.                                                         *)
(* ------------------------------------------------------------------------- *)

val preprocessor : (term -> (term -> term) option) ref = ref (K NONE);

fun add_preprocessor f =
    let
      val ref p = preprocessor

      fun p' tm = case f tm of NONE => p tm | s => s
    in
      preprocessor := p'
    end;

fun preprocess_term tm =
    case total (find_term (Option.isSome o !preprocessor)) tm of
      NONE => tm
    | SOME subtm =>
      case !preprocessor subtm of
        NONE => raise Bug "preprocess"
      | SOME f => preprocess_term (f tm);

fun preprocess_quotation q =
    let
      val t = preprocess_term (Term q)
    in
      `^t`
    end;

(* ------------------------------------------------------------------------- *)
(* Helper proof tools.                                                       *)
(* ------------------------------------------------------------------------- *)

infixr 0 <<
infixr 1 ++ || THENC ORELSEC
infix 2 >>

val op ++ = op THEN;
val op << = op THENL;
val op >> = op THEN1;
val op || = op ORELSE;
val Know = Q_TAC KNOW_TAC;
val Suff = Q_TAC SUFF_TAC;
val REVERSE = Tactical.REVERSE;
val lemma = Tactical.prove;

(* ------------------------------------------------------------------------- *)
(* Helper theorems.                                                          *)
(* ------------------------------------------------------------------------- *)

val () = type_abbrev ("inf", Type `:num -> 'a`);

val seq_map_def = Define `seq_map f s = f o s`;

val seq_zip_def = Define `seq_zip a b i = (a i, b i)`;

val seq_drop_def = Define `seq_drop (n : num) s i = s (n + i)`;

val seq_append_finite_def = Define
  `seq_append_finite (v : 'a ** 'b) (w : 'a ** 'c) =
   FCP i. if i < dimindex (:'b) then v %% i else w %% (i - dimindex (:'b))`;

val seq_append_infinite_def = Define
  `seq_append_infinite (v : 'a ** 'b) s i =
   if i < dimindex (:'b) then v %% i else s (i - dimindex (:'b))`;

val V_def = Define `V l = FCP i. EL i l`;

val () = overload_on ("seq", ``seq_map``);

val () = overload_on ("|", ``seq_zip``);

val () = overload_on ("drop", ``seq_drop``);

val () = overload_on ("#", ``seq_append_finite``);

val () = overload_on ("#", ``seq_append_infinite``);

val () = add_binder ("seq",1);

val () = add_infix ("|",20,HOLgrammars.RIGHT);

val () = add_infix ("#",350,HOLgrammars.RIGHT);

(* ------------------------------------------------------------------------- *)
(* Inferring types for vectors.                                              *)
(* ------------------------------------------------------------------------- *)

val V_tm = ``V``;

fun dest_V tm =
    let
      val (c,a) = dest_comb tm
      val _ = same_const c V_tm orelse raise ERR "dest_V" ""
      val ty = type_of tm
      val b = hd (tl (snd (dest_type ty)))
    in
      (a,b)
    end;

fun list_length tm =
    if listSyntax.is_nil tm then 0
    else if listSyntax.is_cons tm then 1 + list_length (rand tm)
    else raise ERR "list_length" "";

fun infer_vector_type tm =
    let
      val (l,ty) = dest_V tm
      val n = list_length l
      val ty' = fcpLib.index_type (Arbnum.fromInt n)
      val _ = ty <> ty' orelse raise ERR "infer_vector_type" ""
    in
      inst [ty |-> ty']
    end;

val () = add_preprocessor (total infer_vector_type);

(* ------------------------------------------------------------------------- *)
(* The micro Cryptol implementation of the Fibonacci sequence.               *)
(* ------------------------------------------------------------------------- *)

(*
Made up by JEH, so syntax might not be quite right.

fib = [0 1] # [| x + y || x <- drop (1,fib) || y <- fib |]
*)

(* ------------------------------------------------------------------------- *)
(* The lambda-lifted indexed stream form (i.e., streams represented as       *)
(* functions from num to 'a) of the Fibonacci function shallowly             *)
(* embedded into HOL4.                                                       *)
(* ------------------------------------------------------------------------- *)

val fib_def = (Define o preprocess_quotation)
  `fib i : word32 =
   if i < 2 then V [0w; 1w] %% i
   else fib (i - 1) + fib (i - 2)`;

(* ------------------------------------------------------------------------- *)
(* The ACL2 version of the Fibonacci function.                               *)
(* ------------------------------------------------------------------------- *)

(*
;; This is the function that the compiler should generate from
;; the fibs.mcr example file, for the version of fibs that is
;; in indexed recursive stream style.

(defun fibs1 (i)
  (cond
   ((not (acl2::natp i))
    nil)
   ((< i 2)
    (nth (logand i #x1) `(0 1)))
   (t
    (logand (+ (fibs1 (+ i -1))
               (fibs1 (+ i -2)))
            #xff))))
*)

(* ------------------------------------------------------------------------- *)
(* A Cryptol-like version of the Fibonacci function.                         *)
(* ------------------------------------------------------------------------- *)

val fib = prove
  (preprocess_term
   ``fib = V[0w; 1w] # (seq (x,y). x + y) (drop 1 fib | fib)``,
   RW_TAC std_ss [FUN_EQ_THM]
   ++ CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [fib_def]))
   ++ RW_TAC std_ss [seq_append_infinite_def, V_def, FCP_BETA, dimindex_2]
   ++ RW_TAC std_ss [seq_map_def, seq_zip_def, seq_drop_def]
   ++ MATCH_MP_TAC (PROVE [] ``(a = c) /\ (b = d) ==> (a + b = c + d)``)
   ++ CONJ_TAC
   ++ AP_TERM_TAC
   ++ DECIDE_TAC);

(* ------------------------------------------------------------------------- *)
(* The micro Cryptol implementation of TEA.                                  *)
(* ------------------------------------------------------------------------- *)

(*
From page 2 of "A language for symmetric-key cryptographic algorithms and
its efficient implementation" by Mark Shields.

exports code;

N = 32;
W = 32;
Word = B^W;
Block = Word^2;
Key = Word^4;
Index = B^W;

delta : Word;
delta = 0x9e3779b9;

code : (Block, Key) -> Block;
code ([v0, v1], k) = [ys@@N, zs@@N] where {
  rec sums : Word^inf;
  sums = [0] ##
         [ sum + delta | sum <- sums ];
  and ys : Word^inf;
  ys = [v0] ##
       [ y+((z<<4)+k@0 ^^ z+sum ^^ (z>>5)+k@1)
       | sum <- drops{1} sums 
       | y <- ys 
       | z <- zs ];
  and zs : Word^inf;
  zs = [v1] ##
       [ z+((y<<4)+k@2 ^^ y+sum ^^ (y>>5)+k@3)
       | sum <- drops{1} sums 
       | y <- drops{1} ys 
       | z <- zs ];
};
*)

(* ------------------------------------------------------------------------- *)
(* The lambda-lifted indexed stream form of TEA shallowly embedded into      *)
(* HOL4.                                                                     *)
(* ------------------------------------------------------------------------- *)

val tea_N_def = Define `tea_N = 32`;

val () = type_abbrev ("tea_W", Type `:32`);

val () = type_abbrev ("tea_Word", Type `:bool ** tea_W`);

val () = type_abbrev ("tea_Block", Type `:tea_Word ** 2`);

val () = type_abbrev ("tea_Key", Type `:tea_Word ** 4`);

val () = type_abbrev ("tea_Index", Type `:bool ** tea_W`);

val tea_delta_def = Define `tea_delta : tea_Word = 0x9e3779b9w`;

val (tea_inner_def,tea_inner_ind) = Defn.tprove
 (Defn.Hol_defn "tea_inner"
  `(tea_sums (v : tea_Block) (k : tea_Key) i =
    if i < 1 then 0w
    else
      let sum = tea_sums v k (i - 1)
      in sum + tea_delta)
   /\
   (tea_ys v k i =
    if i < 1 then v %% 0
    else
      let sum = tea_sums v k i in
      let y = tea_ys v k (i - 1) in
      let z = tea_zs v k (i - 1) in
      y + (((z << 4) + (k %% 0)) ?? (z + sum) ?? ((z >> 5) + (k %% 1))))
   /\
   (tea_zs v k i =
    if i < 1 then v %% 1
    else
      let sum = tea_sums v k i in
      let y = tea_ys v k i in
      let z = tea_zs v k (i - 1) in
      z + (((y << 4) + (k %% 2)) ?? (y + sum) ?? ((y >> 5) + (k %% 3))))`,
   TotalDefn.WF_REL_TAC
     `measure (\x. case x of INL (v,k,i) -> 3 * i + 1
                          || INR (INL (v,k,i)) -> 3 * i + 2
                          || INR (INR (v,k,i)) -> 3 * i + 3)`);

(* ------------------------------------------------------------------------- *)
(* Rewriting the definition of TEA to look like Cryptol                      *)
(* ------------------------------------------------------------------------- *)

val tea_sums = prove
  (preprocess_term
   ``(tea_sums v k : tea_Word inf) =
       V[0w] # (seq x. x + tea_delta) (tea_sums v k)``,
   RW_TAC std_ss [FUN_EQ_THM]
   ++ CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [tea_inner_def]))
   ++ RW_TAC std_ss [seq_append_infinite_def, V_def, FCP_BETA, index_one]
   >> (Know `x = 0` >> DECIDE_TAC
       ++ RW_TAC std_ss [EL, HD])
   ++ RW_TAC std_ss [seq_map_def, seq_zip_def, seq_drop_def]);

val tea_ys = prove
  (preprocess_term
   ``(tea_ys v k : tea_Word inf) =
       V[v %% 0] #
       (seq (sum,y,z).
        y + (((z << 4) + (k %% 0)) ?? (z + sum) ?? ((z >> 5) + (k %% 1))))
       (drop 1 (tea_sums v k) | (tea_ys v k | tea_zs v k))``,
   RW_TAC std_ss [FUN_EQ_THM]
   ++ CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [tea_inner_def]))
   ++ RW_TAC std_ss [seq_append_infinite_def, V_def, FCP_BETA, index_one]
   >> (Know `x = 0` >> DECIDE_TAC
       ++ RW_TAC std_ss [EL, HD])
   ++ RW_TAC std_ss [seq_map_def, seq_zip_def, seq_drop_def]
   ++ Q.UNABBREV_ALL_TAC
   ++ RW_TAC arith_ss []);

val tea_zs = prove
  (preprocess_term
   ``(tea_zs v k : tea_Word inf) =
       V[v %% 1] #
       (seq (sum,y,z).
        z + (((y << 4) + (k %% 2)) ?? (y + sum) ?? ((y >> 5) + (k %% 3))))
       (drop 1 (tea_sums v k) | (drop 1 (tea_ys v k) | tea_zs v k))``,
   RW_TAC std_ss [FUN_EQ_THM]
   ++ CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [tea_inner_def]))
   ++ RW_TAC std_ss [seq_append_infinite_def, V_def, FCP_BETA, index_one]
   >> (Know `x = 0` >> DECIDE_TAC
       ++ RW_TAC std_ss [EL, HD])
   ++ RW_TAC std_ss [seq_map_def, seq_zip_def, seq_drop_def]
   ++ Q.UNABBREV_ALL_TAC
   ++ RW_TAC arith_ss []);

val tea_def = (Define o preprocess_quotation)
  `(tea : tea_Block # tea_Key -> tea_Block) (v,k) =
     V[tea_ys v k tea_N; tea_zs v k tea_N]`;

val () = export_theory ();