Skip to content
  •  
  •  
  •  
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*
101 changes: 52 additions & 49 deletions .trinity/current-issue.md
Original file line number Diff line number Diff line change
@@ -1,97 +1,100 @@
# Wave Loop 419 β€” physical CCLK capture, real relay gate, or instrument-import parity
# Wave Loop 424 β€” 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:** to be created after W423 closes (#1368).
**Branch:** `wave-loop-424`
**Milestone:** Continue the FPGA boot-evidence line from Wave Loop 423.

---

## 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 423 extended the `tri fpga measured-to-lean` import pipeline to handle CSV
time units, VCD real-net slope filtering, unknown timescale units, and PVT
worst-case validation. Wave 424 executes the first available variant from
`docs/reports/FPGA_LOOP_COOPERATION_W424_2026-07-01.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 unit/noise handling.
- Add any missing parser handling exposed by the real export.
- Run a dry-run cold-POR boot-log for OSCFSEL 6/7 variants.
- 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`.
- Land the next safe gen-verilog #1245 sub-fix from the remaining 7 failures,
if one is narrow and regression-free; otherwise explicitly defer.
- Harden `tri fpga boot-log` / `cclk-sweep` cold-POR artifact capture for
manual-power-cycle mode.
- Add small Lean helpers in `TernaryFPGABoot.lean` if future theorems need them.
- 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 hardening |
| 2 | `fpga/HARDWARE_SSOT.md` / `docs/reports` | Updated protocol or comparison note |
| 3 | `docs/reports/*` | W424 report, evidence, W425 cooperation |
| 4 | `.trinity/experience.md` | W424 learnings |
| 5 | git/PR | squash-merge to `master`, close issue, open #? for W425 |

---

## 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 or noise cases.
- [ ] AC-B3: Dry-run boot-log artifacts exist for OSCFSEL 6/7.

### 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: `boot-log` / `cclk-sweep` cold-POR tooling is measurably more robust or better documented.
- [ ] AC-C2: One safe gen-verilog #1245 sub-fix lands without increasing the 7-failure yosys smoke count, or is explicitly deferred if unsafe.
- [ ] AC-C3: 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 #<W424 issue>`
- Report: `docs/reports/WAVE_LOOP_424_REPORT.md`
- Evidence: `docs/reports/FPGA_LOOP_EVIDENCE_W424_YYYY-MM-DD.md`
- Cooperation W425: `docs/reports/FPGA_LOOP_COOPERATION_W425_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
40 changes: 40 additions & 0 deletions .trinity/current_task/activity.md
Original file line number Diff line number Diff line change
Expand Up @@ -1464,3 +1464,43 @@
- **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

Loading
Loading