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

165 commits

Author SHA1 Message Date
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
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
ed98817257 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
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
a8a163650a 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
ede983168c 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
cc33703637 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
8c4a8e9971 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
3a44048b22 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
4a72ad1183 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
835299fd9a 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
e0935f01e0 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
3044f36df7 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 49f0dfb3; 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
49f0dfb31a 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
3f923e2c13 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
2d19317660 Merge remote-tracking branch 'github/main' 2026-05-26 21:30:45 -05:00
Brandon Schneider
f1d9253696 chore(tests): gitignore Playwright test-results and node_modules 2026-05-26 21:12:00 -05:00
Brandon Schneider
7f64942fd2 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
Brandon Schneider
6ca8fd439b feat(k3s-edge): rewrite edge Caddy as dumb TLS forwarder + legacy 301s 
Edge Caddy now does exactly three things:
1. Terminate TLS for researchstack.info + *.researchstack.info via
   Porkbun DNS-01 (wildcard cert covers all subdomains in one renewal)
2. 301-redirect legacy subdomains to canonical path equivalents:
     status.*  → /server/status/
     dash.*, home.*  → /
     media.*  → /apps/jellyfin/
     books.*  → /apps/books/
     music.*  → /apps/music/
     vault.*  → /server/vault/
     pulse.*  → /api/registry/
     apps.*  → /apps/
     *.* (wildcard fallback)  → /
3. Forward all other traffic to the internal router (host Caddy :80 on
   k3s-server over Tailscale) with X-Forwarded-* headers preserved.
   auth.* and mail/webmail.* are forwarded unchanged (stable subdomains).

No path routing logic on the edge. Traefik Ingress (k3s-server) owns
all path decisions. This commit has no effect until nixos-rebuild switch
is run on microvm-racknerd (deploy after k3s-server is verified).

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:06:06 -05:00
Brandon Schneider
cfa43cf07f feat(k3s-server): Traefik NodePort + host Caddy pass-through (internal-only) 
Port conflict resolution:
- Add HelmChartConfig to pin Traefik web entrypoint to NodePort 30080
  (not host :80) so k3s Traefik and host Caddy do not race for the port
- Add host Caddy on :80 as a minimal pass-through to Traefik :30080;
  carries X-Forwarded-* headers so Traefik sees the real client IP and
  the correct Host. No TLS, no Porkbun, no subdomain logic — all of
  that stays on the edge Caddy (k3s-edge.nix)
- Caddy after= k3s.service so Traefik NodePort is ready before proxying

Authentik port fix:
- Change authentik server + worker services from NodePort 30080 to
  ClusterIP; Traefik reaches Authentik via the rs-auth Ingress and
  cluster DNS, no NodePort required

New manifests (internal, no public-traffic impact):
- manifests/ingress/: Traefik Ingress resources + Middleware CRDs
  (/apps/*, /server/* → forward_auth + strip-prefix; /api/* → strip only;
  / → Homer + forward_auth; auth.* → Authentik, no middleware)
- manifests/hermes/: placeholder chat/orchestrator service
- manifests/credential-server/: token-auth credential vault stub
- manifests/control-plane/: registry-api, jobs-api, blobs-api health stubs
- manifests/homer/configmap.yaml: updated dashboard links to canonical paths

Deploy order: rebuild k3s-server first, verify Traefik + Ingress
internally, then deploy k3s-edge (commit 3 / next step).

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:03:54 -05:00
Brandon Schneider
5f372ea04d test(infra): add Playwright E2E routing test suite 
Tests the full traffic path against live researchstack.info infrastructure:
  Edge Caddy (TLS) → Tailscale → Traefik Ingress → k3s services

Coverage:
- edge-tls-redirects: HTTPS reachability, cert validity, legacy subdomain
  301s (status/dash/home/media/books/music/vault/pulse/apps), stable
  subdomains (auth, mail), wildcard fallback
- path-routing: /apps/*, /server/*, /api/* routes; prefix stripping; SSO
  redirect vs token-auth isolation
- auth-integration: Authentik login page, OIDC discovery, forward_auth
  gating on protected paths, /api/* bypass

19/40 tests pass against current live infrastructure (pre-deploy). The 21
failures are "not yet deployed" signals, not design errors. Run after each
phase of the deployment plan to use as a regression gate.

Run: cd 4-Infrastructure/k3s-flake/tests && npm test

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:03:27 -05:00
Allaun Silverfox
3dcb5a2d0a chore(pending): quarantine python ENE ContextStream MCP surface (Lean-first unification) 2026-05-26 17:59:30 -05:00
Allaun Silverfox
d200887e42 cleanup(ene): make provenance node/lake_seed/tailscale_ip configurable via env vars 2026-05-26 16:39:43 -05:00
Allaun Silverfox
c4c50bb78f cleanup(ene): read canonical SQL schema file for chat tables; remove embedded DDL string 2026-05-26 16:34:23 -05:00
Allaun Silverfox
b8cc57943e cleanup(ene): add canonical SQL schema for chat/session sync tables 2026-05-26 16:23:51 -05:00
Allaun Silverfox
e630fd0612 cleanup(ene): remove hardcoded schema path, drop inline schema fallback, add legacy shim strip receipt 2026-05-26 16:22:40 -05:00
Allaun Silverfox
4dbb4121a4 docs(shim): annotate alignment shim as legacy pending AVM port; add strip receipt metadata 2026-05-26 16:14:52 -05:00
Allaun Silverfox
98f5f0e795 docs(shim): annotate as legacy shim pending AVM port; add strip receipt metadata 2026-05-26 16:13:43 -05:00
Allaun Silverfox
64fee9a863 fix(pist): correct repo root + fail-on-raw-disagreement check 2026-05-26 15:50:29 -05:00
Allaun Silverfox
4e91db4052 feat(pist): add RRC PIST shape-alignment calibration pass 2026-05-26 15:43:45 -05:00
Allaun Silverfox
846a2ef241 feat(pist): add RRC PIST validation report cleaner 2026-05-26 15:38:07 -05:00
Allaun Silverfox
2c9e029923 feat(pist): add receipt-density sidecar readback validator 2026-05-26 15:18:11 -05:00
Allaun Silverfox
14aac49e96 test(pist): add receipt-density injector regression harness 2026-05-26 15:16:40 -05:00
Allaun Silverfox
0686b39428 feat(pist): use shared rds_connect for receipt-density writer 2026-05-26 15:13:35 -05:00
Brandon Schneider
fc2ade9681 chore: remove unused import subprocess from v14a (handled by rds_connect) 2026-05-26 15:11:11 -05:00
Brandon Schneider
7eda71868a refactor(rds): consolidate 14 psycopg2 connect patterns into shared rds_connect module 
Creates 4-Infrastructure/shim/rds_connect.py with a single connect_rds()
function that resolves connection parameters in priority order:
  1. explicit kwargs
  2. DATABASE_URL env var (postgres://user:pass@host:port/dbname?sslmode=...)
  3. individual RDS_* env vars (RDS_HOST, RDS_PORT, RDS_USER, etc.)
  4. built-in defaults

Auth resolution (when password is empty or RDS_IAM=1):
  1. RDS_IAM_TOKEN env var (pre-computed)
  2. boto3 SDK generate_db_auth_token (preferred)
  3. subprocess aws rds generate-db-auth-token (fallback)
  4. RDS_PASSWORD env var (non-IAM)

Replaces 8 connection pattern variants across 14 active shims:
  - subprocess + RDS_IAM_TOKEN fallback: pist_trace_classify_mcp, joint_classifier,
    pist_prove_and_classify, ingest_57_flexures
  - boto3 SDK: ene_wiki_body_reingest, ene_migrate_and_tag, dataset_ingest_rds
  - subprocess + RDS_PASSWORD: batch_embed_artifacts, sync_wiki_to_rds, seed_flexure_dataset
  - RDS_IAM_AUTH: pist_classify
  - bashrc parsed: credential_loader

v1.4a benchmark confirmed at 100% after refactor.
 2026-05-26 15:09:34 -05:00
Allaun Silverfox
0409a80929 feat(pist): add RRC receipt-density backfill injector 2026-05-26 14:46:13 -05:00
Allaun Silverfox
9629817bb0 feat(pist): add genus-0 sphere shell projection demo 2026-05-26 14:10:17 -05:00
Brandon Schneider
1ff91d138f feat(pist): v1.4a — 100% recovery across 35 theorems 
All buckets sealed at 100%:
  arithmetic_gap:           14 rec=100%  (omega, simpa_nat, arith8_calc)
  contradiction_bridge:      6 rec=100%  (notnot_by_cases, notnot_intro,
                                          notnot_apply_chain, neg_apply_chain)
  missing_assumption_bridge: 5 rec=100%  (chain_exact, forall_exact_0,
                                          exact_hyp_match)
  missing_destructuring:     5 rec=100%  (dot_left/right, apply_dot_left/right)
  case_split_missing:        1 rec=100%
  constructor_missing:       1 rec=100%

Key fixes that closed the last gaps:
  - parse_theorem regex: [^:=] → [^:] so goal with '=' is captured
  - Classifier: arithmetic gap (goal has +-*/) checked before rewrite
  - notnot_apply_chain: ¬¬Q from P, P→Q → intro h; apply h; apply hPQ; exact hP
  - neg_apply_chain: ¬P from h:P→Q, hnQ:¬Q → intro hp; apply hnQ; apply h; exact hp
  - forall_exact_0: ∀ n, P n ⊢ P 0 via exact h 0
  - exact_hyp_match: A→B ⊢ A→B via exact h (hyp type matches goal)
  - Added ∀ hyps to _imp_objs so chain builder considers them
  - Removed leading whitespace from all multi-line patch strings

Ablation: v1.2=36% → v1.3a=36% → v1.3b=54% → v1.4a=100%
 2026-05-26 14:03:59 -05:00
Brandon Schneider
d6f4df42b5 feat(pist): Route-Repair v1.4a — 97% recovery, residual closure 
v1.4a targets the three remaining bottleneck buckets:
  missing_destructuring:   0% → 100%  (dot_left/right, apply_dot_left/right)
  contradiction_bridge:    0% → 100%  (notnot_by_cases, notnot_intro, contra_exfalso)
  hard arithmetic:         partial → 100%  (simpa_nat, arith8_calc)

Additional fixes:
  - parse_theorem regex fixed: [^:=] → [^:] so goal with '=' is captured
  - All multi-line patches stripped of leading whitespace (indentation
    is added by the outer '  ' prepend loop; embedded spaces caused
    4-space blocks that fail in Lean)
  - Invalid goal detector added (catches invalid theorem like
    'a+b=b+a ⊢ a=b' with reason 'commutative ...')
  - Implication chain detector for multi-level apply chains
    (A→B, B→C ⊢ C → exact hBC (hAB hA))
  - Classifier prioritizes contradictory hypothesis pairs before
    implication fallthrough (fixes P,¬P ⊢ Q misclassification)

Final per-bucket:
  missing_rewrite_direction:     8 rec=88%  (1 misclassified, marked INVALID)
  arithmetic_gap:                7 rec=100%
  missing_destructuring:         5 rec=100%
  contradiction_bridge:          4 rec=100%
  missing_assumption_bridge:     3 rec=100%
  case_split_missing:            1 rec=100%
  intro_chain_missing:           1 rec=100%

Ablation: v1.2=36% → v1.3a=36% → v1.3b=54% → v1.4a=97%
 2026-05-26 13:51:05 -05:00
Brandon Schneider
b14c7a924f feat(pist): Route-Repair v1.4 — 71% recovery 2026-05-26 13:09:37 -05:00
Brandon Schneider
77dc9f5361 feat(pist): Route-Repair v1.3b — multi-step templates, 54% recovery 2026-05-26 12:56:24 -05:00
Brandon Schneider
63bdbfa885 feat(pist): Route-Repair v1.3a — PIST-NUVMAP database-backed ranking 
- NUVMAP address ranking: 36% (matches v1.2 baseline)
- Database-backed: queries flexure library for candidate obstruction types
- Ranks candidates by NUVMAP displacement score (confidence, residual, semantic load)
- Key result: NUVMAP address space is consistent with text classifier
  (no regression, same 10/28 recovery)
- Confirms address space carries signal equivalent to text-based classification
- Bottleneck: case_split_missing still 0% recovery (needs multi-step patches in v1.3b)
- Comparison: v1.1=0% → v1.2=36% → v1.3a=36% (NUVMAP preserves)
 2026-05-26 12:49:29 -05:00