Propose COBOL COMMAREA copy length guards

Propose a received-length check for application-team review before a direct character MOVE from an incoming COMMAREA. Bind the entry interval and approved existing exit to an exact source path, program, SHA-256 and MOVE line. Derive the required count from the source field offset, literal slice and receiving width. Preserve the MOVE and its padding behavior. Require a concrete short-entry witness and fully known arrivals with an unchanged actual count. Reject unresolved native counts above 9999 and intervals beyond the declared incoming extent. Insert a separate typed IF sentence before a single-statement MOVE sentence on its own fixed-format line. Send insufficient counts through the approved paragraph only when its bounded jump path reaches GOBACK or plain CICS RETURN. Preserve existing messages, sentences and periods. Require ordinary complete source, unaliased storage and validated data copies. Aliases, source switches, alternate ENTRY statements, NEXT SENTENCE, unknown arrivals, unsupported layouts and unproven exits prevent changes and produce explicit barriers. The contract establishes caller admission and exit suitability. The proof establishes the local read extent and terminal path. The proposal does not infer exact-length caller conventions, truncate a copy, add an error routine or change transaction policy. Approved terminal paths may contain bounded literal MOVE stores into validated local scalar fields. Stores require complete ordinary source and unaliased storage. Preserve every existing assignment. Also permit bounded default INITIALIZE on these terminal jump paths. Validate at most 16 local fields or groups and 64 elementary writes. Require complete ordinary unaliased storage. Integer defaults are zero and PIC X defaults are spaces within 256 characters per field. VALUE and FILLER phrases, replacement phrases, FILLER members, tables and unsupported storage prevent this proof. An explicit TO DEFAULT retains default behavior. Preserve every initialization and message before the existing terminal. Preserve known received counts after a supported incoming-area MOVE or plain character DISPLAY only when they cover its complete read extent. Keep paths with an earlier short read unknown. They cannot authorize a later guard insertion. Successful output remains unproven. Require every expanded data COPY to match its separately approved original content hash. Caller hashes do not approve copybook contents. Missing, stale or extra COPY approvals prevent findings and edits. An omitted COPY map approves only a program without COPY references.