Find COBOL COMMAREA display lengths

Prove direct DISPLAY reads beyond the received COMMAREA under an explicit entry contract. Accept one plain character field or fixed DISPLAY group operand. Include its byte offset in the required incoming length. Allow table-free slices with positive literal positions and lengths within the declaration. An omitted length extends to the field end. Follow bounded received-length conditions, normal paragraph fallthrough and direct jumps to unique labels. Preserve admitted length sets through modeled disjoint literal assignments and literal-only DISPLAY messages. Earlier unsupported effects, unknown calls and length or area changes prevent a witness on that path. Multiple operands, functions, output options, exception clauses, dynamic slices and elementary numeric conversions remain unsupported. Require complete source and an unaliased fixed layout. Record the smallest admitted short length that reaches the read. This does not prove successful output, sensitive-data exposure, caller reachability or allocation size. Missing findings do not establish safety. Do not change output, truncate data or invent a failure exit. Preserve incoming lengths across supported SET condition-name TO TRUE assignments to separate ordinary standalone fields. Every target must be disjoint from the received length. Validate all declarations and targets under the existing 16-target and 64-value limits. Writes to the byte count or incoming area and unsupported SET forms remain flow barriers. Setting an error flag does not reject an entry. Preserve incoming lengths across plain INITIALIZE of disjoint ordinary local fields and groups. Validate all targets and members within 16 targets and 64 elementary writes. Writes to the received count or incoming area, unknown targets, aliases and unsupported storage remain flow barriers. Replacement phrases are not modeled. Initializing an error record does not reject short input or establish received bytes. Follow numeric EVALUATE of the configured received count with at most 64 literal WHEN choices and 16 nested selections. Support integer literals of at most 18 digits, inclusive ascending THRU ranges and shared WHEN choices. Use the first matching branch. Unmatched lengths take WHEN OTHER or continue after END-EVALUATE. Validate every label before selecting any branch. Other subjects, ALSO, variable bounds and unsupported choices remain barriers. Branch effects keep their existing rules. Unknown paths do not manufacture received-length witnesses. Follow GO TO paragraph targets qualified by IN or OF when both the named section and its paragraph are unique. Use the resolved declaration, including empty paragraphs and backward jumps. Ambiguous sections, duplicate paragraphs within a section, missing targets and computed jumps remain flow barriers. Qualification does not bypass existing source, storage or statement-effect checks. Preserve incoming lengths across bounded STRING DELIMITED BY SIZE into separate ordinary PIC X storage. Require every field operand to be ordinary local storage and the complete write to fit its receiver. Limit operands to 16 and fields to 256 characters. Writes to the received count or incoming area, direct incoming-area reads, overlap, pointers, overflow handlers and unsupported forms remain barriers. Constructing an error message does not reject an entry or establish received bytes. Treat exact EXEC CICS RETURN END-EXEC without options as leaving the current CICS logical level. Remove only the incoming lengths that take that branch. Preserve earlier access witnesses and unresolved effects. This does not establish whole-task termination. Other RETURN forms remain unsupported. Accept the standard system-supplied DFHEIBLK.EIBCALEN group member under an explicit entry contract. Require ordinary source, unique translator fields and disjoint incoming storage. Accept plain resolved data COPY declarations after validating their source and expanded declaration words. Reject replacement and library phrases, nested copies, procedural copies, explicit interface copies and copied directives. Custom interface declarations, shadow fields, aliases and source-mode barriers remain unsupported. Retain concrete native counts through 9999 when a larger entry interval is admitted. Represent the rest as unknown without manufacturing witnesses. When no concrete short witness is proven and higher counts remain unmodeled, report UNRESOLVED_ENTRY_LENGTHS. That status does not claim an unknown path reaches the operation. Native halfword capacity does not establish compiler comparison semantics above 9999. Writes to the field or its enclosing interface invalidate the entry value. The contract still supplies caller admission and actual received-count meaning. INITIALIZE VALUE and FILLER phrases require a separate effect proof and discard default-assignment facts. An explicit TO DEFAULT without a VALUE, FILLER or replacement phrase retains the default behavior. 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.