vstd/arithmetic/internals/
mod_internals_nonlinear.rs

1//! This file contains proofs related to modulo that require
2//! nonlinear-arithmetic reasoning to prove. These are internal
3//! functions used within the math standard library.
4//!
5//! It's based on the following file from the Dafny math standard library:
6//! `Source/DafnyStandardLibraries/src/Std/Arithmetic/Internal/ModInternalsNonlinear.dfy`.
7//! That file has the following copyright notice:
8//! /*******************************************************************************
9//! *  Original: Copyright (c) Microsoft Corporation
10//! *  SPDX-License-Identifier: MIT
11//! *
12//! *  Modifications and Extensions: Copyright by the contributors to the Dafny Project
13//! *  SPDX-License-Identifier: MIT
14//! *******************************************************************************/
15#[allow(unused_imports)]
16use super::super::super::prelude::*;
17
18verus! {
19
20/// Computes `x % y`. This is useful where we want to trigger on a
21/// modulo operator but we need a functional rather than a
22/// mathematical trigger. (A trigger must be fully functional or fully
23/// mathematical.)
24pub open spec fn modulus(x: int, y: int) -> int {
25    x % y
26}
27
28/// Proof that 0 modulo any positive integer `m` is 0
29proof fn lemma_mod_of_zero_is_zero(m: int)
30    requires
31        0 < m,
32    ensures
33        0 as int % m == 0 as int,
34{
35}
36
37/// Proof of the fundamental theorem of division and modulo: That for
38/// any positive divisor `d` and any integer `x`, `x` is equal to `d`
39/// times `x / d` plus `x % d`.
40#[verifier::nonlinear]
41pub proof fn lemma_fundamental_div_mod(x: int, d: int)
42    requires
43        d != 0,
44    ensures
45        x == d * (x / d) + (x % d),
46{
47}
48
49/// Proof that 0 modulo any integer is 0
50proof fn lemma_0_mod_anything()
51    ensures
52        forall|m: int| m > 0 ==> #[trigger] modulus(0, m) == 0,
53{
54}
55
56/// Proof that a natural number `x` divided by a larger natural number
57/// `m` gives a remainder equal to `x`
58#[verifier::nonlinear]
59pub proof fn lemma_small_mod(x: nat, m: nat)
60    requires
61        x < m,
62        0 < m,
63    ensures
64        #[trigger] modulus(x as int, m as int) == x as int,
65{
66}
67
68/// Proof of Euclid's division lemma, i.e., that any integer `x`
69/// modulo any positive integer `m` is in the half-open range `[0, m)`.
70#[verifier::nonlinear]
71pub proof fn lemma_mod_range(x: int, m: int)
72    requires
73        m > 0,
74    ensures
75        0 <= #[trigger] modulus(x, m) < m,
76{
77}
78
79} // verus!
vstd/arithmetic/internals/mod_internals_nonlinear.rs

vstd/arithmetic/internals/
mod_internals_nonlinear.rs
