Skip to content
Merged
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
Jump to file
Failed to load files.
Loading
Diff view
Diff view
89 changes: 21 additions & 68 deletions .trinity/current-issue.md
Original file line number Diff line number Diff line change
@@ -1,89 +1,42 @@
# Wave Loop 416PVT-envelope CLI, VCD parser coverage, OSCFSEL transaction theorems
# Wave Loop 417hygiene, reland W415/W416, and next-variant gate

**Issue:** #1347
**Branch:** `wave-loop-416`
**Milestone:** Continue the FPGA boot-evidence line from W415.
**Issue:** #1350
**Branch:** `wave-loop-417`
**Milestone:** Close out the W415/W416 reland mess and set up the next FPGA boot-evidence wave.

---

## Goal

Wave 415 delivered the **Variant C** formal-tooling fallback because the bench
was still blocked. Wave 416 re-evaluates the bench state and executes the first
available variant.

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`.
- 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`.

2. **Variant B (if relay hardware is available):**
- 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 in `fpga/HARDWARE_SSOT.md`.

3. **Variant C (fallback if bench still blocked):**
- Add a PVT-envelope CLI helper (`tri fpga pvt-envelope`).
- Prove monotonicity of the PVT derating functions in Lean 4.
- Extend VCD parser coverage for escaped identifiers, scalar x/z transitions,
and hex bus literals.
- Link the OSCFSEL 0..7 nominal theorems to
`transaction_satisfies_flash_spec` proofs.
Wave 415 and Wave 416 were stuck on a dirty PR (#1346) and a branch that had
fallen behind `master`. Wave 417 lands the hygiene work: close/replace stale
PRs, fix the branch target to `master` (Strategy P), repair the CI blocker
introduced by the Russian cross-walk file, and produce the W417 report plus
W418 cooperation variants.

---

## Decomposed plan

See `.claude/plans/wave-loop-416.md` and
`docs/reports/FPGA_LOOP_COOPERATION_W417_2026-07-01.md`.

| Step | File(s) | Deliverable |
|------|---------|-------------|
| 1 | `.claude/plans/wave-loop-416.md` | Decomposed plan + weak points + competitor scan |
| 2 | `fpga/HARDWARE_SSOT.md` | Updated PVT-envelope / VCD protocol |
| 3 | `cli/tri/src/fpga.rs` | `pvt-envelope` subcommand + VCD parser hardening |
| 4 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | PVT monotonicity + OSCFSEL transaction theorems |
| 5 | `docs/reports/*` | W416 report, evidence, W417 cooperation |
| 6 | `.trinity/experience.md` | W416 learnings |
| 7 | git/PR | squash-merge to `master`, close #1347, open #1348 |
| 1 | GitHub PRs/issues | Close superseded #1351; confirm stale wave-loop PRs/issues are closed |
| 2 | `docs/BRANCHING_MODEL.md` | Document Strategy P: wave-loop PR target is `master` |
| 3 | `docs/.legacy-non-english-docs` | Allowlist `conformance/vectors/CROSSWALK_sw_hw.md` until translated |
| 4 | `docs/NOW.md` | Update W417 section to in-progress / close-out state |
| 5 | `docs/reports/*` | `WAVE_LOOP_417_REPORT.md`, `FPGA_LOOP_EVIDENCE_W417_2026-07-04.md`, `FPGA_LOOP_COOPERATION_W418_2026-07-04.md` |
| 6 | `.trinity/experience.md` | Capture W417 learnings |
| 7 | git/PR | Open PR from `wave-loop-417` to `master`, close #1350, create #1353 for W418 |

---

## 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-A2: `tri fpga measured-to-lean --csv/--vcd --raw-ns --standalone` generated Lean files build with `lake build`.
- [ ] AC-A3: Measured CCLK is within the N25Q128_3V spec, or any exceedance is explicitly explained.

### 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 mapping.

### Bundle C
- [ ] AC-C1: `tri fpga pvt-envelope` works with and without `--pvt-context`.
- [ ] AC-C2: VCD parser unit tests cover escaped identifiers, scalar x/z, and hex bus literals.
- [ ] AC-C3: OSCFSEL 0..7 nominal rates are linked to `transaction_satisfies_flash_spec` proofs.
- [ ] AC-C4: PVT derating monotonicity lemmas build in Lean 4.

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

---

## Default variant

Execute **Variant A** if the analyzer is wired. Otherwise try **Variant B** if a
relay is available. Otherwise fall back to **Variant C**.
- [ ] AC-1: `docs/BRANCHING_MODEL.md` clearly states wave-loop PRs target `master`.
- [ ] AC-2: `cargo build --release` in `bootstrap/` no longer panics on the Russian cross-walk file.
- [ ] AC-3: `./scripts/tri test` parse/typecheck/gen/seal phases pass.
- [ ] AC-4: W417 report and W418 cooperation files exist and are linked from `docs/NOW.md`.
- [ ] AC-5: PR from `wave-loop-417` to `master` is opened with `Closes #1350`.

---

Expand Down
4 changes: 4 additions & 0 deletions .trinity/current_task/activity.md
Original file line number Diff line number Diff line change
Expand Up @@ -1440,3 +1440,7 @@
- **Commit:** docs(w415): correct PR/issue numbers for W415 land and W416 setup
- **Files:** docs/NOW.md

## 2026-07-04T16:37:45Z — wave-loop-417
- **Commit:** docs(NOW): W418 header, fix W417 issue reference to #1350, add Last updated line
- **Files:** .trinity/current-issue.md,.trinity/experience.md,docs/.legacy-non-english-docs,docs/BRANCHING_MODEL.md,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W418_2026-07-04.md,docs/reports/FPGA_LOOP_EVIDENCE_W417_2026-07-04.md,docs/reports/WAVE_LOOP_417_REPORT.md

45 changes: 45 additions & 0 deletions .trinity/experience.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,50 @@
# t27 / Trinity Agent Experience Log

## 2026-07-04 — Wave Loop 417 (hygiene, reland W415/W416, Strategy P)

### What worked
- Treating a "hygiene" wave as a real deliverable prevented W415/W416 from
staying stuck on a dirty PR and a stale branch. Closing superseded PR #1351 and
confirming the stale PR/issue list unblocked the next physics wave.
- Rebasing the W415 commits onto `master` and landing them through the W416 PR
(#1352) avoided a second merge conflict window; the W415 reland PR became
unnecessary once its content reached `master`.
- Switching the wave-loop PR target to `master` (Strategy P) matches the current
repo state where `specs/igla/` lives on `trinity-rust-rings`, not `master`.
Updating `docs/BRANCHING_MODEL.md` makes the policy discoverable.
- Adding the Russian cross-walk file to the non-English allowlist fixed the
`bootstrap/build.rs` language-policy panic without translating the file in the
same wave; translation was deferred as a future hygiene task.

### What changed behavior
- `docs/BRANCHING_MODEL.md`: documented Strategy P (`master` as wave-loop merge
target).
- `docs/.legacy-non-english-docs`: allowlisted `conformance/vectors/CROSSWALK_sw_hw.md`.
- `.trinity/current-issue.md`: rewritten for W417 hygiene and corrected to #1350.
- `docs/NOW.md`: W417 close-out state and W418 setup.
- Close-out artifacts: `docs/reports/WAVE_LOOP_417_REPORT.md`,
`docs/reports/FPGA_LOOP_EVIDENCE_W417_2026-07-04.md`, and
`docs/reports/FPGA_LOOP_COOPERATION_W418_2026-07-04.md`.

### Patterns to reuse
- When a PR becomes dirty because `master` moved ahead, prefer a clean rebase
onto current `master` over merging the old branch state; if the clean PR
already landed the same commits, close the old PR as superseded rather than
leaving it open.
- A wave-loop PR should target the branch named in the current branching model;
when the model changes, update `docs/BRANCHING_MODEL.md` in the same hygiene
wave so future branches do not silently target the wrong base.
- If a non-English doc breaks the language-policy build, the cheapest correct
fix is to add it to the legacy allowlist and open a translation issue,
rather than hacking the build script or rushing a partial translation.

### Anti-patterns to avoid
- Do not leave a work branch pointing at an old merge base while `master` moves
forward; the PR will accumulate conflicts and the L1 traceability / NOW.md
freshness checks will drift.
- Do not open a replacement PR without deciding what to do with the old one; an
open superseded PR creates confusion and can block status-check dashboards.

## 2026-07-01 — Wave Loop 416 (PVT-envelope CLI, VCD parser coverage, OSCFSEL transaction theorems)

### What worked
Expand Down
1 change: 1 addition & 0 deletions docs/.legacy-non-english-docs
Original file line number Diff line number Diff line change
Expand Up @@ -39,3 +39,4 @@ docs/reports/WAVE_LOOP_286_COOPERATION.md
docs/reports/WAVE_LOOP_321_COOPERATION.md
docs/reports/WAVE_LOOP_304_COOPERATION.md
docs/reports/WAVE_LOOP_305_COOPERATION.md
conformance/vectors/CROSSWALK_sw_hw.md # Russian SW/HW cross-walk, added W417 while CI blocked
16 changes: 13 additions & 3 deletions docs/BRANCHING_MODEL.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,16 @@ This document records the branch policy agreed in **Wave Loop 392**.
|---|---|---|---|
| `master` | Release / stable dependabot updates | **Never** | N/A |
| `trinity-rust-rings` | IGLA CODER+RACE integration branch | Only emergency recovery | N/A (integration sink) |
| `wave-loop-NNN` | Temporary wave-loop work branches | Allowed while open | `trinity-rust-rings` only |
| `wave-loop-NNN` | Temporary wave-loop work branches | Allowed while open | `master` (Strategy P) |

## Strategy P (Wave Loop 417+)

- Wave-loop PRs are opened against **`master`**, not `trinity-rust-rings`.
- `trinity-rust-rings` remains the IGLA CODER+RACE integration sink, but the
`specs/igla/` tree is no longer on `master`, so FPGA/tooling waves land
directly on `master`.
- Branches are deleted after merge; force-push is still allowed only while the
PR branch is open.

## `master`

Expand All @@ -28,9 +37,10 @@ This document records the branch policy agreed in **Wave Loop 392**.

## `wave-loop-NNN`

- One branch per wave-loop. Branch from the previous wave-loop branch or from `trinity-rust-rings`.
- One branch per wave-loop. Branch from `master` (or from the previous
wave-loop branch only when it has already landed on `master`).
- Force-push to the work branch is allowed while the branch is open.
- PR target is always `trinity-rust-rings`, never `master`.
- PR target is always `master` per Strategy P.
- Deleted after merge.

## Master-alignment epic
Expand Down
10 changes: 6 additions & 4 deletions docs/NOW.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,14 +13,16 @@ Last updated: 2026-07-04

### What landed
- Rebased `wave-loop-415` onto current master; opened replacement PR #1351 and closed dirty PR #1346.
- Rebased `wave-loop-416` onto current master; opened PR #1352 with corrected `Closes #1349` link.
- Rebased `wave-loop-416` onto current master; opened and merged PR #1352 with corrected `Closes #1349` link.
- Closed superseded PR #1351 after its commits reached `master` via PR #1352.
- Closed stale wave-loop PRs #1315, #1317, #1322, #1324, #1330 and issues #1313, #1316, #1318, #1323, #1325.
- Created real tracking issues #1349 (W416) and #1350 (W417).
- Updated `docs/BRANCHING_MODEL.md` to master-first Strategy P.
- Allowlisted `conformance/vectors/CROSSWALK_sw_hw.md` in `docs/.legacy-non-english-docs` to unblock the `fpga-smoke` / `t27c` language-policy check while the file awaits translation.

### Not done (blocked on hardware / CI)
- PR #1351 and #1352 are open and await required status checks (`check-now-freshness`, L1 traceability).
- PR #1348 (Cyrillic panic→warning) is orthogonal and needs separate owner decision.
### Not done (blocked on hardware)
- Real P12 CCLK capture for `OSCFSEL=6/7` — P12 unwired, DLC10 cable missing.
- Real relay cold-POR gate — no relay board / USB power switch available.

---

Expand Down
102 changes: 102 additions & 0 deletions docs/reports/FPGA_LOOP_COOPERATION_W418_2026-07-04.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,102 @@
# FPGA Loop Cooperation Variants — Wave 418 (2026-07-04)

**Next issue:** #1353
**Next branch:** `wave-loop-418`
**Anchor:** φ² + φ⁻² = 3 | TRINITY

Wave 417 closed the W415/W416 hygiene loop and fixed the CI blocker. For Wave
418 the bench status may change, so three cooperation variants are defined.

---

## Variant A — Physical CCLK capture (preferred if bench becomes available)

**Trigger:** P12 is wired to a logic-analyzer channel, the DSLogic / sigrok
setup works, and the DLC10 cable is available for programming.

**Deliverables:**

1. Generate `OSCFSEL=6` and `OSCFSEL=7` bitstream variants with
`tri fpga cclk-variants`.
2. Program each variant to SPI flash and perform a true cold-POR boot.
3. Capture the CCLK trace during configuration for each variant using
`tri fpga measure-cclk --live` or a DSView / sigrok export.
4. Import the captures with `tri fpga measured-to-lean --csv/--vcd --raw-ns
--standalone --validate --pvt-context <ctx.json>` and commit the generated
`.lean` files (or paste them into `proofs/lean4/Trinity/TernaryFPGABoot.lean`).
5. Document the measured frequencies, duty cycles, and PVT context in
`fpga/HARDWARE_SSOT.md`.

**Acceptance criteria:**
- Real CCLK CSV/VCD files exist for both oscillator settings.
- Generated Lean theorems build with `lake build`.
- Measured CCLK satisfies the PVT-aware flash spec or is explicitly explained.

---

## Variant B — Real relay-controlled cold-POR CI gate

**Trigger:** The bench has a relay board (or a USB-controllable power switch)
and the Digilent DLC10 cable is detected, but P12 is not wired for CCLK
capture.

**Deliverables:**

1. Select a relay interface (USB-serial relay module, smart power strip with a
local API, or a microcontroller GPIO bridge).
2. Implement a small `RelayControl` trait with `power_cycle(delay_ms: u64)`.
3. Extend `FpgaCmd::ColdPor` so `--relay-port` accepts real port strings
(`/dev/cu.usbserial-*`, `tcp://...`) in addition to `MOCK`.
4. After relay power-cycle, run `capture_stat` and write a real boot log with
`relay_mock: false`.
5. Add Rust tests for the relay protocol framing (without touching hardware).
6. Document relay wiring, port syntax, and safety rules in
`fpga/HARDWARE_SSOT.md`.

**Acceptance criteria:**
- `tri fpga cold-por <bit> --relay-port <real>` performs an automated
power-cycle and captures STAT.
- The resulting log has `relay_mock: false` and a real STAT raw value.
- `fpga/HARDWARE_SSOT.md` documents relay wiring and port mapping.

---

## Variant C — Further formal tooling (fallback if bench still blocked)

**Trigger:** P12 and the relay hardware are still unavailable.

**Deliverables:**

1. Harden the PVT envelope against real characterization data:
- Add a regression test that checks every envelope context inside the
operating rectangle satisfies `n25q128_min_sck_*_ns_pvt ≥ N25Q128_MIN_SCK_*_NS`.
- Document how to replace the linear coefficients once N25Q128_3V PVT curves
are available.
2. Extend instrument import coverage:
- Parse `$date` / `$version` / `$comment` multi-line VCD headers without
confusing them with `$var` declarations.
- Support Saleae/DSView analog CSV exports that report a voltage column
directly, so `--vcd-threshold-v` is not the only analog path.
3. Build a standalone Lean proof integration test:
- Run `tri fpga measured-to-lean --pvt-context` on a synthetic CSV and
type-check the generated file in a temporary `lake` package.
4. Continue closing the physical-evidence gap in documentation:
- Update `fpga/HARDWARE_SSOT.md` with a checklist for the first real capture.

**Acceptance criteria:**
- At least one new instrument-import unit test lands.
- The PVT envelope has a regression test for the lower-bound invariant.
- A standalone Lean file generated from the CLI type-checks outside the main
`Trinity` tree.

---

## Default selection

1. Try **Variant A** if the analyzer and DLC10 cable are available.
2. Else try **Variant B** if a relay and DLC10 cable are available.
3. Else fall back to **Variant C**.

---

*φ² + φ⁻² = 3 | TRINITY*
68 changes: 68 additions & 0 deletions docs/reports/FPGA_LOOP_EVIDENCE_W417_2026-07-04.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,68 @@
# FPGA Loop Evidence — Wave Loop 417 (2026-07-04)

**Issue:** #1350
**Branch:** `wave-loop-417`
**Scope:** hygiene and reland of W415/W416; no new physical evidence.

---

## 1. PR/issue hygiene

### Closed as superseded
- PR #1351 (`wave-loop-415-reland`) — closed because PR #1352 already carried the
rebased W415 commits to `master`.

### Confirmed already closed
- PRs #1315, #1317, #1322, #1324, #1330 — all `CLOSED`.
- Issues #1313, #1316, #1318, #1323, #1325 — all `CLOSED`.

### Active tracking
- Issue #1349 (W416) — closed by PR #1352.
- Issue #1350 (W417) — open, targeted by this branch.

---

## 2. Branching model change

Evidence: `docs/BRANCHING_MODEL.md`

- `wave-loop-NNN` merge target changed from `trinity-rust-rings` to `master`.
- New "Strategy P (Wave Loop 417+)" section documents the policy.

---

## 3. CI blocker resolution

Evidence: `docs/.legacy-non-english-docs`

- Added `conformance/vectors/CROSSWALK_sw_hw.md` to the allowlist.
- This stops the `bootstrap/build.rs` panic at language-policy check for
Cyrillic characters.

---

## 4. Local verification commands

```bash
# W417 hygiene verification
cd bootstrap && cargo build --release
# Expected: PASS (language-policy check no longer panics on CROSSWALK_sw_hw.md)

./scripts/tri test
# Expected: parse/typecheck/gen/seal phases PASS
```

---

## 5. Hardware status

- P12 CCLK capture: **not wired**.
- DLC10 cable: **missing** (VID 0x03FD not detected).
- Relay board / USB power switch: **not available**.

Therefore W418 will again evaluate A/B/C variants, with Variant C fallback
(formal tooling / regression tests) likely if hardware remains unavailable.

---

*φ² + φ⁻² = 3 | TRINITY*
Loading
Loading