Propose COBOL COMMAREA write length guards

Guard a direct character MOVE into an incoming COMMAREA under an explicit policy that only received bytes are writable. Require exact caller and ordinary COPY snapshots, a complete admitted entry interval and an approved existing terminal exit. Derive the required count from the destination offset and its full width, including MOVE padding. Require an admitted short entry to reach the original write. Preserve that conditional finding when an unresolved exit or layout prevents an edit. Propose a guard only when every arrival has an unchanged actual count and at least one accepted arrival remains. Insert a typed IF sentence before an ordinary single-MOVE sentence on its own fixed-format line. Preserve every original byte outside the guard. Reprove the changed program at the same MOVE. Require exactly the original accepted arrivals and no short or unknown arrivals. Keep native counts above 9999, aliases, unknown effects, alternate entries, NEXT SENTENCE, unsupported layouts and incomplete source unresolved. The contract establishes the intended writable extent and exit suitability. The proof does not establish allocation size, caller execution or a runtime crash. Application-team review remains required. Do not truncate writes or add retries, commits, rollbacks, ABEND or new error routines. 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.