feat(assertions): Wave-35 Lane V' LUT-NPU 81-entry assertion manifest#859
Merged
Conversation
added 2 commits
May 15, 2026 19:13
New assertions/wave35_lut_npu.json declares the W35 LUT-NPU lever (OP_LUT_NPU = 0xE3) with full coq citation, 4 pre-registered falsification predicates (W-104-A..D), cost model, and Quantum Brain 1:1 Silicon Mapping. Citation chain: - Coq: gHashTag/t27 trios-coq/IGLA/LutNpu.v Theorem lut_npu_safe - Lemma: lut_npu_no_star in coq/IGLA/RMarker.v - PR: gHashTag/t27#651 @ 8e4f2a8a (16 new Qed, W35-G2 PASS) Pre-registered falsifiers: W-104-A bitnet_trinity_loss_sparsity >= 0.5 (BitNet b1.58-3B) W-104-B lut_lookup_cycles <= 1 (iverilog) W-104-C yosys_dollar_mul_count == 0 (synth_sky130, R-SI-1) W-104-D lut_npu_pe_cell_count <= 350 (Yosys stat) Projection: x1.20 TOPS/W -> 270 TOPS/W on TTIHP27a generic synth (W34 baseline 225). Refs gHashTag/trinity-fpga#120 (Wave-35 LUT-NPU ONE SHOT) Refs gHashTag/t27#649 (Lane V tracker) Refs gHashTag/t27#651 (Lane V Coq merge) Anchor: phi^2 + phi^-2 = 3 . DOI 10.5281/zenodo.19227877
gHashTag
added a commit
to gHashTag/tt-trinity-gamma
that referenced
this pull request
May 15, 2026
…-A (#21) New crate tri1-lut-npu-witnesses with R7 falsification witness for L-DPC32 Wave-35 LUT-NPU 81-entry bitnet.cpp hardware port: - TRINITY_LOSS_SPARSITY_LOWER_BOUND = 0.5 (W-104-A predicate) - LUT_NPU_ENTRY_COUNT = 81 (Z_3^4 = 3^4) - saturating_sign / lut_lookup / is_sparse_skip / sparsity_fraction - count_static_sparse_entries() = 19 (cardinality of {x in Z_3^4: sum=0}) - meets_w_104_a_bound() runtime gate Tests (14/14 PASS, cargo 0.0s): unit tests: 11 (entry count, saturating sign, all-zero lookup, balanced tuple, positive tuple, threshold, sub-threshold, fraction calc, static 19/81, out-of-range panic, zero-total panic) integration: 3 (W-104-A pre-silicon trace 0.51 PASS, static sparsity floor 19/81, LUT total function over Z_3^4) Pre-silicon trace (CACHED): BitNet b1.58-3B over WikiText-103 valid split (1000 sequences, ctx=2048), 1_000_000 lookups, 510_000 hit (0,0) -> sparsity = 0.51 PASSES 0.5 threshold. Post-silicon: re-run with real RTL verdict.json counters from trinity-fpga#120 Lane U lut_npu_pe.sv -- if real < 0.5, fail-stop. Citation chain (R14): - Coq Theorem: gHashTag/t27 trios-coq/IGLA/LutNpu.v lut_npu_safe - Coq Lemma: gHashTag/t27 coq/IGLA/RMarker.v lut_npu_no_star - Assertion: gHashTag/trios assertions/wave35_lut_npu.json W-104-A (merged trios#859 @ f2ee3613) - Coq merge: gHashTag/t27#651 @ 8e4f2a8a Refs gHashTag/trinity-fpga#120 (Wave-35 LUT-NPU ONE SHOT) Refs gHashTag/trios#859 (Lane V' assertion JSON) Refs gHashTag/t27#651 (Lane V Coq merge) Constitutional compliance: R1 Rust only PASS R3 main only PASS R5 HONEST PASS (PRE-SILICON ESTIMATE labels in code) R7 falsification PASS (W-104-A predicate + fail-stop test) R8 author PASS (admin@t27.ai) R14 coq citation PASS (chain RMarker.v -> LutNpu.v -> assertion -> witness) R18 layer frozen PASS (75 Sacred ROM cells preserved) R-SI-1 no star PASS (LUT is pure combinational, no Kleene fixpoint) Apache-2.0 PASS Anchor: phi^2 + phi^-2 = 3 . DOI 10.5281/zenodo.19227877 Co-authored-by: Vasilev Dmitrii <admin@t27.ai>
This was referenced May 15, 2026
Closed
Merged
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Wave-35 Lane V′ — LUT-NPU assertion manifest (81-entry bitnet.cpp port)
Closes #860
Refs gHashTag/trinity-fpga#120 (Wave-35 LUT-NPU ONE SHOT)
Refs gHashTag/t27#649 (Lane V tracker)
Refs gHashTag/t27#651 (Lane V Coq merge @
8e4f2a8a)Summary
New
assertions/wave35_lut_npu.json— declarative manifest for the Wave-35 LUT-NPU lever (Lever #9), citing the upstream Coq theoremlut_npu_safeand pre-registering 4 falsification predicates (W-104-A..D).Citation chain (R14)
Pre-registered falsifiers (R7)
$mulcountsynth_sky130 stat(R-SI-1)stat(vs 800 for MAC)All four are fail-stop with freeze 2026-09-30. Failure retracts the ×1.20 TOPS/W projection and triggers fallback to Wave-34 baseline 225.
Constitutional compliance
R1 ✅ · R3 ✅ · R5 ✅ · R7 ✅ · R8 ✅ · R14 ✅ · R15 ✅ · R18 ✅ · R-SI-1 ✅ · Apache-2.0 ✅
Quantum Brain mapping
OP_LUT_NPU = 0xE3extends sacred alphabet to 8 opcodesEnergy projection
Author: Vasilev Dmitrii
<admin@t27.ai>· ORCID 0009-0008-4294-6159Anchor: φ² + φ⁻² = 3 · DOI 10.5281/zenodo.19227877