Skip to content

Commit 5d51a6a

Browse files
gHashTagDmitrii Vasilevclaude
authored
feat(fpga): Wave Loop 416 — PVT-envelope CLI, VCD parser coverage, OSCFSEL transaction theorems (#1352)
* feat(fpga): Wave Loop 15 — PVT-aware CCLK validation, VCD robustness, OSCFSEL theorem library Closes #1343 - Add --pvt-context to tri fpga measure-cclk --validate and measured-to-lean. - Harden VCD parser: multi-line $var, scalar/bus mixed dumps, duplicate transitions, $dumpoff/$dumpon regions. - Add OSCFSEL 0..7 nominal and worst-case PVT measured-CCLK theorems. - Update fpga/HARDWARE_SSOT.md and docs/NOW.md. - Reseal generated-code hashes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * docs(w415): correct PR/issue numbers for W415 land and W416 setup Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * feat(fpga): Wave Loop 416 — PVT-envelope CLI, VCD parser coverage, OSCFSEL transaction theorems (Closes #1347) - Add tri fpga pvt-envelope --pvt-context helper with envelope summary and margin output. - Harden VCD parser for escaped identifiers, scalar x/z transitions, and hex bus literals. - Prove PVT derating monotonicity (temp monotone, voltage antitone, ff<=tt<=ss corner ordering). - Link OSCFSEL 0..7 nominal measured-CCLK theorems to transaction_satisfies_flash_spec. - Update HARDWARE_SSOT.md, NOW.md, current-issue.md, experience.md. - Add W416 report, evidence, and W417 cooperation variants. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * docs(NOW): W418 header, fix W417 issue reference to #1350, add Last updated line --------- Co-authored-by: Dmitrii Vasilev <admin@t27.ai> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
1 parent 78e9a04 commit 5d51a6a

591 files changed

Lines changed: 3009 additions & 2802 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.claude/plans/wave-loop-415.md‎

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,9 @@
1111
| Relay / power switch + cable | Variant B |
1212
| Nothing | Variant C |
1313

14-
Current state (2026-07-01): **nothing** — P12 unwired, DLC10 cable missing. Default to **Variant C** unless the bench state changes at the start of the wave.
14+
Current state (2026-07-01): **nothing** — P12 unwired, DLC10 cable missing, no USB relay detected. Confirmed by `dlc10 idcode` (`VID=0x03FD` not found) and `system_profiler SPUSBDataType` (no FTDI/relay/serial signatures). Default to **Variant C** for W415.
15+
16+
Execution status: **Variant C completed**.
1517

1618
## Goals
1719

@@ -72,19 +74,19 @@ Files: `proofs/lean4/Trinity/TernaryFPGABoot.lean`, `cli/tri/src/fpga.rs`
7274

7375
## Verification checklist
7476

75-
- [ ] `cargo test -p tri fpga::tests` passes (new + existing tests).
76-
- [ ] `lake build Trinity.TernaryFPGABoot` passes from `proofs/lean4/`.
77-
- [ ] `./scripts/tri test` passes (parse/typecheck/gen/seal-verify).
78-
- [ ] For Variant A: at least one generated `.lean` file builds standalone.
79-
- [ ] For Variant B: `tri fpga cold-por ... --relay-port <real>` produces a real log when hardware is connected.
80-
- [ ] For Variant C: `--validate` can check against PVT-margin bounds and the VCD parser tests cover bus/real/dumpoff edge cases.
77+
- [x] `cargo test -p tri fpga::tests` passes (32/32).
78+
- [x] `lake build Trinity.TernaryFPGABoot` passes from `proofs/lean4/`.
79+
- [x] `./scripts/tri test` passes seal-verify and all code-generation phases.
80+
- [ ] For Variant A: deferred until P12 / analyzer available.
81+
- [ ] For Variant B: deferred until relay hardware available.
82+
- [x] For Variant C: PVT-aware validation, VCD parser tests (multi-line var, mixed scalar/bus, dumpoff), and OSCFSEL 0..7 nominal/worst-case theorem library landed.
8183

8284
## Acceptance criteria
8385

8486
- The chosen variant is fully implemented and verified.
8587
- All invariant checks pass.
8688
- Report + evidence + W416 cooperation variants are produced.
87-
- PR closes #1343.
89+
- PR #1346 closes #1343.
8890

8991
---
9092

‎.claude/plans/wave-loop-416.md‎

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
# Wave Loop 416 Plan
2+
3+
**Issue:** #1347 (to be created after W415 land)
4+
**Branch:** `wave-loop-416`
5+
6+
---
7+
8+
## Decision gate
9+
10+
| Bench available? | Pick |
11+
|--------------------|------|
12+
| P12 + analyzer + DLC10 cable | Variant A |
13+
| Relay / power switch + DLC10 cable | Variant B |
14+
| Nothing | Variant C |
15+
16+
Current state (2026-07-01): **nothing** — P12 unwired, DLC10 cable missing, no USB relay detected. Confirmed by `dlc10 idcode` (`VID=0x03FD` not found). Default to **Variant C** for W416.
17+
18+
---
19+
20+
## Goals
21+
22+
1. If the bench becomes available, capture real CCLK for OSCFSEL=6/7 and commit instrument-to-Lean theorems (Variant A).
23+
2. If relay hardware becomes available, automate cold-POR power-cycling and capture real STAT (Variant B).
24+
3. Otherwise, continue hardening the formal model: add a PVT-envelope CLI helper, prove monotonicity of the derating functions, extend VCD parser coverage for escaped identifiers / x/z / hex bus literals, and link the OSCFSEL nominal theorems to `transaction_satisfies_flash_spec` proofs (Variant C).
25+
26+
---
27+
28+
## Work breakdown
29+
30+
### Variant A — Physical CCLK capture
31+
32+
Files: `fpga/HARDWARE_SSOT.md`, `proofs/lean4/Trinity/TernaryFPGABoot.lean`, `docs/reports/*`
33+
34+
- Wire P12 to the logic analyzer.
35+
- Generate `OSCFSEL=6` and `OSCFSEL=7` variants with `tri fpga cclk-variants`.
36+
- Program each variant to flash, cold-POR boot, and capture CCLK.
37+
- Import captures with `tri fpga measured-to-lean --csv/--vcd --raw-ns --standalone --validate --pvt-context`.
38+
- Commit generated theorems and update `fpga/HARDWARE_SSOT.md`.
39+
40+
### Variant B — Real relay-controlled cold-POR
41+
42+
Files: `cli/tri/src/fpga.rs`, `fpga/HARDWARE_SSOT.md`
43+
44+
- Select a relay interface (USB-serial relay module, smart power strip, or MCU GPIO bridge).
45+
- Implement a `RelayControl` trait with `power_cycle(delay_ms: u64)`.
46+
- Extend `FpgaCmd::ColdPor` to accept real `--relay-port` values.
47+
- Capture STAT after relay power-cycle and write a non-mock log.
48+
- Document wiring and safety rules.
49+
50+
### Variant C — Further formal tooling (default fallback)
51+
52+
Files: `cli/tri/src/fpga.rs`, `proofs/lean4/Trinity/TernaryFPGABoot.lean`, `fpga/HARDWARE_SSOT.md`, `docs/reports/*`
53+
54+
1. **PVT-envelope CLI helper**: add `tri fpga pvt-envelope --pvt-context <ctx.json>` that prints the derated `t_CL`/`t_CH` bounds, the margin over the nominal 6 ns bound, and the operating-envelope validity status.
55+
2. **PVT monotonicity lemmas** in Lean 4: prove the temperature and voltage derating functions are monotone inside the operating envelope, and that the process-corner derating increases from `ff` to `tt` to `ss`.
56+
3. **VCD parser coverage**: handle escaped identifiers with embedded spaces (e.g. `\my sig `), scalar `x`/`z` transitions (skip them), and hex bus value changes (`hFF !`) with `x`/`z` bit skipping.
57+
4. **OSCFSEL transaction theorems**: for each OSCFSEL 0..7, prove `transaction_satisfies_flash_spec (measured_boot_transaction (cclk_nominal_hz n) 50 bits) = true` using the existing implication theorems.
58+
5. **Docs**: update `fpga/HARDWARE_SSOT.md` with the new `pvt-envelope` command and VCD parser capabilities.
59+
60+
---
61+
62+
## Weak points
63+
64+
1. **Physical evidence gap remains** under Variant C.
65+
2. **PVT envelope coefficients are still informed estimates**, not Micron datasheet curves.
66+
3. **Escaped VCD identifiers** are non-trivial to parse correctly with line-oriented tokenization; our handling will be best-effort for common cases.
67+
4. **Hex bus literals** are not part of the IEEE VCD standard but are emitted by some tools; supporting them is pragmatic, not canonical.
68+
5. **Relay automation** remains unimplemented until hardware is selected.
69+
70+
---
71+
72+
## Competitor scan
73+
74+
- **Sparkle HDL / Verilean:** formal Verilog-to-Lean/Coq verification; no public instrument-to-Lean bridge or PVT-aware timing envelope for flash boot.
75+
- **SymbiYosys / Yosys formal:** bounded property checking on RTL; no link to logic-analyzer measurements.
76+
- **Koika / Kami:** processor-model verification in Coq; unrelated to 7-series boot timing.
77+
- **OpenFPGALoader / prjxray:** bitstream/JTAG tooling; no formal proof pipeline.
78+
- **TinyTapeout / Efaless:** silicon-shuttle flow; relies on PDK characterization, not user-captured proofs.
79+
- **t27 differentiation:** still the only open pipeline converting instrument exports (CSV/VCD) into Lean 4 proofs of flash timing compliance, now with a falsifiable PVT envelope, envelope monotonicity proofs, and per-OSCFSEL transaction theorems.
80+
81+
---
82+
83+
## Verification checklist
84+
85+
- [x] `cargo test -p tri fpga::tests` passes (new + existing tests).
86+
- [x] `lake build Trinity.TernaryFPGABoot` passes from `proofs/lean4/`.
87+
- [x] `./scripts/tri test` passes parse/typecheck/gen/seal-verify.
88+
- [ ] For Variant A: at least one generated `.lean` file builds standalone.
89+
- [ ] For Variant B: real relay port produces a non-mock boot log.
90+
- [x] For Variant C: `tri fpga pvt-envelope` works, VCD tests cover escaped identifiers / x/z / hex, OSCFSEL transaction theorems build.
91+
92+
---
93+
94+
## Acceptance criteria
95+
96+
- The chosen variant is fully implemented and verified.
97+
- All invariant checks pass.
98+
- Report + evidence + W417 cooperation variants are produced.
99+
- PR closes #1347.
100+
101+
---
102+
103+
*φ² + φ⁻² = 3 | TRINITY*

‎.trinity/current-issue.md‎

Lines changed: 29 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,25 @@
1-
# Wave Loop 415 — FPGA physical capture, real relay gate, or further formal tooling
1+
# Wave Loop 416 — PVT-envelope CLI, VCD parser coverage, OSCFSEL transaction theorems
22

3-
**Issue:** #1343
4-
**Branch:** `wave-loop-415`
5-
**Milestone:** Continue the FPGA boot-evidence line from W414.
3+
**Issue:** #1347
4+
**Branch:** `wave-loop-416`
5+
**Milestone:** Continue the FPGA boot-evidence line from W415.
66

77
---
88

99
## Goal
1010

11-
Wave 414 delivered the **Variant C** formal-tooling fallback because the bench
12-
was still blocked. Wave 415 re-evaluates the bench state and executes the first
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
1313
available variant.
1414

1515
1. **Variant A (preferred when bench becomes available):**
1616
- Wire P12 to a logic-analyzer channel and capture real CCLK for
1717
`OSCFSEL=6` and `OSCFSEL=7`.
1818
- Import the captures with `tri fpga measured-to-lean --csv/--vcd --raw-ns
19-
--standalone --validate` and commit the generated Lean theorems.
20-
- Document the measured frequencies/duty cycles in `fpga/HARDWARE_SSOT.md`.
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`.
2123

2224
2. **Variant B (if relay hardware is available):**
2325
- Implement a real `--relay-port` backend for `tri fpga cold-por`
@@ -27,27 +29,29 @@ available variant.
2729
- Document relay wiring in `fpga/HARDWARE_SSOT.md`.
2830

2931
3. **Variant C (fallback if bench still blocked):**
30-
- Integrate the PVT envelope into `tri fpga measure-cclk --validate`.
31-
- Extend VCD parser unit tests for real-world quirks.
32-
- Build a library of measured-CCLK theorems for every documented Artix-7
33-
OSCFSEL value (0..7) under nominal and worst-case PVT contexts.
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.
3438

3539
---
3640

3741
## Decomposed plan
3842

39-
See `.claude/plans/wave-loop-415.md` and
40-
`docs/reports/FPGA_LOOP_COOPERATION_W415_2026-07-01.md`.
43+
See `.claude/plans/wave-loop-416.md` and
44+
`docs/reports/FPGA_LOOP_COOPERATION_W417_2026-07-01.md`.
4145

4246
| Step | File(s) | Deliverable |
4347
|------|---------|-------------|
44-
| 1 | `.claude/plans/wave-loop-415.md` | Decomposed plan + weak points + competitor scan |
45-
| 2 | `fpga/HARDWARE_SSOT.md` | Updated capture / relay protocol |
46-
| 3 | `cli/tri/src/fpga.rs` | Variant A import, B relay backend, or C parser/validate extensions |
47-
| 4 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | PVT-aware theorems or OSCFSEL library |
48-
| 5 | `docs/reports/*` | W415 report, evidence, W416 cooperation |
49-
| 6 | `.trinity/experience.md` | W415 learnings |
50-
| 7 | git/PR | squash-merge to `master`, close #1343, open #1344 |
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 |
5155

5256
---
5357

@@ -64,9 +68,10 @@ See `.claude/plans/wave-loop-415.md` and
6468
- [ ] AC-B3: `fpga/HARDWARE_SSOT.md` documents relay wiring and port mapping.
6569

6670
### Bundle C
67-
- [ ] AC-C1: PVT-aware validation is available in `tri fpga measure-cclk --validate`.
68-
- [ ] AC-C2: VCD parser unit tests cover multi-line declarations, bus values, real thresholds, and `$dumpoff`/`$dumpon`.
69-
- [ ] AC-C3: Measured-CCLK theorem library covers OSCFSEL 0..7 under nominal and worst-case PVT contexts.
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.
7075

7176
### Invariant checks
7277
- [ ] `./scripts/tri test` parse/typecheck/gen/seal-verify phases pass.

‎.trinity/current_task/activity.md‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1424,3 +1424,19 @@
14241424
- **Commit:** docs(w414): W414 setup - issue #1342, branch wave-loop-414, update NOW/plan/cooperation/report
14251425
- **Files:** .claude/plans/wave-loop-414.md,.claude/plans/wave-loop-415.md,.trinity/current-issue.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W415_2026-07-01.md,docs/reports/FPGA_LOOP_EVIDENCE_W414_2026-07-01.md,docs/reports/WAVE_LOOP_414_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
14261426

1427+
## 2026-07-04T15:45:49Z — wave-loop-415
1428+
- **Commit:** feat(igla/fpga): W414 Variant C — PVT envelope, multi-bit/real VCD, --validate
1429+
- **Files:** .claude/plans/wave-loop-415.md,.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"
1430+
1431+
## 2026-07-04T15:48:08Z — wave-loop-415
1432+
- **Commit:** feat(fpga): Wave Loop 15 — PVT-aware CCLK validation, VCD robustness, OSCFSEL theorem library
1433+
- **Files:** .claude/plans/wave-loop-415.md,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W416_2026-07-01.md
1434+
1435+
## 2026-07-04T16:03:17Z — wave-loop-416
1436+
- **Commit:** docs(w415): correct PR/issue numbers for W415 land and W416 setup
1437+
- **Files:** .claude/plans/wave-loop-416.md,.trinity/current-issue.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W417_2026-07-01.md,docs/reports/FPGA_LOOP_EVIDENCE_W416_2026-07-01.md,docs/reports/WAVE_LOOP_416_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
1438+
1439+
## 2026-07-04T16:31:20Z — wave-loop-416
1440+
- **Commit:** docs(w415): correct PR/issue numbers for W415 land and W416 setup
1441+
- **Files:** docs/NOW.md
1442+

‎.trinity/experience.md‎

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,49 @@
11
# t27 / Trinity Agent Experience Log
22

3+
## 2026-07-01 — Wave Loop 416 (PVT-envelope CLI, VCD parser coverage, OSCFSEL transaction theorems)
4+
5+
### What worked
6+
- Adding a standalone `tri fpga pvt-envelope` command separated the "inspect the
7+
envelope" use case from the "validate a capture" use case, making the PVT
8+
model discoverable without an instrument export.
9+
- Proving monotonicity of the temperature/voltage/process-corner derating
10+
functions in Lean 4 lets downstream reasoning pick any context inside the
11+
operating rectangle and know the bound moves in the expected direction
12+
(warmer / slower corner = larger derating; higher voltage = smaller derating).
13+
- Linking each OSCFSEL 0..7 nominal measured-CCLK rate to
14+
`transaction_satisfies_flash_spec` via the existing implication theorem reused
15+
the W410/W414 infrastructure without duplicating arithmetic.
16+
- Extending the line-oriented VCD parser for escaped identifiers, scalar x/z
17+
transitions, and hex bus literals was contained to the value/name extraction
18+
step and was validated by targeted unit tests before the full suite ran.
19+
20+
### What changed behavior
21+
- `cli/tri/src/fpga.rs`: added `FpgaCmd::PvtEnvelope` and `pvt_envelope()`;
22+
hardened `parse_vcd_to_raw_ns` for escaped names, scalar x/z, and hex bus
23+
literals; added 6 new unit tests.
24+
- `proofs/lean4/Trinity/TernaryFPGABoot.lean`: added PVT derating monotonicity
25+
lemmas and `oscfsel_<n>_measured_transaction_ok` for n = 0..7.
26+
- `fpga/HARDWARE_SSOT.md` §3.6.13: documented `tri fpga pvt-envelope` and W16
27+
VCD parser coverage; updated §3.6.9 to reference the OSCFSEL transaction theorems.
28+
- `docs/NOW.md`: W416 close-out and W417 setup.
29+
- Close-out artifacts: `docs/reports/WAVE_LOOP_416_REPORT.md`,
30+
`docs/reports/FPGA_LOOP_EVIDENCE_W416_2026-07-01.md`, and
31+
`docs/reports/FPGA_LOOP_COOPERATION_W417_2026-07-01.md`.
32+
33+
### Patterns to reuse
34+
- A small CLI helper that prints the formal model's parameters makes the model
35+
reviewable by humans and by CI without needing a full instrument export.
36+
- When a `Prop`-valued ordering definition (like `ProcessCorner.worse_than`) is
37+
only needed for concrete corner facts, prove those facts by unfolding the
38+
definition with `simp` rather than relying on `decide` to synthesize a
39+
`Decidable` instance.
40+
- When applying a single-implication theorem, check the actual number of
41+
subgoals produced by `apply` before adding bullet proofs; extra bullets produce
42+
"no goals to be solved" rather than a proof error.
43+
- Keep parser extensions behind unit tests that exercise the exact quirk
44+
(escaped identifier with space, scalar `x`/`z`, hex bus literal) so that future
45+
refactors do not silently drop the special case.
46+
347
## 2026-07-01 — Wave Loop 414 (PVT envelope, multi-bit/real VCD, `--validate`)
448

549
### What worked
@@ -1704,3 +1748,36 @@
17041748
`_name` to avoid linter warnings.
17051749
- Do not let autogenerated `.trinity/seals/*.json` and session logs leak into a
17061750
squash-merge commit; stage only human-authored source + generated reports.
1751+
1752+
## 2026-07-01 — Wave Loop 415 (PVT-aware validation + VCD robustness + OSCFSEL theorem library)
1753+
1754+
### What worked
1755+
- Delivered Variant C because the bench stayed blocked (P12 unwired, DLC10 cable missing, no relay).
1756+
- Wired the W414 PVT envelope into `tri fpga measure-cclk --validate --pvt-context <ctx.json>` and `tri fpga measured-to-lean --pvt-context <ctx.json>`.
1757+
- Generated Lean theorems now use `measured_cclk_with_pvt_satisfies_flash_spec` / `measured_cclk_from_raw_ns_with_pvt_satisfies_flash_spec` and link through the existing PVT implication theorems with `decide` bullets.
1758+
- Hardened the VCD parser against multi-line `$var` declarations, mixed scalar/bus dumps, duplicate transitions, and `$dumpoff`/`$dumpon` regions.
1759+
- Added a complete OSCFSEL 0..7 measured-CCLK theorem library under both nominal and worst-case PVT contexts in `TernaryFPGABoot.lean`.
1760+
- Updated `fpga/HARDWARE_SSOT.md` §3.6.12 with `--pvt-context` usage examples.
1761+
- Rewrote `docs/NOW.md` to English-only content and added W415 close-out / W416 setup.
1762+
- Resealed all specs so `Seal Verify: 576 passed, 0 failed`.
1763+
- `cargo test -p tri fpga::tests`: 32/32 PASS; `lake build Trinity.TernaryFPGABoot`: PASS (2967 jobs).
1764+
1765+
### What changed behavior
1766+
- `cli/tri/src/fpga.rs`: `--pvt-context` flag, PVT-aware validation, duplicate-transition filtering, multi-line VCD `$var` parsing.
1767+
- `proofs/lean4/Trinity/TernaryFPGABoot.lean`: 16 new OSCFSEL nominal/worst-case theorems.
1768+
- `fpga/HARDWARE_SSOT.md`: `--pvt-context` examples.
1769+
- `docs/NOW.md`: W15 close-out / W16 setup.
1770+
- `.trinity/seals/*.json`: resealed to current generated-code hashes.
1771+
- Close-out docs: `docs/reports/WAVE_LOOP_415_REPORT.md`, `docs/reports/FPGA_LOOP_EVIDENCE_W415_2026-07-01.md`, `docs/reports/FPGA_LOOP_COOPERATION_W416_2026-07-01.md`.
1772+
1773+
### Patterns to reuse
1774+
- When adding a new optional CLI path that affects generated Lean syntax, keep the Rust and Lean predicate names identical and reuse the existing implication theorems; this avoids coupling two models.
1775+
- For VCD robustness, ignore duplicate transitions and dump-off windows at parse time rather than at measurement time; this keeps the downstream period/duty computation simple and unchanged.
1776+
- For library-scale `decide`-only theorems, define a shared worst-case context constant and reference it in every theorem to avoid copy/paste errors.
1777+
- When `bootstrap/build.rs` rejects a doc for non-ASCII characters, translate the whole section to English instead of editing only the flagged line; the language check scans the entire file.
1778+
1779+
### Anti-patterns to avoid
1780+
- Do not create temp files in parallel tests using only `process::id()` in the filename; include a per-invocation counter or thread-local suffix to avoid races.
1781+
- Do not assume `t27c seal` persists; pass `--save` to update `.trinity/seals/*.json`.
1782+
- Do not mix `--margin` and `--pvt-context` in the same `measured-to-lean` invocation; use `clap` `conflicts_with` to make the CLI reject the ambiguous combination.
1783+
- Do not record a transition every time a value line is parsed; only record actual state changes, otherwise duty-cycle averages become distorted.

0 commit comments

Comments
 (0)