litex/builtin_code/
common_comparison_properties.rs

1// Common comparison properties: trichotomy and witnesses on R, zero-product, transitivity
2// (props + know), and difference characterization (`a - b` vs `0`).
3// Order closure under +, -, *, / on general inequalities is in `order_algebra_builtin.rs`.
4
5pub const KNOW_REAL_LINE_TRICHOTOMY: &str = r#"
6know:
7    forall a, b R:
8        a < b or a = b or a > b
9        a > b or a = b or a < b
10        a < b or a >= b
11        a > b or a <= b
12        a <= b or a > b
13        a >= b or a < b
14        a <= b or a >= b
15        a >= b or a <= b
16
17    forall a R:
18        exist b R st {a > b}
19        exist b R st {a < b}
20        exist b R st {a = b}
21        exist b R st {a != b}
22        exist b R st {a >= b}
23        exist b R st {a <= b}
24
25        exist b R st {b > a}
26        exist b R st {b < a}
27        exist b R st {b = a}
28        exist b R st {b != a}
29        exist b R st {b >= a}
30        exist b R st {b <= a}
31
32    exist a, b R st {a > b}
33    exist a, b R st {a < b}
34    exist a, b R st {a = b}
35    exist a, b R st {a != b}
36    exist a, b R st {a >= b}
37    exist a, b R st {a <= b}
38
39    exist a, b R st {b > a}
40    exist a, b R st {b < a}
41    exist a, b R st {b = a}
42    exist a, b R st {b != a}
43    exist a, b R st {b >= a}
44    exist a, b R st {b <= a}
45
46    forall a, b R:
47        a * b = 0
48        =>:
49            a = 0 or b = 0
50"#;
51
52pub const ORDER_TRANSITIVITY_PROP_DECLS: &str = r#"
53
54prop a_lt_c(a, b, c R):
55    a < c
56
57prop a_le_c(a, b, c R):
58    a <= c
59
60prop a_gt_c(a, b, c R):
61    a > c
62
63prop a_ge_c(a, b, c R):
64    a >= c
65"#;
66
67pub const KNOW_ORDER_TRANSITIVITY_CHAIN: &str = r#"
68know:
69    forall a, b, c R:
70        a < b
71        b < c
72        =>:
73            $a_lt_c(a, b, c)
74
75    forall a, b, c R:
76        a <= b
77        b <= c
78        =>:
79            $a_le_c(a, b, c)
80
81    forall a, b, c R:
82        a > b
83        b > c
84        =>:
85            $a_gt_c(a, b, c)
86
87    forall a, b, c R:
88        a >= b
89        b >= c
90        =>:
91            $a_ge_c(a, b, c)
92"#;
93
94pub const BUILTIN_ENV_CODE_FOR_COMMON_COMPARISON_PROPERTIES: &str = r#"
95know:
96    forall a, b R:
97        a <= b
98        =>:
99            a - b <= 0
100
101    forall a, b R:
102        a - b <= 0
103        =>:
104            a <= b
105
106    forall a, b R:
107        a < b
108        =>:
109            a - b < 0
110
111    forall a, b R:
112        a - b < 0
113        =>:
114            a < b
115
116    forall a, b, c R:
117        0 < c
118        c * a <= b or a * c <= b
119        =>:
120            a <= b / c
121
122    forall a, b, c R:
123        0 < c
124        a / c <= b
125        =>:
126            a <= b * c
127
128    forall a, b Z:
129        a <= b
130        =>:
131            count(closed_range(a, b)) = b - a + 1
132
133    forall a, b Z:
134        a < b
135        =>:
136            count(range(a, b)) = b - a   
137"#;
litex/builtin_code/common_comparison_properties.rs

litex/builtin_code/
common_comparison_properties.rs
