Concrete disjoint memory regions and derived native fits #
Main results #
BandPreparation.workspace_le_snapshot: protected data are above the complete encoder.BandPreparation.memory_fits: the actual allocation end fits the explicit input budget.BandPreparation.tables_fit,BandPreparation.split_fits,BandPreparation.encoder_fits: component inequalities derived from the same budget, without an intermediate-state oracle.
The native input prefix is disjoint from its protected copy.
The encoder's complete low workspace is below the protected original input.
The protected original-input copy ends exactly at the inverse table.
The inverse table ends exactly at the selected-mask table.
The selected-mask table ends exactly at the shared output catalogue.
The catalogue base is below the complete allocation end, including an empty catalogue.
The protected prefix ends below every table/output allocation.
The snapshot base is within the complete allocation.
The constant margin in the original budget covers all fixed program constants.
The entire real allocation, including both catalogue halves, fits the original numerical word-budget inequality. The sizes of unreachable padded row-major products are irrelevant.
Both table-store addresses and all population/count arithmetic fit before table execution.
Every original band index admits the already proved native digit-loop fits.
The unchanged native encoder's arithmetic/address premise follows from this client's explicit original-parameter bound. Its signed magnitude premise remains separate.