feat(fpga): Wave Loop 416 — PVT-envelope CLI, VCD parser coverage, OSCFSEL transaction theorems by gHashTag · Pull Request #1352 · gHashTag/t27

gHashTag · 2026-07-04T16:27:03Z

Wave Loop 416 continues the FPGA boot-evidence formal pipeline while the physical bench remains blocked.

What changed

Added tri fpga pvt-envelope --pvt-context helper that prints the PVT-derated N25Q128_3V SCK low/high bound, margin over the nominal 6 ns bound, and envelope-validity warnings.
Hardened the VCD parser for escaped identifiers with embedded spaces, scalar x/z transitions, and hex bus literals.
Proved PVT derating monotonicity in Lean 4 (temperature monotone, voltage antitone, ff<=tt<=ss corner ordering).
Linked OSCFSEL 0..7 nominal measured-CCLK theorems to transaction_satisfies_flash_spec via oscfsel_n_measured_transaction_ok.
Updated fpga/HARDWARE_SSOT.md, docs/NOW.md, .trinity/current-issue.md, .trinity/experience.md.
Added W416 report, evidence, and W417 cooperation variants.

Verification

cargo test -p tri fpga::tests: 38/38 PASS (71/71 full tri package).
lake build Trinity.TernaryFPGABoot: PASS (2967 jobs).
./scripts/tri test: parse/typecheck/GF16/gen-Zig/gen-Rust/gen-Verilog/seal/C/fixed-point PASS; gen-verilog-yosys-smoke has 16 pre-existing failures from weak point gen-verilog: 5 lowering defects block iverilog-clean RTL from non-trivial specs #1245.

🤖 Generated with Claude Code

… 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>

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

…CFSEL 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>

github-actions · 2026-07-04T16:27:13Z

📓 NotebookLM Notebook linked to this PR

Notebook ID: b83263109fb055dc
URL: https://notebooklm.google.com/notebook/b83263109fb055dc

This notebook contains session context, decisions, and artifacts for this work.

github-actions · 2026-07-04T16:27:18Z

PR Dashboard

Generated at: 2026-07-04 16:27:15 UTC

feat(fpga): Wave Loop 416 — PVT-envelope CLI, VCD parser coverage, OSCFSEL transaction theorems #1352 feat(fpga): Wave Loop 416 — PVT-envelope CLI, VCD parser coverage, OSCFSEL transaction theorems | Created: 2026-07-04 | Updated: 2026-07-04 | 11 failing / 17 total
feat(fpga): Wave Loop 415 reland — PVT-aware CCLK validation, VCD robustness, OSCFSEL theorem library #1351 feat(fpga): Wave Loop 415 reland — PVT-aware CCLK validation, VCD robustness, OSCFSEL theorem library | Created: 2026-07-04 | Updated: 2026-07-04 | 3 failing / 18 total
fix(build): downgrade docs/*.md Cyrillic check panic→warning (unblocks downstream) #1348 fix(build): downgrade docs/*.md Cyrillic check panic→warning (unblocks downstream) | Created: 2026-07-04 | Updated: 2026-07-04 | 8 failing / 27 total
feat(igla): Wave Loop 410 - measured-duty formal link and Rust JSON export #1330 feat(igla): Wave Loop 410 - measured-duty formal link and Rust JSON export | Created: 2026-07-04 | Updated: 2026-07-04 | 0 failing / 3 total
Wave Loop 409 — per-OSCFSEL SPI transaction lookup + tighter duty bound #1324 Wave Loop 409 — per-OSCFSEL SPI transaction lookup + tighter duty bound | Created: 2026-07-04 | Updated: 2026-07-04 | 0 failing / 4 total
Wave Loop 408 — real P12 CCLK attempt + SPI transaction model in Lean 4 #1322 Wave Loop 408 — real P12 CCLK attempt + SPI transaction model in Lean 4 | Created: 2026-07-04 | Updated: 2026-07-04 | 0 failing / 4 total
feat(igla): Wave Loop 407 — deeper N25Q128 SPI timing in Lean 4 + synthetic CCLK fixture #1317 feat(igla): Wave Loop 407 — deeper N25Q128 SPI timing in Lean 4 + synthetic CCLK fixture | Created: 2026-07-04 | Updated: 2026-07-04 | 5 failing / 26 total
feat(igla): Wave Loop 406 — live CCLK capture + OSCFSEL/CCLK flash-spec safety in Lean 4 #1315 feat(igla): Wave Loop 406 — live CCLK capture + OSCFSEL/CCLK flash-spec safety in Lean 4 | Created: 2026-07-04 | Updated: 2026-07-04 | 5 failing / 25 total
chore(ci)(deps): bump actions/download-artifact from 4 to 8 #1238 chore(ci)(deps): bump actions/download-artifact from 4 to 8 | Created: 2026-07-01 | Updated: 2026-07-01 | 3 failing / 26 total
chore(ci)(deps): bump docker/build-push-action from 6 to 7 #1237 chore(ci)(deps): bump docker/build-push-action from 6 to 7 | Created: 2026-07-01 | Updated: 2026-07-01 | 0 failing / 17 total
chore(ci)(deps): bump actions/upload-artifact from 4 to 7 #1236 chore(ci)(deps): bump actions/upload-artifact from 4 to 7 | Created: 2026-07-01 | Updated: 2026-07-01 | 4 failing / 29 total
chore(deps)(deps): bump uuid from 1.23.2 to 1.23.4 #1227 chore(deps)(deps): bump uuid from 1.23.2 to 1.23.4 | Created: 2026-06-29 | Updated: 2026-06-29 | 3 failing / 25 total
chore(deps)(deps): bump candle-nn from 0.10.2 to 0.11.0 #1226 chore(deps)(deps): bump candle-nn from 0.10.2 to 0.11.0 | Created: 2026-06-29 | Updated: 2026-06-29 | 3 failing / 25 total
docs(metrics): сводка ключевых метрик 83 числовых форматов (SSOT-derived) #1225 docs(metrics): сводка ключевых метрик 83 числовых форматов (SSOT-derived) | Created: 2026-06-28 | Updated: 2026-06-28 | 3 failing / 17 total
chore(deps)(deps): bump tower-http from 0.6.8 to 0.7.0 #1220 chore(deps)(deps): bump tower-http from 0.6.8 to 0.7.0 | Created: 2026-06-22 | Updated: 2026-06-22 | 3 failing / 25 total
conformance: promote gf10/gf256 to bitexact_selfconsistent (WP-34) #1216 conformance: promote gf10/gf256 to bitexact_selfconsistent (WP-34) | Created: 2026-06-19 | Updated: 2026-06-19 | 0 failing / 19 total
chore(deps)(deps): bump ignore from 0.4.25 to 0.4.26 #1145 chore(deps)(deps): bump ignore from 0.4.25 to 0.4.26 | Created: 2026-06-15 | Updated: 2026-06-15 | 1 failing / 25 total
chore(deps)(deps): bump regex from 1.12.3 to 1.12.4 #1143 chore(deps)(deps): bump regex from 1.12.3 to 1.12.4 | Created: 2026-06-15 | Updated: 2026-06-15 | 1 failing / 25 total
conformance(gf14): add 14 bit-exact GF14 vectors (52 -> 53) #1142 conformance(gf14): add 14 bit-exact GF14 vectors (52 -> 53) | Created: 2026-06-15 | Updated: 2026-06-15 | 0 failing / 19 total
ci(trust): OpenSSF Scorecard + SBOM + Sigstore signed releases #1141 ci(trust): OpenSSF Scorecard + SBOM + Sigstore signed releases | Created: 2026-06-15 | Updated: 2026-06-15 | 3 failing / 17 total
fix(gen): untrack stale gen/numeric catalog artifacts (committed gen drifts 77 vs SSOT 83) -- Closes #1120 #1128 fix(gen): untrack stale gen/numeric catalog artifacts (committed gen drifts 77 vs SSOT 83) -- Closes #1120 | Created: 2026-06-14 | Updated: 2026-06-14 | 0 failing / 21 total

Summary

Status	Count
Total Open PRs	21
PRs with Failing Checks	13
PRs with All Checks Green	8
READY	7
FAILING	13
PENDING	0

Seal Status

⚠️ STALE -- sha256(compiler.rs)=621b9883e268 != manifest seal=49e55df6d444.
The committed NMSE numbers were certified against an older compiler.rs.
Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

…pdated line

github-actions · 2026-07-04T16:31:37Z

PR Dashboard

Generated at: 2026-07-04 16:31:35 UTC

feat(fpga): Wave Loop 416 — PVT-envelope CLI, VCD parser coverage, OSCFSEL transaction theorems #1352 feat(fpga): Wave Loop 416 — PVT-envelope CLI, VCD parser coverage, OSCFSEL transaction theorems | Created: 2026-07-04 | Updated: 2026-07-04 | 12 failing / 16 total
feat(fpga): Wave Loop 415 reland — PVT-aware CCLK validation, VCD robustness, OSCFSEL theorem library #1351 feat(fpga): Wave Loop 415 reland — PVT-aware CCLK validation, VCD robustness, OSCFSEL theorem library | Created: 2026-07-04 | Updated: 2026-07-04 | 3 failing / 25 total
fix(build): downgrade docs/*.md Cyrillic check panic→warning (unblocks downstream) #1348 fix(build): downgrade docs/*.md Cyrillic check panic→warning (unblocks downstream) | Created: 2026-07-04 | Updated: 2026-07-04 | 6 failing / 28 total
chore(ci)(deps): bump actions/download-artifact from 4 to 8 #1238 chore(ci)(deps): bump actions/download-artifact from 4 to 8 | Created: 2026-07-01 | Updated: 2026-07-01 | 3 failing / 26 total
chore(ci)(deps): bump docker/build-push-action from 6 to 7 #1237 chore(ci)(deps): bump docker/build-push-action from 6 to 7 | Created: 2026-07-01 | Updated: 2026-07-01 | 0 failing / 17 total
chore(ci)(deps): bump actions/upload-artifact from 4 to 7 #1236 chore(ci)(deps): bump actions/upload-artifact from 4 to 7 | Created: 2026-07-01 | Updated: 2026-07-01 | 4 failing / 29 total
chore(deps)(deps): bump uuid from 1.23.2 to 1.23.4 #1227 chore(deps)(deps): bump uuid from 1.23.2 to 1.23.4 | Created: 2026-06-29 | Updated: 2026-06-29 | 3 failing / 25 total
chore(deps)(deps): bump candle-nn from 0.10.2 to 0.11.0 #1226 chore(deps)(deps): bump candle-nn from 0.10.2 to 0.11.0 | Created: 2026-06-29 | Updated: 2026-06-29 | 3 failing / 25 total
docs(metrics): сводка ключевых метрик 83 числовых форматов (SSOT-derived) #1225 docs(metrics): сводка ключевых метрик 83 числовых форматов (SSOT-derived) | Created: 2026-06-28 | Updated: 2026-06-28 | 3 failing / 17 total
chore(deps)(deps): bump tower-http from 0.6.8 to 0.7.0 #1220 chore(deps)(deps): bump tower-http from 0.6.8 to 0.7.0 | Created: 2026-06-22 | Updated: 2026-06-22 | 3 failing / 25 total
conformance: promote gf10/gf256 to bitexact_selfconsistent (WP-34) #1216 conformance: promote gf10/gf256 to bitexact_selfconsistent (WP-34) | Created: 2026-06-19 | Updated: 2026-06-19 | 0 failing / 19 total
chore(deps)(deps): bump ignore from 0.4.25 to 0.4.26 #1145 chore(deps)(deps): bump ignore from 0.4.25 to 0.4.26 | Created: 2026-06-15 | Updated: 2026-06-15 | 1 failing / 25 total
chore(deps)(deps): bump regex from 1.12.3 to 1.12.4 #1143 chore(deps)(deps): bump regex from 1.12.3 to 1.12.4 | Created: 2026-06-15 | Updated: 2026-06-15 | 1 failing / 25 total
conformance(gf14): add 14 bit-exact GF14 vectors (52 -> 53) #1142 conformance(gf14): add 14 bit-exact GF14 vectors (52 -> 53) | Created: 2026-06-15 | Updated: 2026-06-15 | 0 failing / 19 total
ci(trust): OpenSSF Scorecard + SBOM + Sigstore signed releases #1141 ci(trust): OpenSSF Scorecard + SBOM + Sigstore signed releases | Created: 2026-06-15 | Updated: 2026-06-15 | 3 failing / 17 total
fix(gen): untrack stale gen/numeric catalog artifacts (committed gen drifts 77 vs SSOT 83) -- Closes #1120 #1128 fix(gen): untrack stale gen/numeric catalog artifacts (committed gen drifts 77 vs SSOT 83) -- Closes #1120 | Created: 2026-06-14 | Updated: 2026-06-14 | 0 failing / 21 total

Summary

Status	Count
Total Open PRs	16
PRs with Failing Checks	11
PRs with All Checks Green	5
READY	4
FAILING	11
PENDING	0

Seal Status

⚠️ STALE -- sha256(compiler.rs)=621b9883e268 != manifest seal=49e55df6d444.
The committed NMSE numbers were certified against an older compiler.rs.
Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

github-actions · 2026-07-04T16:31:37Z

📓 NotebookLM Notebook linked to this PR

Notebook ID: b83263109fb055dc
URL: https://notebooklm.google.com/notebook/b83263109fb055dc

This notebook contains session context, decisions, and artifacts for this work.

gHashTag and others added 3 commits July 4, 2026 23:23

docs(w415): correct PR/issue numbers for W415 land and W416 setup

4d3f35f

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

gHashTag enabled auto-merge (squash) July 4, 2026 16:28

docs(NOW): W418 header, fix W417 issue reference to #1350, add Last u…

1962258

…pdated line

gHashTag merged commit 5d51a6a into master Jul 4, 2026
16 of 18 checks passed

This was referenced Jul 4, 2026

feat(fpga): Wave Loop 415 reland — PVT-aware CCLK validation, VCD robustness, OSCFSEL theorem library #1351

Closed

docs(w417): hygiene, Strategy P, legacy allowlist, W417 close-out artifacts #1354

Merged

Navigation Menu

Repository navigation

feat(fpga): Wave Loop 416 — PVT-envelope CLI, VCD parser coverage, OSCFSEL transaction theorems - #1352

feat(fpga): Wave Loop 416 — PVT-envelope CLI, VCD parser coverage, OSCFSEL transaction theorems#1352
gHashTag merged 4 commits into
masterfrom
wave-loop-416

gHashTag commented Jul 4, 2026

Uh oh!

github-actions Bot commented Jul 4, 2026

Uh oh!

github-actions Bot commented Jul 4, 2026

Uh oh!

github-actions Bot commented Jul 4, 2026

Uh oh!

github-actions Bot commented Jul 4, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

gHashTag commented Jul 4, 2026

Uh oh!

github-actions Bot commented Jul 4, 2026

Uh oh!

github-actions Bot commented Jul 4, 2026

PR Dashboard

Summary

Seal Status

Uh oh!

github-actions Bot commented Jul 4, 2026

PR Dashboard

Summary

Seal Status

Uh oh!

github-actions Bot commented Jul 4, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant