-
Notifications
You must be signed in to change notification settings - Fork 13
/
Verification.lean
118 lines (104 loc) · 5.83 KB
/
Verification.lean
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
/- Semantics -/
import Verification.Semantics.Assembly
import Verification.Semantics.Cpu
import Verification.Semantics.Instruction
import Verification.Semantics.SimpAttr
import Verification.Semantics.Util
import Verification.Semantics.Vm
-- Soundness
import Verification.Semantics.Soundness.AssemblyStep
import Verification.Semantics.Soundness.Hoare
import Verification.Semantics.Soundness.Prelude
-- Completeness
import Verification.Semantics.Completeness.VmAssembly
import Verification.Semantics.Completeness.VmAssemblyStep
import Verification.Semantics.Completeness.VmHoare
-- AIR encoding
import Verification.Semantics.AirEncoding.Constraints
import Verification.Semantics.AirEncoding.ConstraintsAutogen
import Verification.Semantics.AirEncoding.Correctness
import Verification.Semantics.AirEncoding.FinalCorrectness
import Verification.Semantics.AirEncoding.Glue
import Verification.Semantics.AirEncoding.Instruction
import Verification.Semantics.AirEncoding.Memory
import Verification.Semantics.AirEncoding.MemoryAux
import Verification.Semantics.AirEncoding.RangeCheck
import Verification.Semantics.AirEncoding.RangeCheckBuiltin
import Verification.Semantics.AirEncoding.Step
/- Libfuncs -/
import Verification.Libfuncs.Common
-- bounded_int
import Verification.Libfuncs.bounded_int.bounded_int_div_rem_known_small_lhs_code
import Verification.Libfuncs.bounded_int.bounded_int_div_rem_known_small_lhs_soundness_spec
import Verification.Libfuncs.bounded_int.bounded_int_div_rem_known_small_lhs_soundness
import Verification.Libfuncs.bounded_int.bounded_int_div_rem_known_small_lhs_completeness_spec
import Verification.Libfuncs.bounded_int.bounded_int_div_rem_known_small_lhs_completeness
import Verification.Libfuncs.bounded_int.bounded_int_div_rem_known_small_quotient_code
import Verification.Libfuncs.bounded_int.bounded_int_div_rem_known_small_quotient_soundness_spec
import Verification.Libfuncs.bounded_int.bounded_int_div_rem_known_small_quotient_soundness
import Verification.Libfuncs.bounded_int.bounded_int_div_rem_known_small_quotient_completeness_spec
import Verification.Libfuncs.bounded_int.bounded_int_div_rem_known_small_quotient_completeness
import Verification.Libfuncs.bounded_int.bounded_int_div_rem_known_small_rhs_code
import Verification.Libfuncs.bounded_int.bounded_int_div_rem_known_small_rhs_soundness_spec
import Verification.Libfuncs.bounded_int.bounded_int_div_rem_known_small_rhs_soundness
import Verification.Libfuncs.bounded_int.bounded_int_div_rem_known_small_rhs_completeness_spec
import Verification.Libfuncs.bounded_int.bounded_int_div_rem_known_small_rhs_completeness
-- u16
import Verification.Libfuncs.u16.u16_overflowing_add_code
import Verification.Libfuncs.u16.u16_overflowing_add_soundness_spec
import Verification.Libfuncs.u16.u16_overflowing_add_soundness
import Verification.Libfuncs.u16.u16_overflowing_sub_code
import Verification.Libfuncs.u16.u16_overflowing_sub_soundness_spec
import Verification.Libfuncs.u16.u16_overflowing_sub_soundness
import Verification.Libfuncs.u16.u16_sqrt_code
import Verification.Libfuncs.u16.u16_sqrt_soundness_spec
import Verification.Libfuncs.u16.u16_sqrt_soundness
-- u32
import Verification.Libfuncs.u32.u32_overflowing_add_code
import Verification.Libfuncs.u32.u32_overflowing_add_soundness_spec
import Verification.Libfuncs.u32.u32_overflowing_add_soundness
import Verification.Libfuncs.u32.u32_overflowing_sub_code
import Verification.Libfuncs.u32.u32_overflowing_sub_soundness_spec
import Verification.Libfuncs.u32.u32_overflowing_sub_soundness
import Verification.Libfuncs.u32.u32_sqrt_code
import Verification.Libfuncs.u32.u32_sqrt_soundness_spec
import Verification.Libfuncs.u32.u32_sqrt_soundness
-- u64
import Verification.Libfuncs.u64.u64_overflowing_add_code
import Verification.Libfuncs.u64.u64_overflowing_add_soundness_spec
import Verification.Libfuncs.u64.u64_overflowing_add_soundness
import Verification.Libfuncs.u64.u64_overflowing_sub_code
import Verification.Libfuncs.u64.u64_overflowing_sub_soundness_spec
import Verification.Libfuncs.u64.u64_overflowing_sub_soundness
import Verification.Libfuncs.u64.u64_sqrt_code
import Verification.Libfuncs.u64.u64_sqrt_soundness_spec
import Verification.Libfuncs.u64.u64_sqrt_soundness
-- u128
import Verification.Libfuncs.u128.u128_overflowing_add_code
import Verification.Libfuncs.u128.u128_overflowing_add_soundness_spec
import Verification.Libfuncs.u128.u128_overflowing_add_soundness
import Verification.Libfuncs.u128.u128_overflowing_add_completeness_spec
import Verification.Libfuncs.u128.u128_overflowing_add_completeness
import Verification.Libfuncs.u128.u128_overflowing_sub_code
import Verification.Libfuncs.u128.u128_overflowing_sub_completeness_spec
import Verification.Libfuncs.u128.u128_safe_divmod_code
import Verification.Libfuncs.u128.u128_safe_divmod_soundness_spec
import Verification.Libfuncs.u128.u128_safe_divmod_soundness
import Verification.Libfuncs.u128.u128_safe_divmod_completeness_spec
import Verification.Libfuncs.u128.u128_sqrt_completeness_spec
-- u256
import Verification.Libfuncs.u256.u256_guarantee_inv_mod_n_code
import Verification.Libfuncs.u256.u256_guarantee_inv_mod_n_soundness_spec
import Verification.Libfuncs.u256.u256_guarantee_inv_mod_n_soundness
import Verification.Libfuncs.u256.u256_guarantee_inv_mod_n_completeness_spec
-- import Verification.Libfuncs.u256.u256_guarantee_inv_mod_n_completeness
import Verification.Libfuncs.u256.u256_safe_divmod_code
import Verification.Libfuncs.u256.u256_safe_divmod_soundness_spec
import Verification.Libfuncs.u256.u256_safe_divmod_soundness
import Verification.Libfuncs.u256.u256_sqrt_code
import Verification.Libfuncs.u256.u256_sqrt_soundness_spec
import Verification.Libfuncs.u256.u256_sqrt_soundness
-- u512
import Verification.Libfuncs.u512.u512_safe_divmod_by_u256_code
import Verification.Libfuncs.u512.u512_safe_divmod_by_u256_soundness_spec
import Verification.Libfuncs.u512.u512_safe_divmod_by_u256_soundness