planarian_schema/
ids.rs

1//! Identifiers, hashes and time.
2//!
3//! Time is integer milliseconds rather than `SystemTime`/`Duration`. Integers keep
4//! the type inside the Verus subset, make the fake clock exact, and give the
5//! journal a stable encoding (docs/deviations.md).
6
7use serde::{Deserialize, Deserializer, Serialize, Serializer};
8use sha2::{Digest, Sha256};
9use std::fmt;
10use vstd::prelude::*;
11
12impl Hash {
13    pub const ZERO: Hash = Hash([0; 32]);
14
15    pub fn of(bytes: &[u8]) -> Hash {
16        Hash(Sha256::digest(bytes).into())
17    }
18
19    pub fn to_hex(&self) -> String {
20        const HEX: &[u8; 16] = b"0123456789abcdef";
21        let mut s = String::with_capacity(64);
22        for b in self.0 {
23            s.push(HEX[(b >> 4) as usize] as char);
24            s.push(HEX[(b & 0xf) as usize] as char);
25        }
26        s
27    }
28
29    pub fn from_hex(s: &str) -> Option<Hash> {
30        let bytes = s.as_bytes();
31        if bytes.len() != 64 {
32            return None;
33        }
34        let nib = |c: u8| match c {
35            b'0'..=b'9' => Some(c - b'0'),
36            b'a'..=b'f' => Some(c - b'a' + 10),
37            _ => None,
38        };
39        let mut out = [0u8; 32];
40        for (i, pair) in bytes.chunks(2).enumerate() {
41            out[i] = (nib(pair[0])? << 4) | nib(pair[1])?;
42        }
43        Some(Hash(out))
44    }
45}
46
47impl fmt::Debug for Hash {
48    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
49        write!(f, "Hash({})", &self.to_hex()[..12])
50    }
51}
52
53impl fmt::Display for Hash {
54    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
55        f.write_str(&self.to_hex())
56    }
57}
58
59impl Serialize for Hash {
60    fn serialize<S: Serializer>(&self, s: S) -> Result<S::Ok, S::Error> {
61        s.serialize_str(&self.to_hex())
62    }
63}
64
65impl<'de> Deserialize<'de> for Hash {
66    fn deserialize<D: Deserializer<'de>>(d: D) -> Result<Self, D::Error> {
67        let s = String::deserialize(d)?;
68        Hash::from_hex(&s).ok_or_else(|| serde::de::Error::custom("expected 64 lowercase hex digits"))
69    }
70}
71
72macro_rules! newtype {
73    ($(#[$m:meta])* $name:ident($inner:ty)) => {
74        $(#[$m])*
75        #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
76        #[serde(transparent)]
77        pub struct $name(pub $inner);
78    };
79}
80
81newtype!(ProbeId(String));
82
83// The identifiers a `Transition` carries, visible to the `policy` proofs. Serde
84// derives are `external_derive`: Verus does not verify serialization.
85verus! {
86
87#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, PartialOrd, Ord, Hash)]
88#[derive(Serialize, Deserialize)]
89#[serde(transparent)]
90#[verifier::external_derive]
91pub struct GenerationId(pub u64);
92
93#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
94#[derive(Serialize, Deserialize)]
95#[serde(transparent)]
96#[verifier::external_derive]
97pub struct StorePath(pub String);
98
99#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
100#[derive(Serialize, Deserialize)]
101#[serde(transparent)]
102#[verifier::external_derive]
103pub struct ChangeId(pub String);
104
105#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
106#[derive(Serialize, Deserialize)]
107#[serde(transparent)]
108#[verifier::external_derive]
109pub struct TxnId(pub u64);
110
111#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
112#[derive(Serialize, Deserialize)]
113#[serde(transparent)]
114#[verifier::external_derive]
115pub struct ModelId(pub String);
116
117/// A principal (§11): a human maps to a uid, an agent to a registered key.
118#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
119#[derive(Serialize, Deserialize)]
120#[serde(transparent)]
121#[verifier::external_derive]
122pub struct PrincipalId(pub u64);
123
124#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
125#[derive(Serialize, Deserialize)]
126#[serde(transparent)]
127#[verifier::external_derive]
128pub struct SnapshotId(pub String);
129
130/// Milliseconds since the Unix epoch.
131#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, PartialOrd, Ord, Hash)]
132#[derive(Serialize, Deserialize)]
133#[serde(transparent)]
134#[verifier::external_derive]
135pub struct Timestamp(pub u64);
136
137/// SHA-256. Serialized as 64 lowercase hex digits.
138#[derive(Clone, Copy, Default, PartialEq, Eq, PartialOrd, Ord, Hash)]
139pub struct Hash(pub [u8; 32]);
140
141#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
142#[derive(Serialize, Deserialize)]
143#[serde(transparent)]
144#[verifier::external_derive]
145pub struct IncidentId(pub u64);
146
147#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
148#[derive(Serialize, Deserialize)]
149#[serde(transparent)]
150#[verifier::external_derive]
151pub struct PolicyVersion(pub Hash);
152
153#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
154#[derive(Serialize, Deserialize)]
155#[serde(transparent)]
156#[verifier::external_derive]
157pub struct JobId(pub String);
158
159/// A duration in milliseconds.
160#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, PartialOrd, Ord, Hash)]
161#[derive(Serialize, Deserialize)]
162#[serde(transparent)]
163#[verifier::external_derive]
164pub struct Millis(pub u64);
165
166/// Durable identity of one mutation attempt (§12). Journaled and fsynced before
167/// the backend call it names; the backend tags the call with it and fences on
168/// `(txn, epoch)`.
169#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
170#[verifier::external_derive]
171pub struct OpId {
172    pub txn: TxnId,
173    pub epoch: u64,
174    pub seq: u64,
175}
176
177} // verus!
178
179impl Timestamp {
180    pub fn plus(self, d: Millis) -> Timestamp {
181        Timestamp(self.0.saturating_add(d.0))
182    }
183}
184
185impl Millis {
186    pub const fn secs(s: u64) -> Millis {
187        Millis(s * 1000)
188    }
189}
190
191impl fmt::Display for OpId {
192    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
193        write!(f, "{}.{}.{}", self.txn.0, self.epoch, self.seq)
194    }
195}
196
197#[cfg(test)]
198mod tests {
199    use super::*;
200
201    #[test]
202    fn hash_hex_roundtrip() {
203        let h = Hash::of(b"planarian");
204        assert_eq!(Hash::from_hex(&h.to_hex()), Some(h));
205        assert_eq!(Hash::from_hex("zz"), None);
206        let json = serde_json::to_string(&h).unwrap();
207        assert_eq!(serde_json::from_str::<Hash>(&json).unwrap(), h);
208    }
209}
planarian_schema/ids.rs

planarian_schema/
ids.rs
