Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
69 changes: 69 additions & 0 deletions .claude/plans/wave-loop-420.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,69 @@
# Wave Loop 420 β€” Decomposed Plan

**Issue:** #1361
**Branch:** `wave-loop-420`
**Default variant:** C (physical bench still blocked: DLC10 cable not found, P12 unwired, no relay)

---

## 1. Weak points identified

1. **Missing VCD `$comment` exact-token terminator.** The W419 report claimed this
hardening landed, but the merged commit (`101fd0748`) did not touch the VCD
parser. The current code still uses `ends_with("$end")` / `contains(" $end")`
heuristics, so a `$comment` block containing the literal substring `$end`
terminates early and corrupts the signal dictionary.
2. **Real-valued VCD nets require an explicit `--vcd-threshold-v`.** There is no
auto-threshold fallback for analog VCD exports; users must know the voltage
swing up-front.
3. **PVT half-period bound lacks a process-corner monotonicity lemma.** We have
temperature monotonicity and VCCINT antitonicity from W419, but no formal
statement that `ff ≀ tt ≀ ss` is preserved by the half-period bound itself.

---

## 2. Competitor landscape (high-level)

The closest formal-HDL competition is **Sparkle / Verilean** (Lean 4 native,
binary RTL). Other credible players: **Clash** (Haskell, external formal),
**Chisel/FIRRTL/CIRCT** (mainstream, SVA/model-checking oriented),
**Bluespec** (rule-based, Coq bridge via Kami), **Coq Kami / Silver Oak**
(dependent-type hardware), **ACL2** (specification/proof layer only).

None combine Lean 4 native proof, a ternary compute stack, spec-first sealed
`*.t27 β†’ gen/` code generation, and physical boot-evidence instrumentation.
That intersection is the gap t27 fills.

---

## 3. Implementation steps

| Step | Files | Deliverable | Acceptance |
|------|-------|-------------|------------|
| 3.1 | `cli/tri/src/fpga.rs` | Replace VCD `$date`/`$version`/`$comment` terminator heuristics with exact-token check; clear state immediately on same-line termination. | `test_parse_vcd_comment_with_embedded_end_token` PASS |
| 3.2 | `cli/tri/src/fpga.rs` | Add VCD auto-threshold for real-valued nets: compute `50% (vmin + vmax)` when `--vcd-threshold-v` is omitted; warn user. | `test_parse_vcd_real_auto_threshold` PASS |
| 3.3 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | Add `pvt_half_ns_monotone_in_process_corner` lemma: `c1.worse_than c2 β†’ bound c1 ≀ bound c2`. | `lake build` PASS |
| 3.4 | `cli/tri/src/fpga.rs` | Add Rust test `test_pvt_half_ns_monotone_in_process_corner`. | `cargo test` PASS |
| 3.5 | `fpga/HARDWARE_SSOT.md` | Document VCD `$comment` exact-terminator behavior and real-net auto-threshold. | docs render clean |
| 3.6 | `.trinity/experience.md` | Capture W420 learnings. | committed |
| 3.7 | `docs/reports/*` | W420 report, evidence, W421 cooperation variants. | committed |

---

## 4. Verification plan

- `cargo test -p tri vcd` β€” expect 12 tests (was 11).
- `cargo test -p tri pvt` β€” expect 10 tests (was 9).
- `cargo test -p tri fpga::tests` β€” expect 47 tests (was 45).
- `lake build Trinity.TernaryFPGABoot` β€” must PASS.
- `./scripts/tri test` β€” must PASS except 16 pre-existing gen-verilog yosys failures.

---

## 5. Land

- Commit with `Closes #1361`.
- Open PR #? from `wave-loop-420` β†’ `master`.
- After merge, create issue #? and branch `wave-loop-421`.

*φ² + φ⁻² = 3 | TRINITY*
77 changes: 77 additions & 0 deletions .claude/plans/wave-loop-421.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,77 @@
# Wave Loop 421 Decomposed Plan

**Issue:** #1363
**Branch:** `wave-loop-421`
**Date:** 2026-07-06
**Selected variant:** C (fallback β€” hardware still unreachable)

---

## 1. Weak-point analysis

### 1.1 W420 dependency / branch state
- `wave-loop-421` was created from `master` (101fd0748) **before** PR #1362
(Wave Loop 420) merges. This means the W421 branch initially lacked the W420
VCD exact-terminator and auto-threshold work.
- **Mitigation:** reset `wave-loop-421` onto `wave-loop-420` so W421 builds on
top of W420. Once PR #1362 lands, W421 can be rebased onto `master` cleanly.

### 1.2 VCD parser remaining gaps
- `$date` / `$version` / `$comment` sections now use exact-token terminators
(W420), but `$timescale` still uses the old substring heuristics
`contains(" $end")` / `ends_with(" $end")`. A `$timescale` comment that
mentions `$end` could therefore mis-parse.
- Real-valued net auto-threshold works, but has no regression test for a
non-default `$timescale` unit (e.g., `1 us` or `1 ps`).

### 1.3 PVT envelope
- W419/W420 proved each axis independently (temp monotone, VCCINT antitone,
corner monotone). The combined ordering (temp ↑, VCCINT ↓, corner worse) is
not yet a single lemma/test, which is what a worst-case operating-point
search actually needs.

### 1.4 Competition
- Sparkle/Verilean (Lean 4 native HDL) is the closest competitor and is
accelerating in 2026: RV32IMA SoC, networking stack, crypto, formal proofs.
- Clash Formal and CIRCT/Chisel LTL/Verif dialects are also closing the formal
gap from the mainstream side.
- t27 must keep differentiating through: (a) ternary/balanced-trit compute + Lean
proof lattice, (b) spec-first `*.t27 β†’ gen/` sealed pipeline, (c) physical
boot-evidence instrumentation.

### 1.5 Hardware
- The Digilent FTDI cable is present (`0x0403:0x6014`), but `openFPGALoader
--detect` reports **0 devices**. The board is either not powered, not wired,
or the JTAG header is disconnected. Variant A is therefore still blocked.

---

## 2. Work items

| # | File | Change | Test |
|---|------|--------|------|
| 1 | `cli/tri/src/fpga.rs` | Apply `vcd_line_ends_with_token` to `$timescale` terminator | `test_parse_vcd_timescale_with_embedded_end_token` |
| 2 | `cli/tri/src/fpga.rs` | Add non-default `$timescale` real-net parse test | `test_parse_vcd_real_auto_threshold_us_timescale` |
| 3 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | Add combined PVT monotonicity lemma | `lake build Trinity.TernaryFPGABoot` |
| 4 | `cli/tri/src/fpga.rs` | Add combined PVT monotonicity Rust test | `test_pvt_half_ns_monotone_combined` |
| 5 | `docs/reports/T27_VS_FORMAL_HDL_2026.md` | Competitor comparison note | visual review |
| 6 | `fpga/HARDWARE_SSOT.md` | Β§3.6.18 documenting W421 parser + PVT improvements | visual review |
| 7 | `docs/NOW.md` | W421 close-out / W422 setup | visual review |
| 8 | `.trinity/experience.md` | W421 learnings | visual review |
| 9 | `docs/reports/*` | W421 report, evidence, W422 cooperation | visual review |
| 10 | git/PR/issue | Commit, open PR #? for W421, create W422 issue + branch | CI passes |

---

## 3. Verification checklist

- [ ] `cargo test -p tri vcd`: all PASS (was 13).
- [ ] `cargo test -p tri pvt`: all PASS (was 10).
- [ ] `cargo test -p tri fpga::tests`: all PASS (was 48).
- [ ] `lake build Trinity.TernaryFPGABoot`: PASS.
- [ ] `./scripts/tri test`: no new failures beyond the 16 pre-existing yosys
smoke failures from weak point #1245.

---

*φ² + φ⁻² = 3 | TRINITY*
104 changes: 55 additions & 49 deletions .trinity/current-issue.md
Original file line number Diff line number Diff line change
@@ -1,97 +1,103 @@
# Wave Loop 419 β€” physical CCLK capture, real relay gate, or instrument-import parity
# Wave Loop 425 β€” FPGA boot-evidence next variant (physical CCLK / real capture import / formal fallback)

**Issue:** #1357
**Branch:** `wave-loop-419`
**Milestone:** Continue the FPGA boot-evidence line from W418.
**Issue:** #1372
**Branch:** `wave-loop-425`
**Milestone:** Continue the FPGA boot-evidence line from Wave Loop 424.

---

## Goal

Wave 418 closed the Variant C fallback (formal tooling and instrument import).
Wave 419 re-evaluates the bench state and executes the first available variant.
Wave 424 hardened the FPGA CLI so that `boot-log`, `cold-por`, and
`cclk-sweep` auto-continue, embed PVT/XADC context, and import CSV captures in
volts or millivolts. Wave 425 executes the first available variant from
`docs/reports/FPGA_LOOP_COOPERATION_W425_2026-07-05.md`.

1. **Variant A (preferred when bench becomes available):**
- Wire P12 to a logic-analyzer channel and capture real CCLK for
`OSCFSEL=6` and `OSCFSEL=7`.
- Program each variant to SPI flash and perform a true cold-POR boot.
- Confirm P12 is wired to a logic-analyzer channel.
- Capture real CCLK for `OSCFSEL=6` and `OSCFSEL=7`.
- Import the captures with `tri fpga measured-to-lean --csv/--vcd --raw-ns
--standalone --validate --pvt-context <ctx.json>` and commit the generated
Lean theorems.
- Document the measured frequencies/duty cycles and PVT context in
`fpga/HARDWARE_SSOT.md`.
- Program each OSCFSEL variant to SPI flash and perform a true cold-POR boot.
- Document measured frequencies/duty cycles and PVT context in
`fpga/HARDWARE_SSOT.md` Β§3.6.21.

2. **Variant B (if relay hardware is available, no CCLK probe):**
- Implement a real `--relay-port` backend for `tri fpga cold-por`
(e.g. serial or TCP relay controlling board power).
- Perform an automated cold-POR power-cycle and capture STAT without
operator intervention.
- Document relay wiring and port syntax in `fpga/HARDWARE_SSOT.md`.
2. **Variant B (if an external capture is available or the board is reachable for dry-run boot-log):**
- Import at least one real or representative CCLK capture end-to-end using the
W423–W424 unit/noise/voltage-unit handling.
- Add any missing parser handling exposed by the real export.
- Run a dry-run cold-POR boot-log for OSCFSEL 6/7 variants with `--pvt-context`.
- Document the import recipe in `fpga/HARDWARE_SSOT.md` Β§3.6.21.

3. **Variant C (fallback if bench still blocked):**
- Extend instrument-import parity: additional VCD/CSV formats and hardened
`$comment` sections.
- Add PVT envelope monotonicity/antitonicity tests in Rust and Lean.
- Document the standalone `lake`-package workflow end-to-end in
`fpga/HARDWARE_SSOT.md`.
- Implement real XADC readout in `tri fpga boot-log` / `cclk-sweep` so the JSON
`xadc` object has `source: "xadc"` and live temp/vccint/vccaux values; or
document the deferral if it is unsafe for the branch.
- Land the next safe gen-verilog #1245 sub-fix from the remaining 7 failures,
if one is narrow and regression-free; otherwise explicitly defer.
- Continue hardening `tri fpga boot-log` / `cold-por` / `cclk-sweep` JSON schema
and decision-tree output.
- Update `docs/reports/T27_VS_FORMAL_HDL_2026.md` if any new 2026 competitor
developments surface.

---

## Decomposed plan

See `docs/reports/FPGA_LOOP_COOPERATION_W419_2026-07-04.md` and
`.claude/plans/wave-loop-419.md`.

| Step | File(s) | Deliverable |
|------|---------|-------------|
| 1 | `cli/tri/src/fpga.rs` | Variant A import, B relay backend, or C parity/monotonicity tests |
| 2 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | PVT monotonicity lemmas or new measured theorems |
| 3 | `fpga/HARDWARE_SSOT.md` | Updated capture / relay / integration protocol |
| 4 | `docs/reports/*` | W419 report, evidence, W420 cooperation |
| 5 | `.trinity/experience.md` | W419 learnings |
| 6 | git/PR | squash-merge to `master`, close #1357, open #? for W420 |
| 1 | `cli/tri/src/fpga.rs` or `bootstrap/src/compiler.rs` or `proofs/lean4/Trinity/TernaryFPGABoot.lean` | Variant A capture import, B import/dry-run, or C parser/formal/gen-verilog/XADC hardening |
| 2 | `fpga/HARDWARE_SSOT.md` / `docs/reports` | Updated protocol or comparison note |
| 3 | `docs/reports/*` | W425 report, evidence, W426 cooperation |
| 4 | `.trinity/experience.md` | W425 learnings |
| 5 | git/PR | squash-merge to `master`, close issue, open #? for W426 |

---

## Acceptance criteria

### Bundle A
- [ ] AC-A1: P12 is wired to a logic-analyzer channel and real CCLK capture files exist for `OSCFSEL=6` and `OSCFSEL=7`.
- [ ] AC-A1: Real CCLK capture for `OSCFSEL=6` and `OSCFSEL=7` exists.
- [ ] AC-A2: `tri fpga measured-to-lean --csv/--vcd --raw-ns --standalone` generated Lean files build with `lake build`.
- [ ] AC-A3: Measured CCLK satisfies the PVT-aware flash spec, or any exceedance is explicitly explained.
- [ ] AC-A4: Cold-POR SPI flash boot for OSCFSEL 6/7 is documented with STAT reads.

### Bundle B
- [ ] AC-B1: `tri fpga cold-por <bit> --relay-port <real>` performs an automated power-cycle and captures STAT.
- [ ] AC-B2: The resulting log has `relay_mock: false` and a real STAT raw value.
- [ ] AC-B3: `fpga/HARDWARE_SSOT.md` documents relay wiring and port syntax.
- [ ] AC-B1: At least one real or representative CCLK/CSV/VCD capture is imported end-to-end.
- [ ] AC-B2: The import path exposes no unhandled unit, voltage-unit, or noise cases.
- [ ] AC-B3: Dry-run boot-log artifacts exist for OSCFSEL 6/7 and include PVT/XADC context fields.

### Bundle C
- [x] AC-C1: At least one additional instrument-import unit test lands (VCD `$comment` hardening + CSV `--csv-channel` explicit select).
- [x] AC-C2: Rust and Lean tests verify PVT envelope monotonicity/antitonicity.
- [x] AC-C3: The standalone lake-package workflow is documented end-to-end.
- [ ] AC-C1: Real XADC readout lands in boot-log/cclk-sweep JSON, or the deferral is documented.
- [ ] AC-C2: `boot-log` / `cold-por` / `cclk-sweep` tooling is measurably more robust or better documented.
- [ ] AC-C3: One safe gen-verilog #1245 sub-fix lands without increasing the 7-failure yosys smoke count, or is explicitly deferred if unsafe.
- [ ] AC-C4: Competitor snapshot is updated if any new 2026 developments are found.

### Invariant checks
- [x] `./scripts/tri test` parse/typecheck/gen/seal-verify phases pass.
- [x] `lake build Trinity.TernaryFPGABoot` passes.
- [x] `cargo test -p tri fpga::tests` passes.
- [ ] `./scripts/tri test` parse/typecheck/gen/seal-verify phases pass.
- [ ] `lake build Trinity.TernaryFPGABoot` passes.
- [ ] `cargo test -p tri fpga::tests` passes.

---

## PR

- Target: `master`
- PR: #1360
- Body: `Closes #1357`
- Report: `docs/reports/WAVE_LOOP_419_REPORT.md`
- Evidence: `docs/reports/FPGA_LOOP_EVIDENCE_W419_2026-07-05.md`
- Cooperation W420: `docs/reports/FPGA_LOOP_COOPERATION_W420_2026-07-05.md`
- PR: to open after work
- Body: `Closes #1372`
- Report: `docs/reports/WAVE_LOOP_425_REPORT.md`
- Evidence: `docs/reports/FPGA_LOOP_EVIDENCE_W425_YYYY-MM-DD.md`
- Cooperation W426: `docs/reports/FPGA_LOOP_COOPERATION_W426_YYYY-MM-DD.md`

---

## Default variant

Execute **Variant A** if the analyzer and DLC10 cable are available. Otherwise
try **Variant B** if a relay and DLC10 cable are available. Otherwise fall back
to **Variant C**.
Execute **Variant A** if P12 is wired and the analyzer is ready.
Otherwise execute **Variant B** if an external capture is available or the board
is reachable for a dry-run boot-log.
Otherwise fall back to **Variant C**.

---

Expand Down
2 changes: 1 addition & 1 deletion .trinity/current_task/.commit_count
Original file line number Diff line number Diff line change
@@ -1 +1 @@
1807
1816
60 changes: 60 additions & 0 deletions .trinity/current_task/activity.md
Original file line number Diff line number Diff line change
Expand Up @@ -1464,3 +1464,63 @@
- **Commit:** docs(w420): set W420 issue number to #1361 and record W419 PR #1360 (Closes #1357, Refs #1361)
- **Files:** .trinity/current-issue.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W420_2026-07-05.md,docs/reports/FPGA_LOOP_EVIDENCE_W419_2026-07-05.md,docs/reports/WAVE_LOOP_419_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean

## 2026-07-04T18:36:50Z β€” wave-loop-420
- **Commit:** feat(igla): Wave Loop 419 β€” Variant C VCD/CSV hardening, PVT monotonicity, standalone lake workflow
- **Files:** .trinity/current-issue.md

## 2026-07-04T18:37:55Z β€” wave-loop-420
- **Commit:** setup(igla): initialize Wave Loop 420 current issue (#1361)
- **Files:** .trinity/current-issue.md,.trinity/current_task/activity.md,docs/NOW.md

## 2026-07-04T19:27:38Z β€” wave-loop-420
- **Commit:** setup(igla): initialize Wave Loop 420 current issue and NOW.md update
- **Files:** .claude/plans/wave-loop-420.md,.trinity/current-issue.md,.trinity/current_task/activity.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W421_2026-07-06.md,docs/reports/FPGA_LOOP_EVIDENCE_W420_2026-07-06.md,docs/reports/WAVE_LOOP_420_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean

## 2026-07-04T19:30:24Z β€” wave-loop-420
- **Commit:** feat(igla): Wave Loop 420 β€” VCD exact-terminator + real-net auto-threshold, PVT process-corner monotonicity
- **Files:** docs/NOW.md

## 2026-07-04T19:34:37Z β€” wave-loop-421
- **Commit:** docs(issue): set current issue to Wave Loop 421\n\nCloses #1363\n\nCo-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- **Files:** .trinity/current-issue.md

## 2026-07-04T19:44:52Z β€” wave-loop-421
- **Commit:** docs(issue): set current issue to Wave Loop 421
- **Files:** .claude/plans/wave-loop-421.md,.trinity/current-issue.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W422_2026-07-06.md,docs/reports/FPGA_LOOP_EVIDENCE_W421_2026-07-06.md,docs/reports/T27_VS_FORMAL_HDL_2026.md,docs/reports/WAVE_LOOP_421_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean

## 2026-07-04T19:45:56Z β€” wave-loop-422
- **Commit:** docs(issue): set current issue to Wave Loop 422\n\nCloses #1365\n\nCo-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- **Files:** .trinity/current-issue.md

## 2026-07-05T06:22:32Z β€” wave-loop-422
- **Commit:** docs(issue): set current issue to Wave Loop 422\n\nCloses #1365\n\nCo-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- **Files:** .trinity/experience.md,.trinity/seals/account_Account.json,.trinity/seals/account_AccountAuth.json,.trinity/seals/account_AccountRepo.json,.trinity/seals/activation_Elu.json,.trinity/seals/activation_Gelu.json,.trinity/seals/activation_GeluApprox.json,.trinity/seals/activation_LeakyRelu.json,.trinity/seals/activation_Relu.json,.trinity/seals/activation_Sigmoid.json,.trinity/seals/activation_SiluSwish.json,.trinity/seals/activation_SiluSwishVbt.json,.trinity/seals/activation_Softmax.json,.trinity/seals/activation_Tanh.json,.trinity/seals/agent_AutonomousUniverse.json,.trinity/seals/agent_EternalMonitor.json,.trinity/seals/agent_FacultyBoard.json,.trinity/seals/agent_Handoff.json,".trinity/seals/agent_Str = \"\",.json",.trinity/seals/agent_String # phi, trinity, gematria, evolution, safety.json

## 2026-07-05T06:23:51Z β€” wave-loop-423
- **Commit:** feat(igla): Wave Loop 422 β€” live XC7A200T SRAM boot, Verilog keyword escape, PVT worst-case bound
- **Files:** .trinity/current-issue.md

## 2026-07-05T06:47:22Z β€” wave-loop-423
- **Commit:** docs(issue): set current issue to Wave Loop 423
- **Files:** .trinity/current-issue.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W424_2026-07-05.md,docs/reports/FPGA_LOOP_EVIDENCE_W423_2026-07-05.md,docs/reports/T27_VS_FORMAL_HDL_2026.md,docs/reports/WAVE_LOOP_423_REPORT.md,fpga/HARDWARE_SSOT.md

## 2026-07-05T06:48:03Z β€” wave-loop-424
- **Commit:** feat(igla): Wave Loop 423 β€” CSV time units, VCD slope filter, PVT worst-case, competitor refresh (Closes #1368)
- **Files:** .trinity/current-issue.md,docs/reports/FPGA_LOOP_COOPERATION_W424_2026-07-05.md

## 2026-07-05T07:13:01Z β€” wave-loop-424
- **Commit:** setup(igla): Wave Loop 424 branch and issue (#1371)
- **Files:** .trinity/current-issue.md,.trinity/current_task/.commit_count,.trinity/current_task/session_log.jsonl,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W425_2026-07-05.md,docs/reports/FPGA_LOOP_EVIDENCE_W424_2026-07-05.md,docs/reports/T27_VS_FORMAL_HDL_2026.md,docs/reports/WAVE_LOOP_424_REPORT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean

## 2026-07-05T07:13:28Z β€” wave-loop-424
- **Commit:** feat(igla): Wave Loop 424 β€” FPGA tooling hardening, PVT context, CSV voltage units, non-blocking continue, W425 setup
- **Files:** .trinity/current_task/.commit_count,.trinity/current_task/session_log.jsonl

## 2026-07-05T07:15:04Z β€” wave-loop-424
- **Commit:** docs(tri): W425 issue + NOW setup (#1374, wave-loop-425)
- **Files:** docs/reports/FPGA_LOOP_COOPERATION_W425_2026-07-05.md

## 2026-07-05T07:15:09Z β€” wave-loop-424
- **Commit:** docs(tri): correct W425 issue reference to #1374
- **Files:** .trinity/current_task/activity.md,docs/reports/FPGA_LOOP_COOPERATION_W425_2026-07-05.md

Loading
Loading