Provedbaguettealphamemory-placementrtx3070
Baguette's 512 MiB logit gradient fits the gradient bank's blocks 0..37 slice
What the notation means · or point at any symbol
- modRemainder
- The remainder when 4 · (65536 · 576) is divided by 2097152. (
(4 * (65536 * 576)) % 2097152) - =Equality
- 4 · (65536 · 576) % 2097152 and 0 are the same. (
(4 * (65536 * 576)) % 2097152 = 0) - ·Multiplication
- 65536 times 576. (
65536 * 576) - +Addition
- 4 · (65536 · 576) plus 4096 · 65536 · 2. (
4 * (65536 * 576) + 4096 * 65536 * 2) - ≤At most
- 4 · (65536 · 576) + 4096 · 65536 · 2 is less than or equal to 4 · (65536 · 576 + 38 · (576 · 960 + 576 · 576 + 3 · 576 ·…. (
4 * (65536 * 576) + 4096 * 65536 * 2 ≤ …) - ∧And
- Both hold: 4 · (65536 · 576) + 4096 · 65536 · 2 ≤ 4 · (65536 · 576 + …, and 4 · (65536 · 576 + 37 · (576 · 960 + 576 · 576 + 3 · 576 ·…. (
4 * (65536 * 576) + 4096 * 65536 * 2 ≤ …) - <Less than
- 4 · (65536 · 576 + 37 · (576 · 960 + 576 · 576 + 3 · 576 ·… is strictly smaller than 4 · (65536 · 576) + 4096 · 65536 · 2. (
4 * (65536 * 576 + 37 * (576 * 960 + 57…)
theorem baguette-logit-gradient-fits-gradient-slice :
(4 * (65536 * 576)) % 2097152 = 0 ∧ 4 * (65536 * 576) + 4096 * 65536 * 2 ≤ 4 * (65536 * 576 + 38 * (576 * 960 + 576 * 576 + 3 * 576 * 1536 + 2 * 576)) ∧ 4 * (65536 * 576 + 37 * (576 * 960 + 576 * 576 + 3 * 576 * 1536 + 2 * 576)) < 4 * (65536 * 576) + 4096 * 65536 * 2Arena reduction for the RTX 3070 (Alpha commit 065122bd): the bfloat16 logit gradient (4096 x 65536 x 2 bytes = 2^29) is placed inside the binary32 gradient bank's slice for decoder blocks 0..37, which the backward (blocks 79 down to 0) writes only after the logit gradient's last reader. Geometry: vocabulary 65536, width 576, QKV width 960, feed 1536; a block holds 576960 + 576576 + 35761536 + 2576 = 3,540,096 binary32 gradients after the 65536576 embedding gradients. The statement checks the slice start is 2 MiB aligned, that 38 blocks hold the plane, and that 37 do not (so 38 is the least slice).
How it was proved
- Proved
- 4 October 2026
- By
- Ajax
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- Classical.choice, Quot.sound, propext
- Proof
- 6 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.