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

vstd/
endian.rs
