Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
201 changes: 201 additions & 0 deletions crates/egglog-r2il-probe/src/catalogue.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,201 @@
//! Stage D (lab): pre-certified mathematical patterns with fallback.
//!
//! Egglog is invoked ONLY when a candidate is cold-certified/promoted.
//! The lookup path is a BTreeMap + exact semantic/target/binding guard + an
//! already-lowered R2IL scalar program. Every miss/refusal calls the existing
//! caller-supplied trusted baseline. This is NOT a production cache, data
//! attestation, benchmark framework, or background task scheduler.

use std::collections::BTreeMap;

use crate::artifact::{ReplayCapsule, ReplayRefusal};
use crate::{LowerRefusal, Problem};

/// Full source expression signature. Deliberately preserve premise order,
/// coefficient, and variable names; no hashes or accidentally merged laws.
#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
pub struct SemanticKey {
goal: String,
target: String,
premises: Vec<(String, i64, String)>,
}

impl From<&Problem> for SemanticKey {
fn from(p: &Problem) -> Self {
Self {
goal: p.goal.to_owned(),
target: p.target_var.to_owned(),
premises: p.premises.iter()
.map(|e| (e.lhs.to_owned(), e.coeff, e.rhs.to_owned()))
.collect(),
}
}
}

/// Caller-supplied lab witness. A production owner must independently attest
/// these values from the sealed source and coordinates before any cache use.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct BindingWitness {
pub source_generation: u64,
pub scope: u64,
pub coordinate_generation: u64,
}

/// Plan compatibility, independent of mathematical identity and bindings.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct TargetAbi {
pub revision: u32,
pub target: String,
}

/// All times are supplied from external measurements; none are inferred from
/// AST size or fabricated by the catalogue.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct CostEvidence {
pub baseline_ns: u64,
pub candidate_ns: u64,
pub compile_and_certify_ns: u64,
pub expected_reuse: u64,
}

impl CostEvidence {
pub fn pays_for_itself(&self) -> bool {
self.candidate_ns < self.baseline_ns
&& self.expected_reuse > 0
&& u128::from(self.baseline_ns - self.candidate_ns)
* u128::from(self.expected_reuse)
> u128::from(self.compile_and_certify_ns)
}
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum PromotionRefusal {
Uncertified(ReplayRefusal),
NotAmortized,
}

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum FallbackReason {
CacheMiss,
BindingChanged,
TargetChanged,
CompiledRefused,
}

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Route {
Certified,
Baseline(FallbackReason),
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct Execution {
pub route: Route,
pub result: Result<i64, LowerRefusal>,
}

struct Entry {
capsule: ReplayCapsule,
binding: BindingWitness,
abi: TargetAbi,
_cost: CostEvidence,
}

/// In-memory lab catalogue; never loads an unverified disk blob.
#[derive(Default)]
pub struct Catalogue {
entries: BTreeMap<SemanticKey, Entry>,
}

impl Catalogue {
pub fn new() -> Self {
Self::default()
}

pub fn len(&self) -> usize {
self.entries.len()
}

pub fn is_empty(&self) -> bool {
self.entries.is_empty()
}

/// Cold gate. A proof, replay, independent i128 oracle and supplied
/// break-even evidence are required before inserting executable steps.
/// This retains the existing Stage B exact-integer / E1-only restriction.
pub fn promote(
&mut self,
capsule: ReplayCapsule,
binding: BindingWitness,
abi: TargetAbi,
cost: CostEvidence,
) -> Result<(), PromotionRefusal> {
capsule.recheck().map_err(PromotionRefusal::Uncertified)?;
for x in [0_i64, 1, -1, 7] {
capsule.replay(x).map_err(PromotionRefusal::Uncertified)?;
}
if !cost.pays_for_itself() {
return Err(PromotionRefusal::NotAmortized);
}
self.entries.insert(
SemanticKey::from(capsule.problem()),
Entry {
capsule,
binding,
abi,
_cost: cost,
},
);
Ok(())
}

/// Hot-compatible lookup and execution: neither egglog nor the i128
/// oracle runs here. Source/coordinate/target validation is fail-closed,
/// but caller-supplied witnesses are not source attestation.
///
/// Any miss or compiled execution refusal invokes baseline unconditionally.
pub fn execute_or<F>(
&self,
problem: &Problem,
binding: BindingWitness,
abi: &TargetAbi,
x: i64,
baseline: F,
) -> Execution
where
F: FnOnce(i64) -> Result<i64, LowerRefusal>,
{
let entry = match self.entries.get(&SemanticKey::from(problem)) {
Some(e) => e,
None => {
return Execution {
route: Route::Baseline(FallbackReason::CacheMiss),
result: baseline(x),
};
}
};
let refusal = if entry.binding != binding {
Some(FallbackReason::BindingChanged)
} else if &entry.abi != abi {
Some(FallbackReason::TargetChanged)
} else {
None
};
if let Some(reason) = refusal {
return Execution {
route: Route::Baseline(reason),
result: baseline(x),
};
}
match entry.capsule.execute(x) {
Ok(value) => Execution {
route: Route::Certified,
result: Ok(value),
},
Err(_) => Execution {
route: Route::Baseline(FallbackReason::CompiledRefused),
result: baseline(x),
},
}
}
}
1 change: 1 addition & 0 deletions crates/egglog-r2il-probe/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@
//! sharing no code with steps 2-4.

pub mod artifact;
pub mod catalogue;
pub mod encode;
pub mod laws;
pub mod lower;
Expand Down
93 changes: 93 additions & 0 deletions crates/egglog-r2il-probe/tests/catalogue.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,93 @@
//! Stage D: certified cache hit, explicit witness fallbacks, no hot egglog.
use egglog_r2il_probe::artifact::ReplayCapsule;
use egglog_r2il_probe::catalogue::{
BindingWitness, Catalogue, CostEvidence, FallbackReason, PromotionRefusal, Route, TargetAbi,
};
use egglog_r2il_probe::{LowerRefusal, e1_problem};

fn bind() -> BindingWitness {
BindingWitness { source_generation: 1, scope: 42, coordinate_generation: 9 }
}

fn abi() -> TargetAbi {
TargetAbi { revision: 1, target: "r2il-checked-i64".into() }
}

fn measured() -> CostEvidence {
// Synthetic evidence for testing the policy, NOT measured performance.
CostEvidence {
baseline_ns: 300,
candidate_ns: 100,
compile_and_certify_ns: 1_000,
expected_reuse: 10,
}
}

fn trusted(x: i64) -> Result<i64, LowerRefusal> {
x.checked_mul(2)
.and_then(|v| v.checked_mul(2))
.and_then(|v| v.checked_mul(2))
.ok_or(LowerRefusal::Overflow)
}

#[test]
fn certified_hit_uses_saved_r2il_and_zero_baseline_calls() {
let mut cache = Catalogue::new();
let p = e1_problem();
let compiled = ReplayCapsule::certify(&p, 8).expect("cold E1");
cache.promote(compiled, bind(), abi(), measured()).unwrap();
assert_eq!(cache.len(), 1);
let hit = cache.execute_or(&p, bind(), &abi(), 7, |_| panic!("baseline on hit"));
assert_eq!(hit.route, Route::Certified);
assert_eq!(hit.result, Ok(56));
}

#[test]
fn no_certificate_is_installed_without_economic_gate() {
let mut cache = Catalogue::new();
let mut losing = measured();
losing.candidate_ns = 500;
let c = ReplayCapsule::certify(&e1_problem(), 8).expect("cold E1");
assert_eq!(
cache.promote(c, bind(), abi(), losing),
Err(PromotionRefusal::NotAmortized)
);
assert!(cache.is_empty());
}

#[test]
fn changed_coordinates_target_and_semantics_call_baseline() {
let mut cache = Catalogue::new();
let p = e1_problem();
cache.promote(
ReplayCapsule::certify(&p, 8).unwrap(), bind(), abi(), measured()
).unwrap();

let mut stale = bind();
stale.source_generation += 1;
let out = cache.execute_or(&p, stale, &abi(), 7, trusted);
assert_eq!(out.route, Route::Baseline(FallbackReason::BindingChanged));
assert_eq!(out.result, Ok(56));

let other = TargetAbi { revision: 2, target: "r2il-checked-i64".into() };
let out = cache.execute_or(&p, bind(), &other, 7, trusted);
assert_eq!(out.route, Route::Baseline(FallbackReason::TargetChanged));

let mut altered = p.clone();
altered.premises[0].coeff = 3;
let out = cache.execute_or(&altered, bind(), &abi(), 7, |_| Ok(-123));
assert_eq!(out.route, Route::Baseline(FallbackReason::CacheMiss));
assert_eq!(out.result, Ok(-123));
}

#[test]
fn overflow_must_fallback_without_manufacturing_an_answer() {
let mut cache = Catalogue::new();
let p = e1_problem();
cache.promote(
ReplayCapsule::certify(&p, 8).unwrap(), bind(), abi(), measured()
).unwrap();
let out = cache.execute_or(&p, bind(), &abi(), i64::MAX, trusted);
assert_eq!(out.route, Route::Baseline(FallbackReason::CompiledRefused));
assert_eq!(out.result, Err(LowerRefusal::Overflow));
}
Loading