vstd/arithmetic/internals/
mul_internals_nonlinear.rs

1//! This file contains proofs related to multiplication 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/MulInternalsNonlinear.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/*
16   WARNING: Think three times before adding to this file, as nonlinear
17   verification is highly unstable!
18*/
19// may be try to use singular?
20#[allow(unused_imports)]
21use super::super::super::prelude::*;
22
23verus! {
24
25/// Proof that multiplying two positive integers `x` and `y` will result in a positive integer
26#[verifier::nonlinear]
27pub proof fn lemma_mul_strictly_positive(x: int, y: int)
28    ensures
29        (0 < x && 0 < y) ==> (0 < x * y),
30{
31}
32
33/// Proof that `x` and `y` are both nonzero if and only if `x * y` is nonzero
34#[verifier::nonlinear]
35pub proof fn lemma_mul_nonzero(x: int, y: int)
36    ensures
37        x * y != 0 <==> x != 0 && y != 0,
38{
39}
40
41/// Proof that multiplication is associative in this specific case,
42/// i.e., that `x * y * z` is the same no matter which of the two
43/// multiplications is done first
44#[verifier::nonlinear]
45pub proof fn lemma_mul_is_associative(x: int, y: int, z: int)
46    ensures
47        x * (y * z) == (x * y) * z,
48{
49}
50
51/// Proof that multiplication distributes over addition in this
52/// specific case, i.e., that `x * (y + z)` equals `x * y` plus `x * z`
53#[verifier::nonlinear]
54pub proof fn lemma_mul_is_distributive_add(x: int, y: int, z: int)
55    ensures
56        x * (y + z) == x * y + x * z,
57{
58}
59
60/// Proof that the if the product of two nonzero integers `x` and `y`
61/// is nonnegative, then it's greater than or equal to each of `x` and
62/// `y`
63#[verifier::nonlinear]
64pub proof fn lemma_mul_ordering(x: int, y: int)
65    requires
66        x != 0,
67        y != 0,
68        0 <= x * y,
69    ensures
70        x * y >= x && x * y >= y,
71{
72}
73
74/// Proof that multiplying by a positive integer preserves inequality
75/// in this specific case, i.e., that since `x < y` and `z > 0` we can
76/// conclude that `x * z < y * z`.
77#[verifier::nonlinear]
78pub proof fn lemma_mul_strict_inequality(x: int, y: int, z: int)
79    requires
80        x < y,
81        z > 0,
82    ensures
83        x * z < y * z,
84{
85}
86
87} // verus!
vstd/arithmetic/internals/mul_internals_nonlinear.rs

vstd/arithmetic/internals/
mul_internals_nonlinear.rs
