Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394959697989910010110210310410510610710810911011111211311411511611711811912012112212312412512612712812913013113213313413513613713813914014114214314414514614714814915015115215315415515615715815916016116216316416516616716816917017117217317417517617717817918018118218318418518618718818919019119219319419519619719819920020120220320420520620720820921021121221321421521621721821922022122222322422522622722822923023123223323423523623723823924024124224324424524624724824925025125225325425525625725825926026126226326426526626726826927027127227327427527627727827928028128228328428528628728828929029129229329429529629729829930030130230330430530630730830931031131231331431531631731831932032132232332432532632732832933033133233333433533633733833934034134234334434534634734834935035135235335435535635735835936036136236336436536636736836937037137237337437537637737837938038138238338438538638738838939039139239339439539639739839940040140240340440540640740840941041141241341441541641741841942042142242342442542642742842943043143243343443543643743843944044144244344444544644744844945045145245345445545645745845946046146246346446546646746846947047147247347447547647747847948048148248348448548648748848949049149249349449549649749849950050150250350450550650750850951051151251351451551651751851952052152252352452552652752852953053153253353453553653753853954054154254354454554654754854955055155255355455555655755855956056156256356456556656756856957057157257357457557657757857958058158258358458558658758858959059159259359459559659759859960060160260360460560660760860961061161261361461561661761861962062162262362462562662762862963063163263363463563663763863964064164264364464564664764864965065165265365465565665765865966066166266366466566666766866967067167267367467567667767867968068168268368468568668768868969069169269369469569669769869970070170270370470570670770870971071171271371471571671771871972072172272372472572672772872973073173273373473573673773873974074174274374474574674774874975075175275375475575675775875976076176276376476576676776876977077177277377477577677777877978078178278378478578678778878979079179279379479579679779879980080180280380480580680780880981081181281381481581681781881982082182282382482582682782882983083183283383483583683783883984084184284384484584684784884985085185285385485585685785885986086186286386486586686786886987087187287387487587687787887988088188288388488588688788888989089189289389489589689789889990090190290390490590690790890991091191291391491591691791891992092192292392492592692792892993093193293393493593693793893994094194294394494594694794894995095195295395495595695795895996096196296396496596696796896997097197297397497597697797897998098198298398498598698798898999099199299399499599699799899910001001100210031004100510061007100810091010101110121013101410151016101710181019102010211022102310241025102610271028102910301031103210331034103510361037103810391040104110421043104410451046104710481049105010511052105310541055105610571058105910601061106210631064106510661067106810691070107110721073107410751076107710781079108010811082108310841085108610871088108910901091109210931094109510961097109810991100110111021103110411051106110711081109111011111112111311141115111611171118111911201121112211231124112511261127112811291130113111321133113411351136113711381139114011411142114311441145114611471148114911501151115211531154115511561157115811591160116111621163116411651166116711681169117011711172117311741175117611771178117911801181118211831184118511861187118811891190119111921193119411951196119711981199120012011202120312041205120612071208120912101211121212131214121512161217121812191220122112221223122412251226122712281229123012311232123312341235123612371238123912401241124212431244124512461247124812491250125112521253125412551256125712581259126012611262126312641265126612671268126912701271127212731274127512761277127812791280128112821283128412851286128712881289129012911292129312941295129612971298129913001301130213031304130513061307130813091310131113121313131413151316131713181319132013211322132313241325132613271328132913301331133213331334133513361337133813391340134113421343134413451346134713481349135013511352135313541355135613571358135913601361136213631364136513661367136813691370137113721373137413751376137713781379138013811382138313841385138613871388138913901391139213931394139513961397139813991400140114021403140414051406140714081409141014111412141314141415141614171418141914201421142214231424142514261427142814291430143114321433143414351436143714381439144014411442144314441445144614471448144914501451145214531454145514561457145814591460146114621463146414651466146714681469147014711472147314741475147614771478147914801481148214831484148514861487148814891490149114921493149414951496149714981499150015011502150315041505150615071508150915101511151215131514151515161517151815191520152115221523152415251526152715281529153015311532153315341535153615371538153915401541154215431544154515461547154815491550155115521553155415551556155715581559156015611562156315641565156615671568156915701571157215731574157515761577157815791580158115821583158415851586158715881589159015911592159315941595159615971598159916001601160216031604160516061607160816091610161116121613161416151616161716181619162016211622162316241625162616271628162916301631163216331634163516361637163816391640164116421643164416451646164716481649165016511652165316541655165616571658165916601661166216631664166516661667166816691670//! This file contains proofs related to integer division (`/`) and//! remainder aka mod (`%`). These are part of the math standard library.//!//! It's based on the following file from the Dafny math standard//! library://! `Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.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//! *******************************************************************************/use super::super::calc_macro::*;#[allow(unused_imports)]use super::super::prelude::*;
verus! {
#[verifier::inline]#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::arithmetic::div_mod::rust_div")]pub open spec fn rust_div(a: int, b: int) -> int recommends b != 0,{ if a == 0 { 0 } else if a > 0 { a / b } else { -((-a) / b) }}
#[verifier::inline]#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::arithmetic::div_mod::rust_rem")]pub open spec fn rust_rem(a: int, b: int) -> int recommends b != 0,{ if a == 0 { 0 } else if a > 0 { a % b } else { -((-a) % b) }}
#[allow(unused_imports)]#[cfg(verus_keep_ghost)]use super::super::arithmetic::internals::div_internals::{ div_recursive, lemma_div_induction_auto, div_auto, div_pos, lemma_div_auto,};use super::super::arithmetic::internals::div_internals_nonlinear as DivINL;#[cfg(verus_keep_ghost)]use super::super::arithmetic::internals::mod_internals::{ lemma_div_add_denominator, lemma_mod_auto, mod_recursive,};use super::super::arithmetic::internals::mod_internals_nonlinear as ModINL;#[cfg(verus_keep_ghost)]use super::internals::mul_internals::{ group_mul_properties_internal, lemma_mul_induction, lemma_mul_induction_auto,};#[cfg(verus_keep_ghost)]use super::super::arithmetic::internals::general_internals::{is_le};#[cfg(verus_keep_ghost)]use super::super::math::{add as add1, sub as sub1, div as div1};use super::super::arithmetic::mul::*;
/****************************************************************************** Division*****************************************************************************/
/// Proof that, for the case of `x / d`, division using `/` is/// equivalent to a recursive definition of division.pub broadcast proof fn lemma_div_is_div_recursive(x: int, d: int) requires 0 < d, ensures div_recursive(x, d) == #[trigger] (x / d),{ reveal(div_recursive); reveal(div_pos); lemma_div_induction_auto(d, x, |u: int| div_recursive(u, d) == u / d);}
/// Proof that the quotient of an integer divided by itself is 1,/// specifically that `d / d == 1`.pub proof fn lemma_div_by_self(d: int) requires d != 0, ensures d / d == 1,{ DivINL::lemma_div_by_self(d);}
/// Proof that 0 divided by a nonzero integer is 0, specifically `0 / d == 0`.pub proof fn lemma_div_of0(d: int) requires d != 0, ensures 0 as int / d == 0,{ DivINL::lemma_div_of0(d);}
/// Proof establishing basic properties of division using `x`: 0/// divided by `x` is 0; `x` divided by 1 is itself; and `x` divided/// by itself is 1.pub proof fn lemma_div_basics(x: int) ensures x != 0 as int ==> 0 as int / x == 0, x / 1 == x, x != 0 ==> x / x == 1,{ if (x != 0) { lemma_div_by_self(x); lemma_div_of0(x); }}
/// Proof for basic property that 0 divided by `x` is 0.pub broadcast proof fn lemma_div_basics_1(x: int) ensures x != 0 as int ==> #[trigger] (0int / x) == 0,{ lemma_div_basics(x);}
/// Proof for basic property that `x` divided by 1 is `x`.pub broadcast proof fn lemma_div_basics_2(x: int) ensures #[trigger] (x / 1) == x,{ lemma_div_basics(x);}
/// Proof for basic property that `x` divided by `x` is 1.pub broadcast proof fn lemma_div_basics_3(x: int) ensures x != 0 ==> #[trigger] (x / x) == 1,{ lemma_div_basics(x);}
/// Proof that dividing any non-negative integer by a positive integer is non-zero.pub broadcast proof fn lemma_div_basics_4(x: int, y: int) ensures x >= 0 && y > 0 ==> #[trigger] (x / y) >= 0,{}
/// Proof that the quotient produced by dividing any non-negative integer `x`/// by a positive integer `y` is at most `x`.pub broadcast proof fn lemma_div_basics_5(x: int, y: int) ensures x >= 0 && y > 0 ==> #[trigger] (x / y) <= x,{ assert forall|x: int, y: int| x >= 0 && y > 0 implies 0 <= #[trigger] (x / y) <= x by { lemma_div_pos_is_pos(x, y); lemma_div_is_ordered_by_denominator(x, 1, y); };}
pub broadcast group group_div_basics { lemma_div_basics_1, lemma_div_basics_2, lemma_div_basics_3, lemma_div_basics_4, lemma_div_basics_5,}
/// Proof that if a dividend is a whole number, the divisor is a/// natural number, and their quotient is 0, then the dividend is/// smaller than the divisor.pub broadcast proof fn lemma_small_div_converse(x: int, d: int) ensures 0 <= x && 0 < d && #[trigger] (x / d) == 0 ==> x < d,{ assert forall|x: int, d: int| 0 <= x && 0 < d && #[trigger] (x / d) == 0 implies x < d by { lemma_div_induction_auto(d, x, |u: int| 0 <= u && 0 < d && u / d == 0 ==> u < d); }}
/// Proof that division of a positive integer by a positive integer/// less than or equal to it is nonzero. Specifically,/// given that `x >= d`, we can conclude that `x / d > 0`.pub proof fn lemma_div_non_zero(x: int, d: int) requires x >= d > 0, ensures #[trigger] (x / d) > 0,{ broadcast use lemma_div_pos_is_pos;
if x / d == 0 { broadcast use lemma_small_div_converse;
}}
/// Proof that given two fractions with the same numerator, the order/// of the fractions is determined by the denominators. However, if/// the numerator is 0, the fractions are equal regardless of the/// denominators' values. Specifically, given that `1 <= y <= z`, we/// know `x / y >= x / z`.pub broadcast proof fn lemma_div_is_ordered_by_denominator(x: int, y: int, z: int) requires 0 <= x, 1 <= y <= z, ensures #[trigger] (x / y) >= #[trigger] (x / z), decreases x,{ reveal(div_recursive); reveal(div_pos); broadcast use lemma_div_is_div_recursive;
assert(forall|u: int, d: int| #![trigger div_recursive(u, d)] #![trigger div1(u, d)] d > 0 ==> div_recursive(u, d) == div1(u, d)); if (x < z) { lemma_div_is_ordered(0, x, y); } else { lemma_div_is_ordered(x - z, x - y, y); lemma_div_is_ordered_by_denominator(x - z, y, z); }}
/// Proof that a number gets strictly smaller when divided by a number/// greater than one. Specifically, `x / d < x`.pub broadcast proof fn lemma_div_is_strictly_smaller(x: int, d: int) requires 0 < x, 1 < d, ensures #[trigger] (x / d) < x, decreases x,{ lemma_div_induction_auto(d, x, |u: int| 0 < u ==> u / d < u);}
/// Proof that, given `r == a % d + b % d - (a + b) % d`, `r` can also/// be expressed as `d * ((a + b) / d) - d * (a / d) - d * (b / d)`.pub broadcast proof fn lemma_dividing_sums(a: int, b: int, d: int, r: int) requires 0 < d, r == a % d + b % d - (a + b) % d, ensures #![trigger (d * ((a + b) / d) - r), (d * (a / d) + d * (b / d))] d * ((a + b) / d) - r == d * (a / d) + d * (b / d),{ ModINL::lemma_fundamental_div_mod(a + b, d); ModINL::lemma_fundamental_div_mod(a, d); ModINL::lemma_fundamental_div_mod(b, d);}
/// Proof that dividing a whole number by a natural number will result/// in a quotient that is greater than or equal to 0. Specifically,/// `x / d >= 0`.pub broadcast proof fn lemma_div_pos_is_pos(x: int, d: int) requires 0 <= x, 0 < d, ensures 0 <= #[trigger] (x / d),{ lemma_div_auto(d); assert(div_auto(d)); let f = |u: int| 0 <= u ==> u / d >= 0; assert forall|i: int| #[trigger] is_le(0, i) && f(i) implies f(i + d) by { assert(i / d >= 0); }; lemma_div_induction_auto(d, x, |u: int| 0 <= u ==> u / d >= 0);}
/// Proof that dividing a number then adding 1 gives the same result/// as adding the divisor and then doing the division. Specifically,/// `1 + (x / d)` is equal to `(d + x) / d`.pub broadcast proof fn lemma_div_plus_one(x: int, d: int) requires 0 < d, ensures #![trigger (1 + x / d), ((d + x) / d)] 1 + x / d == (d + x) / d,{ lemma_div_auto(d);}
/// Proof that dividing a number then subtracting 1 gives the same result/// as subtracting the divisor and then doing the division. Specifically,/// `-1 + (x / d)` is equal to `(-d + x) / d`.pub broadcast proof fn lemma_div_minus_one(x: int, d: int) requires 0 < d, ensures #![trigger (-1 + x / d), ((-d + x) / d)] -1 + x / d == (-d + x) / d,{ lemma_div_auto(d);}
/// Proof that dividing any non-negative integer less than `d` by `d`/// produces a quotient of 0.pub proof fn lemma_basic_div_specific_divisor(d: int) requires 0 < d, ensures forall|x: int| 0 <= x < d ==> #[trigger] (x / d) == 0,{ lemma_div_auto(d);}
/// Proof that dividing any non-negative integer by a larger integer/// produces a quotient of 0.pub broadcast proof fn lemma_basic_div(x: int, d: int) requires 0 <= x < d, ensures #[trigger] (x / d) == 0,{ lemma_basic_div_specific_divisor(d);}
/// Proof that numerical order is preserved when dividing two seperate/// integers by a common positive divisor. Specifically, given that/// `z > 0` and `x <= y`, we know `x / z <= y / z`.pub broadcast proof fn lemma_div_is_ordered(x: int, y: int, z: int) requires x <= y, 0 < z, ensures #[trigger] (x / z) <= #[trigger] (y / z),{ lemma_div_auto(z); let f = |xy: int| xy <= 0 ==> (xy + y) / z <= y / z; assert forall|i: int| #[trigger] is_le(i + 1, z) && f(i) implies f(i - z) by { if (i - z <= 0) { assert(f(i)); assert(i <= 0 ==> (i + y) / z <= y / z); if (i > 0) { assert(z > 0); assert(i <= z); assert(((i + y) - z) / z <= y / z); } else { assert((i + y) / z <= y / z); } assert((i - z + y) / z <= y / z); } }; lemma_div_induction_auto(z, x - y, |xy: int| xy <= 0 ==> (xy + y) / z <= y / z);}
/// Proof that dividing an integer by 2 or more results in a quotient/// that is smaller than the original dividend. Specifically, `x / d < x`.pub broadcast proof fn lemma_div_decreases(x: int, d: int) requires 0 < x, 1 < d, ensures #[trigger] (x / d) < x,{ lemma_div_induction_auto(d, x, |u: int| 0 < u ==> u / d < u);}
/// Proof that dividing an integer by 1 or more results in a quotient/// that is less than or equal to the original dividend. Specifically,/// `x / d <= x`.pub broadcast proof fn lemma_div_nonincreasing(x: int, d: int) requires 0 <= x, 0 < d, ensures #[trigger] (x / d) <= x,{ lemma_div_induction_auto(d, x, |u: int| 0 <= u ==> u / d <= u);}
/// Proof that a natural number x divided by a larger natural number/// gives a remainder equal to x. Specifically, because `x < m`, we/// know `x % m == x`.pub proof fn lemma_small_mod(x: nat, m: nat) requires x < m, 0 < m, ensures x % m == x,{ ModINL::lemma_small_mod(x, m);}
/// The remainder of a nonnegative integer `x` divided by the product of two positive integers/// `y` and `z` is equivalent to dividing `x` by `y`, dividing the quotient by `z`, multiplying/// the remainder by `y`, and then adding the product to the remainder of `x` divided by `y`./// In mathematical terms, `(x % (y * z)) == y * ((x / y) % z) + x % y`.pub broadcast proof fn lemma_breakdown(x: int, y: int, z: int) requires 0 <= x, 0 < y, 0 < z, ensures #![trigger y * z, x % (y * z), y * ((x / y) % z) + x % y] 0 < y * z, (x % (y * z)) == y * ((x / y) % z) + x % y,{ broadcast use lemma_mul_strictly_positive;
lemma_div_pos_is_pos(x, y); calc! { (<) (y * (x / y)) % (y * z) + (x % y) % (y * z); (<=) { lemma_part_bound1(x, y, z); } y * (z - 1) + (x % y) % (y * z); (<) { lemma_part_bound2(x, y, z); } y * (z - 1) + y; (==) { broadcast use group_mul_basics;
} y * (z - 1) + y * 1; (==) { broadcast use group_mul_is_distributive;
} y * (z - 1 + 1); (==) {} y * z; } calc! { (==) x % (y * z); { ModINL::lemma_fundamental_div_mod(x, y); } (y * (x / y) + x % y) % (y * z); { broadcast use group_mod_properties;
assert(0 <= x % y); lemma_mul_nonnegative(y, x / y); assert((y * (x / y)) % (y * z) + (x % y) % (y * z) < y * z); lemma_mod_adds(y * (x / y), x % y, y * z); } (y * (x / y)) % (y * z) + (x % y) % (y * z); { broadcast use {group_mod_properties, lemma_mul_is_commutative};
lemma_mul_increases(z, y); // comparison op can't be chained in calc! // assert forall is also not avaialable in calc! assert((x % y) < y && y <= (y * z)); lemma_small_mod((x % y) as nat, (y * z) as nat); assert((x % y) % (y * z) == x % y); } (y * (x / y)) % (y * z) + x % y; { lemma_truncate_middle(x / y, y, z); } y * ((x / y) % z) + x % y; }}
/// Proof that the difference between a nonnegative integer `x` and a/// positive integer `d` must be strictly less than the quotient of/// `x` divided by `d` and then multiplied by `d`.pub broadcast proof fn lemma_remainder_upper(x: int, d: int) requires 0 <= x, 0 < d, ensures #![trigger (x - d), (x / d * d)] x - d < x / d * d,{ broadcast use group_mul_properties_internal;
lemma_div_induction_auto(d, x, |u: int| 0 <= u ==> u - d < u / d * d);}
/// Proof that the division of a nonnegative integer `x` by a positive/// integer `d` multiplied by `d` is less than or equal to the value/// of `x`.pub broadcast proof fn lemma_remainder_lower(x: int, d: int) requires 0 <= x, 0 < d, ensures x >= #[trigger] (x / d * d),{ broadcast use group_mul_properties_internal;
lemma_div_induction_auto(d, x, |u: int| 0 <= u ==> u >= u / d * d);}
/// Proof that the difference between a nonnegative integer `x` and/// the division of `x` by a positive integer `d` multiplied by `d` is/// lower bounded (inclusively) by 0 and upper bounded (exclusively)/// by `d`.pub broadcast proof fn lemma_remainder(x: int, d: int) requires 0 <= x, 0 < d, ensures 0 <= #[trigger] (x - (x / d * d)) < d,{ broadcast use group_mul_properties_internal;
lemma_div_induction_auto(d, x, |u: int| 0 <= u - u / d * d < d);}
/// Proof of the fundamental theorem of division and modulo, namely/// that `x` can be expressed as `d` times the quotient `x / d` plus/// the remainder `x % d`.pub broadcast proof fn lemma_fundamental_div_mod(x: int, d: int) requires d != 0, ensures x == #[trigger] (d * (x / d) + (x % d)),{ assert(x == d * (x / d) + (x % d)) by { ModINL::lemma_fundamental_div_mod(x, d); }}
/// Proof that dividing `x` by `c * d` is equivalent to first dividing/// `x` by `c` and then dividing the result by `d`.pub broadcast proof fn lemma_div_denominator(x: int, c: int, d: int) requires 0 <= x, 0 < c, 0 < d, ensures c * d != 0, #[trigger] ((x / c) / d) == x / (c * d),{ lemma_mul_strictly_positive(c, d); let r = x % (c as int * d as int); lemma_div_pos_is_pos(r, c as int); if (r / c as int >= d) { ModINL::lemma_fundamental_div_mod(r, c as int); lemma_mul_inequality(d as int, r / c as int, c as int); lemma_mul_is_commutative(d, c); } assert(r / (c as int) < d); lemma_fundamental_div_mod_converse(r / c, d, 0, r / c); assert((r / c as int) % d as int == r / c as int); lemma_fundamental_div_mod(r, c); assert(c * (r / c) + r % c == r); assert(c * ((r / c as int) % d as int) + r % c as int == r); let k = x / (c as int * d as int); lemma_fundamental_div_mod(x, c * d); assert(x == (c * d) * (x / (c * d)) + x % (c * d)); assert(r == x - (c * d) * (x / (c * d))); assert(r == x - (c * d) * k); calc! { (==) c * ((x / c) % d) + x % c; { broadcast use lemma_mul_is_commutative;
lemma_mod_multiples_vanish(-k, x / c, d); } c * ((x / c + (-k) * d) % d) + x % c; { lemma_hoist_over_denominator(x, (-k) * d, c as nat); } c * (((x + (((-k) * d) * c)) / c) % d) + x % c; { lemma_mul_is_associative(-k, d, c); } c * (((x + ((-k) * (d * c))) / c) % d) + x % c; { lemma_mul_unary_negation(k, d * c); } c * (((x + (-(k * (d * c)))) / c) % d) + x % c; { lemma_mul_is_associative(k, d, c); } c * (((x + (-(k * d * c))) / c) % d) + x % c; {} c * (((x - k * d * c) / c) % d) + x % c; { broadcast use {lemma_mul_is_associative, lemma_mul_is_commutative};
} c * ((r / c) % d) + x % c; {} c * (r / c) + x % c; { lemma_fundamental_div_mod(r, c); assert(r == c * (r / c) + r % c); lemma_mod_mod(x, c, d); assert(r % c == x % c); } r; { broadcast use {group_mod_properties, lemma_mod_is_mod_recursive};
} r % (c * d); {} (x - (c * d) * k) % (c * d); { lemma_mul_unary_negation(c * d, k); } (x + (c * d) * (-k)) % (c * d); { lemma_mod_multiples_vanish(-k, x, c * d); } x % (c * d); } assert(c * (x / c) + x % c - r == c * (x / c) - c * ((x / c) % d) ==> x - r == c * (x / c) - c * ((x / c) % d)) by { lemma_fundamental_div_mod(x, c); }; assert(c * (x / c) + x % c - r == c * (x / c) - c * ((x / c) % d)); assert(x - r == c * (x / c) - c * ((x / c) % d)); assert((x / c) / d == x / (c * d)) by { lemma_fundamental_div_mod(x / c, d); assert(d * ((x / c) / d) == x / c - ((x / c) % d)); lemma_fundamental_div_mod(x, c * d); assert(x == (c * d) * (x / (c * d)) + (x % (c * d))); lemma_mul_is_distributive_sub(c, x / c, (x / c) % d); assert(c * (d * ((x / c) / d)) == c * (x / c) - c * ((x / c) % d)); lemma_mul_is_associative(c, d, (x / c) / d); assert((c * d) * ((x / c) / d) == c * (x / c) - c * ((x / c) % d)); assert((c * d) * ((x / c) / d) == x - r); assert((c * d) * ((x / c) / d) == (c * d) * (x / (c * d))); lemma_mul_equality_converse(c * d, (x / c) / d, x / (c * d)); } assert(c * d != 0) by { assert(0 < c * d); } assert(c * d != 0); // work around https://github.com/Z3Prover/z3/issues/8057}
/// Proof that multiplying an integer by a fraction is equivalent to/// multiplying the fraction's numerator by the integer. Specifically,/// `x * (y / z) == (x * y) / z`.pub broadcast proof fn lemma_mul_hoist_inequality(x: int, y: int, z: int) requires 0 <= x, 0 < z, ensures #![trigger (x * (y / z)), ((x * y) / z)] x * (y / z) <= (x * y) / z,{ calc! { (==) (x * y) / z; (==) { lemma_fundamental_div_mod(y, z); } (x * (z * (y / z) + y % z)) / z; (==) { broadcast use group_mul_is_distributive;
} (x * (z * (y / z)) + x * (y % z)) / z; } assert((x * (z * (y / z)) + x * (y % z)) / z >= x * (y / z)) by { broadcast use {group_mod_properties, lemma_mul_is_associative, lemma_mul_is_commutative};
lemma_mul_nonnegative(x, y % z); lemma_div_is_ordered(x * (z * (y / z)), x * (z * (y / z)) + x * (y % z), z); lemma_div_multiples_vanish(x * (y / z), z); };}
/// Proof that for a positive integer `d`, if `a - a % d` is less than/// or equal to `b` and `b` is less than `a + d - a % d`, then the/// quotient of `a` divided by `d` is equivalent to the quotient of/// `b` divided by `d`.////// In other words, if `a` and `b` occur between the same two/// multiples of `d`, then their quotient with `d` is equivalent.pub broadcast proof fn lemma_indistinguishable_quotients(a: int, b: int, d: int) requires 0 < d, 0 <= a - a % d <= b < a + d - a % d, ensures #![trigger (a / d), (b / d)] a / d == b / d,{ lemma_div_induction_auto( d, a - b, |ab: int| { let u = ab + b; 0 <= u - u % d <= b < u + d - u % d ==> u / d == b / d }, );}
/// Proof that common factors from the dividend and divisor of a/// modulus operation can be factored out. Specifically,/// `(b * x) % (b * c) == b * (x % c)`.pub proof fn lemma_truncate_middle(x: int, b: int, c: int) requires 0 <= x, 0 < b, 0 < c, ensures #![trigger (b * (x % c))] 0 < b * c, (b * x) % (b * c) == b * (x % c),{ broadcast use {lemma_mul_strictly_positive, lemma_mul_nonnegative};
calc! { (==) b * x; { ModINL::lemma_fundamental_div_mod(b * x, b * c); } (b * c) * ((b * x) / (b * c)) + (b * x) % (b * c); { lemma_div_denominator(b * x, b, c); } (b * c) * (((b * x) / b) / c) + (b * x) % (b * c); { broadcast use lemma_mul_is_commutative;
lemma_div_by_multiple(x, b); } (b * c) * (x / c) + (b * x) % (b * c); } assert(b * x == (b * c) * (x / c) + b * (x % c)) by { ModINL::lemma_fundamental_div_mod(x, c); broadcast use {group_mul_is_distributive, lemma_mul_is_associative};
};}
/// Proof that multiplying the numerator and denominator by an integer/// does not change the quotient. Specifically,/// `a / d == (x * a) / (x * d)`.pub broadcast proof fn lemma_div_multiples_vanish_quotient(x: int, a: int, d: int) requires 0 < x, 0 <= a, 0 < d, ensures #![trigger a / d, x * a, x * d] 0 < x * d, a / d == (x * a) / (x * d),{ lemma_mul_strictly_positive(x, d); calc! { (==) (x * a) / (x * d); { lemma_mul_nonnegative(x, a); lemma_div_denominator(x * a, x, d); } ((x * a) / x) / d; { lemma_div_multiples_vanish(a, x); } a / d; }}
/// Proof that, since `a % d == 0` and `0 <= r < d`, we can conclude/// `a == d * (a + r) / d`.#[verifier::spinoff_prover]pub broadcast proof fn lemma_round_down(a: int, r: int, d: int) requires 0 < d, a % d == 0, 0 <= r < d, ensures #![trigger (d * ((a + r) / d))] a == d * ((a + r) / d),{ broadcast use group_mul_properties_internal;
lemma_div_induction_auto(d, a, |u: int| u % d == 0 ==> u == d * ((u + r) / d));}
/// Proof that, since `0 <= b < d`, we have `(d * x + b) / d == x`.pub broadcast proof fn lemma_div_multiples_vanish_fancy(x: int, b: int, d: int) requires 0 < d, 0 <= b < d, ensures #![trigger (d * x + b) / d] (d * x + b) / d == x,{ let f = |u: int| (d * u + b) / d == u; assert(f(0)) by { lemma_div_auto(d); } assert forall|i: int| i >= 0 && #[trigger] f(i) implies #[trigger] f(add1(i, 1)) by { assert(d * (i + 1) + b == d * i + b + d) by { assert(d * (i + 1) == d * i + d) by { lemma_mul_is_distributive_add(d, i, 1); lemma_mul_basics(d); } } super::internals::div_internals::lemma_div_basics(d); } assert forall|i: int| i <= 0 && #[trigger] f(i) implies #[trigger] f(sub1(i, 1)) by { assert(d * (i - 1) + b == d * i + b - d) by { assert(d * (i - 1) == d * i - d) by { lemma_mul_is_distributive_sub(d, i, 1); lemma_mul_basics(d); } } super::internals::div_internals::lemma_div_basics(d); } broadcast use group_mul_properties_internal;
lemma_mul_induction(f); assert(f(x));}
/// Proof that multiplying an integer by a common numerator and/// denominator results in the original integer. Specifically,/// `(d * x) / d == x`.pub broadcast proof fn lemma_div_multiples_vanish(x: int, d: int) requires 0 < d, ensures #![trigger (d * x) / d] (d * x) / d == x,{ lemma_div_multiples_vanish_fancy(x, 0, d);}
/// Proof that multiplying a whole number by a common numerator and/// denominator results in the original integer. Specifically,/// `(b * d) / d == b`.pub broadcast proof fn lemma_div_by_multiple(b: int, d: int) requires 0 <= b, 0 < d, ensures #![trigger ((b * d) / d)] (b * d) / d == b,{ lemma_div_multiples_vanish(b, d); broadcast use group_mul_properties_internal;
}
/// Proof that a dividend that is a positive multiple of a divisor/// will always yield a greater quotient than a smaller dividend./// Specifically, `x / z < y / z` because `y == m * z` and `x < y`.pub broadcast proof fn lemma_div_by_multiple_is_strongly_ordered(x: int, y: int, m: int, z: int) requires x < y, y == m * z, 0 < z, ensures #![trigger x / z, m * z, y / z] x / z < y / z,{ lemma_mod_multiples_basic(m, z); lemma_div_induction_auto( z, y - x, |yx: int| { let u = yx + x; x < u && u % z == 0 ==> x / z < u / z }, );}
/// Proof that if an integer is less than or equal to the product of/// two other integers, then the quotient with one of them will be/// less than or equal to the other of them. Specifically, because/// `a <= b * c`, we know `a / b <= c`.pub broadcast proof fn lemma_multiply_divide_le(a: int, b: int, c: int) requires 0 < b, a <= b * c, ensures #![trigger a / b, b * c] a / b <= c,{ lemma_mod_multiples_basic(c, b); let f = |i: int| 0 <= i && (i + a) % b == 0 ==> a / b <= (i + a) / b; lemma_div_induction_auto(b, b * c - a, f); lemma_div_multiples_vanish(c, b);}
/// Proof that if an integer is less than the product of two other/// integers, then the quotient with one of them will be less than the/// other. Specifically, because `a < b * c`, we know `a / b < c`.pub broadcast proof fn lemma_multiply_divide_lt(a: int, b: int, c: int) requires 0 < b, a < b * c, ensures #![trigger a / b, b * c] a / b < c,{ assert(((b * c - a) + a) % b == 0 ==> a / b < ((b * c - a) + a) / b) by { let f = |i: int| 0 < i && (i + a) % b == 0 ==> a / b < (i + a) / b; lemma_div_induction_auto(b, b * c - a, f); } assert(b * c == c * b) by { lemma_mul_is_commutative(b, c); } assert((b * c) % b == 0) by { lemma_mod_multiples_basic(c, b); } assert((b * c) / b == c) by { lemma_div_multiples_vanish(c, b); }}
/// Proof that adding an integer to a fraction is equivalent to adding/// that integer times the denominator to the numerator. Specifically,/// `x / d + j == (x + j * d) / d`.pub broadcast proof fn lemma_hoist_over_denominator(x: int, j: int, d: nat) requires 0 < d, ensures #![trigger x / d as int + j] x / d as int + j == (x + j * d) / d as int,{ let dd = d as int; let q = x / dd; let r = x % dd; assert(x == dd * q + r) by { lemma_fundamental_div_mod(x, dd); } assert(j * dd == dd * j) by { lemma_mul_is_commutative(j, dd); } assert(x + j * dd == dd * (q + j) + r) by { lemma_mul_is_distributive_add(dd, q, j); } assert((x + j * dd) / dd == q + j) by { lemma_fundamental_div_mod_converse(x + j * d, dd, q + j, r); }}
/// Proof that, for nonnegative integer `a` and positive integers `b` and `c`,/// the remainder of `b * (a / b)` divided by `b * c` is less than or equal to `b * (c - 1)`./// This accounts for the rounding down that occurs in integer division.pub broadcast proof fn lemma_part_bound1(a: int, b: int, c: int) requires 0 <= a, 0 < b, 0 < c, ensures #![trigger (b * (a / b) % (b * c))] 0 < b * c, (b * (a / b) % (b * c)) <= b * (c - 1),{ lemma_mul_strictly_positive(b, a / b); lemma_mul_strictly_positive(b, c); lemma_mul_strictly_positive(b, c - 1); calc! { (==) b * (a / b) % (b * c); { ModINL::lemma_fundamental_div_mod(b * (a / b), b * c); } b * (a / b) - (b * c) * ((b * (a / b)) / (b * c)); { broadcast use lemma_mul_is_associative;
} b * (a / b) - b * (c * ((b * (a / b)) / (b * c))); { broadcast use group_mul_is_distributive;
} b * ((a / b) - (c * ((b * (a / b)) / (b * c)))); } assert(b * (a / b) % (b * c) <= b * (c - 1)) by { broadcast use {lemma_mul_is_commutative, lemma_mul_inequality};
};}
/******************************************************************************** Modulus*******************************************************************************/
/// Proof that computing the modulus using `%` is equivalent to/// computing it with a recursive definition of modulus. Specifically,/// `x % m` is equivalent in that way.pub broadcast proof fn lemma_mod_is_mod_recursive(x: int, m: int) requires m > 0, ensures mod_recursive(x, m) == #[trigger] (x % m), decreases (if x < 0 { -x + m } else { x }),{ reveal(mod_recursive); if x < 0 { calc! { (==) mod_recursive(x, m); {} mod_recursive(x + m, m); { lemma_mod_is_mod_recursive(x + m, m); } (x + m) % m; { lemma_add_mod_noop(x, m, m); } ((x % m) + (m % m)) % m; { broadcast use {lemma_mod_self_0, lemma_mod_twice};
} (x % m) % m; { broadcast use {lemma_mod_self_0, lemma_mod_twice};
} x % m; } } else if x < m { lemma_small_mod(x as nat, m as nat); } else { calc! { (==) mod_recursive(x, m); {} mod_recursive(x - m, m); { lemma_mod_is_mod_recursive(x - m, m); } (x - m) % m; { lemma_sub_mod_noop(x, m, m); } ((x % m) - (m % m)) % m; { broadcast use {lemma_mod_self_0, lemma_mod_twice};
} (x % m) % m; { broadcast use {lemma_mod_self_0, lemma_mod_twice};
} x % m; } }}
/// Proof that any integer divided by itself produces a remainder of 0.pub broadcast proof fn lemma_mod_self_0(m: int) requires m > 0, ensures #[trigger] (m % m) == 0,{ lemma_mod_auto(m);}
/// Proof that performing `(x % m) % m` gives the same result as simply perfoming `x % m`.pub broadcast proof fn lemma_mod_twice(x: int, m: int) requires m > 0, ensures #[trigger] ((x % m) % m) == x % m,{ lemma_mod_auto(m);}
pub broadcast group group_mod_basics { lemma_mod_self_0, lemma_mod_twice,}
/// Proof that the remainder of any division will be less than the divisor's value.pub broadcast proof fn lemma_mod_division_less_than_divisor(x: int, m: int) requires m > 0, ensures 0 <= #[trigger] (x % m) < m,{ lemma_mod_auto(m);}
pub broadcast group group_mod_properties { group_mod_basics, lemma_mod_division_less_than_divisor,}
/// Proof that when natural number `x` is divided by natural number/// `m`, the remainder will be less than or equal to `x`.pub broadcast proof fn lemma_mod_decreases(x: nat, m: nat) requires 0 < m, ensures #[trigger] (x % m) <= x,{ lemma_mod_auto(m as int);}
/// Proof that if `x % m` is zero and `x` is positive, then `x >= m`.pub broadcast proof fn lemma_mod_is_zero(x: nat, m: nat) requires x > 0 && m > 0, #[trigger] (x % m) == 0, ensures x >= m,{ if (x < m) { lemma_small_mod(x, m); }}
/// Proof that multiplying by a number then dividing by that same/// number produces a remainder of 0. Specifically, `(x * m) % m == 0`.#[verifier::spinoff_prover]pub broadcast proof fn lemma_mod_multiples_basic(x: int, m: int) requires m > 0, ensures #[trigger] ((x * m) % m) == 0,{ lemma_mod_auto(m); broadcast use group_mul_properties_internal;
let f = |u: int| (u * m) % m == 0; lemma_mul_induction(f); assert(f(x));}
/// Proof that adding the divisor to the dividend doesn't change the/// remainder. Specifically, `(m + b) % m == b % m`.pub broadcast proof fn lemma_mod_add_multiples_vanish(b: int, m: int) requires 0 < m, ensures (m + b) % m == #[trigger] (b % m),{ lemma_mod_auto(m);}
/// Proof that subtracting the divisor from the dividend doesn't/// change the remainder. Specifically, `(-m + b) % m == b % m`.pub broadcast proof fn lemma_mod_sub_multiples_vanish(b: int, m: int) requires 0 < m, ensures (-m + b) % m == #[trigger] (b % m),{ lemma_mod_auto(m);}
/// Proof that adding any multiple of the divisor to the dividend will produce the/// same remainder. In other words, `(m * a + b) % m == b % m`.#[verifier::spinoff_prover]pub broadcast proof fn lemma_mod_multiples_vanish(a: int, b: int, m: int) requires 0 < m, ensures #[trigger] ((m * a + b) % m) == b % m, decreases (if a > 0 { a } else { -a }),{ lemma_mod_auto(m); broadcast use group_mul_properties_internal;
let f = |u: int| (m * u + b) % m == b % m; lemma_mul_induction(f); assert(f(a));}
/// Proof that modulo distributes over subtraction if the subtracted value is/// less than or equal to the modulo of the number it's being subtracted from./// Specifically, because `0 <= s <= x % d`, we can conclude that/// `x % d - s % d == (x - s) % d`.pub broadcast proof fn lemma_mod_subtraction(x: nat, s: nat, d: nat) requires 0 < d, 0 <= s <= x % d, ensures #![trigger ((x - s) % d as int)] x % d - s % d == (x - s) % d as int,{ lemma_mod_auto(d as int);}
/// Proof that modulo distributes over addition, provided you do an/// extra modulo after adding the remainders. Specifically,/// `((x % m) + (y % m)) % m == (x + y) % m`.pub broadcast proof fn lemma_add_mod_noop(x: int, y: int, m: int) requires 0 < m, ensures #![trigger (x + y) % m] ((x % m) + (y % m)) % m == (x + y) % m,{ lemma_mod_auto(m);}
/// Proof that describes an expanded and succinct version of modulus/// operator in relation to addition. Specifically,/// `(x + (y % m)) % m == (x + y) % m`.pub broadcast proof fn lemma_add_mod_noop_right(x: int, y: int, m: int) requires 0 < m, ensures #![trigger (x + y) % m] (x + (y % m)) % m == (x + y) % m,{ lemma_mod_auto(m);}
/// Proof that modulo distributes over subtraction provided you do an/// extra modulo operation after subtracting the remainders./// Specifically, `((x % m) - (y % m)) % m == (x - y) % m`.pub broadcast proof fn lemma_sub_mod_noop(x: int, y: int, m: int) requires 0 < m, ensures #![trigger (x - y) % m] ((x % m) - (y % m)) % m == (x - y) % m,{ lemma_mod_auto(m);}
/// Proof that describes an expanded and succinct version of modulus/// operator in relation to subtraction. Specifically,/// `(x - (y % m)) % m == (x - y) % m`.pub broadcast proof fn lemma_sub_mod_noop_right(x: int, y: int, m: int) requires 0 < m, ensures #![trigger ((x - y) % m)] (x - (y % m)) % m == (x - y) % m,{ lemma_mod_auto(m);}
/// Proof of two properties of the sum of two remainders with the same dividend:/// 1) `a % d + b % d == (a + b) % d + d * ((a % d + b % d) / d)`./// 2) `(a % d + b % d) < d ==> a % d + b % d == (a + b) % d`.pub broadcast proof fn lemma_mod_adds(a: int, b: int, d: int) requires 0 < d, ensures #![trigger ((a + b) % d)] a % d + b % d == (a + b) % d + d * ((a % d + b % d) / d), (a % d + b % d) < d ==> a % d + b % d == (a + b) % d,{ broadcast use group_mul_properties_internal;
lemma_div_auto(d);}
/// Proof that the remainder when dividing integer `x` by positive/// integer `d` is equivalent to the remainder of `x * (1 - d)` by/// `d`.#[verifier::spinoff_prover]pub proof fn lemma_mod_neg_neg(x: int, d: int) requires 0 < d, ensures x % d == (x * (1 - d)) % d,{ broadcast use group_mul_properties_internal;
assert((x - x * d) % d == x % d) by { let f = |i: int| (x - i * d) % d == x % d; assert(f(0) && (forall|i: int| i >= 0 && #[trigger] f(i) ==> #[trigger] f(add1(i, 1))) && ( forall|i: int| i <= 0 && #[trigger] f(i) ==> #[trigger] f(sub1(i, 1)))) by { lemma_mod_auto(d); }; lemma_mul_induction(f); assert(f(x)); }
}
/// This proof isn't exported from this module. It's just used in/// the proof of [`lemma_fundamental_div_mod_converse`].proof fn lemma_fundamental_div_mod_converse_helper_1(u: int, d: int, r: int) requires d != 0, 0 <= r < d, ensures u == (u * d + r) / d, decreases if u >= 0 { u } else { -u },{ if u < 0 { lemma_fundamental_div_mod_converse_helper_1(u + 1, d, r); lemma_div_add_denominator(d, u * d + r); lemma_mul_is_distributive_add_other_way(d, u + 1, -1); assert(u == (u * d + r) / d); } else if u == 0 { DivINL::lemma_small_div(); assert(u == 0 ==> u * d == 0) by (nonlinear_arith); assert(u == (u * d + r) / d); } else { lemma_fundamental_div_mod_converse_helper_1(u - 1, d, r); lemma_div_add_denominator(d, (u - 1) * d + r); lemma_mul_is_distributive_add_other_way(d, u - 1, 1); assert(u * d + r == (u - 1) * d + r + d); assert(u == (u * d + r) / d); }}
/// This proof isn't exported from this module. It's just used in/// the proof of [`lemma_fundamental_div_mod_converse`].proof fn lemma_fundamental_div_mod_converse_helper_2(u: int, d: int, r: int) requires d != 0, 0 <= r < d, ensures r == (u * d + r) % d, decreases if u >= 0 { u } else { -u },{ if u < 0 { lemma_fundamental_div_mod_converse_helper_2(u + 1, d, r); lemma_mod_add_multiples_vanish(u * d + r, d); lemma_mul_is_distributive_add_other_way(d, u + 1, -1); assert(u * d == (u + 1) * d + (-1) * d); assert(u * d + r == (u + 1) * d + r - d); assert(r == (u * d + r) % d); } else if u == 0 { assert(u == 0 ==> u * d == 0) by (nonlinear_arith); if d > 0 { lemma_small_mod(r as nat, d as nat); } else { lemma_small_mod(r as nat, (-d) as nat); } assert(r == (u * d + r) % d); } else { lemma_fundamental_div_mod_converse_helper_2(u - 1, d, r); lemma_mod_add_multiples_vanish((u - 1) * d + r, d); lemma_mul_is_distributive_add_other_way(d, u - 1, 1); assert(u * d + r == (u - 1) * d + r + d); assert(r == (u * d + r) % d); }}
/// Proof of the converse of the fundamental property of division and modulo./// Specifically, if we know `0 <= r < d` and `x == q * d + r`, then we/// know that `r` is the remainder `x % d`.pub broadcast proof fn lemma_fundamental_div_mod_converse_mod(x: int, d: int, q: int, r: int) requires d != 0, 0 <= r < d, x == #[trigger] (q * d + r), ensures r == #[trigger] (x % d),{ lemma_fundamental_div_mod_converse_helper_1(q, d, r); assert(q == (q * d + r) / d); lemma_fundamental_div_mod_converse_helper_2(q, d, r);}
/// Proof of the converse of the fundamental property of division and modulo./// Specifically, if we know `0 <= r < d` and `x == q * d + r`, then we/// know that `q` is the quotient `x / d`.pub broadcast proof fn lemma_fundamental_div_mod_converse_div(x: int, d: int, q: int, r: int) requires d != 0, 0 <= r < d, x == #[trigger] (q * d + r), ensures q == #[trigger] (x / d),{ lemma_fundamental_div_mod_converse_helper_1(q, d, r); assert(q == (q * d + r) / d); lemma_fundamental_div_mod_converse_helper_2(q, d, r);}
/// Proof of the converse of the fundamental property of division and modulo./// Specifically, if we know `0 <= r < d` and `x == q * d + r`, then we/// know that `q` is the quotient `x / d` and `r` is the remainder `x % d`.pub proof fn lemma_fundamental_div_mod_converse(x: int, d: int, q: int, r: int) requires d != 0, 0 <= r < d, x == q * d + r, ensures r == x % d, q == x / d,{ lemma_fundamental_div_mod_converse_mod(x, d, q, r); lemma_fundamental_div_mod_converse_div(x, d, q, r);}
pub broadcast group group_fundamental_div_mod_converse { lemma_fundamental_div_mod_converse_mod, lemma_fundamental_div_mod_converse_div,}
/// Proof that the remainder, when natural number `x` is divided by/// positive integer `m`, is less than `m`.pub broadcast proof fn lemma_mod_pos_bound(x: int, m: int) requires 0 <= x, 0 < m, ensures 0 <= #[trigger] (x % m) < m,{ lemma_mod_auto(m);}
/// Proof that when integer `x` is divided by positive integer `m`,/// the remainder is nonegative and less than `m`.pub broadcast proof fn lemma_mod_bound(x: int, m: int) requires 0 < m, ensures 0 <= #[trigger] (x % m) < m,{ ModINL::lemma_mod_range(x, m);}
/// Proof that the remainder when `x * y` is divided by `m` is/// equivalent to the remainder when `(x % m) * y` is divided by `m`.pub broadcast proof fn lemma_mul_mod_noop_left(x: int, y: int, m: int) requires 0 < m, ensures (x % m) * y % m == #[trigger] (x * y % m),{ lemma_mod_auto(m); lemma_mul_induction_auto(y, |u: int| (x % m) * u % m == x * u % m);}
/// Proof that the remainder when `x * y` is divided by `m` is/// equivalent to the remainder when `x * (y % m)` is divided by `m`.pub broadcast proof fn lemma_mul_mod_noop_right(x: int, y: int, m: int) requires 0 < m, ensures x * (y % m) % m == #[trigger] ((x * y) % m),{ lemma_mod_auto(m); lemma_mul_induction_auto(x, |u: int| u * (y % m) % m == (u * y) % m);}
/// Proof of various properties about modulo equivalence with respect/// to multiplication, specifically various expressions that `(x * y)/// % m` is equivalent to.pub broadcast proof fn lemma_mul_mod_noop_general(x: int, y: int, m: int) requires 0 < m, ensures ((x % m) * y) % m == (x * y) % m, (x * (y % m)) % m == (x * y) % m, ((x % m) * (y % m)) % m == #[trigger] ((x * y) % m),{ lemma_mul_mod_noop_left(x, y, m); lemma_mul_mod_noop_right(x, y, m); lemma_mul_mod_noop_right(x % m, y, m);}
/// Proof that modulo distributes over multiplication, provided you do/// an extra modulo operation after multiplying the remainders. Specifically,/// `(x % m) * (y % m) % m == (x * y) % m`.pub broadcast proof fn lemma_mul_mod_noop(x: int, y: int, m: int) requires 0 < m, ensures (x % m) * (y % m) % m == #[trigger] ((x * y) % m),{ lemma_mul_mod_noop_general(x, y, m);}
/// Proof that `x` and `y` are congruent modulo `m` if and only if `x/// - y` is congruent to 0 modulo `m`. In other words, `x % m == y % m/// <==> (x - y) % m == 0`.////// Note: The Dafny standard library uses the triggers `x % m, y % m`/// for the broadcasted forall quantifier. But this can lead to a trigger loop,/// so we don't do that here.pub broadcast proof fn lemma_mod_equivalence(x: int, y: int, m: int) requires 0 < m, ensures #![trigger (x - y) % m] x % m == y % m <==> (x - y) % m == 0,{ lemma_mod_auto(m);}
/// This function says that `x` is congruent to `y` modulo `m` if and/// only if their difference `x - y` is congruent to 0 modulo `m`.pub open spec fn is_mod_equivalent(x: int, y: int, m: int) -> bool recommends m > 0,{ x % m == y % m <==> (x - y) % m == 0}
/// Proof that if `is_mod_equivalent` holds for `x`, `y`, and `m`,/// then it holds for `x * z`, `y * z`, and `m`.pub broadcast proof fn lemma_mod_mul_equivalent(x: int, y: int, z: int, m: int) requires m > 0, is_mod_equivalent(x, y, m), ensures #[trigger] is_mod_equivalent(x * z, y * z, m),{ lemma_mul_mod_noop_left(x, z, m); lemma_mul_mod_noop_left(y, z, m); lemma_mod_equivalence(x, y, m); lemma_mod_equivalence(x * z, y * z, m);}
/// Proof that multiplying the divisor by a positive number can't/// decrease the remainder. Specifically, because `k > 0`, we have/// `x % d <= x % (d * k)`.pub broadcast proof fn lemma_mod_ordering(x: int, k: int, d: int) requires 1 < d, 0 < k, ensures 0 < d * k, x % d <= #[trigger] (x % (d * k)),{ lemma_mul_strictly_increases(d, k); calc! { (==) x % d + d * (x / d); { lemma_fundamental_div_mod(x, d); } x; { lemma_fundamental_div_mod(x, d * k); } x % (d * k) + (d * k) * (x / (d * k)); { broadcast use lemma_mul_is_associative;
} x % (d * k) + d * (k * (x / (d * k))); } calc! { (==) x % d; { broadcast use group_mod_properties;
} (x % d) % d; { lemma_mod_multiples_vanish(x / d - k * (x / (d * k)), x % d, d); } (x % d + d * (x / d - k * (x / (d * k)))) % d; { broadcast use lemma_mul_is_distributive_sub;
} (x % d + d * (x / d) - d * (k * (x / (d * k)))) % d; {} (x % (d * k)) % d; } assert((x % (d * k)) % d <= x % (d * k)) by { broadcast use group_mod_properties;
lemma_mod_decreases((x % (d * k)) as nat, d as nat); };}
/// Proof that the remainder when `x` is divided by `a * b`, taken/// modulo `a`, is equivalent to `x` modulo `a`. That is,/// `(x % (a * b)) % a == x % a`.pub broadcast proof fn lemma_mod_mod(x: int, a: int, b: int) requires 0 < a, 0 < b, ensures #![trigger (x % (a * b)) % a, x % a] 0 < a * b, (x % (a * b)) % a == x % a,{ broadcast use lemma_mul_strictly_positive;
calc! { (==) x; { lemma_fundamental_div_mod(x, a * b); } (a * b) * (x / (a * b)) + x % (a * b); { broadcast use lemma_mul_is_associative;
} a * (b * (x / (a * b))) + x % (a * b); { lemma_fundamental_div_mod(x % (a * b), a); } a * (b * (x / (a * b))) + a * (x % (a * b) / a) + (x % (a * b)) % a; { broadcast use group_mul_is_distributive;
} a * (b * (x / (a * b)) + x % (a * b) / a) + (x % (a * b)) % a; } broadcast use {group_mod_properties, lemma_mul_is_commutative};
lemma_fundamental_div_mod_converse( x, a, b * (x / (a * b)) + x % (a * b) / a, (x % (a * b)) % a, );}
/// Proof that `(x % y) % (y * z) < y`.pub broadcast proof fn lemma_part_bound2(x: int, y: int, z: int) requires 0 <= x, 0 < y, 0 < z, ensures y * z > 0, #[trigger] (x % y) % #[trigger] (y * z) < y,{ broadcast use { lemma_mul_strictly_positive, group_mod_properties, lemma_mul_is_commutative, lemma_mul_increases, };
assert(x % y < y); assert(y <= y * z); assert(0 <= x % y < y * z); lemma_small_mod((x % y) as nat, (y * z) as nat); assert((x % y) % (y * z) == x % y);}
/// Proof of the validity of an expanded form of the modulus operation./// Specifically, `x % (y * z) == y * ((x / y) % z) + x % y`.pub broadcast proof fn lemma_mod_breakdown(x: int, y: int, z: int) requires 0 <= x, 0 < y, 0 < z, ensures #![trigger x % (y * z)] y * z > 0, x % (y * z) == y * ((x / y) % z) + x % y,{ broadcast use lemma_mul_strictly_positive;
lemma_div_pos_is_pos(x, y); assert(0 <= x / y); assert((y * (x / y)) % (y * z) + (x % y) % (y * z) < y * z) by { lemma_part_bound1(x, y, z); lemma_part_bound2(x, y, z); broadcast use {group_mul_basics, group_mul_is_distributive};
}; calc! { (==) x % (y * z); { lemma_fundamental_div_mod(x, y); } (y * (x / y) + x % y) % (y * z); { broadcast use group_mod_properties;
assert(0 <= x % y); lemma_mul_nonnegative(y, x / y); assert((y * (x / y)) % (y * z) + (x % y) % (y * z) < y * z); lemma_mod_adds(y * (x / y), x % y, y * z); } (y * (x / y)) % (y * z) + (x % y) % (y * z); { broadcast use {group_mod_properties, lemma_mul_is_commutative};
lemma_mul_increases(z, y); assert(x % y < y && y <= y * z); lemma_small_mod((x % y) as nat, (y * z) as nat); assert((x % y) % (y * z) == x % y); } (y * (x / y)) % (y * z) + x % y; { lemma_truncate_middle(x / y, y, z); } y * ((x / y) % z) + x % y; }}
} // verus!