Find prohibited COBOL authorization identity origins

Trace equal-width character MOVEs into an explicitly configured authorization request. Report identity fields copied from sources forbidden by the approved provenance contract. The trace stops at unknown effects and unsupported control flow. Overwrites replace earlier origins. Missing origins do not establish trusted identity. The analysis does not prove reachability, authenticate a principal, validate the authorization result or change application behavior. Join ordinary sentences within one paragraph when the program has no NEXT SENTENCE or procedural COPY. Summarize a noniterative PERFORM of one uniquely resolved paragraph. Allow explicit IN or OF section qualifiers. Limit the expanded call tree and all branches to 64 statements. Record MOVE and PERFORM lines separately. Bound each origin to 64 combined copy and perform steps. Follow at most 16 active local paragraphs. Reject recursion and unresolved targets. Count repeated invocations separately. Supported IF and EVALUATE branches retain every alternative. Conditions count toward the statement limit. Limit combined caller and callee condition nesting to 16. Ranges, iterations, CALL statements and control transfers prevent a performed summary. Retain up to 16 possible copy chains across bounded IF branches with supported read-only conditions. Consider both outcomes and limit nesting to 16 IFs. Every possible origin must violate the configured contract before a finding is emitted. Mixed origins produce supporting evidence. An unknown branch or an exceeded bound discards the entire set. Follow character fields through equal-size group MOVEs only when complete byte spans align in supported DISPLAY records of at most 32767 bytes. Field names do not establish layout equivalence. Unmatched fields lose their origins. Also retain copy origins across supported EVALUATE branches. Every branch must establish a complete origin set. An absent WHEN OTHER includes the incoming state. Unknown alternatives invalidate the affected origin set. Integer selectors allow literal values and ranges. Character selectors allow character literals. TRUE and FALSE selectors use supported read-only conditions. Limit each selection to 64 WHEN labels and combined IF and EVALUATE nesting to 16 levels. Retain at most 16 origins and 64 steps per copy chain. No branch feasibility is inferred. 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.