regorus 0.12.0

A fast, lightweight Rego (OPA policy language) interpreter
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

// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.

use vstd::prelude::*;

verus! {

use super::bigint_assumptions::bigint_bits_ensures;
use vstd::arithmetic::power2::{lemma2_to64_rest, lemma_pow2_strictly_increases, pow2};

pub proof fn lemma_bigint_bits_le_53()
    ensures
        forall|value: int, bits: nat| #[trigger] bigint_bits_ensures(value, bits) ==>
            ((bits <= 53) == (-9_007_199_254_740_992 < value < 9_007_199_254_740_992)),
{
    lemma2_to64_rest();
    assert(pow2(53) == 9_007_199_254_740_992);
    assert forall|value: int, bits: nat| #[trigger] bigint_bits_ensures(value, bits) implies
        ((bits <= 53) == (-9_007_199_254_740_992 < value < 9_007_199_254_740_992)) by
    {
        if bigint_bits_ensures(value, bits) {
            if bits < 53 {
                lemma_pow2_strictly_increases(bits, 53);
            } else if bits > 53 {
                assert(!( -(pow2(53) as int) < value < pow2(53) ));
            }
        }
    }
}

}