oxilean_kernel/serial/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use std::io::Write;
6
7use super::types::{
8    BinarySection, BlobValidator, BufferedOleanWriter, CheckpointedReader, ChecksummedWriter,
9    CompatibilityChecker, DeclDiff, DeclIndex, DeclKindSet, DeltaList, FileStats,
10    FormatDiagnostics, MergeStrategy, MetadataReader, MetadataValue, MetadataWriter, NameTable,
11    OleanArchive, OleanError, OleanReader, OleanWriter, SectionHeader, SectionTable, SerialDecl,
12    SerialError, StringPool,
13};
14
15/// Magic bytes identifying an OleanC file.
16pub(super) const MAGIC: &[u8; 4] = b"OLNC";
17/// Current format version.
18pub(super) const VERSION: u32 = 1;
19/// Header size in bytes: 4 (magic) + 4 (version) + 4 (decl_count) + 8 (metadata_offset) = 20
20pub(super) const HEADER_SIZE: usize = 20;
21/// Declaration kind tag values.
22pub mod kind_tags {
23    pub const AXIOM: u8 = 0;
24    pub const DEFINITION: u8 = 1;
25    pub const THEOREM: u8 = 2;
26    pub const OPAQUE: u8 = 3;
27    pub const INDUCTIVE: u8 = 4;
28    pub const OTHER: u8 = 5;
29}
30/// Serialize a list of declaration names into the OleanC binary format.
31///
32/// Each name is stored as a `SerialDecl::Other` entry.
33pub fn serialize_decl_names(names: &[String]) -> Vec<u8> {
34    let mut w = OleanWriter::new();
35    w.write_header(names.len() as u32);
36    for name in names {
37        w.write_string(name);
38        w.write_u8(kind_tags::OTHER);
39    }
40    w.finish()
41}
42/// Deserialize a list of declaration names from OleanC binary data.
43pub fn deserialize_decl_names(data: &[u8]) -> Result<Vec<String>, OleanError> {
44    let mut r = OleanReader::new(data);
45    let header = r.read_header()?;
46    let mut names = Vec::with_capacity(header.decl_count as usize);
47    for _ in 0..header.decl_count {
48        let name = r.read_string()?;
49        let _kind = r.read_u8()?;
50        names.push(name);
51    }
52    Ok(names)
53}
54/// Write an OleanC file to disk containing the given declaration names.
55pub fn write_oleanc_file(path: &str, decl_names: &[String]) -> std::io::Result<()> {
56    let data = serialize_decl_names(decl_names);
57    let mut file = std::fs::File::create(path)?;
58    file.write_all(&data)?;
59    Ok(())
60}
61/// Read an OleanC file from disk and return its declaration names.
62pub fn read_oleanc_file(path: &str) -> Result<Vec<String>, OleanError> {
63    let data = std::fs::read(path)?;
64    deserialize_decl_names(&data)
65}
66#[cfg(test)]
67mod tests {
68    use super::*;
69    #[test]
70    fn test_writer_read_u32_roundtrip() {
71        let mut w = OleanWriter::new();
72        w.write_u32(42_u32);
73        w.write_u32(0xDEAD_BEEF_u32);
74        let data = w.finish();
75        let mut r = OleanReader::new(&data);
76        assert_eq!(r.read_u32().expect("read_u32 should succeed"), 42);
77        assert_eq!(r.read_u32().expect("read_u32 should succeed"), 0xDEAD_BEEF);
78        assert_eq!(r.remaining(), 0);
79    }
80    #[test]
81    fn test_writer_read_string_roundtrip() {
82        let mut w = OleanWriter::new();
83        w.write_string("Nat.add.comm");
84        w.write_string("");
85        w.write_string("hello world");
86        let data = w.finish();
87        let mut r = OleanReader::new(&data);
88        assert_eq!(
89            r.read_string().expect("read_string should succeed"),
90            "Nat.add.comm"
91        );
92        assert_eq!(r.read_string().expect("read_string should succeed"), "");
93        assert_eq!(
94            r.read_string().expect("read_string should succeed"),
95            "hello world"
96        );
97        assert_eq!(r.remaining(), 0);
98    }
99    #[test]
100    fn test_magic_bytes() {
101        let mut w = OleanWriter::new();
102        w.write_header(0);
103        let data = w.finish();
104        assert_eq!(&data[..4], b"OLNC");
105    }
106    #[test]
107    fn test_header_roundtrip() {
108        let mut w = OleanWriter::new();
109        w.write_header(7);
110        let data = w.finish();
111        let mut r = OleanReader::new(&data);
112        let hdr = r.read_header().expect("hdr should be present");
113        assert_eq!(hdr.version, VERSION);
114        assert_eq!(hdr.decl_count, 7);
115        assert_eq!(hdr.metadata_offset, HEADER_SIZE as u64);
116    }
117    #[test]
118    fn test_serialize_empty_names() {
119        let data = serialize_decl_names(&[]);
120        let names = deserialize_decl_names(&data).expect("names should be present");
121        assert!(names.is_empty());
122    }
123    #[test]
124    fn test_serialize_names_roundtrip() {
125        let input: Vec<String> = vec![
126            "Nat.add".to_string(),
127            "Nat.mul".to_string(),
128            "List.length".to_string(),
129        ];
130        let data = serialize_decl_names(&input);
131        let output = deserialize_decl_names(&data).expect("output should be present");
132        assert_eq!(input, output);
133    }
134    #[test]
135    fn test_invalid_magic_error() {
136        let bad_data = b"BADM\x01\x00\x00\x00\x00\x00\x00\x00\x14\x00\x00\x00\x00\x00\x00\x00";
137        let mut r = OleanReader::new(bad_data);
138        match r.read_header() {
139            Err(OleanError::InvalidMagic) => {}
140            other => panic!("expected InvalidMagic, got {:?}", other),
141        }
142    }
143    #[test]
144    fn test_serial_decl_name() {
145        let decl = SerialDecl::Theorem {
146            name: "Nat.add_comm".to_string(),
147            kind_tag: kind_tags::THEOREM,
148        };
149        assert_eq!(decl.name(), "Nat.add_comm");
150        assert_eq!(decl.kind_tag(), kind_tags::THEOREM);
151        let decl2 = SerialDecl::Inductive {
152            name: "List".to_string(),
153            ctor_count: 2,
154            kind_tag: kind_tags::INDUCTIVE,
155        };
156        assert_eq!(decl2.name(), "List");
157        assert_eq!(decl2.kind_tag(), kind_tags::INDUCTIVE);
158    }
159}
160/// Well-known section tags for the extended binary format.
161#[allow(dead_code)]
162pub mod section_tags {
163    pub const DECLARATIONS: u8 = 0x01;
164    pub const UNIVERSE_LEVELS: u8 = 0x02;
165    pub const NAME_TABLE: u8 = 0x03;
166    pub const EXPORT_LIST: u8 = 0x04;
167    pub const DEBUG_INFO: u8 = 0x05;
168    pub const CHECKSUM: u8 = 0xFF;
169}
170/// Encodes a `SerialDecl` with full field data into bytes.
171#[allow(dead_code)]
172pub fn encode_decl(w: &mut OleanWriter, decl: &SerialDecl) {
173    w.write_string(decl.name());
174    w.write_u8(decl.kind_tag());
175    if let SerialDecl::Inductive { ctor_count, .. } = decl {
176        w.write_u32(*ctor_count);
177    }
178}
179/// Decodes a `SerialDecl` from a reader.
180#[allow(dead_code)]
181pub fn decode_decl(r: &mut OleanReader<'_>) -> Result<SerialDecl, OleanError> {
182    let name = r.read_string()?;
183    let tag = r.read_u8()?;
184    match tag {
185        kind_tags::AXIOM => Ok(SerialDecl::Axiom {
186            name,
187            kind_tag: tag,
188        }),
189        kind_tags::DEFINITION => Ok(SerialDecl::Definition {
190            name,
191            kind_tag: tag,
192        }),
193        kind_tags::THEOREM => Ok(SerialDecl::Theorem {
194            name,
195            kind_tag: tag,
196        }),
197        kind_tags::OPAQUE => Ok(SerialDecl::Opaque {
198            name,
199            kind_tag: tag,
200        }),
201        kind_tags::INDUCTIVE => {
202            let ctor_count = r.read_u32()?;
203            Ok(SerialDecl::Inductive {
204                name,
205                ctor_count,
206                kind_tag: tag,
207            })
208        }
209        kind_tags::OTHER => Ok(SerialDecl::Other {
210            name,
211            kind_tag: tag,
212        }),
213        _ => Err(OleanError::InvalidDeclKind(tag)),
214    }
215}
216/// Serialize a `Vec<SerialDecl>` to binary.
217#[allow(dead_code)]
218pub fn serialize_decls(decls: &[SerialDecl]) -> Vec<u8> {
219    let mut w = OleanWriter::new();
220    w.write_header(decls.len() as u32);
221    for d in decls {
222        encode_decl(&mut w, d);
223    }
224    w.finish()
225}
226/// Deserialize a `Vec<SerialDecl>` from binary.
227#[allow(dead_code)]
228pub fn deserialize_decls(data: &[u8]) -> Result<Vec<SerialDecl>, OleanError> {
229    let mut r = OleanReader::new(data);
230    let header = r.read_header()?;
231    let mut decls = Vec::with_capacity(header.decl_count as usize);
232    for _ in 0..header.decl_count {
233        decls.push(decode_decl(&mut r)?);
234    }
235    Ok(decls)
236}
237/// Write a name table as a section to a writer.
238#[allow(dead_code)]
239pub fn write_name_table_section(table: &NameTable, offset: u64) -> Vec<u8> {
240    let mut inner = OleanWriter::new();
241    table.write(&mut inner);
242    let data = inner.finish();
243    let section = BinarySection::new(section_tags::NAME_TABLE, data, offset);
244    section.to_bytes()
245}
246#[cfg(test)]
247mod tests_serial_extended {
248    use super::*;
249    #[test]
250    fn test_section_header_roundtrip() {
251        let hdr = SectionHeader::new(0x01, 256, 1024);
252        let mut w = OleanWriter::new();
253        hdr.write(&mut w);
254        let data = w.finish();
255        let mut r = OleanReader::new(&data);
256        let hdr2 = SectionHeader::read(&mut r).expect("hdr2 should be present");
257        assert_eq!(hdr2.tag, 0x01);
258        assert_eq!(hdr2.length, 256);
259        assert_eq!(hdr2.offset, 1024);
260    }
261    #[test]
262    fn test_section_table_roundtrip() {
263        let mut table = SectionTable::new();
264        table.add(SectionHeader::new(section_tags::DECLARATIONS, 100, 20));
265        table.add(SectionHeader::new(section_tags::NAME_TABLE, 50, 120));
266        let mut w = OleanWriter::new();
267        table.write(&mut w);
268        let data = w.finish();
269        let mut r = OleanReader::new(&data);
270        let t2 = SectionTable::read(&mut r).expect("t2 should be present");
271        assert_eq!(t2.len(), 2);
272        let decl_hdr = t2
273            .find(section_tags::DECLARATIONS)
274            .expect("decl_hdr should be present");
275        assert_eq!(decl_hdr.length, 100);
276    }
277    #[test]
278    fn test_blob_validator() {
279        let data = b"Hello, OleanC!";
280        let checksum = BlobValidator::compute_checksum(data);
281        let v = BlobValidator::new(checksum);
282        assert!(v.validate(data));
283        assert!(!v.validate(b"Different data"));
284    }
285    #[test]
286    fn test_checksummed_writer() {
287        let mut cw = ChecksummedWriter::new();
288        cw.write_string("test");
289        cw.write_u32(42);
290        let bytes = cw.finish_with_checksum();
291        assert!(bytes.len() > 4);
292    }
293    #[test]
294    fn test_name_table_intern_lookup() {
295        let mut t = NameTable::new();
296        let id0 = t.intern("Nat.add");
297        let id1 = t.intern("List.length");
298        let id0b = t.intern("Nat.add");
299        assert_eq!(id0, id0b);
300        assert_ne!(id0, id1);
301        assert_eq!(t.lookup_id(id0), Some("Nat.add"));
302        assert_eq!(t.lookup_name("List.length"), Some(id1));
303        assert_eq!(t.lookup_id(999), None);
304    }
305    #[test]
306    fn test_name_table_roundtrip() {
307        let mut t = NameTable::new();
308        t.intern("a");
309        t.intern("b");
310        t.intern("c");
311        let mut w = OleanWriter::new();
312        t.write(&mut w);
313        let data = w.finish();
314        let mut r = OleanReader::new(&data);
315        let t2 = NameTable::read(&mut r).expect("t2 should be present");
316        assert_eq!(t2.len(), 3);
317        assert_eq!(t2.lookup_id(0), Some("a"));
318        assert_eq!(t2.lookup_id(2), Some("c"));
319    }
320    #[test]
321    fn test_encode_decode_decl_theorem() {
322        let decl = SerialDecl::Theorem {
323            name: "Nat.add_comm".to_string(),
324            kind_tag: kind_tags::THEOREM,
325        };
326        let mut w = OleanWriter::new();
327        encode_decl(&mut w, &decl);
328        let data = w.finish();
329        let mut r = OleanReader::new(&data);
330        let d2 = decode_decl(&mut r).expect("d2 should be present");
331        assert_eq!(d2.name(), "Nat.add_comm");
332        assert_eq!(d2.kind_tag(), kind_tags::THEOREM);
333    }
334    #[test]
335    fn test_encode_decode_decl_inductive() {
336        let decl = SerialDecl::Inductive {
337            name: "List".to_string(),
338            ctor_count: 2,
339            kind_tag: kind_tags::INDUCTIVE,
340        };
341        let mut w = OleanWriter::new();
342        encode_decl(&mut w, &decl);
343        let data = w.finish();
344        let mut r = OleanReader::new(&data);
345        let d2 = decode_decl(&mut r).expect("d2 should be present");
346        assert_eq!(d2.name(), "List");
347        if let SerialDecl::Inductive { ctor_count, .. } = d2 {
348            assert_eq!(ctor_count, 2);
349        } else {
350            panic!("expected Inductive");
351        }
352    }
353    #[test]
354    fn test_serialize_deserialize_decls() {
355        let decls = vec![
356            SerialDecl::Axiom {
357                name: "propext".to_string(),
358                kind_tag: kind_tags::AXIOM,
359            },
360            SerialDecl::Theorem {
361                name: "Nat.succ_ne_zero".to_string(),
362                kind_tag: kind_tags::THEOREM,
363            },
364            SerialDecl::Inductive {
365                name: "Nat".to_string(),
366                ctor_count: 2,
367                kind_tag: kind_tags::INDUCTIVE,
368            },
369        ];
370        let data = serialize_decls(&decls);
371        let decoded = deserialize_decls(&data).expect("decoded should be present");
372        assert_eq!(decoded.len(), 3);
373        assert_eq!(decoded[0].name(), "propext");
374        assert_eq!(decoded[1].kind_tag(), kind_tags::THEOREM);
375    }
376    #[test]
377    fn test_decode_invalid_kind() {
378        let mut w = OleanWriter::new();
379        w.write_string("bad_decl");
380        w.write_u8(99);
381        let data = w.finish();
382        let mut r = OleanReader::new(&data);
383        match decode_decl(&mut r) {
384            Err(OleanError::InvalidDeclKind(99)) => {}
385            other => panic!("expected InvalidDeclKind(99), got {:?}", other),
386        }
387    }
388    #[test]
389    fn test_binary_section_bytes() {
390        let data = vec![0xDE, 0xAD, 0xBE, 0xEF];
391        let section = BinarySection::new(section_tags::DEBUG_INFO, data, 0);
392        let bytes = section.to_bytes();
393        assert_eq!(bytes.len(), SectionHeader::SIZE + 4);
394        assert_eq!(section.tag(), section_tags::DEBUG_INFO);
395    }
396}
397/// Writes a sequence of booleans compactly as a bitfield.
398#[allow(dead_code)]
399pub fn write_bools(w: &mut OleanWriter, bools: &[bool]) {
400    let n = bools.len();
401    w.write_u32(n as u32);
402    let mut i = 0;
403    while i < n {
404        let mut byte = 0u8;
405        for bit in 0..8 {
406            if i + bit < n && bools[i + bit] {
407                byte |= 1 << bit;
408            }
409        }
410        w.write_u8(byte);
411        i += 8;
412    }
413}
414/// Reads a sequence of booleans from a compact bitfield.
415#[allow(dead_code)]
416pub fn read_bools(r: &mut OleanReader<'_>) -> Result<Vec<bool>, OleanError> {
417    let n = r.read_u32()? as usize;
418    let bytes_needed = (n + 7) / 8;
419    let mut bools = Vec::with_capacity(n);
420    for byte_idx in 0..bytes_needed {
421        let byte = r.read_u8()?;
422        for bit in 0..8 {
423            let idx = byte_idx * 8 + bit;
424            if idx < n {
425                bools.push((byte >> bit) & 1 != 0);
426            }
427        }
428    }
429    Ok(bools)
430}
431#[cfg(test)]
432mod tests_serial_extended2 {
433    use super::*;
434    #[test]
435    fn test_delta_list_roundtrip() {
436        let values = vec![10u32, 20, 35, 36, 100];
437        let dl = DeltaList::encode(&values);
438        let decoded = dl.decode();
439        assert_eq!(decoded, values);
440    }
441    #[test]
442    fn test_delta_list_serial() {
443        let values = vec![0u32, 5, 10, 15];
444        let dl = DeltaList::encode(&values);
445        let mut w = OleanWriter::new();
446        dl.write(&mut w);
447        let data = w.finish();
448        let mut r = OleanReader::new(&data);
449        let dl2 = DeltaList::read(&mut r).expect("dl2 should be present");
450        assert_eq!(dl2.decode(), values);
451    }
452    #[test]
453    fn test_string_pool_roundtrip() {
454        let mut pool = StringPool::new();
455        let i0 = pool.intern("Nat.add");
456        let i1 = pool.intern("List.length");
457        let i0b = pool.intern("Nat.add");
458        assert_eq!(i0, i0b);
459        assert_ne!(i0, i1);
460        assert_eq!(pool.get(i0), Some("Nat.add"));
461        let mut w = OleanWriter::new();
462        pool.write(&mut w);
463        let data = w.finish();
464        let mut r = OleanReader::new(&data);
465        let p2 = StringPool::read(&mut r).expect("p2 should be present");
466        assert_eq!(p2.len(), 2);
467        assert_eq!(p2.get(i1), Some("List.length"));
468    }
469    #[test]
470    fn test_write_read_bools() {
471        let bools = vec![true, false, true, true, false, false, true, false, true];
472        let mut w = OleanWriter::new();
473        write_bools(&mut w, &bools);
474        let data = w.finish();
475        let mut r = OleanReader::new(&data);
476        let decoded = read_bools(&mut r).expect("decoded should be present");
477        assert_eq!(decoded, bools);
478    }
479    #[test]
480    fn test_decl_kind_set() {
481        let mut s = DeclKindSet::new();
482        s.add(kind_tags::AXIOM);
483        s.add(kind_tags::THEOREM);
484        s.add(kind_tags::THEOREM);
485        assert_eq!(s.count(), 2);
486        assert!(s.contains(kind_tags::AXIOM));
487        assert!(s.contains(kind_tags::THEOREM));
488        assert!(!s.contains(kind_tags::INDUCTIVE));
489        assert!(!s.is_empty());
490        let mut w = OleanWriter::new();
491        s.write(&mut w);
492        let data = w.finish();
493        let mut r = OleanReader::new(&data);
494        let s2 = DeclKindSet::read(&mut r).expect("s2 should be present");
495        assert_eq!(s2.mask(), s.mask());
496    }
497}
498/// Computes a simple hash for a binary blob (for integrity checking).
499#[allow(dead_code)]
500pub fn fnv1a_64(data: &[u8]) -> u64 {
501    let mut hash: u64 = 14_695_981_039_346_656_037;
502    for &b in data {
503        hash ^= b as u64;
504        hash = hash.wrapping_mul(1_099_511_628_211);
505    }
506    hash
507}
508/// Checks whether two serialized blobs are identical by hash.
509#[allow(dead_code)]
510pub fn blobs_equal(a: &[u8], b: &[u8]) -> bool {
511    a.len() == b.len() && fnv1a_64(a) == fnv1a_64(b)
512}
513#[cfg(test)]
514mod tests_serial_extended3 {
515    use super::*;
516    #[test]
517    fn test_decl_index_find_and_binary_search() {
518        let mut idx = DeclIndex::new();
519        idx.add("Nat.add", 100);
520        idx.add("Nat.mul", 200);
521        idx.add("List.length", 300);
522        assert_eq!(idx.find_offset("Nat.mul"), Some(200));
523        assert_eq!(idx.find_offset("Unknown"), None);
524        assert!(idx.contains("Nat.add"));
525        let mut idx2 = DeclIndex::new();
526        idx2.add("Alpha", 10);
527        idx2.add("Beta", 20);
528        idx2.add("Gamma", 30);
529        assert_eq!(idx2.binary_search("Beta"), Some(20));
530        assert_eq!(idx2.binary_search("Delta"), None);
531    }
532    #[test]
533    fn test_decl_index_roundtrip() {
534        let mut idx = DeclIndex::new();
535        idx.add("foo", 10);
536        idx.add("bar", 20);
537        let mut w = OleanWriter::new();
538        idx.write(&mut w);
539        let data = w.finish();
540        let mut r = OleanReader::new(&data);
541        let idx2 = DeclIndex::read(&mut r).expect("idx2 should be present");
542        assert_eq!(idx2.len(), 2);
543        assert_eq!(idx2.find_offset("foo"), Some(10));
544    }
545    #[test]
546    fn test_metadata_writer_reader() {
547        let mut mw = MetadataWriter::new();
548        mw.write_str_entry("author", "OxiLean");
549        mw.write_u64_entry("timestamp", 1_700_000_000);
550        mw.write_bool_entry("verified", true);
551        assert_eq!(mw.entry_count(), 3);
552        let data = mw.finish();
553        let mut mr = MetadataReader::new(&data).expect("mr should be present");
554        let entries = mr.read_all().expect("entries should be present");
555        assert_eq!(entries.len(), 3);
556        assert_eq!(entries[0].0, "author");
557        assert!(matches!(entries[0].1, MetadataValue::Str(ref s) if s == "OxiLean"));
558        assert!(matches!(entries[1].1, MetadataValue::U64(1_700_000_000)));
559        assert!(matches!(entries[2].1, MetadataValue::Bool(true)));
560    }
561    #[test]
562    fn test_fnv1a_64() {
563        let h1 = fnv1a_64(b"hello");
564        let h2 = fnv1a_64(b"hello");
565        let h3 = fnv1a_64(b"world");
566        assert_eq!(h1, h2);
567        assert_ne!(h1, h3);
568    }
569    #[test]
570    fn test_blobs_equal() {
571        let a = b"OxiLean kernel serialization";
572        let b = b"OxiLean kernel serialization";
573        let c = b"different content";
574        assert!(blobs_equal(a, b));
575        assert!(!blobs_equal(a, c));
576    }
577}
578/// Validates that a serialized blob starts with valid OleanC magic.
579#[allow(dead_code)]
580pub fn has_valid_magic(data: &[u8]) -> bool {
581    data.len() >= 4 && &data[..4] == b"OLNC"
582}
583/// Returns the declared version from a blob (assumes magic is valid).
584#[allow(dead_code)]
585pub fn peek_version(data: &[u8]) -> Option<u32> {
586    if data.len() < 8 {
587        return None;
588    }
589    let bytes: [u8; 4] = data[4..8].try_into().ok()?;
590    Some(u32::from_le_bytes(bytes))
591}
592/// Returns the declared decl_count from a blob (assumes magic + version valid).
593#[allow(dead_code)]
594pub fn peek_decl_count(data: &[u8]) -> Option<u32> {
595    if data.len() < 12 {
596        return None;
597    }
598    let bytes: [u8; 4] = data[8..12].try_into().ok()?;
599    Some(u32::from_le_bytes(bytes))
600}
601/// Counts declarations by kind in an already-parsed list.
602#[allow(dead_code)]
603pub fn count_by_kind(decls: &[SerialDecl]) -> [u32; 6] {
604    let mut counts = [0u32; 6];
605    for d in decls {
606        let idx = d.kind_tag() as usize;
607        if idx < 6 {
608            counts[idx] += 1;
609        }
610    }
611    counts
612}
613/// Filters declarations by kind tag.
614#[allow(dead_code)]
615pub fn filter_by_kind(decls: &[SerialDecl], tag: u8) -> Vec<&SerialDecl> {
616    decls.iter().filter(|d| d.kind_tag() == tag).collect()
617}
618/// Finds the first declaration with a given name prefix.
619#[allow(dead_code)]
620pub fn find_by_prefix<'a>(decls: &'a [SerialDecl], prefix: &str) -> Option<&'a SerialDecl> {
621    decls.iter().find(|d| d.name().starts_with(prefix))
622}
623#[cfg(test)]
624mod tests_serial_extended4 {
625    use super::*;
626    #[test]
627    fn test_buffered_writer() {
628        let mut bw = BufferedOleanWriter::new(16);
629        bw.write_u32(42);
630        bw.write_string("hi");
631        assert_eq!(bw.total_written(), 10);
632        let data = bw.flush();
633        assert_eq!(data.len(), 10);
634    }
635    #[test]
636    fn test_has_valid_magic() {
637        let mut w = OleanWriter::new();
638        w.write_header(0);
639        let data = w.finish();
640        assert!(has_valid_magic(&data));
641        assert!(!has_valid_magic(b"BADD"));
642        assert!(!has_valid_magic(b"OL"));
643    }
644    #[test]
645    fn test_peek_version_and_decl_count() {
646        let mut w = OleanWriter::new();
647        w.write_header(7);
648        let data = w.finish();
649        assert_eq!(peek_version(&data), Some(1));
650        assert_eq!(peek_decl_count(&data), Some(7));
651    }
652    #[test]
653    fn test_count_by_kind() {
654        let decls = vec![
655            SerialDecl::Axiom {
656                name: "a".to_string(),
657                kind_tag: kind_tags::AXIOM,
658            },
659            SerialDecl::Theorem {
660                name: "t1".to_string(),
661                kind_tag: kind_tags::THEOREM,
662            },
663            SerialDecl::Theorem {
664                name: "t2".to_string(),
665                kind_tag: kind_tags::THEOREM,
666            },
667            SerialDecl::Inductive {
668                name: "I".to_string(),
669                ctor_count: 1,
670                kind_tag: kind_tags::INDUCTIVE,
671            },
672        ];
673        let counts = count_by_kind(&decls);
674        assert_eq!(counts[kind_tags::AXIOM as usize], 1);
675        assert_eq!(counts[kind_tags::THEOREM as usize], 2);
676        assert_eq!(counts[kind_tags::INDUCTIVE as usize], 1);
677        assert_eq!(counts[kind_tags::DEFINITION as usize], 0);
678    }
679    #[test]
680    fn test_filter_and_find() {
681        let decls = vec![
682            SerialDecl::Theorem {
683                name: "Nat.add_comm".to_string(),
684                kind_tag: kind_tags::THEOREM,
685            },
686            SerialDecl::Theorem {
687                name: "Nat.mul_comm".to_string(),
688                kind_tag: kind_tags::THEOREM,
689            },
690            SerialDecl::Axiom {
691                name: "propext".to_string(),
692                kind_tag: kind_tags::AXIOM,
693            },
694        ];
695        let theorems = filter_by_kind(&decls, kind_tags::THEOREM);
696        assert_eq!(theorems.len(), 2);
697        let found = find_by_prefix(&decls, "Nat.mul");
698        assert_eq!(found.map(|d| d.name()), Some("Nat.mul_comm"));
699    }
700}
701/// A type alias for results with `SerialError`.
702#[allow(dead_code)]
703pub type SerialResult<T> = Result<T, SerialError>;
704/// Wraps a deserialization call with context for better error messages.
705#[allow(dead_code)]
706pub fn with_context<T, F>(ctx: &str, offset: usize, f: F) -> SerialResult<T>
707where
708    F: FnOnce() -> Result<T, OleanError>,
709{
710    f().map_err(|e| SerialError::new(e, ctx, offset))
711}
712/// Compute byte size of serializing a string.
713#[allow(dead_code)]
714pub fn serialized_string_size(s: &str) -> usize {
715    4 + s.len()
716}
717/// Compute byte size of serializing a `SerialDecl`.
718#[allow(dead_code)]
719pub fn serialized_decl_size(decl: &SerialDecl) -> usize {
720    let base = serialized_string_size(decl.name()) + 1;
721    match decl {
722        SerialDecl::Inductive { .. } => base + 4,
723        _ => base,
724    }
725}
726/// Compute the total byte size of a serialized declaration list.
727#[allow(dead_code)]
728pub fn total_serialized_size(decls: &[SerialDecl]) -> usize {
729    let header_size = 20;
730    let decl_size: usize = decls.iter().map(serialized_decl_size).sum();
731    header_size + decl_size
732}
733#[cfg(test)]
734mod tests_serial_extended5 {
735    use super::*;
736    #[test]
737    fn test_checkpointed_reader_rollback() {
738        let data = [1u8, 2, 3, 4, 5, 6, 7, 8];
739        let mut cr = CheckpointedReader::new(&data);
740        cr.save();
741        let _ = cr.read_u32().expect("_ should be present");
742        assert_eq!(cr.pos(), 4);
743        let rolled = cr.rollback();
744        assert!(rolled);
745        assert_eq!(cr.pos(), 0);
746        assert_eq!(cr.read_u8().expect("read_u8 should succeed"), 1);
747    }
748    #[test]
749    fn test_checkpointed_reader_no_checkpoint() {
750        let data = [10u8];
751        let mut cr = CheckpointedReader::new(&data);
752        let rolled = cr.rollback();
753        assert!(!rolled);
754    }
755    #[test]
756    fn test_serial_error() {
757        let e = SerialError::new(OleanError::UnexpectedEof, "reading header", 42);
758        let desc = e.describe();
759        assert!(desc.contains("reading header"));
760        assert!(desc.contains("42"));
761    }
762    #[test]
763    fn test_with_context_ok() {
764        let result = with_context("test", 0, || Ok::<u32, OleanError>(42));
765        assert_eq!(result.expect("result should be valid"), 42);
766    }
767    #[test]
768    fn test_with_context_err() {
769        let result = with_context("test ctx", 10, || {
770            Err::<u32, OleanError>(OleanError::UnexpectedEof)
771        });
772        let err = result.unwrap_err();
773        assert!(err.describe().contains("test ctx"));
774        assert_eq!(err.byte_offset, 10);
775    }
776    #[test]
777    fn test_serialized_sizes() {
778        let decl = SerialDecl::Theorem {
779            name: "foo".to_string(),
780            kind_tag: kind_tags::THEOREM,
781        };
782        let size = serialized_decl_size(&decl);
783        assert_eq!(size, 8);
784        let inductive = SerialDecl::Inductive {
785            name: "Nat".to_string(),
786            ctor_count: 2,
787            kind_tag: kind_tags::INDUCTIVE,
788        };
789        let isize = serialized_decl_size(&inductive);
790        assert_eq!(isize, 12);
791        let total = total_serialized_size(&[decl, inductive]);
792        assert_eq!(total, 20 + 8 + 12);
793    }
794}
795/// Merge two declaration lists using a strategy.
796#[allow(dead_code)]
797pub fn merge_decls(a: &[SerialDecl], b: &[SerialDecl], strategy: MergeStrategy) -> Vec<String> {
798    let a_names: Vec<&str> = a.iter().map(|d| d.name()).collect();
799    let b_names: Vec<&str> = b.iter().map(|d| d.name()).collect();
800    match strategy {
801        MergeStrategy::Union => {
802            let mut result: Vec<String> = a.iter().map(|d| d.name().to_string()).collect();
803            for d in b {
804                if !a_names.contains(&d.name()) {
805                    result.push(d.name().to_string());
806                }
807            }
808            result
809        }
810        MergeStrategy::Intersection => a
811            .iter()
812            .filter(|d| b_names.contains(&d.name()))
813            .map(|d| d.name().to_string())
814            .collect(),
815        MergeStrategy::PreferFirst => {
816            let mut result: Vec<String> = a.iter().map(|d| d.name().to_string()).collect();
817            for d in b {
818                if !a_names.contains(&d.name()) {
819                    result.push(d.name().to_string());
820                }
821            }
822            result
823        }
824        MergeStrategy::PreferSecond => {
825            let mut result: Vec<String> = b.iter().map(|d| d.name().to_string()).collect();
826            for d in a {
827                if !b_names.contains(&d.name()) {
828                    result.push(d.name().to_string());
829                }
830            }
831            result
832        }
833    }
834}
835/// Sorts a declaration list by name.
836#[allow(dead_code)]
837pub fn sort_decls_by_name(decls: &mut [SerialDecl]) {
838    decls.sort_by(|a, b| a.name().cmp(b.name()));
839}
840/// Returns deduplicated declarations (last occurrence wins).
841#[allow(dead_code)]
842pub fn dedup_decls(decls: Vec<SerialDecl>) -> Vec<SerialDecl> {
843    let mut seen: Vec<String> = Vec::new();
844    let mut result: Vec<SerialDecl> = Vec::new();
845    for d in decls {
846        if !seen.contains(&d.name().to_string()) {
847            seen.push(d.name().to_string());
848            result.push(d);
849        }
850    }
851    result
852}
853#[cfg(test)]
854mod tests_serial_extended6 {
855    use super::*;
856    #[test]
857    fn test_compatibility_checker() {
858        let checker = CompatibilityChecker::new(vec![1, 2]);
859        assert!(checker.is_compatible(1));
860        assert!(checker.is_compatible(2));
861        assert!(!checker.is_compatible(3));
862        assert_eq!(checker.latest(), Some(2));
863        assert!(checker.needs_upgrade(1, 2));
864        assert!(!checker.needs_upgrade(2, 1));
865    }
866    #[test]
867    fn test_merge_union() {
868        let a = vec![
869            SerialDecl::Theorem {
870                name: "a".to_string(),
871                kind_tag: kind_tags::THEOREM,
872            },
873            SerialDecl::Theorem {
874                name: "b".to_string(),
875                kind_tag: kind_tags::THEOREM,
876            },
877        ];
878        let b = vec![
879            SerialDecl::Theorem {
880                name: "b".to_string(),
881                kind_tag: kind_tags::THEOREM,
882            },
883            SerialDecl::Theorem {
884                name: "c".to_string(),
885                kind_tag: kind_tags::THEOREM,
886            },
887        ];
888        let result = merge_decls(&a, &b, MergeStrategy::Union);
889        assert!(result.contains(&"a".to_string()));
890        assert!(result.contains(&"b".to_string()));
891        assert!(result.contains(&"c".to_string()));
892        assert_eq!(result.len(), 3);
893    }
894    #[test]
895    fn test_merge_intersection() {
896        let a = vec![
897            SerialDecl::Theorem {
898                name: "shared".to_string(),
899                kind_tag: kind_tags::THEOREM,
900            },
901            SerialDecl::Theorem {
902                name: "a_only".to_string(),
903                kind_tag: kind_tags::THEOREM,
904            },
905        ];
906        let b = vec![
907            SerialDecl::Theorem {
908                name: "shared".to_string(),
909                kind_tag: kind_tags::THEOREM,
910            },
911            SerialDecl::Theorem {
912                name: "b_only".to_string(),
913                kind_tag: kind_tags::THEOREM,
914            },
915        ];
916        let result = merge_decls(&a, &b, MergeStrategy::Intersection);
917        assert_eq!(result, vec!["shared".to_string()]);
918    }
919    #[test]
920    fn test_sort_decls_by_name() {
921        let mut decls = vec![
922            SerialDecl::Other {
923                name: "z".to_string(),
924                kind_tag: kind_tags::OTHER,
925            },
926            SerialDecl::Other {
927                name: "a".to_string(),
928                kind_tag: kind_tags::OTHER,
929            },
930            SerialDecl::Other {
931                name: "m".to_string(),
932                kind_tag: kind_tags::OTHER,
933            },
934        ];
935        sort_decls_by_name(&mut decls);
936        assert_eq!(decls[0].name(), "a");
937        assert_eq!(decls[1].name(), "m");
938        assert_eq!(decls[2].name(), "z");
939    }
940    #[test]
941    fn test_dedup_decls() {
942        let decls = vec![
943            SerialDecl::Theorem {
944                name: "a".to_string(),
945                kind_tag: kind_tags::THEOREM,
946            },
947            SerialDecl::Axiom {
948                name: "b".to_string(),
949                kind_tag: kind_tags::AXIOM,
950            },
951            SerialDecl::Theorem {
952                name: "a".to_string(),
953                kind_tag: kind_tags::THEOREM,
954            },
955        ];
956        let deduped = dedup_decls(decls);
957        assert_eq!(deduped.len(), 2);
958        assert_eq!(deduped[0].name(), "a");
959        assert_eq!(deduped[1].name(), "b");
960    }
961}
962#[cfg(test)]
963mod tests_serial_extended7 {
964    use super::*;
965    #[test]
966    fn test_file_stats() {
967        let decls = vec![
968            SerialDecl::Theorem {
969                name: "t".to_string(),
970                kind_tag: kind_tags::THEOREM,
971            },
972            SerialDecl::Axiom {
973                name: "a".to_string(),
974                kind_tag: kind_tags::AXIOM,
975            },
976            SerialDecl::Inductive {
977                name: "I".to_string(),
978                ctor_count: 2,
979                kind_tag: kind_tags::INDUCTIVE,
980            },
981        ];
982        let stats = FileStats::from_decls(&decls, 300);
983        assert_eq!(stats.total_decls, 3);
984        assert_eq!(stats.theorems, 1);
985        assert_eq!(stats.axioms, 1);
986        assert_eq!(stats.inductives, 1);
987        assert!((stats.bytes_per_decl() - 100.0).abs() < 1e-9);
988        let s = stats.summary();
989        assert!(s.contains("total=3"));
990    }
991    #[test]
992    fn test_olean_archive() {
993        let mut archive = OleanArchive::new();
994        archive.add_file(
995            "Nat.lean",
996            vec![SerialDecl::Inductive {
997                name: "Nat".to_string(),
998                ctor_count: 2,
999                kind_tag: kind_tags::INDUCTIVE,
1000            }],
1001        );
1002        archive.add_file(
1003            "List.lean",
1004            vec![
1005                SerialDecl::Inductive {
1006                    name: "List".to_string(),
1007                    ctor_count: 2,
1008                    kind_tag: kind_tags::INDUCTIVE,
1009                },
1010                SerialDecl::Theorem {
1011                    name: "List.length_eq".to_string(),
1012                    kind_tag: kind_tags::THEOREM,
1013                },
1014            ],
1015        );
1016        assert_eq!(archive.total_decls(), 3);
1017        assert_eq!(archive.file_count(), 2);
1018        let (fname, decl) = archive
1019            .find_decl("List.length_eq")
1020            .expect("value should be present");
1021        assert_eq!(fname, "List.lean");
1022        assert_eq!(decl.kind_tag(), kind_tags::THEOREM);
1023        assert_eq!(archive.find_decl("Unknown"), None);
1024        assert!(!archive.is_empty());
1025    }
1026}
1027/// Groups declarations by namespace prefix (up to first dot).
1028#[allow(dead_code)]
1029pub fn group_by_namespace(decls: &[SerialDecl]) -> Vec<(String, Vec<&SerialDecl>)> {
1030    let mut groups: Vec<(String, Vec<&SerialDecl>)> = Vec::new();
1031    for d in decls {
1032        let ns = d.name().split('.').next().unwrap_or("_").to_string();
1033        if let Some(g) = groups.iter_mut().find(|(n, _)| *n == ns) {
1034            g.1.push(d);
1035        } else {
1036            groups.push((ns, vec![d]));
1037        }
1038    }
1039    groups
1040}
1041#[cfg(test)]
1042mod tests_serial_extended8 {
1043    use super::*;
1044    #[test]
1045    fn test_decl_diff() {
1046        let old: Vec<String> = vec!["a".to_string(), "b".to_string()];
1047        let new: Vec<String> = vec!["b".to_string(), "c".to_string()];
1048        let diff = DeclDiff::compute(&old, &new);
1049        assert_eq!(diff.added, vec!["c".to_string()]);
1050        assert_eq!(diff.removed, vec!["a".to_string()]);
1051        assert_eq!(diff.unchanged, vec!["b".to_string()]);
1052        assert!(diff.has_changes());
1053        let s = diff.summary();
1054        assert!(s.contains("+1 -1 =1"));
1055    }
1056    #[test]
1057    fn test_group_by_namespace() {
1058        let decls = vec![
1059            SerialDecl::Theorem {
1060                name: "Nat.add".to_string(),
1061                kind_tag: kind_tags::THEOREM,
1062            },
1063            SerialDecl::Theorem {
1064                name: "Nat.mul".to_string(),
1065                kind_tag: kind_tags::THEOREM,
1066            },
1067            SerialDecl::Theorem {
1068                name: "List.length".to_string(),
1069                kind_tag: kind_tags::THEOREM,
1070            },
1071        ];
1072        let groups = group_by_namespace(&decls);
1073        assert_eq!(groups.len(), 2);
1074        let nat_group = groups
1075            .iter()
1076            .find(|(ns, _)| ns == "Nat")
1077            .expect("nat_group should be present");
1078        assert_eq!(nat_group.1.len(), 2);
1079    }
1080}
1081#[cfg(test)]
1082mod tests_serial_diag {
1083    use super::*;
1084    #[test]
1085    fn test_format_diagnostics() {
1086        let data = serialize_decl_names(&["foo".to_string(), "bar".to_string()]);
1087        let diag = FormatDiagnostics::from_bytes(&data);
1088        assert!(diag.magic_ok);
1089        assert_eq!(diag.decl_count, 2);
1090        assert!(diag.is_well_formed());
1091        let report = diag.report();
1092        assert!(report.contains("magic=true"));
1093    }
1094    #[test]
1095    fn test_format_diagnostics_bad() {
1096        let bad = b"BADD1234";
1097        let diag = FormatDiagnostics::from_bytes(bad);
1098        assert!(!diag.magic_ok);
1099        assert!(!diag.is_well_formed());
1100    }
1101}
1102/// Encode a byte slice as hexadecimal for display.
1103#[allow(dead_code)]
1104pub fn to_hex(data: &[u8]) -> String {
1105    data.iter()
1106        .map(|b| format!("{:02x}", b))
1107        .collect::<Vec<_>>()
1108        .join("")
1109}
1110/// Decode a hexadecimal string to bytes.
1111#[allow(dead_code)]
1112pub fn from_hex(s: &str) -> Option<Vec<u8>> {
1113    if s.len() % 2 != 0 {
1114        return None;
1115    }
1116    (0..s.len() / 2)
1117        .map(|i| u8::from_str_radix(&s[i * 2..i * 2 + 2], 16).ok())
1118        .collect()
1119}
1120#[cfg(test)]
1121mod tests_hex {
1122    use super::*;
1123    #[test]
1124    fn test_hex_roundtrip() {
1125        let data = vec![0xDE, 0xAD, 0xBE, 0xEF];
1126        let hex = to_hex(&data);
1127        assert_eq!(hex, "deadbeef");
1128        assert_eq!(from_hex(&hex), Some(data));
1129    }
1130}
oxilean_kernel/serial/functions.rs

oxilean_kernel/serial/
functions.rs
