gHashTag · gHashTag · Jul 4, 2026 · Jul 4, 2026
@@ -1,54 +1,55 @@
-# Wave Loop 418 — FPGA physical capture, real relay gate, or further formal tooling
+# Wave Loop 419 — physical CCLK capture, real relay gate, or instrument-import parity
 
-**Issue:** #1353  
-**Branch:** `wave-loop-418`  
-**Milestone:** Continue the FPGA boot-evidence line from W417.
+**Issue:** #1357  
+**Branch:** `wave-loop-419`  
+**Milestone:** Continue the FPGA boot-evidence line from W418.
 
 ---
 
 ## Goal
 
-Wave 417 closed the W415/W416 hygiene loop. Wave 418 re-evaluates the bench
-state and executes the first available variant.
+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.
 
 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.
    - 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):**
+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 in `fpga/HARDWARE_SSOT.md`.
+   - Document relay wiring and port syntax in `fpga/HARDWARE_SSOT.md`.
 
 3. **Variant C (fallback if bench still blocked):**
-   - Add a regression test that the PVT envelope stays ≥ the nominal bound
-     across the full operating rectangle.
-   - Extend instrument import for VCD `$date`/`$version`/`$comment` headers and
-     analog CSV voltage columns.
-   - Build a standalone Lean proof integration test from a synthetic CSV.
-   - Document the first-real-capture checklist in `fpga/HARDWARE_SSOT.md`.
+   - 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`.
 
 ---
 
 ## Decomposed plan
 
-See `docs/reports/FPGA_LOOP_COOPERATION_W418_2026-07-04.md`.
+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 regression/integration tests |
-| 2 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | PVT envelope regression lemma or new measured theorems |
+| 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/*` | W418 report, evidence, W419 cooperation |
-| 5 | `.trinity/experience.md` | W418 learnings |
-| 6 | git/PR | squash-merge to `master`, close #1353, open #? for W419 |
+| 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 |
 
 ---
 
@@ -57,29 +58,40 @@ See `docs/reports/FPGA_LOOP_COOPERATION_W418_2026-07-04.md`.
 ### 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.
+- [ ] AC-A3: Measured CCLK satisfies the PVT-aware flash 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.
+- [ ] AC-B3: `fpga/HARDWARE_SSOT.md` documents relay wiring and port syntax.
 
 ### Bundle C
-- [ ] AC-C1: A regression test verifies the PVT envelope lower bound across the operating rectangle.
-- [ ] AC-C2: Instrument import handles VCD `$date`/`$version`/`$comment` headers or analog CSV voltage columns.
-- [ ] AC-C3: A standalone `.lean` file generated from the CLI type-checks in a temporary `lake` package.
+- [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.
 
 ### Invariant checks
-- [ ] `./scripts/tri test` parse/typecheck/gen/seal-verify phases pass.
-- [ ] `lake build Trinity.TernaryFPGABoot` passes.
-- [ ] `cargo test -p tri fpga::tests` passes.
+- [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.
+
+---
+
+## 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`
 
 ---
 
 ## 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**.
+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**.
 
 ---
 

@@ -1460,3 +1460,7 @@
 - **Commit:** docs(NOW): W418 setup, mark W417 PR #1354 merged
 - **Files:** .claude/plans/wave-loop-418.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W419_2026-07-04.md,docs/reports/FPGA_LOOP_EVIDENCE_W418_2026-07-04.md,docs/reports/WAVE_LOOP_418_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
 
+## 2026-07-04T18:22:51Z — wave-loop-419-clean
+- **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
+
@@ -1,5 +1,67 @@
 # t27 / Trinity Agent Experience Log
 
+## 2026-07-05 — Wave Loop 419 (Variant C fallback: VCD/CSV hardening, PVT monotonicity, standalone lake workflow)
+
+### What worked
+- Hardening the VCD `$comment` parser with an **exact-token terminator** closed a
+  real regression vector: vendor comments that contain the substring `$end` no
+  longer confuse the signal dictionary. A single regression test with an embedded
+  `$end`-like token prevents future heuristic drift.
+- Adding `--csv-channel <name>` and extending header-name auto-detection to
+  `cclk`, `vccint`, `vccaux`, `ain`, `a0`, `channel0` makes multi-channel
+  instrument exports first-class. The explicit selector is simpler than trying to
+  guess every vendor dialect.
+- Proving PVT envelope **monotonicity in temperature** and **antitonicity in
+  VCCINT** in both Lean 4 and Rust guards the shape of the placeholder envelope
+  independently of the exact coefficients. The symbolic Lean proofs and the
+  numeric Rust tests reinforce each other.
+- Documenting the full `measured-to-lean --standalone` lake-package workflow in
+  `fpga/HARDWARE_SSOT.md` turned a "works in tests" feature into a reproducible
+  user protocol.
+- Catching the invalid `import Trinity.BitstreamConfig` in the `--standalone`
+  output showed that **string assertions are not enough** for generated-code
+  tests: the integration test that runs `lake build` on the generated file is
+  what found the bug.
+
+### What changed behavior
+- `cli/tri/src/fpga.rs`: VCD `$comment` exact-terminator parsing;
+  `--csv-channel` option and multi-channel header detection;
+  `test_pvt_half_ns_monotone_in_temp` / `test_pvt_half_ns_antitone_in_vccint`;
+  `test_parse_cclk_csv_explicit_channel_select`;
+  `--standalone` template now imports only `Trinity.TernaryFPGABoot`.
+- `proofs/lean4/Trinity/TernaryFPGABoot.lean`: added
+  `pvt_half_ns_monotone_in_temp` and `pvt_half_ns_antitone_in_vccint`.
+- `fpga/HARDWARE_SSOT.md`: added §3.6.16 standalone lake-package workflow.
+- `docs/NOW.md`: W419 close-out and W420 setup.
+- Close-out artifacts: `docs/reports/WAVE_LOOP_419_REPORT.md`,
+  `docs/reports/FPGA_LOOP_EVIDENCE_W419_2026-07-05.md`, and
+  `docs/reports/FPGA_LOOP_COOPERATION_W420_2026-07-05.md`.
+
+### Patterns to reuse
+- For section-skipping parsers, match the **exact delimiter token** and clear
+  state immediately when the delimiter appears on the same line; do not use
+  substring heuristics.
+- When adding user-facing selectors to instrument parsers, also add a
+  regression test that would fail if the selector is ignored or the fallback
+  overrides it.
+- For placeholder model coefficients, prove the **shape** (monotonicity,
+  bounds) symbolically and add a numeric operating-rectangle regression. This
+  combination survives coefficient updates as long as the shape constraints
+  remain.
+- For generated-code deliverables, the canonical integration test is to
+  **type-check the generated artifact in a fresh package** that depends on the
+  real library via a local path. String snapshots catch regressions; package
+  builds catch invalid imports and namespaces.
+
+### Anti-patterns to avoid
+- Do not assert only string contents for generated source files; always exercise
+  the downstream compiler/package build.
+- Do not import a Lean 4 **namespace** as if it were a module. Names inside a
+  file are reached through the file's module name, then opened with `open` if
+  needed.
+- Do not let a parser heuristic silently override an explicit user option;
+  resolve precedence clearly (explicit option > named header > numeric fallback).
+
 ## 2026-07-04 — Wave Loop 418 (Variant C fallback: PVT regression, instrument import, standalone Lean integration)
 
 ### What worked