lean-surfaces/Examples/python/builtin_raise_lab/spec.lean at master · thomasnormal/lean-surfaces · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
import LeanModels.Python.Script

import Examples.python.builtin_raise_lab.proof

open LeanModels LeanModels.Python

load_program builtin_raise_lab from "Examples/python/builtin_raise_lab/builtin_raise_lab.json"
load_program builtin_raise_namedtuple from "Examples/python/builtin_raise_lab/builtin_raise_namedtuple.json"

#py_check builtin_raise_lab.raise_BaseException() raises (.builtinException "BaseException")

#py_check builtin_raise_lab.catch_BaseException(23) = 23

#py_check builtin_raise_lab.raise_Exception() raises (.builtinException "Exception")

#py_check builtin_raise_lab.catch_Exception(23) = 23

#py_check builtin_raise_lab.raise_ArithmeticError() raises (.builtinException "ArithmeticError")

#py_check builtin_raise_lab.catch_ArithmeticError(23) = 23

#py_check builtin_raise_lab.raise_LookupError() raises (.builtinException "LookupError")

#py_check builtin_raise_lab.catch_LookupError(23) = 23

#py_check builtin_raise_lab.raise_TypeError() raises (.builtinException "TypeError")

#py_check builtin_raise_lab.catch_TypeError(23) = 23

#py_check builtin_raise_lab.raise_NameError() raises (.builtinException "NameError")

#py_check builtin_raise_lab.catch_NameError(23) = 23

#py_check builtin_raise_lab.raise_ZeroDivisionError() raises (.builtinException "ZeroDivisionError")

#py_check builtin_raise_lab.catch_ZeroDivisionError(23) = 23

#py_check builtin_raise_lab.raise_OverflowError() raises (.builtinException "OverflowError")

#py_check builtin_raise_lab.catch_OverflowError(23) = 23

#py_check builtin_raise_lab.raise_IndexError() raises (.builtinException "IndexError")

#py_check builtin_raise_lab.catch_IndexError(23) = 23

#py_check builtin_raise_lab.raise_ValueError() raises (.builtinException "ValueError")

#py_check builtin_raise_lab.catch_ValueError(23) = 23

#py_check builtin_raise_lab.raise_KeyError() raises (.builtinException "KeyError")

#py_check builtin_raise_lab.catch_KeyError(23) = 23

#py_check builtin_raise_lab.raise_RuntimeError() raises (.builtinException "RuntimeError")

#py_check builtin_raise_lab.catch_RuntimeError(23) = 23

#py_check builtin_raise_lab.raise_RecursionError() raises (.builtinException "RecursionError")

#py_check builtin_raise_lab.catch_RecursionError(23) = 23

#py_check builtin_raise_lab.raise_AttributeError() raises (.builtinException "AttributeError")

#py_check builtin_raise_lab.catch_AttributeError(23) = 23

#py_check builtin_raise_lab.raise_AssertionError() raises (.builtinException "AssertionError")

#py_check builtin_raise_lab.catch_AssertionError(23) = 23

#py_check builtin_raise_lab.raise_StopIteration() raises (.builtinException "StopIteration")

#py_check builtin_raise_lab.catch_StopIteration(23) = 23

#py_check builtin_raise_lab.base_not_exception() = 2

#py_check builtin_raise_lab.wrong_sibling() = 2

#py_check builtin_raise_lab.retained_state() = (Val.list #[.int 0, .int 1, .int 2])

#py_check builtin_raise_lab.through_call() = 9

#py_check builtin_raise_lab.generator_closed() = 17

#py_check builtin_raise_lab.generator_escape() raises (.runtimeError "generator raised StopIteration")

#py_check builtin_raise_lab.exhaustion_escape() raises (.runtimeError "generator raised StopIteration")

#py_check builtin_raise_lab.caught_inside_generator() = 5

#py_check builtin_raise_namedtuple.raise_value_error() raises
  (.typeError "exceptions must derive from BaseException")

#py_check builtin_raise_namedtuple.raise_stop_iteration() raises
  (.typeError "exceptions must derive from BaseException")

#py_check builtin_raise_namedtuple.raise_record() raises
  (.typeError "exceptions must derive from BaseException")

#py_check builtin_raise_namedtuple.catch_shadow(23) = 23

#py_check builtin_raise_namedtuple.generator_closed() = 17

#py_check builtin_raise_namedtuple.generator_escape() raises
  (.typeError "exceptions must derive from BaseException")

#py_check builtin_raise_namedtuple.invalid_handler() raises
  (.typeError "catching classes that do not inherit from BaseException is not allowed")

#py_check builtin_raise_namedtuple.handler_success(23) = 23

#py_check builtin_raise_namedtuple.handler_retained_state() =
  (Val.list #[.int 0, .int 1, .int 3])

#guard callFunction builtin_raise_lab "late_shadow" #[] 4096 matches
  .exn (.unboundLocalError "ValueError")

#py_check builtin_raise_lab.raised_instance() raises (.builtinException "ValueError")

#py_check builtin_raise_lab.chained() raises (.builtinException "ValueError")

#py_check builtin_raise_lab.unsupported_class() raises (.builtinException "OSError")

#py_check builtin_raise_lab.parameter_shadow(1) raises
  (.typeError "exceptions must derive from BaseException")

theorem catch_value_error_total (value : PyInt) :
    builtin_raise_lab.catch_ValueError(value) ==> value := by proofs

#print axioms catch_value_error_total