vstd/std_specs/
fmt.rs

1use super::super::prelude::*;
2use core::fmt::{Arguments, Error, Formatter};
3
4verus! {
5
6#[verifier::external_type_specification]
7#[verifier::external_body]
8pub struct ExError(Error);
9
10#[verifier::external_type_specification]
11#[verifier::external_body]
12pub struct ExFormatter<'a>(Formatter<'a>);
13
14#[verifier::external_type_specification]
15#[verifier::external_body]
16pub struct ExArguments<'a>(Arguments<'a>);
17
18// Rust has a specially handled private module core::fmt::rt,
19// for which we can't directly declare specifications because it is private.
20// To work around this, declare our own rt module,
21// which Verus specially recognizes as a stand-in for core::fmt::rt:
22#[verifier::external]
23mod rt {
24    #[verusfmt::skip]
25    #[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::fmt::rt::Argument")]
26    pub struct Argument<'a>(&'a ());
27
28    impl<'a> Argument<'a> {
29        #[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::fmt::rt::Argument::new_binary")]
30        pub fn new_binary<'b, T: core::fmt::Binary>(x: &'b T) -> Argument<'b> {
31            unimplemented!()
32        }
33
34        #[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::fmt::rt::Argument::new_debug")]
35        pub fn new_debug<'b, T: core::fmt::Debug>(x: &'b T) -> Argument<'b> {
36            unimplemented!()
37        }
38
39        #[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::fmt::rt::Argument::new_debug_noop")]
40        pub fn new_debug_noop<'b, T: core::fmt::Debug>(x: &'b T) -> Argument<'b> {
41            unimplemented!()
42        }
43
44        #[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::fmt::rt::Argument::new_display")]
45        pub fn new_display<'b, T: core::fmt::Display>(x: &'b T) -> Argument<'b> {
46            unimplemented!()
47        }
48
49        #[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::fmt::rt::Argument::new_lower_exp")]
50        pub fn new_lower_exp<'b, T: core::fmt::LowerExp>(x: &'b T) -> Argument<'b> {
51            unimplemented!()
52        }
53
54        #[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::fmt::rt::Argument::new_lower_hex")]
55        pub fn new_lower_hex<'b, T: core::fmt::LowerHex>(x: &'b T) -> Argument<'b> {
56            unimplemented!()
57        }
58
59        #[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::fmt::rt::Argument::new_octal")]
60        pub fn new_octal<'b, T: core::fmt::Octal>(x: &'b T) -> Argument<'b> {
61            unimplemented!()
62        }
63
64        #[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::fmt::rt::Argument::new_pointer")]
65        pub fn new_pointer<'b, T: core::fmt::Pointer>(x: &'b T) -> Argument<'b> {
66            unimplemented!()
67        }
68
69        #[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::fmt::rt::Argument::new_upper_exp")]
70        pub fn new_upper_exp<'b, T: core::fmt::UpperExp>(x: &'b T) -> Argument<'b> {
71            unimplemented!()
72        }
73
74        #[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::fmt::rt::Argument::new_upper_hex")]
75        pub fn new_upper_hex<'b, T: core::fmt::UpperHex>(x: &'b T) -> Argument<'b> {
76            unimplemented!()
77        }
78
79        #[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::fmt::rt::Argument::from_usize")]
80        pub fn from_usize<'b>(x: &'b usize) -> Argument<'b> {
81            unimplemented!()
82        }
83    }
84
85}
86
87#[verifier::external_type_specification]
88#[verifier::external_body]
89pub struct ExArgument<'a>(rt::Argument<'a>);
90
91macro_rules! def_fmt_trait {
92    ($trait:path, $extrait: ident, $spec_trait:ident, $impl_trait:ident, $new:ident) => {
93        $crate::vstd::prelude::verus! {
94            #[verifier::external_trait_specification]
95            #[verifier::external_trait_extension($spec_trait via $impl_trait)]
96            pub trait $extrait: core::marker::PointeeSized {
97                type ExternalTraitSpecificationFor: $trait;
98
99                spec fn fmt_req(&self, f: &Formatter<'_>) -> bool;
100
101                fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>
102                    requires
103                        self.fmt_req(f);
104            }
105
106            #[doc(hidden)]
107            pub assume_specification<'a, 'b, T: $trait>[ rt::Argument::<'a>::$new ](x: &'b T) -> rt::Argument<'b>
108                requires
109                    forall|f: &Formatter<'a>| x.fmt_req(f),
110            ;
111        }
112};
113}
114
115def_fmt_trait!(core::fmt::Binary, ExBinary, BinarySpec, BinarySpecImpl, new_binary);
116
117def_fmt_trait!(core::fmt::Debug, ExDebug, DebugSpec, DebugSpecImpl, new_debug);
118
119def_fmt_trait!(core::fmt::Display, ExDisplay, DisplaySpec, DisplaySpecImpl, new_display);
120
121def_fmt_trait!(core::fmt::LowerExp, ExLowerExp, LowerExpSpec, LowerExpSpecImpl, new_lower_exp);
122
123def_fmt_trait!(core::fmt::LowerHex, ExLowerHex, LowerHexSpec, LowerHexSpecImpl, new_lower_hex);
124
125def_fmt_trait!(core::fmt::Octal, ExOctal, OctalSpec, OctalSpecImpl, new_octal);
126
127def_fmt_trait!(core::fmt::Pointer, ExPointer, PointerSpec, PointerSpecImpl, new_pointer);
128
129def_fmt_trait!(core::fmt::UpperExp, ExUpperExp, UpperExpSpec, UpperExpSpecImpl, new_upper_exp);
130
131def_fmt_trait!(core::fmt::UpperHex, ExUpperHex, UpperHexSpec, UpperHexSpecImpl, new_upper_hex);
132
133#[doc(hidden)]
134pub assume_specification<'a, 'b, T: core::fmt::Debug>[ rt::Argument::<'a>::new_debug_noop ](
135    x: &'b T,
136) -> rt::Argument<'b>
137    requires
138        forall|f: &Formatter<'a>| x.fmt_req(f),
139;
140
141#[doc(hidden)]
142pub assume_specification<'a, 'b>[ rt::Argument::<'a>::from_usize ](x: &'b usize) -> rt::Argument<'b>
143;
144
145pub assume_specification<'a>[ Arguments::<'a>::from_str ](s: &'static str) -> Arguments<'a>
146;
147
148pub assume_specification<'a>[ Arguments::<'a>::from_str_nonconst ](s: &'static str) -> Arguments<'a>
149;
150
151// Specially handled stand-in for Arguments::new (because it uses the private Argument type)
152#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::fmt::Arguments::new")]
153#[verifier::external]
154#[doc(hidden)]
155pub fn arguments_new<'a, const N: usize, const M: usize>(
156    template: &'a [u8; N],
157    args: &'a [rt::Argument<'a>; M],
158) -> Arguments<'a> {
159    unimplemented!()
160}
161
162#[doc(hidden)]
163pub assume_specification<'a, const N: usize, const M: usize>[ arguments_new ](
164    template: &'a [u8; N],
165    args: &'a [rt::Argument<'a>; M],
166) -> Arguments<'a>
167;
168
169#[cfg(all(feature = "alloc", not(verus_verify_core)))]
170pub assume_specification[ alloc::fmt::format ](args: Arguments<'_>) -> alloc::string::String
171;
172
173pub uninterp spec fn fmt_req_all<A>() -> bool;
174
175macro_rules! def_type_axiom {
176    ($ty:ty, $name: ident) => {
177        $crate::vstd::prelude::verus! {
178            pub broadcast axiom fn $name()
179                ensures
180                    #[trigger] fmt_req_all::<$ty>();
181        }
182};
183}
184
185def_type_axiom!(u8, axiom_fmt_req_all_u8);
186
187def_type_axiom!(u16, axiom_fmt_req_all_u16);
188
189def_type_axiom!(u32, axiom_fmt_req_all_u32);
190
191def_type_axiom!(u64, axiom_fmt_req_all_u64);
192
193def_type_axiom!(u128, axiom_fmt_req_all_u128);
194
195def_type_axiom!(usize, axiom_fmt_req_all_usize);
196
197def_type_axiom!(i8, axiom_fmt_req_all_i8);
198
199def_type_axiom!(i16, axiom_fmt_req_all_i16);
200
201def_type_axiom!(i32, axiom_fmt_req_all_i32);
202
203def_type_axiom!(i64, axiom_fmt_req_all_i64);
204
205def_type_axiom!(i128, axiom_fmt_req_all_i128);
206
207def_type_axiom!(isize, axiom_fmt_req_all_isize);
208
209def_type_axiom!(f32, axiom_fmt_req_all_f32);
210
211def_type_axiom!(f64, axiom_fmt_req_all_f64);
212
213def_type_axiom!(bool, axiom_fmt_req_all_bool);
214
215def_type_axiom!(char, axiom_fmt_req_all_char);
216
217def_type_axiom!(&str, axiom_fmt_req_all_str);
218
219#[cfg(all(feature = "alloc", not(verus_verify_core)))]
220def_type_axiom!(alloc::string::String, axiom_fmt_req_all_string);
221
222pub broadcast axiom fn axiom_fmt_req_all_ref<A>()
223    requires
224        fmt_req_all::<A>(),
225    ensures
226        #[trigger] fmt_req_all::<&A>(),
227;
228
229macro_rules! def_trait_axiom {
230    ($trait:path, $name: ident) => {
231        $crate::vstd::prelude::verus! {
232            pub broadcast axiom fn $name<A: $trait>(a: &A, f: &Formatter)
233                requires
234                    fmt_req_all::<A>(),
235                ensures
236                    #[trigger] a.fmt_req(f);
237        }
238};
239}
240
241def_trait_axiom!(core::fmt::Binary, axiom_fmt_req_all_binary);
242
243def_trait_axiom!(core::fmt::Debug, axiom_fmt_req_all_debug);
244
245def_trait_axiom!(core::fmt::Display, axiom_fmt_req_all_display);
246
247def_trait_axiom!(core::fmt::LowerExp, axiom_fmt_req_all_lower_exp);
248
249def_trait_axiom!(core::fmt::LowerHex, axiom_fmt_req_all_lower_hex);
250
251def_trait_axiom!(core::fmt::Octal, axiom_fmt_req_all_octal);
252
253def_trait_axiom!(core::fmt::Pointer, axiom_fmt_req_all_pointer);
254
255def_trait_axiom!(core::fmt::UpperExp, axiom_fmt_req_all_upper_exp);
256
257def_trait_axiom!(core::fmt::UpperHex, axiom_fmt_req_all_upper_hex);
258
259pub broadcast group group_fmt_axioms {
260    // types
261    axiom_fmt_req_all_u8,
262    axiom_fmt_req_all_u16,
263    axiom_fmt_req_all_u32,
264    axiom_fmt_req_all_u64,
265    axiom_fmt_req_all_u128,
266    axiom_fmt_req_all_usize,
267    axiom_fmt_req_all_i8,
268    axiom_fmt_req_all_i16,
269    axiom_fmt_req_all_i32,
270    axiom_fmt_req_all_i64,
271    axiom_fmt_req_all_i128,
272    axiom_fmt_req_all_isize,
273    axiom_fmt_req_all_f32,
274    axiom_fmt_req_all_f64,
275    axiom_fmt_req_all_bool,
276    axiom_fmt_req_all_char,
277    axiom_fmt_req_all_str,
278    #[cfg(all(feature = "alloc", not(verus_verify_core)))]
279    axiom_fmt_req_all_string,
280    axiom_fmt_req_all_ref,
281    // traits
282    axiom_fmt_req_all_binary,
283    axiom_fmt_req_all_debug,
284    axiom_fmt_req_all_display,
285    axiom_fmt_req_all_lower_exp,
286    axiom_fmt_req_all_lower_hex,
287    axiom_fmt_req_all_octal,
288    axiom_fmt_req_all_pointer,
289    axiom_fmt_req_all_upper_exp,
290    axiom_fmt_req_all_upper_hex,
291}
292
293} // verus!
vstd/std_specs/fmt.rs

vstd/std_specs/
fmt.rs
