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
// Fundamental order on R: difference characterization used by the verifier.
//
// Closure of the nonnegative / positive cone under +, *, /, and weak powers of nonnegative
// bases is implemented in Rust (`verify_order_atomic_fact_numeric_builtin_only` in
// `number_compare.rs`), not duplicated here.
pub const BUILTIN_ENV_CODE_FOR_FUNDAMENTAL_COMPARISON: &str = r#"
know:
forall a, b R:
a <= b
=>:
a = b or a < b
forall a, b R:
a >= b
=>:
a = b or a > b
forall a, b R:
=>:
a <= b
<=>:
0 <= b - a
forall a, b R:
=>:
a < b
<=>:
0 < b - a
forall a R:
a != 0
=>:
0 < a * a
0 < a^2
forall a, b R:
a * b = 0
=>:
a = 0 or b = 0
"#;