Brandon Schneider
bc9b592dbe
docs(infra): update public documentation for virtualized DMA compute backplane
...
- Promote the expanded Virtio-Net Packet-as-Computation (PIST) and QEMU graphics backplane spec from the artifacts directory to 6-Documentation/docs/specs/.
- Update root README.md to highlight virtualized DMA computation fabrics.
- Expand 6-Documentation/INFRASTRUCTURE.md to detail host GPU/APU auto-profiling, lossless color ranges, and framebuffer packing shims.
- Keep AGENTS.md aligned with core surfaces.
Build: 3313 jobs, 0 errors (lake build)
2026-05-30 19:51:24 -05:00
Brandon Schneider
b4133d70b5
docs: enforce lean-proof skill + no-float rule in AGENTS.md Ground Rules
...
- Added lean-proof skill auto-load requirement to Ground Rules
- Added no-Float rule to Ground Rules (front and center)
- lean-proof skill has trigger_patterns for auto-activation
- lean-autoformalization and vcn-compute-substrate also have triggers
- 6 hub skills installed (fpga, systemverilog, verilog-design, math-help, physics-intuition, hardware-counters)
- MCP4EDA registered as MCP server
2026-05-29 00:06:12 -05:00
Brandon Schneider
837ffbc487
feat(lean): add BraidTreeDIATPIST Q0_2 braid compressor with FAMM gate
...
BraidTreeDIATPIST.lean — 8-strand braid compressor as TreeDIAT/PIST
spectral arrays using Q0_2 fixed-point (0, 0.25, 0.5, 0.75) raw-Int
encoding. Implements:
- raw-Int Q0_2 arithmetic (add/mul/abs/sum) with monotone lemmas
- PhaseVec, Strand, State8, ScarBundle, Receipt structures
- fammGate admissibility filter (slot-distinct + bracket-bound)
- crossStep braid-pair crossing with Q0_2 residual accumulation
- eigensolid_convergence theorem (loop stabilizes)
- receipt_invertible theorem (receipt bijectively encodes state)
SSMS.lean: refine aciPreservedByMlgruStep with explicit hBlendACI
premise and refined bound-tracking through mlgru step.
Build: 3313 jobs, 0 errors (lake build Compiler)
2026-05-27 16:10:04 -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
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
d3e18e88f0
docs(agents): add programming choice flow to post-interaction workflow
...
Adds §5 Programming choice flow — a decision tree that runs before writing
any new code. Covers:
- Admissibility / gating / routing logic → Lean only
- Receipt minting / top-level JSON emission → AVMIsa.Emit only (sole boundary)
- Alignment classification → Lean (RRC.Emit or new Semantics.RRC.*)
- Raw input features → Python shim acceptable with strict constraints
(no admissibility logic, regenerable, TODO(lean-port) if portable)
- Float in compute paths → STOP, use Q16_16
- Promotion advancement in shim space → STOP, always not_promoted until
a Lean gate passes
- Pure I/O → Python shim fine, must route receipt output through AVMIsa.Emit
Summary rule: Lean owns all decisions. Python owns all I/O.
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:26:16 -05:00
Brandon Schneider
0a70ba80fe
docs(agents): post-interaction workflow + Compiler surface update
...
Root AGENTS.md:
- Add §Post-Interaction Workflow: mandatory steps after every agent session
that changes code — update AGENTS.md, verify build, commit, check tree
cleanliness. Explicit trigger conditions (file edits, lake build, arch
decisions, new TODO/quarantine). Does NOT trigger for read-only sessions.
- Update AVM glossary entry: ISA is live; AVM is sole output boundary for
RRC receipts; describe AVMIsa.Emit / RRC.Emit / RRC.Corpus278 roles.
Semantics/AGENTS.md:
- Replace stale Blessed Compiler Surface section with current state (commit
3f923e2chttps://cli.devin.ai/docs )
Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
2026-05-26 22:25:26 -05:00
Brandon Schneider
f73d49b342
Add proof worker pool routing
2026-05-25 22:27:18 -05:00
Brandon Schneider
e18a284082
Wire ENE context into remote proof checks
2026-05-25 22:07:58 -05:00
Brandon Schneider
b57e1c2740
Stabilize ENE API and context shim
2026-05-25 21:06:46 -05:00
Brandon Schneider
073a70eb86
WIP: accumulated changes
2026-05-25 16:24:21 -05:00
Brandon Schneider
fd863af6fd
Expand devcontainer with full Python stack, add MCP servers (Notion/AWS), strengthen Lean theorems
...
- .devcontainer/Dockerfile: add PostgreSQL client libs, OpenSSL/libffi headers, gfortran/BLAS for scipy, rclone; install full Python dependency set (boto3, psycopg2-binary, fastapi, uvicorn, notion-client, httpx, pytest, numpy, scipy, etc.) in uv-managed venv; add rclone S3 gateway init script as ENTRYPOINT
- .devcontainer/devcontainer.json: switch from build to pre-built image (localhost/research
2026-05-19 01:52:14 -05:00
Brandon Schneider
d56ef67ec9
Add verified Ollama DeepSeek review emitter
2026-05-11 23:13:54 -05:00
Brandon Schneider
cb96c6bed2
Update repository agent operating contracts
2026-05-11 22:48:54 -05:00
Brandon Schneider
c7989636b7
Document legacy recovery trigger
2026-05-11 15:11:18 -05:00
