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            let endian_nat = Self::from_nat(n, len);
498            let least = endian_nat.least();
499            let rest = endian_nat.drop_least();
500            assert(rest =~= Self::from_nat(n / B::base(), (len - 1) as nat));
501            Self::base_upper_bound_excl_len(n, len);
502            Self::from_nat_to_nat(n / B::base(), (len - 1) as nat);
503            assert((n % B::base()) + (n / B::base()) * B::base() == n) by (nonlinear_arith)
504                requires
505                    B::base() > 0,
506            ;
507        }
508    }
509
510    /// Ensures that performing [`to_nat`] and then [`from_nat`] results in the original `EndianNat`.
511    ///
512    /// [`from_nat`]: EndianNat::from_nat
513    /// [`to_nat`]: EndianNat::to_nat
514    pub broadcast proof fn to_nat_from_nat(endian_nat: Self)
515        requires
516            endian_nat.wf(),
517            endian_nat.endian == endianness(),
518        ensures
519            #[trigger] Self::from_nat(endian_nat.to_nat(), endian_nat.len()) == endian_nat,
520        decreases endian_nat.len(),
521    {
522        reveal(pow);
523        reveal(EndianNat::to_nat);
524        if endian_nat.len() == 0 {
525        } else {
526            let n = endian_nat.to_nat();
527            let least = endian_nat.least();
528            let rest = endian_nat.drop_least();
529            Self::to_nat_from_nat(rest);
530            assert(least == n % B::base() && rest.to_nat() == n / B::base()) by {
531                assert(n == rest.to_nat() * B::base() + least);
532                assert(least < B::base());
533                lemma_fundamental_div_mod_converse(
534                    n as int,
535                    B::base() as int,
536                    rest.to_nat() as int,
537                    least as int,
538                );
539            }
540        }
541    }
542
543    pub broadcast proof fn to_nat_injective(n1: Self, n2: Self)
544        requires
545            n1.wf(),
546            n2.wf(),
547            n1.endian == endianness(),
548            n2.endian == endianness(),
549            n1.len() == n2.len(),
550            #[trigger] n1.to_nat() == #[trigger] n2.to_nat(),
551        ensures
552            n1 == n2,
553    {
554        broadcast use EndianNat::to_nat_from_nat;
555
556        assert(Self::from_nat(n1.to_nat(), n1.len()) == n1);
557        assert(Self::from_nat(n2.to_nat(), n2.len()) == n2);
558    }
559
560    pub broadcast proof fn from_nat_injective(n1: nat, len1: nat, n2: nat, len2: nat)
561        requires
562            n1 < base_upper_bound_excl::<B>(len1),
563            n2 < base_upper_bound_excl::<B>(len2),
564            #[trigger] Self::from_nat(n1, len1) == #[trigger] Self::from_nat(n2, len2),
565        ensures
566            n1 == n2,
567    {
568        broadcast use EndianNat::from_nat_to_nat;
569
570        assert(Self::from_nat(n1, len1).to_nat() == n1);
571        assert(Self::from_nat(n2, len2).to_nat() == n2);
572    }
573
574    /// Converts an `EndianNat` to the natural number that it represents, processing the digits from most significant to least significant, hiding the details of endianness.
575    #[verifier::opaque]
576    pub open spec fn to_nat_most(self) -> nat
577        decreases self.len(),
578    {
579        if self.len() == 0 {
580            0
581        } else {
582            (self.drop_most().to_nat_most() + self.most() * pow(
583                B::base() as int,
584                (self.len() - 1) as nat,
585            )) as nat
586        }
587    }
588
589    /// Ensures that [`to_nat`] and [`to_nat_most`] agree.
590    ///
591    /// [`to_nat`]: EndianNat::to_nat
592    /// [`to_nat_most`]: EndianNat::to_nat_most
593    pub broadcast proof fn to_nat_eq_to_nat_most(self)
594        requires
595            self.wf(),
596        ensures
597            #[trigger] self.to_nat() == #[trigger] self.to_nat_most(),
598        decreases self.len(),
599    {
600        reveal(EndianNat::to_nat);
601        reveal(EndianNat::to_nat_most);
602        if self.len() == 0 {
603        } else {
604            if self.drop_most().len() == 0 {
605                calc! {
606                    (==)
607                    self.to_nat_most(); {
608                        assert(self.drop_most().to_nat_most() == 0);
609                        assert(self.to_nat_most() == (self.most() * pow(
610                            B::base() as int,
611                            (self.len() - 1) as nat,
612                        )) as nat);
613                    }
614                    (self.most() * pow(B::base() as int, (self.len() - 1) as nat)) as nat; {
615                        reveal(pow);
616                        assert((self.most() * pow(B::base() as int, (self.len() - 1) as nat))
617                            == self.most()) by (nonlinear_arith)
618                            requires
619                                pow(B::base() as int, (self.len() - 1) as nat) == 1,
620                                self.most() >= 0,
621                        ;
622                    }
623                    self.most(); {}
624                    self.least(); {
625                        assert(self.drop_least().to_nat() == 0);
626                        assert(0 * B::base() == 0);
627                    }
628                    self.to_nat();
629                };
630            } else {
631                calc! {
632                    (==)
633                    self.to_nat_most() as int; {}
634                    ((self.drop_most().to_nat_most() + self.most() * pow(
635                        B::base() as int,
636                        (self.len() - 1) as nat,
637                    )) as nat) as int; {
638                        assert(self.most() >= 0);
639                        assert(self.len() > 1);
640                        lemma_pow_positive(B::base() as int, (self.len() - 1) as nat);
641                        assert(pow(B::base() as int, (self.len() - 1) as nat) >= 0);
642                    }
643                    self.drop_most().to_nat_most() + self.most() * pow(
644                        B::base() as int,
645                        (self.len() - 1) as nat,
646                    ); {
647                        self.drop_most().to_nat_eq_to_nat_most();
648                    }
649                    self.drop_most().to_nat() + self.most() * pow(
650                        B::base() as int,
651                        (self.len() - 1) as nat,
652                    ); {}
653                    self.drop_most().drop_least().to_nat() * B::base() + self.drop_most().least()
654                        + self.most() * pow(B::base() as int, (self.len() - 1) as nat); {
655                        self.drop_most().drop_least().to_nat_eq_to_nat_most();
656                    }
657                    self.drop_most().drop_least().to_nat_most() * B::base()
658                        + self.drop_most().least() + self.most() * pow(
659                        B::base() as int,
660                        (self.len() - 1) as nat,
661                    ); {
662                        assert(self.drop_most().drop_least() == self.drop_least().drop_most());
663                    }
664                    self.drop_least().drop_most().to_nat_most() * B::base() + self.least()
665                        + self.most() * pow(B::base() as int, (self.len() - 1) as nat); {
666                        assert(self.most() * pow(B::base() as int, (self.len() - 2) as nat)
667                            * B::base() == self.most() * (pow(
668                            B::base() as int,
669                            (self.len() - 2) as nat,
670                        ) * B::base())) by {
671                            broadcast use crate::vstd::arithmetic::mul::lemma_mul_is_associative;
672
673                        }
674                        assert(pow(B::base() as int, (self.len() - 1) as nat) == pow(
675                            B::base() as int,
676                            (self.len() - 2) as nat,
677                        ) * B::base()) by {
678                            assert(B::base() == pow(B::base() as int, 1)) by {
679                                lemma_pow1(B::base() as int);
680                            }
681                            lemma_pow_adds(B::base() as int, (self.len() - 2) as nat, 1);
682                        }
683                    }
684                    self.drop_least().drop_most().to_nat_most() * B::base() + (self.most() * pow(
685                        B::base() as int,
686                        (self.len() - 2) as nat,
687                    )) * B::base() + self.least(); {
688                        lemma_mul_is_distributive_add_other_way(
689                            B::base() as int,
690                            self.drop_least().drop_most().to_nat_most() as int,
691                            self.most() * pow(B::base() as int, (self.len() - 2) as nat),
692                        );
693                    }
694                    (self.drop_least().drop_most().to_nat_most() + self.most() * pow(
695                        B::base() as int,
696                        (self.len() - 2) as nat,
697                    )) * B::base() + self.least(); {
698                        assert((self.drop_least().drop_most().to_nat_most() + self.most() * pow(
699                            B::base() as int,
700                            (self.len() - 2) as nat,
701                        )) == self.drop_least().to_nat_most()) by {
702                            lemma_pow_positive(B::base() as int, (self.len() - 2) as nat);
703                        };
704                    }
705                    (self.drop_least().to_nat_most() * B::base() + self.least()) as int; {
706                        self.drop_least().to_nat_eq_to_nat_most();
707                    }
708                    self.to_nat() as int;
709                }
710            }
711        }
712    }
713}
714
715// /////////////////////////////////////////////////// //
716//         Conversion Routines                         //
717// /////////////////////////////////////////////////// //
718impl<B: Base> EndianNat<B> {
719    /// [`B::base()`] to the power of `exp()` is [`BIG::base()`].
720    /// In other words, `exp()` is the number of digits in base `B` that correspond to a single digit in base `BIG`.
721    ///
722    /// [`B::base()`]: Base::base
723    /// [`BIG::base()`]: Base::base
724    pub open spec fn exp<BIG>() -> nat where BIG: BasePow2, B: CompatibleSmallerBaseFor<BIG> {
725        BIG::bits() / B::bits()
726    }
727
728    pub broadcast proof fn exp_properties<BIG>() where
729        BIG: BasePow2,
730        B: CompatibleSmallerBaseFor<BIG>,
731
732        ensures
733            #![trigger Self::exp()]
734            base_upper_bound_excl::<B>(Self::exp()) == BIG::base(),
735            Self::exp() > 0,
736    {
737        broadcast use crate::vstd::arithmetic::div_mod::group_div_basics;
738
739        assert(forall|x| x != 0 ==> #[trigger] (0int / x) == 0);
740        broadcast use crate::vstd::arithmetic::power::lemma_pow_multiplies;
741
742        B::bits_to_base();
743
744        calc! {
745            (==)
746            BIG::bits(); {
747                crate::vstd::arithmetic::div_mod::lemma_fundamental_div_mod(
748                    BIG::bits() as int,
749                    B::bits() as int,
750                );
751            }
752            B::bits() * (BIG::bits() / B::bits()) + (BIG::bits() % B::bits()); {
753                B::compatible();
754            }
755            B::bits() * (BIG::bits() / B::bits()); {}
756            B::bits() * Self::exp();
757        }
758        calc! {
759            (==)
760            base_upper_bound_excl::<B>(Self::exp()); {
761                crate::vstd::arithmetic::power::lemma_pow_multiplies(2, B::bits(), Self::exp());
762                crate::vstd::arithmetic::power2::lemma_pow2(B::bits());
763            }
764            pow(2, B::bits() * Self::exp()) as int; {}
765            pow(2, BIG::bits()) as int; {
766                crate::vstd::arithmetic::power2::lemma_pow2(BIG::bits());
767            }
768            pow2(BIG::bits()) as int; {
769                BIG::bits_to_base();
770            }
771            BIG::base() as int;
772        }
773
774        B::compatible();
775        assert((BIG::bits() / B::bits()) != 0);
776        BIG::bits_to_base();
777
778    }
779
780    /// Converts an `EndianNat` representation in the "big" base `BIG` to an `EndianNat` representation in the "small" base `B`.
781    /// The result represents the same non-negative number as the original.
782    pub open spec fn from_big<BIG>(n: EndianNat<BIG>) -> Self where
783        BIG: BasePow2,
784        B: CompatibleSmallerBaseFor<BIG>,
785
786        decreases n.len(),
787    {
788        if n.len() == 0 {
789            EndianNat::new(n.endian, Seq::empty())
790        } else {
791            Self::from_big(n.drop_least()).append_least(EndianNat::from_nat(n.least(), Self::exp()))
792        }
793    }
794
795    pub broadcast proof fn from_big_properties<BIG>(n: EndianNat<BIG>) where
796        BIG: BasePow2,
797        B: CompatibleSmallerBaseFor<BIG>,
798
799        requires
800            n.wf(),
801            n.endian == endianness(),
802        ensures
803            #![trigger Self::from_big(n)]
804            Self::from_big(n).wf(),
805            Self::from_big(n).endian == endianness(),
806            Self::from_big(n).len() == n.len() * Self::exp(),
807            Self::from_big(n).to_nat() == n.to_nat(),
808        decreases n.len(),
809    {
810        reveal(EndianNat::to_nat);
811        broadcast use EndianNat::exp_properties;
812
813        if n.len() == 0 {
814        } else {
815            let least = n.least();
816            let rest = n.drop_least();
817            Self::from_big_properties(rest);
818            Self::from_nat_properties(least, Self::exp());
819            assert(Self::from_big(n).len() == n.len() * Self::exp()) by (nonlinear_arith)
820                requires
821                    Self::from_big(n).len() == (n.len() - 1) * Self::exp() + Self::exp(),
822            ;
823            let small_least = EndianNat::from_nat(least, Self::exp());
824            let small_rest = Self::from_big(rest);
825            Self::to_nat_append_least(small_rest, small_least);
826            Self::from_nat_to_nat(least, Self::exp());
827        }
828    }
829
830    /// Converts an `EndianNat` representation in the "small" base `B` to an `EndianNat` representation in the "big" base `BIG`.
831    /// The result represents the same non-negative number as the original.
832    #[verifier::opaque]
833    pub open spec fn to_big<BIG>(n: EndianNat<B>) -> EndianNat<BIG> where
834        BIG: BasePow2,
835        B: CompatibleSmallerBaseFor<BIG>,
836
837        recommends
838            n.len() % Self::exp() == 0,
839        decreases n.len(),
840        when n.len() % Self::exp() == 0
841        via Self::to_big_decreases
842    {
843        if n.len() == 0 {
844            EndianNat::new(n.endian, Seq::empty())
845        } else {
846            Self::to_big(n.skip_least(Self::exp())).append_least(
847                EndianNat::new(n.endian, seq![n.take_least(Self::exp()).to_nat() as int]),
848            )
849        }
850    }
851
852    #[via_fn]
853    proof fn to_big_decreases<BIG>(n: EndianNat<B>) where
854        BIG: BasePow2,
855        B: CompatibleSmallerBaseFor<BIG>,
856     {
857        broadcast use EndianNat::exp_properties;
858
859        if n.len() != 0 {
860            assert(Self::exp() <= n.len()) by {
861                broadcast use crate::vstd::arithmetic::div_mod::lemma_mod_is_zero;
862
863            }
864            assert(n.skip_least(Self::exp()).len() < n.len());
865        }
866    }
867
868    pub broadcast proof fn to_big_properties<BIG>(n: EndianNat<B>) where
869        BIG: BasePow2,
870        B: CompatibleSmallerBaseFor<BIG>,
871
872        requires
873            n.wf(),
874            n.endian == endianness(),
875            n.len() % Self::exp() == 0,
876        ensures
877            #![trigger Self::to_big(n)]
878            Self::to_big(n).wf(),
879            Self::to_big(n).endian == endianness(),
880            Self::to_big(n).len() == n.len() / Self::exp(),
881            Self::to_big(n).to_nat() == n.to_nat(),
882        decreases n.len(),
883    {
884        reveal(EndianNat::to_big);
885        reveal(EndianNat::to_nat);
886        broadcast use EndianNat::exp_properties;
887
888        if n.len() == 0 {
889        } else {
890            let least = n.take_least(Self::exp());
891            let rest = n.skip_least(Self::exp());
892            assert(n.len() >= Self::exp()) by (nonlinear_arith)
893                requires
894                    n.len() % Self::exp() == 0,
895                    Self::exp() > 0,
896                    n.len() > 0,
897            ;
898            assert(rest.len() % Self::exp() == 0) by {
899                lemma_mod_multiples_vanish(-1 as int, n.len() as int, Self::exp() as int);
900                assert(n.len() % Self::exp() == 0);
901                assert(rest.len() == n.len() - Self::exp() == -1 * Self::exp() + n.len());
902            }
903            Self::to_big_properties(rest);
904            Self::to_nat_properties(least);
905            let big_least = EndianNat::<BIG>::new(n.endian, seq![least.to_nat() as int]);
906            let big_rest = Self::to_big(rest);
907            assert(Self::to_big(n).to_nat() == n.to_nat()) by {
908                assert(big_rest.append_least(big_least).to_nat() == (big_rest.to_nat()
909                    * base_upper_bound_excl::<BIG>(big_least.len())) + big_least.to_nat()) by {
910                    EndianNat::<BIG>::to_nat_append_least(big_rest, big_least);
911                }
912                assert(big_least.to_nat() == least.to_nat()) by {
913                    assert(big_least.drop_least().to_nat() * BIG::base() + big_least.least()
914                        == least.to_nat()) by {
915                        assert(big_least.least() == least.to_nat());
916                        assert(big_least.drop_least().to_nat() == 0);
917                        lemma_mul_basics(BIG::base() as int);
918                    }
919                }
920                assert(n.to_nat() == (rest.to_nat() * base_upper_bound_excl::<B>(Self::exp()))
921                    + least.to_nat()) by {
922                    assert(n =~= rest.append_least(least));
923                    EndianNat::<B>::to_nat_append_least(rest, least);
924                }
925                assert(base_upper_bound_excl::<B>(Self::exp()) == base_upper_bound_excl::<BIG>(
926                    big_least.len(),
927                )) by {
928                    broadcast use lemma_pow1;
929
930                }
931            }
932            assert(Self::to_big(n).len() == n.len() / Self::exp()) by {
933                assert(big_rest.len() == rest.len() / Self::exp());
934                assert(Self::to_big(n).len() == big_rest.len() + 1);
935                assert(n.len() == rest.len() + Self::exp());
936                assert(Self::exp() > 0);
937                lemma_div_plus_one(rest.len() as int, Self::exp() as int);
938            }
939        }
940
941    }
942
943    /// Ensures that performing [`to_big`] and then [`from_big`] results in the original `EndianNat<B>`.
944    ///
945    /// [`to_big`]: EndianNat::to_big
946    /// [`from_big`]: EndianNat::from_big
947    pub broadcast proof fn to_big_from_big<BIG>(n: EndianNat<B>) where
948        BIG: BasePow2,
949        B: CompatibleSmallerBaseFor<BIG>,
950
951        requires
952            n.wf(),
953            n.endian == endianness(),
954            n.len() % Self::exp() == 0,
955        ensures
956            #[trigger] Self::from_big(Self::to_big(n)) == n,
957        decreases n.len(),
958    {
959        reveal(EndianNat::to_big);
960        broadcast use EndianNat::exp_properties;
961
962        if n.len() == 0 {
963        } else {
964            let least = n.take_least(Self::exp());
965            let rest = n.skip_least(Self::exp());
966            assert(n.len() >= Self::exp()) by (nonlinear_arith)
967                requires
968                    n.len() % Self::exp() == 0,
969                    Self::exp() > 0,
970                    n.len() > 0,
971            ;
972            assert(rest.len() % Self::exp() == 0) by (nonlinear_arith)
973                requires
974                    rest.len() == n.len() - Self::exp(),
975                    n.len() % Self::exp() == 0,
976            ;
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            assert(small_rest.len() % Self::exp() == 0) by (nonlinear_arith)
1037                requires
1038                    small_rest.len() == rest.len() * Self::exp(),
1039                    Self::exp() > 0,
1040            ;
1041
1042            Self::from_big_properties(n);
1043            assert(small.len() % Self::exp() == 0) by (nonlinear_arith)
1044                requires
1045                    small.len() == n.len() * Self::exp(),
1046                    Self::exp() > 0,
1047            ;
1048        }
1049    }
1050
1051    pub broadcast proof fn to_big_injective<BIG>(n1: EndianNat<B>, n2: EndianNat<B>) where
1052        BIG: BasePow2,
1053        B: CompatibleSmallerBaseFor<BIG>,
1054
1055        requires
1056            n1.wf(),
1057            n2.wf(),
1058            n1.endian == endianness(),
1059            n2.endian == endianness(),
1060            n1.len() % Self::exp() == 0,
1061            n2.len() % Self::exp() == 0,
1062            #[trigger] Self::to_big(n1) == #[trigger] Self::to_big(n2),
1063        ensures
1064            n1 == n2,
1065    {
1066        broadcast use EndianNat::to_big_from_big;
1067
1068        assert(Self::from_big(Self::to_big(n1)) == n1);
1069        assert(Self::from_big(Self::to_big(n2)) == n2);
1070    }
1071
1072    pub broadcast proof fn from_big_injective<BIG>(n1: EndianNat<BIG>, n2: EndianNat<BIG>) where
1073        BIG: BasePow2,
1074        B: CompatibleSmallerBaseFor<BIG>,
1075
1076        requires
1077            n1.wf(),
1078            n2.wf(),
1079            n1.endian == endianness(),
1080            n2.endian == endianness(),
1081            #[trigger] Self::from_big(n1) == #[trigger] Self::from_big(n2),
1082        ensures
1083            n1 == n2,
1084    {
1085        broadcast use EndianNat::from_big_to_big;
1086
1087        assert(Self::to_big(Self::from_big(n1)) == n1);
1088        assert(Self::to_big(Self::from_big(n2)) == n2);
1089    }
1090
1091    pub proof fn to_big_single<BIG>(x: EndianNat<B>) where
1092        BIG: BasePow2,
1093        B: CompatibleSmallerBaseFor<BIG>,
1094
1095        requires
1096            x.len() == Self::exp(),
1097            x.len() > 0,
1098        ensures
1099            Self::to_big(x).len() == 1,
1100            Self::to_big(x).index(0) == x.to_nat() as int,
1101    {
1102        broadcast use EndianNat::exp_properties;
1103
1104        reveal(EndianNat::to_big);
1105        assert(x =~= x.take_least(Self::exp()));
1106        assert(Self::to_big(x) =~= Self::to_big(x.skip_least(Self::exp())).append_least(
1107            EndianNat::new(x.endian, seq![x.take_least(Self::exp()).to_nat() as int]),
1108        ));
1109    }
1110}
1111
1112/***** Functions involving both little and big endian *****/
1113
1114/// Converts a sequence of digits in base `B` in default endianness ([`endianness()`]) to an `EndianNat` in the larger base `BIG`.
1115pub open spec fn to_big_from_digits<BIG, B>(n: Seq<B>) -> EndianNat<BIG> where
1116    BIG: BasePow2,
1117    B: CompatibleSmallerBaseFor<BIG> + Integer,
1118 {
1119    EndianNat::<B>::to_big::<BIG>(EndianNat::<B>::new(endianness(), n.map(|i, d| d as int)))
1120}
1121
1122/***** Implementations and proofs for specific types *****/
1123
1124impl Base for u8 {
1125    open spec fn base() -> nat {
1126        u8::MAX as nat + 1
1127    }
1128
1129    proof fn base_min() {
1130    }
1131}
1132
1133impl Base for u64 {
1134    open spec fn base() -> nat {
1135        u64::MAX as nat + 1
1136    }
1137
1138    proof fn base_min() {
1139    }
1140}
1141
1142impl Base for usize {
1143    open spec fn base() -> nat {
1144        usize::MAX as nat + 1
1145    }
1146
1147    proof fn base_min() {
1148    }
1149}
1150
1151impl BasePow2 for u8 {
1152    open spec fn bits() -> nat {
1153        8
1154    }
1155
1156    proof fn bits_to_base() {
1157        crate::vstd::arithmetic::power2::lemma2_to64();
1158    }
1159}
1160
1161impl BasePow2 for u64 {
1162    open spec fn bits() -> nat {
1163        64
1164    }
1165
1166    proof fn bits_to_base() {
1167        crate::vstd::arithmetic::power2::lemma2_to64();
1168    }
1169}
1170
1171impl BasePow2 for usize {
1172    open spec fn bits() -> nat {
1173        usize::BITS as nat
1174    }
1175
1176    proof fn bits_to_base() {
1177        crate::vstd::arithmetic::power2::lemma2_to64();
1178    }
1179}
1180
1181impl CompatibleSmallerBaseFor<u64> for u8 {
1182    proof fn compatible() {
1183    }
1184}
1185
1186impl CompatibleSmallerBaseFor<usize> for u8 {
1187    proof fn compatible() {
1188    }
1189}
1190
1191pub broadcast group group_endian_nat_axioms {
1192    EndianNat::from_nat_properties,
1193    EndianNat::to_nat_properties,
1194    EndianNat::from_nat_to_nat,
1195    EndianNat::to_nat_from_nat,
1196    EndianNat::to_nat_injective,
1197    EndianNat::from_nat_injective,
1198    EndianNat::to_nat_eq_to_nat_most,
1199    EndianNat::exp_properties,
1200    EndianNat::to_big_properties,
1201    EndianNat::from_big_properties,
1202    EndianNat::from_big_to_big,
1203    EndianNat::to_big_from_big,
1204    EndianNat::to_big_injective,
1205    EndianNat::from_big_injective,
1206}
1207
1208} // verus!
vstd/endian.rs

vstd/
endian.rs
