Theory Exception_Rewriting

(*
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory Exception_Rewriting
imports
  "AutoCorres2_Main.AutoCorres_Main"
begin



install_C_file "Exception_Rewriting.c"

autocorres "Exception_Rewriting.c"


context ts_definition_goo
begin
thm ts_def [no_vars]
end

ML ‹
val stats = Fun_Cache.cache_statistics ()
›


context Exception_Rewriting_all_impl
begin
term "foo':: int ⇒ int ⇒ lifted_globals ⇒ int option"
thm foo'_def [no_vars]

lemma "foo' i j ≡ ofail"
  by (simp add: foo'_def)

term "cond_return'::int ⇒ (int, lifted_globals) res_monad"

thm cond_return'_def[no_vars]
lemma "cond_return' p ≡ finally (do {
                             _ ← when (p = 32 ∨ 2 < p) (when (p ≠ 30 ∧ p ≠ 2) (throw p));
                             v ← gets_the (foo' p p);
                             throw p
                           })"
  by (simp add: cond_return'_def)

term "nested_while':: int ⇒ (int, lifted_globals) res_monad"
thm nested_while'_def[no_vars]
lemma "nested_while' a ≡ finally
 (do {
    y ← try (do {
                (a, y) ←
                  whileLoop (λ(a, y) s. True)
                    (λ(a, y). do {
                          a ← condition (λs. 3 < a)
                                 (throw (Inl 1))
                                 (condition (λs. 1 < a)
                                    (return (a + 1))
                                    (do {
                                       _ ← liftE (finally (whileLoop (λ_ s. True)
                (λ_. throw ())
               ()));
                                       throw (Inr 4)
                                     }));
                          return (a, 4)
                        })
                   (a, 3);
                return y
              });
    _ ← liftE (do {
                  _ ← guard (λ_. 0 ≤ 2147483650 + y);
                  guard (λ_. y ≤ 2147483645)
                });
    throw (2 + y)
  })"
  by (simp add: nested_while'_def)


term "just_exit'::(32 signed word, unit, lifted_globals) exn_monad"
thm just_exit'_def[no_vars]
lemma "just_exit' ≡ throw 1"
  by (simp add: just_exit'_def)

term "call_exit':: (32 signed word, unit, lifted_globals) exn_monad"
thm call_exit'_def[no_vars]
lemma "call_exit' ≡ just_exit'"
  by (simp add: call_exit'_def)

term "ret_or_throw'::int ⇒ (32 signed word, int, lifted_globals) exn_monad"
thm ret_or_throw'_def[no_vars]
lemma "ret_or_throw' a ≡ condition (λs. 2 < a)
                     (return 3)
                     (throw 1)"
  by (simp add: ret_or_throw'_def)

term "while_ret_or_break_or_continue':: int ⇒ (int, lifted_globals) res_monad"
thm while_ret_or_break_or_continue'_def[no_vars]
lemma "while_ret_or_break_or_continue' a ≡
finally
 (try (whileLoop (λa s. True)
         (λa. condition (λs. 3 < a)
                 (throw (Inl 1))
                 (condition (λs. 1 < a)
                    (return (a + 1))
                    (throw (Inr a))))
        a))"
  by (simp add: while_ret_or_break_or_continue'_def)

term "fac_exit':: int ⇒ (32 signed word, int, lifted_globals) exn_monad"
thm fac_exit'.simps[no_vars]
lemma "fac_exit' n = condition (λs. n < 0)
                (throw 1)
                (condition (λs. n = 0)
                   (return 0)
                   (do { guard (λs. n ≤ INT_MAX + 1);
                        fac_exit' (n - 1)
                    }))"
  apply(subst  fac_exit'.simps)
  apply simp
  done


term "while_comb'::int ⇒ (int, lifted_globals) res_monad"
thm while_comb'_def[no_vars]
lemma "while_comb' a ≡ do {
  x ← guard (λs. - 1073741824 ≤ a);
  _ ← guard (λs. 2 * a ≤ INT_MAX);
  x ← condition (λs. 2 * a < 30) (do {
                                     _ ← guard (λs. - (INT_MAX + 1) < 2 * a);
                                     return (2 * a - 1)
                                   })
        (do {
           _ ← guard (λs. 2 * a ≤ INT_MAX - 1);
           return (2 * a + 1)
         });
  finally (do {
             _ ← try (do {
                         a ← whileLoop (λa s. True) (λa. condition (λs. 3 < a) (throw (Inl 1)) (condition (λs. 1 < a) (return (a + 1)) (throw (Inr ())))) a;
                         skip
                       });
             throw x
           })
}"
  by (simp add: while_comb'_def)

term "while_comb_exit':: int ⇒ (32 signed word, int, lifted_globals) exn_monad"
thm while_comb_exit'_def[no_vars]
lemma "while_comb_exit' a ≡ do {
  _ ← liftE (do {
                _ ← guard (λs. - 1073741824 ≤ a);
                guard (λs. 2 * a ≤ INT_MAX)
              });
  x ← liftE (condition (λs. 2 * a < 30) (do {
                                            _ ← guard (λs. - (INT_MAX + 1) < 2 * a);
                                            return (2 * a - 1)
                                          })
               (do {
                  _ ← guard (λs. 2 * a ≤ INT_MAX - 1);
                  return (2 * a + 1)
                }));
  try (do {
         a ← whileLoop (λa s. True) (λa. condition (λs. 3 < a) (throw (Inr 1)) (condition (λs. 1 < a) (return (a + 1)) (throw (Inl 1)))) a;
         throw (Inr x)
       })
}"
  by (simp add: while_comb_exit'_def)

term "while_ret_or_throw'::int ⇒ (32 signed word, int, lifted_globals) exn_monad"
thm "while_ret_or_throw'_def"[no_vars]
lemma "while_ret_or_throw' a ≡
try (do {
       ret ←
         try (whileLoop (λret s. True)
               (λret. condition (λs. 3 < a) (throw (Inl (Inr 1)))
                        (condition (λs. 1 < a) (throw (Inl (Inl 1))) (throw (Inr ()))))
               ());
       throw (Inr 2)
     })"
  by (simp add: while_ret_or_throw'_def)

term "control_flow'::int ⇒ (int, lifted_globals) res_monad"
term whileLoop


thm "control_flow'_def"[no_vars]
term bind

lemma "control_flow' n ≡ do {
  (b::int) ← unknown;
  finally (do {
             j ← whileLoop (λj s. j < n)
                    (λj. do {
                          (i, j) ← whileLoop (λ(i, j) s. i < n)
                                      (λ(i, j). do {
                                            j ← condition (λs. b ≠ 0)
                                                   (throw 0)
                                                   (return j);
                                            liftE (do {
                                                     x ← guard (λs. 0 ≤ 2147483649 + i);
                                                     _ ← guard (λs. i < INT_MAX);
                                                     return (i + 1, j)
                                                   })
                                          })
                                     (j, j);
                          liftE (do {
                                   x ← guard (λs. 0 ≤ 2147483649 + j);
                                   _ ← guard (λs. j < INT_MAX);
                                   return (j + 1)
                                 })
                        })
                   0;
             throw 0
           })
}"
  unfolding control_flow'_def .


term "control_flow_exit'::int ⇒ (int, lifted_globals) res_monad"
thm "control_flow_exit'_def"[no_vars]
lemma "control_flow_exit' n ≡ do {
  b ← unknown::(int, lifted_globals) res_monad;
  i ← unknown;
  finally (do {
             (i, j) ← whileLoop (λ(i, j) s. j < n)
                         (λ(i, j). do {
                               (i, j) ← whileLoop (λ(i, j) s. i < n)
                                           (λ(i, j). do {
                                                 j ← condition (λs. b ≠ 0)
                                                        (throw 0)
                                                        (return j);
                                                 liftE (do {
                                                          x ← guard (λs. 0 ≤ 2147483649 + i);
                                                          _ ← guard (λs. i ≤ INT_MAX - 1);
                                                          return (i + 1, j)
                                                        })
                                               })
                                          (j, j);
                               liftE (do {
                                        x ← guard (λs. 0 ≤ 2147483649 + j);
                                        _ ← guard (λs. j ≤ INT_MAX - 1);
                                        return (i, j + 1)
                                      })
                             })
                        (i, 0);
             liftE (do {
                      x ← guard (λs. - (INT_MAX + 1) ≤ j + i);
                      _ ← guard (λs. j + i ≤ INT_MAX);
                      return (j + i)
                    })
           })
}"
  by (simp add: control_flow_exit'_def)


term "control_flow_exit1'::int ⇒ (8 word, lifted_globals) res_monad"
thm "control_flow_exit1'_def"[no_vars]
lemma "control_flow_exit1' n ≡ finally (do {
                                    result ← whileLoop (λresult s. True)
                                                (λresult. do {
                                                      result ← condition (λs. n ≠ 0)
                                                                  (throw 1)
                                                                  (return result);
                                                      _ ← unless (n = 0) (throw result);
                                                      return result
                                                    })
                                               0;
                                    return 1
                                  })"
  by (simp add: control_flow_exit1'_def)

term "plus'::32 word ⇒ 32 word ⇒ 32 word"
thm plus'_def[no_vars]
lemma "plus' a b ≡ a + b"
  by (simp add: plus'_def)

term "plus2':: 32 word ⇒ 32 word ⇒ lifted_globals ⇒ 32 word option"
thm "plus2'_def"[no_vars]
lemma "plus2' a b ≡ do {
  (a, b) ←
    owhile (λ(a, b) a. 0 < b) (λ(a, b). oreturn (a + 1, b - 1)) (a, b);
  oreturn a
}"
  by (simp add: plus2'_def)

term "call_plus':: 32 word"
thm "call_plus'_def"[no_vars]
lemma "call_plus' ≡ plus' 2 3"
  by (simp add: call_plus'_def)

term "fac'::32 word ⇒ lifted_globals ⇒ 32 word option"
thm "fac'.simps"[no_vars]
lemma "fac' n = ocondition (λs. n = 0) (oreturn 0) (fac' (n - 1))"
  by (subst fac'.simps) simp


term "call_fac_exit':: int ⇒ (32 signed word, int, lifted_globals) exn_monad"
thm "call_fac_exit'_def"[no_vars]
lemma "call_fac_exit' n ≡ do {
  _ ← liftE (do {
                _ ← guard (λs. 0 ≤ 2147483649 + n);
                guard (λs. n ≤ INT_MAX - 1)
              });
  ret'int'1 ← fac_exit' (n + 1);
  _ ← guard (λs. n ≤ 2147483645);
  ret'int'2 ← fac_exit' (n + 2);
  liftE (do {
           x ← guard (λs. - (INT_MAX + 1) ≤ ret'int'1 + ret'int'2);
           _ ← guard (λs. ret'int'1 + ret'int'2 ≤ INT_MAX);
           return (ret'int'1 + ret'int'2)
         })
}"
  by (simp add: call_fac_exit'_def)

term "even'::32 word ⇒ lifted_globals ⇒ 32 word option"
thm "even'.simps"[no_vars]
lemma "even' n =
ocondition (λs. n = 0) (oreturn 1)
 (do {
    ret ← odd' (n - 1);
    oreturn (if ret = 0 then 1 else 0)
  })"
  by (subst even'.simps) simp

term "odd'::32 word ⇒ lifted_globals ⇒ 32 word option"
thm "odd'.simps"[no_vars]
lemma "odd' n =
ocondition (λs. n = 0) (oreturn 0)
 (do {
    ret ← even' (n - 1);
    oreturn (if ret = 0 then 1 else 0)
  })"
  by (subst odd'.simps) simp

term "main'::32 word"
thm "main'_def"[no_vars]
thm plus'_def
lemma "main' ≡ if plus' 2 3 = 0 then 1 else 0"
  by (simp add: main'_def)

thm "goo'_def"[no_vars]
lemma "goo' a b c ≡ finally (do {
                         _ ← unless (a = 0) (unless (b = 0) (throw (- 1)));
                         ix ← whileLoop (λix s. ix = (0::32 word))
                                 (λix. do {
                                       ret'unsigned'1 ← return (id' c);
                                       _ ← unless (ret'unsigned'1 = 0) (throw (- 1));
                                       return 1
                                     })
                                0;
                         throw 0
                       })"
  by (simp add: goo'_def)
end

end