Resource-certified step machines

Turing.StepMachine.ResourceCertificate gives charged plain certificates for the halting test and one step. Its compiler retains the original time, workspace, halting and output contracts; whole-run conclusions use uncharged Turing.MultiTapeTM.ComputableInBigO.

The realizing-machine constructions and normal-form proofs live in the internal machine kernel.