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

xlog_ir/
epistemic_plan.rs
