Don't always require an action state extension proof

[L-as]

Any place where you check X -> Y, check instead X -> Y', Y' -> Y, where X -> Y' is validated with a proof, and Y' -> Y is done in-circuit (and is thus limited). If X = Y' then you can omit checking the proof, accepting a dummy proof, and saving prover time.