hawdb_expression/
null_rejection.rs

1// Copyright 2026 Nowledge
2//
3// Licensed under the Apache License, Version 2.0 (the "License");
4// you may not use this file except in compliance with the License.
5// You may obtain a copy of the License at
6//
7//     http://www.apache.org/licenses/LICENSE-2.0
8//
9// Unless required by applicable law or agreed to in writing, software
10// distributed under the License is distributed on an "AS IS" BASIS,
11// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12// See the License for the specific language governing permissions and
13// limitations under the License.
14
15//! Conservative SQL three-valued-logic analysis for join legality proofs.
16
17use std::{collections::BTreeSet, ops::Not};
18
19/// A stable binder-assigned identity for one relational or graph binding.
20#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
21pub struct BindingId(u32);
22
23impl BindingId {
24    pub const fn new(value: u32) -> Self {
25        Self(value)
26    }
27
28    pub const fn get(self) -> u32 {
29        self.0
30    }
31}
32
33/// A set of bindings used by predicates and null-extension proofs.
34#[derive(Debug, Clone, Default, PartialEq, Eq, PartialOrd, Ord, Hash)]
35pub struct BindingSet(BTreeSet<BindingId>);
36
37impl BindingSet {
38    pub const fn new() -> Self {
39        Self(BTreeSet::new())
40    }
41
42    pub fn insert(&mut self, binding: BindingId) -> bool {
43        self.0.insert(binding)
44    }
45
46    pub fn contains(&self, binding: BindingId) -> bool {
47        self.0.contains(&binding)
48    }
49
50    pub fn is_empty(&self) -> bool {
51        self.0.is_empty()
52    }
53
54    pub fn len(&self) -> usize {
55        self.0.len()
56    }
57
58    pub fn is_subset(&self, other: &Self) -> bool {
59        self.0.is_subset(&other.0)
60    }
61
62    pub fn intersects(&self, other: &Self) -> bool {
63        self.0.iter().any(|binding| other.contains(*binding))
64    }
65
66    pub fn iter(&self) -> impl Iterator<Item = BindingId> + '_ {
67        self.0.iter().copied()
68    }
69
70    pub fn without(&self, binding: BindingId) -> Self {
71        Self(
72            self.0
73                .iter()
74                .copied()
75                .filter(|candidate| *candidate != binding)
76                .collect(),
77        )
78    }
79
80    fn extend(&mut self, other: &Self) {
81        self.0.extend(other.iter());
82    }
83}
84
85impl From<BindingId> for BindingSet {
86    fn from(binding: BindingId) -> Self {
87        Self::from([binding])
88    }
89}
90
91impl<const N: usize> From<[BindingId; N]> for BindingSet {
92    fn from(bindings: [BindingId; N]) -> Self {
93        Self(bindings.into_iter().collect())
94    }
95}
96
97impl FromIterator<BindingId> for BindingSet {
98    fn from_iter<T: IntoIterator<Item = BindingId>>(iter: T) -> Self {
99        Self(iter.into_iter().collect())
100    }
101}
102
103/// One SQL boolean result, including the `UNKNOWN` value produced by `NULL`.
104#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
105pub enum TruthValue {
106    True,
107    False,
108    Unknown,
109}
110
111impl TruthValue {
112    pub const fn and(self, other: Self) -> Self {
113        match (self, other) {
114            (Self::False, _) | (_, Self::False) => Self::False,
115            (Self::True, Self::True) => Self::True,
116            _ => Self::Unknown,
117        }
118    }
119
120    pub const fn or(self, other: Self) -> Self {
121        match (self, other) {
122            (Self::True, _) | (_, Self::True) => Self::True,
123            (Self::False, Self::False) => Self::False,
124            _ => Self::Unknown,
125        }
126    }
127}
128
129impl Not for TruthValue {
130    type Output = Self;
131
132    fn not(self) -> Self::Output {
133        match self {
134            Self::True => Self::False,
135            Self::False => Self::True,
136            Self::Unknown => Self::Unknown,
137        }
138    }
139}
140
141/// An over-approximation of the truth values an expression can produce.
142#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
143pub struct TruthSet(u8);
144
145impl TruthSet {
146    const TRUE_BIT: u8 = 1 << 0;
147    const FALSE_BIT: u8 = 1 << 1;
148    const UNKNOWN_BIT: u8 = 1 << 2;
149
150    pub const fn empty() -> Self {
151        Self(0)
152    }
153
154    pub const fn all() -> Self {
155        Self(Self::TRUE_BIT | Self::FALSE_BIT | Self::UNKNOWN_BIT)
156    }
157
158    pub const fn singleton(value: TruthValue) -> Self {
159        Self(Self::bit(value))
160    }
161
162    pub const fn contains(self, value: TruthValue) -> bool {
163        self.0 & Self::bit(value) != 0
164    }
165
166    pub const fn union(self, other: Self) -> Self {
167        Self(self.0 | other.0)
168    }
169
170    pub fn and(self, other: Self) -> Self {
171        self.combine(other, TruthValue::and)
172    }
173
174    pub fn or(self, other: Self) -> Self {
175        self.combine(other, TruthValue::or)
176    }
177
178    const fn bit(value: TruthValue) -> u8 {
179        match value {
180            TruthValue::True => Self::TRUE_BIT,
181            TruthValue::False => Self::FALSE_BIT,
182            TruthValue::Unknown => Self::UNKNOWN_BIT,
183        }
184    }
185
186    fn map(self, operation: impl Fn(TruthValue) -> TruthValue) -> Self {
187        let mut result = Self::empty();
188        for value in truth_values() {
189            if self.contains(value) {
190                result = result.union(Self::singleton(operation(value)));
191            }
192        }
193        result
194    }
195
196    fn combine(
197        self,
198        other: Self,
199        operation: impl Fn(TruthValue, TruthValue) -> TruthValue,
200    ) -> Self {
201        let mut result = Self::empty();
202        for left in truth_values() {
203            if !self.contains(left) {
204                continue;
205            }
206            for right in truth_values() {
207                if other.contains(right) {
208                    result = result.union(Self::singleton(operation(left, right)));
209                }
210            }
211        }
212        result
213    }
214}
215
216impl Not for TruthSet {
217    type Output = Self;
218
219    fn not(self) -> Self::Output {
220        self.map(Not::not)
221    }
222}
223
224fn truth_values() -> [TruthValue; 3] {
225    [TruthValue::True, TruthValue::False, TruthValue::Unknown]
226}
227
228/// The possible null states of a scalar expression.
229#[derive(Debug, Clone, Copy, PartialEq, Eq)]
230pub enum ScalarNullability {
231    AlwaysNull,
232    AlwaysNonNull,
233    MaybeNull,
234}
235
236impl ScalarNullability {
237    pub const fn can_be_null(self) -> bool {
238        matches!(self, Self::AlwaysNull | Self::MaybeNull)
239    }
240
241    pub const fn can_be_non_null(self) -> bool {
242        matches!(self, Self::AlwaysNonNull | Self::MaybeNull)
243    }
244
245    fn from_possibilities(can_be_null: bool, can_be_non_null: bool) -> Self {
246        match (can_be_null, can_be_non_null) {
247            (true, false) => Self::AlwaysNull,
248            (false, true) => Self::AlwaysNonNull,
249            (true, true) => Self::MaybeNull,
250            (false, false) => unreachable!("a scalar expression must have a possible value"),
251        }
252    }
253}
254
255/// Bound scalar nodes required by the null-rejection analysis.
256///
257/// Binders should use [`Self::Opaque`] for unsupported expressions. A strict
258/// call promises only that a null argument produces a null result; callers
259/// must describe the result's nullability when every argument is non-null.
260#[derive(Debug, Clone, PartialEq, Eq)]
261pub enum BoundScalarExpression {
262    BindingValue {
263        binding: BindingId,
264        nullability: ScalarNullability,
265    },
266    LiteralNull,
267    LiteralNonNull,
268    Parameter {
269        nullability: ScalarNullability,
270    },
271    StrictCall {
272        arguments: Vec<Self>,
273        result_nullability_when_arguments_non_null: ScalarNullability,
274    },
275    Coalesce(Vec<Self>),
276    Opaque {
277        referenced_bindings: BindingSet,
278        nullability: ScalarNullability,
279    },
280}
281
282impl BoundScalarExpression {
283    pub fn referenced_bindings(&self) -> BindingSet {
284        match self {
285            Self::BindingValue { binding, .. } => (*binding).into(),
286            Self::LiteralNull | Self::LiteralNonNull | Self::Parameter { .. } => BindingSet::new(),
287            Self::StrictCall { arguments, .. } | Self::Coalesce(arguments) => {
288                referenced_scalar_bindings(arguments)
289            }
290            Self::Opaque {
291                referenced_bindings,
292                ..
293            } => referenced_bindings.clone(),
294        }
295    }
296
297    fn nullability_when_null_extended(&self, null_bindings: &BindingSet) -> ScalarNullability {
298        match self {
299            Self::BindingValue {
300                binding,
301                nullability,
302            } => {
303                if null_bindings.contains(*binding) {
304                    ScalarNullability::AlwaysNull
305                } else {
306                    *nullability
307                }
308            }
309            Self::LiteralNull => ScalarNullability::AlwaysNull,
310            Self::LiteralNonNull => ScalarNullability::AlwaysNonNull,
311            Self::Parameter { nullability } => *nullability,
312            Self::StrictCall {
313                arguments,
314                result_nullability_when_arguments_non_null,
315            } => strict_call_nullability(
316                arguments,
317                *result_nullability_when_arguments_non_null,
318                null_bindings,
319            ),
320            Self::Coalesce(arguments) => {
321                let nullabilities = arguments
322                    .iter()
323                    .map(|argument| argument.nullability_when_null_extended(null_bindings));
324                ScalarNullability::from_possibilities(
325                    nullabilities.clone().all(ScalarNullability::can_be_null),
326                    nullabilities
327                        .clone()
328                        .any(ScalarNullability::can_be_non_null),
329                )
330            }
331            Self::Opaque { nullability, .. } => *nullability,
332        }
333    }
334}
335
336/// Bound boolean nodes required by the null-rejection analysis.
337#[derive(Debug, Clone, PartialEq, Eq)]
338pub enum BoundPredicate {
339    And(Vec<Self>),
340    Or(Vec<Self>),
341    Not(Box<Self>),
342    Constant(TruthValue),
343    Comparison {
344        left: BoundScalarExpression,
345        right: BoundScalarExpression,
346    },
347    IsNull(BoundScalarExpression),
348    IsNotNull(BoundScalarExpression),
349    InList {
350        expression: BoundScalarExpression,
351        values: Vec<BoundScalarExpression>,
352        negated: bool,
353    },
354    IsDistinctFrom {
355        left: BoundScalarExpression,
356        right: BoundScalarExpression,
357    },
358    IsNotDistinctFrom {
359        left: BoundScalarExpression,
360        right: BoundScalarExpression,
361    },
362    /// Tests whether every listed binding is present in the current row.
363    ///
364    /// This is not a general SQL `EXISTS` subquery. Unsupported subqueries must
365    /// be represented by [`Self::Opaque`].
366    BindingsPresent {
367        required_bindings: BindingSet,
368    },
369    Opaque {
370        referenced_bindings: BindingSet,
371    },
372}
373
374impl BoundPredicate {
375    pub fn referenced_bindings(&self) -> BindingSet {
376        match self {
377            Self::And(predicates) | Self::Or(predicates) => {
378                let mut bindings = BindingSet::new();
379                for predicate in predicates {
380                    bindings.extend(&predicate.referenced_bindings());
381                }
382                bindings
383            }
384            Self::Not(predicate) => predicate.referenced_bindings(),
385            Self::Constant(_) => BindingSet::new(),
386            Self::Comparison { left, right }
387            | Self::IsDistinctFrom { left, right }
388            | Self::IsNotDistinctFrom { left, right } => binary_scalar_bindings(left, right),
389            Self::IsNull(expression) | Self::IsNotNull(expression) => {
390                expression.referenced_bindings()
391            }
392            Self::InList {
393                expression, values, ..
394            } => {
395                let mut bindings = expression.referenced_bindings();
396                bindings.extend(&referenced_scalar_bindings(values));
397                bindings
398            }
399            Self::BindingsPresent { required_bindings }
400            | Self::Opaque {
401                referenced_bindings: required_bindings,
402            } => required_bindings.clone(),
403        }
404    }
405
406    fn possible_truths_when_null_extended(&self, null_bindings: &BindingSet) -> TruthSet {
407        match self {
408            Self::And(predicates) => predicates.iter().fold(
409                TruthSet::singleton(TruthValue::True),
410                |truths, predicate| {
411                    truths.and(predicate.possible_truths_when_null_extended(null_bindings))
412                },
413            ),
414            Self::Or(predicates) => predicates.iter().fold(
415                TruthSet::singleton(TruthValue::False),
416                |truths, predicate| {
417                    truths.or(predicate.possible_truths_when_null_extended(null_bindings))
418                },
419            ),
420            Self::Not(predicate) => predicate
421                .possible_truths_when_null_extended(null_bindings)
422                .not(),
423            Self::Constant(value) => TruthSet::singleton(*value),
424            Self::Comparison { left, right } => strict_comparison_truths(
425                left.nullability_when_null_extended(null_bindings),
426                right.nullability_when_null_extended(null_bindings),
427            ),
428            Self::IsNull(expression) => {
429                is_null_truths(expression.nullability_when_null_extended(null_bindings))
430            }
431            Self::IsNotNull(expression) => {
432                !is_null_truths(expression.nullability_when_null_extended(null_bindings))
433            }
434            Self::InList {
435                expression,
436                values,
437                negated,
438            } => {
439                let truths = in_list_truths(expression, values, null_bindings);
440                if *negated {
441                    !truths
442                } else {
443                    truths
444                }
445            }
446            Self::IsDistinctFrom { left, right } => null_safe_comparison_truths(
447                left.nullability_when_null_extended(null_bindings),
448                right.nullability_when_null_extended(null_bindings),
449            ),
450            Self::IsNotDistinctFrom { left, right } => null_safe_comparison_truths(
451                left.nullability_when_null_extended(null_bindings),
452                right.nullability_when_null_extended(null_bindings),
453            )
454            .not(),
455            Self::BindingsPresent { required_bindings } => {
456                if required_bindings.intersects(null_bindings) {
457                    TruthSet::singleton(TruthValue::False)
458                } else {
459                    TruthSet::singleton(TruthValue::True)
460                        .union(TruthSet::singleton(TruthValue::False))
461                }
462            }
463            Self::Opaque { .. } => TruthSet::all(),
464        }
465    }
466}
467
468/// The result of attempting to prove that a predicate rejects null extension.
469///
470/// A proof is valid only when `TRUE` is absent from the over-approximated truth
471/// set. `NotProven` is intentionally not a claim that the predicate accepts a
472/// null-extended row.
473#[derive(Debug, Clone, Copy, PartialEq, Eq)]
474pub enum NullRejectionProof {
475    Proven { possible_truths: TruthSet },
476    NotProven { possible_truths: TruthSet },
477}
478
479impl NullRejectionProof {
480    pub const fn is_proven(self) -> bool {
481        matches!(self, Self::Proven { .. })
482    }
483
484    pub const fn possible_truths(self) -> TruthSet {
485        match self {
486            Self::Proven { possible_truths } | Self::NotProven { possible_truths } => {
487                possible_truths
488            }
489        }
490    }
491}
492
493/// Proves whether `predicate` can never be `TRUE` after null-extending bindings.
494///
495/// The analysis is conservative: unsupported expressions retain all possible
496/// truth values and therefore cannot independently authorize a join rewrite.
497pub fn prove_null_rejecting(
498    predicate: &BoundPredicate,
499    null_bindings: &BindingSet,
500) -> NullRejectionProof {
501    let possible_truths = predicate.possible_truths_when_null_extended(null_bindings);
502    if possible_truths.contains(TruthValue::True) {
503        NullRejectionProof::NotProven { possible_truths }
504    } else {
505        NullRejectionProof::Proven { possible_truths }
506    }
507}
508
509fn referenced_scalar_bindings(expressions: &[BoundScalarExpression]) -> BindingSet {
510    let mut bindings = BindingSet::new();
511    for expression in expressions {
512        bindings.extend(&expression.referenced_bindings());
513    }
514    bindings
515}
516
517fn binary_scalar_bindings(
518    left: &BoundScalarExpression,
519    right: &BoundScalarExpression,
520) -> BindingSet {
521    let mut bindings = left.referenced_bindings();
522    bindings.extend(&right.referenced_bindings());
523    bindings
524}
525
526fn strict_call_nullability(
527    arguments: &[BoundScalarExpression],
528    result_when_non_null: ScalarNullability,
529    null_bindings: &BindingSet,
530) -> ScalarNullability {
531    let nullabilities = arguments
532        .iter()
533        .map(|argument| argument.nullability_when_null_extended(null_bindings));
534    let arguments_can_all_be_non_null = nullabilities
535        .clone()
536        .all(ScalarNullability::can_be_non_null);
537    if !arguments_can_all_be_non_null {
538        return ScalarNullability::AlwaysNull;
539    }
540
541    let an_argument_can_be_null = nullabilities.clone().any(ScalarNullability::can_be_null);
542    ScalarNullability::from_possibilities(
543        an_argument_can_be_null || result_when_non_null.can_be_null(),
544        result_when_non_null.can_be_non_null(),
545    )
546}
547
548fn strict_comparison_truths(left: ScalarNullability, right: ScalarNullability) -> TruthSet {
549    let mut truths = TruthSet::empty();
550    if left.can_be_null() || right.can_be_null() {
551        truths = truths.union(TruthSet::singleton(TruthValue::Unknown));
552    }
553    if left.can_be_non_null() && right.can_be_non_null() {
554        truths = truths
555            .union(TruthSet::singleton(TruthValue::True))
556            .union(TruthSet::singleton(TruthValue::False));
557    }
558    truths
559}
560
561fn is_null_truths(nullability: ScalarNullability) -> TruthSet {
562    let mut truths = TruthSet::empty();
563    if nullability.can_be_null() {
564        truths = truths.union(TruthSet::singleton(TruthValue::True));
565    }
566    if nullability.can_be_non_null() {
567        truths = truths.union(TruthSet::singleton(TruthValue::False));
568    }
569    truths
570}
571
572fn in_list_truths(
573    expression: &BoundScalarExpression,
574    values: &[BoundScalarExpression],
575    null_bindings: &BindingSet,
576) -> TruthSet {
577    let expression = expression.nullability_when_null_extended(null_bindings);
578    let value_nullabilities: Vec<_> = values
579        .iter()
580        .map(|value| value.nullability_when_null_extended(null_bindings))
581        .collect();
582    let mut truths = TruthSet::empty();
583
584    if expression.can_be_null() {
585        truths = truths.union(TruthSet::singleton(TruthValue::Unknown));
586    }
587    if !expression.can_be_non_null() {
588        return truths;
589    }
590    if value_nullabilities.is_empty() {
591        return truths.union(TruthSet::singleton(TruthValue::False));
592    }
593    if value_nullabilities
594        .iter()
595        .any(|value| value.can_be_non_null())
596    {
597        truths = truths.union(TruthSet::singleton(TruthValue::True));
598    }
599    if value_nullabilities.iter().any(|value| value.can_be_null()) {
600        truths = truths.union(TruthSet::singleton(TruthValue::Unknown));
601    }
602    if value_nullabilities
603        .iter()
604        .all(|value| value.can_be_non_null())
605    {
606        truths = truths.union(TruthSet::singleton(TruthValue::False));
607    }
608    truths
609}
610
611fn null_safe_comparison_truths(left: ScalarNullability, right: ScalarNullability) -> TruthSet {
612    let both_null = left.can_be_null() && right.can_be_null();
613    let exactly_one_null = (left.can_be_null() && right.can_be_non_null())
614        || (left.can_be_non_null() && right.can_be_null());
615    let both_non_null = left.can_be_non_null() && right.can_be_non_null();
616    let mut truths = TruthSet::empty();
617    if both_null || both_non_null {
618        truths = truths.union(TruthSet::singleton(TruthValue::False));
619    }
620    if exactly_one_null || both_non_null {
621        truths = truths.union(TruthSet::singleton(TruthValue::True));
622    }
623    truths
624}
625
626#[cfg(test)]
627mod tests {
628    use super::*;
629
630    const LEFT: BindingId = BindingId::new(1);
631    const RIGHT: BindingId = BindingId::new(2);
632
633    fn binding_value(binding: BindingId) -> BoundScalarExpression {
634        BoundScalarExpression::BindingValue {
635            binding,
636            nullability: ScalarNullability::MaybeNull,
637        }
638    }
639
640    fn non_null_literal() -> BoundScalarExpression {
641        BoundScalarExpression::LiteralNonNull
642    }
643
644    fn comparison(binding: BindingId) -> BoundPredicate {
645        BoundPredicate::Comparison {
646            left: binding_value(binding),
647            right: non_null_literal(),
648        }
649    }
650
651    fn assert_proven(predicate: &BoundPredicate, bindings: impl Into<BindingSet>) {
652        assert!(prove_null_rejecting(predicate, &bindings.into()).is_proven());
653    }
654
655    fn assert_not_proven(predicate: &BoundPredicate, bindings: impl Into<BindingSet>) {
656        assert!(!prove_null_rejecting(predicate, &bindings.into()).is_proven());
657    }
658
659    #[test]
660    fn truth_value_implements_sql_three_valued_logic() {
661        let values = [TruthValue::True, TruthValue::False, TruthValue::Unknown];
662        let expected_not = [TruthValue::False, TruthValue::True, TruthValue::Unknown];
663        let expected_and = [
664            [TruthValue::True, TruthValue::False, TruthValue::Unknown],
665            [TruthValue::False, TruthValue::False, TruthValue::False],
666            [TruthValue::Unknown, TruthValue::False, TruthValue::Unknown],
667        ];
668        let expected_or = [
669            [TruthValue::True, TruthValue::True, TruthValue::True],
670            [TruthValue::True, TruthValue::False, TruthValue::Unknown],
671            [TruthValue::True, TruthValue::Unknown, TruthValue::Unknown],
672        ];
673
674        for (left_index, left) in values.into_iter().enumerate() {
675            assert_eq!(!left, expected_not[left_index]);
676            for (right_index, right) in values.into_iter().enumerate() {
677                assert_eq!(left.and(right), expected_and[left_index][right_index]);
678                assert_eq!(left.or(right), expected_or[left_index][right_index]);
679            }
680        }
681
682        let true_or_unknown =
683            TruthSet::singleton(TruthValue::True).union(TruthSet::singleton(TruthValue::Unknown));
684        assert_eq!(
685            !true_or_unknown,
686            TruthSet::singleton(TruthValue::False).union(TruthSet::singleton(TruthValue::Unknown))
687        );
688    }
689
690    #[test]
691    fn strict_predicates_reject_null_extended_binding() {
692        assert_proven(&comparison(RIGHT), RIGHT);
693        assert_proven(&BoundPredicate::Not(Box::new(comparison(RIGHT))), RIGHT);
694        assert_proven(&BoundPredicate::IsNotNull(binding_value(RIGHT)), RIGHT);
695        assert_not_proven(&BoundPredicate::IsNull(binding_value(RIGHT)), RIGHT);
696    }
697
698    #[test]
699    fn conjunction_and_disjunction_preserve_possible_true_rows() {
700        let left_comparison = comparison(LEFT);
701        let right_comparison = comparison(RIGHT);
702        assert_proven(
703            &BoundPredicate::And(vec![left_comparison.clone(), right_comparison.clone()]),
704            RIGHT,
705        );
706        assert_not_proven(
707            &BoundPredicate::Or(vec![left_comparison, right_comparison]),
708            RIGHT,
709        );
710    }
711
712    #[test]
713    fn coalesce_can_make_a_null_extended_value_non_null() {
714        let predicate = BoundPredicate::Comparison {
715            left: BoundScalarExpression::Coalesce(vec![binding_value(RIGHT), non_null_literal()]),
716            right: non_null_literal(),
717        };
718
719        assert_not_proven(&predicate, RIGHT);
720    }
721
722    #[test]
723    fn null_safe_comparisons_distinguish_null_and_non_null_values() {
724        let distinct = BoundPredicate::IsDistinctFrom {
725            left: binding_value(RIGHT),
726            right: non_null_literal(),
727        };
728        let not_distinct = BoundPredicate::IsNotDistinctFrom {
729            left: binding_value(RIGHT),
730            right: non_null_literal(),
731        };
732        let nulls_not_distinct = BoundPredicate::IsNotDistinctFrom {
733            left: binding_value(RIGHT),
734            right: BoundScalarExpression::LiteralNull,
735        };
736
737        assert_not_proven(&distinct, RIGHT);
738        assert_proven(&not_distinct, RIGHT);
739        assert_not_proven(&nulls_not_distinct, RIGHT);
740    }
741
742    #[test]
743    fn in_and_not_in_reject_a_null_search_value() {
744        let in_list = BoundPredicate::InList {
745            expression: binding_value(RIGHT),
746            values: vec![non_null_literal(), BoundScalarExpression::LiteralNull],
747            negated: false,
748        };
749        let not_in_list = BoundPredicate::InList {
750            expression: binding_value(RIGHT),
751            values: vec![non_null_literal(), BoundScalarExpression::LiteralNull],
752            negated: true,
753        };
754
755        assert_proven(&in_list, RIGHT);
756        assert_proven(&not_in_list, RIGHT);
757    }
758
759    #[test]
760    fn a_binding_set_can_be_rejected_when_each_singleton_is_not() {
761        let predicate = BoundPredicate::Or(vec![
762            BoundPredicate::IsNotNull(binding_value(LEFT)),
763            BoundPredicate::IsNotNull(binding_value(RIGHT)),
764        ]);
765
766        assert_not_proven(&predicate, LEFT);
767        assert_not_proven(&predicate, RIGHT);
768        assert_proven(&predicate, [LEFT, RIGHT]);
769    }
770
771    #[test]
772    fn existence_tracks_null_extended_bindings() {
773        let exists = BoundPredicate::BindingsPresent {
774            required_bindings: RIGHT.into(),
775        };
776
777        assert_proven(&exists, RIGHT);
778        assert_not_proven(&BoundPredicate::Not(Box::new(exists)), RIGHT);
779    }
780
781    #[test]
782    fn opaque_predicates_never_claim_a_proof() {
783        let predicate = BoundPredicate::Opaque {
784            referenced_bindings: RIGHT.into(),
785        };
786
787        let proof = prove_null_rejecting(&predicate, &RIGHT.into());
788        assert_eq!(
789            proof,
790            NullRejectionProof::NotProven {
791                possible_truths: TruthSet::all(),
792            }
793        );
794    }
795
796    #[test]
797    fn referenced_bindings_remain_separate_from_null_rejection() {
798        let constant_false = BoundPredicate::Constant(TruthValue::False);
799
800        assert!(constant_false.referenced_bindings().iter().next().is_none());
801        assert_proven(&constant_false, RIGHT);
802    }
803
804    #[test]
805    fn strict_calls_do_not_assume_non_null_output() {
806        let maybe_null_call = BoundScalarExpression::StrictCall {
807            arguments: vec![non_null_literal()],
808            result_nullability_when_arguments_non_null: ScalarNullability::MaybeNull,
809        };
810        let nullable_result = BoundPredicate::IsNull(maybe_null_call);
811        let null_argument = BoundPredicate::Comparison {
812            left: BoundScalarExpression::StrictCall {
813                arguments: vec![binding_value(RIGHT)],
814                result_nullability_when_arguments_non_null: ScalarNullability::AlwaysNonNull,
815            },
816            right: non_null_literal(),
817        };
818
819        assert_not_proven(&nullable_result, RIGHT);
820        assert_proven(&null_argument, RIGHT);
821    }
822}
hawdb_expression/null_rejection.rs

hawdb_expression/
null_rejection.rs
