litex-lang 0.9.6-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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125

use crate::prelude::*;
use crate::rational_expression::mul_signed_decimal_str;

use super::number_compare::{compare_number_strings, NumberCompareResult};

fn decimal_str_sign_vs_zero(number_value: &str) -> NumberCompareResult {
    compare_number_strings(number_value.trim(), "0")
}

// None if denominator is zero; Some(false) positive; Some(true) negative (flip inequality).
fn nonzero_denominator_requires_flip(denominator_normalized: &str) -> Option<bool> {
    match decimal_str_sign_vs_zero(denominator_normalized) {
        NumberCompareResult::Equal => None,
        NumberCompareResult::Greater => Some(false),
        NumberCompareResult::Less => Some(true),
    }
}

// None if either denominator is zero; Some(true) if v*y > 0; Some(false) if v*y < 0.
fn two_denominators_product_is_positive(left_den: &str, right_den: &str) -> Option<bool> {
    let l = decimal_str_sign_vs_zero(left_den);
    let r = decimal_str_sign_vs_zero(right_den);
    match (l, r) {
        (NumberCompareResult::Equal, _) | (_, NumberCompareResult::Equal) => None,
        (NumberCompareResult::Less, NumberCompareResult::Less)
        | (NumberCompareResult::Greater, NumberCompareResult::Greater) => Some(true),
        _ => Some(false),
    }
}

fn compare_result_matches_less_order(
    compare_result: NumberCompareResult,
    allow_equal: bool,
    flip: bool,
) -> bool {
    if !flip {
        if allow_equal {
            matches!(
                compare_result,
                NumberCompareResult::Less | NumberCompareResult::Equal
            )
        } else {
            matches!(compare_result, NumberCompareResult::Less)
        }
    } else if allow_equal {
        matches!(
            compare_result,
            NumberCompareResult::Greater | NumberCompareResult::Equal
        )
    } else {
        matches!(compare_result, NumberCompareResult::Greater)
    }
}

impl Runtime {
    pub(crate) fn try_verify_numeric_order_via_div_elimination(
        &self,
        left_obj: &Obj,
        right_obj: &Obj,
        allow_equal: bool,
    ) -> Option<bool> {
        if let (Obj::Div(left_div), Obj::Div(right_div)) = (left_obj, right_obj) {
            let left_denominator_number = self.resolve_obj_to_number_resolved(&left_div.right)?;
            let right_denominator_number = self.resolve_obj_to_number_resolved(&right_div.right)?;
            let left_den_str = left_denominator_number.normalized_value.as_str();
            let right_den_str = right_denominator_number.normalized_value.as_str();
            let product_positive = two_denominators_product_is_positive(left_den_str, right_den_str)?;
            let flip = !product_positive;
            let left_numerator_number = self.resolve_obj_to_number_resolved(&left_div.left)?;
            let right_numerator_number = self.resolve_obj_to_number_resolved(&right_div.left)?;
            let left_product = mul_signed_decimal_str(
                &left_numerator_number.normalized_value,
                &right_denominator_number.normalized_value,
            );
            let right_product = mul_signed_decimal_str(
                &right_numerator_number.normalized_value,
                &left_denominator_number.normalized_value,
            );
            let compare_result = compare_number_strings(&left_product, &right_product);
            return Some(compare_result_matches_less_order(
                compare_result,
                allow_equal,
                flip,
            ));
        }

        if let Obj::Div(right_div) = right_obj {
            let denominator_number = self.resolve_obj_to_number_resolved(&right_div.right)?;
            let flip = nonzero_denominator_requires_flip(&denominator_number.normalized_value)?;
            let numerator_number = self.resolve_obj_to_number_resolved(&right_div.left)?;
            let left_number = self.resolve_obj_to_number_resolved(left_obj)?;
            let left_scaled = mul_signed_decimal_str(
                &left_number.normalized_value,
                &denominator_number.normalized_value,
            );
            let compare_result =
                compare_number_strings(&left_scaled, &numerator_number.normalized_value);
            return Some(compare_result_matches_less_order(
                compare_result,
                allow_equal,
                flip,
            ));
        }

        if let Obj::Div(left_div) = left_obj {
            let denominator_number = self.resolve_obj_to_number_resolved(&left_div.right)?;
            let flip = nonzero_denominator_requires_flip(&denominator_number.normalized_value)?;
            let numerator_number = self.resolve_obj_to_number_resolved(&left_div.left)?;
            let right_number = self.resolve_obj_to_number_resolved(right_obj)?;
            let right_scaled = mul_signed_decimal_str(
                &right_number.normalized_value,
                &denominator_number.normalized_value,
            );
            let compare_result =
                compare_number_strings(&numerator_number.normalized_value, &right_scaled);
            return Some(compare_result_matches_less_order(
                compare_result,
                allow_equal,
                flip,
            ));
        }

        None
    }
}