1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
// Copyright (C) 2026 Postquant Labs Incorporated
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU Affero General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
// GNU Affero General Public License for more details.
//
// You should have received a copy of the GNU Affero General Public License
// along with this program. If not, see <https://www.gnu.org/licenses/>.
//
// SPDX-License-Identifier: AGPL-3.0-or-later
/// A bounded join-semilattice over the data-flow value domain.
///
/// Every data-flow value type must implement this trait. The solver uses
/// `top()` to initialise all nodes and `meet` to combine values arriving
/// from multiple predecessors (or successors for backward analyses).
///
/// # Contract
///
/// The following laws must hold for all values `a`, `b`, `c`:
///
/// - **Commutativity**: `a.meet(b) == b.meet(a)`
/// - **Associativity**: `a.meet(b.meet(c)) == (a.meet(b)).meet(c)`
/// - **Idempotence**: `a.meet(a) == a`
/// - **Identity**: `top().meet(a) == a`
///
/// Violation of these laws will cause the worklist solver to diverge or
/// produce incorrect results.
///
/// # Examples
///
/// ```rust
/// use xqvm::dataflow::Lattice;
///
/// /// A simple "may" lattice over a boolean flag.
/// #[derive(Clone, PartialEq, Eq)]
/// enum MayReach { Unreachable, Reachable }
///
/// impl Lattice for MayReach {
/// fn top() -> Self { Self::Unreachable }
/// fn meet(&self, other: &Self) -> Self {
/// match (self, other) {
/// (Self::Reachable, _) | (_, Self::Reachable) => Self::Reachable,
/// _ => Self::Unreachable,
/// }
/// }
/// }
/// ```