/-- **A 1-D stencil**, at every size and window: `out[i] := Σ_{k<w} inp[i+k]`.
The obligation is discharged once, for all `n` and `w`, from one range inequality. -/
theorem stencil_ok (n w inp out : Nat) (h : inp + n + w ≤ out) :
wfB (stencilK n w inp out (fun _ => .lit 1)) = true :=
wfB_stencilK n w inp out _ (fun i j _ hj k hk => n:Natw:Natinp:Natout:Nath:inp + n + w ≤ outi:Natj:Natx✝:i < nhj:j < nk:Nathk:k < w⊢ out + i ≠ inp + j + k All goals completed! 🐙)
/-- **A dense layer**: `out[i] := Σ_j W[i,j] * x[j] + b[i]`. Every thread reads *all* of `x`,
which is exactly the shared-read pattern separating conjunction rejects. -/
theorem dense_ok (rows cols wgt xs bias out : Nat)
(h1 : wgt + rows * cols ≤ xs) (h2 : xs + cols ≤ bias) (h3 : bias + rows ≤ out) :
wfB (denseK rows cols wgt xs bias out) = true := rows:Natcols:Natwgt:Natxs:Natbias:Natout:Nath1:wgt + rows * cols ≤ xsh2:xs + cols ≤ biash3:bias + rows ≤ out⊢ (denseK rows cols wgt xs bias out).wfB = true
refine wfB_denseK rows cols wgt xs bias out (fun i j hi hj k hk => ⟨?_, ?_⟩)
(fun i j hi hj => rows:Natcols:Natwgt:Natxs:Natbias:Natout:Nath1:wgt + rows * cols ≤ xsh2:xs + cols ≤ biash3:bias + rows ≤ outi:Natj:Nathi:i < rowshj:j < rows⊢ out + i ≠ bias + j All goals completed! 🐙)
rows:Natcols:Natwgt:Natxs:Natbias:Natout:Nath1:wgt + rows * cols ≤ xsh2:xs + cols ≤ biash3:bias + rows ≤ outi:Natj:Nathi:i < rowshj:j < rowsk:Nathk:k < cols⊢ out + i ≠ wgt + j * cols + k rows:Natcols:Natwgt:Natxs:Natbias:Natout:Nath1:wgt + rows * cols ≤ xsh2:xs + cols ≤ biash3:bias + rows ≤ outi:Natj:Nathi:i < rowshj:j < rowsk:Nathk:k < colsthis:j * cols + k < rows * cols⊢ out + i ≠ wgt + j * cols + k
All goals completed! 🐙
rows:Natcols:Natwgt:Natxs:Natbias:Natout:Nath1:wgt + rows * cols ≤ xsh2:xs + cols ≤ biash3:bias + rows ≤ outi:Natj:Nathi:i < rowshj:j < rowsk:Nathk:k < cols⊢ out + i ≠ xs + k All goals completed! 🐙
/-- **Bias add**: `out[i,j] := inp[i,j] + bias[j]`. Every row reads the same bias vector. -/
theorem biasAdd_ok (rows cols inp bias out : Nat)
(h1 : inp + rows * cols ≤ bias) (h2 : bias + cols ≤ out) :
wfB (biasAddK rows cols inp bias out) = true := rows:Natcols:Natinp:Natbias:Natout:Nath1:inp + rows * cols ≤ biash2:bias + cols ≤ out⊢ (biasAddK rows cols inp bias out).wfB = true
rows:Natcols:Natinp:Natbias:Natout:Nath1:inp + rows * cols ≤ biash2:bias + cols ≤ outi:Natj:Nati':Natj':Natx✝¹:i < rowshj:j < colsx✝:i' < rowshj':j' < colshne:i ≠ i' ∨ j ≠ j'⊢ out + i * cols + j ≠ out + i' * cols + j'rows:Natcols:Natinp:Natbias:Natout:Nath1:inp + rows * cols ≤ biash2:bias + cols ≤ outi:Natj:Nati':Natj':Nathi:i < rowshj:j < colshi':i' < rowshj':j' < cols⊢ out + i * cols + j ≠ inp + i' * cols + j'rows:Natcols:Natinp:Natbias:Natout:Nath1:inp + rows * cols ≤ biash2:bias + cols ≤ outi:Natj:Nati':Natj':Nathi:i < rowshj:j < colshi':i' < rowshj':j' < cols⊢ out + i * cols + j ≠ bias + j'
rows:Natcols:Natinp:Natbias:Natout:Nath1:inp + rows * cols ≤ biash2:bias + cols ≤ outi:Natj:Nati':Natj':Natx✝¹:i < rowshj:j < colsx✝:i' < rowshj':j' < colshne:i ≠ i' ∨ j ≠ j'⊢ out + i * cols + j ≠ out + i' * cols + j' rows:Natcols:Natinp:Natbias:Natout:Nath1:inp + rows * cols ≤ biash2:bias + cols ≤ outi:Natj:Nati':Natj':Natx✝¹:i < rowshj:j < colsx✝:i' < rowshj':j' < colshne:i ≠ i' ∨ j ≠ j'⊢ out + (i * cols + j) ≠ out + (i' * cols + j')
All goals completed! 🐙
rows:Natcols:Natinp:Natbias:Natout:Nath1:inp + rows * cols ≤ biash2:bias + cols ≤ outi:Natj:Nati':Natj':Nathi:i < rowshj:j < colshi':i' < rowshj':j' < cols⊢ out + i * cols + j ≠ inp + i' * cols + j' rows:Natcols:Natinp:Natbias:Natout:Nath1:inp + rows * cols ≤ biash2:bias + cols ≤ outi:Natj:Nati':Natj':Nathi:i < rowshj:j < colshi':i' < rowshj':j' < colsthis:i * cols + j < rows * cols⊢ out + i * cols + j ≠ inp + i' * cols + j'
rows:Natcols:Natinp:Natbias:Natout:Nath1:inp + rows * cols ≤ biash2:bias + cols ≤ outi:Natj:Nati':Natj':Nathi:i < rowshj:j < colshi':i' < rowshj':j' < colsthis✝:i * cols + j < rows * colsthis:i' * cols + j' < rows * cols⊢ out + i * cols + j ≠ inp + i' * cols + j'
All goals completed! 🐙
rows:Natcols:Natinp:Natbias:Natout:Nath1:inp + rows * cols ≤ biash2:bias + cols ≤ outi:Natj:Nati':Natj':Nathi:i < rowshj:j < colshi':i' < rowshj':j' < cols⊢ out + i * cols + j ≠ bias + j' rows:Natcols:Natinp:Natbias:Natout:Nath1:inp + rows * cols ≤ biash2:bias + cols ≤ outi:Natj:Nati':Natj':Nathi:i < rowshj:j < colshi':i' < rowshj':j' < colsthis:i * cols + j < rows * cols⊢ out + i * cols + j ≠ bias + j'
All goals completed! 🐙