vstd/
endian.rs

1/*!
2Reasoning about representations of non-negative numbers with endianness, including conversion between bases.
3*/
4use crate::vstd::arithmetic::div_mod::*;
5use crate::vstd::arithmetic::mul::*;
6use crate::vstd::arithmetic::power::*;
7use crate::vstd::arithmetic::power2::*;
8use crate::vstd::calc_macro::*;
9use crate::vstd::group_vstd_default;
10use crate::vstd::layout;
11use crate::vstd::prelude::*;
12use core::marker::PhantomData;
13
14verus! {
15
16broadcast use group_vstd_default;
17
18/// Represents a base with value [`Self::base()`].
19pub trait Base {
20    spec fn base() -> nat;
21
22    proof fn base_min()
23        ensures
24            Self::base() > 1,
25    ;
26}
27
28/// The exclusive upper bound on values that can be stored with `len` digits in base [`B::base()`].
29///
30/// [`B::base()`]: Base::base
31pub open spec fn base_upper_bound_excl<B: Base>(len: nat) -> int {
32    pow(B::base() as int, len)
33}
34
35/// Represents a base which is a power of 2 specified by [`Self::bits()`].
36pub trait BasePow2: Base {
37    spec fn bits() -> nat;
38
39    proof fn bits_to_base()
40        ensures
41            Self::bits() > 1,
42            Self::base() == pow2(Self::bits()),
43    ;
44}
45
46/// Represents a base for which each digit of `BIG` converts to multiple digits in this base.
47pub trait CompatibleSmallerBaseFor<BIG: BasePow2>: BasePow2 {
48    proof fn compatible()
49        ensures
50            BIG::bits() > Self::bits() && BIG::bits() % Self::bits() == 0,
51    ;
52}
53
54/// Represents little-endian or big-endian interpretation.
55pub enum Endian {
56    Little,
57    Big,
58}
59
60/// Abstracts the endianness of the currently executing hardware.
61/// Use this when you want to use the same endianness everywhere, but don't wish to specify which endianness is used.
62pub uninterp spec fn endianness() -> Endian;
63
64/// Provides either little-endian or big-endian interpretation of a sequence of numbers with a given base. This interpretation may have any number of leading zeros.
65/// With little-endian, the first digit is the least significant position; the last digit is the most significant position.
66/// With big-endian, the last digit of a sequence is the least significant position; the first digit is the most significant position.
67#[verifier::ext_equal]
68pub struct EndianNat<B: Base> {
69    pub endian: Endian,
70    pub digits: Seq<int>,
71    pub phantom: core::marker::PhantomData<B>,
72}
73
74impl<B: Base> EndianNat<B> {
75    /// True when all numbers in `s` are valid digits in the given base.
76    pub open spec fn in_bounds(s: Seq<int>) -> bool {
77        forall|i| 0 <= i < s.len() ==> 0 <= #[trigger] s[i] < B::base()
78    }
79
80    /// True when all of `self.digits` are valid digits in the given base.
81    pub open spec fn wf(self) -> bool {
82        Self::in_bounds(self.digits)
83    }
84
85    /// Creates a new `EndianNat` with the given digits and endianness.
86    pub open spec fn new(endian: Endian, digits: Seq<int>) -> Self
87        recommends
88            Self::in_bounds(digits),
89    {
90        EndianNat { endian, digits, phantom: PhantomData }
91    }
92
93    /// Creates a new `EndianNat` with the given digits and the default endianness ([`endianness()`]).
94    pub open spec fn new_default(digits: Seq<int>) -> Self
95        recommends
96            Self::in_bounds(digits),
97    {
98        EndianNat { endian: endianness(), digits, phantom: PhantomData }
99    }
100
101    /// Number of digits in this `EndianNat`.
102    pub open spec fn len(self) -> nat {
103        self.digits.len()
104    }
105
106    /// The `i`th digit in this `EndianNat`.
107    pub open spec fn index(self, i: int) -> int
108        recommends
109            0 <= i < self.digits.len(),
110    {
111        self.digits[i]
112    }
113
114    /// The first digit in this `EndianNat`. Ignores endianness.
115    pub open spec fn first(self) -> nat
116        recommends
117            self.digits.len() > 0,
118    {
119        self.digits.first() as nat
120    }
121
122    /// The last digit in this `EndianNat`. Ignores endianness.
123    pub open spec fn last(self) -> nat
124        recommends
125            self.digits.len() > 0,
126    {
127        self.digits.last() as nat
128    }
129
130    /// The least significant digit in this `EndianNat`.
131    pub open spec fn least(self) -> nat
132        recommends
133            self.digits.len() > 0,
134    {
135        match self.endian {
136            Endian::Little => self.first(),
137            Endian::Big => self.last(),
138        }
139    }
140
141    /// The most significant digit in this `EndianNat`.
142    pub open spec fn most(self) -> nat
143        recommends
144            self.digits.len() > 0,
145    {
146        match self.endian {
147            Endian::Little => self.last(),
148            Endian::Big => self.first(),
149        }
150    }
151
152    /// Constructs an `EndianNat` by skipping the first `n` digits of the original `EndianNat`. Ignores endianness.
153    pub open spec fn skip(self, n: nat) -> Self
154        recommends
155            0 <= n <= self.digits.len(),
156    {
157        EndianNat { endian: self.endian, digits: self.digits.skip(n as int), phantom: self.phantom }
158    }
159
160    /// Constructs an `EndianNat` by taking only the first `n` digits of the original `EndianNat`. Ignores endianness.
161    pub open spec fn take(self, n: nat) -> Self
162        recommends
163            0 <= n <= self.digits.len(),
164    {
165        EndianNat { endian: self.endian, digits: self.digits.take(n as int), phantom: self.phantom }
166    }
167
168    /// Constructs an `EndianNat` by skipping the least significant `n` digits of the original `EndianNat`.
169    pub open spec fn skip_least(self, n: nat) -> Self
170        recommends
171            0 <= n <= self.digits.len(),
172    {
173        match self.endian {
174            Endian::Little => self.skip(n),
175            Endian::Big => self.take((self.len() - n) as nat),
176        }
177    }
178
179    /// Constructs an `EndianNat` by skipping the most significant `n` digits of the original `EndianNat`.
180    pub open spec fn skip_most(self, n: nat) -> Self
181        recommends
182            0 <= n <= self.digits.len(),
183    {
184        match self.endian {
185            Endian::Little => self.take((self.len() - n) as nat),
186            Endian::Big => self.skip(n),
187        }
188    }
189
190    /// Constructs an `EndianNat` by taking only the least significant `n` digits of the original `EndianNat`.
191    pub open spec fn take_least(self, n: nat) -> Self
192        recommends
193            0 <= n <= self.digits.len(),
194    {
195        match self.endian {
196            Endian::Little => self.take(n),
197            Endian::Big => self.skip((self.len() - n) as nat),
198        }
199    }
200
201    /// Constructs an `EndianNat` by taking only the most significant `n` digits of the original `EndianNat`.
202    pub open spec fn take_most(self, n: nat) -> Self
203        recommends
204            0 <= n <= self.digits.len(),
205    {
206        match self.endian {
207            Endian::Little => self.skip((self.len() - n) as nat),
208            Endian::Big => self.take(n),
209        }
210    }
211
212    /// Constructs an `EndianNat` by dropping the first digit of the original `EndianNat`. Ignores endianness.
213    pub open spec fn drop_first(self) -> Self
214        recommends
215            self.len() > 0,
216    {
217        EndianNat { endian: self.endian, digits: self.digits.drop_first(), phantom: self.phantom }
218    }
219
220    /// Constructs an `EndianNat` by dropping the last digit of the original `EndianNat`. Ignores endianness.
221    pub open spec fn drop_last(self) -> Self
222        recommends
223            self.len() > 0,
224    {
225        EndianNat { endian: self.endian, digits: self.digits.drop_last(), phantom: self.phantom }
226    }
227
228    /// Constructs an `EndianNat` by dropping the least significant digit of the original `EndianNat`.
229    pub open spec fn drop_least(self) -> Self
230        recommends
231            self.len() > 0,
232    {
233        match self.endian {
234            Endian::Little => self.drop_first(),
235            Endian::Big => self.drop_last(),
236        }
237    }
238
239    /// Constructs an `EndianNat` by dropping the most significant digits of the original `EndianNat`.
240    pub open spec fn drop_most(self) -> Self
241        recommends
242            self.len() > 0,
243    {
244        match self.endian {
245            Endian::Little => self.drop_last(),
246            Endian::Big => self.drop_first(),
247        }
248    }
249
250    /// Constructs an `EndianNat` by appending the digits of `other` to the end of the digits of `self`. Ignores endianness.
251    pub open spec fn append(self, other: Self) -> Self
252        recommends
253            self.endian == other.endian,
254    {
255        EndianNat::new(self.endian, self.digits + other.digits)
256    }
257
258    /// Constructs an `EndianNat` by appending the digits of `other` to the digits of `self` in the least significant position
259    /// (i.e., `other` becomes the least significant bits).
260    pub open spec fn append_least(self, other: Self) -> Self
261        recommends
262            self.endian == other.endian,
263    {
264        match self.endian {
265            Endian::Little => other.append(self),
266            Endian::Big => self.append(other),
267        }
268    }
269
270    /// Constructs an `EndianNat` by appending the digits of `other` to the digits of `self` in the most significant position
271    /// (i.e., `other` becomes the most significant bits).
272    pub open spec fn append_most(self, other: Self) -> Self
273        recommends
274            self.endian == other.endian,
275    {
276        match self.endian {
277            Endian::Little => self.append(other),
278            Endian::Big => other.append(self),
279        }
280    }
281
282    /// Constructs an `EndianNat` by appending `n` to the front of the digits of `self`. Ignores endianness.
283    pub open spec fn push_first(self, n: int) -> Self
284        recommends
285            n < B::base(),
286    {
287        EndianNat { endian: self.endian, digits: seq![n].add(self.digits), phantom: self.phantom }
288    }
289
290    /// Constructs an `EndianNat` by appending `n` to the end of the digits of `self`. Ignores endianness.
291    pub open spec fn push_last(self, n: int) -> Self
292        recommends
293            n < B::base(),
294    {
295        EndianNat { endian: self.endian, digits: self.digits.push(n), phantom: self.phantom }
296    }
297
298    /// Constructs an `EndianNat` by appending `n` to the least significant position in the digits of `self`.
299    pub open spec fn push_least(self, n: int) -> Self
300        recommends
301            n < B::base(),
302    {
303        match self.endian {
304            Endian::Little => self.push_first(n),
305            Endian::Big => self.push_last(n),
306        }
307    }
308
309    /// Constructs an `EndianNat` by appending `n` to the most significant position in the digits of `self`.
310    pub open spec fn push_most(self, n: int) -> Self
311        recommends
312            n < B::base(),
313    {
314        match self.endian {
315            Endian::Little => self.push_last(n),
316            Endian::Big => self.push_first(n),
317        }
318    }
319
320    /// Converts an `EndianNat` to the natural number that it represents, processing the digits from least significant to most significant, hiding the details of endianness.
321    #[verifier::opaque]
322    pub open spec fn to_nat(self) -> nat
323        decreases self.len(),
324    {
325        if self.len() == 0 {
326            0
327        } else {
328            self.drop_least().to_nat() * B::base() + self.least()
329        }
330    }
331
332    pub broadcast proof fn to_nat_properties(self)
333        requires
334            self.wf(),
335        ensures
336            #[trigger] self.to_nat() < base_upper_bound_excl::<B>(self.len()),
337        decreases self.len(),
338    {
339        reveal(EndianNat::to_nat);
340        reveal(pow);
341        if self.len() == 0 {
342        } else {
343            self.drop_least().to_nat_properties();
344
345            calc! {
346                (<)
347                self.to_nat(); (==) {}
348                self.drop_least().to_nat() * B::base() + self.least(); (<) {}
349                self.drop_least().to_nat() * B::base() + B::base(); (<=) {
350                    broadcast use lemma_mul_inequality, lemma_mul_is_distributive_sub_other_way;
351
352                    assert((base_upper_bound_excl::<B>((self.len() - 1) as nat) - 1)
353                        * B::base() as nat == (base_upper_bound_excl::<B>((self.len() - 1) as nat)
354                        * B::base() - B::base()) as nat);
355                }
356                (base_upper_bound_excl::<B>((self.len() - 1) as nat) * B::base() - B::base()
357                    + B::base()) as nat; (==) {
358                    broadcast use lemma_pow1;
359
360                }
361                (base_upper_bound_excl::<B>((self.len() - 1) as nat) * pow(
362                    B::base() as int,
363                    1,
364                )) as nat; (==) {
365                    broadcast use lemma_pow_sub_add_cancel;
366
367                }
368                base_upper_bound_excl::<B>(self.len()) as nat;
369            }
370        }
371    }
372
373    pub proof fn to_nat_append_least(endian: Self, other: Self)
374        requires
375            endian.wf(),
376            other.wf(),
377            endian.endian == other.endian,
378        ensures
379            endian.append_least(other).to_nat() == (endian.to_nat() * base_upper_bound_excl::<B>(
380                other.len(),
381            )) + other.to_nat(),
382        decreases other.len(),
383    {
384        reveal(EndianNat::to_nat);
385        reveal(pow);
386        if other.len() == 0 {
387        } else {
388            let least = other.least();
389            let rest = other.drop_least();
390            Self::to_nat_append_least(endian, rest);
391            assert(endian.append_least(other).drop_least() =~= endian.append_least(rest));
392            assert(endian.to_nat() * base_upper_bound_excl::<B>(rest.len()) * B::base()
393                == endian.to_nat() * base_upper_bound_excl::<B>(rest.len() + 1)) by {
394                broadcast use lemma_pow1;
395
396                assert(B::base() == pow(B::base() as int, 1));
397                broadcast use lemma_pow_adds;
398
399                assert(pow(B::base() as int, rest.len() + 1) == pow(B::base() as int, rest.len())
400                    * pow(B::base() as int, 1));
401                assert(endian.to_nat() * base_upper_bound_excl::<B>(rest.len()) * B::base()
402                    == endian.to_nat() * base_upper_bound_excl::<B>(rest.len() + 1))
403                    by (nonlinear_arith)
404                    requires
405                        base_upper_bound_excl::<B>(rest.len()) * B::base()
406                            == base_upper_bound_excl::<B>(rest.len() + 1),
407                ;
408            }
409            assert(endian.append_least(other).to_nat() == (endian.to_nat()
410                * base_upper_bound_excl::<B>(other.len())) + other.to_nat()) by (nonlinear_arith)
411                requires
412                    endian.append_least(other).to_nat() == endian.append_least(rest).to_nat()
413                        * B::base() + least,
414                    other.to_nat() == rest.to_nat() * B::base() + least,
415                    endian.append_least(rest).to_nat() == (endian.to_nat()
416                        * base_upper_bound_excl::<B>(rest.len())) + rest.to_nat(),
417                    endian.to_nat() * base_upper_bound_excl::<B>(rest.len()) * B::base()
418                        == endian.to_nat() * base_upper_bound_excl::<B>(rest.len() + 1),
419                    other.len() == rest.len() + 1,
420            ;
421        }
422    }
423
424    /// Converts a natural number to an `EndianNat` representation with the specified number of digits (`len`) and default endianness ([`endianness()`]).
425    /// `n` should be less than the maximum number that can be represented in `len` digits in this base.
426    pub open spec fn from_nat(n: nat, len: nat) -> Self
427        recommends
428            n < base_upper_bound_excl::<B>(len),
429        decreases len,
430    {
431        if len == 0 {
432            EndianNat { digits: Seq::empty(), endian: endianness(), phantom: PhantomData }
433        } else {
434            let least = (n % B::base()) as int;
435            let rest = n / B::base();
436            let rest_endian = Self::from_nat(rest, (len - 1) as nat);
437            rest_endian.push_least(least)
438        }
439    }
440
441    proof fn base_upper_bound_excl_len(n: nat, len: nat)
442        requires
443            n < base_upper_bound_excl::<B>(len),
444            0 < len,
445        ensures
446            n / B::base() < base_upper_bound_excl::<B>((len - 1) as nat),
447    {
448        reveal(pow);
449        assert(n / B::base() < base_upper_bound_excl::<B>((len - 1) as nat)) by (nonlinear_arith)
450            requires
451                n < B::base() * base_upper_bound_excl::<B>((len - 1) as nat),
452                B::base() > 0,
453        ;
454    }
455
456    pub broadcast proof fn from_nat_properties(n: nat, len: nat)
457        requires
458            n < base_upper_bound_excl::<B>(len),
459        ensures
460            #![trigger Self::from_nat(n, len)]
461            Self::from_nat(n, len).len() == len,
462            Self::from_nat(n, len).endian == endianness(),
463            Self::from_nat(n, len).wf(),
464        decreases len,
465    {
466        if len == 0 {
467        } else {
468            Self::base_upper_bound_excl_len(n, len);
469            let endian_nat = Self::from_nat(n, len);
470            let least = endian_nat.least();
471            Self::from_nat_properties(n / B::base(), (len - 1) as nat);
472            B::base_min();
473            assert(least < B::base()) by (nonlinear_arith)
474                requires
475                    B::base() > 0,
476                    least == (n % B::base()),
477            ;
478        }
479    }
480
481    /// Ensures that performing [`from_nat`] and then [`to_nat`] results in the original value,
482    /// provided that the value can be encoded in the given base in the given number of digits.
483    ///
484    /// [`from_nat`]: EndianNat::from_nat
485    /// [`to_nat`]: EndianNat::to_nat
486    pub broadcast proof fn from_nat_to_nat(n: nat, len: nat)
487        requires
488            n < base_upper_bound_excl::<B>(len),
489        ensures
490            #[trigger] Self::from_nat(n, len).to_nat() == n,
491        decreases Self::from_nat(n, len).len(),
492    {
493        reveal(pow);
494        reveal(EndianNat::to_nat);
495        if Self::from_nat(n, len).len() == 0 {
496        } else {
497            B::base_min();
498            let endian_nat = Self::from_nat(n, len);
499            let least = endian_nat.least();
500            let rest = endian_nat.drop_least();
501            assert(rest =~= Self::from_nat(n / B::base(), (len - 1) as nat));
502            Self::base_upper_bound_excl_len(n, len);
503            Self::from_nat_to_nat(n / B::base(), (len - 1) as nat);
504            assert((n % B::base()) + (n / B::base()) * B::base() == n) by (nonlinear_arith)
505                requires
506                    B::base() > 0,
507            ;
508        }
509    }
510
511    /// Ensures that performing [`to_nat`] and then [`from_nat`] results in the original `EndianNat`.
512    ///
513    /// [`from_nat`]: EndianNat::from_nat
514    /// [`to_nat`]: EndianNat::to_nat
515    pub broadcast proof fn to_nat_from_nat(endian_nat: Self)
516        requires
517            endian_nat.wf(),
518            endian_nat.endian == endianness(),
519        ensures
520            #[trigger] Self::from_nat(endian_nat.to_nat(), endian_nat.len()) == endian_nat,
521        decreases endian_nat.len(),
522    {
523        reveal(pow);
524        reveal(EndianNat::to_nat);
525        if endian_nat.len() == 0 {
526        } else {
527            let n = endian_nat.to_nat();
528            let least = endian_nat.least();
529            let rest = endian_nat.drop_least();
530            Self::to_nat_from_nat(rest);
531            assert(least == n % B::base() && rest.to_nat() == n / B::base()) by {
532                assert(n == rest.to_nat() * B::base() + least);
533                assert(least < B::base());
534                lemma_fundamental_div_mod_converse(
535                    n as int,
536                    B::base() as int,
537                    rest.to_nat() as int,
538                    least as int,
539                );
540            }
541        }
542    }
543
544    pub broadcast proof fn to_nat_injective(n1: Self, n2: Self)
545        requires
546            n1.wf(),
547            n2.wf(),
548            n1.endian == endianness(),
549            n2.endian == endianness(),
550            n1.len() == n2.len(),
551            #[trigger] n1.to_nat() == #[trigger] n2.to_nat(),
552        ensures
553            n1 == n2,
554    {
555        broadcast use EndianNat::to_nat_from_nat;
556
557        assert(Self::from_nat(n1.to_nat(), n1.len()) == n1);
558        assert(Self::from_nat(n2.to_nat(), n2.len()) == n2);
559    }
560
561    pub broadcast proof fn from_nat_injective(n1: nat, len1: nat, n2: nat, len2: nat)
562        requires
563            n1 < base_upper_bound_excl::<B>(len1),
564            n2 < base_upper_bound_excl::<B>(len2),
565            #[trigger] Self::from_nat(n1, len1) == #[trigger] Self::from_nat(n2, len2),
566        ensures
567            n1 == n2,
568    {
569        broadcast use EndianNat::from_nat_to_nat;
570
571        assert(Self::from_nat(n1, len1).to_nat() == n1);
572        assert(Self::from_nat(n2, len2).to_nat() == n2);
573    }
574
575    /// Converts an `EndianNat` to the natural number that it represents, processing the digits from most significant to least significant, hiding the details of endianness.
576    #[verifier::opaque]
577    pub open spec fn to_nat_most(self) -> nat
578        decreases self.len(),
579    {
580        if self.len() == 0 {
581            0
582        } else {
583            (self.drop_most().to_nat_most() + self.most() * pow(
584                B::base() as int,
585                (self.len() - 1) as nat,
586            )) as nat
587        }
588    }
589
590    /// Ensures that [`to_nat`] and [`to_nat_most`] agree.
591    ///
592    /// [`to_nat`]: EndianNat::to_nat
593    /// [`to_nat_most`]: EndianNat::to_nat_most
594    pub broadcast proof fn to_nat_eq_to_nat_most(self)
595        requires
596            self.wf(),
597        ensures
598            #[trigger] self.to_nat() == #[trigger] self.to_nat_most(),
599        decreases self.len(),
600    {
601        reveal(EndianNat::to_nat);
602        reveal(EndianNat::to_nat_most);
603        if self.len() == 0 {
604        } else {
605            if self.drop_most().len() == 0 {
606                calc! {
607                    (==)
608                    self.to_nat_most(); {
609                        assert(self.drop_most().to_nat_most() == 0);
610                        assert(self.to_nat_most() == (self.most() * pow(
611                            B::base() as int,
612                            (self.len() - 1) as nat,
613                        )) as nat);
614                    }
615                    (self.most() * pow(B::base() as int, (self.len() - 1) as nat)) as nat; {
616                        reveal(pow);
617                        assert((self.most() * pow(B::base() as int, (self.len() - 1) as nat))
618                            == self.most()) by (nonlinear_arith)
619                            requires
620                                pow(B::base() as int, (self.len() - 1) as nat) == 1,
621                                self.most() >= 0,
622                        ;
623                    }
624                    self.most(); {}
625                    self.least(); {
626                        assert(self.drop_least().to_nat() == 0);
627                        assert(0 * B::base() == 0);
628                    }
629                    self.to_nat();
630                };
631            } else {
632                calc! {
633                    (==)
634                    self.to_nat_most() as int; {}
635                    ((self.drop_most().to_nat_most() + self.most() * pow(
636                        B::base() as int,
637                        (self.len() - 1) as nat,
638                    )) as nat) as int; {
639                        assert(self.most() >= 0);
640                        assert(self.len() > 1);
641                        lemma_pow_positive(B::base() as int, (self.len() - 1) as nat);
642                        assert(pow(B::base() as int, (self.len() - 1) as nat) >= 0);
643                    }
644                    self.drop_most().to_nat_most() + self.most() * pow(
645                        B::base() as int,
646                        (self.len() - 1) as nat,
647                    ); {
648                        self.drop_most().to_nat_eq_to_nat_most();
649                    }
650                    self.drop_most().to_nat() + self.most() * pow(
651                        B::base() as int,
652                        (self.len() - 1) as nat,
653                    ); {}
654                    self.drop_most().drop_least().to_nat() * B::base() + self.drop_most().least()
655                        + self.most() * pow(B::base() as int, (self.len() - 1) as nat); {
656                        self.drop_most().drop_least().to_nat_eq_to_nat_most();
657                    }
658                    self.drop_most().drop_least().to_nat_most() * B::base()
659                        + self.drop_most().least() + self.most() * pow(
660                        B::base() as int,
661                        (self.len() - 1) as nat,
662                    ); {
663                        assert(self.drop_most().drop_least() == self.drop_least().drop_most());
664                    }
665                    self.drop_least().drop_most().to_nat_most() * B::base() + self.least()
666                        + self.most() * pow(B::base() as int, (self.len() - 1) as nat); {
667                        assert(self.most() * pow(B::base() as int, (self.len() - 2) as nat)
668                            * B::base() == self.most() * (pow(
669                            B::base() as int,
670                            (self.len() - 2) as nat,
671                        ) * B::base())) by {
672                            broadcast use crate::vstd::arithmetic::mul::lemma_mul_is_associative;
673
674                        }
675                        assert(pow(B::base() as int, (self.len() - 1) as nat) == pow(
676                            B::base() as int,
677                            (self.len() - 2) as nat,
678                        ) * B::base()) by {
679                            assert(B::base() == pow(B::base() as int, 1)) by {
680                                lemma_pow1(B::base() as int);
681                            }
682                            lemma_pow_adds(B::base() as int, (self.len() - 2) as nat, 1);
683                        }
684                    }
685                    self.drop_least().drop_most().to_nat_most() * B::base() + (self.most() * pow(
686                        B::base() as int,
687                        (self.len() - 2) as nat,
688                    )) * B::base() + self.least(); {
689                        lemma_mul_is_distributive_add_other_way(
690                            B::base() as int,
691                            self.drop_least().drop_most().to_nat_most() as int,
692                            self.most() * pow(B::base() as int, (self.len() - 2) as nat),
693                        );
694                    }
695                    (self.drop_least().drop_most().to_nat_most() + self.most() * pow(
696                        B::base() as int,
697                        (self.len() - 2) as nat,
698                    )) * B::base() + self.least(); {
699                        assert((self.drop_least().drop_most().to_nat_most() + self.most() * pow(
700                            B::base() as int,
701                            (self.len() - 2) as nat,
702                        )) == self.drop_least().to_nat_most()) by {
703                            lemma_pow_positive(B::base() as int, (self.len() - 2) as nat);
704                        };
705                    }
706                    (self.drop_least().to_nat_most() * B::base() + self.least()) as int; {
707                        self.drop_least().to_nat_eq_to_nat_most();
708                    }
709                    self.to_nat() as int;
710                }
711            }
712        }
713    }
714}
715
716// /////////////////////////////////////////////////// //
717//         Conversion Routines                         //
718// /////////////////////////////////////////////////// //
719impl<B: Base> EndianNat<B> {
720    /// [`B::base()`] to the power of `exp()` is [`BIG::base()`].
721    /// In other words, `exp()` is the number of digits in base `B` that correspond to a single digit in base `BIG`.
722    ///
723    /// [`B::base()`]: Base::base
724    /// [`BIG::base()`]: Base::base
725    pub open spec fn exp<BIG>() -> nat where BIG: BasePow2, B: CompatibleSmallerBaseFor<BIG> {
726        BIG::bits() / B::bits()
727    }
728
729    pub broadcast proof fn exp_properties<BIG>() where
730        BIG: BasePow2,
731        B: CompatibleSmallerBaseFor<BIG>,
732
733        ensures
734            #![trigger Self::exp()]
735            base_upper_bound_excl::<B>(Self::exp()) == BIG::base(),
736            Self::exp() > 0,
737    {
738        broadcast use crate::vstd::arithmetic::div_mod::group_div_basics;
739
740        assert(forall|x| x != 0 ==> #[trigger] (0int / x) == 0);
741        broadcast use crate::vstd::arithmetic::power::lemma_pow_multiplies;
742
743        B::bits_to_base();
744
745        calc! {
746            (==)
747            BIG::bits(); {
748                crate::vstd::arithmetic::div_mod::lemma_fundamental_div_mod(
749                    BIG::bits() as int,
750                    B::bits() as int,
751                );
752            }
753            B::bits() * (BIG::bits() / B::bits()) + (BIG::bits() % B::bits()); {
754                B::compatible();
755            }
756            B::bits() * (BIG::bits() / B::bits()); {}
757            B::bits() * Self::exp();
758        }
759        calc! {
760            (==)
761            base_upper_bound_excl::<B>(Self::exp()); {
762                crate::vstd::arithmetic::power::lemma_pow_multiplies(2, B::bits(), Self::exp());
763                crate::vstd::arithmetic::power2::lemma_pow2(B::bits());
764            }
765            pow(2, B::bits() * Self::exp()) as int; {}
766            pow(2, BIG::bits()) as int; {
767                crate::vstd::arithmetic::power2::lemma_pow2(BIG::bits());
768            }
769            pow2(BIG::bits()) as int; {
770                BIG::bits_to_base();
771            }
772            BIG::base() as int;
773        }
774
775        B::compatible();
776        assert((BIG::bits() / B::bits()) != 0);
777        BIG::bits_to_base();
778
779    }
780
781    /// Converts an `EndianNat` representation in the "big" base `BIG` to an `EndianNat` representation in the "small" base `B`.
782    /// The result represents the same non-negative number as the original.
783    pub open spec fn from_big<BIG>(n: EndianNat<BIG>) -> Self where
784        BIG: BasePow2,
785        B: CompatibleSmallerBaseFor<BIG>,
786
787        decreases n.len(),
788    {
789        if n.len() == 0 {
790            EndianNat::new(n.endian, Seq::empty())
791        } else {
792            Self::from_big(n.drop_least()).append_least(EndianNat::from_nat(n.least(), Self::exp()))
793        }
794    }
795
796    pub broadcast proof fn from_big_properties<BIG>(n: EndianNat<BIG>) where
797        BIG: BasePow2,
798        B: CompatibleSmallerBaseFor<BIG>,
799
800        requires
801            n.wf(),
802            n.endian == endianness(),
803        ensures
804            #![trigger Self::from_big(n)]
805            Self::from_big(n).wf(),
806            Self::from_big(n).endian == endianness(),
807            Self::from_big(n).len() == n.len() * Self::exp(),
808            Self::from_big(n).to_nat() == n.to_nat(),
809        decreases n.len(),
810    {
811        reveal(EndianNat::to_nat);
812        broadcast use EndianNat::exp_properties;
813
814        if n.len() == 0 {
815        } else {
816            let least = n.least();
817            let rest = n.drop_least();
818            Self::from_big_properties(rest);
819            Self::from_nat_properties(least, Self::exp());
820            assert(Self::from_big(n).len() == n.len() * Self::exp()) by (nonlinear_arith)
821                requires
822                    Self::from_big(n).len() == (n.len() - 1) * Self::exp() + Self::exp(),
823            ;
824            let small_least = EndianNat::from_nat(least, Self::exp());
825            let small_rest = Self::from_big(rest);
826            Self::to_nat_append_least(small_rest, small_least);
827            Self::from_nat_to_nat(least, Self::exp());
828        }
829    }
830
831    /// Converts an `EndianNat` representation in the "small" base `B` to an `EndianNat` representation in the "big" base `BIG`.
832    /// The result represents the same non-negative number as the original.
833    #[verifier::opaque]
834    pub open spec fn to_big<BIG>(n: EndianNat<B>) -> EndianNat<BIG> where
835        BIG: BasePow2,
836        B: CompatibleSmallerBaseFor<BIG>,
837
838        recommends
839            n.len() % Self::exp() == 0,
840        decreases n.len(),
841        when n.len() % Self::exp() == 0
842        via Self::to_big_decreases
843    {
844        if n.len() == 0 {
845            EndianNat::new(n.endian, Seq::empty())
846        } else {
847            Self::to_big(n.skip_least(Self::exp())).append_least(
848                EndianNat::new(n.endian, seq![n.take_least(Self::exp()).to_nat() as int]),
849            )
850        }
851    }
852
853    #[via_fn]
854    proof fn to_big_decreases<BIG>(n: EndianNat<B>) where
855        BIG: BasePow2,
856        B: CompatibleSmallerBaseFor<BIG>,
857     {
858        broadcast use EndianNat::exp_properties;
859
860        if n.len() != 0 {
861            assert(Self::exp() <= n.len()) by {
862                broadcast use crate::vstd::arithmetic::div_mod::lemma_mod_is_zero;
863
864            }
865            assert(n.skip_least(Self::exp()).len() < n.len());
866        }
867    }
868
869    pub broadcast proof fn to_big_properties<BIG>(n: EndianNat<B>) where
870        BIG: BasePow2,
871        B: CompatibleSmallerBaseFor<BIG>,
872
873        requires
874            n.wf(),
875            n.endian == endianness(),
876            n.len() % Self::exp() == 0,
877        ensures
878            #![trigger Self::to_big(n)]
879            Self::to_big(n).wf(),
880            Self::to_big(n).endian == endianness(),
881            Self::to_big(n).len() == n.len() / Self::exp(),
882            Self::to_big(n).to_nat() == n.to_nat(),
883        decreases n.len(),
884    {
885        reveal(EndianNat::to_big);
886        reveal(EndianNat::to_nat);
887        broadcast use EndianNat::exp_properties;
888
889        if n.len() == 0 {
890        } else {
891            let least = n.take_least(Self::exp());
892            let rest = n.skip_least(Self::exp());
893            assert(n.len() >= Self::exp()) by (nonlinear_arith)
894                requires
895                    n.len() % Self::exp() == 0,
896                    Self::exp() > 0,
897                    n.len() > 0,
898            ;
899            assert(rest.len() % Self::exp() == 0) by {
900                lemma_mod_multiples_vanish(-1 as int, n.len() as int, Self::exp() as int);
901                assert(n.len() % Self::exp() == 0);
902                assert(rest.len() == n.len() - Self::exp() == -1 * Self::exp() + n.len());
903            }
904            Self::to_big_properties(rest);
905            Self::to_nat_properties(least);
906            let big_least = EndianNat::<BIG>::new(n.endian, seq![least.to_nat() as int]);
907            let big_rest = Self::to_big(rest);
908            assert(Self::to_big(n).to_nat() == n.to_nat()) by {
909                assert(big_rest.append_least(big_least).to_nat() == (big_rest.to_nat()
910                    * base_upper_bound_excl::<BIG>(big_least.len())) + big_least.to_nat()) by {
911                    EndianNat::<BIG>::to_nat_append_least(big_rest, big_least);
912                }
913                assert(big_least.to_nat() == least.to_nat()) by {
914                    assert(big_least.drop_least().to_nat() * BIG::base() + big_least.least()
915                        == least.to_nat()) by {
916                        assert(big_least.least() == least.to_nat());
917                        assert(big_least.drop_least().to_nat() == 0);
918                        lemma_mul_basics(BIG::base() as int);
919                    }
920                }
921                assert(n.to_nat() == (rest.to_nat() * base_upper_bound_excl::<B>(Self::exp()))
922                    + least.to_nat()) by {
923                    assert(n =~= rest.append_least(least));
924                    EndianNat::<B>::to_nat_append_least(rest, least);
925                }
926                assert(base_upper_bound_excl::<B>(Self::exp()) == base_upper_bound_excl::<BIG>(
927                    big_least.len(),
928                )) by {
929                    broadcast use lemma_pow1;
930
931                }
932            }
933            assert(Self::to_big(n).len() == n.len() / Self::exp()) by {
934                assert(big_rest.len() == rest.len() / Self::exp());
935                assert(Self::to_big(n).len() == big_rest.len() + 1);
936                assert(n.len() == rest.len() + Self::exp());
937                assert(Self::exp() > 0);
938                lemma_div_plus_one(rest.len() as int, Self::exp() as int);
939            }
940        }
941
942    }
943
944    /// Ensures that performing [`to_big`] and then [`from_big`] results in the original `EndianNat<B>`.
945    ///
946    /// [`to_big`]: EndianNat::to_big
947    /// [`from_big`]: EndianNat::from_big
948    pub broadcast proof fn to_big_from_big<BIG>(n: EndianNat<B>) where
949        BIG: BasePow2,
950        B: CompatibleSmallerBaseFor<BIG>,
951
952        requires
953            n.wf(),
954            n.endian == endianness(),
955            n.len() % Self::exp() == 0,
956        ensures
957            #[trigger] Self::from_big(Self::to_big(n)) == n,
958        decreases n.len(),
959    {
960        reveal(EndianNat::to_big);
961        broadcast use EndianNat::exp_properties;
962
963        if n.len() == 0 {
964        } else {
965            let least = n.take_least(Self::exp());
966            let rest = n.skip_least(Self::exp());
967            assert(n.len() >= Self::exp()) by (nonlinear_arith)
968                requires
969                    n.len() % Self::exp() == 0,
970                    Self::exp() > 0,
971                    n.len() > 0,
972            ;
973            // `rest.len() == n.len() - exp` and `n.len() % exp == 0`, so
974            // `rest.len() % exp == (-exp + n.len()) % exp == n.len() % exp == 0`.
975            lemma_mod_sub_multiples_vanish(n.len() as int, Self::exp() as int);
976            assert(rest.len() % Self::exp() == 0);
977            Self::to_big_from_big(rest);
978            let big = Self::to_big(n);
979            assert(big =~= Self::to_big(rest).append_least(
980                EndianNat::new(n.endian, seq![least.to_nat() as int]),
981            ));
982            let big_least = big.least();
983            let big_rest = big.drop_least();
984            assert(big_rest =~= Self::to_big(rest));
985            assert(Self::from_big(big_rest) == rest);
986            Self::to_nat_from_nat(least);
987            assert(EndianNat::<B>::from_nat(big_least, Self::exp()) == least);
988        }
989    }
990
991    /// Ensures that performing [`from_big`] and then [`to_big`] results in the original `EndianNat<BIG>`.
992    ///
993    /// [`to_big`]: EndianNat::to_big
994    /// [`from_big`]: EndianNat::from_big
995    pub broadcast proof fn from_big_to_big<BIG>(n: EndianNat<BIG>) where
996        BIG: BasePow2,
997        B: CompatibleSmallerBaseFor<BIG>,
998
999        requires
1000            n.wf(),
1001            n.endian == endianness(),
1002        ensures
1003            #[trigger] Self::to_big(Self::from_big(n)) == n,
1004        decreases n.len(),
1005    {
1006        reveal(EndianNat::to_big);
1007        reveal(EndianNat::to_nat);
1008        broadcast use EndianNat::exp_properties;
1009
1010        if n.len() == 0 {
1011            Self::from_big_properties(n);
1012            let small = Self::from_big(n);
1013            assert(small.len() % Self::exp() == 0) by (nonlinear_arith)
1014                requires
1015                    small.len() == 0,
1016                    Self::exp() > 0,
1017            ;
1018            Self::to_big_properties(small);
1019            assert(Self::to_big(Self::from_big(n)).digits == n.digits);
1020            assert(Self::to_big(Self::from_big(n)).endian == n.endian);
1021        } else {
1022            let least = n.least();
1023            let rest = n.drop_least();
1024            Self::from_big_to_big(rest);
1025            Self::from_big_properties(rest);
1026
1027            let small = Self::from_big(n);
1028            let small_least = small.take_least(Self::exp());
1029            let small_rest = small.skip_least(Self::exp());
1030            Self::from_nat_properties(least, Self::exp());
1031            let from_nat_least = EndianNat::<B>::from_nat(least, Self::exp());
1032            assert(small_least =~= from_nat_least);
1033            EndianNat::<B>::from_nat_to_nat(least, Self::exp());
1034
1035            assert(small_rest =~= Self::from_big(rest));
1036            // `(rest.len() * exp) % exp == 0`
1037            lemma_mod_multiples_basic(rest.len() as int, Self::exp() as int);
1038            assert(small_rest.len() % Self::exp() == 0);
1039
1040            Self::from_big_properties(n);
1041            // `(n.len() * exp) % exp == 0`.  Use the dedicated lemma rather than
1042            // a bare `nonlinear_arith`, which times out under Z3 >= 4.13.
1043            lemma_mod_multiples_basic(n.len() as int, Self::exp() as int);
1044            assert(small.len() % Self::exp() == 0);
1045        }
1046    }
1047
1048    pub broadcast proof fn to_big_injective<BIG>(n1: EndianNat<B>, n2: EndianNat<B>) where
1049        BIG: BasePow2,
1050        B: CompatibleSmallerBaseFor<BIG>,
1051
1052        requires
1053            n1.wf(),
1054            n2.wf(),
1055            n1.endian == endianness(),
1056            n2.endian == endianness(),
1057            n1.len() % Self::exp() == 0,
1058            n2.len() % Self::exp() == 0,
1059            #[trigger] Self::to_big(n1) == #[trigger] Self::to_big(n2),
1060        ensures
1061            n1 == n2,
1062    {
1063        broadcast use EndianNat::to_big_from_big;
1064
1065        assert(Self::from_big(Self::to_big(n1)) == n1);
1066        assert(Self::from_big(Self::to_big(n2)) == n2);
1067    }
1068
1069    pub broadcast proof fn from_big_injective<BIG>(n1: EndianNat<BIG>, n2: EndianNat<BIG>) where
1070        BIG: BasePow2,
1071        B: CompatibleSmallerBaseFor<BIG>,
1072
1073        requires
1074            n1.wf(),
1075            n2.wf(),
1076            n1.endian == endianness(),
1077            n2.endian == endianness(),
1078            #[trigger] Self::from_big(n1) == #[trigger] Self::from_big(n2),
1079        ensures
1080            n1 == n2,
1081    {
1082        broadcast use EndianNat::from_big_to_big;
1083
1084        assert(Self::to_big(Self::from_big(n1)) == n1);
1085        assert(Self::to_big(Self::from_big(n2)) == n2);
1086    }
1087
1088    #[verifier::spinoff_prover]
1089    pub proof fn to_big_single<BIG>(x: EndianNat<B>) where
1090        BIG: BasePow2,
1091        B: CompatibleSmallerBaseFor<BIG>,
1092
1093        requires
1094            x.len() == Self::exp(),
1095            x.len() > 0,
1096        ensures
1097            Self::to_big(x).len() == 1,
1098            Self::to_big(x).index(0) == x.to_nat() as int,
1099    {
1100        broadcast use EndianNat::exp_properties;
1101
1102        reveal(EndianNat::to_big);
1103        crate::vstd::arithmetic::div_mod::lemma_mod_self_0(Self::exp() as int);
1104        crate::vstd::arithmetic::div_mod::lemma_small_mod(0, Self::exp());
1105        assert(x.len() % Self::exp() == 0);
1106        assert(x.skip_least(Self::exp()).len() == 0);
1107        assert(x.skip_least(Self::exp()).len() % Self::exp() == 0);
1108        assert(x =~= x.take_least(Self::exp()));
1109        assert(Self::to_big(x) == Self::to_big(x.skip_least(Self::exp())).append_least(
1110            EndianNat::new(x.endian, seq![x.take_least(Self::exp()).to_nat() as int]),
1111        ));
1112    }
1113}
1114
1115/***** Functions involving both little and big endian *****/
1116
1117/// Converts a sequence of digits in base `B` in default endianness ([`endianness()`]) to an `EndianNat` in the larger base `BIG`.
1118pub open spec fn to_big_from_digits<BIG, B>(n: Seq<B>) -> EndianNat<BIG> where
1119    BIG: BasePow2,
1120    B: CompatibleSmallerBaseFor<BIG> + Integer,
1121 {
1122    EndianNat::<B>::to_big::<BIG>(EndianNat::<B>::new(endianness(), n.map(|i, d| d as int)))
1123}
1124
1125/***** Implementations and proofs for specific types *****/
1126
1127impl Base for u8 {
1128    open spec fn base() -> nat {
1129        u8::MAX as nat + 1
1130    }
1131
1132    proof fn base_min() {
1133    }
1134}
1135
1136impl Base for u64 {
1137    open spec fn base() -> nat {
1138        u64::MAX as nat + 1
1139    }
1140
1141    proof fn base_min() {
1142    }
1143}
1144
1145impl Base for usize {
1146    open spec fn base() -> nat {
1147        usize::MAX as nat + 1
1148    }
1149
1150    proof fn base_min() {
1151    }
1152}
1153
1154impl BasePow2 for u8 {
1155    open spec fn bits() -> nat {
1156        8
1157    }
1158
1159    proof fn bits_to_base() {
1160        crate::vstd::arithmetic::power2::lemma2_to64();
1161    }
1162}
1163
1164impl BasePow2 for u64 {
1165    open spec fn bits() -> nat {
1166        64
1167    }
1168
1169    proof fn bits_to_base() {
1170        crate::vstd::arithmetic::power2::lemma2_to64();
1171    }
1172}
1173
1174impl BasePow2 for usize {
1175    open spec fn bits() -> nat {
1176        usize::BITS as nat
1177    }
1178
1179    proof fn bits_to_base() {
1180        crate::vstd::arithmetic::power2::lemma2_to64();
1181    }
1182}
1183
1184impl CompatibleSmallerBaseFor<u64> for u8 {
1185    proof fn compatible() {
1186    }
1187}
1188
1189impl CompatibleSmallerBaseFor<usize> for u8 {
1190    proof fn compatible() {
1191    }
1192}
1193
1194pub broadcast group group_endian_nat_axioms {
1195    EndianNat::from_nat_properties,
1196    EndianNat::to_nat_properties,
1197    EndianNat::from_nat_to_nat,
1198    EndianNat::to_nat_from_nat,
1199    EndianNat::to_nat_injective,
1200    EndianNat::from_nat_injective,
1201    EndianNat::to_nat_eq_to_nat_most,
1202    EndianNat::exp_properties,
1203    EndianNat::to_big_properties,
1204    EndianNat::from_big_properties,
1205    EndianNat::from_big_to_big,
1206    EndianNat::to_big_from_big,
1207    EndianNat::to_big_injective,
1208    EndianNat::from_big_injective,
1209}
1210
1211} // verus!
vstd/endian.rs

vstd/
endian.rs
