Skip to main content

omena_incremental/
lib.rs

1//! Salsa-backed incremental computation substrate for omena-css.
2//!
3//! The crate owns graph snapshots, dirty-set planning, cancellation state, and
4//! fuzzable consistency cases. Downstream parser, semantic, and transform
5//! crates depend on these stable V0 payloads instead of reaching into Salsa
6//! internals directly.
7
8use std::collections::{BTreeMap, BTreeSet};
9
10use omena_evidence_graph::{
11    EvidenceDemandEdgeV0, EvidenceGraphBuildErrorV0, EvidenceGraphV0, EvidenceNodeKeyV0,
12    EvidenceNodeSeedV0, FamilyStampV0, GuaranteeKindV0, TypedInvariantWitnessTokenV0,
13    build_evidence_graph_from_edges_v0,
14};
15use salsa::Setter;
16use serde::{Deserialize, Serialize};
17
18mod frame_invalidation;
19pub use frame_invalidation::*;
20
21#[cfg(test)]
22use std::cell::RefCell;
23#[cfg(test)]
24thread_local! {
25    static SALSA_NODE_VALUE_QUERY_RUNS_BY_ID: RefCell<BTreeMap<String, usize>> = const { RefCell::new(BTreeMap::new()) };
26}
27
28#[cfg(test)]
29fn record_salsa_node_value_query_run(id: &str) {
30    SALSA_NODE_VALUE_QUERY_RUNS_BY_ID.with(|runs| {
31        *runs.borrow_mut().entry(id.to_string()).or_default() += 1;
32    });
33}
34
35#[cfg(test)]
36fn reset_salsa_node_value_query_runs() {
37    SALSA_NODE_VALUE_QUERY_RUNS_BY_ID.with(|runs| runs.borrow_mut().clear());
38}
39
40#[cfg(test)]
41fn salsa_node_value_query_runs(id: &str) -> usize {
42    SALSA_NODE_VALUE_QUERY_RUNS_BY_ID
43        .with(|runs| runs.borrow().get(id).copied().unwrap_or_default())
44}
45
46#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
47#[serde(rename_all = "camelCase")]
48pub struct OmenaIncrementalBoundarySummaryV0 {
49    pub schema_version: &'static str,
50    pub product: &'static str,
51    pub engine_name: &'static str,
52    pub invalidation_model: &'static str,
53    pub query_model: &'static str,
54    pub dependency_propagation_policy: &'static str,
55    pub maximum_dependency_propagation_iterations: &'static str,
56    pub node_identity: Vec<&'static str>,
57    pub dirty_reasons: Vec<&'static str>,
58    pub ready_surfaces: Vec<&'static str>,
59}
60
61pub const DEFAULT_INCREMENTAL_CANCELLATION_LIMIT: usize = 128;
62
63#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Deserialize, Serialize)]
64#[serde(rename_all = "camelCase")]
65pub struct IncrementalRevisionV0 {
66    pub value: u64,
67}
68
69#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Deserialize, Serialize)]
70#[serde(rename_all = "camelCase")]
71pub struct OmenaWorkspaceSnapshotIdV0 {
72    pub value: u64,
73}
74
75impl OmenaWorkspaceSnapshotIdV0 {
76    pub fn from_revision(revision: IncrementalRevisionV0) -> Self {
77        Self {
78            value: revision.value,
79        }
80    }
81
82    pub fn revision(self) -> IncrementalRevisionV0 {
83        IncrementalRevisionV0 { value: self.value }
84    }
85}
86
87#[derive(Debug, Clone, PartialEq, Eq)]
88pub struct IncrementalGraphInputV0 {
89    pub revision: IncrementalRevisionV0,
90    pub nodes: Vec<IncrementalNodeInputV0>,
91}
92
93#[derive(Debug, Clone, PartialEq, Eq)]
94pub struct IncrementalNodeInputV0 {
95    pub id: String,
96    pub digest: String,
97    pub dependency_ids: Vec<String>,
98}
99
100#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
101#[serde(rename_all = "camelCase")]
102pub struct IncrementalSnapshotV0 {
103    pub schema_version: &'static str,
104    pub product: &'static str,
105    pub revision: IncrementalRevisionV0,
106    pub nodes: Vec<IncrementalSnapshotNodeV0>,
107}
108
109#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
110#[serde(rename_all = "camelCase")]
111pub struct IncrementalSnapshotNodeV0 {
112    pub id: String,
113    pub digest: String,
114    pub dependency_ids: Vec<String>,
115}
116
117#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
118#[serde(rename_all = "camelCase")]
119pub struct IncrementalComputationPlanV0 {
120    pub schema_version: &'static str,
121    pub product: &'static str,
122    pub revision: IncrementalRevisionV0,
123    pub node_count: usize,
124    pub dirty_node_count: usize,
125    pub changed_input_count: usize,
126    pub new_node_count: usize,
127    pub removed_node_count: usize,
128    pub dependency_dirty_count: usize,
129    pub alpha_equivalence_graph_hash: IncrementalAlphaEquivalenceHashV0,
130    pub shadow_delta_oracle: IncrementalShadowDeltaOracleV0,
131    pub invalidation_priority_plan: IncrementalInvalidationPriorityPlanV0,
132    pub nodes: Vec<IncrementalComputationNodeV0>,
133}
134
135#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
136#[serde(rename_all = "camelCase")]
137pub struct IncrementalComputationNodeV0 {
138    pub id: String,
139    pub digest: String,
140    pub dependency_ids: Vec<String>,
141    pub dirty: bool,
142    pub reasons: Vec<&'static str>,
143    pub changed_at: IncrementalRevisionV0,
144    pub verified_at: IncrementalRevisionV0,
145    pub value_equal_to_previous: bool,
146    pub alpha_equivalence_hash: String,
147}
148
149#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
150#[serde(rename_all = "camelCase")]
151pub struct IncrementalAlphaEquivalenceHashV0 {
152    pub schema_version: &'static str,
153    pub product: &'static str,
154    pub feature_gate: &'static str,
155    pub claim_level: &'static str,
156    pub theorem_claimed: bool,
157    pub hash: String,
158    pub normalized_node_count: usize,
159    pub normalized_edge_count: usize,
160}
161
162#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
163#[serde(rename_all = "camelCase")]
164pub struct IncrementalShadowDeltaOracleV0 {
165    pub schema_version: &'static str,
166    pub product: &'static str,
167    pub feature_gate: &'static str,
168    pub claim_level: &'static str,
169    pub theorem_claimed: bool,
170    pub sampled_shadow_witness_ready: bool,
171    pub incremental_dirty_ids: Vec<String>,
172    pub from_scratch_dirty_ids: Vec<String>,
173    pub incremental_matches_from_scratch_delta: bool,
174    pub dbsp_zset_claim_ready: bool,
175    pub performance_benchmark_claim_ready: bool,
176}
177
178#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
179#[serde(rename_all = "camelCase")]
180pub struct IncrementalEditDistancePriorityInputV0 {
181    pub schema_version: &'static str,
182    pub product: &'static str,
183    pub feature_gate: &'static str,
184    pub claim_level: &'static str,
185    pub theorem_claimed: bool,
186    pub node_id: String,
187    pub edit_distance_total: usize,
188    pub cascade_margin_abs_distance: u64,
189    pub bridge_checked: bool,
190    pub bridge_calibration_stage: &'static str,
191}
192
193#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
194#[serde(rename_all = "camelCase")]
195pub struct IncrementalInvalidationPriorityPlanV0 {
196    pub schema_version: &'static str,
197    pub product: &'static str,
198    pub feature_gate: &'static str,
199    pub claim_level: &'static str,
200    pub theorem_claimed: bool,
201    pub public_safety_claim_ready: bool,
202    pub calibration_stage: &'static str,
203    pub weight_profile: &'static str,
204    pub metric_input_count: usize,
205    pub dirty_node_count: usize,
206    pub metric_consumed_count: usize,
207    pub prioritized_dirty_node_ids: Vec<String>,
208    pub entries: Vec<IncrementalInvalidationPriorityEntryV0>,
209}
210
211#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
212#[serde(rename_all = "camelCase")]
213pub struct IncrementalInvalidationPriorityEntryV0 {
214    pub node_id: String,
215    pub priority_rank: usize,
216    pub priority_score: u64,
217    pub priority_kind: &'static str,
218    pub metric_consumed: bool,
219    pub edit_distance_total: Option<usize>,
220    pub cascade_margin_abs_distance: Option<u64>,
221    pub bridge_checked: bool,
222}
223
224#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
225#[serde(rename_all = "camelCase")]
226pub struct IncrementalCancellationSnapshotV0 {
227    pub schema_version: &'static str,
228    pub product: &'static str,
229    pub cancelled_request_count: usize,
230    pub cancelled_request_ids: Vec<String>,
231}
232
233#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
234#[serde(rename_all = "camelCase")]
235pub struct IncrementalDatabaseUpdateV0 {
236    pub schema_version: &'static str,
237    pub product: &'static str,
238    pub incremental_plan: IncrementalComputationPlanV0,
239    pub datalog_rule_evaluator: DatalogRuleEvaluatorV0,
240    pub next_snapshot: IncrementalSnapshotV0,
241}
242
243#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
244#[serde(rename_all = "camelCase")]
245pub struct IncrementalConsistencyFuzzCaseV0 {
246    pub seed: u64,
247    pub node_count: usize,
248    pub changed_node_index: Option<usize>,
249}
250
251#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
252#[serde(rename_all = "camelCase")]
253pub struct IncrementalConsistencyFuzzResultV0 {
254    pub seed: u64,
255    pub node_count: usize,
256    pub changed_node_id: Option<String>,
257    pub dirty_node_count: usize,
258    pub expected_dirty_node_count: usize,
259    pub passed: bool,
260}
261
262#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
263#[serde(rename_all = "camelCase")]
264pub struct IncrementalFuzzSeedReportV0 {
265    pub schema_version: &'static str,
266    pub product: &'static str,
267    pub case_count: usize,
268    pub passed_count: usize,
269    pub failed_count: usize,
270    pub results: Vec<IncrementalConsistencyFuzzResultV0>,
271}
272
273#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
274#[serde(rename_all = "camelCase")]
275pub struct DatalogRuleEvaluatorRuleV0 {
276    pub name: &'static str,
277    pub head: &'static str,
278    pub body: Vec<&'static str>,
279    pub source: &'static str,
280}
281
282#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
283#[serde(rename_all = "camelCase")]
284/// V0 freeze-candidate typed contract over the incremental dirty-plan substrate.
285///
286/// This exposes Datalog-shaped rules and relations for auditability while the
287/// product path remains the Salsa-backed fixed-point planner. It is not an
288/// external Datalog host, FlowLog/Souffle/egglog binding, or Cargo 1.0 API.
289pub struct DatalogRuleEvaluatorV0 {
290    pub schema_version: &'static str,
291    pub product: &'static str,
292    pub evaluator_kind: &'static str,
293    pub substrate: &'static str,
294    pub external_host_ready: bool,
295    pub revision: IncrementalRevisionV0,
296    pub rule_count: usize,
297    pub relation_count: usize,
298    pub input_node_count: usize,
299    pub dirty_node_count: usize,
300    pub derived_node_count: usize,
301    pub iteration_limit: usize,
302    pub fixed_point_reached: bool,
303    pub relations: Vec<&'static str>,
304    pub rules: Vec<DatalogRuleEvaluatorRuleV0>,
305    pub incremental_plan: IncrementalComputationPlanV0,
306}
307
308#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
309#[serde(rename_all = "camelCase")]
310pub struct IncrementalLayerEvidenceV0 {
311    pub schema_version: &'static str,
312    pub product: &'static str,
313    pub claim_level: &'static str,
314    pub invalidation_layer: &'static str,
315    pub real_invalidation_evidence_ready: bool,
316    pub fuzz_evidence_ready: bool,
317    pub salsa_reuse_evidence_ready: bool,
318    pub datalog_contract_evidence_ready: bool,
319    pub value_equality_backdating_ready: bool,
320    pub alpha_equivalence_hash_ready: bool,
321    pub shadow_delta_oracle_ready: bool,
322    pub edit_distance_priority_ready: bool,
323    pub benchmark_surface_ready: bool,
324    pub performance_benchmark_claim_ready: bool,
325    pub external_datalog_host_ready: bool,
326    pub dbsp_zset_claim_ready: bool,
327    pub public_safety_claim_ready: bool,
328    pub benchmark_gate: &'static str,
329    pub benchmark_evidence_level: &'static str,
330    pub supported_claims: Vec<&'static str>,
331    pub deferred_claims: Vec<&'static str>,
332    pub boundary: OmenaIncrementalBoundarySummaryV0,
333    pub fuzz_report: IncrementalFuzzSeedReportV0,
334    pub sample_update: IncrementalDatabaseUpdateV0,
335}
336
337const INCREMENTAL_EVIDENCE_EDGE_KIND_V0: &str = "incremental-evidence";
338
339fn incremental_guarantee_kind(claim_level: &str) -> GuaranteeKindV0 {
340    GuaranteeKindV0::from_existing_label(claim_level)
341        .unwrap_or_else(GuaranteeKindV0::for_label_less_family)
342}
343
344fn incremental_evidence_node_key(
345    query_identity: impl Into<String>,
346    input_identity: impl Into<String>,
347) -> EvidenceNodeKeyV0 {
348    EvidenceNodeKeyV0::new(query_identity, input_identity)
349}
350
351fn incremental_evidence_edge(
352    from_query_identity: impl Into<String>,
353    to_node_key: EvidenceNodeKeyV0,
354) -> EvidenceDemandEdgeV0 {
355    EvidenceDemandEdgeV0::new(
356        from_query_identity,
357        to_node_key,
358        INCREMENTAL_EVIDENCE_EDGE_KIND_V0,
359    )
360}
361
362fn typed_invariant_family_stamp() -> FamilyStampV0 {
363    let token = TypedInvariantWitnessTokenV0::from_incremental_layer_evidence();
364    FamilyStampV0::typed_invariant_witness(&token)
365}
366
367impl IncrementalAlphaEquivalenceHashV0 {
368    pub fn evidence_node_key(&self) -> EvidenceNodeKeyV0 {
369        incremental_evidence_node_key(self.product, format!("{}:{}", self.feature_gate, self.hash))
370    }
371
372    pub fn evidence_node_seed(&self) -> EvidenceNodeSeedV0 {
373        EvidenceNodeSeedV0::with_family(
374            self.evidence_node_key(),
375            vec![
376                self.product.to_string(),
377                self.feature_gate.to_string(),
378                self.claim_level.to_string(),
379            ],
380            incremental_guarantee_kind(self.claim_level),
381            typed_invariant_family_stamp(),
382        )
383    }
384
385    pub fn evidence_demand_edge(&self) -> EvidenceDemandEdgeV0 {
386        incremental_evidence_edge(self.product, self.evidence_node_key())
387    }
388}
389
390impl IncrementalShadowDeltaOracleV0 {
391    pub fn evidence_node_key(&self) -> EvidenceNodeKeyV0 {
392        incremental_evidence_node_key(
393            self.product,
394            format!(
395                "{}:incremental={}:fromScratch={}",
396                self.feature_gate,
397                self.incremental_dirty_ids.join(","),
398                self.from_scratch_dirty_ids.join(",")
399            ),
400        )
401    }
402
403    pub fn evidence_node_seed(&self) -> EvidenceNodeSeedV0 {
404        EvidenceNodeSeedV0::with_family(
405            self.evidence_node_key(),
406            vec![
407                self.product.to_string(),
408                self.feature_gate.to_string(),
409                self.claim_level.to_string(),
410            ],
411            incremental_guarantee_kind(self.claim_level),
412            typed_invariant_family_stamp(),
413        )
414    }
415
416    pub fn evidence_demand_edge(&self) -> EvidenceDemandEdgeV0 {
417        incremental_evidence_edge(self.product, self.evidence_node_key())
418    }
419}
420
421impl IncrementalEditDistancePriorityInputV0 {
422    pub fn evidence_node_key(&self) -> EvidenceNodeKeyV0 {
423        incremental_evidence_node_key(
424            self.product,
425            format!("{}:{}", self.feature_gate, self.node_id),
426        )
427    }
428
429    pub fn evidence_node_seed(&self) -> EvidenceNodeSeedV0 {
430        EvidenceNodeSeedV0::with_family(
431            self.evidence_node_key(),
432            vec![
433                self.product.to_string(),
434                self.feature_gate.to_string(),
435                self.claim_level.to_string(),
436                self.bridge_calibration_stage.to_string(),
437            ],
438            incremental_guarantee_kind(self.claim_level),
439            typed_invariant_family_stamp(),
440        )
441    }
442
443    pub fn evidence_demand_edge(&self) -> EvidenceDemandEdgeV0 {
444        incremental_evidence_edge(self.product, self.evidence_node_key())
445    }
446}
447
448impl IncrementalInvalidationPriorityPlanV0 {
449    pub fn evidence_node_key(&self) -> EvidenceNodeKeyV0 {
450        incremental_evidence_node_key(
451            self.product,
452            format!(
453                "{}:{}:dirty={}:metric={}",
454                self.feature_gate,
455                self.weight_profile,
456                self.dirty_node_count,
457                self.metric_consumed_count
458            ),
459        )
460    }
461
462    pub fn evidence_node_seed(&self) -> EvidenceNodeSeedV0 {
463        EvidenceNodeSeedV0::with_family(
464            self.evidence_node_key(),
465            vec![
466                self.product.to_string(),
467                self.feature_gate.to_string(),
468                self.claim_level.to_string(),
469                self.calibration_stage.to_string(),
470            ],
471            incremental_guarantee_kind(self.claim_level),
472            typed_invariant_family_stamp(),
473        )
474    }
475
476    pub fn evidence_demand_edge(&self) -> EvidenceDemandEdgeV0 {
477        incremental_evidence_edge(self.product, self.evidence_node_key())
478    }
479}
480
481impl IncrementalComputationPlanV0 {
482    pub fn evidence_node_seeds(&self) -> Vec<EvidenceNodeSeedV0> {
483        vec![
484            self.alpha_equivalence_graph_hash.evidence_node_seed(),
485            self.shadow_delta_oracle.evidence_node_seed(),
486            self.invalidation_priority_plan.evidence_node_seed(),
487        ]
488    }
489
490    pub fn evidence_demand_edges(&self) -> Vec<EvidenceDemandEdgeV0> {
491        vec![
492            self.alpha_equivalence_graph_hash.evidence_demand_edge(),
493            self.shadow_delta_oracle.evidence_demand_edge(),
494            self.invalidation_priority_plan.evidence_demand_edge(),
495        ]
496    }
497
498    pub fn evidence_graph(&self) -> Result<EvidenceGraphV0, EvidenceGraphBuildErrorV0> {
499        build_evidence_graph_from_edges_v0(self.evidence_node_seeds(), self.evidence_demand_edges())
500    }
501}
502
503impl IncrementalLayerEvidenceV0 {
504    pub fn evidence_node_key(&self) -> EvidenceNodeKeyV0 {
505        incremental_evidence_node_key(self.product, self.invalidation_layer)
506    }
507
508    pub fn evidence_node_seed(&self) -> EvidenceNodeSeedV0 {
509        EvidenceNodeSeedV0::with_family(
510            self.evidence_node_key(),
511            vec![
512                self.product.to_string(),
513                self.claim_level.to_string(),
514                self.invalidation_layer.to_string(),
515                self.benchmark_evidence_level.to_string(),
516            ],
517            incremental_guarantee_kind(self.claim_level),
518            typed_invariant_family_stamp(),
519        )
520    }
521
522    pub fn evidence_demand_edge(&self) -> EvidenceDemandEdgeV0 {
523        incremental_evidence_edge(self.product, self.evidence_node_key())
524    }
525
526    pub fn evidence_graph(&self) -> Result<EvidenceGraphV0, EvidenceGraphBuildErrorV0> {
527        let mut seeds = vec![self.evidence_node_seed()];
528        seeds.extend(self.sample_update.incremental_plan.evidence_node_seeds());
529        let mut edges = vec![self.evidence_demand_edge()];
530        edges.extend(self.sample_update.incremental_plan.evidence_demand_edges());
531        build_evidence_graph_from_edges_v0(seeds, edges)
532    }
533}
534
535#[derive(Debug, Clone, PartialEq, Eq)]
536pub struct IncrementalCancellationRegistryV0 {
537    limit: usize,
538    cancelled_request_ids: BTreeSet<String>,
539}
540
541#[salsa::input(debug)]
542pub struct SalsaIncrementalNodeInputV0 {
543    #[returns(ref)]
544    id: String,
545    #[returns(ref)]
546    digest: String,
547    #[returns(ref)]
548    dependency_ids: Vec<String>,
549}
550
551#[salsa::input(debug)]
552pub struct SalsaIncrementalGraphInputV0 {
553    #[returns(ref)]
554    nodes: Vec<SalsaIncrementalNodeInputV0>,
555}
556
557#[salsa::input(debug)]
558pub struct SalsaIncrementalFileRevisionInputV0 {
559    file_id: u32,
560    revision: IncrementalRevisionV0,
561    #[returns(ref)]
562    syntax_node_id: String,
563}
564
565#[salsa::db]
566#[derive(Clone, Default)]
567pub struct OmenaSalsaDatabaseV0 {
568    storage: salsa::Storage<Self>,
569}
570
571#[salsa::db]
572impl salsa::Database for OmenaSalsaDatabaseV0 {}
573
574impl OmenaSalsaDatabaseV0 {
575    pub fn new() -> Self {
576        Self::default()
577    }
578
579    pub fn handle(&self) -> salsa::StorageHandle<Self> {
580        self.storage.clone().into_zalsa_handle()
581    }
582
583    pub fn from_handle(handle: salsa::StorageHandle<Self>) -> Self {
584        Self {
585            storage: handle.into_storage(),
586        }
587    }
588}
589
590#[derive(Default)]
591pub struct OmenaIncrementalDatabaseV0 {
592    db: OmenaSalsaDatabaseV0,
593    node_inputs_by_id: BTreeMap<String, SalsaIncrementalNodeInputV0>,
594    graph_input: Option<SalsaIncrementalGraphInputV0>,
595    current_snapshot: Option<IncrementalSnapshotV0>,
596}
597
598pub fn summarize_omena_incremental_boundary() -> OmenaIncrementalBoundarySummaryV0 {
599    OmenaIncrementalBoundarySummaryV0 {
600        schema_version: "0",
601        product: "omena-incremental.boundary",
602        engine_name: "omena-incremental",
603        invalidation_model: "stableNodeId+inputDigest+dependencyPropagation",
604        query_model: "salsaInput+trackedQueryFieldGranularReuse",
605        dependency_propagation_policy: "salsaDemandDirtySignatureReads",
606        maximum_dependency_propagation_iterations: "oracleOnlyNodeCount+1",
607        node_identity: vec!["id", "digest", "dependencyIds"],
608        dirty_reasons: vec![
609            "newNode",
610            "inputDigestChanged",
611            "dependencySetChanged",
612            "dependencyDirty",
613        ],
614        ready_surfaces: vec![
615            "incrementalGraphInput",
616            "incrementalSnapshot",
617            "incrementalComputationPlan",
618            "incrementalCancellationRegistry",
619            "datalogRuleEvaluatorV0",
620            "salsaPersistentDatabase",
621            "salsaTrackedNodeSnapshotQuery",
622            "salsaFieldGranularReuse",
623            "salsaPlanAndSnapshotUpdate",
624            "salsaDemandDependencyReads",
625            "valueEqualityBackdating",
626            "alphaEquivalenceHash",
627            "incrementalShadowDeltaOracle",
628            "editDistanceInvalidationPriority",
629        ],
630    }
631}
632
633pub fn summarize_datalog_rule_evaluator_v0(
634    input: &IncrementalGraphInputV0,
635    previous: Option<&IncrementalSnapshotV0>,
636) -> DatalogRuleEvaluatorV0 {
637    let mut database = OmenaIncrementalDatabaseV0::default();
638    if let Some(previous) = previous {
639        database.restore_snapshot(previous);
640    }
641    database
642        .plan_and_upsert_graph_input(input)
643        .datalog_rule_evaluator
644}
645
646fn summarize_datalog_rule_evaluator_for_plan_v0(
647    input: &IncrementalGraphInputV0,
648    incremental_plan: IncrementalComputationPlanV0,
649) -> DatalogRuleEvaluatorV0 {
650    let relations = vec![
651        "node(id,digest)",
652        "previousNode(id,digest)",
653        "dependsOn(nodeId,dependencyId)",
654        "changedInput(nodeId)",
655        "dirty(nodeId)",
656    ];
657    let rules = vec![
658        DatalogRuleEvaluatorRuleV0 {
659            name: "newNodeIsDirty",
660            head: "dirty(Node)",
661            body: vec!["node(Node,Digest)", "not previousNode(Node,_)"],
662            source: "omena-incremental.computation-plan",
663        },
664        DatalogRuleEvaluatorRuleV0 {
665            name: "changedDigestIsDirty",
666            head: "dirty(Node)",
667            body: vec![
668                "node(Node,Digest)",
669                "previousNode(Node,PreviousDigest)",
670                "Digest != PreviousDigest",
671            ],
672            source: "omena-incremental.computation-plan",
673        },
674        DatalogRuleEvaluatorRuleV0 {
675            name: "changedDependencySetIsDirty",
676            head: "dirty(Node)",
677            body: vec!["dependsOn(Node,_)", "previousDependencySetDiffers(Node)"],
678            source: "omena-incremental.computation-plan",
679        },
680        DatalogRuleEvaluatorRuleV0 {
681            name: "dependencyDirtyDemandRead",
682            head: "dirty(Node)",
683            body: vec!["dependsOn(Node,Dependency)", "dirty(Dependency)"],
684            source: "omena-incremental.salsa-demand-plan",
685        },
686    ];
687    let iteration_limit = dependency_propagation_iteration_limit(input.nodes.len());
688    let fixed_point_reached = dirty_set_is_dependency_closed(&incremental_plan);
689
690    DatalogRuleEvaluatorV0 {
691        schema_version: "0",
692        product: "omena-incremental.datalog-rule-evaluator",
693        evaluator_kind: "typedContractOverSalsaDemandPlan",
694        substrate: "omena-incremental.salsa-backed-computation-plan",
695        external_host_ready: false,
696        revision: input.revision,
697        rule_count: rules.len(),
698        relation_count: relations.len(),
699        input_node_count: input.nodes.len(),
700        dirty_node_count: incremental_plan.dirty_node_count,
701        derived_node_count: incremental_plan.dependency_dirty_count,
702        iteration_limit,
703        fixed_point_reached,
704        relations,
705        rules,
706        incremental_plan,
707    }
708}
709
710pub fn snapshot_from_graph_input(input: &IncrementalGraphInputV0) -> IncrementalSnapshotV0 {
711    IncrementalSnapshotV0 {
712        schema_version: "0",
713        product: "omena-incremental.snapshot",
714        revision: input.revision,
715        nodes: normalized_snapshot_nodes(input),
716    }
717}
718
719fn graph_input_from_snapshot(snapshot: &IncrementalSnapshotV0) -> IncrementalGraphInputV0 {
720    IncrementalGraphInputV0 {
721        revision: snapshot.revision,
722        nodes: snapshot
723            .nodes
724            .iter()
725            .map(|node| IncrementalNodeInputV0 {
726                id: node.id.clone(),
727                digest: node.digest.clone(),
728                dependency_ids: node.dependency_ids.clone(),
729            })
730            .collect(),
731    }
732}
733
734pub fn summarize_incremental_shadow_delta_oracle_v0(
735    input: &IncrementalGraphInputV0,
736    previous: Option<&IncrementalSnapshotV0>,
737    incremental_dirty_ids: BTreeSet<String>,
738) -> IncrementalShadowDeltaOracleV0 {
739    let from_scratch_dirty_ids = compute_from_scratch_delta_dirty_ids(input, previous);
740    let incremental_dirty_ids = incremental_dirty_ids.into_iter().collect::<Vec<_>>();
741    let from_scratch_dirty_ids = from_scratch_dirty_ids.into_iter().collect::<Vec<_>>();
742    let incremental_matches_from_scratch_delta = incremental_dirty_ids == from_scratch_dirty_ids;
743
744    IncrementalShadowDeltaOracleV0 {
745        schema_version: "0",
746        product: "omena-incremental.shadow-delta-oracle",
747        feature_gate: "incremental-shadow-delta-v0",
748        claim_level: "sampledFixtureWitnessNotEquivalenceProof",
749        theorem_claimed: false,
750        sampled_shadow_witness_ready: incremental_matches_from_scratch_delta,
751        incremental_dirty_ids,
752        from_scratch_dirty_ids,
753        incremental_matches_from_scratch_delta,
754        dbsp_zset_claim_ready: false,
755        performance_benchmark_claim_ready: false,
756    }
757}
758
759pub fn summarize_incremental_invalidation_priority_plan_v0(
760    nodes: &[IncrementalComputationNodeV0],
761    priority_inputs: &[IncrementalEditDistancePriorityInputV0],
762) -> IncrementalInvalidationPriorityPlanV0 {
763    let priority_inputs_by_node = priority_inputs
764        .iter()
765        .map(|input| (input.node_id.as_str(), input))
766        .collect::<BTreeMap<_, _>>();
767    let mut entries = nodes
768        .iter()
769        .filter(|node| node.dirty)
770        .map(|node| {
771            let priority_input = priority_inputs_by_node.get(node.id.as_str()).copied();
772            let edit_distance_total = priority_input.map(|input| input.edit_distance_total);
773            let cascade_margin_abs_distance =
774                priority_input.map(|input| input.cascade_margin_abs_distance);
775            let bridge_checked = priority_input.is_some_and(|input| input.bridge_checked);
776            let metric_consumed = priority_input.is_some();
777            let priority_score = invalidation_priority_score(priority_input);
778
779            IncrementalInvalidationPriorityEntryV0 {
780                node_id: node.id.clone(),
781                priority_rank: 0,
782                priority_score,
783                priority_kind: if metric_consumed {
784                    "editDistanceCascadeMarginWeighted"
785                } else {
786                    "dirtyNodeDefault"
787                },
788                metric_consumed,
789                edit_distance_total,
790                cascade_margin_abs_distance,
791                bridge_checked,
792            }
793        })
794        .collect::<Vec<_>>();
795    entries.sort_by(|left, right| {
796        right
797            .priority_score
798            .cmp(&left.priority_score)
799            .then_with(|| left.node_id.cmp(&right.node_id))
800    });
801    for (index, entry) in entries.iter_mut().enumerate() {
802        entry.priority_rank = index + 1;
803    }
804    let metric_consumed_count = entries.iter().filter(|entry| entry.metric_consumed).count();
805    let prioritized_dirty_node_ids = entries
806        .iter()
807        .map(|entry| entry.node_id.clone())
808        .collect::<Vec<_>>();
809
810    IncrementalInvalidationPriorityPlanV0 {
811        schema_version: "0",
812        product: "omena-incremental.invalidation-priority-plan",
813        feature_gate: "incremental-edit-distance-priority-v0",
814        claim_level: "fixtureWitnessSchedulerPriority",
815        theorem_claimed: false,
816        public_safety_claim_ready: false,
817        calibration_stage: "fixtureWitnessDistanceMarginWeightedV0",
818        weight_profile: "editDistance10+cascadeMargin3+bridgeChecked1",
819        metric_input_count: priority_inputs.len(),
820        dirty_node_count: entries.len(),
821        metric_consumed_count,
822        prioritized_dirty_node_ids,
823        entries,
824    }
825}
826
827fn invalidation_priority_score(
828    priority_input: Option<&IncrementalEditDistancePriorityInputV0>,
829) -> u64 {
830    const DIRTY_NODE_BASE_SCORE: u64 = 1_000;
831    let Some(priority_input) = priority_input else {
832        return DIRTY_NODE_BASE_SCORE;
833    };
834    DIRTY_NODE_BASE_SCORE
835        + (priority_input.edit_distance_total as u64).saturating_mul(10)
836        + priority_input.cascade_margin_abs_distance.saturating_mul(3)
837        + u64::from(priority_input.bridge_checked)
838}
839
840pub fn run_incremental_consistency_fuzz_case(
841    case: IncrementalConsistencyFuzzCaseV0,
842) -> IncrementalConsistencyFuzzResultV0 {
843    let node_count = case.node_count.clamp(1, 64);
844    let previous_input = generated_incremental_fuzz_graph(case.seed, node_count, None);
845    let previous_snapshot = snapshot_from_graph_input(&previous_input);
846    let changed_index = case
847        .changed_node_index
848        .map(|index| index.min(node_count.saturating_sub(1)));
849    let next_input = generated_incremental_fuzz_graph(case.seed, node_count, changed_index);
850    let mut database = OmenaIncrementalDatabaseV0::default();
851    database.restore_snapshot(&previous_snapshot);
852    let plan = database
853        .plan_and_upsert_graph_input(&next_input)
854        .incremental_plan;
855    let changed_node_id = changed_index.map(fuzz_node_id);
856    let expected_dirty_ids = changed_node_id
857        .as_ref()
858        .map(|changed_id| transitive_dependents(&next_input, changed_id))
859        .unwrap_or_default();
860    let actual_dirty_ids = plan
861        .nodes
862        .iter()
863        .filter(|node| node.dirty)
864        .map(|node| node.id.clone())
865        .collect::<BTreeSet<_>>();
866    let expected_dirty_node_count = expected_dirty_ids.len();
867    let passed = actual_dirty_ids == expected_dirty_ids
868        && plan.dirty_node_count == expected_dirty_node_count
869        && plan.changed_input_count == usize::from(changed_node_id.is_some());
870
871    IncrementalConsistencyFuzzResultV0 {
872        seed: case.seed,
873        node_count,
874        changed_node_id,
875        dirty_node_count: plan.dirty_node_count,
876        expected_dirty_node_count,
877        passed,
878    }
879}
880
881pub fn run_incremental_fuzz_seed_corpus() -> IncrementalFuzzSeedReportV0 {
882    let seeds = [1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233];
883    let results = seeds
884        .into_iter()
885        .enumerate()
886        .map(|(index, seed)| {
887            run_incremental_consistency_fuzz_case(IncrementalConsistencyFuzzCaseV0 {
888                seed,
889                node_count: index + 1,
890                changed_node_index: if index % 4 == 0 {
891                    None
892                } else {
893                    Some(index / 2)
894                },
895            })
896        })
897        .collect::<Vec<_>>();
898    let passed_count = results.iter().filter(|result| result.passed).count();
899    let case_count = results.len();
900
901    IncrementalFuzzSeedReportV0 {
902        schema_version: "0",
903        product: "omena-incremental.fuzz-seed-corpus",
904        case_count,
905        passed_count,
906        failed_count: case_count - passed_count,
907        results,
908    }
909}
910
911pub fn summarize_incremental_layer_evidence_v0() -> IncrementalLayerEvidenceV0 {
912    let boundary = summarize_omena_incremental_boundary();
913    let fuzz_report = run_incremental_fuzz_seed_corpus();
914    let mut database = OmenaIncrementalDatabaseV0::default();
915    let previous_input = IncrementalGraphInputV0 {
916        revision: IncrementalRevisionV0 { value: 1 },
917        nodes: vec![
918            IncrementalNodeInputV0 {
919                id: "source".to_string(),
920                digest: "source:v1".to_string(),
921                dependency_ids: Vec::new(),
922            },
923            IncrementalNodeInputV0 {
924                id: "style".to_string(),
925                digest: "style:v1".to_string(),
926                dependency_ids: vec!["source".to_string()],
927            },
928        ],
929    };
930    database.plan_and_upsert_graph_input(&previous_input);
931    let sample_priority_inputs = vec![IncrementalEditDistancePriorityInputV0 {
932        schema_version: "0",
933        product: "omena-incremental.edit-distance-priority-input",
934        feature_gate: "incremental-edit-distance-priority-v0",
935        claim_level: "fixtureWitnessMetricInput",
936        theorem_claimed: false,
937        node_id: "style".to_string(),
938        edit_distance_total: 3,
939        cascade_margin_abs_distance: 2,
940        bridge_checked: true,
941        bridge_calibration_stage: "fixtureWitnessOnlyUncalibrated",
942    }];
943    let sample_update = database.plan_and_upsert_graph_input_with_priority_inputs(
944        &IncrementalGraphInputV0 {
945            revision: IncrementalRevisionV0 { value: 2 },
946            nodes: vec![
947                IncrementalNodeInputV0 {
948                    id: "source".to_string(),
949                    digest: "source:v2".to_string(),
950                    dependency_ids: Vec::new(),
951                },
952                IncrementalNodeInputV0 {
953                    id: "style".to_string(),
954                    digest: "style:v1".to_string(),
955                    dependency_ids: vec!["source".to_string()],
956                },
957            ],
958        },
959        &sample_priority_inputs,
960    );
961
962    IncrementalLayerEvidenceV0 {
963        schema_version: "0",
964        product: "omena-incremental.layer-evidence",
965        claim_level: "m6IncrementalLayerEvidenceOnly",
966        invalidation_layer: "stableNodeIdDigestDependencyGraph",
967        real_invalidation_evidence_ready: sample_update.incremental_plan.changed_input_count == 1
968            && sample_update.incremental_plan.dependency_dirty_count == 1
969            && sample_update.incremental_plan.dirty_node_count == 2,
970        fuzz_evidence_ready: fuzz_report.failed_count == 0,
971        salsa_reuse_evidence_ready: boundary
972            .ready_surfaces
973            .contains(&"salsaTrackedNodeSnapshotQuery"),
974        datalog_contract_evidence_ready: sample_update.datalog_rule_evaluator.fixed_point_reached
975            && !sample_update.datalog_rule_evaluator.external_host_ready,
976        value_equality_backdating_ready: sample_update.incremental_plan.nodes.iter().any(|node| {
977            node.id == "style"
978                && node.value_equal_to_previous
979                && node.changed_at.value == 1
980                && node.verified_at.value == 2
981        }),
982        alpha_equivalence_hash_ready: sample_update
983            .incremental_plan
984            .alpha_equivalence_graph_hash
985            .feature_gate
986            == "incremental-alpha-equivalence-hash-v0"
987            && !sample_update
988                .incremental_plan
989                .alpha_equivalence_graph_hash
990                .theorem_claimed,
991        shadow_delta_oracle_ready: sample_update
992            .incremental_plan
993            .shadow_delta_oracle
994            .incremental_matches_from_scratch_delta
995            && !sample_update
996                .incremental_plan
997                .shadow_delta_oracle
998                .theorem_claimed,
999        edit_distance_priority_ready: sample_update
1000            .incremental_plan
1001            .invalidation_priority_plan
1002            .entries
1003            .iter()
1004            .any(|entry| {
1005                entry.node_id == "style"
1006                    && entry.metric_consumed
1007                    && entry.priority_kind == "editDistanceCascadeMarginWeighted"
1008            }),
1009        benchmark_surface_ready: true,
1010        performance_benchmark_claim_ready: false,
1011        external_datalog_host_ready: false,
1012        dbsp_zset_claim_ready: false,
1013        public_safety_claim_ready: false,
1014        benchmark_gate: "rust/z5-performance-baseline-readiness",
1015        benchmark_evidence_level: "configuredCriterionSurfaceNoTimingClaim",
1016        supported_claims: vec![
1017            "stable node id plus digest invalidation",
1018            "dependency dirty-set fixed point",
1019            "Salsa-backed tracked node snapshot reuse",
1020            "fuzzed dirty-set invariant corpus",
1021            "Datalog-shaped audit contract over the incremental plan",
1022            "value-equality backdating with changed_at/verified_at split",
1023            "alpha-equivalence-aware fixture hash",
1024            "sampled incremental-vs-from-scratch shadow delta oracle",
1025            "edit-distance weighted invalidation priority",
1026        ],
1027        deferred_claims: vec![
1028            "DBSP runtime",
1029            "Z-set differential dataflow semantics",
1030            "external Datalog host execution",
1031            "performance superiority from local timing data",
1032            "public safety claim",
1033        ],
1034        boundary,
1035        fuzz_report,
1036        sample_update,
1037    }
1038}
1039
1040#[salsa::tracked(returns(clone))]
1041pub fn summarize_salsa_incremental_node_snapshot(
1042    db: &dyn salsa::Database,
1043    node: SalsaIncrementalNodeInputV0,
1044) -> IncrementalSnapshotNodeV0 {
1045    IncrementalSnapshotNodeV0 {
1046        id: node.id(db).clone(),
1047        digest: node.digest(db).clone(),
1048        dependency_ids: normalized_ids(node.dependency_ids(db)),
1049    }
1050}
1051
1052#[salsa::tracked(returns(clone))]
1053pub fn read_salsa_incremental_node_digest(
1054    db: &dyn salsa::Database,
1055    node: SalsaIncrementalNodeInputV0,
1056) -> String {
1057    #[cfg(test)]
1058    omena_testkit::current_instrumentation_session_v0().record_salsa_digest_query_run();
1059
1060    node.digest(db).clone()
1061}
1062
1063#[salsa::tracked(returns(clone))]
1064pub fn read_salsa_incremental_node_dependency_ids(
1065    db: &dyn salsa::Database,
1066    node: SalsaIncrementalNodeInputV0,
1067) -> Vec<String> {
1068    #[cfg(test)]
1069    omena_testkit::current_instrumentation_session_v0().record_salsa_dependency_query_run();
1070
1071    normalized_ids(node.dependency_ids(db))
1072}
1073
1074#[salsa::tracked(returns(clone))]
1075fn read_salsa_incremental_node_dependency_edges(
1076    db: &dyn salsa::Database,
1077    node: SalsaIncrementalNodeInputV0,
1078) -> Vec<String> {
1079    normalized_ids(node.dependency_ids(db))
1080}
1081
1082#[cfg(test)]
1083#[salsa::tracked(returns(clone))]
1084fn read_salsa_transitive_leaf(
1085    db: &dyn salsa::Database,
1086    node: SalsaIncrementalNodeInputV0,
1087) -> String {
1088    omena_testkit::current_instrumentation_session_v0().record_salsa_transitive_leaf_query_run();
1089    node.digest(db).clone()
1090}
1091
1092#[cfg(test)]
1093#[salsa::tracked(returns(clone))]
1094fn read_salsa_transitive_a(db: &dyn salsa::Database, a: SalsaIncrementalNodeInputV0) -> String {
1095    omena_testkit::current_instrumentation_session_v0().record_salsa_transitive_a_query_run();
1096    format!("a={}", read_salsa_transitive_leaf(db, a))
1097}
1098
1099#[cfg(test)]
1100#[salsa::tracked(returns(clone))]
1101fn read_salsa_transitive_b(
1102    db: &dyn salsa::Database,
1103    a: SalsaIncrementalNodeInputV0,
1104    b: SalsaIncrementalNodeInputV0,
1105) -> String {
1106    omena_testkit::current_instrumentation_session_v0().record_salsa_transitive_b_query_run();
1107    format!(
1108        "{}|b={}",
1109        read_salsa_transitive_a(db, a),
1110        read_salsa_transitive_leaf(db, b)
1111    )
1112}
1113
1114#[cfg(test)]
1115#[salsa::tracked(returns(clone))]
1116fn read_salsa_transitive_c(
1117    db: &dyn salsa::Database,
1118    a: SalsaIncrementalNodeInputV0,
1119    b: SalsaIncrementalNodeInputV0,
1120    c: SalsaIncrementalNodeInputV0,
1121) -> String {
1122    omena_testkit::current_instrumentation_session_v0().record_salsa_transitive_c_query_run();
1123    format!(
1124        "{}|c={}",
1125        read_salsa_transitive_b(db, a, b),
1126        read_salsa_transitive_leaf(db, c)
1127    )
1128}
1129
1130#[cfg(test)]
1131#[salsa::tracked(returns(clone))]
1132fn read_salsa_transitive_unrelated(
1133    db: &dyn salsa::Database,
1134    node: SalsaIncrementalNodeInputV0,
1135) -> String {
1136    omena_testkit::current_instrumentation_session_v0()
1137        .record_salsa_transitive_unrelated_query_run();
1138    format!("u={}", read_salsa_transitive_leaf(db, node))
1139}
1140
1141#[salsa::tracked(returns(clone))]
1142pub fn read_salsa_file_revision_syntax_key(
1143    db: &dyn salsa::Database,
1144    input: SalsaIncrementalFileRevisionInputV0,
1145) -> String {
1146    let revision = input.revision(db);
1147    format!(
1148        "file={};revision={};syntax={}",
1149        input.file_id(db),
1150        revision.value,
1151        input.syntax_node_id(db)
1152    )
1153}
1154
1155pub fn read_salsa_incremental_node_value(
1156    db: &dyn salsa::Database,
1157    graph: SalsaIncrementalGraphInputV0,
1158    node: SalsaIncrementalNodeInputV0,
1159) -> String {
1160    read_salsa_incremental_node_value_with_path(db, graph, node, String::new())
1161}
1162
1163pub fn read_salsa_incremental_node_dirty_signature(
1164    db: &dyn salsa::Database,
1165    graph: SalsaIncrementalGraphInputV0,
1166    node: SalsaIncrementalNodeInputV0,
1167) -> String {
1168    read_salsa_incremental_node_dirty_signature_with_path(db, graph, node, String::new())
1169}
1170
1171#[salsa::tracked(returns(clone))]
1172fn read_salsa_incremental_node_value_with_path(
1173    db: &dyn salsa::Database,
1174    graph: SalsaIncrementalGraphInputV0,
1175    node: SalsaIncrementalNodeInputV0,
1176    path_key: String,
1177) -> String {
1178    let id = node.id(db).clone();
1179    #[cfg(test)]
1180    record_salsa_node_value_query_run(id.as_str());
1181
1182    if path_contains_id(path_key.as_str(), id.as_str()) {
1183        return format!("{id}=<cycle>");
1184    }
1185
1186    let digest = node.digest(db).clone();
1187    let next_path = append_path_id(path_key.as_str(), id.as_str());
1188    let dependency_values = read_salsa_incremental_node_dependency_edges(db, node)
1189        .into_iter()
1190        .map(|dependency_id| {
1191            if path_contains_id(next_path.as_str(), dependency_id.as_str()) {
1192                return format!("{dependency_id}=<cycle>");
1193            }
1194            find_salsa_incremental_node_by_id(db, graph, dependency_id.as_str())
1195                .map(|dependency| {
1196                    read_salsa_incremental_node_value_with_path(
1197                        db,
1198                        graph,
1199                        dependency,
1200                        next_path.clone(),
1201                    )
1202                })
1203                .unwrap_or_else(|| format!("{dependency_id}=<missing>"))
1204        })
1205        .collect::<Vec<_>>();
1206
1207    format!("{id}={digest};deps=[{}]", dependency_values.join(","))
1208}
1209
1210#[salsa::tracked(returns(clone))]
1211fn read_salsa_incremental_node_dirty_signature_with_path(
1212    db: &dyn salsa::Database,
1213    graph: SalsaIncrementalGraphInputV0,
1214    node: SalsaIncrementalNodeInputV0,
1215    path_key: String,
1216) -> String {
1217    let id = node.id(db).clone();
1218    if path_contains_id(path_key.as_str(), id.as_str()) {
1219        return stable_hash_hex(format!("cycle:{id}").as_bytes());
1220    }
1221
1222    let digest = node.digest(db).clone();
1223    let next_path = append_path_id(path_key.as_str(), id.as_str());
1224    let dependency_signatures = read_salsa_incremental_node_dependency_edges(db, node)
1225        .into_iter()
1226        .map(|dependency_id| {
1227            if path_contains_id(next_path.as_str(), dependency_id.as_str()) {
1228                return stable_hash_hex(format!("cycle:{dependency_id}").as_bytes());
1229            }
1230            find_salsa_incremental_node_by_id(db, graph, dependency_id.as_str())
1231                .map(|dependency| {
1232                    read_salsa_incremental_node_dirty_signature_with_path(
1233                        db,
1234                        graph,
1235                        dependency,
1236                        next_path.clone(),
1237                    )
1238                })
1239                .unwrap_or_else(|| stable_hash_hex(format!("missing:{dependency_id}").as_bytes()))
1240        })
1241        .collect::<Vec<_>>();
1242    let signature = format!("digest={digest};deps=[{}]", dependency_signatures.join(","));
1243    stable_hash_hex(signature.as_bytes())
1244}
1245
1246fn find_salsa_incremental_node_by_id(
1247    db: &dyn salsa::Database,
1248    graph: SalsaIncrementalGraphInputV0,
1249    id: &str,
1250) -> Option<SalsaIncrementalNodeInputV0> {
1251    graph
1252        .nodes(db)
1253        .iter()
1254        .find(|node| node.id(db).as_str() == id)
1255        .copied()
1256}
1257
1258fn path_contains_id(path_key: &str, id: &str) -> bool {
1259    path_key.split('\n').any(|entry| entry == id)
1260}
1261
1262fn append_path_id(path_key: &str, id: &str) -> String {
1263    if path_key.is_empty() {
1264        id.to_string()
1265    } else {
1266        format!("{path_key}\n{id}")
1267    }
1268}
1269
1270fn normalized_snapshot_nodes(input: &IncrementalGraphInputV0) -> Vec<IncrementalSnapshotNodeV0> {
1271    let mut nodes = input
1272        .nodes
1273        .iter()
1274        .map(|node| IncrementalSnapshotNodeV0 {
1275            id: node.id.clone(),
1276            digest: node.digest.clone(),
1277            dependency_ids: normalized_ids(&node.dependency_ids),
1278        })
1279        .collect::<Vec<_>>();
1280    nodes.sort_by(|left, right| left.id.cmp(&right.id));
1281    nodes
1282}
1283
1284fn normalized_existing_snapshot_nodes(
1285    nodes: &[IncrementalSnapshotNodeV0],
1286) -> Vec<IncrementalSnapshotNodeV0> {
1287    let mut nodes = nodes
1288        .iter()
1289        .map(|node| IncrementalSnapshotNodeV0 {
1290            id: node.id.clone(),
1291            digest: node.digest.clone(),
1292            dependency_ids: normalized_ids(&node.dependency_ids),
1293        })
1294        .collect::<Vec<_>>();
1295    nodes.sort_by(|left, right| left.id.cmp(&right.id));
1296    nodes
1297}
1298
1299fn normalized_ids(ids: &[String]) -> Vec<String> {
1300    ids.iter()
1301        .cloned()
1302        .collect::<BTreeSet<_>>()
1303        .into_iter()
1304        .collect()
1305}
1306
1307fn summarize_alpha_equivalence_hash(
1308    input: &IncrementalGraphInputV0,
1309) -> IncrementalAlphaEquivalenceHashV0 {
1310    let node_hashes = alpha_equivalence_hashes_by_node(input);
1311    let normalized_node_count = node_hashes.len();
1312    let normalized_edge_count = input
1313        .nodes
1314        .iter()
1315        .map(|node| normalized_ids(&node.dependency_ids).len())
1316        .sum();
1317    let mut labels = node_hashes.into_values().collect::<Vec<_>>();
1318    labels.sort();
1319    let labels = labels.join("|");
1320    let hash = stable_hash_hex(
1321        format!("nodes={normalized_node_count};edges={normalized_edge_count};labels={labels}")
1322            .as_bytes(),
1323    );
1324
1325    IncrementalAlphaEquivalenceHashV0 {
1326        schema_version: "0",
1327        product: "omena-incremental.alpha-equivalence-hash",
1328        feature_gate: "incremental-alpha-equivalence-hash-v0",
1329        claim_level: "fixtureWitnessAlphaRenamingStableHash",
1330        theorem_claimed: false,
1331        hash,
1332        normalized_node_count,
1333        normalized_edge_count,
1334    }
1335}
1336
1337fn alpha_equivalence_hashes_by_node(input: &IncrementalGraphInputV0) -> BTreeMap<String, String> {
1338    let nodes = normalized_snapshot_nodes(input);
1339    alpha_equivalence_hashes_for_snapshot_nodes(&nodes)
1340}
1341
1342fn alpha_equivalence_hashes_by_snapshot_nodes(
1343    nodes: &[IncrementalSnapshotNodeV0],
1344) -> BTreeMap<String, String> {
1345    let nodes = normalized_existing_snapshot_nodes(nodes);
1346    alpha_equivalence_hashes_for_snapshot_nodes(&nodes)
1347}
1348
1349fn alpha_equivalence_hashes_for_snapshot_nodes(
1350    nodes: &[IncrementalSnapshotNodeV0],
1351) -> BTreeMap<String, String> {
1352    let internal_ids = nodes
1353        .iter()
1354        .map(|node| node.id.as_str())
1355        .collect::<BTreeSet<_>>();
1356    let mut labels = nodes
1357        .iter()
1358        .map(|node| {
1359            (
1360                node.id.clone(),
1361                stable_hash_hex(format!("digest={}", node.digest).as_bytes()),
1362            )
1363        })
1364        .collect::<BTreeMap<_, _>>();
1365
1366    for _ in 0..=nodes.len() {
1367        let next = nodes
1368            .iter()
1369            .map(|node| {
1370                let mut dependency_labels = node
1371                    .dependency_ids
1372                    .iter()
1373                    .map(|dependency_id| {
1374                        if internal_ids.contains(dependency_id.as_str()) {
1375                            labels
1376                                .get(dependency_id)
1377                                .cloned()
1378                                .unwrap_or_else(|| stable_hash_hex(dependency_id.as_bytes()))
1379                        } else {
1380                            format!("external:{dependency_id}")
1381                        }
1382                    })
1383                    .collect::<Vec<_>>();
1384                dependency_labels.sort();
1385                let signature = format!(
1386                    "digest={};deps={}",
1387                    node.digest,
1388                    dependency_labels.join(",")
1389                );
1390                (node.id.clone(), stable_hash_hex(signature.as_bytes()))
1391            })
1392            .collect::<BTreeMap<_, _>>();
1393        if next == labels {
1394            break;
1395        }
1396        labels = next;
1397    }
1398
1399    labels
1400}
1401
1402fn unique_previous_nodes_by_alpha_hash<'a>(
1403    nodes: &'a [IncrementalSnapshotNodeV0],
1404    hashes_by_id: &BTreeMap<String, String>,
1405) -> BTreeMap<String, &'a IncrementalSnapshotNodeV0> {
1406    let mut unique = BTreeMap::new();
1407    let mut duplicates = BTreeSet::new();
1408    for node in nodes {
1409        let Some(hash) = hashes_by_id.get(node.id.as_str()) else {
1410            continue;
1411        };
1412        if unique.insert(hash.clone(), node).is_some() {
1413            duplicates.insert(hash.clone());
1414        }
1415    }
1416    for duplicate in duplicates {
1417        unique.remove(duplicate.as_str());
1418    }
1419    unique
1420}
1421
1422fn snapshot_node_value_matches(
1423    previous_node: &IncrementalSnapshotNodeV0,
1424    node: &IncrementalSnapshotNodeV0,
1425) -> bool {
1426    previous_node.digest == node.digest && previous_node.dependency_ids == node.dependency_ids
1427}
1428
1429fn compute_from_scratch_delta_dirty_ids(
1430    input: &IncrementalGraphInputV0,
1431    previous: Option<&IncrementalSnapshotV0>,
1432) -> BTreeSet<String> {
1433    let normalized_nodes = normalized_snapshot_nodes(input);
1434    let alpha_hashes_by_id = alpha_equivalence_hashes_by_node(input);
1435    let previous_alpha_hashes_by_id = previous
1436        .map(|snapshot| alpha_equivalence_hashes_by_snapshot_nodes(&snapshot.nodes))
1437        .unwrap_or_default();
1438    let previous_by_alpha_hash = previous
1439        .map(|snapshot| {
1440            unique_previous_nodes_by_alpha_hash(&snapshot.nodes, &previous_alpha_hashes_by_id)
1441        })
1442        .unwrap_or_default();
1443    let previous_by_id = previous
1444        .map(|snapshot| {
1445            snapshot
1446                .nodes
1447                .iter()
1448                .map(|node| (node.id.as_str(), node))
1449                .collect::<BTreeMap<_, _>>()
1450        })
1451        .unwrap_or_default();
1452    let mut dirty_ids = normalized_nodes
1453        .iter()
1454        .filter_map(|node| {
1455            let alpha_equivalence_hash = alpha_hashes_by_id
1456                .get(node.id.as_str())
1457                .map(String::as_str)
1458                .unwrap_or(node.id.as_str());
1459            let exact_previous = previous_by_id.get(node.id.as_str()).copied();
1460            let alpha_previous = previous_by_alpha_hash.get(alpha_equivalence_hash).copied();
1461            if exact_previous
1462                .filter(|previous_node| snapshot_node_value_matches(previous_node, node))
1463                .or(alpha_previous)
1464                .is_some()
1465            {
1466                return None;
1467            }
1468            Some(node.id.clone())
1469        })
1470        .collect::<BTreeSet<_>>();
1471
1472    let max_iterations = dependency_propagation_iteration_limit(normalized_nodes.len());
1473    for _ in 0..max_iterations {
1474        let mut changed = false;
1475        for node in &normalized_nodes {
1476            if dirty_ids.contains(node.id.as_str()) {
1477                continue;
1478            }
1479            if node
1480                .dependency_ids
1481                .iter()
1482                .any(|dependency_id| dirty_ids.contains(dependency_id.as_str()))
1483            {
1484                changed = dirty_ids.insert(node.id.clone()) || changed;
1485            }
1486        }
1487        if !changed {
1488            break;
1489        }
1490    }
1491
1492    dirty_ids
1493}
1494
1495fn stable_hash_hex(bytes: &[u8]) -> String {
1496    let mut hash = 0xcbf2_9ce4_8422_2325_u64;
1497    for byte in bytes {
1498        hash ^= u64::from(*byte);
1499        hash = hash.wrapping_mul(0x0000_0100_0000_01b3);
1500    }
1501    format!("{hash:016x}")
1502}
1503
1504fn dirty_set_is_dependency_closed(plan: &IncrementalComputationPlanV0) -> bool {
1505    let dirty_ids = plan
1506        .nodes
1507        .iter()
1508        .filter(|node| node.dirty)
1509        .map(|node| node.id.as_str())
1510        .collect::<BTreeSet<_>>();
1511    plan.nodes.iter().all(|node| {
1512        node.dirty
1513            || node
1514                .dependency_ids
1515                .iter()
1516                .all(|dependency_id| !dirty_ids.contains(dependency_id.as_str()))
1517    })
1518}
1519
1520fn generated_incremental_fuzz_graph(
1521    seed: u64,
1522    node_count: usize,
1523    changed_index: Option<usize>,
1524) -> IncrementalGraphInputV0 {
1525    let mut state = seed ^ 0xa076_1d64_78bd_642f;
1526    let nodes = (0..node_count)
1527        .map(|index| {
1528            let id = fuzz_node_id(index);
1529            let mut digest_seed = fuzz_next(&mut state);
1530            if changed_index == Some(index) {
1531                digest_seed ^= 0xffff_ffff_ffff_ffff;
1532            }
1533            let dependency_ids = (0..index)
1534                .filter(|candidate| {
1535                    let divisor = ((*candidate + 2) as u64).max(2);
1536                    (seed + index as u64).is_multiple_of(divisor)
1537                })
1538                .map(fuzz_node_id)
1539                .collect::<Vec<_>>();
1540            IncrementalNodeInputV0 {
1541                id,
1542                digest: format!("digest-{index}-{digest_seed:016x}"),
1543                dependency_ids,
1544            }
1545        })
1546        .collect();
1547
1548    IncrementalGraphInputV0 {
1549        revision: IncrementalRevisionV0 {
1550            value: 1 + if changed_index.is_some() { 1 } else { 0 },
1551        },
1552        nodes,
1553    }
1554}
1555
1556fn transitive_dependents(input: &IncrementalGraphInputV0, changed_id: &str) -> BTreeSet<String> {
1557    let mut dirty_ids = BTreeSet::from([changed_id.to_string()]);
1558    let max_iterations = dependency_propagation_iteration_limit(input.nodes.len());
1559    for _ in 0..max_iterations {
1560        let mut changed = false;
1561        for node in &input.nodes {
1562            if dirty_ids.contains(&node.id) {
1563                continue;
1564            }
1565            if node
1566                .dependency_ids
1567                .iter()
1568                .any(|dependency_id| dirty_ids.contains(dependency_id))
1569            {
1570                changed = dirty_ids.insert(node.id.clone()) || changed;
1571            }
1572        }
1573        if !changed {
1574            break;
1575        }
1576    }
1577    dirty_ids
1578}
1579
1580fn dependency_propagation_iteration_limit(node_count: usize) -> usize {
1581    node_count.saturating_add(1)
1582}
1583
1584fn fuzz_node_id(index: usize) -> String {
1585    format!("node-{index}")
1586}
1587
1588fn fuzz_next(state: &mut u64) -> u64 {
1589    *state = state
1590        .wrapping_mul(6_364_136_223_846_793_005)
1591        .wrapping_add(1_442_695_040_888_963_407);
1592    *state
1593}
1594
1595impl OmenaIncrementalDatabaseV0 {
1596    pub fn salsa_database(&self) -> &OmenaSalsaDatabaseV0 {
1597        &self.db
1598    }
1599
1600    pub fn node_input(&self, id: &str) -> Option<SalsaIncrementalNodeInputV0> {
1601        self.node_inputs_by_id.get(id).copied()
1602    }
1603
1604    pub fn graph_input(&self) -> Option<SalsaIncrementalGraphInputV0> {
1605        self.graph_input
1606    }
1607
1608    pub fn node_value(&self, id: &str) -> Option<String> {
1609        let graph = self.graph_input?;
1610        let node = self.node_input(id)?;
1611        Some(read_salsa_incremental_node_value(&self.db, graph, node))
1612    }
1613
1614    pub fn node_dirty_signature(&self, id: &str) -> Option<String> {
1615        let graph = self.graph_input?;
1616        let node = self.node_input(id)?;
1617        Some(read_salsa_incremental_node_dirty_signature(
1618            &self.db, graph, node,
1619        ))
1620    }
1621
1622    pub fn current_snapshot(&self) -> Option<&IncrementalSnapshotV0> {
1623        self.current_snapshot.as_ref()
1624    }
1625
1626    pub fn restore_snapshot(&mut self, snapshot: &IncrementalSnapshotV0) {
1627        let input = graph_input_from_snapshot(snapshot);
1628        self.upsert_graph_input(&input);
1629        self.current_snapshot = Some(snapshot.clone());
1630    }
1631
1632    pub fn plan_and_upsert_graph_input(
1633        &mut self,
1634        input: &IncrementalGraphInputV0,
1635    ) -> IncrementalDatabaseUpdateV0 {
1636        self.plan_and_upsert_graph_input_with_priority_inputs(input, &[])
1637    }
1638
1639    pub fn plan_and_upsert_graph_input_with_priority_inputs(
1640        &mut self,
1641        input: &IncrementalGraphInputV0,
1642        priority_inputs: &[IncrementalEditDistancePriorityInputV0],
1643    ) -> IncrementalDatabaseUpdateV0 {
1644        let previous_snapshot = self.current_snapshot.clone();
1645        let previous_signatures = self.dirty_signatures_for_snapshot(previous_snapshot.as_ref());
1646        let next_snapshot = self.upsert_graph_input(input);
1647        let incremental_plan = self.salsa_demand_plan_with_priority_inputs(
1648            input,
1649            previous_snapshot.as_ref(),
1650            previous_signatures,
1651            priority_inputs,
1652        );
1653        let datalog_rule_evaluator =
1654            summarize_datalog_rule_evaluator_for_plan_v0(input, incremental_plan.clone());
1655        self.current_snapshot = Some(next_snapshot.clone());
1656
1657        IncrementalDatabaseUpdateV0 {
1658            schema_version: "0",
1659            product: "omena-incremental.salsa-database-update",
1660            incremental_plan,
1661            datalog_rule_evaluator,
1662            next_snapshot,
1663        }
1664    }
1665
1666    fn dirty_signatures_for_snapshot(
1667        &self,
1668        snapshot: Option<&IncrementalSnapshotV0>,
1669    ) -> (BTreeMap<String, String>, BTreeMap<String, String>) {
1670        let Some(snapshot) = snapshot else {
1671            return (BTreeMap::new(), BTreeMap::new());
1672        };
1673        let Some(graph) = self.graph_input else {
1674            return (BTreeMap::new(), BTreeMap::new());
1675        };
1676        let alpha_hashes_by_id = alpha_equivalence_hashes_by_snapshot_nodes(&snapshot.nodes);
1677        let unique_previous_by_alpha =
1678            unique_previous_nodes_by_alpha_hash(&snapshot.nodes, &alpha_hashes_by_id);
1679        let by_id = snapshot
1680            .nodes
1681            .iter()
1682            .filter_map(|node| {
1683                let node_input = self.node_input(node.id.as_str())?;
1684                Some((
1685                    node.id.clone(),
1686                    read_salsa_incremental_node_dirty_signature(&self.db, graph, node_input),
1687                ))
1688            })
1689            .collect::<BTreeMap<_, _>>();
1690        let by_alpha_hash = unique_previous_by_alpha
1691            .into_iter()
1692            .filter_map(|(alpha_hash, node)| {
1693                by_id
1694                    .get(node.id.as_str())
1695                    .cloned()
1696                    .map(|signature| (alpha_hash, signature))
1697            })
1698            .collect::<BTreeMap<_, _>>();
1699        (by_id, by_alpha_hash)
1700    }
1701
1702    fn salsa_demand_plan_with_priority_inputs(
1703        &self,
1704        input: &IncrementalGraphInputV0,
1705        previous: Option<&IncrementalSnapshotV0>,
1706        previous_signatures: (BTreeMap<String, String>, BTreeMap<String, String>),
1707        priority_inputs: &[IncrementalEditDistancePriorityInputV0],
1708    ) -> IncrementalComputationPlanV0 {
1709        let normalized_nodes = normalized_snapshot_nodes(input);
1710        let alpha_hashes_by_id = alpha_equivalence_hashes_by_node(input);
1711        let alpha_equivalence_graph_hash = summarize_alpha_equivalence_hash(input);
1712        let previous_alpha_hashes_by_id = previous
1713            .map(|snapshot| alpha_equivalence_hashes_by_snapshot_nodes(&snapshot.nodes))
1714            .unwrap_or_default();
1715        let previous_by_alpha_hash = previous
1716            .map(|snapshot| {
1717                unique_previous_nodes_by_alpha_hash(&snapshot.nodes, &previous_alpha_hashes_by_id)
1718            })
1719            .unwrap_or_default();
1720        let previous_by_id = previous
1721            .map(|snapshot| {
1722                snapshot
1723                    .nodes
1724                    .iter()
1725                    .map(|node| (node.id.as_str(), node))
1726                    .collect::<BTreeMap<_, _>>()
1727            })
1728            .unwrap_or_default();
1729        let current_ids = normalized_nodes
1730            .iter()
1731            .map(|node| node.id.as_str())
1732            .collect::<BTreeSet<_>>();
1733        let current_alpha_hashes = alpha_hashes_by_id
1734            .values()
1735            .map(String::as_str)
1736            .collect::<BTreeSet<_>>();
1737        let removed_node_count = previous_by_id
1738            .keys()
1739            .filter(|id| {
1740                if current_ids.contains(**id) {
1741                    return false;
1742                }
1743                previous_alpha_hashes_by_id
1744                    .get(**id)
1745                    .is_none_or(|hash| !current_alpha_hashes.contains(hash.as_str()))
1746            })
1747            .count();
1748        let (previous_signature_by_id, previous_signature_by_alpha_hash) = previous_signatures;
1749        let mut dirty_ids = BTreeSet::<String>::new();
1750        let nodes = normalized_nodes
1751            .into_iter()
1752            .map(|node| {
1753                let alpha_equivalence_hash = alpha_hashes_by_id
1754                    .get(node.id.as_str())
1755                    .cloned()
1756                    .unwrap_or_else(|| stable_hash_hex(node.id.as_bytes()));
1757                let exact_previous = previous_by_id.get(node.id.as_str()).copied();
1758                let alpha_previous = previous_by_alpha_hash
1759                    .get(alpha_equivalence_hash.as_str())
1760                    .copied();
1761                let previous_value_match = exact_previous
1762                    .filter(|previous_node| snapshot_node_value_matches(previous_node, &node))
1763                    .or(alpha_previous);
1764                let current_signature = self.node_dirty_signature(node.id.as_str());
1765                let previous_signature = previous_value_match
1766                    .and_then(|previous_node| {
1767                        previous_signature_by_id.get(previous_node.id.as_str())
1768                    })
1769                    .or_else(|| {
1770                        exact_previous.and_then(|previous_node| {
1771                            previous_signature_by_id.get(previous_node.id.as_str())
1772                        })
1773                    })
1774                    .or_else(|| {
1775                        previous_signature_by_alpha_hash.get(alpha_equivalence_hash.as_str())
1776                    });
1777                let dependency_signature_equal = current_signature
1778                    .as_ref()
1779                    .zip(previous_signature)
1780                    .is_some_and(|(current, previous)| current == previous);
1781                let value_equal_to_previous = previous_value_match.is_some();
1782                let mut reasons = Vec::new();
1783                match previous_value_match.or(exact_previous) {
1784                    None => reasons.push("newNode"),
1785                    Some(previous_node) => {
1786                        if previous_value_match.is_none() {
1787                            if previous_node.digest != node.digest {
1788                                reasons.push("inputDigestChanged");
1789                            }
1790                            if previous_node.dependency_ids != node.dependency_ids {
1791                                reasons.push("dependencySetChanged");
1792                            }
1793                        }
1794                    }
1795                }
1796                if !dependency_signature_equal && reasons.is_empty() {
1797                    reasons.push("dependencyDirty");
1798                }
1799                let changed_at = if value_equal_to_previous {
1800                    previous
1801                        .map(|snapshot| snapshot.revision)
1802                        .unwrap_or(input.revision)
1803                } else {
1804                    input.revision
1805                };
1806                let dirty = !dependency_signature_equal;
1807                if dirty {
1808                    dirty_ids.insert(node.id.clone());
1809                }
1810
1811                IncrementalComputationNodeV0 {
1812                    alpha_equivalence_hash,
1813                    id: node.id,
1814                    digest: node.digest,
1815                    dependency_ids: node.dependency_ids,
1816                    dirty,
1817                    reasons,
1818                    changed_at,
1819                    verified_at: input.revision,
1820                    value_equal_to_previous,
1821                }
1822            })
1823            .collect::<Vec<_>>();
1824        let shadow_delta_oracle =
1825            summarize_incremental_shadow_delta_oracle_v0(input, previous, dirty_ids);
1826        let invalidation_priority_plan =
1827            summarize_incremental_invalidation_priority_plan_v0(&nodes, priority_inputs);
1828
1829        IncrementalComputationPlanV0 {
1830            schema_version: "0",
1831            product: "omena-incremental.computation-plan",
1832            revision: input.revision,
1833            node_count: nodes.len(),
1834            dirty_node_count: nodes.iter().filter(|node| node.dirty).count(),
1835            changed_input_count: nodes
1836                .iter()
1837                .filter(|node| node.reasons.contains(&"inputDigestChanged"))
1838                .count(),
1839            new_node_count: nodes
1840                .iter()
1841                .filter(|node| node.reasons.contains(&"newNode"))
1842                .count(),
1843            removed_node_count,
1844            dependency_dirty_count: nodes
1845                .iter()
1846                .filter(|node| node.reasons.contains(&"dependencyDirty"))
1847                .count(),
1848            alpha_equivalence_graph_hash,
1849            shadow_delta_oracle,
1850            invalidation_priority_plan,
1851            nodes,
1852        }
1853    }
1854
1855    pub fn upsert_graph_input(&mut self, input: &IncrementalGraphInputV0) -> IncrementalSnapshotV0 {
1856        let normalized_nodes = normalized_snapshot_nodes(input);
1857        let current_ids = normalized_nodes
1858            .iter()
1859            .map(|node| node.id.as_str())
1860            .collect::<BTreeSet<_>>();
1861        self.node_inputs_by_id
1862            .retain(|id, _node| current_ids.contains(id.as_str()));
1863
1864        for node in &normalized_nodes {
1865            self.upsert_node_input(node);
1866        }
1867        let graph_nodes = self.node_inputs_by_id.values().copied().collect::<Vec<_>>();
1868        self.sync_graph_input(graph_nodes);
1869
1870        let nodes = self
1871            .node_inputs_by_id
1872            .values()
1873            .copied()
1874            .map(|node| summarize_salsa_incremental_node_snapshot(&self.db, node))
1875            .collect::<Vec<_>>();
1876
1877        IncrementalSnapshotV0 {
1878            schema_version: "0",
1879            product: "omena-incremental.salsa-snapshot",
1880            revision: input.revision,
1881            nodes,
1882        }
1883    }
1884
1885    fn upsert_node_input(&mut self, node: &IncrementalSnapshotNodeV0) {
1886        let Some(node_input) = self.node_inputs_by_id.get(node.id.as_str()).copied() else {
1887            let node_input = SalsaIncrementalNodeInputV0::new(
1888                &self.db,
1889                node.id.clone(),
1890                node.digest.clone(),
1891                node.dependency_ids.clone(),
1892            );
1893            self.node_inputs_by_id.insert(node.id.clone(), node_input);
1894            return;
1895        };
1896
1897        if node_input.digest(&self.db).as_str() != node.digest.as_str() {
1898            node_input.set_digest(&mut self.db).to(node.digest.clone());
1899        }
1900        if node_input.dependency_ids(&self.db).as_slice() != node.dependency_ids.as_slice() {
1901            node_input
1902                .set_dependency_ids(&mut self.db)
1903                .to(node.dependency_ids.clone());
1904        }
1905    }
1906
1907    fn sync_graph_input(&mut self, nodes: Vec<SalsaIncrementalNodeInputV0>) {
1908        match self.graph_input {
1909            Some(graph) => {
1910                if graph.nodes(&self.db).as_slice() != nodes.as_slice() {
1911                    graph.set_nodes(&mut self.db).to(nodes);
1912                }
1913            }
1914            None => {
1915                self.graph_input = Some(SalsaIncrementalGraphInputV0::new(&self.db, nodes));
1916            }
1917        }
1918    }
1919}
1920
1921impl Default for IncrementalCancellationRegistryV0 {
1922    fn default() -> Self {
1923        Self::with_limit(DEFAULT_INCREMENTAL_CANCELLATION_LIMIT)
1924    }
1925}
1926
1927impl IncrementalCancellationRegistryV0 {
1928    pub fn with_limit(limit: usize) -> Self {
1929        Self {
1930            limit: limit.max(1),
1931            cancelled_request_ids: BTreeSet::new(),
1932        }
1933    }
1934
1935    pub fn cancel(&mut self, request_id: impl Into<String>) {
1936        if self.cancelled_request_ids.len() >= self.limit {
1937            self.cancelled_request_ids.clear();
1938        }
1939        self.cancelled_request_ids.insert(request_id.into());
1940    }
1941
1942    pub fn take_cancelled(&mut self, request_id: &str) -> bool {
1943        self.cancelled_request_ids.remove(request_id)
1944    }
1945
1946    pub fn take_cancelled_result(&mut self, request_id: &str) -> Result<(), salsa::Cancelled> {
1947        if self.take_cancelled(request_id) {
1948            Err(salsa::Cancelled::Local)
1949        } else {
1950            Ok(())
1951        }
1952    }
1953
1954    pub fn len(&self) -> usize {
1955        self.cancelled_request_ids.len()
1956    }
1957
1958    pub fn is_empty(&self) -> bool {
1959        self.cancelled_request_ids.is_empty()
1960    }
1961
1962    pub fn snapshot(&self) -> IncrementalCancellationSnapshotV0 {
1963        IncrementalCancellationSnapshotV0 {
1964            schema_version: "0",
1965            product: "omena-incremental.cancellation-registry",
1966            cancelled_request_count: self.cancelled_request_ids.len(),
1967            cancelled_request_ids: self.cancelled_request_ids.iter().cloned().collect(),
1968        }
1969    }
1970}
1971
1972#[cfg(test)]
1973mod tests {
1974    use super::{
1975        GuaranteeKindV0, IncrementalCancellationRegistryV0, IncrementalGraphInputV0,
1976        IncrementalNodeInputV0, IncrementalRevisionV0, OmenaIncrementalDatabaseV0,
1977        OmenaSalsaDatabaseV0, OmenaWorkspaceSnapshotIdV0, SalsaIncrementalNodeInputV0,
1978        read_salsa_incremental_node_dependency_ids, read_salsa_incremental_node_digest,
1979        read_salsa_transitive_c, read_salsa_transitive_unrelated,
1980        reset_salsa_node_value_query_runs, salsa_node_value_query_runs, snapshot_from_graph_input,
1981        summarize_datalog_rule_evaluator_v0, summarize_incremental_layer_evidence_v0,
1982        summarize_omena_incremental_boundary,
1983    };
1984    use omena_evidence_graph::GuaranteeFamilyV0;
1985    use omena_testkit::{InstrumentationSessionV0, with_instrumentation_session};
1986    use salsa::Setter;
1987    use std::collections::BTreeSet;
1988
1989    #[test]
1990    fn summarizes_incremental_boundary() {
1991        let summary = summarize_omena_incremental_boundary();
1992
1993        assert_eq!(summary.product, "omena-incremental.boundary");
1994        assert_eq!(
1995            summary.query_model,
1996            "salsaInput+trackedQueryFieldGranularReuse"
1997        );
1998        assert_eq!(
1999            summary.dependency_propagation_policy,
2000            "salsaDemandDirtySignatureReads"
2001        );
2002        assert_eq!(
2003            summary.maximum_dependency_propagation_iterations,
2004            "oracleOnlyNodeCount+1"
2005        );
2006        assert!(summary.dirty_reasons.contains(&"dependencyDirty"));
2007        assert!(
2008            summary
2009                .ready_surfaces
2010                .contains(&"incrementalCancellationRegistry")
2011        );
2012        assert!(summary.ready_surfaces.contains(&"datalogRuleEvaluatorV0"));
2013        assert!(
2014            summary
2015                .ready_surfaces
2016                .contains(&"salsaTrackedNodeSnapshotQuery")
2017        );
2018        assert!(
2019            summary
2020                .ready_surfaces
2021                .contains(&"salsaDemandDependencyReads")
2022        );
2023    }
2024
2025    #[test]
2026    fn workspace_snapshot_id_rekeys_incremental_revision() {
2027        let first_revision = IncrementalRevisionV0 { value: 7 };
2028        let same_revision = IncrementalRevisionV0 { value: 7 };
2029        let next_revision = IncrementalRevisionV0 { value: 8 };
2030
2031        let first_id = OmenaWorkspaceSnapshotIdV0::from_revision(first_revision);
2032        let same_id = OmenaWorkspaceSnapshotIdV0::from_revision(same_revision);
2033        let next_id = OmenaWorkspaceSnapshotIdV0::from_revision(next_revision);
2034
2035        assert_eq!(first_id, same_id);
2036        assert_ne!(first_id, next_id);
2037        assert_eq!(first_id.revision(), first_revision);
2038    }
2039
2040    #[test]
2041    fn first_plan_marks_all_nodes_dirty() {
2042        let input = sample_input("a:v1", "b:v1", 1);
2043        let plan = plan_from_database(&input, None);
2044
2045        assert_eq!(plan.product, "omena-incremental.computation-plan");
2046        assert_eq!(plan.node_count, 2);
2047        assert_eq!(plan.dirty_node_count, 2);
2048        assert_eq!(plan.new_node_count, 2);
2049    }
2050
2051    #[test]
2052    fn unchanged_second_plan_marks_nodes_clean() {
2053        let input = sample_input("a:v1", "b:v1", 1);
2054        let snapshot = snapshot_from_graph_input(&input);
2055        let next_input = sample_input("a:v1", "b:v1", 2);
2056        let plan = plan_from_database(&next_input, Some(&snapshot));
2057
2058        assert_eq!(plan.dirty_node_count, 0);
2059        assert_eq!(plan.changed_input_count, 0);
2060        assert_eq!(
2061            plan.shadow_delta_oracle.incremental_dirty_ids,
2062            Vec::<String>::new()
2063        );
2064        assert!(
2065            plan.shadow_delta_oracle
2066                .incremental_matches_from_scratch_delta
2067        );
2068        let Some(b) = node_by_id(&plan, "b") else {
2069            assert!(plan.nodes.iter().any(|node| node.id == "b"));
2070            return;
2071        };
2072        assert_eq!(b.changed_at.value, 1);
2073        assert_eq!(b.verified_at.value, 2);
2074        assert!(b.value_equal_to_previous);
2075    }
2076
2077    #[test]
2078    fn changed_dependency_marks_dependent_dirty() {
2079        let input = sample_input("a:v1", "b:v1", 1);
2080        let snapshot = snapshot_from_graph_input(&input);
2081        let next_input = sample_input("a:v2", "b:v1", 2);
2082        let plan = plan_from_database(&next_input, Some(&snapshot));
2083
2084        assert_eq!(plan.changed_input_count, 1);
2085        assert_eq!(plan.dependency_dirty_count, 1);
2086        assert_eq!(node_reasons(&plan, "a"), vec!["inputDigestChanged"]);
2087        assert_eq!(node_reasons(&plan, "b"), vec!["dependencyDirty"]);
2088        assert_eq!(
2089            plan.shadow_delta_oracle.incremental_dirty_ids,
2090            vec!["a".to_string(), "b".to_string()]
2091        );
2092        assert_eq!(
2093            plan.shadow_delta_oracle.from_scratch_dirty_ids,
2094            plan.shadow_delta_oracle.incremental_dirty_ids
2095        );
2096        assert!(
2097            plan.shadow_delta_oracle
2098                .incremental_matches_from_scratch_delta
2099        );
2100
2101        let Some(changed) = node_by_id(&plan, "a") else {
2102            assert!(plan.nodes.iter().any(|node| node.id == "a"));
2103            return;
2104        };
2105        assert_eq!(changed.changed_at.value, 2);
2106        assert_eq!(changed.verified_at.value, 2);
2107        assert!(!changed.value_equal_to_previous);
2108
2109        let Some(backdated) = node_by_id(&plan, "b") else {
2110            assert!(plan.nodes.iter().any(|node| node.id == "b"));
2111            return;
2112        };
2113        assert_eq!(backdated.changed_at.value, 1);
2114        assert_eq!(backdated.verified_at.value, 2);
2115        assert!(backdated.value_equal_to_previous);
2116    }
2117
2118    #[test]
2119    fn alpha_equivalence_hash_ignores_fixture_node_renaming() {
2120        let left = sample_input("root:v1", "leaf:v1", 1);
2121        let right = IncrementalGraphInputV0 {
2122            revision: IncrementalRevisionV0 { value: 1 },
2123            nodes: vec![
2124                IncrementalNodeInputV0 {
2125                    id: "renamed-leaf".to_string(),
2126                    digest: "leaf:v1".to_string(),
2127                    dependency_ids: vec!["renamed-root".to_string()],
2128                },
2129                IncrementalNodeInputV0 {
2130                    id: "renamed-root".to_string(),
2131                    digest: "root:v1".to_string(),
2132                    dependency_ids: Vec::new(),
2133                },
2134            ],
2135        };
2136        let left_plan = plan_from_database(&left, None);
2137        let right_plan = plan_from_database(&right, None);
2138
2139        assert_eq!(
2140            left_plan.alpha_equivalence_graph_hash.product,
2141            "omena-incremental.alpha-equivalence-hash"
2142        );
2143        assert_eq!(
2144            left_plan.alpha_equivalence_graph_hash.feature_gate,
2145            "incremental-alpha-equivalence-hash-v0"
2146        );
2147        assert!(!left_plan.alpha_equivalence_graph_hash.theorem_claimed);
2148        assert_eq!(
2149            left_plan.alpha_equivalence_graph_hash.hash,
2150            right_plan.alpha_equivalence_graph_hash.hash
2151        );
2152    }
2153
2154    #[test]
2155    fn preceding_sibling_insert_keeps_shifted_nodes_clean_by_alpha_hash() {
2156        let previous = IncrementalGraphInputV0 {
2157            revision: IncrementalRevisionV0 { value: 1 },
2158            nodes: vec![
2159                IncrementalNodeInputV0 {
2160                    id: "path:0".to_string(),
2161                    digest: "button:v1".to_string(),
2162                    dependency_ids: Vec::new(),
2163                },
2164                IncrementalNodeInputV0 {
2165                    id: "path:1".to_string(),
2166                    digest: "card:v1".to_string(),
2167                    dependency_ids: Vec::new(),
2168                },
2169            ],
2170        };
2171        let previous_snapshot = snapshot_from_graph_input(&previous);
2172        let next = IncrementalGraphInputV0 {
2173            revision: IncrementalRevisionV0 { value: 2 },
2174            nodes: vec![
2175                IncrementalNodeInputV0 {
2176                    id: "path:0".to_string(),
2177                    digest: "import:v1".to_string(),
2178                    dependency_ids: Vec::new(),
2179                },
2180                IncrementalNodeInputV0 {
2181                    id: "path:1".to_string(),
2182                    digest: "button:v1".to_string(),
2183                    dependency_ids: Vec::new(),
2184                },
2185                IncrementalNodeInputV0 {
2186                    id: "path:2".to_string(),
2187                    digest: "card:v1".to_string(),
2188                    dependency_ids: Vec::new(),
2189                },
2190            ],
2191        };
2192        let plan = plan_from_database(&next, Some(&previous_snapshot));
2193        let dirty_ids = plan
2194            .nodes
2195            .iter()
2196            .filter(|node| node.dirty)
2197            .map(|node| node.id.as_str())
2198            .collect::<Vec<_>>();
2199
2200        assert_eq!(dirty_ids, vec!["path:0"]);
2201        assert!(node_by_id(&plan, "path:1").is_some_and(|node| node.value_equal_to_previous));
2202        assert!(node_by_id(&plan, "path:2").is_some_and(|node| node.value_equal_to_previous));
2203    }
2204
2205    #[test]
2206    fn incremental_shadow_delta_oracle_matches_from_scratch_delta() {
2207        let previous = sample_input("a:v1", "b:v1", 1);
2208        let previous_snapshot = snapshot_from_graph_input(&previous);
2209        let next = sample_input("a:v2", "b:v1", 2);
2210        let plan = plan_from_database(&next, Some(&previous_snapshot));
2211
2212        assert_eq!(
2213            plan.shadow_delta_oracle.product,
2214            "omena-incremental.shadow-delta-oracle"
2215        );
2216        assert_eq!(
2217            plan.shadow_delta_oracle.feature_gate,
2218            "incremental-shadow-delta-v0"
2219        );
2220        assert_eq!(
2221            plan.shadow_delta_oracle.claim_level,
2222            "sampledFixtureWitnessNotEquivalenceProof"
2223        );
2224        assert!(!plan.shadow_delta_oracle.theorem_claimed);
2225        assert_eq!(
2226            plan.shadow_delta_oracle.incremental_dirty_ids,
2227            vec!["a".to_string(), "b".to_string()]
2228        );
2229        assert_eq!(
2230            plan.shadow_delta_oracle.incremental_dirty_ids,
2231            plan.shadow_delta_oracle.from_scratch_dirty_ids
2232        );
2233        assert!(
2234            plan.shadow_delta_oracle
2235                .incremental_matches_from_scratch_delta
2236        );
2237        assert!(plan.shadow_delta_oracle.sampled_shadow_witness_ready);
2238        assert!(!plan.shadow_delta_oracle.dbsp_zset_claim_ready);
2239        assert!(!plan.shadow_delta_oracle.performance_benchmark_claim_ready);
2240    }
2241
2242    #[test]
2243    fn edit_distance_priority_orders_dirty_nodes_for_scheduler() {
2244        let previous = three_node_input("a:v1", "b:v1", "c:v1", 1);
2245        let previous_snapshot = snapshot_from_graph_input(&previous);
2246        let next = three_node_input("a:v2", "b:v2", "c:v1", 2);
2247        let plan = plan_from_database_with_priority_inputs(
2248            &next,
2249            Some(&previous_snapshot),
2250            &[
2251                priority_input("a", 1, 1, true),
2252                priority_input("b", 8, 2, true),
2253            ],
2254        );
2255
2256        assert_eq!(
2257            plan.invalidation_priority_plan.product,
2258            "omena-incremental.invalidation-priority-plan"
2259        );
2260        assert_eq!(
2261            plan.invalidation_priority_plan.feature_gate,
2262            "incremental-edit-distance-priority-v0"
2263        );
2264        assert_eq!(
2265            plan.invalidation_priority_plan.calibration_stage,
2266            "fixtureWitnessDistanceMarginWeightedV0"
2267        );
2268        assert!(!plan.invalidation_priority_plan.theorem_claimed);
2269        assert!(!plan.invalidation_priority_plan.public_safety_claim_ready);
2270        assert_eq!(plan.invalidation_priority_plan.metric_input_count, 2);
2271        assert_eq!(plan.invalidation_priority_plan.metric_consumed_count, 2);
2272        assert_eq!(
2273            plan.invalidation_priority_plan.prioritized_dirty_node_ids,
2274            vec!["b".to_string(), "a".to_string(), "c".to_string()]
2275        );
2276        let first = &plan.invalidation_priority_plan.entries[0];
2277        assert_eq!(first.node_id, "b");
2278        assert_eq!(first.priority_rank, 1);
2279        assert!(first.metric_consumed);
2280        assert_eq!(first.edit_distance_total, Some(8));
2281        assert_eq!(first.cascade_margin_abs_distance, Some(2));
2282        assert!(first.bridge_checked);
2283    }
2284
2285    #[test]
2286    fn datalog_rule_evaluator_contract_matches_incremental_dirty_plan() {
2287        let input = sample_input("a:v1", "b:v1", 1);
2288        let snapshot = snapshot_from_graph_input(&input);
2289        let next_input = sample_input("a:v2", "b:v1", 2);
2290        let summary = summarize_datalog_rule_evaluator_v0(&next_input, Some(&snapshot));
2291
2292        assert_eq!(summary.schema_version, "0");
2293        assert_eq!(summary.product, "omena-incremental.datalog-rule-evaluator");
2294        assert_eq!(summary.evaluator_kind, "typedContractOverSalsaDemandPlan");
2295        assert_eq!(
2296            summary.substrate,
2297            "omena-incremental.salsa-backed-computation-plan"
2298        );
2299        assert!(!summary.external_host_ready);
2300        assert_eq!(summary.rule_count, summary.rules.len());
2301        assert_eq!(summary.relation_count, summary.relations.len());
2302        assert_eq!(summary.input_node_count, 2);
2303        assert_eq!(summary.dirty_node_count, 2);
2304        assert_eq!(summary.derived_node_count, 1);
2305        assert_eq!(summary.iteration_limit, 3);
2306        assert!(summary.fixed_point_reached);
2307        assert_eq!(summary.incremental_plan.changed_input_count, 1);
2308        assert_eq!(summary.incremental_plan.dependency_dirty_count, 1);
2309        assert!(summary.rules.iter().any(|rule| {
2310            rule.name == "dependencyDirtyDemandRead"
2311                && rule.body == vec!["dependsOn(Node,Dependency)", "dirty(Dependency)"]
2312        }));
2313    }
2314
2315    #[test]
2316    fn datalog_rule_evaluator_fixture_corpus_matches_incremental_fixed_point() {
2317        for seed in [1, 2, 3, 5, 8, 13, 21, 34] {
2318            let previous_input = super::generated_incremental_fuzz_graph(seed, 8, None);
2319            let previous_snapshot = snapshot_from_graph_input(&previous_input);
2320            let next_input = super::generated_incremental_fuzz_graph(seed, 8, Some(3));
2321            let plan = plan_from_database(&next_input, Some(&previous_snapshot));
2322            let summary =
2323                summarize_datalog_rule_evaluator_v0(&next_input, Some(&previous_snapshot));
2324
2325            assert_eq!(summary.incremental_plan, plan);
2326            assert_eq!(summary.dirty_node_count, plan.dirty_node_count);
2327            assert_eq!(summary.derived_node_count, plan.dependency_dirty_count);
2328            assert!(summary.fixed_point_reached);
2329            assert!(!summary.external_host_ready);
2330            assert_eq!(summary.rule_count, 4);
2331            assert_eq!(summary.relation_count, 5);
2332        }
2333    }
2334
2335    #[test]
2336    fn cyclic_dependency_graph_uses_bounded_dirty_propagation() {
2337        let input = cyclic_input("a:v1", "b:v1", 1);
2338        let snapshot = snapshot_from_graph_input(&input);
2339        let next_input = cyclic_input("a:v2", "b:v1", 2);
2340        let plan = plan_from_database(&next_input, Some(&snapshot));
2341
2342        assert_eq!(plan.changed_input_count, 1);
2343        assert_eq!(plan.dirty_node_count, 2);
2344        assert_eq!(node_reasons(&plan, "a"), vec!["inputDigestChanged"]);
2345        assert_eq!(node_reasons(&plan, "b"), vec!["dependencyDirty"]);
2346        assert_eq!(
2347            super::dependency_propagation_iteration_limit(input.nodes.len()),
2348            input.nodes.len() + 1
2349        );
2350    }
2351
2352    #[test]
2353    fn fuzz_seed_corpus_preserves_incremental_dirty_set_invariants() {
2354        let report = super::run_incremental_fuzz_seed_corpus();
2355
2356        assert_eq!(report.product, "omena-incremental.fuzz-seed-corpus");
2357        assert_eq!(report.failed_count, 0);
2358        assert_eq!(report.passed_count, report.case_count);
2359        assert!(
2360            report
2361                .results
2362                .iter()
2363                .any(|result| result.changed_node_id.is_none())
2364        );
2365        assert!(
2366            report
2367                .results
2368                .iter()
2369                .any(|result| result.expected_dirty_node_count > 1)
2370        );
2371    }
2372
2373    #[test]
2374    fn m6_incremental_layer_evidence_is_limited_to_real_invalidation_layer() {
2375        let evidence = summarize_incremental_layer_evidence_v0();
2376
2377        assert_eq!(evidence.schema_version, "0");
2378        assert_eq!(evidence.product, "omena-incremental.layer-evidence");
2379        assert_eq!(evidence.claim_level, "m6IncrementalLayerEvidenceOnly");
2380        assert_eq!(
2381            evidence.invalidation_layer,
2382            "stableNodeIdDigestDependencyGraph"
2383        );
2384        assert!(evidence.real_invalidation_evidence_ready);
2385        assert!(evidence.fuzz_evidence_ready);
2386        assert!(evidence.salsa_reuse_evidence_ready);
2387        assert!(evidence.datalog_contract_evidence_ready);
2388        assert!(evidence.value_equality_backdating_ready);
2389        assert!(evidence.alpha_equivalence_hash_ready);
2390        assert!(evidence.shadow_delta_oracle_ready);
2391        assert!(evidence.edit_distance_priority_ready);
2392        assert!(evidence.benchmark_surface_ready);
2393        assert!(!evidence.performance_benchmark_claim_ready);
2394        assert!(!evidence.external_datalog_host_ready);
2395        assert!(!evidence.dbsp_zset_claim_ready);
2396        assert!(!evidence.public_safety_claim_ready);
2397        assert_eq!(
2398            evidence.benchmark_gate,
2399            "rust/z5-performance-baseline-readiness"
2400        );
2401        assert_eq!(evidence.fuzz_report.failed_count, 0);
2402        assert_eq!(
2403            evidence.sample_update.incremental_plan.changed_input_count,
2404            1
2405        );
2406        assert_eq!(
2407            evidence
2408                .sample_update
2409                .incremental_plan
2410                .dependency_dirty_count,
2411            1
2412        );
2413        assert!(
2414            evidence
2415                .supported_claims
2416                .contains(&"dependency dirty-set fixed point")
2417        );
2418        assert!(
2419            evidence
2420                .supported_claims
2421                .contains(&"value-equality backdating with changed_at/verified_at split")
2422        );
2423        assert!(
2424            evidence
2425                .supported_claims
2426                .contains(&"edit-distance weighted invalidation priority")
2427        );
2428        assert!(evidence.deferred_claims.contains(&"DBSP runtime"));
2429        assert!(
2430            evidence
2431                .deferred_claims
2432                .contains(&"Z-set differential dataflow semantics")
2433        );
2434    }
2435
2436    #[test]
2437    fn incremental_claim_levels_round_trip_to_guarantee_kinds() {
2438        let evidence = summarize_incremental_layer_evidence_v0();
2439        let plan = &evidence.sample_update.incremental_plan;
2440        let priority_input = priority_input("style", 3, 2, true);
2441
2442        for claim_level in [
2443            evidence.claim_level,
2444            plan.alpha_equivalence_graph_hash.claim_level,
2445            plan.shadow_delta_oracle.claim_level,
2446            plan.invalidation_priority_plan.claim_level,
2447            priority_input.claim_level,
2448        ] {
2449            assert_eq!(
2450                GuaranteeKindV0::from_existing_label(claim_level)
2451                    .and_then(GuaranteeKindV0::existing_label),
2452                Some(claim_level)
2453            );
2454        }
2455    }
2456
2457    #[test]
2458    fn incremental_layer_evidence_graph_preserves_public_shape() -> Result<(), String> {
2459        let evidence = summarize_incremental_layer_evidence_v0();
2460        let before = serde_json::to_value(&evidence).map_err(|error| error.to_string())?;
2461        let graph = evidence
2462            .evidence_graph()
2463            .map_err(|error| format!("{error:?}"))?;
2464        let after = serde_json::to_value(&evidence).map_err(|error| error.to_string())?;
2465
2466        assert_eq!(before, after);
2467        assert_eq!(graph.nodes.len(), 4);
2468        assert_eq!(graph.edges.len(), 4);
2469        let labels = graph
2470            .nodes
2471            .iter()
2472            .map(|node| node.guarantee.existing_label())
2473            .collect::<Vec<_>>();
2474        assert!(labels.contains(&Some("m6IncrementalLayerEvidenceOnly")));
2475        assert!(labels.contains(&Some("fixtureWitnessAlphaRenamingStableHash")));
2476        assert!(labels.contains(&Some("sampledFixtureWitnessNotEquivalenceProof")));
2477        assert!(labels.contains(&Some("fixtureWitnessSchedulerPriority")));
2478        assert!(
2479            graph
2480                .nodes
2481                .iter()
2482                .all(|node| node.earned_via() == GuaranteeFamilyV0::TypedInvariantWitness)
2483        );
2484        Ok(())
2485    }
2486
2487    #[test]
2488    fn salsa_database_reuses_digest_query_when_only_dependencies_change() {
2489        let session = InstrumentationSessionV0::default();
2490        with_instrumentation_session(session.clone(), || {
2491            session.reset_salsa_query_run_counts();
2492
2493            let mut db = OmenaIncrementalDatabaseV0::default();
2494            let input = IncrementalGraphInputV0 {
2495                revision: IncrementalRevisionV0 { value: 1 },
2496                nodes: vec![IncrementalNodeInputV0 {
2497                    id: "a".to_string(),
2498                    digest: "a:v1".to_string(),
2499                    dependency_ids: Vec::new(),
2500                }],
2501            };
2502            let snapshot = db.upsert_graph_input(&input);
2503            assert_eq!(snapshot.product, "omena-incremental.salsa-snapshot");
2504
2505            let Some(node) = db.node_input("a") else {
2506                return;
2507            };
2508            assert_eq!(
2509                read_salsa_incremental_node_digest(db.salsa_database(), node),
2510                "a:v1"
2511            );
2512            assert_eq!(
2513                read_salsa_incremental_node_dependency_ids(db.salsa_database(), node),
2514                Vec::<String>::new()
2515            );
2516            let counts = session.salsa_query_run_counts();
2517            assert_eq!(counts.digest, 1);
2518            assert_eq!(counts.dependency, 1);
2519
2520            let next_input = IncrementalGraphInputV0 {
2521                revision: IncrementalRevisionV0 { value: 2 },
2522                nodes: vec![IncrementalNodeInputV0 {
2523                    id: "a".to_string(),
2524                    digest: "a:v1".to_string(),
2525                    dependency_ids: vec!["root".to_string()],
2526                }],
2527            };
2528            db.upsert_graph_input(&next_input);
2529
2530            let Some(node) = db.node_input("a") else {
2531                return;
2532            };
2533            assert_eq!(
2534                read_salsa_incremental_node_digest(db.salsa_database(), node),
2535                "a:v1"
2536            );
2537            assert_eq!(
2538                read_salsa_incremental_node_dependency_ids(db.salsa_database(), node),
2539                vec!["root".to_string()]
2540            );
2541            let counts = session.salsa_query_run_counts();
2542            assert_eq!(counts.digest, 1);
2543            assert_eq!(counts.dependency, 2);
2544        });
2545    }
2546
2547    #[test]
2548    fn salsa_transitive_query_graph_matches_planner_dirty_set() {
2549        let session = InstrumentationSessionV0::default();
2550        with_instrumentation_session(session.clone(), || {
2551            session.reset_salsa_query_run_counts();
2552
2553            let mut db = OmenaSalsaDatabaseV0::new();
2554            let a = SalsaIncrementalNodeInputV0::new(
2555                &db,
2556                "a".to_string(),
2557                "a:v1".to_string(),
2558                Vec::new(),
2559            );
2560            let b = SalsaIncrementalNodeInputV0::new(
2561                &db,
2562                "b".to_string(),
2563                "b:v1".to_string(),
2564                vec!["a".to_string()],
2565            );
2566            let c = SalsaIncrementalNodeInputV0::new(
2567                &db,
2568                "c".to_string(),
2569                "c:v1".to_string(),
2570                vec!["b".to_string()],
2571            );
2572            let unrelated = SalsaIncrementalNodeInputV0::new(
2573                &db,
2574                "unrelated".to_string(),
2575                "u:v1".to_string(),
2576                Vec::new(),
2577            );
2578
2579            assert_eq!(
2580                read_salsa_transitive_c(&db, a, b, c),
2581                "a=a:v1|b=b:v1|c=c:v1"
2582            );
2583            assert_eq!(read_salsa_transitive_unrelated(&db, unrelated), "u=u:v1");
2584
2585            session.reset_salsa_query_run_counts();
2586
2587            a.set_digest(&mut db).to("a:v2".to_string());
2588
2589            assert_eq!(
2590                read_salsa_transitive_c(&db, a, b, c),
2591                "a=a:v2|b=b:v1|c=c:v1"
2592            );
2593            assert_eq!(read_salsa_transitive_unrelated(&db, unrelated), "u=u:v1");
2594
2595            let counts = session.salsa_query_run_counts();
2596            assert_eq!(counts.transitive_leaf, 1);
2597            assert_eq!(counts.transitive_a, 1);
2598            assert_eq!(counts.transitive_b, 1);
2599            assert_eq!(counts.transitive_c, 1);
2600            assert_eq!(counts.transitive_unrelated, 0);
2601
2602            let previous = IncrementalGraphInputV0 {
2603                revision: IncrementalRevisionV0 { value: 1 },
2604                nodes: vec![
2605                    IncrementalNodeInputV0 {
2606                        id: "a".to_string(),
2607                        digest: "a:v1".to_string(),
2608                        dependency_ids: Vec::new(),
2609                    },
2610                    IncrementalNodeInputV0 {
2611                        id: "b".to_string(),
2612                        digest: "b:v1".to_string(),
2613                        dependency_ids: vec!["a".to_string()],
2614                    },
2615                    IncrementalNodeInputV0 {
2616                        id: "c".to_string(),
2617                        digest: "c:v1".to_string(),
2618                        dependency_ids: vec!["b".to_string()],
2619                    },
2620                    IncrementalNodeInputV0 {
2621                        id: "unrelated".to_string(),
2622                        digest: "u:v1".to_string(),
2623                        dependency_ids: Vec::new(),
2624                    },
2625                ],
2626            };
2627            let next = IncrementalGraphInputV0 {
2628                revision: IncrementalRevisionV0 { value: 2 },
2629                nodes: vec![
2630                    IncrementalNodeInputV0 {
2631                        id: "a".to_string(),
2632                        digest: "a:v2".to_string(),
2633                        dependency_ids: Vec::new(),
2634                    },
2635                    IncrementalNodeInputV0 {
2636                        id: "b".to_string(),
2637                        digest: "b:v1".to_string(),
2638                        dependency_ids: vec!["a".to_string()],
2639                    },
2640                    IncrementalNodeInputV0 {
2641                        id: "c".to_string(),
2642                        digest: "c:v1".to_string(),
2643                        dependency_ids: vec!["b".to_string()],
2644                    },
2645                    IncrementalNodeInputV0 {
2646                        id: "unrelated".to_string(),
2647                        digest: "u:v1".to_string(),
2648                        dependency_ids: Vec::new(),
2649                    },
2650                ],
2651            };
2652            let previous_snapshot = snapshot_from_graph_input(&previous);
2653            let plan = plan_from_database(&next, Some(&previous_snapshot));
2654            let planner_dirty_ids = plan
2655                .nodes
2656                .iter()
2657                .filter(|node| node.dirty)
2658                .map(|node| node.id.as_str())
2659                .collect::<BTreeSet<_>>();
2660            let salsa_rerun_ids = ["a", "b", "c"].into_iter().collect::<BTreeSet<_>>();
2661
2662            assert_eq!(planner_dirty_ids, salsa_rerun_ids);
2663        });
2664    }
2665
2666    #[test]
2667    fn production_node_value_query_reads_only_transitive_dependencies() {
2668        let mut db = OmenaIncrementalDatabaseV0::default();
2669        let input = IncrementalGraphInputV0 {
2670            revision: IncrementalRevisionV0 { value: 1 },
2671            nodes: vec![
2672                IncrementalNodeInputV0 {
2673                    id: "a".to_string(),
2674                    digest: "a:v1".to_string(),
2675                    dependency_ids: Vec::new(),
2676                },
2677                IncrementalNodeInputV0 {
2678                    id: "b".to_string(),
2679                    digest: "b:v1".to_string(),
2680                    dependency_ids: vec!["a".to_string()],
2681                },
2682                IncrementalNodeInputV0 {
2683                    id: "c".to_string(),
2684                    digest: "c:v1".to_string(),
2685                    dependency_ids: vec!["b".to_string()],
2686                },
2687                IncrementalNodeInputV0 {
2688                    id: "unrelated".to_string(),
2689                    digest: "u:v1".to_string(),
2690                    dependency_ids: Vec::new(),
2691                },
2692            ],
2693        };
2694        db.upsert_graph_input(&input);
2695
2696        assert_eq!(
2697            db.node_value("c"),
2698            Some("c=c:v1;deps=[b=b:v1;deps=[a=a:v1;deps=[]]]".to_string())
2699        );
2700        assert_eq!(
2701            db.node_value("unrelated"),
2702            Some("unrelated=u:v1;deps=[]".to_string())
2703        );
2704
2705        reset_salsa_node_value_query_runs();
2706        let next = IncrementalGraphInputV0 {
2707            revision: IncrementalRevisionV0 { value: 2 },
2708            nodes: vec![
2709                IncrementalNodeInputV0 {
2710                    id: "a".to_string(),
2711                    digest: "a:v2".to_string(),
2712                    dependency_ids: Vec::new(),
2713                },
2714                IncrementalNodeInputV0 {
2715                    id: "b".to_string(),
2716                    digest: "b:v1".to_string(),
2717                    dependency_ids: vec!["a".to_string()],
2718                },
2719                IncrementalNodeInputV0 {
2720                    id: "c".to_string(),
2721                    digest: "c:v1".to_string(),
2722                    dependency_ids: vec!["b".to_string()],
2723                },
2724                IncrementalNodeInputV0 {
2725                    id: "unrelated".to_string(),
2726                    digest: "u:v1".to_string(),
2727                    dependency_ids: Vec::new(),
2728                },
2729            ],
2730        };
2731        db.upsert_graph_input(&next);
2732
2733        assert_eq!(
2734            db.node_value("c"),
2735            Some("c=c:v1;deps=[b=b:v1;deps=[a=a:v2;deps=[]]]".to_string())
2736        );
2737        assert_eq!(
2738            db.node_value("unrelated"),
2739            Some("unrelated=u:v1;deps=[]".to_string())
2740        );
2741        assert_eq!(salsa_node_value_query_runs("a"), 1);
2742        assert_eq!(salsa_node_value_query_runs("b"), 1);
2743        assert_eq!(salsa_node_value_query_runs("c"), 1);
2744        assert_eq!(salsa_node_value_query_runs("unrelated"), 0);
2745    }
2746
2747    #[test]
2748    fn salsa_database_update_owns_plan_and_snapshot_progression() {
2749        let mut db = OmenaIncrementalDatabaseV0::default();
2750        let input = sample_input("a:v1", "b:v1", 1);
2751        let first = db.plan_and_upsert_graph_input(&input);
2752
2753        assert_eq!(first.product, "omena-incremental.salsa-database-update");
2754        assert_eq!(first.incremental_plan.dirty_node_count, 2);
2755        assert_eq!(
2756            first.next_snapshot.product,
2757            "omena-incremental.salsa-snapshot"
2758        );
2759        assert!(db.current_snapshot().is_some());
2760
2761        let unchanged = db.plan_and_upsert_graph_input(&sample_input("a:v1", "b:v1", 2));
2762        assert_eq!(unchanged.incremental_plan.dirty_node_count, 0);
2763
2764        let changed = db.plan_and_upsert_graph_input(&sample_input("a:v2", "b:v1", 3));
2765        assert_eq!(changed.incremental_plan.changed_input_count, 1);
2766        assert_eq!(changed.incremental_plan.dependency_dirty_count, 1);
2767        assert_eq!(changed.datalog_rule_evaluator.revision.value, 3);
2768        assert_eq!(
2769            changed.datalog_rule_evaluator.incremental_plan,
2770            changed.incremental_plan
2771        );
2772        assert_eq!(changed.datalog_rule_evaluator.dirty_node_count, 2);
2773        assert_eq!(changed.datalog_rule_evaluator.derived_node_count, 1);
2774        assert!(changed.datalog_rule_evaluator.fixed_point_reached);
2775        assert!(!changed.datalog_rule_evaluator.external_host_ready);
2776    }
2777
2778    #[test]
2779    fn cancellation_registry_tracks_and_consumes_request_ids() {
2780        let mut registry = IncrementalCancellationRegistryV0::with_limit(4);
2781
2782        registry.cancel("s:hover-1");
2783
2784        assert_eq!(registry.len(), 1);
2785        assert!(matches!(
2786            registry.take_cancelled_result("s:hover-1"),
2787            Err(salsa::Cancelled::Local)
2788        ));
2789        assert!(matches!(
2790            registry.take_cancelled_result("s:hover-1"),
2791            Ok(())
2792        ));
2793        assert!(registry.is_empty());
2794    }
2795
2796    #[test]
2797    fn cancellation_registry_bounds_stale_cancelled_requests() {
2798        let mut registry = IncrementalCancellationRegistryV0::with_limit(2);
2799
2800        registry.cancel("n:1");
2801        registry.cancel("n:2");
2802        registry.cancel("n:3");
2803
2804        let snapshot = registry.snapshot();
2805        assert_eq!(snapshot.product, "omena-incremental.cancellation-registry");
2806        assert_eq!(snapshot.cancelled_request_ids, vec!["n:3"]);
2807    }
2808
2809    fn sample_input(a_digest: &str, b_digest: &str, revision: u64) -> IncrementalGraphInputV0 {
2810        IncrementalGraphInputV0 {
2811            revision: IncrementalRevisionV0 { value: revision },
2812            nodes: vec![
2813                IncrementalNodeInputV0 {
2814                    id: "b".to_string(),
2815                    digest: b_digest.to_string(),
2816                    dependency_ids: vec!["a".to_string()],
2817                },
2818                IncrementalNodeInputV0 {
2819                    id: "a".to_string(),
2820                    digest: a_digest.to_string(),
2821                    dependency_ids: Vec::new(),
2822                },
2823            ],
2824        }
2825    }
2826
2827    fn cyclic_input(a_digest: &str, b_digest: &str, revision: u64) -> IncrementalGraphInputV0 {
2828        IncrementalGraphInputV0 {
2829            revision: IncrementalRevisionV0 { value: revision },
2830            nodes: vec![
2831                IncrementalNodeInputV0 {
2832                    id: "a".to_string(),
2833                    digest: a_digest.to_string(),
2834                    dependency_ids: vec!["b".to_string()],
2835                },
2836                IncrementalNodeInputV0 {
2837                    id: "b".to_string(),
2838                    digest: b_digest.to_string(),
2839                    dependency_ids: vec!["a".to_string()],
2840                },
2841            ],
2842        }
2843    }
2844
2845    fn three_node_input(
2846        a_digest: &str,
2847        b_digest: &str,
2848        c_digest: &str,
2849        revision: u64,
2850    ) -> IncrementalGraphInputV0 {
2851        IncrementalGraphInputV0 {
2852            revision: IncrementalRevisionV0 { value: revision },
2853            nodes: vec![
2854                IncrementalNodeInputV0 {
2855                    id: "a".to_string(),
2856                    digest: a_digest.to_string(),
2857                    dependency_ids: Vec::new(),
2858                },
2859                IncrementalNodeInputV0 {
2860                    id: "b".to_string(),
2861                    digest: b_digest.to_string(),
2862                    dependency_ids: Vec::new(),
2863                },
2864                IncrementalNodeInputV0 {
2865                    id: "c".to_string(),
2866                    digest: c_digest.to_string(),
2867                    dependency_ids: vec!["a".to_string()],
2868                },
2869            ],
2870        }
2871    }
2872
2873    fn priority_input(
2874        node_id: &str,
2875        edit_distance_total: usize,
2876        cascade_margin_abs_distance: u64,
2877        bridge_checked: bool,
2878    ) -> super::IncrementalEditDistancePriorityInputV0 {
2879        super::IncrementalEditDistancePriorityInputV0 {
2880            schema_version: "0",
2881            product: "omena-incremental.edit-distance-priority-input",
2882            feature_gate: "incremental-edit-distance-priority-v0",
2883            claim_level: "fixtureWitnessMetricInput",
2884            theorem_claimed: false,
2885            node_id: node_id.to_string(),
2886            edit_distance_total,
2887            cascade_margin_abs_distance,
2888            bridge_checked,
2889            bridge_calibration_stage: "fixtureWitnessOnlyUncalibrated",
2890        }
2891    }
2892
2893    fn node_by_id<'a>(
2894        plan: &'a super::IncrementalComputationPlanV0,
2895        id: &str,
2896    ) -> Option<&'a super::IncrementalComputationNodeV0> {
2897        plan.nodes.iter().find(|node| node.id == id)
2898    }
2899
2900    fn node_reasons(plan: &super::IncrementalComputationPlanV0, id: &str) -> Vec<&'static str> {
2901        plan.nodes
2902            .iter()
2903            .find(|node| node.id == id)
2904            .map(|node| node.reasons.clone())
2905            .unwrap_or_default()
2906    }
2907
2908    fn plan_from_database(
2909        input: &IncrementalGraphInputV0,
2910        previous: Option<&super::IncrementalSnapshotV0>,
2911    ) -> super::IncrementalComputationPlanV0 {
2912        plan_from_database_with_priority_inputs(input, previous, &[])
2913    }
2914
2915    fn plan_from_database_with_priority_inputs(
2916        input: &IncrementalGraphInputV0,
2917        previous: Option<&super::IncrementalSnapshotV0>,
2918        priority_inputs: &[super::IncrementalEditDistancePriorityInputV0],
2919    ) -> super::IncrementalComputationPlanV0 {
2920        let mut database = OmenaIncrementalDatabaseV0::default();
2921        if let Some(previous) = previous {
2922            database.restore_snapshot(previous);
2923        }
2924        database
2925            .plan_and_upsert_graph_input_with_priority_inputs(input, priority_inputs)
2926            .incremental_plan
2927    }
2928}