Reassociating structured native execution proofs

Main results

• WordRAM.ExecWithin.seq_assoc: compose an already proved instruction block with the surrounding right-associated program, without repeating its execution proof.

Reassociation preserves the same data states and charged bound. This narrow proof-rule module avoids extending the interface of the widely imported structured-code core.

theorem Cslib.WordRAM.ExecWithin.seq_assoc {B : Basis} {r w T : ℕ} {a b c : Code B r} {x y : Data r} : ExecWithin w ((a.seq b).seq c) x y T ↔ ExecWithin w (a.seq (b.seq c)) x y T

Sequential blocks may be regrouped while preserving every instruction charge.