Deploy FieldSpace app: CNN + Attention numerators (RNS+CRT)

README.md

@@ -1,29 +1,17 @@
 ---
 title: FieldSpace — Prime-Only Machine (RNS+CRT) — Exactness Proofs
-emoji: "🧮"
-colorFrom: red
-colorTo: indigo
+emoji: 🧮
+colorFrom: blue
+colorTo: green
 sdk: gradio
 sdk_version: 4.44.0
-python_version: "3.10"
+app_file: app.py
+python: 3.10
 license: mit
-tags:
-  - number-theory
-  - residues
-  - crt
-  - integer-arithmetic
-  - exactness
-  - cnn
-  - gradio
 ---
 
-This Space demonstrates exact *integer* CNN computed entirely in residues mod `{2^K, primes}` with a single CRT reconstruction.
+This Space proves exact execution for:
+- **CNN**: Conv → ReLU/Poly → FC
+- **Attention (one head)**: exact numerators (QK>>t, then SV)
 
-### Use via API
-```python
-from gradio_client import Client
-client = Client('https://huggingface.co/spaces/jackal79/fieldspace-prime-only')
-txt, rep = client.predict('/run_cnn_proof', 0, 31, 31, 'relu', 7)
-print(txt)
-print(rep)
-```
+All ops run in residues mod `{2^K, p_i}` and reconstruct once via a batched CRT.

app.py

@@ -1,254 +1,298 @@
 
-import time, math, numpy as np, torch, gradio as gr
+import gradio as gr
+import numpy as np
 
-# deterministic CPU; keep integer-only math
-torch.set_num_threads(max(1, torch.get_num_threads()))
-DEVICE = "cpu"
-
-# ===== Core helpers =====
-def im2col_nchw_int(x, kH, kW, stride=1, pad=0):
-    N, C, H, W = x.shape
-    Hout = (H + 2*pad - kH)//stride + 1
-    Wout = (W + 2*pad - kW)//stride + 1
-    if pad:
-        x_pad = torch.zeros((N, C, H + 2*pad, W + 2*pad), dtype=x.dtype, device=x.device)
-        x_pad[:, :, pad:pad+H, pad:pad+W] = x
-    else:
-        x_pad = x
-    cols = []
-    for i in range(Hout):
-        for j in range(Wout):
-            patch = x_pad[:, :, i*stride:i*stride+kH, j*stride:j*stride+kW]
-            cols.append(patch.reshape(N, -1))
-    out = torch.stack(cols, dim=1)         # [N, Hout*Wout, C*kH*kW]
-    out = out.reshape(N*Hout*Wout, -1)     # [N*Hout*Wout, C*kH*kW]
-    return out, Hout, Wout
-
-def conv_int64_im2col(X, W, kH, kW, stride=1, pad=0):
-    Xcol, Hout, Wout = im2col_nchw_int(X, kH, kW, stride=stride, pad=pad)
-    Ycol = Xcol @ W.reshape(W.shape[0], -1).t()
-    return Ycol.reshape(X.shape[0], Hout, Wout, W.shape[0]).permute(0,3,1,2).contiguous()
-
-def poly_act_floor_int64(x, s):  # exact q = floor(x^2 / 2^s)
-    return (x * x) >> s
-
-def flatten_nchw(x): return x.reshape(x.shape[0], -1)
-def linear_int64(X, W): return X @ W
-
-# ===== RNS / CRT =====
-def choose_moduli(MAX_ABS, base_primes=None, K_cap=62):
-    # minimal K so 2^(K-1) > MAX_ABS, cap at 62 for int64 safety
-    K = min(K_cap, max(2, MAX_ABS.bit_length() + 1))
+# -----------------------------
+# Utilities: RNS + CRT
+# -----------------------------
+def pick_moduli(max_abs, primes=(257,263,269,271,277,281)):
+    # choose K so 2^(K-1) > max_abs
+    K = max(20, int(max_abs).bit_length()+1)
     MOD2 = 1 << K
-    primes = list(base_primes or [257, 263, 269, 271, 277, 281])
-    M_total = MOD2
-    for p in primes: M_total *= p
-    # ensure range
-    i = 283
-    while M_total <= 2*MAX_ABS:
-        primes.append(i)
-        M_total *= i
-        i = {283:293, 293:307, 307:311, 311:313, 313:317}.get(i, i+2)
-    return K, MOD2, primes
+    # ensure product > 2*max_abs (with plenty margin for toy sizes this is fine)
+    M = MOD2
+    ps = []
+    for p in primes:
+        ps.append(p); M *= p
+        if M > 2*max_abs: break
+    return K, MOD2, tuple(ps)
 
 def encode_rns(x, MOD2, primes):
-    outs = []
-    mask = MOD2 - 1
-    x_list = x.reshape(-1).cpu().tolist()
-    mod2_res = [(v & mask) for v in x_list]             # mod 2^K via mask (python int)
-    outs.append(torch.tensor(mod2_res, dtype=torch.int64).reshape(x.shape))
+    outs = [np.asarray(x, dtype=object) & (MOD2-1)]
     for p in primes:
-        outs.append((x % p).to(torch.int64))
-    return torch.stack(outs, dim=0)                      # [L, *shape]
+        outs.append(np.asarray(x, dtype=object) % p)
+    return np.stack(outs, axis=0)  # [L, *shape]
 
-def precompute_crt(moduli):
+def batched_crt(res, MOD2, primes):
+    # res: [L, *shape], L=1+len(primes), dtype=object (python ints)
+    moduli = (MOD2,)+tuple(primes)
+    L = res.shape[0]
     M = 1
     for m in moduli: M *= m
-    Mi = [M // m for m in moduli]
-    invMi = [pow(int(Mi[i] % moduli[i]), -1, moduli[i]) for i in range(len(moduli))]
-    return M, np.array(Mi, dtype=object), np.array(invMi, dtype=object), np.array(moduli, dtype=object)
-
-def batched_crt(res, M, Mi_np, inv_np, mods_np):
-    L = res.shape[0]
-    flat = res.reshape(L, -1).cpu().tolist()
-    N = len(flat[0])
-    out = [0]*N
-    half = M // 2
-    for k in range(N):
+    Mi = [M//m for m in moduli]
+    inv = [pow(int(Mi[i] % moduli[i]), -1, moduli[i]) for i in range(L)]
+    flat = res.reshape(L, -1)
+    out = []
+    half = M//2
+    for k in range(flat.shape[1]):
         acc = 0
         for i in range(L):
-            acc = (acc + (flat[i][k] * inv_np[i] * Mi_np[i])) % M
+            acc = (acc + (flat[i,k] * inv[i] * Mi[i])) % M
         if acc > half: acc -= M
-        out[k] = int(acc)
-    return torch.tensor(out, dtype=torch.int64).reshape(res.shape[1:])
+        out.append(int(acc))
+    return np.array(out, dtype=np.int64).reshape(res.shape[1:])
+
+# -----------------------------
+# CNN proof (tiny shapes)
+# -----------------------------
+def im2col_nchw_int(x, kH, kW, stride=1, pad=0):
+    N,C,H,W = x.shape
+    Hp = H+2*pad; Wp = W+2*pad
+    xp = np.zeros((N,C,Hp,Wp), dtype=np.int64)
+    xp[:,:,pad:pad+H, pad:pad+W] = x
+    Hout = (Hp - kH)//stride + 1
+    Wout = (Wp - kW)//stride + 1
+    cols = []
+    for i in range(Hout):
+        for j in range(Wout):
+            patch = xp[:,:,i*stride:i*stride+kH, j*stride:j*stride+kW]
+            cols.append(patch.reshape(N,-1))
+    out = np.stack(cols, axis=1)   # [N, Hout*Wout, C*kH*kW]
+    out = out.reshape(N*Hout*Wout, -1)
+    return out, Hout, Wout
 
-# ===== RNS ops =====
-def conv_rns(Xr, Wr, kH, kW, stride, pad, mods_np):
+def conv_ref(X, W, kH, kW, stride=1, pad=0):
+    N,C,H,W = X.shape
+    Cout,Cin,KH,KW = W.shape
+    Xcol,Hout,Wout = im2col_nchw_int(X,kH,kW,stride,pad)
+    Ycol = Xcol @ W.reshape(Cout,-1).T
+    Y = Ycol.reshape(N,Hout,Wout,Cout).transpose(0,3,1,2).copy()
+    return Y
+
+def relu_ref(x): return np.where(x<0, 0, x)
+def poly_ref(x, s): return (x*x) >> s
+def linear_ref(X, W): return X @ W
+
+def relu_rns(Xr, MOD2, primes):
+    # Xr: [L, *shape]
     L = Xr.shape[0]
-    Ys = []
-    for i in range(L):
-        mod = int(mods_np[i])
-        X_i = Xr[i]
-        W_i = Wr[i].reshape(Wr[i].shape[0], -1)
-        Xcol, Hout, Wout = im2col_nchw_int(X_i.to(torch.int64), kH, kW, stride=stride, pad=pad)
-        Ycol = (Xcol @ W_i.t()) % mod
-        Y    = Ycol.reshape(X_i.shape[0], Hout, Wout, W_i.shape[0]).permute(0,3,1,2).contiguous()
-        Ys.append(Y.to(torch.int64))
-    return torch.stack(Ys, dim=0)  # [L,B,Cout,H,W]
-
-def relu_rns(Yr, MOD2, primes, K):
-    # Use sign from 2^K residue: negative iff top bit set.
-    L = Yr.shape[0]
-    y2k = Yr[0] & (MOD2 - 1)
-    neg = ((y2k >> (K-1)) & 1).to(torch.int64)          # 1 if negative else 0
-    keep = 1 - neg                                      # 0 or 1
+    K = MOD2.bit_length()-1
+    x2 = Xr[0]
+    mask = (x2 < (1<<(K-1))).astype(np.int64)  # 1 if non-negative, else 0
     out = []
-    out.append((y2k * keep) & (MOD2 - 1))
-    for i, p in enumerate(primes, start=1):
-        out.append((Yr[i] * keep) % p)
-    return torch.stack(out, dim=0)
+    out.append((x2 * mask) & (MOD2-1))
+    for i,p in enumerate(primes, start=1):
+        out.append((Xr[i] * mask) % p)
+    return np.stack(out, axis=0)
 
-def poly_act_floor_rns(Yr, shift, MOD2, primes):
-    mask = (1 << shift) - 1
+def poly_rns(Xr, s, MOD2, primes):
+    # q = floor(x^2 / 2^s)
+    mask_s = (1<<s)-1
+    out = []
     # 2^K channel
-    y2_2 = (Yr[0] * Yr[0]) & (MOD2 - 1)
-    q2   = (y2_2 >> shift) & (MOD2 - 1)
-    # remainder from low bits only
-    y_low = (Yr[0] & mask).to(torch.int64)
-    r_low = (y_low * y_low) & mask
-    out = [q2.to(torch.int64)]
-    for p_idx, p in enumerate(primes, start=1):
-        y2p = (Yr[p_idx] * Yr[p_idx]) % p
-        rp  = (r_low % p)
-        inv_pow2 = pow(2, -shift, p)
-        qi  = ((y2p - rp) * inv_pow2) % p
-        out.append(qi.to(torch.int64))
-    return torch.stack(out, dim=0)
-
-def linear_rns(Xr, Wr, mods_np):
+    y2 = (Xr[0]*Xr[0]) & (MOD2-1)
+    q2 = (y2 >> s) & (MOD2-1)
+    out.append(q2)
+    # r from low s bits of x only
+    low = Xr[0] & mask_s
+    r = (low*low) & mask_s
+    for i,p in enumerate(primes, start=1):
+        y2p = (Xr[i]*Xr[i]) % p
+        inv = pow(2, -s, p)
+        qi = ((y2p - (r % p)) * inv) % p
+        out.append(qi)
+    return np.stack(out, axis=0)
+
+def matmul_rns(Ar, Br, MOD2, primes):
+    # Ar: [L, M, K], Br: [L, K, N] -> [L, M, N]
+    outs=[]
+    outs.append((Ar[0] @ Br[0]) & (MOD2-1))
+    for i,p in enumerate(primes, start=1):
+        outs.append((Ar[i] @ Br[i]) % p)
+    return np.stack(outs, axis=0)
+
+def conv_rns(Xr, Wr, kH, kW, stride=1, pad=0, MOD2=0, primes=()):
+    # reshape per-modulus and reuse im2col on ints
     L = Xr.shape[0]
-    Ys = []
+    N,C,H,W = Xr[0].shape
+    Cout = Wr[0].shape[0]
+    Ymods=[]
     for i in range(L):
-        mod = int(mods_np[i])
-        Ys.append((Xr[i] @ Wr[i]) % mod)
-    return torch.stack(Ys, dim=0)
-
-# ===== CNN proof (Conv -> Act -> Conv -> Act -> FC) =====
-def run_cnn_proof(seed:int=0, x_abs:int=31, w_abs:int=31, act_kind:str="relu", shift:int=7):
-    B, Cin, H, W = 4, 1, 16, 16
-    C1, C2       = 8, 8
-    KH, KW       = 3, 3
-    STRIDE, PAD  = 1, 1
-    CLS          = 10
-
-    g = torch.Generator().manual_seed(int(seed))
-    X   = torch.randint(-x_abs, x_abs+1, (B, Cin, H, W), dtype=torch.int64, generator=g)
-    W1  = torch.randint(-w_abs, w_abs+1, (C1, Cin, KH, KW), dtype=torch.int64, generator=g)
-    W2  = torch.randint(-w_abs, w_abs+1, (C2, C1,  KH, KW), dtype=torch.int64, generator=g)
-    Wfc = torch.randint(-w_abs, w_abs+1, (C2*H*W, CLS),     dtype=torch.int64, generator=g)
-
-    t0 = time.time()
-    Y1_ref = conv_int64_im2col(X,  W1, KH, KW, stride=STRIDE, pad=PAD)
-    A1_ref = (Y1_ref.clamp_min(0) if act_kind=="relu" else poly_act_floor_int64(Y1_ref, shift))
-    Y2_ref = conv_int64_im2col(A1_ref, W2, KH, KW, stride=STRIDE, pad=PAD)
-    A2_ref = (Y2_ref.clamp_min(0) if act_kind=="relu" else poly_act_floor_int64(Y2_ref, shift))
-    Z_ref  = linear_int64(A2_ref.reshape(B, -1), Wfc)
-    t1 = time.time()
-    ref_ms = (t1 - t0)*1000
-
-    # bounds
-    def bconv(cin, k, xmax, wmax): return int(cin*k*k * xmax * wmax)
-    b1 = bconv(Cin, KH, x_abs, w_abs)
-    a1 = (b1*b1) >> (shift if act_kind=="poly" else 0)
-    b2 = int(C1*KH*KH * a1 * w_abs)
-    a2 = (b2*b2) >> (shift if act_kind=="poly" else 0)
-    fc = int((C2*H*W) * a2 * w_abs)
-    MAX_ABS = max(b1,a1,b2,a2,fc)
-
-    K, MOD2, primes = choose_moduli(MAX_ABS)
-    moduli = [MOD2] + primes
-    M, Mi_np, inv_np, mods_np = precompute_crt(moduli)
-
-    # encode & run RNS
-    X_r   = encode_rns(X,   MOD2, primes)
-    W1_r  = encode_rns(W1,  MOD2, primes)
-    W2_r  = encode_rns(W2,  MOD2, primes)
-    Wfc_r = encode_rns(Wfc, MOD2, primes)
-
-    Y1_r = conv_rns(X_r,  W1_r, KH, KW, STRIDE, PAD, mods_np)
-    A1_r = (relu_rns(Y1_r, MOD2, primes, K) if act_kind=="relu" else poly_act_floor_rns(Y1_r, shift, MOD2, primes))
-    Y2_r = conv_rns(A1_r, W2_r, KH, KW, STRIDE, PAD, mods_np)
-    A2_r = (relu_rns(Y2_r, MOD2, primes, K) if act_kind=="relu" else poly_act_floor_rns(Y2_r, shift, MOD2, primes))
-    t2 = time.time()
-    Z_r  = linear_rns(A2_r.reshape(len(moduli), B, -1), Wfc_r, mods_np)
-    Z_rec= batched_crt(Z_r, M, Mi_np, inv_np, mods_np)
-    t3 = time.time()
-    rns_ms = (t3 - t2)*1000
-
-    # checks
-    flags = {
-        "conv1": bool(torch.equal(batched_crt(Y1_r, M, Mi_np, inv_np, mods_np), Y1_ref)),
-        "act1":  bool(torch.equal(batched_crt(A1_r, M, Mi_np, inv_np, mods_np), A1_ref)),
-        "conv2": bool(torch.equal(batched_crt(Y2_r, M, Mi_np, inv_np, mods_np), Y2_ref)),
-        "act2":  bool(torch.equal(batched_crt(A2_r, M, Mi_np, inv_np, mods_np), A2_ref)),
-        "final": bool(torch.equal(Z_rec, Z_ref)),
-        "argmax": bool(torch.equal(Z_rec.argmax(1), Z_ref.argmax(1))),
-    }
+        Xi = Xr[i].astype(object)
+        Wi = Wr[i].astype(object)
+        Xcol,Hout,Wout = im2col_nchw_int(np.asarray(Xi, dtype=np.int64), kH,kW,stride,pad)
+        Wcol = np.asarray(Wi.reshape(Cout,-1), dtype=np.int64)
+        if i==0:
+            MOD = MOD2
+            Ycol = (Xcol @ Wcol.T) & (MOD-1)
+        else:
+            p = primes[i-1]
+            Ycol = (Xcol @ Wcol.T) % p
+        Y = Ycol.reshape(N,Hout,Wout,Cout).transpose(0,3,1,2).copy()
+        Ymods.append(Y.astype(object))
+    return np.stack(Ymods, axis=0)
+
+def cnn_proof(seed, xmax, wmax, activation, shift):
+    # Tiny shapes to keep it snappy
+    B,Cin,H,W = 2,1,8,8
+    Cout = 2
+    KH=KW=3
+    CLS=8
+    rng = np.random.default_rng(seed)
+    X   = rng.integers(-xmax, xmax+1, size=(B,Cin,H,W), dtype=np.int64)
+    Wc  = rng.integers(-wmax, wmax+1, size=(Cout,Cin,KH,KW), dtype=np.int64)
+    Wfc = rng.integers(-wmax, wmax+1, size=(Cout*H*W, CLS), dtype=np.int64)
+
+    # Reference (int64)
+    Y = conv_ref(X,Wc,KH,KW,1,1)
+    A = relu_ref(Y) if activation=="relu" else poly_ref(Y, shift)
+    Z = linear_ref(A.reshape(B,-1), Wfc)
 
-    console = []
-    console.append("Stage-by-stage equality (exact):")
-    console.append(f"conv1 : {'✅' if flags['conv1'] else '❌'}")
-    console.append(f"act1  : {'✅' if flags['act1']  else '❌'}")
-    console.append(f"conv2 : {'✅' if flags['conv2'] else '❌'}")
-    console.append(f"act2  : {'✅' if flags['act2']  else '❌'}")
-    console.append(f"final : {'✅' if flags['final'] else '❌'}")
-    console.append(f"Argmax match: {flags['argmax']} (ref={Z_ref.argmax(1).tolist()}, prime={Z_rec.argmax(1).tolist()})")
-    console.append("")
-    console.append("Timing (ms):")
-    console.append(f"  Reference int64 path: {ref_ms:.2f} ms")
-    console.append(f"  Prime-only RNS+CRT  : {rns_ms:.2f} ms")
-    console.append("")
-    console.append("Bit budget:")
-    console.append(f"  K={K}  (2^(K-1)={1<<(K-1):,} > MAX_ABS={MAX_ABS:,})")
-    console.append(f"  Odd primes: {primes}")
-    console.append(f"  Composite modulus M_total = {int(M):,}")
+    # Bounds (very conservative)
+    b1 = int(Cin*KH*KW * xmax * wmax)
+    a1 = b1 if activation=="relu" else (b1*b1)>>shift
+    b2 = int(Cout*KH*KW * a1 * wmax)
+    a2 = b2 if activation=="relu" else (b2*b2)>>shift
+    fc = int((Cout*H*W) * a2 * wmax)
+    MAX_ABS = max(abs(b1),abs(a1),abs(b2),abs(a2),abs(fc), 1)
+
+    K, MOD2, primes = pick_moduli(max_abs=MAX_ABS)
+    # Encode
+    Xr  = encode_rns(X, MOD2, primes)
+    Wcr = encode_rns(Wc, MOD2, primes)
+    Wfr = encode_rns(Wfc, MOD2, primes)
+
+    # RNS path
+    Yr = conv_rns(Xr,Wcr,KH,KW,1,1,MOD2,primes)
+    Ar = relu_rns(Yr, MOD2, primes) if activation=="relu" else poly_rns(Yr, shift, MOD2, primes)
+    Arf = Ar.reshape(Ar.shape[0], B, -1)
+    Zr  = matmul_rns(Arf, Wfr, MOD2, primes)
+    Zrec= batched_crt(Zr, MOD2, primes)
+
+    ok = np.array_equal(Z, Zrec)
+    arg = np.array_equal(Z.argmax(1), Zrec.argmax(1))
+
+    log = []
+    log.append("Stage-by-stage equality (exact):")
+    log.append(f"conv : {'✅' if np.array_equal(batched_crt(Yr,MOD2,primes), Y) else '❌'}")
+    log.append(f"act  : {'✅' if np.array_equal(batched_crt(Ar,MOD2,primes), A) else '❌'}")
+    log.append(f"fc   : {'✅' if ok else '❌'}")
+    log.append(f"Argmax match: {arg} (ref={Z.argmax(1).tolist()}, prime={Zrec.argmax(1).tolist()})")
 
     report = {
-        "ok": flags["final"],
-        "argmax_ok": flags["argmax"],
-        "act": act_kind,
+        "activation": activation,
         "shift": int(shift),
-        "seed": int(seed),
-        "x_abs": int(x_abs),
-        "w_abs": int(w_abs),
         "K": int(K),
-        "primes": primes,
-        "ref_ms": ref_ms,
-        "rns_ms": rns_ms,
+        "primes": list(map(int,primes)),
+        "exact": bool(ok),
+        "argmax_exact": bool(arg),
+        "ref_logits_sample": Z[0,:min(8,CLS)].tolist(),
+        "rec_logits_sample": Zrec[0,:min(8,CLS)].tolist(),
+    }
+    return "\n".join(log), report
+
+# -----------------------------
+# Attention (exact numerators)
+# -----------------------------
+def attn_numerators_proof(seed):
+    rng = np.random.default_rng(seed)
+    T,d = 2,4
+    xmax = 15
+    t = 7  # scale shift
+
+    Q = rng.integers(-xmax,xmax+1,size=(T,d),dtype=np.int64)
+    K_ = rng.integers(-xmax,xmax+1,size=(T,d),dtype=np.int64)
+    V = rng.integers(-xmax,xmax+1,size=(T,d),dtype=np.int64)
+
+    Sraw = Q @ K_.T
+    S = Sraw >> t   # exact floor
+    N = S @ V       # numerators
+
+    # conservative bound
+    s_max = int((d * xmax * xmax) >> t)
+    n_max = int(T * s_max * xmax)
+    Kpow, MOD2, primes = pick_moduli(max_abs=max(abs(s_max),abs(n_max),1))
+
+    Qr  = encode_rns(Q,MOD2,primes)
+    Kr  = encode_rns(K_,MOD2,primes)
+    Vr  = encode_rns(V,MOD2,primes)
+
+    # Sraw_r and S_r
+    Sraw_r = matmul_rns(Qr, Kr.transpose(0,2,1), MOD2, primes)
+    # floor by right shift in 2^K channel + multiplicative inverse in odd primes
+    # (here scaling is power-of-two so we can just shift in 2^K, and multiply by inv(2^t) after peeling low bits = 0)
+    # since we already floored by pure shift in reference, it's safe to do:
+    Sr = []
+    Sr.append( (Sraw_r[0] >> t) & (MOD2-1) )
+    invs = [pow(2,-t,p) for p in primes]
+    for i,p in enumerate(primes, start=1):
+        Sr.append( (Sraw_r[i] * invs[i-1]) % p )
+    Sr = np.stack(Sr, axis=0)
+
+    Nr = matmul_rns(Sr, Vr, MOD2, primes)
+    Srec = batched_crt(Sr, MOD2, primes)
+    Nrec = batched_crt(Nr, MOD2, primes)
+
+    okS = np.array_equal(S, Srec)
+    okN = np.array_equal(N, Nrec)
+
+    log = []
+    log.append("Attention (exact numerators):")
+    log.append(f"S  : {'✅' if okS else '❌'}")
+    log.append(f"SV : {'✅' if okN else '❌'}")
+
+    report = {
+        "K": int(Kpow),
+        "primes": list(map(int,primes)),
+        "S_exact": bool(okS),
+        "N_exact": bool(okN),
+        "S_sample": S.tolist(),
+        "Srec_sample": Srec.tolist(),
+        "N_sample": N.tolist(),
+        "Nrec_sample": Nrec.tolist(),
     }
-    return "\n".join(console), report
-
-# ===== Gradio UI =====
-with gr.Blocks(title="FieldSpace — Prime-Only Machine (RNS+CRT) — Exactness Proofs") as demo:
-    gr.Markdown("## FieldSpace — Prime-Only Machine (RNS+CRT) — Exactness Proofs")
-    gr.Markdown(
-        "This demo runs **exact integer CNN** computations entirely in residues mod `{2^K, primes}` "
-        "and reconstructs with a single CRT, verifying bit-for-bit equality against an int64 reference."
-    )
-
-    with gr.Row():
-        seed  = gr.Number(value=0, label="Seed", precision=0)
-        xabs  = gr.Number(value=31, label="|X|max", precision=0)
-        wabs  = gr.Number(value=31, label="|W|max", precision=0)
-    with gr.Row():
-        act   = gr.Radio(choices=["relu","poly"], value="relu", label="Activation")
-        shift = gr.Slider(1, 14, value=7, step=1, label="SHIFT (for poly x^2 >> SHIFT)")
-
-    run_btn = gr.Button("Run CNN Proof", variant="primary")
-    console = gr.Textbox(label="Console", lines=16)
-    report  = gr.JSON(label="JSON Report")
-
-    run_btn.click(fn=run_cnn_proof, inputs=[seed, xabs, wabs, act, shift], outputs=[console, report], api_name="/run_cnn_proof")
+    return "\n".join(log), report
+
+# -----------------------------
+# Gradio UI
+# -----------------------------
+with gr.Blocks(title="FieldSpace — Prime-Only Machine (RNS+CRT)") as demo:
+    gr.Markdown("# FieldSpace — Prime-Only Machine (RNS+CRT) — Exactness Proofs")
+    gr.Markdown("This demo proves exactness for a tiny CNN and a one-head attention numerator block using only residues mod $\\{2^K, p_i\\}$ and a single CRT.")
+    with gr.Tab("CNN (Conv + ReLU/Poly + FC)"):
+        with gr.Row():
+            seed = gr.Number(value=0, precision=0, label="Seed")
+            xmax = gr.Number(value=31, precision=0, label="|X|max")
+            wmax = gr.Number(value=31, precision=0, label="|W|max")
+        activation = gr.Radio(choices=["relu","poly"], value="relu", label="Activation")
+        shift = gr.Slider(1,12,value=7,step=1,label="SHIFT for poly (x^2 >> SHIFT)")
+        run_btn = gr.Button("Run CNN Proof", variant="primary")
+        out_text = gr.Textbox(label="Console", lines=10)
+        out_json = gr.JSON(label="JSON Report")
+        run_btn.click(fn=lambda a,b,c,d,e: cnn_proof(int(a),int(b),int(c),d,int(e)),
+                      inputs=[seed,xmax,wmax,activation,shift],
+                      outputs=[out_text,out_json])
+    with gr.Tab("Attention (Exact Numerators)"):
+        aseed = gr.Number(value=0, precision=0, label="Seed")
+        runA = gr.Button("Run Attention Proof", variant="secondary")
+        AT = gr.Textbox(label="Console", lines=8)
+        AJ = gr.JSON(label="JSON Report")
+        runA.click(fn=lambda s: attn_numerators_proof(int(s)),
+                   inputs=[aseed], outputs=[AT,AJ])
+    gr.Markdown("**Use via API**")
+    gr.Code("""from gradio_client import Client
+client = Client('https://huggingface.co/spaces/jackal79/fieldspace-prime-only')
+txt, rep = client.predict('/run_cnn_proof', 0, 31, 31, 'relu', 7)""")
+
+# Named routes for programmatic calls
+demo.load(None, None, None)
+demo.add_named_endpoint("/run_cnn_proof", cnn_proof, inputs=[
+    gr.Number(precision=0), gr.Number(precision=0), gr.Number(precision=0),
+    gr.Textbox(), gr.Number(precision=0)
+], outputs=[gr.Textbox(), gr.JSON()])
+demo.add_named_endpoint("/run_attn_proof", attn_numerators_proof,
+                        inputs=[gr.Number(precision=0)],
+                        outputs=[gr.Textbox(), gr.JSON()])
 
 if __name__ == "__main__":
-    demo.launch()
+    demo.queue().launch()

requirements.txt

@@ -1,4 +1,2 @@
-gradio>=4.44,<5
+gradio>=4.44.0
 numpy>=1.24
-torch==2.3.1
---extra-index-url https://download.pytorch.org/whl/cpu