Skip to content

Wave Loop 374 — IGLA CODER+RACE + retry board flash + one safe gen-verilog sub-fix #4792

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
gHashTag merged 2 commits into from
Sep 24, 2026
Merged

Wave Loop 374 — IGLA CODER+RACE + retry board flash + one safe gen-verilog sub-fix #4792

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
dfd28e6
salvage(queen-1263): commit what the turn left uncommitted
Sep 24, 2026
5a040a8
docs: the coordination entry this branch needs to land
claude Sep 24, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions ...09-24-published-wave-loop-374-igla-coder-race-retry-board-flash-one-safe-gen.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
22 changes: 11 additions & 11 deletions proofs/lean4/Trinity/TernaryInference.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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) =
Expand Down
Loading