Skip to main content

oxilean_kernel/serial/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use std::io::Write;
6
7use super::functions::kind_tags;
8use super::functions::{
9    count_by_kind, has_valid_magic, peek_decl_count, peek_version, HEADER_SIZE, MAGIC, VERSION,
10};
11
12/// A checksummed binary blob validator.
13#[allow(dead_code)]
14pub struct BlobValidator {
15    expected_checksum: u32,
16}
17#[allow(dead_code)]
18impl BlobValidator {
19    /// Create a validator for a given expected checksum.
20    pub fn new(expected_checksum: u32) -> Self {
21        BlobValidator { expected_checksum }
22    }
23    /// Compute the FNV-1a 32-bit checksum of data.
24    pub fn compute_checksum(data: &[u8]) -> u32 {
25        let mut hash: u32 = 2_166_136_261;
26        for &b in data {
27            hash ^= b as u32;
28            hash = hash.wrapping_mul(16_777_619);
29        }
30        hash
31    }
32    /// Validate the given data against the expected checksum.
33    pub fn validate(&self, data: &[u8]) -> bool {
34        Self::compute_checksum(data) == self.expected_checksum
35    }
36    /// Return the expected checksum.
37    pub fn expected(&self) -> u32 {
38        self.expected_checksum
39    }
40}
41/// Statistics about a serialized file.
42#[allow(dead_code)]
43#[derive(Debug, Clone, Default)]
44pub struct FileStats {
45    pub total_decls: u32,
46    pub axioms: u32,
47    pub definitions: u32,
48    pub theorems: u32,
49    pub opaques: u32,
50    pub inductives: u32,
51    pub other: u32,
52    pub total_bytes: usize,
53}
54#[allow(dead_code)]
55impl FileStats {
56    /// Build stats from a list of declarations and total byte size.
57    pub fn from_decls(decls: &[SerialDecl], total_bytes: usize) -> Self {
58        let counts = count_by_kind(decls);
59        FileStats {
60            total_decls: decls.len() as u32,
61            axioms: counts[kind_tags::AXIOM as usize],
62            definitions: counts[kind_tags::DEFINITION as usize],
63            theorems: counts[kind_tags::THEOREM as usize],
64            opaques: counts[kind_tags::OPAQUE as usize],
65            inductives: counts[kind_tags::INDUCTIVE as usize],
66            other: counts[kind_tags::OTHER as usize],
67            total_bytes,
68        }
69    }
70    /// Return the average bytes per declaration.
71    pub fn bytes_per_decl(&self) -> f64 {
72        if self.total_decls == 0 {
73            0.0
74        } else {
75            self.total_bytes as f64 / self.total_decls as f64
76        }
77    }
78    /// Format a one-line summary.
79    pub fn summary(&self) -> String {
80        format!(
81            "total={} axioms={} defs={} theorems={} inductives={} bytes={}",
82            self.total_decls,
83            self.axioms,
84            self.definitions,
85            self.theorems,
86            self.inductives,
87            self.total_bytes
88        )
89    }
90}
91/// Streaming binary reader for the OleanC format.
92pub struct OleanReader<'a> {
93    data: &'a [u8],
94    pos: usize,
95}
96impl<'a> OleanReader<'a> {
97    /// Create a new reader over the given byte slice.
98    pub fn new(data: &'a [u8]) -> Self {
99        OleanReader { data, pos: 0 }
100    }
101    /// Number of bytes remaining to be read.
102    pub fn remaining(&self) -> usize {
103        self.data.len().saturating_sub(self.pos)
104    }
105    fn ensure(&self, n: usize) -> Result<(), OleanError> {
106        if self.remaining() < n {
107            Err(OleanError::UnexpectedEof)
108        } else {
109            Ok(())
110        }
111    }
112    /// Read and validate the OleanC file header.
113    pub fn read_header(&mut self) -> Result<OleanHeader, OleanError> {
114        self.ensure(HEADER_SIZE)?;
115        let magic = &self.data[self.pos..self.pos + 4];
116        if magic != MAGIC {
117            return Err(OleanError::InvalidMagic);
118        }
119        self.pos += 4;
120        let version = self.read_u32()?;
121        if version != VERSION {
122            return Err(OleanError::UnsupportedVersion(version));
123        }
124        let decl_count = self.read_u32()?;
125        let metadata_offset = self.read_u64()?;
126        Ok(OleanHeader {
127            version,
128            decl_count,
129            metadata_offset,
130        })
131    }
132    /// Read a length-prefixed UTF-8 string.
133    pub fn read_string(&mut self) -> Result<String, OleanError> {
134        let len = self.read_u32()? as usize;
135        self.ensure(len)?;
136        let bytes = self.data[self.pos..self.pos + len].to_vec();
137        self.pos += len;
138        Ok(String::from_utf8(bytes)?)
139    }
140    /// Read a single byte.
141    pub fn read_u8(&mut self) -> Result<u8, OleanError> {
142        self.ensure(1)?;
143        let v = self.data[self.pos];
144        self.pos += 1;
145        Ok(v)
146    }
147    /// Read a u32 in little-endian order.
148    pub fn read_u32(&mut self) -> Result<u32, OleanError> {
149        self.ensure(4)?;
150        let bytes: [u8; 4] = self.data[self.pos..self.pos + 4]
151            .try_into()
152            .expect("slice length must match array size");
153        self.pos += 4;
154        Ok(u32::from_le_bytes(bytes))
155    }
156    /// Read a u64 in little-endian order.
157    pub fn read_u64(&mut self) -> Result<u64, OleanError> {
158        self.ensure(8)?;
159        let bytes: [u8; 8] = self.data[self.pos..self.pos + 8]
160            .try_into()
161            .expect("slice length must match array size");
162        self.pos += 8;
163        Ok(u64::from_le_bytes(bytes))
164    }
165    /// Read an i64 in little-endian order.
166    pub fn read_i64(&mut self) -> Result<i64, OleanError> {
167        self.ensure(8)?;
168        let bytes: [u8; 8] = self.data[self.pos..self.pos + 8]
169            .try_into()
170            .expect("slice length must match array size");
171        self.pos += 8;
172        Ok(i64::from_le_bytes(bytes))
173    }
174    /// Read a bool from a single byte.
175    pub fn read_bool(&mut self) -> Result<bool, OleanError> {
176        Ok(self.read_u8()? != 0)
177    }
178}
179/// A section header for variable-length sections in a binary format.
180#[allow(dead_code)]
181#[derive(Debug, Clone)]
182pub struct SectionHeader {
183    pub tag: u8,
184    pub length: u32,
185    pub offset: u64,
186}
187#[allow(dead_code)]
188impl SectionHeader {
189    /// Create a new section header.
190    pub fn new(tag: u8, length: u32, offset: u64) -> Self {
191        SectionHeader {
192            tag,
193            length,
194            offset,
195        }
196    }
197    /// The size of a serialized section header (1 + 4 + 8 = 13 bytes).
198    pub const SIZE: usize = 13;
199    /// Write this header into a writer.
200    pub fn write(&self, w: &mut OleanWriter) {
201        w.write_u8(self.tag);
202        w.write_u32(self.length);
203        w.write_u64(self.offset);
204    }
205    /// Read a section header from a reader.
206    pub fn read(r: &mut OleanReader<'_>) -> Result<Self, OleanError> {
207        let tag = r.read_u8()?;
208        let length = r.read_u32()?;
209        let offset = r.read_u64()?;
210        Ok(SectionHeader {
211            tag,
212            length,
213            offset,
214        })
215    }
216}
217/// A streaming writer that computes a checksum as it writes.
218#[allow(dead_code)]
219pub struct ChecksummedWriter {
220    inner: OleanWriter,
221    running_hash: u32,
222}
223#[allow(dead_code)]
224impl ChecksummedWriter {
225    /// Create a new checksummed writer.
226    pub fn new() -> Self {
227        ChecksummedWriter {
228            inner: OleanWriter::new(),
229            running_hash: 2_166_136_261,
230        }
231    }
232    /// Write a byte, updating the checksum.
233    pub fn write_byte(&mut self, b: u8) {
234        self.running_hash ^= b as u32;
235        self.running_hash = self.running_hash.wrapping_mul(16_777_619);
236        self.inner.write_u8(b);
237    }
238    /// Write multiple bytes.
239    pub fn write_bytes(&mut self, data: &[u8]) {
240        for &b in data {
241            self.write_byte(b);
242        }
243    }
244    /// Write a u32.
245    pub fn write_u32(&mut self, v: u32) {
246        self.write_bytes(&v.to_le_bytes());
247    }
248    /// Write a u64.
249    pub fn write_u64(&mut self, v: u64) {
250        self.write_bytes(&v.to_le_bytes());
251    }
252    /// Write a string (length-prefixed).
253    pub fn write_string(&mut self, s: &str) {
254        self.write_u32(s.len() as u32);
255        self.write_bytes(s.as_bytes());
256    }
257    /// Return the current running checksum.
258    pub fn current_checksum(&self) -> u32 {
259        self.running_hash
260    }
261    /// Finish and return the data with appended checksum.
262    pub fn finish_with_checksum(mut self) -> Vec<u8> {
263        let checksum = self.running_hash;
264        self.inner.write_u32(checksum);
265        self.inner.finish()
266    }
267    /// Return the number of bytes written (excluding checksum trailer).
268    pub fn len(&self) -> usize {
269        self.inner.len()
270    }
271    /// Returns whether the collection is empty.
272    pub fn is_empty(&self) -> bool {
273        self.len() == 0
274    }
275}
276/// Versioned name → id mapping for a name table section.
277#[allow(dead_code)]
278pub struct NameTable {
279    entries: Vec<(String, u32)>,
280}
281#[allow(dead_code)]
282impl NameTable {
283    /// Create an empty name table.
284    pub fn new() -> Self {
285        NameTable {
286            entries: Vec::new(),
287        }
288    }
289    /// Intern a name; returns the assigned id.
290    pub fn intern(&mut self, name: &str) -> u32 {
291        if let Some(&(_, id)) = self.entries.iter().find(|(n, _)| n == name) {
292            return id;
293        }
294        let id = self.entries.len() as u32;
295        self.entries.push((name.to_string(), id));
296        id
297    }
298    /// Look up a name by id.
299    pub fn lookup_id(&self, id: u32) -> Option<&str> {
300        self.entries
301            .iter()
302            .find(|(_, i)| *i == id)
303            .map(|(n, _)| n.as_str())
304    }
305    /// Look up an id by name.
306    pub fn lookup_name(&self, name: &str) -> Option<u32> {
307        self.entries
308            .iter()
309            .find(|(n, _)| n == name)
310            .map(|(_, id)| *id)
311    }
312    /// Serialize this table into an OleanWriter.
313    pub fn write(&self, w: &mut OleanWriter) {
314        w.write_u32(self.entries.len() as u32);
315        for (name, id) in &self.entries {
316            w.write_string(name);
317            w.write_u32(*id);
318        }
319    }
320    /// Deserialize from a reader.
321    pub fn read(r: &mut OleanReader<'_>) -> Result<Self, OleanError> {
322        let count = r.read_u32()? as usize;
323        let mut t = NameTable::new();
324        for _ in 0..count {
325            let name = r.read_string()?;
326            let id = r.read_u32()?;
327            t.entries.push((name, id));
328        }
329        Ok(t)
330    }
331    /// Return the number of interned names.
332    pub fn len(&self) -> usize {
333        self.entries.len()
334    }
335    /// Return whether the table is empty.
336    pub fn is_empty(&self) -> bool {
337        self.entries.is_empty()
338    }
339    /// Return all names in intern order.
340    pub fn names(&self) -> Vec<&str> {
341        self.entries.iter().map(|(n, _)| n.as_str()).collect()
342    }
343}
344/// A compact encoding for small sets of declaration kinds.
345#[allow(dead_code)]
346pub struct DeclKindSet {
347    mask: u8,
348}
349#[allow(dead_code)]
350impl DeclKindSet {
351    /// Create an empty set.
352    pub fn new() -> Self {
353        DeclKindSet { mask: 0 }
354    }
355    /// Add a kind tag to the set.
356    pub fn add(&mut self, tag: u8) {
357        if tag < 8 {
358            self.mask |= 1 << tag;
359        }
360    }
361    /// Return whether a tag is in the set.
362    pub fn contains(&self, tag: u8) -> bool {
363        tag < 8 && (self.mask >> tag) & 1 != 0
364    }
365    /// Return the raw bitmask.
366    pub fn mask(&self) -> u8 {
367        self.mask
368    }
369    /// Return the number of distinct kinds in the set.
370    pub fn count(&self) -> u32 {
371        self.mask.count_ones()
372    }
373    /// Return whether the set is empty.
374    pub fn is_empty(&self) -> bool {
375        self.mask == 0
376    }
377    /// Write to a writer.
378    pub fn write(&self, w: &mut OleanWriter) {
379        w.write_u8(self.mask);
380    }
381    /// Read from a reader.
382    pub fn read(r: &mut OleanReader<'_>) -> Result<Self, OleanError> {
383        Ok(DeclKindSet { mask: r.read_u8()? })
384    }
385}
386/// Error type for OleanC serialization/deserialization.
387#[derive(Debug)]
388pub enum OleanError {
389    InvalidMagic,
390    UnsupportedVersion(u32),
391    UnexpectedEof,
392    InvalidUtf8(std::string::FromUtf8Error),
393    InvalidDeclKind(u8),
394    IoError(std::io::Error),
395}
396/// A string interning table for efficient repeated string serialization.
397#[allow(dead_code)]
398pub struct StringPool {
399    strings: Vec<String>,
400}
401#[allow(dead_code)]
402impl StringPool {
403    /// Create an empty pool.
404    pub fn new() -> Self {
405        StringPool {
406            strings: Vec::new(),
407        }
408    }
409    /// Intern a string, returning its index.
410    pub fn intern(&mut self, s: &str) -> u32 {
411        if let Some(idx) = self.strings.iter().position(|x| x == s) {
412            return idx as u32;
413        }
414        let idx = self.strings.len() as u32;
415        self.strings.push(s.to_string());
416        idx
417    }
418    /// Retrieve a string by index.
419    pub fn get(&self, idx: u32) -> Option<&str> {
420        self.strings.get(idx as usize).map(|s| s.as_str())
421    }
422    /// Return the number of interned strings.
423    pub fn len(&self) -> usize {
424        self.strings.len()
425    }
426    /// Return whether the pool is empty.
427    pub fn is_empty(&self) -> bool {
428        self.strings.is_empty()
429    }
430    /// Serialize the pool.
431    pub fn write(&self, w: &mut OleanWriter) {
432        w.write_u32(self.strings.len() as u32);
433        for s in &self.strings {
434            w.write_string(s);
435        }
436    }
437    /// Deserialize a pool.
438    pub fn read(r: &mut OleanReader<'_>) -> Result<Self, OleanError> {
439        let count = r.read_u32()? as usize;
440        let mut pool = StringPool::new();
441        for _ in 0..count {
442            let s = r.read_string()?;
443            pool.strings.push(s);
444        }
445        Ok(pool)
446    }
447    /// Return all strings.
448    pub fn all_strings(&self) -> &[String] {
449        &self.strings
450    }
451}
452/// An index of declaration names for fast lookup.
453#[allow(dead_code)]
454pub struct DeclIndex {
455    names: Vec<(String, u32)>,
456}
457#[allow(dead_code)]
458impl DeclIndex {
459    /// Create an empty index.
460    pub fn new() -> Self {
461        DeclIndex { names: Vec::new() }
462    }
463    /// Add a name with its byte offset in the binary file.
464    pub fn add(&mut self, name: &str, offset: u32) {
465        self.names.push((name.to_string(), offset));
466    }
467    /// Look up the offset for a name.
468    pub fn find_offset(&self, name: &str) -> Option<u32> {
469        self.names.iter().find(|(n, _)| n == name).map(|(_, o)| *o)
470    }
471    /// Return whether the index contains a name.
472    pub fn contains(&self, name: &str) -> bool {
473        self.names.iter().any(|(n, _)| n == name)
474    }
475    /// Return the number of indexed names.
476    pub fn len(&self) -> usize {
477        self.names.len()
478    }
479    /// Return whether the index is empty.
480    pub fn is_empty(&self) -> bool {
481        self.names.is_empty()
482    }
483    /// Return names in sorted order for binary search.
484    pub fn sorted_names(&self) -> Vec<&str> {
485        let mut v: Vec<&str> = self.names.iter().map(|(n, _)| n.as_str()).collect();
486        v.sort_unstable();
487        v
488    }
489    /// Binary search for a name (requires sorted order).
490    pub fn binary_search(&self, name: &str) -> Option<u32> {
491        let mut lo = 0usize;
492        let mut hi = self.names.len();
493        while lo < hi {
494            let mid = lo + (hi - lo) / 2;
495            match self.names[mid].0.as_str().cmp(name) {
496                std::cmp::Ordering::Equal => return Some(self.names[mid].1),
497                std::cmp::Ordering::Less => lo = mid + 1,
498                std::cmp::Ordering::Greater => hi = mid,
499            }
500        }
501        None
502    }
503    /// Serialize the index.
504    pub fn write(&self, w: &mut OleanWriter) {
505        w.write_u32(self.names.len() as u32);
506        for (name, offset) in &self.names {
507            w.write_string(name);
508            w.write_u32(*offset);
509        }
510    }
511    /// Deserialize the index.
512    pub fn read(r: &mut OleanReader<'_>) -> Result<Self, OleanError> {
513        let count = r.read_u32()? as usize;
514        let mut idx = DeclIndex::new();
515        for _ in 0..count {
516            let name = r.read_string()?;
517            let offset = r.read_u32()?;
518            idx.names.push((name, offset));
519        }
520        Ok(idx)
521    }
522}
523/// Writes a tagged union of declaration metadata.
524#[allow(dead_code)]
525pub struct MetadataWriter {
526    buf: OleanWriter,
527    entry_count: u32,
528}
529#[allow(dead_code)]
530impl MetadataWriter {
531    /// Create a new metadata writer.
532    pub fn new() -> Self {
533        MetadataWriter {
534            buf: OleanWriter::new(),
535            entry_count: 0,
536        }
537    }
538    /// Write a key-value pair where value is a string.
539    pub fn write_str_entry(&mut self, key: &str, value: &str) {
540        self.buf.write_u8(0);
541        self.buf.write_string(key);
542        self.buf.write_string(value);
543        self.entry_count += 1;
544    }
545    /// Write a key-value pair where value is a u64.
546    pub fn write_u64_entry(&mut self, key: &str, value: u64) {
547        self.buf.write_u8(1);
548        self.buf.write_string(key);
549        self.buf.write_u64(value);
550        self.entry_count += 1;
551    }
552    /// Write a key-value pair where value is a bool.
553    pub fn write_bool_entry(&mut self, key: &str, value: bool) {
554        self.buf.write_u8(2);
555        self.buf.write_string(key);
556        self.buf.write_bool(value);
557        self.entry_count += 1;
558    }
559    /// Return the number of entries written.
560    pub fn entry_count(&self) -> u32 {
561        self.entry_count
562    }
563    /// Finish and produce a section with a count prefix.
564    pub fn finish(self) -> Vec<u8> {
565        let mut w = OleanWriter::new();
566        w.write_u32(self.entry_count);
567        let inner_bytes = self.buf.finish();
568        w.buf.extend_from_slice(&inner_bytes);
569        w.finish()
570    }
571}
572/// A table of section headers for a multi-section binary file.
573#[allow(dead_code)]
574pub struct SectionTable {
575    headers: Vec<SectionHeader>,
576}
577#[allow(dead_code)]
578impl SectionTable {
579    /// Create an empty section table.
580    pub fn new() -> Self {
581        SectionTable {
582            headers: Vec::new(),
583        }
584    }
585    /// Add a section header.
586    pub fn add(&mut self, header: SectionHeader) {
587        self.headers.push(header);
588    }
589    /// Look up a section header by tag.
590    pub fn find(&self, tag: u8) -> Option<&SectionHeader> {
591        self.headers.iter().find(|h| h.tag == tag)
592    }
593    /// Return the number of sections.
594    pub fn len(&self) -> usize {
595        self.headers.len()
596    }
597    /// Return whether the table is empty.
598    pub fn is_empty(&self) -> bool {
599        self.headers.is_empty()
600    }
601    /// Serialize the entire table.
602    pub fn write(&self, w: &mut OleanWriter) {
603        w.write_u32(self.headers.len() as u32);
604        for h in &self.headers {
605            h.write(w);
606        }
607    }
608    /// Deserialize a section table from a reader.
609    pub fn read(r: &mut OleanReader<'_>) -> Result<Self, OleanError> {
610        let count = r.read_u32()? as usize;
611        let mut table = SectionTable::new();
612        for _ in 0..count {
613            table.add(SectionHeader::read(r)?);
614        }
615        Ok(table)
616    }
617}
618/// An OleanReader with checkpoint/rollback support.
619#[allow(dead_code)]
620pub struct CheckpointedReader<'a> {
621    data: &'a [u8],
622    pos: usize,
623    checkpoint: Option<usize>,
624}
625#[allow(dead_code)]
626impl<'a> CheckpointedReader<'a> {
627    /// Create a new reader.
628    pub fn new(data: &'a [u8]) -> Self {
629        CheckpointedReader {
630            data,
631            pos: 0,
632            checkpoint: None,
633        }
634    }
635    /// Save the current position as a checkpoint.
636    pub fn save(&mut self) {
637        self.checkpoint = Some(self.pos);
638    }
639    /// Roll back to the last checkpoint.
640    pub fn rollback(&mut self) -> bool {
641        if let Some(cp) = self.checkpoint {
642            self.pos = cp;
643            true
644        } else {
645            false
646        }
647    }
648    /// Return remaining bytes.
649    pub fn remaining(&self) -> usize {
650        self.data.len().saturating_sub(self.pos)
651    }
652    /// Read a u8.
653    pub fn read_u8(&mut self) -> Result<u8, OleanError> {
654        if self.remaining() < 1 {
655            return Err(OleanError::UnexpectedEof);
656        }
657        let v = self.data[self.pos];
658        self.pos += 1;
659        Ok(v)
660    }
661    /// Read a u32 little-endian.
662    pub fn read_u32(&mut self) -> Result<u32, OleanError> {
663        if self.remaining() < 4 {
664            return Err(OleanError::UnexpectedEof);
665        }
666        let bytes: [u8; 4] = self.data[self.pos..self.pos + 4]
667            .try_into()
668            .expect("slice length must match array size");
669        self.pos += 4;
670        Ok(u32::from_le_bytes(bytes))
671    }
672    /// Read a length-prefixed string.
673    pub fn read_string(&mut self) -> Result<String, OleanError> {
674        let len = self.read_u32()? as usize;
675        if self.remaining() < len {
676            return Err(OleanError::UnexpectedEof);
677        }
678        let s = String::from_utf8(self.data[self.pos..self.pos + len].to_vec())?;
679        self.pos += len;
680        Ok(s)
681    }
682    /// Current position in bytes.
683    pub fn pos(&self) -> usize {
684        self.pos
685    }
686}
687/// A buffered writer that flushes to a Vec when full.
688#[allow(dead_code)]
689pub struct BufferedOleanWriter {
690    buf: Vec<u8>,
691    flush_threshold: usize,
692    total_written: usize,
693}
694#[allow(dead_code)]
695impl BufferedOleanWriter {
696    /// Create a buffered writer with a given flush threshold.
697    pub fn new(flush_threshold: usize) -> Self {
698        BufferedOleanWriter {
699            buf: Vec::with_capacity(flush_threshold),
700            flush_threshold,
701            total_written: 0,
702        }
703    }
704    /// Write a byte.
705    pub fn write_u8(&mut self, b: u8) {
706        self.buf.push(b);
707        self.total_written += 1;
708    }
709    /// Write a u32.
710    pub fn write_u32(&mut self, v: u32) {
711        for b in v.to_le_bytes() {
712            self.write_u8(b);
713        }
714    }
715    /// Write a u64.
716    pub fn write_u64(&mut self, v: u64) {
717        for b in v.to_le_bytes() {
718            self.write_u8(b);
719        }
720    }
721    /// Write a length-prefixed string.
722    pub fn write_string(&mut self, s: &str) {
723        self.write_u32(s.len() as u32);
724        for b in s.as_bytes() {
725            self.write_u8(*b);
726        }
727    }
728    /// Return total bytes written.
729    pub fn total_written(&self) -> usize {
730        self.total_written
731    }
732    /// Return current buffered bytes (not yet flushed to output).
733    pub fn buffered(&self) -> usize {
734        self.buf.len()
735    }
736    /// Flush the buffer and return all accumulated bytes.
737    pub fn flush(self) -> Vec<u8> {
738        self.buf
739    }
740    /// Return whether the buffer is over the flush threshold.
741    pub fn should_flush(&self) -> bool {
742        self.buf.len() >= self.flush_threshold
743    }
744}
745/// A merge strategy for combining two serialized declaration lists.
746#[allow(dead_code)]
747pub enum MergeStrategy {
748    /// Keep all declarations from both lists.
749    Union,
750    /// Keep only declarations present in both (by name).
751    Intersection,
752    /// Prefer the first list; only add from second if not in first.
753    PreferFirst,
754    /// Prefer the second list; only add from first if not in second.
755    PreferSecond,
756}
757/// Diagnostic information about a parsed OleanC file.
758#[allow(dead_code)]
759#[derive(Debug, Clone)]
760pub struct FormatDiagnostics {
761    pub version: u32,
762    pub decl_count: u32,
763    pub total_bytes: usize,
764    pub magic_ok: bool,
765    pub checksum_ok: Option<bool>,
766    pub sections: Vec<String>,
767}
768#[allow(dead_code)]
769impl FormatDiagnostics {
770    /// Parse diagnostics from raw bytes.
771    pub fn from_bytes(data: &[u8]) -> Self {
772        let magic_ok = has_valid_magic(data);
773        let version = peek_version(data).unwrap_or(0);
774        let decl_count = peek_decl_count(data).unwrap_or(0);
775        FormatDiagnostics {
776            version,
777            decl_count,
778            total_bytes: data.len(),
779            magic_ok,
780            checksum_ok: None,
781            sections: Vec::new(),
782        }
783    }
784    /// Format a diagnostic report.
785    pub fn report(&self) -> String {
786        format!(
787            "magic={} version={} decls={} bytes={}",
788            self.magic_ok, self.version, self.decl_count, self.total_bytes
789        )
790    }
791    /// Return whether the file appears well-formed.
792    pub fn is_well_formed(&self) -> bool {
793        self.magic_ok && self.version > 0
794    }
795}
796/// Parsed OleanC file header.
797#[derive(Debug, Clone)]
798pub struct OleanHeader {
799    pub version: u32,
800    pub decl_count: u32,
801    pub metadata_offset: u64,
802}
803/// A serializable record for a kernel declaration.
804#[derive(Debug, Clone, PartialEq)]
805pub enum SerialDecl {
806    Axiom {
807        name: String,
808        kind_tag: u8,
809    },
810    Definition {
811        name: String,
812        kind_tag: u8,
813    },
814    Theorem {
815        name: String,
816        kind_tag: u8,
817    },
818    Opaque {
819        name: String,
820        kind_tag: u8,
821    },
822    Inductive {
823        name: String,
824        ctor_count: u32,
825        kind_tag: u8,
826    },
827    Other {
828        name: String,
829        kind_tag: u8,
830    },
831}
832impl SerialDecl {
833    /// Return the declaration's name.
834    pub fn name(&self) -> &str {
835        match self {
836            SerialDecl::Axiom { name, .. } => name,
837            SerialDecl::Definition { name, .. } => name,
838            SerialDecl::Theorem { name, .. } => name,
839            SerialDecl::Opaque { name, .. } => name,
840            SerialDecl::Inductive { name, .. } => name,
841            SerialDecl::Other { name, .. } => name,
842        }
843    }
844    /// Return the declaration's kind tag byte.
845    pub fn kind_tag(&self) -> u8 {
846        match self {
847            SerialDecl::Axiom { kind_tag, .. } => *kind_tag,
848            SerialDecl::Definition { kind_tag, .. } => *kind_tag,
849            SerialDecl::Theorem { kind_tag, .. } => *kind_tag,
850            SerialDecl::Opaque { kind_tag, .. } => *kind_tag,
851            SerialDecl::Inductive { kind_tag, .. } => *kind_tag,
852            SerialDecl::Other { kind_tag, .. } => *kind_tag,
853        }
854    }
855}
856/// Streaming binary writer for the OleanC format.
857pub struct OleanWriter {
858    buf: Vec<u8>,
859}
860impl OleanWriter {
861    /// Create a new, empty writer.
862    pub fn new() -> Self {
863        OleanWriter { buf: Vec::new() }
864    }
865    /// Write the OleanC file header.
866    ///
867    /// The metadata section offset is set to `HEADER_SIZE` (immediately after the header)
868    /// when no additional body is present; callers may update it afterwards.
869    pub fn write_header(&mut self, decl_count: u32) -> &mut Self {
870        self.buf.extend_from_slice(MAGIC);
871        self.write_u32(VERSION);
872        self.write_u32(decl_count);
873        self.write_u64(HEADER_SIZE as u64);
874        self
875    }
876    /// Write a length-prefixed UTF-8 string (u32 length + bytes).
877    pub fn write_string(&mut self, s: &str) -> &mut Self {
878        let bytes = s.as_bytes();
879        self.write_u32(bytes.len() as u32);
880        self.buf.extend_from_slice(bytes);
881        self
882    }
883    /// Write a single byte.
884    pub fn write_u8(&mut self, v: u8) -> &mut Self {
885        self.buf.push(v);
886        self
887    }
888    /// Write a u32 in little-endian order.
889    pub fn write_u32(&mut self, v: u32) -> &mut Self {
890        self.buf.extend_from_slice(&v.to_le_bytes());
891        self
892    }
893    /// Write a u64 in little-endian order.
894    pub fn write_u64(&mut self, v: u64) -> &mut Self {
895        self.buf.extend_from_slice(&v.to_le_bytes());
896        self
897    }
898    /// Write an i64 in little-endian order.
899    pub fn write_i64(&mut self, v: i64) -> &mut Self {
900        self.buf.extend_from_slice(&v.to_le_bytes());
901        self
902    }
903    /// Write a bool as a single byte (0 or 1).
904    pub fn write_bool(&mut self, v: bool) -> &mut Self {
905        self.write_u8(if v { 1 } else { 0 })
906    }
907    /// Return the current number of bytes written.
908    pub fn len(&self) -> usize {
909        self.buf.len()
910    }
911    /// Return `true` if no bytes have been written yet.
912    pub fn is_empty(&self) -> bool {
913        self.buf.is_empty()
914    }
915    /// Consume the writer and return the accumulated bytes.
916    pub fn finish(self) -> Vec<u8> {
917        self.buf
918    }
919}
920/// A delta-compressed list of u32 values (successive differences).
921#[allow(dead_code)]
922pub struct DeltaList {
923    deltas: Vec<i32>,
924    base: u32,
925}
926#[allow(dead_code)]
927impl DeltaList {
928    /// Encode a sorted list of u32 values as delta-compressed form.
929    pub fn encode(values: &[u32]) -> Self {
930        let mut deltas = Vec::with_capacity(values.len());
931        let mut prev = 0u32;
932        for &v in values {
933            let delta = v as i64 - prev as i64;
934            deltas.push(delta as i32);
935            prev = v;
936        }
937        DeltaList {
938            deltas,
939            base: values.first().copied().unwrap_or(0),
940        }
941    }
942    /// Decode back to a list of u32 values.
943    pub fn decode(&self) -> Vec<u32> {
944        let mut result = Vec::with_capacity(self.deltas.len());
945        let mut cur: i64 = 0;
946        for &d in &self.deltas {
947            cur += d as i64;
948            result.push(cur as u32);
949        }
950        result
951    }
952    /// Return the number of encoded values.
953    pub fn len(&self) -> usize {
954        self.deltas.len()
955    }
956    /// Return whether the list is empty.
957    pub fn is_empty(&self) -> bool {
958        self.deltas.is_empty()
959    }
960    /// Write to an OleanWriter.
961    pub fn write(&self, w: &mut OleanWriter) {
962        w.write_u32(self.base);
963        w.write_u32(self.deltas.len() as u32);
964        for &d in &self.deltas {
965            w.write_i64(d as i64);
966        }
967    }
968    /// Read from an OleanReader.
969    pub fn read(r: &mut OleanReader<'_>) -> Result<Self, OleanError> {
970        let base = r.read_u32()?;
971        let count = r.read_u32()? as usize;
972        let mut deltas = Vec::with_capacity(count);
973        for _ in 0..count {
974            deltas.push(r.read_i64()? as i32);
975        }
976        Ok(DeltaList { deltas, base })
977    }
978}
979/// Reads metadata entries produced by `MetadataWriter`.
980#[allow(dead_code)]
981pub struct MetadataReader<'a> {
982    inner: OleanReader<'a>,
983    count: u32,
984    read: u32,
985}
986#[allow(dead_code)]
987impl<'a> MetadataReader<'a> {
988    /// Create a reader from raw metadata bytes.
989    pub fn new(data: &'a [u8]) -> Result<Self, OleanError> {
990        let mut r = OleanReader::new(data);
991        let count = r.read_u32()?;
992        Ok(MetadataReader {
993            inner: r,
994            count,
995            read: 0,
996        })
997    }
998    /// Return whether more entries are available.
999    pub fn has_next(&self) -> bool {
1000        self.read < self.count
1001    }
1002    /// Read the next (key, value) pair.
1003    pub fn next_entry(&mut self) -> Result<(String, MetadataValue), OleanError> {
1004        let tag = self.inner.read_u8()?;
1005        let key = self.inner.read_string()?;
1006        let value = match tag {
1007            0 => MetadataValue::Str(self.inner.read_string()?),
1008            1 => MetadataValue::U64(self.inner.read_u64()?),
1009            2 => MetadataValue::Bool(self.inner.read_bool()?),
1010            _ => return Err(OleanError::InvalidDeclKind(tag)),
1011        };
1012        self.read += 1;
1013        Ok((key, value))
1014    }
1015    /// Read all entries into a vec.
1016    pub fn read_all(&mut self) -> Result<Vec<(String, MetadataValue)>, OleanError> {
1017        let mut entries = Vec::new();
1018        while self.has_next() {
1019            entries.push(self.next_entry()?);
1020        }
1021        Ok(entries)
1022    }
1023}
1024/// A named section within an extended binary file.
1025#[allow(dead_code)]
1026pub struct BinarySection {
1027    pub header: SectionHeader,
1028    pub data: Vec<u8>,
1029}
1030#[allow(dead_code)]
1031impl BinarySection {
1032    /// Create a new section with raw data.
1033    pub fn new(tag: u8, data: Vec<u8>, offset: u64) -> Self {
1034        let length = data.len() as u32;
1035        BinarySection {
1036            header: SectionHeader::new(tag, length, offset),
1037            data,
1038        }
1039    }
1040    /// Serialize the section to bytes (header + data).
1041    pub fn to_bytes(&self) -> Vec<u8> {
1042        let mut w = OleanWriter::new();
1043        self.header.write(&mut w);
1044        w.finish()
1045            .into_iter()
1046            .chain(self.data.iter().copied())
1047            .collect()
1048    }
1049    /// Return the section tag.
1050    pub fn tag(&self) -> u8 {
1051        self.header.tag
1052    }
1053    /// Return the section data length.
1054    pub fn data_len(&self) -> usize {
1055        self.data.len()
1056    }
1057}
1058/// A metadata entry value.
1059#[allow(dead_code)]
1060#[derive(Debug, Clone)]
1061pub enum MetadataValue {
1062    Str(String),
1063    U64(u64),
1064    Bool(bool),
1065}
1066/// A structured error with context for serialization failures.
1067#[allow(dead_code)]
1068#[derive(Debug)]
1069pub struct SerialError {
1070    pub inner: OleanError,
1071    pub context: String,
1072    pub byte_offset: usize,
1073}
1074#[allow(dead_code)]
1075impl SerialError {
1076    /// Create a new serial error.
1077    pub fn new(inner: OleanError, context: impl Into<String>, byte_offset: usize) -> Self {
1078        SerialError {
1079            inner,
1080            context: context.into(),
1081            byte_offset,
1082        }
1083    }
1084    /// Format a human-readable description.
1085    pub fn describe(&self) -> String {
1086        format!(
1087            "{} at byte {}: {}",
1088            self.context, self.byte_offset, self.inner
1089        )
1090    }
1091}
1092/// Checks binary compatibility between two OleanC files.
1093#[allow(dead_code)]
1094pub struct CompatibilityChecker {
1095    known_versions: Vec<u32>,
1096}
1097#[allow(dead_code)]
1098impl CompatibilityChecker {
1099    /// Create a checker that knows about the given versions.
1100    pub fn new(known_versions: Vec<u32>) -> Self {
1101        CompatibilityChecker { known_versions }
1102    }
1103    /// Return whether the version is known-compatible.
1104    pub fn is_compatible(&self, version: u32) -> bool {
1105        self.known_versions.contains(&version)
1106    }
1107    /// Return the latest known version.
1108    pub fn latest(&self) -> Option<u32> {
1109        self.known_versions.iter().max().copied()
1110    }
1111    /// Return whether an upgrade is needed from `old` to `new`.
1112    pub fn needs_upgrade(&self, old: u32, new: u32) -> bool {
1113        old < new && self.is_compatible(new)
1114    }
1115}
1116/// Computes the diff between two name lists.
1117#[allow(dead_code)]
1118pub struct DeclDiff {
1119    pub added: Vec<String>,
1120    pub removed: Vec<String>,
1121    pub unchanged: Vec<String>,
1122}
1123#[allow(dead_code)]
1124impl DeclDiff {
1125    /// Compute the diff between `old_names` and `new_names`.
1126    pub fn compute(old_names: &[String], new_names: &[String]) -> Self {
1127        let added = new_names
1128            .iter()
1129            .filter(|n| !old_names.contains(n))
1130            .cloned()
1131            .collect();
1132        let removed = old_names
1133            .iter()
1134            .filter(|n| !new_names.contains(n))
1135            .cloned()
1136            .collect();
1137        let unchanged = old_names
1138            .iter()
1139            .filter(|n| new_names.contains(n))
1140            .cloned()
1141            .collect();
1142        DeclDiff {
1143            added,
1144            removed,
1145            unchanged,
1146        }
1147    }
1148    /// Return whether there are any changes.
1149    pub fn has_changes(&self) -> bool {
1150        !self.added.is_empty() || !self.removed.is_empty()
1151    }
1152    /// Format a summary.
1153    pub fn summary(&self) -> String {
1154        format!(
1155            "+{} -{} ={} declarations",
1156            self.added.len(),
1157            self.removed.len(),
1158            self.unchanged.len()
1159        )
1160    }
1161}
1162/// A multi-file archive of OleanC declarations.
1163#[allow(dead_code)]
1164pub struct OleanArchive {
1165    files: Vec<(String, Vec<SerialDecl>)>,
1166}
1167#[allow(dead_code)]
1168impl OleanArchive {
1169    /// Create an empty archive.
1170    pub fn new() -> Self {
1171        OleanArchive { files: Vec::new() }
1172    }
1173    /// Add a file to the archive.
1174    pub fn add_file(&mut self, name: impl Into<String>, decls: Vec<SerialDecl>) {
1175        self.files.push((name.into(), decls));
1176    }
1177    /// Return the total number of declarations across all files.
1178    pub fn total_decls(&self) -> usize {
1179        self.files.iter().map(|(_, d)| d.len()).sum()
1180    }
1181    /// Return the number of files.
1182    pub fn file_count(&self) -> usize {
1183        self.files.len()
1184    }
1185    /// Return all declaration names across all files.
1186    pub fn all_names(&self) -> Vec<&str> {
1187        self.files
1188            .iter()
1189            .flat_map(|(_, d)| d.iter().map(|decl| decl.name()))
1190            .collect()
1191    }
1192    /// Find a declaration by name across all files.
1193    pub fn find_decl(&self, name: &str) -> Option<(&str, &SerialDecl)> {
1194        for (fname, decls) in &self.files {
1195            if let Some(d) = decls.iter().find(|d| d.name() == name) {
1196                return Some((fname.as_str(), d));
1197            }
1198        }
1199        None
1200    }
1201    /// Return whether the archive is empty.
1202    pub fn is_empty(&self) -> bool {
1203        self.files.is_empty()
1204    }
1205}