-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathMidenLean.lean
More file actions
108 lines (108 loc) · 3.65 KB
/
MidenLean.lean
File metadata and controls
108 lines (108 loc) · 3.65 KB
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
import MidenLean.Felt
import MidenLean.State
import MidenLean.Instruction
import MidenLean.Op
import MidenLean.Semantics
import MidenLean.Generated.Word
import MidenLean.Generated.U64
import MidenLean.Generated.U128
import MidenLean.Proofs.SimpAttrs
import MidenLean.Proofs.Helpers
import MidenLean.Proofs.StepLemmas
import MidenLean.Proofs.Tactics
import MidenLean.Proofs.U32.Common
import MidenLean.Proofs.U64.Common
import MidenLean.Proofs.U64.Eq
import MidenLean.Proofs.U64.WrappingSub
import MidenLean.Proofs.U64.OverflowingSub
import MidenLean.Proofs.U64.Lt
import MidenLean.Proofs.U64.Gt
import MidenLean.Proofs.U64.Lte
import MidenLean.Proofs.U64.Gte
import MidenLean.Proofs.U64.And
import MidenLean.Proofs.U64.Or
import MidenLean.Proofs.U64.Xor
import MidenLean.Proofs.U64.Neq
import MidenLean.Proofs.U64.Clz
import MidenLean.Proofs.U64.Ctz
import MidenLean.Proofs.U64.Clo
import MidenLean.Proofs.U64.Cto
import MidenLean.Proofs.U64.WideningAdd
import MidenLean.Proofs.U64.U32Assert4
import MidenLean.Proofs.U64.WrappingMul
import MidenLean.Proofs.U64.Div
import MidenLean.Proofs.U64.Divmod
import MidenLean.Proofs.U64.Max
import MidenLean.Proofs.U64.Min
import MidenLean.Proofs.U64.Mod
import MidenLean.Proofs.U64.Rotl
import MidenLean.Proofs.U64.Rotr
import MidenLean.Proofs.U64.Shl
import MidenLean.Proofs.U64.Shr
import MidenLean.Proofs.U64.WideningMul
import MidenLean.Proofs.U128.Common
import MidenLean.Proofs.U128.And
import MidenLean.Proofs.U128.Clo
import MidenLean.Proofs.U128.Clz
import MidenLean.Proofs.U128.Cto
import MidenLean.Proofs.U128.Ctz
import MidenLean.Proofs.U128.Div
import MidenLean.Proofs.U128.Divmod
import MidenLean.Proofs.U128.Eq
import MidenLean.Proofs.U128.Eqz
import MidenLean.Proofs.U128.Gt
import MidenLean.Proofs.U128.Gte
import MidenLean.Proofs.U128.Lt
import MidenLean.Proofs.U128.Lte
import MidenLean.Proofs.U128.Max
import MidenLean.Proofs.U128.Min
import MidenLean.Proofs.U128.Mod
import MidenLean.Proofs.U128.Not
import MidenLean.Proofs.U128.Neq
import MidenLean.Proofs.U128.Or
import MidenLean.Proofs.U128.OverflowingAdd
import MidenLean.Proofs.U128.OverflowingMul
import MidenLean.Proofs.U128.OverflowingSub
import MidenLean.Proofs.U128.Rotl
import MidenLean.Proofs.U128.Rotr
import MidenLean.Proofs.U128.Shl
import MidenLean.Proofs.U128.Shr
import MidenLean.Proofs.U128.ShrK0
import MidenLean.Proofs.U128.ShrK1
import MidenLean.Proofs.U128.ShrK2
import MidenLean.Proofs.U128.ShrK3
import MidenLean.Proofs.U128.WideningAdd
import MidenLean.Proofs.U128.WideningMul
import MidenLean.Proofs.U128.WrappingAdd
import MidenLean.Proofs.U128.WrappingMul
import MidenLean.Proofs.U128.WrappingSub
import MidenLean.Proofs.U128.Xor
import MidenLean.Proofs.U256.Common
import MidenLean.Proofs.U256.AddWithCarryBe
import MidenLean.Proofs.U256.And
import MidenLean.Proofs.U256.Eq
import MidenLean.Proofs.U256.Eqz
import MidenLean.Proofs.U256.Mulstep
import MidenLean.Proofs.U256.Mulstep4
import MidenLean.Proofs.U256.Or
import MidenLean.Proofs.U256.OverflowingAdd
import MidenLean.Proofs.U256.U256LeToBe
import MidenLean.Proofs.U256.U256LeToBePair
import MidenLean.Proofs.U256.WideningAdd
import MidenLean.Proofs.U256.WrappingAdd
import MidenLean.Proofs.U256.WrappingMul
import MidenLean.Proofs.U256.WrappingMulBridge
import MidenLean.Proofs.U256.Xor
import MidenLean.Proofs.Word.Testz
import MidenLean.Proofs.Word.Eqz
import MidenLean.Proofs.Word.Reverse
import MidenLean.Proofs.Word.StoreWordU32sLe
import MidenLean.Proofs.Word.Arrange
import MidenLean.Proofs.Word.Eq
import MidenLean.Proofs.Word.TestEq
import MidenLean.Proofs.Word.Gt
import MidenLean.Proofs.Word.Lt
import MidenLean.Proofs.Word.Lte
import MidenLean.Proofs.Word.Gte
import MidenLean.Tests.Semantics
import MidenLean.Tests.Procedures