vstd/arithmetic/internals/
mul_internals.rs

Help
1//! This file contains proofs related to multiplication. These are
2//! internal functions used within the math standard library.
3//!
4//! It's based on the following file from the Dafny math standard library:
5//! `Source/DafnyStandardLibraries/src/Std/Arithmetic/Internal/MulInternals.dfy`.
6//! That file has the following copyright notice:
7//! /*******************************************************************************
8//! *  Original: Copyright (c) Microsoft Corporation
9//! *  SPDX-License-Identifier: MIT
10//! *
11//! *  Modifications and Extensions: Copyright by the contributors to the Dafny Project
12//! *  SPDX-License-Identifier: MIT
13//! *******************************************************************************/
14#[allow(unused_imports)]
15use super::super::super::prelude::*;
16
17#[cfg(verus_keep_ghost)]
18use super::super::super::arithmetic::internals::general_internals::{
19    is_le, lemma_induction_helper,
20};
21use super::super::super::arithmetic::internals::mul_internals_nonlinear as MulINL;
22#[cfg(verus_keep_ghost)]
23use super::super::super::math::{add as add1, sub as sub1};
24
25verus! {
26
27/// This function performs multiplication recursively. It's only valid
28/// when `x` is non-negative.
29#[verifier::opaque]
30pub open spec fn mul_pos(x: int, y: int) -> int
31    recommends
32        x >= 0,
33    decreases x,
34{
35    if x <= 0 {
36        0
37    } else {
38        y + mul_pos(x - 1, y)
39    }
40}
41
42/// This function performs multiplication recursively.
43pub open spec fn mul_recursive(x: int, y: int) -> int {
44    if x >= 0 {
45        mul_pos(x, y)
46    } else {
47        -1 * mul_pos(-1 * x, y)
48    }
49}
50
51/// This utility function helps prove a mathematical property by
52/// induction. The caller supplies an integer predicate, proves the
53/// predicate holds in the base case of 0, and proves correctness of
54/// inductive steps both upward and downward from the base case. This
55/// lemma invokes induction to establish that the predicate holds for
56/// all integers.
57///
58/// To prove inductive steps upward from the base case, the caller
59/// must establish that, for any `i >= 0`, `f(i) ==> f(add1(i, 1))`.
60/// `add1(i, 1)` is just `i + 1`, but written in a functional style
61/// so that it can be used where functional triggers are required.
62///
63/// To prove inductive steps downward from the base case, the caller
64/// must establish that, for any `i <= 0`, `f(i) ==> f(sub1(i, 1))`.
65/// `sub1(i, 1)` is just `i - 1`, but written in a functional style
66/// so that it can be used where functional triggers are required.
67pub proof fn lemma_mul_induction(f: spec_fn(int) -> bool)
68    requires
69        f(0),
70        forall|i: int| i >= 0 && #[trigger] f(i) ==> #[trigger] f(add1(i, 1)),
71        forall|i: int| i <= 0 && #[trigger] f(i) ==> #[trigger] f(sub1(i, 1)),
72    ensures
73        forall|i: int| #[trigger] f(i),
74{
75    assert forall|i: int| #[trigger] f(i) by { lemma_induction_helper(1, f, i) };
76}
77
78/// Proof that multiplication is always commutative
79pub broadcast proof fn lemma_mul_commutes(x: int, y: int)
80    ensures
81        #[trigger] (x * y) == y * x,
82{
83}
84
85/// Proof that multiplication distributes over addition by 1 and
86/// over subtraction by 1
87proof fn lemma_mul_successor()
88    ensures
89        forall|x: int, y: int| #[trigger] ((x + 1) * y) == x * y + y,
90        forall|x: int, y: int| #[trigger] ((x - 1) * y) == x * y - y,
91{
92    assert forall|x: int, y: int| #[trigger] ((x + 1) * y) == x * y + y by {
93        MulINL::lemma_mul_is_distributive_add(y, x, 1);
94    }
95    assert forall|x: int, y: int| #[trigger] ((x - 1) * y) == x * y - y by {
96        assert((x - 1) * y == y * (x - 1));
97        MulINL::lemma_mul_is_distributive_add(y, x, -1);
98        assert(y * (x - 1) == y * x + y * -1);
99        assert(-1 * y == -y);
100        assert(x * y + (-1 * y) == x * y - y);
101    }
102}
103
104/// Proof that multiplication distributes over addition and over
105/// subtraction
106#[verifier::spinoff_prover]
107pub broadcast proof fn lemma_mul_distributes_plus(x: int, y: int, z: int)
108    ensures
109        #[trigger] ((x + y) * z) == (x * z + y * z),
110{
111    lemma_mul_successor();
112    assert forall|x: int, y: int, z: int| #[trigger] ((x + y) * z) == (x * z + y * z) by {
113        let f1 = |i: int| ((x + i) * z) == (x * z + i * z);
114        assert(f1(0));
115        assert forall|i: int| i >= 0 && #[trigger] f1(i) implies #[trigger] f1(add1(i, 1)) by {
116            assert((x + (i + 1)) * z == ((x + i) + 1) * z == (x + i) * z + z);
117        };
118        assert forall|i: int| i <= 0 && #[trigger] f1(i) implies #[trigger] f1(sub1(i, 1)) by {
119            assert((x + (i - 1)) * z == ((x + i) - 1) * z == (x + i) * z - z);
120        };
121        lemma_mul_induction(f1);
122        assert(f1(y));
123    }
124}
125
126#[verifier::spinoff_prover]
127pub broadcast proof fn lemma_mul_distributes_minus(x: int, y: int, z: int)
128    ensures
129        #[trigger] ((x - y) * z) == (x * z - y * z),
130{
131    lemma_mul_successor();
132    assert forall|x: int, y: int, z: int| #[trigger] ((x - y) * z) == (x * z - y * z) by {
133        let f2 = |i: int| ((x - i) * z) == (x * z - i * z);
134        assert(f2(0));
135        assert forall|i: int| i >= 0 && #[trigger] f2(i) implies #[trigger] f2(add1(i, 1)) by {
136            assert((x - (i + 1)) * z == ((x - i) - 1) * z == (x - i) * z - z);
137        };
138        assert forall|i: int| i <= 0 && #[trigger] f2(i) implies #[trigger] f2(sub1(i, 1)) by {
139            assert((x - (i - 1)) * z == ((x - i) + 1) * z == (x - i) * z + z);
140        };
141        lemma_mul_induction(f2);
142        assert(f2(y));
143    }
144}
145
146/// This function expresses that multiplication is commutative,
147/// distributes over addition, and distributes over subtraction
148pub open spec fn mul_auto() -> bool {
149    &&& forall|x: int, y: int| #[trigger] (x * y) == (y * x)
150    &&& forall|x: int, y: int, z: int| #[trigger] ((x + y) * z) == (x * z + y * z)
151    &&& forall|x: int, y: int, z: int| #[trigger] ((x - y) * z) == (x * z - y * z)
152}
153
154pub broadcast group group_mul_properties_internal {
155    lemma_mul_commutes,
156    lemma_mul_distributes_plus,
157    lemma_mul_distributes_minus,
158}
159
160// Check that the group_mul_properties_internal broadcast group group_provides the same properties as the _auto lemma it replaces
161proof fn lemma_mul_properties_internal_prove_mul_auto()
162    ensures
163        mul_auto(),
164{
165    broadcast use group_mul_properties_internal;
166
167    assert(mul_auto());
168}
169
170/// This utility function helps prove a mathematical property by
171/// induction. The caller supplies an integer predicate `f`, proves
172/// the predicate holds in the base case of 0, and proves correctness
173/// of inductive steps both upward and downward from the base case.
174/// This lemma invokes induction to establish that the predicate holds
175/// for the given integer `x`.
176///
177/// To prove inductive steps upward from the base case, the caller
178/// must establish that, for any `i`, `is_le(0, i)` implies `f(i) ==>
179/// f(i + 1)`.
180///
181/// To prove inductive steps downward from the base case, the caller
182/// must establish that, for any `i`, `is_le(i, 0)` implies `f(i) ==>
183/// f(i - 1)`.
184pub proof fn lemma_mul_induction_auto(x: int, f: spec_fn(int) -> bool)
185    requires
186        mul_auto() ==> {
187            &&& f(0)
188            &&& (forall|i| #[trigger] is_le(0, i) && f(i) ==> f(i + 1))
189            &&& (forall|i| #[trigger] is_le(i, 0) && f(i) ==> f(i - 1))
190        },
191    ensures
192        mul_auto(),
193        f(x),
194{
195    broadcast use group_mul_properties_internal;
196
197    assert(forall|i| is_le(0, i) && #[trigger] f(i) ==> f(i + 1));
198    assert(forall|i| is_le(i, 0) && #[trigger] f(i) ==> f(i - 1));
199    lemma_mul_induction(f);
200}
201
202/// This utility function helps prove a mathematical property by
203/// induction. The caller supplies an integer predicate `f`, proves
204/// the predicate holds in the base case of 0, and proves correctness
205/// of inductive steps both upward and downward from the base case.
206/// This lemma invokes induction to establish that the predicate holds
207/// for all integers.
208///
209/// To prove inductive steps upward from the base case, the caller
210/// must establish that, for any `i`, `is_le(0, i)` implies `f(i) ==>
211/// f(i + 1)`.
212///
213/// To prove inductive steps downward from the base case, the caller
214/// must establish that, for any `i`, `is_le(i, 0)` implies `f(i) ==>
215/// f(i - 1)`.
216pub proof fn lemma_mul_induction_auto_forall(f: spec_fn(int) -> bool)
217    requires
218        mul_auto() ==> {
219            &&& f(0)
220            &&& (forall|i| #[trigger] is_le(0, i) && f(i) ==> f(i + 1))
221            &&& (forall|i| #[trigger] is_le(i, 0) && f(i) ==> f(i - 1))
222        },
223    ensures
224        mul_auto(),
225        forall|i| #[trigger] f(i),
226{
227    assert(mul_auto()) by {
228        lemma_mul_induction_auto(0, f);
229    }
230    assert forall|i| #[trigger] f(i) by {
231        lemma_mul_induction_auto(i, f);
232    }
233}
234
235} // verus!
vstd/arithmetic/internals/mul_internals.rs

vstd/arithmetic/internals/
mul_internals.rs
