Gate typecheck in check, fix the AESWord annotation and the SRP group narrowing

[derek-miller]

lua-crypto was the one library where typecheck was not part of check, so this class of defect had no CI gate here at all. Gating it surfaces two real annotation defects.

aes_gcm.lua:313 — create_aes_word() returns a 4-element word but annotated its body @type AESState, which is [AESWord, AESWord, AESWord, AESWord]. The same copy-paste as the one fixed in lua-bthome-ble's aes_ccm.lua. Clearing it takes the repo from 11 findings to 6.

srp.lua:140-146 — group.g was read three times across a type(group.g) branch. Narrowing applies to locals, not table fields, so neither arm was narrowed and both bignum.from_number and bignum.from_hex saw the full string|integer union. Reading it into a local once fixes both. Same root cause as the test.expected hoist in lua-bitn.

The remaining four are deliberate negative tests that pass nil or an integer to assert the function rejects it, so the wrong type is the point. Those carry a scoped @diagnostic bypass rather than a signature change: a disable/enable pair around the three in ed25519.lua, and disable-next-line for the single one in srp.lua. The pair was checked for leakage by injecting a fault after the enable: line, which is caught.

Config carries the full bypass set the other four libraries now use, including runtime.plugin, which a grep of the diagnostics paths cannot surface: check_worker.lua does require 'plugin', so an OnSetText returning an empty edit blanks every file and the check passes having analysed nothing. diagnostics.disable is declared empty. #4 landed after this branch forked and deleted that key from main along with its unnecessary-assert entry, so keeping the branch side of the conflict would have silently reverted it. Confirmed inert here rather than merely absent: emptying the list by hand on the pre-merge head does not move the count.

CI installs lua-language-server 3.19.0 before Check, matching the other four.

Full test suite passes, including the SRP change: AES, AES-GCM, ChaCha20, Poly1305, SHA-256/512, BLAKE2, HKDF, SRP, bignum, X25519, X448, Ed25519 and the OpenSSL gating.

Separately, the HAP primitive set is now derived rather than recalled

You asked earlier whether the algorithms in #2 were all we need. That answer was from memory. Traced against pyatv's actual pair-setup and pair-verify call graph, which is the implementation verified against the real hardware:

Required	Provided
SRP-6a, RFC 5054 group 15 (3072-bit MODP, g=5), SHA-512	srp.GROUP_3072, the default
SHA-512	sha512
HKDF-SHA512, 7 distinct salt/info pairs	hkdf.derive("sha512", ...)
Ed25519 sign/verify	ed25519
X25519 ECDH	x25519
ChaCha20-Poly1305, 12-byte nonce	chacha20_poly1305, asserts 12
CSPRNG, 32 bytes for LTSK and session key	random, strong-or-raise

Nothing missing. One caveat worth recording: my first pass grepped crypto imports under auth/ and protocols/companion/ and found no AEAD at all, because ChaCha20-Poly1305 sits behind support/chacha20.py. Same failure mode as the config enumeration, one level up.

The nonce is 4 zero bytes || LE64 counter with separate in and out counters. That is caller logic, not a library gap. chacha20_poly1305 correctly takes a finished 12-byte nonce.

[derek-miller]

Merged main in to clear the conflict. #4 landed after I branched and dropped the whole diagnostics table along with the inert unnecessary-assert entry, so my commit message claim that disable "keeps its existing entry" was wrong. disable is now declared empty, which matches #4's finding while still closing the knob.

The resolution keeps the ignoreDir additions (.install, .lua, .luarocks) that the other four repos needed to stop the check descending into luarocks' own sources.

Still no problems found after the merge, and the full test suite passes.

[svc-finitelabs]

Reviewed at 66c99a1, after the merge from main. Verified end to end with lua-language-server 3.19.0, the same version the workflow installs. The three code changes are correct, and the conflict resolution is the right one. One item left, which I would fix before merging.

The merge resolved the one thing I was going to block on

I started this review at 13243b5, where diagnostics.disable still carried unnecessary-assert. That branch forked from 821ae5c, one commit before ce3e452 (#4) deleted exactly that key from main, so the PR body's line about "keeps its existing unnecessary-assert entry" was true of the base and no longer true of main. Keeping that side of the conflict would have silently reverted #4.

The merge commit took "disable": [], which is the correct resolution. Confirmed independently that it is inert here rather than merely absent: on the pre-merge head I emptied the list by hand and the count did not move, no problems found either way. So nothing was traded away to preserve #4.

Worth noting only because the PR body still asserts the entry is kept, and the body no longer describes the diff. Not load-bearing on the permanent record, since this repo squashes with COMMIT_MESSAGES, so the commit messages are what survive rather than the body.

The one item left: the Makefile comment now says the opposite of the code

Makefile:167-169, twenty lines above the check target this PR edits, still reads:

# Deliberately NOT part of `check`: a handful of type-narrowing and
# deliberate-bad-argument diagnostics remain, and turning CI red on those is a
# separate decision from making the check runnable.

That paragraph names the exact two categories this PR resolves, and the decision it defers is the decision this PR makes. It is now actively contradictory rather than merely stale, sitting directly above the target whose behaviour it misdescribes.

I am flagging it rather than waving it through because it is the same defect class #4 just spent a PR removing: dead documentation that "reads as a known exception to anyone changing this file later, so it is worse than nothing." A comment that states the previous policy as current is a strictly worse version of that. It is a three-line edit in a file already in the diff.

What I verified at 66c99a1

The gate is real, which is the part worth checking rather than assuming. lua-language-server --check exits non-zero when it finds anything, so this turns CI red rather than just running:

ref	result	exit
main	11 problems in 3 files	2
main + the AESWord line alone	6 problems in 2 files	2
66c99a1	no problems found	0

The 11 to 6 arithmetic is exact, and the residual 6 decompose the way the body says: ed25519.lua:1206,1207,1208 are three negative tests, srp.lua:142,145 are both arms of the un-narrowed group.g, and srp.lua:793 is the fourth negative test. Both arms appearing is what confirms the narrowing diagnosis, and hoisting into g_spec once is behaviour-preserving on a plain group table.

I checked that the two bypasses are scoped rather than assuming it, since a file-wide @diagnostic disable would hide real defects behind a green check:

• ed25519 uses a disable / enable pair, not the disable-next-line the body describes. I injected a real param-type-mismatch immediately after the enable: line and it was caught, so the pair brackets properly and does not leak to end of file.
• srp's disable-next-line covers exactly its one line. An injected bad call on the following line was caught.

Also clean: 21 Lua files in the repo and all 21 analysed, largest 108KB against the new preloadFileSize: 500, so that pin and maxPreload are headroom rather than silent skips. make test 15/15 including SRP-6a and Ed25519. make format-check clean.

One gap, stated so it does not read as covered: I could not run make lint, a broken luacheck rock under Lua 5.5 on my machine, so the luacheck third of check is unverified here. CI pins v2.1.0 through the action and covers it.

On the HAP table

Not code in this PR, so no verdict, but the support/chacha20.py miss is worth keeping in the log. It is the same enumeration failure as the config one, one level up, and it is why grepping imports keeps under-reporting.

Artifact

Comment rather than approval, held only on the Makefile paragraph. To be clear about what that does and does not mean: the code is correct and I verified every claim in the description, so this is not hedging on the change. Fix the comment and I will approve. Flagging separately that the head moved from 13243b5 to 66c99a1 while I was mid-review, so if anything else lands before I re-check, I will re-scope rather than approve a head I have not read.

[derek-miller]

Fixed at 382dc15. The paragraph now states the current policy and why the two categories no longer hold it out:

# Part of `check`, so CI enforces it. The type-narrowing and
# deliberate-bad-argument findings that held it out are resolved: the narrowing
# ones were real defects, and the bad-argument ones are negative tests carrying
# a scoped `@diagnostic` bypass.

You were right to hold on it rather than wave it through. It is worse than stale: it names the exact decision the diff makes and states the opposite as current, directly above the target it misdescribes. I grepped the repo for other statements of the old policy and found none.

Still no problems found after the edit.

Two corrections to the record, both yours:

The PR body is wrong about unnecessary-assert. It says the entry is kept; the merge took "disable": []. I noted that in a comment when I merged main in, but did not fix the body, so the body still misdescribes the diff. Thank you for confirming independently that the key is inert here rather than merely absent, which is the part I had not established before resolving the conflict that way. As you say, COMMIT_MESSAGES means the commit messages are the permanent record, and those are correct.

ed25519 uses a disable/enable pair, not disable-next-line. The body describes both as disable-next-line. Your bracketing test is the check I should have run myself, since a leaked file-wide disable is exactly how this change could have hidden real defects behind a green check.

On the HAP note: agreed, and it is logged. The support/chacha20.py miss and the runtime.plugin miss are the same failure, which is that I keep enumerating from a scope and then reporting the result as if it were the population. The config version of it cost four review rounds.

Noted on re-scoping if the head moves. Nothing else is queued for this branch, so 382dc15 should be the head you read.

[svc-finitelabs]

Approving. The Makefile paragraph is fixed at 382dc15, and that was the only thing I held on.

The delta is exactly the fix, and nothing rode along with it

382dc15 is a linear commit on top of 66c99a1, the head I reviewed, so this is not a force-push and the earlier verification still stands. The whole diff is Makefile, 4 insertions and 3 deletions, the one paragraph. No other file moved.

The replacement is accurate against the code rather than merely different: typecheck is in fact a prerequisite of check now, the narrowing findings were real defects, and the bad-argument ones do carry a scoped bypass. It also keeps the reason on the record instead of just deleting the stale claim, which is the part that makes it useful to the next person editing the target.

Worth more than the comment fix: this branch is behind main, and CI has not tested the combination

#6 merged 4c17f4a, vendoring bitn v0.6.1, at 18:13. That is after the head I reviewed at 17:58 and before this one at 18:36, so the branch never contained it. Every green check on this PR ran against the old bitn.

Normally that is unremarkable, but not for this PR specifically. vendor sits in ignoreDir and in workspace.library, so bitn is not itself diagnosed while its definitions still feed type resolution for everything under src/. This PR's entire purpose is to make that resolution CI-blocking. A vendored library bump is exactly the input that can move the new gate, and it is the one input the gate has not been run against.

So I built the merge locally rather than reasoning about it. It is a clean merge, vendor/bitn.lua only, 28 insertions and 15 deletions:

on the merge result	outcome
lua-language-server --check, 3.19.0, repo config	no problems found, exit 0
same, with an injected param-type-mismatch	caught, exit 1
make test	15/15 modules, including SRP-6a, Ed25519, OpenSSL gating
make format-check	clean, exit 0

The injected fault matters more than the green: a check that analyses nothing also exits 0, and runtime.plugin is the documented way for this config to silently do that. Appending a bad call to src/crypto/srp.lua turned it red, so the gate is live against the new bitn, not merely quiet. I restored the file and confirmed the tree was clean before running anything else.

Reassuring on the mechanism too: bitn carries zero ---@ annotations in both versions, so inference is the only channel it could have moved the count through, and it did not.

Net: the bitn bump does not break the gate. You do not need to merge main again to find that out, though GitHub may still ask you to for its own up-to-date requirement.

What I did not verify

make lint again, same broken luacheck rock under Lua 5.5 on my machine, so the luacheck third of check is unverified locally for the second round running. CI covers it, and all 11 checks are green at 382dc15 including Check itself.

The merge result is my local construction, not the merge GitHub will produce. Same parents and a clean strategy, so I expect them identical, but the record should say I tested a reconstruction.

Artifact

Formal approval this time, since the code is correct, the gate is real, and it holds against the newer main. Auto-merge is unarmed as I write this, so this approval does not merge anything on its own and the trigger stays yours.