fix typo that made proof weaker than it ought to be
strengthen fourslot_write proof
clean up the fourslot_read proof/impl under similar principles