vstd/arithmetic/internals/
div_internals_nonlinear.rs

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
//! This file contains proofs related to division that require
//! nonlinear-arithmetic reasoning to prove. These are internal
//! functions used within the math standard library.
//!
//! It's based on the following file from the Dafny math standard library:
//! `Source/DafnyStandardLibraries/src/Std/Arithmetic/Internal/DivInternalsNonlinear.dfy`.
//! That file has the following copyright notice:
//! /*******************************************************************************
//! *  Original: Copyright (c) Microsoft Corporation
//! *  SPDX-License-Identifier: MIT
//! *
//! *  Modifications and Extensions: Copyright by the contributors to the Dafny Project
//! *  SPDX-License-Identifier: MIT
//! *******************************************************************************/
#[allow(unused_imports)]
use super::super::super::prelude::*;

verus! {

/// Proof that 0 divided by any given integer `d` is 0
#[verifier::nonlinear]
pub proof fn lemma_div_of0(d: int)
    requires
        d != 0 as int,
    ensures
        0 as int / d == 0 as int,
{
}

/// Proof that any given integer `d` divided by itself is 1
pub proof fn lemma_div_by_self(d: int)
    requires
        d != 0,
    ensures
        d / d == 1,
{
}

/// Proof that dividing a non-negative integer by a larger integer results in a quotient of 0
#[verifier::nonlinear]
pub proof fn lemma_small_div()
    ensures
        forall|x: int, d: int| 0 <= x < d && d > 0 ==> #[trigger] (x / d) == 0,
{
}

} // verus!