modify PLRU to allow access to internals by formal proof