Crate verified

Expand description

§Verifiable Rust

A collection of crates to facilitate the development of formally verifiable rust code.

Type level programming allows us to implement logic that can be verified by the compiler, which makes it possible to catch bugs at compile time, rather than at runtime.

Say we have an algorithm where the runtime scales exponentially. We would like to be able to restrict the number of elements in our working set to a reasonable number, let’s say 128, in order to ensure that the algorithm completes in a reasonable amount of time, every time.

use verified::*;

#[derive(Default)]
struct Collection<E, Size: Unsigned> {
    elements: Vec<E>,
    size: Size,
}

#[verify]
fn slow_routine<E, Size: Unsigned>(working_set: Collection<E, Size>)
where
    // Restrict the size of the working set.
    _: Verify<{ Size < 128 }, { Size > 0 }>
{
    // TODO
}

fn main() {
    // No problem here...
    slow_routine::<String, U1>(Default::default());
    slow_routine::<String, U127>(Default::default());

    // XXX: Does not compile because our working set is empty.
    slow_routine::<String, U0>(Default::default());

    // XXX: Does not compile because our working set is one element too large.
    slow_routine::<String, U128>(Default::default());
}

§#[verify]

The verified crate is built on top of the typenum crate, and provides syntactic sugar for defining type-level values via the #[verify] macro from the verify_macro crate. You can annotate almost any item with #[verify] (still a work in progress), and anywhere you would typically use a type like <A as Add>::Output, you can now simply write { A + B }.

For a more complete example, see the vec module. Here is an abbreviated snippet:

use verified::*;
use std::vec::Vec as Raw;

pub struct Vec<Size: Unsigned, Element>(Size, Raw<Element>);

#[verify]
impl<Size: Unsigned, Element> Vec<Size, Element> {
    pub fn append<OtherSize: Unsigned>(
        self,
        other: Vec<OtherSize, Element>,
    ) -> Vec<{ Size + OtherSize }, Element> {
        self + other
    }

    pub fn pop(self) -> (Vec<{ Size - 1 }, Element>, Element)
    where
        _: Verify<{ Size > 0 }>,
    {
        self.into()
    }

    pub fn push(self, e: Element) -> Vec<{ Size + 1 }, Element> {
        (self, e).into()
    }
}

#[verify]
impl<SizeL: Unsigned, SizeR: Unsigned, Element> std::ops::Add<Vec<SizeR, Element>>
    for Vec<SizeL, Element>
{
    type Output = Vec<{ SizeL + SizeR }, Element>;
    fn add(self, Vec(os, mut ov): Vec<SizeR, Element>) -> Self::Output {
        let Self(s, mut v) = self;
        v.append(&mut ov);
        Vec(s + os, v)
    }
}

#[verify]
impl<Size: Unsigned, Element> std::convert::From<(Vec<Size, Element>, Element)>
    for Vec<{ Size + 1 }, Element>
{
    fn from((Vec(_, mut v), e): (Vec<Size, Element>, Element)) -> Self {
        v.push(e);
        Self(Default::default(), v)
    }
}

#[verify]
impl<Size: Unsigned, Element> std::convert::From<Vec<Size, Element>>
    for (Vec<{ Size - 1 }, Element>, Element)
where
    _: Verify<{ Size > 0 }>,
{
    fn from(Vec(_, mut v): Vec<Size, Element>) -> Self {
        let e = v.pop().unwrap();
        (Vec(Default::default(), v), e)
    }
}

§Verify<…>

You may have noticed the strange where clauses that look like _: Verify<{ ... }, ...>. This Verify “trait” is processed by the #[verify] attribute. You can think of each argument as an expression that must evaluate to “true” in order to compile. This allows us to instrument our code with additional compile time checks for added safety.

§$ Compiling

The verified crate is built on top of the typenum crate. Naturally, the compiler errors can get pretty hairy. Here, I’ve accidentally typed 2 instead of 1 somewhere in the vec module. This is perhaps one of the less cryptic errors you may see…

$ cargo build

error[E0277]: cannot add `typenum::uint::UInt<typenum::uint::UTerm, typenum::bit::B1>` to `Size`
  --> verified/src/vec.rs:44:19
   |
44 |         (self, e).into()
   |                   ^^^^ no implementation for `Size + typenum::uint::UInt<typenum::uint::UTerm, typenum::bit::B1>`
   |
   = help: the trait `std::ops::Add<typenum::uint::UInt<typenum::uint::UTerm, typenum::bit::B1>>` is not implemented for `Size`
help: consider further restricting this bound with `+ std::ops::Add<typenum::uint::UInt<typenum::uint::UTerm, typenum::bit::B1>>`
  --> verified/src/vec.rs:28:12
   |
28 | impl<Size: Unsigned, Element> Vec<Size, Element> {
   |            ^^^^^^^^
   = note: required because of the requirements on the impl of `std::convert::From<(vec::Vec<Size, Element>, Element)>` for `vec::Vec<<Size as std::ops::Add<typenum::uint::UInt<typenum::uint::UInt<typenum::uint::UTerm, typenum::bit::B1>, typenum::bit::B0>>>::Output, Element>`
   = note: required because of the requirements on the impl of `std::convert::Into<vec::Vec<<Size as std::ops::Add<typenum::uint::UInt<typenum::uint::UInt<typenum::uint::UTerm, typenum::bit::B1>, typenum::bit::B0>>>::Output, Element>>` for `(vec::Vec<Size, Element>, Element)`

cargo-verify tries to help by translating types into simple arithmetic expressions where possible.

§$ cargo-verify

$ cargo verify build

error[E0277]: cannot add `1` to `Size`
  --> verified/src/vec.rs:44:19
   |
44 |         (self, e).into()
   |                   ^^^^ no implementation for `Size + 1`
   |
   = help: the trait `{ _ + 1 }` is not implemented for `Size`
help: consider further restricting this bound with `+ { _ + 1 }`
  --> verified/src/vec.rs:28:12
   |
28 | impl<Size: Unsigned, Element> Vec<Size, Element> {
   |            ^^^^^^^^
   = note: required because of the requirements on the impl of `std::convert::From<(vec::Vec<Size, Element>, Element)>` for `vec::Vec<{ Size + 2 }, Element>`
   = note: required because of the requirements on the impl of `std::convert::Into<vec::Vec<{ Size + 2 }, Element>>` for `(vec::Vec<Size, Element>, Element)`

§Install

$ cargo install cargo-verify

To upgrade:

$ cargo install --force cargo-verify

Or clone and build with $ cargo build then place the binary in your $PATH.

§Usage

$ cargo verify [COMMAND] [OPTIONS]...

Modules§

array: A type-level array of type-level numbers.
bit: Type-level bits.
consts
int: Type-level signed integers.
marker_traits: All of the marker traits used in typenum.
operator_aliases: Aliases for the type operators used in this crate. Their purpose is to increase the ergonomics of performing operations on the types defined here. For even more ergonomics, consider using the op! macro instead.
type_operators: Useful type operators that are not defined in core::ops.
uint: Type-level unsigned integers.
vec

Macros§

assert_type: Asserts that a type is True, aka B1.
assert_type_eq: Asserts that two types are the same.
cmpDeprecated: A convenience macro for comparing type numbers. Use op! instead.
op: Convenient type operations.
tarr: Create a new type-level array. Only usable on Rust 1.13.0 or newer.
vec

Structs§

ATerm: The terminating type for type arrays.
B0: The type-level bit 0.
B1: The type-level bit 1.
Equal: A potential output from Cmp, this is the type equivalent to the enum variant core::cmp::Ordering::Equal.
Greater: A potential output from Cmp, this is the type equivalent to the enum variant core::cmp::Ordering::Greater.
Less: A potential output from Cmp, this is the type equivalent to the enum variant core::cmp::Ordering::Less.
NInt: Type-level signed integers with negative sign.
PInt: Type-level signed integers with positive sign.
TArr: TArr is a type that acts as an array of types. It is defined similarly to UInt, only its values can be more than bits, and it is designed to act as an array. So you can only add two if they have the same number of elements, for example.
UInt: UInt is defined recursively, where B is the least significant bit and U is the rest of the number. Conceptually, U should be bound by the trait Unsigned and B should be bound by the trait Bit, but enforcing these bounds causes linear instead of logrithmic scaling in some places, so they are left off for now. They may be enforced in future.
UTerm: The terminating type for UInt; it always comes after the most significant bit. UTerm by itself represents zero, which is aliased to U0.
Z0: The type-level signed integer 0.

Traits§

Abs: A type operator that returns the absolute value.
Add: The addition operator +.
Bit: The marker trait for compile time bits.
BitAnd: The bitwise AND operator &.
BitOr: The bitwise OR operator |.
BitXor: The bitwise XOR operator ^.
Cmp: A type operator for comparing Self and Rhs. It provides a similar functionality to the function core::cmp::Ord::cmp but for types.
Div: The division operator /.
FoldAdd: A type operator that gives the sum of all elements of an Array.
FoldMul: A type operator that gives the product of all elements of an Array.
Gcd: A type operator that computes the greatest common divisor of Self and Rhs.
Integer: The marker trait for compile time signed integers.
IsEqual: A type operator that returns True if Self == Rhs, otherwise returns False.
IsGreater: A type operator that returns True if Self > Rhs, otherwise returns False.
IsGreaterOrEqual: A type operator that returns True if Self >= Rhs, otherwise returns False.
IsLess: A type operator that returns True if Self < Rhs, otherwise returns False.
IsLessOrEqual: A type operator that returns True if Self <= Rhs, otherwise returns False.
IsNotEqual: A type operator that returns True if Self != Rhs, otherwise returns False.
Len: A type operator that gives the length of an Array or the number of bits in a UInt.
Logarithm2: A type operator for taking the integer binary logarithm of Self.
Max: A type operator that returns the maximum of Self and Rhs.
Min: A type operator that returns the minimum of Self and Rhs.
Mul: The multiplication operator *.
NonZero: A marker trait to designate that a type is not zero. All number types in this crate implement NonZero except B0, U0, and Z0.
Not: The unary logical negation operator !.
Ord: A Marker trait for the types Greater, Equal, and Less.
PartialDiv: Division as a partial function. This type operator performs division just as Div, but is only defined when the result is an integer (i.e. there is no remainder).
Pow: A type operator that provides exponentiation by repeated squaring.
PowerOfTwo: The marker trait for type-level numbers which are a power of two.
Rem: The remainder operator %.
Same: A type operator that ensures that Rhs is the same as Self, it is mainly useful for writing macros that can take arbitrary binary or unary operators.
Shl: The left shift operator <<. Note that because this trait is implemented for all integer types with multiple right-hand-side types, Rust’s type checker has special handling for _ << _, setting the result type for integer operations to the type of the left-hand-side operand. This means that though a << b and a.shl(b) are one and the same from an evaluation standpoint, they are different when it comes to type inference.
Shr: The right shift operator >>. Note that because this trait is implemented for all integer types with multiple right-hand-side types, Rust’s type checker has special handling for _ >> _, setting the result type for integer operations to the type of the left-hand-side operand. This means that though a >> b and a.shr(b) are one and the same from an evaluation standpoint, they are different when it comes to type inference.
SquareRoot: A type operator for taking the integer square root of Self.
Sub: The subtraction operator -.
ToInt: A type operator for taking a concrete integer value from a type.
TypeArray: The marker trait for type-level arrays of type-level numbers.
Unsigned: The marker trait for compile time unsigned integers.
Zero: A marker trait to designate that a type is zero. Only B0, U0, and Z0 implement this trait.

Type Aliases§

AbsVal: Alias for the associated type of Abs: AbsVal<A> = <A as Abs>::Output
Add1: Alias to make it easy to add 1: Add1<A> = <A as Add<B1>>::Output
And: Alias for the associated type of BitAnd: And<A, B> = <A as BitAnd>::Output
Compare: Alias for the associated type of Cmp: Compare<A, B> = <A as Cmp>::Output
Cube: Alias to make it easy to cube. Cube<A> = <Square<A> as Mul<A>>::Output
Diff: Alias for the associated type of Sub: Diff<A, B> = <A as Sub>::Output
Double: Alias to make it easy to multiply by 2. Double<A> = Shleft<A, B1>
Eq: Alias for the associated type of IsEqual: Eq<A, B> = <A as IsEqual>::Output
Exp: Alias for the associated type of Pow: Exp<A, B> = <A as Pow>::Output
False
FoldProd: Alias for the associated type of FoldMul: FoldProd<A> = <A as FoldMul>::Output
FoldSum: Alias for the associated type of FoldAdd: FoldSum<A> = <A as FoldAdd>::Output
Gcf: Alias for the associated type of Gcd: Gcf<A, B> = <A as Gcd>::Output>
Gr: Alias for the associated type of IsGreater: Gr<A, B> = <A as IsGreater>::Output
GrEq: Alias for the associated type of IsGreaterOrEqual: GrEq<A, B> = <A as IsGreaterOrEqual>::Output
Le: Alias for the associated type of IsLess: Le<A, B> = <A as IsLess>::Output
LeEq: Alias for the associated type of IsLessOrEqual: LeEq<A, B> = <A as IsLessOrEqual>::Output
Length: Alias for the associated type of Len: Length<A> = <A as Len>::Output
Log2: Alias for the associated type of Logarithm2: Log2<A> = <A as Logarithm2>::Output
Maximum: Alias for the associated type of Max: Maximum<A, B> = <A as Max>::Output
Minimum: Alias for the associated type of Min: Minimum<A, B> = <A as Min>::Output
Mod: Alias for the associated type of Rem: Mod<A, B> = <A as Rem>::Output
N1
N2
N3
N4
N5
N6
N7
N8
N9
N10
N11
N12
N13
N14
N15
N16
N17
N18
N19
N20
N21
N22
N23
N24
N25
N26
N27
N28
N29
N30
N31
N32
N33
N34
N35
N36
N37
N38
N39
N40
N41
N42
N43
N44
N45
N46
N47
N48
N49
N50
N51
N52
N53
N54
N55
N56
N57
N58
N59
N60
N61
N62
N63
N64
N65
N66
N67
N68
N69
N70
N71
N72
N73
N74
N75
N76
N77
N78
N79
N80
N81
N82
N83
N84
N85
N86
N87
N88
N89
N90
N91
N92
N93
N94
N95
N96
N97
N98
N99
N100
N101
N102
N103
N104
N105
N106
N107
N108
N109
N110
N111
N112
N113
N114
N115
N116
N117
N118
N119
N120
N121
N122
N123
N124
N125
N126
N127
N128
N129
N130
N131
N132
N133
N134
N135
N136
N137
N138
N139
N140
N141
N142
N143
N144
N145
N146
N147
N148
N149
N150
N151
N152
N153
N154
N155
N156
N157
N158
N159
N160
N161
N162
N163
N164
N165
N166
N167
N168
N169
N170
N171
N172
N173
N174
N175
N176
N177
N178
N179
N180
N181
N182
N183
N184
N185
N186
N187
N188
N189
N190
N191
N192
N193
N194
N195
N196
N197
N198
N199
N200
N201
N202
N203
N204
N205
N206
N207
N208
N209
N210
N211
N212
N213
N214
N215
N216
N217
N218
N219
N220
N221
N222
N223
N224
N225
N226
N227
N228
N229
N230
N231
N232
N233
N234
N235
N236
N237
N238
N239
N240
N241
N242
N243
N244
N245
N246
N247
N248
N249
N250
N251
N252
N253
N254
N255
N256
N257
N258
N259
N260
N261
N262
N263
N264
N265
N266
N267
N268
N269
N270
N271
N272
N273
N274
N275
N276
N277
N278
N279
N280
N281
N282
N283
N284
N285
N286
N287
N288
N289
N290
N291
N292
N293
N294
N295
N296
N297
N298
N299
N300
N301
N302
N303
N304
N305
N306
N307
N308
N309
N310
N311
N312
N313
N314
N315
N316
N317
N318
N319
N320
N321
N322
N323
N324
N325
N326
N327
N328
N329
N330
N331
N332
N333
N334
N335
N336
N337
N338
N339
N340
N341
N342
N343
N344
N345
N346
N347
N348
N349
N350
N351
N352
N353
N354
N355
N356
N357
N358
N359
N360
N361
N362
N363
N364
N365
N366
N367
N368
N369
N370
N371
N372
N373
N374
N375
N376
N377
N378
N379
N380
N381
N382
N383
N384
N385
N386
N387
N388
N389
N390
N391
N392
N393
N394
N395
N396
N397
N398
N399
N400
N401
N402
N403
N404
N405
N406
N407
N408
N409
N410
N411
N412
N413
N414
N415
N416
N417
N418
N419
N420
N421
N422
N423
N424
N425
N426
N427
N428
N429
N430
N431
N432
N433
N434
N435
N436
N437
N438
N439
N440
N441
N442
N443
N444
N445
N446
N447
N448
N449
N450
N451
N452
N453
N454
N455
N456
N457
N458
N459
N460
N461
N462
N463
N464
N465
N466
N467
N468
N469
N470
N471
N472
N473
N474
N475
N476
N477
N478
N479
N480
N481
N482
N483
N484
N485
N486
N487
N488
N489
N490
N491
N492
N493
N494
N495
N496
N497
N498
N499
N500
N501
N502
N503
N504
N505
N506
N507
N508
N509
N510
N511
N512
N513
N514
N515
N516
N517
N518
N519
N520
N521
N522
N523
N524
N525
N526
N527
N528
N529
N530
N531
N532
N533
N534
N535
N536
N537
N538
N539
N540
N541
N542
N543
N544
N545
N546
N547
N548
N549
N550
N551
N552
N553
N554
N555
N556
N557
N558
N559
N560
N561
N562
N563
N564
N565
N566
N567
N568
N569
N570
N571
N572
N573
N574
N575
N576
N577
N578
N579
N580
N581
N582
N583
N584
N585
N586
N587
N588
N589
N590
N591
N592
N593
N594
N595
N596
N597
N598
N599
N600
N601
N602
N603
N604
N605
N606
N607
N608
N609
N610
N611
N612
N613
N614
N615
N616
N617
N618
N619
N620
N621
N622
N623
N624
N625
N626
N627
N628
N629
N630
N631
N632
N633
N634
N635
N636
N637
N638
N639
N640
N641
N642
N643
N644
N645
N646
N647
N648
N649
N650
N651
N652
N653
N654
N655
N656
N657
N658
N659
N660
N661
N662
N663
N664
N665
N666
N667
N668
N669
N670
N671
N672
N673
N674
N675
N676
N677
N678
N679
N680
N681
N682
N683
N684
N685
N686
N687
N688
N689
N690
N691
N692
N693
N694
N695
N696
N697
N698
N699
N700
N701
N702
N703
N704
N705
N706
N707
N708
N709
N710
N711
N712
N713
N714
N715
N716
N717
N718
N719
N720
N721
N722
N723
N724
N725
N726
N727
N728
N729
N730
N731
N732
N733
N734
N735
N736
N737
N738
N739
N740
N741
N742
N743
N744
N745
N746
N747
N748
N749
N750
N751
N752
N753
N754
N755
N756
N757
N758
N759
N760
N761
N762
N763
N764
N765
N766
N767
N768
N769
N770
N771
N772
N773
N774
N775
N776
N777
N778
N779
N780
N781
N782
N783
N784
N785
N786
N787
N788
N789
N790
N791
N792
N793
N794
N795
N796
N797
N798
N799
N800
N801
N802
N803
N804
N805
N806
N807
N808
N809
N810
N811
N812
N813
N814
N815
N816
N817
N818
N819
N820
N821
N822
N823
N824
N825
N826
N827
N828
N829
N830
N831
N832
N833
N834
N835
N836
N837
N838
N839
N840
N841
N842
N843
N844
N845
N846
N847
N848
N849
N850
N851
N852
N853
N854
N855
N856
N857
N858
N859
N860
N861
N862
N863
N864
N865
N866
N867
N868
N869
N870
N871
N872
N873
N874
N875
N876
N877
N878
N879
N880
N881
N882
N883
N884
N885
N886
N887
N888
N889
N890
N891
N892
N893
N894
N895
N896
N897
N898
N899
N900
N901
N902
N903
N904
N905
N906
N907
N908
N909
N910
N911
N912
N913
N914
N915
N916
N917
N918
N919
N920
N921
N922
N923
N924
N925
N926
N927
N928
N929
N930
N931
N932
N933
N934
N935
N936
N937
N938
N939
N940
N941
N942
N943
N944
N945
N946
N947
N948
N949
N950
N951
N952
N953
N954
N955
N956
N957
N958
N959
N960
N961
N962
N963
N964
N965
N966
N967
N968
N969
N970
N971
N972
N973
N974
N975
N976
N977
N978
N979
N980
N981
N982
N983
N984
N985
N986
N987
N988
N989
N990
N991
N992
N993
N994
N995
N996
N997
N998
N999
N1000
N1001
N1002
N1003
N1004
N1005
N1006
N1007
N1008
N1009
N1010
N1011
N1012
N1013
N1014
N1015
N1016
N1017
N1018
N1019
N1020
N1021
N1022
N1023
N1024
N2048
N3600
N4096
N8192
N10000
N16384
N32768
N65536
N100000
N131072
N262144
N524288
N1000000
N1048576
N2097152
N4194304
N8388608
N10000000
N16777216
N33554432
N67108864
N100000000
N134217728
N268435456
N536870912
N1000000000
N1073741824
N2147483648
N4294967296
N8589934592
N10000000000
N17179869184
N34359738368
N68719476736
N100000000000
N137438953472
N274877906944
N549755813888
N1000000000000
N1099511627776
N2199023255552
N4398046511104
N8796093022208
N10000000000000
N17592186044416
N35184372088832
N70368744177664
N100000000000000
N140737488355328
N281474976710656
N562949953421312
N1000000000000000
N1125899906842624
N2251799813685248
N4503599627370496
N9007199254740992
N10000000000000000
N18014398509481984
N36028797018963968
N72057594037927936
N100000000000000000
N144115188075855872
N288230376151711744
N576460752303423488
N1000000000000000000
N1152921504606846976
N2305843009213693952
N4611686018427387904
Negate: Alias for the associated type of Neg: Negate<A> = <A as Neg>::Output
NotEq: Alias for the associated type of IsNotEqual: NotEq<A, B> = <A as IsNotEqual>::Output
Or: Alias for the associated type of BitOr: Or<A, B> = <A as BitOr>::Output
P1
P2
P3
P4
P5
P6
P7
P8
P9
P10
P11
P12
P13
P14
P15
P16
P17
P18
P19
P20
P21
P22
P23
P24
P25
P26
P27
P28
P29
P30
P31
P32
P33
P34
P35
P36
P37
P38
P39
P40
P41
P42
P43
P44
P45
P46
P47
P48
P49
P50
P51
P52
P53
P54
P55
P56
P57
P58
P59
P60
P61
P62
P63
P64
P65
P66
P67
P68
P69
P70
P71
P72
P73
P74
P75
P76
P77
P78
P79
P80
P81
P82
P83
P84
P85
P86
P87
P88
P89
P90
P91
P92
P93
P94
P95
P96
P97
P98
P99
P100
P101
P102
P103
P104
P105
P106
P107
P108
P109
P110
P111
P112
P113
P114
P115
P116
P117
P118
P119
P120
P121
P122
P123
P124
P125
P126
P127
P128
P129
P130
P131
P132
P133
P134
P135
P136
P137
P138
P139
P140
P141
P142
P143
P144
P145
P146
P147
P148
P149
P150
P151
P152
P153
P154
P155
P156
P157
P158
P159
P160
P161
P162
P163
P164
P165
P166
P167
P168
P169
P170
P171
P172
P173
P174
P175
P176
P177
P178
P179
P180
P181
P182
P183
P184
P185
P186
P187
P188
P189
P190
P191
P192
P193
P194
P195
P196
P197
P198
P199
P200
P201
P202
P203
P204
P205
P206
P207
P208
P209
P210
P211
P212
P213
P214
P215
P216
P217
P218
P219
P220
P221
P222
P223
P224
P225
P226
P227
P228
P229
P230
P231
P232
P233
P234
P235
P236
P237
P238
P239
P240
P241
P242
P243
P244
P245
P246
P247
P248
P249
P250
P251
P252
P253
P254
P255
P256
P257
P258
P259
P260
P261
P262
P263
P264
P265
P266
P267
P268
P269
P270
P271
P272
P273
P274
P275
P276
P277
P278
P279
P280
P281
P282
P283
P284
P285
P286
P287
P288
P289
P290
P291
P292
P293
P294
P295
P296
P297
P298
P299
P300
P301
P302
P303
P304
P305
P306
P307
P308
P309
P310
P311
P312
P313
P314
P315
P316
P317
P318
P319
P320
P321
P322
P323
P324
P325
P326
P327
P328
P329
P330
P331
P332
P333
P334
P335
P336
P337
P338
P339
P340
P341
P342
P343
P344
P345
P346
P347
P348
P349
P350
P351
P352
P353
P354
P355
P356
P357
P358
P359
P360
P361
P362
P363
P364
P365
P366
P367
P368
P369
P370
P371
P372
P373
P374
P375
P376
P377
P378
P379
P380
P381
P382
P383
P384
P385
P386
P387
P388
P389
P390
P391
P392
P393
P394
P395
P396
P397
P398
P399
P400
P401
P402
P403
P404
P405
P406
P407
P408
P409
P410
P411
P412
P413
P414
P415
P416
P417
P418
P419
P420
P421
P422
P423
P424
P425
P426
P427
P428
P429
P430
P431
P432
P433
P434
P435
P436
P437
P438
P439
P440
P441
P442
P443
P444
P445
P446
P447
P448
P449
P450
P451
P452
P453
P454
P455
P456
P457
P458
P459
P460
P461
P462
P463
P464
P465
P466
P467
P468
P469
P470
P471
P472
P473
P474
P475
P476
P477
P478
P479
P480
P481
P482
P483
P484
P485
P486
P487
P488
P489
P490
P491
P492
P493
P494
P495
P496
P497
P498
P499
P500
P501
P502
P503
P504
P505
P506
P507
P508
P509
P510
P511
P512
P513
P514
P515
P516
P517
P518
P519
P520
P521
P522
P523
P524
P525
P526
P527
P528
P529
P530
P531
P532
P533
P534
P535
P536
P537
P538
P539
P540
P541
P542
P543
P544
P545
P546
P547
P548
P549
P550
P551
P552
P553
P554
P555
P556
P557
P558
P559
P560
P561
P562
P563
P564
P565
P566
P567
P568
P569
P570
P571
P572
P573
P574
P575
P576
P577
P578
P579
P580
P581
P582
P583
P584
P585
P586
P587
P588
P589
P590
P591
P592
P593
P594
P595
P596
P597
P598
P599
P600
P601
P602
P603
P604
P605
P606
P607
P608
P609
P610
P611
P612
P613
P614
P615
P616
P617
P618
P619
P620
P621
P622
P623
P624
P625
P626
P627
P628
P629
P630
P631
P632
P633
P634
P635
P636
P637
P638
P639
P640
P641
P642
P643
P644
P645
P646
P647
P648
P649
P650
P651
P652
P653
P654
P655
P656
P657
P658
P659
P660
P661
P662
P663
P664
P665
P666
P667
P668
P669
P670
P671
P672
P673
P674
P675
P676
P677
P678
P679
P680
P681
P682
P683
P684
P685
P686
P687
P688
P689
P690
P691
P692
P693
P694
P695
P696
P697
P698
P699
P700
P701
P702
P703
P704
P705
P706
P707
P708
P709
P710
P711
P712
P713
P714
P715
P716
P717
P718
P719
P720
P721
P722
P723
P724
P725
P726
P727
P728
P729
P730
P731
P732
P733
P734
P735
P736
P737
P738
P739
P740
P741
P742
P743
P744
P745
P746
P747
P748
P749
P750
P751
P752
P753
P754
P755
P756
P757
P758
P759
P760
P761
P762
P763
P764
P765
P766
P767
P768
P769
P770
P771
P772
P773
P774
P775
P776
P777
P778
P779
P780
P781
P782
P783
P784
P785
P786
P787
P788
P789
P790
P791
P792
P793
P794
P795
P796
P797
P798
P799
P800
P801
P802
P803
P804
P805
P806
P807
P808
P809
P810
P811
P812
P813
P814
P815
P816
P817
P818
P819
P820
P821
P822
P823
P824
P825
P826
P827
P828
P829
P830
P831
P832
P833
P834
P835
P836
P837
P838
P839
P840
P841
P842
P843
P844
P845
P846
P847
P848
P849
P850
P851
P852
P853
P854
P855
P856
P857
P858
P859
P860
P861
P862
P863
P864
P865
P866
P867
P868
P869
P870
P871
P872
P873
P874
P875
P876
P877
P878
P879
P880
P881
P882
P883
P884
P885
P886
P887
P888
P889
P890
P891
P892
P893
P894
P895
P896
P897
P898
P899
P900
P901
P902
P903
P904
P905
P906
P907
P908
P909
P910
P911
P912
P913
P914
P915
P916
P917
P918
P919
P920
P921
P922
P923
P924
P925
P926
P927
P928
P929
P930
P931
P932
P933
P934
P935
P936
P937
P938
P939
P940
P941
P942
P943
P944
P945
P946
P947
P948
P949
P950
P951
P952
P953
P954
P955
P956
P957
P958
P959
P960
P961
P962
P963
P964
P965
P966
P967
P968
P969
P970
P971
P972
P973
P974
P975
P976
P977
P978
P979
P980
P981
P982
P983
P984
P985
P986
P987
P988
P989
P990
P991
P992
P993
P994
P995
P996
P997
P998
P999
P1000
P1001
P1002
P1003
P1004
P1005
P1006
P1007
P1008
P1009
P1010
P1011
P1012
P1013
P1014
P1015
P1016
P1017
P1018
P1019
P1020
P1021
P1022
P1023
P1024
P2048
P3600
P4096
P8192
P10000
P16384
P32768
P65536
P100000
P131072
P262144
P524288
P1000000
P1048576
P2097152
P4194304
P8388608
P10000000
P16777216
P33554432
P67108864
P100000000
P134217728
P268435456
P536870912
P1000000000
P1073741824
P2147483648
P4294967296
P8589934592
P10000000000
P17179869184
P34359738368
P68719476736
P100000000000
P137438953472
P274877906944
P549755813888
P1000000000000
P1099511627776
P2199023255552
P4398046511104
P8796093022208
P10000000000000
P17592186044416
P35184372088832
P70368744177664
P100000000000000
P140737488355328
P281474976710656
P562949953421312
P1000000000000000
P1125899906842624
P2251799813685248
P4503599627370496
P9007199254740992
P10000000000000000
P18014398509481984
P36028797018963968
P72057594037927936
P100000000000000000
P144115188075855872
P288230376151711744
P576460752303423488
P1000000000000000000
P1152921504606846976
P2305843009213693952
P4611686018427387904
PartialQuot: Alias for the associated type of PartialDiv: PartialQuot<A, B> = <A as PartialDiv>::Output
Prod: Alias for the associated type of Mul: Prod<A, B> = <A as Mul>::Output
Quot: Alias for the associated type of Div: Quot<A, B> = <A as Div>::Output
Shleft: Alias for the associated type of Shl: Shleft<A, B> = <A as Shl>::Output
Shright: Alias for the associated type of Shr: Shright<A, B> = <A as Shr>::Output
Sqrt: Alias for the associated type of SquareRoot: Sqrt<A> = <A as SquareRoot>::Output
Square: Alias to make it easy to square. Square<A> = <A as Mul<A>>::Output
Sub1: Alias to make it easy to subtract 1: Sub1<A> = <A as Sub<B1>>::Output
Sum: Alias for the associated type of Add: Sum<A, B> = <A as Add>::Output
True
U0
U1
U2
U3
U4
U5
U6
U7
U8
U9
U10
U11
U12
U13
U14
U15
U16
U17
U18
U19
U20
U21
U22
U23
U24
U25
U26
U27
U28
U29
U30
U31
U32
U33
U34
U35
U36
U37
U38
U39
U40
U41
U42
U43
U44
U45
U46
U47
U48
U49
U50
U51
U52
U53
U54
U55
U56
U57
U58
U59
U60
U61
U62
U63
U64
U65
U66
U67
U68
U69
U70
U71
U72
U73
U74
U75
U76
U77
U78
U79
U80
U81
U82
U83
U84
U85
U86
U87
U88
U89
U90
U91
U92
U93
U94
U95
U96
U97
U98
U99
U100
U101
U102
U103
U104
U105
U106
U107
U108
U109
U110
U111
U112
U113
U114
U115
U116
U117
U118
U119
U120
U121
U122
U123
U124
U125
U126
U127
U128
U129
U130
U131
U132
U133
U134
U135
U136
U137
U138
U139
U140
U141
U142
U143
U144
U145
U146
U147
U148
U149
U150
U151
U152
U153
U154
U155
U156
U157
U158
U159
U160
U161
U162
U163
U164
U165
U166
U167
U168
U169
U170
U171
U172
U173
U174
U175
U176
U177
U178
U179
U180
U181
U182
U183
U184
U185
U186
U187
U188
U189
U190
U191
U192
U193
U194
U195
U196
U197
U198
U199
U200
U201
U202
U203
U204
U205
U206
U207
U208
U209
U210
U211
U212
U213
U214
U215
U216
U217
U218
U219
U220
U221
U222
U223
U224
U225
U226
U227
U228
U229
U230
U231
U232
U233
U234
U235
U236
U237
U238
U239
U240
U241
U242
U243
U244
U245
U246
U247
U248
U249
U250
U251
U252
U253
U254
U255
U256
U257
U258
U259
U260
U261
U262
U263
U264
U265
U266
U267
U268
U269
U270
U271
U272
U273
U274
U275
U276
U277
U278
U279
U280
U281
U282
U283
U284
U285
U286
U287
U288
U289
U290
U291
U292
U293
U294
U295
U296
U297
U298
U299
U300
U301
U302
U303
U304
U305
U306
U307
U308
U309
U310
U311
U312
U313
U314
U315
U316
U317
U318
U319
U320
U321
U322
U323
U324
U325
U326
U327
U328
U329
U330
U331
U332
U333
U334
U335
U336
U337
U338
U339
U340
U341
U342
U343
U344
U345
U346
U347
U348
U349
U350
U351
U352
U353
U354
U355
U356
U357
U358
U359
U360
U361
U362
U363
U364
U365
U366
U367
U368
U369
U370
U371
U372
U373
U374
U375
U376
U377
U378
U379
U380
U381
U382
U383
U384
U385
U386
U387
U388
U389
U390
U391
U392
U393
U394
U395
U396
U397
U398
U399
U400
U401
U402
U403
U404
U405
U406
U407
U408
U409
U410
U411
U412
U413
U414
U415
U416
U417
U418
U419
U420
U421
U422
U423
U424
U425
U426
U427
U428
U429
U430
U431
U432
U433
U434
U435
U436
U437
U438
U439
U440
U441
U442
U443
U444
U445
U446
U447
U448
U449
U450
U451
U452
U453
U454
U455
U456
U457
U458
U459
U460
U461
U462
U463
U464
U465
U466
U467
U468
U469
U470
U471
U472
U473
U474
U475
U476
U477
U478
U479
U480
U481
U482
U483
U484
U485
U486
U487
U488
U489
U490
U491
U492
U493
U494
U495
U496
U497
U498
U499
U500
U501
U502
U503
U504
U505
U506
U507
U508
U509
U510
U511
U512
U513
U514
U515
U516
U517
U518
U519
U520
U521
U522
U523
U524
U525
U526
U527
U528
U529
U530
U531
U532
U533
U534
U535
U536
U537
U538
U539
U540
U541
U542
U543
U544
U545
U546
U547
U548
U549
U550
U551
U552
U553
U554
U555
U556
U557
U558
U559
U560
U561
U562
U563
U564
U565
U566
U567
U568
U569
U570
U571
U572
U573
U574
U575
U576
U577
U578
U579
U580
U581
U582
U583
U584
U585
U586
U587
U588
U589
U590
U591
U592
U593
U594
U595
U596
U597
U598
U599
U600
U601
U602
U603
U604
U605
U606
U607
U608
U609
U610
U611
U612
U613
U614
U615
U616
U617
U618
U619
U620
U621
U622
U623
U624
U625
U626
U627
U628
U629
U630
U631
U632
U633
U634
U635
U636
U637
U638
U639
U640
U641
U642
U643
U644
U645
U646
U647
U648
U649
U650
U651
U652
U653
U654
U655
U656
U657
U658
U659
U660
U661
U662
U663
U664
U665
U666
U667
U668
U669
U670
U671
U672
U673
U674
U675
U676
U677
U678
U679
U680
U681
U682
U683
U684
U685
U686
U687
U688
U689
U690
U691
U692
U693
U694
U695
U696
U697
U698
U699
U700
U701
U702
U703
U704
U705
U706
U707
U708
U709
U710
U711
U712
U713
U714
U715
U716
U717
U718
U719
U720
U721
U722
U723
U724
U725
U726
U727
U728
U729
U730
U731
U732
U733
U734
U735
U736
U737
U738
U739
U740
U741
U742
U743
U744
U745
U746
U747
U748
U749
U750
U751
U752
U753
U754
U755
U756
U757
U758
U759
U760
U761
U762
U763
U764
U765
U766
U767
U768
U769
U770
U771
U772
U773
U774
U775
U776
U777
U778
U779
U780
U781
U782
U783
U784
U785
U786
U787
U788
U789
U790
U791
U792
U793
U794
U795
U796
U797
U798
U799
U800
U801
U802
U803
U804
U805
U806
U807
U808
U809
U810
U811
U812
U813
U814
U815
U816
U817
U818
U819
U820
U821
U822
U823
U824
U825
U826
U827
U828
U829
U830
U831
U832
U833
U834
U835
U836
U837
U838
U839
U840
U841
U842
U843
U844
U845
U846
U847
U848
U849
U850
U851
U852
U853
U854
U855
U856
U857
U858
U859
U860
U861
U862
U863
U864
U865
U866
U867
U868
U869
U870
U871
U872
U873
U874
U875
U876
U877
U878
U879
U880
U881
U882
U883
U884
U885
U886
U887
U888
U889
U890
U891
U892
U893
U894
U895
U896
U897
U898
U899
U900
U901
U902
U903
U904
U905
U906
U907
U908
U909
U910
U911
U912
U913
U914
U915
U916
U917
U918
U919
U920
U921
U922
U923
U924
U925
U926
U927
U928
U929
U930
U931
U932
U933
U934
U935
U936
U937
U938
U939
U940
U941
U942
U943
U944
U945
U946
U947
U948
U949
U950
U951
U952
U953
U954
U955
U956
U957
U958
U959
U960
U961
U962
U963
U964
U965
U966
U967
U968
U969
U970
U971
U972
U973
U974
U975
U976
U977
U978
U979
U980
U981
U982
U983
U984
U985
U986
U987
U988
U989
U990
U991
U992
U993
U994
U995
U996
U997
U998
U999
U1000
U1001
U1002
U1003
U1004
U1005
U1006
U1007
U1008
U1009
U1010
U1011
U1012
U1013
U1014
U1015
U1016
U1017
U1018
U1019
U1020
U1021
U1022
U1023
U1024
U2048
U3600
U4096
U8192
U10000
U16384
U32768
U65536
U100000
U131072
U262144
U524288
U1000000
U1048576
U2097152
U4194304
U8388608
U10000000
U16777216
U33554432
U67108864
U100000000
U134217728
U268435456
U536870912
U1000000000
U1073741824
U2147483648
U4294967296
U8589934592
U10000000000
U17179869184
U34359738368
U68719476736
U100000000000
U137438953472
U274877906944
U549755813888
U1000000000000
U1099511627776
U2199023255552
U4398046511104
U8796093022208
U10000000000000
U17592186044416
U35184372088832
U70368744177664
U100000000000000
U140737488355328
U281474976710656
U562949953421312
U1000000000000000
U1125899906842624
U2251799813685248
U4503599627370496
U9007199254740992
U10000000000000000
U18014398509481984
U36028797018963968
U72057594037927936
U100000000000000000
U144115188075855872
U288230376151711744
U576460752303423488
U1000000000000000000
U1152921504606846976
U2305843009213693952
U4611686018427387904
U9223372036854775808
U10000000000000000000
Xor: Alias for the associated type of BitXor: Xor<A, B> = <A as BitXor>::Output

Attribute Macros§

verify

Crate verifiedCopy item path