|
| 1 | +//! Stage D (lab): pre-certified mathematical patterns with fallback. |
| 2 | +//! |
| 3 | +//! Egglog is invoked ONLY when a candidate is cold-certified/promoted. |
| 4 | +//! The lookup path is a BTreeMap + exact semantic/target/binding guard + an |
| 5 | +//! already-lowered R2IL scalar program. Every miss/refusal calls the existing |
| 6 | +//! caller-supplied trusted baseline. This is NOT a production cache, data |
| 7 | +//! attestation, benchmark framework, or background task scheduler. |
| 8 | +
|
| 9 | +use std::collections::BTreeMap; |
| 10 | + |
| 11 | +use crate::artifact::{ReplayCapsule, ReplayRefusal}; |
| 12 | +use crate::{LowerRefusal, Problem}; |
| 13 | + |
| 14 | +/// Full source expression signature. Deliberately preserve premise order, |
| 15 | +/// coefficient, and variable names; no hashes or accidentally merged laws. |
| 16 | +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)] |
| 17 | +pub struct SemanticKey { |
| 18 | + goal: String, |
| 19 | + target: String, |
| 20 | + premises: Vec<(String, i64, String)>, |
| 21 | +} |
| 22 | + |
| 23 | +impl From<&Problem> for SemanticKey { |
| 24 | + fn from(p: &Problem) -> Self { |
| 25 | + Self { |
| 26 | + goal: p.goal.to_owned(), |
| 27 | + target: p.target_var.to_owned(), |
| 28 | + premises: p.premises.iter() |
| 29 | + .map(|e| (e.lhs.to_owned(), e.coeff, e.rhs.to_owned())) |
| 30 | + .collect(), |
| 31 | + } |
| 32 | + } |
| 33 | +} |
| 34 | + |
| 35 | +/// Caller-supplied lab witness. A production owner must independently attest |
| 36 | +/// these values from the sealed source and coordinates before any cache use. |
| 37 | +#[derive(Debug, Clone, Copy, PartialEq, Eq)] |
| 38 | +pub struct BindingWitness { |
| 39 | + pub source_generation: u64, |
| 40 | + pub scope: u64, |
| 41 | + pub coordinate_generation: u64, |
| 42 | +} |
| 43 | + |
| 44 | +/// Plan compatibility, independent of mathematical identity and bindings. |
| 45 | +#[derive(Debug, Clone, PartialEq, Eq)] |
| 46 | +pub struct TargetAbi { |
| 47 | + pub revision: u32, |
| 48 | + pub target: String, |
| 49 | +} |
| 50 | + |
| 51 | +/// All times are supplied from external measurements; none are inferred from |
| 52 | +/// AST size or fabricated by the catalogue. |
| 53 | +#[derive(Debug, Clone, Copy, PartialEq, Eq)] |
| 54 | +pub struct CostEvidence { |
| 55 | + pub baseline_ns: u64, |
| 56 | + pub candidate_ns: u64, |
| 57 | + pub compile_and_certify_ns: u64, |
| 58 | + pub expected_reuse: u64, |
| 59 | +} |
| 60 | + |
| 61 | +impl CostEvidence { |
| 62 | + pub fn pays_for_itself(&self) -> bool { |
| 63 | + self.candidate_ns < self.baseline_ns |
| 64 | + && self.expected_reuse > 0 |
| 65 | + && u128::from(self.baseline_ns - self.candidate_ns) |
| 66 | + * u128::from(self.expected_reuse) |
| 67 | + > u128::from(self.compile_and_certify_ns) |
| 68 | + } |
| 69 | +} |
| 70 | + |
| 71 | +#[derive(Debug, Clone, PartialEq, Eq)] |
| 72 | +pub enum PromotionRefusal { |
| 73 | + Uncertified(ReplayRefusal), |
| 74 | + NotAmortized, |
| 75 | +} |
| 76 | + |
| 77 | +#[derive(Debug, Clone, Copy, PartialEq, Eq)] |
| 78 | +pub enum FallbackReason { |
| 79 | + CacheMiss, |
| 80 | + BindingChanged, |
| 81 | + TargetChanged, |
| 82 | + CompiledRefused, |
| 83 | +} |
| 84 | + |
| 85 | +#[derive(Debug, Clone, Copy, PartialEq, Eq)] |
| 86 | +pub enum Route { |
| 87 | + Certified, |
| 88 | + Baseline(FallbackReason), |
| 89 | +} |
| 90 | + |
| 91 | +#[derive(Debug, Clone, PartialEq, Eq)] |
| 92 | +pub struct Execution { |
| 93 | + pub route: Route, |
| 94 | + pub result: Result<i64, LowerRefusal>, |
| 95 | +} |
| 96 | + |
| 97 | +struct Entry { |
| 98 | + capsule: ReplayCapsule, |
| 99 | + binding: BindingWitness, |
| 100 | + abi: TargetAbi, |
| 101 | + _cost: CostEvidence, |
| 102 | +} |
| 103 | + |
| 104 | +/// In-memory lab catalogue; never loads an unverified disk blob. |
| 105 | +#[derive(Default)] |
| 106 | +pub struct Catalogue { |
| 107 | + entries: BTreeMap<SemanticKey, Entry>, |
| 108 | +} |
| 109 | + |
| 110 | +impl Catalogue { |
| 111 | + pub fn new() -> Self { |
| 112 | + Self::default() |
| 113 | + } |
| 114 | + |
| 115 | + pub fn len(&self) -> usize { |
| 116 | + self.entries.len() |
| 117 | + } |
| 118 | + |
| 119 | + pub fn is_empty(&self) -> bool { |
| 120 | + self.entries.is_empty() |
| 121 | + } |
| 122 | + |
| 123 | + /// Cold gate. A proof, replay, independent i128 oracle and supplied |
| 124 | + /// break-even evidence are required before inserting executable steps. |
| 125 | + /// This retains the existing Stage B exact-integer / E1-only restriction. |
| 126 | + pub fn promote( |
| 127 | + &mut self, |
| 128 | + capsule: ReplayCapsule, |
| 129 | + binding: BindingWitness, |
| 130 | + abi: TargetAbi, |
| 131 | + cost: CostEvidence, |
| 132 | + ) -> Result<(), PromotionRefusal> { |
| 133 | + capsule.recheck().map_err(PromotionRefusal::Uncertified)?; |
| 134 | + for x in [0_i64, 1, -1, 7] { |
| 135 | + capsule.replay(x).map_err(PromotionRefusal::Uncertified)?; |
| 136 | + } |
| 137 | + if !cost.pays_for_itself() { |
| 138 | + return Err(PromotionRefusal::NotAmortized); |
| 139 | + } |
| 140 | + self.entries.insert( |
| 141 | + SemanticKey::from(capsule.problem()), |
| 142 | + Entry { |
| 143 | + capsule, |
| 144 | + binding, |
| 145 | + abi, |
| 146 | + _cost: cost, |
| 147 | + }, |
| 148 | + ); |
| 149 | + Ok(()) |
| 150 | + } |
| 151 | + |
| 152 | + /// Hot-compatible lookup and execution: neither egglog nor the i128 |
| 153 | + /// oracle runs here. Source/coordinate/target validation is fail-closed, |
| 154 | + /// but caller-supplied witnesses are not source attestation. |
| 155 | + /// |
| 156 | + /// Any miss or compiled execution refusal invokes baseline unconditionally. |
| 157 | + pub fn execute_or<F>( |
| 158 | + &self, |
| 159 | + problem: &Problem, |
| 160 | + binding: BindingWitness, |
| 161 | + abi: &TargetAbi, |
| 162 | + x: i64, |
| 163 | + baseline: F, |
| 164 | + ) -> Execution |
| 165 | + where |
| 166 | + F: FnOnce(i64) -> Result<i64, LowerRefusal>, |
| 167 | + { |
| 168 | + let entry = match self.entries.get(&SemanticKey::from(problem)) { |
| 169 | + Some(e) => e, |
| 170 | + None => { |
| 171 | + return Execution { |
| 172 | + route: Route::Baseline(FallbackReason::CacheMiss), |
| 173 | + result: baseline(x), |
| 174 | + }; |
| 175 | + } |
| 176 | + }; |
| 177 | + let refusal = if entry.binding != binding { |
| 178 | + Some(FallbackReason::BindingChanged) |
| 179 | + } else if &entry.abi != abi { |
| 180 | + Some(FallbackReason::TargetChanged) |
| 181 | + } else { |
| 182 | + None |
| 183 | + }; |
| 184 | + if let Some(reason) = refusal { |
| 185 | + return Execution { |
| 186 | + route: Route::Baseline(reason), |
| 187 | + result: baseline(x), |
| 188 | + }; |
| 189 | + } |
| 190 | + match entry.capsule.execute(x) { |
| 191 | + Ok(value) => Execution { |
| 192 | + route: Route::Certified, |
| 193 | + result: Ok(value), |
| 194 | + }, |
| 195 | + Err(_) => Execution { |
| 196 | + route: Route::Baseline(FallbackReason::CompiledRefused), |
| 197 | + result: baseline(x), |
| 198 | + }, |
| 199 | + } |
| 200 | + } |
| 201 | +} |
0 commit comments