elicitation/verification/types/
integers.rs

1//! Integer contract types.
2
3use super::ValidationError;
4use crate::{ElicitCommunicator, ElicitResult, Elicitation, Prompt};
5use anodized::spec;
6use elicitation_derive::contract_type;
7#[cfg(not(kani))]
8use elicitation_macros::instrumented_impl;
9use schemars::JsonSchema;
10use serde::{Deserialize, Serialize};
11
12// ============================================================================
13// Macro: Default Wrapper Generation for Integer Types
14// ============================================================================
15
16/// Generate a Default wrapper for an integer primitive type.
17///
18/// This macro creates an unconstrained wrapper type that:
19/// - Has Serialize, Deserialize, and JsonSchema derives
20/// - Is marked as elicit-safe for rmcp
21/// - Uses serde deserialization instead of manual parsing
22/// - Provides new/get/into_inner methods
23/// - Implements Prompt and Elicitation traits
24macro_rules! impl_integer_default_wrapper {
25    ($primitive:ty, $wrapper:ident, $min:expr, $max:expr) => {
26        #[doc = concat!("Default wrapper for ", stringify!($primitive), " (unconstrained).")]
27        ///
28        /// Used internally for MCP elicitation of primitive values.
29        /// Provides JsonSchema for client-side validation.
30        #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord, Serialize, Deserialize, JsonSchema)]
31        #[schemars(description = concat!(stringify!($primitive), " value"))]
32        pub struct $wrapper(
33            #[schemars(range(min = $min, max = $max))]
34            $primitive
35        );
36
37        rmcp::elicit_safe!($wrapper);
38
39        impl $wrapper {
40            /// Creates a new wrapper.
41            pub fn new(value: $primitive) -> Self {
42                Self(value)
43            }
44
45            /// Gets the inner value.
46            pub fn get(&self) -> $primitive {
47                self.0
48            }
49
50            /// Unwraps to the inner value.
51            pub fn into_inner(self) -> $primitive {
52                self.0
53            }
54        }
55
56        paste::paste! {
57            crate::default_style!($wrapper => [<$wrapper Style>]);
58
59            impl Prompt for $wrapper {
60                fn prompt() -> Option<&'static str> {
61                    Some(concat!("Please enter a ", stringify!($primitive), ":"))
62                }
63            }
64
65            impl Elicitation for $wrapper {
66                type Style = [<$wrapper Style>];
67
68                #[tracing::instrument(skip(communicator))]
69                async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
70                    // Consult style context for a custom prompt, fall back to default
71                    let prompt = communicator
72                        .style_context()
73                        .prompt_for_type::<$primitive>(
74                            "value",
75                            stringify!($primitive),
76                            &crate::style::PromptContext::new(0, 1),
77                        )?
78                        .unwrap_or_else(|| Self::prompt().unwrap().to_string());
79
80                    tracing::debug!(
81                        prompt = %prompt,
82                        concat!("Eliciting ", stringify!($wrapper))
83                    );
84
85                    let response = communicator.send_prompt(&prompt).await?;
86
87                    // Parse response as integer
88                    let value: $primitive = response.trim().parse().map_err(|e| {
89                        crate::ElicitError::new(crate::ElicitErrorKind::ParseError(
90                            format!("Failed to parse {}: {}", stringify!($primitive), e),
91                        ))
92                    })?;
93
94                    Ok(Self::new(value))
95                }
96
97    fn kani_proof() -> proc_macro2::TokenStream {
98        crate::verification::proof_helpers::kani_integer_default(
99            stringify!($wrapper),
100            stringify!($primitive),
101        )
102    }
103
104    fn verus_proof() -> proc_macro2::TokenStream {
105        crate::verification::proof_helpers::verus_integer_default(
106            stringify!($wrapper),
107            stringify!($primitive),
108        )
109    }
110
111    fn creusot_proof() -> proc_macro2::TokenStream {
112        crate::verification::proof_helpers::creusot_integer_default(
113            stringify!($wrapper),
114            stringify!($primitive),
115        )
116    }
117}
118        }
119    };
120}
121
122// ============================================================================
123// Serde Bridge: Constrained Integer Types
124// ============================================================================
125
126/// Add validated Deserialize + JsonSchema to constrained integer types that
127/// already have a plain `#[derive(Deserialize)]` (I8 variants).
128///
129/// Adds: `impl TryFrom<$prim> for $ty` delegating to `new()`.
130/// Combined with `#[serde(try_from = "$prim")]` on the struct, this makes
131/// Deserialize route through the validated constructor.
132macro_rules! impl_integer_tryfrom {
133    ($ty:ident, $prim:ty) => {
134        impl ::std::convert::TryFrom<$prim> for $ty {
135            type Error = super::ValidationError;
136            #[inline]
137            fn try_from(v: $prim) -> Result<Self, Self::Error> {
138                Self::new(v)
139            }
140        }
141    };
142}
143
144/// Generate Serialize + validated Deserialize + JsonSchema for constrained
145/// integer types that do NOT yet have serde derives.
146///
147/// * `$ty` — the constrained newtype (e.g. `U8Positive`)
148/// * `$prim` — the inner primitive (e.g. `u8`)
149/// * `$description` — human-readable description for JSON schema
150/// * extra JSON schema key/value pairs (e.g. `"minimum": 1`)
151macro_rules! impl_integer_serde_bridge {
152    ($ty:ident, $prim:ty, $description:expr, { $($key:literal: $val:tt),* $(,)? }) => {
153        impl serde::Serialize for $ty {
154            fn serialize<S: serde::Serializer>(&self, s: S) -> Result<S::Ok, S::Error> {
155                self.0.serialize(s)
156            }
157        }
158        impl<'de> serde::Deserialize<'de> for $ty {
159            fn deserialize<D: serde::Deserializer<'de>>(d: D) -> Result<Self, D::Error> {
160                let v = <$prim>::deserialize(d)?;
161                Self::new(v).map_err(serde::de::Error::custom)
162            }
163        }
164        impl schemars::JsonSchema for $ty {
165            fn schema_name() -> ::std::borrow::Cow<'static, str> {
166                stringify!($ty).into()
167            }
168            fn json_schema(_gen: &mut schemars::SchemaGenerator) -> schemars::Schema {
169                schemars::json_schema!({
170                    "type": "integer",
171                    "description": $description,
172                    $($key: $val),*
173                })
174            }
175        }
176    };
177}
178
179/// Generate Serialize + validated Deserialize + JsonSchema for const-generic
180/// Range integer types (e.g. `I8Range<MIN, MAX>`).
181macro_rules! impl_integer_range_serde_bridge {
182    ($ty:ident<$prim:ty>) => {
183        impl<const MIN: $prim, const MAX: $prim> serde::Serialize for $ty<MIN, MAX> {
184            fn serialize<S: serde::Serializer>(&self, s: S) -> Result<S::Ok, S::Error> {
185                self.0.serialize(s)
186            }
187        }
188        impl<'de, const MIN: $prim, const MAX: $prim> serde::Deserialize<'de> for $ty<MIN, MAX> {
189            fn deserialize<D: serde::Deserializer<'de>>(d: D) -> Result<Self, D::Error> {
190                let v = <$prim>::deserialize(d)?;
191                Self::new(v).map_err(serde::de::Error::custom)
192            }
193        }
194        impl<const MIN: $prim, const MAX: $prim> schemars::JsonSchema for $ty<MIN, MAX> {
195            fn schema_name() -> ::std::borrow::Cow<'static, str> {
196                format!(concat!(stringify!($ty), "<{},{}>"), MIN, MAX).into()
197            }
198            fn json_schema(_gen: &mut schemars::SchemaGenerator) -> schemars::Schema {
199                // MIN/MAX as i128/u128 for JSON — the json_schema! macro needs literals,
200                // so we build the schema value manually.
201                let mut obj = serde_json::Map::new();
202                obj.insert("type".into(), serde_json::Value::String("integer".into()));
203                obj.insert("minimum".into(), serde_json::json!(MIN as i128));
204                obj.insert("maximum".into(), serde_json::json!(MAX as i128));
205                schemars::Schema::from(obj)
206            }
207        }
208    };
209}
210
211// ============================================================================
212// Verification Types (Constrained)
213// ============================================================================
214
215/// Contract type for positive i8 values (> 0).
216///
217/// This type validates on construction and can be unwrapped to `i8`.
218///
219/// # Trenchcoat Pattern
220///
221/// ```text
222/// LLM → I8Positive::new(value) → validate → .into_inner() → i8
223///       ^^^^^^^^^^^^^^^^^^^^     ^^^^^^^^   ^^^^^^^^^^^^^   ^^^
224///       Put on coat              Check      Take off coat   Familiar
225/// ```
226///
227/// # Example
228///
229/// ```rust,ignore
230/// // Validation at construction
231/// let positive = I8Positive::new(42)?;
232/// assert_eq!(positive.get(), 42);
233///
234/// // Unwrap to stdlib type
235/// let value: i8 = positive.into_inner();
236/// assert_eq!(value, 42);
237/// ```
238#[contract_type(requires = "value > 0", ensures = "result.get() > 0")]
239#[derive(
240    Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord, Serialize, Deserialize, JsonSchema,
241)]
242#[serde(try_from = "i8")]
243#[schemars(description = "Positive integer value (> 0)")]
244pub struct I8Positive(#[schemars(range(min = 1))] i8);
245
246// Mark as safe for MCP elicitation
247rmcp::elicit_safe!(I8Positive);
248impl_integer_tryfrom!(I8Positive, i8);
249
250#[cfg_attr(not(kani), instrumented_impl)]
251impl I8Positive {
252    /// Creates a new `I8Positive` if the value is positive (> 0).
253    ///
254    /// # Errors
255    ///
256    /// Returns `ValidationError::NotPositive` if value <= 0.
257    #[spec(requires: [value > 0])]
258    pub fn new(value: i8) -> Result<Self, ValidationError> {
259        if value > 0 {
260            Ok(Self(value))
261        } else {
262            Err(ValidationError::NotPositive(value as i128))
263        }
264    }
265
266    /// Gets the inner value.
267    pub fn get(&self) -> i8 {
268        self.0
269    }
270
271    /// Unwraps to the inner `i8` (trenchcoat pattern: take off coat).
272    ///
273    /// This is the "output boundary" of the trenchcoat pattern.
274    pub fn into_inner(self) -> i8 {
275        self.0
276    }
277}
278
279// Generate default-only style enum for I8Positive
280crate::default_style!(I8Positive => I8PositiveStyle);
281
282#[cfg_attr(not(kani), instrumented_impl)]
283impl Prompt for I8Positive {
284    fn prompt() -> Option<&'static str> {
285        Some("Please enter a positive number (> 0):")
286    }
287}
288
289#[cfg_attr(not(kani), instrumented_impl)]
290impl Elicitation for I8Positive {
291    type Style = I8PositiveStyle;
292
293    #[tracing::instrument(skip(communicator), fields(type_name = "I8Positive"))]
294    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
295        tracing::debug!("Eliciting I8Positive (positive i8 value)");
296
297        loop {
298            // Elicit base i8 value
299            let value = i8::elicit(communicator).await?;
300
301            // Try to construct I8Positive (validates)
302            match Self::new(value) {
303                Ok(positive) => {
304                    tracing::debug!(value, "Valid I8Positive constructed");
305                    return Ok(positive);
306                }
307                Err(e) => {
308                    tracing::warn!(value, error = %e, "Invalid I8Positive, re-prompting");
309                    // Loop continues, will re-prompt
310                }
311            }
312        }
313    }
314
315    fn kani_proof() -> proc_macro2::TokenStream {
316        crate::verification::proof_helpers::kani_numeric_positive("I8Positive", "i8")
317    }
318
319    fn verus_proof() -> proc_macro2::TokenStream {
320        crate::verification::proof_helpers::verus_numeric_positive("I8Positive", "i8")
321    }
322
323    fn creusot_proof() -> proc_macro2::TokenStream {
324        crate::verification::proof_helpers::creusot_numeric_positive("I8Positive", "i8")
325    }
326}
327
328#[cfg(test)]
329mod tests {
330    use super::*;
331
332    #[test]
333    fn i8_positive_new_valid() {
334        let result = I8Positive::new(1);
335        assert!(result.is_ok());
336        assert_eq!(result.unwrap().get(), 1);
337    }
338
339    #[test]
340    fn i8_positive_new_zero_invalid() {
341        let result = I8Positive::new(0);
342        assert!(result.is_err());
343    }
344
345    #[test]
346    fn i8_positive_new_negative_invalid() {
347        let result = I8Positive::new(-1);
348        assert!(result.is_err());
349    }
350
351    #[test]
352    fn i8_positive_into_inner() {
353        let positive = I8Positive::new(42).unwrap();
354        let value: i8 = positive.into_inner();
355        assert_eq!(value, 42);
356    }
357}
358
359// ============================================================================
360// I8NonNegative (i8 >= 0)
361// ============================================================================
362
363/// Contract type for non-negative i8 values (>= 0).
364///
365/// Validates on construction, then can unwrap to stdlib i8 via `into_inner()`.
366#[derive(
367    Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord, Serialize, Deserialize, JsonSchema,
368)]
369#[serde(try_from = "i8")]
370#[schemars(description = "Non-negative integer value (>= 0)")]
371pub struct I8NonNegative(#[schemars(range(min = 0))] i8);
372
373rmcp::elicit_safe!(I8NonNegative);
374impl_integer_tryfrom!(I8NonNegative, i8);
375
376#[cfg_attr(not(kani), instrumented_impl)]
377#[cfg_attr(not(kani), instrumented_impl)]
378#[cfg_attr(not(kani), instrumented_impl)]
379impl I8NonNegative {
380    /// Constructs a non-negative i8 value.
381    ///
382    /// # Errors
383    ///
384    /// Returns `ValidationError::Negative` if value < 0.
385    #[spec(requires: [value >= 0])]
386    pub fn new(value: i8) -> Result<Self, ValidationError> {
387        if value >= 0 {
388            Ok(Self(value))
389        } else {
390            Err(ValidationError::Negative(value as i128))
391        }
392    }
393
394    /// Gets the wrapped value.
395    pub fn get(&self) -> i8 {
396        self.0
397    }
398
399    /// Unwraps to stdlib i8 (trenchcoat off).
400    pub fn into_inner(self) -> i8 {
401        self.0
402    }
403}
404
405crate::default_style!(I8NonNegative => I8NonNegativeStyle);
406
407#[cfg_attr(not(kani), instrumented_impl)]
408impl Prompt for I8NonNegative {
409    fn prompt() -> Option<&'static str> {
410        Some("Please enter a non-negative number (>= 0):")
411    }
412}
413
414#[cfg_attr(not(kani), instrumented_impl)]
415impl Elicitation for I8NonNegative {
416    type Style = I8NonNegativeStyle;
417
418    #[tracing::instrument(skip(communicator), fields(type_name = "I8NonNegative"))]
419    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
420        tracing::debug!("Eliciting I8NonNegative (non-negative i8 value)");
421
422        loop {
423            let value = i8::elicit(communicator).await?;
424
425            match Self::new(value) {
426                Ok(non_negative) => {
427                    tracing::debug!(value, "Valid I8NonNegative constructed");
428                    return Ok(non_negative);
429                }
430                Err(e) => {
431                    tracing::warn!(value, error = %e, "Invalid I8NonNegative, re-prompting");
432                }
433            }
434        }
435    }
436
437    fn kani_proof() -> proc_macro2::TokenStream {
438        crate::verification::proof_helpers::kani_numeric_nonneg("I8NonNegative", "i8")
439    }
440
441    fn verus_proof() -> proc_macro2::TokenStream {
442        crate::verification::proof_helpers::verus_numeric_positive("I8NonNegative", "i8")
443    }
444
445    fn creusot_proof() -> proc_macro2::TokenStream {
446        crate::verification::proof_helpers::creusot_numeric_positive("I8NonNegative", "i8")
447    }
448}
449
450// ============================================================================
451// I8 NonZero Type
452// ============================================================================
453
454/// Contract type for non-zero i8 values (!= 0).
455///
456/// Validates on construction, unwraps to stdlib i8.
457#[contract_type(requires = "value != 0", ensures = "result.get() != 0")]
458#[derive(
459    Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord, Serialize, Deserialize, JsonSchema,
460)]
461#[serde(try_from = "i8")]
462#[schemars(description = "Non-zero integer value (!= 0)")]
463pub struct I8NonZero(i8);
464
465rmcp::elicit_safe!(I8NonZero);
466impl_integer_tryfrom!(I8NonZero, i8);
467
468#[cfg_attr(not(kani), instrumented_impl)]
469impl I8NonZero {
470    /// Creates a new `I8NonZero` if value is non-zero.
471    ///
472    /// # Errors
473    ///
474    /// Returns `ValidationError::Zero` if value == 0.
475    #[spec(requires: [value != 0])]
476    pub fn new(value: i8) -> Result<Self, ValidationError> {
477        if value != 0 {
478            Ok(Self(value))
479        } else {
480            Err(ValidationError::Zero)
481        }
482    }
483
484    /// Gets the inner value.
485    pub fn get(&self) -> i8 {
486        self.0
487    }
488
489    /// Unwraps to inner i8.
490    pub fn into_inner(self) -> i8 {
491        self.0
492    }
493}
494
495crate::default_style!(I8NonZero => I8NonZeroStyle);
496
497#[cfg_attr(not(kani), instrumented_impl)]
498impl Prompt for I8NonZero {
499    fn prompt() -> Option<&'static str> {
500        Some("Please enter a non-zero number (!= 0):")
501    }
502}
503
504#[cfg_attr(not(kani), instrumented_impl)]
505impl Elicitation for I8NonZero {
506    type Style = I8NonZeroStyle;
507
508    #[tracing::instrument(skip(communicator), fields(type_name = "I8NonZero"))]
509    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
510        tracing::debug!("Eliciting I8NonZero");
511
512        loop {
513            let value = i8::elicit(communicator).await?;
514
515            match Self::new(value) {
516                Ok(non_zero) => {
517                    tracing::debug!(value, "Valid I8NonZero constructed");
518                    return Ok(non_zero);
519                }
520                Err(e) => {
521                    tracing::warn!(value, error = %e, "Invalid I8NonZero, re-prompting");
522                }
523            }
524        }
525    }
526
527    fn kani_proof() -> proc_macro2::TokenStream {
528        crate::verification::proof_helpers::kani_numeric_nonzero("I8NonZero", "i8")
529    }
530
531    fn verus_proof() -> proc_macro2::TokenStream {
532        crate::verification::proof_helpers::verus_numeric_nonzero("I8NonZero", "i8")
533    }
534
535    fn creusot_proof() -> proc_macro2::TokenStream {
536        crate::verification::proof_helpers::creusot_numeric_nonzero("I8NonZero", "i8")
537    }
538}
539
540// ============================================================================
541// I8Range (MIN <= i8 <= MAX)
542// ============================================================================
543
544/// Contract type for i8 values within a specified range [MIN, MAX].
545///
546/// Validates on construction, then can unwrap to stdlib i8 via `into_inner()`.
547#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
548pub struct I8Range<const MIN: i8, const MAX: i8>(i8);
549
550impl<const MIN: i8, const MAX: i8> I8Range<MIN, MAX> {
551    /// Constructs an i8 value within the specified range.
552    ///
553    /// # Errors
554    ///
555    /// Returns `ValidationError::OutOfRange` if value not in [MIN, MAX].
556    #[spec(requires: [value >= MIN, value <= MAX])]
557    pub fn new(value: i8) -> Result<Self, ValidationError> {
558        if value >= MIN && value <= MAX {
559            Ok(Self(value))
560        } else {
561            Err(ValidationError::OutOfRange {
562                value: value as i128,
563                min: MIN as i128,
564                max: MAX as i128,
565            })
566        }
567    }
568
569    /// Gets the wrapped value.
570    pub fn get(&self) -> i8 {
571        self.0
572    }
573
574    /// Unwraps to stdlib i8 (trenchcoat off).
575    pub fn into_inner(self) -> i8 {
576        self.0
577    }
578}
579
580// Manual style enum for I8Range (const generics don't work with macros)
581/// Default-only style enum for I8Range.
582#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)]
583pub enum I8RangeStyle {
584    /// Default presentation style.
585    #[default]
586    Default,
587}
588
589#[cfg_attr(not(kani), instrumented_impl)]
590impl crate::Prompt for I8RangeStyle {
591    fn prompt() -> Option<&'static str> {
592        None // No style selection needed
593    }
594}
595
596#[cfg_attr(not(kani), instrumented_impl)]
597impl crate::Elicitation for I8RangeStyle {
598    type Style = I8RangeStyle;
599
600    async fn elicit<C: crate::ElicitCommunicator>(_communicator: &C) -> crate::ElicitResult<Self> {
601        Ok(Self::Default)
602    }
603
604    fn kani_proof() -> proc_macro2::TokenStream {
605        proc_macro2::TokenStream::new()
606    }
607
608    fn verus_proof() -> proc_macro2::TokenStream {
609        proc_macro2::TokenStream::new()
610    }
611
612    fn creusot_proof() -> proc_macro2::TokenStream {
613        proc_macro2::TokenStream::new()
614    }
615}
616
617impl crate::style::ElicitationStyle for I8RangeStyle {}
618
619impl_integer_range_serde_bridge!(I8Range<i8>);
620
621impl<const MIN: i8, const MAX: i8> Prompt for I8Range<MIN, MAX> {
622    fn prompt() -> Option<&'static str> {
623        // TODO: Dynamic prompt showing MIN/MAX
624        Some("Please enter a number within the specified range:")
625    }
626}
627
628impl<const MIN: i8, const MAX: i8> Elicitation for I8Range<MIN, MAX> {
629    type Style = I8RangeStyle;
630
631    #[tracing::instrument(skip(communicator), fields(type_name = "I8Range", min = MIN, max = MAX))]
632    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
633        tracing::debug!("Eliciting I8Range<{}, {}> (i8 in range)", MIN, MAX);
634
635        loop {
636            let value = i8::elicit(communicator).await?;
637
638            match Self::new(value) {
639                Ok(ranged) => {
640                    tracing::debug!(value, min = MIN, max = MAX, "Valid I8Range constructed");
641                    return Ok(ranged);
642                }
643                Err(e) => {
644                    tracing::warn!(value, error = %e, min = MIN, max = MAX, "Invalid I8Range, re-prompting");
645                }
646            }
647        }
648    }
649
650    fn kani_proof() -> proc_macro2::TokenStream {
651        proc_macro2::TokenStream::new()
652    }
653
654    fn verus_proof() -> proc_macro2::TokenStream {
655        proc_macro2::TokenStream::new()
656    }
657
658    fn creusot_proof() -> proc_macro2::TokenStream {
659        proc_macro2::TokenStream::new()
660    }
661}
662
663#[cfg(test)]
664mod i8_nonnegative_tests {
665    use super::*;
666
667    #[test]
668    fn i8_nonnegative_new_valid_positive() {
669        let result = I8NonNegative::new(42);
670        assert!(result.is_ok());
671        assert_eq!(result.unwrap().get(), 42);
672    }
673
674    #[test]
675    fn i8_nonnegative_new_valid_zero() {
676        let result = I8NonNegative::new(0);
677        assert!(result.is_ok());
678        assert_eq!(result.unwrap().get(), 0);
679    }
680
681    #[test]
682    fn i8_nonnegative_new_negative_invalid() {
683        let result = I8NonNegative::new(-1);
684        assert!(result.is_err());
685    }
686
687    #[test]
688    fn i8_nonnegative_into_inner() {
689        let non_neg = I8NonNegative::new(10).unwrap();
690        let value: i8 = non_neg.into_inner();
691        assert_eq!(value, 10);
692    }
693}
694
695#[cfg(test)]
696mod i8_range_tests {
697    use super::*;
698
699    #[test]
700    fn i8_range_new_valid_within_range() {
701        let result = I8Range::<10, 20>::new(15);
702        assert!(result.is_ok());
703        assert_eq!(result.unwrap().get(), 15);
704    }
705
706    #[test]
707    fn i8_range_new_valid_at_min() {
708        let result = I8Range::<10, 20>::new(10);
709        assert!(result.is_ok());
710        assert_eq!(result.unwrap().get(), 10);
711    }
712
713    #[test]
714    fn i8_range_new_valid_at_max() {
715        let result = I8Range::<10, 20>::new(20);
716        assert!(result.is_ok());
717        assert_eq!(result.unwrap().get(), 20);
718    }
719
720    #[test]
721    fn i8_range_new_below_min_invalid() {
722        let result = I8Range::<10, 20>::new(9);
723        assert!(result.is_err());
724    }
725
726    #[test]
727    fn i8_range_new_above_max_invalid() {
728        let result = I8Range::<10, 20>::new(21);
729        assert!(result.is_err());
730    }
731
732    #[test]
733    fn i8_range_into_inner() {
734        let ranged = I8Range::<10, 20>::new(15).unwrap();
735        let value: i8 = ranged.into_inner();
736        assert_eq!(value, 15);
737    }
738}
739
740// ============================================================================
741// I16Positive (i16 > 0)
742// ============================================================================
743
744/// Contract type for positive i16 values (> 0).
745///
746/// Validates on construction, then can unwrap to stdlib i16 via `into_inner()`.
747#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
748pub struct I16Positive(i16);
749
750#[cfg_attr(not(kani), instrumented_impl)]
751#[cfg_attr(not(kani), instrumented_impl)]
752impl I16Positive {
753    /// Constructs a positive i16 value.
754    ///
755    /// # Errors
756    ///
757    /// Returns `ValidationError::NotPositive` if value <= 0.
758    #[spec(requires: [value > 0])]
759    pub fn new(value: i16) -> Result<Self, ValidationError> {
760        if value > 0 {
761            Ok(Self(value))
762        } else {
763            Err(ValidationError::NotPositive(value as i128))
764        }
765    }
766
767    /// Gets the wrapped value.
768    pub fn get(&self) -> i16 {
769        self.0
770    }
771
772    /// Unwraps to stdlib i16 (trenchcoat off).
773    pub fn into_inner(self) -> i16 {
774        self.0
775    }
776}
777
778crate::default_style!(I16Positive => I16PositiveStyle);
779impl_integer_serde_bridge!(I16Positive, i16, "Positive i16 value (> 0)", { "minimum": 1 });
780
781#[cfg_attr(not(kani), instrumented_impl)]
782impl Prompt for I16Positive {
783    fn prompt() -> Option<&'static str> {
784        Some("Please enter a positive number (> 0):")
785    }
786}
787
788#[cfg_attr(not(kani), instrumented_impl)]
789impl Elicitation for I16Positive {
790    type Style = I16PositiveStyle;
791
792    #[tracing::instrument(skip(communicator), fields(type_name = "I16Positive"))]
793    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
794        tracing::debug!("Eliciting I16Positive (positive i16 value)");
795
796        loop {
797            let value = i16::elicit(communicator).await?;
798
799            match Self::new(value) {
800                Ok(positive) => {
801                    tracing::debug!(value, "Valid I16Positive constructed");
802                    return Ok(positive);
803                }
804                Err(e) => {
805                    tracing::warn!(value, error = %e, "Invalid I16Positive, re-prompting");
806                }
807            }
808        }
809    }
810
811    fn kani_proof() -> proc_macro2::TokenStream {
812        crate::verification::proof_helpers::kani_numeric_positive("I16Positive", "i16")
813    }
814
815    fn verus_proof() -> proc_macro2::TokenStream {
816        crate::verification::proof_helpers::verus_numeric_positive("I16Positive", "i16")
817    }
818
819    fn creusot_proof() -> proc_macro2::TokenStream {
820        crate::verification::proof_helpers::creusot_numeric_positive("I16Positive", "i16")
821    }
822}
823
824// ============================================================================
825// I16NonNegative (i16 >= 0)
826// ============================================================================
827
828/// Contract type for non-negative i16 values (>= 0).
829///
830/// Validates on construction, then can unwrap to stdlib i16 via `into_inner()`.
831#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
832pub struct I16NonNegative(i16);
833
834#[cfg_attr(not(kani), instrumented_impl)]
835#[cfg_attr(not(kani), instrumented_impl)]
836impl I16NonNegative {
837    /// Constructs a non-negative i16 value.
838    ///
839    /// # Errors
840    ///
841    /// Returns `ValidationError::Negative` if value < 0.
842    #[spec(requires: [value >= 0])]
843    pub fn new(value: i16) -> Result<Self, ValidationError> {
844        if value >= 0 {
845            Ok(Self(value))
846        } else {
847            Err(ValidationError::Negative(value as i128))
848        }
849    }
850
851    /// Gets the wrapped value.
852    pub fn get(&self) -> i16 {
853        self.0
854    }
855
856    /// Unwraps to stdlib i16 (trenchcoat off).
857    pub fn into_inner(self) -> i16 {
858        self.0
859    }
860}
861
862crate::default_style!(I16NonNegative => I16NonNegativeStyle);
863impl_integer_serde_bridge!(I16NonNegative, i16, "Non-negative i16 value (>= 0)", { "minimum": 0 });
864
865#[cfg_attr(not(kani), instrumented_impl)]
866impl Prompt for I16NonNegative {
867    fn prompt() -> Option<&'static str> {
868        Some("Please enter a non-negative number (>= 0):")
869    }
870}
871
872#[cfg_attr(not(kani), instrumented_impl)]
873impl Elicitation for I16NonNegative {
874    type Style = I16NonNegativeStyle;
875
876    #[tracing::instrument(skip(communicator), fields(type_name = "I16NonNegative"))]
877    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
878        tracing::debug!("Eliciting I16NonNegative (non-negative i16 value)");
879
880        loop {
881            let value = i16::elicit(communicator).await?;
882
883            match Self::new(value) {
884                Ok(non_negative) => {
885                    tracing::debug!(value, "Valid I16NonNegative constructed");
886                    return Ok(non_negative);
887                }
888                Err(e) => {
889                    tracing::warn!(value, error = %e, "Invalid I16NonNegative, re-prompting");
890                }
891            }
892        }
893    }
894
895    fn kani_proof() -> proc_macro2::TokenStream {
896        crate::verification::proof_helpers::kani_numeric_nonneg("I16NonNegative", "i16")
897    }
898
899    fn verus_proof() -> proc_macro2::TokenStream {
900        crate::verification::proof_helpers::verus_numeric_positive("I16NonNegative", "i16")
901    }
902
903    fn creusot_proof() -> proc_macro2::TokenStream {
904        crate::verification::proof_helpers::creusot_numeric_positive("I16NonNegative", "i16")
905    }
906}
907
908// ============================================================================
909// I16 NonZero Type
910// ============================================================================
911
912/// Contract type for non-zero i16 values (!= 0).
913#[contract_type(requires = "value != 0", ensures = "result.get() != 0")]
914#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
915pub struct I16NonZero(i16);
916
917#[cfg_attr(not(kani), instrumented_impl)]
918impl I16NonZero {
919    /// Creates a new `I16NonZero` if value is non-zero.
920    ///
921    /// # Errors
922    ///
923    /// Returns `ValidationError::Zero` if value == 0.
924    #[spec(requires: [value != 0])]
925    pub fn new(value: i16) -> Result<Self, ValidationError> {
926        if value != 0 {
927            Ok(Self(value))
928        } else {
929            Err(ValidationError::Zero)
930        }
931    }
932
933    /// Gets the inner value.
934    pub fn get(&self) -> i16 {
935        self.0
936    }
937
938    /// Unwraps to inner i16.
939    pub fn into_inner(self) -> i16 {
940        self.0
941    }
942}
943
944crate::default_style!(I16NonZero => I16NonZeroStyle);
945impl_integer_serde_bridge!(I16NonZero, i16, "Non-zero i16 value (!= 0)", { "not": {"const": 0} });
946
947#[cfg_attr(not(kani), instrumented_impl)]
948impl Prompt for I16NonZero {
949    fn prompt() -> Option<&'static str> {
950        Some("Please enter a non-zero number (!= 0):")
951    }
952}
953
954#[cfg_attr(not(kani), instrumented_impl)]
955impl Elicitation for I16NonZero {
956    type Style = I16NonZeroStyle;
957
958    #[tracing::instrument(skip(communicator), fields(type_name = "I16NonZero"))]
959    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
960        tracing::debug!("Eliciting I16NonZero");
961
962        loop {
963            let value = i16::elicit(communicator).await?;
964
965            match Self::new(value) {
966                Ok(non_zero) => {
967                    tracing::debug!(value, "Valid I16NonZero constructed");
968                    return Ok(non_zero);
969                }
970                Err(e) => {
971                    tracing::warn!(value, error = %e, "Invalid I16NonZero, re-prompting");
972                }
973            }
974        }
975    }
976
977    fn kani_proof() -> proc_macro2::TokenStream {
978        crate::verification::proof_helpers::kani_numeric_nonzero("I16NonZero", "i16")
979    }
980
981    fn verus_proof() -> proc_macro2::TokenStream {
982        crate::verification::proof_helpers::verus_numeric_nonzero("I16NonZero", "i16")
983    }
984
985    fn creusot_proof() -> proc_macro2::TokenStream {
986        crate::verification::proof_helpers::creusot_numeric_nonzero("I16NonZero", "i16")
987    }
988}
989
990// ============================================================================
991// I16Range (MIN <= i16 <= MAX)
992// ============================================================================
993
994/// Contract type for i16 values within a specified range [MIN, MAX].
995///
996/// Validates on construction, then can unwrap to stdlib i16 via `into_inner()`.
997#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
998pub struct I16Range<const MIN: i16, const MAX: i16>(i16);
999
1000impl<const MIN: i16, const MAX: i16> I16Range<MIN, MAX> {
1001    /// Constructs an i16 value within the specified range.
1002    ///
1003    /// # Errors
1004    ///
1005    /// Returns `ValidationError::OutOfRange` if value not in [MIN, MAX].
1006    #[spec(requires: [value >= MIN, value <= MAX])]
1007    pub fn new(value: i16) -> Result<Self, ValidationError> {
1008        if value >= MIN && value <= MAX {
1009            Ok(Self(value))
1010        } else {
1011            Err(ValidationError::OutOfRange {
1012                value: value as i128,
1013                min: MIN as i128,
1014                max: MAX as i128,
1015            })
1016        }
1017    }
1018
1019    /// Gets the wrapped value.
1020    pub fn get(&self) -> i16 {
1021        self.0
1022    }
1023
1024    /// Unwraps to stdlib i16 (trenchcoat off).
1025    pub fn into_inner(self) -> i16 {
1026        self.0
1027    }
1028}
1029
1030/// Default-only style enum for I16Range.
1031#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)]
1032pub enum I16RangeStyle {
1033    /// Default presentation style.
1034    #[default]
1035    Default,
1036}
1037
1038#[cfg_attr(not(kani), instrumented_impl)]
1039impl crate::Prompt for I16RangeStyle {
1040    fn prompt() -> Option<&'static str> {
1041        None
1042    }
1043}
1044
1045#[cfg_attr(not(kani), instrumented_impl)]
1046impl crate::Elicitation for I16RangeStyle {
1047    type Style = I16RangeStyle;
1048
1049    async fn elicit<C: crate::ElicitCommunicator>(_communicator: &C) -> crate::ElicitResult<Self> {
1050        Ok(Self::Default)
1051    }
1052
1053    fn kani_proof() -> proc_macro2::TokenStream {
1054        proc_macro2::TokenStream::new()
1055    }
1056
1057    fn verus_proof() -> proc_macro2::TokenStream {
1058        proc_macro2::TokenStream::new()
1059    }
1060
1061    fn creusot_proof() -> proc_macro2::TokenStream {
1062        proc_macro2::TokenStream::new()
1063    }
1064}
1065
1066impl crate::style::ElicitationStyle for I16RangeStyle {}
1067
1068impl_integer_range_serde_bridge!(I16Range<i16>);
1069
1070impl<const MIN: i16, const MAX: i16> Prompt for I16Range<MIN, MAX> {
1071    fn prompt() -> Option<&'static str> {
1072        Some("Please enter a number within the specified range:")
1073    }
1074}
1075
1076impl<const MIN: i16, const MAX: i16> Elicitation for I16Range<MIN, MAX> {
1077    type Style = I16RangeStyle;
1078
1079    #[tracing::instrument(skip(communicator), fields(type_name = "I16Range", min = MIN, max = MAX))]
1080    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
1081        tracing::debug!("Eliciting I16Range<{}, {}> (i16 in range)", MIN, MAX);
1082
1083        loop {
1084            let value = i16::elicit(communicator).await?;
1085
1086            match Self::new(value) {
1087                Ok(ranged) => {
1088                    tracing::debug!(value, min = MIN, max = MAX, "Valid I16Range constructed");
1089                    return Ok(ranged);
1090                }
1091                Err(e) => {
1092                    tracing::warn!(value, error = %e, min = MIN, max = MAX, "Invalid I16Range, re-prompting");
1093                }
1094            }
1095        }
1096    }
1097
1098    fn kani_proof() -> proc_macro2::TokenStream {
1099        proc_macro2::TokenStream::new()
1100    }
1101
1102    fn verus_proof() -> proc_macro2::TokenStream {
1103        proc_macro2::TokenStream::new()
1104    }
1105
1106    fn creusot_proof() -> proc_macro2::TokenStream {
1107        proc_macro2::TokenStream::new()
1108    }
1109}
1110
1111#[cfg(test)]
1112mod i16_positive_tests {
1113    use super::*;
1114
1115    #[test]
1116    fn i16_positive_new_valid() {
1117        let result = I16Positive::new(1);
1118        assert!(result.is_ok());
1119        assert_eq!(result.unwrap().get(), 1);
1120    }
1121
1122    #[test]
1123    fn i16_positive_new_zero_invalid() {
1124        let result = I16Positive::new(0);
1125        assert!(result.is_err());
1126    }
1127
1128    #[test]
1129    fn i16_positive_new_negative_invalid() {
1130        let result = I16Positive::new(-1);
1131        assert!(result.is_err());
1132    }
1133
1134    #[test]
1135    fn i16_positive_into_inner() {
1136        let positive = I16Positive::new(1000).unwrap();
1137        let value: i16 = positive.into_inner();
1138        assert_eq!(value, 1000);
1139    }
1140}
1141
1142#[cfg(test)]
1143mod i16_nonnegative_tests {
1144    use super::*;
1145
1146    #[test]
1147    fn i16_nonnegative_new_valid_positive() {
1148        let result = I16NonNegative::new(1000);
1149        assert!(result.is_ok());
1150        assert_eq!(result.unwrap().get(), 1000);
1151    }
1152
1153    #[test]
1154    fn i16_nonnegative_new_valid_zero() {
1155        let result = I16NonNegative::new(0);
1156        assert!(result.is_ok());
1157        assert_eq!(result.unwrap().get(), 0);
1158    }
1159
1160    #[test]
1161    fn i16_nonnegative_new_negative_invalid() {
1162        let result = I16NonNegative::new(-1);
1163        assert!(result.is_err());
1164    }
1165
1166    #[test]
1167    fn i16_nonnegative_into_inner() {
1168        let non_neg = I16NonNegative::new(500).unwrap();
1169        let value: i16 = non_neg.into_inner();
1170        assert_eq!(value, 500);
1171    }
1172}
1173
1174#[cfg(test)]
1175mod i16_range_tests {
1176    use super::*;
1177
1178    #[test]
1179    fn i16_range_new_valid_within_range() {
1180        let result = I16Range::<100, 200>::new(150);
1181        assert!(result.is_ok());
1182        assert_eq!(result.unwrap().get(), 150);
1183    }
1184
1185    #[test]
1186    fn i16_range_new_valid_at_min() {
1187        let result = I16Range::<100, 200>::new(100);
1188        assert!(result.is_ok());
1189        assert_eq!(result.unwrap().get(), 100);
1190    }
1191
1192    #[test]
1193    fn i16_range_new_valid_at_max() {
1194        let result = I16Range::<100, 200>::new(200);
1195        assert!(result.is_ok());
1196        assert_eq!(result.unwrap().get(), 200);
1197    }
1198
1199    #[test]
1200    fn i16_range_new_below_min_invalid() {
1201        let result = I16Range::<100, 200>::new(99);
1202        assert!(result.is_err());
1203    }
1204
1205    #[test]
1206    fn i16_range_new_above_max_invalid() {
1207        let result = I16Range::<100, 200>::new(201);
1208        assert!(result.is_err());
1209    }
1210
1211    #[test]
1212    fn i16_range_into_inner() {
1213        let ranged = I16Range::<100, 200>::new(150).unwrap();
1214        let value: i16 = ranged.into_inner();
1215        assert_eq!(value, 150);
1216    }
1217}
1218
1219// ============================================================================
1220// U8NonZero (u8 != 0)
1221// ============================================================================
1222
1223/// Contract type for non-zero u8 values (!= 0).
1224///
1225/// Validates on construction, then can unwrap to stdlib u8 via `into_inner()`.
1226#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
1227pub struct U8NonZero(u8);
1228
1229#[cfg_attr(not(kani), instrumented_impl)]
1230#[cfg_attr(not(kani), instrumented_impl)]
1231impl U8NonZero {
1232    /// Constructs a non-zero u8 value.
1233    ///
1234    /// # Errors
1235    ///
1236    /// Returns `ValidationError::Zero` if value == 0.
1237    #[spec(requires: [value != 0])]
1238    pub fn new(value: u8) -> Result<Self, ValidationError> {
1239        if value != 0 {
1240            Ok(Self(value))
1241        } else {
1242            Err(ValidationError::Zero)
1243        }
1244    }
1245
1246    /// Gets the wrapped value.
1247    pub fn get(&self) -> u8 {
1248        self.0
1249    }
1250
1251    /// Unwraps to stdlib u8 (trenchcoat off).
1252    pub fn into_inner(self) -> u8 {
1253        self.0
1254    }
1255}
1256
1257crate::default_style!(U8NonZero => U8NonZeroStyle);
1258impl_integer_serde_bridge!(U8NonZero, u8, "Non-zero u8 value (!= 0)", { "minimum": 1 });
1259
1260#[cfg_attr(not(kani), instrumented_impl)]
1261impl Prompt for U8NonZero {
1262    fn prompt() -> Option<&'static str> {
1263        Some("Please enter a non-zero number (!= 0):")
1264    }
1265}
1266
1267#[cfg_attr(not(kani), instrumented_impl)]
1268impl Elicitation for U8NonZero {
1269    type Style = U8NonZeroStyle;
1270
1271    #[tracing::instrument(skip(communicator), fields(type_name = "U8NonZero"))]
1272    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
1273        tracing::debug!("Eliciting U8NonZero (non-zero u8 value)");
1274
1275        loop {
1276            let value = u8::elicit(communicator).await?;
1277
1278            match Self::new(value) {
1279                Ok(non_zero) => {
1280                    tracing::debug!(value, "Valid U8NonZero constructed");
1281                    return Ok(non_zero);
1282                }
1283                Err(e) => {
1284                    tracing::warn!(value, error = %e, "Invalid U8NonZero, re-prompting");
1285                }
1286            }
1287        }
1288    }
1289
1290    fn kani_proof() -> proc_macro2::TokenStream {
1291        crate::verification::proof_helpers::kani_numeric_nonzero("U8NonZero", "u8")
1292    }
1293
1294    fn verus_proof() -> proc_macro2::TokenStream {
1295        crate::verification::proof_helpers::verus_numeric_nonzero("U8NonZero", "u8")
1296    }
1297
1298    fn creusot_proof() -> proc_macro2::TokenStream {
1299        crate::verification::proof_helpers::creusot_numeric_nonzero("U8NonZero", "u8")
1300    }
1301}
1302
1303// ============================================================================
1304// U8Range (MIN <= u8 <= MAX)
1305// ============================================================================
1306
1307/// Contract type for u8 values within a specified range [MIN, MAX].
1308///
1309/// Validates on construction, then can unwrap to stdlib u8 via `into_inner()`.
1310#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
1311pub struct U8Range<const MIN: u8, const MAX: u8>(u8);
1312
1313impl<const MIN: u8, const MAX: u8> U8Range<MIN, MAX> {
1314    /// Constructs a u8 value within the specified range.
1315    ///
1316    /// # Errors
1317    ///
1318    /// Returns `ValidationError::OutOfRange` if value not in [MIN, MAX].
1319    #[spec(requires: [value >= MIN, value <= MAX])]
1320    pub fn new(value: u8) -> Result<Self, ValidationError> {
1321        if value >= MIN && value <= MAX {
1322            Ok(Self(value))
1323        } else {
1324            Err(ValidationError::OutOfRange {
1325                value: value as i128,
1326                min: MIN as i128,
1327                max: MAX as i128,
1328            })
1329        }
1330    }
1331
1332    /// Gets the wrapped value.
1333    pub fn get(&self) -> u8 {
1334        self.0
1335    }
1336
1337    /// Unwraps to stdlib u8 (trenchcoat off).
1338    pub fn into_inner(self) -> u8 {
1339        self.0
1340    }
1341}
1342
1343/// Default-only style enum for U8Range.
1344#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)]
1345pub enum U8RangeStyle {
1346    /// Default presentation style.
1347    #[default]
1348    Default,
1349}
1350
1351#[cfg_attr(not(kani), instrumented_impl)]
1352impl crate::Prompt for U8RangeStyle {
1353    fn prompt() -> Option<&'static str> {
1354        None
1355    }
1356}
1357
1358#[cfg_attr(not(kani), instrumented_impl)]
1359impl crate::Elicitation for U8RangeStyle {
1360    type Style = U8RangeStyle;
1361
1362    async fn elicit<C: crate::ElicitCommunicator>(_communicator: &C) -> crate::ElicitResult<Self> {
1363        Ok(Self::Default)
1364    }
1365
1366    fn kani_proof() -> proc_macro2::TokenStream {
1367        proc_macro2::TokenStream::new()
1368    }
1369
1370    fn verus_proof() -> proc_macro2::TokenStream {
1371        proc_macro2::TokenStream::new()
1372    }
1373
1374    fn creusot_proof() -> proc_macro2::TokenStream {
1375        proc_macro2::TokenStream::new()
1376    }
1377}
1378
1379impl crate::style::ElicitationStyle for U8RangeStyle {}
1380
1381impl_integer_range_serde_bridge!(U8Range<u8>);
1382
1383impl<const MIN: u8, const MAX: u8> Prompt for U8Range<MIN, MAX> {
1384    fn prompt() -> Option<&'static str> {
1385        Some("Please enter a number within the specified range:")
1386    }
1387}
1388
1389impl<const MIN: u8, const MAX: u8> Elicitation for U8Range<MIN, MAX> {
1390    type Style = U8RangeStyle;
1391
1392    #[tracing::instrument(skip(communicator), fields(type_name = "U8Range", min = MIN, max = MAX))]
1393    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
1394        tracing::debug!("Eliciting U8Range<{}, {}> (u8 in range)", MIN, MAX);
1395
1396        loop {
1397            let value = u8::elicit(communicator).await?;
1398
1399            match Self::new(value) {
1400                Ok(ranged) => {
1401                    tracing::debug!(value, min = MIN, max = MAX, "Valid U8Range constructed");
1402                    return Ok(ranged);
1403                }
1404                Err(e) => {
1405                    tracing::warn!(value, error = %e, min = MIN, max = MAX, "Invalid U8Range, re-prompting");
1406                }
1407            }
1408        }
1409    }
1410
1411    fn kani_proof() -> proc_macro2::TokenStream {
1412        proc_macro2::TokenStream::new()
1413    }
1414
1415    fn verus_proof() -> proc_macro2::TokenStream {
1416        proc_macro2::TokenStream::new()
1417    }
1418
1419    fn creusot_proof() -> proc_macro2::TokenStream {
1420        proc_macro2::TokenStream::new()
1421    }
1422}
1423
1424// ============================================================================
1425// U16NonZero (u16 != 0)
1426// ============================================================================
1427
1428/// Contract type for non-zero u16 values (!= 0).
1429///
1430/// Validates on construction, then can unwrap to stdlib u16 via `into_inner()`.
1431#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
1432pub struct U16NonZero(u16);
1433
1434#[cfg_attr(not(kani), instrumented_impl)]
1435#[cfg_attr(not(kani), instrumented_impl)]
1436impl U16NonZero {
1437    /// Constructs a non-zero u16 value.
1438    ///
1439    /// # Errors
1440    ///
1441    /// Returns `ValidationError::Zero` if value == 0.
1442    #[spec(requires: [value != 0])]
1443    pub fn new(value: u16) -> Result<Self, ValidationError> {
1444        if value != 0 {
1445            Ok(Self(value))
1446        } else {
1447            Err(ValidationError::Zero)
1448        }
1449    }
1450
1451    /// Gets the wrapped value.
1452    pub fn get(&self) -> u16 {
1453        self.0
1454    }
1455
1456    /// Unwraps to stdlib u16 (trenchcoat off).
1457    pub fn into_inner(self) -> u16 {
1458        self.0
1459    }
1460}
1461
1462crate::default_style!(U16NonZero => U16NonZeroStyle);
1463impl_integer_serde_bridge!(U16NonZero, u16, "Non-zero u16 value (!= 0)", { "minimum": 1 });
1464
1465#[cfg_attr(not(kani), instrumented_impl)]
1466impl Prompt for U16NonZero {
1467    fn prompt() -> Option<&'static str> {
1468        Some("Please enter a non-zero number (!= 0):")
1469    }
1470}
1471
1472#[cfg_attr(not(kani), instrumented_impl)]
1473impl Elicitation for U16NonZero {
1474    type Style = U16NonZeroStyle;
1475
1476    #[tracing::instrument(skip(communicator), fields(type_name = "U16NonZero"))]
1477    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
1478        tracing::debug!("Eliciting U16NonZero (non-zero u16 value)");
1479
1480        loop {
1481            let value = u16::elicit(communicator).await?;
1482
1483            match Self::new(value) {
1484                Ok(non_zero) => {
1485                    tracing::debug!(value, "Valid U16NonZero constructed");
1486                    return Ok(non_zero);
1487                }
1488                Err(e) => {
1489                    tracing::warn!(value, error = %e, "Invalid U16NonZero, re-prompting");
1490                }
1491            }
1492        }
1493    }
1494
1495    fn kani_proof() -> proc_macro2::TokenStream {
1496        crate::verification::proof_helpers::kani_numeric_nonzero("U16NonZero", "u16")
1497    }
1498
1499    fn verus_proof() -> proc_macro2::TokenStream {
1500        crate::verification::proof_helpers::verus_numeric_nonzero("U16NonZero", "u16")
1501    }
1502
1503    fn creusot_proof() -> proc_macro2::TokenStream {
1504        crate::verification::proof_helpers::creusot_numeric_nonzero("U16NonZero", "u16")
1505    }
1506}
1507
1508// ============================================================================
1509// U16Range (MIN <= u16 <= MAX)
1510// ============================================================================
1511
1512/// Contract type for u16 values within a specified range [MIN, MAX].
1513///
1514/// Validates on construction, then can unwrap to stdlib u16 via `into_inner()`.
1515#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
1516pub struct U16Range<const MIN: u16, const MAX: u16>(u16);
1517
1518impl<const MIN: u16, const MAX: u16> U16Range<MIN, MAX> {
1519    /// Constructs a u16 value within the specified range.
1520    ///
1521    /// # Errors
1522    ///
1523    /// Returns `ValidationError::OutOfRange` if value not in [MIN, MAX].
1524    #[spec(requires: [value >= MIN, value <= MAX])]
1525    pub fn new(value: u16) -> Result<Self, ValidationError> {
1526        if value >= MIN && value <= MAX {
1527            Ok(Self(value))
1528        } else {
1529            Err(ValidationError::OutOfRange {
1530                value: value as i128,
1531                min: MIN as i128,
1532                max: MAX as i128,
1533            })
1534        }
1535    }
1536
1537    /// Gets the wrapped value.
1538    pub fn get(&self) -> u16 {
1539        self.0
1540    }
1541
1542    /// Unwraps to stdlib u16 (trenchcoat off).
1543    pub fn into_inner(self) -> u16 {
1544        self.0
1545    }
1546}
1547
1548/// Default-only style enum for U16Range.
1549#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)]
1550pub enum U16RangeStyle {
1551    /// Default presentation style.
1552    #[default]
1553    Default,
1554}
1555
1556#[cfg_attr(not(kani), instrumented_impl)]
1557impl crate::Prompt for U16RangeStyle {
1558    fn prompt() -> Option<&'static str> {
1559        None
1560    }
1561}
1562
1563#[cfg_attr(not(kani), instrumented_impl)]
1564impl crate::Elicitation for U16RangeStyle {
1565    type Style = U16RangeStyle;
1566
1567    async fn elicit<C: crate::ElicitCommunicator>(_communicator: &C) -> crate::ElicitResult<Self> {
1568        Ok(Self::Default)
1569    }
1570
1571    fn kani_proof() -> proc_macro2::TokenStream {
1572        proc_macro2::TokenStream::new()
1573    }
1574
1575    fn verus_proof() -> proc_macro2::TokenStream {
1576        proc_macro2::TokenStream::new()
1577    }
1578
1579    fn creusot_proof() -> proc_macro2::TokenStream {
1580        proc_macro2::TokenStream::new()
1581    }
1582}
1583
1584impl crate::style::ElicitationStyle for U16RangeStyle {}
1585
1586impl_integer_range_serde_bridge!(U16Range<u16>);
1587
1588impl<const MIN: u16, const MAX: u16> Prompt for U16Range<MIN, MAX> {
1589    fn prompt() -> Option<&'static str> {
1590        Some("Please enter a number within the specified range:")
1591    }
1592}
1593
1594impl<const MIN: u16, const MAX: u16> Elicitation for U16Range<MIN, MAX> {
1595    type Style = U16RangeStyle;
1596
1597    #[tracing::instrument(skip(communicator), fields(type_name = "U16Range", min = MIN, max = MAX))]
1598    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
1599        tracing::debug!("Eliciting U16Range<{}, {}> (u16 in range)", MIN, MAX);
1600
1601        loop {
1602            let value = u16::elicit(communicator).await?;
1603
1604            match Self::new(value) {
1605                Ok(ranged) => {
1606                    tracing::debug!(value, min = MIN, max = MAX, "Valid U16Range constructed");
1607                    return Ok(ranged);
1608                }
1609                Err(e) => {
1610                    tracing::warn!(value, error = %e, min = MIN, max = MAX, "Invalid U16Range, re-prompting");
1611                }
1612            }
1613        }
1614    }
1615
1616    fn kani_proof() -> proc_macro2::TokenStream {
1617        proc_macro2::TokenStream::new()
1618    }
1619
1620    fn verus_proof() -> proc_macro2::TokenStream {
1621        proc_macro2::TokenStream::new()
1622    }
1623
1624    fn creusot_proof() -> proc_macro2::TokenStream {
1625        proc_macro2::TokenStream::new()
1626    }
1627}
1628
1629#[cfg(test)]
1630mod u8_nonzero_tests {
1631    use super::*;
1632
1633    #[test]
1634    fn u8_nonzero_new_valid() {
1635        let result = U8NonZero::new(1);
1636        assert!(result.is_ok());
1637        assert_eq!(result.unwrap().get(), 1);
1638    }
1639
1640    #[test]
1641    fn u8_nonzero_new_zero_invalid() {
1642        let result = U8NonZero::new(0);
1643        assert!(result.is_err());
1644    }
1645
1646    #[test]
1647    fn u8_nonzero_into_inner() {
1648        let non_zero = U8NonZero::new(255).unwrap();
1649        let value: u8 = non_zero.into_inner();
1650        assert_eq!(value, 255);
1651    }
1652}
1653
1654#[cfg(test)]
1655mod u8_range_tests {
1656    use super::*;
1657
1658    #[test]
1659    fn u8_range_new_valid_within_range() {
1660        let result = U8Range::<10, 20>::new(15);
1661        assert!(result.is_ok());
1662        assert_eq!(result.unwrap().get(), 15);
1663    }
1664
1665    #[test]
1666    fn u8_range_new_valid_at_min() {
1667        let result = U8Range::<10, 20>::new(10);
1668        assert!(result.is_ok());
1669        assert_eq!(result.unwrap().get(), 10);
1670    }
1671
1672    #[test]
1673    fn u8_range_new_valid_at_max() {
1674        let result = U8Range::<10, 20>::new(20);
1675        assert!(result.is_ok());
1676        assert_eq!(result.unwrap().get(), 20);
1677    }
1678
1679    #[test]
1680    fn u8_range_new_below_min_invalid() {
1681        let result = U8Range::<10, 20>::new(9);
1682        assert!(result.is_err());
1683    }
1684
1685    #[test]
1686    fn u8_range_new_above_max_invalid() {
1687        let result = U8Range::<10, 20>::new(21);
1688        assert!(result.is_err());
1689    }
1690
1691    #[test]
1692    fn u8_range_into_inner() {
1693        let ranged = U8Range::<10, 20>::new(15).unwrap();
1694        let value: u8 = ranged.into_inner();
1695        assert_eq!(value, 15);
1696    }
1697}
1698
1699#[cfg(test)]
1700mod u16_nonzero_tests {
1701    use super::*;
1702
1703    #[test]
1704    fn u16_nonzero_new_valid() {
1705        let result = U16NonZero::new(1000);
1706        assert!(result.is_ok());
1707        assert_eq!(result.unwrap().get(), 1000);
1708    }
1709
1710    #[test]
1711    fn u16_nonzero_new_zero_invalid() {
1712        let result = U16NonZero::new(0);
1713        assert!(result.is_err());
1714    }
1715
1716    #[test]
1717    fn u16_nonzero_into_inner() {
1718        let non_zero = U16NonZero::new(65535).unwrap();
1719        let value: u16 = non_zero.into_inner();
1720        assert_eq!(value, 65535);
1721    }
1722}
1723
1724#[cfg(test)]
1725mod u16_range_tests {
1726    use super::*;
1727
1728    #[test]
1729    fn u16_range_new_valid_within_range() {
1730        let result = U16Range::<1000, 2000>::new(1500);
1731        assert!(result.is_ok());
1732        assert_eq!(result.unwrap().get(), 1500);
1733    }
1734
1735    #[test]
1736    fn u16_range_new_valid_at_min() {
1737        let result = U16Range::<1000, 2000>::new(1000);
1738        assert!(result.is_ok());
1739        assert_eq!(result.unwrap().get(), 1000);
1740    }
1741
1742    #[test]
1743    fn u16_range_new_valid_at_max() {
1744        let result = U16Range::<1000, 2000>::new(2000);
1745        assert!(result.is_ok());
1746        assert_eq!(result.unwrap().get(), 2000);
1747    }
1748
1749    #[test]
1750    fn u16_range_new_below_min_invalid() {
1751        let result = U16Range::<1000, 2000>::new(999);
1752        assert!(result.is_err());
1753    }
1754
1755    #[test]
1756    fn u16_range_new_above_max_invalid() {
1757        let result = U16Range::<1000, 2000>::new(2001);
1758        assert!(result.is_err());
1759    }
1760
1761    #[test]
1762    fn u16_range_into_inner() {
1763        let ranged = U16Range::<1000, 2000>::new(1500).unwrap();
1764        let value: u16 = ranged.into_inner();
1765        assert_eq!(value, 1500);
1766    }
1767}
1768
1769// U8Positive - Positive u8 (> 0)
1770/// Contract type for positive u8 values (> 0).
1771#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
1772pub struct U8Positive(u8);
1773
1774#[cfg_attr(not(kani), instrumented_impl)]
1775impl U8Positive {
1776    /// Create a new U8Positive, validating value is positive (> 0).
1777    #[spec(requires: [value > 0])]
1778    pub fn new(value: u8) -> Result<Self, ValidationError> {
1779        if value > 0 {
1780            Ok(Self(value))
1781        } else {
1782            Err(ValidationError::Zero)
1783        }
1784    }
1785    /// Get the inner u8 value.
1786    pub fn get(&self) -> u8 {
1787        self.0
1788    }
1789    /// Consume self and return the inner u8 value.
1790    pub fn into_inner(self) -> u8 {
1791        self.0
1792    }
1793}
1794
1795crate::default_style!(U8Positive => U8PositiveStyle);
1796impl_integer_serde_bridge!(U8Positive, u8, "Positive u8 value (> 0)", { "minimum": 1 });
1797
1798#[cfg_attr(not(kani), instrumented_impl)]
1799impl Prompt for U8Positive {
1800    fn prompt() -> Option<&'static str> {
1801        Some("Please enter a positive number (> 0):")
1802    }
1803}
1804
1805#[cfg_attr(not(kani), instrumented_impl)]
1806impl Elicitation for U8Positive {
1807    type Style = U8PositiveStyle;
1808    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
1809        loop {
1810            if let Ok(v) = Self::new(u8::elicit(communicator).await?) {
1811                return Ok(v);
1812            }
1813        }
1814    }
1815
1816    fn kani_proof() -> proc_macro2::TokenStream {
1817        crate::verification::proof_helpers::kani_numeric_positive("U8Positive", "u8")
1818    }
1819
1820    fn verus_proof() -> proc_macro2::TokenStream {
1821        crate::verification::proof_helpers::verus_numeric_positive("U8Positive", "u8")
1822    }
1823
1824    fn creusot_proof() -> proc_macro2::TokenStream {
1825        crate::verification::proof_helpers::creusot_numeric_positive("U8Positive", "u8")
1826    }
1827}
1828
1829// U16Positive - Positive u16 (> 0)
1830/// Contract type for positive u16 values (> 0).
1831#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
1832pub struct U16Positive(u16);
1833
1834#[cfg_attr(not(kani), instrumented_impl)]
1835impl U16Positive {
1836    /// Create a new U16Positive, validating value is positive (> 0).
1837    #[spec(requires: [value > 0])]
1838    pub fn new(value: u16) -> Result<Self, ValidationError> {
1839        if value > 0 {
1840            Ok(Self(value))
1841        } else {
1842            Err(ValidationError::Zero)
1843        }
1844    }
1845    /// Get the inner u16 value.
1846    pub fn get(&self) -> u16 {
1847        self.0
1848    }
1849    /// Consume self and return the inner u16 value.
1850    pub fn into_inner(self) -> u16 {
1851        self.0
1852    }
1853}
1854
1855crate::default_style!(U16Positive => U16PositiveStyle);
1856impl_integer_serde_bridge!(U16Positive, u16, "Positive u16 value (> 0)", { "minimum": 1 });
1857
1858#[cfg_attr(not(kani), instrumented_impl)]
1859impl Prompt for U16Positive {
1860    fn prompt() -> Option<&'static str> {
1861        Some("Please enter a positive number (> 0):")
1862    }
1863}
1864
1865#[cfg_attr(not(kani), instrumented_impl)]
1866impl Elicitation for U16Positive {
1867    type Style = U16PositiveStyle;
1868    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
1869        loop {
1870            if let Ok(v) = Self::new(u16::elicit(communicator).await?) {
1871                return Ok(v);
1872            }
1873        }
1874    }
1875
1876    fn kani_proof() -> proc_macro2::TokenStream {
1877        crate::verification::proof_helpers::kani_numeric_positive("U16Positive", "u16")
1878    }
1879
1880    fn verus_proof() -> proc_macro2::TokenStream {
1881        crate::verification::proof_helpers::verus_numeric_positive("U16Positive", "u16")
1882    }
1883
1884    fn creusot_proof() -> proc_macro2::TokenStream {
1885        crate::verification::proof_helpers::creusot_numeric_positive("U16Positive", "u16")
1886    }
1887}
1888
1889// ============================================================================
1890// Macro to generate signed integer contract types (Positive, NonNegative, Range)
1891// ============================================================================
1892
1893macro_rules! impl_signed_contracts {
1894    ($base:ty, $positive:ident, $nonnegative:ident, $range:ident, $range_style:ident, $test_pos_value:expr, $test_nonneg_value:expr, $test_range_min:expr, $test_range_max:expr, $test_range_value:expr) => {
1895        // Positive variant (value > 0)
1896        #[doc = concat!("Contract type for positive ", stringify!($base), " values (> 0).")]
1897        ///
1898        /// Validates on construction, then can unwrap to stdlib type via `into_inner()`.
1899        #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
1900        pub struct $positive($base);
1901
1902        impl $positive {
1903            /// Constructs a positive value.
1904            ///
1905            /// # Errors
1906            ///
1907            /// Returns `ValidationError::NotPositive` if value <= 0.
1908            #[spec(requires: [value > 0])]
1909            pub fn new(value: $base) -> Result<Self, ValidationError> {
1910                if value > 0 {
1911                    Ok(Self(value))
1912                } else {
1913                    Err(ValidationError::NotPositive(value as i128))
1914                }
1915            }
1916
1917            /// Gets the wrapped value.
1918            pub fn get(&self) -> $base {
1919                self.0
1920            }
1921
1922            /// Unwraps to stdlib type (trenchcoat off).
1923            pub fn into_inner(self) -> $base {
1924                self.0
1925            }
1926        }
1927
1928        paste::paste! {
1929            crate::default_style!($positive => [<$positive Style>]);
1930
1931            impl Prompt for $positive {
1932                fn prompt() -> Option<&'static str> {
1933                    Some("Please enter a positive number (> 0):")
1934                }
1935            }
1936
1937            impl Elicitation for $positive {
1938                type Style = [<$positive Style>];
1939
1940                #[tracing::instrument(skip(communicator), fields(type_name = stringify!($positive)))]
1941                async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
1942                    tracing::debug!(concat!("Eliciting ", stringify!($positive), " (positive ", stringify!($base), " value)"));
1943
1944                    loop {
1945                        let value = <$base>::elicit(communicator).await?;
1946
1947                        match Self::new(value) {
1948                            Ok(positive) => {
1949                                tracing::debug!(value, concat!("Valid ", stringify!($positive), " constructed"));
1950                                return Ok(positive);
1951                            }
1952                            Err(e) => {
1953                                tracing::warn!(value, error = %e, concat!("Invalid ", stringify!($positive), ", re-prompting"));
1954                            }
1955                        }
1956                    }
1957                }
1958
1959                fn kani_proof() -> proc_macro2::TokenStream {
1960                    crate::verification::proof_helpers::kani_numeric_positive(stringify!($positive), stringify!($base))
1961                }
1962
1963                fn verus_proof() -> proc_macro2::TokenStream {
1964                    crate::verification::proof_helpers::verus_numeric_positive(stringify!($positive), stringify!($base))
1965                }
1966
1967                fn creusot_proof() -> proc_macro2::TokenStream {
1968                    crate::verification::proof_helpers::creusot_numeric_positive(stringify!($positive), stringify!($base))
1969                }
1970
1971            }
1972        }
1973
1974        // NonNegative variant (value >= 0)
1975        #[doc = concat!("Contract type for non-negative ", stringify!($base), " values (>= 0).")]
1976        ///
1977        /// Validates on construction, then can unwrap to stdlib type via `into_inner()`.
1978        #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
1979        pub struct $nonnegative($base);
1980
1981        impl $nonnegative {
1982            /// Constructs a non-negative value.
1983            ///
1984            /// # Errors
1985            ///
1986            /// Returns `ValidationError::Negative` if value < 0.
1987            #[spec(requires: [value >= 0])]
1988            pub fn new(value: $base) -> Result<Self, ValidationError> {
1989                if value >= 0 {
1990                    Ok(Self(value))
1991                } else {
1992                    Err(ValidationError::Negative(value as i128))
1993                }
1994            }
1995
1996            /// Gets the wrapped value.
1997            pub fn get(&self) -> $base {
1998                self.0
1999            }
2000
2001            /// Unwraps to stdlib type (trenchcoat off).
2002            pub fn into_inner(self) -> $base {
2003                self.0
2004            }
2005        }
2006
2007        paste::paste! {
2008            crate::default_style!($nonnegative => [<$nonnegative Style>]);
2009
2010            impl Prompt for $nonnegative {
2011                fn prompt() -> Option<&'static str> {
2012                    Some("Please enter a non-negative number (>= 0):")
2013                }
2014            }
2015
2016            impl Elicitation for $nonnegative {
2017                type Style = [<$nonnegative Style>];
2018
2019                #[tracing::instrument(skip(communicator), fields(type_name = stringify!($nonnegative)))]
2020                async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
2021                    tracing::debug!(concat!("Eliciting ", stringify!($nonnegative), " (non-negative ", stringify!($base), " value)"));
2022
2023                    loop {
2024                        let value = <$base>::elicit(communicator).await?;
2025
2026                        match Self::new(value) {
2027                            Ok(non_negative) => {
2028                                tracing::debug!(value, concat!("Valid ", stringify!($nonnegative), " constructed"));
2029                                return Ok(non_negative);
2030                            }
2031                            Err(e) => {
2032                                tracing::warn!(value, error = %e, concat!("Invalid ", stringify!($nonnegative), ", re-prompting"));
2033                            }
2034                        }
2035                    }
2036                }
2037
2038                fn kani_proof() -> proc_macro2::TokenStream {
2039                    crate::verification::proof_helpers::kani_numeric_nonneg(stringify!($nonnegative), stringify!($base))
2040                }
2041
2042                fn verus_proof() -> proc_macro2::TokenStream {
2043                    crate::verification::proof_helpers::verus_numeric_positive(stringify!($nonnegative), stringify!($base))
2044                }
2045
2046                fn creusot_proof() -> proc_macro2::TokenStream {
2047                    crate::verification::proof_helpers::creusot_numeric_positive(stringify!($nonnegative), stringify!($base))
2048                }
2049
2050            }
2051        }
2052
2053        // Range variant (MIN <= value <= MAX)
2054        #[doc = concat!("Contract type for ", stringify!($base), " values within a specified range [MIN, MAX].")]
2055        ///
2056        /// Validates on construction, then can unwrap to stdlib type via `into_inner()`.
2057        #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
2058        pub struct $range<const MIN: $base, const MAX: $base>($base);
2059
2060        impl<const MIN: $base, const MAX: $base> $range<MIN, MAX> {
2061            /// Constructs a value within the specified range.
2062            ///
2063            /// # Errors
2064            ///
2065            /// Returns `ValidationError::OutOfRange` if value not in [MIN, MAX].
2066            #[spec(requires: [value >= MIN, value <= MAX])]
2067            pub fn new(value: $base) -> Result<Self, ValidationError> {
2068                if value >= MIN && value <= MAX {
2069                    Ok(Self(value))
2070                } else {
2071                    Err(ValidationError::OutOfRange {
2072                        value: value as i128,
2073                        min: MIN as i128,
2074                        max: MAX as i128,
2075                    })
2076                }
2077            }
2078
2079            /// Gets the wrapped value.
2080            pub fn get(&self) -> $base {
2081                self.0
2082            }
2083
2084            /// Unwraps to stdlib type (trenchcoat off).
2085            pub fn into_inner(self) -> $base {
2086                self.0
2087            }
2088        }
2089
2090        #[doc = concat!("Default-only style enum for ", stringify!($range), ".")]
2091        #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)]
2092        pub enum $range_style {
2093            /// Default presentation style.
2094            #[default]
2095            Default,
2096        }
2097
2098        impl crate::Prompt for $range_style {
2099            fn prompt() -> Option<&'static str> {
2100                None
2101            }
2102        }
2103
2104        impl crate::Elicitation for $range_style {
2105            type Style = $range_style;
2106
2107            async fn elicit<C: crate::ElicitCommunicator>(_communicator: &C) -> crate::ElicitResult<Self> {
2108                Ok(Self::Default)
2109            }
2110
2111    fn kani_proof() -> proc_macro2::TokenStream {
2112        proc_macro2::TokenStream::new()
2113    }
2114
2115    fn verus_proof() -> proc_macro2::TokenStream {
2116        proc_macro2::TokenStream::new()
2117    }
2118
2119    fn creusot_proof() -> proc_macro2::TokenStream {
2120        proc_macro2::TokenStream::new()
2121    }
2122}
2123
2124
2125        impl crate::style::ElicitationStyle for $range_style {}
2126        impl<const MIN: $base, const MAX: $base> Prompt for $range<MIN, MAX> {
2127            fn prompt() -> Option<&'static str> {
2128                Some("Please enter a number within the specified range:")
2129            }
2130        }
2131
2132        impl<const MIN: $base, const MAX: $base> Elicitation for $range<MIN, MAX> {
2133            type Style = $range_style;
2134
2135            #[tracing::instrument(skip(communicator), fields(type_name = stringify!($range), min = MIN, max = MAX))]
2136            async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
2137                tracing::debug!(concat!("Eliciting ", stringify!($range), "<{}, {}> (", stringify!($base), " in range)"), MIN, MAX);
2138
2139                loop {
2140                    let value = <$base>::elicit(communicator).await?;
2141
2142                    match Self::new(value) {
2143                        Ok(ranged) => {
2144                            tracing::debug!(value, min = MIN, max = MAX, concat!("Valid ", stringify!($range), " constructed"));
2145                            return Ok(ranged);
2146                        }
2147                        Err(e) => {
2148                            tracing::warn!(value, error = %e, min = MIN, max = MAX, concat!("Invalid ", stringify!($range), ", re-prompting"));
2149                        }
2150                    }
2151                }
2152            }
2153
2154    fn kani_proof() -> proc_macro2::TokenStream {
2155        proc_macro2::TokenStream::new()
2156    }
2157
2158    fn verus_proof() -> proc_macro2::TokenStream {
2159        proc_macro2::TokenStream::new()
2160    }
2161
2162    fn creusot_proof() -> proc_macro2::TokenStream {
2163        proc_macro2::TokenStream::new()
2164    }
2165}
2166
2167        // Tests
2168        paste::paste! {
2169            #[cfg(test)]
2170            mod [<$positive:snake _tests>] {
2171                use super::*;
2172
2173                #[test]
2174                fn [<$positive:snake _new_valid>]() {
2175                    let result = $positive::new($test_pos_value);
2176                    assert!(result.is_ok());
2177                    assert_eq!(result.unwrap().get(), $test_pos_value);
2178                }
2179
2180                #[test]
2181                fn [<$positive:snake _new_zero_invalid>]() {
2182                    let result = $positive::new(0);
2183                    assert!(result.is_err());
2184                }
2185
2186                #[test]
2187                fn [<$positive:snake _new_negative_invalid>]() {
2188                    let result = $positive::new(-1);
2189                    assert!(result.is_err());
2190                }
2191
2192                #[test]
2193                fn [<$positive:snake _into_inner>]() {
2194                    let positive = $positive::new($test_pos_value).unwrap();
2195                    let value: $base = positive.into_inner();
2196                    assert_eq!(value, $test_pos_value);
2197                }
2198            }
2199
2200            #[cfg(test)]
2201            mod [<$nonnegative:snake _tests>] {
2202                use super::*;
2203
2204                #[test]
2205                fn [<$nonnegative:snake _new_valid_positive>]() {
2206                    let result = $nonnegative::new($test_nonneg_value);
2207                    assert!(result.is_ok());
2208                    assert_eq!(result.unwrap().get(), $test_nonneg_value);
2209                }
2210
2211                #[test]
2212                fn [<$nonnegative:snake _new_valid_zero>]() {
2213                    let result = $nonnegative::new(0);
2214                    assert!(result.is_ok());
2215                    assert_eq!(result.unwrap().get(), 0);
2216                }
2217
2218                #[test]
2219                fn [<$nonnegative:snake _new_negative_invalid>]() {
2220                    let result = $nonnegative::new(-1);
2221                    assert!(result.is_err());
2222                }
2223
2224                #[test]
2225                fn [<$nonnegative:snake _into_inner>]() {
2226                    let non_neg = $nonnegative::new($test_nonneg_value).unwrap();
2227                    let value: $base = non_neg.into_inner();
2228                    assert_eq!(value, $test_nonneg_value);
2229                }
2230            }
2231
2232            #[cfg(test)]
2233            mod [<$range:snake _tests>] {
2234                use super::*;
2235
2236                #[test]
2237                fn [<$range:snake _new_valid_within_range>]() {
2238                    let result = $range::<$test_range_min, $test_range_max>::new($test_range_value);
2239                    assert!(result.is_ok());
2240                    assert_eq!(result.unwrap().get(), $test_range_value);
2241                }
2242
2243                #[test]
2244                fn [<$range:snake _new_valid_at_min>]() {
2245                    let result = $range::<$test_range_min, $test_range_max>::new($test_range_min);
2246                    assert!(result.is_ok());
2247                    assert_eq!(result.unwrap().get(), $test_range_min);
2248                }
2249
2250                #[test]
2251                fn [<$range:snake _new_valid_at_max>]() {
2252                    let result = $range::<$test_range_min, $test_range_max>::new($test_range_max);
2253                    assert!(result.is_ok());
2254                    assert_eq!(result.unwrap().get(), $test_range_max);
2255                }
2256
2257                #[test]
2258                fn [<$range:snake _new_below_min_invalid>]() {
2259                    let result = $range::<$test_range_min, $test_range_max>::new($test_range_min - 1);
2260                    assert!(result.is_err());
2261                }
2262
2263                #[test]
2264                fn [<$range:snake _new_above_max_invalid>]() {
2265                    let result = $range::<$test_range_min, $test_range_max>::new($test_range_max + 1);
2266                    assert!(result.is_err());
2267                }
2268
2269                #[test]
2270                fn [<$range:snake _into_inner>]() {
2271                    let ranged = $range::<$test_range_min, $test_range_max>::new($test_range_value).unwrap();
2272                    let value: $base = ranged.into_inner();
2273                    assert_eq!(value, $test_range_value);
2274                }
2275            }
2276        }
2277    };
2278}
2279
2280// ============================================================================
2281// Macro to generate unsigned integer contract types (NonZero, Range)
2282// ============================================================================
2283
2284macro_rules! impl_unsigned_contracts {
2285    ($base:ty, $nonzero:ident, $range:ident, $range_style:ident, $test_nonzero_value:expr, $test_range_min:expr, $test_range_max:expr, $test_range_value:expr) => {
2286        // NonZero variant (value != 0)
2287        #[doc = concat!("Contract type for non-zero ", stringify!($base), " values (!= 0).")]
2288        ///
2289        /// Validates on construction, then can unwrap to stdlib type via `into_inner()`.
2290        #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
2291        pub struct $nonzero($base);
2292
2293        impl $nonzero {
2294            /// Constructs a non-zero value.
2295            ///
2296            /// # Errors
2297            ///
2298            /// Returns `ValidationError::Zero` if value == 0.
2299            #[spec(requires: [value != 0])]
2300            pub fn new(value: $base) -> Result<Self, ValidationError> {
2301                if value != 0 {
2302                    Ok(Self(value))
2303                } else {
2304                    Err(ValidationError::Zero)
2305                }
2306            }
2307
2308            /// Gets the wrapped value.
2309            pub fn get(&self) -> $base {
2310                self.0
2311            }
2312
2313            /// Unwraps to stdlib type (trenchcoat off).
2314            pub fn into_inner(self) -> $base {
2315                self.0
2316            }
2317        }
2318
2319        paste::paste! {
2320            crate::default_style!($nonzero => [<$nonzero Style>]);
2321
2322            impl Prompt for $nonzero {
2323                fn prompt() -> Option<&'static str> {
2324                    Some("Please enter a non-zero number (!= 0):")
2325                }
2326            }
2327
2328            impl Elicitation for $nonzero {
2329                type Style = [<$nonzero Style>];
2330
2331                #[tracing::instrument(skip(communicator), fields(type_name = stringify!($nonzero)))]
2332                async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
2333                    tracing::debug!(concat!("Eliciting ", stringify!($nonzero), " (non-zero ", stringify!($base), " value)"));
2334
2335                    loop {
2336                        let value = <$base>::elicit(communicator).await?;
2337
2338                        match Self::new(value) {
2339                            Ok(non_zero) => {
2340                                tracing::debug!(value, concat!("Valid ", stringify!($nonzero), " constructed"));
2341                                return Ok(non_zero);
2342                            }
2343                            Err(e) => {
2344                                tracing::warn!(value, error = %e, concat!("Invalid ", stringify!($nonzero), ", re-prompting"));
2345                            }
2346                        }
2347                    }
2348                }
2349
2350                fn kani_proof() -> proc_macro2::TokenStream {
2351                    crate::verification::proof_helpers::kani_numeric_nonzero(stringify!($nonzero), stringify!($base))
2352                }
2353
2354                fn verus_proof() -> proc_macro2::TokenStream {
2355                    crate::verification::proof_helpers::verus_numeric_nonzero(stringify!($nonzero), stringify!($base))
2356                }
2357
2358                fn creusot_proof() -> proc_macro2::TokenStream {
2359                    crate::verification::proof_helpers::creusot_numeric_nonzero(stringify!($nonzero), stringify!($base))
2360                }
2361
2362            }
2363        }
2364
2365        // Range variant (MIN <= value <= MAX)
2366        #[doc = concat!("Contract type for ", stringify!($base), " values within a specified range [MIN, MAX].")]
2367        ///
2368        /// Validates on construction, then can unwrap to stdlib type via `into_inner()`.
2369        #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
2370        pub struct $range<const MIN: $base, const MAX: $base>($base);
2371
2372        impl<const MIN: $base, const MAX: $base> $range<MIN, MAX> {
2373            /// Constructs a value within the specified range.
2374            ///
2375            /// # Errors
2376            ///
2377            /// Returns `ValidationError::OutOfRange` if value not in [MIN, MAX].
2378            #[spec(requires: [value >= MIN, value <= MAX])]
2379            pub fn new(value: $base) -> Result<Self, ValidationError> {
2380                if value >= MIN && value <= MAX {
2381                    Ok(Self(value))
2382                } else {
2383                    Err(ValidationError::OutOfRange {
2384                        value: value as i128,
2385                        min: MIN as i128,
2386                        max: MAX as i128,
2387                    })
2388                }
2389            }
2390
2391            /// Gets the wrapped value.
2392            pub fn get(&self) -> $base {
2393                self.0
2394            }
2395
2396            /// Unwraps to stdlib type (trenchcoat off).
2397            pub fn into_inner(self) -> $base {
2398                self.0
2399            }
2400        }
2401
2402        #[doc = concat!("Default-only style enum for ", stringify!($range), ".")]
2403        #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)]
2404        pub enum $range_style {
2405            /// Default presentation style.
2406            #[default]
2407            Default,
2408        }
2409
2410        impl crate::Prompt for $range_style {
2411            fn prompt() -> Option<&'static str> {
2412                None
2413            }
2414        }
2415
2416        impl crate::Elicitation for $range_style {
2417            type Style = $range_style;
2418
2419            async fn elicit<C: crate::ElicitCommunicator>(_communicator: &C) -> crate::ElicitResult<Self> {
2420                Ok(Self::Default)
2421            }
2422
2423    fn kani_proof() -> proc_macro2::TokenStream {
2424        proc_macro2::TokenStream::new()
2425    }
2426
2427    fn verus_proof() -> proc_macro2::TokenStream {
2428        proc_macro2::TokenStream::new()
2429    }
2430
2431    fn creusot_proof() -> proc_macro2::TokenStream {
2432        proc_macro2::TokenStream::new()
2433    }
2434}
2435
2436
2437        impl crate::style::ElicitationStyle for $range_style {}
2438        impl<const MIN: $base, const MAX: $base> Prompt for $range<MIN, MAX> {
2439            fn prompt() -> Option<&'static str> {
2440                Some("Please enter a number within the specified range:")
2441            }
2442        }
2443
2444        impl<const MIN: $base, const MAX: $base> Elicitation for $range<MIN, MAX> {
2445            type Style = $range_style;
2446
2447            #[tracing::instrument(skip(communicator), fields(type_name = stringify!($range), min = MIN, max = MAX))]
2448            async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
2449                tracing::debug!(concat!("Eliciting ", stringify!($range), "<{}, {}> (", stringify!($base), " in range)"), MIN, MAX);
2450
2451                loop {
2452                    let value = <$base>::elicit(communicator).await?;
2453
2454                    match Self::new(value) {
2455                        Ok(ranged) => {
2456                            tracing::debug!(value, min = MIN, max = MAX, concat!("Valid ", stringify!($range), " constructed"));
2457                            return Ok(ranged);
2458                        }
2459                        Err(e) => {
2460                            tracing::warn!(value, error = %e, min = MIN, max = MAX, concat!("Invalid ", stringify!($range), ", re-prompting"));
2461                        }
2462                    }
2463                }
2464            }
2465
2466    fn kani_proof() -> proc_macro2::TokenStream {
2467        proc_macro2::TokenStream::new()
2468    }
2469
2470    fn verus_proof() -> proc_macro2::TokenStream {
2471        proc_macro2::TokenStream::new()
2472    }
2473
2474    fn creusot_proof() -> proc_macro2::TokenStream {
2475        proc_macro2::TokenStream::new()
2476    }
2477}
2478
2479        // Tests
2480        paste::paste! {
2481            #[cfg(test)]
2482            mod [<$nonzero:snake _tests>] {
2483                use super::*;
2484
2485                #[test]
2486                fn [<$nonzero:snake _new_valid>]() {
2487                    let result = $nonzero::new($test_nonzero_value);
2488                    assert!(result.is_ok());
2489                    assert_eq!(result.unwrap().get(), $test_nonzero_value);
2490                }
2491
2492                #[test]
2493                fn [<$nonzero:snake _new_zero_invalid>]() {
2494                    let result = $nonzero::new(0);
2495                    assert!(result.is_err());
2496                }
2497
2498                #[test]
2499                fn [<$nonzero:snake _into_inner>]() {
2500                    let non_zero = $nonzero::new($test_nonzero_value).unwrap();
2501                    let value: $base = non_zero.into_inner();
2502                    assert_eq!(value, $test_nonzero_value);
2503                }
2504            }
2505
2506            #[cfg(test)]
2507            mod [<$range:snake _tests>] {
2508                use super::*;
2509
2510                #[test]
2511                fn [<$range:snake _new_valid_within_range>]() {
2512                    let result = $range::<$test_range_min, $test_range_max>::new($test_range_value);
2513                    assert!(result.is_ok());
2514                    assert_eq!(result.unwrap().get(), $test_range_value);
2515                }
2516
2517                #[test]
2518                fn [<$range:snake _new_valid_at_min>]() {
2519                    let result = $range::<$test_range_min, $test_range_max>::new($test_range_min);
2520                    assert!(result.is_ok());
2521                    assert_eq!(result.unwrap().get(), $test_range_min);
2522                }
2523
2524                #[test]
2525                fn [<$range:snake _new_valid_at_max>]() {
2526                    let result = $range::<$test_range_min, $test_range_max>::new($test_range_max);
2527                    assert!(result.is_ok());
2528                    assert_eq!(result.unwrap().get(), $test_range_max);
2529                }
2530
2531                #[test]
2532                fn [<$range:snake _new_below_min_invalid>]() {
2533                    let result = $range::<$test_range_min, $test_range_max>::new($test_range_min - 1);
2534                    assert!(result.is_err());
2535                }
2536
2537                #[test]
2538                fn [<$range:snake _new_above_max_invalid>]() {
2539                    let result = $range::<$test_range_min, $test_range_max>::new($test_range_max + 1);
2540                    assert!(result.is_err());
2541                }
2542
2543                #[test]
2544                fn [<$range:snake _into_inner>]() {
2545                    let ranged = $range::<$test_range_min, $test_range_max>::new($test_range_value).unwrap();
2546                    let value: $base = ranged.into_inner();
2547                    assert_eq!(value, $test_range_value);
2548                }
2549            }
2550        }
2551    };
2552}
2553
2554// ============================================================================
2555// Generate remaining integer contract types using macros
2556// ============================================================================
2557
2558// i32 family
2559impl_signed_contracts!(
2560    i32,
2561    I32Positive,
2562    I32NonNegative,
2563    I32Range,
2564    I32RangeStyle,
2565    42,
2566    100,
2567    10,
2568    100,
2569    50
2570);
2571
2572// u32 family
2573impl_unsigned_contracts!(u32, U32NonZero, U32Range, U32RangeStyle, 42, 10, 100, 50);
2574
2575// Serde/JsonSchema bridges for i32 and u32 families
2576impl_integer_serde_bridge!(I32Positive, i32, "Positive i32 value (> 0)", { "minimum": 1 });
2577impl_integer_serde_bridge!(I32NonNegative, i32, "Non-negative i32 value (>= 0)", { "minimum": 0 });
2578impl_integer_range_serde_bridge!(I32Range<i32>);
2579impl_integer_serde_bridge!(I32NonZero, i32, "Non-zero i32 value (!= 0)", { "not": {"const": 0} });
2580impl_integer_serde_bridge!(U32NonZero, u32, "Non-zero u32 value (!= 0)", { "minimum": 1 });
2581impl_integer_range_serde_bridge!(U32Range<u32>);
2582
2583// ============================================================================
2584// Default Wrappers (for MCP elicitation of primitives)
2585// ============================================================================
2586
2587// Generate Default wrappers for all signed integer types
2588impl_integer_default_wrapper!(i8, I8Default, i8::MIN as i64, i8::MAX as i64);
2589impl_integer_default_wrapper!(i16, I16Default, i16::MIN as i64, i16::MAX as i64);
2590impl_integer_default_wrapper!(i32, I32Default, i32::MIN as i64, i32::MAX as i64);
2591impl_integer_default_wrapper!(i64, I64Default, i64::MIN, i64::MAX);
2592impl_integer_default_wrapper!(i128, I128Default, i64::MIN, i64::MAX); // Clamped to i64 range for MCP
2593impl_integer_default_wrapper!(isize, IsizeDefault, isize::MIN as i64, isize::MAX as i64);
2594
2595// Generate Default wrappers for all unsigned integer types
2596impl_integer_default_wrapper!(u8, U8Default, 0, u8::MAX as i64);
2597impl_integer_default_wrapper!(u16, U16Default, 0, u16::MAX as i64);
2598impl_integer_default_wrapper!(u32, U32Default, 0, u32::MAX as i64);
2599impl_integer_default_wrapper!(u64, U64Default, 0, i64::MAX); // Clamped to i64::MAX for MCP
2600impl_integer_default_wrapper!(u128, U128Default, 0, i64::MAX); // Clamped to i64::MAX for MCP
2601impl_integer_default_wrapper!(usize, UsizeDefault, 0, isize::MAX as i64);
2602
2603// ============================================================================
2604// Type Families Generated by Macros
2605// ============================================================================
2606
2607// i64 family
2608impl_signed_contracts!(
2609    i64,
2610    I64Positive,
2611    I64NonNegative,
2612    I64Range,
2613    I64RangeStyle,
2614    42,
2615    100,
2616    10,
2617    100,
2618    50
2619);
2620
2621// u64 family
2622impl_unsigned_contracts!(u64, U64NonZero, U64Range, U64RangeStyle, 42, 10, 100, 50);
2623
2624// Serde/JsonSchema bridges for i64 and u64 families
2625impl_integer_serde_bridge!(I64Positive, i64, "Positive i64 value (> 0)", { "minimum": 1 });
2626impl_integer_serde_bridge!(I64NonNegative, i64, "Non-negative i64 value (>= 0)", { "minimum": 0 });
2627impl_integer_range_serde_bridge!(I64Range<i64>);
2628impl_integer_serde_bridge!(I64NonZero, i64, "Non-zero i64 value (!= 0)", { "not": {"const": 0} });
2629impl_integer_serde_bridge!(U64NonZero, u64, "Non-zero u64 value (!= 0)", { "minimum": 1 });
2630impl_integer_range_serde_bridge!(U64Range<u64>);
2631
2632// i128 family
2633impl_signed_contracts!(
2634    i128,
2635    I128Positive,
2636    I128NonNegative,
2637    I128Range,
2638    I128RangeStyle,
2639    42,
2640    100,
2641    10,
2642    100,
2643    50
2644);
2645
2646// u128 family
2647impl_unsigned_contracts!(
2648    u128,
2649    U128NonZero,
2650    U128Range,
2651    U128RangeStyle,
2652    42,
2653    10,
2654    100,
2655    50
2656);
2657
2658// Serde/JsonSchema bridges for i128 and u128 families
2659impl_integer_serde_bridge!(I128Positive, i128, "Positive i128 value (> 0)", { "minimum": 1 });
2660impl_integer_serde_bridge!(I128NonNegative, i128, "Non-negative i128 value (>= 0)", { "minimum": 0 });
2661impl_integer_range_serde_bridge!(I128Range<i128>);
2662impl_integer_serde_bridge!(I128NonZero, i128, "Non-zero i128 value (!= 0)", { "not": {"const": 0} });
2663impl_integer_serde_bridge!(U128NonZero, u128, "Non-zero u128 value (!= 0)", { "minimum": 1 });
2664impl_integer_range_serde_bridge!(U128Range<u128>);
2665
2666// isize family
2667impl_signed_contracts!(
2668    isize,
2669    IsizePositive,
2670    IsizeNonNegative,
2671    IsizeRange,
2672    IsizeRangeStyle,
2673    42,
2674    100,
2675    10,
2676    100,
2677    50
2678);
2679
2680// usize family
2681impl_unsigned_contracts!(
2682    usize,
2683    UsizeNonZero,
2684    UsizeRange,
2685    UsizeRangeStyle,
2686    42,
2687    10,
2688    100,
2689    50
2690);
2691
2692// Serde/JsonSchema bridges for isize and usize families
2693impl_integer_serde_bridge!(IsizePositive, isize, "Positive isize value (> 0)", { "minimum": 1 });
2694impl_integer_serde_bridge!(IsizeNonNegative, isize, "Non-negative isize value (>= 0)", { "minimum": 0 });
2695impl_integer_range_serde_bridge!(IsizeRange<isize>);
2696impl_integer_serde_bridge!(IsizeNonZero, isize, "Non-zero isize value (!= 0)", { "not": {"const": 0} });
2697impl_integer_serde_bridge!(UsizeNonZero, usize, "Non-zero usize value (!= 0)", { "minimum": 1 });
2698impl_integer_range_serde_bridge!(UsizeRange<usize>);
2699
2700// ============================================================================
2701// Additional Signed NonZero Types (for Prusti proofs)
2702// ============================================================================
2703
2704macro_rules! impl_signed_nonzero {
2705    ($base:ty, $nonzero:ident, $test_value:expr) => {
2706        #[doc = concat!("Contract type for non-zero ", stringify!($base), " values (!= 0).")]
2707        #[contract_type(requires = "value != 0", ensures = "result.get() != 0")]
2708        #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
2709        pub struct $nonzero($base);
2710
2711        impl $nonzero {
2712            /// Creates a non-zero value.
2713            ///
2714            /// # Errors
2715            ///
2716            /// Returns `ValidationError::Zero` if value == 0.
2717            #[spec(requires: [value != 0])]
2718            pub fn new(value: $base) -> Result<Self, ValidationError> {
2719                if value != 0 {
2720                    Ok(Self(value))
2721                } else {
2722                    Err(ValidationError::Zero)
2723                }
2724            }
2725
2726            /// Gets the wrapped value.
2727            pub fn get(&self) -> $base {
2728                self.0
2729            }
2730
2731            /// Unwraps to stdlib type.
2732            pub fn into_inner(self) -> $base {
2733                self.0
2734            }
2735        }
2736
2737        paste::paste! {
2738            crate::default_style!($nonzero => [<$nonzero Style>]);
2739
2740            impl Prompt for $nonzero {
2741                fn prompt() -> Option<&'static str> {
2742                    Some("Please enter a non-zero number (!= 0):")
2743                }
2744            }
2745
2746            impl Elicitation for $nonzero {
2747                type Style = [<$nonzero Style>];
2748
2749                #[tracing::instrument(skip(communicator), fields(type_name = stringify!($nonzero)))]
2750                async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
2751                    loop {
2752                        let value = <$base>::elicit(communicator).await?;
2753                        match Self::new(value) {
2754                            Ok(v) => return Ok(v),
2755                            Err(e) => tracing::warn!(error = %e, "Invalid, re-prompting"),
2756                        }
2757                    }
2758                }
2759
2760                fn kani_proof() -> proc_macro2::TokenStream {
2761                    crate::verification::proof_helpers::kani_numeric_nonzero(stringify!($nonzero), stringify!($base))
2762                }
2763
2764                fn verus_proof() -> proc_macro2::TokenStream {
2765                    crate::verification::proof_helpers::verus_numeric_nonzero(stringify!($nonzero), stringify!($base))
2766                }
2767
2768                fn creusot_proof() -> proc_macro2::TokenStream {
2769                    crate::verification::proof_helpers::creusot_numeric_nonzero(stringify!($nonzero), stringify!($base))
2770                }
2771
2772            }
2773        }
2774    };
2775}
2776
2777// Generate missing signed NonZero types
2778impl_signed_nonzero!(i32, I32NonZero, 42);
2779impl_signed_nonzero!(i64, I64NonZero, 42);
2780impl_signed_nonzero!(i128, I128NonZero, 42);
2781impl_signed_nonzero!(isize, IsizeNonZero, 42);
2782
2783// ============================================================================
2784// Additional Unsigned Positive Types (for Prusti proofs)
2785// ============================================================================
2786
2787macro_rules! impl_unsigned_positive {
2788    ($base:ty, $positive:ident, $test_value:expr) => {
2789        #[doc = concat!("Contract type for positive ", stringify!($base), " values (> 0).")]
2790        #[contract_type(requires = "value > 0", ensures = "result.get() > 0")]
2791        #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
2792        pub struct $positive($base);
2793
2794        impl $positive {
2795            /// Creates a positive value.
2796            ///
2797            /// # Errors
2798            ///
2799            /// Returns `ValidationError::NotPositive` if value <= 0.
2800            #[spec(requires: [value > 0])]
2801            pub fn new(value: $base) -> Result<Self, ValidationError> {
2802                if value > 0 {
2803                    Ok(Self(value))
2804                } else {
2805                    Err(ValidationError::NotPositive(value as i128))
2806                }
2807            }
2808
2809            /// Gets the wrapped value.
2810            pub fn get(&self) -> $base {
2811                self.0
2812            }
2813
2814            /// Unwraps to stdlib type.
2815            pub fn into_inner(self) -> $base {
2816                self.0
2817            }
2818        }
2819
2820        paste::paste! {
2821            crate::default_style!($positive => [<$positive Style>]);
2822
2823            impl Prompt for $positive {
2824                fn prompt() -> Option<&'static str> {
2825                    Some("Please enter a positive number (> 0):")
2826                }
2827            }
2828
2829            impl Elicitation for $positive {
2830                type Style = [<$positive Style>];
2831
2832                #[tracing::instrument(skip(communicator), fields(type_name = stringify!($positive)))]
2833                async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
2834                    loop {
2835                        let value = <$base>::elicit(communicator).await?;
2836                        match Self::new(value) {
2837                            Ok(v) => return Ok(v),
2838                            Err(e) => tracing::warn!(error = %e, "Invalid, re-prompting"),
2839                        }
2840                    }
2841                }
2842
2843                fn kani_proof() -> proc_macro2::TokenStream {
2844                    crate::verification::proof_helpers::kani_numeric_positive(stringify!($positive), stringify!($base))
2845                }
2846
2847                fn verus_proof() -> proc_macro2::TokenStream {
2848                    crate::verification::proof_helpers::verus_numeric_positive(stringify!($positive), stringify!($base))
2849                }
2850
2851                fn creusot_proof() -> proc_macro2::TokenStream {
2852                    crate::verification::proof_helpers::creusot_numeric_positive(stringify!($positive), stringify!($base))
2853                }
2854
2855            }
2856        }
2857    };
2858}
2859
2860// Generate missing unsigned Positive types
2861impl_unsigned_positive!(u32, U32Positive, 42);
2862impl_unsigned_positive!(u64, U64Positive, 42);
2863impl_unsigned_positive!(u128, U128Positive, 42);
2864impl_unsigned_positive!(usize, UsizePositive, 42);
2865
2866impl_integer_serde_bridge!(U32Positive, u32, "Positive u32 value (> 0)", { "minimum": 1 });
2867impl_integer_serde_bridge!(U64Positive, u64, "Positive u64 value (> 0)", { "minimum": 1 });
2868impl_integer_serde_bridge!(U128Positive, u128, "Positive u128 value (> 0)", { "minimum": 1 });
2869impl_integer_serde_bridge!(UsizePositive, usize, "Positive usize value (> 0)", { "minimum": 1 });
2870
2871// ============================================================================
2872// Float Contract Types (f32, f64)
2873// ============================================================================
2874
2875// ── ToCodeLiteral impls ───────────────────────────────────────────────────────
2876
2877mod emit_impls {
2878    use super::*;
2879    use crate::emit_code::ToCodeLiteral;
2880    use proc_macro2::TokenStream;
2881
2882    /// Generate a `ToCodeLiteral` impl for a simple (non-generic) constrained integer type.
2883    macro_rules! impl_to_code_literal_int {
2884        ($T:ident) => {
2885            impl ToCodeLiteral for $T {
2886                fn to_code_literal(&self) -> TokenStream {
2887                    let v = self.get();
2888                    let msg = concat!("valid ", stringify!($T));
2889                    let type_path: TokenStream = concat!("elicitation::", stringify!($T))
2890                        .parse()
2891                        .expect("valid type path");
2892                    quote::quote! { #type_path::new(#v).expect(#msg) }
2893                }
2894            }
2895        };
2896    }
2897
2898    /// Generate a `ToCodeLiteral` impl for a range type with two const generics.
2899    macro_rules! impl_to_code_literal_range {
2900        ($T:ident, $prim:ty) => {
2901            impl<const MIN: $prim, const MAX: $prim> ToCodeLiteral for $T<MIN, MAX> {
2902                fn to_code_literal(&self) -> TokenStream {
2903                    let v = self.get();
2904                    let msg = concat!("valid ", stringify!($T));
2905                    let type_path: TokenStream = concat!("elicitation::", stringify!($T))
2906                        .parse()
2907                        .expect("valid type path");
2908                    quote::quote! { #type_path::<#MIN, #MAX>::new(#v).expect(#msg) }
2909                }
2910            }
2911        };
2912    }
2913
2914    // i8 family
2915    impl_to_code_literal_int!(I8Positive);
2916    impl_to_code_literal_int!(I8NonNegative);
2917    impl_to_code_literal_int!(I8NonZero);
2918    impl_to_code_literal_range!(I8Range, i8);
2919    // i16 family
2920    impl_to_code_literal_int!(I16Positive);
2921    impl_to_code_literal_int!(I16NonNegative);
2922    impl_to_code_literal_int!(I16NonZero);
2923    impl_to_code_literal_range!(I16Range, i16);
2924    // i32 family
2925    impl_to_code_literal_int!(I32Positive);
2926    impl_to_code_literal_int!(I32NonNegative);
2927    impl_to_code_literal_int!(I32NonZero);
2928    impl_to_code_literal_range!(I32Range, i32);
2929    // i64 family
2930    impl_to_code_literal_int!(I64Positive);
2931    impl_to_code_literal_int!(I64NonNegative);
2932    impl_to_code_literal_int!(I64NonZero);
2933    impl_to_code_literal_range!(I64Range, i64);
2934    // i128 family
2935    impl_to_code_literal_int!(I128Positive);
2936    impl_to_code_literal_int!(I128NonNegative);
2937    impl_to_code_literal_int!(I128NonZero);
2938    impl_to_code_literal_range!(I128Range, i128);
2939    // isize family
2940    impl_to_code_literal_int!(IsizePositive);
2941    impl_to_code_literal_int!(IsizeNonNegative);
2942    impl_to_code_literal_int!(IsizeNonZero);
2943    impl_to_code_literal_range!(IsizeRange, isize);
2944    // u8 family
2945    impl_to_code_literal_int!(U8NonZero);
2946    impl_to_code_literal_int!(U8Positive);
2947    impl_to_code_literal_range!(U8Range, u8);
2948    // u16 family
2949    impl_to_code_literal_int!(U16NonZero);
2950    impl_to_code_literal_int!(U16Positive);
2951    impl_to_code_literal_range!(U16Range, u16);
2952    // u32 family
2953    impl_to_code_literal_int!(U32NonZero);
2954    impl_to_code_literal_int!(U32Positive);
2955    impl_to_code_literal_range!(U32Range, u32);
2956    // u64 family
2957    impl_to_code_literal_int!(U64NonZero);
2958    impl_to_code_literal_int!(U64Positive);
2959    impl_to_code_literal_range!(U64Range, u64);
2960    // u128 family
2961    impl_to_code_literal_int!(U128NonZero);
2962    impl_to_code_literal_int!(U128Positive);
2963    impl_to_code_literal_range!(U128Range, u128);
2964    // usize family
2965    impl_to_code_literal_int!(UsizeNonZero);
2966    impl_to_code_literal_int!(UsizePositive);
2967    impl_to_code_literal_range!(UsizeRange, usize);
2968}
2969
2970// ── ElicitIntrospect impls ────────────────────────────────────────────────────
2971
2972macro_rules! impl_primitive_introspect {
2973    ($($ty:ty => $name:literal),+ $(,)?) => {
2974        $(
2975            impl crate::ElicitIntrospect for $ty {
2976                fn pattern() -> crate::ElicitationPattern {
2977                    crate::ElicitationPattern::Primitive
2978                }
2979                fn metadata() -> crate::TypeMetadata {
2980                    crate::TypeMetadata {
2981                        type_name: $name,
2982                        description: <$ty as crate::Prompt>::prompt(),
2983                        details: crate::PatternDetails::Primitive,
2984                    }
2985                }
2986            }
2987        )+
2988    };
2989}
2990
2991impl_primitive_introspect!(
2992    I8Positive => "I8Positive",
2993    I8NonNegative => "I8NonNegative",
2994    I8NonZero => "I8NonZero",
2995    I16Positive => "I16Positive",
2996    I16NonNegative => "I16NonNegative",
2997    I16NonZero => "I16NonZero",
2998    I32Positive => "I32Positive",
2999    I32NonNegative => "I32NonNegative",
3000    I32NonZero => "I32NonZero",
3001    I64Positive => "I64Positive",
3002    I64NonNegative => "I64NonNegative",
3003    I64NonZero => "I64NonZero",
3004    I128Positive => "I128Positive",
3005    I128NonNegative => "I128NonNegative",
3006    I128NonZero => "I128NonZero",
3007    IsizePositive => "IsizePositive",
3008    IsizeNonNegative => "IsizeNonNegative",
3009    IsizeNonZero => "IsizeNonZero",
3010    U8NonZero => "U8NonZero",
3011    U8Positive => "U8Positive",
3012    U16NonZero => "U16NonZero",
3013    U16Positive => "U16Positive",
3014    U32NonZero => "U32NonZero",
3015    U32Positive => "U32Positive",
3016    U64NonZero => "U64NonZero",
3017    U64Positive => "U64Positive",
3018    U128NonZero => "U128NonZero",
3019    U128Positive => "U128Positive",
3020    UsizeNonZero => "UsizeNonZero",
3021    UsizePositive => "UsizePositive",
3022);
elicitation/verification/types/integers.rs

elicitation/verification/types/
integers.rs
