Skip to content

Wave Loop 426 — finite-grid PVT theorems, machine-readable tri fpga JSON, competitor refresh (Closes #1376)#1378

Open
gHashTag wants to merge 18 commits into
masterfrom
wave-loop-426
Open

Wave Loop 426 — finite-grid PVT theorems, machine-readable tri fpga JSON, competitor refresh (Closes #1376)#1378
gHashTag wants to merge 18 commits into
masterfrom
wave-loop-426

Conversation

@gHashTag

@gHashTag gHashTag commented Jul 5, 2026

Copy link
Copy Markdown
Owner

Wave Loop 426 Close-Out Report

Date: 2026-07-05
Issue: #1376
Branch: wave-loop-426
Variant executed: C (formal / tooling / competitor refresh)
Anchor: φ² + φ⁻² = 3 | TRINITY

Goal

Continue the FPGA boot-evidence line after Wave Loop 425. The bench remained
blocked (P12 CCLK probe unwired, no relay/remote-power gate, DLC10 missing), so
the wave executed Variant C from
docs/reports/FPGA_LOOP_COOPERATION_W426_2026-07-05.md.

What landed

  1. Finite-grid PVT theorems in Lean 4

    • File: proofs/lean4/Trinity/TernaryFPGABoot.lean
    • Theorems: pvt_half_ns_operating_rectangle_grid_bounded,
      pvt_low_ns_operating_rectangle_grid_bounded
    • Build: lake build Trinity.TernaryFPGABoot — 2967 jobs, 0 errors.

  2. Machine-readable tri fpga JSON output

    • File: cli/tri/src/fpga.rs
    • cclk-sweep logs now include pvt_envelope_margin_ns and recommendation.
    • boot-log and cold-por logs now include recommendation and
      pvt_envelope_margin_ns: null.
    • Added Rust mirror of the Lean cclk_nominal_hz table.

  3. Rust unit tests

    • 8 new tests for cclk_nominal_hz, pvt_envelope_margin_ns, and
      recommendation_from_conclusion.
    • cargo test -p tri — 101/101 pass.

  4. Competitor snapshot refresh

    • File: docs/reports/T27_VS_FORMAL_HDL_2026.md
    • Added Sparkle July 2026 Functional Matsuri talk and Clash 1.8.5
      verification fixes.

  5. Close-out artifacts

    • docs/reports/W426_WEAK_POINTS_AND_COMPETITORS.md
    • docs/reports/FPGA_LOOP_EVIDENCE_W426_2026-07-05.md
    • docs/reports/FPGA_LOOP_COOPERATION_W427_2026-07-05.md

Verification

Check Result
cargo test -p tri 101/101 pass
lake build Trinity.TernaryFPGABoot 2967 jobs, 0 errors
./scripts/tri test parse/typecheck/gen-zig/gen-rust/gen-c/seal-verify PASS
./scripts/tri test gen-verilog-yosys-smoke 7 pre-existing failures (#1245)

Weak points still open

Next wave

See docs/reports/FPGA_LOOP_COOPERATION_W427_2026-07-05.md for the W427
variant plan (Variant A if P12 is wired, Variant B if real XADC readout or
external capture is available, Variant C otherwise).

φ² + φ⁻² = 3 | TRINITY

Dmitrii Vasilev and others added 18 commits July 5, 2026 02:27
@claude
feat(igla): Wave Loop 420 — VCD exact-terminator + real-net auto-thre…
e01edd3 
…shold, PVT process-corner monotonicity

Closes #1361

Variant C fallback (bench still blocked: P12 unwired, DLC10 cable missing,
no relay). Instrument-import depth and formal guarding only.

- cli/tri/src/fpga.rs:
  - exact-token VCD $date/$version/$comment terminator with regression test
    for embedded $end-like tokens (closes W419 report/actual gap)
  - real-valued VCD net auto-threshold from observed voltage swing
  - PVT half-period process-corner monotonicity regression test
- proofs/lean4/Trinity/TernaryFPGABoot.lean:
  - pvt_half_ns_monotone_in_process_corner (ff ≤ tt ≤ ss)
- fpga/HARDWARE_SSOT.md: §3.6.17 documenting W420 VCD/PVT improvements
- .trinity/experience.md: W420 learnings
- docs/reports: W420 report, evidence, and W421 cooperation variants

Verification:
- cargo test -p tri vcd: 13/13 PASS
- cargo test -p tri pvt: 10/10 PASS
- cargo test -p tri fpga::tests: 48/48 PASS
- lake build Trinity.TernaryFPGABoot: PASS (2967 jobs)
- ./scripts/tri test: 16 pre-existing yosys failures (#1245), no new ones

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@claude
docs(now): record W420 PR #1362 and merge-pending status
7d8bae0 
Refs: #1362
Closes #1361

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@claude
docs(issue): set current issue to Wave Loop 421
5fe9fe4 
Closes #1363

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@claude
feat(igla): Wave Loop 421 — VCD $timescale exact terminator, combined…
c602505 
… PVT monotonicity, competitor snapshot

Closes #1363

Variant C fallback (bench still blocked: openFPGALoader --detect reports 0 devices).

- cli/tri/src/fpga.rs:
  - apply vcd_line_ends_with_token to $timescale terminator
  - add test_parse_vcd_timescale_with_embedded_end_token
  - add test_parse_vcd_real_auto_threshold_us_timescale
  - add test_pvt_half_ns_monotone_combined
- proofs/lean4/Trinity/TernaryFPGABoot.lean:
  - add pvt_half_ns_monotone_combined
- fpga/HARDWARE_SSOT.md: §3.6.18 documenting W421 improvements
- docs/reports/T27_VS_FORMAL_HDL_2026.md: competitor comparison
- .trinity/experience.md: W421 learnings
- docs/reports: W421 report, evidence, and W422 cooperation variants

Verification:
- cargo test -p tri vcd: 15/15 PASS
- cargo test -p tri pvt: 11/11 PASS
- cargo test -p tri fpga::tests: 51/51 PASS
- lake build Trinity.TernaryFPGABoot: PASS (2967 jobs)
- ./scripts/tri test: 16 pre-existing yosys failures (#1245), no new ones

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
docs(issue): set current issue to Wave Loop 422\n\nCloses #1365\n\nCo…
0fa33e3 
…-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@claude
feat(igla): Wave Loop 422 — live XC7A200T SRAM boot, Verilog keyword …
95f9ba7 
…escape, PVT worst-case bound

Closes #1365

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@claude
docs(issue): set current issue to Wave Loop 423
ea3e32e 
Closes #1368

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@claude
feat(igla): Wave Loop 423 — CSV time units, VCD slope filter, PVT wor…
b624405 
…st-case, competitor refresh (Closes #1368)

- cli/tri/src/fpga.rs: CSV ms/us/ns/sample-number normalization, VCD real-net
  slope filter, unknown timescale fallback, dumpoff/dumpon without timestamp,
  --pvt-worstcase mode; +10 regression tests (60/60 PASS).
- fpga/HARDWARE_SSOT.md: add §3.6.20 documenting W423 instrument-import depth.
- docs/reports/T27_VS_FORMAL_HDL_2026.md: refresh Sparkle/Verilean, Clash, CIRCT.
- docs/reports/WAVE_LOOP_423_REPORT.md, FPGA_LOOP_EVIDENCE_W423_2026-07-05.md,
  FPGA_LOOP_COOPERATION_W424_2026-07-05.md: W423 close-out + W424 variants.
- docs/NOW.md, .trinity/experience.md, .trinity/current-issue.md: W423 close-out
  and W424 setup.

Full sweep: 576 passed, 0 seal mismatches, 7 pre-existing gen-verilog yosys
smoke failures, 0 FPGA smoke failures.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@claude
setup(igla): Wave Loop 424 branch and issue (#1371)
d746f9d 
Update .trinity/current-issue.md and cooperation file with the new W424
issue number.

Reference #1371

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@claude
feat(igla): Wave Loop 424 — FPGA tooling hardening, PVT context, CSV …
bda6e1b 
…voltage units, non-blocking continue, W425 setup

- Add non-blocking wait_for_continue helper for boot-log/cold-por/cclk-sweep

- Parse CSV voltage units (v/mv) and scale to volts before threshold detection

- Embed optional PVT context + XADC placeholder into boot-log JSON

- Expand default CCLK sweep to OSCFSEL 0..7

- Add Lean 4 ProcessCorner decidability/severity helpers

- W424 report, evidence, and W425 cooperation variants

Closes #1371

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@claude
chore(tri): update session log and commit count after W424 close-out
59faa4b 
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@claude
docs(tri): W425 issue + NOW setup (#1374, wave-loop-425)
0baae16 
- Update .trinity/current-issue.md with W425 goal, plan, acceptance criteria

- Prepend W424 close-out and W425 setup to docs/NOW.md

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@claude
docs(tri): correct W425 issue reference to #1374
3960166 
Closes #1371

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@claude
merge W424 into W425
555ef7b 
Closes #1374

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@claude
feat(igla): Wave Loop 425 — OSCFSEL 0–7 sweep, PVT worst-case envelop…
7653d7e 
…e theorems (closes #1374)

- cli/tri/src/fpga.rs: expand cclk-sweep/smoke-gate default OSCFSEL range to 0–7
- proofs/lean4/Trinity/TernaryFPGABoot.lean: add pvt_half_ns_worst_case_is_upper_envelope
  and pvt_low_ns_worst_case_is_upper_envelope; move OSCFSEL_WORST_CASE_PVT_CONTEXT earlier
- docs/reports: W425 report, evidence, and W426 cooperation variants
- .trinity/current-issue.md + experience.md: W425 close-out learnings
- Variant C executed because P12 is still unwired and no relay gate is available

Verification: cargo test -p tri PASS, lake build PASS, tri test PASS (7 pre-existing gen-verilog yosys smoke failures unchanged)

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
docs(w426): set up Wave Loop 426 current issue (#1376)
ae095f5
chore(w426): merge wave-loop-425 close-out into W426 branch
a93aad5 
Inherit W425 changes (PR #1375, closes #1374) so W426 work builds on the
OSCFSEL 0–7 sweep and PVT worst-case envelope theorems.

[ref: #1374]
@claude
feat(igla): Wave Loop 426 — finite-grid PVT theorems, machine-readabl…
09f2e55 
…e tri fpga JSON, competitor refresh (Variant C)

Wave 426 executed Variant C because the physical bench is still blocked:
P12 CCLK probe unwired, no relay gate, DLC10 missing.

Deliverables:
- proofs/lean4/Trinity/TernaryFPGABoot.lean:
  - pvt_half_ns_operating_rectangle_grid_bounded
  - pvt_low_ns_operating_rectangle_grid_bounded
  - exhaustive 75-point worst-case corner dominance proof
- cli/tri/src/fpga.rs:
  - cclk_nominal_hz mirror of the Lean CCLK table
  - pvt_envelope_margin_ns and recommendation_from_conclusion helpers
  - SweepLog, boot-log, and cold-por JSON now emit recommendation and margin
  - 8 new unit tests (101/101 pass)
- docs/reports/T27_VS_FORMAL_HDL_2026.md: Sparkle July 2026 Functional Matsuri
  talk, Clash 1.8.5 verification fixes, CIRCT/firtool notes
- docs/reports/W426_WEAK_POINTS_AND_COMPETITORS.md: updated weak-point scan
- docs/reports/WAVE_LOOP_426_REPORT.md and FPGA_LOOP_EVIDENCE_W426_2026-07-05.md
- docs/reports/FPGA_LOOP_COOPERATION_W427_2026-07-05.md: next-wave variants
- .trinity/experience.md: W426 learnings
- docs/NOW.md: W426 close-out / W427 setup
- .trinity/current-issue.md: mark Variant C acceptance criteria complete

Verification:
- cargo test -p tri: 101/101 pass
- lake build Trinity.TernaryFPGABoot: 2967 jobs, 0 errors
- ./scripts/tri test: parse/typecheck/gen/seal-verify PASS; 7 pre-existing
  gen-verilog-yosys-smoke failures (#1245) unchanged

Closes #1376

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This was referenced Jul 5, 2026
Merged
Merged
Open
Merged
Open
Closed
Closed
Closed
Closed
Closed
Closed
Open
This was referenced Jul 6, 2026
Open
Open
Open
@gHashTag

gHashTag commented Jul 6, 2026

Copy link
Copy Markdown
Owner Author

Closing: stale wave-loop-4xx PR, superseded by later waves. Reopen if still relevant.

@gHashTag gHashTag closed this Jul 6, 2026
@gHashTag gHashTag reopened this Jul 6, 2026
This was referenced Jul 6, 2026
Open
Merged
Open
Merged
Merged
Merged
Draft
Open
Merged
Merged
Open
Open
Open
Open
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@gHashTag