Method parse_lazy_index

crates/ixon/src/serialize.rs:1532–1637

Parse an `.ixe` buffer into a metadata-light, **zero-copy** index for the anon/lazy check path (see [`LazyIndex`]). Mirrors [`Env::get`]'s section walk and reuses the same battle-tested parsers (so every metadata variant — e.g. `CallSite` — is handled), but: - constants are recorded as `(addr, offset, len)` windows into `data` rather than copied/stored, and their bodies are never parsed here; - t

(data: &[u8])

// ============================================================================
// Env serialization
// ============================================================================

use super::comm::Comm;
use super::env::{Env, LazyConstSlice, LazyIndex, LazyNamed};
#[cfg(not(target_arch = "riscv64"))]
use super::merkle::merkle_root_canonical_sorted;
use super::merkle::{merkle_root_canonical, zero_address};

impl Env {
  /// Tag4 flag for Env (0xE).
  pub const FLAG: u8 = 0xE;

  /// `.ixe` format version, carried in the header's Tag4 size field
  /// (versions < 8 cost zero extra bytes). Any change to serialized
  /// bytes bumps this. Readers reject a mismatch; there is no
  /// back-compat reading of old versions — `.ixe` files are
  /// regenerated artifacts. Mirrors `Ixon.Env.VERSION` in
  /// `Ix/Ixon.lean`.
  pub const VERSION: u64 = 1;

  /// Serialize an Env to bytes.
  ///
  /// Streaming design: for each section, collect only the *keys* from the
  /// underlying DashMap, sort them (in parallel for the big ones), then
  /// look up each value via `DashMap::get` and serialize it. The `Ref`
  /// guard returned by `get` drops at the end of each loop iteration, so
  /// at most one value is held live beyond the DashMap's own storage —
  /// peak RAM stays close to the steady-state env size instead of 2×.
  ///
  /// Why not just iterate the DashMap directly? Serialization requires a
  /// canonical order (byte-determinism across runs and across different
  /// insertion orders), and DashMap iteration order is shard-dependent.
  /// Sorting the keys is the minimum work to guarantee that.
  pub fn put(&self, buf: &mut Vec<u8>) -> Result<(), String> {
    #[cfg(not(target_arch = "riscv64"))]
    use rayon::slice::ParallelSliceMut;

    // Chatty per-section logging, off unless IX_VERBOSE=1 (or its
    // pipeline-wide alias IX_COMPILE_DBG), so we can diagnose
    // serialization stalls on huge envs (Mathlib: ~1M consts).
    let verbose = std::env::var("IX_VERBOSE").is_ok()
      || std::env::var("IX_COMPILE_DBG").is_ok();
    let overall_start = std::time::Instant::now();

    // Header: Tag4 with flag=0xE, size=VERSION (format version)
    Tag4::new(Self::FLAG, Self::VERSION).put(buf);

    // ─────────────────────────────────────────────────────────────────────
    // Canonical merkle root over consts.keys()
    //
    // Hoisted before section 1 so we can sort const_addrs once and reuse
    // it for section 2 below. Always 32 bytes (non-optional) — empty
    // const sets serialize as `zero_address()` (a fixed sentinel that
    // cannot collide with any non-empty canonical root since
    // `merkle_root_canonical` always returns a Blake3 hash for n>=1).
    // Verifiers recompute on deserialize and reject mismatches.
    // ─────────────────────────────────────────────────────────────────────