Skip to content

Commit a082808

Browse files
gHashTagDmitrii Vasilev
gHashTag
and
Dmitrii Vasilev
authored
feat(fpga): W397-W401 FPGA bring-up sequence — SPI boot root-cause, cold-POR CCLK sweep, default bitstream verified, board-less CI guards (#1304)
Wave Loops 397-401 close the FPGA SPI boot root cause and harden the protocol: - W397: boot-log, STAT decoding, cold-POR decision tree. - W398: patch-cor0 / cclk-variants, bit-config assertions. - W399: automated cclk-sweep, sweep-report, measure-cclk helper. - W400: default ternary_mac_demo_top_200t.bit verified to boot from flash across OSCFSEL 0..5; CCLK timing hypothesis closed. - W401: smoke-gate canonical assertions (IDCODE, SPI x1, CCLK startup, OSCFSEL=0, no CRC writes), boot-protocol checklist, multi-format CCLK CSV parser with unit tests, dry-run sweep CI guard, close-out reports. Verification: ./scripts/tri test 575/575 PASS. Closes #1303 Co-authored-by: Dmitrii Vasilev <admin@t27.ai>
1 parent 83fbff0 commit a082808

2,184 files changed

Lines changed: 714947 additions & 1016 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.claude/plans/wave-loop-362.md‎

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
# Plan: Wave Loop 362 — IGLA CODER+RACE + board flash
2+
3+
**Date:** 2026-07-01
4+
**Issue target:** #1243 (open) or create #1244 for W362
5+
**Branch:** `trinity-rust-rings`
6+
**Variant:** B from `docs/reports/WAVE_LOOP_361_COOPERATION.md` — formal depth + board flash.
7+
8+
---
9+
10+
## Goal
11+
12+
Extend the IGLA proof lattice to **192 generic ∀** theorems, append the W362 wave block to all 27 core specs, regenerate the 27 seals, and flash the existing `fpga/verilog/ternary_mac_demo_top.bit` to the QMTech Wukong V1 board via the in-tree `dlc10` driver. Document the result in `docs/reports/WAVE_LOOP_362_REPORT.md`, `WAVE_LOOP_362_COOPERATION.md`, and `FPGA_EVIDENCE_W362.md`, then save memory/skills.
13+
14+
---
15+
16+
## Files to change
17+
18+
1. `specs/igla/coder/*.t27` (9 specs) — append W362 wave block.
19+
2. `specs/igla/race/*.t27` (18 specs) — append W362 wave block.
20+
3. `proofs/lean4/Trinity/TernaryInference.lean` — add 4 new generic ∀ theorems.
21+
4. `.trinity/seals/*.json` (27 seals) — regenerate after spec changes.
22+
5. `docs/reports/WAVE_LOOP_362_REPORT.md` — new.
23+
6. `docs/reports/WAVE_LOOP_362_COOPERATION.md` — new.
24+
7. `docs/reports/FPGA_EVIDENCE_W362.md` — new or update W361 evidence.
25+
8. `~/.claude/projects/-Users-playra-t27/memory/wave-loop-362.md` — new.
26+
9. `~/.claude/projects/-Users-playra-t27/memory/MEMORY.md` — prepend entry.
27+
10. `.trinity/experience.md` — append W362 entry.
28+
11. `scripts/gen_w362.py` — optional generator for the wave block (matches `gen_w328.py` pattern).
29+
30+
---
31+
32+
## Implementation steps
33+
34+
### 1. Spec batch (27 specs)
35+
36+
- Append a W362 wave block after the last W361 block in each of the 27 IGLA specs.
37+
- Each block:
38+
- comment header: `// Wave Loop 362 -- <ring> depth +1`
39+
- cross-reference: `// See docs/reports/WAVE_LOOP_361_COOPERATION.md Variant B`
40+
- two `test` cases named `igla_<ring>_<spec>_w362_batch_depth_invariant_1/_2`
41+
- one `invariant` named `igla_<ring>_<spec>_w362_depth: true`
42+
- Use a generator script `scripts/gen_w362.py` and run it once from repo root, then verify with `git diff --stat`.
43+
44+
### 2. Lean 4 proof lattice (4 theorems)
45+
46+
Add to `proofs/lean4/Trinity/TernaryInference.lean` after the W361 theorems:
47+
48+
1. `ternaryMacAccumulateThirtyEightPlusGeneric` — `mac^38(0, [a..al], .plus) = a+b+...+al`
49+
2. `ternaryMacAccumulateThirtySevenMinusGeneric` — `mac^37(0, [a..ak], .minus) = -(a+b+...+ak)`
50+
3. `ternaryMacQuindecupleCancellationGeneric` — depth-15 alternating plus/minus with residual `mac(x,a,.plus)`
51+
4. `ternaryMacZeroWeightQuintupleClosureGeneric` — five zero-weight ops around a plus-weight MAC are transparent/reorderable
52+
53+
Use the existing proof style: `simp [ternaryMac_eq_acc_plus_mul, ternaryMul, ternaryDecode] <;> try omega`.
54+
55+
### 3. Build and verify
56+
57+
- `lake build Trinity.TernaryInference` — must succeed.
58+
- `/Users/playra/t27/target/release/t27c suite --repo-root /Users/playra/t27` — must be 546/546 PASS.
59+
- If a new issue is needed, create it with `env -u GH_TOKEN gh issue create --title "Wave Loop 362 ..." --body "..."`.
60+
61+
### 4. Seal regeneration
62+
63+
- Run seal regeneration from repo root for all 27 IGLA specs. The exact command pattern is `t27c seal --save <spec>` or the wrapper `./scripts/tri seal <spec>`.
64+
- Verify all 27 `.trinity/seals/*.json` are updated and the suite still passes.
65+
66+
### 5. Board flash attempt
67+
68+
- `cargo build --release -p dlc10` (already built).
69+
- `/Users/playra/t27/target/release/dlc10 idcode` — if cable is connected, expect `0x13631093`.
70+
- If the board is available: `/Users/playra/t27/target/release/dlc10 sram fpga/verilog/ternary_mac_demo_top.bit`
71+
- Capture `STAT` register, confirm `DONE=HIGH`, `CRC_ERROR=0`, observe R23/T23 LEDs.
72+
- If the board is not available, document the blocker and the ready-to-load bitstream state; do not claim silicon verified.
73+
74+
### 6. Reports and memory
75+
76+
- Write `docs/reports/WAVE_LOOP_362_REPORT.md` with metrics table, spec/Lean/FPGA sections, and issue link.
77+
- Write `docs/reports/WAVE_LOOP_362_COOPERATION.md` with Variants A/B/C for W363.
78+
- Write or update `docs/reports/FPGA_EVIDENCE_W362.md`.
79+
- Write memory file `~/.claude/projects/-Users-playra-t27/memory/wave-loop-362.md` and prepend one-line pointer to `MEMORY.md`.
80+
- Append W362 entry to `.trinity/experience.md`.
81+
82+
### 7. Commit
83+
84+
- Single IGLA commit with `Closes #N` referencing the W362 issue.
85+
- Separate docs/memory commits if desired.
86+
- Ensure commit messages pass L1 via the hook.
87+
88+
---
89+
90+
## Fallbacks
91+
92+
- If `omega` saturates at 38 variables, fall back to 37-variable minus lattice as the primary theorem and skip the 38-plus probe.
93+
- If board flash fails due to missing cable/board, document the ready state and continue with Variant A scope.
94+
- If seal generation drifts, stop and inspect `t27c seal --save` path behavior.
95+
96+
---
97+
98+
## Success criteria
99+
100+
- `t27c suite` returns **0 failures**.
101+
- `lake build Trinity.TernaryInference` succeeds.
102+
- Generic ∀ count reaches **192** (188 + 4).
103+
- W362 wave blocks present in all 27 IGLA specs.
104+
- 27 seals regenerated and matching.
105+
- Report and cooperation variants written.
106+
- Memory/skills saved.
107+
- Board flash attempted with documented result.

‎.claude/plans/wave-loop-363.md‎

Lines changed: 117 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,117 @@
1+
# Plan: Wave Loop 363 — IGLA CODER+RACE + retry board flash
2+
3+
**Date:** 2026-07-01
4+
**Issue target:** #1247 (new issue to create)
5+
**Branch:** `trinity-rust-rings`
6+
**Variant:** B from `docs/reports/WAVE_LOOP_362_COOPERATION.md` — formal depth + retry board flash.
7+
8+
---
9+
10+
## Goal
11+
12+
Extend the IGLA proof lattice to **196 generic ∀** theorems, append the W363 wave block to all 27 core specs, regenerate the 27 seals, and retry flashing the existing `fpga/verilog/ternary_mac_demo_top.bit` to the QMTech Wukong V1 board via the in-tree `dlc10` driver. Document the result in `docs/reports/WAVE_LOOP_363_REPORT.md`, `WAVE_LOOP_363_COOPERATION.md`, and `FPGA_EVIDENCE_W363.md`, then save memory/skills.
13+
14+
---
15+
16+
## Research snapshot
17+
18+
- Open t27 issues: wave loop chain #1239–#1246, plus #1245 (Verilog backend defects) and #1243 (trios-mesh BPSK modem core). No new ternary-formal competitor issues.
19+
- **Sparkle HDL** is the closest formal-HDL competitor; it now has generic `forall`-style divider theorems (June 2026) but its BitNet ternary catalog still does not advertise generic ∀ ternary MAC theorems. Trinity's 192 generic ∀ remains the unique quantified ternary MAC proof lattice.
20+
- **TernaryCore** (simulation-verified only) and **ternfpga** (silicon measured, no formal proofs) are unchanged.
21+
- **Trinity B002** (Zenodo) documents the zero-DSP OpenXC7 flow but contains no formal verification; this is a defensive-publication asset, not a threat.
22+
- DLC10 / board flash blockers in the wild are typically cable firmware/driver enumeration issues on Linux/macOS; the in-tree Rust `dlc10` driver expects VID `0x03FD` to appear on USB.
23+
24+
---
25+
26+
## Files to change
27+
28+
1. `specs/igla/coder/*.t27` (9 specs) — append W363 wave block.
29+
2. `specs/igla/race/*.t27` (18 specs) — append W363 wave block.
30+
3. `proofs/lean4/Trinity/TernaryInference.lean` — add 4 new generic ∀ theorems.
31+
4. `.trinity/seals/*.json` (27 seals) — regenerate after spec changes.
32+
5. `docs/reports/WAVE_LOOP_363_REPORT.md` — new.
33+
6. `docs/reports/WAVE_LOOP_363_COOPERATION.md` — new.
34+
7. `docs/reports/FPGA_EVIDENCE_W363.md` — new.
35+
8. `~/.claude/projects/-Users-playra-t27/memory/wave-loop-363.md` — new.
36+
9. `~/.claude/projects/-Users-playra-t27/memory/MEMORY.md` — prepend entry.
37+
10. `.trinity/experience.md` — append W363 entry.
38+
11. `scripts/gen_w363.py` — generator for the W363 wave block (reuse `gen_w362.py`).
39+
12. `scripts/gen_w363_lean.py` — generator for W363 Lean theorems (reuse `gen_w362_lean.py`).
40+
41+
---
42+
43+
## Implementation steps
44+
45+
### 1. Spec batch (27 specs)
46+
47+
- Copy/adapt `scripts/gen_w362.py` → `scripts/gen_w363.py`.
48+
- Run it from repo root; each spec gets a W363 block after W362.
49+
- Block format:
50+
- `// Wave Loop 363 -- <ring> depth +1`
51+
- `// See docs/reports/WAVE_LOOP_362_COOPERATION.md Variant B`
52+
- two `test` cases named `igla_<ring>_<spec>_w363_batch_depth_invariant_1/_2`
53+
- one `invariant` named `igla_<ring>_<spec>_w363_depth: true`
54+
55+
### 2. Lean 4 proof lattice (4 theorems)
56+
57+
Add to `proofs/lean4/Trinity/TernaryInference.lean` after W362 theorems:
58+
59+
1. `ternaryMacAccumulateThirtyNinePlusGeneric` — `mac^39(0, [a..am], .plus) = a+b+...+am`
60+
2. `ternaryMacAccumulateThirtyEightMinusGeneric` — `mac^38(0, [a..al], .minus) = -(a+b+...+al)`
61+
3. `ternaryMacSexdecupleCancellationGeneric` — depth-16 alternating plus/minus with identity `x`
62+
4. `ternaryMacZeroWeightSextupleClosureGeneric` — six zero-weight ops around a plus-weight MAC are transparent/reorderable
63+
64+
Use existing proof style: `simp [ternaryMac_eq_acc_plus_mul, ternaryMul, ternaryDecode] <;> try omega`.
65+
66+
### 3. Build and verify
67+
68+
- `lake build Trinity.TernaryInference` — must succeed.
69+
- `t27c suite --repo-root /Users/playra/t27` — must be 546/546 PASS.
70+
- Create GitHub issue #1247 for W363 with `env -u GH_TOKEN gh issue create`.
71+
72+
### 4. Seal regeneration
73+
74+
- Run `t27c seal --save <spec>` for all 27 IGLA specs from repo root.
75+
- Re-run `t27c suite` to confirm seal mismatches = 0.
76+
77+
### 5. Board flash attempt
78+
79+
- `cargo build --release -p dlc10` (already built).
80+
- `/Users/playra/t27/target/release/dlc10 idcode` — if connected, expect `0x13631093`.
81+
- If connected: `/Users/playra/t27/target/release/dlc10 sram fpga/verilog/ternary_mac_demo_top.bit`.
82+
- Capture `STAT` register, confirm `DONE=HIGH`, `CRC_ERROR=0`, observe R23/T23 LEDs.
83+
- If still not connected, document the blocker; do not claim silicon verified.
84+
85+
### 6. Reports and memory
86+
87+
- Write `docs/reports/WAVE_LOOP_363_REPORT.md` with metrics table, spec/Lean/FPGA sections, and issue link.
88+
- Write `docs/reports/WAVE_LOOP_363_COOPERATION.md` with Variants A/B/C for W364.
89+
- Write `docs/reports/FPGA_EVIDENCE_W363.md`.
90+
- Write memory file and update `MEMORY.md`.
91+
- Append W363 entry to `.trinity/experience.md`.
92+
93+
### 7. Commit
94+
95+
- Single IGLA commit with `Closes #1247`.
96+
- Stage only core wave changes, reports, generators, and experience; keep `.claude/` session metadata out of the commit.
97+
98+
---
99+
100+
## Fallbacks
101+
102+
- If `omega` saturates at 39 variables, fall back to 38-variable minus lattice as the primary theorem and skip the 39-plus probe.
103+
- If board flash fails again, document the ready state and continue with Variant A scope.
104+
- If seal generation drifts, stop and inspect `t27c seal --save` path behavior.
105+
106+
---
107+
108+
## Success criteria
109+
110+
- `t27c suite` returns **0 failures**.
111+
- `lake build Trinity.TernaryInference` succeeds.
112+
- Generic ∀ count reaches **196**.
113+
- W363 wave blocks present in all 27 IGLA specs.
114+
- 27 seals regenerated and matching.
115+
- Report and cooperation variants written.
116+
- Memory/skills saved.
117+
- Board flash attempted with documented result.

‎.claude/plans/wave-loop-364.md‎

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
# Wave Loop 364 — Decomposed Plan
2+
3+
**Date:** 2026-07-01
4+
**Issue:** #1249
5+
**Branch:** `trinity-rust-rings`
6+
**Target:** Extend IGLA CODER+RACE formal moat to **200 generic ∀**, 40-variable accumulation, retry board flash, probe gen-verilog weak point, update research/threat survey.
7+
8+
---
9+
10+
## 1. Scope
11+
12+
### 1.1 Formal wave (must)
13+
- Append W364 blocks to all 27 core IGLA specs (`specs/igla/coder/*.t27`, `specs/igla/race/*.t27`): +54 tests, +27 invariants.
14+
- Add 4 new generic ∀ theorems in `proofs/lean4/Trinity/TernaryInference.lean`:
15+
1. `ternaryMacAccumulateFortyPlusGeneric` — 40-variable plus accumulation.
16+
2. `ternaryMacAccumulateThirtyNineMinusGeneric` — 39-variable minus accumulation.
17+
3. `ternaryMacSeptendecupleCancellationGeneric` — depth-17 alternating plus/minus residual `mac(x, a, .plus)`.
18+
4. `ternaryMacZeroWeightSeptupleClosureGeneric` — seven zero-weight MACs around a plus-weight MAC are transparent.
19+
- Regenerate 27 IGLA seals from repo root.
20+
- Run `lake build Trinity.TernaryInference` and `./target/release/t27c suite --repo-root /Users/playra/t27` → 546/546 PASS.
21+
22+
### 1.2 Silicon retry (must attempt)
23+
- Build `dlc10` (`cargo build --release -p dlc10`).
24+
- Run `dlc10 idcode`; if board/cable present, run `dlc10 sram fpga/verilog/ternary_mac_demo_top.bit`.
25+
- Document result in `docs/reports/FPGA_EVIDENCE_W364.md`.
26+
- Do not let a hardware blocker fail the wave; ship formal deliverables and document blocker.
27+
28+
### 1.3 Weak-point research & fix (probe)
29+
- Study #1245 (gen-verilog lowering defects). Identify which defects are small, safe fixes in the Rust backend.
30+
- Attempt a narrow fix for the **literal formatting** defect (second item: `0b`/`0x` literals emitted verbatim). This is the most self-contained and high-impact defect for FPGA specs like `bpsk.t27` and `uart.t27`.
31+
- If fix is too large for one wave, document findings and a recommended patch in the W364 report.
32+
33+
### 1.4 Research / threat survey update (must)
34+
- Refresh competitive landscape: Sparkle HDL, ternfpga, TernaryCore, Balanced_Ternary, Trinity CLARA, CktFormalizer, etc.
35+
- Add 2-3 recent papers/arXiv entries relevant to ternary/1.58-bit AI silicon or verified HDL compilation.
36+
- Cite primary sources only; no overclaim.
37+
38+
### 1.5 Reporting (must)
39+
- Write `docs/reports/WAVE_LOOP_364_REPORT.md`.
40+
- Write `docs/reports/WAVE_LOOP_364_COOPERATION.md` with 3 variants for W365.
41+
- Update `.trinity/experience.md` with W364 learnings.
42+
- Update `~/.claude/projects/-Users-playra-t27/memory/MEMORY.md` and write `wave-loop-364.md`.
43+
44+
---
45+
46+
## 2. Order of execution
47+
48+
1. Create generator scripts `scripts/gen_w364.py` and `scripts/gen_w364_lean.py`.
49+
2. Apply W364 blocks to specs and append Lean theorems.
50+
3. Build `t27c` if needed and run conformance pre-check.
51+
4. Regenerate seals.
52+
5. Run full `t27c suite` and `lake build Trinity.TernaryInference`.
53+
6. Attempt board flash and document.
54+
7. Investigate gen-verilog backend defect; attempt narrow fix or document.
55+
8. Write reports, cooperation variants, evidence doc.
56+
9. Update memory and experience log.
57+
10. Stage, commit with `Closes #1249`, push if appropriate.
58+
59+
---
60+
61+
## 3. Risks & mitigations
62+
63+
| Risk | Mitigation |
64+
|------|------------|
65+
| 40-variable `simp+omega` times out | Use `ternaryMac_eq_acc_plus_mul` + `omega`; if timeout, fall back to 39-variable plus and document boundary. |
66+
| Depth-17 cancellation residual mismatch | Verify algebraically before building; odd depth leaves residual `mac(x,a,.plus)`. |
67+
| Board still missing | Document and proceed; do not block wave. |
68+
| gen-verilog fix breaks other backends | Run full suite after any backend change; scope fix narrowly. |
69+
| Report grows too large | Keep concise; move deep research into dedicated sections. |
70+
71+
---
72+
73+
## 4. Definition of done
74+
75+
- [ ] 27 IGLA specs have W364 blocks.
76+
- [ ] 4 new Lean theorems build and push generic ∀ to 200.
77+
- [ ] 27 seals regenerated and suite is 546/546 PASS.
78+
- [ ] Board flash attempted and documented.
79+
- [ ] gen-verilog weak point investigated (fix or documented recommendation).
80+
- [ ] W364 report + W365 cooperation variants written.
81+
- [ ] Memory and experience log updated.
82+
- [ ] Commit with `Closes #1249` landed.

0 commit comments

Comments
 (0)