xlog_cuda/
semantic_program.rs

1//! Binary positive program data shared by cold source lowering and the resident evaluator.
2
3use crate::DeviceRepr;
4
5/// Native transition storage admits at most this many input facts per task.
6pub(crate) const RESIDENT_PROGRAM_FACT_CAPACITY: usize = 4096;
7/// The two sampled edits reserve two entries in this resident rule bank.
8const RESIDENT_PROGRAM_RULE_CAPACITY: usize = 256;
9
10/// One typed binary tuple. Predicate indices come from the admitted declaration order.
11#[repr(C)]
12#[derive(Clone, Copy, Debug, PartialEq, Eq)]
13pub struct SemanticProgramFact {
14    pub predicate: u32,
15    pub first: u32,
16    pub second: u32,
17}
18
19// SAFETY: the C layout has three u32 fields and no references or padding.
20unsafe impl DeviceRepr for SemanticProgramFact {}
21
22/// One range-restricted positive rule with one or two binary body atoms.
23/// Equal variable indices encode repeated-variable equalities.
24#[repr(C)]
25#[derive(Clone, Copy, Debug, PartialEq, Eq)]
26pub struct SemanticProgramRule {
27    pub head_predicate: u32,
28    pub left_predicate: u32,
29    pub right_predicate: u32,
30    pub body_count: u32,
31    pub head_variables: [u32; 2],
32    pub left_variables: [u32; 2],
33    pub right_variables: [u32; 2],
34}
35
36// SAFETY: the C layout has ten u32 fields and no references or padding.
37unsafe impl DeviceRepr for SemanticProgramRule {}
38
39/// Exact initial program and input facts prepared before a resident task starts.
40#[derive(Clone, Debug, PartialEq, Eq)]
41pub struct SemanticProgramAdmission {
42    pub predicate_count: u32,
43    pub initial_facts: Vec<SemanticProgramFact>,
44    pub initial_rules: Vec<SemanticProgramRule>,
45    pub queries: [SemanticProgramFact; 3],
46}
47
48impl SemanticProgramAdmission {
49    pub(crate) fn validate(&self) -> Result<(), &'static str> {
50        if self.predicate_count == 0
51            || self.initial_facts.len() > u32::MAX as usize
52            || self.initial_rules.len() > u32::MAX as usize
53            || self
54                .queries
55                .iter()
56                .chain(&self.initial_facts)
57                .any(|fact| fact.predicate >= self.predicate_count)
58        {
59            return Err("binary program has an invalid predicate or fact count");
60        }
61        if self.initial_facts.len() > RESIDENT_PROGRAM_FACT_CAPACITY {
62            return Err("binary program exceeds resident fact capacity");
63        }
64        if self.initial_rules.len() > RESIDENT_PROGRAM_RULE_CAPACITY - 2 {
65            return Err("binary program leaves no room for two rule edits");
66        }
67        for rule in &self.initial_rules {
68            if !(1..=2).contains(&rule.body_count)
69                || rule.head_predicate >= self.predicate_count
70                || rule.left_predicate >= self.predicate_count
71                || (rule.body_count == 2 && rule.right_predicate >= self.predicate_count)
72                || (rule.body_count == 1
73                    && (rule.right_predicate != 0 || rule.right_variables != [0, 0]))
74            {
75                return Err("binary program has an invalid rule predicate or body");
76            }
77            let mut bound = [false; 4];
78            for &variable in rule.left_variables.iter().chain(
79                (rule.body_count == 2)
80                    .then_some(&rule.right_variables)
81                    .into_iter()
82                    .flatten(),
83            ) {
84                let slot = bound
85                    .get_mut(variable as usize)
86                    .ok_or("binary rule variable exceeds its four-slot domain")?;
87                *slot = true;
88            }
89            if rule
90                .head_variables
91                .iter()
92                .any(|&variable| !bound.get(variable as usize).copied().unwrap_or(false))
93            {
94                return Err("binary rule head contains an unbound variable");
95            }
96        }
97        Ok(())
98    }
99
100    /// Canonical device-bank words, independent of host struct padding.
101    pub(crate) fn words(&self) -> Vec<u64> {
102        let mut words =
103            Vec::with_capacity(12 + self.initial_facts.len() * 3 + self.initial_rules.len() * 10);
104        words.extend([
105            u64::from(self.predicate_count),
106            self.initial_facts.len() as u64,
107            self.initial_rules.len() as u64,
108        ]);
109        for fact in self.queries.iter().chain(&self.initial_facts) {
110            words.extend([
111                u64::from(fact.predicate),
112                u64::from(fact.first),
113                u64::from(fact.second),
114            ]);
115        }
116        for rule in &self.initial_rules {
117            words.extend([
118                u64::from(rule.head_predicate),
119                u64::from(rule.left_predicate),
120                u64::from(rule.right_predicate),
121                u64::from(rule.body_count),
122                u64::from(rule.head_variables[0]),
123                u64::from(rule.head_variables[1]),
124                u64::from(rule.left_variables[0]),
125                u64::from(rule.left_variables[1]),
126                u64::from(rule.right_variables[0]),
127                u64::from(rule.right_variables[1]),
128            ]);
129        }
130        words
131    }
132}
133
134const _: () = {
135    assert!(std::mem::size_of::<SemanticProgramFact>() == 12);
136    assert!(std::mem::size_of::<SemanticProgramRule>() == 40);
137};
138
139#[cfg(test)]
140mod tests {
141    use super::*;
142
143    #[test]
144    fn program_bank_words_match_the_native_decoder_layout() {
145        let program = SemanticProgramAdmission {
146            predicate_count: 2,
147            initial_facts: vec![SemanticProgramFact {
148                predicate: 0,
149                first: 1,
150                second: 3,
151            }],
152            initial_rules: vec![SemanticProgramRule {
153                head_predicate: 1,
154                left_predicate: 0,
155                right_predicate: 0,
156                body_count: 1,
157                head_variables: [0, 1],
158                left_variables: [0, 1],
159                right_variables: [0, 0],
160            }],
161            queries: [
162                SemanticProgramFact {
163                    predicate: 1,
164                    first: 1,
165                    second: 3,
166                },
167                SemanticProgramFact {
168                    predicate: 1,
169                    first: 2,
170                    second: 3,
171                },
172                SemanticProgramFact {
173                    predicate: 1,
174                    first: 3,
175                    second: 4,
176                },
177            ],
178        };
179        assert_eq!(
180            program.words(),
181            [2, 1, 1, 1, 1, 3, 1, 2, 3, 1, 3, 4, 0, 1, 3, 1, 0, 0, 1, 0, 1, 0, 1, 0, 0]
182        );
183        assert_eq!(program.validate(), Ok(()));
184        let mut unsafe_rule = program.clone();
185        unsafe_rule.initial_rules[0].head_variables = [2, 2];
186        assert_eq!(
187            unsafe_rule.validate(),
188            Err("binary rule head contains an unbound variable")
189        );
190        let mut too_many_facts = program.clone();
191        too_many_facts.initial_facts = vec![program.initial_facts[0]; 4097];
192        assert_eq!(
193            too_many_facts.validate(),
194            Err("binary program exceeds resident fact capacity")
195        );
196        let mut too_many_rules = program.clone();
197        too_many_rules.initial_rules = vec![program.initial_rules[0]; 255];
198        assert_eq!(
199            too_many_rules.validate(),
200            Err("binary program leaves no room for two rule edits")
201        );
202    }
203}
xlog_cuda/semantic_program.rs

xlog_cuda/
semantic_program.rs
