|
1 | 1 | //! This file contains auxiliary definitions for Flux |
2 | 2 |
|
| 3 | + |
| 4 | +use crate::hash; |
| 5 | +use crate::time; |
| 6 | + |
| 7 | + |
3 | 8 | /// List of properties tracked for the result of primitive bitwise operations. |
4 | 9 | /// See the following link for more information on how extensible properties for primitive operations work: |
5 | 10 | /// <https://flux-rs.github.io/flux/guide/specifications.html#extensible-properties-for-primitive-ops> |
|
65 | 70 | ntail: usize{v: v <= 8}, // how many bytes in tail are valid |
66 | 71 | _marker: PhantomData<S>, |
67 | 72 | } |
| 73 | +
|
| 74 | + impl hash::Hasher for Hasher { |
| 75 | + fn write(self: &mut Self, msg: &[u8]) ensures self: Self; // mut-ref-unfolding |
| 76 | + } |
68 | 77 | } |
69 | 78 |
|
70 | 79 | impl BuildHasherDefault { |
71 | 80 | #[trusted(reason="https://github.com/flux-rs/flux/issues/1185")] |
72 | 81 | fn new() -> Self; |
73 | 82 | } |
74 | | - } |
75 | 83 |
|
76 | | - impl Hasher for hash::sip::Hasher { |
77 | | - fn write(self: &mut Self, msg: &[u8]) ensures self: Self; // mut-ref-unfolding |
78 | | - } |
79 | | -
|
80 | | - impl Clone for hash::BuildHasherDefault { |
81 | | - #[trusted(reason="https://github.com/flux-rs/flux/issues/1185")] |
82 | | - fn clone(self: &Self) -> Self; |
| 84 | + impl clone::Clone for BuildHasherDefault { |
| 85 | + #[trusted(reason="https://github.com/flux-rs/flux/issues/1185")] |
| 86 | + fn clone(self: &Self) -> Self; |
| 87 | + } |
83 | 88 | } |
84 | 89 |
|
85 | | - impl Debug for time::Duration { |
86 | | - #[trusted(reason="modular arithmetic invariant inside nested fmt_decimal")] |
87 | | - fn fmt(self: &Self, f: &mut fmt::Formatter) -> fmt::Result; |
| 90 | + mod time { |
| 91 | + impl fmt::Debug for Duration { |
| 92 | + #[trusted(reason="modular arithmetic invariant inside nested fmt_decimal")] |
| 93 | + fn fmt(self: &Self, f: &mut fmt::Formatter) -> fmt::Result; |
| 94 | + } |
88 | 95 | } |
89 | 96 | }] |
90 | 97 | const _: () = {}; |
0 commit comments