python: verify the two gate facts (frame reader, KeyboardInterrupt) #1384

Created with Claude Code from the spec in #1341.

Parent

Sub-issue of #1341. Ticket 3 of 14.

What to build

Two written findings, each with the probe code that proved it, committed under the Python workspace's docs. The spec (#1341, Further Notes) names two facts the design assumes but nobody has verified:

1. vitaminc-aead-frame exposes a reader the extension can use to walk a stored frame and recover the value kind without decrypting. The decrypt preflight (DECRYPT_FOREIGN_ROW, DECRYPT_MALFORMED) depends on this.
2. With the GIL released around a blocking engine call, a KeyboardInterrupt lands only after the detached call returns, and an early-dropped Pending future wipes its buffers. The sync-and-GIL contract depends on this.

If either is false, draft the amendment to #1341 as a comment on #1341 in this ticket and name which downstream tickets change (the decrypt ticket, the concurrency ticket).

Amendment, 28 October 2026: the wording of fact 1

Fact 1 says the extension can "recover the value kind without decrypting". That is not possible for a sealed value. The kind of a sealed value is stored inside its encryption, so only decrypting shows it. The doc comment on dynamic::decrypt in packages/stack-encrypt/src/dynamic/record.rs says the same: "the type tag is inside the AEAD envelope, so only opening can see it."

Read fact 1 as follows instead: the extension can walk the record frame that stack_encrypt::dynamic::decrypt returns, and recover each field's value kind. The extension needs only the public API of stack-encrypt, with no new engine code.

Fact 1 also says that the decrypt preflight (DECRYPT_FOREIGN_ROW, DECRYPT_MALFORMED) depends on it. That is not correct either. Neither check needs the value kind:

• DECRYPT_FOREIGN_ROW compares the stored i value with the expected table and column. The i value is plain JSON.
• DECRYPT_MALFORMED checks that the column value parses as EQL JSON.

What depends on fact 1 is the step after decrypting: building model instances from the opened record, and the DECRYPT_KIND_MISMATCH check.

The design does not change. The spec in #1341 already checks the kind after decrypting, so #1341 needs no amendment for fact 1.

Acceptance criteria

• A findings file for each fact: what was probed, on which commit of the dependency, the result, and the probe code or a pointer to it.
• The probes are either committed as tests in the engine crate or recorded as throwaway with their output pasted.
• If a fact is false, a comment on Python SDK: core call over psycopg, on EQL v4 and Stack Encrypt #1341 states the amendment and the affected tickets.
• The decrypt and concurrency tickets are updated (comment) with "gate facts confirmed" or the amendment.