Sync-ephemeral-whs-with-persistent-whs
establishing wormhole coherence
General Form:
(sync-ephemeral-whs-with-persistent-whs name state)
where name is the quoted name of a wormhole other than one of
the built-in ACL2 system wormholes. It is forbidden to invoke
sync-ephemeral-whs-with-persistent-whs on the names listed in the
constant *protected-system-wormhole-names* which includes brr (the
break-rewrite wormhole name), accumulated-persistence, and
fc-wormhole (the name of the wormhole managing forward-chaining-reports), among others.
If executed on the live state and while in the named wormhole, this
function moves the wormhole's status from the persistent-whs (located in that
part of the memory outside of ACL2's state) to the ephemeral-whs (the value
of the state global variable wormhole-status). Subsequently,
name's persistent-whs is equal to its ephemeral-whs: the name
wormhole is coherent. If executed on a state other than the live one or
while outside of the named wormhole, this function is a no-op. Of course,
the next time the name wormhole is entered it will be in a coherent
state since entry to a wormhole initializes the wormhole-status to the
persistent-whs. sync-ephemeral-whs-with-persistent-whs returns the new
state.
Logically speaking, this function uses read-ACL2-oracle to obtain
the wormhole's hidden status. So the output state is almost certainly
different than the input state.
See wormhole-programming-tips for some tips for using this
function.
