oxilean-kernel 0.1.2

OxiLean kernel - The trusted computing base for type checking
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146

//! Types for the memoized WHNF reduction layer.
//!
//! Provides cache key/entry/configuration/statistics types for the WHNF memo
//! table.  Cache correctness is guaranteed by including the current environment
//! version in every key: when the environment grows (a new declaration is
//! added), `invalidate_all` bumps `env_version`, rendering all prior entries
//! stale without requiring an explicit scan.

use std::collections::HashMap;

// ---------------------------------------------------------------------------
// WhnfKey
// ---------------------------------------------------------------------------

/// Cache key for a single WHNF reduction result.
///
/// Including `env_version` ensures that cached reductions are invalidated
/// automatically when the environment changes: a key computed under version `v`
/// will never match an entry stored under version `v'` where `v' != v`.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub struct WhnfKey {
    /// FNV-1a hash of the expression bytes to be reduced.
    pub expr_hash: u64,
    /// Monotonically increasing environment version at query time.
    pub env_version: u32,
}

// ---------------------------------------------------------------------------
// WhnfEntry
// ---------------------------------------------------------------------------

/// A single cached WHNF reduction result.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct WhnfEntry {
    /// FNV-1a hash of the WHNF-reduced result expression.
    pub result_hash: u64,
    /// Number of reduction steps performed to reach WHNF (used for eviction
    /// decisions: entries that required few steps are cheap to recompute).
    pub reduction_steps: u32,
    /// Number of times this entry has been returned from the cache.
    pub access_count: u32,
}

// ---------------------------------------------------------------------------
// MemoConfig
// ---------------------------------------------------------------------------

/// Configuration parameters for a [`WhnfMemo`] instance.
#[derive(Clone, Debug)]
pub struct MemoConfig {
    /// Maximum number of entries in the cache before eviction is triggered.
    pub max_entries: usize,
    /// Minimum number of reduction steps required before a result is cached.
    ///
    /// Results achieved in fewer steps are cheap to recompute and not worth
    /// the memory overhead.
    pub min_steps_to_cache: u32,
    /// Fraction of `max_entries` used as the access-count threshold during
    /// cold eviction.  Entries whose `access_count` is below
    /// `floor(max_entries * eviction_threshold)` are considered cold and may
    /// be removed.
    pub eviction_threshold: f64,
}

impl Default for MemoConfig {
    fn default() -> Self {
        MemoConfig {
            max_entries: 4096,
            min_steps_to_cache: 2,
            eviction_threshold: 0.1,
        }
    }
}

// ---------------------------------------------------------------------------
// WhnfMemo
// ---------------------------------------------------------------------------

/// Memoization table for WHNF reduction results.
///
/// # Correctness
///
/// Every lookup and insertion is tied to `env_version`.  Calling
/// `invalidate_all` bumps the version and clears all entries, guaranteeing
/// that stale results (computed against an older environment) are never
/// returned.
///
/// # Eviction
///
/// When the table reaches `config.max_entries`, `evict_cold` is called
/// automatically during `insert`.  Cold entries — those whose `access_count`
/// falls below a threshold derived from `config.eviction_threshold` — are
/// removed.  If no cold entries exist the oldest-inserted entry is dropped.
pub struct WhnfMemo {
    /// Cached entries, keyed by (expression hash, env version).
    pub(crate) entries: HashMap<WhnfKey, WhnfEntry>,
    /// Total number of successful cache lookups.
    pub hits: u64,
    /// Total number of cache misses.
    pub misses: u64,
    /// Total number of entries removed by eviction.
    pub evictions: u64,
    /// Current environment version.
    pub env_version: u32,
    /// Configuration controlling capacity, caching threshold, and eviction.
    pub(crate) config: MemoConfig,
    /// Monotonically increasing insertion counter (used to implement FIFO
    /// fallback eviction when no cold entries are found).
    pub(crate) insert_order: Vec<WhnfKey>,
}

// ---------------------------------------------------------------------------
// MemoStats
// ---------------------------------------------------------------------------

/// A snapshot of [`WhnfMemo`] performance statistics.
#[derive(Clone, Debug)]
pub struct MemoStats {
    /// Total cache hits.
    pub hits: u64,
    /// Total cache misses.
    pub misses: u64,
    /// Total evictions.
    pub evictions: u64,
    /// Hit rate in [0.0, 1.0].
    pub hit_rate: f64,
    /// Current number of cached entries.
    pub size: usize,
    /// Current environment version.
    pub env_version: u32,
}

impl std::fmt::Display for MemoStats {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(
            f,
            "MemoStats {{ hits: {}, misses: {}, evictions: {}, hit_rate: {:.2}%, size: {}, env_version: {} }}",
            self.hits,
            self.misses,
            self.evictions,
            self.hit_rate * 100.0,
            self.size,
            self.env_version
        )
    }
}