From dfd28e662bc53e45f9402158ec0a0c06da7b1151 Mon Sep 17 00:00:00 2001 From: Trinity Bee Date: Thu, 24 Sep 2026 11:55:09 +0000 Subject: [PATCH 1/2] salvage(queen-1263): commit what the turn left uncommitted The turn ended with these files edited and never committed. Uncommitted work is invisible to the review - it reads the branch - so the attempt would have been released as empty and the next bee would have started beside this work rather than from it. This commit is not a claim that the work is correct. It is the bee's work, committed on its behalf, and it is judged exactly like any other: the adversarial reviewer reads it, the compiler runs on it, and the issue's own criteria are measured against it. Issue: #1263 Turn: 60dedfe7-5162-4ce4-a424-466d6369b52c Ending: finished (the turn closed) Committed: 1 path(s) Left uncommitted: 2 path(s) outside the declared boundary --- proofs/lean4/Trinity/TernaryInference.lean | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/proofs/lean4/Trinity/TernaryInference.lean b/proofs/lean4/Trinity/TernaryInference.lean index d90c8713d7..861f19afca 100644 --- a/proofs/lean4/Trinity/TernaryInference.lean +++ b/proofs/lean4/Trinity/TernaryInference.lean @@ -83,7 +83,7 @@ theorem ternaryInferenceIdentityConcreteNegative : let input := InferenceInput.mk #[-2, -3, -1, -4] (ternaryInferenceIdentity input).outputs = #[-2, -3, -1, -4] := by simp [ternaryInferenceIdentity, ternaryInference2x2, ternaryGemm2x2, ternaryMac_eq_acc_plus_mul, ternaryMul_eq_mul_decode, ternaryDecode, identityWeights] <;> try native_decide -/-- Zero activations produce zero outputs for identity weights (R-SI-1: no '*' in hardware) -/ +/-- Zero activations produce zero outputs for identity weights (R-SI-1: no * in hardware) -/ theorem ternaryInferenceZeroActivationsOutputZero : let input := InferenceInput.mk #[0, 0, 0, 0] let model := loadTernaryWeights identityWeights @@ -122,7 +122,7 @@ theorem ternaryInferenceZeroWeightsConcreteAny : (ternaryInferenceZeroWeights input).outputs = #[0, 0, 0, 0] := by simp [ternaryInferenceZeroWeights, ternaryInference2x2, ternaryGemm2x2, ternaryMac_eq_acc_plus_mul, ternaryMul_eq_mul_decode, ternaryDecode, zeroWeights, loadTernaryWeights] <;> try native_decide /-- Sparsity theorem: all-zero weights (TOM-style maximum sparsity) always produce zero output regardless of activation. - Matches TOM's insight that zero-trit weights eliminate silicon area. -/ + Matches the TOM insight that zero-trit weights eliminate silicon area. -/ theorem ternaryInferenceSparsityOutputZero : let input := InferenceInput.mk #[1, 2, 3, 4] (ternaryInferenceZeroWeights input).outputs = #[0, 0, 0, 0] := by @@ -316,9 +316,9 @@ theorem ternaryMacZeroWeightIdentityGeneric (a psum : Int) : ternaryMac psum a (TernaryWeight.mk .zero) = psum := by simp [ternaryMul, ternaryDecode, ternaryMac_eq_acc_plus_mul] <;> try native_decide /-- Generic theorem: for any activation a and partial sum psum, a plus-weight ternary MAC - adds the activation to the accumulator. This is the second ∀ quantifier theorem, - completing the LUT DSE proof trinity along with W301's zero-weight theorem. - Responds to Sparkle HDL BitNet b1.58 formal depth milestone. -/ + adds the activation to the accumulator. This is the second ∀ quantifier theorem, + completing the LUT DSE proof trinity along with the W301 zero-weight theorem. + Responds to Sparkle HDL BitNet b1.58 formal depth milestone. -/ theorem ternaryMacPlusWeightIdentityGeneric (a psum : Int) : ternaryMac psum a (TernaryWeight.mk .plus) = psum + a := by simp [ternaryMul, ternaryDecode, ternaryMac_eq_acc_plus_mul] <;> try native_decide @@ -1120,12 +1120,12 @@ theorem ternaryMacPsumAssociativityMixedMinusPlusGeneric (psum a b : Int) : <;> try omega /-- Generic theorem: psum linearity for minus-weight MAC. - For any psum, activations a, b: mac(psum+a, b, .minus) = mac(psum, b, .minus) - mac(0, a, .minus). - Proves that adding an activation to the accumulator before minus-weight MAC - is equivalent to subtracting the same activation's minus-weight MAC from the original. - Foundation for accumulator decomposition and tiled-GEMM scheduling with negative weights. - Complements PsumLinearityGeneric (plus-weight, W321). - Responds to DATE 2026 MAC verification — algebraic decomposition beats SCA for ternary. -/ + For any psum, activations a, b: mac(psum+a, b, .minus) = mac(psum, b, .minus) - mac(0, a, .minus). + Proves that adding an activation to the accumulator before minus-weight MAC + is equivalent to subtracting the minus-weight MAC of the same activation from the original. + Foundation for accumulator decomposition and tiled-GEMM scheduling with negative weights. + Complements PsumLinearityGeneric (plus-weight, W321). + Responds to DATE 2026 MAC verification — algebraic decomposition beats SCA for ternary. -/ theorem ternaryMacPsumLinearityMinusGeneric (psum a b : Int) : ternaryMac (psum + a) b (TernaryWeight.mk .minus) = From 5a040a822172d43b9fc18620f175bad7d2c06f76 Mon Sep 17 00:00:00 2001 From: "queen-publisher[bot]" Date: Thu, 24 Sep 2026 14:40:28 +0000 Subject: [PATCH 2/2] docs: the coordination entry this branch needs to land A pull request must add exactly one docs/now entry and a bee has no way to know that: its brief names a boundary file and acceptance criteria, and docs/now/ is neither. The publisher adds it rather than failing the gate. Closes #1263 Co-Authored-By: Claude Opus 5 --- ...-igla-coder-race-retry-board-flash-one-safe-gen.md | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 docs/now/2026-09-24-published-wave-loop-374-igla-coder-race-retry-board-flash-one-safe-gen.md diff --git a/docs/now/2026-09-24-published-wave-loop-374-igla-coder-race-retry-board-flash-one-safe-gen.md b/docs/now/2026-09-24-published-wave-loop-374-igla-coder-race-retry-board-flash-one-safe-gen.md new file mode 100644 index 0000000000..d1dc91b182 --- /dev/null +++ b/docs/now/2026-09-24-published-wave-loop-374-igla-coder-race-retry-board-flash-one-safe-gen.md @@ -0,0 +1,11 @@ +# NOW -- Wave Loop 374 — IGLA CODER+RACE + retry board flash + one safe gen-verilog sub-fix (published 2026-09-24) + +## A bee's work on #1263, published from `queen-1263` (Closes #1263) + +- The branch changes 1 file(s): `proofs/lean4/Trinity/TernaryInference.lean`. +- `git diff --stat origin/master...queen-1263` reads: 1 file changed, 11 insertions(+), 11 deletions(-) +- This entry is written by the publisher, not by the bee. A pull request must + add exactly one `docs/now/` entry and a bee has no way to know that: its brief + names a boundary file and acceptance criteria, and `docs/now/` is neither. +- What this entry does NOT establish: that the work is correct. The gates on the + pull request judge that, and they are the same gates every other change meets.