text: abstract function, written in acl2, about which we can readily prove interesting correctness
  properties. in the extensive code documentation for codewalker, the system is described as follows [18]:
  two main facilities are provided by codewalker: the abstraction of a piece of code into an
  acl2 “semantic function” that returns the same machine state, and the “projection” of such
  a function into another function that computes the final value of a given state component
  using only the values of the relevant initial state components.