proofs
Provedbaguettealphamemory-placementrtx3070

Baguette's 512 MiB logit gradient fits the gradient bank's blocks 0..37 slice

4(65536⋅576) mod 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⋅2\begin{aligned} & \htmlData{mx=3}{\htmlData{mx=2}{4(\htmlData{mx=1}{65536 \cdot 576})} \bmod 2097152} \mathrel{\htmlData{mx=4}{=}} 0 \\ & \htmlData{mx=0}{\land} \htmlData{mx=10}{\htmlData{mx=7}{4(\htmlData{mx=6}{65536 \cdot 576})} + \htmlData{mx=9}{\htmlData{mx=8}{4096 \cdot 65536} \cdot 2}} \\ & \quad \htmlData{mx=5}{\leq} \htmlData{mx=22}{4(\htmlData{mx=21}{\htmlData{mx=11}{65536 \cdot 576} + \htmlData{mx=20}{38(\htmlData{mx=19}{\htmlData{mx=17}{\htmlData{mx=14}{\htmlData{mx=12}{576 \cdot 960} + \htmlData{mx=13}{576 \cdot 576}} + \htmlData{mx=16}{\htmlData{mx=15}{3 \cdot 576} \cdot 1536}} + \htmlData{mx=18}{2 \cdot 576}})}})} \\ & \htmlData{mx=0}{\land} \htmlData{mx=35}{4(\htmlData{mx=34}{\htmlData{mx=24}{65536 \cdot 576} + \htmlData{mx=33}{37(\htmlData{mx=32}{\htmlData{mx=30}{\htmlData{mx=27}{\htmlData{mx=25}{576 \cdot 960} + \htmlData{mx=26}{576 \cdot 576}} + \htmlData{mx=29}{\htmlData{mx=28}{3 \cdot 576} \cdot 1536}} + \htmlData{mx=31}{2 \cdot 576}})}})} \\ & \quad \htmlData{mx=23}{<} \htmlData{mx=40}{\htmlData{mx=37}{4(\htmlData{mx=36}{65536 \cdot 576})} + \htmlData{mx=39}{\htmlData{mx=38}{4096 \cdot 65536} \cdot 2}} \end{aligned}
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…)

Arena 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.

More proved statements