LAWS_order.bend

bend-osdev-u32@0.1.0.0 · 165 lines · 23 definitions

1# The order of Nat and of Base's words: transitivity, reflexivity and
2# antisymmetry, for Nat.is_lt and Nat.is_le (and x <= x + w), Word.cmp of
3# every width n, and U32.cmp, U32.is_lt and U32.is_le. Other bend-osdev packages' proofs use
4# these laws instead of each proving them again.
5import Base
6
7# Nat
8
9law nat_le_trans:
10  for +x: Nat
11  for +y: Nat
12  for +z: Nat
13  for h1: {Nat.is_le(x, y) == True{} : Bool}
14  for h2: {Nat.is_le(y, z) == True{} : Bool}
15  {Nat.is_le(x, z) == True{} : Bool}
16
17law nat_lt_trans:
18  for +x: Nat
19  for +y: Nat
20  for +z: Nat
21  for h1: {Nat.is_lt(x, y) == True{} : Bool}
22  for h2: {Nat.is_lt(y, z) == True{} : Bool}
23  {Nat.is_lt(x, z) == True{} : Bool}
24
25law nat_lt_le_trans:
26  for +x: Nat
27  for +y: Nat
28  for +z: Nat
29  for h1: {Nat.is_lt(x, y) == True{} : Bool}
30  for h2: {Nat.is_le(y, z) == True{} : Bool}
31  {Nat.is_lt(x, z) == True{} : Bool}
32
33law nat_le_lt_trans:
34  for +x: Nat
35  for +y: Nat
36  for +z: Nat
37  for h1: {Nat.is_le(x, y) == True{} : Bool}
38  for h2: {Nat.is_lt(y, z) == True{} : Bool}
39  {Nat.is_lt(x, z) == True{} : Bool}
40
41law nat_le_add_r:
42  for +x: Nat
43  for +w: Nat
44  {Nat.is_le(x, Nat.add(x, w)) == True{} : Bool}
45
46# Words of any width n
47
48law word_cmp_refl:
49  for +n: Nat
50  for +a: Word(n)
51  {Word.cmp(n, a, a) == EQ{} : Cmp}
52
53law word_cmp_eq:
54  for +n: Nat
55  for +a: Word(n)
56  for +b: Word(n)
57  for e: {Word.cmp(n, a, b) == EQ{} : Cmp}
58  {a == b : Word(n)}
59
60law word_cmp_lt_trans:
61  for +n: Nat
62  for +a: Word(n)
63  for +b: Word(n)
64  for +c: Word(n)
65  for h1: {Word.cmp(n, a, b) == LT{} : Cmp}
66  for h2: {Word.cmp(n, b, c) == LT{} : Cmp}
67  {Word.cmp(n, a, c) == LT{} : Cmp}
68
69# U32
70
71law u32_cmp_refl:
72  for +a: U32
73  {U32.cmp(a, a) == EQ{} : Cmp}
74
75law u32_cmp_eq:
76  for +a: U32
77  for +b: U32
78  for e: {U32.cmp(a, b) == EQ{} : Cmp}
79  {a == b : U32}
80
81law u32_cmp_lt_trans:
82  for +a: U32
83  for +b: U32
84  for +c: U32
85  for h1: {U32.cmp(a, b) == LT{} : Cmp}
86  for h2: {U32.cmp(b, c) == LT{} : Cmp}
87  {U32.cmp(a, c) == LT{} : Cmp}
88
89law u32_le_refl:
90  for +a: U32
91  {U32.is_le(a, a) == True{} : Bool}
92
93law u32_lt_irrefl:
94  for +a: U32
95  for e: {U32.is_lt(a, a) == True{} : Bool}
96  Empty
97
98law u32_lt_le:
99  for +a: U32
100  for +b: U32
101  for e: {U32.is_lt(a, b) == True{} : Bool}
102  {U32.is_le(a, b) == True{} : Bool}
103
104law u32_lt_trans:
105  for +a: U32
106  for +b: U32
107  for +c: U32
108  for h1: {U32.is_lt(a, b) == True{} : Bool}
109  for h2: {U32.is_lt(b, c) == True{} : Bool}
110  {U32.is_lt(a, c) == True{} : Bool}
111
112law u32_le_trans:
113  for +a: U32
114  for +b: U32
115  for +c: U32
116  for h1: {U32.is_le(a, b) == True{} : Bool}
117  for h2: {U32.is_le(b, c) == True{} : Bool}
118  {U32.is_le(a, c) == True{} : Bool}
119
120law u32_lt_le_trans:
121  for +a: U32
122  for +b: U32
123  for +c: U32
124  for h1: {U32.is_lt(a, b) == True{} : Bool}
125  for h2: {U32.is_le(b, c) == True{} : Bool}
126  {U32.is_lt(a, c) == True{} : Bool}
127
128law u32_le_lt_trans:
129  for +a: U32
130  for +b: U32
131  for +c: U32
132  for h1: {U32.is_le(a, b) == True{} : Bool}
133  for h2: {U32.is_lt(b, c) == True{} : Bool}
134  {U32.is_lt(a, c) == True{} : Bool}
135
136law u32_le_antisym:
137  for +a: U32
138  for +b: U32
139  for h1: {U32.is_le(a, b) == True{} : Bool}
140  for h2: {U32.is_le(b, a) == True{} : Bool}
141  {a == b : U32}
142
143law u32_not_lt:
144  for +a: U32
145  for +b: U32
146  for e: {U32.is_lt(a, b) == False{} : Bool}
147  {U32.is_le(b, a) == True{} : Bool}
148
149law u32_not_le:
150  for +a: U32
151  for +b: U32
152  for e: {U32.is_le(a, b) == False{} : Bool}
153  {U32.is_lt(b, a) == True{} : Bool}
154
155law u32_lt_not_le:
156  for +a: U32
157  for +b: U32
158  for e: {U32.is_lt(a, b) == True{} : Bool}
159  {U32.is_le(b, a) == False{} : Bool}
160
161law u32_le_not_lt:
162  for +a: U32
163  for +b: U32
164  for e: {U32.is_le(a, b) == True{} : Bool}
165  {U32.is_lt(b, a) == False{} : Bool}