(* This code extends 'std_prelude'. *)

Dlet (Pvar "word_add")
  (Fun "v1"
     (Fun "v2"
        (Let "x" (App (Opn Plus) (Var "v1") (Var "v2"))
           (App (Opn Modulo) (Var "x")
              (Val (Lit (IntLit 4294967296)))))))

Dlet (Pvar "word_mul")
  (Fun "v1"
     (Fun "v2"
        (Let "x" (App (Opn Times) (Var "v1") (Var "v2"))
           (App (Opn Modulo) (Var "x")
              (Val (Lit (IntLit 4294967296)))))))

Dlet (Pvar "word_add_1")
  (Fun "v1"
     (Fun "v2"
        (Let "x" (App (Opn Plus) (Var "v1") (Var "v2"))
           (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536)))))))

Dlet (Pvar "word_mul_1")
  (Fun "v1"
     (Fun "v2"
        (Let "x" (App (Opn Times) (Var "v1") (Var "v2"))
           (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536)))))))

Dlet (Pvar "word_add_2")
  (Fun "v1"
     (Fun "v2"
        (Let "x" (App (Opn Plus) (Var "v1") (Var "v2"))
           (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))))

Dlet (Pvar "word_mul_2")
  (Fun "v1"
     (Fun "v2"
        (Let "x" (App (Opn Times) (Var "v1") (Var "v2"))
           (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))))

Dletrec
  [("BITWISE","v1",
    Fun "v2"
      (Fun "v3"
         (Fun "v4"
            (If (App (Opb Leq) (Var "v1") (Val (Lit (IntLit 0))))
               (Val (Lit (IntLit 0)))
               (App (Opn Plus)
                  (App Opapp
                     (App Opapp
                        (App Opapp
                           (App Opapp (Var "BITWISE")
                              (App (Opn Minus) (Var "v1")
                                 (Val (Lit (IntLit 1))))) (Var "v2"))
                        (Var "v3")) (Var "v4"))
                  (App Opapp
                     (App Opapp (Var "SBIT")
                        (App Opapp
                           (App Opapp (Var "v2")
                              (App Opapp
                                 (App Opapp (Var "BIT")
                                    (App (Opn Minus) (Var "v1")
                                       (Val (Lit (IntLit 1)))))
                                 (Var "v3")))
                           (App Opapp
                              (App Opapp (Var "BIT")
                                 (App (Opn Minus) (Var "v1")
                                    (Val (Lit (IntLit 1)))))
                              (Var "v4"))))
                     (App (Opn Minus) (Var "v1")
                        (Val (Lit (IntLit 1))))))))))]

Dlet (Pvar "word_xor")
  (Fun "v4"
     (Fun "v3"
        (Let "x"
           (App Opapp
              (App Opapp
                 (App Opapp
                    (App Opapp (Var "BITWISE") (Val (Lit (IntLit 32))))
                    (Fun "v2"
                       (Fun "v1"
                          (App Equality
                             (App Equality (Var "v2") (Var "v1"))
                             (Val (Lit (Bool F))))))) (Var "v4"))
              (Var "v3"))
           (App (Opn Modulo) (Var "x")
              (Val (Lit (IntLit 4294967296)))))))

Dlet (Pvar "word_xor_1")
  (Fun "v4"
     (Fun "v3"
        (Let "x"
           (App Opapp
              (App Opapp
                 (App Opapp
                    (App Opapp (Var "BITWISE") (Val (Lit (IntLit 8))))
                    (Fun "v2"
                       (Fun "v1"
                          (App Equality
                             (App Equality (Var "v2") (Var "v1"))
                             (Val (Lit (Bool F))))))) (Var "v4"))
              (Var "v3"))
           (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))))

Dlet (Pvar "word_xor_2")
  (Fun "v4"
     (Fun "v3"
        (Let "x"
           (App Opapp
              (App Opapp
                 (App Opapp
                    (App Opapp (Var "BITWISE") (Val (Lit (IntLit 16))))
                    (Fun "v2"
                       (Fun "v1"
                          (App Equality
                             (App Equality (Var "v2") (Var "v1"))
                             (Val (Lit (Bool F))))))) (Var "v4"))
              (Var "v3"))
           (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536)))))))

Dlet (Pvar "word_or")
  (Fun "v4"
     (Fun "v3"
        (Let "x"
           (App Opapp
              (App Opapp
                 (App Opapp
                    (App Opapp (Var "BITWISE") (Val (Lit (IntLit 32))))
                    (Fun "v2"
                       (Fun "v1" (Log Or (Var "v2") (Var "v1")))))
                 (Var "v4")) (Var "v3"))
           (App (Opn Modulo) (Var "x")
              (Val (Lit (IntLit 4294967296)))))))

Dlet (Pvar "word_or_1")
  (Fun "v4"
     (Fun "v3"
        (Let "x"
           (App Opapp
              (App Opapp
                 (App Opapp
                    (App Opapp (Var "BITWISE") (Val (Lit (IntLit 16))))
                    (Fun "v2"
                       (Fun "v1" (Log Or (Var "v2") (Var "v1")))))
                 (Var "v4")) (Var "v3"))
           (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536)))))))

Dlet (Pvar "word_and")
  (Fun "v4"
     (Fun "v3"
        (Let "x"
           (App Opapp
              (App Opapp
                 (App Opapp
                    (App Opapp (Var "BITWISE") (Val (Lit (IntLit 32))))
                    (Fun "v2"
                       (Fun "v1" (Log And (Var "v2") (Var "v1")))))
                 (Var "v4")) (Var "v3"))
           (App (Opn Modulo) (Var "x")
              (Val (Lit (IntLit 4294967296)))))))

Dlet (Pvar "word_lsl")
  (Fun "v1"
     (Fun "v2"
        (App Opapp
           (App Opapp (Var "word_mul")
              (Let "x"
                 (App Opapp
                    (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                    (Var "v2"))
                 (App (Opn Modulo) (Var "x")
                    (Val (Lit (IntLit 4294967296)))))) (Var "v1"))))

Dlet (Pvar "word_lsl_1")
  (Fun "v1"
     (Fun "v2"
        (App Opapp
           (App Opapp (Var "word_mul_1")
              (Let "x"
                 (App Opapp
                    (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                    (Var "v2"))
                 (App (Opn Modulo) (Var "x")
                    (Val (Lit (IntLit 65536)))))) (Var "v1"))))

Dlet (Pvar "word_lsl_2")
  (Fun "v1"
     (Fun "v2"
        (App Opapp
           (App Opapp (Var "word_mul_2")
              (Let "x"
                 (App Opapp
                    (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                    (Var "v2"))
                 (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256))))))
           (Var "v1"))))

Dlet (Pvar "word_lsr")
  (Fun "v2"
     (Fun "v1"
        (Let "x"
           (App (Opn Divide) (Var "v2")
              (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                 (Var "v1")))
           (App (Opn Modulo) (Var "x")
              (Val (Lit (IntLit 4294967296)))))))

Dlet (Pvar "word_lsr_1")
  (Fun "v2"
     (Fun "v1"
        (Let "x"
           (App (Opn Divide) (Var "v2")
              (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                 (Var "v1")))
           (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536)))))))

Dlet (Pvar "word_lsr_2")
  (Fun "v2"
     (Fun "v1"
        (Let "x"
           (App (Opn Divide) (Var "v2")
              (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2))))
                 (Var "v1")))
           (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))))

Dlet (Pvar "word_msb")
  (Fun "v1"
     (App Opapp (App Opapp (Var "BIT") (Val (Lit (IntLit 31))))
        (Var "v1")))

Dlet (Pvar "word_msb_1")
  (Fun "v1"
     (App Opapp (App Opapp (Var "BIT") (Val (Lit (IntLit 15))))
        (Var "v1")))

Dlet (Pvar "word_msb_2")
  (Fun "v1"
     (App Opapp (App Opapp (Var "BIT") (Val (Lit (IntLit 7))))
        (Var "v1")))

Dlet (Pvar "word_lsb")
  (Fun "v1"
     (App Equality
        (App (Opb Leq)
           (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2))))
           (Val (Lit (IntLit 0)))) (Val (Lit (Bool F)))))

Dlet (Pvar "word_lsb_1")
  (Fun "v1"
     (App Equality
        (App (Opb Leq)
           (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2))))
           (Val (Lit (IntLit 0)))) (Val (Lit (Bool F)))))

Dlet (Pvar "word_lsb_2")
  (Fun "v1"
     (App Equality
        (App (Opb Leq)
           (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2))))
           (Val (Lit (IntLit 0)))) (Val (Lit (Bool F)))))

Dlet (Pvar "word_asr")
  (Fun "v2"
     (Fun "v1"
        (If (App Opapp (Var "word_msb") (Var "v2"))
           (App Opapp
              (App Opapp (Var "word_or")
                 (Let "x"
                    (Let "k"
                       (App (Opn Minus) (Val (Lit (IntLit 4294967296)))
                          (App Opapp
                             (App Opapp (Var "EXP")
                                (Val (Lit (IntLit 2))))
                             (Let "k"
                                (App (Opn Minus) (Val (Lit (IntLit 32)))
                                   (App Opapp
                                      (App Opapp (Var "MIN") (Var "v1"))
                                      (Val (Lit (IntLit 32)))))
                                (If
                                   (App (Opb Lt) (Var "k")
                                      (Val (Lit (IntLit 0))))
                                   (Val (Lit (IntLit 0))) (Var "k")))))
                       (If
                          (App (Opb Lt) (Var "k")
                             (Val (Lit (IntLit 0))))
                          (Val (Lit (IntLit 0))) (Var "k")))
                    (App (Opn Modulo) (Var "x")
                       (Val (Lit (IntLit 4294967296))))))
              (App Opapp (App Opapp (Var "word_lsr") (Var "v2"))
                 (Var "v1")))
           (App Opapp (App Opapp (Var "word_lsr") (Var "v2"))
              (Var "v1")))))

Dlet (Pvar "word_asr_1")
  (Fun "v2"
     (Fun "v1"
        (If (App Opapp (Var "word_msb_1") (Var "v2"))
           (App Opapp
              (App Opapp (Var "word_or_1")
                 (Let "x"
                    (Let "k"
                       (App (Opn Minus) (Val (Lit (IntLit 65536)))
                          (App Opapp
                             (App Opapp (Var "EXP")
                                (Val (Lit (IntLit 2))))
                             (Let "k"
                                (App (Opn Minus) (Val (Lit (IntLit 16)))
                                   (App Opapp
                                      (App Opapp (Var "MIN") (Var "v1"))
                                      (Val (Lit (IntLit 16)))))
                                (If
                                   (App (Opb Lt) (Var "k")
                                      (Val (Lit (IntLit 0))))
                                   (Val (Lit (IntLit 0))) (Var "k")))))
                       (If
                          (App (Opb Lt) (Var "k")
                             (Val (Lit (IntLit 0))))
                          (Val (Lit (IntLit 0))) (Var "k")))
                    (App (Opn Modulo) (Var "x")
                       (Val (Lit (IntLit 65536))))))
              (App Opapp (App Opapp (Var "word_lsr_1") (Var "v2"))
                 (Var "v1")))
           (App Opapp (App Opapp (Var "word_lsr_1") (Var "v2"))
              (Var "v1")))))

Dlet (Pvar "word_sub")
  (Fun "v1"
     (Fun "v2"
        (App Opapp (App Opapp (Var "word_add") (Var "v1"))
           (Let "x"
              (Let "k"
                 (App (Opn Minus) (Val (Lit (IntLit 4294967296)))
                    (Var "v2"))
                 (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
                    (Val (Lit (IntLit 0))) (Var "k")))
              (App (Opn Modulo) (Var "x")
                 (Val (Lit (IntLit 4294967296))))))))

Dlet (Pvar "word_sub_1")
  (Fun "v1"
     (Fun "v2"
        (App Opapp (App Opapp (Var "word_add_1") (Var "v1"))
           (Let "x"
              (Let "k"
                 (App (Opn Minus) (Val (Lit (IntLit 65536))) (Var "v2"))
                 (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
                    (Val (Lit (IntLit 0))) (Var "k")))
              (App (Opn Modulo) (Var "x")
                 (Val (Lit (IntLit 65536))))))))

Dlet (Pvar "word_sub_2")
  (Fun "v1"
     (Fun "v2"
        (App Opapp (App Opapp (Var "word_add_2") (Var "v1"))
           (Let "x"
              (Let "k"
                 (App (Opn Minus) (Val (Lit (IntLit 256))) (Var "v2"))
                 (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
                    (Val (Lit (IntLit 0))) (Var "k")))
              (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256))))))))

Dlet (Pvar "word_bits")
  (Fun "v1"
     (Fun "v2"
        (Fun "v3"
           (Let "x"
              (App Opapp
                 (App Opapp
                    (App Opapp (Var "BITS")
                       (App Opapp (App Opapp (Var "MIN") (Var "v1"))
                          (Val (Lit (IntLit 31))))) (Var "v2"))
                 (Var "v3"))
              (App (Opn Modulo) (Var "x")
                 (Val (Lit (IntLit 4294967296))))))))

Dlet (Pvar "word_ror")
  (Fun "v3"
     (Fun "v2"
        (Let "v1" (App (Opn Modulo) (Var "v2") (Val (Lit (IntLit 32))))
           (App Opapp
              (App Opapp (Var "word_or")
                 (App Opapp
                    (App Opapp
                       (App Opapp (Var "word_bits")
                          (Val (Lit (IntLit 31)))) (Var "v1"))
                    (Var "v3")))
              (App Opapp
                 (App Opapp (Var "word_lsl")
                    (App Opapp
                       (App Opapp
                          (App Opapp (Var "word_bits")
                             (Let "k"
                                (App (Opn Minus) (Var "v1")
                                   (Val (Lit (IntLit 1))))
                                (If
                                   (App (Opb Lt) (Var "k")
                                      (Val (Lit (IntLit 0))))
                                   (Val (Lit (IntLit 0))) (Var "k"))))
                          (Val (Lit (IntLit 0)))) (Var "v3")))
                 (Let "k"
                    (App (Opn Minus) (Val (Lit (IntLit 32))) (Var "v1"))
                    (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
                       (Val (Lit (IntLit 0))) (Var "k"))))))))

Dlet (Pvar "word_rol")
  (Fun "v2"
     (Fun "v1"
        (App Opapp (App Opapp (Var "word_ror") (Var "v2"))
           (Let "k"
              (App (Opn Minus) (Val (Lit (IntLit 32)))
                 (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 32)))))
              (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
                 (Val (Lit (IntLit 0))) (Var "k"))))))