litex-lang 0.9.86-beta

A simple formal proof language and verifier, learnable in 2 hours
Documentation 
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

pub const BUILTIN_ENV_CODE_FOR_COMMON_FUNCTIONS: &str = r#"
# Existence of such function is valid by definition of comparison

let max_of_finite_set fn(s power_set(R): $is_finite_set(s)) R
let min_of_finite_set fn(s power_set(R): $is_finite_set(s)) R

know:
    forall s power_set(R), item s:
        $is_finite_set(s)
        =>:
            item <= max_of_finite_set(s)
            min_of_finite_set(s) <= item

    forall s power_set(R):
        $is_finite_set(s)
        =>:
            max_of_finite_set(s) $in s
            min_of_finite_set(s) $in s

let min_of_N_set fn(s power_set(N)) N

know:
    forall s power_set(N), item s:
        min_of_N_set(s) <= item

    forall s power_set(N):
        min_of_N_set(s) $in s
"#;