Analyze copied classified data in TSQ writes

Trace classified character values into supported WRITEQ TS source buffers. The scoped contract must prohibit queue write requests containing these values or their copies and establish disjoint incoming and local storage. Require a literal length from 1 through 32763 within the complete source layout and prove that it includes the whole copied field. Support ordinary fixed DISPLAY records with character and unsigned integer fields up to 32767 bytes. Partial fields, unknown lengths, aliases, incomplete source and unknown copy histories remain unresolved. Follow at most 16 active local paragraphs. Allow explicit IN or OF section qualifiers. Reject recursion and unresolved targets. Count repeated invocations separately. Summarized paragraphs may contain supported IF and EVALUATE branches. Count all statements across every branch and expanded call toward a limit of 64. Limit combined caller and callee condition nesting to 16. Unknown calls and control transfers prevent summaries. Retain at most 16 origins through supported IF and EVALUATE branches and 64 MOVE and summarized PERFORM steps per chain. Every origin must violate the supplied classification for a finding. Mixed origins are reported without a finding. Report a queue write contract violation without inferring queue accessibility, successful storage, reachability or a CWE. Do not delete writes, shorten records, mask data or change queue lifecycle and transaction behavior. Produce evidence without marking source. Simple EXIT and CONTINUE preserve local facts. Other EXIT forms remain outside this proof. Plain DISPLAY of quoted ASCII text preserves local fields and does not inspect a status value or terminate processing. Accept at most 16 literals of at most 256 characters each. Device options, screen positioning, exception clauses, field reads and functions remain barriers. Supported SET condition-name TO TRUE statements overwrite their parent fields and discard those copy origins. Preserve unrelated origins. Validate every declaration and target before applying assignments from left to right. Limit each SET to 16 condition names and each declaration to 64 value intervals. Unsupported forms discard local facts. Model plain INITIALIZE of at most 16 ordinary fields or groups. Validate every member before applying at most 64 elementary writes. Supported integers become zero and PIC X fields of at most 256 characters become spaces. Declaration VALUE clauses do not supply these values. Discard overwritten copy origins and cached ancestor origins. Preserve unrelated origins. FILLER members, OCCURS, replacement phrases and unsupported storage prevent this proof. Validate STRING DELIMITED BY SIZE with at most 16 nonoverlapping ASCII literal or ordinary PIC X sources and a receiver of at most 256 characters. Require all transfers to fit without a pointer or overflow handler. Preserve unrelated local facts. Construct character values only from known sources and retain the previous unwritten suffix. An unknown suffix remains unknown. Bound character sets to 16 values and evidence to 64 steps. A STRING receiver loses its complete-copy origin. This does not prove that sensitive substrings were erased. 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.