SNAPKITTYWEST commited on
Commit
8ed6bba
·
verified ·
1 Parent(s): f8bd003

chore: convert from dataset to model repo

Browse files
Files changed (7) hide show
  1. README.md +123 -0
  2. assets/logo.svg +16 -0
  3. assets/usage.svg +68 -0
  4. css/style.css +101 -0
  5. index.html +64 -0
  6. js/app.js +61 -0
  7. js/array-lang.js +88 -0
README.md ADDED
@@ -0,0 +1,123 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ <!--OMEGA-FIELD:START-->
2
+ <div align="center">
3
+
4
+ ![License](https://img.shields.io/badge/license-Sovereign%20Source%20v2.0-blueviolet)
5
+ ![Stack](https://img.shields.io/badge/stack-Lean%204%20%7C%20C%2B%2B20%20%7C%20JS-orange)
6
+ ![Kernels](https://img.shields.io/badge/kernels-5%20%CE%A0--maps-green)
7
+ ![Status](https://img.shields.io/badge/status-zero--sorry-success)
8
+ ![Tests](https://img.shields.io/badge/tests-11%2F11%20passing-brightgreen)
9
+ ![Abjad](https://img.shields.io/badge/Abjad--free-red)
10
+ ![DigitalRoot](https://img.shields.io/badge/digital--root--free-red)
11
+ ![NP-magic](https://img.shields.io/badge/NP--magic--free-red)
12
+
13
+ </div>
14
+ <!--OMEGA-FIELD:END-->
15
+
16
+ ---
17
+
18
+ <div align="center">
19
+
20
+ ```
21
+ ____ ____ ____ ____ ____ _ _ ___ ____ ____ _ _ ____ ____
22
+ / ___)( _ \\( _ \\( __)( \\( \\/ )/ __)( __)( _ \\( \\/ )( __)( _ \\
23
+ \\___ \\ ) / ) __/ ) _) ) D ( \\ / \\__ \\ ) _) ) __/ \\ / ) _) ) /
24
+ (____/(__\\_)(__) (____)(____/ \\/ (___/(____)(__) (__) (____)(__\\_)
25
+ A R R A Y L A N G U A G E · A R R A Y I α = I → α
26
+ ```
27
+
28
+ **Array I α = I → α &nbsp;·&nbsp; broadcast = pullback π : J → I &nbsp;·&nbsp; pmap₂ = Π-map &nbsp;·&nbsp; no sorry remains**
29
+
30
+ </div>
31
+
32
+ ---
33
+
34
+ # Sovereign Array Language — Front-End
35
+
36
+ The **front-end** for the [Sovereign Array Language](../sovereign-array): an
37
+ interactive browser playground that runs the *same denotational semantics*
38
+ as the Lean 4 spec and the C++20 kernel — no Abjad, no digital root, no NP-magic.
39
+
40
+ > The denotational semantics of array computing *are* exactly a slice of
41
+ > dependent type theory. This front-end is the view layer over that substrate.
42
+
43
+ ## What this repo is
44
+
45
+ | Layer | Repo | Role |
46
+ |-------|------|------|
47
+ | **Spec** | [`sovereign-array`](../sovereign-array) | Lean 4 — `Array I α = I → α`, zero-sorry proofs |
48
+ | **Kernel** | [`sovereign-array`](../sovereign-array) | C++20 — `Array<T>`, `pmap2`, `broadcast`, `softmax`, `nand_attention` |
49
+ | **Front-End** | **`sovereign-array-frontend`** (this repo) | Browser playground + usage guide |
50
+
51
+ ## Quick Start
52
+
53
+ ```bash
54
+ # Serve the playground (any static server)
55
+ cd sovereign-array-frontend
56
+ python -m http.server 8080
57
+ # open http://localhost:8080
58
+ ```
59
+
60
+ No build step. Pure HTML/CSS/JS (ES modules).
61
+
62
+ ## How to use the language
63
+
64
+ 1. **Spec (Lean 4)** — define arrays as dependent functions `Fin n → α`;
65
+ prove `broadcast_is_pullback` and `softmax_is_pmap` with `lake build` (zero sorry).
66
+ 2. **Kernel (C++20)** — `#include "sovereign_array.h"`; build with CMake;
67
+ run `sovarr_test` (11/11 checks).
68
+ 3. **Front-end (this page)** — open `index.html`; the playground runs the
69
+ same denotational semantics in the browser.
70
+ 4. **Compose** — chain `pmap₂` / `broadcast` / `softmax` / `nand_attention`;
71
+ fusion is Π-map fusion — no loop in the denotation.
72
+
73
+ ## Usage Guide (SVG)
74
+
75
+ ![Sovereign Array usage guide](assets/usage.svg)
76
+
77
+ ## Kernels demonstrated
78
+
79
+ | Kernel | Semantics | Status |
80
+ |--------|-----------|--------|
81
+ | `pmap₂` | Pointwise `Π`-map over index space `I` | ✅ |
82
+ | `broadcast` | Pullback along projection `π : J → I` | ✅ |
83
+ | `softmax` | `Π`-map normalization (shift-invariant) | ✅ |
84
+ | `nand` | Universal boolean gate | ✅ |
85
+ | `nand_attention` | NAND-extracted attention spec | ✅ |
86
+
87
+ ## Layout
88
+
89
+ ```
90
+ sovereign-array-frontend/
91
+ ├── index.html # Playground page
92
+ ├── css/style.css # Sovereign dark theme
93
+ ├── js/
94
+ │ ├── array-lang.js # Browser reference impl (SOVArray, broadcast, softmax, nand)
95
+ │ └── app.js # Playground wiring
96
+ ├── assets/
97
+ │ ├── logo.svg # Σ · I → α mark
98
+ │ └── usage.svg # SVG usage guide
99
+ └── README.md
100
+ ```
101
+
102
+ ## The forbidden list (fatal conflations we do NOT make)
103
+
104
+ - ❌ Proof `O(1)` substitution ⇒ `O(1)` decision procedure (NP stays hard)
105
+ - ❌ Abjad / digital root as universal arithmetic (quotients lose information)
106
+ - ❌ "Univalence replaces SIMD" (needs a compiler: Lean → C → LLVM → SIMD)
107
+
108
+ ---
109
+
110
+ <div align="center">
111
+
112
+ **The substrate is always free. The array is a function.**
113
+
114
+ ```
115
+ Array I α = I → α
116
+ broadcast = pullback π
117
+ pmap₂ = Π-map
118
+ no sorry remains.
119
+ ```
120
+
121
+ *Sovereign Array Language · Front-End · 2026 · Ahmad Ali Parr*
122
+
123
+ </div>
assets/logo.svg ADDED
assets/usage.svg ADDED
css/style.css ADDED
@@ -0,0 +1,101 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ :root {
2
+ --bg: #0a0e1a;
3
+ --panel: #121829;
4
+ --ink: #e6ecff;
5
+ --accent: #7af7c8;
6
+ --accent2: #6ea8ff;
7
+ --muted: #8b95b5;
8
+ --border: #243049;
9
+ }
10
+
11
+ * { box-sizing: border-box; }
12
+
13
+ body {
14
+ margin: 0;
15
+ font-family: "Courier New", ui-monospace, monospace;
16
+ background: var(--bg);
17
+ color: var(--ink);
18
+ line-height: 1.5;
19
+ }
20
+
21
+ .hero {
22
+ text-align: center;
23
+ padding: 2.5rem 1rem 1.5rem;
24
+ border-bottom: 1px solid var(--border);
25
+ background: radial-gradient(circle at 50% 0%, #16203a 0%, var(--bg) 70%);
26
+ }
27
+
28
+ .logo { width: 120px; height: 120px; }
29
+
30
+ .hero h1 {
31
+ margin: 0.5rem 0 0.2rem;
32
+ font-size: 2rem;
33
+ letter-spacing: 0.08em;
34
+ background: linear-gradient(90deg, var(--accent), var(--accent2));
35
+ -webkit-background-clip: text;
36
+ background-clip: text;
37
+ color: transparent;
38
+ }
39
+
40
+ .tagline { color: var(--muted); margin: 0; font-size: 0.85rem; }
41
+
42
+ main {
43
+ max-width: 960px;
44
+ margin: 0 auto;
45
+ padding: 1.5rem 1rem;
46
+ display: grid;
47
+ gap: 1.5rem;
48
+ }
49
+
50
+ .panel {
51
+ background: var(--panel);
52
+ border: 1px solid var(--border);
53
+ border-radius: 10px;
54
+ padding: 1.25rem 1.5rem;
55
+ }
56
+
57
+ .panel h2 { margin-top: 0; color: var(--accent); }
58
+ .panel h3 { color: var(--accent2); margin-bottom: 0.4rem; }
59
+
60
+ button#run {
61
+ background: linear-gradient(90deg, var(--accent), var(--accent2));
62
+ color: #06121f;
63
+ border: none;
64
+ padding: 0.55rem 1.1rem;
65
+ border-radius: 6px;
66
+ font-weight: bold;
67
+ cursor: pointer;
68
+ font-family: inherit;
69
+ }
70
+
71
+ .status { color: var(--accent); min-height: 1.2em; }
72
+
73
+ .kernel {
74
+ border-left: 3px solid var(--accent2);
75
+ padding-left: 0.9rem;
76
+ margin: 1rem 0;
77
+ }
78
+
79
+ pre {
80
+ background: #0c1220;
81
+ border: 1px solid var(--border);
82
+ border-radius: 6px;
83
+ padding: 0.6rem 0.8rem;
84
+ overflow-x: auto;
85
+ color: var(--ink);
86
+ font-size: 0.85rem;
87
+ }
88
+
89
+ .usage { width: 100%; border: 1px solid var(--border); border-radius: 8px; background: #0c1220; }
90
+
91
+ code { color: var(--accent); }
92
+
93
+ footer {
94
+ text-align: center;
95
+ padding: 1.5rem;
96
+ color: var(--muted);
97
+ border-top: 1px solid var(--border);
98
+ font-size: 0.8rem;
99
+ }
100
+
101
+ a { color: var(--accent2); }
index.html ADDED
@@ -0,0 +1,64 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ <!DOCTYPE html>
2
+ <html lang="en">
3
+ <head>
4
+ <meta charset="UTF-8" />
5
+ <meta name="viewport" content="width=device-width, initial-scale=1.0" />
6
+ <title>Sovereign Array Language — Playground</title>
7
+ <link rel="stylesheet" href="css/style.css" />
8
+ <link rel="icon" href="assets/logo.svg" />
9
+ </head>
10
+ <body>
11
+ <header class="hero">
12
+ <img src="assets/logo.svg" alt="Sovereign Array logo" class="logo" />
13
+ <h1>Sovereign Array Language</h1>
14
+ <p class="tagline">Array I α = I → α &nbsp;·&nbsp; broadcast = pullback &nbsp;·&nbsp; pmap₂ = Π-map &nbsp;·&nbsp; no sorry remains</p>
15
+ </header>
16
+
17
+ <main>
18
+ <section class="panel">
19
+ <h2>Playground</h2>
20
+ <button id="run">Run all kernels</button>
21
+ <p id="status" class="status"></p>
22
+
23
+ <div class="kernel">
24
+ <h3>pmap₂ — pointwise Π-map</h3>
25
+ <pre id="out-pmap2">…</pre>
26
+ </div>
27
+ <div class="kernel">
28
+ <h3>broadcast — pullback π : J → I</h3>
29
+ <pre id="out-broadcast">…</pre>
30
+ </div>
31
+ <div class="kernel">
32
+ <h3>softmax — Π-map normalization</h3>
33
+ <pre id="out-softmax">…</pre>
34
+ </div>
35
+ <div class="kernel">
36
+ <h3>NAND — universal gate</h3>
37
+ <pre id="out-nand">…</pre>
38
+ </div>
39
+ <div class="kernel">
40
+ <h3>attention — NAND-extracted spec</h3>
41
+ <pre id="out-attention">…</pre>
42
+ </div>
43
+ </section>
44
+
45
+ <section class="panel">
46
+ <h2>Usage Guide</h2>
47
+ <img src="assets/usage.svg" alt="Sovereign Array usage guide" class="usage" />
48
+ <h3>How to use the language</h3>
49
+ <ol>
50
+ <li><strong>Spec (Lean 4)</strong> — define arrays as dependent functions <code>Fin n → α</code>; prove <code>broadcast_is_pullback</code> and <code>softmax_is_pmap</code> with <code>lake build</code> (zero sorry).</li>
51
+ <li><strong>Kernel (C++20)</strong> — <code>#include "sovereign_array.h"</code>; build with CMake; run <code>sovarr_test</code> (11/11 checks).</li>
52
+ <li><strong>Front-end (this page)</strong> — open <code>index.html</code>; the playground runs the same denotational semantics in the browser.</li>
53
+ <li><strong>Compose</strong> — chain <code>pmap₂</code> / <code>broadcast</code> / <code>softmax</code> / <code>nand_attention</code>; fusion is Π-map fusion — no loop in the denotation.</li>
54
+ </ol>
55
+ </section>
56
+ </main>
57
+
58
+ <footer>
59
+ <p>Sovereign Array Language · 2026 · Ahmad Ali Parr &nbsp;·&nbsp; <a href="https://github.com/SNAPKITTYWEST/SNAPKITTYWEST">SNAPKITTYWEST</a></p>
60
+ </footer>
61
+
62
+ <script type="module" src="js/app.js"></script>
63
+ </body>
64
+ </html>
js/app.js ADDED
@@ -0,0 +1,61 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Front-end app logic for the Sovereign Array playground.
2
+ import { SOVArray, broadcast, softmax, nandGate, nandAttention } from "./array-lang.js";
3
+
4
+ const $ = (id) => document.getElementById(id);
5
+
6
+ function renderArray(a) {
7
+ return a.shape.join("×") + " = [" + a.data.map(x => (Math.round(x * 1000) / 1000)).join(", ") + "]";
8
+ }
9
+
10
+ function demoPmap2() {
11
+ const a = new SOVArray([2, 2], [1, 2, 3, 4]);
12
+ const b = new SOVArray([2, 2], [10, 20, 30, 40]);
13
+ const c = a.pmap2((x, y) => x + y, b);
14
+ $("out-pmap2").textContent = renderArray(c);
15
+ }
16
+
17
+ function demoBroadcast() {
18
+ const mat = new SOVArray([2, 3], [1, 2, 3, 4, 5, 6]);
19
+ const row = new SOVArray([3], [10, 20, 30]);
20
+ const bc = broadcast([2, 3], mat, row);
21
+ $("out-broadcast").textContent = renderArray(bc);
22
+ }
23
+
24
+ function demoSoftmax() {
25
+ const v = new SOVArray([4], [1, 2, 3, 4]);
26
+ const sm = softmax(v);
27
+ const sum = sm.data.reduce((a, x) => a + x, 0);
28
+ $("out-softmax").textContent = renderArray(sm) + " (Σ = " + (Math.round(sum * 1000) / 1000) + ")";
29
+ }
30
+
31
+ function demoNand() {
32
+ const rows = [
33
+ `nand(T,T) = ${nandGate(true, true)}`,
34
+ `nand(T,F) = ${nandGate(true, false)}`,
35
+ `nand(F,F) = ${nandGate(false, false)}`,
36
+ `and(T,T) = ${nandGate(nandGate(true, true), nandGate(true, true))}`,
37
+ ];
38
+ $("out-nand").textContent = rows.join("\n");
39
+ }
40
+
41
+ function demoAttention() {
42
+ const q = new SOVArray([3], [1, 0, 0]);
43
+ const k = new SOVArray([3], [1, 1, 1]);
44
+ const v = new SOVArray([3], [2, 4, 6]);
45
+ const att = nandAttention(q, k, v);
46
+ $("out-attention").textContent = renderArray(att);
47
+ }
48
+
49
+ function runAll() {
50
+ demoPmap2();
51
+ demoBroadcast();
52
+ demoSoftmax();
53
+ demoNand();
54
+ demoAttention();
55
+ $("status").textContent = "✅ All kernels executed — zero Abjad, zero digital root, zero NP-magic.";
56
+ }
57
+
58
+ window.addEventListener("DOMContentLoaded", () => {
59
+ $("run").addEventListener("click", runAll);
60
+ runAll();
61
+ });
js/array-lang.js ADDED
@@ -0,0 +1,88 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Sovereign Array Language — browser reference implementation
2
+ // Denotational model (valid isomorphisms only):
3
+ // Array I α ≃ I → α (dependent function, row-major storage)
4
+ // Shape ≃ finite type I (number[] index space)
5
+ // Broadcast ≃ pullback π : J → I
6
+ // VecOp ≃ Π-map over I
7
+ // No Abjad, no digital root, no NP-magic.
8
+
9
+ export class SOVArray {
10
+ constructor(shape, data) {
11
+ this.shape = shape;
12
+ this.data = data;
13
+ if (this.prod(shape) !== data.length)
14
+ throw new Error("SOVArray: shape/data size mismatch");
15
+ }
16
+
17
+ prod(s) { return s.reduce((a, b) => a * b, 1); }
18
+ rank() { return this.shape.length; }
19
+ size() { return this.data.length; }
20
+ raw() { return this.data.slice(); }
21
+
22
+ at(idx) { return this.data[this.stride(idx)]; }
23
+
24
+ stride(idx) {
25
+ if (idx.length !== this.shape.length) throw new Error("rank mismatch");
26
+ let off = 0, st = 1;
27
+ for (let d = this.shape.length; d-- > 0;) {
28
+ off += idx[d] * st;
29
+ st *= this.shape[d];
30
+ }
31
+ return off;
32
+ }
33
+
34
+ // pmap₂: pointwise binary op (the Π-map over the index space I)
35
+ pmap2(op, other) {
36
+ if (JSON.stringify(this.shape) !== JSON.stringify(other.shape))
37
+ throw new Error("pmap2: shape mismatch");
38
+ return new SOVArray(
39
+ this.shape,
40
+ this.data.map((x, i) => op(x, other.data[i]))
41
+ );
42
+ }
43
+ }
44
+
45
+ // Broadcasting = pullback along projection π : J → I (NumPy-style right-align)
46
+ export function broadcast(targetShape, v, w) {
47
+ const out = new Array(v.prod(targetShape)).fill(0);
48
+ const vRank = v.rank(), wRank = w.rank();
49
+ for (let flat = 0; flat < out.length; ++flat) {
50
+ const idx = unravel(flat, targetShape);
51
+ const vi = idx.slice(targetShape.length - vRank);
52
+ const wi = idx.slice(targetShape.length - wRank);
53
+ out[flat] = v.at(vi) + w.at(wi);
54
+ }
55
+ return new SOVArray(targetShape, out);
56
+ }
57
+
58
+ // Softmax as Π-map: out_i = exp(v_i) / Σ_j exp(v_j)
59
+ export function softmax(v) {
60
+ const s = v.data.reduce((a, x) => a + Math.exp(x), 0);
61
+ return new SOVArray(v.shape, v.data.map(x => Math.exp(x) / s));
62
+ }
63
+
64
+ // NAND gate — universal boolean connective
65
+ export function nandGate(a, b) { return !(a && b); }
66
+
67
+ // Attention spec over floats: scores = q·k, weights = softmax(scores), out = w·v
68
+ export function nandAttention(q, k, v) {
69
+ const n = q.shape[0];
70
+ const scores = new Array(n).fill(0).map((_, i) =>
71
+ new Array(n).fill(0).reduce((acc, _, j) => acc + q.at([i]) * k.at([j]), 0)
72
+ );
73
+ const w = softmax(new SOVArray([n], scores));
74
+ const out = new Array(n).fill(0).map((_, i) =>
75
+ new Array(n).fill(0).reduce((acc, _, j) => acc + w.at([i]) * v.at([j]), 0)
76
+ );
77
+ return new SOVArray([n], out);
78
+ }
79
+
80
+ function unravel(flat, shape) {
81
+ const idx = new Array(shape.length).fill(0);
82
+ let st = 1;
83
+ for (let d = shape.length; d-- > 0;) {
84
+ idx[d] = Math.floor(flat / st) % shape[d];
85
+ st *= shape[d];
86
+ }
87
+ return idx;
88
+ }