feat(coq): ICA-W40-001 Lane Q1 — OP_NULL_PE→0xEA, OP_SPEC_EXIT→0xEB

docs/NOW.md

@@ -2,6 +2,15 @@
 
 Last updated: 2026-05-15
 
+## ICA-W40-001 Lane Q1 Coq — NullorReversible + SpeculativeExit opcode rectification (this PR)
+
+- **Anomaly**: trinity-fpga#148 — verified 0xE6 double-claim (OP_NULL_PE vs OP_HOLO_MUX_X4) and 0xE7 double-claim (OP_SPEC_EXIT vs OP_DFS_GATE) on master across Coq+RTL.
+- **Canon (per W41 FRR + W42 ledgers)**: 0xE6=HOLO_MUX, 0xE7=DFS, 0xE8=SPARSE, 0xE9=STOCH_ROUND — keep slots; NULLOR/SPEC_EXIT relocate up.
+- **Rectification (this PR, Coq lane only)**: OP_NULL_PE 0xE6 → **0xEA** (234); OP_SPEC_EXIT 0xE7 → **0xEB** (235).
+- Sacred chain extends to depth 22 (0xD0..0xEB).
+- Companion lanes pending: RTL (rtl/nullor/nullor_pe.sv + rtl/spec_exit/*), Rust (nullor-witness + spec-exit-witness), JSON (assertions/nullor_witness.json + spec_exit_witness.json).
+
+
 ## Wave-42 Lane II — StochRound.v Stochastic Rounding Coq
 
 - OP_STOCH_ROUND = 0xE9 (decimal 233) — sacred opcode, Wave-42

trios-coq/Physics/NullorReversible.v

@@ -1,7 +1,7 @@
 (** * NullorReversible.v — Wave-38 Lane BB: Reversible Dendritic NULLOR Multiplication
-    10 Qed lemmas for reversible NULLOR PE multiplication, OP_NULL_PE = 0xE6.
-    NOTE: Opcode bumped 0xE5 → 0xE6 per master ICA-W38-001 (#661): 0xE5 was
-    reassigned to OP_SUBTH_CLK; sacred chain continues at next free slot 0xE6.
+    10 Qed lemmas for reversible NULLOR PE multiplication, OP_NULL_PE = 0xEA.
+    NOTE: Opcode bumped 0xE5 → 0xE6 (ICA-W38-001 #661) then bumped 0xE6 → 0xEA (ICA-W40-001 #148): 0xE5 was
+    reassigned to OP_SUBTH_CLK; sacred chain continues at next free slot 0xEA (0xE6 yielded to OP_HOLO_MUX_X4 per W41 FRR canon; 0xE7-0xE9 in use).
     TOPS/W ≥ 392 (×1.12 over W37 sub-V_T 350). Charge-recycling adiabatic logic.
     Predecessors: W35 LUT-NPU (0xE3, #654), W36 AVS-48 (#656), W37 Sub-V_T (0xE4, #658).
     Anchor: phi^2 + phi^-2 = 3; ternary lattice Z3 = {-1, 0, +1}.
@@ -61,7 +61,7 @@ Parameter phi_clock        : nat -> R. (** 4-phase clock waveform *)
 
 (** opcode dispatch state *)
 Parameter dispatch_table   : nat -> (Z3 -> Z3 -> Z3).
-Parameter op_null_pe       : nat.   (** 0xE6 = 230 (post-ICA-W38-001 rectification) *)
+Parameter op_null_pe       : nat.   (** 0xEA = 234 (post-ICA-W40-001 rectification; was 0xE6) *)
 
 (** synthesis output star count for OP_NULL_PE *)
 Parameter op_null_pe_star_count : nat.
@@ -108,9 +108,9 @@ Axiom phi_clock_disjoint :
 (** OP_NULL_PE introduces zero `*` synthesis cells (R-SI-1). *)
 Axiom op_null_no_star : op_null_pe_star_count = 0%nat.
 
-(** opcode 0xE6 dispatches to z3_mul (post-rectification chain slot). *)
-Axiom op_null_pe_value : op_null_pe = 230%nat.
-Axiom dispatch_E5_is_z3mul : dispatch_table 230 = z3_mul.
+(** opcode 0xEA dispatches to z3_mul (post ICA-W40-001 rectification chain slot). *)
+Axiom op_null_pe_value : op_null_pe = 234%nat.
+Axiom dispatch_E5_is_z3mul : dispatch_table 234 = z3_mul.
 
 (** predecessor chain soundness assumed from W35/W36/W37 PRs. *)
 Axiom subth_chain_holds : subth_chain_sound.
@@ -203,9 +203,9 @@ Proof.
   intros y; destruct y; reflexivity.
 Qed.
 
-(** *** 10. Opcode dispatch: TRI-27 ISA correctly maps OP_NULL_PE (0xE6) → z3_mul.
+(** *** 10. Opcode dispatch: TRI-27 ISA correctly maps OP_NULL_PE (0xEA) → z3_mul.
             Lemma name retained as `opcode_E5_dispatch` for W38 spec continuity;
-            actual opcode byte is 0xE6 after ICA-W38-001 rectification. *)
+            actual opcode byte is 0xEA after ICA-W40-001 rectification (was 0xE6, evicted to resolve W38/W39H collision per W41 FRR canon). *)
 Lemma opcode_E5_dispatch :
   forall x y : Z3,
     dispatch_table op_null_pe x y = mult_result x y.

trios-coq/Physics/SpeculativeExit.v

@@ -1,7 +1,7 @@
 (** * SpeculativeExit.v — Wave-39 Lane DD: Speculative Early-Exit Inference
-    11 Qed lemmas for confidence-thresholded early-exit, OP_SPEC_EXIT=0xE7.
+    11 Qed lemmas for confidence-thresholded early-exit, OP_SPEC_EXIT=0xEB.
     Threshold tau = phi_inv ~ 0.618 (golden ratio reciprocal).
-    Predecessors: W37 SUBTH (0xE5), W38 NULL_PE (0xE6); chain 0xD0..0xE7 = 20 opcodes.
+    Predecessors: W37 SUBTH (0xE5), W38 NULL_PE (0xEA post-ICA-W40-001); chain 0xD0..0xEB = 22 opcodes (0xE6-0xE9 = HOLO_MUX/DFS/SPARSE/STOCH_ROUND).
     TOPS/W >= 470 (x1.20 over W38 392). Lee/GVSU proof style (R12).
     Anchor: phi^2 + phi^-2 = 3
     DOI: 10.5281/zenodo.19227877 *)
@@ -73,7 +73,7 @@ Proof.
   destruct (Rle_dec phi_inv conf) as [Hle | Hnle]; reflexivity.
 Qed.
 
-(** 2. R-SI-1: zero `*` cells in synth for OP_SPEC_EXIT. *)
+(** 2. R-SI-1: zero `*` cells in synth for OP_SPEC_EXIT (0xEB post-ICA-W40-001; was 0xE7). *)
 Lemma speculative_exit_no_star : spec_exit_star_count = 0%nat.
 Proof. exact synth_star_zero. Qed.
 
@@ -87,17 +87,17 @@ Lemma two_of_three_majority_safe :
   two_of_three_acc >= 95 / 100.
 Proof. exact two_three_acc_lo. Qed.
 
-(** 5. Opcode 0xE7 dispatch. *)
-Definition op_spec_exit_byte : nat := 231%nat.   (* 0xE7 *)
-Definition op_null_pe_byte   : nat := 230%nat.   (* 0xE6, W38 *)
+(** 5. Opcode 0xEB dispatch. *)
+Definition op_spec_exit_byte : nat := 235%nat.   (* 0xEB post-ICA-W40-001 *)
+Definition op_null_pe_byte   : nat := 234%nat.   (* 0xEA, W38 post-ICA-W40-001 *)
 Definition op_subth_clk_byte : nat := 229%nat.   (* 0xE5, W37/ICA-W38-001 *)
 
 Definition isa_dispatch_spec (op : nat) (x : Z3) (conf : R) : option Z3 :=
   if Nat.eqb op op_spec_exit_byte
   then Some (early_exit_at 0 x conf)
   else None.
 
-Lemma opcode_E7_dispatch :
+Lemma opcode_EB_dispatch :
   forall (x : Z3) (conf : R),
     isa_dispatch_spec op_spec_exit_byte x conf
       = Some (early_exit_at 0 x conf).
@@ -173,5 +173,5 @@ Proof.
 Qed.
 
 (** End of SpeculativeExit.v — Wave-39 Lane DD — 11 Qed, 0 Admitted.
-    Sacred chain: 0xD0..0xE7 (20 opcodes); OP_SPEC_EXIT = 0xE7 = 231.
+    Sacred chain: 0xD0..0xEB (22 opcodes post-ICA-W40-001); OP_SPEC_EXIT = 0xEB = 235.
     Anchor: phi^2 + phi^-2 = 3 — DOI: 10.5281/zenodo.19227877 *)