diff --git a/nanvm-lib/todo/generated-rust-module-rustfmt-skip.md b/nanvm-lib/todo/generated-rust-module-rustfmt-skip.md
new file mode 100644
index 000000000..731b1ea88
--- /dev/null
+++ b/nanvm-lib/todo/generated-rust-module-rustfmt-skip.md
@@ -0,0 +1,71 @@
+## generated-rust-module-rustfmt-skip. Skip rustfmt once for the generated module
+
+**Priority:** P4
+**Status:** open
+
+### Problem
+
+`fjs/nanvm/rust/module.f.mjs` currently emits `#[rustfmt::skip]` before `eq`
+and each generated per-operation function in
+`nanvm-lib/tests/test/generated.rs`. The final `all` function is not currently
+annotated.
+
+The whole module is generated and intentionally uses one statement per test
+case. Formatting those generated functions is therefore not useful, and
+repeating the attribute at every function-emission site adds generated noise.
+
+The per-function skips are still necessary today: removing them without a
+replacement causes `cargo fmt` to rewrap generated assertions and destroys the
+one-statement-per-case layout.
+
+This follows the post-merge review comment on #1489 to make the formatting skip
+global for the generated module.
+
+### Proposal
+
+Do not use an inner `#![rustfmt::skip]` attribute inside `generated.rs`.
+Custom tool attributes in inner position are unstable on stable Rust and make
+`cargo check --tests` fail.
+
+Instead, annotate the generated module declaration in the hand-written
+`nanvm-lib/tests/test/main.rs`:
+
+```rust
+#[rustfmt::skip]
+mod generated;
+```
+
+Then stop emitting the repeated `#[rustfmt::skip]` attributes from
+`fjs/nanvm/rust/module.f.mjs`.
+
+This keeps one formatting-policy declaration for the whole generated module
+while remaining valid on stable Rust. The attribute belongs to `main.rs`, not
+to the generated file, so the generator should only stop emitting its
+per-function attributes; it should not try to emit a replacement inner
+attribute.
+
+A module-wide skip also covers `generated::all`, which is currently the one
+generated function without a `#[rustfmt::skip]` attribute. That broader skip is
+intentional: the entire module is generated and should be left byte-for-byte in
+the layout chosen by the generator.
+
+### Tasks
+
+- [ ] Add `#[rustfmt::skip]` to the `mod generated;` declaration in
+      `nanvm-lib/tests/test/main.rs`.
+- [ ] Stop emitting `#[rustfmt::skip]` before `eq` and individual generated
+      operation functions.
+- [ ] Do not emit `#![rustfmt::skip]` inside `generated.rs`.
+- [ ] Update comments/documentation in `fjs/nanvm/rust/module.f.mjs` to describe
+      the module-level formatting policy owned by `main.rs`.
+- [ ] Update the Rust generator proof if its expected output covers these
+      attributes.
+- [ ] Regenerate `nanvm-lib/tests/test/generated.rs` with `npm run ci-update`.
+- [ ] Verify a second `npm run ci-update` leaves the tree unchanged.
+- [ ] Run `fjs test`, `cargo check --tests`, `cargo test`, and
+      `cargo fmt -- --check`.
+
+### Related
+
+- #1489 — introduced the generated shared operator tests.
+- #1489 review: https://github.com/functionalscript/functionalscript/pull/1489#discussion_r3770843238
diff --git a/nanvm-lib/todo/operator-test-operation-model.md b/nanvm-lib/todo/operator-test-operation-model.md
new file mode 100644
index 000000000..2790b5abb
--- /dev/null
+++ b/nanvm-lib/todo/operator-test-operation-model.md
@@ -0,0 +1,129 @@
+## operator-test-operation-model. Describe operations by syntax and arity
+
+**Priority:** P3
+**Status:** open
+
+### Problem
+
+The shared operator corpus in `fjs/nanvm/` currently uses implementation-style
+names such as `unaryPlus`, `unaryMinus`, and `mul`:
+
+```ts
+export type Op = 'unaryPlus' | 'unaryMinus' | 'mul' | 'stringCoercion'
+```
+
+`Case.args` is also just `readonly Value[]`, so the type system does not connect
+an operation with its number of arguments. A unary operation can therefore be
+given two arguments, or a binary operation one argument, without a type error.
+
+The shared corpus should describe the JavaScript operation itself rather than
+the identifier chosen by a particular proof or code generator. Consumer-specific
+names such as Rust function names belong in the consumer.
+
+This follows the post-merge review discussion on #1489:
+
+- use operation spellings such as `+`, `-`, and `*` instead of `unaryPlus`,
+  `unaryMinus`, and `mul`;
+- associate every operation with its arity and use that arity to type its cases.
+
+### Proposal
+
+Represent an operation as a small immutable tuple containing its semantic name
+and argument count:
+
+```ts
+export type Operation<N extends number = number> =
+    readonly [name: string, argsN: N]
+```
+
+The corpus can then describe operations along these lines:
+
+```ts
+['+', 1]
+['-', 1]
+['*', 2]
+['String', 1]
+```
+
+The arity disambiguates operations that share syntax, such as unary `+` and a
+future binary `+`. The tuple keeps the shared data compact and makes the arity
+available directly as `O[1]` for types such as `Case<O[1]>`.
+
+Make `Case` generic over the argument count and use the existing fixed-length
+array machinery (`Tuple<N, T>`) so an operation's cases have exactly the right
+number of arguments:
+
+```ts
+export type Case<N extends number> = {
+    readonly name: string
+    readonly args: Tuple<N, Value>
+    readonly expected: Value
+    readonly rust?: string
+}
+```
+
+Keep the case `name`. It is diagnostic metadata and a stable proof key, not part
+of the operation semantics. The arguments and expected result are not sufficient
+as a unique key: for a commutative operation, a case with equal arguments is
+identical to its swapped form, so an expression such as `2 * 2 === 4` cannot
+distinguish the two entries. The current proof uses the case name and derives a
+`Swapped` suffix for the reversed order; preserve that explicit disambiguation
+rather than relying on `fromEntries` to silently collapse duplicate keys.
+
+Semantic expressions may still be generated as supplemental diagnostics. When
+doing so, render operands as faithful source literals so distinct values remain
+distinct (`123` versus `123n`, `0` versus `-0`, quoted strings, and so on), and
+use an explicit `Object.is(...)` form when `===` would describe the comparison
+incorrectly. Throwing cases should likewise use an explicit form such as
+`+0n throws`.
+
+Groups must preserve the operation's literal arity so their cases are typed as
+`Case<O[1]>`, where element `1` is the operation's `argsN`. The exact TypeScript
+shape may use generic groups or separate unary/binary group types; the important
+invariant is that invalid case arity is rejected statically.
+
+`commutative` only makes sense for binary operations. Prefer a type shape where
+it is available only for binary groups rather than a general optional property.
+
+The JavaScript proof and Rust printer should translate the semantic operation
+into their own implementation. In particular, the Rust printer must not derive
+Rust identifiers by applying `snakeCase` to punctuation such as `+`; it should
+own an explicit mapping from an operation plus arity to the Rust expression and,
+when needed, generated function name.
+
+Do not broaden this task into making strict equality (`===`) use the generic
+`Group` representation. `Eq` has shared-reference requirements today; it can be
+unified later if doing so becomes clearly useful. Its existing case representation
+is therefore outside this task as well.
+
+### Tasks
+
+- [ ] Replace the current string-union `Op` model with `readonly [name, argsN]`
+      operations carrying a semantic name and literal argument count.
+- [ ] Make `Case` generic over argument count while keeping its stable `name`,
+      and type `args` as a fixed-length tuple.
+- [ ] Keep case names as FunctionalScript proof keys and Rust assertion
+      diagnostics; keep the explicit `Swapped` disambiguation for reversed
+      commutative cases.
+- [ ] If semantic expressions are generated for diagnostics, render values as
+      faithful source literals and handle `Object.is`-sensitive and throwing
+      cases explicitly.
+- [ ] Make each group's cases derive their argument count from `operation[1]`.
+- [ ] Restrict `commutative` to binary groups.
+- [ ] Update `fjs/nanvm/module.f.mjs` to use semantic operation descriptions.
+- [ ] Update `fjs/nanvm/proof.f.mjs` to dispatch on the semantic operation and
+      arity while preserving unique case proof keys.
+- [ ] Update `fjs/nanvm/rust/module.f.mjs` to map semantic operations to Rust
+      syntax and generated identifiers without leaking those identifiers into
+      the shared data.
+- [ ] Add type-level coverage proving that wrong argument counts are rejected.
+- [ ] Regenerate `nanvm-lib/tests/test/generated.rs` and keep the generated test
+      behavior unchanged.
+- [ ] Run `npx tsc`, `fjs test`, `npm run ci-update`, `cargo test`,
+      `cargo clippy -- -D warnings`, and `cargo fmt -- --check`.
+
+### Related
+
+- #1489 — introduced the shared operator corpus.
+- #1489 review: https://github.com/functionalscript/functionalscript/pull/1489#discussion_r3770780551
+- #1489 review: https://github.com/functionalscript/functionalscript/pull/1489#discussion_r3770797058