vstd/
endian.rs

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

vstd/
endian.rs
