(* This code extends 'word_prelude'. *)

Dlet (Pvar "ShiftXor")
  (Fun "v7"
     (Mat (Var "v7")
        [(Pcon "Pair" [Pvar "v6"; Pvar "v5"],
          Mat (Var "v5")
            [(Pcon "Pair" [Pvar "v4"; Pvar "v3"],
              Mat (Var "v3")
                [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],
                  App Opapp
                    (App Opapp (Var "word_xor")
                       (App Opapp
                          (App Opapp (Var "word_add")
                             (App Opapp
                                (App Opapp (Var "word_lsl") (Var "v6"))
                                (Val (Lit (IntLit 4))))) (Var "v2")))
                    (App Opapp
                       (App Opapp (Var "word_xor")
                          (App Opapp
                             (App Opapp (Var "word_add") (Var "v6"))
                             (Var "v4")))
                       (App Opapp
                          (App Opapp (Var "word_add")
                             (App Opapp
                                (App Opapp (Var "word_asr") (Var "v6"))
                                (Val (Lit (IntLit 5)))))
                          (Var "v1"))))])])]))

Dlet (Pvar "Round")
  (Fun "v15"
     (Mat (Var "v15")
        [(Pcon "Pair" [Pvar "v14"; Pvar "v13"],
          Mat (Var "v14")
            [(Pcon "Pair" [Pvar "v12"; Pvar "v11"],
              Mat (Var "v13")
                [(Pcon "Pair" [Pvar "v10"; Pvar "v9"],
                  Mat (Var "v10")
                    [(Pcon "Pair" [Pvar "v8"; Pvar "v7"],
                      Mat (Var "v7")
                        [(Pcon "Pair" [Pvar "v6"; Pvar "v5"],
                          Mat (Var "v5")
                            [(Pcon "Pair" [Pvar "v4"; Pvar "v3"],
                              Let "v2"
                                (App Opapp
                                   (App Opapp (Var "word_add")
                                      (Var "v9"))
                                   (Let "x"
                                      (Val (Lit (IntLit 2654435769)))
                                      (App (Opn Modulo) (Var "x")
                                         (Val
                                            (Lit
                                               (IntLit 4294967296))))))
                                (Let "v1"
                                   (App Opapp
                                      (App Opapp (Var "word_add")
                                         (Var "v12"))
                                      (App Opapp (Var "ShiftXor")
                                         (Con "Pair"
                                            [Var "v11";
                                             Con "Pair"
                                               [Var "v2";
                                                Con "Pair"
                                                  [Var "v8";
                                                   Var "v6"]]])))
                                   (Con "Pair"
                                      [Con "Pair"
                                         [Var "v1";
                                          App Opapp
                                            (App Opapp (Var "word_add")
                                               (Var "v11"))
                                            (App Opapp (Var "ShiftXor")
                                               (Con "Pair"
                                                  [Var "v1";
                                                   Con "Pair"
                                                     [Var "v2";
                                                      Con "Pair"
                                                        [Var "v4";
                                                         Var "v3"]]]))];
                                       Con "Pair"
                                         [Con "Pair"
                                            [Var "v8";
                                             Con "Pair"
                                               [Var "v6";
                                                Con "Pair"
                                                  [Var "v4";
                                                   Var "v3"]]];
                                          Var "v2"]])))])])])])])]))

Dlet (Pvar "InvRound")
  (Fun "v13"
     (Mat (Var "v13")
        [(Pcon "Pair" [Pvar "v12"; Pvar "v11"],
          Mat (Var "v12")
            [(Pcon "Pair" [Pvar "v10"; Pvar "v9"],
              Mat (Var "v11")
                [(Pcon "Pair" [Pvar "v8"; Pvar "v7"],
                  Mat (Var "v8")
                    [(Pcon "Pair" [Pvar "v6"; Pvar "v5"],
                      Mat (Var "v5")
                        [(Pcon "Pair" [Pvar "v4"; Pvar "v3"],
                          Mat (Var "v3")
                            [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],
                              Con "Pair"
                                [Con "Pair"
                                   [App Opapp
                                      (App Opapp (Var "word_sub")
                                         (Var "v10"))
                                      (App Opapp (Var "ShiftXor")
                                         (Con "Pair"
                                            [App Opapp
                                               (App Opapp
                                                  (Var "word_sub")
                                                  (Var "v9"))
                                               (App Opapp
                                                  (Var "ShiftXor")
                                                  (Con "Pair"
                                                     [Var "v10";
                                                      Con "Pair"
                                                        [Var "v7";
                                                         Con "Pair"
                                                           [Var "v2";
                                                            Var
                                                              "v1"]]]));
                                             Con "Pair"
                                               [Var "v7";
                                                Con "Pair"
                                                  [Var "v6";
                                                   Var "v4"]]]));
                                    App Opapp
                                      (App Opapp (Var "word_sub")
                                         (Var "v9"))
                                      (App Opapp (Var "ShiftXor")
                                         (Con "Pair"
                                            [Var "v10";
                                             Con "Pair"
                                               [Var "v7";
                                                Con "Pair"
                                                  [Var "v2";
                                                   Var "v1"]]]))];
                                 Con "Pair"
                                   [Con "Pair"
                                      [Var "v6";
                                       Con "Pair"
                                         [Var "v4";
                                          Con "Pair"
                                            [Var "v2"; Var "v1"]]];
                                    App Opapp
                                      (App Opapp (Var "word_sub")
                                         (Var "v7"))
                                      (Let "x"
                                         (Val (Lit (IntLit 2654435769)))
                                         (App (Opn Modulo) (Var "x")
                                            (Val
                                               (Lit
                                                  (IntLit
                                                     4294967296)))))]])])])])])])]))

Dletrec
  [("Rounds","v3",
    Mat (Var "v3")
      [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],
        If
          (App Equality (Var "v2")
             (Let "x" (Val (Lit (IntLit 0)))
                (App (Opn Modulo) (Var "x")
                   (Val (Lit (IntLit 4294967296)))))) (Var "v1")
          (App Opapp (Var "Rounds")
             (Con "Pair"
                [App Opapp (App Opapp (Var "word_sub") (Var "v2"))
                   (Let "x" (Val (Lit (IntLit 1)))
                      (App (Opn Modulo) (Var "x")
                         (Val (Lit (IntLit 4294967296)))));
                 App Opapp (Var "Round") (Var "v1")])))])]

Dletrec
  [("InvRounds","v3",
    Mat (Var "v3")
      [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],
        If
          (App Equality (Var "v2")
             (Let "x" (Val (Lit (IntLit 0)))
                (App (Opn Modulo) (Var "x")
                   (Val (Lit (IntLit 4294967296)))))) (Var "v1")
          (App Opapp (Var "InvRounds")
             (Con "Pair"
                [App Opapp (App Opapp (Var "word_sub") (Var "v2"))
                   (Let "x" (Val (Lit (IntLit 1)))
                      (App (Opn Modulo) (Var "x")
                         (Val (Lit (IntLit 4294967296)))));
                 App Opapp (Var "InvRound") (Var "v1")])))])]

Dlet (Pvar "teaEncrypt")
  (Fun "v8"
     (Mat (Var "v8")
        [(Pcon "Pair" [Pvar "v7"; Pvar "v6"],
          Let "v5"
            (App Opapp (Var "Rounds")
               (Con "Pair"
                  [Let "x" (Val (Lit (IntLit 32)))
                     (App (Opn Modulo) (Var "x")
                        (Val (Lit (IntLit 4294967296))));
                   Con "Pair"
                     [Var "v6";
                      Con "Pair"
                        [Var "v7";
                         Let "x" (Val (Lit (IntLit 0)))
                           (App (Opn Modulo) (Var "x")
                              (Val (Lit (IntLit 4294967296))))]]]))
            (Mat (Var "v5")
               [(Pcon "Pair" [Pvar "v4"; Pvar "v3"],
                 Mat (Var "v3")
                   [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],
                     Var "v4")])]))]))

Dlet (Pvar "teaDecrypt")
  (Fun "v8"
     (Mat (Var "v8")
        [(Pcon "Pair" [Pvar "v7"; Pvar "v6"],
          Let "v5"
            (App Opapp (Var "InvRounds")
               (Con "Pair"
                  [Let "x" (Val (Lit (IntLit 32)))
                     (App (Opn Modulo) (Var "x")
                        (Val (Lit (IntLit 4294967296))));
                   Con "Pair"
                     [Var "v6";
                      Con "Pair"
                        [Var "v7";
                         App Opapp
                           (App Opapp (Var "word_lsl")
                              (Let "x" (Val (Lit (IntLit 2654435769)))
                                 (App (Opn Modulo) (Var "x")
                                    (Val (Lit (IntLit 4294967296))))))
                           (Val (Lit (IntLit 5)))]]]))
            (Mat (Var "v5")
               [(Pcon "Pair" [Pvar "v4"; Pvar "v3"],
                 Mat (Var "v3")
                   [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],
                     Var "v4")])]))]))