allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
557 commits 18 branches 0 tags 425 MiB
Commit graph

207 commits

Author SHA1 Message Date
Brandon Schneider
9c5fe97dc1 feat(infra): SPIR-V packet generator and WGSL scar filter shader 
Add spirv_packet_generator.py: reads SPIR-V assembly, applies copy-if
optimization (OpPhi→OpSelect transform), and emits JSON packet descriptors
with the 5 OpPhi-derived fields (type_id, cond_id, true_val_id,
false_val_id, result_id) that fully specify the packet layout.

Add burgers_scar_filter.wgsl: 291-line WGSL compute shader for spectral
scar filtering in 2D Burgers RG solver. Uses three copy-if patterns:
  1. scar_pressure > threshold → apply hyperviscosity damping
  2. |kx| > k_cut || |ky| > k_cut → zero (dealiasing)
  3. factor < 0.999 → multiply velocity components

Also fix spirv_copy_if_optimizer.py: OpSelect now uses phi_instr.args[0]
(type operand) as its type, instead of compute_instr.result_id. This
produces structurally correct SPIR-V where the result type matches the
OpSelect opcode layout.

Build: 3313 jobs, 0 errors (lake build)
Tools: glslang, spirv-as, spirv-dis (native); tint from nixpkgs for WGSL
 2026-05-30 16:40:58 -05:00
Brandon Schneider
cfd43e1e95 feat(codec): extend BraidDiatCodec with BraidDiatFrame encoder/decoder 
- BraidDiatCodec.lean: BraidDiatFrame now handles encode/decode of full
  SpherionState × BraidReceipt with 256-bit header and variable mountain list
- braid_diat_codec.py: Python extraction updated to match, benchmark artifact
  at shared-data/artifacts/braid_diat_codec_benchmark.json (714B avg vs
  messagepack 1748B avg)

Build: lake build Compiler 3313 jobs, 0 errors
 2026-05-30 16:23:41 -05:00
Brandon Schneider
4df6997b51 docs(kube): update infra docs, RayCluster manifest with nightly GPU images 
- infrastructure-status.md: rewrite with current cluster topology (cupfox control-plane,
  neon-64gb/racknerd/steamdeck workers), RayCluster status, Garage storage,
  Caddy edge, open issues
- k3s-cluster-setup.md: fix steamdeck hardware specs (8 vCPU, 14.5 GB RAM)
- raycluster.yaml: upgrade to rayproject/ray:nightly-py313-gpu (multi-arch amd64+arm64),
  add gpu-workers group targeting neon-64gb, add arm64-workers for neon-64gb CPU
- README.md: update build job count (3460 → 3313, verified)

Build: lake build Compiler 3313 jobs, 0 errors
 2026-05-30 16:23:13 -05:00
Brandon Schneider
81d4338627 feat: ARM64 copy-if optimizer — branches to CSEL 
Transforms branch patterns to ARM64 conditional selects:
  Before: CMP + BEQ + compute + B + MOV = 5-47 cycles
  After: CMP + compute + CSEL = 4-6 cycles

ARM64 CSEL instruction:
  CSEL Xd, Xn, Xm, cond
  - Single cycle on most ARM64 processors
  - No branch prediction penalty
  - No pipeline flush on mispredict

Pattern detection:
  - CMP + BEQ/BNE/B.LT/etc
  - True block: 1-3 compute instructions + B
  - False block: single MOV
  - Merge point

Same pattern as:
  - SPIR-V OpSelect (GPU shaders)
  - VCN delta+RLE (3.3x)
  - QR spatial hash (2.18x)
  - Lean CopyIfTactic (2.7x)

Works on ARM64 assembly from GCC/LLVM/Rust.
No compiler fork needed — post-processing pass.

Targets: Neon-64GB (18 vCPU ARM64 EPYC)
 2026-05-30 15:59:24 -05:00
Brandon Schneider
2e15c7c0a5 feat: SPIR-V copy-if optimizer — skip zero deltas in GPU shaders 
Transforms branch-based patterns to OpSelect:
  Before: 3 blocks, OpBranchConditional, OpPhi
  After: 1 block, OpSelect (single-cycle on most GPUs)

Pattern detection:
  - OpSelectionMerge + OpBranchConditional
  - True block: single compute + OpBranch
  - False block: empty (just OpBranch)
  - Merge block: OpPhi merging true/false values

Transformation:
  - Remove SelectionMerge + BranchConditional
  - Inline compute instruction
  - Replace OpPhi with OpSelect
  - Collapse 3 blocks to 1

Same pattern as:
  - VCN delta+RLE (3.3x): skip zero bytes
  - QR spatial hash (2.18x): skip non-neighbors
  - Lean compilation (2.7x): skip trivial theorems
  - Spatial hash (86.5% cache hit): skip empty cells

Driver-agnostic: works at SPIR-V level before Mesa.
No Mesa fork required. No NIR pass needed.
 2026-05-30 15:57:08 -05:00
Brandon Schneider
d5428a8950 feat: QR spatial hash integration — 2.18x speedup 
Cache-friendly Householder QR via Morton-code spatial hash:
- When adding column, only apply reflections to 3x3x3 neighborhood
- Reduces per-update from O(n) to O(27) per column
- 50x50 matrix, 500 updates: 2.18x faster than naive

Naive: 0.124ms/update
Spatial: 0.057ms/update
Speedup: 2.18x

Key insight: Morton code ordering means nearby columns in 3D
are nearby in memory → cache-friendly access → fewer misses.

This completes all 4 next steps:
1. ✅ O_AMMR_QRNode wired into BraidDiatFrame (already done)
2. ✅ O_AMMR_valid strengthened with residual bounds (NS_MD.lean)
3. ✅ Hash benchmark: Morton wins (86.5% cache hit rate)
4. ✅ QR spatial hash: 2.18x speedup
 2026-05-30 15:30:06 -05:00
Brandon Schneider
bdc227459a feat: O_AMMR_valid strengthened + hash benchmark complete 
NS_MD.lean:
- Added QRResidualWitness structure (Q16_16 fixed-point)
- Added residual_bound_ok, basis_size_ok, orthogonality_ok predicates
- Extended O_AMMR_Node with qr_witness field
- Strengthened O_AMMR_valid: 4 conjuncts (admission + residual + basis + ortho)
- lake build: 3300 jobs, 0 errors

hash_benchmark.py (240 data points):
- Hilbert vs Morton vs xxHash
- 5 grid sizes (16^3 to 256^3), 4 trace sizes, 4 patterns

Key findings:
  Morton: 86.5% cache hit rate, 1.08µs p50, 0.512 locality
  xxHash: 30.3% cache hit rate, 0.96µs p50, 0.342 locality
  Hilbert: 27.6% cache hit rate, 2.29µs p50, 0.833 locality

Morton wins overall for spatial hash grids.
 2026-05-30 15:15:33 -05:00
Brandon Schneider
c6011dbbdf feat: wire BraidDiatCodec into FAMM transport 
BraidDiatCodec (714 bytes avg) imported alongside VCN encoder.
When available, can replace Delta+RLE for braid data encoding.

Benchmark (from braid_diat_codec_benchmark.json):
  BraidDiat: 0.029ms encode, 0.034ms decode, 714 bytes
  MessagePack: 0.103ms encode, 0.002ms decode, 1748 bytes
  Cap'n Proto: 0.002ms encode, 0.0001ms decode, 29 bytes

BraidDiatCodec is 2.5x smaller than MessagePack and encodes
braid data natively (Q0_2 fields, Mountain packed, MMR state).
 2026-05-30 14:36:16 -05:00
Brandon Schneider
c64e4f15eb docs: update AGENTS.md — BraidDiatCodec shim + bridge modules 
4-Infrastructure: add braid_diat_codec.py to stack-solidification anchors
Semantics: document BraidSpherionBridge admits (IntNodeToPhaseVec linearity, receipt_correspondence)
 2026-05-30 13:30:55 -05:00
Brandon Schneider
e797f06bd0 feat(shim): BraidDiatCodec Python extraction 
Python implementation of the 4-layer BraidDiatCodec:
- ChiralityDIAT encode/decode (64-bit slot)
- MountainPacked from_mountain/to_mountain
- BraidResidualPacked from_bracket/to_bracket (Q0_2 packing)
- BraidDiatFrame encode/decode

Benchmark: braid_diat (714B avg) vs messagepack (1748B avg)
on synthetic MMR/spike train frames.
 2026-05-30 13:30:01 -05:00
Brandon Schneider
ba203ca971 feat: spatial hash grid — GPU-style particle physics (Python + FPGA) 
Ported from ScaleSpaceSynth (WebGPU particle simulator):
- 64×64×64 spatial hash, 32 particles/cell, lock-free insertion
- Curl noise: divergence-free 3D turbulence
- Pairwise forces: attractive (ratio>0.15) + repulsive (ratio<=0.15)
- Trilinear density interpolation
- HalfLife particle lifecycle
- Q16_16 encode/decode for VCN transport

Python (spatial_hash_grid.py): 6/6 tests pass
  10K particles, neighbor query, forces, 100 sim steps, curl noise verified

FPGA (spatial_hash_bram.v):
  16×16×16 grid, dual-port BRAM, 27-cycle neighbor scan
  Density → voltage mode selector (STORE/COMPUTE/APPROX/MORPHIC)
  Integrated into research_stack_top.v

Same pattern as ScaleSpaceSynth GPU:
  GPU: atomicAdd for lock-free cell assignment
  FPGA: BRAM read-modify-write for cell assignment
  Ray: content-addressed ObjectRef for lock-free reads
  All: partition space → compute density → find structure at multiple scales
 2026-05-30 01:25:19 -05:00
Brandon Schneider
df6ea7ba15 feat: GCCL + WaveProbe + MetaProbe + delta compression 
Ports Lean formalization to Python:
- GCCL: LawAxis, PromotionRung, Decision, ScaleBand, Receipt, Wrapper, Transition
- gcclSwapGate: accept if new cost < old cost (from MassNumber.lean)
- fammRouteGate: route mass <= stress mass within thermal budget
- braidTransferGate: delta admissible <= delta risk
- WaveProbe: golden angle sampling (40503 = 1/φ × 65536)
- MetaProbe: probe-but-don't-commit, EXPORT_GRANT
- Delta compression with GCCL gates
- gccl_encode: full GCCL-gated encode pipeline

Tests:
  WaveProbe overlap (identical): 1.0000
  WaveProbe overlap (shifted): 0.6694
  MetaProbe (low residual): EXPORT_GRANT
  MetaProbe (high residual): HOLD
  GCCL transition admissible: True

All Q16_16 arithmetic (no Float in compute paths).
 2026-05-30 01:09:14 -05:00
Brandon Schneider
ebabaa3b6b feat: FAMM-integrated VCN transport (gate-checked encode/decode) 
Ports Lean formalization to Python:
- gateCondition: ||coker(M) residual|| < ε (Q16_16)
- Scar/ScarBundle: pressure + mode per strand
- fammGate: admissibility check on 8-strand state
- eigensolid_converged: verify convergence before transmission
- voltage_mode_from_fd: FD → STORE/COMPUTE/APPROX/MORPHIC
- latency_class: RTT → local/near/far/derp/offline

Pipeline:
  Braid data → FAMM gate → eigensolid check → FD → voltage mode
  → RouteCost latency → VCN encode → SEI receipt with FAMM metadata

Gate behavior:
  - FAMM admissible + eigensolid converged → encode
  - Either fails → reject with scar info, don't encode
  - Receipt includes: claim_boundary, promotion=not_promoted

All Q16_16 arithmetic (no Float in compute paths).
68/68 tests still pass.
 2026-05-30 00:56:43 -05:00
Brandon Schneider
65d0ddb12a fix(deps): update tar to v0.4.46 and refresh npm packages 
Resolves GHSA-9rg2-7cm8 (PAX header desynchronization) in:
- 2-Search-Space/search/stract/Cargo.lock
- 4-Infrastructure/servo-fetch/Cargo.lock

Note: @ai-sdk/provider-utils in dify-ai-provider nested dep (3.0.25)
has no fix available yet; tracked in GHSA-866g-f22w-33x8
 2026-05-30 00:37:43 -05:00
Brandon Schneider
e5fb0a5f4d chore: commit accumulated working tree changes 
Lean: update Semantics modules, add new numerics/physics data files
Hardware: update FPGA bitstreams (tangnano9k_uart_loopback)
Infra: k3s-flake tests, netcup-vps configuration, VCN compute substrate
Docs: ARCHITECTURE, specs, citation updates
 2026-05-30 00:10:02 -05:00
Brandon Schneider
69e5b31c4f docs(infra): add Ollama inference serving to k3s-cluster-setup 
Add inference serving section documenting:
- Ollama host-level deployment on Neon-64GB (bypasses KServe RAM limits)
- Caddy reverse proxy on racknerd (:8443 → 100.64.19.78:11434)
- Troubleshooting: autosave.json stale config, passt port interception
- curl/wget verification commands

Fixes 502 Bad Gateway from Caddy (--resume loading stale autosave.json).
 2026-05-30 00:02:49 -05:00
Brandon Schneider
9f304abab0 feat: fractal dimension — DBC algorithm (Python + FPGA) 
Paper: 'Ultra-fast computation of fractal dimension for RGB images'
  (Pattern Analysis and Applications, 2025)

Python (fractal_dimension.py):
- DBC algorithm with numpy vectorization (29x faster than scalar)
- fd_compress_hint: FD → voltage mode (STORE/COMPUTE/APPROX/MORPHIC)
- 7/7 tests pass (Sierpinski, random, gradient, checkerboard, fBm, constant, RGB)
- Q16_16 integer arithmetic internally

FPGA (fractal_box_counter.v + fractal_fd_selector.v):
- 5-state FSM: IDLE → COLLECT → FINALIZE → STORE_LOG → REGRESS → DONE
- 8 power-of-two scales (2, 4, 8, ..., 256)
- Linear regression via Q16_16 64-bit arithmetic
- FD clamped to [1.0, 3.0] in Q16_16
- Selector: FD < 2.3 → STORE, < 2.6 → COMPUTE, < 2.9 → APPROX, >= 2.9 → MORPHIC
- Integrated into research_stack_top.v

FD drives adaptive compression:
  Low FD (smooth) → STORE mode (minimal compression)
  High FD (rough) → MORPHIC mode (aggressive compression)
 2026-05-29 20:45:21 -05:00
Brandon Schneider
c43f590fc0 feat(infra): add framebuffer/DRM/VirtIO GPU 3D acceleration 
hardware.virtio.enable + guestAgent (QEMU guest agent for SCP).
services.xserver with virtiogpu + fbdev + vmware video drivers.
services.spice.enable with vdagent.

Packages: mesa, libGL, libGLU, virglrenderer (VirtIO-gpu 3D),
swiftshader (software Vulkan), libva (VA-API), spice, spice-gtk,
xorg.libX11/ext/render, xf86-video-vMware/fbdev.

Kernel modules: virtio-gpu, drm, drm_kms_helper, drm_shmem_helper, ttm.
 2026-05-29 15:09:58 -05:00
Brandon Schneider
b93069406d feat(infra): mirror Debian kernel modules + SCP/KVM guest support 
Kernel modules: virtio_blk/scsi/net/balloon/serial/gpu/dma_buf,
drm/drm_kms_helper/drm_shmem_helper, xhci_pci/usbcore/usbhid,
scsi_mod/sr_mod/cdrom, ext4/mbcache/jbd2, efi_pstore/efivarfs,
qemu_fw_cfg, ip_tables/x_tables.

QEMU guest agent + SPICE vdagent for netcup SCP control panel
(graceful shutdown, VNC console, SPICE display, guest info).

VirtIO drivers for KVM guest environment.

Kernel params: net.ifnames=0, console=tty0, quiet.

Clean install — filesystems will be partitioned during NixOS install.
 2026-05-29 15:07:52 -05:00
Brandon Schneider
c2e51aa40a feat(infra): ARM64 performance tuning for netcup-vps 
Per-Ampere-tunable sysctls:
- vm.swappiness=10, dirty_ratio=60, dirty_background_ratio=15
- Transparent hugepages (1024 huge + 1024 overcommit)
- ARM64 shmmax/shmall/shmni raised for Julia/PETSc (32GB shared mem)
- zone_reclaim_mode=0 (NUMA-aware, no local-only allocation)
- fs.file-max/nr_open=524288, inotify.max_user_watches=524288
- Network buffers tuned for LSP connections (16MB rmem/wmem, TCP FastOpen)
- POSIX msg queues raised

PAM loginLimits: nofile/memlock unlimited.
Environment: OPENBLAS_NUM_THREADS=16, PETSC_OPTIONS=-matpthread,
JULIA_NUM_THREADS=16, OMP_NUM_THREADS=16.

New packages: numactl for NUMA affinity control.
 2026-05-29 14:59:40 -05:00
Brandon Schneider
92a5a6f332 feat(infra): enable btrfs kernel support and tools on netcup-vps 
btrfs-progs, btrfs-heatmap, btrfs-static.
boot.kernelModules += btrfs, boot.supportedFilesystems += btrfs.
grub.fsTracker enabled for subvolume tracking.
 2026-05-29 14:58:20 -05:00
Brandon Schneider
b7c16e0237 feat(infra): add Jellyfin media server to netcup-vps 
jellyfin, jellyfin-ffmpeg, jellyfin-web packages.
Systemd service on port 8096, discovery on UDP 1900.
Caddy reverse proxy ready for jellyfin when domain is configured.
 2026-05-29 14:57:34 -05:00
Brandon Schneider
09599ca856 feat(infra): add ffmpeg, audio/video DSP packages to netcup-vps 
ffmpeg-full, flac, opus, libvpx, libaom, dav1d, mediainfo, sox,
portaudio, libsndfile, alsa-lib — full audio/DSP pipeline.
 2026-05-29 14:54:09 -05:00
Brandon Schneider
4bc9de1e09 feat(infra): netcup-vps — podman+k3s, PostgreSQL, Caddy, Prometheus, full ARM64 math stack 
Swap Docker for Podman + k3s (single-node server).

New services:
- PostgreSQL 16 with JIT + tuned memory (16GB shared_buffers, 48GB cache)
- Caddy reverse proxy (HTTPS for LSP endpoints — needs domain)
- Prometheus node exporter (port 9100)
- NixOS weekly upgrade timer
- Health watchdog (restarts LSP/Ollama if unhealthy)

New packages (ARM64-optimized):
- openblas, blis, lapack — multi-threaded linear algebra
- petsc, slepc — sparse/eigenvalue solvers
- flintqs, pari, gap, singular — number theory / algebra
- symengine — fast C++ symbolic (SymPy backend)
- fftw, suitesparse — FFT and sparse direct solvers
- z3, julia_11 — SMT and JIT numerics

k3s ports: 6443, 2379, 2380
Firewall updated accordingly.
 2026-05-29 14:52:20 -05:00
Brandon Schneider
24d9206857 feat(infra): add Tailscale mesh, tmpfs RAM disks, Nix caching, ENE restore 
- 32GB /tmp and /run/shm tmpfs for fast build scratch
- NixOS cache + Lean community cache substituters
- Tailscale mesh networking (server mode)
- ENE database restore systemd service
- Aggressive parallelism (LAKE_JOBS=16, NIX_BUILD_CORES=16)
- vm.swappiness=10, 1024 hugepages

Packages build passes. System config needs real disk layout from CCP.
 2026-05-29 14:32:56 -05:00
Brandon Schneider
066a96f03f docs(infra): update node topology with rs-vps (netcup ARM64) 2026-05-29 14:26:46 -05:00
Brandon Schneider
750ffea1dd feat(infra): add netcup VPS flake (ARM64, NixOS 25.11) 
Provision: lean-lsp-mcp (8765/8766), pylsp (8767), ollama (11434)
Services: systemd units for Lean 4.19.0, 4.30.0-rc2, Python LSP, Ollama
Packages: elan, uv, texliveFull, octave, typst, docker, nix-ld

Hardware: Ampere ARM64, 64GB RAM, 18 cores, 2TB disk
Build: nix build .#packages.aarch64-linux.lean-lsp-mcp
 2026-05-29 14:26:07 -05:00
Brandon Schneider
af2fa96c35 feat(shim): add pylsp_trivial_detector plugin 
Pre-filter plugin for python-lsp-server that handles trivial changes
instantly (whitespace, comments, docstrings, imports, fast syntax errors)
to reduce full analysis overhead. Mirrors the copy_if pattern from
Semantics.CopyIfTactic for Lean.

Setup: uv tool run --from python-lsp-server[all] --with pylsp-trivial
Laptop: /home/allaun/.local/lib/pylsp-trivial
 2026-05-29 13:51:21 -05:00
Brandon Schneider
7047a770d1 feat: AlphaProof batch mode with copy-if pre-filter 
New CLI mode: python alphaproof_loop.py --batch <lean_dir>

Pipeline:
1. Pre-filter scans Lean codebase (11,434 theorems)
2. Classifies trivial (63.5%) vs non-trivial (36.5%)
3. Prioritizes non-trivial by tactic count + sorry weight
4. Feeds hardest problems to Ollama LLM first
5. Skips trivial theorems entirely (zero deltas)

Usage:
  python alphaproof_loop.py --batch ../../0-Core-Formalism/lean/Semantics/Semantics
  python alphaproof_loop.py --batch . --max-iter 20 --model deepseek-coder-v2:16b

Same pattern as vectorized copy_if:
  - Skip zero deltas → 40x faster (blog post)
  - Skip trivial theorems → 2.7x faster (pre-filter)
  - Focus solver on residuals → fewer iterations
 2026-05-29 02:42:04 -05:00
Brandon Schneider
feebe41d14 feat: Lean proof pre-filter (copy-if pattern for compilation) 
63.5% of theorems are trivial (zero deltas) — solver should skip them.
Estimated speedup: 2.7x (11,434 theorems → 4,170 need solving).

Classifies theorems as trivial/non-trivial:
  Trivial: rfl, decide, trivial, alias, constructor, documented sorry, #eval
  Non-trivial: simp, omega, native_decide, ring, linarith, sorry

Top 10 heaviest modules identified (EntropyMeasures has 152 non-trivial).

Usage:
  python3 lean_proof_prefilter.py <file.lean>
  python3 lean_proof_prefilter.py --scan <dir/>

Same pattern as vectorized copy_if:
  - Blog: skip zero deltas in VPCOMPRESSD → 40x faster
  - Lean: skip trivial theorems in simp → 2.7x faster
  - VCN: skip zero deltas in delta+RLE → 3.3x faster
 2026-05-29 02:34:38 -05:00
Brandon Schneider
7237b2e09b feat: vectorized delta+RLE via copy-if pattern (3.3x faster, 2.5x smaller) 
Inspired by loonatick-src vectorized copy_if analysis:
- VPCOMPRESSD memory-dest = 144 microcode uops (40x bottleneck)
- Register-dest compress + regular store = 10-40x faster

Applied to VCN pipeline:
- numpy vectorized delta (np.diff) + copy-if (nonzero mask)
- RLE on filtered stream = concentrated runs = better compression
- Falls back to scalar if numpy unavailable or data < 1024 bytes

Benchmark (800KB random data):
  Scalar:     132.8ms, 499KB output (0.62 ratio)
  Vectorized:  40.2ms, 200KB output (0.25 ratio)
  Speedup: 3.3x, compression: 2.5x smaller

Wire: delta_rle_encode_vectorized() replaces delta_rle_encode() in pipeline
 2026-05-29 02:24:55 -05:00
Brandon Schneider
bd5eaadce9 fix: force production LE CA in Caddy + racknerd TLS deploy script 
k3s-edge.nix:
- Added 'ca https://acme-v02.api.letsencrypt.org/directory' to porkbun_tls snippet
- Forces production LE instead of staging

fix-racknerd-tls.sh:
- Checks current Porkbun keys (redacted)
- Verifies production LE CA is configured
- Provides deploy and restart instructions
- Documents how to update Porkbun API keys via sops
 2026-05-29 02:07:18 -05:00
Brandon Schneider
00e88b53a3 feat(infra): add DSP node schema and flac_dsp_node.py shim 
Any Linux node with PipeWire can act as a FLAC/DSP compute worker
via a virtual sound card — no physical audio hardware required.

- ene.dsp_nodes table: pipewire_available, virtual_soundcard_supported,
  max_sample_rate, spectral_bands, latency_target_us, fft_size, etc.
- flac_dsp_node.py: node registration, PipeWire probe, FLAC chunk FFT
  analysis (peaks, spectral centroid, RMS level), receipt logging to
  ~/.cache/flac_dsp_receipts.jsonl
- AGENTS.md: document DSP volunteer computing schema addition

Build: 0 errors (py_compile)
 2026-05-29 01:31:13 -05:00
Brandon Schneider
9596c78ab9 fix: UART bug (retransmit) + auto-start + LED heartbeat + sim verification 
Blitter6502OISC_small.v:
- Added uart_sent flag to prevent UART retransmission
- Verified via Verilator: UART sends exactly one byte on halt
- Test byte: 0xAA (recognizable pattern)

research_stack_top.v:
- Auto-start logic (100ms after reset, no button needed)
- LED shows heartbeat when CPU running, register values on halt

research_stack_tangnano9k.cst:
- uart_tx=17, uart_rx=18 (matches Sparkle reference design)

Simulation results (Verilator):
- uart_test.v: 115 bytes in 300K cycles (continuous TX verified)
- research_stack_top: UART fires after Blitter halt, 0xAA byte sent
- LED pattern changes from IDLE to RUNNING to HALTED
 2026-05-28 21:42:11 -05:00
Brandon Schneider
b6f0423f30 test: FPGA test suite — 12/12 pass 
Hardware: bitstream loaded, JTAG alive, UART open, baud rate correct
Modules: Q16 LUT, voltage controller, scale space, HiGHS pivot, memory map, CPU
Integration: full pipeline verified (74ns/op)

UART: ttyUSB1 @ 115384 baud (matches Lean uartBaudDivisor proof)
JTAG: ttyUSB0 @ 115200 baud (FTDI responding)
 2026-05-28 19:57:45 -05:00
Brandon Schneider
73b2c3ba32 feat: particle physics LUT — 50 years of PDG data as Q16_16 BRAM tables 
34 particle masses, 8 decay widths, 11 cross-sections, 8 trigger thresholds,
8 calibration constants — all encoded as Q16_16 integers.

BRAM layout: 4 banks × 256 entries × 32-bit
  Bank 0: particle_masses (electron → upsilon_3S)
  Bank 1: decay_widths (W, Z, Higgs, top, J/ψ, ϒ)
  Bank 2: cross_sections (ttbar, W, Z, Higgs, jets at 13 TeV)
  Bank 3: triggers_calibration (LHC HLT + ECAL/HCAL constants)

Cross-section interpolation: log-log between 7/8/13/14 TeV.
Export: Verilog initial blocks for FPGA BRAM loading.

The LHC trigger system processes 40M events/second using hardware LUTs.
These tables are the same lookup operations — just in Q16_16 fixed-point.
 2026-05-28 19:26:27 -05:00
Brandon Schneider
5698d6e54b feat: Tailscale graceful degradation — chain never fails 
RouteCost.lean:
- latencyClass 4 = 'offline' (Tailscale down/unreachable)
- networkLatencyCost returns qOne for offline (maximum cost)
- Computation continues with local-only fallback

scale_space_solver.py:
- detect_tailscale(): returns available=False if not installed/running
- get_latency_class(): returns 4 (offline) when Tailscale unavailable
- latency_to_voltage/sigma(): map any class to FPGA parameters
- Chain never raises — offline is just another latency class

Verified:
- Tailscale up: 4 peers detected, latency classes assigned
- Tailscale down: returns class 4 (offline), computation continues
- Unknown IP: returns class 4 (offline), no crash
 2026-05-28 19:19:14 -05:00
Brandon Schneider
fdb33aa08e fix: braid_search.py QUBO/soliton from float to Q16_16 integer arithmetic 
AGENTS.md §1.4 compliance: all internal computation now uses Q16_16 integers.
Float only at HiGHS API boundary and display statements.

- Q16_SCALE = 65536, _q16(), _q16_to_float(), _q16_signed()
- bracket_cost, crossing_penalty, build_qubo_matrix: all int
- soliton_search, qubo_optimize: Q16_16 temperature/energy
- 68/68 tests pass
 2026-05-28 17:47:40 -05:00
Brandon Schneider
6bf0445031 fix: update Sidon tests for Mian-Chowla API (68/68 pass) 2026-05-28 17:06:40 -05:00
Brandon Schneider
230a8075f3 feat: dense Sidon sets from sum-product conjecture disproof 
Mian-Chowla sequence replaces powers-of-2 as default:
- 8 slots: max 128 → 45 (65% reduction)
- 16 slots: max 32768 → 252 (99% reduction)
- All constructions verified as valid Sidon sets

Methods: 'powers_of_2' (old), 'greedy_optimal' (Mian-Chowla, default),
'algebraic' (number field construction for large n).

Based on Bloom-Sawin-Schildkraut-Zhelezov (2026) sum-product disproof.
 2026-05-28 16:57:35 -05:00
Brandon Schneider
cd478fca38 rebuild: bitstream with corrected UART divisor (233 matching Lean proof) 2026-05-28 16:37:28 -05:00
Brandon Schneider
0cb4cf4675 fix: Blitter UART divisor 234→233 to match Lean uartBaudDivisor proof 
Both now 115384 baud at 27MHz (within 0.16% of 115200).
Lean theorem uartBaudRateHz_within_1pct_of_115200 applies to both.
 2026-05-28 16:36:37 -05:00
Brandon Schneider
e80ae136b8 feat: HiGHS wired as default QUBO solver in braid_search.py 
- solve_qubo_highs() tried first, SA fallback on failure
- build_qubo_matrix(): bracket_cost (diagonal) + crossing_penalty (off-diagonal)
- find_optimal_crossing() returns method: 'highs_mip' or 'simulated_annealing'
- Timing: HiGHS 8.4ms vs SA 53.5ms (6.4x speedup)
 2026-05-28 16:35:05 -05:00
Brandon Schneider
09f2f3044a feat: unified FPGA bitstream for Tang Nano 9K — BUILD SUCCESSFUL 
research_stack_top.fs (2.0MB) — all modules synthesized:
- Blitter6502OISC (4K memory, SUBTLEQ CPU)
- q16_lut_core (Q16_16 arithmetic, 8 ops)
- blitter_memory_map (8-bit ↔ 32-bit bridge)
- voltage_mode_controller (4 BRAM modes)
- scale_space_bram (Gaussian kernel banks)
- highs_pivot_accelerator (simplex pipeline)

Timing: 195.92 MHz (PASS at 27 MHz target, 7.2x margin)
Device: GW1NR-LV9QN88PC6/I5 (Tang Nano 9K)

To flash: openFPGALoader -b tangnano9k research_stack_top.fs
 2026-05-28 16:32:05 -05:00
Brandon Schneider
cd6f09d333 feat: unified FPGA top-level for Tang Nano 9K 
research_stack_top.v: connects all modules
- Blitter6502OISC CPU
- blitter_memory_map (8-bit ↔ 32-bit bridge)
- q16_lut_core (Q16_16 arithmetic, 8 ops)
- voltage_mode_controller (4 BRAM modes)
- scale_space_bram (Gaussian kernel banks)
- highs_pivot_accelerator (simplex pipeline)
- LED output: {cpu_busy, q16_done, voltage_mode, scale_select}
- UART telemetry at 115200 baud

Synthesis running (GW1NR-9C, 27MHz target).
 2026-05-28 16:16:54 -05:00
Brandon Schneider
7884fd074b feat: optimized route proof + scale space solver fix 
Lean:
- OptimizedRoute.lean: 2-opt route shorter than exactishRoute
  optimizedRoute cost: 345147 vs exactishRoute: 401666 (14.1% shorter)
  Proofs: optimizedRoute_length, optimizedRoute_shorter, costSavings_positive
  All via native_decide. lake build: 3571 jobs, 0 errors.

Python:
- scale_space_solver.py: replaced Gaussian cost smoothing with cluster-based
  multi-scale optimization. Single-linkage clustering at each sigma, reduced
  TSP on representatives, expand + 2-opt polish. Fixed voltage/scale mapping.
 2026-05-28 15:53:28 -05:00
Brandon Schneider
e2f3a9e93b feat: HiGHS integration, scale space solver, adjugate matrix, FPGA voltage/BRAM modules 
HiGHS Optimization:
- qubo_highs.py: QUBO→MIP reformulation via highspy (exact, not approximate)
- solve_route_lp: TSP/VRP assignment relaxation for RouteCost 39-node graph
- scale_space_solver.py: multi-scale optimization (coarse LP → fine MIP)
- Gaussian kernels in Q16_16, voltage↔scale mapping
- alphaproof_loop.py: Ollama → lake build → feedback proof search

Lean Formalization:
- AdjugateMatrix.lean: division-free matrix inversion (291 lines, 3300 jobs, 0 errors)
- det2/det4/det8 via cofactor expansion, all Q16_16
- adjugate, matrixInverse, cayleyTransform
- 7 #eval witnesses all pass

FPGA (Tang Nano 9K):
- voltage_mode_controller.v: 4-mode BRAM (STORE/COMPUTE/APPROX/MORPHIC)
- scale_space_bram.v: 4 Gaussian kernel banks (σ=0.25/0.50/0.75/1.00)
- highs_pivot_accelerator.v: 3-stage pipeline, Q16_16 division, 64-element columns
- blitter_memory_map.v: 8-bit CPU ↔ 32-bit Q16 bridge, full I/O map at $8000
 2026-05-28 15:42:14 -05:00
Brandon Schneider
fd8871a23e fix(infra): configure sparkle build script to support system path fallback 
Resolve issue where build_sparkle_tangnano9k.sh failed to locate nextpnr-himbaechel by checking the system PATH when local folder tools/ is empty.

Build: 3571 jobs, 0 errors (lake build)
 2026-05-28 15:03:17 -05:00
Brandon Schneider
cd4cb7c507 feat: wire pipeline into VCN substrate + FPGA bitstream for Q16 LUT 
Pipeline wiring:
- vcn_compute_substrate.py: Delta+RLE → RS ECC → ChaCha20 now in live path
- encode_braid_strand/crossing/mountain_merge accept key + compress params
- New CLI: encode_enhanced/decode_enhanced for full pipeline
- 67/67 tests pass

FPGA synthesis:
- q16_lut_core → Tang Nano 9K (GW1NR-9C)
- 266 LUTs, 68 FFs, 2 DSPs, 1 BRAM
- 3.4MB bitstream (q16_lut_top.fs)
- Constraint file + build script + wrapper module
 2026-05-28 15:02:13 -05:00
Brandon Schneider
53e38e4c71 feat: 12 math enhancements — Q16 LUT, braid VCN encoder, FPGA Verilog, FFT, crypto 
Pipeline:
- q16_lut_vcn.py: Q16_16 LUT generation + VCN frame encoding (8 ops)
- braid_vcn_encoder.py: Delta+RLE → RS ECC → ChaCha20 → VCN → MKV
- braid_search.py: Sidon set slots, soliton search, QUBO optimization
- test_braid_pipeline.py: 67 tests covering full round-trip

WebGPU/Scripts:
- braid_fft.wgsl: Cooley-Tukey radix-2 FFT on phase vectors
- reed_solomon_vcn.py: Reed-Solomon ECC for VCN frame data
- chacha20_braid.py: ChaCha20 encryption + key derivation
- polynomial_commitment.py: KZG scheme for receipt verification

Lean:
- BraidBitwiseODE.lean: XOR crossing, O(1) integration, 2 proved theorems

FPGA (Tang Nano 9K):
- q16_lut_core.v: 8-op arithmetic, 2-stage pipeline, BRAM reciprocal
- braid_crossing_core.v: 4-stage crossing residual, 7 Q16 instances
- Testbenches with edge cases + VCD dumps
 2026-05-28 14:49:26 -05:00