more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
tuned;

less ambitious memo_eval, since memo_result is still not robust here;

less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;

more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
edit of perspective touches node superficially, to ensure revisit after update;

Command.memo including physical interrupts (unlike Lazy.lazy);
re-assign unstable exec, i.e. reset interrupted transaction;
node result as direct exec -- avoid potential interrupt instability of Lazy.map;

tuned;

tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;

proper signature constraint;

tuned comments;

separate module for prover command execution;