Commit graph

14 commits

Author SHA1 Message Date
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
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
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
31b2f1f66f 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
e203a5215e 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
a99e839bab Track remaining source and documentation inventory 2026-05-11 22:18:31 -05:00
Brandon Schneider
29f9b78b6d Stage stack solidification source slice 2026-05-11 22:08:10 -05:00
Brandon Schneider
0cf775c80e collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution
- Prover-Integrated Orchestration Layers (L0-L3): Goedel-Prover-V2 watchdog, BFS-Prover-V2 swarm consensus, bf4prover topology adaptation
- FAMM Verilator benchmark: uniform vs preshaped delay comparison (4.4x speedup)
- Swarm topological device prober: 11 agents probing traces, caps, delays, errors, vias, PDN
- Spec sheet puller: 10 components with key params and topological relevance
- Virtual FPGA system tests: 6/6 passed, 134K ops/s throughput
- Fixed merge conflicts in AI-Newton test_experiment.ipynb
2026-05-06 23:42:01 -05:00
Brandon Schneider
0709b298b3 Consolidate research stack updates 2026-05-05 21:09:48 -05:00
Brandon Schneider
5f88abf618 initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00