22
33//! Correctness/Soundness type properties
44
5- use super :: { ErrorKind , Property } ;
6- use crate :: ScriptContext ;
5+ use super :: ErrorKind ;
76
87/// Basic type representing where the fragment can go
98#[ derive( Copy , Clone , PartialEq , Eq , PartialOrd , Ord , Debug , Hash ) ]
@@ -47,12 +46,24 @@ pub enum Input {
4746}
4847
4948impl Input {
49+ // FIXME rustc should eventually support derived == on enums in constfns
50+ const fn constfn_eq ( self , other : Self ) -> bool {
51+ matches ! (
52+ ( self , other) ,
53+ ( Input :: Zero , Input :: Zero )
54+ | ( Input :: One , Input :: One )
55+ | ( Input :: Any , Input :: Any )
56+ | ( Input :: OneNonZero , Input :: OneNonZero )
57+ | ( Input :: AnyNonZero , Input :: AnyNonZero )
58+ )
59+ }
60+
5061 /// Check whether given `Input` is a subtype of `other`. That is,
5162 /// if some Input is `OneNonZero` then it must be `One`, hence `OneNonZero` is
5263 /// a subtype if `One`. Returns `true` for `a.is_subtype(a)`.
53- fn is_subtype ( & self , other : Self ) -> bool {
64+ const fn is_subtype ( & self , other : Self ) -> bool {
5465 match ( * self , other) {
55- ( x, y) if x == y => true ,
66+ ( x, y) if x. constfn_eq ( y ) => true ,
5667 ( Input :: OneNonZero , Input :: One )
5768 | ( Input :: OneNonZero , Input :: AnyNonZero )
5869 | ( _, Input :: Any ) => true ,
@@ -95,16 +106,15 @@ impl Correctness {
95106 /// This checks whether the argument `other` has attributes which are present
96107 /// in the given `Type`. This returns `true` on same arguments
97108 /// `a.is_subtype(a)` is `true`.
98- pub fn is_subtype ( & self , other : Self ) -> bool {
99- self . base == other. base
109+ pub const fn is_subtype ( & self , other : Self ) -> bool {
110+ self . base as u8 == other. base as u8
100111 && self . input . is_subtype ( other. input )
101112 && self . dissatisfiable >= other. dissatisfiable
102113 && self . unit >= other. unit
103114 }
104- }
105115
106- impl Property for Correctness {
107- fn sanity_checks ( & self ) {
116+ /// Confirm invariants of the correctness checker.
117+ pub fn sanity_checks ( & self ) {
108118 match self . base {
109119 Base :: B => { }
110120 Base :: K => {
@@ -115,21 +125,19 @@ impl Property for Correctness {
115125 debug_assert ! ( !self . dissatisfiable) ;
116126 }
117127 Base :: W => {
118- debug_assert ! ( self . input != Input :: OneNonZero ) ;
119- debug_assert ! ( self . input != Input :: AnyNonZero ) ;
128+ debug_assert ! ( ! self . input. constfn_eq ( Input :: OneNonZero ) ) ;
129+ debug_assert ! ( ! self . input. constfn_eq ( Input :: AnyNonZero ) ) ;
120130 }
121131 }
122132 }
123133
124- fn from_true ( ) -> Self { Self :: TRUE }
125-
126- fn from_false ( ) -> Self { Self :: FALSE }
127-
128- fn from_pk_k < Ctx : ScriptContext > ( ) -> Self {
134+ /// Constructor for the correctness properties of the `pk_k` fragment.
135+ pub const fn pk_k ( ) -> Self {
129136 Correctness { base : Base :: K , input : Input :: OneNonZero , dissatisfiable : true , unit : true }
130137 }
131138
132- fn from_pk_h < Ctx : ScriptContext > ( ) -> Self {
139+ /// Constructor for the correctness properties of the `pk_h` fragment.
140+ pub const fn pk_h ( ) -> Self {
133141 Correctness {
134142 base : Base :: K ,
135143 input : Input :: AnyNonZero ,
@@ -138,23 +146,28 @@ impl Property for Correctness {
138146 }
139147 }
140148
141- fn from_multi ( _: usize , _: usize ) -> Self {
149+ /// Constructor for the correctness properties of the `multi` fragment.
150+ pub const fn multi ( ) -> Self {
142151 Correctness { base : Base :: B , input : Input :: AnyNonZero , dissatisfiable : true , unit : true }
143152 }
144153
145- fn from_multi_a ( _: usize , _: usize ) -> Self {
154+ /// Constructor for the correctness properties of the `multi_a` fragment.
155+ pub const fn multi_a ( ) -> Self {
146156 Correctness { base : Base :: B , input : Input :: Any , dissatisfiable : true , unit : true }
147157 }
148158
149- fn from_hash ( ) -> Self {
159+ /// Constructor for the correctness properties of any of the hash fragments.
160+ pub const fn hash ( ) -> Self {
150161 Correctness { base : Base :: B , input : Input :: OneNonZero , dissatisfiable : true , unit : true }
151162 }
152163
153- fn from_time ( _: u32 ) -> Self {
164+ /// Constructor for the correctness properties of either of the time fragments.
165+ pub const fn time ( ) -> Self {
154166 Correctness { base : Base :: B , input : Input :: Zero , dissatisfiable : false , unit : false }
155167 }
156168
157- fn cast_alt ( self ) -> Result < Self , ErrorKind > {
169+ /// Constructor for the correctness properties of the `a:` fragment.
170+ pub const fn cast_alt ( self ) -> Result < Self , ErrorKind > {
158171 Ok ( Correctness {
159172 base : match self . base {
160173 Base :: B => Base :: W ,
@@ -166,7 +179,8 @@ impl Property for Correctness {
166179 } )
167180 }
168181
169- fn cast_swap ( self ) -> Result < Self , ErrorKind > {
182+ /// Constructor for the correctness properties of the `s:` fragment.
183+ pub const fn cast_swap ( self ) -> Result < Self , ErrorKind > {
170184 Ok ( Correctness {
171185 base : match self . base {
172186 Base :: B => Base :: W ,
@@ -181,7 +195,8 @@ impl Property for Correctness {
181195 } )
182196 }
183197
184- fn cast_check ( self ) -> Result < Self , ErrorKind > {
198+ /// Constructor for the correctness properties of the `c:` fragment.
199+ pub const fn cast_check ( self ) -> Result < Self , ErrorKind > {
185200 Ok ( Correctness {
186201 base : match self . base {
187202 Base :: K => Base :: B ,
@@ -193,7 +208,8 @@ impl Property for Correctness {
193208 } )
194209 }
195210
196- fn cast_dupif ( self ) -> Result < Self , ErrorKind > {
211+ /// Constructor for the correctness properties of the `d:` fragment.
212+ pub const fn cast_dupif ( self ) -> Result < Self , ErrorKind > {
197213 Ok ( Correctness {
198214 base : match self . base {
199215 Base :: V => Base :: B ,
@@ -208,7 +224,8 @@ impl Property for Correctness {
208224 } )
209225 }
210226
211- fn cast_verify ( self ) -> Result < Self , ErrorKind > {
227+ /// Constructor for the correctness properties of the `v:` fragment.
228+ pub const fn cast_verify ( self ) -> Result < Self , ErrorKind > {
212229 Ok ( Correctness {
213230 base : match self . base {
214231 Base :: B => Base :: V ,
@@ -220,8 +237,9 @@ impl Property for Correctness {
220237 } )
221238 }
222239
223- fn cast_nonzero ( self ) -> Result < Self , ErrorKind > {
224- if self . input != Input :: OneNonZero && self . input != Input :: AnyNonZero {
240+ /// Constructor for the correctness properties of the `j:` fragment.
241+ pub const fn cast_nonzero ( self ) -> Result < Self , ErrorKind > {
242+ if !self . input . constfn_eq ( Input :: OneNonZero ) && !self . input . constfn_eq ( Input :: AnyNonZero ) {
225243 return Err ( ErrorKind :: NonZeroZero ) ;
226244 }
227245 Ok ( Correctness {
@@ -235,7 +253,8 @@ impl Property for Correctness {
235253 } )
236254 }
237255
238- fn cast_zeronotequal ( self ) -> Result < Self , ErrorKind > {
256+ /// Constructor for the correctness properties of the `n:` fragment.
257+ pub const fn cast_zeronotequal ( self ) -> Result < Self , ErrorKind > {
239258 Ok ( Correctness {
240259 base : match self . base {
241260 Base :: B => Base :: B ,
@@ -247,7 +266,8 @@ impl Property for Correctness {
247266 } )
248267 }
249268
250- fn cast_true ( self ) -> Result < Self , ErrorKind > {
269+ /// Constructor for the correctness properties of the `t:` fragment.
270+ pub const fn cast_true ( self ) -> Result < Self , ErrorKind > {
251271 Ok ( Correctness {
252272 base : match self . base {
253273 Base :: V => Base :: B ,
@@ -259,7 +279,8 @@ impl Property for Correctness {
259279 } )
260280 }
261281
262- fn cast_or_i_false ( self ) -> Result < Self , ErrorKind > {
282+ /// Constructor for the correctness properties of the `l:` and `u:` fragments.
283+ pub const fn cast_or_i_false ( self ) -> Result < Self , ErrorKind > {
263284 Ok ( Correctness {
264285 base : match self . base {
265286 Base :: B => Base :: B ,
@@ -276,7 +297,8 @@ impl Property for Correctness {
276297 } )
277298 }
278299
279- fn and_b ( left : Self , right : Self ) -> Result < Self , ErrorKind > {
300+ /// Constructor for the correctness properties of the `and_b` fragment
301+ pub const fn and_b ( left : Self , right : Self ) -> Result < Self , ErrorKind > {
280302 Ok ( Correctness {
281303 base : match ( left. base , right. base ) {
282304 ( Base :: B , Base :: W ) => Base :: B ,
@@ -298,7 +320,8 @@ impl Property for Correctness {
298320 } )
299321 }
300322
301- fn and_v ( left : Self , right : Self ) -> Result < Self , ErrorKind > {
323+ /// Constructor for the correctness properties of the `and_v` fragment
324+ pub const fn and_v ( left : Self , right : Self ) -> Result < Self , ErrorKind > {
302325 Ok ( Correctness {
303326 base : match ( left. base , right. base ) {
304327 ( Base :: V , Base :: B ) => Base :: B ,
@@ -322,7 +345,8 @@ impl Property for Correctness {
322345 } )
323346 }
324347
325- fn or_b ( left : Self , right : Self ) -> Result < Self , ErrorKind > {
348+ /// Constructor for the correctness properties of the `or_b` fragment
349+ pub const fn or_b ( left : Self , right : Self ) -> Result < Self , ErrorKind > {
326350 if !left. dissatisfiable {
327351 return Err ( ErrorKind :: LeftNotDissatisfiable ) ;
328352 }
@@ -347,7 +371,8 @@ impl Property for Correctness {
347371 } )
348372 }
349373
350- fn or_d ( left : Self , right : Self ) -> Result < Self , ErrorKind > {
374+ /// Constructor for the correctness properties of the `or_d` fragment
375+ pub const fn or_d ( left : Self , right : Self ) -> Result < Self , ErrorKind > {
351376 if !left. dissatisfiable {
352377 return Err ( ErrorKind :: LeftNotDissatisfiable ) ;
353378 }
@@ -369,7 +394,8 @@ impl Property for Correctness {
369394 } )
370395 }
371396
372- fn or_c ( left : Self , right : Self ) -> Result < Self , ErrorKind > {
397+ /// Constructor for the correctness properties of the `or_c` fragment
398+ pub const fn or_c ( left : Self , right : Self ) -> Result < Self , ErrorKind > {
373399 if !left. dissatisfiable {
374400 return Err ( ErrorKind :: LeftNotDissatisfiable ) ;
375401 }
@@ -391,7 +417,8 @@ impl Property for Correctness {
391417 } )
392418 }
393419
394- fn or_i ( left : Self , right : Self ) -> Result < Self , ErrorKind > {
420+ /// Constructor for the correctness properties of the `or_i` fragment
421+ pub const fn or_i ( left : Self , right : Self ) -> Result < Self , ErrorKind > {
395422 Ok ( Correctness {
396423 base : match ( left. base , right. base ) {
397424 ( Base :: B , Base :: B ) => Base :: B ,
@@ -408,7 +435,8 @@ impl Property for Correctness {
408435 } )
409436 }
410437
411- fn and_or ( a : Self , b : Self , c : Self ) -> Result < Self , ErrorKind > {
438+ /// Constructor for the correctness properties of the `andor` fragment
439+ pub const fn and_or ( a : Self , b : Self , c : Self ) -> Result < Self , ErrorKind > {
412440 if !a. dissatisfiable {
413441 return Err ( ErrorKind :: LeftNotDissatisfiable ) ;
414442 }
@@ -437,7 +465,9 @@ impl Property for Correctness {
437465 } )
438466 }
439467
440- fn threshold < S > ( _k : usize , n : usize , mut sub_ck : S ) -> Result < Self , ErrorKind >
468+ /// Constructor for the correctness properties of the `thresh` fragment
469+ // Cannot be constfn because it takes a closure.
470+ pub fn threshold < S > ( _k : usize , n : usize , mut sub_ck : S ) -> Result < Self , ErrorKind >
441471 where
442472 S : FnMut ( usize ) -> Result < Self , ErrorKind > ,
443473 {
0 commit comments