Certificate theorem for EVEN:

|- DeclAssum example_primality_test_decls env ⇒
   Eval env (Var "EVEN") ((NUM --> BOOL) EVEN)

Definition of refinement invariant:

|- ∀a b x_2 x_1 v.
     PAIR_TYPE a b (x_2,x_1) v ⇔
     ∃v1_1 v1_2.
       (v = Conv "Pair" [v1_1; v1_2]) ∧ a x_2 v1_1 ∧ b x_1 v1_2

Certificate theorem for UNIT:

|- DeclAssum example_primality_test_decls env ⇒
   Eval env (Var "UNIT") ((b --> a --> PAIR_TYPE b a) UNIT)

Certificate theorem for BIND:

|- DeclAssum example_primality_test_decls env ⇒
   Eval env (Var "BIND")
     (((a --> PAIR_TYPE b a) --> (b --> a --> PAIR_TYPE c a) --> a -->
       PAIR_TYPE c a) BIND)

Certificate theorem for prob_while_cut:

|- DeclAssum example_primality_test_decls env ⇒
   Eval env (Var "prob_while_cut")
     (((b --> BOOL) --> (b --> a --> PAIR_TYPE b a) --> NUM --> b -->
       a --> PAIR_TYPE b a) prob_while_cut)

Certificate theorem for K:

|- DeclAssum example_primality_test_decls env ⇒
   Eval env (Var "K") ((a --> b --> a) K)

Certificate theorem for I:

|- DeclAssum example_primality_test_decls env ⇒
   Eval env (Var "I") ((a --> a) I)

Certificate theorem for many:

|- DeclAssum example_primality_test_decls env ⇒
   Eval env (Var "many")
     (((a --> PAIR_TYPE BOOL a) --> NUM --> a --> PAIR_TYPE BOOL a)
        many)

Certificate theorem for log2:

|- DeclAssum example_primality_test_decls env ⇒
   Eval env (Var "log2") ((NUM --> NUM) log2)

Certificate theorem for factor_twos:

|- DeclAssum example_primality_test_decls env ⇒
   Eval env (Var "factor_twos")
     ((NUM --> PAIR_TYPE NUM NUM) factor_twos)

Certificate theorem for modexp:

|- DeclAssum example_primality_test_decls env ∧ modexp_side v5 v3 v4 ⇒
   Eval env (Var "modexp")
     ((Eq NUM v5 --> Eq NUM v3 --> Eq NUM v4 --> NUM) modexp)

Definition of side condition for modexp:

|- modexp_side v1 v2 v3 ⇔
   case v3 of
     0 => T
   | SUC v__1 =>
       ((¬EVEN (SUC v__1) ⇒ v1 ≠ 0) ∧
        modexp_side v1 v2 (SUC v__1 DIV 2)) ∧ v1 ≠ 0

Certificate theorem for witness_tail:

|- DeclAssum example_primality_test_decls env ∧
   witness_tail_side v2 v3 v4 ⇒
   Eval env (Var "witness_tail")
     ((Eq NUM v2 --> Eq NUM v3 --> Eq NUM v4 --> BOOL) witness_tail)

Definition of side condition for witness_tail:

|- witness_tail_side v1 v2 v3 ⇔
   case v3 of
     0 => T
   | SUC v__1 =>
       ((v2 * v2) MOD v1 ≠ 1 ⇒
        witness_tail_side v1 ((v2 * v2) MOD v1) v__1) ∧ v1 ≠ 0

Certificate theorem for witness:

|- DeclAssum example_primality_test_decls env ∧ witness_side v5 v4 ⇒
   Eval env (Var "witness") ((Eq NUM v5 --> Eq NUM v4 --> BOOL) witness)

Definition of side condition for witness:

|- witness_side v5 v4 ⇔
   ∀v2 v1.
     (factor_twos (v5 − 1) = (v2,v1)) ⇒
     witness_tail_side v5 (modexp v5 v4 v1) v2 ∧ modexp_side v5 v4 v1

Certificate theorem for shd:

|- DeclAssum example_primality_test_decls env ⇒
   Eval env (Var "shd") (((NUM --> a) --> a) shd)

Certificate theorem for stl:

|- DeclAssum example_primality_test_decls env ⇒
   Eval env (Var "stl") (((NUM --> a) --> NUM --> a) stl)

Certificate theorem for prob_unif:

|- DeclAssum example_primality_test_decls env ⇒
   Eval env (Var "prob_unif")
     ((NUM --> (NUM --> BOOL) --> PAIR_TYPE NUM (NUM --> BOOL))
        prob_unif)

Certificate theorem for prob_uniform_cut:

|- DeclAssum example_primality_test_decls env ∧
   prob_uniform_cut_side x x1 x2 ⇒
   Eval env (Var "prob_uniform_cut")
     ((Eq NUM x --> Eq NUM x1 --> Eq (NUM --> BOOL) x2 -->
       PAIR_TYPE NUM (NUM --> BOOL)) prob_uniform_cut)

Definition of side condition for prob_uniform_cut:

|- prob_uniform_cut_side v1 v2 v3 ⇔
   case v1 of
     0 => v2 ≠ 0 ∧ ∃v__5. v2 = SUC v__5
   | SUC v__4 =>
       (v2 ≠ 0 ∧
        ∀v__3.
          (v2 = SUC v__3) ⇒
          ∀v__2 v__1.
            (prob_unif v__3 v3 = (v__2,v__1)) ⇒
            ¬(v__2 < v__3 + 1) ⇒
            prob_uniform_cut_side v__4 (v__3 + 1) v__1) ∧
       ∃v__6. v2 = SUC v__6

Certificate theorem for miller_rabin_1:

|- DeclAssum example_primality_test_decls env ∧
   miller_rabin_1_side v4 v5 ⇒
   Eval env (Var "miller_rabin_1")
     ((Eq NUM v4 --> Eq (NUM --> BOOL) v5 -->
       PAIR_TYPE BOOL (NUM --> BOOL)) miller_rabin_1)

Definition of side condition for miller_rabin_1:

|- miller_rabin_1_side v4 v5 ⇔
   v4 ≠ 2 ⇒
   v4 ≠ 1 ∧ ¬EVEN v4 ⇒
   prob_uniform_cut_side (2 * log2 (v4 − 1)) (v4 − 2) v5 ∧
   ∀v2 v1.
     (prob_uniform_cut (2 * log2 (v4 − 1)) (v4 − 2) v5 = (v2,v1)) ⇒
     witness_side v4 (v2 + 2)

Certificate theorem for miller_rabin:

|- DeclAssum example_primality_test_decls env ∧
   miller_rabin_side v1 v2 ⇒
   Eval env (Var "miller_rabin")
     ((Eq NUM v1 --> Eq NUM v2 --> (NUM --> BOOL) -->
       PAIR_TYPE BOOL (NUM --> BOOL)) miller_rabin)

Definition of side condition for miller_rabin:

|- miller_rabin_side v1 v2 ⇔ ∀v1'. miller_rabin_1_side v1 v1'

Definition of declaration list:

|- example_primality_test_decls =
   [Dlet (Pvar "EVEN")
      (Fun "v1"
         (App (Opb Leq)
            (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2))))
            (Val (Lit (IntLit 0)))));
    Dtype [(["a"; "b"],"prod",[("Pair",[Tvar "a"; Tvar "b"])])];
    Dlet (Pvar "UNIT")
      (Fun "v2" (Fun "v1" (Con "Pair" [Var "v2"; Var "v1"])));
    Dlet (Pvar "BIND")
      (Fun "v4"
         (Fun "v3"
            (Fun "v5"
               (Mat (App Opapp (Var "v4") (Var "v5"))
                  [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],
                    App Opapp (App Opapp (Var "v3") (Var "v2"))
                      (Var "v1"))]))));
    Dletrec
      [("prob_while_cut","v2",
        Fun "v3"
          (Fun "v4"
             (Fun "v5"
                (If (App (Opb Leq) (Var "v4") (Val (Lit (IntLit 0))))
                   (App Opapp (Var "UNIT") (Var "v5"))
                   (If (App Opapp (Var "v2") (Var "v5"))
                      (App Opapp
                         (App Opapp (Var "BIND")
                            (App Opapp (Var "v3") (Var "v5")))
                         (Fun "v1"
                            (App Opapp
                               (App Opapp
                                  (App Opapp
                                     (App Opapp (Var "prob_while_cut")
                                        (Var "v2")) (Var "v3"))
                                  (Let "k"
                                     (App (Opn Minus) (Var "v4")
                                        (Val (Lit (IntLit 1))))
                                     (If
                                        (App (Opb Lt) (Var "k")
                                           (Val (Lit (IntLit 0))))
                                        (Val (Lit (IntLit 0)))
                                        (Var "k")))) (Var "v1"))))
                      (App Opapp (Var "UNIT") (Var "v5")))))))];
    Dlet (Pvar "K") (Fun "v2" (Fun "v1" (Var "v2")));
    Dlet (Pvar "I") (Fun "v1" (Var "v1"));
    Dlet (Pvar "many")
      (Fun "v1"
         (Fun "v2"
            (App Opapp
               (App Opapp
                  (App Opapp
                     (App Opapp (Var "prob_while_cut") (Var "I"))
                     (App Opapp (Var "K") (Var "v1"))) (Var "v2"))
               (Val (Lit (Bool T))))));
    Dletrec
      [("log2","v1",
        If (App (Opb Leq) (Var "v1") (Val (Lit (IntLit 0))))
          (Val (Lit (IntLit 0)))
          (App (Opn Plus)
             (App Opapp (Var "log2")
                (App (Opn Divide) (Var "v1") (Val (Lit (IntLit 2)))))
             (Val (Lit (IntLit 1)))))];
    Dletrec
      [("factor_twos","v4",
        If
          (Log And (App (Opb Lt) (Val (Lit (IntLit 0))) (Var "v4"))
             (App Opapp (Var "EVEN") (Var "v4")))
          (Let "v3"
             (App Opapp (Var "factor_twos")
                (App (Opn Divide) (Var "v4") (Val (Lit (IntLit 2)))))
             (Mat (Var "v3")
                [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],
                  Con "Pair"
                    [App (Opn Plus) (Var "v2") (Val (Lit (IntLit 1)));
                     Var "v1"])]))
          (Con "Pair" [Val (Lit (IntLit 0)); Var "v4"]))];
    Dletrec
      [("modexp","v5",
        Fun "v3"
          (Fun "v4"
             (If (App (Opb Leq) (Var "v4") (Val (Lit (IntLit 0))))
                (Val (Lit (IntLit 1)))
                (Let "v2"
                   (App Opapp
                      (App Opapp (App Opapp (Var "modexp") (Var "v5"))
                         (Var "v3"))
                      (App (Opn Divide) (Var "v4")
                         (Val (Lit (IntLit 2)))))
                   (Let "v1"
                      (App (Opn Modulo)
                         (App (Opn Times) (Var "v2") (Var "v2"))
                         (Var "v5"))
                      (If (App Opapp (Var "EVEN") (Var "v4")) (Var "v1")
                         (App (Opn Modulo)
                            (App (Opn Times) (Var "v1") (Var "v3"))
                            (Var "v5"))))))))];
    Dletrec
      [("witness_tail","v2",
        Fun "v3"
          (Fun "v4"
             (If (App (Opb Leq) (Var "v4") (Val (Lit (IntLit 0))))
                (App Equality
                   (App Equality (Var "v3") (Val (Lit (IntLit 1))))
                   (Val (Lit (Bool F))))
                (Let "v1"
                   (App (Opn Modulo)
                      (App (Opn Times) (Var "v3") (Var "v3"))
                      (Var "v2"))
                   (If (App Equality (Var "v1") (Val (Lit (IntLit 1))))
                      (Log And
                         (App Equality
                            (App Equality (Var "v3")
                               (Val (Lit (IntLit 1))))
                            (Val (Lit (Bool F))))
                         (App Equality
                            (App Equality (Var "v3")
                               (Let "k"
                                  (App (Opn Minus) (Var "v2")
                                     (Val (Lit (IntLit 1))))
                                  (If
                                     (App (Opb Lt) (Var "k")
                                        (Val (Lit (IntLit 0))))
                                     (Val (Lit (IntLit 0))) (Var "k"))))
                            (Val (Lit (Bool F)))))
                      (App Opapp
                         (App Opapp
                            (App Opapp (Var "witness_tail") (Var "v2"))
                            (Var "v1"))
                         (App (Opn Minus) (Var "v4")
                            (Val (Lit (IntLit 1))))))))))];
    Dlet (Pvar "witness")
      (Fun "v5"
         (Fun "v4"
            (Let "v3"
               (App Opapp (Var "factor_twos")
                  (Let "k"
                     (App (Opn Minus) (Var "v5") (Val (Lit (IntLit 1))))
                     (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
                        (Val (Lit (IntLit 0))) (Var "k"))))
               (Mat (Var "v3")
                  [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],
                    App Opapp
                      (App Opapp
                         (App Opapp (Var "witness_tail") (Var "v5"))
                         (App Opapp
                            (App Opapp
                               (App Opapp (Var "modexp") (Var "v5"))
                               (Var "v4")) (Var "v1")))
                      (Var "v2"))]))));
    Dlet (Pvar "shd")
      (Fun "v1" (App Opapp (Var "v1") (Val (Lit (IntLit 0)))));
    Dlet (Pvar "stl")
      (Fun "v1"
         (Fun "v2"
            (App Opapp (Var "v1")
               (App (Opn Plus) (Var "v2") (Val (Lit (IntLit 1)))))));
    Dletrec
      [("prob_unif","v4",
        Fun "v5"
          (If (App (Opb Leq) (Var "v4") (Val (Lit (IntLit 0))))
             (Con "Pair" [Val (Lit (IntLit 0)); Var "v5"])
             (Let "v3"
                (App Opapp
                   (App Opapp (Var "prob_unif")
                      (App (Opn Divide) (Var "v4")
                         (Val (Lit (IntLit 2))))) (Var "v5"))
                (Mat (Var "v3")
                   [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],
                     Con "Pair"
                       [If (App Opapp (Var "shd") (Var "v1"))
                          (App (Opn Plus)
                             (App (Opn Times) (Val (Lit (IntLit 2)))
                                (Var "v2")) (Val (Lit (IntLit 1))))
                          (App (Opn Times) (Val (Lit (IntLit 2)))
                             (Var "v2"));
                        App Opapp (Var "stl") (Var "v1")])]))))];
    Dletrec
      [("prob_uniform_cut","x",
        Fun "x1"
          (Fun "x2"
             (If (App (Opb Leq) (Var "x") (Val (Lit (IntLit 0))))
                (If (App (Opb Leq) (Var "x1") (Val (Lit (IntLit 0))))
                   (Raise Bind_error)
                   (Con "Pair" [Val (Lit (IntLit 0)); Var "x2"]))
                (If (App (Opb Leq) (Var "x1") (Val (Lit (IntLit 0))))
                   (Raise Bind_error)
                   (Let "v3"
                      (App Opapp
                         (App Opapp (Var "prob_unif")
                            (App (Opn Minus) (Var "x1")
                               (Val (Lit (IntLit 1))))) (Var "x2"))
                      (Mat (Var "v3")
                         [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],
                           If (App (Opb Lt) (Var "v2") (Var "x1"))
                             (Con "Pair" [Var "v2"; Var "v1"])
                             (App Opapp
                                (App Opapp
                                   (App Opapp (Var "prob_uniform_cut")
                                      (App (Opn Minus) (Var "x")
                                         (Val (Lit (IntLit 1)))))
                                   (Var "x1")) (Var "v1")))]))))))];
    Dlet (Pvar "miller_rabin_1")
      (Fun "v4"
         (Fun "v5"
            (If (App Equality (Var "v4") (Val (Lit (IntLit 2))))
               (Con "Pair" [Val (Lit (Bool T)); Var "v5"])
               (If
                  (Log Or
                     (App Equality (Var "v4") (Val (Lit (IntLit 1))))
                     (App Opapp (Var "EVEN") (Var "v4")))
                  (Con "Pair" [Val (Lit (Bool F)); Var "v5"])
                  (Let "v3"
                     (App Opapp
                        (App Opapp
                           (App Opapp (Var "prob_uniform_cut")
                              (App (Opn Times) (Val (Lit (IntLit 2)))
                                 (App Opapp (Var "log2")
                                    (Let "k"
                                       (App (Opn Minus) (Var "v4")
                                          (Val (Lit (IntLit 1))))
                                       (If
                                          (App (Opb Lt) (Var "k")
                                             (Val (Lit (IntLit 0))))
                                          (Val (Lit (IntLit 0)))
                                          (Var "k"))))))
                           (Let "k"
                              (App (Opn Minus) (Var "v4")
                                 (Val (Lit (IntLit 2))))
                              (If
                                 (App (Opb Lt) (Var "k")
                                    (Val (Lit (IntLit 0))))
                                 (Val (Lit (IntLit 0))) (Var "k"))))
                        (Var "v5"))
                     (Mat (Var "v3")
                        [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],
                          Con "Pair"
                            [App Equality
                               (App Opapp
                                  (App Opapp (Var "witness") (Var "v4"))
                                  (App (Opn Plus) (Var "v2")
                                     (Val (Lit (IntLit 2)))))
                               (Val (Lit (Bool F))); Var "v1"])]))))));
    Dlet (Pvar "miller_rabin")
      (Fun "v1"
         (Fun "v2"
            (App Opapp
               (App Opapp (Var "many")
                  (App Opapp (Var "miller_rabin_1") (Var "v1")))
               (Var "v2"))))]