|
1553 | 1553 | - Do not rely on `simp [h_low, h_high]` to close goals involving concrete Nat constants; follow with `constructor`/`omega` where needed. |
1554 | 1554 | - Do not use `std::io::Stdin::read_to_string` directly; import `std::io::Read` first. |
1555 | 1555 | - Do not try to typecheck a generated snippet via a shell heredoc named `import`; write it to a real `.lean` file and run `lake build` instead. |
| 1556 | + |
| 1557 | +## 2026-07-04 — Wave Loop 412 (measured-to-lean standalone + raw-ns + PVT context) |
| 1558 | + |
| 1559 | +### What worked |
| 1560 | +- Delivered Variant C fallback because P12 and DLC10 remained unavailable. |
| 1561 | +- Added `--standalone` mode that emits a self-contained `.lean` file with the |
| 1562 | + correct `Trinity.BitstreamConfig` namespace wrapper. |
| 1563 | +- Added `--raw-ns` mode and a `MeasuredCclkRawNs` record so instrument exports |
| 1564 | + can supply period/low/high directly without duty-cycle quantization. |
| 1565 | +- Added `PvtContext { temp_c, vccint_mv, vccaux_mv, process_corner }` and a |
| 1566 | + placeholder derating model in Lean 4. The implication theorems only require the |
| 1567 | + derated limits to be ≥ the nominal 6 ns bounds, so real PVT data can be |
| 1568 | + swapped in later without touching theorem statements. |
| 1569 | +- Reorganized the W411 branch into a single clean commit on top of `master` |
| 1570 | + (discarding autogenerated seal churn) and squash-merged PR #1331 with `--admin`. |
| 1571 | +- Updated `docs/BRANCHING_MODEL.md` to reflect Strategy P: `master` is now the |
| 1572 | + integration+release branch; `trinity-rust-rings` is archived/deprecated. |
| 1573 | +- `lake build Trinity.TernaryFPGABoot` passed; `cargo test -p tri fpga::tests` |
| 1574 | + passed 16/16. |
| 1575 | + |
| 1576 | +### What changed behavior |
| 1577 | +- `tri fpga measured-to-lean` now accepts `--standalone` and `--raw-ns`. |
| 1578 | +- `proofs/lean4/Trinity/TernaryFPGABoot.lean` has raw-ns and PVT-aware predicates. |
| 1579 | +- `fpga/HARDWARE_SSOT.md` §3.6.12 documents the new modes and PVT placeholder. |
| 1580 | +- `docs/BRANCHING_MODEL.md` records the new branch policy. |
| 1581 | +- Close-out docs: `docs/reports/WAVE_LOOP_412_REPORT.md`, |
| 1582 | + `docs/reports/FPGA_LOOP_EVIDENCE_W412_2026-07-04.md`, |
| 1583 | + `docs/reports/FPGA_LOOP_COOPERATION_W413_2026-07-04.md`. |
| 1584 | + |
| 1585 | +### Patterns to reuse |
| 1586 | +- When a generated Lean file must be type-correct standalone, emit the same |
| 1587 | + imports and namespace wrapper already used by the target module. |
| 1588 | +- Keep placeholder PVT functions returning constants that are provably ≥ the |
| 1589 | + nominal bounds; the proof machinery stays valid when the placeholder is |
| 1590 | + replaced with real curves. |
| 1591 | +- Use `git reset --soft origin/master` + selective restaging to clean up a |
| 1592 | + long-running wave-loop branch that accumulated autogenerated seal noise before |
| 1593 | + squash-merging. |
| 1594 | + |
| 1595 | +### Anti-patterns to avoid |
| 1596 | +- Do not define theorems that reference later definitions in the same file |
| 1597 | + unless they are inside a `mutual` block; reorder so dependencies come first. |
| 1598 | +- Do not include unused parameters in Lean definitions; rename them to `_` or |
| 1599 | + `_name` to avoid linter warnings. |
| 1600 | +- Do not let autogenerated `.trinity/seals/*.json` and session logs leak into a |
| 1601 | + squash-merge commit; stage only human-authored source + generated reports. |
0 commit comments