(* This code extends 'word_prelude'. *)

let GETKEYS = 
  (fun v87 -> 
    (match v87 with 
        (Pair (v86, v85)) -> 
          (match v85 with 
              (Pair (v84, v83)) -> 
                (match v83 with 
                    (Pair (v82, v81)) -> 
                      (match v81 with 
                          (Pair (v80, v79)) -> 
                            (match v79 with 
                              (Pair (v78, v77)) -> 
                              (match v77 with 
                              (Pair (v76, v75)) -> 
                              (match v75 with 
                              (Pair (v74, v73)) -> 
                              (match v73 with 
                              (Pair (v72, v71)) -> 
                              (match v71 with 
                              (Pair (v70, v69)) -> 
                              (match v69 with 
                              (Pair (v68, v67)) -> 
                              (match v67 with 
                              (Pair (v66, v65)) -> 
                              (match v65 with 
                              (Pair (v64, v63)) -> 
                              (match v63 with 
                              (Pair (v62, v61)) -> 
                              (match v61 with 
                              (Pair (v60, v59)) -> 
                              (match v59 with 
                              (Pair (v58, v57)) -> 
                              (match v57 with 
                              (Pair (v56, v55)) -> 
                              (match v55 with 
                              (Pair (v54, v53)) -> 
                              (match v53 with 
                              (Pair (v52, v51)) -> 
                              (match v51 with 
                              (Pair (v50, v49)) -> 
                              (match v49 with 
                              (Pair (v48, v47)) -> 
                              (match v47 with 
                              (Pair (v46, v45)) -> 
                              (match v45 with 
                              (Pair (v44, v43)) -> 
                              (match v43 with 
                              (Pair (v42, v41)) -> 
                              (match v41 with 
                              (Pair (v40, v39)) -> 
                              (match v39 with 
                              (Pair (v38, v37)) -> 
                              (match v37 with 
                              (Pair (v36, v35)) -> 
                              (match v35 with 
                              (Pair (v34, v33)) -> 
                              (match v33 with 
                              (Pair (v32, v31)) -> 
                              (match v31 with 
                              (Pair (v30, v29)) -> 
                              (match v29 with 
                              (Pair (v28, v27)) -> 
                              (match v27 with 
                              (Pair (v26, v25)) -> 
                              (match v25 with 
                              (Pair (v24, v23)) -> 
                              (match v23 with 
                              (Pair (v22, v21)) -> 
                              (match v21 with 
                              (Pair (v20, v19)) -> 
                              (match v19 with 
                              (Pair (v18, v17)) -> 
                              (match v17 with 
                              (Pair (v16, v15)) -> 
                              (match v15 with 
                              (Pair (v14, v13)) -> 
                              (match v13 with 
                              (Pair (v12, v11)) -> 
                              (match v11 with 
                              (Pair (v10, v9)) -> 
                              (match v9 with 
                              (Pair (v8, v7)) -> 
                              (match v7 with 
                              (Pair (v6, v5)) -> 
                              (match v5 with 
                              (Pair (v4, v3)) -> 
                              (match v3 with 
                              (Pair (v2, v1)) -> (Pair (v86, v84)))))))))))))))))))))))))))))))))))))))))))))) ;;

let PreWhitening = 
  (fun v7 -> 
    (fun v8 -> 
      (match v8 with 
          (Pair (v6, v5)) -> 
            (match v5 with 
                (Pair (v4, v3)) -> 
                  (match v3 with 
                      (Pair (v2, v1)) -> (Pair (v6, (Pair (((word_add v4) (FST (GETKEYS v7))), (Pair (v2, ((word_add v1) (SND (GETKEYS v7)))))))))))))) ;;

let ROTKEYS = 
  (fun v87 -> 
    (match v87 with 
        (Pair (v86, v85)) -> 
          (match v85 with 
              (Pair (v84, v83)) -> 
                (match v83 with 
                    (Pair (v82, v81)) -> 
                      (match v81 with 
                          (Pair (v80, v79)) -> 
                            (match v79 with 
                              (Pair (v78, v77)) -> 
                              (match v77 with 
                              (Pair (v76, v75)) -> 
                              (match v75 with 
                              (Pair (v74, v73)) -> 
                              (match v73 with 
                              (Pair (v72, v71)) -> 
                              (match v71 with 
                              (Pair (v70, v69)) -> 
                              (match v69 with 
                              (Pair (v68, v67)) -> 
                              (match v67 with 
                              (Pair (v66, v65)) -> 
                              (match v65 with 
                              (Pair (v64, v63)) -> 
                              (match v63 with 
                              (Pair (v62, v61)) -> 
                              (match v61 with 
                              (Pair (v60, v59)) -> 
                              (match v59 with 
                              (Pair (v58, v57)) -> 
                              (match v57 with 
                              (Pair (v56, v55)) -> 
                              (match v55 with 
                              (Pair (v54, v53)) -> 
                              (match v53 with 
                              (Pair (v52, v51)) -> 
                              (match v51 with 
                              (Pair (v50, v49)) -> 
                              (match v49 with 
                              (Pair (v48, v47)) -> 
                              (match v47 with 
                              (Pair (v46, v45)) -> 
                              (match v45 with 
                              (Pair (v44, v43)) -> 
                              (match v43 with 
                              (Pair (v42, v41)) -> 
                              (match v41 with 
                              (Pair (v40, v39)) -> 
                              (match v39 with 
                              (Pair (v38, v37)) -> 
                              (match v37 with 
                              (Pair (v36, v35)) -> 
                              (match v35 with 
                              (Pair (v34, v33)) -> 
                              (match v33 with 
                              (Pair (v32, v31)) -> 
                              (match v31 with 
                              (Pair (v30, v29)) -> 
                              (match v29 with 
                              (Pair (v28, v27)) -> 
                              (match v27 with 
                              (Pair (v26, v25)) -> 
                              (match v25 with 
                              (Pair (v24, v23)) -> 
                              (match v23 with 
                              (Pair (v22, v21)) -> 
                              (match v21 with 
                              (Pair (v20, v19)) -> 
                              (match v19 with 
                              (Pair (v18, v17)) -> 
                              (match v17 with 
                              (Pair (v16, v15)) -> 
                              (match v15 with 
                              (Pair (v14, v13)) -> 
                              (match v13 with 
                              (Pair (v12, v11)) -> 
                              (match v11 with 
                              (Pair (v10, v9)) -> 
                              (match v9 with 
                              (Pair (v8, v7)) -> 
                              (match v7 with 
                              (Pair (v6, v5)) -> 
                              (match v5 with 
                              (Pair (v4, v3)) -> 
                              (match v3 with 
                              (Pair (v2, v1)) -> (Pair (v82, (Pair (v80, (Pair (v78, (Pair (v76, (Pair (v74, (Pair (v72, (Pair (v70, (Pair (v68, (Pair (v66, (Pair (v64, (Pair (v62, (Pair (v60, (Pair (v58, (Pair (v56, (Pair (v54, (Pair (v52, (Pair (v50, (Pair (v48, (Pair (v46, (Pair (v44, (Pair (v42, (Pair (v40, (Pair (v38, (Pair (v36, (Pair (v34, (Pair (v32, (Pair (v30, (Pair (v28, (Pair (v26, (Pair (v24, (Pair (v22, (Pair (v20, (Pair (v18, (Pair (v16, (Pair (v14, (Pair (v12, (Pair (v10, (Pair (v8, (Pair (v6, (Pair (v4, (Pair (v2, (Pair (v1, (Pair (v86, v84)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ;;

let InvPostWhitening = 
  (fun v7 -> 
    (fun v8 -> 
      (match v8 with 
          (Pair (v6, v5)) -> 
            (match v5 with 
                (Pair (v4, v3)) -> 
                  (match v3 with 
                      (Pair (v2, v1)) -> (Pair (v6, (Pair (((word_sub v4) (FST (GETKEYS v7))), (Pair (v2, ((word_sub v1) (SND (GETKEYS v7)))))))))))))) ;;

let InvPreWhitening = 
  (fun v7 -> 
    (fun v8 -> 
      (match v8 with 
          (Pair (v6, v5)) -> 
            (match v5 with 
                (Pair (v4, v3)) -> 
                  (match v3 with 
                      (Pair (v2, v1)) -> (Pair (((word_sub v6) (SND (GETKEYS v7))), (Pair (v4, (Pair (((word_sub v2) (SND (GETKEYS v7))), v1))))))))))) ;;

let RightShift = 
  (fun v2 -> 
    (fun v1 -> ((word_ror v2) v1))) ;;

let LeftShift = 
  (fun v2 -> 
    (fun v1 -> ((word_rol v2) v1))) ;;

let CompUT = 
  (fun v1 -> ((word_rol ((word_mul v1) ((word_add ((word_add v1) v1)) 
    (let x = 1 
    in (x mod 4294967296))))) 5)) ;;

let FwdRound = 
  (fun v10 -> 
    (fun v9 -> 
      (match v10 with 
          (Pair (v8, v7)) -> 
            (match v7 with 
                (Pair (v6, v5)) -> 
                  (match v5 with 
                      (Pair (v4, v3)) -> 
                        (match v9 with 
                            (Pair (v2, v1)) -> (Pair (v6, (Pair (((word_add ((LeftShift ((word_xor v4) (CompUT v3))) (CompUT v6))) v1), (Pair (v3, ((word_add ((LeftShift ((word_xor v8) (CompUT v6))) (CompUT v3))) v2))))))))))))) ;;

let BwdRound = 
  (fun v10 -> 
    (fun v9 -> 
      (match v10 with 
          (Pair (v8, v7)) -> 
            (match v7 with 
                (Pair (v6, v5)) -> 
                  (match v5 with 
                      (Pair (v4, v3)) -> 
                        (match v9 with 
                            (Pair (v2, v1)) -> (Pair (((word_xor ((RightShift ((word_sub v3) v2)) (CompUT v4))) (CompUT v8)), (Pair (v8, (Pair (((word_xor ((RightShift ((word_sub v6) v1)) (CompUT v8))) (CompUT v4)), v4)))))))))))) ;;

let PostWhitening = 
  (fun v7 -> 
    (fun v8 -> 
      (match v8 with 
          (Pair (v6, v5)) -> 
            (match v5 with 
                (Pair (v4, v3)) -> 
                  (match v3 with 
                      (Pair (v2, v1)) -> (Pair (((word_add v6) (SND (GETKEYS v7))), (Pair (v4, (Pair (((word_add v2) (SND (GETKEYS v7))), v1))))))))))) ;;

let rec Round v3 = 
  (fun v2 -> 
    (fun v1 -> 
      (if (v3 <= 0) 
      then ((PostWhitening v2) v1) 
      else (((Round (v3 - 1)) (ROTKEYS v2)) ((FwdRound v1) (GETKEYS v2)))))) ;;

let rec InvRound v3 = 
  (fun v2 -> 
    (fun v1 -> 
      (if (v3 <= 0) 
      then ((InvPreWhitening v2) v1) 
      else ((BwdRound (((InvRound (v3 - 1)) (ROTKEYS v2)) v1)) (GETKEYS v2))))) ;;

let r = 20 ;;

let RC6_FWD = 
  (fun v1 -> ((o ((Round r) v1)) (PreWhitening v1))) ;;

let RC6_BWD = 
  (fun v1 -> ((o (InvPostWhitening v1)) ((InvRound r) v1))) ;;