qualia_core_db/modalities/
linear.rs

1use crate::NQuin;
2
3// Marks a Quin as consumed by setting metadata bit 59 (CONSUMED_BIT).
4// Canonical bit position lives in the FrameLayout ABI (single source of truth).
5pub use crate::frame_layout::CONSUMED_BIT;
6
7pub fn consume_quin(q: &mut NQuin) {
8    q.metadata |= CONSUMED_BIT;
9}
10
11pub fn is_consumed(q: &NQuin) -> bool {
12    (q.metadata & CONSUMED_BIT) != 0
13}
14
15// ─── Girard's linear-logic connectives ──────────────────────────────────────────────
16//
17// Linear logic treats propositions as RESOURCES: each is used exactly once unless explicitly
18// marked reusable with the `!` exponential. The connectives split into multiplicatives
19// (⊗ tensor, ⅋ par), additives (⊕ plus, & with), their units, and the exponentials (! ?).
20
21#[derive(Debug, Clone, Copy, PartialEq, Eq)]
22pub enum Connective {
23    /// A positive literal.
24    Atom,
25    /// A literal's linear negation `a⊥`.
26    AtomDual,
27    /// `A ⊗ B` — multiplicative conjunction ("both, together").
28    Tensor,
29    /// `A ⅋ B` — multiplicative disjunction.
30    Par,
31    /// `A ⊕ B` — additive disjunction (internal choice).
32    Plus,
33    /// `A & B` — additive conjunction (external choice).
34    With,
35    /// `1` — unit of `⊗`.
36    One,
37    /// `⊥` — unit of `⅋`.
38    Bottom,
39    /// `0` — unit of `⊕`.
40    Zero,
41    /// `⊤` — unit of `&`.
42    Top,
43    /// `!A` — exponential "of course" (reusable: weakening + contraction apply).
44    OfCourse,
45    /// `?A` — exponential "why not" (dual of `!`).
46    WhyNot,
47}
48
49impl Connective {
50    /// Linear negation `(·)⊥` — the involutive De Morgan dual (`A⊥⊥ = A`).
51    pub fn dual(self) -> Connective {
52        use Connective::*;
53        match self {
54            Atom => AtomDual,
55            AtomDual => Atom,
56            Tensor => Par,
57            Par => Tensor,
58            Plus => With,
59            With => Plus,
60            One => Bottom,
61            Bottom => One,
62            Zero => Top,
63            Top => Zero,
64            OfCourse => WhyNot,
65            WhyNot => OfCourse,
66        }
67    }
68
69    /// Multiplicative connectives/units (`⊗ ⅋ 1 ⊥`).
70    pub fn is_multiplicative(self) -> bool {
71        use Connective::*;
72        matches!(self, Tensor | Par | One | Bottom)
73    }
74
75    /// Additive connectives/units (`⊕ & 0 ⊤`).
76    pub fn is_additive(self) -> bool {
77        use Connective::*;
78        matches!(self, Plus | With | Zero | Top)
79    }
80
81    /// Exponential connectives (`! ?`).
82    pub fn is_exponential(self) -> bool {
83        matches!(self, Connective::OfCourse | Connective::WhyNot)
84    }
85
86    /// A resource under `!` ("of course") is **reusable** — structural weakening and contraction
87    /// are licensed. Everything else is linear (consume-once).
88    pub fn is_reusable(self) -> bool {
89        matches!(self, Connective::OfCourse)
90    }
91}
92
93/// Whether a resource quin `q` may be consumed to satisfy a demand: a reusable (`!`-marked)
94/// resource always can; a linear resource only if not already consumed.
95pub fn can_consume(q: &NQuin, reusable: bool) -> bool {
96    reusable || !is_consumed(q)
97}
98
99/// `A ⊗ B` consumption: a tensor demand needs **both** operands available *together*. Consumes
100/// each linear operand (leaves reusable ones); returns `false` without mutating if either is
101/// already exhausted.
102pub fn tensor_consume(a: &mut NQuin, a_reusable: bool, b: &mut NQuin, b_reusable: bool) -> bool {
103    if !can_consume(a, a_reusable) || !can_consume(b, b_reusable) {
104        return false;
105    }
106    if !a_reusable {
107        consume_quin(a);
108    }
109    if !b_reusable {
110        consume_quin(b);
111    }
112    true
113}
114
115// ─── Structural-rule discipline (weakening & contraction strictly controlled) ───────
116//
117// Linear logic's defining feature: the structural rules WEAKENING (discard a resource) and
118// CONTRACTION (duplicate a resource) are NOT freely available — they are licensed only on
119// reusable `!`-marked formulas. Exchange (reorder) is always fine.
120
121#[derive(Debug, Clone, Copy, PartialEq, Eq)]
122pub enum StructuralRule {
123    /// Discard a formula from the sequent.
124    Weakening,
125    /// Duplicate a formula in the sequent.
126    Contraction,
127    /// Reorder formulas.
128    Exchange,
129}
130
131/// Is applying `rule` to a formula with the given reusability licensed? Exchange always; Weakening
132/// and Contraction **only** on a reusable (`!`-marked) formula — applying either to a linear
133/// resource is an illegal proof step (resources must be used exactly once).
134pub fn structural_rule_licensed(rule: StructuralRule, reusable: bool) -> bool {
135    match rule {
136        StructuralRule::Exchange => true,
137        StructuralRule::Weakening | StructuralRule::Contraction => reusable,
138    }
139}
140
141/// Validate a whole sequence of structural-rule applications `(rule, reusable)`; every step must
142/// be licensed for the derivation to be well-formed.
143pub fn structural_derivation_valid(steps: &[(StructuralRule, bool)]) -> bool {
144    steps
145        .iter()
146        .all(|&(rule, reusable)| structural_rule_licensed(rule, reusable))
147}
148
149// ─── Proof-net validation (Danos-Regnier correctness, multiplicative fragment) ──────
150//
151// A multiplicative proof structure is a genuine PROOF NET iff every Danos-Regnier *switching*
152// (each `⅋` node keeps exactly one of its two premise edges) yields a tree — acyclic AND
153// connected. We enumerate the 2^(#par) switchings and check each with union-find. Bounded and
154// zero-heap (fixed-size stack arrays).
155
156/// Max nodes / par-links for the bounded DR check.
157pub const MAX_PN_NODES: usize = 32;
158/// Max `⅋` links (2^MAX_PN_PARS switchings enumerated).
159pub const MAX_PN_PARS: usize = 12;
160
161#[inline]
162fn pn_find(parent: &mut [usize; MAX_PN_NODES], mut x: usize) -> usize {
163    while parent[x] != x {
164        parent[x] = parent[parent[x]]; // path halving
165        x = parent[x];
166    }
167    x
168}
169
170/// Union `a`,`b`; returns `false` if they were already connected (i.e. this edge closes a cycle).
171#[inline]
172fn pn_union(parent: &mut [usize; MAX_PN_NODES], a: usize, b: usize) -> bool {
173    let ra = pn_find(parent, a);
174    let rb = pn_find(parent, b);
175    if ra == rb {
176        return false;
177    }
178    parent[ra] = rb;
179    true
180}
181
182/// Danos-Regnier check: is the proof structure a **proof net**? `n_nodes` formula occurrences,
183/// the always-present `fixed_edges` (axiom / cut / `⊗` links), and the `par_switches` (each a
184/// pair of candidate edges for one `⅋`, one chosen per switching). Returns true iff EVERY
185/// switching graph is a tree. Bounded by [`MAX_PN_NODES`] / [`MAX_PN_PARS`].
186pub fn is_proof_net(
187    n_nodes: usize,
188    fixed_edges: &[(usize, usize)],
189    par_switches: &[((usize, usize), (usize, usize))],
190) -> bool {
191    if n_nodes == 0 || n_nodes > MAX_PN_NODES || par_switches.len() > MAX_PN_PARS {
192        return false;
193    }
194    let k = par_switches.len();
195    for mask in 0u32..(1u32 << k) {
196        let mut parent = [0usize; MAX_PN_NODES];
197        for (i, p) in parent.iter_mut().enumerate().take(n_nodes) {
198            *p = i;
199        }
200        let mut acyclic = true;
201        let mut edge_count = 0usize;
202
203        for &(a, b) in fixed_edges {
204            if a >= n_nodes || b >= n_nodes {
205                return false;
206            }
207            if !pn_union(&mut parent, a, b) {
208                acyclic = false;
209            }
210            edge_count += 1;
211        }
212        for (j, &(ea, eb)) in par_switches.iter().enumerate() {
213            let (a, b) = if (mask >> j) & 1 == 0 { ea } else { eb };
214            if a >= n_nodes || b >= n_nodes {
215                return false;
216            }
217            if !pn_union(&mut parent, a, b) {
218                acyclic = false;
219            }
220            edge_count += 1;
221        }
222
223        // Tree ⟺ acyclic ∧ connected ⟺ acyclic ∧ edge_count == n-1 ∧ single component.
224        if !acyclic || edge_count != n_nodes - 1 {
225            return false;
226        }
227        let root = pn_find(&mut parent, 0);
228        for i in 1..n_nodes {
229            if pn_find(&mut parent, i) != root {
230                return false; // disconnected switching → not a proof net
231            }
232        }
233    }
234    true
235}
236
237// ─── Zero-knowledge–gated resource exhaustion ───────────────────────────────────────
238
239/// ZK-gated consumption: a linear resource may be exhausted **only** if a zero-knowledge proof of
240/// entitlement verifies (the witness stays private). Composes the verification boolean — produced
241/// by `zk_proofs` / `legal_compose::zk_eligibility` — with the linear consume-once discipline.
242/// Consumes (and returns `true`) iff the proof holds AND the resource is available. The webizen-VM
243/// opcode dispatch that *invokes* this gate is a separate, out-of-(this-crate-scope) wiring step.
244pub fn zk_gated_consume(q: &mut NQuin, reusable: bool, proof_verified: bool) -> bool {
245    if !proof_verified || !can_consume(q, reusable) {
246        return false;
247    }
248    if !reusable {
249        consume_quin(q);
250    }
251    true
252}
253
254#[cfg(test)]
255mod tests {
256    use super::*;
257
258    #[test]
259    fn test_consume_quin() {
260        let mut q = NQuin {
261            subject: 0,
262            predicate: 0,
263            object: 0,
264            context: 0,
265            metadata: 0,
266            parity: 0,
267        };
268        assert!(!is_consumed(&q));
269        consume_quin(&mut q);
270        assert!(is_consumed(&q));
271    }
272
273    #[test]
274    fn linear_negation_is_involutive_and_dualises_connectives() {
275        use Connective::*;
276        for c in [
277            Atom, AtomDual, Tensor, Par, Plus, With, One, Bottom, Zero, Top, OfCourse, WhyNot,
278        ] {
279            assert_eq!(c.dual().dual(), c, "(A⊥)⊥ = A for {:?}", c);
280            assert_ne!(c.dual(), c, "no connective is its own dual: {:?}", c);
281        }
282        // The characteristic De Morgan dualities.
283        assert_eq!(Tensor.dual(), Par);
284        assert_eq!(Plus.dual(), With);
285        assert_eq!(One.dual(), Bottom);
286        assert_eq!(Zero.dual(), Top);
287        assert_eq!(OfCourse.dual(), WhyNot);
288    }
289
290    #[test]
291    fn connective_classification_and_reuse() {
292        use Connective::*;
293        assert!(Tensor.is_multiplicative() && !Tensor.is_additive());
294        assert!(With.is_additive() && !With.is_multiplicative());
295        assert!(OfCourse.is_exponential() && WhyNot.is_exponential());
296        // Only `!A` is reusable; linear atoms are consume-once.
297        assert!(OfCourse.is_reusable());
298        assert!(!Atom.is_reusable());
299    }
300
301    #[test]
302    fn tensor_consumes_both_and_respects_reuse() {
303        let mk = || NQuin {
304            subject: 1,
305            predicate: 2,
306            object: 3,
307            context: 0,
308            metadata: 0,
309            parity: 0,
310        };
311        // Two linear resources: tensor consumes both; a second demand fails.
312        let mut a = mk();
313        let mut b = mk();
314        assert!(tensor_consume(&mut a, false, &mut b, false));
315        assert!(is_consumed(&a) && is_consumed(&b));
316        assert!(
317            !tensor_consume(&mut a, false, &mut b, false),
318            "linear resources are exhausted"
319        );
320
321        // A reusable (!-marked) resource is never exhausted.
322        let mut r = mk();
323        let mut s = mk();
324        assert!(tensor_consume(&mut r, true, &mut s, false));
325        assert!(!is_consumed(&r), "reusable resource is not consumed");
326        assert!(is_consumed(&s));
327        assert!(
328            tensor_consume(&mut r, true, &mut s, true),
329            "reusable can satisfy again"
330        );
331    }
332
333    #[test]
334    fn structural_rules_are_controlled() {
335        // Weakening / contraction only on reusable (!) formulas; never on linear ones.
336        assert!(!structural_rule_licensed(StructuralRule::Weakening, false));
337        assert!(!structural_rule_licensed(
338            StructuralRule::Contraction,
339            false
340        ));
341        assert!(structural_rule_licensed(StructuralRule::Weakening, true));
342        assert!(structural_rule_licensed(StructuralRule::Contraction, true));
343        // Exchange is always fine.
344        assert!(structural_rule_licensed(StructuralRule::Exchange, false));
345        // A whole derivation: contraction on a reusable + exchange on a linear → valid.
346        assert!(structural_derivation_valid(&[
347            (StructuralRule::Contraction, true),
348            (StructuralRule::Exchange, false),
349        ]));
350        // …but contraction on a linear resource invalidates it.
351        assert!(!structural_derivation_valid(&[(
352            StructuralRule::Contraction,
353            false
354        )]));
355    }
356
357    #[test]
358    fn danos_regnier_distinguishes_nets_from_non_nets() {
359        // A single edge over 2 nodes, no pars → tree → net.
360        assert!(is_proof_net(2, &[(0, 1)], &[]));
361        // Disconnected: 3 nodes, 1 edge → not connected → not a net.
362        assert!(!is_proof_net(3, &[(0, 1)], &[]));
363        // Cyclic: 3 nodes, edges forming a triangle → cycle → not a net.
364        assert!(!is_proof_net(3, &[(0, 1), (1, 2), (0, 2)], &[]));
365
366        // A par link: 3 nodes, fixed edge (0,1), the ⅋ switches between (0,2) and (1,2).
367        // BOTH switchings give a 3-node/2-edge connected acyclic tree → net.
368        assert!(is_proof_net(3, &[(0, 1)], &[((0, 2), (1, 2))]));
369
370        // A par whose both candidate edges duplicate the fixed edge → every switching makes a
371        // cycle on {0,1} and leaves node 2 isolated → not a net.
372        assert!(!is_proof_net(3, &[(0, 1)], &[((0, 1), (0, 1))]));
373
374        // Bounds are enforced.
375        assert!(!is_proof_net(0, &[], &[]));
376        assert!(
377            !is_proof_net(2, &[(0, 5)], &[]),
378            "edge to out-of-range node rejected"
379        );
380    }
381
382    #[test]
383    fn zk_gate_controls_resource_exhaustion() {
384        let mk = || NQuin {
385            subject: 1,
386            predicate: 2,
387            object: 3,
388            context: 0,
389            metadata: 0,
390            parity: 0,
391        };
392        // No proof → no consumption, resource untouched.
393        let mut q = mk();
394        assert!(!zk_gated_consume(&mut q, false, false));
395        assert!(!is_consumed(&q));
396        // Valid proof → linear resource consumed once, then exhausted.
397        assert!(zk_gated_consume(&mut q, false, true));
398        assert!(is_consumed(&q));
399        assert!(!zk_gated_consume(&mut q, false, true), "already exhausted");
400        // Reusable resource with a valid proof is never exhausted.
401        let mut r = mk();
402        assert!(zk_gated_consume(&mut r, true, true));
403        assert!(!is_consumed(&r));
404    }
405}
qualia_core_db/modalities/linear.rs

qualia_core_db/modalities/
linear.rs
