@@ -32,9 +32,7 @@ impl Field {
32
32
/// (e.g. 254 for the BN254 field) allow for multiple bit decompositions. This is due to how the `Field` will
33
33
/// wrap around due to overflow when verifying the decomposition.
34
34
#[builtin(to_le_bits)]
35
- // docs:start:to_le_bits
36
- pub fn to_le_bits <let N : u32 >(self : Self ) -> [u1 ; N ] {}
37
- // docs:end:to_le_bits
35
+ fn _to_le_bits <let N : u32 >(self : Self ) -> [u1 ; N ] {}
38
36
39
37
/// Decomposes `self` into its big endian bit decomposition as a `[u1; N]` array.
40
38
/// This array will be zero padded should not all bits be necessary to represent `self`.
@@ -48,9 +46,71 @@ impl Field {
48
46
/// (e.g. 254 for the BN254 field) allow for multiple bit decompositions. This is due to how the `Field` will
49
47
/// wrap around due to overflow when verifying the decomposition.
50
48
#[builtin(to_be_bits)]
49
+ fn _to_be_bits <let N : u32 >(self : Self ) -> [u1 ; N ] {}
50
+
51
+ /// Decomposes `self` into its little endian bit decomposition as a `[u1; N]` array.
52
+ /// This slice will be zero padded should not all bits be necessary to represent `self`.
53
+ ///
54
+ /// # Failures
55
+ /// Causes a constraint failure for `Field` values exceeding `2^N` as the resulting slice will not
56
+ /// be able to represent the original `Field`.
57
+ ///
58
+ /// # Safety
59
+ /// The bit decomposition returned is canonical and is guaranteed to not overflow the modulus.
60
+ // docs:start:to_le_bits
61
+ pub fn to_le_bits <let N : u32 >(self : Self ) -> [u1 ; N ] {
62
+ // docs:end:to_le_bits
63
+ let bits = self ._to_le_bits ();
64
+
65
+ if !is_unconstrained () {
66
+ // Ensure that the byte decomposition does not overflow the modulus
67
+ let p = modulus_le_bits ();
68
+ assert (bits .len () <= p .len ());
69
+ let mut ok = bits .len () != p .len ();
70
+ for i in 0 ..N {
71
+ if !ok {
72
+ if (bits [N - 1 - i ] != p [N - 1 - i ]) {
73
+ assert (p [N - 1 - i ] == 1 );
74
+ ok = true ;
75
+ }
76
+ }
77
+ }
78
+ assert (ok );
79
+ }
80
+ bits
81
+ }
82
+
83
+ /// Decomposes `self` into its big endian bit decomposition as a `[u1; N]` array.
84
+ /// This array will be zero padded should not all bits be necessary to represent `self`.
85
+ ///
86
+ /// # Failures
87
+ /// Causes a constraint failure for `Field` values exceeding `2^N` as the resulting slice will not
88
+ /// be able to represent the original `Field`.
89
+ ///
90
+ /// # Safety
91
+ /// The bit decomposition returned is canonical and is guaranteed to not overflow the modulus.
51
92
// docs:start:to_be_bits
52
- pub fn to_be_bits <let N : u32 >(self : Self ) -> [u1 ; N ] {}
53
- // docs:end:to_be_bits
93
+ pub fn to_be_bits <let N : u32 >(self : Self ) -> [u1 ; N ] {
94
+ // docs:end:to_be_bits
95
+ let bits = self ._to_be_bits ();
96
+
97
+ if !is_unconstrained () {
98
+ // Ensure that the decomposition does not overflow the modulus
99
+ let p = modulus_be_bits ();
100
+ assert (bits .len () <= p .len ());
101
+ let mut ok = bits .len () != p .len ();
102
+ for i in 0 ..N {
103
+ if !ok {
104
+ if (bits [i ] != p [i ]) {
105
+ assert (p [i ] == 1 );
106
+ ok = true ;
107
+ }
108
+ }
109
+ }
110
+ assert (ok );
111
+ }
112
+ bits
113
+ }
54
114
55
115
/// Decomposes `self` into its little endian byte decomposition as a `[u8;N]` array
56
116
/// This array will be zero padded should not all bytes be necessary to represent `self`.
0 commit comments