|
1 | | -# Wave Loop 416 — PVT-envelope CLI, VCD parser coverage, OSCFSEL transaction theorems |
| 1 | +# Wave Loop 417 — hygiene, reland W415/W416, and next-variant gate |
2 | 2 |
|
3 | | -**Issue:** #1347 |
4 | | -**Branch:** `wave-loop-416` |
5 | | -**Milestone:** Continue the FPGA boot-evidence line from W415. |
| 3 | +**Issue:** #1350 |
| 4 | +**Branch:** `wave-loop-417` |
| 5 | +**Milestone:** Close out the W415/W416 reland mess and set up the next FPGA boot-evidence wave. |
6 | 6 |
|
7 | 7 | --- |
8 | 8 |
|
9 | 9 | ## Goal |
10 | 10 |
|
11 | | -Wave 415 delivered the **Variant C** formal-tooling fallback because the bench |
12 | | -was still blocked. Wave 416 re-evaluates the bench state and executes the first |
13 | | -available variant. |
14 | | - |
15 | | -1. **Variant A (preferred when bench becomes available):** |
16 | | - - Wire P12 to a logic-analyzer channel and capture real CCLK for |
17 | | - `OSCFSEL=6` and `OSCFSEL=7`. |
18 | | - - Import the captures with `tri fpga measured-to-lean --csv/--vcd --raw-ns |
19 | | - --standalone --validate --pvt-context <ctx.json>` and commit the generated |
20 | | - Lean theorems. |
21 | | - - Document the measured frequencies/duty cycles and PVT context in |
22 | | - `fpga/HARDWARE_SSOT.md`. |
23 | | - |
24 | | -2. **Variant B (if relay hardware is available):** |
25 | | - - Implement a real `--relay-port` backend for `tri fpga cold-por` |
26 | | - (e.g. serial or TCP relay controlling board power). |
27 | | - - Perform an automated cold-POR power-cycle and capture STAT without |
28 | | - operator intervention. |
29 | | - - Document relay wiring in `fpga/HARDWARE_SSOT.md`. |
30 | | - |
31 | | -3. **Variant C (fallback if bench still blocked):** |
32 | | - - Add a PVT-envelope CLI helper (`tri fpga pvt-envelope`). |
33 | | - - Prove monotonicity of the PVT derating functions in Lean 4. |
34 | | - - Extend VCD parser coverage for escaped identifiers, scalar x/z transitions, |
35 | | - and hex bus literals. |
36 | | - - Link the OSCFSEL 0..7 nominal theorems to |
37 | | - `transaction_satisfies_flash_spec` proofs. |
| 11 | +Wave 415 and Wave 416 were stuck on a dirty PR (#1346) and a branch that had |
| 12 | +fallen behind `master`. Wave 417 lands the hygiene work: close/replace stale |
| 13 | +PRs, fix the branch target to `master` (Strategy P), repair the CI blocker |
| 14 | +introduced by the Russian cross-walk file, and produce the W417 report plus |
| 15 | +W418 cooperation variants. |
38 | 16 |
|
39 | 17 | --- |
40 | 18 |
|
41 | 19 | ## Decomposed plan |
42 | 20 |
|
43 | | -See `.claude/plans/wave-loop-416.md` and |
44 | | -`docs/reports/FPGA_LOOP_COOPERATION_W417_2026-07-01.md`. |
45 | | - |
46 | 21 | | Step | File(s) | Deliverable | |
47 | 22 | |------|---------|-------------| |
48 | | -| 1 | `.claude/plans/wave-loop-416.md` | Decomposed plan + weak points + competitor scan | |
49 | | -| 2 | `fpga/HARDWARE_SSOT.md` | Updated PVT-envelope / VCD protocol | |
50 | | -| 3 | `cli/tri/src/fpga.rs` | `pvt-envelope` subcommand + VCD parser hardening | |
51 | | -| 4 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | PVT monotonicity + OSCFSEL transaction theorems | |
52 | | -| 5 | `docs/reports/*` | W416 report, evidence, W417 cooperation | |
53 | | -| 6 | `.trinity/experience.md` | W416 learnings | |
54 | | -| 7 | git/PR | squash-merge to `master`, close #1347, open #1348 | |
| 23 | +| 1 | GitHub PRs/issues | Close superseded #1351; confirm stale wave-loop PRs/issues are closed | |
| 24 | +| 2 | `docs/BRANCHING_MODEL.md` | Document Strategy P: wave-loop PR target is `master` | |
| 25 | +| 3 | `docs/.legacy-non-english-docs` | Allowlist `conformance/vectors/CROSSWALK_sw_hw.md` until translated | |
| 26 | +| 4 | `docs/NOW.md` | Update W417 section to in-progress / close-out state | |
| 27 | +| 5 | `docs/reports/*` | `WAVE_LOOP_417_REPORT.md`, `FPGA_LOOP_EVIDENCE_W417_2026-07-04.md`, `FPGA_LOOP_COOPERATION_W418_2026-07-04.md` | |
| 28 | +| 6 | `.trinity/experience.md` | Capture W417 learnings | |
| 29 | +| 7 | git/PR | Open PR from `wave-loop-417` to `master`, close #1350, create #1353 for W418 | |
55 | 30 |
|
56 | 31 | --- |
57 | 32 |
|
58 | 33 | ## Acceptance criteria |
59 | 34 |
|
60 | | -### Bundle A |
61 | | -- [ ] AC-A1: P12 is wired to a logic-analyzer channel and real CCLK capture files exist for `OSCFSEL=6` and `OSCFSEL=7`. |
62 | | -- [ ] AC-A2: `tri fpga measured-to-lean --csv/--vcd --raw-ns --standalone` generated Lean files build with `lake build`. |
63 | | -- [ ] AC-A3: Measured CCLK is within the N25Q128_3V spec, or any exceedance is explicitly explained. |
64 | | - |
65 | | -### Bundle B |
66 | | -- [ ] AC-B1: `tri fpga cold-por <bit> --relay-port <real>` performs an automated power-cycle and captures STAT. |
67 | | -- [ ] AC-B2: The resulting log has `relay_mock: false` and a real STAT raw value. |
68 | | -- [ ] AC-B3: `fpga/HARDWARE_SSOT.md` documents relay wiring and port mapping. |
69 | | - |
70 | | -### Bundle C |
71 | | -- [ ] AC-C1: `tri fpga pvt-envelope` works with and without `--pvt-context`. |
72 | | -- [ ] AC-C2: VCD parser unit tests cover escaped identifiers, scalar x/z, and hex bus literals. |
73 | | -- [ ] AC-C3: OSCFSEL 0..7 nominal rates are linked to `transaction_satisfies_flash_spec` proofs. |
74 | | -- [ ] AC-C4: PVT derating monotonicity lemmas build in Lean 4. |
75 | | - |
76 | | -### Invariant checks |
77 | | -- [ ] `./scripts/tri test` parse/typecheck/gen/seal-verify phases pass. |
78 | | -- [ ] `lake build Trinity.TernaryFPGABoot` passes. |
79 | | -- [ ] `cargo test -p tri fpga::tests` passes. |
80 | | - |
81 | | ---- |
82 | | - |
83 | | -## Default variant |
84 | | - |
85 | | -Execute **Variant A** if the analyzer is wired. Otherwise try **Variant B** if a |
86 | | -relay is available. Otherwise fall back to **Variant C**. |
| 35 | +- [ ] AC-1: `docs/BRANCHING_MODEL.md` clearly states wave-loop PRs target `master`. |
| 36 | +- [ ] AC-2: `cargo build --release` in `bootstrap/` no longer panics on the Russian cross-walk file. |
| 37 | +- [ ] AC-3: `./scripts/tri test` parse/typecheck/gen/seal phases pass. |
| 38 | +- [ ] AC-4: W417 report and W418 cooperation files exist and are linked from `docs/NOW.md`. |
| 39 | +- [ ] AC-5: PR from `wave-loop-417` to `master` is opened with `Closes #1350`. |
87 | 40 |
|
88 | 41 | --- |
89 | 42 |
|
|
0 commit comments