From 93019c5cb9d1b52b5b21ce814b969f9a2584f166 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 18 Oct 2026 21:28:40 +0000 Subject: [PATCH] spec(maxpool2d_layer): a lowerable out_side(kernel, stride) for the nn-maxpool widget (Closes #10664) gHashTag/trinity#1696 (course 10) was refused because the nn-maxpool widget hand-holds K_OUT_SIDES = [2, 2, 3, 1]. Those are out_size(4, cfg(k, s)), but out_size takes a MaxPool2DConfig struct and does not lower to WASM. - out_side(kernel: u32, stride: u32) -> u32 returns out_size(4, cfg(kernel, stride)); t27-logic.mjs lowers it as outSide. - Tests: the widget's four configs (2,2)->2, (3,1)->2, (2,1)->3, (4,1)->1, and the edges (1,1)->4, (3,2)->1, (1,3)->2. - test-report 7 of 7 pass, 0 vacuous; 4 mutants of the fn, 4 killed. - Seal saved; NOW entry in docs/now/. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01ScHVrGSr6zZUdwkdC8DR9k --- .trinity/seals/Maxpool2d.json | 16 ++++++++-------- .trinity/seals/layers_Maxpool2d.json | 20 ++++++++++---------- docs/now/2026-10-18-maxpool-out-side.md | 11 +++++++++++ specs/ml/layers/maxpool2d_layer.t27 | 22 ++++++++++++++++++++++ 4 files changed, 51 insertions(+), 18 deletions(-) create mode 100644 docs/now/2026-10-18-maxpool-out-side.md diff --git a/.trinity/seals/Maxpool2d.json b/.trinity/seals/Maxpool2d.json index f05807418e..89c3de8174 100644 --- a/.trinity/seals/Maxpool2d.json +++ b/.trinity/seals/Maxpool2d.json @@ -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 } } \ No newline at end of file diff --git a/.trinity/seals/layers_Maxpool2d.json b/.trinity/seals/layers_Maxpool2d.json index f344b261e7..b91d2939ba 100644 --- a/.trinity/seals/layers_Maxpool2d.json +++ b/.trinity/seals/layers_Maxpool2d.json @@ -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", @@ -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" } } \ No newline at end of file diff --git a/docs/now/2026-10-18-maxpool-out-side.md b/docs/now/2026-10-18-maxpool-out-side.md new file mode 100644 index 0000000000..ae4d464cc6 --- /dev/null +++ b/docs/now/2026-10-18-maxpool-out-side.md @@ -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. diff --git a/specs/ml/layers/maxpool2d_layer.t27 b/specs/ml/layers/maxpool2d_layer.t27 index 6841238ca8..7b972a41a5 100644 --- a/specs/ml/layers/maxpool2d_layer.t27 +++ b/specs/ml/layers/maxpool2d_layer.t27 @@ -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 @@ -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