Skip to content

spec(maxpool2d_layer): a lowerable out_side(kernel, stride) for the nn-maxpool widget (Closes #10664) #10665

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 1 commit into from
Oct 18, 2026
Merged

spec(maxpool2d_layer): a lowerable out_side(kernel, stride) for the nn-maxpool widget (Closes #10664) #10665

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
16 changes: 8 additions & 8 deletions .trinity/seals/Maxpool2d.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,19 +1,19 @@
{
"gen_hash_c": "sha256:bb0efd8ee8b00c56e51782abd9347cf5da092380c69bf2857442cc09506fba6f",
"gen_hash_rust": "sha256:0a837e60765cad86302184dcd07084c7b60fc8ea496840962f19029d938f1cf8",
"gen_hash_verilog": "sha256:50407bfd895365b8c5377e6f3148a4098b5a976f47afab0e7a5b0f1e0c9c8500",
"gen_hash_zig": "sha256:27d2cb541c227f40c4eba94663d758c38c13259d430d75f861d096f49a33fbbc",
"gen_hash_c": "sha256:6e708ec93f81a12af61c9753d1a4186ecb8b7fb3078e120ce3df26b5872bca9c",
"gen_hash_rust": "sha256:7e107b2c4bbce9d33ad1588e4b934828a4b23c86dad0325d35351928d181f019",
"gen_hash_verilog": "sha256:b1581e22f6ad1d843a39a6696c212acd8ca1c13675e84f72816059f3bc817261",
"gen_hash_zig": "sha256:4857e2adccd62add1dd719ce5020e5e9862379ccd399a9fcc32c0923a381cb64",
"module": "Maxpool2d",
"ring": 12,
"sealed_at": "2026-10-11T10:43:19Z",
"spec_hash": "sha256:70e420bb07469fa920c9fabeaaa29116ee913b5b203951594cfb7ef20730db46",
"sealed_at": "2026-10-18T21:27:49Z",
"spec_hash": "sha256:12627dff26da63deb67347730d28228fda9b60ca09779e37d052f4a94f3e7e0a",
"spec_path": "specs/ml/layers/maxpool2d_layer.t27",
"tests": {
"failed": 0,
"failing": [],
"forced": false,
"passed": 5,
"total": 5,
"passed": 7,
"total": 7,
"vacuous": 0
}
}
20 changes: 10 additions & 10 deletions .trinity/seals/layers_Maxpool2d.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
{
"built_by": "t27c-bootstrap@0.5.2+cc19d1fcd",
"built_by": "t27c-bootstrap@0.5.2+239b4b059",
"closure": [
{
"spec": "specs/base/types.t27",
Expand All @@ -11,27 +11,27 @@
}
],
"config": "gen=c,rust,verilog,zig;tests=zig",
"gen_hash_c": "sha256:bb0efd8ee8b00c56e51782abd9347cf5da092380c69bf2857442cc09506fba6f",
"gen_hash_rust": "sha256:0a837e60765cad86302184dcd07084c7b60fc8ea496840962f19029d938f1cf8",
"gen_hash_verilog": "sha256:50407bfd895365b8c5377e6f3148a4098b5a976f47afab0e7a5b0f1e0c9c8500",
"gen_hash_zig": "sha256:27d2cb541c227f40c4eba94663d758c38c13259d430d75f861d096f49a33fbbc",
"gen_hash_c": "sha256:6e708ec93f81a12af61c9753d1a4186ecb8b7fb3078e120ce3df26b5872bca9c",
"gen_hash_rust": "sha256:7e107b2c4bbce9d33ad1588e4b934828a4b23c86dad0325d35351928d181f019",
"gen_hash_verilog": "sha256:b1581e22f6ad1d843a39a6696c212acd8ca1c13675e84f72816059f3bc817261",
"gen_hash_zig": "sha256:4857e2adccd62add1dd719ce5020e5e9862379ccd399a9fcc32c0923a381cb64",
"module": "Maxpool2d",
"ring": 12,
"seal_schema": 2,
"sealed_at": "2026-10-11T10:43:19Z",
"sealed_at": "2026-10-18T21:27:49Z",
"sealed_by": "t27c-bootstrap@0.5.2",
"spec_hash": "sha256:70e420bb07469fa920c9fabeaaa29116ee913b5b203951594cfb7ef20730db46",
"spec_hash": "sha256:12627dff26da63deb67347730d28228fda9b60ca09779e37d052f4a94f3e7e0a",
"spec_path": "specs/ml/layers/maxpool2d_layer.t27",
"tests": {
"failed": 0,
"failing": [],
"forced": false,
"passed": 5,
"total": 5,
"passed": 7,
"total": 7,
"vacuous": 0
},
"toolchain": {
"test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d",
"test_runner": "sha256:8512b80da533b79289110fca4a65f3336abd7a059ca4b72ea595d5e33ff8ad10",
"zig": "0.16.0"
}
}
11 changes: 11 additions & 0 deletions docs/now/2026-10-18-maxpool-out-side.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
# NOW -- maxpool2d_layer.t27: a lowerable out_side(kernel, stride) for the nn-maxpool widget (2026-10-18)

## specs/ml/layers/maxpool2d_layer.t27 (Closes #10664)

- Why: gHashTag/trinity#1696 (course 10) was refused because the nn-maxpool widget hand-holds `K_OUT_SIDES = [2, 2, 3, 1]`; `out_size` takes a `MaxPool2DConfig` struct and is in `__NOT_LOWERED__`, so the widget had no compiled output side.
- `out_side(kernel, stride)` = `out_size(4, cfg(kernel, stride))` on two u32s; `scripts/t27-logic.mjs` now lowers 3 fns (`outSide`, `poolAt`, `backwardAt`), 4 not (`out_size`, `forward`, `backward`, `cfg`).
- Tests: the widget's four configs (2,2)->2, (3,1)->2, (2,1)->3, (4,1)->1; edges (1,1)->4, (3,2)->1, (1,3)->2 (floor division).
- t27c (bootstrap unchanged since 239b4b059), zig 0.16.0: test-report 7 of 7 pass, 0 vacuous, invariant proved; the compiled WASM returns the same seven values in node.
- Negative controls: 4 mutants of the fn body (side 5, stride forced to 1, stride dropped, ceiling division), 4 killed; the ceiling mutant is killed only by the edge test.
- Seal saved (`Maxpool2d.json`, `layers_Maxpool2d.json`).
- Not here: the re-vendor into trinity, `outSide(k, st)` in `nn-maxpool/tool.js`, dropping `K_OUT_SIDES` and its hand formula test.
22 changes: 22 additions & 0 deletions specs/ml/layers/maxpool2d_layer.t27
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,13 @@ module Maxpool2d;
return MaxPool2DConfig{ .kernel_size = kernel, .stride = stride, .padding = 0, .dilation = 1, .return_indices = true };
}

// The output side on the 4 x 4 fixture for a k x k window and a stride.
// out_size takes a MaxPool2DConfig struct and does not lower to WASM; this
// takes two integers, so a host reads the side from the compiled spec.
fn out_side(kernel: u32, stride: u32) -> u32 {
return out_size(4, cfg(kernel, stride));
}

// The 4 x 4 fixture
// 1 2 5 6
// 3 4 8 7
Expand Down Expand Up @@ -143,5 +150,20 @@ module Maxpool2d;
when others = backward_at(0) + backward_at(1) + backward_at(4) + backward_at(15)
then total == 10.0 and others == 0.0 and backward_at(13) == 3.0

// The four window/stride pairs the nn-maxpool widget offers, on the 4 x 4 fixture:
// 2 x 2 stride 2 -> 2, 3 x 3 stride 1 -> 2, 2 x 2 stride 1 -> 3, 4 x 4 stride 1 -> 1
test out_side_of_each_widget_config
given halved = out_side(2, 2)
when whole = out_side(4, 1)
then halved == 2 and out_side(3, 1) == 2 and out_side(2, 1) == 3 and whole == 1

// Edges: a 1 x 1 window at stride 1 keeps the side; a stride that does not
// divide (4 - k) rounds down (3 x 3 at stride 2 fits one window, 1 x 1 at
// stride 3 fits two)
test out_side_identity_and_floor
given same = out_side(1, 1)
when floored = out_side(3, 2)
then same == 4 and floored == 1 and out_side(1, 3) == 2

invariant maxpool_output_size_formula
assert out_size(4, cfg(2, 2)) == 2 and out_size(4, cfg(3, 1)) == 2 and out_size(5, cfg(2, 2)) == 2
Loading