Repository navigation
det/CICS: READ / REWRITE / DELETE / UNLOCK TOKEN (update tokens; makes CBSA whole) #5078
Description
READ / REWRITE / DELETE with TOKEN (RLS / file-control update tokens) are refused by name. CBSA uses READ TOKEN and DELETE TOKEN in one program, which is otherwise one gap from whole.
Do: model UPDATE TOKEN semantics per IBM (READ UPDATE TOKEN returns a token; REWRITE/DELETE/UNLOCK TOKEN act on that record; INVREQ when the token doesn't match), in the oracle stub and the det port, with a register entry and scenarios over valid/invalid/reused tokens. Class sweep: UNLOCK TOKEN, READNEXT/READPREV UPDATE TOKEN.
Acceptance: the CBSA program translates whole; the token class is modelled or refused by name member by member.
Measured on origin/main 36671d5 (2026-10-13) over the 8 local corpora + 10 census clones (12 with CICS): cics_census.py survey --baseline --census-corpora <census> then proof_blockers.py <survey dir> --census-corpora <census> --json. 103 of 125 CICS programs translate whole; only 14 are proven (all CardDemo BMS).
Owner-approved re-ranking of the CICS queue by estate/program reach (2026-10-13).
🤖 Generated with Claude Code
Activity
CICS spec: UNLOCK is modelled; READNEXT / READPREV carry register X52…
CICS spec: UNLOCK engine access, det tests for the TOKEN class (Part of
squid-protocol commentedon Oct 14, 2026
Siblings: #5092 (tokenless INVREQ RESP2 28/30/31, from the PR #5090 review)
CICS: file update TOKEN (READ UPDATE / REWRITE / DELETE / UNLOCK TOKE…
squid-protocol commentedon Oct 14, 2026
Closing: PR #5090 meets the acceptance. CBSA DELCUS translates whole (det_survey 140/140 statements, port compiles), and the token class is modelled or refused by name member by member (register X52). Not covered here: end-to-end proof of DELCUS (no equivalence case yet) and UNLOCK without TOKEN, which is tracked in #5079.