feat(igla): Wave Loop 431 — XADC→PVT context bridge, computable envelope, measured-to-lean --json summary hardening

Closes #1389

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

Author: Dmitrii Vasilev

.trinity/current-issue.md

@@ -1,60 +1,61 @@
-# Wave Loop 431 — FPGA boot-evidence next variant (physical CCLK / XADC sweep / formal fallback)
+# Wave Loop 432 — FPGA boot-evidence next variant (real CCLK capture, live XADC validation, or master-merge)
 
-**Issue:** #1389  
-**Branch:** `wave-loop-431`  
-**Milestone:** Continue the FPGA boot-evidence line from Wave Loop 430.
+**Issue:** #1391  
+**Branch:** `wave-loop-432`  
+**Milestone:** Continue the FPGA boot-evidence line from Wave Loop 431.
 
 ---
 
 ## Goal
 
-Wave Loop 430 added live XADC readout and a formal PVT-envelope bridge while
-the bench remained partially blocked (P12 unwired, no relay gate, no DLC10
-cable). Wave Loop 431 executes the first available variant from
-`docs/reports/FPGA_LOOP_COOPERATION_W431_2026-07-01.md`.
+Wave Loop 431 hardened the XADC → PVT context bridge, added a computable Lean 4
+envelope check, and improved the machine-readable `measured-to-lean --json`
+summary while the bench remained partially blocked (P12 unwired, no relay gate,
+no DLC10 cable). Wave Loop 432 executes the first available variant from
+`docs/reports/FPGA_LOOP_COOPERATION_W432_2026-07-01.md`.
 
 1. **Variant A (preferred when bench becomes fully available):**
    - Confirm P12 is wired to a logic-analyzer channel and a relay/remote-power
      gate is available.
-   - Program SPI flash with OSCFSEL=6 and OSCFSEL=7 variants.
-   - Capture real CCLK during cold-POR boot for both variants.
-   - Run `tri fpga cclk-sweep ... --xadc` so boot logs record live operating
-     points.
+   - Program SPI flash with OSCFSEL=6 (and OSCFSEL=7 if time permits).
+   - Capture real CCLK during cold-POR boot.
+   - Run `tri fpga cclk-sweep ... --xadc` so boot logs record live operating points.
    - Import with `tri fpga measured-to-lean --csv/--vcd --raw-ns --standalone
-     --validate --pvt-context <ctx.json> --out <theorem.lean> --json` and commit
+     --validate --pvt-context <xadc.json> --out <theorem.lean> --json` and commit
      generated Lean theorems plus JSON summaries.
-   - Document frequencies, duty cycles, and XADC/PVT context in
-     `fpga/HARDWARE_SSOT.md` §3.6 / §9.6.
+   - Update `fpga/HARDWARE_SSOT.md` §3.6 with measured frequency/duty/margin.
 
 2. **Variant B (if board is reachable but P12 / relay are still blocked):**
-   - Run a real `tri fpga cclk-sweep` over OSCFSEL 0..7 with `--xadc` and a
-     supplied `--pvt-context`, performing manual power cycles.
-   - Alternatively, import at least one external CSV/VCD capture end-to-end.
-   - Add a Lean theorem or decidability lemma connecting a concrete XADC JSON
-     operating point to `xadc_operating_point_envelope_implies_worst_case_bound`.
-   - Document the sweep/import recipe in `fpga/HARDWARE_SSOT.md`.
+   - Capture a real `tri fpga read-xadc --json` from the live board.
+   - Verify the JSON converts to a valid `PvtContext` via `tri fpga pvt-envelope`.
+   - Generate at least one `measured-to-lean` theorem using the real XADC context
+     (synthetic CCLK fixture is acceptable for proof-of-pipeline).
+   - Alternatively, run `tri fpga cclk-sweep` over OSCFSEL 0..5 with `--xadc` and
+     manual power cycles.
+   - Refresh `docs/reports/T27_VS_FORMAL_HDL_2026.md` and re-evaluate
+     `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md`.
 
 3. **Variant C (fallback if bench still blocked):**
-   - Extend the XADC/PVT theorem library (e.g. computable envelope check or an
-     implication theorem linking measured raw-ns + XADC to transaction OK).
-   - Land one safe gen-verilog #1245 sub-fix if narrow and regression-free;
-     otherwise explicitly defer and update
-     `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md`.
-   - Harden `tri fpga measured-to-lean` JSON output further.
-   - Refresh `docs/reports/T27_VS_FORMAL_HDL_2026.md` if new competitor signals
-     appear.
+   - Execute the deferred master-merge/rebase wave to bring the `master` fix set
+     (`701d79b3b`) into `wave-loop-432` and clear the 7 residual yosys smoke
+     failures (#1245).
+   - If the merge is too risky for one wave, land a formal/tooling sub-task:
+     per-OSCFSEL PVT-corner theorems, machine-readable `sweep-report --json`, or
+     a deeper competitor refresh.
+   - Update `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md` with the new baseline.
 
 ---
 
 ## Definition of done
 
 - [ ] The chosen variant is executed and its acceptance criteria are met.
 - [ ] `lake build Trinity.TernaryFPGABoot` passes.
-- [ ] `./scripts/tri test` passes with no new failures beyond the documented
-      7 gen-verilog #1245 failures.
+- [ ] `./scripts/tri test` passes with the new documented baseline (ideally 0 new
+      gen-verilog failures; if Variant C succeeds, the 7 #1245 failures are
+      cleared).
 - [ ] `cargo test --bin tri fpga::` passes.
 - [ ] Close-out report and next-wave cooperation variants are written.
-- [ ] Issue/branch for Wave Loop 432 are created.
+- [ ] Issue/branch for Wave Loop 433 are created.
 
 ---
 

.trinity/current_task/activity.md

@@ -1588,3 +1588,7 @@
 - **Commit:** feat(igla): Wave Loop 430 — live XADC readout, PVT-envelope bridge, W431 cooperation\n\n- Add tri fpga read-xadc and --xadc flags on boot-log/cold-por/cclk-sweep.\n- Parse openFPGALoader --read-xadc output and embed live temp/vccint/vccaux in JSON logs.\n- Add XadcOperatingPoint formal bridge and worst-case-bound theorem in TernaryFPGABoot.lean.\n- Update fpga/HARDWARE_SSOT.md, T27_VS_FORMAL_HDL_2026.md, GEN_VERILOG_DEFECTS_REPRO.md.\n- Create WAVE_LOOP_430_REPORT.md and FPGA_LOOP_COOPERATION_W431_2026-07-01.md.\n- Verification: cargo test fpga:: 79/79, lake build pass, tri test pass except 7 pre-existing #1245 failures.\n\nCloses #1388\n\nCo-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 - **Files:** .trinity/experience.md
 
+## 2026-07-05T10:42:19Z — wave-loop-431
+- **Commit:** docs(trinity): W431 setup — current issue, NOW, experience (Wave Loop 430 close-out)\n\n- Point .trinity/current-issue.md and docs/NOW.md to W431 (#1389).\n- Add W430 learnings to .trinity/experience.md.\n\nCo-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
+- **Files:** .trinity/current-issue.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W432_2026-07-01.md,docs/reports/FPGA_LOOP_EVIDENCE_W431_2026-07-01.md,docs/reports/GEN_VERILOG_DEFECTS_REPRO.md,docs/reports/T27_VS_FORMAL_HDL_2026.md,docs/reports/WAVE_LOOP_431_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
+

.trinity/experience.md

@@ -1,3 +1,60 @@
+## 2026-07-01 — Wave Loop 431 (FPGA boot-evidence: XADC → PVT context bridge, computable envelope check, `measured-to-lean --json` summary hardening, W431 close-out / W432 setup)
+
+### What worked
+- Executing **Variant C** kept the wave shippable: P12 and the relay gate are
+  still unwired, so the wave focused on formal/tooling debt instead of physical
+  capture.
+- Converting live XADC `f64` values (°C / V) into the integer `PvtContext` in
+  `XadcContext::to_pvt_context` removes the manual JSON editing step and makes
+  `tri fpga read-xadc --json` directly consumable as `--pvt-context`.
+- Writing a direct `Bool` envelope check (`xadc_operating_point_within_envelope_dec`)
+  and proving equivalence with the propositional version avoids the Lean
+  `Decidable` synthesis failure that blocked the naive `decide (predicate pt)`
+  approach.
+- Proving `xadc_envelope_implies_raw_ns_satisfies_any_in_envelope` and
+  `xadc_envelope_justifies_worstcase_transaction_proof` means a real, in-envelope
+  XADC measurement can be used in proof goals without weakening the existing
+  worst-case transaction theorem.
+- Extending `build_measured_to_lean_summary` with `flash_min_half_period_ns`,
+  `margin_ns`, and a closed `recommendation` vocabulary gives downstream CI a
+  machine-readable signal instead of free-form text.
+- Updating the existing summary unit tests to assert the new fields catches
+  schema drift immediately.
+- Keeping the gen-verilog #1245 deferral explicit in
+  `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md` prevents scope creep.
+
+### What changed behavior
+- `cli/tri/src/fpga.rs`:
+  - Added `XadcContext::to_pvt_context` and unit tests for rounding / unit
+    conversion.
+  - Extended `build_measured_to_lean_summary` with `flash_min_half_period_ns`,
+    `margin_ns`, and `recommendation`.
+  - Updated unit tests for the summary builder.
+- `proofs/lean4/Trinity/TernaryFPGABoot.lean`:
+  - Added `xadc_operating_point_within_envelope_dec` with proven `Bool` ↔
+    propositional equivalence.
+  - Added `xadc_envelope_implies_raw_ns_satisfies_any_in_envelope`.
+  - Added `xadc_envelope_justifies_worstcase_transaction_proof`.
+- `fpga/HARDWARE_SSOT.md`: added §9.6.1 documenting the XADC → PVT bridge and
+  the `--json` summary fields.
+- `docs/reports/T27_VS_FORMAL_HDL_2026.md`: refreshed for W431; noted Sparkle
+  July 2026 activity signals.
+- `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md`: added W431 triage decision
+  confirming the same 7 residual yosys smoke failures and recommending a
+  dedicated master-merge wave in W432.
+- Close-out artifacts: `docs/reports/WAVE_LOOP_431_REPORT.md`,
+  `docs/reports/FPGA_LOOP_EVIDENCE_W431_2026-07-01.md`,
+  `docs/reports/FPGA_LOOP_COOPERATION_W432_2026-07-01.md`.
+- Issue/branch: GitHub issue #1391, branch `wave-loop-432`; PR closes #1389.
+
+### Verification
+- `cargo test --bin tri fpga::`: 81/81 pass.
+- `lake build Trinity.TernaryFPGABoot`: 2967 jobs, 0 errors.
+- `./scripts/tri test`: all phases pass; 7 pre-existing gen-verilog yosys smoke
+  failures (#1245); 0 FPGA smoke failures; 0 seal mismatches.
+
+---
+
 ## 2026-07-01 — Wave Loop 430 (FPGA boot-evidence: live XADC readout, PVT-envelope bridge, W430 close-out / W431 setup)
 
 ### What worked

cli/tri/src/fpga.rs

@@ -2694,6 +2694,30 @@ impl XadcContext {
         }
         value
     }
+
+    /// Convert the live XADC readout to the `PvtContext` used by the PVT envelope.
+    /// The XADC reports temperatures in °C and voltages in volts, while the PVT
+    /// model uses integer °C and millivolts. Values are rounded to the nearest
+    /// integer. The process corner is not measured by the XADC and must be
+    /// supplied by the caller (default `ss` for worst-case reasoning).
+    fn to_pvt_context(&self, corner: ProcessCorner) -> Result<PvtContext> {
+        let temp_c = self
+            .temp_c
+            .round()
+            .clamp(i64::MIN as f64, i64::MAX as f64) as i64;
+        let vccint_mv = (self.vccint_v * 1000.0)
+            .round()
+            .clamp(0.0, u64::MAX as f64) as u64;
+        let vccaux_mv = (self.vccaux_v * 1000.0)
+            .round()
+            .clamp(0.0, u64::MAX as f64) as u64;
+        Ok(PvtContext {
+            temp_c,
+            vccint_mv,
+            vccaux_mv,
+            process_corner: corner,
+        })
+    }
 }
 
 /// Remove trailing commas that appear immediately before a closing brace or
@@ -3537,7 +3561,7 @@ fn build_measured_to_lean_summary(
     pvt_ctx: &Option<PvtContext>,
     text: &str,
 ) -> Result<serde_json::Value> {
-    let (source, theorem_base, predicate) = if raw_ns {
+    let (source, theorem_base, predicate, period_ns, low_ns, high_ns) = if raw_ns {
         let m: MeasuredCclkRawNs =
             serde_json::from_str(text).context("parse MeasuredCclkRawNs JSON for summary")?;
         let source_suffix = sanitize_lean_ident(&m.source);
@@ -3557,7 +3581,14 @@ fn build_measured_to_lean_summary(
         } else {
             "measured_cclk_from_raw_ns_satisfies_flash_spec"
         };
-        (m.source, theorem_base, predicate.to_string())
+        (
+            m.source,
+            theorem_base,
+            predicate.to_string(),
+            m.period_ns,
+            m.sck_low_ns,
+            m.sck_high_ns,
+        )
     } else {
         let m: MeasuredCclk =
             serde_json::from_str(text).context("parse MeasuredCclk JSON for summary")?;
@@ -3575,7 +3606,32 @@ fn build_measured_to_lean_summary(
         } else {
             "measured_cclk_satisfies_flash_spec"
         };
-        (m.source, theorem_base, predicate.to_string())
+        (
+            m.source,
+            theorem_base,
+            predicate.to_string(),
+            m.period_ns,
+            m.sck_low_ns,
+            m.sck_high_ns,
+        )
+    };
+
+    // Compute the flash-spec minimum half-period and the measured margin.
+    let nominal_min_half_ns = (N25Q128_MIN_SCK_LOW_S * 1.0e9).round() as i64;
+    let flash_min_half_period_ns = pvt_ctx
+        .as_ref()
+        .map(|ctx| n25q128_min_sck_half_ns_pvt(ctx) as i64)
+        .unwrap_or(nominal_min_half_ns);
+    let measured_min_half_ns = std::cmp::min(low_ns, high_ns) as i64;
+    let margin_ns = measured_min_half_ns - flash_min_half_period_ns;
+    let recommendation = if pvt_ctx.is_none() {
+        "needs_pvt_context"
+    } else if raw_ns && low_ns + high_ns != period_ns {
+        "out_of_spec"
+    } else if margin_ns >= 0 {
+        "in_spec"
+    } else {
+        "out_of_spec"
     };
 
     Ok(serde_json::json!({
@@ -3585,6 +3641,9 @@ fn build_measured_to_lean_summary(
         "pvt_context": pvt_ctx.as_ref().map(|ctx| serde_json::to_value(ctx).unwrap_or(serde_json::Value::Null)),
         "raw_ns": raw_ns,
         "margin": margin,
+        "flash_min_half_period_ns": flash_min_half_period_ns,
+        "margin_ns": margin_ns,
+        "recommendation": recommendation,
     }))
 }
 
@@ -6452,6 +6511,12 @@ mod tests {
         assert_eq!(summary["raw_ns"].as_bool().unwrap(), false);
         assert_eq!(summary["margin"].as_bool().unwrap(), false);
         assert!(summary["pvt_context"].is_null());
+        assert_eq!(summary["flash_min_half_period_ns"].as_i64().unwrap(), 6);
+        assert_eq!(summary["margin_ns"].as_i64().unwrap(), 194);
+        assert_eq!(
+            summary["recommendation"].as_str().unwrap(),
+            "needs_pvt_context"
+        );
     }
 
     #[test]
@@ -6476,6 +6541,12 @@ mod tests {
         );
         assert_eq!(summary["raw_ns"].as_bool().unwrap(), true);
         assert!(summary["pvt_context"].is_null());
+        assert_eq!(summary["flash_min_half_period_ns"].as_i64().unwrap(), 6);
+        assert_eq!(summary["margin_ns"].as_i64().unwrap(), 14);
+        assert_eq!(
+            summary["recommendation"].as_str().unwrap(),
+            "needs_pvt_context"
+        );
     }
 
     #[test]
@@ -6499,6 +6570,9 @@ mod tests {
         let ctx_out = summary["pvt_context"].as_object().unwrap();
         assert_eq!(ctx_out["temp_c"].as_i64().unwrap(), 85);
         assert_eq!(ctx_out["process_corner"].as_str().unwrap(), "ss");
+        assert_eq!(summary["flash_min_half_period_ns"].as_i64().unwrap(), 13);
+        assert_eq!(summary["margin_ns"].as_i64().unwrap(), 7);
+        assert_eq!(summary["recommendation"].as_str().unwrap(), "in_spec");
     }
 
     #[test]
@@ -8329,4 +8403,45 @@ mod tests {
         assert_eq!(json["temp_c"], 35);
         assert_eq!(json["vccint_mv"], 1000);
     }
+
+    #[test]
+    fn test_xadc_context_to_pvt_context_rounds_and_converts_units() {
+        let ctx = XadcContext {
+            temp_c: 42.7,
+            max_temp_c: 85.0,
+            min_temp_c: -40.0,
+            vccint_v: 1.00049,
+            max_vccint_v: 1.050,
+            min_vccint_v: 0.950,
+            vccaux_v: 1.80615,
+            max_vccaux_v: 1.890,
+            min_vccaux_v: 1.710,
+            raw: None,
+        };
+        let pvt = ctx.to_pvt_context(ProcessCorner::Ss).unwrap();
+        assert_eq!(pvt.temp_c, 43);
+        assert_eq!(pvt.vccint_mv, 1000);
+        assert_eq!(pvt.vccaux_mv, 1806);
+        assert_eq!(pvt.process_corner, ProcessCorner::Ss);
+    }
+
+    #[test]
+    fn test_xadc_context_to_pvt_context_negative_temp_rounds() {
+        let ctx = XadcContext {
+            temp_c: -12.4,
+            max_temp_c: 85.0,
+            min_temp_c: -40.0,
+            vccint_v: 0.950,
+            max_vccint_v: 1.050,
+            min_vccint_v: 0.950,
+            vccaux_v: 1.800,
+            max_vccaux_v: 1.890,
+            min_vccaux_v: 1.710,
+            raw: None,
+        };
+        let pvt = ctx.to_pvt_context(ProcessCorner::Tt).unwrap();
+        assert_eq!(pvt.temp_c, -12);
+        assert_eq!(pvt.vccint_mv, 950);
+        assert_eq!(pvt.process_corner, ProcessCorner::Tt);
+    }
 }