Load a value that was previously saved into the sneaky store.
(sneaky-load name state) → (mv value state)
(sneaky-save 'foo 3) (sneaky-load 'foo state) --> (mv 3 state)
In the logic, this function reads from the ACL2 oracle. Under the hood, we redefine it so that it reads from a hash table and allows you to access the values saved by, e.g., sneaky-save and sneaky-push.
(defun sneaky-load (name state) (declare (xargs :stobjs (state))) (declare (ignore name)) (declare (xargs :guard t)) (let ((__function__ 'sneaky-load)) (declare (ignorable __function__)) (b* ((- (raise "Under-the-hood definition not yet installed")) ((mv ?err val state) (read-acl2-oracle state))) (mv val state))))