Module programming 

Operand-checked evidence for application update range selection.

Selection is not a write proof: the caller must bind the total-length source and establish that the programming call consumes the selected cells. In particular, matching a header does not imply that boot is preserved.

Structs

AcceptanceTail

Operand-bound acceptance checks and programming arguments.

IntegritySelection

Calls and branches selecting optional boot CMAC and mandatory application CMAC. The referenced checker routines still require independent validation.

PlainSignature

A direct staged-byte signature comparison following range selection. Every instruction between selection and comparison is checked: there is no intervening decoder call on this path. Earlier stream effects remain a separate obligation.

ReservedSkips

Complete checked skip branches and their register preconditions.

Selection

Both branches of the legacy application’s update-bit-zero range selection.

Functions

inspect_acceptance_tail

Match both validation branches and every instruction of the success path. This proves argument use, not the independently called helper bodies.

inspect_legacy_integrity

Establish the legacy application’s complete boot/application CMAC choice. Clearing update bit zero skips the boot checker, never the application one.

inspect_legacy_selection

Match all instructions, both branches, literals and the branch join. This compiler form selects start zero when MMIO bit zero is set, otherwise 0x10000; it always stores length total - start. Other forms return None.

inspect_plain_signature

Bind the legacy direct signature loop to an independently matched selection. This establishes a plaintext constraint, not acceptance of the whole image.

inspect_reserved_skips

Check every instruction in both reserved-region branches. r7/r6/r5 must separately be established as destination/source/remaining pointers, and r4 must equal 0x10000. Matching this component alone does not establish a loop.

inspect_selection

Inspect either established compiler form, rejecting ambiguous matches.