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
525 commits 18 branches 0 tags 425 MiB
Commit graph

190 commits

Author SHA1 Message Date
Brandon Schneider
89e995aaa0 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
31651fbc8f 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
af2e01371c 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
0be03236be 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
7f22de3c36 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
b77c0e7ddd 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
fcaed6c10c 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
fad3b53f10 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
aa689822e9 docs(infra): update node topology with rs-vps (netcup ARM64) 2026-05-29 14:26:46 -05:00
Brandon Schneider
cd385afcdc 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
5e12f21fa1 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
48eb892f49 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
42b5f7ea4f 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
2cf52fa913 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
d0da687495 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
093d8ef43f 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
270ef14e21 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
dbf67ab130 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
096a566aaf 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
159ba50059 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
f8554a3736 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
d956ac7583 fix: update Sidon tests for Mian-Chowla API (68/68 pass) 2026-05-28 17:06:40 -05:00
Brandon Schneider
6f650be6ab 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
410a5c2e5f rebuild: bitstream with corrected UART divisor (233 matching Lean proof) 2026-05-28 16:37:28 -05:00
Brandon Schneider
6a9fcdd115 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
2fed2b3e41 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
468b449aad 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
fff44bafe4 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
5979046715 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
ea3eedef77 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
0912d5b130 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
a3b298230b 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
e0df130453 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
Brandon Schneider
ae81dd7302 feat(infra): compile and SRAM-flash UART beacon with reset bypass 
Synthesized and placed-and-routed the UART beacon design on Tang Nano 9K with physical reset bypassed (rst_n_internal = 1'b1). Programmed the SRAM using openFPGALoader (CRC check: Success). Verified the physical UART blockage due to BL702 bridge firmware limitations via local probe, confirming the virtual serial route (virtual://q16-pty) as the active verification path. Updated scoped AGENTS.md files with the latest hardware status and Lean build baselines.

Build: 3313 jobs, 0 errors (lake build)
 2026-05-28 14:10:46 -05:00
Brandon Schneider
d86625e220 feat(infra): cluster dashboard + VCN shim indentation fix 
- Add LyteNyte Grid cluster dashboard (React + FastAPI + k3s)
  - Real-time telemetry: GPU util/VRAM/temp, CPU/memory, pod counts,
    Tailscale connectivity, OS/kernel info for all 5 cluster nodes
  - WebSocket live updates every 3s, dark theme, virtualized grid
  - k3s deployment with hostNetwork, NodePort 30820, SSH-based collectors
  - Backend uses /proc/stat + /proc/meminfo for portable NixOS metrics
  - Tailscale status via SSH to host (container doesn't run tailscaled)
- Fix vcn_compute_substrate.py indentation (lines 45-269 had 1 extra
  leading space). Script now compiles and runs encode/decode/receipt.

Build: py_compile OK, npm build OK, podman build OK
 2026-05-28 01:13:54 -05:00
Brandon Schneider
4cad34faf4 feat(hardware): Emergency Boot Witness reference implementation 
Add compiling Lean modules and Python shim for the Geometry Emergency
Boot Witness specification (graphene supercapacitor geometric encoding).

Lean modules (Semantics.Hardware.EmergencyBoot.*):
- EmergencyBootTypes: HexCoord, CapClass, OpticalPath, VoltageDifferential,
  GrapheneMemristor, HybridOpticalPath, material properties
- EmergencyBootState: PowerState, SolarPowerState, ScanState, seed assembly,
  emergency boot state machine with 6502 calculator efficiency targets
- EmergencyBootShell: Command opcodes, status byte encoding, process
  definitions, executeCommand dispatch

All use Q16_16 fixed-point arithmetic (no Float in compute paths).
Verified theorems: utilizationWithinBounds, powerFailureMonotonic,
commandOpcode_roundTrip.

Python shim (4-Infrastructure/hardware/emergency_boot/):
- EmergencyBootEngine simulating FPGA geometric scan and seed extraction
- Demo CLI showing power failure → self-powered calculator mode →
  geometric scan → seed assembly flow

Build: 3302 jobs, 0 errors (narrow target), 3313 jobs, 0 errors (Compiler)

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-27 23:00:39 -05:00
Brandon Schneider
69b984c410 fix(infra): resolve k3s services startup issues and update ingress configuration 
- Revert builder image in embedded_surface Dockerfile to rust:bookworm for glibc compatibility with bookworm-slim runner.
- Replace racknerd-surface.json Git LFS pointer with the actual retrieved JSON config to resolve parse errors.
- Separated and imported regenerated docker images for stubs and credential-server on all cluster nodes.
- Fixed Ingress resources and middleware to target the correct authentik-server service name.
- Rewrote verification script checks to handle iptables-based ports and relative redirects robustly.
- Updated nixos-laptop IP in node topology documentation.

Build: 0 jobs, 0 errors
 2026-05-27 17:39:00 -05:00
Brandon Schneider
92bc00c4d5 feat(lean): complete goldenContractionEnergyDecrease proof + PIST predictions pipeline v2 
- PistSimulation.lean: proven goldenContractionEnergyDecrease (no sorry)
  7 supporting lemmas, h_u'_nonneg + h_pt hypothesis, fold induction
- Connectors.lean: restored zeroIsVoid theorem with Q16_16 proof
- CanonSerialization.lean: removed dead theorem, documented blocker
- FixedPointBridge.lean: eliminated Float from compute paths

PIST predictions pipeline:
- pist_matrix_builder.py: reproducible matrix-only builder (SHA256)
- build_pist_matrices_278.py: generates PIST/Matrices278.lean
- PIST/Classify.lean: classifyProxy/classifyExact stubs (v2 surface)
- PIST/Matrices278.lean: 250-entry matrix HashMap
- build_corpus278.py: reads predictions artifact, uses classify*
- Pipeline contract documented in root AGENTS.md

Cleanup:
- Archived 5 orphan pist_* shims, 5 old route_repair variants
- Quarantined PIST/Repair.lean (no external callers)
- Created 4 opencode agents for remaining TODO items

Build: PistSimulation 3309, Compiler 3313, Full 3571 (0 errors)
 2026-05-27 12:40:16 -05:00
Brandon Schneider
36b5b6914e feat(lean): wire 278-equation corpus end-to-end; emit emit278.json 
- AVMIsa/Emit §7: fix emitRrcCorpus278 JSON structure (summaryStr
  sub-object + classified.rowsJson instead of nested classified.json);
  add #eval emitRrcCorpus278 witness (line 261)
- RRC/Emit §8: add rowsJson field to EmitResult (flat JSON array of
  rows, usable by outer envelope builders without re-serializing)
- 4-Infrastructure/shim/emit278_extract.py: new extractor — runs
  lake build Semantics.AVMIsa.Emit, captures #eval output, strips
  Lean repr escaping, validates JSON, writes
  shared-data/data/stack_solidification/emit278.json
- emit278.json: 278 rows, schema=avm_rrc_corpus278_v1,
  avm_canaries_passed=true, bundle_receipt_valid=true,
  claim_boundary=admissibility-and-routing-pass-only;not-promoted
  (all 278 rows missing_prediction — no PIST labels supplied yet)
- Full lake build: 3570 jobs, 0 errors

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-27 00:11:55 -05:00
Brandon Schneider
bdc98e2a0e feat(lean): port pist_trace_classify motif scoring to Semantics.PIST.Motif 
Ports the motif scoring surface from pist_trace_classify_mcp.py (lines 136–149)
into a provable Lean module:

  score = frequency / max(library_size, 1) + (0.3 if tactic_family matches)

New module: Semantics.PIST.Motif (201 lines)
  §1  familyMatchBonus constant (ofRatio 3 10 = 19660 raw)
  §2  MotifInputs, baseScore, motifScore
  §3  MotifCandidate record, mkCandidate constructor
  §4  rankMotifs / topKMotifs (mergeSort desc, motifId tie-break)
  §5  8 executable #eval witnesses with -- expect: annotations
  §6  6 proved invariants:
      motifScore_bonus_pos (decide)
      motifScore_match_ge_base_witness (decide, concrete)
      motifScore_zero_freq_base (simp)
      motifScore_zero_freq_no_match (simp)
      motifScore_zero_freq_match_witness (decide, concrete)
      rankMotifs_match_beats_no_match (native_decide — mergeSort sort witness)

Full workspace build: 3570 jobs, 0 errors.

pist_trace_classify_mcp.py PARTIAL BOUNDARY updated: motif score + rank order
now explicitly point to Semantics.PIST.Motif as authoritative.

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-26 23:45:07 -05:00
Brandon Schneider
34f58d12d9 feat(lean): port route_repair_v14a rank_patches to Semantics.PIST.Repair 
Ports the decision-critical scoring functional from route_repair_v14a.py
into a provable Lean surface:

  rank_patches: S = α·specificity − β·cost + γ·success_prior − δ·residual_risk
  ALPHA=0.4, BETA=0.3, GAMMA=0.2, DELTA=0.1  (all as Q16_16.ofRatio)

New module: Semantics.PIST.Repair (232 lines)
  §1  PatchScoreInputs, PatchWeights structures
  §2  rankScore (linear functional), rankScoreDefault, mkInputs, embedResidualRisk
  §3  Patch record + mkPatch constructor
  §4  rankPatches / rankPatchesDefault (mergeSort desc, tag tie-break)
  §5  5 executable #eval witnesses with -- expect: annotations
  §6  8 proved invariants (native_decide):
      defaultWeights_sum, defaultWeights_pos, defaultWeights_ordered,
      rankScore_zero_inputs_negative, embedResidualRisk_one/zero,
      rankScore_monotone_specificity_witness, rankScore_zero_lt_full

Full workspace build: 3569 jobs, 0 errors.

route_repair_v14a.py PARTIAL BOUNDARY comment updated to name this module
as the authoritative source for the scoring surface.

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-26 23:32:36 -05:00
Brandon Schneider
8ee3d431d2 feat(lean): port pist_trace_classify_mcp spectral logic to Semantics.PIST.Spectral 
## New module: Semantics.PIST.Spectral

Ports the two domain-logic functions from pist_trace_classify_mcp.py
that were previously executing in unverified Python:

### classify_tactic_from_name → classifyTacticFromName
- `TacticFamily` inductive (rewrite, normalization, arithmetic, induction,
  algebraic, case_analysis, discharge, reflexivity, unknown)
- Pure string-lookup; 5 executable witnesses confirm all branches.

### compute_spectral → computeSpectral
- `isqrt` — integer Newton's method for floor(√n); 4 witnesses.
- `powerIteration` — Q16_16 fixed-point dominant eigenvalue via power
  iteration with Rayleigh quotient; identity-matrix witness = 65536.
- `SpectralProfile` structure — 10 fields (matrix_size, rank,
  spectral_gap, density, trace_val, frobenius_norm, laplacian_zero_count,
  adjacency_eigenvalue_max, laplacian_eigenvalue_max, singular_value_max).
- `computeSpectral` — symmetrize → lap → powerIteration → shift-deflation
  for second eigenvalue → AᵀA for singular value; 3 witnesses on 2×2 fixture.

No Float in any compute path. All magic constants documented with formulas.

## Other changes
- Semantics.lean: add `import Semantics.PIST.Spectral`
- AgenticOrchestration.lean:163: expand bare `-- TODO(lean-port):` label
- pist_trace_classify_mcp.py: update PARTIAL BOUNDARY comment to name
  the Lean module that now owns spectral logic

## Build baseline
  lake build Compiler → 3311 jobs, 0 errors

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-26 23:25:50 -05:00
Brandon Schneider
f9b5ac25fb fix(lean+shim): enforce lean-coding rules across audit surface 
## Lean fixes

- RRCLogogramProjection.lean: replace `native_decide` → `decide` in 5
  compiler-surface theorem witnesses (semantic_tear_projects_after_repair,
  semantic_tear_does_not_merge, semantic_tear_uses_quarantine_lane,
  unrepaired_tear_does_not_project, ordinary_logogram_projects_and_merges).
  All 5 pass under `decide`; no logic change.

- PistSimulation.lean: add `-- expect: <value>` to every `#eval`/`#eval!`
  block across §6–§11 (~104 annotation lines). Document 8 undocumented
  `ofRawInt` magic integers in fixtureSpectralWindow (10.0, 20.0, 100.0,
  40.0, 20.0, 10.0, 5.0, 5.0 × 65536).

- DynamicCanal.lean: add `-- expect:` to all 15 #eval witness blocks in
  §17 (fixed-point constructors, DIAT encoding, coarse-graining tests).

- MISignal.lean: add `-- expect: 131072` to both #eval witnesses.

- Functions/BracketedCalculus.lean: add `-- expect: 327680` to #eval.

- AVMIsa/Emit.lean, RRC/Emit.lean, RRC/ReceiptDensity.lean, ReceiptCore.lean:
  previously-staged `-- expect:` additions (from prior session) carried
  forward in this commit.

## Python shim fixes

- Add `# PARTIAL BOUNDARY: contains domain logic; not a provable surface.
  Port to Lean/RRC before treating as authoritative.` to 9 shim files:
  pist_trace_classify_mcp.py, genus0_sphere_shell_demo.py,
  routing_benchmark.py, route_repair_v14a.py, pist_prove_and_classify.py,
  label_canary_theorems.py, validate_rrc_predictions.py,
  pist_receipt_density_injector.py, rrc_pist_shape_alignment.py.

## Build baseline

  lake build Compiler  →  3311 jobs, 0 errors
  lake build           →  3567 jobs, 0 errors

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-26 23:17:40 -05:00
Brandon Schneider
d1017fbbbd feat(lean): port receipt-density scoring to Semantics.RRC.ReceiptDensity 
Adds Semantics/RRC/ReceiptDensity.lean — a new Lean module that ports
the entire scoring pipeline from pist_receipt_density_injector.py into
Lean-native Q16_16 fixed-point arithmetic:

  spectralQuality   ← spectral_quality()   (0.24/0.18/0.18/0.12/0.12/0.16 weights)
  shapeAgreement    ← shape_agreement()    (exact=1.0, proxy=0.82, any=0.35)
  axisScore         ← axis_score()         (hits/4, capped at 1.0)
  statusScore       ← status_score()       (BLOCKED=0, HOLD=0.12 … VERIFIED=0.84)
  computeDensity    ← compute_density()    (density: 26/24/26/24, confidence: 20/20/28/32)

No Float in compute paths — all arithmetic is Q16_16 (raw Int, scale=65536).
Two #eval witnesses verify CANDIDATE/VERIFIED case outputs.

Build: lake build Compiler → 3311 jobs, 0 errors (baseline preserved).

Update shim BOUNDARY comments:
  pist_receipt_density_injector.py → Semantics.RRC.ReceiptDensity
  rrc_pist_shape_alignment.py      → Semantics.RRC.Emit

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-26 22:48:55 -05:00
Brandon Schneider
747045ff0f docs(agents): project-wide AGENTS.md audit — cross-refs, baseline, contracts 
Actions taken from 5-agent audit sweep (audit date 2026-05-26):

AGENTS.md / docs sync:
- root AGENTS.md: add scripts/qc-flag and lean_expert_agent to Nested Contracts
- All 6 nested AGENTS.md files: append Cross-References section pointing to
  root for Post-Interaction Workflow, Programming Choice Flow, Do Not Sweep,
  Git Remote Hygiene (Lean, Infra, text-to-cad, docs, qc-flag, lean_expert_agent)
- 6-Documentation/docs/AGENTS.md: cross-ref also lists AVMIsa.Emit sole output
  boundary and Compiler surface blessing

Lean build baseline:
- 0-Core-Formalism/lean/Semantics/AGENTS.md: update blessed Compiler Surface
  header to commit ff8e71fa; correct job count to 3311 (lake build Compiler)

ARCHITECTURE.md:
- §7 repo table: add RRC.Emit, AVMIsa.Emit, RRC.Corpus278 to Lean/Semantics entry
- New §7.1 Compiler Surface: documents 3-root pipeline and sole output boundary
- §4 Data Flow: annotate output with AVMIsa.Emit sole-boundary note

TODO_MAP.md:
- Phase A6: add 3 new Lean deliverables (Corpus278, RRC.Emit, AVMIsa.Emit);
  update status/result with Compiler build baseline; refine next action

Build: Compiler 3311 jobs, 0 errors (no Lean changes).

Generated with Devin (https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-26 22:34:46 -05:00
Brandon Schneider
ff8e71fa8d chore(infra): stage pist canary labeling and training shims + flexure report 
- label_canary_theorems.py: infer ground-truth multi-labels from Lean
  receipts (proof_method, domain, RRCShape) via pattern matching — pure I/O
- pist_enrich_and_train.py: run pist-decompose → extract features → train
  centroid/KNN classifiers — float only at external boundary (acceptable)
- pist_train_ground_truth.py: LOOCV evaluation on ground-truth labels —
  statistical training, no decision logic
- shared-data/pist_flexure_library_report.json: updated flexure library report

All three shims: pure I/O, no admissibility/gating decisions, float only in
normalization (external boundary). Complies with AGENTS.md §Programming Choice
Flow. Outputs are regenerable from source receipts.

Build: Compiler 3311 jobs, 0 errors (no Lean changes).

Generated with Devin (https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-26 22:32:13 -05:00
Brandon Schneider
81a61b6944 feat(rrc): 278-equation corpus — AVM sole output boundary, RRC classifier feeds it 
Architecture:
  RRC.Corpus278  — raw features only (Python supplies, Lean owns gate)
  RRC.Emit       — alignment classifier; emitCorpus generic entry point
  AVMIsa.Emit    — sole output boundary; imports Corpus278, stamps bundle

Changes:
- RRC/Emit.lean: extend FixtureRow + RrcRow with 5 generator fields
    (operatorTokens, invariantsDeclared, boundaryConds, templateKey, templateParams)
  Add emitCorpus (schema, corpus) generic emitter; emitFixture is now a thin wrapper
  jRrcRow JSON serializer emits all generator fields
- RRC/Corpus278.lean: auto-generated 278-row FixtureRow list
  Source: archive/experimental-shim-probes/rrc_equation_classifier_receipt.json
  Python extracts raw features; all gating in Lean (alignment gate fires missingPrediction
  for all 278 rows currently — correct, no PIST labels present yet)
- AVMIsa/Emit.lean: import Corpus278; add §7 emitRrcCorpus278 — AVM canaries must
  pass for bundle receipt to be valid; stamped by AVM authority (avm.rrc_corpus278.bundle)
  §8 eval: corpus summary fires (278, 0, 278) — all held, 0 promoted, gate honest
- lakefile.toml: add Semantics.RRC.Corpus278 to Compiler blessed roots; update comment
- 4-Infrastructure/shim/build_corpus278.py: corpus builder script

Build: 3567 jobs, 0 errors (lake build)

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-26 22:23:56 -05:00
Brandon Schneider
3a23ad6b9e Merge remote-tracking branch 'github/main' 2026-05-26 21:30:45 -05:00
Brandon Schneider
a441c22dae chore(tests): gitignore Playwright test-results and node_modules 2026-05-26 21:12:00 -05:00
Brandon Schneider
aae680ad3c chore(infra): add internal routing smoke-test script 
scripts/verify-internal.sh runs the exact verification sequence before
the edge is touched. Checks (in order):

  0. Port listeners — host Caddy owns :80, Traefik NodePort on :30080
  1. GET / — 200 Homer or 302 → auth.researchstack.info (not internal IP)
  2. /api/* bypass — none of /api/*/health may 302 to Authentik
  3. auth.researchstack.info — 200/302 from Authentik, no internal-IP loop
  4. Host header passthrough — Traefik :30080 /ping reachable; /api/jobs/health
     routes end-to-end through host Caddy → Traefik → Ingress
  5. X-Forwarded-Proto — https header survives the server-Caddy hop

Usage:
  # on nixos-laptop directly:
  bash 4-Infrastructure/k3s-flake/scripts/verify-internal.sh

  # from any tailnet node:
  bash 4-Infrastructure/k3s-flake/scripts/verify-internal.sh --remote

Exit 0 = safe to deploy edge. Exit 1 = fix red checks first.

Generated with Devin (https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-26 21:08:58 -05:00