Hugging Face's logo

Snapkitty
/
hyperkitty-constraint-dsl

Rust
snapkitty
formal-verification
wasm
Model card Files
xet
 Community
hyperkitty-constraint-dsl
File size: 3,144 Bytes
224e773
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
//! QRA Routing Tensor: Deterministic 6×6 transition table

use super::glyph::Glyph;

/// Complete routing tensor Q[current][previous] = next_glyph
/// H = 0 nats (deterministic): same (current, previous) always yields same next
pub struct Tensor;

impl Tensor {
    /// Look up next glyph given current and previous
    pub fn lookup(current: Glyph, previous: Glyph) -> Glyph {
        Self::TABLE[current.index()][previous.index()]
    }

    /// Full routing table: Q[current][previous] = next
    const TABLE: [[Glyph; 6]; 6] = [
        // current=Pi (0)
        [
            Glyph::Pi,
            Glyph::Gamma,
            Glyph::Delta,
            Glyph::Omega,
            Glyph::Pi,
            Glyph::Psi,
        ],
        // current=Gamma (1)
        [
            Glyph::Gamma,
            Glyph::Delta,
            Glyph::Omega,
            Glyph::Lambda,
            Glyph::Gamma,
            Glyph::Psi,
        ],
        // current=Delta (2)
        [
            Glyph::Delta,
            Glyph::Omega,
            Glyph::Lambda,
            Glyph::Psi,
            Glyph::Delta,
            Glyph::Pi,
        ],
        // current=Omega (3) - ABSORBER: always outputs Omega
        [
            Glyph::Omega,
            Glyph::Omega,
            Glyph::Omega,
            Glyph::Omega,
            Glyph::Omega,
            Glyph::Omega,
        ],
        // current=Lambda (4) - LEFT IDENTITY: passes through previous
        [
            Glyph::Pi,
            Glyph::Gamma,
            Glyph::Delta,
            Glyph::Omega,
            Glyph::Lambda,
            Glyph::Psi,
        ],
        // current=Psi (5)
        [
            Glyph::Psi,
            Glyph::Pi,
            Glyph::Gamma,
            Glyph::Delta,
            Glyph::Psi,
            Glyph::Omega,
        ],
    ];
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn absorber_property() {
        // Omega absorbs: Q[Ω][j] = Ω for all j
        for prev in super::super::glyph::all_glyphs() {
            assert_eq!(Tensor::lookup(Glyph::Omega, prev), Glyph::Omega);
        }
    }

    #[test]
    fn identity_property() {
        // Lambda is left identity: Q[Λ][j] = j for all j
        for prev in super::super::glyph::all_glyphs() {
            assert_eq!(Tensor::lookup(Glyph::Lambda, prev), prev);
        }
    }

    #[test]
    fn determinism() {
        // Same inputs produce same output
        for _ in 0..100 {
            let c = Glyph::Gamma;
            let p = Glyph::Delta;
            let result1 = Tensor::lookup(c, p);
            let result2 = Tensor::lookup(c, p);
            assert_eq!(result1, result2);
        }
    }

    #[test]
    fn complete_table() {
        // All 36 transitions defined
        let mut count = 0;
        for c in super::super::glyph::all_glyphs() {
            for p in super::super::glyph::all_glyphs() {
                let _ = Tensor::lookup(c, p);
                count += 1;
            }
        }
        assert_eq!(count, 36);
    }
}