litex/builtin_code/
common_functions.rs

1pub const BUILTIN_ENV_CODE_FOR_COMMON_FUNCTIONS: &str = r#"
2# Existence of such function is valid by definition of comparison
3
4let max_of_finite_set fn(s power_set(R): $is_finite_set(s)) R
5let min_of_finite_set fn(s power_set(R): $is_finite_set(s)) R
6let floor fn(x R) Z
7let ceil fn(x R) Z
8
9know:
10    forall x R:
11        floor(x) <= x
12        x < floor(x) + 1
13        ceil(x) - 1 < x
14        x <= ceil(x)
15
16    forall x R, y Z:
17        0 <= x - y
18        x - y < 1
19        =>:
20            y = floor(x)
21
22    forall x R, y Z:
23        0 <= y - x
24        y - x < 1
25        =>:
26            y = ceil(x)
27
28    forall s power_set(R), item s:
29        $is_finite_set(s)
30        =>:
31            item <= max_of_finite_set(s)
32            min_of_finite_set(s) <= item
33
34    forall s power_set(R):
35        $is_finite_set(s)
36        =>:
37            max_of_finite_set(s) $in s
38            min_of_finite_set(s) $in s
39
40let min_of_N_set fn(s power_set(N)) N
41
42know:
43    forall s power_set(N), item s:
44        min_of_N_set(s) <= item
45
46    forall s power_set(N):
47        min_of_N_set(s) $in s
48"#;
litex/builtin_code/common_functions.rs

litex/builtin_code/
common_functions.rs
