xlog_ir/
epistemic_plan.rs

1//! GPU-native epistemic execution planning contracts.
2
3use std::collections::{BTreeMap, BTreeSet};
4
5use xlog_core::RelId;
6
7use crate::eir::{EirEpistemicLiteral, EirEpistemicMode, EirEpistemicOp, EirTerm};
8use crate::plan::ExecutionPlan;
9
10/// Generate-Propagate-Test hot-path phase that must execute on GPU.
11#[derive(Debug, Clone, Copy, PartialEq, Eq)]
12pub enum EpistemicGpuHotPathPhase {
13    /// Candidate epistemic assumptions are generated on device.
14    CandidateGeneration,
15    /// Candidate assumptions are propagated into reduced programs on device.
16    Propagation,
17    /// Candidate bitsets are validated on device before production dispatch.
18    CandidateValidation,
19    /// Stable-model tuple membership is populated on device.
20    ModelMembership,
21    /// Reduced-program stable models are checked against world-view guesses on device.
22    WorldViewValidation,
23    /// Accepted world views and query results are materialized from device buffers.
24    ResultMaterialization,
25    /// Final result flags are materialized from device-side output metadata.
26    FinalResultMaterialization,
27    /// Final query tuples are materialized into a device-resident output buffer.
28    FinalTupleMaterialization,
29}
30
31/// GPU-resident buffer category required by accepted epistemic execution.
32#[derive(Debug, Clone, Copy, PartialEq, Eq)]
33pub enum EpistemicGpuBufferKind {
34    /// Candidate assumption bitsets.
35    CandidateAssumptions,
36    /// Accepted and candidate world-view bitsets.
37    WorldViews,
38    /// Per-model membership checks used by `know` and `possible`.
39    ModelMembership,
40    /// Structured rejection reasons for failed candidates.
41    RejectionReasons,
42}
43
44/// WCOJ status for a reduced ordinary program.
45#[derive(Debug, Clone, Copy, PartialEq, Eq)]
46pub enum EpistemicWcojReductionStatus {
47    /// The reduced body is too small or otherwise not a WCOJ candidate.
48    NotWcojCandidate,
49    /// The reduced body must be submitted to the production WCOJ planner.
50    RequiresPlannerEligibility,
51}
52
53/// CPU fallback counters that must remain zero on the accepted hot path.
54#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
55pub struct EpistemicCpuFallbackCounters {
56    /// CPU candidate enumeration count.
57    pub candidate_enumeration: u64,
58    /// CPU world-view validation count.
59    pub world_view_validation: u64,
60    /// CPU SAT/MaxSAT search count.
61    pub solver_search: u64,
62    /// CPU-only probabilistic recomputation count.
63    pub probabilistic_recompute: u64,
64}
65
66impl EpistemicCpuFallbackCounters {
67    /// Return true when every forbidden CPU fallback counter is zero.
68    pub fn is_zero(&self) -> bool {
69        self.candidate_enumeration == 0
70            && self.world_view_validation == 0
71            && self.solver_search == 0
72            && self.probabilistic_recompute == 0
73    }
74}
75
76/// One epistemic rule's reduced ordinary-program planning summary.
77#[derive(Debug, Clone, PartialEq, Eq)]
78pub struct EpistemicReductionPlan {
79    /// Source-order rule index.
80    pub rule_index: usize,
81    /// Head predicate materialized by the reduced production runtime plan.
82    pub head_predicate: String,
83    /// PUBLIC head arity (the user-visible head term count, before any augmentation
84    /// with modal-literal variables). The reduced relation buffer may carry extra
85    /// augmented columns appended after these; per-head materialization projects the
86    /// first `public_head_arity` columns so each coupled head keeps ITS OWN projection
87    /// (coupled heads of differing arity all materialize their own public tuple shape).
88    pub public_head_arity: usize,
89    /// Positive relational body atom count after removing epistemic literals.
90    pub relational_body_atoms: usize,
91    /// WCOJ planner status for the reduced ordinary body.
92    pub wcoj_status: EpistemicWcojReductionStatus,
93}
94
95/// Binding from an epistemic literal to reduced stable-model tuple evidence.
96#[derive(Debug, Clone, PartialEq, Eq)]
97pub struct EpistemicTupleMembershipBinding {
98    /// Index of the epistemic literal in `EpistemicGpuPlan::epistemic_literals`.
99    pub literal_index: usize,
100    /// Index of the reduced rule in `EpistemicGpuPlan::reductions`.
101    pub reduction_index: usize,
102    /// Predicate whose stable-model tuples must be checked.
103    pub predicate: String,
104    /// Predicate arity whose stable-model tuples must be checked.
105    pub arity: usize,
106    /// Source relation columns that form the tuple key for this epistemic atom.
107    pub key_columns: Vec<usize>,
108    /// Source atom terms that must be matched against the stable-model tuple key.
109    pub key_terms: Vec<EirTerm>,
110    /// Reduced output column for each variable tuple-key term.
111    ///
112    /// Ground terms use `None`; variable terms use `Some(column_index)`.
113    pub bound_output_columns: Vec<Option<usize>>,
114    /// Epistemic operator whose membership semantics are being checked.
115    pub op: EirEpistemicOp,
116    /// Whether the epistemic literal is explicitly negated.
117    pub negated: bool,
118}
119
120/// World-view integrity constraint lowered for accepted GPU execution.
121///
122/// An epistemic integrity constraint (`:- know unsafe().`) must reject a
123/// candidate world view when the conjunction of its body literals evaluates
124/// true under the selected epistemic semantics. Each body epistemic literal is
125/// kept first-class as an [`EpistemicGpuPlan::epistemic_literals`] entry; this
126/// plan only records which literal indices form the constraint conjunction so
127/// the device constraint kernel can prune candidates whose accepted world view
128/// satisfies the constraint body.
129#[derive(Debug, Clone, PartialEq, Eq)]
130pub struct EpistemicConstraintPlan {
131    /// Source-order constraint index.
132    pub constraint_index: usize,
133    /// Indices into [`EpistemicGpuPlan::epistemic_literals`] forming the body conjunction.
134    ///
135    /// The accepted world view violates the constraint exactly when every
136    /// referenced literal's negation-folded modal value holds, so the device
137    /// kernel rejects a candidate when all of these literal assumption bits are set.
138    pub literal_indices: Vec<usize>,
139}
140
141/// Solver production capability required by accepted epistemic execution.
142#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
143pub enum EpistemicSolverCapability {
144    /// Incremental SAT solve calls with pushed assumptions.
145    IncrementalSat,
146    /// Explicit push, solve, retract assumption lifecycle.
147    AssumptionLifecycle,
148    /// Learned-clause publication and reuse across valid incremental calls.
149    LearnedClauseTransfer,
150    /// Weighted MaxSAT soft-constraint solving.
151    WeightedMaxSat,
152    /// GPU-backed SAT/MaxSAT portfolio dispatch.
153    PortfolioSatMaxSat,
154}
155
156/// Solver status kind that must cross the epistemic boundary distinctly.
157#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
158pub enum EpistemicSolverStatusKind {
159    /// Satisfiable solver result.
160    Sat,
161    /// Unsatisfiable solver result.
162    Unsat,
163    /// Inconclusive solver result.
164    Unknown,
165    /// Budget-exhausted solver result.
166    Timeout,
167}
168
169/// Binding from an epistemic literal to a solver assumption obligation.
170#[derive(Debug, Clone, PartialEq, Eq)]
171pub struct EpistemicSolverAssumptionBinding {
172    /// Index of the epistemic literal in `EpistemicGpuPlan::epistemic_literals`.
173    pub literal_index: usize,
174    /// Index of the reduced rule in `EpistemicGpuPlan::reductions`.
175    pub reduction_index: usize,
176    /// Predicate whose epistemic truth becomes a solver assumption.
177    pub predicate: String,
178    /// Predicate arity for the solver assumption.
179    pub arity: usize,
180    /// Source atom terms that define the solver assumption key.
181    pub terms: Vec<EirTerm>,
182    /// Epistemic operator represented by the assumption.
183    pub op: EirEpistemicOp,
184    /// Whether the epistemic literal is explicitly negated.
185    pub negated: bool,
186}
187
188/// Solver-service contract exported from the epistemic semantic plan.
189#[derive(Debug, Clone, PartialEq, Eq)]
190pub struct EpistemicSolverServiceContract {
191    /// Per-literal solver assumptions that must be pushed and retracted.
192    pub assumption_bindings: Vec<EpistemicSolverAssumptionBinding>,
193    /// Production solver capabilities required before this plan can count as accepted.
194    pub required_capabilities: Vec<EpistemicSolverCapability>,
195    /// Solver statuses that must remain distinct across the interface.
196    pub required_statuses: Vec<EpistemicSolverStatusKind>,
197}
198
199impl EpistemicSolverServiceContract {
200    /// Build the v0.9 production solver contract for the provided assumptions.
201    pub fn production_default(assumption_bindings: Vec<EpistemicSolverAssumptionBinding>) -> Self {
202        Self {
203            assumption_bindings,
204            required_capabilities: vec![
205                EpistemicSolverCapability::IncrementalSat,
206                EpistemicSolverCapability::AssumptionLifecycle,
207                EpistemicSolverCapability::LearnedClauseTransfer,
208                EpistemicSolverCapability::WeightedMaxSat,
209                EpistemicSolverCapability::PortfolioSatMaxSat,
210            ],
211            required_statuses: vec![
212                EpistemicSolverStatusKind::Sat,
213                EpistemicSolverStatusKind::Unsat,
214                EpistemicSolverStatusKind::Unknown,
215                EpistemicSolverStatusKind::Timeout,
216            ],
217        }
218    }
219
220    /// Count distinct required solver capabilities.
221    pub fn distinct_required_capability_count(&self) -> usize {
222        self.required_capabilities
223            .iter()
224            .copied()
225            .collect::<BTreeSet<_>>()
226            .len()
227    }
228
229    /// Count distinct solver statuses that must cross the semantic boundary.
230    pub fn distinct_required_status_count(&self) -> usize {
231        self.required_statuses
232            .iter()
233            .copied()
234            .collect::<BTreeSet<_>>()
235            .len()
236    }
237}
238
239/// Production-facing GPU execution contract for an epistemic program.
240#[derive(Debug, Clone, PartialEq, Eq)]
241pub struct EpistemicGpuPlan {
242    /// Selected epistemic semantics mode.
243    pub mode: EirEpistemicMode,
244    /// Epistemic literals preserved from EIR.
245    pub epistemic_literals: Vec<EirEpistemicLiteral>,
246    /// Coarse Generate-Propagate-Test phases required by the hot path.
247    pub required_phases: Vec<EpistemicGpuHotPathPhase>,
248    /// Concrete GPU kernel phases required by accepted production execution.
249    pub required_kernel_phases: Vec<EpistemicGpuHotPathPhase>,
250    /// GPU buffer classes required by the hot path.
251    pub required_buffers: Vec<EpistemicGpuBufferKind>,
252    /// Reduced ordinary-program planning summaries.
253    pub reductions: Vec<EpistemicReductionPlan>,
254    /// Per-literal stable-model tuple membership bindings.
255    pub tuple_membership_bindings: Vec<EpistemicTupleMembershipBinding>,
256    /// World-view integrity constraints lowered for accepted GPU execution.
257    pub constraints: Vec<EpistemicConstraintPlan>,
258    /// Reduced-output columns copied into the public final output.
259    /// `None` means identity/all columns; `Some([])` is a real zero-arity projection.
260    pub final_output_columns: Option<Vec<usize>>,
261    /// Solver-service obligations exported by the epistemic semantic plan.
262    pub solver_contract: EpistemicSolverServiceContract,
263    /// Forbidden CPU fallback counters. Release certification must keep these zero.
264    pub cpu_fallbacks: EpistemicCpuFallbackCounters,
265}
266
267impl EpistemicGpuPlan {
268    /// Create a plan with the standard GPU hot-path phase and buffer requirements.
269    pub fn new(
270        mode: EirEpistemicMode,
271        epistemic_literals: Vec<EirEpistemicLiteral>,
272        reductions: Vec<EpistemicReductionPlan>,
273    ) -> Self {
274        let tuple_membership_bindings = epistemic_literals
275            .iter()
276            .enumerate()
277            .map(|(literal_index, literal)| EpistemicTupleMembershipBinding {
278                literal_index,
279                reduction_index: literal_index.min(reductions.len().saturating_sub(1)),
280                predicate: literal.atom.predicate.clone(),
281                arity: literal.atom.arity,
282                key_columns: (0..literal.atom.arity).collect(),
283                key_terms: literal.atom.terms.clone(),
284                bound_output_columns: vec![None; literal.atom.arity],
285                op: literal.op,
286                negated: literal.negated,
287            })
288            .collect();
289        let solver_assumption_bindings = epistemic_literals
290            .iter()
291            .enumerate()
292            .map(
293                |(literal_index, literal)| EpistemicSolverAssumptionBinding {
294                    literal_index,
295                    reduction_index: literal_index.min(reductions.len().saturating_sub(1)),
296                    predicate: literal.atom.predicate.clone(),
297                    arity: literal.atom.arity,
298                    terms: literal.atom.terms.clone(),
299                    op: literal.op,
300                    negated: literal.negated,
301                },
302            )
303            .collect();
304
305        Self {
306            mode,
307            epistemic_literals,
308            required_phases: vec![
309                EpistemicGpuHotPathPhase::CandidateGeneration,
310                EpistemicGpuHotPathPhase::Propagation,
311                EpistemicGpuHotPathPhase::WorldViewValidation,
312                EpistemicGpuHotPathPhase::ResultMaterialization,
313            ],
314            required_kernel_phases: vec![
315                EpistemicGpuHotPathPhase::CandidateGeneration,
316                EpistemicGpuHotPathPhase::Propagation,
317                EpistemicGpuHotPathPhase::CandidateValidation,
318                EpistemicGpuHotPathPhase::ModelMembership,
319                EpistemicGpuHotPathPhase::WorldViewValidation,
320                EpistemicGpuHotPathPhase::ResultMaterialization,
321                EpistemicGpuHotPathPhase::FinalResultMaterialization,
322                EpistemicGpuHotPathPhase::FinalTupleMaterialization,
323            ],
324            required_buffers: vec![
325                EpistemicGpuBufferKind::CandidateAssumptions,
326                EpistemicGpuBufferKind::WorldViews,
327                EpistemicGpuBufferKind::ModelMembership,
328                EpistemicGpuBufferKind::RejectionReasons,
329            ],
330            reductions,
331            tuple_membership_bindings,
332            constraints: Vec::new(),
333            final_output_columns: None,
334            solver_contract: EpistemicSolverServiceContract::production_default(
335                solver_assumption_bindings,
336            ),
337            cpu_fallbacks: EpistemicCpuFallbackCounters::default(),
338        }
339    }
340
341    /// Replace inferred tuple-membership bindings with planner-derived bindings.
342    pub fn with_tuple_membership_bindings(
343        mut self,
344        tuple_membership_bindings: Vec<EpistemicTupleMembershipBinding>,
345    ) -> Self {
346        self.tuple_membership_bindings = tuple_membership_bindings;
347        self
348    }
349
350    /// Attach world-view integrity constraints lowered for accepted GPU execution.
351    pub fn with_constraints(mut self, constraints: Vec<EpistemicConstraintPlan>) -> Self {
352        self.constraints = constraints;
353        self
354    }
355
356    /// Set the public projection applied after GPU tuple membership row filtering.
357    pub fn with_final_output_columns(mut self, final_output_columns: Option<Vec<usize>>) -> Self {
358        self.final_output_columns = final_output_columns;
359        self
360    }
361
362    /// Validate that every world-view constraint references in-range epistemic literals.
363    pub fn validate_constraints(&self) -> xlog_core::Result<()> {
364        for constraint in &self.constraints {
365            if constraint.literal_indices.is_empty() {
366                return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
367                    construct: "epistemic GPU world-view constraint".to_string(),
368                    context: format!(
369                        "constraint[{}] has no epistemic body literals; epistemic integrity \
370                         constraints must constrain accepted world views through at least one \
371                         know/possible literal",
372                        constraint.constraint_index
373                    ),
374                });
375            }
376            let mut seen = vec![false; self.epistemic_literals.len()];
377            for &literal_index in &constraint.literal_indices {
378                if literal_index >= self.epistemic_literals.len() {
379                    return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
380                        construct: "epistemic GPU world-view constraint".to_string(),
381                        context: format!(
382                            "constraint[{}] references literal_index {} exceeding literal count {}",
383                            constraint.constraint_index,
384                            literal_index,
385                            self.epistemic_literals.len()
386                        ),
387                    });
388                }
389                if seen[literal_index] {
390                    return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
391                        construct: "epistemic GPU world-view constraint".to_string(),
392                        context: format!(
393                            "constraint[{}] references literal_index {} more than once",
394                            constraint.constraint_index, literal_index
395                        ),
396                    });
397                }
398                seen[literal_index] = true;
399            }
400        }
401        Ok(())
402    }
403
404    /// Replace inferred solver obligations with planner-derived obligations.
405    pub fn with_solver_contract(mut self, solver_contract: EpistemicSolverServiceContract) -> Self {
406        self.solver_contract = solver_contract;
407        self
408    }
409
410    /// Validate that solver obligations match the epistemic semantic boundary.
411    pub fn validate_solver_contract(&self) -> xlog_core::Result<()> {
412        let contract = &self.solver_contract;
413        if contract.assumption_bindings.len() != self.epistemic_literals.len() {
414            return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
415                construct: "epistemic solver service contract".to_string(),
416                context: format!(
417                    "expected {} solver assumption bindings for epistemic literals, found {}",
418                    self.epistemic_literals.len(),
419                    contract.assumption_bindings.len()
420                ),
421            });
422        }
423
424        let distinct_capability_count = contract.distinct_required_capability_count();
425        if distinct_capability_count != contract.required_capabilities.len() {
426            return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
427                construct: "epistemic solver service contract".to_string(),
428                context: format!(
429                    "solver capability requirements must be distinct, got {} entries but {} distinct",
430                    contract.required_capabilities.len(),
431                    distinct_capability_count
432                ),
433            });
434        }
435
436        let distinct_status_count = contract.distinct_required_status_count();
437        if distinct_status_count != contract.required_statuses.len() {
438            return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
439                construct: "epistemic solver service contract".to_string(),
440                context: format!(
441                    "solver status requirements must be distinct, got {} entries but {} distinct",
442                    contract.required_statuses.len(),
443                    distinct_status_count
444                ),
445            });
446        }
447
448        for required in [
449            EpistemicSolverCapability::IncrementalSat,
450            EpistemicSolverCapability::AssumptionLifecycle,
451            EpistemicSolverCapability::LearnedClauseTransfer,
452            EpistemicSolverCapability::WeightedMaxSat,
453            EpistemicSolverCapability::PortfolioSatMaxSat,
454        ] {
455            if !contract.required_capabilities.contains(&required) {
456                return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
457                    construct: "epistemic solver service contract".to_string(),
458                    context: format!("missing required solver capability {required:?}"),
459                });
460            }
461        }
462
463        for required in [
464            EpistemicSolverStatusKind::Sat,
465            EpistemicSolverStatusKind::Unsat,
466            EpistemicSolverStatusKind::Unknown,
467            EpistemicSolverStatusKind::Timeout,
468        ] {
469            if !contract.required_statuses.contains(&required) {
470                return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
471                    construct: "epistemic solver service contract".to_string(),
472                    context: format!("missing required solver status {required:?}"),
473                });
474            }
475        }
476
477        let mut seen_literals = vec![false; self.epistemic_literals.len()];
478        for binding in &contract.assumption_bindings {
479            if binding.literal_index >= self.epistemic_literals.len() {
480                return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
481                    construct: "epistemic solver service contract".to_string(),
482                    context: format!(
483                        "literal_index {} exceeds literal count {}",
484                        binding.literal_index,
485                        self.epistemic_literals.len()
486                    ),
487                });
488            }
489            if seen_literals[binding.literal_index] {
490                return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
491                    construct: "epistemic solver service contract".to_string(),
492                    context: format!(
493                        "duplicate solver assumption for literal_index {}",
494                        binding.literal_index
495                    ),
496                });
497            }
498            seen_literals[binding.literal_index] = true;
499
500            if binding.reduction_index >= self.reductions.len() {
501                return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
502                    construct: "epistemic solver service contract".to_string(),
503                    context: format!(
504                        "reduction_index {} exceeds reduction count {}",
505                        binding.reduction_index,
506                        self.reductions.len()
507                    ),
508                });
509            }
510
511            let literal = &self.epistemic_literals[binding.literal_index];
512            let tuple_binding =
513                self.tuple_membership_bindings
514                    .iter()
515                    .find(|tuple_binding| tuple_binding.literal_index == binding.literal_index)
516                    .ok_or_else(|| {
517                        xlog_core::XlogError::UnsupportedEpistemicConstruct {
518                            construct: "epistemic solver service contract".to_string(),
519                            context: format!(
520                                "solver assumption for literal_index {} has no matching tuple-membership binding",
521                                binding.literal_index
522                            ),
523                        }
524                    })?;
525            if binding.reduction_index != tuple_binding.reduction_index {
526                return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
527                    construct: "epistemic solver service contract".to_string(),
528                    context: format!(
529                        "solver assumption for literal_index {} uses reduction_index {}, but tuple membership uses {}",
530                        binding.literal_index,
531                        binding.reduction_index,
532                        tuple_binding.reduction_index
533                    ),
534                });
535            }
536            if binding.predicate != literal.atom.predicate
537                || binding.arity != literal.atom.arity
538                || binding.terms != literal.atom.terms
539                || binding.op != literal.op
540                || binding.negated != literal.negated
541            {
542                return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
543                    construct: "epistemic solver service contract".to_string(),
544                    context: format!(
545                        "solver assumption for literal_index {} does not match epistemic literal",
546                        binding.literal_index
547                    ),
548                });
549            }
550        }
551
552        Ok(())
553    }
554
555    /// Validate that every epistemic literal has a matching tuple-membership binding.
556    pub fn validate_tuple_membership_bindings(&self) -> xlog_core::Result<()> {
557        if self.tuple_membership_bindings.len() != self.epistemic_literals.len() {
558            return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
559                construct: "epistemic GPU tuple membership binding".to_string(),
560                context: format!(
561                    "expected {} bindings for epistemic literals, found {}",
562                    self.epistemic_literals.len(),
563                    self.tuple_membership_bindings.len()
564                ),
565            });
566        }
567
568        let mut seen_literals = vec![false; self.epistemic_literals.len()];
569
570        for binding in &self.tuple_membership_bindings {
571            if binding.literal_index >= self.epistemic_literals.len() {
572                return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
573                    construct: "epistemic GPU tuple membership binding".to_string(),
574                    context: format!(
575                        "literal_index {} exceeds literal count {}",
576                        binding.literal_index,
577                        self.epistemic_literals.len()
578                    ),
579                });
580            }
581            if seen_literals[binding.literal_index] {
582                return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
583                    construct: "epistemic GPU tuple membership binding".to_string(),
584                    context: format!(
585                        "duplicate literal_index {} in tuple-membership bindings",
586                        binding.literal_index
587                    ),
588                });
589            }
590            seen_literals[binding.literal_index] = true;
591
592            if binding.reduction_index >= self.reductions.len() {
593                return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
594                    construct: "epistemic GPU tuple membership binding".to_string(),
595                    context: format!(
596                        "reduction_index {} exceeds reduction count {}",
597                        binding.reduction_index,
598                        self.reductions.len()
599                    ),
600                });
601            }
602
603            let literal = &self.epistemic_literals[binding.literal_index];
604            if binding.predicate != literal.atom.predicate
605                || binding.arity != literal.atom.arity
606                || binding.op != literal.op
607                || binding.negated != literal.negated
608            {
609                return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
610                    construct: "epistemic GPU tuple membership binding".to_string(),
611                    context: format!(
612                        "binding for literal_index {} does not match epistemic literal",
613                        binding.literal_index
614                    ),
615                });
616            }
617
618            if binding.key_columns.len() != binding.arity {
619                return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
620                    construct: "epistemic GPU tuple membership binding".to_string(),
621                    context: format!(
622                        "binding for literal_index {} has {} key columns for arity {}",
623                        binding.literal_index,
624                        binding.key_columns.len(),
625                        binding.arity
626                    ),
627                });
628            }
629
630            if binding.key_terms.len() != binding.arity {
631                return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
632                    construct: "epistemic GPU tuple membership binding".to_string(),
633                    context: format!(
634                        "binding for literal_index {} has {} key terms for arity {}",
635                        binding.literal_index,
636                        binding.key_terms.len(),
637                        binding.arity
638                    ),
639                });
640            }
641
642            if binding.key_terms != literal.atom.terms {
643                return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
644                    construct: "epistemic GPU tuple membership binding".to_string(),
645                    context: format!(
646                        "key terms for literal_index {} do not match epistemic literal",
647                        binding.literal_index
648                    ),
649                });
650            }
651
652            if binding.bound_output_columns.len() != binding.arity {
653                return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
654                    construct: "epistemic GPU tuple membership binding".to_string(),
655                    context: format!(
656                        "binding for literal_index {} has {} bound output columns for arity {}",
657                        binding.literal_index,
658                        binding.bound_output_columns.len(),
659                        binding.arity
660                    ),
661                });
662            }
663
664            for (term, bound_col) in binding
665                .key_terms
666                .iter()
667                .zip(binding.bound_output_columns.iter())
668            {
669                match (term, bound_col) {
670                    (EirTerm::Variable(_), Some(_)) => {}
671                    (EirTerm::Variable(variable), None) => {
672                        return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
673                            construct: "epistemic GPU tuple membership binding".to_string(),
674                            context: format!(
675                                "variable tuple key {variable} for literal_index {} is missing a \
676                                 reduced output column",
677                                binding.literal_index
678                            ),
679                        });
680                    }
681                    (_, None) => {}
682                    (_, Some(bound_col)) => {
683                        return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
684                            construct: "epistemic GPU tuple membership binding".to_string(),
685                            context: format!(
686                                "ground tuple key for literal_index {} unexpectedly binds \
687                                 reduced output column {}",
688                                binding.literal_index, bound_col
689                            ),
690                        });
691                    }
692                }
693            }
694
695            let mut seen_key_columns = vec![false; binding.arity];
696            for &key_col in &binding.key_columns {
697                if key_col >= binding.arity {
698                    return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
699                        construct: "epistemic GPU tuple membership binding".to_string(),
700                        context: format!(
701                            "key column {} exceeds arity {} for literal_index {}",
702                            key_col, binding.arity, binding.literal_index
703                        ),
704                    });
705                }
706                if seen_key_columns[key_col] {
707                    return Err(xlog_core::XlogError::UnsupportedEpistemicConstruct {
708                        construct: "epistemic GPU tuple membership binding".to_string(),
709                        context: format!(
710                            "duplicate key column {} for literal_index {}",
711                            key_col, binding.literal_index
712                        ),
713                    });
714                }
715                seen_key_columns[key_col] = true;
716            }
717        }
718
719        Ok(())
720    }
721}
722
723/// Production-facing executable plan for accepted epistemic lowering.
724#[derive(Debug, Clone)]
725pub struct EpistemicExecutablePlan {
726    /// GPU semantic contract for the epistemic hot path.
727    pub gpu_plan: EpistemicGpuPlan,
728    /// Predicate-to-relation ID map produced by the reduced production compiler.
729    pub relation_ids: BTreeMap<String, RelId>,
730    /// Ordinary reduced program compiled through the production runtime pipeline.
731    pub reduced_runtime_plan: ExecutionPlan,
732}
xlog_ir/epistemic_plan.rs

xlog_ir/
epistemic_plan.rs
